%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GRP130-1.003 : TPTP v8.1.2. Released v1.2.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n004.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu May 9 17:23:12 EDT 2024
% Result : Unsatisfiable 58.15s 58.33s
% Output : Refutation 58.15s
% Verified :
% SZS Type : Refutation
% Derivation depth : 24
% Number of leaves : 13
% Syntax : Number of clauses : 91 ( 15 unt; 67 nHn; 91 RR)
% Number of literals : 257 ( 0 equ; 43 neg)
% Maximal clause size : 5 ( 2 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 4 ( 3 usr; 1 prp; 0-3 aty)
% Number of functors : 3 ( 3 usr; 3 con; 0-0 aty)
% Number of variables : 47 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
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_total_function2,axiom,
( ~ product(X3,X5,X2)
| ~ product(X3,X5,X4)
| equalish(X2,X4) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',product_total_function2) ).
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(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(X18,X21,X19)
| ~ product(X20,X21,X19)
| equalish(X18,X20) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',product_left_cancellation) ).
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_1,axiom,
group_element(e_1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',element_1) ).
cnf(product_total_function1,axiom,
( ~ group_element(X9)
| ~ group_element(X10)
| product(X9,X10,e_1)
| product(X9,X10,e_2)
| product(X9,X10,e_3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',product_total_function1) ).
cnf(c1,plain,
( ~ group_element(X29)
| product(X29,X29,e_1)
| product(X29,X29,e_2)
| product(X29,X29,e_3) ),
inference(factor,[status(thm)],[product_total_function1]) ).
cnf(c8,plain,
( product(e_1,e_1,e_1)
| product(e_1,e_1,e_2)
| product(e_1,e_1,e_3) ),
inference(resolution,[status(thm)],[c1,element_1]) ).
cnf(c41,plain,
( product(e_1,e_1,e_1)
| product(e_1,e_1,e_2)
| ~ product(X58,e_1,e_3)
| equalish(X58,e_1) ),
inference(resolution,[status(thm)],[c8,product_left_cancellation]) ).
cnf(qg3,negated_conjecture,
( ~ product(X26,X28,X27)
| ~ product(X26,X27,X25)
| product(X25,X28,X26) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',qg3) ).
cnf(c7,plain,
( ~ product(X31,X30,X30)
| product(X30,X30,X31) ),
inference(factor,[status(thm)],[qg3]) ).
cnf(element_2,axiom,
group_element(e_2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',element_2) ).
cnf(c2,plain,
( ~ group_element(X32)
| product(X32,e_1,e_1)
| product(X32,e_1,e_2)
| product(X32,e_1,e_3) ),
inference(resolution,[status(thm)],[product_total_function1,element_1]) ).
cnf(c12,plain,
( product(e_2,e_1,e_1)
| product(e_2,e_1,e_2)
| product(e_2,e_1,e_3) ),
inference(resolution,[status(thm)],[c2,element_2]) ).
cnf(c110,plain,
( product(e_2,e_1,e_2)
| product(e_2,e_1,e_3)
| product(e_1,e_1,e_2) ),
inference(resolution,[status(thm)],[c12,c7]) ).
cnf(c410,plain,
( product(e_2,e_1,e_2)
| product(e_1,e_1,e_2)
| product(e_1,e_1,e_1)
| equalish(e_2,e_1) ),
inference(resolution,[status(thm)],[c110,c41]) ).
cnf(c2774,plain,
( product(e_2,e_1,e_2)
| product(e_1,e_1,e_2)
| product(e_1,e_1,e_1) ),
inference(resolution,[status(thm)],[c410,e_2_is_not_e_1]) ).
cnf(c2822,plain,
( product(e_2,e_1,e_2)
| product(e_1,e_1,e_1)
| ~ product(e_1,e_1,X268)
| equalish(X268,e_2) ),
inference(resolution,[status(thm)],[c2774,product_total_function2]) ).
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(c34,plain,
( product(e_1,e_1,e_1)
| product(e_1,e_1,e_3)
| ~ product(X54,e_1,e_2)
| equalish(X54,e_1) ),
inference(resolution,[status(thm)],[c8,product_left_cancellation]) ).
cnf(element_3,axiom,
group_element(e_3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',element_3) ).
cnf(c13,plain,
( product(e_3,e_1,e_1)
| product(e_3,e_1,e_2)
| product(e_3,e_1,e_3) ),
inference(resolution,[status(thm)],[c2,element_3]) ).
cnf(c147,plain,
( product(e_3,e_1,e_2)
| product(e_3,e_1,e_3)
| product(e_1,e_1,e_3) ),
inference(resolution,[status(thm)],[c13,c7]) ).
cnf(c441,plain,
( product(e_3,e_1,e_3)
| product(e_1,e_1,e_3)
| product(e_1,e_1,e_1)
| equalish(e_3,e_1) ),
inference(resolution,[status(thm)],[c147,c34]) ).
cnf(c4014,plain,
( product(e_3,e_1,e_3)
| product(e_1,e_1,e_3)
| product(e_1,e_1,e_1) ),
inference(resolution,[status(thm)],[c441,e_3_is_not_e_1]) ).
cnf(c4058,plain,
( product(e_3,e_1,e_3)
| product(e_1,e_1,e_1)
| product(e_2,e_1,e_2)
| equalish(e_3,e_2) ),
inference(resolution,[status(thm)],[c4014,c2822]) ).
cnf(c12068,plain,
( product(e_3,e_1,e_3)
| product(e_1,e_1,e_1)
| product(e_2,e_1,e_2) ),
inference(resolution,[status(thm)],[c4058,e_3_is_not_e_2]) ).
cnf(c12277,plain,
( product(e_3,e_1,e_3)
| product(e_1,e_1,e_1)
| ~ product(X343,e_1,e_2)
| equalish(X343,e_2) ),
inference(resolution,[status(thm)],[c12068,product_left_cancellation]) ).
cnf(c2795,plain,
( product(e_1,e_1,e_2)
| product(e_1,e_1,e_1)
| ~ product(e_2,e_1,X265)
| equalish(X265,e_2) ),
inference(resolution,[status(thm)],[c2774,product_total_function2]) ).
cnf(product_right_cancellation,axiom,
( ~ product(X12,X11,X14)
| ~ product(X12,X13,X14)
| equalish(X11,X13) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',product_right_cancellation) ).
cnf(c401,plain,
( product(e_2,e_1,e_3)
| product(e_1,e_1,e_2)
| ~ product(e_2,X209,e_2)
| equalish(X209,e_1) ),
inference(resolution,[status(thm)],[c110,product_right_cancellation]) ).
cnf(c9,plain,
( product(e_2,e_2,e_1)
| product(e_2,e_2,e_2)
| product(e_2,e_2,e_3) ),
inference(resolution,[status(thm)],[c1,element_2]) ).
cnf(c42,plain,
( product(e_2,e_2,e_2)
| product(e_2,e_2,e_3)
| ~ product(e_2,X59,e_2)
| product(e_1,X59,e_2) ),
inference(resolution,[status(thm)],[c9,qg3]) ).
cnf(c399,plain,
( product(e_2,e_1,e_3)
| product(e_1,e_1,e_2)
| product(e_2,e_2,e_2)
| product(e_2,e_2,e_3) ),
inference(resolution,[status(thm)],[c110,c42]) ).
cnf(c4428,plain,
( product(e_2,e_1,e_3)
| product(e_1,e_1,e_2)
| product(e_2,e_2,e_3)
| equalish(e_2,e_1) ),
inference(resolution,[status(thm)],[c399,c401]) ).
cnf(c14130,plain,
( product(e_2,e_1,e_3)
| product(e_1,e_1,e_2)
| product(e_2,e_2,e_3) ),
inference(resolution,[status(thm)],[c4428,e_2_is_not_e_1]) ).
cnf(c14231,plain,
( product(e_2,e_1,e_3)
| product(e_1,e_1,e_2)
| ~ product(e_2,X355,e_3)
| equalish(X355,e_2) ),
inference(resolution,[status(thm)],[c14130,product_right_cancellation]) ).
cnf(c119,plain,
( product(e_2,e_1,e_1)
| product(e_2,e_1,e_3)
| ~ product(e_2,X131,e_2)
| equalish(X131,e_1) ),
inference(resolution,[status(thm)],[c12,product_right_cancellation]) ).
cnf(c4,plain,
( ~ group_element(X34)
| product(X34,e_3,e_1)
| product(X34,e_3,e_2)
| product(X34,e_3,e_3) ),
inference(resolution,[status(thm)],[product_total_function1,element_3]) ).
cnf(c18,plain,
( product(e_2,e_3,e_1)
| product(e_2,e_3,e_2)
| product(e_2,e_3,e_3) ),
inference(resolution,[status(thm)],[c4,element_2]) ).
cnf(c115,plain,
( product(e_2,e_1,e_1)
| product(e_2,e_1,e_3)
| ~ product(e_2,X130,e_1)
| product(e_2,X130,e_2) ),
inference(resolution,[status(thm)],[c12,qg3]) ).
cnf(c653,plain,
( product(e_2,e_1,e_1)
| product(e_2,e_1,e_3)
| product(e_2,e_3,e_2)
| product(e_2,e_3,e_3) ),
inference(resolution,[status(thm)],[c115,c18]) ).
cnf(c13519,plain,
( product(e_2,e_1,e_1)
| product(e_2,e_1,e_3)
| product(e_2,e_3,e_3)
| equalish(e_3,e_1) ),
inference(resolution,[status(thm)],[c653,c119]) ).
cnf(c55682,plain,
( product(e_2,e_1,e_1)
| product(e_2,e_1,e_3)
| product(e_2,e_3,e_3) ),
inference(resolution,[status(thm)],[c13519,e_3_is_not_e_1]) ).
cnf(c55713,plain,
( product(e_2,e_1,e_3)
| product(e_2,e_3,e_3)
| product(e_1,e_1,e_2) ),
inference(resolution,[status(thm)],[c55682,c7]) ).
cnf(c56358,plain,
( product(e_2,e_1,e_3)
| product(e_1,e_1,e_2)
| equalish(e_3,e_2) ),
inference(resolution,[status(thm)],[c55713,c14231]) ).
cnf(c56749,plain,
( product(e_1,e_1,e_2)
| equalish(e_3,e_2)
| product(e_1,e_1,e_1) ),
inference(resolution,[status(thm)],[c56358,c2795]) ).
cnf(c57764,plain,
( product(e_1,e_1,e_2)
| product(e_1,e_1,e_1) ),
inference(resolution,[status(thm)],[c56749,e_3_is_not_e_2]) ).
cnf(c57849,plain,
( product(e_1,e_1,e_1)
| product(e_3,e_1,e_3)
| equalish(e_1,e_2) ),
inference(resolution,[status(thm)],[c57764,c12277]) ).
cnf(c62899,plain,
( product(e_1,e_1,e_1)
| product(e_3,e_1,e_3) ),
inference(resolution,[status(thm)],[c57849,e_1_is_not_e_2]) ).
cnf(c62913,plain,
( product(e_3,e_1,e_3)
| ~ product(e_1,e_1,X549)
| equalish(X549,e_1) ),
inference(resolution,[status(thm)],[c62899,product_total_function2]) ).
cnf(c277,plain,
( product(e_2,e_3,e_2)
| product(e_2,e_3,e_3)
| ~ product(e_2,X192,e_3)
| product(e_1,X192,e_2) ),
inference(resolution,[status(thm)],[c18,qg3]) ).
cnf(c281,plain,
( product(e_2,e_3,e_2)
| product(e_2,e_3,e_3)
| ~ product(e_2,X193,e_1)
| equalish(X193,e_3) ),
inference(resolution,[status(thm)],[c18,product_right_cancellation]) ).
cnf(c13471,plain,
( product(e_2,e_1,e_3)
| product(e_2,e_3,e_2)
| product(e_2,e_3,e_3)
| equalish(e_1,e_3) ),
inference(resolution,[status(thm)],[c653,c281]) ).
cnf(c47551,plain,
( product(e_2,e_1,e_3)
| product(e_2,e_3,e_2)
| product(e_2,e_3,e_3) ),
inference(resolution,[status(thm)],[c13471,e_1_is_not_e_3]) ).
cnf(c47570,plain,
( product(e_2,e_3,e_2)
| product(e_2,e_3,e_3)
| product(e_1,e_1,e_2) ),
inference(resolution,[status(thm)],[c47551,c277]) ).
cnf(c48020,plain,
( product(e_2,e_3,e_2)
| product(e_1,e_1,e_2)
| ~ product(e_2,X485,e_3)
| equalish(X485,e_3) ),
inference(resolution,[status(thm)],[c47570,product_right_cancellation]) ).
cnf(c56821,plain,
( product(e_2,e_1,e_3)
| product(e_1,e_1,e_2) ),
inference(resolution,[status(thm)],[c56358,e_3_is_not_e_2]) ).
cnf(c56848,plain,
( product(e_1,e_1,e_2)
| product(e_2,e_3,e_2)
| equalish(e_1,e_3) ),
inference(resolution,[status(thm)],[c56821,c48020]) ).
cnf(c58702,plain,
( product(e_1,e_1,e_2)
| product(e_2,e_3,e_2) ),
inference(resolution,[status(thm)],[c56848,e_1_is_not_e_3]) ).
cnf(c59018,plain,
( product(e_1,e_1,e_2)
| ~ product(e_2,X524,e_2)
| equalish(X524,e_3) ),
inference(resolution,[status(thm)],[c58702,product_right_cancellation]) ).
cnf(c59007,plain,
( product(e_1,e_1,e_2)
| ~ product(e_2,X574,e_3)
| product(e_2,X574,e_2) ),
inference(resolution,[status(thm)],[c58702,qg3]) ).
cnf(c65889,plain,
( product(e_1,e_1,e_2)
| product(e_2,e_1,e_2) ),
inference(resolution,[status(thm)],[c59007,c56821]) ).
cnf(c65959,plain,
( product(e_1,e_1,e_2)
| equalish(e_1,e_3) ),
inference(resolution,[status(thm)],[c65889,c59018]) ).
cnf(c66209,plain,
product(e_1,e_1,e_2),
inference(resolution,[status(thm)],[c65959,e_1_is_not_e_3]) ).
cnf(c66218,plain,
( product(e_3,e_1,e_3)
| equalish(e_2,e_1) ),
inference(resolution,[status(thm)],[c66209,c62913]) ).
cnf(c66447,plain,
product(e_3,e_1,e_3),
inference(resolution,[status(thm)],[c66218,e_2_is_not_e_1]) ).
cnf(c66458,plain,
( ~ product(e_3,e_1,X579)
| equalish(X579,e_3) ),
inference(resolution,[status(thm)],[c66447,product_total_function2]) ).
cnf(c128,plain,
( product(e_2,e_1,e_1)
| product(e_2,e_1,e_2)
| ~ product(X136,e_1,e_3)
| equalish(X136,e_2) ),
inference(resolution,[status(thm)],[c12,product_left_cancellation]) ).
cnf(c11991,plain,
( product(e_1,e_1,e_1)
| product(e_2,e_1,e_2)
| equalish(e_3,e_2)
| product(e_2,e_1,e_1) ),
inference(resolution,[status(thm)],[c4058,c128]) ).
cnf(c36171,plain,
( product(e_1,e_1,e_1)
| product(e_2,e_1,e_2)
| product(e_2,e_1,e_1) ),
inference(resolution,[status(thm)],[c11991,e_3_is_not_e_2]) ).
cnf(c36259,plain,
( product(e_1,e_1,e_1)
| product(e_2,e_1,e_1)
| ~ product(X435,e_1,e_2)
| equalish(X435,e_2) ),
inference(resolution,[status(thm)],[c36171,product_left_cancellation]) ).
cnf(c57846,plain,
( product(e_1,e_1,e_1)
| product(e_2,e_1,e_1)
| equalish(e_1,e_2) ),
inference(resolution,[status(thm)],[c57764,c36259]) ).
cnf(c62127,plain,
( product(e_1,e_1,e_1)
| product(e_2,e_1,e_1) ),
inference(resolution,[status(thm)],[c57846,e_1_is_not_e_2]) ).
cnf(c62141,plain,
( product(e_2,e_1,e_1)
| ~ product(e_1,e_1,X541)
| equalish(X541,e_1) ),
inference(resolution,[status(thm)],[c62127,product_total_function2]) ).
cnf(c66237,plain,
( product(e_2,e_1,e_1)
| equalish(e_2,e_1) ),
inference(resolution,[status(thm)],[c66209,c62141]) ).
cnf(c66634,plain,
product(e_2,e_1,e_1),
inference(resolution,[status(thm)],[c66237,e_2_is_not_e_1]) ).
cnf(c66660,plain,
( ~ product(e_2,X584,e_1)
| equalish(X584,e_1) ),
inference(resolution,[status(thm)],[c66634,product_right_cancellation]) ).
cnf(c3,plain,
( ~ group_element(X33)
| product(X33,e_2,e_1)
| product(X33,e_2,e_2)
| product(X33,e_2,e_3) ),
inference(resolution,[status(thm)],[product_total_function1,element_2]) ).
cnf(c14,plain,
( product(e_1,e_2,e_1)
| product(e_1,e_2,e_2)
| product(e_1,e_2,e_3) ),
inference(resolution,[status(thm)],[c3,element_1]) ).
cnf(c184,plain,
( product(e_1,e_2,e_1)
| product(e_1,e_2,e_3)
| product(e_2,e_2,e_1) ),
inference(resolution,[status(thm)],[c14,c7]) ).
cnf(c66239,plain,
( ~ product(e_1,X585,e_1)
| product(e_2,X585,e_1) ),
inference(resolution,[status(thm)],[c66209,qg3]) ).
cnf(c66806,plain,
( product(e_2,e_2,e_1)
| product(e_1,e_2,e_3) ),
inference(resolution,[status(thm)],[c66239,c184]) ).
cnf(c66972,plain,
( product(e_1,e_2,e_3)
| equalish(e_2,e_1) ),
inference(resolution,[status(thm)],[c66806,c66660]) ).
cnf(c67067,plain,
product(e_1,e_2,e_3),
inference(resolution,[status(thm)],[c66972,e_2_is_not_e_1]) ).
cnf(c67089,plain,
( ~ product(e_1,X594,e_2)
| product(e_3,X594,e_1) ),
inference(resolution,[status(thm)],[c67067,qg3]) ).
cnf(c67232,plain,
product(e_3,e_1,e_1),
inference(resolution,[status(thm)],[c67089,c66209]) ).
cnf(c67242,plain,
equalish(e_1,e_3),
inference(resolution,[status(thm)],[c67232,c66458]) ).
cnf(c67261,plain,
$false,
inference(resolution,[status(thm)],[c67242,e_1_is_not_e_3]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.14/0.14 % Problem : GRP130-1.003 : TPTP v8.1.2. Released v1.2.0.
% 0.14/0.15 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.36 % Computer : n004.cluster.edu
% 0.14/0.36 % Model : x86_64 x86_64
% 0.14/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.36 % Memory : 8042.1875MB
% 0.14/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.36 % CPULimit : 300
% 0.14/0.36 % WCLimit : 300
% 0.14/0.36 % DateTime : Thu May 9 04:14:08 EDT 2024
% 0.14/0.36 % CPUTime :
% 58.15/58.33 % Version: 1.5
% 58.15/58.33 % SZS status Unsatisfiable
% 58.15/58.33 % SZS output start CNFRefutation
% See solution above
% 58.15/58.33
% 58.15/58.33 % Initial clauses : 14
% 58.15/58.33 % Processed clauses : 844
% 58.15/58.33 % Factors computed : 5
% 58.15/58.33 % Resolvents computed: 67257
% 58.15/58.33 % Tautologies deleted: 18
% 58.15/58.33 % Forward subsumed : 2075
% 58.15/58.33 % Backward subsumed : 510
% 58.15/58.33 % -------- CPU Time ---------
% 58.15/58.33 % User time : 57.771 s
% 58.15/58.33 % System time : 0.201 s
% 58.15/58.33 % Total time : 57.972 s
%------------------------------------------------------------------------------