%------------------------------------------------------------------------------
% File : E---3.5.1
% Problem : GRP130-3.004 : TPTP v9.3.1. Released v1.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n016.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 12:38:41 PM UTC 2026
% Result : Satisfiable 0.14s 5.87s
% Output : Saturation 0.14s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named c_0_42ERROR: Could not build tree for root c_0_51ERROR: MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(c_0_45,plain,
( ~ group_element(X2)
| ~ group_element(X1)
| product(X1,X2,e_4)
| product(X1,X2,e_3)
| product(X1,X2,e_2)
| product(X1,X2,e_1) ),
c_0_42,
[final] ).
cnf(c_0_46,axiom,
group_element(e_1),
element_1,
[final] ).
cnf(c_0_47,axiom,
group_element(e_2),
element_2,
[final] ).
cnf(c_0_49,plain,
~ equalish(e_2,e_1),
c_0_43,
[final] ).
cnf(c_0_50,plain,
( ~ product(X1,X4,X3)
| ~ product(X1,X2,X3)
| equalish(X2,X4) ),
c_0_44,
[final] ).
cnf(c_0_51,plain,
( ~ group_element(X1)
| product(X1,e_1,e_1)
| product(X1,e_1,e_2)
| product(X1,e_1,e_3)
| product(X1,e_1,e_4) ),
inference(spm,[status(thm)],[c_0_45,c_0_46]),
[final] ).
cnf(c_0_53,plain,
( ~ group_element(X1)
| product(X1,e_2,e_1)
| product(X1,e_2,e_2)
| product(X1,e_2,e_3)
| product(X1,e_2,e_4) ),
inference(spm,[status(thm)],[c_0_45,c_0_47]),
[final] ).
cnf(c_0_54,plain,
( ~ product(X1,X2,X4)
| ~ product(X1,X2,X3)
| equalish(X3,X4) ),
c_0_48,
[final] ).
cnf(c_0_56,axiom,
group_element(e_4),
element_4,
[final] ).
cnf(c_0_58,plain,
( ~ product(X1,e_2,X2)
| ~ product(X1,e_1,X2) ),
inference(spm,[status(thm)],[c_0_49,c_0_50]),
[final] ).
cnf(c_0_60,negated_conjecture,
( ~ product(X1,X3,X4)
| ~ product(X1,X2,X3)
| product(X4,X2,X1) ),
c_0_52,
[final] ).
cnf(c_0_62,plain,
( ~ product(X1,X2,e_2)
| ~ product(X1,X2,e_1) ),
inference(spm,[status(thm)],[c_0_49,c_0_54]),
[final] ).
cnf(c_0_64,plain,
~ equalish(e_2,e_4),
c_0_55,
[final] ).
cnf(c_0_65,plain,
( ~ group_element(X1)
| product(X1,e_4,e_1)
| product(X1,e_4,e_2)
| product(X1,e_4,e_3)
| product(X1,e_4,e_4) ),
inference(spm,[status(thm)],[c_0_45,c_0_56]),
[final] ).
cnf(c_0_66,plain,
~ equalish(e_1,e_4),
c_0_57,
[final] ).
cnf(c_0_69,plain,
( ~ product(X4,X2,X3)
| ~ product(X1,X2,X3)
| equalish(X1,X4) ),
c_0_63,
[final] ).
cnf(c_0_71,plain,
( ~ product(X1,e_2,X2)
| ~ product(X1,e_4,X2) ),
inference(spm,[status(thm)],[c_0_64,c_0_50]),
[final] ).
cnf(c_0_73,plain,
( ~ product(X1,X2,e_1)
| ~ product(X1,X2,e_4) ),
inference(spm,[status(thm)],[c_0_66,c_0_54]),
[final] ).
cnf(c_0_75,plain,
( ~ product(e_1,X1,X2)
| ~ product(e_4,X1,X2) ),
inference(spm,[status(thm)],[c_0_66,c_0_69]),
[final] ).
cnf(c_0_77,plain,
~ equalish(e_3,e_4),
c_0_70,
[final] ).
cnf(c_0_78,axiom,
group_element(e_3),
element_3,
[final] ).
cnf(c_0_82,plain,
~ equalish(e_1,e_3),
c_0_76,
[final] ).
cnf(c_0_83,plain,
( ~ product(X1,e_3,X2)
| ~ product(X1,e_4,X2) ),
inference(spm,[status(thm)],[c_0_77,c_0_50]),
[final] ).
cnf(c_0_84,plain,
( ~ group_element(X1)
| product(X1,e_3,e_1)
| product(X1,e_3,e_2)
| product(X1,e_3,e_3)
| product(X1,e_3,e_4) ),
inference(spm,[status(thm)],[c_0_45,c_0_78]),
[final] ).
cnf(c_0_87,plain,
( ~ product(e_1,X1,X2)
| ~ product(e_3,X1,X2) ),
inference(spm,[status(thm)],[c_0_82,c_0_69]),
[final] ).
cnf(c_0_97,plain,
~ equalish(e_2,e_3),
c_0_93,
[final] ).
cnf(c_0_104,plain,
( ~ product(X1,e_2,X2)
| ~ product(X1,e_3,X2) ),
inference(spm,[status(thm)],[c_0_97,c_0_50]),
[final] ).
cnf(c_0_105,plain,
~ equalish(e_4,e_2),
c_0_98,
[final] ).
cnf(c_0_106,plain,
( ~ next(X1,X4)
| ~ greater(X2,e_0)
| ~ product(X1,e_1,X3)
| ~ cycle(X1,X2)
| equalish(X3,X4) ),
c_0_99,
[final] ).
cnf(c_0_107,plain,
( ~ group_element(X1)
| cycle(X1,e_3)
| cycle(X1,e_2)
| cycle(X1,e_1)
| cycle(X1,e_0) ),
c_0_100,
[final] ).
cnf(c_0_111,plain,
( ~ next(X1,e_2)
| ~ greater(X2,e_0)
| ~ cycle(X1,X2)
| ~ product(X1,e_1,e_4) ),
inference(spm,[status(thm)],[c_0_105,c_0_106]),
[final] ).
cnf(c_0_113,axiom,
greater(e_1,e_0),
e_1_greater_e_0,
[final] ).
cnf(c_0_114,axiom,
next(e_1,e_2),
e_1_then_e_2,
[final] ).
cnf(c_0_122,plain,
( ~ greater(X2,X1)
| ~ product(X1,e_1,X2)
| ~ cycle(X1,e_0) ),
c_0_118,
[final] ).
cnf(c_0_126,axiom,
greater(e_4,e_1),
e_4_greater_e_1,
[final] ).
cnf(c_0_130,plain,
( ~ product(e_2,X1,X2)
| ~ product(e_1,X1,X2) ),
inference(spm,[status(thm)],[c_0_49,c_0_69]),
[final] ).
cnf(c_0_133,axiom,
greater(e_3,e_0),
e_3_greater_e_0,
[final] ).
cnf(c_0_140,axiom,
greater(e_2,e_0),
e_2_greater_e_0,
[final] ).
cnf(c_0_143,plain,
( ~ product(e_3,X1,X2)
| ~ product(e_4,X1,X2) ),
inference(spm,[status(thm)],[c_0_77,c_0_69]),
[final] ).
cnf(c_0_144,plain,
( ~ product(e_2,X1,X2)
| ~ product(e_4,X1,X2) ),
inference(spm,[status(thm)],[c_0_64,c_0_69]),
[final] ).
cnf(c_0_145,plain,
( ~ product(X1,e_1,X2)
| ~ product(X1,e_4,X2) ),
inference(spm,[status(thm)],[c_0_66,c_0_50]),
[final] ).
cnf(c_0_160,plain,
( ~ product(X1,X2,e_2)
| ~ product(X1,X2,e_4) ),
inference(spm,[status(thm)],[c_0_64,c_0_54]),
[final] ).
cnf(c_0_161,plain,
( ~ product(X1,X2,e_3)
| ~ product(X1,X2,e_4) ),
inference(spm,[status(thm)],[c_0_77,c_0_54]),
[final] ).
cnf(c_0_163,plain,
( ~ product(X1,e_1,X2)
| ~ product(X1,e_3,X2) ),
inference(spm,[status(thm)],[c_0_82,c_0_50]),
[final] ).
cnf(c_0_185,plain,
~ equalish(e_1,e_2),
c_0_177,
[final] ).
cnf(c_0_186,plain,
~ equalish(e_3,e_2),
c_0_178,
[final] ).
cnf(c_0_190,plain,
( ~ next(X1,e_2)
| ~ greater(X2,e_0)
| ~ cycle(X1,X2)
| ~ product(X1,e_1,e_1) ),
inference(spm,[status(thm)],[c_0_185,c_0_106]),
[final] ).
cnf(c_0_191,plain,
( ~ next(X1,e_2)
| ~ greater(X2,e_0)
| ~ cycle(X1,X2)
| ~ product(X1,e_1,e_3) ),
inference(spm,[status(thm)],[c_0_186,c_0_106]),
[final] ).
cnf(c_0_202,plain,
( ~ product(e_2,X1,X2)
| ~ product(e_3,X1,X2) ),
inference(spm,[status(thm)],[c_0_97,c_0_69]),
[final] ).
cnf(c_0_204,plain,
( ~ product(X1,X2,e_2)
| ~ product(X1,X2,e_3) ),
inference(spm,[status(thm)],[c_0_97,c_0_54]),
[final] ).
cnf(c_0_210,axiom,
greater(e_3,e_1),
e_3_greater_e_1,
[final] ).
cnf(c_0_212,plain,
( ~ product(e_1,e_4,e_4)
| product(e_1,e_2,e_3)
| product(e_1,e_2,e_2)
| product(e_1,e_1,e_3) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_145,c_0_74]),c_0_71]),
[final] ).
cnf(c_0_261,negated_conjecture,
~ product(e_3,e_2,e_2),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_249,c_0_241]),c_0_104]),c_0_250]),c_0_251]),
[final] ).
cnf(c_0_297,negated_conjecture,
~ product(e_2,e_2,e_3),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_130,c_0_289]),c_0_58]),c_0_161]),c_0_202]),
[final] ).
cnf(c_0_326,negated_conjecture,
product(e_2,e_2,e_2),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_324,c_0_305]),c_0_261]),
[final] ).
cnf(c_0_331,plain,
( ~ next(X4,X5)
| ~ greater(X2,e_0)
| ~ next(X1,X3)
| ~ cycle(X3,X4)
| ~ cycle(X1,X2)
| equalish(X2,X5) ),
c_0_327,
[final] ).
cnf(c_0_336,plain,
( ~ next(X1,X2)
| ~ next(X3,e_2)
| ~ cycle(X2,X3)
| ~ cycle(X1,e_1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_185,c_0_331]),c_0_113])]),
[final] ).
cnf(c_0_338,plain,
( ~ next(X1,X2)
| ~ next(X3,e_2)
| ~ cycle(X2,X3)
| ~ cycle(X1,e_3) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_186,c_0_331]),c_0_133])]),
[final] ).
cnf(c_0_340,negated_conjecture,
~ product(e_3,e_4,e_4),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_145,c_0_332]),c_0_83]),c_0_73]),
[final] ).
cnf(c_0_349,plain,
( cycle(e_3,e_0)
| cycle(e_3,e_1)
| cycle(e_3,e_2)
| cycle(e_3,e_3) ),
inference(spm,[status(thm)],[c_0_107,c_0_78]),
[final] ).
cnf(c_0_350,axiom,
next(e_2,e_3),
e_2_then_e_3,
[final] ).
cnf(c_0_353,negated_conjecture,
( ~ product(e_1,e_1,e_2)
| product(e_4,e_1,e_3)
| product(e_4,e_1,e_4) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_160,c_0_120]),c_0_75]),
[final] ).
cnf(c_0_355,plain,
( ~ greater(X2,X5)
| ~ greater(X3,X1)
| ~ next(X3,X4)
| ~ cycle(X4,X5)
| ~ cycle(X3,e_0)
| ~ cycle(X1,X2) ),
c_0_347,
[final] ).
cnf(c_0_362,axiom,
greater(e_3,e_2),
e_3_greater_e_2,
[final] ).
cnf(c_0_367,plain,
( ~ product(X1,X2,e_1)
| ~ product(X1,X2,e_3) ),
inference(spm,[status(thm)],[c_0_82,c_0_54]),
[final] ).
cnf(c_0_374,plain,
( ~ next(X1,X2)
| ~ next(X3,e_4)
| ~ cycle(X2,X3)
| ~ cycle(X1,e_1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_66,c_0_331]),c_0_113])]),
[final] ).
cnf(c_0_375,plain,
( ~ next(X1,X2)
| ~ next(X3,e_4)
| ~ cycle(X2,X3)
| ~ cycle(X1,e_2) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_64,c_0_331]),c_0_140])]),
[final] ).
cnf(c_0_376,plain,
( ~ next(X1,X2)
| ~ next(X3,e_4)
| ~ cycle(X2,X3)
| ~ cycle(X1,e_3) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_77,c_0_331]),c_0_133])]),
[final] ).
cnf(c_0_381,negated_conjecture,
~ product(e_2,e_1,e_2),
inference(spm,[status(thm)],[c_0_373,c_0_346]),
[final] ).
cnf(c_0_382,plain,
( ~ next(X1,X2)
| ~ next(X3,e_3)
| ~ cycle(X2,X3)
| ~ cycle(X1,e_1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_82,c_0_331]),c_0_113])]),
[final] ).
cnf(c_0_383,plain,
( ~ next(X1,X2)
| ~ next(X3,e_3)
| ~ cycle(X2,X3)
| ~ cycle(X1,e_2) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_97,c_0_331]),c_0_140])]),
[final] ).
cnf(c_0_385,axiom,
next(e_3,e_4),
e_3_then_e_4,
[final] ).
cnf(c_0_387,axiom,
cycle(e_4,e_0),
cycle3,
[final] ).
cnf(c_0_392,plain,
( ~ next(e_2,X1)
| ~ cycle(X1,e_3)
| cycle(e_2,e_0) ),
inference(spm,[status(thm)],[c_0_384,c_0_385]),
[final] ).
cnf(c_0_397,plain,
( ~ next(e_2,X1)
| ~ cycle(X1,e_2)
| cycle(e_2,e_0)
| cycle(e_2,e_3) ),
inference(spm,[status(thm)],[c_0_391,c_0_350]),
[final] ).
cnf(c_0_408,plain,
~ equalish(e_4,e_3),
c_0_403,
[final] ).
cnf(c_0_411,axiom,
greater(e_4,e_2),
e_4_greater_e_2,
[final] ).
cnf(c_0_414,axiom,
greater(e_4,e_3),
e_4_greater_e_3,
[final] ).
cnf(c_0_415,plain,
( ~ next(X1,e_3)
| ~ greater(X2,e_0)
| ~ cycle(X1,X2)
| ~ product(X1,e_1,e_4) ),
inference(spm,[status(thm)],[c_0_408,c_0_106]),
[final] ).
cnf(c_0_422,plain,
( ~ next(X1,X2)
| ~ next(X3,e_1)
| ~ cycle(X2,X3)
| ~ cycle(X1,e_2) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_49,c_0_331]),c_0_140])]),
[final] ).
cnf(c_0_424,plain,
~ equalish(e_3,e_1),
c_0_419,
[final] ).
cnf(c_0_425,negated_conjecture,
product(e_2,e_1,e_3),
inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_415,c_0_420]),c_0_140]),c_0_350])]),c_0_410]),
[final] ).
cnf(c_0_426,plain,
( ~ next(X1,e_4)
| ~ greater(X2,e_0)
| ~ cycle(X1,X2)
| ~ product(X1,e_1,e_1) ),
inference(spm,[status(thm)],[c_0_66,c_0_106]),
[final] ).
cnf(c_0_427,plain,
( ~ next(X1,e_4)
| ~ greater(X2,e_0)
| ~ cycle(X1,X2)
| ~ product(X1,e_1,e_3) ),
inference(spm,[status(thm)],[c_0_77,c_0_106]),
[final] ).
cnf(c_0_428,plain,
( ~ next(X1,e_4)
| ~ greater(X2,e_0)
| ~ cycle(X1,X2)
| ~ product(X1,e_1,e_2) ),
inference(spm,[status(thm)],[c_0_64,c_0_106]),
[final] ).
cnf(c_0_431,axiom,
next(e_0,e_1),
e_0_then_e_1,
[final] ).
cnf(c_0_432,plain,
( ~ next(X1,X2)
| ~ next(X3,e_1)
| ~ cycle(X2,X3)
| ~ cycle(X1,e_3) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_424,c_0_331]),c_0_133])]),
[final] ).
cnf(c_0_440,negated_conjecture,
( ~ next(e_2,X1)
| ~ next(X2,e_1)
| ~ cycle(X1,X2) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_432,c_0_433]),c_0_422]),
[final] ).
cnf(c_0_445,negated_conjecture,
( ~ next(e_2,X1)
| ~ next(X2,e_4)
| ~ cycle(X1,X2) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_376,c_0_433]),c_0_375]),
[final] ).
cnf(c_0_450,negated_conjecture,
~ product(e_3,e_1,e_3),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_161,c_0_444]),c_0_204]),
[final] ).
cnf(c_0_455,negated_conjecture,
product(e_3,e_1,e_4),
inference(csr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_428,c_0_451]),c_0_140]),c_0_385])]),c_0_444]),
[final] ).
cnf(c_0_458,negated_conjecture,
~ product(e_3,e_1,e_2),
inference(spm,[status(thm)],[c_0_160,c_0_455]),
[final] ).
cnf(c_0_461,negated_conjecture,
( cycle(e_1,e_0)
| cycle(e_1,e_3) ),
inference(sr,[status(thm)],[c_0_457,c_0_458]),
[final] ).
cnf(c_0_465,negated_conjecture,
( ~ greater(X1,e_1)
| ~ product(e_1,e_1,X1)
| cycle(e_1,e_3) ),
inference(spm,[status(thm)],[c_0_122,c_0_461]),
[final] ).
cnf(c_0_467,negated_conjecture,
product(e_3,e_2,e_1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_130,c_0_464]),c_0_425])]),
[final] ).
cnf(c_0_473,negated_conjecture,
~ product(e_1,e_1,e_4),
inference(spm,[status(thm)],[c_0_468,c_0_126]),
[final] ).
cnf(c_0_474,negated_conjecture,
~ product(e_1,e_1,e_3),
inference(spm,[status(thm)],[c_0_469,c_0_210]),
[final] ).
cnf(c_0_476,negated_conjecture,
product(e_4,e_1,e_2),
inference(sr,[status(thm)],[c_0_471,c_0_458]),
[final] ).
cnf(c_0_477,negated_conjecture,
( ~ product(e_3,X1,e_2)
| product(e_1,X1,e_3) ),
inference(spm,[status(thm)],[c_0_60,c_0_467]),
[final] ).
cnf(c_0_479,plain,
( product(e_1,e_1,e_1)
| product(e_1,e_1,e_2) ),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[c_0_59,c_0_473]),c_0_474]),
[final] ).
cnf(c_0_481,negated_conjecture,
~ product(e_4,e_2,e_2),
inference(spm,[status(thm)],[c_0_58,c_0_476]),
[final] ).
cnf(c_0_484,negated_conjecture,
product(e_3,e_4,e_2),
inference(spm,[status(thm)],[c_0_478,c_0_455]),
[final] ).
cnf(c_0_486,negated_conjecture,
product(e_4,e_2,e_3),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_480,c_0_476]),c_0_450]),c_0_458]),c_0_481]),
[final] ).
cnf(c_0_487,negated_conjecture,
~ product(e_4,e_3,e_2),
inference(spm,[status(thm)],[c_0_163,c_0_476]),
[final] ).
cnf(c_0_488,negated_conjecture,
~ product(e_3,e_3,e_4),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_482,c_0_370]),c_0_352]),c_0_160]),
[final] ).
cnf(c_0_489,negated_conjecture,
~ product(e_1,e_3,e_3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_483,c_0_484])]),
[final] ).
cnf(c_0_490,plain,
~ product(e_1,e_3,e_1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_75,c_0_485]),c_0_476])]),
[final] ).
cnf(c_0_494,negated_conjecture,
product(e_2,e_3,e_4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_104,c_0_491]),c_0_486])]),
[final] ).
cnf(c_0_497,plain,
product(e_1,e_3,e_2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_130,c_0_493]),c_0_494])]),
[final] ).
cnf(c_0_500,plain,
~ product(e_1,e_2,e_2),
inference(spm,[status(thm)],[c_0_104,c_0_497]),
[final] ).
cnf(c_0_504,negated_conjecture,
( ~ product(e_1,X1,e_3)
| product(e_2,X1,e_1) ),
inference(spm,[status(thm)],[c_0_60,c_0_497]),
[final] ).
cnf(c_0_505,negated_conjecture,
product(e_1,e_2,e_4),
inference(sr,[status(thm)],[c_0_499,c_0_500]),
[final] ).
cnf(c_0_506,plain,
( ~ next(e_4,X1)
| ~ greater(X4,X2)
| ~ greater(e_4,X3)
| ~ cycle(X3,X4)
| ~ cycle(X1,X2) ),
inference(spm,[status(thm)],[c_0_355,c_0_387]),
[final] ).
cnf(c_0_510,negated_conjecture,
( ~ product(e_3,X1,e_2)
| product(e_2,X1,e_1) ),
inference(spm,[status(thm)],[c_0_504,c_0_477]),
[final] ).
cnf(c_0_511,negated_conjecture,
( ~ product(e_1,X1,e_2)
| product(e_4,X1,e_1) ),
inference(spm,[status(thm)],[c_0_60,c_0_505]),
[final] ).
cnf(c_0_513,plain,
( ~ next(e_3,X1)
| ~ next(X2,e_4)
| ~ cycle(X1,X2)
| cycle(e_3,e_0) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_374,c_0_349]),c_0_375]),c_0_376]),
[final] ).
cnf(c_0_515,plain,
( ~ next(e_4,X2)
| ~ greater(X1,X3)
| ~ cycle(X2,X3)
| ~ cycle(e_2,X1) ),
inference(spm,[status(thm)],[c_0_506,c_0_411]),
[final] ).
cnf(c_0_516,negated_conjecture,
cycle(e_2,e_2),
inference(sr,[status(thm)],[c_0_454,c_0_458]),
[final] ).
cnf(c_0_517,negated_conjecture,
~ product(e_3,e_2,e_4),
inference(spm,[status(thm)],[c_0_58,c_0_455]),
[final] ).
cnf(c_0_518,negated_conjecture,
( ~ product(e_2,X1,e_1)
| product(e_3,X1,e_2) ),
inference(spm,[status(thm)],[c_0_60,c_0_425]),
[final] ).
cnf(c_0_523,negated_conjecture,
product(e_2,e_4,e_1),
inference(spm,[status(thm)],[c_0_510,c_0_484]),
[final] ).
cnf(c_0_524,negated_conjecture,
product(e_4,e_3,e_1),
inference(spm,[status(thm)],[c_0_511,c_0_497]),
[final] ).
cnf(c_0_525,plain,
( ~ next(e_4,X2)
| ~ greater(X1,X3)
| ~ cycle(X2,X3)
| ~ cycle(e_1,X1) ),
inference(spm,[status(thm)],[c_0_506,c_0_126]),
[final] ).
cnf(c_0_526,plain,
( ~ cycle(X1,X3)
| ~ cycle(X1,X2)
| equalish(X2,X3) ),
c_0_512,
[final] ).
cnf(c_0_527,plain,
( ~ next(e_3,X1)
| ~ cycle(X1,e_3)
| cycle(e_3,e_0) ),
inference(spm,[status(thm)],[c_0_513,c_0_385]),
[final] ).
cnf(c_0_528,plain,
( ~ next(e_1,X1)
| ~ next(X2,e_4)
| ~ cycle(X1,X2)
| cycle(e_1,e_0) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_374,c_0_112]),c_0_375]),c_0_376]),
[final] ).
cnf(c_0_529,plain,
~ equalish(e_4,e_1),
c_0_514,
[final] ).
cnf(c_0_530,negated_conjecture,
( ~ next(e_4,X1)
| ~ greater(e_2,X2)
| ~ cycle(X1,X2) ),
inference(spm,[status(thm)],[c_0_515,c_0_516]),
[final] ).
cnf(c_0_532,negated_conjecture,
( ~ product(e_3,X1,X2)
| ~ product(e_2,X2,e_1)
| product(e_2,X1,e_3) ),
inference(spm,[status(thm)],[c_0_60,c_0_518]),
[final] ).
cnf(c_0_533,negated_conjecture,
~ product(e_2,e_4,e_3),
inference(spm,[status(thm)],[c_0_145,c_0_425]),
[final] ).
cnf(c_0_536,negated_conjecture,
~ product(e_4,e_4,e_2),
inference(spm,[status(thm)],[c_0_145,c_0_476]),
[final] ).
cnf(c_0_538,negated_conjecture,
( ~ product(e_2,X1,e_4)
| product(e_1,X1,e_2) ),
inference(spm,[status(thm)],[c_0_60,c_0_523]),
[final] ).
cnf(c_0_539,negated_conjecture,
( ~ product(e_4,X1,e_3)
| product(e_1,X1,e_4) ),
inference(spm,[status(thm)],[c_0_60,c_0_524]),
[final] ).
cnf(c_0_540,negated_conjecture,
( ~ next(e_4,X2)
| ~ greater(X1,e_1)
| ~ greater(e_3,X3)
| ~ cycle(X2,X3)
| ~ product(e_1,e_1,X1) ),
inference(spm,[status(thm)],[c_0_525,c_0_465]),
[final] ).
cnf(c_0_541,plain,
( ~ cycle(X1,e_1)
| ~ cycle(X1,e_4) ),
inference(spm,[status(thm)],[c_0_66,c_0_526]),
[final] ).
cnf(c_0_542,plain,
( ~ cycle(X1,e_2)
| ~ cycle(X1,e_4) ),
inference(spm,[status(thm)],[c_0_64,c_0_526]),
[final] ).
cnf(c_0_543,plain,
( ~ cycle(X1,e_3)
| ~ cycle(X1,e_4) ),
inference(spm,[status(thm)],[c_0_77,c_0_526]),
[final] ).
cnf(c_0_544,plain,
( ~ next(X1,e_3)
| ~ greater(X2,e_0)
| ~ cycle(X1,X2)
| ~ product(X1,e_1,e_2) ),
inference(spm,[status(thm)],[c_0_97,c_0_106]),
[final] ).
cnf(c_0_546,plain,
( ~ next(e_1,X1)
| ~ cycle(X1,e_3)
| cycle(e_1,e_0) ),
inference(spm,[status(thm)],[c_0_528,c_0_385]),
[final] ).
cnf(c_0_547,plain,
( ~ next(X1,e_1)
| ~ greater(X2,e_0)
| ~ cycle(X1,X2)
| ~ product(X1,e_1,e_4) ),
inference(spm,[status(thm)],[c_0_529,c_0_106]),
[final] ).
cnf(c_0_548,negated_conjecture,
( ~ next(e_4,e_1)
| cycle(e_1,e_3) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_530,c_0_461]),c_0_140])]),
[final] ).
cnf(c_0_549,negated_conjecture,
( ~ product(e_4,X1,e_2)
| product(e_3,X1,e_4) ),
inference(spm,[status(thm)],[c_0_60,c_0_486]),
[final] ).
cnf(c_0_550,negated_conjecture,
( ~ product(e_2,X1,e_3)
| product(e_4,X1,e_2) ),
inference(spm,[status(thm)],[c_0_60,c_0_494]),
[final] ).
cnf(c_0_551,plain,
( ~ next(e_3,X1)
| ~ next(X2,e_3)
| ~ cycle(X1,X2)
| cycle(e_3,e_3)
| cycle(e_3,e_0) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_382,c_0_349]),c_0_383]),
[final] ).
cnf(c_0_552,plain,
( ~ next(X1,e_1)
| ~ greater(X2,e_0)
| ~ cycle(X1,X2)
| ~ product(X1,e_1,e_2) ),
inference(spm,[status(thm)],[c_0_49,c_0_106]),
[final] ).
cnf(c_0_554,plain,
( ~ next(e_1,X1)
| ~ next(X2,e_2)
| ~ cycle(X1,X2)
| cycle(e_1,e_2)
| cycle(e_1,e_0) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_336,c_0_112]),c_0_338]),
[final] ).
cnf(c_0_555,plain,
( ~ next(e_3,X1)
| ~ next(X2,e_2)
| ~ cycle(X1,X2)
| cycle(e_3,e_2)
| cycle(e_3,e_0) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_336,c_0_349]),c_0_338]),
[final] ).
cnf(c_0_556,plain,
( ~ next(e_4,X2)
| ~ greater(X1,X3)
| ~ cycle(X2,X3)
| ~ cycle(e_3,X1) ),
inference(spm,[status(thm)],[c_0_506,c_0_414]),
[final] ).
cnf(c_0_560,negated_conjecture,
( ~ product(e_3,X1,e_1)
| product(e_4,X1,e_3) ),
inference(spm,[status(thm)],[c_0_60,c_0_455]),
[final] ).
cnf(c_0_561,plain,
( ~ next(X1,e_3)
| ~ greater(X2,e_0)
| ~ cycle(X1,X2)
| ~ product(X1,e_1,e_1) ),
inference(spm,[status(thm)],[c_0_82,c_0_106]),
[final] ).
cnf(c_0_562,plain,
( ~ next(X1,e_1)
| ~ greater(X2,e_0)
| ~ cycle(X1,X2)
| ~ product(X1,e_1,e_3) ),
inference(spm,[status(thm)],[c_0_424,c_0_106]),
[final] ).
cnf(c_0_565,negated_conjecture,
( ~ product(e_2,X1,e_4)
| product(e_4,X1,e_1) ),
inference(spm,[status(thm)],[c_0_511,c_0_538]),
[final] ).
cnf(c_0_566,negated_conjecture,
( ~ product(e_4,X1,e_3)
| ~ product(e_2,X1,e_4) ),
inference(spm,[status(thm)],[c_0_130,c_0_539]),
[final] ).
cnf(c_0_567,negated_conjecture,
( ~ product(e_1,X1,X2)
| ~ product(e_3,X2,e_2)
| product(e_3,X1,e_1) ),
inference(spm,[status(thm)],[c_0_60,c_0_477]),
[final] ).
cnf(c_0_569,axiom,
greater(e_2,e_1),
e_2_greater_e_1,
[final] ).
cnf(c_0_570,negated_conjecture,
( ~ next(e_2,X1)
| ~ next(X2,e_3)
| ~ cycle(X1,X2) ),
inference(spm,[status(thm)],[c_0_383,c_0_516]),
[final] ).
cnf(c_0_571,negated_conjecture,
( ~ next(e_4,e_2)
| ~ greater(X1,e_1)
| ~ product(e_1,e_1,X1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_540,c_0_516]),c_0_362])]),
[final] ).
cnf(c_0_572,negated_conjecture,
( ~ next(e_1,X2)
| ~ next(X3,e_1)
| ~ greater(X1,e_1)
| ~ cycle(X2,X3)
| ~ product(e_1,e_1,X1) ),
inference(spm,[status(thm)],[c_0_432,c_0_465]),
[final] ).
cnf(c_0_573,plain,
( ~ cycle(e_2,e_4)
| cycle(e_2,e_0) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_541,c_0_337]),c_0_542]),c_0_543]),
[final] ).
cnf(c_0_574,negated_conjecture,
( ~ next(e_1,X1)
| ~ greater(X4,X2)
| ~ greater(e_1,X3)
| ~ cycle(X3,X4)
| ~ cycle(X1,X2)
| cycle(e_1,e_3) ),
inference(spm,[status(thm)],[c_0_355,c_0_461]),
[final] ).
cnf(c_0_577,negated_conjecture,
( ~ next(e_3,e_1)
| ~ greater(X1,e_1)
| ~ product(e_1,e_1,X1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_440,c_0_545]),c_0_431]),c_0_350])]),
[final] ).
cnf(c_0_578,negated_conjecture,
( ~ next(e_1,e_1)
| ~ greater(X1,e_1)
| ~ product(e_1,e_1,X1) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_546,c_0_465]),c_0_122]),
[final] ).
cnf(c_0_580,negated_conjecture,
( ~ next(e_4,X1)
| ~ next(e_4,e_1)
| ~ greater(e_3,X2)
| ~ cycle(X1,X2) ),
inference(spm,[status(thm)],[c_0_525,c_0_548]),
[final] ).
cnf(c_0_581,negated_conjecture,
( ~ next(e_1,X1)
| ~ next(X2,e_1)
| ~ next(e_4,e_1)
| ~ cycle(X1,X2) ),
inference(spm,[status(thm)],[c_0_432,c_0_548]),
[final] ).
cnf(c_0_582,negated_conjecture,
( ~ product(e_2,X1,e_3)
| product(e_3,X1,e_4) ),
inference(spm,[status(thm)],[c_0_549,c_0_550]),
[final] ).
cnf(c_0_583,plain,
( ~ cycle(X1,e_2)
| ~ cycle(X1,e_3) ),
inference(spm,[status(thm)],[c_0_97,c_0_526]),
[final] ).
cnf(c_0_587,plain,
( ~ cycle(e_1,e_4)
| cycle(e_1,e_0) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_541,c_0_112]),c_0_542]),c_0_543]),
[final] ).
cnf(c_0_588,plain,
( ~ next(e_3,X1)
| ~ cycle(X1,e_2)
| cycle(e_3,e_0)
| cycle(e_3,e_3) ),
inference(spm,[status(thm)],[c_0_551,c_0_350]),
[final] ).
cnf(c_0_592,plain,
( ~ next(e_1,X1)
| ~ cycle(X1,e_1)
| cycle(e_1,e_0)
| cycle(e_1,e_2) ),
inference(spm,[status(thm)],[c_0_554,c_0_114]),
[final] ).
cnf(c_0_593,plain,
( ~ next(e_3,X1)
| ~ cycle(X1,e_1)
| cycle(e_3,e_0)
| cycle(e_3,e_2) ),
inference(spm,[status(thm)],[c_0_555,c_0_114]),
[final] ).
cnf(c_0_594,plain,
( ~ next(e_4,X1)
| ~ greater(e_1,X2)
| ~ cycle(X1,X2)
| cycle(e_3,e_3)
| cycle(e_3,e_2)
| cycle(e_3,e_0) ),
inference(spm,[status(thm)],[c_0_556,c_0_349]),
[final] ).
cnf(c_0_595,axiom,
greater(e_4,e_0),
e_4_greater_e_0,
[final] ).
cnf(c_0_605,negated_conjecture,
~ product(e_2,e_3,e_3),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_163,c_0_559]),c_0_507]),
[final] ).
cnf(c_0_615,negated_conjecture,
( ~ product(e_4,X1,X2)
| ~ product(e_2,X2,e_4)
| product(e_1,X1,e_4) ),
inference(spm,[status(thm)],[c_0_60,c_0_565]),
[final] ).
cnf(c_0_616,negated_conjecture,
( ~ product(e_1,X1,X2)
| ~ product(e_2,X2,e_4)
| product(e_2,X1,e_1) ),
inference(spm,[status(thm)],[c_0_60,c_0_538]),
[final] ).
cnf(c_0_617,negated_conjecture,
( ~ product(e_3,X1,e_1)
| ~ product(e_2,X1,e_4) ),
inference(spm,[status(thm)],[c_0_566,c_0_560]),
[final] ).
cnf(c_0_618,negated_conjecture,
( ~ product(e_2,X1,e_4)
| ~ product(e_3,X1,e_2) ),
inference(spm,[status(thm)],[c_0_87,c_0_538]),
[final] ).
cnf(c_0_619,negated_conjecture,
( ~ product(e_2,X1,e_4)
| ~ product(e_4,X1,e_2) ),
inference(spm,[status(thm)],[c_0_75,c_0_538]),
[final] ).
cnf(c_0_620,negated_conjecture,
( ~ product(e_4,X1,e_3)
| product(e_3,X1,e_1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_567,c_0_539]),c_0_484])]),
[final] ).
cnf(c_0_621,negated_conjecture,
( ~ product(e_1,X1,X2)
| ~ product(e_4,X2,e_3)
| product(e_4,X1,e_1) ),
inference(spm,[status(thm)],[c_0_60,c_0_539]),
[final] ).
cnf(c_0_622,negated_conjecture,
( ~ product(e_4,X1,e_3)
| ~ product(e_3,X1,e_4) ),
inference(spm,[status(thm)],[c_0_87,c_0_539]),
[final] ).
cnf(c_0_623,negated_conjecture,
( ~ product(e_4,X1,e_3)
| ~ product(e_1,X1,e_2) ),
inference(spm,[status(thm)],[c_0_160,c_0_539]),
[final] ).
cnf(c_0_624,negated_conjecture,
( ~ product(e_1,X1,e_4)
| product(e_3,X1,e_1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_568,c_0_523])]),
[final] ).
cnf(c_0_625,negated_conjecture,
( ~ next(e_4,e_3)
| cycle(e_3,e_3)
| cycle(e_3,e_2)
| cycle(e_3,e_0) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_530,c_0_349]),c_0_569])]),
[final] ).
cnf(c_0_626,negated_conjecture,
( ~ next(e_1,e_3)
| cycle(e_3,e_3)
| cycle(e_3,e_2)
| cycle(e_3,e_0) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_570,c_0_349]),c_0_350])]),
[final] ).
cnf(c_0_627,negated_conjecture,
( ~ product(e_3,X1,e_4)
| product(e_2,X1,e_3) ),
inference(spm,[status(thm)],[c_0_60,c_0_484]),
[final] ).
cnf(c_0_628,negated_conjecture,
( ~ next(e_4,e_2)
| ~ product(e_1,e_1,e_2) ),
inference(spm,[status(thm)],[c_0_571,c_0_569]),
[final] ).
cnf(c_0_629,negated_conjecture,
( ~ greater(X1,e_1)
| ~ cycle(e_2,e_4)
| ~ product(e_1,e_1,X1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_572,c_0_573]),c_0_431]),c_0_114])]),
[final] ).
cnf(c_0_630,negated_conjecture,
( ~ next(e_1,e_4)
| ~ greater(X1,e_1)
| ~ product(e_1,e_1,X1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_572,c_0_387]),c_0_431])]),
[final] ).
cnf(c_0_631,negated_conjecture,
( ~ next(e_1,X2)
| ~ next(X3,e_2)
| ~ greater(X1,e_1)
| ~ cycle(X2,X3)
| ~ product(e_1,e_1,X1) ),
inference(spm,[status(thm)],[c_0_338,c_0_465]),
[final] ).
cnf(c_0_632,negated_conjecture,
( ~ next(e_1,X2)
| ~ next(X3,e_4)
| ~ greater(X1,e_1)
| ~ cycle(X2,X3)
| ~ product(e_1,e_1,X1) ),
inference(spm,[status(thm)],[c_0_376,c_0_465]),
[final] ).
cnf(c_0_633,negated_conjecture,
( ~ next(e_1,X2)
| ~ greater(X1,X3)
| ~ cycle(X2,X3)
| ~ cycle(e_0,X1)
| cycle(e_1,e_3) ),
inference(spm,[status(thm)],[c_0_574,c_0_113]),
[final] ).
cnf(c_0_634,negated_conjecture,
( ~ next(e_1,e_3)
| ~ product(e_1,e_1,e_2) ),
inference(spm,[status(thm)],[c_0_575,c_0_569]),
[final] ).
cnf(c_0_635,negated_conjecture,
( ~ next(e_1,e_4)
| ~ product(e_1,e_1,e_2) ),
inference(spm,[status(thm)],[c_0_576,c_0_569]),
[final] ).
cnf(c_0_636,negated_conjecture,
( ~ next(e_3,e_1)
| ~ product(e_1,e_1,e_2) ),
inference(spm,[status(thm)],[c_0_577,c_0_569]),
[final] ).
cnf(c_0_637,negated_conjecture,
( ~ next(e_1,e_1)
| ~ product(e_1,e_1,e_2) ),
inference(spm,[status(thm)],[c_0_578,c_0_569]),
[final] ).
cnf(c_0_638,plain,
( ~ next(e_3,e_1)
| cycle(e_3,e_0)
| cycle(e_3,e_2)
| cycle(e_3,e_3) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_579,c_0_455])]),
[final] ).
cnf(c_0_639,negated_conjecture,
( ~ next(e_1,e_1)
| cycle(e_3,e_3)
| cycle(e_3,e_2)
| cycle(e_3,e_0) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_440,c_0_349]),c_0_350])]),
[final] ).
cnf(c_0_640,negated_conjecture,
( ~ next(e_4,e_1)
| ~ greater(e_3,e_3) ),
inference(spm,[status(thm)],[c_0_580,c_0_548]),
[final] ).
cnf(c_0_641,negated_conjecture,
( ~ next(e_4,e_2)
| ~ next(e_4,e_1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_580,c_0_516]),c_0_362])]),
[final] ).
cnf(c_0_642,negated_conjecture,
( ~ next(e_4,e_1)
| ~ cycle(e_2,e_4) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_581,c_0_573]),c_0_431]),c_0_114])]),
[final] ).
cnf(c_0_643,negated_conjecture,
( ~ next(e_1,e_4)
| ~ next(e_4,e_1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_581,c_0_387]),c_0_431])]),
[final] ).
cnf(c_0_644,negated_conjecture,
( ~ next(e_1,X1)
| ~ next(X2,e_2)
| ~ next(e_4,e_1)
| ~ cycle(X1,X2) ),
inference(spm,[status(thm)],[c_0_338,c_0_548]),
[final] ).
cnf(c_0_645,negated_conjecture,
( ~ product(e_3,X1,X2)
| ~ product(e_2,X2,e_3)
| product(e_4,X1,e_3) ),
inference(spm,[status(thm)],[c_0_60,c_0_582]),
[final] ).
cnf(c_0_646,negated_conjecture,
( ~ product(e_4,X1,X2)
| ~ product(e_2,X2,e_3)
| product(e_2,X1,e_4) ),
inference(spm,[status(thm)],[c_0_60,c_0_550]),
[final] ).
cnf(c_0_647,negated_conjecture,
( ~ product(e_4,X1,X2)
| ~ product(e_3,X2,e_1)
| product(e_3,X1,e_4) ),
inference(spm,[status(thm)],[c_0_60,c_0_560]),
[final] ).
cnf(c_0_648,negated_conjecture,
( ~ next(e_4,X1)
| ~ greater(e_0,X2)
| ~ cycle(X1,X2)
| cycle(e_1,e_3) ),
inference(spm,[status(thm)],[c_0_525,c_0_461]),
[final] ).
cnf(c_0_649,negated_conjecture,
( ~ next(e_1,e_4)
| cycle(e_3,e_3)
| cycle(e_3,e_2)
| cycle(e_3,e_0) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_445,c_0_349]),c_0_350])]),
[final] ).
cnf(c_0_650,negated_conjecture,
( ~ next(e_1,X1)
| ~ next(X2,e_4)
| ~ next(e_4,e_1)
| ~ cycle(X1,X2) ),
inference(spm,[status(thm)],[c_0_376,c_0_548]),
[final] ).
cnf(c_0_651,negated_conjecture,
( ~ greater(X1,e_1)
| ~ product(e_1,e_1,X1)
| ~ product(e_1,e_1,e_1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_190,c_0_465]),c_0_133]),c_0_114])]),
[final] ).
cnf(c_0_652,negated_conjecture,
( ~ greater(X1,e_1)
| ~ cycle(e_1,e_2)
| ~ product(e_1,e_1,X1) ),
inference(spm,[status(thm)],[c_0_583,c_0_465]),
[final] ).
cnf(c_0_653,negated_conjecture,
( ~ greater(e_0,e_0)
| ~ product(e_1,e_1,e_1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_190,c_0_584]),c_0_133]),c_0_114])]),
[final] ).
cnf(c_0_654,negated_conjecture,
( ~ next(e_4,e_1)
| ~ next(e_3,e_1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_440,c_0_585]),c_0_431]),c_0_350])]),
[final] ).
cnf(c_0_655,negated_conjecture,
( ~ next(e_1,e_1)
| ~ next(e_4,e_1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_530,c_0_586]),c_0_140])]),
[final] ).
cnf(c_0_656,negated_conjecture,
( ~ next(e_4,e_1)
| ~ product(e_1,e_1,e_1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_190,c_0_548]),c_0_133]),c_0_114])]),
[final] ).
cnf(c_0_657,negated_conjecture,
( ~ next(e_4,e_1)
| ~ cycle(e_1,e_2) ),
inference(spm,[status(thm)],[c_0_583,c_0_548]),
[final] ).
cnf(c_0_658,negated_conjecture,
( ~ next(e_4,e_1)
| ~ greater(e_2,e_3) ),
inference(spm,[status(thm)],[c_0_530,c_0_548]),
[final] ).
cnf(c_0_659,negated_conjecture,
( ~ next(e_4,e_1)
| ~ cycle(e_1,e_4) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_530,c_0_587]),c_0_140])]),
[final] ).
cnf(c_0_660,negated_conjecture,
( ~ next(e_4,e_2)
| ~ cycle(e_2,e_4) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_530,c_0_573]),c_0_140])]),
[final] ).
cnf(c_0_661,negated_conjecture,
( ~ next(e_4,e_2)
| ~ greater(e_2,e_2) ),
inference(spm,[status(thm)],[c_0_530,c_0_516]),
[final] ).
cnf(c_0_662,negated_conjecture,
( ~ next(e_3,e_2)
| cycle(e_3,e_3)
| cycle(e_3,e_0) ),
inference(spm,[status(thm)],[c_0_588,c_0_516]),
[final] ).
cnf(c_0_663,negated_conjecture,
( ~ product(e_3,X1,e_2)
| ~ product(e_4,X1,e_3) ),
inference(spm,[status(thm)],[c_0_75,c_0_477]),
[final] ).
cnf(c_0_664,negated_conjecture,
( ~ product(e_3,X1,e_2)
| ~ product(e_2,X1,e_3) ),
inference(spm,[status(thm)],[c_0_130,c_0_477]),
[final] ).
cnf(c_0_665,negated_conjecture,
( ~ product(e_3,X1,e_1)
| ~ product(e_2,X1,e_3) ),
inference(spm,[status(thm)],[c_0_144,c_0_560]),
[final] ).
cnf(c_0_666,negated_conjecture,
( ~ product(e_3,X1,e_1)
| ~ product(e_4,X1,e_2) ),
inference(spm,[status(thm)],[c_0_204,c_0_560]),
[final] ).
cnf(c_0_667,negated_conjecture,
( ~ product(e_4,X1,e_1)
| product(e_2,X1,e_4) ),
inference(spm,[status(thm)],[c_0_60,c_0_476]),
[final] ).
cnf(c_0_668,plain,
( ~ next(e_4,e_1)
| ~ greater(e_0,e_0) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_589,c_0_476])]),
[final] ).
cnf(c_0_669,plain,
( ~ next(e_4,e_3)
| ~ greater(e_0,e_0) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_590,c_0_476])]),
[final] ).
cnf(c_0_670,plain,
( ~ product(e_1,e_3,e_4)
| product(e_1,e_2,e_3)
| product(e_1,e_2,e_2)
| product(e_1,e_1,e_3) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_163,c_0_74]),c_0_104]),
[final] ).
cnf(c_0_671,negated_conjecture,
( ~ product(e_4,e_1,e_4)
| product(e_4,e_3,e_2)
| product(e_4,e_3,e_3) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_75,c_0_591]),c_0_163]),c_0_160]),
[final] ).
cnf(c_0_672,negated_conjecture,
( ~ product(e_1,e_1,e_2)
| product(e_4,e_3,e_2)
| product(e_4,e_3,e_3)
| product(e_4,e_3,e_4) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_160,c_0_591]),c_0_75]),
[final] ).
cnf(c_0_673,plain,
( ~ greater(e_1,e_1)
| cycle(e_1,e_2)
| cycle(e_1,e_3)
| product(e_1,e_1,e_2)
| product(e_1,e_1,e_3)
| product(e_1,e_1,e_4) ),
inference(spm,[status(thm)],[c_0_209,c_0_59]),
[final] ).
cnf(c_0_674,plain,
( ~ next(e_1,e_3)
| cycle(e_1,e_2)
| cycle(e_1,e_0)
| cycle(e_3,e_2)
| cycle(e_3,e_0) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_592,c_0_349]),c_0_546]),
[final] ).
cnf(c_0_675,plain,
( ~ next(e_3,e_1)
| cycle(e_3,e_2)
| cycle(e_3,e_0)
| cycle(e_1,e_2)
| cycle(e_1,e_0) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_593,c_0_112]),c_0_527]),
[final] ).
cnf(c_0_676,plain,
( ~ next(e_4,X1)
| ~ cycle(X1,e_0)
| cycle(e_3,e_0)
| cycle(e_3,e_2)
| cycle(e_3,e_3) ),
inference(spm,[status(thm)],[c_0_594,c_0_113]),
[final] ).
cnf(c_0_677,plain,
( ~ next(e_1,e_1)
| cycle(e_1,e_2)
| cycle(e_1,e_0) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_592,c_0_112]),c_0_546]),
[final] ).
cnf(c_0_678,plain,
( ~ next(e_3,e_3)
| cycle(e_3,e_2)
| cycle(e_3,e_0) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_593,c_0_349]),c_0_527]),
[final] ).
cnf(c_0_679,plain,
( ~ next(e_1,X1)
| ~ greater(X4,X2)
| ~ greater(e_1,X3)
| ~ cycle(X3,X4)
| ~ cycle(X1,X2)
| ~ cycle(e_1,e_4) ),
inference(spm,[status(thm)],[c_0_355,c_0_587]),
[final] ).
cnf(c_0_680,plain,
( ~ next(e_2,X1)
| ~ greater(X4,X2)
| ~ greater(e_2,X3)
| ~ cycle(X3,X4)
| ~ cycle(X1,X2)
| ~ cycle(e_2,e_4) ),
inference(spm,[status(thm)],[c_0_355,c_0_573]),
[final] ).
cnf(c_0_681,plain,
( ~ next(e_4,e_2)
| ~ greater(e_0,e_0)
| ~ product(e_4,e_1,e_4) ),
inference(spm,[status(thm)],[c_0_111,c_0_387]),
[final] ).
cnf(c_0_682,plain,
( ~ next(e_4,X1)
| ~ greater(e_0,X2)
| ~ cycle(X1,X2)
| ~ cycle(e_1,e_4) ),
inference(spm,[status(thm)],[c_0_525,c_0_587]),
[final] ).
cnf(c_0_683,plain,
( ~ next(e_4,X1)
| ~ greater(e_0,X2)
| ~ cycle(X1,X2)
| ~ cycle(e_2,e_4) ),
inference(spm,[status(thm)],[c_0_515,c_0_573]),
[final] ).
cnf(c_0_684,plain,
( ~ next(e_4,X2)
| ~ greater(X1,X3)
| ~ cycle(X2,X3)
| ~ cycle(e_0,X1) ),
inference(spm,[status(thm)],[c_0_506,c_0_595]),
[final] ).
cnf(c_0_685,plain,
( ~ next(X1,X2)
| ~ next(X3,e_1)
| ~ cycle(X2,X3)
| ~ cycle(X1,e_4) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_529,c_0_331]),c_0_595])]),
[final] ).
cnf(c_0_686,plain,
( ~ next(X1,X2)
| ~ next(X3,e_2)
| ~ cycle(X2,X3)
| ~ cycle(X1,e_4) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_105,c_0_331]),c_0_595])]),
[final] ).
cnf(c_0_687,plain,
( ~ next(X1,X2)
| ~ next(X3,e_3)
| ~ cycle(X2,X3)
| ~ cycle(X1,e_4) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_408,c_0_331]),c_0_595])]),
[final] ).
cnf(c_0_688,plain,
( ~ greater(X1,e_1)
| ~ cycle(e_1,e_4)
| ~ product(e_1,e_1,X1) ),
inference(spm,[status(thm)],[c_0_122,c_0_587]),
[final] ).
cnf(c_0_689,plain,
( ~ greater(X1,e_2)
| ~ cycle(e_2,e_4)
| ~ product(e_2,e_1,X1) ),
inference(spm,[status(thm)],[c_0_122,c_0_573]),
[final] ).
cnf(c_0_690,plain,
( ~ greater(X1,e_4)
| ~ product(e_4,e_1,X1) ),
inference(spm,[status(thm)],[c_0_122,c_0_387]),
[final] ).
cnf(c_0_691,plain,
( ~ cycle(X1,e_1)
| ~ cycle(X1,e_3) ),
inference(spm,[status(thm)],[c_0_82,c_0_526]),
[final] ).
cnf(c_0_692,plain,
( ~ cycle(X1,e_2)
| ~ cycle(X1,e_1) ),
inference(spm,[status(thm)],[c_0_49,c_0_526]),
[final] ).
cnf(c_0_693,negated_conjecture,
~ product(e_4,e_1,e_3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_58,c_0_539]),c_0_505])]),
[final] ).
cnf(c_0_694,negated_conjecture,
~ product(e_2,e_4,e_4),
inference(spm,[status(thm)],[c_0_73,c_0_523]),
[final] ).
cnf(c_0_695,negated_conjecture,
~ product(e_1,e_4,e_2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_596,c_0_523])]),
[final] ).
cnf(c_0_696,negated_conjecture,
~ product(e_4,e_4,e_3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_564,c_0_523])]),
[final] ).
cnf(c_0_697,negated_conjecture,
~ product(e_3,e_4,e_3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_597,c_0_523])]),
[final] ).
cnf(c_0_698,negated_conjecture,
~ product(e_4,e_2,e_1),
inference(spm,[status(thm)],[c_0_104,c_0_524]),
[final] ).
cnf(c_0_699,negated_conjecture,
~ product(e_4,e_3,e_3),
inference(spm,[status(thm)],[c_0_367,c_0_524]),
[final] ).
cnf(c_0_700,negated_conjecture,
~ product(e_4,e_3,e_4),
inference(spm,[status(thm)],[c_0_73,c_0_524]),
[final] ).
cnf(c_0_701,plain,
~ product(e_4,e_1,e_1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_75,c_0_598]),c_0_476])]),
[final] ).
cnf(c_0_702,plain,
~ product(e_1,e_4,e_1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_75,c_0_599]),c_0_476])]),
[final] ).
cnf(c_0_703,plain,
~ product(e_1,e_2,e_1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_75,c_0_600]),c_0_476])]),
[final] ).
cnf(c_0_704,negated_conjecture,
~ product(e_4,e_2,e_4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_130,c_0_601]),c_0_326])]),
[final] ).
cnf(c_0_705,negated_conjecture,
~ product(e_3,e_3,e_2),
inference(spm,[status(thm)],[c_0_83,c_0_484]),
[final] ).
cnf(c_0_706,negated_conjecture,
~ product(e_1,e_2,e_3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_602,c_0_484])]),
[final] ).
cnf(c_0_707,negated_conjecture,
~ product(e_2,e_4,e_2),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_603,c_0_472]),c_0_202]),
[final] ).
cnf(c_0_708,negated_conjecture,
~ next(e_4,e_4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_530,c_0_387]),c_0_140])]),
[final] ).
cnf(c_0_709,negated_conjecture,
~ product(e_2,e_3,e_1),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_532,c_0_604]),c_0_605]),
[final] ).
cnf(c_0_710,negated_conjecture,
~ product(e_2,e_2,e_4),
inference(spm,[status(thm)],[c_0_104,c_0_494]),
[final] ).
cnf(c_0_711,negated_conjecture,
~ product(e_2,e_3,e_2),
inference(spm,[status(thm)],[c_0_160,c_0_494]),
[final] ).
cnf(c_0_712,negated_conjecture,
~ product(e_3,e_1,e_1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_606,c_0_560]),c_0_467])]),
[final] ).
cnf(c_0_713,negated_conjecture,
~ product(e_3,e_4,e_1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_607,c_0_560]),c_0_467])]),
[final] ).
cnf(c_0_714,negated_conjecture,
~ product(e_3,e_2,e_3),
inference(spm,[status(thm)],[c_0_367,c_0_467]),
[final] ).
cnf(c_0_715,negated_conjecture,
~ cycle(e_3,e_4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_440,c_0_608]),c_0_431]),c_0_350])]),
[final] ).
cnf(c_0_716,negated_conjecture,
~ product(e_2,e_2,e_1),
inference(spm,[status(thm)],[c_0_261,c_0_518]),
[final] ).
cnf(c_0_717,negated_conjecture,
~ product(e_2,e_1,e_1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_561,c_0_609]),c_0_140]),c_0_350])]),
[final] ).
cnf(c_0_718,negated_conjecture,
~ product(e_2,e_1,e_4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_415,c_0_610]),c_0_140]),c_0_350])]),
[final] ).
cnf(c_0_719,negated_conjecture,
~ next(e_2,e_2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_191,c_0_611]),c_0_425]),c_0_140])]),
[final] ).
cnf(c_0_720,negated_conjecture,
~ next(e_2,e_4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_427,c_0_612]),c_0_425]),c_0_140])]),
[final] ).
cnf(c_0_721,negated_conjecture,
~ next(e_2,e_1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_562,c_0_613]),c_0_425]),c_0_140])]),
[final] ).
cnf(c_0_722,negated_conjecture,
~ product(e_3,e_3,e_1),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_83,c_0_456]),c_0_104]),
[final] ).
cnf(c_0_723,negated_conjecture,
product(e_1,e_4,e_3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_537,c_0_523])]),
[final] ).
cnf(c_0_724,plain,
product(e_4,e_4,e_4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_614,c_0_523])]),
[final] ).
cnf(c_0_725,negated_conjecture,
product(e_3,e_3,e_3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_502,c_0_484])]),
[final] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GRP130-3.004 : TPTP v9.3.1. Released v1.2.0.
% 0.00/0.04 % Command : run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/5.37 % Computer : n016.cluster.edu
% 0.11/5.37 % Model : x86_64 x86_64
% 0.11/5.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/5.37 % Memory : 8046.5625MB
% 0.11/5.37 % OS : Linux 6.8.0-71-generic
% 0.11/5.37 % CPULimit : 300
% 0.11/5.37 % WCLimit : 300
% 0.11/5.37 % DateTime : Sun Sep 20 20:05:58 UTC 2026
% 0.11/5.38 % CPUTime :
% 0.11/5.38 Running run_E /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.14/5.42 Running first-order theorem proving
% 0.14/5.42 Running: /export/starexec/sandbox/solver/bin/eprover --delete-bad-limit=2000000000 --definitional-cnf=24 -s --print-statistics -R --print-version --proof-object --auto-schedule=8 --cpu-limit=300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.14/5.87 % Version: 3.5.1
% 0.14/5.87 % Preprocessing class: FSMSSMSSSSSNFFN.
% 0.14/5.87 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.14/5.87 % Starting G-E--_208_C18_F1_SE_CS_SOS_SP_PS_S5PRR_RG_S04AN with 1500s (5) cores
% 0.14/5.87 % Starting new_bool_3 with 300s (1) cores
% 0.14/5.87 % Starting new_bool_1 with 300s (1) cores
% 0.14/5.87 % Starting sh5l with 300s (1) cores
% 0.14/5.87 % G-E--_208_C18_F1_SE_CS_SOS_SP_PS_S5PRR_RG_S04AN with pid 675460 completed with status 1
% 0.14/5.87 % Result found by G-E--_208_C18_F1_SE_CS_SOS_SP_PS_S5PRR_RG_S04AN
% 0.14/5.87 % Preprocessing class: FSMSSMSSSSSNFFN.
% 0.14/5.87 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.14/5.87 % Starting G-E--_208_C18_F1_SE_CS_SOS_SP_PS_S5PRR_RG_S04AN with 1500s (5) cores
% 0.14/5.87 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 0.14/5.87 % No SInE strategy applied
% 0.14/5.87 % Search class: FGHNF-FFMM00-SFFFFFNN
% 0.14/5.87 % Scheduled 7 strats onto 5 cores with 1500 seconds (1500 total)
% 0.14/5.87 % Starting SubtermCWHack with 136s (1) cores
% 0.14/5.87 % Starting G-E--_208_C18_F1_SE_CS_SOS_SP_PS_S5PRR_RG_S04AN with 151s (1) cores
% 0.14/5.87 % Starting H----_011_C07_F1_PI_AE_OS_R8_SP_S1U with 136s (1) cores
% 0.14/5.87 % Starting G----_425_C05_02_F1_SE_CS_SP_PS_RG_S04AI with 136s (1) cores
% 0.14/5.87 % Starting G-E--_208_B07--C_F1_SE_CS_SP_PS_S5PRR_RG_S04AN with 136s (1) cores
% 0.14/5.87 % G----_425_C05_02_F1_SE_CS_SP_PS_RG_S04AI with pid 675469 completed with status 1
% 0.14/5.87 % Result found by G----_425_C05_02_F1_SE_CS_SP_PS_RG_S04AI
% 0.14/5.87 % Preprocessing class: FSMSSMSSSSSNFFN.
% 0.14/5.87 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 0.14/5.87 % Starting G-E--_208_C18_F1_SE_CS_SOS_SP_PS_S5PRR_RG_S04AN with 1500s (5) cores
% 0.14/5.87 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 0.14/5.87 % No SInE strategy applied
% 0.14/5.87 % Search class: FGHNF-FFMM00-SFFFFFNN
% 0.14/5.87 % Scheduled 7 strats onto 5 cores with 1500 seconds (1500 total)
% 0.14/5.87 % Starting SubtermCWHack with 136s (1) cores
% 0.14/5.87 % Starting G-E--_208_C18_F1_SE_CS_SOS_SP_PS_S5PRR_RG_S04AN with 151s (1) cores
% 0.14/5.87 % Starting H----_011_C07_F1_PI_AE_OS_R8_SP_S1U with 136s (1) cores
% 0.14/5.87 % Starting G----_425_C05_02_F1_SE_CS_SP_PS_RG_S04AI with 136s (1) cores
% 0.14/5.87 % Preprocessing time : 0.001 s
% 0.14/5.87 % Presaturation interreduction done
% 0.14/5.87
% 0.14/5.87 % No proof found!
% 0.14/5.87 % SZS status Satisfiable
% 0.14/5.87 % SZS output start Saturation
% See solution above
% 0.14/5.87 % Parsed axioms : 42
% 0.14/5.87 % Removed by relevancy pruning/SinE : 0
% 0.14/5.87 % Initial clauses : 42
% 0.14/5.87 % Removed in clause preprocessing : 0
% 0.14/5.87 % Initial clauses in saturation : 42
% 0.14/5.87 % Processed clauses : 3446
% 0.14/5.87 % ...of these trivial : 57
% 0.14/5.87 % ...subsumed : 1658
% 0.14/5.87 % ...remaining for further processing : 1731
% 0.14/5.87 % Other redundant clauses eliminated : 0
% 0.14/5.87 % Clauses deleted for lack of memory : 0
% 0.14/5.87 % Backward-subsumed : 1147
% 0.14/5.87 % Backward-rewritten : 191
% 0.14/5.87 % Generated clauses : 8323
% 0.14/5.87 % ...of the previous two non-redundant : 7779
% 0.14/5.87 % ...aggressively subsumed : 0
% 0.14/5.87 % Contextual simplify-reflections : 398
% 0.14/5.87 % Paramodulations : 8256
% 0.14/5.87 % Factorizations : 0
% 0.14/5.87 % NegExts : 0
% 0.14/5.87 % Equation resolutions : 0
% 0.14/5.87 % Disequality decompositions : 0
% 0.14/5.87 % Total rewrite steps : 1344
% 0.14/5.87 % ...of those cached : 1313
% 0.14/5.87 % Propositional unsat checks : 0
% 0.14/5.87 % Propositional check models : 0
% 0.14/5.87 % Propositional check unsatisfiable : 0
% 0.14/5.87 % Propositional clauses : 0
% 0.14/5.87 % Propositional clauses after purity: 0
% 0.14/5.87 % Propositional unsat core size : 0
% 0.14/5.87 % Propositional preprocessing time : 0.000
% 0.14/5.87 % Propositional encoding time : 0.000
% 0.14/5.87 % Propositional solver time : 0.000
% 0.14/5.87 % Success case prop preproc time : 0.000
% 0.14/5.87 % Success case prop encoding time : 0.000
% 0.14/5.87 % Success case prop solver time : 0.000
% 0.14/5.87 % Current number of processed clauses : 284
% 0.14/5.87 % Positive orientable unit clauses : 35
% 0.14/5.87 % Positive unorientable unit clauses: 0
% 0.14/5.87 % Negative unit clauses : 60
% 0.14/5.87 % Non-unit-clauses : 189
% 0.14/5.87 % Current number of unprocessed clauses: 0
% 0.14/5.87 % ...number of literals in the above : 0
% 0.14/5.87 % Current number of archived formulas : 0
% 0.14/5.87 % Current number of archived clauses : 1447
% 0.14/5.87 % Clause-clause subsumption calls (NU) : 223844
% 0.14/5.87 % Rec. Clause-clause subsumption calls : 75470
% 0.14/5.87 % Non-unit clause-clause subsumptions : 2394
% 0.14/5.87 % Unit Clause-clause subsumption calls : 13140
% 0.14/5.87 % Rewrite failures with RHS unbound : 0
% 0.14/5.87 % BW rewrite match attempts : 64
% 0.14/5.87 % BW rewrite match successes : 16
% 0.14/5.87 % Condensation attempts : 0
% 0.14/5.87 % Condensation successes : 0
% 0.14/5.87 % Termbank termtop insertions : 126926
% 0.14/5.87 % Search garbage collected termcells : 98
% 0.14/5.87
% 0.14/5.87 % -------------------------------------------------
% 0.14/5.87 % User time : 0.413 s
% 0.14/5.87 % System time : 0.009 s
% 0.14/5.87 % Total time : 0.422 s
% 0.14/5.87 % Maximum resident set size: 3656 pages
% 0.14/5.87
% 0.14/5.87 % -------------------------------------------------
% 0.14/5.87 % User time : 2.064 s
% 0.14/5.87 % System time : 0.059 s
% 0.14/5.87 % Total time : 2.123 s
% 0.14/5.87 % Maximum resident set size: 4608 pages
% 0.14/5.87 % E exiting
%------------------------------------------------------------------------------