%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : FLD026-3 : 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 : n012.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:20 PM UTC 2026
% Result : Unsatisfiable 131.48s 31.95s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : FLD026-3 : TPTP v9.3.1. Bugfixed v2.1.0.
% 0.00/0.02 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.05/15.33 % Computer : n012.cluster.edu
% 0.05/15.33 % Model : x86_64 x86_64
% 0.05/15.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.05/15.33 % Memory : 8046.5625MB
% 0.05/15.33 % OS : Linux 6.8.0-71-generic
% 0.05/15.33 % CPULimit : 300
% 0.05/15.33 % WCLimit : 300
% 0.05/15.33 % DateTime : Mon Sep 21 15:38:54 UTC 2026
% 0.05/15.34 % CPUTime :
% 0.05/15.34 % Drodi V4.1.1
% 131.48/31.95 % Refutation found
% 131.48/31.95 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 131.48/31.95 % SZS output start CNFRefutation for theBenchmark
% 131.48/31.95 fof(f2,axiom,(
% 131.48/31.95 (![U,Z,W,X,Y,V]: (( sum(U,Z,W)| ~ sum(X,Y,U)| ~ sum(Y,Z,V)| ~ sum(X,V,W) ) ))),
% 131.48/31.95 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 131.48/31.95 fof(f3,axiom,(
% 131.48/31.95 (![X]: (( sum(additive_identity,X,X)| ~ defined(X) ) ))),
% 131.48/31.95 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 131.48/31.95 fof(f6,axiom,(
% 131.48/31.95 (![X,V,W,Y,U,Z]: (( product(X,V,W)| ~ product(X,Y,U)| ~ product(Y,Z,V)| ~ product(U,Z,W) ) ))),
% 131.48/31.95 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 131.48/31.95 fof(f8,axiom,(
% 131.48/31.95 (![X]: (( product(multiplicative_identity,X,X)| ~ defined(X) ) ))),
% 131.48/31.95 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 131.48/31.95 fof(f9,axiom,(
% 131.48/31.95 (![X]: (( product(multiplicative_inverse(X),X,multiplicative_identity)| sum(additive_identity,X,additive_identity)| ~ defined(X) ) ))),
% 131.48/31.95 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 131.48/31.95 fof(f10,axiom,(
% 131.48/31.95 (![Y,X,Z]: (( product(Y,X,Z)| ~ product(X,Y,Z) ) ))),
% 131.48/31.95 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 131.48/31.95 fof(f11,axiom,(
% 131.48/31.95 (![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) ) ))),
% 131.48/31.95 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 131.48/31.95 fof(f13,axiom,(
% 131.48/31.95 (![X,Y]: (( defined(add(X,Y))| ~ defined(X)| ~ defined(Y) ) ))),
% 131.48/31.95 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 131.48/31.95 fof(f14,axiom,(
% 131.48/31.95 defined(additive_identity) ),
% 131.48/31.95 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 131.48/31.95 fof(f15,axiom,(
% 131.48/31.95 (![X]: (( defined(additive_inverse(X))| ~ defined(X) ) ))),
% 131.48/31.95 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 131.48/31.95 fof(f16,axiom,(
% 131.48/31.95 (![X,Y]: (( defined(multiply(X,Y))| ~ defined(X)| ~ defined(Y) ) ))),
% 131.48/31.95 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 131.48/31.95 fof(f17,axiom,(
% 131.48/31.95 defined(multiplicative_identity) ),
% 131.48/31.95 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 131.48/31.95 fof(f18,axiom,(
% 131.48/31.95 (![X]: (( defined(multiplicative_inverse(X))| ~ defined(X)| sum(additive_identity,X,additive_identity) ) ))),
% 131.48/31.95 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 131.48/31.95 fof(f23,axiom,(
% 131.48/31.95 (![X,Y]: (( less_or_equal(X,Y)| less_or_equal(Y,X)| ~ defined(X)| ~ defined(Y) ) ))),
% 131.48/31.95 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 131.48/31.95 fof(f26,axiom,(
% 131.48/31.95 ~ sum(additive_identity,additive_identity,multiplicative_identity) ),
% 131.48/31.95 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 131.48/31.95 fof(f27,hypothesis,(
% 131.48/31.95 defined(a) ),
% 131.48/31.95 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 131.48/31.95 fof(f28,hypothesis,(
% 131.48/31.95 defined(b) ),
% 131.48/31.95 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 131.48/31.95 fof(f29,negated_conjecture,(
% 131.48/31.95 ~ sum(additive_identity,a,additive_identity) ),
% 131.48/31.95 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 131.48/31.95 fof(f30,negated_conjecture,(
% 131.48/31.95 product(multiplicative_identity,a,b) ),
% 131.48/31.95 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 131.48/31.95 fof(f31,negated_conjecture,(
% 131.48/31.95 ~ product(multiplicative_identity,multiplicative_inverse(a),multiplicative_inverse(b)) ),
% 131.48/31.95 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 131.48/31.95 fof(f34,plain,(
% 131.48/31.95 ![W,X,V]: ((![Z,Y]: ((![U]: (sum(U,Z,W)|~sum(X,Y,U)))|~sum(Y,Z,V)))|~sum(X,V,W))),
% 131.48/31.95 inference(miniscoping,[status(thm)],[f2])).
% 131.48/31.95 fof(f35,plain,(
% 131.48/31.95 ![X0,X1,X2,X3,X4,X5]: (sum(X0,X1,X2)|~sum(X3,X4,X0)|~sum(X4,X1,X5)|~sum(X3,X5,X2))),
% 131.48/31.95 inference(cnf_transformation,[status(thm)],[f34])).
% 131.48/31.95 fof(f36,plain,(
% 131.48/31.95 ![X0]: (sum(additive_identity,X0,X0)|~defined(X0))),
% 131.48/31.95 inference(cnf_transformation,[status(thm)],[f3])).
% 131.48/31.95 fof(f39,plain,(
% 131.48/31.95 ![W,U,Z]: ((![V,Y]: ((![X]: (product(X,V,W)|~product(X,Y,U)))|~product(Y,Z,V)))|~product(U,Z,W))),
% 131.48/31.95 inference(miniscoping,[status(thm)],[f6])).
% 131.48/31.95 fof(f40,plain,(
% 131.48/31.95 ![X0,X1,X2,X3,X4,X5]: (product(X0,X1,X2)|~product(X0,X3,X4)|~product(X3,X5,X1)|~product(X4,X5,X2))),
% 131.48/31.95 inference(cnf_transformation,[status(thm)],[f39])).
% 131.48/31.95 fof(f43,plain,(
% 131.48/31.95 ![X0]: (product(multiplicative_identity,X0,X0)|~defined(X0))),
% 131.48/31.95 inference(cnf_transformation,[status(thm)],[f8])).
% 131.48/31.95 fof(f44,plain,(
% 131.48/31.95 ![X0]: (product(multiplicative_inverse(X0),X0,multiplicative_identity)|sum(additive_identity,X0,additive_identity)|~defined(X0))),
% 131.48/31.95 inference(cnf_transformation,[status(thm)],[f9])).
% 131.48/31.95 fof(f45,plain,(
% 131.48/31.95 ![X0,X1,X2]: (product(X0,X1,X2)|~product(X1,X0,X2))),
% 131.48/31.95 inference(cnf_transformation,[status(thm)],[f10])).
% 131.48/31.95 fof(f46,plain,(
% 131.48/31.95 ![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))),
% 131.48/31.95 inference(miniscoping,[status(thm)],[f11])).
% 131.48/31.95 fof(f47,plain,(
% 131.48/31.95 ![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))),
% 131.48/31.95 inference(cnf_transformation,[status(thm)],[f46])).
% 131.48/31.95 fof(f50,plain,(
% 131.48/31.95 ![Y]: ((![X]: (defined(add(X,Y))|~defined(X)))|~defined(Y))),
% 131.48/31.95 inference(miniscoping,[status(thm)],[f13])).
% 131.48/31.95 fof(f51,plain,(
% 131.48/31.95 ![X0,X1]: (defined(add(X0,X1))|~defined(X0)|~defined(X1))),
% 131.48/31.95 inference(cnf_transformation,[status(thm)],[f50])).
% 131.48/31.95 fof(f52,plain,(
% 131.48/31.95 defined(additive_identity)),
% 131.48/31.95 inference(cnf_transformation,[status(thm)],[f14])).
% 131.48/31.95 fof(f53,plain,(
% 131.48/31.95 ![X0]: (defined(additive_inverse(X0))|~defined(X0))),
% 131.48/31.95 inference(cnf_transformation,[status(thm)],[f15])).
% 131.48/31.95 fof(f54,plain,(
% 131.48/31.95 ![Y]: ((![X]: (defined(multiply(X,Y))|~defined(X)))|~defined(Y))),
% 131.48/31.95 inference(miniscoping,[status(thm)],[f16])).
% 131.48/31.95 fof(f55,plain,(
% 131.48/31.95 ![X0,X1]: (defined(multiply(X0,X1))|~defined(X0)|~defined(X1))),
% 131.48/31.95 inference(cnf_transformation,[status(thm)],[f54])).
% 131.48/31.95 fof(f56,plain,(
% 131.48/31.95 defined(multiplicative_identity)),
% 131.48/31.95 inference(cnf_transformation,[status(thm)],[f17])).
% 131.48/31.95 fof(f57,plain,(
% 131.48/31.95 ![X0]: (defined(multiplicative_inverse(X0))|~defined(X0)|sum(additive_identity,X0,additive_identity))),
% 131.48/31.95 inference(cnf_transformation,[status(thm)],[f18])).
% 131.48/31.95 fof(f65,plain,(
% 131.48/31.95 ![Y]: ((![X]: ((less_or_equal(X,Y)|less_or_equal(Y,X))|~defined(X)))|~defined(Y))),
% 131.48/31.95 inference(miniscoping,[status(thm)],[f23])).
% 131.48/31.95 fof(f66,plain,(
% 131.48/31.95 ![X0,X1]: (less_or_equal(X0,X1)|less_or_equal(X1,X0)|~defined(X0)|~defined(X1))),
% 131.48/31.95 inference(cnf_transformation,[status(thm)],[f65])).
% 131.48/31.95 fof(f70,plain,(
% 131.48/31.95 ~sum(additive_identity,additive_identity,multiplicative_identity)),
% 131.48/31.95 inference(cnf_transformation,[status(thm)],[f26])).
% 131.48/31.95 fof(f71,plain,(
% 131.48/31.95 defined(a)),
% 131.48/31.95 inference(cnf_transformation,[status(thm)],[f27])).
% 131.48/31.95 fof(f72,plain,(
% 131.48/31.95 defined(b)),
% 131.48/31.95 inference(cnf_transformation,[status(thm)],[f28])).
% 131.48/31.95 fof(f73,plain,(
% 131.48/31.95 ~sum(additive_identity,a,additive_identity)),
% 131.48/31.95 inference(cnf_transformation,[status(thm)],[f29])).
% 131.48/31.95 fof(f74,plain,(
% 131.48/31.95 product(multiplicative_identity,a,b)),
% 131.48/31.95 inference(cnf_transformation,[status(thm)],[f30])).
% 131.48/31.95 fof(f75,plain,(
% 131.48/31.95 ~product(multiplicative_identity,multiplicative_inverse(a),multiplicative_inverse(b))),
% 131.48/31.95 inference(cnf_transformation,[status(thm)],[f31])).
% 131.48/31.95 fof(f77,plain,(
% 131.48/31.95 sum(additive_identity,additive_identity,additive_identity)),
% 131.48/31.95 inference(resolution,[status(thm)],[f36,f52])).
% 131.48/31.95 fof(f78,plain,(
% 131.48/31.95 sum(additive_identity,a,a)),
% 131.48/31.95 inference(resolution,[status(thm)],[f71,f36])).
% 131.48/31.95 fof(f80,plain,(
% 131.48/31.95 defined(additive_inverse(b))),
% 131.48/31.95 inference(resolution,[status(thm)],[f53,f72])).
% 131.48/31.95 fof(f81,plain,(
% 131.48/31.95 defined(additive_inverse(a))),
% 131.48/31.95 inference(resolution,[status(thm)],[f53,f71])).
% 131.48/31.95 fof(f82,plain,(
% 131.48/31.95 defined(additive_inverse(multiplicative_identity))),
% 131.48/31.95 inference(resolution,[status(thm)],[f53,f56])).
% 131.48/31.95 fof(f83,plain,(
% 131.48/31.95 defined(additive_inverse(additive_identity))),
% 131.48/31.95 inference(resolution,[status(thm)],[f53,f52])).
% 131.48/31.95 fof(f91,plain,(
% 131.48/31.95 product(multiplicative_identity,a,a)),
% 131.48/31.95 inference(resolution,[status(thm)],[f43,f71])).
% 131.48/31.95 fof(f93,plain,(
% 131.48/31.95 product(multiplicative_identity,additive_identity,additive_identity)),
% 131.48/31.95 inference(resolution,[status(thm)],[f43,f52])).
% 131.48/31.95 fof(f94,plain,(
% 131.48/31.95 product(a,multiplicative_identity,b)),
% 131.48/31.95 inference(resolution,[status(thm)],[f45,f74])).
% 131.48/31.95 fof(f95,plain,(
% 131.48/31.95 defined(multiplicative_inverse(b))|sum(additive_identity,b,additive_identity)),
% 131.48/31.95 inference(resolution,[status(thm)],[f57,f72])).
% 131.48/31.95 fof(f99,definition,(
% 131.48/31.95 sQ0_spl <=> (defined(multiplicative_inverse(b)))),
% 131.48/31.95 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 131.48/31.95 fof(f100,plain,(
% 131.48/31.95 defined(multiplicative_inverse(b))|~sQ0_spl),
% 131.48/31.95 inference(component_clause,[status(thm)],[f99])).
% 131.48/31.95 fof(f102,definition,(
% 131.48/31.95 sQ1_spl <=> (sum(additive_identity,b,additive_identity))),
% 131.48/31.95 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 131.48/31.95 fof(f103,plain,(
% 131.48/31.95 sum(additive_identity,b,additive_identity)|~sQ1_spl),
% 131.48/31.95 inference(component_clause,[status(thm)],[f102])).
% 131.48/31.95 fof(f105,plain,(
% 131.48/31.95 sQ0_spl|sQ1_spl),
% 131.48/31.95 inference(split_clause,[status(thm)],[f95,f99,f102])).
% 131.48/31.95 fof(f109,definition,(
% 131.48/31.95 sQ3_spl <=> (sum(additive_identity,a,additive_identity))),
% 131.48/31.95 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 131.48/31.95 fof(f110,plain,(
% 131.48/31.95 sum(additive_identity,a,additive_identity)|~sQ3_spl),
% 131.48/31.95 inference(component_clause,[status(thm)],[f109])).
% 131.48/31.95 fof(f127,plain,(
% 131.48/31.95 product(multiplicative_inverse(b),b,multiplicative_identity)|sum(additive_identity,b,additive_identity)),
% 131.48/31.95 inference(resolution,[status(thm)],[f44,f72])).
% 131.48/31.95 fof(f128,plain,(
% 131.48/31.95 product(multiplicative_inverse(a),a,multiplicative_identity)|sum(additive_identity,a,additive_identity)),
% 131.48/31.95 inference(resolution,[status(thm)],[f44,f71])).
% 131.48/31.95 fof(f131,definition,(
% 131.48/31.95 sQ8_spl <=> (product(multiplicative_inverse(b),b,multiplicative_identity))),
% 131.48/31.95 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 131.48/31.95 fof(f132,plain,(
% 131.48/31.95 product(multiplicative_inverse(b),b,multiplicative_identity)|~sQ8_spl),
% 131.48/31.95 inference(component_clause,[status(thm)],[f131])).
% 131.48/31.95 fof(f134,plain,(
% 131.48/31.95 sQ8_spl|sQ1_spl),
% 131.48/31.95 inference(split_clause,[status(thm)],[f127,f131,f102])).
% 131.48/31.95 fof(f135,definition,(
% 131.48/31.95 sQ9_spl <=> (product(multiplicative_inverse(a),a,multiplicative_identity))),
% 131.48/31.95 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 131.48/31.95 fof(f136,plain,(
% 131.48/31.95 product(multiplicative_inverse(a),a,multiplicative_identity)|~sQ9_spl),
% 131.48/31.95 inference(component_clause,[status(thm)],[f135])).
% 131.48/31.95 fof(f138,plain,(
% 131.48/31.95 sQ9_spl|sQ3_spl),
% 131.48/31.95 inference(split_clause,[status(thm)],[f128,f135,f109])).
% 131.48/31.95 fof(f147,plain,(
% 131.48/31.95 $false|~sQ3_spl),
% 131.48/31.95 inference(forward_subsumption_resolution,[status(thm)],[f110,f73])).
% 131.48/31.95 fof(f148,plain,(
% 131.48/31.95 ~sQ3_spl),
% 131.48/31.95 inference(contradiction_clause,[status(thm)],[f147])).
% 131.48/31.95 fof(f149,plain,(
% 131.48/31.95 ![X0]: (less_or_equal(b,X0)|less_or_equal(X0,b)|~defined(X0))),
% 131.48/31.95 inference(resolution,[status(thm)],[f66,f72])).
% 131.48/31.95 fof(f150,plain,(
% 131.48/31.95 ![X0]: (less_or_equal(a,X0)|less_or_equal(X0,a)|~defined(X0))),
% 131.48/31.95 inference(resolution,[status(thm)],[f66,f71])).
% 131.48/31.95 fof(f151,plain,(
% 131.48/31.95 ![X0]: (less_or_equal(multiplicative_identity,X0)|less_or_equal(X0,multiplicative_identity)|~defined(X0))),
% 131.48/31.95 inference(resolution,[status(thm)],[f66,f56])).
% 131.48/31.95 fof(f152,plain,(
% 131.48/31.95 ![X0]: (less_or_equal(additive_identity,X0)|less_or_equal(X0,additive_identity)|~defined(X0))),
% 131.48/31.95 inference(resolution,[status(thm)],[f66,f52])).
% 131.48/31.95 fof(f153,plain,(
% 131.48/31.95 less_or_equal(b,b)|less_or_equal(b,b)),
% 131.48/31.95 inference(resolution,[status(thm)],[f149,f72])).
% 131.48/31.95 fof(f157,definition,(
% 131.48/31.95 sQ12_spl <=> (less_or_equal(b,b))),
% 131.48/31.95 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 131.48/31.95 fof(f160,plain,(
% 131.48/31.95 sQ12_spl),
% 131.48/31.95 inference(split_clause,[status(thm)],[f153,f157])).
% 131.48/31.95 fof(f183,plain,(
% 131.48/31.95 less_or_equal(a,a)|less_or_equal(a,a)),
% 131.48/31.95 inference(resolution,[status(thm)],[f150,f71])).
% 131.48/31.95 fof(f187,definition,(
% 131.48/31.95 sQ19_spl <=> (less_or_equal(a,a))),
% 131.48/31.95 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 131.48/31.95 fof(f190,plain,(
% 131.48/31.95 sQ19_spl),
% 131.48/31.95 inference(split_clause,[status(thm)],[f183,f187])).
% 131.48/31.95 fof(f207,plain,(
% 131.48/31.95 less_or_equal(multiplicative_identity,multiplicative_identity)|less_or_equal(multiplicative_identity,multiplicative_identity)),
% 131.48/31.95 inference(resolution,[status(thm)],[f151,f56])).
% 131.48/31.95 fof(f211,definition,(
% 131.48/31.95 sQ24_spl <=> (less_or_equal(multiplicative_identity,multiplicative_identity))),
% 131.48/31.95 introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition])).
% 131.48/31.95 fof(f214,plain,(
% 131.48/31.95 sQ24_spl),
% 131.48/31.95 inference(split_clause,[status(thm)],[f207,f211])).
% 131.48/31.95 fof(f225,plain,(
% 131.48/31.95 less_or_equal(additive_identity,additive_identity)|less_or_equal(additive_identity,additive_identity)),
% 131.48/31.95 inference(resolution,[status(thm)],[f152,f52])).
% 131.48/31.95 fof(f229,definition,(
% 131.48/31.95 sQ27_spl <=> (less_or_equal(additive_identity,additive_identity))),
% 131.48/31.95 introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition])).
% 131.48/31.95 fof(f232,plain,(
% 131.48/31.95 sQ27_spl),
% 131.48/31.95 inference(split_clause,[status(thm)],[f225,f229])).
% 131.48/31.95 fof(f237,plain,(
% 131.48/31.95 ![X0,X1,X2]: (product(a,X0,X1)|~product(multiplicative_identity,X2,X0)|~product(b,X2,X1))),
% 131.48/31.95 inference(resolution,[status(thm)],[f94,f40])).
% 131.48/31.95 fof(f244,plain,(
% 131.48/31.95 ![X0]: (less_or_equal(additive_inverse(b),X0)|less_or_equal(X0,additive_inverse(b))|~defined(X0))),
% 131.48/31.95 inference(resolution,[status(thm)],[f80,f66])).
% 131.48/31.95 fof(f249,plain,(
% 131.48/31.95 defined(additive_inverse(additive_inverse(b)))),
% 131.48/31.95 inference(resolution,[status(thm)],[f80,f53])).
% 131.48/31.95 fof(f290,plain,(
% 131.48/31.95 less_or_equal(additive_inverse(b),additive_inverse(b))|less_or_equal(additive_inverse(b),additive_inverse(b))),
% 131.48/31.95 inference(resolution,[status(thm)],[f244,f80])).
% 131.48/31.95 fof(f295,definition,(
% 131.48/31.95 sQ39_spl <=> (less_or_equal(additive_inverse(b),additive_inverse(b)))),
% 131.48/31.95 introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition])).
% 131.48/31.95 fof(f298,plain,(
% 131.48/31.95 sQ39_spl),
% 131.48/31.95 inference(split_clause,[status(thm)],[f290,f295])).
% 131.48/31.95 fof(f308,plain,(
% 131.48/31.95 ![X0]: (less_or_equal(additive_inverse(a),X0)|less_or_equal(X0,additive_inverse(a))|~defined(X0))),
% 131.48/31.95 inference(resolution,[status(thm)],[f81,f66])).
% 131.48/31.95 fof(f313,plain,(
% 131.48/31.95 defined(additive_inverse(additive_inverse(a)))),
% 131.48/31.95 inference(resolution,[status(thm)],[f81,f53])).
% 131.48/31.95 fof(f361,plain,(
% 131.48/31.95 less_or_equal(additive_inverse(a),additive_inverse(a))|less_or_equal(additive_inverse(a),additive_inverse(a))),
% 131.48/31.95 inference(resolution,[status(thm)],[f308,f81])).
% 131.48/31.95 fof(f367,definition,(
% 131.48/31.95 sQ53_spl <=> (less_or_equal(additive_inverse(a),additive_inverse(a)))),
% 131.48/31.95 introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition])).
% 131.48/31.95 fof(f370,plain,(
% 131.48/31.95 sQ53_spl),
% 131.48/31.95 inference(split_clause,[status(thm)],[f361,f367])).
% 131.48/31.95 fof(f382,plain,(
% 131.48/31.95 ![X0]: (less_or_equal(additive_inverse(multiplicative_identity),X0)|less_or_equal(X0,additive_inverse(multiplicative_identity))|~defined(X0))),
% 131.48/31.95 inference(resolution,[status(thm)],[f82,f66])).
% 131.48/31.95 fof(f387,plain,(
% 131.48/31.95 defined(additive_inverse(additive_inverse(multiplicative_identity)))),
% 131.48/31.95 inference(resolution,[status(thm)],[f82,f53])).
% 131.48/31.95 fof(f442,plain,(
% 131.48/31.95 less_or_equal(additive_inverse(multiplicative_identity),additive_inverse(multiplicative_identity))|less_or_equal(additive_inverse(multiplicative_identity),additive_inverse(multiplicative_identity))),
% 131.48/31.95 inference(resolution,[status(thm)],[f382,f82])).
% 131.48/31.95 fof(f449,definition,(
% 131.48/31.95 sQ69_spl <=> (less_or_equal(additive_inverse(multiplicative_identity),additive_inverse(multiplicative_identity)))),
% 131.48/31.95 introduced(definition,[new_symbols(definition,[sQ69_spl])],[split_symbol_definition])).
% 131.48/31.95 fof(f452,plain,(
% 131.48/31.95 sQ69_spl),
% 131.48/31.95 inference(split_clause,[status(thm)],[f442,f449])).
% 131.48/31.95 fof(f466,plain,(
% 131.48/31.95 ![X0]: (less_or_equal(additive_inverse(additive_identity),X0)|less_or_equal(X0,additive_inverse(additive_identity))|~defined(X0))),
% 131.48/31.95 inference(resolution,[status(thm)],[f83,f66])).
% 131.48/31.95 fof(f471,plain,(
% 131.48/31.95 defined(additive_inverse(additive_inverse(additive_identity)))),
% 131.48/31.95 inference(resolution,[status(thm)],[f83,f53])).
% 131.48/31.95 fof(f533,plain,(
% 131.48/31.95 less_or_equal(additive_inverse(additive_identity),additive_inverse(additive_identity))|less_or_equal(additive_inverse(additive_identity),additive_inverse(additive_identity))),
% 131.48/31.95 inference(resolution,[status(thm)],[f466,f83])).
% 131.48/31.95 fof(f541,definition,(
% 131.48/31.95 sQ87_spl <=> (less_or_equal(additive_inverse(additive_identity),additive_inverse(additive_identity)))),
% 131.48/31.95 introduced(definition,[new_symbols(definition,[sQ87_spl])],[split_symbol_definition])).
% 131.48/31.95 fof(f544,plain,(
% 131.48/31.95 sQ87_spl),
% 131.48/31.95 inference(split_clause,[status(thm)],[f533,f541])).
% 131.48/31.95 fof(f560,plain,(
% 131.48/31.95 ![X0,X1,X2]: (sum(additive_identity,X0,X1)|~sum(additive_identity,X0,X2)|~sum(additive_identity,X2,X1))),
% 131.48/31.95 inference(resolution,[status(thm)],[f77,f35])).
% 131.48/31.95 fof(f563,plain,(
% 131.48/31.95 ![X0,X1,X2,X3]: (sum(X0,X1,X2)|~product(a,X3,X2)|~product(additive_identity,X3,X0)|~product(a,X3,X1))),
% 131.48/31.95 inference(resolution,[status(thm)],[f78,f47])).
% 131.48/31.95 fof(f599,plain,(
% 131.48/31.95 product(a,multiplicative_identity,a)),
% 131.48/31.95 inference(resolution,[status(thm)],[f91,f45])).
% 131.48/31.95 fof(f727,plain,(
% 131.48/31.95 product(additive_identity,multiplicative_identity,additive_identity)),
% 131.48/31.95 inference(resolution,[status(thm)],[f93,f45])).
% 131.48/31.95 fof(f742,plain,(
% 131.48/31.95 ![X0,X1,X2]: (product(multiplicative_inverse(a),X0,X1)|~product(a,X2,X0)|~product(multiplicative_identity,X2,X1)|~sQ9_spl)),
% 131.48/31.95 inference(resolution,[status(thm)],[f136,f40])).
% 131.48/31.95 fof(f764,plain,(
% 131.48/31.95 ![X0]: (less_or_equal(additive_inverse(additive_inverse(b)),X0)|less_or_equal(X0,additive_inverse(additive_inverse(b)))|~defined(X0))),
% 131.48/31.95 inference(resolution,[status(thm)],[f249,f66])).
% 131.48/31.95 fof(f846,plain,(
% 131.48/31.95 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)))),
% 131.48/31.95 inference(resolution,[status(thm)],[f764,f249])).
% 131.48/31.95 fof(f856,definition,(
% 131.48/31.95 sQ129_spl <=> (less_or_equal(additive_inverse(additive_inverse(b)),additive_inverse(additive_inverse(b))))),
% 131.48/31.95 introduced(definition,[new_symbols(definition,[sQ129_spl])],[split_symbol_definition])).
% 131.48/31.95 fof(f859,plain,(
% 131.48/31.95 sQ129_spl),
% 131.48/31.95 inference(split_clause,[status(thm)],[f846,f856])).
% 131.48/31.95 fof(f888,plain,(
% 131.48/31.95 ![X0]: (less_or_equal(additive_inverse(additive_inverse(a)),X0)|less_or_equal(X0,additive_inverse(additive_inverse(a)))|~defined(X0))),
% 131.48/31.95 inference(resolution,[status(thm)],[f313,f66])).
% 131.48/31.95 fof(f1005,plain,(
% 131.48/31.95 ![X0]: (defined(add(b,X0))|~defined(X0))),
% 131.48/31.95 inference(resolution,[status(thm)],[f51,f72])).
% 131.48/31.95 fof(f1006,plain,(
% 131.48/31.95 ![X0]: (defined(add(a,X0))|~defined(X0))),
% 131.48/31.95 inference(resolution,[status(thm)],[f51,f71])).
% 131.48/31.95 fof(f1007,plain,(
% 131.48/31.95 ![X0]: (defined(add(multiplicative_identity,X0))|~defined(X0))),
% 131.48/31.95 inference(resolution,[status(thm)],[f51,f56])).
% 131.48/31.95 fof(f1008,plain,(
% 131.48/31.95 ![X0]: (defined(add(additive_identity,X0))|~defined(X0))),
% 131.48/31.95 inference(resolution,[status(thm)],[f51,f52])).
% 131.48/31.95 fof(f1016,plain,(
% 131.48/31.95 ![X0]: (defined(multiply(b,X0))|~defined(X0))),
% 131.48/31.95 inference(resolution,[status(thm)],[f55,f72])).
% 131.48/31.95 fof(f1017,plain,(
% 131.48/31.95 ![X0]: (defined(multiply(a,X0))|~defined(X0))),
% 131.48/31.95 inference(resolution,[status(thm)],[f55,f71])).
% 131.48/31.95 fof(f1018,plain,(
% 131.48/31.95 ![X0]: (defined(multiply(multiplicative_identity,X0))|~defined(X0))),
% 131.48/31.95 inference(resolution,[status(thm)],[f55,f56])).
% 131.48/31.95 fof(f1019,plain,(
% 131.48/31.95 ![X0]: (defined(multiply(additive_identity,X0))|~defined(X0))),
% 131.48/31.95 inference(resolution,[status(thm)],[f55,f52])).
% 131.48/31.95 fof(f1139,plain,(
% 131.48/31.95 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)))),
% 131.48/31.95 inference(resolution,[status(thm)],[f888,f313])).
% 131.48/31.95 fof(f1150,definition,(
% 131.48/31.95 sQ167_spl <=> (less_or_equal(additive_inverse(additive_inverse(a)),additive_inverse(additive_inverse(a))))),
% 131.48/31.95 introduced(definition,[new_symbols(definition,[sQ167_spl])],[split_symbol_definition])).
% 131.48/31.95 fof(f1153,plain,(
% 131.48/31.95 sQ167_spl),
% 131.48/31.95 inference(split_clause,[status(thm)],[f1139,f1150])).
% 131.48/31.95 fof(f1166,plain,(
% 131.48/31.95 defined(add(b,additive_inverse(additive_identity)))),
% 131.48/31.95 inference(resolution,[status(thm)],[f1005,f83])).
% 131.48/31.95 fof(f1167,plain,(
% 131.48/31.95 defined(add(b,additive_inverse(multiplicative_identity)))),
% 131.48/31.95 inference(resolution,[status(thm)],[f1005,f82])).
% 131.48/31.95 fof(f1168,plain,(
% 131.48/31.95 defined(add(b,additive_inverse(a)))),
% 131.48/31.95 inference(resolution,[status(thm)],[f1005,f81])).
% 131.48/31.95 fof(f1169,plain,(
% 131.48/31.95 defined(add(b,additive_inverse(b)))),
% 131.48/31.95 inference(resolution,[status(thm)],[f1005,f80])).
% 131.48/31.95 fof(f1170,plain,(
% 131.48/31.95 defined(add(b,b))),
% 131.48/31.95 inference(resolution,[status(thm)],[f1005,f72])).
% 131.48/31.95 fof(f1171,plain,(
% 131.48/31.95 defined(add(b,a))),
% 131.48/31.95 inference(resolution,[status(thm)],[f1005,f71])).
% 131.48/31.95 fof(f1172,plain,(
% 131.48/31.95 defined(add(b,multiplicative_identity))),
% 131.48/31.95 inference(resolution,[status(thm)],[f1005,f56])).
% 131.48/31.95 fof(f1173,plain,(
% 131.48/31.95 defined(add(b,additive_identity))),
% 131.48/31.95 inference(resolution,[status(thm)],[f1005,f52])).
% 131.48/31.95 fof(f1177,plain,(
% 131.48/31.95 defined(add(a,additive_inverse(additive_identity)))),
% 131.48/31.95 inference(resolution,[status(thm)],[f1006,f83])).
% 131.48/31.95 fof(f1178,plain,(
% 131.48/31.95 defined(add(a,additive_inverse(multiplicative_identity)))),
% 131.48/31.95 inference(resolution,[status(thm)],[f1006,f82])).
% 131.48/31.95 fof(f1179,plain,(
% 131.48/31.95 defined(add(a,additive_inverse(a)))),
% 131.48/31.95 inference(resolution,[status(thm)],[f1006,f81])).
% 131.48/31.95 fof(f1180,plain,(
% 131.48/31.95 defined(add(a,additive_inverse(b)))),
% 131.48/31.95 inference(resolution,[status(thm)],[f1006,f80])).
% 131.48/31.95 fof(f1181,plain,(
% 131.48/31.95 defined(add(a,b))),
% 131.48/31.95 inference(resolution,[status(thm)],[f1006,f72])).
% 131.48/31.95 fof(f1182,plain,(
% 131.48/31.95 defined(add(a,a))),
% 131.48/31.95 inference(resolution,[status(thm)],[f1006,f71])).
% 131.48/31.95 fof(f1183,plain,(
% 131.48/31.95 defined(add(a,multiplicative_identity))),
% 131.48/31.95 inference(resolution,[status(thm)],[f1006,f56])).
% 131.48/31.95 fof(f1184,plain,(
% 131.48/31.95 defined(add(a,additive_identity))),
% 131.48/31.95 inference(resolution,[status(thm)],[f1006,f52])).
% 131.48/31.95 fof(f1188,plain,(
% 131.48/31.95 defined(add(multiplicative_identity,additive_inverse(additive_identity)))),
% 131.48/31.95 inference(resolution,[status(thm)],[f1007,f83])).
% 131.48/31.95 fof(f1189,plain,(
% 131.48/31.95 defined(add(multiplicative_identity,additive_inverse(multiplicative_identity)))),
% 131.48/31.95 inference(resolution,[status(thm)],[f1007,f82])).
% 131.48/31.95 fof(f1190,plain,(
% 131.48/31.95 defined(add(multiplicative_identity,additive_inverse(a)))),
% 131.48/31.95 inference(resolution,[status(thm)],[f1007,f81])).
% 131.48/31.95 fof(f1191,plain,(
% 131.48/31.95 defined(add(multiplicative_identity,additive_inverse(b)))),
% 131.48/31.95 inference(resolution,[status(thm)],[f1007,f80])).
% 131.48/31.95 fof(f1192,plain,(
% 131.48/31.95 defined(add(multiplicative_identity,b))),
% 131.48/31.95 inference(resolution,[status(thm)],[f1007,f72])).
% 131.48/31.95 fof(f1193,plain,(
% 131.48/31.95 defined(add(multiplicative_identity,a))),
% 131.48/31.95 inference(resolution,[status(thm)],[f1007,f71])).
% 131.48/31.95 fof(f1194,plain,(
% 131.48/31.95 defined(add(multiplicative_identity,multiplicative_identity))),
% 131.48/31.95 inference(resolution,[status(thm)],[f1007,f56])).
% 131.48/31.95 fof(f1195,plain,(
% 131.48/31.95 defined(add(multiplicative_identity,additive_identity))),
% 131.48/31.95 inference(resolution,[status(thm)],[f1007,f52])).
% 131.48/31.95 fof(f1199,plain,(
% 131.48/31.95 defined(add(additive_identity,additive_inverse(additive_identity)))),
% 131.48/31.95 inference(resolution,[status(thm)],[f1008,f83])).
% 131.48/31.95 fof(f1200,plain,(
% 131.48/31.95 defined(add(additive_identity,additive_inverse(multiplicative_identity)))),
% 131.48/31.95 inference(resolution,[status(thm)],[f1008,f82])).
% 131.48/31.95 fof(f1201,plain,(
% 131.48/31.95 defined(add(additive_identity,additive_inverse(a)))),
% 131.48/31.95 inference(resolution,[status(thm)],[f1008,f81])).
% 131.48/31.95 fof(f1202,plain,(
% 131.48/31.95 defined(add(additive_identity,additive_inverse(b)))),
% 131.48/31.95 inference(resolution,[status(thm)],[f1008,f80])).
% 131.48/31.95 fof(f1203,plain,(
% 131.48/31.95 defined(add(additive_identity,b))),
% 131.48/31.95 inference(resolution,[status(thm)],[f1008,f72])).
% 131.48/31.95 fof(f1204,plain,(
% 131.48/31.95 defined(add(additive_identity,a))),
% 131.48/31.95 inference(resolution,[status(thm)],[f1008,f71])).
% 131.48/31.95 fof(f1205,plain,(
% 131.48/31.95 defined(add(additive_identity,multiplicative_identity))),
% 131.48/31.95 inference(resolution,[status(thm)],[f1008,f56])).
% 131.48/31.95 fof(f1206,plain,(
% 131.48/31.95 defined(add(additive_identity,additive_identity))),
% 131.48/31.95 inference(resolution,[status(thm)],[f1008,f52])).
% 131.48/31.95 fof(f1210,plain,(
% 131.48/31.95 defined(multiply(b,additive_inverse(additive_identity)))),
% 131.48/31.95 inference(resolution,[status(thm)],[f1016,f83])).
% 131.48/31.95 fof(f1211,plain,(
% 131.48/31.95 defined(multiply(b,additive_inverse(multiplicative_identity)))),
% 131.48/31.95 inference(resolution,[status(thm)],[f1016,f82])).
% 131.48/31.95 fof(f1212,plain,(
% 131.48/31.95 defined(multiply(b,additive_inverse(a)))),
% 131.48/31.95 inference(resolution,[status(thm)],[f1016,f81])).
% 131.48/31.95 fof(f1213,plain,(
% 131.48/31.95 defined(multiply(b,additive_inverse(b)))),
% 131.48/31.95 inference(resolution,[status(thm)],[f1016,f80])).
% 131.48/31.95 fof(f1214,plain,(
% 131.48/31.95 defined(multiply(b,b))),
% 131.48/31.95 inference(resolution,[status(thm)],[f1016,f72])).
% 131.48/31.95 fof(f1215,plain,(
% 131.48/31.95 defined(multiply(b,a))),
% 131.48/31.95 inference(resolution,[status(thm)],[f1016,f71])).
% 131.48/31.95 fof(f1216,plain,(
% 131.48/31.95 defined(multiply(b,multiplicative_identity))),
% 131.48/31.95 inference(resolution,[status(thm)],[f1016,f56])).
% 131.48/31.95 fof(f1217,plain,(
% 131.48/31.95 defined(multiply(b,additive_identity))),
% 131.48/31.95 inference(resolution,[status(thm)],[f1016,f52])).
% 131.48/31.95 fof(f1221,plain,(
% 131.48/31.95 defined(multiply(a,additive_inverse(additive_identity)))),
% 131.48/31.95 inference(resolution,[status(thm)],[f1017,f83])).
% 131.48/31.95 fof(f1222,plain,(
% 131.48/31.95 defined(multiply(a,additive_inverse(multiplicative_identity)))),
% 131.48/31.95 inference(resolution,[status(thm)],[f1017,f82])).
% 131.48/31.95 fof(f1223,plain,(
% 131.48/31.95 defined(multiply(a,additive_inverse(a)))),
% 131.48/31.95 inference(resolution,[status(thm)],[f1017,f81])).
% 131.48/31.95 fof(f1224,plain,(
% 131.48/31.95 defined(multiply(a,additive_inverse(b)))),
% 131.48/31.95 inference(resolution,[status(thm)],[f1017,f80])).
% 131.48/31.95 fof(f1225,plain,(
% 131.48/31.95 defined(multiply(a,b))),
% 131.48/31.95 inference(resolution,[status(thm)],[f1017,f72])).
% 131.48/31.95 fof(f1226,plain,(
% 131.48/31.95 defined(multiply(a,a))),
% 131.48/31.95 inference(resolution,[status(thm)],[f1017,f71])).
% 131.48/31.95 fof(f1227,plain,(
% 131.48/31.95 defined(multiply(a,multiplicative_identity))),
% 131.48/31.95 inference(resolution,[status(thm)],[f1017,f56])).
% 131.48/31.95 fof(f1228,plain,(
% 131.48/31.95 defined(multiply(a,additive_identity))),
% 131.48/31.95 inference(resolution,[status(thm)],[f1017,f52])).
% 131.48/31.95 fof(f1232,plain,(
% 131.48/31.95 defined(multiply(multiplicative_identity,additive_inverse(additive_identity)))),
% 131.48/31.95 inference(resolution,[status(thm)],[f1018,f83])).
% 131.48/31.95 fof(f1233,plain,(
% 131.48/31.95 defined(multiply(multiplicative_identity,additive_inverse(multiplicative_identity)))),
% 131.48/31.95 inference(resolution,[status(thm)],[f1018,f82])).
% 131.48/31.95 fof(f1234,plain,(
% 131.48/31.95 defined(multiply(multiplicative_identity,additive_inverse(a)))),
% 131.48/31.95 inference(resolution,[status(thm)],[f1018,f81])).
% 131.48/31.95 fof(f1235,plain,(
% 131.48/31.95 defined(multiply(multiplicative_identity,additive_inverse(b)))),
% 131.48/31.95 inference(resolution,[status(thm)],[f1018,f80])).
% 131.48/31.95 fof(f1236,plain,(
% 131.48/31.95 defined(multiply(multiplicative_identity,b))),
% 131.48/31.95 inference(resolution,[status(thm)],[f1018,f72])).
% 131.48/31.95 fof(f1237,plain,(
% 131.48/31.95 defined(multiply(multiplicative_identity,a))),
% 131.48/31.95 inference(resolution,[status(thm)],[f1018,f71])).
% 131.48/31.95 fof(f1238,plain,(
% 131.48/31.95 defined(multiply(multiplicative_identity,multiplicative_identity))),
% 131.48/31.95 inference(resolution,[status(thm)],[f1018,f56])).
% 131.48/31.95 fof(f1239,plain,(
% 131.48/31.95 defined(multiply(multiplicative_identity,additive_identity))),
% 131.48/31.95 inference(resolution,[status(thm)],[f1018,f52])).
% 131.48/31.95 fof(f1243,plain,(
% 131.48/31.95 defined(multiply(additive_identity,additive_inverse(additive_identity)))),
% 131.48/31.95 inference(resolution,[status(thm)],[f1019,f83])).
% 131.48/31.95 fof(f1244,plain,(
% 131.48/31.95 defined(multiply(additive_identity,additive_inverse(multiplicative_identity)))),
% 131.48/31.95 inference(resolution,[status(thm)],[f1019,f82])).
% 131.48/31.95 fof(f1245,plain,(
% 131.48/31.95 defined(multiply(additive_identity,additive_inverse(a)))),
% 131.48/31.95 inference(resolution,[status(thm)],[f1019,f81])).
% 131.48/31.95 fof(f1246,plain,(
% 131.48/31.95 defined(multiply(additive_identity,additive_inverse(b)))),
% 131.48/31.95 inference(resolution,[status(thm)],[f1019,f80])).
% 131.48/31.95 fof(f1247,plain,(
% 131.48/31.95 defined(multiply(additive_identity,b))),
% 131.48/31.95 inference(resolution,[status(thm)],[f1019,f72])).
% 131.48/31.95 fof(f1248,plain,(
% 131.48/31.95 defined(multiply(additive_identity,a))),
% 131.48/31.95 inference(resolution,[status(thm)],[f1019,f71])).
% 131.48/31.95 fof(f1249,plain,(
% 131.48/31.95 defined(multiply(additive_identity,multiplicative_identity))),
% 131.48/31.95 inference(resolution,[status(thm)],[f1019,f56])).
% 131.48/31.95 fof(f1250,plain,(
% 131.48/31.95 defined(multiply(additive_identity,additive_identity))),
% 131.48/31.95 inference(resolution,[status(thm)],[f1019,f52])).
% 131.48/31.95 fof(f1274,plain,(
% 131.48/31.95 ![X0]: (less_or_equal(additive_inverse(additive_inverse(multiplicative_identity)),X0)|less_or_equal(X0,additive_inverse(additive_inverse(multiplicative_identity)))|~defined(X0))),
% 131.48/31.95 inference(resolution,[status(thm)],[f387,f66])).
% 131.48/31.95 fof(f1370,plain,(
% 131.48/31.95 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)))),
% 131.48/31.95 inference(resolution,[status(thm)],[f1274,f387])).
% 131.48/31.95 fof(f1382,definition,(
% 131.48/31.95 sQ193_spl <=> (less_or_equal(additive_inverse(additive_inverse(multiplicative_identity)),additive_inverse(additive_inverse(multiplicative_identity))))),
% 131.48/31.95 introduced(definition,[new_symbols(definition,[sQ193_spl])],[split_symbol_definition])).
% 131.48/31.95 fof(f1385,plain,(
% 131.48/31.95 sQ193_spl),
% 131.48/31.95 inference(split_clause,[status(thm)],[f1370,f1382])).
% 131.48/31.95 fof(f1444,plain,(
% 131.48/31.95 ![X0]: (less_or_equal(additive_inverse(additive_inverse(additive_identity)),X0)|less_or_equal(X0,additive_inverse(additive_inverse(additive_identity)))|~defined(X0))),
% 131.48/31.95 inference(resolution,[status(thm)],[f471,f66])).
% 131.48/31.95 fof(f1547,plain,(
% 131.48/31.95 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)))),
% 131.48/31.95 inference(resolution,[status(thm)],[f1444,f471])).
% 131.48/31.95 fof(f1560,definition,(
% 131.48/31.95 sQ225_spl <=> (less_or_equal(additive_inverse(additive_inverse(additive_identity)),additive_inverse(additive_inverse(additive_identity))))),
% 131.48/31.95 introduced(definition,[new_symbols(definition,[sQ225_spl])],[split_symbol_definition])).
% 131.48/31.95 fof(f1563,plain,(
% 131.48/31.95 sQ225_spl),
% 131.48/31.95 inference(split_clause,[status(thm)],[f1547,f1560])).
% 131.48/31.95 fof(f2006,plain,(
% 131.48/31.95 ![X0,X1]: (sum(X0,X1,b)|~product(additive_identity,multiplicative_identity,X0)|~product(a,multiplicative_identity,X1))),
% 131.48/31.95 inference(resolution,[status(thm)],[f563,f94])).
% 131.48/31.95 fof(f2126,plain,(
% 131.48/31.95 ![X0]: (sum(additive_identity,X0,b)|~product(a,multiplicative_identity,X0))),
% 131.48/31.95 inference(resolution,[status(thm)],[f2006,f727])).
% 131.48/31.95 fof(f2127,plain,(
% 131.48/31.95 sum(additive_identity,a,b)),
% 131.48/31.95 inference(resolution,[status(thm)],[f2126,f599])).
% 131.48/31.95 fof(f2130,plain,(
% 131.48/31.95 ![X0]: (sum(additive_identity,a,X0)|~sum(additive_identity,b,X0))),
% 131.48/31.95 inference(resolution,[status(thm)],[f2127,f560])).
% 131.48/31.95 fof(f2140,plain,(
% 131.48/31.95 sum(additive_identity,a,additive_identity)|~sQ1_spl),
% 131.48/31.95 inference(resolution,[status(thm)],[f2130,f103])).
% 131.48/31.95 fof(f2142,plain,(
% 131.48/31.95 sQ3_spl|~sQ1_spl),
% 131.48/31.95 inference(split_clause,[status(thm)],[f2140,f109,f102])).
% 131.48/31.95 fof(f2322,definition,(
% 131.48/31.95 sQ264_spl <=> (sum(additive_identity,additive_identity,multiplicative_identity))),
% 131.48/31.95 introduced(definition,[new_symbols(definition,[sQ264_spl])],[split_symbol_definition])).
% 131.48/31.95 fof(f2323,plain,(
% 131.48/31.95 sum(additive_identity,additive_identity,multiplicative_identity)|~sQ264_spl),
% 131.48/31.95 inference(component_clause,[status(thm)],[f2322])).
% 131.48/31.95 fof(f2363,plain,(
% 131.48/31.95 product(multiplicative_identity,multiplicative_inverse(b),multiplicative_inverse(b))|~sQ0_spl),
% 131.48/31.95 inference(resolution,[status(thm)],[f100,f43])).
% 131.48/31.95 fof(f2477,plain,(
% 131.48/31.95 product(b,multiplicative_inverse(b),multiplicative_identity)|~sQ8_spl),
% 131.48/31.95 inference(resolution,[status(thm)],[f132,f45])).
% 131.48/31.95 fof(f2481,plain,(
% 131.48/31.95 $false|~sQ264_spl),
% 131.48/31.95 inference(forward_subsumption_resolution,[status(thm)],[f2323,f70])).
% 131.48/31.95 fof(f2482,plain,(
% 131.48/31.95 ~sQ264_spl),
% 131.48/31.95 inference(contradiction_clause,[status(thm)],[f2481])).
% 131.48/31.95 fof(f3942,plain,(
% 131.48/31.95 ![X0]: (less_or_equal(add(b,b),X0)|less_or_equal(X0,add(b,b))|~defined(X0))),
% 131.48/31.95 inference(resolution,[status(thm)],[f1170,f66])).
% 131.48/31.95 fof(f4108,plain,(
% 131.48/31.95 ![X0]: (less_or_equal(add(b,a),X0)|less_or_equal(X0,add(b,a))|~defined(X0))),
% 131.48/31.95 inference(resolution,[status(thm)],[f1171,f66])).
% 131.48/31.95 fof(f4318,plain,(
% 131.48/31.95 ![X0]: (less_or_equal(add(b,multiplicative_identity),X0)|less_or_equal(X0,add(b,multiplicative_identity))|~defined(X0))),
% 131.48/31.95 inference(resolution,[status(thm)],[f1172,f66])).
% 131.48/31.95 fof(f4484,plain,(
% 131.48/31.95 ![X0]: (less_or_equal(add(b,additive_identity),X0)|less_or_equal(X0,add(b,additive_identity))|~defined(X0))),
% 131.48/31.95 inference(resolution,[status(thm)],[f1173,f66])).
% 131.48/31.95 fof(f4650,plain,(
% 131.48/31.95 ![X0]: (less_or_equal(add(a,b),X0)|less_or_equal(X0,add(a,b))|~defined(X0))),
% 131.48/31.95 inference(resolution,[status(thm)],[f1181,f66])).
% 131.48/31.95 fof(f4850,plain,(
% 131.48/31.95 less_or_equal(add(b,b),add(b,b))|less_or_equal(add(b,b),add(b,b))),
% 131.48/31.95 inference(resolution,[status(thm)],[f3942,f1170])).
% 131.48/31.95 fof(f4895,definition,(
% 131.48/31.95 sQ514_spl <=> (less_or_equal(add(b,b),add(b,b)))),
% 131.48/31.95 introduced(definition,[new_symbols(definition,[sQ514_spl])],[split_symbol_definition])).
% 131.48/31.95 fof(f4898,plain,(
% 131.48/31.95 sQ514_spl),
% 131.48/31.95 inference(split_clause,[status(thm)],[f4850,f4895])).
% 131.48/31.95 fof(f4918,plain,(
% 131.48/31.95 less_or_equal(add(b,a),add(b,a))|less_or_equal(add(b,a),add(b,a))),
% 131.48/31.95 inference(resolution,[status(thm)],[f4108,f1171])).
% 131.48/31.95 fof(f4957,definition,(
% 131.48/31.95 sQ521_spl <=> (less_or_equal(add(b,a),add(b,a)))),
% 131.48/31.95 introduced(definition,[new_symbols(definition,[sQ521_spl])],[split_symbol_definition])).
% 131.48/31.95 fof(f4960,plain,(
% 131.48/31.95 sQ521_spl),
% 131.48/31.95 inference(split_clause,[status(thm)],[f4918,f4957])).
% 131.48/31.95 fof(f4980,plain,(
% 131.48/31.95 less_or_equal(add(b,multiplicative_identity),add(b,multiplicative_identity))|less_or_equal(add(b,multiplicative_identity),add(b,multiplicative_identity))),
% 131.48/31.95 inference(resolution,[status(thm)],[f4318,f1172])).
% 131.48/31.95 fof(f5013,definition,(
% 131.48/31.95 sQ526_spl <=> (less_or_equal(add(b,multiplicative_identity),add(b,multiplicative_identity)))),
% 131.48/31.95 introduced(definition,[new_symbols(definition,[sQ526_spl])],[split_symbol_definition])).
% 131.48/31.95 fof(f5016,plain,(
% 131.48/31.95 sQ526_spl),
% 131.48/31.95 inference(split_clause,[status(thm)],[f4980,f5013])).
% 131.48/31.95 fof(f5036,plain,(
% 131.48/31.95 less_or_equal(add(b,additive_identity),add(b,additive_identity))|less_or_equal(add(b,additive_identity),add(b,additive_identity))),
% 131.48/31.95 inference(resolution,[status(thm)],[f4484,f1173])).
% 131.48/31.95 fof(f5063,definition,(
% 131.48/31.95 sQ529_spl <=> (less_or_equal(add(b,additive_identity),add(b,additive_identity)))),
% 131.48/31.95 introduced(definition,[new_symbols(definition,[sQ529_spl])],[split_symbol_definition])).
% 131.48/31.95 fof(f5066,plain,(
% 131.48/31.95 sQ529_spl),
% 131.48/31.95 inference(split_clause,[status(thm)],[f5036,f5063])).
% 131.48/31.95 fof(f5086,plain,(
% 131.48/31.95 less_or_equal(add(a,b),add(a,b))|less_or_equal(add(a,b),add(a,b))),
% 131.48/31.95 inference(resolution,[status(thm)],[f4650,f1181])).
% 131.48/31.95 fof(f5107,definition,(
% 131.48/31.95 sQ530_spl <=> (less_or_equal(add(a,b),add(a,b)))),
% 131.48/31.95 introduced(definition,[new_symbols(definition,[sQ530_spl])],[split_symbol_definition])).
% 131.48/31.95 fof(f5110,plain,(
% 131.48/31.95 sQ530_spl),
% 131.48/31.95 inference(split_clause,[status(thm)],[f5086,f5107])).
% 131.48/31.95 fof(f5618,plain,(
% 131.48/31.95 ![X0]: (less_or_equal(add(a,a),X0)|less_or_equal(X0,add(a,a))|~defined(X0))),
% 131.48/31.95 inference(resolution,[status(thm)],[f1182,f66])).
% 131.48/31.95 fof(f5830,plain,(
% 131.48/31.95 ![X0]: (less_or_equal(add(a,multiplicative_identity),X0)|less_or_equal(X0,add(a,multiplicative_identity))|~defined(X0))),
% 131.48/31.95 inference(resolution,[status(thm)],[f1183,f66])).
% 131.48/31.95 fof(f6042,plain,(
% 131.48/31.95 ![X0]: (less_or_equal(add(a,additive_identity),X0)|less_or_equal(X0,add(a,additive_identity))|~defined(X0))),
% 131.48/31.95 inference(resolution,[status(thm)],[f1184,f66])).
% 131.48/31.95 fof(f6353,plain,(
% 131.48/31.95 less_or_equal(add(a,a),add(a,a))|less_or_equal(add(a,a),add(a,a))),
% 131.48/31.95 inference(resolution,[status(thm)],[f5618,f1182])).
% 131.48/31.95 fof(f6389,definition,(
% 131.48/31.95 sQ670_spl <=> (less_or_equal(add(a,a),add(a,a)))),
% 131.48/31.95 introduced(definition,[new_symbols(definition,[sQ670_spl])],[split_symbol_definition])).
% 131.48/31.95 fof(f6392,plain,(
% 131.48/31.95 sQ670_spl),
% 131.48/31.95 inference(split_clause,[status(thm)],[f6353,f6389])).
% 131.48/31.95 fof(f6415,plain,(
% 131.48/31.95 less_or_equal(add(a,multiplicative_identity),add(a,multiplicative_identity))|less_or_equal(add(a,multiplicative_identity),add(a,multiplicative_identity))),
% 131.48/31.95 inference(resolution,[status(thm)],[f5830,f1183])).
% 131.48/31.95 fof(f6445,definition,(
% 131.48/31.95 sQ673_spl <=> (less_or_equal(add(a,multiplicative_identity),add(a,multiplicative_identity)))),
% 131.48/31.95 introduced(definition,[new_symbols(definition,[sQ673_spl])],[split_symbol_definition])).
% 131.48/31.95 fof(f6448,plain,(
% 131.48/31.95 sQ673_spl),
% 131.48/31.95 inference(split_clause,[status(thm)],[f6415,f6445])).
% 131.48/31.95 fof(f6471,plain,(
% 131.48/31.95 less_or_equal(add(a,additive_identity),add(a,additive_identity))|less_or_equal(add(a,additive_identity),add(a,additive_identity))),
% 131.48/31.95 inference(resolution,[status(thm)],[f6042,f1184])).
% 131.48/31.95 fof(f6495,definition,(
% 131.48/31.95 sQ674_spl <=> (less_or_equal(add(a,additive_identity),add(a,additive_identity)))),
% 131.48/31.95 introduced(definition,[new_symbols(definition,[sQ674_spl])],[split_symbol_definition])).
% 131.48/31.95 fof(f6498,plain,(
% 131.48/31.95 sQ674_spl),
% 131.48/31.95 inference(split_clause,[status(thm)],[f6471,f6495])).
% 131.48/31.95 fof(f6939,plain,(
% 131.48/31.95 ![X0]: (less_or_equal(add(multiplicative_identity,b),X0)|less_or_equal(X0,add(multiplicative_identity,b))|~defined(X0))),
% 131.48/31.95 inference(resolution,[status(thm)],[f1192,f66])).
% 131.48/31.95 fof(f7285,plain,(
% 131.48/31.95 ![X0]: (less_or_equal(add(multiplicative_identity,a),X0)|less_or_equal(X0,add(multiplicative_identity,a))|~defined(X0))),
% 131.48/31.95 inference(resolution,[status(thm)],[f1193,f66])).
% 131.48/31.95 fof(f7531,plain,(
% 131.48/31.95 ![X0]: (less_or_equal(add(multiplicative_identity,multiplicative_identity),X0)|less_or_equal(X0,add(multiplicative_identity,multiplicative_identity))|~defined(X0))),
% 131.48/31.95 inference(resolution,[status(thm)],[f1194,f66])).
% 131.48/31.95 fof(f7777,plain,(
% 131.48/31.95 ![X0]: (less_or_equal(add(multiplicative_identity,additive_identity),X0)|less_or_equal(X0,add(multiplicative_identity,additive_identity))|~defined(X0))),
% 131.48/31.95 inference(resolution,[status(thm)],[f1195,f66])).
% 131.48/31.95 fof(f8389,plain,(
% 131.48/31.95 ![X0]: (less_or_equal(add(b,additive_inverse(additive_identity)),X0)|less_or_equal(X0,add(b,additive_inverse(additive_identity)))|~defined(X0))),
% 131.48/31.95 inference(resolution,[status(thm)],[f1166,f66])).
% 131.48/31.95 fof(f8578,plain,(
% 131.48/31.95 less_or_equal(add(multiplicative_identity,b),add(multiplicative_identity,b))|less_or_equal(add(multiplicative_identity,b),add(multiplicative_identity,b))),
% 131.48/31.95 inference(resolution,[status(thm)],[f6939,f1192])).
% 131.48/31.95 fof(f8626,definition,(
% 131.48/31.95 sQ987_spl <=> (less_or_equal(add(multiplicative_identity,b),add(multiplicative_identity,b)))),
% 131.48/31.95 introduced(definition,[new_symbols(definition,[sQ987_spl])],[split_symbol_definition])).
% 131.48/31.95 fof(f8629,plain,(
% 131.48/31.95 sQ987_spl),
% 131.48/31.95 inference(split_clause,[status(thm)],[f8578,f8626])).
% 131.48/31.95 fof(f8670,plain,(
% 131.48/31.95 less_or_equal(add(multiplicative_identity,a),add(multiplicative_identity,a))|less_or_equal(add(multiplicative_identity,a),add(multiplicative_identity,a))),
% 131.48/31.95 inference(resolution,[status(thm)],[f7285,f1193])).
% 131.48/31.95 fof(f8712,definition,(
% 131.48/31.95 sQ996_spl <=> (less_or_equal(add(multiplicative_identity,a),add(multiplicative_identity,a)))),
% 131.48/31.95 introduced(definition,[new_symbols(definition,[sQ996_spl])],[split_symbol_definition])).
% 131.48/31.95 fof(f8715,plain,(
% 131.48/31.95 sQ996_spl),
% 131.48/31.95 inference(split_clause,[status(thm)],[f8670,f8712])).
% 131.48/31.95 fof(f8756,plain,(
% 131.48/31.95 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))),
% 131.48/31.95 inference(resolution,[status(thm)],[f7531,f1194])).
% 131.48/31.95 fof(f8792,definition,(
% 131.48/31.95 sQ1003_spl <=> (less_or_equal(add(multiplicative_identity,multiplicative_identity),add(multiplicative_identity,multiplicative_identity)))),
% 131.48/31.95 introduced(definition,[new_symbols(definition,[sQ1003_spl])],[split_symbol_definition])).
% 131.48/31.95 fof(f8795,plain,(
% 131.48/31.95 sQ1003_spl),
% 131.48/31.95 inference(split_clause,[status(thm)],[f8756,f8792])).
% 131.48/31.95 fof(f8836,plain,(
% 131.48/31.95 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))),
% 131.48/31.95 inference(resolution,[status(thm)],[f7777,f1195])).
% 131.48/31.95 fof(f8866,definition,(
% 131.48/31.95 sQ1008_spl <=> (less_or_equal(add(multiplicative_identity,additive_identity),add(multiplicative_identity,additive_identity)))),
% 131.48/31.95 introduced(definition,[new_symbols(definition,[sQ1008_spl])],[split_symbol_definition])).
% 131.48/31.95 fof(f8869,plain,(
% 131.48/31.95 sQ1008_spl),
% 131.48/31.95 inference(split_clause,[status(thm)],[f8836,f8866])).
% 131.48/31.95 fof(f8988,plain,(
% 131.48/31.95 less_or_equal(add(b,additive_inverse(additive_identity)),add(b,additive_inverse(additive_identity)))|less_or_equal(add(b,additive_inverse(additive_identity)),add(b,additive_inverse(additive_identity)))),
% 131.48/31.95 inference(resolution,[status(thm)],[f8389,f1166])).
% 131.48/31.95 fof(f9018,definition,(
% 131.48/31.95 sQ1016_spl <=> (less_or_equal(add(b,additive_inverse(additive_identity)),add(b,additive_inverse(additive_identity))))),
% 131.48/31.95 introduced(definition,[new_symbols(definition,[sQ1016_spl])],[split_symbol_definition])).
% 131.48/31.95 fof(f9021,plain,(
% 131.48/31.95 sQ1016_spl),
% 131.48/31.95 inference(split_clause,[status(thm)],[f8988,f9018])).
% 131.48/31.95 fof(f9419,plain,(
% 131.48/31.95 ![X0]: (less_or_equal(add(additive_identity,b),X0)|less_or_equal(X0,add(additive_identity,b))|~defined(X0))),
% 131.48/31.95 inference(resolution,[status(thm)],[f1203,f66])).
% 131.48/31.95 fof(f9717,plain,(
% 131.48/31.95 ![X0]: (less_or_equal(add(additive_identity,a),X0)|less_or_equal(X0,add(additive_identity,a))|~defined(X0))),
% 131.48/31.95 inference(resolution,[status(thm)],[f1204,f66])).
% 131.48/31.95 fof(f10015,plain,(
% 131.48/31.95 ![X0]: (less_or_equal(add(b,additive_inverse(multiplicative_identity)),X0)|less_or_equal(X0,add(b,additive_inverse(multiplicative_identity)))|~defined(X0))),
% 131.48/31.95 inference(resolution,[status(thm)],[f1167,f66])).
% 131.48/31.95 fof(f10313,plain,(
% 131.48/31.95 ![X0]: (less_or_equal(add(b,additive_inverse(a)),X0)|less_or_equal(X0,add(b,additive_inverse(a)))|~defined(X0))),
% 131.48/31.95 inference(resolution,[status(thm)],[f1168,f66])).
% 131.48/31.95 fof(f10611,plain,(
% 131.48/31.95 ![X0]: (less_or_equal(add(b,additive_inverse(b)),X0)|less_or_equal(X0,add(b,additive_inverse(b)))|~defined(X0))),
% 131.48/31.95 inference(resolution,[status(thm)],[f1169,f66])).
% 131.48/31.95 fof(f11207,plain,(
% 131.48/31.95 ![X0]: (less_or_equal(add(additive_identity,multiplicative_identity),X0)|less_or_equal(X0,add(additive_identity,multiplicative_identity))|~defined(X0))),
% 131.48/31.95 inference(resolution,[status(thm)],[f1205,f66])).
% 131.48/31.95 fof(f11505,plain,(
% 131.48/31.95 ![X0]: (less_or_equal(add(additive_identity,additive_identity),X0)|less_or_equal(X0,add(additive_identity,additive_identity))|~defined(X0))),
% 131.48/31.95 inference(resolution,[status(thm)],[f1206,f66])).
% 131.48/31.95 fof(f11803,plain,(
% 131.48/31.95 ![X0]: (less_or_equal(multiply(b,b),X0)|less_or_equal(X0,multiply(b,b))|~defined(X0))),
% 131.48/31.95 inference(resolution,[status(thm)],[f1214,f66])).
% 131.48/31.95 fof(f12101,plain,(
% 131.48/31.95 ![X0]: (less_or_equal(add(a,additive_inverse(additive_identity)),X0)|less_or_equal(X0,add(a,additive_inverse(additive_identity)))|~defined(X0))),
% 131.48/31.95 inference(resolution,[status(thm)],[f1177,f66])).
% 131.48/31.95 fof(f12399,plain,(
% 131.48/31.95 ![X0]: (less_or_equal(add(a,additive_inverse(multiplicative_identity)),X0)|less_or_equal(X0,add(a,additive_inverse(multiplicative_identity)))|~defined(X0))),
% 131.48/31.95 inference(resolution,[status(thm)],[f1178,f66])).
% 131.48/31.95 fof(f12697,plain,(
% 131.48/31.95 ![X0]: (less_or_equal(add(a,additive_inverse(a)),X0)|less_or_equal(X0,add(a,additive_inverse(a)))|~defined(X0))),
% 131.48/31.95 inference(resolution,[status(thm)],[f1179,f66])).
% 131.48/31.95 fof(f12995,plain,(
% 131.48/31.95 ![X0]: (less_or_equal(add(a,additive_inverse(b)),X0)|less_or_equal(X0,add(a,additive_inverse(b)))|~defined(X0))),
% 131.48/31.95 inference(resolution,[status(thm)],[f1180,f66])).
% 131.48/31.95 fof(f13591,plain,(
% 131.48/31.95 ![X0]: (less_or_equal(add(multiplicative_identity,additive_inverse(additive_identity)),X0)|less_or_equal(X0,add(multiplicative_identity,additive_inverse(additive_identity)))|~defined(X0))),
% 131.48/31.95 inference(resolution,[status(thm)],[f1188,f66])).
% 131.48/31.95 fof(f13823,plain,(
% 131.48/31.95 less_or_equal(add(additive_identity,b),add(additive_identity,b))|less_or_equal(add(additive_identity,b),add(additive_identity,b))),
% 131.48/31.95 inference(resolution,[status(thm)],[f9419,f1203])).
% 131.48/31.95 fof(f13892,definition,(
% 131.48/31.95 sQ1970_spl <=> (less_or_equal(add(additive_identity,b),add(additive_identity,b)))),
% 131.48/31.95 introduced(definition,[new_symbols(definition,[sQ1970_spl])],[split_symbol_definition])).
% 131.48/31.95 fof(f13895,plain,(
% 131.48/31.95 sQ1970_spl),
% 131.48/31.95 inference(split_clause,[status(thm)],[f13823,f13892])).
% 131.48/31.95 fof(f13999,plain,(
% 131.48/31.95 less_or_equal(add(additive_identity,a),add(additive_identity,a))|less_or_equal(add(additive_identity,a),add(additive_identity,a))),
% 131.48/31.95 inference(resolution,[status(thm)],[f9717,f1204])).
% 131.48/31.95 fof(f14062,definition,(
% 131.48/31.95 sQ1997_spl <=> (less_or_equal(add(additive_identity,a),add(additive_identity,a)))),
% 131.48/31.95 introduced(definition,[new_symbols(definition,[sQ1997_spl])],[split_symbol_definition])).
% 131.48/31.95 fof(f14065,plain,(
% 131.48/31.95 sQ1997_spl),
% 131.48/31.95 inference(split_clause,[status(thm)],[f13999,f14062])).
% 131.48/31.95 fof(f14169,plain,(
% 131.48/31.95 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))),
% 131.48/31.95 inference(resolution,[status(thm)],[f11207,f1205])).
% 131.48/31.95 fof(f14226,definition,(
% 131.48/31.95 sQ2022_spl <=> (less_or_equal(add(additive_identity,multiplicative_identity),add(additive_identity,multiplicative_identity)))),
% 131.48/31.95 introduced(definition,[new_symbols(definition,[sQ2022_spl])],[split_symbol_definition])).
% 131.48/31.95 fof(f14229,plain,(
% 131.48/31.95 sQ2022_spl),
% 131.48/31.95 inference(split_clause,[status(thm)],[f14169,f14226])).
% 131.48/31.95 fof(f14333,plain,(
% 131.48/31.95 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))),
% 131.48/31.95 inference(resolution,[status(thm)],[f11505,f1206])).
% 131.48/31.95 fof(f14384,definition,(
% 131.48/31.95 sQ2045_spl <=> (less_or_equal(add(additive_identity,additive_identity),add(additive_identity,additive_identity)))),
% 131.48/31.95 introduced(definition,[new_symbols(definition,[sQ2045_spl])],[split_symbol_definition])).
% 131.48/31.95 fof(f14387,plain,(
% 131.48/31.95 sQ2045_spl),
% 131.48/31.95 inference(split_clause,[status(thm)],[f14333,f14384])).
% 131.48/31.95 fof(f14513,plain,(
% 131.48/31.95 less_or_equal(add(b,additive_inverse(multiplicative_identity)),add(b,additive_inverse(multiplicative_identity)))|less_or_equal(add(b,additive_inverse(multiplicative_identity)),add(b,additive_inverse(multiplicative_identity)))),
% 131.48/31.95 inference(resolution,[status(thm)],[f10015,f1167])).
% 131.48/31.95 fof(f14618,definition,(
% 131.48/31.95 sQ2086_spl <=> (less_or_equal(add(b,additive_inverse(multiplicative_identity)),add(b,additive_inverse(multiplicative_identity))))),
% 131.48/31.95 introduced(definition,[new_symbols(definition,[sQ2086_spl])],[split_symbol_definition])).
% 131.48/31.95 fof(f14621,plain,(
% 131.48/31.95 sQ2086_spl),
% 131.48/31.95 inference(split_clause,[status(thm)],[f14513,f14618])).
% 131.48/31.95 fof(f14665,plain,(
% 131.48/31.95 less_or_equal(add(b,additive_inverse(a)),add(b,additive_inverse(a)))|less_or_equal(add(b,additive_inverse(a)),add(b,additive_inverse(a)))),
% 131.48/31.95 inference(resolution,[status(thm)],[f10313,f1168])).
% 131.48/31.95 fof(f14764,definition,(
% 131.48/31.95 sQ2105_spl <=> (less_or_equal(add(b,additive_inverse(a)),add(b,additive_inverse(a))))),
% 131.48/31.95 introduced(definition,[new_symbols(definition,[sQ2105_spl])],[split_symbol_definition])).
% 131.48/31.95 fof(f14767,plain,(
% 131.48/31.95 sQ2105_spl),
% 131.48/31.95 inference(split_clause,[status(thm)],[f14665,f14764])).
% 131.48/31.95 fof(f14811,plain,(
% 131.48/31.95 less_or_equal(add(b,additive_inverse(b)),add(b,additive_inverse(b)))|less_or_equal(add(b,additive_inverse(b)),add(b,additive_inverse(b)))),
% 131.48/31.95 inference(resolution,[status(thm)],[f10611,f1169])).
% 131.48/31.95 fof(f14904,definition,(
% 131.48/31.95 sQ2122_spl <=> (less_or_equal(add(b,additive_inverse(b)),add(b,additive_inverse(b))))),
% 131.48/31.95 introduced(definition,[new_symbols(definition,[sQ2122_spl])],[split_symbol_definition])).
% 131.48/31.95 fof(f14907,plain,(
% 131.48/31.95 sQ2122_spl),
% 131.48/31.95 inference(split_clause,[status(thm)],[f14811,f14904])).
% 131.48/31.95 fof(f15067,plain,(
% 131.48/31.95 less_or_equal(multiply(b,b),multiply(b,b))|less_or_equal(multiply(b,b),multiply(b,b))),
% 131.48/31.95 inference(resolution,[status(thm)],[f11803,f1214])).
% 131.48/31.95 fof(f15112,definition,(
% 131.48/31.95 sQ2138_spl <=> (less_or_equal(multiply(b,b),multiply(b,b)))),
% 131.48/31.95 introduced(definition,[new_symbols(definition,[sQ2138_spl])],[split_symbol_definition])).
% 131.48/31.95 fof(f15115,plain,(
% 131.48/31.95 sQ2138_spl),
% 131.48/31.95 inference(split_clause,[status(thm)],[f15067,f15112])).
% 131.48/31.95 fof(f15210,plain,(
% 131.48/31.95 less_or_equal(add(a,additive_inverse(additive_identity)),add(a,additive_inverse(additive_identity)))|less_or_equal(add(a,additive_inverse(additive_identity)),add(a,additive_inverse(additive_identity)))),
% 131.48/31.95 inference(resolution,[status(thm)],[f12101,f1177])).
% 131.48/31.95 fof(f15285,definition,(
% 131.48/31.95 sQ2161_spl <=> (less_or_equal(add(a,additive_inverse(additive_identity)),add(a,additive_inverse(additive_identity))))),
% 131.48/31.95 introduced(definition,[new_symbols(definition,[sQ2161_spl])],[split_symbol_definition])).
% 131.48/31.95 fof(f15288,plain,(
% 131.48/31.95 sQ2161_spl),
% 131.48/31.95 inference(split_clause,[status(thm)],[f15210,f15285])).
% 131.48/31.95 fof(f15332,plain,(
% 131.48/31.95 less_or_equal(add(a,additive_inverse(multiplicative_identity)),add(a,additive_inverse(multiplicative_identity)))|less_or_equal(add(a,additive_inverse(multiplicative_identity)),add(a,additive_inverse(multiplicative_identity)))),
% 131.48/31.95 inference(resolution,[status(thm)],[f12399,f1178])).
% 131.48/31.95 fof(f15401,definition,(
% 131.48/31.95 sQ2170_spl <=> (less_or_equal(add(a,additive_inverse(multiplicative_identity)),add(a,additive_inverse(multiplicative_identity))))),
% 131.48/31.95 introduced(definition,[new_symbols(definition,[sQ2170_spl])],[split_symbol_definition])).
% 131.48/31.95 fof(f15404,plain,(
% 131.48/31.95 sQ2170_spl),
% 131.48/31.95 inference(split_clause,[status(thm)],[f15332,f15401])).
% 131.48/31.95 fof(f15448,plain,(
% 131.48/31.95 less_or_equal(add(a,additive_inverse(a)),add(a,additive_inverse(a)))|less_or_equal(add(a,additive_inverse(a)),add(a,additive_inverse(a)))),
% 131.48/31.95 inference(resolution,[status(thm)],[f12697,f1179])).
% 131.48/31.95 fof(f15511,definition,(
% 131.48/31.95 sQ2177_spl <=> (less_or_equal(add(a,additive_inverse(a)),add(a,additive_inverse(a))))),
% 131.48/31.95 introduced(definition,[new_symbols(definition,[sQ2177_spl])],[split_symbol_definition])).
% 131.48/31.95 fof(f15514,plain,(
% 131.48/31.95 sQ2177_spl),
% 131.48/31.95 inference(split_clause,[status(thm)],[f15448,f15511])).
% 131.48/31.95 fof(f15558,plain,(
% 131.48/31.95 less_or_equal(add(a,additive_inverse(b)),add(a,additive_inverse(b)))|less_or_equal(add(a,additive_inverse(b)),add(a,additive_inverse(b)))),
% 131.48/31.95 inference(resolution,[status(thm)],[f12995,f1180])).
% 131.48/31.95 fof(f15615,definition,(
% 131.48/31.95 sQ2182_spl <=> (less_or_equal(add(a,additive_inverse(b)),add(a,additive_inverse(b))))),
% 131.48/31.95 introduced(definition,[new_symbols(definition,[sQ2182_spl])],[split_symbol_definition])).
% 131.48/31.95 fof(f15618,plain,(
% 131.48/31.95 sQ2182_spl),
% 131.48/31.95 inference(split_clause,[status(thm)],[f15558,f15615])).
% 131.48/31.95 fof(f15756,plain,(
% 131.48/31.95 less_or_equal(add(multiplicative_identity,additive_inverse(additive_identity)),add(multiplicative_identity,additive_inverse(additive_identity)))|less_or_equal(add(multiplicative_identity,additive_inverse(additive_identity)),add(multiplicative_identity,additive_inverse(additive_identity)))),
% 131.48/31.97 inference(resolution,[status(thm)],[f13591,f1188])).
% 131.48/31.97 fof(f15801,definition,(
% 131.48/31.97 sQ2186_spl <=> (less_or_equal(add(multiplicative_identity,additive_inverse(additive_identity)),add(multiplicative_identity,additive_inverse(additive_identity))))),
% 131.48/31.97 introduced(definition,[new_symbols(definition,[sQ2186_spl])],[split_symbol_definition])).
% 131.48/31.97 fof(f15804,plain,(
% 131.48/31.97 sQ2186_spl),
% 131.48/31.97 inference(split_clause,[status(thm)],[f15756,f15801])).
% 131.48/31.97 fof(f16139,plain,(
% 131.48/31.97 ![X0]: (less_or_equal(multiply(b,a),X0)|less_or_equal(X0,multiply(b,a))|~defined(X0))),
% 131.48/31.97 inference(resolution,[status(thm)],[f1215,f66])).
% 131.48/31.97 fof(f16557,plain,(
% 131.48/31.97 ![X0]: (less_or_equal(multiply(b,multiplicative_identity),X0)|less_or_equal(X0,multiply(b,multiplicative_identity))|~defined(X0))),
% 131.48/31.97 inference(resolution,[status(thm)],[f1216,f66])).
% 131.48/31.97 fof(f16975,plain,(
% 131.48/31.97 ![X0]: (less_or_equal(add(multiplicative_identity,additive_inverse(multiplicative_identity)),X0)|less_or_equal(X0,add(multiplicative_identity,additive_inverse(multiplicative_identity)))|~defined(X0))),
% 131.48/31.97 inference(resolution,[status(thm)],[f1189,f66])).
% 131.48/31.97 fof(f17393,plain,(
% 131.48/31.97 ![X0]: (less_or_equal(add(multiplicative_identity,additive_inverse(a)),X0)|less_or_equal(X0,add(multiplicative_identity,additive_inverse(a)))|~defined(X0))),
% 131.48/31.97 inference(resolution,[status(thm)],[f1190,f66])).
% 131.48/31.97 fof(f17811,plain,(
% 131.48/31.97 ![X0]: (less_or_equal(add(multiplicative_identity,additive_inverse(b)),X0)|less_or_equal(X0,add(multiplicative_identity,additive_inverse(b)))|~defined(X0))),
% 131.48/31.97 inference(resolution,[status(thm)],[f1191,f66])).
% 131.48/31.97 fof(f18647,plain,(
% 131.48/31.97 ![X0]: (less_or_equal(multiply(b,additive_identity),X0)|less_or_equal(X0,multiply(b,additive_identity))|~defined(X0))),
% 131.48/31.97 inference(resolution,[status(thm)],[f1217,f66])).
% 131.48/31.97 fof(f19065,plain,(
% 131.48/31.97 ![X0]: (less_or_equal(multiply(a,b),X0)|less_or_equal(X0,multiply(a,b))|~defined(X0))),
% 131.48/31.97 inference(resolution,[status(thm)],[f1225,f66])).
% 131.48/31.97 fof(f19483,plain,(
% 131.48/31.97 ![X0]: (less_or_equal(multiply(a,a),X0)|less_or_equal(X0,multiply(a,a))|~defined(X0))),
% 131.48/31.97 inference(resolution,[status(thm)],[f1226,f66])).
% 131.48/31.97 fof(f19901,plain,(
% 131.48/31.97 ![X0]: (less_or_equal(add(additive_identity,additive_inverse(additive_identity)),X0)|less_or_equal(X0,add(additive_identity,additive_inverse(additive_identity)))|~defined(X0))),
% 131.48/31.97 inference(resolution,[status(thm)],[f1199,f66])).
% 131.48/31.97 fof(f20319,plain,(
% 131.48/31.97 ![X0]: (less_or_equal(add(additive_identity,additive_inverse(multiplicative_identity)),X0)|less_or_equal(X0,add(additive_identity,additive_inverse(multiplicative_identity)))|~defined(X0))),
% 131.48/31.97 inference(resolution,[status(thm)],[f1200,f66])).
% 131.48/31.97 fof(f20737,plain,(
% 131.48/31.97 ![X0]: (less_or_equal(add(additive_identity,additive_inverse(a)),X0)|less_or_equal(X0,add(additive_identity,additive_inverse(a)))|~defined(X0))),
% 131.48/31.97 inference(resolution,[status(thm)],[f1201,f66])).
% 131.48/31.97 fof(f21155,plain,(
% 131.48/31.97 ![X0]: (less_or_equal(add(additive_identity,additive_inverse(b)),X0)|less_or_equal(X0,add(additive_identity,additive_inverse(b)))|~defined(X0))),
% 131.48/31.97 inference(resolution,[status(thm)],[f1202,f66])).
% 131.48/31.97 fof(f21991,plain,(
% 131.48/31.97 ![X0]: (less_or_equal(multiply(b,additive_inverse(additive_identity)),X0)|less_or_equal(X0,multiply(b,additive_inverse(additive_identity)))|~defined(X0))),
% 131.48/31.97 inference(resolution,[status(thm)],[f1210,f66])).
% 131.48/31.97 fof(f22330,plain,(
% 131.48/31.97 less_or_equal(multiply(b,a),multiply(b,a))|less_or_equal(multiply(b,a),multiply(b,a))),
% 131.48/31.97 inference(resolution,[status(thm)],[f16139,f1215])).
% 131.48/31.97 fof(f22426,definition,(
% 131.48/31.97 sQ3594_spl <=> (less_or_equal(multiply(b,a),multiply(b,a)))),
% 131.48/31.97 introduced(definition,[new_symbols(definition,[sQ3594_spl])],[split_symbol_definition])).
% 131.48/31.97 fof(f22429,plain,(
% 131.48/31.97 sQ3594_spl),
% 131.48/31.97 inference(split_clause,[status(thm)],[f22330,f22426])).
% 131.48/31.97 fof(f22536,plain,(
% 131.48/31.97 less_or_equal(multiply(b,multiplicative_identity),multiply(b,multiplicative_identity))|less_or_equal(multiply(b,multiplicative_identity),multiply(b,multiplicative_identity))),
% 131.48/31.97 inference(resolution,[status(thm)],[f16557,f1216])).
% 131.48/31.97 fof(f22626,definition,(
% 131.48/31.97 sQ3621_spl <=> (less_or_equal(multiply(b,multiplicative_identity),multiply(b,multiplicative_identity)))),
% 131.48/31.97 introduced(definition,[new_symbols(definition,[sQ3621_spl])],[split_symbol_definition])).
% 131.48/31.97 fof(f22629,plain,(
% 131.48/31.97 sQ3621_spl),
% 131.48/31.97 inference(split_clause,[status(thm)],[f22536,f22626])).
% 131.48/31.97 fof(f22736,plain,(
% 131.48/31.97 less_or_equal(multiply(b,additive_identity),multiply(b,additive_identity))|less_or_equal(multiply(b,additive_identity),multiply(b,additive_identity))),
% 131.48/31.97 inference(resolution,[status(thm)],[f18647,f1217])).
% 131.48/31.97 fof(f22820,definition,(
% 131.48/31.97 sQ3646_spl <=> (less_or_equal(multiply(b,additive_identity),multiply(b,additive_identity)))),
% 131.48/31.97 introduced(definition,[new_symbols(definition,[sQ3646_spl])],[split_symbol_definition])).
% 131.48/31.97 fof(f22823,plain,(
% 131.48/31.97 sQ3646_spl),
% 131.48/31.97 inference(split_clause,[status(thm)],[f22736,f22820])).
% 131.48/31.97 fof(f22928,plain,(
% 131.48/31.97 less_or_equal(multiply(a,b),multiply(a,b))|less_or_equal(multiply(a,b),multiply(a,b))),
% 131.48/31.97 inference(resolution,[status(thm)],[f19065,f1225])).
% 131.48/31.97 fof(f22994,definition,(
% 131.48/31.97 sQ3665_spl <=> (less_or_equal(multiply(a,b),multiply(a,b)))),
% 131.48/31.97 introduced(definition,[new_symbols(definition,[sQ3665_spl])],[split_symbol_definition])).
% 131.48/31.97 fof(f22997,plain,(
% 131.48/31.97 sQ3665_spl),
% 131.48/31.97 inference(split_clause,[status(thm)],[f22928,f22994])).
% 131.48/31.97 fof(f23135,plain,(
% 131.48/31.97 less_or_equal(add(multiplicative_identity,additive_inverse(multiplicative_identity)),add(multiplicative_identity,additive_inverse(multiplicative_identity)))|less_or_equal(add(multiplicative_identity,additive_inverse(multiplicative_identity)),add(multiplicative_identity,additive_inverse(multiplicative_identity)))),
% 131.48/31.97 inference(resolution,[status(thm)],[f16975,f1189])).
% 131.48/31.97 fof(f23255,definition,(
% 131.48/31.97 sQ3706_spl <=> (less_or_equal(add(multiplicative_identity,additive_inverse(multiplicative_identity)),add(multiplicative_identity,additive_inverse(multiplicative_identity))))),
% 131.48/31.97 introduced(definition,[new_symbols(definition,[sQ3706_spl])],[split_symbol_definition])).
% 131.48/31.97 fof(f23258,plain,(
% 131.48/31.97 sQ3706_spl),
% 131.48/31.97 inference(split_clause,[status(thm)],[f23135,f23255])).
% 131.48/31.97 fof(f23317,plain,(
% 131.48/31.97 less_or_equal(add(multiplicative_identity,additive_inverse(a)),add(multiplicative_identity,additive_inverse(a)))|less_or_equal(add(multiplicative_identity,additive_inverse(a)),add(multiplicative_identity,additive_inverse(a)))),
% 131.48/31.97 inference(resolution,[status(thm)],[f17393,f1190])).
% 131.48/31.97 fof(f23431,definition,(
% 131.48/31.97 sQ3725_spl <=> (less_or_equal(add(multiplicative_identity,additive_inverse(a)),add(multiplicative_identity,additive_inverse(a))))),
% 131.48/31.97 introduced(definition,[new_symbols(definition,[sQ3725_spl])],[split_symbol_definition])).
% 131.48/31.97 fof(f23434,plain,(
% 131.48/31.97 sQ3725_spl),
% 131.48/31.97 inference(split_clause,[status(thm)],[f23317,f23431])).
% 131.48/31.97 fof(f23493,plain,(
% 131.48/31.97 less_or_equal(add(multiplicative_identity,additive_inverse(b)),add(multiplicative_identity,additive_inverse(b)))|less_or_equal(add(multiplicative_identity,additive_inverse(b)),add(multiplicative_identity,additive_inverse(b)))),
% 131.48/31.97 inference(resolution,[status(thm)],[f17811,f1191])).
% 131.48/31.97 fof(f23601,definition,(
% 131.48/31.97 sQ3742_spl <=> (less_or_equal(add(multiplicative_identity,additive_inverse(b)),add(multiplicative_identity,additive_inverse(b))))),
% 131.48/31.97 introduced(definition,[new_symbols(definition,[sQ3742_spl])],[split_symbol_definition])).
% 131.48/31.97 fof(f23604,plain,(
% 131.48/31.97 sQ3742_spl),
% 131.48/31.97 inference(split_clause,[status(thm)],[f23493,f23601])).
% 131.48/31.97 fof(f23812,plain,(
% 131.48/31.97 less_or_equal(multiply(a,a),multiply(a,a))|less_or_equal(multiply(a,a),multiply(a,a))),
% 131.48/31.97 inference(resolution,[status(thm)],[f19483,f1226])).
% 131.48/31.97 fof(f23872,definition,(
% 131.48/31.97 sQ3758_spl <=> (less_or_equal(multiply(a,a),multiply(a,a)))),
% 131.48/31.97 introduced(definition,[new_symbols(definition,[sQ3758_spl])],[split_symbol_definition])).
% 131.48/31.97 fof(f23875,plain,(
% 131.48/31.97 sQ3758_spl),
% 131.48/31.97 inference(split_clause,[status(thm)],[f23812,f23872])).
% 131.48/31.97 fof(f23982,plain,(
% 131.48/31.97 less_or_equal(add(additive_identity,additive_inverse(additive_identity)),add(additive_identity,additive_inverse(additive_identity)))|less_or_equal(add(additive_identity,additive_inverse(additive_identity)),add(additive_identity,additive_inverse(additive_identity)))),
% 131.48/31.97 inference(resolution,[status(thm)],[f19901,f1199])).
% 131.48/31.97 fof(f24072,definition,(
% 131.48/31.97 sQ3781_spl <=> (less_or_equal(add(additive_identity,additive_inverse(additive_identity)),add(additive_identity,additive_inverse(additive_identity))))),
% 131.48/31.97 introduced(definition,[new_symbols(definition,[sQ3781_spl])],[split_symbol_definition])).
% 131.48/31.97 fof(f24075,plain,(
% 131.48/31.97 sQ3781_spl),
% 131.48/31.97 inference(split_clause,[status(thm)],[f23982,f24072])).
% 131.48/31.97 fof(f24134,plain,(
% 131.48/31.97 less_or_equal(add(additive_identity,additive_inverse(multiplicative_identity)),add(additive_identity,additive_inverse(multiplicative_identity)))|less_or_equal(add(additive_identity,additive_inverse(multiplicative_identity)),add(additive_identity,additive_inverse(multiplicative_identity)))),
% 131.48/31.97 inference(resolution,[status(thm)],[f20319,f1200])).
% 131.48/31.97 fof(f24218,definition,(
% 131.48/31.97 sQ3790_spl <=> (less_or_equal(add(additive_identity,additive_inverse(multiplicative_identity)),add(additive_identity,additive_inverse(multiplicative_identity))))),
% 131.48/31.97 introduced(definition,[new_symbols(definition,[sQ3790_spl])],[split_symbol_definition])).
% 131.48/31.97 fof(f24221,plain,(
% 131.48/31.97 sQ3790_spl),
% 131.48/31.97 inference(split_clause,[status(thm)],[f24134,f24218])).
% 131.48/31.97 fof(f24280,plain,(
% 131.48/31.97 less_or_equal(add(additive_identity,additive_inverse(a)),add(additive_identity,additive_inverse(a)))|less_or_equal(add(additive_identity,additive_inverse(a)),add(additive_identity,additive_inverse(a)))),
% 131.48/31.97 inference(resolution,[status(thm)],[f20737,f1201])).
% 131.48/31.97 fof(f24358,definition,(
% 131.48/31.97 sQ3797_spl <=> (less_or_equal(add(additive_identity,additive_inverse(a)),add(additive_identity,additive_inverse(a))))),
% 131.48/31.97 introduced(definition,[new_symbols(definition,[sQ3797_spl])],[split_symbol_definition])).
% 131.48/31.97 fof(f24361,plain,(
% 131.48/31.97 sQ3797_spl),
% 131.48/31.97 inference(split_clause,[status(thm)],[f24280,f24358])).
% 131.48/31.97 fof(f24420,plain,(
% 131.48/31.97 less_or_equal(add(additive_identity,additive_inverse(b)),add(additive_identity,additive_inverse(b)))|less_or_equal(add(additive_identity,additive_inverse(b)),add(additive_identity,additive_inverse(b)))),
% 131.48/31.97 inference(resolution,[status(thm)],[f21155,f1202])).
% 131.48/31.97 fof(f24492,definition,(
% 131.48/31.97 sQ3802_spl <=> (less_or_equal(add(additive_identity,additive_inverse(b)),add(additive_identity,additive_inverse(b))))),
% 131.48/31.97 introduced(definition,[new_symbols(definition,[sQ3802_spl])],[split_symbol_definition])).
% 131.48/31.97 fof(f24495,plain,(
% 131.48/31.97 sQ3802_spl),
% 131.48/31.97 inference(split_clause,[status(thm)],[f24420,f24492])).
% 131.48/31.97 fof(f24678,plain,(
% 131.48/31.97 less_or_equal(multiply(b,additive_inverse(additive_identity)),multiply(b,additive_inverse(additive_identity)))|less_or_equal(multiply(b,additive_inverse(additive_identity)),multiply(b,additive_inverse(additive_identity)))),
% 131.48/31.97 inference(resolution,[status(thm)],[f21991,f1210])).
% 131.48/31.97 fof(f24738,definition,(
% 131.48/31.97 sQ3806_spl <=> (less_or_equal(multiply(b,additive_inverse(additive_identity)),multiply(b,additive_inverse(additive_identity))))),
% 131.48/31.97 introduced(definition,[new_symbols(definition,[sQ3806_spl])],[split_symbol_definition])).
% 131.48/31.97 fof(f24741,plain,(
% 131.48/31.97 sQ3806_spl),
% 131.48/31.97 inference(split_clause,[status(thm)],[f24678,f24738])).
% 131.48/31.97 fof(f24998,plain,(
% 131.48/31.97 ![X0]: (less_or_equal(multiply(a,multiplicative_identity),X0)|less_or_equal(X0,multiply(a,multiplicative_identity))|~defined(X0))),
% 131.48/31.97 inference(resolution,[status(thm)],[f1227,f66])).
% 131.48/31.97 fof(f25536,plain,(
% 131.48/31.97 ![X0]: (less_or_equal(multiply(a,additive_identity),X0)|less_or_equal(X0,multiply(a,additive_identity))|~defined(X0))),
% 131.48/31.97 inference(resolution,[status(thm)],[f1228,f66])).
% 131.48/31.97 fof(f26074,plain,(
% 131.48/31.97 ![X0]: (less_or_equal(multiply(b,additive_inverse(multiplicative_identity)),X0)|less_or_equal(X0,multiply(b,additive_inverse(multiplicative_identity)))|~defined(X0))),
% 131.48/31.97 inference(resolution,[status(thm)],[f1211,f66])).
% 131.48/31.97 fof(f26612,plain,(
% 131.48/31.97 ![X0]: (less_or_equal(multiply(b,additive_inverse(a)),X0)|less_or_equal(X0,multiply(b,additive_inverse(a)))|~defined(X0))),
% 131.48/31.97 inference(resolution,[status(thm)],[f1212,f66])).
% 131.48/31.97 fof(f27150,plain,(
% 131.48/31.97 ![X0]: (less_or_equal(multiply(b,additive_inverse(b)),X0)|less_or_equal(X0,multiply(b,additive_inverse(b)))|~defined(X0))),
% 131.48/31.97 inference(resolution,[status(thm)],[f1213,f66])).
% 131.48/31.97 fof(f28226,plain,(
% 131.48/31.97 ![X0]: (less_or_equal(multiply(multiplicative_identity,b),X0)|less_or_equal(X0,multiply(multiplicative_identity,b))|~defined(X0))),
% 131.48/31.97 inference(resolution,[status(thm)],[f1236,f66])).
% 131.48/31.97 fof(f28764,plain,(
% 131.48/31.97 ![X0]: (less_or_equal(multiply(multiplicative_identity,a),X0)|less_or_equal(X0,multiply(multiplicative_identity,a))|~defined(X0))),
% 131.48/31.97 inference(resolution,[status(thm)],[f1237,f66])).
% 131.48/31.97 fof(f29302,plain,(
% 131.48/31.97 ![X0]: (less_or_equal(multiply(multiplicative_identity,multiplicative_identity),X0)|less_or_equal(X0,multiply(multiplicative_identity,multiplicative_identity))|~defined(X0))),
% 131.48/31.97 inference(resolution,[status(thm)],[f1238,f66])).
% 131.48/31.97 fof(f29840,plain,(
% 131.48/31.97 ![X0]: (less_or_equal(multiply(a,additive_inverse(additive_identity)),X0)|less_or_equal(X0,multiply(a,additive_inverse(additive_identity)))|~defined(X0))),
% 131.48/31.97 inference(resolution,[status(thm)],[f1221,f66])).
% 131.48/31.97 fof(f30378,plain,(
% 131.48/31.97 ![X0]: (less_or_equal(multiply(a,additive_inverse(multiplicative_identity)),X0)|less_or_equal(X0,multiply(a,additive_inverse(multiplicative_identity)))|~defined(X0))),
% 131.48/31.97 inference(resolution,[status(thm)],[f1222,f66])).
% 131.48/31.97 fof(f30916,plain,(
% 131.48/31.97 ![X0]: (less_or_equal(multiply(a,additive_inverse(a)),X0)|less_or_equal(X0,multiply(a,additive_inverse(a)))|~defined(X0))),
% 131.48/31.97 inference(resolution,[status(thm)],[f1223,f66])).
% 131.48/31.97 fof(f31454,plain,(
% 131.48/31.97 ![X0]: (less_or_equal(multiply(a,additive_inverse(b)),X0)|less_or_equal(X0,multiply(a,additive_inverse(b)))|~defined(X0))),
% 131.48/31.97 inference(resolution,[status(thm)],[f1224,f66])).
% 131.48/31.97 fof(f32530,plain,(
% 131.48/31.97 ![X0]: (less_or_equal(multiply(multiplicative_identity,additive_inverse(additive_identity)),X0)|less_or_equal(X0,multiply(multiplicative_identity,additive_inverse(additive_identity)))|~defined(X0))),
% 131.48/31.97 inference(resolution,[status(thm)],[f1232,f66])).
% 131.48/31.97 fof(f32979,plain,(
% 131.48/31.97 less_or_equal(multiply(a,multiplicative_identity),multiply(a,multiplicative_identity))|less_or_equal(multiply(a,multiplicative_identity),multiply(a,multiplicative_identity))),
% 131.48/31.97 inference(resolution,[status(thm)],[f24998,f1227])).
% 131.48/31.97 fof(f33120,definition,(
% 131.48/31.97 sQ5674_spl <=> (less_or_equal(multiply(a,multiplicative_identity),multiply(a,multiplicative_identity)))),
% 131.48/31.97 introduced(definition,[new_symbols(definition,[sQ5674_spl])],[split_symbol_definition])).
% 131.48/31.97 fof(f33123,plain,(
% 131.48/31.97 sQ5674_spl),
% 131.48/31.97 inference(split_clause,[status(thm)],[f32979,f33120])).
% 131.48/31.97 fof(f33215,plain,(
% 131.48/31.97 less_or_equal(multiply(a,additive_identity),multiply(a,additive_identity))|less_or_equal(multiply(a,additive_identity),multiply(a,additive_identity))),
% 131.48/31.97 inference(resolution,[status(thm)],[f25536,f1228])).
% 131.48/31.97 fof(f33350,definition,(
% 131.48/31.97 sQ5701_spl <=> (less_or_equal(multiply(a,additive_identity),multiply(a,additive_identity)))),
% 131.48/31.97 introduced(definition,[new_symbols(definition,[sQ5701_spl])],[split_symbol_definition])).
% 131.48/31.97 fof(f33353,plain,(
% 131.48/31.97 sQ5701_spl),
% 131.48/31.97 inference(split_clause,[status(thm)],[f33215,f33350])).
% 131.48/31.97 fof(f33440,plain,(
% 131.48/31.97 less_or_equal(multiply(multiplicative_identity,b),multiply(multiplicative_identity,b))|less_or_equal(multiply(multiplicative_identity,b),multiply(multiplicative_identity,b))),
% 131.48/31.97 inference(resolution,[status(thm)],[f28226,f1236])).
% 131.48/31.97 fof(f33539,definition,(
% 131.48/31.97 sQ5716_spl <=> (less_or_equal(multiply(multiplicative_identity,b),multiply(multiplicative_identity,b)))),
% 131.48/31.97 introduced(definition,[new_symbols(definition,[sQ5716_spl])],[split_symbol_definition])).
% 131.48/31.97 fof(f33542,plain,(
% 131.48/31.97 sQ5716_spl),
% 131.48/31.97 inference(split_clause,[status(thm)],[f33440,f33539])).
% 131.48/31.97 fof(f33664,plain,(
% 131.48/31.97 less_or_equal(multiply(multiplicative_identity,a),multiply(multiplicative_identity,a))|less_or_equal(multiply(multiplicative_identity,a),multiply(multiplicative_identity,a))),
% 131.48/31.97 inference(resolution,[status(thm)],[f28764,f1237])).
% 131.48/31.97 fof(f33757,definition,(
% 131.48/31.97 sQ5739_spl <=> (less_or_equal(multiply(multiplicative_identity,a),multiply(multiplicative_identity,a)))),
% 131.48/31.97 introduced(definition,[new_symbols(definition,[sQ5739_spl])],[split_symbol_definition])).
% 131.48/31.97 fof(f33760,plain,(
% 131.48/31.97 sQ5739_spl),
% 131.48/31.97 inference(split_clause,[status(thm)],[f33664,f33757])).
% 131.48/31.97 fof(f33896,plain,(
% 131.48/31.97 less_or_equal(multiply(b,additive_inverse(multiplicative_identity)),multiply(b,additive_inverse(multiplicative_identity)))|less_or_equal(multiply(b,additive_inverse(multiplicative_identity)),multiply(b,additive_inverse(multiplicative_identity)))),
% 131.48/31.97 inference(resolution,[status(thm)],[f26074,f1211])).
% 131.48/31.97 fof(f34031,definition,(
% 131.48/31.97 sQ5776_spl <=> (less_or_equal(multiply(b,additive_inverse(multiplicative_identity)),multiply(b,additive_inverse(multiplicative_identity))))),
% 131.48/31.97 introduced(definition,[new_symbols(definition,[sQ5776_spl])],[split_symbol_definition])).
% 131.48/31.97 fof(f34034,plain,(
% 131.48/31.97 sQ5776_spl),
% 131.48/31.97 inference(split_clause,[status(thm)],[f33896,f34031])).
% 131.48/31.97 fof(f34108,plain,(
% 131.48/31.97 less_or_equal(multiply(b,additive_inverse(a)),multiply(b,additive_inverse(a)))|less_or_equal(multiply(b,additive_inverse(a)),multiply(b,additive_inverse(a)))),
% 131.48/31.97 inference(resolution,[status(thm)],[f26612,f1212])).
% 131.48/31.97 fof(f34237,definition,(
% 131.48/31.97 sQ5795_spl <=> (less_or_equal(multiply(b,additive_inverse(a)),multiply(b,additive_inverse(a))))),
% 131.48/31.97 introduced(definition,[new_symbols(definition,[sQ5795_spl])],[split_symbol_definition])).
% 131.48/31.97 fof(f34240,plain,(
% 131.48/31.97 sQ5795_spl),
% 131.48/31.97 inference(split_clause,[status(thm)],[f34108,f34237])).
% 131.48/31.97 fof(f34314,plain,(
% 131.48/31.97 less_or_equal(multiply(b,additive_inverse(b)),multiply(b,additive_inverse(b)))|less_or_equal(multiply(b,additive_inverse(b)),multiply(b,additive_inverse(b)))),
% 131.48/31.97 inference(resolution,[status(thm)],[f27150,f1213])).
% 131.48/31.97 fof(f34437,definition,(
% 131.48/31.97 sQ5812_spl <=> (less_or_equal(multiply(b,additive_inverse(b)),multiply(b,additive_inverse(b))))),
% 131.48/31.97 introduced(definition,[new_symbols(definition,[sQ5812_spl])],[split_symbol_definition])).
% 131.48/31.97 fof(f34440,plain,(
% 131.48/31.97 sQ5812_spl),
% 131.48/31.97 inference(split_clause,[status(thm)],[f34314,f34437])).
% 131.48/31.97 fof(f34698,plain,(
% 131.48/31.97 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))),
% 131.48/31.97 inference(resolution,[status(thm)],[f29302,f1238])).
% 131.48/31.97 fof(f34785,definition,(
% 131.48/31.97 sQ5832_spl <=> (less_or_equal(multiply(multiplicative_identity,multiplicative_identity),multiply(multiplicative_identity,multiplicative_identity)))),
% 131.48/31.97 introduced(definition,[new_symbols(definition,[sQ5832_spl])],[split_symbol_definition])).
% 131.48/31.97 fof(f34788,plain,(
% 131.48/31.97 sQ5832_spl),
% 131.48/31.97 inference(split_clause,[status(thm)],[f34698,f34785])).
% 131.48/31.97 fof(f34893,plain,(
% 131.48/31.97 less_or_equal(multiply(a,additive_inverse(additive_identity)),multiply(a,additive_inverse(additive_identity)))|less_or_equal(multiply(a,additive_inverse(additive_identity)),multiply(a,additive_inverse(additive_identity)))),
% 131.48/31.97 inference(resolution,[status(thm)],[f29840,f1221])).
% 131.48/31.97 fof(f34998,definition,(
% 131.48/31.97 sQ5851_spl <=> (less_or_equal(multiply(a,additive_inverse(additive_identity)),multiply(a,additive_inverse(additive_identity))))),
% 131.48/31.97 introduced(definition,[new_symbols(definition,[sQ5851_spl])],[split_symbol_definition])).
% 131.48/31.97 fof(f35001,plain,(
% 131.48/31.97 sQ5851_spl),
% 131.48/31.97 inference(split_clause,[status(thm)],[f34893,f34998])).
% 131.48/31.97 fof(f35075,plain,(
% 131.48/31.97 less_or_equal(multiply(a,additive_inverse(multiplicative_identity)),multiply(a,additive_inverse(multiplicative_identity)))|less_or_equal(multiply(a,additive_inverse(multiplicative_identity)),multiply(a,additive_inverse(multiplicative_identity)))),
% 131.48/31.97 inference(resolution,[status(thm)],[f30378,f1222])).
% 131.48/31.97 fof(f35174,definition,(
% 131.48/31.97 sQ5860_spl <=> (less_or_equal(multiply(a,additive_inverse(multiplicative_identity)),multiply(a,additive_inverse(multiplicative_identity))))),
% 131.48/31.97 introduced(definition,[new_symbols(definition,[sQ5860_spl])],[split_symbol_definition])).
% 131.48/31.97 fof(f35177,plain,(
% 131.48/31.97 sQ5860_spl),
% 131.48/31.97 inference(split_clause,[status(thm)],[f35075,f35174])).
% 131.48/31.97 fof(f35251,plain,(
% 131.48/31.97 less_or_equal(multiply(a,additive_inverse(a)),multiply(a,additive_inverse(a)))|less_or_equal(multiply(a,additive_inverse(a)),multiply(a,additive_inverse(a)))),
% 131.48/31.97 inference(resolution,[status(thm)],[f30916,f1223])).
% 131.48/31.97 fof(f35344,definition,(
% 131.48/31.97 sQ5867_spl <=> (less_or_equal(multiply(a,additive_inverse(a)),multiply(a,additive_inverse(a))))),
% 131.48/31.97 introduced(definition,[new_symbols(definition,[sQ5867_spl])],[split_symbol_definition])).
% 131.48/31.97 fof(f35347,plain,(
% 131.48/31.97 sQ5867_spl),
% 131.48/31.97 inference(split_clause,[status(thm)],[f35251,f35344])).
% 131.48/31.97 fof(f35421,plain,(
% 131.48/31.97 less_or_equal(multiply(a,additive_inverse(b)),multiply(a,additive_inverse(b)))|less_or_equal(multiply(a,additive_inverse(b)),multiply(a,additive_inverse(b)))),
% 131.48/31.97 inference(resolution,[status(thm)],[f31454,f1224])).
% 131.48/31.97 fof(f35508,definition,(
% 131.48/31.97 sQ5872_spl <=> (less_or_equal(multiply(a,additive_inverse(b)),multiply(a,additive_inverse(b))))),
% 131.48/31.97 introduced(definition,[new_symbols(definition,[sQ5872_spl])],[split_symbol_definition])).
% 131.48/31.97 fof(f35511,plain,(
% 131.48/31.97 sQ5872_spl),
% 131.48/31.97 inference(split_clause,[status(thm)],[f35421,f35508])).
% 131.48/31.97 fof(f35740,plain,(
% 131.48/31.97 less_or_equal(multiply(multiplicative_identity,additive_inverse(additive_identity)),multiply(multiplicative_identity,additive_inverse(additive_identity)))|less_or_equal(multiply(multiplicative_identity,additive_inverse(additive_identity)),multiply(multiplicative_identity,additive_inverse(additive_identity)))),
% 131.48/31.97 inference(resolution,[status(thm)],[f32530,f1232])).
% 131.48/31.97 fof(f35815,definition,(
% 131.48/31.97 sQ5876_spl <=> (less_or_equal(multiply(multiplicative_identity,additive_inverse(additive_identity)),multiply(multiplicative_identity,additive_inverse(additive_identity))))),
% 131.48/31.97 introduced(definition,[new_symbols(definition,[sQ5876_spl])],[split_symbol_definition])).
% 131.48/31.97 fof(f35818,plain,(
% 131.48/31.97 sQ5876_spl),
% 131.48/31.97 inference(split_clause,[status(thm)],[f35740,f35815])).
% 131.48/31.97 fof(f36268,plain,(
% 131.48/31.97 ![X0]: (less_or_equal(multiply(multiplicative_identity,additive_identity),X0)|less_or_equal(X0,multiply(multiplicative_identity,additive_identity))|~defined(X0))),
% 131.48/31.97 inference(resolution,[status(thm)],[f1239,f66])).
% 131.48/31.97 fof(f36926,plain,(
% 131.48/31.97 ![X0]: (less_or_equal(multiply(additive_identity,b),X0)|less_or_equal(X0,multiply(additive_identity,b))|~defined(X0))),
% 131.48/31.97 inference(resolution,[status(thm)],[f1247,f66])).
% 131.48/31.97 fof(f37584,plain,(
% 131.48/31.97 ![X0]: (less_or_equal(multiply(multiplicative_identity,additive_inverse(multiplicative_identity)),X0)|less_or_equal(X0,multiply(multiplicative_identity,additive_inverse(multiplicative_identity)))|~defined(X0))),
% 131.48/31.97 inference(resolution,[status(thm)],[f1233,f66])).
% 131.48/31.97 fof(f38242,plain,(
% 131.48/31.97 ![X0]: (less_or_equal(multiply(multiplicative_identity,additive_inverse(a)),X0)|less_or_equal(X0,multiply(multiplicative_identity,additive_inverse(a)))|~defined(X0))),
% 131.48/31.97 inference(resolution,[status(thm)],[f1234,f66])).
% 131.48/31.97 fof(f38900,plain,(
% 131.48/31.97 ![X0]: (less_or_equal(multiply(multiplicative_identity,additive_inverse(b)),X0)|less_or_equal(X0,multiply(multiplicative_identity,additive_inverse(b)))|~defined(X0))),
% 131.48/31.97 inference(resolution,[status(thm)],[f1235,f66])).
% 131.48/31.97 fof(f40216,plain,(
% 131.48/31.97 ![X0]: (less_or_equal(multiply(additive_identity,a),X0)|less_or_equal(X0,multiply(additive_identity,a))|~defined(X0))),
% 131.48/31.97 inference(resolution,[status(thm)],[f1248,f66])).
% 131.48/31.97 fof(f40874,plain,(
% 131.48/31.97 ![X0]: (less_or_equal(multiply(additive_identity,multiplicative_identity),X0)|less_or_equal(X0,multiply(additive_identity,multiplicative_identity))|~defined(X0))),
% 131.48/31.97 inference(resolution,[status(thm)],[f1249,f66])).
% 131.48/31.97 fof(f41532,plain,(
% 131.48/31.97 ![X0]: (less_or_equal(multiply(additive_identity,additive_identity),X0)|less_or_equal(X0,multiply(additive_identity,additive_identity))|~defined(X0))),
% 131.48/31.97 inference(resolution,[status(thm)],[f1250,f66])).
% 131.48/31.97 fof(f42190,plain,(
% 131.48/31.97 ![X0]: (less_or_equal(multiply(additive_identity,additive_inverse(additive_identity)),X0)|less_or_equal(X0,multiply(additive_identity,additive_inverse(additive_identity)))|~defined(X0))),
% 131.48/31.97 inference(resolution,[status(thm)],[f1243,f66])).
% 131.48/31.97 fof(f42848,plain,(
% 131.48/31.97 ![X0]: (less_or_equal(multiply(additive_identity,additive_inverse(multiplicative_identity)),X0)|less_or_equal(X0,multiply(additive_identity,additive_inverse(multiplicative_identity)))|~defined(X0))),
% 131.48/31.97 inference(resolution,[status(thm)],[f1244,f66])).
% 131.48/31.97 fof(f43506,plain,(
% 131.48/31.97 ![X0]: (less_or_equal(multiply(additive_identity,additive_inverse(a)),X0)|less_or_equal(X0,multiply(additive_identity,additive_inverse(a)))|~defined(X0))),
% 131.48/31.97 inference(resolution,[status(thm)],[f1245,f66])).
% 131.48/31.97 fof(f44164,plain,(
% 131.48/31.97 ![X0]: (less_or_equal(multiply(additive_identity,additive_inverse(b)),X0)|less_or_equal(X0,multiply(additive_identity,additive_inverse(b)))|~defined(X0))),
% 131.48/31.97 inference(resolution,[status(thm)],[f1246,f66])).
% 131.48/31.97 fof(f44776,plain,(
% 131.48/31.97 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))),
% 131.48/31.97 inference(resolution,[status(thm)],[f36268,f1239])).
% 131.48/31.97 fof(f44918,definition,(
% 131.48/31.97 sQ7884_spl <=> (less_or_equal(multiply(multiplicative_identity,additive_identity),multiply(multiplicative_identity,additive_identity)))),
% 131.48/31.97 introduced(definition,[new_symbols(definition,[sQ7884_spl])],[split_symbol_definition])).
% 131.48/31.97 fof(f44921,plain,(
% 131.48/31.97 sQ7884_spl),
% 131.48/31.97 inference(split_clause,[status(thm)],[f44776,f44918])).
% 131.48/31.97 fof(f45026,plain,(
% 131.48/31.97 less_or_equal(multiply(additive_identity,b),multiply(additive_identity,b))|less_or_equal(multiply(additive_identity,b),multiply(additive_identity,b))),
% 131.48/31.97 inference(resolution,[status(thm)],[f36926,f1247])).
% 131.48/31.97 fof(f45162,definition,(
% 131.48/31.97 sQ7907_spl <=> (less_or_equal(multiply(additive_identity,b),multiply(additive_identity,b)))),
% 131.48/31.97 introduced(definition,[new_symbols(definition,[sQ7907_spl])],[split_symbol_definition])).
% 131.48/31.97 fof(f45165,plain,(
% 131.48/31.97 sQ7907_spl),
% 131.48/31.97 inference(split_clause,[status(thm)],[f45026,f45162])).
% 131.48/31.97 fof(f45269,plain,(
% 131.48/31.97 less_or_equal(multiply(additive_identity,a),multiply(additive_identity,a))|less_or_equal(multiply(additive_identity,a),multiply(additive_identity,a))),
% 131.48/31.97 inference(resolution,[status(thm)],[f40216,f1248])).
% 131.48/31.97 fof(f45393,definition,(
% 131.48/31.97 sQ7926_spl <=> (less_or_equal(multiply(additive_identity,a),multiply(additive_identity,a)))),
% 131.48/31.97 introduced(definition,[new_symbols(definition,[sQ7926_spl])],[split_symbol_definition])).
% 131.48/31.97 fof(f45396,plain,(
% 131.48/31.97 sQ7926_spl),
% 131.48/31.97 inference(split_clause,[status(thm)],[f45269,f45393])).
% 131.48/31.97 fof(f45507,plain,(
% 131.48/31.97 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))),
% 131.48/31.97 inference(resolution,[status(thm)],[f40874,f1249])).
% 131.48/31.97 fof(f45625,definition,(
% 131.48/31.97 sQ7945_spl <=> (less_or_equal(multiply(additive_identity,multiplicative_identity),multiply(additive_identity,multiplicative_identity)))),
% 131.48/31.97 introduced(definition,[new_symbols(definition,[sQ7945_spl])],[split_symbol_definition])).
% 131.48/31.97 fof(f45628,plain,(
% 131.48/31.97 sQ7945_spl),
% 131.48/31.97 inference(split_clause,[status(thm)],[f45507,f45625])).
% 131.48/31.97 fof(f45747,plain,(
% 131.48/31.97 less_or_equal(multiply(multiplicative_identity,additive_inverse(multiplicative_identity)),multiply(multiplicative_identity,additive_inverse(multiplicative_identity)))|less_or_equal(multiply(multiplicative_identity,additive_inverse(multiplicative_identity)),multiply(multiplicative_identity,additive_inverse(multiplicative_identity)))),
% 131.48/31.97 inference(resolution,[status(thm)],[f37584,f1233])).
% 131.48/31.97 fof(f45883,definition,(
% 131.48/31.97 sQ7970_spl <=> (less_or_equal(multiply(multiplicative_identity,additive_inverse(multiplicative_identity)),multiply(multiplicative_identity,additive_inverse(multiplicative_identity))))),
% 131.48/31.97 introduced(definition,[new_symbols(definition,[sQ7970_spl])],[split_symbol_definition])).
% 131.48/31.97 fof(f45886,plain,(
% 131.48/31.97 sQ7970_spl),
% 131.48/31.97 inference(split_clause,[status(thm)],[f45747,f45883])).
% 131.48/31.97 fof(f45973,plain,(
% 131.48/31.97 less_or_equal(multiply(multiplicative_identity,additive_inverse(a)),multiply(multiplicative_identity,additive_inverse(a)))|less_or_equal(multiply(multiplicative_identity,additive_inverse(a)),multiply(multiplicative_identity,additive_inverse(a)))),
% 131.48/31.97 inference(resolution,[status(thm)],[f38242,f1234])).
% 131.48/31.97 fof(f46103,definition,(
% 131.48/31.97 sQ7985_spl <=> (less_or_equal(multiply(multiplicative_identity,additive_inverse(a)),multiply(multiplicative_identity,additive_inverse(a))))),
% 131.48/31.97 introduced(definition,[new_symbols(definition,[sQ7985_spl])],[split_symbol_definition])).
% 131.48/31.97 fof(f46106,plain,(
% 131.48/31.97 sQ7985_spl),
% 131.48/31.97 inference(split_clause,[status(thm)],[f45973,f46103])).
% 131.48/31.97 fof(f46193,plain,(
% 131.48/31.97 less_or_equal(multiply(multiplicative_identity,additive_inverse(b)),multiply(multiplicative_identity,additive_inverse(b)))|less_or_equal(multiply(multiplicative_identity,additive_inverse(b)),multiply(multiplicative_identity,additive_inverse(b)))),
% 131.48/31.97 inference(resolution,[status(thm)],[f38900,f1235])).
% 131.48/31.97 fof(f46317,definition,(
% 131.48/31.97 sQ7998_spl <=> (less_or_equal(multiply(multiplicative_identity,additive_inverse(b)),multiply(multiplicative_identity,additive_inverse(b))))),
% 131.48/31.97 introduced(definition,[new_symbols(definition,[sQ7998_spl])],[split_symbol_definition])).
% 131.48/31.97 fof(f46320,plain,(
% 131.48/31.97 sQ7998_spl),
% 131.48/31.97 inference(split_clause,[status(thm)],[f46193,f46317])).
% 131.48/31.97 fof(f46611,plain,(
% 131.48/31.97 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))),
% 131.48/31.97 inference(resolution,[status(thm)],[f41532,f1250])).
% 131.48/31.97 fof(f46723,definition,(
% 131.48/31.97 sQ8018_spl <=> (less_or_equal(multiply(additive_identity,additive_identity),multiply(additive_identity,additive_identity)))),
% 131.48/31.97 introduced(definition,[new_symbols(definition,[sQ8018_spl])],[split_symbol_definition])).
% 131.48/31.97 fof(f46726,plain,(
% 131.48/31.97 sQ8018_spl),
% 131.48/31.97 inference(split_clause,[status(thm)],[f46611,f46723])).
% 131.48/31.97 fof(f46813,plain,(
% 131.48/31.97 less_or_equal(multiply(additive_identity,additive_inverse(additive_identity)),multiply(additive_identity,additive_inverse(additive_identity)))|less_or_equal(multiply(additive_identity,additive_inverse(additive_identity)),multiply(additive_identity,additive_inverse(additive_identity)))),
% 131.48/31.97 inference(resolution,[status(thm)],[f42190,f1243])).
% 131.48/31.97 fof(f46919,definition,(
% 131.48/31.97 sQ8025_spl <=> (less_or_equal(multiply(additive_identity,additive_inverse(additive_identity)),multiply(additive_identity,additive_inverse(additive_identity))))),
% 131.48/31.97 introduced(definition,[new_symbols(definition,[sQ8025_spl])],[split_symbol_definition])).
% 131.48/31.97 fof(f46922,plain,(
% 131.48/31.97 sQ8025_spl),
% 131.48/31.97 inference(split_clause,[status(thm)],[f46813,f46919])).
% 131.48/31.97 fof(f47009,plain,(
% 131.48/31.97 less_or_equal(multiply(additive_identity,additive_inverse(multiplicative_identity)),multiply(additive_identity,additive_inverse(multiplicative_identity)))|less_or_equal(multiply(additive_identity,additive_inverse(multiplicative_identity)),multiply(additive_identity,additive_inverse(multiplicative_identity)))),
% 131.48/31.97 inference(resolution,[status(thm)],[f42848,f1244])).
% 131.48/31.97 fof(f47109,definition,(
% 131.48/31.97 sQ8030_spl <=> (less_or_equal(multiply(additive_identity,additive_inverse(multiplicative_identity)),multiply(additive_identity,additive_inverse(multiplicative_identity))))),
% 131.48/31.97 introduced(definition,[new_symbols(definition,[sQ8030_spl])],[split_symbol_definition])).
% 131.48/31.97 fof(f47112,plain,(
% 131.48/31.97 sQ8030_spl),
% 131.48/31.97 inference(split_clause,[status(thm)],[f47009,f47109])).
% 131.48/31.97 fof(f47199,plain,(
% 131.48/31.97 less_or_equal(multiply(additive_identity,additive_inverse(a)),multiply(additive_identity,additive_inverse(a)))|less_or_equal(multiply(additive_identity,additive_inverse(a)),multiply(additive_identity,additive_inverse(a)))),
% 131.48/31.97 inference(resolution,[status(thm)],[f43506,f1245])).
% 131.48/31.97 fof(f47293,definition,(
% 131.48/31.97 sQ8033_spl <=> (less_or_equal(multiply(additive_identity,additive_inverse(a)),multiply(additive_identity,additive_inverse(a))))),
% 131.48/31.97 introduced(definition,[new_symbols(definition,[sQ8033_spl])],[split_symbol_definition])).
% 131.48/31.97 fof(f47296,plain,(
% 131.48/31.97 sQ8033_spl),
% 131.48/31.97 inference(split_clause,[status(thm)],[f47199,f47293])).
% 131.48/31.97 fof(f47383,plain,(
% 131.48/31.97 less_or_equal(multiply(additive_identity,additive_inverse(b)),multiply(additive_identity,additive_inverse(b)))|less_or_equal(multiply(additive_identity,additive_inverse(b)),multiply(additive_identity,additive_inverse(b)))),
% 131.48/31.97 inference(resolution,[status(thm)],[f44164,f1246])).
% 131.48/31.97 fof(f47471,definition,(
% 131.48/31.97 sQ8034_spl <=> (less_or_equal(multiply(additive_identity,additive_inverse(b)),multiply(additive_identity,additive_inverse(b))))),
% 131.48/31.97 introduced(definition,[new_symbols(definition,[sQ8034_spl])],[split_symbol_definition])).
% 131.48/31.97 fof(f47474,plain,(
% 131.48/31.97 sQ8034_spl),
% 131.48/31.97 inference(split_clause,[status(thm)],[f47383,f47471])).
% 131.48/31.97 fof(f71207,plain,(
% 131.48/31.97 ![X0]: (product(a,multiplicative_inverse(b),X0)|~product(b,multiplicative_inverse(b),X0)|~sQ0_spl)),
% 106.64/32.07 inference(resolution,[status(thm)],[f2363,f237])).
% 106.64/32.07 fof(f71380,plain,(
% 106.64/32.07 product(a,multiplicative_inverse(b),multiplicative_identity)|~sQ0_spl|~sQ8_spl),
% 106.64/32.07 inference(resolution,[status(thm)],[f71207,f2477])).
% 106.64/32.07 fof(f71441,plain,(
% 106.64/32.07 ![X0]: (product(multiplicative_inverse(a),multiplicative_identity,X0)|~product(multiplicative_identity,multiplicative_inverse(b),X0)|~sQ0_spl|~sQ8_spl|~sQ9_spl)),
% 106.64/32.07 inference(resolution,[status(thm)],[f71380,f742])).
% 106.64/32.07 fof(f85941,plain,(
% 106.64/32.07 product(multiplicative_inverse(a),multiplicative_identity,multiplicative_inverse(b))|~sQ8_spl|~sQ9_spl|~sQ0_spl),
% 106.64/32.07 inference(resolution,[status(thm)],[f71441,f2363])).
% 106.64/32.07 fof(f93940,plain,(
% 106.64/32.07 product(multiplicative_identity,multiplicative_inverse(a),multiplicative_inverse(b))|~sQ8_spl|~sQ9_spl|~sQ0_spl),
% 106.64/32.07 inference(resolution,[status(thm)],[f85941,f45])).
% 106.64/32.07 fof(f93944,plain,(
% 106.64/32.07 $false|~sQ8_spl|~sQ9_spl|~sQ0_spl),
% 106.64/32.07 inference(forward_subsumption_resolution,[status(thm)],[f93940,f75])).
% 106.64/32.07 fof(f93945,plain,(
% 106.64/32.07 ~sQ8_spl|~sQ9_spl|~sQ0_spl),
% 106.64/32.07 inference(contradiction_clause,[status(thm)],[f93944])).
% 106.64/32.07 fof(f93946,plain,(
% 106.64/32.07 $false),
% 106.64/32.07 inference(sat_refutation,[status(thm)],[f105,f134,f138,f148,f160,f190,f214,f232,f298,f370,f452,f544,f859,f1153,f1385,f1563,f2142,f2482,f4898,f4960,f5016,f5066,f5110,f6392,f6448,f6498,f8629,f8715,f8795,f8869,f9021,f13895,f14065,f14229,f14387,f14621,f14767,f14907,f15115,f15288,f15404,f15514,f15618,f15804,f22429,f22629,f22823,f22997,f23258,f23434,f23604,f23875,f24075,f24221,f24361,f24495,f24741,f33123,f33353,f33542,f33760,f34034,f34240,f34440,f34788,f35001,f35177,f35347,f35511,f35818,f44921,f45165,f45396,f45628,f45886,f46106,f46320,f46726,f46922,f47112,f47296,f47474,f93945])).
% 106.64/32.07 % SZS output end CNFRefutation for theBenchmark.p
% 3.30/32.11 % Elapsed time: 16.758513 seconds
% 3.30/32.11 % CPU time: 132.825023 seconds
% 3.30/32.11 % Total memory used: 714.875 MB
% 3.30/32.11 % Net memory used: 674.515 MB
%------------------------------------------------------------------------------