%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GRP123-3.004 : TPTP v8.1.2. Released v1.2.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n025.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu May 9 17:23:02 EDT 2024
% Result : Satisfiable 8.71s 8.89s
% Output : Saturation 8.75s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(e_4_is_not_e_3,axiom,
~ equalish(e_4,e_3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_4_is_not_e_3) ).
cnf(product_right_cancellation,axiom,
( ~ product(X32,X31,X34)
| ~ product(X32,X33,X34)
| equalish(X31,X33) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',product_right_cancellation) ).
cnf(e_3_is_not_e_1,axiom,
~ equalish(e_3,e_1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_3_is_not_e_1) ).
cnf(product_idempotence,axiom,
product(X2,X2,X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',product_idempotence) ).
cnf(qg1_2,negated_conjecture,
( ~ product(X85,X87,X84)
| ~ product(X86,X88,X84)
| ~ product(X83,X87,X85)
| ~ product(X83,X88,X86)
| equalish(X87,X88) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',qg1_2) ).
cnf(c73,plain,
( ~ product(X140,X139,X138)
| ~ product(X137,X137,X138)
| ~ product(X137,X139,X140)
| equalish(X139,X137) ),
inference(resolution,[status(thm)],[qg1_2,product_idempotence]) ).
cnf(e_3_is_not_e_2,axiom,
~ equalish(e_3,e_2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_3_is_not_e_2) ).
cnf(e_2_is_not_e_1,axiom,
~ equalish(e_2,e_1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_2_is_not_e_1) ).
cnf(e_1_is_not_e_2,axiom,
~ equalish(e_1,e_2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_1_is_not_e_2) ).
cnf(product_left_cancellation,axiom,
( ~ product(X43,X46,X44)
| ~ product(X45,X46,X44)
| equalish(X43,X45) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',product_left_cancellation) ).
cnf(c33,plain,
( ~ product(X55,X54,X54)
| equalish(X55,X54) ),
inference(resolution,[status(thm)],[product_left_cancellation,product_idempotence]) ).
cnf(c29,plain,
( ~ product(X40,X41,X40)
| equalish(X41,X40) ),
inference(resolution,[status(thm)],[product_right_cancellation,product_idempotence]) ).
cnf(element_1,axiom,
group_element(e_1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',element_1) ).
cnf(element_2,axiom,
group_element(e_2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',element_2) ).
cnf(product_total_function1,axiom,
( ~ group_element(X61)
| ~ group_element(X60)
| product(X61,X60,e_1)
| product(X61,X60,e_2)
| product(X61,X60,e_3)
| product(X61,X60,e_4) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',product_total_function1) ).
cnf(c43,plain,
( ~ group_element(X226)
| product(X226,e_2,e_1)
| product(X226,e_2,e_2)
| product(X226,e_2,e_3)
| product(X226,e_2,e_4) ),
inference(resolution,[status(thm)],[product_total_function1,element_2]) ).
cnf(c326,plain,
( product(e_1,e_2,e_1)
| product(e_1,e_2,e_2)
| product(e_1,e_2,e_3)
| product(e_1,e_2,e_4) ),
inference(resolution,[status(thm)],[c43,element_1]) ).
cnf(c833,plain,
( product(e_1,e_2,e_2)
| product(e_1,e_2,e_3)
| product(e_1,e_2,e_4)
| equalish(e_2,e_1) ),
inference(resolution,[status(thm)],[c326,c29]) ).
cnf(c2218,plain,
( product(e_1,e_2,e_2)
| product(e_1,e_2,e_3)
| product(e_1,e_2,e_4) ),
inference(resolution,[status(thm)],[c833,e_2_is_not_e_1]) ).
cnf(c2222,plain,
( product(e_1,e_2,e_3)
| product(e_1,e_2,e_4)
| equalish(e_1,e_2) ),
inference(resolution,[status(thm)],[c2218,c33]) ).
cnf(c2265,plain,
( product(e_1,e_2,e_3)
| product(e_1,e_2,e_4) ),
inference(resolution,[status(thm)],[c2222,e_1_is_not_e_2]) ).
cnf(c2269,plain,
( product(e_1,e_2,e_4)
| ~ product(e_3,e_2,X726)
| ~ product(e_1,e_1,X726)
| equalish(e_2,e_1) ),
inference(resolution,[status(thm)],[c2265,c73]) ).
cnf(c2302,plain,
( product(e_1,e_2,e_4)
| ~ product(e_3,e_2,e_1)
| equalish(e_2,e_1) ),
inference(resolution,[status(thm)],[c2269,product_idempotence]) ).
cnf(e_2_then_e_3,axiom,
next(e_2,e_3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_2_then_e_3) ).
cnf(e_1_greater_e_0,axiom,
greater(e_1,e_0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_1_greater_e_0) ).
cnf(e_1_then_e_2,axiom,
next(e_1,e_2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_1_then_e_2) ).
cnf(cycle4,axiom,
( ~ cycle(X11,X9)
| ~ cycle(X10,X13)
| ~ next(X11,X10)
| ~ greater(X9,e_0)
| ~ next(X13,X12)
| equalish(X9,X12) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cycle4) ).
cnf(c11,plain,
( ~ cycle(X156,X155)
| ~ cycle(X154,e_1)
| ~ next(X156,X154)
| ~ greater(X155,e_0)
| equalish(X155,e_2) ),
inference(resolution,[status(thm)],[cycle4,e_1_then_e_2]) ).
cnf(c131,plain,
( ~ cycle(X205,e_1)
| ~ cycle(X204,e_1)
| ~ next(X205,X204)
| equalish(e_1,e_2) ),
inference(resolution,[status(thm)],[c11,e_1_greater_e_0]) ).
cnf(c277,plain,
( ~ cycle(e_2,e_1)
| ~ cycle(e_3,e_1)
| equalish(e_1,e_2) ),
inference(resolution,[status(thm)],[c131,e_2_then_e_3]) ).
cnf(cycle3,axiom,
cycle(e_4,e_0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cycle3) ).
cnf(e_3_then_e_4,axiom,
next(e_3,e_4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_3_then_e_4) ).
cnf(e_3_greater_e_2,axiom,
greater(e_3,e_2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_3_greater_e_2) ).
cnf(e_2_greater_e_0,axiom,
greater(e_2,e_0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_2_greater_e_0) ).
cnf(cycle5,axiom,
( ~ cycle(X24,X26)
| ~ cycle(X22,e_0)
| ~ cycle(X23,X25)
| ~ next(X22,X23)
| ~ greater(X22,X24)
| ~ greater(X26,X25) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cycle5) ).
cnf(c24,plain,
( ~ cycle(X202,e_2)
| ~ cycle(X203,e_0)
| ~ cycle(X201,e_0)
| ~ next(X203,X201)
| ~ greater(X203,X202) ),
inference(resolution,[status(thm)],[cycle5,e_2_greater_e_0]) ).
cnf(c272,plain,
( ~ cycle(e_2,e_2)
| ~ cycle(e_3,e_0)
| ~ cycle(X322,e_0)
| ~ next(e_3,X322) ),
inference(resolution,[status(thm)],[c24,e_3_greater_e_2]) ).
cnf(c504,plain,
( ~ cycle(e_2,e_2)
| ~ cycle(e_3,e_0)
| ~ cycle(e_4,e_0) ),
inference(resolution,[status(thm)],[c272,e_3_then_e_4]) ).
cnf(c505,plain,
( ~ cycle(e_2,e_2)
| ~ cycle(e_3,e_0) ),
inference(resolution,[status(thm)],[c504,cycle3]) ).
cnf(e_3_greater_e_0,axiom,
greater(e_3,e_0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_3_greater_e_0) ).
cnf(e_0_then_e_1,axiom,
next(e_0,e_1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_0_then_e_1) ).
cnf(c10,plain,
( ~ cycle(X151,X150)
| ~ cycle(X149,e_0)
| ~ next(X151,X149)
| ~ greater(X150,e_0)
| equalish(X150,e_1) ),
inference(resolution,[status(thm)],[cycle4,e_0_then_e_1]) ).
cnf(c124,plain,
( ~ cycle(X196,e_3)
| ~ cycle(X197,e_0)
| ~ next(X196,X197)
| equalish(e_3,e_1) ),
inference(resolution,[status(thm)],[c10,e_3_greater_e_0]) ).
cnf(c250,plain,
( ~ cycle(e_3,e_3)
| ~ cycle(e_4,e_0)
| equalish(e_3,e_1) ),
inference(resolution,[status(thm)],[c124,e_3_then_e_4]) ).
cnf(c264,plain,
( ~ cycle(e_3,e_3)
| equalish(e_3,e_1) ),
inference(resolution,[status(thm)],[c250,cycle3]) ).
cnf(element_3,axiom,
group_element(e_3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',element_3) ).
cnf(cycle2,axiom,
( ~ group_element(X6)
| cycle(X6,e_0)
| cycle(X6,e_1)
| cycle(X6,e_2)
| cycle(X6,e_3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cycle2) ).
cnf(c4,plain,
( cycle(e_3,e_0)
| cycle(e_3,e_1)
| cycle(e_3,e_2)
| cycle(e_3,e_3) ),
inference(resolution,[status(thm)],[cycle2,element_3]) ).
cnf(c123,plain,
( ~ cycle(X191,e_2)
| ~ cycle(X192,e_0)
| ~ next(X191,X192)
| equalish(e_2,e_1) ),
inference(resolution,[status(thm)],[c10,e_2_greater_e_0]) ).
cnf(c232,plain,
( ~ cycle(e_3,e_2)
| ~ cycle(e_4,e_0)
| equalish(e_2,e_1) ),
inference(resolution,[status(thm)],[c123,e_3_then_e_4]) ).
cnf(c246,plain,
( ~ cycle(e_3,e_2)
| equalish(e_2,e_1) ),
inference(resolution,[status(thm)],[c232,cycle3]) ).
cnf(c247,plain,
( equalish(e_2,e_1)
| cycle(e_3,e_0)
| cycle(e_3,e_1)
| cycle(e_3,e_3) ),
inference(resolution,[status(thm)],[c246,c4]) ).
cnf(c527,plain,
( cycle(e_3,e_0)
| cycle(e_3,e_1)
| cycle(e_3,e_3) ),
inference(resolution,[status(thm)],[c247,e_2_is_not_e_1]) ).
cnf(c599,plain,
( cycle(e_3,e_0)
| cycle(e_3,e_1)
| equalish(e_3,e_1) ),
inference(resolution,[status(thm)],[c527,c264]) ).
cnf(c642,plain,
( cycle(e_3,e_0)
| cycle(e_3,e_1) ),
inference(resolution,[status(thm)],[c599,e_3_is_not_e_1]) ).
cnf(c654,plain,
( cycle(e_3,e_1)
| ~ cycle(e_2,e_2) ),
inference(resolution,[status(thm)],[c642,c505]) ).
cnf(c19,plain,
( ~ cycle(X177,e_1)
| ~ cycle(X178,e_0)
| ~ cycle(X176,e_0)
| ~ next(X178,X176)
| ~ greater(X178,X177) ),
inference(resolution,[status(thm)],[cycle5,e_1_greater_e_0]) ).
cnf(c191,plain,
( ~ cycle(e_2,e_1)
| ~ cycle(e_3,e_0)
| ~ cycle(X265,e_0)
| ~ next(e_3,X265) ),
inference(resolution,[status(thm)],[c19,e_3_greater_e_2]) ).
cnf(c426,plain,
( ~ cycle(e_2,e_1)
| ~ cycle(e_3,e_0)
| ~ cycle(e_4,e_0) ),
inference(resolution,[status(thm)],[c191,e_3_then_e_4]) ).
cnf(c427,plain,
( ~ cycle(e_2,e_1)
| ~ cycle(e_3,e_0) ),
inference(resolution,[status(thm)],[c426,cycle3]) ).
cnf(c650,plain,
( cycle(e_3,e_1)
| ~ cycle(e_2,e_1) ),
inference(resolution,[status(thm)],[c642,c427]) ).
cnf(c3,plain,
( cycle(e_2,e_0)
| cycle(e_2,e_1)
| cycle(e_2,e_2)
| cycle(e_2,e_3) ),
inference(resolution,[status(thm)],[cycle2,element_2]) ).
cnf(c25,plain,
( ~ cycle(X207,e_3)
| ~ cycle(X208,e_0)
| ~ cycle(X206,e_0)
| ~ next(X208,X206)
| ~ greater(X208,X207) ),
inference(resolution,[status(thm)],[cycle5,e_3_greater_e_0]) ).
cnf(c287,plain,
( ~ cycle(e_2,e_3)
| ~ cycle(e_3,e_0)
| ~ cycle(X332,e_0)
| ~ next(e_3,X332) ),
inference(resolution,[status(thm)],[c25,e_3_greater_e_2]) ).
cnf(c516,plain,
( ~ cycle(e_2,e_3)
| ~ cycle(e_3,e_0)
| ~ cycle(e_4,e_0) ),
inference(resolution,[status(thm)],[c287,e_3_then_e_4]) ).
cnf(c518,plain,
( ~ cycle(e_2,e_3)
| ~ cycle(e_3,e_0) ),
inference(resolution,[status(thm)],[c516,cycle3]) ).
cnf(c647,plain,
( cycle(e_3,e_1)
| ~ cycle(e_2,e_3) ),
inference(resolution,[status(thm)],[c642,c518]) ).
cnf(c670,plain,
( cycle(e_3,e_1)
| cycle(e_2,e_0)
| cycle(e_2,e_1)
| cycle(e_2,e_2) ),
inference(resolution,[status(thm)],[c647,c3]) ).
cnf(c895,plain,
( cycle(e_3,e_1)
| cycle(e_2,e_0)
| cycle(e_2,e_2) ),
inference(resolution,[status(thm)],[c670,c650]) ).
cnf(c946,plain,
( cycle(e_3,e_1)
| cycle(e_2,e_0) ),
inference(resolution,[status(thm)],[c895,c654]) ).
cnf(c961,plain,
( cycle(e_2,e_0)
| ~ cycle(e_2,e_1)
| equalish(e_1,e_2) ),
inference(resolution,[status(thm)],[c946,c277]) ).
cnf(c134,plain,
( ~ cycle(X217,e_3)
| ~ cycle(X216,e_1)
| ~ next(X217,X216)
| equalish(e_3,e_2) ),
inference(resolution,[status(thm)],[c11,e_3_greater_e_0]) ).
cnf(c308,plain,
( ~ cycle(e_2,e_3)
| ~ cycle(e_3,e_1)
| equalish(e_3,e_2) ),
inference(resolution,[status(thm)],[c134,e_2_then_e_3]) ).
cnf(c959,plain,
( cycle(e_2,e_0)
| ~ cycle(e_2,e_3)
| equalish(e_3,e_2) ),
inference(resolution,[status(thm)],[c946,c308]) ).
cnf(c1032,plain,
( cycle(e_2,e_0)
| equalish(e_3,e_2)
| cycle(e_2,e_1)
| cycle(e_2,e_2) ),
inference(resolution,[status(thm)],[c959,c3]) ).
cnf(c1320,plain,
( cycle(e_2,e_0)
| cycle(e_2,e_1)
| cycle(e_2,e_2) ),
inference(resolution,[status(thm)],[c1032,e_3_is_not_e_2]) ).
cnf(c1377,plain,
( cycle(e_2,e_0)
| cycle(e_2,e_2)
| equalish(e_1,e_2) ),
inference(resolution,[status(thm)],[c1320,c961]) ).
cnf(c1418,plain,
( cycle(e_2,e_0)
| cycle(e_2,e_2) ),
inference(resolution,[status(thm)],[c1377,e_1_is_not_e_2]) ).
cnf(e_4_greater_e_2,axiom,
greater(e_4,e_2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_4_greater_e_2) ).
cnf(cycle6,axiom,
( ~ cycle(X39,e_0)
| ~ product(X39,e_1,X38)
| ~ greater(X38,X39) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cycle6) ).
cnf(c42,plain,
( ~ group_element(X222)
| product(X222,e_1,e_1)
| product(X222,e_1,e_2)
| product(X222,e_1,e_3)
| product(X222,e_1,e_4) ),
inference(resolution,[status(thm)],[product_total_function1,element_1]) ).
cnf(c321,plain,
( product(e_2,e_1,e_1)
| product(e_2,e_1,e_2)
| product(e_2,e_1,e_3)
| product(e_2,e_1,e_4) ),
inference(resolution,[status(thm)],[c42,element_2]) ).
cnf(c692,plain,
( product(e_2,e_1,e_2)
| product(e_2,e_1,e_3)
| product(e_2,e_1,e_4)
| equalish(e_2,e_1) ),
inference(resolution,[status(thm)],[c321,c33]) ).
cnf(c1492,plain,
( product(e_2,e_1,e_2)
| product(e_2,e_1,e_3)
| product(e_2,e_1,e_4) ),
inference(resolution,[status(thm)],[c692,e_2_is_not_e_1]) ).
cnf(c1504,plain,
( product(e_2,e_1,e_3)
| product(e_2,e_1,e_4)
| equalish(e_1,e_2) ),
inference(resolution,[status(thm)],[c1492,c29]) ).
cnf(c1549,plain,
( product(e_2,e_1,e_3)
| product(e_2,e_1,e_4) ),
inference(resolution,[status(thm)],[c1504,e_1_is_not_e_2]) ).
cnf(c1555,plain,
( product(e_2,e_1,e_4)
| ~ cycle(e_2,e_0)
| ~ greater(e_3,e_2) ),
inference(resolution,[status(thm)],[c1549,cycle6]) ).
cnf(c1578,plain,
( product(e_2,e_1,e_4)
| ~ cycle(e_2,e_0) ),
inference(resolution,[status(thm)],[c1555,e_3_greater_e_2]) ).
cnf(c1580,plain,
( product(e_2,e_1,e_4)
| cycle(e_2,e_2) ),
inference(resolution,[status(thm)],[c1578,c1418]) ).
cnf(c1610,plain,
( cycle(e_2,e_2)
| ~ cycle(e_2,e_0)
| ~ greater(e_4,e_2) ),
inference(resolution,[status(thm)],[c1580,cycle6]) ).
cnf(c1666,plain,
( cycle(e_2,e_2)
| ~ cycle(e_2,e_0) ),
inference(resolution,[status(thm)],[c1610,e_4_greater_e_2]) ).
cnf(c1667,plain,
cycle(e_2,e_2),
inference(resolution,[status(thm)],[c1666,c1418]) ).
cnf(cycle7,axiom,
( ~ cycle(X51,X50)
| ~ product(X51,e_1,X52)
| ~ greater(X50,e_0)
| ~ next(X51,X53)
| equalish(X52,X53) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cycle7) ).
cnf(c1570,plain,
( product(e_2,e_1,e_3)
| ~ cycle(e_2,X472)
| ~ greater(X472,e_0)
| ~ next(e_2,X473)
| equalish(e_4,X473) ),
inference(resolution,[status(thm)],[c1549,cycle7]) ).
cnf(c1716,plain,
( product(e_2,e_1,e_3)
| ~ cycle(e_2,X474)
| ~ greater(X474,e_0)
| equalish(e_4,e_3) ),
inference(resolution,[status(thm)],[c1570,e_2_then_e_3]) ).
cnf(c1719,plain,
( product(e_2,e_1,e_3)
| ~ cycle(e_2,e_2)
| equalish(e_4,e_3) ),
inference(resolution,[status(thm)],[c1716,e_2_greater_e_0]) ).
cnf(c1721,plain,
( product(e_2,e_1,e_3)
| equalish(e_4,e_3) ),
inference(resolution,[status(thm)],[c1719,c1667]) ).
cnf(c1738,plain,
product(e_2,e_1,e_3),
inference(resolution,[status(thm)],[c1721,e_4_is_not_e_3]) ).
cnf(c1739,plain,
( ~ product(X475,e_1,e_3)
| equalish(X475,e_2) ),
inference(resolution,[status(thm)],[c1738,product_left_cancellation]) ).
cnf(qg1_1,negated_conjecture,
( ~ product(X69,X71,X68)
| ~ product(X70,X72,X68)
| ~ product(X67,X71,X69)
| ~ product(X67,X72,X70)
| equalish(X69,X70) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',qg1_1) ).
cnf(c57,plain,
( ~ product(X110,X109,X107)
| ~ product(X108,X108,X107)
| ~ product(X108,X109,X110)
| equalish(X110,X108) ),
inference(resolution,[status(thm)],[qg1_1,product_idempotence]) ).
cnf(c1740,plain,
( ~ product(e_3,e_1,X488)
| ~ product(e_2,e_2,X488)
| equalish(e_3,e_2) ),
inference(resolution,[status(thm)],[c1738,c57]) ).
cnf(c1773,plain,
( ~ product(e_3,e_1,e_2)
| equalish(e_3,e_2) ),
inference(resolution,[status(thm)],[c1740,product_idempotence]) ).
cnf(c322,plain,
( product(e_3,e_1,e_1)
| product(e_3,e_1,e_2)
| product(e_3,e_1,e_3)
| product(e_3,e_1,e_4) ),
inference(resolution,[status(thm)],[c42,element_3]) ).
cnf(c738,plain,
( product(e_3,e_1,e_2)
| product(e_3,e_1,e_3)
| product(e_3,e_1,e_4)
| equalish(e_3,e_1) ),
inference(resolution,[status(thm)],[c322,c33]) ).
cnf(c1858,plain,
( product(e_3,e_1,e_2)
| product(e_3,e_1,e_3)
| product(e_3,e_1,e_4) ),
inference(resolution,[status(thm)],[c738,e_3_is_not_e_1]) ).
cnf(c1861,plain,
( product(e_3,e_1,e_3)
| product(e_3,e_1,e_4)
| equalish(e_3,e_2) ),
inference(resolution,[status(thm)],[c1858,c1773]) ).
cnf(c1915,plain,
( product(e_3,e_1,e_4)
| equalish(e_3,e_2) ),
inference(resolution,[status(thm)],[c1861,c1739]) ).
cnf(c1946,plain,
product(e_3,e_1,e_4),
inference(resolution,[status(thm)],[c1915,e_3_is_not_e_2]) ).
cnf(c1949,plain,
( ~ product(e_3,X545,e_4)
| equalish(X545,e_1) ),
inference(resolution,[status(thm)],[c1946,product_right_cancellation]) ).
cnf(e_2_is_not_e_3,axiom,
~ equalish(e_2,e_3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_2_is_not_e_3) ).
cnf(c328,plain,
( product(e_3,e_2,e_1)
| product(e_3,e_2,e_2)
| product(e_3,e_2,e_3)
| product(e_3,e_2,e_4) ),
inference(resolution,[status(thm)],[c43,element_3]) ).
cnf(c1008,plain,
( product(e_3,e_2,e_1)
| product(e_3,e_2,e_3)
| product(e_3,e_2,e_4)
| equalish(e_3,e_2) ),
inference(resolution,[status(thm)],[c328,c33]) ).
cnf(c2354,plain,
( product(e_3,e_2,e_1)
| product(e_3,e_2,e_3)
| product(e_3,e_2,e_4) ),
inference(resolution,[status(thm)],[c1008,e_3_is_not_e_2]) ).
cnf(c2380,plain,
( product(e_3,e_2,e_1)
| product(e_3,e_2,e_4)
| equalish(e_2,e_3) ),
inference(resolution,[status(thm)],[c2354,c29]) ).
cnf(c2421,plain,
( product(e_3,e_2,e_1)
| product(e_3,e_2,e_4) ),
inference(resolution,[status(thm)],[c2380,e_2_is_not_e_3]) ).
cnf(c2446,plain,
( product(e_3,e_2,e_1)
| equalish(e_2,e_1) ),
inference(resolution,[status(thm)],[c2421,c1949]) ).
cnf(c2453,plain,
( equalish(e_2,e_1)
| product(e_1,e_2,e_4) ),
inference(resolution,[status(thm)],[c2446,c2302]) ).
cnf(c2480,plain,
product(e_1,e_2,e_4),
inference(resolution,[status(thm)],[c2453,e_2_is_not_e_1]) ).
cnf(c2499,plain,
( ~ product(e_1,X759,e_4)
| equalish(X759,e_2) ),
inference(resolution,[status(thm)],[c2480,product_right_cancellation]) ).
cnf(e_1_is_not_e_3,axiom,
~ equalish(e_1,e_3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_1_is_not_e_3) ).
cnf(c44,plain,
( ~ group_element(X230)
| product(X230,e_3,e_1)
| product(X230,e_3,e_2)
| product(X230,e_3,e_3)
| product(X230,e_3,e_4) ),
inference(resolution,[status(thm)],[product_total_function1,element_3]) ).
cnf(c334,plain,
( product(e_1,e_3,e_1)
| product(e_1,e_3,e_2)
| product(e_1,e_3,e_3)
| product(e_1,e_3,e_4) ),
inference(resolution,[status(thm)],[c44,element_1]) ).
cnf(c1081,plain,
( product(e_1,e_3,e_2)
| product(e_1,e_3,e_3)
| product(e_1,e_3,e_4)
| equalish(e_3,e_1) ),
inference(resolution,[status(thm)],[c334,c29]) ).
cnf(c2823,plain,
( product(e_1,e_3,e_2)
| product(e_1,e_3,e_3)
| product(e_1,e_3,e_4) ),
inference(resolution,[status(thm)],[c1081,e_3_is_not_e_1]) ).
cnf(c2843,plain,
( product(e_1,e_3,e_2)
| product(e_1,e_3,e_4)
| equalish(e_1,e_3) ),
inference(resolution,[status(thm)],[c2823,c33]) ).
cnf(c2882,plain,
( product(e_1,e_3,e_2)
| product(e_1,e_3,e_4) ),
inference(resolution,[status(thm)],[c2843,e_1_is_not_e_3]) ).
cnf(c2895,plain,
( product(e_1,e_3,e_2)
| equalish(e_3,e_2) ),
inference(resolution,[status(thm)],[c2882,c2499]) ).
cnf(c2917,plain,
product(e_1,e_3,e_2),
inference(resolution,[status(thm)],[c2895,e_3_is_not_e_2]) ).
cnf(c2919,plain,
( ~ product(e_2,e_3,X1022)
| ~ product(e_1,e_1,X1022)
| equalish(e_3,e_1) ),
inference(resolution,[status(thm)],[c2917,c73]) ).
cnf(c2939,plain,
( ~ product(e_2,e_3,e_1)
| equalish(e_3,e_1) ),
inference(resolution,[status(thm)],[c2919,product_idempotence]) ).
cnf(e_4_is_not_e_1,axiom,
~ equalish(e_4,e_1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_4_is_not_e_1) ).
cnf(c2498,plain,
( ~ product(X758,e_2,e_4)
| equalish(X758,e_1) ),
inference(resolution,[status(thm)],[c2480,product_left_cancellation]) ).
cnf(c2482,plain,
( equalish(e_2,e_1)
| ~ product(e_4,e_2,X789)
| ~ product(e_1,e_1,X789) ),
inference(resolution,[status(thm)],[c2453,c73]) ).
cnf(c2518,plain,
( equalish(e_2,e_1)
| ~ product(e_4,e_2,e_1) ),
inference(resolution,[status(thm)],[c2482,product_idempotence]) ).
cnf(e_4_is_not_e_2,axiom,
~ equalish(e_4,e_2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_4_is_not_e_2) ).
cnf(element_4,axiom,
group_element(e_4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',element_4) ).
cnf(c329,plain,
( product(e_4,e_2,e_1)
| product(e_4,e_2,e_2)
| product(e_4,e_2,e_3)
| product(e_4,e_2,e_4) ),
inference(resolution,[status(thm)],[c43,element_4]) ).
cnf(c1048,plain,
( product(e_4,e_2,e_1)
| product(e_4,e_2,e_3)
| product(e_4,e_2,e_4)
| equalish(e_4,e_2) ),
inference(resolution,[status(thm)],[c329,c33]) ).
cnf(c2624,plain,
( product(e_4,e_2,e_1)
| product(e_4,e_2,e_3)
| product(e_4,e_2,e_4) ),
inference(resolution,[status(thm)],[c1048,e_4_is_not_e_2]) ).
cnf(c2630,plain,
( product(e_4,e_2,e_3)
| product(e_4,e_2,e_4)
| equalish(e_2,e_1) ),
inference(resolution,[status(thm)],[c2624,c2518]) ).
cnf(c2701,plain,
( product(e_4,e_2,e_3)
| product(e_4,e_2,e_4) ),
inference(resolution,[status(thm)],[c2630,e_2_is_not_e_1]) ).
cnf(c2720,plain,
( product(e_4,e_2,e_3)
| equalish(e_4,e_1) ),
inference(resolution,[status(thm)],[c2701,c2498]) ).
cnf(c2744,plain,
product(e_4,e_2,e_3),
inference(resolution,[status(thm)],[c2720,e_4_is_not_e_1]) ).
cnf(c2505,plain,
( ~ product(X826,X825,X824)
| ~ product(e_4,e_2,X824)
| ~ product(e_1,X825,X826)
| equalish(X825,e_2) ),
inference(resolution,[status(thm)],[c2480,qg1_2]) ).
cnf(c2913,plain,
( equalish(e_3,e_2)
| ~ product(e_2,e_3,X1017)
| ~ product(e_4,e_2,X1017) ),
inference(resolution,[status(thm)],[c2895,c2505]) ).
cnf(c2935,plain,
( equalish(e_3,e_2)
| ~ product(e_2,e_3,e_3) ),
inference(resolution,[status(thm)],[c2913,c2744]) ).
cnf(c335,plain,
( product(e_2,e_3,e_1)
| product(e_2,e_3,e_2)
| product(e_2,e_3,e_3)
| product(e_2,e_3,e_4) ),
inference(resolution,[status(thm)],[c44,element_2]) ).
cnf(c1128,plain,
( product(e_2,e_3,e_1)
| product(e_2,e_3,e_3)
| product(e_2,e_3,e_4)
| equalish(e_3,e_2) ),
inference(resolution,[status(thm)],[c335,c29]) ).
cnf(c3004,plain,
( product(e_2,e_3,e_1)
| product(e_2,e_3,e_4)
| equalish(e_3,e_2) ),
inference(resolution,[status(thm)],[c1128,c2935]) ).
cnf(c3067,plain,
( product(e_2,e_3,e_1)
| product(e_2,e_3,e_4) ),
inference(resolution,[status(thm)],[c3004,e_3_is_not_e_2]) ).
cnf(c3074,plain,
( product(e_2,e_3,e_4)
| equalish(e_3,e_1) ),
inference(resolution,[status(thm)],[c3067,c2939]) ).
cnf(c3117,plain,
product(e_2,e_3,e_4),
inference(resolution,[status(thm)],[c3074,e_3_is_not_e_1]) ).
cnf(c3127,plain,
( ~ product(e_2,X1096,e_4)
| equalish(X1096,e_3) ),
inference(resolution,[status(thm)],[c3117,product_right_cancellation]) ).
cnf(c2922,plain,
( ~ product(e_1,X1003,e_2)
| equalish(X1003,e_3) ),
inference(resolution,[status(thm)],[c2917,product_right_cancellation]) ).
cnf(c45,plain,
( ~ group_element(X234)
| product(X234,e_4,e_1)
| product(X234,e_4,e_2)
| product(X234,e_4,e_3)
| product(X234,e_4,e_4) ),
inference(resolution,[status(thm)],[product_total_function1,element_4]) ).
cnf(c341,plain,
( product(e_1,e_4,e_1)
| product(e_1,e_4,e_2)
| product(e_1,e_4,e_3)
| product(e_1,e_4,e_4) ),
inference(resolution,[status(thm)],[c45,element_1]) ).
cnf(c1195,plain,
( product(e_1,e_4,e_2)
| product(e_1,e_4,e_3)
| product(e_1,e_4,e_4)
| equalish(e_4,e_1) ),
inference(resolution,[status(thm)],[c341,c29]) ).
cnf(c3430,plain,
( product(e_1,e_4,e_2)
| product(e_1,e_4,e_3)
| product(e_1,e_4,e_4) ),
inference(resolution,[status(thm)],[c1195,e_4_is_not_e_1]) ).
cnf(c3435,plain,
( product(e_1,e_4,e_3)
| product(e_1,e_4,e_4)
| equalish(e_4,e_3) ),
inference(resolution,[status(thm)],[c3430,c2922]) ).
cnf(c3501,plain,
( product(e_1,e_4,e_3)
| product(e_1,e_4,e_4) ),
inference(resolution,[status(thm)],[c3435,e_4_is_not_e_3]) ).
cnf(c3516,plain,
( product(e_1,e_4,e_3)
| equalish(e_4,e_2) ),
inference(resolution,[status(thm)],[c3501,c2499]) ).
cnf(c3543,plain,
product(e_1,e_4,e_3),
inference(resolution,[status(thm)],[c3516,e_4_is_not_e_2]) ).
cnf(c3548,plain,
( ~ product(X1296,e_4,e_3)
| equalish(X1296,e_1) ),
inference(resolution,[status(thm)],[c3543,product_left_cancellation]) ).
cnf(c342,plain,
( product(e_2,e_4,e_1)
| product(e_2,e_4,e_2)
| product(e_2,e_4,e_3)
| product(e_2,e_4,e_4) ),
inference(resolution,[status(thm)],[c45,element_2]) ).
cnf(c1242,plain,
( product(e_2,e_4,e_1)
| product(e_2,e_4,e_3)
| product(e_2,e_4,e_4)
| equalish(e_4,e_2) ),
inference(resolution,[status(thm)],[c342,c29]) ).
cnf(c3654,plain,
( product(e_2,e_4,e_1)
| product(e_2,e_4,e_3)
| product(e_2,e_4,e_4) ),
inference(resolution,[status(thm)],[c1242,e_4_is_not_e_2]) ).
cnf(c3680,plain,
( product(e_2,e_4,e_1)
| product(e_2,e_4,e_4)
| equalish(e_2,e_1) ),
inference(resolution,[status(thm)],[c3654,c3548]) ).
cnf(c3726,plain,
( product(e_2,e_4,e_1)
| product(e_2,e_4,e_4) ),
inference(resolution,[status(thm)],[c3680,e_2_is_not_e_1]) ).
cnf(c3745,plain,
( product(e_2,e_4,e_1)
| equalish(e_4,e_3) ),
inference(resolution,[status(thm)],[c3726,c3127]) ).
cnf(c3768,plain,
product(e_2,e_4,e_1),
inference(resolution,[status(thm)],[c3745,e_4_is_not_e_3]) ).
cnf(c2461,plain,
product(e_3,e_2,e_1),
inference(resolution,[status(thm)],[c2446,e_2_is_not_e_1]) ).
cnf(c2468,plain,
( ~ product(e_3,X753,e_1)
| equalish(X753,e_2) ),
inference(resolution,[status(thm)],[c2461,product_right_cancellation]) ).
cnf(c2928,plain,
( ~ product(X1038,X1037,X1036)
| ~ product(e_2,e_3,X1036)
| ~ product(e_1,X1037,X1038)
| equalish(X1037,e_3) ),
inference(resolution,[status(thm)],[c2917,qg1_2]) ).
cnf(c3547,plain,
( ~ product(e_3,e_4,X1319)
| ~ product(e_2,e_3,X1319)
| equalish(e_4,e_3) ),
inference(resolution,[status(thm)],[c3543,c2928]) ).
cnf(c3570,plain,
( ~ product(e_3,e_4,e_4)
| equalish(e_4,e_3) ),
inference(resolution,[status(thm)],[c3547,c3117]) ).
cnf(c343,plain,
( product(e_3,e_4,e_1)
| product(e_3,e_4,e_2)
| product(e_3,e_4,e_3)
| product(e_3,e_4,e_4) ),
inference(resolution,[status(thm)],[c45,element_3]) ).
cnf(c1289,plain,
( product(e_3,e_4,e_1)
| product(e_3,e_4,e_2)
| product(e_3,e_4,e_4)
| equalish(e_4,e_3) ),
inference(resolution,[status(thm)],[c343,c29]) ).
cnf(c3860,plain,
( product(e_3,e_4,e_1)
| product(e_3,e_4,e_2)
| equalish(e_4,e_3) ),
inference(resolution,[status(thm)],[c1289,c3570]) ).
cnf(c3921,plain,
( product(e_3,e_4,e_1)
| product(e_3,e_4,e_2) ),
inference(resolution,[status(thm)],[c3860,e_4_is_not_e_3]) ).
cnf(c3923,plain,
( product(e_3,e_4,e_2)
| equalish(e_4,e_2) ),
inference(resolution,[status(thm)],[c3921,c2468]) ).
cnf(c3985,plain,
product(e_3,e_4,e_2),
inference(resolution,[status(thm)],[c3923,e_4_is_not_e_2]) ).
cnf(c4004,plain,
( ~ product(X1573,X1572,X1571)
| ~ product(e_2,e_4,X1571)
| ~ product(e_3,X1572,X1573)
| equalish(X1572,e_4) ),
inference(resolution,[status(thm)],[c3985,qg1_2]) ).
cnf(c4027,plain,
( ~ product(e_1,e_2,X1582)
| ~ product(e_2,e_4,X1582)
| equalish(e_2,e_4) ),
inference(resolution,[status(thm)],[c4004,c2461]) ).
cnf(c4030,plain,
( ~ product(e_1,e_2,e_1)
| equalish(e_2,e_4) ),
inference(resolution,[status(thm)],[c4027,c3768]) ).
cnf(c4026,plain,
( ~ product(e_4,e_1,X1580)
| ~ product(e_2,e_4,X1580)
| equalish(e_1,e_4) ),
inference(resolution,[status(thm)],[c4004,c1946]) ).
cnf(c4029,plain,
( ~ product(e_4,e_1,e_1)
| equalish(e_1,e_4) ),
inference(resolution,[status(thm)],[c4026,c3768]) ).
cnf(c4025,plain,
( ~ product(e_3,e_3,X1579)
| ~ product(e_2,e_4,X1579)
| equalish(e_3,e_4) ),
inference(resolution,[status(thm)],[c4004,product_idempotence]) ).
cnf(c4023,plain,
( ~ product(e_3,X1578,e_3)
| ~ product(e_2,e_4,e_3)
| equalish(X1578,e_4) ),
inference(factor,[status(thm)],[c4004]) ).
cnf(c4002,plain,
( ~ product(X1563,X1562,X1561)
| ~ product(e_2,e_4,X1561)
| ~ product(e_3,X1562,X1563)
| equalish(X1563,e_2) ),
inference(resolution,[status(thm)],[c3985,qg1_1]) ).
cnf(c4015,plain,
( ~ product(e_3,X1570,e_3)
| ~ product(e_2,e_4,e_3)
| equalish(e_3,e_2) ),
inference(factor,[status(thm)],[c4002]) ).
cnf(c4019,plain,
( ~ product(e_1,e_2,X1569)
| ~ product(e_2,e_4,X1569)
| equalish(e_1,e_2) ),
inference(resolution,[status(thm)],[c4002,c2461]) ).
cnf(c4022,plain,
( ~ product(e_1,e_2,e_1)
| equalish(e_1,e_2) ),
inference(resolution,[status(thm)],[c4019,c3768]) ).
cnf(c4018,plain,
( ~ product(e_4,e_1,X1567)
| ~ product(e_2,e_4,X1567)
| equalish(e_4,e_2) ),
inference(resolution,[status(thm)],[c4002,c1946]) ).
cnf(c4021,plain,
( ~ product(e_4,e_1,e_1)
| equalish(e_4,e_2) ),
inference(resolution,[status(thm)],[c4018,c3768]) ).
cnf(c4017,plain,
( ~ product(e_3,e_3,X1566)
| ~ product(e_2,e_4,X1566)
| equalish(e_3,e_2) ),
inference(resolution,[status(thm)],[c4002,product_idempotence]) ).
cnf(c71,plain,
( ~ product(X126,X124,X123)
| ~ product(X123,X125,X123)
| ~ product(X123,X124,X126)
| equalish(X124,X125) ),
inference(factor,[status(thm)],[qg1_2]) ).
cnf(c3999,plain,
( ~ product(e_2,e_4,e_3)
| ~ product(e_3,X1552,e_3)
| equalish(e_4,X1552) ),
inference(resolution,[status(thm)],[c3985,c71]) ).
cnf(c1947,plain,
( ~ product(X541,e_1,e_4)
| equalish(X541,e_3) ),
inference(resolution,[status(thm)],[c1946,product_left_cancellation]) ).
cnf(c1948,plain,
( ~ product(e_4,e_1,X554)
| ~ product(e_3,e_3,X554)
| equalish(e_4,e_3) ),
inference(resolution,[status(thm)],[c1946,c57]) ).
cnf(c1967,plain,
( ~ product(e_4,e_1,e_3)
| equalish(e_4,e_3) ),
inference(resolution,[status(thm)],[c1948,product_idempotence]) ).
cnf(c323,plain,
( product(e_4,e_1,e_1)
| product(e_4,e_1,e_2)
| product(e_4,e_1,e_3)
| product(e_4,e_1,e_4) ),
inference(resolution,[status(thm)],[c42,element_4]) ).
cnf(c784,plain,
( product(e_4,e_1,e_2)
| product(e_4,e_1,e_3)
| product(e_4,e_1,e_4)
| equalish(e_4,e_1) ),
inference(resolution,[status(thm)],[c323,c33]) ).
cnf(c2053,plain,
( product(e_4,e_1,e_2)
| product(e_4,e_1,e_3)
| product(e_4,e_1,e_4) ),
inference(resolution,[status(thm)],[c784,e_4_is_not_e_1]) ).
cnf(c2077,plain,
( product(e_4,e_1,e_2)
| product(e_4,e_1,e_4)
| equalish(e_4,e_3) ),
inference(resolution,[status(thm)],[c2053,c1967]) ).
cnf(c2123,plain,
( product(e_4,e_1,e_2)
| equalish(e_4,e_3) ),
inference(resolution,[status(thm)],[c2077,c1947]) ).
cnf(c2142,plain,
product(e_4,e_1,e_2),
inference(resolution,[status(thm)],[c2123,e_4_is_not_e_3]) ).
cnf(c1955,plain,
( ~ product(X567,X566,X565)
| ~ product(e_4,e_1,X565)
| ~ product(e_3,X566,X567)
| equalish(X567,e_4) ),
inference(resolution,[status(thm)],[c1946,qg1_1]) ).
cnf(c3991,plain,
( ~ product(e_2,e_4,X1550)
| ~ product(e_4,e_1,X1550)
| equalish(e_2,e_4) ),
inference(resolution,[status(thm)],[c3985,c1955]) ).
cnf(c4013,plain,
( ~ product(e_2,e_4,e_2)
| equalish(e_2,e_4) ),
inference(resolution,[status(thm)],[c3991,c2142]) ).
cnf(c1959,plain,
( ~ product(X574,X573,X572)
| ~ product(e_4,e_1,X572)
| ~ product(e_3,X573,X574)
| equalish(X573,e_1) ),
inference(resolution,[status(thm)],[c1946,qg1_2]) ).
cnf(c3990,plain,
( ~ product(e_2,e_4,X1549)
| ~ product(e_4,e_1,X1549)
| equalish(e_4,e_1) ),
inference(resolution,[status(thm)],[c3985,c1959]) ).
cnf(c4012,plain,
( ~ product(e_2,e_4,e_2)
| equalish(e_4,e_1) ),
inference(resolution,[status(thm)],[c3990,c2142]) ).
cnf(c3988,plain,
( ~ product(e_2,e_4,X1547)
| ~ product(e_3,e_3,X1547)
| equalish(e_4,e_3) ),
inference(resolution,[status(thm)],[c3985,c73]) ).
cnf(c4011,plain,
( ~ product(e_2,e_4,e_3)
| equalish(e_4,e_3) ),
inference(resolution,[status(thm)],[c3988,product_idempotence]) ).
cnf(c2473,plain,
( ~ product(X799,X798,X797)
| ~ product(e_1,e_2,X797)
| ~ product(e_3,X798,X799)
| equalish(X799,e_1) ),
inference(resolution,[status(thm)],[c2461,qg1_1]) ).
cnf(c3987,plain,
( ~ product(e_2,e_4,X1546)
| ~ product(e_1,e_2,X1546)
| equalish(e_2,e_1) ),
inference(resolution,[status(thm)],[c3985,c2473]) ).
cnf(c4010,plain,
( ~ product(e_2,e_4,e_4)
| equalish(e_2,e_1) ),
inference(resolution,[status(thm)],[c3987,c2480]) ).
cnf(c3986,plain,
( ~ product(e_2,e_4,X1545)
| ~ product(e_3,e_3,X1545)
| equalish(e_2,e_3) ),
inference(resolution,[status(thm)],[c3985,c57]) ).
cnf(c4009,plain,
( ~ product(e_2,e_4,e_3)
| equalish(e_2,e_3) ),
inference(resolution,[status(thm)],[c3986,product_idempotence]) ).
cnf(c2474,plain,
( ~ product(X810,X809,X808)
| ~ product(e_1,e_2,X808)
| ~ product(e_3,X809,X810)
| equalish(X809,e_2) ),
inference(resolution,[status(thm)],[c2461,qg1_2]) ).
cnf(c3980,plain,
( equalish(e_4,e_2)
| ~ product(e_2,e_4,X1543)
| ~ product(e_1,e_2,X1543) ),
inference(resolution,[status(thm)],[c3923,c2474]) ).
cnf(c4008,plain,
( equalish(e_4,e_2)
| ~ product(e_2,e_4,e_4) ),
inference(resolution,[status(thm)],[c3980,c2480]) ).
cnf(c3556,plain,
( ~ product(X1340,X1339,X1338)
| ~ product(e_3,e_4,X1338)
| ~ product(e_1,X1339,X1340)
| equalish(X1339,e_4) ),
inference(resolution,[status(thm)],[c3543,qg1_2]) ).
cnf(c3596,plain,
( ~ product(e_4,e_2,X1344)
| ~ product(e_3,e_4,X1344)
| equalish(e_2,e_4) ),
inference(resolution,[status(thm)],[c3556,c2480]) ).
cnf(c3995,plain,
( ~ product(e_4,e_2,e_2)
| equalish(e_2,e_4) ),
inference(resolution,[status(thm)],[c3985,c3596]) ).
cnf(c3597,plain,
( ~ product(e_2,e_3,X1346)
| ~ product(e_3,e_4,X1346)
| equalish(e_3,e_4) ),
inference(resolution,[status(thm)],[c3556,c2917]) ).
cnf(c3994,plain,
( ~ product(e_2,e_3,e_2)
| equalish(e_3,e_4) ),
inference(resolution,[status(thm)],[c3985,c3597]) ).
cnf(c3555,plain,
( ~ product(X1330,X1329,X1328)
| ~ product(e_3,e_4,X1328)
| ~ product(e_1,X1329,X1330)
| equalish(X1330,e_3) ),
inference(resolution,[status(thm)],[c3543,qg1_1]) ).
cnf(c3579,plain,
( ~ product(e_2,e_3,X1335)
| ~ product(e_3,e_4,X1335)
| equalish(e_2,e_3) ),
inference(resolution,[status(thm)],[c3555,c2917]) ).
cnf(c3993,plain,
( ~ product(e_2,e_3,e_2)
| equalish(e_2,e_3) ),
inference(resolution,[status(thm)],[c3985,c3579]) ).
cnf(c3578,plain,
( ~ product(e_4,e_2,X1334)
| ~ product(e_3,e_4,X1334)
| equalish(e_4,e_3) ),
inference(resolution,[status(thm)],[c3555,c2480]) ).
cnf(c3992,plain,
( ~ product(e_4,e_2,e_2)
| equalish(e_4,e_3) ),
inference(resolution,[status(thm)],[c3985,c3578]) ).
cnf(product_total_function2,axiom,
( ~ product(X16,X15,X18)
| ~ product(X16,X15,X17)
| equalish(X18,X17) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',product_total_function2) ).
cnf(c4001,plain,
( ~ product(e_3,e_4,X1522)
| equalish(X1522,e_2) ),
inference(resolution,[status(thm)],[c3985,product_total_function2]) ).
cnf(c3997,plain,
( ~ product(e_3,X1521,e_2)
| equalish(X1521,e_4) ),
inference(resolution,[status(thm)],[c3985,product_right_cancellation]) ).
cnf(c3996,plain,
( ~ product(X1519,e_4,e_2)
| equalish(X1519,e_3) ),
inference(resolution,[status(thm)],[c3985,product_left_cancellation]) ).
cnf(c3781,plain,
( ~ product(X1451,X1450,X1449)
| ~ product(e_1,e_4,X1449)
| ~ product(e_2,X1450,X1451)
| equalish(X1450,e_4) ),
inference(resolution,[status(thm)],[c3768,qg1_2]) ).
cnf(c3804,plain,
( ~ product(e_2,e_2,X1460)
| ~ product(e_1,e_4,X1460)
| equalish(e_2,e_4) ),
inference(resolution,[status(thm)],[c3781,product_idempotence]) ).
cnf(c3803,plain,
( ~ product(e_3,e_1,X1458)
| ~ product(e_1,e_4,X1458)
| equalish(e_1,e_4) ),
inference(resolution,[status(thm)],[c3781,c1738]) ).
cnf(c3807,plain,
( ~ product(e_3,e_1,e_3)
| equalish(e_1,e_4) ),
inference(resolution,[status(thm)],[c3803,c3543]) ).
cnf(c3802,plain,
( ~ product(e_4,e_3,X1457)
| ~ product(e_1,e_4,X1457)
| equalish(e_3,e_4) ),
inference(resolution,[status(thm)],[c3781,c3117]) ).
cnf(c3806,plain,
( ~ product(e_4,e_3,e_3)
| equalish(e_3,e_4) ),
inference(resolution,[status(thm)],[c3802,c3543]) ).
cnf(c3801,plain,
( ~ product(e_2,X1456,e_2)
| ~ product(e_1,e_4,e_2)
| equalish(X1456,e_4) ),
inference(factor,[status(thm)],[c3781]) ).
cnf(c3780,plain,
( ~ product(X1442,X1441,X1440)
| ~ product(e_1,e_4,X1440)
| ~ product(e_2,X1441,X1442)
| equalish(X1442,e_1) ),
inference(resolution,[status(thm)],[c3768,qg1_1]) ).
cnf(c3793,plain,
( ~ product(e_2,X1448,e_2)
| ~ product(e_1,e_4,e_2)
| equalish(e_2,e_1) ),
inference(factor,[status(thm)],[c3780]) ).
cnf(c3796,plain,
( ~ product(e_2,e_2,X1447)
| ~ product(e_1,e_4,X1447)
| equalish(e_2,e_1) ),
inference(resolution,[status(thm)],[c3780,product_idempotence]) ).
cnf(c3795,plain,
( ~ product(e_3,e_1,X1445)
| ~ product(e_1,e_4,X1445)
| equalish(e_3,e_1) ),
inference(resolution,[status(thm)],[c3780,c1738]) ).
cnf(c3799,plain,
( ~ product(e_3,e_1,e_3)
| equalish(e_3,e_1) ),
inference(resolution,[status(thm)],[c3795,c3543]) ).
cnf(c3794,plain,
( ~ product(e_4,e_3,X1444)
| ~ product(e_1,e_4,X1444)
| equalish(e_4,e_1) ),
inference(resolution,[status(thm)],[c3780,c3117]) ).
cnf(c3798,plain,
( ~ product(e_4,e_3,e_3)
| equalish(e_4,e_1) ),
inference(resolution,[status(thm)],[c3794,c3543]) ).
cnf(c3778,plain,
( ~ product(e_1,e_4,e_2)
| ~ product(e_2,X1436,e_2)
| equalish(e_4,X1436) ),
inference(resolution,[status(thm)],[c3768,c71]) ).
cnf(c3119,plain,
( ~ product(e_4,e_3,X1120)
| ~ product(e_2,e_2,X1120)
| equalish(e_3,e_2) ),
inference(resolution,[status(thm)],[c3117,c73]) ).
cnf(c3142,plain,
( ~ product(e_4,e_3,e_2)
| equalish(e_3,e_2) ),
inference(resolution,[status(thm)],[c3119,product_idempotence]) ).
cnf(c1748,plain,
( ~ product(X501,X500,X499)
| ~ product(e_3,e_1,X499)
| ~ product(e_2,X500,X501)
| equalish(X501,e_3) ),
inference(resolution,[status(thm)],[c1738,qg1_1]) ).
cnf(c3120,plain,
( ~ product(e_4,e_3,X1121)
| ~ product(e_3,e_1,X1121)
| equalish(e_4,e_3) ),
inference(resolution,[status(thm)],[c3117,c1748]) ).
cnf(c3144,plain,
( ~ product(e_4,e_3,e_4)
| equalish(e_4,e_3) ),
inference(resolution,[status(thm)],[c3120,c1946]) ).
cnf(c337,plain,
( product(e_4,e_3,e_1)
| product(e_4,e_3,e_2)
| product(e_4,e_3,e_3)
| product(e_4,e_3,e_4) ),
inference(resolution,[status(thm)],[c44,element_4]) ).
cnf(c1171,plain,
( product(e_4,e_3,e_1)
| product(e_4,e_3,e_2)
| product(e_4,e_3,e_4)
| equalish(e_4,e_3) ),
inference(resolution,[status(thm)],[c337,c33]) ).
cnf(c3241,plain,
( product(e_4,e_3,e_1)
| product(e_4,e_3,e_2)
| equalish(e_4,e_3) ),
inference(resolution,[status(thm)],[c1171,c3144]) ).
cnf(c3286,plain,
( product(e_4,e_3,e_1)
| product(e_4,e_3,e_2) ),
inference(resolution,[status(thm)],[c3241,e_4_is_not_e_3]) ).
cnf(c3318,plain,
( product(e_4,e_3,e_1)
| equalish(e_3,e_2) ),
inference(resolution,[status(thm)],[c3286,c3142]) ).
cnf(c3344,plain,
product(e_4,e_3,e_1),
inference(resolution,[status(thm)],[c3318,e_3_is_not_e_2]) ).
cnf(c3131,plain,
( ~ product(X1131,X1130,X1129)
| ~ product(e_4,e_3,X1129)
| ~ product(e_2,X1130,X1131)
| equalish(X1131,e_4) ),
inference(resolution,[status(thm)],[c3117,qg1_1]) ).
cnf(c3777,plain,
( ~ product(e_1,e_4,X1435)
| ~ product(e_4,e_3,X1435)
| equalish(e_1,e_4) ),
inference(resolution,[status(thm)],[c3768,c3131]) ).
cnf(c3791,plain,
( ~ product(e_1,e_4,e_1)
| equalish(e_1,e_4) ),
inference(resolution,[status(thm)],[c3777,c3344]) ).
cnf(c1753,plain,
( ~ product(X508,X507,X506)
| ~ product(e_3,e_1,X506)
| ~ product(e_2,X507,X508)
| equalish(X507,e_1) ),
inference(resolution,[status(thm)],[c1738,qg1_2]) ).
cnf(c3773,plain,
( ~ product(e_1,e_4,X1434)
| ~ product(e_3,e_1,X1434)
| equalish(e_4,e_1) ),
inference(resolution,[status(thm)],[c3768,c1753]) ).
cnf(c3790,plain,
( ~ product(e_1,e_4,e_4)
| equalish(e_4,e_1) ),
inference(resolution,[status(thm)],[c3773,c1946]) ).
cnf(c3771,plain,
( ~ product(e_1,e_4,X1431)
| ~ product(e_3,e_1,X1431)
| equalish(e_1,e_3) ),
inference(resolution,[status(thm)],[c3768,c1748]) ).
cnf(c3789,plain,
( ~ product(e_1,e_4,e_4)
| equalish(e_1,e_3) ),
inference(resolution,[status(thm)],[c3771,c1946]) ).
cnf(c3770,plain,
( ~ product(e_1,e_4,X1430)
| ~ product(e_2,e_2,X1430)
| equalish(e_4,e_2) ),
inference(resolution,[status(thm)],[c3768,c73]) ).
cnf(c3788,plain,
( ~ product(e_1,e_4,e_2)
| equalish(e_4,e_2) ),
inference(resolution,[status(thm)],[c3770,product_idempotence]) ).
cnf(c3769,plain,
( ~ product(e_1,e_4,X1426)
| ~ product(e_2,e_2,X1426)
| equalish(e_1,e_2) ),
inference(resolution,[status(thm)],[c3768,c57]) ).
cnf(c3787,plain,
( ~ product(e_1,e_4,e_2)
| equalish(e_1,e_2) ),
inference(resolution,[status(thm)],[c3769,product_idempotence]) ).
cnf(c3132,plain,
( ~ product(X1138,X1137,X1136)
| ~ product(e_4,e_3,X1136)
| ~ product(e_2,X1137,X1138)
| equalish(X1137,e_3) ),
inference(resolution,[status(thm)],[c3117,qg1_2]) ).
cnf(c3758,plain,
( equalish(e_4,e_3)
| ~ product(e_1,e_4,X1425)
| ~ product(e_4,e_3,X1425) ),
inference(resolution,[status(thm)],[c3745,c3132]) ).
cnf(c3786,plain,
( equalish(e_4,e_3)
| ~ product(e_1,e_4,e_1) ),
inference(resolution,[status(thm)],[c3758,c3344]) ).
cnf(c3779,plain,
( ~ product(e_2,e_4,X1412)
| equalish(X1412,e_1) ),
inference(resolution,[status(thm)],[c3768,product_total_function2]) ).
cnf(c3775,plain,
( ~ product(e_2,X1411,e_1)
| equalish(X1411,e_4) ),
inference(resolution,[status(thm)],[c3768,product_right_cancellation]) ).
cnf(c3774,plain,
( ~ product(X1407,e_4,e_1)
| equalish(X1407,e_2) ),
inference(resolution,[status(thm)],[c3768,product_left_cancellation]) ).
cnf(c3595,plain,
( ~ product(e_1,e_1,X1343)
| ~ product(e_3,e_4,X1343)
| equalish(e_1,e_4) ),
inference(resolution,[status(thm)],[c3556,product_idempotence]) ).
cnf(c3593,plain,
( ~ product(e_1,X1342,e_1)
| ~ product(e_3,e_4,e_1)
| equalish(X1342,e_4) ),
inference(factor,[status(thm)],[c3556]) ).
cnf(c3575,plain,
( ~ product(e_1,X1336,e_1)
| ~ product(e_3,e_4,e_1)
| equalish(e_1,e_3) ),
inference(factor,[status(thm)],[c3555]) ).
cnf(c3577,plain,
( ~ product(e_1,e_1,X1333)
| ~ product(e_3,e_4,X1333)
| equalish(e_1,e_3) ),
inference(resolution,[status(thm)],[c3555,product_idempotence]) ).
cnf(c2927,plain,
( ~ product(X1030,X1029,X1028)
| ~ product(e_2,e_3,X1028)
| ~ product(e_1,X1029,X1030)
| equalish(X1030,e_2) ),
inference(resolution,[status(thm)],[c2917,qg1_1]) ).
cnf(c3553,plain,
( ~ product(e_3,e_4,X1323)
| ~ product(e_2,e_3,X1323)
| equalish(e_3,e_2) ),
inference(resolution,[status(thm)],[c3543,c2927]) ).
cnf(c3573,plain,
( ~ product(e_3,e_4,e_4)
| equalish(e_3,e_2) ),
inference(resolution,[status(thm)],[c3553,c3117]) ).
cnf(c3551,plain,
( ~ product(e_3,e_4,e_1)
| ~ product(e_1,X1321,e_1)
| equalish(e_4,X1321) ),
inference(resolution,[status(thm)],[c3543,c71]) ).
cnf(c2504,plain,
( ~ product(X818,X817,X816)
| ~ product(e_4,e_2,X816)
| ~ product(e_1,X817,X818)
| equalish(X818,e_4) ),
inference(resolution,[status(thm)],[c2480,qg1_1]) ).
cnf(c3546,plain,
( ~ product(e_3,e_4,X1318)
| ~ product(e_4,e_2,X1318)
| equalish(e_3,e_4) ),
inference(resolution,[status(thm)],[c3543,c2504]) ).
cnf(c3568,plain,
( ~ product(e_3,e_4,e_3)
| equalish(e_3,e_4) ),
inference(resolution,[status(thm)],[c3546,c2744]) ).
cnf(c3545,plain,
( ~ product(e_3,e_4,X1317)
| ~ product(e_1,e_1,X1317)
| equalish(e_4,e_1) ),
inference(resolution,[status(thm)],[c3543,c73]) ).
cnf(c3566,plain,
( ~ product(e_3,e_4,e_1)
| equalish(e_4,e_1) ),
inference(resolution,[status(thm)],[c3545,product_idempotence]) ).
cnf(c3544,plain,
( ~ product(e_3,e_4,X1315)
| ~ product(e_1,e_1,X1315)
| equalish(e_3,e_1) ),
inference(resolution,[status(thm)],[c3543,c57]) ).
cnf(c3564,plain,
( ~ product(e_3,e_4,e_1)
| equalish(e_3,e_1) ),
inference(resolution,[status(thm)],[c3544,product_idempotence]) ).
cnf(c3538,plain,
( equalish(e_4,e_2)
| ~ product(e_3,e_4,X1314)
| ~ product(e_4,e_2,X1314) ),
inference(resolution,[status(thm)],[c3516,c2505]) ).
cnf(c3562,plain,
( equalish(e_4,e_2)
| ~ product(e_3,e_4,e_3) ),
inference(resolution,[status(thm)],[c3538,c2744]) ).
cnf(c3554,plain,
( ~ product(e_1,e_4,X1299)
| equalish(X1299,e_3) ),
inference(resolution,[status(thm)],[c3543,product_total_function2]) ).
cnf(c3549,plain,
( ~ product(e_1,X1298,e_3)
| equalish(X1298,e_4) ),
inference(resolution,[status(thm)],[c3543,product_right_cancellation]) ).
cnf(c3361,plain,
( ~ product(X1234,X1233,X1232)
| ~ product(e_1,e_3,X1232)
| ~ product(e_4,X1233,X1234)
| equalish(X1233,e_3) ),
inference(resolution,[status(thm)],[c3344,qg1_2]) ).
cnf(c3384,plain,
( ~ product(e_2,e_1,X1243)
| ~ product(e_1,e_3,X1243)
| equalish(e_1,e_3) ),
inference(resolution,[status(thm)],[c3361,c2142]) ).
cnf(c3387,plain,
( ~ product(e_2,e_1,e_2)
| equalish(e_1,e_3) ),
inference(resolution,[status(thm)],[c3384,c2917]) ).
cnf(c3382,plain,
( ~ product(e_3,e_2,X1239)
| ~ product(e_1,e_3,X1239)
| equalish(e_2,e_3) ),
inference(resolution,[status(thm)],[c3361,c2744]) ).
cnf(c3386,plain,
( ~ product(e_3,e_2,e_2)
| equalish(e_2,e_3) ),
inference(resolution,[status(thm)],[c3382,c2917]) ).
cnf(c3381,plain,
( ~ product(e_4,e_4,X1238)
| ~ product(e_1,e_3,X1238)
| equalish(e_4,e_3) ),
inference(resolution,[status(thm)],[c3361,product_idempotence]) ).
cnf(c3380,plain,
( ~ product(e_4,X1237,e_4)
| ~ product(e_1,e_3,e_4)
| equalish(X1237,e_3) ),
inference(factor,[status(thm)],[c3361]) ).
cnf(c3360,plain,
( ~ product(X1224,X1223,X1222)
| ~ product(e_1,e_3,X1222)
| ~ product(e_4,X1223,X1224)
| equalish(X1224,e_1) ),
inference(resolution,[status(thm)],[c3344,qg1_1]) ).
cnf(c3372,plain,
( ~ product(e_4,X1231,e_4)
| ~ product(e_1,e_3,e_4)
| equalish(e_4,e_1) ),
inference(factor,[status(thm)],[c3360]) ).
cnf(c3376,plain,
( ~ product(e_2,e_1,X1230)
| ~ product(e_1,e_3,X1230)
| equalish(e_2,e_1) ),
inference(resolution,[status(thm)],[c3360,c2142]) ).
cnf(c3379,plain,
( ~ product(e_2,e_1,e_2)
| equalish(e_2,e_1) ),
inference(resolution,[status(thm)],[c3376,c2917]) ).
cnf(c3374,plain,
( ~ product(e_3,e_2,X1228)
| ~ product(e_1,e_3,X1228)
| equalish(e_3,e_1) ),
inference(resolution,[status(thm)],[c3360,c2744]) ).
cnf(c3378,plain,
( ~ product(e_3,e_2,e_2)
| equalish(e_3,e_1) ),
inference(resolution,[status(thm)],[c3374,c2917]) ).
cnf(c3373,plain,
( ~ product(e_4,e_4,X1227)
| ~ product(e_1,e_3,X1227)
| equalish(e_4,e_1) ),
inference(resolution,[status(thm)],[c3360,product_idempotence]) ).
cnf(c3356,plain,
( ~ product(e_1,e_3,e_4)
| ~ product(e_4,X1214,e_4)
| equalish(e_3,X1214) ),
inference(resolution,[status(thm)],[c3344,c71]) ).
cnf(c2155,plain,
( ~ product(X648,X647,X646)
| ~ product(e_2,e_1,X646)
| ~ product(e_4,X647,X648)
| equalish(X647,e_1) ),
inference(resolution,[status(thm)],[c2142,qg1_2]) ).
cnf(c3355,plain,
( ~ product(e_1,e_3,X1212)
| ~ product(e_2,e_1,X1212)
| equalish(e_3,e_1) ),
inference(resolution,[status(thm)],[c3344,c2155]) ).
cnf(c3370,plain,
( ~ product(e_1,e_3,e_3)
| equalish(e_3,e_1) ),
inference(resolution,[status(thm)],[c3355,c1738]) ).
cnf(c2756,plain,
( ~ product(X926,X925,X924)
| ~ product(e_3,e_2,X924)
| ~ product(e_4,X925,X926)
| equalish(X926,e_3) ),
inference(resolution,[status(thm)],[c2744,qg1_1]) ).
cnf(c3350,plain,
( ~ product(e_1,e_3,X1211)
| ~ product(e_3,e_2,X1211)
| equalish(e_1,e_3) ),
inference(resolution,[status(thm)],[c3344,c2756]) ).
cnf(c3369,plain,
( ~ product(e_1,e_3,e_1)
| equalish(e_1,e_3) ),
inference(resolution,[status(thm)],[c3350,c2461]) ).
cnf(c2151,plain,
( ~ product(X639,X638,X637)
| ~ product(e_2,e_1,X637)
| ~ product(e_4,X638,X639)
| equalish(X639,e_2) ),
inference(resolution,[status(thm)],[c2142,qg1_1]) ).
cnf(c3349,plain,
( ~ product(e_1,e_3,X1210)
| ~ product(e_2,e_1,X1210)
| equalish(e_1,e_2) ),
inference(resolution,[status(thm)],[c3344,c2151]) ).
cnf(c3368,plain,
( ~ product(e_1,e_3,e_3)
| equalish(e_1,e_2) ),
inference(resolution,[status(thm)],[c3349,c1738]) ).
cnf(c3346,plain,
( ~ product(e_1,e_3,X1208)
| ~ product(e_4,e_4,X1208)
| equalish(e_3,e_4) ),
inference(resolution,[status(thm)],[c3344,c73]) ).
cnf(c3367,plain,
( ~ product(e_1,e_3,e_4)
| equalish(e_3,e_4) ),
inference(resolution,[status(thm)],[c3346,product_idempotence]) ).
cnf(c3345,plain,
( ~ product(e_1,e_3,X1207)
| ~ product(e_4,e_4,X1207)
| equalish(e_1,e_4) ),
inference(resolution,[status(thm)],[c3344,c57]) ).
cnf(c3366,plain,
( ~ product(e_1,e_3,e_4)
| equalish(e_1,e_4) ),
inference(resolution,[status(thm)],[c3345,product_idempotence]) ).
cnf(c2757,plain,
( ~ product(X934,X933,X932)
| ~ product(e_3,e_2,X932)
| ~ product(e_4,X933,X934)
| equalish(X933,e_2) ),
inference(resolution,[status(thm)],[c2744,qg1_2]) ).
cnf(c3339,plain,
( equalish(e_3,e_2)
| ~ product(e_1,e_3,X1205)
| ~ product(e_3,e_2,X1205) ),
inference(resolution,[status(thm)],[c3318,c2757]) ).
cnf(c3365,plain,
( equalish(e_3,e_2)
| ~ product(e_1,e_3,e_1) ),
inference(resolution,[status(thm)],[c3339,c2461]) ).
cnf(c3152,plain,
( ~ product(e_3,e_1,X1133)
| ~ product(e_4,e_3,X1133)
| equalish(e_3,e_4) ),
inference(resolution,[status(thm)],[c3131,c1738]) ).
cnf(c3354,plain,
( ~ product(e_3,e_1,e_1)
| equalish(e_3,e_4) ),
inference(resolution,[status(thm)],[c3344,c3152]) ).
cnf(c3169,plain,
( ~ product(e_3,e_1,X1141)
| ~ product(e_4,e_3,X1141)
| equalish(e_1,e_3) ),
inference(resolution,[status(thm)],[c3132,c1738]) ).
cnf(c3347,plain,
( ~ product(e_3,e_1,e_1)
| equalish(e_1,e_3) ),
inference(resolution,[status(thm)],[c3344,c3169]) ).
cnf(c3359,plain,
( ~ product(e_4,e_3,X1185)
| equalish(X1185,e_1) ),
inference(resolution,[status(thm)],[c3344,product_total_function2]) ).
cnf(c3352,plain,
( ~ product(e_4,X1184,e_1)
| equalish(X1184,e_3) ),
inference(resolution,[status(thm)],[c3344,product_right_cancellation]) ).
cnf(c3351,plain,
( ~ product(X1182,e_3,e_1)
| equalish(X1182,e_4) ),
inference(resolution,[status(thm)],[c3344,product_left_cancellation]) ).
cnf(c3170,plain,
( ~ product(e_2,e_2,X1142)
| ~ product(e_4,e_3,X1142)
| equalish(e_2,e_3) ),
inference(resolution,[status(thm)],[c3132,product_idempotence]) ).
cnf(c3165,plain,
( ~ product(e_2,X1140,e_2)
| ~ product(e_4,e_3,e_2)
| equalish(X1140,e_3) ),
inference(factor,[status(thm)],[c3132]) ).
cnf(c3148,plain,
( ~ product(e_2,X1135,e_2)
| ~ product(e_4,e_3,e_2)
| equalish(e_2,e_4) ),
inference(factor,[status(thm)],[c3131]) ).
cnf(c3153,plain,
( ~ product(e_2,e_2,X1134)
| ~ product(e_4,e_3,X1134)
| equalish(e_2,e_4) ),
inference(resolution,[status(thm)],[c3131,product_idempotence]) ).
cnf(c3129,plain,
( ~ product(e_4,e_3,e_2)
| ~ product(e_2,X1124,e_2)
| equalish(e_3,X1124) ),
inference(resolution,[status(thm)],[c3117,c71]) ).
cnf(c3118,plain,
( ~ product(e_4,e_3,X1119)
| ~ product(e_2,e_2,X1119)
| equalish(e_4,e_2) ),
inference(resolution,[status(thm)],[c3117,c57]) ).
cnf(c3140,plain,
( ~ product(e_4,e_3,e_2)
| equalish(e_4,e_2) ),
inference(resolution,[status(thm)],[c3118,product_idempotence]) ).
cnf(c3107,plain,
( equalish(e_3,e_1)
| ~ product(e_4,e_3,X1115)
| ~ product(e_3,e_1,X1115) ),
inference(resolution,[status(thm)],[c3074,c1753]) ).
cnf(c3138,plain,
( equalish(e_3,e_1)
| ~ product(e_4,e_3,e_4) ),
inference(resolution,[status(thm)],[c3107,c1946]) ).
cnf(c2949,plain,
( ~ product(e_4,e_2,X1034)
| ~ product(e_2,e_3,X1034)
| equalish(e_4,e_2) ),
inference(resolution,[status(thm)],[c2927,c2480]) ).
cnf(c3126,plain,
( ~ product(e_4,e_2,e_4)
| equalish(e_4,e_2) ),
inference(resolution,[status(thm)],[c3117,c2949]) ).
cnf(c2966,plain,
( ~ product(e_4,e_2,X1043)
| ~ product(e_2,e_3,X1043)
| equalish(e_2,e_3) ),
inference(resolution,[status(thm)],[c2928,c2480]) ).
cnf(c3121,plain,
( ~ product(e_4,e_2,e_4)
| equalish(e_2,e_3) ),
inference(resolution,[status(thm)],[c3117,c2966]) ).
cnf(c3130,plain,
( ~ product(e_2,e_3,X1100)
| equalish(X1100,e_4) ),
inference(resolution,[status(thm)],[c3117,product_total_function2]) ).
cnf(c3125,plain,
( ~ product(X1095,e_3,e_4)
| equalish(X1095,e_2) ),
inference(resolution,[status(thm)],[c3117,product_left_cancellation]) ).
cnf(c2965,plain,
( ~ product(e_1,e_1,X1042)
| ~ product(e_2,e_3,X1042)
| equalish(e_1,e_3) ),
inference(resolution,[status(thm)],[c2928,product_idempotence]) ).
cnf(c2962,plain,
( ~ product(e_1,X1041,e_1)
| ~ product(e_2,e_3,e_1)
| equalish(X1041,e_3) ),
inference(factor,[status(thm)],[c2928]) ).
cnf(c2945,plain,
( ~ product(e_1,X1035,e_1)
| ~ product(e_2,e_3,e_1)
| equalish(e_1,e_2) ),
inference(factor,[status(thm)],[c2927]) ).
cnf(c2948,plain,
( ~ product(e_1,e_1,X1033)
| ~ product(e_2,e_3,X1033)
| equalish(e_1,e_2) ),
inference(resolution,[status(thm)],[c2927,product_idempotence]) ).
cnf(c2924,plain,
( ~ product(e_2,e_3,e_1)
| ~ product(e_1,X1024,e_1)
| equalish(e_3,X1024) ),
inference(resolution,[status(thm)],[c2917,c71]) ).
cnf(c2920,plain,
( ~ product(e_2,e_3,X1023)
| ~ product(e_4,e_2,X1023)
| equalish(e_2,e_4) ),
inference(resolution,[status(thm)],[c2917,c2504]) ).
cnf(c2941,plain,
( ~ product(e_2,e_3,e_3)
| equalish(e_2,e_4) ),
inference(resolution,[status(thm)],[c2920,c2744]) ).
cnf(c2918,plain,
( ~ product(e_2,e_3,X1018)
| ~ product(e_1,e_1,X1018)
| equalish(e_2,e_1) ),
inference(resolution,[status(thm)],[c2917,c57]) ).
cnf(c2937,plain,
( ~ product(e_2,e_3,e_1)
| equalish(e_2,e_1) ),
inference(resolution,[status(thm)],[c2918,product_idempotence]) ).
cnf(c2926,plain,
( ~ product(e_1,e_3,X1004)
| equalish(X1004,e_2) ),
inference(resolution,[status(thm)],[c2917,product_total_function2]) ).
cnf(c2921,plain,
( ~ product(X1002,e_3,e_2)
| equalish(X1002,e_1) ),
inference(resolution,[status(thm)],[c2917,product_left_cancellation]) ).
cnf(c2784,plain,
( ~ product(e_2,e_1,X940)
| ~ product(e_3,e_2,X940)
| equalish(e_1,e_2) ),
inference(resolution,[status(thm)],[c2757,c2142]) ).
cnf(c2787,plain,
( ~ product(e_2,e_1,e_1)
| equalish(e_1,e_2) ),
inference(resolution,[status(thm)],[c2784,c2461]) ).
cnf(c2781,plain,
( ~ product(e_4,e_4,X939)
| ~ product(e_3,e_2,X939)
| equalish(e_4,e_2) ),
inference(resolution,[status(thm)],[c2757,product_idempotence]) ).
cnf(c2778,plain,
( ~ product(e_4,X936,e_4)
| ~ product(e_3,e_2,e_4)
| equalish(X936,e_2) ),
inference(factor,[status(thm)],[c2757]) ).
cnf(c2768,plain,
( ~ product(e_4,X931,e_4)
| ~ product(e_3,e_2,e_4)
| equalish(e_4,e_3) ),
inference(factor,[status(thm)],[c2756]) ).
cnf(c2774,plain,
( ~ product(e_2,e_1,X929)
| ~ product(e_3,e_2,X929)
| equalish(e_2,e_3) ),
inference(resolution,[status(thm)],[c2756,c2142]) ).
cnf(c2777,plain,
( ~ product(e_2,e_1,e_1)
| equalish(e_2,e_3) ),
inference(resolution,[status(thm)],[c2774,c2461]) ).
cnf(c2771,plain,
( ~ product(e_4,e_4,X928)
| ~ product(e_3,e_2,X928)
| equalish(e_4,e_3) ),
inference(resolution,[status(thm)],[c2756,product_idempotence]) ).
cnf(c2753,plain,
( ~ product(e_3,e_2,e_4)
| ~ product(e_4,X918,e_4)
| equalish(e_2,X918) ),
inference(resolution,[status(thm)],[c2744,c71]) ).
cnf(c2752,plain,
( ~ product(e_3,e_2,X917)
| ~ product(e_2,e_1,X917)
| equalish(e_2,e_1) ),
inference(resolution,[status(thm)],[c2744,c2155]) ).
cnf(c2765,plain,
( ~ product(e_3,e_2,e_3)
| equalish(e_2,e_1) ),
inference(resolution,[status(thm)],[c2752,c1738]) ).
cnf(c2748,plain,
( ~ product(e_3,e_2,X915)
| ~ product(e_2,e_1,X915)
| equalish(e_3,e_2) ),
inference(resolution,[status(thm)],[c2744,c2151]) ).
cnf(c2764,plain,
( ~ product(e_3,e_2,e_3)
| equalish(e_3,e_2) ),
inference(resolution,[status(thm)],[c2748,c1738]) ).
cnf(c2746,plain,
( ~ product(e_3,e_2,X914)
| ~ product(e_4,e_4,X914)
| equalish(e_2,e_4) ),
inference(resolution,[status(thm)],[c2744,c73]) ).
cnf(c2763,plain,
( ~ product(e_3,e_2,e_4)
| equalish(e_2,e_4) ),
inference(resolution,[status(thm)],[c2746,product_idempotence]) ).
cnf(c2745,plain,
( ~ product(e_3,e_2,X913)
| ~ product(e_4,e_4,X913)
| equalish(e_3,e_4) ),
inference(resolution,[status(thm)],[c2744,c57]) ).
cnf(c2762,plain,
( ~ product(e_3,e_2,e_4)
| equalish(e_3,e_4) ),
inference(resolution,[status(thm)],[c2745,product_idempotence]) ).
cnf(c2755,plain,
( ~ product(e_4,e_2,X897)
| equalish(X897,e_3) ),
inference(resolution,[status(thm)],[c2744,product_total_function2]) ).
cnf(c2750,plain,
( ~ product(e_4,X896,e_3)
| equalish(X896,e_2) ),
inference(resolution,[status(thm)],[c2744,product_right_cancellation]) ).
cnf(c2749,plain,
( ~ product(X894,e_2,e_3)
| equalish(X894,e_4) ),
inference(resolution,[status(thm)],[c2744,product_left_cancellation]) ).
cnf(c2565,plain,
( ~ product(e_1,e_1,X829)
| ~ product(e_4,e_2,X829)
| equalish(e_1,e_2) ),
inference(resolution,[status(thm)],[c2505,product_idempotence]) ).
cnf(c2561,plain,
( ~ product(e_1,X828,e_1)
| ~ product(e_4,e_2,e_1)
| equalish(X828,e_2) ),
inference(factor,[status(thm)],[c2505]) ).
cnf(c2545,plain,
( ~ product(e_1,X823,e_1)
| ~ product(e_4,e_2,e_1)
| equalish(e_1,e_4) ),
inference(factor,[status(thm)],[c2504]) ).
cnf(c2549,plain,
( ~ product(e_1,e_1,X820)
| ~ product(e_4,e_2,X820)
| equalish(e_1,e_4) ),
inference(resolution,[status(thm)],[c2504,product_idempotence]) ).
cnf(c2540,plain,
( ~ product(e_4,e_1,X815)
| ~ product(e_1,e_2,X815)
| equalish(e_1,e_2) ),
inference(resolution,[status(thm)],[c2474,c1946]) ).
cnf(c2544,plain,
( ~ product(e_4,e_1,e_4)
| equalish(e_1,e_2) ),
inference(resolution,[status(thm)],[c2540,c2480]) ).
cnf(c2538,plain,
( ~ product(e_3,e_3,X813)
| ~ product(e_1,e_2,X813)
| equalish(e_3,e_2) ),
inference(resolution,[status(thm)],[c2474,product_idempotence]) ).
cnf(c2535,plain,
( ~ product(e_3,X812,e_3)
| ~ product(e_1,e_2,e_3)
| equalish(X812,e_2) ),
inference(factor,[status(thm)],[c2474]) ).
cnf(c2525,plain,
( ~ product(e_3,X806,e_3)
| ~ product(e_1,e_2,e_3)
| equalish(e_3,e_1) ),
inference(factor,[status(thm)],[c2473]) ).
cnf(c2530,plain,
( ~ product(e_4,e_1,X805)
| ~ product(e_1,e_2,X805)
| equalish(e_4,e_1) ),
inference(resolution,[status(thm)],[c2473,c1946]) ).
cnf(c2534,plain,
( ~ product(e_4,e_1,e_4)
| equalish(e_4,e_1) ),
inference(resolution,[status(thm)],[c2530,c2480]) ).
cnf(c2528,plain,
( ~ product(e_3,e_3,X804)
| ~ product(e_1,e_2,X804)
| equalish(e_3,e_1) ),
inference(resolution,[status(thm)],[c2473,product_idempotence]) ).
cnf(c2502,plain,
( ~ product(e_4,e_2,e_1)
| ~ product(e_1,X794,e_1)
| equalish(e_2,X794) ),
inference(resolution,[status(thm)],[c2480,c71]) ).
cnf(c2494,plain,
( ~ product(e_4,e_2,X791)
| ~ product(e_1,e_1,X791)
| equalish(e_4,e_1) ),
inference(resolution,[status(thm)],[c2480,c57]) ).
cnf(c2520,plain,
( ~ product(e_4,e_2,e_1)
| equalish(e_4,e_1) ),
inference(resolution,[status(thm)],[c2494,product_idempotence]) ).
cnf(c2470,plain,
( ~ product(e_1,e_2,e_3)
| ~ product(e_3,X787,e_3)
| equalish(e_2,X787) ),
inference(resolution,[status(thm)],[c2461,c71]) ).
cnf(c2465,plain,
( ~ product(e_1,e_2,X786)
| ~ product(e_4,e_1,X786)
| equalish(e_1,e_4) ),
inference(resolution,[status(thm)],[c2461,c1955]) ).
cnf(c2515,plain,
( ~ product(e_1,e_2,e_2)
| equalish(e_1,e_4) ),
inference(resolution,[status(thm)],[c2465,c2142]) ).
cnf(c2463,plain,
( ~ product(e_1,e_2,X783)
| ~ product(e_3,e_3,X783)
| equalish(e_2,e_3) ),
inference(resolution,[status(thm)],[c2461,c73]) ).
cnf(c2514,plain,
( ~ product(e_1,e_2,e_3)
| equalish(e_2,e_3) ),
inference(resolution,[status(thm)],[c2463,product_idempotence]) ).
cnf(c2462,plain,
( ~ product(e_1,e_2,X782)
| ~ product(e_3,e_3,X782)
| equalish(e_1,e_3) ),
inference(resolution,[status(thm)],[c2461,c57]) ).
cnf(c2513,plain,
( ~ product(e_1,e_2,e_3)
| equalish(e_1,e_3) ),
inference(resolution,[status(thm)],[c2462,product_idempotence]) ).
cnf(c2450,plain,
( equalish(e_2,e_1)
| ~ product(e_1,e_2,X778)
| ~ product(e_4,e_1,X778) ),
inference(resolution,[status(thm)],[c2446,c1959]) ).
cnf(c2512,plain,
( equalish(e_2,e_1)
| ~ product(e_1,e_2,e_2) ),
inference(resolution,[status(thm)],[c2450,c2142]) ).
cnf(c2503,plain,
( ~ product(e_1,e_2,X760)
| equalish(X760,e_4) ),
inference(resolution,[status(thm)],[c2480,product_total_function2]) ).
cnf(c2472,plain,
( ~ product(e_3,e_2,X754)
| equalish(X754,e_1) ),
inference(resolution,[status(thm)],[c2461,product_total_function2]) ).
cnf(c2466,plain,
( ~ product(X752,e_2,e_1)
| equalish(X752,e_3) ),
inference(resolution,[status(thm)],[c2461,product_left_cancellation]) ).
cnf(c2181,plain,
( ~ product(e_4,e_4,X652)
| ~ product(e_2,e_1,X652)
| equalish(e_4,e_1) ),
inference(resolution,[status(thm)],[c2155,product_idempotence]) ).
cnf(c2178,plain,
( ~ product(e_4,X651,e_4)
| ~ product(e_2,e_1,e_4)
| equalish(X651,e_1) ),
inference(factor,[status(thm)],[c2155]) ).
cnf(c2166,plain,
( ~ product(e_4,X645,e_4)
| ~ product(e_2,e_1,e_4)
| equalish(e_4,e_2) ),
inference(factor,[status(thm)],[c2151]) ).
cnf(c2169,plain,
( ~ product(e_4,e_4,X644)
| ~ product(e_2,e_1,X644)
| equalish(e_4,e_2) ),
inference(resolution,[status(thm)],[c2151,product_idempotence]) ).
cnf(c2152,plain,
( ~ product(e_2,e_1,e_4)
| ~ product(e_4,X635,e_4)
| equalish(e_1,X635) ),
inference(resolution,[status(thm)],[c2142,c71]) ).
cnf(c2149,plain,
( ~ cycle(e_4,X633)
| ~ greater(X633,e_0)
| ~ next(e_4,X634)
| equalish(e_2,X634) ),
inference(resolution,[status(thm)],[c2142,cycle7]) ).
cnf(c2147,plain,
( ~ product(e_2,e_1,X631)
| ~ product(e_4,e_4,X631)
| equalish(e_1,e_4) ),
inference(resolution,[status(thm)],[c2142,c73]) ).
cnf(c2162,plain,
( ~ product(e_2,e_1,e_4)
| equalish(e_1,e_4) ),
inference(resolution,[status(thm)],[c2147,product_idempotence]) ).
cnf(c2144,plain,
( ~ product(e_2,e_1,X630)
| ~ product(e_4,e_4,X630)
| equalish(e_2,e_4) ),
inference(resolution,[status(thm)],[c2142,c57]) ).
cnf(c2161,plain,
( ~ product(e_2,e_1,e_4)
| equalish(e_2,e_4) ),
inference(resolution,[status(thm)],[c2144,product_idempotence]) ).
cnf(c2154,plain,
( ~ cycle(e_4,e_0)
| ~ greater(e_2,e_4) ),
inference(resolution,[status(thm)],[c2142,cycle6]) ).
cnf(c2150,plain,
( ~ product(e_4,e_1,X623)
| equalish(X623,e_2) ),
inference(resolution,[status(thm)],[c2142,product_total_function2]) ).
cnf(c2146,plain,
( ~ product(e_4,X622,e_2)
| equalish(X622,e_1) ),
inference(resolution,[status(thm)],[c2142,product_right_cancellation]) ).
cnf(c2143,plain,
( ~ product(X618,e_1,e_2)
| equalish(X618,e_4) ),
inference(resolution,[status(thm)],[c2142,product_left_cancellation]) ).
cnf(c1996,plain,
( ~ product(e_3,e_3,X578)
| ~ product(e_4,e_1,X578)
| equalish(e_3,e_1) ),
inference(resolution,[status(thm)],[c1959,product_idempotence]) ).
cnf(c1991,plain,
( ~ product(e_3,X576,e_3)
| ~ product(e_4,e_1,e_3)
| equalish(X576,e_1) ),
inference(factor,[status(thm)],[c1959]) ).
cnf(c1975,plain,
( ~ product(e_3,X571,e_3)
| ~ product(e_4,e_1,e_3)
| equalish(e_3,e_4) ),
inference(factor,[status(thm)],[c1955]) ).
cnf(c1980,plain,
( ~ product(e_3,e_3,X570)
| ~ product(e_4,e_1,X570)
| equalish(e_3,e_4) ),
inference(resolution,[status(thm)],[c1955,product_idempotence]) ).
cnf(c1956,plain,
( ~ product(e_4,e_1,e_3)
| ~ product(e_3,X560,e_3)
| equalish(e_1,X560) ),
inference(resolution,[status(thm)],[c1946,c71]) ).
cnf(c1953,plain,
( ~ cycle(e_3,X557)
| ~ greater(X557,e_0)
| ~ next(e_3,X558)
| equalish(e_4,X558) ),
inference(resolution,[status(thm)],[c1946,cycle7]) ).
cnf(c1951,plain,
( ~ product(e_4,e_1,X555)
| ~ product(e_3,e_3,X555)
| equalish(e_1,e_3) ),
inference(resolution,[status(thm)],[c1946,c73]) ).
cnf(c1969,plain,
( ~ product(e_4,e_1,e_3)
| equalish(e_1,e_3) ),
inference(resolution,[status(thm)],[c1951,product_idempotence]) ).
cnf(e_4_greater_e_3,axiom,
greater(e_4,e_3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_4_greater_e_3) ).
cnf(c1958,plain,
( ~ cycle(e_3,e_0)
| ~ greater(e_4,e_3) ),
inference(resolution,[status(thm)],[c1946,cycle6]) ).
cnf(c1966,plain,
~ cycle(e_3,e_0),
inference(resolution,[status(thm)],[c1958,e_4_greater_e_3]) ).
cnf(c1954,plain,
( ~ product(e_3,e_1,X546)
| equalish(X546,e_4) ),
inference(resolution,[status(thm)],[c1946,product_total_function2]) ).
cnf(c1801,plain,
( ~ product(e_2,e_2,X511)
| ~ product(e_3,e_1,X511)
| equalish(e_2,e_1) ),
inference(resolution,[status(thm)],[c1753,product_idempotence]) ).
cnf(c1797,plain,
( ~ product(e_2,X510,e_2)
| ~ product(e_3,e_1,e_2)
| equalish(X510,e_1) ),
inference(factor,[status(thm)],[c1753]) ).
cnf(c1781,plain,
( ~ product(e_2,X505,e_2)
| ~ product(e_3,e_1,e_2)
| equalish(e_2,e_3) ),
inference(factor,[status(thm)],[c1748]) ).
cnf(c1785,plain,
( ~ product(e_2,e_2,X503)
| ~ product(e_3,e_1,X503)
| equalish(e_2,e_3) ),
inference(resolution,[status(thm)],[c1748,product_idempotence]) ).
cnf(c1749,plain,
( ~ product(e_3,e_1,e_2)
| ~ product(e_2,X494,e_2)
| equalish(e_1,X494) ),
inference(resolution,[status(thm)],[c1738,c71]) ).
cnf(c1746,plain,
( ~ cycle(e_2,X491)
| ~ greater(X491,e_0)
| ~ next(e_2,X492)
| equalish(e_3,X492) ),
inference(resolution,[status(thm)],[c1738,cycle7]) ).
cnf(c1743,plain,
( ~ product(e_3,e_1,X490)
| ~ product(e_2,e_2,X490)
| equalish(e_1,e_2) ),
inference(resolution,[status(thm)],[c1738,c73]) ).
cnf(c1775,plain,
( ~ product(e_3,e_1,e_2)
| equalish(e_1,e_2) ),
inference(resolution,[status(thm)],[c1743,product_idempotence]) ).
cnf(c1752,plain,
( ~ cycle(e_2,e_0)
| ~ greater(e_3,e_2) ),
inference(resolution,[status(thm)],[c1738,cycle6]) ).
cnf(c1772,plain,
~ cycle(e_2,e_0),
inference(resolution,[status(thm)],[c1752,e_3_greater_e_2]) ).
cnf(c1747,plain,
( ~ product(e_2,e_1,X480)
| equalish(X480,e_3) ),
inference(resolution,[status(thm)],[c1738,product_total_function2]) ).
cnf(c1741,plain,
( ~ product(e_2,X479,e_3)
| equalish(X479,e_1) ),
inference(resolution,[status(thm)],[c1738,product_right_cancellation]) ).
cnf(c34,plain,
( ~ cycle(e_1,X57)
| ~ greater(X57,e_0)
| ~ next(e_1,X58)
| equalish(e_1,X58) ),
inference(resolution,[status(thm)],[cycle7,product_idempotence]) ).
cnf(c36,plain,
( ~ cycle(e_1,X59)
| ~ greater(X59,e_0)
| equalish(e_1,e_2) ),
inference(resolution,[status(thm)],[c34,e_1_then_e_2]) ).
cnf(c40,plain,
( ~ cycle(e_1,e_3)
| equalish(e_1,e_2) ),
inference(resolution,[status(thm)],[c36,e_3_greater_e_0]) ).
cnf(c39,plain,
( ~ cycle(e_1,e_2)
| equalish(e_1,e_2) ),
inference(resolution,[status(thm)],[c36,e_2_greater_e_0]) ).
cnf(c37,plain,
( ~ cycle(e_1,e_1)
| equalish(e_1,e_2) ),
inference(resolution,[status(thm)],[c36,e_1_greater_e_0]) ).
cnf(c2,plain,
( cycle(e_1,e_0)
| cycle(e_1,e_1)
| cycle(e_1,e_2)
| cycle(e_1,e_3) ),
inference(resolution,[status(thm)],[cycle2,element_1]) ).
cnf(c76,plain,
( cycle(e_1,e_0)
| cycle(e_1,e_2)
| cycle(e_1,e_3)
| equalish(e_1,e_2) ),
inference(resolution,[status(thm)],[c2,c37]) ).
cnf(c371,plain,
( cycle(e_1,e_0)
| cycle(e_1,e_3)
| equalish(e_1,e_2) ),
inference(resolution,[status(thm)],[c76,c39]) ).
cnf(c392,plain,
( cycle(e_1,e_0)
| equalish(e_1,e_2) ),
inference(resolution,[status(thm)],[c371,c40]) ).
cnf(c403,plain,
cycle(e_1,e_0),
inference(resolution,[status(thm)],[c392,e_1_is_not_e_2]) ).
cnf(c18,plain,
( ~ cycle(X170,e_4)
| ~ cycle(X171,e_0)
| ~ cycle(X169,e_2)
| ~ next(X171,X169)
| ~ greater(X171,X170) ),
inference(resolution,[status(thm)],[cycle5,e_4_greater_e_2]) ).
cnf(c172,plain,
( ~ cycle(e_0,e_4)
| ~ cycle(e_1,e_0)
| ~ cycle(X250,e_2)
| ~ next(e_1,X250) ),
inference(resolution,[status(thm)],[c18,e_1_greater_e_0]) ).
cnf(c410,plain,
( ~ cycle(e_0,e_4)
| ~ cycle(e_1,e_0)
| ~ cycle(e_2,e_2) ),
inference(resolution,[status(thm)],[c172,e_1_then_e_2]) ).
cnf(c1674,plain,
( ~ cycle(e_0,e_4)
| ~ cycle(e_1,e_0) ),
inference(resolution,[status(thm)],[c1667,c410]) ).
cnf(c1677,plain,
~ cycle(e_0,e_4),
inference(resolution,[status(thm)],[c1674,c403]) ).
cnf(e_4_greater_e_0,axiom,
greater(e_4,e_0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_4_greater_e_0) ).
cnf(c8,plain,
( ~ cycle(X119,X118)
| ~ cycle(X117,e_2)
| ~ next(X119,X117)
| ~ greater(X118,e_0)
| equalish(X118,e_3) ),
inference(resolution,[status(thm)],[cycle4,e_2_then_e_3]) ).
cnf(c104,plain,
( ~ cycle(X153,e_4)
| ~ cycle(X152,e_2)
| ~ next(X153,X152)
| equalish(e_4,e_3) ),
inference(resolution,[status(thm)],[c8,e_4_greater_e_0]) ).
cnf(c130,plain,
( ~ cycle(e_1,e_4)
| ~ cycle(e_2,e_2)
| equalish(e_4,e_3) ),
inference(resolution,[status(thm)],[c104,e_1_then_e_2]) ).
cnf(c1672,plain,
( ~ cycle(e_1,e_4)
| equalish(e_4,e_3) ),
inference(resolution,[status(thm)],[c1667,c130]) ).
cnf(c105,plain,
( ~ cycle(X158,e_2)
| ~ cycle(X157,e_2)
| ~ next(X158,X157)
| equalish(e_2,e_3) ),
inference(resolution,[status(thm)],[c8,e_2_greater_e_0]) ).
cnf(c140,plain,
( ~ cycle(e_1,e_2)
| ~ cycle(e_2,e_2)
| equalish(e_2,e_3) ),
inference(resolution,[status(thm)],[c105,e_1_then_e_2]) ).
cnf(c1670,plain,
( ~ cycle(e_1,e_2)
| equalish(e_2,e_3) ),
inference(resolution,[status(thm)],[c1667,c140]) ).
cnf(c103,plain,
( ~ cycle(X148,e_1)
| ~ cycle(X147,e_2)
| ~ next(X148,X147)
| equalish(e_1,e_3) ),
inference(resolution,[status(thm)],[c8,e_1_greater_e_0]) ).
cnf(c120,plain,
( ~ cycle(e_1,e_1)
| ~ cycle(e_2,e_2)
| equalish(e_1,e_3) ),
inference(resolution,[status(thm)],[c103,e_1_then_e_2]) ).
cnf(c1669,plain,
( ~ cycle(e_1,e_1)
| equalish(e_1,e_3) ),
inference(resolution,[status(thm)],[c1667,c120]) ).
cnf(c22,plain,
( ~ cycle(X194,e_3)
| ~ cycle(X195,e_0)
| ~ cycle(X193,e_2)
| ~ next(X195,X193)
| ~ greater(X195,X194) ),
inference(resolution,[status(thm)],[cycle5,e_3_greater_e_2]) ).
cnf(c238,plain,
( ~ cycle(e_0,e_3)
| ~ cycle(e_1,e_0)
| ~ cycle(X297,e_2)
| ~ next(e_1,X297) ),
inference(resolution,[status(thm)],[c22,e_1_greater_e_0]) ).
cnf(c477,plain,
( ~ cycle(e_0,e_3)
| ~ cycle(e_1,e_0)
| ~ cycle(e_2,e_2) ),
inference(resolution,[status(thm)],[c238,e_1_then_e_2]) ).
cnf(c1668,plain,
( ~ cycle(e_0,e_3)
| ~ cycle(e_1,e_0) ),
inference(resolution,[status(thm)],[c1667,c477]) ).
cnf(c1676,plain,
~ cycle(e_0,e_3),
inference(resolution,[status(thm)],[c1668,c403]) ).
cnf(cycle1,axiom,
( ~ cycle(X4,X3)
| ~ cycle(X4,X5)
| equalish(X3,X5) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cycle1) ).
cnf(c1671,plain,
( ~ cycle(e_2,X401)
| equalish(X401,e_2) ),
inference(resolution,[status(thm)],[c1667,cycle1]) ).
cnf(c1579,plain,
( product(e_2,e_1,e_4)
| cycle(e_3,e_1) ),
inference(resolution,[status(thm)],[c1578,c946]) ).
cnf(c1586,plain,
( cycle(e_3,e_1)
| ~ cycle(e_2,e_0)
| ~ greater(e_4,e_2) ),
inference(resolution,[status(thm)],[c1579,cycle6]) ).
cnf(c1636,plain,
( cycle(e_3,e_1)
| ~ cycle(e_2,e_0) ),
inference(resolution,[status(thm)],[c1586,e_4_greater_e_2]) ).
cnf(c1637,plain,
cycle(e_3,e_1),
inference(resolution,[status(thm)],[c1636,c946]) ).
cnf(c1643,plain,
( ~ cycle(e_3,X390)
| equalish(X390,e_1) ),
inference(resolution,[status(thm)],[c1637,cycle1]) ).
cnf(e_2_greater_e_1,axiom,
greater(e_2,e_1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_2_greater_e_1) ).
cnf(c26,plain,
( ~ cycle(X212,e_2)
| ~ cycle(X213,e_0)
| ~ cycle(X211,e_1)
| ~ next(X213,X211)
| ~ greater(X213,X212) ),
inference(resolution,[status(thm)],[cycle5,e_2_greater_e_1]) ).
cnf(c304,plain,
( ~ cycle(e_3,e_2)
| ~ cycle(e_4,e_0)
| ~ cycle(X343,e_1)
| ~ next(e_4,X343) ),
inference(resolution,[status(thm)],[c26,e_4_greater_e_3]) ).
cnf(c301,plain,
( ~ cycle(e_0,e_2)
| ~ cycle(e_4,e_0)
| ~ cycle(X340,e_1)
| ~ next(e_4,X340) ),
inference(resolution,[status(thm)],[c26,e_4_greater_e_0]) ).
cnf(c300,plain,
( ~ cycle(e_0,e_2)
| ~ cycle(e_1,e_0)
| ~ cycle(X339,e_1)
| ~ next(e_1,X339) ),
inference(resolution,[status(thm)],[c26,e_1_greater_e_0]) ).
cnf(c522,plain,
( ~ cycle(e_0,e_2)
| ~ cycle(e_1,e_0)
| ~ cycle(e_2,e_1) ),
inference(resolution,[status(thm)],[c300,e_1_then_e_2]) ).
cnf(c299,plain,
( ~ cycle(e_2,e_2)
| ~ cycle(e_4,e_0)
| ~ cycle(X338,e_1)
| ~ next(e_4,X338) ),
inference(resolution,[status(thm)],[c26,e_4_greater_e_2]) ).
cnf(e_4_greater_e_1,axiom,
greater(e_4,e_1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_4_greater_e_1) ).
cnf(c298,plain,
( ~ cycle(e_1,e_2)
| ~ cycle(e_4,e_0)
| ~ cycle(X337,e_1)
| ~ next(e_4,X337) ),
inference(resolution,[status(thm)],[c26,e_4_greater_e_1]) ).
cnf(c288,plain,
( ~ cycle(e_3,e_3)
| ~ cycle(e_4,e_0)
| ~ cycle(X333,e_0)
| ~ next(e_4,X333) ),
inference(resolution,[status(thm)],[c25,e_4_greater_e_3]) ).
cnf(c283,plain,
( ~ cycle(e_2,e_3)
| ~ cycle(e_4,e_0)
| ~ cycle(X328,e_0)
| ~ next(e_4,X328) ),
inference(resolution,[status(thm)],[c25,e_4_greater_e_2]) ).
cnf(c282,plain,
( ~ cycle(e_1,e_3)
| ~ cycle(e_4,e_0)
| ~ cycle(X327,e_0)
| ~ next(e_4,X327) ),
inference(resolution,[status(thm)],[c25,e_4_greater_e_1]) ).
cnf(c273,plain,
( ~ cycle(e_3,e_2)
| ~ cycle(e_4,e_0)
| ~ cycle(X323,e_0)
| ~ next(e_4,X323) ),
inference(resolution,[status(thm)],[c24,e_4_greater_e_3]) ).
cnf(c270,plain,
( ~ cycle(e_0,e_2)
| ~ cycle(e_4,e_0)
| ~ cycle(X320,e_0)
| ~ next(e_4,X320) ),
inference(resolution,[status(thm)],[c24,e_4_greater_e_0]) ).
cnf(c269,plain,
( ~ cycle(e_0,e_2)
| ~ cycle(e_1,e_0)
| ~ cycle(X319,e_0)
| ~ next(e_1,X319) ),
inference(resolution,[status(thm)],[c24,e_1_greater_e_0]) ).
cnf(c268,plain,
( ~ cycle(e_2,e_2)
| ~ cycle(e_4,e_0)
| ~ cycle(X318,e_0)
| ~ next(e_4,X318) ),
inference(resolution,[status(thm)],[c24,e_4_greater_e_2]) ).
cnf(c267,plain,
( ~ cycle(e_1,e_2)
| ~ cycle(e_4,e_0)
| ~ cycle(X317,e_0)
| ~ next(e_4,X317) ),
inference(resolution,[status(thm)],[c24,e_4_greater_e_1]) ).
cnf(c23,plain,
( ~ cycle(X199,e_4)
| ~ cycle(X200,e_0)
| ~ cycle(X198,e_3)
| ~ next(X200,X198)
| ~ greater(X200,X199) ),
inference(resolution,[status(thm)],[cycle5,e_4_greater_e_3]) ).
cnf(c254,plain,
( ~ cycle(e_2,e_4)
| ~ cycle(e_4,e_0)
| ~ cycle(X308,e_3)
| ~ next(e_4,X308) ),
inference(resolution,[status(thm)],[c23,e_4_greater_e_2]) ).
cnf(c253,plain,
( ~ cycle(e_1,e_4)
| ~ cycle(e_4,e_0)
| ~ cycle(X307,e_3)
| ~ next(e_4,X307) ),
inference(resolution,[status(thm)],[c23,e_4_greater_e_1]) ).
cnf(c242,plain,
( ~ cycle(e_3,e_3)
| ~ cycle(e_4,e_0)
| ~ cycle(X301,e_2)
| ~ next(e_4,X301) ),
inference(resolution,[status(thm)],[c22,e_4_greater_e_3]) ).
cnf(c237,plain,
( ~ cycle(e_2,e_3)
| ~ cycle(e_4,e_0)
| ~ cycle(X296,e_2)
| ~ next(e_4,X296) ),
inference(resolution,[status(thm)],[c22,e_4_greater_e_2]) ).
cnf(c236,plain,
( ~ cycle(e_1,e_3)
| ~ cycle(e_4,e_0)
| ~ cycle(X295,e_2)
| ~ next(e_4,X295) ),
inference(resolution,[status(thm)],[c22,e_4_greater_e_1]) ).
cnf(e_3_greater_e_1,axiom,
greater(e_3,e_1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_3_greater_e_1) ).
cnf(c21,plain,
( ~ cycle(X189,e_3)
| ~ cycle(X190,e_0)
| ~ cycle(X188,e_1)
| ~ next(X190,X188)
| ~ greater(X190,X189) ),
inference(resolution,[status(thm)],[cycle5,e_3_greater_e_1]) ).
cnf(c226,plain,
( ~ cycle(e_3,e_3)
| ~ cycle(e_4,e_0)
| ~ cycle(X291,e_1)
| ~ next(e_4,X291) ),
inference(resolution,[status(thm)],[c21,e_4_greater_e_3]) ).
cnf(c221,plain,
( ~ cycle(e_2,e_3)
| ~ cycle(e_4,e_0)
| ~ cycle(X285,e_1)
| ~ next(e_4,X285) ),
inference(resolution,[status(thm)],[c21,e_4_greater_e_2]) ).
cnf(c220,plain,
( ~ cycle(e_1,e_3)
| ~ cycle(e_4,e_0)
| ~ cycle(X284,e_1)
| ~ next(e_4,X284) ),
inference(resolution,[status(thm)],[c21,e_4_greater_e_1]) ).
cnf(c20,plain,
( ~ cycle(X182,e_4)
| ~ cycle(X183,e_0)
| ~ cycle(X181,e_0)
| ~ next(X183,X181)
| ~ greater(X183,X182) ),
inference(resolution,[status(thm)],[cycle5,e_4_greater_e_0]) ).
cnf(c209,plain,
( ~ cycle(e_3,e_4)
| ~ cycle(e_4,e_0)
| ~ cycle(X279,e_0)
| ~ next(e_4,X279) ),
inference(resolution,[status(thm)],[c20,e_4_greater_e_3]) ).
cnf(c204,plain,
( ~ cycle(e_2,e_4)
| ~ cycle(e_4,e_0)
| ~ cycle(X273,e_0)
| ~ next(e_4,X273) ),
inference(resolution,[status(thm)],[c20,e_4_greater_e_2]) ).
cnf(c203,plain,
( ~ cycle(e_1,e_4)
| ~ cycle(e_4,e_0)
| ~ cycle(X272,e_0)
| ~ next(e_4,X272) ),
inference(resolution,[status(thm)],[c20,e_4_greater_e_1]) ).
cnf(c192,plain,
( ~ cycle(e_3,e_1)
| ~ cycle(e_4,e_0)
| ~ cycle(X267,e_0)
| ~ next(e_4,X267) ),
inference(resolution,[status(thm)],[c19,e_4_greater_e_3]) ).
cnf(c189,plain,
( ~ cycle(e_0,e_1)
| ~ cycle(e_4,e_0)
| ~ cycle(X263,e_0)
| ~ next(e_4,X263) ),
inference(resolution,[status(thm)],[c19,e_4_greater_e_0]) ).
cnf(c187,plain,
( ~ cycle(e_2,e_1)
| ~ cycle(e_4,e_0)
| ~ cycle(X261,e_0)
| ~ next(e_4,X261) ),
inference(resolution,[status(thm)],[c19,e_4_greater_e_2]) ).
cnf(c186,plain,
( ~ cycle(e_1,e_1)
| ~ cycle(e_4,e_0)
| ~ cycle(X260,e_0)
| ~ next(e_4,X260) ),
inference(resolution,[status(thm)],[c19,e_4_greater_e_1]) ).
cnf(c176,plain,
( ~ cycle(e_3,e_4)
| ~ cycle(e_4,e_0)
| ~ cycle(X255,e_2)
| ~ next(e_4,X255) ),
inference(resolution,[status(thm)],[c18,e_4_greater_e_3]) ).
cnf(c7,plain,
( ~ cycle(X64,X63)
| ~ cycle(X62,X64)
| ~ next(X64,X62)
| ~ greater(X63,e_0)
| equalish(X63,X62) ),
inference(factor,[status(thm)],[cycle4]) ).
cnf(c48,plain,
( ~ cycle(X80,e_2)
| ~ cycle(X79,X80)
| ~ next(X80,X79)
| equalish(e_2,X79) ),
inference(resolution,[status(thm)],[c7,e_2_greater_e_0]) ).
cnf(c64,plain,
( ~ cycle(e_0,e_2)
| ~ cycle(e_1,e_0)
| equalish(e_2,e_1) ),
inference(resolution,[status(thm)],[c48,e_0_then_e_1]) ).
cnf(c407,plain,
( ~ cycle(e_0,e_2)
| equalish(e_2,e_1) ),
inference(resolution,[status(thm)],[c403,c64]) ).
cnf(c405,plain,
( ~ cycle(e_1,X246)
| equalish(X246,e_0) ),
inference(resolution,[status(thm)],[c403,cycle1]) ).
cnf(c170,plain,
( ~ cycle(e_1,e_4)
| ~ cycle(e_4,e_0)
| ~ cycle(X245,e_2)
| ~ next(e_4,X245) ),
inference(resolution,[status(thm)],[c18,e_4_greater_e_1]) ).
cnf(c17,plain,
( ~ cycle(X165,e_4)
| ~ cycle(X166,e_0)
| ~ cycle(X164,e_1)
| ~ next(X166,X164)
| ~ greater(X166,X165) ),
inference(resolution,[status(thm)],[cycle5,e_4_greater_e_1]) ).
cnf(c159,plain,
( ~ cycle(e_3,e_4)
| ~ cycle(e_4,e_0)
| ~ cycle(X240,e_1)
| ~ next(e_4,X240) ),
inference(resolution,[status(thm)],[c17,e_4_greater_e_3]) ).
cnf(c154,plain,
( ~ cycle(e_2,e_4)
| ~ cycle(e_4,e_0)
| ~ cycle(X233,e_1)
| ~ next(e_4,X233) ),
inference(resolution,[status(thm)],[c17,e_4_greater_e_2]) ).
cnf(c16,plain,
( ~ cycle(X159,X160)
| ~ cycle(X160,e_0)
| ~ cycle(X161,X159)
| ~ next(X160,X161)
| ~ greater(X160,X159) ),
inference(factor,[status(thm)],[cycle5]) ).
cnf(c147,plain,
( ~ cycle(e_3,e_4)
| ~ cycle(e_4,e_0)
| ~ cycle(X227,e_3)
| ~ next(e_4,X227) ),
inference(resolution,[status(thm)],[c16,e_4_greater_e_3]) ).
cnf(c143,plain,
( ~ cycle(e_0,e_1)
| ~ cycle(e_1,e_0)
| ~ cycle(X221,e_0)
| ~ next(e_1,X221) ),
inference(resolution,[status(thm)],[c16,e_1_greater_e_0]) ).
cnf(c142,plain,
( ~ cycle(e_2,e_4)
| ~ cycle(e_4,e_0)
| ~ cycle(X220,e_2)
| ~ next(e_4,X220) ),
inference(resolution,[status(thm)],[c16,e_4_greater_e_2]) ).
cnf(c141,plain,
( ~ cycle(e_1,e_4)
| ~ cycle(e_4,e_0)
| ~ cycle(X219,e_1)
| ~ next(e_4,X219) ),
inference(resolution,[status(thm)],[c16,e_4_greater_e_1]) ).
cnf(c41,plain,
( ~ group_element(X218)
| product(X218,X218,e_1)
| product(X218,X218,e_2)
| product(X218,X218,e_3)
| product(X218,X218,e_4) ),
inference(factor,[status(thm)],[product_total_function1]) ).
cnf(c309,plain,
( ~ cycle(e_3,e_3)
| ~ cycle(e_4,e_1)
| equalish(e_3,e_2) ),
inference(resolution,[status(thm)],[c134,e_3_then_e_4]) ).
cnf(c132,plain,
( ~ cycle(X210,e_4)
| ~ cycle(X209,e_1)
| ~ next(X210,X209)
| equalish(e_4,e_2) ),
inference(resolution,[status(thm)],[c11,e_4_greater_e_0]) ).
cnf(c293,plain,
( ~ cycle(e_3,e_4)
| ~ cycle(e_4,e_1)
| equalish(e_4,e_2) ),
inference(resolution,[status(thm)],[c132,e_3_then_e_4]) ).
cnf(c278,plain,
( ~ cycle(e_3,e_1)
| ~ cycle(e_4,e_1)
| equalish(e_1,e_2) ),
inference(resolution,[status(thm)],[c131,e_3_then_e_4]) ).
cnf(c122,plain,
( ~ cycle(X186,e_4)
| ~ cycle(X187,e_0)
| ~ next(X186,X187)
| equalish(e_4,e_1) ),
inference(resolution,[status(thm)],[c10,e_4_greater_e_0]) ).
cnf(c9,plain,
( ~ cycle(X136,X135)
| ~ cycle(X134,e_3)
| ~ next(X136,X134)
| ~ greater(X135,e_0)
| equalish(X135,e_4) ),
inference(resolution,[status(thm)],[cycle4,e_3_then_e_4]) ).
cnf(c113,plain,
( ~ cycle(X180,e_3)
| ~ cycle(X179,e_3)
| ~ next(X180,X179)
| equalish(e_3,e_4) ),
inference(resolution,[status(thm)],[c9,e_3_greater_e_0]) ).
cnf(c200,plain,
( ~ cycle(e_1,e_3)
| ~ cycle(e_2,e_3)
| equalish(e_3,e_4) ),
inference(resolution,[status(thm)],[c113,e_1_then_e_2]) ).
cnf(c197,plain,
( ~ cycle(e_2,e_3)
| ~ cycle(e_3,e_3)
| equalish(e_3,e_4) ),
inference(resolution,[status(thm)],[c113,e_2_then_e_3]) ).
cnf(c112,plain,
( ~ cycle(X175,e_2)
| ~ cycle(X174,e_3)
| ~ next(X175,X174)
| equalish(e_2,e_4) ),
inference(resolution,[status(thm)],[c9,e_2_greater_e_0]) ).
cnf(c183,plain,
( ~ cycle(e_1,e_2)
| ~ cycle(e_2,e_3)
| equalish(e_2,e_4) ),
inference(resolution,[status(thm)],[c112,e_1_then_e_2]) ).
cnf(c182,plain,
( ~ cycle(e_0,e_2)
| ~ cycle(e_1,e_3)
| equalish(e_2,e_4) ),
inference(resolution,[status(thm)],[c112,e_0_then_e_1]) ).
cnf(c180,plain,
( ~ cycle(e_2,e_2)
| ~ cycle(e_3,e_3)
| equalish(e_2,e_4) ),
inference(resolution,[status(thm)],[c112,e_2_then_e_3]) ).
cnf(c110,plain,
( ~ cycle(X168,e_1)
| ~ cycle(X167,e_3)
| ~ next(X168,X167)
| equalish(e_1,e_4) ),
inference(resolution,[status(thm)],[c9,e_1_greater_e_0]) ).
cnf(c166,plain,
( ~ cycle(e_1,e_1)
| ~ cycle(e_2,e_3)
| equalish(e_1,e_4) ),
inference(resolution,[status(thm)],[c110,e_1_then_e_2]) ).
cnf(c165,plain,
( ~ cycle(e_0,e_1)
| ~ cycle(e_1,e_3)
| equalish(e_1,e_4) ),
inference(resolution,[status(thm)],[c110,e_0_then_e_1]) ).
cnf(c163,plain,
( ~ cycle(e_2,e_1)
| ~ cycle(e_3,e_3)
| equalish(e_1,e_4) ),
inference(resolution,[status(thm)],[c110,e_2_then_e_3]) ).
cnf(c138,plain,
( ~ cycle(e_3,e_2)
| ~ cycle(e_4,e_2)
| equalish(e_2,e_3) ),
inference(resolution,[status(thm)],[c105,e_3_then_e_4]) ).
cnf(c128,plain,
( ~ cycle(e_3,e_4)
| ~ cycle(e_4,e_2)
| equalish(e_4,e_3) ),
inference(resolution,[status(thm)],[c104,e_3_then_e_4]) ).
cnf(c119,plain,
( ~ cycle(e_0,e_1)
| ~ cycle(e_1,e_2)
| equalish(e_1,e_3) ),
inference(resolution,[status(thm)],[c103,e_0_then_e_1]) ).
cnf(c118,plain,
( ~ cycle(e_3,e_1)
| ~ cycle(e_4,e_2)
| equalish(e_1,e_3) ),
inference(resolution,[status(thm)],[c103,e_3_then_e_4]) ).
cnf(c55,plain,
( ~ product(X99,X98,X97)
| ~ product(X97,X96,X97)
| ~ product(X97,X98,X99)
| equalish(X99,X97) ),
inference(factor,[status(thm)],[qg1_1]) ).
cnf(c49,plain,
( ~ cycle(X82,e_3)
| ~ cycle(X81,X82)
| ~ next(X82,X81)
| equalish(e_3,X81) ),
inference(resolution,[status(thm)],[c7,e_3_greater_e_0]) ).
cnf(c69,plain,
( ~ cycle(e_1,e_3)
| ~ cycle(e_2,e_1)
| equalish(e_3,e_2) ),
inference(resolution,[status(thm)],[c49,e_1_then_e_2]) ).
cnf(c67,plain,
( ~ cycle(e_3,e_3)
| ~ cycle(e_4,e_3)
| equalish(e_3,e_4) ),
inference(resolution,[status(thm)],[c49,e_3_then_e_4]) ).
cnf(c63,plain,
( ~ cycle(e_3,e_2)
| ~ cycle(e_4,e_3)
| equalish(e_2,e_4) ),
inference(resolution,[status(thm)],[c48,e_3_then_e_4]) ).
cnf(c62,plain,
( ~ cycle(e_2,e_2)
| ~ cycle(e_3,e_2)
| equalish(e_2,e_3) ),
inference(resolution,[status(thm)],[c48,e_2_then_e_3]) ).
cnf(c47,plain,
( ~ cycle(X78,e_4)
| ~ cycle(X77,X78)
| ~ next(X78,X77)
| equalish(e_4,X77) ),
inference(resolution,[status(thm)],[c7,e_4_greater_e_0]) ).
cnf(c61,plain,
( ~ cycle(e_1,e_4)
| ~ cycle(e_2,e_1)
| equalish(e_4,e_2) ),
inference(resolution,[status(thm)],[c47,e_1_then_e_2]) ).
cnf(c58,plain,
( ~ cycle(e_2,e_4)
| ~ cycle(e_3,e_2)
| equalish(e_4,e_3) ),
inference(resolution,[status(thm)],[c47,e_2_then_e_3]) ).
cnf(c46,plain,
( ~ cycle(X66,e_1)
| ~ cycle(X65,X66)
| ~ next(X66,X65)
| equalish(e_1,X65) ),
inference(resolution,[status(thm)],[c7,e_1_greater_e_0]) ).
cnf(c51,plain,
( ~ cycle(e_3,e_1)
| ~ cycle(e_4,e_3)
| equalish(e_1,e_4) ),
inference(resolution,[status(thm)],[c46,e_3_then_e_4]) ).
cnf(c50,plain,
( ~ cycle(e_2,e_1)
| ~ cycle(e_3,e_2)
| equalish(e_1,e_3) ),
inference(resolution,[status(thm)],[c46,e_2_then_e_3]) ).
cnf(c38,plain,
( ~ cycle(e_1,e_4)
| equalish(e_1,e_2) ),
inference(resolution,[status(thm)],[c36,e_4_greater_e_0]) ).
cnf(c30,plain,
( ~ cycle(e_1,e_0)
| ~ greater(e_1,e_1) ),
inference(resolution,[status(thm)],[cycle6,product_idempotence]) ).
cnf(c14,plain,
( ~ product(X28,X28,X29)
| equalish(X29,X28) ),
inference(resolution,[status(thm)],[product_total_function2,product_idempotence]) ).
cnf(c13,plain,
( ~ product(X20,X19,X21)
| equalish(X21,X21) ),
inference(factor,[status(thm)],[product_total_function2]) ).
cnf(c15,plain,
equalish(X27,X27),
inference(resolution,[status(thm)],[c13,product_idempotence]) ).
cnf(c1,plain,
( ~ cycle(e_4,X14)
| equalish(X14,e_0) ),
inference(resolution,[status(thm)],[cycle1,cycle3]) ).
cnf(e_3_is_not_e_4,axiom,
~ equalish(e_3,e_4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_3_is_not_e_4) ).
cnf(e_2_is_not_e_4,axiom,
~ equalish(e_2,e_4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_2_is_not_e_4) ).
cnf(e_1_is_not_e_4,axiom,
~ equalish(e_1,e_4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_1_is_not_e_4) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : GRP123-3.004 : TPTP v8.1.2. Released v1.2.0.
% 0.03/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.34 % Computer : n025.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Thu May 9 04:53:08 EDT 2024
% 0.13/0.35 % CPUTime :
% 8.71/8.89 % Version: 1.5
% 8.71/8.89 % SZS status Satisfiable
% 8.71/8.89 % SZS output start Saturation
% See solution above
% 8.75/8.91
% 8.75/8.91 % Initial clauses : 44
% 8.75/8.91 % Processed clauses : 858
% 8.75/8.91 % Factors computed : 47
% 8.75/8.91 % Resolvents computed: 3984
% 8.75/8.91 % Tautologies deleted: 19
% 8.75/8.91 % Forward subsumed : 3198
% 8.75/8.91 % Backward subsumed : 407
% 8.75/8.91 % -------- CPU Time ---------
% 8.75/8.91 % User time : 8.534 s
% 8.75/8.91 % System time : 0.024 s
% 8.75/8.91 % Total time : 8.558 s
%------------------------------------------------------------------------------