%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : KRS007-1 : TPTP v8.1.0. Released v2.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 : Sun Jul 17 03:30:15 EDT 2022
% Result : Satisfiable 0.21s 0.43s
% Output : Saturation 0.21s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named 18)
% Comments :
%------------------------------------------------------------------------------
cnf(98,plain,
( ~ r2least(u)
| ~ d(v)
| ~ s2least(u6r1(u))
| ~ r(u,v)
| e(u) ),
inference(sor,[status(thm)],[80,2]),
[iquote('0:SoR:80.2,2.1')] ).
cnf(105,plain,
( ~ e(u)
| ~ d(u4r2(u)) ),
inference(sor,[status(thm)],[93,7]),
[iquote('0:SoR:93.0,7.1')] ).
cnf(103,plain,
( ~ e(u)
| ~ c(u4r3(u)) ),
inference(sor,[status(thm)],[91,1]),
[iquote('0:SoR:91.1,1.1')] ).
cnf(106,plain,
( ~ e(u)
| s2least(u4r2(u)) ),
inference(sor,[status(thm)],[93,60]),
[iquote('0:SoR:93.0,60.1')] ).
cnf(93,plain,
( ~ s1most(u4r2(u))
| ~ e(u) ),
inference(ems,[status(thm)],[88,8,15]),
[iquote('0:EmS:88.0,88.1,8.1,15.1')] ).
cnf(87,plain,
( ~ r2least(u)
| ~ d(v)
| ~ s2least(u6r2(u))
| ~ r(u,v)
| e(u) ),
inference(sor,[status(thm)],[79,2]),
[iquote('0:SoR:79.2,2.1')] ).
cnf(91,plain,
( ~ e(u)
| ~ s2least(u4r3(u)) ),
inference(ems,[status(thm)],[88,13,2]),
[iquote('0:EmS:88.0,88.1,13.1,2.1')] ).
cnf(96,plain,
~ d(u4r2(exist)),
inference(sor,[status(thm)],[94,7]),
[iquote('0:SoR:94.0,7.1')] ).
cnf(95,plain,
~ c(u4r3(exist)),
inference(sor,[status(thm)],[92,1]),
[iquote('0:SoR:92.0,1.1')] ).
cnf(97,plain,
s2least(u4r2(exist)),
inference(sor,[status(thm)],[94,60]),
[iquote('0:SoR:94.0,60.1')] ).
cnf(80,plain,
( ~ r2least(u)
| ~ d(v)
| ~ c(u6r1(u))
| ~ r(u,v)
| e(u) ),
inference(res,[status(thm),theory(equality)],[22,27]),
[iquote('0:Res:22.1,27.2')] ).
cnf(94,plain,
~ s1most(u4r2(exist)),
inference(ems,[status(thm)],[88,8,32]),
[iquote('0:EmS:88.0,88.1,8.1,32.0')] ).
cnf(92,plain,
~ s2least(u4r3(exist)),
inference(ems,[status(thm)],[88,31,2]),
[iquote('0:EmS:88.0,88.1,31.0,2.1')] ).
cnf(88,plain,
( ~ d(u)
| ~ c(u) ),
inference(ems,[status(thm)],[86,7,1]),
[iquote('0:EmS:86.0,86.1,7.1,1.1')] ).
cnf(86,plain,
( ~ s1most(u)
| ~ s2least(u) ),
inference(mrr,[status(thm)],[85,5]),
[iquote('0:MRR:85.2,5.1')] ).
cnf(79,plain,
( ~ r2least(u)
| ~ d(v)
| ~ c(u6r2(u))
| ~ r(u,v)
| e(u) ),
inference(res,[status(thm),theory(equality)],[23,27]),
[iquote('0:Res:23.1,27.2')] ).
cnf(68,plain,
( ~ e(u)
| ~ r(u,v)
| r2least(u)
| equalish(v,u4r3(u)) ),
inference(res,[status(thm),theory(equality)],[14,24]),
[iquote('0:Res:14.1,24.0')] ).
cnf(67,plain,
( ~ e(u)
| ~ r(u,v)
| r2least(u)
| equalish(v,u4r2(u)) ),
inference(res,[status(thm),theory(equality)],[16,24]),
[iquote('0:Res:16.1,24.0')] ).
cnf(27,plain,
( ~ d(u)
| ~ c(v)
| ~ r(w,v)
| ~ r(w,u)
| e(w) ),
inference(con,[status(thm)],[18]),
[iquote('0:Con:18.2')] ).
cnf(66,plain,
( ~ e(u)
| ~ r(u,v)
| r2least(u)
| equalish(v,u4r1(u)) ),
inference(res,[status(thm),theory(equality)],[17,24]),
[iquote('0:Res:17.1,24.0')] ).
cnf(71,plain,
( ~ r(exist,u)
| equalish(u,u4r3(exist)) ),
inference(mrr,[status(thm)],[63,33]),
[iquote('0:MRR:63.1,33.0')] ).
cnf(70,plain,
( ~ r(exist,u)
| equalish(u,u4r2(exist)) ),
inference(mrr,[status(thm)],[62,33]),
[iquote('0:MRR:62.1,33.0')] ).
cnf(69,plain,
( ~ r(exist,u)
| equalish(u,u4r1(exist)) ),
inference(mrr,[status(thm)],[61,33]),
[iquote('0:MRR:61.1,33.0')] ).
cnf(9,axiom,
( ~ s1most(u)
| ~ s(u,v)
| ~ s(u,w)
| equalish(w,v) ),
file('KRS007-1.p',unknown),
[] ).
cnf(24,axiom,
( ~ r(u,v)
| ~ r(u,w)
| r2least(u)
| equalish(w,v) ),
file('KRS007-1.p',unknown),
[] ).
cnf(60,plain,
( s2least(u)
| s1most(u) ),
inference(mrr,[status(thm)],[59,12]),
[iquote('0:MRR:59.0,12.1')] ).
cnf(6,axiom,
( ~ s(u,v)
| ~ s(u,w)
| s2least(u)
| equalish(w,v) ),
file('KRS007-1.p',unknown),
[] ).
cnf(21,axiom,
( ~ r2least(u)
| ~ equalish(u6r2(u),u6r1(u)) ),
file('KRS007-1.p',unknown),
[] ).
cnf(3,axiom,
( ~ s2least(u)
| ~ equalish(u1r2(u),u1r1(u)) ),
file('KRS007-1.p',unknown),
[] ).
cnf(10,axiom,
( ~ equalish(u3r2(u),u3r1(u))
| s1most(u) ),
file('KRS007-1.p',unknown),
[] ).
cnf(14,axiom,
( ~ e(u)
| r(u,u4r3(u)) ),
file('KRS007-1.p',unknown),
[] ).
cnf(16,axiom,
( ~ e(u)
| r(u,u4r2(u)) ),
file('KRS007-1.p',unknown),
[] ).
cnf(17,axiom,
( ~ e(u)
| r(u,u4r1(u)) ),
file('KRS007-1.p',unknown),
[] ).
cnf(22,axiom,
( ~ r2least(u)
| r(u,u6r1(u)) ),
file('KRS007-1.p',unknown),
[] ).
cnf(23,axiom,
( ~ r2least(u)
| r(u,u6r2(u)) ),
file('KRS007-1.p',unknown),
[] ).
cnf(4,axiom,
( ~ s2least(u)
| s(u,u1r1(u)) ),
file('KRS007-1.p',unknown),
[] ).
cnf(5,axiom,
( ~ s2least(u)
| s(u,u1r2(u)) ),
file('KRS007-1.p',unknown),
[] ).
cnf(11,axiom,
( s1most(u)
| s(u,u3r1(u)) ),
file('KRS007-1.p',unknown),
[] ).
cnf(12,axiom,
( s1most(u)
| s(u,u3r2(u)) ),
file('KRS007-1.p',unknown),
[] ).
cnf(13,axiom,
( ~ e(u)
| d(u4r3(u)) ),
file('KRS007-1.p',unknown),
[] ).
cnf(52,plain,
~ f(exist),
inference(sor,[status(thm)],[33,19]),
[iquote('0:SoR:33.0,19.1')] ).
cnf(15,axiom,
( ~ e(u)
| c(u4r2(u)) ),
file('KRS007-1.p',unknown),
[] ).
cnf(19,axiom,
( ~ f(u)
| r2least(u) ),
file('KRS007-1.p',unknown),
[] ).
cnf(1,axiom,
( ~ c(u)
| s2least(u) ),
file('KRS007-1.p',unknown),
[] ).
cnf(7,axiom,
( ~ d(u)
| s1most(u) ),
file('KRS007-1.p',unknown),
[] ).
cnf(2,axiom,
( ~ s2least(u)
| c(u) ),
file('KRS007-1.p',unknown),
[] ).
cnf(8,axiom,
( ~ s1most(u)
| d(u) ),
file('KRS007-1.p',unknown),
[] ).
cnf(28,plain,
r(exist,u4r3(exist)),
inference(res,[status(thm),theory(equality)],[25,14]),
[iquote('0:Res:25.0,14.0')] ).
cnf(29,plain,
r(exist,u4r2(exist)),
inference(res,[status(thm),theory(equality)],[25,16]),
[iquote('0:Res:25.0,16.0')] ).
cnf(30,plain,
r(exist,u4r1(exist)),
inference(res,[status(thm),theory(equality)],[25,17]),
[iquote('0:Res:25.0,17.0')] ).
cnf(31,plain,
d(u4r3(exist)),
inference(res,[status(thm),theory(equality)],[25,13]),
[iquote('0:Res:25.0,13.0')] ).
cnf(20,axiom,
( ~ r2least(u)
| f(u) ),
file('KRS007-1.p',unknown),
[] ).
cnf(32,plain,
c(u4r2(exist)),
inference(res,[status(thm),theory(equality)],[25,15]),
[iquote('0:Res:25.0,15.0')] ).
cnf(33,plain,
~ r2least(exist),
inference(res,[status(thm),theory(equality)],[20,26]),
[iquote('0:Res:20.1,26.0')] ).
cnf(26,axiom,
~ f(exist),
file('KRS007-1.p',unknown),
[] ).
cnf(25,axiom,
e(exist),
file('KRS007-1.p',unknown),
[] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : KRS007-1 : TPTP v8.1.0. Released v2.0.0.
% 0.07/0.13 % Command : run_spass %d %s
% 0.13/0.34 % Computer : n020.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % 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 Jun 7 08:11:36 EDT 2022
% 0.13/0.35 % CPUTime :
% 0.21/0.43
% 0.21/0.43 SPASS V 3.9
% 0.21/0.43 SPASS beiseite: Completion found.
% 0.21/0.43 % SZS status CounterSatisfiable
% 0.21/0.43 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.21/0.43 SPASS derived 60 clauses, backtracked 0 clauses, performed 0 splits and kept 60 clauses.
% 0.21/0.43 SPASS allocated 75671 KBytes.
% 0.21/0.43 SPASS spent 0:00:00.07 on the problem.
% 0.21/0.43 0:00:00.04 for the input.
% 0.21/0.43 0:00:00.00 for the FLOTTER CNF translation.
% 0.21/0.43 0:00:00.00 for inferences.
% 0.21/0.43 0:00:00.00 for the backtracking.
% 0.21/0.43 0:00:00.00 for the reduction.
% 0.21/0.43
% 0.21/0.43
% 0.21/0.43 The saturated set of worked-off clauses is :
% 0.21/0.43 % SZS output start Saturation
% See solution above
%------------------------------------------------------------------------------