%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GRP033-3 : TPTP v8.1.2. Bugfixed v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n032.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:51 EDT 2024
% Result : Unsatisfiable 0.80s 0.97s
% Output : Refutation 0.80s
% Verified :
% SZS Type : Refutation
% Derivation depth : 7
% Number of leaves : 11
% Syntax : Number of clauses : 28 ( 15 unt; 0 nHn; 21 RR)
% Number of literals : 48 ( 0 equ; 23 neg)
% Maximal clause size : 4 ( 1 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 4 ( 3 usr; 1 prp; 0-3 aty)
% Number of functors : 4 ( 4 usr; 2 con; 0-1 aty)
% Number of variables : 31 ( 1 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(subgr2_clause1,plain,
( ~ subgroup_member(X15)
| subgroup_member(j(X15)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',subgr2_clause1) ).
cnf(a_is_in_subgroup,plain,
subgroup_member(a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a_is_in_subgroup) ).
cnf(c3,plain,
subgroup_member(j(a)),
inference(resolution,[status(thm)],[subgr2_clause1,a_is_in_subgroup]) ).
cnf(c5,plain,
subgroup_member(j(j(a))),
inference(resolution,[status(thm)],[c3,subgr2_clause1]) ).
cnf(c6,plain,
subgroup_member(j(j(j(a)))),
inference(resolution,[status(thm)],[c5,subgr2_clause1]) ).
cnf(c9,plain,
subgroup_member(j(j(j(j(a))))),
inference(resolution,[status(thm)],[c6,subgr2_clause1]) ).
cnf(right_inverse,axiom,
product(X12,inverse(X12),identity),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',right_inverse) ).
cnf(closure_of_product_and_inverse,axiom,
( ~ subgroup_member(X99)
| ~ subgroup_member(X101)
| ~ product(X99,inverse(X101),X100)
| subgroup_member(X100) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',closure_of_product_and_inverse) ).
cnf(c129,plain,
( ~ subgroup_member(X103)
| subgroup_member(identity) ),
inference(resolution,[status(thm)],[closure_of_product_and_inverse,right_inverse]) ).
cnf(c130,plain,
subgroup_member(identity),
inference(resolution,[status(thm)],[c129,c9]) ).
cnf(subgroup_member_substitution,axiom,
( ~ equalish(X25,X26)
| ~ subgroup_member(X25)
| subgroup_member(X26) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',subgroup_member_substitution) ).
cnf(left_identity,axiom,
product(identity,X3,X3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',left_identity) ).
cnf(total_function2,axiom,
( ~ product(X69,X68,X71)
| ~ product(X69,X68,X70)
| equalish(X71,X70) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',total_function2) ).
cnf(c35,plain,
( ~ product(identity,X78,X77)
| equalish(X77,X78) ),
inference(resolution,[status(thm)],[total_function2,left_identity]) ).
cnf(c43,plain,
equalish(identity,inverse(identity)),
inference(resolution,[status(thm)],[c35,right_inverse]) ).
cnf(c63,plain,
( ~ subgroup_member(identity)
| subgroup_member(inverse(identity)) ),
inference(resolution,[status(thm)],[c43,subgroup_member_substitution]) ).
cnf(c205,plain,
subgroup_member(inverse(identity)),
inference(resolution,[status(thm)],[c63,c130]) ).
cnf(right_identity,axiom,
product(X4,identity,X4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',right_identity) ).
cnf(product_substitution2,axiom,
( ~ equalish(X45,X44)
| ~ product(X46,X45,X47)
| product(X46,X44,X47) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',product_substitution2) ).
cnf(c21,plain,
( ~ equalish(identity,X52)
| product(X53,X52,X53) ),
inference(resolution,[status(thm)],[product_substitution2,right_identity]) ).
cnf(c64,plain,
product(X88,inverse(identity),X88),
inference(resolution,[status(thm)],[c43,c21]) ).
cnf(product_substitution1,axiom,
( ~ equalish(X36,X35)
| ~ product(X36,X37,X38)
| product(X35,X37,X38) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',product_substitution1) ).
cnf(c12,plain,
( ~ equalish(identity,X39)
| product(X39,X40,X40) ),
inference(resolution,[status(thm)],[product_substitution1,left_identity]) ).
cnf(c66,plain,
product(inverse(identity),X89,X89),
inference(resolution,[status(thm)],[c43,c12]) ).
cnf(prove_subgr2,negated_conjecture,
( ~ product(j(X104),X104,j(X104))
| ~ product(X104,j(X104),j(X104))
| ~ subgroup_member(X104) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_subgr2) ).
cnf(c136,plain,
( ~ product(j(inverse(identity)),inverse(identity),j(inverse(identity)))
| ~ subgroup_member(inverse(identity)) ),
inference(resolution,[status(thm)],[prove_subgr2,c66]) ).
cnf(c2033,plain,
~ subgroup_member(inverse(identity)),
inference(resolution,[status(thm)],[c136,c64]) ).
cnf(c2034,plain,
$false,
inference(resolution,[status(thm)],[c2033,c205]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.10 % Problem : GRP033-3 : TPTP v8.1.2. Bugfixed v4.0.0.
% 0.06/0.10 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.10/0.29 % Computer : n032.cluster.edu
% 0.10/0.29 % Model : x86_64 x86_64
% 0.10/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.29 % Memory : 8042.1875MB
% 0.10/0.29 % OS : Linux 3.10.0-693.el7.x86_64
% 0.10/0.29 % CPULimit : 300
% 0.10/0.29 % WCLimit : 300
% 0.10/0.29 % DateTime : Thu May 9 03:35:22 EDT 2024
% 0.10/0.29 % CPUTime :
% 0.80/0.97 % Version: 1.5
% 0.80/0.97 % SZS status Unsatisfiable
% 0.80/0.97 % SZS output start CNFRefutation
% See solution above
% 0.80/0.98
% 0.80/0.98 % Initial clauses : 22
% 0.80/0.98 % Processed clauses : 195
% 0.80/0.98 % Factors computed : 27
% 0.80/0.98 % Resolvents computed: 2008
% 0.80/0.98 % Tautologies deleted: 17
% 0.80/0.98 % Forward subsumed : 179
% 0.80/0.98 % Backward subsumed : 6
% 0.80/0.98 % -------- CPU Time ---------
% 0.80/0.98 % User time : 0.655 s
% 0.80/0.98 % System time : 0.010 s
% 0.80/0.98 % Total time : 0.665 s
%------------------------------------------------------------------------------