%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GRP133-1.003 : TPTP v8.1.2. Released v1.2.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n021.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:14 EDT 2024
% Result : Unsatisfiable 190.14s 190.32s
% Output : Refutation 190.14s
% Verified :
% SZS Type : Refutation
% Derivation depth : 30
% Number of leaves : 14
% Syntax : Number of clauses : 123 ( 15 unt; 99 nHn; 123 RR)
% Number of literals : 375 ( 0 equ; 52 neg)
% Maximal clause size : 5 ( 3 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 : 55 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
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(product_left_cancellation,axiom,
( ~ product(X21,X19,X20)
| ~ product(X18,X19,X20)
| equalish(X21,X18) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',product_left_cancellation) ).
cnf(product_right_cancellation,axiom,
( ~ product(X13,X14,X12)
| ~ product(X13,X11,X12)
| equalish(X14,X11) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',product_right_cancellation) ).
cnf(qg3,negated_conjecture,
( ~ product(X27,X25,X26)
| ~ product(X25,X27,X28)
| product(X26,X28,X27) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',qg3) ).
cnf(c7,plain,
( ~ product(X31,X31,X30)
| product(X30,X30,X31) ),
inference(factor,[status(thm)],[qg3]) ).
cnf(element_1,axiom,
group_element(e_1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',element_1) ).
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(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(c43,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(c458,plain,
( product(e_1,e_1,e_1)
| product(e_3,e_3,e_1)
| ~ product(X221,e_1,e_2)
| equalish(X221,e_1) ),
inference(resolution,[status(thm)],[c43,product_left_cancellation]) ).
cnf(c35,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(c401,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)],[c35,c7]) ).
cnf(element_2,axiom,
group_element(e_2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',element_2) ).
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(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(c899,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_3,e_3,e_1) ),
inference(resolution,[status(thm)],[c120,c401]) ).
cnf(c11954,plain,
( product(e_2,e_1,e_3)
| equalish(e_2,e_1)
| product(e_1,e_1,e_1)
| product(e_3,e_3,e_1) ),
inference(resolution,[status(thm)],[c899,c458]) ).
cnf(c16690,plain,
( product(e_2,e_1,e_3)
| product(e_1,e_1,e_1)
| product(e_3,e_3,e_1) ),
inference(resolution,[status(thm)],[c11954,e_2_is_not_e_1]) ).
cnf(c16822,plain,
( product(e_1,e_1,e_1)
| product(e_3,e_3,e_1)
| ~ product(e_1,e_2,X471)
| product(X471,e_3,e_1) ),
inference(resolution,[status(thm)],[c16690,qg3]) ).
cnf(c454,plain,
( product(e_1,e_1,e_1)
| product(e_3,e_3,e_1)
| ~ product(e_1,X220,e_2)
| equalish(X220,e_1) ),
inference(resolution,[status(thm)],[c43,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(c1012,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_3,e_3,e_1) ),
inference(resolution,[status(thm)],[c180,c401]) ).
cnf(c32008,plain,
( product(e_1,e_2,e_3)
| equalish(e_2,e_1)
| product(e_1,e_1,e_1)
| product(e_3,e_3,e_1) ),
inference(resolution,[status(thm)],[c1012,c454]) ).
cnf(c109041,plain,
( equalish(e_2,e_1)
| product(e_1,e_1,e_1)
| product(e_3,e_3,e_1) ),
inference(resolution,[status(thm)],[c32008,c16822]) ).
cnf(c109288,plain,
( product(e_1,e_1,e_1)
| product(e_3,e_3,e_1) ),
inference(resolution,[status(thm)],[c109041,e_2_is_not_e_1]) ).
cnf(c109645,plain,
( product(e_1,e_1,e_1)
| product(e_1,e_1,e_3) ),
inference(resolution,[status(thm)],[c109288,c7]) ).
cnf(c110080,plain,
( product(e_1,e_1,e_1)
| ~ product(e_1,X743,e_3)
| equalish(X743,e_1) ),
inference(resolution,[status(thm)],[c109645,product_right_cancellation]) ).
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_total_function2,axiom,
( ~ product(X4,X3,X5)
| ~ product(X4,X3,X2)
| equalish(X5,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',product_total_function2) ).
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(c51,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(c501,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)],[c51,c7]) ).
cnf(c462,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)],[c43,product_total_function2]) ).
cnf(c1343,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)],[c462,c501]) ).
cnf(c5819,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)],[c1343,e_2_is_not_e_1]) ).
cnf(c5919,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)],[c5819,c7]) ).
cnf(c6064,plain,
( product(e_1,e_1,e_1)
| product(e_2,e_2,e_1)
| ~ product(e_2,X345,e_2)
| equalish(X345,e_2) ),
inference(resolution,[status(thm)],[c5919,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(c940,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_2,e_2,e_1) ),
inference(resolution,[status(thm)],[c136,c35]) ).
cnf(c17412,plain,
( product(e_2,e_1,e_1)
| equalish(e_1,e_2)
| product(e_1,e_1,e_1)
| product(e_2,e_2,e_1) ),
inference(resolution,[status(thm)],[c940,c6064]) ).
cnf(c41931,plain,
( product(e_2,e_1,e_1)
| product(e_1,e_1,e_1)
| product(e_2,e_2,e_1) ),
inference(resolution,[status(thm)],[c17412,e_1_is_not_e_2]) ).
cnf(c42216,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)],[c41931,c7]) ).
cnf(c42896,plain,
( product(e_2,e_1,e_1)
| product(e_1,e_1,e_1)
| ~ product(e_1,e_1,X517)
| equalish(X517,e_2) ),
inference(resolution,[status(thm)],[c42216,product_total_function2]) ).
cnf(c109995,plain,
( product(e_1,e_1,e_1)
| product(e_2,e_1,e_1)
| equalish(e_3,e_2) ),
inference(resolution,[status(thm)],[c109645,c42896]) ).
cnf(c115404,plain,
( product(e_1,e_1,e_1)
| product(e_2,e_1,e_1) ),
inference(resolution,[status(thm)],[c109995,e_3_is_not_e_2]) ).
cnf(c115485,plain,
( product(e_1,e_1,e_1)
| ~ product(e_1,e_2,X805)
| product(X805,e_1,e_1) ),
inference(resolution,[status(thm)],[c115404,qg3]) ).
cnf(c187,plain,
( product(e_1,e_2,e_1)
| product(e_1,e_2,e_3)
| ~ product(X158,e_2,e_2)
| equalish(X158,e_1) ),
inference(resolution,[status(thm)],[c14,product_left_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_2) ),
inference(resolution,[status(thm)],[c14,qg3]) ).
cnf(c5897,plain,
( product(e_1,e_1,e_2)
| product(e_2,e_2,e_2)
| ~ product(X335,e_1,e_1)
| equalish(X335,e_1) ),
inference(resolution,[status(thm)],[c5819,product_left_cancellation]) ).
cnf(c134,plain,
( product(e_2,e_1,e_1)
| product(e_2,e_1,e_2)
| ~ product(e_2,X135,e_3)
| equalish(X135,e_1) ),
inference(resolution,[status(thm)],[c12,product_right_cancellation]) ).
cnf(c935,plain,
( product(e_2,e_1,e_1)
| product(e_2,e_1,e_2)
| equalish(e_2,e_1)
| product(e_2,e_2,e_2)
| product(e_1,e_1,e_2) ),
inference(resolution,[status(thm)],[c134,c51]) ).
cnf(c16294,plain,
( product(e_2,e_1,e_2)
| equalish(e_2,e_1)
| product(e_2,e_2,e_2)
| product(e_1,e_1,e_2) ),
inference(resolution,[status(thm)],[c935,c5897]) ).
cnf(c24625,plain,
( product(e_2,e_1,e_2)
| product(e_2,e_2,e_2)
| product(e_1,e_1,e_2) ),
inference(resolution,[status(thm)],[c16294,e_2_is_not_e_1]) ).
cnf(c24916,plain,
( product(e_2,e_1,e_2)
| product(e_2,e_2,e_2)
| ~ product(e_1,e_1,X442)
| equalish(X442,e_2) ),
inference(resolution,[status(thm)],[c24625,product_total_function2]) ).
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_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(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(element_3,axiom,
group_element(e_3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',element_3) ).
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(c99,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(c606,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)],[c99,c7]) ).
cnf(c404,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)],[c35,product_total_function2]) ).
cnf(c1270,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)],[c404,c606]) ).
cnf(c4500,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)],[c1270,e_3_is_not_e_1]) ).
cnf(c4606,plain,
( product(e_1,e_1,e_1)
| product(e_3,e_3,e_3)
| ~ product(e_1,e_1,X319)
| equalish(X319,e_3) ),
inference(resolution,[status(thm)],[c4500,product_total_function2]) ).
cnf(c5924,plain,
( product(e_1,e_1,e_1)
| product(e_2,e_2,e_2)
| product(e_3,e_3,e_3)
| equalish(e_2,e_3) ),
inference(resolution,[status(thm)],[c5819,c4606]) ).
cnf(c9167,plain,
( product(e_1,e_1,e_1)
| product(e_2,e_2,e_2)
| product(e_3,e_3,e_3) ),
inference(resolution,[status(thm)],[c5924,e_2_is_not_e_3]) ).
cnf(c9304,plain,
( product(e_1,e_1,e_1)
| product(e_2,e_2,e_2)
| ~ product(e_3,e_3,X383)
| equalish(X383,e_3) ),
inference(resolution,[status(thm)],[c9167,product_total_function2]) ).
cnf(c109691,plain,
( product(e_1,e_1,e_1)
| product(e_2,e_2,e_2)
| equalish(e_1,e_3) ),
inference(resolution,[status(thm)],[c109288,c9304]) ).
cnf(c114100,plain,
( product(e_1,e_1,e_1)
| product(e_2,e_2,e_2) ),
inference(resolution,[status(thm)],[c109691,e_1_is_not_e_3]) ).
cnf(c114185,plain,
( product(e_2,e_2,e_2)
| product(e_2,e_1,e_2)
| equalish(e_1,e_2) ),
inference(resolution,[status(thm)],[c114100,c24916]) ).
cnf(c122252,plain,
( product(e_2,e_2,e_2)
| product(e_2,e_1,e_2) ),
inference(resolution,[status(thm)],[c114185,e_1_is_not_e_2]) ).
cnf(c122387,plain,
( product(e_2,e_2,e_2)
| product(e_1,e_2,e_1)
| product(e_1,e_2,e_3) ),
inference(resolution,[status(thm)],[c122252,c181]) ).
cnf(c135036,plain,
( product(e_1,e_2,e_1)
| product(e_1,e_2,e_3)
| equalish(e_2,e_1) ),
inference(resolution,[status(thm)],[c122387,c187]) ).
cnf(c135182,plain,
( product(e_1,e_2,e_1)
| product(e_1,e_2,e_3) ),
inference(resolution,[status(thm)],[c135036,e_2_is_not_e_1]) ).
cnf(c135196,plain,
( product(e_1,e_2,e_3)
| product(e_1,e_1,e_1) ),
inference(resolution,[status(thm)],[c135182,c115485]) ).
cnf(c135276,plain,
( product(e_1,e_1,e_1)
| equalish(e_2,e_1) ),
inference(resolution,[status(thm)],[c135196,c110080]) ).
cnf(c135401,plain,
product(e_1,e_1,e_1),
inference(resolution,[status(thm)],[c135276,e_2_is_not_e_1]) ).
cnf(c135425,plain,
( ~ product(X871,e_1,e_1)
| equalish(X871,e_1) ),
inference(resolution,[status(thm)],[c135401,product_left_cancellation]) ).
cnf(c624,plain,
( product(e_3,e_3,e_2)
| product(e_3,e_3,e_3)
| ~ product(X250,e_1,e_3)
| equalish(X250,e_1) ),
inference(resolution,[status(thm)],[c99,product_left_cancellation]) ).
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(c18915,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,c624]) ).
cnf(c59217,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)],[c18915,e_3_is_not_e_1]) ).
cnf(c59680,plain,
( product(e_3,e_1,e_2)
| product(e_3,e_3,e_3)
| product(e_2,e_2,e_3) ),
inference(resolution,[status(thm)],[c59217,c7]) ).
cnf(c60364,plain,
( product(e_3,e_1,e_2)
| product(e_2,e_2,e_3)
| ~ product(e_3,X572,e_3)
| equalish(X572,e_3) ),
inference(resolution,[status(thm)],[c59680,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(c42,plain,
( product(e_1,e_1,e_1)
| product(e_1,e_1,e_2)
| ~ product(X58,e_1,e_3)
| equalish(X58,e_1) ),
inference(resolution,[status(thm)],[c8,product_left_cancellation]) ).
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_1,e_1,e_2) ),
inference(resolution,[status(thm)],[c157,c43]) ).
cnf(c18556,plain,
( product(e_3,e_1,e_2)
| equalish(e_3,e_1)
| product(e_1,e_1,e_1)
| product(e_1,e_1,e_2) ),
inference(resolution,[status(thm)],[c949,c42]) ).
cnf(c53543,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)],[c18556,e_3_is_not_e_1]) ).
cnf(c53906,plain,
( product(e_3,e_1,e_2)
| product(e_1,e_1,e_1)
| ~ product(e_1,e_1,X547)
| equalish(X547,e_2) ),
inference(resolution,[status(thm)],[c53543,product_total_function2]) ).
cnf(c110034,plain,
( product(e_1,e_1,e_1)
| product(e_3,e_1,e_2)
| equalish(e_3,e_2) ),
inference(resolution,[status(thm)],[c109645,c53906]) ).
cnf(c117104,plain,
( product(e_1,e_1,e_1)
| product(e_3,e_1,e_2) ),
inference(resolution,[status(thm)],[c110034,e_3_is_not_e_2]) ).
cnf(c117135,plain,
( product(e_3,e_1,e_2)
| product(e_3,e_1,e_3)
| equalish(e_1,e_3) ),
inference(resolution,[status(thm)],[c117104,c159]) ).
cnf(c125071,plain,
( product(e_3,e_1,e_2)
| equalish(e_1,e_3)
| product(e_2,e_2,e_3) ),
inference(resolution,[status(thm)],[c117135,c60364]) ).
cnf(c130456,plain,
( product(e_3,e_1,e_2)
| product(e_2,e_2,e_3) ),
inference(resolution,[status(thm)],[c125071,e_1_is_not_e_3]) ).
cnf(c130572,plain,
( product(e_3,e_1,e_2)
| ~ product(X836,e_2,e_3)
| equalish(X836,e_2) ),
inference(resolution,[status(thm)],[c130456,product_left_cancellation]) ).
cnf(c135449,plain,
( ~ product(e_1,X873,e_1)
| equalish(X873,e_1) ),
inference(resolution,[status(thm)],[c135401,product_right_cancellation]) ).
cnf(c135642,plain,
( equalish(e_2,e_1)
| product(e_1,e_2,e_3) ),
inference(resolution,[status(thm)],[c135449,c135182]) ).
cnf(c136034,plain,
product(e_1,e_2,e_3),
inference(resolution,[status(thm)],[c135642,e_2_is_not_e_1]) ).
cnf(c136098,plain,
( product(e_3,e_1,e_2)
| equalish(e_1,e_2) ),
inference(resolution,[status(thm)],[c136034,c130572]) ).
cnf(c136395,plain,
product(e_3,e_1,e_2),
inference(resolution,[status(thm)],[c136098,e_1_is_not_e_2]) ).
cnf(c136428,plain,
( ~ product(e_3,X882,e_2)
| equalish(X882,e_1) ),
inference(resolution,[status(thm)],[c136395,product_right_cancellation]) ).
cnf(c127,plain,
( product(e_2,e_1,e_1)
| product(e_2,e_1,e_3)
| ~ product(e_2,X124,e_2)
| equalish(X124,e_1) ),
inference(resolution,[status(thm)],[c12,product_right_cancellation]) ).
cnf(c756,plain,
( product(e_2,e_2,e_2)
| product(e_3,e_3,e_2)
| ~ product(X276,e_1,e_2)
| equalish(X276,e_1) ),
inference(resolution,[status(thm)],[c501,product_left_cancellation]) ).
cnf(c67,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(c902,plain,
( product(e_2,e_1,e_2)
| product(e_2,e_1,e_3)
| equalish(e_2,e_1)
| product(e_2,e_2,e_2)
| product(e_3,e_3,e_2) ),
inference(resolution,[status(thm)],[c120,c67]) ).
cnf(c12332,plain,
( product(e_2,e_1,e_3)
| equalish(e_2,e_1)
| product(e_2,e_2,e_2)
| product(e_3,e_3,e_2) ),
inference(resolution,[status(thm)],[c902,c756]) ).
cnf(c20444,plain,
( product(e_2,e_1,e_3)
| equalish(e_2,e_1)
| product(e_3,e_3,e_2)
| product(e_2,e_1,e_1) ),
inference(resolution,[status(thm)],[c12332,c127]) ).
cnf(c67703,plain,
( product(e_2,e_1,e_3)
| product(e_3,e_3,e_2)
| product(e_2,e_1,e_1) ),
inference(resolution,[status(thm)],[c20444,e_2_is_not_e_1]) ).
cnf(c136076,plain,
( ~ product(e_2,e_1,X879)
| product(X879,e_3,e_2) ),
inference(resolution,[status(thm)],[c136034,qg3]) ).
cnf(c136294,plain,
( product(e_3,e_3,e_2)
| product(e_2,e_1,e_1) ),
inference(resolution,[status(thm)],[c136076,c67703]) ).
cnf(c136934,plain,
( product(e_2,e_1,e_1)
| equalish(e_3,e_1) ),
inference(resolution,[status(thm)],[c136294,c136428]) ).
cnf(c137049,plain,
product(e_2,e_1,e_1),
inference(resolution,[status(thm)],[c136934,e_3_is_not_e_1]) ).
cnf(c137060,plain,
equalish(e_2,e_1),
inference(resolution,[status(thm)],[c137049,c135425]) ).
cnf(c137084,plain,
$false,
inference(resolution,[status(thm)],[c137060,e_2_is_not_e_1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.13/0.14 % Problem : GRP133-1.003 : TPTP v8.1.2. Released v1.2.0.
% 0.13/0.15 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.15/0.36 % Computer : n021.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:56:23 EDT 2024
% 0.15/0.37 % CPUTime :
% 190.14/190.32 % Version: 1.5
% 190.14/190.32 % SZS status Unsatisfiable
% 190.14/190.32 % SZS output start CNFRefutation
% See solution above
% 190.14/190.32
% 190.14/190.32 % Initial clauses : 14
% 190.14/190.32 % Processed clauses : 1246
% 190.14/190.32 % Factors computed : 5
% 190.14/190.32 % Resolvents computed: 137080
% 190.14/190.32 % Tautologies deleted: 0
% 190.14/190.32 % Forward subsumed : 4492
% 190.14/190.32 % Backward subsumed : 907
% 190.14/190.32 % -------- CPU Time ---------
% 190.14/190.32 % User time : 189.440 s
% 190.14/190.32 % System time : 0.496 s
% 190.14/190.32 % Total time : 189.936 s
%------------------------------------------------------------------------------