%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : SWX203+1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d
% Computer : n017.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 : Tue May 5 05:34:43 PM UTC 2026
% Result : Theorem 2.05s 1.94s
% Output : CNFRefutation 2.05s
% Verified :
% SZS Type : Refutation
% Derivation depth : 28
% Number of leaves : 18
% Syntax : Number of formulae : 94 ( 47 unt; 0 def)
% Number of atoms : 241 ( 56 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 210 ( 63 ~; 128 |; 10 &)
% ( 5 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 3 avg)
% Maximal term depth : 6 ( 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 : 143 ( 9 sgn 53 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(axiom_021,axiom,
! [X3,X7] : rev(cons(X3,X7)) = append(rev(X7),cons(X3,nil)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_021) ).
fof(axiom_018,axiom,
! [X3] : append(nil,X3) = X3,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_018) ).
fof(axiom_017,axiom,
! [X3,X7] :
( unique(cons(X3,X7))
<=> ( ~ elemNat(X3,X7)
& unique(X7) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_017) ).
fof(axiom_014,axiom,
! [X1] : ~ elemNat(X1,nil),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_014) ).
fof(axiom_020,axiom,
rev(nil) = nil,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_020) ).
fof(axiom_019,axiom,
! [X3,X4,X7] : append(cons(X4,X7),X3) = cons(X4,append(X7,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_019) ).
fof(goal_022,conjecture,
? [X7] :
~ ( sorted(rev(X7))
=> ( unique(X7)
=> leqNat(lengthNat(X7),s(s(s(z)))) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goal_022) ).
fof(axiom_016,axiom,
unique(nil),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_016) ).
fof(axiom_013,axiom,
! [X3,X7] : lengthNat(cons(X3,X7)) = s(lengthNat(X7)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_013) ).
fof(axiom_012,axiom,
lengthNat(nil) = z,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_012) ).
fof(axiom_011,axiom,
! [X3,X6,X7] :
( sorted(cons(X3,cons(X6,X7)))
<=> ( leqNat(X3,X6)
& sorted(cons(X6,X7)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_011) ).
fof(axiom_010,axiom,
! [X3] : sorted(cons(X3,nil)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_010) ).
fof(axiom_006,axiom,
! [X3] : leqNat(z,X3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_006) ).
fof(axiom_008,axiom,
! [X4,X5] :
( leqNat(s(X4),s(X5))
<=> leqNat(X4,X5) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_008) ).
fof(axiom_015,axiom,
! [X1,X4,X7] :
( elemNat(X1,cons(X4,X7))
<=> ( X1 = X4
| elemNat(X1,X7) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_015) ).
fof(axiom_005,axiom,
! [X1] : z != s(X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_005) ).
fof(axiom_007,axiom,
! [X4] : ~ leqNat(s(X4),z),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_007) ).
fof(axiom_004,axiom,
! [X1] : proj1S(s(X1)) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_004) ).
fof(c_0_18,plain,
! [X67,X68] : rev(cons(X67,X68)) = append(rev(X68),cons(X67,nil)),
inference(variable_rename,[status(thm)],[axiom_021]) ).
fof(c_0_19,plain,
! [X63] : append(nil,X63) = X63,
inference(variable_rename,[status(thm)],[axiom_018]) ).
fof(c_0_20,plain,
! [X3,X7] :
( unique(cons(X3,X7))
<=> ( ~ elemNat(X3,X7)
& unique(X7) ) ),
inference(fof_simplification,[status(thm)],[axiom_017]) ).
fof(c_0_21,plain,
! [X1] : ~ elemNat(X1,nil),
inference(fof_simplification,[status(thm)],[axiom_014]) ).
cnf(c_0_22,plain,
rev(cons(X1,X2)) = append(rev(X2),cons(X1,nil)),
inference(split_conjunct,[status(thm)],[c_0_18]) ).
cnf(c_0_23,plain,
rev(nil) = nil,
inference(split_conjunct,[status(thm)],[axiom_020]) ).
cnf(c_0_24,plain,
append(nil,X1) = X1,
inference(split_conjunct,[status(thm)],[c_0_19]) ).
fof(c_0_25,plain,
! [X64,X65,X66] : append(cons(X65,X66),X64) = cons(X65,append(X66,X64)),
inference(variable_rename,[status(thm)],[axiom_019]) ).
fof(c_0_26,plain,
! [X61,X62] :
( ( ~ elemNat(X61,X62)
| ~ unique(cons(X61,X62)) )
& ( unique(X62)
| ~ unique(cons(X61,X62)) )
& ( elemNat(X61,X62)
| ~ unique(X62)
| unique(cons(X61,X62)) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_20])])]) ).
fof(c_0_27,plain,
! [X57] : ~ elemNat(X57,nil),
inference(variable_rename,[status(thm)],[c_0_21]) ).
fof(c_0_28,negated_conjecture,
~ ? [X7] :
~ ( sorted(rev(X7))
=> ( unique(X7)
=> leqNat(lengthNat(X7),s(s(s(z)))) ) ),
inference(assume_negation,[status(cth)],[goal_022]) ).
cnf(c_0_29,plain,
rev(cons(X1,nil)) = cons(X1,nil),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_22,c_0_23]),c_0_24]) ).
cnf(c_0_30,plain,
append(cons(X1,X2),X3) = cons(X1,append(X2,X3)),
inference(split_conjunct,[status(thm)],[c_0_25]) ).
cnf(c_0_31,plain,
( elemNat(X1,X2)
| unique(cons(X1,X2))
| ~ unique(X2) ),
inference(split_conjunct,[status(thm)],[c_0_26]) ).
cnf(c_0_32,plain,
unique(nil),
inference(split_conjunct,[status(thm)],[axiom_016]) ).
cnf(c_0_33,plain,
~ elemNat(X1,nil),
inference(split_conjunct,[status(thm)],[c_0_27]) ).
fof(c_0_34,negated_conjecture,
! [X69] :
( ~ sorted(rev(X69))
| ~ unique(X69)
| leqNat(lengthNat(X69),s(s(s(z)))) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_28])]) ).
fof(c_0_35,plain,
! [X55,X56] : lengthNat(cons(X55,X56)) = s(lengthNat(X56)),
inference(variable_rename,[status(thm)],[axiom_013]) ).
cnf(c_0_36,plain,
rev(cons(X1,cons(X2,nil))) = cons(X2,cons(X1,nil)),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_22,c_0_29]),c_0_30]),c_0_24]) ).
cnf(c_0_37,plain,
unique(cons(X1,nil)),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_31,c_0_32]),c_0_33]) ).
cnf(c_0_38,negated_conjecture,
( leqNat(lengthNat(X1),s(s(s(z))))
| ~ sorted(rev(X1))
| ~ unique(X1) ),
inference(split_conjunct,[status(thm)],[c_0_34]) ).
cnf(c_0_39,plain,
lengthNat(cons(X1,X2)) = s(lengthNat(X2)),
inference(split_conjunct,[status(thm)],[c_0_35]) ).
cnf(c_0_40,plain,
rev(cons(X1,cons(X2,cons(X3,nil)))) = cons(X3,cons(X2,cons(X1,nil))),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_22,c_0_36]),c_0_30]),c_0_30]),c_0_24]) ).
cnf(c_0_41,plain,
( unique(cons(X1,cons(X2,nil)))
| elemNat(X1,cons(X2,nil)) ),
inference(spm,[status(thm)],[c_0_31,c_0_37]) ).
cnf(c_0_42,negated_conjecture,
( leqNat(s(lengthNat(X1)),s(s(s(z))))
| ~ unique(cons(X2,X1))
| ~ sorted(rev(cons(X2,X1))) ),
inference(spm,[status(thm)],[c_0_38,c_0_39]) ).
cnf(c_0_43,plain,
rev(cons(X1,cons(X2,cons(X3,cons(X4,nil))))) = cons(X4,cons(X3,cons(X2,cons(X1,nil)))),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_22,c_0_40]),c_0_30]),c_0_30]),c_0_30]),c_0_24]) ).
cnf(c_0_44,plain,
lengthNat(nil) = z,
inference(split_conjunct,[status(thm)],[axiom_012]) ).
cnf(c_0_45,plain,
( unique(cons(X1,cons(X2,cons(X3,nil))))
| elemNat(X1,cons(X2,cons(X3,nil)))
| elemNat(X2,cons(X3,nil)) ),
inference(spm,[status(thm)],[c_0_31,c_0_41]) ).
cnf(c_0_46,negated_conjecture,
( leqNat(s(s(s(s(z)))),s(s(s(z))))
| ~ unique(cons(X1,cons(X2,cons(X3,cons(X4,nil)))))
| ~ sorted(cons(X4,cons(X3,cons(X2,cons(X1,nil))))) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_42,c_0_43]),c_0_39]),c_0_39]),c_0_39]),c_0_44]) ).
cnf(c_0_47,plain,
( unique(cons(X1,cons(X2,cons(X3,cons(X4,nil)))))
| elemNat(X1,cons(X2,cons(X3,cons(X4,nil))))
| elemNat(X2,cons(X3,cons(X4,nil)))
| elemNat(X3,cons(X4,nil)) ),
inference(spm,[status(thm)],[c_0_31,c_0_45]) ).
fof(c_0_48,plain,
! [X52,X53,X54] :
( ( leqNat(X52,X53)
| ~ sorted(cons(X52,cons(X53,X54))) )
& ( sorted(cons(X53,X54))
| ~ sorted(cons(X52,cons(X53,X54))) )
& ( ~ leqNat(X52,X53)
| ~ sorted(cons(X53,X54))
| sorted(cons(X52,cons(X53,X54))) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_011])])]) ).
cnf(c_0_49,negated_conjecture,
( elemNat(X1,cons(X2,cons(X3,cons(X4,nil))))
| elemNat(X2,cons(X3,cons(X4,nil)))
| elemNat(X3,cons(X4,nil))
| leqNat(s(s(s(s(z)))),s(s(s(z))))
| ~ sorted(cons(X4,cons(X3,cons(X2,cons(X1,nil))))) ),
inference(spm,[status(thm)],[c_0_46,c_0_47]) ).
cnf(c_0_50,plain,
( sorted(cons(X1,cons(X2,X3)))
| ~ leqNat(X1,X2)
| ~ sorted(cons(X2,X3)) ),
inference(split_conjunct,[status(thm)],[c_0_48]) ).
cnf(c_0_51,negated_conjecture,
( elemNat(X1,cons(X2,cons(X3,cons(X4,nil))))
| elemNat(X2,cons(X3,cons(X4,nil)))
| elemNat(X3,cons(X4,nil))
| leqNat(s(s(s(s(z)))),s(s(s(z))))
| ~ sorted(cons(X3,cons(X2,cons(X1,nil))))
| ~ leqNat(X4,X3) ),
inference(spm,[status(thm)],[c_0_49,c_0_50]) ).
fof(c_0_52,plain,
! [X51] : sorted(cons(X51,nil)),
inference(variable_rename,[status(thm)],[axiom_010]) ).
cnf(c_0_53,negated_conjecture,
( leqNat(s(s(z)),s(s(s(z))))
| ~ unique(cons(X1,cons(X2,nil)))
| ~ sorted(cons(X2,cons(X1,nil))) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_42,c_0_36]),c_0_39]),c_0_44]) ).
cnf(c_0_54,negated_conjecture,
( elemNat(X1,cons(X2,cons(X3,cons(X4,nil))))
| elemNat(X2,cons(X3,cons(X4,nil)))
| elemNat(X3,cons(X4,nil))
| leqNat(s(s(s(s(z)))),s(s(s(z))))
| ~ sorted(cons(X2,cons(X1,nil)))
| ~ leqNat(X4,X3)
| ~ leqNat(X3,X2) ),
inference(spm,[status(thm)],[c_0_51,c_0_50]) ).
cnf(c_0_55,plain,
sorted(cons(X1,nil)),
inference(split_conjunct,[status(thm)],[c_0_52]) ).
fof(c_0_56,plain,
! [X47] : leqNat(z,X47),
inference(variable_rename,[status(thm)],[axiom_006]) ).
cnf(c_0_57,negated_conjecture,
( elemNat(X1,cons(X2,nil))
| leqNat(s(s(z)),s(s(s(z))))
| ~ sorted(cons(X2,cons(X1,nil))) ),
inference(spm,[status(thm)],[c_0_53,c_0_41]) ).
cnf(c_0_58,negated_conjecture,
( elemNat(X1,cons(X2,cons(X3,cons(X4,nil))))
| elemNat(X2,cons(X3,cons(X4,nil)))
| elemNat(X3,cons(X4,nil))
| leqNat(s(s(s(s(z)))),s(s(s(z))))
| ~ leqNat(X4,X3)
| ~ leqNat(X3,X2)
| ~ leqNat(X2,X1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_54,c_0_50]),c_0_55])]) ).
cnf(c_0_59,plain,
leqNat(z,X1),
inference(split_conjunct,[status(thm)],[c_0_56]) ).
fof(c_0_60,plain,
! [X49,X50] :
( ( ~ leqNat(s(X49),s(X50))
| leqNat(X49,X50) )
& ( ~ leqNat(X49,X50)
| leqNat(s(X49),s(X50)) ) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_008])]) ).
fof(c_0_61,plain,
! [X58,X59,X60] :
( ( ~ elemNat(X58,cons(X59,X60))
| X58 = X59
| elemNat(X58,X60) )
& ( X58 != X59
| elemNat(X58,cons(X59,X60)) )
& ( ~ elemNat(X58,X60)
| elemNat(X58,cons(X59,X60)) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_015])])]) ).
cnf(c_0_62,negated_conjecture,
( elemNat(X1,cons(X2,nil))
| leqNat(s(s(z)),s(s(s(z))))
| ~ leqNat(X2,X1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_57,c_0_50]),c_0_55])]) ).
cnf(c_0_63,negated_conjecture,
( elemNat(X1,cons(X2,cons(X3,cons(z,nil))))
| elemNat(X2,cons(X3,cons(z,nil)))
| elemNat(X3,cons(z,nil))
| leqNat(s(s(s(s(z)))),s(s(s(z))))
| ~ leqNat(X3,X2)
| ~ leqNat(X2,X1) ),
inference(spm,[status(thm)],[c_0_58,c_0_59]) ).
cnf(c_0_64,plain,
( leqNat(s(X1),s(X2))
| ~ leqNat(X1,X2) ),
inference(split_conjunct,[status(thm)],[c_0_60]) ).
cnf(c_0_65,plain,
( X1 = X2
| elemNat(X1,X3)
| ~ elemNat(X1,cons(X2,X3)) ),
inference(split_conjunct,[status(thm)],[c_0_61]) ).
cnf(c_0_66,negated_conjecture,
( elemNat(X1,cons(z,nil))
| leqNat(s(s(z)),s(s(s(z)))) ),
inference(spm,[status(thm)],[c_0_62,c_0_59]) ).
fof(c_0_67,plain,
! [X46] : z != s(X46),
inference(variable_rename,[status(thm)],[axiom_005]) ).
cnf(c_0_68,negated_conjecture,
( elemNat(X1,cons(s(X2),cons(s(X3),cons(z,nil))))
| elemNat(s(X2),cons(s(X3),cons(z,nil)))
| elemNat(s(X3),cons(z,nil))
| leqNat(s(s(s(s(z)))),s(s(s(z))))
| ~ leqNat(s(X2),X1)
| ~ leqNat(X3,X2) ),
inference(spm,[status(thm)],[c_0_63,c_0_64]) ).
cnf(c_0_69,negated_conjecture,
( X1 = z
| leqNat(s(s(z)),s(s(s(z)))) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_65,c_0_66]),c_0_33]) ).
cnf(c_0_70,plain,
z != s(X1),
inference(split_conjunct,[status(thm)],[c_0_67]) ).
cnf(c_0_71,negated_conjecture,
( elemNat(s(X1),cons(s(X2),cons(s(X3),cons(z,nil))))
| elemNat(s(X2),cons(s(X3),cons(z,nil)))
| elemNat(s(X3),cons(z,nil))
| leqNat(s(s(s(s(z)))),s(s(s(z))))
| ~ leqNat(X3,X2)
| ~ leqNat(X2,X1) ),
inference(spm,[status(thm)],[c_0_68,c_0_64]) ).
cnf(c_0_72,plain,
( leqNat(X1,X2)
| ~ leqNat(s(X1),s(X2)) ),
inference(split_conjunct,[status(thm)],[c_0_60]) ).
cnf(c_0_73,negated_conjecture,
leqNat(s(s(z)),s(s(s(z)))),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_39,c_0_69]),c_0_70]) ).
cnf(c_0_74,negated_conjecture,
( elemNat(s(X1),cons(s(X2),cons(s(z),cons(z,nil))))
| elemNat(s(X2),cons(s(z),cons(z,nil)))
| elemNat(s(z),cons(z,nil))
| leqNat(s(s(s(s(z)))),s(s(s(z))))
| ~ leqNat(X2,X1) ),
inference(spm,[status(thm)],[c_0_71,c_0_59]) ).
cnf(c_0_75,negated_conjecture,
leqNat(s(z),s(s(z))),
inference(spm,[status(thm)],[c_0_72,c_0_73]) ).
cnf(c_0_76,negated_conjecture,
( elemNat(s(s(s(z))),cons(s(s(z)),cons(s(z),cons(z,nil))))
| elemNat(s(s(z)),cons(s(z),cons(z,nil)))
| elemNat(s(z),cons(z,nil))
| leqNat(s(s(s(s(z)))),s(s(s(z)))) ),
inference(spm,[status(thm)],[c_0_74,c_0_75]) ).
cnf(c_0_77,negated_conjecture,
( s(s(s(z))) = s(s(z))
| elemNat(s(s(s(z))),cons(s(z),cons(z,nil)))
| elemNat(s(s(z)),cons(s(z),cons(z,nil)))
| elemNat(s(z),cons(z,nil))
| leqNat(s(s(s(s(z)))),s(s(s(z)))) ),
inference(spm,[status(thm)],[c_0_65,c_0_76]) ).
cnf(c_0_78,negated_conjecture,
( s(s(s(z))) = s(s(z))
| elemNat(s(s(s(z))),cons(s(z),cons(z,nil)))
| elemNat(s(s(z)),cons(s(z),cons(z,nil)))
| elemNat(s(z),cons(z,nil))
| leqNat(s(s(s(z))),s(s(z))) ),
inference(spm,[status(thm)],[c_0_72,c_0_77]) ).
cnf(c_0_79,negated_conjecture,
( s(s(s(z))) = s(s(z))
| s(s(s(z))) = s(z)
| elemNat(s(s(z)),cons(s(z),cons(z,nil)))
| elemNat(s(s(s(z))),cons(z,nil))
| elemNat(s(z),cons(z,nil))
| leqNat(s(s(s(z))),s(s(z))) ),
inference(spm,[status(thm)],[c_0_65,c_0_78]) ).
cnf(c_0_80,negated_conjecture,
( s(s(s(z))) = s(s(z))
| s(s(s(z))) = s(z)
| s(s(z)) = s(z)
| elemNat(s(s(s(z))),cons(z,nil))
| elemNat(s(s(z)),cons(z,nil))
| elemNat(s(z),cons(z,nil))
| leqNat(s(s(s(z))),s(s(z))) ),
inference(spm,[status(thm)],[c_0_65,c_0_79]) ).
cnf(c_0_81,negated_conjecture,
( s(s(s(z))) = s(s(z))
| s(s(s(z))) = s(z)
| s(s(z)) = s(z)
| elemNat(s(s(s(z))),cons(z,nil))
| elemNat(s(s(z)),cons(z,nil))
| elemNat(s(z),cons(z,nil))
| leqNat(s(s(z)),s(z)) ),
inference(spm,[status(thm)],[c_0_72,c_0_80]) ).
fof(c_0_82,plain,
! [X4] : ~ leqNat(s(X4),z),
inference(fof_simplification,[status(thm)],[axiom_007]) ).
cnf(c_0_83,negated_conjecture,
( s(s(s(z))) = s(s(z))
| s(s(s(z))) = s(z)
| s(s(z)) = s(z)
| elemNat(s(s(z)),cons(z,nil))
| elemNat(s(z),cons(z,nil))
| leqNat(s(s(z)),s(z)) ),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_65,c_0_81]),c_0_70]),c_0_33]) ).
fof(c_0_84,plain,
! [X48] : ~ leqNat(s(X48),z),
inference(variable_rename,[status(thm)],[c_0_82]) ).
cnf(c_0_85,negated_conjecture,
( s(s(s(z))) = s(s(z))
| s(s(s(z))) = s(z)
| s(s(z)) = s(z)
| elemNat(s(z),cons(z,nil))
| leqNat(s(s(z)),s(z)) ),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_65,c_0_83]),c_0_70]),c_0_33]) ).
cnf(c_0_86,plain,
~ leqNat(s(X1),z),
inference(split_conjunct,[status(thm)],[c_0_84]) ).
fof(c_0_87,plain,
! [X45] : proj1S(s(X45)) = X45,
inference(variable_rename,[status(thm)],[axiom_004]) ).
cnf(c_0_88,negated_conjecture,
( s(s(s(z))) = s(s(z))
| s(s(s(z))) = s(z)
| s(s(z)) = s(z)
| elemNat(s(z),cons(z,nil)) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_72,c_0_85]),c_0_86]) ).
cnf(c_0_89,plain,
proj1S(s(X1)) = X1,
inference(split_conjunct,[status(thm)],[c_0_87]) ).
cnf(c_0_90,negated_conjecture,
( s(s(s(z))) = s(s(z))
| s(s(s(z))) = s(z)
| s(s(z)) = s(z) ),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_65,c_0_88]),c_0_70]),c_0_33]) ).
cnf(c_0_91,negated_conjecture,
( s(s(s(z))) = s(z)
| s(s(z)) = s(z) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_89,c_0_90]),c_0_89])]) ).
cnf(c_0_92,negated_conjecture,
s(s(z)) = s(z),
inference(sr,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_89,c_0_91]),c_0_89]),c_0_70]) ).
cnf(c_0_93,negated_conjecture,
$false,
inference(sr,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_89,c_0_92]),c_0_89]),c_0_70]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SWX203+1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.12 % Command : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d
% 0.16/0.32 % Computer : n017.cluster.edu
% 0.16/0.32 % Model : x86_64 x86_64
% 0.16/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.32 % Memory : 8042.1875MB
% 0.16/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.33 % CPULimit : 300
% 0.16/0.33 % WCLimit : 300
% 0.16/0.33 % DateTime : Tue May 5 07:55:12 EDT 2026
% 0.16/0.33 % CPUTime :
% 0.16/0.34 % start to proof: theBenchmark
% 2.05/1.94 % Version : CSE_E---1.7
% 2.05/1.94 % Problem : theBenchmark.p
% 2.05/1.94 % SZS status Theorem for theBenchmark.p
% 2.05/1.94 % SZS output start CNFRefutation
% See solution above
% 2.05/1.94 % Total time : 1.374s
%------------------------------------------------------------------------------