%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : FLD012-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 : n011.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:17 PM UTC 2026
% Result : Unsatisfiable 201.19s 25.84s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : FLD012-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 : n011.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:37:41 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.08/0.36 % Drodi V4.1.1
% 201.19/25.84 % Refutation found
% 201.19/25.84 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 201.19/25.84 % SZS output start CNFRefutation for theBenchmark
% 201.19/25.84 fof(f1,axiom,(
% 201.19/25.84 (![X,V,W,Y,U,Z]: (( sum(X,V,W)| ~ sum(X,Y,U)| ~ sum(Y,Z,V)| ~ sum(U,Z,W) ) ))),
% 201.19/25.84 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 201.19/25.84 fof(f2,axiom,(
% 201.19/25.84 (![U,Z,W,X,Y,V]: (( sum(U,Z,W)| ~ sum(X,Y,U)| ~ sum(Y,Z,V)| ~ sum(X,V,W) ) ))),
% 201.19/25.84 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 201.19/25.84 fof(f3,axiom,(
% 201.19/25.84 (![X]: (( sum(additive_identity,X,X)| ~ defined(X) ) ))),
% 201.19/25.84 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 201.19/25.84 fof(f4,axiom,(
% 201.19/25.84 (![X]: (( sum(additive_inverse(X),X,additive_identity)| ~ defined(X) ) ))),
% 201.19/25.84 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 201.19/25.84 fof(f5,axiom,(
% 201.19/25.84 (![Y,X,Z]: (( sum(Y,X,Z)| ~ sum(X,Y,Z) ) ))),
% 201.19/25.84 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 201.19/25.84 fof(f6,axiom,(
% 201.19/25.84 (![X,V,W,Y,U,Z]: (( product(X,V,W)| ~ product(X,Y,U)| ~ product(Y,Z,V)| ~ product(U,Z,W) ) ))),
% 201.19/25.84 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 201.19/25.84 fof(f7,axiom,(
% 201.19/25.84 (![U,Z,W,X,Y,V]: (( product(U,Z,W)| ~ product(X,Y,U)| ~ product(Y,Z,V)| ~ product(X,V,W) ) ))),
% 201.19/25.84 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 201.19/25.84 fof(f8,axiom,(
% 201.19/25.84 (![X]: (( product(multiplicative_identity,X,X)| ~ defined(X) ) ))),
% 201.19/25.84 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 201.19/25.84 fof(f9,axiom,(
% 201.19/25.84 (![X]: (( product(multiplicative_inverse(X),X,multiplicative_identity)| sum(additive_identity,X,additive_identity)| ~ defined(X) ) ))),
% 201.19/25.84 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 201.19/25.84 fof(f10,axiom,(
% 201.19/25.84 (![Y,X,Z]: (( product(Y,X,Z)| ~ product(X,Y,Z) ) ))),
% 201.19/25.84 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 201.19/25.84 fof(f11,axiom,(
% 201.19/25.84 (![C,D,B,X,Y,A,Z]: (( sum(C,D,B)| ~ sum(X,Y,A)| ~ product(A,Z,B)| ~ product(X,Z,C)| ~ product(Y,Z,D) ) ))),
% 201.19/25.84 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 201.19/25.84 fof(f13,axiom,(
% 201.19/25.84 (![X,Y]: (( defined(add(X,Y))| ~ defined(X)| ~ defined(Y) ) ))),
% 201.19/25.84 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 201.19/25.84 fof(f14,axiom,(
% 201.19/25.84 defined(additive_identity) ),
% 201.19/25.84 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 201.19/25.84 fof(f15,axiom,(
% 201.19/25.84 (![X]: (( defined(additive_inverse(X))| ~ defined(X) ) ))),
% 201.19/25.84 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 201.19/25.84 fof(f16,axiom,(
% 201.19/25.84 (![X,Y]: (( defined(multiply(X,Y))| ~ defined(X)| ~ defined(Y) ) ))),
% 201.19/25.84 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 201.19/25.84 fof(f17,axiom,(
% 201.19/25.84 defined(multiplicative_identity) ),
% 201.19/25.84 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 201.19/25.84 fof(f18,axiom,(
% 201.19/25.84 (![X]: (( defined(multiplicative_inverse(X))| ~ defined(X)| sum(additive_identity,X,additive_identity) ) ))),
% 201.19/25.84 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 201.19/25.84 fof(f23,axiom,(
% 201.19/25.84 (![X,Y]: (( less_or_equal(X,Y)| less_or_equal(Y,X)| ~ defined(X)| ~ defined(Y) ) ))),
% 201.19/25.84 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 201.19/25.84 fof(f26,axiom,(
% 201.19/25.84 ~ sum(additive_identity,additive_identity,multiplicative_identity) ),
% 201.19/25.84 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 201.19/25.84 fof(f27,hypothesis,(
% 201.19/25.84 defined(a) ),
% 201.19/25.84 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 201.19/25.84 fof(f28,hypothesis,(
% 201.19/25.84 defined(b) ),
% 201.19/25.84 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 201.19/25.84 fof(f29,hypothesis,(
% 201.19/25.84 defined(u) ),
% 201.19/25.84 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 201.19/25.84 fof(f30,hypothesis,(
% 201.19/25.84 defined(v) ),
% 201.19/25.84 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 201.19/25.84 fof(f31,negated_conjecture,(
% 201.19/25.84 ~ sum(additive_identity,a,additive_identity) ),
% 201.19/25.84 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 201.19/25.84 fof(f32,negated_conjecture,(
% 201.19/25.84 ~ sum(additive_identity,b,additive_identity) ),
% 201.19/25.84 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 201.19/25.84 fof(f33,negated_conjecture,(
% 201.19/25.84 product(a,b,u) ),
% 201.19/25.84 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 201.19/25.84 fof(f34,negated_conjecture,(
% 201.19/25.84 product(multiplicative_inverse(a),multiplicative_inverse(b),v) ),
% 201.19/25.84 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 201.19/25.84 fof(f35,negated_conjecture,(
% 201.19/25.84 ~ product(multiplicative_identity,multiplicative_inverse(u),v) ),
% 201.19/25.84 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 201.19/25.84 fof(f36,plain,(
% 201.19/25.84 ![W,U,Z]: ((![V,Y]: ((![X]: (sum(X,V,W)|~sum(X,Y,U)))|~sum(Y,Z,V)))|~sum(U,Z,W))),
% 201.19/25.84 inference(miniscoping,[status(thm)],[f1])).
% 201.19/25.84 fof(f37,plain,(
% 201.19/25.84 ![X0,X1,X2,X3,X4,X5]: (sum(X0,X1,X2)|~sum(X0,X3,X4)|~sum(X3,X5,X1)|~sum(X4,X5,X2))),
% 201.19/25.84 inference(cnf_transformation,[status(thm)],[f36])).
% 201.19/25.84 fof(f38,plain,(
% 201.19/25.84 ![W,X,V]: ((![Z,Y]: ((![U]: (sum(U,Z,W)|~sum(X,Y,U)))|~sum(Y,Z,V)))|~sum(X,V,W))),
% 201.19/25.84 inference(miniscoping,[status(thm)],[f2])).
% 201.19/25.84 fof(f39,plain,(
% 201.19/25.84 ![X0,X1,X2,X3,X4,X5]: (sum(X0,X1,X2)|~sum(X3,X4,X0)|~sum(X4,X1,X5)|~sum(X3,X5,X2))),
% 201.19/25.84 inference(cnf_transformation,[status(thm)],[f38])).
% 201.19/25.84 fof(f40,plain,(
% 201.19/25.84 ![X0]: (sum(additive_identity,X0,X0)|~defined(X0))),
% 201.19/25.84 inference(cnf_transformation,[status(thm)],[f3])).
% 201.19/25.84 fof(f41,plain,(
% 201.19/25.84 ![X0]: (sum(additive_inverse(X0),X0,additive_identity)|~defined(X0))),
% 201.19/25.84 inference(cnf_transformation,[status(thm)],[f4])).
% 201.19/25.84 fof(f42,plain,(
% 201.19/25.84 ![X0,X1,X2]: (sum(X0,X1,X2)|~sum(X1,X0,X2))),
% 201.19/25.84 inference(cnf_transformation,[status(thm)],[f5])).
% 201.19/25.84 fof(f43,plain,(
% 201.19/25.84 ![W,U,Z]: ((![V,Y]: ((![X]: (product(X,V,W)|~product(X,Y,U)))|~product(Y,Z,V)))|~product(U,Z,W))),
% 201.19/25.84 inference(miniscoping,[status(thm)],[f6])).
% 201.19/25.84 fof(f44,plain,(
% 201.19/25.84 ![X0,X1,X2,X3,X4,X5]: (product(X0,X1,X2)|~product(X0,X3,X4)|~product(X3,X5,X1)|~product(X4,X5,X2))),
% 201.19/25.84 inference(cnf_transformation,[status(thm)],[f43])).
% 201.19/25.84 fof(f45,plain,(
% 201.19/25.84 ![W,X,V]: ((![Z,Y]: ((![U]: (product(U,Z,W)|~product(X,Y,U)))|~product(Y,Z,V)))|~product(X,V,W))),
% 201.19/25.84 inference(miniscoping,[status(thm)],[f7])).
% 201.19/25.84 fof(f46,plain,(
% 201.19/25.84 ![X0,X1,X2,X3,X4,X5]: (product(X0,X1,X2)|~product(X3,X4,X0)|~product(X4,X1,X5)|~product(X3,X5,X2))),
% 201.19/25.84 inference(cnf_transformation,[status(thm)],[f45])).
% 201.19/25.84 fof(f47,plain,(
% 201.19/25.84 ![X0]: (product(multiplicative_identity,X0,X0)|~defined(X0))),
% 201.19/25.84 inference(cnf_transformation,[status(thm)],[f8])).
% 201.19/25.84 fof(f48,plain,(
% 201.19/25.84 ![X0]: (product(multiplicative_inverse(X0),X0,multiplicative_identity)|sum(additive_identity,X0,additive_identity)|~defined(X0))),
% 201.19/25.84 inference(cnf_transformation,[status(thm)],[f9])).
% 201.19/25.84 fof(f49,plain,(
% 201.19/25.84 ![X0,X1,X2]: (product(X0,X1,X2)|~product(X1,X0,X2))),
% 201.19/25.84 inference(cnf_transformation,[status(thm)],[f10])).
% 201.19/25.84 fof(f50,plain,(
% 201.19/25.84 ![D,Y,Z]: ((![C,X]: ((![B,A]: ((sum(C,D,B)|~sum(X,Y,A))|~product(A,Z,B)))|~product(X,Z,C)))|~product(Y,Z,D))),
% 201.19/25.84 inference(miniscoping,[status(thm)],[f11])).
% 201.19/25.84 fof(f51,plain,(
% 201.19/25.84 ![X0,X1,X2,X3,X4,X5,X6]: (sum(X0,X1,X2)|~sum(X3,X4,X5)|~product(X5,X6,X2)|~product(X3,X6,X0)|~product(X4,X6,X1))),
% 201.19/25.84 inference(cnf_transformation,[status(thm)],[f50])).
% 201.19/25.84 fof(f54,plain,(
% 201.19/25.84 ![Y]: ((![X]: (defined(add(X,Y))|~defined(X)))|~defined(Y))),
% 201.19/25.84 inference(miniscoping,[status(thm)],[f13])).
% 201.19/25.84 fof(f55,plain,(
% 201.19/25.84 ![X0,X1]: (defined(add(X0,X1))|~defined(X0)|~defined(X1))),
% 201.19/25.84 inference(cnf_transformation,[status(thm)],[f54])).
% 201.19/25.84 fof(f56,plain,(
% 201.19/25.84 defined(additive_identity)),
% 201.19/25.84 inference(cnf_transformation,[status(thm)],[f14])).
% 201.19/25.84 fof(f57,plain,(
% 201.19/25.84 ![X0]: (defined(additive_inverse(X0))|~defined(X0))),
% 201.19/25.84 inference(cnf_transformation,[status(thm)],[f15])).
% 201.19/25.84 fof(f58,plain,(
% 201.19/25.84 ![Y]: ((![X]: (defined(multiply(X,Y))|~defined(X)))|~defined(Y))),
% 201.19/25.84 inference(miniscoping,[status(thm)],[f16])).
% 201.19/25.84 fof(f59,plain,(
% 201.19/25.84 ![X0,X1]: (defined(multiply(X0,X1))|~defined(X0)|~defined(X1))),
% 201.19/25.84 inference(cnf_transformation,[status(thm)],[f58])).
% 201.19/25.84 fof(f60,plain,(
% 201.19/25.84 defined(multiplicative_identity)),
% 201.19/25.84 inference(cnf_transformation,[status(thm)],[f17])).
% 201.19/25.84 fof(f61,plain,(
% 201.19/25.84 ![X0]: (defined(multiplicative_inverse(X0))|~defined(X0)|sum(additive_identity,X0,additive_identity))),
% 201.19/25.84 inference(cnf_transformation,[status(thm)],[f18])).
% 201.19/25.84 fof(f69,plain,(
% 201.19/25.84 ![Y]: ((![X]: ((less_or_equal(X,Y)|less_or_equal(Y,X))|~defined(X)))|~defined(Y))),
% 201.19/25.84 inference(miniscoping,[status(thm)],[f23])).
% 201.19/25.84 fof(f70,plain,(
% 201.19/25.84 ![X0,X1]: (less_or_equal(X0,X1)|less_or_equal(X1,X0)|~defined(X0)|~defined(X1))),
% 201.19/25.84 inference(cnf_transformation,[status(thm)],[f69])).
% 201.19/25.84 fof(f74,plain,(
% 201.19/25.84 ~sum(additive_identity,additive_identity,multiplicative_identity)),
% 201.19/25.84 inference(cnf_transformation,[status(thm)],[f26])).
% 201.19/25.84 fof(f75,plain,(
% 201.19/25.84 defined(a)),
% 201.19/25.84 inference(cnf_transformation,[status(thm)],[f27])).
% 201.19/25.84 fof(f76,plain,(
% 201.19/25.84 defined(b)),
% 201.19/25.84 inference(cnf_transformation,[status(thm)],[f28])).
% 201.19/25.84 fof(f77,plain,(
% 201.19/25.84 defined(u)),
% 201.19/25.84 inference(cnf_transformation,[status(thm)],[f29])).
% 201.19/25.84 fof(f78,plain,(
% 201.19/25.84 defined(v)),
% 201.19/25.84 inference(cnf_transformation,[status(thm)],[f30])).
% 201.19/25.84 fof(f79,plain,(
% 201.19/25.84 ~sum(additive_identity,a,additive_identity)),
% 201.19/25.84 inference(cnf_transformation,[status(thm)],[f31])).
% 201.19/25.84 fof(f80,plain,(
% 201.19/25.84 ~sum(additive_identity,b,additive_identity)),
% 201.19/25.84 inference(cnf_transformation,[status(thm)],[f32])).
% 201.19/25.84 fof(f81,plain,(
% 201.19/25.84 product(a,b,u)),
% 201.19/25.84 inference(cnf_transformation,[status(thm)],[f33])).
% 201.19/25.84 fof(f82,plain,(
% 201.19/25.84 product(multiplicative_inverse(a),multiplicative_inverse(b),v)),
% 201.19/25.84 inference(cnf_transformation,[status(thm)],[f34])).
% 201.19/25.84 fof(f83,plain,(
% 201.19/25.84 ~product(multiplicative_identity,multiplicative_inverse(u),v)),
% 201.19/25.84 inference(cnf_transformation,[status(thm)],[f35])).
% 201.19/25.84 fof(f84,plain,(
% 201.19/25.84 ![X0,X1,X2,X3]: (sum(X0,X1,X1)|~sum(X0,X2,X2)|~sum(X2,X3,X1))),
% 201.19/25.84 inference(factoring,[status(thm)],[f37])).
% 201.19/25.84 fof(f86,plain,(
% 201.19/25.84 defined(additive_inverse(v))),
% 201.19/25.84 inference(resolution,[status(thm)],[f57,f78])).
% 201.19/25.84 fof(f87,plain,(
% 201.19/25.84 defined(additive_inverse(u))),
% 201.19/25.84 inference(resolution,[status(thm)],[f57,f77])).
% 201.19/25.84 fof(f88,plain,(
% 201.19/25.84 defined(additive_inverse(b))),
% 201.19/25.84 inference(resolution,[status(thm)],[f57,f76])).
% 201.19/25.84 fof(f89,plain,(
% 201.19/25.84 defined(additive_inverse(a))),
% 201.19/25.84 inference(resolution,[status(thm)],[f57,f75])).
% 201.19/25.84 fof(f90,plain,(
% 201.19/25.84 defined(additive_inverse(multiplicative_identity))),
% 201.19/25.84 inference(resolution,[status(thm)],[f57,f60])).
% 201.19/25.84 fof(f91,plain,(
% 201.19/25.84 defined(additive_inverse(additive_identity))),
% 201.19/25.84 inference(resolution,[status(thm)],[f57,f56])).
% 201.19/25.84 fof(f92,plain,(
% 201.19/25.84 defined(additive_inverse(additive_inverse(v)))),
% 201.19/25.84 inference(resolution,[status(thm)],[f86,f57])).
% 201.19/25.84 fof(f93,plain,(
% 201.19/25.84 defined(additive_inverse(additive_inverse(u)))),
% 201.19/25.84 inference(resolution,[status(thm)],[f87,f57])).
% 201.19/25.84 fof(f94,plain,(
% 201.19/25.84 defined(additive_inverse(additive_inverse(b)))),
% 201.19/25.84 inference(resolution,[status(thm)],[f88,f57])).
% 201.19/25.84 fof(f99,plain,(
% 201.19/25.84 sum(additive_identity,u,u)),
% 201.19/25.84 inference(resolution,[status(thm)],[f40,f77])).
% 201.19/25.84 fof(f100,plain,(
% 201.19/25.84 sum(additive_identity,b,b)),
% 201.19/25.84 inference(resolution,[status(thm)],[f40,f76])).
% 201.19/25.84 fof(f109,plain,(
% 201.19/25.84 sum(additive_inverse(b),b,additive_identity)),
% 201.19/25.84 inference(resolution,[status(thm)],[f41,f76])).
% 201.19/25.84 fof(f110,plain,(
% 201.19/25.84 sum(additive_inverse(a),a,additive_identity)),
% 201.19/25.84 inference(resolution,[status(thm)],[f41,f75])).
% 201.19/25.84 fof(f119,plain,(
% 201.19/25.84 defined(multiplicative_inverse(a))|sum(additive_identity,a,additive_identity)),
% 201.19/25.84 inference(resolution,[status(thm)],[f61,f75])).
% 201.19/25.84 fof(f153,definition,(
% 201.19/25.84 sQ9_spl <=> (sum(additive_identity,u,additive_identity))),
% 201.19/25.84 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 201.19/25.84 fof(f154,plain,(
% 201.19/25.84 sum(additive_identity,u,additive_identity)|~sQ9_spl),
% 201.19/25.84 inference(component_clause,[status(thm)],[f153])).
% 201.19/25.84 fof(f160,definition,(
% 201.19/25.84 sQ11_spl <=> (sum(additive_identity,b,additive_identity))),
% 201.19/25.84 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 201.19/25.84 fof(f161,plain,(
% 201.19/25.84 sum(additive_identity,b,additive_identity)|~sQ11_spl),
% 201.19/25.84 inference(component_clause,[status(thm)],[f160])).
% 201.19/25.84 fof(f164,definition,(
% 201.19/25.84 sQ12_spl <=> (defined(multiplicative_inverse(a)))),
% 201.19/25.84 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 201.19/25.84 fof(f165,plain,(
% 201.19/25.84 defined(multiplicative_inverse(a))|~sQ12_spl),
% 201.19/25.84 inference(component_clause,[status(thm)],[f164])).
% 201.19/25.84 fof(f167,definition,(
% 201.19/25.84 sQ13_spl <=> (sum(additive_identity,a,additive_identity))),
% 201.19/25.84 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 201.19/25.84 fof(f168,plain,(
% 201.19/25.84 sum(additive_identity,a,additive_identity)|~sQ13_spl),
% 201.19/25.84 inference(component_clause,[status(thm)],[f167])).
% 201.19/25.84 fof(f170,plain,(
% 201.19/25.84 sQ12_spl|sQ13_spl),
% 201.19/25.84 inference(split_clause,[status(thm)],[f119,f164,f167])).
% 201.19/25.84 fof(f189,plain,(
% 201.19/25.84 product(multiplicative_inverse(u),u,multiplicative_identity)|sum(additive_identity,u,additive_identity)),
% 201.19/25.84 inference(resolution,[status(thm)],[f48,f77])).
% 201.19/25.84 fof(f190,plain,(
% 201.19/25.84 product(multiplicative_inverse(b),b,multiplicative_identity)|sum(additive_identity,b,additive_identity)),
% 201.19/25.84 inference(resolution,[status(thm)],[f48,f76])).
% 201.19/25.84 fof(f191,plain,(
% 201.19/25.84 product(multiplicative_inverse(a),a,multiplicative_identity)|sum(additive_identity,a,additive_identity)),
% 201.19/25.84 inference(resolution,[status(thm)],[f48,f75])).
% 201.19/25.84 fof(f210,definition,(
% 201.19/25.84 sQ22_spl <=> (product(multiplicative_inverse(u),u,multiplicative_identity))),
% 201.19/25.84 introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition])).
% 201.19/25.84 fof(f211,plain,(
% 201.19/25.84 product(multiplicative_inverse(u),u,multiplicative_identity)|~sQ22_spl),
% 201.19/25.84 inference(component_clause,[status(thm)],[f210])).
% 201.19/25.84 fof(f213,plain,(
% 201.19/25.84 sQ22_spl|sQ9_spl),
% 201.19/25.84 inference(split_clause,[status(thm)],[f189,f210,f153])).
% 201.19/25.84 fof(f214,definition,(
% 201.19/25.84 sQ23_spl <=> (product(multiplicative_inverse(b),b,multiplicative_identity))),
% 201.19/25.84 introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition])).
% 201.19/25.84 fof(f215,plain,(
% 201.19/25.84 product(multiplicative_inverse(b),b,multiplicative_identity)|~sQ23_spl),
% 201.19/25.84 inference(component_clause,[status(thm)],[f214])).
% 201.19/25.84 fof(f217,plain,(
% 201.19/25.84 sQ23_spl|sQ11_spl),
% 201.19/25.84 inference(split_clause,[status(thm)],[f190,f214,f160])).
% 201.19/25.84 fof(f218,definition,(
% 201.19/25.84 sQ24_spl <=> (product(multiplicative_inverse(a),a,multiplicative_identity))),
% 201.19/25.84 introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition])).
% 201.19/25.84 fof(f219,plain,(
% 201.19/25.84 product(multiplicative_inverse(a),a,multiplicative_identity)|~sQ24_spl),
% 201.19/25.84 inference(component_clause,[status(thm)],[f218])).
% 201.19/25.84 fof(f221,plain,(
% 201.19/25.84 sQ24_spl|sQ13_spl),
% 201.19/25.84 inference(split_clause,[status(thm)],[f191,f218,f167])).
% 201.19/25.84 fof(f230,plain,(
% 201.19/25.84 $false|~sQ13_spl),
% 201.19/25.84 inference(forward_subsumption_resolution,[status(thm)],[f168,f79])).
% 201.19/25.84 fof(f231,plain,(
% 201.19/25.84 ~sQ13_spl),
% 201.19/25.84 inference(contradiction_clause,[status(thm)],[f230])).
% 201.19/25.84 fof(f232,plain,(
% 201.19/25.84 $false|~sQ11_spl),
% 201.19/25.84 inference(forward_subsumption_resolution,[status(thm)],[f161,f80])).
% 201.19/25.84 fof(f233,plain,(
% 201.19/25.84 ~sQ11_spl),
% 201.19/25.84 inference(contradiction_clause,[status(thm)],[f232])).
% 201.19/25.84 fof(f234,plain,(
% 201.19/25.84 ![X0]: (less_or_equal(X0,additive_inverse(b))|less_or_equal(additive_inverse(b),X0)|~defined(X0))),
% 201.19/25.84 inference(resolution,[status(thm)],[f70,f88])).
% 201.19/25.84 fof(f235,plain,(
% 201.19/25.84 ![X0]: (less_or_equal(X0,additive_inverse(u))|less_or_equal(additive_inverse(u),X0)|~defined(X0))),
% 201.19/25.84 inference(resolution,[status(thm)],[f70,f87])).
% 201.19/25.84 fof(f236,plain,(
% 201.19/25.84 ![X0]: (less_or_equal(X0,additive_inverse(v))|less_or_equal(additive_inverse(v),X0)|~defined(X0))),
% 201.19/25.84 inference(resolution,[status(thm)],[f70,f86])).
% 201.19/25.84 fof(f237,plain,(
% 201.19/25.84 ![X0]: (less_or_equal(X0,v)|less_or_equal(v,X0)|~defined(X0))),
% 201.19/25.84 inference(resolution,[status(thm)],[f70,f78])).
% 201.19/25.84 fof(f238,plain,(
% 201.19/25.84 ![X0]: (less_or_equal(X0,u)|less_or_equal(u,X0)|~defined(X0))),
% 201.19/25.84 inference(resolution,[status(thm)],[f70,f77])).
% 201.19/25.84 fof(f239,plain,(
% 201.19/25.84 ![X0]: (less_or_equal(X0,b)|less_or_equal(b,X0)|~defined(X0))),
% 201.19/25.84 inference(resolution,[status(thm)],[f70,f76])).
% 201.19/25.84 fof(f240,plain,(
% 201.19/25.84 ![X0]: (less_or_equal(X0,a)|less_or_equal(a,X0)|~defined(X0))),
% 201.19/25.84 inference(resolution,[status(thm)],[f70,f75])).
% 201.19/25.84 fof(f241,plain,(
% 201.19/25.84 ![X0]: (less_or_equal(X0,multiplicative_identity)|less_or_equal(multiplicative_identity,X0)|~defined(X0))),
% 201.19/25.84 inference(resolution,[status(thm)],[f70,f60])).
% 201.19/25.84 fof(f242,plain,(
% 201.19/25.84 ![X0]: (less_or_equal(X0,additive_identity)|less_or_equal(additive_identity,X0)|~defined(X0))),
% 201.19/25.84 inference(resolution,[status(thm)],[f70,f56])).
% 201.19/25.84 fof(f246,plain,(
% 201.19/25.84 less_or_equal(v,v)|less_or_equal(v,v)),
% 201.19/25.84 inference(resolution,[status(thm)],[f237,f78])).
% 201.19/25.84 fof(f273,definition,(
% 201.19/25.84 sQ33_spl <=> (less_or_equal(v,v))),
% 201.19/25.84 introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition])).
% 201.19/25.84 fof(f276,plain,(
% 201.19/25.84 sQ33_spl),
% 201.19/25.84 inference(split_clause,[status(thm)],[f246,f273])).
% 201.19/25.84 fof(f316,plain,(
% 201.19/25.84 less_or_equal(u,u)|less_or_equal(u,u)),
% 201.19/25.84 inference(resolution,[status(thm)],[f238,f77])).
% 201.19/25.84 fof(f343,definition,(
% 201.19/25.84 sQ50_spl <=> (less_or_equal(u,u))),
% 201.19/25.84 introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition])).
% 201.19/25.84 fof(f346,plain,(
% 201.19/25.84 sQ50_spl),
% 201.19/25.84 inference(split_clause,[status(thm)],[f316,f343])).
% 201.19/25.84 fof(f380,plain,(
% 201.19/25.84 less_or_equal(b,b)|less_or_equal(b,b)),
% 201.19/25.84 inference(resolution,[status(thm)],[f239,f76])).
% 201.19/25.84 fof(f407,definition,(
% 201.19/25.84 sQ65_spl <=> (less_or_equal(b,b))),
% 201.19/25.84 introduced(definition,[new_symbols(definition,[sQ65_spl])],[split_symbol_definition])).
% 201.19/25.84 fof(f410,plain,(
% 201.19/25.84 sQ65_spl),
% 201.19/25.84 inference(split_clause,[status(thm)],[f380,f407])).
% 201.19/25.84 fof(f438,plain,(
% 201.19/25.84 less_or_equal(a,a)|less_or_equal(a,a)),
% 201.19/25.84 inference(resolution,[status(thm)],[f240,f75])).
% 201.19/25.84 fof(f465,definition,(
% 201.19/25.84 sQ78_spl <=> (less_or_equal(a,a))),
% 201.19/25.84 introduced(definition,[new_symbols(definition,[sQ78_spl])],[split_symbol_definition])).
% 201.19/25.84 fof(f468,plain,(
% 201.19/25.84 sQ78_spl),
% 201.19/25.84 inference(split_clause,[status(thm)],[f438,f465])).
% 201.19/25.84 fof(f490,plain,(
% 201.19/25.84 less_or_equal(multiplicative_identity,multiplicative_identity)|less_or_equal(multiplicative_identity,multiplicative_identity)),
% 201.19/25.84 inference(resolution,[status(thm)],[f241,f60])).
% 201.19/25.84 fof(f517,definition,(
% 201.19/25.84 sQ89_spl <=> (less_or_equal(multiplicative_identity,multiplicative_identity))),
% 201.19/25.84 introduced(definition,[new_symbols(definition,[sQ89_spl])],[split_symbol_definition])).
% 201.19/25.84 fof(f520,plain,(
% 201.19/25.84 sQ89_spl),
% 201.19/25.84 inference(split_clause,[status(thm)],[f490,f517])).
% 201.19/25.84 fof(f536,plain,(
% 201.19/25.84 less_or_equal(additive_identity,additive_identity)|less_or_equal(additive_identity,additive_identity)),
% 201.19/25.84 inference(resolution,[status(thm)],[f242,f56])).
% 201.19/25.84 fof(f563,definition,(
% 201.19/25.84 sQ98_spl <=> (less_or_equal(additive_identity,additive_identity))),
% 201.19/25.84 introduced(definition,[new_symbols(definition,[sQ98_spl])],[split_symbol_definition])).
% 201.19/25.84 fof(f566,plain,(
% 201.19/25.84 sQ98_spl),
% 201.19/25.84 inference(split_clause,[status(thm)],[f536,f563])).
% 201.19/25.84 fof(f567,plain,(
% 201.19/25.84 less_or_equal(additive_inverse(b),additive_inverse(b))|less_or_equal(additive_inverse(b),additive_inverse(b))),
% 201.19/25.84 inference(resolution,[status(thm)],[f234,f88])).
% 201.19/25.84 fof(f576,definition,(
% 201.19/25.84 sQ99_spl <=> (less_or_equal(additive_inverse(b),additive_inverse(b)))),
% 201.19/25.84 introduced(definition,[new_symbols(definition,[sQ99_spl])],[split_symbol_definition])).
% 201.19/25.84 fof(f579,plain,(
% 201.19/25.84 sQ99_spl),
% 201.19/25.84 inference(split_clause,[status(thm)],[f567,f576])).
% 201.19/25.84 fof(f601,plain,(
% 201.19/25.84 less_or_equal(additive_inverse(u),additive_inverse(u))|less_or_equal(additive_inverse(u),additive_inverse(u))),
% 201.19/25.84 inference(resolution,[status(thm)],[f235,f87])).
% 201.19/25.84 fof(f610,definition,(
% 201.19/25.84 sQ104_spl <=> (less_or_equal(additive_inverse(u),additive_inverse(u)))),
% 201.19/25.84 introduced(definition,[new_symbols(definition,[sQ104_spl])],[split_symbol_definition])).
% 201.19/25.84 fof(f613,plain,(
% 201.19/25.84 sQ104_spl),
% 201.19/25.84 inference(split_clause,[status(thm)],[f601,f610])).
% 201.19/25.84 fof(f629,plain,(
% 201.19/25.84 less_or_equal(additive_inverse(v),additive_inverse(v))|less_or_equal(additive_inverse(v),additive_inverse(v))),
% 201.19/25.84 inference(resolution,[status(thm)],[f236,f86])).
% 201.19/25.84 fof(f638,definition,(
% 201.19/25.84 sQ107_spl <=> (less_or_equal(additive_inverse(v),additive_inverse(v)))),
% 201.19/25.84 introduced(definition,[new_symbols(definition,[sQ107_spl])],[split_symbol_definition])).
% 201.19/25.84 fof(f641,plain,(
% 201.19/25.84 sQ107_spl),
% 201.19/25.84 inference(split_clause,[status(thm)],[f629,f638])).
% 201.19/25.84 fof(f657,plain,(
% 201.19/25.84 ![X0]: (less_or_equal(X0,additive_inverse(a))|less_or_equal(additive_inverse(a),X0)|~defined(X0))),
% 201.19/25.84 inference(resolution,[status(thm)],[f89,f70])).
% 201.19/25.84 fof(f662,plain,(
% 201.19/25.84 defined(additive_inverse(additive_inverse(a)))),
% 201.19/25.84 inference(resolution,[status(thm)],[f89,f57])).
% 201.19/25.84 fof(f737,plain,(
% 201.19/25.84 less_or_equal(additive_inverse(a),additive_inverse(a))|less_or_equal(additive_inverse(a),additive_inverse(a))),
% 201.19/25.84 inference(resolution,[status(thm)],[f657,f89])).
% 201.19/25.84 fof(f747,definition,(
% 201.19/25.84 sQ129_spl <=> (less_or_equal(additive_inverse(a),additive_inverse(a)))),
% 201.19/25.84 introduced(definition,[new_symbols(definition,[sQ129_spl])],[split_symbol_definition])).
% 201.19/25.84 fof(f750,plain,(
% 201.19/25.84 sQ129_spl),
% 201.19/25.84 inference(split_clause,[status(thm)],[f737,f747])).
% 201.19/25.84 fof(f770,plain,(
% 201.19/25.84 ![X0]: (less_or_equal(X0,additive_inverse(multiplicative_identity))|less_or_equal(additive_inverse(multiplicative_identity),X0)|~defined(X0))),
% 201.19/25.84 inference(resolution,[status(thm)],[f90,f70])).
% 201.19/25.84 fof(f775,plain,(
% 201.19/25.84 defined(additive_inverse(additive_inverse(multiplicative_identity)))),
% 201.19/25.84 inference(resolution,[status(thm)],[f90,f57])).
% 201.19/25.84 fof(f857,plain,(
% 201.19/25.84 less_or_equal(additive_inverse(multiplicative_identity),additive_inverse(multiplicative_identity))|less_or_equal(additive_inverse(multiplicative_identity),additive_inverse(multiplicative_identity))),
% 201.19/25.84 inference(resolution,[status(thm)],[f770,f90])).
% 201.19/25.84 fof(f868,definition,(
% 201.19/25.84 sQ153_spl <=> (less_or_equal(additive_inverse(multiplicative_identity),additive_inverse(multiplicative_identity)))),
% 201.19/25.84 introduced(definition,[new_symbols(definition,[sQ153_spl])],[split_symbol_definition])).
% 201.19/25.84 fof(f871,plain,(
% 201.19/25.84 sQ153_spl),
% 201.19/25.84 inference(split_clause,[status(thm)],[f857,f868])).
% 201.19/25.84 fof(f893,plain,(
% 201.19/25.84 ![X0]: (less_or_equal(X0,additive_inverse(additive_identity))|less_or_equal(additive_inverse(additive_identity),X0)|~defined(X0))),
% 201.19/25.84 inference(resolution,[status(thm)],[f91,f70])).
% 201.19/25.84 fof(f898,plain,(
% 201.19/25.84 defined(additive_inverse(additive_inverse(additive_identity)))),
% 201.19/25.84 inference(resolution,[status(thm)],[f91,f57])).
% 201.19/25.84 fof(f987,plain,(
% 201.19/25.84 less_or_equal(additive_inverse(additive_identity),additive_inverse(additive_identity))|less_or_equal(additive_inverse(additive_identity),additive_inverse(additive_identity))),
% 201.19/25.84 inference(resolution,[status(thm)],[f893,f91])).
% 201.19/25.84 fof(f999,definition,(
% 201.19/25.84 sQ179_spl <=> (less_or_equal(additive_inverse(additive_identity),additive_inverse(additive_identity)))),
% 201.19/25.84 introduced(definition,[new_symbols(definition,[sQ179_spl])],[split_symbol_definition])).
% 201.19/25.84 fof(f1002,plain,(
% 201.19/25.84 sQ179_spl),
% 201.19/25.84 inference(split_clause,[status(thm)],[f987,f999])).
% 201.19/25.84 fof(f1311,plain,(
% 201.19/25.84 ![X0,X1,X2]: (product(X0,u,X1)|~product(X0,a,X2)|~product(X2,b,X1))),
% 201.19/25.84 inference(resolution,[status(thm)],[f44,f81])).
% 201.19/25.84 fof(f1312,plain,(
% 201.19/25.84 ![X0,X1,X2]: (product(X0,X1,v)|~product(X0,X2,multiplicative_inverse(a))|~product(X2,multiplicative_inverse(b),X1))),
% 201.19/25.84 inference(resolution,[status(thm)],[f44,f82])).
% 201.19/25.84 fof(f1319,plain,(
% 201.19/25.84 ![X0,X1,X2]: (product(X0,multiplicative_inverse(b),X1)|~product(X2,multiplicative_inverse(a),X0)|~product(X2,v,X1))),
% 201.19/25.84 inference(resolution,[status(thm)],[f46,f82])).
% 201.19/25.84 fof(f1327,plain,(
% 201.19/25.84 product(multiplicative_identity,multiplicative_inverse(a),multiplicative_inverse(a))|~sQ12_spl),
% 201.19/25.84 inference(resolution,[status(thm)],[f47,f165])).
% 201.19/25.84 fof(f1336,plain,(
% 201.19/25.84 product(multiplicative_identity,b,b)),
% 201.19/25.84 inference(resolution,[status(thm)],[f47,f76])).
% 201.19/25.84 fof(f1337,plain,(
% 201.19/25.84 product(multiplicative_identity,a,a)),
% 201.19/25.84 inference(resolution,[status(thm)],[f47,f75])).
% 201.19/25.84 fof(f1340,plain,(
% 201.19/25.84 product(multiplicative_inverse(b),multiplicative_inverse(a),v)),
% 201.19/25.84 inference(resolution,[status(thm)],[f49,f82])).
% 201.19/25.84 fof(f1341,plain,(
% 201.19/25.84 product(b,a,u)),
% 201.19/25.84 inference(resolution,[status(thm)],[f49,f81])).
% 201.19/25.84 fof(f1356,plain,(
% 201.19/25.84 ![X0,X1,X2]: (product(X0,u,X1)|~product(X0,b,X2)|~product(X2,a,X1))),
% 201.19/25.84 inference(resolution,[status(thm)],[f1341,f44])).
% 201.19/25.84 fof(f1378,plain,(
% 201.19/25.84 ![X0]: (less_or_equal(X0,additive_inverse(additive_inverse(v)))|less_or_equal(additive_inverse(additive_inverse(v)),X0)|~defined(X0))),
% 201.19/25.84 inference(resolution,[status(thm)],[f92,f70])).
% 201.19/25.84 fof(f1508,plain,(
% 201.19/25.84 ![X0]: (less_or_equal(X0,additive_inverse(additive_inverse(u)))|less_or_equal(additive_inverse(additive_inverse(u)),X0)|~defined(X0))),
% 201.19/25.84 inference(resolution,[status(thm)],[f93,f70])).
% 201.19/25.84 fof(f1638,plain,(
% 201.19/25.84 ![X0]: (less_or_equal(X0,additive_inverse(additive_inverse(b)))|less_or_equal(additive_inverse(additive_inverse(b)),X0)|~defined(X0))),
% 201.19/25.84 inference(resolution,[status(thm)],[f94,f70])).
% 201.19/25.84 fof(f1782,plain,(
% 201.19/25.84 ![X0,X1,X2]: (sum(X0,X0,X0)|~sum(X1,X1,X1)|~product(X1,X2,X0))),
% 201.19/25.84 inference(factoring,[status(thm)],[f51])).
% 201.19/25.84 fof(f1783,definition,(
% 201.19/25.84 sQ331_spl <=> (sum(u,u,u))),
% 201.19/25.84 introduced(definition,[new_symbols(definition,[sQ331_spl])],[split_symbol_definition])).
% 201.19/25.84 fof(f1801,definition,(
% 201.19/25.84 sQ336_spl <=> (sum(a,a,a))),
% 201.19/25.84 introduced(definition,[new_symbols(definition,[sQ336_spl])],[split_symbol_definition])).
% 201.19/25.84 fof(f1802,plain,(
% 201.19/25.84 sum(a,a,a)|~sQ336_spl),
% 201.19/25.84 inference(component_clause,[status(thm)],[f1801])).
% 201.19/25.84 fof(f1835,plain,(
% 201.19/25.84 ![X0]: (sum(X0,b,b)|~sum(X0,additive_identity,additive_identity))),
% 201.19/25.84 inference(resolution,[status(thm)],[f100,f37])).
% 201.19/25.84 fof(f1880,plain,(
% 201.19/25.84 ![X0]: (defined(add(X0,v))|~defined(X0))),
% 201.19/25.84 inference(resolution,[status(thm)],[f55,f78])).
% 201.19/25.84 fof(f1881,plain,(
% 201.19/25.84 ![X0]: (defined(add(X0,u))|~defined(X0))),
% 201.19/25.84 inference(resolution,[status(thm)],[f55,f77])).
% 201.19/25.84 fof(f1882,plain,(
% 201.19/25.84 ![X0]: (defined(add(X0,b))|~defined(X0))),
% 201.19/25.84 inference(resolution,[status(thm)],[f55,f76])).
% 201.19/25.84 fof(f1883,plain,(
% 201.19/25.84 ![X0]: (defined(add(X0,a))|~defined(X0))),
% 201.19/25.84 inference(resolution,[status(thm)],[f55,f75])).
% 201.19/25.84 fof(f1884,plain,(
% 201.19/25.84 ![X0]: (defined(add(X0,multiplicative_identity))|~defined(X0))),
% 201.19/25.84 inference(resolution,[status(thm)],[f55,f60])).
% 201.19/25.84 fof(f1885,plain,(
% 201.19/25.84 ![X0]: (defined(add(X0,additive_identity))|~defined(X0))),
% 201.19/25.84 inference(resolution,[status(thm)],[f55,f56])).
% 201.19/25.84 fof(f1897,plain,(
% 201.19/25.84 ![X0]: (defined(multiply(X0,v))|~defined(X0))),
% 201.19/25.84 inference(resolution,[status(thm)],[f59,f78])).
% 201.19/25.84 fof(f1898,plain,(
% 201.19/25.84 ![X0]: (defined(multiply(X0,u))|~defined(X0))),
% 201.19/25.84 inference(resolution,[status(thm)],[f59,f77])).
% 201.19/25.84 fof(f1899,plain,(
% 201.19/25.84 ![X0]: (defined(multiply(X0,b))|~defined(X0))),
% 201.19/25.84 inference(resolution,[status(thm)],[f59,f76])).
% 201.19/25.84 fof(f1900,plain,(
% 201.19/25.84 ![X0]: (defined(multiply(X0,a))|~defined(X0))),
% 201.19/25.84 inference(resolution,[status(thm)],[f59,f75])).
% 201.19/25.84 fof(f1901,plain,(
% 201.19/25.84 ![X0]: (defined(multiply(X0,multiplicative_identity))|~defined(X0))),
% 201.19/25.84 inference(resolution,[status(thm)],[f59,f60])).
% 201.19/25.84 fof(f1902,plain,(
% 201.19/25.84 ![X0]: (defined(multiply(X0,additive_identity))|~defined(X0))),
% 201.19/25.84 inference(resolution,[status(thm)],[f59,f56])).
% 201.19/25.84 fof(f1924,plain,(
% 201.19/25.84 less_or_equal(additive_inverse(additive_inverse(v)),additive_inverse(additive_inverse(v)))|less_or_equal(additive_inverse(additive_inverse(v)),additive_inverse(additive_inverse(v)))),
% 201.19/25.84 inference(resolution,[status(thm)],[f1378,f92])).
% 201.19/25.84 fof(f1953,definition,(
% 201.19/25.84 sQ341_spl <=> (less_or_equal(additive_inverse(additive_inverse(v)),additive_inverse(additive_inverse(v))))),
% 201.19/25.84 introduced(definition,[new_symbols(definition,[sQ341_spl])],[split_symbol_definition])).
% 201.19/25.84 fof(f1956,plain,(
% 201.19/25.84 sQ341_spl),
% 201.19/25.84 inference(split_clause,[status(thm)],[f1924,f1953])).
% 201.19/25.84 fof(f1972,plain,(
% 201.19/25.84 less_or_equal(additive_inverse(additive_inverse(u)),additive_inverse(additive_inverse(u)))|less_or_equal(additive_inverse(additive_inverse(u)),additive_inverse(additive_inverse(u)))),
% 201.19/25.84 inference(resolution,[status(thm)],[f1508,f93])).
% 201.19/25.84 fof(f1995,definition,(
% 201.19/25.84 sQ344_spl <=> (less_or_equal(additive_inverse(additive_inverse(u)),additive_inverse(additive_inverse(u))))),
% 201.19/25.84 introduced(definition,[new_symbols(definition,[sQ344_spl])],[split_symbol_definition])).
% 201.19/25.84 fof(f1998,plain,(
% 201.19/25.84 sQ344_spl),
% 201.19/25.84 inference(split_clause,[status(thm)],[f1972,f1995])).
% 201.19/25.84 fof(f2014,plain,(
% 201.19/25.84 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)))),
% 201.19/25.84 inference(resolution,[status(thm)],[f1638,f94])).
% 201.19/25.84 fof(f2031,definition,(
% 201.19/25.84 sQ345_spl <=> (less_or_equal(additive_inverse(additive_inverse(b)),additive_inverse(additive_inverse(b))))),
% 201.19/25.84 introduced(definition,[new_symbols(definition,[sQ345_spl])],[split_symbol_definition])).
% 201.19/25.84 fof(f2034,plain,(
% 201.19/25.84 sQ345_spl),
% 201.19/25.84 inference(split_clause,[status(thm)],[f2014,f2031])).
% 201.19/25.84 fof(f2225,plain,(
% 201.19/25.84 sum(u,additive_identity,additive_identity)|~sQ9_spl),
% 201.19/25.84 inference(resolution,[status(thm)],[f154,f42])).
% 201.19/25.84 fof(f3464,definition,(
% 201.19/25.84 sQ377_spl <=> (sum(additive_identity,additive_identity,multiplicative_identity))),
% 201.19/25.84 introduced(definition,[new_symbols(definition,[sQ377_spl])],[split_symbol_definition])).
% 201.19/25.84 fof(f3465,plain,(
% 201.19/25.84 sum(additive_identity,additive_identity,multiplicative_identity)|~sQ377_spl),
% 201.19/25.84 inference(component_clause,[status(thm)],[f3464])).
% 201.19/25.84 fof(f3468,plain,(
% 201.19/25.84 $false|~sQ377_spl),
% 201.19/25.84 inference(forward_subsumption_resolution,[status(thm)],[f3465,f74])).
% 201.19/25.84 fof(f3469,plain,(
% 201.19/25.84 ~sQ377_spl),
% 201.19/25.84 inference(contradiction_clause,[status(thm)],[f3468])).
% 201.19/25.84 fof(f3603,plain,(
% 201.19/25.84 ![X0]: (product(multiplicative_inverse(b),u,X0)|~product(multiplicative_identity,a,X0)|~sQ23_spl)),
% 201.19/25.84 inference(resolution,[status(thm)],[f215,f1356])).
% 201.19/25.84 fof(f4408,plain,(
% 201.19/25.84 ![X0]: (product(X0,u,b)|~product(X0,a,multiplicative_identity))),
% 201.19/25.84 inference(resolution,[status(thm)],[f1336,f1311])).
% 201.19/25.84 fof(f4444,definition,(
% 201.19/25.84 sQ441_spl <=> (sum(b,u,b))),
% 201.19/25.84 introduced(definition,[new_symbols(definition,[sQ441_spl])],[split_symbol_definition])).
% 201.19/25.84 fof(f4445,plain,(
% 201.19/25.84 sum(b,u,b)|~sQ441_spl),
% 201.19/25.84 inference(component_clause,[status(thm)],[f4444])).
% 201.19/25.84 fof(f4451,definition,(
% 201.19/25.84 sQ443_spl <=> (sum(u,b,b))),
% 201.19/25.84 introduced(definition,[new_symbols(definition,[sQ443_spl])],[split_symbol_definition])).
% 201.19/25.84 fof(f4452,plain,(
% 201.19/25.84 sum(u,b,b)|~sQ443_spl),
% 201.19/25.84 inference(component_clause,[status(thm)],[f4451])).
% 201.19/25.84 fof(f4842,plain,(
% 201.19/25.84 product(multiplicative_inverse(a),u,b)|~sQ24_spl),
% 201.19/25.84 inference(resolution,[status(thm)],[f4408,f219])).
% 201.19/25.84 fof(f4983,plain,(
% 201.19/25.84 product(u,multiplicative_inverse(a),b)|~sQ24_spl),
% 201.19/25.84 inference(resolution,[status(thm)],[f4842,f49])).
% 201.19/25.84 fof(f4985,plain,(
% 201.19/25.84 ![X0,X1,X2]: (product(X0,u,X1)|~product(X2,multiplicative_inverse(a),X0)|~product(X2,b,X1)|~sQ24_spl)),
% 201.19/25.84 inference(resolution,[status(thm)],[f4842,f46])).
% 201.19/25.84 fof(f5012,plain,(
% 201.19/25.84 ![X0]: (product(b,multiplicative_inverse(b),X0)|~product(u,v,X0)|~sQ24_spl)),
% 201.19/25.84 inference(resolution,[status(thm)],[f4983,f1319])).
% 201.19/25.84 fof(f5031,plain,(
% 201.19/25.84 ![X0,X1,X2]: (product(X0,b,X1)|~product(X0,u,X2)|~product(X2,multiplicative_inverse(a),X1)|~sQ24_spl)),
% 201.19/25.84 inference(resolution,[status(thm)],[f4983,f44])).
% 201.19/25.84 fof(f5231,plain,(
% 201.19/25.84 product(multiplicative_inverse(b),u,a)|~sQ23_spl),
% 201.19/25.84 inference(resolution,[status(thm)],[f1337,f3603])).
% 201.19/25.84 fof(f5557,plain,(
% 201.19/25.84 ![X0,X1,X2]: (sum(X0,a,X1)|~sum(X2,a,X0)|~sum(X2,a,X1)|~sQ336_spl)),
% 201.19/25.84 inference(resolution,[status(thm)],[f1802,f39])).
% 201.19/25.84 fof(f5746,plain,(
% 201.19/25.84 ![X0]: (sum(X0,a,additive_identity)|~sum(additive_inverse(a),a,X0)|~sQ336_spl)),
% 201.19/25.84 inference(resolution,[status(thm)],[f5557,f110])).
% 201.19/25.84 fof(f5943,plain,(
% 201.19/25.84 product(u,multiplicative_inverse(b),a)|~sQ23_spl),
% 201.19/25.84 inference(resolution,[status(thm)],[f5231,f49])).
% 201.19/25.84 fof(f6164,plain,(
% 201.19/25.84 defined(add(v,v))),
% 201.19/25.84 inference(resolution,[status(thm)],[f1880,f78])).
% 201.19/25.84 fof(f6165,plain,(
% 201.19/25.84 defined(add(u,v))),
% 201.19/25.84 inference(resolution,[status(thm)],[f1880,f77])).
% 201.19/25.84 fof(f6166,plain,(
% 201.19/25.84 defined(add(b,v))),
% 201.19/25.84 inference(resolution,[status(thm)],[f1880,f76])).
% 201.19/25.84 fof(f6167,plain,(
% 201.19/25.84 defined(add(a,v))),
% 201.19/25.84 inference(resolution,[status(thm)],[f1880,f75])).
% 201.19/25.84 fof(f6168,plain,(
% 201.19/25.84 defined(add(multiplicative_identity,v))),
% 201.19/25.84 inference(resolution,[status(thm)],[f1880,f60])).
% 201.19/25.84 fof(f6169,plain,(
% 201.19/25.84 defined(add(additive_identity,v))),
% 201.19/25.84 inference(resolution,[status(thm)],[f1880,f56])).
% 201.19/25.84 fof(f6181,plain,(
% 201.19/25.84 defined(add(v,u))),
% 201.19/25.84 inference(resolution,[status(thm)],[f1881,f78])).
% 201.19/25.84 fof(f6182,plain,(
% 201.19/25.84 defined(add(u,u))),
% 201.19/25.84 inference(resolution,[status(thm)],[f1881,f77])).
% 201.19/25.84 fof(f6183,plain,(
% 201.19/25.84 defined(add(b,u))),
% 201.19/25.84 inference(resolution,[status(thm)],[f1881,f76])).
% 201.19/25.84 fof(f6184,plain,(
% 201.19/25.84 defined(add(a,u))),
% 201.19/25.84 inference(resolution,[status(thm)],[f1881,f75])).
% 201.19/25.84 fof(f6185,plain,(
% 201.19/25.84 defined(add(multiplicative_identity,u))),
% 201.19/25.84 inference(resolution,[status(thm)],[f1881,f60])).
% 201.19/25.84 fof(f6186,plain,(
% 201.19/25.84 defined(add(additive_identity,u))),
% 201.19/25.84 inference(resolution,[status(thm)],[f1881,f56])).
% 201.19/25.84 fof(f6213,plain,(
% 201.19/25.84 defined(add(v,b))),
% 201.19/25.84 inference(resolution,[status(thm)],[f1882,f78])).
% 201.19/25.84 fof(f6214,plain,(
% 201.19/25.84 defined(add(u,b))),
% 201.19/25.84 inference(resolution,[status(thm)],[f1882,f77])).
% 201.19/25.84 fof(f6215,plain,(
% 201.19/25.84 defined(add(b,b))),
% 201.19/25.84 inference(resolution,[status(thm)],[f1882,f76])).
% 201.19/25.84 fof(f6216,plain,(
% 201.19/25.84 defined(add(a,b))),
% 201.19/25.84 inference(resolution,[status(thm)],[f1882,f75])).
% 201.19/25.84 fof(f6217,plain,(
% 201.19/25.84 defined(add(multiplicative_identity,b))),
% 201.19/25.84 inference(resolution,[status(thm)],[f1882,f60])).
% 201.19/25.84 fof(f6218,plain,(
% 201.19/25.84 defined(add(additive_identity,b))),
% 201.19/25.84 inference(resolution,[status(thm)],[f1882,f56])).
% 201.19/25.84 fof(f6230,plain,(
% 201.19/25.84 defined(add(v,a))),
% 201.19/25.84 inference(resolution,[status(thm)],[f1883,f78])).
% 201.19/25.84 fof(f6231,plain,(
% 201.19/25.84 defined(add(u,a))),
% 201.19/25.84 inference(resolution,[status(thm)],[f1883,f77])).
% 201.19/25.84 fof(f6232,plain,(
% 201.19/25.84 defined(add(b,a))),
% 201.19/25.84 inference(resolution,[status(thm)],[f1883,f76])).
% 201.19/25.84 fof(f6233,plain,(
% 201.19/25.84 defined(add(a,a))),
% 201.19/25.84 inference(resolution,[status(thm)],[f1883,f75])).
% 201.19/25.84 fof(f6234,plain,(
% 201.19/25.84 defined(add(multiplicative_identity,a))),
% 201.19/25.84 inference(resolution,[status(thm)],[f1883,f60])).
% 201.19/25.84 fof(f6235,plain,(
% 201.19/25.84 defined(add(additive_identity,a))),
% 201.19/25.84 inference(resolution,[status(thm)],[f1883,f56])).
% 201.19/25.84 fof(f6247,plain,(
% 201.19/25.85 defined(add(v,multiplicative_identity))),
% 201.19/25.85 inference(resolution,[status(thm)],[f1884,f78])).
% 201.19/25.85 fof(f6248,plain,(
% 201.19/25.85 defined(add(u,multiplicative_identity))),
% 201.19/25.85 inference(resolution,[status(thm)],[f1884,f77])).
% 201.19/25.85 fof(f6249,plain,(
% 201.19/25.85 defined(add(b,multiplicative_identity))),
% 201.19/25.85 inference(resolution,[status(thm)],[f1884,f76])).
% 201.19/25.85 fof(f6250,plain,(
% 201.19/25.85 defined(add(a,multiplicative_identity))),
% 201.19/25.85 inference(resolution,[status(thm)],[f1884,f75])).
% 201.19/25.85 fof(f6251,plain,(
% 201.19/25.85 defined(add(multiplicative_identity,multiplicative_identity))),
% 201.19/25.85 inference(resolution,[status(thm)],[f1884,f60])).
% 201.19/25.85 fof(f6252,plain,(
% 201.19/25.85 defined(add(additive_identity,multiplicative_identity))),
% 201.19/25.85 inference(resolution,[status(thm)],[f1884,f56])).
% 201.19/25.85 fof(f6284,plain,(
% 201.19/25.85 sum(u,b,b)|~sQ441_spl),
% 201.19/25.85 inference(resolution,[status(thm)],[f4445,f42])).
% 201.19/25.85 fof(f6290,plain,(
% 201.19/25.85 ![X0,X1,X2]: (sum(X0,b,X1)|~sum(X0,b,X2)|~sum(X2,u,X1)|~sQ441_spl)),
% 201.19/25.85 inference(resolution,[status(thm)],[f4445,f37])).
% 201.19/25.85 fof(f6300,plain,(
% 201.19/25.85 sum(b,u,b)|~sQ443_spl),
% 201.19/25.85 inference(resolution,[status(thm)],[f4452,f42])).
% 201.19/25.85 fof(f6526,plain,(
% 201.19/25.85 sum(a,a,a)|~sum(u,u,u)|~sQ23_spl),
% 201.19/25.85 inference(resolution,[status(thm)],[f5943,f1782])).
% 201.19/25.85 fof(f6573,plain,(
% 201.19/25.85 sQ336_spl|~sQ331_spl|~sQ23_spl),
% 201.19/25.85 inference(split_clause,[status(thm)],[f6526,f1801,f1783,f214])).
% 201.19/25.85 fof(f6947,plain,(
% 201.19/25.85 defined(add(v,additive_identity))),
% 201.19/25.85 inference(resolution,[status(thm)],[f1885,f78])).
% 201.19/25.85 fof(f6948,plain,(
% 201.19/25.85 defined(add(u,additive_identity))),
% 201.19/25.85 inference(resolution,[status(thm)],[f1885,f77])).
% 201.19/25.85 fof(f6949,plain,(
% 201.19/25.85 defined(add(b,additive_identity))),
% 201.19/25.85 inference(resolution,[status(thm)],[f1885,f76])).
% 201.19/25.85 fof(f6950,plain,(
% 201.19/25.85 defined(add(a,additive_identity))),
% 201.19/25.85 inference(resolution,[status(thm)],[f1885,f75])).
% 201.19/25.85 fof(f6951,plain,(
% 201.19/25.85 defined(add(multiplicative_identity,additive_identity))),
% 201.19/25.85 inference(resolution,[status(thm)],[f1885,f60])).
% 201.19/25.85 fof(f6952,plain,(
% 201.19/25.85 defined(add(additive_identity,additive_identity))),
% 201.19/25.85 inference(resolution,[status(thm)],[f1885,f56])).
% 201.19/25.85 fof(f6965,plain,(
% 201.19/25.85 defined(multiply(v,v))),
% 201.19/25.85 inference(resolution,[status(thm)],[f1897,f78])).
% 201.19/25.85 fof(f6966,plain,(
% 201.19/25.85 defined(multiply(u,v))),
% 201.19/25.85 inference(resolution,[status(thm)],[f1897,f77])).
% 201.19/25.85 fof(f6967,plain,(
% 201.19/25.85 defined(multiply(b,v))),
% 201.19/25.85 inference(resolution,[status(thm)],[f1897,f76])).
% 201.19/25.85 fof(f6968,plain,(
% 201.19/25.85 defined(multiply(a,v))),
% 201.19/25.85 inference(resolution,[status(thm)],[f1897,f75])).
% 201.19/25.85 fof(f6969,plain,(
% 201.19/25.85 defined(multiply(multiplicative_identity,v))),
% 201.19/25.85 inference(resolution,[status(thm)],[f1897,f60])).
% 201.19/25.85 fof(f6970,plain,(
% 201.19/25.85 defined(multiply(additive_identity,v))),
% 201.19/25.85 inference(resolution,[status(thm)],[f1897,f56])).
% 201.19/25.85 fof(f7003,plain,(
% 201.19/25.85 defined(multiply(v,u))),
% 201.19/25.85 inference(resolution,[status(thm)],[f1898,f78])).
% 201.19/25.85 fof(f7004,plain,(
% 201.19/25.85 defined(multiply(u,u))),
% 201.19/25.85 inference(resolution,[status(thm)],[f1898,f77])).
% 201.19/25.85 fof(f7005,plain,(
% 201.19/25.85 defined(multiply(b,u))),
% 201.19/25.85 inference(resolution,[status(thm)],[f1898,f76])).
% 201.19/25.85 fof(f7006,plain,(
% 201.19/25.85 defined(multiply(a,u))),
% 201.19/25.85 inference(resolution,[status(thm)],[f1898,f75])).
% 201.19/25.85 fof(f7007,plain,(
% 201.19/25.85 defined(multiply(multiplicative_identity,u))),
% 201.19/25.85 inference(resolution,[status(thm)],[f1898,f60])).
% 201.19/25.85 fof(f7008,plain,(
% 201.19/25.85 defined(multiply(additive_identity,u))),
% 201.19/25.85 inference(resolution,[status(thm)],[f1898,f56])).
% 201.19/25.85 fof(f7020,plain,(
% 201.19/25.85 defined(multiply(v,b))),
% 201.19/25.85 inference(resolution,[status(thm)],[f1899,f78])).
% 201.19/25.85 fof(f7021,plain,(
% 201.19/25.85 defined(multiply(u,b))),
% 201.19/25.85 inference(resolution,[status(thm)],[f1899,f77])).
% 201.19/25.85 fof(f7022,plain,(
% 201.19/25.85 defined(multiply(b,b))),
% 201.19/25.85 inference(resolution,[status(thm)],[f1899,f76])).
% 201.19/25.85 fof(f7023,plain,(
% 201.19/25.85 defined(multiply(a,b))),
% 201.19/25.85 inference(resolution,[status(thm)],[f1899,f75])).
% 201.19/25.85 fof(f7024,plain,(
% 201.19/25.85 defined(multiply(multiplicative_identity,b))),
% 201.19/25.85 inference(resolution,[status(thm)],[f1899,f60])).
% 201.19/25.85 fof(f7025,plain,(
% 201.19/25.85 defined(multiply(additive_identity,b))),
% 201.19/25.85 inference(resolution,[status(thm)],[f1899,f56])).
% 201.19/25.85 fof(f7037,plain,(
% 201.19/25.85 defined(multiply(v,a))),
% 201.19/25.85 inference(resolution,[status(thm)],[f1900,f78])).
% 201.19/25.85 fof(f7038,plain,(
% 201.19/25.85 defined(multiply(u,a))),
% 201.19/25.85 inference(resolution,[status(thm)],[f1900,f77])).
% 201.19/25.85 fof(f7039,plain,(
% 201.19/25.85 defined(multiply(b,a))),
% 201.19/25.85 inference(resolution,[status(thm)],[f1900,f76])).
% 201.19/25.85 fof(f7040,plain,(
% 201.19/25.85 defined(multiply(a,a))),
% 201.19/25.85 inference(resolution,[status(thm)],[f1900,f75])).
% 201.19/25.85 fof(f7041,plain,(
% 201.19/25.85 defined(multiply(multiplicative_identity,a))),
% 201.19/25.85 inference(resolution,[status(thm)],[f1900,f60])).
% 201.19/25.85 fof(f7042,plain,(
% 201.19/25.85 defined(multiply(additive_identity,a))),
% 201.19/25.85 inference(resolution,[status(thm)],[f1900,f56])).
% 201.19/25.85 fof(f7371,plain,(
% 201.19/25.85 sum(additive_identity,a,additive_identity)|~sQ336_spl),
% 201.19/25.85 inference(resolution,[status(thm)],[f5746,f110])).
% 201.19/25.85 fof(f7372,plain,(
% 201.19/25.85 sQ13_spl|~sQ336_spl),
% 201.19/25.85 inference(split_clause,[status(thm)],[f7371,f167,f1801])).
% 201.19/25.85 fof(f7419,plain,(
% 201.19/25.85 defined(multiply(v,multiplicative_identity))),
% 201.19/25.85 inference(resolution,[status(thm)],[f1901,f78])).
% 201.19/25.85 fof(f7420,plain,(
% 201.19/25.85 defined(multiply(u,multiplicative_identity))),
% 201.19/25.85 inference(resolution,[status(thm)],[f1901,f77])).
% 201.19/25.85 fof(f7421,plain,(
% 201.19/25.85 defined(multiply(b,multiplicative_identity))),
% 201.19/25.85 inference(resolution,[status(thm)],[f1901,f76])).
% 201.19/25.85 fof(f7422,plain,(
% 201.19/25.85 defined(multiply(a,multiplicative_identity))),
% 201.19/25.85 inference(resolution,[status(thm)],[f1901,f75])).
% 201.19/25.85 fof(f7423,plain,(
% 201.19/25.85 defined(multiply(multiplicative_identity,multiplicative_identity))),
% 201.19/25.85 inference(resolution,[status(thm)],[f1901,f60])).
% 201.19/25.85 fof(f7424,plain,(
% 201.19/25.85 defined(multiply(additive_identity,multiplicative_identity))),
% 201.19/25.85 inference(resolution,[status(thm)],[f1901,f56])).
% 201.19/25.85 fof(f7436,plain,(
% 201.19/25.85 defined(multiply(v,additive_identity))),
% 201.19/25.85 inference(resolution,[status(thm)],[f1902,f78])).
% 201.19/25.85 fof(f7437,plain,(
% 201.19/25.85 defined(multiply(u,additive_identity))),
% 201.19/25.85 inference(resolution,[status(thm)],[f1902,f77])).
% 201.19/25.85 fof(f7438,plain,(
% 201.19/25.85 defined(multiply(b,additive_identity))),
% 201.19/25.85 inference(resolution,[status(thm)],[f1902,f76])).
% 201.19/25.85 fof(f7439,plain,(
% 201.19/25.85 defined(multiply(a,additive_identity))),
% 201.19/25.85 inference(resolution,[status(thm)],[f1902,f75])).
% 201.19/25.85 fof(f7440,plain,(
% 201.19/25.85 defined(multiply(multiplicative_identity,additive_identity))),
% 201.19/25.85 inference(resolution,[status(thm)],[f1902,f60])).
% 201.19/25.85 fof(f7441,plain,(
% 201.19/25.85 defined(multiply(additive_identity,additive_identity))),
% 201.19/25.85 inference(resolution,[status(thm)],[f1902,f56])).
% 201.19/25.85 fof(f7575,plain,(
% 201.19/25.85 ![X0]: (product(v,u,X0)|~product(multiplicative_inverse(b),b,X0)|~sQ24_spl)),
% 201.19/25.85 inference(resolution,[status(thm)],[f4985,f1340])).
% 201.19/25.85 fof(f7641,plain,(
% 201.19/25.85 ![X0]: (less_or_equal(X0,additive_inverse(additive_inverse(a)))|less_or_equal(additive_inverse(additive_inverse(a)),X0)|~defined(X0))),
% 201.19/25.85 inference(resolution,[status(thm)],[f662,f70])).
% 201.19/25.85 fof(f7882,plain,(
% 201.19/25.85 ![X0]: (less_or_equal(X0,additive_inverse(additive_inverse(multiplicative_identity)))|less_or_equal(additive_inverse(additive_inverse(multiplicative_identity)),X0)|~defined(X0))),
% 201.19/25.85 inference(resolution,[status(thm)],[f775,f70])).
% 201.19/25.85 fof(f8078,plain,(
% 201.19/25.85 less_or_equal(additive_inverse(additive_inverse(a)),additive_inverse(additive_inverse(a)))|less_or_equal(additive_inverse(additive_inverse(a)),additive_inverse(additive_inverse(a)))),
% 201.19/25.85 inference(resolution,[status(thm)],[f7641,f662])).
% 201.19/25.85 fof(f8103,definition,(
% 201.19/25.85 sQ588_spl <=> (less_or_equal(additive_inverse(additive_inverse(a)),additive_inverse(additive_inverse(a))))),
% 201.19/25.85 introduced(definition,[new_symbols(definition,[sQ588_spl])],[split_symbol_definition])).
% 201.19/25.85 fof(f8106,plain,(
% 201.19/25.85 sQ588_spl),
% 201.19/25.85 inference(split_clause,[status(thm)],[f8078,f8103])).
% 201.19/25.85 fof(f8124,plain,(
% 201.19/25.85 less_or_equal(additive_inverse(additive_inverse(multiplicative_identity)),additive_inverse(additive_inverse(multiplicative_identity)))|less_or_equal(additive_inverse(additive_inverse(multiplicative_identity)),additive_inverse(additive_inverse(multiplicative_identity)))),
% 201.19/25.85 inference(resolution,[status(thm)],[f7882,f775])).
% 201.19/25.85 fof(f8143,definition,(
% 201.19/25.85 sQ589_spl <=> (less_or_equal(additive_inverse(additive_inverse(multiplicative_identity)),additive_inverse(additive_inverse(multiplicative_identity))))),
% 201.19/25.85 introduced(definition,[new_symbols(definition,[sQ589_spl])],[split_symbol_definition])).
% 201.19/25.85 fof(f8146,plain,(
% 201.19/25.85 sQ589_spl),
% 201.19/25.85 inference(split_clause,[status(thm)],[f8124,f8143])).
% 201.19/25.85 fof(f8222,plain,(
% 201.19/25.85 ![X0]: (sum(X0,b,u)|~sum(X0,b,additive_identity)|~sQ441_spl)),
% 201.19/25.85 inference(resolution,[status(thm)],[f6290,f99])).
% 201.19/25.85 fof(f8236,plain,(
% 201.19/25.85 sum(additive_inverse(b),b,u)|~sQ441_spl),
% 201.19/25.85 inference(resolution,[status(thm)],[f8222,f109])).
% 201.19/25.85 fof(f8241,plain,(
% 201.19/25.85 sum(b,additive_inverse(b),u)|~sQ441_spl),
% 201.19/25.85 inference(resolution,[status(thm)],[f8236,f42])).
% 201.19/25.85 fof(f8250,plain,(
% 201.19/25.85 ![X0]: (sum(X0,u,u)|~sum(X0,b,b)|~sQ441_spl)),
% 201.19/25.85 inference(resolution,[status(thm)],[f8241,f84])).
% 201.19/25.85 fof(f8260,plain,(
% 201.19/25.85 sum(u,u,u)|~sQ441_spl),
% 201.19/25.85 inference(resolution,[status(thm)],[f8250,f6284])).
% 201.19/25.85 fof(f8262,plain,(
% 201.19/25.85 sQ331_spl|~sQ441_spl),
% 201.19/25.85 inference(split_clause,[status(thm)],[f8260,f1783,f4444])).
% 201.19/25.85 fof(f8580,plain,(
% 201.19/25.85 product(v,u,multiplicative_identity)|~sQ24_spl|~sQ23_spl),
% 201.19/25.85 inference(resolution,[status(thm)],[f7575,f215])).
% 201.19/25.85 fof(f8598,plain,(
% 201.19/25.85 product(u,v,multiplicative_identity)|~sQ24_spl|~sQ23_spl),
% 201.19/25.85 inference(resolution,[status(thm)],[f8580,f49])).
% 201.19/25.85 fof(f8611,plain,(
% 201.19/25.85 product(b,multiplicative_inverse(b),multiplicative_identity)|~sQ23_spl|~sQ24_spl),
% 201.19/25.85 inference(resolution,[status(thm)],[f8598,f5012])).
% 201.19/25.85 fof(f9094,plain,(
% 201.19/25.85 ![X0]: (less_or_equal(X0,additive_inverse(additive_inverse(additive_identity)))|less_or_equal(additive_inverse(additive_inverse(additive_identity)),X0)|~defined(X0))),
% 201.19/25.85 inference(resolution,[status(thm)],[f898,f70])).
% 201.19/25.85 fof(f9286,plain,(
% 201.19/25.85 less_or_equal(additive_inverse(additive_inverse(additive_identity)),additive_inverse(additive_inverse(additive_identity)))|less_or_equal(additive_inverse(additive_inverse(additive_identity)),additive_inverse(additive_inverse(additive_identity)))),
% 201.19/25.85 inference(resolution,[status(thm)],[f9094,f898])).
% 201.19/25.85 fof(f9306,definition,(
% 201.19/25.85 sQ661_spl <=> (less_or_equal(additive_inverse(additive_inverse(additive_identity)),additive_inverse(additive_inverse(additive_identity))))),
% 201.19/25.85 introduced(definition,[new_symbols(definition,[sQ661_spl])],[split_symbol_definition])).
% 201.19/25.85 fof(f9309,plain,(
% 201.19/25.85 sQ661_spl),
% 201.19/25.85 inference(split_clause,[status(thm)],[f9286,f9306])).
% 201.19/25.85 fof(f9622,plain,(
% 201.19/25.85 ![X0]: (product(X0,multiplicative_identity,v)|~product(X0,b,multiplicative_inverse(a))|~sQ23_spl|~sQ24_spl)),
% 201.19/25.85 inference(resolution,[status(thm)],[f8611,f1312])).
% 201.19/25.85 fof(f11716,plain,(
% 201.19/25.85 ![X0]: (product(X0,b,multiplicative_inverse(a))|~product(X0,u,multiplicative_identity)|~sQ12_spl|~sQ24_spl)),
% 201.19/25.85 inference(resolution,[status(thm)],[f1327,f5031])).
% 201.19/25.85 fof(f13365,plain,(
% 201.19/25.85 ![X0]: (less_or_equal(X0,add(v,v))|less_or_equal(add(v,v),X0)|~defined(X0))),
% 201.19/25.85 inference(resolution,[status(thm)],[f6164,f70])).
% 201.19/25.85 fof(f13595,plain,(
% 201.19/25.85 ![X0]: (less_or_equal(X0,add(u,v))|less_or_equal(add(u,v),X0)|~defined(X0))),
% 201.19/25.85 inference(resolution,[status(thm)],[f6165,f70])).
% 201.19/25.85 fof(f14082,plain,(
% 201.19/25.85 less_or_equal(add(v,v),add(v,v))|less_or_equal(add(v,v),add(v,v))),
% 201.19/25.85 inference(resolution,[status(thm)],[f13365,f6164])).
% 201.19/25.85 fof(f14114,definition,(
% 201.19/25.85 sQ1004_spl <=> (less_or_equal(add(v,v),add(v,v)))),
% 201.19/25.85 introduced(definition,[new_symbols(definition,[sQ1004_spl])],[split_symbol_definition])).
% 201.19/25.85 fof(f14117,plain,(
% 201.19/25.85 sQ1004_spl),
% 201.19/25.85 inference(split_clause,[status(thm)],[f14082,f14114])).
% 201.19/25.85 fof(f14142,plain,(
% 201.19/25.85 less_or_equal(add(u,v),add(u,v))|less_or_equal(add(u,v),add(u,v))),
% 201.19/25.85 inference(resolution,[status(thm)],[f13595,f6165])).
% 201.19/25.85 fof(f14168,definition,(
% 201.19/25.85 sQ1005_spl <=> (less_or_equal(add(u,v),add(u,v)))),
% 201.19/25.85 introduced(definition,[new_symbols(definition,[sQ1005_spl])],[split_symbol_definition])).
% 201.19/25.85 fof(f14171,plain,(
% 201.19/25.85 sQ1005_spl),
% 201.19/25.85 inference(split_clause,[status(thm)],[f14142,f14168])).
% 201.19/25.85 fof(f14413,plain,(
% 201.19/25.85 sQ441_spl|~sQ443_spl),
% 201.19/25.85 inference(split_clause,[status(thm)],[f6300,f4444,f4451])).
% 201.19/25.85 fof(f15079,plain,(
% 201.19/25.85 ![X0]: (less_or_equal(X0,add(b,v))|less_or_equal(add(b,v),X0)|~defined(X0))),
% 201.19/25.85 inference(resolution,[status(thm)],[f6166,f70])).
% 201.19/25.85 fof(f15292,plain,(
% 201.19/25.85 less_or_equal(add(b,v),add(b,v))|less_or_equal(add(b,v),add(b,v))),
% 201.19/25.85 inference(resolution,[status(thm)],[f15079,f6166])).
% 201.19/25.85 fof(f15319,definition,(
% 201.19/25.85 sQ1068_spl <=> (less_or_equal(add(b,v),add(b,v)))),
% 201.19/25.85 introduced(definition,[new_symbols(definition,[sQ1068_spl])],[split_symbol_definition])).
% 201.19/25.85 fof(f15322,plain,(
% 201.19/25.85 sQ1068_spl),
% 201.19/25.85 inference(split_clause,[status(thm)],[f15292,f15319])).
% 201.19/25.85 fof(f15583,plain,(
% 201.19/25.85 ![X0]: (less_or_equal(X0,add(a,v))|less_or_equal(add(a,v),X0)|~defined(X0))),
% 201.19/25.85 inference(resolution,[status(thm)],[f6167,f70])).
% 201.19/25.85 fof(f15845,plain,(
% 201.19/25.85 ![X0]: (less_or_equal(X0,add(multiplicative_identity,v))|less_or_equal(add(multiplicative_identity,v),X0)|~defined(X0))),
% 201.19/25.85 inference(resolution,[status(thm)],[f6168,f70])).
% 201.19/25.85 fof(f16107,plain,(
% 201.19/25.85 ![X0]: (less_or_equal(X0,add(additive_identity,v))|less_or_equal(add(additive_identity,v),X0)|~defined(X0))),
% 201.19/25.85 inference(resolution,[status(thm)],[f6169,f70])).
% 201.19/25.85 fof(f16369,plain,(
% 201.19/25.85 ![X0]: (less_or_equal(X0,add(v,u))|less_or_equal(add(v,u),X0)|~defined(X0))),
% 201.19/25.85 inference(resolution,[status(thm)],[f6181,f70])).
% 201.19/25.85 fof(f16643,plain,(
% 201.19/25.85 ![X0]: (less_or_equal(X0,add(u,u))|less_or_equal(add(u,u),X0)|~defined(X0))),
% 201.19/25.85 inference(resolution,[status(thm)],[f6182,f70])).
% 201.19/25.85 fof(f16905,plain,(
% 201.19/25.85 ![X0]: (less_or_equal(X0,add(b,u))|less_or_equal(add(b,u),X0)|~defined(X0))),
% 201.19/25.85 inference(resolution,[status(thm)],[f6183,f70])).
% 201.19/25.85 fof(f17167,plain,(
% 201.19/25.85 ![X0]: (less_or_equal(X0,add(a,u))|less_or_equal(add(a,u),X0)|~defined(X0))),
% 201.19/25.85 inference(resolution,[status(thm)],[f6184,f70])).
% 201.19/25.85 fof(f17429,plain,(
% 201.19/25.85 ![X0]: (less_or_equal(X0,add(multiplicative_identity,u))|less_or_equal(add(multiplicative_identity,u),X0)|~defined(X0))),
% 201.19/25.85 inference(resolution,[status(thm)],[f6185,f70])).
% 201.19/25.85 fof(f17691,plain,(
% 201.19/25.85 ![X0]: (less_or_equal(X0,add(additive_identity,u))|less_or_equal(add(additive_identity,u),X0)|~defined(X0))),
% 201.19/25.85 inference(resolution,[status(thm)],[f6186,f70])).
% 201.19/25.85 fof(f17953,plain,(
% 201.19/25.85 ![X0]: (less_or_equal(X0,add(v,b))|less_or_equal(add(v,b),X0)|~defined(X0))),
% 201.19/25.85 inference(resolution,[status(thm)],[f6213,f70])).
% 201.19/25.85 fof(f18188,plain,(
% 201.19/25.85 less_or_equal(add(a,v),add(a,v))|less_or_equal(add(a,v),add(a,v))),
% 201.19/25.85 inference(resolution,[status(thm)],[f15583,f6167])).
% 201.19/25.85 fof(f18255,definition,(
% 201.19/25.85 sQ1649_spl <=> (less_or_equal(add(a,v),add(a,v)))),
% 201.19/25.85 introduced(definition,[new_symbols(definition,[sQ1649_spl])],[split_symbol_definition])).
% 201.19/25.85 fof(f18258,plain,(
% 201.19/25.85 sQ1649_spl),
% 201.19/25.85 inference(split_clause,[status(thm)],[f18188,f18255])).
% 201.19/25.85 fof(f18317,plain,(
% 201.19/25.85 less_or_equal(add(multiplicative_identity,v),add(multiplicative_identity,v))|less_or_equal(add(multiplicative_identity,v),add(multiplicative_identity,v))),
% 201.19/25.85 inference(resolution,[status(thm)],[f15845,f6168])).
% 201.19/25.85 fof(f18372,definition,(
% 201.19/25.85 sQ1664_spl <=> (less_or_equal(add(multiplicative_identity,v),add(multiplicative_identity,v)))),
% 201.19/25.85 introduced(definition,[new_symbols(definition,[sQ1664_spl])],[split_symbol_definition])).
% 201.19/25.85 fof(f18375,plain,(
% 201.19/25.85 sQ1664_spl),
% 201.19/25.85 inference(split_clause,[status(thm)],[f18317,f18372])).
% 201.19/25.85 fof(f18440,plain,(
% 201.19/25.85 less_or_equal(add(additive_identity,v),add(additive_identity,v))|less_or_equal(add(additive_identity,v),add(additive_identity,v))),
% 201.19/25.85 inference(resolution,[status(thm)],[f16107,f6169])).
% 201.19/25.85 fof(f18483,definition,(
% 201.19/25.85 sQ1677_spl <=> (less_or_equal(add(additive_identity,v),add(additive_identity,v)))),
% 201.19/25.85 introduced(definition,[new_symbols(definition,[sQ1677_spl])],[split_symbol_definition])).
% 201.19/25.85 fof(f18486,plain,(
% 201.19/25.85 sQ1677_spl),
% 201.19/25.85 inference(split_clause,[status(thm)],[f18440,f18483])).
% 201.19/25.85 fof(f18569,plain,(
% 201.19/25.85 less_or_equal(add(v,u),add(v,u))|less_or_equal(add(v,u),add(v,u))),
% 201.19/25.85 inference(resolution,[status(thm)],[f16369,f6181])).
% 201.19/25.85 fof(f18642,definition,(
% 201.19/25.85 sQ1702_spl <=> (less_or_equal(add(v,u),add(v,u)))),
% 201.19/25.85 introduced(definition,[new_symbols(definition,[sQ1702_spl])],[split_symbol_definition])).
% 201.19/25.85 fof(f18645,plain,(
% 201.19/25.85 sQ1702_spl),
% 201.19/25.85 inference(split_clause,[status(thm)],[f18569,f18642])).
% 201.19/25.85 fof(f18679,plain,(
% 201.19/25.85 less_or_equal(add(u,u),add(u,u))|less_or_equal(add(u,u),add(u,u))),
% 201.19/25.85 inference(resolution,[status(thm)],[f16643,f6182])).
% 201.19/25.85 fof(f18740,definition,(
% 201.19/25.85 sQ1711_spl <=> (less_or_equal(add(u,u),add(u,u)))),
% 201.19/25.85 introduced(definition,[new_symbols(definition,[sQ1711_spl])],[split_symbol_definition])).
% 201.19/25.85 fof(f18743,plain,(
% 201.19/25.85 sQ1711_spl),
% 201.19/25.85 inference(split_clause,[status(thm)],[f18679,f18740])).
% 201.19/25.85 fof(f18784,plain,(
% 201.19/25.85 less_or_equal(add(b,u),add(b,u))|less_or_equal(add(b,u),add(b,u))),
% 201.19/25.85 inference(resolution,[status(thm)],[f16905,f6183])).
% 201.19/25.85 fof(f18839,definition,(
% 201.19/25.85 sQ1720_spl <=> (less_or_equal(add(b,u),add(b,u)))),
% 201.19/25.85 introduced(definition,[new_symbols(definition,[sQ1720_spl])],[split_symbol_definition])).
% 201.19/25.85 fof(f18842,plain,(
% 201.19/25.85 sQ1720_spl),
% 201.19/25.85 inference(split_clause,[status(thm)],[f18784,f18839])).
% 201.19/25.85 fof(f18883,plain,(
% 201.19/25.85 less_or_equal(add(a,u),add(a,u))|less_or_equal(add(a,u),add(a,u))),
% 201.19/25.85 inference(resolution,[status(thm)],[f17167,f6184])).
% 201.19/25.85 fof(f18932,definition,(
% 201.19/25.85 sQ1727_spl <=> (less_or_equal(add(a,u),add(a,u)))),
% 201.19/25.85 introduced(definition,[new_symbols(definition,[sQ1727_spl])],[split_symbol_definition])).
% 201.19/25.85 fof(f18935,plain,(
% 201.19/25.85 sQ1727_spl),
% 201.19/25.85 inference(split_clause,[status(thm)],[f18883,f18932])).
% 201.19/25.85 fof(f18976,plain,(
% 201.19/25.85 less_or_equal(add(multiplicative_identity,u),add(multiplicative_identity,u))|less_or_equal(add(multiplicative_identity,u),add(multiplicative_identity,u))),
% 201.19/25.85 inference(resolution,[status(thm)],[f17429,f6185])).
% 201.19/25.85 fof(f19019,definition,(
% 201.19/25.85 sQ1732_spl <=> (less_or_equal(add(multiplicative_identity,u),add(multiplicative_identity,u)))),
% 201.19/25.85 introduced(definition,[new_symbols(definition,[sQ1732_spl])],[split_symbol_definition])).
% 201.19/25.85 fof(f19022,plain,(
% 201.19/25.85 sQ1732_spl),
% 201.19/25.85 inference(split_clause,[status(thm)],[f18976,f19019])).
% 201.19/25.85 fof(f19063,plain,(
% 201.19/25.85 less_or_equal(add(additive_identity,u),add(additive_identity,u))|less_or_equal(add(additive_identity,u),add(additive_identity,u))),
% 201.19/25.85 inference(resolution,[status(thm)],[f17691,f6186])).
% 201.19/25.85 fof(f19100,definition,(
% 201.19/25.85 sQ1735_spl <=> (less_or_equal(add(additive_identity,u),add(additive_identity,u)))),
% 201.19/25.85 introduced(definition,[new_symbols(definition,[sQ1735_spl])],[split_symbol_definition])).
% 201.19/25.85 fof(f19103,plain,(
% 201.19/25.85 sQ1735_spl),
% 201.19/25.85 inference(split_clause,[status(thm)],[f19063,f19100])).
% 201.19/25.85 fof(f19156,plain,(
% 201.19/25.85 less_or_equal(add(v,b),add(v,b))|less_or_equal(add(v,b),add(v,b))),
% 201.19/25.85 inference(resolution,[status(thm)],[f17953,f6213])).
% 201.19/25.85 fof(f19193,definition,(
% 201.19/25.85 sQ1738_spl <=> (less_or_equal(add(v,b),add(v,b)))),
% 201.19/25.85 introduced(definition,[new_symbols(definition,[sQ1738_spl])],[split_symbol_definition])).
% 201.19/25.85 fof(f19196,plain,(
% 201.19/25.85 sQ1738_spl),
% 201.19/25.85 inference(split_clause,[status(thm)],[f19156,f19193])).
% 201.19/25.85 fof(f21153,plain,(
% 201.19/25.85 ![X0]: (less_or_equal(X0,add(u,b))|less_or_equal(add(u,b),X0)|~defined(X0))),
% 201.19/25.85 inference(resolution,[status(thm)],[f6214,f70])).
% 201.19/25.85 fof(f21503,plain,(
% 201.19/25.85 ![X0]: (less_or_equal(X0,add(b,b))|less_or_equal(add(b,b),X0)|~defined(X0))),
% 201.19/25.85 inference(resolution,[status(thm)],[f6215,f70])).
% 201.19/25.85 fof(f21876,plain,(
% 201.19/25.85 ![X0]: (less_or_equal(X0,add(a,b))|less_or_equal(add(a,b),X0)|~defined(X0))),
% 201.19/25.85 inference(resolution,[status(thm)],[f6216,f70])).
% 201.19/25.85 fof(f22226,plain,(
% 201.19/25.85 ![X0]: (less_or_equal(X0,add(multiplicative_identity,b))|less_or_equal(add(multiplicative_identity,b),X0)|~defined(X0))),
% 201.19/25.85 inference(resolution,[status(thm)],[f6217,f70])).
% 201.19/25.85 fof(f22576,plain,(
% 201.19/25.85 ![X0]: (less_or_equal(X0,add(additive_identity,b))|less_or_equal(add(additive_identity,b),X0)|~defined(X0))),
% 201.19/25.85 inference(resolution,[status(thm)],[f6218,f70])).
% 201.19/25.85 fof(f22926,plain,(
% 201.19/25.85 ![X0]: (less_or_equal(X0,add(v,a))|less_or_equal(add(v,a),X0)|~defined(X0))),
% 201.19/25.85 inference(resolution,[status(thm)],[f6230,f70])).
% 201.19/25.85 fof(f23276,plain,(
% 201.19/25.85 ![X0]: (less_or_equal(X0,add(u,a))|less_or_equal(add(u,a),X0)|~defined(X0))),
% 201.19/25.85 inference(resolution,[status(thm)],[f6231,f70])).
% 201.19/25.85 fof(f23626,plain,(
% 201.19/25.85 ![X0]: (less_or_equal(X0,add(b,a))|less_or_equal(add(b,a),X0)|~defined(X0))),
% 201.19/25.85 inference(resolution,[status(thm)],[f6232,f70])).
% 201.19/25.85 fof(f23930,plain,(
% 201.19/25.85 less_or_equal(add(u,b),add(u,b))|less_or_equal(add(u,b),add(u,b))),
% 201.19/25.85 inference(resolution,[status(thm)],[f21153,f6214])).
% 201.19/25.85 fof(f24012,definition,(
% 201.19/25.85 sQ2486_spl <=> (less_or_equal(add(u,b),add(u,b)))),
% 201.19/25.85 introduced(definition,[new_symbols(definition,[sQ2486_spl])],[split_symbol_definition])).
% 201.19/25.85 fof(f24015,plain,(
% 201.19/25.85 sQ2486_spl),
% 201.19/25.85 inference(split_clause,[status(thm)],[f23930,f24012])).
% 201.19/25.85 fof(f24063,plain,(
% 201.19/25.85 less_or_equal(add(b,b),add(b,b))|less_or_equal(add(b,b),add(b,b))),
% 201.19/25.85 inference(resolution,[status(thm)],[f21503,f6215])).
% 201.19/25.85 fof(f24133,definition,(
% 201.19/25.85 sQ2497_spl <=> (less_or_equal(add(b,b),add(b,b)))),
% 201.19/25.85 introduced(definition,[new_symbols(definition,[sQ2497_spl])],[split_symbol_definition])).
% 201.19/25.85 fof(f24136,plain,(
% 201.19/25.85 sQ2497_spl),
% 201.19/25.85 inference(split_clause,[status(thm)],[f24063,f24133])).
% 201.19/25.85 fof(f24190,plain,(
% 201.19/25.85 less_or_equal(add(a,b),add(a,b))|less_or_equal(add(a,b),add(a,b))),
% 201.19/25.85 inference(resolution,[status(thm)],[f21876,f6216])).
% 201.19/25.85 fof(f24248,definition,(
% 201.19/25.85 sQ2506_spl <=> (less_or_equal(add(a,b),add(a,b)))),
% 201.19/25.85 introduced(definition,[new_symbols(definition,[sQ2506_spl])],[split_symbol_definition])).
% 201.19/25.85 fof(f24251,plain,(
% 201.19/25.85 sQ2506_spl),
% 201.19/25.85 inference(split_clause,[status(thm)],[f24190,f24248])).
% 201.19/25.85 fof(f24312,plain,(
% 201.19/25.85 less_or_equal(add(multiplicative_identity,b),add(multiplicative_identity,b))|less_or_equal(add(multiplicative_identity,b),add(multiplicative_identity,b))),
% 201.19/25.85 inference(resolution,[status(thm)],[f22226,f6217])).
% 201.19/25.85 fof(f24364,definition,(
% 201.19/25.85 sQ2515_spl <=> (less_or_equal(add(multiplicative_identity,b),add(multiplicative_identity,b)))),
% 201.19/25.85 introduced(definition,[new_symbols(definition,[sQ2515_spl])],[split_symbol_definition])).
% 201.19/25.85 fof(f24367,plain,(
% 201.19/25.85 sQ2515_spl),
% 201.19/25.85 inference(split_clause,[status(thm)],[f24312,f24364])).
% 201.19/25.85 fof(f24428,plain,(
% 201.19/25.85 less_or_equal(add(additive_identity,b),add(additive_identity,b))|less_or_equal(add(additive_identity,b),add(additive_identity,b))),
% 201.19/25.85 inference(resolution,[status(thm)],[f22576,f6218])).
% 201.19/25.85 fof(f24474,definition,(
% 201.19/25.85 sQ2522_spl <=> (less_or_equal(add(additive_identity,b),add(additive_identity,b)))),
% 201.19/25.85 introduced(definition,[new_symbols(definition,[sQ2522_spl])],[split_symbol_definition])).
% 201.19/25.85 fof(f24477,plain,(
% 201.19/25.85 sQ2522_spl),
% 201.19/25.85 inference(split_clause,[status(thm)],[f24428,f24474])).
% 201.19/25.85 fof(f24558,plain,(
% 201.19/25.85 less_or_equal(add(v,a),add(v,a))|less_or_equal(add(v,a),add(v,a))),
% 201.19/25.85 inference(resolution,[status(thm)],[f22926,f6230])).
% 201.19/25.85 fof(f24616,definition,(
% 201.19/25.85 sQ2533_spl <=> (less_or_equal(add(v,a),add(v,a)))),
% 201.19/25.85 introduced(definition,[new_symbols(definition,[sQ2533_spl])],[split_symbol_definition])).
% 201.19/25.85 fof(f24619,plain,(
% 201.19/25.85 sQ2533_spl),
% 201.19/25.85 inference(split_clause,[status(thm)],[f24558,f24616])).
% 201.19/25.85 fof(f24661,plain,(
% 201.19/25.85 less_or_equal(add(u,a),add(u,a))|less_or_equal(add(u,a),add(u,a))),
% 201.19/25.85 inference(resolution,[status(thm)],[f23276,f6231])).
% 201.19/25.85 fof(f24713,definition,(
% 201.19/25.85 sQ2536_spl <=> (less_or_equal(add(u,a),add(u,a)))),
% 201.19/25.85 introduced(definition,[new_symbols(definition,[sQ2536_spl])],[split_symbol_definition])).
% 201.19/25.85 fof(f24716,plain,(
% 201.19/25.85 sQ2536_spl),
% 201.19/25.85 inference(split_clause,[status(thm)],[f24661,f24713])).
% 201.19/25.85 fof(f24758,plain,(
% 201.19/25.85 less_or_equal(add(b,a),add(b,a))|less_or_equal(add(b,a),add(b,a))),
% 201.19/25.85 inference(resolution,[status(thm)],[f23626,f6232])).
% 201.19/25.85 fof(f24804,definition,(
% 201.19/25.85 sQ2537_spl <=> (less_or_equal(add(b,a),add(b,a)))),
% 201.19/25.85 introduced(definition,[new_symbols(definition,[sQ2537_spl])],[split_symbol_definition])).
% 201.19/25.85 fof(f24807,plain,(
% 201.19/25.85 sQ2537_spl),
% 201.19/25.85 inference(split_clause,[status(thm)],[f24758,f24804])).
% 201.19/25.85 fof(f25616,plain,(
% 201.19/25.85 ![X0]: (less_or_equal(X0,add(a,a))|less_or_equal(add(a,a),X0)|~defined(X0))),
% 201.19/25.85 inference(resolution,[status(thm)],[f6233,f70])).
% 201.19/25.85 fof(f25973,plain,(
% 201.19/25.85 less_or_equal(add(a,a),add(a,a))|less_or_equal(add(a,a),add(a,a))),
% 201.19/25.85 inference(resolution,[status(thm)],[f25616,f6233])).
% 201.19/25.85 fof(f26020,definition,(
% 201.19/25.85 sQ2633_spl <=> (less_or_equal(add(a,a),add(a,a)))),
% 201.19/25.85 introduced(definition,[new_symbols(definition,[sQ2633_spl])],[split_symbol_definition])).
% 201.19/25.85 fof(f26023,plain,(
% 201.19/25.85 sQ2633_spl),
% 201.19/25.85 inference(split_clause,[status(thm)],[f25973,f26020])).
% 201.19/25.85 fof(f26349,plain,(
% 201.19/25.85 ![X0]: (less_or_equal(X0,add(multiplicative_identity,a))|less_or_equal(add(multiplicative_identity,a),X0)|~defined(X0))),
% 201.19/25.85 inference(resolution,[status(thm)],[f6234,f70])).
% 201.19/25.85 fof(f26771,plain,(
% 201.19/25.85 ![X0]: (less_or_equal(X0,add(additive_identity,a))|less_or_equal(add(additive_identity,a),X0)|~defined(X0))),
% 201.19/25.85 inference(resolution,[status(thm)],[f6235,f70])).
% 201.19/25.85 fof(f27193,plain,(
% 201.19/25.85 ![X0]: (less_or_equal(X0,add(v,multiplicative_identity))|less_or_equal(add(v,multiplicative_identity),X0)|~defined(X0))),
% 201.19/25.85 inference(resolution,[status(thm)],[f6247,f70])).
% 201.19/25.85 fof(f27615,plain,(
% 201.19/25.85 ![X0]: (less_or_equal(X0,add(u,multiplicative_identity))|less_or_equal(add(u,multiplicative_identity),X0)|~defined(X0))),
% 201.19/25.85 inference(resolution,[status(thm)],[f6248,f70])).
% 201.19/25.85 fof(f28060,plain,(
% 201.19/25.85 ![X0]: (less_or_equal(X0,add(b,multiplicative_identity))|less_or_equal(add(b,multiplicative_identity),X0)|~defined(X0))),
% 201.19/25.85 inference(resolution,[status(thm)],[f6249,f70])).
% 201.19/25.85 fof(f28482,plain,(
% 201.19/25.85 ![X0]: (less_or_equal(X0,add(a,multiplicative_identity))|less_or_equal(add(a,multiplicative_identity),X0)|~defined(X0))),
% 201.19/25.85 inference(resolution,[status(thm)],[f6250,f70])).
% 201.19/25.85 fof(f28904,plain,(
% 201.19/25.85 ![X0]: (less_or_equal(X0,add(multiplicative_identity,multiplicative_identity))|less_or_equal(add(multiplicative_identity,multiplicative_identity),X0)|~defined(X0))),
% 201.19/25.85 inference(resolution,[status(thm)],[f6251,f70])).
% 201.19/25.85 fof(f29326,plain,(
% 201.19/25.85 ![X0]: (less_or_equal(X0,add(additive_identity,multiplicative_identity))|less_or_equal(add(additive_identity,multiplicative_identity),X0)|~defined(X0))),
% 201.19/25.85 inference(resolution,[status(thm)],[f6252,f70])).
% 201.19/25.85 fof(f29748,plain,(
% 201.19/25.85 ![X0]: (less_or_equal(X0,add(v,additive_identity))|less_or_equal(add(v,additive_identity),X0)|~defined(X0))),
% 201.19/25.85 inference(resolution,[status(thm)],[f6947,f70])).
% 201.19/25.85 fof(f30170,plain,(
% 201.19/25.85 ![X0]: (less_or_equal(X0,add(u,additive_identity))|less_or_equal(add(u,additive_identity),X0)|~defined(X0))),
% 201.19/25.85 inference(resolution,[status(thm)],[f6948,f70])).
% 201.19/25.85 fof(f30530,plain,(
% 201.19/25.85 less_or_equal(add(multiplicative_identity,a),add(multiplicative_identity,a))|less_or_equal(add(multiplicative_identity,a),add(multiplicative_identity,a))),
% 201.19/25.85 inference(resolution,[status(thm)],[f26349,f6234])).
% 201.19/25.85 fof(f30605,definition,(
% 201.19/25.85 sQ3613_spl <=> (less_or_equal(add(multiplicative_identity,a),add(multiplicative_identity,a)))),
% 201.19/25.85 introduced(definition,[new_symbols(definition,[sQ3613_spl])],[split_symbol_definition])).
% 201.19/25.85 fof(f30608,plain,(
% 201.19/25.85 sQ3613_spl),
% 201.19/25.85 inference(split_clause,[status(thm)],[f30530,f30605])).
% 201.19/25.85 fof(f30696,plain,(
% 201.19/25.85 less_or_equal(add(additive_identity,a),add(additive_identity,a))|less_or_equal(add(additive_identity,a),add(additive_identity,a))),
% 201.19/25.85 inference(resolution,[status(thm)],[f26771,f6235])).
% 201.19/25.85 fof(f30759,definition,(
% 201.19/25.85 sQ3628_spl <=> (less_or_equal(add(additive_identity,a),add(additive_identity,a)))),
% 201.19/25.85 introduced(definition,[new_symbols(definition,[sQ3628_spl])],[split_symbol_definition])).
% 201.19/25.85 fof(f30762,plain,(
% 201.19/25.85 sQ3628_spl),
% 201.19/25.85 inference(split_clause,[status(thm)],[f30696,f30759])).
% 201.19/25.85 fof(f30887,plain,(
% 201.19/25.85 less_or_equal(add(v,multiplicative_identity),add(v,multiplicative_identity))|less_or_equal(add(v,multiplicative_identity),add(v,multiplicative_identity))),
% 201.19/25.85 inference(resolution,[status(thm)],[f27193,f6247])).
% 201.19/25.85 fof(f30986,definition,(
% 201.19/25.85 sQ3657_spl <=> (less_or_equal(add(v,multiplicative_identity),add(v,multiplicative_identity)))),
% 201.19/25.85 introduced(definition,[new_symbols(definition,[sQ3657_spl])],[split_symbol_definition])).
% 201.19/25.85 fof(f30989,plain,(
% 201.19/25.85 sQ3657_spl),
% 201.19/25.85 inference(split_clause,[status(thm)],[f30887,f30986])).
% 201.19/25.85 fof(f31040,plain,(
% 201.19/25.85 less_or_equal(add(u,multiplicative_identity),add(u,multiplicative_identity))|less_or_equal(add(u,multiplicative_identity),add(u,multiplicative_identity))),
% 201.19/25.85 inference(resolution,[status(thm)],[f27615,f6248])).
% 201.19/25.85 fof(f31127,definition,(
% 201.19/25.85 sQ3668_spl <=> (less_or_equal(add(u,multiplicative_identity),add(u,multiplicative_identity)))),
% 201.19/25.85 introduced(definition,[new_symbols(definition,[sQ3668_spl])],[split_symbol_definition])).
% 201.19/25.85 fof(f31130,plain,(
% 201.19/25.85 sQ3668_spl),
% 201.19/25.85 inference(split_clause,[status(thm)],[f31040,f31127])).
% 201.19/25.85 fof(f31187,plain,(
% 201.19/25.85 less_or_equal(add(b,multiplicative_identity),add(b,multiplicative_identity))|less_or_equal(add(b,multiplicative_identity),add(b,multiplicative_identity))),
% 201.19/25.85 inference(resolution,[status(thm)],[f28060,f6249])).
% 201.19/25.85 fof(f31262,definition,(
% 201.19/25.85 sQ3677_spl <=> (less_or_equal(add(b,multiplicative_identity),add(b,multiplicative_identity)))),
% 201.19/25.85 introduced(definition,[new_symbols(definition,[sQ3677_spl])],[split_symbol_definition])).
% 201.19/25.85 fof(f31265,plain,(
% 201.19/25.85 sQ3677_spl),
% 201.19/25.85 inference(split_clause,[status(thm)],[f31187,f31262])).
% 201.19/25.85 fof(f31329,plain,(
% 201.19/25.85 less_or_equal(add(a,multiplicative_identity),add(a,multiplicative_identity))|less_or_equal(add(a,multiplicative_identity),add(a,multiplicative_identity))),
% 201.19/25.85 inference(resolution,[status(thm)],[f28482,f6250])).
% 201.19/25.85 fof(f31398,definition,(
% 201.19/25.85 sQ3686_spl <=> (less_or_equal(add(a,multiplicative_identity),add(a,multiplicative_identity)))),
% 201.19/25.85 introduced(definition,[new_symbols(definition,[sQ3686_spl])],[split_symbol_definition])).
% 201.19/25.85 fof(f31401,plain,(
% 201.19/25.85 sQ3686_spl),
% 201.19/25.85 inference(split_clause,[status(thm)],[f31329,f31398])).
% 201.19/25.85 fof(f31465,plain,(
% 201.19/25.85 less_or_equal(add(multiplicative_identity,multiplicative_identity),add(multiplicative_identity,multiplicative_identity))|less_or_equal(add(multiplicative_identity,multiplicative_identity),add(multiplicative_identity,multiplicative_identity))),
% 201.19/25.85 inference(resolution,[status(thm)],[f28904,f6251])).
% 201.19/25.85 fof(f31528,definition,(
% 201.19/25.85 sQ3693_spl <=> (less_or_equal(add(multiplicative_identity,multiplicative_identity),add(multiplicative_identity,multiplicative_identity)))),
% 201.19/25.85 introduced(definition,[new_symbols(definition,[sQ3693_spl])],[split_symbol_definition])).
% 201.19/25.85 fof(f31531,plain,(
% 201.19/25.85 sQ3693_spl),
% 201.19/25.85 inference(split_clause,[status(thm)],[f31465,f31528])).
% 201.19/25.85 fof(f31595,plain,(
% 201.19/25.85 less_or_equal(add(additive_identity,multiplicative_identity),add(additive_identity,multiplicative_identity))|less_or_equal(add(additive_identity,multiplicative_identity),add(additive_identity,multiplicative_identity))),
% 201.19/25.85 inference(resolution,[status(thm)],[f29326,f6252])).
% 201.19/25.85 fof(f31652,definition,(
% 201.19/25.85 sQ3698_spl <=> (less_or_equal(add(additive_identity,multiplicative_identity),add(additive_identity,multiplicative_identity)))),
% 201.19/25.85 introduced(definition,[new_symbols(definition,[sQ3698_spl])],[split_symbol_definition])).
% 201.19/25.85 fof(f31655,plain,(
% 201.19/25.85 sQ3698_spl),
% 201.19/25.85 inference(split_clause,[status(thm)],[f31595,f31652])).
% 201.19/25.85 fof(f31750,plain,(
% 201.19/25.85 less_or_equal(add(v,additive_identity),add(v,additive_identity))|less_or_equal(add(v,additive_identity),add(v,additive_identity))),
% 201.19/25.85 inference(resolution,[status(thm)],[f29748,f6947])).
% 201.19/25.85 fof(f31813,definition,(
% 201.19/25.85 sQ3705_spl <=> (less_or_equal(add(v,additive_identity),add(v,additive_identity)))),
% 201.19/25.85 introduced(definition,[new_symbols(definition,[sQ3705_spl])],[split_symbol_definition])).
% 201.19/25.85 fof(f31816,plain,(
% 201.19/25.85 sQ3705_spl),
% 201.19/25.85 inference(split_clause,[status(thm)],[f31750,f31813])).
% 201.19/25.85 fof(f31867,plain,(
% 201.19/25.85 less_or_equal(add(u,additive_identity),add(u,additive_identity))|less_or_equal(add(u,additive_identity),add(u,additive_identity))),
% 201.19/25.85 inference(resolution,[status(thm)],[f30170,f6948])).
% 201.19/25.85 fof(f31924,definition,(
% 201.19/25.85 sQ3706_spl <=> (less_or_equal(add(u,additive_identity),add(u,additive_identity)))),
% 201.19/25.85 introduced(definition,[new_symbols(definition,[sQ3706_spl])],[split_symbol_definition])).
% 201.19/25.85 fof(f31927,plain,(
% 201.19/25.85 sQ3706_spl),
% 201.19/25.85 inference(split_clause,[status(thm)],[f31867,f31924])).
% 201.19/25.85 fof(f32227,plain,(
% 201.19/25.85 ![X0]: (less_or_equal(X0,add(b,additive_identity))|less_or_equal(add(b,additive_identity),X0)|~defined(X0))),
% 201.19/25.85 inference(resolution,[status(thm)],[f6949,f70])).
% 201.19/25.85 fof(f32732,plain,(
% 201.19/25.85 ![X0]: (less_or_equal(X0,add(a,additive_identity))|less_or_equal(add(a,additive_identity),X0)|~defined(X0))),
% 201.19/25.85 inference(resolution,[status(thm)],[f6950,f70])).
% 201.19/25.85 fof(f33234,plain,(
% 201.19/25.85 ![X0]: (less_or_equal(X0,add(multiplicative_identity,additive_identity))|less_or_equal(add(multiplicative_identity,additive_identity),X0)|~defined(X0))),
% 201.19/25.85 inference(resolution,[status(thm)],[f6951,f70])).
% 201.19/25.85 fof(f33736,plain,(
% 201.19/25.85 ![X0]: (less_or_equal(X0,add(additive_identity,additive_identity))|less_or_equal(add(additive_identity,additive_identity),X0)|~defined(X0))),
% 201.19/25.85 inference(resolution,[status(thm)],[f6952,f70])).
% 201.19/25.85 fof(f34238,plain,(
% 201.19/25.85 ![X0]: (less_or_equal(X0,multiply(v,v))|less_or_equal(multiply(v,v),X0)|~defined(X0))),
% 201.19/25.85 inference(resolution,[status(thm)],[f6965,f70])).
% 201.19/25.85 fof(f34740,plain,(
% 201.19/25.85 ![X0]: (less_or_equal(X0,multiply(u,v))|less_or_equal(multiply(u,v),X0)|~defined(X0))),
% 201.19/25.85 inference(resolution,[status(thm)],[f6966,f70])).
% 201.19/25.85 fof(f35242,plain,(
% 201.19/25.85 ![X0]: (less_or_equal(X0,multiply(b,v))|less_or_equal(multiply(b,v),X0)|~defined(X0))),
% 201.19/25.85 inference(resolution,[status(thm)],[f6967,f70])).
% 201.19/25.85 fof(f35713,plain,(
% 201.19/25.85 less_or_equal(add(b,additive_identity),add(b,additive_identity))|less_or_equal(add(b,additive_identity),add(b,additive_identity))),
% 201.19/25.85 inference(resolution,[status(thm)],[f32227,f6949])).
% 201.19/25.85 fof(f35813,definition,(
% 201.19/25.85 sQ4538_spl <=> (less_or_equal(add(b,additive_identity),add(b,additive_identity)))),
% 201.19/25.85 introduced(definition,[new_symbols(definition,[sQ4538_spl])],[split_symbol_definition])).
% 201.19/25.85 fof(f35816,plain,(
% 201.19/25.85 sQ4538_spl),
% 201.19/25.85 inference(split_clause,[status(thm)],[f35713,f35813])).
% 201.19/25.85 fof(f35874,plain,(
% 201.19/25.85 less_or_equal(add(a,additive_identity),add(a,additive_identity))|less_or_equal(add(a,additive_identity),add(a,additive_identity))),
% 201.19/25.85 inference(resolution,[status(thm)],[f32732,f6950])).
% 201.19/25.85 fof(f35968,definition,(
% 201.19/25.85 sQ4549_spl <=> (less_or_equal(add(a,additive_identity),add(a,additive_identity)))),
% 201.19/25.85 introduced(definition,[new_symbols(definition,[sQ4549_spl])],[split_symbol_definition])).
% 201.19/25.85 fof(f35971,plain,(
% 201.19/25.85 sQ4549_spl),
% 201.19/25.85 inference(split_clause,[status(thm)],[f35874,f35968])).
% 201.19/25.85 fof(f36029,plain,(
% 201.19/25.85 less_or_equal(add(multiplicative_identity,additive_identity),add(multiplicative_identity,additive_identity))|less_or_equal(add(multiplicative_identity,additive_identity),add(multiplicative_identity,additive_identity))),
% 201.19/25.85 inference(resolution,[status(thm)],[f33234,f6951])).
% 201.19/25.85 fof(f36117,definition,(
% 201.19/25.85 sQ4558_spl <=> (less_or_equal(add(multiplicative_identity,additive_identity),add(multiplicative_identity,additive_identity)))),
% 201.19/25.85 introduced(definition,[new_symbols(definition,[sQ4558_spl])],[split_symbol_definition])).
% 201.19/25.85 fof(f36120,plain,(
% 201.19/25.85 sQ4558_spl),
% 201.19/25.85 inference(split_clause,[status(thm)],[f36029,f36117])).
% 201.19/25.85 fof(f36178,plain,(
% 201.19/25.85 less_or_equal(add(additive_identity,additive_identity),add(additive_identity,additive_identity))|less_or_equal(add(additive_identity,additive_identity),add(additive_identity,additive_identity))),
% 201.19/25.85 inference(resolution,[status(thm)],[f33736,f6952])).
% 201.19/25.85 fof(f36260,definition,(
% 201.19/25.85 sQ4565_spl <=> (less_or_equal(add(additive_identity,additive_identity),add(additive_identity,additive_identity)))),
% 201.19/25.85 introduced(definition,[new_symbols(definition,[sQ4565_spl])],[split_symbol_definition])).
% 201.19/25.85 fof(f36263,plain,(
% 201.19/25.85 sQ4565_spl),
% 201.19/25.85 inference(split_clause,[status(thm)],[f36178,f36260])).
% 201.19/25.85 fof(f36326,plain,(
% 201.19/25.85 less_or_equal(multiply(v,v),multiply(v,v))|less_or_equal(multiply(v,v),multiply(v,v))),
% 201.19/25.85 inference(resolution,[status(thm)],[f34238,f6965])).
% 201.19/25.85 fof(f36402,definition,(
% 201.19/25.85 sQ4570_spl <=> (less_or_equal(multiply(v,v),multiply(v,v)))),
% 201.19/25.85 introduced(definition,[new_symbols(definition,[sQ4570_spl])],[split_symbol_definition])).
% 201.19/25.85 fof(f36405,plain,(
% 201.19/25.85 sQ4570_spl),
% 201.19/25.85 inference(split_clause,[status(thm)],[f36326,f36402])).
% 201.19/25.85 fof(f36468,plain,(
% 201.19/25.85 less_or_equal(multiply(u,v),multiply(u,v))|less_or_equal(multiply(u,v),multiply(u,v))),
% 201.19/25.85 inference(resolution,[status(thm)],[f34740,f6966])).
% 201.19/25.85 fof(f36538,definition,(
% 201.19/25.85 sQ4573_spl <=> (less_or_equal(multiply(u,v),multiply(u,v)))),
% 201.19/25.85 introduced(definition,[new_symbols(definition,[sQ4573_spl])],[split_symbol_definition])).
% 201.19/25.85 fof(f36541,plain,(
% 201.19/25.85 sQ4573_spl),
% 201.19/25.85 inference(split_clause,[status(thm)],[f36468,f36538])).
% 201.19/25.85 fof(f36604,plain,(
% 201.19/25.85 less_or_equal(multiply(b,v),multiply(b,v))|less_or_equal(multiply(b,v),multiply(b,v))),
% 201.19/25.85 inference(resolution,[status(thm)],[f35242,f6967])).
% 201.19/25.85 fof(f36668,definition,(
% 201.19/25.85 sQ4574_spl <=> (less_or_equal(multiply(b,v),multiply(b,v)))),
% 201.19/25.85 introduced(definition,[new_symbols(definition,[sQ4574_spl])],[split_symbol_definition])).
% 201.19/25.85 fof(f36671,plain,(
% 201.19/25.85 sQ4574_spl),
% 201.19/25.85 inference(split_clause,[status(thm)],[f36604,f36668])).
% 201.19/25.85 fof(f37260,plain,(
% 201.19/25.85 ![X0]: (less_or_equal(X0,multiply(a,v))|less_or_equal(multiply(a,v),X0)|~defined(X0))),
% 201.19/25.85 inference(resolution,[status(thm)],[f6968,f70])).
% 201.19/25.85 fof(f37818,plain,(
% 201.19/25.85 ![X0]: (less_or_equal(X0,multiply(multiplicative_identity,v))|less_or_equal(multiply(multiplicative_identity,v),X0)|~defined(X0))),
% 201.19/25.85 inference(resolution,[status(thm)],[f6969,f70])).
% 201.19/25.85 fof(f38381,plain,(
% 201.19/25.85 ![X0]: (less_or_equal(X0,multiply(additive_identity,v))|less_or_equal(multiply(additive_identity,v),X0)|~defined(X0))),
% 201.19/25.85 inference(resolution,[status(thm)],[f6970,f70])).
% 201.19/25.85 fof(f38980,plain,(
% 201.19/25.85 ![X0]: (less_or_equal(X0,multiply(v,u))|less_or_equal(multiply(v,u),X0)|~defined(X0))),
% 201.19/25.85 inference(resolution,[status(thm)],[f7003,f70])).
% 201.19/25.85 fof(f39538,plain,(
% 201.19/25.85 ![X0]: (less_or_equal(X0,multiply(u,u))|less_or_equal(multiply(u,u),X0)|~defined(X0))),
% 201.19/25.85 inference(resolution,[status(thm)],[f7004,f70])).
% 201.19/25.85 fof(f40096,plain,(
% 201.19/25.85 ![X0]: (less_or_equal(X0,multiply(b,u))|less_or_equal(multiply(b,u),X0)|~defined(X0))),
% 201.19/25.85 inference(resolution,[status(thm)],[f7005,f70])).
% 201.19/25.85 fof(f40570,plain,(
% 201.19/25.85 less_or_equal(multiply(a,v),multiply(a,v))|less_or_equal(multiply(a,v),multiply(a,v))),
% 201.19/25.85 inference(resolution,[status(thm)],[f37260,f6968])).
% 201.19/25.85 fof(f40652,definition,(
% 201.19/25.85 sQ5365_spl <=> (less_or_equal(multiply(a,v),multiply(a,v)))),
% 201.19/25.85 introduced(definition,[new_symbols(definition,[sQ5365_spl])],[split_symbol_definition])).
% 201.19/25.85 fof(f40655,plain,(
% 201.19/25.85 sQ5365_spl),
% 201.19/25.85 inference(split_clause,[status(thm)],[f40570,f40652])).
% 201.19/25.85 fof(f40742,plain,(
% 201.19/25.85 less_or_equal(multiply(multiplicative_identity,v),multiply(multiplicative_identity,v))|less_or_equal(multiply(multiplicative_identity,v),multiply(multiplicative_identity,v))),
% 201.19/25.85 inference(resolution,[status(thm)],[f37818,f6969])).
% 201.19/25.85 fof(f40818,definition,(
% 201.19/25.85 sQ5374_spl <=> (less_or_equal(multiply(multiplicative_identity,v),multiply(multiplicative_identity,v)))),
% 201.19/25.85 introduced(definition,[new_symbols(definition,[sQ5374_spl])],[split_symbol_definition])).
% 195.59/25.87 fof(f40821,plain,(
% 195.59/25.87 sQ5374_spl),
% 195.59/25.87 inference(split_clause,[status(thm)],[f40742,f40818])).
% 195.59/25.87 fof(f40908,plain,(
% 195.59/25.87 less_or_equal(multiply(additive_identity,v),multiply(additive_identity,v))|less_or_equal(multiply(additive_identity,v),multiply(additive_identity,v))),
% 195.59/25.87 inference(resolution,[status(thm)],[f38381,f6970])).
% 195.59/25.87 fof(f40978,definition,(
% 195.59/25.87 sQ5381_spl <=> (less_or_equal(multiply(additive_identity,v),multiply(additive_identity,v)))),
% 195.59/25.87 introduced(definition,[new_symbols(definition,[sQ5381_spl])],[split_symbol_definition])).
% 195.59/25.87 fof(f40981,plain,(
% 195.59/25.87 sQ5381_spl),
% 195.59/25.87 inference(split_clause,[status(thm)],[f40908,f40978])).
% 195.59/25.87 fof(f41076,plain,(
% 195.59/25.87 less_or_equal(multiply(v,u),multiply(v,u))|less_or_equal(multiply(v,u),multiply(v,u))),
% 195.59/25.87 inference(resolution,[status(thm)],[f38980,f7003])).
% 195.59/25.87 fof(f41158,definition,(
% 195.59/25.87 sQ5392_spl <=> (less_or_equal(multiply(v,u),multiply(v,u)))),
% 195.59/25.87 introduced(definition,[new_symbols(definition,[sQ5392_spl])],[split_symbol_definition])).
% 195.59/25.87 fof(f41161,plain,(
% 195.59/25.87 sQ5392_spl),
% 195.59/25.87 inference(split_clause,[status(thm)],[f41076,f41158])).
% 195.59/25.87 fof(f41229,plain,(
% 195.59/25.87 less_or_equal(multiply(u,u),multiply(u,u))|less_or_equal(multiply(u,u),multiply(u,u))),
% 195.59/25.87 inference(resolution,[status(thm)],[f39538,f7004])).
% 195.59/25.87 fof(f41305,definition,(
% 195.59/25.87 sQ5395_spl <=> (less_or_equal(multiply(u,u),multiply(u,u)))),
% 195.59/25.87 introduced(definition,[new_symbols(definition,[sQ5395_spl])],[split_symbol_definition])).
% 195.59/25.87 fof(f41308,plain,(
% 195.59/25.87 sQ5395_spl),
% 195.59/25.87 inference(split_clause,[status(thm)],[f41229,f41305])).
% 195.59/25.87 fof(f41376,plain,(
% 195.59/25.87 less_or_equal(multiply(b,u),multiply(b,u))|less_or_equal(multiply(b,u),multiply(b,u))),
% 195.59/25.87 inference(resolution,[status(thm)],[f40096,f7005])).
% 195.59/25.87 fof(f41446,definition,(
% 195.59/25.87 sQ5396_spl <=> (less_or_equal(multiply(b,u),multiply(b,u)))),
% 195.59/25.87 introduced(definition,[new_symbols(definition,[sQ5396_spl])],[split_symbol_definition])).
% 195.59/25.87 fof(f41449,plain,(
% 195.59/25.87 sQ5396_spl),
% 195.59/25.87 inference(split_clause,[status(thm)],[f41376,f41446])).
% 195.59/25.87 fof(f41797,plain,(
% 195.59/25.87 ![X0]: (less_or_equal(X0,multiply(a,u))|less_or_equal(multiply(a,u),X0)|~defined(X0))),
% 195.59/25.87 inference(resolution,[status(thm)],[f7006,f70])).
% 195.59/25.87 fof(f42403,plain,(
% 195.59/25.87 ![X0]: (less_or_equal(X0,multiply(multiplicative_identity,u))|less_or_equal(multiply(multiplicative_identity,u),X0)|~defined(X0))),
% 195.59/25.87 inference(resolution,[status(thm)],[f7007,f70])).
% 195.59/25.87 fof(f43022,plain,(
% 195.59/25.87 ![X0]: (less_or_equal(X0,multiply(additive_identity,u))|less_or_equal(multiply(additive_identity,u),X0)|~defined(X0))),
% 195.59/25.87 inference(resolution,[status(thm)],[f7008,f70])).
% 195.59/25.87 fof(f43628,plain,(
% 195.59/25.87 ![X0]: (less_or_equal(X0,multiply(v,b))|less_or_equal(multiply(v,b),X0)|~defined(X0))),
% 195.59/25.87 inference(resolution,[status(thm)],[f7020,f70])).
% 195.59/25.87 fof(f44234,plain,(
% 195.59/25.87 ![X0]: (less_or_equal(X0,multiply(u,b))|less_or_equal(multiply(u,b),X0)|~defined(X0))),
% 195.59/25.87 inference(resolution,[status(thm)],[f7021,f70])).
% 195.59/25.87 fof(f44840,plain,(
% 195.59/25.87 ![X0]: (less_or_equal(X0,multiply(b,b))|less_or_equal(multiply(b,b),X0)|~defined(X0))),
% 195.59/25.87 inference(resolution,[status(thm)],[f7022,f70])).
% 195.59/25.87 fof(f45446,plain,(
% 195.59/25.87 ![X0]: (less_or_equal(X0,multiply(a,b))|less_or_equal(multiply(a,b),X0)|~defined(X0))),
% 195.59/25.87 inference(resolution,[status(thm)],[f7023,f70])).
% 195.59/25.87 fof(f46052,plain,(
% 195.59/25.87 ![X0]: (less_or_equal(X0,multiply(multiplicative_identity,b))|less_or_equal(multiply(multiplicative_identity,b),X0)|~defined(X0))),
% 195.59/25.87 inference(resolution,[status(thm)],[f7024,f70])).
% 195.59/25.87 fof(f46590,plain,(
% 195.59/25.87 less_or_equal(multiply(a,u),multiply(a,u))|less_or_equal(multiply(a,u),multiply(a,u))),
% 195.59/25.87 inference(resolution,[status(thm)],[f41797,f7006])).
% 195.59/25.87 fof(f46692,definition,(
% 195.59/25.87 sQ6549_spl <=> (less_or_equal(multiply(a,u),multiply(a,u)))),
% 195.59/25.87 introduced(definition,[new_symbols(definition,[sQ6549_spl])],[split_symbol_definition])).
% 195.59/25.87 fof(f46695,plain,(
% 195.59/25.87 sQ6549_spl),
% 195.59/25.87 inference(split_clause,[status(thm)],[f46590,f46692])).
% 195.59/25.87 fof(f46788,plain,(
% 195.59/25.87 less_or_equal(multiply(multiplicative_identity,u),multiply(multiplicative_identity,u))|less_or_equal(multiply(multiplicative_identity,u),multiply(multiplicative_identity,u))),
% 195.59/25.87 inference(resolution,[status(thm)],[f42403,f7007])).
% 195.59/25.87 fof(f46878,definition,(
% 195.59/25.87 sQ6560_spl <=> (less_or_equal(multiply(multiplicative_identity,u),multiply(multiplicative_identity,u)))),
% 195.59/25.87 introduced(definition,[new_symbols(definition,[sQ6560_spl])],[split_symbol_definition])).
% 195.59/25.87 fof(f46881,plain,(
% 195.59/25.87 sQ6560_spl),
% 195.59/25.87 inference(split_clause,[status(thm)],[f46788,f46878])).
% 195.59/25.87 fof(f46980,plain,(
% 195.59/25.87 less_or_equal(multiply(additive_identity,u),multiply(additive_identity,u))|less_or_equal(multiply(additive_identity,u),multiply(additive_identity,u))),
% 195.59/25.87 inference(resolution,[status(thm)],[f43022,f7008])).
% 195.59/25.87 fof(f47058,definition,(
% 195.59/25.87 sQ6569_spl <=> (less_or_equal(multiply(additive_identity,u),multiply(additive_identity,u)))),
% 195.59/25.87 introduced(definition,[new_symbols(definition,[sQ6569_spl])],[split_symbol_definition])).
% 195.59/25.87 fof(f47061,plain,(
% 195.59/25.87 sQ6569_spl),
% 195.59/25.87 inference(split_clause,[status(thm)],[f46980,f47058])).
% 195.59/25.87 fof(f47183,plain,(
% 195.59/25.87 less_or_equal(multiply(v,b),multiply(v,b))|less_or_equal(multiply(v,b),multiply(v,b))),
% 195.59/25.87 inference(resolution,[status(thm)],[f43628,f7020])).
% 195.59/25.87 fof(f47285,definition,(
% 195.59/25.87 sQ6588_spl <=> (less_or_equal(multiply(v,b),multiply(v,b)))),
% 195.59/25.87 introduced(definition,[new_symbols(definition,[sQ6588_spl])],[split_symbol_definition])).
% 195.59/25.87 fof(f47288,plain,(
% 195.59/25.87 sQ6588_spl),
% 195.59/25.87 inference(split_clause,[status(thm)],[f47183,f47285])).
% 195.59/25.87 fof(f47363,plain,(
% 195.59/25.87 less_or_equal(multiply(u,b),multiply(u,b))|less_or_equal(multiply(u,b),multiply(u,b))),
% 195.59/25.87 inference(resolution,[status(thm)],[f44234,f7021])).
% 195.59/25.87 fof(f47459,definition,(
% 195.59/25.87 sQ6595_spl <=> (less_or_equal(multiply(u,b),multiply(u,b)))),
% 195.59/25.87 introduced(definition,[new_symbols(definition,[sQ6595_spl])],[split_symbol_definition])).
% 195.59/25.87 fof(f47462,plain,(
% 195.59/25.87 sQ6595_spl),
% 195.59/25.87 inference(split_clause,[status(thm)],[f47363,f47459])).
% 195.59/25.87 fof(f47537,plain,(
% 195.59/25.87 less_or_equal(multiply(b,b),multiply(b,b))|less_or_equal(multiply(b,b),multiply(b,b))),
% 195.59/25.87 inference(resolution,[status(thm)],[f44840,f7022])).
% 195.59/25.87 fof(f47627,definition,(
% 195.59/25.87 sQ6600_spl <=> (less_or_equal(multiply(b,b),multiply(b,b)))),
% 195.59/25.87 introduced(definition,[new_symbols(definition,[sQ6600_spl])],[split_symbol_definition])).
% 195.59/25.87 fof(f47630,plain,(
% 195.59/25.87 sQ6600_spl),
% 195.59/25.87 inference(split_clause,[status(thm)],[f47537,f47627])).
% 195.59/25.87 fof(f47705,plain,(
% 195.59/25.87 less_or_equal(multiply(a,b),multiply(a,b))|less_or_equal(multiply(a,b),multiply(a,b))),
% 195.59/25.87 inference(resolution,[status(thm)],[f45446,f7023])).
% 195.59/25.87 fof(f47789,definition,(
% 195.59/25.87 sQ6603_spl <=> (less_or_equal(multiply(a,b),multiply(a,b)))),
% 195.59/25.87 introduced(definition,[new_symbols(definition,[sQ6603_spl])],[split_symbol_definition])).
% 195.59/25.87 fof(f47792,plain,(
% 195.59/25.87 sQ6603_spl),
% 195.59/25.87 inference(split_clause,[status(thm)],[f47705,f47789])).
% 195.59/25.87 fof(f47867,plain,(
% 195.59/25.87 less_or_equal(multiply(multiplicative_identity,b),multiply(multiplicative_identity,b))|less_or_equal(multiply(multiplicative_identity,b),multiply(multiplicative_identity,b))),
% 195.59/25.87 inference(resolution,[status(thm)],[f46052,f7024])).
% 195.59/25.87 fof(f47945,definition,(
% 195.59/25.87 sQ6604_spl <=> (less_or_equal(multiply(multiplicative_identity,b),multiply(multiplicative_identity,b)))),
% 195.59/25.87 introduced(definition,[new_symbols(definition,[sQ6604_spl])],[split_symbol_definition])).
% 195.59/25.87 fof(f47948,plain,(
% 195.59/25.87 sQ6604_spl),
% 195.59/25.87 inference(split_clause,[status(thm)],[f47867,f47945])).
% 195.59/25.87 fof(f48810,plain,(
% 195.59/25.87 ![X0]: (less_or_equal(X0,multiply(additive_identity,b))|less_or_equal(multiply(additive_identity,b),X0)|~defined(X0))),
% 195.59/25.87 inference(resolution,[status(thm)],[f7025,f70])).
% 195.59/25.87 fof(f49472,plain,(
% 195.59/25.87 ![X0]: (less_or_equal(X0,multiply(v,a))|less_or_equal(multiply(v,a),X0)|~defined(X0))),
% 195.59/25.87 inference(resolution,[status(thm)],[f7037,f70])).
% 195.59/25.87 fof(f50134,plain,(
% 195.59/25.87 ![X0]: (less_or_equal(X0,multiply(u,a))|less_or_equal(multiply(u,a),X0)|~defined(X0))),
% 195.59/25.87 inference(resolution,[status(thm)],[f7038,f70])).
% 195.59/25.87 fof(f50796,plain,(
% 195.59/25.87 ![X0]: (less_or_equal(X0,multiply(b,a))|less_or_equal(multiply(b,a),X0)|~defined(X0))),
% 195.59/25.87 inference(resolution,[status(thm)],[f7039,f70])).
% 195.59/25.87 fof(f51458,plain,(
% 195.59/25.87 ![X0]: (less_or_equal(X0,multiply(a,a))|less_or_equal(multiply(a,a),X0)|~defined(X0))),
% 195.59/25.87 inference(resolution,[status(thm)],[f7040,f70])).
% 195.59/25.87 fof(f52260,plain,(
% 195.59/25.87 less_or_equal(multiply(additive_identity,b),multiply(additive_identity,b))|less_or_equal(multiply(additive_identity,b),multiply(additive_identity,b))),
% 195.59/25.87 inference(resolution,[status(thm)],[f48810,f7025])).
% 195.59/25.87 fof(f52342,definition,(
% 195.59/25.87 sQ7391_spl <=> (less_or_equal(multiply(additive_identity,b),multiply(additive_identity,b)))),
% 195.59/25.87 introduced(definition,[new_symbols(definition,[sQ7391_spl])],[split_symbol_definition])).
% 195.59/25.87 fof(f52345,plain,(
% 195.59/25.87 sQ7391_spl),
% 195.59/25.87 inference(split_clause,[status(thm)],[f52260,f52342])).
% 195.59/25.87 fof(f52469,plain,(
% 195.59/25.87 less_or_equal(multiply(v,a),multiply(v,a))|less_or_equal(multiply(v,a),multiply(v,a))),
% 195.59/25.87 inference(resolution,[status(thm)],[f49472,f7037])).
% 195.59/25.87 fof(f52569,definition,(
% 195.59/25.87 sQ7406_spl <=> (less_or_equal(multiply(v,a),multiply(v,a)))),
% 195.59/25.87 introduced(definition,[new_symbols(definition,[sQ7406_spl])],[split_symbol_definition])).
% 195.59/25.87 fof(f52572,plain,(
% 195.59/25.87 sQ7406_spl),
% 195.59/25.87 inference(split_clause,[status(thm)],[f52469,f52569])).
% 195.59/25.87 fof(f52650,plain,(
% 195.59/25.87 less_or_equal(multiply(u,a),multiply(u,a))|less_or_equal(multiply(u,a),multiply(u,a))),
% 195.59/25.87 inference(resolution,[status(thm)],[f50134,f7038])).
% 195.59/25.87 fof(f52744,definition,(
% 195.59/25.87 sQ7411_spl <=> (less_or_equal(multiply(u,a),multiply(u,a)))),
% 195.59/25.87 introduced(definition,[new_symbols(definition,[sQ7411_spl])],[split_symbol_definition])).
% 195.59/25.87 fof(f52747,plain,(
% 195.59/25.87 sQ7411_spl),
% 195.59/25.87 inference(split_clause,[status(thm)],[f52650,f52744])).
% 195.59/25.87 fof(f52825,plain,(
% 195.59/25.87 less_or_equal(multiply(b,a),multiply(b,a))|less_or_equal(multiply(b,a),multiply(b,a))),
% 195.59/25.87 inference(resolution,[status(thm)],[f50796,f7039])).
% 195.59/25.87 fof(f52913,definition,(
% 195.59/25.87 sQ7414_spl <=> (less_or_equal(multiply(b,a),multiply(b,a)))),
% 195.59/25.87 introduced(definition,[new_symbols(definition,[sQ7414_spl])],[split_symbol_definition])).
% 195.59/25.87 fof(f52916,plain,(
% 195.59/25.87 sQ7414_spl),
% 195.59/25.87 inference(split_clause,[status(thm)],[f52825,f52913])).
% 195.59/25.87 fof(f52994,plain,(
% 195.59/25.87 less_or_equal(multiply(a,a),multiply(a,a))|less_or_equal(multiply(a,a),multiply(a,a))),
% 195.59/25.87 inference(resolution,[status(thm)],[f51458,f7040])).
% 195.59/25.87 fof(f53076,definition,(
% 195.59/25.87 sQ7415_spl <=> (less_or_equal(multiply(a,a),multiply(a,a)))),
% 195.59/25.87 introduced(definition,[new_symbols(definition,[sQ7415_spl])],[split_symbol_definition])).
% 195.59/25.87 fof(f53079,plain,(
% 195.59/25.87 sQ7415_spl),
% 195.59/25.87 inference(split_clause,[status(thm)],[f52994,f53076])).
% 195.59/25.87 fof(f55548,plain,(
% 195.59/25.87 ![X0]: (less_or_equal(X0,multiply(multiplicative_identity,a))|less_or_equal(multiply(multiplicative_identity,a),X0)|~defined(X0))),
% 195.59/25.87 inference(resolution,[status(thm)],[f7041,f70])).
% 195.59/25.87 fof(f56439,plain,(
% 195.59/25.87 ![X0]: (less_or_equal(X0,multiply(additive_identity,a))|less_or_equal(multiply(additive_identity,a),X0)|~defined(X0))),
% 195.59/25.87 inference(resolution,[status(thm)],[f7042,f70])).
% 195.59/25.87 fof(f57165,plain,(
% 195.59/25.87 ![X0]: (less_or_equal(X0,multiply(v,multiplicative_identity))|less_or_equal(multiply(v,multiplicative_identity),X0)|~defined(X0))),
% 195.59/25.87 inference(resolution,[status(thm)],[f7419,f70])).
% 195.59/25.87 fof(f57888,plain,(
% 195.59/25.87 ![X0]: (less_or_equal(X0,multiply(u,multiplicative_identity))|less_or_equal(multiply(u,multiplicative_identity),X0)|~defined(X0))),
% 195.59/25.87 inference(resolution,[status(thm)],[f7420,f70])).
% 195.59/25.87 fof(f58611,plain,(
% 195.59/25.87 ![X0]: (less_or_equal(X0,multiply(b,multiplicative_identity))|less_or_equal(multiply(b,multiplicative_identity),X0)|~defined(X0))),
% 195.59/25.87 inference(resolution,[status(thm)],[f7421,f70])).
% 195.59/25.87 fof(f59477,plain,(
% 195.59/25.87 less_or_equal(multiply(multiplicative_identity,a),multiply(multiplicative_identity,a))|less_or_equal(multiply(multiplicative_identity,a),multiply(multiplicative_identity,a))),
% 195.59/25.87 inference(resolution,[status(thm)],[f55548,f7041])).
% 195.59/25.87 fof(f59571,definition,(
% 195.59/25.87 sQ8275_spl <=> (less_or_equal(multiply(multiplicative_identity,a),multiply(multiplicative_identity,a)))),
% 195.59/25.87 introduced(definition,[new_symbols(definition,[sQ8275_spl])],[split_symbol_definition])).
% 195.59/25.87 fof(f59574,plain,(
% 195.59/25.87 sQ8275_spl),
% 195.59/25.87 inference(split_clause,[status(thm)],[f59477,f59571])).
% 195.59/25.87 fof(f59676,plain,(
% 195.59/25.87 less_or_equal(multiply(additive_identity,a),multiply(additive_identity,a))|less_or_equal(multiply(additive_identity,a),multiply(additive_identity,a))),
% 195.59/25.87 inference(resolution,[status(thm)],[f56439,f7042])).
% 195.59/25.87 fof(f59764,definition,(
% 195.59/25.87 sQ8282_spl <=> (less_or_equal(multiply(additive_identity,a),multiply(additive_identity,a)))),
% 195.59/25.87 introduced(definition,[new_symbols(definition,[sQ8282_spl])],[split_symbol_definition])).
% 195.59/25.87 fof(f59767,plain,(
% 195.59/25.87 sQ8282_spl),
% 195.59/25.87 inference(split_clause,[status(thm)],[f59676,f59764])).
% 195.59/25.87 fof(f59895,plain,(
% 195.59/25.87 less_or_equal(multiply(v,multiplicative_identity),multiply(v,multiplicative_identity))|less_or_equal(multiply(v,multiplicative_identity),multiply(v,multiplicative_identity))),
% 195.59/25.87 inference(resolution,[status(thm)],[f57165,f7419])).
% 195.59/25.87 fof(f59995,definition,(
% 195.59/25.87 sQ8293_spl <=> (less_or_equal(multiply(v,multiplicative_identity),multiply(v,multiplicative_identity)))),
% 195.59/25.87 introduced(definition,[new_symbols(definition,[sQ8293_spl])],[split_symbol_definition])).
% 195.59/25.87 fof(f59998,plain,(
% 195.59/25.87 sQ8293_spl),
% 195.59/25.87 inference(split_clause,[status(thm)],[f59895,f59995])).
% 195.59/25.87 fof(f60081,plain,(
% 195.59/25.87 less_or_equal(multiply(u,multiplicative_identity),multiply(u,multiplicative_identity))|less_or_equal(multiply(u,multiplicative_identity),multiply(u,multiplicative_identity))),
% 195.59/25.87 inference(resolution,[status(thm)],[f57888,f7420])).
% 195.59/25.87 fof(f60175,definition,(
% 195.59/25.87 sQ8296_spl <=> (less_or_equal(multiply(u,multiplicative_identity),multiply(u,multiplicative_identity)))),
% 195.59/25.87 introduced(definition,[new_symbols(definition,[sQ8296_spl])],[split_symbol_definition])).
% 195.59/25.87 fof(f60178,plain,(
% 195.59/25.87 sQ8296_spl),
% 195.59/25.87 inference(split_clause,[status(thm)],[f60081,f60175])).
% 195.59/25.87 fof(f60261,plain,(
% 195.59/25.87 less_or_equal(multiply(b,multiplicative_identity),multiply(b,multiplicative_identity))|less_or_equal(multiply(b,multiplicative_identity),multiply(b,multiplicative_identity))),
% 195.59/25.87 inference(resolution,[status(thm)],[f58611,f7421])).
% 195.59/25.87 fof(f60349,definition,(
% 195.59/25.87 sQ8297_spl <=> (less_or_equal(multiply(b,multiplicative_identity),multiply(b,multiplicative_identity)))),
% 195.59/25.87 introduced(definition,[new_symbols(definition,[sQ8297_spl])],[split_symbol_definition])).
% 195.59/25.87 fof(f60352,plain,(
% 195.59/25.87 sQ8297_spl),
% 195.59/25.87 inference(split_clause,[status(thm)],[f60261,f60349])).
% 195.59/25.87 fof(f61052,plain,(
% 195.59/25.87 ![X0]: (less_or_equal(X0,multiply(a,multiplicative_identity))|less_or_equal(multiply(a,multiplicative_identity),X0)|~defined(X0))),
% 195.59/25.87 inference(resolution,[status(thm)],[f7422,f70])).
% 195.59/25.87 fof(f61820,plain,(
% 195.59/25.87 ![X0]: (less_or_equal(X0,multiply(multiplicative_identity,multiplicative_identity))|less_or_equal(multiply(multiplicative_identity,multiplicative_identity),X0)|~defined(X0))),
% 195.59/25.87 inference(resolution,[status(thm)],[f7423,f70])).
% 195.59/25.87 fof(f62588,plain,(
% 195.59/25.87 ![X0]: (less_or_equal(X0,multiply(additive_identity,multiplicative_identity))|less_or_equal(multiply(additive_identity,multiplicative_identity),X0)|~defined(X0))),
% 195.59/25.87 inference(resolution,[status(thm)],[f7424,f70])).
% 195.59/25.87 fof(f63504,plain,(
% 195.59/25.87 less_or_equal(multiply(a,multiplicative_identity),multiply(a,multiplicative_identity))|less_or_equal(multiply(a,multiplicative_identity),multiply(a,multiplicative_identity))),
% 195.59/25.87 inference(resolution,[status(thm)],[f61052,f7422])).
% 195.59/25.87 fof(f63607,definition,(
% 195.59/25.87 sQ8839_spl <=> (less_or_equal(multiply(a,multiplicative_identity),multiply(a,multiplicative_identity)))),
% 195.59/25.87 introduced(definition,[new_symbols(definition,[sQ8839_spl])],[split_symbol_definition])).
% 195.59/25.87 fof(f63610,plain,(
% 195.59/25.87 sQ8839_spl),
% 195.59/25.87 inference(split_clause,[status(thm)],[f63504,f63607])).
% 195.59/25.87 fof(f63696,plain,(
% 195.59/25.87 less_or_equal(multiply(multiplicative_identity,multiplicative_identity),multiply(multiplicative_identity,multiplicative_identity))|less_or_equal(multiply(multiplicative_identity,multiplicative_identity),multiply(multiplicative_identity,multiplicative_identity))),
% 195.59/25.87 inference(resolution,[status(thm)],[f61820,f7423])).
% 195.59/25.87 fof(f63793,definition,(
% 195.59/25.87 sQ8842_spl <=> (less_or_equal(multiply(multiplicative_identity,multiplicative_identity),multiply(multiplicative_identity,multiplicative_identity)))),
% 195.59/25.87 introduced(definition,[new_symbols(definition,[sQ8842_spl])],[split_symbol_definition])).
% 195.59/25.87 fof(f63796,plain,(
% 195.59/25.87 sQ8842_spl),
% 195.59/25.87 inference(split_clause,[status(thm)],[f63696,f63793])).
% 195.59/25.87 fof(f63882,plain,(
% 195.59/25.87 less_or_equal(multiply(additive_identity,multiplicative_identity),multiply(additive_identity,multiplicative_identity))|less_or_equal(multiply(additive_identity,multiplicative_identity),multiply(additive_identity,multiplicative_identity))),
% 195.59/25.87 inference(resolution,[status(thm)],[f62588,f7424])).
% 195.59/25.87 fof(f63973,definition,(
% 195.59/25.87 sQ8843_spl <=> (less_or_equal(multiply(additive_identity,multiplicative_identity),multiply(additive_identity,multiplicative_identity)))),
% 195.59/25.87 introduced(definition,[new_symbols(definition,[sQ8843_spl])],[split_symbol_definition])).
% 195.59/25.87 fof(f63976,plain,(
% 195.59/25.87 sQ8843_spl),
% 195.59/25.87 inference(split_clause,[status(thm)],[f63882,f63973])).
% 195.59/25.87 fof(f64849,plain,(
% 195.59/25.87 ![X0]: (less_or_equal(X0,multiply(v,additive_identity))|less_or_equal(multiply(v,additive_identity),X0)|~defined(X0))),
% 195.59/25.87 inference(resolution,[status(thm)],[f7436,f70])).
% 195.59/25.87 fof(f65644,plain,(
% 195.59/25.87 ![X0]: (less_or_equal(X0,multiply(u,additive_identity))|less_or_equal(multiply(u,additive_identity),X0)|~defined(X0))),
% 195.59/25.87 inference(resolution,[status(thm)],[f7437,f70])).
% 195.59/25.87 fof(f66439,plain,(
% 195.59/25.87 ![X0]: (less_or_equal(X0,multiply(b,additive_identity))|less_or_equal(multiply(b,additive_identity),X0)|~defined(X0))),
% 195.59/25.87 inference(resolution,[status(thm)],[f7438,f70])).
% 195.59/25.87 fof(f67234,plain,(
% 195.59/25.87 ![X0]: (less_or_equal(X0,multiply(a,additive_identity))|less_or_equal(multiply(a,additive_identity),X0)|~defined(X0))),
% 195.59/25.87 inference(resolution,[status(thm)],[f7439,f70])).
% 195.59/25.87 fof(f68201,plain,(
% 195.59/25.87 less_or_equal(multiply(v,additive_identity),multiply(v,additive_identity))|less_or_equal(multiply(v,additive_identity),multiply(v,additive_identity))),
% 195.59/25.87 inference(resolution,[status(thm)],[f64849,f7436])).
% 195.59/25.87 fof(f68314,definition,(
% 195.59/25.87 sQ9590_spl <=> (less_or_equal(multiply(v,additive_identity),multiply(v,additive_identity)))),
% 195.59/25.87 introduced(definition,[new_symbols(definition,[sQ9590_spl])],[split_symbol_definition])).
% 195.59/25.87 fof(f68317,plain,(
% 195.59/25.87 sQ9590_spl),
% 195.59/25.87 inference(split_clause,[status(thm)],[f68201,f68314])).
% 195.59/25.87 fof(f68406,plain,(
% 195.59/25.87 less_or_equal(multiply(u,additive_identity),multiply(u,additive_identity))|less_or_equal(multiply(u,additive_identity),multiply(u,additive_identity))),
% 195.59/25.87 inference(resolution,[status(thm)],[f65644,f7437])).
% 195.59/25.87 fof(f68513,definition,(
% 195.59/25.87 sQ9595_spl <=> (less_or_equal(multiply(u,additive_identity),multiply(u,additive_identity)))),
% 195.59/25.87 introduced(definition,[new_symbols(definition,[sQ9595_spl])],[split_symbol_definition])).
% 195.59/25.87 fof(f68516,plain,(
% 195.59/25.87 sQ9595_spl),
% 195.59/25.87 inference(split_clause,[status(thm)],[f68406,f68513])).
% 195.59/25.87 fof(f68605,plain,(
% 195.59/25.87 less_or_equal(multiply(b,additive_identity),multiply(b,additive_identity))|less_or_equal(multiply(b,additive_identity),multiply(b,additive_identity))),
% 195.59/25.87 inference(resolution,[status(thm)],[f66439,f7438])).
% 195.59/25.87 fof(f68706,definition,(
% 195.59/25.87 sQ9598_spl <=> (less_or_equal(multiply(b,additive_identity),multiply(b,additive_identity)))),
% 195.59/25.87 introduced(definition,[new_symbols(definition,[sQ9598_spl])],[split_symbol_definition])).
% 195.59/25.87 fof(f68709,plain,(
% 195.59/25.87 sQ9598_spl),
% 195.59/25.87 inference(split_clause,[status(thm)],[f68605,f68706])).
% 195.59/25.87 fof(f68798,plain,(
% 195.59/25.87 less_or_equal(multiply(a,additive_identity),multiply(a,additive_identity))|less_or_equal(multiply(a,additive_identity),multiply(a,additive_identity))),
% 195.59/25.87 inference(resolution,[status(thm)],[f67234,f7439])).
% 195.59/25.87 fof(f68893,definition,(
% 195.59/25.87 sQ9599_spl <=> (less_or_equal(multiply(a,additive_identity),multiply(a,additive_identity)))),
% 144.85/25.95 introduced(definition,[new_symbols(definition,[sQ9599_spl])],[split_symbol_definition])).
% 144.85/25.95 fof(f68896,plain,(
% 144.85/25.95 sQ9599_spl),
% 144.85/25.95 inference(split_clause,[status(thm)],[f68798,f68893])).
% 144.85/25.95 fof(f70835,plain,(
% 144.85/25.95 ![X0]: (less_or_equal(X0,multiply(multiplicative_identity,additive_identity))|less_or_equal(multiply(multiplicative_identity,additive_identity),X0)|~defined(X0))),
% 144.85/25.95 inference(resolution,[status(thm)],[f7440,f70])).
% 144.85/25.95 fof(f71670,plain,(
% 144.85/25.95 ![X0]: (less_or_equal(X0,multiply(additive_identity,additive_identity))|less_or_equal(multiply(additive_identity,additive_identity),X0)|~defined(X0))),
% 144.85/25.95 inference(resolution,[status(thm)],[f7441,f70])).
% 144.85/25.95 fof(f72655,plain,(
% 144.85/25.95 less_or_equal(multiply(multiplicative_identity,additive_identity),multiply(multiplicative_identity,additive_identity))|less_or_equal(multiply(multiplicative_identity,additive_identity),multiply(multiplicative_identity,additive_identity))),
% 144.85/25.95 inference(resolution,[status(thm)],[f70835,f7440])).
% 144.85/25.95 fof(f72758,definition,(
% 144.85/25.95 sQ9994_spl <=> (less_or_equal(multiply(multiplicative_identity,additive_identity),multiply(multiplicative_identity,additive_identity)))),
% 144.85/25.95 introduced(definition,[new_symbols(definition,[sQ9994_spl])],[split_symbol_definition])).
% 144.85/25.95 fof(f72761,plain,(
% 144.85/25.95 sQ9994_spl),
% 144.85/25.95 inference(split_clause,[status(thm)],[f72655,f72758])).
% 144.85/25.95 fof(f72852,plain,(
% 144.85/25.95 less_or_equal(multiply(additive_identity,additive_identity),multiply(additive_identity,additive_identity))|less_or_equal(multiply(additive_identity,additive_identity),multiply(additive_identity,additive_identity))),
% 144.85/25.95 inference(resolution,[status(thm)],[f71670,f7441])).
% 144.85/25.95 fof(f72949,definition,(
% 144.85/25.95 sQ9995_spl <=> (less_or_equal(multiply(additive_identity,additive_identity),multiply(additive_identity,additive_identity)))),
% 144.85/25.95 introduced(definition,[new_symbols(definition,[sQ9995_spl])],[split_symbol_definition])).
% 144.85/25.95 fof(f72952,plain,(
% 144.85/25.95 sQ9995_spl),
% 144.85/25.95 inference(split_clause,[status(thm)],[f72852,f72949])).
% 144.85/25.95 fof(f81343,plain,(
% 144.85/25.95 product(multiplicative_inverse(u),b,multiplicative_inverse(a))|~sQ12_spl|~sQ24_spl|~sQ22_spl),
% 144.85/25.95 inference(resolution,[status(thm)],[f11716,f211])).
% 144.85/25.95 fof(f81345,plain,(
% 144.85/25.95 product(multiplicative_inverse(u),multiplicative_identity,v)|~sQ12_spl|~sQ22_spl|~sQ23_spl|~sQ24_spl),
% 144.85/25.95 inference(resolution,[status(thm)],[f81343,f9622])).
% 144.85/25.95 fof(f81590,plain,(
% 144.85/25.95 product(multiplicative_identity,multiplicative_inverse(u),v)|~sQ12_spl|~sQ22_spl|~sQ23_spl|~sQ24_spl),
% 144.85/25.95 inference(resolution,[status(thm)],[f81345,f49])).
% 144.85/25.95 fof(f81612,plain,(
% 144.85/25.95 $false|~sQ12_spl|~sQ22_spl|~sQ23_spl|~sQ24_spl),
% 144.85/25.95 inference(forward_subsumption_resolution,[status(thm)],[f81590,f83])).
% 144.85/25.95 fof(f81613,plain,(
% 144.85/25.95 ~sQ12_spl|~sQ22_spl|~sQ23_spl|~sQ24_spl),
% 144.85/25.95 inference(contradiction_clause,[status(thm)],[f81612])).
% 144.85/25.95 fof(f83922,plain,(
% 144.85/25.95 sum(u,b,b)|~sQ9_spl),
% 144.85/25.95 inference(resolution,[status(thm)],[f2225,f1835])).
% 144.85/25.95 fof(f83943,plain,(
% 144.85/25.95 sQ443_spl|~sQ9_spl),
% 144.85/25.95 inference(split_clause,[status(thm)],[f83922,f4451,f153])).
% 144.85/25.95 fof(f83946,plain,(
% 144.85/25.95 $false),
% 144.85/25.95 inference(sat_refutation,[status(thm)],[f170,f213,f217,f221,f231,f233,f276,f346,f410,f468,f520,f566,f579,f613,f641,f750,f871,f1002,f1956,f1998,f2034,f3469,f6573,f7372,f8106,f8146,f8262,f9309,f14117,f14171,f14413,f15322,f18258,f18375,f18486,f18645,f18743,f18842,f18935,f19022,f19103,f19196,f24015,f24136,f24251,f24367,f24477,f24619,f24716,f24807,f26023,f30608,f30762,f30989,f31130,f31265,f31401,f31531,f31655,f31816,f31927,f35816,f35971,f36120,f36263,f36405,f36541,f36671,f40655,f40821,f40981,f41161,f41308,f41449,f46695,f46881,f47061,f47288,f47462,f47630,f47792,f47948,f52345,f52572,f52747,f52916,f53079,f59574,f59767,f59998,f60178,f60352,f63610,f63796,f63976,f68317,f68516,f68709,f68896,f72761,f72952,f81613,f83943])).
% 144.85/25.95 % SZS output end CNFRefutation for theBenchmark.p
% 144.85/25.98 % Elapsed time: 25.615113 seconds
% 144.85/25.98 % CPU time: 202.933011 seconds
% 144.85/25.98 % Total memory used: 815.155 MB
% 144.85/25.98 % Net memory used: 760.024 MB
%------------------------------------------------------------------------------