%------------------------------------------------------------------------------
% File     : SWX186+1 : TPTP v9.3.0. Released v9.3.0.
% Domain   : Software Verification
% Problem  : A faulty property of the function drop
% Version  : Especial.
% English  :

% Refs     : [CST26] Claessen et al. (2026), Email to Geoff Sutcliffe
% Source   : [CST26]
% Names    : Definitions_prop_drop_inj2.p [CST26]

% Status   : Theorem
% Rating   : 0.00 v9.3.0
% Syntax   : Number of formulae    :    9 (   8 unt;   0 def)
%            Number of atoms       :   10 (  10 equ)
%            Maximal formula atoms :    2 (   1 avg)
%            Number of connectives :    4 (   3   ~;   0   |;   0   &)
%                                         (   0 <=>;   1  =>;   0  <=;   0 <~>)
%            Maximal formula depth :    6 (   3 avg)
%            Maximal term depth    :    3 (   1 avg)
%            Number of predicates  :    1 (   0 usr;   0 prp; 2-2 aty)
%            Number of functors    :    8 (   8 usr;   2 con; 0-2 aty)
%            Number of variables   :   16 (  13   !;   3   ?)
% SPC      : FOF_THM_RFO_PEQ

% Comments :
%------------------------------------------------------------------------------
fof(axiom_001,axiom,
    ! [X,X2] : head(cons(X,X2)) = X ).

fof(axiom_002,axiom,
    ! [X,X2] : tail(cons(X,X2)) = X2 ).

fof(axiom_003,axiom,
    ! [X,X2] : nil != cons(X,X2) ).

fof(axiom_004,axiom,
    ! [X] : proj1S(s(X)) = X ).

fof(axiom_005,axiom,
    ! [X] : s(X) != z ).

fof(axiom_006,axiom,
    ! [Z] : drop(s(Z),nil) = nil ).

fof(axiom_007,axiom,
    ! [Z,X2,X3] : drop(s(Z),cons(X2,X3)) = drop(Z,X3) ).

fof(axiom_008,axiom,
    ! [Y] : drop(z,Y) = Y ).

fof(goal_009,conjecture,
    ? [N,Xs,Ys] :
      ~ ( drop(N,Xs) = drop(N,Ys)
       => Xs = Ys ) ).

%------------------------------------------------------------------------------