%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GRP130-3.003 : 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:13 EDT 2024
% Result : Unsatisfiable 22.07s 22.32s
% Output : Refutation 22.15s
% Verified :
% SZS Type : Refutation
% Derivation depth : 54
% Number of leaves : 27
% Syntax : Number of clauses : 167 ( 25 unt; 112 nHn; 167 RR)
% Number of literals : 469 ( 0 equ; 136 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 : 4 ( 4 usr; 4 con; 0-0 aty)
% Number of variables : 90 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(e_1_is_not_e_3,axiom,
~ equalish(e_1,e_3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_1_is_not_e_3) ).
cnf(product_total_function2,axiom,
( ~ product(X11,X12,X10)
| ~ product(X11,X12,X9)
| equalish(X10,X9) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',product_total_function2) ).
cnf(e_2_is_not_e_3,axiom,
~ equalish(e_2,e_3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_2_is_not_e_3) ).
cnf(product_left_cancellation,axiom,
( ~ product(X29,X31,X30)
| ~ product(X28,X31,X30)
| equalish(X29,X28) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',product_left_cancellation) ).
cnf(qg3,negated_conjecture,
( ~ product(X38,X39,X37)
| ~ product(X38,X37,X40)
| product(X40,X39,X38) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',qg3) ).
cnf(c14,plain,
( ~ product(X41,X42,X42)
| product(X42,X42,X41) ),
inference(factor,[status(thm)],[qg3]) ).
cnf(element_3,axiom,
group_element(e_3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',element_3) ).
cnf(element_1,axiom,
group_element(e_1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',element_1) ).
cnf(product_total_function1,axiom,
( ~ group_element(X52)
| ~ group_element(X53)
| product(X52,X53,e_1)
| product(X52,X53,e_2)
| product(X52,X53,e_3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',product_total_function1) ).
cnf(c52,plain,
( ~ group_element(X134)
| product(X134,e_1,e_1)
| product(X134,e_1,e_2)
| product(X134,e_1,e_3) ),
inference(resolution,[status(thm)],[product_total_function1,element_1]) ).
cnf(c255,plain,
( product(e_3,e_1,e_1)
| product(e_3,e_1,e_2)
| product(e_3,e_1,e_3) ),
inference(resolution,[status(thm)],[c52,element_3]) ).
cnf(c718,plain,
( product(e_3,e_1,e_2)
| product(e_3,e_1,e_3)
| product(e_1,e_1,e_3) ),
inference(resolution,[status(thm)],[c255,c14]) ).
cnf(c890,plain,
( product(e_3,e_1,e_3)
| product(e_1,e_1,e_3)
| ~ product(X511,e_1,e_2)
| equalish(X511,e_3) ),
inference(resolution,[status(thm)],[c718,product_left_cancellation]) ).
cnf(e_1_is_not_e_2,axiom,
~ equalish(e_1,e_2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_1_is_not_e_2) ).
cnf(e_2_is_not_e_1,axiom,
~ equalish(e_2,e_1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_2_is_not_e_1) ).
cnf(product_right_cancellation,axiom,
( ~ product(X18,X17,X19)
| ~ product(X18,X16,X19)
| equalish(X17,X16) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',product_right_cancellation) ).
cnf(e_3_is_not_e_1,axiom,
~ equalish(e_3,e_1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_3_is_not_e_1) ).
cnf(cycle2,axiom,
( ~ group_element(X8)
| cycle(X8,e_0)
| cycle(X8,e_1)
| cycle(X8,e_2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cycle2) ).
cnf(c5,plain,
( cycle(e_1,e_0)
| cycle(e_1,e_1)
| cycle(e_1,e_2) ),
inference(resolution,[status(thm)],[cycle2,element_1]) ).
cnf(e_1_then_e_2,axiom,
next(e_1,e_2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_1_then_e_2) ).
cnf(e_1_greater_e_0,axiom,
greater(e_1,e_0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_1_greater_e_0) ).
cnf(cycle4,axiom,
( ~ cycle(X27,X23)
| ~ cycle(X26,X25)
| ~ next(X27,X26)
| ~ greater(X23,e_0)
| ~ next(X25,X24)
| equalish(X23,X24) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cycle4) ).
cnf(c9,plain,
( ~ cycle(X54,X55)
| ~ cycle(X56,X54)
| ~ next(X54,X56)
| ~ greater(X55,e_0)
| equalish(X55,X56) ),
inference(factor,[status(thm)],[cycle4]) ).
cnf(c59,plain,
( ~ cycle(X62,e_1)
| ~ cycle(X63,X62)
| ~ next(X62,X63)
| equalish(e_1,X63) ),
inference(resolution,[status(thm)],[c9,e_1_greater_e_0]) ).
cnf(c68,plain,
( ~ cycle(e_1,e_1)
| ~ cycle(e_2,e_1)
| equalish(e_1,e_2) ),
inference(resolution,[status(thm)],[c59,e_1_then_e_2]) ).
cnf(element_2,axiom,
group_element(e_2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',element_2) ).
cnf(c6,plain,
( cycle(e_2,e_0)
| cycle(e_2,e_1)
| cycle(e_2,e_2) ),
inference(resolution,[status(thm)],[cycle2,element_2]) ).
cnf(cycle3,axiom,
cycle(e_3,e_0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cycle3) ).
cnf(e_2_then_e_3,axiom,
next(e_2,e_3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_2_then_e_3) ).
cnf(e_2_greater_e_0,axiom,
greater(e_2,e_0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_2_greater_e_0) ).
cnf(e_0_then_e_1,axiom,
next(e_0,e_1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_0_then_e_1) ).
cnf(c10,plain,
( ~ cycle(X61,X60)
| ~ cycle(X59,e_0)
| ~ next(X61,X59)
| ~ greater(X60,e_0)
| equalish(X60,e_1) ),
inference(resolution,[status(thm)],[cycle4,e_0_then_e_1]) ).
cnf(c64,plain,
( ~ cycle(X73,e_2)
| ~ cycle(X72,e_0)
| ~ next(X73,X72)
| equalish(e_2,e_1) ),
inference(resolution,[status(thm)],[c10,e_2_greater_e_0]) ).
cnf(c93,plain,
( ~ cycle(e_2,e_2)
| ~ cycle(e_3,e_0)
| equalish(e_2,e_1) ),
inference(resolution,[status(thm)],[c64,e_2_then_e_3]) ).
cnf(c98,plain,
( ~ cycle(e_2,e_2)
| equalish(e_2,e_1) ),
inference(resolution,[status(thm)],[c93,cycle3]) ).
cnf(c105,plain,
( equalish(e_2,e_1)
| cycle(e_2,e_0)
| cycle(e_2,e_1) ),
inference(resolution,[status(thm)],[c98,c6]) ).
cnf(c107,plain,
( cycle(e_2,e_0)
| cycle(e_2,e_1) ),
inference(resolution,[status(thm)],[c105,e_2_is_not_e_1]) ).
cnf(e_2_greater_e_1,axiom,
greater(e_2,e_1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_2_greater_e_1) ).
cnf(cycle5,axiom,
( ~ cycle(X46,X44)
| ~ cycle(X43,e_0)
| ~ cycle(X45,X47)
| ~ next(X43,X45)
| ~ greater(X43,X46)
| ~ greater(X44,X47) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cycle5) ).
cnf(c16,plain,
( ~ cycle(X78,e_2)
| ~ cycle(X77,e_0)
| ~ cycle(X79,e_0)
| ~ next(X77,X79)
| ~ greater(X77,X78) ),
inference(resolution,[status(thm)],[cycle5,e_2_greater_e_0]) ).
cnf(c126,plain,
( ~ cycle(e_1,e_2)
| ~ cycle(e_2,e_0)
| ~ cycle(X144,e_0)
| ~ next(e_2,X144) ),
inference(resolution,[status(thm)],[c16,e_2_greater_e_1]) ).
cnf(c268,plain,
( ~ cycle(e_1,e_2)
| ~ cycle(e_2,e_0)
| ~ cycle(e_3,e_0) ),
inference(resolution,[status(thm)],[c126,e_2_then_e_3]) ).
cnf(c269,plain,
( ~ cycle(e_1,e_2)
| ~ cycle(e_2,e_0) ),
inference(resolution,[status(thm)],[c268,cycle3]) ).
cnf(c270,plain,
( ~ cycle(e_1,e_2)
| cycle(e_2,e_1) ),
inference(resolution,[status(thm)],[c269,c107]) ).
cnf(c272,plain,
( cycle(e_2,e_1)
| cycle(e_1,e_0)
| cycle(e_1,e_1) ),
inference(resolution,[status(thm)],[c270,c5]) ).
cnf(c19,plain,
( ~ cycle(X90,e_1)
| ~ cycle(X89,e_0)
| ~ cycle(X91,e_0)
| ~ next(X89,X91)
| ~ greater(X89,X90) ),
inference(resolution,[status(thm)],[cycle5,e_1_greater_e_0]) ).
cnf(c159,plain,
( ~ cycle(e_1,e_1)
| ~ cycle(e_2,e_0)
| ~ cycle(X162,e_0)
| ~ next(e_2,X162) ),
inference(resolution,[status(thm)],[c19,e_2_greater_e_1]) ).
cnf(c318,plain,
( ~ cycle(e_1,e_1)
| ~ cycle(e_2,e_0)
| ~ cycle(e_3,e_0) ),
inference(resolution,[status(thm)],[c159,e_2_then_e_3]) ).
cnf(c319,plain,
( ~ cycle(e_1,e_1)
| ~ cycle(e_2,e_0) ),
inference(resolution,[status(thm)],[c318,cycle3]) ).
cnf(c320,plain,
( ~ cycle(e_1,e_1)
| cycle(e_2,e_1) ),
inference(resolution,[status(thm)],[c319,c107]) ).
cnf(c322,plain,
( cycle(e_2,e_1)
| cycle(e_1,e_0) ),
inference(resolution,[status(thm)],[c320,c272]) ).
cnf(c326,plain,
( cycle(e_1,e_0)
| ~ cycle(e_1,e_1)
| equalish(e_1,e_2) ),
inference(resolution,[status(thm)],[c322,c68]) ).
cnf(c356,plain,
( cycle(e_1,e_0)
| equalish(e_1,e_2)
| cycle(e_1,e_2) ),
inference(resolution,[status(thm)],[c326,c5]) ).
cnf(c398,plain,
( cycle(e_1,e_0)
| cycle(e_1,e_2) ),
inference(resolution,[status(thm)],[c356,e_1_is_not_e_2]) ).
cnf(e_3_greater_e_1,axiom,
greater(e_3,e_1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_3_greater_e_1) ).
cnf(cycle6,axiom,
( ~ cycle(X35,e_0)
| ~ product(X35,e_1,X36)
| ~ greater(X36,X35) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cycle6) ).
cnf(c911,plain,
( product(e_3,e_1,e_2)
| product(e_3,e_1,e_3)
| ~ cycle(e_1,e_0)
| ~ greater(e_3,e_1) ),
inference(resolution,[status(thm)],[c718,cycle6]) ).
cnf(c3167,plain,
( product(e_3,e_1,e_2)
| product(e_3,e_1,e_3)
| ~ cycle(e_1,e_0) ),
inference(resolution,[status(thm)],[c911,e_3_greater_e_1]) ).
cnf(c3168,plain,
( product(e_3,e_1,e_2)
| product(e_3,e_1,e_3)
| cycle(e_1,e_2) ),
inference(resolution,[status(thm)],[c3167,c398]) ).
cnf(c3214,plain,
( product(e_3,e_1,e_2)
| cycle(e_1,e_2)
| ~ product(e_3,X526,e_3)
| equalish(X526,e_1) ),
inference(resolution,[status(thm)],[c3168,product_right_cancellation]) ).
cnf(c3203,plain,
( product(e_3,e_1,e_2)
| cycle(e_1,e_2)
| ~ product(e_3,X638,e_1)
| product(e_3,X638,e_3) ),
inference(resolution,[status(thm)],[c3168,qg3]) ).
cnf(c50,plain,
( ~ group_element(X121)
| product(X121,X121,e_1)
| product(X121,X121,e_2)
| product(X121,X121,e_3) ),
inference(factor,[status(thm)],[product_total_function1]) ).
cnf(c234,plain,
( product(e_1,e_1,e_1)
| product(e_1,e_1,e_2)
| product(e_1,e_1,e_3) ),
inference(resolution,[status(thm)],[c50,element_1]) ).
cnf(c520,plain,
( product(e_1,e_1,e_1)
| product(e_1,e_1,e_2)
| ~ cycle(e_1,e_0)
| ~ greater(e_3,e_1) ),
inference(resolution,[status(thm)],[c234,cycle6]) ).
cnf(c1156,plain,
( product(e_1,e_1,e_1)
| product(e_1,e_1,e_2)
| ~ cycle(e_1,e_0) ),
inference(resolution,[status(thm)],[c520,e_3_greater_e_1]) ).
cnf(c1157,plain,
( product(e_1,e_1,e_1)
| product(e_1,e_1,e_2)
| cycle(e_1,e_2) ),
inference(resolution,[status(thm)],[c1156,c398]) ).
cnf(c511,plain,
( product(e_1,e_1,e_1)
| product(e_1,e_1,e_3)
| ~ cycle(e_1,e_0)
| ~ greater(e_2,e_1) ),
inference(resolution,[status(thm)],[c234,cycle6]) ).
cnf(c1034,plain,
( product(e_1,e_1,e_1)
| product(e_1,e_1,e_3)
| ~ cycle(e_1,e_0) ),
inference(resolution,[status(thm)],[c511,e_2_greater_e_1]) ).
cnf(c1036,plain,
( product(e_1,e_1,e_1)
| product(e_1,e_1,e_3)
| cycle(e_1,e_2) ),
inference(resolution,[status(thm)],[c1034,c398]) ).
cnf(c1055,plain,
( product(e_1,e_1,e_1)
| cycle(e_1,e_2)
| ~ product(e_1,e_1,X289)
| equalish(X289,e_3) ),
inference(resolution,[status(thm)],[c1036,product_total_function2]) ).
cnf(c1283,plain,
( product(e_1,e_1,e_1)
| cycle(e_1,e_2)
| equalish(e_2,e_3) ),
inference(resolution,[status(thm)],[c1055,c1157]) ).
cnf(c1325,plain,
( product(e_1,e_1,e_1)
| cycle(e_1,e_2) ),
inference(resolution,[status(thm)],[c1283,e_2_is_not_e_3]) ).
cnf(c1326,plain,
( cycle(e_1,e_2)
| ~ product(e_1,X293,e_1)
| equalish(X293,e_1) ),
inference(resolution,[status(thm)],[c1325,product_right_cancellation]) ).
cnf(c51,plain,
( ~ group_element(X132)
| product(X132,e_3,e_1)
| product(X132,e_3,e_2)
| product(X132,e_3,e_3) ),
inference(resolution,[status(thm)],[product_total_function1,element_3]) ).
cnf(c249,plain,
( product(e_1,e_3,e_1)
| product(e_1,e_3,e_2)
| product(e_1,e_3,e_3) ),
inference(resolution,[status(thm)],[c51,element_1]) ).
cnf(c664,plain,
( product(e_1,e_3,e_1)
| product(e_1,e_3,e_2)
| product(e_3,e_3,e_1) ),
inference(resolution,[status(thm)],[c249,c14]) ).
cnf(c233,plain,
( product(e_3,e_3,e_1)
| product(e_3,e_3,e_2)
| product(e_3,e_3,e_3) ),
inference(resolution,[status(thm)],[c50,element_3]) ).
cnf(c469,plain,
( product(e_3,e_3,e_1)
| product(e_3,e_3,e_3)
| ~ product(X215,e_3,e_2)
| equalish(X215,e_3) ),
inference(resolution,[status(thm)],[c233,product_left_cancellation]) ).
cnf(c878,plain,
( product(e_3,e_3,e_1)
| product(e_3,e_3,e_3)
| equalish(e_1,e_3)
| product(e_1,e_3,e_1) ),
inference(resolution,[status(thm)],[c469,c664]) ).
cnf(c3821,plain,
( product(e_3,e_3,e_1)
| product(e_3,e_3,e_3)
| product(e_1,e_3,e_1) ),
inference(resolution,[status(thm)],[c878,e_1_is_not_e_3]) ).
cnf(c3910,plain,
( product(e_3,e_3,e_1)
| product(e_3,e_3,e_3)
| cycle(e_1,e_2)
| equalish(e_3,e_1) ),
inference(resolution,[status(thm)],[c3821,c1326]) ).
cnf(c10456,plain,
( product(e_3,e_3,e_1)
| product(e_3,e_3,e_3)
| cycle(e_1,e_2) ),
inference(resolution,[status(thm)],[c3910,e_3_is_not_e_1]) ).
cnf(c10484,plain,
( product(e_3,e_3,e_3)
| cycle(e_1,e_2)
| product(e_3,e_1,e_2) ),
inference(resolution,[status(thm)],[c10456,c3203]) ).
cnf(c10686,plain,
( cycle(e_1,e_2)
| product(e_3,e_1,e_2)
| equalish(e_3,e_1) ),
inference(resolution,[status(thm)],[c10484,c3214]) ).
cnf(c10817,plain,
( cycle(e_1,e_2)
| product(e_3,e_1,e_2) ),
inference(resolution,[status(thm)],[c10686,e_3_is_not_e_1]) ).
cnf(c10860,plain,
( cycle(e_1,e_2)
| ~ product(e_3,X659,e_2)
| equalish(X659,e_1) ),
inference(resolution,[status(thm)],[c10817,product_right_cancellation]) ).
cnf(e_3_is_not_e_2,axiom,
~ equalish(e_3,e_2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_3_is_not_e_2) ).
cnf(c257,plain,
( product(e_2,e_1,e_1)
| product(e_2,e_1,e_2)
| product(e_2,e_1,e_3) ),
inference(resolution,[status(thm)],[c52,element_2]) ).
cnf(c746,plain,
( product(e_2,e_1,e_2)
| product(e_2,e_1,e_3)
| product(e_1,e_1,e_2) ),
inference(resolution,[status(thm)],[c257,c14]) ).
cnf(c947,plain,
( product(e_2,e_1,e_2)
| product(e_2,e_1,e_3)
| ~ cycle(e_1,e_0)
| ~ greater(e_2,e_1) ),
inference(resolution,[status(thm)],[c746,cycle6]) ).
cnf(c4057,plain,
( product(e_2,e_1,e_2)
| product(e_2,e_1,e_3)
| ~ cycle(e_1,e_0) ),
inference(resolution,[status(thm)],[c947,e_2_greater_e_1]) ).
cnf(c4058,plain,
( product(e_2,e_1,e_2)
| product(e_2,e_1,e_3)
| cycle(e_1,e_2) ),
inference(resolution,[status(thm)],[c4057,c398]) ).
cnf(c4079,plain,
( product(e_2,e_1,e_3)
| cycle(e_1,e_2)
| ~ product(X539,e_1,e_2)
| equalish(X539,e_2) ),
inference(resolution,[status(thm)],[c4058,product_left_cancellation]) ).
cnf(c10859,plain,
( cycle(e_1,e_2)
| product(e_2,e_1,e_3)
| equalish(e_3,e_2) ),
inference(resolution,[status(thm)],[c10817,c4079]) ).
cnf(c11035,plain,
( cycle(e_1,e_2)
| product(e_2,e_1,e_3) ),
inference(resolution,[status(thm)],[c10859,e_3_is_not_e_2]) ).
cnf(c11059,plain,
( cycle(e_1,e_2)
| ~ product(e_2,X669,e_1)
| product(e_3,X669,e_2) ),
inference(resolution,[status(thm)],[c11035,qg3]) ).
cnf(c53,plain,
( ~ group_element(X138)
| product(X138,e_2,e_1)
| product(X138,e_2,e_2)
| product(X138,e_2,e_3) ),
inference(resolution,[status(thm)],[product_total_function1,element_2]) ).
cnf(c263,plain,
( product(e_1,e_2,e_1)
| product(e_1,e_2,e_2)
| product(e_1,e_2,e_3) ),
inference(resolution,[status(thm)],[c53,element_1]) ).
cnf(c1391,plain,
( cycle(e_1,e_2)
| equalish(e_2,e_1)
| product(e_1,e_2,e_2)
| product(e_1,e_2,e_3) ),
inference(resolution,[status(thm)],[c1326,c263]) ).
cnf(c5431,plain,
( cycle(e_1,e_2)
| product(e_1,e_2,e_2)
| product(e_1,e_2,e_3) ),
inference(resolution,[status(thm)],[c1391,e_2_is_not_e_1]) ).
cnf(c5513,plain,
( cycle(e_1,e_2)
| product(e_1,e_2,e_3)
| ~ product(e_1,X597,e_2)
| equalish(X597,e_2) ),
inference(resolution,[status(thm)],[c5431,product_right_cancellation]) ).
cnf(c1392,plain,
( cycle(e_1,e_2)
| equalish(e_3,e_1)
| product(e_1,e_3,e_2)
| product(e_1,e_3,e_3) ),
inference(resolution,[status(thm)],[c1326,c249]) ).
cnf(c6469,plain,
( cycle(e_1,e_2)
| product(e_1,e_3,e_2)
| product(e_1,e_3,e_3) ),
inference(resolution,[status(thm)],[c1392,e_3_is_not_e_1]) ).
cnf(c6722,plain,
( cycle(e_1,e_2)
| product(e_1,e_3,e_2)
| ~ product(X615,e_3,e_3)
| equalish(X615,e_1) ),
inference(resolution,[status(thm)],[c6469,product_left_cancellation]) ).
cnf(c6727,plain,
( cycle(e_1,e_2)
| product(e_1,e_3,e_2)
| product(e_3,e_3,e_1) ),
inference(resolution,[status(thm)],[c6469,c14]) ).
cnf(c10839,plain,
( cycle(e_1,e_2)
| ~ product(e_3,X662,e_1)
| product(e_2,X662,e_3) ),
inference(resolution,[status(thm)],[c10817,qg3]) ).
cnf(c10960,plain,
( cycle(e_1,e_2)
| product(e_2,e_3,e_3)
| product(e_1,e_3,e_2) ),
inference(resolution,[status(thm)],[c10839,c6727]) ).
cnf(c11183,plain,
( cycle(e_1,e_2)
| product(e_1,e_3,e_2)
| equalish(e_2,e_1) ),
inference(resolution,[status(thm)],[c10960,c6722]) ).
cnf(c11297,plain,
( cycle(e_1,e_2)
| product(e_1,e_3,e_2) ),
inference(resolution,[status(thm)],[c11183,e_2_is_not_e_1]) ).
cnf(c11316,plain,
( cycle(e_1,e_2)
| product(e_1,e_2,e_3)
| equalish(e_3,e_2) ),
inference(resolution,[status(thm)],[c11297,c5513]) ).
cnf(c11482,plain,
( cycle(e_1,e_2)
| product(e_1,e_2,e_3) ),
inference(resolution,[status(thm)],[c11316,e_3_is_not_e_2]) ).
cnf(c11319,plain,
( cycle(e_1,e_2)
| ~ product(e_1,X682,e_3)
| product(e_2,X682,e_1) ),
inference(resolution,[status(thm)],[c11297,qg3]) ).
cnf(c11767,plain,
( cycle(e_1,e_2)
| product(e_2,e_2,e_1) ),
inference(resolution,[status(thm)],[c11319,c11482]) ).
cnf(c11783,plain,
( cycle(e_1,e_2)
| product(e_3,e_2,e_2) ),
inference(resolution,[status(thm)],[c11767,c11059]) ).
cnf(c11973,plain,
( cycle(e_1,e_2)
| equalish(e_2,e_1) ),
inference(resolution,[status(thm)],[c11783,c10860]) ).
cnf(c11985,plain,
cycle(e_1,e_2),
inference(resolution,[status(thm)],[c11973,e_2_is_not_e_1]) ).
cnf(cycle7,axiom,
( ~ cycle(X49,X51)
| ~ product(X49,e_1,X48)
| ~ greater(X51,e_0)
| ~ next(X49,X50)
| equalish(X48,X50) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cycle7) ).
cnf(c499,plain,
( product(e_1,e_1,e_2)
| product(e_1,e_1,e_3)
| ~ cycle(e_1,X245)
| ~ greater(X245,e_0)
| ~ next(e_1,X244)
| equalish(e_1,X244) ),
inference(resolution,[status(thm)],[c234,cycle7]) ).
cnf(c1009,plain,
( product(e_1,e_1,e_2)
| product(e_1,e_1,e_3)
| ~ cycle(e_1,X609)
| ~ greater(X609,e_0)
| equalish(e_1,e_2) ),
inference(resolution,[status(thm)],[c499,e_1_then_e_2]) ).
cnf(c6731,plain,
( product(e_1,e_1,e_2)
| product(e_1,e_1,e_3)
| ~ cycle(e_1,e_2)
| equalish(e_1,e_2) ),
inference(resolution,[status(thm)],[c1009,e_2_greater_e_0]) ).
cnf(c15467,plain,
( product(e_1,e_1,e_2)
| product(e_1,e_1,e_3)
| equalish(e_1,e_2) ),
inference(resolution,[status(thm)],[c6731,c11985]) ).
cnf(c15528,plain,
( product(e_1,e_1,e_2)
| product(e_1,e_1,e_3) ),
inference(resolution,[status(thm)],[c15467,e_1_is_not_e_2]) ).
cnf(c15532,plain,
( product(e_1,e_1,e_3)
| product(e_3,e_1,e_3)
| equalish(e_1,e_3) ),
inference(resolution,[status(thm)],[c15528,c890]) ).
cnf(c16794,plain,
( product(e_1,e_1,e_3)
| product(e_3,e_1,e_3) ),
inference(resolution,[status(thm)],[c15532,e_1_is_not_e_3]) ).
cnf(c16795,plain,
( product(e_3,e_1,e_3)
| ~ product(e_1,e_1,X765)
| equalish(X765,e_3) ),
inference(resolution,[status(thm)],[c16794,product_total_function2]) ).
cnf(c15578,plain,
( product(e_1,e_1,e_2)
| ~ product(X757,e_1,e_3)
| equalish(X757,e_1) ),
inference(resolution,[status(thm)],[c15528,product_left_cancellation]) ).
cnf(c726,plain,
( product(e_3,e_1,e_1)
| product(e_3,e_1,e_3)
| ~ product(X391,e_1,e_2)
| equalish(X391,e_3) ),
inference(resolution,[status(thm)],[c255,product_left_cancellation]) ).
cnf(c937,plain,
( product(e_2,e_1,e_2)
| product(e_1,e_1,e_2)
| ~ product(X533,e_1,e_3)
| equalish(X533,e_2) ),
inference(resolution,[status(thm)],[c746,product_left_cancellation]) ).
cnf(c15526,plain,
( product(e_1,e_1,e_2)
| equalish(e_1,e_2)
| product(e_2,e_1,e_2) ),
inference(resolution,[status(thm)],[c15467,c937]) ).
cnf(c16230,plain,
( product(e_1,e_1,e_2)
| product(e_2,e_1,e_2) ),
inference(resolution,[status(thm)],[c15526,e_1_is_not_e_2]) ).
cnf(c16262,plain,
( product(e_2,e_1,e_2)
| ~ product(e_1,e_1,X759)
| equalish(X759,e_2) ),
inference(resolution,[status(thm)],[c16230,product_total_function2]) ).
cnf(c16796,plain,
( product(e_3,e_1,e_3)
| product(e_2,e_1,e_2)
| equalish(e_3,e_2) ),
inference(resolution,[status(thm)],[c16794,c16262]) ).
cnf(c18138,plain,
( product(e_3,e_1,e_3)
| product(e_2,e_1,e_2) ),
inference(resolution,[status(thm)],[c16796,e_3_is_not_e_2]) ).
cnf(c18193,plain,
( product(e_3,e_1,e_3)
| product(e_3,e_1,e_1)
| equalish(e_2,e_3) ),
inference(resolution,[status(thm)],[c18138,c726]) ).
cnf(c20127,plain,
( product(e_3,e_1,e_3)
| product(e_3,e_1,e_1) ),
inference(resolution,[status(thm)],[c18193,e_2_is_not_e_3]) ).
cnf(c20144,plain,
( product(e_3,e_1,e_1)
| product(e_1,e_1,e_2)
| equalish(e_3,e_1) ),
inference(resolution,[status(thm)],[c20127,c15578]) ).
cnf(c22222,plain,
( product(e_3,e_1,e_1)
| product(e_1,e_1,e_2) ),
inference(resolution,[status(thm)],[c20144,e_3_is_not_e_1]) ).
cnf(c22225,plain,
( product(e_1,e_1,e_2)
| ~ product(e_3,e_1,X806)
| equalish(X806,e_1) ),
inference(resolution,[status(thm)],[c22222,product_total_function2]) ).
cnf(c16314,plain,
( product(e_1,e_1,e_2)
| ~ product(e_2,X764,e_2)
| equalish(X764,e_1) ),
inference(resolution,[status(thm)],[c16230,product_right_cancellation]) ).
cnf(c235,plain,
( product(e_2,e_2,e_1)
| product(e_2,e_2,e_2)
| product(e_2,e_2,e_3) ),
inference(resolution,[status(thm)],[c50,element_2]) ).
cnf(c541,plain,
( product(e_2,e_2,e_2)
| product(e_2,e_2,e_3)
| ~ product(e_2,X285,e_2)
| product(e_1,X285,e_2) ),
inference(resolution,[status(thm)],[c235,qg3]) ).
cnf(c16297,plain,
( product(e_1,e_1,e_2)
| product(e_2,e_2,e_2)
| product(e_2,e_2,e_3) ),
inference(resolution,[status(thm)],[c16230,c541]) ).
cnf(c25062,plain,
( product(e_1,e_1,e_2)
| product(e_2,e_2,e_3)
| equalish(e_2,e_1) ),
inference(resolution,[status(thm)],[c16297,c16314]) ).
cnf(c25161,plain,
( product(e_1,e_1,e_2)
| product(e_2,e_2,e_3) ),
inference(resolution,[status(thm)],[c25062,e_2_is_not_e_1]) ).
cnf(c25202,plain,
( product(e_1,e_1,e_2)
| ~ product(e_2,X844,e_2)
| product(e_3,X844,e_2) ),
inference(resolution,[status(thm)],[c25161,qg3]) ).
cnf(c26823,plain,
( product(e_1,e_1,e_2)
| product(e_3,e_1,e_2) ),
inference(resolution,[status(thm)],[c25202,c16230]) ).
cnf(c26905,plain,
( product(e_1,e_1,e_2)
| equalish(e_2,e_1) ),
inference(resolution,[status(thm)],[c26823,c22225]) ).
cnf(c26951,plain,
product(e_1,e_1,e_2),
inference(resolution,[status(thm)],[c26905,e_2_is_not_e_1]) ).
cnf(c26957,plain,
( product(e_3,e_1,e_3)
| equalish(e_2,e_3) ),
inference(resolution,[status(thm)],[c26951,c16795]) ).
cnf(c27471,plain,
product(e_3,e_1,e_3),
inference(resolution,[status(thm)],[c26957,e_2_is_not_e_3]) ).
cnf(c27592,plain,
( ~ product(e_3,e_1,X848)
| equalish(X848,e_3) ),
inference(resolution,[status(thm)],[c27471,product_total_function2]) ).
cnf(c763,plain,
( product(e_2,e_1,e_1)
| product(e_2,e_1,e_2)
| ~ product(X412,e_1,e_3)
| equalish(X412,e_2) ),
inference(resolution,[status(thm)],[c257,product_left_cancellation]) ).
cnf(c18094,plain,
( product(e_2,e_1,e_2)
| equalish(e_3,e_2)
| product(e_2,e_1,e_1) ),
inference(resolution,[status(thm)],[c16796,c763]) ).
cnf(c19380,plain,
( product(e_2,e_1,e_2)
| product(e_2,e_1,e_1) ),
inference(resolution,[status(thm)],[c18094,e_3_is_not_e_2]) ).
cnf(c19429,plain,
( product(e_2,e_1,e_1)
| ~ product(X784,e_1,e_2)
| equalish(X784,e_2) ),
inference(resolution,[status(thm)],[c19380,product_left_cancellation]) ).
cnf(c26964,plain,
( product(e_2,e_1,e_1)
| equalish(e_1,e_2) ),
inference(resolution,[status(thm)],[c26951,c19429]) ).
cnf(c28139,plain,
product(e_2,e_1,e_1),
inference(resolution,[status(thm)],[c26964,e_1_is_not_e_2]) ).
cnf(c28159,plain,
( ~ product(e_2,X854,e_1)
| equalish(X854,e_1) ),
inference(resolution,[status(thm)],[c28139,product_right_cancellation]) ).
cnf(c801,plain,
( product(e_1,e_2,e_1)
| product(e_1,e_2,e_3)
| product(e_2,e_2,e_1) ),
inference(resolution,[status(thm)],[c263,c14]) ).
cnf(c26962,plain,
( ~ product(e_1,X851,e_1)
| product(e_2,X851,e_1) ),
inference(resolution,[status(thm)],[c26951,qg3]) ).
cnf(c28072,plain,
( product(e_2,e_2,e_1)
| product(e_1,e_2,e_3) ),
inference(resolution,[status(thm)],[c26962,c801]) ).
cnf(c28447,plain,
( product(e_1,e_2,e_3)
| equalish(e_2,e_1) ),
inference(resolution,[status(thm)],[c28072,c28159]) ).
cnf(c28506,plain,
product(e_1,e_2,e_3),
inference(resolution,[status(thm)],[c28447,e_2_is_not_e_1]) ).
cnf(c28514,plain,
( ~ product(e_1,X860,e_2)
| product(e_3,X860,e_1) ),
inference(resolution,[status(thm)],[c28506,qg3]) ).
cnf(c28702,plain,
product(e_3,e_1,e_1),
inference(resolution,[status(thm)],[c28514,c26951]) ).
cnf(c28729,plain,
equalish(e_1,e_3),
inference(resolution,[status(thm)],[c28702,c27592]) ).
cnf(c28745,plain,
$false,
inference(resolution,[status(thm)],[c28729,e_1_is_not_e_3]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.14 % Problem : GRP130-3.003 : TPTP v8.1.2. Released v1.2.0.
% 0.08/0.15 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.15/0.36 % Computer : n011.cluster.edu
% 0.15/0.36 % Model : x86_64 x86_64
% 0.15/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.36 % Memory : 8042.1875MB
% 0.15/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.36 % CPULimit : 300
% 0.15/0.36 % WCLimit : 300
% 0.15/0.36 % DateTime : Thu May 9 04:05:23 EDT 2024
% 0.15/0.37 % CPUTime :
% 22.07/22.32 % Version: 1.5
% 22.07/22.32 % SZS status Unsatisfiable
% 22.07/22.32 % SZS output start CNFRefutation
% See solution above
% 22.15/22.32
% 22.15/22.32 % Initial clauses : 30
% 22.15/22.32 % Processed clauses : 960
% 22.15/22.32 % Factors computed : 8
% 22.15/22.32 % Resolvents computed: 28738
% 22.15/22.32 % Tautologies deleted: 24
% 22.15/22.32 % Forward subsumed : 2691
% 22.15/22.32 % Backward subsumed : 653
% 22.15/22.32 % -------- CPU Time ---------
% 22.15/22.32 % User time : 21.847 s
% 22.15/22.32 % System time : 0.093 s
% 22.15/22.32 % Total time : 21.940 s
%------------------------------------------------------------------------------