%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : NUM538+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:15 EDT 2022
% Result : Theorem 18.94s 19.16s
% Output : Refutation 18.94s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 11
% Syntax : Number of clauses : 28 ( 9 unt; 9 nHn; 28 RR)
% Number of literals : 89 ( 0 equ; 55 neg)
% Maximal clause size : 7 ( 3 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 7 ( 6 usr; 1 prp; 0-3 aty)
% Number of functors : 10 ( 10 usr; 6 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(4,axiom,
aSet0(xS),
file('NUM538+1.p',unknown),
[] ).
cnf(5,axiom,
isFinite0(xS),
file('NUM538+1.p',unknown),
[] ).
cnf(7,axiom,
aElementOf0(xx,xS),
file('NUM538+1.p',unknown),
[] ).
cnf(22,axiom,
~ equal(szszuzczcdt0(sbrdtbr0(sdtmndt0(xS,xx))),sbrdtbr0(xS)),
file('NUM538+1.p',unknown),
[] ).
cnf(23,axiom,
( ~ aSet0(u)
| ~ aElementOf0(v,u)
| aElement0(v) ),
file('NUM538+1.p',unknown),
[] ).
cnf(26,axiom,
( ~ equal(u,v)
| ~ skP1(v,w,u) ),
file('NUM538+1.p',unknown),
[] ).
cnf(43,axiom,
( ~ isFinite0(u)
| ~ aSet0(u)
| ~ aElement0(v)
| isFinite0(sdtmndt0(u,v)) ),
file('NUM538+1.p',unknown),
[] ).
cnf(47,axiom,
( ~ aElement0(u)
| ~ aSet0(v)
| ~ equal(w,sdtmndt0(v,u))
| aSet0(w) ),
file('NUM538+1.p',unknown),
[] ).
cnf(49,axiom,
( ~ aSet0(u)
| ~ aElementOf0(v,u)
| equal(sdtpldt0(sdtmndt0(u,v),v),u) ),
file('NUM538+1.p',unknown),
[] ).
cnf(58,axiom,
( ~ aElement0(u)
| ~ isFinite0(v)
| ~ aSet0(v)
| aElementOf0(u,v)
| equal(sbrdtbr0(sdtpldt0(v,u)),szszuzczcdt0(sbrdtbr0(v))) ),
file('NUM538+1.p',unknown),
[] ).
cnf(60,axiom,
( ~ aElement0(u)
| ~ aSet0(v)
| ~ aElementOf0(w,x)
| ~ equal(x,sdtmndt0(v,u))
| skP1(u,v,w) ),
file('NUM538+1.p',unknown),
[] ).
cnf(97,plain,
( ~ aSet0(xS)
| aElement0(xx) ),
inference(res,[status(thm),theory(equality)],[7,23]),
[iquote('0:Res:7.0,23.1')] ).
cnf(101,plain,
aElement0(xx),
inference(ssi,[status(thm)],[97,5,4]),
[iquote('0:SSi:97.0,5.0,4.0')] ).
cnf(189,plain,
( ~ aElement0(u)
| ~ aSet0(v)
| aSet0(sdtmndt0(v,u)) ),
inference(eqr,[status(thm),theory(equality)],[47]),
[iquote('0:EqR:47.2')] ).
cnf(887,plain,
( ~ aSet0(u)
| ~ aElement0(v)
| ~ isFinite0(sdtmndt0(u,v))
| ~ aSet0(sdtmndt0(u,v))
| ~ aElementOf0(v,u)
| aElementOf0(v,sdtmndt0(u,v))
| equal(szszuzczcdt0(sbrdtbr0(sdtmndt0(u,v))),sbrdtbr0(u)) ),
inference(spr,[status(thm),theory(equality)],[49,58]),
[iquote('0:SpR:49.2,58.4')] ).
cnf(897,plain,
( ~ aSet0(u)
| ~ aElement0(v)
| ~ isFinite0(sdtmndt0(u,v))
| ~ aElementOf0(v,u)
| aElementOf0(v,sdtmndt0(u,v))
| equal(szszuzczcdt0(sbrdtbr0(sdtmndt0(u,v))),sbrdtbr0(u)) ),
inference(ssi,[status(thm)],[887,189]),
[iquote('0:SSi:887.3,189.2')] ).
cnf(898,plain,
( ~ aSet0(u)
| ~ isFinite0(sdtmndt0(u,v))
| ~ aElementOf0(v,u)
| aElementOf0(v,sdtmndt0(u,v))
| equal(szszuzczcdt0(sbrdtbr0(sdtmndt0(u,v))),sbrdtbr0(u)) ),
inference(mrr,[status(thm)],[897,23]),
[iquote('0:MRR:897.1,23.2')] ).
cnf(965,plain,
( ~ aElement0(u)
| ~ aSet0(v)
| ~ aElementOf0(w,sdtmndt0(v,u))
| skP1(u,v,w) ),
inference(eqr,[status(thm),theory(equality)],[60]),
[iquote('0:EqR:60.3')] ).
cnf(3913,plain,
( ~ aSet0(u)
| ~ aElement0(v)
| ~ aSet0(u)
| ~ isFinite0(u)
| ~ aElementOf0(v,u)
| aElementOf0(v,sdtmndt0(u,v))
| equal(szszuzczcdt0(sbrdtbr0(sdtmndt0(u,v))),sbrdtbr0(u)) ),
inference(sor,[status(thm)],[898,43]),
[iquote('0:SoR:898.1,43.3')] ).
cnf(3918,plain,
( ~ aElement0(u)
| ~ aSet0(v)
| ~ isFinite0(v)
| ~ aElementOf0(u,v)
| aElementOf0(u,sdtmndt0(v,u))
| equal(szszuzczcdt0(sbrdtbr0(sdtmndt0(v,u))),sbrdtbr0(v)) ),
inference(obv,[status(thm),theory(equality)],[3913]),
[iquote('0:Obv:3913.0')] ).
cnf(3919,plain,
( ~ aSet0(u)
| ~ isFinite0(u)
| ~ aElementOf0(v,u)
| aElementOf0(v,sdtmndt0(u,v))
| equal(szszuzczcdt0(sbrdtbr0(sdtmndt0(u,v))),sbrdtbr0(u)) ),
inference(mrr,[status(thm)],[3918,23]),
[iquote('0:MRR:3918.0,23.2')] ).
cnf(34853,plain,
( ~ aSet0(xS)
| ~ isFinite0(xS)
| aElementOf0(xx,sdtmndt0(xS,xx))
| equal(szszuzczcdt0(sbrdtbr0(sdtmndt0(xS,xx))),sbrdtbr0(xS)) ),
inference(res,[status(thm),theory(equality)],[7,3919]),
[iquote('0:Res:7.0,3919.2')] ).
cnf(34863,plain,
( aElementOf0(xx,sdtmndt0(xS,xx))
| equal(szszuzczcdt0(sbrdtbr0(sdtmndt0(xS,xx))),sbrdtbr0(xS)) ),
inference(ssi,[status(thm)],[34853,5,4]),
[iquote('0:SSi:34853.1,34853.0,5.0,4.0,5.0,4.0')] ).
cnf(34864,plain,
aElementOf0(xx,sdtmndt0(xS,xx)),
inference(mrr,[status(thm)],[34863,22]),
[iquote('0:MRR:34863.1,22.0')] ).
cnf(34900,plain,
( ~ aElement0(xx)
| ~ aSet0(xS)
| skP1(xx,xS,xx) ),
inference(res,[status(thm),theory(equality)],[34864,965]),
[iquote('0:Res:34864.0,965.2')] ).
cnf(34902,plain,
skP1(xx,xS,xx),
inference(ssi,[status(thm)],[34900,5,4,101]),
[iquote('0:SSi:34900.1,34900.0,5.0,4.0,101.0')] ).
cnf(34915,plain,
~ equal(xx,xx),
inference(res,[status(thm),theory(equality)],[34902,26]),
[iquote('0:Res:34902.0,26.1')] ).
cnf(34916,plain,
$false,
inference(obv,[status(thm),theory(equality)],[34915]),
[iquote('0:Obv:34915.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.13 % Problem : NUM538+1 : TPTP v8.1.0. Released v4.0.0.
% 0.04/0.13 % Command : run_spass %d %s
% 0.13/0.35 % Computer : n020.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 600
% 0.13/0.35 % DateTime : Wed Jul 6 20:12:44 EDT 2022
% 0.13/0.35 % CPUTime :
% 18.94/19.16
% 18.94/19.16 SPASS V 3.9
% 18.94/19.16 SPASS beiseite: Proof found.
% 18.94/19.16 % SZS status Theorem
% 18.94/19.16 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 18.94/19.16 SPASS derived 26643 clauses, backtracked 4766 clauses, performed 24 splits and kept 9504 clauses.
% 18.94/19.16 SPASS allocated 124054 KBytes.
% 18.94/19.16 SPASS spent 0:0:16.47 on the problem.
% 18.94/19.16 0:00:00.03 for the input.
% 18.94/19.16 0:00:00.06 for the FLOTTER CNF translation.
% 18.94/19.16 0:00:00.40 for inferences.
% 18.94/19.16 0:00:00.45 for the backtracking.
% 18.94/19.16 0:0:15.37 for the reduction.
% 18.94/19.16
% 18.94/19.16
% 18.94/19.16 Here is a proof with depth 5, length 28 :
% 18.94/19.16 % SZS output start Refutation
% See solution above
% 18.94/19.16 Formulae used in the proof : m__1522 m__1522_02 m__ mEOfElem mDefDiff mFDiffSet mConsDiff mCardCons
% 18.94/19.16
%------------------------------------------------------------------------------