%------------------------------------------------------------------------------
% File : LisaTT---0.9.1
% Problem : SWX206+1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : java -cp /export/starexec/sandbox2/solver/bin/lisa-assembly-0.9.jar TPTP_Lisa tableau --input /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n018.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Apr 29 02:35:38 PM UTC 2026
% Result : Theorem 1.77s 1.13s
% Output : Proof 1.77s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(axiom_001,axiom,
! [X] : proj1S(s(X)) = X ).
fof(axiom_002,axiom,
! [X] : z != s(X) ).
fof(axiom_003,axiom,
! [Y] : x2(z,Y) = Y ).
fof(axiom_004,axiom,
! [Y,N] : x2(s(N),Y) = s(x2(N,Y)) ).
fof(s0,plain,
( [ x2(z,z) = z,x2(z,z) != z ]
--> [ ] ),
inference(restate_true,[status(thm)],[]) ).
fof(s1,plain,
( [ x2(z,z) = z,
! [X] : x2(X,X) != X ]
--> [ ] ),
inference(left_forall,[status(thm)],[s0]) ).
fof(s2,plain,
( [ ! [X] : x2(X,X) != X,
! [Y] : x2(z,Y) = Y ]
--> [ ] ),
inference(left_forall,[status(thm)],[s1]) ).
fof(s3,plain,
( [ ! [X] : x2(X,X) != X,
( ! [Y,N] : s(x2(N,Y)) = x2(s(N),Y)
& ! [X] : s(X) != z
& ! [X] : proj1S(s(X)) = X
& ! [Y] : x2(z,Y) = Y ) ]
--> [ ] ),
inference(weakening,[status(thm)],[s2]) ).
fof(s4,plain,
( [ ( ! [Y,N] : s(x2(N,Y)) = x2(s(N),Y)
& ! [X] : s(X) != z
& ! [X] : proj1S(s(X)) = X
& ! [Y] : x2(z,Y) = Y
& ! [X] : x2(X,X) != X ) ]
--> [ ] ),
inference(weakening,[status(thm)],[s3]) ).
fof(s5,plain,
( [ ( ! [Y,N] : s(x2(N,Y)) = x2(s(N),Y)
& ! [X] : s(X) != z
& ! [X] : proj1S(s(X)) = X
& ! [Y] : x2(z,Y) = Y
& ! [X] : x2(X,X) != X ) ]
--> [ ] ),
inference(weakening,[status(thm)],[s4]) ).
fof(s6,plain,
( [ ! [X] : proj1S(s(X)) = X,
! [X] : z != s(X),
! [Y] : x2(z,Y) = Y,
! [Y,N] : x2(s(N),Y) = s(x2(N,Y)) ]
--> [ ? [X] : x2(X,X) = X ] ),
inference(restate,[status(thm)],[s5]) ).
fof(final,theorem,
? [X] : x2(X,X) = X,
inference(big_cut,[status(thm)],[axiom_001,axiom_002,axiom_003,axiom_004]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.11 % Problem : SWX206+1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.12 % Command : java -cp /export/starexec/sandbox2/solver/bin/lisa-assembly-0.9.jar TPTP_Lisa tableau --input /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.15/0.33 % Computer : n018.cluster.edu
% 0.15/0.33 % Model : x86_64 x86_64
% 0.15/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.33 % Memory : 8042.1875MB
% 0.15/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.33 % CPULimit : 300
% 0.15/0.33 % WCLimit : 300
% 0.15/0.33 % DateTime : Wed Apr 29 00:57:01 EDT 2026
% 0.15/0.33 % CPUTime :
% 1.77/1.13 % SZS status Theorem
% 1.77/1.15 % SZS output start Proof
% See solution above
%------------------------------------------------------------------------------