%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GRP127-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:10 EDT 2024
% Result : Unsatisfiable 15.28s 15.52s
% Output : Refutation 15.28s
% Verified :
% SZS Type : Refutation
% Derivation depth : 37
% Number of leaves : 23
% Syntax : Number of clauses : 115 ( 24 unt; 78 nHn; 114 RR)
% Number of literals : 288 ( 0 equ; 51 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 : 55 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
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_total_function2,axiom,
( ~ product(X25,X26,X27)
| ~ product(X25,X26,X28)
| equalish(X27,X28) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',product_total_function2) ).
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(product_right_cancellation,axiom,
( ~ product(X38,X40,X39)
| ~ product(X38,X41,X39)
| equalish(X40,X41) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',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(product_idempotence,axiom,
product(X2,X2,X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',product_idempotence) ).
cnf(c18,plain,
( ~ product(X35,X35,X36)
| equalish(X36,X35) ),
inference(resolution,[status(thm)],[product_total_function2,product_idempotence]) ).
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(c27,plain,
( ~ product(X49,X50,X49)
| equalish(X50,X49) ),
inference(resolution,[status(thm)],[product_right_cancellation,product_idempotence]) ).
cnf(element_3,axiom,
group_element(e_3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',element_3) ).
cnf(element_2,axiom,
group_element(e_2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',element_2) ).
cnf(row_surjectivity,axiom,
( ~ group_element(X3)
| ~ group_element(X4)
| product(e_1,X3,X4)
| product(e_2,X3,X4)
| product(e_3,X3,X4)
| product(e_4,X3,X4) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',row_surjectivity) ).
cnf(c1,plain,
( ~ group_element(X67)
| product(e_1,X67,e_2)
| product(e_2,X67,e_2)
| product(e_3,X67,e_2)
| product(e_4,X67,e_2) ),
inference(resolution,[status(thm)],[row_surjectivity,element_2]) ).
cnf(c40,plain,
( product(e_1,e_3,e_2)
| product(e_2,e_3,e_2)
| product(e_3,e_3,e_2)
| product(e_4,e_3,e_2) ),
inference(resolution,[status(thm)],[c1,element_3]) ).
cnf(c108,plain,
( product(e_1,e_3,e_2)
| product(e_3,e_3,e_2)
| product(e_4,e_3,e_2)
| equalish(e_3,e_2) ),
inference(resolution,[status(thm)],[c40,c27]) ).
cnf(c144,plain,
( product(e_1,e_3,e_2)
| product(e_3,e_3,e_2)
| product(e_4,e_3,e_2) ),
inference(resolution,[status(thm)],[c108,e_3_is_not_e_2]) ).
cnf(c153,plain,
( product(e_1,e_3,e_2)
| product(e_4,e_3,e_2)
| equalish(e_2,e_3) ),
inference(resolution,[status(thm)],[c144,c18]) ).
cnf(c177,plain,
( product(e_1,e_3,e_2)
| product(e_4,e_3,e_2) ),
inference(resolution,[status(thm)],[c153,e_2_is_not_e_3]) ).
cnf(c189,plain,
( product(e_1,e_3,e_2)
| ~ product(e_4,X86,e_2)
| equalish(X86,e_3) ),
inference(resolution,[status(thm)],[c177,product_right_cancellation]) ).
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(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(element_1,axiom,
group_element(e_1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',element_1) ).
cnf(c42,plain,
( product(e_1,e_1,e_2)
| product(e_2,e_1,e_2)
| product(e_3,e_1,e_2)
| product(e_4,e_1,e_2) ),
inference(resolution,[status(thm)],[c1,element_1]) ).
cnf(c226,plain,
( product(e_2,e_1,e_2)
| product(e_3,e_1,e_2)
| product(e_4,e_1,e_2)
| equalish(e_2,e_1) ),
inference(resolution,[status(thm)],[c42,c18]) ).
cnf(c1073,plain,
( product(e_2,e_1,e_2)
| product(e_3,e_1,e_2)
| product(e_4,e_1,e_2) ),
inference(resolution,[status(thm)],[c226,e_2_is_not_e_1]) ).
cnf(c1080,plain,
( product(e_3,e_1,e_2)
| product(e_4,e_1,e_2)
| equalish(e_1,e_2) ),
inference(resolution,[status(thm)],[c1073,c27]) ).
cnf(c1115,plain,
( product(e_3,e_1,e_2)
| product(e_4,e_1,e_2) ),
inference(resolution,[status(thm)],[c1080,e_1_is_not_e_2]) ).
cnf(c1129,plain,
( product(e_3,e_1,e_2)
| product(e_1,e_3,e_2)
| equalish(e_1,e_3) ),
inference(resolution,[status(thm)],[c1115,c189]) ).
cnf(c1864,plain,
( product(e_3,e_1,e_2)
| product(e_1,e_3,e_2) ),
inference(resolution,[status(thm)],[c1129,e_1_is_not_e_3]) ).
cnf(c1868,plain,
( product(e_1,e_3,e_2)
| ~ product(e_3,e_1,X209)
| equalish(X209,e_2) ),
inference(resolution,[status(thm)],[c1864,product_total_function2]) ).
cnf(qg3_2,negated_conjecture,
( product(X17,X16,X18)
| ~ product(X18,X16,X19)
| ~ product(X16,X19,X17) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',qg3_2) ).
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(product_left_cancellation,axiom,
( ~ product(X43,X42,X44)
| ~ product(X45,X42,X44)
| equalish(X43,X45) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',product_left_cancellation) ).
cnf(e_1_is_not_e_4,axiom,
~ equalish(e_1,e_4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_1_is_not_e_4) ).
cnf(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(element_4,axiom,
group_element(e_4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',element_4) ).
cnf(c41,plain,
( product(e_1,e_4,e_2)
| product(e_2,e_4,e_2)
| product(e_3,e_4,e_2)
| product(e_4,e_4,e_2) ),
inference(resolution,[status(thm)],[c1,element_4]) ).
cnf(c203,plain,
( product(e_1,e_4,e_2)
| product(e_3,e_4,e_2)
| product(e_4,e_4,e_2)
| equalish(e_4,e_2) ),
inference(resolution,[status(thm)],[c41,c27]) ).
cnf(c311,plain,
( product(e_1,e_4,e_2)
| product(e_3,e_4,e_2)
| product(e_4,e_4,e_2) ),
inference(resolution,[status(thm)],[c203,e_4_is_not_e_2]) ).
cnf(c325,plain,
( product(e_1,e_4,e_2)
| product(e_3,e_4,e_2)
| equalish(e_2,e_4) ),
inference(resolution,[status(thm)],[c311,c18]) ).
cnf(c347,plain,
( product(e_1,e_4,e_2)
| product(e_3,e_4,e_2) ),
inference(resolution,[status(thm)],[c325,e_2_is_not_e_4]) ).
cnf(c360,plain,
( product(e_1,e_4,e_2)
| ~ product(e_3,X128,e_2)
| equalish(X128,e_4) ),
inference(resolution,[status(thm)],[c347,product_right_cancellation]) ).
cnf(c1117,plain,
( product(e_4,e_1,e_2)
| product(e_1,e_4,e_2)
| equalish(e_1,e_4) ),
inference(resolution,[status(thm)],[c1115,c360]) ).
cnf(c1292,plain,
( product(e_4,e_1,e_2)
| product(e_1,e_4,e_2) ),
inference(resolution,[status(thm)],[c1117,e_1_is_not_e_4]) ).
cnf(c1302,plain,
( product(e_1,e_4,e_2)
| product(e_1,e_3,e_2)
| equalish(e_1,e_3) ),
inference(resolution,[status(thm)],[c1292,c189]) ).
cnf(c2256,plain,
( product(e_1,e_4,e_2)
| product(e_1,e_3,e_2) ),
inference(resolution,[status(thm)],[c1302,e_1_is_not_e_3]) ).
cnf(c2286,plain,
( product(e_1,e_4,e_2)
| ~ product(X222,e_3,e_2)
| equalish(X222,e_1) ),
inference(resolution,[status(thm)],[c2256,product_left_cancellation]) ).
cnf(c2,plain,
( ~ group_element(X70)
| product(e_1,X70,e_3)
| product(e_2,X70,e_3)
| product(e_3,X70,e_3)
| product(e_4,X70,e_3) ),
inference(resolution,[status(thm)],[row_surjectivity,element_3]) ).
cnf(c51,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)],[c2,element_2]) ).
cnf(c266,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)],[c51,c18]) ).
cnf(c2763,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)],[c266,e_3_is_not_e_2]) ).
cnf(c2779,plain,
( product(e_1,e_2,e_3)
| product(e_4,e_2,e_3)
| equalish(e_2,e_3) ),
inference(resolution,[status(thm)],[c2763,c27]) ).
cnf(c2809,plain,
( product(e_1,e_2,e_3)
| product(e_4,e_2,e_3) ),
inference(resolution,[status(thm)],[c2779,e_2_is_not_e_3]) ).
cnf(c2817,plain,
( product(e_4,e_2,e_3)
| product(e_3,e_1,X413)
| ~ product(X413,e_1,e_2) ),
inference(resolution,[status(thm)],[c2809,qg3_2]) ).
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(c183,plain,
( product(e_4,e_3,e_2)
| ~ product(e_1,X83,e_2)
| equalish(X83,e_3) ),
inference(resolution,[status(thm)],[c177,product_right_cancellation]) ).
cnf(c354,plain,
( product(e_3,e_4,e_2)
| product(e_4,e_3,e_2)
| equalish(e_4,e_3) ),
inference(resolution,[status(thm)],[c347,c183]) ).
cnf(c491,plain,
( product(e_3,e_4,e_2)
| product(e_4,e_3,e_2) ),
inference(resolution,[status(thm)],[c354,e_4_is_not_e_3]) ).
cnf(c501,plain,
( product(e_4,e_3,e_2)
| ~ product(e_3,X134,e_2)
| equalish(X134,e_4) ),
inference(resolution,[status(thm)],[c491,product_right_cancellation]) ).
cnf(c1119,plain,
( product(e_4,e_1,e_2)
| product(e_4,e_3,e_2)
| equalish(e_1,e_4) ),
inference(resolution,[status(thm)],[c1115,c501]) ).
cnf(c1424,plain,
( product(e_4,e_1,e_2)
| product(e_4,e_3,e_2) ),
inference(resolution,[status(thm)],[c1119,e_1_is_not_e_4]) ).
cnf(c1444,plain,
( product(e_4,e_1,e_2)
| ~ product(X196,e_3,e_2)
| equalish(X196,e_4) ),
inference(resolution,[status(thm)],[c1424,product_left_cancellation]) ).
cnf(c1872,plain,
( product(e_1,e_3,e_2)
| ~ product(X210,e_1,e_2)
| equalish(X210,e_3) ),
inference(resolution,[status(thm)],[c1864,product_left_cancellation]) ).
cnf(qg3,negated_conjecture,
( ~ product(X57,X60,X58)
| ~ product(X58,X57,X59)
| product(X59,X57,X60) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',qg3) ).
cnf(c1878,plain,
( product(e_1,e_3,e_2)
| ~ product(e_1,X261,e_3)
| product(e_2,e_1,X261) ),
inference(resolution,[status(thm)],[c1864,qg3]) ).
cnf(c2810,plain,
( product(e_4,e_2,e_3)
| product(e_1,e_3,e_2)
| product(e_2,e_1,e_2) ),
inference(resolution,[status(thm)],[c2809,c1878]) ).
cnf(c2984,plain,
( product(e_4,e_2,e_3)
| product(e_1,e_3,e_2)
| equalish(e_2,e_3) ),
inference(resolution,[status(thm)],[c2810,c1872]) ).
cnf(c3026,plain,
( product(e_4,e_2,e_3)
| product(e_1,e_3,e_2) ),
inference(resolution,[status(thm)],[c2984,e_2_is_not_e_3]) ).
cnf(c3043,plain,
( product(e_4,e_2,e_3)
| product(e_4,e_1,e_2)
| equalish(e_1,e_4) ),
inference(resolution,[status(thm)],[c3026,c1444]) ).
cnf(c3296,plain,
( product(e_4,e_2,e_3)
| product(e_4,e_1,e_2) ),
inference(resolution,[status(thm)],[c3043,e_1_is_not_e_4]) ).
cnf(c3315,plain,
( product(e_4,e_2,e_3)
| product(e_3,e_1,e_4) ),
inference(resolution,[status(thm)],[c3296,c2817]) ).
cnf(c3345,plain,
( product(e_3,e_1,e_4)
| ~ product(X449,e_2,e_3)
| equalish(X449,e_4) ),
inference(resolution,[status(thm)],[c3315,product_left_cancellation]) ).
cnf(c495,plain,
( product(e_4,e_3,e_2)
| ~ product(X133,e_4,e_2)
| equalish(X133,e_3) ),
inference(resolution,[status(thm)],[c491,product_left_cancellation]) ).
cnf(c497,plain,
( product(e_4,e_3,e_2)
| ~ product(e_4,X142,e_3)
| product(e_2,e_4,X142) ),
inference(resolution,[status(thm)],[c491,qg3]) ).
cnf(c2820,plain,
( product(e_1,e_2,e_3)
| product(e_4,e_3,e_2)
| product(e_2,e_4,e_2) ),
inference(resolution,[status(thm)],[c2809,c497]) ).
cnf(c4818,plain,
( product(e_1,e_2,e_3)
| product(e_4,e_3,e_2)
| equalish(e_2,e_3) ),
inference(resolution,[status(thm)],[c2820,c495]) ).
cnf(c4881,plain,
( product(e_1,e_2,e_3)
| product(e_4,e_3,e_2) ),
inference(resolution,[status(thm)],[c4818,e_2_is_not_e_3]) ).
cnf(c4894,plain,
( product(e_4,e_3,e_2)
| product(e_3,e_1,e_4)
| equalish(e_1,e_4) ),
inference(resolution,[status(thm)],[c4881,c3345]) ).
cnf(c5318,plain,
( product(e_4,e_3,e_2)
| product(e_3,e_1,e_4) ),
inference(resolution,[status(thm)],[c4894,e_1_is_not_e_4]) ).
cnf(c5320,plain,
( product(e_3,e_1,e_4)
| product(e_1,e_4,e_2)
| equalish(e_4,e_1) ),
inference(resolution,[status(thm)],[c5318,c2286]) ).
cnf(c7117,plain,
( product(e_3,e_1,e_4)
| product(e_1,e_4,e_2) ),
inference(resolution,[status(thm)],[c5320,e_4_is_not_e_1]) ).
cnf(c7176,plain,
( product(e_3,e_1,e_4)
| product(e_2,e_1,X732)
| ~ product(X732,e_1,e_4) ),
inference(resolution,[status(thm)],[c7117,qg3_2]) ).
cnf(c3,plain,
( ~ group_element(X71)
| product(e_1,X71,e_4)
| product(e_2,X71,e_4)
| product(e_3,X71,e_4)
| product(e_4,X71,e_4) ),
inference(resolution,[status(thm)],[row_surjectivity,element_4]) ).
cnf(c58,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)],[c3,element_1]) ).
cnf(c561,plain,
( product(e_2,e_1,e_4)
| product(e_3,e_1,e_4)
| product(e_4,e_1,e_4)
| equalish(e_4,e_1) ),
inference(resolution,[status(thm)],[c58,c18]) ).
cnf(c13219,plain,
( product(e_2,e_1,e_4)
| product(e_3,e_1,e_4)
| equalish(e_4,e_1) ),
inference(resolution,[status(thm)],[c561,c7176]) ).
cnf(c13831,plain,
( product(e_2,e_1,e_4)
| product(e_3,e_1,e_4) ),
inference(resolution,[status(thm)],[c13219,e_4_is_not_e_1]) ).
cnf(c14041,plain,
( product(e_3,e_1,e_4)
| product(e_2,e_1,e_2) ),
inference(resolution,[status(thm)],[c13831,c7176]) ).
cnf(c14171,plain,
( product(e_3,e_1,e_4)
| equalish(e_1,e_2) ),
inference(resolution,[status(thm)],[c14041,c27]) ).
cnf(c14248,plain,
product(e_3,e_1,e_4),
inference(resolution,[status(thm)],[c14171,e_1_is_not_e_2]) ).
cnf(c14262,plain,
( product(e_1,e_3,e_2)
| equalish(e_4,e_2) ),
inference(resolution,[status(thm)],[c14248,c1868]) ).
cnf(c14566,plain,
product(e_1,e_3,e_2),
inference(resolution,[status(thm)],[c14262,e_4_is_not_e_2]) ).
cnf(c14583,plain,
( ~ product(e_1,e_3,X787)
| equalish(X787,e_2) ),
inference(resolution,[status(thm)],[c14566,product_total_function2]) ).
cnf(qg3_1,negated_conjecture,
( product(X7,X10,X8)
| ~ product(X9,X7,X10)
| ~ product(X8,X7,X9) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',qg3_1) ).
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(c1131,plain,
( product(e_3,e_1,e_2)
| ~ product(e_4,X185,e_2)
| equalish(X185,e_1) ),
inference(resolution,[status(thm)],[c1115,product_right_cancellation]) ).
cnf(c4910,plain,
( product(e_1,e_2,e_3)
| product(e_3,e_1,e_2)
| equalish(e_3,e_1) ),
inference(resolution,[status(thm)],[c4881,c1131]) ).
cnf(c6313,plain,
( product(e_1,e_2,e_3)
| product(e_3,e_1,e_2) ),
inference(resolution,[status(thm)],[c4910,e_3_is_not_e_1]) ).
cnf(c6390,plain,
( product(e_1,e_2,e_3)
| ~ product(e_3,e_1,X621)
| equalish(X621,e_2) ),
inference(resolution,[status(thm)],[c6313,product_total_function2]) ).
cnf(c14251,plain,
( product(e_1,e_2,e_3)
| equalish(e_4,e_2) ),
inference(resolution,[status(thm)],[c14248,c6390]) ).
cnf(c14368,plain,
product(e_1,e_2,e_3),
inference(resolution,[status(thm)],[c14251,e_4_is_not_e_2]) ).
cnf(c14252,plain,
( ~ product(e_1,X780,e_3)
| product(e_4,e_1,X780) ),
inference(resolution,[status(thm)],[c14248,qg3]) ).
cnf(c14454,plain,
product(e_4,e_1,e_2),
inference(resolution,[status(thm)],[c14252,c14368]) ).
cnf(c14503,plain,
( product(e_1,X809,e_4)
| ~ product(e_2,e_1,X809) ),
inference(resolution,[status(thm)],[c14454,qg3_1]) ).
cnf(c14491,plain,
( ~ product(e_4,e_1,X782)
| equalish(X782,e_2) ),
inference(resolution,[status(thm)],[c14454,product_total_function2]) ).
cnf(c54,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)],[c2,element_1]) ).
cnf(c403,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)],[c54,c18]) ).
cnf(c14580,plain,
( product(e_2,e_1,X811)
| ~ product(X811,e_1,e_3) ),
inference(resolution,[status(thm)],[c14566,qg3_2]) ).
cnf(c15133,plain,
( product(e_2,e_1,e_3)
| product(e_4,e_1,e_3)
| equalish(e_3,e_1) ),
inference(resolution,[status(thm)],[c14580,c403]) ).
cnf(c16928,plain,
( product(e_2,e_1,e_3)
| product(e_4,e_1,e_3) ),
inference(resolution,[status(thm)],[c15133,e_3_is_not_e_1]) ).
cnf(c16958,plain,
( product(e_2,e_1,e_3)
| equalish(e_3,e_2) ),
inference(resolution,[status(thm)],[c16928,c14491]) ).
cnf(c16981,plain,
product(e_2,e_1,e_3),
inference(resolution,[status(thm)],[c16958,e_3_is_not_e_2]) ).
cnf(c16986,plain,
product(e_1,e_3,e_4),
inference(resolution,[status(thm)],[c16981,c14503]) ).
cnf(c17009,plain,
equalish(e_4,e_2),
inference(resolution,[status(thm)],[c16986,c14583]) ).
cnf(c17019,plain,
$false,
inference(resolution,[status(thm)],[c17009,e_4_is_not_e_2]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : GRP127-4.004 : TPTP v8.1.2. Bugfixed v1.2.1.
% 0.03/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:08 EDT 2024
% 0.13/0.35 % CPUTime :
% 15.28/15.52 % Version: 1.5
% 15.28/15.52 % SZS status Unsatisfiable
% 15.28/15.52 % SZS output start CNFRefutation
% See solution above
% 15.28/15.52
% 15.28/15.52 % Initial clauses : 26
% 15.28/15.52 % Processed clauses : 693
% 15.28/15.52 % Factors computed : 9
% 15.28/15.52 % Resolvents computed: 17011
% 15.28/15.52 % Tautologies deleted: 2
% 15.28/15.52 % Forward subsumed : 2049
% 15.28/15.52 % Backward subsumed : 469
% 15.28/15.52 % -------- CPU Time ---------
% 15.28/15.52 % User time : 15.103 s
% 15.28/15.52 % System time : 0.066 s
% 15.28/15.52 % Total time : 15.169 s
%------------------------------------------------------------------------------