%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SWX203+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 : n017.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:19 AM UTC 2026
% Result : Theorem 0.22s 5.78s
% Output : CNFRefutation 0.22s
% Verified :
% SZS Type : Refutation
% Derivation depth : 43
% Number of leaves : 18
% Syntax : Number of formulae : 127 ( 47 unt; 0 def)
% Number of atoms : 276 ( 122 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 227 ( 78 ~; 139 |; 2 &)
% ( 4 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 3 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 6 ( 4 usr; 1 prp; 0-2 aty)
% Number of functors : 8 ( 8 usr; 2 con; 0-2 aty)
% Number of variables : 245 ( 25 sgn 24 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(axiom_004,axiom,
! [X] : proj1S(s(X)) = X,
file('theBenchmark.p',axiom_004) ).
fof(axiom_005,axiom,
! [X] : z != s(X),
file('theBenchmark.p',axiom_005) ).
fof(axiom_006,axiom,
! [Y] : leqNat(z,Y),
file('theBenchmark.p',axiom_006) ).
fof(axiom_007,axiom,
! [Z] : ~ leqNat(s(Z),z),
file('theBenchmark.p',axiom_007) ).
fof(axiom_008,axiom,
! [Z,M] :
( leqNat(s(Z),s(M))
<=> leqNat(Z,M) ),
file('theBenchmark.p',axiom_008) ).
fof(axiom_010,axiom,
! [Y] : sorted(cons(Y,nil)),
file('theBenchmark.p',axiom_010) ).
fof(axiom_011,axiom,
! [Y,Y2,Xs] :
( sorted(cons(Y,cons(Y2,Xs)))
<=> ( sorted(cons(Y2,Xs))
& leqNat(Y,Y2) ) ),
file('theBenchmark.p',axiom_011) ).
fof(axiom_013,axiom,
! [Y,Xs] : lengthNat(cons(Y,Xs)) = s(lengthNat(Xs)),
file('theBenchmark.p',axiom_013) ).
fof(axiom_014,axiom,
! [X] : ~ elemNat(X,nil),
file('theBenchmark.p',axiom_014) ).
fof(axiom_015,axiom,
! [X,Z,Xs] :
( elemNat(X,cons(Z,Xs))
<=> ( elemNat(X,Xs)
| X = Z ) ),
file('theBenchmark.p',axiom_015) ).
fof(axiom_017,axiom,
! [Y,Xs] :
( unique(cons(Y,Xs))
<=> ( unique(Xs)
& ~ elemNat(Y,Xs) ) ),
file('theBenchmark.p',axiom_017) ).
fof(axiom_018,axiom,
! [Y] : append(nil,Y) = Y,
file('theBenchmark.p',axiom_018) ).
fof(axiom_019,axiom,
! [Y,Z,Xs] : append(cons(Z,Xs),Y) = cons(Z,append(Xs,Y)),
file('theBenchmark.p',axiom_019) ).
fof(axiom_021,axiom,
! [Y,Xs] : rev(cons(Y,Xs)) = append(rev(Xs),cons(Y,nil)),
file('theBenchmark.p',axiom_021) ).
fof(goal_022,conjecture,
? [Xs] :
~ ( sorted(rev(Xs))
=> ( unique(Xs)
=> leqNat(lengthNat(Xs),s(s(s(z)))) ) ),
file('theBenchmark.p',goal_022) ).
fof(goal_022_neg,negated_conjecture,
~ ? [Xs] :
~ ( sorted(rev(Xs))
=> ( unique(Xs)
=> leqNat(lengthNat(Xs),s(s(s(z)))) ) ),
inference(assume_negation,[status(cth)],[goal_022]) ).
cnf(c_22,plain,
proj1S(s(A)) = A,
inference(clausify,[status(thm)],[axiom_004]) ).
cnf(c_23,plain,
s(A) != z,
inference(clausify,[status(thm)],[axiom_005]) ).
cnf(c_24,plain,
leqNat(z,A),
inference(clausify,[status(thm)],[axiom_006]) ).
cnf(c_25,plain,
~ leqNat(s(A),z),
inference(clausify,[status(thm)],[axiom_007]) ).
cnf(c_26,plain,
( leqNat(A,B)
| ~ leqNat(s(A),s(B)) ),
inference(clausify,[status(thm)],[axiom_008]) ).
cnf(c_27,plain,
( ~ leqNat(A,B)
| leqNat(s(A),s(B)) ),
inference(clausify,[status(thm)],[axiom_008]) ).
cnf(c_29,plain,
sorted(cons(A,nil)),
inference(clausify,[status(thm)],[axiom_010]) ).
cnf(c_32,plain,
( ~ sorted(cons(B,C))
| ~ leqNat(A,B)
| sorted(cons(A,cons(B,C))) ),
inference(clausify,[status(thm)],[axiom_011]) ).
fof(axiom_012,axiom,
lengthNat(nil) = z,
file('theBenchmark.p',axiom_012) ).
cnf(c_33,plain,
lengthNat(nil) = z,
inference(clausify,[status(thm)],[axiom_012]) ).
cnf(c_34,plain,
z = lengthNat(nil),
inference(copy,[status(thm)],[c_33]) ).
cnf(c_35,plain,
lengthNat(cons(A,B)) = s(lengthNat(B)),
inference(clausify,[status(thm)],[axiom_013]) ).
cnf(c_36,plain,
~ elemNat(A,nil),
inference(clausify,[status(thm)],[axiom_014]) ).
cnf(c_37,plain,
( elemNat(A,C)
| B = A
| ~ elemNat(A,cons(B,C)) ),
inference(clausify,[status(thm)],[axiom_015]) ).
fof(axiom_016,axiom,
unique(nil),
file('theBenchmark.p',axiom_016) ).
cnf(c_40,plain,
unique(nil),
inference(clausify,[status(thm)],[axiom_016]) ).
cnf(c_41,plain,
( ~ elemNat(A,B)
| ~ unique(cons(A,B)) ),
inference(clausify,[status(thm)],[axiom_017]) ).
cnf(c_43,plain,
( ~ unique(B)
| elemNat(A,B)
| unique(cons(A,B)) ),
inference(clausify,[status(thm)],[axiom_017]) ).
cnf(c_44,plain,
append(nil,A) = A,
inference(clausify,[status(thm)],[axiom_018]) ).
cnf(c_45,plain,
append(cons(A,B),C) = cons(A,append(B,C)),
inference(clausify,[status(thm)],[axiom_019]) ).
fof(axiom_020,axiom,
rev(nil) = nil,
file('theBenchmark.p',axiom_020) ).
cnf(c_46,plain,
rev(nil) = nil,
inference(clausify,[status(thm)],[axiom_020]) ).
cnf(c_47,plain,
rev(cons(A,B)) = append(rev(B),cons(A,nil)),
inference(clausify,[status(thm)],[axiom_021]) ).
cnf(c_48,negated_conjecture,
( leqNat(lengthNat(A),s(s(s(z))))
| ~ unique(A)
| ~ sorted(rev(A)) ),
inference(clausify,[status(thm)],[goal_022_neg]) ).
cnf(c_49,negated_conjecture,
( leqNat(lengthNat(A),s(s(s(lengthNat(nil)))))
| ~ unique(A)
| ~ sorted(rev(A)) ),
inference(paramod,[status(thm)],[c_34,c_48]) ).
cnf(c_50,plain,
~ leqNat(s(A),lengthNat(nil)),
inference(paramod,[status(thm)],[c_34,c_25]) ).
cnf(c_51,plain,
leqNat(lengthNat(nil),A),
inference(paramod,[status(thm)],[c_34,c_24]) ).
cnf(c_575,plain,
s(A) != lengthNat(nil),
inference(paramod,[status(thm)],[c_34,c_23]) ).
cnf(c_52,plain,
lengthNat(nil) != s(A),
inference(copy,[status(thm)],[c_575]) ).
cnf(c_53,plain,
( ~ leqNat(A,B)
| sorted(cons(A,cons(B,nil))) ),
inference(resolve,[status(thm)],[c_32,c_29]) ).
cnf(c_576,plain,
( elemNat(A,nil)
| unique(cons(A,nil)) ),
inference(resolve,[status(thm)],[c_43,c_40]) ).
cnf(c_59,plain,
unique(cons(A,nil)),
inference(resolve,[status(thm)],[c_36,c_576]) ).
cnf(c_577,plain,
( leqNat(lengthNat(cons(B,A)),s(s(s(lengthNat(nil)))))
| ~ unique(cons(B,A))
| ~ sorted(append(rev(A),cons(B,nil))) ),
inference(paramod,[status(thm)],[c_47,c_49]) ).
cnf(c_60,plain,
( leqNat(s(lengthNat(A)),s(s(s(lengthNat(nil)))))
| ~ unique(cons(B,A))
| ~ sorted(append(rev(A),cons(B,nil))) ),
inference(paramod,[status(thm)],[c_35,c_577]) ).
cnf(c_62,plain,
~ leqNat(s(s(A)),s(lengthNat(nil))),
inference(resolve,[status(thm)],[c_26,c_50]) ).
cnf(c_63,plain,
( ~ sorted(cons(A,B))
| sorted(cons(lengthNat(nil),cons(A,B))) ),
inference(resolve,[status(thm)],[c_51,c_32]) ).
cnf(c_64,plain,
leqNat(s(lengthNat(nil)),s(A)),
inference(resolve,[status(thm)],[c_51,c_27]) ).
cnf(c_578,plain,
( elemNat(s(A),B)
| ~ elemNat(s(A),cons(lengthNat(nil),B)) ),
inference(resolve,[status(thm)],[c_37,c_52]) ).
cnf(c_65,plain,
~ elemNat(s(A),cons(lengthNat(nil),nil)),
inference(resolve,[status(thm)],[c_578,c_36]) ).
cnf(c_73,plain,
~ leqNat(s(s(s(A))),s(s(lengthNat(nil)))),
inference(resolve,[status(thm)],[c_26,c_62]) ).
cnf(c_75,plain,
( elemNat(A,cons(B,nil))
| unique(cons(A,cons(B,nil))) ),
inference(resolve,[status(thm)],[c_59,c_43]) ).
cnf(c_79,plain,
( ~ sorted(cons(s(A),B))
| sorted(cons(s(lengthNat(nil)),cons(s(A),B))) ),
inference(resolve,[status(thm)],[c_64,c_32]) ).
cnf(c_80,plain,
leqNat(s(s(lengthNat(nil))),s(s(A))),
inference(resolve,[status(thm)],[c_64,c_27]) ).
cnf(c_579,plain,
( leqNat(s(lengthNat(cons(B,A))),s(s(s(lengthNat(nil)))))
| ~ unique(cons(C,cons(B,A)))
| ~ sorted(append(append(rev(A),cons(B,nil)),cons(C,nil))) ),
inference(paramod,[status(thm)],[c_47,c_60]) ).
cnf(c_85,plain,
( leqNat(s(s(lengthNat(A))),s(s(s(lengthNat(nil)))))
| ~ unique(cons(C,cons(B,A)))
| ~ sorted(append(append(rev(A),cons(B,nil)),cons(C,nil))) ),
inference(paramod,[status(thm)],[c_35,c_579]) ).
cnf(c_93,plain,
unique(cons(s(A),cons(lengthNat(nil),nil))),
inference(resolve,[status(thm)],[c_75,c_65]) ).
cnf(c_580,plain,
( elemNat(A,nil)
| B = A
| unique(cons(A,cons(B,nil))) ),
inference(resolve,[status(thm)],[c_75,c_37]) ).
cnf(c_97,plain,
( B = A
| unique(cons(A,cons(B,nil))) ),
inference(resolve,[status(thm)],[c_36,c_580]) ).
cnf(c_98,plain,
( elemNat(C,cons(B,cons(A,nil)))
| unique(cons(C,cons(B,cons(A,nil))))
| A = B ),
inference(resolve,[status(thm)],[c_97,c_43]) ).
cnf(c_99,plain,
( ~ elemNat(B,cons(A,nil))
| A = B ),
inference(resolve,[status(thm)],[c_97,c_41]) ).
cnf(c_101,plain,
( elemNat(A,cons(s(B),cons(lengthNat(nil),nil)))
| unique(cons(A,cons(s(B),cons(lengthNat(nil),nil)))) ),
inference(resolve,[status(thm)],[c_93,c_43]) ).
cnf(c_106,plain,
~ leqNat(s(s(s(s(A)))),s(s(s(lengthNat(nil))))),
inference(resolve,[status(thm)],[c_26,c_73]) ).
cnf(c_113,plain,
sorted(cons(s(s(lengthNat(nil))),cons(s(s(A)),nil))),
inference(resolve,[status(thm)],[c_80,c_53]) ).
cnf(c_581,plain,
( leqNat(s(s(lengthNat(cons(B,A)))),s(s(s(lengthNat(nil)))))
| ~ unique(cons(D,cons(C,cons(B,A))))
| ~ sorted(append(append(append(rev(A),cons(B,nil)),cons(C,nil)),cons(D,nil))) ),
inference(paramod,[status(thm)],[c_47,c_85]) ).
cnf(c_122,plain,
( leqNat(s(s(s(lengthNat(A)))),s(s(s(lengthNat(nil)))))
| ~ unique(cons(D,cons(C,cons(B,A))))
| ~ sorted(append(append(append(rev(A),cons(B,nil)),cons(C,nil)),cons(D,nil))) ),
inference(paramod,[status(thm)],[c_35,c_581]) ).
cnf(c_136,plain,
sorted(cons(s(lengthNat(nil)),cons(s(s(lengthNat(nil))),cons(s(s(A)),nil)))),
inference(resolve,[status(thm)],[c_113,c_79]) ).
cnf(c_142,plain,
( elemNat(C,cons(A,nil))
| B = C
| unique(cons(C,cons(B,cons(A,nil))))
| A = B ),
inference(resolve,[status(thm)],[c_98,c_37]) ).
cnf(c_146,plain,
( elemNat(A,cons(lengthNat(nil),nil))
| s(B) = A
| unique(cons(A,cons(s(B),cons(lengthNat(nil),nil)))) ),
inference(resolve,[status(thm)],[c_101,c_37]) ).
cnf(c_152,plain,
( A = C
| B = C
| unique(cons(C,cons(B,cons(A,nil))))
| A = B ),
inference(resolve,[status(thm)],[c_142,c_99]) ).
cnf(c_582,plain,
( A = s(B)
| unique(cons(s(B),cons(A,cons(lengthNat(nil),nil))))
| lengthNat(nil) = A ),
inference(resolve,[status(thm)],[c_142,c_65]) ).
cnf(c_154,plain,
( s(B) = A
| unique(cons(s(B),cons(A,cons(lengthNat(nil),nil))))
| lengthNat(nil) = A ),
inference(copy,[status(thm)],[c_582]) ).
cnf(c_159,plain,
( elemNat(D,cons(C,cons(B,cons(A,nil))))
| unique(cons(D,cons(C,cons(B,cons(A,nil)))))
| A = C
| B = C
| A = B ),
inference(resolve,[status(thm)],[c_152,c_43]) ).
cnf(c_180,plain,
( ~ elemNat(s(B),cons(A,cons(lengthNat(nil),nil)))
| s(B) = A
| lengthNat(nil) = A ),
inference(resolve,[status(thm)],[c_154,c_41]) ).
cnf(c_583,plain,
( unique(cons(s(B),cons(s(A),cons(lengthNat(nil),nil))))
| s(B) = s(A)
| lengthNat(nil) = s(A) ),
inference(resolve,[status(thm)],[c_180,c_101]) ).
cnf(c_181,plain,
( unique(cons(s(A),cons(s(B),cons(lengthNat(nil),nil))))
| s(A) = s(B) ),
inference(resolve,[status(thm)],[c_52,c_583]) ).
cnf(c_183,plain,
( ~ elemNat(s(A),cons(s(B),cons(lengthNat(nil),nil)))
| s(A) = s(B) ),
inference(resolve,[status(thm)],[c_181,c_41]) ).
cnf(c_584,plain,
( leqNat(s(s(s(lengthNat(cons(B,A))))),s(s(s(lengthNat(nil)))))
| ~ unique(cons(E,cons(D,cons(C,cons(B,A)))))
| ~ sorted(append(append(append(append(rev(A),cons(B,nil)),cons(C,nil)),cons(D,nil)),cons(E,nil))) ),
inference(paramod,[status(thm)],[c_47,c_122]) ).
cnf(c_585,plain,
( leqNat(s(s(s(s(lengthNat(A))))),s(s(s(lengthNat(nil)))))
| ~ unique(cons(E,cons(D,cons(C,cons(B,A)))))
| ~ sorted(append(append(append(append(rev(A),cons(B,nil)),cons(C,nil)),cons(D,nil)),cons(E,nil))) ),
inference(paramod,[status(thm)],[c_35,c_584]) ).
cnf(c_202,plain,
( ~ unique(cons(E,cons(D,cons(C,cons(B,A)))))
| ~ sorted(append(append(append(append(rev(A),cons(B,nil)),cons(C,nil)),cons(D,nil)),cons(E,nil))) ),
inference(resolve,[status(thm)],[c_106,c_585]) ).
cnf(c_213,plain,
( s(B) = s(A)
| unique(cons(s(A),cons(s(B),cons(lengthNat(nil),nil)))) ),
inference(resolve,[status(thm)],[c_146,c_65]) ).
cnf(c_216,plain,
( elemNat(C,cons(s(B),cons(s(A),cons(lengthNat(nil),nil))))
| unique(cons(C,cons(s(B),cons(s(A),cons(lengthNat(nil),nil)))))
| s(A) = s(B) ),
inference(resolve,[status(thm)],[c_213,c_43]) ).
cnf(c_248,plain,
sorted(cons(lengthNat(nil),cons(s(lengthNat(nil)),cons(s(s(lengthNat(nil))),cons(s(s(A)),nil))))),
inference(resolve,[status(thm)],[c_136,c_63]) ).
cnf(c_284,plain,
( elemNat(D,cons(B,cons(A,nil)))
| C = D
| unique(cons(D,cons(C,cons(B,cons(A,nil)))))
| A = C
| B = C
| A = B ),
inference(resolve,[status(thm)],[c_159,c_37]) ).
cnf(c_586,plain,
( ~ unique(cons(D,cons(C,cons(B,cons(A,nil)))))
| ~ sorted(append(append(append(append(nil,cons(A,nil)),cons(B,nil)),cons(C,nil)),cons(D,nil))) ),
inference(paramod,[status(thm)],[c_46,c_202]) ).
cnf(c_587,plain,
( ~ unique(cons(D,cons(C,cons(B,cons(A,nil)))))
| ~ sorted(append(append(append(cons(A,nil),cons(B,nil)),cons(C,nil)),cons(D,nil))) ),
inference(paramod,[status(thm)],[c_44,c_586]) ).
cnf(c_588,plain,
( ~ unique(cons(D,cons(C,cons(B,cons(A,nil)))))
| ~ sorted(append(append(cons(A,append(nil,cons(B,nil))),cons(C,nil)),cons(D,nil))) ),
inference(paramod,[status(thm)],[c_45,c_587]) ).
cnf(c_589,plain,
( ~ unique(cons(D,cons(C,cons(B,cons(A,nil)))))
| ~ sorted(append(append(cons(A,cons(B,nil)),cons(C,nil)),cons(D,nil))) ),
inference(paramod,[status(thm)],[c_44,c_588]) ).
cnf(c_590,plain,
( ~ unique(cons(D,cons(C,cons(B,cons(A,nil)))))
| ~ sorted(append(cons(A,append(cons(B,nil),cons(C,nil))),cons(D,nil))) ),
inference(paramod,[status(thm)],[c_45,c_589]) ).
cnf(c_591,plain,
( ~ unique(cons(D,cons(C,cons(B,cons(A,nil)))))
| ~ sorted(append(cons(A,cons(B,append(nil,cons(C,nil)))),cons(D,nil))) ),
inference(paramod,[status(thm)],[c_45,c_590]) ).
cnf(c_592,plain,
( ~ unique(cons(D,cons(C,cons(B,cons(A,nil)))))
| ~ sorted(append(cons(A,cons(B,cons(C,nil))),cons(D,nil))) ),
inference(paramod,[status(thm)],[c_44,c_591]) ).
cnf(c_593,plain,
( ~ unique(cons(D,cons(C,cons(B,cons(A,nil)))))
| ~ sorted(cons(A,append(cons(B,cons(C,nil)),cons(D,nil)))) ),
inference(paramod,[status(thm)],[c_45,c_592]) ).
cnf(c_594,plain,
( ~ unique(cons(D,cons(C,cons(B,cons(A,nil)))))
| ~ sorted(cons(A,cons(B,append(cons(C,nil),cons(D,nil))))) ),
inference(paramod,[status(thm)],[c_45,c_593]) ).
cnf(c_595,plain,
( ~ unique(cons(D,cons(C,cons(B,cons(A,nil)))))
| ~ sorted(cons(A,cons(B,cons(C,append(nil,cons(D,nil)))))) ),
inference(paramod,[status(thm)],[c_45,c_594]) ).
cnf(c_289,plain,
( ~ unique(cons(D,cons(C,cons(B,cons(A,nil)))))
| ~ sorted(cons(A,cons(B,cons(C,cons(D,nil))))) ),
inference(paramod,[status(thm)],[c_44,c_595]) ).
cnf(c_596,plain,
( s(C) = s(A)
| B = s(C)
| unique(cons(s(C),cons(B,cons(s(A),cons(lengthNat(nil),nil)))))
| lengthNat(nil) = B
| s(A) = B
| lengthNat(nil) = s(A) ),
inference(resolve,[status(thm)],[c_284,c_183]) ).
cnf(c_597,plain,
( s(C) = s(A)
| s(C) = B
| unique(cons(s(C),cons(B,cons(s(A),cons(lengthNat(nil),nil)))))
| lengthNat(nil) = B
| s(A) = B
| lengthNat(nil) = s(A) ),
inference(copy,[status(thm)],[c_596]) ).
cnf(c_338,plain,
( s(C) = s(A)
| s(C) = B
| unique(cons(s(C),cons(B,cons(s(A),cons(lengthNat(nil),nil)))))
| lengthNat(nil) = B
| s(A) = B ),
inference(resolve,[status(thm)],[c_52,c_597]) ).
cnf(c_377,plain,
( ~ elemNat(s(C),cons(B,cons(s(A),cons(lengthNat(nil),nil))))
| s(C) = s(A)
| s(C) = B
| lengthNat(nil) = B
| s(A) = B ),
inference(resolve,[status(thm)],[c_338,c_41]) ).
cnf(c_598,plain,
( unique(cons(s(C),cons(s(B),cons(s(A),cons(lengthNat(nil),nil)))))
| s(A) = s(B)
| s(C) = s(A)
| s(C) = s(B)
| lengthNat(nil) = s(B)
| s(A) = s(B) ),
inference(resolve,[status(thm)],[c_377,c_216]) ).
cnf(c_599,plain,
( unique(cons(s(C),cons(s(B),cons(s(A),cons(lengthNat(nil),nil)))))
| s(C) = s(A)
| s(C) = s(B)
| lengthNat(nil) = s(B)
| s(A) = s(B) ),
inference(copy,[status(thm)],[c_598]) ).
cnf(c_378,plain,
( unique(cons(s(C),cons(s(B),cons(s(A),cons(lengthNat(nil),nil)))))
| s(C) = s(A)
| s(C) = s(B)
| s(A) = s(B) ),
inference(resolve,[status(thm)],[c_52,c_599]) ).
cnf(c_379,plain,
( ~ sorted(cons(lengthNat(nil),cons(s(A),cons(s(B),cons(s(C),nil)))))
| s(C) = s(A)
| s(C) = s(B)
| s(A) = s(B) ),
inference(resolve,[status(thm)],[c_378,c_289]) ).
cnf(c_600,plain,
( s(s(A)) = s(lengthNat(nil))
| s(s(A)) = s(s(lengthNat(nil)))
| s(lengthNat(nil)) = s(s(lengthNat(nil))) ),
inference(resolve,[status(thm)],[c_248,c_379]) ).
cnf(c_601,plain,
( s(s(A)) = s(lengthNat(nil))
| s(s(A)) = s(s(lengthNat(nil)))
| s(s(lengthNat(nil))) = s(lengthNat(nil)) ),
inference(copy,[status(thm)],[c_600]) ).
cnf(c_602,plain,
( s(s(A)) = s(lengthNat(nil))
| s(s(lengthNat(nil))) = s(s(A))
| s(s(lengthNat(nil))) = s(lengthNat(nil)) ),
inference(copy,[status(thm)],[c_601]) ).
cnf(c_392,plain,
( s(lengthNat(nil)) = s(s(A))
| s(s(lengthNat(nil))) = s(s(A))
| s(s(lengthNat(nil))) = s(lengthNat(nil)) ),
inference(copy,[status(thm)],[c_602]) ).
cnf(c_603,plain,
( proj1S(s(lengthNat(nil))) = s(lengthNat(nil))
| s(lengthNat(nil)) = s(s(A))
| s(s(lengthNat(nil))) = s(s(A)) ),
inference(paramod,[status(thm)],[c_392,c_22]) ).
cnf(c_604,plain,
( lengthNat(nil) = s(lengthNat(nil))
| s(lengthNat(nil)) = s(s(A))
| s(s(lengthNat(nil))) = s(s(A)) ),
inference(paramod,[status(thm)],[c_22,c_603]) ).
cnf(c_605,plain,
( s(lengthNat(nil)) = lengthNat(nil)
| s(lengthNat(nil)) = s(s(A))
| s(s(lengthNat(nil))) = s(s(A)) ),
inference(copy,[status(thm)],[c_604]) ).
cnf(c_404,plain,
( s(lengthNat(nil)) = s(s(A))
| s(s(lengthNat(nil))) = s(s(A)) ),
inference(resolve,[status(thm)],[c_52,c_605]) ).
cnf(c_606,plain,
( proj1S(s(s(A))) = s(lengthNat(nil))
| s(lengthNat(nil)) = s(s(A)) ),
inference(paramod,[status(thm)],[c_404,c_22]) ).
cnf(c_607,plain,
( s(A) = s(lengthNat(nil))
| s(lengthNat(nil)) = s(s(A)) ),
inference(paramod,[status(thm)],[c_22,c_606]) ).
cnf(c_469,plain,
( s(lengthNat(nil)) = s(A)
| s(lengthNat(nil)) = s(s(A)) ),
inference(copy,[status(thm)],[c_607]) ).
cnf(c_608,plain,
( proj1S(s(s(A))) = lengthNat(nil)
| s(lengthNat(nil)) = s(A) ),
inference(paramod,[status(thm)],[c_469,c_22]) ).
cnf(c_609,plain,
( s(A) = lengthNat(nil)
| s(lengthNat(nil)) = s(A) ),
inference(paramod,[status(thm)],[c_22,c_608]) ).
cnf(c_610,plain,
( lengthNat(nil) = s(A)
| s(lengthNat(nil)) = s(A) ),
inference(copy,[status(thm)],[c_609]) ).
cnf(c_570,plain,
s(lengthNat(nil)) = s(A),
inference(resolve,[status(thm)],[c_52,c_610]) ).
cnf(c_611,plain,
proj1S(s(A)) = lengthNat(nil),
inference(paramod,[status(thm)],[c_570,c_22]) ).
cnf(c_612,plain,
A = lengthNat(nil),
inference(paramod,[status(thm)],[c_22,c_611]) ).
cnf(c_573,plain,
lengthNat(nil) = A,
inference(copy,[status(thm)],[c_612]) ).
cnf(c_574,plain,
$false,
inference(resolve,[status(thm)],[c_573,c_52]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SWX203+1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.06 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.18/5.45 % Computer : n017.cluster.edu
% 0.18/5.45 % Model : x86_64 x86_64
% 0.18/5.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/5.45 % Memory : 8046.5625MB
% 0.18/5.45 % OS : Linux 6.8.0-71-generic
% 0.18/5.45 % CPULimit : 300
% 0.18/5.45 % WCLimit : 300
% 0.18/5.45 % DateTime : Sat Sep 26 16:50:40 UTC 2026
% 0.18/5.45 % CPUTime :
% 0.18/5.45 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.18/5.45 % Process 1205993 was started by sandbox on n017,
% 0.18/5.45 % Sat Sep 26 16:50:40 2026
% 0.18/5.45 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.18/5.46
% 0.18/5.46 % From the command line: assign(max_seconds, 300).
% 0.22/5.78
% 0.22/5.78 % SZS status Theorem for theBenchmark
% 0.22/5.78
% 0.22/5.78 % Proof 1 at 0.23 (+ 0.08) seconds.
% 0.22/5.78 % Length of proof is 85.
% 0.22/5.78 % Level of proof is 20.
% 0.22/5.78 % Maximum clause weight is 99.000.
% 0.22/5.78 % Given clauses 278.
% 0.22/5.78
% 0.22/5.78 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------