%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GRP124-1.004 : TPTP v8.1.2. Released v1.2.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n016.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:04 EDT 2024
% Result : Unsatisfiable 4.98s 5.18s
% Output : Refutation 4.98s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 15
% Syntax : Number of clauses : 71 ( 16 unt; 42 nHn; 70 RR)
% Number of literals : 189 ( 0 equ; 48 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 : 47 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
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(e_4_is_not_e_2,axiom,
~ equalish(e_4,e_2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_4_is_not_e_2) ).
cnf(product_idempotence,axiom,
product(X2,X2,X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',product_idempotence) ).
cnf(qg2_1,negated_conjecture,
( ~ product(X37,X36,X35)
| ~ product(X34,X38,X35)
| ~ product(X33,X37,X36)
| ~ product(X33,X34,X38)
| equalish(X37,X34) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',qg2_1) ).
cnf(c17,plain,
( ~ product(X73,X72,X70)
| ~ product(X71,X71,X70)
| ~ product(X71,X73,X72)
| equalish(X73,X71) ),
inference(resolution,[status(thm)],[qg2_1,product_idempotence]) ).
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(product_left_cancellation,axiom,
( ~ product(X27,X26,X28)
| ~ product(X29,X26,X28)
| equalish(X27,X29) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',product_left_cancellation) ).
cnf(c13,plain,
( ~ product(X40,X39,X39)
| equalish(X40,X39) ),
inference(resolution,[status(thm)],[product_left_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(product_right_cancellation,axiom,
( ~ product(X18,X17,X16)
| ~ product(X18,X19,X16)
| equalish(X17,X19) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',product_right_cancellation) ).
cnf(c10,plain,
( ~ product(X23,X24,X23)
| equalish(X24,X23) ),
inference(resolution,[status(thm)],[product_right_cancellation,product_idempotence]) ).
cnf(element_1,axiom,
group_element(e_1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',element_1) ).
cnf(element_4,axiom,
group_element(e_4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',element_4) ).
cnf(product_total_function1,axiom,
( ~ group_element(X4)
| ~ group_element(X3)
| product(X4,X3,e_1)
| product(X4,X3,e_2)
| product(X4,X3,e_3)
| product(X4,X3,e_4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',product_total_function1) ).
cnf(c1,plain,
( ~ group_element(X77)
| product(X77,e_4,e_1)
| product(X77,e_4,e_2)
| product(X77,e_4,e_3)
| product(X77,e_4,e_4) ),
inference(resolution,[status(thm)],[product_total_function1,element_4]) ).
cnf(c37,plain,
( product(e_1,e_4,e_1)
| product(e_1,e_4,e_2)
| product(e_1,e_4,e_3)
| product(e_1,e_4,e_4) ),
inference(resolution,[status(thm)],[c1,element_1]) ).
cnf(c59,plain,
( product(e_1,e_4,e_2)
| product(e_1,e_4,e_3)
| product(e_1,e_4,e_4)
| equalish(e_4,e_1) ),
inference(resolution,[status(thm)],[c37,c10]) ).
cnf(c110,plain,
( product(e_1,e_4,e_2)
| product(e_1,e_4,e_3)
| product(e_1,e_4,e_4) ),
inference(resolution,[status(thm)],[c59,e_4_is_not_e_1]) ).
cnf(c128,plain,
( product(e_1,e_4,e_2)
| product(e_1,e_4,e_3)
| equalish(e_1,e_4) ),
inference(resolution,[status(thm)],[c110,c13]) ).
cnf(c147,plain,
( product(e_1,e_4,e_2)
| product(e_1,e_4,e_3) ),
inference(resolution,[status(thm)],[c128,e_1_is_not_e_4]) ).
cnf(c160,plain,
( product(e_1,e_4,e_2)
| ~ product(X106,e_4,e_3)
| equalish(X106,e_1) ),
inference(resolution,[status(thm)],[c147,product_left_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(element_2,axiom,
group_element(e_2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',element_2) ).
cnf(c38,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)],[c1,element_2]) ).
cnf(c170,plain,
( product(e_2,e_4,e_1)
| product(e_2,e_4,e_3)
| product(e_2,e_4,e_4)
| equalish(e_4,e_2) ),
inference(resolution,[status(thm)],[c38,c10]) ).
cnf(c415,plain,
( product(e_2,e_4,e_1)
| product(e_2,e_4,e_3)
| product(e_2,e_4,e_4) ),
inference(resolution,[status(thm)],[c170,e_4_is_not_e_2]) ).
cnf(c434,plain,
( product(e_2,e_4,e_1)
| product(e_2,e_4,e_3)
| equalish(e_2,e_4) ),
inference(resolution,[status(thm)],[c415,c13]) ).
cnf(c454,plain,
( product(e_2,e_4,e_1)
| product(e_2,e_4,e_3) ),
inference(resolution,[status(thm)],[c434,e_2_is_not_e_4]) ).
cnf(c462,plain,
( product(e_2,e_4,e_1)
| product(e_1,e_4,e_2)
| equalish(e_2,e_1) ),
inference(resolution,[status(thm)],[c454,c160]) ).
cnf(c599,plain,
( product(e_2,e_4,e_1)
| product(e_1,e_4,e_2) ),
inference(resolution,[status(thm)],[c462,e_2_is_not_e_1]) ).
cnf(c609,plain,
( product(e_1,e_4,e_2)
| ~ product(e_4,e_1,X184)
| ~ product(e_2,e_2,X184)
| equalish(e_4,e_2) ),
inference(resolution,[status(thm)],[c599,c17]) ).
cnf(c699,plain,
( product(e_1,e_4,e_2)
| ~ product(e_4,e_1,e_2)
| equalish(e_4,e_2) ),
inference(resolution,[status(thm)],[c609,product_idempotence]) ).
cnf(c2,plain,
( ~ group_element(X88)
| product(X88,e_1,e_1)
| product(X88,e_1,e_2)
| product(X88,e_1,e_3)
| product(X88,e_1,e_4) ),
inference(resolution,[status(thm)],[product_total_function1,element_1]) ).
cnf(c43,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)],[c2,element_4]) ).
cnf(c234,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)],[c43,c13]) ).
cnf(c1806,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)],[c234,e_4_is_not_e_1]) ).
cnf(c1837,plain,
( product(e_4,e_1,e_2)
| product(e_4,e_1,e_3)
| equalish(e_1,e_4) ),
inference(resolution,[status(thm)],[c1806,c10]) ).
cnf(c1867,plain,
( product(e_4,e_1,e_2)
| product(e_4,e_1,e_3) ),
inference(resolution,[status(thm)],[c1837,e_1_is_not_e_4]) ).
cnf(c1871,plain,
( product(e_4,e_1,e_3)
| product(e_1,e_4,e_2)
| equalish(e_4,e_2) ),
inference(resolution,[status(thm)],[c1867,c699]) ).
cnf(c1953,plain,
( product(e_4,e_1,e_3)
| product(e_1,e_4,e_2) ),
inference(resolution,[status(thm)],[c1871,e_4_is_not_e_2]) ).
cnf(qg2_2,negated_conjecture,
( ~ product(X54,X53,X52)
| ~ product(X51,X55,X52)
| ~ product(X50,X54,X53)
| ~ product(X50,X51,X55)
| equalish(X53,X55) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',qg2_2) ).
cnf(c25,plain,
( ~ product(X90,X91,X92)
| ~ product(X93,X93,X92)
| ~ product(X93,X90,X91)
| equalish(X91,X93) ),
inference(resolution,[status(thm)],[qg2_2,product_idempotence]) ).
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(c45,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)],[c2,element_2]) ).
cnf(c267,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)],[c45,c13]) ).
cnf(c2883,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)],[c267,e_2_is_not_e_1]) ).
cnf(c3330,plain,
( product(e_2,e_1,e_3)
| product(e_2,e_1,e_4)
| equalish(e_1,e_2) ),
inference(resolution,[status(thm)],[c2883,c10]) ).
cnf(c3455,plain,
( product(e_2,e_1,e_3)
| product(e_2,e_1,e_4) ),
inference(resolution,[status(thm)],[c3330,e_1_is_not_e_2]) ).
cnf(c3482,plain,
( product(e_2,e_1,e_4)
| ~ product(X667,e_1,e_3)
| equalish(X667,e_2) ),
inference(resolution,[status(thm)],[c3455,product_left_cancellation]) ).
cnf(c458,plain,
( product(e_2,e_4,e_3)
| ~ product(e_4,e_1,X174)
| ~ product(e_2,e_2,X174)
| equalish(e_1,e_2) ),
inference(resolution,[status(thm)],[c454,c25]) ).
cnf(c687,plain,
( product(e_2,e_4,e_3)
| ~ product(e_4,e_1,e_2)
| equalish(e_1,e_2) ),
inference(resolution,[status(thm)],[c458,product_idempotence]) ).
cnf(c1872,plain,
( product(e_4,e_1,e_3)
| product(e_2,e_4,e_3)
| equalish(e_1,e_2) ),
inference(resolution,[status(thm)],[c1867,c687]) ).
cnf(c2090,plain,
( product(e_4,e_1,e_3)
| product(e_2,e_4,e_3) ),
inference(resolution,[status(thm)],[c1872,e_1_is_not_e_2]) ).
cnf(c2114,plain,
( product(e_4,e_1,e_3)
| ~ product(e_2,X518,e_3)
| equalish(X518,e_4) ),
inference(resolution,[status(thm)],[c2090,product_right_cancellation]) ).
cnf(c3458,plain,
( product(e_2,e_1,e_4)
| product(e_4,e_1,e_3)
| equalish(e_1,e_4) ),
inference(resolution,[status(thm)],[c3455,c2114]) ).
cnf(c3752,plain,
( product(e_2,e_1,e_4)
| product(e_4,e_1,e_3) ),
inference(resolution,[status(thm)],[c3458,e_1_is_not_e_4]) ).
cnf(c3785,plain,
( product(e_2,e_1,e_4)
| equalish(e_4,e_2) ),
inference(resolution,[status(thm)],[c3752,c3482]) ).
cnf(c3849,plain,
( equalish(e_4,e_2)
| ~ product(e_1,e_4,X703)
| ~ product(e_2,e_2,X703) ),
inference(resolution,[status(thm)],[c3785,c25]) ).
cnf(c3973,plain,
( equalish(e_4,e_2)
| ~ product(e_1,e_4,e_2) ),
inference(resolution,[status(thm)],[c3849,product_idempotence]) ).
cnf(c3977,plain,
( equalish(e_4,e_2)
| product(e_4,e_1,e_3) ),
inference(resolution,[status(thm)],[c3973,c1953]) ).
cnf(c4252,plain,
product(e_4,e_1,e_3),
inference(resolution,[status(thm)],[c3977,e_4_is_not_e_2]) ).
cnf(c3974,plain,
( equalish(e_4,e_2)
| product(e_1,e_4,e_3) ),
inference(resolution,[status(thm)],[c3973,c147]) ).
cnf(c3978,plain,
product(e_1,e_4,e_3),
inference(resolution,[status(thm)],[c3974,e_4_is_not_e_2]) ).
cnf(c3976,plain,
( equalish(e_4,e_2)
| product(e_2,e_4,e_1) ),
inference(resolution,[status(thm)],[c3973,c599]) ).
cnf(c4180,plain,
product(e_2,e_4,e_1),
inference(resolution,[status(thm)],[c3976,e_4_is_not_e_2]) ).
cnf(c3852,plain,
product(e_2,e_1,e_4),
inference(resolution,[status(thm)],[c3785,e_4_is_not_e_2]) ).
cnf(c3855,plain,
( ~ product(X826,X827,X828)
| ~ product(e_1,e_4,X828)
| ~ product(e_2,X826,X827)
| equalish(X827,e_4) ),
inference(resolution,[status(thm)],[c3852,qg2_2]) ).
cnf(c4845,plain,
( ~ product(e_4,e_1,X830)
| ~ product(e_1,e_4,X830)
| equalish(e_1,e_4) ),
inference(resolution,[status(thm)],[c3855,c4180]) ).
cnf(c4850,plain,
( ~ product(e_4,e_1,e_3)
| equalish(e_1,e_4) ),
inference(resolution,[status(thm)],[c4845,c3978]) ).
cnf(c4851,plain,
equalish(e_1,e_4),
inference(resolution,[status(thm)],[c4850,c4252]) ).
cnf(c4933,plain,
$false,
inference(resolution,[status(thm)],[c4851,e_1_is_not_e_4]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.13 % Problem : GRP124-1.004 : TPTP v8.1.2. Released v1.2.0.
% 0.03/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.35 % Computer : n016.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 04:16:38 EDT 2024
% 0.13/0.35 % CPUTime :
% 4.98/5.18 % Version: 1.5
% 4.98/5.18 % SZS status Unsatisfiable
% 4.98/5.18 % SZS output start CNFRefutation
% See solution above
% 4.98/5.18
% 4.98/5.18 % Initial clauses : 23
% 4.98/5.18 % Processed clauses : 464
% 4.98/5.18 % Factors computed : 82
% 4.98/5.18 % Resolvents computed: 4852
% 4.98/5.18 % Tautologies deleted: 0
% 4.98/5.18 % Forward subsumed : 1337
% 4.98/5.18 % Backward subsumed : 302
% 4.98/5.18 % -------- CPU Time ---------
% 4.98/5.18 % User time : 4.784 s
% 4.98/5.18 % System time : 0.038 s
% 4.98/5.18 % Total time : 4.822 s
%------------------------------------------------------------------------------