%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GRP125-3.005 : TPTP v8.1.2. Released v1.2.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n011.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:07 EDT 2024
% Result : Unsatisfiable 116.48s 116.71s
% Output : Refutation 116.48s
% Verified :
% SZS Type : Refutation
% Derivation depth : 103
% Number of leaves : 53
% Syntax : Number of clauses : 414 ( 59 unt; 263 nHn; 413 RR)
% Number of literals : 1292 ( 0 equ; 370 neg)
% Maximal clause size : 7 ( 3 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 7 ( 6 usr; 1 prp; 0-3 aty)
% Number of functors : 6 ( 6 usr; 6 con; 0-0 aty)
% Number of variables : 164 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(e_1_is_not_e_5,axiom,
~ equalish(e_1,e_5),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_1_is_not_e_5) ).
cnf(product_left_cancellation,axiom,
( ~ product(X52,X49,X51)
| ~ product(X50,X49,X51)
| equalish(X52,X50) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',product_left_cancellation) ).
cnf(e_2_is_not_e_5,axiom,
~ equalish(e_2,e_5),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_2_is_not_e_5) ).
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(product_right_cancellation,axiom,
( ~ product(X37,X40,X38)
| ~ product(X37,X39,X38)
| equalish(X40,X39) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',product_right_cancellation) ).
cnf(e_4_is_not_e_5,axiom,
~ equalish(e_4,e_5),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_4_is_not_e_5) ).
cnf(product_idempotence,axiom,
product(X2,X2,X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',product_idempotence) ).
cnf(c38,plain,
( ~ product(X47,X46,X47)
| equalish(X46,X47) ),
inference(resolution,[status(thm)],[product_right_cancellation,product_idempotence]) ).
cnf(e_5_is_not_e_4,axiom,
~ equalish(e_5,e_4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_5_is_not_e_4) ).
cnf(c47,plain,
( ~ product(X57,X56,X56)
| equalish(X57,X56) ),
inference(resolution,[status(thm)],[product_left_cancellation,product_idempotence]) ).
cnf(element_5,axiom,
group_element(e_5),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',element_5) ).
cnf(element_4,axiom,
group_element(e_4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',element_4) ).
cnf(product_total_function1,axiom,
( ~ group_element(X44)
| ~ group_element(X45)
| product(X44,X45,e_1)
| product(X44,X45,e_2)
| product(X44,X45,e_3)
| product(X44,X45,e_4)
| product(X44,X45,e_5) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',product_total_function1) ).
cnf(c42,plain,
( ~ group_element(X193)
| product(X193,e_4,e_1)
| product(X193,e_4,e_2)
| product(X193,e_4,e_3)
| product(X193,e_4,e_4)
| product(X193,e_4,e_5) ),
inference(resolution,[status(thm)],[product_total_function1,element_4]) ).
cnf(c557,plain,
( product(e_5,e_4,e_1)
| product(e_5,e_4,e_2)
| product(e_5,e_4,e_3)
| product(e_5,e_4,e_4)
| product(e_5,e_4,e_5) ),
inference(resolution,[status(thm)],[c42,element_5]) ).
cnf(c2282,plain,
( product(e_5,e_4,e_1)
| product(e_5,e_4,e_2)
| product(e_5,e_4,e_3)
| product(e_5,e_4,e_5)
| equalish(e_5,e_4) ),
inference(resolution,[status(thm)],[c557,c47]) ).
cnf(c11248,plain,
( product(e_5,e_4,e_1)
| product(e_5,e_4,e_2)
| product(e_5,e_4,e_3)
| product(e_5,e_4,e_5) ),
inference(resolution,[status(thm)],[c2282,e_5_is_not_e_4]) ).
cnf(c12142,plain,
( product(e_5,e_4,e_1)
| product(e_5,e_4,e_2)
| product(e_5,e_4,e_3)
| equalish(e_4,e_5) ),
inference(resolution,[status(thm)],[c11248,c38]) ).
cnf(c12192,plain,
( product(e_5,e_4,e_1)
| product(e_5,e_4,e_2)
| product(e_5,e_4,e_3) ),
inference(resolution,[status(thm)],[c12142,e_4_is_not_e_5]) ).
cnf(c12218,plain,
( product(e_5,e_4,e_1)
| product(e_5,e_4,e_3)
| ~ product(e_5,X1305,e_2)
| equalish(X1305,e_4) ),
inference(resolution,[status(thm)],[c12192,product_right_cancellation]) ).
cnf(e_3_is_not_e_5,axiom,
~ equalish(e_3,e_5),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_3_is_not_e_5) ).
cnf(e_5_is_not_e_1,axiom,
~ equalish(e_5,e_1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_5_is_not_e_1) ).
cnf(element_1,axiom,
group_element(e_1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',element_1) ).
cnf(c40,plain,
( ~ group_element(X187)
| product(X187,e_1,e_1)
| product(X187,e_1,e_2)
| product(X187,e_1,e_3)
| product(X187,e_1,e_4)
| product(X187,e_1,e_5) ),
inference(resolution,[status(thm)],[product_total_function1,element_1]) ).
cnf(c531,plain,
( product(e_5,e_1,e_1)
| product(e_5,e_1,e_2)
| product(e_5,e_1,e_3)
| product(e_5,e_1,e_4)
| product(e_5,e_1,e_5) ),
inference(resolution,[status(thm)],[c40,element_5]) ).
cnf(c1865,plain,
( product(e_5,e_1,e_2)
| product(e_5,e_1,e_3)
| product(e_5,e_1,e_4)
| product(e_5,e_1,e_5)
| equalish(e_5,e_1) ),
inference(resolution,[status(thm)],[c531,c47]) ).
cnf(c6194,plain,
( product(e_5,e_1,e_2)
| product(e_5,e_1,e_3)
| product(e_5,e_1,e_4)
| product(e_5,e_1,e_5) ),
inference(resolution,[status(thm)],[c1865,e_5_is_not_e_1]) ).
cnf(c7988,plain,
( product(e_5,e_1,e_2)
| product(e_5,e_1,e_3)
| product(e_5,e_1,e_4)
| equalish(e_1,e_5) ),
inference(resolution,[status(thm)],[c6194,c38]) ).
cnf(c8047,plain,
( product(e_5,e_1,e_2)
| product(e_5,e_1,e_3)
| product(e_5,e_1,e_4) ),
inference(resolution,[status(thm)],[c7988,e_1_is_not_e_5]) ).
cnf(c8070,plain,
( product(e_5,e_1,e_2)
| product(e_5,e_1,e_4)
| ~ product(X1035,e_1,e_3)
| equalish(X1035,e_5) ),
inference(resolution,[status(thm)],[c8047,product_left_cancellation]) ).
cnf(e_5_is_not_e_3,axiom,
~ equalish(e_5,e_3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_5_is_not_e_3) ).
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_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(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_2_greater_e_0,axiom,
greater(e_2,e_0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_2_greater_e_0) ).
cnf(cycle4,axiom,
( ~ cycle(X7,X9)
| ~ cycle(X11,X10)
| ~ next(X7,X11)
| ~ greater(X9,e_0)
| ~ next(X10,X8)
| equalish(X9,X8) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cycle4) ).
cnf(c7,plain,
( ~ cycle(X72,X73)
| ~ cycle(X74,X72)
| ~ next(X72,X74)
| ~ greater(X73,e_0)
| equalish(X73,X74) ),
inference(factor,[status(thm)],[cycle4]) ).
cnf(c73,plain,
( ~ cycle(X76,e_2)
| ~ cycle(X75,X76)
| ~ next(X76,X75)
| equalish(e_2,X75) ),
inference(resolution,[status(thm)],[c7,e_2_greater_e_0]) ).
cnf(c79,plain,
( ~ cycle(e_2,e_2)
| ~ cycle(e_3,e_2)
| equalish(e_2,e_3) ),
inference(resolution,[status(thm)],[c73,e_2_then_e_3]) ).
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_4_greater_e_1,axiom,
greater(e_4,e_1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_4_greater_e_1) ).
cnf(cycle5,axiom,
( ~ cycle(X12,X13)
| ~ cycle(X14,e_0)
| ~ cycle(X16,X15)
| ~ next(X14,X16)
| ~ greater(X14,X12)
| ~ greater(X13,X15) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cycle5) ).
cnf(c28,plain,
( ~ cycle(X179,e_4)
| ~ cycle(X181,e_0)
| ~ cycle(X180,e_1)
| ~ next(X181,X180)
| ~ greater(X181,X179) ),
inference(resolution,[status(thm)],[cycle5,e_4_greater_e_1]) ).
cnf(c496,plain,
( ~ cycle(e_2,e_4)
| ~ cycle(e_3,e_0)
| ~ cycle(X449,e_1)
| ~ next(e_3,X449) ),
inference(resolution,[status(thm)],[c28,e_3_greater_e_2]) ).
cnf(c1175,plain,
( ~ cycle(e_2,e_4)
| ~ cycle(e_3,e_0)
| ~ cycle(e_4,e_1) ),
inference(resolution,[status(thm)],[c496,e_3_then_e_4]) ).
cnf(cycle3,axiom,
cycle(e_5,e_0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cycle3) ).
cnf(e_4_then_e_5,axiom,
next(e_4,e_5),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_4_then_e_5) ).
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(e_3_greater_e_0,axiom,
greater(e_3,e_0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_3_greater_e_0) ).
cnf(c25,plain,
( ~ cycle(X164,e_3)
| ~ cycle(X166,e_0)
| ~ cycle(X165,e_0)
| ~ next(X166,X165)
| ~ greater(X166,X164) ),
inference(resolution,[status(thm)],[cycle5,e_3_greater_e_0]) ).
cnf(c437,plain,
( ~ cycle(e_2,e_3)
| ~ cycle(e_4,e_0)
| ~ cycle(X411,e_0)
| ~ next(e_4,X411) ),
inference(resolution,[status(thm)],[c25,e_4_greater_e_2]) ).
cnf(c1111,plain,
( ~ cycle(e_2,e_3)
| ~ cycle(e_4,e_0)
| ~ cycle(e_5,e_0) ),
inference(resolution,[status(thm)],[c437,e_4_then_e_5]) ).
cnf(c1112,plain,
( ~ cycle(e_2,e_3)
| ~ cycle(e_4,e_0) ),
inference(resolution,[status(thm)],[c1111,cycle3]) ).
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(e_4_greater_e_0,axiom,
greater(e_4,e_0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_4_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(c11,plain,
( ~ cycle(X98,X99)
| ~ cycle(X100,e_0)
| ~ next(X98,X100)
| ~ greater(X99,e_0)
| equalish(X99,e_1) ),
inference(resolution,[status(thm)],[cycle4,e_0_then_e_1]) ).
cnf(c149,plain,
( ~ cycle(X178,e_4)
| ~ cycle(X177,e_0)
| ~ next(X178,X177)
| equalish(e_4,e_1) ),
inference(resolution,[status(thm)],[c11,e_4_greater_e_0]) ).
cnf(c489,plain,
( ~ cycle(e_4,e_4)
| ~ cycle(e_5,e_0)
| equalish(e_4,e_1) ),
inference(resolution,[status(thm)],[c149,e_4_then_e_5]) ).
cnf(c494,plain,
( ~ cycle(e_4,e_4)
| equalish(e_4,e_1) ),
inference(resolution,[status(thm)],[c489,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(c151,plain,
( ~ cycle(X185,e_3)
| ~ cycle(X184,e_0)
| ~ next(X185,X184)
| equalish(e_3,e_1) ),
inference(resolution,[status(thm)],[c11,e_3_greater_e_0]) ).
cnf(c514,plain,
( ~ cycle(e_4,e_3)
| ~ cycle(e_5,e_0)
| equalish(e_3,e_1) ),
inference(resolution,[status(thm)],[c151,e_4_then_e_5]) ).
cnf(c524,plain,
( ~ cycle(e_4,e_3)
| equalish(e_3,e_1) ),
inference(resolution,[status(thm)],[c514,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(cycle2,axiom,
( ~ group_element(X6)
| cycle(X6,e_0)
| cycle(X6,e_1)
| cycle(X6,e_2)
| cycle(X6,e_3)
| cycle(X6,e_4) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cycle2) ).
cnf(c4,plain,
( cycle(e_4,e_0)
| cycle(e_4,e_1)
| cycle(e_4,e_2)
| cycle(e_4,e_3)
| cycle(e_4,e_4) ),
inference(resolution,[status(thm)],[cycle2,element_4]) ).
cnf(c148,plain,
( ~ cycle(X170,e_2)
| ~ cycle(X169,e_0)
| ~ next(X170,X169)
| equalish(e_2,e_1) ),
inference(resolution,[status(thm)],[c11,e_2_greater_e_0]) ).
cnf(c449,plain,
( ~ cycle(e_4,e_2)
| ~ cycle(e_5,e_0)
| equalish(e_2,e_1) ),
inference(resolution,[status(thm)],[c148,e_4_then_e_5]) ).
cnf(c469,plain,
( ~ cycle(e_4,e_2)
| equalish(e_2,e_1) ),
inference(resolution,[status(thm)],[c449,cycle3]) ).
cnf(c470,plain,
( equalish(e_2,e_1)
| cycle(e_4,e_0)
| cycle(e_4,e_1)
| cycle(e_4,e_3)
| cycle(e_4,e_4) ),
inference(resolution,[status(thm)],[c469,c4]) ).
cnf(c1191,plain,
( cycle(e_4,e_0)
| cycle(e_4,e_1)
| cycle(e_4,e_3)
| cycle(e_4,e_4) ),
inference(resolution,[status(thm)],[c470,e_2_is_not_e_1]) ).
cnf(c1589,plain,
( cycle(e_4,e_0)
| cycle(e_4,e_1)
| cycle(e_4,e_4)
| equalish(e_3,e_1) ),
inference(resolution,[status(thm)],[c1191,c524]) ).
cnf(c1953,plain,
( cycle(e_4,e_0)
| cycle(e_4,e_1)
| cycle(e_4,e_4) ),
inference(resolution,[status(thm)],[c1589,e_3_is_not_e_1]) ).
cnf(c1997,plain,
( cycle(e_4,e_0)
| cycle(e_4,e_1)
| equalish(e_4,e_1) ),
inference(resolution,[status(thm)],[c1953,c494]) ).
cnf(c2101,plain,
( cycle(e_4,e_0)
| cycle(e_4,e_1) ),
inference(resolution,[status(thm)],[c1997,e_4_is_not_e_1]) ).
cnf(c2120,plain,
( cycle(e_4,e_1)
| ~ cycle(e_2,e_3) ),
inference(resolution,[status(thm)],[c2101,c1112]) ).
cnf(c17,plain,
( ~ cycle(X126,e_2)
| ~ cycle(X128,e_0)
| ~ cycle(X127,e_0)
| ~ next(X128,X127)
| ~ greater(X128,X126) ),
inference(resolution,[status(thm)],[cycle5,e_2_greater_e_0]) ).
cnf(c264,plain,
( ~ cycle(e_2,e_2)
| ~ cycle(e_4,e_0)
| ~ cycle(X290,e_0)
| ~ next(e_4,X290) ),
inference(resolution,[status(thm)],[c17,e_4_greater_e_2]) ).
cnf(c933,plain,
( ~ cycle(e_2,e_2)
| ~ cycle(e_4,e_0)
| ~ cycle(e_5,e_0) ),
inference(resolution,[status(thm)],[c264,e_4_then_e_5]) ).
cnf(c934,plain,
( ~ cycle(e_2,e_2)
| ~ cycle(e_4,e_0) ),
inference(resolution,[status(thm)],[c933,cycle3]) ).
cnf(c2113,plain,
( cycle(e_4,e_1)
| ~ cycle(e_2,e_2) ),
inference(resolution,[status(thm)],[c2101,c934]) ).
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(c24,plain,
( ~ cycle(X159,e_1)
| ~ cycle(X161,e_0)
| ~ cycle(X160,e_0)
| ~ next(X161,X160)
| ~ greater(X161,X159) ),
inference(resolution,[status(thm)],[cycle5,e_1_greater_e_0]) ).
cnf(c414,plain,
( ~ cycle(e_2,e_1)
| ~ cycle(e_4,e_0)
| ~ cycle(X396,e_0)
| ~ next(e_4,X396) ),
inference(resolution,[status(thm)],[c24,e_4_greater_e_2]) ).
cnf(c1085,plain,
( ~ cycle(e_2,e_1)
| ~ cycle(e_4,e_0)
| ~ cycle(e_5,e_0) ),
inference(resolution,[status(thm)],[c414,e_4_then_e_5]) ).
cnf(c1086,plain,
( ~ cycle(e_2,e_1)
| ~ cycle(e_4,e_0) ),
inference(resolution,[status(thm)],[c1085,cycle3]) ).
cnf(c2122,plain,
( cycle(e_4,e_1)
| ~ cycle(e_2,e_1) ),
inference(resolution,[status(thm)],[c2101,c1086]) ).
cnf(element_2,axiom,
group_element(e_2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',element_2) ).
cnf(c3,plain,
( cycle(e_2,e_0)
| cycle(e_2,e_1)
| cycle(e_2,e_2)
| cycle(e_2,e_3)
| cycle(e_2,e_4) ),
inference(resolution,[status(thm)],[cycle2,element_2]) ).
cnf(c18,plain,
( ~ cycle(X129,e_4)
| ~ cycle(X131,e_0)
| ~ cycle(X130,e_0)
| ~ next(X131,X130)
| ~ greater(X131,X129) ),
inference(resolution,[status(thm)],[cycle5,e_4_greater_e_0]) ).
cnf(c282,plain,
( ~ cycle(e_2,e_4)
| ~ cycle(e_4,e_0)
| ~ cycle(X306,e_0)
| ~ next(e_4,X306) ),
inference(resolution,[status(thm)],[c18,e_4_greater_e_2]) ).
cnf(c964,plain,
( ~ cycle(e_2,e_4)
| ~ cycle(e_4,e_0)
| ~ cycle(e_5,e_0) ),
inference(resolution,[status(thm)],[c282,e_4_then_e_5]) ).
cnf(c965,plain,
( ~ cycle(e_2,e_4)
| ~ cycle(e_4,e_0) ),
inference(resolution,[status(thm)],[c964,cycle3]) ).
cnf(c2106,plain,
( cycle(e_4,e_1)
| ~ cycle(e_2,e_4) ),
inference(resolution,[status(thm)],[c2101,c965]) ).
cnf(c2167,plain,
( cycle(e_4,e_1)
| cycle(e_2,e_0)
| cycle(e_2,e_1)
| cycle(e_2,e_2)
| cycle(e_2,e_3) ),
inference(resolution,[status(thm)],[c2106,c3]) ).
cnf(c2843,plain,
( cycle(e_4,e_1)
| cycle(e_2,e_0)
| cycle(e_2,e_2)
| cycle(e_2,e_3) ),
inference(resolution,[status(thm)],[c2167,c2122]) ).
cnf(c2924,plain,
( cycle(e_4,e_1)
| cycle(e_2,e_0)
| cycle(e_2,e_3) ),
inference(resolution,[status(thm)],[c2843,c2113]) ).
cnf(c3001,plain,
( cycle(e_4,e_1)
| cycle(e_2,e_0) ),
inference(resolution,[status(thm)],[c2924,c2120]) ).
cnf(c3014,plain,
( cycle(e_2,e_0)
| ~ cycle(e_2,e_4)
| ~ cycle(e_3,e_0) ),
inference(resolution,[status(thm)],[c3001,c1175]) ).
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(e_1_then_e_2,axiom,
next(e_1,e_2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_1_then_e_2) ).
cnf(c8,plain,
( ~ cycle(X85,X86)
| ~ cycle(X87,e_1)
| ~ next(X85,X87)
| ~ greater(X86,e_0)
| equalish(X86,e_2) ),
inference(resolution,[status(thm)],[cycle4,e_1_then_e_2]) ).
cnf(c121,plain,
( ~ cycle(X97,e_4)
| ~ cycle(X96,e_1)
| ~ next(X97,X96)
| equalish(e_4,e_2) ),
inference(resolution,[status(thm)],[c8,e_4_greater_e_0]) ).
cnf(c147,plain,
( ~ cycle(e_3,e_4)
| ~ cycle(e_4,e_1)
| equalish(e_4,e_2) ),
inference(resolution,[status(thm)],[c121,e_3_then_e_4]) ).
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(c283,plain,
( ~ cycle(e_3,e_4)
| ~ cycle(e_4,e_0)
| ~ cycle(X307,e_0)
| ~ next(e_4,X307) ),
inference(resolution,[status(thm)],[c18,e_4_greater_e_3]) ).
cnf(c967,plain,
( ~ cycle(e_3,e_4)
| ~ cycle(e_4,e_0)
| ~ cycle(e_5,e_0) ),
inference(resolution,[status(thm)],[c283,e_4_then_e_5]) ).
cnf(c968,plain,
( ~ cycle(e_3,e_4)
| ~ cycle(e_4,e_0) ),
inference(resolution,[status(thm)],[c967,cycle3]) ).
cnf(c2108,plain,
( cycle(e_4,e_1)
| ~ cycle(e_3,e_4) ),
inference(resolution,[status(thm)],[c2101,c968]) ).
cnf(c438,plain,
( ~ cycle(e_3,e_3)
| ~ cycle(e_4,e_0)
| ~ cycle(X412,e_0)
| ~ next(e_4,X412) ),
inference(resolution,[status(thm)],[c25,e_4_greater_e_3]) ).
cnf(c1114,plain,
( ~ cycle(e_3,e_3)
| ~ cycle(e_4,e_0)
| ~ cycle(e_5,e_0) ),
inference(resolution,[status(thm)],[c438,e_4_then_e_5]) ).
cnf(c1115,plain,
( ~ cycle(e_3,e_3)
| ~ cycle(e_4,e_0) ),
inference(resolution,[status(thm)],[c1114,cycle3]) ).
cnf(c2111,plain,
( cycle(e_4,e_1)
| ~ cycle(e_3,e_3) ),
inference(resolution,[status(thm)],[c2101,c1115]) ).
cnf(c265,plain,
( ~ cycle(e_3,e_2)
| ~ cycle(e_4,e_0)
| ~ cycle(X292,e_0)
| ~ next(e_4,X292) ),
inference(resolution,[status(thm)],[c17,e_4_greater_e_3]) ).
cnf(c941,plain,
( ~ cycle(e_3,e_2)
| ~ cycle(e_4,e_0)
| ~ cycle(e_5,e_0) ),
inference(resolution,[status(thm)],[c265,e_4_then_e_5]) ).
cnf(c942,plain,
( ~ cycle(e_3,e_2)
| ~ cycle(e_4,e_0) ),
inference(resolution,[status(thm)],[c941,cycle3]) ).
cnf(c2115,plain,
( cycle(e_4,e_1)
| ~ cycle(e_3,e_2) ),
inference(resolution,[status(thm)],[c2101,c942]) ).
cnf(element_3,axiom,
group_element(e_3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',element_3) ).
cnf(c5,plain,
( cycle(e_3,e_0)
| cycle(e_3,e_1)
| cycle(e_3,e_2)
| cycle(e_3,e_3)
| cycle(e_3,e_4) ),
inference(resolution,[status(thm)],[cycle2,element_3]) ).
cnf(c415,plain,
( ~ cycle(e_3,e_1)
| ~ cycle(e_4,e_0)
| ~ cycle(X397,e_0)
| ~ next(e_4,X397) ),
inference(resolution,[status(thm)],[c24,e_4_greater_e_3]) ).
cnf(c1088,plain,
( ~ cycle(e_3,e_1)
| ~ cycle(e_4,e_0)
| ~ cycle(e_5,e_0) ),
inference(resolution,[status(thm)],[c415,e_4_then_e_5]) ).
cnf(c1089,plain,
( ~ cycle(e_3,e_1)
| ~ cycle(e_4,e_0) ),
inference(resolution,[status(thm)],[c1088,cycle3]) ).
cnf(c2105,plain,
( cycle(e_4,e_1)
| ~ cycle(e_3,e_1) ),
inference(resolution,[status(thm)],[c2101,c1089]) ).
cnf(c2166,plain,
( cycle(e_4,e_1)
| cycle(e_3,e_0)
| cycle(e_3,e_2)
| cycle(e_3,e_3)
| cycle(e_3,e_4) ),
inference(resolution,[status(thm)],[c2105,c5]) ).
cnf(c2550,plain,
( cycle(e_4,e_1)
| cycle(e_3,e_0)
| cycle(e_3,e_3)
| cycle(e_3,e_4) ),
inference(resolution,[status(thm)],[c2166,c2115]) ).
cnf(c2647,plain,
( cycle(e_4,e_1)
| cycle(e_3,e_0)
| cycle(e_3,e_4) ),
inference(resolution,[status(thm)],[c2550,c2111]) ).
cnf(c2716,plain,
( cycle(e_4,e_1)
| cycle(e_3,e_0) ),
inference(resolution,[status(thm)],[c2647,c2108]) ).
cnf(c2744,plain,
( cycle(e_3,e_0)
| ~ cycle(e_3,e_4)
| equalish(e_4,e_2) ),
inference(resolution,[status(thm)],[c2716,c147]) ).
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(c123,plain,
( ~ cycle(X110,e_3)
| ~ cycle(X109,e_1)
| ~ next(X110,X109)
| equalish(e_3,e_2) ),
inference(resolution,[status(thm)],[c8,e_3_greater_e_0]) ).
cnf(c187,plain,
( ~ cycle(e_3,e_3)
| ~ cycle(e_4,e_1)
| equalish(e_3,e_2) ),
inference(resolution,[status(thm)],[c123,e_3_then_e_4]) ).
cnf(c2733,plain,
( cycle(e_3,e_0)
| ~ cycle(e_3,e_3)
| equalish(e_3,e_2) ),
inference(resolution,[status(thm)],[c2716,c187]) ).
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(c122,plain,
( ~ cycle(X105,e_1)
| ~ cycle(X104,e_1)
| ~ next(X105,X104)
| equalish(e_1,e_2) ),
inference(resolution,[status(thm)],[c8,e_1_greater_e_0]) ).
cnf(c165,plain,
( ~ cycle(e_3,e_1)
| ~ cycle(e_4,e_1)
| equalish(e_1,e_2) ),
inference(resolution,[status(thm)],[c122,e_3_then_e_4]) ).
cnf(c2728,plain,
( cycle(e_3,e_0)
| ~ cycle(e_3,e_1)
| equalish(e_1,e_2) ),
inference(resolution,[status(thm)],[c2716,c165]) ).
cnf(c2787,plain,
( cycle(e_3,e_0)
| equalish(e_1,e_2)
| cycle(e_3,e_2)
| cycle(e_3,e_3)
| cycle(e_3,e_4) ),
inference(resolution,[status(thm)],[c2728,c5]) ).
cnf(c3124,plain,
( cycle(e_3,e_0)
| cycle(e_3,e_2)
| cycle(e_3,e_3)
| cycle(e_3,e_4) ),
inference(resolution,[status(thm)],[c2787,e_1_is_not_e_2]) ).
cnf(c3254,plain,
( cycle(e_3,e_0)
| cycle(e_3,e_2)
| cycle(e_3,e_4)
| equalish(e_3,e_2) ),
inference(resolution,[status(thm)],[c3124,c2733]) ).
cnf(c3351,plain,
( cycle(e_3,e_0)
| cycle(e_3,e_2)
| cycle(e_3,e_4) ),
inference(resolution,[status(thm)],[c3254,e_3_is_not_e_2]) ).
cnf(c3423,plain,
( cycle(e_3,e_0)
| cycle(e_3,e_2)
| equalish(e_4,e_2) ),
inference(resolution,[status(thm)],[c3351,c2744]) ).
cnf(c3485,plain,
( cycle(e_3,e_0)
| cycle(e_3,e_2) ),
inference(resolution,[status(thm)],[c3423,e_4_is_not_e_2]) ).
cnf(c3527,plain,
( cycle(e_3,e_2)
| cycle(e_2,e_0)
| ~ cycle(e_2,e_4) ),
inference(resolution,[status(thm)],[c3485,c3014]) ).
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(c27,plain,
( ~ cycle(X174,e_2)
| ~ cycle(X176,e_0)
| ~ cycle(X175,e_1)
| ~ next(X176,X175)
| ~ greater(X176,X174) ),
inference(resolution,[status(thm)],[cycle5,e_2_greater_e_1]) ).
cnf(c472,plain,
( ~ cycle(e_2,e_2)
| ~ cycle(e_3,e_0)
| ~ cycle(X434,e_1)
| ~ next(e_3,X434) ),
inference(resolution,[status(thm)],[c27,e_3_greater_e_2]) ).
cnf(c1159,plain,
( ~ cycle(e_2,e_2)
| ~ cycle(e_3,e_0)
| ~ cycle(e_4,e_1) ),
inference(resolution,[status(thm)],[c472,e_3_then_e_4]) ).
cnf(c3019,plain,
( cycle(e_2,e_0)
| ~ cycle(e_2,e_2)
| ~ cycle(e_3,e_0) ),
inference(resolution,[status(thm)],[c3001,c1159]) ).
cnf(c3525,plain,
( cycle(e_3,e_2)
| cycle(e_2,e_0)
| ~ cycle(e_2,e_2) ),
inference(resolution,[status(thm)],[c3485,c3019]) ).
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(c19,plain,
( ~ cycle(X134,e_3)
| ~ cycle(X136,e_0)
| ~ cycle(X135,e_1)
| ~ next(X136,X135)
| ~ greater(X136,X134) ),
inference(resolution,[status(thm)],[cycle5,e_3_greater_e_1]) ).
cnf(c297,plain,
( ~ cycle(e_2,e_3)
| ~ cycle(e_3,e_0)
| ~ cycle(X314,e_1)
| ~ next(e_3,X314) ),
inference(resolution,[status(thm)],[c19,e_3_greater_e_2]) ).
cnf(c984,plain,
( ~ cycle(e_2,e_3)
| ~ cycle(e_3,e_0)
| ~ cycle(e_4,e_1) ),
inference(resolution,[status(thm)],[c297,e_3_then_e_4]) ).
cnf(c3012,plain,
( cycle(e_2,e_0)
| ~ cycle(e_2,e_3)
| ~ cycle(e_3,e_0) ),
inference(resolution,[status(thm)],[c3001,c984]) ).
cnf(c3507,plain,
( cycle(e_3,e_2)
| cycle(e_2,e_0)
| ~ cycle(e_2,e_3) ),
inference(resolution,[status(thm)],[c3485,c3012]) ).
cnf(c3567,plain,
( cycle(e_3,e_2)
| cycle(e_2,e_0)
| cycle(e_2,e_1)
| cycle(e_2,e_2)
| cycle(e_2,e_4) ),
inference(resolution,[status(thm)],[c3507,c3]) ).
cnf(c3658,plain,
( cycle(e_3,e_2)
| cycle(e_2,e_0)
| cycle(e_2,e_1)
| cycle(e_2,e_4) ),
inference(resolution,[status(thm)],[c3567,c3525]) ).
cnf(c3771,plain,
( cycle(e_3,e_2)
| cycle(e_2,e_0)
| cycle(e_2,e_1) ),
inference(resolution,[status(thm)],[c3658,c3527]) ).
cnf(c3782,plain,
( cycle(e_2,e_0)
| cycle(e_2,e_1)
| ~ cycle(e_2,e_2)
| equalish(e_2,e_3) ),
inference(resolution,[status(thm)],[c3771,c79]) ).
cnf(c74,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(c84,plain,
( ~ cycle(e_2,e_4)
| ~ cycle(e_3,e_2)
| equalish(e_4,e_3) ),
inference(resolution,[status(thm)],[c74,e_2_then_e_3]) ).
cnf(c3776,plain,
( cycle(e_2,e_0)
| cycle(e_2,e_1)
| ~ cycle(e_2,e_4)
| equalish(e_4,e_3) ),
inference(resolution,[status(thm)],[c3771,c84]) ).
cnf(c3856,plain,
( cycle(e_2,e_0)
| cycle(e_2,e_1)
| equalish(e_4,e_3)
| cycle(e_2,e_2)
| cycle(e_2,e_3) ),
inference(resolution,[status(thm)],[c3776,c3]) ).
cnf(c3911,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)],[c3856,e_4_is_not_e_3]) ).
cnf(c4022,plain,
( cycle(e_2,e_0)
| cycle(e_2,e_1)
| cycle(e_2,e_3)
| equalish(e_2,e_3) ),
inference(resolution,[status(thm)],[c3911,c3782]) ).
cnf(c4110,plain,
( cycle(e_2,e_0)
| cycle(e_2,e_1)
| cycle(e_2,e_3) ),
inference(resolution,[status(thm)],[c4022,e_2_is_not_e_3]) ).
cnf(e_5_greater_e_2,axiom,
greater(e_5,e_2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_5_greater_e_2) ).
cnf(cycle6,axiom,
( ~ cycle(X19,e_0)
| ~ product(X19,e_1,X20)
| ~ greater(X20,X19) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cycle6) ).
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(c528,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)
| product(e_2,e_1,e_5) ),
inference(resolution,[status(thm)],[c40,element_2]) ).
cnf(c1763,plain,
( product(e_2,e_1,e_2)
| product(e_2,e_1,e_3)
| product(e_2,e_1,e_4)
| product(e_2,e_1,e_5)
| equalish(e_2,e_1) ),
inference(resolution,[status(thm)],[c528,c47]) ).
cnf(c4445,plain,
( product(e_2,e_1,e_2)
| product(e_2,e_1,e_3)
| product(e_2,e_1,e_4)
| product(e_2,e_1,e_5) ),
inference(resolution,[status(thm)],[c1763,e_2_is_not_e_1]) ).
cnf(c4449,plain,
( product(e_2,e_1,e_3)
| product(e_2,e_1,e_4)
| product(e_2,e_1,e_5)
| equalish(e_1,e_2) ),
inference(resolution,[status(thm)],[c4445,c38]) ).
cnf(c4489,plain,
( product(e_2,e_1,e_3)
| product(e_2,e_1,e_4)
| product(e_2,e_1,e_5) ),
inference(resolution,[status(thm)],[c4449,e_1_is_not_e_2]) ).
cnf(c4501,plain,
( product(e_2,e_1,e_3)
| product(e_2,e_1,e_5)
| ~ cycle(e_2,e_0)
| ~ greater(e_4,e_2) ),
inference(resolution,[status(thm)],[c4489,cycle6]) ).
cnf(c4708,plain,
( product(e_2,e_1,e_3)
| product(e_2,e_1,e_5)
| ~ cycle(e_2,e_0) ),
inference(resolution,[status(thm)],[c4501,e_4_greater_e_2]) ).
cnf(c4710,plain,
( product(e_2,e_1,e_3)
| product(e_2,e_1,e_5)
| cycle(e_2,e_1)
| cycle(e_2,e_3) ),
inference(resolution,[status(thm)],[c4708,c4110]) ).
cnf(product_total_function2,axiom,
( ~ product(X22,X25,X23)
| ~ product(X22,X25,X24)
| equalish(X23,X24) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',product_total_function2) ).
cnf(c4495,plain,
( product(e_2,e_1,e_4)
| product(e_2,e_1,e_5)
| ~ cycle(e_2,e_0)
| ~ greater(e_3,e_2) ),
inference(resolution,[status(thm)],[c4489,cycle6]) ).
cnf(c4519,plain,
( product(e_2,e_1,e_4)
| product(e_2,e_1,e_5)
| ~ cycle(e_2,e_0) ),
inference(resolution,[status(thm)],[c4495,e_3_greater_e_2]) ).
cnf(c4521,plain,
( product(e_2,e_1,e_4)
| product(e_2,e_1,e_5)
| cycle(e_2,e_1)
| cycle(e_2,e_3) ),
inference(resolution,[status(thm)],[c4519,c4110]) ).
cnf(c4789,plain,
( product(e_2,e_1,e_5)
| cycle(e_2,e_1)
| cycle(e_2,e_3)
| ~ product(e_2,e_1,X719)
| equalish(X719,e_4) ),
inference(resolution,[status(thm)],[c4521,product_total_function2]) ).
cnf(c5741,plain,
( product(e_2,e_1,e_5)
| cycle(e_2,e_1)
| cycle(e_2,e_3)
| equalish(e_3,e_4) ),
inference(resolution,[status(thm)],[c4789,c4710]) ).
cnf(c5799,plain,
( product(e_2,e_1,e_5)
| cycle(e_2,e_1)
| cycle(e_2,e_3) ),
inference(resolution,[status(thm)],[c5741,e_3_is_not_e_4]) ).
cnf(c5809,plain,
( cycle(e_2,e_1)
| cycle(e_2,e_3)
| ~ cycle(e_2,e_0)
| ~ greater(e_5,e_2) ),
inference(resolution,[status(thm)],[c5799,cycle6]) ).
cnf(c5909,plain,
( cycle(e_2,e_1)
| cycle(e_2,e_3)
| ~ cycle(e_2,e_0) ),
inference(resolution,[status(thm)],[c5809,e_5_greater_e_2]) ).
cnf(c5910,plain,
( cycle(e_2,e_1)
| cycle(e_2,e_3) ),
inference(resolution,[status(thm)],[c5909,c4110]) ).
cnf(cycle7,axiom,
( ~ cycle(X29,X32)
| ~ product(X29,e_1,X30)
| ~ greater(X32,e_0)
| ~ next(X29,X31)
| equalish(X30,X31) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cycle7) ).
cnf(c4502,plain,
( product(e_2,e_1,e_3)
| product(e_2,e_1,e_4)
| ~ product(X649,e_1,e_5)
| equalish(X649,e_2) ),
inference(resolution,[status(thm)],[c4489,product_left_cancellation]) ).
cnf(c4523,plain,
( product(e_2,e_1,e_4)
| product(e_2,e_1,e_5)
| cycle(e_4,e_1) ),
inference(resolution,[status(thm)],[c4519,c3001]) ).
cnf(c4530,plain,
( product(e_2,e_1,e_5)
| cycle(e_4,e_1)
| ~ cycle(e_2,e_0)
| ~ greater(e_4,e_2) ),
inference(resolution,[status(thm)],[c4523,cycle6]) ).
cnf(c4574,plain,
( product(e_2,e_1,e_5)
| cycle(e_4,e_1)
| ~ cycle(e_2,e_0) ),
inference(resolution,[status(thm)],[c4530,e_4_greater_e_2]) ).
cnf(c4578,plain,
( product(e_2,e_1,e_5)
| cycle(e_4,e_1) ),
inference(resolution,[status(thm)],[c4574,c3001]) ).
cnf(c4585,plain,
( cycle(e_4,e_1)
| ~ cycle(e_2,e_0)
| ~ greater(e_5,e_2) ),
inference(resolution,[status(thm)],[c4578,cycle6]) ).
cnf(c4621,plain,
( cycle(e_4,e_1)
| ~ cycle(e_2,e_0) ),
inference(resolution,[status(thm)],[c4585,e_5_greater_e_2]) ).
cnf(c4625,plain,
cycle(e_4,e_1),
inference(resolution,[status(thm)],[c4621,c3001]) ).
cnf(c529,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)
| product(e_4,e_1,e_5) ),
inference(resolution,[status(thm)],[c40,element_4]) ).
cnf(c1797,plain,
( product(e_4,e_1,e_2)
| product(e_4,e_1,e_3)
| product(e_4,e_1,e_4)
| product(e_4,e_1,e_5)
| equalish(e_4,e_1) ),
inference(resolution,[status(thm)],[c529,c47]) ).
cnf(c5199,plain,
( product(e_4,e_1,e_2)
| product(e_4,e_1,e_3)
| product(e_4,e_1,e_4)
| product(e_4,e_1,e_5) ),
inference(resolution,[status(thm)],[c1797,e_4_is_not_e_1]) ).
cnf(c6291,plain,
( product(e_4,e_1,e_2)
| product(e_4,e_1,e_3)
| product(e_4,e_1,e_5)
| equalish(e_1,e_4) ),
inference(resolution,[status(thm)],[c5199,c38]) ).
cnf(c6349,plain,
( product(e_4,e_1,e_2)
| product(e_4,e_1,e_3)
| product(e_4,e_1,e_5) ),
inference(resolution,[status(thm)],[c6291,e_1_is_not_e_4]) ).
cnf(c6357,plain,
( product(e_4,e_1,e_3)
| product(e_4,e_1,e_5)
| ~ product(X839,e_1,e_2)
| equalish(X839,e_4) ),
inference(resolution,[status(thm)],[c6349,product_left_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(c75,plain,
( ~ cycle(X80,e_1)
| ~ cycle(X79,X80)
| ~ next(X80,X79)
| equalish(e_1,X79) ),
inference(resolution,[status(thm)],[c7,e_1_greater_e_0]) ).
cnf(c94,plain,
( ~ cycle(e_2,e_1)
| ~ cycle(e_3,e_2)
| equalish(e_1,e_3) ),
inference(resolution,[status(thm)],[c75,e_2_then_e_3]) ).
cnf(c3541,plain,
( cycle(e_3,e_0)
| ~ cycle(e_2,e_1)
| equalish(e_1,e_3) ),
inference(resolution,[status(thm)],[c3485,c94]) ).
cnf(c4153,plain,
( cycle(e_2,e_0)
| cycle(e_2,e_3)
| cycle(e_3,e_0)
| equalish(e_1,e_3) ),
inference(resolution,[status(thm)],[c4110,c3541]) ).
cnf(c4294,plain,
( cycle(e_2,e_0)
| cycle(e_2,e_3)
| cycle(e_3,e_0) ),
inference(resolution,[status(thm)],[c4153,e_1_is_not_e_3]) ).
cnf(c4709,plain,
( product(e_2,e_1,e_3)
| product(e_2,e_1,e_5)
| cycle(e_2,e_3)
| cycle(e_3,e_0) ),
inference(resolution,[status(thm)],[c4708,c4294]) ).
cnf(c4520,plain,
( product(e_2,e_1,e_4)
| product(e_2,e_1,e_5)
| cycle(e_2,e_3)
| cycle(e_3,e_0) ),
inference(resolution,[status(thm)],[c4519,c4294]) ).
cnf(c4733,plain,
( product(e_2,e_1,e_5)
| cycle(e_2,e_3)
| cycle(e_3,e_0)
| ~ product(e_2,e_1,X676)
| equalish(X676,e_4) ),
inference(resolution,[status(thm)],[c4520,product_total_function2]) ).
cnf(c5335,plain,
( product(e_2,e_1,e_5)
| cycle(e_2,e_3)
| cycle(e_3,e_0)
| equalish(e_3,e_4) ),
inference(resolution,[status(thm)],[c4733,c4709]) ).
cnf(c5398,plain,
( product(e_2,e_1,e_5)
| cycle(e_2,e_3)
| cycle(e_3,e_0) ),
inference(resolution,[status(thm)],[c5335,e_3_is_not_e_4]) ).
cnf(c5408,plain,
( cycle(e_2,e_3)
| cycle(e_3,e_0)
| ~ cycle(e_2,e_0)
| ~ greater(e_5,e_2) ),
inference(resolution,[status(thm)],[c5398,cycle6]) ).
cnf(c5501,plain,
( cycle(e_2,e_3)
| cycle(e_3,e_0)
| ~ cycle(e_2,e_0) ),
inference(resolution,[status(thm)],[c5408,e_5_greater_e_2]) ).
cnf(c5502,plain,
( cycle(e_2,e_3)
| cycle(e_3,e_0) ),
inference(resolution,[status(thm)],[c5501,c4294]) ).
cnf(e_5_greater_e_3,axiom,
greater(e_5,e_3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_5_greater_e_3) ).
cnf(c530,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)
| product(e_3,e_1,e_5) ),
inference(resolution,[status(thm)],[c40,element_3]) ).
cnf(c1831,plain,
( product(e_3,e_1,e_2)
| product(e_3,e_1,e_3)
| product(e_3,e_1,e_4)
| product(e_3,e_1,e_5)
| equalish(e_3,e_1) ),
inference(resolution,[status(thm)],[c530,c47]) ).
cnf(c5720,plain,
( product(e_3,e_1,e_2)
| product(e_3,e_1,e_3)
| product(e_3,e_1,e_4)
| product(e_3,e_1,e_5) ),
inference(resolution,[status(thm)],[c1831,e_3_is_not_e_1]) ).
cnf(c6597,plain,
( product(e_3,e_1,e_2)
| product(e_3,e_1,e_4)
| product(e_3,e_1,e_5)
| equalish(e_1,e_3) ),
inference(resolution,[status(thm)],[c5720,c38]) ).
cnf(c6681,plain,
( product(e_3,e_1,e_2)
| product(e_3,e_1,e_4)
| product(e_3,e_1,e_5) ),
inference(resolution,[status(thm)],[c6597,e_1_is_not_e_3]) ).
cnf(c6707,plain,
( product(e_3,e_1,e_2)
| product(e_3,e_1,e_5)
| ~ cycle(e_3,e_0)
| ~ greater(e_4,e_3) ),
inference(resolution,[status(thm)],[c6681,cycle6]) ).
cnf(c6746,plain,
( product(e_3,e_1,e_2)
| product(e_3,e_1,e_5)
| ~ cycle(e_3,e_0) ),
inference(resolution,[status(thm)],[c6707,e_4_greater_e_3]) ).
cnf(c6747,plain,
( product(e_3,e_1,e_2)
| product(e_3,e_1,e_5)
| cycle(e_2,e_3) ),
inference(resolution,[status(thm)],[c6746,c5502]) ).
cnf(c6775,plain,
( product(e_3,e_1,e_2)
| cycle(e_2,e_3)
| ~ cycle(e_3,e_0)
| ~ greater(e_5,e_3) ),
inference(resolution,[status(thm)],[c6747,cycle6]) ).
cnf(c6870,plain,
( product(e_3,e_1,e_2)
| cycle(e_2,e_3)
| ~ cycle(e_3,e_0) ),
inference(resolution,[status(thm)],[c6775,e_5_greater_e_3]) ).
cnf(c6871,plain,
( product(e_3,e_1,e_2)
| cycle(e_2,e_3) ),
inference(resolution,[status(thm)],[c6870,c5502]) ).
cnf(c6884,plain,
( cycle(e_2,e_3)
| product(e_4,e_1,e_3)
| product(e_4,e_1,e_5)
| equalish(e_3,e_4) ),
inference(resolution,[status(thm)],[c6871,c6357]) ).
cnf(c7339,plain,
( cycle(e_2,e_3)
| product(e_4,e_1,e_3)
| product(e_4,e_1,e_5) ),
inference(resolution,[status(thm)],[c6884,e_3_is_not_e_4]) ).
cnf(c7368,plain,
( cycle(e_2,e_3)
| product(e_4,e_1,e_5)
| ~ cycle(e_4,X1897)
| ~ greater(X1897,e_0)
| ~ next(e_4,X1898)
| equalish(e_3,X1898) ),
inference(resolution,[status(thm)],[c7339,cycle7]) ).
cnf(c21517,plain,
( cycle(e_2,e_3)
| product(e_4,e_1,e_5)
| ~ cycle(e_4,X1899)
| ~ greater(X1899,e_0)
| equalish(e_3,e_5) ),
inference(resolution,[status(thm)],[c7368,e_4_then_e_5]) ).
cnf(c21520,plain,
( cycle(e_2,e_3)
| product(e_4,e_1,e_5)
| ~ cycle(e_4,e_1)
| equalish(e_3,e_5) ),
inference(resolution,[status(thm)],[c21517,e_1_greater_e_0]) ).
cnf(c21523,plain,
( cycle(e_2,e_3)
| product(e_4,e_1,e_5)
| equalish(e_3,e_5) ),
inference(resolution,[status(thm)],[c21520,c4625]) ).
cnf(c21584,plain,
( cycle(e_2,e_3)
| product(e_4,e_1,e_5) ),
inference(resolution,[status(thm)],[c21523,e_3_is_not_e_5]) ).
cnf(c21629,plain,
( cycle(e_2,e_3)
| product(e_2,e_1,e_3)
| product(e_2,e_1,e_4)
| equalish(e_4,e_2) ),
inference(resolution,[status(thm)],[c21584,c4502]) ).
cnf(c22716,plain,
( cycle(e_2,e_3)
| product(e_2,e_1,e_3)
| product(e_2,e_1,e_4) ),
inference(resolution,[status(thm)],[c21629,e_4_is_not_e_2]) ).
cnf(c22756,plain,
( cycle(e_2,e_3)
| product(e_2,e_1,e_4)
| ~ product(e_2,X1971,e_3)
| equalish(X1971,e_1) ),
inference(resolution,[status(thm)],[c22716,product_right_cancellation]) ).
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(c6887,plain,
( cycle(e_2,e_3)
| ~ cycle(e_3,X918)
| ~ greater(X918,e_0)
| ~ next(e_3,X919)
| equalish(e_2,X919) ),
inference(resolution,[status(thm)],[c6871,cycle7]) ).
cnf(c7141,plain,
( cycle(e_2,e_3)
| ~ cycle(e_3,X920)
| ~ greater(X920,e_0)
| equalish(e_2,e_4) ),
inference(resolution,[status(thm)],[c6887,e_3_then_e_4]) ).
cnf(c7142,plain,
( cycle(e_2,e_3)
| ~ cycle(e_3,e_2)
| equalish(e_2,e_4) ),
inference(resolution,[status(thm)],[c7141,e_2_greater_e_0]) ).
cnf(c4633,plain,
( ~ cycle(e_2,e_3)
| ~ cycle(e_3,e_0) ),
inference(resolution,[status(thm)],[c4625,c984]) ).
cnf(c4656,plain,
( ~ cycle(e_2,e_3)
| cycle(e_3,e_2) ),
inference(resolution,[status(thm)],[c4633,c3485]) ).
cnf(c6894,plain,
( product(e_3,e_1,e_2)
| cycle(e_3,e_2) ),
inference(resolution,[status(thm)],[c6871,c4656]) ).
cnf(qg3,negated_conjecture,
( ~ product(X58,X61,X60)
| ~ product(X61,X58,X59)
| product(X60,X59,X58) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',qg3) ).
cnf(c33,plain,
( ~ product(X34,X34,X35)
| equalish(X35,X34) ),
inference(resolution,[status(thm)],[product_total_function2,product_idempotence]) ).
cnf(c6901,plain,
( cycle(e_3,e_2)
| ~ product(e_1,e_3,X901)
| product(X901,e_2,e_1) ),
inference(resolution,[status(thm)],[c6894,qg3]) ).
cnf(c43,plain,
( ~ group_element(X198)
| product(X198,e_3,e_1)
| product(X198,e_3,e_2)
| product(X198,e_3,e_3)
| product(X198,e_3,e_4)
| product(X198,e_3,e_5) ),
inference(resolution,[status(thm)],[product_total_function1,element_3]) ).
cnf(c564,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)
| product(e_1,e_3,e_5) ),
inference(resolution,[status(thm)],[c43,element_1]) ).
cnf(c2302,plain,
( product(e_1,e_3,e_2)
| product(e_1,e_3,e_3)
| product(e_1,e_3,e_4)
| product(e_1,e_3,e_5)
| equalish(e_3,e_1) ),
inference(resolution,[status(thm)],[c564,c38]) ).
cnf(c11805,plain,
( product(e_1,e_3,e_2)
| product(e_1,e_3,e_3)
| product(e_1,e_3,e_4)
| product(e_1,e_3,e_5) ),
inference(resolution,[status(thm)],[c2302,e_3_is_not_e_1]) ).
cnf(c12437,plain,
( product(e_1,e_3,e_2)
| product(e_1,e_3,e_4)
| product(e_1,e_3,e_5)
| equalish(e_1,e_3) ),
inference(resolution,[status(thm)],[c11805,c47]) ).
cnf(c12521,plain,
( product(e_1,e_3,e_2)
| product(e_1,e_3,e_4)
| product(e_1,e_3,e_5) ),
inference(resolution,[status(thm)],[c12437,e_1_is_not_e_3]) ).
cnf(c12549,plain,
( product(e_1,e_3,e_4)
| product(e_1,e_3,e_5)
| cycle(e_3,e_2)
| product(e_2,e_2,e_1) ),
inference(resolution,[status(thm)],[c12521,c6901]) ).
cnf(c12712,plain,
( product(e_1,e_3,e_4)
| product(e_1,e_3,e_5)
| cycle(e_3,e_2)
| equalish(e_1,e_2) ),
inference(resolution,[status(thm)],[c12549,c33]) ).
cnf(c12768,plain,
( product(e_1,e_3,e_4)
| product(e_1,e_3,e_5)
| cycle(e_3,e_2) ),
inference(resolution,[status(thm)],[c12712,e_1_is_not_e_2]) ).
cnf(c12769,plain,
( product(e_1,e_3,e_5)
| cycle(e_3,e_2)
| ~ product(e_3,e_1,X1379)
| product(X1379,e_4,e_3) ),
inference(resolution,[status(thm)],[c12768,qg3]) ).
cnf(c13251,plain,
( product(e_1,e_3,e_5)
| cycle(e_3,e_2)
| product(e_2,e_4,e_3) ),
inference(resolution,[status(thm)],[c12769,c6894]) ).
cnf(c13253,plain,
( cycle(e_3,e_2)
| product(e_2,e_4,e_3)
| ~ product(e_3,e_1,X1500)
| product(X1500,e_5,e_3) ),
inference(resolution,[status(thm)],[c13251,qg3]) ).
cnf(c15432,plain,
( cycle(e_3,e_2)
| product(e_2,e_4,e_3)
| product(e_2,e_5,e_3) ),
inference(resolution,[status(thm)],[c13253,c6894]) ).
cnf(c15462,plain,
( product(e_2,e_4,e_3)
| product(e_2,e_5,e_3)
| cycle(e_2,e_3)
| equalish(e_2,e_4) ),
inference(resolution,[status(thm)],[c15432,c7142]) ).
cnf(c18036,plain,
( product(e_2,e_4,e_3)
| product(e_2,e_5,e_3)
| cycle(e_2,e_3) ),
inference(resolution,[status(thm)],[c15462,e_2_is_not_e_4]) ).
cnf(c18094,plain,
( product(e_2,e_4,e_3)
| cycle(e_2,e_3)
| ~ product(e_2,X1611,e_3)
| equalish(X1611,e_5) ),
inference(resolution,[status(thm)],[c18036,product_right_cancellation]) ).
cnf(c22764,plain,
( cycle(e_2,e_3)
| product(e_2,e_1,e_4)
| product(e_2,e_4,e_3)
| equalish(e_1,e_5) ),
inference(resolution,[status(thm)],[c22716,c18094]) ).
cnf(c33370,plain,
( cycle(e_2,e_3)
| product(e_2,e_1,e_4)
| product(e_2,e_4,e_3) ),
inference(resolution,[status(thm)],[c22764,e_1_is_not_e_5]) ).
cnf(c33503,plain,
( cycle(e_2,e_3)
| product(e_2,e_1,e_4)
| equalish(e_4,e_1) ),
inference(resolution,[status(thm)],[c33370,c22756]) ).
cnf(c33587,plain,
( cycle(e_2,e_3)
| product(e_2,e_1,e_4) ),
inference(resolution,[status(thm)],[c33503,e_4_is_not_e_1]) ).
cnf(c33631,plain,
( cycle(e_2,e_3)
| ~ cycle(e_2,X2216)
| ~ greater(X2216,e_0)
| ~ next(e_2,X2217)
| equalish(e_4,X2217) ),
inference(resolution,[status(thm)],[c33587,cycle7]) ).
cnf(c34445,plain,
( cycle(e_2,e_3)
| ~ cycle(e_2,X2218)
| ~ greater(X2218,e_0)
| equalish(e_4,e_3) ),
inference(resolution,[status(thm)],[c33631,e_2_then_e_3]) ).
cnf(c34448,plain,
( cycle(e_2,e_3)
| ~ cycle(e_2,e_1)
| equalish(e_4,e_3) ),
inference(resolution,[status(thm)],[c34445,e_1_greater_e_0]) ).
cnf(c34451,plain,
( cycle(e_2,e_3)
| equalish(e_4,e_3) ),
inference(resolution,[status(thm)],[c34448,c5910]) ).
cnf(c34489,plain,
cycle(e_2,e_3),
inference(resolution,[status(thm)],[c34451,e_4_is_not_e_3]) ).
cnf(c4497,plain,
( product(e_2,e_1,e_3)
| product(e_2,e_1,e_5)
| ~ cycle(e_2,X2058)
| ~ greater(X2058,e_0)
| ~ next(e_2,X2059)
| equalish(e_4,X2059) ),
inference(resolution,[status(thm)],[c4489,cycle7]) ).
cnf(c24532,plain,
( product(e_2,e_1,e_3)
| product(e_2,e_1,e_5)
| ~ cycle(e_2,X2404)
| ~ greater(X2404,e_0)
| equalish(e_4,e_3) ),
inference(resolution,[status(thm)],[c4497,e_2_then_e_3]) ).
cnf(c40400,plain,
( product(e_2,e_1,e_3)
| product(e_2,e_1,e_5)
| ~ cycle(e_2,e_3)
| equalish(e_4,e_3) ),
inference(resolution,[status(thm)],[c24532,e_3_greater_e_0]) ).
cnf(c40402,plain,
( product(e_2,e_1,e_3)
| product(e_2,e_1,e_5)
| equalish(e_4,e_3) ),
inference(resolution,[status(thm)],[c40400,c34489]) ).
cnf(c40439,plain,
( product(e_2,e_1,e_3)
| product(e_2,e_1,e_5) ),
inference(resolution,[status(thm)],[c40402,e_4_is_not_e_3]) ).
cnf(c40461,plain,
( product(e_2,e_1,e_3)
| ~ cycle(e_2,X2429)
| ~ greater(X2429,e_0)
| ~ next(e_2,X2430)
| equalish(e_5,X2430) ),
inference(resolution,[status(thm)],[c40439,cycle7]) ).
cnf(c40752,plain,
( product(e_2,e_1,e_3)
| ~ cycle(e_2,X2431)
| ~ greater(X2431,e_0)
| equalish(e_5,e_3) ),
inference(resolution,[status(thm)],[c40461,e_2_then_e_3]) ).
cnf(c40756,plain,
( product(e_2,e_1,e_3)
| ~ cycle(e_2,e_3)
| equalish(e_5,e_3) ),
inference(resolution,[status(thm)],[c40752,e_3_greater_e_0]) ).
cnf(c40758,plain,
( product(e_2,e_1,e_3)
| equalish(e_5,e_3) ),
inference(resolution,[status(thm)],[c40756,c34489]) ).
cnf(c40776,plain,
product(e_2,e_1,e_3),
inference(resolution,[status(thm)],[c40758,e_5_is_not_e_3]) ).
cnf(c40780,plain,
( product(e_5,e_1,e_2)
| product(e_5,e_1,e_4)
| equalish(e_2,e_5) ),
inference(resolution,[status(thm)],[c40776,c8070]) ).
cnf(c41024,plain,
( product(e_5,e_1,e_2)
| product(e_5,e_1,e_4) ),
inference(resolution,[status(thm)],[c40780,e_2_is_not_e_5]) ).
cnf(c41043,plain,
( product(e_5,e_1,e_2)
| ~ product(X2451,e_1,e_4)
| equalish(X2451,e_5) ),
inference(resolution,[status(thm)],[c41024,product_left_cancellation]) ).
cnf(c6713,plain,
( product(e_3,e_1,e_2)
| product(e_3,e_1,e_4)
| ~ product(X929,e_1,e_5)
| equalish(X929,e_3) ),
inference(resolution,[status(thm)],[c6681,product_left_cancellation]) ).
cnf(c6369,plain,
( product(e_4,e_1,e_2)
| product(e_4,e_1,e_5)
| ~ product(X843,e_1,e_3)
| equalish(X843,e_4) ),
inference(resolution,[status(thm)],[c6349,product_left_cancellation]) ).
cnf(c40782,plain,
( product(e_4,e_1,e_2)
| product(e_4,e_1,e_5)
| equalish(e_2,e_4) ),
inference(resolution,[status(thm)],[c40776,c6369]) ).
cnf(c41195,plain,
( product(e_4,e_1,e_2)
| product(e_4,e_1,e_5) ),
inference(resolution,[status(thm)],[c40782,e_2_is_not_e_4]) ).
cnf(c41199,plain,
( product(e_4,e_1,e_5)
| ~ cycle(e_4,X2640)
| ~ greater(X2640,e_0)
| ~ next(e_4,X2641)
| equalish(e_2,X2641) ),
inference(resolution,[status(thm)],[c41195,cycle7]) ).
cnf(c45413,plain,
( product(e_4,e_1,e_5)
| ~ cycle(e_4,X2642)
| ~ greater(X2642,e_0)
| equalish(e_2,e_5) ),
inference(resolution,[status(thm)],[c41199,e_4_then_e_5]) ).
cnf(c45416,plain,
( product(e_4,e_1,e_5)
| ~ cycle(e_4,e_1)
| equalish(e_2,e_5) ),
inference(resolution,[status(thm)],[c45413,e_1_greater_e_0]) ).
cnf(c45419,plain,
( product(e_4,e_1,e_5)
| equalish(e_2,e_5) ),
inference(resolution,[status(thm)],[c45416,c4625]) ).
cnf(c45439,plain,
product(e_4,e_1,e_5),
inference(resolution,[status(thm)],[c45419,e_2_is_not_e_5]) ).
cnf(c45453,plain,
( product(e_3,e_1,e_2)
| product(e_3,e_1,e_4)
| equalish(e_4,e_3) ),
inference(resolution,[status(thm)],[c45439,c6713]) ).
cnf(c45970,plain,
( product(e_3,e_1,e_2)
| product(e_3,e_1,e_4) ),
inference(resolution,[status(thm)],[c45453,e_4_is_not_e_3]) ).
cnf(c45986,plain,
( product(e_3,e_1,e_4)
| ~ product(e_3,X2678,e_2)
| equalish(X2678,e_1) ),
inference(resolution,[status(thm)],[c45970,product_right_cancellation]) ).
cnf(c41,plain,
( ~ group_element(X190)
| product(X190,e_2,e_1)
| product(X190,e_2,e_2)
| product(X190,e_2,e_3)
| product(X190,e_2,e_4)
| product(X190,e_2,e_5) ),
inference(resolution,[status(thm)],[product_total_function1,element_2]) ).
cnf(c540,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)
| product(e_1,e_2,e_5) ),
inference(resolution,[status(thm)],[c41,element_1]) ).
cnf(c2012,plain,
( product(e_1,e_2,e_2)
| product(e_1,e_2,e_3)
| product(e_1,e_2,e_4)
| product(e_1,e_2,e_5)
| equalish(e_2,e_1) ),
inference(resolution,[status(thm)],[c540,c38]) ).
cnf(c7003,plain,
( product(e_1,e_2,e_2)
| product(e_1,e_2,e_3)
| product(e_1,e_2,e_4)
| product(e_1,e_2,e_5) ),
inference(resolution,[status(thm)],[c2012,e_2_is_not_e_1]) ).
cnf(c9513,plain,
( product(e_1,e_2,e_3)
| product(e_1,e_2,e_4)
| product(e_1,e_2,e_5)
| equalish(e_1,e_2) ),
inference(resolution,[status(thm)],[c7003,c47]) ).
cnf(c9619,plain,
( product(e_1,e_2,e_3)
| product(e_1,e_2,e_4)
| product(e_1,e_2,e_5) ),
inference(resolution,[status(thm)],[c9513,e_1_is_not_e_2]) ).
cnf(c9620,plain,
( product(e_1,e_2,e_4)
| product(e_1,e_2,e_5)
| ~ product(e_2,e_1,X1121)
| product(X1121,e_3,e_2) ),
inference(resolution,[status(thm)],[c9619,qg3]) ).
cnf(c40787,plain,
( product(e_1,e_2,e_4)
| product(e_1,e_2,e_5)
| product(e_3,e_3,e_2) ),
inference(resolution,[status(thm)],[c40776,c9620]) ).
cnf(c42296,plain,
( product(e_1,e_2,e_4)
| product(e_1,e_2,e_5)
| equalish(e_2,e_3) ),
inference(resolution,[status(thm)],[c40787,c33]) ).
cnf(c42334,plain,
( product(e_1,e_2,e_4)
| product(e_1,e_2,e_5) ),
inference(resolution,[status(thm)],[c42296,e_2_is_not_e_3]) ).
cnf(c42342,plain,
( product(e_1,e_2,e_5)
| ~ product(e_2,e_1,X2532)
| product(X2532,e_4,e_2) ),
inference(resolution,[status(thm)],[c42334,qg3]) ).
cnf(c42699,plain,
( product(e_1,e_2,e_5)
| product(e_3,e_4,e_2) ),
inference(resolution,[status(thm)],[c42342,c40776]) ).
cnf(c42709,plain,
( product(e_3,e_4,e_2)
| ~ product(e_2,e_1,X2565)
| product(X2565,e_5,e_2) ),
inference(resolution,[status(thm)],[c42699,qg3]) ).
cnf(c43870,plain,
( product(e_3,e_4,e_2)
| product(e_3,e_5,e_2) ),
inference(resolution,[status(thm)],[c42709,c40776]) ).
cnf(c43890,plain,
( product(e_3,e_5,e_2)
| ~ product(e_3,X2568,e_2)
| equalish(X2568,e_4) ),
inference(resolution,[status(thm)],[c43870,product_right_cancellation]) ).
cnf(c45980,plain,
( product(e_3,e_1,e_4)
| product(e_3,e_5,e_2)
| equalish(e_1,e_4) ),
inference(resolution,[status(thm)],[c45970,c43890]) ).
cnf(c47409,plain,
( product(e_3,e_1,e_4)
| product(e_3,e_5,e_2) ),
inference(resolution,[status(thm)],[c45980,e_1_is_not_e_4]) ).
cnf(c47456,plain,
( product(e_3,e_1,e_4)
| equalish(e_5,e_1) ),
inference(resolution,[status(thm)],[c47409,c45986]) ).
cnf(c47483,plain,
product(e_3,e_1,e_4),
inference(resolution,[status(thm)],[c47456,e_5_is_not_e_1]) ).
cnf(c47486,plain,
( product(e_5,e_1,e_2)
| equalish(e_3,e_5) ),
inference(resolution,[status(thm)],[c47483,c41043]) ).
cnf(c47555,plain,
product(e_5,e_1,e_2),
inference(resolution,[status(thm)],[c47486,e_3_is_not_e_5]) ).
cnf(c47563,plain,
( product(e_5,e_4,e_1)
| product(e_5,e_4,e_3)
| equalish(e_1,e_4) ),
inference(resolution,[status(thm)],[c47555,c12218]) ).
cnf(c48805,plain,
( product(e_5,e_4,e_1)
| product(e_5,e_4,e_3) ),
inference(resolution,[status(thm)],[c47563,e_1_is_not_e_4]) ).
cnf(c48806,plain,
( product(e_5,e_4,e_3)
| ~ product(X2826,e_4,e_1)
| equalish(X2826,e_5) ),
inference(resolution,[status(thm)],[c48805,product_left_cancellation]) ).
cnf(c47495,plain,
( ~ product(e_3,X2738,e_4)
| equalish(X2738,e_1) ),
inference(resolution,[status(thm)],[c47483,product_right_cancellation]) ).
cnf(c554,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)
| product(e_2,e_4,e_5) ),
inference(resolution,[status(thm)],[c42,element_2]) ).
cnf(c2229,plain,
( product(e_2,e_4,e_1)
| product(e_2,e_4,e_3)
| product(e_2,e_4,e_4)
| product(e_2,e_4,e_5)
| equalish(e_4,e_2) ),
inference(resolution,[status(thm)],[c554,c38]) ).
cnf(c9328,plain,
( product(e_2,e_4,e_1)
| product(e_2,e_4,e_3)
| product(e_2,e_4,e_4)
| product(e_2,e_4,e_5) ),
inference(resolution,[status(thm)],[c2229,e_4_is_not_e_2]) ).
cnf(c11056,plain,
( product(e_2,e_4,e_1)
| product(e_2,e_4,e_3)
| product(e_2,e_4,e_5)
| equalish(e_2,e_4) ),
inference(resolution,[status(thm)],[c9328,c47]) ).
cnf(c11122,plain,
( product(e_2,e_4,e_1)
| product(e_2,e_4,e_3)
| product(e_2,e_4,e_5) ),
inference(resolution,[status(thm)],[c11056,e_2_is_not_e_4]) ).
cnf(c11151,plain,
( product(e_2,e_4,e_1)
| product(e_2,e_4,e_5)
| ~ product(e_2,X1230,e_3)
| equalish(X1230,e_4) ),
inference(resolution,[status(thm)],[c11122,product_right_cancellation]) ).
cnf(c40791,plain,
( product(e_2,e_4,e_1)
| product(e_2,e_4,e_5)
| equalish(e_1,e_4) ),
inference(resolution,[status(thm)],[c40776,c11151]) ).
cnf(c41582,plain,
( product(e_2,e_4,e_1)
| product(e_2,e_4,e_5) ),
inference(resolution,[status(thm)],[c40791,e_1_is_not_e_4]) ).
cnf(c41605,plain,
( product(e_2,e_4,e_1)
| ~ product(e_4,e_2,X2503)
| product(X2503,e_5,e_4) ),
inference(resolution,[status(thm)],[c41582,qg3]) ).
cnf(c40784,plain,
( ~ product(e_1,e_2,X2438)
| product(X2438,e_3,e_1) ),
inference(resolution,[status(thm)],[c40776,qg3]) ).
cnf(c42338,plain,
( product(e_1,e_2,e_5)
| product(e_4,e_3,e_1) ),
inference(resolution,[status(thm)],[c42334,c40784]) ).
cnf(c42384,plain,
( product(e_1,e_2,e_5)
| ~ product(e_4,X2519,e_1)
| equalish(X2519,e_3) ),
inference(resolution,[status(thm)],[c42338,product_right_cancellation]) ).
cnf(c542,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)
| product(e_4,e_2,e_5) ),
inference(resolution,[status(thm)],[c41,element_4]) ).
cnf(c2041,plain,
( product(e_4,e_2,e_1)
| product(e_4,e_2,e_3)
| product(e_4,e_2,e_4)
| product(e_4,e_2,e_5)
| equalish(e_4,e_2) ),
inference(resolution,[status(thm)],[c542,c47]) ).
cnf(c7273,plain,
( product(e_4,e_2,e_1)
| product(e_4,e_2,e_3)
| product(e_4,e_2,e_4)
| product(e_4,e_2,e_5) ),
inference(resolution,[status(thm)],[c2041,e_4_is_not_e_2]) ).
cnf(c9826,plain,
( product(e_4,e_2,e_1)
| product(e_4,e_2,e_3)
| product(e_4,e_2,e_5)
| equalish(e_2,e_4) ),
inference(resolution,[status(thm)],[c7273,c38]) ).
cnf(c9920,plain,
( product(e_4,e_2,e_1)
| product(e_4,e_2,e_3)
| product(e_4,e_2,e_5) ),
inference(resolution,[status(thm)],[c9826,e_2_is_not_e_4]) ).
cnf(c9973,plain,
( product(e_4,e_2,e_1)
| product(e_4,e_2,e_3)
| ~ product(e_4,X1138,e_5)
| equalish(X1138,e_2) ),
inference(resolution,[status(thm)],[c9920,product_right_cancellation]) ).
cnf(c45448,plain,
( product(e_4,e_2,e_1)
| product(e_4,e_2,e_3)
| equalish(e_1,e_2) ),
inference(resolution,[status(thm)],[c45439,c9973]) ).
cnf(c45852,plain,
( product(e_4,e_2,e_1)
| product(e_4,e_2,e_3) ),
inference(resolution,[status(thm)],[c45448,e_1_is_not_e_2]) ).
cnf(c45861,plain,
( product(e_4,e_2,e_3)
| product(e_1,e_2,e_5)
| equalish(e_2,e_3) ),
inference(resolution,[status(thm)],[c45852,c42384]) ).
cnf(c46788,plain,
( product(e_4,e_2,e_3)
| product(e_1,e_2,e_5) ),
inference(resolution,[status(thm)],[c45861,e_2_is_not_e_3]) ).
cnf(c46805,plain,
( product(e_4,e_2,e_3)
| ~ product(X2713,e_2,e_5)
| equalish(X2713,e_1) ),
inference(resolution,[status(thm)],[c46788,product_left_cancellation]) ).
cnf(c45853,plain,
( product(e_4,e_2,e_3)
| ~ product(X2666,e_2,e_1)
| equalish(X2666,e_4) ),
inference(resolution,[status(thm)],[c45852,product_left_cancellation]) ).
cnf(c543,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)
| product(e_3,e_2,e_5) ),
inference(resolution,[status(thm)],[c41,element_3]) ).
cnf(c2149,plain,
( product(e_3,e_2,e_1)
| product(e_3,e_2,e_3)
| product(e_3,e_2,e_4)
| product(e_3,e_2,e_5)
| equalish(e_3,e_2) ),
inference(resolution,[status(thm)],[c543,c47]) ).
cnf(c7731,plain,
( product(e_3,e_2,e_1)
| product(e_3,e_2,e_3)
| product(e_3,e_2,e_4)
| product(e_3,e_2,e_5) ),
inference(resolution,[status(thm)],[c2149,e_3_is_not_e_2]) ).
cnf(c10174,plain,
( product(e_3,e_2,e_1)
| product(e_3,e_2,e_4)
| product(e_3,e_2,e_5)
| equalish(e_2,e_3) ),
inference(resolution,[status(thm)],[c7731,c38]) ).
cnf(c10248,plain,
( product(e_3,e_2,e_1)
| product(e_3,e_2,e_4)
| product(e_3,e_2,e_5) ),
inference(resolution,[status(thm)],[c10174,e_2_is_not_e_3]) ).
cnf(c10270,plain,
( product(e_3,e_2,e_1)
| product(e_3,e_2,e_5)
| ~ product(e_3,X1159,e_4)
| equalish(X1159,e_2) ),
inference(resolution,[status(thm)],[c10248,product_right_cancellation]) ).
cnf(c47491,plain,
( product(e_3,e_2,e_1)
| product(e_3,e_2,e_5)
| equalish(e_1,e_2) ),
inference(resolution,[status(thm)],[c47483,c10270]) ).
cnf(c48547,plain,
( product(e_3,e_2,e_1)
| product(e_3,e_2,e_5) ),
inference(resolution,[status(thm)],[c47491,e_1_is_not_e_2]) ).
cnf(c48551,plain,
( product(e_3,e_2,e_5)
| product(e_4,e_2,e_3)
| equalish(e_3,e_4) ),
inference(resolution,[status(thm)],[c48547,c45853]) ).
cnf(c49527,plain,
( product(e_3,e_2,e_5)
| product(e_4,e_2,e_3) ),
inference(resolution,[status(thm)],[c48551,e_3_is_not_e_4]) ).
cnf(c49539,plain,
( product(e_4,e_2,e_3)
| equalish(e_3,e_1) ),
inference(resolution,[status(thm)],[c49527,c46805]) ).
cnf(c49595,plain,
product(e_4,e_2,e_3),
inference(resolution,[status(thm)],[c49539,e_3_is_not_e_1]) ).
cnf(c49618,plain,
( product(e_2,e_4,e_1)
| product(e_3,e_5,e_4) ),
inference(resolution,[status(thm)],[c49595,c41605]) ).
cnf(c49748,plain,
( product(e_2,e_4,e_1)
| equalish(e_5,e_1) ),
inference(resolution,[status(thm)],[c49618,c47495]) ).
cnf(c49768,plain,
product(e_2,e_4,e_1),
inference(resolution,[status(thm)],[c49748,e_5_is_not_e_1]) ).
cnf(c49778,plain,
( product(e_5,e_4,e_3)
| equalish(e_2,e_5) ),
inference(resolution,[status(thm)],[c49768,c48806]) ).
cnf(c49833,plain,
product(e_5,e_4,e_3),
inference(resolution,[status(thm)],[c49778,e_2_is_not_e_5]) ).
cnf(c49834,plain,
( ~ product(X2883,e_4,e_3)
| equalish(X2883,e_5) ),
inference(resolution,[status(thm)],[c49833,product_left_cancellation]) ).
cnf(c42702,plain,
( product(e_3,e_4,e_2)
| product(e_5,e_3,e_1) ),
inference(resolution,[status(thm)],[c42699,c40784]) ).
cnf(c42749,plain,
( product(e_3,e_4,e_2)
| ~ product(X2543,e_3,e_1)
| equalish(X2543,e_5) ),
inference(resolution,[status(thm)],[c42702,product_left_cancellation]) ).
cnf(c566,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)
| product(e_4,e_3,e_5) ),
inference(resolution,[status(thm)],[c43,element_4]) ).
cnf(c2357,plain,
( product(e_4,e_3,e_1)
| product(e_4,e_3,e_2)
| product(e_4,e_3,e_4)
| product(e_4,e_3,e_5)
| equalish(e_4,e_3) ),
inference(resolution,[status(thm)],[c566,c47]) ).
cnf(c13503,plain,
( product(e_4,e_3,e_1)
| product(e_4,e_3,e_2)
| product(e_4,e_3,e_4)
| product(e_4,e_3,e_5) ),
inference(resolution,[status(thm)],[c2357,e_4_is_not_e_3]) ).
cnf(c18742,plain,
( product(e_4,e_3,e_1)
| product(e_4,e_3,e_2)
| product(e_4,e_3,e_5)
| equalish(e_3,e_4) ),
inference(resolution,[status(thm)],[c13503,c38]) ).
cnf(c18872,plain,
( product(e_4,e_3,e_1)
| product(e_4,e_3,e_2)
| product(e_4,e_3,e_5) ),
inference(resolution,[status(thm)],[c18742,e_3_is_not_e_4]) ).
cnf(c18939,plain,
( product(e_4,e_3,e_1)
| product(e_4,e_3,e_2)
| ~ product(e_4,X1654,e_5)
| equalish(X1654,e_3) ),
inference(resolution,[status(thm)],[c18872,product_right_cancellation]) ).
cnf(c45441,plain,
( product(e_4,e_3,e_1)
| product(e_4,e_3,e_2)
| equalish(e_1,e_3) ),
inference(resolution,[status(thm)],[c45439,c18939]) ).
cnf(c45699,plain,
( product(e_4,e_3,e_1)
| product(e_4,e_3,e_2) ),
inference(resolution,[status(thm)],[c45441,e_1_is_not_e_3]) ).
cnf(c45706,plain,
( product(e_4,e_3,e_2)
| product(e_3,e_4,e_2)
| equalish(e_4,e_5) ),
inference(resolution,[status(thm)],[c45699,c42749]) ).
cnf(c46464,plain,
( product(e_4,e_3,e_2)
| product(e_3,e_4,e_2) ),
inference(resolution,[status(thm)],[c45706,e_4_is_not_e_5]) ).
cnf(c46508,plain,
( product(e_4,e_3,e_2)
| ~ product(e_3,X2697,e_2)
| equalish(X2697,e_4) ),
inference(resolution,[status(thm)],[c46464,product_right_cancellation]) ).
cnf(c44,plain,
( ~ group_element(X199)
| product(X199,e_5,e_1)
| product(X199,e_5,e_2)
| product(X199,e_5,e_3)
| product(X199,e_5,e_4)
| product(X199,e_5,e_5) ),
inference(resolution,[status(thm)],[product_total_function1,element_5]) ).
cnf(c575,plain,
( product(e_3,e_5,e_1)
| product(e_3,e_5,e_2)
| product(e_3,e_5,e_3)
| product(e_3,e_5,e_4)
| product(e_3,e_5,e_5) ),
inference(resolution,[status(thm)],[c44,element_3]) ).
cnf(c2469,plain,
( product(e_3,e_5,e_1)
| product(e_3,e_5,e_2)
| product(e_3,e_5,e_4)
| product(e_3,e_5,e_5)
| equalish(e_5,e_3) ),
inference(resolution,[status(thm)],[c575,c38]) ).
cnf(c17536,plain,
( product(e_3,e_5,e_1)
| product(e_3,e_5,e_2)
| product(e_3,e_5,e_4)
| product(e_3,e_5,e_5) ),
inference(resolution,[status(thm)],[c2469,e_5_is_not_e_3]) ).
cnf(c20516,plain,
( product(e_3,e_5,e_1)
| product(e_3,e_5,e_2)
| product(e_3,e_5,e_4)
| equalish(e_3,e_5) ),
inference(resolution,[status(thm)],[c17536,c47]) ).
cnf(c20572,plain,
( product(e_3,e_5,e_1)
| product(e_3,e_5,e_2)
| product(e_3,e_5,e_4) ),
inference(resolution,[status(thm)],[c20516,e_3_is_not_e_5]) ).
cnf(c20614,plain,
( product(e_3,e_5,e_1)
| product(e_3,e_5,e_2)
| ~ product(e_3,X1770,e_4)
| equalish(X1770,e_5) ),
inference(resolution,[status(thm)],[c20572,product_right_cancellation]) ).
cnf(c47425,plain,
( product(e_3,e_5,e_2)
| product(e_3,e_5,e_1)
| equalish(e_1,e_5) ),
inference(resolution,[status(thm)],[c47409,c20614]) ).
cnf(c48399,plain,
( product(e_3,e_5,e_2)
| product(e_3,e_5,e_1) ),
inference(resolution,[status(thm)],[c47425,e_1_is_not_e_5]) ).
cnf(c48411,plain,
( product(e_3,e_5,e_1)
| product(e_4,e_3,e_2)
| equalish(e_5,e_4) ),
inference(resolution,[status(thm)],[c48399,c46508]) ).
cnf(c48925,plain,
( product(e_3,e_5,e_1)
| product(e_4,e_3,e_2) ),
inference(resolution,[status(thm)],[c48411,e_5_is_not_e_4]) ).
cnf(c48952,plain,
( product(e_3,e_5,e_1)
| ~ product(X2838,e_3,e_2)
| equalish(X2838,e_4) ),
inference(resolution,[status(thm)],[c48925,product_left_cancellation]) ).
cnf(c49612,plain,
( ~ product(e_2,e_4,X2869)
| product(X2869,e_3,e_2) ),
inference(resolution,[status(thm)],[c49595,qg3]) ).
cnf(c49769,plain,
product(e_1,e_3,e_2),
inference(resolution,[status(thm)],[c49768,c49612]) ).
cnf(c49787,plain,
( product(e_3,e_5,e_1)
| equalish(e_1,e_4) ),
inference(resolution,[status(thm)],[c49769,c48952]) ).
cnf(c50029,plain,
product(e_3,e_5,e_1),
inference(resolution,[status(thm)],[c49787,e_1_is_not_e_4]) ).
cnf(c568,plain,
( product(e_5,e_3,e_1)
| product(e_5,e_3,e_2)
| product(e_5,e_3,e_3)
| product(e_5,e_3,e_4)
| product(e_5,e_3,e_5) ),
inference(resolution,[status(thm)],[c43,element_5]) ).
cnf(c2379,plain,
( product(e_5,e_3,e_1)
| product(e_5,e_3,e_2)
| product(e_5,e_3,e_4)
| product(e_5,e_3,e_5)
| equalish(e_5,e_3) ),
inference(resolution,[status(thm)],[c568,c47]) ).
cnf(c14685,plain,
( product(e_5,e_3,e_1)
| product(e_5,e_3,e_2)
| product(e_5,e_3,e_4)
| product(e_5,e_3,e_5) ),
inference(resolution,[status(thm)],[c2379,e_5_is_not_e_3]) ).
cnf(c19110,plain,
( product(e_5,e_3,e_1)
| product(e_5,e_3,e_2)
| product(e_5,e_3,e_4)
| equalish(e_3,e_5) ),
inference(resolution,[status(thm)],[c14685,c38]) ).
cnf(c19198,plain,
( product(e_5,e_3,e_1)
| product(e_5,e_3,e_2)
| product(e_5,e_3,e_4) ),
inference(resolution,[status(thm)],[c19110,e_3_is_not_e_5]) ).
cnf(c19233,plain,
( product(e_5,e_3,e_1)
| product(e_5,e_3,e_4)
| ~ product(e_5,X1677,e_2)
| equalish(X1677,e_3) ),
inference(resolution,[status(thm)],[c19198,product_right_cancellation]) ).
cnf(c47560,plain,
( product(e_5,e_3,e_1)
| product(e_5,e_3,e_4)
| equalish(e_1,e_3) ),
inference(resolution,[status(thm)],[c47555,c19233]) ).
cnf(c48665,plain,
( product(e_5,e_3,e_1)
| product(e_5,e_3,e_4) ),
inference(resolution,[status(thm)],[c47560,e_1_is_not_e_3]) ).
cnf(c48666,plain,
( product(e_5,e_3,e_4)
| ~ product(X2820,e_3,e_1)
| equalish(X2820,e_5) ),
inference(resolution,[status(thm)],[c48665,product_left_cancellation]) ).
cnf(c45733,plain,
( product(e_4,e_3,e_1)
| ~ product(X2663,e_3,e_2)
| equalish(X2663,e_4) ),
inference(resolution,[status(thm)],[c45699,product_left_cancellation]) ).
cnf(c49783,plain,
( product(e_4,e_3,e_1)
| equalish(e_1,e_4) ),
inference(resolution,[status(thm)],[c49769,c45733]) ).
cnf(c49890,plain,
product(e_4,e_3,e_1),
inference(resolution,[status(thm)],[c49783,e_1_is_not_e_4]) ).
cnf(c49901,plain,
( product(e_5,e_3,e_4)
| equalish(e_4,e_5) ),
inference(resolution,[status(thm)],[c49890,c48666]) ).
cnf(c50128,plain,
product(e_5,e_3,e_4),
inference(resolution,[status(thm)],[c49901,e_4_is_not_e_5]) ).
cnf(c50135,plain,
( ~ product(e_3,e_5,X2912)
| product(X2912,e_4,e_3) ),
inference(resolution,[status(thm)],[c50128,qg3]) ).
cnf(c50177,plain,
product(e_1,e_4,e_3),
inference(resolution,[status(thm)],[c50135,c50029]) ).
cnf(c50187,plain,
equalish(e_1,e_5),
inference(resolution,[status(thm)],[c50177,c49834]) ).
cnf(c50188,plain,
$false,
inference(resolution,[status(thm)],[c50187,e_1_is_not_e_5]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : GRP125-3.005 : TPTP v8.1.2. Released v1.2.0.
% 0.07/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.35 % Computer : n011.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 300
% 0.13/0.35 % DateTime : Thu May 9 03:56:53 EDT 2024
% 0.13/0.35 % CPUTime :
% 116.48/116.71 % Version: 1.5
% 116.48/116.71 % SZS status Unsatisfiable
% 116.48/116.71 % SZS output start CNFRefutation
% See solution above
% 116.48/116.72
% 116.48/116.72 % Initial clauses : 58
% 116.48/116.72 % Processed clauses : 3475
% 116.48/116.72 % Factors computed : 8
% 116.48/116.72 % Resolvents computed: 50181
% 116.48/116.72 % Tautologies deleted: 122
% 116.48/116.72 % Forward subsumed : 11069
% 116.48/116.72 % Backward subsumed : 3063
% 116.48/116.72 % -------- CPU Time ---------
% 116.48/116.72 % User time : 116.154 s
% 116.48/116.72 % System time : 0.195 s
% 116.48/116.72 % Total time : 116.349 s
%------------------------------------------------------------------------------