%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GRP039-6 : TPTP v8.1.2. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n022.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:22:53 EDT 2024
% Result : Unsatisfiable 222.69s 222.95s
% Output : Refutation 222.69s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 17
% Syntax : Number of clauses : 53 ( 20 unt; 14 nHn; 42 RR)
% Number of literals : 106 ( 0 equ; 36 neg)
% Maximal clause size : 4 ( 2 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 4 ( 3 usr; 1 prp; 0-3 aty)
% Number of functors : 7 ( 7 usr; 5 con; 0-2 aty)
% Number of variables : 52 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(prove_d_is_in_subgroup,negated_conjecture,
~ subgroup_member(d),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_d_is_in_subgroup) ).
cnf(subgroup_member_substitution,axiom,
( ~ equalish(X4,X5)
| ~ subgroup_member(X4)
| subgroup_member(X5) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',subgroup_member_substitution) ).
cnf(right_identity,axiom,
product(X3,identity,X3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',right_identity) ).
cnf(well_defined,axiom,
( ~ product(X56,X55,X58)
| ~ product(X56,X55,X57)
| equalish(X58,X57) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',well_defined) ).
cnf(c72,plain,
( ~ product(X90,identity,X89)
| equalish(X89,X90) ),
inference(resolution,[status(thm)],[well_defined,right_identity]) ).
cnf(product_substitution3,axiom,
( ~ equalish(X10,X9)
| ~ product(X11,X12,X10)
| product(X11,X12,X9) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',product_substitution3) ).
cnf(c4,plain,
( ~ equalish(X14,X13)
| product(X14,identity,X13) ),
inference(resolution,[status(thm)],[product_substitution3,right_identity]) ).
cnf(right_inverse,axiom,
product(X8,inverse(X8),identity),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',right_inverse) ).
cnf(left_inverse,axiom,
product(inverse(X7),X7,identity),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',left_inverse) ).
cnf(product_right_cancellation,axiom,
( ~ product(X64,X67,X65)
| ~ product(X64,X66,X65)
| equalish(X66,X67) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',product_right_cancellation) ).
cnf(c92,plain,
( ~ product(inverse(X126),X127,identity)
| equalish(X126,X127) ),
inference(resolution,[status(thm)],[product_right_cancellation,left_inverse]) ).
cnf(c278,plain,
equalish(X129,inverse(inverse(X129))),
inference(resolution,[status(thm)],[c92,right_inverse]) ).
cnf(c279,plain,
product(X130,identity,inverse(inverse(X130))),
inference(resolution,[status(thm)],[c278,c4]) ).
cnf(c294,plain,
equalish(inverse(inverse(X131)),X131),
inference(resolution,[status(thm)],[c279,c72]) ).
cnf(c302,plain,
( ~ subgroup_member(inverse(inverse(X149)))
| subgroup_member(X149) ),
inference(resolution,[status(thm)],[c294,subgroup_member_substitution]) ).
cnf(closure_of_inverse,axiom,
( ~ subgroup_member(X6)
| subgroup_member(inverse(X6)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',closure_of_inverse) ).
cnf(b_is_in_subgroup,negated_conjecture,
subgroup_member(b),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',b_is_in_subgroup) ).
cnf(c0,plain,
subgroup_member(inverse(b)),
inference(resolution,[status(thm)],[closure_of_inverse,b_is_in_subgroup]) ).
cnf(closure_of_product,axiom,
( ~ subgroup_member(X28)
| ~ subgroup_member(X30)
| ~ product(X28,X30,X29)
| subgroup_member(X29) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',closure_of_product) ).
cnf(b_times_a_inverse_is_c,negated_conjecture,
product(b,inverse(a),c),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',b_times_a_inverse_is_c) ).
cnf(left_identity,axiom,
product(identity,X2,X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',left_identity) ).
cnf(associativity1,axiom,
( ~ product(X36,X38,X35)
| ~ product(X38,X39,X37)
| ~ product(X35,X39,X34)
| product(X36,X37,X34) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',associativity1) ).
cnf(c43,plain,
( ~ product(X150,X151,identity)
| ~ product(X151,X152,X153)
| product(X150,X153,X152) ),
inference(resolution,[status(thm)],[associativity1,left_identity]) ).
cnf(c446,plain,
( ~ product(X1116,b,identity)
| product(X1116,c,inverse(a)) ),
inference(resolution,[status(thm)],[c43,b_times_a_inverse_is_c]) ).
cnf(c8890,plain,
product(inverse(b),c,inverse(a)),
inference(resolution,[status(thm)],[c446,left_inverse]) ).
cnf(c8897,plain,
( ~ subgroup_member(inverse(b))
| ~ subgroup_member(c)
| subgroup_member(inverse(a)) ),
inference(resolution,[status(thm)],[c8890,closure_of_product]) ).
cnf(c70653,plain,
( ~ subgroup_member(c)
| subgroup_member(inverse(a)) ),
inference(resolution,[status(thm)],[c8897,c0]) ).
cnf(an_element_in_O2,axiom,
( subgroup_member(element_in_O2(X20,X21))
| subgroup_member(X21)
| subgroup_member(X20) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',an_element_in_O2) ).
cnf(c16,plain,
( subgroup_member(element_in_O2(X26,d))
| subgroup_member(X26) ),
inference(resolution,[status(thm)],[an_element_in_O2,prove_d_is_in_subgroup]) ).
cnf(a_times_c_is_d,negated_conjecture,
product(a,c,d),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a_times_c_is_d) ).
cnf(c35,plain,
( ~ subgroup_member(a)
| ~ subgroup_member(c)
| subgroup_member(d) ),
inference(resolution,[status(thm)],[closure_of_product,a_times_c_is_d]) ).
cnf(c26,plain,
( subgroup_member(element_in_O2(X53,d))
| subgroup_member(inverse(X53)) ),
inference(resolution,[status(thm)],[c16,closure_of_inverse]) ).
cnf(c30,plain,
( ~ subgroup_member(b)
| ~ subgroup_member(inverse(a))
| subgroup_member(c) ),
inference(resolution,[status(thm)],[closure_of_product,b_times_a_inverse_is_c]) ).
cnf(c194,plain,
( ~ subgroup_member(b)
| subgroup_member(c)
| subgroup_member(element_in_O2(a,d)) ),
inference(resolution,[status(thm)],[c30,c26]) ).
cnf(c2302,plain,
( subgroup_member(c)
| subgroup_member(element_in_O2(a,d)) ),
inference(resolution,[status(thm)],[c194,b_is_in_subgroup]) ).
cnf(c3028,plain,
( subgroup_member(element_in_O2(a,d))
| ~ subgroup_member(a)
| subgroup_member(d) ),
inference(resolution,[status(thm)],[c2302,c35]) ).
cnf(c63766,plain,
( subgroup_member(element_in_O2(a,d))
| subgroup_member(d) ),
inference(resolution,[status(thm)],[c3028,c16]) ).
cnf(c63926,plain,
subgroup_member(element_in_O2(a,d)),
inference(resolution,[status(thm)],[c63766,prove_d_is_in_subgroup]) ).
cnf(property_of_O2,axiom,
( product(X83,element_in_O2(X83,X84),X84)
| subgroup_member(X84)
| subgroup_member(X83) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',property_of_O2) ).
cnf(c104,plain,
( subgroup_member(X286)
| subgroup_member(X285)
| ~ product(X285,X284,X286)
| equalish(element_in_O2(X285,X286),X284) ),
inference(resolution,[status(thm)],[property_of_O2,product_right_cancellation]) ).
cnf(c905,plain,
( subgroup_member(d)
| subgroup_member(a)
| equalish(element_in_O2(a,d),c) ),
inference(resolution,[status(thm)],[c104,a_times_c_is_d]) ).
cnf(c18350,plain,
( subgroup_member(a)
| equalish(element_in_O2(a,d),c) ),
inference(resolution,[status(thm)],[c905,prove_d_is_in_subgroup]) ).
cnf(c30701,plain,
( subgroup_member(a)
| ~ subgroup_member(element_in_O2(a,d))
| subgroup_member(c) ),
inference(resolution,[status(thm)],[c18350,subgroup_member_substitution]) ).
cnf(c98903,plain,
( subgroup_member(a)
| subgroup_member(c) ),
inference(resolution,[status(thm)],[c30701,c63926]) ).
cnf(c99199,plain,
( subgroup_member(c)
| subgroup_member(inverse(a)) ),
inference(resolution,[status(thm)],[c98903,closure_of_inverse]) ).
cnf(c99211,plain,
subgroup_member(inverse(a)),
inference(resolution,[status(thm)],[c99199,c70653]) ).
cnf(c99221,plain,
subgroup_member(inverse(inverse(a))),
inference(resolution,[status(thm)],[c99211,closure_of_inverse]) ).
cnf(c99474,plain,
subgroup_member(a),
inference(resolution,[status(thm)],[c99221,c302]) ).
cnf(c99216,plain,
( subgroup_member(c)
| ~ subgroup_member(b) ),
inference(resolution,[status(thm)],[c99199,c30]) ).
cnf(c99293,plain,
subgroup_member(c),
inference(resolution,[status(thm)],[c99216,b_is_in_subgroup]) ).
cnf(c99467,plain,
( ~ subgroup_member(a)
| subgroup_member(d) ),
inference(resolution,[status(thm)],[c99293,c35]) ).
cnf(c99593,plain,
subgroup_member(d),
inference(resolution,[status(thm)],[c99467,c99474]) ).
cnf(c99739,plain,
$false,
inference(resolution,[status(thm)],[c99593,prove_d_is_in_subgroup]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.14 % Problem : GRP039-6 : TPTP v8.1.2. Released v1.0.0.
% 0.04/0.15 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.15/0.36 % Computer : n022.cluster.edu
% 0.15/0.36 % Model : x86_64 x86_64
% 0.15/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.36 % Memory : 8042.1875MB
% 0.15/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.36 % CPULimit : 300
% 0.15/0.36 % WCLimit : 300
% 0.15/0.36 % DateTime : Thu May 9 04:44:23 EDT 2024
% 0.15/0.36 % CPUTime :
% 222.69/222.95 % Version: 1.5
% 222.69/222.95 % SZS status Unsatisfiable
% 222.69/222.95 % SZS output start CNFRefutation
% See solution above
% 222.69/222.95
% 222.69/222.95 % Initial clauses : 22
% 222.69/222.95 % Processed clauses : 1885
% 222.69/222.95 % Factors computed : 252
% 222.69/222.95 % Resolvents computed: 99489
% 222.69/222.95 % Tautologies deleted: 122
% 222.69/222.95 % Forward subsumed : 10493
% 222.69/222.95 % Backward subsumed : 293
% 222.69/222.95 % -------- CPU Time ---------
% 222.69/222.95 % User time : 222.260 s
% 222.69/222.95 % System time : 0.246 s
% 222.69/222.95 % Total time : 222.506 s
%------------------------------------------------------------------------------