%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SWX240-1 : TPTP v9.3.1. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n018.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sun Sep 27 09:16:26 AM UTC 2026
% Result : Unsatisfiable 8.44s 1.58s
% Output : CNFRefutation 8.44s
% Verified :
% SZS Type : Refutation
% Derivation depth : 29
% Number of leaves : 33
% Syntax : Number of formulae : 134 ( 134 unt; 0 def)
% Number of atoms : 134 ( 133 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 21 ( 21 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 2 avg)
% Maximal term depth : 8 ( 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 : 225 ( 34 sgn 56 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(axiom,axiom,
! [VAR_0,VAR_1,VAR_2] : aux(VAR_0,VAR_1,VAR_2,btrue) = del(VAR_0,VAR_2),
file('theBenchmark.p',axiom) ).
cnf(c_1,plain,
aux(A,B,C,btrue) = del(A,C),
inference(clausify,[status(thm)],[axiom]) ).
fof(axiom_003,axiom,
! [VAR_0,VAR_1,VAR_2] : aux2(VAR_0,VAR_1,VAR_2,bfalse) = del(VAR_1,VAR_0),
file('theBenchmark.p',axiom_003) ).
cnf(c_4,plain,
aux2(A,B,C,bfalse) = del(B,A),
inference(clausify,[status(thm)],[axiom_003]) ).
fof(axiom_004,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] : aux3(VAR_0,VAR_1,VAR_2,VAR_3,btrue) = run(VAR_0,VAR_2),
file('theBenchmark.p',axiom_004) ).
cnf(c_5,plain,
aux3(A,B,C,D,btrue) = run(A,C),
inference(clausify,[status(thm)],[axiom_004]) ).
fof(axiom_005,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] : aux3(VAR_0,VAR_1,VAR_2,VAR_3,bfalse) = run(VAR_0,VAR_3),
file('theBenchmark.p',axiom_005) ).
cnf(c_6,plain,
aux3(A,B,C,D,bfalse) = run(A,D),
inference(clausify,[status(thm)],[axiom_005]) ).
fof(axiom_006,axiom,
! [VAR_0] : orb(btrue,VAR_0) = btrue,
file('theBenchmark.p',axiom_006) ).
cnf(c_7,plain,
orb(btrue,A) = btrue,
inference(clausify,[status(thm)],[axiom_006]) ).
fof(axiom_007,axiom,
! [VAR_0] : orb(bfalse,VAR_0) = VAR_0,
file('theBenchmark.p',axiom_007) ).
cnf(c_8,plain,
orb(bfalse,A) = A,
inference(clausify,[status(thm)],[axiom_007]) ).
fof(axiom_012,axiom,
secret(fF) = bfalse,
file('theBenchmark.p',axiom_012) ).
cnf(c_14,plain,
secret(fF) = bfalse,
inference(clausify,[status(thm)],[axiom_012]) ).
fof(axiom_014,axiom,
notb(bfalse) = btrue,
file('theBenchmark.p',axiom_014) ).
cnf(c_16,plain,
notb(bfalse) = btrue,
inference(clausify,[status(thm)],[axiom_014]) ).
fof(axiom_015,axiom,
l = low(zero),
file('theBenchmark.p',axiom_015) ).
cnf(c_17,plain,
l = low(zero),
inference(clausify,[status(thm)],[axiom_015]) ).
cnf(c_18,plain,
low(zero) = l,
inference(copy,[status(thm)],[c_17]) ).
fof(axiom_016,axiom,
! [VAR_0] : impl(btrue,VAR_0) = VAR_0,
file('theBenchmark.p',axiom_016) ).
cnf(c_19,plain,
impl(btrue,A) = A,
inference(clausify,[status(thm)],[axiom_016]) ).
fof(axiom_018,axiom,
h = high(zero),
file('theBenchmark.p',axiom_018) ).
cnf(c_21,plain,
h = high(zero),
inference(clausify,[status(thm)],[axiom_018]) ).
cnf(c_22,plain,
high(zero) = h,
inference(copy,[status(thm)],[c_21]) ).
fof(axiom_019,axiom,
! [VAR_0] : elem(VAR_0,nil) = bfalse,
file('theBenchmark.p',axiom_019) ).
cnf(c_23,plain,
elem(A,nil) = bfalse,
inference(clausify,[status(thm)],[axiom_019]) ).
fof(axiom_020,axiom,
! [VAR_0,VAR_1,VAR_2] : elem(VAR_0,cons(VAR_1,VAR_2)) = orb(eq2(VAR_1,VAR_0),elem(VAR_0,VAR_2)),
file('theBenchmark.p',axiom_020) ).
cnf(c_24,plain,
elem(A,cons(B,C)) = orb(eq2(B,A),elem(A,C)),
inference(clausify,[status(thm)],[axiom_020]) ).
cnf(c_25,plain,
orb(eq2(A,B),elem(B,C)) = elem(B,cons(A,C)),
inference(copy,[status(thm)],[c_24]) ).
fof(axiom_021,axiom,
! [VAR_0] : del(VAR_0,nil) = nil,
file('theBenchmark.p',axiom_021) ).
cnf(c_26,plain,
del(A,nil) = nil,
inference(clausify,[status(thm)],[axiom_021]) ).
fof(axiom_022,axiom,
! [VAR_0,VAR_1,VAR_2] : del(VAR_0,cons(VAR_1,VAR_2)) = aux(VAR_0,VAR_1,VAR_2,eq2(VAR_0,VAR_1)),
file('theBenchmark.p',axiom_022) ).
cnf(c_27,plain,
del(A,cons(B,C)) = aux(A,B,C,eq2(A,B)),
inference(clausify,[status(thm)],[axiom_022]) ).
cnf(c_28,plain,
aux(A,B,C,eq2(A,B)) = del(A,cons(B,C)),
inference(copy,[status(thm)],[c_27]) ).
fof(axiom_023,axiom,
! [VAR_0] : andb(btrue,VAR_0) = VAR_0,
file('theBenchmark.p',axiom_023) ).
cnf(c_29,plain,
andb(btrue,A) = A,
inference(clausify,[status(thm)],[axiom_023]) ).
fof(axiom_027,axiom,
! [VAR_0] : eval(VAR_0,fF) = bfalse,
file('theBenchmark.p',axiom_027) ).
cnf(c_34,plain,
eval(A,fF) = bfalse,
inference(clausify,[status(thm)],[axiom_027]) ).
fof(axiom_028,axiom,
! [VAR_0,VAR_1] : eval(VAR_0,var(VAR_1)) = elem(VAR_1,VAR_0),
file('theBenchmark.p',axiom_028) ).
cnf(c_35,plain,
eval(A,var(B)) = elem(B,A),
inference(clausify,[status(thm)],[axiom_028]) ).
cnf(c_36,plain,
elem(A,B) = eval(B,var(A)),
inference(copy,[status(thm)],[c_35]) ).
fof(axiom_029,axiom,
! [VAR_0] : run(VAR_0,skip) = VAR_0,
file('theBenchmark.p',axiom_029) ).
cnf(c_37,plain,
run(A,skip) = A,
inference(clausify,[status(thm)],[axiom_029]) ).
fof(axiom_030,axiom,
! [VAR_0,VAR_1,VAR_2] : run(VAR_0,assign(VAR_1,VAR_2)) = aux2(VAR_0,VAR_1,VAR_2,eval(VAR_0,VAR_2)),
file('theBenchmark.p',axiom_030) ).
cnf(c_38,plain,
run(A,assign(B,C)) = aux2(A,B,C,eval(A,C)),
inference(clausify,[status(thm)],[axiom_030]) ).
cnf(c_39,plain,
aux2(A,B,C,eval(A,C)) = run(A,assign(B,C)),
inference(copy,[status(thm)],[c_38]) ).
fof(axiom_032,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] : run(VAR_0,ifThenElse(VAR_1,VAR_2,VAR_3)) = aux3(VAR_0,VAR_1,VAR_2,VAR_3,eval(VAR_0,VAR_1)),
file('theBenchmark.p',axiom_032) ).
cnf(c_42,plain,
run(A,ifThenElse(B,C,D)) = aux3(A,B,C,D,eval(A,B)),
inference(clausify,[status(thm)],[axiom_032]) ).
cnf(c_43,plain,
aux3(A,B,C,D,eval(A,B)) = run(A,ifThenElse(B,C,D)),
inference(copy,[status(thm)],[c_42]) ).
fof(axiom_033,axiom,
typeCorrect(skip) = btrue,
file('theBenchmark.p',axiom_033) ).
cnf(c_44,plain,
typeCorrect(skip) = btrue,
inference(clausify,[status(thm)],[axiom_033]) ).
fof(axiom_035,axiom,
! [VAR_0,VAR_1] : typeCorrect(assign(low(VAR_0),VAR_1)) = notb(secret(VAR_1)),
file('theBenchmark.p',axiom_035) ).
cnf(c_46,plain,
typeCorrect(assign(low(A),B)) = notb(secret(B)),
inference(clausify,[status(thm)],[axiom_035]) ).
fof(axiom_036,axiom,
! [VAR_0,VAR_1] : typeCorrect(seq(VAR_0,VAR_1)) = andb(typeCorrect(VAR_0),typeCorrect(VAR_1)),
file('theBenchmark.p',axiom_036) ).
cnf(c_47,plain,
typeCorrect(seq(A,B)) = andb(typeCorrect(A),typeCorrect(B)),
inference(clausify,[status(thm)],[axiom_036]) ).
cnf(c_48,plain,
andb(typeCorrect(A),typeCorrect(B)) = typeCorrect(seq(A,B)),
inference(copy,[status(thm)],[c_47]) ).
fof(axiom_037,axiom,
! [VAR_0,VAR_1,VAR_2] : typeCorrect(ifThenElse(VAR_0,VAR_1,VAR_2)) = andb(typeCorrect(VAR_1),typeCorrect(VAR_2)),
file('theBenchmark.p',axiom_037) ).
cnf(c_49,plain,
typeCorrect(ifThenElse(A,B,C)) = andb(typeCorrect(B),typeCorrect(C)),
inference(clausify,[status(thm)],[axiom_037]) ).
cnf(c_50,plain,
typeCorrect(ifThenElse(A,B,C)) = typeCorrect(seq(B,C)),
inference(paramod,[status(thm)],[c_48,c_49]) ).
fof(axiom_038,axiom,
! [VAR_0,VAR_1] : prop(VAR_0,VAR_1) = impl(typeCorrect(VAR_0),eq5(elem(l,run(VAR_1,VAR_0)),elem(l,run(cons(h,VAR_1),VAR_0)))),
file('theBenchmark.p',axiom_038) ).
cnf(c_51,plain,
prop(A,B) = impl(typeCorrect(A),eq5(elem(l,run(B,A)),elem(l,run(cons(h,B),A)))),
inference(clausify,[status(thm)],[axiom_038]) ).
cnf(c_2840,plain,
prop(A,B) = impl(typeCorrect(A),eq5(eval(run(B,A),var(l)),elem(l,run(cons(h,B),A)))),
inference(paramod,[status(thm)],[c_36,c_51]) ).
cnf(c_52,plain,
prop(A,B) = impl(typeCorrect(A),eq5(eval(run(B,A),var(l)),eval(run(cons(h,B),A),var(l)))),
inference(paramod,[status(thm)],[c_36,c_2840]) ).
fof(axiom_041,axiom,
eq5(bfalse,btrue) = bfalse,
file('theBenchmark.p',axiom_041) ).
cnf(c_55,plain,
eq5(bfalse,btrue) = bfalse,
inference(clausify,[status(thm)],[axiom_041]) ).
fof(axiom_045,axiom,
! [VAR_0,VAR_1] : eq3(var(VAR_0),var(VAR_1)) = eq2(VAR_0,VAR_1),
file('theBenchmark.p',axiom_045) ).
cnf(c_59,plain,
eq3(var(A),var(B)) = eq2(A,B),
inference(clausify,[status(thm)],[axiom_045]) ).
cnf(c_60,plain,
eq2(A,B) = eq3(var(A),var(B)),
inference(copy,[status(thm)],[c_59]) ).
fof(axiom_058,axiom,
! [VAR_0,VAR_1] : eq2(high(VAR_0),low(VAR_1)) = bfalse,
file('theBenchmark.p',axiom_058) ).
cnf(c_75,plain,
eq2(high(A),low(B)) = bfalse,
inference(clausify,[status(thm)],[axiom_058]) ).
cnf(c_76,plain,
eq3(var(high(A)),var(low(B))) = bfalse,
inference(paramod,[status(thm)],[c_60,c_75]) ).
fof(axiom_059,axiom,
! [VAR_0,VAR_1] : eq2(low(VAR_0),high(VAR_1)) = bfalse,
file('theBenchmark.p',axiom_059) ).
cnf(c_77,plain,
eq2(low(A),high(B)) = bfalse,
inference(clausify,[status(thm)],[axiom_059]) ).
cnf(c_78,plain,
eq3(var(low(A)),var(high(B))) = bfalse,
inference(paramod,[status(thm)],[c_60,c_77]) ).
fof(axiom_084,axiom,
! [VAR_0] : eq3(VAR_0,VAR_0) = btrue,
file('theBenchmark.p',axiom_084) ).
cnf(c_110,plain,
eq3(A,A) = btrue,
inference(clausify,[status(thm)],[axiom_084]) ).
fof(axiom_086,axiom,
! [VAR_0] : eq5(VAR_0,VAR_0) = btrue,
file('theBenchmark.p',axiom_086) ).
cnf(c_112,plain,
eq5(A,A) = btrue,
inference(clausify,[status(thm)],[axiom_086]) ).
fof(goal,axiom,
! [VAR_0,VAR_1] : eq5(prop(VAR_0,VAR_1),bfalse) != btrue,
file('theBenchmark.p',goal) ).
cnf(c_113,plain,
eq5(prop(A,B),bfalse) != btrue,
inference(clausify,[status(thm)],[goal]) ).
cnf(c_114,plain,
eq5(impl(typeCorrect(A),eq5(eval(run(B,A),var(l)),eval(run(cons(h,B),A),var(l)))),bfalse) != btrue,
inference(paramod,[status(thm)],[c_52,c_113]) ).
cnf(c_2841,plain,
orb(eq3(var(A),var(B)),elem(B,C)) = elem(B,cons(A,C)),
inference(paramod,[status(thm)],[c_60,c_25]) ).
cnf(c_2842,plain,
orb(eq3(var(A),var(B)),eval(C,var(B))) = elem(B,cons(A,C)),
inference(paramod,[status(thm)],[c_36,c_2841]) ).
cnf(c_115,plain,
orb(eq3(var(A),var(B)),eval(C,var(B))) = eval(cons(A,C),var(B)),
inference(paramod,[status(thm)],[c_36,c_2842]) ).
cnf(c_116,plain,
eval(nil,var(A)) = bfalse,
inference(paramod,[status(thm)],[c_36,c_23]) ).
cnf(c_117,plain,
aux(A,B,C,eq3(var(A),var(B))) = del(A,cons(B,C)),
inference(paramod,[status(thm)],[c_60,c_28]) ).
cnf(c_2843,plain,
aux2(A,B,fF,bfalse) = run(A,assign(B,fF)),
inference(paramod,[status(thm)],[c_34,c_39]) ).
cnf(c_2844,plain,
del(B,A) = run(A,assign(B,fF)),
inference(paramod,[status(thm)],[c_4,c_2843]) ).
cnf(c_133,plain,
run(A,assign(B,fF)) = del(B,A),
inference(copy,[status(thm)],[c_2844]) ).
cnf(c_140,plain,
typeCorrect(assign(l,A)) = notb(secret(A)),
inference(paramod,[status(thm)],[c_18,c_46]) ).
cnf(c_2845,plain,
andb(btrue,typeCorrect(A)) = typeCorrect(seq(skip,A)),
inference(paramod,[status(thm)],[c_44,c_48]) ).
cnf(c_2846,plain,
typeCorrect(A) = typeCorrect(seq(skip,A)),
inference(paramod,[status(thm)],[c_29,c_2845]) ).
cnf(c_141,plain,
typeCorrect(seq(skip,A)) = typeCorrect(A),
inference(copy,[status(thm)],[c_2846]) ).
cnf(c_165,plain,
eq3(var(high(A)),var(l)) = bfalse,
inference(paramod,[status(thm)],[c_18,c_76]) ).
cnf(c_168,plain,
eq3(var(l),var(high(A))) = bfalse,
inference(paramod,[status(thm)],[c_18,c_78]) ).
cnf(c_221,plain,
eq5(impl(typeCorrect(seq(A,B)),eq5(eval(run(C,ifThenElse(D,A,B)),var(l)),eval(run(cons(h,C),ifThenElse(D,A,B)),var(l)))),bfalse) != btrue,
inference(paramod,[status(thm)],[c_50,c_114]) ).
cnf(c_2847,plain,
orb(btrue,eval(A,var(B))) = eval(cons(B,A),var(B)),
inference(paramod,[status(thm)],[c_110,c_115]) ).
cnf(c_2848,plain,
btrue = eval(cons(B,A),var(B)),
inference(paramod,[status(thm)],[c_7,c_2847]) ).
cnf(c_227,plain,
eval(cons(A,B),var(A)) = btrue,
inference(copy,[status(thm)],[c_2848]) ).
cnf(c_2849,plain,
aux(A,A,B,btrue) = del(A,cons(A,B)),
inference(paramod,[status(thm)],[c_110,c_117]) ).
cnf(c_2850,plain,
del(A,B) = del(A,cons(A,B)),
inference(paramod,[status(thm)],[c_1,c_2849]) ).
cnf(c_238,plain,
del(A,cons(A,B)) = del(A,B),
inference(copy,[status(thm)],[c_2850]) ).
cnf(c_276,plain,
eq5(impl(typeCorrect(A),eq5(eval(run(B,ifThenElse(C,skip,A)),var(l)),eval(run(cons(h,B),ifThenElse(C,skip,A)),var(l)))),bfalse) != btrue,
inference(paramod,[status(thm)],[c_141,c_221]) ).
cnf(c_2851,plain,
aux3(cons(A,B),var(A),C,D,btrue) = run(cons(A,B),ifThenElse(var(A),C,D)),
inference(paramod,[status(thm)],[c_227,c_43]) ).
cnf(c_2852,plain,
run(cons(A,B),C) = run(cons(A,B),ifThenElse(var(A),C,D)),
inference(paramod,[status(thm)],[c_5,c_2851]) ).
cnf(c_284,plain,
run(cons(A,B),ifThenElse(var(A),C,D)) = run(cons(A,B),C),
inference(copy,[status(thm)],[c_2852]) ).
cnf(c_2853,plain,
orb(eq3(var(A),var(B)),btrue) = eval(cons(A,cons(B,C)),var(B)),
inference(paramod,[status(thm)],[c_227,c_115]) ).
cnf(c_285,plain,
eval(cons(A,cons(B,C)),var(B)) = orb(eq3(var(A),var(B)),btrue),
inference(copy,[status(thm)],[c_2853]) ).
cnf(c_359,plain,
eq3(var(h),var(l)) = bfalse,
inference(paramod,[status(thm)],[c_22,c_165]) ).
cnf(c_399,plain,
eq3(var(l),var(h)) = bfalse,
inference(paramod,[status(thm)],[c_22,c_168]) ).
cnf(c_2854,plain,
orb(bfalse,eval(A,var(h))) = eval(cons(l,A),var(h)),
inference(paramod,[status(thm)],[c_399,c_115]) ).
cnf(c_2855,plain,
eval(A,var(h)) = eval(cons(l,A),var(h)),
inference(paramod,[status(thm)],[c_8,c_2854]) ).
cnf(c_420,plain,
eval(cons(l,A),var(h)) = eval(A,var(h)),
inference(copy,[status(thm)],[c_2855]) ).
cnf(c_427,plain,
aux3(cons(l,A),var(h),B,C,eval(A,var(h))) = run(cons(l,A),ifThenElse(var(h),B,C)),
inference(paramod,[status(thm)],[c_420,c_43]) ).
cnf(c_2856,plain,
aux3(cons(l,nil),var(h),A,B,bfalse) = run(cons(l,nil),ifThenElse(var(h),A,B)),
inference(paramod,[status(thm)],[c_116,c_427]) ).
cnf(c_2857,plain,
run(cons(l,nil),B) = run(cons(l,nil),ifThenElse(var(h),A,B)),
inference(paramod,[status(thm)],[c_6,c_2856]) ).
cnf(c_2662,plain,
run(cons(l,nil),ifThenElse(var(h),A,B)) = run(cons(l,nil),B),
inference(copy,[status(thm)],[c_2857]) ).
cnf(c_2858,plain,
eq5(impl(typeCorrect(A),eq5(eval(run(cons(l,nil),A),var(l)),eval(run(cons(h,cons(l,nil)),ifThenElse(var(h),skip,A)),var(l)))),bfalse) != btrue,
inference(paramod,[status(thm)],[c_2662,c_276]) ).
cnf(c_2859,plain,
eq5(impl(typeCorrect(A),eq5(eval(run(cons(l,nil),A),var(l)),eval(run(cons(h,cons(l,nil)),skip),var(l)))),bfalse) != btrue,
inference(paramod,[status(thm)],[c_284,c_2858]) ).
cnf(c_2860,plain,
eq5(impl(typeCorrect(A),eq5(eval(run(cons(l,nil),A),var(l)),eval(cons(h,cons(l,nil)),var(l)))),bfalse) != btrue,
inference(paramod,[status(thm)],[c_37,c_2859]) ).
cnf(c_2861,plain,
eq5(impl(typeCorrect(A),eq5(eval(run(cons(l,nil),A),var(l)),orb(eq3(var(h),var(l)),btrue))),bfalse) != btrue,
inference(paramod,[status(thm)],[c_285,c_2860]) ).
cnf(c_2862,plain,
eq5(impl(typeCorrect(A),eq5(eval(run(cons(l,nil),A),var(l)),orb(bfalse,btrue))),bfalse) != btrue,
inference(paramod,[status(thm)],[c_359,c_2861]) ).
cnf(c_2752,plain,
eq5(impl(typeCorrect(A),eq5(eval(run(cons(l,nil),A),var(l)),btrue)),bfalse) != btrue,
inference(paramod,[status(thm)],[c_8,c_2862]) ).
cnf(c_2759,plain,
eq5(impl(typeCorrect(assign(A,fF)),eq5(eval(del(A,cons(l,nil)),var(l)),btrue)),bfalse) != btrue,
inference(paramod,[status(thm)],[c_133,c_2752]) ).
cnf(c_2863,plain,
eq5(impl(notb(secret(fF)),eq5(eval(del(l,cons(l,nil)),var(l)),btrue)),bfalse) != btrue,
inference(paramod,[status(thm)],[c_140,c_2759]) ).
cnf(c_2864,plain,
eq5(impl(notb(bfalse),eq5(eval(del(l,cons(l,nil)),var(l)),btrue)),bfalse) != btrue,
inference(paramod,[status(thm)],[c_14,c_2863]) ).
cnf(c_2865,plain,
eq5(impl(btrue,eq5(eval(del(l,cons(l,nil)),var(l)),btrue)),bfalse) != btrue,
inference(paramod,[status(thm)],[c_16,c_2864]) ).
cnf(c_2866,plain,
eq5(impl(btrue,eq5(eval(del(l,nil),var(l)),btrue)),bfalse) != btrue,
inference(paramod,[status(thm)],[c_238,c_2865]) ).
cnf(c_2867,plain,
eq5(impl(btrue,eq5(eval(nil,var(l)),btrue)),bfalse) != btrue,
inference(paramod,[status(thm)],[c_26,c_2866]) ).
cnf(c_2868,plain,
eq5(impl(btrue,eq5(bfalse,btrue)),bfalse) != btrue,
inference(paramod,[status(thm)],[c_116,c_2867]) ).
cnf(c_2869,plain,
eq5(impl(btrue,bfalse),bfalse) != btrue,
inference(paramod,[status(thm)],[c_55,c_2868]) ).
cnf(c_2870,plain,
eq5(bfalse,bfalse) != btrue,
inference(paramod,[status(thm)],[c_19,c_2869]) ).
cnf(c_2871,plain,
btrue != btrue,
inference(paramod,[status(thm)],[c_112,c_2870]) ).
cnf(c_2839,plain,
$false,
inference(copy,[status(thm)],[c_2871]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWX240-1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.37 % Computer : n018.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Sat Sep 26 17:04:22 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.10/0.37 % Process 940766 was started by sandbox2 on n018,
% 0.10/0.37 % Sat Sep 26 17:04:22 2026
% 0.10/0.37 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.10/0.38
% 0.10/0.38 % From the command line: assign(max_seconds, 300).
% 8.44/1.58
% 8.44/1.58 % given #500 (T,wt=41): 452 eval(nil,nand(A,nand(var(B),C))) = eval(nil,nand(A,tT)). [para(228(a,1),32(a,1,1,2)),rewrite([129(5)]),flip(a)].
% 8.44/1.58
% 8.44/1.58 % SZS status Unsatisfiable for theBenchmark
% 8.44/1.58
% 8.44/1.58 % Proof 1 at 0.90 (+ 0.26) seconds.
% 8.44/1.58 % Length of proof is 69.
% 8.44/1.58 % Level of proof is 10.
% 8.44/1.58 % Maximum clause weight is 65.000.
% 8.44/1.58 % Given clauses 605.
% 8.44/1.58
% 8.44/1.58 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------