%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GRP129-2.004 : TPTP v8.1.2. Released v1.2.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n027.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:11 EDT 2024
% Result : Unsatisfiable 50.59s 50.83s
% Output : Refutation 50.59s
% Verified :
% SZS Type : Refutation
% Derivation depth : 63
% Number of leaves : 25
% Syntax : Number of clauses : 163 ( 30 unt; 122 nHn; 163 RR)
% Number of literals : 479 ( 0 equ; 76 neg)
% Maximal clause size : 6 ( 2 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 6 ( 5 usr; 1 prp; 0-3 aty)
% Number of functors : 4 ( 4 usr; 4 con; 0-0 aty)
% Number of variables : 68 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
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(product_left_cancellation,axiom,
( ~ product(X24,X22,X23)
| ~ product(X21,X22,X23)
| equalish(X24,X21) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',product_left_cancellation) ).
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(e_1_then_e_2,axiom,
next(e_1,e_2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_1_then_e_2) ).
cnf(e_4_greater_e_2,axiom,
greater(e_4,e_2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_4_greater_e_2) ).
cnf(no_redundancy,axiom,
( ~ product(X3,e_1,X2)
| ~ next(X3,X4)
| ~ greater(X2,X4) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',no_redundancy) ).
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(element_1,axiom,
group_element(e_1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',element_1) ).
cnf(product_total_function1,axiom,
( ~ group_element(X17)
| ~ group_element(X16)
| product(X17,X16,e_1)
| product(X17,X16,e_2)
| product(X17,X16,e_3)
| product(X17,X16,e_4) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',product_total_function1) ).
cnf(c2,plain,
( ~ group_element(X33)
| product(X33,X33,e_1)
| product(X33,X33,e_2)
| product(X33,X33,e_3)
| product(X33,X33,e_4) ),
inference(factor,[status(thm)],[product_total_function1]) ).
cnf(c9,plain,
( product(e_1,e_1,e_1)
| product(e_1,e_1,e_2)
| product(e_1,e_1,e_3)
| product(e_1,e_1,e_4) ),
inference(resolution,[status(thm)],[c2,element_1]) ).
cnf(c52,plain,
( product(e_1,e_1,e_1)
| product(e_1,e_1,e_2)
| product(e_1,e_1,e_4)
| ~ next(e_1,X80)
| ~ greater(e_3,X80) ),
inference(resolution,[status(thm)],[c9,no_redundancy]) ).
cnf(c910,plain,
( product(e_1,e_1,e_1)
| product(e_1,e_1,e_2)
| product(e_1,e_1,e_4)
| ~ next(e_1,e_2) ),
inference(resolution,[status(thm)],[c52,e_3_greater_e_2]) ).
cnf(c1123,plain,
( product(e_1,e_1,e_1)
| product(e_1,e_1,e_2)
| product(e_1,e_1,e_4) ),
inference(resolution,[status(thm)],[c910,e_1_then_e_2]) ).
cnf(c1163,plain,
( product(e_1,e_1,e_1)
| product(e_1,e_1,e_2)
| ~ next(e_1,X169)
| ~ greater(e_4,X169) ),
inference(resolution,[status(thm)],[c1123,no_redundancy]) ).
cnf(c1181,plain,
( product(e_1,e_1,e_1)
| product(e_1,e_1,e_2)
| ~ next(e_1,e_2) ),
inference(resolution,[status(thm)],[c1163,e_4_greater_e_2]) ).
cnf(c1182,plain,
( product(e_1,e_1,e_1)
| product(e_1,e_1,e_2) ),
inference(resolution,[status(thm)],[c1181,e_1_then_e_2]) ).
cnf(c1207,plain,
( product(e_1,e_1,e_1)
| ~ product(X180,e_1,e_2)
| equalish(X180,e_1) ),
inference(resolution,[status(thm)],[c1182,product_left_cancellation]) ).
cnf(product_right_cancellation,axiom,
( ~ product(X14,X15,X13)
| ~ product(X14,X12,X13)
| equalish(X15,X12) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',product_right_cancellation) ).
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(element_3,axiom,
group_element(e_3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',element_3) ).
cnf(c3,plain,
( ~ group_element(X34)
| product(X34,e_1,e_1)
| product(X34,e_1,e_2)
| product(X34,e_1,e_3)
| product(X34,e_1,e_4) ),
inference(resolution,[status(thm)],[product_total_function1,element_1]) ).
cnf(c15,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) ),
inference(resolution,[status(thm)],[c3,element_3]) ).
cnf(c1195,plain,
( product(e_1,e_1,e_2)
| ~ product(X176,e_1,e_1)
| equalish(X176,e_1) ),
inference(resolution,[status(thm)],[c1182,product_left_cancellation]) ).
cnf(c1224,plain,
( product(e_1,e_1,e_2)
| equalish(e_3,e_1)
| product(e_3,e_1,e_2)
| product(e_3,e_1,e_3)
| product(e_3,e_1,e_4) ),
inference(resolution,[status(thm)],[c1195,c15]) ).
cnf(c3869,plain,
( product(e_1,e_1,e_2)
| product(e_3,e_1,e_2)
| product(e_3,e_1,e_3)
| product(e_3,e_1,e_4) ),
inference(resolution,[status(thm)],[c1224,e_3_is_not_e_1]) ).
cnf(c4009,plain,
( product(e_1,e_1,e_2)
| product(e_3,e_1,e_2)
| product(e_3,e_1,e_4)
| ~ product(X702,e_1,e_3)
| equalish(X702,e_3) ),
inference(resolution,[status(thm)],[c3869,product_left_cancellation]) ).
cnf(e_2_is_not_e_1,axiom,
~ equalish(e_2,e_1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_2_is_not_e_1) ).
cnf(e_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(element_2,axiom,
group_element(e_2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',element_2) ).
cnf(c4,plain,
( ~ group_element(X35)
| product(X35,e_2,e_1)
| product(X35,e_2,e_2)
| product(X35,e_2,e_3)
| product(X35,e_2,e_4) ),
inference(resolution,[status(thm)],[product_total_function1,element_2]) ).
cnf(c17,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) ),
inference(resolution,[status(thm)],[c4,element_1]) ).
cnf(c295,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,X352,e_1)
| equalish(X352,e_2) ),
inference(resolution,[status(thm)],[c17,product_right_cancellation]) ).
cnf(qg3,negated_conjecture,
( ~ product(X29,X30,X31)
| ~ product(X30,X31,X28)
| product(X31,X29,X28) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',qg3) ).
cnf(c1206,plain,
( product(e_1,e_1,e_1)
| ~ product(X184,e_1,e_1)
| product(e_1,X184,e_2) ),
inference(resolution,[status(thm)],[c1182,qg3]) ).
cnf(c290,plain,
( product(e_1,e_2,e_2)
| product(e_1,e_2,e_3)
| product(e_1,e_2,e_4)
| ~ product(X347,e_1,e_2)
| product(e_2,X347,e_1) ),
inference(resolution,[status(thm)],[c17,qg3]) ).
cnf(c1197,plain,
( product(e_1,e_1,e_2)
| ~ product(e_1,X177,e_1)
| equalish(X177,e_1) ),
inference(resolution,[status(thm)],[c1182,product_right_cancellation]) ).
cnf(c1229,plain,
( product(e_1,e_1,e_2)
| equalish(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) ),
inference(resolution,[status(thm)],[c1197,c17]) ).
cnf(c5837,plain,
( product(e_1,e_1,e_2)
| product(e_1,e_2,e_2)
| product(e_1,e_2,e_3)
| product(e_1,e_2,e_4) ),
inference(resolution,[status(thm)],[c1229,e_2_is_not_e_1]) ).
cnf(c5931,plain,
( product(e_1,e_2,e_2)
| product(e_1,e_2,e_3)
| product(e_1,e_2,e_4)
| product(e_2,e_1,e_1) ),
inference(resolution,[status(thm)],[c5837,c290]) ).
cnf(c6100,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_1,e_1) ),
inference(resolution,[status(thm)],[c5931,c1206]) ).
cnf(c6369,plain,
( product(e_1,e_2,e_2)
| product(e_1,e_2,e_3)
| product(e_1,e_2,e_4)
| equalish(e_1,e_2) ),
inference(resolution,[status(thm)],[c6100,c295]) ).
cnf(c7804,plain,
( product(e_1,e_2,e_2)
| product(e_1,e_2,e_3)
| product(e_1,e_2,e_4) ),
inference(resolution,[status(thm)],[c6369,e_1_is_not_e_2]) ).
cnf(c7829,plain,
( product(e_1,e_2,e_3)
| product(e_1,e_2,e_4)
| ~ product(X747,e_2,e_2)
| equalish(X747,e_1) ),
inference(resolution,[status(thm)],[c7804,product_left_cancellation]) ).
cnf(product_total_function2,axiom,
( ~ product(X7,X6,X8)
| ~ product(X7,X6,X5)
| equalish(X8,X5) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',product_total_function2) ).
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_4_greater_e_3,axiom,
greater(e_4,e_3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_4_greater_e_3) ).
cnf(c14,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)],[c3,element_2]) ).
cnf(c224,plain,
( product(e_2,e_1,e_1)
| product(e_2,e_1,e_2)
| product(e_2,e_1,e_3)
| ~ next(e_2,X260)
| ~ greater(e_4,X260) ),
inference(resolution,[status(thm)],[c14,no_redundancy]) ).
cnf(c1363,plain,
( product(e_2,e_1,e_1)
| product(e_2,e_1,e_2)
| product(e_2,e_1,e_3)
| ~ next(e_2,e_3) ),
inference(resolution,[status(thm)],[c224,e_4_greater_e_3]) ).
cnf(c1366,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)],[c1363,e_2_then_e_3]) ).
cnf(c1380,plain,
( product(e_2,e_1,e_2)
| product(e_2,e_1,e_3)
| product(e_1,e_1,e_2)
| equalish(e_2,e_1) ),
inference(resolution,[status(thm)],[c1366,c1195]) ).
cnf(c1524,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)],[c1380,e_2_is_not_e_1]) ).
cnf(c1565,plain,
( product(e_2,e_1,e_2)
| product(e_2,e_1,e_3)
| ~ product(e_1,e_1,X299)
| equalish(X299,e_2) ),
inference(resolution,[status(thm)],[c1524,product_total_function2]) ).
cnf(c1209,plain,
( product(e_1,e_1,e_1)
| ~ product(e_1,X182,e_2)
| equalish(X182,e_1) ),
inference(resolution,[status(thm)],[c1182,product_right_cancellation]) ).
cnf(c1397,plain,
( product(e_2,e_1,e_1)
| product(e_2,e_1,e_3)
| product(e_1,e_1,e_1)
| equalish(e_2,e_1) ),
inference(resolution,[status(thm)],[c1366,c1207]) ).
cnf(c1710,plain,
( product(e_2,e_1,e_1)
| product(e_2,e_1,e_3)
| product(e_1,e_1,e_1) ),
inference(resolution,[status(thm)],[c1397,e_2_is_not_e_1]) ).
cnf(c1718,plain,
( product(e_2,e_1,e_3)
| product(e_1,e_1,e_1)
| product(e_1,e_2,e_2) ),
inference(resolution,[status(thm)],[c1710,c1206]) ).
cnf(c1811,plain,
( product(e_2,e_1,e_3)
| product(e_1,e_1,e_1)
| equalish(e_2,e_1) ),
inference(resolution,[status(thm)],[c1718,c1209]) ).
cnf(c1872,plain,
( product(e_2,e_1,e_3)
| product(e_1,e_1,e_1) ),
inference(resolution,[status(thm)],[c1811,e_2_is_not_e_1]) ).
cnf(c1904,plain,
( product(e_2,e_1,e_3)
| product(e_2,e_1,e_2)
| equalish(e_1,e_2) ),
inference(resolution,[status(thm)],[c1872,c1565]) ).
cnf(c2024,plain,
( product(e_2,e_1,e_3)
| product(e_2,e_1,e_2) ),
inference(resolution,[status(thm)],[c1904,e_1_is_not_e_2]) ).
cnf(c7810,plain,
( product(e_1,e_2,e_3)
| product(e_1,e_2,e_4)
| ~ product(X786,e_1,e_2)
| product(e_2,X786,e_2) ),
inference(resolution,[status(thm)],[c7804,qg3]) ).
cnf(c13224,plain,
( product(e_1,e_2,e_3)
| product(e_1,e_2,e_4)
| product(e_2,e_2,e_2)
| product(e_2,e_1,e_3) ),
inference(resolution,[status(thm)],[c7810,c2024]) ).
cnf(c15727,plain,
( product(e_1,e_2,e_3)
| product(e_1,e_2,e_4)
| product(e_2,e_1,e_3)
| equalish(e_2,e_1) ),
inference(resolution,[status(thm)],[c13224,c7829]) ).
cnf(c16135,plain,
( product(e_1,e_2,e_3)
| product(e_1,e_2,e_4)
| product(e_2,e_1,e_3) ),
inference(resolution,[status(thm)],[c15727,e_2_is_not_e_1]) ).
cnf(c16157,plain,
( product(e_1,e_2,e_4)
| product(e_2,e_1,e_3)
| ~ product(X796,e_2,e_3)
| equalish(X796,e_1) ),
inference(resolution,[status(thm)],[c16135,product_left_cancellation]) ).
cnf(c16138,plain,
( product(e_1,e_2,e_4)
| product(e_2,e_1,e_3)
| ~ product(X803,e_1,e_2)
| product(e_2,X803,e_3) ),
inference(resolution,[status(thm)],[c16135,qg3]) ).
cnf(c17923,plain,
( product(e_1,e_2,e_4)
| product(e_2,e_1,e_3)
| product(e_2,e_2,e_3) ),
inference(resolution,[status(thm)],[c16138,c2024]) ).
cnf(c18000,plain,
( product(e_1,e_2,e_4)
| product(e_2,e_1,e_3)
| equalish(e_2,e_1) ),
inference(resolution,[status(thm)],[c17923,c16157]) ).
cnf(c18377,plain,
( product(e_1,e_2,e_4)
| product(e_2,e_1,e_3) ),
inference(resolution,[status(thm)],[c18000,e_2_is_not_e_1]) ).
cnf(c18403,plain,
( product(e_2,e_1,e_3)
| ~ product(X807,e_2,e_4)
| equalish(X807,e_1) ),
inference(resolution,[status(thm)],[c18377,product_left_cancellation]) ).
cnf(c18380,plain,
( product(e_2,e_1,e_3)
| ~ product(X811,e_1,e_2)
| product(e_2,X811,e_4) ),
inference(resolution,[status(thm)],[c18377,qg3]) ).
cnf(c19583,plain,
( product(e_2,e_1,e_3)
| product(e_2,e_2,e_4) ),
inference(resolution,[status(thm)],[c18380,c2024]) ).
cnf(c19636,plain,
( product(e_2,e_1,e_3)
| equalish(e_2,e_1) ),
inference(resolution,[status(thm)],[c19583,c18403]) ).
cnf(c19966,plain,
product(e_2,e_1,e_3),
inference(resolution,[status(thm)],[c19636,e_2_is_not_e_1]) ).
cnf(c19987,plain,
( product(e_1,e_1,e_2)
| product(e_3,e_1,e_2)
| product(e_3,e_1,e_4)
| equalish(e_2,e_3) ),
inference(resolution,[status(thm)],[c19966,c4009]) ).
cnf(c28032,plain,
( product(e_1,e_1,e_2)
| product(e_3,e_1,e_2)
| product(e_3,e_1,e_4) ),
inference(resolution,[status(thm)],[c19987,e_2_is_not_e_3]) ).
cnf(c28123,plain,
( product(e_1,e_1,e_2)
| product(e_3,e_1,e_2)
| ~ product(X915,e_1,e_4)
| equalish(X915,e_3) ),
inference(resolution,[status(thm)],[c28032,product_left_cancellation]) ).
cnf(c19972,plain,
( ~ product(e_2,X813,e_3)
| equalish(X813,e_1) ),
inference(resolution,[status(thm)],[c19966,product_right_cancellation]) ).
cnf(c19975,plain,
( ~ product(X816,e_2,e_1)
| product(e_1,X816,e_3) ),
inference(resolution,[status(thm)],[c19966,qg3]) ).
cnf(c10,plain,
( product(e_2,e_2,e_1)
| product(e_2,e_2,e_2)
| product(e_2,e_2,e_3)
| product(e_2,e_2,e_4) ),
inference(resolution,[status(thm)],[c2,element_2]) ).
cnf(c81,plain,
( product(e_2,e_2,e_1)
| product(e_2,e_2,e_2)
| product(e_2,e_2,e_4)
| ~ product(e_2,X121,e_3)
| equalish(X121,e_2) ),
inference(resolution,[status(thm)],[c10,product_right_cancellation]) ).
cnf(c19594,plain,
( product(e_2,e_2,e_4)
| product(e_2,e_2,e_1)
| product(e_2,e_2,e_2)
| equalish(e_1,e_2) ),
inference(resolution,[status(thm)],[c19583,c81]) ).
cnf(c24050,plain,
( product(e_2,e_2,e_4)
| product(e_2,e_2,e_1)
| product(e_2,e_2,e_2) ),
inference(resolution,[status(thm)],[c19594,e_1_is_not_e_2]) ).
cnf(c24081,plain,
( product(e_2,e_2,e_4)
| product(e_2,e_2,e_2)
| product(e_1,e_2,e_3) ),
inference(resolution,[status(thm)],[c24050,c19975]) ).
cnf(c24430,plain,
( product(e_2,e_2,e_2)
| product(e_1,e_2,e_3)
| ~ product(e_2,X865,e_4)
| equalish(X865,e_2) ),
inference(resolution,[status(thm)],[c24081,product_right_cancellation]) ).
cnf(c24432,plain,
( product(e_2,e_2,e_2)
| product(e_1,e_2,e_3)
| ~ product(X943,e_2,e_2)
| product(e_2,X943,e_4) ),
inference(resolution,[status(thm)],[c24081,qg3]) ).
cnf(c7884,plain,
( product(e_1,e_2,e_2)
| product(e_1,e_2,e_3)
| ~ product(X753,e_2,e_4)
| equalish(X753,e_1) ),
inference(resolution,[status(thm)],[c7804,product_left_cancellation]) ).
cnf(c24444,plain,
( product(e_2,e_2,e_2)
| product(e_1,e_2,e_3)
| product(e_1,e_2,e_2)
| equalish(e_2,e_1) ),
inference(resolution,[status(thm)],[c24081,c7884]) ).
cnf(c30150,plain,
( product(e_2,e_2,e_2)
| product(e_1,e_2,e_3)
| product(e_1,e_2,e_2) ),
inference(resolution,[status(thm)],[c24444,e_2_is_not_e_1]) ).
cnf(c30213,plain,
( product(e_2,e_2,e_2)
| product(e_1,e_2,e_3)
| product(e_2,e_1,e_4) ),
inference(resolution,[status(thm)],[c30150,c24432]) ).
cnf(c30291,plain,
( product(e_2,e_2,e_2)
| product(e_1,e_2,e_3)
| equalish(e_1,e_2) ),
inference(resolution,[status(thm)],[c30213,c24430]) ).
cnf(c30687,plain,
( product(e_2,e_2,e_2)
| product(e_1,e_2,e_3) ),
inference(resolution,[status(thm)],[c30291,e_1_is_not_e_2]) ).
cnf(c30695,plain,
( product(e_1,e_2,e_3)
| product(e_1,e_2,e_4)
| equalish(e_2,e_1) ),
inference(resolution,[status(thm)],[c30687,c7829]) ).
cnf(c31356,plain,
( product(e_1,e_2,e_3)
| product(e_1,e_2,e_4) ),
inference(resolution,[status(thm)],[c30695,e_2_is_not_e_1]) ).
cnf(c31362,plain,
( product(e_1,e_2,e_4)
| ~ product(X958,e_1,e_2)
| product(e_2,X958,e_3) ),
inference(resolution,[status(thm)],[c31356,qg3]) ).
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(element_4,axiom,
group_element(e_4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',element_4) ).
cnf(c16,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)],[c3,element_4]) ).
cnf(c1226,plain,
( product(e_1,e_1,e_2)
| equalish(e_4,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)],[c1195,c16]) ).
cnf(c4668,plain,
( product(e_1,e_1,e_2)
| 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)],[c1226,e_4_is_not_e_1]) ).
cnf(c4818,plain,
( product(e_1,e_1,e_2)
| product(e_4,e_1,e_2)
| product(e_4,e_1,e_4)
| ~ product(X718,e_1,e_3)
| equalish(X718,e_4) ),
inference(resolution,[status(thm)],[c4668,product_left_cancellation]) ).
cnf(c19971,plain,
( product(e_1,e_1,e_2)
| product(e_4,e_1,e_2)
| product(e_4,e_1,e_4)
| equalish(e_2,e_4) ),
inference(resolution,[status(thm)],[c19966,c4818]) ).
cnf(c26599,plain,
( product(e_1,e_1,e_2)
| product(e_4,e_1,e_2)
| product(e_4,e_1,e_4) ),
inference(resolution,[status(thm)],[c19971,e_2_is_not_e_4]) ).
cnf(c26606,plain,
( product(e_4,e_1,e_2)
| product(e_4,e_1,e_4)
| ~ product(e_1,X877,e_2)
| equalish(X877,e_1) ),
inference(resolution,[status(thm)],[c26599,product_right_cancellation]) ).
cnf(c277,plain,
( product(e_4,e_1,e_1)
| product(e_4,e_1,e_2)
| product(e_4,e_1,e_4)
| ~ product(X329,e_1,e_3)
| equalish(X329,e_4) ),
inference(resolution,[status(thm)],[c16,product_left_cancellation]) ).
cnf(c19988,plain,
( product(e_4,e_1,e_1)
| product(e_4,e_1,e_2)
| product(e_4,e_1,e_4)
| equalish(e_2,e_4) ),
inference(resolution,[status(thm)],[c19966,c277]) ).
cnf(c29112,plain,
( product(e_4,e_1,e_1)
| product(e_4,e_1,e_2)
| product(e_4,e_1,e_4) ),
inference(resolution,[status(thm)],[c19988,e_2_is_not_e_4]) ).
cnf(c26611,plain,
( product(e_4,e_1,e_2)
| product(e_4,e_1,e_4)
| ~ product(X997,e_1,e_1)
| product(e_1,X997,e_2) ),
inference(resolution,[status(thm)],[c26599,qg3]) ).
cnf(c32799,plain,
( product(e_4,e_1,e_2)
| product(e_4,e_1,e_4)
| product(e_1,e_4,e_2) ),
inference(resolution,[status(thm)],[c26611,c29112]) ).
cnf(c32894,plain,
( product(e_4,e_1,e_2)
| product(e_4,e_1,e_4)
| equalish(e_4,e_1) ),
inference(resolution,[status(thm)],[c32799,c26606]) ).
cnf(c32963,plain,
( product(e_4,e_1,e_2)
| product(e_4,e_1,e_4) ),
inference(resolution,[status(thm)],[c32894,e_4_is_not_e_1]) ).
cnf(c32981,plain,
( product(e_4,e_1,e_4)
| product(e_1,e_2,e_4)
| product(e_2,e_4,e_3) ),
inference(resolution,[status(thm)],[c32963,c31362]) ).
cnf(c34214,plain,
( product(e_4,e_1,e_4)
| product(e_1,e_2,e_4)
| equalish(e_4,e_1) ),
inference(resolution,[status(thm)],[c32981,c19972]) ).
cnf(c34266,plain,
( product(e_4,e_1,e_4)
| product(e_1,e_2,e_4) ),
inference(resolution,[status(thm)],[c34214,e_4_is_not_e_1]) ).
cnf(c34295,plain,
( product(e_4,e_1,e_4)
| ~ product(X1028,e_1,e_2)
| product(e_2,X1028,e_4) ),
inference(resolution,[status(thm)],[c34266,qg3]) ).
cnf(c34556,plain,
( product(e_4,e_1,e_4)
| product(e_2,e_4,e_4) ),
inference(resolution,[status(thm)],[c34295,c32963]) ).
cnf(c34597,plain,
( product(e_4,e_1,e_4)
| ~ product(X1044,e_2,e_4)
| product(e_4,X1044,e_4) ),
inference(resolution,[status(thm)],[c34556,qg3]) ).
cnf(c36110,plain,
product(e_4,e_1,e_4),
inference(resolution,[status(thm)],[c34597,c34266]) ).
cnf(c36139,plain,
( product(e_1,e_1,e_2)
| product(e_3,e_1,e_2)
| equalish(e_4,e_3) ),
inference(resolution,[status(thm)],[c36110,c28123]) ).
cnf(c36366,plain,
( product(e_1,e_1,e_2)
| product(e_3,e_1,e_2) ),
inference(resolution,[status(thm)],[c36139,e_4_is_not_e_3]) ).
cnf(c36371,plain,
( product(e_3,e_1,e_2)
| ~ product(e_1,X1054,e_2)
| equalish(X1054,e_1) ),
inference(resolution,[status(thm)],[c36366,product_right_cancellation]) ).
cnf(c245,plain,
( product(e_3,e_1,e_1)
| product(e_3,e_1,e_2)
| product(e_3,e_1,e_4)
| ~ product(X287,e_1,e_3)
| equalish(X287,e_3) ),
inference(resolution,[status(thm)],[c15,product_left_cancellation]) ).
cnf(c19989,plain,
( product(e_3,e_1,e_1)
| product(e_3,e_1,e_2)
| product(e_3,e_1,e_4)
| equalish(e_2,e_3) ),
inference(resolution,[status(thm)],[c19966,c245]) ).
cnf(c29579,plain,
( product(e_3,e_1,e_1)
| product(e_3,e_1,e_2)
| product(e_3,e_1,e_4) ),
inference(resolution,[status(thm)],[c19989,e_2_is_not_e_3]) ).
cnf(c29658,plain,
( product(e_3,e_1,e_1)
| product(e_3,e_1,e_2)
| ~ product(X939,e_1,e_4)
| equalish(X939,e_3) ),
inference(resolution,[status(thm)],[c29579,product_left_cancellation]) ).
cnf(c36154,plain,
( product(e_3,e_1,e_1)
| product(e_3,e_1,e_2)
| equalish(e_4,e_3) ),
inference(resolution,[status(thm)],[c36110,c29658]) ).
cnf(c36703,plain,
( product(e_3,e_1,e_1)
| product(e_3,e_1,e_2) ),
inference(resolution,[status(thm)],[c36154,e_4_is_not_e_3]) ).
cnf(c36377,plain,
( product(e_3,e_1,e_2)
| ~ product(X1068,e_1,e_1)
| product(e_1,X1068,e_2) ),
inference(resolution,[status(thm)],[c36366,qg3]) ).
cnf(c37035,plain,
( product(e_3,e_1,e_2)
| product(e_1,e_3,e_2) ),
inference(resolution,[status(thm)],[c36377,c36703]) ).
cnf(c37080,plain,
( product(e_3,e_1,e_2)
| equalish(e_3,e_1) ),
inference(resolution,[status(thm)],[c37035,c36371]) ).
cnf(c37114,plain,
( equalish(e_3,e_1)
| product(e_1,e_1,e_1) ),
inference(resolution,[status(thm)],[c37080,c1207]) ).
cnf(c37229,plain,
product(e_1,e_1,e_1),
inference(resolution,[status(thm)],[c37114,e_3_is_not_e_1]) ).
cnf(c37268,plain,
( ~ product(X1076,e_1,e_1)
| equalish(X1076,e_1) ),
inference(resolution,[status(thm)],[c37229,product_left_cancellation]) ).
cnf(c37123,plain,
product(e_3,e_1,e_2),
inference(resolution,[status(thm)],[c37080,e_3_is_not_e_1]) ).
cnf(c37137,plain,
( product(e_1,e_2,e_4)
| product(e_2,e_3,e_3) ),
inference(resolution,[status(thm)],[c37123,c31362]) ).
cnf(c37440,plain,
( product(e_1,e_2,e_4)
| equalish(e_3,e_1) ),
inference(resolution,[status(thm)],[c37137,c19972]) ).
cnf(c37466,plain,
product(e_1,e_2,e_4),
inference(resolution,[status(thm)],[c37440,e_3_is_not_e_1]) ).
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(c30726,plain,
( product(e_2,e_2,e_2)
| ~ product(e_1,e_2,X948)
| equalish(X948,e_3) ),
inference(resolution,[status(thm)],[c30687,product_total_function2]) ).
cnf(c37483,plain,
( product(e_2,e_2,e_2)
| equalish(e_4,e_3) ),
inference(resolution,[status(thm)],[c37466,c30726]) ).
cnf(c37662,plain,
product(e_2,e_2,e_2),
inference(resolution,[status(thm)],[c37483,e_4_is_not_e_3]) ).
cnf(c37664,plain,
( ~ product(e_2,X1087,e_2)
| equalish(X1087,e_2) ),
inference(resolution,[status(thm)],[c37662,product_right_cancellation]) ).
cnf(e_3_is_not_e_4,axiom,
~ equalish(e_3,e_4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_3_is_not_e_4) ).
cnf(e_1_is_not_e_4,axiom,
~ equalish(e_1,e_4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_1_is_not_e_4) ).
cnf(c6,plain,
( ~ group_element(X37)
| product(X37,e_4,e_1)
| product(X37,e_4,e_2)
| product(X37,e_4,e_3)
| product(X37,e_4,e_4) ),
inference(resolution,[status(thm)],[product_total_function1,element_4]) ).
cnf(c26,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)],[c6,element_2]) ).
cnf(c609,plain,
( product(e_2,e_4,e_1)
| product(e_2,e_4,e_2)
| product(e_2,e_4,e_4)
| ~ product(e_2,X642,e_3)
| equalish(X642,e_4) ),
inference(resolution,[status(thm)],[c26,product_right_cancellation]) ).
cnf(c19978,plain,
( product(e_2,e_4,e_1)
| product(e_2,e_4,e_2)
| product(e_2,e_4,e_4)
| equalish(e_1,e_4) ),
inference(resolution,[status(thm)],[c19966,c609]) ).
cnf(c27030,plain,
( product(e_2,e_4,e_1)
| product(e_2,e_4,e_2)
| product(e_2,e_4,e_4) ),
inference(resolution,[status(thm)],[c19978,e_1_is_not_e_4]) ).
cnf(c27079,plain,
( product(e_2,e_4,e_1)
| product(e_2,e_4,e_2)
| ~ product(e_2,X892,e_4)
| equalish(X892,e_4) ),
inference(resolution,[status(thm)],[c27030,product_right_cancellation]) ).
cnf(c37471,plain,
( ~ product(X1083,e_1,e_2)
| product(e_2,X1083,e_4) ),
inference(resolution,[status(thm)],[c37466,qg3]) ).
cnf(c37543,plain,
product(e_2,e_3,e_4),
inference(resolution,[status(thm)],[c37471,c37123]) ).
cnf(c37554,plain,
( product(e_2,e_4,e_1)
| product(e_2,e_4,e_2)
| equalish(e_3,e_4) ),
inference(resolution,[status(thm)],[c37543,c27079]) ).
cnf(c37791,plain,
( product(e_2,e_4,e_1)
| product(e_2,e_4,e_2) ),
inference(resolution,[status(thm)],[c37554,e_3_is_not_e_4]) ).
cnf(c37812,plain,
( product(e_2,e_4,e_1)
| equalish(e_4,e_2) ),
inference(resolution,[status(thm)],[c37791,c37664]) ).
cnf(c37841,plain,
product(e_2,e_4,e_1),
inference(resolution,[status(thm)],[c37812,e_4_is_not_e_2]) ).
cnf(c37847,plain,
( ~ product(X1140,e_2,e_4)
| product(e_4,X1140,e_1) ),
inference(resolution,[status(thm)],[c37841,qg3]) ).
cnf(c37912,plain,
product(e_4,e_1,e_1),
inference(resolution,[status(thm)],[c37847,c37466]) ).
cnf(c37933,plain,
equalish(e_4,e_1),
inference(resolution,[status(thm)],[c37912,c37268]) ).
cnf(c37943,plain,
$false,
inference(resolution,[status(thm)],[c37933,e_4_is_not_e_1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : GRP129-2.004 : TPTP v8.1.2. Released v1.2.0.
% 0.11/0.12 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.12/0.33 % Computer : n027.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Thu May 9 04:47:23 EDT 2024
% 0.12/0.33 % CPUTime :
% 50.59/50.83 % Version: 1.5
% 50.59/50.83 % SZS status Unsatisfiable
% 50.59/50.83 % SZS output start CNFRefutation
% See solution above
% 50.59/50.84
% 50.59/50.84 % Initial clauses : 31
% 50.59/50.84 % Processed clauses : 1058
% 50.59/50.84 % Factors computed : 5
% 50.59/50.84 % Resolvents computed: 37939
% 50.59/50.84 % Tautologies deleted: 1
% 50.59/50.84 % Forward subsumed : 3215
% 50.59/50.84 % Backward subsumed : 754
% 50.59/50.84 % -------- CPU Time ---------
% 50.59/50.84 % User time : 50.333 s
% 50.59/50.84 % System time : 0.136 s
% 50.59/50.84 % Total time : 50.469 s
%------------------------------------------------------------------------------