%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GRP048-2 : TPTP v8.1.2. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n007.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:54 EDT 2024
% Result : Unsatisfiable 4.69s 4.86s
% Output : Refutation 4.69s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 8
% Syntax : Number of clauses : 40 ( 19 unt; 0 nHn; 30 RR)
% Number of literals : 73 ( 0 equ; 34 neg)
% Maximal clause size : 4 ( 1 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 3 ( 2 usr; 1 prp; 0-3 aty)
% Number of functors : 4 ( 4 usr; 3 con; 0-1 aty)
% Number of variables : 74 ( 3 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(prove_inverse_substitution,negated_conjecture,
~ equalish(inverse(a),inverse(b)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_inverse_substitution) ).
cnf(total_function2,axiom,
( ~ product(X9,X6,X7)
| ~ product(X9,X6,X8)
| equalish(X7,X8) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GRP005-0.ax',total_function2) ).
cnf(left_identity,axiom,
product(identity,X2,X2),
file('/export/starexec/sandbox2/benchmark/Axioms/GRP005-0.ax',left_identity) ).
cnf(associativity2,axiom,
( ~ product(X30,X34,X33)
| ~ product(X34,X29,X31)
| ~ product(X30,X31,X32)
| product(X33,X29,X32) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GRP005-0.ax',associativity2) ).
cnf(c16,plain,
( ~ product(X92,X93,X91)
| ~ product(X93,X90,X93)
| product(X91,X90,X91) ),
inference(factor,[status(thm)],[associativity2]) ).
cnf(c111,plain,
( ~ product(X142,identity,X141)
| product(X141,identity,X141) ),
inference(resolution,[status(thm)],[c16,left_identity]) ).
cnf(left_inverse,axiom,
product(inverse(X3),X3,identity),
file('/export/starexec/sandbox2/benchmark/Axioms/GRP005-0.ax',left_inverse) ).
cnf(associativity1,axiom,
( ~ product(X18,X22,X21)
| ~ product(X22,X17,X19)
| ~ product(X21,X17,X20)
| product(X18,X19,X20) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GRP005-0.ax',associativity1) ).
cnf(c12,plain,
( ~ product(X69,X70,identity)
| ~ product(X70,X68,X71)
| product(X69,X71,X68) ),
inference(resolution,[status(thm)],[associativity1,left_identity]) ).
cnf(c76,plain,
( ~ product(X227,inverse(X226),identity)
| product(X227,identity,X226) ),
inference(resolution,[status(thm)],[c12,left_inverse]) ).
cnf(c635,plain,
product(inverse(inverse(X228)),identity,X228),
inference(resolution,[status(thm)],[c76,left_inverse]) ).
cnf(c648,plain,
product(X229,identity,X229),
inference(resolution,[status(thm)],[c635,c111]) ).
cnf(c664,plain,
( ~ product(X243,identity,X244)
| equalish(X244,X243) ),
inference(resolution,[status(thm)],[c648,total_function2]) ).
cnf(c19,plain,
( ~ product(identity,X106,X107)
| ~ product(X106,X109,X108)
| product(X107,X109,X108) ),
inference(resolution,[status(thm)],[associativity2,left_identity]) ).
cnf(c142,plain,
( ~ product(identity,inverse(X418),X417)
| product(X417,X418,identity) ),
inference(resolution,[status(thm)],[c19,left_inverse]) ).
cnf(product_substitution3,axiom,
( ~ equalish(X45,X42)
| ~ product(X44,X43,X45)
| product(X44,X43,X42) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GRP005-0.ax',product_substitution3) ).
cnf(c25,plain,
( ~ equalish(X49,X50)
| product(identity,X49,X50) ),
inference(resolution,[status(thm)],[product_substitution3,left_identity]) ).
cnf(a_equals_b,plain,
equalish(a,b),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a_equals_b) ).
cnf(c30,plain,
product(identity,a,b),
inference(resolution,[status(thm)],[c25,a_equals_b]) ).
cnf(c38,plain,
( ~ product(identity,a,X89)
| equalish(X89,b) ),
inference(resolution,[status(thm)],[c30,total_function2]) ).
cnf(c776,plain,
equalish(X246,inverse(inverse(X246))),
inference(resolution,[status(thm)],[c664,c635]) ).
cnf(c794,plain,
product(identity,X282,inverse(inverse(X282))),
inference(resolution,[status(thm)],[c776,c25]) ).
cnf(c1045,plain,
equalish(inverse(inverse(a)),b),
inference(resolution,[status(thm)],[c794,c38]) ).
cnf(c1372,plain,
product(identity,inverse(inverse(a)),b),
inference(resolution,[status(thm)],[c1045,c25]) ).
cnf(c4556,plain,
product(b,inverse(a),identity),
inference(resolution,[status(thm)],[c1372,c142]) ).
cnf(c24,plain,
( ~ equalish(identity,X66)
| product(inverse(X65),X65,X66) ),
inference(resolution,[status(thm)],[product_substitution3,left_inverse]) ).
cnf(c2,plain,
( ~ product(identity,X15,X14)
| equalish(X14,X15) ),
inference(resolution,[status(thm)],[total_function2,left_identity]) ).
cnf(c10,plain,
( ~ product(X53,X54,X54)
| ~ product(X54,X55,X52)
| product(X53,X52,X52) ),
inference(factor,[status(thm)],[associativity1]) ).
cnf(c50,plain,
( ~ product(X110,identity,identity)
| product(X110,X111,X111) ),
inference(resolution,[status(thm)],[c10,left_identity]) ).
cnf(c145,plain,
product(inverse(identity),X113,X113),
inference(resolution,[status(thm)],[c50,left_inverse]) ).
cnf(c18,plain,
( ~ product(inverse(X103),X101,X102)
| ~ product(X101,X104,X103)
| product(X102,X104,identity) ),
inference(resolution,[status(thm)],[associativity2,left_inverse]) ).
cnf(c128,plain,
( ~ product(X163,X162,X163)
| product(identity,X162,identity) ),
inference(resolution,[status(thm)],[c18,left_inverse]) ).
cnf(c359,plain,
product(identity,inverse(identity),identity),
inference(resolution,[status(thm)],[c128,c145]) ).
cnf(c366,plain,
equalish(identity,inverse(identity)),
inference(resolution,[status(thm)],[c359,c2]) ).
cnf(c376,plain,
product(inverse(X165),X165,inverse(identity)),
inference(resolution,[status(thm)],[c366,c24]) ).
cnf(c146,plain,
( ~ product(X427,X428,inverse(identity))
| ~ product(X428,X429,X426)
| product(X427,X426,X429) ),
inference(resolution,[status(thm)],[c145,associativity1]) ).
cnf(c1962,plain,
( ~ product(X783,X784,X785)
| product(inverse(X783),X785,X784) ),
inference(resolution,[status(thm)],[c146,c376]) ).
cnf(c5545,plain,
product(inverse(b),identity,inverse(a)),
inference(resolution,[status(thm)],[c1962,c4556]) ).
cnf(c9818,plain,
equalish(inverse(a),inverse(b)),
inference(resolution,[status(thm)],[c5545,c664]) ).
cnf(c9854,plain,
$false,
inference(resolution,[status(thm)],[c9818,prove_inverse_substitution]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.13 % Problem : GRP048-2 : TPTP v8.1.2. Released v1.0.0.
% 0.14/0.14 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.14/0.36 % Computer : n007.cluster.edu
% 0.14/0.36 % Model : x86_64 x86_64
% 0.14/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.36 % Memory : 8042.1875MB
% 0.14/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.36 % CPULimit : 300
% 0.14/0.36 % WCLimit : 300
% 0.14/0.36 % DateTime : Thu May 9 05:00:08 EDT 2024
% 0.14/0.36 % CPUTime :
% 4.69/4.86 % Version: 1.5
% 4.69/4.86 % SZS status Unsatisfiable
% 4.69/4.86 % SZS output start CNFRefutation
% See solution above
% 4.69/4.86
% 4.69/4.86 % Initial clauses : 9
% 4.69/4.86 % Processed clauses : 447
% 4.69/4.86 % Factors computed : 43
% 4.69/4.86 % Resolvents computed: 9827
% 4.69/4.86 % Tautologies deleted: 22
% 4.69/4.86 % Forward subsumed : 941
% 4.69/4.86 % Backward subsumed : 24
% 4.69/4.86 % -------- CPU Time ---------
% 4.69/4.86 % User time : 4.464 s
% 4.69/4.86 % System time : 0.031 s
% 4.69/4.86 % Total time : 4.495 s
%------------------------------------------------------------------------------