%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : SYN532-1 : TPTP v8.1.0. Released v2.1.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n003.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:36 EDT 2022
% Result : Satisfiable 0.16s 0.40s
% Output : Saturation 0.16s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named 110)
% Comments :
%------------------------------------------------------------------------------
cnf(313,plain,
( ~ c2_1(a412)
| c3_2(a412,a417) ),
inference(res,[status(thm),theory(equality)],[212,303]),
[iquote('11:Res:212.1,303.0')] ).
cnf(303,plain,
( ~ c2_2(a412,u)
| c3_2(a412,u) ),
inference(mrr,[status(thm)],[210,300]),
[iquote('11:MRR:210.1,300.0')] ).
cnf(312,plain,
~ ssskC2,
inference(spt,[],[252]),
[iquote('16:Spt:252.0')] ).
cnf(311,plain,
~ c5_1(a438),
inference(mrr,[status(thm)],[258,308]),
[iquote('15:MRR:258.0,308.0')] ).
cnf(302,plain,
~ c4_1(a412),
inference(mrr,[status(thm)],[42,300]),
[iquote('11:MRR:42.1,300.0')] ).
cnf(310,plain,
c1_1(a438),
inference(mrr,[status(thm)],[256,308]),
[iquote('15:MRR:256.0,308.0')] ).
cnf(309,plain,
c2_1(a438),
inference(mrr,[status(thm)],[257,308]),
[iquote('15:MRR:257.0,308.0')] ).
cnf(308,plain,
ssskC6,
inference(spt,[],[17]),
[iquote('15:Spt:17.0')] ).
cnf(300,plain,
~ ssskC0,
inference(spt,[],[298,43,259]),
[iquote('11:Spt:298.0,43.1,259.0')] ).
cnf(307,plain,
( ~ ssskP1(u)
| ~ ssskP0(u)
| ~ c4_2(u,a430) ),
inference(spt,[],[124]),
[iquote('14:Spt:124.0,124.1,124.2')] ).
cnf(306,plain,
( ~ ssskP1(u)
| ~ ssskP0(u)
| c5_2(u,a430) ),
inference(spt,[],[121]),
[iquote('13:Spt:121.0,121.1,121.3')] ).
cnf(305,plain,
( ~ ssskP1(u)
| ~ ssskP0(u)
| c1_2(u,a430) ),
inference(spt,[],[122]),
[iquote('12:Spt:122.0,122.1,122.3')] ).
cnf(301,plain,
~ c2_1(a412),
inference(spt,[],[298,43]),
[iquote('11:Spt:298.0,43.0')] ).
cnf(277,plain,
( c3_2(a439,a429)
| ssskP1(a439) ),
inference(res,[status(thm),theory(equality)],[211,55]),
[iquote('4:Res:211.1,55.0')] ).
cnf(211,plain,
( c3_2(a439,u)
| c5_2(a439,u) ),
inference(mrr,[status(thm)],[206,207]),
[iquote('4:MRR:206.0,207.0')] ).
cnf(55,axiom,
( ~ c5_2(u,a429)
| ssskP1(u) ),
file('SYN532-1.p',unknown),
[] ).
cnf(54,axiom,
( ~ c4_2(u,a429)
| ssskP1(u) ),
file('SYN532-1.p',unknown),
[] ).
cnf(57,axiom,
( ~ c3_2(u,a428)
| ssskP0(u) ),
file('SYN532-1.p',unknown),
[] ).
cnf(56,axiom,
( ~ c4_2(u,a428)
| ssskP0(u) ),
file('SYN532-1.p',unknown),
[] ).
cnf(38,axiom,
( ssskP1(u)
| c1_2(u,a429) ),
file('SYN532-1.p',unknown),
[] ).
cnf(250,plain,
ssskC1,
inference(spt,[],[249,30,226]),
[iquote('9:Spt:249.0,30.1,226.0')] ).
cnf(255,plain,
ssskC5,
inference(spt,[],[37]),
[iquote('10:Spt:37.0')] ).
cnf(225,plain,
~ c5_2(a425,a427),
inference(mrr,[status(thm)],[58,218]),
[iquote('8:MRR:58.1,218.0')] ).
cnf(224,plain,
~ c3_2(a425,a427),
inference(mrr,[status(thm)],[59,218]),
[iquote('8:MRR:59.1,218.0')] ).
cnf(223,plain,
~ c2_2(a425,a426),
inference(mrr,[status(thm)],[60,218]),
[iquote('8:MRR:60.1,218.0')] ).
cnf(222,plain,
~ c5_2(a425,a426),
inference(mrr,[status(thm)],[61,218]),
[iquote('8:MRR:61.1,218.0')] ).
cnf(221,plain,
c2_2(a425,a427),
inference(mrr,[status(thm)],[39,218]),
[iquote('8:MRR:39.0,218.0')] ).
cnf(220,plain,
c4_2(a425,a426),
inference(mrr,[status(thm)],[40,218]),
[iquote('8:MRR:40.0,218.0')] ).
cnf(219,plain,
~ c3_1(a425),
inference(mrr,[status(thm)],[41,218]),
[iquote('8:MRR:41.1,218.0')] ).
cnf(217,plain,
~ c4_1(a415),
inference(mrr,[status(thm)],[204,214]),
[iquote('7:MRR:204.0,214.0')] ).
cnf(216,plain,
c2_1(a415),
inference(mrr,[status(thm)],[203,214]),
[iquote('7:MRR:203.0,214.0')] ).
cnf(215,plain,
c5_1(a415),
inference(mrr,[status(thm)],[202,214]),
[iquote('7:MRR:202.0,214.0')] ).
cnf(205,plain,
c5_1(a439),
inference(mrr,[status(thm)],[9,201]),
[iquote('3:MRR:9.0,201.0')] ).
cnf(201,plain,
~ c3_0,
inference(mrr,[status(thm)],[104,200]),
[iquote('3:MRR:104.0,200.0')] ).
cnf(218,plain,
~ ssskC3,
inference(spt,[],[27]),
[iquote('8:Spt:27.1')] ).
cnf(103,plain,
ndr1_0,
inference(mrr,[status(thm)],[50,2,102]),
[iquote('0:MRR:50.0,50.1,2.1,102.1')] ).
cnf(214,plain,
c4_0,
inference(spt,[],[13]),
[iquote('7:Spt:13.0')] ).
cnf(213,plain,
( ~ c2_1(u)
| ~ c4_2(u,a417) ),
inference(spt,[],[112]),
[iquote('6:Spt:112.0,112.1')] ).
cnf(212,plain,
( ~ c2_1(u)
| c2_2(u,a417) ),
inference(spt,[],[110]),
[iquote('5:Spt:110.0,110.2')] ).
cnf(207,plain,
ndr1_1(u),
inference(spt,[],[117]),
[iquote('4:Spt:117.1')] ).
cnf(200,plain,
c5_0,
inference(spt,[],[131]),
[iquote('3:Spt:131.1')] ).
cnf(199,plain,
( ~ c1_1(u)
| c2_1(u)
| c5_1(u) ),
inference(spt,[],[125]),
[iquote('2:Spt:125.0,125.3,125.4')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.10 % Problem : SYN532-1 : TPTP v8.1.0. Released v2.1.0.
% 0.06/0.11 % Command : run_spass %d %s
% 0.11/0.30 % Computer : n003.cluster.edu
% 0.11/0.30 % Model : x86_64 x86_64
% 0.11/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.30 % Memory : 8042.1875MB
% 0.11/0.30 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.30 % CPULimit : 300
% 0.11/0.30 % WCLimit : 600
% 0.11/0.30 % DateTime : Tue Jul 12 02:50:45 EDT 2022
% 0.11/0.30 % CPUTime :
% 0.16/0.40
% 0.16/0.40 SPASS V 3.9
% 0.16/0.40 SPASS beiseite: Completion found.
% 0.16/0.40 % SZS status CounterSatisfiable
% 0.16/0.40 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.16/0.40 SPASS derived 105 clauses, backtracked 70 clauses, performed 28 splits and kept 240 clauses.
% 0.16/0.40 SPASS allocated 75781 KBytes.
% 0.16/0.40 SPASS spent 0:00:00.08 on the problem.
% 0.16/0.40 0:00:00.04 for the input.
% 0.16/0.40 0:00:00.00 for the FLOTTER CNF translation.
% 0.16/0.40 0:00:00.00 for inferences.
% 0.16/0.40 0:00:00.00 for the backtracking.
% 0.16/0.40 0:00:00.01 for the reduction.
% 0.16/0.40
% 0.16/0.40
% 0.16/0.40 The saturated set of worked-off clauses is :
% 0.16/0.40 % SZS output start Saturation
% See solution above
%------------------------------------------------------------------------------