%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SWX185+1 : TPTP v9.3.1. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n010.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 03:32:03 PM UTC 2026
% Result : Theorem 21.95s 3.67s
% Output : Proof 21.95s
% Verified :
% SZS Type : Refutation
% Derivation depth : 27
% Number of leaves : 12
% Syntax : Number of formulae : 81 ( 65 unt; 0 def)
% Number of atoms : 97 ( 96 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 41 ( 25 ~; 12 |; 0 &)
% ( 0 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 2 avg)
% Maximal term depth : 4 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 15 ( 15 usr; 4 con; 0-2 aty)
% Number of variables : 133 ( 27 sgn 70 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f31,axiom,
! [A2,B2] : assoc(x2(A2,B2)) = x2(assoc(A2),assoc(B2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_032) ).
fof(f31_nnf,plain,
! [A2,B2] : assoc(x2(A2,B2)) = x2(assoc(A2),assoc(B2)),
inference(nnf_transformation,[status(thm)],[f31]) ).
fof(f31_sk,plain,
! [A2,B2] : assoc(x2(A2,B2)) = x2(assoc(A2),assoc(B2)),
inference(skolemisation,[status(esa)],[f31_nnf]) ).
cnf(c31,plain,
assoc(x2(X0,X1)) = x2(assoc(X0),assoc(X1)),
inference(cnf_transformation,[status(esa)],[f31_sk]) ).
fof(f37,axiom,
! [A3,B2] : lin(x2(A3,B2)) = append(lin(A3),append(cons(mul,nil),lin(B2))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_038) ).
fof(f37_nnf,plain,
! [A3,B2] : lin(x2(A3,B2)) = append(lin(A3),append(cons(mul,nil),lin(B2))),
inference(nnf_transformation,[status(thm)],[f37]) ).
fof(f37_sk,plain,
! [A3,B2] : lin(x2(A3,B2)) = append(lin(A3),append(cons(mul,nil),lin(B2))),
inference(skolemisation,[status(esa)],[f37_nnf]) ).
cnf(c37,plain,
lin(x2(X0,X1)) = append(lin(X0),append(cons(mul,nil),lin(X1))),
inference(cnf_transformation,[status(esa)],[f37_sk]) ).
fof(f34,axiom,
! [X] :
( X != x2(proj12(X),proj22(X))
=> linTerm(X) = lin(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_035) ).
fof(f34_nnf,plain,
! [X] :
( linTerm(X) = lin(X)
| X = x2(proj12(X),proj22(X)) ),
inference(nnf_transformation,[status(thm)],[f34]) ).
fof(f34_sk,plain,
! [X] :
( linTerm(X) = lin(X)
| X = x2(proj12(X),proj22(X)) ),
inference(skolemisation,[status(esa)],[f34_nnf]) ).
cnf(c34,plain,
( linTerm(X0) = lin(X0)
| X0 = x2(proj12(X0),proj22(X0)) ),
inference(cnf_transformation,[status(esa)],[f34_sk]) ).
fof(f25,axiom,
! [X,X2] : x2(X,X2) != eX,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_026) ).
fof(f25_nnf,plain,
! [X,X2] : x2(X,X2) != eX,
inference(nnf_transformation,[status(thm)],[f25]) ).
fof(f25_sk,plain,
! [X,X2] : x2(X,X2) != eX,
inference(skolemisation,[status(esa)],[f25_nnf]) ).
cnf(c25,plain,
x2(X0,X1) != eX,
inference(cnf_transformation,[status(esa)],[f25_sk]) ).
cnf(p83,plain,
( X0 != eX
| linTerm(X0) = lin(X0) ),
inference(superposition,[status(thm)],[c34,c25]) ).
cnf(p115,plain,
linTerm(eX) = lin(eX),
inference(equality_resolution,[status(thm)],[p83]) ).
fof(f38,axiom,
lin(eX) = cons(x,nil),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_039) ).
fof(f38_nnf,plain,
lin(eX) = cons(x,nil),
inference(nnf_transformation,[status(thm)],[f38]) ).
cnf(c38,plain,
lin(eX) = cons(x,nil),
inference(cnf_transformation,[status(esa)],[f38_nnf]) ).
fof(f33,axiom,
! [Y,Z,Xs] : append(cons(Z,Xs),Y) = cons(Z,append(Xs,Y)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_034) ).
fof(f33_nnf,plain,
! [Y,Z,Xs] : append(cons(Z,Xs),Y) = cons(Z,append(Xs,Y)),
inference(nnf_transformation,[status(thm)],[f33]) ).
fof(f33_sk,plain,
! [Z,Xs,Y] : append(cons(Z,Xs),Y) = cons(Z,append(Xs,Y)),
inference(skolemisation,[status(esa)],[f33_nnf]) ).
cnf(c33,plain,
append(cons(X1,X2),X0) = cons(X1,append(X2,X0)),
inference(cnf_transformation,[status(esa)],[f33_sk]) ).
cnf(p69,plain,
append(lin(eX),X0) = cons(x,X0),
inference(superposition,[status(thm)],[c38,c33]) ).
cnf(p71,plain,
cons(x,nil) = lin(eX),
inference(superposition,[status(thm)],[c38,p69]) ).
cnf(p122,plain,
lin(eX) = linTerm(eX),
inference(superposition,[status(thm)],[p115,p71]) ).
cnf(p226,plain,
lin(x2(eX,X0)) = cons(x,cons(mul,lin(X0))),
inference(superposition,[status(thm)],[p122,c37]) ).
cnf(p236,plain,
lin(x2(eX,eX)) = cons(x,cons(mul,linTerm(eX))),
inference(superposition,[status(thm)],[p122,p226]) ).
cnf(p245,plain,
append(lin(x2(eX,eX)),X0) = cons(x,cons(mul,cons(x,X0))),
inference(superposition,[status(thm)],[p236,c33]) ).
cnf(p121,plain,
append(linTerm(eX),X0) = cons(x,X0),
inference(superposition,[status(thm)],[p115,p69]) ).
cnf(p286,plain,
cons(x,cons(mul,cons(x,X0))) = append(lin(x2(eX,eX)),X0),
inference(superposition,[status(thm)],[p245,p121]) ).
cnf(p321,plain,
lin(x2(eX,x2(eX,X0))) = lin(x2(x2(eX,eX),X0)),
inference(superposition,[status(thm)],[c37,p286]) ).
fof(f40,conjecture,
? [U,V] :
~ ( lin(U) = lin(V)
=> assoc(U) = assoc(V) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goal_041) ).
fof(f40_neg,negated_conjecture,
~ ? [U,V] :
~ ( lin(U) = lin(V)
=> assoc(U) = assoc(V) ),
inference(negated_conjecture,[status(cth)],[f40]) ).
fof(f40_nnf,plain,
! [U,V] :
( assoc(U) = assoc(V)
| lin(U) != lin(V) ),
inference(nnf_transformation,[status(thm)],[f40_neg]) ).
fof(f40_sk,plain,
! [U,V] :
( assoc(U) = assoc(V)
| lin(U) != lin(V) ),
inference(skolemisation,[status(esa)],[f40_nnf]) ).
cnf(c40,plain,
( assoc(X0) = assoc(X1)
| lin(X0) != lin(X1) ),
inference(cnf_transformation,[status(esa)],[f40_sk]) ).
cnf(p325,plain,
assoc(x2(eX,x2(eX,X0))) = assoc(x2(x2(eX,eX),X0)),
inference(resolution,[status(thm)],[p321,c40]) ).
fof(f20,axiom,
! [X,X2] : proj12(x2(X,X2)) = X,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_021) ).
fof(f20_nnf,plain,
! [X,X2] : proj12(x2(X,X2)) = X,
inference(nnf_transformation,[status(thm)],[f20]) ).
fof(f20_sk,plain,
! [X,X2] : proj12(x2(X,X2)) = X,
inference(skolemisation,[status(esa)],[f20_nnf]) ).
cnf(c20,plain,
proj12(x2(X0,X1)) = X0,
inference(cnf_transformation,[status(esa)],[f20_sk]) ).
cnf(p49,plain,
proj12(assoc(x2(X0,X1))) = assoc(X0),
inference(superposition,[status(thm)],[c31,c20]) ).
cnf(p344,plain,
assoc(eX) = assoc(x2(eX,eX)),
inference(superposition,[status(thm)],[p325,p49]) ).
cnf(p347,plain,
assoc(x2(x2(eX,eX),X0)) = x2(assoc(eX),assoc(X0)),
inference(superposition,[status(thm)],[p344,c31]) ).
cnf(p419,plain,
x2(assoc(eX),assoc(X0)) = assoc(x2(eX,X0)),
inference(superposition,[status(thm)],[c31,p347]) ).
cnf(p345,plain,
assoc(x2(x2(eX,eX),X0)) = assoc(x2(eX,x2(eX,X0))),
inference(superposition,[status(thm)],[p325,p49]) ).
cnf(p348,plain,
x2(assoc(eX),assoc(X0)) = assoc(x2(eX,x2(eX,X0))),
inference(demodulation,[status(thm)],[p347,p345]) ).
cnf(p422,plain,
assoc(x2(eX,X0)) = assoc(x2(eX,x2(eX,X0))),
inference(demodulation,[status(thm)],[p419,p348]) ).
fof(f21,axiom,
! [X,X2] : proj22(x2(X,X2)) = X2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_022) ).
fof(f21_nnf,plain,
! [X,X2] : proj22(x2(X,X2)) = X2,
inference(nnf_transformation,[status(thm)],[f21]) ).
fof(f21_sk,plain,
! [X,X2] : proj22(x2(X,X2)) = X2,
inference(skolemisation,[status(esa)],[f21_nnf]) ).
cnf(c21,plain,
proj22(x2(X0,X1)) = X1,
inference(cnf_transformation,[status(esa)],[f21_sk]) ).
cnf(p50,plain,
proj22(assoc(x2(X0,X1))) = assoc(X1),
inference(superposition,[status(thm)],[c31,c21]) ).
cnf(p448,plain,
assoc(X0) = assoc(x2(eX,X0)),
inference(superposition,[status(thm)],[p422,p50]) ).
cnf(p456,plain,
proj12(assoc(X0)) = assoc(eX),
inference(superposition,[status(thm)],[p448,p49]) ).
cnf(p457,plain,
assoc(eX) = assoc(X0),
inference(demodulation,[status(thm)],[p456,p49]) ).
cnf(p550,plain,
x2(assoc(eX),assoc(X0)) = assoc(eX),
inference(superposition,[status(thm)],[p457,p419]) ).
cnf(p552,plain,
assoc(X0) = assoc(eX),
inference(superposition,[status(thm)],[p457,p448]) ).
cnf(p563,plain,
assoc(X0) = assoc(X1),
inference(superposition,[status(thm)],[p552,p457]) ).
fof(f29,axiom,
! [Y,C] :
( Y != z(proj1(Y),proj2(Y))
=> assoc(z(Y,C)) = z(assoc(Y),assoc(C)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_030) ).
fof(f29_nnf,plain,
! [Y,C] :
( assoc(z(Y,C)) = z(assoc(Y),assoc(C))
| Y = z(proj1(Y),proj2(Y)) ),
inference(nnf_transformation,[status(thm)],[f29]) ).
fof(f29_sk,plain,
! [Y,C] :
( assoc(z(Y,C)) = z(assoc(Y),assoc(C))
| Y = z(proj1(Y),proj2(Y)) ),
inference(skolemisation,[status(esa)],[f29_nnf]) ).
cnf(c29,plain,
( assoc(z(X0,X1)) = z(assoc(X0),assoc(X1))
| X0 = z(proj1(X0),proj2(X0)) ),
inference(cnf_transformation,[status(esa)],[f29_sk]) ).
cnf(p553,plain,
( assoc(eX) = z(assoc(X0),assoc(X1))
| X0 = z(proj1(X0),proj2(X0)) ),
inference(demodulation,[status(thm)],[p552,c29]) ).
fof(f23,axiom,
! [X,X2] : z(X,X2) != eX,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_024) ).
fof(f23_nnf,plain,
! [X,X2] : z(X,X2) != eX,
inference(nnf_transformation,[status(thm)],[f23]) ).
fof(f23_sk,plain,
! [X,X2] : z(X,X2) != eX,
inference(skolemisation,[status(esa)],[f23_nnf]) ).
cnf(c23,plain,
z(X0,X1) != eX,
inference(cnf_transformation,[status(esa)],[f23_sk]) ).
cnf(p814,plain,
( X0 != eX
| assoc(eX) = z(assoc(X0),assoc(X1)) ),
inference(superposition,[status(thm)],[p553,c23]) ).
cnf(p830,plain,
assoc(eX) = z(assoc(eX),assoc(X0)),
inference(equality_resolution,[status(thm)],[p814]) ).
fof(f22,axiom,
! [X,X2,X3,X4] : z(X,X2) != x2(X3,X4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_023) ).
fof(f22_nnf,plain,
! [X,X2,X3,X4] : z(X,X2) != x2(X3,X4),
inference(nnf_transformation,[status(thm)],[f22]) ).
fof(f22_sk,plain,
! [X,X2,X3,X4] : z(X,X2) != x2(X3,X4),
inference(skolemisation,[status(esa)],[f22_nnf]) ).
cnf(c22,plain,
z(X0,X1) != x2(X2,X3),
inference(cnf_transformation,[status(esa)],[f22_sk]) ).
cnf(p835,plain,
assoc(eX) != x2(X0,X1),
inference(superposition,[status(thm)],[p830,c22]) ).
cnf(p853,plain,
assoc(X0) != x2(X1,X2),
inference(superposition,[status(thm)],[p563,p835]) ).
cnf(p918,plain,
assoc(X0) != assoc(eX),
inference(superposition,[status(thm)],[p550,p853]) ).
cnf(p920,plain,
$false,
inference(equality_resolution,[status(thm)],[p918]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SWX185+1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.06 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.16/0.42 % Computer : n010.cluster.edu
% 0.16/0.42 % Model : x86_64 x86_64
% 0.16/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.42 % Memory : 8046.5625MB
% 0.16/0.42 % OS : Linux 6.8.0-71-generic
% 0.16/0.42 % CPULimit : 300
% 0.16/0.42 % WCLimit : 300
% 0.16/0.42 % DateTime : Thu Sep 24 23:32:58 UTC 2026
% 0.16/0.42 % CPUTime :
% 0.16/0.43 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 21.95/3.67 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 21.95/3.67 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------