%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : NUM597+3 : TPTP v8.1.0. Released v4.0.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 : 600s
% DateTime : Mon Jul 18 14:27:55 EDT 2022
% Result : Theorem 1.07s 1.24s
% Output : Refutation 1.07s
% Verified :
% SZS Type : Refutation
% Derivation depth : 6
% Number of leaves : 9
% Syntax : Number of clauses : 21 ( 10 unt; 0 nHn; 21 RR)
% Number of literals : 38 ( 0 equ; 22 neg)
% Maximal clause size : 4 ( 1 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 5 ( 4 usr; 1 prp; 0-2 aty)
% Number of functors : 12 ( 12 usr; 7 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(4,axiom,
aSet0(xT),
file('NUM597+3.p',unknown),
[] ).
cnf(29,axiom,
equal(szDzozmdt0(xd),szNzAzT0),
file('NUM597+3.p',unknown),
[] ).
cnf(30,axiom,
~ aElementOf0(szDzizrdt0(xd),xT),
file('NUM597+3.p',unknown),
[] ).
cnf(48,axiom,
aSubsetOf0(sdtlcdtrc0(xd,szDzozmdt0(xd)),xT),
file('NUM597+3.p',unknown),
[] ).
cnf(49,axiom,
aElementOf0(skc94,sdtlbdtrb0(xd,szDzizrdt0(xd))),
file('NUM597+3.p',unknown),
[] ).
cnf(92,axiom,
( ~ aElementOf0(u,sdtlbdtrb0(xd,szDzizrdt0(xd)))
| aElementOf0(u,szDzozmdt0(xd)) ),
file('NUM597+3.p',unknown),
[] ).
cnf(121,axiom,
( ~ aElementOf0(u,sdtlbdtrb0(xd,szDzizrdt0(xd)))
| equal(sdtlpdtrp0(xd,u),szDzizrdt0(xd)) ),
file('NUM597+3.p',unknown),
[] ).
cnf(122,axiom,
( ~ aSet0(u)
| ~ aElementOf0(v,w)
| ~ aSubsetOf0(w,u)
| aElementOf0(v,u) ),
file('NUM597+3.p',unknown),
[] ).
cnf(184,axiom,
( ~ aElementOf0(u,szDzozmdt0(xd))
| ~ equal(sdtlpdtrp0(xd,u),v)
| aElementOf0(v,sdtlcdtrc0(xd,szDzozmdt0(xd))) ),
file('NUM597+3.p',unknown),
[] ).
cnf(353,plain,
aSubsetOf0(sdtlcdtrc0(xd,szNzAzT0),xT),
inference(rew,[status(thm),theory(equality)],[29,48]),
[iquote('0:Rew:29.0,48.0')] ).
cnf(355,plain,
( ~ aElementOf0(u,sdtlbdtrb0(xd,szDzizrdt0(xd)))
| aElementOf0(u,szNzAzT0) ),
inference(rew,[status(thm),theory(equality)],[29,92]),
[iquote('0:Rew:29.0,92.1')] ).
cnf(370,plain,
( ~ aElementOf0(u,szNzAzT0)
| ~ equal(sdtlpdtrp0(xd,u),v)
| aElementOf0(v,sdtlcdtrc0(xd,szNzAzT0)) ),
inference(rew,[status(thm),theory(equality)],[29,184]),
[iquote('0:Rew:29.0,184.2,29.0,184.0')] ).
cnf(446,plain,
( ~ aSet0(xT)
| ~ aSubsetOf0(u,xT)
| ~ aElementOf0(szDzizrdt0(xd),u) ),
inference(res,[status(thm),theory(equality)],[122,30]),
[iquote('0:Res:122.3,30.0')] ).
cnf(452,plain,
( ~ aSubsetOf0(u,xT)
| ~ aElementOf0(szDzizrdt0(xd),u) ),
inference(mrr,[status(thm)],[446,4]),
[iquote('0:MRR:446.0,4.0')] ).
cnf(560,plain,
aElementOf0(skc94,szNzAzT0),
inference(res,[status(thm),theory(equality)],[49,355]),
[iquote('0:Res:49.0,355.0')] ).
cnf(1036,plain,
equal(sdtlpdtrp0(xd,skc94),szDzizrdt0(xd)),
inference(res,[status(thm),theory(equality)],[49,121]),
[iquote('0:Res:49.0,121.0')] ).
cnf(2125,plain,
( ~ aElementOf0(skc94,szNzAzT0)
| ~ equal(szDzizrdt0(xd),u)
| aElementOf0(u,sdtlcdtrc0(xd,szNzAzT0)) ),
inference(spl,[status(thm),theory(equality)],[1036,370]),
[iquote('0:SpL:1036.0,370.1')] ).
cnf(2128,plain,
( ~ equal(szDzizrdt0(xd),u)
| aElementOf0(u,sdtlcdtrc0(xd,szNzAzT0)) ),
inference(mrr,[status(thm)],[2125,560]),
[iquote('0:MRR:2125.0,560.0')] ).
cnf(2143,plain,
( ~ equal(szDzizrdt0(xd),szDzizrdt0(xd))
| ~ aSubsetOf0(sdtlcdtrc0(xd,szNzAzT0),xT) ),
inference(res,[status(thm),theory(equality)],[2128,452]),
[iquote('0:Res:2128.1,452.1')] ).
cnf(2152,plain,
~ aSubsetOf0(sdtlcdtrc0(xd,szNzAzT0),xT),
inference(obv,[status(thm),theory(equality)],[2143]),
[iquote('0:Obv:2143.0')] ).
cnf(2153,plain,
$false,
inference(mrr,[status(thm)],[2152,353]),
[iquote('0:MRR:2152.0,353.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : NUM597+3 : TPTP v8.1.0. Released v4.0.0.
% 0.07/0.13 % Command : run_spass %d %s
% 0.12/0.33 % Computer : n026.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 600
% 0.12/0.34 % DateTime : Thu Jul 7 04:51:39 EDT 2022
% 0.12/0.34 % CPUTime :
% 1.07/1.24
% 1.07/1.24 SPASS V 3.9
% 1.07/1.24 SPASS beiseite: Proof found.
% 1.07/1.24 % SZS status Theorem
% 1.07/1.24 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 1.07/1.24 SPASS derived 1340 clauses, backtracked 111 clauses, performed 4 splits and kept 1033 clauses.
% 1.07/1.24 SPASS allocated 104671 KBytes.
% 1.07/1.24 SPASS spent 0:00:00.89 on the problem.
% 1.07/1.24 0:00:00.03 for the input.
% 1.07/1.24 0:00:00.63 for the FLOTTER CNF translation.
% 1.07/1.24 0:00:00.02 for inferences.
% 1.07/1.24 0:00:00.00 for the backtracking.
% 1.07/1.24 0:00:00.17 for the reduction.
% 1.07/1.24
% 1.07/1.24
% 1.07/1.24 Here is a proof with depth 3, length 21 :
% 1.07/1.24 % SZS output start Refutation
% See solution above
% 1.07/1.24 Formulae used in the proof : m__3291 m__4730 m__ m__4758 m__4868 mDefSub
% 1.07/1.24
%------------------------------------------------------------------------------