%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GRP126-1.004 : TPTP v8.1.2. Released v1.2.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n004.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:08 EDT 2024
% Result : Unsatisfiable 1.29s 1.49s
% Output : Refutation 1.29s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 18
% Syntax : Number of clauses : 66 ( 19 unt; 38 nHn; 65 RR)
% Number of literals : 159 ( 0 equ; 30 neg)
% Maximal clause size : 6 ( 2 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 4 ( 3 usr; 1 prp; 0-3 aty)
% Number of functors : 4 ( 4 usr; 4 con; 0-0 aty)
% Number of variables : 34 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
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(product_right_cancellation,axiom,
( ~ product(X17,X16,X18)
| ~ product(X17,X19,X18)
| equalish(X16,X19) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',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(product_left_cancellation,axiom,
( ~ product(X26,X28,X27)
| ~ product(X29,X28,X27)
| equalish(X26,X29) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',product_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(product_idempotence,axiom,
product(X2,X2,X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',product_idempotence) ).
cnf(c10,plain,
( ~ product(X23,X24,X23)
| equalish(X24,X23) ),
inference(resolution,[status(thm)],[product_right_cancellation,product_idempotence]) ).
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(c13,plain,
( ~ product(X37,X38,X38)
| equalish(X37,X38) ),
inference(resolution,[status(thm)],[product_left_cancellation,product_idempotence]) ).
cnf(element_4,axiom,
group_element(e_4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',element_4) ).
cnf(element_1,axiom,
group_element(e_1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',element_1) ).
cnf(product_total_function1,axiom,
( ~ group_element(X3)
| ~ group_element(X4)
| product(X3,X4,e_1)
| product(X3,X4,e_2)
| product(X3,X4,e_3)
| product(X3,X4,e_4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',product_total_function1) ).
cnf(c1,plain,
( ~ group_element(X47)
| product(X47,e_1,e_1)
| product(X47,e_1,e_2)
| product(X47,e_1,e_3)
| product(X47,e_1,e_4) ),
inference(resolution,[status(thm)],[product_total_function1,element_1]) ).
cnf(c26,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)],[c1,element_4]) ).
cnf(c122,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)],[c26,c13]) ).
cnf(c476,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)],[c122,e_4_is_not_e_1]) ).
cnf(c490,plain,
( product(e_4,e_1,e_2)
| product(e_4,e_1,e_3)
| equalish(e_1,e_4) ),
inference(resolution,[status(thm)],[c476,c10]) ).
cnf(c508,plain,
( product(e_4,e_1,e_2)
| product(e_4,e_1,e_3) ),
inference(resolution,[status(thm)],[c490,e_1_is_not_e_4]) ).
cnf(c518,plain,
( product(e_4,e_1,e_2)
| ~ product(X138,e_1,e_3)
| equalish(X138,e_4) ),
inference(resolution,[status(thm)],[c508,product_left_cancellation]) ).
cnf(product_total_function2,axiom,
( ~ product(X6,X7,X5)
| ~ product(X6,X7,X8)
| equalish(X5,X8) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',product_total_function2) ).
cnf(c6,plain,
( ~ product(X14,X14,X13)
| equalish(X13,X14) ),
inference(resolution,[status(thm)],[product_total_function2,product_idempotence]) ).
cnf(qg4,negated_conjecture,
( ~ product(X35,X36,X33)
| ~ product(X36,X35,X34)
| product(X33,X34,X36) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',qg4) ).
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_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_2,axiom,
group_element(e_2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',element_2) ).
cnf(c24,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)],[c1,element_2]) ).
cnf(c40,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)],[c24,c13]) ).
cnf(c88,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)],[c40,e_2_is_not_e_1]) ).
cnf(c93,plain,
( product(e_2,e_1,e_3)
| product(e_2,e_1,e_4)
| equalish(e_1,e_2) ),
inference(resolution,[status(thm)],[c88,c10]) ).
cnf(c110,plain,
( product(e_2,e_1,e_3)
| product(e_2,e_1,e_4) ),
inference(resolution,[status(thm)],[c93,e_1_is_not_e_2]) ).
cnf(c116,plain,
( product(e_2,e_1,e_3)
| ~ product(e_1,e_2,X58)
| product(X58,e_4,e_2) ),
inference(resolution,[status(thm)],[c110,qg4]) ).
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(c118,plain,
( product(e_2,e_1,e_3)
| ~ product(X56,e_1,e_4)
| equalish(X56,e_2) ),
inference(resolution,[status(thm)],[c110,product_left_cancellation]) ).
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(element_3,axiom,
group_element(e_3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',element_3) ).
cnf(c25,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)],[c1,element_3]) ).
cnf(c58,plain,
( product(e_3,e_1,e_2)
| product(e_3,e_1,e_3)
| product(e_3,e_1,e_4)
| equalish(e_3,e_1) ),
inference(resolution,[status(thm)],[c25,c13]) ).
cnf(c264,plain,
( 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)],[c58,e_3_is_not_e_1]) ).
cnf(c274,plain,
( product(e_3,e_1,e_2)
| product(e_3,e_1,e_4)
| equalish(e_1,e_3) ),
inference(resolution,[status(thm)],[c264,c10]) ).
cnf(c289,plain,
( product(e_3,e_1,e_2)
| product(e_3,e_1,e_4) ),
inference(resolution,[status(thm)],[c274,e_1_is_not_e_3]) ).
cnf(c295,plain,
( product(e_3,e_1,e_2)
| product(e_2,e_1,e_3)
| equalish(e_3,e_2) ),
inference(resolution,[status(thm)],[c289,c118]) ).
cnf(c388,plain,
( product(e_3,e_1,e_2)
| product(e_2,e_1,e_3) ),
inference(resolution,[status(thm)],[c295,e_3_is_not_e_2]) ).
cnf(c396,plain,
( product(e_2,e_1,e_3)
| ~ product(e_3,X85,e_2)
| equalish(X85,e_1) ),
inference(resolution,[status(thm)],[c388,product_right_cancellation]) ).
cnf(c2,plain,
( ~ group_element(X48)
| product(X48,e_2,e_1)
| product(X48,e_2,e_2)
| product(X48,e_2,e_3)
| product(X48,e_2,e_4) ),
inference(resolution,[status(thm)],[product_total_function1,element_2]) ).
cnf(c27,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)],[c2,element_1]) ).
cnf(c147,plain,
( product(e_1,e_2,e_2)
| product(e_1,e_2,e_3)
| product(e_1,e_2,e_4)
| equalish(e_2,e_1) ),
inference(resolution,[status(thm)],[c27,c10]) ).
cnf(c1044,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)],[c147,e_2_is_not_e_1]) ).
cnf(c1103,plain,
( product(e_1,e_2,e_3)
| product(e_1,e_2,e_4)
| equalish(e_1,e_2) ),
inference(resolution,[status(thm)],[c1044,c13]) ).
cnf(c1154,plain,
( product(e_1,e_2,e_3)
| product(e_1,e_2,e_4) ),
inference(resolution,[status(thm)],[c1103,e_1_is_not_e_2]) ).
cnf(c1157,plain,
( product(e_1,e_2,e_4)
| product(e_2,e_1,e_3)
| product(e_3,e_4,e_2) ),
inference(resolution,[status(thm)],[c1154,c116]) ).
cnf(c1240,plain,
( product(e_1,e_2,e_4)
| product(e_2,e_1,e_3)
| equalish(e_4,e_1) ),
inference(resolution,[status(thm)],[c1157,c396]) ).
cnf(c1280,plain,
( product(e_1,e_2,e_4)
| product(e_2,e_1,e_3) ),
inference(resolution,[status(thm)],[c1240,e_4_is_not_e_1]) ).
cnf(c1285,plain,
( product(e_2,e_1,e_3)
| product(e_4,e_4,e_2) ),
inference(resolution,[status(thm)],[c1280,c116]) ).
cnf(c1337,plain,
( product(e_2,e_1,e_3)
| equalish(e_2,e_4) ),
inference(resolution,[status(thm)],[c1285,c6]) ).
cnf(c1354,plain,
( equalish(e_2,e_4)
| product(e_4,e_1,e_2) ),
inference(resolution,[status(thm)],[c1337,c518]) ).
cnf(c1437,plain,
product(e_4,e_1,e_2),
inference(resolution,[status(thm)],[c1354,e_2_is_not_e_4]) ).
cnf(c1456,plain,
( ~ product(e_4,X258,e_2)
| equalish(X258,e_1) ),
inference(resolution,[status(thm)],[c1437,product_right_cancellation]) ).
cnf(c1368,plain,
product(e_2,e_1,e_3),
inference(resolution,[status(thm)],[c1337,e_2_is_not_e_4]) ).
cnf(c1384,plain,
( ~ product(e_1,e_2,X261)
| product(X261,e_3,e_2) ),
inference(resolution,[status(thm)],[c1368,qg4]) ).
cnf(c1161,plain,
( product(e_1,e_2,e_4)
| ~ product(e_2,e_1,X243)
| product(X243,e_3,e_1) ),
inference(resolution,[status(thm)],[c1154,qg4]) ).
cnf(c1307,plain,
( product(e_1,e_2,e_4)
| product(e_3,e_3,e_1) ),
inference(resolution,[status(thm)],[c1280,c1161]) ).
cnf(c1568,plain,
( product(e_1,e_2,e_4)
| equalish(e_1,e_3) ),
inference(resolution,[status(thm)],[c1307,c6]) ).
cnf(c1584,plain,
product(e_1,e_2,e_4),
inference(resolution,[status(thm)],[c1568,e_1_is_not_e_3]) ).
cnf(c1585,plain,
product(e_4,e_3,e_2),
inference(resolution,[status(thm)],[c1584,c1384]) ).
cnf(c1595,plain,
equalish(e_3,e_1),
inference(resolution,[status(thm)],[c1585,c1456]) ).
cnf(c1598,plain,
$false,
inference(resolution,[status(thm)],[c1595,e_3_is_not_e_1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : GRP126-1.004 : TPTP v8.1.2. Released v1.2.0.
% 0.07/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.12/0.34 % Computer : n004.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Thu May 9 03:37:38 EDT 2024
% 0.12/0.34 % CPUTime :
% 1.29/1.49 % Version: 1.5
% 1.29/1.49 % SZS status Unsatisfiable
% 1.29/1.49 % SZS output start CNFRefutation
% See solution above
% 1.29/1.49
% 1.29/1.49 % Initial clauses : 22
% 1.29/1.49 % Processed clauses : 190
% 1.29/1.49 % Factors computed : 5
% 1.29/1.49 % Resolvents computed: 1594
% 1.29/1.49 % Tautologies deleted: 0
% 1.29/1.49 % Forward subsumed : 478
% 1.29/1.49 % Backward subsumed : 128
% 1.29/1.49 % -------- CPU Time ---------
% 1.29/1.49 % User time : 1.131 s
% 1.29/1.49 % System time : 0.018 s
% 1.29/1.49 % Total time : 1.149 s
%------------------------------------------------------------------------------