%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GRP134-2.003 : TPTP v8.1.2. Released v1.2.0.
% 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:15 EDT 2024
% Result : Unsatisfiable 4.91s 5.17s
% Output : Refutation 4.91s
% Verified :
% SZS Type : Refutation
% Derivation depth : 31
% Number of leaves : 15
% Syntax : Number of clauses : 83 ( 14 unt; 60 nHn; 83 RR)
% Number of literals : 211 ( 0 equ; 44 neg)
% Maximal clause size : 5 ( 2 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 6 ( 5 usr; 1 prp; 0-3 aty)
% Number of functors : 3 ( 3 usr; 3 con; 0-0 aty)
% Number of variables : 45 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
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(product_left_cancellation,axiom,
( ~ product(X23,X24,X21)
| ~ product(X22,X24,X21)
| equalish(X23,X22) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',product_left_cancellation) ).
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(product_total_function2,axiom,
( ~ product(X7,X8,X6)
| ~ product(X7,X8,X5)
| equalish(X6,X5) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',product_total_function2) ).
cnf(qg4,negated_conjecture,
( ~ product(X29,X31,X28)
| ~ product(X31,X29,X30)
| product(X28,X30,X31) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',qg4) ).
cnf(c7,plain,
( ~ product(X33,X33,X34)
| product(X34,X34,X33) ),
inference(factor,[status(thm)],[qg4]) ).
cnf(e_1_then_e_2,axiom,
next(e_1,e_2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_1_then_e_2) ).
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(no_redundancy,axiom,
( ~ product(X3,e_1,X4)
| ~ next(X3,X2)
| ~ greater(X4,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',no_redundancy) ).
cnf(element_3,axiom,
group_element(e_3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',element_3) ).
cnf(product_total_function1,axiom,
( ~ group_element(X12)
| ~ group_element(X13)
| product(X12,X13,e_1)
| product(X12,X13,e_2)
| product(X12,X13,e_3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',product_total_function1) ).
cnf(c1,plain,
( ~ group_element(X32)
| product(X32,X32,e_1)
| product(X32,X32,e_2)
| product(X32,X32,e_3) ),
inference(factor,[status(thm)],[product_total_function1]) ).
cnf(c10,plain,
( product(e_3,e_3,e_1)
| product(e_3,e_3,e_2)
| product(e_3,e_3,e_3) ),
inference(resolution,[status(thm)],[c1,element_3]) ).
cnf(c100,plain,
( product(e_3,e_3,e_2)
| product(e_3,e_3,e_3)
| product(e_1,e_1,e_3) ),
inference(resolution,[status(thm)],[c10,c7]) ).
cnf(c782,plain,
( product(e_3,e_3,e_2)
| product(e_3,e_3,e_3)
| ~ next(e_1,X189)
| ~ greater(e_3,X189) ),
inference(resolution,[status(thm)],[c100,no_redundancy]) ).
cnf(c1077,plain,
( product(e_3,e_3,e_2)
| product(e_3,e_3,e_3)
| ~ next(e_1,e_2) ),
inference(resolution,[status(thm)],[c782,e_3_greater_e_2]) ).
cnf(c1079,plain,
( product(e_3,e_3,e_2)
| product(e_3,e_3,e_3) ),
inference(resolution,[status(thm)],[c1077,e_1_then_e_2]) ).
cnf(c1087,plain,
( product(e_3,e_3,e_3)
| product(e_2,e_2,e_3) ),
inference(resolution,[status(thm)],[c1079,c7]) ).
cnf(c1140,plain,
( product(e_3,e_3,e_3)
| ~ product(e_2,e_2,X208)
| equalish(X208,e_3) ),
inference(resolution,[status(thm)],[c1087,product_total_function2]) ).
cnf(c1143,plain,
( product(e_3,e_3,e_3)
| ~ product(X209,e_2,e_3)
| equalish(X209,e_2) ),
inference(resolution,[status(thm)],[c1087,product_left_cancellation]) ).
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(element_1,axiom,
group_element(e_1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',element_1) ).
cnf(element_2,axiom,
group_element(e_2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',element_2) ).
cnf(c3,plain,
( ~ group_element(X36)
| product(X36,e_2,e_1)
| product(X36,e_2,e_2)
| product(X36,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(c198,plain,
( product(e_1,e_2,e_2)
| product(e_1,e_2,e_3)
| ~ product(X204,e_2,e_1)
| equalish(X204,e_1) ),
inference(resolution,[status(thm)],[c14,product_left_cancellation]) ).
cnf(product_right_cancellation,axiom,
( ~ product(X16,X15,X17)
| ~ product(X16,X14,X17)
| equalish(X15,X14) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',product_right_cancellation) ).
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(c44,plain,
( product(e_1,e_1,e_1)
| product(e_1,e_1,e_2)
| ~ next(e_1,X65)
| ~ greater(e_3,X65) ),
inference(resolution,[status(thm)],[c8,no_redundancy]) ).
cnf(c485,plain,
( product(e_1,e_1,e_1)
| product(e_1,e_1,e_2)
| ~ next(e_1,e_2) ),
inference(resolution,[status(thm)],[c44,e_3_greater_e_2]) ).
cnf(c560,plain,
( product(e_1,e_1,e_1)
| product(e_1,e_1,e_2) ),
inference(resolution,[status(thm)],[c485,e_1_then_e_2]) ).
cnf(c563,plain,
( product(e_1,e_1,e_2)
| ~ product(e_1,X80,e_1)
| equalish(X80,e_1) ),
inference(resolution,[status(thm)],[c560,product_right_cancellation]) ).
cnf(c673,plain,
( product(e_1,e_1,e_2)
| equalish(e_2,e_1)
| product(e_1,e_2,e_2)
| product(e_1,e_2,e_3) ),
inference(resolution,[status(thm)],[c563,c14]) ).
cnf(c2594,plain,
( product(e_1,e_1,e_2)
| product(e_1,e_2,e_2)
| product(e_1,e_2,e_3) ),
inference(resolution,[status(thm)],[c673,e_2_is_not_e_1]) ).
cnf(c2663,plain,
( product(e_1,e_2,e_2)
| product(e_1,e_2,e_3)
| product(e_2,e_2,e_1) ),
inference(resolution,[status(thm)],[c2594,c7]) ).
cnf(c2769,plain,
( product(e_1,e_2,e_2)
| product(e_1,e_2,e_3)
| equalish(e_2,e_1) ),
inference(resolution,[status(thm)],[c2663,c198]) ).
cnf(c2838,plain,
( product(e_1,e_2,e_2)
| product(e_1,e_2,e_3) ),
inference(resolution,[status(thm)],[c2769,e_2_is_not_e_1]) ).
cnf(c2874,plain,
( product(e_1,e_2,e_2)
| product(e_3,e_3,e_3)
| equalish(e_1,e_2) ),
inference(resolution,[status(thm)],[c2838,c1143]) ).
cnf(c3271,plain,
( product(e_1,e_2,e_2)
| product(e_3,e_3,e_3) ),
inference(resolution,[status(thm)],[c2874,e_1_is_not_e_2]) ).
cnf(c3279,plain,
( product(e_3,e_3,e_3)
| ~ product(e_2,e_1,X395)
| product(X395,e_2,e_1) ),
inference(resolution,[status(thm)],[c3271,qg4]) ).
cnf(c1132,plain,
( product(e_3,e_3,e_3)
| ~ product(e_2,X206,e_3)
| equalish(X206,e_2) ),
inference(resolution,[status(thm)],[c1087,product_right_cancellation]) ).
cnf(c2,plain,
( ~ group_element(X35)
| product(X35,e_1,e_1)
| product(X35,e_1,e_2)
| product(X35,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(c126,plain,
( product(e_2,e_1,e_2)
| product(e_2,e_1,e_3)
| ~ product(e_1,e_2,X129)
| product(X129,e_1,e_2) ),
inference(resolution,[status(thm)],[c12,qg4]) ).
cnf(c3282,plain,
( product(e_3,e_3,e_3)
| product(e_2,e_1,e_2)
| product(e_2,e_1,e_3) ),
inference(resolution,[status(thm)],[c3271,c126]) ).
cnf(c4041,plain,
( product(e_3,e_3,e_3)
| product(e_2,e_1,e_2)
| equalish(e_1,e_2) ),
inference(resolution,[status(thm)],[c3282,c1132]) ).
cnf(c4117,plain,
( product(e_3,e_3,e_3)
| product(e_2,e_1,e_2) ),
inference(resolution,[status(thm)],[c4041,e_1_is_not_e_2]) ).
cnf(c4161,plain,
( product(e_3,e_3,e_3)
| product(e_2,e_2,e_1) ),
inference(resolution,[status(thm)],[c4117,c3279]) ).
cnf(c4454,plain,
( product(e_3,e_3,e_3)
| equalish(e_1,e_3) ),
inference(resolution,[status(thm)],[c4161,c1140]) ).
cnf(c4642,plain,
product(e_3,e_3,e_3),
inference(resolution,[status(thm)],[c4454,e_1_is_not_e_3]) ).
cnf(c4669,plain,
( ~ product(e_3,e_3,X400)
| equalish(X400,e_3) ),
inference(resolution,[status(thm)],[c4642,product_total_function2]) ).
cnf(c577,plain,
( product(e_1,e_1,e_1)
| ~ product(e_1,X84,e_2)
| equalish(X84,e_1) ),
inference(resolution,[status(thm)],[c560,product_right_cancellation]) ).
cnf(c2807,plain,
( product(e_1,e_2,e_3)
| equalish(e_2,e_1)
| product(e_1,e_1,e_1) ),
inference(resolution,[status(thm)],[c2769,c577]) ).
cnf(c2941,plain,
( product(e_1,e_2,e_3)
| product(e_1,e_1,e_1) ),
inference(resolution,[status(thm)],[c2807,e_2_is_not_e_1]) ).
cnf(c3014,plain,
( product(e_1,e_2,e_3)
| ~ product(e_1,e_1,X384)
| equalish(X384,e_1) ),
inference(resolution,[status(thm)],[c2941,product_total_function2]) ).
cnf(c2842,plain,
( product(e_1,e_2,e_3)
| ~ product(X372,e_2,e_2)
| equalish(X372,e_1) ),
inference(resolution,[status(thm)],[c2838,product_left_cancellation]) ).
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(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(c65,plain,
( product(e_2,e_2,e_1)
| product(e_2,e_2,e_2)
| product(e_3,e_3,e_2) ),
inference(resolution,[status(thm)],[c9,c7]) ).
cnf(c660,plain,
( product(e_2,e_2,e_1)
| product(e_2,e_2,e_2)
| ~ product(e_3,e_3,X320)
| equalish(X320,e_2) ),
inference(resolution,[status(thm)],[c65,product_total_function2]) ).
cnf(c4429,plain,
( product(e_2,e_2,e_1)
| product(e_2,e_2,e_2)
| equalish(e_3,e_2) ),
inference(resolution,[status(thm)],[c4161,c660]) ).
cnf(c4954,plain,
( product(e_2,e_2,e_1)
| product(e_2,e_2,e_2) ),
inference(resolution,[status(thm)],[c4429,e_3_is_not_e_2]) ).
cnf(c5001,plain,
( product(e_2,e_2,e_1)
| product(e_1,e_2,e_3)
| equalish(e_2,e_1) ),
inference(resolution,[status(thm)],[c4954,c2842]) ).
cnf(c6537,plain,
( product(e_2,e_2,e_1)
| product(e_1,e_2,e_3) ),
inference(resolution,[status(thm)],[c5001,e_2_is_not_e_1]) ).
cnf(c6557,plain,
( product(e_1,e_2,e_3)
| product(e_1,e_1,e_2) ),
inference(resolution,[status(thm)],[c6537,c7]) ).
cnf(c6601,plain,
( product(e_1,e_2,e_3)
| equalish(e_2,e_1) ),
inference(resolution,[status(thm)],[c6557,c3014]) ).
cnf(c6639,plain,
product(e_1,e_2,e_3),
inference(resolution,[status(thm)],[c6601,e_2_is_not_e_1]) ).
cnf(c6647,plain,
( ~ product(e_2,e_1,X468)
| product(X468,e_3,e_1) ),
inference(resolution,[status(thm)],[c6639,qg4]) ).
cnf(c128,plain,
( product(e_2,e_1,e_2)
| product(e_2,e_1,e_3)
| ~ product(e_2,X131,e_1)
| equalish(X131,e_1) ),
inference(resolution,[status(thm)],[c12,product_right_cancellation]) ).
cnf(c584,plain,
( product(e_1,e_1,e_1)
| product(e_2,e_2,e_1) ),
inference(resolution,[status(thm)],[c560,c7]) ).
cnf(c611,plain,
( product(e_2,e_2,e_1)
| ~ product(X91,e_1,e_1)
| equalish(X91,e_1) ),
inference(resolution,[status(thm)],[c584,product_left_cancellation]) ).
cnf(c717,plain,
( product(e_2,e_2,e_1)
| equalish(e_2,e_1)
| product(e_2,e_1,e_2)
| product(e_2,e_1,e_3) ),
inference(resolution,[status(thm)],[c611,c12]) ).
cnf(c5731,plain,
( equalish(e_2,e_1)
| product(e_2,e_1,e_2)
| product(e_2,e_1,e_3) ),
inference(resolution,[status(thm)],[c717,c128]) ).
cnf(c7275,plain,
( product(e_2,e_1,e_2)
| product(e_2,e_1,e_3) ),
inference(resolution,[status(thm)],[c5731,e_2_is_not_e_1]) ).
cnf(c7344,plain,
( product(e_2,e_1,e_2)
| product(e_3,e_3,e_1) ),
inference(resolution,[status(thm)],[c7275,c6647]) ).
cnf(c7413,plain,
( product(e_2,e_1,e_2)
| equalish(e_1,e_3) ),
inference(resolution,[status(thm)],[c7344,c4669]) ).
cnf(c7436,plain,
product(e_2,e_1,e_2),
inference(resolution,[status(thm)],[c7413,e_1_is_not_e_3]) ).
cnf(c7439,plain,
( ~ product(X522,e_1,e_2)
| equalish(X522,e_2) ),
inference(resolution,[status(thm)],[c7436,product_left_cancellation]) ).
cnf(c4984,plain,
( product(e_2,e_2,e_2)
| product(e_1,e_1,e_2) ),
inference(resolution,[status(thm)],[c4954,c7]) ).
cnf(c5032,plain,
( product(e_1,e_1,e_2)
| ~ product(e_2,X429,e_2)
| equalish(X429,e_2) ),
inference(resolution,[status(thm)],[c4984,product_right_cancellation]) ).
cnf(c7440,plain,
( product(e_1,e_1,e_2)
| equalish(e_1,e_2) ),
inference(resolution,[status(thm)],[c7436,c5032]) ).
cnf(c7577,plain,
equalish(e_1,e_2),
inference(resolution,[status(thm)],[c7440,c7439]) ).
cnf(c7598,plain,
$false,
inference(resolution,[status(thm)],[c7577,e_1_is_not_e_2]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.12 % Problem : GRP134-2.003 : TPTP v8.1.2. Released v1.2.0.
% 0.10/0.12 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.12/0.34 % Computer : n023.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:32:53 EDT 2024
% 0.12/0.34 % CPUTime :
% 4.91/5.17 % Version: 1.5
% 4.91/5.17 % SZS status Unsatisfiable
% 4.91/5.17 % SZS output start CNFRefutation
% See solution above
% 4.91/5.17
% 4.91/5.17 % Initial clauses : 20
% 4.91/5.17 % Processed clauses : 471
% 4.91/5.17 % Factors computed : 5
% 4.91/5.17 % Resolvents computed: 7594
% 4.91/5.17 % Tautologies deleted: 0
% 4.91/5.17 % Forward subsumed : 1570
% 4.91/5.17 % Backward subsumed : 312
% 4.91/5.17 % -------- CPU Time ---------
% 4.91/5.17 % User time : 4.787 s
% 4.91/5.17 % System time : 0.023 s
% 4.91/5.17 % Total time : 4.810 s
%------------------------------------------------------------------------------