%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SWX187+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 : n015.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 6.93s 6.36s
% Output : Proof 6.93s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 10
% Syntax : Number of formulae : 63 ( 40 unt; 0 def)
% Number of atoms : 140 ( 101 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 134 ( 57 ~; 64 |; 2 &)
% ( 1 <=>; 10 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 4 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 8 ( 8 usr; 2 con; 0-2 aty)
% Number of variables : 167 ( 8 sgn 53 !; 8 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f12,axiom,
! [Y,Z,Xs] : x(cons(Z,Xs),Y) = cons(Z,x(Xs,Y)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_013) ).
fof(f12_nnf,plain,
! [Y,Z,Xs] : x(cons(Z,Xs),Y) = cons(Z,x(Xs,Y)),
inference(nnf_transformation,[status(thm)],[f12]) ).
fof(f12_sk,plain,
! [Z,Xs,Y] : x(cons(Z,Xs),Y) = cons(Z,x(Xs,Y)),
inference(skolemisation,[status(esa)],[f12_nnf]) ).
cnf(c13,plain,
x(cons(X1,X2),X0) = cons(X1,x(X2,X0)),
inference(cnf_transformation,[status(esa)],[f12_sk]) ).
fof(f14,axiom,
! [Z,X2,X3] : rotate(s(Z),cons(X2,X3)) = rotate(Z,x(X3,cons(X2,nil))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_015) ).
fof(f14_nnf,plain,
! [Z,X2,X3] : rotate(s(Z),cons(X2,X3)) = rotate(Z,x(X3,cons(X2,nil))),
inference(nnf_transformation,[status(thm)],[f14]) ).
fof(f14_sk,plain,
! [Z,X2,X3] : rotate(s(Z),cons(X2,X3)) = rotate(Z,x(X3,cons(X2,nil))),
inference(skolemisation,[status(esa)],[f14_nnf]) ).
cnf(c15,plain,
rotate(s(X0),cons(X1,X2)) = rotate(X0,x(X2,cons(X1,nil))),
inference(cnf_transformation,[status(esa)],[f14_sk]) ).
cnf(p108,plain,
rotate(s(X0),cons(X1,cons(X2,X3))) = rotate(X0,cons(X2,x(X3,cons(X1,nil)))),
inference(superposition,[status(thm)],[c13,c15]) ).
cnf(p197,plain,
rotate(s(X0),cons(X1,cons(X2,cons(X3,X4)))) = rotate(X0,cons(X2,cons(X3,x(X4,cons(X1,nil))))),
inference(superposition,[status(thm)],[c13,p108]) ).
fof(f15,axiom,
! [Y] : rotate(z,Y) = Y,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_016) ).
fof(f15_nnf,plain,
! [Y] : rotate(z,Y) = Y,
inference(nnf_transformation,[status(thm)],[f15]) ).
fof(f15_sk,plain,
! [Y] : rotate(z,Y) = Y,
inference(skolemisation,[status(esa)],[f15_nnf]) ).
cnf(c16,plain,
rotate(z,X0) = X0,
inference(cnf_transformation,[status(esa)],[f15_sk]) ).
cnf(p81,plain,
rotate(s(z),cons(X0,X1)) = x(X1,cons(X0,nil)),
inference(superposition,[status(thm)],[c15,c16]) ).
cnf(p359,plain,
rotate(s(s(z)),cons(X0,cons(X1,cons(X2,X3)))) = cons(X2,x(x(X3,cons(X0,nil)),cons(X1,nil))),
inference(superposition,[status(thm)],[p197,p81]) ).
fof(f5,axiom,
length(nil) = z,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_006) ).
fof(f5_nnf,plain,
length(nil) = z,
inference(nnf_transformation,[status(thm)],[f5]) ).
cnf(c5,plain,
length(nil) = z,
inference(cnf_transformation,[status(esa)],[f5_nnf]) ).
fof(f6,axiom,
! [Y,Xs] : length(cons(Y,Xs)) = s(length(Xs)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_007) ).
fof(f6_nnf,plain,
! [Y,Xs] : length(cons(Y,Xs)) = s(length(Xs)),
inference(nnf_transformation,[status(thm)],[f6]) ).
fof(f6_sk,plain,
! [Y,Xs] : length(cons(Y,Xs)) = s(length(Xs)),
inference(skolemisation,[status(esa)],[f6_nnf]) ).
cnf(c6,plain,
length(cons(X0,X1)) = s(length(X1)),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
fof(f16,conjecture,
? [N,M,Ys,Xs] :
~ ( x2(N,length(Xs))
=> ( x2(M,length(Ys))
=> ( Xs = Ys
=> ( rotate(s(z),Xs) != Xs
=> ( rotate(N,Xs) = rotate(M,Ys)
=> N = M ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goal_017) ).
fof(f16_neg,negated_conjecture,
~ ? [N,M,Ys,Xs] :
~ ( x2(N,length(Xs))
=> ( x2(M,length(Ys))
=> ( Xs = Ys
=> ( rotate(s(z),Xs) != Xs
=> ( rotate(N,Xs) = rotate(M,Ys)
=> N = M ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f16]) ).
fof(f16_nnf,plain,
! [N,M,Ys,Xs] :
( N = M
| rotate(N,Xs) != rotate(M,Ys)
| rotate(s(z),Xs) = Xs
| Xs != Ys
| ~ x2(M,length(Ys))
| ~ x2(N,length(Xs)) ),
inference(nnf_transformation,[status(thm)],[f16_neg]) ).
fof(f16_sk,plain,
! [N,Xs,M,Ys] :
( N = M
| rotate(N,Xs) != rotate(M,Ys)
| rotate(s(z),Xs) = Xs
| Xs != Ys
| ~ x2(M,length(Ys))
| ~ x2(N,length(Xs)) ),
inference(skolemisation,[status(esa)],[f16_nnf]) ).
cnf(c17,plain,
( X0 = X1
| rotate(X0,X3) != rotate(X1,X2)
| rotate(s(z),X3) = X3
| X3 != X2
| ~ x2(X1,length(X2))
| ~ x2(X0,length(X3)) ),
inference(cnf_transformation,[status(esa)],[f16_sk]) ).
cnf(p31,plain,
( X0 = X2
| rotate(X0,cons(X4,X1)) != rotate(X2,X3)
| rotate(s(z),cons(X4,X1)) = cons(X4,X1)
| cons(X4,X1) != X3
| ~ x2(X2,length(X3))
| ~ x2(X0,s(length(X1))) ),
inference(superposition,[status(thm)],[c6,c17]) ).
fof(f9,axiom,
! [X2] : x2(z,s(X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_010) ).
fof(f9_nnf,plain,
! [X2] : x2(z,s(X2)),
inference(nnf_transformation,[status(thm)],[f9]) ).
fof(f9_sk,plain,
! [X2] : x2(z,s(X2)),
inference(skolemisation,[status(esa)],[f9_nnf]) ).
cnf(c10,plain,
x2(z,s(X0)),
inference(cnf_transformation,[status(esa)],[f9_sk]) ).
cnf(p55,plain,
( z = X0
| cons(X2,X3) != rotate(X0,X1)
| rotate(s(z),cons(X2,X3)) = cons(X2,X3)
| cons(X2,X3) != X1
| ~ x2(X0,length(X1)) ),
inference(resolution,[status(thm)],[p31,c10]) ).
cnf(p58,plain,
( z = X0
| cons(X2,X3) != rotate(X0,cons(X4,X1))
| rotate(s(z),cons(X2,X3)) = cons(X2,X3)
| cons(X2,X3) != cons(X4,X1)
| ~ x2(X0,s(length(X1))) ),
inference(superposition,[status(thm)],[c6,p55]) ).
cnf(p60,plain,
( z = X0
| cons(X2,X3) != rotate(X0,cons(X4,cons(X5,X1)))
| rotate(s(z),cons(X2,X3)) = cons(X2,X3)
| cons(X2,X3) != cons(X4,cons(X5,X1))
| ~ x2(X0,s(s(length(X1)))) ),
inference(superposition,[status(thm)],[c6,p58]) ).
cnf(p69,plain,
( z = X0
| cons(X2,X3) != rotate(X0,cons(X4,cons(X5,cons(X6,X1))))
| rotate(s(z),cons(X2,X3)) = cons(X2,X3)
| cons(X2,X3) != cons(X4,cons(X5,cons(X6,X1)))
| ~ x2(X0,s(s(s(length(X1))))) ),
inference(superposition,[status(thm)],[c6,p60]) ).
cnf(p107,plain,
( z = X0
| cons(X2,X3) != rotate(X0,cons(X4,cons(X5,cons(X6,X1))))
| x(X3,cons(X2,nil)) = cons(X2,X3)
| cons(X2,X3) != cons(X4,cons(X5,cons(X6,X1)))
| ~ x2(X0,s(s(s(length(X1))))) ),
inference(demodulation,[status(thm)],[p81,p69]) ).
cnf(p161,plain,
( z = X0
| cons(X2,X3) != rotate(X0,cons(X4,cons(X5,cons(X6,cons(X7,X1)))))
| x(X3,cons(X2,nil)) = cons(X2,X3)
| cons(X2,X3) != cons(X4,cons(X5,cons(X6,cons(X7,X1))))
| ~ x2(X0,s(s(s(s(length(X1)))))) ),
inference(superposition,[status(thm)],[c6,p107]) ).
cnf(p275,plain,
( z = X0
| cons(X1,X2) != rotate(X0,cons(X3,cons(X4,cons(X5,cons(X6,nil)))))
| x(X2,cons(X1,nil)) = cons(X1,X2)
| cons(X1,X2) != cons(X3,cons(X4,cons(X5,cons(X6,nil))))
| ~ x2(X0,s(s(s(s(z))))) ),
inference(superposition,[status(thm)],[c5,p161]) ).
cnf(p279,plain,
( z = X0
| cons(X4,cons(X1,cons(X2,cons(X3,nil)))) != rotate(X0,cons(X4,cons(X1,cons(X2,cons(X3,nil)))))
| cons(X1,cons(X2,cons(X3,cons(X4,nil)))) = cons(X4,cons(X1,cons(X2,cons(X3,nil))))
| ~ x2(X0,s(s(s(s(z))))) ),
inference(equality_resolution,[status(thm)],[p275]) ).
fof(f7,axiom,
! [Z,Y2] :
( x2(s(Z),s(Y2))
<=> x2(Z,Y2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_008) ).
fof(f7_nnf,plain,
! [Z,Y2] :
( ( ~ x2(Z,Y2)
| x2(s(Z),s(Y2)) )
& ( x2(Z,Y2)
| ~ x2(s(Z),s(Y2)) ) ),
inference(nnf_transformation,[status(thm)],[f7]) ).
fof(f7_sk,plain,
! [Z,Y2] :
( ( ~ x2(Z,Y2)
| x2(s(Z),s(Y2)) )
& ( x2(Z,Y2)
| ~ x2(s(Z),s(Y2)) ) ),
inference(skolemisation,[status(esa)],[f7_nnf]) ).
cnf(c8,plain,
( ~ x2(X0,X1)
| x2(s(X0),s(X1)) ),
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
cnf(p53,plain,
x2(s(z),s(s(X0))),
inference(resolution,[status(thm)],[c8,c10]) ).
cnf(p111,plain,
x2(s(s(z)),s(s(s(X0)))),
inference(resolution,[status(thm)],[p53,c8]) ).
cnf(p307,plain,
( z = s(s(z))
| cons(X3,cons(X0,cons(X1,cons(X2,nil)))) != rotate(s(s(z)),cons(X3,cons(X0,cons(X1,cons(X2,nil)))))
| cons(X0,cons(X1,cons(X2,cons(X3,nil)))) = cons(X3,cons(X0,cons(X1,cons(X2,nil)))) ),
inference(resolution,[status(thm)],[p279,p111]) ).
cnf(p371,plain,
( z = s(s(z))
| cons(X3,cons(X0,cons(X1,cons(X2,nil)))) != cons(X1,x(x(cons(X2,nil),cons(X3,nil)),cons(X0,nil)))
| cons(X0,cons(X1,cons(X2,cons(X3,nil)))) = cons(X3,cons(X0,cons(X1,cons(X2,nil)))) ),
inference(demodulation,[status(thm)],[p359,p307]) ).
cnf(p406,plain,
( z = s(s(z))
| cons(X3,cons(X0,cons(X1,cons(X2,nil)))) != cons(X1,cons(X2,cons(X3,cons(X0,nil))))
| cons(X0,cons(X1,cons(X2,cons(X3,nil)))) = cons(X3,cons(X0,cons(X1,cons(X2,nil)))) ),
inference(superposition,[status(thm)],[c13,p371]) ).
cnf(p407,plain,
( z = s(s(z))
| cons(X0,cons(X1,cons(X0,cons(X1,nil)))) = cons(X1,cons(X0,cons(X1,cons(X0,nil)))) ),
inference(equality_resolution,[status(thm)],[p406]) ).
fof(f0,axiom,
! [X,X2] : head(cons(X,X2)) = X,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_001) ).
fof(f0_nnf,plain,
! [X,X2] : head(cons(X,X2)) = X,
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
! [X,X2] : head(cons(X,X2)) = X,
inference(skolemisation,[status(esa)],[f0_nnf]) ).
cnf(c0,plain,
head(cons(X0,X1)) = X0,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(p408,plain,
( X0 = X1
| z = s(s(z)) ),
inference(superposition,[status(thm)],[p407,c0]) ).
cnf(p409,plain,
z = s(s(z)),
inference(factoring,[status(thm)],[p408]) ).
fof(f4,axiom,
! [X] : s(X) != z,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_005) ).
fof(f4_nnf,plain,
! [X] : s(X) != z,
inference(nnf_transformation,[status(thm)],[f4]) ).
fof(f4_sk,plain,
! [X] : s(X) != z,
inference(skolemisation,[status(esa)],[f4_nnf]) ).
cnf(c4,plain,
s(X0) != z,
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(p411,plain,
z != z,
inference(superposition,[status(thm)],[p409,c4]) ).
cnf(p457,plain,
$false,
inference(equality_resolution,[status(thm)],[p411]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWX187+1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.10/5.38 % Computer : n015.cluster.edu
% 0.10/5.38 % Model : x86_64 x86_64
% 0.10/5.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/5.38 % Memory : 8046.5625MB
% 0.10/5.38 % OS : Linux 6.8.0-71-generic
% 0.10/5.38 % CPULimit : 300
% 0.10/5.38 % WCLimit : 300
% 0.10/5.39 % DateTime : Thu Sep 24 23:36:01 UTC 2026
% 0.10/5.39 % CPUTime :
% 0.10/5.39 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 6.93/6.36 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 6.93/6.36 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------