%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GRP124-8.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:06 EDT 2024
% Result : Unsatisfiable 8.73s 8.93s
% Output : Refutation 8.73s
% Verified :
% SZS Type : Refutation
% Derivation depth : 24
% Number of leaves : 22
% Syntax : Number of clauses : 90 ( 22 unt; 56 nHn; 88 RR)
% Number of literals : 222 ( 0 equ; 38 neg)
% Maximal clause size : 6 ( 2 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 5 ( 4 usr; 1 prp; 0-3 aty)
% Number of functors : 4 ( 4 usr; 4 con; 0-0 aty)
% Number of variables : 43 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(e_4_is_not_e_1,axiom,
~ equalish(e_4,e_1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_4_is_not_e_1) ).
cnf(product1_left_cancellation,axiom,
( ~ product1(X44,X45,X47)
| ~ product1(X46,X45,X47)
| equalish(X44,X46) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',product1_left_cancellation) ).
cnf(e_4_is_not_e_2,axiom,
~ equalish(e_4,e_2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_4_is_not_e_2) ).
cnf(product1_total_function2,axiom,
( ~ product1(X16,X18,X17)
| ~ product1(X16,X18,X19)
| equalish(X17,X19) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',product1_total_function2) ).
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(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(product1_idempotence,axiom,
product1(X2,X2,X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',product1_idempotence) ).
cnf(product1_right_cancellation,axiom,
( ~ product1(X32,X33,X34)
| ~ product1(X32,X35,X34)
| equalish(X33,X35) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',product1_right_cancellation) ).
cnf(c29,plain,
( ~ product1(X41,X42,X41)
| equalish(X42,X41) ),
inference(resolution,[status(thm)],[product1_right_cancellation,product1_idempotence]) ).
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(c32,plain,
( ~ product1(X56,X55,X55)
| equalish(X56,X55) ),
inference(resolution,[status(thm)],[product1_left_cancellation,product1_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(product1_total_function1,axiom,
( ~ group_element(X67)
| ~ group_element(X68)
| product1(X67,X68,e_1)
| product1(X67,X68,e_2)
| product1(X67,X68,e_3)
| product1(X67,X68,e_4) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',product1_total_function1) ).
cnf(c38,plain,
( ~ group_element(X194)
| product1(X194,e_1,e_1)
| product1(X194,e_1,e_2)
| product1(X194,e_1,e_3)
| product1(X194,e_1,e_4) ),
inference(resolution,[status(thm)],[product1_total_function1,element_1]) ).
cnf(c314,plain,
( product1(e_2,e_1,e_1)
| product1(e_2,e_1,e_2)
| product1(e_2,e_1,e_3)
| product1(e_2,e_1,e_4) ),
inference(resolution,[status(thm)],[c38,element_2]) ).
cnf(c935,plain,
( product1(e_2,e_1,e_2)
| product1(e_2,e_1,e_3)
| product1(e_2,e_1,e_4)
| equalish(e_2,e_1) ),
inference(resolution,[status(thm)],[c314,c32]) ).
cnf(c1884,plain,
( product1(e_2,e_1,e_2)
| product1(e_2,e_1,e_3)
| product1(e_2,e_1,e_4) ),
inference(resolution,[status(thm)],[c935,e_2_is_not_e_1]) ).
cnf(c1886,plain,
( product1(e_2,e_1,e_3)
| product1(e_2,e_1,e_4)
| equalish(e_1,e_2) ),
inference(resolution,[status(thm)],[c1884,c29]) ).
cnf(c1907,plain,
( product1(e_2,e_1,e_3)
| product1(e_2,e_1,e_4) ),
inference(resolution,[status(thm)],[c1886,e_1_is_not_e_2]) ).
cnf(c1915,plain,
( product1(e_2,e_1,e_3)
| ~ product1(X382,e_1,e_4)
| equalish(X382,e_2) ),
inference(resolution,[status(thm)],[c1907,product1_left_cancellation]) ).
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(element_3,axiom,
group_element(e_3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',element_3) ).
cnf(c315,plain,
( product1(e_3,e_1,e_1)
| product1(e_3,e_1,e_2)
| product1(e_3,e_1,e_3)
| product1(e_3,e_1,e_4) ),
inference(resolution,[status(thm)],[c38,element_3]) ).
cnf(c956,plain,
( product1(e_3,e_1,e_2)
| product1(e_3,e_1,e_3)
| product1(e_3,e_1,e_4)
| equalish(e_3,e_1) ),
inference(resolution,[status(thm)],[c315,c32]) ).
cnf(c1954,plain,
( product1(e_3,e_1,e_2)
| product1(e_3,e_1,e_3)
| product1(e_3,e_1,e_4) ),
inference(resolution,[status(thm)],[c956,e_3_is_not_e_1]) ).
cnf(c1960,plain,
( product1(e_3,e_1,e_2)
| product1(e_3,e_1,e_4)
| equalish(e_1,e_3) ),
inference(resolution,[status(thm)],[c1954,c29]) ).
cnf(c1980,plain,
( product1(e_3,e_1,e_2)
| product1(e_3,e_1,e_4) ),
inference(resolution,[status(thm)],[c1960,e_1_is_not_e_3]) ).
cnf(c1987,plain,
( product1(e_3,e_1,e_2)
| product1(e_2,e_1,e_3)
| equalish(e_3,e_2) ),
inference(resolution,[status(thm)],[c1980,c1915]) ).
cnf(c2027,plain,
( product1(e_3,e_1,e_2)
| product1(e_2,e_1,e_3) ),
inference(resolution,[status(thm)],[c1987,e_3_is_not_e_2]) ).
cnf(c2031,plain,
( product1(e_2,e_1,e_3)
| ~ product1(e_3,e_1,X412)
| equalish(X412,e_2) ),
inference(resolution,[status(thm)],[c2027,product1_total_function2]) ).
cnf(product2_idempotence,axiom,
product2(X3,X3,X3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',product2_idempotence) ).
cnf(product2_total_function2,axiom,
( ~ product2(X58,X60,X59)
| ~ product2(X58,X60,X61)
| equalish(X59,X61) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',product2_total_function2) ).
cnf(c35,plain,
( ~ product2(X66,X66,X65)
| equalish(X65,X66) ),
inference(resolution,[status(thm)],[product2_total_function2,product2_idempotence]) ).
cnf(qg2a,negated_conjecture,
( ~ product1(X92,X94,X95)
| ~ product1(X95,X92,X93)
| product2(X93,X94,X92) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',qg2a) ).
cnf(c1982,plain,
( product1(e_3,e_1,e_4)
| ~ product1(e_1,X408,e_3)
| product2(e_2,X408,e_1) ),
inference(resolution,[status(thm)],[c1980,qg2a]) ).
cnf(c39,plain,
( ~ group_element(X197)
| product1(X197,e_2,e_1)
| product1(X197,e_2,e_2)
| product1(X197,e_2,e_3)
| product1(X197,e_2,e_4) ),
inference(resolution,[status(thm)],[product1_total_function1,element_2]) ).
cnf(c322,plain,
( product1(e_1,e_2,e_1)
| product1(e_1,e_2,e_2)
| product1(e_1,e_2,e_3)
| product1(e_1,e_2,e_4) ),
inference(resolution,[status(thm)],[c39,element_1]) ).
cnf(c993,plain,
( product1(e_1,e_2,e_2)
| product1(e_1,e_2,e_3)
| product1(e_1,e_2,e_4)
| equalish(e_2,e_1) ),
inference(resolution,[status(thm)],[c322,c29]) ).
cnf(c2619,plain,
( product1(e_1,e_2,e_2)
| product1(e_1,e_2,e_3)
| product1(e_1,e_2,e_4) ),
inference(resolution,[status(thm)],[c993,e_2_is_not_e_1]) ).
cnf(c2794,plain,
( product1(e_1,e_2,e_3)
| product1(e_1,e_2,e_4)
| equalish(e_1,e_2) ),
inference(resolution,[status(thm)],[c2619,c32]) ).
cnf(c2862,plain,
( product1(e_1,e_2,e_3)
| product1(e_1,e_2,e_4) ),
inference(resolution,[status(thm)],[c2794,e_1_is_not_e_2]) ).
cnf(c2869,plain,
( product1(e_1,e_2,e_4)
| product1(e_3,e_1,e_4)
| product2(e_2,e_2,e_1) ),
inference(resolution,[status(thm)],[c2862,c1982]) ).
cnf(c3031,plain,
( product1(e_1,e_2,e_4)
| product1(e_3,e_1,e_4)
| equalish(e_1,e_2) ),
inference(resolution,[status(thm)],[c2869,c35]) ).
cnf(c3068,plain,
( product1(e_1,e_2,e_4)
| product1(e_3,e_1,e_4) ),
inference(resolution,[status(thm)],[c3031,e_1_is_not_e_2]) ).
cnf(c3088,plain,
( product1(e_1,e_2,e_4)
| product1(e_2,e_1,e_3)
| equalish(e_4,e_2) ),
inference(resolution,[status(thm)],[c3068,c2031]) ).
cnf(c3330,plain,
( product1(e_1,e_2,e_4)
| product1(e_2,e_1,e_3) ),
inference(resolution,[status(thm)],[c3088,e_4_is_not_e_2]) ).
cnf(c3350,plain,
( product1(e_1,e_2,e_4)
| ~ product1(X589,e_1,e_3)
| equalish(X589,e_2) ),
inference(resolution,[status(thm)],[c3330,product1_left_cancellation]) ).
cnf(e_4_is_not_e_3,axiom,
~ equalish(e_4,e_3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_4_is_not_e_3) ).
cnf(c2029,plain,
( product1(e_2,e_1,e_3)
| ~ product1(X411,e_1,e_2)
| equalish(X411,e_3) ),
inference(resolution,[status(thm)],[c2027,product1_left_cancellation]) ).
cnf(e_1_is_not_e_4,axiom,
~ equalish(e_1,e_4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_1_is_not_e_4) ).
cnf(element_4,axiom,
group_element(e_4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',element_4) ).
cnf(c316,plain,
( product1(e_4,e_1,e_1)
| product1(e_4,e_1,e_2)
| product1(e_4,e_1,e_3)
| product1(e_4,e_1,e_4) ),
inference(resolution,[status(thm)],[c38,element_4]) ).
cnf(c975,plain,
( product1(e_4,e_1,e_2)
| product1(e_4,e_1,e_3)
| product1(e_4,e_1,e_4)
| equalish(e_4,e_1) ),
inference(resolution,[status(thm)],[c316,c32]) ).
cnf(c2090,plain,
( product1(e_4,e_1,e_2)
| product1(e_4,e_1,e_3)
| product1(e_4,e_1,e_4) ),
inference(resolution,[status(thm)],[c975,e_4_is_not_e_1]) ).
cnf(c2104,plain,
( product1(e_4,e_1,e_2)
| product1(e_4,e_1,e_3)
| equalish(e_1,e_4) ),
inference(resolution,[status(thm)],[c2090,c29]) ).
cnf(c2123,plain,
( product1(e_4,e_1,e_2)
| product1(e_4,e_1,e_3) ),
inference(resolution,[status(thm)],[c2104,e_1_is_not_e_4]) ).
cnf(c2128,plain,
( product1(e_4,e_1,e_3)
| product1(e_2,e_1,e_3)
| equalish(e_4,e_3) ),
inference(resolution,[status(thm)],[c2123,c2029]) ).
cnf(c2241,plain,
( product1(e_4,e_1,e_3)
| product1(e_2,e_1,e_3) ),
inference(resolution,[status(thm)],[c2128,e_4_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(c324,plain,
( product1(e_3,e_2,e_1)
| product1(e_3,e_2,e_2)
| product1(e_3,e_2,e_3)
| product1(e_3,e_2,e_4) ),
inference(resolution,[status(thm)],[c39,element_3]) ).
cnf(c1017,plain,
( product1(e_3,e_2,e_1)
| product1(e_3,e_2,e_3)
| product1(e_3,e_2,e_4)
| equalish(e_3,e_2) ),
inference(resolution,[status(thm)],[c324,c32]) ).
cnf(c3201,plain,
( product1(e_3,e_2,e_1)
| product1(e_3,e_2,e_3)
| product1(e_3,e_2,e_4) ),
inference(resolution,[status(thm)],[c1017,e_3_is_not_e_2]) ).
cnf(c6924,plain,
( product1(e_3,e_2,e_1)
| product1(e_3,e_2,e_4)
| equalish(e_2,e_3) ),
inference(resolution,[status(thm)],[c3201,c29]) ).
cnf(c7004,plain,
( product1(e_3,e_2,e_1)
| product1(e_3,e_2,e_4) ),
inference(resolution,[status(thm)],[c6924,e_2_is_not_e_3]) ).
cnf(c7031,plain,
( product1(e_3,e_2,e_1)
| ~ product1(e_3,X805,e_4)
| equalish(X805,e_2) ),
inference(resolution,[status(thm)],[c7004,product1_right_cancellation]) ).
cnf(c3069,plain,
( product1(e_3,e_1,e_4)
| ~ product1(X567,e_2,e_4)
| equalish(X567,e_1) ),
inference(resolution,[status(thm)],[c3068,product1_left_cancellation]) ).
cnf(c7025,plain,
( product1(e_3,e_2,e_1)
| product1(e_3,e_1,e_4)
| equalish(e_3,e_1) ),
inference(resolution,[status(thm)],[c7004,c3069]) ).
cnf(c7479,plain,
( product1(e_3,e_2,e_1)
| product1(e_3,e_1,e_4) ),
inference(resolution,[status(thm)],[c7025,e_3_is_not_e_1]) ).
cnf(c7509,plain,
( product1(e_3,e_2,e_1)
| equalish(e_1,e_2) ),
inference(resolution,[status(thm)],[c7479,c7031]) ).
cnf(c7556,plain,
product1(e_3,e_2,e_1),
inference(resolution,[status(thm)],[c7509,e_1_is_not_e_2]) ).
cnf(c7566,plain,
( ~ product1(e_2,X829,e_3)
| product2(e_1,X829,e_2) ),
inference(resolution,[status(thm)],[c7556,qg2a]) ).
cnf(c7618,plain,
( product2(e_1,e_1,e_2)
| product1(e_4,e_1,e_3) ),
inference(resolution,[status(thm)],[c7566,c2241]) ).
cnf(c7643,plain,
( product1(e_4,e_1,e_3)
| equalish(e_2,e_1) ),
inference(resolution,[status(thm)],[c7618,c35]) ).
cnf(c7714,plain,
product1(e_4,e_1,e_3),
inference(resolution,[status(thm)],[c7643,e_2_is_not_e_1]) ).
cnf(c7720,plain,
( product1(e_1,e_2,e_4)
| equalish(e_4,e_2) ),
inference(resolution,[status(thm)],[c7714,c3350]) ).
cnf(c7878,plain,
product1(e_1,e_2,e_4),
inference(resolution,[status(thm)],[c7720,e_4_is_not_e_2]) ).
cnf(c7880,plain,
( ~ product1(X841,e_2,e_4)
| equalish(X841,e_1) ),
inference(resolution,[status(thm)],[c7878,product1_left_cancellation]) ).
cnf(c7737,plain,
( ~ product1(e_4,X833,e_3)
| equalish(X833,e_1) ),
inference(resolution,[status(thm)],[c7714,product1_right_cancellation]) ).
cnf(c7559,plain,
( ~ product1(X824,e_2,e_1)
| equalish(X824,e_3) ),
inference(resolution,[status(thm)],[c7556,product1_left_cancellation]) ).
cnf(c325,plain,
( product1(e_4,e_2,e_1)
| product1(e_4,e_2,e_2)
| product1(e_4,e_2,e_3)
| product1(e_4,e_2,e_4) ),
inference(resolution,[status(thm)],[c39,element_4]) ).
cnf(c1036,plain,
( product1(e_4,e_2,e_1)
| product1(e_4,e_2,e_3)
| product1(e_4,e_2,e_4)
| equalish(e_4,e_2) ),
inference(resolution,[status(thm)],[c325,c32]) ).
cnf(c3917,plain,
( product1(e_4,e_2,e_1)
| product1(e_4,e_2,e_3)
| product1(e_4,e_2,e_4) ),
inference(resolution,[status(thm)],[c1036,e_4_is_not_e_2]) ).
cnf(c8729,plain,
( product1(e_4,e_2,e_3)
| product1(e_4,e_2,e_4)
| equalish(e_4,e_3) ),
inference(resolution,[status(thm)],[c3917,c7559]) ).
cnf(c8798,plain,
( product1(e_4,e_2,e_3)
| product1(e_4,e_2,e_4) ),
inference(resolution,[status(thm)],[c8729,e_4_is_not_e_3]) ).
cnf(c8806,plain,
( product1(e_4,e_2,e_4)
| equalish(e_2,e_1) ),
inference(resolution,[status(thm)],[c8798,c7737]) ).
cnf(c8843,plain,
product1(e_4,e_2,e_4),
inference(resolution,[status(thm)],[c8806,e_2_is_not_e_1]) ).
cnf(c8846,plain,
equalish(e_4,e_1),
inference(resolution,[status(thm)],[c8843,c7880]) ).
cnf(c8855,plain,
$false,
inference(resolution,[status(thm)],[c8846,e_4_is_not_e_1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : GRP124-8.004 : TPTP v8.1.2. Released v1.2.0.
% 0.07/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.34 % Computer : n004.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Thu May 9 04:20:38 EDT 2024
% 0.13/0.34 % CPUTime :
% 8.73/8.93 % Version: 1.5
% 8.73/8.93 % SZS status Unsatisfiable
% 8.73/8.93 % SZS output start CNFRefutation
% See solution above
% 8.73/8.94
% 8.73/8.94 % Initial clauses : 48
% 8.73/8.94 % Processed clauses : 1072
% 8.73/8.94 % Factors computed : 12
% 8.73/8.94 % Resolvents computed: 8844
% 8.73/8.94 % Tautologies deleted: 33
% 8.73/8.94 % Forward subsumed : 2667
% 8.73/8.94 % Backward subsumed : 472
% 8.73/8.94 % -------- CPU Time ---------
% 8.73/8.94 % User time : 8.557 s
% 8.73/8.94 % System time : 0.032 s
% 8.73/8.94 % Total time : 8.589 s
%------------------------------------------------------------------------------