%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GRP126-2.004 : TPTP v8.1.2. Released v1.2.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n027.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 0.59s 0.85s
% Output : Refutation 0.59s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 19
% Syntax : Number of clauses : 53 ( 19 unt; 21 nHn; 52 RR)
% Number of literals : 121 ( 0 equ; 31 neg)
% Maximal clause size : 6 ( 2 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 6 ( 5 usr; 1 prp; 0-3 aty)
% Number of functors : 4 ( 4 usr; 4 con; 0-0 aty)
% Number of variables : 34 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
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(product_right_cancellation,axiom,
( ~ product(X23,X20,X22)
| ~ product(X23,X21,X22)
| equalish(X20,X21) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',product_right_cancellation) ).
cnf(e_1_is_not_e_4,axiom,
~ equalish(e_1,e_4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_1_is_not_e_4) ).
cnf(product_idempotence,axiom,
product(X2,X2,X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',product_idempotence) ).
cnf(c11,plain,
( ~ product(X31,X32,X31)
| equalish(X32,X31) ),
inference(resolution,[status(thm)],[product_right_cancellation,product_idempotence]) ).
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_left_cancellation,axiom,
( ~ product(X24,X26,X27)
| ~ product(X25,X26,X27)
| equalish(X24,X25) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',product_left_cancellation) ).
cnf(e_2_then_e_3,axiom,
next(e_2,e_3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_2_then_e_3) ).
cnf(e_4_greater_e_3,axiom,
greater(e_4,e_3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',e_4_greater_e_3) ).
cnf(no_redundancy,axiom,
( ~ product(X5,e_1,X3)
| ~ next(X5,X4)
| ~ greater(X3,X4) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',no_redundancy) ).
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(c13,plain,
( ~ product(X37,X38,X38)
| equalish(X37,X38) ),
inference(resolution,[status(thm)],[product_left_cancellation,product_idempotence]) ).
cnf(element_2,axiom,
group_element(e_2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',element_2) ).
cnf(element_1,axiom,
group_element(e_1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',element_1) ).
cnf(product_total_function1,axiom,
( ~ group_element(X12)
| ~ group_element(X11)
| product(X12,X11,e_1)
| product(X12,X11,e_2)
| product(X12,X11,e_3)
| product(X12,X11,e_4) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',product_total_function1) ).
cnf(c4,plain,
( ~ group_element(X51)
| product(X51,e_1,e_1)
| product(X51,e_1,e_2)
| product(X51,e_1,e_3)
| product(X51,e_1,e_4) ),
inference(resolution,[status(thm)],[product_total_function1,element_1]) ).
cnf(c25,plain,
( product(e_2,e_1,e_1)
| product(e_2,e_1,e_2)
| product(e_2,e_1,e_3)
| product(e_2,e_1,e_4) ),
inference(resolution,[status(thm)],[c4,element_2]) ).
cnf(c43,plain,
( product(e_2,e_1,e_2)
| product(e_2,e_1,e_3)
| product(e_2,e_1,e_4)
| equalish(e_2,e_1) ),
inference(resolution,[status(thm)],[c25,c13]) ).
cnf(c78,plain,
( product(e_2,e_1,e_2)
| product(e_2,e_1,e_3)
| product(e_2,e_1,e_4) ),
inference(resolution,[status(thm)],[c43,e_2_is_not_e_1]) ).
cnf(c106,plain,
( product(e_2,e_1,e_3)
| product(e_2,e_1,e_4)
| equalish(e_1,e_2) ),
inference(resolution,[status(thm)],[c78,c11]) ).
cnf(c127,plain,
( product(e_2,e_1,e_3)
| product(e_2,e_1,e_4) ),
inference(resolution,[status(thm)],[c106,e_1_is_not_e_2]) ).
cnf(c137,plain,
( product(e_2,e_1,e_3)
| ~ next(e_2,X56)
| ~ greater(e_4,X56) ),
inference(resolution,[status(thm)],[c127,no_redundancy]) ).
cnf(c164,plain,
( product(e_2,e_1,e_3)
| ~ next(e_2,e_3) ),
inference(resolution,[status(thm)],[c137,e_4_greater_e_3]) ).
cnf(c165,plain,
product(e_2,e_1,e_3),
inference(resolution,[status(thm)],[c164,e_2_then_e_3]) ).
cnf(c186,plain,
( ~ product(X60,e_1,e_3)
| equalish(X60,e_2) ),
inference(resolution,[status(thm)],[c165,product_left_cancellation]) ).
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(element_4,axiom,
group_element(e_4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',element_4) ).
cnf(c27,plain,
( product(e_4,e_1,e_1)
| product(e_4,e_1,e_2)
| product(e_4,e_1,e_3)
| product(e_4,e_1,e_4) ),
inference(resolution,[status(thm)],[c4,element_4]) ).
cnf(c143,plain,
( product(e_4,e_1,e_2)
| product(e_4,e_1,e_3)
| product(e_4,e_1,e_4)
| equalish(e_4,e_1) ),
inference(resolution,[status(thm)],[c27,c13]) ).
cnf(c447,plain,
( product(e_4,e_1,e_2)
| product(e_4,e_1,e_3)
| product(e_4,e_1,e_4) ),
inference(resolution,[status(thm)],[c143,e_4_is_not_e_1]) ).
cnf(c456,plain,
( product(e_4,e_1,e_2)
| product(e_4,e_1,e_4)
| equalish(e_4,e_2) ),
inference(resolution,[status(thm)],[c447,c186]) ).
cnf(c480,plain,
( product(e_4,e_1,e_2)
| product(e_4,e_1,e_4) ),
inference(resolution,[status(thm)],[c456,e_4_is_not_e_2]) ).
cnf(c493,plain,
( product(e_4,e_1,e_2)
| equalish(e_1,e_4) ),
inference(resolution,[status(thm)],[c480,c11]) ).
cnf(c500,plain,
product(e_4,e_1,e_2),
inference(resolution,[status(thm)],[c493,e_1_is_not_e_4]) ).
cnf(c505,plain,
( ~ product(e_4,X141,e_2)
| equalish(X141,e_1) ),
inference(resolution,[status(thm)],[c500,product_right_cancellation]) ).
cnf(qg4,negated_conjecture,
( ~ product(X42,X40,X39)
| ~ product(X40,X42,X41)
| product(X39,X41,X40) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',qg4) ).
cnf(c187,plain,
( ~ product(e_1,e_2,X61)
| product(X61,e_3,e_2) ),
inference(resolution,[status(thm)],[c165,qg4]) ).
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_total_function2,axiom,
( ~ product(X10,X9,X7)
| ~ product(X10,X9,X8)
| equalish(X7,X8) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',product_total_function2) ).
cnf(c2,plain,
( ~ product(X17,X17,X18)
| equalish(X18,X17) ),
inference(resolution,[status(thm)],[product_total_function2,product_idempotence]) ).
cnf(c5,plain,
( ~ group_element(X52)
| product(X52,e_2,e_1)
| product(X52,e_2,e_2)
| product(X52,e_2,e_3)
| product(X52,e_2,e_4) ),
inference(resolution,[status(thm)],[product_total_function1,element_2]) ).
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) ),
inference(resolution,[status(thm)],[c5,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)
| equalish(e_2,e_1) ),
inference(resolution,[status(thm)],[c28,c11]) ).
cnf(c564,plain,
( product(e_1,e_2,e_2)
| product(e_1,e_2,e_3)
| product(e_1,e_2,e_4) ),
inference(resolution,[status(thm)],[c170,e_2_is_not_e_1]) ).
cnf(c567,plain,
( product(e_1,e_2,e_3)
| product(e_1,e_2,e_4)
| equalish(e_1,e_2) ),
inference(resolution,[status(thm)],[c564,c13]) ).
cnf(c591,plain,
( product(e_1,e_2,e_3)
| product(e_1,e_2,e_4) ),
inference(resolution,[status(thm)],[c567,e_1_is_not_e_2]) ).
cnf(c596,plain,
( product(e_1,e_2,e_4)
| product(e_3,e_3,e_2) ),
inference(resolution,[status(thm)],[c591,c187]) ).
cnf(c613,plain,
( product(e_1,e_2,e_4)
| equalish(e_2,e_3) ),
inference(resolution,[status(thm)],[c596,c2]) ).
cnf(c619,plain,
product(e_1,e_2,e_4),
inference(resolution,[status(thm)],[c613,e_2_is_not_e_3]) ).
cnf(c624,plain,
product(e_4,e_3,e_2),
inference(resolution,[status(thm)],[c619,c187]) ).
cnf(c629,plain,
equalish(e_3,e_1),
inference(resolution,[status(thm)],[c624,c505]) ).
cnf(c630,plain,
$false,
inference(resolution,[status(thm)],[c629,e_3_is_not_e_1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : GRP126-2.004 : TPTP v8.1.2. Released v1.2.0.
% 0.11/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.12/0.34 % Computer : n027.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Thu May 9 04:20:53 EDT 2024
% 0.12/0.34 % CPUTime :
% 0.59/0.85 % Version: 1.5
% 0.59/0.85 % SZS status Unsatisfiable
% 0.59/0.85 % SZS output start CNFRefutation
% See solution above
% 0.59/0.85
% 0.59/0.85 % Initial clauses : 32
% 0.59/0.85 % Processed clauses : 125
% 0.59/0.85 % Factors computed : 5
% 0.59/0.85 % Resolvents computed: 626
% 0.59/0.85 % Tautologies deleted: 0
% 0.59/0.85 % Forward subsumed : 181
% 0.59/0.85 % Backward subsumed : 47
% 0.59/0.85 % -------- CPU Time ---------
% 0.59/0.85 % User time : 0.500 s
% 0.59/0.85 % System time : 0.008 s
% 0.59/0.85 % Total time : 0.508 s
%------------------------------------------------------------------------------