%------------------------------------------------------------------------------
% File : SPASS---3.9
% Problem : SYN432-1 : TPTP v8.1.0. Released v2.1.0.
% Transfm : none
% Format : tptp
% Command : run_spass %d %s
% Computer : n029.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:27 EDT 2022
% Result : Satisfiable 0.52s 0.71s
% Output : Saturation 0.52s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named 136)
% Comments :
%------------------------------------------------------------------------------
cnf(234,plain,
( ~ c2_1(u)
| ~ c3_1(u)
| c1_1(u) ),
inference(spt,[],[136]),
[iquote('2:Spt:136.1,136.2,136.7')] ).
cnf(3926,plain,
( c3_1(u)
| c2_1(u) ),
inference(spt,[],[3925,3905]),
[iquote('35:Spt:3925.0,3905.1,3905.2')] ).
cnf(3919,plain,
~ c2_1(a168),
inference(res,[status(thm),theory(equality)],[3596,3918]),
[iquote('34:Res:3596.1,3918.0')] ).
cnf(3918,plain,
~ c0_1(a168),
inference(mrr,[status(thm)],[121,3915]),
[iquote('34:MRR:121.0,3915.0')] ).
cnf(3917,plain,
~ c1_1(a168),
inference(mrr,[status(thm)],[123,3915]),
[iquote('34:MRR:123.0,3915.0')] ).
cnf(3915,plain,
hskp0,
inference(spt,[],[3913,122,3907]),
[iquote('34:Spt:3913.0,122.0,3907.0')] ).
cnf(3916,plain,
~ c2_1(a168),
inference(spt,[],[3913,122]),
[iquote('34:Spt:3913.0,122.1')] ).
cnf(3904,plain,
( ~ c1_1(u)
| c3_1(u) ),
inference(mrr,[status(thm)],[3879,3903]),
[iquote('32:MRR:3879.1,3903.0')] ).
cnf(3902,plain,
c2_1(a184),
inference(mrr,[status(thm)],[47,3899]),
[iquote('31:MRR:47.0,3899.0')] ).
cnf(3901,plain,
c0_1(a184),
inference(mrr,[status(thm)],[48,3899]),
[iquote('31:MRR:48.0,3899.0')] ).
cnf(3906,plain,
~ hskp5,
inference(spt,[],[109]),
[iquote('33:Spt:109.0')] ).
cnf(3899,plain,
hskp23,
inference(spt,[],[3898,46,3881]),
[iquote('31:Spt:3898.0,46.0,3881.0')] ).
cnf(3903,plain,
~ hskp4,
inference(spt,[],[113]),
[iquote('32:Spt:113.0')] ).
cnf(3900,plain,
c1_1(a184),
inference(spt,[],[3898,46]),
[iquote('31:Spt:3898.0,46.1')] ).
cnf(3880,plain,
~ hskp9,
inference(spt,[],[76]),
[iquote('30:Spt:76.0')] ).
cnf(3877,plain,
~ hskp26,
inference(spt,[],[41]),
[iquote('29:Spt:41.0')] ).
cnf(3872,plain,
c2_1(a170),
inference(mrr,[status(thm)],[66,3869]),
[iquote('25:MRR:66.0,3869.0')] ).
cnf(3876,plain,
~ hskp18,
inference(spt,[],[57]),
[iquote('28:Spt:57.0')] ).
cnf(3871,plain,
c0_1(a170),
inference(mrr,[status(thm)],[65,3869]),
[iquote('25:MRR:65.0,3869.0')] ).
cnf(3874,plain,
~ hskp14,
inference(spt,[],[67]),
[iquote('27:Spt:67.0')] ).
cnf(3869,plain,
hskp15,
inference(spt,[],[3868,64,3845]),
[iquote('25:Spt:3868.0,64.0,3845.0')] ).
cnf(3873,plain,
~ hskp8,
inference(spt,[],[77]),
[iquote('26:Spt:77.0')] ).
cnf(3870,plain,
c1_1(a170),
inference(spt,[],[3868,64]),
[iquote('25:Spt:3868.0,64.1')] ).
cnf(3844,plain,
~ hskp28,
inference(spt,[],[38]),
[iquote('24:Spt:38.0')] ).
cnf(3839,plain,
~ c2_1(a166),
inference(mrr,[status(thm)],[97,3836]),
[iquote('20:MRR:97.0,3836.0')] ).
cnf(3843,plain,
~ hskp27,
inference(spt,[],[40]),
[iquote('23:Spt:40.0')] ).
cnf(3838,plain,
c1_1(a166),
inference(mrr,[status(thm)],[69,3836]),
[iquote('20:MRR:69.0,3836.0')] ).
cnf(3842,plain,
~ hskp7,
inference(spt,[],[78]),
[iquote('22:Spt:78.0')] ).
cnf(3836,plain,
hskp13,
inference(spt,[],[3835,70,3602]),
[iquote('20:Spt:3835.0,70.0,3602.0')] ).
cnf(3840,plain,
~ hskp10,
inference(spt,[],[74]),
[iquote('21:Spt:74.0')] ).
cnf(3837,plain,
c3_1(a166),
inference(spt,[],[3835,70]),
[iquote('20:Spt:3835.0,70.1')] ).
cnf(3596,plain,
( ~ c2_1(u)
| c0_1(u) ),
inference(mrr,[status(thm)],[3580,3595]),
[iquote('17:MRR:3580.1,3595.0')] ).
cnf(3601,plain,
~ hskp6,
inference(spt,[],[80]),
[iquote('19:Spt:80.0')] ).
cnf(3599,plain,
~ hskp19,
inference(spt,[],[56]),
[iquote('18:Spt:56.0')] ).
cnf(3595,plain,
~ hskp29,
inference(spt,[],[35]),
[iquote('17:Spt:35.0')] ).
cnf(3593,plain,
~ hskp1,
inference(spt,[],[83]),
[iquote('16:Spt:83.0')] ).
cnf(3592,plain,
~ hskp12,
inference(spt,[],[71]),
[iquote('15:Spt:71.0')] ).
cnf(3591,plain,
~ hskp16,
inference(spt,[],[62]),
[iquote('14:Spt:62.0')] ).
cnf(3590,plain,
~ hskp20,
inference(spt,[],[54]),
[iquote('13:Spt:54.0')] ).
cnf(3587,plain,
~ c2_1(a163),
inference(ssi,[status(thm)],[3586,3576,3577]),
[iquote('7:SSi:3586.1,3576.0,3577.0')] ).
cnf(3588,plain,
~ hskp3,
inference(spt,[],[81]),
[iquote('12:Spt:81.0')] ).
cnf(3578,plain,
~ c1_1(a163),
inference(mrr,[status(thm)],[100,3575]),
[iquote('7:MRR:100.0,3575.0')] ).
cnf(3585,plain,
~ hskp2,
inference(spt,[],[82]),
[iquote('11:Spt:82.0')] ).
cnf(3577,plain,
c3_1(a163),
inference(mrr,[status(thm)],[73,3575]),
[iquote('7:MRR:73.0,3575.0')] ).
cnf(3583,plain,
~ hskp24,
inference(spt,[],[43]),
[iquote('10:Spt:43.0')] ).
cnf(3575,plain,
hskp11,
inference(spt,[],[3567,72,259]),
[iquote('7:Spt:3567.0,72.0,259.0')] ).
cnf(3582,plain,
~ hskp17,
inference(spt,[],[61]),
[iquote('9:Spt:61.0')] ).
cnf(3579,plain,
~ hskp25,
inference(spt,[],[42]),
[iquote('8:Spt:42.0')] ).
cnf(3576,plain,
c0_1(a163),
inference(spt,[],[3567,72]),
[iquote('7:Spt:3567.0,72.1')] ).
cnf(282,plain,
~ c3_1(a183),
inference(ssi,[status(thm)],[280,256,257]),
[iquote('6:SSi:280.1,256.0,257.0')] ).
cnf(276,plain,
~ c1_1(a183),
inference(ssi,[status(thm)],[275,256,257]),
[iquote('6:SSi:275.0,256.0,257.0')] ).
cnf(273,plain,
~ c2_1(a180),
inference(ssi,[status(thm)],[272,252]),
[iquote('5:SSi:272.1,252.0')] ).
cnf(258,plain,
~ c3_1(a183),
inference(mrr,[status(thm)],[90,255]),
[iquote('6:MRR:90.0,255.0')] ).
cnf(254,plain,
~ c1_1(a180),
inference(mrr,[status(thm)],[91,251]),
[iquote('5:MRR:91.0,251.0')] ).
cnf(253,plain,
~ c2_1(a180),
inference(mrr,[status(thm)],[92,251]),
[iquote('5:MRR:92.0,251.0')] ).
cnf(257,plain,
c2_1(a183),
inference(mrr,[status(thm)],[49,255]),
[iquote('6:MRR:49.0,255.0')] ).
cnf(256,plain,
c0_1(a183),
inference(mrr,[status(thm)],[50,255]),
[iquote('6:MRR:50.0,255.0')] ).
cnf(252,plain,
c3_1(a180),
inference(mrr,[status(thm)],[51,251]),
[iquote('5:MRR:51.0,251.0')] ).
cnf(255,plain,
hskp22,
inference(spt,[],[32]),
[iquote('6:Spt:32.0')] ).
cnf(251,plain,
hskp21,
inference(spt,[],[31]),
[iquote('5:Spt:31.0')] ).
cnf(239,plain,
ndr1_0,
inference(spt,[],[19]),
[iquote('4:Spt:19.1')] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : SYN432-1 : TPTP v8.1.0. Released v2.1.0.
% 0.07/0.13 % Command : run_spass %d %s
% 0.13/0.32 % Computer : n029.cluster.edu
% 0.13/0.32 % Model : x86_64 x86_64
% 0.13/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.32 % Memory : 8042.1875MB
% 0.13/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.32 % CPULimit : 300
% 0.13/0.32 % WCLimit : 600
% 0.13/0.32 % DateTime : Mon Jul 11 14:45:47 EDT 2022
% 0.13/0.32 % CPUTime :
% 0.52/0.71
% 0.52/0.71 SPASS V 3.9
% 0.52/0.71 SPASS beiseite: Completion found.
% 0.52/0.71 % SZS status CounterSatisfiable
% 0.52/0.71 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.52/0.71 SPASS derived 2827 clauses, backtracked 3817 clauses, performed 879 splits and kept 5746 clauses.
% 0.52/0.71 SPASS allocated 77190 KBytes.
% 0.52/0.71 SPASS spent 0:00:00.37 on the problem.
% 0.52/0.71 0:00:00.04 for the input.
% 0.52/0.71 0:00:00.00 for the FLOTTER CNF translation.
% 0.52/0.71 0:00:00.02 for inferences.
% 0.52/0.71 0:00:00.01 for the backtracking.
% 0.52/0.71 0:00:00.23 for the reduction.
% 0.52/0.71
% 0.52/0.71
% 0.52/0.71 The saturated set of worked-off clauses is :
% 0.52/0.71 % SZS output start Saturation
% See solution above
%------------------------------------------------------------------------------