%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : SWX240_1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n026.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 07:07:29 PM UTC 2026
% Result : Theorem 8.73s 8.92s
% Output : Refutation 8.73s
% Verified :
% SZS Type : Refutation
% Derivation depth : 29
% Number of leaves : 29
% Syntax : Number of clauses : 98 ( 24 unt; 53 nHn; 98 RR)
% Number of literals : 282 ( 0 equ; 129 neg)
% Maximal clause size : 6 ( 2 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 6 ( 5 usr; 1 prp; 0-2 aty)
% Number of functors : 22 ( 22 usr; 11 con; 0-3 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(1,axiom,
typeCorrect(skip),
file('SWX240_1.p',unknown),
[] ).
cnf(2,axiom,
eval(u,tT),
file('SWX240_1.p',unknown),
[] ).
cnf(3,axiom,
~ equal(fF,tT),
file('SWX240_1.p',unknown),
[] ).
cnf(5,axiom,
equal(low(zero),l),
file('SWX240_1.p',unknown),
[] ).
cnf(7,axiom,
~ elem(u,nil),
file('SWX240_1.p',unknown),
[] ).
cnf(8,axiom,
~ eval(u,fF),
file('SWX240_1.p',unknown),
[] ).
cnf(14,axiom,
~ equal(var(u),tT),
file('SWX240_1.p',unknown),
[] ).
cnf(15,axiom,
~ equal(var(u),fF),
file('SWX240_1.p',unknown),
[] ).
cnf(19,axiom,
equal(run(u,skip),u),
file('SWX240_1.p',unknown),
[] ).
cnf(24,axiom,
equal(proj1Nand(nand__dfg(u,v)),u),
file('SWX240_1.p',unknown),
[] ).
cnf(25,axiom,
equal(proj2Nand(nand__dfg(u,v)),v),
file('SWX240_1.p',unknown),
[] ).
cnf(26,axiom,
~ equal(nand__dfg(u,v),tT),
file('SWX240_1.p',unknown),
[] ).
cnf(27,axiom,
~ equal(nand__dfg(u,v),fF),
file('SWX240_1.p',unknown),
[] ).
cnf(34,axiom,
~ equal(nand__dfg(u,v),var(w)),
file('SWX240_1.p',unknown),
[] ).
cnf(41,axiom,
( secret(u)
| typeCorrect(assign(low(v),u)) ),
file('SWX240_1.p',unknown),
[] ).
cnf(48,axiom,
( eval(u,v)
| eval(u,nand__dfg(w,v)) ),
file('SWX240_1.p',unknown),
[] ).
cnf(49,axiom,
( ~ eval(u,var(v))
| elem(v,u) ),
file('SWX240_1.p',unknown),
[] ).
cnf(50,axiom,
( ~ elem(u,v)
| eval(v,var(u)) ),
file('SWX240_1.p',unknown),
[] ).
cnf(53,axiom,
( ~ secret(nand__dfg(u,v))
| secret(u)
| secret(v) ),
file('SWX240_1.p',unknown),
[] ).
cnf(55,axiom,
( ~ equal(u,v)
| elem(v,cons(u,w)) ),
file('SWX240_1.p',unknown),
[] ).
cnf(59,axiom,
( ~ typeCorrect(u)
| ~ typeCorrect(v)
| typeCorrect(ifThenElse(w,u,v)) ),
file('SWX240_1.p',unknown),
[] ).
cnf(62,axiom,
( eval(u,v)
| equal(run(u,assign(w,v)),del(w,u)) ),
file('SWX240_1.p',unknown),
[] ).
cnf(63,axiom,
( ~ eval(u,v)
| equal(run(u,assign(w,v)),cons(w,u)) ),
file('SWX240_1.p',unknown),
[] ).
cnf(64,axiom,
( eval(u,v)
| equal(run(u,ifThenElse(v,w,x)),run(u,x)) ),
file('SWX240_1.p',unknown),
[] ).
cnf(65,axiom,
( ~ eval(u,v)
| ~ eval(u,w)
| ~ eval(u,nand__dfg(v,w)) ),
file('SWX240_1.p',unknown),
[] ).
cnf(67,axiom,
( ~ eval(u,v)
| equal(run(u,ifThenElse(v,w,x)),run(u,w)) ),
file('SWX240_1.p',unknown),
[] ).
cnf(68,axiom,
( ~ secret(u)
| equal(var(proj1Var(u)),u)
| equal(nand__dfg(proj1Nand(u),proj2Nand(u)),u) ),
file('SWX240_1.p',unknown),
[] ).
cnf(69,axiom,
( ~ typeCorrect(u)
| ~ elem(l,run(v,u))
| elem(l,run(cons(h,v),u)) ),
file('SWX240_1.p',unknown),
[] ).
cnf(70,axiom,
( ~ typeCorrect(u)
| ~ elem(l,run(cons(h,v),u))
| elem(l,run(v,u)) ),
file('SWX240_1.p',unknown),
[] ).
cnf(102,plain,
( secret(u)
| typeCorrect(assign(l,u)) ),
inference(spr,[status(thm),theory(equality)],[5,41]),
[iquote('0:SpR:5.0,41.1')] ).
cnf(186,plain,
( ~ secret(u)
| ~ equal(u,fF)
| equal(var(proj1Var(u)),u) ),
inference(spl,[status(thm),theory(equality)],[68,27]),
[iquote('0:SpL:68.2,27.0')] ).
cnf(187,plain,
( ~ secret(u)
| ~ equal(u,tT)
| equal(var(proj1Var(u)),u) ),
inference(spl,[status(thm),theory(equality)],[68,26]),
[iquote('0:SpL:68.2,26.0')] ).
cnf(188,plain,
( ~ secret(u)
| ~ secret(u)
| equal(var(proj1Var(u)),u)
| secret(proj1Nand(u))
| secret(proj2Nand(u)) ),
inference(spl,[status(thm),theory(equality)],[68,53]),
[iquote('0:SpL:68.2,53.0')] ).
cnf(191,plain,
( ~ secret(u)
| equal(var(proj1Var(u)),u)
| secret(proj1Nand(u))
| secret(proj2Nand(u)) ),
inference(obv,[status(thm),theory(equality)],[188]),
[iquote('0:Obv:188.0')] ).
cnf(198,plain,
( ~ secret(u)
| ~ equal(u,fF)
| ~ equal(u,fF) ),
inference(spl,[status(thm),theory(equality)],[186,15]),
[iquote('0:SpL:186.2,15.0')] ).
cnf(202,plain,
( ~ secret(u)
| ~ equal(u,fF) ),
inference(obv,[status(thm),theory(equality)],[198]),
[iquote('0:Obv:198.1')] ).
cnf(213,plain,
( ~ typeCorrect(assign(u,v))
| ~ elem(l,run(w,assign(u,v)))
| eval(cons(h,w),v)
| elem(l,del(u,cons(h,w))) ),
inference(spr,[status(thm),theory(equality)],[62,69]),
[iquote('0:SpR:62.1,69.2')] ).
cnf(226,plain,
( ~ secret(u)
| ~ equal(u,tT)
| ~ equal(u,tT) ),
inference(spl,[status(thm),theory(equality)],[187,14]),
[iquote('0:SpL:187.2,14.0')] ).
cnf(229,plain,
( ~ secret(u)
| ~ equal(u,tT) ),
inference(obv,[status(thm),theory(equality)],[226]),
[iquote('0:Obv:226.1')] ).
cnf(242,plain,
( ~ secret(u)
| ~ equal(nand__dfg(v,w),u)
| secret(proj1Nand(u))
| secret(proj2Nand(u)) ),
inference(spl,[status(thm),theory(equality)],[191,34]),
[iquote('0:SpL:191.1,34.0')] ).
cnf(250,plain,
( ~ typeCorrect(assign(u,v))
| ~ eval(cons(h,w),v)
| ~ elem(l,cons(u,cons(h,w)))
| elem(l,run(w,assign(u,v))) ),
inference(spl,[status(thm),theory(equality)],[63,70]),
[iquote('0:SpL:63.1,70.1')] ).
cnf(251,plain,
( ~ typeCorrect(assign(u,v))
| ~ elem(l,del(u,cons(h,w)))
| eval(cons(h,w),v)
| elem(l,run(w,assign(u,v))) ),
inference(spl,[status(thm),theory(equality)],[62,70]),
[iquote('0:SpL:62.1,70.1')] ).
cnf(253,plain,
( ~ typeCorrect(ifThenElse(u,v,w))
| ~ elem(l,run(cons(h,x),w))
| eval(cons(h,x),u)
| elem(l,run(x,ifThenElse(u,v,w))) ),
inference(spl,[status(thm),theory(equality)],[64,70]),
[iquote('0:SpL:64.1,70.1')] ).
cnf(280,plain,
( ~ equal(proj2Nand(u),fF)
| ~ equal(nand__dfg(v,w),u)
| ~ secret(u)
| secret(proj1Nand(u)) ),
inference(ems,[status(thm)],[202,242]),
[iquote('0:EmS:202.0,242.3')] ).
cnf(382,plain,
( ~ equal(proj1Nand(u),tT)
| ~ secret(u)
| ~ equal(nand__dfg(v,w),u)
| ~ equal(proj2Nand(u),fF) ),
inference(ems,[status(thm)],[229,280]),
[iquote('0:EmS:229.0,280.3')] ).
cnf(570,plain,
( ~ elem(l,run(u,assign(l,v)))
| eval(cons(h,u),v)
| elem(l,del(l,cons(h,u)))
| secret(v) ),
inference(sor,[status(thm)],[213,102]),
[iquote('0:SoR:213.0,102.1')] ).
cnf(625,plain,
( ~ elem(l,del(l,cons(h,u)))
| eval(cons(h,u),v)
| elem(l,run(u,assign(l,v)))
| secret(v) ),
inference(sor,[status(thm)],[251,102]),
[iquote('0:SoR:251.0,102.1')] ).
cnf(673,plain,
( ~ eval(cons(h,u),v)
| ~ elem(l,cons(l,cons(h,u)))
| elem(l,run(u,assign(l,v)))
| secret(v) ),
inference(sor,[status(thm)],[250,102]),
[iquote('0:SoR:250.0,102.1')] ).
cnf(696,plain,
( ~ equal(proj1Nand(nand__dfg(u,v)),tT)
| ~ secret(nand__dfg(u,v))
| ~ equal(proj2Nand(nand__dfg(u,v)),fF) ),
inference(eqr,[status(thm),theory(equality)],[382]),
[iquote('0:EqR:382.2')] ).
cnf(698,plain,
( ~ equal(u,tT)
| ~ secret(nand__dfg(u,v))
| ~ equal(v,fF) ),
inference(rew,[status(thm),theory(equality)],[25,696,24]),
[iquote('0:Rew:25.0,696.2,24.0,696.0')] ).
cnf(744,plain,
( ~ typeCorrect(u)
| ~ typeCorrect(v)
| ~ elem(l,run(cons(h,w),u))
| eval(cons(h,w),x)
| elem(l,run(w,ifThenElse(x,v,u))) ),
inference(sor,[status(thm)],[253,59]),
[iquote('0:SoR:253.0,59.2')] ).
cnf(991,plain,
( ~ eval(u,v)
| ~ elem(l,cons(l,u))
| eval(cons(h,u),v)
| elem(l,del(l,cons(h,u)))
| secret(v) ),
inference(spl,[status(thm),theory(equality)],[63,570]),
[iquote('0:SpL:63.1,570.0')] ).
cnf(1019,plain,
( ~ eval(u,v)
| ~ elem(l,del(l,cons(h,u)))
| eval(cons(h,u),v)
| elem(l,cons(l,u))
| secret(v) ),
inference(spr,[status(thm),theory(equality)],[63,625]),
[iquote('0:SpR:63.1,625.2')] ).
cnf(1022,plain,
( ~ typeCorrect(assign(l,u))
| ~ elem(l,del(l,cons(h,cons(h,v))))
| eval(cons(h,cons(h,v)),u)
| secret(u)
| elem(l,run(v,assign(l,u))) ),
inference(res,[status(thm),theory(equality)],[625,70]),
[iquote('0:Res:625.2,70.1')] ).
cnf(1024,plain,
( ~ elem(l,del(l,cons(h,cons(h,u))))
| eval(cons(h,cons(h,u)),v)
| secret(v)
| elem(l,run(u,assign(l,v))) ),
inference(mrr,[status(thm)],[1022,102]),
[iquote('0:MRR:1022.0,102.1')] ).
cnf(1290,plain,
( ~ eval(u,v)
| ~ eval(cons(h,u),v)
| ~ elem(l,cons(l,cons(h,u)))
| elem(l,cons(l,u))
| secret(v) ),
inference(spr,[status(thm),theory(equality)],[63,673]),
[iquote('0:SpR:63.1,673.2')] ).
cnf(1291,plain,
( ~ eval(cons(h,u),v)
| ~ elem(l,cons(l,cons(h,u)))
| eval(u,v)
| elem(l,del(l,u))
| secret(v) ),
inference(spr,[status(thm),theory(equality)],[62,673]),
[iquote('0:SpR:62.1,673.2')] ).
cnf(1295,plain,
( ~ typeCorrect(assign(l,u))
| ~ eval(cons(h,cons(h,v)),u)
| ~ elem(l,cons(l,cons(h,cons(h,v))))
| secret(u)
| elem(l,run(v,assign(l,u))) ),
inference(res,[status(thm),theory(equality)],[673,70]),
[iquote('0:Res:673.2,70.1')] ).
cnf(1298,plain,
( ~ eval(cons(h,cons(h,u)),v)
| ~ elem(l,cons(l,cons(h,cons(h,u))))
| secret(v)
| elem(l,run(u,assign(l,v))) ),
inference(mrr,[status(thm)],[1295,102]),
[iquote('0:MRR:1295.0,102.1')] ).
cnf(2198,plain,
( ~ typeCorrect(u)
| ~ typeCorrect(v)
| ~ eval(w,x)
| ~ elem(l,run(cons(h,w),u))
| eval(cons(h,w),x)
| elem(l,run(w,v)) ),
inference(spr,[status(thm),theory(equality)],[67,744]),
[iquote('0:SpR:67.1,744.4')] ).
cnf(2596,plain,
( ~ equal(l,l)
| ~ eval(u,v)
| eval(cons(h,u),v)
| elem(l,del(l,cons(h,u)))
| secret(v) ),
inference(res,[status(thm),theory(equality)],[55,991]),
[iquote('0:Res:55.1,991.1')] ).
cnf(2612,plain,
( ~ eval(u,v)
| eval(cons(h,u),v)
| elem(l,del(l,cons(h,u)))
| secret(v) ),
inference(obv,[status(thm),theory(equality)],[2596]),
[iquote('0:Obv:2596.0')] ).
cnf(2616,plain,
( ~ eval(u,v)
| eval(cons(h,u),v)
| elem(l,cons(l,u))
| secret(v) ),
inference(mrr,[status(thm)],[1019,2612]),
[iquote('0:MRR:1019.1,2612.2')] ).
cnf(2617,plain,
( ~ eval(u,v)
| ~ elem(l,cons(l,cons(h,u)))
| elem(l,cons(l,u))
| secret(v) ),
inference(mrr,[status(thm)],[1290,2616]),
[iquote('0:MRR:1290.1,2616.1')] ).
cnf(2699,plain,
( ~ equal(l,l)
| ~ eval(u,v)
| elem(l,cons(l,u))
| secret(v) ),
inference(res,[status(thm),theory(equality)],[55,2617]),
[iquote('0:Res:55.1,2617.1')] ).
cnf(2705,plain,
( ~ eval(u,v)
| elem(l,cons(l,u))
| secret(v) ),
inference(obv,[status(thm),theory(equality)],[2699]),
[iquote('0:Obv:2699.0')] ).
cnf(2707,plain,
( ~ eval(cons(h,u),v)
| eval(u,v)
| elem(l,del(l,u))
| secret(v) ),
inference(mrr,[status(thm)],[1291,2705]),
[iquote('0:MRR:1291.1,2705.1')] ).
cnf(2713,plain,
( ~ eval(cons(h,cons(h,u)),v)
| secret(v)
| elem(l,run(u,assign(l,v))) ),
inference(mrr,[status(thm)],[1298,2705]),
[iquote('0:MRR:1298.1,2705.1')] ).
cnf(2716,plain,
( ~ elem(l,del(l,cons(h,cons(h,u))))
| secret(v)
| elem(l,run(u,assign(l,v))) ),
inference(mrr,[status(thm)],[1024,2713]),
[iquote('0:MRR:1024.1,2713.0')] ).
cnf(2776,plain,
( eval(cons(h,u),v)
| eval(u,nand__dfg(w,v))
| elem(l,del(l,u))
| secret(nand__dfg(w,v)) ),
inference(res,[status(thm),theory(equality)],[48,2707]),
[iquote('0:Res:48.1,2707.0')] ).
cnf(2799,plain,
( secret(tT)
| elem(l,run(u,assign(l,tT))) ),
inference(res,[status(thm),theory(equality)],[2,2713]),
[iquote('0:Res:2.0,2713.0')] ).
cnf(2823,plain,
secret(tT),
inference(spt,[spt(split,[position(s1)])],[2799]),
[iquote('1:Spt:2799.0')] ).
cnf(2831,plain,
~ equal(tT,tT),
inference(ems,[status(thm)],[229,2823]),
[iquote('1:EmS:229.0,2823.0')] ).
cnf(2833,plain,
$false,
inference(obv,[status(thm),theory(equality)],[2831]),
[iquote('1:Obv:2831.0')] ).
cnf(2834,plain,
~ secret(tT),
inference(spt,[spt(split,[position(sa)])],[2833,2823]),
[iquote('1:Spt:2833.0,2799.0,2823.0')] ).
cnf(2835,plain,
elem(l,run(u,assign(l,tT))),
inference(spt,[spt(split,[position(s2)])],[2799]),
[iquote('1:Spt:2833.0,2799.1')] ).
cnf(3114,plain,
( eval(u,nand__dfg(v,fF))
| elem(l,del(l,u))
| secret(nand__dfg(v,fF)) ),
inference(res,[status(thm),theory(equality)],[2776,8]),
[iquote('0:Res:2776.0,8.0')] ).
cnf(3154,plain,
( elem(l,del(l,cons(h,cons(h,u))))
| secret(nand__dfg(v,fF))
| secret(nand__dfg(v,fF))
| elem(l,run(u,assign(l,nand__dfg(v,fF)))) ),
inference(res,[status(thm),theory(equality)],[3114,2713]),
[iquote('0:Res:3114.0,2713.0')] ).
cnf(3157,plain,
( elem(l,del(l,cons(h,cons(h,u))))
| secret(nand__dfg(v,fF))
| elem(l,run(u,assign(l,nand__dfg(v,fF)))) ),
inference(obv,[status(thm),theory(equality)],[3154]),
[iquote('0:Obv:3154.1')] ).
cnf(3158,plain,
( secret(nand__dfg(u,fF))
| elem(l,run(v,assign(l,nand__dfg(u,fF)))) ),
inference(mrr,[status(thm)],[3157,2716]),
[iquote('0:MRR:3157.0,2716.0')] ).
cnf(7735,plain,
( ~ typeCorrect(assign(l,nand__dfg(u,fF)))
| ~ typeCorrect(v)
| ~ eval(w,x)
| secret(nand__dfg(u,fF))
| eval(cons(h,w),x)
| elem(l,run(w,v)) ),
inference(res,[status(thm),theory(equality)],[3158,2198]),
[iquote('0:Res:3158.1,2198.3')] ).
cnf(7771,plain,
( ~ typeCorrect(u)
| ~ eval(v,w)
| secret(nand__dfg(x,fF))
| eval(cons(h,v),w)
| elem(l,run(v,u)) ),
inference(mrr,[status(thm)],[7735,102]),
[iquote('0:MRR:7735.0,102.1')] ).
cnf(7973,plain,
( ~ typeCorrect(u)
| ~ eval(v,w)
| eval(cons(h,v),w)
| elem(l,run(v,u)) ),
inference(spt,[spt(split,[position(s2s1)])],[7771]),
[iquote('2:Spt:7771.0,7771.1,7771.3,7771.4')] ).
cnf(7982,plain,
( ~ typeCorrect(u)
| eval(v,w)
| eval(cons(h,v),nand__dfg(x,w))
| elem(l,run(v,u)) ),
inference(res,[status(thm),theory(equality)],[48,7973]),
[iquote('2:Res:48.1,7973.1')] ).
cnf(9019,plain,
( ~ typeCorrect(u)
| ~ eval(cons(h,v),w)
| ~ eval(cons(h,v),x)
| eval(v,x)
| elem(l,run(v,u)) ),
inference(res,[status(thm),theory(equality)],[7982,65]),
[iquote('2:Res:7982.2,65.2')] ).
cnf(9064,plain,
( ~ typeCorrect(u)
| ~ eval(cons(h,v),w)
| eval(v,w)
| elem(l,run(v,u)) ),
inference(con,[status(thm)],[9019]),
[iquote('2:Con:9019.1')] ).
cnf(9102,plain,
( ~ typeCorrect(u)
| ~ elem(v,cons(h,w))
| eval(w,var(v))
| elem(l,run(w,u)) ),
inference(res,[status(thm),theory(equality)],[50,9064]),
[iquote('2:Res:50.1,9064.1')] ).
cnf(9349,plain,
( ~ typeCorrect(u)
| ~ equal(h,v)
| eval(w,var(v))
| elem(l,run(w,u)) ),
inference(res,[status(thm),theory(equality)],[55,9102]),
[iquote('2:Res:55.1,9102.1')] ).
cnf(9384,plain,
( ~ typeCorrect(u)
| eval(v,var(h))
| elem(l,run(v,u)) ),
inference(eqr,[status(thm),theory(equality)],[9349]),
[iquote('2:EqR:9349.1')] ).
cnf(9402,plain,
( ~ typeCorrect(skip)
| eval(u,var(h))
| elem(l,u) ),
inference(spr,[status(thm),theory(equality)],[19,9384]),
[iquote('2:SpR:19.0,9384.2')] ).
cnf(9472,plain,
( eval(u,var(h))
| elem(l,u) ),
inference(ssi,[status(thm)],[9402,1]),
[iquote('2:SSi:9402.0,1.0')] ).
cnf(9528,plain,
( elem(l,u)
| elem(h,u) ),
inference(res,[status(thm),theory(equality)],[9472,49]),
[iquote('2:Res:9472.0,49.0')] ).
cnf(9556,plain,
elem(l,nil),
inference(res,[status(thm),theory(equality)],[9528,7]),
[iquote('2:Res:9528.1,7.0')] ).
cnf(9567,plain,
$false,
inference(mrr,[status(thm)],[9556,7]),
[iquote('2:MRR:9556.0,7.0')] ).
cnf(9584,plain,
secret(nand__dfg(u,fF)),
inference(spt,[spt(split,[position(s2s2)])],[7771]),
[iquote('2:Spt:9567.0,7771.2')] ).
cnf(9595,plain,
( ~ equal(u,tT)
| ~ equal(fF,fF) ),
inference(res,[status(thm),theory(equality)],[9584,698]),
[iquote('2:Res:9584.0,698.1')] ).
cnf(9611,plain,
~ equal(u,tT),
inference(obv,[status(thm),theory(equality)],[9595]),
[iquote('2:Obv:9595.1')] ).
cnf(9612,plain,
$false,
inference(aed,[status(thm),theory(equality)],[3,9611]),
[iquote('2:AED:3.0,9611.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SWX240_1 : TPTP v9.3.0. Released v9.3.0.
% 0.00/0.13 % Command : run_spass %d %s
% 0.17/0.34 % Computer : n026.cluster.edu
% 0.17/0.34 % Model : x86_64 x86_64
% 0.17/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.34 % Memory : 8042.1875MB
% 0.17/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.17/0.34 % CPULimit : 300
% 0.17/0.34 % WCLimit : 300
% 0.17/0.34 % DateTime : Tue May 5 13:23:08 EDT 2026
% 0.17/0.34 % CPUTime :
% 8.73/8.92
% 8.73/8.92 SPASS V 3.9
% 8.73/8.92 SPASS beiseite: Proof found.
% 8.73/8.92 % SZS status Theorem
% 8.73/8.92 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 8.73/8.92 SPASS derived 7533 clauses, backtracked 1146 clauses, performed 19 splits and kept 5114 clauses.
% 8.73/8.92 SPASS allocated 109588 KBytes.
% 8.73/8.92 SPASS spent 0:00:08.56 on the problem.
% 8.73/8.92 0:00:00.04 for the input.
% 8.73/8.92 0:00:00.03 for the FLOTTER CNF translation.
% 8.73/8.92 0:00:00.16 for inferences.
% 8.73/8.92 0:00:00.71 for the backtracking.
% 8.73/8.92 0:00:07.55 for the reduction.
% 8.73/8.92
% 8.73/8.92
% 8.73/8.92 Here is a proof with depth 16, length 98 :
% 8.73/8.92 % SZS output start Refutation
% See solution above
% 8.73/8.99 Formulae used in the proof : axiom_035 axiom_045 axiom_015 axiom_040 axiom_042 axiom_046 axiom_016 axiom_017 axiom_051 axiom_009 axiom_010 axiom_012 axiom_013 axiom_014 axiom_037 axiom_044 axiom_047 axiom_032 axiom_043 axiom_039 axiom_053 axiom_052 axiom_056 axiom_055 axiom_031 goal_057
% 8.73/8.99
%------------------------------------------------------------------------------