%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : FLD050-4 : TPTP v9.3.1. Bugfixed v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n004.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:22:02 PM UTC 2026
% Result : Unsatisfiable 0.24s 6.09s
% Output : CNFRefutation 0.24s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 47
% Syntax : Number of formulae : 178 ( 71 unt; 26 def)
% Number of atoms : 329 ( 0 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 237 ( 86 ~; 125 |; 0 &)
% ( 26 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 31 ( 30 usr; 27 prp; 0-3 aty)
% Number of functors : 10 ( 10 usr; 8 con; 0-1 aty)
% Number of variables : 69 ( 69 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f6,axiom,
! [X,V,W,Y,U,Z] :
( ~ product(U,Z,W)
| ~ product(Y,Z,V)
| ~ product(X,Y,U)
| product(X,V,W) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f8,axiom,
! [X] :
( ~ defined(X)
| product(multiplicative_identity,X,X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f9,axiom,
! [X] :
( ~ defined(X)
| sum(additive_identity,X,additive_identity)
| product(multiplicative_inverse(X),X,multiplicative_identity) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f10,axiom,
! [Y,X,Z] :
( ~ product(X,Y,Z)
| product(Y,X,Z) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f14,axiom,
defined(additive_identity),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f15,axiom,
! [X] :
( ~ defined(X)
| defined(additive_inverse(X)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f17,axiom,
defined(multiplicative_identity),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f23,axiom,
! [X,Y] :
( ~ defined(Y)
| ~ defined(X)
| less_or_equal(Y,X)
| less_or_equal(X,Y) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f26,axiom,
~ sum(additive_identity,additive_identity,multiplicative_identity),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f27,hypothesis,
defined(a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f28,hypothesis,
defined(b),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f29,hypothesis,
defined(c),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f30,hypothesis,
defined(d),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f31,hypothesis,
defined(k),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f32,hypothesis,
defined(s),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f33,negated_conjecture,
~ sum(additive_identity,b,additive_identity),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f34,negated_conjecture,
~ sum(additive_identity,d,additive_identity),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f35,negated_conjecture,
product(a,multiplicative_inverse(b),s),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f36,negated_conjecture,
product(a,d,k),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f37,negated_conjecture,
product(b,c,k),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f38,negated_conjecture,
~ product(c,multiplicative_inverse(d),s),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f46,plain,
! [W,U,Z] :
( ~ product(U,Z,W)
| ! [V,Y] :
( ~ product(Y,Z,V)
| ! [X] :
( ~ product(X,Y,U)
| product(X,V,W) ) ) ),
inference(miniscoping,[status(thm)],[f6]) ).
fof(f47,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ product(X4,X5,X2)
| ~ product(X3,X5,X1)
| ~ product(X0,X3,X4)
| product(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f46]) ).
fof(f50,plain,
! [X0] :
( ~ defined(X0)
| product(multiplicative_identity,X0,X0) ),
inference(cnf_transformation,[status(thm)],[f8]) ).
fof(f51,plain,
! [X0] :
( ~ defined(X0)
| sum(additive_identity,X0,additive_identity)
| product(multiplicative_inverse(X0),X0,multiplicative_identity) ),
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f52,plain,
! [X0,X1,X2] :
( ~ product(X1,X0,X2)
| product(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f10]) ).
fof(f59,plain,
defined(additive_identity),
inference(cnf_transformation,[status(thm)],[f14]) ).
fof(f60,plain,
! [X0] :
( ~ defined(X0)
| defined(additive_inverse(X0)) ),
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f63,plain,
defined(multiplicative_identity),
inference(cnf_transformation,[status(thm)],[f17]) ).
fof(f72,plain,
! [Y] :
( ~ defined(Y)
| ! [X] :
( ~ defined(X)
| less_or_equal(Y,X)
| less_or_equal(X,Y) ) ),
inference(miniscoping,[status(thm)],[f23]) ).
fof(f73,plain,
! [X0,X1] :
( ~ defined(X1)
| ~ defined(X0)
| less_or_equal(X1,X0)
| less_or_equal(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f72]) ).
fof(f77,plain,
~ sum(additive_identity,additive_identity,multiplicative_identity),
inference(cnf_transformation,[status(thm)],[f26]) ).
fof(f78,plain,
defined(a),
inference(cnf_transformation,[status(thm)],[f27]) ).
fof(f79,plain,
defined(b),
inference(cnf_transformation,[status(thm)],[f28]) ).
fof(f80,plain,
defined(c),
inference(cnf_transformation,[status(thm)],[f29]) ).
fof(f81,plain,
defined(d),
inference(cnf_transformation,[status(thm)],[f30]) ).
fof(f82,plain,
defined(k),
inference(cnf_transformation,[status(thm)],[f31]) ).
fof(f83,plain,
defined(s),
inference(cnf_transformation,[status(thm)],[f32]) ).
fof(f84,plain,
~ sum(additive_identity,b,additive_identity),
inference(cnf_transformation,[status(thm)],[f33]) ).
fof(f85,plain,
~ sum(additive_identity,d,additive_identity),
inference(cnf_transformation,[status(thm)],[f34]) ).
fof(f86,plain,
product(a,multiplicative_inverse(b),s),
inference(cnf_transformation,[status(thm)],[f35]) ).
fof(f87,plain,
product(a,d,k),
inference(cnf_transformation,[status(thm)],[f36]) ).
fof(f88,plain,
product(b,c,k),
inference(cnf_transformation,[status(thm)],[f37]) ).
fof(f89,plain,
~ product(c,multiplicative_inverse(d),s),
inference(cnf_transformation,[status(thm)],[f38]) ).
fof(f90,plain,
defined(additive_inverse(s)),
inference(resolution,[status(thm)],[f60,f83]) ).
fof(f91,plain,
defined(additive_inverse(k)),
inference(resolution,[status(thm)],[f60,f82]) ).
fof(f92,plain,
defined(additive_inverse(d)),
inference(resolution,[status(thm)],[f60,f81]) ).
fof(f93,plain,
defined(additive_inverse(multiplicative_identity)),
inference(resolution,[status(thm)],[f60,f63]) ).
fof(f94,plain,
defined(additive_inverse(c)),
inference(resolution,[status(thm)],[f60,f80]) ).
fof(f95,plain,
defined(additive_inverse(b)),
inference(resolution,[status(thm)],[f60,f79]) ).
fof(f96,plain,
defined(additive_inverse(a)),
inference(resolution,[status(thm)],[f60,f78]) ).
fof(f97,plain,
defined(additive_inverse(additive_identity)),
inference(resolution,[status(thm)],[f60,f59]) ).
fof(f98,plain,
defined(additive_inverse(additive_inverse(s))),
inference(resolution,[status(thm)],[f90,f60]) ).
fof(f150,definition,
( sQ7_spl
<=> sum(additive_identity,d,additive_identity) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f151,plain,
( ~ sQ7_spl
| sum(additive_identity,d,additive_identity) ),
inference(component_clause,[status(thm)],[f150]) ).
fof(f171,definition,
( sQ13_spl
<=> sum(additive_identity,b,additive_identity) ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f172,plain,
( ~ sQ13_spl
| sum(additive_identity,b,additive_identity) ),
inference(component_clause,[status(thm)],[f171]) ).
fof(f192,plain,
( sum(additive_identity,d,additive_identity)
| product(multiplicative_inverse(d),d,multiplicative_identity) ),
inference(resolution,[status(thm)],[f51,f81]) ).
fof(f195,plain,
( sum(additive_identity,b,additive_identity)
| product(multiplicative_inverse(b),b,multiplicative_identity) ),
inference(resolution,[status(thm)],[f51,f79]) ).
fof(f210,definition,
( sQ21_spl
<=> product(multiplicative_inverse(d),d,multiplicative_identity) ),
introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition]) ).
fof(f211,plain,
( ~ sQ21_spl
| product(multiplicative_inverse(d),d,multiplicative_identity) ),
inference(component_clause,[status(thm)],[f210]) ).
fof(f213,plain,
( sQ7_spl
| sQ21_spl ),
inference(split_clause,[status(thm)],[f192,f210,f150]) ).
fof(f222,definition,
( sQ24_spl
<=> product(multiplicative_inverse(b),b,multiplicative_identity) ),
introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition]) ).
fof(f223,plain,
( ~ sQ24_spl
| product(multiplicative_inverse(b),b,multiplicative_identity) ),
inference(component_clause,[status(thm)],[f222]) ).
fof(f225,plain,
( sQ13_spl
| sQ24_spl ),
inference(split_clause,[status(thm)],[f195,f222,f171]) ).
fof(f234,plain,
( ~ sQ13_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f172,f84]) ).
fof(f235,plain,
~ sQ13_spl,
inference(contradiction_clause,[status(thm)],[f234]) ).
fof(f236,plain,
( ~ sQ7_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f151,f85]) ).
fof(f237,plain,
~ sQ7_spl,
inference(contradiction_clause,[status(thm)],[f236]) ).
fof(f238,plain,
! [X0] :
( ~ defined(X0)
| less_or_equal(additive_inverse(s),X0)
| less_or_equal(X0,additive_inverse(s)) ),
inference(resolution,[status(thm)],[f73,f90]) ).
fof(f239,plain,
! [X0] :
( ~ defined(X0)
| less_or_equal(s,X0)
| less_or_equal(X0,s) ),
inference(resolution,[status(thm)],[f73,f83]) ).
fof(f240,plain,
! [X0] :
( ~ defined(X0)
| less_or_equal(k,X0)
| less_or_equal(X0,k) ),
inference(resolution,[status(thm)],[f73,f82]) ).
fof(f241,plain,
! [X0] :
( ~ defined(X0)
| less_or_equal(d,X0)
| less_or_equal(X0,d) ),
inference(resolution,[status(thm)],[f73,f81]) ).
fof(f242,plain,
! [X0] :
( ~ defined(X0)
| less_or_equal(multiplicative_identity,X0)
| less_or_equal(X0,multiplicative_identity) ),
inference(resolution,[status(thm)],[f73,f63]) ).
fof(f243,plain,
! [X0] :
( ~ defined(X0)
| less_or_equal(c,X0)
| less_or_equal(X0,c) ),
inference(resolution,[status(thm)],[f73,f80]) ).
fof(f244,plain,
! [X0] :
( ~ defined(X0)
| less_or_equal(b,X0)
| less_or_equal(X0,b) ),
inference(resolution,[status(thm)],[f73,f79]) ).
fof(f245,plain,
! [X0] :
( ~ defined(X0)
| less_or_equal(a,X0)
| less_or_equal(X0,a) ),
inference(resolution,[status(thm)],[f73,f78]) ).
fof(f246,plain,
! [X0] :
( ~ defined(X0)
| less_or_equal(additive_identity,X0)
| less_or_equal(X0,additive_identity) ),
inference(resolution,[status(thm)],[f73,f59]) ).
fof(f248,plain,
( less_or_equal(s,s)
| less_or_equal(s,s) ),
inference(resolution,[status(thm)],[f239,f83]) ).
fof(f263,definition,
( sQ29_spl
<=> less_or_equal(s,s) ),
introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition]) ).
fof(f266,plain,
sQ29_spl,
inference(split_clause,[status(thm)],[f248,f263]) ).
fof(f318,plain,
( less_or_equal(k,k)
| less_or_equal(k,k) ),
inference(resolution,[status(thm)],[f240,f82]) ).
fof(f333,definition,
( sQ46_spl
<=> less_or_equal(k,k) ),
introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition]) ).
fof(f336,plain,
sQ46_spl,
inference(split_clause,[status(thm)],[f318,f333]) ).
fof(f382,plain,
( less_or_equal(d,d)
| less_or_equal(d,d) ),
inference(resolution,[status(thm)],[f241,f81]) ).
fof(f397,definition,
( sQ61_spl
<=> less_or_equal(d,d) ),
introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition]) ).
fof(f400,plain,
sQ61_spl,
inference(split_clause,[status(thm)],[f382,f397]) ).
fof(f441,plain,
( less_or_equal(c,c)
| less_or_equal(c,c) ),
inference(resolution,[status(thm)],[f243,f80]) ).
fof(f462,definition,
( sQ76_spl
<=> less_or_equal(c,c) ),
introduced(definition,[new_symbols(definition,[sQ76_spl])],[split_symbol_definition]) ).
fof(f465,plain,
sQ76_spl,
inference(split_clause,[status(thm)],[f441,f462]) ).
fof(f493,plain,
( less_or_equal(b,b)
| less_or_equal(b,b) ),
inference(resolution,[status(thm)],[f244,f79]) ).
fof(f514,definition,
( sQ87_spl
<=> less_or_equal(b,b) ),
introduced(definition,[new_symbols(definition,[sQ87_spl])],[split_symbol_definition]) ).
fof(f517,plain,
sQ87_spl,
inference(split_clause,[status(thm)],[f493,f514]) ).
fof(f539,plain,
( less_or_equal(a,a)
| less_or_equal(a,a) ),
inference(resolution,[status(thm)],[f245,f78]) ).
fof(f560,definition,
( sQ96_spl
<=> less_or_equal(a,a) ),
introduced(definition,[new_symbols(definition,[sQ96_spl])],[split_symbol_definition]) ).
fof(f563,plain,
sQ96_spl,
inference(split_clause,[status(thm)],[f539,f560]) ).
fof(f579,plain,
( less_or_equal(additive_identity,additive_identity)
| less_or_equal(additive_identity,additive_identity) ),
inference(resolution,[status(thm)],[f246,f59]) ).
fof(f600,definition,
( sQ103_spl
<=> less_or_equal(additive_identity,additive_identity) ),
introduced(definition,[new_symbols(definition,[sQ103_spl])],[split_symbol_definition]) ).
fof(f603,plain,
sQ103_spl,
inference(split_clause,[status(thm)],[f579,f600]) ).
fof(f604,plain,
( less_or_equal(additive_inverse(s),additive_inverse(s))
| less_or_equal(additive_inverse(s),additive_inverse(s)) ),
inference(resolution,[status(thm)],[f238,f90]) ).
fof(f613,definition,
( sQ104_spl
<=> less_or_equal(additive_inverse(s),additive_inverse(s)) ),
introduced(definition,[new_symbols(definition,[sQ104_spl])],[split_symbol_definition]) ).
fof(f616,plain,
sQ104_spl,
inference(split_clause,[status(thm)],[f604,f613]) ).
fof(f635,plain,
( less_or_equal(multiplicative_identity,multiplicative_identity)
| less_or_equal(multiplicative_identity,multiplicative_identity) ),
inference(resolution,[status(thm)],[f242,f63]) ).
fof(f644,definition,
( sQ107_spl
<=> less_or_equal(multiplicative_identity,multiplicative_identity) ),
introduced(definition,[new_symbols(definition,[sQ107_spl])],[split_symbol_definition]) ).
fof(f647,plain,
sQ107_spl,
inference(split_clause,[status(thm)],[f635,f644]) ).
fof(f661,plain,
! [X0] :
( ~ defined(X0)
| less_or_equal(additive_inverse(k),X0)
| less_or_equal(X0,additive_inverse(k)) ),
inference(resolution,[status(thm)],[f91,f73]) ).
fof(f666,plain,
defined(additive_inverse(additive_inverse(k))),
inference(resolution,[status(thm)],[f91,f60]) ).
fof(f741,plain,
( less_or_equal(additive_inverse(k),additive_inverse(k))
| less_or_equal(additive_inverse(k),additive_inverse(k)) ),
inference(resolution,[status(thm)],[f661,f91]) ).
fof(f751,definition,
( sQ129_spl
<=> less_or_equal(additive_inverse(k),additive_inverse(k)) ),
introduced(definition,[new_symbols(definition,[sQ129_spl])],[split_symbol_definition]) ).
fof(f754,plain,
sQ129_spl,
inference(split_clause,[status(thm)],[f741,f751]) ).
fof(f774,plain,
! [X0] :
( ~ defined(X0)
| less_or_equal(additive_inverse(d),X0)
| less_or_equal(X0,additive_inverse(d)) ),
inference(resolution,[status(thm)],[f92,f73]) ).
fof(f779,plain,
defined(additive_inverse(additive_inverse(d))),
inference(resolution,[status(thm)],[f92,f60]) ).
fof(f861,plain,
( less_or_equal(additive_inverse(d),additive_inverse(d))
| less_or_equal(additive_inverse(d),additive_inverse(d)) ),
inference(resolution,[status(thm)],[f774,f92]) ).
fof(f872,definition,
( sQ153_spl
<=> less_or_equal(additive_inverse(d),additive_inverse(d)) ),
introduced(definition,[new_symbols(definition,[sQ153_spl])],[split_symbol_definition]) ).
fof(f875,plain,
sQ153_spl,
inference(split_clause,[status(thm)],[f861,f872]) ).
fof(f897,plain,
! [X0] :
( ~ defined(X0)
| less_or_equal(additive_inverse(c),X0)
| less_or_equal(X0,additive_inverse(c)) ),
inference(resolution,[status(thm)],[f94,f73]) ).
fof(f902,plain,
defined(additive_inverse(additive_inverse(c))),
inference(resolution,[status(thm)],[f94,f60]) ).
fof(f991,plain,
( less_or_equal(additive_inverse(c),additive_inverse(c))
| less_or_equal(additive_inverse(c),additive_inverse(c)) ),
inference(resolution,[status(thm)],[f897,f94]) ).
fof(f1003,definition,
( sQ179_spl
<=> less_or_equal(additive_inverse(c),additive_inverse(c)) ),
introduced(definition,[new_symbols(definition,[sQ179_spl])],[split_symbol_definition]) ).
fof(f1006,plain,
sQ179_spl,
inference(split_clause,[status(thm)],[f991,f1003]) ).
fof(f1030,plain,
! [X0] :
( ~ defined(X0)
| less_or_equal(additive_inverse(b),X0)
| less_or_equal(X0,additive_inverse(b)) ),
inference(resolution,[status(thm)],[f95,f73]) ).
fof(f1035,plain,
defined(additive_inverse(additive_inverse(b))),
inference(resolution,[status(thm)],[f95,f60]) ).
fof(f1131,plain,
( less_or_equal(additive_inverse(b),additive_inverse(b))
| less_or_equal(additive_inverse(b),additive_inverse(b)) ),
inference(resolution,[status(thm)],[f1030,f95]) ).
fof(f1144,definition,
( sQ207_spl
<=> less_or_equal(additive_inverse(b),additive_inverse(b)) ),
introduced(definition,[new_symbols(definition,[sQ207_spl])],[split_symbol_definition]) ).
fof(f1147,plain,
sQ207_spl,
inference(split_clause,[status(thm)],[f1131,f1144]) ).
fof(f1173,plain,
! [X0] :
( ~ defined(X0)
| less_or_equal(additive_inverse(a),X0)
| less_or_equal(X0,additive_inverse(a)) ),
inference(resolution,[status(thm)],[f96,f73]) ).
fof(f1281,plain,
( less_or_equal(additive_inverse(a),additive_inverse(a))
| less_or_equal(additive_inverse(a),additive_inverse(a)) ),
inference(resolution,[status(thm)],[f1173,f96]) ).
fof(f1295,definition,
( sQ237_spl
<=> less_or_equal(additive_inverse(a),additive_inverse(a)) ),
introduced(definition,[new_symbols(definition,[sQ237_spl])],[split_symbol_definition]) ).
fof(f1298,plain,
sQ237_spl,
inference(split_clause,[status(thm)],[f1281,f1295]) ).
fof(f1326,plain,
! [X0] :
( ~ defined(X0)
| less_or_equal(additive_inverse(additive_identity),X0)
| less_or_equal(X0,additive_inverse(additive_identity)) ),
inference(resolution,[status(thm)],[f97,f73]) ).
fof(f1441,plain,
( less_or_equal(additive_inverse(additive_identity),additive_inverse(additive_identity))
| less_or_equal(additive_inverse(additive_identity),additive_inverse(additive_identity)) ),
inference(resolution,[status(thm)],[f1326,f97]) ).
fof(f1456,definition,
( sQ269_spl
<=> less_or_equal(additive_inverse(additive_identity),additive_inverse(additive_identity)) ),
introduced(definition,[new_symbols(definition,[sQ269_spl])],[split_symbol_definition]) ).
fof(f1459,plain,
sQ269_spl,
inference(split_clause,[status(thm)],[f1441,f1456]) ).
fof(f1647,plain,
! [X0,X1,X2] :
( ~ product(X2,c,X1)
| ~ product(X0,b,X2)
| product(X0,k,X1) ),
inference(resolution,[status(thm)],[f47,f88]) ).
fof(f1654,plain,
! [X0,X1,X2] :
( ~ product(X2,multiplicative_inverse(b),X1)
| ~ product(X0,X2,a)
| product(X0,X1,s) ),
inference(resolution,[status(thm)],[f47,f86]) ).
fof(f1852,plain,
product(d,a,k),
inference(resolution,[status(thm)],[f52,f87]) ).
fof(f1869,plain,
! [X0,X1,X2] :
( ~ product(X2,a,X1)
| ~ product(X0,d,X2)
| product(X0,k,X1) ),
inference(resolution,[status(thm)],[f1852,f47]) ).
fof(f1895,plain,
! [X0] :
( ~ defined(X0)
| less_or_equal(additive_inverse(multiplicative_identity),X0)
| less_or_equal(X0,additive_inverse(multiplicative_identity)) ),
inference(resolution,[status(thm)],[f93,f73]) ).
fof(f2045,plain,
product(multiplicative_identity,c,c),
inference(resolution,[status(thm)],[f50,f80]) ).
fof(f2047,plain,
product(multiplicative_identity,a,a),
inference(resolution,[status(thm)],[f50,f78]) ).
fof(f2087,plain,
( less_or_equal(additive_inverse(multiplicative_identity),additive_inverse(multiplicative_identity))
| less_or_equal(additive_inverse(multiplicative_identity),additive_inverse(multiplicative_identity)) ),
inference(resolution,[status(thm)],[f1895,f93]) ).
fof(f2105,definition,
( sQ377_spl
<=> less_or_equal(additive_inverse(multiplicative_identity),additive_inverse(multiplicative_identity)) ),
introduced(definition,[new_symbols(definition,[sQ377_spl])],[split_symbol_definition]) ).
fof(f2108,plain,
sQ377_spl,
inference(split_clause,[status(thm)],[f2087,f2105]) ).
fof(f2243,plain,
! [X0] :
( ~ defined(X0)
| less_or_equal(additive_inverse(additive_inverse(s)),X0)
| less_or_equal(X0,additive_inverse(additive_inverse(s))) ),
inference(resolution,[status(thm)],[f98,f73]) ).
fof(f2388,plain,
( less_or_equal(additive_inverse(additive_inverse(s)),additive_inverse(additive_inverse(s)))
| less_or_equal(additive_inverse(additive_inverse(s)),additive_inverse(additive_inverse(s))) ),
inference(resolution,[status(thm)],[f2243,f98]) ).
fof(f2407,definition,
( sQ417_spl
<=> less_or_equal(additive_inverse(additive_inverse(s)),additive_inverse(additive_inverse(s))) ),
introduced(definition,[new_symbols(definition,[sQ417_spl])],[split_symbol_definition]) ).
fof(f2410,plain,
sQ417_spl,
inference(split_clause,[status(thm)],[f2388,f2407]) ).
fof(f2494,plain,
! [X0] :
( ~ defined(X0)
| less_or_equal(additive_inverse(additive_inverse(k)),X0)
| less_or_equal(X0,additive_inverse(additive_inverse(k))) ),
inference(resolution,[status(thm)],[f666,f73]) ).
fof(f2646,plain,
( less_or_equal(additive_inverse(additive_inverse(k)),additive_inverse(additive_inverse(k)))
| less_or_equal(additive_inverse(additive_inverse(k)),additive_inverse(additive_inverse(k))) ),
inference(resolution,[status(thm)],[f2494,f666]) ).
fof(f2666,definition,
( sQ459_spl
<=> less_or_equal(additive_inverse(additive_inverse(k)),additive_inverse(additive_inverse(k))) ),
introduced(definition,[new_symbols(definition,[sQ459_spl])],[split_symbol_definition]) ).
fof(f2669,plain,
sQ459_spl,
inference(split_clause,[status(thm)],[f2646,f2666]) ).
fof(f2756,plain,
! [X0] :
( ~ sQ24_spl
| ~ product(multiplicative_identity,c,X0)
| product(multiplicative_inverse(b),k,X0) ),
inference(resolution,[status(thm)],[f223,f1647]) ).
fof(f2764,plain,
! [X0] :
( ~ sQ21_spl
| ~ product(multiplicative_identity,a,X0)
| product(multiplicative_inverse(d),k,X0) ),
inference(resolution,[status(thm)],[f211,f1869]) ).
fof(f2798,plain,
! [X0] :
( ~ defined(X0)
| less_or_equal(additive_inverse(additive_inverse(d)),X0)
| less_or_equal(X0,additive_inverse(additive_inverse(d))) ),
inference(resolution,[status(thm)],[f779,f73]) ).
fof(f3183,definition,
( sQ530_spl
<=> sum(additive_identity,additive_identity,multiplicative_identity) ),
introduced(definition,[new_symbols(definition,[sQ530_spl])],[split_symbol_definition]) ).
fof(f3184,plain,
( ~ sQ530_spl
| sum(additive_identity,additive_identity,multiplicative_identity) ),
inference(component_clause,[status(thm)],[f3183]) ).
fof(f3282,plain,
( ~ sQ530_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3184,f77]) ).
fof(f3283,plain,
~ sQ530_spl,
inference(contradiction_clause,[status(thm)],[f3282]) ).
fof(f3286,plain,
( less_or_equal(additive_inverse(additive_inverse(d)),additive_inverse(additive_inverse(d)))
| less_or_equal(additive_inverse(additive_inverse(d)),additive_inverse(additive_inverse(d))) ),
inference(resolution,[status(thm)],[f2798,f779]) ).
fof(f3307,definition,
( sQ553_spl
<=> less_or_equal(additive_inverse(additive_inverse(d)),additive_inverse(additive_inverse(d))) ),
introduced(definition,[new_symbols(definition,[sQ553_spl])],[split_symbol_definition]) ).
fof(f3310,plain,
sQ553_spl,
inference(split_clause,[status(thm)],[f3286,f3307]) ).
fof(f3386,plain,
! [X0] :
( ~ defined(X0)
| less_or_equal(additive_inverse(additive_inverse(c)),X0)
| less_or_equal(X0,additive_inverse(additive_inverse(c))) ),
inference(resolution,[status(thm)],[f902,f73]) ).
fof(f3552,plain,
( less_or_equal(additive_inverse(additive_inverse(c)),additive_inverse(additive_inverse(c)))
| less_or_equal(additive_inverse(additive_inverse(c)),additive_inverse(additive_inverse(c))) ),
inference(resolution,[status(thm)],[f3386,f902]) ).
fof(f3574,definition,
( sQ602_spl
<=> less_or_equal(additive_inverse(additive_inverse(c)),additive_inverse(additive_inverse(c))) ),
introduced(definition,[new_symbols(definition,[sQ602_spl])],[split_symbol_definition]) ).
fof(f3577,plain,
sQ602_spl,
inference(split_clause,[status(thm)],[f3552,f3574]) ).
fof(f3633,plain,
( ~ sQ24_spl
| product(multiplicative_inverse(b),k,c) ),
inference(resolution,[status(thm)],[f2045,f2756]) ).
fof(f3649,plain,
( ~ sQ24_spl
| product(k,multiplicative_inverse(b),c) ),
inference(resolution,[status(thm)],[f3633,f52]) ).
fof(f3660,plain,
! [X0] :
( ~ sQ24_spl
| ~ product(X0,k,a)
| product(X0,c,s) ),
inference(resolution,[status(thm)],[f3649,f1654]) ).
fof(f3763,plain,
! [X0] :
( ~ defined(X0)
| less_or_equal(additive_inverse(additive_inverse(b)),X0)
| less_or_equal(X0,additive_inverse(additive_inverse(b))) ),
inference(resolution,[status(thm)],[f1035,f73]) ).
fof(f3960,plain,
( ~ sQ21_spl
| product(multiplicative_inverse(d),k,a) ),
inference(resolution,[status(thm)],[f2047,f2764]) ).
fof(f4142,plain,
( less_or_equal(additive_inverse(additive_inverse(b)),additive_inverse(additive_inverse(b)))
| less_or_equal(additive_inverse(additive_inverse(b)),additive_inverse(additive_inverse(b))) ),
inference(resolution,[status(thm)],[f3763,f1035]) ).
fof(f4165,definition,
( sQ666_spl
<=> less_or_equal(additive_inverse(additive_inverse(b)),additive_inverse(additive_inverse(b))) ),
introduced(definition,[new_symbols(definition,[sQ666_spl])],[split_symbol_definition]) ).
fof(f4168,plain,
sQ666_spl,
inference(split_clause,[status(thm)],[f4142,f4165]) ).
fof(f4190,plain,
( ~ sQ24_spl
| ~ sQ21_spl
| product(multiplicative_inverse(d),c,s) ),
inference(resolution,[status(thm)],[f3960,f3660]) ).
fof(f4205,plain,
( ~ sQ24_spl
| ~ sQ21_spl
| product(c,multiplicative_inverse(d),s) ),
inference(resolution,[status(thm)],[f4190,f52]) ).
fof(f4213,plain,
( ~ sQ24_spl
| ~ sQ21_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4205,f89]) ).
fof(f4214,plain,
( ~ sQ24_spl
| ~ sQ21_spl ),
inference(contradiction_clause,[status(thm)],[f4213]) ).
fof(f4215,plain,
$false,
inference(sat_refutation,[status(thm)],[f213,f225,f235,f237,f266,f336,f400,f465,f517,f563,f603,f616,f647,f754,f875,f1006,f1147,f1298,f1459,f2108,f2410,f2669,f3283,f3310,f3577,f4168,f4214]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : FLD050-4 : TPTP v9.3.1. Bugfixed v2.1.0.
% 0.00/0.07 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.19/5.50 % Computer : n004.cluster.edu
% 0.19/5.50 % Model : x86_64 x86_64
% 0.19/5.50 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/5.50 % Memory : 8046.5625MB
% 0.19/5.50 % OS : Linux 6.8.0-71-generic
% 0.19/5.50 % CPULimit : 300
% 0.19/5.50 % WCLimit : 300
% 0.19/5.50 % DateTime : Mon Sep 21 15:41:26 UTC 2026
% 0.19/5.51 % CPUTime :
% 0.19/5.52 % Drodi V4.1.1
% 0.24/6.09 % Refutation found
% 0.24/6.09 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.24/6.09 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.24/6.13 % Elapsed time: 0.602829 seconds
% 0.24/6.13 % CPU time: 4.314676 seconds
% 0.24/6.13 % Total memory used: 42.132 MB
% 0.24/6.13 % Net memory used: 38.768 MB
%------------------------------------------------------------------------------