%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : SYN433-1 : TPTP v8.1.0. Released v2.1.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 : Thu Jul 21 12:21:28 EDT 2022
% Result : Satisfiable 0.19s 0.50s
% Output : Saturation 0.19s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named 230)
% Comments :
%------------------------------------------------------------------------------
cnf(1263,plain,
( ~ c2_1(u)
| c3_1(u) ),
inference(mrr,[status(thm)],[230,1262]),
[iquote('32:MRR:230.2,1262.0')] ).
cnf(1262,plain,
( ~ c0_1(u)
| c3_1(u) ),
inference(spt,[],[1242]),
[iquote('32:Spt:1242.0,1242.2')] ).
cnf(227,plain,
( ~ c3_1(u)
| c2_1(u)
| c0_1(u) ),
inference(spt,[],[115]),
[iquote('2:Spt:115.2,115.6,115.7')] ).
cnf(1252,plain,
~ c0_1(a197),
inference(mrr,[status(thm)],[1250,458]),
[iquote('30:MRR:1250.1,458.0')] ).
cnf(1241,plain,
( ~ c3_1(u)
| c1_1(u) ),
inference(mrr,[status(thm)],[1034,1196]),
[iquote('25:MRR:1034.1,1196.0')] ).
cnf(1196,plain,
( ~ c0_1(u)
| c1_1(u) ),
inference(ems,[status(thm)],[402,1058,1059]),
[iquote('25:EmS:402.0,402.1,1058.0,1059.0')] ).
cnf(1240,plain,
~ c0_1(a200),
inference(mrr,[status(thm)],[78,1237]),
[iquote('28:MRR:78.0,1237.0')] ).
cnf(1246,plain,
~ hskp11,
inference(spt,[],[83]),
[iquote('31:Spt:83.0')] ).
cnf(1239,plain,
c3_1(a200),
inference(mrr,[status(thm)],[57,1237]),
[iquote('28:MRR:57.0,1237.0')] ).
cnf(1244,plain,
~ hskp5,
inference(spt,[],[99]),
[iquote('30:Spt:99.0')] ).
cnf(1237,plain,
hskp15,
inference(spt,[],[1236,56,1063]),
[iquote('28:Spt:1236.0,56.0,1063.0')] ).
cnf(1243,plain,
~ hskp22,
inference(spt,[],[40]),
[iquote('29:Spt:40.0')] ).
cnf(1238,plain,
c2_1(a200),
inference(spt,[],[1236,56]),
[iquote('28:Spt:1236.0,56.1')] ).
cnf(1077,plain,
c1_1(a204),
inference(ssi,[status(thm)],[1075,286,287]),
[iquote('23:SSi:1075.0,286.0,287.0')] ).
cnf(1059,plain,
c2_1(a218),
inference(mrr,[status(thm)],[36,1056]),
[iquote('25:MRR:36.0,1056.0')] ).
cnf(1058,plain,
c0_1(a218),
inference(mrr,[status(thm)],[37,1056]),
[iquote('25:MRR:37.0,1056.0')] ).
cnf(1062,plain,
~ hskp8,
inference(spt,[],[64]),
[iquote('27:Spt:64.0')] ).
cnf(1056,plain,
hskp23,
inference(spt,[],[1055,38,1036]),
[iquote('25:Spt:1055.0,38.0,1036.0')] ).
cnf(1060,plain,
~ hskp1,
inference(spt,[],[72]),
[iquote('26:Spt:72.0')] ).
cnf(1057,plain,
c3_1(a218),
inference(spt,[],[1055,38]),
[iquote('25:Spt:1055.0,38.1')] ).
cnf(1031,plain,
~ c2_1(a222),
inference(mrr,[status(thm)],[82,1028]),
[iquote('21:MRR:82.0,1028.0')] ).
cnf(1035,plain,
~ hskp21,
inference(spt,[],[42]),
[iquote('24:Spt:42.0')] ).
cnf(1030,plain,
c3_1(a222),
inference(mrr,[status(thm)],[61,1028]),
[iquote('21:MRR:61.0,1028.0')] ).
cnf(1033,plain,
~ hskp6,
inference(spt,[],[66]),
[iquote('23:Spt:66.0')] ).
cnf(1028,plain,
hskp12,
inference(spt,[],[1027,62,413]),
[iquote('21:Spt:1027.0,62.0,413.0')] ).
cnf(1032,plain,
~ hskp2,
inference(spt,[],[69]),
[iquote('22:Spt:69.0')] ).
cnf(1029,plain,
c0_1(a222),
inference(spt,[],[1027,62]),
[iquote('21:Spt:1027.0,62.1')] ).
cnf(459,plain,
~ c3_1(a197),
inference(mrr,[status(thm)],[398,458]),
[iquote('10:MRR:398.1,458.0')] ).
cnf(458,plain,
~ c2_1(a197),
inference(mrr,[status(thm)],[457,394]),
[iquote('10:MRR:457.1,394.0')] ).
cnf(412,plain,
~ hskp13,
inference(spt,[],[60]),
[iquote('20:Spt:60.0')] ).
cnf(410,plain,
~ hskp7,
inference(spt,[],[65]),
[iquote('19:Spt:65.0')] ).
cnf(409,plain,
~ hskp19,
inference(spt,[],[48]),
[iquote('18:Spt:48.0')] ).
cnf(407,plain,
~ hskp20,
inference(spt,[],[44]),
[iquote('17:Spt:44.0')] ).
cnf(405,plain,
~ hskp24,
inference(spt,[],[34]),
[iquote('16:Spt:34.0')] ).
cnf(401,plain,
~ hskp14,
inference(spt,[],[58]),
[iquote('15:Spt:58.0')] ).
cnf(400,plain,
~ hskp16,
inference(spt,[],[55]),
[iquote('14:Spt:55.0')] ).
cnf(395,plain,
~ c3_1(a197),
inference(mrr,[status(thm)],[106,392]),
[iquote('10:MRR:106.0,392.0')] ).
cnf(399,plain,
~ hskp3,
inference(spt,[],[68]),
[iquote('13:Spt:68.0')] ).
cnf(394,plain,
~ c0_1(a197),
inference(mrr,[status(thm)],[107,392]),
[iquote('10:MRR:107.0,392.0')] ).
cnf(397,plain,
~ hskp10,
inference(spt,[],[63]),
[iquote('12:Spt:63.0')] ).
cnf(392,plain,
hskp0,
inference(spt,[],[391,73,289]),
[iquote('10:Spt:391.0,73.0,289.0')] ).
cnf(396,plain,
~ hskp25,
inference(spt,[],[32]),
[iquote('11:Spt:32.0')] ).
cnf(393,plain,
c1_1(a197),
inference(spt,[],[391,73]),
[iquote('10:Spt:391.0,73.1')] ).
cnf(303,plain,
~ c2_1(a215),
inference(mrr,[status(thm)],[301,248]),
[iquote('6:MRR:301.1,248.0')] ).
cnf(302,plain,
~ c0_1(a215),
inference(mrr,[status(thm)],[300,249]),
[iquote('6:MRR:300.1,249.0')] ).
cnf(288,plain,
~ c0_1(a204),
inference(mrr,[status(thm)],[76,285]),
[iquote('9:MRR:76.0,285.0')] ).
cnf(265,plain,
~ c3_1(a215),
inference(mrr,[status(thm)],[264,250]),
[iquote('6:MRR:264.1,250.0')] ).
cnf(287,plain,
c3_1(a204),
inference(mrr,[status(thm)],[53,285]),
[iquote('9:MRR:53.0,285.0')] ).
cnf(286,plain,
c2_1(a204),
inference(mrr,[status(thm)],[52,285]),
[iquote('9:MRR:52.0,285.0')] ).
cnf(284,plain,
c1_1(a206),
inference(mrr,[status(thm)],[49,281]),
[iquote('8:MRR:49.0,281.0')] ).
cnf(283,plain,
c3_1(a206),
inference(mrr,[status(thm)],[50,281]),
[iquote('8:MRR:50.0,281.0')] ).
cnf(282,plain,
c0_1(a206),
inference(mrr,[status(thm)],[51,281]),
[iquote('8:MRR:51.0,281.0')] ).
cnf(279,plain,
~ hskp4,
inference(spt,[],[278,28,251]),
[iquote('7:Spt:278.0,28.0,251.0')] ).
cnf(285,plain,
hskp17,
inference(spt,[],[27]),
[iquote('9:Spt:27.0')] ).
cnf(281,plain,
hskp18,
inference(spt,[],[280]),
[iquote('8:Spt:280.0')] ).
cnf(250,plain,
~ c2_1(a215),
inference(mrr,[status(thm)],[88,247]),
[iquote('6:MRR:88.0,247.0')] ).
cnf(249,plain,
~ c1_1(a215),
inference(mrr,[status(thm)],[89,247]),
[iquote('6:MRR:89.0,247.0')] ).
cnf(248,plain,
~ c0_1(a215),
inference(mrr,[status(thm)],[90,247]),
[iquote('6:MRR:90.0,247.0')] ).
cnf(247,plain,
hskp9,
inference(spt,[],[29]),
[iquote('6:Spt:29.0')] ).
cnf(236,plain,
ndr1_0,
inference(spt,[],[26]),
[iquote('5:Spt:26.1')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.12 % Problem : SYN433-1 : TPTP v8.1.0. Released v2.1.0.
% 0.12/0.13 % Command : run_spass %d %s
% 0.13/0.34 % Computer : n019.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.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 600
% 0.13/0.34 % DateTime : Mon Jul 11 17:39:08 EDT 2022
% 0.13/0.34 % CPUTime :
% 0.19/0.50
% 0.19/0.50 SPASS V 3.9
% 0.19/0.50 SPASS beiseite: Completion found.
% 0.19/0.50 % SZS status CounterSatisfiable
% 0.19/0.50 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.19/0.50 SPASS derived 842 clauses, backtracked 598 clauses, performed 142 splits and kept 1106 clauses.
% 0.19/0.50 SPASS allocated 76122 KBytes.
% 0.19/0.50 SPASS spent 0:00:00.14 on the problem.
% 0.19/0.50 0:00:00.04 for the input.
% 0.19/0.50 0:00:00.00 for the FLOTTER CNF translation.
% 0.19/0.50 0:00:00.01 for inferences.
% 0.19/0.50 0:00:00.00 for the backtracking.
% 0.19/0.50 0:00:00.06 for the reduction.
% 0.19/0.50
% 0.19/0.50
% 0.19/0.50 The saturated set of worked-off clauses is :
% 0.19/0.50 % SZS output start Saturation
% See solution above
%------------------------------------------------------------------------------