%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : SWX241_1 : TPTP v9.3.0. Released v9.3.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n027.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:30 PM UTC 2026
% Result : Theorem 20.74s 21.02s
% Output : Refutation 20.96s
% 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('SWX241_1.p',unknown),
[] ).
cnf(2,axiom,
eval(u,tT),
file('SWX241_1.p',unknown),
[] ).
cnf(3,axiom,
~ equal(fF,tT),
file('SWX241_1.p',unknown),
[] ).
cnf(5,axiom,
equal(low(zero),l),
file('SWX241_1.p',unknown),
[] ).
cnf(7,axiom,
~ elem(u,nil),
file('SWX241_1.p',unknown),
[] ).
cnf(8,axiom,
~ eval(u,fF),
file('SWX241_1.p',unknown),
[] ).
cnf(14,axiom,
~ equal(var(u),tT),
file('SWX241_1.p',unknown),
[] ).
cnf(15,axiom,
~ equal(var(u),fF),
file('SWX241_1.p',unknown),
[] ).
cnf(19,axiom,
equal(run(u,skip),u),
file('SWX241_1.p',unknown),
[] ).
cnf(24,axiom,
equal(proj1Nand(nand__dfg(u,v)),u),
file('SWX241_1.p',unknown),
[] ).
cnf(25,axiom,
equal(proj2Nand(nand__dfg(u,v)),v),
file('SWX241_1.p',unknown),
[] ).
cnf(26,axiom,
~ equal(nand__dfg(u,v),tT),
file('SWX241_1.p',unknown),
[] ).
cnf(27,axiom,
~ equal(nand__dfg(u,v),fF),
file('SWX241_1.p',unknown),
[] ).
cnf(37,axiom,
~ equal(nand__dfg(u,v),var(w)),
file('SWX241_1.p',unknown),
[] ).
cnf(44,axiom,
( secret(u)
| typeCorrect(assign(low(v),u)) ),
file('SWX241_1.p',unknown),
[] ).
cnf(55,axiom,
( eval(u,v)
| eval(u,nand__dfg(w,v)) ),
file('SWX241_1.p',unknown),
[] ).
cnf(56,axiom,
( ~ eval(u,var(v))
| elem(v,u) ),
file('SWX241_1.p',unknown),
[] ).
cnf(57,axiom,
( ~ elem(u,v)
| eval(v,var(u)) ),
file('SWX241_1.p',unknown),
[] ).
cnf(61,axiom,
( ~ secret(nand__dfg(u,v))
| secret(u)
| secret(v) ),
file('SWX241_1.p',unknown),
[] ).
cnf(63,axiom,
( ~ equal(u,v)
| elem(v,cons(u,w)) ),
file('SWX241_1.p',unknown),
[] ).
cnf(67,axiom,
( ~ typeCorrect(u)
| ~ typeCorrect(v)
| typeCorrect(ifThenElse(w,u,v)) ),
file('SWX241_1.p',unknown),
[] ).
cnf(70,axiom,
( eval(u,v)
| equal(run(u,assign(w,v)),del(w,u)) ),
file('SWX241_1.p',unknown),
[] ).
cnf(71,axiom,
( ~ eval(u,v)
| equal(run(u,assign(w,v)),cons(w,u)) ),
file('SWX241_1.p',unknown),
[] ).
cnf(72,axiom,
( eval(u,v)
| equal(run(u,ifThenElse(v,w,x)),run(u,x)) ),
file('SWX241_1.p',unknown),
[] ).
cnf(73,axiom,
( ~ eval(u,v)
| ~ eval(u,w)
| ~ eval(u,nand__dfg(v,w)) ),
file('SWX241_1.p',unknown),
[] ).
cnf(75,axiom,
( ~ eval(u,v)
| equal(run(u,ifThenElse(v,w,x)),run(u,w)) ),
file('SWX241_1.p',unknown),
[] ).
cnf(76,axiom,
( ~ secret(u)
| equal(var(proj1Var(u)),u)
| equal(nand__dfg(proj1Nand(u),proj2Nand(u)),u) ),
file('SWX241_1.p',unknown),
[] ).
cnf(77,axiom,
( ~ typeCorrect(u)
| ~ elem(l,run(v,u))
| elem(l,run(cons(h,v),u)) ),
file('SWX241_1.p',unknown),
[] ).
cnf(78,axiom,
( ~ typeCorrect(u)
| ~ elem(l,run(cons(h,v),u))
| elem(l,run(v,u)) ),
file('SWX241_1.p',unknown),
[] ).
cnf(113,plain,
( secret(u)
| typeCorrect(assign(l,u)) ),
inference(spr,[status(thm),theory(equality)],[5,44]),
[iquote('0:SpR:5.0,44.1')] ).
cnf(198,plain,
( ~ secret(u)
| ~ equal(u,fF)
| equal(var(proj1Var(u)),u) ),
inference(spl,[status(thm),theory(equality)],[76,27]),
[iquote('0:SpL:76.2,27.0')] ).
cnf(199,plain,
( ~ secret(u)
| ~ equal(u,tT)
| equal(var(proj1Var(u)),u) ),
inference(spl,[status(thm),theory(equality)],[76,26]),
[iquote('0:SpL:76.2,26.0')] ).
cnf(200,plain,
( ~ secret(u)
| ~ secret(u)
| equal(var(proj1Var(u)),u)
| secret(proj1Nand(u))
| secret(proj2Nand(u)) ),
inference(spl,[status(thm),theory(equality)],[76,61]),
[iquote('0:SpL:76.2,61.0')] ).
cnf(203,plain,
( ~ secret(u)
| equal(var(proj1Var(u)),u)
| secret(proj1Nand(u))
| secret(proj2Nand(u)) ),
inference(obv,[status(thm),theory(equality)],[200]),
[iquote('0:Obv:200.0')] ).
cnf(210,plain,
( ~ secret(u)
| ~ equal(u,fF)
| ~ equal(u,fF) ),
inference(spl,[status(thm),theory(equality)],[198,15]),
[iquote('0:SpL:198.2,15.0')] ).
cnf(214,plain,
( ~ secret(u)
| ~ equal(u,fF) ),
inference(obv,[status(thm),theory(equality)],[210]),
[iquote('0:Obv:210.1')] ).
cnf(224,plain,
( ~ secret(u)
| ~ equal(u,tT)
| ~ equal(u,tT) ),
inference(spl,[status(thm),theory(equality)],[199,14]),
[iquote('0:SpL:199.2,14.0')] ).
cnf(227,plain,
( ~ secret(u)
| ~ equal(u,tT) ),
inference(obv,[status(thm),theory(equality)],[224]),
[iquote('0:Obv:224.1')] ).
cnf(238,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)],[70,77]),
[iquote('0:SpR:70.1,77.2')] ).
cnf(254,plain,
( ~ secret(u)
| ~ equal(nand__dfg(v,w),u)
| secret(proj1Nand(u))
| secret(proj2Nand(u)) ),
inference(spl,[status(thm),theory(equality)],[203,37]),
[iquote('0:SpL:203.1,37.0')] ).
cnf(268,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)],[71,78]),
[iquote('0:SpL:71.1,78.1')] ).
cnf(269,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)],[70,78]),
[iquote('0:SpL:70.1,78.1')] ).
cnf(271,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)],[72,78]),
[iquote('0:SpL:72.1,78.1')] ).
cnf(322,plain,
( ~ equal(proj2Nand(u),fF)
| ~ equal(nand__dfg(v,w),u)
| ~ secret(u)
| secret(proj1Nand(u)) ),
inference(ems,[status(thm)],[214,254]),
[iquote('0:EmS:214.0,254.3')] ).
cnf(441,plain,
( ~ equal(proj1Nand(u),tT)
| ~ secret(u)
| ~ equal(nand__dfg(v,w),u)
| ~ equal(proj2Nand(u),fF) ),
inference(ems,[status(thm)],[227,322]),
[iquote('0:EmS:227.0,322.3')] ).
cnf(803,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)],[238,113]),
[iquote('0:SoR:238.0,113.1')] ).
cnf(836,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)],[269,113]),
[iquote('0:SoR:269.0,113.1')] ).
cnf(848,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)],[441]),
[iquote('0:EqR:441.2')] ).
cnf(850,plain,
( ~ equal(u,tT)
| ~ secret(nand__dfg(u,v))
| ~ equal(v,fF) ),
inference(rew,[status(thm),theory(equality)],[25,848,24]),
[iquote('0:Rew:25.0,848.2,24.0,848.0')] ).
cnf(903,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)],[268,113]),
[iquote('0:SoR:268.0,113.1')] ).
cnf(998,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)],[271,67]),
[iquote('0:SoR:271.0,67.2')] ).
cnf(1265,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)],[71,803]),
[iquote('0:SpL:71.1,803.0')] ).
cnf(1306,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)],[71,836]),
[iquote('0:SpR:71.1,836.2')] ).
cnf(1309,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)],[836,78]),
[iquote('0:Res:836.2,78.1')] ).
cnf(1311,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)],[1309,113]),
[iquote('0:MRR:1309.0,113.1')] ).
cnf(1579,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)],[71,903]),
[iquote('0:SpR:71.1,903.2')] ).
cnf(1580,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)],[70,903]),
[iquote('0:SpR:70.1,903.2')] ).
cnf(1585,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)],[903,78]),
[iquote('0:Res:903.2,78.1')] ).
cnf(1588,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)],[1585,113]),
[iquote('0:MRR:1585.0,113.1')] ).
cnf(3273,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)],[63,1265]),
[iquote('0:Res:63.1,1265.1')] ).
cnf(3289,plain,
( ~ eval(u,v)
| eval(cons(h,u),v)
| elem(l,del(l,cons(h,u)))
| secret(v) ),
inference(obv,[status(thm),theory(equality)],[3273]),
[iquote('0:Obv:3273.0')] ).
cnf(3293,plain,
( ~ eval(u,v)
| eval(cons(h,u),v)
| elem(l,cons(l,u))
| secret(v) ),
inference(mrr,[status(thm)],[1306,3289]),
[iquote('0:MRR:1306.1,3289.2')] ).
cnf(3294,plain,
( ~ eval(u,v)
| ~ elem(l,cons(l,cons(h,u)))
| elem(l,cons(l,u))
| secret(v) ),
inference(mrr,[status(thm)],[1579,3293]),
[iquote('0:MRR:1579.1,3293.1')] ).
cnf(3384,plain,
( ~ equal(l,l)
| ~ eval(u,v)
| elem(l,cons(l,u))
| secret(v) ),
inference(res,[status(thm),theory(equality)],[63,3294]),
[iquote('0:Res:63.1,3294.1')] ).
cnf(3390,plain,
( ~ eval(u,v)
| elem(l,cons(l,u))
| secret(v) ),
inference(obv,[status(thm),theory(equality)],[3384]),
[iquote('0:Obv:3384.0')] ).
cnf(3392,plain,
( ~ eval(cons(h,u),v)
| eval(u,v)
| elem(l,del(l,u))
| secret(v) ),
inference(mrr,[status(thm)],[1580,3390]),
[iquote('0:MRR:1580.1,3390.1')] ).
cnf(3398,plain,
( ~ eval(cons(h,cons(h,u)),v)
| secret(v)
| elem(l,run(u,assign(l,v))) ),
inference(mrr,[status(thm)],[1588,3390]),
[iquote('0:MRR:1588.1,3390.1')] ).
cnf(3401,plain,
( ~ elem(l,del(l,cons(h,cons(h,u))))
| secret(v)
| elem(l,run(u,assign(l,v))) ),
inference(mrr,[status(thm)],[1311,3398]),
[iquote('0:MRR:1311.1,3398.0')] ).
cnf(3461,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)],[55,3392]),
[iquote('0:Res:55.1,3392.0')] ).
cnf(3484,plain,
( secret(tT)
| elem(l,run(u,assign(l,tT))) ),
inference(res,[status(thm),theory(equality)],[2,3398]),
[iquote('0:Res:2.0,3398.0')] ).
cnf(3508,plain,
secret(tT),
inference(spt,[spt(split,[position(s1)])],[3484]),
[iquote('1:Spt:3484.0')] ).
cnf(3516,plain,
~ equal(tT,tT),
inference(ems,[status(thm)],[227,3508]),
[iquote('1:EmS:227.0,3508.0')] ).
cnf(3518,plain,
$false,
inference(obv,[status(thm),theory(equality)],[3516]),
[iquote('1:Obv:3516.0')] ).
cnf(3519,plain,
~ secret(tT),
inference(spt,[spt(split,[position(sa)])],[3518,3508]),
[iquote('1:Spt:3518.0,3484.0,3508.0')] ).
cnf(3520,plain,
elem(l,run(u,assign(l,tT))),
inference(spt,[spt(split,[position(s2)])],[3484]),
[iquote('1:Spt:3518.0,3484.1')] ).
cnf(3530,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)],[75,998]),
[iquote('0:SpR:75.1,998.4')] ).
cnf(3889,plain,
( eval(u,nand__dfg(v,fF))
| elem(l,del(l,u))
| secret(nand__dfg(v,fF)) ),
inference(res,[status(thm),theory(equality)],[3461,8]),
[iquote('0:Res:3461.0,8.0')] ).
cnf(3929,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)],[3889,3398]),
[iquote('0:Res:3889.0,3398.0')] ).
cnf(3932,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)],[3929]),
[iquote('0:Obv:3929.1')] ).
cnf(3933,plain,
( secret(nand__dfg(u,fF))
| elem(l,run(v,assign(l,nand__dfg(u,fF)))) ),
inference(mrr,[status(thm)],[3932,3401]),
[iquote('0:MRR:3932.0,3401.0')] ).
cnf(12356,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)],[3933,3530]),
[iquote('0:Res:3933.1,3530.3')] ).
cnf(12415,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)],[12356,113]),
[iquote('0:MRR:12356.0,113.1')] ).
cnf(13575,plain,
( ~ typeCorrect(u)
| ~ eval(v,w)
| eval(cons(h,v),w)
| elem(l,run(v,u)) ),
inference(spt,[spt(split,[position(s2s1)])],[12415]),
[iquote('2:Spt:12415.0,12415.1,12415.3,12415.4')] ).
cnf(13585,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)],[55,13575]),
[iquote('2:Res:55.1,13575.1')] ).
cnf(14902,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)],[13585,73]),
[iquote('2:Res:13585.2,73.2')] ).
cnf(14956,plain,
( ~ typeCorrect(u)
| ~ eval(cons(h,v),w)
| eval(v,w)
| elem(l,run(v,u)) ),
inference(con,[status(thm)],[14902]),
[iquote('2:Con:14902.1')] ).
cnf(14999,plain,
( ~ typeCorrect(u)
| ~ elem(v,cons(h,w))
| eval(w,var(v))
| elem(l,run(w,u)) ),
inference(res,[status(thm),theory(equality)],[57,14956]),
[iquote('2:Res:57.1,14956.1')] ).
cnf(15299,plain,
( ~ typeCorrect(u)
| ~ equal(h,v)
| eval(w,var(v))
| elem(l,run(w,u)) ),
inference(res,[status(thm),theory(equality)],[63,14999]),
[iquote('2:Res:63.1,14999.1')] ).
cnf(15345,plain,
( ~ typeCorrect(u)
| eval(v,var(h))
| elem(l,run(v,u)) ),
inference(eqr,[status(thm),theory(equality)],[15299]),
[iquote('2:EqR:15299.1')] ).
cnf(15346,plain,
( ~ typeCorrect(skip)
| eval(u,var(h))
| elem(l,u) ),
inference(spr,[status(thm),theory(equality)],[19,15345]),
[iquote('2:SpR:19.0,15345.2')] ).
cnf(15457,plain,
( eval(u,var(h))
| elem(l,u) ),
inference(ssi,[status(thm)],[15346,1]),
[iquote('2:SSi:15346.0,1.0')] ).
cnf(15584,plain,
( elem(l,u)
| elem(h,u) ),
inference(res,[status(thm),theory(equality)],[15457,56]),
[iquote('2:Res:15457.0,56.0')] ).
cnf(15616,plain,
elem(l,nil),
inference(res,[status(thm),theory(equality)],[15584,7]),
[iquote('2:Res:15584.1,7.0')] ).
cnf(15630,plain,
$false,
inference(mrr,[status(thm)],[15616,7]),
[iquote('2:MRR:15616.0,7.0')] ).
cnf(15647,plain,
secret(nand__dfg(u,fF)),
inference(spt,[spt(split,[position(s2s2)])],[12415]),
[iquote('2:Spt:15630.0,12415.2')] ).
cnf(15658,plain,
( ~ equal(u,tT)
| ~ equal(fF,fF) ),
inference(res,[status(thm),theory(equality)],[15647,850]),
[iquote('2:Res:15647.0,850.1')] ).
cnf(15674,plain,
~ equal(u,tT),
inference(obv,[status(thm),theory(equality)],[15658]),
[iquote('2:Obv:15658.1')] ).
cnf(15675,plain,
$false,
inference(aed,[status(thm),theory(equality)],[3,15674]),
[iquote('2:AED:3.0,15674.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SWX241_1 : TPTP v9.3.0. Released v9.3.0.
% 0.11/0.13 % Command : run_spass %d %s
% 0.16/0.34 % Computer : n027.cluster.edu
% 0.16/0.34 % Model : x86_64 x86_64
% 0.16/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.34 % Memory : 8042.1875MB
% 0.16/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.34 % CPULimit : 300
% 0.16/0.34 % WCLimit : 300
% 0.16/0.34 % DateTime : Tue May 5 13:27:49 EDT 2026
% 0.16/0.34 % CPUTime :
% 20.74/21.02
% 20.74/21.02 SPASS V 3.9
% 20.74/21.02 SPASS beiseite: Proof found.
% 20.74/21.02 % SZS status Theorem
% 20.74/21.02 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 20.74/21.02 SPASS derived 12305 clauses, backtracked 1712 clauses, performed 21 splits and kept 7750 clauses.
% 20.74/21.02 SPASS allocated 117208 KBytes.
% 20.74/21.02 SPASS spent 0:0:20.66 on the problem.
% 20.74/21.02 0:00:00.03 for the input.
% 20.74/21.02 0:00:00.04 for the FLOTTER CNF translation.
% 20.74/21.02 0:00:00.27 for inferences.
% 20.74/21.02 0:00:01.77 for the backtracking.
% 20.74/21.02 0:0:18.46 for the reduction.
% 20.74/21.02
% 20.74/21.02
% 20.74/21.02 Here is a proof with depth 16, length 98 :
% 20.74/21.02 % SZS output start Refutation
% See solution above
% 20.96/21.18 Formulae used in the proof : axiom_041 axiom_052 axiom_015 axiom_047 axiom_049 axiom_053 axiom_016 axiom_017 axiom_058 axiom_009 axiom_010 axiom_012 axiom_013 axiom_014 axiom_043 axiom_051 axiom_054 axiom_038 axiom_050 axiom_045 axiom_060 axiom_059 axiom_063 axiom_062 axiom_037 goal_065
% 20.96/21.18
%------------------------------------------------------------------------------