%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GRP128-2.004 : TPTP v8.1.2. Released v1.2.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n008.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:10 EDT 2024
% Result : Satisfiable 5.81s 6.07s
% Output : Saturation 5.91s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(product_total_function2,axiom,
( ~ product(X6,X8,X5)
| ~ product(X6,X8,X7)
| equalish(X5,X7) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',product_total_function2) ).
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(product_right_cancellation,axiom,
( ~ product(X13,X12,X15)
| ~ product(X13,X14,X15)
| equalish(X12,X14) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',product_right_cancellation) ).
cnf(qg3,negated_conjecture,
( ~ product(X29,X31,X30)
| ~ product(X30,X31,X28)
| product(X29,X30,X28) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',qg3) ).
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(product_left_cancellation,axiom,
( ~ product(X21,X24,X22)
| ~ product(X23,X24,X22)
| equalish(X21,X23) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',product_left_cancellation) ).
cnf(e_2_then_e_3,axiom,
next(e_2,e_3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_2_then_e_3) ).
cnf(e_4_greater_e_3,axiom,
greater(e_4,e_3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_4_greater_e_3) ).
cnf(no_redundancy,axiom,
( ~ product(X2,e_1,X4)
| ~ next(X2,X3)
| ~ greater(X4,X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',no_redundancy) ).
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(c8,plain,
( ~ product(X32,X33,X32)
| product(X32,X32,X32) ),
inference(factor,[status(thm)],[qg3]) ).
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(product_total_function1,axiom,
( ~ group_element(X16)
| ~ group_element(X17)
| product(X16,X17,e_1)
| product(X16,X17,e_2)
| product(X16,X17,e_3)
| product(X16,X17,e_4) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',product_total_function1) ).
cnf(c3,plain,
( ~ group_element(X35)
| product(X35,e_1,e_1)
| product(X35,e_1,e_2)
| product(X35,e_1,e_3)
| product(X35,e_1,e_4) ),
inference(resolution,[status(thm)],[product_total_function1,element_1]) ).
cnf(c14,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)],[c3,element_2]) ).
cnf(c213,plain,
( product(e_2,e_1,e_1)
| product(e_2,e_1,e_3)
| product(e_2,e_1,e_4)
| product(e_2,e_2,e_2) ),
inference(resolution,[status(thm)],[c14,c8]) ).
cnf(c211,plain,
( product(e_2,e_1,e_1)
| product(e_2,e_1,e_3)
| product(e_2,e_1,e_4)
| ~ product(e_2,X216,e_2)
| equalish(X216,e_1) ),
inference(resolution,[status(thm)],[c14,product_right_cancellation]) ).
cnf(c1441,plain,
( product(e_2,e_1,e_1)
| product(e_2,e_1,e_3)
| product(e_2,e_1,e_4)
| equalish(e_2,e_1) ),
inference(resolution,[status(thm)],[c211,c213]) ).
cnf(c1489,plain,
( product(e_2,e_1,e_1)
| product(e_2,e_1,e_3)
| product(e_2,e_1,e_4) ),
inference(resolution,[status(thm)],[c1441,e_2_is_not_e_1]) ).
cnf(c1520,plain,
( product(e_2,e_1,e_1)
| product(e_2,e_1,e_3)
| ~ next(e_2,X224)
| ~ greater(e_4,X224) ),
inference(resolution,[status(thm)],[c1489,no_redundancy]) ).
cnf(c1536,plain,
( product(e_2,e_1,e_1)
| product(e_2,e_1,e_3)
| ~ next(e_2,e_3) ),
inference(resolution,[status(thm)],[c1520,e_4_greater_e_3]) ).
cnf(c1539,plain,
( product(e_2,e_1,e_1)
| product(e_2,e_1,e_3) ),
inference(resolution,[status(thm)],[c1536,e_2_then_e_3]) ).
cnf(c1547,plain,
( product(e_2,e_1,e_3)
| ~ product(X231,e_1,e_1)
| equalish(X231,e_2) ),
inference(resolution,[status(thm)],[c1539,product_left_cancellation]) ).
cnf(c1543,plain,
( product(e_2,e_1,e_3)
| ~ product(X238,e_1,e_2)
| product(X238,e_2,e_1) ),
inference(resolution,[status(thm)],[c1539,qg3]) ).
cnf(e_1_then_e_2,axiom,
next(e_1,e_2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_1_then_e_2) ).
cnf(e_4_greater_e_2,axiom,
greater(e_4,e_2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_4_greater_e_2) ).
cnf(e_3_greater_e_2,axiom,
greater(e_3,e_2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_3_greater_e_2) ).
cnf(c2,plain,
( ~ group_element(X34)
| product(X34,X34,e_1)
| product(X34,X34,e_2)
| product(X34,X34,e_3)
| product(X34,X34,e_4) ),
inference(factor,[status(thm)],[product_total_function1]) ).
cnf(c9,plain,
( product(e_1,e_1,e_1)
| product(e_1,e_1,e_2)
| product(e_1,e_1,e_3)
| product(e_1,e_1,e_4) ),
inference(resolution,[status(thm)],[c2,element_1]) ).
cnf(c53,plain,
( product(e_1,e_1,e_1)
| product(e_1,e_1,e_2)
| product(e_1,e_1,e_4)
| ~ next(e_1,X81)
| ~ greater(e_3,X81) ),
inference(resolution,[status(thm)],[c9,no_redundancy]) ).
cnf(c932,plain,
( product(e_1,e_1,e_1)
| product(e_1,e_1,e_2)
| product(e_1,e_1,e_4)
| ~ next(e_1,e_2) ),
inference(resolution,[status(thm)],[c53,e_3_greater_e_2]) ).
cnf(c1141,plain,
( product(e_1,e_1,e_1)
| product(e_1,e_1,e_2)
| product(e_1,e_1,e_4) ),
inference(resolution,[status(thm)],[c932,e_1_then_e_2]) ).
cnf(c1180,plain,
( product(e_1,e_1,e_1)
| product(e_1,e_1,e_2)
| ~ next(e_1,X170)
| ~ greater(e_4,X170) ),
inference(resolution,[status(thm)],[c1141,no_redundancy]) ).
cnf(c1199,plain,
( product(e_1,e_1,e_1)
| product(e_1,e_1,e_2)
| ~ next(e_1,e_2) ),
inference(resolution,[status(thm)],[c1180,e_4_greater_e_2]) ).
cnf(c1204,plain,
( product(e_1,e_1,e_1)
| product(e_1,e_1,e_2) ),
inference(resolution,[status(thm)],[c1199,e_1_then_e_2]) ).
cnf(c1212,plain,
( product(e_1,e_1,e_2)
| ~ product(X177,e_1,e_1)
| equalish(X177,e_1) ),
inference(resolution,[status(thm)],[c1204,product_left_cancellation]) ).
cnf(c1544,plain,
( product(e_2,e_1,e_3)
| product(e_1,e_1,e_2)
| equalish(e_2,e_1) ),
inference(resolution,[status(thm)],[c1539,c1212]) ).
cnf(c1621,plain,
( product(e_2,e_1,e_3)
| product(e_1,e_1,e_2) ),
inference(resolution,[status(thm)],[c1544,e_2_is_not_e_1]) ).
cnf(c1640,plain,
( product(e_2,e_1,e_3)
| product(e_1,e_2,e_1) ),
inference(resolution,[status(thm)],[c1621,c1543]) ).
cnf(c1676,plain,
( product(e_2,e_1,e_3)
| product(e_1,e_1,e_1) ),
inference(resolution,[status(thm)],[c1640,c8]) ).
cnf(c1703,plain,
( product(e_2,e_1,e_3)
| equalish(e_1,e_2) ),
inference(resolution,[status(thm)],[c1676,c1547]) ).
cnf(c1733,plain,
product(e_2,e_1,e_3),
inference(resolution,[status(thm)],[c1703,e_1_is_not_e_2]) ).
cnf(c1743,plain,
( ~ product(X252,e_1,e_2)
| product(X252,e_2,e_3) ),
inference(resolution,[status(thm)],[c1733,qg3]) ).
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(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(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_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(c15,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)],[c3,element_3]) ).
cnf(c1744,plain,
( ~ product(X248,e_1,e_3)
| equalish(X248,e_2) ),
inference(resolution,[status(thm)],[c1733,product_left_cancellation]) ).
cnf(c1759,plain,
( equalish(e_3,e_2)
| product(e_3,e_1,e_1)
| product(e_3,e_1,e_2)
| product(e_3,e_1,e_4) ),
inference(resolution,[status(thm)],[c1744,c15]) ).
cnf(c2168,plain,
( product(e_3,e_1,e_1)
| product(e_3,e_1,e_2)
| product(e_3,e_1,e_4) ),
inference(resolution,[status(thm)],[c1759,e_3_is_not_e_2]) ).
cnf(c1224,plain,
( product(e_1,e_1,e_1)
| ~ product(X182,e_1,e_2)
| equalish(X182,e_1) ),
inference(resolution,[status(thm)],[c1204,product_left_cancellation]) ).
cnf(c1223,plain,
( product(e_1,e_1,e_1)
| ~ product(X186,e_1,e_1)
| product(X186,e_1,e_2) ),
inference(resolution,[status(thm)],[c1204,qg3]) ).
cnf(c2237,plain,
( product(e_3,e_1,e_2)
| product(e_3,e_1,e_4)
| product(e_1,e_1,e_1) ),
inference(resolution,[status(thm)],[c2168,c1223]) ).
cnf(c2299,plain,
( product(e_3,e_1,e_4)
| product(e_1,e_1,e_1)
| equalish(e_3,e_1) ),
inference(resolution,[status(thm)],[c2237,c1224]) ).
cnf(c2387,plain,
( product(e_3,e_1,e_4)
| product(e_1,e_1,e_1) ),
inference(resolution,[status(thm)],[c2299,e_3_is_not_e_1]) ).
cnf(c2412,plain,
( product(e_3,e_1,e_4)
| ~ product(X381,e_1,e_1)
| equalish(X381,e_1) ),
inference(resolution,[status(thm)],[c2387,product_left_cancellation]) ).
cnf(c2475,plain,
( product(e_3,e_1,e_4)
| equalish(e_3,e_1)
| product(e_3,e_1,e_2) ),
inference(resolution,[status(thm)],[c2412,c2168]) ).
cnf(c2573,plain,
( product(e_3,e_1,e_4)
| product(e_3,e_1,e_2) ),
inference(resolution,[status(thm)],[c2475,e_3_is_not_e_1]) ).
cnf(c2613,plain,
( product(e_3,e_1,e_4)
| product(e_3,e_2,e_3) ),
inference(resolution,[status(thm)],[c2573,c1743]) ).
cnf(c2661,plain,
( product(e_3,e_1,e_4)
| product(e_3,e_3,e_3) ),
inference(resolution,[status(thm)],[c2613,c8]) ).
cnf(c2651,plain,
( product(e_3,e_1,e_4)
| ~ product(e_3,X427,e_3)
| equalish(X427,e_2) ),
inference(resolution,[status(thm)],[c2613,product_right_cancellation]) ).
cnf(c2757,plain,
( product(e_3,e_1,e_4)
| equalish(e_3,e_2) ),
inference(resolution,[status(thm)],[c2651,c2661]) ).
cnf(c2786,plain,
product(e_3,e_1,e_4),
inference(resolution,[status(thm)],[c2757,e_3_is_not_e_2]) ).
cnf(c2793,plain,
( ~ product(X433,e_1,e_4)
| equalish(X433,e_3) ),
inference(resolution,[status(thm)],[c2786,product_left_cancellation]) ).
cnf(element_4,axiom,
group_element(e_4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',element_4) ).
cnf(c16,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)],[c3,element_4]) ).
cnf(c1760,plain,
( equalish(e_4,e_2)
| product(e_4,e_1,e_1)
| product(e_4,e_1,e_2)
| product(e_4,e_1,e_4) ),
inference(resolution,[status(thm)],[c1744,c16]) ).
cnf(c3352,plain,
( product(e_4,e_1,e_1)
| product(e_4,e_1,e_2)
| product(e_4,e_1,e_4) ),
inference(resolution,[status(thm)],[c1760,e_4_is_not_e_2]) ).
cnf(c3448,plain,
( product(e_4,e_1,e_1)
| product(e_4,e_1,e_2)
| equalish(e_4,e_3) ),
inference(resolution,[status(thm)],[c3352,c2793]) ).
cnf(c3513,plain,
( product(e_4,e_1,e_1)
| product(e_4,e_1,e_2) ),
inference(resolution,[status(thm)],[c3448,e_4_is_not_e_3]) ).
cnf(c3523,plain,
( product(e_4,e_1,e_2)
| product(e_1,e_1,e_1) ),
inference(resolution,[status(thm)],[c3513,c1223]) ).
cnf(c3558,plain,
( product(e_1,e_1,e_1)
| equalish(e_4,e_1) ),
inference(resolution,[status(thm)],[c3523,c1224]) ).
cnf(c3603,plain,
product(e_1,e_1,e_1),
inference(resolution,[status(thm)],[c3558,e_4_is_not_e_1]) ).
cnf(c3608,plain,
( ~ product(X575,e_1,e_1)
| equalish(X575,e_1) ),
inference(resolution,[status(thm)],[c3603,product_left_cancellation]) ).
cnf(c3626,plain,
( equalish(e_4,e_1)
| product(e_4,e_1,e_2) ),
inference(resolution,[status(thm)],[c3608,c3513]) ).
cnf(c3629,plain,
product(e_4,e_1,e_2),
inference(resolution,[status(thm)],[c3626,e_4_is_not_e_1]) ).
cnf(c3645,plain,
product(e_4,e_2,e_3),
inference(resolution,[status(thm)],[c3629,c1743]) ).
cnf(c3660,plain,
( ~ product(e_4,X590,e_3)
| equalish(X590,e_2) ),
inference(resolution,[status(thm)],[c3645,product_right_cancellation]) ).
cnf(c3652,plain,
( ~ product(X594,e_1,e_4)
| product(X594,e_4,e_2) ),
inference(resolution,[status(thm)],[c3629,qg3]) ).
cnf(c3689,plain,
product(e_3,e_4,e_2),
inference(resolution,[status(thm)],[c3652,c2786]) ).
cnf(c2798,plain,
( ~ product(X436,e_1,e_3)
| product(X436,e_3,e_4) ),
inference(resolution,[status(thm)],[c2786,qg3]) ).
cnf(c2829,plain,
product(e_2,e_3,e_4),
inference(resolution,[status(thm)],[c2798,c1733]) ).
cnf(c2837,plain,
( ~ product(e_2,X438,e_4)
| equalish(X438,e_3) ),
inference(resolution,[status(thm)],[c2829,product_right_cancellation]) ).
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(c3692,plain,
( ~ product(X597,e_4,e_2)
| equalish(X597,e_3) ),
inference(resolution,[status(thm)],[c3689,product_left_cancellation]) ).
cnf(c6,plain,
( ~ group_element(X38)
| product(X38,e_4,e_1)
| product(X38,e_4,e_2)
| product(X38,e_4,e_3)
| product(X38,e_4,e_4) ),
inference(resolution,[status(thm)],[product_total_function1,element_4]) ).
cnf(c26,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)],[c6,element_2]) ).
cnf(c1747,plain,
( ~ product(e_2,X249,e_3)
| equalish(X249,e_1) ),
inference(resolution,[status(thm)],[c1733,product_right_cancellation]) ).
cnf(c1762,plain,
( equalish(e_4,e_1)
| product(e_2,e_4,e_1)
| product(e_2,e_4,e_2)
| product(e_2,e_4,e_4) ),
inference(resolution,[status(thm)],[c1747,c26]) ).
cnf(c3715,plain,
( product(e_2,e_4,e_1)
| product(e_2,e_4,e_2)
| product(e_2,e_4,e_4) ),
inference(resolution,[status(thm)],[c1762,e_4_is_not_e_1]) ).
cnf(c3758,plain,
( product(e_2,e_4,e_1)
| product(e_2,e_4,e_4)
| equalish(e_2,e_3) ),
inference(resolution,[status(thm)],[c3715,c3692]) ).
cnf(c3801,plain,
( product(e_2,e_4,e_1)
| product(e_2,e_4,e_4) ),
inference(resolution,[status(thm)],[c3758,e_2_is_not_e_3]) ).
cnf(c3813,plain,
( product(e_2,e_4,e_1)
| equalish(e_4,e_3) ),
inference(resolution,[status(thm)],[c3801,c2837]) ).
cnf(c3832,plain,
product(e_2,e_4,e_1),
inference(resolution,[status(thm)],[c3813,e_4_is_not_e_3]) ).
cnf(c3837,plain,
( ~ product(X688,e_4,e_2)
| product(X688,e_2,e_1) ),
inference(resolution,[status(thm)],[c3832,qg3]) ).
cnf(c3898,plain,
product(e_3,e_2,e_1),
inference(resolution,[status(thm)],[c3837,c3689]) ).
cnf(c3907,plain,
( ~ product(X697,e_2,e_3)
| product(X697,e_3,e_1) ),
inference(resolution,[status(thm)],[c3898,qg3]) ).
cnf(c3935,plain,
product(e_4,e_3,e_1),
inference(resolution,[status(thm)],[c3907,c3645]) ).
cnf(c3939,plain,
( ~ product(e_4,X699,e_1)
| equalish(X699,e_3) ),
inference(resolution,[status(thm)],[c3935,product_right_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(c12,plain,
( product(e_4,e_4,e_1)
| product(e_4,e_4,e_2)
| product(e_4,e_4,e_3)
| product(e_4,e_4,e_4) ),
inference(resolution,[status(thm)],[c2,element_4]) ).
cnf(c181,plain,
( product(e_4,e_4,e_1)
| product(e_4,e_4,e_3)
| product(e_4,e_4,e_4)
| ~ product(e_4,X188,e_2)
| equalish(X188,e_4) ),
inference(resolution,[status(thm)],[c12,product_right_cancellation]) ).
cnf(c3653,plain,
( product(e_4,e_4,e_1)
| product(e_4,e_4,e_3)
| product(e_4,e_4,e_4)
| equalish(e_1,e_4) ),
inference(resolution,[status(thm)],[c3629,c181]) ).
cnf(c4419,plain,
( product(e_4,e_4,e_1)
| product(e_4,e_4,e_3)
| product(e_4,e_4,e_4) ),
inference(resolution,[status(thm)],[c3653,e_1_is_not_e_4]) ).
cnf(c4421,plain,
( product(e_4,e_4,e_3)
| product(e_4,e_4,e_4)
| equalish(e_4,e_3) ),
inference(resolution,[status(thm)],[c4419,c3939]) ).
cnf(c4495,plain,
( product(e_4,e_4,e_3)
| product(e_4,e_4,e_4) ),
inference(resolution,[status(thm)],[c4421,e_4_is_not_e_3]) ).
cnf(c4498,plain,
( product(e_4,e_4,e_4)
| equalish(e_4,e_2) ),
inference(resolution,[status(thm)],[c4495,c3660]) ).
cnf(c4536,plain,
product(e_4,e_4,e_4),
inference(resolution,[status(thm)],[c4498,e_4_is_not_e_2]) ).
cnf(c4544,plain,
( ~ product(e_4,e_4,X906)
| equalish(X906,e_4) ),
inference(resolution,[status(thm)],[c4536,product_total_function2]) ).
cnf(c4538,plain,
( ~ product(X905,e_4,e_4)
| equalish(X905,e_4) ),
inference(resolution,[status(thm)],[c4536,product_left_cancellation]) ).
cnf(c4537,plain,
( ~ product(e_4,X904,e_4)
| equalish(X904,e_4) ),
inference(resolution,[status(thm)],[c4536,product_right_cancellation]) ).
cnf(e_3_is_not_e_4,axiom,
~ equalish(e_3,e_4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_3_is_not_e_4) ).
cnf(c3690,plain,
( ~ product(e_3,X596,e_2)
| equalish(X596,e_4) ),
inference(resolution,[status(thm)],[c3689,product_right_cancellation]) ).
cnf(c3940,plain,
( ~ product(X700,e_3,e_1)
| equalish(X700,e_4) ),
inference(resolution,[status(thm)],[c3935,product_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(c11,plain,
( product(e_3,e_3,e_1)
| product(e_3,e_3,e_2)
| product(e_3,e_3,e_3)
| product(e_3,e_3,e_4) ),
inference(resolution,[status(thm)],[c2,element_3]) ).
cnf(c167,plain,
( product(e_3,e_3,e_1)
| product(e_3,e_3,e_2)
| product(e_3,e_3,e_3)
| ~ product(e_3,X166,e_4)
| equalish(X166,e_3) ),
inference(resolution,[status(thm)],[c11,product_right_cancellation]) ).
cnf(c2675,plain,
( product(e_3,e_3,e_3)
| product(e_3,e_3,e_1)
| product(e_3,e_3,e_2)
| equalish(e_1,e_3) ),
inference(resolution,[status(thm)],[c2661,c167]) ).
cnf(c4263,plain,
( product(e_3,e_3,e_3)
| product(e_3,e_3,e_1)
| product(e_3,e_3,e_2) ),
inference(resolution,[status(thm)],[c2675,e_1_is_not_e_3]) ).
cnf(c4284,plain,
( product(e_3,e_3,e_3)
| product(e_3,e_3,e_2)
| equalish(e_3,e_4) ),
inference(resolution,[status(thm)],[c4263,c3940]) ).
cnf(c4336,plain,
( product(e_3,e_3,e_3)
| equalish(e_3,e_4) ),
inference(resolution,[status(thm)],[c4284,c3690]) ).
cnf(c4355,plain,
product(e_3,e_3,e_3),
inference(resolution,[status(thm)],[c4336,e_3_is_not_e_4]) ).
cnf(c4364,plain,
( ~ product(e_3,e_3,X851)
| equalish(X851,e_3) ),
inference(resolution,[status(thm)],[c4355,product_total_function2]) ).
cnf(c4357,plain,
( ~ product(X849,e_3,e_3)
| equalish(X849,e_3) ),
inference(resolution,[status(thm)],[c4355,product_left_cancellation]) ).
cnf(c4356,plain,
( ~ product(e_3,X848,e_3)
| equalish(X848,e_3) ),
inference(resolution,[status(thm)],[c4355,product_right_cancellation]) ).
cnf(c3694,plain,
( ~ product(X601,e_4,e_3)
| product(X601,e_3,e_2) ),
inference(resolution,[status(thm)],[c3689,qg3]) ).
cnf(c3665,plain,
( ~ product(X600,e_2,e_4)
| product(X600,e_4,e_3) ),
inference(resolution,[status(thm)],[c3645,qg3]) ).
cnf(c10,plain,
( product(e_2,e_2,e_1)
| product(e_2,e_2,e_2)
| product(e_2,e_2,e_3)
| product(e_2,e_2,e_4) ),
inference(resolution,[status(thm)],[c2,element_2]) ).
cnf(c83,plain,
( product(e_2,e_2,e_1)
| product(e_2,e_2,e_2)
| product(e_2,e_2,e_4)
| ~ product(e_2,X122,e_3)
| equalish(X122,e_2) ),
inference(resolution,[status(thm)],[c10,product_right_cancellation]) ).
cnf(c1730,plain,
( equalish(e_1,e_2)
| product(e_2,e_2,e_1)
| product(e_2,e_2,e_2)
| product(e_2,e_2,e_4) ),
inference(resolution,[status(thm)],[c1703,c83]) ).
cnf(c2022,plain,
( product(e_2,e_2,e_1)
| product(e_2,e_2,e_2)
| product(e_2,e_2,e_4) ),
inference(resolution,[status(thm)],[c1730,e_1_is_not_e_2]) ).
cnf(c2096,plain,
( product(e_2,e_2,e_1)
| product(e_2,e_2,e_2)
| ~ product(e_2,X362,e_4)
| equalish(X362,e_2) ),
inference(resolution,[status(thm)],[c2022,product_right_cancellation]) ).
cnf(c2840,plain,
( product(e_2,e_2,e_1)
| product(e_2,e_2,e_2)
| equalish(e_3,e_2) ),
inference(resolution,[status(thm)],[c2829,c2096]) ).
cnf(c3057,plain,
( product(e_2,e_2,e_1)
| product(e_2,e_2,e_2) ),
inference(resolution,[status(thm)],[c2840,e_3_is_not_e_2]) ).
cnf(c3059,plain,
( product(e_2,e_2,e_2)
| ~ product(e_2,X487,e_1)
| equalish(X487,e_2) ),
inference(resolution,[status(thm)],[c3057,product_right_cancellation]) ).
cnf(c3833,plain,
( product(e_2,e_2,e_2)
| equalish(e_4,e_2) ),
inference(resolution,[status(thm)],[c3832,c3059]) ).
cnf(c3867,plain,
product(e_2,e_2,e_2),
inference(resolution,[status(thm)],[c3833,e_4_is_not_e_2]) ).
cnf(c3870,plain,
( ~ product(X685,e_2,e_2)
| equalish(X685,e_2) ),
inference(resolution,[status(thm)],[c3867,product_left_cancellation]) ).
cnf(c3661,plain,
( ~ product(X591,e_2,e_3)
| equalish(X591,e_4) ),
inference(resolution,[status(thm)],[c3645,product_left_cancellation]) ).
cnf(c4,plain,
( ~ group_element(X36)
| product(X36,e_2,e_1)
| product(X36,e_2,e_2)
| product(X36,e_2,e_3)
| product(X36,e_2,e_4) ),
inference(resolution,[status(thm)],[product_total_function1,element_2]) ).
cnf(c17,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)],[c4,element_1]) ).
cnf(c1776,plain,
( product(e_1,e_2,e_3)
| product(e_1,e_1,e_1) ),
inference(resolution,[status(thm)],[c1743,c1204]) ).
cnf(c1788,plain,
( product(e_1,e_2,e_3)
| ~ product(e_1,X296,e_1)
| equalish(X296,e_1) ),
inference(resolution,[status(thm)],[c1776,product_right_cancellation]) ).
cnf(c1865,plain,
( product(e_1,e_2,e_3)
| equalish(e_2,e_1)
| product(e_1,e_2,e_2)
| product(e_1,e_2,e_4) ),
inference(resolution,[status(thm)],[c1788,c17]) ).
cnf(c4008,plain,
( product(e_1,e_2,e_3)
| product(e_1,e_2,e_2)
| product(e_1,e_2,e_4) ),
inference(resolution,[status(thm)],[c1865,e_2_is_not_e_1]) ).
cnf(c4046,plain,
( product(e_1,e_2,e_2)
| product(e_1,e_2,e_4)
| equalish(e_1,e_4) ),
inference(resolution,[status(thm)],[c4008,c3661]) ).
cnf(c4113,plain,
( product(e_1,e_2,e_2)
| product(e_1,e_2,e_4) ),
inference(resolution,[status(thm)],[c4046,e_1_is_not_e_4]) ).
cnf(c4118,plain,
( product(e_1,e_2,e_4)
| equalish(e_1,e_2) ),
inference(resolution,[status(thm)],[c4113,c3870]) ).
cnf(c4156,plain,
product(e_1,e_2,e_4),
inference(resolution,[status(thm)],[c4118,e_1_is_not_e_2]) ).
cnf(c4165,plain,
product(e_1,e_4,e_3),
inference(resolution,[status(thm)],[c4156,c3665]) ).
cnf(c4181,plain,
product(e_1,e_3,e_2),
inference(resolution,[status(thm)],[c4165,c3694]) ).
cnf(c4192,plain,
( ~ product(X773,e_3,e_1)
| product(X773,e_1,e_2) ),
inference(resolution,[status(thm)],[c4181,qg3]) ).
cnf(c4179,plain,
( ~ product(X771,e_4,e_1)
| product(X771,e_1,e_3) ),
inference(resolution,[status(thm)],[c4165,qg3]) ).
cnf(c4163,plain,
( ~ product(X770,e_2,e_1)
| product(X770,e_1,e_4) ),
inference(resolution,[status(thm)],[c4156,qg3]) ).
cnf(c4194,plain,
( ~ product(e_1,e_3,X767)
| equalish(X767,e_2) ),
inference(resolution,[status(thm)],[c4181,product_total_function2]) ).
cnf(c4186,plain,
( ~ product(X766,e_3,e_2)
| equalish(X766,e_1) ),
inference(resolution,[status(thm)],[c4181,product_left_cancellation]) ).
cnf(c4185,plain,
( ~ product(e_1,X764,e_2)
| equalish(X764,e_3) ),
inference(resolution,[status(thm)],[c4181,product_right_cancellation]) ).
cnf(c4182,plain,
( ~ product(e_1,e_4,X763)
| equalish(X763,e_3) ),
inference(resolution,[status(thm)],[c4165,product_total_function2]) ).
cnf(c4176,plain,
( ~ product(X762,e_4,e_3)
| equalish(X762,e_1) ),
inference(resolution,[status(thm)],[c4165,product_left_cancellation]) ).
cnf(c4175,plain,
( ~ product(e_1,X760,e_3)
| equalish(X760,e_4) ),
inference(resolution,[status(thm)],[c4165,product_right_cancellation]) ).
cnf(c4166,plain,
( ~ product(e_1,e_2,X759)
| equalish(X759,e_4) ),
inference(resolution,[status(thm)],[c4156,product_total_function2]) ).
cnf(c4159,plain,
( ~ product(X757,e_2,e_4)
| equalish(X757,e_1) ),
inference(resolution,[status(thm)],[c4156,product_left_cancellation]) ).
cnf(c4158,plain,
( ~ product(e_1,X756,e_4)
| equalish(X756,e_2) ),
inference(resolution,[status(thm)],[c4156,product_right_cancellation]) ).
cnf(c3947,plain,
( ~ product(X703,e_3,e_4)
| product(X703,e_4,e_1) ),
inference(resolution,[status(thm)],[c3935,qg3]) ).
cnf(c3949,plain,
( ~ product(e_4,e_3,X701)
| equalish(X701,e_1) ),
inference(resolution,[status(thm)],[c3935,product_total_function2]) ).
cnf(c3910,plain,
( ~ product(e_3,e_2,X693)
| equalish(X693,e_1) ),
inference(resolution,[status(thm)],[c3898,product_total_function2]) ).
cnf(c3904,plain,
( ~ product(X692,e_2,e_1)
| equalish(X692,e_3) ),
inference(resolution,[status(thm)],[c3898,product_left_cancellation]) ).
cnf(c3902,plain,
( ~ product(e_3,X690,e_1)
| equalish(X690,e_2) ),
inference(resolution,[status(thm)],[c3898,product_right_cancellation]) ).
cnf(c3876,plain,
( ~ product(e_2,e_2,X687)
| equalish(X687,e_2) ),
inference(resolution,[status(thm)],[c3867,product_total_function2]) ).
cnf(c3869,plain,
( ~ product(e_2,X684,e_2)
| equalish(X684,e_2) ),
inference(resolution,[status(thm)],[c3867,product_right_cancellation]) ).
cnf(c3839,plain,
( ~ product(e_2,e_4,X680)
| equalish(X680,e_1) ),
inference(resolution,[status(thm)],[c3832,product_total_function2]) ).
cnf(c3835,plain,
( ~ product(X679,e_4,e_1)
| equalish(X679,e_2) ),
inference(resolution,[status(thm)],[c3832,product_left_cancellation]) ).
cnf(c3834,plain,
( ~ product(e_2,X677,e_1)
| equalish(X677,e_4) ),
inference(resolution,[status(thm)],[c3832,product_right_cancellation]) ).
cnf(c3696,plain,
( ~ product(e_3,e_4,X599)
| equalish(X599,e_2) ),
inference(resolution,[status(thm)],[c3689,product_total_function2]) ).
cnf(c3668,plain,
( ~ product(e_4,e_2,X592)
| equalish(X592,e_3) ),
inference(resolution,[status(thm)],[c3645,product_total_function2]) ).
cnf(c3655,plain,
( ~ product(e_4,e_1,X588)
| equalish(X588,e_2) ),
inference(resolution,[status(thm)],[c3629,product_total_function2]) ).
cnf(c3647,plain,
( ~ product(X587,e_1,e_2)
| equalish(X587,e_4) ),
inference(resolution,[status(thm)],[c3629,product_left_cancellation]) ).
cnf(c3646,plain,
( ~ product(e_4,X585,e_2)
| equalish(X585,e_1) ),
inference(resolution,[status(thm)],[c3629,product_right_cancellation]) ).
cnf(e_2_greater_e_1,axiom,
greater(e_2,e_1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_2_greater_e_1) ).
cnf(c3657,plain,
( ~ next(e_4,X583)
| ~ greater(e_2,X583) ),
inference(resolution,[status(thm)],[c3629,no_redundancy]) ).
cnf(c3676,plain,
~ next(e_4,e_1),
inference(resolution,[status(thm)],[c3657,e_2_greater_e_1]) ).
cnf(c3616,plain,
( ~ product(e_1,e_1,X577)
| equalish(X577,e_1) ),
inference(resolution,[status(thm)],[c3603,product_total_function2]) ).
cnf(c3606,plain,
( ~ product(e_1,X574,e_1)
| equalish(X574,e_1) ),
inference(resolution,[status(thm)],[c3603,product_right_cancellation]) ).
cnf(c3618,plain,
( ~ next(e_1,X572)
| ~ greater(e_1,X572) ),
inference(resolution,[status(thm)],[c3603,no_redundancy]) ).
cnf(c2841,plain,
( ~ product(X444,e_3,e_2)
| product(X444,e_2,e_4) ),
inference(resolution,[status(thm)],[c2829,qg3]) ).
cnf(c2843,plain,
( ~ product(e_2,e_3,X441)
| equalish(X441,e_4) ),
inference(resolution,[status(thm)],[c2829,product_total_function2]) ).
cnf(c2838,plain,
( ~ product(X440,e_3,e_4)
| equalish(X440,e_2) ),
inference(resolution,[status(thm)],[c2829,product_left_cancellation]) ).
cnf(c2802,plain,
( ~ product(e_3,e_1,X434)
| equalish(X434,e_4) ),
inference(resolution,[status(thm)],[c2786,product_total_function2]) ).
cnf(c2788,plain,
( ~ product(e_3,X431,e_4)
| equalish(X431,e_1) ),
inference(resolution,[status(thm)],[c2786,product_right_cancellation]) ).
cnf(c2807,plain,
( ~ next(e_3,X429)
| ~ greater(e_4,X429) ),
inference(resolution,[status(thm)],[c2786,no_redundancy]) ).
cnf(c2812,plain,
~ next(e_3,e_2),
inference(resolution,[status(thm)],[c2807,e_4_greater_e_2]) ).
cnf(e_4_greater_e_1,axiom,
greater(e_4,e_1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_4_greater_e_1) ).
cnf(c2811,plain,
~ next(e_3,e_1),
inference(resolution,[status(thm)],[c2807,e_4_greater_e_1]) ).
cnf(c2810,plain,
~ next(e_3,e_3),
inference(resolution,[status(thm)],[c2807,e_4_greater_e_3]) ).
cnf(c1741,plain,
( ~ product(e_2,e_1,X247)
| equalish(X247,e_3) ),
inference(resolution,[status(thm)],[c1733,product_total_function2]) ).
cnf(c1748,plain,
( ~ next(e_2,X244)
| ~ greater(e_3,X244) ),
inference(resolution,[status(thm)],[c1733,no_redundancy]) ).
cnf(c1753,plain,
~ next(e_2,e_2),
inference(resolution,[status(thm)],[c1748,e_3_greater_e_2]) ).
cnf(e_3_greater_e_1,axiom,
greater(e_3,e_1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_3_greater_e_1) ).
cnf(c1752,plain,
~ next(e_2,e_1),
inference(resolution,[status(thm)],[c1748,e_3_greater_e_1]) ).
cnf(c1,plain,
( ~ product(X20,X18,X19)
| equalish(X18,X18) ),
inference(factor,[status(thm)],[product_right_cancellation]) ).
cnf(c7,plain,
( ~ product(X26,X27,X25)
| equalish(X26,X26) ),
inference(factor,[status(thm)],[product_left_cancellation]) ).
cnf(c168,plain,
( product(e_4,e_4,e_2)
| product(e_4,e_4,e_3)
| product(e_4,e_4,e_4)
| equalish(e_4,e_4) ),
inference(resolution,[status(thm)],[c12,c7]) ).
cnf(c1000,plain,
( product(e_4,e_4,e_3)
| product(e_4,e_4,e_4)
| equalish(e_4,e_4) ),
inference(resolution,[status(thm)],[c168,c1]) ).
cnf(c1022,plain,
( product(e_4,e_4,e_4)
| equalish(e_4,e_4) ),
inference(resolution,[status(thm)],[c1000,c1]) ).
cnf(c1037,plain,
equalish(e_4,e_4),
inference(resolution,[status(thm)],[c1022,c1]) ).
cnf(c139,plain,
( product(e_3,e_3,e_2)
| product(e_3,e_3,e_3)
| product(e_3,e_3,e_4)
| equalish(e_3,e_3) ),
inference(resolution,[status(thm)],[c11,c7]) ).
cnf(c887,plain,
( product(e_3,e_3,e_3)
| product(e_3,e_3,e_4)
| equalish(e_3,e_3) ),
inference(resolution,[status(thm)],[c139,c7]) ).
cnf(c909,plain,
( product(e_3,e_3,e_4)
| equalish(e_3,e_3) ),
inference(resolution,[status(thm)],[c887,c7]) ).
cnf(c924,plain,
equalish(e_3,e_3),
inference(resolution,[status(thm)],[c909,c7]) ).
cnf(c62,plain,
( product(e_2,e_2,e_2)
| product(e_2,e_2,e_3)
| product(e_2,e_2,e_4)
| equalish(e_2,e_2) ),
inference(resolution,[status(thm)],[c10,c7]) ).
cnf(c692,plain,
( product(e_2,e_2,e_3)
| product(e_2,e_2,e_4)
| equalish(e_2,e_2) ),
inference(resolution,[status(thm)],[c62,c7]) ).
cnf(c714,plain,
( product(e_2,e_2,e_4)
| equalish(e_2,e_2) ),
inference(resolution,[status(thm)],[c692,c7]) ).
cnf(c739,plain,
equalish(e_2,e_2),
inference(resolution,[status(thm)],[c714,c7]) ).
cnf(c29,plain,
( product(e_1,e_1,e_2)
| product(e_1,e_1,e_3)
| product(e_1,e_1,e_4)
| equalish(e_1,e_1) ),
inference(resolution,[status(thm)],[c9,c7]) ).
cnf(c91,plain,
( product(e_1,e_1,e_3)
| product(e_1,e_1,e_4)
| equalish(e_1,e_1) ),
inference(resolution,[status(thm)],[c29,c7]) ).
cnf(c115,plain,
( product(e_1,e_1,e_4)
| equalish(e_1,e_1) ),
inference(resolution,[status(thm)],[c91,c7]) ).
cnf(c131,plain,
equalish(e_1,e_1),
inference(resolution,[status(thm)],[c115,c7]) ).
cnf(c5,plain,
( ~ group_element(X37)
| product(X37,e_3,e_1)
| product(X37,e_3,e_2)
| product(X37,e_3,e_3)
| product(X37,e_3,e_4) ),
inference(resolution,[status(thm)],[product_total_function1,element_3]) ).
cnf(c0,plain,
( ~ product(X11,X10,X9)
| equalish(X9,X9) ),
inference(factor,[status(thm)],[product_total_function2]) ).
cnf(e_2_is_not_e_4,axiom,
~ equalish(e_2,e_4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_2_is_not_e_4) ).
cnf(e_3_then_e_4,axiom,
next(e_3,e_4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_3_then_e_4) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : GRP128-2.004 : TPTP v8.1.2. Released v1.2.0.
% 0.11/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.12/0.33 % Computer : n008.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Thu May 9 03:58:38 EDT 2024
% 0.12/0.34 % CPUTime :
% 5.81/6.07 % Version: 1.5
% 5.81/6.07 % SZS status Satisfiable
% 5.81/6.07 % SZS output start Saturation
% See solution above
% 5.91/6.07
% 5.91/6.07 % Initial clauses : 31
% 5.91/6.07 % Processed clauses : 535
% 5.91/6.07 % Factors computed : 5
% 5.91/6.07 % Resolvents computed: 4546
% 5.91/6.07 % Tautologies deleted: 56
% 5.91/6.07 % Forward subsumed : 3991
% 5.91/6.07 % Backward subsumed : 405
% 5.91/6.07 % -------- CPU Time ---------
% 5.91/6.07 % User time : 5.719 s
% 5.91/6.07 % System time : 0.015 s
% 5.91/6.07 % Total time : 5.734 s
%------------------------------------------------------------------------------