%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GRP130-4.003 : TPTP v8.1.2. Bugfixed v1.2.1.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n025.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:13 EDT 2024
% Result : Unsatisfiable 0.69s 0.91s
% Output : Refutation 0.69s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 10
% Syntax : Number of clauses : 30 ( 11 unt; 12 nHn; 30 RR)
% Number of literals : 65 ( 0 equ; 18 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 : 24 ( 1 sgn)
% Comments :
%------------------------------------------------------------------------------
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_left_cancellation,axiom,
( ~ product(X22,X20,X21)
| ~ product(X23,X20,X21)
| equalish(X22,X23) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',product_left_cancellation) ).
cnf(qg3_2,negated_conjecture,
( product(X34,X36,X35)
| ~ product(X35,X33,X34)
| ~ product(X34,X33,X36) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',qg3_2) ).
cnf(c12,plain,
( product(X38,X38,X38)
| ~ product(X38,X37,X38) ),
inference(factor,[status(thm)],[qg3_2]) ).
cnf(element_2,axiom,
group_element(e_2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',element_2) ).
cnf(column_surjectivity,axiom,
( ~ group_element(X9)
| ~ group_element(X8)
| product(X9,e_1,X8)
| product(X9,e_2,X8)
| product(X9,e_3,X8) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',column_surjectivity) ).
cnf(c5,plain,
( ~ group_element(X48)
| product(X48,e_1,X48)
| product(X48,e_2,X48)
| product(X48,e_3,X48) ),
inference(factor,[status(thm)],[column_surjectivity]) ).
cnf(c21,plain,
( product(e_2,e_1,e_2)
| product(e_2,e_2,e_2)
| product(e_2,e_3,e_2) ),
inference(resolution,[status(thm)],[c5,element_2]) ).
cnf(c185,plain,
( product(e_2,e_2,e_2)
| product(e_2,e_3,e_2) ),
inference(resolution,[status(thm)],[c21,c12]) ).
cnf(c231,plain,
product(e_2,e_2,e_2),
inference(resolution,[status(thm)],[c185,c12]) ).
cnf(c250,plain,
( ~ product(X64,e_2,e_2)
| equalish(X64,e_2) ),
inference(resolution,[status(thm)],[c231,product_left_cancellation]) ).
cnf(qg3_1,negated_conjecture,
( product(X28,X27,X30)
| ~ product(X29,X27,X28)
| ~ product(X28,X30,X29) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',qg3_1) ).
cnf(c11,plain,
( product(X31,X32,X32)
| ~ product(X31,X32,X31) ),
inference(factor,[status(thm)],[qg3_1]) ).
cnf(element_3,axiom,
group_element(e_3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',element_3) ).
cnf(product_total_function1,axiom,
( ~ group_element(X46)
| ~ group_element(X45)
| product(X46,X45,e_1)
| product(X46,X45,e_2)
| product(X46,X45,e_3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',product_total_function1) ).
cnf(c15,plain,
( ~ group_element(X56)
| product(X56,e_2,e_1)
| product(X56,e_2,e_2)
| product(X56,e_2,e_3) ),
inference(resolution,[status(thm)],[product_total_function1,element_2]) ).
cnf(c46,plain,
( product(e_3,e_2,e_1)
| product(e_3,e_2,e_2)
| product(e_3,e_2,e_3) ),
inference(resolution,[status(thm)],[c15,element_3]) ).
cnf(c847,plain,
( product(e_3,e_2,e_1)
| product(e_3,e_2,e_2) ),
inference(resolution,[status(thm)],[c46,c11]) ).
cnf(c868,plain,
( product(e_3,e_2,e_1)
| equalish(e_3,e_2) ),
inference(resolution,[status(thm)],[c847,c250]) ).
cnf(c885,plain,
product(e_3,e_2,e_1),
inference(resolution,[status(thm)],[c868,e_3_is_not_e_2]) ).
cnf(c920,plain,
( product(e_3,X105,e_2)
| ~ product(e_1,X105,e_3) ),
inference(resolution,[status(thm)],[c885,qg3_1]) ).
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(element_1,axiom,
group_element(e_1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',element_1) ).
cnf(c47,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)],[c15,element_1]) ).
cnf(c889,plain,
( product(e_1,e_2,e_2)
| product(e_1,e_2,e_3) ),
inference(resolution,[status(thm)],[c47,c11]) ).
cnf(c1052,plain,
( product(e_1,e_2,e_3)
| equalish(e_1,e_2) ),
inference(resolution,[status(thm)],[c889,c250]) ).
cnf(c1082,plain,
product(e_1,e_2,e_3),
inference(resolution,[status(thm)],[c1052,e_1_is_not_e_2]) ).
cnf(c1087,plain,
product(e_3,e_2,e_2),
inference(resolution,[status(thm)],[c1082,c920]) ).
cnf(c1131,plain,
equalish(e_3,e_2),
inference(resolution,[status(thm)],[c1087,c250]) ).
cnf(c1141,plain,
$false,
inference(resolution,[status(thm)],[c1131,e_3_is_not_e_2]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : GRP130-4.003 : 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 : n025.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:36:38 EDT 2024
% 0.13/0.34 % CPUTime :
% 0.69/0.91 % Version: 1.5
% 0.69/0.91 % SZS status Unsatisfiable
% 0.69/0.91 % SZS output start CNFRefutation
% See solution above
% 0.69/0.91
% 0.69/0.91 % Initial clauses : 18
% 0.69/0.91 % Processed clauses : 96
% 0.69/0.91 % Factors computed : 9
% 0.69/0.91 % Resolvents computed: 1133
% 0.69/0.91 % Tautologies deleted: 6
% 0.69/0.91 % Forward subsumed : 141
% 0.69/0.91 % Backward subsumed : 24
% 0.69/0.91 % -------- CPU Time ---------
% 0.69/0.91 % User time : 0.550 s
% 0.69/0.91 % System time : 0.023 s
% 0.69/0.91 % Total time : 0.573 s
%------------------------------------------------------------------------------