%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GRP123-4.003 : TPTP v8.1.2. Bugfixed v1.2.1.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n032.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:02 EDT 2024
% Result : Unsatisfiable 0.49s 0.68s
% Output : Refutation 0.49s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 13
% Syntax : Number of clauses : 36 ( 13 unt; 14 nHn; 35 RR)
% Number of literals : 80 ( 0 equ; 26 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 : 29 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
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(product_idempotence,axiom,
product(X2,X2,X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',product_idempotence) ).
cnf(product_total_function2,axiom,
( ~ product(X9,X10,X7)
| ~ product(X9,X10,X8)
| equalish(X7,X8) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',product_total_function2) ).
cnf(c9,plain,
( ~ product(X16,X16,X15)
| equalish(X15,X16) ),
inference(resolution,[status(thm)],[product_total_function2,product_idempotence]) ).
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(qg1_2,negated_conjecture,
( ~ product(X57,X55,X56)
| ~ product(X54,X58,X56)
| ~ product(X53,X55,X57)
| ~ product(X53,X58,X54)
| equalish(X55,X58) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',qg1_2) ).
cnf(c29,plain,
( ~ product(X101,X102,X103)
| ~ product(X100,X100,X103)
| ~ product(X100,X102,X101)
| equalish(X102,X100) ),
inference(resolution,[status(thm)],[qg1_2,product_idempotence]) ).
cnf(product_right_cancellation,axiom,
( ~ product(X22,X20,X23)
| ~ product(X22,X21,X23)
| equalish(X20,X21) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',product_right_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(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(c17,plain,
( ~ product(X27,X28,X27)
| equalish(X28,X27) ),
inference(resolution,[status(thm)],[product_right_cancellation,product_idempotence]) ).
cnf(element_2,axiom,
group_element(e_2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',element_2) ).
cnf(element_1,axiom,
group_element(e_1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',element_1) ).
cnf(row_surjectivity,axiom,
( ~ group_element(X3)
| ~ group_element(X4)
| product(e_1,X3,X4)
| product(e_2,X3,X4)
| product(e_3,X3,X4) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',row_surjectivity) ).
cnf(c1,plain,
( ~ group_element(X88)
| product(e_1,X88,e_1)
| product(e_2,X88,e_1)
| product(e_3,X88,e_1) ),
inference(resolution,[status(thm)],[row_surjectivity,element_1]) ).
cnf(c40,plain,
( product(e_1,e_2,e_1)
| product(e_2,e_2,e_1)
| product(e_3,e_2,e_1) ),
inference(resolution,[status(thm)],[c1,element_2]) ).
cnf(c85,plain,
( product(e_2,e_2,e_1)
| product(e_3,e_2,e_1)
| equalish(e_2,e_1) ),
inference(resolution,[status(thm)],[c40,c17]) ).
cnf(c155,plain,
( product(e_2,e_2,e_1)
| product(e_3,e_2,e_1) ),
inference(resolution,[status(thm)],[c85,e_2_is_not_e_1]) ).
cnf(c163,plain,
( product(e_3,e_2,e_1)
| equalish(e_1,e_2) ),
inference(resolution,[status(thm)],[c155,c9]) ).
cnf(c184,plain,
product(e_3,e_2,e_1),
inference(resolution,[status(thm)],[c163,e_1_is_not_e_2]) ).
cnf(c188,plain,
( ~ product(e_3,X120,e_1)
| equalish(X120,e_2) ),
inference(resolution,[status(thm)],[c184,product_right_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(element_3,axiom,
group_element(e_3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',element_3) ).
cnf(c41,plain,
( product(e_1,e_3,e_1)
| product(e_2,e_3,e_1)
| product(e_3,e_3,e_1) ),
inference(resolution,[status(thm)],[c1,element_3]) ).
cnf(c114,plain,
( product(e_2,e_3,e_1)
| product(e_3,e_3,e_1)
| equalish(e_3,e_1) ),
inference(resolution,[status(thm)],[c41,c17]) ).
cnf(c285,plain,
( product(e_2,e_3,e_1)
| product(e_3,e_3,e_1) ),
inference(resolution,[status(thm)],[c114,e_3_is_not_e_1]) ).
cnf(c296,plain,
( product(e_2,e_3,e_1)
| equalish(e_3,e_2) ),
inference(resolution,[status(thm)],[c285,c188]) ).
cnf(c310,plain,
( equalish(e_3,e_2)
| ~ product(e_1,e_3,X148)
| ~ product(e_2,e_2,X148) ),
inference(resolution,[status(thm)],[c296,c29]) ).
cnf(c361,plain,
( equalish(e_3,e_2)
| ~ product(e_1,e_3,e_2) ),
inference(resolution,[status(thm)],[c310,product_idempotence]) ).
cnf(c2,plain,
( ~ group_element(X104)
| product(e_1,X104,e_2)
| product(e_2,X104,e_2)
| product(e_3,X104,e_2) ),
inference(resolution,[status(thm)],[row_surjectivity,element_2]) ).
cnf(c50,plain,
( product(e_1,e_3,e_2)
| product(e_2,e_3,e_2)
| product(e_3,e_3,e_2) ),
inference(resolution,[status(thm)],[c2,element_3]) ).
cnf(c243,plain,
( product(e_1,e_3,e_2)
| product(e_3,e_3,e_2)
| equalish(e_3,e_2) ),
inference(resolution,[status(thm)],[c50,c17]) ).
cnf(c515,plain,
( product(e_3,e_3,e_2)
| equalish(e_3,e_2) ),
inference(resolution,[status(thm)],[c243,c361]) ).
cnf(c551,plain,
product(e_3,e_3,e_2),
inference(resolution,[status(thm)],[c515,e_3_is_not_e_2]) ).
cnf(c565,plain,
equalish(e_2,e_3),
inference(resolution,[status(thm)],[c551,c9]) ).
cnf(c567,plain,
$false,
inference(resolution,[status(thm)],[c565,e_2_is_not_e_3]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.02/0.09 % Problem : GRP123-4.003 : TPTP v8.1.2. Bugfixed v1.2.1.
% 0.02/0.10 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.09/0.29 % Computer : n032.cluster.edu
% 0.09/0.29 % Model : x86_64 x86_64
% 0.09/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.29 % Memory : 8042.1875MB
% 0.09/0.29 % OS : Linux 3.10.0-693.el7.x86_64
% 0.09/0.29 % CPULimit : 300
% 0.09/0.29 % WCLimit : 300
% 0.09/0.29 % DateTime : Thu May 9 04:07:22 EDT 2024
% 0.09/0.29 % CPUTime :
% 0.49/0.68 % Version: 1.5
% 0.49/0.68 % SZS status Unsatisfiable
% 0.49/0.68 % SZS output start CNFRefutation
% See solution above
% 0.49/0.68
% 0.49/0.68 % Initial clauses : 18
% 0.49/0.68 % Processed clauses : 86
% 0.49/0.68 % Factors computed : 20
% 0.49/0.68 % Resolvents computed: 548
% 0.49/0.68 % Tautologies deleted: 0
% 0.49/0.68 % Forward subsumed : 90
% 0.49/0.68 % Backward subsumed : 20
% 0.49/0.68 % -------- CPU Time ---------
% 0.49/0.68 % User time : 0.374 s
% 0.49/0.68 % System time : 0.013 s
% 0.49/0.68 % Total time : 0.387 s
%------------------------------------------------------------------------------