%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GRP134-1.003 : TPTP v8.1.2. Released v1.2.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n025.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:15 EDT 2024
% Result : Unsatisfiable 203.77s 203.98s
% Output : Refutation 203.77s
% Verified :
% SZS Type : Refutation
% Derivation depth : 33
% Number of leaves : 14
% Syntax : Number of clauses : 140 ( 16 unt; 114 nHn; 140 RR)
% Number of literals : 417 ( 0 equ; 58 neg)
% Maximal clause size : 5 ( 2 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 4 ( 3 usr; 1 prp; 0-3 aty)
% Number of functors : 3 ( 3 usr; 3 con; 0-0 aty)
% Number of variables : 61 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
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(product_right_cancellation,axiom,
( ~ product(X13,X12,X11)
| ~ product(X13,X14,X11)
| equalish(X12,X14) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',product_right_cancellation) ).
cnf(qg4,negated_conjecture,
( ~ product(X27,X26,X25)
| ~ product(X26,X27,X28)
| product(X25,X28,X26) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',qg4) ).
cnf(c7,plain,
( ~ product(X30,X30,X31)
| product(X31,X31,X30) ),
inference(factor,[status(thm)],[qg4]) ).
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(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(product_left_cancellation,axiom,
( ~ product(X19,X18,X20)
| ~ product(X21,X18,X20)
| equalish(X19,X21) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',product_left_cancellation) ).
cnf(element_3,axiom,
group_element(e_3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',element_3) ).
cnf(product_total_function1,axiom,
( ~ group_element(X10)
| ~ group_element(X9)
| product(X10,X9,e_1)
| product(X10,X9,e_2)
| product(X10,X9,e_3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',product_total_function1) ).
cnf(c1,plain,
( ~ group_element(X29)
| product(X29,X29,e_1)
| product(X29,X29,e_2)
| product(X29,X29,e_3) ),
inference(factor,[status(thm)],[product_total_function1]) ).
cnf(c10,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)],[c1,element_3]) ).
cnf(c95,plain,
( product(e_3,e_3,e_2)
| product(e_3,e_3,e_3)
| product(e_1,e_1,e_3) ),
inference(resolution,[status(thm)],[c10,c7]) ).
cnf(c623,plain,
( product(e_3,e_3,e_2)
| product(e_3,e_3,e_3)
| ~ product(X251,e_1,e_3)
| equalish(X251,e_1) ),
inference(resolution,[status(thm)],[c95,product_left_cancellation]) ).
cnf(element_1,axiom,
group_element(e_1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',element_1) ).
cnf(c2,plain,
( ~ group_element(X32)
| product(X32,e_1,e_1)
| product(X32,e_1,e_2)
| product(X32,e_1,e_3) ),
inference(resolution,[status(thm)],[product_total_function1,element_1]) ).
cnf(c13,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)],[c2,element_3]) ).
cnf(c157,plain,
( product(e_3,e_1,e_2)
| product(e_3,e_1,e_3)
| ~ product(e_3,X140,e_1)
| equalish(X140,e_1) ),
inference(resolution,[status(thm)],[c13,product_right_cancellation]) ).
cnf(c950,plain,
( product(e_3,e_1,e_2)
| product(e_3,e_1,e_3)
| equalish(e_3,e_1)
| product(e_3,e_3,e_2)
| product(e_3,e_3,e_3) ),
inference(resolution,[status(thm)],[c157,c10]) ).
cnf(c19076,plain,
( product(e_3,e_1,e_2)
| equalish(e_3,e_1)
| product(e_3,e_3,e_2)
| product(e_3,e_3,e_3) ),
inference(resolution,[status(thm)],[c950,c623]) ).
cnf(c60964,plain,
( product(e_3,e_1,e_2)
| product(e_3,e_3,e_2)
| product(e_3,e_3,e_3) ),
inference(resolution,[status(thm)],[c19076,e_3_is_not_e_1]) ).
cnf(c61326,plain,
( product(e_3,e_1,e_2)
| product(e_3,e_3,e_2)
| ~ product(e_3,X566,e_3)
| equalish(X566,e_3) ),
inference(resolution,[status(thm)],[c60964,product_right_cancellation]) ).
cnf(c159,plain,
( product(e_3,e_1,e_2)
| product(e_3,e_1,e_3)
| ~ product(X142,e_1,e_1)
| equalish(X142,e_3) ),
inference(resolution,[status(thm)],[c13,product_left_cancellation]) ).
cnf(product_total_function2,axiom,
( ~ product(X4,X2,X3)
| ~ product(X4,X2,X5)
| equalish(X3,X5) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',product_total_function2) ).
cnf(c8,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)],[c1,element_1]) ).
cnf(c31,plain,
( product(e_1,e_1,e_1)
| product(e_1,e_1,e_3)
| product(e_2,e_2,e_1) ),
inference(resolution,[status(thm)],[c8,c7]) ).
cnf(c394,plain,
( product(e_1,e_1,e_1)
| product(e_2,e_2,e_1)
| ~ product(X212,e_1,e_3)
| equalish(X212,e_1) ),
inference(resolution,[status(thm)],[c31,product_left_cancellation]) ).
cnf(c386,plain,
( product(e_1,e_1,e_1)
| product(e_2,e_2,e_1)
| product(e_3,e_3,e_1) ),
inference(resolution,[status(thm)],[c31,c7]) ).
cnf(c949,plain,
( product(e_3,e_1,e_2)
| product(e_3,e_1,e_3)
| equalish(e_3,e_1)
| product(e_1,e_1,e_1)
| product(e_2,e_2,e_1) ),
inference(resolution,[status(thm)],[c157,c386]) ).
cnf(c18780,plain,
( product(e_3,e_1,e_2)
| equalish(e_3,e_1)
| product(e_1,e_1,e_1)
| product(e_2,e_2,e_1) ),
inference(resolution,[status(thm)],[c949,c394]) ).
cnf(c55465,plain,
( product(e_3,e_1,e_2)
| product(e_1,e_1,e_1)
| product(e_2,e_2,e_1) ),
inference(resolution,[status(thm)],[c18780,e_3_is_not_e_1]) ).
cnf(c55824,plain,
( product(e_3,e_1,e_2)
| product(e_1,e_1,e_1)
| product(e_1,e_1,e_2) ),
inference(resolution,[status(thm)],[c55465,c7]) ).
cnf(c56453,plain,
( product(e_3,e_1,e_2)
| product(e_1,e_1,e_1)
| ~ product(e_1,e_1,X555)
| equalish(X555,e_2) ),
inference(resolution,[status(thm)],[c55824,product_total_function2]) ).
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(c605,plain,
( product(e_3,e_3,e_3)
| product(e_1,e_1,e_3)
| product(e_2,e_2,e_3) ),
inference(resolution,[status(thm)],[c95,c7]) ).
cnf(c397,plain,
( product(e_1,e_1,e_1)
| product(e_1,e_1,e_3)
| ~ product(e_2,e_2,X213)
| equalish(X213,e_1) ),
inference(resolution,[status(thm)],[c31,product_total_function2]) ).
cnf(c1264,plain,
( product(e_1,e_1,e_1)
| product(e_1,e_1,e_3)
| equalish(e_3,e_1)
| product(e_3,e_3,e_3) ),
inference(resolution,[status(thm)],[c397,c605]) ).
cnf(c4082,plain,
( product(e_1,e_1,e_1)
| product(e_1,e_1,e_3)
| product(e_3,e_3,e_3) ),
inference(resolution,[status(thm)],[c1264,e_3_is_not_e_1]) ).
cnf(c4392,plain,
( product(e_1,e_1,e_1)
| product(e_1,e_1,e_3)
| ~ product(e_3,e_3,X323)
| equalish(X323,e_3) ),
inference(resolution,[status(thm)],[c4082,product_total_function2]) ).
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(c35,plain,
( product(e_1,e_1,e_1)
| product(e_1,e_1,e_3)
| ~ product(X54,e_1,e_2)
| equalish(X54,e_1) ),
inference(resolution,[status(thm)],[c8,product_left_cancellation]) ).
cnf(element_2,axiom,
group_element(e_2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',element_2) ).
cnf(c12,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)],[c2,element_2]) ).
cnf(c120,plain,
( product(e_2,e_1,e_2)
| product(e_2,e_1,e_3)
| ~ product(e_2,X103,e_1)
| equalish(X103,e_1) ),
inference(resolution,[status(thm)],[c12,product_right_cancellation]) ).
cnf(c897,plain,
( product(e_2,e_1,e_2)
| product(e_2,e_1,e_3)
| equalish(e_2,e_1)
| product(e_1,e_1,e_1)
| product(e_1,e_1,e_3) ),
inference(resolution,[status(thm)],[c120,c31]) ).
cnf(c11939,plain,
( product(e_2,e_1,e_3)
| equalish(e_2,e_1)
| product(e_1,e_1,e_1)
| product(e_1,e_1,e_3) ),
inference(resolution,[status(thm)],[c897,c35]) ).
cnf(c17304,plain,
( product(e_2,e_1,e_3)
| product(e_1,e_1,e_1)
| product(e_1,e_1,e_3) ),
inference(resolution,[status(thm)],[c11939,e_2_is_not_e_1]) ).
cnf(c17644,plain,
( product(e_1,e_1,e_1)
| product(e_1,e_1,e_3)
| ~ product(e_1,e_2,X489)
| product(X489,e_3,e_2) ),
inference(resolution,[status(thm)],[c17304,qg4]) ).
cnf(c33,plain,
( product(e_1,e_1,e_1)
| product(e_1,e_1,e_3)
| ~ product(e_1,X53,e_2)
| equalish(X53,e_1) ),
inference(resolution,[status(thm)],[c8,product_right_cancellation]) ).
cnf(c3,plain,
( ~ group_element(X33)
| product(X33,e_2,e_1)
| product(X33,e_2,e_2)
| product(X33,e_2,e_3) ),
inference(resolution,[status(thm)],[product_total_function1,element_2]) ).
cnf(c14,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)],[c3,element_1]) ).
cnf(c180,plain,
( product(e_1,e_2,e_2)
| product(e_1,e_2,e_3)
| ~ product(X154,e_2,e_1)
| equalish(X154,e_1) ),
inference(resolution,[status(thm)],[c14,product_left_cancellation]) ).
cnf(c1011,plain,
( product(e_1,e_2,e_2)
| product(e_1,e_2,e_3)
| equalish(e_2,e_1)
| product(e_1,e_1,e_1)
| product(e_1,e_1,e_3) ),
inference(resolution,[status(thm)],[c180,c31]) ).
cnf(c31942,plain,
( product(e_1,e_2,e_3)
| equalish(e_2,e_1)
| product(e_1,e_1,e_1)
| product(e_1,e_1,e_3) ),
inference(resolution,[status(thm)],[c1011,c33]) ).
cnf(c109801,plain,
( product(e_1,e_2,e_3)
| product(e_1,e_1,e_1)
| product(e_1,e_1,e_3) ),
inference(resolution,[status(thm)],[c31942,e_2_is_not_e_1]) ).
cnf(c110061,plain,
( product(e_1,e_1,e_1)
| product(e_1,e_1,e_3)
| product(e_3,e_3,e_2) ),
inference(resolution,[status(thm)],[c109801,c17644]) ).
cnf(c110746,plain,
( product(e_1,e_1,e_1)
| product(e_1,e_1,e_3)
| equalish(e_2,e_3) ),
inference(resolution,[status(thm)],[c110061,c4392]) ).
cnf(c111154,plain,
( product(e_1,e_1,e_1)
| product(e_1,e_1,e_3) ),
inference(resolution,[status(thm)],[c110746,e_2_is_not_e_3]) ).
cnf(c111282,plain,
( product(e_1,e_1,e_1)
| product(e_3,e_1,e_2)
| equalish(e_3,e_2) ),
inference(resolution,[status(thm)],[c111154,c56453]) ).
cnf(c114475,plain,
( product(e_1,e_1,e_1)
| product(e_3,e_1,e_2) ),
inference(resolution,[status(thm)],[c111282,e_3_is_not_e_2]) ).
cnf(c114483,plain,
( product(e_3,e_1,e_2)
| product(e_3,e_1,e_3)
| equalish(e_1,e_3) ),
inference(resolution,[status(thm)],[c114475,c159]) ).
cnf(c120141,plain,
( product(e_3,e_1,e_2)
| equalish(e_1,e_3)
| product(e_3,e_3,e_2) ),
inference(resolution,[status(thm)],[c114483,c61326]) ).
cnf(c128318,plain,
( product(e_3,e_1,e_2)
| product(e_3,e_3,e_2) ),
inference(resolution,[status(thm)],[c120141,e_1_is_not_e_3]) ).
cnf(c128470,plain,
( product(e_3,e_1,e_2)
| product(e_2,e_2,e_3) ),
inference(resolution,[status(thm)],[c128318,c7]) ).
cnf(c128799,plain,
( product(e_2,e_2,e_3)
| ~ product(e_1,e_3,X851)
| product(X851,e_2,e_3) ),
inference(resolution,[status(thm)],[c128470,qg4]) ).
cnf(c4,plain,
( ~ group_element(X34)
| product(X34,e_3,e_1)
| product(X34,e_3,e_2)
| product(X34,e_3,e_3) ),
inference(resolution,[status(thm)],[product_total_function1,element_3]) ).
cnf(c17,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)],[c4,element_1]) ).
cnf(c260,plain,
( product(e_1,e_3,e_2)
| product(e_1,e_3,e_3)
| ~ product(e_1,X180,e_1)
| equalish(X180,e_3) ),
inference(resolution,[status(thm)],[c17,product_right_cancellation]) ).
cnf(c114600,plain,
( product(e_1,e_1,e_1)
| ~ product(X751,e_1,e_2)
| equalish(X751,e_3) ),
inference(resolution,[status(thm)],[c114475,product_left_cancellation]) ).
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(c9,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)],[c1,element_2]) ).
cnf(c47,plain,
( product(e_2,e_2,e_2)
| product(e_2,e_2,e_3)
| product(e_1,e_1,e_2) ),
inference(resolution,[status(thm)],[c9,c7]) ).
cnf(c493,plain,
( product(e_2,e_2,e_2)
| product(e_1,e_1,e_2)
| product(e_3,e_3,e_2) ),
inference(resolution,[status(thm)],[c47,c7]) ).
cnf(c39,plain,
( product(e_1,e_1,e_1)
| product(e_1,e_1,e_2)
| product(e_3,e_3,e_1) ),
inference(resolution,[status(thm)],[c8,c7]) ).
cnf(c453,plain,
( product(e_1,e_1,e_1)
| product(e_1,e_1,e_2)
| ~ product(e_3,e_3,X222)
| equalish(X222,e_1) ),
inference(resolution,[status(thm)],[c39,product_total_function2]) ).
cnf(c1346,plain,
( product(e_1,e_1,e_1)
| product(e_1,e_1,e_2)
| equalish(e_2,e_1)
| product(e_2,e_2,e_2) ),
inference(resolution,[status(thm)],[c453,c493]) ).
cnf(c5818,plain,
( product(e_1,e_1,e_1)
| product(e_1,e_1,e_2)
| product(e_2,e_2,e_2) ),
inference(resolution,[status(thm)],[c1346,e_2_is_not_e_1]) ).
cnf(c5990,plain,
( product(e_1,e_1,e_1)
| product(e_1,e_1,e_2)
| ~ product(e_2,X340,e_2)
| equalish(X340,e_2) ),
inference(resolution,[status(thm)],[c5818,product_right_cancellation]) ).
cnf(c136,plain,
( product(e_2,e_1,e_1)
| product(e_2,e_1,e_2)
| ~ product(X136,e_1,e_3)
| equalish(X136,e_2) ),
inference(resolution,[status(thm)],[c12,product_left_cancellation]) ).
cnf(c942,plain,
( product(e_2,e_1,e_1)
| product(e_2,e_1,e_2)
| equalish(e_1,e_2)
| product(e_1,e_1,e_1)
| product(e_1,e_1,e_2) ),
inference(resolution,[status(thm)],[c136,c8]) ).
cnf(c17950,plain,
( product(e_2,e_1,e_1)
| equalish(e_1,e_2)
| product(e_1,e_1,e_1)
| product(e_1,e_1,e_2) ),
inference(resolution,[status(thm)],[c942,c5990]) ).
cnf(c48451,plain,
( product(e_2,e_1,e_1)
| product(e_1,e_1,e_1)
| product(e_1,e_1,e_2) ),
inference(resolution,[status(thm)],[c17950,e_1_is_not_e_2]) ).
cnf(c48769,plain,
( product(e_2,e_1,e_1)
| product(e_1,e_1,e_1)
| ~ product(e_1,e_1,X525)
| equalish(X525,e_2) ),
inference(resolution,[status(thm)],[c48451,product_total_function2]) ).
cnf(c111321,plain,
( product(e_1,e_1,e_1)
| product(e_2,e_1,e_1)
| equalish(e_3,e_2) ),
inference(resolution,[status(thm)],[c111154,c48769]) ).
cnf(c118384,plain,
( product(e_1,e_1,e_1)
| product(e_2,e_1,e_1) ),
inference(resolution,[status(thm)],[c111321,e_3_is_not_e_2]) ).
cnf(c118515,plain,
( product(e_1,e_1,e_1)
| ~ product(e_1,e_2,X814)
| product(X814,e_1,e_2) ),
inference(resolution,[status(thm)],[c118384,qg4]) ).
cnf(c111386,plain,
( product(e_1,e_1,e_1)
| ~ product(e_1,X738,e_3)
| equalish(X738,e_1) ),
inference(resolution,[status(thm)],[c111154,product_right_cancellation]) ).
cnf(c181,plain,
( product(e_1,e_2,e_1)
| product(e_1,e_2,e_3)
| ~ product(e_2,e_1,X155)
| product(X155,e_2,e_1) ),
inference(resolution,[status(thm)],[c14,qg4]) ).
cnf(c118493,plain,
( product(e_1,e_1,e_1)
| product(e_1,e_2,e_1)
| product(e_1,e_2,e_3) ),
inference(resolution,[status(thm)],[c118384,c181]) ).
cnf(c137802,plain,
( product(e_1,e_1,e_1)
| product(e_1,e_2,e_1)
| equalish(e_2,e_1) ),
inference(resolution,[status(thm)],[c118493,c111386]) ).
cnf(c137924,plain,
( product(e_1,e_1,e_1)
| product(e_1,e_2,e_1) ),
inference(resolution,[status(thm)],[c137802,e_2_is_not_e_1]) ).
cnf(c137981,plain,
( product(e_1,e_1,e_1)
| product(e_1,e_1,e_2) ),
inference(resolution,[status(thm)],[c137924,c118515]) ).
cnf(c138090,plain,
( product(e_1,e_1,e_1)
| equalish(e_1,e_3) ),
inference(resolution,[status(thm)],[c137981,c114600]) ).
cnf(c138132,plain,
( equalish(e_1,e_3)
| product(e_1,e_3,e_2)
| product(e_1,e_3,e_3) ),
inference(resolution,[status(thm)],[c138090,c260]) ).
cnf(c140114,plain,
( product(e_1,e_3,e_2)
| product(e_1,e_3,e_3) ),
inference(resolution,[status(thm)],[c138132,e_1_is_not_e_3]) ).
cnf(c140219,plain,
( product(e_1,e_3,e_3)
| product(e_2,e_2,e_3) ),
inference(resolution,[status(thm)],[c140114,c128799]) ).
cnf(c140302,plain,
( product(e_2,e_2,e_3)
| product(e_3,e_2,e_3) ),
inference(resolution,[status(thm)],[c140219,c128799]) ).
cnf(c140336,plain,
( product(e_1,e_3,e_3)
| product(e_3,e_3,e_2) ),
inference(resolution,[status(thm)],[c140219,c7]) ).
cnf(c140204,plain,
( product(e_1,e_3,e_3)
| ~ product(X898,e_3,e_2)
| equalish(X898,e_1) ),
inference(resolution,[status(thm)],[c140114,product_left_cancellation]) ).
cnf(c140734,plain,
( product(e_1,e_3,e_3)
| equalish(e_3,e_1) ),
inference(resolution,[status(thm)],[c140204,c140336]) ).
cnf(c140853,plain,
product(e_1,e_3,e_3),
inference(resolution,[status(thm)],[c140734,e_3_is_not_e_1]) ).
cnf(c140876,plain,
( ~ product(X900,e_3,e_3)
| equalish(X900,e_1) ),
inference(resolution,[status(thm)],[c140853,product_left_cancellation]) ).
cnf(c5943,plain,
( product(e_1,e_1,e_1)
| product(e_2,e_2,e_2)
| product(e_2,e_2,e_1) ),
inference(resolution,[status(thm)],[c5818,c7]) ).
cnf(c6009,plain,
( product(e_2,e_2,e_2)
| product(e_2,e_2,e_1)
| ~ product(X342,e_1,e_1)
| equalish(X342,e_1) ),
inference(resolution,[status(thm)],[c5943,product_left_cancellation]) ).
cnf(c63,plain,
( product(e_2,e_2,e_1)
| product(e_2,e_2,e_2)
| product(e_3,e_3,e_2) ),
inference(resolution,[status(thm)],[c9,c7]) ).
cnf(c164,plain,
( product(e_3,e_1,e_1)
| product(e_3,e_1,e_3)
| ~ product(e_3,X144,e_2)
| equalish(X144,e_1) ),
inference(resolution,[status(thm)],[c13,product_right_cancellation]) ).
cnf(c968,plain,
( product(e_3,e_1,e_1)
| product(e_3,e_1,e_3)
| equalish(e_3,e_1)
| product(e_2,e_2,e_1)
| product(e_2,e_2,e_2) ),
inference(resolution,[status(thm)],[c164,c63]) ).
cnf(c22455,plain,
( product(e_3,e_1,e_3)
| equalish(e_3,e_1)
| product(e_2,e_2,e_1)
| product(e_2,e_2,e_2) ),
inference(resolution,[status(thm)],[c968,c6009]) ).
cnf(c82278,plain,
( product(e_3,e_1,e_3)
| product(e_2,e_2,e_1)
| product(e_2,e_2,e_2) ),
inference(resolution,[status(thm)],[c22455,e_3_is_not_e_1]) ).
cnf(c82583,plain,
( product(e_3,e_1,e_3)
| product(e_2,e_2,e_2)
| product(e_1,e_1,e_2) ),
inference(resolution,[status(thm)],[c82278,c7]) ).
cnf(c82881,plain,
( product(e_3,e_1,e_3)
| product(e_2,e_2,e_2)
| ~ product(e_1,e_1,X624)
| equalish(X624,e_2) ),
inference(resolution,[status(thm)],[c82583,product_total_function2]) ).
cnf(c5953,plain,
( product(e_1,e_1,e_1)
| product(e_2,e_2,e_2)
| ~ product(e_1,e_1,X338)
| equalish(X338,e_2) ),
inference(resolution,[status(thm)],[c5818,product_total_function2]) ).
cnf(c17720,plain,
( product(e_2,e_1,e_3)
| product(e_1,e_1,e_1)
| product(e_2,e_2,e_2)
| equalish(e_3,e_2) ),
inference(resolution,[status(thm)],[c17304,c5953]) ).
cnf(c45017,plain,
( product(e_2,e_1,e_3)
| product(e_1,e_1,e_1)
| product(e_2,e_2,e_2) ),
inference(resolution,[status(thm)],[c17720,e_3_is_not_e_2]) ).
cnf(c45051,plain,
( product(e_1,e_1,e_1)
| product(e_2,e_2,e_2)
| ~ product(X510,e_1,e_3)
| equalish(X510,e_2) ),
inference(resolution,[status(thm)],[c45017,product_left_cancellation]) ).
cnf(c111298,plain,
( product(e_1,e_1,e_1)
| product(e_2,e_2,e_2)
| equalish(e_1,e_2) ),
inference(resolution,[status(thm)],[c111154,c45051]) ).
cnf(c116595,plain,
( product(e_2,e_2,e_2)
| equalish(e_1,e_2)
| product(e_3,e_1,e_3) ),
inference(resolution,[status(thm)],[c111298,c82881]) ).
cnf(c121987,plain,
( product(e_2,e_2,e_2)
| product(e_3,e_1,e_3) ),
inference(resolution,[status(thm)],[c116595,e_1_is_not_e_2]) ).
cnf(c122202,plain,
( product(e_2,e_2,e_2)
| ~ product(e_1,e_3,X834)
| product(X834,e_3,e_3) ),
inference(resolution,[status(thm)],[c121987,qg4]) ).
cnf(c140867,plain,
( product(e_2,e_2,e_2)
| product(e_3,e_3,e_3) ),
inference(resolution,[status(thm)],[c140853,c122202]) ).
cnf(c141266,plain,
( product(e_2,e_2,e_2)
| equalish(e_3,e_1) ),
inference(resolution,[status(thm)],[c140867,c140876]) ).
cnf(c141382,plain,
product(e_2,e_2,e_2),
inference(resolution,[status(thm)],[c141266,e_3_is_not_e_1]) ).
cnf(c141396,plain,
( ~ product(e_2,e_2,X903)
| equalish(X903,e_2) ),
inference(resolution,[status(thm)],[c141382,product_total_function2]) ).
cnf(c141453,plain,
( equalish(e_3,e_2)
| product(e_3,e_2,e_3) ),
inference(resolution,[status(thm)],[c141396,c140302]) ).
cnf(c141909,plain,
product(e_3,e_2,e_3),
inference(resolution,[status(thm)],[c141453,e_3_is_not_e_2]) ).
cnf(c141968,plain,
( ~ product(e_3,X918,e_3)
| equalish(X918,e_2) ),
inference(resolution,[status(thm)],[c141909,product_right_cancellation]) ).
cnf(c140878,plain,
( ~ product(e_3,e_1,X902)
| product(X902,e_3,e_1) ),
inference(resolution,[status(thm)],[c140853,qg4]) ).
cnf(c128827,plain,
( product(e_3,e_1,e_2)
| ~ product(e_2,e_2,X827)
| equalish(X827,e_3) ),
inference(resolution,[status(thm)],[c128470,product_total_function2]) ).
cnf(c141397,plain,
( product(e_3,e_1,e_2)
| equalish(e_2,e_3) ),
inference(resolution,[status(thm)],[c141382,c128827]) ).
cnf(c141627,plain,
product(e_3,e_1,e_2),
inference(resolution,[status(thm)],[c141397,e_2_is_not_e_3]) ).
cnf(c141637,plain,
product(e_2,e_3,e_1),
inference(resolution,[status(thm)],[c141627,c140878]) ).
cnf(c141673,plain,
( ~ product(X912,e_3,e_1)
| equalish(X912,e_2) ),
inference(resolution,[status(thm)],[c141637,product_left_cancellation]) ).
cnf(c4269,plain,
( product(e_1,e_1,e_3)
| product(e_3,e_3,e_3)
| ~ product(X315,e_1,e_1)
| equalish(X315,e_1) ),
inference(resolution,[status(thm)],[c4082,product_left_cancellation]) ).
cnf(c969,plain,
( product(e_3,e_1,e_1)
| product(e_3,e_1,e_3)
| equalish(e_3,e_1)
| product(e_3,e_3,e_3)
| product(e_1,e_1,e_3) ),
inference(resolution,[status(thm)],[c164,c95]) ).
cnf(c22639,plain,
( product(e_3,e_1,e_3)
| equalish(e_3,e_1)
| product(e_3,e_3,e_3)
| product(e_1,e_1,e_3) ),
inference(resolution,[status(thm)],[c969,c4269]) ).
cnf(c86000,plain,
( product(e_3,e_1,e_3)
| product(e_3,e_3,e_3)
| product(e_1,e_1,e_3) ),
inference(resolution,[status(thm)],[c22639,e_3_is_not_e_1]) ).
cnf(c86419,plain,
( product(e_3,e_1,e_3)
| product(e_3,e_3,e_3)
| product(e_3,e_3,e_1) ),
inference(resolution,[status(thm)],[c86000,c7]) ).
cnf(c141093,plain,
( product(e_3,e_3,e_1)
| product(e_3,e_3,e_3) ),
inference(resolution,[status(thm)],[c140878,c86419]) ).
cnf(c142147,plain,
( product(e_3,e_3,e_3)
| equalish(e_3,e_2) ),
inference(resolution,[status(thm)],[c141093,c141673]) ).
cnf(c142298,plain,
equalish(e_3,e_2),
inference(resolution,[status(thm)],[c142147,c141968]) ).
cnf(c142312,plain,
$false,
inference(resolution,[status(thm)],[c142298,e_3_is_not_e_2]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.13 % Problem : GRP134-1.003 : TPTP v8.1.2. Released v1.2.0.
% 0.11/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.35 % Computer : n025.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:35:23 EDT 2024
% 0.13/0.35 % CPUTime :
% 203.77/203.98 % Version: 1.5
% 203.77/203.98 % SZS status Unsatisfiable
% 203.77/203.98 % SZS output start CNFRefutation
% See solution above
% 203.77/203.98
% 203.77/203.98 % Initial clauses : 14
% 203.77/203.98 % Processed clauses : 1283
% 203.77/203.98 % Factors computed : 5
% 203.77/203.98 % Resolvents computed: 142308
% 203.77/203.98 % Tautologies deleted: 0
% 203.77/203.98 % Forward subsumed : 4685
% 203.77/203.98 % Backward subsumed : 972
% 203.77/203.98 % -------- CPU Time ---------
% 203.77/203.98 % User time : 203.063 s
% 203.77/203.98 % System time : 0.526 s
% 203.77/203.98 % Total time : 203.588 s
%------------------------------------------------------------------------------