%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : SYN740-1 : TPTP v8.1.0. Released v2.5.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n009.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:24:05 EDT 2022
% Result : Satisfiable 0.91s 1.15s
% Output : Saturation 0.91s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named 2889)
% Comments :
%------------------------------------------------------------------------------
cnf(2895,plain,
( ~ ssPv2(skf1(u))
| ~ ssPv2(u)
| ~ ssPv3(v)
| ~ ssPv3(u)
| ~ ssRr(u,v) ),
inference(res,[status(thm),theory(equality)],[1,2890]),
[iquote('0:Res:1.0,2890.4')] ).
cnf(2890,plain,
( ~ ssPv2(u)
| ~ ssPv2(v)
| ~ ssPv3(w)
| ~ ssPv3(v)
| ~ ssRr(v,u)
| ~ ssRr(v,w) ),
inference(con,[status(thm)],[2889]),
[iquote('0:Con:2889.2')] ).
cnf(2891,plain,
( ~ ssPv2(skf1(u))
| ~ ssPv2(u)
| ~ ssPv4(v)
| ~ ssPv3(u)
| ~ ssRr(u,v) ),
inference(res,[status(thm),theory(equality)],[1,2887]),
[iquote('0:Res:1.0,2887.4')] ).
cnf(2887,plain,
( ~ ssPv2(u)
| ~ ssPv2(v)
| ~ ssPv4(w)
| ~ ssPv3(v)
| ~ ssRr(v,u)
| ~ ssRr(v,w) ),
inference(obv,[status(thm),theory(equality)],[2881]),
[iquote('0:Obv:2881.1')] ).
cnf(2750,plain,
( ~ ssPv3(skf1(u))
| ~ ssPv2(v)
| ~ ssPv3(u)
| ~ ssPv2(u)
| ~ ssRr(u,v) ),
inference(con,[status(thm)],[2749]),
[iquote('0:Con:2749.5')] ).
cnf(973,plain,
( ~ ssPv1(u)
| ~ ssPv4(v)
| ~ ssPv1(v)
| ~ ssPv4(w)
| ~ ssRr(v,u)
| ~ ssRr(v,w)
| ssPv3(v)
| ssPv1(skf1(v)) ),
inference(sor,[status(thm)],[963,547]),
[iquote('0:SoR:963.1,547.4')] ).
cnf(977,plain,
( ~ ssPv1(u)
| ~ ssPv4(v)
| ~ ssPv1(v)
| ~ ssRr(v,u)
| ~ ssRr(v,w)
| ssPv3(v)
| ssPv1(skf1(v))
| ssPv1(w) ),
inference(sor,[status(thm)],[963,139]),
[iquote('0:SoR:963.1,139.4')] ).
cnf(2431,plain,
( ~ ssPv2(skf1(u))
| ~ ssPv3(v)
| ~ ssPv2(u)
| ~ ssPv4(u)
| ~ ssRr(u,v)
| ssPv4(skf1(u)) ),
inference(res,[status(thm),theory(equality)],[1,2203]),
[iquote('0:Res:1.0,2203.4')] ).
cnf(2203,plain,
( ~ ssPv2(u)
| ~ ssPv3(v)
| ~ ssPv2(w)
| ~ ssPv4(w)
| ~ ssRr(w,u)
| ~ ssRr(w,v)
| ssPv4(skf1(w)) ),
inference(res,[status(thm),theory(equality)],[1,996]),
[iquote('0:Res:1.0,996.4')] ).
cnf(996,plain,
( ~ ssPv2(u)
| ~ ssPv3(v)
| ~ ssPv2(w)
| ~ ssPv4(w)
| ~ ssRr(w,x)
| ~ ssRr(w,u)
| ~ ssRr(w,v)
| ssPv4(x) ),
inference(obv,[status(thm),theory(equality)],[985]),
[iquote('0:Obv:985.0')] ).
cnf(1896,plain,
( ~ ssPv3(u)
| ~ ssPv3(v)
| ~ ssPv2(w)
| ~ ssRr(u,v)
| ~ ssRr(u,w)
| ssPv3(skf1(u)) ),
inference(mrr,[status(thm)],[1895,113]),
[iquote('0:MRR:1895.1,113.2')] ).
cnf(1687,plain,
( ~ ssPv2(skf1(u))
| ~ ssPv4(u)
| ~ ssPv3(u)
| ~ ssPv2(u) ),
inference(res,[status(thm),theory(equality)],[1,1576]),
[iquote('0:Res:1.0,1576.4')] ).
cnf(1576,plain,
( ~ ssPv2(u)
| ~ ssPv4(v)
| ~ ssPv3(v)
| ~ ssPv2(v)
| ~ ssRr(v,u) ),
inference(con,[status(thm)],[1575]),
[iquote('0:Con:1575.1')] ).
cnf(1334,plain,
( ~ ssPv1(u)
| ~ ssPv1(skf1(u))
| ~ ssPv2(v)
| ~ ssRr(u,w)
| ~ ssRr(u,v)
| ssPv1(w) ),
inference(res,[status(thm),theory(equality)],[1,30]),
[iquote('0:Res:1.0,30.3')] ).
cnf(30,axiom,
( ~ ssPv1(u)
| ~ ssPv1(v)
| ~ ssPv2(w)
| ~ ssRr(u,v)
| ~ ssRr(u,x)
| ~ ssRr(u,w)
| ssPv1(x) ),
file('SYN740-1.p',unknown),
[] ).
cnf(1004,plain,
( ~ ssPv2(u)
| ~ ssPv2(skf1(u))
| ~ ssPv3(v)
| ~ ssRr(u,w)
| ~ ssRr(u,v)
| ssPv3(w) ),
inference(res,[status(thm),theory(equality)],[1,28]),
[iquote('0:Res:1.0,28.3')] ).
cnf(28,axiom,
( ~ ssPv2(u)
| ~ ssPv2(v)
| ~ ssPv3(w)
| ~ ssRr(u,v)
| ~ ssRr(u,x)
| ~ ssRr(u,w)
| ssPv3(x) ),
file('SYN740-1.p',unknown),
[] ).
cnf(998,plain,
( ~ ssPv2(skf1(u))
| ~ ssPv1(u)
| ~ ssPv4(u)
| ~ ssPv2(u) ),
inference(res,[status(thm),theory(equality)],[1,997]),
[iquote('0:Res:1.0,997.4')] ).
cnf(997,plain,
( ~ ssPv2(u)
| ~ ssPv1(v)
| ~ ssPv4(v)
| ~ ssPv2(v)
| ~ ssRr(v,u) ),
inference(res,[status(thm),theory(equality)],[1,991]),
[iquote('0:Res:1.0,991.4')] ).
cnf(980,plain,
( ~ ssPv2(u)
| ~ ssPv1(skf1(u))
| ~ ssPv2(v)
| ~ ssRr(u,w)
| ~ ssRr(u,v)
| ssPv4(w) ),
inference(res,[status(thm),theory(equality)],[1,31]),
[iquote('0:Res:1.0,31.3')] ).
cnf(31,axiom,
( ~ ssPv2(u)
| ~ ssPv1(v)
| ~ ssPv2(w)
| ~ ssRr(u,v)
| ~ ssRr(u,x)
| ~ ssRr(u,w)
| ssPv4(x) ),
file('SYN740-1.p',unknown),
[] ).
cnf(520,plain,
( ~ ssPv3(u)
| ~ ssPv4(v)
| ~ ssPv2(u)
| ~ ssRr(u,w)
| ~ ssRr(u,v)
| ssPv4(u)
| ssPv1(w) ),
inference(obv,[status(thm),theory(equality)],[515]),
[iquote('0:Obv:515.0')] ).
cnf(963,plain,
( ~ ssPv1(u)
| ~ ssPv3(skf1(v))
| ~ ssRr(v,u)
| ssPv3(v)
| ssPv1(skf1(v)) ),
inference(res,[status(thm),theory(equality)],[1,914]),
[iquote('0:Res:1.0,914.2')] ).
cnf(914,plain,
( ~ ssPv1(u)
| ~ ssPv3(v)
| ~ ssRr(w,v)
| ~ ssRr(w,u)
| ssPv3(w)
| ssPv1(skf1(w)) ),
inference(res,[status(thm),theory(equality)],[1,26]),
[iquote('0:Res:1.0,26.2')] ).
cnf(913,plain,
( ~ ssPv2(u)
| ~ ssPv4(skf1(v))
| ~ ssRr(v,u)
| ssPv4(v)
| ssPv3(skf1(v)) ),
inference(res,[status(thm),theory(equality)],[1,759]),
[iquote('0:Res:1.0,759.2')] ).
cnf(26,axiom,
( ~ ssPv1(u)
| ~ ssPv3(v)
| ~ ssRr(w,x)
| ~ ssRr(w,v)
| ~ ssRr(w,u)
| ssPv3(w)
| ssPv1(x) ),
file('SYN740-1.p',unknown),
[] ).
cnf(759,plain,
( ~ ssPv2(u)
| ~ ssPv4(v)
| ~ ssRr(w,v)
| ~ ssRr(w,u)
| ssPv4(w)
| ssPv3(skf1(w)) ),
inference(res,[status(thm),theory(equality)],[1,25]),
[iquote('0:Res:1.0,25.2')] ).
cnf(550,plain,
( ~ ssPv1(u)
| ~ ssPv2(v)
| ~ ssRr(w,v)
| ~ ssRr(w,u)
| ssPv1(w)
| ssPv2(skf1(w)) ),
inference(res,[status(thm),theory(equality)],[1,27]),
[iquote('0:Res:1.0,27.2')] ).
cnf(760,plain,
( ~ ssPv2(u)
| ~ ssPv1(u)
| ~ ssPv4(u)
| ~ ssRr(u,v)
| ssPv3(v) ),
inference(res,[status(thm),theory(equality)],[1,549]),
[iquote('0:Res:1.0,549.3')] ).
cnf(25,axiom,
( ~ ssPv2(u)
| ~ ssPv4(v)
| ~ ssRr(w,x)
| ~ ssRr(w,v)
| ~ ssRr(w,u)
| ssPv4(w)
| ssPv3(x) ),
file('SYN740-1.p',unknown),
[] ).
cnf(547,plain,
( ~ ssPv4(u)
| ~ ssPv1(v)
| ~ ssPv4(v)
| ~ ssRr(v,u)
| ssPv3(skf1(v)) ),
inference(mrr,[status(thm)],[150,546]),
[iquote('0:MRR:150.4,546.0')] ).
cnf(587,plain,
( ~ ssPv4(skf1(u))
| ~ ssPv1(u)
| ~ ssPv4(u)
| ssPv3(skf1(u)) ),
inference(mrr,[status(thm)],[152,586]),
[iquote('0:MRR:152.3,586.0')] ).
cnf(586,plain,
( ~ ssPv2(u)
| ~ ssPv1(u)
| ~ ssPv4(u)
| ssPv3(skf1(u)) ),
inference(res,[status(thm),theory(equality)],[1,546]),
[iquote('0:Res:1.0,546.3')] ).
cnf(27,axiom,
( ~ ssPv1(u)
| ~ ssPv2(v)
| ~ ssRr(w,x)
| ~ ssRr(w,v)
| ~ ssRr(w,u)
| ssPv1(w)
| ssPv2(x) ),
file('SYN740-1.p',unknown),
[] ).
cnf(535,plain,
( ~ ssPv2(u)
| ~ ssPv1(u)
| ~ ssPv1(v)
| ~ ssPv2(skf1(u))
| ~ ssRr(u,v) ),
inference(res,[status(thm),theory(equality)],[1,24]),
[iquote('0:Res:1.0,24.4')] ).
cnf(484,plain,
( ~ ssPv2(u)
| ~ ssPv1(u)
| ~ ssPv2(v)
| ~ ssPv4(skf1(u))
| ~ ssRr(u,v) ),
inference(res,[status(thm),theory(equality)],[1,23]),
[iquote('0:Res:1.0,23.4')] ).
cnf(536,plain,
( ~ ssPv1(u)
| ~ ssPv2(u)
| ~ ssPv4(skf1(u))
| ~ ssPv3(u) ),
inference(res,[status(thm),theory(equality)],[1,492]),
[iquote('0:Res:1.0,492.4')] ).
cnf(492,plain,
( ~ ssPv1(u)
| ~ ssPv2(u)
| ~ ssPv4(v)
| ~ ssPv3(u)
| ~ ssRr(u,v) ),
inference(obv,[status(thm),theory(equality)],[489]),
[iquote('0:Obv:489.2')] ).
cnf(24,axiom,
( ~ ssPv2(u)
| ~ ssPv1(u)
| ~ ssPv1(v)
| ~ ssPv2(w)
| ~ ssRr(u,w)
| ~ ssRr(u,v) ),
file('SYN740-1.p',unknown),
[] ).
cnf(518,plain,
( ~ ssPv2(u)
| ~ ssPv4(skf1(u))
| ~ ssPv3(u)
| ssPv1(skf1(u)) ),
inference(res,[status(thm),theory(equality)],[1,483]),
[iquote('0:Res:1.0,483.3')] ).
cnf(483,plain,
( ~ ssPv2(u)
| ~ ssPv4(v)
| ~ ssPv3(u)
| ~ ssRr(u,v)
| ssPv1(skf1(u)) ),
inference(obv,[status(thm),theory(equality)],[480]),
[iquote('0:Obv:480.0')] ).
cnf(485,plain,
( ~ ssPv1(u)
| ~ ssPv3(skf1(u))
| ~ ssPv2(u)
| ~ ssPv3(u) ),
inference(res,[status(thm),theory(equality)],[1,467]),
[iquote('0:Res:1.0,467.4')] ).
cnf(467,plain,
( ~ ssPv1(u)
| ~ ssPv3(v)
| ~ ssPv2(u)
| ~ ssPv3(u)
| ~ ssRr(u,v) ),
inference(obv,[status(thm),theory(equality)],[465]),
[iquote('0:Obv:465.1')] ).
cnf(23,axiom,
( ~ ssPv2(u)
| ~ ssPv1(u)
| ~ ssPv2(v)
| ~ ssPv4(w)
| ~ ssRr(u,w)
| ~ ssRr(u,v) ),
file('SYN740-1.p',unknown),
[] ).
cnf(466,plain,
( ~ ssPv3(u)
| ~ ssPv2(u)
| ~ ssPv3(skf1(u))
| ssPv1(skf1(u)) ),
inference(res,[status(thm),theory(equality)],[1,370]),
[iquote('0:Res:1.0,370.3')] ).
cnf(370,plain,
( ~ ssPv3(u)
| ~ ssPv2(u)
| ~ ssPv3(v)
| ~ ssRr(u,v)
| ssPv1(skf1(u)) ),
inference(res,[status(thm),theory(equality)],[1,19]),
[iquote('0:Res:1.0,19.3')] ).
cnf(395,plain,
( ~ ssPv2(u)
| ~ ssPv4(u)
| ~ ssPv1(u)
| ssPv1(skf1(u)) ),
inference(res,[status(thm),theory(equality)],[1,184]),
[iquote('0:Res:1.0,184.3')] ).
cnf(19,axiom,
( ~ ssPv3(u)
| ~ ssPv2(u)
| ~ ssPv3(v)
| ~ ssRr(u,w)
| ~ ssRr(u,v)
| ssPv1(w) ),
file('SYN740-1.p',unknown),
[] ).
cnf(189,plain,
( ~ ssPv1(u)
| ~ ssPv4(u)
| ~ ssPv3(u)
| ~ ssPv2(u) ),
inference(obv,[status(thm),theory(equality)],[188]),
[iquote('0:Obv:188.1')] ).
cnf(182,plain,
( ~ ssPv2(u)
| ~ ssPv3(u)
| ~ ssPv4(u)
| ssPv1(skf1(u)) ),
inference(obv,[status(thm),theory(equality)],[179]),
[iquote('0:Obv:179.0')] ).
cnf(174,plain,
( ~ ssPv4(u)
| ~ ssPv2(u)
| ~ ssPv3(skf1(u))
| ssPv1(skf1(u)) ),
inference(res,[status(thm),theory(equality)],[1,169]),
[iquote('0:Res:1.0,169.3')] ).
cnf(169,plain,
( ~ ssPv4(u)
| ~ ssPv2(u)
| ~ ssPv3(v)
| ~ ssRr(u,v)
| ssPv1(skf1(u)) ),
inference(res,[status(thm),theory(equality)],[1,17]),
[iquote('0:Res:1.0,17.3')] ).
cnf(17,axiom,
( ~ ssPv4(u)
| ~ ssPv2(u)
| ~ ssPv3(v)
| ~ ssRr(u,w)
| ~ ssRr(u,v)
| ssPv1(w) ),
file('SYN740-1.p',unknown),
[] ).
cnf(161,plain,
( ~ ssPv1(u)
| ~ ssPv4(u)
| ~ ssRr(u,v)
| ssPv1(skf1(u))
| ssPv3(v) ),
inference(res,[status(thm),theory(equality)],[1,141]),
[iquote('0:Res:1.0,141.2')] ).
cnf(141,plain,
( ~ ssPv1(u)
| ~ ssPv4(u)
| ~ ssRr(u,v)
| ~ ssRr(u,w)
| ssPv1(v)
| ssPv3(w) ),
inference(mrr,[status(thm)],[140,110]),
[iquote('0:MRR:140.4,110.1')] ).
cnf(153,plain,
( ~ ssPv1(u)
| ~ ssPv1(skf1(u))
| ~ ssPv4(v)
| ~ ssRr(u,v)
| ssPv2(u) ),
inference(res,[status(thm),theory(equality)],[1,22]),
[iquote('0:Res:1.0,22.3')] ).
cnf(22,axiom,
( ~ ssPv1(u)
| ~ ssPv1(v)
| ~ ssPv4(w)
| ~ ssRr(u,v)
| ~ ssRr(u,w)
| ssPv2(u) ),
file('SYN740-1.p',unknown),
[] ).
cnf(142,plain,
( ~ ssPv4(u)
| ~ ssPv2(skf1(u))
| ~ ssPv4(v)
| ~ ssRr(u,v)
| ssPv2(u) ),
inference(res,[status(thm),theory(equality)],[1,21]),
[iquote('0:Res:1.0,21.3')] ).
cnf(143,plain,
( ~ ssPv1(u)
| ~ ssPv4(u)
| ssPv1(skf1(u))
| ssPv3(skf1(u)) ),
inference(res,[status(thm),theory(equality)],[1,139]),
[iquote('0:Res:1.0,139.2')] ).
cnf(139,plain,
( ~ ssPv1(u)
| ~ ssPv4(u)
| ~ ssRr(u,v)
| ssPv1(v)
| ssPv3(skf1(u)) ),
inference(mrr,[status(thm)],[138,114]),
[iquote('0:MRR:138.3,114.1')] ).
cnf(21,axiom,
( ~ ssPv4(u)
| ~ ssPv2(v)
| ~ ssPv4(w)
| ~ ssRr(u,v)
| ~ ssRr(u,w)
| ssPv2(u) ),
file('SYN740-1.p',unknown),
[] ).
cnf(135,plain,
( ~ ssPv1(u)
| ~ ssPv2(skf1(u))
| ~ ssRr(u,v)
| ssPv3(u)
| ssPv1(v) ),
inference(res,[status(thm),theory(equality)],[1,12]),
[iquote('0:Res:1.0,12.2')] ).
cnf(12,axiom,
( ~ ssPv1(u)
| ~ ssPv2(v)
| ~ ssRr(u,v)
| ~ ssRr(u,w)
| ssPv3(u)
| ssPv1(w) ),
file('SYN740-1.p',unknown),
[] ).
cnf(133,plain,
( ~ ssPv3(u)
| ~ ssPv1(skf1(u))
| ~ ssRr(u,v)
| ssPv4(u)
| ssPv1(v) ),
inference(res,[status(thm),theory(equality)],[1,8]),
[iquote('0:Res:1.0,8.2')] ).
cnf(132,plain,
( ~ ssPv4(u)
| ~ ssPv1(u)
| ssPv2(skf1(u))
| ssPv3(skf1(u)) ),
inference(res,[status(thm),theory(equality)],[1,131]),
[iquote('0:Res:1.0,131.2')] ).
cnf(8,axiom,
( ~ ssPv3(u)
| ~ ssPv1(v)
| ~ ssRr(u,v)
| ~ ssRr(u,w)
| ssPv4(u)
| ssPv1(w) ),
file('SYN740-1.p',unknown),
[] ).
cnf(131,plain,
( ~ ssPv4(u)
| ~ ssPv1(u)
| ~ ssRr(u,v)
| ssPv2(skf1(u))
| ssPv3(v) ),
inference(res,[status(thm),theory(equality)],[1,6]),
[iquote('0:Res:1.0,6.2')] ).
cnf(6,axiom,
( ~ ssPv4(u)
| ~ ssPv1(u)
| ~ ssRr(u,v)
| ~ ssRr(u,w)
| ssPv2(v)
| ssPv3(w) ),
file('SYN740-1.p',unknown),
[] ).
cnf(120,plain,
( ~ ssPv1(u)
| ~ ssPv4(v)
| ~ ssRr(u,v)
| ssPv4(skf1(u)) ),
inference(res,[status(thm),theory(equality)],[1,112]),
[iquote('0:Res:1.0,112.2')] ).
cnf(119,plain,
( ~ ssPv1(u)
| ~ ssPv4(skf1(u))
| ~ ssRr(u,v)
| ssPv3(v) ),
inference(res,[status(thm),theory(equality)],[1,109]),
[iquote('0:Res:1.0,109.2')] ).
cnf(112,plain,
( ~ ssPv1(u)
| ~ ssPv4(v)
| ~ ssRr(u,w)
| ~ ssRr(u,v)
| ssPv4(w) ),
inference(con,[status(thm)],[111]),
[iquote('0:Con:111.2')] ).
cnf(109,plain,
( ~ ssPv1(u)
| ~ ssPv4(v)
| ~ ssRr(u,v)
| ~ ssRr(u,w)
| ssPv3(w) ),
inference(mrr,[status(thm)],[11,107]),
[iquote('0:MRR:11.4,107.0')] ).
cnf(116,plain,
( ~ ssPv3(u)
| ~ ssPv4(skf1(u))
| ssPv3(skf1(u)) ),
inference(res,[status(thm),theory(equality)],[1,115]),
[iquote('0:Res:1.0,115.2')] ).
cnf(115,plain,
( ~ ssPv3(u)
| ~ ssPv4(v)
| ~ ssRr(u,v)
| ssPv3(skf1(u)) ),
inference(res,[status(thm),theory(equality)],[1,107]),
[iquote('0:Res:1.0,107.2')] ).
cnf(114,plain,
( ~ ssPv4(u)
| ~ ssPv3(u)
| ssPv3(skf1(u)) ),
inference(res,[status(thm),theory(equality)],[1,110]),
[iquote('0:Res:1.0,110.2')] ).
cnf(107,plain,
( ~ ssPv3(u)
| ~ ssPv4(v)
| ~ ssRr(u,w)
| ~ ssRr(u,v)
| ssPv3(w) ),
inference(mrr,[status(thm)],[18,106]),
[iquote('0:MRR:18.1,106.3')] ).
cnf(110,plain,
( ~ ssPv4(u)
| ~ ssPv3(u)
| ~ ssRr(u,v)
| ssPv3(v) ),
inference(con,[status(thm)],[108]),
[iquote('0:Con:108.3')] ).
cnf(113,plain,
( ~ ssPv3(u)
| ssPv3(skf1(u))
| ssPv2(u) ),
inference(res,[status(thm),theory(equality)],[1,106]),
[iquote('0:Res:1.0,106.1')] ).
cnf(106,plain,
( ~ ssPv3(u)
| ~ ssRr(u,v)
| ssPv3(v)
| ssPv2(u) ),
inference(mrr,[status(thm)],[105,2]),
[iquote('0:MRR:105.0,2.3')] ).
cnf(100,plain,
( ~ ssPv1(u)
| ~ ssPv1(skf1(u))
| ~ ssRr(u,v)
| ssPv4(u)
| ssPv3(v) ),
inference(res,[status(thm),theory(equality)],[1,9]),
[iquote('0:Res:1.0,9.2')] ).
cnf(9,axiom,
( ~ ssPv1(u)
| ~ ssPv1(v)
| ~ ssRr(u,v)
| ~ ssRr(u,w)
| ssPv4(u)
| ssPv3(w) ),
file('SYN740-1.p',unknown),
[] ).
cnf(97,plain,
( ~ ssPv2(u)
| ~ ssPv4(skf1(v))
| ~ ssRr(v,u)
| ssPv4(v)
| ssPv3(v) ),
inference(res,[status(thm),theory(equality)],[1,13]),
[iquote('0:Res:1.0,13.2')] ).
cnf(13,axiom,
( ~ ssPv2(u)
| ~ ssPv4(v)
| ~ ssRr(w,v)
| ~ ssRr(w,u)
| ssPv4(w)
| ssPv3(w) ),
file('SYN740-1.p',unknown),
[] ).
cnf(92,plain,
( ~ ssPv3(u)
| ~ ssPv4(skf1(u))
| ~ ssRr(u,v)
| ssPv1(u)
| ssPv2(v) ),
inference(res,[status(thm),theory(equality)],[1,16]),
[iquote('0:Res:1.0,16.2')] ).
cnf(16,axiom,
( ~ ssPv3(u)
| ~ ssPv4(v)
| ~ ssRr(u,v)
| ~ ssRr(u,w)
| ssPv1(u)
| ssPv2(w) ),
file('SYN740-1.p',unknown),
[] ).
cnf(89,plain,
( ~ ssPv3(u)
| ~ ssPv4(skf1(v))
| ~ ssRr(v,u)
| ssPv3(v)
| ssPv2(v) ),
inference(res,[status(thm),theory(equality)],[1,15]),
[iquote('0:Res:1.0,15.2')] ).
cnf(15,axiom,
( ~ ssPv3(u)
| ~ ssPv4(v)
| ~ ssRr(w,v)
| ~ ssRr(w,u)
| ssPv3(w)
| ssPv2(w) ),
file('SYN740-1.p',unknown),
[] ).
cnf(83,plain,
( ~ ssPv3(u)
| ~ ssPv4(skf1(u))
| ~ ssRr(u,v)
| ssPv4(u)
| ssPv4(v) ),
inference(res,[status(thm),theory(equality)],[1,7]),
[iquote('0:Res:1.0,7.2')] ).
cnf(7,axiom,
( ~ ssPv3(u)
| ~ ssPv4(v)
| ~ ssRr(u,v)
| ~ ssRr(u,w)
| ssPv4(u)
| ssPv4(w) ),
file('SYN740-1.p',unknown),
[] ).
cnf(79,plain,
( ~ ssPv2(u)
| ~ ssPv1(v)
| ~ ssRr(u,v)
| ssPv1(skf1(u)) ),
inference(res,[status(thm),theory(equality)],[1,32]),
[iquote('0:Res:1.0,32.2')] ).
cnf(32,plain,
( ~ ssPv2(u)
| ~ ssPv1(v)
| ~ ssRr(u,w)
| ~ ssRr(u,v)
| ssPv1(w) ),
inference(mrr,[status(thm)],[20,10]),
[iquote('0:MRR:20.2,10.5')] ).
cnf(78,plain,
( ~ ssPv3(u)
| ~ ssPv2(u)
| ~ ssPv1(u)
| ~ ssPv1(skf1(u)) ),
inference(res,[status(thm),theory(equality)],[1,4]),
[iquote('0:Res:1.0,4.4')] ).
cnf(77,plain,
( ~ ssPv3(u)
| ~ ssPv1(u)
| ssPv2(u)
| ssPv4(skf1(u)) ),
inference(res,[status(thm),theory(equality)],[1,3]),
[iquote('0:Res:1.0,3.2')] ).
cnf(4,axiom,
( ~ ssPv3(u)
| ~ ssPv2(u)
| ~ ssPv1(u)
| ~ ssPv1(v)
| ~ ssRr(u,v) ),
file('SYN740-1.p',unknown),
[] ).
cnf(3,axiom,
( ~ ssPv3(u)
| ~ ssPv1(u)
| ~ ssRr(u,v)
| ssPv2(u)
| ssPv4(v) ),
file('SYN740-1.p',unknown),
[] ).
cnf(1,axiom,
ssRr(u,skf1(u)),
file('SYN740-1.p',unknown),
[] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : SYN740-1 : TPTP v8.1.0. Released v2.5.0.
% 0.11/0.12 % Command : run_spass %d %s
% 0.12/0.33 % Computer : n009.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.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 600
% 0.12/0.33 % DateTime : Mon Jul 11 12:40:37 EDT 2022
% 0.12/0.33 % CPUTime :
% 0.91/1.15
% 0.91/1.15 SPASS V 3.9
% 0.91/1.15 SPASS beiseite: Completion found.
% 0.91/1.15 % SZS status CounterSatisfiable
% 0.91/1.15 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.91/1.15 SPASS derived 1814 clauses, backtracked 0 clauses, performed 0 splits and kept 129 clauses.
% 0.91/1.15 SPASS allocated 80651 KBytes.
% 0.91/1.15 SPASS spent 0:00:00.35 on the problem.
% 0.91/1.15 0:00:00.03 for the input.
% 0.91/1.15 0:00:00.00 for the FLOTTER CNF translation.
% 0.91/1.15 0:00:00.08 for inferences.
% 0.91/1.15 0:00:00.00 for the backtracking.
% 0.91/1.15 0:00:00.21 for the reduction.
% 0.91/1.15
% 0.91/1.15
% 0.91/1.15 The saturated set of worked-off clauses is :
% 0.91/1.15 % SZS output start Saturation
% See solution above
%------------------------------------------------------------------------------