%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : FLD050-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 : n005.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.13s 0.51s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : FLD050-4 : TPTP v9.3.1. Bugfixed v2.1.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n005.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Mon Sep 21 15:41:20 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.13/0.36 % Drodi V4.1.1
% 0.13/0.51 % Refutation found
% 0.13/0.51 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.13/0.51 % SZS output start CNFRefutation for theBenchmark
% 0.13/0.51 fof(f6,axiom,(
% 0.13/0.51 (![X,V,W,Y,U,Z]: (( product(X,V,W)| ~ product(X,Y,U)| ~ product(Y,Z,V)| ~ product(U,Z,W) ) ))),
% 0.13/0.51 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.51 fof(f8,axiom,(
% 0.13/0.51 (![X]: (( product(multiplicative_identity,X,X)| ~ defined(X) ) ))),
% 0.13/0.51 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.51 fof(f9,axiom,(
% 0.13/0.51 (![X]: (( product(multiplicative_inverse(X),X,multiplicative_identity)| sum(additive_identity,X,additive_identity)| ~ defined(X) ) ))),
% 0.13/0.51 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.51 fof(f10,axiom,(
% 0.13/0.51 (![Y,X,Z]: (( product(Y,X,Z)| ~ product(X,Y,Z) ) ))),
% 0.13/0.51 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.51 fof(f14,axiom,(
% 0.13/0.51 defined(additive_identity) ),
% 0.13/0.51 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.51 fof(f15,axiom,(
% 0.13/0.51 (![X]: (( defined(additive_inverse(X))| ~ defined(X) ) ))),
% 0.13/0.51 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.51 fof(f17,axiom,(
% 0.13/0.51 defined(multiplicative_identity) ),
% 0.13/0.51 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.51 fof(f23,axiom,(
% 0.13/0.51 (![X,Y]: (( less_or_equal(X,Y)| less_or_equal(Y,X)| ~ defined(X)| ~ defined(Y) ) ))),
% 0.13/0.51 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.51 fof(f26,axiom,(
% 0.13/0.51 ~ sum(additive_identity,additive_identity,multiplicative_identity) ),
% 0.13/0.51 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.51 fof(f27,hypothesis,(
% 0.13/0.51 defined(a) ),
% 0.13/0.51 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.51 fof(f28,hypothesis,(
% 0.13/0.51 defined(b) ),
% 0.13/0.51 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.51 fof(f29,hypothesis,(
% 0.13/0.51 defined(c) ),
% 0.13/0.51 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.51 fof(f30,hypothesis,(
% 0.13/0.51 defined(d) ),
% 0.13/0.51 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.51 fof(f31,hypothesis,(
% 0.13/0.51 defined(k) ),
% 0.13/0.51 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.51 fof(f32,hypothesis,(
% 0.13/0.51 defined(s) ),
% 0.13/0.51 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.51 fof(f33,negated_conjecture,(
% 0.13/0.51 ~ sum(additive_identity,b,additive_identity) ),
% 0.13/0.51 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.51 fof(f34,negated_conjecture,(
% 0.13/0.51 ~ sum(additive_identity,d,additive_identity) ),
% 0.13/0.51 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.51 fof(f35,negated_conjecture,(
% 0.13/0.51 product(a,multiplicative_inverse(b),s) ),
% 0.13/0.51 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.51 fof(f36,negated_conjecture,(
% 0.13/0.51 product(a,d,k) ),
% 0.13/0.51 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.51 fof(f37,negated_conjecture,(
% 0.13/0.51 product(b,c,k) ),
% 0.13/0.51 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.51 fof(f38,negated_conjecture,(
% 0.13/0.51 ~ product(c,multiplicative_inverse(d),s) ),
% 0.13/0.51 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.51 fof(f46,plain,(
% 0.13/0.51 ![W,U,Z]: ((![V,Y]: ((![X]: (product(X,V,W)|~product(X,Y,U)))|~product(Y,Z,V)))|~product(U,Z,W))),
% 0.13/0.51 inference(miniscoping,[status(thm)],[f6])).
% 0.13/0.51 fof(f47,plain,(
% 0.13/0.51 ![X0,X1,X2,X3,X4,X5]: (product(X0,X1,X2)|~product(X0,X3,X4)|~product(X3,X5,X1)|~product(X4,X5,X2))),
% 0.13/0.51 inference(cnf_transformation,[status(thm)],[f46])).
% 0.13/0.51 fof(f50,plain,(
% 0.13/0.51 ![X0]: (product(multiplicative_identity,X0,X0)|~defined(X0))),
% 0.13/0.51 inference(cnf_transformation,[status(thm)],[f8])).
% 0.13/0.51 fof(f51,plain,(
% 0.13/0.51 ![X0]: (product(multiplicative_inverse(X0),X0,multiplicative_identity)|sum(additive_identity,X0,additive_identity)|~defined(X0))),
% 0.13/0.51 inference(cnf_transformation,[status(thm)],[f9])).
% 0.13/0.51 fof(f52,plain,(
% 0.13/0.51 ![X0,X1,X2]: (product(X0,X1,X2)|~product(X1,X0,X2))),
% 0.13/0.51 inference(cnf_transformation,[status(thm)],[f10])).
% 0.13/0.51 fof(f59,plain,(
% 0.13/0.51 defined(additive_identity)),
% 0.13/0.51 inference(cnf_transformation,[status(thm)],[f14])).
% 0.13/0.51 fof(f60,plain,(
% 0.13/0.51 ![X0]: (defined(additive_inverse(X0))|~defined(X0))),
% 0.13/0.51 inference(cnf_transformation,[status(thm)],[f15])).
% 0.13/0.51 fof(f63,plain,(
% 0.13/0.51 defined(multiplicative_identity)),
% 0.13/0.51 inference(cnf_transformation,[status(thm)],[f17])).
% 0.13/0.51 fof(f72,plain,(
% 0.13/0.51 ![Y]: ((![X]: ((less_or_equal(X,Y)|less_or_equal(Y,X))|~defined(X)))|~defined(Y))),
% 0.13/0.51 inference(miniscoping,[status(thm)],[f23])).
% 0.13/0.51 fof(f73,plain,(
% 0.13/0.51 ![X0,X1]: (less_or_equal(X0,X1)|less_or_equal(X1,X0)|~defined(X0)|~defined(X1))),
% 0.13/0.51 inference(cnf_transformation,[status(thm)],[f72])).
% 0.13/0.51 fof(f77,plain,(
% 0.13/0.51 ~sum(additive_identity,additive_identity,multiplicative_identity)),
% 0.13/0.51 inference(cnf_transformation,[status(thm)],[f26])).
% 0.13/0.51 fof(f78,plain,(
% 0.13/0.51 defined(a)),
% 0.13/0.51 inference(cnf_transformation,[status(thm)],[f27])).
% 0.13/0.51 fof(f79,plain,(
% 0.13/0.51 defined(b)),
% 0.13/0.51 inference(cnf_transformation,[status(thm)],[f28])).
% 0.13/0.51 fof(f80,plain,(
% 0.13/0.51 defined(c)),
% 0.13/0.51 inference(cnf_transformation,[status(thm)],[f29])).
% 0.13/0.51 fof(f81,plain,(
% 0.13/0.51 defined(d)),
% 0.13/0.51 inference(cnf_transformation,[status(thm)],[f30])).
% 0.13/0.51 fof(f82,plain,(
% 0.13/0.51 defined(k)),
% 0.13/0.51 inference(cnf_transformation,[status(thm)],[f31])).
% 0.13/0.51 fof(f83,plain,(
% 0.13/0.51 defined(s)),
% 0.13/0.51 inference(cnf_transformation,[status(thm)],[f32])).
% 0.13/0.51 fof(f84,plain,(
% 0.13/0.51 ~sum(additive_identity,b,additive_identity)),
% 0.13/0.51 inference(cnf_transformation,[status(thm)],[f33])).
% 0.13/0.51 fof(f85,plain,(
% 0.13/0.51 ~sum(additive_identity,d,additive_identity)),
% 0.13/0.51 inference(cnf_transformation,[status(thm)],[f34])).
% 0.13/0.51 fof(f86,plain,(
% 0.13/0.51 product(a,multiplicative_inverse(b),s)),
% 0.13/0.51 inference(cnf_transformation,[status(thm)],[f35])).
% 0.13/0.51 fof(f87,plain,(
% 0.13/0.51 product(a,d,k)),
% 0.13/0.51 inference(cnf_transformation,[status(thm)],[f36])).
% 0.13/0.51 fof(f88,plain,(
% 0.13/0.51 product(b,c,k)),
% 0.13/0.51 inference(cnf_transformation,[status(thm)],[f37])).
% 0.13/0.51 fof(f89,plain,(
% 0.13/0.51 ~product(c,multiplicative_inverse(d),s)),
% 0.13/0.51 inference(cnf_transformation,[status(thm)],[f38])).
% 0.13/0.51 fof(f90,plain,(
% 0.13/0.51 defined(additive_inverse(s))),
% 0.13/0.51 inference(resolution,[status(thm)],[f60,f83])).
% 0.13/0.51 fof(f91,plain,(
% 0.13/0.51 defined(additive_inverse(k))),
% 0.13/0.51 inference(resolution,[status(thm)],[f60,f82])).
% 0.13/0.51 fof(f92,plain,(
% 0.13/0.51 defined(additive_inverse(d))),
% 0.13/0.51 inference(resolution,[status(thm)],[f60,f81])).
% 0.13/0.51 fof(f93,plain,(
% 0.13/0.51 defined(additive_inverse(multiplicative_identity))),
% 0.13/0.51 inference(resolution,[status(thm)],[f60,f63])).
% 0.13/0.51 fof(f94,plain,(
% 0.13/0.51 defined(additive_inverse(c))),
% 0.13/0.51 inference(resolution,[status(thm)],[f60,f80])).
% 0.13/0.51 fof(f95,plain,(
% 0.13/0.51 defined(additive_inverse(b))),
% 0.13/0.51 inference(resolution,[status(thm)],[f60,f79])).
% 0.13/0.51 fof(f96,plain,(
% 0.13/0.51 defined(additive_inverse(a))),
% 0.13/0.51 inference(resolution,[status(thm)],[f60,f78])).
% 0.13/0.51 fof(f97,plain,(
% 0.13/0.51 defined(additive_inverse(additive_identity))),
% 0.13/0.51 inference(resolution,[status(thm)],[f60,f59])).
% 0.13/0.51 fof(f98,plain,(
% 0.13/0.51 defined(additive_inverse(additive_inverse(s)))),
% 0.13/0.51 inference(resolution,[status(thm)],[f90,f60])).
% 0.13/0.51 fof(f150,definition,(
% 0.13/0.51 sQ7_spl <=> (sum(additive_identity,d,additive_identity))),
% 0.13/0.51 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.13/0.51 fof(f151,plain,(
% 0.13/0.51 sum(additive_identity,d,additive_identity)|~sQ7_spl),
% 0.13/0.51 inference(component_clause,[status(thm)],[f150])).
% 0.13/0.51 fof(f171,definition,(
% 0.13/0.51 sQ13_spl <=> (sum(additive_identity,b,additive_identity))),
% 0.13/0.51 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 0.13/0.51 fof(f172,plain,(
% 0.13/0.51 sum(additive_identity,b,additive_identity)|~sQ13_spl),
% 0.13/0.51 inference(component_clause,[status(thm)],[f171])).
% 0.13/0.51 fof(f192,plain,(
% 0.13/0.51 product(multiplicative_inverse(d),d,multiplicative_identity)|sum(additive_identity,d,additive_identity)),
% 0.13/0.51 inference(resolution,[status(thm)],[f51,f81])).
% 0.13/0.51 fof(f195,plain,(
% 0.13/0.51 product(multiplicative_inverse(b),b,multiplicative_identity)|sum(additive_identity,b,additive_identity)),
% 0.13/0.51 inference(resolution,[status(thm)],[f51,f79])).
% 0.13/0.51 fof(f210,definition,(
% 0.13/0.51 sQ21_spl <=> (product(multiplicative_inverse(d),d,multiplicative_identity))),
% 0.13/0.51 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 0.13/0.51 fof(f211,plain,(
% 0.13/0.51 product(multiplicative_inverse(d),d,multiplicative_identity)|~sQ21_spl),
% 0.13/0.51 inference(component_clause,[status(thm)],[f210])).
% 0.13/0.51 fof(f213,plain,(
% 0.13/0.51 sQ21_spl|sQ7_spl),
% 0.13/0.51 inference(split_clause,[status(thm)],[f192,f210,f150])).
% 0.13/0.51 fof(f222,definition,(
% 0.13/0.51 sQ24_spl <=> (product(multiplicative_inverse(b),b,multiplicative_identity))),
% 0.13/0.51 introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition])).
% 0.13/0.51 fof(f223,plain,(
% 0.13/0.51 product(multiplicative_inverse(b),b,multiplicative_identity)|~sQ24_spl),
% 0.13/0.51 inference(component_clause,[status(thm)],[f222])).
% 0.13/0.51 fof(f225,plain,(
% 0.13/0.51 sQ24_spl|sQ13_spl),
% 0.13/0.51 inference(split_clause,[status(thm)],[f195,f222,f171])).
% 0.13/0.51 fof(f234,plain,(
% 0.13/0.51 $false|~sQ13_spl),
% 0.13/0.51 inference(forward_subsumption_resolution,[status(thm)],[f172,f84])).
% 0.13/0.51 fof(f235,plain,(
% 0.13/0.51 ~sQ13_spl),
% 0.13/0.51 inference(contradiction_clause,[status(thm)],[f234])).
% 0.13/0.51 fof(f236,plain,(
% 0.13/0.51 $false|~sQ7_spl),
% 0.13/0.51 inference(forward_subsumption_resolution,[status(thm)],[f151,f85])).
% 0.13/0.51 fof(f237,plain,(
% 0.13/0.51 ~sQ7_spl),
% 0.13/0.51 inference(contradiction_clause,[status(thm)],[f236])).
% 0.13/0.51 fof(f238,plain,(
% 0.13/0.51 ![X0]: (less_or_equal(X0,additive_inverse(s))|less_or_equal(additive_inverse(s),X0)|~defined(X0))),
% 0.13/0.51 inference(resolution,[status(thm)],[f73,f90])).
% 0.13/0.51 fof(f239,plain,(
% 0.13/0.51 ![X0]: (less_or_equal(X0,s)|less_or_equal(s,X0)|~defined(X0))),
% 0.13/0.51 inference(resolution,[status(thm)],[f73,f83])).
% 0.13/0.51 fof(f240,plain,(
% 0.13/0.51 ![X0]: (less_or_equal(X0,k)|less_or_equal(k,X0)|~defined(X0))),
% 0.13/0.51 inference(resolution,[status(thm)],[f73,f82])).
% 0.13/0.51 fof(f241,plain,(
% 0.13/0.51 ![X0]: (less_or_equal(X0,d)|less_or_equal(d,X0)|~defined(X0))),
% 0.13/0.51 inference(resolution,[status(thm)],[f73,f81])).
% 0.13/0.51 fof(f242,plain,(
% 0.13/0.51 ![X0]: (less_or_equal(X0,multiplicative_identity)|less_or_equal(multiplicative_identity,X0)|~defined(X0))),
% 0.13/0.51 inference(resolution,[status(thm)],[f73,f63])).
% 0.13/0.51 fof(f243,plain,(
% 0.13/0.51 ![X0]: (less_or_equal(X0,c)|less_or_equal(c,X0)|~defined(X0))),
% 0.13/0.51 inference(resolution,[status(thm)],[f73,f80])).
% 0.13/0.51 fof(f244,plain,(
% 0.13/0.51 ![X0]: (less_or_equal(X0,b)|less_or_equal(b,X0)|~defined(X0))),
% 0.13/0.51 inference(resolution,[status(thm)],[f73,f79])).
% 0.13/0.51 fof(f245,plain,(
% 0.13/0.51 ![X0]: (less_or_equal(X0,a)|less_or_equal(a,X0)|~defined(X0))),
% 0.13/0.51 inference(resolution,[status(thm)],[f73,f78])).
% 0.13/0.51 fof(f246,plain,(
% 0.13/0.51 ![X0]: (less_or_equal(X0,additive_identity)|less_or_equal(additive_identity,X0)|~defined(X0))),
% 0.13/0.51 inference(resolution,[status(thm)],[f73,f59])).
% 0.13/0.51 fof(f248,plain,(
% 0.13/0.51 less_or_equal(s,s)|less_or_equal(s,s)),
% 0.13/0.51 inference(resolution,[status(thm)],[f239,f83])).
% 0.13/0.51 fof(f263,definition,(
% 0.13/0.51 sQ29_spl <=> (less_or_equal(s,s))),
% 0.13/0.51 introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition])).
% 0.13/0.51 fof(f266,plain,(
% 0.13/0.51 sQ29_spl),
% 0.13/0.51 inference(split_clause,[status(thm)],[f248,f263])).
% 0.13/0.51 fof(f318,plain,(
% 0.13/0.51 less_or_equal(k,k)|less_or_equal(k,k)),
% 0.13/0.51 inference(resolution,[status(thm)],[f240,f82])).
% 0.13/0.51 fof(f333,definition,(
% 0.13/0.51 sQ46_spl <=> (less_or_equal(k,k))),
% 0.13/0.51 introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition])).
% 0.13/0.51 fof(f336,plain,(
% 0.13/0.51 sQ46_spl),
% 0.13/0.51 inference(split_clause,[status(thm)],[f318,f333])).
% 0.13/0.51 fof(f382,plain,(
% 0.13/0.51 less_or_equal(d,d)|less_or_equal(d,d)),
% 0.13/0.51 inference(resolution,[status(thm)],[f241,f81])).
% 0.13/0.51 fof(f397,definition,(
% 0.13/0.51 sQ61_spl <=> (less_or_equal(d,d))),
% 0.13/0.51 introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition])).
% 0.13/0.51 fof(f400,plain,(
% 0.13/0.51 sQ61_spl),
% 0.13/0.51 inference(split_clause,[status(thm)],[f382,f397])).
% 0.13/0.51 fof(f441,plain,(
% 0.13/0.51 less_or_equal(c,c)|less_or_equal(c,c)),
% 0.13/0.51 inference(resolution,[status(thm)],[f243,f80])).
% 0.13/0.51 fof(f462,definition,(
% 0.13/0.51 sQ76_spl <=> (less_or_equal(c,c))),
% 0.13/0.51 introduced(definition,[new_symbols(definition,[sQ76_spl])],[split_symbol_definition])).
% 0.13/0.51 fof(f465,plain,(
% 0.13/0.51 sQ76_spl),
% 0.13/0.51 inference(split_clause,[status(thm)],[f441,f462])).
% 0.13/0.51 fof(f493,plain,(
% 0.13/0.51 less_or_equal(b,b)|less_or_equal(b,b)),
% 0.13/0.51 inference(resolution,[status(thm)],[f244,f79])).
% 0.13/0.51 fof(f514,definition,(
% 0.13/0.51 sQ87_spl <=> (less_or_equal(b,b))),
% 0.13/0.51 introduced(definition,[new_symbols(definition,[sQ87_spl])],[split_symbol_definition])).
% 0.13/0.51 fof(f517,plain,(
% 0.13/0.51 sQ87_spl),
% 0.13/0.51 inference(split_clause,[status(thm)],[f493,f514])).
% 0.13/0.51 fof(f539,plain,(
% 0.13/0.51 less_or_equal(a,a)|less_or_equal(a,a)),
% 0.13/0.51 inference(resolution,[status(thm)],[f245,f78])).
% 0.13/0.51 fof(f560,definition,(
% 0.13/0.51 sQ96_spl <=> (less_or_equal(a,a))),
% 0.13/0.51 introduced(definition,[new_symbols(definition,[sQ96_spl])],[split_symbol_definition])).
% 0.13/0.51 fof(f563,plain,(
% 0.13/0.51 sQ96_spl),
% 0.13/0.51 inference(split_clause,[status(thm)],[f539,f560])).
% 0.13/0.51 fof(f579,plain,(
% 0.13/0.51 less_or_equal(additive_identity,additive_identity)|less_or_equal(additive_identity,additive_identity)),
% 0.13/0.51 inference(resolution,[status(thm)],[f246,f59])).
% 0.13/0.51 fof(f600,definition,(
% 0.13/0.51 sQ103_spl <=> (less_or_equal(additive_identity,additive_identity))),
% 0.13/0.51 introduced(definition,[new_symbols(definition,[sQ103_spl])],[split_symbol_definition])).
% 0.13/0.51 fof(f603,plain,(
% 0.13/0.51 sQ103_spl),
% 0.13/0.51 inference(split_clause,[status(thm)],[f579,f600])).
% 0.13/0.51 fof(f604,plain,(
% 0.13/0.51 less_or_equal(additive_inverse(s),additive_inverse(s))|less_or_equal(additive_inverse(s),additive_inverse(s))),
% 0.13/0.51 inference(resolution,[status(thm)],[f238,f90])).
% 0.13/0.51 fof(f613,definition,(
% 0.13/0.51 sQ104_spl <=> (less_or_equal(additive_inverse(s),additive_inverse(s)))),
% 0.13/0.51 introduced(definition,[new_symbols(definition,[sQ104_spl])],[split_symbol_definition])).
% 0.13/0.51 fof(f616,plain,(
% 0.13/0.51 sQ104_spl),
% 0.13/0.51 inference(split_clause,[status(thm)],[f604,f613])).
% 0.13/0.51 fof(f635,plain,(
% 0.13/0.51 less_or_equal(multiplicative_identity,multiplicative_identity)|less_or_equal(multiplicative_identity,multiplicative_identity)),
% 0.13/0.51 inference(resolution,[status(thm)],[f242,f63])).
% 0.13/0.51 fof(f644,definition,(
% 0.13/0.51 sQ107_spl <=> (less_or_equal(multiplicative_identity,multiplicative_identity))),
% 0.13/0.51 introduced(definition,[new_symbols(definition,[sQ107_spl])],[split_symbol_definition])).
% 0.13/0.51 fof(f647,plain,(
% 0.13/0.51 sQ107_spl),
% 0.13/0.51 inference(split_clause,[status(thm)],[f635,f644])).
% 0.13/0.51 fof(f661,plain,(
% 0.13/0.51 ![X0]: (less_or_equal(X0,additive_inverse(k))|less_or_equal(additive_inverse(k),X0)|~defined(X0))),
% 0.13/0.51 inference(resolution,[status(thm)],[f91,f73])).
% 0.13/0.51 fof(f666,plain,(
% 0.13/0.51 defined(additive_inverse(additive_inverse(k)))),
% 0.13/0.51 inference(resolution,[status(thm)],[f91,f60])).
% 0.13/0.51 fof(f741,plain,(
% 0.13/0.51 less_or_equal(additive_inverse(k),additive_inverse(k))|less_or_equal(additive_inverse(k),additive_inverse(k))),
% 0.13/0.51 inference(resolution,[status(thm)],[f661,f91])).
% 0.13/0.51 fof(f751,definition,(
% 0.13/0.51 sQ129_spl <=> (less_or_equal(additive_inverse(k),additive_inverse(k)))),
% 0.13/0.51 introduced(definition,[new_symbols(definition,[sQ129_spl])],[split_symbol_definition])).
% 0.13/0.51 fof(f754,plain,(
% 0.13/0.51 sQ129_spl),
% 0.13/0.51 inference(split_clause,[status(thm)],[f741,f751])).
% 0.13/0.51 fof(f774,plain,(
% 0.13/0.51 ![X0]: (less_or_equal(X0,additive_inverse(d))|less_or_equal(additive_inverse(d),X0)|~defined(X0))),
% 0.13/0.51 inference(resolution,[status(thm)],[f92,f73])).
% 0.13/0.51 fof(f779,plain,(
% 0.13/0.51 defined(additive_inverse(additive_inverse(d)))),
% 0.13/0.51 inference(resolution,[status(thm)],[f92,f60])).
% 0.13/0.51 fof(f861,plain,(
% 0.13/0.51 less_or_equal(additive_inverse(d),additive_inverse(d))|less_or_equal(additive_inverse(d),additive_inverse(d))),
% 0.13/0.51 inference(resolution,[status(thm)],[f774,f92])).
% 0.13/0.51 fof(f872,definition,(
% 0.13/0.51 sQ153_spl <=> (less_or_equal(additive_inverse(d),additive_inverse(d)))),
% 0.13/0.51 introduced(definition,[new_symbols(definition,[sQ153_spl])],[split_symbol_definition])).
% 0.13/0.51 fof(f875,plain,(
% 0.13/0.51 sQ153_spl),
% 0.13/0.51 inference(split_clause,[status(thm)],[f861,f872])).
% 0.13/0.51 fof(f897,plain,(
% 0.13/0.51 ![X0]: (less_or_equal(X0,additive_inverse(c))|less_or_equal(additive_inverse(c),X0)|~defined(X0))),
% 0.13/0.51 inference(resolution,[status(thm)],[f94,f73])).
% 0.13/0.51 fof(f902,plain,(
% 0.13/0.51 defined(additive_inverse(additive_inverse(c)))),
% 0.13/0.51 inference(resolution,[status(thm)],[f94,f60])).
% 0.13/0.51 fof(f991,plain,(
% 0.13/0.51 less_or_equal(additive_inverse(c),additive_inverse(c))|less_or_equal(additive_inverse(c),additive_inverse(c))),
% 0.13/0.51 inference(resolution,[status(thm)],[f897,f94])).
% 0.13/0.51 fof(f1003,definition,(
% 0.13/0.51 sQ179_spl <=> (less_or_equal(additive_inverse(c),additive_inverse(c)))),
% 0.13/0.51 introduced(definition,[new_symbols(definition,[sQ179_spl])],[split_symbol_definition])).
% 0.13/0.51 fof(f1006,plain,(
% 0.13/0.51 sQ179_spl),
% 0.13/0.51 inference(split_clause,[status(thm)],[f991,f1003])).
% 0.13/0.51 fof(f1030,plain,(
% 0.13/0.51 ![X0]: (less_or_equal(X0,additive_inverse(b))|less_or_equal(additive_inverse(b),X0)|~defined(X0))),
% 0.13/0.51 inference(resolution,[status(thm)],[f95,f73])).
% 0.13/0.51 fof(f1035,plain,(
% 0.13/0.51 defined(additive_inverse(additive_inverse(b)))),
% 0.13/0.51 inference(resolution,[status(thm)],[f95,f60])).
% 0.13/0.51 fof(f1131,plain,(
% 0.13/0.51 less_or_equal(additive_inverse(b),additive_inverse(b))|less_or_equal(additive_inverse(b),additive_inverse(b))),
% 0.13/0.51 inference(resolution,[status(thm)],[f1030,f95])).
% 0.13/0.51 fof(f1144,definition,(
% 0.13/0.51 sQ207_spl <=> (less_or_equal(additive_inverse(b),additive_inverse(b)))),
% 0.13/0.51 introduced(definition,[new_symbols(definition,[sQ207_spl])],[split_symbol_definition])).
% 0.13/0.51 fof(f1147,plain,(
% 0.13/0.51 sQ207_spl),
% 0.13/0.51 inference(split_clause,[status(thm)],[f1131,f1144])).
% 0.13/0.51 fof(f1173,plain,(
% 0.13/0.51 ![X0]: (less_or_equal(X0,additive_inverse(a))|less_or_equal(additive_inverse(a),X0)|~defined(X0))),
% 0.13/0.51 inference(resolution,[status(thm)],[f96,f73])).
% 0.13/0.51 fof(f1281,plain,(
% 0.13/0.51 less_or_equal(additive_inverse(a),additive_inverse(a))|less_or_equal(additive_inverse(a),additive_inverse(a))),
% 0.13/0.51 inference(resolution,[status(thm)],[f1173,f96])).
% 0.13/0.51 fof(f1295,definition,(
% 0.13/0.51 sQ237_spl <=> (less_or_equal(additive_inverse(a),additive_inverse(a)))),
% 0.13/0.51 introduced(definition,[new_symbols(definition,[sQ237_spl])],[split_symbol_definition])).
% 0.13/0.51 fof(f1298,plain,(
% 0.13/0.51 sQ237_spl),
% 0.13/0.51 inference(split_clause,[status(thm)],[f1281,f1295])).
% 0.13/0.51 fof(f1326,plain,(
% 0.13/0.51 ![X0]: (less_or_equal(X0,additive_inverse(additive_identity))|less_or_equal(additive_inverse(additive_identity),X0)|~defined(X0))),
% 0.13/0.51 inference(resolution,[status(thm)],[f97,f73])).
% 0.13/0.51 fof(f1441,plain,(
% 0.13/0.51 less_or_equal(additive_inverse(additive_identity),additive_inverse(additive_identity))|less_or_equal(additive_inverse(additive_identity),additive_inverse(additive_identity))),
% 0.13/0.51 inference(resolution,[status(thm)],[f1326,f97])).
% 0.13/0.51 fof(f1456,definition,(
% 0.13/0.51 sQ269_spl <=> (less_or_equal(additive_inverse(additive_identity),additive_inverse(additive_identity)))),
% 0.13/0.51 introduced(definition,[new_symbols(definition,[sQ269_spl])],[split_symbol_definition])).
% 0.13/0.51 fof(f1459,plain,(
% 0.13/0.51 sQ269_spl),
% 0.13/0.51 inference(split_clause,[status(thm)],[f1441,f1456])).
% 0.13/0.51 fof(f1647,plain,(
% 0.13/0.51 ![X0,X1,X2]: (product(X0,k,X1)|~product(X0,b,X2)|~product(X2,c,X1))),
% 0.13/0.51 inference(resolution,[status(thm)],[f47,f88])).
% 0.13/0.51 fof(f1654,plain,(
% 0.13/0.51 ![X0,X1,X2]: (product(X0,X1,s)|~product(X0,X2,a)|~product(X2,multiplicative_inverse(b),X1))),
% 0.13/0.51 inference(resolution,[status(thm)],[f47,f86])).
% 0.13/0.51 fof(f1852,plain,(
% 0.13/0.51 product(d,a,k)),
% 0.13/0.51 inference(resolution,[status(thm)],[f52,f87])).
% 0.13/0.51 fof(f1869,plain,(
% 0.13/0.51 ![X0,X1,X2]: (product(X0,k,X1)|~product(X0,d,X2)|~product(X2,a,X1))),
% 0.13/0.51 inference(resolution,[status(thm)],[f1852,f47])).
% 0.13/0.51 fof(f1895,plain,(
% 0.13/0.51 ![X0]: (less_or_equal(X0,additive_inverse(multiplicative_identity))|less_or_equal(additive_inverse(multiplicative_identity),X0)|~defined(X0))),
% 0.13/0.51 inference(resolution,[status(thm)],[f93,f73])).
% 0.13/0.51 fof(f2045,plain,(
% 0.13/0.51 product(multiplicative_identity,c,c)),
% 0.13/0.51 inference(resolution,[status(thm)],[f50,f80])).
% 0.13/0.51 fof(f2047,plain,(
% 0.13/0.51 product(multiplicative_identity,a,a)),
% 0.13/0.51 inference(resolution,[status(thm)],[f50,f78])).
% 0.13/0.51 fof(f2087,plain,(
% 0.13/0.51 less_or_equal(additive_inverse(multiplicative_identity),additive_inverse(multiplicative_identity))|less_or_equal(additive_inverse(multiplicative_identity),additive_inverse(multiplicative_identity))),
% 0.13/0.51 inference(resolution,[status(thm)],[f1895,f93])).
% 0.13/0.51 fof(f2105,definition,(
% 0.13/0.51 sQ377_spl <=> (less_or_equal(additive_inverse(multiplicative_identity),additive_inverse(multiplicative_identity)))),
% 0.13/0.51 introduced(definition,[new_symbols(definition,[sQ377_spl])],[split_symbol_definition])).
% 0.13/0.51 fof(f2108,plain,(
% 0.13/0.51 sQ377_spl),
% 0.13/0.51 inference(split_clause,[status(thm)],[f2087,f2105])).
% 0.13/0.51 fof(f2243,plain,(
% 0.13/0.51 ![X0]: (less_or_equal(X0,additive_inverse(additive_inverse(s)))|less_or_equal(additive_inverse(additive_inverse(s)),X0)|~defined(X0))),
% 0.13/0.51 inference(resolution,[status(thm)],[f98,f73])).
% 0.13/0.51 fof(f2388,plain,(
% 0.13/0.51 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)))),
% 0.13/0.51 inference(resolution,[status(thm)],[f2243,f98])).
% 0.13/0.51 fof(f2407,definition,(
% 0.13/0.51 sQ417_spl <=> (less_or_equal(additive_inverse(additive_inverse(s)),additive_inverse(additive_inverse(s))))),
% 0.13/0.51 introduced(definition,[new_symbols(definition,[sQ417_spl])],[split_symbol_definition])).
% 0.13/0.51 fof(f2410,plain,(
% 0.13/0.51 sQ417_spl),
% 0.13/0.51 inference(split_clause,[status(thm)],[f2388,f2407])).
% 0.13/0.51 fof(f2494,plain,(
% 0.13/0.51 ![X0]: (less_or_equal(X0,additive_inverse(additive_inverse(k)))|less_or_equal(additive_inverse(additive_inverse(k)),X0)|~defined(X0))),
% 0.13/0.51 inference(resolution,[status(thm)],[f666,f73])).
% 0.13/0.51 fof(f2646,plain,(
% 0.13/0.51 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)))),
% 0.13/0.51 inference(resolution,[status(thm)],[f2494,f666])).
% 0.13/0.51 fof(f2666,definition,(
% 0.13/0.51 sQ459_spl <=> (less_or_equal(additive_inverse(additive_inverse(k)),additive_inverse(additive_inverse(k))))),
% 0.13/0.51 introduced(definition,[new_symbols(definition,[sQ459_spl])],[split_symbol_definition])).
% 0.13/0.51 fof(f2669,plain,(
% 0.13/0.51 sQ459_spl),
% 0.13/0.51 inference(split_clause,[status(thm)],[f2646,f2666])).
% 0.13/0.51 fof(f2756,plain,(
% 0.13/0.51 ![X0]: (product(multiplicative_inverse(b),k,X0)|~product(multiplicative_identity,c,X0)|~sQ24_spl)),
% 0.13/0.51 inference(resolution,[status(thm)],[f223,f1647])).
% 0.13/0.51 fof(f2764,plain,(
% 0.13/0.51 ![X0]: (product(multiplicative_inverse(d),k,X0)|~product(multiplicative_identity,a,X0)|~sQ21_spl)),
% 0.13/0.51 inference(resolution,[status(thm)],[f211,f1869])).
% 0.13/0.51 fof(f2798,plain,(
% 0.13/0.51 ![X0]: (less_or_equal(X0,additive_inverse(additive_inverse(d)))|less_or_equal(additive_inverse(additive_inverse(d)),X0)|~defined(X0))),
% 0.13/0.51 inference(resolution,[status(thm)],[f779,f73])).
% 0.13/0.51 fof(f3183,definition,(
% 0.13/0.51 sQ530_spl <=> (sum(additive_identity,additive_identity,multiplicative_identity))),
% 0.13/0.51 introduced(definition,[new_symbols(definition,[sQ530_spl])],[split_symbol_definition])).
% 0.13/0.51 fof(f3184,plain,(
% 0.13/0.51 sum(additive_identity,additive_identity,multiplicative_identity)|~sQ530_spl),
% 0.13/0.51 inference(component_clause,[status(thm)],[f3183])).
% 0.13/0.51 fof(f3282,plain,(
% 0.13/0.51 $false|~sQ530_spl),
% 0.13/0.51 inference(forward_subsumption_resolution,[status(thm)],[f3184,f77])).
% 0.13/0.51 fof(f3283,plain,(
% 0.13/0.51 ~sQ530_spl),
% 0.13/0.51 inference(contradiction_clause,[status(thm)],[f3282])).
% 0.13/0.51 fof(f3286,plain,(
% 0.13/0.51 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)))),
% 0.13/0.51 inference(resolution,[status(thm)],[f2798,f779])).
% 0.13/0.51 fof(f3307,definition,(
% 0.13/0.51 sQ553_spl <=> (less_or_equal(additive_inverse(additive_inverse(d)),additive_inverse(additive_inverse(d))))),
% 0.13/0.51 introduced(definition,[new_symbols(definition,[sQ553_spl])],[split_symbol_definition])).
% 0.13/0.51 fof(f3310,plain,(
% 0.13/0.51 sQ553_spl),
% 0.13/0.51 inference(split_clause,[status(thm)],[f3286,f3307])).
% 0.13/0.51 fof(f3386,plain,(
% 0.13/0.51 ![X0]: (less_or_equal(X0,additive_inverse(additive_inverse(c)))|less_or_equal(additive_inverse(additive_inverse(c)),X0)|~defined(X0))),
% 0.13/0.51 inference(resolution,[status(thm)],[f902,f73])).
% 0.13/0.51 fof(f3552,plain,(
% 0.13/0.51 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)))),
% 0.13/0.51 inference(resolution,[status(thm)],[f3386,f902])).
% 0.13/0.51 fof(f3574,definition,(
% 0.13/0.51 sQ602_spl <=> (less_or_equal(additive_inverse(additive_inverse(c)),additive_inverse(additive_inverse(c))))),
% 0.13/0.51 introduced(definition,[new_symbols(definition,[sQ602_spl])],[split_symbol_definition])).
% 0.13/0.51 fof(f3577,plain,(
% 0.13/0.51 sQ602_spl),
% 0.13/0.51 inference(split_clause,[status(thm)],[f3552,f3574])).
% 0.13/0.51 fof(f3633,plain,(
% 0.13/0.51 product(multiplicative_inverse(b),k,c)|~sQ24_spl),
% 0.13/0.51 inference(resolution,[status(thm)],[f2045,f2756])).
% 0.13/0.51 fof(f3649,plain,(
% 0.13/0.51 product(k,multiplicative_inverse(b),c)|~sQ24_spl),
% 0.13/0.51 inference(resolution,[status(thm)],[f3633,f52])).
% 0.13/0.51 fof(f3660,plain,(
% 0.13/0.51 ![X0]: (product(X0,c,s)|~product(X0,k,a)|~sQ24_spl)),
% 0.13/0.51 inference(resolution,[status(thm)],[f3649,f1654])).
% 0.13/0.51 fof(f3763,plain,(
% 0.13/0.51 ![X0]: (less_or_equal(X0,additive_inverse(additive_inverse(b)))|less_or_equal(additive_inverse(additive_inverse(b)),X0)|~defined(X0))),
% 0.13/0.51 inference(resolution,[status(thm)],[f1035,f73])).
% 0.13/0.51 fof(f3960,plain,(
% 0.13/0.51 product(multiplicative_inverse(d),k,a)|~sQ21_spl),
% 0.13/0.51 inference(resolution,[status(thm)],[f2047,f2764])).
% 0.13/0.51 fof(f4142,plain,(
% 0.13/0.51 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)))),
% 0.13/0.51 inference(resolution,[status(thm)],[f3763,f1035])).
% 0.13/0.51 fof(f4165,definition,(
% 0.13/0.51 sQ666_spl <=> (less_or_equal(additive_inverse(additive_inverse(b)),additive_inverse(additive_inverse(b))))),
% 0.13/0.51 introduced(definition,[new_symbols(definition,[sQ666_spl])],[split_symbol_definition])).
% 0.13/0.51 fof(f4168,plain,(
% 0.13/0.51 sQ666_spl),
% 0.13/0.51 inference(split_clause,[status(thm)],[f4142,f4165])).
% 0.13/0.51 fof(f4190,plain,(
% 0.13/0.51 product(multiplicative_inverse(d),c,s)|~sQ21_spl|~sQ24_spl),
% 0.13/0.51 inference(resolution,[status(thm)],[f3960,f3660])).
% 0.13/0.51 fof(f4205,plain,(
% 0.13/0.51 product(c,multiplicative_inverse(d),s)|~sQ21_spl|~sQ24_spl),
% 0.13/0.51 inference(resolution,[status(thm)],[f4190,f52])).
% 0.13/0.51 fof(f4213,plain,(
% 0.13/0.51 $false|~sQ21_spl|~sQ24_spl),
% 0.13/0.51 inference(forward_subsumption_resolution,[status(thm)],[f4205,f89])).
% 0.13/0.51 fof(f4214,plain,(
% 0.13/0.51 ~sQ21_spl|~sQ24_spl),
% 0.13/0.51 inference(contradiction_clause,[status(thm)],[f4213])).
% 0.13/0.51 fof(f4215,plain,(
% 0.13/0.51 $false),
% 0.13/0.51 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])).
% 0.13/0.51 % SZS output end CNFRefutation for theBenchmark.p
% 0.66/0.53 % Elapsed time: 0.154306 seconds
% 0.66/0.53 % CPU time: 0.981814 seconds
% 0.66/0.53 % Total memory used: 33.024 MB
% 0.66/0.53 % Net memory used: 31.870 MB
%------------------------------------------------------------------------------