%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : FLD031-1 : TPTP v9.3.1. Bugfixed v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n010.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 : Thu Sep 24 12:21:57 PM UTC 2026
% Result : Unsatisfiable 1.26s 0.80s
% Output : CNFRefutation 2.92s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 22
% Syntax : Number of formulae : 83 ( 17 unt; 10 def)
% Number of atoms : 184 ( 0 equ)
% Maximal formula atoms : 4 ( 2 avg)
% Number of connectives : 201 ( 100 ~; 91 |; 0 &)
% ( 10 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 13 ( 12 usr; 11 prp; 0-2 aty)
% Number of functors : 5 ( 5 usr; 3 con; 0-2 aty)
% Number of variables : 58 ( 58 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f6,axiom,
! [X] :
( ~ defined(X)
| equalish(multiply(multiplicative_identity,X),X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f7,axiom,
! [X] :
( equalish(X,additive_identity)
| ~ defined(X)
| equalish(multiply(X,multiplicative_inverse(X)),multiplicative_identity) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f14,axiom,
defined(multiplicative_identity),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f15,axiom,
! [X] :
( equalish(X,additive_identity)
| ~ defined(X)
| defined(multiplicative_inverse(X)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f21,axiom,
! [X] :
( ~ defined(X)
| equalish(X,X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f22,axiom,
! [X,Y] :
( ~ equalish(Y,X)
| equalish(X,Y) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f23,axiom,
! [X,Z,Y] :
( ~ equalish(Y,Z)
| ~ equalish(X,Y)
| equalish(X,Z) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f25,axiom,
! [X,Z,Y] :
( ~ equalish(X,Y)
| ~ defined(Z)
| equalish(multiply(X,Z),multiply(Y,Z)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f28,hypothesis,
defined(a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f29,negated_conjecture,
equalish(a,multiplicative_identity),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f30,negated_conjecture,
~ equalish(a,additive_identity),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f31,negated_conjecture,
~ equalish(multiplicative_inverse(a),multiplicative_identity),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f40,plain,
! [X0] :
( ~ defined(X0)
| equalish(multiply(multiplicative_identity,X0),X0) ),
inference(cnf_transformation,[status(thm)],[f6]) ).
fof(f41,plain,
! [X0] :
( equalish(X0,additive_identity)
| ~ defined(X0)
| equalish(multiply(X0,multiplicative_inverse(X0)),multiplicative_identity) ),
inference(cnf_transformation,[status(thm)],[f7]) ).
fof(f52,plain,
defined(multiplicative_identity),
inference(cnf_transformation,[status(thm)],[f14]) ).
fof(f53,plain,
! [X0] :
( equalish(X0,additive_identity)
| ~ defined(X0)
| defined(multiplicative_inverse(X0)) ),
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f63,plain,
! [X0] :
( ~ defined(X0)
| equalish(X0,X0) ),
inference(cnf_transformation,[status(thm)],[f21]) ).
fof(f64,plain,
! [X0,X1] :
( ~ equalish(X1,X0)
| equalish(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f22]) ).
fof(f65,plain,
! [Z,Y] :
( ~ equalish(Y,Z)
| ! [X] :
( ~ equalish(X,Y)
| equalish(X,Z) ) ),
inference(miniscoping,[status(thm)],[f23]) ).
fof(f66,plain,
! [X0,X1,X2] :
( ~ equalish(X2,X1)
| ~ equalish(X0,X2)
| equalish(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f65]) ).
fof(f69,plain,
! [X,Y] :
( ~ equalish(X,Y)
| ! [Z] :
( ~ defined(Z)
| equalish(multiply(X,Z),multiply(Y,Z)) ) ),
inference(miniscoping,[status(thm)],[f25]) ).
fof(f70,plain,
! [X0,X1,X2] :
( ~ equalish(X0,X2)
| ~ defined(X1)
| equalish(multiply(X0,X1),multiply(X2,X1)) ),
inference(cnf_transformation,[status(thm)],[f69]) ).
fof(f74,plain,
defined(a),
inference(cnf_transformation,[status(thm)],[f28]) ).
fof(f75,plain,
equalish(a,multiplicative_identity),
inference(cnf_transformation,[status(thm)],[f29]) ).
fof(f76,plain,
~ equalish(a,additive_identity),
inference(cnf_transformation,[status(thm)],[f30]) ).
fof(f77,plain,
~ equalish(multiplicative_inverse(a),multiplicative_identity),
inference(cnf_transformation,[status(thm)],[f31]) ).
fof(f79,plain,
equalish(multiplicative_identity,multiplicative_identity),
inference(resolution,[status(thm)],[f63,f52]) ).
fof(f85,plain,
equalish(multiplicative_identity,a),
inference(resolution,[status(thm)],[f64,f75]) ).
fof(f93,plain,
! [X0] :
( ~ equalish(a,X0)
| equalish(multiplicative_identity,X0) ),
inference(resolution,[status(thm)],[f66,f85]) ).
fof(f104,plain,
! [X0] :
( ~ equalish(X0,multiplicative_identity)
| equalish(X0,a) ),
inference(resolution,[status(thm)],[f66,f85]) ).
fof(f108,plain,
! [X0] :
( ~ equalish(X0,a)
| equalish(X0,multiplicative_identity) ),
inference(resolution,[status(thm)],[f66,f75]) ).
fof(f113,plain,
! [X0,X1] :
( ~ equalish(X1,X0)
| equalish(X1,a)
| ~ equalish(X0,multiplicative_identity) ),
inference(resolution,[status(thm)],[f104,f66]) ).
fof(f116,plain,
! [X0] :
( equalish(a,X0)
| ~ equalish(X0,multiplicative_identity) ),
inference(resolution,[status(thm)],[f104,f64]) ).
fof(f117,definition,
( sQ0_spl
<=> equalish(a,multiplicative_identity) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f119,plain,
( sQ0_spl
| ~ equalish(a,multiplicative_identity) ),
inference(component_clause,[status(thm)],[f117]) ).
fof(f125,plain,
( sQ0_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f119,f75]) ).
fof(f126,plain,
sQ0_spl,
inference(contradiction_clause,[status(thm)],[f125]) ).
fof(f139,definition,
( sQ3_spl
<=> defined(a) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f141,plain,
( sQ3_spl
| ~ defined(a) ),
inference(component_clause,[status(thm)],[f139]) ).
fof(f147,plain,
( sQ3_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f141,f74]) ).
fof(f148,plain,
sQ3_spl,
inference(contradiction_clause,[status(thm)],[f147]) ).
fof(f154,plain,
! [X0,X1] :
( ~ equalish(X0,X1)
| equalish(a,X1)
| ~ equalish(X0,multiplicative_identity) ),
inference(resolution,[status(thm)],[f116,f66]) ).
fof(f164,plain,
! [X0,X1] :
( equalish(a,X1)
| ~ equalish(X1,X0)
| ~ equalish(X0,multiplicative_identity) ),
inference(resolution,[status(thm)],[f113,f64]) ).
fof(f189,plain,
! [X0] :
( ~ equalish(X0,additive_identity)
| ~ equalish(X0,multiplicative_identity) ),
inference(resolution,[status(thm)],[f154,f76]) ).
fof(f196,plain,
! [X0,X1] :
( equalish(X1,a)
| ~ equalish(X0,X1)
| ~ equalish(X0,multiplicative_identity) ),
inference(resolution,[status(thm)],[f154,f64]) ).
fof(f210,plain,
( ~ equalish(multiplicative_identity,multiplicative_identity)
| ~ equalish(a,additive_identity) ),
inference(resolution,[status(thm)],[f189,f116]) ).
fof(f222,definition,
( sQ13_spl
<=> equalish(a,additive_identity) ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f225,definition,
! [X0] :
( sQ14_spl
<=> ( ~ equalish(X0,multiplicative_identity)
| ~ equalish(X0,multiplicative_identity) ) ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f226,plain,
! [X0] :
( ~ sQ14_spl
| ~ equalish(X0,multiplicative_identity)
| ~ equalish(X0,multiplicative_identity) ),
inference(component_clause,[status(thm)],[f225]) ).
fof(f229,definition,
( sQ15_spl
<=> equalish(multiplicative_identity,multiplicative_identity) ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f231,plain,
( sQ15_spl
| ~ equalish(multiplicative_identity,multiplicative_identity) ),
inference(component_clause,[status(thm)],[f229]) ).
fof(f232,plain,
( ~ sQ15_spl
| ~ sQ13_spl ),
inference(split_clause,[status(thm)],[f210,f222,f229]) ).
fof(f318,plain,
( sQ15_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f231,f79]) ).
fof(f319,plain,
sQ15_spl,
inference(contradiction_clause,[status(thm)],[f318]) ).
fof(f358,plain,
! [X0,X1] :
( equalish(X1,multiplicative_identity)
| ~ equalish(X0,X1)
| ~ equalish(X0,multiplicative_identity) ),
inference(resolution,[status(thm)],[f196,f108]) ).
fof(f444,definition,
( sQ33_spl
<=> equalish(multiplicative_identity,a) ),
introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition]) ).
fof(f484,plain,
! [X0] :
( ~ equalish(X0,multiplicative_inverse(a))
| ~ equalish(X0,multiplicative_identity) ),
inference(resolution,[status(thm)],[f358,f77]) ).
fof(f496,plain,
! [X0] :
( ~ sQ14_spl
| ~ equalish(X0,multiplicative_identity) ),
inference(duplicate_literals_removal,[status(thm)],[f226]) ).
fof(f499,plain,
( ~ sQ14_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f79,f496]) ).
fof(f504,plain,
~ sQ14_spl,
inference(contradiction_clause,[status(thm)],[f499]) ).
fof(f553,plain,
( ~ defined(multiplicative_inverse(a))
| ~ equalish(multiply(multiplicative_identity,multiplicative_inverse(a)),multiplicative_identity) ),
inference(resolution,[status(thm)],[f484,f40]) ).
fof(f557,definition,
( sQ38_spl
<=> equalish(multiply(multiplicative_identity,multiplicative_inverse(a)),multiplicative_identity) ),
introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition]) ).
fof(f559,plain,
( sQ38_spl
| ~ equalish(multiply(multiplicative_identity,multiplicative_inverse(a)),multiplicative_identity) ),
inference(component_clause,[status(thm)],[f557]) ).
fof(f560,definition,
( sQ39_spl
<=> defined(multiplicative_inverse(a)) ),
introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition]) ).
fof(f562,plain,
( sQ39_spl
| ~ defined(multiplicative_inverse(a)) ),
inference(component_clause,[status(thm)],[f560]) ).
fof(f563,plain,
( ~ sQ39_spl
| ~ sQ38_spl ),
inference(split_clause,[status(thm)],[f553,f557,f560]) ).
fof(f576,plain,
( sQ39_spl
| equalish(a,additive_identity)
| ~ defined(a) ),
inference(resolution,[status(thm)],[f562,f53]) ).
fof(f577,plain,
( sQ39_spl
| sQ13_spl
| ~ sQ3_spl ),
inference(split_clause,[status(thm)],[f576,f139,f222,f560]) ).
fof(f722,plain,
! [X0] :
( sQ38_spl
| ~ equalish(X0,multiply(multiplicative_identity,multiplicative_inverse(a)))
| ~ equalish(X0,multiplicative_identity) ),
inference(resolution,[status(thm)],[f358,f559]) ).
fof(f1467,plain,
! [X0,X1] :
( ~ equalish(X0,X1)
| ~ equalish(X1,multiplicative_identity)
| equalish(multiplicative_identity,X0) ),
inference(resolution,[status(thm)],[f93,f164]) ).
fof(f1474,plain,
( ~ equalish(a,multiplicative_identity)
| equalish(multiplicative_identity,a) ),
inference(resolution,[status(thm)],[f93,f104]) ).
fof(f1484,plain,
( ~ sQ0_spl
| sQ33_spl ),
inference(split_clause,[status(thm)],[f1474,f444,f117]) ).
fof(f1891,plain,
! [X0] :
( sQ38_spl
| ~ equalish(multiply(multiplicative_identity,multiplicative_inverse(a)),X0)
| ~ equalish(X0,multiplicative_identity)
| ~ equalish(multiplicative_identity,multiplicative_identity) ),
inference(resolution,[status(thm)],[f722,f1467]) ).
fof(f1930,definition,
! [X0] :
( sQ142_spl
<=> ( ~ equalish(multiply(multiplicative_identity,multiplicative_inverse(a)),X0)
| ~ equalish(X0,multiplicative_identity) ) ),
introduced(definition,[new_symbols(definition,[sQ142_spl])],[split_symbol_definition]) ).
fof(f1931,plain,
! [X0] :
( ~ sQ142_spl
| ~ equalish(multiply(multiplicative_identity,multiplicative_inverse(a)),X0)
| ~ equalish(X0,multiplicative_identity) ),
inference(component_clause,[status(thm)],[f1930]) ).
fof(f1933,plain,
( sQ38_spl
| sQ142_spl
| ~ sQ15_spl ),
inference(split_clause,[status(thm)],[f1891,f229,f1930,f557]) ).
fof(f3061,plain,
! [X0] :
( ~ sQ142_spl
| ~ equalish(multiply(X0,multiplicative_inverse(a)),multiplicative_identity)
| ~ equalish(multiplicative_identity,X0)
| ~ defined(multiplicative_inverse(a)) ),
inference(resolution,[status(thm)],[f70,f1931]) ).
fof(f3074,definition,
! [X0] :
( sQ263_spl
<=> ( ~ equalish(multiply(X0,multiplicative_inverse(a)),multiplicative_identity)
| ~ equalish(multiplicative_identity,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ263_spl])],[split_symbol_definition]) ).
fof(f3075,plain,
! [X0] :
( ~ sQ263_spl
| ~ equalish(multiply(X0,multiplicative_inverse(a)),multiplicative_identity)
| ~ equalish(multiplicative_identity,X0) ),
inference(component_clause,[status(thm)],[f3074]) ).
fof(f3077,plain,
( ~ sQ142_spl
| sQ263_spl
| ~ sQ39_spl ),
inference(split_clause,[status(thm)],[f3061,f560,f3074,f1930]) ).
fof(f3233,plain,
( ~ sQ263_spl
| equalish(a,additive_identity)
| ~ defined(a)
| ~ equalish(multiplicative_identity,a) ),
inference(resolution,[status(thm)],[f3075,f41]) ).
fof(f3236,plain,
( ~ sQ263_spl
| sQ13_spl
| ~ sQ3_spl
| ~ sQ33_spl ),
inference(split_clause,[status(thm)],[f3233,f444,f139,f222,f3074]) ).
fof(f3237,plain,
$false,
inference(sat_refutation,[status(thm)],[f126,f148,f232,f319,f504,f563,f577,f1484,f1933,f3077,f3236]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : FLD031-1 : TPTP v9.3.1. Bugfixed v2.1.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.37 % Computer : n010.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Mon Sep 21 15:39:44 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.39 % Drodi V4.1.1
% 1.26/0.80 % Refutation found
% 1.26/0.80 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 1.26/0.80 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 2.92/0.83 % Elapsed time: 0.432272 seconds
% 2.92/0.83 % CPU time: 3.206306 seconds
% 2.92/0.83 % Total memory used: 62.416 MB
% 2.92/0.83 % Net memory used: 56.627 MB
%------------------------------------------------------------------------------