%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : GRP012-2 : TPTP v8.1.2. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n018.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:46 EDT 2024
% Result : Unsatisfiable 4.32s 4.48s
% Output : Refutation 4.32s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 10
% Syntax : Number of clauses : 21 ( 12 unt; 0 nHn; 17 RR)
% Number of literals : 37 ( 4 equ; 17 neg)
% Maximal clause size : 4 ( 1 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-3 aty)
% Number of functors : 6 ( 6 usr; 5 con; 0-1 aty)
% Number of variables : 36 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(prove_c_inverse_equals_d,negated_conjecture,
inverse(c) != d,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_c_inverse_equals_d) ).
cnf(left_identity,axiom,
product(identity,X3,X3),
file('/export/starexec/sandbox2/benchmark/Axioms/GRP003-0.ax',left_identity) ).
cnf(total_function2,axiom,
( ~ product(X13,X14,X15)
| ~ product(X13,X14,X12)
| X15 = X12 ),
file('/export/starexec/sandbox2/benchmark/Axioms/GRP003-0.ax',total_function2) ).
cnf(c8,plain,
( ~ product(identity,X20,X19)
| X19 = X20 ),
inference(resolution,[status(thm)],[total_function2,left_identity]) ).
cnf(left_inverse,axiom,
product(inverse(X5),X5,identity),
file('/export/starexec/sandbox2/benchmark/Axioms/GRP003-0.ax',left_inverse) ).
cnf(right_identity,axiom,
product(X4,identity,X4),
file('/export/starexec/sandbox2/benchmark/Axioms/GRP003-0.ax',right_identity) ).
cnf(associativity2,axiom,
( ~ product(X32,X36,X34)
| ~ product(X36,X31,X33)
| ~ product(X32,X33,X35)
| product(X34,X31,X35) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GRP003-0.ax',associativity2) ).
cnf(c35,plain,
( ~ product(X198,X197,X195)
| ~ product(X197,X196,identity)
| product(X195,X196,X198) ),
inference(resolution,[status(thm)],[associativity2,right_identity]) ).
cnf(a_multiply_b_is_c,plain,
product(a,b,c),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a_multiply_b_is_c) ).
cnf(right_inverse,axiom,
product(X6,inverse(X6),identity),
file('/export/starexec/sandbox2/benchmark/Axioms/GRP003-0.ax',right_inverse) ).
cnf(c402,plain,
( ~ product(X352,X351,X350)
| product(X350,inverse(X351),X352) ),
inference(resolution,[status(thm)],[c35,right_inverse]) ).
cnf(c1477,plain,
product(c,inverse(b),a),
inference(resolution,[status(thm)],[c402,a_multiply_b_is_c]) ).
cnf(inverse_b_multiply_inverse_a_is_d,plain,
product(inverse(b),inverse(a),d),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',inverse_b_multiply_inverse_a_is_d) ).
cnf(associativity1,axiom,
( ~ product(X24,X28,X26)
| ~ product(X28,X23,X25)
| ~ product(X26,X23,X27)
| product(X24,X25,X27) ),
file('/export/starexec/sandbox2/benchmark/Axioms/GRP003-0.ax',associativity1) ).
cnf(c25,plain,
( ~ product(X145,X143,X146)
| ~ product(X143,inverse(X146),X144)
| product(X145,X144,identity) ),
inference(resolution,[status(thm)],[associativity1,right_inverse]) ).
cnf(c278,plain,
( ~ product(X904,inverse(b),a)
| product(X904,d,identity) ),
inference(resolution,[status(thm)],[c25,inverse_b_multiply_inverse_a_is_d]) ).
cnf(c8256,plain,
product(c,d,identity),
inference(resolution,[status(thm)],[c278,c1477]) ).
cnf(c8275,plain,
( ~ product(X1173,c,X1172)
| product(X1172,d,X1173) ),
inference(resolution,[status(thm)],[c8256,c35]) ).
cnf(c11634,plain,
product(identity,d,inverse(c)),
inference(resolution,[status(thm)],[c8275,left_inverse]) ).
cnf(c11729,plain,
inverse(c) = d,
inference(resolution,[status(thm)],[c11634,c8]) ).
cnf(c11773,plain,
$false,
inference(resolution,[status(thm)],[c11729,prove_c_inverse_equals_d]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.13 % Problem : GRP012-2 : TPTP v8.1.2. Released v1.0.0.
% 0.04/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.35 % Computer : n018.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 300
% 0.13/0.35 % DateTime : Thu May 9 04:50:23 EDT 2024
% 0.13/0.35 % CPUTime :
% 4.32/4.48 % Version: 1.5
% 4.32/4.48 % SZS status Unsatisfiable
% 4.32/4.48 % SZS output start CNFRefutation
% See solution above
% 4.32/4.48
% 4.32/4.48 % Initial clauses : 17
% 4.32/4.48 % Processed clauses : 433
% 4.32/4.48 % Factors computed : 33
% 4.32/4.48 % Resolvents computed: 11741
% 4.32/4.48 % Tautologies deleted: 21
% 4.32/4.49 % Forward subsumed : 851
% 4.32/4.49 % Backward subsumed : 12
% 4.32/4.49 % -------- CPU Time ---------
% 4.32/4.49 % User time : 4.097 s
% 4.32/4.49 % System time : 0.032 s
% 4.32/4.49 % Total time : 4.129 s
%------------------------------------------------------------------------------