%------------------------------------------------------------------------------
% File : E---3.5.1
% Problem : GRP135-2.005 : TPTP v9.3.1. Released v1.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n018.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:43 PM UTC 2026
% Result : Satisfiable 65.11s 10.01s
% Output : Saturation 65.11s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named c_0_45ERROR: Could not build tree for root c_0_51ERROR: MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(c_0_47,plain,
( ~ group_element(X2)
| ~ group_element(X1)
| product(X1,X2,e_5)
| product(X1,X2,e_4)
| product(X1,X2,e_3)
| product(X1,X2,e_2)
| product(X1,X2,e_1) ),
c_0_45,
[final] ).
cnf(c_0_48,axiom,
group_element(e_1),
element_1,
[final] ).
cnf(c_0_49,plain,
( ~ greater(X2,X3)
| ~ next(X1,X3)
| ~ product(X1,e_1,X2) ),
c_0_46,
[final] ).
cnf(c_0_50,axiom,
greater(e_5,e_3),
e_5_greater_e_3,
[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)
| product(X1,e_1,e_5) ),
inference(spm,[status(thm)],[c_0_47,c_0_48]),
[final] ).
cnf(c_0_52,axiom,
group_element(e_2),
element_2,
[final] ).
cnf(c_0_53,plain,
( ~ next(X1,e_3)
| ~ product(X1,e_1,e_5) ),
inference(spm,[status(thm)],[c_0_49,c_0_50]),
[final] ).
cnf(c_0_54,axiom,
next(e_2,e_3),
e_2_then_e_3,
[final] ).
cnf(c_0_55,axiom,
greater(e_4,e_3),
e_4_greater_e_3,
[final] ).
cnf(c_0_56,axiom,
greater(e_5,e_2),
e_5_greater_e_2,
[final] ).
cnf(c_0_57,axiom,
greater(e_3,e_2),
e_3_greater_e_2,
[final] ).
cnf(c_0_58,axiom,
greater(e_4,e_2),
e_4_greater_e_2,
[final] ).
cnf(c_0_60,plain,
~ product(e_2,e_1,e_5),
inference(spm,[status(thm)],[c_0_53,c_0_54]),
[final] ).
cnf(c_0_61,plain,
( ~ next(X1,e_3)
| ~ product(X1,e_1,e_4) ),
inference(spm,[status(thm)],[c_0_49,c_0_55]),
[final] ).
cnf(c_0_64,plain,
( ~ next(X1,e_2)
| ~ product(X1,e_1,e_5) ),
inference(spm,[status(thm)],[c_0_49,c_0_56]),
[final] ).
cnf(c_0_65,axiom,
next(e_1,e_2),
e_1_then_e_2,
[final] ).
cnf(c_0_66,plain,
( ~ next(X1,e_2)
| ~ product(X1,e_1,e_3) ),
inference(spm,[status(thm)],[c_0_49,c_0_57]),
[final] ).
cnf(c_0_67,plain,
( ~ next(X1,e_2)
| ~ product(X1,e_1,e_4) ),
inference(spm,[status(thm)],[c_0_49,c_0_58]),
[final] ).
cnf(c_0_70,plain,
~ product(e_2,e_1,e_4),
inference(spm,[status(thm)],[c_0_61,c_0_54]),
[final] ).
cnf(c_0_71,plain,
~ equalish(e_2,e_1),
c_0_62,
[final] ).
cnf(c_0_72,plain,
( ~ product(X4,X2,X3)
| ~ product(X1,X2,X3)
| equalish(X1,X4) ),
c_0_63,
[final] ).
cnf(c_0_74,plain,
~ product(e_1,e_1,e_5),
inference(spm,[status(thm)],[c_0_64,c_0_65]),
[final] ).
cnf(c_0_75,plain,
~ product(e_1,e_1,e_3),
inference(spm,[status(thm)],[c_0_66,c_0_65]),
[final] ).
cnf(c_0_76,plain,
~ product(e_1,e_1,e_4),
inference(spm,[status(thm)],[c_0_67,c_0_65]),
[final] ).
cnf(c_0_78,negated_conjecture,
( ~ product(X3,X1,X4)
| ~ product(X1,X2,X3)
| product(X4,X1,X2) ),
c_0_68,
[final] ).
cnf(c_0_80,plain,
( ~ product(e_2,X1,X2)
| ~ product(e_1,X1,X2) ),
inference(spm,[status(thm)],[c_0_71,c_0_72]),
[final] ).
cnf(c_0_81,plain,
( product(e_1,e_1,e_1)
| product(e_1,e_1,e_2) ),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[c_0_73,c_0_74]),c_0_75]),c_0_76]),
[final] ).
cnf(c_0_82,plain,
( ~ product(X1,X2,X4)
| ~ product(X1,X2,X3)
| equalish(X3,X4) ),
c_0_77,
[final] ).
cnf(c_0_86,plain,
( ~ product(X1,X2,e_2)
| ~ product(X1,X2,e_1) ),
inference(spm,[status(thm)],[c_0_71,c_0_82]),
[final] ).
cnf(c_0_88,plain,
~ equalish(e_1,e_3),
c_0_85,
[final] ).
cnf(c_0_90,plain,
( ~ product(X1,X2,e_1)
| ~ product(X1,X2,e_3) ),
inference(spm,[status(thm)],[c_0_88,c_0_82]),
[final] ).
cnf(c_0_92,negated_conjecture,
~ product(e_2,e_1,e_1),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_89,c_0_84]),c_0_90]),
[final] ).
cnf(c_0_93,plain,
( ~ product(X1,X4,X3)
| ~ product(X1,X2,X3)
| equalish(X2,X4) ),
c_0_91,
[final] ).
cnf(c_0_94,plain,
( ~ product(e_1,X1,X2)
| ~ product(e_3,X1,X2) ),
inference(spm,[status(thm)],[c_0_88,c_0_72]),
[final] ).
cnf(c_0_97,plain,
( ~ product(X1,e_2,X2)
| ~ product(X1,e_1,X2) ),
inference(spm,[status(thm)],[c_0_71,c_0_93]),
[final] ).
cnf(c_0_99,plain,
~ equalish(e_1,e_5),
c_0_95,
[final] ).
cnf(c_0_101,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)
| product(X1,e_2,e_5) ),
inference(spm,[status(thm)],[c_0_47,c_0_52]),
[final] ).
cnf(c_0_102,axiom,
group_element(e_3),
element_3,
[final] ).
cnf(c_0_107,axiom,
group_element(e_5),
element_5,
[final] ).
cnf(c_0_108,plain,
( ~ product(X1,e_1,X2)
| ~ product(X1,e_5,X2) ),
inference(spm,[status(thm)],[c_0_99,c_0_93]),
[final] ).
cnf(c_0_109,plain,
~ equalish(e_1,e_4),
c_0_100,
[final] ).
cnf(c_0_112,plain,
~ equalish(e_2,e_5),
c_0_106,
[final] ).
cnf(c_0_113,plain,
( ~ group_element(X1)
| product(X1,e_5,e_1)
| product(X1,e_5,e_2)
| product(X1,e_5,e_3)
| product(X1,e_5,e_4)
| product(X1,e_5,e_5) ),
inference(spm,[status(thm)],[c_0_47,c_0_107]),
[final] ).
cnf(c_0_118,axiom,
group_element(e_4),
element_4,
[final] ).
cnf(c_0_119,plain,
( ~ product(X1,e_1,X2)
| ~ product(X1,e_4,X2) ),
inference(spm,[status(thm)],[c_0_109,c_0_93]),
[final] ).
cnf(c_0_121,plain,
~ product(e_1,e_2,e_1),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_80,c_0_104]),c_0_111]),
[final] ).
cnf(c_0_123,plain,
( ~ product(X1,e_2,X2)
| ~ product(X1,e_5,X2) ),
inference(spm,[status(thm)],[c_0_112,c_0_93]),
[final] ).
cnf(c_0_127,plain,
~ equalish(e_2,e_3),
c_0_116,
[final] ).
cnf(c_0_128,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)
| product(X1,e_3,e_5) ),
inference(spm,[status(thm)],[c_0_47,c_0_102]),
[final] ).
cnf(c_0_129,plain,
( ~ product(X1,e_1,X2)
| ~ product(X1,e_3,X2) ),
inference(spm,[status(thm)],[c_0_88,c_0_93]),
[final] ).
cnf(c_0_130,plain,
~ equalish(e_2,e_4),
c_0_117,
[final] ).
cnf(c_0_131,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)
| product(X1,e_4,e_5) ),
inference(spm,[status(thm)],[c_0_47,c_0_118]),
[final] ).
cnf(c_0_135,plain,
~ equalish(e_3,e_5),
c_0_122,
[final] ).
cnf(c_0_138,plain,
( ~ product(X1,e_2,X2)
| ~ product(X1,e_3,X2) ),
inference(spm,[status(thm)],[c_0_127,c_0_93]),
[final] ).
cnf(c_0_142,plain,
( ~ product(X1,e_2,X2)
| ~ product(X1,e_4,X2) ),
inference(spm,[status(thm)],[c_0_130,c_0_93]),
[final] ).
cnf(c_0_145,plain,
~ equalish(e_4,e_5),
c_0_133,
[final] ).
cnf(c_0_147,plain,
( ~ product(X1,e_3,X2)
| ~ product(X1,e_5,X2) ),
inference(spm,[status(thm)],[c_0_135,c_0_93]),
[final] ).
cnf(c_0_151,plain,
~ equalish(e_3,e_4),
c_0_141,
[final] ).
cnf(c_0_154,plain,
( ~ product(X1,e_4,X2)
| ~ product(X1,e_5,X2) ),
inference(spm,[status(thm)],[c_0_145,c_0_93]),
[final] ).
cnf(c_0_155,plain,
( ~ product(e_2,X1,X2)
| ~ product(e_5,X1,X2) ),
inference(spm,[status(thm)],[c_0_112,c_0_72]),
[final] ).
cnf(c_0_157,plain,
( ~ product(e_2,X1,X2)
| ~ product(e_3,X1,X2) ),
inference(spm,[status(thm)],[c_0_127,c_0_72]),
[final] ).
cnf(c_0_160,plain,
( ~ product(X1,e_3,X2)
| ~ product(X1,e_4,X2) ),
inference(spm,[status(thm)],[c_0_151,c_0_93]),
[final] ).
cnf(c_0_175,plain,
( ~ product(e_2,X1,X2)
| ~ product(e_4,X1,X2) ),
inference(spm,[status(thm)],[c_0_130,c_0_72]),
[final] ).
cnf(c_0_177,plain,
( ~ product(X1,X2,e_1)
| ~ product(X1,X2,e_4) ),
inference(spm,[status(thm)],[c_0_109,c_0_82]),
[final] ).
cnf(c_0_178,negated_conjecture,
( ~ product(e_1,X1,e_1)
| product(e_1,e_1,X1)
| product(e_1,e_1,e_2) ),
inference(spm,[status(thm)],[c_0_78,c_0_81]),
[final] ).
cnf(c_0_187,plain,
( ~ product(e_3,X1,X2)
| ~ product(e_5,X1,X2) ),
inference(spm,[status(thm)],[c_0_135,c_0_72]),
[final] ).
cnf(c_0_214,plain,
( ~ product(e_1,X1,X2)
| ~ product(e_4,X1,X2) ),
inference(spm,[status(thm)],[c_0_109,c_0_72]),
[final] ).
cnf(c_0_224,plain,
( ~ product(e_3,X1,X2)
| ~ product(e_4,X1,X2) ),
inference(spm,[status(thm)],[c_0_151,c_0_72]),
[final] ).
cnf(c_0_229,axiom,
greater(e_5,e_4),
e_5_greater_e_4,
[final] ).
cnf(c_0_231,plain,
( ~ product(e_1,X1,X2)
| ~ product(e_5,X1,X2) ),
inference(spm,[status(thm)],[c_0_99,c_0_72]),
[final] ).
cnf(c_0_236,plain,
( ~ next(X1,e_4)
| ~ product(X1,e_1,e_5) ),
inference(spm,[status(thm)],[c_0_49,c_0_229]),
[final] ).
cnf(c_0_237,axiom,
next(e_3,e_4),
e_3_then_e_4,
[final] ).
cnf(c_0_242,plain,
~ product(e_4,e_1,e_1),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_80,c_0_223]),c_0_232]),
[final] ).
cnf(c_0_244,plain,
~ product(e_3,e_1,e_5),
inference(spm,[status(thm)],[c_0_236,c_0_237]),
[final] ).
cnf(c_0_257,plain,
~ product(e_5,e_1,e_1),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_80,c_0_239]),c_0_247]),
[final] ).
cnf(c_0_264,plain,
( ~ product(e_4,X1,X2)
| ~ product(e_5,X1,X2) ),
inference(spm,[status(thm)],[c_0_145,c_0_72]),
[final] ).
cnf(c_0_277,plain,
( ~ product(X1,X2,e_1)
| ~ product(X1,X2,e_5) ),
inference(spm,[status(thm)],[c_0_99,c_0_82]),
[final] ).
cnf(c_0_319,plain,
( ~ product(X1,X2,e_2)
| ~ product(X1,X2,e_3) ),
inference(spm,[status(thm)],[c_0_127,c_0_82]),
[final] ).
cnf(c_0_320,plain,
( ~ product(X1,X2,e_2)
| ~ product(X1,X2,e_4) ),
inference(spm,[status(thm)],[c_0_130,c_0_82]),
[final] ).
cnf(c_0_343,plain,
( ~ product(X1,X2,e_3)
| ~ product(X1,X2,e_4) ),
inference(spm,[status(thm)],[c_0_151,c_0_82]),
[final] ).
cnf(c_0_377,plain,
( ~ product(X1,X2,e_4)
| ~ product(X1,X2,e_5) ),
inference(spm,[status(thm)],[c_0_145,c_0_82]),
[final] ).
cnf(c_0_378,plain,
( ~ product(X1,X2,e_2)
| ~ product(X1,X2,e_5) ),
inference(spm,[status(thm)],[c_0_112,c_0_82]),
[final] ).
cnf(c_0_396,negated_conjecture,
~ product(e_2,e_2,e_1),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_155,c_0_393]),c_0_90]),c_0_86]),c_0_177]),
[final] ).
cnf(c_0_434,negated_conjecture,
~ product(e_2,e_3,e_2),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_129,c_0_417]),c_0_138]),
[final] ).
cnf(c_0_440,negated_conjecture,
~ product(e_4,e_2,e_2),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_214,c_0_433]),c_0_402]),
[final] ).
cnf(c_0_446,negated_conjecture,
~ product(e_2,e_4,e_2),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_119,c_0_417]),c_0_142]),
[final] ).
cnf(c_0_490,negated_conjecture,
~ product(e_5,e_2,e_2),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_231,c_0_488]),c_0_155]),
[final] ).
cnf(c_0_507,plain,
( ~ product(X1,X2,e_3)
| ~ product(X1,X2,e_5) ),
inference(spm,[status(thm)],[c_0_135,c_0_82]),
[final] ).
cnf(c_0_508,negated_conjecture,
~ product(e_3,e_2,e_2),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_94,c_0_488]),c_0_157]),
[final] ).
cnf(c_0_525,negated_conjecture,
~ product(e_2,e_2,e_5),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_515,c_0_516]),c_0_377]),c_0_378]),
[final] ).
cnf(c_0_600,negated_conjecture,
~ product(e_2,e_5,e_2),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_108,c_0_417]),c_0_123]),
[final] ).
cnf(c_0_626,negated_conjecture,
~ product(e_2,e_4,e_3),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_90,c_0_620]),c_0_142]),c_0_144]),
[final] ).
cnf(c_0_633,negated_conjecture,
~ product(e_2,e_2,e_4),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_378,c_0_629]),c_0_630]),
[final] ).
cnf(c_0_747,negated_conjecture,
product(e_2,e_2,e_2),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_160,c_0_742]),c_0_689]),
[final] ).
cnf(c_0_754,plain,
~ product(e_2,e_5,e_3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_126,c_0_747])]),
[final] ).
cnf(c_0_779,negated_conjecture,
~ product(e_2,e_3,e_3),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_773,c_0_668]),c_0_762]),
[final] ).
cnf(c_0_799,negated_conjecture,
~ product(e_3,e_1,e_2),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_86,c_0_793]),c_0_320]),c_0_319]),
[final] ).
cnf(c_0_1101,negated_conjecture,
~ product(e_2,e_4,e_4),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_154,c_0_1097]),c_0_160]),
[final] ).
cnf(c_0_1198,negated_conjecture,
product(e_2,e_5,e_4),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_187,c_0_1190]),c_0_1172]),
[final] ).
cnf(c_0_1239,negated_conjecture,
~ product(e_2,e_3,e_4),
inference(spm,[status(thm)],[c_0_147,c_0_1198]),
[final] ).
cnf(c_0_1240,negated_conjecture,
product(e_2,e_4,e_5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_97,c_0_1234]),c_0_747])]),
[final] ).
cnf(c_0_1247,negated_conjecture,
~ product(e_2,e_3,e_5),
inference(spm,[status(thm)],[c_0_160,c_0_1240]),
[final] ).
cnf(c_0_1298,negated_conjecture,
~ product(e_3,e_5,e_4),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_377,c_0_1117]),c_0_157]),c_0_343]),c_0_320]),
[final] ).
cnf(c_0_1301,plain,
product(e_2,e_3,e_1),
inference(sr,[status(thm)],[c_0_1290,c_0_1247]),
[final] ).
cnf(c_0_1304,negated_conjecture,
~ product(e_4,e_1,e_2),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_378,c_0_1294]),c_0_175]),
[final] ).
cnf(c_0_1305,negated_conjecture,
~ product(e_2,e_4,e_1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_97,c_0_1295]),c_0_747])]),
[final] ).
cnf(c_0_1310,negated_conjecture,
~ product(e_3,e_5,e_3),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_108,c_0_1299]),c_0_147]),
[final] ).
cnf(c_0_1312,negated_conjecture,
( ~ product(e_3,X1,e_2)
| product(e_1,e_3,X1) ),
inference(spm,[status(thm)],[c_0_78,c_0_1301]),
[final] ).
cnf(c_0_1318,negated_conjecture,
( ~ product(e_3,X1,e_2)
| ~ product(e_3,X2,e_1)
| product(X1,e_3,X2) ),
inference(spm,[status(thm)],[c_0_78,c_0_1312]),
[final] ).
cnf(c_0_1340,negated_conjecture,
( ~ product(e_3,X1,e_2)
| ~ product(e_5,e_3,X1) ),
inference(spm,[status(thm)],[c_0_231,c_0_1312]),
[final] ).
cnf(c_0_1343,negated_conjecture,
~ product(e_4,e_1,e_3),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_507,c_0_1338]),c_0_224]),
[final] ).
cnf(c_0_1345,negated_conjecture,
~ product(e_5,e_3,e_3),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_160,c_0_1339]),c_0_1340]),
[final] ).
cnf(c_0_1346,negated_conjecture,
~ product(e_5,e_3,e_2),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_320,c_0_1328]),c_0_187]),
[final] ).
cnf(c_0_1371,negated_conjecture,
~ product(e_3,e_3,e_1),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_160,c_0_1319]),c_0_86]),
[final] ).
cnf(c_0_1407,negated_conjecture,
~ product(e_3,e_4,e_2),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_1397,c_0_1339]),c_0_160]),
[final] ).
cnf(c_0_1408,negated_conjecture,
~ product(e_3,e_4,e_3),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_187,c_0_1349]),c_0_119]),
[final] ).
cnf(c_0_1410,negated_conjecture,
( ~ product(e_4,X1,e_2)
| product(e_5,e_4,X1) ),
inference(spm,[status(thm)],[c_0_78,c_0_1240]),
[final] ).
cnf(c_0_1415,negated_conjecture,
~ product(e_3,e_3,e_5),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_1403,c_0_1404]),c_0_147]),
[final] ).
cnf(c_0_1417,negated_conjecture,
( ~ product(e_4,X1,e_2)
| ~ product(e_5,e_2,X1) ),
inference(spm,[status(thm)],[c_0_142,c_0_1410]),
[final] ).
cnf(c_0_1430,negated_conjecture,
( ~ product(e_5,X1,e_2)
| product(e_4,e_5,X1) ),
inference(spm,[status(thm)],[c_0_78,c_0_1198]),
[final] ).
cnf(c_0_1434,negated_conjecture,
( ~ product(e_3,X1,e_2)
| ~ product(e_4,e_3,X1) ),
inference(spm,[status(thm)],[c_0_214,c_0_1312]),
[final] ).
cnf(c_0_1440,negated_conjecture,
~ product(e_3,e_5,e_5),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_1435,c_0_1436]),c_0_123]),
[final] ).
cnf(c_0_1448,negated_conjecture,
product(e_3,e_5,e_2),
inference(sr,[status(thm)],[c_0_1422,c_0_1440]),
[final] ).
cnf(c_0_1458,negated_conjecture,
product(e_2,e_1,e_3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1437,c_0_1448])]),
[final] ).
cnf(c_0_1463,negated_conjecture,
product(e_3,e_3,e_3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1451,c_0_1448])]),
[final] ).
cnf(c_0_1469,negated_conjecture,
~ product(e_3,e_4,e_5),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_154,c_0_1422]),c_0_1455]),
[final] ).
cnf(c_0_1470,negated_conjecture,
~ product(e_3,e_4,e_4),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_224,c_0_1456]),c_0_142]),
[final] ).
cnf(c_0_1473,negated_conjecture,
product(e_5,e_1,e_2),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1442,c_0_1458])]),c_0_1239]),c_0_1247]),c_0_1304]),
[final] ).
cnf(c_0_1475,negated_conjecture,
~ product(e_1,e_3,e_2),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_160,c_0_1459]),c_0_94]),
[final] ).
cnf(c_0_1476,negated_conjecture,
~ product(e_1,e_3,e_3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1419,c_0_1448])]),
[final] ).
cnf(c_0_1477,negated_conjecture,
~ product(e_1,e_3,e_4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1460,c_0_1448])]),
[final] ).
cnf(c_0_1480,negated_conjecture,
~ product(e_2,e_1,e_2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1462,c_0_1463])]),
[final] ).
cnf(c_0_1493,negated_conjecture,
product(e_4,e_5,e_1),
inference(spm,[status(thm)],[c_0_1430,c_0_1473]),
[final] ).
cnf(c_0_1494,negated_conjecture,
product(e_1,e_3,e_5),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1474,c_0_1473])]),c_0_1475]),c_0_1476]),c_0_1477]),
[final] ).
cnf(c_0_1496,negated_conjecture,
product(e_1,e_2,e_4),
inference(sr,[status(thm)],[c_0_1479,c_0_1480]),
[final] ).
cnf(c_0_1497,negated_conjecture,
product(e_5,e_2,e_1),
inference(sr,[status(thm)],[c_0_1481,c_0_1480]),
[final] ).
cnf(c_0_1500,negated_conjecture,
~ product(e_5,e_5,e_4),
inference(csr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1483,c_0_1484]),c_0_60]),c_0_1485]),
[final] ).
cnf(c_0_1510,negated_conjecture,
( ~ product(e_5,X1,e_4)
| product(e_1,e_5,X1) ),
inference(spm,[status(thm)],[c_0_78,c_0_1493]),
[final] ).
cnf(c_0_1511,negated_conjecture,
( ~ product(e_3,X1,e_1)
| product(e_5,e_3,X1) ),
inference(spm,[status(thm)],[c_0_78,c_0_1494]),
[final] ).
cnf(c_0_1512,negated_conjecture,
product(e_3,e_2,e_5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1425,c_0_1448])]),
[final] ).
cnf(c_0_1513,negated_conjecture,
( ~ product(e_3,X1,e_5)
| product(e_4,e_3,X1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1424,c_0_1448])]),
[final] ).
cnf(c_0_1516,negated_conjecture,
( ~ product(e_2,X1,e_1)
| product(e_4,e_2,X1) ),
inference(spm,[status(thm)],[c_0_78,c_0_1496]),
[final] ).
cnf(c_0_1517,negated_conjecture,
( ~ product(e_2,X1,e_5)
| product(e_1,e_2,X1) ),
inference(spm,[status(thm)],[c_0_78,c_0_1497]),
[final] ).
cnf(c_0_1518,negated_conjecture,
( ~ product(e_4,X1,e_3)
| product(e_1,e_4,X1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1495,c_0_1463])]),
[final] ).
cnf(c_0_1524,negated_conjecture,
~ product(e_3,e_3,e_2),
inference(spm,[status(thm)],[c_0_147,c_0_1448]),
[final] ).
cnf(c_0_1537,negated_conjecture,
( ~ product(e_5,X1,e_4)
| ~ product(e_1,e_4,X1) ),
inference(spm,[status(thm)],[c_0_154,c_0_1510]),
[final] ).
cnf(c_0_1538,negated_conjecture,
( ~ product(e_5,X1,e_4)
| ~ product(e_1,e_3,X1) ),
inference(spm,[status(thm)],[c_0_147,c_0_1510]),
[final] ).
cnf(c_0_1539,negated_conjecture,
( ~ product(e_5,X1,e_4)
| ~ product(e_1,e_2,X1) ),
inference(spm,[status(thm)],[c_0_123,c_0_1510]),
[final] ).
cnf(c_0_1540,negated_conjecture,
( ~ product(e_3,X1,e_1)
| ~ product(e_5,e_2,X1) ),
inference(spm,[status(thm)],[c_0_138,c_0_1511]),
[final] ).
cnf(c_0_1541,negated_conjecture,
( ~ product(e_2,X1,e_3)
| product(e_5,e_2,X1) ),
inference(spm,[status(thm)],[c_0_78,c_0_1512]),
[final] ).
cnf(c_0_1542,negated_conjecture,
( ~ product(e_3,X1,e_5)
| ~ product(e_4,e_2,X1) ),
inference(spm,[status(thm)],[c_0_138,c_0_1513]),
[final] ).
cnf(c_0_1543,negated_conjecture,
( ~ product(e_4,X1,e_3)
| ~ product(e_1,e_2,X1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1514,c_0_1463])]),
[final] ).
cnf(c_0_1544,negated_conjecture,
( ~ product(e_3,X1,e_2)
| ~ product(e_1,e_2,X1) ),
inference(spm,[status(thm)],[c_0_138,c_0_1312]),
[final] ).
cnf(c_0_1545,negated_conjecture,
( ~ product(e_4,X1,e_2)
| ~ product(e_5,e_3,X1) ),
inference(spm,[status(thm)],[c_0_160,c_0_1410]),
[final] ).
cnf(c_0_1556,negated_conjecture,
( ~ product(e_2,X1,e_1)
| ~ product(e_2,X2,e_4)
| product(X1,e_2,X2) ),
inference(spm,[status(thm)],[c_0_78,c_0_1516]),
[final] ).
cnf(c_0_1557,negated_conjecture,
( ~ product(e_2,X1,e_5)
| ~ product(e_2,X2,e_1)
| product(X1,e_2,X2) ),
inference(spm,[status(thm)],[c_0_78,c_0_1517]),
[final] ).
cnf(c_0_1558,negated_conjecture,
( ~ product(e_5,X1,e_4)
| ~ product(e_5,X2,e_1)
| product(X1,e_5,X2) ),
inference(spm,[status(thm)],[c_0_78,c_0_1510]),
[final] ).
cnf(c_0_1559,negated_conjecture,
( ~ product(e_3,X1,e_1)
| ~ product(e_3,X2,e_5)
| product(X1,e_3,X2) ),
inference(spm,[status(thm)],[c_0_78,c_0_1511]),
[final] ).
cnf(c_0_1560,negated_conjecture,
( ~ product(e_4,X1,e_3)
| ~ product(e_4,X2,e_1)
| product(X1,e_4,X2) ),
inference(spm,[status(thm)],[c_0_78,c_0_1518]),
[final] ).
cnf(c_0_1561,negated_conjecture,
( ~ product(e_3,X1,e_5)
| ~ product(e_3,X2,e_4)
| product(X1,e_3,X2) ),
inference(spm,[status(thm)],[c_0_78,c_0_1513]),
[final] ).
cnf(c_0_1562,negated_conjecture,
product(e_3,e_1,e_4),
inference(sr,[status(thm)],[c_0_1519,c_0_1480]),
[final] ).
cnf(c_0_1563,negated_conjecture,
( ~ product(e_2,X1,e_4)
| ~ product(e_2,X2,e_3)
| product(X1,e_2,X2) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1520,c_0_1458])]),
[final] ).
cnf(c_0_1564,negated_conjecture,
( ~ product(e_2,X1,e_3)
| ~ product(e_2,X2,e_5)
| product(X1,e_2,X2) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1521,c_0_1458])]),
[final] ).
cnf(c_0_1565,negated_conjecture,
product(e_5,e_5,e_5),
inference(sr,[status(thm)],[c_0_1522,c_0_1480]),
[final] ).
cnf(c_0_1566,negated_conjecture,
product(e_1,e_5,e_3),
inference(sr,[status(thm)],[c_0_1523,c_0_1480]),
[final] ).
cnf(c_0_1567,negated_conjecture,
( ~ product(e_4,X1,e_2)
| ~ product(e_4,X2,e_5)
| product(X1,e_4,X2) ),
inference(spm,[status(thm)],[c_0_78,c_0_1410]),
[final] ).
cnf(c_0_1568,negated_conjecture,
product(e_4,e_1,e_5),
inference(sr,[status(thm)],[c_0_1294,c_0_1480]),
[final] ).
cnf(c_0_1569,negated_conjecture,
product(e_4,e_3,e_2),
inference(sr,[status(thm)],[c_0_1293,c_0_1524]),
[final] ).
cnf(c_0_1570,negated_conjecture,
product(e_5,e_4,e_3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1525,c_0_1512])]),
[final] ).
cnf(c_0_1574,axiom,
greater(e_2,e_1),
e_2_greater_e_1,
[final] ).
cnf(c_0_1575,axiom,
greater(e_3,e_1),
e_3_greater_e_1,
[final] ).
cnf(c_0_1576,axiom,
greater(e_4,e_1),
e_4_greater_e_1,
[final] ).
cnf(c_0_1577,axiom,
greater(e_5,e_1),
e_5_greater_e_1,
[final] ).
cnf(c_0_1580,negated_conjecture,
product(e_1,e_4,e_2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1526,c_0_1448])]),
[final] ).
cnf(c_0_1583,negated_conjecture,
( ~ product(e_4,X1,e_4)
| product(e_4,e_4,X1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1528,c_0_1448])]),
[final] ).
cnf(c_0_1589,negated_conjecture,
product(e_4,e_4,e_4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1487,c_0_1448])]),
[final] ).
cnf(c_0_1606,negated_conjecture,
( ~ product(e_2,X1,e_2)
| product(e_2,e_2,X1) ),
inference(spm,[status(thm)],[c_0_78,c_0_747]),
[final] ).
cnf(c_0_1618,negated_conjecture,
( ~ product(e_4,X1,e_3)
| ~ product(e_5,X1,e_4) ),
inference(spm,[status(thm)],[c_0_1537,c_0_1518]),
[final] ).
cnf(c_0_1619,negated_conjecture,
( ~ product(e_3,X1,e_2)
| ~ product(e_5,X1,e_4) ),
inference(spm,[status(thm)],[c_0_1538,c_0_1312]),
[final] ).
cnf(c_0_1620,negated_conjecture,
( ~ product(e_2,X1,e_5)
| ~ product(e_5,X1,e_4) ),
inference(spm,[status(thm)],[c_0_1539,c_0_1517]),
[final] ).
cnf(c_0_1621,negated_conjecture,
( ~ product(e_2,X1,e_3)
| ~ product(e_3,X1,e_1) ),
inference(spm,[status(thm)],[c_0_1540,c_0_1541]),
[final] ).
cnf(c_0_1622,negated_conjecture,
( ~ product(e_2,X1,e_1)
| ~ product(e_3,X1,e_5) ),
inference(spm,[status(thm)],[c_0_1542,c_0_1516]),
[final] ).
cnf(c_0_1623,negated_conjecture,
( ~ product(e_2,X1,e_5)
| ~ product(e_4,X1,e_3) ),
inference(spm,[status(thm)],[c_0_1543,c_0_1517]),
[final] ).
cnf(c_0_1624,negated_conjecture,
( ~ product(e_2,X1,e_1)
| ~ product(e_3,e_2,X1) ),
inference(spm,[status(thm)],[c_0_224,c_0_1516]),
[final] ).
cnf(c_0_1625,negated_conjecture,
( ~ product(e_2,X1,e_1)
| ~ product(e_2,e_2,X1) ),
inference(spm,[status(thm)],[c_0_175,c_0_1516]),
[final] ).
cnf(c_0_1626,negated_conjecture,
( ~ product(e_2,X1,e_5)
| ~ product(e_3,X1,e_2) ),
inference(spm,[status(thm)],[c_0_1544,c_0_1517]),
[final] ).
cnf(c_0_1627,negated_conjecture,
( ~ product(e_2,X1,e_5)
| ~ product(e_3,e_2,X1) ),
inference(spm,[status(thm)],[c_0_94,c_0_1517]),
[final] ).
cnf(c_0_1628,negated_conjecture,
( ~ product(e_2,X1,e_5)
| ~ product(e_4,e_2,X1) ),
inference(spm,[status(thm)],[c_0_214,c_0_1517]),
[final] ).
cnf(c_0_1629,negated_conjecture,
( ~ product(e_2,X1,e_5)
| ~ product(e_5,e_2,X1) ),
inference(spm,[status(thm)],[c_0_231,c_0_1517]),
[final] ).
cnf(c_0_1630,negated_conjecture,
( ~ product(e_2,X1,e_5)
| ~ product(e_2,e_2,X1) ),
inference(spm,[status(thm)],[c_0_80,c_0_1517]),
[final] ).
cnf(c_0_1631,negated_conjecture,
( ~ product(e_5,X1,e_4)
| ~ product(e_3,e_5,X1) ),
inference(spm,[status(thm)],[c_0_94,c_0_1510]),
[final] ).
cnf(c_0_1632,negated_conjecture,
( ~ product(e_5,X1,e_4)
| ~ product(e_4,e_5,X1) ),
inference(spm,[status(thm)],[c_0_214,c_0_1510]),
[final] ).
cnf(c_0_1633,negated_conjecture,
( ~ product(e_5,X1,e_4)
| ~ product(e_5,e_5,X1) ),
inference(spm,[status(thm)],[c_0_231,c_0_1510]),
[final] ).
cnf(c_0_1634,negated_conjecture,
( ~ product(e_5,X1,e_4)
| ~ product(e_2,e_5,X1) ),
inference(spm,[status(thm)],[c_0_80,c_0_1510]),
[final] ).
cnf(c_0_1635,negated_conjecture,
( ~ product(e_3,X1,e_1)
| ~ product(e_4,X1,e_2) ),
inference(spm,[status(thm)],[c_0_1545,c_0_1511]),
[final] ).
cnf(c_0_1636,negated_conjecture,
( ~ product(e_3,X1,e_1)
| ~ product(e_4,e_3,X1) ),
inference(spm,[status(thm)],[c_0_264,c_0_1511]),
[final] ).
cnf(c_0_1637,negated_conjecture,
( ~ product(e_3,X1,e_1)
| ~ product(e_3,e_3,X1) ),
inference(spm,[status(thm)],[c_0_187,c_0_1511]),
[final] ).
cnf(c_0_1638,negated_conjecture,
( ~ product(e_3,X1,e_1)
| ~ product(e_2,e_3,X1) ),
inference(spm,[status(thm)],[c_0_155,c_0_1511]),
[final] ).
cnf(c_0_1639,negated_conjecture,
( ~ product(e_3,X1,e_5)
| ~ product(e_3,e_3,X1) ),
inference(spm,[status(thm)],[c_0_224,c_0_1513]),
[final] ).
cnf(c_0_1640,negated_conjecture,
( ~ product(e_3,X1,e_5)
| ~ product(e_2,e_3,X1) ),
inference(spm,[status(thm)],[c_0_175,c_0_1513]),
[final] ).
cnf(c_0_1641,negated_conjecture,
( ~ product(e_2,X1,e_4)
| ~ product(e_2,e_2,X1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1546,c_0_1458])]),
[final] ).
cnf(c_0_1642,negated_conjecture,
( ~ product(e_2,X1,e_3)
| ~ product(e_2,e_2,X1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1547,c_0_1458])]),
[final] ).
cnf(c_0_1643,negated_conjecture,
( ~ product(e_2,X1,e_3)
| ~ product(e_3,e_2,X1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1548,c_0_1458])]),
[final] ).
cnf(c_0_1644,negated_conjecture,
( ~ product(e_2,X1,e_3)
| ~ product(e_4,e_2,X1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1549,c_0_1458])]),
[final] ).
cnf(c_0_1645,negated_conjecture,
( ~ product(e_2,X1,e_3)
| ~ product(e_4,X1,e_2) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1550,c_0_1458])]),
[final] ).
cnf(c_0_1646,negated_conjecture,
( ~ product(e_3,X1,e_2)
| ~ product(e_4,X1,e_3) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1551,c_0_1463])]),
[final] ).
cnf(c_0_1647,negated_conjecture,
( ~ product(e_4,X1,e_3)
| ~ product(e_3,e_4,X1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1552,c_0_1463])]),
[final] ).
cnf(c_0_1648,negated_conjecture,
( ~ product(e_4,X1,e_3)
| ~ product(e_4,e_4,X1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1553,c_0_1463])]),
[final] ).
cnf(c_0_1649,negated_conjecture,
( ~ product(e_4,X1,e_3)
| ~ product(e_5,e_4,X1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1554,c_0_1463])]),
[final] ).
cnf(c_0_1650,negated_conjecture,
( ~ product(e_4,X1,e_3)
| ~ product(e_2,e_4,X1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1555,c_0_1463])]),
[final] ).
cnf(c_0_1651,negated_conjecture,
( ~ product(e_4,X1,e_3)
| ~ product(e_1,e_3,X1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1515,c_0_1463])]),
[final] ).
cnf(c_0_1652,negated_conjecture,
( ~ product(e_2,X1,e_1)
| product(X1,e_2,e_5) ),
inference(spm,[status(thm)],[c_0_1556,c_0_1198]),
[final] ).
cnf(c_0_1653,negated_conjecture,
( ~ product(e_2,X1,e_5)
| product(X1,e_2,e_3) ),
inference(spm,[status(thm)],[c_0_1557,c_0_1301]),
[final] ).
cnf(c_0_1654,negated_conjecture,
( ~ product(e_5,X1,e_4)
| product(X1,e_5,e_2) ),
inference(spm,[status(thm)],[c_0_1558,c_0_1497]),
[final] ).
cnf(c_0_1655,negated_conjecture,
( ~ product(e_3,X1,e_1)
| product(X1,e_3,e_2) ),
inference(spm,[status(thm)],[c_0_1559,c_0_1512]),
[final] ).
cnf(c_0_1656,negated_conjecture,
( ~ product(e_4,X1,e_3)
| product(X1,e_4,e_5) ),
inference(spm,[status(thm)],[c_0_1560,c_0_1493]),
[final] ).
cnf(c_0_1657,negated_conjecture,
( ~ product(e_3,X1,e_5)
| product(X1,e_3,e_1) ),
inference(spm,[status(thm)],[c_0_1561,c_0_1562]),
[final] ).
cnf(c_0_1658,negated_conjecture,
( ~ product(e_2,X1,e_4)
| product(X1,e_2,e_1) ),
inference(spm,[status(thm)],[c_0_1563,c_0_1458]),
[final] ).
cnf(c_0_1659,negated_conjecture,
( ~ product(e_2,X1,e_3)
| product(X1,e_2,e_4) ),
inference(spm,[status(thm)],[c_0_1564,c_0_1240]),
[final] ).
cnf(c_0_1660,negated_conjecture,
( ~ product(e_5,X1,e_5)
| product(e_5,e_5,X1) ),
inference(spm,[status(thm)],[c_0_78,c_0_1565]),
[final] ).
cnf(c_0_1661,negated_conjecture,
( ~ product(e_5,X1,e_1)
| product(e_3,e_5,X1) ),
inference(spm,[status(thm)],[c_0_78,c_0_1566]),
[final] ).
cnf(c_0_1662,negated_conjecture,
( ~ product(e_4,X1,e_2)
| product(X1,e_4,e_1) ),
inference(spm,[status(thm)],[c_0_1567,c_0_1568]),
[final] ).
cnf(c_0_1663,negated_conjecture,
( ~ product(e_1,X1,e_4)
| product(e_5,e_1,X1) ),
inference(spm,[status(thm)],[c_0_78,c_0_1568]),
[final] ).
cnf(c_0_1664,negated_conjecture,
( ~ product(e_1,X1,e_3)
| product(e_4,e_1,X1) ),
inference(spm,[status(thm)],[c_0_78,c_0_1562]),
[final] ).
cnf(c_0_1665,negated_conjecture,
( ~ product(e_3,X1,e_4)
| product(e_2,e_3,X1) ),
inference(spm,[status(thm)],[c_0_78,c_0_1569]),
[final] ).
cnf(c_0_1666,negated_conjecture,
( ~ product(e_1,X1,e_5)
| product(e_2,e_1,X1) ),
inference(spm,[status(thm)],[c_0_78,c_0_1473]),
[final] ).
cnf(c_0_1667,negated_conjecture,
( ~ product(e_4,X1,e_5)
| product(e_3,e_4,X1) ),
inference(spm,[status(thm)],[c_0_78,c_0_1570]),
[final] ).
cnf(c_0_1668,negated_conjecture,
( ~ product(e_1,X1,e_2)
| product(e_3,e_1,X1) ),
inference(spm,[status(thm)],[c_0_78,c_0_1458]),
[final] ).
cnf(c_0_1669,negated_conjecture,
( ~ product(e_3,X1,e_3)
| product(e_3,e_3,X1) ),
inference(spm,[status(thm)],[c_0_78,c_0_1463]),
[final] ).
cnf(c_0_1670,negated_conjecture,
( ~ product(e_3,X1,e_2)
| product(X1,e_3,e_4) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1571,c_0_1463])]),
[final] ).
cnf(c_0_1671,negated_conjecture,
( ~ product(e_5,X1,e_3)
| product(e_2,e_5,X1) ),
inference(spm,[status(thm)],[c_0_78,c_0_1448]),
[final] ).
cnf(c_0_1672,negated_conjecture,
( ~ product(e_4,X1,e_1)
| product(e_2,e_4,X1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1572,c_0_1448])]),
[final] ).
cnf(c_0_1673,negated_conjecture,
( ~ product(e_2,X1,e_4)
| product(e_3,e_2,X1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1573,c_0_1448])]),
[final] ).
cnf(c_0_1674,negated_conjecture,
( ~ product(e_3,X1,e_2)
| ~ product(e_3,e_3,X1) ),
inference(spm,[status(thm)],[c_0_94,c_0_1312]),
[final] ).
cnf(c_0_1675,negated_conjecture,
( ~ product(e_3,X1,e_2)
| ~ product(e_2,e_3,X1) ),
inference(spm,[status(thm)],[c_0_80,c_0_1312]),
[final] ).
cnf(c_0_1676,negated_conjecture,
( ~ product(e_4,X1,e_2)
| ~ product(e_4,e_4,X1) ),
inference(spm,[status(thm)],[c_0_264,c_0_1410]),
[final] ).
cnf(c_0_1677,negated_conjecture,
( ~ product(e_4,X1,e_2)
| ~ product(e_3,e_4,X1) ),
inference(spm,[status(thm)],[c_0_187,c_0_1410]),
[final] ).
cnf(c_0_1678,negated_conjecture,
( ~ product(e_4,X1,e_2)
| ~ product(e_2,e_4,X1) ),
inference(spm,[status(thm)],[c_0_155,c_0_1410]),
[final] ).
cnf(c_0_1679,negated_conjecture,
( ~ product(e_1,e_5,e_4)
| product(e_4,e_5,e_2)
| product(e_2,e_5,e_5) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_377,c_0_969]),c_0_80]),
[final] ).
cnf(c_0_1680,negated_conjecture,
( ~ product(e_1,e_5,e_4)
| product(e_2,e_1,e_2)
| product(e_2,e_3,e_4)
| product(e_2,e_3,e_5)
| product(e_4,e_1,e_2)
| product(e_2,e_5,e_5) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_177,c_0_724]),c_0_80]),
[final] ).
cnf(c_0_1681,plain,
( ~ next(X1,e_1)
| ~ product(X1,e_1,e_2) ),
inference(spm,[status(thm)],[c_0_49,c_0_1574]),
[final] ).
cnf(c_0_1682,plain,
( ~ next(X1,e_1)
| ~ product(X1,e_1,e_3) ),
inference(spm,[status(thm)],[c_0_49,c_0_1575]),
[final] ).
cnf(c_0_1683,plain,
( ~ next(X1,e_1)
| ~ product(X1,e_1,e_4) ),
inference(spm,[status(thm)],[c_0_49,c_0_1576]),
[final] ).
cnf(c_0_1684,plain,
( ~ next(X1,e_1)
| ~ product(X1,e_1,e_5) ),
inference(spm,[status(thm)],[c_0_49,c_0_1577]),
[final] ).
cnf(c_0_1685,negated_conjecture,
~ product(e_5,e_4,e_4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_343,c_0_1510]),c_0_1566])]),
[final] ).
cnf(c_0_1686,negated_conjecture,
~ product(e_5,e_1,e_4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_90,c_0_1510]),c_0_1566])]),
[final] ).
cnf(c_0_1687,negated_conjecture,
~ product(e_5,e_4,e_5),
inference(spm,[status(thm)],[c_0_154,c_0_1565]),
[final] ).
cnf(c_0_1688,negated_conjecture,
~ product(e_5,e_5,e_3),
inference(spm,[status(thm)],[c_0_231,c_0_1566]),
[final] ).
cnf(c_0_1689,negated_conjecture,
~ product(e_1,e_4,e_3),
inference(spm,[status(thm)],[c_0_154,c_0_1566]),
[final] ).
cnf(c_0_1690,negated_conjecture,
~ product(e_1,e_5,e_2),
inference(spm,[status(thm)],[c_0_319,c_0_1566]),
[final] ).
cnf(c_0_1691,negated_conjecture,
~ product(e_4,e_1,e_4),
inference(spm,[status(thm)],[c_0_377,c_0_1568]),
[final] ).
cnf(c_0_1692,negated_conjecture,
~ product(e_3,e_1,e_3),
inference(spm,[status(thm)],[c_0_343,c_0_1562]),
[final] ).
cnf(c_0_1693,negated_conjecture,
~ product(e_1,e_2,e_3),
inference(spm,[status(thm)],[c_0_343,c_0_1496]),
[final] ).
cnf(c_0_1694,negated_conjecture,
~ product(e_4,e_4,e_1),
inference(spm,[status(thm)],[c_0_154,c_0_1493]),
[final] ).
cnf(c_0_1695,negated_conjecture,
~ product(e_4,e_3,e_1),
inference(spm,[status(thm)],[c_0_147,c_0_1493]),
[final] ).
cnf(c_0_1696,negated_conjecture,
~ product(e_4,e_2,e_1),
inference(spm,[status(thm)],[c_0_123,c_0_1493]),
[final] ).
cnf(c_0_1697,negated_conjecture,
~ product(e_5,e_3,e_5),
inference(spm,[status(thm)],[c_0_231,c_0_1494]),
[final] ).
cnf(c_0_1698,negated_conjecture,
~ product(e_1,e_2,e_5),
inference(spm,[status(thm)],[c_0_138,c_0_1494]),
[final] ).
cnf(c_0_1699,negated_conjecture,
~ product(e_5,e_5,e_2),
inference(spm,[status(thm)],[c_0_108,c_0_1473]),
[final] ).
cnf(c_0_1700,plain,
~ product(e_1,e_4,e_1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1578,c_0_1473])]),
[final] ).
cnf(c_0_1701,plain,
~ product(e_1,e_5,e_1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1579,c_0_1580])]),
[final] ).
cnf(c_0_1702,negated_conjecture,
~ product(e_5,e_2,e_5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1581,c_0_1458])]),
[final] ).
cnf(c_0_1703,negated_conjecture,
~ product(e_4,e_3,e_3),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1582,c_0_1518]),c_0_1480]),
[final] ).
cnf(c_0_1704,negated_conjecture,
~ product(e_4,e_4,e_5),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_1583,c_0_1584]),c_0_277]),
[final] ).
cnf(c_0_1705,negated_conjecture,
~ product(e_4,e_5,e_2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1585,c_0_1512])]),
[final] ).
cnf(c_0_1706,negated_conjecture,
~ product(e_5,e_2,e_3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1586,c_0_1512])]),
[final] ).
cnf(c_0_1707,negated_conjecture,
~ product(e_3,e_5,e_1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1587,c_0_1463])]),
[final] ).
cnf(c_0_1708,negated_conjecture,
~ product(e_3,e_2,e_4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1273,c_0_1463])]),
[final] ).
cnf(c_0_1709,plain,
~ product(e_4,e_3,e_5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1588,c_0_1589])]),
[final] ).
cnf(c_0_1710,plain,
~ product(e_4,e_5,e_5),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1590,c_0_1589])]),
[final] ).
cnf(c_0_1711,negated_conjecture,
~ product(e_5,e_4,e_2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1591,c_0_1448])]),
[final] ).
cnf(c_0_1712,negated_conjecture,
~ product(e_1,e_2,e_2),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1592,c_0_1448])]),
[final] ).
cnf(c_0_1713,negated_conjecture,
~ product(e_4,e_4,e_3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1593,c_0_1448])]),
[final] ).
cnf(c_0_1714,negated_conjecture,
~ product(e_4,e_3,e_4),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_1594,c_0_1433]),c_0_1595]),
[final] ).
cnf(c_0_1715,negated_conjecture,
~ product(e_4,e_2,e_5),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_123,c_0_1433]),c_0_507]),
[final] ).
cnf(c_0_1716,negated_conjecture,
~ product(e_4,e_5,e_3),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_507,c_0_1433]),c_0_123]),
[final] ).
cnf(c_0_1717,negated_conjecture,
~ product(e_2,e_5,e_5),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_155,c_0_1522]),c_0_1596]),
[final] ).
cnf(c_0_1718,negated_conjecture,
~ product(e_4,e_5,e_4),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_177,c_0_1465]),c_0_1597]),
[final] ).
cnf(c_0_1719,negated_conjecture,
~ product(e_4,e_2,e_4),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_142,c_0_1456]),c_0_224]),
[final] ).
cnf(c_0_1720,negated_conjecture,
~ product(e_3,e_2,e_1),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_1402,c_0_1598]),c_0_177]),
[final] ).
cnf(c_0_1721,negated_conjecture,
~ product(e_5,e_2,e_4),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_138,c_0_1368]),c_0_187]),
[final] ).
cnf(c_0_1722,negated_conjecture,
~ product(e_3,e_3,e_4),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_1307,c_0_1599]),c_0_177]),c_0_320]),
[final] ).
cnf(c_0_1723,negated_conjecture,
~ product(e_4,e_4,e_2),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_1600,c_0_1312]),c_0_1601]),
[final] ).
cnf(c_0_1724,negated_conjecture,
~ product(e_3,e_1,e_1),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_321,c_0_1602]),c_0_253]),
[final] ).
cnf(c_0_1725,negated_conjecture,
~ product(e_1,e_3,e_1),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_1603,c_0_1602]),c_0_1604]),
[final] ).
cnf(c_0_1726,negated_conjecture,
~ product(e_2,e_5,e_1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_97,c_0_1605]),c_0_747])]),
[final] ).
cnf(c_0_1727,negated_conjecture,
~ product(e_3,e_2,e_3),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_187,c_0_1386]),c_0_224]),
[final] ).
cnf(c_0_1728,negated_conjecture,
~ product(e_2,e_2,e_3),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_1606,c_0_165]),c_0_396]),
[final] ).
cnf(c_0_1729,plain,
~ equalish(e_5,e_4),
c_0_1607,
[final] ).
cnf(c_0_1730,plain,
~ equalish(e_5,e_3),
c_0_1608,
[final] ).
cnf(c_0_1731,plain,
~ equalish(e_5,e_2),
c_0_1609,
[final] ).
cnf(c_0_1732,plain,
~ equalish(e_5,e_1),
c_0_1610,
[final] ).
cnf(c_0_1733,plain,
~ equalish(e_4,e_3),
c_0_1611,
[final] ).
cnf(c_0_1734,plain,
~ equalish(e_4,e_2),
c_0_1612,
[final] ).
cnf(c_0_1735,plain,
~ equalish(e_4,e_1),
c_0_1613,
[final] ).
cnf(c_0_1736,plain,
~ equalish(e_3,e_2),
c_0_1614,
[final] ).
cnf(c_0_1737,plain,
~ equalish(e_3,e_1),
c_0_1615,
[final] ).
cnf(c_0_1738,plain,
~ equalish(e_1,e_2),
c_0_1616,
[final] ).
cnf(c_0_1739,negated_conjecture,
product(e_3,e_4,e_1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1617,c_0_1448])]),
[final] ).
cnf(c_0_1740,negated_conjecture,
product(e_5,e_3,e_4),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1418,c_0_1448])]),
[final] ).
cnf(c_0_1741,negated_conjecture,
product(e_4,e_2,e_3),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_1428,c_0_1448])]),
[final] ).
cnf(c_0_1742,axiom,
next(e_4,e_5),
e_4_then_e_5,
[final] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : GRP135-2.005 : TPTP v9.3.1. Released v1.2.0.
% 0.00/0.07 % Command : run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.13/0.38 % Computer : n018.cluster.edu
% 0.13/0.38 % Model : x86_64 x86_64
% 0.13/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.38 % Memory : 8046.5625MB
% 0.13/0.38 % OS : Linux 6.8.0-71-generic
% 0.13/0.38 % CPULimit : 300
% 0.13/0.38 % WCLimit : 300
% 0.13/0.38 % DateTime : Sun Sep 20 20:04:12 UTC 2026
% 0.13/0.38 % CPUTime :
% 0.13/0.38 Running run_E /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.17/0.46 Running first-order theorem proving
% 0.17/0.46 Running: /export/starexec/sandbox2/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/sandbox2/benchmark/theBenchmark.p
% 65.11/10.01 % Version: 3.5.1
% 65.11/10.01 % Preprocessing class: FSMSSMSSSSSNFFN.
% 65.11/10.01 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 65.11/10.01 % Starting G-E--_208_C18_F1_SE_CS_SOS_SP_PS_S5PRR_RG_S04AN with 1500s (5) cores
% 65.11/10.01 % Starting new_bool_3 with 300s (1) cores
% 65.11/10.01 % Starting new_bool_1 with 300s (1) cores
% 65.11/10.01 % Starting sh5l with 300s (1) cores
% 65.11/10.01 % G-E--_208_C18_F1_SE_CS_SOS_SP_PS_S5PRR_RG_S04AN with pid 64618 completed with status 1
% 65.11/10.01 % Result found by G-E--_208_C18_F1_SE_CS_SOS_SP_PS_S5PRR_RG_S04AN
% 65.11/10.01 % Preprocessing class: FSMSSMSSSSSNFFN.
% 65.11/10.01 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 65.11/10.01 % Starting G-E--_208_C18_F1_SE_CS_SOS_SP_PS_S5PRR_RG_S04AN with 1500s (5) cores
% 65.11/10.01 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 65.11/10.01 % No SInE strategy applied
% 65.11/10.01 % Search class: FGHNF-FFSM00-SFFFFFNN
% 65.11/10.01 % Scheduled 7 strats onto 5 cores with 1500 seconds (1500 total)
% 65.11/10.01 % Starting SubtermCWHack with 136s (1) cores
% 65.11/10.01 % Starting G-E--_208_C18_F1_SE_CS_SOS_SP_PS_S5PRR_RG_S04AN with 151s (1) cores
% 65.11/10.01 % Starting G----_404_C05_02_F1_SE_CS_SP_PS_RG_S04AI with 136s (1) cores
% 65.11/10.01 % Starting new_bool_3 with 136s (1) cores
% 65.11/10.01 % Starting new_bool_1 with 136s (1) cores
% 65.11/10.01 % G----_404_C05_02_F1_SE_CS_SP_PS_RG_S04AI with pid 64625 completed with status 1
% 65.11/10.01 % Result found by G----_404_C05_02_F1_SE_CS_SP_PS_RG_S04AI
% 65.11/10.01 % Preprocessing class: FSMSSMSSSSSNFFN.
% 65.11/10.01 % Scheduled 4 strats onto 8 cores with 300 seconds (2400 total)
% 65.11/10.01 % Starting G-E--_208_C18_F1_SE_CS_SOS_SP_PS_S5PRR_RG_S04AN with 1500s (5) cores
% 65.11/10.01 % (lift_lambdas = 1, lambda_to_forall = 1,unroll_only_formulas = 1, sine = Auto)
% 65.11/10.01 % No SInE strategy applied
% 65.11/10.01 % Search class: FGHNF-FFSM00-SFFFFFNN
% 65.11/10.01 % Scheduled 7 strats onto 5 cores with 1500 seconds (1500 total)
% 65.11/10.01 % Starting SubtermCWHack with 136s (1) cores
% 65.11/10.01 % Starting G-E--_208_C18_F1_SE_CS_SOS_SP_PS_S5PRR_RG_S04AN with 151s (1) cores
% 65.11/10.01 % Starting G----_404_C05_02_F1_SE_CS_SP_PS_RG_S04AI with 136s (1) cores
% 65.11/10.01 % Preprocessing time : 0.002 s
% 65.11/10.01 % Presaturation interreduction done
% 65.11/10.01
% 65.11/10.01 % No proof found!
% 65.11/10.01 % SZS status Satisfiable
% 65.11/10.01 % SZS output start Saturation
% See solution above
% 65.11/10.01 % Parsed axioms : 45
% 65.11/10.01 % Removed by relevancy pruning/SinE : 0
% 65.11/10.01 % Initial clauses : 45
% 65.11/10.01 % Removed in clause preprocessing : 0
% 65.11/10.01 % Initial clauses in saturation : 45
% 65.11/10.01 % Processed clauses : 14848
% 65.11/10.01 % ...of these trivial : 373
% 65.11/10.01 % ...subsumed : 7179
% 65.11/10.01 % ...remaining for further processing : 7296
% 65.11/10.01 % Other redundant clauses eliminated : 0
% 65.11/10.01 % Clauses deleted for lack of memory : 0
% 65.11/10.01 % Backward-subsumed : 5608
% 65.11/10.01 % Backward-rewritten : 733
% 65.11/10.01 % Generated clauses : 70692
% 65.11/10.01 % ...of the previous two non-redundant : 67455
% 65.11/10.01 % ...aggressively subsumed : 0
% 65.11/10.01 % Contextual simplify-reflections : 2500
% 65.11/10.01 % Paramodulations : 70084
% 65.11/10.01 % Factorizations : 0
% 65.11/10.01 % NegExts : 0
% 65.11/10.01 % Equation resolutions : 0
% 65.11/10.01 % Disequality decompositions : 0
% 65.11/10.01 % Total rewrite steps : 1779
% 65.11/10.01 % ...of those cached : 1755
% 65.11/10.01 % Propositional unsat checks : 0
% 65.11/10.01 % Propositional check models : 0
% 65.11/10.01 % Propositional check unsatisfiable : 0
% 65.11/10.01 % Propositional clauses : 0
% 65.11/10.01 % Propositional clauses after purity: 0
% 65.11/10.01 % Propositional unsat core size : 0
% 65.11/10.01 % Propositional preprocessing time : 0.000
% 65.11/10.01 % Propositional encoding time : 0.000
% 65.11/10.01 % Propositional solver time : 0.000
% 65.11/10.01 % Success case prop preproc time : 0.000
% 65.11/10.01 % Success case prop encoding time : 0.000
% 65.11/10.01 % Success case prop solver time : 0.000
% 65.11/10.01 % Current number of processed clauses : 302
% 65.11/10.01 % Positive orientable unit clauses : 43
% 65.11/10.01 % Positive unorientable unit clauses: 0
% 65.11/10.01 % Negative unit clauses : 110
% 65.11/10.01 % Non-unit-clauses : 149
% 65.11/10.01 % Current number of unprocessed clauses: 0
% 65.11/10.01 % ...number of literals in the above : 0
% 65.11/10.01 % Current number of archived formulas : 0
% 65.11/10.01 % Current number of archived clauses : 6994
% 65.11/10.01 % Clause-clause subsumption calls (NU) : 2745076
% 65.11/10.01 % Rec. Clause-clause subsumption calls : 175785
% 65.11/10.01 % Non-unit clause-clause subsumptions : 12338
% 65.11/10.01 % Unit Clause-clause subsumption calls : 12232
% 65.11/10.01 % Rewrite failures with RHS unbound : 0
% 65.11/10.01 % BW rewrite match attempts : 143
% 65.11/10.01 % BW rewrite match successes : 24
% 65.11/10.01 % Condensation attempts : 0
% 65.11/10.01 % Condensation successes : 0
% 65.11/10.01 % Termbank termtop insertions : 1638640
% 65.11/10.01 % Search garbage collected termcells : 72
% 65.11/10.01
% 65.11/10.01 % -------------------------------------------------
% 65.11/10.01 % User time : 9.148 s
% 65.11/10.01 % System time : 0.113 s
% 65.11/10.01 % Total time : 9.261 s
% 65.11/10.01 % Maximum resident set size: 3908 pages
% 65.11/10.01
% 65.11/10.01 % -------------------------------------------------
% 65.11/10.01 % User time : 45.352 s
% 65.11/10.01 % System time : 0.660 s
% 65.11/10.01 % Total time : 46.011 s
% 65.11/10.01 % Maximum resident set size: 5120 pages
% 65.11/10.01 % E exiting
%------------------------------------------------------------------------------