%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : SWX241_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 : n012.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 3.86s 3.03s
% Output : CNFRefutation 3.86s
% Verified :
% SZS Type : Refutation
% Derivation depth : 18
% Number of leaves : 16
% Syntax : Number of formulae : 73 ( 23 unt; 0 def)
% Number of atoms : 174 ( 36 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 183 ( 82 ~; 76 |; 8 &)
% ( 7 <=>; 10 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 6 ( 4 usr; 1 prp; 0-2 aty)
% Number of functors : 16 ( 16 usr; 6 con; 0-3 aty)
% Number of variables : 142 ( 14 sgn 66 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(goal_065,conjecture,
? [X10,X20] :
~ ( typeCorrect(X10)
=> ( elem(l,run(X20,X10))
<=> elem(l,run(cons(h,X20),X10)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goal_065) ).
fof(axiom_059,axiom,
! [X1,X8,X9] :
( eval(X1,X9)
=> run(X1,assign(X8,X9)) = cons(X8,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_059) ).
fof(axiom_050,axiom,
! [X1,X8,X17] :
( elem(X1,cons(X8,X17))
<=> ( X8 = X1
| elem(X1,X17) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_050) ).
fof(axiom_062,axiom,
! [X1,X15,X13,X14] :
( eval(X1,X15)
=> run(X1,ifThenElse(X15,X13,X14)) = run(X1,X13) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_062) ).
fof(axiom_052,axiom,
! [X1] : eval(X1,tT),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_052) ).
fof(axiom_045,axiom,
! [X12,X13,X14] :
( typeCorrect(ifThenElse(X12,X13,X14))
<=> ( typeCorrect(X13)
& typeCorrect(X14) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_045) ).
fof(axiom_063,axiom,
! [X1,X15,X13,X14] :
( ~ eval(X1,X15)
=> run(X1,ifThenElse(X15,X13,X14)) = run(X1,X14) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_063) ).
fof(axiom_054,axiom,
! [X1,X8] :
( eval(X1,var(X8))
<=> elem(X8,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_054) ).
fof(axiom_043,axiom,
! [X9,X2] :
( typeCorrect(assign(low(X2),X9))
<=> ~ secret(X9) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_043) ).
fof(axiom_047,axiom,
l = low(zero),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_047) ).
fof(axiom_037,axiom,
! [X1] :
( X1 != nand(proj1Nand(X1),proj2Nand(X1))
=> ( X1 != var(proj1Var(X1))
=> ~ secret(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_037) ).
fof(axiom_058,axiom,
! [X1] : run(X1,skip) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_058) ).
fof(axiom_012,axiom,
! [X1,X2] : nand(X1,X2) != tT,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_012) ).
fof(axiom_049,axiom,
! [X1] : ~ elem(X1,nil),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_049) ).
fof(axiom_041,axiom,
typeCorrect(skip),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_041) ).
fof(axiom_016,axiom,
! [X1] : tT != var(X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_016) ).
fof(c_0_16,negated_conjecture,
~ ? [X10,X20] :
~ ( typeCorrect(X10)
=> ( elem(l,run(X20,X10))
<=> elem(l,run(cons(h,X20),X10)) ) ),
inference(assume_negation,[status(cth)],[goal_065]) ).
fof(c_0_17,negated_conjecture,
! [X299,X300] :
( ( ~ elem(l,run(X300,X299))
| elem(l,run(cons(h,X300),X299))
| ~ typeCorrect(X299) )
& ( ~ elem(l,run(cons(h,X300),X299))
| elem(l,run(X300,X299))
| ~ typeCorrect(X299) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_16])])]) ).
fof(c_0_18,plain,
! [X279,X280,X281] :
( ~ eval(X279,X281)
| run(X279,assign(X280,X281)) = cons(X280,X279) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_059])]) ).
fof(c_0_19,plain,
! [X261,X262,X263] :
( ( ~ elem(X261,cons(X262,X263))
| X262 = X261
| elem(X261,X263) )
& ( X262 != X261
| elem(X261,cons(X262,X263)) )
& ( ~ elem(X261,X263)
| elem(X261,cons(X262,X263)) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_050])])]) ).
cnf(c_0_20,negated_conjecture,
( elem(l,run(X1,X2))
| ~ elem(l,run(cons(h,X1),X2))
| ~ typeCorrect(X2) ),
inference(split_conjunct,[status(thm)],[c_0_17]) ).
cnf(c_0_21,plain,
( run(X1,assign(X3,X2)) = cons(X3,X1)
| ~ eval(X1,X2) ),
inference(split_conjunct,[status(thm)],[c_0_18]) ).
cnf(c_0_22,plain,
( elem(X2,cons(X1,X3))
| X1 != X2 ),
inference(split_conjunct,[status(thm)],[c_0_19]) ).
cnf(c_0_23,negated_conjecture,
( elem(l,run(X1,assign(X2,X3)))
| ~ eval(cons(h,X1),X3)
| ~ elem(l,cons(X2,cons(h,X1)))
| ~ typeCorrect(assign(X2,X3)) ),
inference(spm,[status(thm)],[c_0_20,c_0_21]) ).
cnf(c_0_24,plain,
elem(X1,cons(X1,X2)),
inference(er,[status(thm)],[c_0_22]) ).
cnf(c_0_25,negated_conjecture,
( elem(l,run(X1,assign(l,X2)))
| ~ eval(cons(h,X1),X2)
| ~ typeCorrect(assign(l,X2)) ),
inference(spm,[status(thm)],[c_0_23,c_0_24]) ).
fof(c_0_26,plain,
! [X288,X289,X290,X291] :
( ~ eval(X288,X289)
| run(X288,ifThenElse(X289,X290,X291)) = run(X288,X290) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_062])]) ).
cnf(c_0_27,negated_conjecture,
( elem(l,run(X1,assign(l,X2)))
| ~ eval(cons(h,cons(h,X1)),X2)
| ~ typeCorrect(assign(l,X2)) ),
inference(spm,[status(thm)],[c_0_20,c_0_25]) ).
fof(c_0_28,plain,
! [X267] : eval(X267,tT),
inference(variable_rename,[status(thm)],[axiom_052]) ).
cnf(c_0_29,plain,
( run(X1,ifThenElse(X2,X3,X4)) = run(X1,X3)
| ~ eval(X1,X2) ),
inference(split_conjunct,[status(thm)],[c_0_26]) ).
cnf(c_0_30,negated_conjecture,
( elem(l,run(X1,assign(l,X2)))
| ~ eval(cons(h,cons(h,cons(h,X1))),X2)
| ~ typeCorrect(assign(l,X2)) ),
inference(spm,[status(thm)],[c_0_20,c_0_27]) ).
cnf(c_0_31,plain,
eval(X1,tT),
inference(split_conjunct,[status(thm)],[c_0_28]) ).
fof(c_0_32,plain,
! [X255,X256,X257] :
( ( typeCorrect(X256)
| ~ typeCorrect(ifThenElse(X255,X256,X257)) )
& ( typeCorrect(X257)
| ~ typeCorrect(ifThenElse(X255,X256,X257)) )
& ( ~ typeCorrect(X256)
| ~ typeCorrect(X257)
| typeCorrect(ifThenElse(X255,X256,X257)) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_045])])]) ).
fof(c_0_33,plain,
! [X1,X15,X13,X14] :
( ~ eval(X1,X15)
=> run(X1,ifThenElse(X15,X13,X14)) = run(X1,X14) ),
inference(fof_simplification,[status(thm)],[axiom_063]) ).
cnf(c_0_34,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_20,c_0_29]) ).
cnf(c_0_35,negated_conjecture,
( elem(l,run(X1,assign(l,tT)))
| ~ typeCorrect(assign(l,tT)) ),
inference(spm,[status(thm)],[c_0_30,c_0_31]) ).
cnf(c_0_36,plain,
( typeCorrect(X1)
| ~ typeCorrect(ifThenElse(X2,X1,X3)) ),
inference(split_conjunct,[status(thm)],[c_0_32]) ).
fof(c_0_37,plain,
! [X292,X293,X294,X295] :
( eval(X292,X293)
| run(X292,ifThenElse(X293,X294,X295)) = run(X292,X295) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_33])]) ).
cnf(c_0_38,negated_conjecture,
( elem(l,run(X1,ifThenElse(X2,assign(l,tT),X3)))
| ~ eval(cons(h,X1),X2)
| ~ typeCorrect(ifThenElse(X2,assign(l,tT),X3)) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_34,c_0_35]),c_0_36]) ).
cnf(c_0_39,plain,
( eval(X1,X2)
| run(X1,ifThenElse(X2,X3,X4)) = run(X1,X4) ),
inference(split_conjunct,[status(thm)],[c_0_37]) ).
cnf(c_0_40,negated_conjecture,
( eval(X1,X2)
| elem(l,run(X1,X3))
| ~ eval(cons(h,X1),X2)
| ~ typeCorrect(ifThenElse(X2,assign(l,tT),X3)) ),
inference(spm,[status(thm)],[c_0_38,c_0_39]) ).
cnf(c_0_41,plain,
( typeCorrect(ifThenElse(X3,X1,X2))
| ~ typeCorrect(X1)
| ~ typeCorrect(X2) ),
inference(split_conjunct,[status(thm)],[c_0_32]) ).
fof(c_0_42,plain,
! [X269,X270] :
( ( ~ eval(X269,var(X270))
| elem(X270,X269) )
& ( ~ elem(X270,X269)
| eval(X269,var(X270)) ) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[axiom_054])]) ).
fof(c_0_43,plain,
! [X9,X2] :
( typeCorrect(assign(low(X2),X9))
<=> ~ secret(X9) ),
inference(fof_simplification,[status(thm)],[axiom_043]) ).
cnf(c_0_44,negated_conjecture,
( eval(X1,X2)
| elem(l,run(X1,X3))
| ~ eval(cons(h,X1),X2)
| ~ typeCorrect(assign(l,tT))
| ~ typeCorrect(X3) ),
inference(spm,[status(thm)],[c_0_40,c_0_41]) ).
cnf(c_0_45,plain,
( eval(X2,var(X1))
| ~ elem(X1,X2) ),
inference(split_conjunct,[status(thm)],[c_0_42]) ).
fof(c_0_46,plain,
! [X251,X252] :
( ( ~ typeCorrect(assign(low(X252),X251))
| ~ secret(X251) )
& ( secret(X251)
| typeCorrect(assign(low(X252),X251)) ) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_43])]) ).
cnf(c_0_47,negated_conjecture,
( eval(X1,var(X2))
| elem(l,run(X1,X3))
| ~ elem(X2,cons(h,X1))
| ~ typeCorrect(assign(l,tT))
| ~ typeCorrect(X3) ),
inference(spm,[status(thm)],[c_0_44,c_0_45]) ).
cnf(c_0_48,plain,
( secret(X1)
| typeCorrect(assign(low(X2),X1)) ),
inference(split_conjunct,[status(thm)],[c_0_46]) ).
cnf(c_0_49,plain,
l = low(zero),
inference(split_conjunct,[status(thm)],[axiom_047]) ).
fof(c_0_50,plain,
! [X1] :
( X1 != nand(proj1Nand(X1),proj2Nand(X1))
=> ( X1 != var(proj1Var(X1))
=> ~ secret(X1) ) ),
inference(fof_simplification,[status(thm)],[axiom_037]) ).
cnf(c_0_51,negated_conjecture,
( eval(X1,var(h))
| elem(l,run(X1,X2))
| ~ typeCorrect(assign(l,tT))
| ~ typeCorrect(X2) ),
inference(spm,[status(thm)],[c_0_47,c_0_24]) ).
cnf(c_0_52,plain,
( typeCorrect(assign(l,X1))
| secret(X1) ),
inference(spm,[status(thm)],[c_0_48,c_0_49]) ).
fof(c_0_53,plain,
! [X278] : run(X278,skip) = X278,
inference(variable_rename,[status(thm)],[axiom_058]) ).
fof(c_0_54,plain,
! [X178,X179] : nand(X178,X179) != tT,
inference(variable_rename,[status(thm)],[axiom_012]) ).
fof(c_0_55,plain,
! [X244] :
( X244 = nand(proj1Nand(X244),proj2Nand(X244))
| X244 = var(proj1Var(X244))
| ~ secret(X244) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[c_0_50])]) ).
fof(c_0_56,plain,
! [X1] : ~ elem(X1,nil),
inference(fof_simplification,[status(thm)],[axiom_049]) ).
cnf(c_0_57,negated_conjecture,
( eval(X1,var(h))
| elem(l,run(X1,X2))
| secret(tT)
| ~ typeCorrect(X2) ),
inference(spm,[status(thm)],[c_0_51,c_0_52]) ).
cnf(c_0_58,plain,
typeCorrect(skip),
inference(split_conjunct,[status(thm)],[axiom_041]) ).
cnf(c_0_59,plain,
run(X1,skip) = X1,
inference(split_conjunct,[status(thm)],[c_0_53]) ).
fof(c_0_60,plain,
! [X185] : tT != var(X185),
inference(variable_rename,[status(thm)],[axiom_016]) ).
cnf(c_0_61,plain,
nand(X1,X2) != tT,
inference(split_conjunct,[status(thm)],[c_0_54]) ).
cnf(c_0_62,plain,
( X1 = nand(proj1Nand(X1),proj2Nand(X1))
| X1 = var(proj1Var(X1))
| ~ secret(X1) ),
inference(split_conjunct,[status(thm)],[c_0_55]) ).
fof(c_0_63,plain,
! [X260] : ~ elem(X260,nil),
inference(variable_rename,[status(thm)],[c_0_56]) ).
cnf(c_0_64,plain,
( elem(X2,X1)
| ~ eval(X1,var(X2)) ),
inference(split_conjunct,[status(thm)],[c_0_42]) ).
cnf(c_0_65,negated_conjecture,
( eval(X1,var(h))
| elem(l,X1)
| secret(tT) ),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_57,c_0_58]),c_0_59]) ).
cnf(c_0_66,plain,
tT != var(X1),
inference(split_conjunct,[status(thm)],[c_0_60]) ).
cnf(c_0_67,plain,
( var(proj1Var(X1)) = X1
| X1 != tT
| ~ secret(X1) ),
inference(spm,[status(thm)],[c_0_61,c_0_62]) ).
cnf(c_0_68,plain,
~ elem(X1,nil),
inference(split_conjunct,[status(thm)],[c_0_63]) ).
cnf(c_0_69,negated_conjecture,
( elem(l,X1)
| elem(h,X1)
| secret(tT) ),
inference(spm,[status(thm)],[c_0_64,c_0_65]) ).
cnf(c_0_70,plain,
( X1 != tT
| ~ secret(X1) ),
inference(spm,[status(thm)],[c_0_66,c_0_67]) ).
cnf(c_0_71,negated_conjecture,
secret(tT),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_68,c_0_69]),c_0_68]) ).
cnf(c_0_72,negated_conjecture,
$false,
inference(spm,[status(thm)],[c_0_70,c_0_71]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.07 % Problem : SWX241_1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.07 % 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.08/0.25 % Computer : n012.cluster.edu
% 0.08/0.25 % Model : x86_64 x86_64
% 0.08/0.25 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.25 % Memory : 8042.1875MB
% 0.08/0.25 % OS : Linux 3.10.0-693.el7.x86_64
% 0.08/0.25 % CPULimit : 300
% 0.08/0.25 % WCLimit : 300
% 0.08/0.25 % DateTime : Tue May 5 08:01:31 EDT 2026
% 0.08/0.25 % CPUTime :
% 0.08/0.26 % start to proof: theBenchmark
% 3.86/3.03 % Version : CSE_E---1.7
% 3.86/3.03 % Problem : theBenchmark.p
% 3.86/3.03 % SZS status Theorem for theBenchmark.p
% 3.86/3.03 % SZS output start CNFRefutation
% See solution above
% 3.86/3.04 % Total time : 2.364s
%------------------------------------------------------------------------------