%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : SWX240_1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% Computer : n022.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 06:56:41 PM UTC 2026
% Result : Theorem 90.79s 54.47s
% Output : CNFRefutation 90.99s
% Verified :
% SZS Type : Refutation
% Derivation depth : 45
% Number of leaves : 24
% Syntax : Number of formulae : 176 ( 56 unt; 0 typ; 0 def)
% Number of atoms : 370 ( 92 equ)
% Maximal formula atoms : 5 ( 2 avg)
% Number of connectives : 338 ( 144 ~; 178 |; 2 &)
% ( 7 <=>; 7 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 5 avg)
% Maximal term depth : 6 ( 1 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 6 ( 4 usr; 1 prp; 0-2 aty)
% Number of functors : 33 ( 33 usr; 7 con; 0-3 aty)
% Number of variables : 381 ( 379 !; 2 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ eval > elem > typeCorrect > secret > ifThenElse > seq > run > nand > del > cons > assign > #nlpp > var > tail > suc > proj3IfThenElse > proj2Seq > proj2Nand > proj2IfThenElse > proj2Assign > proj1Var > proj1Suc > proj1Seq > proj1Nand > proj1Low > proj1IfThenElse > proj1High > proj1Assign > low > high > head > zero > tT > skip > nil > l > h > fF
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(proj3IfThenElse,type,
proj3IfThenElse: $i > $i ).
tff(del,type,
del: ( $i * $i ) > $i ).
tff(tT,type,
tT: $i ).
tff(high,type,
high: $i > $i ).
tff(h,type,
h: $i ).
tff(proj1Low,type,
proj1Low: $i > $i ).
tff(low,type,
low: $i > $i ).
tff(fF,type,
fF: $i ).
tff(l,type,
l: $i ).
tff(elem,type,
elem: ( $i * $i ) > $o ).
tff(proj2Nand,type,
proj2Nand: $i > $i ).
tff(proj1Suc,type,
proj1Suc: $i > $i ).
tff(seq,type,
seq: ( $i * $i ) > $i ).
tff(proj2IfThenElse,type,
proj2IfThenElse: $i > $i ).
tff(nand,type,
nand: ( $i * $i ) > $i ).
tff(proj2Seq,type,
proj2Seq: $i > $i ).
tff(ifThenElse,type,
ifThenElse: ( $i * $i * $i ) > $i ).
tff(eval,type,
eval: ( $i * $i ) > $o ).
tff(proj1Assign,type,
proj1Assign: $i > $i ).
tff(secret,type,
secret: $i > $o ).
tff(proj1Seq,type,
proj1Seq: $i > $i ).
tff(typeCorrect,type,
typeCorrect: $i > $o ).
tff(assign,type,
assign: ( $i * $i ) > $i ).
tff(skip,type,
skip: $i ).
tff(var,type,
var: $i > $i ).
tff(proj1Var,type,
proj1Var: $i > $i ).
tff(suc,type,
suc: $i > $i ).
tff(cons,type,
cons: ( $i * $i ) > $i ).
tff(proj1High,type,
proj1High: $i > $i ).
tff(proj1Nand,type,
proj1Nand: $i > $i ).
tff(proj1IfThenElse,type,
proj1IfThenElse: $i > $i ).
tff(tail,type,
tail: $i > $i ).
tff(run,type,
run: ( $i * $i ) > $i ).
tff(head,type,
head: $i > $i ).
tff(nil,type,
nil: $i ).
tff(proj2Assign,type,
proj2Assign: $i > $i ).
tff(zero,type,
zero: $i ).
tff(f_140,axiom,
h = high(zero),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_041) ).
tff(f_139,axiom,
l = low(zero),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_040) ).
tff(f_43,axiom,
! [X,X2] : ( high(X) != low(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_008) ).
tff(f_121,axiom,
! [E,Z] : typeCorrect(assign(high(Z),E)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_036) ).
tff(f_149,axiom,
! [X,Z,Xs] :
( elem(X,cons(Z,Xs))
<=> ( ( Z = X )
| elem(X,Xs) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_043) ).
tff(f_143,axiom,
! [X] : ~ elem(X,nil),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_042) ).
tff(f_166,axiom,
! [X,Z] :
( eval(X,var(Z))
<=> elem(Z,X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_047) ).
tff(f_159,axiom,
! [X] : eval(X,tT),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_045) ).
tff(f_107,axiom,
! [X] :
( ( X != nand(proj1Nand(X),proj2Nand(X)) )
=> ( ( X != var(proj1Var(X)) )
=> ~ secret(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_031) ).
tff(f_52,axiom,
! [X,X2] : ( nand(X,X2) != tT ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_012) ).
tff(f_126,axiom,
! [E,X2] :
( typeCorrect(assign(low(X2),E))
<=> ~ secret(E) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_037) ).
tff(f_183,axiom,
! [X,Z,E] :
( eval(X,E)
=> ( run(X,assign(Z,E)) = cons(Z,X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_052) ).
tff(f_207,negated_conjecture,
~ ? [P,S] :
~ ( typeCorrect(P)
=> ( elem(l,run(S,P))
<=> elem(l,run(cons(h,S),P)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goal_057) ).
tff(f_119,axiom,
typeCorrect(skip),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_035) ).
tff(f_138,axiom,
! [C,R,Q2] :
( typeCorrect(ifThenElse(C,R,Q2))
<=> ( typeCorrect(R)
& typeCorrect(Q2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_039) ).
tff(f_162,axiom,
! [X] : ~ eval(X,fF),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_046) ).
tff(f_168,axiom,
! [X] : ( del(X,nil) = nil ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_048) ).
tff(f_179,axiom,
! [X] : ( run(X,skip) = X ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_051) ).
tff(f_190,axiom,
! [X,P,Q] : ( run(X,seq(P,Q)) = run(run(X,P),Q) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_054) ).
tff(f_199,axiom,
! [X,E2,R,Q2] :
( ~ eval(X,E2)
=> ( run(X,ifThenElse(E2,R,Q2)) = run(X,Q2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_056) ).
tff(f_188,axiom,
! [X,Z,E] :
( ~ eval(X,E)
=> ( run(X,assign(Z,E)) = del(Z,X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_053) ).
tff(f_157,axiom,
! [X,A,B] :
( eval(X,nand(A,B))
<=> ( ~ eval(X,A)
| ~ eval(X,B) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_044) ).
tff(f_194,axiom,
! [X,E2,R,Q2] :
( eval(X,E2)
=> ( run(X,ifThenElse(E2,R,Q2)) = run(X,R) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_055) ).
tff(f_132,axiom,
! [P,Q] :
( typeCorrect(seq(P,Q))
<=> ( typeCorrect(P)
& typeCorrect(Q) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',axiom_038) ).
tff(c_96,plain,
high(zero) = h,
inference(cnfTransformation,[status(thm)],[f_140]) ).
tff(c_94,plain,
low(zero) = l,
inference(cnfTransformation,[status(thm)],[f_139]) ).
tff(c_176,plain,
! [X2_129,X_130] : ( low(X2_129) != high(X_130) ),
inference(cnfTransformation,[status(thm)],[f_43]) ).
tff(c_179,plain,
! [X_131] : ( high(X_131) != l ),
inference(superposition,[status(thm),theory(equality)],[c_94,c_176]) ).
tff(c_181,plain,
l != h,
inference(superposition,[status(thm),theory(equality)],[c_96,c_179]) ).
tff(c_296,plain,
! [Z_165,E_166] : typeCorrect(assign(high(Z_165),E_166)),
inference(cnfTransformation,[status(thm)],[f_121]) ).
tff(c_298,plain,
! [E_166] : typeCorrect(assign(h,E_166)),
inference(superposition,[status(thm),theory(equality)],[c_96,c_296]) ).
tff(c_104,plain,
! [Z_81,Xs_82] : elem(Z_81,cons(Z_81,Xs_82)),
inference(cnfTransformation,[status(thm)],[f_149]) ).
tff(c_98,plain,
! [X_79] : ~ elem(X_79,nil),
inference(cnfTransformation,[status(thm)],[f_143]) ).
tff(c_118,plain,
! [X_88,Z_89] :
( eval(X_88,var(Z_89))
| ~ elem(Z_89,X_88) ),
inference(cnfTransformation,[status(thm)],[f_166]) ).
tff(c_112,plain,
! [X_86] : eval(X_86,tT),
inference(cnfTransformation,[status(thm)],[f_159]) ).
tff(c_645,plain,
! [X_264] :
( ~ secret(X_264)
| ( var(proj1Var(X_264)) = X_264 )
| ( nand(proj1Nand(X_264),proj2Nand(X_264)) = X_264 ) ),
inference(cnfTransformation,[status(thm)],[f_107]) ).
tff(c_24,plain,
! [X_18,X2_19] : ( nand(X_18,X2_19) != tT ),
inference(cnfTransformation,[status(thm)],[f_52]) ).
tff(c_793,plain,
! [X_272] :
( ( tT != X_272 )
| ~ secret(X_272)
| ( var(proj1Var(X_272)) = X_272 ) ),
inference(superposition,[status(thm),theory(equality)],[c_645,c_24]) ).
tff(c_116,plain,
! [Z_89,X_88] :
( elem(Z_89,X_88)
| ~ eval(X_88,var(Z_89)) ),
inference(cnfTransformation,[status(thm)],[f_166]) ).
tff(c_1005,plain,
! [X_298,X_299] :
( elem(proj1Var(X_298),X_299)
| ~ eval(X_299,X_298)
| ( tT != X_298 )
| ~ secret(X_298) ),
inference(superposition,[status(thm),theory(equality)],[c_793,c_116]) ).
tff(c_1024,plain,
! [X_300] :
( ~ eval(nil,X_300)
| ( tT != X_300 )
| ~ secret(X_300) ),
inference(resolution,[status(thm)],[c_1005,c_98]) ).
tff(c_1044,plain,
~ secret(tT),
inference(resolution,[status(thm)],[c_112,c_1024]) ).
tff(c_379,plain,
! [X2_209,E_210] :
( typeCorrect(assign(low(X2_209),E_210))
| secret(E_210) ),
inference(cnfTransformation,[status(thm)],[f_126]) ).
tff(c_384,plain,
! [E_210] :
( typeCorrect(assign(l,E_210))
| secret(E_210) ),
inference(superposition,[status(thm),theory(equality)],[c_94,c_379]) ).
tff(c_514,plain,
! [X_250,Z_251,E_252] :
( ( run(X_250,assign(Z_251,E_252)) = cons(Z_251,X_250) )
| ~ eval(X_250,E_252) ),
inference(cnfTransformation,[status(thm)],[f_183]) ).
tff(c_138,plain,
! [S_116,P_115] :
( elem(l,run(S_116,P_115))
| ~ elem(l,run(cons(h,S_116),P_115))
| ~ typeCorrect(P_115) ),
inference(cnfTransformation,[status(thm)],[f_207]) ).
tff(c_852,plain,
! [S_277,Z_278,E_279] :
( elem(l,run(S_277,assign(Z_278,E_279)))
| ~ elem(l,cons(Z_278,cons(h,S_277)))
| ~ typeCorrect(assign(Z_278,E_279))
| ~ eval(cons(h,S_277),E_279) ),
inference(superposition,[status(thm),theory(equality)],[c_514,c_138]) ).
tff(c_2661,plain,
! [S_431,Z_432,E_433] :
( elem(l,run(S_431,assign(Z_432,E_433)))
| ~ elem(l,cons(Z_432,cons(h,cons(h,S_431))))
| ~ typeCorrect(assign(Z_432,E_433))
| ~ eval(cons(h,cons(h,S_431)),E_433) ),
inference(resolution,[status(thm)],[c_852,c_138]) ).
tff(c_7623,plain,
! [S_571,E_572] :
( elem(l,run(S_571,assign(l,E_572)))
| ~ typeCorrect(assign(l,E_572))
| ~ eval(cons(h,cons(h,S_571)),E_572) ),
inference(resolution,[status(thm)],[c_104,c_2661]) ).
tff(c_7701,plain,
! [S_571] :
( elem(l,run(S_571,assign(l,tT)))
| ~ typeCorrect(assign(l,tT)) ),
inference(resolution,[status(thm)],[c_112,c_7623]) ).
tff(c_7702,plain,
~ typeCorrect(assign(l,tT)),
inference(splitLeft,[status(thm)],[c_7701]) ).
tff(c_7705,plain,
secret(tT),
inference(resolution,[status(thm)],[c_384,c_7702]) ).
tff(c_7709,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_1044,c_7705]) ).
tff(c_7711,plain,
typeCorrect(assign(l,tT)),
inference(splitRight,[status(thm)],[c_7701]) ).
tff(c_74,plain,
typeCorrect(skip),
inference(cnfTransformation,[status(thm)],[f_119]) ).
tff(c_88,plain,
! [C_76,R_77,Q2_78] :
( typeCorrect(ifThenElse(C_76,R_77,Q2_78))
| ~ typeCorrect(Q2_78)
| ~ typeCorrect(R_77) ),
inference(cnfTransformation,[status(thm)],[f_138]) ).
tff(c_114,plain,
! [X_87] : ~ eval(X_87,fF),
inference(cnfTransformation,[status(thm)],[f_162]) ).
tff(c_120,plain,
! [X_90] : ( del(X_90,nil) = nil ),
inference(cnfTransformation,[status(thm)],[f_168]) ).
tff(c_126,plain,
! [X_97] : ( run(X_97,skip) = X_97 ),
inference(cnfTransformation,[status(thm)],[f_179]) ).
tff(c_453,plain,
! [X_245,P_246,Q_247] : ( run(run(X_245,P_246),Q_247) = run(X_245,seq(P_246,Q_247)) ),
inference(cnfTransformation,[status(thm)],[f_190]) ).
tff(c_472,plain,
! [X_97,Q_247] : ( run(X_97,seq(skip,Q_247)) = run(X_97,Q_247) ),
inference(superposition,[status(thm),theory(equality)],[c_126,c_453]) ).
tff(c_132,plain,
! [X_104,P_105,Q_106] : ( run(run(X_104,P_105),Q_106) = run(X_104,seq(P_105,Q_106)) ),
inference(cnfTransformation,[status(thm)],[f_190]) ).
tff(c_1045,plain,
! [X_301,E2_302,R_303,Q2_304] :
( ( run(X_301,ifThenElse(E2_302,R_303,Q2_304)) = run(X_301,Q2_304) )
| eval(X_301,E2_302) ),
inference(cnfTransformation,[status(thm)],[f_199]) ).
tff(c_1054,plain,
! [Q_106,X_301,E2_302,Q2_304,R_303] :
( ( run(X_301,seq(ifThenElse(E2_302,R_303,Q2_304),Q_106)) = run(run(X_301,Q2_304),Q_106) )
| eval(X_301,E2_302) ),
inference(superposition,[status(thm),theory(equality)],[c_1045,c_132]) ).
tff(c_1078,plain,
! [Q_106,X_301,E2_302,Q2_304,R_303] :
( ( run(X_301,seq(ifThenElse(E2_302,R_303,Q2_304),Q_106)) = run(X_301,seq(Q2_304,Q_106)) )
| eval(X_301,E2_302) ),
inference(demodulation,[status(thm),theory(equality)],[c_132,c_1054]) ).
tff(c_586,plain,
! [X_255,Z_256,E_257] :
( ( run(X_255,assign(Z_256,E_257)) = del(Z_256,X_255) )
| eval(X_255,E_257) ),
inference(cnfTransformation,[status(thm)],[f_188]) ).
tff(c_2803,plain,
! [X_443,P_444,Z_445,E_446] :
( ( run(X_443,seq(P_444,assign(Z_445,E_446))) = del(Z_445,run(X_443,P_444)) )
| eval(run(X_443,P_444),E_446) ),
inference(superposition,[status(thm),theory(equality)],[c_132,c_586]) ).
tff(c_66907,plain,
! [Z_1512,E_1510,X_1508,R_1509,Q2_1511,E2_1507] :
( ( run(X_1508,seq(Q2_1511,assign(Z_1512,E_1510))) = del(Z_1512,run(X_1508,ifThenElse(E2_1507,R_1509,Q2_1511))) )
| eval(run(X_1508,ifThenElse(E2_1507,R_1509,Q2_1511)),E_1510)
| eval(X_1508,E2_1507) ),
inference(superposition,[status(thm),theory(equality)],[c_1078,c_2803]) ).
tff(c_128109,plain,
! [Q2_2529,X_2525,R_2526,Z_2527,E2_2528] :
( ( run(X_2525,seq(Q2_2529,assign(Z_2527,fF))) = del(Z_2527,run(X_2525,ifThenElse(E2_2528,R_2526,Q2_2529))) )
| eval(X_2525,E2_2528) ),
inference(resolution,[status(thm)],[c_66907,c_114]) ).
tff(c_129350,plain,
! [Z_2544,X_2545,E2_2546,R_2547] :
( ( del(Z_2544,run(X_2545,ifThenElse(E2_2546,R_2547,skip))) = run(X_2545,assign(Z_2544,fF)) )
| eval(X_2545,E2_2546) ),
inference(superposition,[status(thm),theory(equality)],[c_472,c_128109]) ).
tff(c_617,plain,
! [X_104,P_105,Z_256,E_257] :
( ( run(X_104,seq(P_105,assign(Z_256,E_257))) = del(Z_256,run(X_104,P_105)) )
| eval(run(X_104,P_105),E_257) ),
inference(superposition,[status(thm),theory(equality)],[c_132,c_586]) ).
tff(c_128573,plain,
! [Q2_2529,X_2525,R_2526,Z_2527,E2_2528] :
( ( del(Z_2527,run(X_2525,ifThenElse(E2_2528,R_2526,Q2_2529))) = del(Z_2527,run(X_2525,Q2_2529)) )
| eval(run(X_2525,Q2_2529),fF)
| eval(X_2525,E2_2528) ),
inference(superposition,[status(thm),theory(equality)],[c_128109,c_617]) ).
tff(c_128826,plain,
! [Q2_2529,X_2525,R_2526,Z_2527,E2_2528] :
( ( del(Z_2527,run(X_2525,ifThenElse(E2_2528,R_2526,Q2_2529))) = del(Z_2527,run(X_2525,Q2_2529)) )
| eval(X_2525,E2_2528) ),
inference(negUnitSimplification,[status(thm)],[c_114,c_128573]) ).
tff(c_129360,plain,
! [X_2545,Z_2544,E2_2546] :
( ( run(X_2545,assign(Z_2544,fF)) = del(Z_2544,run(X_2545,skip)) )
| eval(X_2545,E2_2546)
| eval(X_2545,E2_2546) ),
inference(superposition,[status(thm),theory(equality)],[c_129350,c_128826]) ).
tff(c_129566,plain,
! [X_2545,Z_2544,E2_2546] :
( ( run(X_2545,assign(Z_2544,fF)) = del(Z_2544,X_2545) )
| eval(X_2545,E2_2546)
| eval(X_2545,E2_2546) ),
inference(demodulation,[status(thm),theory(equality)],[c_126,c_129360]) ).
tff(c_130412,plain,
! [X_2551,Z_2552,E2_2553] :
( ( run(X_2551,assign(Z_2552,fF)) = del(Z_2552,X_2551) )
| eval(X_2551,E2_2553) ),
inference(factorization,[status(thm),theory(equality)],[c_129566]) ).
tff(c_106,plain,
! [X_83,B_85,A_84] :
( ~ eval(X_83,B_85)
| ~ eval(X_83,A_84)
| ~ eval(X_83,nand(A_84,B_85)) ),
inference(cnfTransformation,[status(thm)],[f_157]) ).
tff(c_133337,plain,
! [X_2565,B_2566,A_2567,Z_2568] :
( ~ eval(X_2565,B_2566)
| ~ eval(X_2565,A_2567)
| ( run(X_2565,assign(Z_2568,fF)) = del(Z_2568,X_2565) ) ),
inference(resolution,[status(thm)],[c_130412,c_106]) ).
tff(c_133629,plain,
! [X_2569,A_2570,Z_2571] :
( ~ eval(X_2569,A_2570)
| ( run(X_2569,assign(Z_2571,fF)) = del(Z_2571,X_2569) ) ),
inference(resolution,[status(thm)],[c_112,c_133337]) ).
tff(c_133920,plain,
! [X_86,Z_2571] : ( run(X_86,assign(Z_2571,fF)) = del(Z_2571,X_86) ),
inference(resolution,[status(thm)],[c_112,c_133629]) ).
tff(c_595,plain,
! [X_255,Z_256,E_257,Q_106] :
( ( run(X_255,seq(assign(Z_256,E_257),Q_106)) = run(del(Z_256,X_255),Q_106) )
| eval(X_255,E_257) ),
inference(superposition,[status(thm),theory(equality)],[c_586,c_132]) ).
tff(c_26835,plain,
! [Z_896,X_897,E_898,E_895,Z_899] :
( ( run(del(Z_899,X_897),assign(Z_896,E_895)) = del(Z_896,run(X_897,assign(Z_899,E_898))) )
| eval(X_897,E_898)
| eval(run(X_897,assign(Z_899,E_898)),E_895) ),
inference(superposition,[status(thm),theory(equality)],[c_2803,c_595]) ).
tff(c_27092,plain,
! [Z_900,X_901,Z_902,E_903] :
( ( run(del(Z_900,X_901),assign(Z_902,fF)) = del(Z_902,run(X_901,assign(Z_900,E_903))) )
| eval(X_901,E_903) ),
inference(resolution,[status(thm)],[c_26835,c_114]) ).
tff(c_27469,plain,
! [Z_911,X_912,E_913] :
( ( del(Z_911,run(nil,assign(X_912,E_913))) = run(nil,assign(Z_911,fF)) )
| eval(nil,E_913) ),
inference(superposition,[status(thm),theory(equality)],[c_120,c_27092]) ).
tff(c_130,plain,
! [X_101,Z_102,E_103] :
( ( run(X_101,assign(Z_102,E_103)) = del(Z_102,X_101) )
| eval(X_101,E_103) ),
inference(cnfTransformation,[status(thm)],[f_188]) ).
tff(c_27206,plain,
! [Z_902,X_901,Z_900,E_903] :
( ( del(Z_902,run(X_901,assign(Z_900,E_903))) = del(Z_902,del(Z_900,X_901)) )
| eval(del(Z_900,X_901),fF)
| eval(X_901,E_903) ),
inference(superposition,[status(thm),theory(equality)],[c_27092,c_130]) ).
tff(c_27295,plain,
! [Z_902,X_901,Z_900,E_903] :
( ( del(Z_902,run(X_901,assign(Z_900,E_903))) = del(Z_902,del(Z_900,X_901)) )
| eval(X_901,E_903) ),
inference(negUnitSimplification,[status(thm)],[c_114,c_27206]) ).
tff(c_27479,plain,
! [Z_911,X_912,E_913] :
( ( run(nil,assign(Z_911,fF)) = del(Z_911,del(X_912,nil)) )
| eval(nil,E_913)
| eval(nil,E_913) ),
inference(superposition,[status(thm),theory(equality)],[c_27469,c_27295]) ).
tff(c_27565,plain,
! [Z_911,E_913] :
( ( run(nil,assign(Z_911,fF)) = nil )
| eval(nil,E_913)
| eval(nil,E_913) ),
inference(demodulation,[status(thm),theory(equality)],[c_120,c_120,c_27479]) ).
tff(c_27577,plain,
! [E_913] :
( eval(nil,E_913)
| eval(nil,E_913) ),
inference(splitLeft,[status(thm)],[c_27565]) ).
tff(c_27586,plain,
! [E_913] : eval(nil,E_913),
inference(factorization,[status(thm),theory(equality)],[c_27577]) ).
tff(c_27623,plain,
! [E_915] : eval(nil,E_915),
inference(factorization,[status(thm),theory(equality)],[c_27577]) ).
tff(c_27631,plain,
! [B_85,A_84] :
( ~ eval(nil,B_85)
| ~ eval(nil,A_84) ),
inference(resolution,[status(thm)],[c_27623,c_106]) ).
tff(c_27645,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_27586,c_27586,c_27631]) ).
tff(c_27646,plain,
! [Z_911] : ( run(nil,assign(Z_911,fF)) = nil ),
inference(splitRight,[status(thm)],[c_27565]) ).
tff(c_463,plain,
! [X_245,P_246] : ( run(X_245,seq(P_246,skip)) = run(X_245,P_246) ),
inference(superposition,[status(thm),theory(equality)],[c_453,c_126]) ).
tff(c_1058,plain,
! [X_104,E2_302,Q2_304,P_105,R_303] :
( ( run(X_104,seq(P_105,ifThenElse(E2_302,R_303,Q2_304))) = run(run(X_104,P_105),Q2_304) )
| eval(run(X_104,P_105),E2_302) ),
inference(superposition,[status(thm),theory(equality)],[c_1045,c_132]) ).
tff(c_4933,plain,
! [P_507,E2_503,X_506,Q2_505,R_504] :
( ( run(X_506,seq(P_507,ifThenElse(E2_503,R_504,Q2_505))) = run(X_506,seq(P_507,Q2_505)) )
| eval(run(X_506,P_507),E2_503) ),
inference(demodulation,[status(thm),theory(equality)],[c_132,c_1058]) ).
tff(c_46896,plain,
! [Q2_1252,R_1251,E2_1248,Z_1253,X_1250,E_1249] :
( ( run(del(Z_1253,X_1250),ifThenElse(E2_1248,R_1251,Q2_1252)) = run(X_1250,seq(assign(Z_1253,E_1249),Q2_1252)) )
| eval(run(X_1250,assign(Z_1253,E_1249)),E2_1248)
| eval(X_1250,E_1249) ),
inference(superposition,[status(thm),theory(equality)],[c_595,c_4933]) ).
tff(c_196159,plain,
! [Z_3316,E2_3318,X_3317,E_3319,R_3315] :
( ( run(del(Z_3316,X_3317),ifThenElse(E2_3318,R_3315,skip)) = run(X_3317,assign(Z_3316,E_3319)) )
| eval(run(X_3317,assign(Z_3316,E_3319)),E2_3318)
| eval(X_3317,E_3319) ),
inference(superposition,[status(thm),theory(equality)],[c_463,c_46896]) ).
tff(c_197053,plain,
! [Z_911,E2_3318,R_3315] :
( ( run(del(Z_911,nil),ifThenElse(E2_3318,R_3315,skip)) = run(nil,assign(Z_911,fF)) )
| eval(nil,E2_3318)
| eval(nil,fF) ),
inference(superposition,[status(thm),theory(equality)],[c_27646,c_196159]) ).
tff(c_197217,plain,
! [E2_3318,R_3315] :
( ( run(nil,ifThenElse(E2_3318,R_3315,skip)) = nil )
| eval(nil,E2_3318)
| eval(nil,fF) ),
inference(demodulation,[status(thm),theory(equality)],[c_120,c_120,c_133920,c_197053]) ).
tff(c_197218,plain,
! [E2_3318,R_3315] :
( ( run(nil,ifThenElse(E2_3318,R_3315,skip)) = nil )
| eval(nil,E2_3318) ),
inference(negUnitSimplification,[status(thm)],[c_114,c_197217]) ).
tff(c_761,plain,
! [X_268,E2_269,R_270,Q2_271] :
( ( run(X_268,ifThenElse(E2_269,R_270,Q2_271)) = run(X_268,R_270) )
| ~ eval(X_268,E2_269) ),
inference(cnfTransformation,[status(thm)],[f_194]) ).
tff(c_767,plain,
! [Q_106,R_270,X_268,Q2_271,E2_269] :
( ( run(X_268,seq(ifThenElse(E2_269,R_270,Q2_271),Q_106)) = run(run(X_268,R_270),Q_106) )
| ~ eval(X_268,E2_269) ),
inference(superposition,[status(thm),theory(equality)],[c_761,c_132]) ).
tff(c_788,plain,
! [Q_106,R_270,X_268,Q2_271,E2_269] :
( ( run(X_268,seq(ifThenElse(E2_269,R_270,Q2_271),Q_106)) = run(X_268,seq(R_270,Q_106)) )
| ~ eval(X_268,E2_269) ),
inference(demodulation,[status(thm),theory(equality)],[c_132,c_767]) ).
tff(c_2481,plain,
! [X_422,P_423,Z_424,E_425] :
( ( run(X_422,seq(P_423,assign(Z_424,E_425))) = cons(Z_424,run(X_422,P_423)) )
| ~ eval(run(X_422,P_423),E_425) ),
inference(superposition,[status(thm),theory(equality)],[c_514,c_132]) ).
tff(c_63144,plain,
! [E2_1468,Z_1469,Q2_1467,R_1470,X_1471,E_1472] :
( ( run(X_1471,seq(R_1470,assign(Z_1469,E_1472))) = cons(Z_1469,run(X_1471,ifThenElse(E2_1468,R_1470,Q2_1467))) )
| ~ eval(run(X_1471,ifThenElse(E2_1468,R_1470,Q2_1467)),E_1472)
| ~ eval(X_1471,E2_1468) ),
inference(superposition,[status(thm),theory(equality)],[c_788,c_2481]) ).
tff(c_144457,plain,
! [E2_2656,X_2659,R_2660,Z_2657,Q2_2658] :
( ( run(X_2659,seq(R_2660,assign(Z_2657,tT))) = cons(Z_2657,run(X_2659,ifThenElse(E2_2656,R_2660,Q2_2658))) )
| ~ eval(X_2659,E2_2656) ),
inference(resolution,[status(thm)],[c_112,c_63144]) ).
tff(c_82,plain,
! [P_74,Q_75] :
( typeCorrect(seq(P_74,Q_75))
| ~ typeCorrect(Q_75)
| ~ typeCorrect(P_74) ),
inference(cnfTransformation,[status(thm)],[f_132]) ).
tff(c_520,plain,
! [X_250,Z_251,E_252,Q_106] :
( ( run(X_250,seq(assign(Z_251,E_252),Q_106)) = run(cons(Z_251,X_250),Q_106) )
| ~ eval(X_250,E_252) ),
inference(superposition,[status(thm),theory(equality)],[c_514,c_132]) ).
tff(c_27759,plain,
! [E_920,Z_921,E_919,X_917,Z_918] :
( ( run(cons(Z_921,X_917),assign(Z_918,E_920)) = cons(Z_918,run(X_917,assign(Z_921,E_919))) )
| ~ eval(run(X_917,assign(Z_921,E_919)),E_920)
| ~ eval(X_917,E_919) ),
inference(superposition,[status(thm),theory(equality)],[c_520,c_2481]) ).
tff(c_30676,plain,
! [Z_963,X_964,Z_965,E_966] :
( ( run(cons(Z_963,X_964),assign(Z_965,tT)) = cons(Z_965,run(X_964,assign(Z_963,E_966))) )
| ~ eval(X_964,E_966) ),
inference(resolution,[status(thm)],[c_112,c_27759]) ).
tff(c_128,plain,
! [X_98,Z_99,E_100] :
( ( run(X_98,assign(Z_99,E_100)) = cons(Z_99,X_98) )
| ~ eval(X_98,E_100) ),
inference(cnfTransformation,[status(thm)],[f_183]) ).
tff(c_7710,plain,
! [S_571] : elem(l,run(S_571,assign(l,tT))),
inference(splitRight,[status(thm)],[c_7701]) ).
tff(c_102,plain,
! [X_80,Xs_82,Z_81] :
( ~ elem(X_80,Xs_82)
| elem(X_80,cons(Z_81,Xs_82)) ),
inference(cnfTransformation,[status(thm)],[f_149]) ).
tff(c_140,plain,
! [S_116,P_115] :
( elem(l,run(cons(h,S_116),P_115))
| ~ elem(l,run(S_116,P_115))
| ~ typeCorrect(P_115) ),
inference(cnfTransformation,[status(thm)],[f_207]) ).
tff(c_620,plain,
! [Z_258,S_259,E_260] :
( elem(l,cons(Z_258,cons(h,S_259)))
| ~ elem(l,run(S_259,assign(Z_258,E_260)))
| ~ typeCorrect(assign(Z_258,E_260))
| ~ eval(cons(h,S_259),E_260) ),
inference(superposition,[status(thm),theory(equality)],[c_514,c_140]) ).
tff(c_4518,plain,
! [Z_492,S_493,E_494] :
( elem(l,cons(Z_492,cons(h,cons(h,S_493))))
| ~ eval(cons(h,cons(h,S_493)),E_494)
| ~ elem(l,run(S_493,assign(Z_492,E_494)))
| ~ typeCorrect(assign(Z_492,E_494)) ),
inference(resolution,[status(thm)],[c_140,c_620]) ).
tff(c_9923,plain,
! [Z_633,S_634] :
( elem(l,cons(Z_633,cons(h,cons(h,S_634))))
| ~ elem(l,run(S_634,assign(Z_633,tT)))
| ~ typeCorrect(assign(Z_633,tT)) ),
inference(resolution,[status(thm)],[c_112,c_4518]) ).
tff(c_100,plain,
! [X_80,Xs_82,Z_81] :
( elem(X_80,Xs_82)
| ( Z_81 = X_80 )
| ~ elem(X_80,cons(Z_81,Xs_82)) ),
inference(cnfTransformation,[status(thm)],[f_149]) ).
tff(c_15502,plain,
! [S_712,Z_713] :
( elem(l,cons(h,cons(h,S_712)))
| ( l = Z_713 )
| ~ elem(l,run(S_712,assign(Z_713,tT)))
| ~ typeCorrect(assign(Z_713,tT)) ),
inference(resolution,[status(thm)],[c_9923,c_100]) ).
tff(c_15545,plain,
! [X_98,Z_99] :
( elem(l,cons(h,cons(h,X_98)))
| ( l = Z_99 )
| ~ elem(l,cons(Z_99,X_98))
| ~ typeCorrect(assign(Z_99,tT))
| ~ eval(X_98,tT) ),
inference(superposition,[status(thm),theory(equality)],[c_128,c_15502]) ).
tff(c_15573,plain,
! [X_714,Z_715] :
( elem(l,cons(h,cons(h,X_714)))
| ( l = Z_715 )
| ~ elem(l,cons(Z_715,X_714))
| ~ typeCorrect(assign(Z_715,tT)) ),
inference(demodulation,[status(thm),theory(equality)],[c_112,c_15545]) ).
tff(c_15595,plain,
! [Xs_82,Z_81] :
( elem(l,cons(h,cons(h,Xs_82)))
| ( l = Z_81 )
| ~ typeCorrect(assign(Z_81,tT))
| ~ elem(l,Xs_82) ),
inference(resolution,[status(thm)],[c_102,c_15573]) ).
tff(c_15601,plain,
! [Xs_716] :
( elem(l,cons(h,cons(h,Xs_716)))
| ~ elem(l,Xs_716) ),
inference(splitLeft,[status(thm)],[c_15595]) ).
tff(c_15571,plain,
! [X_98,Z_99] :
( elem(l,cons(h,cons(h,X_98)))
| ( l = Z_99 )
| ~ elem(l,cons(Z_99,X_98))
| ~ typeCorrect(assign(Z_99,tT)) ),
inference(demodulation,[status(thm),theory(equality)],[c_112,c_15545]) ).
tff(c_15603,plain,
! [Xs_716] :
( elem(l,cons(h,cons(h,cons(h,Xs_716))))
| ( l = h )
| ~ typeCorrect(assign(h,tT))
| ~ elem(l,Xs_716) ),
inference(resolution,[status(thm)],[c_15601,c_15571]) ).
tff(c_15618,plain,
! [Xs_716] :
( elem(l,cons(h,cons(h,cons(h,Xs_716))))
| ( l = h )
| ~ elem(l,Xs_716) ),
inference(demodulation,[status(thm),theory(equality)],[c_298,c_15603]) ).
tff(c_15627,plain,
! [Xs_717] :
( elem(l,cons(h,cons(h,cons(h,Xs_717))))
| ~ elem(l,Xs_717) ),
inference(negUnitSimplification,[status(thm)],[c_181,c_15618]) ).
tff(c_871,plain,
! [S_116,Z_278,E_279] :
( elem(l,run(S_116,assign(Z_278,E_279)))
| ~ elem(l,cons(Z_278,cons(h,cons(h,S_116))))
| ~ typeCorrect(assign(Z_278,E_279))
| ~ eval(cons(h,cons(h,S_116)),E_279) ),
inference(resolution,[status(thm)],[c_852,c_138]) ).
tff(c_15633,plain,
! [Xs_717,E_279] :
( elem(l,run(Xs_717,assign(h,E_279)))
| ~ typeCorrect(assign(h,E_279))
| ~ eval(cons(h,cons(h,Xs_717)),E_279)
| ~ elem(l,Xs_717) ),
inference(resolution,[status(thm)],[c_15627,c_871]) ).
tff(c_16566,plain,
! [Xs_734,E_735] :
( elem(l,run(Xs_734,assign(h,E_735)))
| ~ eval(cons(h,cons(h,Xs_734)),E_735)
| ~ elem(l,Xs_734) ),
inference(demodulation,[status(thm),theory(equality)],[c_298,c_15633]) ).
tff(c_16659,plain,
! [Xs_736] :
( elem(l,run(Xs_736,assign(h,tT)))
| ~ elem(l,Xs_736) ),
inference(resolution,[status(thm)],[c_112,c_16566]) ).
tff(c_16913,plain,
! [X_738,P_739] :
( elem(l,run(X_738,seq(P_739,assign(h,tT))))
| ~ elem(l,run(X_738,P_739)) ),
inference(superposition,[status(thm),theory(equality)],[c_132,c_16659]) ).
tff(c_23498,plain,
! [Z_830,X_831,E_832] :
( elem(l,run(cons(Z_830,X_831),assign(h,tT)))
| ~ elem(l,run(X_831,assign(Z_830,E_832)))
| ~ eval(X_831,E_832) ),
inference(superposition,[status(thm),theory(equality)],[c_520,c_16913]) ).
tff(c_23552,plain,
! [S_571] :
( elem(l,run(cons(l,S_571),assign(h,tT)))
| ~ eval(S_571,tT) ),
inference(resolution,[status(thm)],[c_7710,c_23498]) ).
tff(c_23639,plain,
! [S_833] : elem(l,run(cons(l,S_833),assign(h,tT))),
inference(demodulation,[status(thm),theory(equality)],[c_112,c_23552]) ).
tff(c_23675,plain,
! [S_833] :
( elem(l,cons(h,cons(l,S_833)))
| ~ eval(cons(l,S_833),tT) ),
inference(superposition,[status(thm),theory(equality)],[c_128,c_23639]) ).
tff(c_23712,plain,
! [S_833] : elem(l,cons(h,cons(l,S_833))),
inference(demodulation,[status(thm),theory(equality)],[c_112,c_23675]) ).
tff(c_32352,plain,
! [Z_998,X_999,E_1000] :
( elem(l,cons(h,run(cons(Z_998,X_999),assign(l,tT))))
| ~ eval(X_999,E_1000) ),
inference(superposition,[status(thm),theory(equality)],[c_30676,c_23712]) ).
tff(c_32456,plain,
! [Z_1001,X_1002] : elem(l,cons(h,run(cons(Z_1001,X_1002),assign(l,tT)))),
inference(resolution,[status(thm)],[c_112,c_32352]) ).
tff(c_32464,plain,
! [Z_1001,X_1002] :
( elem(l,cons(h,cons(h,run(cons(Z_1001,X_1002),assign(l,tT)))))
| ( l = h )
| ~ typeCorrect(assign(h,tT)) ),
inference(resolution,[status(thm)],[c_32456,c_15571]) ).
tff(c_32491,plain,
! [Z_1001,X_1002] :
( elem(l,cons(h,cons(h,run(cons(Z_1001,X_1002),assign(l,tT)))))
| ( l = h ) ),
inference(demodulation,[status(thm),theory(equality)],[c_298,c_32464]) ).
tff(c_32526,plain,
! [Z_1006,X_1007] : elem(l,cons(h,cons(h,run(cons(Z_1006,X_1007),assign(l,tT))))),
inference(negUnitSimplification,[status(thm)],[c_181,c_32491]) ).
tff(c_32542,plain,
! [Z_1006,X_1007] :
( elem(l,cons(h,cons(h,cons(h,run(cons(Z_1006,X_1007),assign(l,tT))))))
| ( l = h )
| ~ typeCorrect(assign(h,tT)) ),
inference(resolution,[status(thm)],[c_32526,c_15571]) ).
tff(c_32576,plain,
! [Z_1006,X_1007] :
( elem(l,cons(h,cons(h,cons(h,run(cons(Z_1006,X_1007),assign(l,tT))))))
| ( l = h ) ),
inference(demodulation,[status(thm),theory(equality)],[c_298,c_32542]) ).
tff(c_34283,plain,
! [Z_1032,X_1033] : elem(l,cons(h,cons(h,cons(h,run(cons(Z_1032,X_1033),assign(l,tT)))))),
inference(negUnitSimplification,[status(thm)],[c_181,c_32576]) ).
tff(c_16729,plain,
! [S_116] :
( elem(l,run(S_116,assign(h,tT)))
| ~ typeCorrect(assign(h,tT))
| ~ elem(l,cons(h,S_116)) ),
inference(resolution,[status(thm)],[c_16659,c_138]) ).
tff(c_16786,plain,
! [S_737] :
( elem(l,run(S_737,assign(h,tT)))
| ~ elem(l,cons(h,S_737)) ),
inference(demodulation,[status(thm),theory(equality)],[c_298,c_16729]) ).
tff(c_16856,plain,
! [S_116] :
( elem(l,run(S_116,assign(h,tT)))
| ~ typeCorrect(assign(h,tT))
| ~ elem(l,cons(h,cons(h,S_116))) ),
inference(resolution,[status(thm)],[c_16786,c_138]) ).
tff(c_17244,plain,
! [S_742] :
( elem(l,run(S_742,assign(h,tT)))
| ~ elem(l,cons(h,cons(h,S_742))) ),
inference(demodulation,[status(thm),theory(equality)],[c_298,c_16856]) ).
tff(c_17314,plain,
! [S_116] :
( elem(l,run(S_116,assign(h,tT)))
| ~ typeCorrect(assign(h,tT))
| ~ elem(l,cons(h,cons(h,cons(h,S_116)))) ),
inference(resolution,[status(thm)],[c_17244,c_138]) ).
tff(c_17367,plain,
! [S_116] :
( elem(l,run(S_116,assign(h,tT)))
| ~ elem(l,cons(h,cons(h,cons(h,S_116)))) ),
inference(demodulation,[status(thm),theory(equality)],[c_298,c_17314]) ).
tff(c_34296,plain,
! [Z_1032,X_1033] : elem(l,run(run(cons(Z_1032,X_1033),assign(l,tT)),assign(h,tT))),
inference(resolution,[status(thm)],[c_34283,c_17367]) ).
tff(c_34367,plain,
! [Z_1034,X_1035] : elem(l,run(cons(Z_1034,X_1035),seq(assign(l,tT),assign(h,tT)))),
inference(demodulation,[status(thm),theory(equality)],[c_132,c_34296]) ).
tff(c_34471,plain,
! [X_1035] :
( elem(l,run(X_1035,seq(assign(l,tT),assign(h,tT))))
| ~ typeCorrect(seq(assign(l,tT),assign(h,tT))) ),
inference(resolution,[status(thm)],[c_34367,c_138]) ).
tff(c_36042,plain,
~ typeCorrect(seq(assign(l,tT),assign(h,tT))),
inference(splitLeft,[status(thm)],[c_34471]) ).
tff(c_36045,plain,
( ~ typeCorrect(assign(h,tT))
| ~ typeCorrect(assign(l,tT)) ),
inference(resolution,[status(thm)],[c_82,c_36042]) ).
tff(c_36049,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_7711,c_298,c_36045]) ).
tff(c_36050,plain,
! [X_1035] : elem(l,run(X_1035,seq(assign(l,tT),assign(h,tT)))),
inference(splitRight,[status(thm)],[c_34471]) ).
tff(c_227332,plain,
! [X_3659,E2_3660,Q2_3661] :
( elem(l,cons(h,run(X_3659,ifThenElse(E2_3660,assign(l,tT),Q2_3661))))
| ~ eval(X_3659,E2_3660) ),
inference(superposition,[status(thm),theory(equality)],[c_144457,c_36050]) ).
tff(c_227362,plain,
! [X_3659,E2_3660,Q2_3661] :
( elem(l,run(X_3659,ifThenElse(E2_3660,assign(l,tT),Q2_3661)))
| ( l = h )
| ~ eval(X_3659,E2_3660) ),
inference(resolution,[status(thm)],[c_227332,c_100]) ).
tff(c_227475,plain,
! [X_3662,E2_3663,Q2_3664] :
( elem(l,run(X_3662,ifThenElse(E2_3663,assign(l,tT),Q2_3664)))
| ~ eval(X_3662,E2_3663) ),
inference(negUnitSimplification,[status(thm)],[c_181,c_227362]) ).
tff(c_231424,plain,
! [S_3687,E2_3688,Q2_3689] :
( elem(l,run(S_3687,ifThenElse(E2_3688,assign(l,tT),Q2_3689)))
| ~ typeCorrect(ifThenElse(E2_3688,assign(l,tT),Q2_3689))
| ~ eval(cons(h,S_3687),E2_3688) ),
inference(resolution,[status(thm)],[c_227475,c_138]) ).
tff(c_231593,plain,
! [E2_3318] :
( elem(l,nil)
| ~ typeCorrect(ifThenElse(E2_3318,assign(l,tT),skip))
| ~ eval(cons(h,nil),E2_3318)
| eval(nil,E2_3318) ),
inference(superposition,[status(thm),theory(equality)],[c_197218,c_231424]) ).
tff(c_231739,plain,
! [E2_3690] :
( ~ typeCorrect(ifThenElse(E2_3690,assign(l,tT),skip))
| ~ eval(cons(h,nil),E2_3690)
| eval(nil,E2_3690) ),
inference(negUnitSimplification,[status(thm)],[c_98,c_231593]) ).
tff(c_231743,plain,
! [C_76] :
( ~ eval(cons(h,nil),C_76)
| eval(nil,C_76)
| ~ typeCorrect(skip)
| ~ typeCorrect(assign(l,tT)) ),
inference(resolution,[status(thm)],[c_88,c_231739]) ).
tff(c_231747,plain,
! [C_3691] :
( ~ eval(cons(h,nil),C_3691)
| eval(nil,C_3691) ),
inference(demodulation,[status(thm),theory(equality)],[c_7711,c_74,c_231743]) ).
tff(c_231962,plain,
! [Z_3692] :
( eval(nil,var(Z_3692))
| ~ elem(Z_3692,cons(h,nil)) ),
inference(resolution,[status(thm)],[c_118,c_231747]) ).
tff(c_231996,plain,
! [Z_3692] :
( elem(Z_3692,nil)
| ~ elem(Z_3692,cons(h,nil)) ),
inference(resolution,[status(thm)],[c_231962,c_116]) ).
tff(c_232039,plain,
! [Z_3693] : ~ elem(Z_3693,cons(h,nil)),
inference(negUnitSimplification,[status(thm)],[c_98,c_231996]) ).
tff(c_232090,plain,
$false,
inference(resolution,[status(thm)],[c_104,c_232039]) ).
tff(c_232092,plain,
! [Z_3694] :
( ( l = Z_3694 )
| ~ typeCorrect(assign(Z_3694,tT)) ),
inference(splitRight,[status(thm)],[c_15595]) ).
tff(c_232107,plain,
l = h,
inference(resolution,[status(thm)],[c_298,c_232092]) ).
tff(c_232124,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_181,c_232107]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SWX240_1 : TPTP v9.3.0. Released v9.3.0.
% 0.12/0.13 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% 0.16/0.33 % Computer : n022.cluster.edu
% 0.16/0.33 % Model : x86_64 x86_64
% 0.16/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.33 % Memory : 8042.1875MB
% 0.16/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.33 % CPULimit : 300
% 0.16/0.33 % WCLimit : 300
% 0.16/0.33 % DateTime : Tue May 5 13:23:36 EDT 2026
% 0.16/0.34 % CPUTime :
% 90.79/54.47 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 90.79/54.49
% 90.79/54.49 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------