%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SWX187+1 : TPTP v9.3.1. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n001.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 : Sun Sep 27 09:16:16 AM UTC 2026
% Result : Theorem 0.22s 0.56s
% Output : CNFRefutation 0.22s
% Verified :
% SZS Type : Refutation
% Derivation depth : 31
% Number of leaves : 11
% Syntax : Number of formulae : 64 ( 38 unt; 0 def)
% Number of atoms : 151 ( 120 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 157 ( 70 ~; 76 |; 0 &)
% ( 1 <=>; 10 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 3 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 : 204 ( 11 sgn 16 !; 8 ?)
% Comments :
%------------------------------------------------------------------------------
fof(axiom_001,axiom,
! [X,X2] : head(cons(X,X2)) = X,
file('theBenchmark.p',axiom_001) ).
fof(axiom_005,axiom,
! [X] : s(X) != z,
file('theBenchmark.p',axiom_005) ).
fof(axiom_007,axiom,
! [Y,Xs] : length(cons(Y,Xs)) = s(length(Xs)),
file('theBenchmark.p',axiom_007) ).
fof(axiom_008,axiom,
! [Z,Y2] :
( x2(s(Z),s(Y2))
<=> x2(Z,Y2) ),
file('theBenchmark.p',axiom_008) ).
fof(axiom_010,axiom,
! [X2] : x2(z,s(X2)),
file('theBenchmark.p',axiom_010) ).
fof(axiom_012,axiom,
! [Y] : x(nil,Y) = Y,
file('theBenchmark.p',axiom_012) ).
fof(axiom_013,axiom,
! [Y,Z,Xs] : x(cons(Z,Xs),Y) = cons(Z,x(Xs,Y)),
file('theBenchmark.p',axiom_013) ).
fof(axiom_015,axiom,
! [Z,X2,X3] : rotate(s(Z),cons(X2,X3)) = rotate(Z,x(X3,cons(X2,nil))),
file('theBenchmark.p',axiom_015) ).
fof(axiom_016,axiom,
! [Y] : rotate(z,Y) = Y,
file('theBenchmark.p',axiom_016) ).
fof(goal_017,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('theBenchmark.p',goal_017) ).
fof(goal_017_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(assume_negation,[status(cth)],[goal_017]) ).
cnf(c_16,plain,
head(cons(A,B)) = A,
inference(clausify,[status(thm)],[axiom_001]) ).
cnf(c_20,plain,
s(A) != z,
inference(clausify,[status(thm)],[axiom_005]) ).
fof(axiom_006,axiom,
length(nil) = z,
file('theBenchmark.p',axiom_006) ).
cnf(c_21,plain,
length(nil) = z,
inference(clausify,[status(thm)],[axiom_006]) ).
cnf(c_22,plain,
z = length(nil),
inference(copy,[status(thm)],[c_21]) ).
cnf(c_23,plain,
length(cons(A,B)) = s(length(B)),
inference(clausify,[status(thm)],[axiom_007]) ).
cnf(c_25,plain,
( ~ x2(A,B)
| x2(s(A),s(B)) ),
inference(clausify,[status(thm)],[axiom_008]) ).
cnf(c_28,plain,
x2(z,s(A)),
inference(clausify,[status(thm)],[axiom_010]) ).
cnf(c_29,plain,
x2(length(nil),s(A)),
inference(paramod,[status(thm)],[c_22,c_28]) ).
cnf(c_32,plain,
x(nil,A) = A,
inference(clausify,[status(thm)],[axiom_012]) ).
cnf(c_33,plain,
x(cons(A,B),C) = cons(A,x(B,C)),
inference(clausify,[status(thm)],[axiom_013]) ).
cnf(c_35,plain,
rotate(s(A),cons(B,C)) = rotate(A,x(C,cons(B,nil))),
inference(clausify,[status(thm)],[axiom_015]) ).
cnf(c_36,plain,
rotate(A,x(B,cons(C,nil))) = rotate(s(A),cons(C,B)),
inference(copy,[status(thm)],[c_35]) ).
cnf(c_37,plain,
rotate(z,A) = A,
inference(clausify,[status(thm)],[axiom_016]) ).
cnf(c_38,plain,
rotate(length(nil),A) = A,
inference(paramod,[status(thm)],[c_22,c_37]) ).
cnf(c_39,negated_conjecture,
( C = A
| rotate(C,D) != rotate(A,B)
| rotate(s(z),B) = B
| D != B
| ~ x2(C,length(D))
| ~ x2(A,length(B)) ),
inference(clausify,[status(thm)],[goal_017_neg]) ).
cnf(c_40,negated_conjecture,
( C = A
| rotate(C,D) != rotate(A,B)
| rotate(s(length(nil)),B) = B
| D != B
| ~ x2(C,length(D))
| ~ x2(A,length(B)) ),
inference(paramod,[status(thm)],[c_22,c_39]) ).
cnf(c_132,plain,
s(A) != length(nil),
inference(paramod,[status(thm)],[c_22,c_20]) ).
cnf(c_41,plain,
length(nil) != s(A),
inference(copy,[status(thm)],[c_132]) ).
cnf(c_44,plain,
x2(s(length(nil)),s(s(A))),
inference(resolve,[status(thm)],[c_29,c_25]) ).
cnf(c_47,plain,
rotate(A,cons(B,x(C,cons(D,nil)))) = rotate(s(A),cons(D,cons(B,C))),
inference(paramod,[status(thm)],[c_33,c_36]) ).
cnf(c_133,plain,
x(A,cons(B,nil)) = rotate(s(length(nil)),cons(B,A)),
inference(paramod,[status(thm)],[c_38,c_36]) ).
cnf(c_48,plain,
rotate(s(length(nil)),cons(A,B)) = x(B,cons(A,nil)),
inference(copy,[status(thm)],[c_133]) ).
cnf(c_50,plain,
( C = A
| rotate(C,cons(E,D)) != rotate(A,B)
| rotate(s(length(nil)),B) = B
| cons(E,D) != B
| ~ x2(C,s(length(D)))
| ~ x2(A,length(B)) ),
inference(paramod,[status(thm)],[c_23,c_40]) ).
cnf(c_58,plain,
x2(s(s(length(nil))),s(s(s(A)))),
inference(resolve,[status(thm)],[c_44,c_25]) ).
cnf(c_62,plain,
rotate(s(s(length(nil))),cons(A,cons(B,C))) = x(x(C,cons(A,nil)),cons(B,nil)),
inference(paramod,[status(thm)],[c_47,c_48]) ).
cnf(c_74,plain,
( C = A
| rotate(C,cons(E,cons(F,D))) != rotate(A,B)
| rotate(s(length(nil)),B) = B
| cons(E,cons(F,D)) != B
| ~ x2(C,s(s(length(D))))
| ~ x2(A,length(B)) ),
inference(paramod,[status(thm)],[c_23,c_50]) ).
cnf(c_89,plain,
( C = A
| rotate(C,cons(E,cons(F,cons(V6,D)))) != rotate(A,B)
| rotate(s(length(nil)),B) = B
| cons(E,cons(F,cons(V6,D))) != B
| ~ x2(C,s(s(s(length(D)))))
| ~ x2(A,length(B)) ),
inference(paramod,[status(thm)],[c_23,c_74]) ).
cnf(c_134,plain,
( s(s(length(nil))) = A
| rotate(s(s(length(nil))),cons(C,cons(D,cons(E,F)))) != rotate(A,B)
| rotate(s(length(nil)),B) = B
| cons(C,cons(D,cons(E,F))) != B
| ~ x2(A,length(B)) ),
inference(resolve,[status(thm)],[c_89,c_58]) ).
cnf(c_135,plain,
( s(s(length(nil))) = A
| x(x(cons(E,F),cons(C,nil)),cons(D,nil)) != rotate(A,B)
| rotate(s(length(nil)),B) = B
| cons(C,cons(D,cons(E,F))) != B
| ~ x2(A,length(B)) ),
inference(paramod,[status(thm)],[c_62,c_134]) ).
cnf(c_136,plain,
( s(s(length(nil))) = A
| x(cons(E,x(F,cons(C,nil))),cons(D,nil)) != rotate(A,B)
| rotate(s(length(nil)),B) = B
| cons(C,cons(D,cons(E,F))) != B
| ~ x2(A,length(B)) ),
inference(paramod,[status(thm)],[c_33,c_135]) ).
cnf(c_137,plain,
( s(s(length(nil))) = A
| cons(E,x(x(F,cons(C,nil)),cons(D,nil))) != rotate(A,B)
| rotate(s(length(nil)),B) = B
| cons(C,cons(D,cons(E,F))) != B
| ~ x2(A,length(B)) ),
inference(paramod,[status(thm)],[c_33,c_136]) ).
cnf(c_117,plain,
( s(s(length(nil))) = A
| rotate(A,B) != cons(E,x(x(F,cons(C,nil)),cons(D,nil)))
| rotate(s(length(nil)),B) = B
| cons(C,cons(D,cons(E,F))) != B
| ~ x2(A,length(B)) ),
inference(copy,[status(thm)],[c_137]) ).
cnf(c_138,plain,
( s(s(length(nil))) = A
| rotate(A,cons(V6,B)) != cons(E,x(x(F,cons(C,nil)),cons(D,nil)))
| rotate(s(length(nil)),cons(V6,B)) = cons(V6,B)
| cons(C,cons(D,cons(E,F))) != cons(V6,B)
| ~ x2(A,s(length(B))) ),
inference(paramod,[status(thm)],[c_23,c_117]) ).
cnf(c_120,plain,
( s(s(length(nil))) = A
| rotate(A,cons(V6,B)) != cons(E,x(x(F,cons(C,nil)),cons(D,nil)))
| x(B,cons(V6,nil)) = cons(V6,B)
| cons(C,cons(D,cons(E,F))) != cons(V6,B)
| ~ x2(A,s(length(B))) ),
inference(paramod,[status(thm)],[c_48,c_138]) ).
cnf(c_139,plain,
( s(s(length(nil))) = length(nil)
| rotate(length(nil),cons(E,F)) != cons(C,x(x(D,cons(A,nil)),cons(B,nil)))
| x(F,cons(E,nil)) = cons(E,F)
| cons(A,cons(B,cons(C,D))) != cons(E,F) ),
inference(resolve,[status(thm)],[c_120,c_29]) ).
cnf(c_140,plain,
( s(s(length(nil))) = length(nil)
| cons(E,F) != cons(C,x(x(D,cons(A,nil)),cons(B,nil)))
| x(F,cons(E,nil)) = cons(E,F)
| cons(A,cons(B,cons(C,D))) != cons(E,F) ),
inference(paramod,[status(thm)],[c_38,c_139]) ).
cnf(c_141,plain,
( s(s(length(nil))) = length(nil)
| cons(C,x(x(D,cons(A,nil)),cons(B,nil))) != cons(E,F)
| x(F,cons(E,nil)) = cons(E,F)
| cons(A,cons(B,cons(C,D))) != cons(E,F) ),
inference(copy,[status(thm)],[c_140]) ).
cnf(c_121,plain,
( cons(C,x(x(D,cons(A,nil)),cons(B,nil))) != cons(E,F)
| x(F,cons(E,nil)) = cons(E,F)
| cons(A,cons(B,cons(C,D))) != cons(E,F) ),
inference(resolve,[status(thm)],[c_41,c_141]) ).
cnf(c_142,plain,
( cons(C,x(cons(D,x(E,cons(A,nil))),cons(B,nil))) != cons(F,V6)
| x(V6,cons(F,nil)) = cons(F,V6)
| cons(A,cons(B,cons(C,cons(D,E)))) != cons(F,V6) ),
inference(paramod,[status(thm)],[c_33,c_121]) ).
cnf(c_123,plain,
( cons(C,cons(D,x(x(E,cons(A,nil)),cons(B,nil)))) != cons(F,V6)
| x(V6,cons(F,nil)) = cons(F,V6)
| cons(A,cons(B,cons(C,cons(D,E)))) != cons(F,V6) ),
inference(paramod,[status(thm)],[c_33,c_142]) ).
cnf(c_143,plain,
( cons(C,cons(D,x(cons(A,nil),cons(B,nil)))) != cons(E,F)
| x(F,cons(E,nil)) = cons(E,F)
| cons(A,cons(B,cons(C,cons(D,nil)))) != cons(E,F) ),
inference(paramod,[status(thm)],[c_32,c_123]) ).
cnf(c_144,plain,
( cons(C,cons(D,cons(A,x(nil,cons(B,nil))))) != cons(E,F)
| x(F,cons(E,nil)) = cons(E,F)
| cons(A,cons(B,cons(C,cons(D,nil)))) != cons(E,F) ),
inference(paramod,[status(thm)],[c_33,c_143]) ).
cnf(c_127,plain,
( cons(C,cons(D,cons(A,cons(B,nil)))) != cons(E,F)
| x(F,cons(E,nil)) = cons(E,F)
| cons(A,cons(B,cons(C,cons(D,nil)))) != cons(E,F) ),
inference(paramod,[status(thm)],[c_32,c_144]) ).
cnf(c_128,plain,
( x(D,cons(C,nil)) = cons(C,D)
| cons(A,cons(B,cons(A,cons(B,nil)))) != cons(C,D) ),
inference(factor,[status(thm)],[c_127]) ).
cnf(c_145,plain,
x(cons(A,cons(B,cons(A,nil))),cons(B,nil)) = cons(B,cons(A,cons(B,cons(A,nil)))),
inference(xxres,[status(thm)],[c_128]) ).
cnf(c_146,plain,
cons(A,x(cons(B,cons(A,nil)),cons(B,nil))) = cons(B,cons(A,cons(B,cons(A,nil)))),
inference(paramod,[status(thm)],[c_33,c_145]) ).
cnf(c_147,plain,
cons(A,cons(B,x(cons(A,nil),cons(B,nil)))) = cons(B,cons(A,cons(B,cons(A,nil)))),
inference(paramod,[status(thm)],[c_33,c_146]) ).
cnf(c_148,plain,
cons(A,cons(B,cons(A,x(nil,cons(B,nil))))) = cons(B,cons(A,cons(B,cons(A,nil)))),
inference(paramod,[status(thm)],[c_33,c_147]) ).
cnf(c_129,plain,
cons(A,cons(B,cons(A,cons(B,nil)))) = cons(B,cons(A,cons(B,cons(A,nil)))),
inference(paramod,[status(thm)],[c_32,c_148]) ).
cnf(c_149,plain,
head(cons(A,cons(B,cons(A,cons(B,nil))))) = B,
inference(paramod,[status(thm)],[c_129,c_16]) ).
cnf(c_130,plain,
A = B,
inference(paramod,[status(thm)],[c_16,c_149]) ).
cnf(c_131,plain,
$false,
inference(resolve,[status(thm)],[c_130,c_41]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWX187+1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.07 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.16/0.44 % Computer : n001.cluster.edu
% 0.16/0.44 % Model : x86_64 x86_64
% 0.16/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.44 % Memory : 8046.5625MB
% 0.16/0.44 % OS : Linux 6.8.0-71-generic
% 0.16/0.44 % CPULimit : 300
% 0.16/0.44 % WCLimit : 300
% 0.16/0.44 % DateTime : Sat Sep 26 16:56:44 UTC 2026
% 0.16/0.44 % CPUTime :
% 0.16/0.44 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.16/0.44 % Process 2254805 was started by sandbox on n001,
% 0.16/0.44 % Sat Sep 26 16:56:44 2026
% 0.16/0.44 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.16/0.45
% 0.16/0.45 % From the command line: assign(max_seconds, 300).
% 0.22/0.56
% 0.22/0.56 % SZS status Theorem for theBenchmark
% 0.22/0.56
% 0.22/0.56 % Proof 1 at 0.07 (+ 0.01) seconds.
% 0.22/0.56 % Length of proof is 44.
% 0.22/0.56 % Level of proof is 14.
% 0.22/0.56 % Maximum clause weight is 98.000.
% 0.22/0.56 % Given clauses 100.
% 0.22/0.56
% 0.22/0.56 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------