%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : LCL639+1.001 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n017.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Mon Sep 7 01:07:50 PM UTC 2026
% Result : CounterSatisfiable 0.41s 0.66s
% Output : Saturation 0.41s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named 22ERROR: Could not build tree for root 93ERROR: MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(93,plain,
( ~ r1(skc4,u)
| ~ r1(v,u)
| ~ r1(skc4,v)
| r1(v,skf12(v)) ),
inference(res,[status(thm),theory(equality)],[13,49]),
[iquote('2:Res:13.1,49.0')] ).
cnf(135,plain,
( ~ r1(skc4,skf12(u))
| ~ r1(u,skc10)
| ~ r1(skc4,u) ),
inference(res,[status(thm),theory(equality)],[13,134]),
[iquote('2:Res:13.1,134.2')] ).
cnf(134,plain,
( ~ r1(u,skc10)
| ~ r1(skc4,u)
| ~ r1(skf12(u),v) ),
inference(mrr,[status(thm)],[128,41]),
[iquote('2:MRR:128.0,41.1')] ).
cnf(125,plain,
( ~ p1(skf12(u))
| ~ r1(u,skc10)
| ~ r1(skc4,u) ),
inference(res,[status(thm),theory(equality)],[91,43]),
[iquote('2:Res:91.2,43.1')] ).
cnf(112,plain,
( ~ p1(skf12(u))
| ~ r1(u,skc4)
| ~ r1(skc4,u) ),
inference(res,[status(thm),theory(equality)],[90,43]),
[iquote('2:Res:90.2,43.1')] ).
cnf(91,plain,
( ~ r1(u,skc10)
| ~ r1(skc4,u)
| r1(u,skf12(u)) ),
inference(res,[status(thm),theory(equality)],[2,49]),
[iquote('2:Res:2.0,49.0')] ).
cnf(90,plain,
( ~ r1(u,skc4)
| ~ r1(skc4,u)
| r1(u,skf12(u)) ),
inference(res,[status(thm),theory(equality)],[3,49]),
[iquote('2:Res:3.0,49.0')] ).
cnf(84,plain,
( ~ skP0(u)
| ~ r1(skc4,v)
| ~ r1(u,v) ),
inference(mrr,[status(thm)],[80,75]),
[iquote('2:MRR:80.3,75.1')] ).
cnf(77,plain,
( ~ skP0(u)
| ~ r1(u,skc4)
| r1(skc10,skf14(skc10)) ),
inference(res,[status(thm),theory(equality)],[3,46]),
[iquote('2:Res:3.0,46.1')] ).
cnf(101,plain,
( ~ r1(skc4,skf10(u))
| ~ r1(skc4,u) ),
inference(res,[status(thm),theory(equality)],[13,76]),
[iquote('2:Res:13.1,76.1')] ).
cnf(76,plain,
( ~ r1(skc4,u)
| ~ r1(skf10(u),v) ),
inference(mrr,[status(thm)],[72,41]),
[iquote('2:MRR:72.0,41.1')] ).
cnf(96,plain,
( ~ r1(skc4,skf13(u))
| ~ r1(skc4,u) ),
inference(res,[status(thm),theory(equality)],[13,75]),
[iquote('2:Res:13.1,75.1')] ).
cnf(75,plain,
( ~ r1(skc4,u)
| ~ r1(skf13(u),v) ),
inference(mrr,[status(thm)],[71,41]),
[iquote('2:MRR:71.0,41.1')] ).
cnf(89,plain,
~ r1(skc4,skc4),
inference(mrr,[status(thm)],[67,88]),
[iquote('2:MRR:67.1,88.0')] ).
cnf(88,plain,
~ skP0(skc4),
inference(res,[status(thm),theory(equality)],[3,83]),
[iquote('2:Res:3.0,83.1')] ).
cnf(49,plain,
( ~ r1(u,v)
| ~ r1(w,u)
| ~ r1(skc4,w)
| r1(w,skf12(w)) ),
inference(mrr,[status(thm)],[22,43]),
[iquote('2:MRR:22.3,43.0')] ).
cnf(83,plain,
( ~ skP0(u)
| ~ r1(u,skc10) ),
inference(mrr,[status(thm)],[78,47]),
[iquote('2:MRR:78.2,47.0')] ).
cnf(68,plain,
( ~ skP1(skc4)
| ~ r1(skc10,u) ),
inference(res,[status(thm),theory(equality)],[3,45]),
[iquote('2:Res:3.0,45.1')] ).
cnf(85,plain,
~ r1(skc4,skc12),
inference(res,[status(thm),theory(equality)],[13,74]),
[iquote('2:Res:13.1,74.0')] ).
cnf(74,plain,
~ r1(skc12,u),
inference(ssi,[status(thm)],[70,50]),
[iquote('2:SSi:70.0,50.0')] ).
cnf(46,plain,
( ~ skP0(u)
| ~ r1(v,w)
| ~ r1(u,v)
| r1(w,skf14(w)) ),
inference(mrr,[status(thm)],[21,43]),
[iquote('2:MRR:21.3,43.0')] ).
cnf(45,plain,
( ~ skP1(u)
| ~ r1(u,v)
| ~ r1(v,w) ),
inference(mrr,[status(thm)],[20,42]),
[iquote('2:MRR:20.0,42.0')] ).
cnf(63,plain,
( ~ r1(skc4,skf8(u))
| ~ r1(skc4,u)
| skP0(u) ),
inference(res,[status(thm),theory(equality)],[13,48]),
[iquote('2:Res:13.1,48.1')] ).
cnf(62,plain,
( ~ p1(skf8(u))
| ~ r1(skc4,u)
| skP0(u) ),
inference(res,[status(thm),theory(equality)],[15,43]),
[iquote('2:Res:15.2,43.1')] ).
cnf(48,plain,
( ~ r1(skc4,u)
| ~ r1(skf8(u),v)
| skP0(u) ),
inference(mrr,[status(thm)],[19,43]),
[iquote('2:MRR:19.3,43.0')] ).
cnf(15,axiom,
( ~ r1(skc4,u)
| skP0(u)
| r1(u,skf8(u)) ),
file('LCL639+1.001.p',unknown),
[] ).
cnf(59,plain,
( ~ p1(skf10(u))
| ~ r1(skc4,u) ),
inference(res,[status(thm),theory(equality)],[44,43]),
[iquote('2:Res:44.1,43.1')] ).
cnf(44,plain,
( ~ r1(skc4,u)
| r1(u,skf10(u)) ),
inference(mrr,[status(thm)],[18,42]),
[iquote('2:MRR:18.0,42.0')] ).
cnf(56,plain,
( ~ p1(skf13(u))
| ~ r1(skc4,u) ),
inference(res,[status(thm),theory(equality)],[13,43]),
[iquote('2:Res:13.1,43.1')] ).
cnf(55,plain,
~ r1(skc4,skc11),
inference(res,[status(thm),theory(equality)],[13,47]),
[iquote('2:Res:13.1,47.0')] ).
cnf(53,plain,
~ p1(skc12),
inference(res,[status(thm),theory(equality)],[1,43]),
[iquote('2:Res:1.0,43.1')] ).
cnf(13,axiom,
( ~ r1(skc4,u)
| r1(u,skf13(u)) ),
file('LCL639+1.001.p',unknown),
[] ).
cnf(52,plain,
~ p1(skc11),
inference(res,[status(thm),theory(equality)],[2,43]),
[iquote('2:Res:2.0,43.1')] ).
cnf(51,plain,
~ p1(skc10),
inference(res,[status(thm),theory(equality)],[3,43]),
[iquote('2:Res:3.0,43.1')] ).
cnf(43,plain,
( ~ p1(u)
| ~ r1(v,u) ),
inference(mrr,[status(thm)],[17,42]),
[iquote('2:MRR:17.1,42.0')] ).
cnf(47,plain,
~ r1(skc11,u),
inference(mrr,[status(thm)],[11,43]),
[iquote('2:MRR:11.1,43.0')] ).
cnf(5,axiom,
~ p1(skf14(u)),
file('LCL639+1.001.p',unknown),
[] ).
cnf(6,axiom,
~ p1(skf12(u)),
file('LCL639+1.001.p',unknown),
[] ).
cnf(7,axiom,
~ p1(skf10(u)),
file('LCL639+1.001.p',unknown),
[] ).
cnf(8,axiom,
~ p1(skf9(u)),
file('LCL639+1.001.p',unknown),
[] ).
cnf(9,axiom,
~ p1(skf8(u)),
file('LCL639+1.001.p',unknown),
[] ).
cnf(4,axiom,
~ p1(skc12),
file('LCL639+1.001.p',unknown),
[] ).
cnf(1,axiom,
r1(skc10,skc12),
file('LCL639+1.001.p',unknown),
[] ).
cnf(2,axiom,
r1(skc10,skc11),
file('LCL639+1.001.p',unknown),
[] ).
cnf(50,plain,
skP1(skc10),
inference(res,[status(thm),theory(equality)],[3,41]),
[iquote('1:Res:3.0,41.0')] ).
cnf(3,axiom,
r1(skc4,skc10),
file('LCL639+1.001.p',unknown),
[] ).
cnf(42,plain,
skP2(u),
inference(spt,[],[10]),
[iquote('2:Spt:10.0')] ).
cnf(41,plain,
( ~ r1(skc4,u)
| skP1(u) ),
inference(spt,[],[14]),
[iquote('1:Spt:14.0,14.1')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL639+1.001 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_spass %d %s
% 0.10/0.36 % Computer : n017.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Sat Sep 5 02:36:06 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.41/0.66
% 0.41/0.66 SPASS V 3.9
% 0.41/0.66 SPASS beiseite: Completion found.
% 0.41/0.66 % SZS status CounterSatisfiable
% 0.41/0.66 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.41/0.66 SPASS derived 96 clauses, backtracked 0 clauses, performed 2 splits and kept 65 clauses.
% 0.41/0.66 SPASS allocated 98076 KBytes.
% 0.41/0.66 SPASS spent 0:00:00.27 on the problem.
% 0.41/0.66 0:00:00.09 for the input.
% 0.41/0.66 0:00:00.12 for the FLOTTER CNF translation.
% 0.41/0.66 0:00:00.00 for inferences.
% 0.41/0.66 0:00:00.00 for the backtracking.
% 0.41/0.66 0:00:00.01 for the reduction.
% 0.41/0.66
% 0.41/0.66
% 0.41/0.66 The saturated set of worked-off clauses is :
% 0.41/0.66 % SZS output start Saturation
% See solution above
%------------------------------------------------------------------------------