%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GRP126-3.004 : TPTP v8.1.2. Released v1.2.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n008.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:08 EDT 2024
% Result : Unsatisfiable 3.41s 3.64s
% Output : Refutation 3.41s
% Verified :
% SZS Type : Refutation
% Derivation depth : 23
% Number of leaves : 34
% Syntax : Number of clauses : 136 ( 29 unt; 64 nHn; 135 RR)
% Number of literals : 371 ( 0 equ; 137 neg)
% Maximal clause size : 6 ( 2 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 7 ( 6 usr; 1 prp; 0-3 aty)
% Number of functors : 5 ( 5 usr; 5 con; 0-0 aty)
% Number of variables : 74 ( 0 sgn)
% 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(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_then_e_3,axiom,
next(e_2,e_3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_2_then_e_3) ).
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_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,X10)
| ~ cycle(X13,X12)
| ~ next(X11,X13)
| ~ greater(X10,e_0)
| ~ next(X12,X9)
| equalish(X10,X9) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cycle4) ).
cnf(c9,plain,
( ~ cycle(X89,X90)
| ~ cycle(X88,e_1)
| ~ next(X89,X88)
| ~ greater(X90,e_0)
| equalish(X90,e_2) ),
inference(resolution,[status(thm)],[cycle4,e_1_then_e_2]) ).
cnf(c101,plain,
( ~ cycle(X107,e_3)
| ~ cycle(X106,e_1)
| ~ next(X107,X106)
| equalish(e_3,e_2) ),
inference(resolution,[status(thm)],[c9,e_3_greater_e_0]) ).
cnf(c144,plain,
( ~ cycle(e_2,e_3)
| ~ cycle(e_3,e_1)
| equalish(e_3,e_2) ),
inference(resolution,[status(thm)],[c101,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(X25,X24)
| ~ cycle(X23,e_0)
| ~ cycle(X26,X22)
| ~ next(X23,X26)
| ~ greater(X23,X25)
| ~ greater(X24,X22) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cycle5) ).
cnf(c21,plain,
( ~ cycle(X130,e_2)
| ~ cycle(X131,e_0)
| ~ cycle(X132,e_0)
| ~ next(X131,X132)
| ~ greater(X131,X130) ),
inference(resolution,[status(thm)],[cycle5,e_2_greater_e_0]) ).
cnf(c212,plain,
( ~ cycle(e_2,e_2)
| ~ cycle(e_3,e_0)
| ~ cycle(X234,e_0)
| ~ next(e_3,X234) ),
inference(resolution,[status(thm)],[c21,e_3_greater_e_2]) ).
cnf(c452,plain,
( ~ cycle(e_2,e_2)
| ~ cycle(e_3,e_0)
| ~ cycle(e_4,e_0) ),
inference(resolution,[status(thm)],[c212,e_3_then_e_4]) ).
cnf(c454,plain,
( ~ cycle(e_2,e_2)
| ~ cycle(e_3,e_0) ),
inference(resolution,[status(thm)],[c452,cycle3]) ).
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_0_then_e_1,axiom,
next(e_0,e_1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_0_then_e_1) ).
cnf(c8,plain,
( ~ cycle(X84,X85)
| ~ cycle(X83,e_0)
| ~ next(X84,X83)
| ~ greater(X85,e_0)
| equalish(X85,e_1) ),
inference(resolution,[status(thm)],[cycle4,e_0_then_e_1]) ).
cnf(c93,plain,
( ~ cycle(X95,e_2)
| ~ cycle(X94,e_0)
| ~ next(X95,X94)
| equalish(e_2,e_1) ),
inference(resolution,[status(thm)],[c8,e_2_greater_e_0]) ).
cnf(c116,plain,
( ~ cycle(e_3,e_2)
| ~ cycle(e_4,e_0)
| equalish(e_2,e_1) ),
inference(resolution,[status(thm)],[c93,e_3_then_e_4]) ).
cnf(c119,plain,
( ~ cycle(e_3,e_2)
| equalish(e_2,e_1) ),
inference(resolution,[status(thm)],[c116,cycle3]) ).
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(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(c5,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(c92,plain,
( ~ cycle(X87,e_3)
| ~ cycle(X86,e_0)
| ~ next(X87,X86)
| equalish(e_3,e_1) ),
inference(resolution,[status(thm)],[c8,e_3_greater_e_0]) ).
cnf(c100,plain,
( ~ cycle(e_3,e_3)
| ~ cycle(e_4,e_0)
| equalish(e_3,e_1) ),
inference(resolution,[status(thm)],[c92,e_3_then_e_4]) ).
cnf(c107,plain,
( ~ cycle(e_3,e_3)
| equalish(e_3,e_1) ),
inference(resolution,[status(thm)],[c100,cycle3]) ).
cnf(c108,plain,
( equalish(e_3,e_1)
| cycle(e_3,e_0)
| cycle(e_3,e_1)
| cycle(e_3,e_2) ),
inference(resolution,[status(thm)],[c107,c5]) ).
cnf(c490,plain,
( cycle(e_3,e_0)
| cycle(e_3,e_1)
| cycle(e_3,e_2) ),
inference(resolution,[status(thm)],[c108,e_3_is_not_e_1]) ).
cnf(c562,plain,
( cycle(e_3,e_0)
| cycle(e_3,e_1)
| equalish(e_2,e_1) ),
inference(resolution,[status(thm)],[c490,c119]) ).
cnf(c593,plain,
( cycle(e_3,e_0)
| cycle(e_3,e_1) ),
inference(resolution,[status(thm)],[c562,e_2_is_not_e_1]) ).
cnf(c603,plain,
( cycle(e_3,e_1)
| ~ cycle(e_2,e_2) ),
inference(resolution,[status(thm)],[c593,c454]) ).
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(c25,plain,
( ~ cycle(X150,e_1)
| ~ cycle(X151,e_0)
| ~ cycle(X152,e_0)
| ~ next(X151,X152)
| ~ greater(X151,X150) ),
inference(resolution,[status(thm)],[cycle5,e_1_greater_e_0]) ).
cnf(c278,plain,
( ~ cycle(e_2,e_1)
| ~ cycle(e_3,e_0)
| ~ cycle(X278,e_0)
| ~ next(e_3,X278) ),
inference(resolution,[status(thm)],[c25,e_3_greater_e_2]) ).
cnf(c641,plain,
( ~ cycle(e_2,e_1)
| ~ cycle(e_3,e_0)
| ~ cycle(e_4,e_0) ),
inference(resolution,[status(thm)],[c278,e_3_then_e_4]) ).
cnf(c642,plain,
( ~ cycle(e_2,e_1)
| ~ cycle(e_3,e_0) ),
inference(resolution,[status(thm)],[c641,cycle3]) ).
cnf(c643,plain,
( ~ cycle(e_2,e_1)
| cycle(e_3,e_1) ),
inference(resolution,[status(thm)],[c642,c593]) ).
cnf(element_2,axiom,
group_element(e_2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',element_2) ).
cnf(c4,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(c17,plain,
( ~ cycle(X108,e_3)
| ~ cycle(X109,e_0)
| ~ cycle(X110,e_0)
| ~ next(X109,X110)
| ~ greater(X109,X108) ),
inference(resolution,[status(thm)],[cycle5,e_3_greater_e_0]) ).
cnf(c154,plain,
( ~ cycle(e_2,e_3)
| ~ cycle(e_3,e_0)
| ~ cycle(X182,e_0)
| ~ next(e_3,X182) ),
inference(resolution,[status(thm)],[c17,e_3_greater_e_2]) ).
cnf(c333,plain,
( ~ cycle(e_2,e_3)
| ~ cycle(e_3,e_0)
| ~ cycle(e_4,e_0) ),
inference(resolution,[status(thm)],[c154,e_3_then_e_4]) ).
cnf(c334,plain,
( ~ cycle(e_2,e_3)
| ~ cycle(e_3,e_0) ),
inference(resolution,[status(thm)],[c333,cycle3]) ).
cnf(c599,plain,
( cycle(e_3,e_1)
| ~ cycle(e_2,e_3) ),
inference(resolution,[status(thm)],[c593,c334]) ).
cnf(c617,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)],[c599,c4]) ).
cnf(c684,plain,
( cycle(e_3,e_1)
| cycle(e_2,e_0)
| cycle(e_2,e_2) ),
inference(resolution,[status(thm)],[c617,c643]) ).
cnf(c738,plain,
( cycle(e_3,e_1)
| cycle(e_2,e_0) ),
inference(resolution,[status(thm)],[c684,c603]) ).
cnf(c752,plain,
( cycle(e_2,e_0)
| ~ cycle(e_2,e_3)
| equalish(e_3,e_2) ),
inference(resolution,[status(thm)],[c738,c144]) ).
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(c104,plain,
( ~ cycle(X119,e_1)
| ~ cycle(X118,e_1)
| ~ next(X119,X118)
| equalish(e_1,e_2) ),
inference(resolution,[status(thm)],[c9,e_1_greater_e_0]) ).
cnf(c176,plain,
( ~ cycle(e_2,e_1)
| ~ cycle(e_3,e_1)
| equalish(e_1,e_2) ),
inference(resolution,[status(thm)],[c104,e_2_then_e_3]) ).
cnf(c751,plain,
( cycle(e_2,e_0)
| ~ cycle(e_2,e_1)
| equalish(e_1,e_2) ),
inference(resolution,[status(thm)],[c738,c176]) ).
cnf(c819,plain,
( cycle(e_2,e_0)
| equalish(e_1,e_2)
| cycle(e_2,e_2)
| cycle(e_2,e_3) ),
inference(resolution,[status(thm)],[c751,c4]) ).
cnf(c991,plain,
( cycle(e_2,e_0)
| cycle(e_2,e_2)
| cycle(e_2,e_3) ),
inference(resolution,[status(thm)],[c819,e_1_is_not_e_2]) ).
cnf(c1055,plain,
( cycle(e_2,e_0)
| cycle(e_2,e_2)
| equalish(e_3,e_2) ),
inference(resolution,[status(thm)],[c991,c752]) ).
cnf(c1105,plain,
( cycle(e_2,e_0)
| cycle(e_2,e_2) ),
inference(resolution,[status(thm)],[c1055,e_3_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(X38,e_0)
| ~ product(X38,e_1,X39)
| ~ greater(X39,X38) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cycle6) ).
cnf(product_idempotence,axiom,
product(X2,X2,X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',product_idempotence) ).
cnf(product_right_cancellation,axiom,
( ~ product(X33,X32,X34)
| ~ product(X33,X31,X34)
| equalish(X32,X31) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',product_right_cancellation) ).
cnf(c29,plain,
( ~ product(X40,X41,X40)
| equalish(X41,X40) ),
inference(resolution,[status(thm)],[product_right_cancellation,product_idempotence]) ).
cnf(product_left_cancellation,axiom,
( ~ product(X44,X46,X45)
| ~ product(X43,X46,X45)
| equalish(X44,X43) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',product_left_cancellation) ).
cnf(c33,plain,
( ~ product(X54,X55,X55)
| equalish(X54,X55) ),
inference(resolution,[status(thm)],[product_left_cancellation,product_idempotence]) ).
cnf(element_1,axiom,
group_element(e_1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',element_1) ).
cnf(product_total_function1,axiom,
( ~ group_element(X64)
| ~ group_element(X65)
| product(X64,X65,e_1)
| product(X64,X65,e_2)
| product(X64,X65,e_3)
| product(X64,X65,e_4) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',product_total_function1) ).
cnf(c41,plain,
( ~ group_element(X171)
| product(X171,e_1,e_1)
| product(X171,e_1,e_2)
| product(X171,e_1,e_3)
| product(X171,e_1,e_4) ),
inference(resolution,[status(thm)],[product_total_function1,element_1]) ).
cnf(c316,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)],[c41,element_2]) ).
cnf(c867,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)],[c316,c33]) ).
cnf(c2131,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)],[c867,e_2_is_not_e_1]) ).
cnf(c2319,plain,
( product(e_2,e_1,e_3)
| product(e_2,e_1,e_4)
| equalish(e_1,e_2) ),
inference(resolution,[status(thm)],[c2131,c29]) ).
cnf(c2358,plain,
( product(e_2,e_1,e_3)
| product(e_2,e_1,e_4) ),
inference(resolution,[status(thm)],[c2319,e_1_is_not_e_2]) ).
cnf(c2360,plain,
( product(e_2,e_1,e_4)
| ~ cycle(e_2,e_0)
| ~ greater(e_3,e_2) ),
inference(resolution,[status(thm)],[c2358,cycle6]) ).
cnf(c2380,plain,
( product(e_2,e_1,e_4)
| ~ cycle(e_2,e_0) ),
inference(resolution,[status(thm)],[c2360,e_3_greater_e_2]) ).
cnf(c2381,plain,
( product(e_2,e_1,e_4)
| cycle(e_2,e_2) ),
inference(resolution,[status(thm)],[c2380,c1105]) ).
cnf(c2384,plain,
( cycle(e_2,e_2)
| ~ cycle(e_2,e_0)
| ~ greater(e_4,e_2) ),
inference(resolution,[status(thm)],[c2381,cycle6]) ).
cnf(c2422,plain,
( cycle(e_2,e_2)
| ~ cycle(e_2,e_0) ),
inference(resolution,[status(thm)],[c2384,e_4_greater_e_2]) ).
cnf(c2423,plain,
cycle(e_2,e_2),
inference(resolution,[status(thm)],[c2422,c1105]) ).
cnf(cycle7,axiom,
( ~ cycle(X52,X53)
| ~ product(X52,e_1,X51)
| ~ greater(X53,e_0)
| ~ next(X52,X50)
| equalish(X51,X50) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cycle7) ).
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_1_is_not_e_4,axiom,
~ equalish(e_1,e_4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_1_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_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(c40,plain,
( ~ group_element(X167)
| product(X167,e_4,e_1)
| product(X167,e_4,e_2)
| product(X167,e_4,e_3)
| product(X167,e_4,e_4) ),
inference(resolution,[status(thm)],[product_total_function1,element_4]) ).
cnf(c310,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)],[c40,element_2]) ).
cnf(c809,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)],[c310,c29]) ).
cnf(c1263,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)],[c809,e_4_is_not_e_2]) ).
cnf(c1275,plain,
( product(e_2,e_4,e_1)
| product(e_2,e_4,e_3)
| equalish(e_2,e_4) ),
inference(resolution,[status(thm)],[c1263,c33]) ).
cnf(c1287,plain,
( product(e_2,e_4,e_1)
| product(e_2,e_4,e_3) ),
inference(resolution,[status(thm)],[c1275,e_2_is_not_e_4]) ).
cnf(c1295,plain,
( product(e_2,e_4,e_1)
| ~ product(e_2,X361,e_3)
| equalish(X361,e_4) ),
inference(resolution,[status(thm)],[c1287,product_right_cancellation]) ).
cnf(c2363,plain,
( product(e_2,e_1,e_4)
| product(e_2,e_4,e_1)
| equalish(e_1,e_4) ),
inference(resolution,[status(thm)],[c2358,c1295]) ).
cnf(c2649,plain,
( product(e_2,e_1,e_4)
| product(e_2,e_4,e_1) ),
inference(resolution,[status(thm)],[c2363,e_1_is_not_e_4]) ).
cnf(c2663,plain,
( product(e_2,e_1,e_4)
| ~ product(e_2,X575,e_1)
| equalish(X575,e_4) ),
inference(resolution,[status(thm)],[c2649,product_right_cancellation]) ).
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(c314,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)],[c41,element_4]) ).
cnf(c841,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)],[c314,c33]) ).
cnf(c1933,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)],[c841,e_4_is_not_e_1]) ).
cnf(c2193,plain,
( product(e_4,e_1,e_2)
| product(e_4,e_1,e_3)
| equalish(e_1,e_4) ),
inference(resolution,[status(thm)],[c1933,c29]) ).
cnf(c2233,plain,
( product(e_4,e_1,e_2)
| product(e_4,e_1,e_3) ),
inference(resolution,[status(thm)],[c2193,e_1_is_not_e_4]) ).
cnf(c2261,plain,
( product(e_4,e_1,e_2)
| ~ product(X522,e_1,e_3)
| equalish(X522,e_4) ),
inference(resolution,[status(thm)],[c2233,product_left_cancellation]) ).
cnf(c2367,plain,
( product(e_2,e_1,e_4)
| product(e_4,e_1,e_2)
| equalish(e_2,e_4) ),
inference(resolution,[status(thm)],[c2358,c2261]) ).
cnf(c2890,plain,
( product(e_2,e_1,e_4)
| product(e_4,e_1,e_2) ),
inference(resolution,[status(thm)],[c2367,e_2_is_not_e_4]) ).
cnf(qg4,negated_conjecture,
( ~ product(X59,X60,X58)
| ~ product(X60,X59,X57)
| product(X58,X57,X60) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',qg4) ).
cnf(c309,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)],[c40,element_1]) ).
cnf(c787,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)],[c309,c29]) ).
cnf(c1194,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)],[c787,e_4_is_not_e_1]) ).
cnf(c1205,plain,
( product(e_1,e_4,e_2)
| product(e_1,e_4,e_3)
| equalish(e_1,e_4) ),
inference(resolution,[status(thm)],[c1194,c33]) ).
cnf(c1216,plain,
( product(e_1,e_4,e_2)
| product(e_1,e_4,e_3) ),
inference(resolution,[status(thm)],[c1205,e_1_is_not_e_4]) ).
cnf(c1220,plain,
( product(e_1,e_4,e_3)
| ~ product(X325,e_4,e_2)
| equalish(X325,e_1) ),
inference(resolution,[status(thm)],[c1216,product_left_cancellation]) ).
cnf(c1291,plain,
( product(e_2,e_4,e_3)
| ~ product(X358,e_4,e_1)
| equalish(X358,e_2) ),
inference(resolution,[status(thm)],[c1287,product_left_cancellation]) ).
cnf(c311,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)],[c40,element_3]) ).
cnf(c833,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)],[c311,c29]) ).
cnf(c1398,plain,
( product(e_3,e_4,e_1)
| product(e_3,e_4,e_2)
| product(e_3,e_4,e_4) ),
inference(resolution,[status(thm)],[c833,e_4_is_not_e_3]) ).
cnf(c1413,plain,
( product(e_3,e_4,e_1)
| product(e_3,e_4,e_2)
| equalish(e_3,e_4) ),
inference(resolution,[status(thm)],[c1398,c33]) ).
cnf(c1428,plain,
( product(e_3,e_4,e_1)
| product(e_3,e_4,e_2) ),
inference(resolution,[status(thm)],[c1413,e_3_is_not_e_4]) ).
cnf(c1434,plain,
( product(e_3,e_4,e_2)
| product(e_2,e_4,e_3)
| equalish(e_3,e_2) ),
inference(resolution,[status(thm)],[c1428,c1291]) ).
cnf(c1556,plain,
( product(e_3,e_4,e_2)
| product(e_2,e_4,e_3) ),
inference(resolution,[status(thm)],[c1434,e_3_is_not_e_2]) ).
cnf(c1557,plain,
( product(e_2,e_4,e_3)
| product(e_1,e_4,e_3)
| equalish(e_3,e_1) ),
inference(resolution,[status(thm)],[c1556,c1220]) ).
cnf(c1820,plain,
( product(e_2,e_4,e_3)
| product(e_1,e_4,e_3) ),
inference(resolution,[status(thm)],[c1557,e_3_is_not_e_1]) ).
cnf(c1822,plain,
( product(e_1,e_4,e_3)
| ~ product(e_2,X469,e_3)
| equalish(X469,e_4) ),
inference(resolution,[status(thm)],[c1820,product_right_cancellation]) ).
cnf(c2364,plain,
( product(e_2,e_1,e_4)
| product(e_1,e_4,e_3)
| equalish(e_1,e_4) ),
inference(resolution,[status(thm)],[c2358,c1822]) ).
cnf(c2764,plain,
( product(e_2,e_1,e_4)
| product(e_1,e_4,e_3) ),
inference(resolution,[status(thm)],[c2364,e_1_is_not_e_4]) ).
cnf(c2798,plain,
( product(e_2,e_1,e_4)
| ~ product(e_4,e_1,X626)
| product(X626,e_3,e_1) ),
inference(resolution,[status(thm)],[c2764,qg4]) ).
cnf(c3178,plain,
( product(e_2,e_1,e_4)
| product(e_2,e_3,e_1) ),
inference(resolution,[status(thm)],[c2798,c2890]) ).
cnf(c3212,plain,
( product(e_2,e_1,e_4)
| equalish(e_3,e_4) ),
inference(resolution,[status(thm)],[c3178,c2663]) ).
cnf(c3242,plain,
product(e_2,e_1,e_4),
inference(resolution,[status(thm)],[c3212,e_3_is_not_e_4]) ).
cnf(c3249,plain,
( ~ cycle(e_2,X652)
| ~ greater(X652,e_0)
| ~ next(e_2,X651)
| equalish(e_4,X651) ),
inference(resolution,[status(thm)],[c3242,cycle7]) ).
cnf(c3394,plain,
( ~ cycle(e_2,X653)
| ~ greater(X653,e_0)
| equalish(e_4,e_3) ),
inference(resolution,[status(thm)],[c3249,e_2_then_e_3]) ).
cnf(c3396,plain,
( ~ cycle(e_2,e_2)
| equalish(e_4,e_3) ),
inference(resolution,[status(thm)],[c3394,e_2_greater_e_0]) ).
cnf(c3399,plain,
equalish(e_4,e_3),
inference(resolution,[status(thm)],[c3396,c2423]) ).
cnf(c3400,plain,
$false,
inference(resolution,[status(thm)],[c3399,e_4_is_not_e_3]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : GRP126-3.004 : TPTP v8.1.2. Released v1.2.0.
% 0.12/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.34 % Computer : n008.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 03:53:08 EDT 2024
% 0.13/0.34 % CPUTime :
% 3.41/3.64 % Version: 1.5
% 3.41/3.64 % SZS status Unsatisfiable
% 3.41/3.64 % SZS output start CNFRefutation
% See solution above
% 3.41/3.64
% 3.41/3.64 % Initial clauses : 43
% 3.41/3.64 % Processed clauses : 723
% 3.41/3.64 % Factors computed : 8
% 3.41/3.64 % Resolvents computed: 3424
% 3.41/3.64 % Tautologies deleted: 19
% 3.41/3.64 % Forward subsumed : 1112
% 3.41/3.64 % Backward subsumed : 390
% 3.41/3.64 % -------- CPU Time ---------
% 3.41/3.64 % User time : 3.277 s
% 3.41/3.64 % System time : 0.018 s
% 3.41/3.64 % Total time : 3.295 s
%------------------------------------------------------------------------------