%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : NUM541+1 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n020.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 : 600s
% DateTime : Mon Jul 18 14:27:17 EDT 2022
% Result : Theorem 53.81s 54.02s
% Output : Refutation 56.76s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 18
% Syntax : Number of clauses : 78 ( 20 unt; 15 nHn; 78 RR)
% Number of literals : 240 ( 0 equ; 158 neg)
% Maximal clause size : 7 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 4 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 7 con; 0-1 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(5,axiom,
aElementOf0(xm,szNzAzT0),
file('NUM541+1.p',unknown),
[] ).
cnf(6,axiom,
aElementOf0(xn,szNzAzT0),
file('NUM541+1.p',unknown),
[] ).
cnf(7,axiom,
aElementOf0(skf13(u),szNzAzT0),
file('NUM541+1.p',unknown),
[] ).
cnf(16,axiom,
( ~ aElementOf0(u,szNzAzT0)
| sdtlseqdt0(u,u) ),
file('NUM541+1.p',unknown),
[] ).
cnf(20,axiom,
( ~ aElementOf0(u,szNzAzT0)
| aElementOf0(szszuzczcdt0(u),szNzAzT0) ),
file('NUM541+1.p',unknown),
[] ).
cnf(21,axiom,
( ~ aElementOf0(u,szNzAzT0)
| sdtlseqdt0(u,szszuzczcdt0(u)) ),
file('NUM541+1.p',unknown),
[] ).
cnf(27,axiom,
( ~ aElementOf0(u,szNzAzT0)
| ~ equal(szszuzczcdt0(u),sz00) ),
file('NUM541+1.p',unknown),
[] ).
cnf(28,axiom,
( ~ aElementOf0(u,szNzAzT0)
| ~ equal(szszuzczcdt0(u),u) ),
file('NUM541+1.p',unknown),
[] ).
cnf(30,axiom,
( ~ equal(xn,xm)
| ~ aElementOf0(xm,slbdtrb0(szszuzczcdt0(xn))) ),
file('NUM541+1.p',unknown),
[] ).
cnf(34,axiom,
( ~ aElementOf0(xm,slbdtrb0(xn))
| ~ aElementOf0(xm,slbdtrb0(szszuzczcdt0(xn))) ),
file('NUM541+1.p',unknown),
[] ).
cnf(41,axiom,
( equal(xn,xm)
| aElementOf0(xm,slbdtrb0(xn))
| aElementOf0(xm,slbdtrb0(szszuzczcdt0(xn))) ),
file('NUM541+1.p',unknown),
[] ).
cnf(43,axiom,
( ~ aElementOf0(u,szNzAzT0)
| equal(u,sz00)
| equal(szszuzczcdt0(skf13(u)),u) ),
file('NUM541+1.p',unknown),
[] ).
cnf(55,axiom,
( ~ aElementOf0(u,szNzAzT0)
| ~ aElementOf0(v,szNzAzT0)
| sdtlseqdt0(v,u)
| sdtlseqdt0(szszuzczcdt0(u),v) ),
file('NUM541+1.p',unknown),
[] ).
cnf(62,axiom,
( ~ sdtlseqdt0(u,v)
| ~ aElementOf0(v,szNzAzT0)
| ~ aElementOf0(u,szNzAzT0)
| sdtlseqdt0(szszuzczcdt0(u),szszuzczcdt0(v)) ),
file('NUM541+1.p',unknown),
[] ).
cnf(64,axiom,
( ~ aElementOf0(u,v)
| ~ aElementOf0(w,szNzAzT0)
| ~ equal(v,slbdtrb0(w))
| sdtlseqdt0(szszuzczcdt0(u),w) ),
file('NUM541+1.p',unknown),
[] ).
cnf(67,axiom,
( ~ sdtlseqdt0(u,v)
| ~ sdtlseqdt0(v,u)
| ~ aElementOf0(u,szNzAzT0)
| ~ aElementOf0(v,szNzAzT0)
| equal(v,u) ),
file('NUM541+1.p',unknown),
[] ).
cnf(78,axiom,
( ~ aElementOf0(u,szNzAzT0)
| ~ aElementOf0(v,szNzAzT0)
| ~ equal(w,slbdtrb0(u))
| ~ sdtlseqdt0(szszuzczcdt0(v),u)
| aElementOf0(v,w) ),
file('NUM541+1.p',unknown),
[] ).
cnf(84,axiom,
( ~ sdtlseqdt0(u,v)
| ~ sdtlseqdt0(w,u)
| ~ aElementOf0(v,szNzAzT0)
| ~ aElementOf0(u,szNzAzT0)
| ~ aElementOf0(w,szNzAzT0)
| sdtlseqdt0(w,v) ),
file('NUM541+1.p',unknown),
[] ).
cnf(102,plain,
equal(xn,xm),
inference(spt,[spt(split,[position(s1)])],[41]),
[iquote('1:Spt:41.0')] ).
cnf(103,plain,
( ~ equal(xm,xm)
| ~ aElementOf0(xm,slbdtrb0(szszuzczcdt0(xn))) ),
inference(rew,[status(thm),theory(equality)],[102,30]),
[iquote('1:Rew:102.0,30.0')] ).
cnf(106,plain,
~ aElementOf0(xm,slbdtrb0(szszuzczcdt0(xn))),
inference(obv,[status(thm),theory(equality)],[103]),
[iquote('1:Obv:103.0')] ).
cnf(107,plain,
~ aElementOf0(xm,slbdtrb0(szszuzczcdt0(xm))),
inference(rew,[status(thm),theory(equality)],[102,106]),
[iquote('1:Rew:102.0,106.0')] ).
cnf(125,plain,
~ equal(szszuzczcdt0(skf13(u)),skf13(u)),
inference(res,[status(thm),theory(equality)],[7,28]),
[iquote('0:Res:7.0,28.0')] ).
cnf(186,plain,
( ~ aElementOf0(u,szNzAzT0)
| ~ aElementOf0(skf13(u),szNzAzT0)
| equal(u,sz00)
| sdtlseqdt0(skf13(u),u) ),
inference(spr,[status(thm),theory(equality)],[43,21]),
[iquote('0:SpR:43.2,21.1')] ).
cnf(195,plain,
( ~ aElementOf0(u,szNzAzT0)
| ~ equal(skf13(u),u)
| equal(u,sz00) ),
inference(spl,[status(thm),theory(equality)],[43,125]),
[iquote('0:SpL:43.2,125.0')] ).
cnf(197,plain,
( ~ aElementOf0(u,szNzAzT0)
| equal(u,sz00)
| sdtlseqdt0(skf13(u),u) ),
inference(mrr,[status(thm)],[186,7]),
[iquote('0:MRR:186.1,7.0')] ).
cnf(536,plain,
( ~ aElementOf0(u,szNzAzT0)
| ~ aElementOf0(skf13(u),szNzAzT0)
| ~ aElementOf0(v,szNzAzT0)
| equal(u,sz00)
| sdtlseqdt0(v,skf13(u))
| sdtlseqdt0(u,v) ),
inference(spr,[status(thm),theory(equality)],[43,55]),
[iquote('0:SpR:43.2,55.3')] ).
cnf(540,plain,
( ~ aElementOf0(u,szNzAzT0)
| ~ aElementOf0(v,szNzAzT0)
| equal(u,sz00)
| sdtlseqdt0(v,skf13(u))
| sdtlseqdt0(u,v) ),
inference(mrr,[status(thm)],[536,7]),
[iquote('0:MRR:536.1,7.0')] ).
cnf(756,plain,
( ~ aElementOf0(u,slbdtrb0(v))
| ~ aElementOf0(v,szNzAzT0)
| sdtlseqdt0(szszuzczcdt0(u),v) ),
inference(eqr,[status(thm),theory(equality)],[64]),
[iquote('0:EqR:64.2')] ).
cnf(917,plain,
( ~ aElementOf0(u,szNzAzT0)
| ~ sdtlseqdt0(u,skf13(u))
| ~ aElementOf0(skf13(u),szNzAzT0)
| ~ aElementOf0(u,szNzAzT0)
| equal(u,sz00)
| equal(skf13(u),u) ),
inference(res,[status(thm),theory(equality)],[197,67]),
[iquote('0:Res:197.2,67.0')] ).
cnf(919,plain,
( ~ aElementOf0(u,szNzAzT0)
| ~ sdtlseqdt0(szszuzczcdt0(u),u)
| ~ aElementOf0(u,szNzAzT0)
| ~ aElementOf0(szszuzczcdt0(u),szNzAzT0)
| equal(szszuzczcdt0(u),u) ),
inference(res,[status(thm),theory(equality)],[21,67]),
[iquote('0:Res:21.1,67.0')] ).
cnf(920,plain,
( ~ sdtlseqdt0(u,v)
| ~ aElementOf0(v,szNzAzT0)
| ~ aElementOf0(u,szNzAzT0)
| ~ sdtlseqdt0(szszuzczcdt0(v),szszuzczcdt0(u))
| ~ aElementOf0(szszuzczcdt0(u),szNzAzT0)
| ~ aElementOf0(szszuzczcdt0(v),szNzAzT0)
| equal(szszuzczcdt0(v),szszuzczcdt0(u)) ),
inference(res,[status(thm),theory(equality)],[62,67]),
[iquote('0:Res:62.3,67.0')] ).
cnf(928,plain,
( ~ sdtlseqdt0(szszuzczcdt0(u),u)
| ~ aElementOf0(u,szNzAzT0)
| ~ aElementOf0(szszuzczcdt0(u),szNzAzT0)
| equal(szszuzczcdt0(u),u) ),
inference(obv,[status(thm),theory(equality)],[919]),
[iquote('0:Obv:919.0')] ).
cnf(929,plain,
( ~ sdtlseqdt0(szszuzczcdt0(u),u)
| ~ aElementOf0(u,szNzAzT0) ),
inference(mrr,[status(thm)],[928,20,28]),
[iquote('0:MRR:928.2,928.3,20.1,28.1')] ).
cnf(930,plain,
( ~ sdtlseqdt0(u,skf13(u))
| ~ aElementOf0(skf13(u),szNzAzT0)
| ~ aElementOf0(u,szNzAzT0)
| equal(u,sz00)
| equal(skf13(u),u) ),
inference(obv,[status(thm),theory(equality)],[917]),
[iquote('0:Obv:917.0')] ).
cnf(931,plain,
( ~ sdtlseqdt0(u,skf13(u))
| ~ aElementOf0(u,szNzAzT0)
| equal(u,sz00) ),
inference(mrr,[status(thm)],[930,7,195]),
[iquote('0:MRR:930.1,930.4,7.0,195.1')] ).
cnf(936,plain,
( ~ sdtlseqdt0(u,v)
| ~ aElementOf0(v,szNzAzT0)
| ~ aElementOf0(u,szNzAzT0)
| ~ sdtlseqdt0(szszuzczcdt0(v),szszuzczcdt0(u))
| equal(szszuzczcdt0(v),szszuzczcdt0(u)) ),
inference(mrr,[status(thm)],[920,20]),
[iquote('0:MRR:920.4,920.5,20.1,20.1')] ).
cnf(964,plain,
( ~ aElementOf0(u,szNzAzT0)
| ~ aElementOf0(skf13(szszuzczcdt0(u)),szNzAzT0)
| ~ aElementOf0(szszuzczcdt0(u),szNzAzT0)
| sdtlseqdt0(skf13(szszuzczcdt0(u)),u)
| equal(szszuzczcdt0(u),sz00) ),
inference(res,[status(thm),theory(equality)],[55,931]),
[iquote('0:Res:55.3,931.0')] ).
cnf(966,plain,
( ~ aElementOf0(u,szNzAzT0)
| sdtlseqdt0(skf13(szszuzczcdt0(u)),u) ),
inference(mrr,[status(thm)],[964,7,20,27]),
[iquote('0:MRR:964.1,964.2,964.4,7.0,20.1,27.1')] ).
cnf(970,plain,
( ~ aElementOf0(u,szNzAzT0)
| ~ sdtlseqdt0(u,skf13(szszuzczcdt0(u)))
| ~ aElementOf0(skf13(szszuzczcdt0(u)),szNzAzT0)
| ~ aElementOf0(u,szNzAzT0)
| equal(skf13(szszuzczcdt0(u)),u) ),
inference(res,[status(thm),theory(equality)],[966,67]),
[iquote('0:Res:966.1,67.0')] ).
cnf(972,plain,
( ~ sdtlseqdt0(u,skf13(szszuzczcdt0(u)))
| ~ aElementOf0(skf13(szszuzczcdt0(u)),szNzAzT0)
| ~ aElementOf0(u,szNzAzT0)
| equal(skf13(szszuzczcdt0(u)),u) ),
inference(obv,[status(thm),theory(equality)],[970]),
[iquote('0:Obv:970.0')] ).
cnf(973,plain,
( ~ sdtlseqdt0(u,skf13(szszuzczcdt0(u)))
| ~ aElementOf0(u,szNzAzT0)
| equal(skf13(szszuzczcdt0(u)),u) ),
inference(mrr,[status(thm)],[972,7]),
[iquote('0:MRR:972.1,7.0')] ).
cnf(1317,plain,
( ~ aElementOf0(u,szNzAzT0)
| ~ aElementOf0(v,szNzAzT0)
| ~ sdtlseqdt0(szszuzczcdt0(v),u)
| aElementOf0(v,slbdtrb0(u)) ),
inference(eqr,[status(thm),theory(equality)],[78]),
[iquote('0:EqR:78.2')] ).
cnf(1607,plain,
( ~ aElementOf0(u,szNzAzT0)
| ~ sdtlseqdt0(v,u)
| ~ aElementOf0(szszuzczcdt0(u),szNzAzT0)
| ~ aElementOf0(u,szNzAzT0)
| ~ aElementOf0(v,szNzAzT0)
| sdtlseqdt0(v,szszuzczcdt0(u)) ),
inference(res,[status(thm),theory(equality)],[21,84]),
[iquote('0:Res:21.1,84.0')] ).
cnf(1618,plain,
( ~ sdtlseqdt0(u,v)
| ~ aElementOf0(szszuzczcdt0(v),szNzAzT0)
| ~ aElementOf0(v,szNzAzT0)
| ~ aElementOf0(u,szNzAzT0)
| sdtlseqdt0(u,szszuzczcdt0(v)) ),
inference(obv,[status(thm),theory(equality)],[1607]),
[iquote('0:Obv:1607.0')] ).
cnf(1619,plain,
( ~ sdtlseqdt0(u,v)
| ~ aElementOf0(v,szNzAzT0)
| ~ aElementOf0(u,szNzAzT0)
| sdtlseqdt0(u,szszuzczcdt0(v)) ),
inference(mrr,[status(thm)],[1618,20]),
[iquote('0:MRR:1618.1,20.1')] ).
cnf(2824,plain,
( ~ aElementOf0(szszuzczcdt0(u),szNzAzT0)
| ~ aElementOf0(szszuzczcdt0(u),szNzAzT0)
| ~ aElementOf0(u,szNzAzT0)
| aElementOf0(u,slbdtrb0(szszuzczcdt0(u))) ),
inference(res,[status(thm),theory(equality)],[16,1317]),
[iquote('0:Res:16.1,1317.2')] ).
cnf(2828,plain,
( ~ aElementOf0(u,szNzAzT0)
| ~ aElementOf0(v,szNzAzT0)
| ~ aElementOf0(v,szNzAzT0)
| ~ aElementOf0(u,szNzAzT0)
| sdtlseqdt0(v,u)
| aElementOf0(u,slbdtrb0(v)) ),
inference(res,[status(thm),theory(equality)],[55,1317]),
[iquote('0:Res:55.3,1317.2')] ).
cnf(2829,plain,
( ~ sdtlseqdt0(szszuzczcdt0(u),v)
| ~ aElementOf0(v,szNzAzT0)
| ~ aElementOf0(szszuzczcdt0(u),szNzAzT0)
| ~ aElementOf0(szszuzczcdt0(v),szNzAzT0)
| ~ aElementOf0(u,szNzAzT0)
| aElementOf0(u,slbdtrb0(szszuzczcdt0(v))) ),
inference(res,[status(thm),theory(equality)],[1619,1317]),
[iquote('0:Res:1619.3,1317.2')] ).
cnf(2831,plain,
( ~ aElementOf0(szszuzczcdt0(u),szNzAzT0)
| ~ aElementOf0(u,szNzAzT0)
| aElementOf0(u,slbdtrb0(szszuzczcdt0(u))) ),
inference(obv,[status(thm),theory(equality)],[2824]),
[iquote('0:Obv:2824.0')] ).
cnf(2832,plain,
( ~ aElementOf0(u,szNzAzT0)
| aElementOf0(u,slbdtrb0(szszuzczcdt0(u))) ),
inference(mrr,[status(thm)],[2831,20]),
[iquote('0:MRR:2831.0,20.1')] ).
cnf(2834,plain,
( ~ aElementOf0(u,szNzAzT0)
| ~ aElementOf0(v,szNzAzT0)
| sdtlseqdt0(u,v)
| aElementOf0(v,slbdtrb0(u)) ),
inference(obv,[status(thm),theory(equality)],[2828]),
[iquote('0:Obv:2828.1')] ).
cnf(2838,plain,
( ~ sdtlseqdt0(szszuzczcdt0(u),v)
| ~ aElementOf0(v,szNzAzT0)
| ~ aElementOf0(u,szNzAzT0)
| aElementOf0(u,slbdtrb0(szszuzczcdt0(v))) ),
inference(mrr,[status(thm)],[2829,20]),
[iquote('0:MRR:2829.2,2829.3,20.1,20.1')] ).
cnf(2844,plain,
~ aElementOf0(xm,szNzAzT0),
inference(res,[status(thm),theory(equality)],[2832,107]),
[iquote('1:Res:2832.1,107.0')] ).
cnf(2850,plain,
$false,
inference(mrr,[status(thm)],[2844,5]),
[iquote('1:MRR:2844.0,5.0')] ).
cnf(2853,plain,
~ equal(xn,xm),
inference(spt,[spt(split,[position(sa)])],[2850,102]),
[iquote('1:Spt:2850.0,41.0,102.0')] ).
cnf(2854,plain,
( aElementOf0(xm,slbdtrb0(xn))
| aElementOf0(xm,slbdtrb0(szszuzczcdt0(xn))) ),
inference(spt,[spt(split,[position(s2)])],[41]),
[iquote('1:Spt:2850.0,41.1,41.2')] ).
cnf(2903,plain,
aElementOf0(xm,slbdtrb0(xn)),
inference(spt,[spt(split,[position(s2s1)])],[2854]),
[iquote('2:Spt:2854.0')] ).
cnf(2904,plain,
~ aElementOf0(xm,slbdtrb0(szszuzczcdt0(xn))),
inference(mrr,[status(thm)],[34,2903]),
[iquote('2:MRR:34.0,2903.0')] ).
cnf(3540,plain,
( ~ aElementOf0(szszuzczcdt0(u),szNzAzT0)
| ~ aElementOf0(u,szNzAzT0)
| ~ aElementOf0(u,szNzAzT0)
| equal(szszuzczcdt0(u),sz00)
| sdtlseqdt0(szszuzczcdt0(u),u)
| equal(skf13(szszuzczcdt0(u)),u) ),
inference(res,[status(thm),theory(equality)],[540,973]),
[iquote('0:Res:540.3,973.0')] ).
cnf(3548,plain,
( ~ aElementOf0(szszuzczcdt0(u),szNzAzT0)
| ~ aElementOf0(u,szNzAzT0)
| equal(szszuzczcdt0(u),sz00)
| sdtlseqdt0(szszuzczcdt0(u),u)
| equal(skf13(szszuzczcdt0(u)),u) ),
inference(obv,[status(thm),theory(equality)],[3540]),
[iquote('0:Obv:3540.1')] ).
cnf(3549,plain,
( ~ aElementOf0(u,szNzAzT0)
| equal(skf13(szszuzczcdt0(u)),u) ),
inference(mrr,[status(thm)],[3548,20,27,929]),
[iquote('0:MRR:3548.0,3548.2,3548.3,20.1,27.1,929.0')] ).
cnf(5803,plain,
( ~ aElementOf0(u,slbdtrb0(szszuzczcdt0(v)))
| ~ aElementOf0(szszuzczcdt0(v),szNzAzT0)
| ~ sdtlseqdt0(v,u)
| ~ aElementOf0(u,szNzAzT0)
| ~ aElementOf0(v,szNzAzT0)
| equal(szszuzczcdt0(u),szszuzczcdt0(v)) ),
inference(res,[status(thm),theory(equality)],[756,936]),
[iquote('0:Res:756.2,936.3')] ).
cnf(5813,plain,
( ~ aElementOf0(u,slbdtrb0(szszuzczcdt0(v)))
| ~ sdtlseqdt0(v,u)
| ~ aElementOf0(u,szNzAzT0)
| ~ aElementOf0(v,szNzAzT0)
| equal(szszuzczcdt0(u),szszuzczcdt0(v)) ),
inference(mrr,[status(thm)],[5803,20]),
[iquote('0:MRR:5803.1,20.1')] ).
cnf(17301,plain,
( ~ sdtlseqdt0(szszuzczcdt0(xm),xn)
| ~ aElementOf0(xn,szNzAzT0)
| ~ aElementOf0(xm,szNzAzT0) ),
inference(res,[status(thm),theory(equality)],[2838,2904]),
[iquote('2:Res:2838.3,2904.0')] ).
cnf(17321,plain,
~ sdtlseqdt0(szszuzczcdt0(xm),xn),
inference(mrr,[status(thm)],[17301,6,5]),
[iquote('2:MRR:17301.1,17301.2,6.0,5.0')] ).
cnf(17337,plain,
( ~ aElementOf0(xm,slbdtrb0(xn))
| ~ aElementOf0(xn,szNzAzT0) ),
inference(res,[status(thm),theory(equality)],[756,17321]),
[iquote('2:Res:756.2,17321.0')] ).
cnf(17339,plain,
$false,
inference(mrr,[status(thm)],[17337,2903,6]),
[iquote('2:MRR:17337.0,17337.1,2903.0,6.0')] ).
cnf(17341,plain,
~ aElementOf0(xm,slbdtrb0(xn)),
inference(spt,[spt(split,[position(s2sa)])],[17339,2903]),
[iquote('2:Spt:17339.0,2854.0,2903.0')] ).
cnf(17342,plain,
aElementOf0(xm,slbdtrb0(szszuzczcdt0(xn))),
inference(spt,[spt(split,[position(s2s2)])],[2854]),
[iquote('2:Spt:17339.0,2854.1')] ).
cnf(17431,plain,
( ~ aElementOf0(xn,szNzAzT0)
| ~ aElementOf0(xm,szNzAzT0)
| sdtlseqdt0(xn,xm) ),
inference(res,[status(thm),theory(equality)],[2834,17341]),
[iquote('2:Res:2834.3,17341.0')] ).
cnf(17434,plain,
sdtlseqdt0(xn,xm),
inference(mrr,[status(thm)],[17431,6,5]),
[iquote('2:MRR:17431.0,17431.1,6.0,5.0')] ).
cnf(37984,plain,
( ~ sdtlseqdt0(xn,xm)
| ~ aElementOf0(xm,szNzAzT0)
| ~ aElementOf0(xn,szNzAzT0)
| equal(szszuzczcdt0(xn),szszuzczcdt0(xm)) ),
inference(res,[status(thm),theory(equality)],[17342,5813]),
[iquote('2:Res:17342.0,5813.0')] ).
cnf(38053,plain,
equal(szszuzczcdt0(xn),szszuzczcdt0(xm)),
inference(mrr,[status(thm)],[37984,17434,5,6]),
[iquote('2:MRR:37984.0,37984.1,37984.2,17434.0,5.0,6.0')] ).
cnf(38461,plain,
( ~ aElementOf0(xn,szNzAzT0)
| equal(skf13(szszuzczcdt0(xm)),xn) ),
inference(spr,[status(thm),theory(equality)],[38053,3549]),
[iquote('2:SpR:38053.0,3549.1')] ).
cnf(38555,plain,
equal(skf13(szszuzczcdt0(xm)),xn),
inference(mrr,[status(thm)],[38461,6]),
[iquote('2:MRR:38461.0,6.0')] ).
cnf(39032,plain,
( ~ aElementOf0(xm,szNzAzT0)
| equal(xn,xm) ),
inference(spr,[status(thm),theory(equality)],[38555,3549]),
[iquote('2:SpR:38555.0,3549.1')] ).
cnf(39087,plain,
$false,
inference(mrr,[status(thm)],[39032,5,2853]),
[iquote('2:MRR:39032.0,39032.1,5.0,2853.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.14 % Problem : NUM541+1 : TPTP v8.1.0. Released v4.0.0.
% 0.08/0.15 % Command : run_spass %d %s
% 0.15/0.37 % Computer : n020.cluster.edu
% 0.15/0.37 % Model : x86_64 x86_64
% 0.15/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.37 % Memory : 8042.1875MB
% 0.15/0.37 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.37 % CPULimit : 300
% 0.15/0.37 % WCLimit : 600
% 0.15/0.37 % DateTime : Wed Jul 6 19:53:29 EDT 2022
% 0.15/0.37 % CPUTime :
% 53.81/54.02
% 53.81/54.02 SPASS V 3.9
% 53.81/54.02 SPASS beiseite: Proof found.
% 53.81/54.02 % SZS status Theorem
% 53.81/54.02 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 53.81/54.02 SPASS derived 27530 clauses, backtracked 4430 clauses, performed 53 splits and kept 12359 clauses.
% 53.81/54.02 SPASS allocated 128277 KBytes.
% 53.81/54.02 SPASS spent 0:0:53.60 on the problem.
% 53.81/54.02 0:00:00.04 for the input.
% 53.81/54.02 0:00:00.11 for the FLOTTER CNF translation.
% 53.81/54.02 0:00:00.57 for inferences.
% 53.81/54.02 0:00:00.65 for the backtracking.
% 53.81/54.02 0:0:51.91 for the reduction.
% 53.81/54.02
% 53.81/54.02
% 53.81/54.02 Here is a proof with depth 7, length 78 :
% 53.81/54.02 % SZS output start Refutation
% See solution above
% 56.76/56.96 Formulae used in the proof : m__1936 mNatExtra mLessRefl mSuccNum mLessSucc mNatNSucc m__ mLessTotal mSuccLess mDefSeg mLessASymm mLessTrans
% 56.76/56.96
%------------------------------------------------------------------------------