%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : SWX197+1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox2/solver/bin/cse --final-prover /export/starexec/sandbox2/solver/bin/eprover --proof-time %d --global-time-limit %d
% Computer : n022.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:41 PM UTC 2026
% Result : Theorem 273.62s 108.32s
% Output : CNFRefutation 274.23s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 28
% Syntax : Number of formulae : 136 ( 111 unt; 0 def)
% Number of atoms : 168 ( 167 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 71 ( 39 ~; 28 |; 0 &)
% ( 0 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 2 avg)
% Maximal term depth : 9 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 30 ( 30 usr; 4 con; 0-3 aty)
% Number of variables : 362 ( 63 sgn 129 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(axiom_045,axiom,
! [X1] :
( X1 != while(proj1While(X1),proj2While(X1))
=> ( X1 != if(proj1If(X1),proj2If(X1),proj3If(X1))
=> opti2(X1) = X1 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_045) ).
fof(axiom_073,axiom,
! [X14] : apply1(lam,X14) = opti2(X14),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_073) ).
fof(axiom_066,axiom,
! [X1,X13,X21,X10] : run(X1,cons2(while(X21,X10),X13)) = run(X1,cons2(if(X21,append(X10,cons2(while(X21,X10),nil2)),nil2),X13)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_066) ).
fof(axiom_072,axiom,
! [X14,X6,X25] : append(cons2(X6,X25),X14) = cons2(X6,append(X25,X14)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_072) ).
fof(axiom_068,axiom,
! [X1,X13,X22,X12,X23,X3] :
( eval(X1,X22) = suc(X3)
=> run(X1,cons2(if(X22,X12,X23),X13)) = run(X1,append(X12,X13)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_068) ).
fof(axiom_057,axiom,
! [X1,X7] : eval(X1,n(X7)) = X7,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_057) ).
fof(axiom_046,axiom,
! [X9,X10] : opti2(while(X9,X10)) = while(X9,map(lam,X10)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_046) ).
fof(axiom_031,axiom,
! [X1,X2,X3,X4] : print(X1) != if(X2,X3,X4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_031) ).
fof(axiom_030,axiom,
! [X1,X2,X3] : print(X1) != while(X2,X3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_030) ).
fof(axiom_035,axiom,
! [X1,X2] : head(cons(X1,X2)) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_035) ).
fof(axiom_064,axiom,
! [X1,X13,X9] : run(X1,cons2(print(X9),X13)) = cons(eval(X1,X9),run(X1,X13)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_064) ).
fof(axiom_070,axiom,
! [X24,X14,X25] : map(X24,cons2(X14,X25)) = cons2(apply1(X24,X14),map(X24,X25)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_070) ).
fof(axiom_065,axiom,
! [X1,X13,X2,X20] : run(X1,cons2(x(X2,X20),X13)) = run(store(X1,X2,eval(X1,X20)),X13),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_065) ).
fof(axiom_060,axiom,
! [X1,X18,X19] :
( eval(X1,X18) = eval(X1,X19)
=> eval(X1,eq(X18,X19)) = suc(zero) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_060) ).
fof(axiom_049,axiom,
! [X7,X8] : fetch(cons(X7,X8),zero) = X7,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_049) ).
fof(axiom_062,axiom,
! [X1,X6] : eval(X1,v(X6)) = fetch(X1,X6),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_062) ).
fof(axiom_050,axiom,
! [X7,X8,X6] : fetch(cons(X7,X8),suc(X6)) = fetch(X8,X6),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_050) ).
fof(axiom_058,axiom,
! [X1,X15,X16] : eval(X1,add(X15,X16)) = addNat(eval(X1,X15),eval(X1,X16)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_058) ).
fof(axiom_041,axiom,
! [X6] : store(nil,zero,X6) = cons(X6,nil),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_041) ).
fof(axiom_048,axiom,
! [X14] : fetch(nil,X14) = zero,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_048) ).
fof(axiom_051,axiom,
! [X14] : addNat(zero,X14) = X14,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_051) ).
fof(axiom_053,axiom,
! [X6,X2] : addNat(suc(X6),suc(X2)) = suc(addNat(X6,suc(X2))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_053) ).
fof(axiom_047,axiom,
! [X11,X12,X13] : opti2(if(X11,X12,X13)) = if(add(n(suc(zero)),X11),X13,X12),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_047) ).
fof(goal_074,conjecture,
? [X10] : run(nil,cons2(X10,nil2)) != run(nil,cons2(opti2(X10),nil2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goal_074) ).
fof(axiom_069,axiom,
! [X24] : map(X24,nil2) = nil2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_069) ).
fof(axiom_037,axiom,
! [X1,X2] : nil != cons(X1,X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_037) ).
fof(axiom_071,axiom,
! [X14] : append(nil2,X14) = X14,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_071) ).
fof(axiom_063,axiom,
! [X1] : run(X1,nil2) = nil,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_063) ).
fof(c_0_28,plain,
! [X319] :
( X319 = while(proj1While(X319),proj2While(X319))
| X319 = if(proj1If(X319),proj2If(X319),proj3If(X319))
| opti2(X319) = X319 ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_045])]) ).
fof(c_0_29,plain,
! [X386] : apply1(lam,X386) = opti2(X386),
inference(variable_rename,[status(thm)],[axiom_073]) ).
fof(c_0_30,plain,
! [X363,X364,X365,X366] : run(X363,cons2(while(X365,X366),X364)) = run(X363,cons2(if(X365,append(X366,cons2(while(X365,X366),nil2)),nil2),X364)),
inference(variable_rename,[status(thm)],[axiom_066]) ).
fof(c_0_31,plain,
! [X383,X384,X385] : append(cons2(X384,X385),X383) = cons2(X384,append(X385,X383)),
inference(variable_rename,[status(thm)],[axiom_072]) ).
fof(c_0_32,plain,
! [X372,X373,X374,X375,X376,X377] :
( eval(X372,X374) != suc(X377)
| run(X372,cons2(if(X374,X375,X376),X373)) = run(X372,append(X375,X373)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_068])]) ).
fof(c_0_33,plain,
! [X339,X340] : eval(X339,n(X340)) = X340,
inference(variable_rename,[status(thm)],[axiom_057]) ).
fof(c_0_34,plain,
! [X320,X321] : opti2(while(X320,X321)) = while(X320,map(lam,X321)),
inference(variable_rename,[status(thm)],[axiom_046]) ).
fof(c_0_35,plain,
! [X279,X280,X281,X282] : print(X279) != if(X280,X281,X282),
inference(variable_rename,[status(thm)],[axiom_031]) ).
cnf(c_0_36,plain,
( X1 = while(proj1While(X1),proj2While(X1))
| X1 = if(proj1If(X1),proj2If(X1),proj3If(X1))
| opti2(X1) = X1 ),
inference(split_conjunct,[status(thm)],[c_0_28]) ).
cnf(c_0_37,plain,
apply1(lam,X1) = opti2(X1),
inference(split_conjunct,[status(thm)],[c_0_29]) ).
fof(c_0_38,plain,
! [X276,X277,X278] : print(X276) != while(X277,X278),
inference(variable_rename,[status(thm)],[axiom_030]) ).
fof(c_0_39,plain,
! [X297,X298] : head(cons(X297,X298)) = X297,
inference(variable_rename,[status(thm)],[axiom_035]) ).
fof(c_0_40,plain,
! [X356,X357,X358] : run(X356,cons2(print(X358),X357)) = cons(eval(X356,X358),run(X356,X357)),
inference(variable_rename,[status(thm)],[axiom_064]) ).
cnf(c_0_41,plain,
run(X1,cons2(while(X2,X3),X4)) = run(X1,cons2(if(X2,append(X3,cons2(while(X2,X3),nil2)),nil2),X4)),
inference(split_conjunct,[status(thm)],[c_0_30]) ).
cnf(c_0_42,plain,
append(cons2(X1,X2),X3) = cons2(X1,append(X2,X3)),
inference(split_conjunct,[status(thm)],[c_0_31]) ).
cnf(c_0_43,plain,
( run(X1,cons2(if(X2,X4,X5),X6)) = run(X1,append(X4,X6))
| eval(X1,X2) != suc(X3) ),
inference(split_conjunct,[status(thm)],[c_0_32]) ).
cnf(c_0_44,plain,
eval(X1,n(X2)) = X2,
inference(split_conjunct,[status(thm)],[c_0_33]) ).
fof(c_0_45,plain,
! [X379,X380,X381] : map(X379,cons2(X380,X381)) = cons2(apply1(X379,X380),map(X379,X381)),
inference(variable_rename,[status(thm)],[axiom_070]) ).
cnf(c_0_46,plain,
opti2(while(X1,X2)) = while(X1,map(lam,X2)),
inference(split_conjunct,[status(thm)],[c_0_34]) ).
cnf(c_0_47,plain,
print(X1) != if(X2,X3,X4),
inference(split_conjunct,[status(thm)],[c_0_35]) ).
cnf(c_0_48,plain,
( apply1(lam,X1) = X1
| X1 = while(proj1While(X1),proj2While(X1))
| X1 = if(proj1If(X1),proj2If(X1),proj3If(X1)) ),
inference(rw,[status(thm)],[c_0_36,c_0_37]) ).
cnf(c_0_49,plain,
print(X1) != while(X2,X3),
inference(split_conjunct,[status(thm)],[c_0_38]) ).
fof(c_0_50,plain,
! [X359,X360,X361,X362] : run(X359,cons2(x(X361,X362),X360)) = run(store(X359,X361,eval(X359,X362)),X360),
inference(variable_rename,[status(thm)],[axiom_065]) ).
fof(c_0_51,plain,
! [X347,X348,X349] :
( eval(X347,X348) != eval(X347,X349)
| eval(X347,eq(X348,X349)) = suc(zero) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_060])]) ).
fof(c_0_52,plain,
! [X326,X327] : fetch(cons(X326,X327),zero) = X326,
inference(variable_rename,[status(thm)],[axiom_049]) ).
fof(c_0_53,plain,
! [X353,X354] : eval(X353,v(X354)) = fetch(X353,X354),
inference(variable_rename,[status(thm)],[axiom_062]) ).
cnf(c_0_54,plain,
head(cons(X1,X2)) = X1,
inference(split_conjunct,[status(thm)],[c_0_39]) ).
cnf(c_0_55,plain,
run(X1,cons2(print(X2),X3)) = cons(eval(X1,X2),run(X1,X3)),
inference(split_conjunct,[status(thm)],[c_0_40]) ).
cnf(c_0_56,plain,
run(X1,cons2(if(X2,cons2(X3,append(X4,cons2(while(X2,cons2(X3,X4)),nil2))),nil2),X5)) = run(X1,cons2(while(X2,cons2(X3,X4)),X5)),
inference(spm,[status(thm)],[c_0_41,c_0_42]) ).
cnf(c_0_57,plain,
run(X1,cons2(if(n(suc(X2)),X3,X4),X5)) = run(X1,append(X3,X5)),
inference(er,[status(thm)],[inference(spm,[status(thm)],[c_0_43,c_0_44])]) ).
cnf(c_0_58,plain,
map(X1,cons2(X2,X3)) = cons2(apply1(X1,X2),map(X1,X3)),
inference(split_conjunct,[status(thm)],[c_0_45]) ).
cnf(c_0_59,plain,
apply1(lam,while(X1,X2)) = while(X1,map(lam,X2)),
inference(rw,[status(thm)],[c_0_46,c_0_37]) ).
cnf(c_0_60,plain,
apply1(lam,print(X1)) = print(X1),
inference(sr,[status(thm)],[inference(er,[status(thm)],[inference(spm,[status(thm)],[c_0_47,c_0_48])]),c_0_49]) ).
cnf(c_0_61,plain,
run(X1,cons2(x(X2,X3),X4)) = run(store(X1,X2,eval(X1,X3)),X4),
inference(split_conjunct,[status(thm)],[c_0_50]) ).
cnf(c_0_62,plain,
( eval(X1,eq(X2,X3)) = suc(zero)
| eval(X1,X2) != eval(X1,X3) ),
inference(split_conjunct,[status(thm)],[c_0_51]) ).
fof(c_0_63,plain,
! [X328,X329,X330] : fetch(cons(X328,X329),suc(X330)) = fetch(X329,X330),
inference(variable_rename,[status(thm)],[axiom_050]) ).
fof(c_0_64,plain,
! [X341,X342,X343] : eval(X341,add(X342,X343)) = addNat(eval(X341,X342),eval(X341,X343)),
inference(variable_rename,[status(thm)],[axiom_058]) ).
cnf(c_0_65,plain,
fetch(cons(X1,X2),zero) = X1,
inference(split_conjunct,[status(thm)],[c_0_52]) ).
cnf(c_0_66,plain,
eval(X1,v(X2)) = fetch(X1,X2),
inference(split_conjunct,[status(thm)],[c_0_53]) ).
cnf(c_0_67,plain,
head(run(X1,cons2(print(X2),X3))) = eval(X1,X2),
inference(spm,[status(thm)],[c_0_54,c_0_55]) ).
cnf(c_0_68,plain,
run(X1,cons2(X2,append(append(X3,cons2(while(n(suc(X4)),cons2(X2,X3)),nil2)),X5))) = run(X1,cons2(while(n(suc(X4)),cons2(X2,X3)),X5)),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_56,c_0_57]),c_0_42]) ).
cnf(c_0_69,plain,
cons2(while(X1,map(lam,X2)),map(lam,X3)) = map(lam,cons2(while(X1,X2),X3)),
inference(spm,[status(thm)],[c_0_58,c_0_59]) ).
cnf(c_0_70,plain,
map(lam,cons2(print(X1),X2)) = cons2(print(X1),map(lam,X2)),
inference(spm,[status(thm)],[c_0_58,c_0_60]) ).
cnf(c_0_71,plain,
( run(X1,cons2(x(X2,eq(X3,X4)),X5)) = run(store(X1,X2,suc(zero)),X5)
| eval(X1,X3) != eval(X1,X4) ),
inference(spm,[status(thm)],[c_0_61,c_0_62]) ).
fof(c_0_72,plain,
! [X309] : store(nil,zero,X309) = cons(X309,nil),
inference(variable_rename,[status(thm)],[axiom_041]) ).
cnf(c_0_73,plain,
fetch(cons(X1,X2),suc(X3)) = fetch(X2,X3),
inference(split_conjunct,[status(thm)],[c_0_63]) ).
cnf(c_0_74,plain,
eval(X1,add(X2,X3)) = addNat(eval(X1,X2),eval(X1,X3)),
inference(split_conjunct,[status(thm)],[c_0_64]) ).
cnf(c_0_75,plain,
eval(cons(X1,X2),v(zero)) = X1,
inference(rw,[status(thm)],[c_0_65,c_0_66]) ).
fof(c_0_76,plain,
! [X325] : fetch(nil,X325) = zero,
inference(variable_rename,[status(thm)],[axiom_048]) ).
cnf(c_0_77,plain,
head(run(X1,cons2(while(n(suc(X2)),cons2(print(X3),X4)),X5))) = eval(X1,X3),
inference(spm,[status(thm)],[c_0_67,c_0_68]) ).
cnf(c_0_78,plain,
cons2(while(X1,cons2(print(X2),map(lam,X3))),map(lam,X4)) = map(lam,cons2(while(X1,cons2(print(X2),X3)),X4)),
inference(spm,[status(thm)],[c_0_69,c_0_70]) ).
cnf(c_0_79,plain,
( run(store(X1,X2,eval(X1,eq(X3,X4))),X5) = run(store(X1,X2,suc(zero)),X5)
| eval(X1,X3) != eval(X1,X4) ),
inference(spm,[status(thm)],[c_0_61,c_0_71]) ).
cnf(c_0_80,plain,
store(nil,zero,X1) = cons(X1,nil),
inference(split_conjunct,[status(thm)],[c_0_72]) ).
cnf(c_0_81,plain,
eval(cons(X1,X2),v(suc(X3))) = eval(X2,v(X3)),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_73,c_0_66]),c_0_66]) ).
cnf(c_0_82,plain,
addNat(eval(cons(X1,X2),X3),X1) = eval(cons(X1,X2),add(X3,v(zero))),
inference(spm,[status(thm)],[c_0_74,c_0_75]) ).
cnf(c_0_83,plain,
fetch(nil,X1) = zero,
inference(split_conjunct,[status(thm)],[c_0_76]) ).
fof(c_0_84,plain,
! [X331] : addNat(zero,X331) = X331,
inference(variable_rename,[status(thm)],[axiom_051]) ).
cnf(c_0_85,plain,
head(run(X1,map(lam,cons2(while(n(suc(X2)),cons2(print(X3),X4)),X5)))) = eval(X1,X3),
inference(spm,[status(thm)],[c_0_77,c_0_78]) ).
cnf(c_0_86,plain,
( run(cons(eval(nil,eq(X1,X2)),nil),X3) = run(cons(suc(zero),nil),X3)
| eval(nil,X1) != eval(nil,X2) ),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_79,c_0_80]),c_0_80]) ).
cnf(c_0_87,plain,
addNat(eval(X1,v(X2)),eval(cons(X3,X1),X4)) = eval(cons(X3,X1),add(v(suc(X2)),X4)),
inference(spm,[status(thm)],[c_0_74,c_0_81]) ).
cnf(c_0_88,plain,
addNat(X1,X1) = eval(cons(X1,X2),add(v(zero),v(zero))),
inference(spm,[status(thm)],[c_0_82,c_0_75]) ).
cnf(c_0_89,plain,
eval(nil,v(X1)) = zero,
inference(rw,[status(thm)],[c_0_83,c_0_66]) ).
cnf(c_0_90,plain,
addNat(zero,X1) = X1,
inference(split_conjunct,[status(thm)],[c_0_84]) ).
fof(c_0_91,plain,
! [X333,X334] : addNat(suc(X333),suc(X334)) = suc(addNat(X333,suc(X334))),
inference(variable_rename,[status(thm)],[axiom_053]) ).
cnf(c_0_92,plain,
( eval(cons(eval(nil,eq(X1,X2)),nil),X3) = eval(cons(suc(zero),nil),X3)
| eval(nil,X1) != eval(nil,X2) ),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_85,c_0_86]),c_0_85]) ).
cnf(c_0_93,plain,
addNat(eval(X1,v(X2)),addNat(X3,X3)) = eval(cons(X3,X1),add(v(suc(X2)),add(v(zero),v(zero)))),
inference(spm,[status(thm)],[c_0_87,c_0_88]) ).
cnf(c_0_94,plain,
eval(cons(X1,nil),add(v(suc(X2)),X3)) = eval(cons(X1,nil),X3),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_87,c_0_89]),c_0_90]) ).
cnf(c_0_95,plain,
addNat(suc(X1),suc(X2)) = suc(addNat(X1,suc(X2))),
inference(split_conjunct,[status(thm)],[c_0_91]) ).
cnf(c_0_96,plain,
( eval(X1,add(X2,eq(X3,X4))) = addNat(eval(X1,X2),suc(zero))
| eval(X1,X3) != eval(X1,X4) ),
inference(spm,[status(thm)],[c_0_74,c_0_62]) ).
cnf(c_0_97,plain,
( eval(X1,add(eq(X2,X3),X4)) = addNat(suc(zero),eval(X1,X4))
| eval(X1,X2) != eval(X1,X3) ),
inference(spm,[status(thm)],[c_0_74,c_0_62]) ).
cnf(c_0_98,plain,
( eval(nil,add(eq(X1,X2),eq(X1,X2))) = suc(suc(zero))
| eval(nil,X1) != eval(nil,X2) ),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_92,c_0_93]),c_0_89]),c_0_74]),c_0_90]),c_0_94]),c_0_88]),c_0_95]),c_0_90]) ).
cnf(c_0_99,plain,
( addNat(suc(zero),eval(X1,eq(X2,X3))) = addNat(eval(X1,eq(X4,X5)),suc(zero))
| eval(X1,X2) != eval(X1,X3)
| eval(X1,X4) != eval(X1,X5) ),
inference(spm,[status(thm)],[c_0_96,c_0_97]) ).
cnf(c_0_100,plain,
( addNat(eval(nil,eq(X1,X2)),suc(zero)) = suc(suc(zero))
| eval(nil,X1) != eval(nil,X2) ),
inference(spm,[status(thm)],[c_0_96,c_0_98]) ).
cnf(c_0_101,plain,
( addNat(suc(zero),eval(nil,eq(X1,X2))) = suc(suc(zero))
| eval(nil,X1) != eval(nil,X2)
| eval(nil,X3) != eval(nil,X4) ),
inference(spm,[status(thm)],[c_0_99,c_0_100]) ).
fof(c_0_102,plain,
! [X322,X323,X324] : opti2(if(X322,X323,X324)) = if(add(n(suc(zero)),X322),X324,X323),
inference(variable_rename,[status(thm)],[axiom_047]) ).
fof(c_0_103,negated_conjecture,
~ ? [X10] : run(nil,cons2(X10,nil2)) != run(nil,cons2(opti2(X10),nil2)),
inference(assume_negation,[status(cth)],[goal_074]) ).
cnf(c_0_104,plain,
eval(X1,add(n(X2),X3)) = addNat(X2,eval(X1,X3)),
inference(spm,[status(thm)],[c_0_74,c_0_44]) ).
cnf(c_0_105,plain,
( addNat(suc(zero),eval(nil,eq(X1,X1))) = suc(suc(zero))
| eval(nil,X2) != eval(nil,X3) ),
inference(er,[status(thm)],[c_0_101]) ).
cnf(c_0_106,plain,
opti2(if(X1,X2,X3)) = if(add(n(suc(zero)),X1),X3,X2),
inference(split_conjunct,[status(thm)],[c_0_102]) ).
fof(c_0_107,negated_conjecture,
! [X387] : run(nil,cons2(X387,nil2)) = run(nil,cons2(opti2(X387),nil2)),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_103])]) ).
fof(c_0_108,plain,
! [X378] : map(X378,nil2) = nil2,
inference(variable_rename,[status(thm)],[axiom_069]) ).
cnf(c_0_109,plain,
( run(X1,cons2(if(add(n(X2),X3),X4,X5),X6)) = run(X1,append(X4,X6))
| addNat(X2,eval(X1,X3)) != suc(X7) ),
inference(spm,[status(thm)],[c_0_43,c_0_104]) ).
cnf(c_0_110,plain,
addNat(suc(zero),eval(nil,eq(X1,X1))) = suc(suc(zero)),
inference(er,[status(thm)],[c_0_105]) ).
cnf(c_0_111,plain,
apply1(lam,if(X1,X2,X3)) = if(add(n(suc(zero)),X1),X3,X2),
inference(rw,[status(thm)],[c_0_106,c_0_37]) ).
cnf(c_0_112,negated_conjecture,
run(nil,cons2(X1,nil2)) = run(nil,cons2(opti2(X1),nil2)),
inference(split_conjunct,[status(thm)],[c_0_107]) ).
cnf(c_0_113,plain,
map(X1,nil2) = nil2,
inference(split_conjunct,[status(thm)],[c_0_108]) ).
cnf(c_0_114,plain,
( run(nil,cons2(apply1(lam,if(eq(X1,X1),X2,X3)),X4)) = run(nil,append(X3,X4))
| suc(suc(zero)) != suc(X5) ),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_109,c_0_110]),c_0_111]) ).
cnf(c_0_115,negated_conjecture,
run(nil,cons2(X1,nil2)) = run(nil,cons2(apply1(lam,X1),nil2)),
inference(rw,[status(thm)],[c_0_112,c_0_37]) ).
cnf(c_0_116,plain,
cons2(apply1(X1,X2),nil2) = map(X1,cons2(X2,nil2)),
inference(spm,[status(thm)],[c_0_58,c_0_113]) ).
fof(c_0_117,plain,
! [X301,X302] : nil != cons(X301,X302),
inference(variable_rename,[status(thm)],[axiom_037]) ).
cnf(c_0_118,plain,
( run(X1,cons2(if(eq(X2,X3),X4,X5),X6)) = run(X1,append(X4,X6))
| eval(X1,X2) != eval(X1,X3)
| suc(zero) != suc(X7) ),
inference(spm,[status(thm)],[c_0_43,c_0_62]) ).
cnf(c_0_119,plain,
run(nil,cons2(apply1(lam,if(eq(X1,X1),X2,X3)),X4)) = run(nil,append(X3,X4)),
inference(er,[status(thm)],[c_0_114]) ).
cnf(c_0_120,negated_conjecture,
run(nil,map(lam,cons2(X1,nil2))) = run(nil,cons2(X1,nil2)),
inference(rw,[status(thm)],[c_0_115,c_0_116]) ).
cnf(c_0_121,plain,
nil != cons(X1,X2),
inference(split_conjunct,[status(thm)],[c_0_117]) ).
cnf(c_0_122,plain,
( run(X1,cons2(if(eq(X2,X3),X4,X5),X6)) = run(X1,append(X4,X6))
| eval(X1,X2) != eval(X1,X3) ),
inference(er,[status(thm)],[c_0_118]) ).
cnf(c_0_123,plain,
run(nil,cons2(if(eq(X1,X1),X2,X3),nil2)) = run(nil,append(X3,nil2)),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_119,c_0_116]),c_0_120]) ).
fof(c_0_124,plain,
! [X382] : append(nil2,X382) = X382,
inference(variable_rename,[status(thm)],[axiom_071]) ).
fof(c_0_125,plain,
! [X355] : run(X355,nil2) = nil,
inference(variable_rename,[status(thm)],[axiom_063]) ).
cnf(c_0_126,plain,
run(X1,cons2(print(X2),X3)) != nil,
inference(spm,[status(thm)],[c_0_121,c_0_55]) ).
cnf(c_0_127,plain,
run(nil,append(X1,nil2)) = run(nil,append(X2,nil2)),
inference(spm,[status(thm)],[c_0_122,c_0_123]) ).
cnf(c_0_128,plain,
append(nil2,X1) = X1,
inference(split_conjunct,[status(thm)],[c_0_124]) ).
cnf(c_0_129,plain,
run(X1,nil2) = nil,
inference(split_conjunct,[status(thm)],[c_0_125]) ).
cnf(c_0_130,plain,
run(X1,cons2(while(n(suc(X2)),cons2(print(X3),X4)),X5)) != nil,
inference(spm,[status(thm)],[c_0_126,c_0_68]) ).
cnf(c_0_131,plain,
run(nil,append(X1,nil2)) = nil,
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_127,c_0_128]),c_0_129]) ).
cnf(c_0_132,plain,
append(map(X1,cons2(X2,nil2)),X3) = cons2(apply1(X1,X2),X3),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_42,c_0_116]),c_0_128]) ).
cnf(c_0_133,plain,
run(X1,map(lam,cons2(while(n(suc(X2)),cons2(print(X3),X4)),X5))) != nil,
inference(spm,[status(thm)],[c_0_130,c_0_78]) ).
cnf(c_0_134,plain,
run(nil,map(X1,cons2(X2,nil2))) = nil,
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_131,c_0_132]),c_0_116]) ).
cnf(c_0_135,plain,
$false,
inference(spm,[status(thm)],[c_0_133,c_0_134]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SWX197+1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.12 % Command : /export/starexec/sandbox2/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox2/solver/bin/cse --final-prover /export/starexec/sandbox2/solver/bin/eprover --proof-time %d --global-time-limit %d
% 0.16/0.32 % Computer : n022.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:21 EDT 2026
% 0.16/0.33 % CPUTime :
% 0.16/0.34 % start to proof: theBenchmark
% 273.62/108.32 % Version : CSE_E---1.7
% 273.62/108.32 % Problem : theBenchmark.p
% 273.62/108.32 % SZS status Theorem for theBenchmark.p
% 273.62/108.32 % SZS output start CNFRefutation
% See solution above
% 274.23/109.00 % Total time : 82.441s
%------------------------------------------------------------------------------