%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : SYN529+1 : TPTP v8.1.0. Released v2.1.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n025.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:34 EDT 2022
% Result : CounterSatisfiable 0.18s 0.46s
% Output : Saturation 0.18s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named 129)
% Comments :
%------------------------------------------------------------------------------
cnf(169,plain,
( ~ c2_1(u)
| ~ ndr1_1(u)
| ~ skC1
| ~ c4_2(u,v)
| ~ c3_2(u,v)
| c2_2(u,v)
| c5_2(u,a321) ),
inference(mrr,[status(thm)],[129,140]),
[iquote('0:MRR:129.5,140.0')] ).
cnf(289,plain,
( ~ ndr1_1(u)
| ~ c3_2(u,v)
| skP0(u)
| c1_2(u,v)
| c2_2(u,v)
| c3_2(u,a341) ),
inference(mrr,[status(thm)],[256,286]),
[iquote('17:MRR:256.2,286.0')] ).
cnf(288,plain,
( ~ ndr1_1(u)
| ~ c3_2(u,v)
| skP0(u)
| c1_2(u,v)
| c2_2(u,v)
| c4_2(u,a341) ),
inference(mrr,[status(thm)],[255,286]),
[iquote('17:MRR:255.2,286.0')] ).
cnf(307,plain,
( ~ c2_1(a353)
| ~ c1_2(a353,u)
| c3_1(a353)
| c2_2(a353,u)
| c3_2(a353,u) ),
inference(ssi,[status(thm)],[306,279]),
[iquote('14:SSi:306.1,279.0')] ).
cnf(315,plain,
( ~ skP0(a353)
| c3_2(a353,a340) ),
inference(mrr,[status(thm)],[313,104]),
[iquote('21:MRR:313.1,104.1')] ).
cnf(311,plain,
( ~ c2_2(a353,u)
| c4_2(a353,u)
| c3_2(a353,u) ),
inference(spt,[],[309]),
[iquote('21:Spt:309.0,309.3,309.4')] ).
cnf(287,plain,
( ~ ndr1_1(u)
| ~ c3_2(u,v)
| skP0(u)
| c1_2(u,v)
| c2_2(u,v)
| c2_2(u,a341) ),
inference(mrr,[status(thm)],[254,286]),
[iquote('17:MRR:254.2,286.0')] ).
cnf(299,plain,
( ~ c3_1(a318)
| ~ c3_2(a318,a350)
| c5_2(a318,a319)
| c1_2(a318,a319) ),
inference(ssi,[status(thm)],[295,273]),
[iquote('13:SSi:295.0,273.0')] ).
cnf(298,plain,
( ~ c3_1(a318)
| ~ c1_2(a318,a350)
| c5_2(a318,a319)
| c1_2(a318,a319) ),
inference(ssi,[status(thm)],[294,273]),
[iquote('13:SSi:294.0,273.0')] ).
cnf(297,plain,
( ~ c3_1(a318)
| c5_2(a318,a319)
| c1_2(a318,a319)
| c2_2(a318,a350) ),
inference(ssi,[status(thm)],[296,273]),
[iquote('13:SSi:296.0,273.0')] ).
cnf(305,plain,
( ~ c1_2(a353,a334)
| c5_1(a353)
| c3_1(a353)
| c3_2(a353,a334) ),
inference(res,[status(thm),theory(equality)],[268,282]),
[iquote('14:Res:268.2,282.0')] ).
cnf(283,plain,
( ~ c5_2(a353,u)
| ~ c2_2(a353,u)
| c3_2(a353,u) ),
inference(mrr,[status(thm)],[250,278]),
[iquote('14:MRR:250.2,278.0')] ).
cnf(282,plain,
( ~ c4_2(a353,u)
| ~ c1_2(a353,u)
| c3_2(a353,u) ),
inference(mrr,[status(thm)],[249,278]),
[iquote('14:MRR:249.2,278.0')] ).
cnf(104,axiom,
( ~ skP0(u)
| ~ c4_2(u,a340) ),
file('SYN529+1.p',unknown),
[] ).
cnf(105,axiom,
( ~ skP0(u)
| ~ c1_2(u,a340) ),
file('SYN529+1.p',unknown),
[] ).
cnf(102,axiom,
( ~ skP0(u)
| c2_2(u,a340) ),
file('SYN529+1.p',unknown),
[] ).
cnf(79,axiom,
( ~ skP0(u)
| ndr1_1(u) ),
file('SYN529+1.p',unknown),
[] ).
cnf(277,plain,
~ c4_2(a318,a320),
inference(mrr,[status(thm)],[242,272]),
[iquote('13:MRR:242.1,272.0')] ).
cnf(292,plain,
~ c3_1(a333),
inference(mrr,[status(thm)],[238,291]),
[iquote('19:MRR:238.1,291.0')] ).
cnf(281,plain,
c2_2(a353,a354),
inference(mrr,[status(thm)],[248,278]),
[iquote('14:MRR:248.0,278.0')] ).
cnf(280,plain,
c3_2(a353,a354),
inference(mrr,[status(thm)],[247,278]),
[iquote('14:MRR:247.0,278.0')] ).
cnf(276,plain,
c4_2(a318,a319),
inference(mrr,[status(thm)],[241,272]),
[iquote('13:MRR:241.0,272.0')] ).
cnf(275,plain,
c2_2(a318,a319),
inference(mrr,[status(thm)],[240,272]),
[iquote('13:MRR:240.0,272.0')] ).
cnf(274,plain,
c2_2(a318,a320),
inference(mrr,[status(thm)],[239,272]),
[iquote('13:MRR:239.0,272.0')] ).
cnf(245,plain,
~ c1_1(a343),
inference(mrr,[status(thm)],[30,236]),
[iquote('1:MRR:30.1,236.0')] ).
cnf(279,plain,
ndr1_1(a353),
inference(mrr,[status(thm)],[244,278]),
[iquote('14:MRR:244.0,278.0')] ).
cnf(273,plain,
ndr1_1(a318),
inference(mrr,[status(thm)],[237,272]),
[iquote('13:MRR:237.0,272.0')] ).
cnf(293,plain,
~ skC3,
inference(spt,[],[39]),
[iquote('20:Spt:39.0')] ).
cnf(243,plain,
c2_1(a343),
inference(mrr,[status(thm)],[8,236]),
[iquote('1:MRR:8.0,236.0')] ).
cnf(291,plain,
~ skC4,
inference(spt,[],[42]),
[iquote('19:Spt:42.0')] ).
cnf(290,plain,
~ skC7,
inference(spt,[],[47]),
[iquote('18:Spt:47.0')] ).
cnf(236,plain,
~ c3_0,
inference(mrr,[status(thm)],[144,235]),
[iquote('1:MRR:144.1,235.0')] ).
cnf(286,plain,
~ skC5,
inference(spt,[],[43]),
[iquote('17:Spt:43.0')] ).
cnf(285,plain,
~ skC6,
inference(spt,[],[46]),
[iquote('16:Spt:46.0')] ).
cnf(284,plain,
~ skC2,
inference(spt,[],[38]),
[iquote('15:Spt:38.0')] ).
cnf(253,plain,
c2_0,
inference(mrr,[status(thm)],[2,252]),
[iquote('3:MRR:2.0,252.0')] ).
cnf(278,plain,
~ skC8,
inference(spt,[],[49]),
[iquote('14:Spt:49.0')] ).
cnf(272,plain,
~ skC0,
inference(spt,[],[37]),
[iquote('13:Spt:37.0')] ).
cnf(268,plain,
( c5_1(u)
| c3_1(u)
| c4_2(u,a334) ),
inference(spt,[],[149]),
[iquote('12:Spt:149.1,149.2,149.3')] ).
cnf(267,plain,
( c5_1(u)
| c3_1(u)
| c2_2(u,a334) ),
inference(spt,[],[148]),
[iquote('11:Spt:148.1,148.2,148.3')] ).
cnf(140,plain,
ndr1_0,
inference(mrr,[status(thm)],[27,138,14]),
[iquote('0:MRR:27.0,27.2,138.1,14.0')] ).
cnf(266,plain,
( c5_1(u)
| c3_1(u)
| ndr1_1(u) ),
inference(spt,[],[146]),
[iquote('10:Spt:146.1,146.2,146.3')] ).
cnf(265,plain,
( ~ ndr1_1(u)
| c2_1(u)
| c4_1(u)
| c4_2(u,v)
| c5_2(u,v) ),
inference(spt,[],[170]),
[iquote('9:Spt:170.0,170.2,170.3,170.7,170.8')] ).
cnf(263,plain,
( ~ ndr1_1(u)
| ~ c3_1(u)
| ~ c4_2(u,v)
| ~ c1_2(u,a350)
| c5_2(u,v)
| c1_2(u,v) ),
inference(spt,[],[164]),
[iquote('8:Spt:164.0,164.1,164.2,164.3,164.5,164.6')] ).
cnf(261,plain,
( ~ ndr1_1(u)
| ~ c3_1(u)
| ~ c4_2(u,v)
| ~ c3_2(u,a350)
| c5_2(u,v)
| c1_2(u,v) ),
inference(spt,[],[165]),
[iquote('7:Spt:165.0,165.1,165.2,165.3,165.5,165.6')] ).
cnf(259,plain,
( ~ ndr1_1(u)
| ~ c3_1(u)
| ~ c4_2(u,v)
| c5_2(u,v)
| c1_2(u,v)
| c2_2(u,a350) ),
inference(spt,[],[161]),
[iquote('6:Spt:161.0,161.1,161.2,161.4,161.5,161.6')] ).
cnf(258,plain,
( ~ c2_1(u)
| ~ ndr1_1(u)
| ~ c3_2(u,v)
| ~ c4_2(u,v)
| ~ c1_2(u,a321)
| c2_2(u,v) ),
inference(spt,[],[175]),
[iquote('5:Spt:175.0,175.1,175.3,175.4,175.5,175.6')] ).
cnf(257,plain,
( ~ c2_1(u)
| ~ ndr1_1(u)
| ~ c3_2(u,v)
| ~ c4_2(u,v)
| ~ c2_2(u,a321)
| c2_2(u,v) ),
inference(spt,[],[174]),
[iquote('4:Spt:174.0,174.1,174.3,174.4,174.5,174.6')] ).
cnf(252,plain,
c5_0,
inference(spt,[],[87]),
[iquote('3:Spt:87.2')] ).
cnf(251,plain,
( ~ c2_1(u)
| ~ ndr1_1(u)
| c3_1(u)
| c2_2(u,v)
| c3_2(u,v)
| c4_2(u,v) ),
inference(spt,[],[160]),
[iquote('2:Spt:160.0,160.1,160.3,160.4,160.5,160.6')] ).
cnf(235,plain,
c4_0,
inference(spt,[],[90]),
[iquote('1:Spt:90.2')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.11 % Problem : SYN529+1 : TPTP v8.1.0. Released v2.1.0.
% 0.03/0.12 % Command : run_spass %d %s
% 0.12/0.33 % Computer : n025.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 Jul 12 01:10:32 EDT 2022
% 0.12/0.33 % CPUTime :
% 0.18/0.46
% 0.18/0.46 SPASS V 3.9
% 0.18/0.46 SPASS beiseite: Completion found.
% 0.18/0.46 % SZS status CounterSatisfiable
% 0.18/0.46 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.18/0.46 SPASS derived 80 clauses, backtracked 0 clauses, performed 21 splits and kept 194 clauses.
% 0.18/0.46 SPASS allocated 97921 KBytes.
% 0.18/0.46 SPASS spent 0:00:00.12 on the problem.
% 0.18/0.46 0:00:00.04 for the input.
% 0.18/0.46 0:00:00.04 for the FLOTTER CNF translation.
% 0.18/0.46 0:00:00.00 for inferences.
% 0.18/0.46 0:00:00.00 for the backtracking.
% 0.18/0.46 0:00:00.01 for the reduction.
% 0.18/0.46
% 0.18/0.46
% 0.18/0.46 The saturated set of worked-off clauses is :
% 0.18/0.46 % SZS output start Saturation
% See solution above
%------------------------------------------------------------------------------