%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : RNG090+2 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n023.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 20:41:26 EDT 2022
% Result : Theorem 52.25s 52.43s
% Output : Refutation 52.25s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 16
% Syntax : Number of clauses : 58 ( 21 unt; 0 nHn; 58 RR)
% Number of literals : 142 ( 0 equ; 95 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 : 12 ( 12 usr; 11 con; 0-2 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(3,axiom,
aSet0(xI),
file('RNG090+2.p',unknown),
[] ).
cnf(4,axiom,
aIdeal0(xI),
file('RNG090+2.p',unknown),
[] ).
cnf(5,axiom,
aSet0(xJ),
file('RNG090+2.p',unknown),
[] ).
cnf(6,axiom,
aIdeal0(xJ),
file('RNG090+2.p',unknown),
[] ).
cnf(13,axiom,
aElementOf0(xk,xI),
file('RNG090+2.p',unknown),
[] ).
cnf(14,axiom,
aElementOf0(xl,xJ),
file('RNG090+2.p',unknown),
[] ).
cnf(15,axiom,
aElementOf0(xm,xI),
file('RNG090+2.p',unknown),
[] ).
cnf(16,axiom,
aElementOf0(xn,xJ),
file('RNG090+2.p',unknown),
[] ).
cnf(23,axiom,
equal(sdtpldt0(xk,xl),xx),
file('RNG090+2.p',unknown),
[] ).
cnf(24,axiom,
equal(sdtpldt0(xm,xn),xy),
file('RNG090+2.p',unknown),
[] ).
cnf(26,axiom,
aElementOf0(sdtpldt0(xl,xn),xJ),
file('RNG090+2.p',unknown),
[] ).
cnf(39,axiom,
( ~ aSet0(u)
| ~ aElementOf0(v,u)
| aElement0(v) ),
file('RNG090+2.p',unknown),
[] ).
cnf(42,axiom,
( ~ aElement0(u)
| ~ aElement0(v)
| aElement0(sdtpldt0(v,u)) ),
file('RNG090+2.p',unknown),
[] ).
cnf(48,axiom,
~ equal(sdtpldt0(sdtpldt0(xk,xm),sdtpldt0(xl,xn)),sdtpldt0(xx,xy)),
file('RNG090+2.p',unknown),
[] ).
cnf(51,axiom,
( ~ aElement0(u)
| ~ aElement0(v)
| equal(sdtpldt0(v,u),sdtpldt0(u,v)) ),
file('RNG090+2.p',unknown),
[] ).
cnf(69,axiom,
( ~ aElement0(u)
| ~ aElement0(v)
| ~ aElement0(w)
| equal(sdtpldt0(sdtpldt0(w,v),u),sdtpldt0(w,sdtpldt0(v,u))) ),
file('RNG090+2.p',unknown),
[] ).
cnf(105,plain,
( ~ aSet0(xJ)
| aElement0(xn) ),
inference(res,[status(thm),theory(equality)],[16,39]),
[iquote('0:Res:16.0,39.1')] ).
cnf(106,plain,
( ~ aSet0(xJ)
| aElement0(xl) ),
inference(res,[status(thm),theory(equality)],[14,39]),
[iquote('0:Res:14.0,39.1')] ).
cnf(110,plain,
( ~ aSet0(xJ)
| aElement0(sdtpldt0(xl,xn)) ),
inference(res,[status(thm),theory(equality)],[26,39]),
[iquote('0:Res:26.0,39.1')] ).
cnf(111,plain,
( ~ aSet0(xI)
| aElement0(xm) ),
inference(res,[status(thm),theory(equality)],[15,39]),
[iquote('0:Res:15.0,39.1')] ).
cnf(112,plain,
( ~ aSet0(xI)
| aElement0(xk) ),
inference(res,[status(thm),theory(equality)],[13,39]),
[iquote('0:Res:13.0,39.1')] ).
cnf(121,plain,
aElement0(xn),
inference(ssi,[status(thm)],[105,6,5]),
[iquote('0:SSi:105.0,6.0,5.0')] ).
cnf(122,plain,
aElement0(xl),
inference(ssi,[status(thm)],[106,6,5]),
[iquote('0:SSi:106.0,6.0,5.0')] ).
cnf(125,plain,
aElement0(xm),
inference(ssi,[status(thm)],[111,4,3]),
[iquote('0:SSi:111.0,4.0,3.0')] ).
cnf(126,plain,
aElement0(xk),
inference(ssi,[status(thm)],[112,4,3]),
[iquote('0:SSi:112.0,4.0,3.0')] ).
cnf(130,plain,
aElement0(sdtpldt0(xl,xn)),
inference(ssi,[status(thm)],[110,6,5]),
[iquote('0:SSi:110.0,6.0,5.0')] ).
cnf(153,plain,
( ~ aElement0(xn)
| ~ aElement0(xm)
| aElement0(xy) ),
inference(spr,[status(thm),theory(equality)],[24,42]),
[iquote('0:SpR:24.0,42.2')] ).
cnf(161,plain,
aElement0(xy),
inference(ssi,[status(thm)],[153,125,121]),
[iquote('0:SSi:153.1,153.0,125.0,121.0')] ).
cnf(823,plain,
( ~ aElement0(u)
| ~ aElement0(xn)
| ~ aElement0(xm)
| equal(sdtpldt0(xm,sdtpldt0(xn,u)),sdtpldt0(xy,u)) ),
inference(spr,[status(thm),theory(equality)],[24,69]),
[iquote('0:SpR:24.0,69.3')] ).
cnf(824,plain,
( ~ aElement0(u)
| ~ aElement0(xl)
| ~ aElement0(xk)
| equal(sdtpldt0(xk,sdtpldt0(xl,u)),sdtpldt0(xx,u)) ),
inference(spr,[status(thm),theory(equality)],[23,69]),
[iquote('0:SpR:23.0,69.3')] ).
cnf(832,plain,
( ~ aElement0(u)
| ~ aElement0(v)
| ~ aElement0(w)
| ~ aElement0(v)
| ~ aElement0(u)
| equal(sdtpldt0(sdtpldt0(v,u),w),sdtpldt0(u,sdtpldt0(v,w))) ),
inference(spr,[status(thm),theory(equality)],[51,69]),
[iquote('0:SpR:51.2,69.3')] ).
cnf(837,plain,
( ~ aElement0(sdtpldt0(xl,xn))
| ~ aElement0(xm)
| ~ aElement0(xk)
| ~ equal(sdtpldt0(xk,sdtpldt0(xm,sdtpldt0(xl,xn))),sdtpldt0(xx,xy)) ),
inference(spl,[status(thm),theory(equality)],[69,48]),
[iquote('0:SpL:69.3,48.0')] ).
cnf(838,plain,
( ~ aElement0(u)
| equal(sdtpldt0(xm,sdtpldt0(xn,u)),sdtpldt0(xy,u)) ),
inference(ssi,[status(thm)],[823,125,121]),
[iquote('0:SSi:823.2,823.1,125.0,121.0')] ).
cnf(839,plain,
( ~ aElement0(u)
| equal(sdtpldt0(xk,sdtpldt0(xl,u)),sdtpldt0(xx,u)) ),
inference(ssi,[status(thm)],[824,126,122]),
[iquote('0:SSi:824.2,824.1,126.0,122.0')] ).
cnf(848,plain,
~ equal(sdtpldt0(xk,sdtpldt0(xm,sdtpldt0(xl,xn))),sdtpldt0(xx,xy)),
inference(ssi,[status(thm)],[837,126,125,130]),
[iquote('0:SSi:837.2,837.1,837.0,126.0,125.0,130.0')] ).
cnf(858,plain,
( ~ aElement0(u)
| ~ aElement0(v)
| ~ aElement0(w)
| equal(sdtpldt0(sdtpldt0(v,w),u),sdtpldt0(w,sdtpldt0(v,u))) ),
inference(obv,[status(thm),theory(equality)],[832]),
[iquote('0:Obv:832.1')] ).
cnf(859,plain,
( ~ aElement0(u)
| ~ aElement0(v)
| ~ aElement0(w)
| equal(sdtpldt0(v,sdtpldt0(w,u)),sdtpldt0(w,sdtpldt0(v,u))) ),
inference(rew,[status(thm),theory(equality)],[69,858]),
[iquote('0:Rew:69.3,858.3')] ).
cnf(1208,plain,
( ~ aElement0(u)
| ~ aElement0(xn)
| ~ aElement0(u)
| equal(sdtpldt0(xm,sdtpldt0(u,xn)),sdtpldt0(xy,u)) ),
inference(spr,[status(thm),theory(equality)],[51,838]),
[iquote('0:SpR:51.2,838.1')] ).
cnf(1218,plain,
( ~ aElement0(xn)
| ~ aElement0(u)
| equal(sdtpldt0(xm,sdtpldt0(u,xn)),sdtpldt0(xy,u)) ),
inference(obv,[status(thm),theory(equality)],[1208]),
[iquote('0:Obv:1208.0')] ).
cnf(1219,plain,
( ~ aElement0(u)
| equal(sdtpldt0(xm,sdtpldt0(u,xn)),sdtpldt0(xy,u)) ),
inference(ssi,[status(thm)],[1218,121]),
[iquote('0:SSi:1218.0,121.0')] ).
cnf(1644,plain,
( ~ aElement0(u)
| ~ aElement0(xl)
| ~ aElement0(u)
| equal(sdtpldt0(xk,sdtpldt0(u,xl)),sdtpldt0(xx,u)) ),
inference(spr,[status(thm),theory(equality)],[51,839]),
[iquote('0:SpR:51.2,839.1')] ).
cnf(1654,plain,
( ~ aElement0(xl)
| ~ aElement0(u)
| equal(sdtpldt0(xk,sdtpldt0(u,xl)),sdtpldt0(xx,u)) ),
inference(obv,[status(thm),theory(equality)],[1644]),
[iquote('0:Obv:1644.0')] ).
cnf(1655,plain,
( ~ aElement0(u)
| equal(sdtpldt0(xk,sdtpldt0(u,xl)),sdtpldt0(xx,u)) ),
inference(ssi,[status(thm)],[1654,122]),
[iquote('0:SSi:1654.0,122.0')] ).
cnf(9905,plain,
( ~ aElement0(xn)
| ~ aElement0(u)
| ~ aElement0(xm)
| equal(sdtpldt0(xm,sdtpldt0(u,xn)),sdtpldt0(u,xy)) ),
inference(spr,[status(thm),theory(equality)],[24,859]),
[iquote('0:SpR:24.0,859.3')] ).
cnf(9907,plain,
( ~ aElement0(xl)
| ~ aElement0(u)
| ~ aElement0(xk)
| equal(sdtpldt0(xk,sdtpldt0(u,xl)),sdtpldt0(u,xx)) ),
inference(spr,[status(thm),theory(equality)],[23,859]),
[iquote('0:SpR:23.0,859.3')] ).
cnf(10178,plain,
( ~ aElement0(xn)
| ~ aElement0(xl)
| ~ aElement0(xm)
| ~ equal(sdtpldt0(xk,sdtpldt0(xl,sdtpldt0(xm,xn))),sdtpldt0(xx,xy)) ),
inference(spl,[status(thm),theory(equality)],[859,848]),
[iquote('0:SpL:859.3,848.0')] ).
cnf(10185,plain,
( ~ aElement0(xn)
| ~ aElement0(u)
| ~ aElement0(xm)
| equal(sdtpldt0(xy,u),sdtpldt0(u,xy)) ),
inference(rew,[status(thm),theory(equality)],[1219,9905]),
[iquote('0:Rew:1219.1,9905.3')] ).
cnf(10186,plain,
( ~ aElement0(u)
| equal(sdtpldt0(xy,u),sdtpldt0(u,xy)) ),
inference(ssi,[status(thm)],[10185,125,121]),
[iquote('0:SSi:10185.2,10185.0,125.0,121.0')] ).
cnf(10187,plain,
( ~ aElement0(xl)
| ~ aElement0(u)
| ~ aElement0(xk)
| equal(sdtpldt0(xx,u),sdtpldt0(u,xx)) ),
inference(rew,[status(thm),theory(equality)],[1655,9907]),
[iquote('0:Rew:1655.1,9907.3')] ).
cnf(10188,plain,
( ~ aElement0(u)
| equal(sdtpldt0(xx,u),sdtpldt0(u,xx)) ),
inference(ssi,[status(thm)],[10187,126,122]),
[iquote('0:SSi:10187.2,10187.0,126.0,122.0')] ).
cnf(10291,plain,
( ~ aElement0(xn)
| ~ aElement0(xl)
| ~ aElement0(xm)
| ~ equal(sdtpldt0(xk,sdtpldt0(xl,xy)),sdtpldt0(xx,xy)) ),
inference(rew,[status(thm),theory(equality)],[24,10178]),
[iquote('0:Rew:24.0,10178.3')] ).
cnf(10292,plain,
( ~ aElement0(xn)
| ~ aElement0(xl)
| ~ aElement0(xm)
| ~ equal(sdtpldt0(xk,sdtpldt0(xy,xl)),sdtpldt0(xx,xy)) ),
inference(rew,[status(thm),theory(equality)],[10186,10291]),
[iquote('0:Rew:10186.1,10291.3')] ).
cnf(10293,plain,
~ equal(sdtpldt0(xk,sdtpldt0(xy,xl)),sdtpldt0(xx,xy)),
inference(ssi,[status(thm)],[10292,125,122,121]),
[iquote('0:SSi:10292.2,10292.1,10292.0,125.0,122.0,121.0')] ).
cnf(33045,plain,
( ~ aElement0(xl)
| ~ aElement0(xy)
| ~ aElement0(xk)
| ~ equal(sdtpldt0(xy,sdtpldt0(xk,xl)),sdtpldt0(xx,xy)) ),
inference(spl,[status(thm),theory(equality)],[859,10293]),
[iquote('0:SpL:859.3,10293.0')] ).
cnf(33050,plain,
( ~ aElement0(xl)
| ~ aElement0(xy)
| ~ aElement0(xk)
| ~ equal(sdtpldt0(xy,xx),sdtpldt0(xx,xy)) ),
inference(rew,[status(thm),theory(equality)],[23,33045]),
[iquote('0:Rew:23.0,33045.3')] ).
cnf(33051,plain,
( ~ aElement0(xl)
| ~ aElement0(xy)
| ~ aElement0(xk)
| ~ equal(sdtpldt0(xx,xy),sdtpldt0(xx,xy)) ),
inference(rew,[status(thm),theory(equality)],[10188,33050]),
[iquote('0:Rew:10188.1,33050.3')] ).
cnf(33052,plain,
( ~ aElement0(xl)
| ~ aElement0(xy)
| ~ aElement0(xk) ),
inference(obv,[status(thm),theory(equality)],[33051]),
[iquote('0:Obv:33051.3')] ).
cnf(33053,plain,
$false,
inference(ssi,[status(thm)],[33052,126,161,122]),
[iquote('0:SSi:33052.2,33052.1,33052.0,126.0,161.0,122.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : RNG090+2 : TPTP v8.1.0. Released v4.0.0.
% 0.03/0.13 % Command : run_spass %d %s
% 0.13/0.35 % Computer : n023.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 : Mon May 30 13:57:57 EDT 2022
% 0.13/0.35 % CPUTime :
% 52.25/52.43
% 52.25/52.43 SPASS V 3.9
% 52.25/52.43 SPASS beiseite: Proof found.
% 52.25/52.43 % SZS status Theorem
% 52.25/52.43 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 52.25/52.43 SPASS derived 18036 clauses, backtracked 0 clauses, performed 1 splits and kept 5291 clauses.
% 52.25/52.43 SPASS allocated 136110 KBytes.
% 52.25/52.43 SPASS spent 0:0:44.03 on the problem.
% 52.25/52.43 0:00:00.03 for the input.
% 52.25/52.43 0:00:00.10 for the FLOTTER CNF translation.
% 52.25/52.43 0:00:00.19 for inferences.
% 52.25/52.43 0:00:00.07 for the backtracking.
% 52.25/52.43 0:0:43.54 for the reduction.
% 52.25/52.43
% 52.25/52.43
% 52.25/52.43 Here is a proof with depth 3, length 58 :
% 52.25/52.43 % SZS output start Refutation
% See solution above
% 52.25/52.43 Formulae used in the proof : m__870 m__934 m__967 m__994 mEOfElem mSortsB m__ mAddComm mAddAsso
% 52.25/52.43
%------------------------------------------------------------------------------