%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GRP126-4.004 : TPTP v8.1.2. Bugfixed v1.2.1.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n023.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:08 EDT 2024
% Result : Unsatisfiable 36.08s 36.30s
% Output : Refutation 36.08s
% Verified :
% SZS Type : Refutation
% Derivation depth : 26
% Number of leaves : 23
% Syntax : Number of clauses : 110 ( 24 unt; 73 nHn; 109 RR)
% Number of literals : 270 ( 0 equ; 50 neg)
% Maximal clause size : 6 ( 2 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 4 ( 3 usr; 1 prp; 0-3 aty)
% Number of functors : 4 ( 4 usr; 4 con; 0-0 aty)
% Number of variables : 56 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
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(product_right_cancellation,axiom,
( ~ product(X39,X36,X37)
| ~ product(X39,X38,X37)
| equalish(X36,X38) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',product_right_cancellation) ).
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(product_left_cancellation,axiom,
( ~ product(X43,X44,X46)
| ~ product(X45,X44,X46)
| equalish(X43,X45) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',product_left_cancellation) ).
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(qg4_1,negated_conjecture,
( product(X9,X7,X8)
| ~ product(X8,X10,X7)
| ~ product(X7,X9,X10) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',qg4_1) ).
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(product_idempotence,axiom,
product(X2,X2,X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',product_idempotence) ).
cnf(product_total_function2,axiom,
( ~ product(X26,X23,X24)
| ~ product(X26,X23,X25)
| equalish(X24,X25) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',product_total_function2) ).
cnf(c17,plain,
( ~ product(X33,X33,X34)
| equalish(X34,X33) ),
inference(resolution,[status(thm)],[product_total_function2,product_idempotence]) ).
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(c26,plain,
( ~ product(X47,X48,X47)
| equalish(X48,X47) ),
inference(resolution,[status(thm)],[product_right_cancellation,product_idempotence]) ).
cnf(element_4,axiom,
group_element(e_4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',element_4) ).
cnf(element_3,axiom,
group_element(e_3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',element_3) ).
cnf(row_surjectivity,axiom,
( ~ group_element(X4)
| ~ group_element(X3)
| product(e_1,X4,X3)
| product(e_2,X4,X3)
| product(e_3,X4,X3)
| product(e_4,X4,X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',row_surjectivity) ).
cnf(c1,plain,
( ~ group_element(X67)
| product(e_1,X67,e_3)
| product(e_2,X67,e_3)
| product(e_3,X67,e_3)
| product(e_4,X67,e_3) ),
inference(resolution,[status(thm)],[row_surjectivity,element_3]) ).
cnf(c40,plain,
( product(e_1,e_4,e_3)
| product(e_2,e_4,e_3)
| product(e_3,e_4,e_3)
| product(e_4,e_4,e_3) ),
inference(resolution,[status(thm)],[c1,element_4]) ).
cnf(c110,plain,
( product(e_1,e_4,e_3)
| product(e_2,e_4,e_3)
| product(e_4,e_4,e_3)
| equalish(e_4,e_3) ),
inference(resolution,[status(thm)],[c40,c26]) ).
cnf(c145,plain,
( product(e_1,e_4,e_3)
| product(e_2,e_4,e_3)
| product(e_4,e_4,e_3) ),
inference(resolution,[status(thm)],[c110,e_4_is_not_e_3]) ).
cnf(c163,plain,
( product(e_1,e_4,e_3)
| product(e_2,e_4,e_3)
| equalish(e_3,e_4) ),
inference(resolution,[status(thm)],[c145,c17]) ).
cnf(c179,plain,
( product(e_1,e_4,e_3)
| product(e_2,e_4,e_3) ),
inference(resolution,[status(thm)],[c163,e_3_is_not_e_4]) ).
cnf(c187,plain,
( product(e_1,e_4,e_3)
| ~ product(e_2,X84,e_3)
| equalish(X84,e_4) ),
inference(resolution,[status(thm)],[c179,product_right_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_1,axiom,
group_element(e_1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',element_1) ).
cnf(c41,plain,
( product(e_1,e_1,e_3)
| product(e_2,e_1,e_3)
| product(e_3,e_1,e_3)
| product(e_4,e_1,e_3) ),
inference(resolution,[status(thm)],[c1,element_1]) ).
cnf(c197,plain,
( product(e_2,e_1,e_3)
| product(e_3,e_1,e_3)
| product(e_4,e_1,e_3)
| equalish(e_3,e_1) ),
inference(resolution,[status(thm)],[c41,c17]) ).
cnf(c317,plain,
( product(e_2,e_1,e_3)
| product(e_3,e_1,e_3)
| product(e_4,e_1,e_3) ),
inference(resolution,[status(thm)],[c197,e_3_is_not_e_1]) ).
cnf(c328,plain,
( product(e_2,e_1,e_3)
| product(e_4,e_1,e_3)
| equalish(e_1,e_3) ),
inference(resolution,[status(thm)],[c317,c26]) ).
cnf(c354,plain,
( product(e_2,e_1,e_3)
| product(e_4,e_1,e_3) ),
inference(resolution,[status(thm)],[c328,e_1_is_not_e_3]) ).
cnf(c360,plain,
( product(e_4,e_1,e_3)
| product(e_1,e_4,e_3)
| equalish(e_1,e_4) ),
inference(resolution,[status(thm)],[c354,c187]) ).
cnf(c535,plain,
( product(e_4,e_1,e_3)
| product(e_1,e_4,e_3) ),
inference(resolution,[status(thm)],[c360,e_1_is_not_e_4]) ).
cnf(c539,plain,
( product(e_1,e_4,e_3)
| product(e_1,e_4,X142)
| ~ product(X142,e_3,e_4) ),
inference(resolution,[status(thm)],[c535,qg4_1]) ).
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(c2,plain,
( ~ group_element(X70)
| product(e_1,X70,e_4)
| product(e_2,X70,e_4)
| product(e_3,X70,e_4)
| product(e_4,X70,e_4) ),
inference(resolution,[status(thm)],[row_surjectivity,element_4]) ).
cnf(c51,plain,
( product(e_1,e_3,e_4)
| product(e_2,e_3,e_4)
| product(e_3,e_3,e_4)
| product(e_4,e_3,e_4) ),
inference(resolution,[status(thm)],[c2,element_3]) ).
cnf(c286,plain,
( product(e_1,e_3,e_4)
| product(e_2,e_3,e_4)
| product(e_4,e_3,e_4)
| equalish(e_4,e_3) ),
inference(resolution,[status(thm)],[c51,c17]) ).
cnf(c2829,plain,
( product(e_1,e_3,e_4)
| product(e_2,e_3,e_4)
| product(e_4,e_3,e_4) ),
inference(resolution,[status(thm)],[c286,e_4_is_not_e_3]) ).
cnf(c2866,plain,
( product(e_1,e_3,e_4)
| product(e_2,e_3,e_4)
| equalish(e_3,e_4) ),
inference(resolution,[status(thm)],[c2829,c26]) ).
cnf(c2892,plain,
( product(e_1,e_3,e_4)
| product(e_2,e_3,e_4) ),
inference(resolution,[status(thm)],[c2866,e_3_is_not_e_4]) ).
cnf(c2895,plain,
( product(e_2,e_3,e_4)
| product(e_1,e_4,e_3)
| product(e_1,e_4,e_1) ),
inference(resolution,[status(thm)],[c2892,c539]) ).
cnf(c3131,plain,
( product(e_2,e_3,e_4)
| product(e_1,e_4,e_3)
| equalish(e_4,e_1) ),
inference(resolution,[status(thm)],[c2895,c26]) ).
cnf(c3175,plain,
( product(e_2,e_3,e_4)
| product(e_1,e_4,e_3) ),
inference(resolution,[status(thm)],[c3131,e_4_is_not_e_1]) ).
cnf(c3179,plain,
( product(e_1,e_4,e_3)
| product(e_1,e_4,e_2) ),
inference(resolution,[status(thm)],[c3175,c539]) ).
cnf(c3180,plain,
( product(e_1,e_4,e_3)
| product(e_3,e_2,X456)
| ~ product(X456,e_4,e_2) ),
inference(resolution,[status(thm)],[c3175,qg4_1]) ).
cnf(c3378,plain,
( product(e_1,e_4,e_3)
| product(e_3,e_2,e_1) ),
inference(resolution,[status(thm)],[c3180,c3179]) ).
cnf(c3410,plain,
( product(e_3,e_2,e_1)
| ~ product(e_1,X459,e_3)
| equalish(X459,e_4) ),
inference(resolution,[status(thm)],[c3378,product_right_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(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(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(element_2,axiom,
group_element(e_2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',element_2) ).
cnf(c42,plain,
( product(e_1,e_2,e_3)
| product(e_2,e_2,e_3)
| product(e_3,e_2,e_3)
| product(e_4,e_2,e_3) ),
inference(resolution,[status(thm)],[c1,element_2]) ).
cnf(c238,plain,
( product(e_1,e_2,e_3)
| product(e_3,e_2,e_3)
| product(e_4,e_2,e_3)
| equalish(e_3,e_2) ),
inference(resolution,[status(thm)],[c42,c17]) ).
cnf(c1812,plain,
( product(e_1,e_2,e_3)
| product(e_3,e_2,e_3)
| product(e_4,e_2,e_3) ),
inference(resolution,[status(thm)],[c238,e_3_is_not_e_2]) ).
cnf(c1826,plain,
( product(e_1,e_2,e_3)
| product(e_4,e_2,e_3)
| equalish(e_2,e_3) ),
inference(resolution,[status(thm)],[c1812,c26]) ).
cnf(c1861,plain,
( product(e_1,e_2,e_3)
| product(e_4,e_2,e_3) ),
inference(resolution,[status(thm)],[c1826,e_2_is_not_e_3]) ).
cnf(c1875,plain,
( product(e_1,e_2,e_3)
| product(e_2,e_4,X251)
| ~ product(X251,e_3,e_4) ),
inference(resolution,[status(thm)],[c1861,qg4_1]) ).
cnf(c2906,plain,
( product(e_1,e_3,e_4)
| product(e_1,e_2,e_3)
| product(e_2,e_4,e_2) ),
inference(resolution,[status(thm)],[c2892,c1875]) ).
cnf(c8464,plain,
( product(e_1,e_3,e_4)
| product(e_1,e_2,e_3)
| equalish(e_4,e_2) ),
inference(resolution,[status(thm)],[c2906,c26]) ).
cnf(c8535,plain,
( product(e_1,e_3,e_4)
| product(e_1,e_2,e_3) ),
inference(resolution,[status(thm)],[c8464,e_4_is_not_e_2]) ).
cnf(c8573,plain,
( product(e_1,e_3,e_4)
| product(e_3,e_2,e_1)
| equalish(e_2,e_4) ),
inference(resolution,[status(thm)],[c8535,c3410]) ).
cnf(c10606,plain,
( product(e_1,e_3,e_4)
| product(e_3,e_2,e_1) ),
inference(resolution,[status(thm)],[c8573,e_2_is_not_e_4]) ).
cnf(c10618,plain,
( product(e_3,e_2,e_1)
| ~ product(X733,e_3,e_4)
| equalish(X733,e_1) ),
inference(resolution,[status(thm)],[c10606,product_left_cancellation]) ).
cnf(qg4_2,negated_conjecture,
( product(X15,X18,X17)
| ~ product(X16,X17,X15)
| ~ product(X18,X15,X16) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',qg4_2) ).
cnf(c2898,plain,
( product(e_2,e_3,e_4)
| product(e_3,e_1,X432)
| ~ product(e_4,X432,e_3) ),
inference(resolution,[status(thm)],[c2892,qg4_2]) ).
cnf(c1869,plain,
( product(e_4,e_2,e_3)
| ~ product(e_1,X215,e_3)
| equalish(X215,e_2) ),
inference(resolution,[status(thm)],[c1861,product_right_cancellation]) ).
cnf(c3193,plain,
( product(e_2,e_3,e_4)
| product(e_4,e_2,e_3)
| equalish(e_4,e_2) ),
inference(resolution,[status(thm)],[c3175,c1869]) ).
cnf(c3563,plain,
( product(e_2,e_3,e_4)
| product(e_4,e_2,e_3) ),
inference(resolution,[status(thm)],[c3193,e_4_is_not_e_2]) ).
cnf(c3606,plain,
( product(e_2,e_3,e_4)
| product(e_3,e_1,e_2) ),
inference(resolution,[status(thm)],[c3563,c2898]) ).
cnf(c3676,plain,
( product(e_2,e_3,e_4)
| ~ product(e_3,e_1,X489)
| equalish(X489,e_2) ),
inference(resolution,[status(thm)],[c3606,product_total_function2]) ).
cnf(c367,plain,
( product(e_2,e_1,e_3)
| ~ product(e_4,X128,e_3)
| equalish(X128,e_1) ),
inference(resolution,[status(thm)],[c354,product_right_cancellation]) ).
cnf(c1876,plain,
( product(e_1,e_2,e_3)
| product(e_2,e_1,e_3)
| equalish(e_2,e_1) ),
inference(resolution,[status(thm)],[c1861,c367]) ).
cnf(c2434,plain,
( product(e_1,e_2,e_3)
| product(e_2,e_1,e_3) ),
inference(resolution,[status(thm)],[c1876,e_2_is_not_e_1]) ).
cnf(c2450,plain,
( product(e_2,e_1,e_3)
| ~ product(e_1,X255,e_3)
| equalish(X255,e_2) ),
inference(resolution,[status(thm)],[c2434,product_right_cancellation]) ).
cnf(c3202,plain,
( product(e_2,e_3,e_4)
| product(e_2,e_1,e_3)
| equalish(e_4,e_2) ),
inference(resolution,[status(thm)],[c3175,c2450]) ).
cnf(c4069,plain,
( product(e_2,e_3,e_4)
| product(e_2,e_1,e_3) ),
inference(resolution,[status(thm)],[c3202,e_4_is_not_e_2]) ).
cnf(c4098,plain,
( product(e_2,e_3,e_4)
| ~ product(e_2,e_1,X508)
| equalish(X508,e_3) ),
inference(resolution,[status(thm)],[c4069,product_total_function2]) ).
cnf(c14,plain,
( product(X20,X20,X21)
| ~ product(X20,X21,X20) ),
inference(resolution,[status(thm)],[qg4_2,product_idempotence]) ).
cnf(qg4,negated_conjecture,
( ~ product(X58,X56,X57)
| ~ product(X56,X58,X59)
| product(X57,X59,X56) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',qg4) ).
cnf(c31,plain,
( ~ product(X61,X61,X60)
| product(X60,X60,X61) ),
inference(factor,[status(thm)],[qg4]) ).
cnf(c53,plain,
( product(e_1,e_1,e_4)
| product(e_2,e_1,e_4)
| product(e_3,e_1,e_4)
| product(e_4,e_1,e_4) ),
inference(resolution,[status(thm)],[c2,element_1]) ).
cnf(c375,plain,
( product(e_2,e_1,e_4)
| product(e_3,e_1,e_4)
| product(e_4,e_1,e_4)
| product(e_4,e_4,e_1) ),
inference(resolution,[status(thm)],[c53,c31]) ).
cnf(c5210,plain,
( product(e_2,e_1,e_4)
| product(e_3,e_1,e_4)
| product(e_4,e_4,e_1) ),
inference(resolution,[status(thm)],[c375,c14]) ).
cnf(c29196,plain,
( product(e_2,e_1,e_4)
| product(e_3,e_1,e_4)
| equalish(e_1,e_4) ),
inference(resolution,[status(thm)],[c5210,c17]) ).
cnf(c29303,plain,
( product(e_2,e_1,e_4)
| product(e_3,e_1,e_4) ),
inference(resolution,[status(thm)],[c29196,e_1_is_not_e_4]) ).
cnf(c29305,plain,
( product(e_3,e_1,e_4)
| product(e_2,e_3,e_4)
| equalish(e_4,e_3) ),
inference(resolution,[status(thm)],[c29303,c4098]) ).
cnf(c29636,plain,
( product(e_3,e_1,e_4)
| product(e_2,e_3,e_4) ),
inference(resolution,[status(thm)],[c29305,e_4_is_not_e_3]) ).
cnf(c29652,plain,
( product(e_2,e_3,e_4)
| equalish(e_4,e_2) ),
inference(resolution,[status(thm)],[c29636,c3676]) ).
cnf(c29806,plain,
product(e_2,e_3,e_4),
inference(resolution,[status(thm)],[c29652,e_4_is_not_e_2]) ).
cnf(c29817,plain,
( product(e_3,e_2,e_1)
| equalish(e_2,e_1) ),
inference(resolution,[status(thm)],[c29806,c10618]) ).
cnf(c30104,plain,
product(e_3,e_2,e_1),
inference(resolution,[status(thm)],[c29817,e_2_is_not_e_1]) ).
cnf(c29849,plain,
( ~ product(e_3,e_2,X1075)
| product(X1075,e_4,e_2) ),
inference(resolution,[status(thm)],[c29806,qg4]) ).
cnf(c30381,plain,
product(e_1,e_4,e_2),
inference(resolution,[status(thm)],[c29849,c30104]) ).
cnf(c30434,plain,
( ~ product(e_1,X1078,e_2)
| equalish(X1078,e_4) ),
inference(resolution,[status(thm)],[c30381,product_right_cancellation]) ).
cnf(c181,plain,
( product(e_2,e_4,e_3)
| ~ product(e_1,X81,e_3)
| equalish(X81,e_4) ),
inference(resolution,[status(thm)],[c179,product_right_cancellation]) ).
cnf(c1867,plain,
( product(e_4,e_2,e_3)
| product(e_2,e_4,e_3)
| equalish(e_2,e_4) ),
inference(resolution,[status(thm)],[c1861,c181]) ).
cnf(c2034,plain,
( product(e_4,e_2,e_3)
| product(e_2,e_4,e_3) ),
inference(resolution,[status(thm)],[c1867,e_2_is_not_e_4]) ).
cnf(c2042,plain,
( product(e_2,e_4,e_3)
| ~ product(X225,e_2,e_3)
| equalish(X225,e_4) ),
inference(resolution,[status(thm)],[c2034,product_left_cancellation]) ).
cnf(c8572,plain,
( product(e_1,e_3,e_4)
| product(e_2,e_4,e_3)
| equalish(e_1,e_4) ),
inference(resolution,[status(thm)],[c8535,c2042]) ).
cnf(c9875,plain,
( product(e_1,e_3,e_4)
| product(e_2,e_4,e_3) ),
inference(resolution,[status(thm)],[c8572,e_1_is_not_e_4]) ).
cnf(c9906,plain,
( product(e_2,e_4,e_3)
| ~ product(X717,e_3,e_4)
| equalish(X717,e_1) ),
inference(resolution,[status(thm)],[c9875,product_left_cancellation]) ).
cnf(c29856,plain,
( product(e_2,e_4,e_3)
| equalish(e_2,e_1) ),
inference(resolution,[status(thm)],[c29806,c9906]) ).
cnf(c30546,plain,
product(e_2,e_4,e_3),
inference(resolution,[status(thm)],[c29856,e_2_is_not_e_1]) ).
cnf(c29347,plain,
( product(e_3,e_1,e_4)
| ~ product(e_2,X1054,e_4)
| equalish(X1054,e_1) ),
inference(resolution,[status(thm)],[c29303,product_right_cancellation]) ).
cnf(c29698,plain,
( product(e_3,e_1,e_4)
| equalish(e_3,e_1) ),
inference(resolution,[status(thm)],[c29636,c29347]) ).
cnf(c29961,plain,
product(e_3,e_1,e_4),
inference(resolution,[status(thm)],[c29698,e_3_is_not_e_1]) ).
cnf(c29992,plain,
( product(e_1,e_3,X1088)
| ~ product(X1088,e_4,e_3) ),
inference(resolution,[status(thm)],[c29961,qg4_1]) ).
cnf(c30886,plain,
product(e_1,e_3,e_2),
inference(resolution,[status(thm)],[c29992,c30546]) ).
cnf(c30915,plain,
equalish(e_3,e_4),
inference(resolution,[status(thm)],[c30886,c30434]) ).
cnf(c30916,plain,
$false,
inference(resolution,[status(thm)],[c30915,e_3_is_not_e_4]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : GRP126-4.004 : TPTP v8.1.2. Bugfixed v1.2.1.
% 0.07/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.34 % Computer : n023.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:55:38 EDT 2024
% 0.13/0.34 % CPUTime :
% 36.08/36.30 % Version: 1.5
% 36.08/36.30 % SZS status Unsatisfiable
% 36.08/36.30 % SZS output start CNFRefutation
% See solution above
% 36.08/36.31
% 36.08/36.31 % Initial clauses : 26
% 36.08/36.31 % Processed clauses : 916
% 36.08/36.31 % Factors computed : 9
% 36.08/36.31 % Resolvents computed: 30908
% 36.08/36.31 % Tautologies deleted: 2
% 36.08/36.31 % Forward subsumed : 3052
% 36.08/36.31 % Backward subsumed : 587
% 36.08/36.31 % -------- CPU Time ---------
% 36.08/36.31 % User time : 35.862 s
% 36.08/36.31 % System time : 0.099 s
% 36.08/36.31 % Total time : 35.961 s
%------------------------------------------------------------------------------