%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GRP129-4.004 : TPTP v8.1.2. Bugfixed v1.2.1.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n010.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 3.16s 3.34s
% Output : Refutation 3.16s
% Verified :
% SZS Type : Refutation
% Derivation depth : 25
% Number of leaves : 19
% Syntax : Number of clauses : 83 ( 24 unt; 50 nHn; 83 RR)
% Number of literals : 200 ( 0 equ; 36 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 : 33 ( 1 sgn)
% Comments :
%------------------------------------------------------------------------------
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(X14,X13,X12)
| ~ product(X14,X13,X15)
| equalish(X12,X15) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',product_total_function2) ).
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(product_right_cancellation,axiom,
( ~ product(X21,X19,X20)
| ~ product(X21,X22,X20)
| equalish(X19,X22) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',product_right_cancellation) ).
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(qg3_1,negated_conjecture,
( product(X7,X8,X6)
| ~ product(X6,X7,X9)
| ~ product(X8,X6,X9) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',qg3_1) ).
cnf(c10,plain,
( product(X10,X10,X10)
| ~ product(X10,X10,X11) ),
inference(factor,[status(thm)],[qg3_1]) ).
cnf(element_2,axiom,
group_element(e_2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',element_2) ).
cnf(product_total_function1,axiom,
( ~ group_element(X43)
| ~ group_element(X42)
| product(X43,X42,e_1)
| product(X43,X42,e_2)
| product(X43,X42,e_3)
| product(X43,X42,e_4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',product_total_function1) ).
cnf(c16,plain,
( ~ group_element(X47)
| product(X47,X47,e_1)
| product(X47,X47,e_2)
| product(X47,X47,e_3)
| product(X47,X47,e_4) ),
inference(factor,[status(thm)],[product_total_function1]) ).
cnf(c30,plain,
( product(e_2,e_2,e_1)
| product(e_2,e_2,e_2)
| product(e_2,e_2,e_3)
| product(e_2,e_2,e_4) ),
inference(resolution,[status(thm)],[c16,element_2]) ).
cnf(c539,plain,
( product(e_2,e_2,e_2)
| product(e_2,e_2,e_3)
| product(e_2,e_2,e_4) ),
inference(resolution,[status(thm)],[c30,c10]) ).
cnf(c866,plain,
( product(e_2,e_2,e_2)
| product(e_2,e_2,e_4) ),
inference(resolution,[status(thm)],[c539,c10]) ).
cnf(c896,plain,
product(e_2,e_2,e_2),
inference(resolution,[status(thm)],[c866,c10]) ).
cnf(c899,plain,
( ~ product(e_2,e_2,X94)
| equalish(X94,e_2) ),
inference(resolution,[status(thm)],[c896,product_total_function2]) ).
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(c29,plain,
( product(e_1,e_1,e_1)
| product(e_1,e_1,e_2)
| product(e_1,e_1,e_3)
| product(e_1,e_1,e_4) ),
inference(resolution,[status(thm)],[c16,element_1]) ).
cnf(c449,plain,
( product(e_1,e_1,e_1)
| product(e_1,e_1,e_3)
| product(e_1,e_1,e_4) ),
inference(resolution,[status(thm)],[c29,c10]) ).
cnf(c489,plain,
( product(e_1,e_1,e_1)
| product(e_1,e_1,e_4) ),
inference(resolution,[status(thm)],[c449,c10]) ).
cnf(c519,plain,
product(e_1,e_1,e_1),
inference(resolution,[status(thm)],[c489,c10]) ).
cnf(c527,plain,
( ~ product(e_1,X78,e_1)
| equalish(X78,e_1) ),
inference(resolution,[status(thm)],[c519,product_right_cancellation]) ).
cnf(row_surjectivity,axiom,
( ~ group_element(X3)
| ~ group_element(X2)
| product(e_1,X3,X2)
| product(e_2,X3,X2)
| product(e_3,X3,X2)
| product(e_4,X3,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',row_surjectivity) ).
cnf(c1,plain,
( ~ group_element(X48)
| product(e_1,X48,e_1)
| product(e_2,X48,e_1)
| product(e_3,X48,e_1)
| product(e_4,X48,e_1) ),
inference(resolution,[status(thm)],[row_surjectivity,element_1]) ).
cnf(c34,plain,
( product(e_1,e_2,e_1)
| product(e_2,e_2,e_1)
| product(e_3,e_2,e_1)
| product(e_4,e_2,e_1) ),
inference(resolution,[status(thm)],[c1,element_2]) ).
cnf(c657,plain,
( product(e_2,e_2,e_1)
| product(e_3,e_2,e_1)
| product(e_4,e_2,e_1)
| equalish(e_2,e_1) ),
inference(resolution,[status(thm)],[c34,c527]) ).
cnf(c2320,plain,
( product(e_2,e_2,e_1)
| product(e_3,e_2,e_1)
| product(e_4,e_2,e_1) ),
inference(resolution,[status(thm)],[c657,e_2_is_not_e_1]) ).
cnf(c2328,plain,
( product(e_3,e_2,e_1)
| product(e_4,e_2,e_1)
| equalish(e_1,e_2) ),
inference(resolution,[status(thm)],[c2320,c899]) ).
cnf(c2368,plain,
( product(e_3,e_2,e_1)
| product(e_4,e_2,e_1) ),
inference(resolution,[status(thm)],[c2328,e_1_is_not_e_2]) ).
cnf(e_2_is_not_e_3,axiom,
~ equalish(e_2,e_3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_2_is_not_e_3) ).
cnf(element_3,axiom,
group_element(e_3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',element_3) ).
cnf(c31,plain,
( product(e_3,e_3,e_1)
| product(e_3,e_3,e_2)
| product(e_3,e_3,e_3)
| product(e_3,e_3,e_4) ),
inference(resolution,[status(thm)],[c16,element_3]) ).
cnf(c581,plain,
( product(e_3,e_3,e_2)
| product(e_3,e_3,e_3)
| product(e_3,e_3,e_4) ),
inference(resolution,[status(thm)],[c31,c10]) ).
cnf(c1191,plain,
( product(e_3,e_3,e_3)
| product(e_3,e_3,e_4) ),
inference(resolution,[status(thm)],[c581,c10]) ).
cnf(c1231,plain,
product(e_3,e_3,e_3),
inference(resolution,[status(thm)],[c1191,c10]) ).
cnf(c1234,plain,
( ~ product(e_3,e_3,X112)
| equalish(X112,e_3) ),
inference(resolution,[status(thm)],[c1231,product_total_function2]) ).
cnf(c2372,plain,
( product(e_4,e_2,e_1)
| product(X236,e_3,e_2)
| ~ product(e_2,X236,e_1) ),
inference(resolution,[status(thm)],[c2368,qg3_1]) ).
cnf(e_3_is_not_e_1,axiom,
~ equalish(e_3,e_1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_3_is_not_e_1) ).
cnf(c35,plain,
( product(e_1,e_3,e_1)
| product(e_2,e_3,e_1)
| product(e_3,e_3,e_1)
| product(e_4,e_3,e_1) ),
inference(resolution,[status(thm)],[c1,element_3]) ).
cnf(c696,plain,
( product(e_2,e_3,e_1)
| product(e_3,e_3,e_1)
| product(e_4,e_3,e_1)
| equalish(e_3,e_1) ),
inference(resolution,[status(thm)],[c35,c527]) ).
cnf(c2534,plain,
( product(e_2,e_3,e_1)
| product(e_3,e_3,e_1)
| product(e_4,e_3,e_1) ),
inference(resolution,[status(thm)],[c696,e_3_is_not_e_1]) ).
cnf(c2557,plain,
( product(e_2,e_3,e_1)
| product(e_4,e_3,e_1)
| equalish(e_1,e_3) ),
inference(resolution,[status(thm)],[c2534,c1234]) ).
cnf(c2589,plain,
( product(e_2,e_3,e_1)
| product(e_4,e_3,e_1) ),
inference(resolution,[status(thm)],[c2557,e_1_is_not_e_3]) ).
cnf(c2590,plain,
( product(e_4,e_3,e_1)
| product(e_4,e_2,e_1)
| product(e_3,e_3,e_2) ),
inference(resolution,[status(thm)],[c2589,c2372]) ).
cnf(c3258,plain,
( product(e_4,e_3,e_1)
| product(e_4,e_2,e_1)
| equalish(e_2,e_3) ),
inference(resolution,[status(thm)],[c2590,c1234]) ).
cnf(c3295,plain,
( product(e_4,e_3,e_1)
| product(e_4,e_2,e_1) ),
inference(resolution,[status(thm)],[c3258,e_2_is_not_e_3]) ).
cnf(c3308,plain,
( product(e_4,e_2,e_1)
| product(X370,e_4,e_3)
| ~ product(e_3,X370,e_1) ),
inference(resolution,[status(thm)],[c3295,qg3_1]) ).
cnf(c3415,plain,
( product(e_4,e_2,e_1)
| product(e_2,e_4,e_3) ),
inference(resolution,[status(thm)],[c3308,c2368]) ).
cnf(c3423,plain,
( product(e_2,e_4,e_3)
| ~ product(e_4,X373,e_1)
| equalish(X373,e_2) ),
inference(resolution,[status(thm)],[c3415,product_right_cancellation]) ).
cnf(c3325,plain,
( product(e_4,e_3,e_1)
| product(X385,e_4,e_2)
| ~ product(e_2,X385,e_1) ),
inference(resolution,[status(thm)],[c3295,qg3_1]) ).
cnf(c3540,plain,
( product(e_4,e_3,e_1)
| product(e_3,e_4,e_2) ),
inference(resolution,[status(thm)],[c3325,c2589]) ).
cnf(c3576,plain,
( product(e_4,e_3,e_1)
| ~ product(e_3,e_4,X394)
| equalish(X394,e_2) ),
inference(resolution,[status(thm)],[c3540,product_total_function2]) ).
cnf(e_4_is_not_e_3,axiom,
~ equalish(e_4,e_3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_4_is_not_e_3) ).
cnf(c2599,plain,
( product(e_4,e_3,e_1)
| ~ product(e_2,X278,e_1)
| equalish(X278,e_3) ),
inference(resolution,[status(thm)],[c2589,product_right_cancellation]) ).
cnf(e_1_is_not_e_4,axiom,
~ equalish(e_1,e_4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_1_is_not_e_4) ).
cnf(element_4,axiom,
group_element(e_4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',element_4) ).
cnf(c32,plain,
( product(e_4,e_4,e_1)
| product(e_4,e_4,e_2)
| product(e_4,e_4,e_3)
| product(e_4,e_4,e_4) ),
inference(resolution,[status(thm)],[c16,element_4]) ).
cnf(c622,plain,
( product(e_4,e_4,e_2)
| product(e_4,e_4,e_3)
| product(e_4,e_4,e_4) ),
inference(resolution,[status(thm)],[c32,c10]) ).
cnf(c1581,plain,
( product(e_4,e_4,e_3)
| product(e_4,e_4,e_4) ),
inference(resolution,[status(thm)],[c622,c10]) ).
cnf(c1611,plain,
product(e_4,e_4,e_4),
inference(resolution,[status(thm)],[c1581,c10]) ).
cnf(c1629,plain,
( ~ product(e_4,e_4,X130)
| equalish(X130,e_4) ),
inference(resolution,[status(thm)],[c1611,product_total_function2]) ).
cnf(e_4_is_not_e_1,axiom,
~ equalish(e_4,e_1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_4_is_not_e_1) ).
cnf(c36,plain,
( product(e_1,e_4,e_1)
| product(e_2,e_4,e_1)
| product(e_3,e_4,e_1)
| product(e_4,e_4,e_1) ),
inference(resolution,[status(thm)],[c1,element_4]) ).
cnf(c735,plain,
( product(e_2,e_4,e_1)
| product(e_3,e_4,e_1)
| product(e_4,e_4,e_1)
| equalish(e_4,e_1) ),
inference(resolution,[status(thm)],[c36,c527]) ).
cnf(c4019,plain,
( product(e_2,e_4,e_1)
| product(e_3,e_4,e_1)
| product(e_4,e_4,e_1) ),
inference(resolution,[status(thm)],[c735,e_4_is_not_e_1]) ).
cnf(c4068,plain,
( product(e_2,e_4,e_1)
| product(e_3,e_4,e_1)
| equalish(e_1,e_4) ),
inference(resolution,[status(thm)],[c4019,c1629]) ).
cnf(c4121,plain,
( product(e_2,e_4,e_1)
| product(e_3,e_4,e_1) ),
inference(resolution,[status(thm)],[c4068,e_1_is_not_e_4]) ).
cnf(c4123,plain,
( product(e_3,e_4,e_1)
| product(e_4,e_3,e_1)
| equalish(e_4,e_3) ),
inference(resolution,[status(thm)],[c4121,c2599]) ).
cnf(c4275,plain,
( product(e_3,e_4,e_1)
| product(e_4,e_3,e_1) ),
inference(resolution,[status(thm)],[c4123,e_4_is_not_e_3]) ).
cnf(c4284,plain,
( product(e_4,e_3,e_1)
| equalish(e_1,e_2) ),
inference(resolution,[status(thm)],[c4275,c3576]) ).
cnf(c4349,plain,
product(e_4,e_3,e_1),
inference(resolution,[status(thm)],[c4284,e_1_is_not_e_2]) ).
cnf(c4352,plain,
( product(e_2,e_4,e_3)
| equalish(e_3,e_2) ),
inference(resolution,[status(thm)],[c4349,c3423]) ).
cnf(c4482,plain,
product(e_2,e_4,e_3),
inference(resolution,[status(thm)],[c4352,e_3_is_not_e_2]) ).
cnf(c4491,plain,
( ~ product(e_2,e_4,X561)
| equalish(X561,e_3) ),
inference(resolution,[status(thm)],[c4482,product_total_function2]) ).
cnf(e_2_is_not_e_4,axiom,
~ equalish(e_2,e_4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',e_2_is_not_e_4) ).
cnf(c4151,plain,
( product(e_2,e_4,e_1)
| ~ product(e_3,X539,e_1)
| equalish(X539,e_4) ),
inference(resolution,[status(thm)],[c4121,product_right_cancellation]) ).
cnf(c2385,plain,
( product(e_3,e_2,e_1)
| ~ product(e_4,X231,e_1)
| equalish(X231,e_2) ),
inference(resolution,[status(thm)],[c2368,product_right_cancellation]) ).
cnf(c4351,plain,
( product(e_3,e_2,e_1)
| equalish(e_3,e_2) ),
inference(resolution,[status(thm)],[c4349,c2385]) ).
cnf(c4418,plain,
product(e_3,e_2,e_1),
inference(resolution,[status(thm)],[c4351,e_3_is_not_e_2]) ).
cnf(c4440,plain,
( product(e_2,e_4,e_1)
| equalish(e_2,e_4) ),
inference(resolution,[status(thm)],[c4418,c4151]) ).
cnf(c4563,plain,
product(e_2,e_4,e_1),
inference(resolution,[status(thm)],[c4440,e_2_is_not_e_4]) ).
cnf(c4573,plain,
equalish(e_1,e_3),
inference(resolution,[status(thm)],[c4563,c4491]) ).
cnf(c4580,plain,
$false,
inference(resolution,[status(thm)],[c4573,e_1_is_not_e_3]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : GRP129-4.004 : TPTP v8.1.2. Bugfixed v1.2.1.
% 0.07/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.35 % Computer : n010.cluster.edu
% 0.14/0.35 % Model : x86_64 x86_64
% 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.35 % Memory : 8042.1875MB
% 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.35 % CPULimit : 300
% 0.14/0.35 % WCLimit : 300
% 0.14/0.35 % DateTime : Thu May 9 03:36:53 EDT 2024
% 0.14/0.35 % CPUTime :
% 3.16/3.34 % Version: 1.5
% 3.16/3.34 % SZS status Unsatisfiable
% 3.16/3.34 % SZS output start CNFRefutation
% See solution above
% 3.16/3.34
% 3.16/3.34 % Initial clauses : 25
% 3.16/3.34 % Processed clauses : 291
% 3.16/3.34 % Factors computed : 9
% 3.16/3.34 % Resolvents computed: 4572
% 3.16/3.34 % Tautologies deleted: 17
% 3.16/3.34 % Forward subsumed : 1187
% 3.16/3.34 % Backward subsumed : 158
% 3.16/3.34 % -------- CPU Time ---------
% 3.16/3.34 % User time : 2.953 s
% 3.16/3.34 % System time : 0.029 s
% 3.16/3.34 % Total time : 2.982 s
%------------------------------------------------------------------------------