%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SWX241-1 : TPTP v9.3.1. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n019.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 17.76s 2.66s
% Output : CNFRefutation 17.76s
% Verified :
% SZS Type : Refutation
% Derivation depth : 33
% Number of leaves : 34
% Syntax : Number of formulae : 142 ( 142 unt; 0 def)
% Number of atoms : 142 ( 141 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 26 ( 26 ~; 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 : 245 ( 31 sgn 59 !; 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_33,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_34,plain,
eval(A,var(B)) = elem(B,A),
inference(clausify,[status(thm)],[axiom_028]) ).
cnf(c_35,plain,
elem(A,B) = eval(B,var(A)),
inference(copy,[status(thm)],[c_34]) ).
fof(axiom_029,axiom,
! [VAR_0] : run(VAR_0,skip) = VAR_0,
file('theBenchmark.p',axiom_029) ).
cnf(c_36,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_37,plain,
run(A,assign(B,C)) = aux2(A,B,C,eval(A,C)),
inference(clausify,[status(thm)],[axiom_030]) ).
cnf(c_38,plain,
aux2(A,B,C,eval(A,C)) = run(A,assign(B,C)),
inference(copy,[status(thm)],[c_37]) ).
fof(axiom_031,axiom,
! [VAR_0,VAR_1,VAR_2] : run(VAR_0,seq(VAR_1,VAR_2)) = run(run(VAR_0,VAR_1),VAR_2),
file('theBenchmark.p',axiom_031) ).
cnf(c_39,plain,
run(A,seq(B,C)) = run(run(A,B),C),
inference(clausify,[status(thm)],[axiom_031]) ).
cnf(c_40,plain,
run(run(A,B),C) = run(A,seq(B,C)),
inference(copy,[status(thm)],[c_39]) ).
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_41,plain,
run(A,ifThenElse(B,C,D)) = aux3(A,B,C,D,eval(A,B)),
inference(clausify,[status(thm)],[axiom_032]) ).
cnf(c_42,plain,
aux3(A,B,C,D,eval(A,B)) = run(A,ifThenElse(B,C,D)),
inference(copy,[status(thm)],[c_41]) ).
fof(axiom_034,axiom,
typeCorrect(skip) = btrue,
file('theBenchmark.p',axiom_034) ).
cnf(c_45,plain,
typeCorrect(skip) = btrue,
inference(clausify,[status(thm)],[axiom_034]) ).
fof(axiom_036,axiom,
! [VAR_0,VAR_1] : typeCorrect(assign(low(VAR_0),VAR_1)) = notb(secret(VAR_1)),
file('theBenchmark.p',axiom_036) ).
cnf(c_47,plain,
typeCorrect(assign(low(A),B)) = notb(secret(B)),
inference(clausify,[status(thm)],[axiom_036]) ).
fof(axiom_037,axiom,
! [VAR_0,VAR_1] : typeCorrect(seq(VAR_0,VAR_1)) = andb(typeCorrect(VAR_0),typeCorrect(VAR_1)),
file('theBenchmark.p',axiom_037) ).
cnf(c_48,plain,
typeCorrect(seq(A,B)) = andb(typeCorrect(A),typeCorrect(B)),
inference(clausify,[status(thm)],[axiom_037]) ).
fof(axiom_038,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_038) ).
cnf(c_49,plain,
typeCorrect(ifThenElse(A,B,C)) = andb(typeCorrect(B),typeCorrect(C)),
inference(clausify,[status(thm)],[axiom_038]) ).
fof(axiom_040,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_040) ).
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_040]) ).
cnf(c_12874,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_35,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_35,c_12874]) ).
fof(axiom_043,axiom,
eq5(bfalse,btrue) = bfalse,
file('theBenchmark.p',axiom_043) ).
cnf(c_55,plain,
eq5(bfalse,btrue) = bfalse,
inference(clausify,[status(thm)],[axiom_043]) ).
fof(axiom_047,axiom,
! [VAR_0,VAR_1] : eq3(var(VAR_0),var(VAR_1)) = eq2(VAR_0,VAR_1),
file('theBenchmark.p',axiom_047) ).
cnf(c_59,plain,
eq3(var(A),var(B)) = eq2(A,B),
inference(clausify,[status(thm)],[axiom_047]) ).
cnf(c_60,plain,
eq2(A,B) = eq3(var(A),var(B)),
inference(copy,[status(thm)],[c_59]) ).
fof(axiom_060,axiom,
! [VAR_0,VAR_1] : eq2(high(VAR_0),low(VAR_1)) = bfalse,
file('theBenchmark.p',axiom_060) ).
cnf(c_75,plain,
eq2(high(A),low(B)) = bfalse,
inference(clausify,[status(thm)],[axiom_060]) ).
cnf(c_76,plain,
eq3(var(high(A)),var(low(B))) = bfalse,
inference(paramod,[status(thm)],[c_60,c_75]) ).
fof(axiom_061,axiom,
! [VAR_0,VAR_1] : eq2(low(VAR_0),high(VAR_1)) = bfalse,
file('theBenchmark.p',axiom_061) ).
cnf(c_77,plain,
eq2(low(A),high(B)) = bfalse,
inference(clausify,[status(thm)],[axiom_061]) ).
cnf(c_78,plain,
eq3(var(low(A)),var(high(B))) = bfalse,
inference(paramod,[status(thm)],[c_60,c_77]) ).
fof(axiom_096,axiom,
! [VAR_0] : eq3(VAR_0,VAR_0) = btrue,
file('theBenchmark.p',axiom_096) ).
cnf(c_120,plain,
eq3(A,A) = btrue,
inference(clausify,[status(thm)],[axiom_096]) ).
fof(axiom_098,axiom,
! [VAR_0] : eq5(VAR_0,VAR_0) = btrue,
file('theBenchmark.p',axiom_098) ).
cnf(c_122,plain,
eq5(A,A) = btrue,
inference(clausify,[status(thm)],[axiom_098]) ).
fof(goal,axiom,
! [VAR_0,VAR_1] : eq5(prop(VAR_0,VAR_1),bfalse) != btrue,
file('theBenchmark.p',goal) ).
cnf(c_123,plain,
eq5(prop(A,B),bfalse) != btrue,
inference(clausify,[status(thm)],[goal]) ).
cnf(c_124,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_123]) ).
cnf(c_12875,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_12876,plain,
orb(eq3(var(A),var(B)),eval(C,var(B))) = elem(B,cons(A,C)),
inference(paramod,[status(thm)],[c_35,c_12875]) ).
cnf(c_125,plain,
orb(eq3(var(A),var(B)),eval(C,var(B))) = eval(cons(A,C),var(B)),
inference(paramod,[status(thm)],[c_35,c_12876]) ).
cnf(c_126,plain,
eval(nil,var(A)) = bfalse,
inference(paramod,[status(thm)],[c_35,c_23]) ).
cnf(c_127,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_12877,plain,
aux2(A,B,fF,bfalse) = run(A,assign(B,fF)),
inference(paramod,[status(thm)],[c_33,c_38]) ).
cnf(c_12878,plain,
del(B,A) = run(A,assign(B,fF)),
inference(paramod,[status(thm)],[c_4,c_12877]) ).
cnf(c_143,plain,
run(A,assign(B,fF)) = del(B,A),
inference(copy,[status(thm)],[c_12878]) ).
cnf(c_155,plain,
typeCorrect(assign(l,A)) = notb(secret(A)),
inference(paramod,[status(thm)],[c_18,c_47]) ).
cnf(c_177,plain,
eq3(var(high(A)),var(l)) = bfalse,
inference(paramod,[status(thm)],[c_18,c_76]) ).
cnf(c_180,plain,
eq3(var(l),var(high(A))) = bfalse,
inference(paramod,[status(thm)],[c_18,c_78]) ).
cnf(c_334,plain,
eq5(impl(andb(typeCorrect(A),typeCorrect(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_49,c_124]) ).
cnf(c_12879,plain,
orb(btrue,eval(A,var(B))) = eval(cons(B,A),var(B)),
inference(paramod,[status(thm)],[c_120,c_125]) ).
cnf(c_12880,plain,
btrue = eval(cons(B,A),var(B)),
inference(paramod,[status(thm)],[c_7,c_12879]) ).
cnf(c_342,plain,
eval(cons(A,B),var(A)) = btrue,
inference(copy,[status(thm)],[c_12880]) ).
cnf(c_12881,plain,
aux(A,A,B,btrue) = del(A,cons(A,B)),
inference(paramod,[status(thm)],[c_120,c_127]) ).
cnf(c_12882,plain,
del(A,B) = del(A,cons(A,B)),
inference(paramod,[status(thm)],[c_1,c_12881]) ).
cnf(c_352,plain,
del(A,cons(A,B)) = del(A,B),
inference(copy,[status(thm)],[c_12882]) ).
cnf(c_12883,plain,
aux3(cons(A,B),var(A),C,D,btrue) = run(cons(A,B),ifThenElse(var(A),C,D)),
inference(paramod,[status(thm)],[c_342,c_42]) ).
cnf(c_12884,plain,
run(cons(A,B),C) = run(cons(A,B),ifThenElse(var(A),C,D)),
inference(paramod,[status(thm)],[c_5,c_12883]) ).
cnf(c_424,plain,
run(cons(A,B),ifThenElse(var(A),C,D)) = run(cons(A,B),C),
inference(copy,[status(thm)],[c_12884]) ).
cnf(c_431,plain,
run(del(A,B),C) = run(B,seq(assign(A,fF),C)),
inference(paramod,[status(thm)],[c_143,c_40]) ).
cnf(c_694,plain,
eq3(var(h),var(l)) = bfalse,
inference(paramod,[status(thm)],[c_22,c_177]) ).
cnf(c_12885,plain,
orb(bfalse,eval(A,var(l))) = eval(cons(h,A),var(l)),
inference(paramod,[status(thm)],[c_694,c_125]) ).
cnf(c_12886,plain,
eval(A,var(l)) = eval(cons(h,A),var(l)),
inference(paramod,[status(thm)],[c_8,c_12885]) ).
cnf(c_701,plain,
eval(cons(h,A),var(l)) = eval(A,var(l)),
inference(copy,[status(thm)],[c_12886]) ).
cnf(c_757,plain,
eq3(var(l),var(h)) = bfalse,
inference(paramod,[status(thm)],[c_22,c_180]) ).
cnf(c_12887,plain,
orb(bfalse,eval(A,var(h))) = eval(cons(l,A),var(h)),
inference(paramod,[status(thm)],[c_757,c_125]) ).
cnf(c_12888,plain,
eval(A,var(h)) = eval(cons(l,A),var(h)),
inference(paramod,[status(thm)],[c_8,c_12887]) ).
cnf(c_764,plain,
eval(cons(l,A),var(h)) = eval(A,var(h)),
inference(copy,[status(thm)],[c_12888]) ).
cnf(c_784,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_764,c_42]) ).
cnf(c_12889,plain,
run(del(A,B),C) = run(cons(A,B),seq(assign(A,fF),C)),
inference(paramod,[status(thm)],[c_352,c_431]) ).
cnf(c_1431,plain,
run(cons(A,B),seq(assign(A,fF),C)) = run(del(A,B),C),
inference(copy,[status(thm)],[c_12889]) ).
cnf(c_1952,plain,
run(cons(A,B),seq(assign(A,fF),C)) = run(B,seq(assign(A,fF),C)),
inference(paramod,[status(thm)],[c_1431,c_431]) ).
cnf(c_12890,plain,
eq5(impl(andb(btrue,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_45,c_334]) ).
cnf(c_2836,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_29,c_12890]) ).
cnf(c_12891,plain,
aux3(cons(l,nil),var(h),A,B,bfalse) = run(cons(l,nil),ifThenElse(var(h),A,B)),
inference(paramod,[status(thm)],[c_126,c_784]) ).
cnf(c_12892,plain,
run(cons(l,nil),B) = run(cons(l,nil),ifThenElse(var(h),A,B)),
inference(paramod,[status(thm)],[c_6,c_12891]) ).
cnf(c_9088,plain,
run(cons(l,nil),ifThenElse(var(h),A,B)) = run(cons(l,nil),B),
inference(copy,[status(thm)],[c_12892]) ).
cnf(c_12893,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_9088,c_2836]) ).
cnf(c_12894,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_424,c_12893]) ).
cnf(c_12895,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_36,c_12894]) ).
cnf(c_12896,plain,
eq5(impl(typeCorrect(A),eq5(eval(run(cons(l,nil),A),var(l)),eval(cons(l,nil),var(l)))),bfalse) != btrue,
inference(paramod,[status(thm)],[c_701,c_12895]) ).
cnf(c_11748,plain,
eq5(impl(typeCorrect(A),eq5(eval(run(cons(l,nil),A),var(l)),btrue)),bfalse) != btrue,
inference(paramod,[status(thm)],[c_342,c_12896]) ).
cnf(c_12897,plain,
eq5(impl(typeCorrect(seq(assign(l,fF),A)),eq5(eval(run(nil,seq(assign(l,fF),A)),var(l)),btrue)),bfalse) != btrue,
inference(paramod,[status(thm)],[c_1952,c_11748]) ).
cnf(c_12898,plain,
eq5(impl(andb(typeCorrect(assign(l,fF)),typeCorrect(A)),eq5(eval(run(nil,seq(assign(l,fF),A)),var(l)),btrue)),bfalse) != btrue,
inference(paramod,[status(thm)],[c_48,c_12897]) ).
cnf(c_12899,plain,
eq5(impl(andb(notb(secret(fF)),typeCorrect(A)),eq5(eval(run(nil,seq(assign(l,fF),A)),var(l)),btrue)),bfalse) != btrue,
inference(paramod,[status(thm)],[c_155,c_12898]) ).
cnf(c_12900,plain,
eq5(impl(andb(notb(bfalse),typeCorrect(A)),eq5(eval(run(nil,seq(assign(l,fF),A)),var(l)),btrue)),bfalse) != btrue,
inference(paramod,[status(thm)],[c_14,c_12899]) ).
cnf(c_12901,plain,
eq5(impl(andb(btrue,typeCorrect(A)),eq5(eval(run(nil,seq(assign(l,fF),A)),var(l)),btrue)),bfalse) != btrue,
inference(paramod,[status(thm)],[c_16,c_12900]) ).
cnf(c_12902,plain,
eq5(impl(typeCorrect(A),eq5(eval(run(nil,seq(assign(l,fF),A)),var(l)),btrue)),bfalse) != btrue,
inference(paramod,[status(thm)],[c_29,c_12901]) ).
cnf(c_12903,plain,
eq5(impl(typeCorrect(A),eq5(eval(run(run(nil,assign(l,fF)),A),var(l)),btrue)),bfalse) != btrue,
inference(paramod,[status(thm)],[c_40,c_12902]) ).
cnf(c_12904,plain,
eq5(impl(typeCorrect(A),eq5(eval(run(del(l,nil),A),var(l)),btrue)),bfalse) != btrue,
inference(paramod,[status(thm)],[c_143,c_12903]) ).
cnf(c_11773,plain,
eq5(impl(typeCorrect(A),eq5(eval(run(nil,A),var(l)),btrue)),bfalse) != btrue,
inference(paramod,[status(thm)],[c_26,c_12904]) ).
cnf(c_12905,plain,
eq5(impl(typeCorrect(skip),eq5(eval(nil,var(l)),btrue)),bfalse) != btrue,
inference(paramod,[status(thm)],[c_36,c_11773]) ).
cnf(c_12906,plain,
eq5(impl(btrue,eq5(eval(nil,var(l)),btrue)),bfalse) != btrue,
inference(paramod,[status(thm)],[c_45,c_12905]) ).
cnf(c_12907,plain,
eq5(impl(btrue,eq5(bfalse,btrue)),bfalse) != btrue,
inference(paramod,[status(thm)],[c_126,c_12906]) ).
cnf(c_12908,plain,
eq5(impl(btrue,bfalse),bfalse) != btrue,
inference(paramod,[status(thm)],[c_55,c_12907]) ).
cnf(c_12909,plain,
eq5(bfalse,bfalse) != btrue,
inference(paramod,[status(thm)],[c_19,c_12908]) ).
cnf(c_12910,plain,
btrue != btrue,
inference(paramod,[status(thm)],[c_122,c_12909]) ).
cnf(c_12873,plain,
$false,
inference(copy,[status(thm)],[c_12910]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWX241-1 : TPTP v9.3.1. Released v9.3.0.
% 0.00/0.03 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.34 % Computer : n019.cluster.edu
% 0.08/0.34 % Model : x86_64 x86_64
% 0.08/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.34 % Memory : 8046.5625MB
% 0.08/0.34 % OS : Linux 6.8.0-71-generic
% 0.08/0.34 % CPULimit : 300
% 0.08/0.34 % WCLimit : 300
% 0.08/0.35 % DateTime : Sat Sep 26 17:02:04 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.08/0.35 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.08/0.35 % Process 1789729 was started by sandbox on n019,
% 0.08/0.35 % Sat Sep 26 17:02:04 2026
% 0.08/0.35 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.08/0.36
% 0.08/0.36 % From the command line: assign(max_seconds, 300).
% 17.76/2.66
% 17.76/2.66 % given #500 (W,wt=38): 438 aux2(A,B,nand(tT,C),notb(eval(A,C))) = run(A,assign(B,nand(tT,C))). [para(32(a,1),141(a,1,4,1,1)),rewrite([29(5)])].
% 17.76/2.66
% 17.76/2.66 % SZS status Unsatisfiable for theBenchmark
% 17.76/2.66
% 17.76/2.66 % Proof 1 at 1.87 (+ 0.41) seconds.
% 17.76/2.66 % Length of proof is 71.
% 17.76/2.66 % Level of proof is 10.
% 17.76/2.66 % Maximum clause weight is 66.000.
% 17.76/2.66 % Given clauses 960.
% 17.76/2.66
% 17.76/2.66 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------