%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : KRS011-1 : TPTP v8.1.0. Released v2.0.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n019.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:16 EDT 2022
% Result : Satisfiable 0.18s 0.41s
% Output : Saturation 0.18s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named 130)
% Comments :
%------------------------------------------------------------------------------
cnf(131,plain,
( ~ f1(u)
| equalish(u9r5(u),u9r5(u)) ),
inference(obv,[status(thm),theory(equality)],[130]),
[iquote('0:Obv:130.2')] ).
cnf(127,plain,
( ~ f1(u)
| ~ t(u9r4(u),v)
| ~ t(u9r4(u),w)
| equalish(v,u9r5(u))
| equalish(w,u9r5(u))
| equalish(w,v) ),
inference(obv,[status(thm),theory(equality)],[126]),
[iquote('0:Obv:126.0')] ).
cnf(125,plain,
( ~ f2(u)
| equalish(u10r5(u),u10r5(u)) ),
inference(obv,[status(thm),theory(equality)],[124]),
[iquote('0:Obv:124.2')] ).
cnf(15,axiom,
( ~ f1(u)
| ~ t(u9r4(u),v)
| ~ t(u9r4(u),w)
| ~ t(u9r4(u),x)
| equalish(w,v)
| equalish(x,v)
| equalish(x,w) ),
file('KRS011-1.p',unknown),
[] ).
cnf(119,plain,
( ~ f2(u)
| ~ t(u10r4(u),v)
| ~ t(u10r4(u),w)
| equalish(v,u10r5(u))
| equalish(w,u10r5(u))
| equalish(w,v) ),
inference(obv,[status(thm),theory(equality)],[118]),
[iquote('0:Obv:118.0')] ).
cnf(121,plain,
( ~ f3(u)
| equalish(u11r5(u),u11r5(u)) ),
inference(obv,[status(thm),theory(equality)],[120]),
[iquote('0:Obv:120.2')] ).
cnf(25,axiom,
( ~ f2(u)
| ~ t(u10r4(u),v)
| ~ t(u10r4(u),w)
| ~ t(u10r4(u),x)
| equalish(w,v)
| equalish(x,v)
| equalish(x,w) ),
file('KRS011-1.p',unknown),
[] ).
cnf(115,plain,
( ~ f3(u)
| ~ t(u11r4(u),v)
| ~ t(u11r4(u),w)
| equalish(v,u11r5(u))
| equalish(w,u11r5(u))
| equalish(w,v) ),
inference(obv,[status(thm),theory(equality)],[114]),
[iquote('0:Obv:114.0')] ).
cnf(35,axiom,
( ~ f3(u)
| ~ t(u11r4(u),v)
| ~ t(u11r4(u),w)
| ~ t(u11r4(u),x)
| equalish(w,v)
| equalish(x,v)
| equalish(x,w) ),
file('KRS011-1.p',unknown),
[] ).
cnf(17,axiom,
( ~ c(u)
| ~ r1(v,w)
| ~ t1(w,u)
| ~ equalish(u9r2(w,v),u9r1(w,v))
| f1(v) ),
file('KRS011-1.p',unknown),
[] ).
cnf(18,axiom,
( ~ c(u)
| ~ r1(v,w)
| ~ t1(w,u)
| ~ equalish(u9r3(w,v),u9r1(w,v))
| f1(v) ),
file('KRS011-1.p',unknown),
[] ).
cnf(19,axiom,
( ~ c(u)
| ~ r1(v,w)
| ~ t1(w,u)
| ~ equalish(u9r3(w,v),u9r2(w,v))
| f1(v) ),
file('KRS011-1.p',unknown),
[] ).
cnf(27,axiom,
( ~ d(u)
| ~ r2(v,w)
| ~ t2(w,u)
| ~ equalish(u10r2(w,v),u10r1(w,v))
| f2(v) ),
file('KRS011-1.p',unknown),
[] ).
cnf(28,axiom,
( ~ d(u)
| ~ r2(v,w)
| ~ t2(w,u)
| ~ equalish(u10r3(w,v),u10r1(w,v))
| f2(v) ),
file('KRS011-1.p',unknown),
[] ).
cnf(29,axiom,
( ~ d(u)
| ~ r2(v,w)
| ~ t2(w,u)
| ~ equalish(u10r3(w,v),u10r2(w,v))
| f2(v) ),
file('KRS011-1.p',unknown),
[] ).
cnf(37,axiom,
( ~ e(u)
| ~ r3(v,w)
| ~ t3(w,u)
| ~ equalish(u11r2(w,v),u11r1(w,v))
| f3(v) ),
file('KRS011-1.p',unknown),
[] ).
cnf(38,axiom,
( ~ e(u)
| ~ r3(v,w)
| ~ t3(w,u)
| ~ equalish(u11r3(w,v),u11r1(w,v))
| f3(v) ),
file('KRS011-1.p',unknown),
[] ).
cnf(39,axiom,
( ~ e(u)
| ~ r3(v,w)
| ~ t3(w,u)
| ~ equalish(u11r3(w,v),u11r2(w,v))
| f3(v) ),
file('KRS011-1.p',unknown),
[] ).
cnf(20,axiom,
( ~ c(u)
| ~ r1(v,w)
| ~ t1(w,u)
| f1(v)
| t(w,u9r1(w,v)) ),
file('KRS011-1.p',unknown),
[] ).
cnf(21,axiom,
( ~ c(u)
| ~ r1(v,w)
| ~ t1(w,u)
| f1(v)
| t(w,u9r2(w,v)) ),
file('KRS011-1.p',unknown),
[] ).
cnf(22,axiom,
( ~ c(u)
| ~ r1(v,w)
| ~ t1(w,u)
| f1(v)
| t(w,u9r3(w,v)) ),
file('KRS011-1.p',unknown),
[] ).
cnf(30,axiom,
( ~ d(u)
| ~ r2(v,w)
| ~ t2(w,u)
| f2(v)
| t(w,u10r1(w,v)) ),
file('KRS011-1.p',unknown),
[] ).
cnf(31,axiom,
( ~ d(u)
| ~ r2(v,w)
| ~ t2(w,u)
| f2(v)
| t(w,u10r2(w,v)) ),
file('KRS011-1.p',unknown),
[] ).
cnf(32,axiom,
( ~ d(u)
| ~ r2(v,w)
| ~ t2(w,u)
| f2(v)
| t(w,u10r3(w,v)) ),
file('KRS011-1.p',unknown),
[] ).
cnf(40,axiom,
( ~ e(u)
| ~ r3(v,w)
| ~ t3(w,u)
| f3(v)
| t(w,u11r1(w,v)) ),
file('KRS011-1.p',unknown),
[] ).
cnf(41,axiom,
( ~ e(u)
| ~ r3(v,w)
| ~ t3(w,u)
| f3(v)
| t(w,u11r2(w,v)) ),
file('KRS011-1.p',unknown),
[] ).
cnf(42,axiom,
( ~ e(u)
| ~ r3(v,w)
| ~ t3(w,u)
| f3(v)
| t(w,u11r3(w,v)) ),
file('KRS011-1.p',unknown),
[] ).
cnf(104,plain,
( ~ f1(u)
| ~ r(u,v)
| r2least(u)
| equalish(v,u9r4(u)) ),
inference(res,[status(thm),theory(equality)],[96,52]),
[iquote('0:Res:96.1,52.0')] ).
cnf(103,plain,
( ~ f2(u)
| ~ r(u,v)
| r2least(u)
| equalish(v,u10r4(u)) ),
inference(res,[status(thm),theory(equality)],[95,52]),
[iquote('0:Res:95.1,52.0')] ).
cnf(102,plain,
( ~ f3(u)
| ~ r(u,v)
| r2least(u)
| equalish(v,u11r4(u)) ),
inference(res,[status(thm),theory(equality)],[94,52]),
[iquote('0:Res:94.1,52.0')] ).
cnf(52,axiom,
( ~ r(u,v)
| ~ r(u,w)
| r2least(u)
| equalish(w,v) ),
file('KRS011-1.p',unknown),
[] ).
cnf(46,axiom,
( ~ f3(u)
| ~ f2(u)
| ~ f1(u)
| f(u) ),
file('KRS011-1.p',unknown),
[] ).
cnf(49,axiom,
( ~ r2least(u)
| ~ equalish(u14r2(u),u14r1(u)) ),
file('KRS011-1.p',unknown),
[] ).
cnf(99,plain,
( ~ f1(u)
| t(u9r4(u),u9r5(u)) ),
inference(res,[status(thm),theory(equality)],[14,4]),
[iquote('0:Res:14.1,4.0')] ).
cnf(98,plain,
( ~ f2(u)
| t(u10r4(u),u10r5(u)) ),
inference(res,[status(thm),theory(equality)],[24,5]),
[iquote('0:Res:24.1,5.0')] ).
cnf(97,plain,
( ~ f3(u)
| t(u11r4(u),u11r5(u)) ),
inference(res,[status(thm),theory(equality)],[34,6]),
[iquote('0:Res:34.1,6.0')] ).
cnf(14,axiom,
( ~ f1(u)
| t1(u9r4(u),u9r5(u)) ),
file('KRS011-1.p',unknown),
[] ).
cnf(24,axiom,
( ~ f2(u)
| t2(u10r4(u),u10r5(u)) ),
file('KRS011-1.p',unknown),
[] ).
cnf(34,axiom,
( ~ f3(u)
| t3(u11r4(u),u11r5(u)) ),
file('KRS011-1.p',unknown),
[] ).
cnf(4,axiom,
( ~ t1(u,v)
| t(u,v) ),
file('KRS011-1.p',unknown),
[] ).
cnf(5,axiom,
( ~ t2(u,v)
| t(u,v) ),
file('KRS011-1.p',unknown),
[] ).
cnf(6,axiom,
( ~ t3(u,v)
| t(u,v) ),
file('KRS011-1.p',unknown),
[] ).
cnf(96,plain,
( ~ f1(u)
| r(u,u9r4(u)) ),
inference(res,[status(thm),theory(equality)],[16,1]),
[iquote('0:Res:16.1,1.0')] ).
cnf(1,axiom,
( ~ r1(u,v)
| r(u,v) ),
file('KRS011-1.p',unknown),
[] ).
cnf(95,plain,
( ~ f2(u)
| r(u,u10r4(u)) ),
inference(res,[status(thm),theory(equality)],[26,2]),
[iquote('0:Res:26.1,2.0')] ).
cnf(94,plain,
( ~ f3(u)
| r(u,u11r4(u)) ),
inference(res,[status(thm),theory(equality)],[36,3]),
[iquote('0:Res:36.1,3.0')] ).
cnf(2,axiom,
( ~ r2(u,v)
| r(u,v) ),
file('KRS011-1.p',unknown),
[] ).
cnf(3,axiom,
( ~ r3(u,v)
| r(u,v) ),
file('KRS011-1.p',unknown),
[] ).
cnf(16,axiom,
( ~ f1(u)
| r1(u,u9r4(u)) ),
file('KRS011-1.p',unknown),
[] ).
cnf(26,axiom,
( ~ f2(u)
| r2(u,u10r4(u)) ),
file('KRS011-1.p',unknown),
[] ).
cnf(36,axiom,
( ~ f3(u)
| r3(u,u11r4(u)) ),
file('KRS011-1.p',unknown),
[] ).
cnf(50,axiom,
( ~ r2least(u)
| r(u,u14r1(u)) ),
file('KRS011-1.p',unknown),
[] ).
cnf(51,axiom,
( ~ r2least(u)
| r(u,u14r2(u)) ),
file('KRS011-1.p',unknown),
[] ).
cnf(13,axiom,
( ~ f1(u)
| c(u9r5(u)) ),
file('KRS011-1.p',unknown),
[] ).
cnf(23,axiom,
( ~ f2(u)
| d(u10r5(u)) ),
file('KRS011-1.p',unknown),
[] ).
cnf(33,axiom,
( ~ f3(u)
| e(u11r5(u)) ),
file('KRS011-1.p',unknown),
[] ).
cnf(10,axiom,
( ~ c(u)
| ~ d(u) ),
file('KRS011-1.p',unknown),
[] ).
cnf(11,axiom,
( ~ d(u)
| ~ e(u) ),
file('KRS011-1.p',unknown),
[] ).
cnf(12,axiom,
( ~ c(u)
| ~ e(u) ),
file('KRS011-1.p',unknown),
[] ).
cnf(43,axiom,
( ~ f(u)
| f3(u) ),
file('KRS011-1.p',unknown),
[] ).
cnf(44,axiom,
( ~ f(u)
| f2(u) ),
file('KRS011-1.p',unknown),
[] ).
cnf(45,axiom,
( ~ f(u)
| f1(u) ),
file('KRS011-1.p',unknown),
[] ).
cnf(92,plain,
~ g(exists__dfg),
inference(sor,[status(thm)],[58,47]),
[iquote('0:SoR:58.0,47.1')] ).
cnf(47,axiom,
( ~ g(u)
| r2least(u) ),
file('KRS011-1.p',unknown),
[] ).
cnf(48,axiom,
( ~ r2least(u)
| g(u) ),
file('KRS011-1.p',unknown),
[] ).
cnf(58,plain,
~ r2least(exists__dfg),
inference(res,[status(thm),theory(equality)],[48,54]),
[iquote('0:Res:48.1,54.0')] ).
cnf(54,axiom,
~ g(exists__dfg),
file('KRS011-1.p',unknown),
[] ).
cnf(55,plain,
f3(exists__dfg),
inference(res,[status(thm),theory(equality)],[53,43]),
[iquote('0:Res:53.0,43.0')] ).
cnf(56,plain,
f2(exists__dfg),
inference(res,[status(thm),theory(equality)],[53,44]),
[iquote('0:Res:53.0,44.0')] ).
cnf(57,plain,
f1(exists__dfg),
inference(res,[status(thm),theory(equality)],[53,45]),
[iquote('0:Res:53.0,45.0')] ).
cnf(53,axiom,
f(exists__dfg),
file('KRS011-1.p',unknown),
[] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : KRS011-1 : TPTP v8.1.0. Released v2.0.0.
% 0.03/0.12 % Command : run_spass %d %s
% 0.12/0.33 % Computer : n019.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 : Tue Jun 7 07:51:55 EDT 2022
% 0.12/0.34 % CPUTime :
% 0.18/0.41
% 0.18/0.41 SPASS V 3.9
% 0.18/0.41 SPASS beiseite: Completion found.
% 0.18/0.41 % SZS status CounterSatisfiable
% 0.18/0.41 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.18/0.41 SPASS derived 36 clauses, backtracked 0 clauses, performed 0 splits and kept 74 clauses.
% 0.18/0.41 SPASS allocated 75713 KBytes.
% 0.18/0.41 SPASS spent 0:00:00.06 on the problem.
% 0.18/0.41 0:00:00.03 for the input.
% 0.18/0.41 0:00:00.00 for the FLOTTER CNF translation.
% 0.18/0.41 0:00:00.00 for inferences.
% 0.18/0.41 0:00:00.00 for the backtracking.
% 0.18/0.41 0:00:00.01 for the reduction.
% 0.18/0.41
% 0.18/0.41
% 0.18/0.41 The saturated set of worked-off clauses is :
% 0.18/0.41 % SZS output start Saturation
% See solution above
%------------------------------------------------------------------------------