%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : ALG002-1 : TPTP v8.1.2. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n009.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:14:35 EDT 2024
% Result : Unsatisfiable 1.82s 2.07s
% Output : Refutation 1.82s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 13
% Syntax : Number of clauses : 38 ( 16 unt; 8 nHn; 32 RR)
% Number of literals : 69 ( 0 equ; 27 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 : 5 ( 5 usr; 3 con; 0-1 aty)
% Number of variables : 29 ( 2 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(inverse_greater_than_0,axiom,
( ~ greater_than_0(X3)
| ~ greater_than_0(additive_inverse(X3)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',inverse_greater_than_0) ).
cnf(product_of_inverses2,axiom,
( product(X16,X14,X15)
| ~ product(additive_inverse(X16),additive_inverse(X14),X15) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',product_of_inverses2) ).
cnf(right_identity,axiom,
product(X2,multiplicative_identity,X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',right_identity) ).
cnf(product_to_inverse,axiom,
( ~ product(X24,X22,X23)
| product(X24,additive_inverse(X22),additive_inverse(X23)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',product_to_inverse) ).
cnf(c10,plain,
product(X25,additive_inverse(multiplicative_identity),additive_inverse(X25)),
inference(resolution,[status(thm)],[product_to_inverse,right_identity]) ).
cnf(c16,plain,
product(X27,multiplicative_identity,additive_inverse(additive_inverse(X27))),
inference(resolution,[status(thm)],[c10,product_of_inverses2]) ).
cnf(product_and_greater_than_0,axiom,
( ~ product(X41,X42,X43)
| ~ greater_than_0(X41)
| ~ greater_than_0(X42)
| greater_than_0(X43) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',product_and_greater_than_0) ).
cnf(c67,plain,
( ~ greater_than_0(X73)
| ~ greater_than_0(multiplicative_identity)
| greater_than_0(additive_inverse(additive_inverse(X73))) ),
inference(resolution,[status(thm)],[product_and_greater_than_0,c16]) ).
cnf(c233,plain,
( ~ greater_than_0(multiplicative_identity)
| greater_than_0(additive_inverse(additive_inverse(multiplicative_identity))) ),
inference(factor,[status(thm)],[c67]) ).
cnf(a_greater_than_0,plain,
greater_than_0(a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a_greater_than_0) ).
cnf(not_abelian,axiom,
~ product(multiplicative_identity,multiplicative_identity,additive_identity),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',not_abelian) ).
cnf(product_and_inverse,axiom,
( greater_than_0(X34)
| product(X34,X34,additive_identity)
| greater_than_0(additive_inverse(X34)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',product_and_inverse) ).
cnf(c47,plain,
( greater_than_0(multiplicative_identity)
| greater_than_0(additive_inverse(multiplicative_identity)) ),
inference(resolution,[status(thm)],[product_and_inverse,not_abelian]) ).
cnf(commutativity_of_product,axiom,
( ~ product(X10,X8,X9)
| product(X8,X10,X9) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',commutativity_of_product) ).
cnf(c17,plain,
product(additive_inverse(multiplicative_identity),X28,additive_inverse(X28)),
inference(resolution,[status(thm)],[c10,commutativity_of_product]) ).
cnf(c74,plain,
( ~ greater_than_0(additive_inverse(multiplicative_identity))
| ~ greater_than_0(X76)
| greater_than_0(additive_inverse(X76)) ),
inference(resolution,[status(thm)],[product_and_greater_than_0,c17]) ).
cnf(c244,plain,
( ~ greater_than_0(X77)
| greater_than_0(additive_inverse(X77))
| greater_than_0(multiplicative_identity) ),
inference(resolution,[status(thm)],[c74,c47]) ).
cnf(c249,plain,
( greater_than_0(additive_inverse(a))
| greater_than_0(multiplicative_identity) ),
inference(resolution,[status(thm)],[c244,a_greater_than_0]) ).
cnf(c252,plain,
( greater_than_0(multiplicative_identity)
| ~ greater_than_0(a) ),
inference(resolution,[status(thm)],[c249,inverse_greater_than_0]) ).
cnf(c264,plain,
greater_than_0(multiplicative_identity),
inference(resolution,[status(thm)],[c252,a_greater_than_0]) ).
cnf(c279,plain,
greater_than_0(additive_inverse(additive_inverse(multiplicative_identity))),
inference(resolution,[status(thm)],[c264,c233]) ).
cnf(c284,plain,
~ greater_than_0(additive_inverse(multiplicative_identity)),
inference(resolution,[status(thm)],[c279,inverse_greater_than_0]) ).
cnf(greater_than_0_square,axiom,
( ~ greater_than_0(X7)
| ~ product(X7,X7,additive_identity) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',greater_than_0_square) ).
cnf(inverse_and_identity,axiom,
( product(X30,multiplicative_inverse(X30),multiplicative_identity)
| product(X30,X30,additive_identity) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',inverse_and_identity) ).
cnf(c36,plain,
( product(X35,multiplicative_inverse(X35),multiplicative_identity)
| ~ greater_than_0(X35) ),
inference(resolution,[status(thm)],[inverse_and_identity,greater_than_0_square]) ).
cnf(c55,plain,
product(a,multiplicative_inverse(a),multiplicative_identity),
inference(resolution,[status(thm)],[c36,a_greater_than_0]) ).
cnf(c59,plain,
product(a,additive_inverse(multiplicative_inverse(a)),additive_inverse(multiplicative_identity)),
inference(resolution,[status(thm)],[c55,product_to_inverse]) ).
cnf(c202,plain,
( ~ greater_than_0(a)
| ~ greater_than_0(additive_inverse(multiplicative_inverse(a)))
| greater_than_0(additive_inverse(multiplicative_identity)) ),
inference(resolution,[status(thm)],[c59,product_and_greater_than_0]) ).
cnf(c60,plain,
product(multiplicative_inverse(a),a,multiplicative_identity),
inference(resolution,[status(thm)],[c55,commutativity_of_product]) ).
cnf(square_to_0,axiom,
( ~ product(X36,X37,X38)
| ~ product(X36,X36,additive_identity)
| product(X38,X38,additive_identity) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',square_to_0) ).
cnf(prove_a_inverse_greater_than_0,negated_conjecture,
~ greater_than_0(multiplicative_inverse(a)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_a_inverse_greater_than_0) ).
cnf(c44,plain,
( product(multiplicative_inverse(a),multiplicative_inverse(a),additive_identity)
| greater_than_0(additive_inverse(multiplicative_inverse(a))) ),
inference(resolution,[status(thm)],[product_and_inverse,prove_a_inverse_greater_than_0]) ).
cnf(c270,plain,
( greater_than_0(additive_inverse(multiplicative_inverse(a)))
| ~ product(multiplicative_inverse(a),X353,X352)
| product(X352,X352,additive_identity) ),
inference(resolution,[status(thm)],[c44,square_to_0]) ).
cnf(c3085,plain,
( greater_than_0(additive_inverse(multiplicative_inverse(a)))
| product(multiplicative_identity,multiplicative_identity,additive_identity) ),
inference(resolution,[status(thm)],[c270,c60]) ).
cnf(c3321,plain,
greater_than_0(additive_inverse(multiplicative_inverse(a))),
inference(resolution,[status(thm)],[c3085,not_abelian]) ).
cnf(c3340,plain,
( ~ greater_than_0(a)
| greater_than_0(additive_inverse(multiplicative_identity)) ),
inference(resolution,[status(thm)],[c3321,c202]) ).
cnf(c3347,plain,
greater_than_0(additive_inverse(multiplicative_identity)),
inference(resolution,[status(thm)],[c3340,a_greater_than_0]) ).
cnf(c3354,plain,
$false,
inference(resolution,[status(thm)],[c3347,c284]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.12 % Problem : ALG002-1 : TPTP v8.1.2. Released v1.0.0.
% 0.08/0.12 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.12/0.33 % Computer : n009.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Thu May 9 00:34:53 EDT 2024
% 0.12/0.33 % CPUTime :
% 1.82/2.07 % Version: 1.5
% 1.82/2.07 % SZS status Unsatisfiable
% 1.82/2.07 % SZS output start CNFRefutation
% See solution above
% 1.82/2.07
% 1.82/2.07 % Initial clauses : 14
% 1.82/2.07 % Processed clauses : 232
% 1.82/2.07 % Factors computed : 5
% 1.82/2.07 % Resolvents computed: 3367
% 1.82/2.07 % Tautologies deleted: 29
% 1.82/2.07 % Forward subsumed : 411
% 1.82/2.07 % Backward subsumed : 34
% 1.82/2.07 % -------- CPU Time ---------
% 1.82/2.07 % User time : 1.698 s
% 1.82/2.07 % System time : 0.023 s
% 1.82/2.07 % Total time : 1.721 s
%------------------------------------------------------------------------------