%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : SWX240_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 : n004.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:49 PM UTC 2026
% Result : Theorem 35.17s 20.72s
% Output : CNFRefutation 35.28s
% Verified :
% SZS Type : Refutation
% Derivation depth : 24
% Number of leaves : 25
% Syntax : Number of formulae : 129 ( 41 unt; 0 def)
% Number of atoms : 326 ( 67 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 359 ( 162 ~; 164 |; 11 &)
% ( 8 <=>; 14 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 4 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 6 ( 4 usr; 1 prp; 0-2 aty)
% Number of functors : 19 ( 19 usr; 6 con; 0-3 aty)
% Number of variables : 281 ( 30 sgn 107 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(goal_057,conjecture,
? [X10,X18] :
~ ( typeCorrect(X10)
=> ( elem(l,run(X18,X10))
<=> elem(l,run(cons(h,X18),X10)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goal_057) ).
fof(axiom_054,axiom,
! [X1,X10,X11] : run(X1,seq(X10,X11)) = run(run(X1,X10),X11),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_054) ).
fof(axiom_051,axiom,
! [X1] : run(X1,skip) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_051) ).
fof(axiom_055,axiom,
! [X1,X17,X13,X14] :
( eval(X1,X17)
=> run(X1,ifThenElse(X17,X13,X14)) = run(X1,X13) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_055) ).
fof(axiom_053,axiom,
! [X1,X8,X9] :
( ~ eval(X1,X9)
=> run(X1,assign(X8,X9)) = del(X8,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_053) ).
fof(axiom_038,axiom,
! [X10,X11] :
( typeCorrect(seq(X10,X11))
<=> ( typeCorrect(X10)
& typeCorrect(X11) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_038) ).
fof(axiom_049,axiom,
! [X1,X8,X16] :
( X1 = X8
=> del(X1,cons(X8,X16)) = del(X1,X16) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_049) ).
fof(axiom_036,axiom,
! [X9,X8] : typeCorrect(assign(high(X8),X9)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_036) ).
fof(axiom_039,axiom,
! [X12,X13,X14] :
( typeCorrect(ifThenElse(X12,X13,X14))
<=> ( typeCorrect(X13)
& typeCorrect(X14) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_039) ).
fof(axiom_041,axiom,
h = high(zero),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_041) ).
fof(axiom_042,axiom,
! [X1] : ~ elem(X1,nil),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_042) ).
fof(axiom_048,axiom,
! [X1] : del(X1,nil) = nil,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_048) ).
fof(axiom_052,axiom,
! [X1,X8,X9] :
( eval(X1,X9)
=> run(X1,assign(X8,X9)) = cons(X8,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_052) ).
fof(axiom_035,axiom,
typeCorrect(skip),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_035) ).
fof(axiom_045,axiom,
! [X1] : eval(X1,tT),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_045) ).
fof(axiom_050,axiom,
! [X1,X8,X16] :
( X1 != X8
=> del(X1,cons(X8,X16)) = cons(X8,del(X1,X16)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_050) ).
fof(axiom_043,axiom,
! [X1,X8,X15] :
( elem(X1,cons(X8,X15))
<=> ( X8 = X1
| elem(X1,X15) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_043) ).
fof(axiom_008,axiom,
! [X1,X2] : high(X1) != low(X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_008) ).
fof(axiom_056,axiom,
! [X1,X17,X13,X14] :
( ~ eval(X1,X17)
=> run(X1,ifThenElse(X17,X13,X14)) = run(X1,X14) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_056) ).
fof(axiom_040,axiom,
l = low(zero),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_040) ).
fof(axiom_037,axiom,
! [X9,X2] :
( typeCorrect(assign(low(X2),X9))
<=> ~ secret(X9) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_037) ).
fof(axiom_047,axiom,
! [X1,X8] :
( eval(X1,var(X8))
<=> elem(X8,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_047) ).
fof(axiom_031,axiom,
! [X1] :
( X1 != nand(proj1Nand(X1),proj2Nand(X1))
=> ( X1 != var(proj1Var(X1))
=> ~ secret(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_031) ).
fof(axiom_012,axiom,
! [X1,X2] : nand(X1,X2) != tT,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_012) ).
fof(axiom_016,axiom,
! [X1] : tT != var(X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_016) ).
fof(c_0_25,negated_conjecture,
~ ? [X10,X18] :
~ ( typeCorrect(X10)
=> ( elem(l,run(X18,X10))
<=> elem(l,run(cons(h,X18),X10)) ) ),
inference(assume_negation,[status(cth)],[goal_057]) ).
fof(c_0_26,negated_conjecture,
! [X249,X250] :
( ( ~ elem(l,run(X250,X249))
| elem(l,run(cons(h,X250),X249))
| ~ typeCorrect(X249) )
& ( ~ elem(l,run(cons(h,X250),X249))
| elem(l,run(X250,X249))
| ~ typeCorrect(X249) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_25])])]) ).
fof(c_0_27,plain,
! [X238,X239,X240] : run(X238,seq(X239,X240)) = run(run(X238,X239),X240),
inference(variable_rename,[status(thm)],[axiom_054]) ).
cnf(c_0_28,negated_conjecture,
( elem(l,run(X1,X2))
| ~ elem(l,run(cons(h,X1),X2))
| ~ typeCorrect(X2) ),
inference(split_conjunct,[status(thm)],[c_0_26]) ).
cnf(c_0_29,plain,
run(X1,seq(X2,X3)) = run(run(X1,X2),X3),
inference(split_conjunct,[status(thm)],[c_0_27]) ).
cnf(c_0_30,negated_conjecture,
( elem(l,run(run(X1,X2),X3))
| ~ elem(l,run(run(cons(h,X1),X2),X3))
| ~ typeCorrect(seq(X2,X3)) ),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_28,c_0_29]),c_0_29]) ).
fof(c_0_31,plain,
! [X231] : run(X231,skip) = X231,
inference(variable_rename,[status(thm)],[axiom_051]) ).
cnf(c_0_32,negated_conjecture,
( elem(l,run(run(run(X1,X2),X3),X4))
| ~ elem(l,run(run(run(cons(h,X1),X2),X3),X4))
| ~ typeCorrect(seq(seq(X2,X3),X4)) ),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_30,c_0_29]),c_0_29]) ).
cnf(c_0_33,plain,
run(X1,skip) = X1,
inference(split_conjunct,[status(thm)],[c_0_31]) ).
cnf(c_0_34,negated_conjecture,
( elem(l,run(run(X1,X2),X3))
| ~ elem(l,run(run(cons(h,X1),X2),X3))
| ~ typeCorrect(seq(seq(skip,X2),X3)) ),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_32,c_0_33]),c_0_33]) ).
fof(c_0_35,plain,
! [X241,X242,X243,X244] :
( ~ eval(X241,X242)
| run(X241,ifThenElse(X242,X243,X244)) = run(X241,X243) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_055])]) ).
fof(c_0_36,plain,
! [X1,X8,X9] :
( ~ eval(X1,X9)
=> run(X1,assign(X8,X9)) = del(X8,X1) ),
inference(fof_simplification,[status(thm)],[axiom_053]) ).
cnf(c_0_37,negated_conjecture,
( elem(l,run(X1,X2))
| ~ elem(l,run(cons(h,X1),X2))
| ~ typeCorrect(seq(seq(skip,skip),X2)) ),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_34,c_0_33]),c_0_33]) ).
cnf(c_0_38,plain,
( run(X1,ifThenElse(X2,X3,X4)) = run(X1,X3)
| ~ eval(X1,X2) ),
inference(split_conjunct,[status(thm)],[c_0_35]) ).
fof(c_0_39,plain,
! [X208,X209] :
( ( typeCorrect(X208)
| ~ typeCorrect(seq(X208,X209)) )
& ( typeCorrect(X209)
| ~ typeCorrect(seq(X208,X209)) )
& ( ~ typeCorrect(X208)
| ~ typeCorrect(X209)
| typeCorrect(seq(X208,X209)) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_038])])]) ).
fof(c_0_40,plain,
! [X235,X236,X237] :
( eval(X235,X237)
| run(X235,assign(X236,X237)) = del(X236,X235) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_36])]) ).
fof(c_0_41,plain,
! [X225,X226,X227] :
( X225 != X226
| del(X225,cons(X226,X227)) = del(X225,X227) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_049])]) ).
fof(c_0_42,plain,
! [X204,X205] : typeCorrect(assign(high(X205),X204)),
inference(variable_rename,[status(thm)],[axiom_036]) ).
cnf(c_0_43,negated_conjecture,
( elem(l,run(X1,X2))
| ~ eval(X1,X3)
| ~ elem(l,run(cons(h,X1),ifThenElse(X3,X2,X4)))
| ~ typeCorrect(seq(seq(skip,skip),ifThenElse(X3,X2,X4))) ),
inference(spm,[status(thm)],[c_0_37,c_0_38]) ).
cnf(c_0_44,negated_conjecture,
( elem(l,run(cons(h,X1),X2))
| ~ elem(l,run(X1,X2))
| ~ typeCorrect(X2) ),
inference(split_conjunct,[status(thm)],[c_0_26]) ).
cnf(c_0_45,plain,
( typeCorrect(X1)
| ~ typeCorrect(seq(X2,X1)) ),
inference(split_conjunct,[status(thm)],[c_0_39]) ).
cnf(c_0_46,negated_conjecture,
( elem(l,run(X1,ifThenElse(X2,X3,X4)))
| ~ eval(cons(h,X1),X2)
| ~ elem(l,run(cons(h,X1),X3))
| ~ typeCorrect(ifThenElse(X2,X3,X4)) ),
inference(spm,[status(thm)],[c_0_28,c_0_38]) ).
fof(c_0_47,plain,
! [X210,X211,X212] :
( ( typeCorrect(X211)
| ~ typeCorrect(ifThenElse(X210,X211,X212)) )
& ( typeCorrect(X212)
| ~ typeCorrect(ifThenElse(X210,X211,X212)) )
& ( ~ typeCorrect(X211)
| ~ typeCorrect(X212)
| typeCorrect(ifThenElse(X210,X211,X212)) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_039])])]) ).
cnf(c_0_48,plain,
( eval(X1,X2)
| run(X1,assign(X3,X2)) = del(X3,X1) ),
inference(split_conjunct,[status(thm)],[c_0_40]) ).
cnf(c_0_49,plain,
( del(X1,cons(X2,X3)) = del(X1,X3)
| X1 != X2 ),
inference(split_conjunct,[status(thm)],[c_0_41]) ).
cnf(c_0_50,plain,
typeCorrect(assign(high(X1),X2)),
inference(split_conjunct,[status(thm)],[c_0_42]) ).
cnf(c_0_51,plain,
h = high(zero),
inference(split_conjunct,[status(thm)],[axiom_041]) ).
fof(c_0_52,plain,
! [X1] : ~ elem(X1,nil),
inference(fof_simplification,[status(thm)],[axiom_042]) ).
cnf(c_0_53,negated_conjecture,
( elem(l,run(X1,X2))
| ~ eval(X1,X3)
| ~ elem(l,run(X1,ifThenElse(X3,X2,X4)))
| ~ typeCorrect(seq(seq(skip,skip),ifThenElse(X3,X2,X4))) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_43,c_0_44]),c_0_45]) ).
cnf(c_0_54,plain,
( typeCorrect(seq(X1,X2))
| ~ typeCorrect(X1)
| ~ typeCorrect(X2) ),
inference(split_conjunct,[status(thm)],[c_0_39]) ).
cnf(c_0_55,negated_conjecture,
( elem(l,run(X1,ifThenElse(X2,X3,X4)))
| ~ eval(cons(h,cons(h,X1)),X2)
| ~ elem(l,run(cons(h,cons(h,X1)),X3))
| ~ typeCorrect(ifThenElse(X2,X3,X4)) ),
inference(spm,[status(thm)],[c_0_28,c_0_46]) ).
cnf(c_0_56,plain,
( typeCorrect(X1)
| ~ typeCorrect(ifThenElse(X2,X1,X3)) ),
inference(split_conjunct,[status(thm)],[c_0_47]) ).
cnf(c_0_57,negated_conjecture,
( eval(cons(h,X1),X2)
| elem(l,del(X3,cons(h,X1)))
| ~ elem(l,run(X1,assign(X3,X2)))
| ~ typeCorrect(assign(X3,X2)) ),
inference(spm,[status(thm)],[c_0_44,c_0_48]) ).
cnf(c_0_58,plain,
del(X1,cons(X1,X2)) = del(X1,X2),
inference(er,[status(thm)],[c_0_49]) ).
cnf(c_0_59,plain,
typeCorrect(assign(h,X1)),
inference(spm,[status(thm)],[c_0_50,c_0_51]) ).
fof(c_0_60,plain,
! [X224] : del(X224,nil) = nil,
inference(variable_rename,[status(thm)],[axiom_048]) ).
fof(c_0_61,plain,
! [X213] : ~ elem(X213,nil),
inference(variable_rename,[status(thm)],[c_0_52]) ).
cnf(c_0_62,negated_conjecture,
( elem(l,run(X1,X2))
| ~ eval(X1,X3)
| ~ elem(l,run(X1,ifThenElse(X3,X2,X4)))
| ~ typeCorrect(seq(skip,skip))
| ~ typeCorrect(ifThenElse(X3,X2,X4)) ),
inference(spm,[status(thm)],[c_0_53,c_0_54]) ).
cnf(c_0_63,negated_conjecture,
( elem(l,run(X1,ifThenElse(X2,X3,X4)))
| ~ eval(cons(h,cons(h,X1)),X2)
| ~ elem(l,run(cons(h,X1),X3))
| ~ typeCorrect(ifThenElse(X2,X3,X4)) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_55,c_0_44]),c_0_56]) ).
cnf(c_0_64,negated_conjecture,
( eval(cons(h,X1),X2)
| elem(l,run(X1,assign(X3,X2)))
| ~ elem(l,del(X3,cons(h,X1)))
| ~ typeCorrect(assign(X3,X2)) ),
inference(spm,[status(thm)],[c_0_28,c_0_48]) ).
cnf(c_0_65,negated_conjecture,
( eval(cons(h,X1),X2)
| elem(l,del(h,X1))
| ~ elem(l,run(X1,assign(h,X2))) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_57,c_0_58]),c_0_59])]) ).
cnf(c_0_66,plain,
del(X1,nil) = nil,
inference(split_conjunct,[status(thm)],[c_0_60]) ).
cnf(c_0_67,plain,
~ elem(X1,nil),
inference(split_conjunct,[status(thm)],[c_0_61]) ).
fof(c_0_68,plain,
! [X232,X233,X234] :
( ~ eval(X232,X234)
| run(X232,assign(X233,X234)) = cons(X233,X232) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_052])]) ).
cnf(c_0_69,negated_conjecture,
( elem(l,run(X1,X2))
| ~ eval(cons(h,cons(h,X1)),X3)
| ~ eval(X1,X3)
| ~ elem(l,run(cons(h,X1),X2))
| ~ typeCorrect(seq(skip,skip))
| ~ typeCorrect(ifThenElse(X3,X2,X4)) ),
inference(spm,[status(thm)],[c_0_62,c_0_63]) ).
cnf(c_0_70,plain,
typeCorrect(skip),
inference(split_conjunct,[status(thm)],[axiom_035]) ).
fof(c_0_71,plain,
! [X220] : eval(X220,tT),
inference(variable_rename,[status(thm)],[axiom_045]) ).
fof(c_0_72,plain,
! [X228,X229,X230] :
( X228 = X229
| del(X228,cons(X229,X230)) = cons(X229,del(X228,X230)) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_050])]) ).
cnf(c_0_73,negated_conjecture,
( eval(cons(h,X1),X2)
| eval(X1,X2)
| elem(l,del(X3,X1))
| ~ elem(l,del(X3,cons(h,X1)))
| ~ typeCorrect(assign(X3,X2)) ),
inference(spm,[status(thm)],[c_0_64,c_0_48]) ).
cnf(c_0_74,negated_conjecture,
( eval(cons(h,nil),X1)
| ~ elem(l,run(nil,assign(h,X1))) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_65,c_0_66]),c_0_67]) ).
cnf(c_0_75,plain,
( run(X1,assign(X3,X2)) = cons(X3,X1)
| ~ eval(X1,X2) ),
inference(split_conjunct,[status(thm)],[c_0_68]) ).
cnf(c_0_76,negated_conjecture,
( elem(l,run(X1,X2))
| ~ eval(cons(h,cons(h,X1)),X3)
| ~ eval(X1,X3)
| ~ elem(l,run(cons(h,X1),X2))
| ~ typeCorrect(ifThenElse(X3,X2,X4)) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_69,c_0_54]),c_0_70])]) ).
cnf(c_0_77,plain,
eval(X1,tT),
inference(split_conjunct,[status(thm)],[c_0_71]) ).
fof(c_0_78,plain,
! [X214,X215,X216] :
( ( ~ elem(X214,cons(X215,X216))
| X215 = X214
| elem(X214,X216) )
& ( X215 != X214
| elem(X214,cons(X215,X216)) )
& ( ~ elem(X214,X216)
| elem(X214,cons(X215,X216)) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_043])])]) ).
cnf(c_0_79,plain,
( X1 = X2
| del(X1,cons(X2,X3)) = cons(X2,del(X1,X3)) ),
inference(split_conjunct,[status(thm)],[c_0_72]) ).
cnf(c_0_80,negated_conjecture,
( eval(cons(h,nil),X1)
| eval(nil,X1)
| ~ elem(l,del(X2,cons(h,nil)))
| ~ typeCorrect(assign(X2,X1)) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_73,c_0_66]),c_0_67]) ).
cnf(c_0_81,negated_conjecture,
( eval(cons(h,nil),X1)
| ~ eval(nil,X1)
| ~ elem(l,cons(h,nil)) ),
inference(spm,[status(thm)],[c_0_74,c_0_75]) ).
fof(c_0_82,plain,
! [X145,X146] : high(X145) != low(X146),
inference(variable_rename,[status(thm)],[axiom_008]) ).
fof(c_0_83,plain,
! [X1,X17,X13,X14] :
( ~ eval(X1,X17)
=> run(X1,ifThenElse(X17,X13,X14)) = run(X1,X14) ),
inference(fof_simplification,[status(thm)],[axiom_056]) ).
cnf(c_0_84,negated_conjecture,
( elem(l,run(X1,X2))
| ~ elem(l,run(cons(h,X1),X2))
| ~ typeCorrect(ifThenElse(tT,X2,X3)) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_76,c_0_77]),c_0_77])]) ).
cnf(c_0_85,plain,
( elem(X2,cons(X1,X3))
| X1 != X2 ),
inference(split_conjunct,[status(thm)],[c_0_78]) ).
cnf(c_0_86,negated_conjecture,
( X1 = h
| eval(cons(h,X2),X3)
| elem(l,cons(h,del(X1,X2)))
| ~ elem(l,run(X2,assign(X1,X3)))
| ~ typeCorrect(assign(X1,X3)) ),
inference(spm,[status(thm)],[c_0_57,c_0_79]) ).
cnf(c_0_87,negated_conjecture,
( X1 = h
| eval(cons(h,nil),X2)
| ~ elem(l,cons(h,nil))
| ~ typeCorrect(assign(X1,X2)) ),
inference(csr,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_80,c_0_79]),c_0_66]),c_0_81]) ).
cnf(c_0_88,plain,
high(X1) != low(X2),
inference(split_conjunct,[status(thm)],[c_0_82]) ).
fof(c_0_89,plain,
! [X245,X246,X247,X248] :
( eval(X245,X246)
| run(X245,ifThenElse(X246,X247,X248)) = run(X245,X248) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_83])]) ).
cnf(c_0_90,negated_conjecture,
( elem(l,run(X1,assign(X2,X3)))
| ~ eval(cons(h,X1),X3)
| ~ elem(l,cons(X2,cons(h,X1)))
| ~ typeCorrect(ifThenElse(tT,assign(X2,X3),X4)) ),
inference(spm,[status(thm)],[c_0_84,c_0_75]) ).
cnf(c_0_91,plain,
elem(X1,cons(X1,X2)),
inference(er,[status(thm)],[c_0_85]) ).
cnf(c_0_92,negated_conjecture,
( X1 = h
| eval(cons(h,nil),X2)
| ~ elem(l,run(nil,assign(X1,X2)))
| ~ typeCorrect(assign(X1,X2)) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_86,c_0_66]),c_0_87]) ).
cnf(c_0_93,plain,
low(X1) != h,
inference(spm,[status(thm)],[c_0_88,c_0_51]) ).
cnf(c_0_94,plain,
l = low(zero),
inference(split_conjunct,[status(thm)],[axiom_040]) ).
fof(c_0_95,plain,
! [X9,X2] :
( typeCorrect(assign(low(X2),X9))
<=> ~ secret(X9) ),
inference(fof_simplification,[status(thm)],[axiom_037]) ).
cnf(c_0_96,plain,
( eval(X1,X2)
| run(X1,ifThenElse(X2,X3,X4)) = run(X1,X4) ),
inference(split_conjunct,[status(thm)],[c_0_89]) ).
cnf(c_0_97,negated_conjecture,
( elem(l,run(X1,assign(l,X2)))
| ~ eval(cons(h,X1),X2)
| ~ typeCorrect(ifThenElse(tT,assign(l,X2),X3)) ),
inference(spm,[status(thm)],[c_0_90,c_0_91]) ).
cnf(c_0_98,plain,
( typeCorrect(ifThenElse(X3,X1,X2))
| ~ typeCorrect(X1)
| ~ typeCorrect(X2) ),
inference(split_conjunct,[status(thm)],[c_0_47]) ).
cnf(c_0_99,negated_conjecture,
( X1 = h
| eval(cons(h,nil),X2)
| ~ eval(nil,X2)
| ~ elem(l,cons(X1,nil))
| ~ typeCorrect(assign(X1,X2)) ),
inference(spm,[status(thm)],[c_0_92,c_0_75]) ).
cnf(c_0_100,plain,
h != l,
inference(spm,[status(thm)],[c_0_93,c_0_94]) ).
fof(c_0_101,plain,
! [X206,X207] :
( ( ~ typeCorrect(assign(low(X207),X206))
| ~ secret(X206) )
& ( secret(X206)
| typeCorrect(assign(low(X207),X206)) ) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_95])]) ).
cnf(c_0_102,negated_conjecture,
( eval(X1,X2)
| elem(l,run(X1,X3))
| ~ eval(cons(h,X1),X2)
| ~ elem(l,run(cons(h,X1),X4))
| ~ typeCorrect(ifThenElse(X2,X4,X3)) ),
inference(spm,[status(thm)],[c_0_46,c_0_96]) ).
cnf(c_0_103,negated_conjecture,
( elem(l,run(X1,assign(l,X2)))
| ~ eval(cons(h,X1),X2)
| ~ typeCorrect(assign(l,X2))
| ~ typeCorrect(X3) ),
inference(spm,[status(thm)],[c_0_97,c_0_98]) ).
cnf(c_0_104,negated_conjecture,
( eval(cons(h,nil),X1)
| ~ eval(nil,X1)
| ~ typeCorrect(assign(l,X1)) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_99,c_0_91]),c_0_100]) ).
cnf(c_0_105,plain,
( secret(X1)
| typeCorrect(assign(low(X2),X1)) ),
inference(split_conjunct,[status(thm)],[c_0_101]) ).
cnf(c_0_106,negated_conjecture,
( eval(X1,X2)
| elem(l,run(X1,X3))
| ~ eval(cons(h,X1),X2)
| ~ elem(l,run(X1,X4))
| ~ typeCorrect(ifThenElse(X2,X4,X3)) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_102,c_0_44]),c_0_56]) ).
fof(c_0_107,plain,
! [X222,X223] :
( ( ~ eval(X222,var(X223))
| elem(X223,X222) )
& ( ~ elem(X223,X222)
| eval(X222,var(X223)) ) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_047])]) ).
cnf(c_0_108,negated_conjecture,
( elem(l,run(nil,assign(l,X1)))
| ~ eval(nil,X1)
| ~ typeCorrect(assign(l,X1))
| ~ typeCorrect(X2) ),
inference(spm,[status(thm)],[c_0_103,c_0_104]) ).
cnf(c_0_109,plain,
( typeCorrect(assign(l,X1))
| secret(X1) ),
inference(spm,[status(thm)],[c_0_105,c_0_94]) ).
cnf(c_0_110,negated_conjecture,
( eval(X1,X2)
| elem(l,X1)
| ~ eval(cons(h,X1),X2)
| ~ elem(l,run(X1,X3))
| ~ typeCorrect(ifThenElse(X2,X3,skip)) ),
inference(spm,[status(thm)],[c_0_106,c_0_33]) ).
cnf(c_0_111,plain,
( eval(X2,var(X1))
| ~ elem(X1,X2) ),
inference(split_conjunct,[status(thm)],[c_0_107]) ).
cnf(c_0_112,negated_conjecture,
( elem(l,run(nil,assign(l,X1)))
| secret(X1)
| ~ eval(nil,X1)
| ~ typeCorrect(X2) ),
inference(spm,[status(thm)],[c_0_108,c_0_109]) ).
cnf(c_0_113,negated_conjecture,
( eval(X1,var(X2))
| elem(l,X1)
| ~ elem(l,run(X1,X3))
| ~ elem(X2,cons(h,X1))
| ~ typeCorrect(ifThenElse(var(X2),X3,skip)) ),
inference(spm,[status(thm)],[c_0_110,c_0_111]) ).
cnf(c_0_114,negated_conjecture,
( elem(l,run(nil,assign(l,tT)))
| secret(tT)
| ~ typeCorrect(X1) ),
inference(spm,[status(thm)],[c_0_112,c_0_77]) ).
cnf(c_0_115,negated_conjecture,
( eval(X1,var(X2))
| elem(l,X1)
| ~ elem(l,run(X1,X3))
| ~ elem(X2,cons(h,X1))
| ~ typeCorrect(X3) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_113,c_0_98]),c_0_70])]) ).
cnf(c_0_116,negated_conjecture,
( elem(l,run(nil,assign(l,tT)))
| secret(tT) ),
inference(spm,[status(thm)],[c_0_114,c_0_70]) ).
fof(c_0_117,plain,
! [X1] :
( X1 != nand(proj1Nand(X1),proj2Nand(X1))
=> ( X1 != var(proj1Var(X1))
=> ~ secret(X1) ) ),
inference(fof_simplification,[status(thm)],[axiom_031]) ).
cnf(c_0_118,negated_conjecture,
( eval(nil,var(X1))
| secret(tT)
| ~ elem(X1,cons(h,nil)) ),
inference(csr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_115,c_0_116]),c_0_67]),c_0_109]) ).
fof(c_0_119,plain,
! [X199] :
( X199 = nand(proj1Nand(X199),proj2Nand(X199))
| X199 = var(proj1Var(X199))
| ~ secret(X199) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_117])]) ).
cnf(c_0_120,plain,
( elem(X2,X1)
| ~ eval(X1,var(X2)) ),
inference(split_conjunct,[status(thm)],[c_0_107]) ).
cnf(c_0_121,negated_conjecture,
( eval(nil,var(h))
| secret(tT) ),
inference(spm,[status(thm)],[c_0_118,c_0_91]) ).
fof(c_0_122,plain,
! [X152,X153] : nand(X152,X153) != tT,
inference(variable_rename,[status(thm)],[axiom_012]) ).
fof(c_0_123,plain,
! [X159] : tT != var(X159),
inference(variable_rename,[status(thm)],[axiom_016]) ).
cnf(c_0_124,plain,
( X1 = nand(proj1Nand(X1),proj2Nand(X1))
| X1 = var(proj1Var(X1))
| ~ secret(X1) ),
inference(split_conjunct,[status(thm)],[c_0_119]) ).
cnf(c_0_125,negated_conjecture,
secret(tT),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_120,c_0_121]),c_0_67]) ).
cnf(c_0_126,plain,
nand(X1,X2) != tT,
inference(split_conjunct,[status(thm)],[c_0_122]) ).
cnf(c_0_127,plain,
tT != var(X1),
inference(split_conjunct,[status(thm)],[c_0_123]) ).
cnf(c_0_128,negated_conjecture,
$false,
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_124,c_0_125]),c_0_126]),c_0_127]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SWX240_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.15/0.33 % Computer : n004.cluster.edu
% 0.15/0.33 % Model : x86_64 x86_64
% 0.15/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.33 % Memory : 8042.1875MB
% 0.15/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.33 % CPULimit : 300
% 0.15/0.33 % WCLimit : 300
% 0.15/0.33 % DateTime : Tue May 5 08:01:47 EDT 2026
% 0.15/0.34 % CPUTime :
% 0.15/0.35 % start to proof: theBenchmark
% 35.17/20.72 % Version : CSE_E---1.7
% 35.17/20.72 % Problem : theBenchmark.p
% 35.17/20.72 % SZS status Theorem for theBenchmark.p
% 35.17/20.72 % SZS output start CNFRefutation
% See solution above
% 35.28/20.85 % Total time : 15.398s
%------------------------------------------------------------------------------