%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : SYN516+1 : TPTP v8.1.0. Released v2.1.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n023.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:22:23 EDT 2022
% Result : CounterSatisfiable 0.19s 0.45s
% Output : Saturation 0.19s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named 65)
% Comments :
%------------------------------------------------------------------------------
cnf(90,plain,
( ~ ndr1_1(u)
| ~ skC2
| ~ c5_2(u,a36)
| c5_1(u)
| c2_2(u,v)
| c3_2(u,v) ),
inference(mrr,[status(thm)],[65,75]),
[iquote('0:MRR:65.3,75.0')] ).
cnf(89,plain,
( ~ ndr1_1(u)
| ~ skC2
| ~ c1_2(u,a36)
| c5_1(u)
| c2_2(u,v)
| c3_2(u,v) ),
inference(mrr,[status(thm)],[66,75]),
[iquote('0:MRR:66.3,75.0')] ).
cnf(160,plain,
( ~ c1_2(u,a37)
| ~ c5_2(u,a37)
| c4_1(u)
| c5_1(u)
| c3_1(u)
| c2_2(u,a29) ),
inference(mrr,[status(thm)],[159,146]),
[iquote('9:MRR:159.0,146.2')] ).
cnf(88,plain,
( ~ ndr1_1(u)
| ~ skC2
| c5_1(u)
| c2_2(u,v)
| c3_2(u,v)
| c3_2(u,a36) ),
inference(mrr,[status(thm)],[63,75]),
[iquote('0:MRR:63.2,75.0')] ).
cnf(174,plain,
( ~ c5_2(a39,a40)
| ~ c3_2(a39,a40)
| ~ c1_2(a39,a29)
| c3_1(a39) ),
inference(ssi,[status(thm)],[173,151,152]),
[iquote('6:SSi:173.0,151.0,152.0')] ).
cnf(85,plain,
( ~ c5_1(u)
| ~ c3_0
| c4_1(u)
| c3_2(u,a38) ),
inference(mrr,[status(thm)],[60,75]),
[iquote('0:MRR:60.2,75.0')] ).
cnf(86,plain,
( ~ c5_1(u)
| ~ c3_0
| c4_1(u)
| c1_2(u,a38) ),
inference(mrr,[status(thm)],[59,75]),
[iquote('0:MRR:59.2,75.0')] ).
cnf(155,plain,
( ~ c5_2(a39,u)
| c1_2(a39,u) ),
inference(mrr,[status(thm)],[84,150]),
[iquote('6:MRR:84.0,150.0')] ).
cnf(147,plain,
( ~ c3_0
| c4_1(u)
| ndr1_1(u) ),
inference(mrr,[status(thm)],[82,146]),
[iquote('3:MRR:82.0,146.1')] ).
cnf(76,plain,
( ~ skC0
| c2_1(u)
| ndr1_1(u) ),
inference(mrr,[status(thm)],[51,75]),
[iquote('0:MRR:51.1,75.0')] ).
cnf(29,axiom,
( ~ c2_0
| ~ c3_1(a46) ),
file('SYN516+1.p',unknown),
[] ).
cnf(169,plain,
~ c4_2(a44,a45),
inference(mrr,[status(thm)],[138,163]),
[iquote('12:MRR:138.1,163.0')] ).
cnf(168,plain,
~ c2_2(a44,a45),
inference(mrr,[status(thm)],[137,163]),
[iquote('12:MRR:137.1,163.0')] ).
cnf(176,plain,
~ c4_0,
inference(spt,[],[140]),
[iquote('16:Spt:140.0')] ).
cnf(167,plain,
c1_2(a44,a45),
inference(mrr,[status(thm)],[136,163]),
[iquote('12:MRR:136.0,163.0')] ).
cnf(154,plain,
c1_2(a39,a40),
inference(mrr,[status(thm)],[31,150]),
[iquote('6:MRR:31.0,150.0')] ).
cnf(153,plain,
c2_2(a39,a40),
inference(mrr,[status(thm)],[32,150]),
[iquote('6:MRR:32.0,150.0')] ).
cnf(166,plain,
ndr1_1(a44),
inference(mrr,[status(thm)],[135,163]),
[iquote('12:MRR:135.0,163.0')] ).
cnf(165,plain,
c3_1(a44),
inference(mrr,[status(thm)],[134,163]),
[iquote('12:MRR:134.0,163.0')] ).
cnf(164,plain,
c4_1(a44),
inference(mrr,[status(thm)],[133,163]),
[iquote('12:MRR:133.0,163.0')] ).
cnf(172,plain,
~ skC5,
inference(spt,[],[35]),
[iquote('15:Spt:35.0')] ).
cnf(152,plain,
ndr1_1(a39),
inference(mrr,[status(thm)],[16,150]),
[iquote('6:MRR:16.0,150.0')] ).
cnf(171,plain,
( ~ c5_2(u,a28)
| c2_1(u) ),
inference(spt,[],[79]),
[iquote('14:Spt:79.1,79.2')] ).
cnf(170,plain,
( ~ c3_2(u,a28)
| c2_1(u) ),
inference(spt,[],[78]),
[iquote('13:Spt:78.1,78.2')] ).
cnf(163,plain,
~ skC4,
inference(spt,[],[34]),
[iquote('12:Spt:34.0')] ).
cnf(151,plain,
c2_1(a39),
inference(mrr,[status(thm)],[17,150]),
[iquote('6:MRR:17.0,150.0')] ).
cnf(162,plain,
~ skC1,
inference(spt,[],[15]),
[iquote('11:Spt:15.0')] ).
cnf(161,plain,
( ~ c2_2(u,a37)
| c4_1(u)
| c5_1(u) ),
inference(spt,[],[83]),
[iquote('10:Spt:83.0,83.2,83.3')] ).
cnf(158,plain,
( c4_1(u)
| c5_1(u)
| c3_2(u,a37) ),
inference(spt,[],[80]),
[iquote('9:Spt:80.1,80.2,80.3')] ).
cnf(157,plain,
( c4_1(u)
| c5_1(u)
| c4_2(u,a37) ),
inference(spt,[],[81]),
[iquote('8:Spt:81.1,81.2,81.3')] ).
cnf(75,plain,
ndr1_0,
inference(mrr,[status(thm)],[12,74,7]),
[iquote('0:MRR:12.0,12.2,74.1,7.0')] ).
cnf(156,plain,
( ~ c5_1(u)
| ~ c5_2(u,a38)
| c4_1(u) ),
inference(spt,[],[87]),
[iquote('7:Spt:87.0,87.2,87.3')] ).
cnf(150,plain,
skC3,
inference(spt,[],[25]),
[iquote('6:Spt:25.1')] ).
cnf(149,plain,
( ~ ndr1_1(u)
| ~ c1_2(u,v)
| ~ c5_2(u,v)
| ~ c3_2(u,v)
| ~ c1_2(u,a29)
| c3_1(u) ),
inference(spt,[],[96]),
[iquote('5:Spt:96.0,96.1,96.2,96.3,96.4,96.6')] ).
cnf(148,plain,
( ~ ndr1_1(u)
| ~ c3_2(u,v)
| ~ c1_2(u,v)
| ~ c5_2(u,v)
| c3_1(u)
| c2_2(u,a29) ),
inference(spt,[],[95]),
[iquote('4:Spt:95.0,95.1,95.2,95.3,95.5,95.6')] ).
cnf(146,plain,
( c4_1(u)
| c5_1(u)
| ndr1_1(u) ),
inference(spt,[],[77]),
[iquote('3:Spt:77.1,77.2,77.3')] ).
cnf(139,plain,
c1_0,
inference(spt,[],[91]),
[iquote('2:Spt:91.3')] ).
cnf(132,plain,
c5_0,
inference(spt,[],[37]),
[iquote('1:Spt:37.1')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SYN516+1 : TPTP v8.1.0. Released v2.1.0.
% 0.12/0.13 % Command : run_spass %d %s
% 0.12/0.34 % Computer : n023.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 600
% 0.12/0.34 % DateTime : Mon Jul 11 23:43:39 EDT 2022
% 0.12/0.34 % CPUTime :
% 0.19/0.45
% 0.19/0.45 SPASS V 3.9
% 0.19/0.45 SPASS beiseite: Completion found.
% 0.19/0.45 % SZS status CounterSatisfiable
% 0.19/0.45 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.19/0.45 SPASS derived 43 clauses, backtracked 0 clauses, performed 16 splits and kept 112 clauses.
% 0.19/0.45 SPASS allocated 97745 KBytes.
% 0.19/0.45 SPASS spent 0:00:00.10 on the problem.
% 0.19/0.45 0:00:00.04 for the input.
% 0.19/0.45 0:00:00.03 for the FLOTTER CNF translation.
% 0.19/0.45 0:00:00.00 for inferences.
% 0.19/0.45 0:00:00.00 for the backtracking.
% 0.19/0.45 0:00:00.01 for the reduction.
% 0.19/0.45
% 0.19/0.45
% 0.19/0.45 The saturated set of worked-off clauses is :
% 0.19/0.45 % SZS output start Saturation
% See solution above
%------------------------------------------------------------------------------