%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : FLD049-4 : 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 : n014.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:25 PM UTC 2026
% Result : Unsatisfiable 0.37s 0.54s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : FLD049-4 : TPTP v9.3.1. Bugfixed v2.1.0.
% 0.00/0.06 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.17/0.42 % Computer : n014.cluster.edu
% 0.17/0.42 % Model : x86_64 x86_64
% 0.17/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.42 % Memory : 8046.5625MB
% 0.17/0.42 % OS : Linux 6.8.0-71-generic
% 0.17/0.42 % CPULimit : 300
% 0.17/0.42 % WCLimit : 300
% 0.17/0.42 % DateTime : Mon Sep 21 15:41:34 UTC 2026
% 0.17/0.43 % CPUTime :
% 0.17/0.43 % Drodi V4.1.1
% 0.37/0.54 % Refutation found
% 0.37/0.54 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.37/0.54 % SZS output start CNFRefutation for theBenchmark
% 0.37/0.54 fof(f7,axiom,(
% 0.37/0.54 (![U,Z,W,X,Y,V]: (( product(U,Z,W)| ~ product(X,Y,U)| ~ product(Y,Z,V)| ~ product(X,V,W) ) ))),
% 0.37/0.54 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.37/0.54 fof(f8,axiom,(
% 0.37/0.54 (![X]: (( product(multiplicative_identity,X,X)| ~ defined(X) ) ))),
% 0.37/0.54 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.37/0.54 fof(f9,axiom,(
% 0.37/0.54 (![X]: (( product(multiplicative_inverse(X),X,multiplicative_identity)| sum(additive_identity,X,additive_identity)| ~ defined(X) ) ))),
% 0.37/0.54 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.37/0.54 fof(f10,axiom,(
% 0.37/0.54 (![Y,X,Z]: (( product(Y,X,Z)| ~ product(X,Y,Z) ) ))),
% 0.37/0.54 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.37/0.54 fof(f14,axiom,(
% 0.37/0.54 defined(additive_identity) ),
% 0.37/0.54 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.37/0.54 fof(f15,axiom,(
% 0.37/0.54 (![X]: (( defined(additive_inverse(X))| ~ defined(X) ) ))),
% 0.37/0.54 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.37/0.54 fof(f17,axiom,(
% 0.37/0.54 defined(multiplicative_identity) ),
% 0.37/0.54 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.37/0.54 fof(f23,axiom,(
% 0.37/0.54 (![X,Y]: (( less_or_equal(X,Y)| less_or_equal(Y,X)| ~ defined(X)| ~ defined(Y) ) ))),
% 0.37/0.54 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.37/0.54 fof(f27,hypothesis,(
% 0.37/0.54 defined(a) ),
% 0.37/0.54 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.37/0.54 fof(f28,hypothesis,(
% 0.37/0.54 defined(b) ),
% 0.37/0.54 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.37/0.54 fof(f29,hypothesis,(
% 0.37/0.54 defined(c) ),
% 0.37/0.54 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.37/0.54 fof(f30,hypothesis,(
% 0.37/0.54 defined(d) ),
% 0.37/0.54 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.37/0.54 fof(f31,hypothesis,(
% 0.37/0.54 defined(k) ),
% 0.37/0.54 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.37/0.54 fof(f32,hypothesis,(
% 0.37/0.54 defined(s) ),
% 0.37/0.54 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.37/0.54 fof(f33,negated_conjecture,(
% 0.37/0.54 ~ sum(additive_identity,b,additive_identity) ),
% 0.37/0.54 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.37/0.54 fof(f34,negated_conjecture,(
% 0.37/0.54 ~ sum(additive_identity,d,additive_identity) ),
% 0.37/0.54 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.37/0.54 fof(f35,negated_conjecture,(
% 0.37/0.54 product(a,multiplicative_inverse(b),s) ),
% 0.37/0.54 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.37/0.54 fof(f36,negated_conjecture,(
% 0.37/0.54 product(c,multiplicative_inverse(d),s) ),
% 0.37/0.54 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.37/0.54 fof(f37,negated_conjecture,(
% 0.37/0.54 product(a,d,k) ),
% 0.37/0.54 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.37/0.54 fof(f38,negated_conjecture,(
% 0.37/0.54 ~ product(b,c,k) ),
% 0.37/0.54 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.37/0.54 fof(f48,plain,(
% 0.37/0.54 ![W,X,V]: ((![Z,Y]: ((![U]: (product(U,Z,W)|~product(X,Y,U)))|~product(Y,Z,V)))|~product(X,V,W))),
% 0.37/0.54 inference(miniscoping,[status(thm)],[f7])).
% 0.37/0.54 fof(f49,plain,(
% 0.37/0.54 ![X0,X1,X2,X3,X4,X5]: (product(X0,X1,X2)|~product(X3,X4,X0)|~product(X4,X1,X5)|~product(X3,X5,X2))),
% 0.37/0.54 inference(cnf_transformation,[status(thm)],[f48])).
% 0.37/0.54 fof(f50,plain,(
% 0.37/0.54 ![X0]: (product(multiplicative_identity,X0,X0)|~defined(X0))),
% 0.37/0.54 inference(cnf_transformation,[status(thm)],[f8])).
% 0.37/0.54 fof(f51,plain,(
% 0.37/0.54 ![X0]: (product(multiplicative_inverse(X0),X0,multiplicative_identity)|sum(additive_identity,X0,additive_identity)|~defined(X0))),
% 0.37/0.54 inference(cnf_transformation,[status(thm)],[f9])).
% 0.37/0.54 fof(f52,plain,(
% 0.37/0.54 ![X0,X1,X2]: (product(X0,X1,X2)|~product(X1,X0,X2))),
% 0.37/0.54 inference(cnf_transformation,[status(thm)],[f10])).
% 0.37/0.54 fof(f59,plain,(
% 0.37/0.54 defined(additive_identity)),
% 0.37/0.54 inference(cnf_transformation,[status(thm)],[f14])).
% 0.37/0.54 fof(f60,plain,(
% 0.37/0.54 ![X0]: (defined(additive_inverse(X0))|~defined(X0))),
% 0.37/0.54 inference(cnf_transformation,[status(thm)],[f15])).
% 0.37/0.54 fof(f63,plain,(
% 0.37/0.54 defined(multiplicative_identity)),
% 0.37/0.54 inference(cnf_transformation,[status(thm)],[f17])).
% 0.37/0.54 fof(f72,plain,(
% 0.37/0.54 ![Y]: ((![X]: ((less_or_equal(X,Y)|less_or_equal(Y,X))|~defined(X)))|~defined(Y))),
% 0.37/0.54 inference(miniscoping,[status(thm)],[f23])).
% 0.37/0.54 fof(f73,plain,(
% 0.37/0.54 ![X0,X1]: (less_or_equal(X0,X1)|less_or_equal(X1,X0)|~defined(X0)|~defined(X1))),
% 0.37/0.55 inference(cnf_transformation,[status(thm)],[f72])).
% 0.37/0.55 fof(f78,plain,(
% 0.37/0.55 defined(a)),
% 0.37/0.55 inference(cnf_transformation,[status(thm)],[f27])).
% 0.37/0.55 fof(f79,plain,(
% 0.37/0.55 defined(b)),
% 0.37/0.55 inference(cnf_transformation,[status(thm)],[f28])).
% 0.37/0.55 fof(f80,plain,(
% 0.37/0.55 defined(c)),
% 0.37/0.55 inference(cnf_transformation,[status(thm)],[f29])).
% 0.37/0.55 fof(f81,plain,(
% 0.37/0.55 defined(d)),
% 0.37/0.55 inference(cnf_transformation,[status(thm)],[f30])).
% 0.37/0.55 fof(f82,plain,(
% 0.37/0.55 defined(k)),
% 0.37/0.55 inference(cnf_transformation,[status(thm)],[f31])).
% 0.37/0.55 fof(f83,plain,(
% 0.37/0.55 defined(s)),
% 0.37/0.55 inference(cnf_transformation,[status(thm)],[f32])).
% 0.37/0.55 fof(f84,plain,(
% 0.37/0.55 ~sum(additive_identity,b,additive_identity)),
% 0.37/0.55 inference(cnf_transformation,[status(thm)],[f33])).
% 0.37/0.55 fof(f85,plain,(
% 0.37/0.55 ~sum(additive_identity,d,additive_identity)),
% 0.37/0.55 inference(cnf_transformation,[status(thm)],[f34])).
% 0.37/0.55 fof(f86,plain,(
% 0.37/0.55 product(a,multiplicative_inverse(b),s)),
% 0.37/0.55 inference(cnf_transformation,[status(thm)],[f35])).
% 0.37/0.55 fof(f87,plain,(
% 0.37/0.55 product(c,multiplicative_inverse(d),s)),
% 0.37/0.55 inference(cnf_transformation,[status(thm)],[f36])).
% 0.37/0.55 fof(f88,plain,(
% 0.37/0.55 product(a,d,k)),
% 0.37/0.55 inference(cnf_transformation,[status(thm)],[f37])).
% 0.37/0.55 fof(f89,plain,(
% 0.37/0.55 ~product(b,c,k)),
% 0.37/0.55 inference(cnf_transformation,[status(thm)],[f38])).
% 0.37/0.55 fof(f102,plain,(
% 0.37/0.55 product(multiplicative_identity,c,c)),
% 0.37/0.55 inference(resolution,[status(thm)],[f50,f80])).
% 0.37/0.55 fof(f105,plain,(
% 0.37/0.55 product(multiplicative_identity,a,a)),
% 0.37/0.55 inference(resolution,[status(thm)],[f50,f78])).
% 0.37/0.55 fof(f123,definition,(
% 0.37/0.55 sQ3_spl <=> (sum(additive_identity,b,additive_identity))),
% 0.37/0.55 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.37/0.55 fof(f124,plain,(
% 0.37/0.55 sum(additive_identity,b,additive_identity)|~sQ3_spl),
% 0.37/0.55 inference(component_clause,[status(thm)],[f123])).
% 0.37/0.55 fof(f149,plain,(
% 0.37/0.55 product(multiplicative_inverse(b),b,multiplicative_identity)|sum(additive_identity,b,additive_identity)),
% 0.37/0.55 inference(resolution,[status(thm)],[f51,f79])).
% 0.37/0.55 fof(f157,definition,(
% 0.37/0.55 sQ11_spl <=> (product(multiplicative_inverse(b),b,multiplicative_identity))),
% 0.37/0.55 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 0.37/0.55 fof(f158,plain,(
% 0.37/0.55 product(multiplicative_inverse(b),b,multiplicative_identity)|~sQ11_spl),
% 0.37/0.55 inference(component_clause,[status(thm)],[f157])).
% 0.37/0.55 fof(f160,plain,(
% 0.37/0.55 sQ11_spl|sQ3_spl),
% 0.37/0.55 inference(split_clause,[status(thm)],[f149,f157,f123])).
% 0.37/0.55 fof(f173,plain,(
% 0.37/0.55 $false|~sQ3_spl),
% 0.37/0.55 inference(forward_subsumption_resolution,[status(thm)],[f124,f84])).
% 0.37/0.55 fof(f174,plain,(
% 0.37/0.55 ~sQ3_spl),
% 0.37/0.55 inference(contradiction_clause,[status(thm)],[f173])).
% 0.37/0.55 fof(f306,plain,(
% 0.37/0.55 ![X0,X1,X2]: (product(s,X0,X1)|~product(multiplicative_inverse(d),X0,X2)|~product(c,X2,X1))),
% 0.37/0.55 inference(resolution,[status(thm)],[f87,f49])).
% 0.37/0.55 fof(f308,plain,(
% 0.37/0.55 product(d,a,k)),
% 0.37/0.55 inference(resolution,[status(thm)],[f88,f52])).
% 0.37/0.55 fof(f312,plain,(
% 0.37/0.55 ![X0,X1,X2]: (product(k,X0,X1)|~product(a,X0,X2)|~product(d,X2,X1))),
% 0.37/0.55 inference(resolution,[status(thm)],[f308,f49])).
% 0.37/0.55 fof(f324,plain,(
% 0.37/0.55 ![X0]: (product(k,multiplicative_inverse(b),X0)|~product(d,s,X0))),
% 0.37/0.55 inference(resolution,[status(thm)],[f312,f86])).
% 0.37/0.55 fof(f341,plain,(
% 0.37/0.55 ![X0]: (less_or_equal(d,X0)|less_or_equal(X0,d)|~defined(X0))),
% 0.37/0.55 inference(resolution,[status(thm)],[f81,f73])).
% 0.37/0.55 fof(f342,plain,(
% 0.37/0.55 product(multiplicative_inverse(d),d,multiplicative_identity)|sum(additive_identity,d,additive_identity)),
% 0.37/0.55 inference(resolution,[status(thm)],[f81,f51])).
% 0.37/0.55 fof(f382,definition,(
% 0.37/0.55 sQ50_spl <=> (product(multiplicative_inverse(d),d,multiplicative_identity))),
% 0.37/0.55 introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition])).
% 0.37/0.55 fof(f383,plain,(
% 0.37/0.55 product(multiplicative_inverse(d),d,multiplicative_identity)|~sQ50_spl),
% 0.37/0.55 inference(component_clause,[status(thm)],[f382])).
% 0.37/0.55 fof(f385,definition,(
% 0.37/0.55 sQ51_spl <=> (sum(additive_identity,d,additive_identity))),
% 0.37/0.55 introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition])).
% 0.37/0.55 fof(f386,plain,(
% 0.37/0.55 sum(additive_identity,d,additive_identity)|~sQ51_spl),
% 0.37/0.55 inference(component_clause,[status(thm)],[f385])).
% 0.37/0.55 fof(f388,plain,(
% 0.37/0.55 sQ50_spl|sQ51_spl),
% 0.37/0.55 inference(split_clause,[status(thm)],[f342,f382,f385])).
% 0.37/0.55 fof(f393,plain,(
% 0.37/0.55 $false|~sQ51_spl),
% 0.37/0.55 inference(forward_subsumption_resolution,[status(thm)],[f386,f85])).
% 0.37/0.55 fof(f394,plain,(
% 0.37/0.55 ~sQ51_spl),
% 0.37/0.55 inference(contradiction_clause,[status(thm)],[f393])).
% 0.37/0.55 fof(f395,plain,(
% 0.37/0.55 less_or_equal(d,d)|less_or_equal(d,d)),
% 0.37/0.55 inference(resolution,[status(thm)],[f341,f81])).
% 0.37/0.55 fof(f401,definition,(
% 0.37/0.55 sQ53_spl <=> (less_or_equal(d,d))),
% 0.37/0.55 introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition])).
% 0.37/0.55 fof(f404,plain,(
% 0.37/0.55 sQ53_spl),
% 0.37/0.55 inference(split_clause,[status(thm)],[f395,f401])).
% 0.37/0.55 fof(f416,plain,(
% 0.37/0.55 ![X0]: (less_or_equal(k,X0)|less_or_equal(X0,k)|~defined(X0))),
% 0.37/0.55 inference(resolution,[status(thm)],[f82,f73])).
% 0.37/0.55 fof(f475,plain,(
% 0.37/0.55 less_or_equal(k,k)|less_or_equal(k,k)),
% 0.37/0.55 inference(resolution,[status(thm)],[f416,f82])).
% 0.37/0.55 fof(f482,definition,(
% 0.37/0.55 sQ69_spl <=> (less_or_equal(k,k))),
% 0.37/0.55 introduced(definition,[new_symbols(definition,[sQ69_spl])],[split_symbol_definition])).
% 0.37/0.55 fof(f485,plain,(
% 0.37/0.55 sQ69_spl),
% 0.37/0.55 inference(split_clause,[status(thm)],[f475,f482])).
% 0.37/0.55 fof(f499,plain,(
% 0.37/0.55 ![X0]: (less_or_equal(s,X0)|less_or_equal(X0,s)|~defined(X0))),
% 0.37/0.55 inference(resolution,[status(thm)],[f83,f73])).
% 0.37/0.55 fof(f565,plain,(
% 0.37/0.55 less_or_equal(s,s)|less_or_equal(s,s)),
% 0.37/0.55 inference(resolution,[status(thm)],[f499,f83])).
% 0.37/0.55 fof(f573,definition,(
% 0.37/0.55 sQ87_spl <=> (less_or_equal(s,s))),
% 0.37/0.55 introduced(definition,[new_symbols(definition,[sQ87_spl])],[split_symbol_definition])).
% 0.37/0.55 fof(f576,plain,(
% 0.37/0.55 sQ87_spl),
% 0.37/0.55 inference(split_clause,[status(thm)],[f565,f573])).
% 0.37/0.55 fof(f731,plain,(
% 0.37/0.55 product(c,multiplicative_identity,c)),
% 0.37/0.55 inference(resolution,[status(thm)],[f102,f52])).
% 0.37/0.55 fof(f737,plain,(
% 0.37/0.55 product(a,multiplicative_identity,a)),
% 0.37/0.55 inference(resolution,[status(thm)],[f105,f52])).
% 0.37/0.55 fof(f777,plain,(
% 0.37/0.55 ![X0]: (product(s,d,X0)|~product(c,multiplicative_identity,X0)|~sQ50_spl)),
% 0.37/0.55 inference(resolution,[status(thm)],[f383,f306])).
% 0.37/0.55 fof(f900,plain,(
% 0.37/0.55 defined(additive_inverse(s))),
% 0.37/0.55 inference(resolution,[status(thm)],[f60,f83])).
% 0.37/0.55 fof(f901,plain,(
% 0.37/0.55 defined(additive_inverse(k))),
% 0.37/0.55 inference(resolution,[status(thm)],[f60,f82])).
% 0.37/0.55 fof(f902,plain,(
% 0.37/0.55 defined(additive_inverse(d))),
% 0.37/0.55 inference(resolution,[status(thm)],[f60,f81])).
% 0.37/0.55 fof(f903,plain,(
% 0.37/0.55 defined(additive_inverse(c))),
% 0.37/0.55 inference(resolution,[status(thm)],[f60,f80])).
% 0.37/0.55 fof(f904,plain,(
% 0.37/0.55 defined(additive_inverse(b))),
% 0.37/0.55 inference(resolution,[status(thm)],[f60,f79])).
% 0.37/0.55 fof(f905,plain,(
% 0.37/0.55 defined(additive_inverse(multiplicative_identity))),
% 0.37/0.55 inference(resolution,[status(thm)],[f60,f63])).
% 0.37/0.55 fof(f906,plain,(
% 0.37/0.55 defined(additive_inverse(a))),
% 0.37/0.55 inference(resolution,[status(thm)],[f60,f78])).
% 0.37/0.55 fof(f907,plain,(
% 0.37/0.55 defined(additive_inverse(additive_identity))),
% 0.37/0.55 inference(resolution,[status(thm)],[f60,f59])).
% 0.37/0.55 fof(f1184,plain,(
% 0.37/0.55 ![X0]: (less_or_equal(additive_inverse(s),X0)|less_or_equal(X0,additive_inverse(s))|~defined(X0))),
% 0.37/0.55 inference(resolution,[status(thm)],[f900,f73])).
% 0.37/0.55 fof(f1271,plain,(
% 0.37/0.55 less_or_equal(additive_inverse(s),additive_inverse(s))|less_or_equal(additive_inverse(s),additive_inverse(s))),
% 0.37/0.55 inference(resolution,[status(thm)],[f1184,f900])).
% 0.37/0.55 fof(f1282,definition,(
% 0.37/0.55 sQ174_spl <=> (less_or_equal(additive_inverse(s),additive_inverse(s)))),
% 0.37/0.55 introduced(definition,[new_symbols(definition,[sQ174_spl])],[split_symbol_definition])).
% 0.37/0.55 fof(f1285,plain,(
% 0.37/0.55 sQ174_spl),
% 0.37/0.55 inference(split_clause,[status(thm)],[f1271,f1282])).
% 0.37/0.55 fof(f1319,plain,(
% 0.37/0.55 ![X0]: (less_or_equal(additive_inverse(k),X0)|less_or_equal(X0,additive_inverse(k))|~defined(X0))),
% 0.37/0.55 inference(resolution,[status(thm)],[f901,f73])).
% 0.37/0.55 fof(f1413,plain,(
% 0.37/0.55 less_or_equal(additive_inverse(k),additive_inverse(k))|less_or_equal(additive_inverse(k),additive_inverse(k))),
% 0.37/0.55 inference(resolution,[status(thm)],[f1319,f901])).
% 0.37/0.55 fof(f1425,definition,(
% 0.37/0.55 sQ200_spl <=> (less_or_equal(additive_inverse(k),additive_inverse(k)))),
% 0.37/0.55 introduced(definition,[new_symbols(definition,[sQ200_spl])],[split_symbol_definition])).
% 0.37/0.55 fof(f1428,plain,(
% 0.37/0.55 sQ200_spl),
% 0.37/0.55 inference(split_clause,[status(thm)],[f1413,f1425])).
% 0.37/0.55 fof(f1464,plain,(
% 0.37/0.55 ![X0]: (less_or_equal(additive_inverse(d),X0)|less_or_equal(X0,additive_inverse(d))|~defined(X0))),
% 0.37/0.55 inference(resolution,[status(thm)],[f902,f73])).
% 0.37/0.55 fof(f1565,plain,(
% 0.37/0.55 less_or_equal(additive_inverse(d),additive_inverse(d))|less_or_equal(additive_inverse(d),additive_inverse(d))),
% 0.37/0.55 inference(resolution,[status(thm)],[f1464,f902])).
% 0.37/0.55 fof(f1578,definition,(
% 0.37/0.55 sQ228_spl <=> (less_or_equal(additive_inverse(d),additive_inverse(d)))),
% 0.37/0.55 introduced(definition,[new_symbols(definition,[sQ228_spl])],[split_symbol_definition])).
% 0.37/0.55 fof(f1581,plain,(
% 0.37/0.55 sQ228_spl),
% 0.37/0.55 inference(split_clause,[status(thm)],[f1565,f1578])).
% 0.37/0.55 fof(f1619,plain,(
% 0.37/0.55 ![X0]: (less_or_equal(additive_inverse(c),X0)|less_or_equal(X0,additive_inverse(c))|~defined(X0))),
% 0.37/0.55 inference(resolution,[status(thm)],[f903,f73])).
% 0.37/0.55 fof(f1727,plain,(
% 0.37/0.55 less_or_equal(additive_inverse(c),additive_inverse(c))|less_or_equal(additive_inverse(c),additive_inverse(c))),
% 0.37/0.55 inference(resolution,[status(thm)],[f1619,f903])).
% 0.37/0.55 fof(f1741,definition,(
% 0.37/0.55 sQ258_spl <=> (less_or_equal(additive_inverse(c),additive_inverse(c)))),
% 0.37/0.55 introduced(definition,[new_symbols(definition,[sQ258_spl])],[split_symbol_definition])).
% 0.37/0.55 fof(f1744,plain,(
% 0.37/0.55 sQ258_spl),
% 0.37/0.55 inference(split_clause,[status(thm)],[f1727,f1741])).
% 0.37/0.55 fof(f1784,plain,(
% 0.37/0.55 ![X0]: (less_or_equal(additive_inverse(b),X0)|less_or_equal(X0,additive_inverse(b))|~defined(X0))),
% 0.37/0.55 inference(resolution,[status(thm)],[f904,f73])).
% 0.37/0.55 fof(f1899,plain,(
% 0.37/0.55 less_or_equal(additive_inverse(b),additive_inverse(b))|less_or_equal(additive_inverse(b),additive_inverse(b))),
% 0.37/0.55 inference(resolution,[status(thm)],[f1784,f904])).
% 0.37/0.55 fof(f1914,definition,(
% 0.37/0.55 sQ290_spl <=> (less_or_equal(additive_inverse(b),additive_inverse(b)))),
% 0.37/0.55 introduced(definition,[new_symbols(definition,[sQ290_spl])],[split_symbol_definition])).
% 0.37/0.55 fof(f1917,plain,(
% 0.37/0.55 sQ290_spl),
% 0.37/0.55 inference(split_clause,[status(thm)],[f1899,f1914])).
% 0.37/0.55 fof(f1959,plain,(
% 0.37/0.55 ![X0]: (less_or_equal(additive_inverse(a),X0)|less_or_equal(X0,additive_inverse(a))|~defined(X0))),
% 0.37/0.55 inference(resolution,[status(thm)],[f906,f73])).
% 0.37/0.55 fof(f2081,plain,(
% 0.37/0.55 less_or_equal(additive_inverse(a),additive_inverse(a))|less_or_equal(additive_inverse(a),additive_inverse(a))),
% 0.37/0.55 inference(resolution,[status(thm)],[f1959,f906])).
% 0.37/0.55 fof(f2097,definition,(
% 0.37/0.55 sQ324_spl <=> (less_or_equal(additive_inverse(a),additive_inverse(a)))),
% 0.37/0.55 introduced(definition,[new_symbols(definition,[sQ324_spl])],[split_symbol_definition])).
% 0.37/0.55 fof(f2100,plain,(
% 0.37/0.55 sQ324_spl),
% 0.37/0.55 inference(split_clause,[status(thm)],[f2081,f2097])).
% 0.37/0.55 fof(f2144,plain,(
% 0.37/0.55 ![X0]: (less_or_equal(additive_inverse(additive_identity),X0)|less_or_equal(X0,additive_inverse(additive_identity))|~defined(X0))),
% 0.37/0.55 inference(resolution,[status(thm)],[f907,f73])).
% 0.37/0.55 fof(f2273,plain,(
% 0.37/0.55 less_or_equal(additive_inverse(additive_identity),additive_inverse(additive_identity))|less_or_equal(additive_inverse(additive_identity),additive_inverse(additive_identity))),
% 0.37/0.55 inference(resolution,[status(thm)],[f2144,f907])).
% 0.37/0.55 fof(f2290,definition,(
% 0.37/0.55 sQ360_spl <=> (less_or_equal(additive_inverse(additive_identity),additive_inverse(additive_identity)))),
% 0.37/0.55 introduced(definition,[new_symbols(definition,[sQ360_spl])],[split_symbol_definition])).
% 0.37/0.55 fof(f2293,plain,(
% 0.37/0.55 sQ360_spl),
% 0.37/0.55 inference(split_clause,[status(thm)],[f2273,f2290])).
% 0.37/0.55 fof(f2830,plain,(
% 0.37/0.55 ![X0]: (less_or_equal(additive_inverse(multiplicative_identity),X0)|less_or_equal(X0,additive_inverse(multiplicative_identity))|~defined(X0))),
% 0.37/0.55 inference(resolution,[status(thm)],[f905,f73])).
% 0.37/0.55 fof(f3114,plain,(
% 0.37/0.55 less_or_equal(additive_inverse(multiplicative_identity),additive_inverse(multiplicative_identity))|less_or_equal(additive_inverse(multiplicative_identity),additive_inverse(multiplicative_identity))),
% 0.37/0.55 inference(resolution,[status(thm)],[f2830,f905])).
% 0.37/0.55 fof(f3132,definition,(
% 0.37/0.55 sQ417_spl <=> (less_or_equal(additive_inverse(multiplicative_identity),additive_inverse(multiplicative_identity)))),
% 0.37/0.55 introduced(definition,[new_symbols(definition,[sQ417_spl])],[split_symbol_definition])).
% 0.37/0.55 fof(f3135,plain,(
% 0.37/0.55 sQ417_spl),
% 0.37/0.55 inference(split_clause,[status(thm)],[f3114,f3132])).
% 0.37/0.55 fof(f3191,plain,(
% 0.37/0.55 product(s,d,c)|~sQ50_spl),
% 0.37/0.55 inference(resolution,[status(thm)],[f731,f777])).
% 0.37/0.55 fof(f3202,plain,(
% 0.37/0.55 product(d,s,c)|~sQ50_spl),
% 0.37/0.55 inference(resolution,[status(thm)],[f3191,f52])).
% 0.37/0.55 fof(f3206,plain,(
% 0.37/0.55 product(k,multiplicative_inverse(b),c)|~sQ50_spl),
% 0.37/0.55 inference(resolution,[status(thm)],[f3202,f324])).
% 0.37/0.55 fof(f3225,plain,(
% 0.37/0.55 ![X0,X1,X2]: (product(c,X0,X1)|~product(multiplicative_inverse(b),X0,X2)|~product(k,X2,X1)|~sQ50_spl)),
% 0.37/0.55 inference(resolution,[status(thm)],[f3206,f49])).
% 0.37/0.55 fof(f3266,plain,(
% 0.37/0.55 ![X0]: (product(c,b,X0)|~product(k,multiplicative_identity,X0)|~sQ50_spl|~sQ11_spl)),
% 0.37/0.55 inference(resolution,[status(thm)],[f3225,f158])).
% 0.37/0.55 fof(f3359,plain,(
% 0.37/0.55 ![X0]: (product(k,multiplicative_identity,X0)|~product(d,a,X0))),
% 0.37/0.55 inference(resolution,[status(thm)],[f737,f312])).
% 0.37/0.55 fof(f3482,plain,(
% 0.37/0.55 product(k,multiplicative_identity,k)),
% 0.37/0.55 inference(resolution,[status(thm)],[f3359,f308])).
% 0.37/0.55 fof(f3490,plain,(
% 0.37/0.55 product(c,b,k)|~sQ50_spl|~sQ11_spl),
% 0.37/0.55 inference(resolution,[status(thm)],[f3482,f3266])).
% 0.37/0.55 fof(f3509,plain,(
% 0.37/0.55 product(b,c,k)|~sQ50_spl|~sQ11_spl),
% 0.37/0.55 inference(resolution,[status(thm)],[f3490,f52])).
% 0.37/0.55 fof(f3513,plain,(
% 0.37/0.55 $false|~sQ50_spl|~sQ11_spl),
% 0.37/0.55 inference(forward_subsumption_resolution,[status(thm)],[f3509,f89])).
% 0.37/0.55 fof(f3514,plain,(
% 0.37/0.55 ~sQ50_spl|~sQ11_spl),
% 0.37/0.55 inference(contradiction_clause,[status(thm)],[f3513])).
% 0.37/0.55 fof(f3515,plain,(
% 0.37/0.55 $false),
% 0.37/0.55 inference(sat_refutation,[status(thm)],[f160,f174,f388,f394,f404,f485,f576,f1285,f1428,f1581,f1744,f1917,f2100,f2293,f3135,f3514])).
% 0.37/0.55 % SZS output end CNFRefutation for theBenchmark.p
% 0.37/0.58 % Elapsed time: 0.139269 seconds
% 0.37/0.58 % CPU time: 0.800947 seconds
% 0.37/0.58 % Total memory used: 26.740 MB
% 0.37/0.58 % Net memory used: 26.210 MB
%------------------------------------------------------------------------------