%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GRP127-2.005 : TPTP v8.1.2. Released v1.2.0.
% 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:09 EDT 2024
% Result : Satisfiable 59.02s 59.25s
% Output : Saturation 59.02s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(qg3,negated_conjecture,
( ~ product(X35,X34,X37)
| ~ product(X37,X35,X36)
| product(X36,X35,X34) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',qg3) ).
cnf(e_5_is_not_e_4,axiom,
~ equalish(e_5,e_4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_5_is_not_e_4) ).
cnf(product_right_cancellation,axiom,
( ~ product(X19,X21,X22)
| ~ product(X19,X20,X22)
| equalish(X21,X20) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',product_right_cancellation) ).
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(product_idempotence,axiom,
product(X2,X2,X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',product_idempotence) ).
cnf(c12,plain,
( ~ product(X27,X28,X27)
| equalish(X28,X27) ),
inference(resolution,[status(thm)],[product_right_cancellation,product_idempotence]) ).
cnf(e_2_is_not_e_3,axiom,
~ equalish(e_2,e_3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_2_is_not_e_3) ).
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(product_left_cancellation,axiom,
( ~ product(X32,X33,X30)
| ~ product(X31,X33,X30)
| equalish(X32,X31) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',product_left_cancellation) ).
cnf(c15,plain,
( ~ product(X42,X41,X41)
| equalish(X42,X41) ),
inference(resolution,[status(thm)],[product_left_cancellation,product_idempotence]) ).
cnf(element_3,axiom,
group_element(e_3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',element_3) ).
cnf(element_2,axiom,
group_element(e_2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',element_2) ).
cnf(product_total_function1,axiom,
( ~ group_element(X6)
| ~ group_element(X7)
| product(X6,X7,e_1)
| product(X6,X7,e_2)
| product(X6,X7,e_3)
| product(X6,X7,e_4)
| product(X6,X7,e_5) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',product_total_function1) ).
cnf(c2,plain,
( ~ group_element(X49)
| product(X49,e_2,e_1)
| product(X49,e_2,e_2)
| product(X49,e_2,e_3)
| product(X49,e_2,e_4)
| product(X49,e_2,e_5) ),
inference(resolution,[status(thm)],[product_total_function1,element_2]) ).
cnf(c29,plain,
( product(e_3,e_2,e_1)
| product(e_3,e_2,e_2)
| product(e_3,e_2,e_3)
| product(e_3,e_2,e_4)
| product(e_3,e_2,e_5) ),
inference(resolution,[status(thm)],[c2,element_3]) ).
cnf(c200,plain,
( product(e_3,e_2,e_1)
| product(e_3,e_2,e_3)
| product(e_3,e_2,e_4)
| product(e_3,e_2,e_5)
| equalish(e_3,e_2) ),
inference(resolution,[status(thm)],[c29,c15]) ).
cnf(c899,plain,
( product(e_3,e_2,e_1)
| product(e_3,e_2,e_3)
| product(e_3,e_2,e_4)
| product(e_3,e_2,e_5) ),
inference(resolution,[status(thm)],[c200,e_3_is_not_e_2]) ).
cnf(c908,plain,
( product(e_3,e_2,e_1)
| product(e_3,e_2,e_4)
| product(e_3,e_2,e_5)
| equalish(e_2,e_3) ),
inference(resolution,[status(thm)],[c899,c12]) ).
cnf(c945,plain,
( product(e_3,e_2,e_1)
| product(e_3,e_2,e_4)
| product(e_3,e_2,e_5) ),
inference(resolution,[status(thm)],[c908,e_2_is_not_e_3]) ).
cnf(c947,plain,
( product(e_3,e_2,e_4)
| product(e_3,e_2,e_5)
| ~ product(e_2,X191,e_3)
| product(e_1,e_2,X191) ),
inference(resolution,[status(thm)],[c945,qg3]) ).
cnf(e_2_then_e_3,axiom,
next(e_2,e_3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_2_then_e_3) ).
cnf(e_5_greater_e_3,axiom,
greater(e_5,e_3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_5_greater_e_3) ).
cnf(no_redundancy,axiom,
( ~ product(X3,e_1,X4)
| ~ next(X3,X5)
| ~ greater(X4,X5) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',no_redundancy) ).
cnf(e_4_greater_e_3,axiom,
greater(e_4,e_3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_4_greater_e_3) ).
cnf(element_1,axiom,
group_element(e_1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',element_1) ).
cnf(c5,plain,
( ~ group_element(X52)
| product(X52,e_1,e_1)
| product(X52,e_1,e_2)
| product(X52,e_1,e_3)
| product(X52,e_1,e_4)
| product(X52,e_1,e_5) ),
inference(resolution,[status(thm)],[product_total_function1,element_1]) ).
cnf(c40,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)
| product(e_2,e_1,e_5) ),
inference(resolution,[status(thm)],[c5,element_2]) ).
cnf(c497,plain,
( product(e_2,e_1,e_2)
| product(e_2,e_1,e_3)
| product(e_2,e_1,e_4)
| product(e_2,e_1,e_5)
| equalish(e_2,e_1) ),
inference(resolution,[status(thm)],[c40,c15]) ).
cnf(c3120,plain,
( product(e_2,e_1,e_2)
| product(e_2,e_1,e_3)
| product(e_2,e_1,e_4)
| product(e_2,e_1,e_5) ),
inference(resolution,[status(thm)],[c497,e_2_is_not_e_1]) ).
cnf(c3126,plain,
( product(e_2,e_1,e_3)
| product(e_2,e_1,e_4)
| product(e_2,e_1,e_5)
| equalish(e_1,e_2) ),
inference(resolution,[status(thm)],[c3120,c12]) ).
cnf(c3184,plain,
( product(e_2,e_1,e_3)
| product(e_2,e_1,e_4)
| product(e_2,e_1,e_5) ),
inference(resolution,[status(thm)],[c3126,e_1_is_not_e_2]) ).
cnf(c3198,plain,
( product(e_2,e_1,e_3)
| product(e_2,e_1,e_5)
| ~ next(e_2,X633)
| ~ greater(e_4,X633) ),
inference(resolution,[status(thm)],[c3184,no_redundancy]) ).
cnf(c3216,plain,
( product(e_2,e_1,e_3)
| product(e_2,e_1,e_5)
| ~ next(e_2,e_3) ),
inference(resolution,[status(thm)],[c3198,e_4_greater_e_3]) ).
cnf(c3218,plain,
( product(e_2,e_1,e_3)
| product(e_2,e_1,e_5) ),
inference(resolution,[status(thm)],[c3216,e_2_then_e_3]) ).
cnf(c3233,plain,
( product(e_2,e_1,e_3)
| ~ next(e_2,X637)
| ~ greater(e_5,X637) ),
inference(resolution,[status(thm)],[c3218,no_redundancy]) ).
cnf(c3241,plain,
( product(e_2,e_1,e_3)
| ~ next(e_2,e_3) ),
inference(resolution,[status(thm)],[c3233,e_5_greater_e_3]) ).
cnf(c3244,plain,
product(e_2,e_1,e_3),
inference(resolution,[status(thm)],[c3241,e_2_then_e_3]) ).
cnf(c3247,plain,
( product(e_3,e_2,e_4)
| product(e_3,e_2,e_5)
| product(e_1,e_2,e_1) ),
inference(resolution,[status(thm)],[c3244,c947]) ).
cnf(c3595,plain,
( product(e_3,e_2,e_4)
| product(e_3,e_2,e_5)
| equalish(e_2,e_1) ),
inference(resolution,[status(thm)],[c3247,c12]) ).
cnf(c3627,plain,
( product(e_3,e_2,e_4)
| product(e_3,e_2,e_5) ),
inference(resolution,[status(thm)],[c3595,e_2_is_not_e_1]) ).
cnf(c3630,plain,
( product(e_3,e_2,e_5)
| ~ product(e_3,X693,e_4)
| equalish(X693,e_2) ),
inference(resolution,[status(thm)],[c3627,product_right_cancellation]) ).
cnf(c3254,plain,
( ~ product(e_1,X642,e_2)
| product(e_3,e_1,X642) ),
inference(resolution,[status(thm)],[c3244,qg3]) ).
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_1,axiom,
~ equalish(e_4,e_1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_4_is_not_e_1) ).
cnf(element_4,axiom,
group_element(e_4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',element_4) ).
cnf(c3,plain,
( ~ group_element(X50)
| product(X50,e_4,e_1)
| product(X50,e_4,e_2)
| product(X50,e_4,e_3)
| product(X50,e_4,e_4)
| product(X50,e_4,e_5) ),
inference(resolution,[status(thm)],[product_total_function1,element_4]) ).
cnf(c33,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)
| product(e_1,e_4,e_5) ),
inference(resolution,[status(thm)],[c3,element_1]) ).
cnf(c279,plain,
( product(e_1,e_4,e_2)
| product(e_1,e_4,e_3)
| product(e_1,e_4,e_4)
| product(e_1,e_4,e_5)
| equalish(e_4,e_1) ),
inference(resolution,[status(thm)],[c33,c12]) ).
cnf(c1297,plain,
( product(e_1,e_4,e_2)
| product(e_1,e_4,e_3)
| product(e_1,e_4,e_4)
| product(e_1,e_4,e_5) ),
inference(resolution,[status(thm)],[c279,e_4_is_not_e_1]) ).
cnf(c1312,plain,
( product(e_1,e_4,e_2)
| product(e_1,e_4,e_3)
| product(e_1,e_4,e_5)
| equalish(e_1,e_4) ),
inference(resolution,[status(thm)],[c1297,c15]) ).
cnf(c1340,plain,
( product(e_1,e_4,e_2)
| product(e_1,e_4,e_3)
| product(e_1,e_4,e_5) ),
inference(resolution,[status(thm)],[c1312,e_1_is_not_e_4]) ).
cnf(c1355,plain,
( product(e_1,e_4,e_2)
| product(e_1,e_4,e_3)
| ~ product(X331,e_4,e_5)
| equalish(X331,e_1) ),
inference(resolution,[status(thm)],[c1340,product_left_cancellation]) ).
cnf(e_4_is_not_e_3,axiom,
~ equalish(e_4,e_3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_4_is_not_e_3) ).
cnf(product_total_function2,axiom,
( ~ product(X9,X12,X11)
| ~ product(X9,X12,X10)
| equalish(X11,X10) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',product_total_function2) ).
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(e_4_is_not_e_5,axiom,
~ equalish(e_4,e_5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_4_is_not_e_5) ).
cnf(c3653,plain,
( product(e_3,e_2,e_4)
| ~ product(e_2,X712,e_3)
| product(e_5,e_2,X712) ),
inference(resolution,[status(thm)],[c3627,qg3]) ).
cnf(c3784,plain,
( product(e_3,e_2,e_4)
| product(e_5,e_2,e_1) ),
inference(resolution,[status(thm)],[c3653,c3244]) ).
cnf(c3807,plain,
( product(e_3,e_2,e_4)
| ~ product(X719,e_2,e_1)
| equalish(X719,e_5) ),
inference(resolution,[status(thm)],[c3784,product_left_cancellation]) ).
cnf(e_3_is_not_e_4,axiom,
~ equalish(e_3,e_4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_3_is_not_e_4) ).
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(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(c26,plain,
( product(e_4,e_2,e_1)
| product(e_4,e_2,e_2)
| product(e_4,e_2,e_3)
| product(e_4,e_2,e_4)
| product(e_4,e_2,e_5) ),
inference(resolution,[status(thm)],[c2,element_4]) ).
cnf(c55,plain,
( product(e_4,e_2,e_1)
| product(e_4,e_2,e_3)
| product(e_4,e_2,e_4)
| product(e_4,e_2,e_5)
| equalish(e_4,e_2) ),
inference(resolution,[status(thm)],[c26,c15]) ).
cnf(c91,plain,
( product(e_4,e_2,e_1)
| product(e_4,e_2,e_3)
| product(e_4,e_2,e_4)
| product(e_4,e_2,e_5) ),
inference(resolution,[status(thm)],[c55,e_4_is_not_e_2]) ).
cnf(c105,plain,
( product(e_4,e_2,e_1)
| product(e_4,e_2,e_3)
| product(e_4,e_2,e_5)
| equalish(e_2,e_4) ),
inference(resolution,[status(thm)],[c91,c12]) ).
cnf(c122,plain,
( product(e_4,e_2,e_1)
| product(e_4,e_2,e_3)
| product(e_4,e_2,e_5) ),
inference(resolution,[status(thm)],[c105,e_2_is_not_e_4]) ).
cnf(c132,plain,
( product(e_4,e_2,e_1)
| product(e_4,e_2,e_3)
| ~ product(X60,e_2,e_5)
| equalish(X60,e_4) ),
inference(resolution,[status(thm)],[c122,product_left_cancellation]) ).
cnf(c3638,plain,
( product(e_3,e_2,e_5)
| ~ product(e_2,X701,e_3)
| product(e_4,e_2,X701) ),
inference(resolution,[status(thm)],[c3627,qg3]) ).
cnf(c3695,plain,
( product(e_3,e_2,e_5)
| product(e_4,e_2,e_1) ),
inference(resolution,[status(thm)],[c3638,c3244]) ).
cnf(c3700,plain,
( product(e_4,e_2,e_1)
| product(e_4,e_2,e_3)
| equalish(e_3,e_4) ),
inference(resolution,[status(thm)],[c3695,c132]) ).
cnf(c3917,plain,
( product(e_4,e_2,e_1)
| product(e_4,e_2,e_3) ),
inference(resolution,[status(thm)],[c3700,e_3_is_not_e_4]) ).
cnf(c3938,plain,
( product(e_4,e_2,e_3)
| product(e_3,e_2,e_4)
| equalish(e_4,e_5) ),
inference(resolution,[status(thm)],[c3917,c3807]) ).
cnf(c4274,plain,
( product(e_4,e_2,e_3)
| product(e_3,e_2,e_4) ),
inference(resolution,[status(thm)],[c3938,e_4_is_not_e_5]) ).
cnf(c4305,plain,
( product(e_4,e_2,e_3)
| ~ product(e_3,e_2,X767)
| equalish(X767,e_4) ),
inference(resolution,[status(thm)],[c4274,product_total_function2]) ).
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(c3631,plain,
( product(e_3,e_2,e_5)
| ~ product(X694,e_2,e_4)
| equalish(X694,e_3) ),
inference(resolution,[status(thm)],[c3627,product_left_cancellation]) ).
cnf(c28,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)
| product(e_1,e_2,e_5) ),
inference(resolution,[status(thm)],[c2,element_1]) ).
cnf(c170,plain,
( product(e_1,e_2,e_2)
| product(e_1,e_2,e_3)
| product(e_1,e_2,e_4)
| product(e_1,e_2,e_5)
| equalish(e_2,e_1) ),
inference(resolution,[status(thm)],[c28,c12]) ).
cnf(c774,plain,
( product(e_1,e_2,e_2)
| product(e_1,e_2,e_3)
| product(e_1,e_2,e_4)
| product(e_1,e_2,e_5) ),
inference(resolution,[status(thm)],[c170,e_2_is_not_e_1]) ).
cnf(c777,plain,
( product(e_1,e_2,e_3)
| product(e_1,e_2,e_4)
| product(e_1,e_2,e_5)
| equalish(e_1,e_2) ),
inference(resolution,[status(thm)],[c774,c15]) ).
cnf(c812,plain,
( product(e_1,e_2,e_3)
| product(e_1,e_2,e_4)
| product(e_1,e_2,e_5) ),
inference(resolution,[status(thm)],[c777,e_1_is_not_e_2]) ).
cnf(c814,plain,
( product(e_1,e_2,e_4)
| product(e_1,e_2,e_5)
| ~ product(e_2,X144,e_1)
| product(e_3,e_2,X144) ),
inference(resolution,[status(thm)],[c812,qg3]) ).
cnf(e_1_is_not_e_5,axiom,
~ equalish(e_1,e_5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_1_is_not_e_5) ).
cnf(e_2_is_not_e_5,axiom,
~ equalish(e_2,e_5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_2_is_not_e_5) ).
cnf(e_5_is_not_e_2,axiom,
~ equalish(e_5,e_2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_5_is_not_e_2) ).
cnf(element_5,axiom,
group_element(e_5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',element_5) ).
cnf(c4,plain,
( ~ group_element(X51)
| product(X51,e_5,e_1)
| product(X51,e_5,e_2)
| product(X51,e_5,e_3)
| product(X51,e_5,e_4)
| product(X51,e_5,e_5) ),
inference(resolution,[status(thm)],[product_total_function1,element_5]) ).
cnf(c35,plain,
( product(e_2,e_5,e_1)
| product(e_2,e_5,e_2)
| product(e_2,e_5,e_3)
| product(e_2,e_5,e_4)
| product(e_2,e_5,e_5) ),
inference(resolution,[status(thm)],[c4,element_2]) ).
cnf(c329,plain,
( product(e_2,e_5,e_1)
| product(e_2,e_5,e_3)
| product(e_2,e_5,e_4)
| product(e_2,e_5,e_5)
| equalish(e_5,e_2) ),
inference(resolution,[status(thm)],[c35,c12]) ).
cnf(c1641,plain,
( product(e_2,e_5,e_1)
| product(e_2,e_5,e_3)
| product(e_2,e_5,e_4)
| product(e_2,e_5,e_5) ),
inference(resolution,[status(thm)],[c329,e_5_is_not_e_2]) ).
cnf(c1673,plain,
( product(e_2,e_5,e_1)
| product(e_2,e_5,e_3)
| product(e_2,e_5,e_4)
| equalish(e_2,e_5) ),
inference(resolution,[status(thm)],[c1641,c15]) ).
cnf(c1697,plain,
( product(e_2,e_5,e_1)
| product(e_2,e_5,e_3)
| product(e_2,e_5,e_4) ),
inference(resolution,[status(thm)],[c1673,e_2_is_not_e_5]) ).
cnf(c1709,plain,
( product(e_2,e_5,e_1)
| product(e_2,e_5,e_4)
| ~ product(e_2,X416,e_3)
| equalish(X416,e_5) ),
inference(resolution,[status(thm)],[c1697,product_right_cancellation]) ).
cnf(c3248,plain,
( product(e_2,e_5,e_1)
| product(e_2,e_5,e_4)
| equalish(e_1,e_5) ),
inference(resolution,[status(thm)],[c3244,c1709]) ).
cnf(c3372,plain,
( product(e_2,e_5,e_1)
| product(e_2,e_5,e_4) ),
inference(resolution,[status(thm)],[c3248,e_1_is_not_e_5]) ).
cnf(c3726,plain,
( product(e_3,e_2,e_5)
| ~ product(e_2,X741,e_4)
| product(e_1,e_2,X741) ),
inference(resolution,[status(thm)],[c3695,qg3]) ).
cnf(c4102,plain,
( product(e_3,e_2,e_5)
| product(e_1,e_2,e_5)
| product(e_2,e_5,e_1) ),
inference(resolution,[status(thm)],[c3726,c3372]) ).
cnf(c4994,plain,
( product(e_3,e_2,e_5)
| product(e_1,e_2,e_5)
| product(e_1,e_2,e_4) ),
inference(resolution,[status(thm)],[c4102,c814]) ).
cnf(c5573,plain,
( product(e_3,e_2,e_5)
| product(e_1,e_2,e_5)
| equalish(e_1,e_3) ),
inference(resolution,[status(thm)],[c4994,c3631]) ).
cnf(c5605,plain,
( product(e_3,e_2,e_5)
| product(e_1,e_2,e_5) ),
inference(resolution,[status(thm)],[c5573,e_1_is_not_e_3]) ).
cnf(c5622,plain,
( product(e_1,e_2,e_5)
| product(e_4,e_2,e_3)
| equalish(e_5,e_4) ),
inference(resolution,[status(thm)],[c5605,c4305]) ).
cnf(c5999,plain,
( product(e_1,e_2,e_5)
| product(e_4,e_2,e_3) ),
inference(resolution,[status(thm)],[c5622,e_5_is_not_e_4]) ).
cnf(c6008,plain,
( product(e_4,e_2,e_3)
| ~ product(X859,e_2,e_5)
| equalish(X859,e_1) ),
inference(resolution,[status(thm)],[c5999,product_left_cancellation]) ).
cnf(c3717,plain,
( product(e_3,e_2,e_5)
| ~ product(X708,e_2,e_1)
| equalish(X708,e_4) ),
inference(resolution,[status(thm)],[c3695,product_left_cancellation]) ).
cnf(e_3_is_not_e_5,axiom,
~ equalish(e_3,e_5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_3_is_not_e_5) ).
cnf(c27,plain,
( product(e_5,e_2,e_1)
| product(e_5,e_2,e_2)
| product(e_5,e_2,e_3)
| product(e_5,e_2,e_4)
| product(e_5,e_2,e_5) ),
inference(resolution,[status(thm)],[c2,element_5]) ).
cnf(c140,plain,
( product(e_5,e_2,e_1)
| product(e_5,e_2,e_3)
| product(e_5,e_2,e_4)
| product(e_5,e_2,e_5)
| equalish(e_5,e_2) ),
inference(resolution,[status(thm)],[c27,c15]) ).
cnf(c419,plain,
( product(e_5,e_2,e_1)
| product(e_5,e_2,e_3)
| product(e_5,e_2,e_4)
| product(e_5,e_2,e_5) ),
inference(resolution,[status(thm)],[c140,e_5_is_not_e_2]) ).
cnf(c460,plain,
( product(e_5,e_2,e_1)
| product(e_5,e_2,e_3)
| product(e_5,e_2,e_4)
| equalish(e_2,e_5) ),
inference(resolution,[status(thm)],[c419,c12]) ).
cnf(c478,plain,
( product(e_5,e_2,e_1)
| product(e_5,e_2,e_3)
| product(e_5,e_2,e_4) ),
inference(resolution,[status(thm)],[c460,e_2_is_not_e_5]) ).
cnf(c491,plain,
( product(e_5,e_2,e_1)
| product(e_5,e_2,e_3)
| ~ product(X101,e_2,e_4)
| equalish(X101,e_5) ),
inference(resolution,[status(thm)],[c478,product_left_cancellation]) ).
cnf(c3792,plain,
( product(e_5,e_2,e_1)
| product(e_5,e_2,e_3)
| equalish(e_3,e_5) ),
inference(resolution,[status(thm)],[c3784,c491]) ).
cnf(c4149,plain,
( product(e_5,e_2,e_1)
| product(e_5,e_2,e_3) ),
inference(resolution,[status(thm)],[c3792,e_3_is_not_e_5]) ).
cnf(c4153,plain,
( product(e_5,e_2,e_3)
| product(e_3,e_2,e_5)
| equalish(e_5,e_4) ),
inference(resolution,[status(thm)],[c4149,c3717]) ).
cnf(c4395,plain,
( product(e_5,e_2,e_3)
| product(e_3,e_2,e_5) ),
inference(resolution,[status(thm)],[c4153,e_5_is_not_e_4]) ).
cnf(c4414,plain,
( product(e_3,e_2,e_5)
| ~ product(e_5,e_2,X783)
| equalish(X783,e_3) ),
inference(resolution,[status(thm)],[c4395,product_total_function2]) ).
cnf(c30,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)
| product(e_2,e_4,e_5) ),
inference(resolution,[status(thm)],[c3,element_2]) ).
cnf(c236,plain,
( product(e_2,e_4,e_1)
| product(e_2,e_4,e_3)
| product(e_2,e_4,e_4)
| product(e_2,e_4,e_5)
| equalish(e_4,e_2) ),
inference(resolution,[status(thm)],[c30,c12]) ).
cnf(c1035,plain,
( product(e_2,e_4,e_1)
| product(e_2,e_4,e_3)
| product(e_2,e_4,e_4)
| product(e_2,e_4,e_5) ),
inference(resolution,[status(thm)],[c236,e_4_is_not_e_2]) ).
cnf(c1054,plain,
( product(e_2,e_4,e_1)
| product(e_2,e_4,e_3)
| product(e_2,e_4,e_5)
| equalish(e_2,e_4) ),
inference(resolution,[status(thm)],[c1035,c15]) ).
cnf(c1086,plain,
( product(e_2,e_4,e_1)
| product(e_2,e_4,e_3)
| product(e_2,e_4,e_5) ),
inference(resolution,[status(thm)],[c1054,e_2_is_not_e_4]) ).
cnf(c1094,plain,
( product(e_2,e_4,e_1)
| product(e_2,e_4,e_5)
| ~ product(e_2,X230,e_3)
| equalish(X230,e_4) ),
inference(resolution,[status(thm)],[c1086,product_right_cancellation]) ).
cnf(c3245,plain,
( product(e_2,e_4,e_1)
| product(e_2,e_4,e_5)
| equalish(e_1,e_4) ),
inference(resolution,[status(thm)],[c3244,c1094]) ).
cnf(c3300,plain,
( product(e_2,e_4,e_1)
| product(e_2,e_4,e_5) ),
inference(resolution,[status(thm)],[c3245,e_1_is_not_e_4]) ).
cnf(c5635,plain,
( product(e_3,e_2,e_5)
| ~ product(e_2,X866,e_1)
| product(e_5,e_2,X866) ),
inference(resolution,[status(thm)],[c5605,qg3]) ).
cnf(c6115,plain,
( product(e_3,e_2,e_5)
| product(e_5,e_2,e_4)
| product(e_2,e_4,e_5) ),
inference(resolution,[status(thm)],[c5635,c3300]) ).
cnf(c6847,plain,
( product(e_3,e_2,e_5)
| product(e_2,e_4,e_5)
| equalish(e_4,e_3) ),
inference(resolution,[status(thm)],[c6115,c4414]) ).
cnf(c6935,plain,
( product(e_3,e_2,e_5)
| product(e_2,e_4,e_5) ),
inference(resolution,[status(thm)],[c6847,e_4_is_not_e_3]) ).
cnf(c6953,plain,
( product(e_2,e_4,e_5)
| product(e_4,e_2,e_3)
| equalish(e_3,e_1) ),
inference(resolution,[status(thm)],[c6935,c6008]) ).
cnf(c7388,plain,
( product(e_2,e_4,e_5)
| product(e_4,e_2,e_3) ),
inference(resolution,[status(thm)],[c6953,e_3_is_not_e_1]) ).
cnf(c7440,plain,
( product(e_2,e_4,e_5)
| ~ product(e_4,e_2,X1007)
| equalish(X1007,e_3) ),
inference(resolution,[status(thm)],[c7388,product_total_function2]) ).
cnf(c3648,plain,
( product(e_3,e_2,e_4)
| ~ product(X699,e_2,e_5)
| equalish(X699,e_3) ),
inference(resolution,[status(thm)],[c3627,product_left_cancellation]) ).
cnf(c816,plain,
( product(e_1,e_2,e_4)
| product(e_1,e_2,e_5)
| ~ product(X133,e_2,e_3)
| equalish(X133,e_1) ),
inference(resolution,[status(thm)],[c812,product_left_cancellation]) ).
cnf(c6021,plain,
( product(e_1,e_2,e_5)
| product(e_1,e_2,e_4)
| equalish(e_4,e_1) ),
inference(resolution,[status(thm)],[c5999,c816]) ).
cnf(c6175,plain,
( product(e_1,e_2,e_5)
| product(e_1,e_2,e_4) ),
inference(resolution,[status(thm)],[c6021,e_4_is_not_e_1]) ).
cnf(c6185,plain,
( product(e_1,e_2,e_4)
| product(e_3,e_2,e_4)
| equalish(e_1,e_3) ),
inference(resolution,[status(thm)],[c6175,c3648]) ).
cnf(c6453,plain,
( product(e_1,e_2,e_4)
| product(e_3,e_2,e_4) ),
inference(resolution,[status(thm)],[c6185,e_1_is_not_e_3]) ).
cnf(c6485,plain,
( product(e_1,e_2,e_4)
| ~ product(e_3,e_2,X918)
| equalish(X918,e_4) ),
inference(resolution,[status(thm)],[c6453,product_total_function2]) ).
cnf(c6942,plain,
( product(e_2,e_4,e_5)
| product(e_1,e_2,e_4)
| equalish(e_5,e_4) ),
inference(resolution,[status(thm)],[c6935,c6485]) ).
cnf(c7074,plain,
( product(e_2,e_4,e_5)
| product(e_1,e_2,e_4) ),
inference(resolution,[status(thm)],[c6942,e_5_is_not_e_4]) ).
cnf(c7119,plain,
( product(e_2,e_4,e_5)
| ~ product(e_2,X1024,e_1)
| product(e_4,e_2,X1024) ),
inference(resolution,[status(thm)],[c7074,qg3]) ).
cnf(c7866,plain,
( product(e_2,e_4,e_5)
| product(e_4,e_2,e_4) ),
inference(resolution,[status(thm)],[c7119,c3300]) ).
cnf(c7903,plain,
( product(e_2,e_4,e_5)
| equalish(e_4,e_3) ),
inference(resolution,[status(thm)],[c7866,c7440]) ).
cnf(c7959,plain,
product(e_2,e_4,e_5),
inference(resolution,[status(thm)],[c7903,e_4_is_not_e_3]) ).
cnf(c7991,plain,
( product(e_1,e_4,e_2)
| product(e_1,e_4,e_3)
| equalish(e_2,e_1) ),
inference(resolution,[status(thm)],[c7959,c1355]) ).
cnf(c9107,plain,
( product(e_1,e_4,e_2)
| product(e_1,e_4,e_3) ),
inference(resolution,[status(thm)],[c7991,e_2_is_not_e_1]) ).
cnf(c9118,plain,
( product(e_1,e_4,e_3)
| product(e_3,e_1,e_4) ),
inference(resolution,[status(thm)],[c9107,c3254]) ).
cnf(c9148,plain,
( product(e_1,e_4,e_3)
| product(e_3,e_2,e_5)
| equalish(e_1,e_2) ),
inference(resolution,[status(thm)],[c9118,c3630]) ).
cnf(c10253,plain,
( product(e_1,e_4,e_3)
| product(e_3,e_2,e_5) ),
inference(resolution,[status(thm)],[c9148,e_1_is_not_e_2]) ).
cnf(c10266,plain,
( product(e_3,e_2,e_5)
| ~ product(e_1,X1152,e_3)
| equalish(X1152,e_4) ),
inference(resolution,[status(thm)],[c10253,product_right_cancellation]) ).
cnf(e_3_then_e_4,axiom,
next(e_3,e_4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_3_then_e_4) ).
cnf(e_5_greater_e_4,axiom,
greater(e_5,e_4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_5_greater_e_4) ).
cnf(e_5_is_not_e_1,axiom,
~ equalish(e_5,e_1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_5_is_not_e_1) ).
cnf(c38,plain,
( product(e_1,e_5,e_1)
| product(e_1,e_5,e_2)
| product(e_1,e_5,e_3)
| product(e_1,e_5,e_4)
| product(e_1,e_5,e_5) ),
inference(resolution,[status(thm)],[c4,element_1]) ).
cnf(c377,plain,
( product(e_1,e_5,e_2)
| product(e_1,e_5,e_3)
| product(e_1,e_5,e_4)
| product(e_1,e_5,e_5)
| equalish(e_5,e_1) ),
inference(resolution,[status(thm)],[c38,c12]) ).
cnf(c2184,plain,
( product(e_1,e_5,e_2)
| product(e_1,e_5,e_3)
| product(e_1,e_5,e_4)
| product(e_1,e_5,e_5) ),
inference(resolution,[status(thm)],[c377,e_5_is_not_e_1]) ).
cnf(c2210,plain,
( product(e_1,e_5,e_2)
| product(e_1,e_5,e_3)
| product(e_1,e_5,e_4)
| equalish(e_1,e_5) ),
inference(resolution,[status(thm)],[c2184,c15]) ).
cnf(c2232,plain,
( product(e_1,e_5,e_2)
| product(e_1,e_5,e_3)
| product(e_1,e_5,e_4) ),
inference(resolution,[status(thm)],[c2210,e_1_is_not_e_5]) ).
cnf(c2249,plain,
( product(e_1,e_5,e_2)
| product(e_1,e_5,e_3)
| ~ product(X512,e_5,e_4)
| equalish(X512,e_1) ),
inference(resolution,[status(thm)],[c2232,product_left_cancellation]) ).
cnf(e_5_is_not_e_3,axiom,
~ equalish(e_5,e_3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_5_is_not_e_3) ).
cnf(c6116,plain,
( product(e_3,e_2,e_5)
| product(e_5,e_2,e_5)
| product(e_2,e_5,e_4) ),
inference(resolution,[status(thm)],[c5635,c3372]) ).
cnf(c14964,plain,
( product(e_3,e_2,e_5)
| product(e_2,e_5,e_4)
| equalish(e_5,e_3) ),
inference(resolution,[status(thm)],[c6116,c4414]) ).
cnf(c15070,plain,
( product(e_3,e_2,e_5)
| product(e_2,e_5,e_4) ),
inference(resolution,[status(thm)],[c14964,e_5_is_not_e_3]) ).
cnf(c15102,plain,
( product(e_2,e_5,e_4)
| ~ product(X1323,e_2,e_5)
| equalish(X1323,e_3) ),
inference(resolution,[status(thm)],[c15070,product_left_cancellation]) ).
cnf(c15071,plain,
( product(e_2,e_5,e_4)
| product(e_1,e_2,e_4)
| equalish(e_5,e_4) ),
inference(resolution,[status(thm)],[c15070,c6485]) ).
cnf(c15620,plain,
( product(e_2,e_5,e_4)
| product(e_1,e_2,e_4) ),
inference(resolution,[status(thm)],[c15071,e_5_is_not_e_4]) ).
cnf(c15677,plain,
( product(e_2,e_5,e_4)
| ~ product(e_2,X1365,e_1)
| product(e_4,e_2,X1365) ),
inference(resolution,[status(thm)],[c15620,qg3]) ).
cnf(c16288,plain,
( product(e_2,e_5,e_4)
| product(e_4,e_2,e_5) ),
inference(resolution,[status(thm)],[c15677,c3372]) ).
cnf(c16334,plain,
( product(e_2,e_5,e_4)
| equalish(e_4,e_3) ),
inference(resolution,[status(thm)],[c16288,c15102]) ).
cnf(c16394,plain,
product(e_2,e_5,e_4),
inference(resolution,[status(thm)],[c16334,e_4_is_not_e_3]) ).
cnf(c16417,plain,
( product(e_1,e_5,e_2)
| product(e_1,e_5,e_3)
| equalish(e_2,e_1) ),
inference(resolution,[status(thm)],[c16394,c2249]) ).
cnf(c17504,plain,
( product(e_1,e_5,e_2)
| product(e_1,e_5,e_3) ),
inference(resolution,[status(thm)],[c16417,e_2_is_not_e_1]) ).
cnf(c17515,plain,
( product(e_1,e_5,e_3)
| product(e_3,e_1,e_5) ),
inference(resolution,[status(thm)],[c17504,c3254]) ).
cnf(c17568,plain,
( product(e_1,e_5,e_3)
| ~ next(e_3,X1403)
| ~ greater(e_5,X1403) ),
inference(resolution,[status(thm)],[c17515,no_redundancy]) ).
cnf(c17596,plain,
( product(e_1,e_5,e_3)
| ~ next(e_3,e_4) ),
inference(resolution,[status(thm)],[c17568,e_5_greater_e_4]) ).
cnf(c17598,plain,
product(e_1,e_5,e_3),
inference(resolution,[status(thm)],[c17596,e_3_then_e_4]) ).
cnf(c17603,plain,
( product(e_3,e_2,e_5)
| equalish(e_5,e_4) ),
inference(resolution,[status(thm)],[c17598,c10266]) ).
cnf(c17933,plain,
product(e_3,e_2,e_5),
inference(resolution,[status(thm)],[c17603,e_5_is_not_e_4]) ).
cnf(c34,plain,
( product(e_3,e_4,e_1)
| product(e_3,e_4,e_2)
| product(e_3,e_4,e_3)
| product(e_3,e_4,e_4)
| product(e_3,e_4,e_5) ),
inference(resolution,[status(thm)],[c3,element_3]) ).
cnf(c310,plain,
( product(e_3,e_4,e_1)
| product(e_3,e_4,e_2)
| product(e_3,e_4,e_4)
| product(e_3,e_4,e_5)
| equalish(e_4,e_3) ),
inference(resolution,[status(thm)],[c34,c12]) ).
cnf(c1427,plain,
( product(e_3,e_4,e_1)
| product(e_3,e_4,e_2)
| product(e_3,e_4,e_4)
| product(e_3,e_4,e_5) ),
inference(resolution,[status(thm)],[c310,e_4_is_not_e_3]) ).
cnf(c1516,plain,
( product(e_3,e_4,e_1)
| product(e_3,e_4,e_2)
| product(e_3,e_4,e_5)
| equalish(e_3,e_4) ),
inference(resolution,[status(thm)],[c1427,c15]) ).
cnf(c1544,plain,
( product(e_3,e_4,e_1)
| product(e_3,e_4,e_2)
| product(e_3,e_4,e_5) ),
inference(resolution,[status(thm)],[c1516,e_3_is_not_e_4]) ).
cnf(c1560,plain,
( product(e_3,e_4,e_1)
| product(e_3,e_4,e_2)
| ~ product(X375,e_4,e_5)
| equalish(X375,e_3) ),
inference(resolution,[status(thm)],[c1544,product_left_cancellation]) ).
cnf(c7970,plain,
( product(e_3,e_4,e_1)
| product(e_3,e_4,e_2)
| equalish(e_2,e_3) ),
inference(resolution,[status(thm)],[c7959,c1560]) ).
cnf(c9039,plain,
( product(e_3,e_4,e_1)
| product(e_3,e_4,e_2) ),
inference(resolution,[status(thm)],[c7970,e_2_is_not_e_3]) ).
cnf(c9052,plain,
( product(e_3,e_4,e_1)
| ~ product(X1086,e_4,e_2)
| equalish(X1086,e_3) ),
inference(resolution,[status(thm)],[c9039,product_left_cancellation]) ).
cnf(c9115,plain,
( product(e_1,e_4,e_3)
| product(e_3,e_4,e_1)
| equalish(e_1,e_3) ),
inference(resolution,[status(thm)],[c9107,c9052]) ).
cnf(c9369,plain,
( product(e_1,e_4,e_3)
| product(e_3,e_4,e_1) ),
inference(resolution,[status(thm)],[c9115,e_1_is_not_e_3]) ).
cnf(c9375,plain,
( product(e_3,e_4,e_1)
| ~ product(e_1,X1114,e_3)
| equalish(X1114,e_4) ),
inference(resolution,[status(thm)],[c9369,product_right_cancellation]) ).
cnf(c17602,plain,
( product(e_3,e_4,e_1)
| equalish(e_5,e_4) ),
inference(resolution,[status(thm)],[c17598,c9375]) ).
cnf(c17858,plain,
product(e_3,e_4,e_1),
inference(resolution,[status(thm)],[c17602,e_5_is_not_e_4]) ).
cnf(c3788,plain,
( product(e_5,e_2,e_1)
| ~ product(e_3,X713,e_4)
| equalish(X713,e_2) ),
inference(resolution,[status(thm)],[c3784,product_right_cancellation]) ).
cnf(c9145,plain,
( product(e_1,e_4,e_3)
| product(e_5,e_2,e_1)
| equalish(e_1,e_2) ),
inference(resolution,[status(thm)],[c9118,c3788]) ).
cnf(c10038,plain,
( product(e_1,e_4,e_3)
| product(e_5,e_2,e_1) ),
inference(resolution,[status(thm)],[c9145,e_1_is_not_e_2]) ).
cnf(c10048,plain,
( product(e_5,e_2,e_1)
| ~ product(e_1,X1143,e_3)
| equalish(X1143,e_4) ),
inference(resolution,[status(thm)],[c10038,product_right_cancellation]) ).
cnf(c17599,plain,
( product(e_5,e_2,e_1)
| equalish(e_5,e_4) ),
inference(resolution,[status(thm)],[c17598,c10048]) ).
cnf(c17679,plain,
product(e_5,e_2,e_1),
inference(resolution,[status(thm)],[c17599,e_5_is_not_e_4]) ).
cnf(c17620,plain,
( ~ product(e_5,X1438,e_1)
| product(e_3,e_5,X1438) ),
inference(resolution,[status(thm)],[c17598,qg3]) ).
cnf(c18160,plain,
product(e_3,e_5,e_2),
inference(resolution,[status(thm)],[c17620,c17679]) ).
cnf(c7975,plain,
( ~ product(e_2,X1026,e_5)
| equalish(X1026,e_4) ),
inference(resolution,[status(thm)],[c7959,product_right_cancellation]) ).
cnf(c16410,plain,
( ~ product(e_2,X1367,e_4)
| equalish(X1367,e_5) ),
inference(resolution,[status(thm)],[c16394,product_right_cancellation]) ).
cnf(c6,plain,
( ~ group_element(X53)
| product(X53,e_3,e_1)
| product(X53,e_3,e_2)
| product(X53,e_3,e_3)
| product(X53,e_3,e_4)
| product(X53,e_3,e_5) ),
inference(resolution,[status(thm)],[product_total_function1,element_3]) ).
cnf(c45,plain,
( product(e_2,e_3,e_1)
| product(e_2,e_3,e_2)
| product(e_2,e_3,e_3)
| product(e_2,e_3,e_4)
| product(e_2,e_3,e_5) ),
inference(resolution,[status(thm)],[c6,element_2]) ).
cnf(c655,plain,
( product(e_2,e_3,e_1)
| product(e_2,e_3,e_3)
| product(e_2,e_3,e_4)
| product(e_2,e_3,e_5)
| equalish(e_3,e_2) ),
inference(resolution,[status(thm)],[c45,c12]) ).
cnf(c10624,plain,
( product(e_2,e_3,e_1)
| product(e_2,e_3,e_3)
| product(e_2,e_3,e_4)
| product(e_2,e_3,e_5) ),
inference(resolution,[status(thm)],[c655,e_3_is_not_e_2]) ).
cnf(c19390,plain,
( product(e_2,e_3,e_1)
| product(e_2,e_3,e_4)
| product(e_2,e_3,e_5)
| equalish(e_2,e_3) ),
inference(resolution,[status(thm)],[c10624,c15]) ).
cnf(c19476,plain,
( product(e_2,e_3,e_1)
| product(e_2,e_3,e_4)
| product(e_2,e_3,e_5) ),
inference(resolution,[status(thm)],[c19390,e_2_is_not_e_3]) ).
cnf(c19495,plain,
( product(e_2,e_3,e_1)
| product(e_2,e_3,e_5)
| equalish(e_3,e_5) ),
inference(resolution,[status(thm)],[c19476,c16410]) ).
cnf(c19545,plain,
( product(e_2,e_3,e_1)
| product(e_2,e_3,e_5) ),
inference(resolution,[status(thm)],[c19495,e_3_is_not_e_5]) ).
cnf(c19558,plain,
( product(e_2,e_3,e_1)
| equalish(e_3,e_4) ),
inference(resolution,[status(thm)],[c19545,c7975]) ).
cnf(c19583,plain,
product(e_2,e_3,e_1),
inference(resolution,[status(thm)],[c19558,e_3_is_not_e_4]) ).
cnf(c19594,plain,
( ~ product(e_3,X2199,e_2)
| product(e_1,e_3,X2199) ),
inference(resolution,[status(thm)],[c19583,qg3]) ).
cnf(c19617,plain,
product(e_1,e_3,e_5),
inference(resolution,[status(thm)],[c19594,c18160]) ).
cnf(c19627,plain,
( ~ product(e_3,X2204,e_1)
| product(e_5,e_3,X2204) ),
inference(resolution,[status(thm)],[c19617,qg3]) ).
cnf(c19645,plain,
product(e_5,e_3,e_4),
inference(resolution,[status(thm)],[c19627,c17858]) ).
cnf(c19653,plain,
( ~ product(e_3,X2209,e_5)
| product(e_4,e_3,X2209) ),
inference(resolution,[status(thm)],[c19645,qg3]) ).
cnf(c19666,plain,
product(e_4,e_3,e_2),
inference(resolution,[status(thm)],[c19653,c17933]) ).
cnf(c19674,plain,
( ~ product(e_3,X2214,e_4)
| product(e_2,e_3,X2214) ),
inference(resolution,[status(thm)],[c19666,qg3]) ).
cnf(c19672,plain,
( ~ product(X2212,e_3,e_2)
| equalish(X2212,e_4) ),
inference(resolution,[status(thm)],[c19666,product_left_cancellation]) ).
cnf(c19670,plain,
( ~ product(e_4,X2211,e_2)
| equalish(X2211,e_3) ),
inference(resolution,[status(thm)],[c19666,product_right_cancellation]) ).
cnf(c19668,plain,
( ~ product(e_4,e_3,X2210)
| equalish(X2210,e_2) ),
inference(resolution,[status(thm)],[c19666,product_total_function2]) ).
cnf(c19651,plain,
( ~ product(X2208,e_3,e_4)
| equalish(X2208,e_5) ),
inference(resolution,[status(thm)],[c19645,product_left_cancellation]) ).
cnf(c19649,plain,
( ~ product(e_5,X2206,e_4)
| equalish(X2206,e_3) ),
inference(resolution,[status(thm)],[c19645,product_right_cancellation]) ).
cnf(c19647,plain,
( ~ product(e_5,e_3,X2205)
| equalish(X2205,e_4) ),
inference(resolution,[status(thm)],[c19645,product_total_function2]) ).
cnf(c19626,plain,
( ~ product(X2203,e_3,e_5)
| equalish(X2203,e_1) ),
inference(resolution,[status(thm)],[c19617,product_left_cancellation]) ).
cnf(c19623,plain,
( ~ product(e_1,X2202,e_5)
| equalish(X2202,e_3) ),
inference(resolution,[status(thm)],[c19617,product_right_cancellation]) ).
cnf(c19618,plain,
( ~ product(e_1,e_3,X2201)
| equalish(X2201,e_5) ),
inference(resolution,[status(thm)],[c19617,product_total_function2]) ).
cnf(c19593,plain,
( ~ product(X2198,e_3,e_1)
| equalish(X2198,e_2) ),
inference(resolution,[status(thm)],[c19583,product_left_cancellation]) ).
cnf(c19589,plain,
( ~ product(e_2,X2197,e_1)
| equalish(X2197,e_3) ),
inference(resolution,[status(thm)],[c19583,product_right_cancellation]) ).
cnf(c19587,plain,
( ~ product(e_2,e_3,X2196)
| equalish(X2196,e_1) ),
inference(resolution,[status(thm)],[c19583,product_total_function2]) ).
cnf(c9124,plain,
( product(e_1,e_4,e_2)
| ~ product(e_1,X1094,e_3)
| equalish(X1094,e_4) ),
inference(resolution,[status(thm)],[c9107,product_right_cancellation]) ).
cnf(c17614,plain,
( product(e_1,e_4,e_2)
| equalish(e_5,e_4) ),
inference(resolution,[status(thm)],[c17598,c9124]) ).
cnf(c18095,plain,
product(e_1,e_4,e_2),
inference(resolution,[status(thm)],[c17614,e_5_is_not_e_4]) ).
cnf(c18106,plain,
( ~ product(X1432,e_4,e_2)
| equalish(X1432,e_1) ),
inference(resolution,[status(thm)],[c18095,product_left_cancellation]) ).
cnf(c32,plain,
( product(e_5,e_4,e_1)
| product(e_5,e_4,e_2)
| product(e_5,e_4,e_3)
| product(e_5,e_4,e_4)
| product(e_5,e_4,e_5) ),
inference(resolution,[status(thm)],[c3,element_5]) ).
cnf(c268,plain,
( product(e_5,e_4,e_1)
| product(e_5,e_4,e_2)
| product(e_5,e_4,e_3)
| product(e_5,e_4,e_5)
| equalish(e_5,e_4) ),
inference(resolution,[status(thm)],[c32,c15]) ).
cnf(c1173,plain,
( product(e_5,e_4,e_1)
| product(e_5,e_4,e_2)
| product(e_5,e_4,e_3)
| product(e_5,e_4,e_5) ),
inference(resolution,[status(thm)],[c268,e_5_is_not_e_4]) ).
cnf(c1192,plain,
( product(e_5,e_4,e_1)
| product(e_5,e_4,e_2)
| product(e_5,e_4,e_3)
| equalish(e_4,e_5) ),
inference(resolution,[status(thm)],[c1173,c12]) ).
cnf(c1213,plain,
( product(e_5,e_4,e_1)
| product(e_5,e_4,e_2)
| product(e_5,e_4,e_3) ),
inference(resolution,[status(thm)],[c1192,e_4_is_not_e_5]) ).
cnf(c1214,plain,
( product(e_5,e_4,e_2)
| product(e_5,e_4,e_3)
| ~ product(e_5,X273,e_1)
| equalish(X273,e_4) ),
inference(resolution,[status(thm)],[c1213,product_right_cancellation]) ).
cnf(c17689,plain,
( product(e_5,e_4,e_2)
| product(e_5,e_4,e_3)
| equalish(e_2,e_4) ),
inference(resolution,[status(thm)],[c17679,c1214]) ).
cnf(c18614,plain,
( product(e_5,e_4,e_2)
| product(e_5,e_4,e_3) ),
inference(resolution,[status(thm)],[c17689,e_2_is_not_e_4]) ).
cnf(c18624,plain,
( product(e_5,e_4,e_3)
| equalish(e_5,e_1) ),
inference(resolution,[status(thm)],[c18614,c18106]) ).
cnf(c18647,plain,
product(e_5,e_4,e_3),
inference(resolution,[status(thm)],[c18624,e_5_is_not_e_1]) ).
cnf(c18656,plain,
( ~ product(e_4,X1530,e_5)
| product(e_3,e_4,X1530) ),
inference(resolution,[status(thm)],[c18647,qg3]) ).
cnf(c18655,plain,
( ~ product(X1528,e_4,e_3)
| equalish(X1528,e_5) ),
inference(resolution,[status(thm)],[c18647,product_left_cancellation]) ).
cnf(c18651,plain,
( ~ product(e_5,X1527,e_3)
| equalish(X1527,e_4) ),
inference(resolution,[status(thm)],[c18647,product_right_cancellation]) ).
cnf(c18649,plain,
( ~ product(e_5,e_4,X1526)
| equalish(X1526,e_3) ),
inference(resolution,[status(thm)],[c18647,product_total_function2]) ).
cnf(c16423,plain,
( ~ product(e_5,X1370,e_2)
| product(e_4,e_5,X1370) ),
inference(resolution,[status(thm)],[c16394,qg3]) ).
cnf(c6477,plain,
( product(e_1,e_2,e_4)
| ~ product(e_3,X915,e_4)
| equalish(X915,e_2) ),
inference(resolution,[status(thm)],[c6453,product_right_cancellation]) ).
cnf(c9142,plain,
( product(e_1,e_4,e_3)
| product(e_1,e_2,e_4)
| equalish(e_1,e_2) ),
inference(resolution,[status(thm)],[c9118,c6477]) ).
cnf(c9842,plain,
( product(e_1,e_4,e_3)
| product(e_1,e_2,e_4) ),
inference(resolution,[status(thm)],[c9142,e_1_is_not_e_2]) ).
cnf(c9851,plain,
( product(e_1,e_2,e_4)
| ~ product(e_1,X1134,e_3)
| equalish(X1134,e_4) ),
inference(resolution,[status(thm)],[c9842,product_right_cancellation]) ).
cnf(c17601,plain,
( product(e_1,e_2,e_4)
| equalish(e_5,e_4) ),
inference(resolution,[status(thm)],[c17598,c9851]) ).
cnf(c17781,plain,
product(e_1,e_2,e_4),
inference(resolution,[status(thm)],[c17601,e_5_is_not_e_4]) ).
cnf(c18107,plain,
product(e_3,e_1,e_4),
inference(resolution,[status(thm)],[c18095,c3254]) ).
cnf(c18131,plain,
( ~ product(e_1,X1451,e_3)
| product(e_4,e_1,X1451) ),
inference(resolution,[status(thm)],[c18107,qg3]) ).
cnf(c18244,plain,
product(e_4,e_1,e_5),
inference(resolution,[status(thm)],[c18131,c17598]) ).
cnf(c18258,plain,
( ~ product(e_1,X1457,e_4)
| product(e_5,e_1,X1457) ),
inference(resolution,[status(thm)],[c18244,qg3]) ).
cnf(c18298,plain,
product(e_5,e_1,e_2),
inference(resolution,[status(thm)],[c18258,c17781]) ).
cnf(c18309,plain,
product(e_4,e_5,e_1),
inference(resolution,[status(thm)],[c18298,c16423]) ).
cnf(c18320,plain,
( ~ product(e_5,X1466,e_4)
| product(e_1,e_5,X1466) ),
inference(resolution,[status(thm)],[c18309,qg3]) ).
cnf(c18311,plain,
( ~ product(e_1,X1465,e_5)
| product(e_2,e_1,X1465) ),
inference(resolution,[status(thm)],[c18298,qg3]) ).
cnf(c18318,plain,
( ~ product(X1464,e_5,e_1)
| equalish(X1464,e_4) ),
inference(resolution,[status(thm)],[c18309,product_left_cancellation]) ).
cnf(c18315,plain,
( ~ product(e_4,X1463,e_1)
| equalish(X1463,e_5) ),
inference(resolution,[status(thm)],[c18309,product_right_cancellation]) ).
cnf(c18312,plain,
( ~ product(e_4,e_5,X1462)
| equalish(X1462,e_1) ),
inference(resolution,[status(thm)],[c18309,product_total_function2]) ).
cnf(c18310,plain,
( ~ product(X1461,e_1,e_2)
| equalish(X1461,e_5) ),
inference(resolution,[status(thm)],[c18298,product_left_cancellation]) ).
cnf(c18308,plain,
( ~ product(e_5,X1460,e_2)
| equalish(X1460,e_1) ),
inference(resolution,[status(thm)],[c18298,product_right_cancellation]) ).
cnf(c18303,plain,
( ~ product(e_5,e_1,X1459)
| equalish(X1459,e_2) ),
inference(resolution,[status(thm)],[c18298,product_total_function2]) ).
cnf(e_2_greater_e_1,axiom,
greater(e_2,e_1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_2_greater_e_1) ).
cnf(c18301,plain,
( ~ next(e_5,X1458)
| ~ greater(e_2,X1458) ),
inference(resolution,[status(thm)],[c18298,no_redundancy]) ).
cnf(c18321,plain,
~ next(e_5,e_1),
inference(resolution,[status(thm)],[c18301,e_2_greater_e_1]) ).
cnf(c18179,plain,
( ~ product(e_5,X1456,e_3)
| product(e_2,e_5,X1456) ),
inference(resolution,[status(thm)],[c18160,qg3]) ).
cnf(c18255,plain,
( ~ product(X1455,e_1,e_5)
| equalish(X1455,e_4) ),
inference(resolution,[status(thm)],[c18244,product_left_cancellation]) ).
cnf(c18252,plain,
( ~ product(e_4,X1454,e_5)
| equalish(X1454,e_1) ),
inference(resolution,[status(thm)],[c18244,product_right_cancellation]) ).
cnf(c18249,plain,
( ~ product(e_4,e_1,X1453)
| equalish(X1453,e_5) ),
inference(resolution,[status(thm)],[c18244,product_total_function2]) ).
cnf(e_5_greater_e_1,axiom,
greater(e_5,e_1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_5_greater_e_1) ).
cnf(c18248,plain,
( ~ next(e_4,X1452)
| ~ greater(e_5,X1452) ),
inference(resolution,[status(thm)],[c18244,no_redundancy]) ).
cnf(c18263,plain,
~ next(e_4,e_1),
inference(resolution,[status(thm)],[c18248,e_5_greater_e_1]) ).
cnf(c18262,plain,
~ next(e_4,e_4),
inference(resolution,[status(thm)],[c18248,e_5_greater_e_4]) ).
cnf(c18261,plain,
~ next(e_4,e_3),
inference(resolution,[status(thm)],[c18248,e_5_greater_e_3]) ).
cnf(e_5_greater_e_2,axiom,
greater(e_5,e_2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_5_greater_e_2) ).
cnf(c18260,plain,
~ next(e_4,e_2),
inference(resolution,[status(thm)],[c18248,e_5_greater_e_2]) ).
cnf(c18108,plain,
( ~ product(e_4,X1450,e_1)
| product(e_2,e_4,X1450) ),
inference(resolution,[status(thm)],[c18095,qg3]) ).
cnf(c4300,plain,
( product(e_4,e_2,e_3)
| ~ product(e_3,X765,e_4)
| equalish(X765,e_2) ),
inference(resolution,[status(thm)],[c4274,product_right_cancellation]) ).
cnf(c9141,plain,
( product(e_1,e_4,e_3)
| product(e_4,e_2,e_3)
| equalish(e_1,e_2) ),
inference(resolution,[status(thm)],[c9118,c4300]) ).
cnf(c9657,plain,
( product(e_1,e_4,e_3)
| product(e_4,e_2,e_3) ),
inference(resolution,[status(thm)],[c9141,e_1_is_not_e_2]) ).
cnf(c9672,plain,
( product(e_4,e_2,e_3)
| ~ product(e_1,X1125,e_3)
| equalish(X1125,e_4) ),
inference(resolution,[status(thm)],[c9657,product_right_cancellation]) ).
cnf(c17612,plain,
( product(e_4,e_2,e_3)
| equalish(e_5,e_4) ),
inference(resolution,[status(thm)],[c17598,c9672]) ).
cnf(c18019,plain,
product(e_4,e_2,e_3),
inference(resolution,[status(thm)],[c17612,e_5_is_not_e_4]) ).
cnf(c18048,plain,
( ~ product(e_2,X1449,e_4)
| product(e_3,e_2,X1449) ),
inference(resolution,[status(thm)],[c18019,qg3]) ).
cnf(c17962,plain,
( ~ product(e_2,X1448,e_3)
| product(e_5,e_2,X1448) ),
inference(resolution,[status(thm)],[c17933,qg3]) ).
cnf(c17879,plain,
( ~ product(e_4,X1447,e_3)
| product(e_1,e_4,X1447) ),
inference(resolution,[status(thm)],[c17858,qg3]) ).
cnf(c17809,plain,
( ~ product(e_2,X1446,e_1)
| product(e_4,e_2,X1446) ),
inference(resolution,[status(thm)],[c17781,qg3]) ).
cnf(c17711,plain,
( ~ product(e_2,X1443,e_5)
| product(e_1,e_2,X1443) ),
inference(resolution,[status(thm)],[c17679,qg3]) ).
cnf(c18177,plain,
( ~ product(X1441,e_5,e_2)
| equalish(X1441,e_3) ),
inference(resolution,[status(thm)],[c18160,product_left_cancellation]) ).
cnf(c18172,plain,
( ~ product(e_3,X1440,e_2)
| equalish(X1440,e_5) ),
inference(resolution,[status(thm)],[c18160,product_right_cancellation]) ).
cnf(c18169,plain,
( ~ product(e_3,e_5,X1439)
| equalish(X1439,e_2) ),
inference(resolution,[status(thm)],[c18160,product_total_function2]) ).
cnf(c18127,plain,
( ~ product(X1436,e_1,e_4)
| equalish(X1436,e_3) ),
inference(resolution,[status(thm)],[c18107,product_left_cancellation]) ).
cnf(c18121,plain,
( ~ product(e_3,X1435,e_4)
| equalish(X1435,e_1) ),
inference(resolution,[status(thm)],[c18107,product_right_cancellation]) ).
cnf(c18113,plain,
( ~ product(e_3,e_1,X1433)
| equalish(X1433,e_4) ),
inference(resolution,[status(thm)],[c18107,product_total_function2]) ).
cnf(c18101,plain,
( ~ product(e_1,X1430,e_2)
| equalish(X1430,e_4) ),
inference(resolution,[status(thm)],[c18095,product_right_cancellation]) ).
cnf(c18098,plain,
( ~ product(e_1,e_4,X1429)
| equalish(X1429,e_2) ),
inference(resolution,[status(thm)],[c18095,product_total_function2]) ).
cnf(e_4_greater_e_1,axiom,
greater(e_4,e_1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_4_greater_e_1) ).
cnf(c18112,plain,
( ~ next(e_3,X1428)
| ~ greater(e_4,X1428) ),
inference(resolution,[status(thm)],[c18107,no_redundancy]) ).
cnf(c18134,plain,
~ next(e_3,e_1),
inference(resolution,[status(thm)],[c18112,e_4_greater_e_1]) ).
cnf(c18133,plain,
~ next(e_3,e_3),
inference(resolution,[status(thm)],[c18112,e_4_greater_e_3]) ).
cnf(e_4_greater_e_2,axiom,
greater(e_4,e_2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_4_greater_e_2) ).
cnf(c18132,plain,
~ next(e_3,e_2),
inference(resolution,[status(thm)],[c18112,e_4_greater_e_2]) ).
cnf(c18042,plain,
( ~ product(X1427,e_2,e_3)
| equalish(X1427,e_4) ),
inference(resolution,[status(thm)],[c18019,product_left_cancellation]) ).
cnf(c18031,plain,
( ~ product(e_4,X1426,e_3)
| equalish(X1426,e_2) ),
inference(resolution,[status(thm)],[c18019,product_right_cancellation]) ).
cnf(c18023,plain,
( ~ product(e_4,e_2,X1425)
| equalish(X1425,e_3) ),
inference(resolution,[status(thm)],[c18019,product_total_function2]) ).
cnf(c17959,plain,
( ~ product(X1424,e_2,e_5)
| equalish(X1424,e_3) ),
inference(resolution,[status(thm)],[c17933,product_left_cancellation]) ).
cnf(c17945,plain,
( ~ product(e_3,X1422,e_5)
| equalish(X1422,e_2) ),
inference(resolution,[status(thm)],[c17933,product_right_cancellation]) ).
cnf(c17935,plain,
( ~ product(e_3,e_2,X1421)
| equalish(X1421,e_5) ),
inference(resolution,[status(thm)],[c17933,product_total_function2]) ).
cnf(c17875,plain,
( ~ product(X1419,e_4,e_1)
| equalish(X1419,e_3) ),
inference(resolution,[status(thm)],[c17858,product_left_cancellation]) ).
cnf(c17869,plain,
( ~ product(e_3,X1418,e_1)
| equalish(X1418,e_4) ),
inference(resolution,[status(thm)],[c17858,product_right_cancellation]) ).
cnf(c17863,plain,
( ~ product(e_3,e_4,X1416)
| equalish(X1416,e_1) ),
inference(resolution,[status(thm)],[c17858,product_total_function2]) ).
cnf(c17804,plain,
( ~ product(X1415,e_2,e_4)
| equalish(X1415,e_1) ),
inference(resolution,[status(thm)],[c17781,product_left_cancellation]) ).
cnf(c17797,plain,
( ~ product(e_1,X1414,e_4)
| equalish(X1414,e_2) ),
inference(resolution,[status(thm)],[c17781,product_right_cancellation]) ).
cnf(c17785,plain,
( ~ product(e_1,e_2,X1413)
| equalish(X1413,e_4) ),
inference(resolution,[status(thm)],[c17781,product_total_function2]) ).
cnf(c17703,plain,
( ~ product(X1411,e_2,e_1)
| equalish(X1411,e_5) ),
inference(resolution,[status(thm)],[c17679,product_left_cancellation]) ).
cnf(c17698,plain,
( ~ product(e_5,X1410,e_1)
| equalish(X1410,e_2) ),
inference(resolution,[status(thm)],[c17679,product_right_cancellation]) ).
cnf(c17688,plain,
( ~ product(e_5,e_2,X1409)
| equalish(X1409,e_1) ),
inference(resolution,[status(thm)],[c17679,product_total_function2]) ).
cnf(c17615,plain,
( ~ product(X1407,e_5,e_3)
| equalish(X1407,e_1) ),
inference(resolution,[status(thm)],[c17598,product_left_cancellation]) ).
cnf(c17607,plain,
( ~ product(e_1,X1406,e_3)
| equalish(X1406,e_5) ),
inference(resolution,[status(thm)],[c17598,product_right_cancellation]) ).
cnf(c17600,plain,
( ~ product(e_1,e_5,X1404)
| equalish(X1404,e_3) ),
inference(resolution,[status(thm)],[c17598,product_total_function2]) ).
cnf(c16420,plain,
( ~ product(X1368,e_5,e_4)
| equalish(X1368,e_2) ),
inference(resolution,[status(thm)],[c16394,product_left_cancellation]) ).
cnf(c16399,plain,
( ~ product(e_2,e_5,X1366)
| equalish(X1366,e_4) ),
inference(resolution,[status(thm)],[c16394,product_total_function2]) ).
cnf(c7992,plain,
( ~ product(e_4,X1031,e_2)
| product(e_5,e_4,X1031) ),
inference(resolution,[status(thm)],[c7959,qg3]) ).
cnf(c7990,plain,
( ~ product(e_2,e_4,X1029)
| equalish(X1029,e_5) ),
inference(resolution,[status(thm)],[c7959,product_total_function2]) ).
cnf(c7979,plain,
( ~ product(X1027,e_4,e_5)
| equalish(X1027,e_2) ),
inference(resolution,[status(thm)],[c7959,product_left_cancellation]) ).
cnf(c3252,plain,
( ~ product(e_2,e_1,X641)
| equalish(X641,e_3) ),
inference(resolution,[status(thm)],[c3244,product_total_function2]) ).
cnf(c3251,plain,
( ~ product(X640,e_1,e_3)
| equalish(X640,e_2) ),
inference(resolution,[status(thm)],[c3244,product_left_cancellation]) ).
cnf(c3249,plain,
( ~ product(e_2,X639,e_3)
| equalish(X639,e_1) ),
inference(resolution,[status(thm)],[c3244,product_right_cancellation]) ).
cnf(e_3_greater_e_1,axiom,
greater(e_3,e_1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_3_greater_e_1) ).
cnf(c3250,plain,
( ~ next(e_2,X638)
| ~ greater(e_3,X638) ),
inference(resolution,[status(thm)],[c3244,no_redundancy]) ).
cnf(c3256,plain,
~ next(e_2,e_1),
inference(resolution,[status(thm)],[c3250,e_3_greater_e_1]) ).
cnf(e_3_greater_e_2,axiom,
greater(e_3,e_2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_3_greater_e_2) ).
cnf(c3255,plain,
~ next(e_2,e_2),
inference(resolution,[status(thm)],[c3250,e_3_greater_e_2]) ).
cnf(c1,plain,
( ~ group_element(X47)
| product(X47,X47,e_1)
| product(X47,X47,e_2)
| product(X47,X47,e_3)
| product(X47,X47,e_4)
| product(X47,X47,e_5) ),
inference(factor,[status(thm)],[product_total_function1]) ).
cnf(c17,plain,
( ~ product(X45,X46,X45)
| product(X45,X45,X46) ),
inference(resolution,[status(thm)],[qg3,product_idempotence]) ).
cnf(c8,plain,
( ~ product(X17,X17,X18)
| equalish(X18,X17) ),
inference(resolution,[status(thm)],[product_total_function2,product_idempotence]) ).
cnf(c7,plain,
( ~ product(X15,X13,X14)
| equalish(X14,X14) ),
inference(factor,[status(thm)],[product_total_function2]) ).
cnf(c9,plain,
equalish(X16,X16),
inference(resolution,[status(thm)],[c7,product_idempotence]) ).
cnf(c0,plain,
( ~ next(e_1,X8)
| ~ greater(e_1,X8) ),
inference(resolution,[status(thm)],[no_redundancy,product_idempotence]) ).
cnf(e_4_then_e_5,axiom,
next(e_4,e_5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_4_then_e_5) ).
cnf(e_1_then_e_2,axiom,
next(e_1,e_2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_1_then_e_2) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.11 % Problem : GRP127-2.005 : TPTP v8.1.2. Released v1.2.0.
% 0.10/0.12 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.10/0.32 % Computer : n032.cluster.edu
% 0.10/0.32 % Model : x86_64 x86_64
% 0.10/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.32 % Memory : 8042.1875MB
% 0.10/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.10/0.32 % CPULimit : 300
% 0.10/0.32 % WCLimit : 300
% 0.10/0.32 % DateTime : Thu May 9 03:39:52 EDT 2024
% 0.10/0.32 % CPUTime :
% 59.02/59.25 % Version: 1.5
% 59.02/59.25 % SZS status Satisfiable
% 59.02/59.25 % SZS output start Saturation
% See solution above
% 59.02/59.26
% 59.02/59.26 % Initial clauses : 46
% 59.02/59.26 % Processed clauses : 1103
% 59.02/59.26 % Factors computed : 5
% 59.02/59.26 % Resolvents computed: 19674
% 59.02/59.26 % Tautologies deleted: 1
% 59.02/59.26 % Forward subsumed : 18621
% 59.02/59.26 % Backward subsumed : 931
% 59.02/59.26 % -------- CPU Time ---------
% 59.02/59.26 % User time : 58.815 s
% 59.02/59.26 % System time : 0.084 s
% 59.02/59.26 % Total time : 58.899 s
%------------------------------------------------------------------------------