%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : LCL643+1.015 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n010.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:52 PM UTC 2026
% Result : CounterSatisfiable 153.86s 154.16s
% Output : Saturation 153.86s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named 3755ERROR: Could not build tree for root 3763ERROR: MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(3763,plain,
( ~ r1(u,v)
| ~ r1(w,u)
| p2(v) ),
inference(mrr,[status(thm)],[3755,3762]),
[iquote('21:MRR:3755.0,3762.0')] ).
cnf(3766,plain,
( ~ p2(u)
| ~ r1(skc55,u)
| skP2(u) ),
inference(mrr,[status(thm)],[3761,3764]),
[iquote('21:MRR:3761.0,3764.0')] ).
cnf(3752,plain,
( ~ r1(skc48,u)
| p1(u) ),
inference(mrr,[status(thm)],[75,3751]),
[iquote('11:MRR:75.2,3751.0')] ).
cnf(60,axiom,
~ p1(skf53(u)),
file('LCL643+1.015.p',unknown),
[] ).
cnf(36,axiom,
~ p2(skf102(u)),
file('LCL643+1.015.p',unknown),
[] ).
cnf(37,axiom,
~ p2(skf100(u)),
file('LCL643+1.015.p',unknown),
[] ).
cnf(38,axiom,
~ p2(skf96(u)),
file('LCL643+1.015.p',unknown),
[] ).
cnf(39,axiom,
~ p2(skf94(u)),
file('LCL643+1.015.p',unknown),
[] ).
cnf(40,axiom,
~ p2(skf92(u)),
file('LCL643+1.015.p',unknown),
[] ).
cnf(41,axiom,
~ p2(skf91(u)),
file('LCL643+1.015.p',unknown),
[] ).
cnf(61,axiom,
~ p2(skf51(u)),
file('LCL643+1.015.p',unknown),
[] ).
cnf(42,axiom,
~ p3(skf85(u)),
file('LCL643+1.015.p',unknown),
[] ).
cnf(43,axiom,
~ p3(skf83(u)),
file('LCL643+1.015.p',unknown),
[] ).
cnf(44,axiom,
~ p3(skf81(u)),
file('LCL643+1.015.p',unknown),
[] ).
cnf(45,axiom,
~ p3(skf79(u)),
file('LCL643+1.015.p',unknown),
[] ).
cnf(46,axiom,
~ p3(skf77(u)),
file('LCL643+1.015.p',unknown),
[] ).
cnf(47,axiom,
~ p3(skf76(u)),
file('LCL643+1.015.p',unknown),
[] ).
cnf(48,axiom,
~ p3(skf74(u)),
file('LCL643+1.015.p',unknown),
[] ).
cnf(49,axiom,
~ p3(skf73(u)),
file('LCL643+1.015.p',unknown),
[] ).
cnf(50,axiom,
~ p3(skf71(u)),
file('LCL643+1.015.p',unknown),
[] ).
cnf(51,axiom,
~ p3(skf70(u)),
file('LCL643+1.015.p',unknown),
[] ).
cnf(52,axiom,
~ p3(skf68(u)),
file('LCL643+1.015.p',unknown),
[] ).
cnf(53,axiom,
~ p3(skf67(u)),
file('LCL643+1.015.p',unknown),
[] ).
cnf(54,axiom,
~ p3(skf65(u)),
file('LCL643+1.015.p',unknown),
[] ).
cnf(55,axiom,
~ p3(skf64(u)),
file('LCL643+1.015.p',unknown),
[] ).
cnf(56,axiom,
~ p3(skf63(u)),
file('LCL643+1.015.p',unknown),
[] ).
cnf(57,axiom,
~ p3(skf61(u)),
file('LCL643+1.015.p',unknown),
[] ).
cnf(58,axiom,
~ p3(skf60(u)),
file('LCL643+1.015.p',unknown),
[] ).
cnf(59,axiom,
~ p3(skf59(u)),
file('LCL643+1.015.p',unknown),
[] ).
cnf(62,axiom,
~ p3(skf49(u)),
file('LCL643+1.015.p',unknown),
[] ).
cnf(1,axiom,
~ p1(skc118),
file('LCL643+1.015.p',unknown),
[] ).
cnf(6,axiom,
~ p1(skc108),
file('LCL643+1.015.p',unknown),
[] ).
cnf(15,axiom,
~ p1(skc90),
file('LCL643+1.015.p',unknown),
[] ).
cnf(28,axiom,
~ p1(skc64),
file('LCL643+1.015.p',unknown),
[] ).
cnf(35,axiom,
~ p1(skc48),
file('LCL643+1.015.p',unknown),
[] ).
cnf(2,axiom,
~ p2(skc116),
file('LCL643+1.015.p',unknown),
[] ).
cnf(8,axiom,
~ p2(skc104),
file('LCL643+1.015.p',unknown),
[] ).
cnf(18,axiom,
~ p2(skc84),
file('LCL643+1.015.p',unknown),
[] ).
cnf(32,axiom,
~ p2(skc56),
file('LCL643+1.015.p',unknown),
[] ).
cnf(34,axiom,
~ p2(skc48),
file('LCL643+1.015.p',unknown),
[] ).
cnf(3,axiom,
~ p3(skc114),
file('LCL643+1.015.p',unknown),
[] ).
cnf(4,axiom,
~ p3(skc112),
file('LCL643+1.015.p',unknown),
[] ).
cnf(5,axiom,
~ p3(skc109),
file('LCL643+1.015.p',unknown),
[] ).
cnf(7,axiom,
~ p3(skc105),
file('LCL643+1.015.p',unknown),
[] ).
cnf(9,axiom,
~ p3(skc101),
file('LCL643+1.015.p',unknown),
[] ).
cnf(10,axiom,
~ p3(skc100),
file('LCL643+1.015.p',unknown),
[] ).
cnf(11,axiom,
~ p3(skc97),
file('LCL643+1.015.p',unknown),
[] ).
cnf(12,axiom,
~ p3(skc96),
file('LCL643+1.015.p',unknown),
[] ).
cnf(13,axiom,
~ p3(skc92),
file('LCL643+1.015.p',unknown),
[] ).
cnf(14,axiom,
~ p3(skc91),
file('LCL643+1.015.p',unknown),
[] ).
cnf(16,axiom,
~ p3(skc86),
file('LCL643+1.015.p',unknown),
[] ).
cnf(17,axiom,
~ p3(skc85),
file('LCL643+1.015.p',unknown),
[] ).
cnf(19,axiom,
~ p3(skc80),
file('LCL643+1.015.p',unknown),
[] ).
cnf(20,axiom,
~ p3(skc79),
file('LCL643+1.015.p',unknown),
[] ).
cnf(21,axiom,
~ p3(skc78),
file('LCL643+1.015.p',unknown),
[] ).
cnf(22,axiom,
~ p3(skc74),
file('LCL643+1.015.p',unknown),
[] ).
cnf(23,axiom,
~ p3(skc73),
file('LCL643+1.015.p',unknown),
[] ).
cnf(24,axiom,
~ p3(skc72),
file('LCL643+1.015.p',unknown),
[] ).
cnf(25,axiom,
~ p3(skc67),
file('LCL643+1.015.p',unknown),
[] ).
cnf(26,axiom,
~ p3(skc66),
file('LCL643+1.015.p',unknown),
[] ).
cnf(27,axiom,
~ p3(skc65),
file('LCL643+1.015.p',unknown),
[] ).
cnf(29,axiom,
~ p3(skc59),
file('LCL643+1.015.p',unknown),
[] ).
cnf(30,axiom,
~ p3(skc58),
file('LCL643+1.015.p',unknown),
[] ).
cnf(31,axiom,
~ p3(skc57),
file('LCL643+1.015.p',unknown),
[] ).
cnf(3768,plain,
skP2(skc48),
inference(spt,[],[63]),
[iquote('22:Spt:63.0')] ).
cnf(3764,plain,
skP0(u),
inference(mrr,[status(thm)],[64,3762]),
[iquote('21:MRR:64.0,3762.0')] ).
cnf(3762,plain,
skP1(u),
inference(spt,[],[66]),
[iquote('21:Spt:66.0')] ).
cnf(33,axiom,
~ p3(skc48),
file('LCL643+1.015.p',unknown),
[] ).
cnf(3760,plain,
( ~ skP2(u)
| ~ r1(u,v)
| p2(v) ),
inference(spt,[],[81]),
[iquote('19:Spt:81.0,81.1,81.2')] ).
cnf(3754,plain,
( ~ r1(skc48,u)
| p2(u) ),
inference(spt,[],[69]),
[iquote('13:Spt:69.0,69.1')] ).
cnf(3753,plain,
( ~ r1(skc48,u)
| p3(u) ),
inference(spt,[],[68]),
[iquote('12:Spt:68.0,68.1')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LCL643+1.015 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_spass %d %s
% 0.10/0.36 % Computer : n010.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 15:38:09 UTC 2026
% 0.10/0.36 % CPUTime :
% 153.86/154.16
% 153.86/154.16 SPASS V 3.9
% 153.86/154.16 SPASS beiseite: Completion found.
% 153.86/154.16 % SZS status CounterSatisfiable
% 153.86/154.16 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 153.86/154.16 SPASS derived 28 clauses, backtracked 0 clauses, performed 22 splits and kept 359 clauses.
% 153.86/154.16 SPASS allocated 132984 KBytes.
% 153.86/154.16 SPASS spent 0:2:33.77 on the problem.
% 153.86/154.16 0:00:00.07 for the input.
% 153.86/154.16 0:0:43.14 for the FLOTTER CNF translation.
% 153.86/154.16 0:00:00.00 for inferences.
% 153.86/154.16 0:00:00.00 for the backtracking.
% 153.86/154.16 0:00:01.47 for the reduction.
% 153.86/154.16
% 153.86/154.16
% 153.86/154.16 The saturated set of worked-off clauses is :
% 153.86/154.16 % SZS output start Saturation
% See solution above
%------------------------------------------------------------------------------