%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : FLD055-1 : TPTP v9.3.1. Bugfixed v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -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:26 PM UTC 2026
% Result : Unsatisfiable 0.14s 0.41s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : FLD055-1 : TPTP v9.3.1. Bugfixed v2.1.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.36 % Computer : n004.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Mon Sep 21 15:42:39 UTC 2026
% 0.08/0.37 % CPUTime :
% 0.08/0.38 % Drodi V4.1.1
% 0.14/0.41 % Refutation found
% 0.14/0.41 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.14/0.41 % SZS output start CNFRefutation for theBenchmark
% 0.14/0.41 fof(f11,axiom,(
% 0.14/0.41 defined(additive_identity) ),
% 0.14/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.41 fof(f14,axiom,(
% 0.14/0.41 defined(multiplicative_identity) ),
% 0.14/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.41 fof(f16,axiom,(
% 0.14/0.41 (![X,Y]: (( equalish(X,Y)| ~ less_or_equal(X,Y)| ~ less_or_equal(Y,X) ) ))),
% 0.14/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.41 fof(f17,axiom,(
% 0.14/0.41 (![X,Z,Y]: (( less_or_equal(X,Z)| ~ less_or_equal(X,Y)| ~ less_or_equal(Y,Z) ) ))),
% 0.14/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.41 fof(f18,axiom,(
% 0.14/0.41 (![X,Y]: (( less_or_equal(X,Y)| less_or_equal(Y,X)| ~ defined(X)| ~ defined(Y) ) ))),
% 0.14/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.41 fof(f22,axiom,(
% 0.14/0.41 (![X,Y]: (( equalish(X,Y)| ~ equalish(Y,X) ) ))),
% 0.14/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.41 fof(f26,axiom,(
% 0.14/0.41 (![Y,Z,X]: (( less_or_equal(Y,Z)| ~ less_or_equal(X,Z)| ~ equalish(X,Y) ) ))),
% 0.14/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.41 fof(f28,hypothesis,(
% 0.14/0.41 defined(a) ),
% 0.14/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.41 fof(f29,hypothesis,(
% 0.14/0.41 defined(b) ),
% 0.14/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.41 fof(f30,hypothesis,(
% 0.14/0.41 defined(c) ),
% 0.14/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.41 fof(f31,negated_conjecture,(
% 0.14/0.41 less_or_equal(a,b) ),
% 0.14/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.41 fof(f32,negated_conjecture,(
% 0.14/0.41 equalish(b,c) ),
% 0.14/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.41 fof(f33,negated_conjecture,(
% 0.14/0.41 ~ less_or_equal(a,c) ),
% 0.14/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.14/0.41 fof(f50,plain,(
% 0.14/0.41 defined(additive_identity)),
% 0.14/0.41 inference(cnf_transformation,[status(thm)],[f11])).
% 0.14/0.41 fof(f54,plain,(
% 0.14/0.41 defined(multiplicative_identity)),
% 0.14/0.41 inference(cnf_transformation,[status(thm)],[f14])).
% 0.14/0.41 fof(f56,plain,(
% 0.14/0.41 ![X0,X1]: (equalish(X0,X1)|~less_or_equal(X0,X1)|~less_or_equal(X1,X0))),
% 0.14/0.41 inference(cnf_transformation,[status(thm)],[f16])).
% 0.14/0.41 fof(f57,plain,(
% 0.14/0.41 ![Z,Y]: ((![X]: (less_or_equal(X,Z)|~less_or_equal(X,Y)))|~less_or_equal(Y,Z))),
% 0.14/0.41 inference(miniscoping,[status(thm)],[f17])).
% 0.14/0.41 fof(f58,plain,(
% 0.14/0.41 ![X0,X1,X2]: (less_or_equal(X0,X1)|~less_or_equal(X0,X2)|~less_or_equal(X2,X1))),
% 0.14/0.41 inference(cnf_transformation,[status(thm)],[f57])).
% 0.14/0.41 fof(f59,plain,(
% 0.14/0.41 ![Y]: ((![X]: ((less_or_equal(X,Y)|less_or_equal(Y,X))|~defined(X)))|~defined(Y))),
% 0.14/0.41 inference(miniscoping,[status(thm)],[f18])).
% 0.14/0.41 fof(f60,plain,(
% 0.14/0.41 ![X0,X1]: (less_or_equal(X0,X1)|less_or_equal(X1,X0)|~defined(X0)|~defined(X1))),
% 0.14/0.41 inference(cnf_transformation,[status(thm)],[f59])).
% 0.14/0.41 fof(f66,plain,(
% 0.14/0.41 ![X0,X1]: (equalish(X0,X1)|~equalish(X1,X0))),
% 0.14/0.41 inference(cnf_transformation,[status(thm)],[f22])).
% 0.14/0.41 fof(f73,plain,(
% 0.14/0.41 ![Y,X]: ((![Z]: (less_or_equal(Y,Z)|~less_or_equal(X,Z)))|~equalish(X,Y))),
% 0.14/0.41 inference(miniscoping,[status(thm)],[f26])).
% 0.14/0.41 fof(f74,plain,(
% 0.14/0.41 ![X0,X1,X2]: (less_or_equal(X0,X1)|~less_or_equal(X2,X1)|~equalish(X2,X0))),
% 0.14/0.41 inference(cnf_transformation,[status(thm)],[f73])).
% 0.14/0.41 fof(f76,plain,(
% 0.14/0.41 defined(a)),
% 0.14/0.41 inference(cnf_transformation,[status(thm)],[f28])).
% 0.14/0.41 fof(f77,plain,(
% 0.14/0.41 defined(b)),
% 0.14/0.41 inference(cnf_transformation,[status(thm)],[f29])).
% 0.14/0.41 fof(f78,plain,(
% 0.14/0.41 defined(c)),
% 0.14/0.41 inference(cnf_transformation,[status(thm)],[f30])).
% 0.14/0.41 fof(f79,plain,(
% 0.14/0.41 less_or_equal(a,b)),
% 0.14/0.41 inference(cnf_transformation,[status(thm)],[f31])).
% 0.14/0.41 fof(f80,plain,(
% 0.14/0.41 equalish(b,c)),
% 0.14/0.41 inference(cnf_transformation,[status(thm)],[f32])).
% 0.14/0.41 fof(f81,plain,(
% 0.14/0.41 ~less_or_equal(a,c)),
% 0.14/0.41 inference(cnf_transformation,[status(thm)],[f33])).
% 0.14/0.41 fof(f82,plain,(
% 0.14/0.41 equalish(b,a)|~less_or_equal(b,a)),
% 0.14/0.41 inference(resolution,[status(thm)],[f56,f79])).
% 0.14/0.41 fof(f83,definition,(
% 0.14/0.41 sQ0_spl <=> (equalish(b,a))),
% 0.14/0.41 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.14/0.41 fof(f84,plain,(
% 0.14/0.41 equalish(b,a)|~sQ0_spl),
% 0.14/0.41 inference(component_clause,[status(thm)],[f83])).
% 0.14/0.41 fof(f86,definition,(
% 0.14/0.41 sQ1_spl <=> (less_or_equal(b,a))),
% 0.14/0.41 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.14/0.41 fof(f88,plain,(
% 0.14/0.41 ~less_or_equal(b,a)|sQ1_spl),
% 0.14/0.41 inference(component_clause,[status(thm)],[f86])).
% 0.14/0.41 fof(f89,plain,(
% 0.14/0.41 sQ0_spl|~sQ1_spl),
% 0.14/0.41 inference(split_clause,[status(thm)],[f82,f83,f86])).
% 0.14/0.41 fof(f90,plain,(
% 0.14/0.41 ![X0]: (less_or_equal(X0,b)|~less_or_equal(X0,a))),
% 0.14/0.41 inference(resolution,[status(thm)],[f58,f79])).
% 0.14/0.41 fof(f91,plain,(
% 0.14/0.41 ![X0]: (less_or_equal(X0,c)|less_or_equal(c,X0)|~defined(X0))),
% 0.14/0.41 inference(resolution,[status(thm)],[f60,f78])).
% 0.14/0.41 fof(f92,plain,(
% 0.14/0.41 ![X0]: (less_or_equal(X0,b)|less_or_equal(b,X0)|~defined(X0))),
% 0.14/0.41 inference(resolution,[status(thm)],[f60,f77])).
% 0.14/0.41 fof(f93,plain,(
% 0.14/0.41 ![X0]: (less_or_equal(X0,a)|less_or_equal(a,X0)|~defined(X0))),
% 0.14/0.41 inference(resolution,[status(thm)],[f60,f76])).
% 0.14/0.41 fof(f94,plain,(
% 0.14/0.41 ![X0]: (less_or_equal(X0,additive_identity)|less_or_equal(additive_identity,X0)|~defined(X0))),
% 0.14/0.41 inference(resolution,[status(thm)],[f50,f60])).
% 0.14/0.41 fof(f95,plain,(
% 0.14/0.41 ![X0]: (less_or_equal(X0,multiplicative_identity)|less_or_equal(multiplicative_identity,X0)|~defined(X0))),
% 0.14/0.41 inference(resolution,[status(thm)],[f54,f60])).
% 0.14/0.41 fof(f118,definition,(
% 0.14/0.41 sQ5_spl <=> (defined(additive_identity))),
% 0.14/0.41 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.14/0.41 fof(f120,plain,(
% 0.14/0.41 ~defined(additive_identity)|sQ5_spl),
% 0.14/0.41 inference(component_clause,[status(thm)],[f118])).
% 0.14/0.41 fof(f152,plain,(
% 0.14/0.41 less_or_equal(c,c)|less_or_equal(c,c)),
% 0.14/0.41 inference(resolution,[status(thm)],[f91,f78])).
% 0.14/0.41 fof(f154,plain,(
% 0.14/0.41 less_or_equal(a,c)|less_or_equal(c,a)),
% 0.14/0.41 inference(resolution,[status(thm)],[f91,f76])).
% 0.14/0.41 fof(f169,definition,(
% 0.14/0.41 sQ12_spl <=> (less_or_equal(c,c))),
% 0.14/0.41 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 0.14/0.41 fof(f170,plain,(
% 0.14/0.41 less_or_equal(c,c)|~sQ12_spl),
% 0.14/0.41 inference(component_clause,[status(thm)],[f169])).
% 0.14/0.41 fof(f172,plain,(
% 0.14/0.41 sQ12_spl),
% 0.14/0.41 inference(split_clause,[status(thm)],[f152,f169])).
% 0.14/0.41 fof(f173,definition,(
% 0.14/0.41 sQ13_spl <=> (less_or_equal(b,c))),
% 0.14/0.41 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 0.14/0.41 fof(f174,plain,(
% 0.14/0.41 less_or_equal(b,c)|~sQ13_spl),
% 0.14/0.41 inference(component_clause,[status(thm)],[f173])).
% 0.14/0.41 fof(f175,plain,(
% 0.14/0.41 ~less_or_equal(b,c)|sQ13_spl),
% 0.14/0.41 inference(component_clause,[status(thm)],[f173])).
% 0.14/0.41 fof(f176,definition,(
% 0.14/0.41 sQ14_spl <=> (less_or_equal(c,b))),
% 0.14/0.41 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 0.14/0.41 fof(f178,plain,(
% 0.14/0.41 ~less_or_equal(c,b)|sQ14_spl),
% 0.14/0.41 inference(component_clause,[status(thm)],[f176])).
% 0.14/0.41 fof(f180,definition,(
% 0.14/0.41 sQ15_spl <=> (less_or_equal(a,c))),
% 0.14/0.41 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 0.14/0.41 fof(f181,plain,(
% 0.14/0.41 less_or_equal(a,c)|~sQ15_spl),
% 0.14/0.41 inference(component_clause,[status(thm)],[f180])).
% 0.14/0.41 fof(f183,definition,(
% 0.14/0.41 sQ16_spl <=> (less_or_equal(c,a))),
% 0.14/0.41 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 0.14/0.41 fof(f184,plain,(
% 0.14/0.41 less_or_equal(c,a)|~sQ16_spl),
% 0.14/0.41 inference(component_clause,[status(thm)],[f183])).
% 0.14/0.41 fof(f186,plain,(
% 0.14/0.41 sQ15_spl|sQ16_spl),
% 0.14/0.41 inference(split_clause,[status(thm)],[f154,f180,f183])).
% 0.14/0.41 fof(f187,plain,(
% 0.14/0.41 $false|~sQ15_spl),
% 0.14/0.41 inference(forward_subsumption_resolution,[status(thm)],[f181,f81])).
% 0.14/0.41 fof(f188,plain,(
% 0.14/0.41 ~sQ15_spl),
% 0.14/0.41 inference(contradiction_clause,[status(thm)],[f187])).
% 0.14/0.41 fof(f194,plain,(
% 0.14/0.41 less_or_equal(b,b)|less_or_equal(b,b)),
% 0.14/0.41 inference(resolution,[status(thm)],[f92,f77])).
% 0.14/0.41 fof(f211,definition,(
% 0.14/0.41 sQ21_spl <=> (less_or_equal(b,b))),
% 0.14/0.41 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 0.14/0.41 fof(f214,plain,(
% 0.14/0.41 sQ21_spl),
% 0.14/0.41 inference(split_clause,[status(thm)],[f194,f211])).
% 0.14/0.41 fof(f219,plain,(
% 0.14/0.41 ![X0]: (less_or_equal(X0,c)|~equalish(c,X0)|~sQ12_spl)),
% 0.14/0.41 inference(resolution,[status(thm)],[f170,f74])).
% 0.14/0.41 fof(f226,plain,(
% 0.14/0.41 ![X0]: (less_or_equal(X0,c)|~equalish(b,X0)|~sQ13_spl)),
% 0.14/0.41 inference(resolution,[status(thm)],[f174,f74])).
% 0.14/0.41 fof(f228,plain,(
% 0.14/0.41 equalish(c,b)|~less_or_equal(c,b)|~sQ13_spl),
% 0.14/0.41 inference(resolution,[status(thm)],[f174,f56])).
% 0.14/0.41 fof(f229,definition,(
% 0.14/0.41 sQ24_spl <=> (equalish(c,b))),
% 0.14/0.41 introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition])).
% 0.14/0.41 fof(f230,plain,(
% 0.14/0.41 equalish(c,b)|~sQ24_spl),
% 0.14/0.41 inference(component_clause,[status(thm)],[f229])).
% 0.14/0.41 fof(f232,plain,(
% 0.14/0.41 sQ24_spl|~sQ14_spl|~sQ13_spl),
% 0.14/0.41 inference(split_clause,[status(thm)],[f228,f229,f176,f173])).
% 0.14/0.41 fof(f247,plain,(
% 0.14/0.41 less_or_equal(c,b)|~sQ16_spl),
% 0.14/0.41 inference(resolution,[status(thm)],[f184,f90])).
% 0.14/0.41 fof(f248,plain,(
% 0.14/0.41 ![X0]: (less_or_equal(X0,a)|~equalish(c,X0)|~sQ16_spl)),
% 0.14/0.41 inference(resolution,[status(thm)],[f184,f74])).
% 0.14/0.41 fof(f306,plain,(
% 0.14/0.41 less_or_equal(a,a)|less_or_equal(a,a)),
% 0.14/0.41 inference(resolution,[status(thm)],[f93,f76])).
% 0.14/0.41 fof(f323,definition,(
% 0.14/0.41 sQ36_spl <=> (less_or_equal(a,a))),
% 0.14/0.41 introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition])).
% 0.14/0.41 fof(f326,plain,(
% 0.14/0.41 sQ36_spl),
% 0.14/0.41 inference(split_clause,[status(thm)],[f306,f323])).
% 0.14/0.41 fof(f330,plain,(
% 0.14/0.41 less_or_equal(additive_identity,additive_identity)|less_or_equal(additive_identity,additive_identity)),
% 0.14/0.41 inference(resolution,[status(thm)],[f94,f50])).
% 0.14/0.41 fof(f341,definition,(
% 0.14/0.41 sQ39_spl <=> (less_or_equal(additive_identity,additive_identity))),
% 0.14/0.41 introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition])).
% 0.14/0.41 fof(f344,plain,(
% 0.14/0.41 sQ39_spl),
% 0.14/0.41 inference(split_clause,[status(thm)],[f330,f341])).
% 0.14/0.41 fof(f413,plain,(
% 0.14/0.41 $false|sQ5_spl),
% 0.14/0.41 inference(forward_subsumption_resolution,[status(thm)],[f120,f50])).
% 0.14/0.41 fof(f414,plain,(
% 0.14/0.41 sQ5_spl),
% 0.14/0.41 inference(contradiction_clause,[status(thm)],[f413])).
% 0.14/0.41 fof(f427,plain,(
% 0.14/0.41 less_or_equal(multiplicative_identity,multiplicative_identity)|less_or_equal(multiplicative_identity,multiplicative_identity)),
% 0.14/0.41 inference(resolution,[status(thm)],[f95,f54])).
% 0.14/0.41 fof(f432,definition,(
% 0.14/0.41 sQ45_spl <=> (less_or_equal(multiplicative_identity,multiplicative_identity))),
% 0.14/0.41 introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition])).
% 0.14/0.41 fof(f435,plain,(
% 0.14/0.41 sQ45_spl),
% 0.14/0.41 inference(split_clause,[status(thm)],[f427,f432])).
% 0.14/0.41 fof(f613,plain,(
% 0.14/0.41 ~equalish(b,a)|~sQ13_spl),
% 0.14/0.41 inference(resolution,[status(thm)],[f226,f81])).
% 0.14/0.41 fof(f618,plain,(
% 0.14/0.41 $false|~sQ0_spl|~sQ13_spl),
% 0.14/0.41 inference(forward_subsumption_resolution,[status(thm)],[f613,f84])).
% 0.14/0.41 fof(f619,plain,(
% 0.14/0.41 ~sQ0_spl|~sQ13_spl),
% 0.14/0.41 inference(contradiction_clause,[status(thm)],[f618])).
% 0.14/0.41 fof(f620,plain,(
% 0.14/0.41 ~equalish(c,b)|sQ13_spl|~sQ12_spl),
% 0.14/0.41 inference(resolution,[status(thm)],[f175,f219])).
% 0.14/0.41 fof(f622,plain,(
% 0.14/0.41 ~equalish(b,c)|sQ13_spl|~sQ12_spl),
% 0.14/0.41 inference(resolution,[status(thm)],[f620,f66])).
% 0.14/0.41 fof(f623,plain,(
% 0.14/0.41 $false|sQ13_spl|~sQ12_spl),
% 0.14/0.41 inference(forward_subsumption_resolution,[status(thm)],[f622,f80])).
% 0.14/0.41 fof(f624,plain,(
% 0.14/0.41 sQ13_spl|~sQ12_spl),
% 0.14/0.41 inference(contradiction_clause,[status(thm)],[f623])).
% 0.14/0.41 fof(f650,plain,(
% 0.14/0.41 ~equalish(c,b)|~sQ16_spl|sQ1_spl),
% 0.14/0.41 inference(resolution,[status(thm)],[f248,f88])).
% 0.14/0.41 fof(f656,plain,(
% 0.14/0.41 $false|~sQ24_spl|~sQ16_spl|sQ1_spl),
% 0.14/0.41 inference(forward_subsumption_resolution,[status(thm)],[f650,f230])).
% 0.14/0.41 fof(f657,plain,(
% 0.14/0.41 ~sQ24_spl|~sQ16_spl|sQ1_spl),
% 0.14/0.41 inference(contradiction_clause,[status(thm)],[f656])).
% 0.14/0.41 fof(f658,plain,(
% 0.14/0.41 $false|~sQ16_spl|sQ14_spl),
% 0.14/0.41 inference(forward_subsumption_resolution,[status(thm)],[f178,f247])).
% 0.14/0.41 fof(f659,plain,(
% 0.14/0.41 ~sQ16_spl|sQ14_spl),
% 0.14/0.41 inference(contradiction_clause,[status(thm)],[f658])).
% 0.14/0.41 fof(f660,plain,(
% 0.14/0.41 $false),
% 0.14/0.41 inference(sat_refutation,[status(thm)],[f89,f172,f186,f188,f214,f232,f326,f344,f414,f435,f619,f624,f657,f659])).
% 0.14/0.41 % SZS output end CNFRefutation for theBenchmark.p
% 0.14/0.48 % Elapsed time: 0.106852 seconds
% 0.14/0.48 % CPU time: 0.143723 seconds
% 0.14/0.48 % Total memory used: 5.126 MB
% 0.14/0.48 % Net memory used: 5.030 MB
%------------------------------------------------------------------------------