%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GRP124-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:04 EDT 2024
% Result : Unsatisfiable 3.62s 3.82s
% Output : Refutation 3.62s
% Verified :
% SZS Type : Refutation
% Derivation depth : 23
% Number of leaves : 33
% Syntax : Number of clauses : 116 ( 28 unt; 44 nHn; 115 RR)
% Number of literals : 319 ( 0 equ; 139 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 : 76 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(e_4_is_not_e_3,axiom,
~ equalish(e_4,e_3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_4_is_not_e_3) ).
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_then_e_3,axiom,
next(e_2,e_3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_2_then_e_3) ).
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(e_1_then_e_2,axiom,
next(e_1,e_2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_1_then_e_2) ).
cnf(cycle4,axiom,
( ~ cycle(X13,X10)
| ~ cycle(X11,X9)
| ~ next(X13,X11)
| ~ greater(X10,e_0)
| ~ next(X9,X12)
| equalish(X10,X12) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cycle4) ).
cnf(c9,plain,
( ~ cycle(X125,X126)
| ~ cycle(X124,e_1)
| ~ next(X125,X124)
| ~ greater(X126,e_0)
| equalish(X126,e_2) ),
inference(resolution,[status(thm)],[cycle4,e_1_then_e_2]) ).
cnf(c115,plain,
( ~ cycle(X170,e_1)
| ~ cycle(X169,e_1)
| ~ next(X170,X169)
| equalish(e_1,e_2) ),
inference(resolution,[status(thm)],[c9,e_1_greater_e_0]) ).
cnf(c199,plain,
( ~ cycle(e_2,e_1)
| ~ cycle(e_3,e_1)
| equalish(e_1,e_2) ),
inference(resolution,[status(thm)],[c115,e_2_then_e_3]) ).
cnf(cycle3,axiom,
cycle(e_4,e_0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cycle3) ).
cnf(e_3_then_e_4,axiom,
next(e_3,e_4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_3_then_e_4) ).
cnf(e_3_greater_e_2,axiom,
greater(e_3,e_2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_3_greater_e_2) ).
cnf(e_3_greater_e_0,axiom,
greater(e_3,e_0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_3_greater_e_0) ).
cnf(cycle5,axiom,
( ~ cycle(X25,X24)
| ~ cycle(X22,e_0)
| ~ cycle(X23,X26)
| ~ next(X22,X23)
| ~ greater(X22,X25)
| ~ greater(X24,X26) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cycle5) ).
cnf(c22,plain,
( ~ cycle(X181,e_3)
| ~ cycle(X183,e_0)
| ~ cycle(X182,e_0)
| ~ next(X183,X182)
| ~ greater(X183,X181) ),
inference(resolution,[status(thm)],[cycle5,e_3_greater_e_0]) ).
cnf(c242,plain,
( ~ cycle(e_2,e_3)
| ~ cycle(e_3,e_0)
| ~ cycle(X296,e_0)
| ~ next(e_3,X296) ),
inference(resolution,[status(thm)],[c22,e_3_greater_e_2]) ).
cnf(c485,plain,
( ~ cycle(e_2,e_3)
| ~ cycle(e_3,e_0)
| ~ cycle(e_4,e_0) ),
inference(resolution,[status(thm)],[c242,e_3_then_e_4]) ).
cnf(c486,plain,
( ~ cycle(e_2,e_3)
| ~ cycle(e_3,e_0) ),
inference(resolution,[status(thm)],[c485,cycle3]) ).
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(e_0_then_e_1,axiom,
next(e_0,e_1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_0_then_e_1) ).
cnf(c8,plain,
( ~ cycle(X111,X112)
| ~ cycle(X110,e_0)
| ~ next(X111,X110)
| ~ greater(X112,e_0)
| equalish(X112,e_1) ),
inference(resolution,[status(thm)],[cycle4,e_0_then_e_1]) ).
cnf(c109,plain,
( ~ cycle(X157,e_3)
| ~ cycle(X158,e_0)
| ~ next(X157,X158)
| equalish(e_3,e_1) ),
inference(resolution,[status(thm)],[c8,e_3_greater_e_0]) ).
cnf(c166,plain,
( ~ cycle(e_3,e_3)
| ~ cycle(e_4,e_0)
| equalish(e_3,e_1) ),
inference(resolution,[status(thm)],[c109,e_3_then_e_4]) ).
cnf(c169,plain,
( ~ cycle(e_3,e_3)
| equalish(e_3,e_1) ),
inference(resolution,[status(thm)],[c166,cycle3]) ).
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(element_3,axiom,
group_element(e_3),
file('/export/starexec/sandbox/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/sandbox/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(e_2_greater_e_0,axiom,
greater(e_2,e_0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_2_greater_e_0) ).
cnf(c106,plain,
( ~ cycle(X142,e_2)
| ~ cycle(X143,e_0)
| ~ next(X142,X143)
| equalish(e_2,e_1) ),
inference(resolution,[status(thm)],[c8,e_2_greater_e_0]) ).
cnf(c127,plain,
( ~ cycle(e_3,e_2)
| ~ cycle(e_4,e_0)
| equalish(e_2,e_1) ),
inference(resolution,[status(thm)],[c106,e_3_then_e_4]) ).
cnf(c134,plain,
( ~ cycle(e_3,e_2)
| equalish(e_2,e_1) ),
inference(resolution,[status(thm)],[c127,cycle3]) ).
cnf(c135,plain,
( equalish(e_2,e_1)
| cycle(e_3,e_0)
| cycle(e_3,e_1)
| cycle(e_3,e_3) ),
inference(resolution,[status(thm)],[c134,c5]) ).
cnf(c499,plain,
( cycle(e_3,e_0)
| cycle(e_3,e_1)
| cycle(e_3,e_3) ),
inference(resolution,[status(thm)],[c135,e_2_is_not_e_1]) ).
cnf(c571,plain,
( cycle(e_3,e_0)
| cycle(e_3,e_1)
| equalish(e_3,e_1) ),
inference(resolution,[status(thm)],[c499,c169]) ).
cnf(c606,plain,
( cycle(e_3,e_0)
| cycle(e_3,e_1) ),
inference(resolution,[status(thm)],[c571,e_3_is_not_e_1]) ).
cnf(c611,plain,
( cycle(e_3,e_1)
| ~ cycle(e_2,e_3) ),
inference(resolution,[status(thm)],[c606,c486]) ).
cnf(c17,plain,
( ~ cycle(X154,e_2)
| ~ cycle(X156,e_0)
| ~ cycle(X155,e_0)
| ~ next(X156,X155)
| ~ greater(X156,X154) ),
inference(resolution,[status(thm)],[cycle5,e_2_greater_e_0]) ).
cnf(c161,plain,
( ~ cycle(e_2,e_2)
| ~ cycle(e_3,e_0)
| ~ cycle(X234,e_0)
| ~ next(e_3,X234) ),
inference(resolution,[status(thm)],[c17,e_3_greater_e_2]) ).
cnf(c362,plain,
( ~ cycle(e_2,e_2)
| ~ cycle(e_3,e_0)
| ~ cycle(e_4,e_0) ),
inference(resolution,[status(thm)],[c161,e_3_then_e_4]) ).
cnf(c363,plain,
( ~ cycle(e_2,e_2)
| ~ cycle(e_3,e_0) ),
inference(resolution,[status(thm)],[c362,cycle3]) ).
cnf(c612,plain,
( cycle(e_3,e_1)
| ~ cycle(e_2,e_2) ),
inference(resolution,[status(thm)],[c606,c363]) ).
cnf(element_2,axiom,
group_element(e_2),
file('/export/starexec/sandbox/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(c21,plain,
( ~ cycle(X176,e_1)
| ~ cycle(X178,e_0)
| ~ cycle(X177,e_0)
| ~ next(X178,X177)
| ~ greater(X178,X176) ),
inference(resolution,[status(thm)],[cycle5,e_1_greater_e_0]) ).
cnf(c225,plain,
( ~ cycle(e_2,e_1)
| ~ cycle(e_3,e_0)
| ~ cycle(X285,e_0)
| ~ next(e_3,X285) ),
inference(resolution,[status(thm)],[c21,e_3_greater_e_2]) ).
cnf(c468,plain,
( ~ cycle(e_2,e_1)
| ~ cycle(e_3,e_0)
| ~ cycle(e_4,e_0) ),
inference(resolution,[status(thm)],[c225,e_3_then_e_4]) ).
cnf(c469,plain,
( ~ cycle(e_2,e_1)
| ~ cycle(e_3,e_0) ),
inference(resolution,[status(thm)],[c468,cycle3]) ).
cnf(c610,plain,
( cycle(e_3,e_1)
| ~ cycle(e_2,e_1) ),
inference(resolution,[status(thm)],[c606,c469]) ).
cnf(c633,plain,
( cycle(e_3,e_1)
| cycle(e_2,e_0)
| cycle(e_2,e_2)
| cycle(e_2,e_3) ),
inference(resolution,[status(thm)],[c610,c4]) ).
cnf(c761,plain,
( cycle(e_3,e_1)
| cycle(e_2,e_0)
| cycle(e_2,e_3) ),
inference(resolution,[status(thm)],[c633,c612]) ).
cnf(c811,plain,
( cycle(e_3,e_1)
| cycle(e_2,e_0) ),
inference(resolution,[status(thm)],[c761,c611]) ).
cnf(c820,plain,
( cycle(e_2,e_0)
| ~ cycle(e_2,e_1)
| equalish(e_1,e_2) ),
inference(resolution,[status(thm)],[c811,c199]) ).
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(c116,plain,
( ~ cycle(X175,e_3)
| ~ cycle(X174,e_1)
| ~ next(X175,X174)
| equalish(e_3,e_2) ),
inference(resolution,[status(thm)],[c9,e_3_greater_e_0]) ).
cnf(c214,plain,
( ~ cycle(e_2,e_3)
| ~ cycle(e_3,e_1)
| equalish(e_3,e_2) ),
inference(resolution,[status(thm)],[c116,e_2_then_e_3]) ).
cnf(c816,plain,
( cycle(e_2,e_0)
| ~ cycle(e_2,e_3)
| equalish(e_3,e_2) ),
inference(resolution,[status(thm)],[c811,c214]) ).
cnf(c882,plain,
( cycle(e_2,e_0)
| equalish(e_3,e_2)
| cycle(e_2,e_1)
| cycle(e_2,e_2) ),
inference(resolution,[status(thm)],[c816,c4]) ).
cnf(c1138,plain,
( cycle(e_2,e_0)
| cycle(e_2,e_1)
| cycle(e_2,e_2) ),
inference(resolution,[status(thm)],[c882,e_3_is_not_e_2]) ).
cnf(c1223,plain,
( cycle(e_2,e_0)
| cycle(e_2,e_2)
| equalish(e_1,e_2) ),
inference(resolution,[status(thm)],[c1138,c820]) ).
cnf(c1266,plain,
( cycle(e_2,e_0)
| cycle(e_2,e_2) ),
inference(resolution,[status(thm)],[c1223,e_1_is_not_e_2]) ).
cnf(e_4_greater_e_2,axiom,
greater(e_4,e_2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_4_greater_e_2) ).
cnf(cycle6,axiom,
( ~ cycle(X39,e_0)
| ~ product(X39,e_1,X38)
| ~ greater(X38,X39) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cycle6) ).
cnf(product_idempotence,axiom,
product(X2,X2,X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',product_idempotence) ).
cnf(product_right_cancellation,axiom,
( ~ product(X33,X34,X32)
| ~ product(X33,X31,X32)
| equalish(X34,X31) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',product_right_cancellation) ).
cnf(c29,plain,
( ~ product(X41,X40,X41)
| equalish(X40,X41) ),
inference(resolution,[status(thm)],[product_right_cancellation,product_idempotence]) ).
cnf(product_left_cancellation,axiom,
( ~ product(X46,X44,X45)
| ~ product(X43,X44,X45)
| equalish(X46,X43) ),
file('/export/starexec/sandbox/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/sandbox/benchmark/theBenchmark.p',element_1) ).
cnf(product_total_function1,axiom,
( ~ group_element(X61)
| ~ group_element(X60)
| product(X61,X60,e_1)
| product(X61,X60,e_2)
| product(X61,X60,e_3)
| product(X61,X60,e_4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',product_total_function1) ).
cnf(c43,plain,
( ~ group_element(X217)
| product(X217,e_1,e_1)
| product(X217,e_1,e_2)
| product(X217,e_1,e_3)
| product(X217,e_1,e_4) ),
inference(resolution,[status(thm)],[product_total_function1,element_1]) ).
cnf(c330,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)],[c43,element_2]) ).
cnf(c926,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)],[c330,c33]) ).
cnf(c3056,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)],[c926,e_2_is_not_e_1]) ).
cnf(c3070,plain,
( product(e_2,e_1,e_3)
| product(e_2,e_1,e_4)
| equalish(e_1,e_2) ),
inference(resolution,[status(thm)],[c3056,c29]) ).
cnf(c3141,plain,
( product(e_2,e_1,e_3)
| product(e_2,e_1,e_4) ),
inference(resolution,[status(thm)],[c3070,e_1_is_not_e_2]) ).
cnf(c3156,plain,
( product(e_2,e_1,e_4)
| ~ cycle(e_2,e_0)
| ~ greater(e_3,e_2) ),
inference(resolution,[status(thm)],[c3141,cycle6]) ).
cnf(c3188,plain,
( product(e_2,e_1,e_4)
| ~ cycle(e_2,e_0) ),
inference(resolution,[status(thm)],[c3156,e_3_greater_e_2]) ).
cnf(c3190,plain,
( product(e_2,e_1,e_4)
| cycle(e_2,e_2) ),
inference(resolution,[status(thm)],[c3188,c1266]) ).
cnf(c3224,plain,
( cycle(e_2,e_2)
| ~ cycle(e_2,e_0)
| ~ greater(e_4,e_2) ),
inference(resolution,[status(thm)],[c3190,cycle6]) ).
cnf(c3276,plain,
( cycle(e_2,e_2)
| ~ cycle(e_2,e_0) ),
inference(resolution,[status(thm)],[c3224,e_4_greater_e_2]) ).
cnf(c3277,plain,
cycle(e_2,e_2),
inference(resolution,[status(thm)],[c3276,c1266]) ).
cnf(cycle7,axiom,
( ~ cycle(X53,X51)
| ~ product(X53,e_1,X50)
| ~ greater(X51,e_0)
| ~ next(X53,X52)
| equalish(X50,X52) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cycle7) ).
cnf(e_4_is_not_e_1,axiom,
~ equalish(e_4,e_1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_4_is_not_e_1) ).
cnf(c3151,plain,
( product(e_2,e_1,e_4)
| ~ product(e_2,X737,e_3)
| equalish(X737,e_1) ),
inference(resolution,[status(thm)],[c3141,product_right_cancellation]) ).
cnf(e_2_is_not_e_4,axiom,
~ equalish(e_2,e_4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_2_is_not_e_4) ).
cnf(qg2_2,negated_conjecture,
( ~ product(X87,X88,X85)
| ~ product(X84,X86,X85)
| ~ product(X83,X87,X88)
| ~ product(X83,X84,X86)
| equalish(X88,X86) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',qg2_2) ).
cnf(c73,plain,
( ~ product(X130,X132,X133)
| ~ product(X131,X131,X133)
| ~ product(X131,X130,X132)
| equalish(X132,X131) ),
inference(resolution,[status(thm)],[qg2_2,product_idempotence]) ).
cnf(e_4_is_not_e_2,axiom,
~ equalish(e_4,e_2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_4_is_not_e_2) ).
cnf(element_4,axiom,
group_element(e_4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',element_4) ).
cnf(c42,plain,
( ~ group_element(X212)
| product(X212,e_4,e_1)
| product(X212,e_4,e_2)
| product(X212,e_4,e_3)
| product(X212,e_4,e_4) ),
inference(resolution,[status(thm)],[product_total_function1,element_4]) ).
cnf(c324,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)],[c42,element_2]) ).
cnf(c701,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)],[c324,c29]) ).
cnf(c1458,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)],[c701,e_4_is_not_e_2]) ).
cnf(c1480,plain,
( product(e_2,e_4,e_1)
| product(e_2,e_4,e_3)
| equalish(e_2,e_4) ),
inference(resolution,[status(thm)],[c1458,c33]) ).
cnf(c1497,plain,
( product(e_2,e_4,e_1)
| product(e_2,e_4,e_3) ),
inference(resolution,[status(thm)],[c1480,e_2_is_not_e_4]) ).
cnf(c1501,plain,
( product(e_2,e_4,e_3)
| ~ product(e_4,e_1,X465)
| ~ product(e_2,e_2,X465)
| equalish(e_1,e_2) ),
inference(resolution,[status(thm)],[c1497,c73]) ).
cnf(c1646,plain,
( product(e_2,e_4,e_3)
| ~ product(e_4,e_1,e_2)
| equalish(e_1,e_2) ),
inference(resolution,[status(thm)],[c1501,product_idempotence]) ).
cnf(e_1_is_not_e_4,axiom,
~ equalish(e_1,e_4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_1_is_not_e_4) ).
cnf(c328,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)],[c43,element_4]) ).
cnf(c888,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)],[c328,c33]) ).
cnf(c2461,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)],[c888,e_4_is_not_e_1]) ).
cnf(c2492,plain,
( product(e_4,e_1,e_2)
| product(e_4,e_1,e_3)
| equalish(e_1,e_4) ),
inference(resolution,[status(thm)],[c2461,c29]) ).
cnf(c2516,plain,
( product(e_4,e_1,e_2)
| product(e_4,e_1,e_3) ),
inference(resolution,[status(thm)],[c2492,e_1_is_not_e_4]) ).
cnf(c2518,plain,
( product(e_4,e_1,e_3)
| product(e_2,e_4,e_3)
| equalish(e_1,e_2) ),
inference(resolution,[status(thm)],[c2516,c1646]) ).
cnf(c2594,plain,
( product(e_4,e_1,e_3)
| product(e_2,e_4,e_3) ),
inference(resolution,[status(thm)],[c2518,e_1_is_not_e_2]) ).
cnf(c2597,plain,
( product(e_2,e_4,e_3)
| ~ product(X668,e_1,e_3)
| equalish(X668,e_4) ),
inference(resolution,[status(thm)],[c2594,product_left_cancellation]) ).
cnf(c3144,plain,
( product(e_2,e_1,e_4)
| product(e_2,e_4,e_3)
| equalish(e_2,e_4) ),
inference(resolution,[status(thm)],[c3141,c2597]) ).
cnf(c3495,plain,
( product(e_2,e_1,e_4)
| product(e_2,e_4,e_3) ),
inference(resolution,[status(thm)],[c3144,e_2_is_not_e_4]) ).
cnf(c3539,plain,
( product(e_2,e_1,e_4)
| equalish(e_4,e_1) ),
inference(resolution,[status(thm)],[c3495,c3151]) ).
cnf(c3590,plain,
product(e_2,e_1,e_4),
inference(resolution,[status(thm)],[c3539,e_4_is_not_e_1]) ).
cnf(c3592,plain,
( ~ cycle(e_2,X811)
| ~ greater(X811,e_0)
| ~ next(e_2,X812)
| equalish(e_4,X812) ),
inference(resolution,[status(thm)],[c3590,cycle7]) ).
cnf(c3633,plain,
( ~ cycle(e_2,X813)
| ~ greater(X813,e_0)
| equalish(e_4,e_3) ),
inference(resolution,[status(thm)],[c3592,e_2_then_e_3]) ).
cnf(c3634,plain,
( ~ cycle(e_2,e_2)
| equalish(e_4,e_3) ),
inference(resolution,[status(thm)],[c3633,e_2_greater_e_0]) ).
cnf(c3638,plain,
equalish(e_4,e_3),
inference(resolution,[status(thm)],[c3634,c3277]) ).
cnf(c3639,plain,
$false,
inference(resolution,[status(thm)],[c3638,e_4_is_not_e_3]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.12 % Problem : GRP124-3.004 : TPTP v8.1.2. Released v1.2.0.
% 0.04/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.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 300
% 0.13/0.35 % DateTime : Thu May 9 03:43:23 EDT 2024
% 0.13/0.35 % CPUTime :
% 3.62/3.82 % Version: 1.5
% 3.62/3.82 % SZS status Unsatisfiable
% 3.62/3.82 % SZS output start CNFRefutation
% See solution above
% 3.62/3.82
% 3.62/3.82 % Initial clauses : 44
% 3.62/3.82 % Processed clauses : 671
% 3.62/3.82 % Factors computed : 44
% 3.62/3.82 % Resolvents computed: 3596
% 3.62/3.82 % Tautologies deleted: 20
% 3.62/3.82 % Forward subsumed : 1229
% 3.62/3.82 % Backward subsumed : 336
% 3.62/3.82 % -------- CPU Time ---------
% 3.62/3.82 % User time : 3.438 s
% 3.62/3.82 % System time : 0.023 s
% 3.62/3.82 % Total time : 3.461 s
%------------------------------------------------------------------------------