%------------------------------------------------------------------------------
% 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 : n022.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 : Satisfiable 0.22s 0.45s
% Output : Saturation 0.22s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named 360)
% Comments :
%------------------------------------------------------------------------------
cnf(365,plain,
( ~ c3_1(u)
| ~ ndr1_1(u)
| ~ c3_2(u,a350)
| c2_1(u)
| c4_1(u)
| c5_2(u,v)
| c1_2(u,v) ),
inference(obv,[status(thm),theory(equality)],[360]),
[iquote('13:Obv:360.6')] ).
cnf(355,plain,
( ~ c3_1(u)
| ~ ndr1_1(u)
| ~ c1_2(u,a350)
| c2_1(u)
| c4_1(u)
| c5_2(u,v)
| c1_2(u,v) ),
inference(obv,[status(thm),theory(equality)],[350]),
[iquote('13:Obv:350.6')] ).
cnf(364,plain,
( ~ c3_1(a318)
| ~ c3_2(a318,a350)
| c5_2(a318,a319)
| c1_2(a318,a319) ),
inference(ssi,[status(thm)],[363,275]),
[iquote('13:SSi:363.1,275.0')] ).
cnf(303,plain,
( ~ c3_1(u)
| ~ ndr1_1(u)
| ~ c4_2(u,v)
| ~ c3_2(u,a350)
| c5_2(u,v)
| c1_2(u,v) ),
inference(mrr,[status(thm)],[166,300]),
[iquote('13:MRR:166.2,300.0')] ).
cnf(359,plain,
( ~ c3_1(a353)
| ~ c2_2(a353,u)
| c2_1(a353)
| c4_1(a353)
| c1_2(a353,u)
| c2_2(a353,a350)
| c3_2(a353,u) ),
inference(ssi,[status(thm)],[358,281]),
[iquote('13:SSi:358.1,281.0')] ).
cnf(349,plain,
( ~ c3_1(u)
| ~ ndr1_1(u)
| c2_1(u)
| c4_1(u)
| c5_2(u,v)
| c1_2(u,v)
| c2_2(u,a350) ),
inference(obv,[status(thm),theory(equality)],[344]),
[iquote('13:Obv:344.5')] ).
cnf(354,plain,
( ~ c3_1(a318)
| ~ c1_2(a318,a350)
| c5_2(a318,a319)
| c1_2(a318,a319) ),
inference(ssi,[status(thm)],[353,275]),
[iquote('13:SSi:353.1,275.0')] ).
cnf(348,plain,
( ~ c3_1(a318)
| c5_2(a318,a319)
| c1_2(a318,a319)
| c2_2(a318,a350) ),
inference(ssi,[status(thm)],[347,275]),
[iquote('13:SSi:347.1,275.0')] ).
cnf(302,plain,
( ~ c3_1(u)
| ~ ndr1_1(u)
| ~ c4_2(u,v)
| ~ c1_2(u,a350)
| c5_2(u,v)
| c1_2(u,v) ),
inference(mrr,[status(thm)],[167,300]),
[iquote('13:MRR:167.2,300.0')] ).
cnf(301,plain,
( ~ c3_1(u)
| ~ ndr1_1(u)
| ~ c4_2(u,v)
| c5_2(u,v)
| c1_2(u,v)
| c2_2(u,a350) ),
inference(mrr,[status(thm)],[164,300]),
[iquote('13:MRR:164.2,300.0')] ).
cnf(333,plain,
( ~ c2_1(a353)
| ~ c1_2(a353,u)
| c3_1(a353)
| c2_2(a353,u)
| c3_2(a353,u) ),
inference(ssi,[status(thm)],[332,281]),
[iquote('9:SSi:332.1,281.0')] ).
cnf(343,plain,
( ~ c1_2(a353,u)
| c5_2(a353,u)
| c3_2(a353,u) ),
inference(spt,[],[331]),
[iquote('17:Spt:331.0,331.3,331.4')] ).
cnf(339,plain,
( c2_1(a353)
| c4_1(a353)
| ssskP0(a353)
| c3_2(a353,a340) ),
inference(mrr,[status(thm)],[338,57]),
[iquote('9:MRR:338.0,57.1')] ).
cnf(285,plain,
( ~ c5_2(a353,u)
| ~ c2_2(a353,u)
| c3_2(a353,u) ),
inference(mrr,[status(thm)],[252,280]),
[iquote('9:MRR:252.0,280.0')] ).
cnf(330,plain,
( ~ c1_2(a353,a334)
| c5_1(a353)
| c3_1(a353)
| c3_2(a353,a334) ),
inference(res,[status(thm),theory(equality)],[272,284]),
[iquote('9:Res:272.2,284.0')] ).
cnf(325,plain,
( c2_1(u)
| c4_1(u)
| c5_2(u,a340)
| ssskP0(u) ),
inference(mrr,[status(thm)],[323,23]),
[iquote('7:MRR:323.0,23.1')] ).
cnf(319,plain,
( ~ c4_2(a326,a327)
| ~ c2_2(a326,a321) ),
inference(mrr,[status(thm)],[318,292]),
[iquote('10:MRR:318.2,292.0')] ).
cnf(317,plain,
( ~ c4_2(a326,a327)
| ~ c1_2(a326,a321) ),
inference(mrr,[status(thm)],[316,292]),
[iquote('10:MRR:316.2,292.0')] ).
cnf(284,plain,
( ~ c4_2(a353,u)
| ~ c1_2(a353,u)
| c3_2(a353,u) ),
inference(mrr,[status(thm)],[251,280]),
[iquote('9:MRR:251.0,280.0')] ).
cnf(272,plain,
( c5_1(u)
| c3_1(u)
| c4_2(u,a334) ),
inference(mrr,[status(thm)],[150,269]),
[iquote('6:MRR:150.0,269.0')] ).
cnf(271,plain,
( c5_1(u)
| c3_1(u)
| c2_2(u,a334) ),
inference(mrr,[status(thm)],[149,269]),
[iquote('6:MRR:149.0,269.0')] ).
cnf(322,plain,
( c2_1(a318)
| c4_1(a318)
| c5_2(a318,a320) ),
inference(ssi,[status(thm)],[320,275]),
[iquote('8:SSi:320.0,275.0')] ).
cnf(315,plain,
( ~ c4_2(a326,a327)
| c5_2(a326,a321) ),
inference(mrr,[status(thm)],[314,292]),
[iquote('10:MRR:314.1,292.0')] ).
cnf(270,plain,
( c5_1(u)
| c3_1(u)
| ndr1_1(u) ),
inference(mrr,[status(thm)],[147,269]),
[iquote('6:MRR:147.0,269.0')] ).
cnf(85,axiom,
( ~ c4_2(u,a340)
| ssskP0(u) ),
file('SYN529-1.p',unknown),
[] ).
cnf(86,axiom,
( ~ c1_2(u,a340)
| ssskP0(u) ),
file('SYN529-1.p',unknown),
[] ).
cnf(57,axiom,
( ssskP0(u)
| c2_2(u,a340) ),
file('SYN529-1.p',unknown),
[] ).
cnf(23,axiom,
( ssskP0(u)
| ndr1_1(u) ),
file('SYN529-1.p',unknown),
[] ).
cnf(298,plain,
~ c5_2(a346,a347),
inference(mrr,[status(thm)],[268,293]),
[iquote('11:MRR:268.0,293.0')] ).
cnf(292,plain,
~ c2_2(a326,a327),
inference(mrr,[status(thm)],[267,286]),
[iquote('10:MRR:267.0,286.0')] ).
cnf(291,plain,
~ c5_2(a326,a327),
inference(mrr,[status(thm)],[266,286]),
[iquote('10:MRR:266.0,286.0')] ).
cnf(279,plain,
~ c4_2(a318,a320),
inference(mrr,[status(thm)],[244,274]),
[iquote('8:MRR:244.0,274.0')] ).
cnf(305,plain,
~ c3_1(a333),
inference(mrr,[status(thm)],[243,304]),
[iquote('14:MRR:243.0,304.0')] ).
cnf(297,plain,
c1_2(a346,a347),
inference(mrr,[status(thm)],[265,293]),
[iquote('11:MRR:265.0,293.0')] ).
cnf(290,plain,
c3_2(a326,a327),
inference(mrr,[status(thm)],[264,286]),
[iquote('10:MRR:264.0,286.0')] ).
cnf(283,plain,
c2_2(a353,a354),
inference(mrr,[status(thm)],[250,280]),
[iquote('9:MRR:250.0,280.0')] ).
cnf(282,plain,
c3_2(a353,a354),
inference(mrr,[status(thm)],[249,280]),
[iquote('9:MRR:249.0,280.0')] ).
cnf(278,plain,
c2_2(a318,a320),
inference(mrr,[status(thm)],[242,274]),
[iquote('8:MRR:242.0,274.0')] ).
cnf(277,plain,
c4_2(a318,a319),
inference(mrr,[status(thm)],[241,274]),
[iquote('8:MRR:241.0,274.0')] ).
cnf(276,plain,
c2_2(a318,a319),
inference(mrr,[status(thm)],[240,274]),
[iquote('8:MRR:240.0,274.0')] ).
cnf(247,plain,
~ c1_1(a343),
inference(mrr,[status(thm)],[39,238]),
[iquote('1:MRR:39.1,238.0')] ).
cnf(296,plain,
ndr1_1(a346),
inference(mrr,[status(thm)],[263,293]),
[iquote('11:MRR:263.0,293.0')] ).
cnf(295,plain,
c4_1(a346),
inference(mrr,[status(thm)],[262,293]),
[iquote('11:MRR:262.0,293.0')] ).
cnf(294,plain,
c3_1(a346),
inference(mrr,[status(thm)],[261,293]),
[iquote('11:MRR:261.0,293.0')] ).
cnf(289,plain,
ndr1_1(a326),
inference(mrr,[status(thm)],[260,286]),
[iquote('10:MRR:260.0,286.0')] ).
cnf(288,plain,
c2_1(a326),
inference(mrr,[status(thm)],[259,286]),
[iquote('10:MRR:259.0,286.0')] ).
cnf(287,plain,
c4_1(a326),
inference(mrr,[status(thm)],[258,286]),
[iquote('10:MRR:258.0,286.0')] ).
cnf(281,plain,
ndr1_1(a353),
inference(mrr,[status(thm)],[248,280]),
[iquote('9:MRR:248.0,280.0')] ).
cnf(275,plain,
ndr1_1(a318),
inference(mrr,[status(thm)],[239,274]),
[iquote('8:MRR:239.0,274.0')] ).
cnf(307,plain,
ssskC3,
inference(spt,[],[30]),
[iquote('16:Spt:30.0')] ).
cnf(269,plain,
~ c1_0,
inference(mrr,[status(thm)],[246,257]),
[iquote('6:MRR:246.1,257.0')] ).
cnf(306,plain,
c2_0,
inference(spt,[],[138]),
[iquote('15:Spt:138.0')] ).
cnf(304,plain,
ssskC4,
inference(spt,[],[29]),
[iquote('14:Spt:29.0')] ).
cnf(245,plain,
c2_1(a343),
inference(mrr,[status(thm)],[12,238]),
[iquote('1:MRR:12.0,238.0')] ).
cnf(300,plain,
ssskC7,
inference(spt,[],[21]),
[iquote('13:Spt:21.0')] ).
cnf(299,plain,
ssskC5,
inference(spt,[],[25]),
[iquote('12:Spt:25.0')] ).
cnf(238,plain,
~ c3_0,
inference(mrr,[status(thm)],[143,237]),
[iquote('1:MRR:143.1,237.0')] ).
cnf(293,plain,
ssskC6,
inference(spt,[],[22]),
[iquote('11:Spt:22.0')] ).
cnf(286,plain,
ssskC2,
inference(spt,[],[31]),
[iquote('10:Spt:31.0')] ).
cnf(280,plain,
ssskC8,
inference(spt,[],[20]),
[iquote('9:Spt:20.0')] ).
cnf(274,plain,
ssskC0,
inference(spt,[],[33]),
[iquote('8:Spt:33.0')] ).
cnf(142,plain,
ndr1_0,
inference(mrr,[status(thm)],[49,9,140]),
[iquote('0:MRR:49.0,49.1,9.1,140.1')] ).
cnf(273,plain,
( ~ ndr1_1(u)
| c2_1(u)
| c4_1(u)
| c4_2(u,v)
| c5_2(u,v) ),
inference(spt,[],[168]),
[iquote('7:Spt:168.1,168.5,168.6,168.7,168.8')] ).
cnf(257,plain,
~ c5_0,
inference(spt,[],[17]),
[iquote('6:Spt:17.0')] ).
cnf(256,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,[],[172]),
[iquote('5:Spt:172.0,172.1,172.2,172.3,172.4,172.6')] ).
cnf(255,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,[],[173]),
[iquote('4:Spt:173.0,173.1,173.2,173.3,173.4,173.6')] ).
cnf(254,plain,
( ~ c2_1(u)
| ~ ndr1_1(u)
| ~ c3_2(u,v)
| ~ c4_2(u,v)
| c2_2(u,v)
| c5_2(u,a321) ),
inference(spt,[],[165]),
[iquote('3:Spt:165.0,165.1,165.2,165.3,165.5,165.6')] ).
cnf(253,plain,
( ~ c2_1(u)
| ~ ndr1_1(u)
| c3_1(u)
| c2_2(u,v)
| c3_2(u,v)
| c4_2(u,v) ),
inference(spt,[],[161]),
[iquote('2:Spt:161.0,161.1,161.3,161.4,161.5,161.6')] ).
cnf(237,plain,
c4_0,
inference(spt,[],[94]),
[iquote('1:Spt:94.2')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.13 % Problem : SYN529-1 : TPTP v8.1.0. Released v2.1.0.
% 0.08/0.14 % Command : run_spass %d %s
% 0.15/0.35 % Computer : n022.cluster.edu
% 0.15/0.35 % Model : x86_64 x86_64
% 0.15/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.35 % Memory : 8042.1875MB
% 0.15/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.36 % CPULimit : 300
% 0.15/0.36 % WCLimit : 600
% 0.15/0.36 % DateTime : Tue Jul 12 08:24:55 EDT 2022
% 0.15/0.36 % CPUTime :
% 0.22/0.45
% 0.22/0.45 SPASS V 3.9
% 0.22/0.45 SPASS beiseite: Completion found.
% 0.22/0.45 % SZS status CounterSatisfiable
% 0.22/0.45 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.22/0.45 SPASS derived 111 clauses, backtracked 0 clauses, performed 17 splits and kept 223 clauses.
% 0.22/0.45 SPASS allocated 75861 KBytes.
% 0.22/0.45 SPASS spent 0:00:00.08 on the problem.
% 0.22/0.45 0:00:00.04 for the input.
% 0.22/0.45 0:00:00.00 for the FLOTTER CNF translation.
% 0.22/0.45 0:00:00.00 for inferences.
% 0.22/0.45 0:00:00.00 for the backtracking.
% 0.22/0.45 0:00:00.02 for the reduction.
% 0.22/0.45
% 0.22/0.45
% 0.22/0.45 The saturated set of worked-off clauses is :
% 0.22/0.45 % SZS output start Saturation
% See solution above
%------------------------------------------------------------------------------