%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : ALG002-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n017.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sun Sep 27 06:49:05 AM UTC 2026
% Result : Unsatisfiable 0.15s 0.39s
% Output : CNFRefutation 0.15s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 13
% Syntax : Number of formulae : 50 ( 24 unt; 0 def)
% Number of atoms : 86 ( 0 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 78 ( 42 ~; 36 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 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 : 47 ( 1 sgn 20 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(right_identity,axiom,
! [VAR_0] : product(VAR_0,multiplicative_identity,VAR_0),
file('theBenchmark.p',right_identity) ).
cnf(c_1,plain,
product(A,multiplicative_identity,A),
inference(clausify,[status(thm)],[right_identity]) ).
fof(not_abelian,axiom,
~ product(multiplicative_identity,multiplicative_identity,additive_identity),
file('theBenchmark.p',not_abelian) ).
cnf(c_2,plain,
~ product(multiplicative_identity,multiplicative_identity,additive_identity),
inference(clausify,[status(thm)],[not_abelian]) ).
fof(product_of_inverses1,axiom,
! [VAR_0,VAR_1,VAR_2] :
( product(additive_inverse(VAR_0),additive_inverse(VAR_1),VAR_2)
| ~ product(VAR_0,VAR_1,VAR_2) ),
file('theBenchmark.p',product_of_inverses1) ).
cnf(c_3,plain,
( product(additive_inverse(A),additive_inverse(B),C)
| ~ product(A,B,C) ),
inference(clausify,[status(thm)],[product_of_inverses1]) ).
fof(product_to_inverse,axiom,
! [VAR_0,VAR_1,VAR_2] :
( product(VAR_0,additive_inverse(VAR_1),additive_inverse(VAR_2))
| ~ product(VAR_0,VAR_1,VAR_2) ),
file('theBenchmark.p',product_to_inverse) ).
cnf(c_5,plain,
( product(A,additive_inverse(B),additive_inverse(C))
| ~ product(A,B,C) ),
inference(clausify,[status(thm)],[product_to_inverse]) ).
fof(inverse_and_identity,axiom,
! [VAR_0] :
( product(VAR_0,VAR_0,additive_identity)
| product(VAR_0,multiplicative_inverse(VAR_0),multiplicative_identity) ),
file('theBenchmark.p',inverse_and_identity) ).
cnf(c_6,plain,
( product(A,A,additive_identity)
| product(A,multiplicative_inverse(A),multiplicative_identity) ),
inference(clausify,[status(thm)],[inverse_and_identity]) ).
fof(inverse_greater_than_0,axiom,
! [VAR_0] :
( ~ greater_than_0(additive_inverse(VAR_0))
| ~ greater_than_0(VAR_0) ),
file('theBenchmark.p',inverse_greater_than_0) ).
cnf(c_7,plain,
( ~ greater_than_0(additive_inverse(A))
| ~ greater_than_0(A) ),
inference(clausify,[status(thm)],[inverse_greater_than_0]) ).
fof(greater_than_0_square,axiom,
! [VAR_0] :
( ~ product(VAR_0,VAR_0,additive_identity)
| ~ greater_than_0(VAR_0) ),
file('theBenchmark.p',greater_than_0_square) ).
cnf(c_8,plain,
( ~ product(A,A,additive_identity)
| ~ greater_than_0(A) ),
inference(clausify,[status(thm)],[greater_than_0_square]) ).
fof(commutativity_of_product,axiom,
! [VAR_0,VAR_1,VAR_2] :
( product(VAR_1,VAR_0,VAR_2)
| ~ product(VAR_0,VAR_1,VAR_2) ),
file('theBenchmark.p',commutativity_of_product) ).
cnf(c_9,plain,
( product(B,A,C)
| ~ product(A,B,C) ),
inference(clausify,[status(thm)],[commutativity_of_product]) ).
fof(product_and_inverse,axiom,
! [VAR_0] :
( greater_than_0(additive_inverse(VAR_0))
| product(VAR_0,VAR_0,additive_identity)
| greater_than_0(VAR_0) ),
file('theBenchmark.p',product_and_inverse) ).
cnf(c_10,plain,
( greater_than_0(additive_inverse(A))
| product(A,A,additive_identity)
| greater_than_0(A) ),
inference(clausify,[status(thm)],[product_and_inverse]) ).
fof(square_to_0,axiom,
! [VAR_0,VAR_1,VAR_2] :
( product(VAR_2,VAR_2,additive_identity)
| ~ product(VAR_0,VAR_0,additive_identity)
| ~ product(VAR_0,VAR_1,VAR_2) ),
file('theBenchmark.p',square_to_0) ).
cnf(c_11,plain,
( product(C,C,additive_identity)
| ~ product(A,A,additive_identity)
| ~ product(A,B,C) ),
inference(clausify,[status(thm)],[square_to_0]) ).
fof(product_and_greater_than_0,axiom,
! [VAR_0,VAR_1,VAR_2] :
( greater_than_0(VAR_2)
| ~ greater_than_0(VAR_1)
| ~ greater_than_0(VAR_0)
| ~ product(VAR_0,VAR_1,VAR_2) ),
file('theBenchmark.p',product_and_greater_than_0) ).
cnf(c_12,plain,
( greater_than_0(C)
| ~ greater_than_0(B)
| ~ greater_than_0(A)
| ~ product(A,B,C) ),
inference(clausify,[status(thm)],[product_and_greater_than_0]) ).
fof(a_greater_than_0,axiom,
greater_than_0(a),
file('theBenchmark.p',a_greater_than_0) ).
cnf(c_13,plain,
greater_than_0(a),
inference(clausify,[status(thm)],[a_greater_than_0]) ).
fof(prove_a_inverse_greater_than_0,axiom,
~ greater_than_0(multiplicative_inverse(a)),
file('theBenchmark.p',prove_a_inverse_greater_than_0) ).
cnf(c_14,plain,
~ greater_than_0(multiplicative_inverse(a)),
inference(clausify,[status(thm)],[prove_a_inverse_greater_than_0]) ).
cnf(c_17,plain,
product(additive_inverse(A),additive_inverse(multiplicative_identity),A),
inference(resolve,[status(thm)],[c_3,c_1]) ).
cnf(c_19,plain,
product(A,additive_inverse(multiplicative_identity),additive_inverse(A)),
inference(resolve,[status(thm)],[c_5,c_1]) ).
cnf(c_37,plain,
~ product(a,a,additive_identity),
inference(resolve,[status(thm)],[c_8,c_13]) ).
cnf(c_38,plain,
~ greater_than_0(additive_inverse(a)),
inference(resolve,[status(thm)],[c_7,c_13]) ).
cnf(c_39,plain,
( greater_than_0(additive_inverse(multiplicative_inverse(a)))
| product(multiplicative_inverse(a),multiplicative_inverse(a),additive_identity) ),
inference(resolve,[status(thm)],[c_14,c_10]) ).
cnf(c_56,plain,
product(a,multiplicative_inverse(a),multiplicative_identity),
inference(resolve,[status(thm)],[c_37,c_6]) ).
cnf(c_295,plain,
( product(A,A,additive_identity)
| ~ product(additive_inverse(A),additive_inverse(A),additive_identity) ),
inference(resolve,[status(thm)],[c_11,c_17]) ).
cnf(c_57,plain,
~ product(additive_inverse(a),additive_inverse(a),additive_identity),
inference(resolve,[status(thm)],[c_295,c_37]) ).
cnf(c_296,plain,
( greater_than_0(additive_inverse(additive_inverse(a)))
| product(additive_inverse(a),additive_inverse(a),additive_identity) ),
inference(resolve,[status(thm)],[c_38,c_10]) ).
cnf(c_58,plain,
greater_than_0(additive_inverse(additive_inverse(a))),
inference(resolve,[status(thm)],[c_57,c_296]) ).
cnf(c_297,plain,
( greater_than_0(additive_inverse(A))
| ~ greater_than_0(additive_inverse(multiplicative_identity))
| ~ greater_than_0(A) ),
inference(resolve,[status(thm)],[c_12,c_19]) ).
cnf(c_298,plain,
( greater_than_0(additive_inverse(a))
| ~ greater_than_0(additive_inverse(multiplicative_identity)) ),
inference(resolve,[status(thm)],[c_297,c_13]) ).
cnf(c_60,plain,
~ greater_than_0(additive_inverse(multiplicative_identity)),
inference(resolve,[status(thm)],[c_298,c_38]) ).
cnf(c_77,plain,
product(multiplicative_inverse(a),a,multiplicative_identity),
inference(resolve,[status(thm)],[c_56,c_9]) ).
cnf(c_299,plain,
( product(multiplicative_identity,multiplicative_identity,additive_identity)
| ~ product(multiplicative_inverse(a),multiplicative_inverse(a),additive_identity) ),
inference(resolve,[status(thm)],[c_77,c_11]) ).
cnf(c_118,plain,
~ product(multiplicative_inverse(a),multiplicative_inverse(a),additive_identity),
inference(resolve,[status(thm)],[c_2,c_299]) ).
cnf(c_119,plain,
product(multiplicative_inverse(a),additive_inverse(a),additive_inverse(multiplicative_identity)),
inference(resolve,[status(thm)],[c_77,c_5]) ).
cnf(c_121,plain,
greater_than_0(additive_inverse(multiplicative_inverse(a))),
inference(resolve,[status(thm)],[c_118,c_39]) ).
cnf(c_149,plain,
product(additive_inverse(a),multiplicative_inverse(a),additive_inverse(multiplicative_identity)),
inference(resolve,[status(thm)],[c_119,c_9]) ).
cnf(c_155,plain,
product(additive_inverse(additive_inverse(a)),additive_inverse(multiplicative_inverse(a)),additive_inverse(multiplicative_identity)),
inference(resolve,[status(thm)],[c_149,c_3]) ).
cnf(c_300,plain,
( greater_than_0(B)
| ~ greater_than_0(A)
| ~ product(additive_inverse(additive_inverse(a)),A,B) ),
inference(resolve,[status(thm)],[c_12,c_58]) ).
cnf(c_301,plain,
( greater_than_0(A)
| ~ product(additive_inverse(additive_inverse(a)),additive_inverse(multiplicative_inverse(a)),A) ),
inference(resolve,[status(thm)],[c_300,c_121]) ).
cnf(c_302,plain,
~ product(additive_inverse(additive_inverse(a)),additive_inverse(multiplicative_inverse(a)),additive_inverse(multiplicative_identity)),
inference(resolve,[status(thm)],[c_301,c_60]) ).
cnf(c_294,plain,
$false,
inference(resolve,[status(thm)],[c_155,c_302]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ALG002-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n017.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Sat Sep 26 20:52:33 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.36 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.09/0.36 % Process 1619822 was started by sandbox on n017,
% 0.09/0.36 % Sat Sep 26 20:52:33 2026
% 0.09/0.36 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.15/0.37
% 0.15/0.37 % From the command line: assign(max_seconds, 300).
% 0.15/0.39
% 0.15/0.39 % SZS status Unsatisfiable for theBenchmark
% 0.15/0.39
% 0.15/0.39 % Proof 1 at 0.01 (+ 0.01) seconds.
% 0.15/0.39 % Length of proof is 29.
% 0.15/0.39 % Level of proof is 7.
% 0.15/0.39 % Maximum clause weight is 25.000.
% 0.15/0.39 % Given clauses 89.
% 0.15/0.39
% 0.15/0.39 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------