%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : SWX240-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 : n005.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 : Unsatisfiable 18.79s 14.50s
% Output : CNFRefutation 18.79s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 33
% Syntax : Number of clauses : 93 ( 93 unt; 0 nHn; 19 RR)
% Number of literals : 93 ( 92 equ; 2 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 32 ( 32 usr; 8 con; 0-5 aty)
% Number of variables : 156 ( 48 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(axiom_059,axiom,
eq2(low(X1),high(X2)) = bfalse,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_059) ).
cnf(axiom_045,axiom,
eq3(var(X1),var(X2)) = eq2(X1,X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_045) ).
cnf(axiom_018,axiom,
h = high(zero),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_018) ).
cnf(axiom_036,axiom,
typeCorrect(seq(X1,X2)) = andb(typeCorrect(X1),typeCorrect(X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_036) ).
cnf(axiom_033,axiom,
typeCorrect(skip) = btrue,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_033) ).
cnf(axiom_023,axiom,
andb(btrue,X1) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_023) ).
cnf(axiom_037,axiom,
typeCorrect(ifThenElse(X1,X2,X3)) = andb(typeCorrect(X2),typeCorrect(X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_037) ).
cnf(axiom_020,axiom,
elem(X1,cons(X2,X3)) = orb(eq2(X2,X1),elem(X1,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_020) ).
cnf(axiom_028,axiom,
eval(X1,var(X2)) = elem(X2,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_028) ).
cnf(axiom_015,axiom,
l = low(zero),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_015) ).
cnf(axiom_058,axiom,
eq2(high(X1),low(X2)) = bfalse,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_058) ).
cnf(axiom_038,axiom,
prop(X1,X2) = impl(typeCorrect(X1),eq5(elem(l,run(X2,X1)),elem(l,run(cons(h,X2),X1)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_038) ).
cnf(axiom_035,axiom,
typeCorrect(assign(low(X1),X2)) = notb(secret(X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_035) ).
cnf(axiom_007,axiom,
orb(bfalse,X1) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_007) ).
cnf(axiom_012,axiom,
secret(fF) = bfalse,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_012) ).
cnf(axiom_014,axiom,
notb(bfalse) = btrue,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_014) ).
cnf(axiom_032,axiom,
run(X1,ifThenElse(X2,X3,X4)) = aux3(X1,X2,X3,X4,eval(X1,X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_032) ).
cnf(axiom_019,axiom,
elem(X1,nil) = bfalse,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_019) ).
cnf(axiom_022,axiom,
del(X1,cons(X2,X3)) = aux(X1,X2,X3,eq2(X1,X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_022) ).
cnf(axiom_084,axiom,
eq3(X1,X1) = btrue,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_084) ).
cnf(axiom_006,axiom,
orb(btrue,X1) = btrue,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_006) ).
cnf(axiom_016,axiom,
impl(btrue,X1) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_016) ).
cnf(axiom_005,axiom,
aux3(X1,X2,X3,X4,bfalse) = run(X1,X4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_005) ).
cnf(axiom_030,axiom,
run(X1,assign(X2,X3)) = aux2(X1,X2,X3,eval(X1,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_030) ).
cnf(axiom_027,axiom,
eval(X1,fF) = bfalse,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_027) ).
cnf(axiom_003,axiom,
aux2(X1,X2,X3,bfalse) = del(X2,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_003) ).
cnf(axiom,axiom,
aux(X1,X2,X3,btrue) = del(X1,X3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom) ).
cnf(axiom_004,axiom,
aux3(X1,X2,X3,X4,btrue) = run(X1,X3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_004) ).
cnf(axiom_021,axiom,
del(X1,nil) = nil,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_021) ).
cnf(axiom_029,axiom,
run(X1,skip) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_029) ).
cnf(axiom_041,axiom,
eq5(bfalse,btrue) = bfalse,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_041) ).
cnf(goal,negated_conjecture,
eq5(prop(X1,X2),bfalse) != btrue,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goal) ).
cnf(axiom_086,axiom,
eq5(X1,X1) = btrue,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_086) ).
cnf(c_0_33,axiom,
eq2(low(X1),high(X2)) = bfalse,
axiom_059 ).
cnf(c_0_34,axiom,
eq3(var(X1),var(X2)) = eq2(X1,X2),
axiom_045 ).
cnf(c_0_35,plain,
eq3(var(low(X1)),var(high(X2))) = bfalse,
inference(rw,[status(thm)],[c_0_33,c_0_34]) ).
cnf(c_0_36,axiom,
h = high(zero),
axiom_018 ).
cnf(c_0_37,axiom,
typeCorrect(seq(X1,X2)) = andb(typeCorrect(X1),typeCorrect(X2)),
axiom_036 ).
cnf(c_0_38,axiom,
typeCorrect(skip) = btrue,
axiom_033 ).
cnf(c_0_39,axiom,
andb(btrue,X1) = X1,
axiom_023 ).
cnf(c_0_40,axiom,
typeCorrect(ifThenElse(X1,X2,X3)) = andb(typeCorrect(X2),typeCorrect(X3)),
axiom_037 ).
cnf(c_0_41,axiom,
elem(X1,cons(X2,X3)) = orb(eq2(X2,X1),elem(X1,X3)),
axiom_020 ).
cnf(c_0_42,axiom,
eval(X1,var(X2)) = elem(X2,X1),
axiom_028 ).
cnf(c_0_43,plain,
eq3(var(low(X1)),var(h)) = bfalse,
inference(spm,[status(thm)],[c_0_35,c_0_36]) ).
cnf(c_0_44,axiom,
l = low(zero),
axiom_015 ).
cnf(c_0_45,axiom,
eq2(high(X1),low(X2)) = bfalse,
axiom_058 ).
cnf(c_0_46,axiom,
prop(X1,X2) = impl(typeCorrect(X1),eq5(elem(l,run(X2,X1)),elem(l,run(cons(h,X2),X1)))),
axiom_038 ).
cnf(c_0_47,plain,
typeCorrect(seq(skip,X1)) = typeCorrect(X1),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_37,c_0_38]),c_0_39]) ).
cnf(c_0_48,plain,
typeCorrect(ifThenElse(X1,X2,X3)) = typeCorrect(seq(X2,X3)),
inference(rw,[status(thm)],[c_0_40,c_0_37]) ).
cnf(c_0_49,axiom,
typeCorrect(assign(low(X1),X2)) = notb(secret(X2)),
axiom_035 ).
cnf(c_0_50,plain,
eval(cons(X2,X3),var(X1)) = orb(eq3(var(X2),var(X1)),eval(X3,var(X1))),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_41,c_0_42]),c_0_42]),c_0_34]) ).
cnf(c_0_51,plain,
eq3(var(l),var(h)) = bfalse,
inference(spm,[status(thm)],[c_0_43,c_0_44]) ).
cnf(c_0_52,axiom,
orb(bfalse,X1) = X1,
axiom_007 ).
cnf(c_0_53,plain,
eq3(var(high(X1)),var(low(X2))) = bfalse,
inference(rw,[status(thm)],[c_0_45,c_0_34]) ).
cnf(c_0_54,plain,
prop(X1,X2) = impl(typeCorrect(X1),eq5(eval(run(X2,X1),var(l)),eval(run(cons(h,X2),X1),var(l)))),
inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_46,c_0_42]),c_0_42]) ).
cnf(c_0_55,plain,
typeCorrect(ifThenElse(X1,skip,X2)) = typeCorrect(X2),
inference(spm,[status(thm)],[c_0_47,c_0_48]) ).
cnf(c_0_56,plain,
notb(secret(X1)) = typeCorrect(assign(l,X1)),
inference(spm,[status(thm)],[c_0_49,c_0_44]) ).
cnf(c_0_57,axiom,
secret(fF) = bfalse,
axiom_012 ).
cnf(c_0_58,axiom,
notb(bfalse) = btrue,
axiom_014 ).
cnf(c_0_59,axiom,
run(X1,ifThenElse(X2,X3,X4)) = aux3(X1,X2,X3,X4,eval(X1,X2)),
axiom_032 ).
cnf(c_0_60,plain,
eval(cons(l,X1),var(h)) = eval(X1,var(h)),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_50,c_0_51]),c_0_52]) ).
cnf(c_0_61,axiom,
elem(X1,nil) = bfalse,
axiom_019 ).
cnf(c_0_62,axiom,
del(X1,cons(X2,X3)) = aux(X1,X2,X3,eq2(X1,X2)),
axiom_022 ).
cnf(c_0_63,axiom,
eq3(X1,X1) = btrue,
axiom_084 ).
cnf(c_0_64,axiom,
orb(btrue,X1) = btrue,
axiom_006 ).
cnf(c_0_65,plain,
eq3(var(high(X1)),var(l)) = bfalse,
inference(spm,[status(thm)],[c_0_53,c_0_44]) ).
cnf(c_0_66,plain,
impl(typeCorrect(X1),eq5(eval(run(X2,ifThenElse(X3,skip,X1)),var(l)),eval(run(cons(h,X2),ifThenElse(X3,skip,X1)),var(l)))) = prop(ifThenElse(X3,skip,X1),X2),
inference(spm,[status(thm)],[c_0_54,c_0_55]) ).
cnf(c_0_67,plain,
typeCorrect(assign(l,fF)) = btrue,
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_56,c_0_57]),c_0_58]) ).
cnf(c_0_68,axiom,
impl(btrue,X1) = X1,
axiom_016 ).
cnf(c_0_69,plain,
aux3(cons(l,X1),var(h),X2,X3,eval(X1,var(h))) = run(cons(l,X1),ifThenElse(var(h),X2,X3)),
inference(spm,[status(thm)],[c_0_59,c_0_60]) ).
cnf(c_0_70,plain,
eval(nil,var(X1)) = bfalse,
inference(rw,[status(thm)],[c_0_61,c_0_42]) ).
cnf(c_0_71,axiom,
aux3(X1,X2,X3,X4,bfalse) = run(X1,X4),
axiom_005 ).
cnf(c_0_72,axiom,
run(X1,assign(X2,X3)) = aux2(X1,X2,X3,eval(X1,X3)),
axiom_030 ).
cnf(c_0_73,axiom,
eval(X1,fF) = bfalse,
axiom_027 ).
cnf(c_0_74,axiom,
aux2(X1,X2,X3,bfalse) = del(X2,X1),
axiom_003 ).
cnf(c_0_75,plain,
del(X1,cons(X2,X3)) = aux(X1,X2,X3,eq3(var(X1),var(X2))),
inference(rw,[status(thm)],[c_0_62,c_0_34]) ).
cnf(c_0_76,axiom,
aux(X1,X2,X3,btrue) = del(X1,X3),
axiom ).
cnf(c_0_77,plain,
eval(cons(X1,X2),var(X1)) = btrue,
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_50,c_0_63]),c_0_64]) ).
cnf(c_0_78,axiom,
aux3(X1,X2,X3,X4,btrue) = run(X1,X3),
axiom_004 ).
cnf(c_0_79,plain,
eq3(var(h),var(l)) = bfalse,
inference(spm,[status(thm)],[c_0_65,c_0_36]) ).
cnf(c_0_80,plain,
eq5(eval(run(X1,ifThenElse(X2,skip,assign(l,fF))),var(l)),eval(run(cons(h,X1),ifThenElse(X2,skip,assign(l,fF))),var(l))) = prop(ifThenElse(X2,skip,assign(l,fF)),X1),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_66,c_0_67]),c_0_68]) ).
cnf(c_0_81,plain,
run(cons(l,nil),ifThenElse(var(h),X1,X2)) = run(cons(l,nil),X2),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_69,c_0_70]),c_0_71]) ).
cnf(c_0_82,plain,
run(X1,assign(X2,fF)) = del(X2,X1),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_72,c_0_73]),c_0_74]) ).
cnf(c_0_83,plain,
del(X1,cons(X1,X2)) = del(X1,X2),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_75,c_0_63]),c_0_76]) ).
cnf(c_0_84,axiom,
del(X1,nil) = nil,
axiom_021 ).
cnf(c_0_85,plain,
run(cons(X1,X2),ifThenElse(var(X1),X3,X4)) = run(cons(X1,X2),X3),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_59,c_0_77]),c_0_78]) ).
cnf(c_0_86,axiom,
run(X1,skip) = X1,
axiom_029 ).
cnf(c_0_87,plain,
eval(cons(h,X1),var(l)) = eval(X1,var(l)),
inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_50,c_0_79]),c_0_52]) ).
cnf(c_0_88,axiom,
eq5(bfalse,btrue) = bfalse,
axiom_041 ).
cnf(c_0_89,negated_conjecture,
eq5(prop(X1,X2),bfalse) != btrue,
goal ).
cnf(c_0_90,plain,
prop(ifThenElse(var(h),skip,assign(l,fF)),cons(l,nil)) = bfalse,
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(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_80,c_0_81]),c_0_82]),c_0_83]),c_0_84]),c_0_70]),c_0_85]),c_0_86]),c_0_87]),c_0_77]),c_0_88]) ).
cnf(c_0_91,axiom,
eq5(X1,X1) = btrue,
axiom_086 ).
cnf(c_0_92,negated_conjecture,
$false,
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_89,c_0_90]),c_0_91])]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.21 % Problem : SWX240-1 : TPTP v9.3.0. Released v9.3.0.
% 0.03/0.21 % 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.12/0.45 % Computer : n005.cluster.edu
% 0.12/0.45 % Model : x86_64 x86_64
% 0.12/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.45 % Memory : 8042.1875MB
% 0.12/0.45 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.45 % CPULimit : 300
% 0.12/0.45 % WCLimit : 300
% 0.12/0.45 % DateTime : Tue May 5 08:01:45 EDT 2026
% 0.12/0.45 % CPUTime :
% 0.12/0.46 % start to proof: theBenchmark
% 18.79/14.50 % Version : CSE_E---1.7
% 18.79/14.50 % Problem : theBenchmark.p
% 18.79/14.50 % SZS status Unsatisfiable for theBenchmark.p
% 18.79/14.50 % SZS output start CNFRefutation
% See solution above
% 18.79/14.56 % Total time : 11.576s
%------------------------------------------------------------------------------