%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : SYN138-1 : TPTP v8.1.0. Released v1.1.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n013.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 : Thu Jul 21 12:18:58 EDT 2022
% Result : Unsatisfiable 0.42s 0.60s
% Output : Refutation 0.42s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 60
% Syntax : Number of clauses : 145 ( 65 unt; 0 nHn; 145 RR)
% Number of literals : 281 ( 0 equ; 142 neg)
% Maximal clause size : 5 ( 1 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 32 ( 31 usr; 1 prp; 0-3 aty)
% Number of functors : 9 ( 9 usr; 9 con; 0-0 aty)
% Number of variables : 0 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(1,axiom,
~ m3(c,e,c),
file('SYN138-1.p',unknown),
[] ).
cnf(2,axiom,
s0(d),
file('SYN138-1.p',unknown),
[] ).
cnf(4,axiom,
n0(d,e),
file('SYN138-1.p',unknown),
[] ).
cnf(6,axiom,
s0(b),
file('SYN138-1.p',unknown),
[] ).
cnf(10,axiom,
r0(b),
file('SYN138-1.p',unknown),
[] ).
cnf(12,axiom,
n0(e,b),
file('SYN138-1.p',unknown),
[] ).
cnf(13,axiom,
m0(a,u,a),
file('SYN138-1.p',unknown),
[] ).
cnf(14,axiom,
r0(e),
file('SYN138-1.p',unknown),
[] ).
cnf(15,axiom,
p0(b,u),
file('SYN138-1.p',unknown),
[] ).
cnf(16,axiom,
n0(a,b),
file('SYN138-1.p',unknown),
[] ).
cnf(18,axiom,
q0(u,d),
file('SYN138-1.p',unknown),
[] ).
cnf(20,axiom,
m0(u,d,v),
file('SYN138-1.p',unknown),
[] ).
cnf(21,axiom,
l0(a),
file('SYN138-1.p',unknown),
[] ).
cnf(25,axiom,
l0(c),
file('SYN138-1.p',unknown),
[] ).
cnf(27,axiom,
n0(d,c),
file('SYN138-1.p',unknown),
[] ).
cnf(29,axiom,
k0(e),
file('SYN138-1.p',unknown),
[] ).
cnf(32,axiom,
m0(b,b,e),
file('SYN138-1.p',unknown),
[] ).
cnf(33,axiom,
k0(b),
file('SYN138-1.p',unknown),
[] ).
cnf(35,axiom,
n0(c,d),
file('SYN138-1.p',unknown),
[] ).
cnf(37,axiom,
q0(a,b),
file('SYN138-1.p',unknown),
[] ).
cnf(38,axiom,
n0(b,a),
file('SYN138-1.p',unknown),
[] ).
cnf(40,axiom,
( ~ n0(u,v)
| k1(v) ),
file('SYN138-1.p',unknown),
[] ).
cnf(41,axiom,
( ~ n0(u,v)
| l1(v,v) ),
file('SYN138-1.p',unknown),
[] ).
cnf(55,axiom,
( ~ m1(u,v,w)
| ~ m1(u,w,x)
| m1(x,w,w) ),
file('SYN138-1.p',unknown),
[] ).
cnf(60,axiom,
( ~ k0(u)
| ~ l0(v)
| m1(v,u,v) ),
file('SYN138-1.p',unknown),
[] ).
cnf(63,axiom,
( ~ m0(a,u,a)
| ~ q0(v,w)
| ~ m1(w,c,w)
| m1(v,a,w) ),
file('SYN138-1.p',unknown),
[] ).
cnf(68,axiom,
( ~ s0(u)
| ~ p0(u,v)
| m1(u,v,u) ),
file('SYN138-1.p',unknown),
[] ).
cnf(75,axiom,
( ~ m0(b,u,v)
| n1(v,v,u) ),
file('SYN138-1.p',unknown),
[] ).
cnf(124,axiom,
( ~ p0(u,v)
| p1(v,v,v) ),
file('SYN138-1.p',unknown),
[] ).
cnf(146,axiom,
( ~ m0(u,d,u)
| ~ m0(e,d,u)
| q1(e,u,u) ),
file('SYN138-1.p',unknown),
[] ).
cnf(152,axiom,
( ~ r0(u)
| ~ m1(v,w,w)
| q1(v,v,w) ),
file('SYN138-1.p',unknown),
[] ).
cnf(160,axiom,
( ~ m0(u,v,w)
| q1(w,w,w) ),
file('SYN138-1.p',unknown),
[] ).
cnf(163,axiom,
( ~ q0(u,v)
| ~ s0(d)
| ~ q1(d,v,d)
| r1(u) ),
file('SYN138-1.p',unknown),
[] ).
cnf(164,axiom,
( ~ p0(u,u)
| s1(u) ),
file('SYN138-1.p',unknown),
[] ).
cnf(165,axiom,
( ~ s1(u)
| ~ q0(v,w)
| s1(v) ),
file('SYN138-1.p',unknown),
[] ).
cnf(166,axiom,
( ~ k1(u)
| ~ k2(u,v)
| ~ m1(w,v,x)
| k2(x,v) ),
file('SYN138-1.p',unknown),
[] ).
cnf(168,axiom,
( ~ q1(u,v,v)
| k2(v,v) ),
file('SYN138-1.p',unknown),
[] ).
cnf(170,axiom,
( ~ s1(u)
| ~ l2(v,v)
| ~ n0(e,v)
| l2(u,v) ),
file('SYN138-1.p',unknown),
[] ).
cnf(172,axiom,
( ~ s1(u)
| ~ p0(v,v)
| ~ m0(w,u,x)
| l2(x,x) ),
file('SYN138-1.p',unknown),
[] ).
cnf(175,axiom,
( ~ k1(b)
| m2(b) ),
file('SYN138-1.p',unknown),
[] ).
cnf(176,axiom,
( ~ p1(u,v,w)
| n2(w) ),
file('SYN138-1.p',unknown),
[] ).
cnf(194,axiom,
( ~ k1(u)
| ~ p2(e,v,w)
| p2(v,w,w) ),
file('SYN138-1.p',unknown),
[] ).
cnf(213,axiom,
( ~ n2(u)
| ~ k1(e)
| p2(u,u,u) ),
file('SYN138-1.p',unknown),
[] ).
cnf(215,axiom,
( ~ m1(u,v,u)
| p2(v,u,v) ),
file('SYN138-1.p',unknown),
[] ).
cnf(216,axiom,
( ~ k0(u)
| ~ p1(v,v,v)
| q2(v,u,u) ),
file('SYN138-1.p',unknown),
[] ).
cnf(220,axiom,
( ~ p1(u,u,u)
| q2(u,u,u) ),
file('SYN138-1.p',unknown),
[] ).
cnf(222,axiom,
( ~ k1(u)
| ~ l0(c)
| ~ l2(u,v)
| q2(v,c,u) ),
file('SYN138-1.p',unknown),
[] ).
cnf(225,axiom,
( ~ l1(u,v)
| q2(v,v,u) ),
file('SYN138-1.p',unknown),
[] ).
cnf(226,axiom,
( ~ k0(u)
| ~ r1(u)
| ~ q2(u,u,u)
| ~ m0(v,w,x)
| q2(x,u,x) ),
file('SYN138-1.p',unknown),
[] ).
cnf(227,axiom,
( ~ l0(u)
| ~ r1(u)
| r2(u) ),
file('SYN138-1.p',unknown),
[] ).
cnf(228,axiom,
( ~ s1(b)
| ~ q2(b,u,b)
| s2(u) ),
file('SYN138-1.p',unknown),
[] ).
cnf(270,axiom,
( ~ r2(u)
| ~ k2(c,v)
| m3(u,v,u) ),
file('SYN138-1.p',unknown),
[] ).
cnf(279,axiom,
( ~ p2(u,v,w)
| n3(w) ),
file('SYN138-1.p',unknown),
[] ).
cnf(283,axiom,
( ~ n2(u)
| p3(u,u,u) ),
file('SYN138-1.p',unknown),
[] ).
cnf(294,axiom,
( ~ n0(u,v)
| ~ q2(u,v,w)
| q3(v,w) ),
file('SYN138-1.p',unknown),
[] ).
cnf(296,axiom,
( ~ s2(u)
| ~ q3(v,u)
| ~ n1(w,u,v)
| q3(u,v) ),
file('SYN138-1.p',unknown),
[] ).
cnf(306,axiom,
( ~ p2(u,v,w)
| r3(u,w,u) ),
file('SYN138-1.p',unknown),
[] ).
cnf(313,axiom,
( ~ n0(c,d)
| ~ q3(e,b)
| ~ n3(e)
| k4(c) ),
file('SYN138-1.p',unknown),
[] ).
cnf(315,axiom,
( ~ q3(u,u)
| ~ r3(u,e,v)
| ~ q1(a,a,v)
| k4(e) ),
file('SYN138-1.p',unknown),
[] ).
cnf(338,axiom,
( ~ l1(u,v)
| ~ p3(w,v,x)
| s4(u) ),
file('SYN138-1.p',unknown),
[] ).
cnf(394,plain,
( ~ n3(e)
| ~ q3(e,b)
| k4(c) ),
inference(mrr,[status(thm)],[313,35]),
[iquote('0:MRR:313.0,35.0')] ).
cnf(400,plain,
( ~ k1(u)
| ~ l2(u,v)
| q2(v,c,u) ),
inference(mrr,[status(thm)],[222,25]),
[iquote('0:MRR:222.1,25.0')] ).
cnf(401,plain,
( ~ q0(u,v)
| ~ q1(d,v,d)
| r1(u) ),
inference(mrr,[status(thm)],[163,2]),
[iquote('0:MRR:163.1,2.0')] ).
cnf(403,plain,
q1(e,u,u),
inference(mrr,[status(thm)],[146,20]),
[iquote('0:MRR:146.0,146.1,20.0,20.0')] ).
cnf(416,plain,
( ~ q0(u,v)
| ~ m1(v,c,v)
| m1(u,a,v) ),
inference(mrr,[status(thm)],[63,13]),
[iquote('0:MRR:63.0,13.0')] ).
cnf(419,plain,
( ~ r2(c)
| ~ k2(c,e) ),
inference(res,[status(thm),theory(equality)],[270,1]),
[iquote('0:Res:270.2,1.0')] ).
cnf(455,plain,
s1(b),
inference(res,[status(thm),theory(equality)],[15,164]),
[iquote('0:Res:15.0,164.0')] ).
cnf(456,plain,
( ~ q2(b,u,b)
| s2(u) ),
inference(mrr,[status(thm)],[228,455]),
[iquote('0:MRR:228.0,455.0')] ).
cnf(457,plain,
k1(a),
inference(res,[status(thm),theory(equality)],[38,40]),
[iquote('0:Res:38.0,40.0')] ).
cnf(459,plain,
k1(c),
inference(res,[status(thm),theory(equality)],[27,40]),
[iquote('0:Res:27.0,40.0')] ).
cnf(460,plain,
k1(e),
inference(res,[status(thm),theory(equality)],[4,40]),
[iquote('0:Res:4.0,40.0')] ).
cnf(461,plain,
k1(b),
inference(res,[status(thm),theory(equality)],[16,40]),
[iquote('0:Res:16.0,40.0')] ).
cnf(468,plain,
( ~ n2(u)
| p2(u,u,u) ),
inference(mrr,[status(thm)],[213,460]),
[iquote('0:MRR:213.1,460.0')] ).
cnf(469,plain,
m2(b),
inference(mrr,[status(thm)],[175,461]),
[iquote('0:MRR:175.0,461.0')] ).
cnf(472,plain,
l1(a,a),
inference(res,[status(thm),theory(equality)],[38,41]),
[iquote('0:Res:38.0,41.0')] ).
cnf(474,plain,
l1(c,c),
inference(res,[status(thm),theory(equality)],[27,41]),
[iquote('0:Res:27.0,41.0')] ).
cnf(475,plain,
l1(e,e),
inference(res,[status(thm),theory(equality)],[4,41]),
[iquote('0:Res:4.0,41.0')] ).
cnf(476,plain,
l1(b,b),
inference(res,[status(thm),theory(equality)],[16,41]),
[iquote('0:Res:16.0,41.0')] ).
cnf(492,plain,
( ~ n2(u)
| n3(u) ),
inference(res,[status(thm),theory(equality)],[468,279]),
[iquote('0:Res:468.1,279.0')] ).
cnf(493,plain,
( ~ r1(c)
| ~ l0(c)
| ~ k2(c,e) ),
inference(sor,[status(thm)],[419,227]),
[iquote('0:SoR:419.0,227.2')] ).
cnf(496,plain,
( ~ r1(c)
| ~ k2(c,e) ),
inference(ssi,[status(thm)],[493,25,459]),
[iquote('0:SSi:493.1,25.0,459.0')] ).
cnf(504,plain,
q2(b,b,b),
inference(res,[status(thm),theory(equality)],[476,225]),
[iquote('0:Res:476.0,225.0')] ).
cnf(506,plain,
s2(b),
inference(res,[status(thm),theory(equality)],[504,456]),
[iquote('0:Res:504.0,456.0')] ).
cnf(544,plain,
p1(u,u,u),
inference(res,[status(thm),theory(equality)],[15,124]),
[iquote('0:Res:15.0,124.0')] ).
cnf(545,plain,
q2(u,u,u),
inference(mrr,[status(thm)],[220,544]),
[iquote('0:MRR:220.0,544.0')] ).
cnf(546,plain,
( ~ k0(u)
| q2(v,u,u) ),
inference(mrr,[status(thm)],[216,544]),
[iquote('0:MRR:216.1,544.0')] ).
cnf(547,plain,
( ~ k0(u)
| ~ r1(u)
| ~ m0(v,w,x)
| q2(x,u,x) ),
inference(mrr,[status(thm)],[226,545]),
[iquote('0:MRR:226.2,545.0')] ).
cnf(548,plain,
n2(u),
inference(res,[status(thm),theory(equality)],[544,176]),
[iquote('0:Res:544.0,176.0')] ).
cnf(550,plain,
p3(u,u,u),
inference(mrr,[status(thm)],[283,548]),
[iquote('0:MRR:283.0,548.0')] ).
cnf(555,plain,
n3(u),
inference(mrr,[status(thm)],[492,548]),
[iquote('0:MRR:492.0,548.0')] ).
cnf(566,plain,
( ~ q3(e,b)
| k4(c) ),
inference(mrr,[status(thm)],[394,555]),
[iquote('0:MRR:394.0,555.0')] ).
cnf(580,plain,
k2(u,u),
inference(res,[status(thm),theory(equality)],[403,168]),
[iquote('0:Res:403.0,168.0')] ).
cnf(605,plain,
( ~ q0(u,v)
| s1(u) ),
inference(ems,[status(thm)],[165,455]),
[iquote('0:EmS:165.0,455.0')] ).
cnf(611,plain,
s1(u),
inference(res,[status(thm),theory(equality)],[18,605]),
[iquote('0:Res:18.0,605.0')] ).
cnf(617,plain,
( ~ l2(u,u)
| ~ n0(e,u)
| l2(v,u) ),
inference(mrr,[status(thm)],[170,611]),
[iquote('0:MRR:170.0,611.0')] ).
cnf(618,plain,
( ~ p0(u,u)
| ~ m0(v,w,x)
| l2(x,x) ),
inference(mrr,[status(thm)],[172,611]),
[iquote('0:MRR:172.0,611.0')] ).
cnf(625,plain,
n1(e,e,b),
inference(res,[status(thm),theory(equality)],[32,75]),
[iquote('0:Res:32.0,75.0')] ).
cnf(654,plain,
q1(u,u,u),
inference(res,[status(thm),theory(equality)],[20,160]),
[iquote('0:Res:20.0,160.0')] ).
cnf(682,plain,
( ~ q0(u,d)
| r1(u) ),
inference(res,[status(thm),theory(equality)],[654,401]),
[iquote('0:Res:654.0,401.1')] ).
cnf(683,plain,
r1(u),
inference(mrr,[status(thm)],[682,18]),
[iquote('0:MRR:682.0,18.0')] ).
cnf(686,plain,
~ k2(c,e),
inference(mrr,[status(thm)],[496,683]),
[iquote('0:MRR:496.0,683.0')] ).
cnf(688,plain,
( ~ k0(u)
| ~ m0(v,w,x)
| q2(x,u,x) ),
inference(mrr,[status(thm)],[547,683]),
[iquote('0:MRR:547.1,683.0')] ).
cnf(711,plain,
( ~ s0(b)
| m1(b,u,b) ),
inference(res,[status(thm),theory(equality)],[15,68]),
[iquote('0:Res:15.0,68.1')] ).
cnf(712,plain,
m1(b,u,b),
inference(ssi,[status(thm)],[711,6,33,10,469,461,506]),
[iquote('0:SSi:711.0,6.0,33.0,10.0,469.0,461.0,506.0')] ).
cnf(713,plain,
p2(u,b,u),
inference(res,[status(thm),theory(equality)],[712,215]),
[iquote('0:Res:712.0,215.0')] ).
cnf(737,plain,
( ~ l1(u,v)
| s4(u) ),
inference(res,[status(thm),theory(equality)],[550,338]),
[iquote('0:Res:550.0,338.1')] ).
cnf(738,plain,
s4(c),
inference(res,[status(thm),theory(equality)],[474,737]),
[iquote('0:Res:474.0,737.0')] ).
cnf(739,plain,
s4(a),
inference(res,[status(thm),theory(equality)],[472,737]),
[iquote('0:Res:472.0,737.0')] ).
cnf(741,plain,
s4(e),
inference(res,[status(thm),theory(equality)],[475,737]),
[iquote('0:Res:475.0,737.0')] ).
cnf(742,plain,
s4(b),
inference(res,[status(thm),theory(equality)],[476,737]),
[iquote('0:Res:476.0,737.0')] ).
cnf(787,plain,
( ~ p2(e,u,v)
| p2(u,v,v) ),
inference(ems,[status(thm)],[194,461]),
[iquote('0:EmS:194.0,461.0')] ).
cnf(795,plain,
p2(b,e,e),
inference(res,[status(thm),theory(equality)],[713,787]),
[iquote('0:Res:713.0,787.0')] ).
cnf(804,plain,
r3(b,e,b),
inference(res,[status(thm),theory(equality)],[795,306]),
[iquote('0:Res:795.0,306.0')] ).
cnf(894,plain,
( ~ m1(u,v,v)
| q1(u,u,v) ),
inference(ems,[status(thm)],[152,10]),
[iquote('0:EmS:152.0,10.0')] ).
cnf(943,plain,
( ~ k0(u)
| ~ n0(v,u)
| q3(u,u) ),
inference(res,[status(thm),theory(equality)],[546,294]),
[iquote('0:Res:546.1,294.1')] ).
cnf(995,plain,
( ~ p0(u,u)
| l2(v,v) ),
inference(res,[status(thm),theory(equality)],[20,618]),
[iquote('0:Res:20.0,618.1')] ).
cnf(1003,plain,
( ~ k0(u)
| q2(v,u,v) ),
inference(res,[status(thm),theory(equality)],[20,688]),
[iquote('0:Res:20.0,688.1')] ).
cnf(1004,plain,
l2(u,u),
inference(res,[status(thm),theory(equality)],[15,995]),
[iquote('0:Res:15.0,995.0')] ).
cnf(1007,plain,
( ~ n0(e,u)
| l2(v,u) ),
inference(mrr,[status(thm)],[617,1004]),
[iquote('0:MRR:617.0,1004.0')] ).
cnf(1012,plain,
l2(u,b),
inference(res,[status(thm),theory(equality)],[12,1007]),
[iquote('0:Res:12.0,1007.0')] ).
cnf(1015,plain,
( ~ k1(u)
| q2(b,c,u) ),
inference(res,[status(thm),theory(equality)],[1012,400]),
[iquote('0:Res:1012.0,400.1')] ).
cnf(1019,plain,
( ~ k1(b)
| s2(c) ),
inference(res,[status(thm),theory(equality)],[1015,456]),
[iquote('0:Res:1015.1,456.0')] ).
cnf(1022,plain,
s2(c),
inference(ssi,[status(thm)],[1019,6,33,10,469,461,506,742]),
[iquote('0:SSi:1019.0,6.0,33.0,10.0,469.0,461.0,506.0,742.0')] ).
cnf(1042,plain,
( ~ k0(u)
| s2(u) ),
inference(res,[status(thm),theory(equality)],[1003,456]),
[iquote('0:Res:1003.1,456.0')] ).
cnf(1043,plain,
( ~ k0(u)
| ~ n0(v,u)
| q3(u,v) ),
inference(res,[status(thm),theory(equality)],[1003,294]),
[iquote('0:Res:1003.1,294.1')] ).
cnf(1086,plain,
( ~ k0(b)
| q3(b,b) ),
inference(res,[status(thm),theory(equality)],[16,943]),
[iquote('0:Res:16.0,943.1')] ).
cnf(1090,plain,
q3(b,b),
inference(ssi,[status(thm)],[1086,6,33,10,469,461,506,742]),
[iquote('0:SSi:1086.0,6.0,33.0,10.0,469.0,461.0,506.0,742.0')] ).
cnf(1102,plain,
( ~ k0(b)
| q3(b,e) ),
inference(res,[status(thm),theory(equality)],[12,1043]),
[iquote('0:Res:12.0,1043.1')] ).
cnf(1107,plain,
q3(b,e),
inference(ssi,[status(thm)],[1102,6,33,10,469,461,506,742]),
[iquote('0:SSi:1102.0,6.0,33.0,10.0,469.0,461.0,506.0,742.0')] ).
cnf(1126,plain,
( ~ q0(u,b)
| m1(u,a,b) ),
inference(res,[status(thm),theory(equality)],[712,416]),
[iquote('0:Res:712.0,416.1')] ).
cnf(1133,plain,
m1(a,a,b),
inference(res,[status(thm),theory(equality)],[37,1126]),
[iquote('0:Res:37.0,1126.0')] ).
cnf(1316,plain,
( ~ m1(a,b,u)
| m1(u,b,b) ),
inference(res,[status(thm),theory(equality)],[1133,55]),
[iquote('0:Res:1133.0,55.0')] ).
cnf(1389,plain,
( ~ k0(b)
| ~ l0(a)
| m1(a,b,b) ),
inference(res,[status(thm),theory(equality)],[60,1316]),
[iquote('0:Res:60.2,1316.0')] ).
cnf(1390,plain,
m1(a,b,b),
inference(ssi,[status(thm)],[1389,21,457,739,6,33,10,469,461,506,742]),
[iquote('0:SSi:1389.1,1389.0,21.0,457.0,739.0,6.0,33.0,10.0,469.0,461.0,506.0,742.0')] ).
cnf(1395,plain,
( ~ s2(e)
| ~ q3(b,e)
| q3(e,b) ),
inference(res,[status(thm),theory(equality)],[625,296]),
[iquote('0:Res:625.0,296.2')] ).
cnf(1411,plain,
( ~ q3(b,e)
| q3(e,b) ),
inference(ssi,[status(thm)],[1395,1042,29,14,460,741]),
[iquote('0:SSi:1395.0,1042.0,29.0,14.0,460.0,741.1')] ).
cnf(1412,plain,
q3(e,b),
inference(mrr,[status(thm)],[1411,1107]),
[iquote('0:MRR:1411.0,1107.0')] ).
cnf(1413,plain,
k4(c),
inference(mrr,[status(thm)],[566,1412]),
[iquote('0:MRR:566.0,1412.0')] ).
cnf(1437,plain,
q1(a,a,b),
inference(res,[status(thm),theory(equality)],[1390,894]),
[iquote('0:Res:1390.0,894.0')] ).
cnf(1451,plain,
( ~ k0(u)
| ~ l0(v)
| ~ k1(w)
| ~ k2(w,u)
| k2(v,u) ),
inference(res,[status(thm),theory(equality)],[60,166]),
[iquote('0:Res:60.2,166.2')] ).
cnf(1489,plain,
( ~ q3(b,b)
| ~ q1(a,a,b)
| k4(e) ),
inference(res,[status(thm),theory(equality)],[804,315]),
[iquote('0:Res:804.0,315.1')] ).
cnf(1492,plain,
k4(e),
inference(mrr,[status(thm)],[1489,1090,1437]),
[iquote('0:MRR:1489.0,1489.1,1090.0,1437.0')] ).
cnf(2017,plain,
( ~ k0(u)
| ~ l0(v)
| ~ k1(u)
| k2(v,u) ),
inference(res,[status(thm),theory(equality)],[580,1451]),
[iquote('0:Res:580.0,1451.3')] ).
cnf(2310,plain,
( ~ k0(e)
| ~ l0(c)
| ~ k1(e) ),
inference(res,[status(thm),theory(equality)],[2017,686]),
[iquote('0:Res:2017.3,686.0')] ).
cnf(2319,plain,
$false,
inference(ssi,[status(thm)],[2310,29,14,460,741,1492,25,459,738,1022,1413]),
[iquote('0:SSi:2310.2,2310.1,2310.0,29.0,14.0,460.0,741.0,1492.0,25.0,459.0,738.0,1022.0,1413.0,29.0,14.0,460.0,741.0,1492.0')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.13 % Problem : SYN138-1 : TPTP v8.1.0. Released v1.1.0.
% 0.13/0.13 % Command : run_spass %d %s
% 0.13/0.35 % Computer : n013.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 : Tue Jul 12 04:50:29 EDT 2022
% 0.21/0.35 % CPUTime :
% 0.42/0.60
% 0.42/0.60 SPASS V 3.9
% 0.42/0.60 SPASS beiseite: Proof found.
% 0.42/0.60 % SZS status Theorem
% 0.42/0.60 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.42/0.60 SPASS derived 1708 clauses, backtracked 0 clauses, performed 0 splits and kept 1130 clauses.
% 0.42/0.60 SPASS allocated 77134 KBytes.
% 0.42/0.60 SPASS spent 0:00:00.23 on the problem.
% 0.42/0.60 0:00:00.04 for the input.
% 0.42/0.60 0:00:00.00 for the FLOTTER CNF translation.
% 0.42/0.60 0:00:00.01 for inferences.
% 0.42/0.60 0:00:00.00 for the backtracking.
% 0.42/0.60 0:00:00.12 for the reduction.
% 0.42/0.60
% 0.42/0.60
% 0.42/0.60 Here is a proof with depth 6, length 145 :
% 0.42/0.60 % SZS output start Refutation
% See solution above
% 0.42/0.60 Formulae used in the proof : prove_this axiom_1 axiom_3 axiom_5 axiom_9 axiom_11 axiom_12 axiom_13 axiom_14 axiom_15 axiom_17 axiom_19 axiom_20 axiom_24 axiom_26 axiom_28 axiom_31 axiom_32 axiom_34 axiom_36 axiom_37 rule_001 rule_002 rule_016 rule_021 rule_024 rule_029 rule_036 rule_085 rule_107 rule_113 rule_121 rule_124 rule_125 rule_126 rule_127 rule_129 rule_131 rule_133 rule_136 rule_137 rule_155 rule_174 rule_176 rule_177 rule_181 rule_183 rule_186 rule_187 rule_188 rule_189 rule_231 rule_240 rule_244 rule_255 rule_257 rule_267 rule_274 rule_276 rule_299
% 0.42/0.60
%------------------------------------------------------------------------------