%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GRP124-7.004 : TPTP v8.1.2. Released v1.2.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n029.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:05 EDT 2024
% Result : Unsatisfiable 7.42s 7.61s
% Output : Refutation 7.42s
% Verified :
% SZS Type : Refutation
% Derivation depth : 34
% Number of leaves : 24
% Syntax : Number of clauses : 119 ( 24 unt; 82 nHn; 117 RR)
% Number of literals : 295 ( 0 equ; 50 neg)
% Maximal clause size : 6 ( 2 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 5 ( 4 usr; 1 prp; 0-3 aty)
% Number of functors : 4 ( 4 usr; 4 con; 0-0 aty)
% Number of variables : 56 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
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(product1_left_cancellation,axiom,
( ~ product1(X27,X24,X25)
| ~ product1(X26,X24,X25)
| equalish(X27,X26) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',product1_left_cancellation) ).
cnf(e_3_is_not_e_4,axiom,
~ equalish(e_3,e_4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_3_is_not_e_4) ).
cnf(product2_left_cancellation,axiom,
( ~ product2(X65,X62,X63)
| ~ product2(X64,X62,X63)
| equalish(X65,X64) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',product2_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(product1_idempotence,axiom,
product1(X2,X2,X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',product1_idempotence) ).
cnf(c12,plain,
( ~ product1(X38,X37,X37)
| equalish(X38,X37) ),
inference(resolution,[status(thm)],[product1_left_cancellation,product1_idempotence]) ).
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(product1_right_cancellation,axiom,
( ~ product1(X21,X23,X20)
| ~ product1(X21,X22,X20)
| equalish(X23,X22) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',product1_right_cancellation) ).
cnf(c10,plain,
( ~ product1(X31,X32,X31)
| equalish(X32,X31) ),
inference(resolution,[status(thm)],[product1_right_cancellation,product1_idempotence]) ).
cnf(element_1,axiom,
group_element(e_1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',element_1) ).
cnf(element_2,axiom,
group_element(e_2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',element_2) ).
cnf(product1_total_function1,axiom,
( ~ group_element(X12)
| ~ group_element(X11)
| product1(X12,X11,e_1)
| product1(X12,X11,e_2)
| product1(X12,X11,e_3)
| product1(X12,X11,e_4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',product1_total_function1) ).
cnf(c4,plain,
( ~ group_element(X83)
| product1(X83,e_2,e_1)
| product1(X83,e_2,e_2)
| product1(X83,e_2,e_3)
| product1(X83,e_2,e_4) ),
inference(resolution,[status(thm)],[product1_total_function1,element_2]) ).
cnf(c44,plain,
( product1(e_1,e_2,e_1)
| product1(e_1,e_2,e_2)
| product1(e_1,e_2,e_3)
| product1(e_1,e_2,e_4) ),
inference(resolution,[status(thm)],[c4,element_1]) ).
cnf(c184,plain,
( product1(e_1,e_2,e_2)
| product1(e_1,e_2,e_3)
| product1(e_1,e_2,e_4)
| equalish(e_2,e_1) ),
inference(resolution,[status(thm)],[c44,c10]) ).
cnf(c1225,plain,
( product1(e_1,e_2,e_2)
| product1(e_1,e_2,e_3)
| product1(e_1,e_2,e_4) ),
inference(resolution,[status(thm)],[c184,e_2_is_not_e_1]) ).
cnf(c1235,plain,
( product1(e_1,e_2,e_3)
| product1(e_1,e_2,e_4)
| equalish(e_1,e_2) ),
inference(resolution,[status(thm)],[c1225,c12]) ).
cnf(c1277,plain,
( product1(e_1,e_2,e_3)
| product1(e_1,e_2,e_4) ),
inference(resolution,[status(thm)],[c1235,e_1_is_not_e_2]) ).
cnf(qg2a,negated_conjecture,
( ~ product1(X71,X70,X69)
| ~ product1(X69,X71,X72)
| product2(X72,X70,X71) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',qg2a) ).
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(product1_total_function2,axiom,
( ~ product1(X8,X7,X10)
| ~ product1(X8,X7,X9)
| equalish(X10,X9) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',product1_total_function2) ).
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_3,axiom,
~ equalish(e_1,e_3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_1_is_not_e_3) ).
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(element_3,axiom,
group_element(e_3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',element_3) ).
cnf(c3,plain,
( ~ group_element(X82)
| product1(X82,e_1,e_1)
| product1(X82,e_1,e_2)
| product1(X82,e_1,e_3)
| product1(X82,e_1,e_4) ),
inference(resolution,[status(thm)],[product1_total_function1,element_1]) ).
cnf(c42,plain,
( product1(e_3,e_1,e_1)
| product1(e_3,e_1,e_2)
| product1(e_3,e_1,e_3)
| product1(e_3,e_1,e_4) ),
inference(resolution,[status(thm)],[c3,element_3]) ).
cnf(c141,plain,
( product1(e_3,e_1,e_2)
| product1(e_3,e_1,e_3)
| product1(e_3,e_1,e_4)
| equalish(e_3,e_1) ),
inference(resolution,[status(thm)],[c42,c12]) ).
cnf(c304,plain,
( product1(e_3,e_1,e_2)
| product1(e_3,e_1,e_3)
| product1(e_3,e_1,e_4) ),
inference(resolution,[status(thm)],[c141,e_3_is_not_e_1]) ).
cnf(c310,plain,
( product1(e_3,e_1,e_2)
| product1(e_3,e_1,e_4)
| equalish(e_1,e_3) ),
inference(resolution,[status(thm)],[c304,c10]) ).
cnf(c330,plain,
( product1(e_3,e_1,e_2)
| product1(e_3,e_1,e_4) ),
inference(resolution,[status(thm)],[c310,e_1_is_not_e_3]) ).
cnf(c334,plain,
( product1(e_3,e_1,e_4)
| ~ product1(X120,e_1,e_2)
| equalish(X120,e_3) ),
inference(resolution,[status(thm)],[c330,product1_left_cancellation]) ).
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(element_4,axiom,
group_element(e_4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',element_4) ).
cnf(c43,plain,
( product1(e_4,e_1,e_1)
| product1(e_4,e_1,e_2)
| product1(e_4,e_1,e_3)
| product1(e_4,e_1,e_4) ),
inference(resolution,[status(thm)],[c3,element_4]) ).
cnf(c165,plain,
( product1(e_4,e_1,e_2)
| product1(e_4,e_1,e_3)
| product1(e_4,e_1,e_4)
| equalish(e_4,e_1) ),
inference(resolution,[status(thm)],[c43,c12]) ).
cnf(c660,plain,
( product1(e_4,e_1,e_2)
| product1(e_4,e_1,e_3)
| product1(e_4,e_1,e_4) ),
inference(resolution,[status(thm)],[c165,e_4_is_not_e_1]) ).
cnf(c678,plain,
( product1(e_4,e_1,e_2)
| product1(e_4,e_1,e_3)
| equalish(e_1,e_4) ),
inference(resolution,[status(thm)],[c660,c10]) ).
cnf(c693,plain,
( product1(e_4,e_1,e_2)
| product1(e_4,e_1,e_3) ),
inference(resolution,[status(thm)],[c678,e_1_is_not_e_4]) ).
cnf(c696,plain,
( product1(e_4,e_1,e_3)
| product1(e_3,e_1,e_4)
| equalish(e_4,e_3) ),
inference(resolution,[status(thm)],[c693,c334]) ).
cnf(c773,plain,
( product1(e_4,e_1,e_3)
| product1(e_3,e_1,e_4) ),
inference(resolution,[status(thm)],[c696,e_4_is_not_e_3]) ).
cnf(c779,plain,
( product1(e_3,e_1,e_4)
| ~ product1(e_4,e_1,X168)
| equalish(X168,e_3) ),
inference(resolution,[status(thm)],[c773,product1_total_function2]) ).
cnf(product2_idempotence,axiom,
product2(X3,X3,X3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',product2_idempotence) ).
cnf(product2_total_function2,axiom,
( ~ product2(X43,X42,X45)
| ~ product2(X43,X42,X44)
| equalish(X45,X44) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',product2_total_function2) ).
cnf(c21,plain,
( ~ product2(X50,X50,X49)
| equalish(X49,X50) ),
inference(resolution,[status(thm)],[product2_total_function2,product2_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(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(c41,plain,
( product1(e_2,e_1,e_1)
| product1(e_2,e_1,e_2)
| product1(e_2,e_1,e_3)
| product1(e_2,e_1,e_4) ),
inference(resolution,[status(thm)],[c3,element_2]) ).
cnf(c76,plain,
( product1(e_2,e_1,e_2)
| product1(e_2,e_1,e_3)
| product1(e_2,e_1,e_4)
| equalish(e_2,e_1) ),
inference(resolution,[status(thm)],[c41,c12]) ).
cnf(c105,plain,
( product1(e_2,e_1,e_2)
| product1(e_2,e_1,e_3)
| product1(e_2,e_1,e_4) ),
inference(resolution,[status(thm)],[c76,e_2_is_not_e_1]) ).
cnf(c106,plain,
( product1(e_2,e_1,e_3)
| product1(e_2,e_1,e_4)
| equalish(e_1,e_2) ),
inference(resolution,[status(thm)],[c105,c10]) ).
cnf(c128,plain,
( product1(e_2,e_1,e_3)
| product1(e_2,e_1,e_4) ),
inference(resolution,[status(thm)],[c106,e_1_is_not_e_2]) ).
cnf(c136,plain,
( product1(e_2,e_1,e_3)
| ~ product1(X95,e_1,e_4)
| equalish(X95,e_2) ),
inference(resolution,[status(thm)],[c128,product1_left_cancellation]) ).
cnf(c339,plain,
( product1(e_3,e_1,e_2)
| product1(e_2,e_1,e_3)
| equalish(e_3,e_2) ),
inference(resolution,[status(thm)],[c330,c136]) ).
cnf(c436,plain,
( product1(e_3,e_1,e_2)
| product1(e_2,e_1,e_3) ),
inference(resolution,[status(thm)],[c339,e_3_is_not_e_2]) ).
cnf(c451,plain,
( product1(e_3,e_1,e_2)
| ~ product1(X131,e_1,e_3)
| equalish(X131,e_2) ),
inference(resolution,[status(thm)],[c436,product1_left_cancellation]) ).
cnf(c702,plain,
( product1(e_4,e_1,e_2)
| product1(e_3,e_1,e_2)
| equalish(e_4,e_2) ),
inference(resolution,[status(thm)],[c693,c451]) ).
cnf(c927,plain,
( product1(e_4,e_1,e_2)
| product1(e_3,e_1,e_2) ),
inference(resolution,[status(thm)],[c702,e_4_is_not_e_2]) ).
cnf(c941,plain,
( product1(e_4,e_1,e_2)
| ~ product1(e_1,X231,e_3)
| product2(e_2,X231,e_1) ),
inference(resolution,[status(thm)],[c927,qg2a]) ).
cnf(c1278,plain,
( product1(e_1,e_2,e_4)
| product1(e_4,e_1,e_2)
| product2(e_2,e_2,e_1) ),
inference(resolution,[status(thm)],[c1277,c941]) ).
cnf(c1353,plain,
( product1(e_1,e_2,e_4)
| product1(e_4,e_1,e_2)
| equalish(e_1,e_2) ),
inference(resolution,[status(thm)],[c1278,c21]) ).
cnf(c1388,plain,
( product1(e_1,e_2,e_4)
| product1(e_4,e_1,e_2) ),
inference(resolution,[status(thm)],[c1353,e_1_is_not_e_2]) ).
cnf(c1417,plain,
( product1(e_1,e_2,e_4)
| product1(e_3,e_1,e_4)
| equalish(e_2,e_3) ),
inference(resolution,[status(thm)],[c1388,c779]) ).
cnf(c1735,plain,
( product1(e_1,e_2,e_4)
| product1(e_3,e_1,e_4) ),
inference(resolution,[status(thm)],[c1417,e_2_is_not_e_3]) ).
cnf(c1769,plain,
( product1(e_1,e_2,e_4)
| ~ product1(e_1,X413,e_3)
| product2(e_4,X413,e_1) ),
inference(resolution,[status(thm)],[c1735,qg2a]) ).
cnf(c2267,plain,
( product1(e_1,e_2,e_4)
| product2(e_4,e_2,e_1) ),
inference(resolution,[status(thm)],[c1769,c1277]) ).
cnf(c2298,plain,
( product1(e_1,e_2,e_4)
| ~ product2(X419,e_2,e_1)
| equalish(X419,e_4) ),
inference(resolution,[status(thm)],[c2267,product2_left_cancellation]) ).
cnf(c442,plain,
( product1(e_2,e_1,e_3)
| ~ product1(X128,e_1,e_2)
| equalish(X128,e_3) ),
inference(resolution,[status(thm)],[c436,product1_left_cancellation]) ).
cnf(c699,plain,
( product1(e_4,e_1,e_3)
| product1(e_2,e_1,e_3)
| equalish(e_4,e_3) ),
inference(resolution,[status(thm)],[c693,c442]) ).
cnf(c842,plain,
( product1(e_4,e_1,e_3)
| product1(e_2,e_1,e_3) ),
inference(resolution,[status(thm)],[c699,e_4_is_not_e_3]) ).
cnf(c847,plain,
( product1(e_2,e_1,e_3)
| ~ product1(e_1,X219,e_4)
| product2(e_3,X219,e_1) ),
inference(resolution,[status(thm)],[c842,qg2a]) ).
cnf(c1409,plain,
( product1(e_1,e_2,e_4)
| product1(e_2,e_1,e_3)
| equalish(e_4,e_3) ),
inference(resolution,[status(thm)],[c1388,c442]) ).
cnf(c1552,plain,
( product1(e_1,e_2,e_4)
| product1(e_2,e_1,e_3) ),
inference(resolution,[status(thm)],[c1409,e_4_is_not_e_3]) ).
cnf(c1569,plain,
( product1(e_2,e_1,e_3)
| product2(e_3,e_2,e_1) ),
inference(resolution,[status(thm)],[c1552,c847]) ).
cnf(c46,plain,
( product1(e_3,e_2,e_1)
| product1(e_3,e_2,e_2)
| product1(e_3,e_2,e_3)
| product1(e_3,e_2,e_4) ),
inference(resolution,[status(thm)],[c4,element_3]) ).
cnf(c216,plain,
( product1(e_3,e_2,e_1)
| product1(e_3,e_2,e_3)
| product1(e_3,e_2,e_4)
| equalish(e_3,e_2) ),
inference(resolution,[status(thm)],[c46,c12]) ).
cnf(c1958,plain,
( product1(e_3,e_2,e_1)
| product1(e_3,e_2,e_3)
| product1(e_3,e_2,e_4) ),
inference(resolution,[status(thm)],[c216,e_3_is_not_e_2]) ).
cnf(c6840,plain,
( product1(e_3,e_2,e_1)
| product1(e_3,e_2,e_4)
| equalish(e_2,e_3) ),
inference(resolution,[status(thm)],[c1958,c10]) ).
cnf(c6907,plain,
( product1(e_3,e_2,e_1)
| product1(e_3,e_2,e_4) ),
inference(resolution,[status(thm)],[c6840,e_2_is_not_e_3]) ).
cnf(c6939,plain,
( product1(e_3,e_2,e_1)
| ~ product1(X597,e_2,e_4)
| equalish(X597,e_3) ),
inference(resolution,[status(thm)],[c6907,product1_left_cancellation]) ).
cnf(c1758,plain,
( product1(e_1,e_2,e_4)
| ~ product1(e_3,X368,e_4)
| equalish(X368,e_1) ),
inference(resolution,[status(thm)],[c1735,product1_right_cancellation]) ).
cnf(c6925,plain,
( product1(e_3,e_2,e_1)
| product1(e_1,e_2,e_4)
| equalish(e_2,e_1) ),
inference(resolution,[status(thm)],[c6907,c1758]) ).
cnf(c7203,plain,
( product1(e_3,e_2,e_1)
| product1(e_1,e_2,e_4) ),
inference(resolution,[status(thm)],[c6925,e_2_is_not_e_1]) ).
cnf(c7226,plain,
( product1(e_3,e_2,e_1)
| equalish(e_1,e_3) ),
inference(resolution,[status(thm)],[c7203,c6939]) ).
cnf(c7270,plain,
product1(e_3,e_2,e_1),
inference(resolution,[status(thm)],[c7226,e_1_is_not_e_3]) ).
cnf(c7280,plain,
( ~ product1(e_2,X602,e_3)
| product2(e_1,X602,e_2) ),
inference(resolution,[status(thm)],[c7270,qg2a]) ).
cnf(c7489,plain,
( product2(e_1,e_1,e_2)
| product2(e_3,e_2,e_1) ),
inference(resolution,[status(thm)],[c7280,c1569]) ).
cnf(c7510,plain,
( product2(e_3,e_2,e_1)
| equalish(e_2,e_1) ),
inference(resolution,[status(thm)],[c7489,c21]) ).
cnf(c7558,plain,
product2(e_3,e_2,e_1),
inference(resolution,[status(thm)],[c7510,e_2_is_not_e_1]) ).
cnf(c7571,plain,
( product1(e_1,e_2,e_4)
| equalish(e_3,e_4) ),
inference(resolution,[status(thm)],[c7558,c2298]) ).
cnf(c7818,plain,
product1(e_1,e_2,e_4),
inference(resolution,[status(thm)],[c7571,e_3_is_not_e_4]) ).
cnf(c7844,plain,
( ~ product1(X619,e_2,e_4)
| equalish(X619,e_1) ),
inference(resolution,[status(thm)],[c7818,product1_left_cancellation]) ).
cnf(c785,plain,
( product1(e_4,e_1,e_3)
| ~ product1(e_1,X214,e_3)
| product2(e_4,X214,e_1) ),
inference(resolution,[status(thm)],[c773,qg2a]) ).
cnf(c865,plain,
( product1(e_4,e_1,e_3)
| ~ product1(e_2,e_1,X181)
| equalish(X181,e_3) ),
inference(resolution,[status(thm)],[c842,product1_total_function2]) ).
cnf(c132,plain,
( product1(e_2,e_1,e_4)
| ~ product1(X92,e_1,e_3)
| equalish(X92,e_2) ),
inference(resolution,[status(thm)],[c128,product1_left_cancellation]) ).
cnf(c705,plain,
( product1(e_4,e_1,e_2)
| product1(e_2,e_1,e_4)
| equalish(e_4,e_2) ),
inference(resolution,[status(thm)],[c693,c132]) ).
cnf(c1010,plain,
( product1(e_4,e_1,e_2)
| product1(e_2,e_1,e_4) ),
inference(resolution,[status(thm)],[c705,e_4_is_not_e_2]) ).
cnf(c1013,plain,
( product1(e_2,e_1,e_4)
| ~ product1(e_1,X238,e_4)
| product2(e_2,X238,e_1) ),
inference(resolution,[status(thm)],[c1010,qg2a]) ).
cnf(c1292,plain,
( product1(e_1,e_2,e_3)
| product1(e_2,e_1,e_4)
| product2(e_2,e_2,e_1) ),
inference(resolution,[status(thm)],[c1277,c1013]) ).
cnf(c2896,plain,
( product1(e_1,e_2,e_3)
| product1(e_2,e_1,e_4)
| equalish(e_1,e_2) ),
inference(resolution,[status(thm)],[c1292,c21]) ).
cnf(c2948,plain,
( product1(e_1,e_2,e_3)
| product1(e_2,e_1,e_4) ),
inference(resolution,[status(thm)],[c2896,e_1_is_not_e_2]) ).
cnf(c2984,plain,
( product1(e_1,e_2,e_3)
| product1(e_4,e_1,e_3)
| equalish(e_4,e_3) ),
inference(resolution,[status(thm)],[c2948,c865]) ).
cnf(c3406,plain,
( product1(e_1,e_2,e_3)
| product1(e_4,e_1,e_3) ),
inference(resolution,[status(thm)],[c2984,e_4_is_not_e_3]) ).
cnf(c3423,plain,
( product1(e_4,e_1,e_3)
| product2(e_4,e_2,e_1) ),
inference(resolution,[status(thm)],[c3406,c785]) ).
cnf(c3483,plain,
( product1(e_4,e_1,e_3)
| ~ product2(X473,e_2,e_1)
| equalish(X473,e_4) ),
inference(resolution,[status(thm)],[c3423,product2_left_cancellation]) ).
cnf(c7569,plain,
( product1(e_4,e_1,e_3)
| equalish(e_3,e_4) ),
inference(resolution,[status(thm)],[c7558,c3483]) ).
cnf(c7731,plain,
product1(e_4,e_1,e_3),
inference(resolution,[status(thm)],[c7569,e_3_is_not_e_4]) ).
cnf(c7733,plain,
( ~ product1(e_4,X612,e_3)
| equalish(X612,e_1) ),
inference(resolution,[status(thm)],[c7731,product1_right_cancellation]) ).
cnf(c7282,plain,
( ~ product1(X601,e_2,e_1)
| equalish(X601,e_3) ),
inference(resolution,[status(thm)],[c7270,product1_left_cancellation]) ).
cnf(c47,plain,
( product1(e_4,e_2,e_1)
| product1(e_4,e_2,e_2)
| product1(e_4,e_2,e_3)
| product1(e_4,e_2,e_4) ),
inference(resolution,[status(thm)],[c4,element_4]) ).
cnf(c235,plain,
( product1(e_4,e_2,e_1)
| product1(e_4,e_2,e_3)
| product1(e_4,e_2,e_4)
| equalish(e_4,e_2) ),
inference(resolution,[status(thm)],[c47,c12]) ).
cnf(c2180,plain,
( product1(e_4,e_2,e_1)
| product1(e_4,e_2,e_3)
| product1(e_4,e_2,e_4) ),
inference(resolution,[status(thm)],[c235,e_4_is_not_e_2]) ).
cnf(c8532,plain,
( product1(e_4,e_2,e_3)
| product1(e_4,e_2,e_4)
| equalish(e_4,e_3) ),
inference(resolution,[status(thm)],[c2180,c7282]) ).
cnf(c8595,plain,
( product1(e_4,e_2,e_3)
| product1(e_4,e_2,e_4) ),
inference(resolution,[status(thm)],[c8532,e_4_is_not_e_3]) ).
cnf(c8600,plain,
( product1(e_4,e_2,e_4)
| equalish(e_2,e_1) ),
inference(resolution,[status(thm)],[c8595,c7733]) ).
cnf(c8634,plain,
product1(e_4,e_2,e_4),
inference(resolution,[status(thm)],[c8600,e_2_is_not_e_1]) ).
cnf(c8642,plain,
equalish(e_4,e_1),
inference(resolution,[status(thm)],[c8634,c7844]) ).
cnf(c8646,plain,
$false,
inference(resolution,[status(thm)],[c8642,e_4_is_not_e_1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.14 % Problem : GRP124-7.004 : TPTP v8.1.2. Released v1.2.0.
% 0.07/0.15 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.36 % Computer : n029.cluster.edu
% 0.14/0.36 % Model : x86_64 x86_64
% 0.14/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.36 % Memory : 8042.1875MB
% 0.14/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.37 % CPULimit : 300
% 0.14/0.37 % WCLimit : 300
% 0.14/0.37 % DateTime : Thu May 9 04:17:23 EDT 2024
% 0.14/0.37 % CPUTime :
% 7.42/7.61 % Version: 1.5
% 7.42/7.61 % SZS status Unsatisfiable
% 7.42/7.61 % SZS output start CNFRefutation
% See solution above
% 7.42/7.61
% 7.42/7.61 % Initial clauses : 37
% 7.42/7.61 % Processed clauses : 605
% 7.42/7.61 % Factors computed : 9
% 7.42/7.61 % Resolvents computed: 8638
% 7.42/7.61 % Tautologies deleted: 0
% 7.42/7.61 % Forward subsumed : 1823
% 7.42/7.61 % Backward subsumed : 321
% 7.42/7.61 % -------- CPU Time ---------
% 7.42/7.61 % User time : 7.193 s
% 7.42/7.61 % System time : 0.042 s
% 7.42/7.61 % Total time : 7.235 s
%------------------------------------------------------------------------------