%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : FLD032-1 : TPTP v9.3.1. Bugfixed v2.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n005.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 12:22:22 PM UTC 2026
% Result : Unsatisfiable 10.94s 1.87s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : FLD032-1 : TPTP v9.3.1. Bugfixed v2.1.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.35 % Computer : n005.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Mon Sep 21 15:39:03 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.38 % Drodi V4.1.1
% 10.94/1.87 % Refutation found
% 10.94/1.87 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 10.94/1.87 % SZS output start CNFRefutation for theBenchmark
% 10.94/1.87 fof(f6,axiom,(
% 10.94/1.87 (![X]: (( equalish(multiply(multiplicative_identity,X),X)| ~ defined(X) ) ))),
% 10.94/1.87 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.94/1.87 fof(f7,axiom,(
% 10.94/1.87 (![X]: (( equalish(multiply(X,multiplicative_inverse(X)),multiplicative_identity)| ~ defined(X)| equalish(X,additive_identity) ) ))),
% 10.94/1.87 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.94/1.87 fof(f8,axiom,(
% 10.94/1.87 (![X,Y]: (( equalish(multiply(X,Y),multiply(Y,X))| ~ defined(X)| ~ defined(Y) ) ))),
% 10.94/1.87 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.94/1.87 fof(f10,axiom,(
% 10.94/1.87 (![X,Y]: (( defined(add(X,Y))| ~ defined(X)| ~ defined(Y) ) ))),
% 10.94/1.87 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.94/1.87 fof(f11,axiom,(
% 10.94/1.87 defined(additive_identity) ),
% 10.94/1.87 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.94/1.87 fof(f12,axiom,(
% 10.94/1.87 (![X]: (( defined(additive_inverse(X))| ~ defined(X) ) ))),
% 10.94/1.87 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.94/1.87 fof(f13,axiom,(
% 10.94/1.87 (![X,Y]: (( defined(multiply(X,Y))| ~ defined(X)| ~ defined(Y) ) ))),
% 10.94/1.87 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.94/1.87 fof(f14,axiom,(
% 10.94/1.87 defined(multiplicative_identity) ),
% 10.94/1.87 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.94/1.87 fof(f15,axiom,(
% 10.94/1.87 (![X]: (( defined(multiplicative_inverse(X))| ~ defined(X)| equalish(X,additive_identity) ) ))),
% 10.94/1.87 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.94/1.87 fof(f18,axiom,(
% 10.94/1.87 (![X,Y]: (( less_or_equal(X,Y)| less_or_equal(Y,X)| ~ defined(X)| ~ defined(Y) ) ))),
% 10.94/1.87 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.94/1.87 fof(f22,axiom,(
% 10.94/1.87 (![X,Y]: (( equalish(X,Y)| ~ equalish(Y,X) ) ))),
% 10.94/1.87 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.94/1.87 fof(f23,axiom,(
% 10.94/1.87 (![X,Z,Y]: (( equalish(X,Z)| ~ equalish(X,Y)| ~ equalish(Y,Z) ) ))),
% 10.94/1.87 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.94/1.87 fof(f25,axiom,(
% 10.94/1.87 (![X,Z,Y]: (( equalish(multiply(X,Z),multiply(Y,Z))| ~ defined(Z)| ~ equalish(X,Y) ) ))),
% 10.94/1.87 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.94/1.87 fof(f28,hypothesis,(
% 10.94/1.87 defined(a) ),
% 10.94/1.87 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.94/1.87 fof(f29,negated_conjecture,(
% 10.94/1.87 ~ equalish(a,additive_identity) ),
% 10.94/1.87 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.94/1.87 fof(f30,negated_conjecture,(
% 10.94/1.87 equalish(multiplicative_inverse(a),multiplicative_identity) ),
% 10.94/1.87 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.94/1.87 fof(f31,negated_conjecture,(
% 10.94/1.87 ~ equalish(a,multiplicative_identity) ),
% 10.94/1.87 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 10.94/1.87 fof(f40,plain,(
% 10.94/1.87 ![X0]: (equalish(multiply(multiplicative_identity,X0),X0)|~defined(X0))),
% 10.94/1.87 inference(cnf_transformation,[status(thm)],[f6])).
% 10.94/1.87 fof(f41,plain,(
% 10.94/1.87 ![X0]: (equalish(multiply(X0,multiplicative_inverse(X0)),multiplicative_identity)|~defined(X0)|equalish(X0,additive_identity))),
% 10.94/1.87 inference(cnf_transformation,[status(thm)],[f7])).
% 10.94/1.87 fof(f42,plain,(
% 10.94/1.87 ![Y]: ((![X]: (equalish(multiply(X,Y),multiply(Y,X))|~defined(X)))|~defined(Y))),
% 10.94/1.87 inference(miniscoping,[status(thm)],[f8])).
% 10.94/1.87 fof(f43,plain,(
% 10.94/1.87 ![X0,X1]: (equalish(multiply(X0,X1),multiply(X1,X0))|~defined(X0)|~defined(X1))),
% 10.94/1.87 inference(cnf_transformation,[status(thm)],[f42])).
% 10.94/1.87 fof(f46,plain,(
% 10.94/1.87 ![Y]: ((![X]: (defined(add(X,Y))|~defined(X)))|~defined(Y))),
% 10.94/1.87 inference(miniscoping,[status(thm)],[f10])).
% 10.94/1.87 fof(f47,plain,(
% 10.94/1.87 ![X0,X1]: (defined(add(X0,X1))|~defined(X0)|~defined(X1))),
% 10.94/1.87 inference(cnf_transformation,[status(thm)],[f46])).
% 10.94/1.87 fof(f48,plain,(
% 10.94/1.87 defined(additive_identity)),
% 10.94/1.87 inference(cnf_transformation,[status(thm)],[f11])).
% 10.94/1.87 fof(f49,plain,(
% 10.94/1.87 ![X0]: (defined(additive_inverse(X0))|~defined(X0))),
% 10.94/1.87 inference(cnf_transformation,[status(thm)],[f12])).
% 10.94/1.87 fof(f50,plain,(
% 10.94/1.87 ![Y]: ((![X]: (defined(multiply(X,Y))|~defined(X)))|~defined(Y))),
% 10.94/1.87 inference(miniscoping,[status(thm)],[f13])).
% 10.94/1.87 fof(f51,plain,(
% 10.94/1.87 ![X0,X1]: (defined(multiply(X0,X1))|~defined(X0)|~defined(X1))),
% 10.94/1.87 inference(cnf_transformation,[status(thm)],[f50])).
% 10.94/1.87 fof(f52,plain,(
% 10.94/1.87 defined(multiplicative_identity)),
% 10.94/1.87 inference(cnf_transformation,[status(thm)],[f14])).
% 10.94/1.87 fof(f53,plain,(
% 10.94/1.87 ![X0]: (defined(multiplicative_inverse(X0))|~defined(X0)|equalish(X0,additive_identity))),
% 10.94/1.87 inference(cnf_transformation,[status(thm)],[f15])).
% 10.94/1.87 fof(f57,plain,(
% 10.94/1.87 ![Y]: ((![X]: ((less_or_equal(X,Y)|less_or_equal(Y,X))|~defined(X)))|~defined(Y))),
% 10.94/1.87 inference(miniscoping,[status(thm)],[f18])).
% 10.94/1.87 fof(f58,plain,(
% 10.94/1.87 ![X0,X1]: (less_or_equal(X0,X1)|less_or_equal(X1,X0)|~defined(X0)|~defined(X1))),
% 10.94/1.87 inference(cnf_transformation,[status(thm)],[f57])).
% 10.94/1.87 fof(f64,plain,(
% 10.94/1.87 ![X0,X1]: (equalish(X0,X1)|~equalish(X1,X0))),
% 10.94/1.87 inference(cnf_transformation,[status(thm)],[f22])).
% 10.94/1.87 fof(f65,plain,(
% 10.94/1.87 ![Z,Y]: ((![X]: (equalish(X,Z)|~equalish(X,Y)))|~equalish(Y,Z))),
% 10.94/1.87 inference(miniscoping,[status(thm)],[f23])).
% 10.94/1.87 fof(f66,plain,(
% 10.94/1.87 ![X0,X1,X2]: (equalish(X0,X1)|~equalish(X0,X2)|~equalish(X2,X1))),
% 10.94/1.87 inference(cnf_transformation,[status(thm)],[f65])).
% 10.94/1.87 fof(f69,plain,(
% 10.94/1.87 ![X,Y]: ((![Z]: (equalish(multiply(X,Z),multiply(Y,Z))|~defined(Z)))|~equalish(X,Y))),
% 10.94/1.87 inference(miniscoping,[status(thm)],[f25])).
% 10.94/1.87 fof(f70,plain,(
% 10.94/1.87 ![X0,X1,X2]: (equalish(multiply(X0,X1),multiply(X2,X1))|~defined(X1)|~equalish(X0,X2))),
% 10.94/1.87 inference(cnf_transformation,[status(thm)],[f69])).
% 10.94/1.87 fof(f74,plain,(
% 10.94/1.87 defined(a)),
% 10.94/1.87 inference(cnf_transformation,[status(thm)],[f28])).
% 10.94/1.87 fof(f75,plain,(
% 10.94/1.87 ~equalish(a,additive_identity)),
% 10.94/1.87 inference(cnf_transformation,[status(thm)],[f29])).
% 10.94/1.87 fof(f76,plain,(
% 10.94/1.87 equalish(multiplicative_inverse(a),multiplicative_identity)),
% 10.94/1.87 inference(cnf_transformation,[status(thm)],[f30])).
% 10.94/1.87 fof(f77,plain,(
% 10.94/1.87 ~equalish(a,multiplicative_identity)),
% 10.94/1.87 inference(cnf_transformation,[status(thm)],[f31])).
% 10.94/1.87 fof(f85,plain,(
% 10.94/1.87 equalish(multiply(multiplicative_identity,a),a)),
% 10.94/1.87 inference(resolution,[status(thm)],[f74,f40])).
% 10.94/1.87 fof(f99,plain,(
% 10.94/1.87 ![X0]: (equalish(multiply(a,X0),multiply(X0,a))|~defined(X0))),
% 10.94/1.87 inference(resolution,[status(thm)],[f43,f74])).
% 10.94/1.87 fof(f105,plain,(
% 10.94/1.87 defined(multiplicative_inverse(a))|equalish(a,additive_identity)),
% 10.94/1.87 inference(resolution,[status(thm)],[f53,f74])).
% 10.94/1.87 fof(f108,definition,(
% 10.94/1.87 sQ0_spl <=> (defined(multiplicative_inverse(a)))),
% 10.94/1.87 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 10.94/1.87 fof(f109,plain,(
% 10.94/1.87 defined(multiplicative_inverse(a))|~sQ0_spl),
% 10.94/1.87 inference(component_clause,[status(thm)],[f108])).
% 10.94/1.87 fof(f111,definition,(
% 10.94/1.87 sQ1_spl <=> (equalish(a,additive_identity))),
% 10.94/1.87 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 10.94/1.87 fof(f112,plain,(
% 10.94/1.87 equalish(a,additive_identity)|~sQ1_spl),
% 10.94/1.87 inference(component_clause,[status(thm)],[f111])).
% 10.94/1.87 fof(f114,plain,(
% 10.94/1.87 sQ0_spl|sQ1_spl),
% 10.94/1.87 inference(split_clause,[status(thm)],[f105,f108,f111])).
% 10.94/1.87 fof(f129,plain,(
% 10.94/1.87 equalish(multiply(a,multiplicative_inverse(a)),multiplicative_identity)|equalish(a,additive_identity)),
% 10.94/1.87 inference(resolution,[status(thm)],[f41,f74])).
% 10.94/1.87 fof(f132,definition,(
% 10.94/1.87 sQ6_spl <=> (equalish(multiply(a,multiplicative_inverse(a)),multiplicative_identity))),
% 10.94/1.87 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 10.94/1.87 fof(f133,plain,(
% 10.94/1.87 equalish(multiply(a,multiplicative_inverse(a)),multiplicative_identity)|~sQ6_spl),
% 10.94/1.87 inference(component_clause,[status(thm)],[f132])).
% 10.94/1.87 fof(f135,plain,(
% 10.94/1.87 sQ6_spl|sQ1_spl),
% 10.94/1.87 inference(split_clause,[status(thm)],[f129,f132,f111])).
% 10.94/1.87 fof(f144,plain,(
% 10.94/1.87 $false|~sQ1_spl),
% 10.94/1.87 inference(forward_subsumption_resolution,[status(thm)],[f112,f75])).
% 10.94/1.87 fof(f145,plain,(
% 10.94/1.87 ~sQ1_spl),
% 10.94/1.87 inference(contradiction_clause,[status(thm)],[f144])).
% 10.94/1.87 fof(f195,plain,(
% 10.94/1.87 equalish(multiplicative_identity,multiplicative_inverse(a))),
% 10.94/1.87 inference(resolution,[status(thm)],[f64,f76])).
% 10.94/1.87 fof(f197,plain,(
% 10.94/1.87 ![X0]: (equalish(multiplicative_identity,X0)|~equalish(multiplicative_inverse(a),X0))),
% 10.94/1.87 inference(resolution,[status(thm)],[f66,f195])).
% 10.94/1.87 fof(f199,plain,(
% 10.94/1.87 ![X0]: (equalish(multiplicative_inverse(a),X0)|~equalish(multiplicative_identity,X0))),
% 10.94/1.87 inference(resolution,[status(thm)],[f66,f76])).
% 10.94/1.87 fof(f413,plain,(
% 10.94/1.87 equalish(multiply(a,multiplicative_inverse(a)),multiply(multiplicative_inverse(a),a))|~sQ0_spl),
% 10.94/1.87 inference(resolution,[status(thm)],[f99,f109])).
% 10.94/1.87 fof(f443,plain,(
% 10.94/1.87 equalish(multiplicative_identity,multiply(a,multiplicative_inverse(a)))|~sQ6_spl),
% 10.94/1.87 inference(resolution,[status(thm)],[f133,f64])).
% 10.94/1.87 fof(f514,plain,(
% 10.94/1.87 defined(additive_inverse(a))),
% 10.94/1.87 inference(resolution,[status(thm)],[f49,f74])).
% 10.94/1.87 fof(f515,plain,(
% 10.94/1.87 defined(additive_inverse(multiplicative_identity))),
% 10.94/1.87 inference(resolution,[status(thm)],[f49,f52])).
% 10.94/1.87 fof(f516,plain,(
% 10.94/1.87 defined(additive_inverse(additive_identity))),
% 10.94/1.87 inference(resolution,[status(thm)],[f49,f48])).
% 10.94/1.87 fof(f517,plain,(
% 10.94/1.87 defined(additive_inverse(additive_inverse(a)))),
% 10.94/1.87 inference(resolution,[status(thm)],[f514,f49])).
% 10.94/1.87 fof(f543,plain,(
% 10.94/1.87 ![X0]: (less_or_equal(additive_inverse(a),X0)|less_or_equal(X0,additive_inverse(a))|~defined(X0))),
% 10.94/1.87 inference(resolution,[status(thm)],[f514,f58])).
% 10.94/1.87 fof(f601,plain,(
% 10.94/1.87 defined(additive_inverse(additive_inverse(multiplicative_identity)))),
% 10.94/1.87 inference(resolution,[status(thm)],[f515,f49])).
% 10.94/1.87 fof(f627,plain,(
% 10.94/1.87 ![X0]: (less_or_equal(additive_inverse(multiplicative_identity),X0)|less_or_equal(X0,additive_inverse(multiplicative_identity))|~defined(X0))),
% 10.94/1.87 inference(resolution,[status(thm)],[f515,f58])).
% 10.94/1.87 fof(f689,plain,(
% 10.94/1.87 ![X0]: (defined(add(a,X0))|~defined(X0))),
% 10.94/1.87 inference(resolution,[status(thm)],[f47,f74])).
% 10.94/1.87 fof(f690,plain,(
% 10.94/1.87 ![X0]: (defined(add(multiplicative_identity,X0))|~defined(X0))),
% 10.94/1.87 inference(resolution,[status(thm)],[f47,f52])).
% 10.94/1.87 fof(f691,plain,(
% 10.94/1.87 ![X0]: (defined(add(additive_identity,X0))|~defined(X0))),
% 10.94/1.87 inference(resolution,[status(thm)],[f47,f48])).
% 10.94/1.87 fof(f696,plain,(
% 10.94/1.87 ![X0]: (defined(multiply(a,X0))|~defined(X0))),
% 10.94/1.87 inference(resolution,[status(thm)],[f51,f74])).
% 10.94/1.87 fof(f697,plain,(
% 10.94/1.87 ![X0]: (defined(multiply(multiplicative_identity,X0))|~defined(X0))),
% 10.94/1.87 inference(resolution,[status(thm)],[f51,f52])).
% 10.94/1.87 fof(f698,plain,(
% 10.94/1.87 ![X0]: (defined(multiply(additive_identity,X0))|~defined(X0))),
% 10.94/1.87 inference(resolution,[status(thm)],[f51,f48])).
% 10.94/1.87 fof(f736,definition,(
% 10.94/1.87 sQ72_spl <=> (equalish(a,multiplicative_identity))),
% 10.94/1.87 introduced(definition,[new_symbols(definition,[sQ72_spl])],[split_symbol_definition])).
% 10.94/1.87 fof(f737,plain,(
% 10.94/1.87 equalish(a,multiplicative_identity)|~sQ72_spl),
% 10.94/1.87 inference(component_clause,[status(thm)],[f736])).
% 10.94/1.87 fof(f745,plain,(
% 10.94/1.87 $false|~sQ72_spl),
% 10.94/1.87 inference(forward_subsumption_resolution,[status(thm)],[f737,f77])).
% 10.94/1.87 fof(f746,plain,(
% 10.94/1.87 ~sQ72_spl),
% 10.94/1.87 inference(contradiction_clause,[status(thm)],[f745])).
% 10.94/1.87 fof(f773,plain,(
% 10.94/1.87 less_or_equal(additive_inverse(a),additive_inverse(a))|less_or_equal(additive_inverse(a),additive_inverse(a))),
% 10.94/1.87 inference(resolution,[status(thm)],[f543,f514])).
% 10.94/1.87 fof(f786,definition,(
% 10.94/1.87 sQ76_spl <=> (less_or_equal(additive_inverse(a),additive_inverse(a)))),
% 10.94/1.87 introduced(definition,[new_symbols(definition,[sQ76_spl])],[split_symbol_definition])).
% 10.94/1.87 fof(f789,plain,(
% 10.94/1.87 sQ76_spl),
% 10.94/1.87 inference(split_clause,[status(thm)],[f773,f786])).
% 10.94/1.87 fof(f795,plain,(
% 10.94/1.87 less_or_equal(additive_inverse(multiplicative_identity),additive_inverse(multiplicative_identity))|less_or_equal(additive_inverse(multiplicative_identity),additive_inverse(multiplicative_identity))),
% 10.94/1.87 inference(resolution,[status(thm)],[f627,f515])).
% 10.94/1.87 fof(f802,definition,(
% 10.94/1.87 sQ77_spl <=> (less_or_equal(additive_inverse(multiplicative_identity),additive_inverse(multiplicative_identity)))),
% 10.94/1.87 introduced(definition,[new_symbols(definition,[sQ77_spl])],[split_symbol_definition])).
% 10.94/1.87 fof(f805,plain,(
% 10.94/1.87 sQ77_spl),
% 10.94/1.87 inference(split_clause,[status(thm)],[f795,f802])).
% 10.94/1.87 fof(f848,plain,(
% 10.94/1.87 defined(additive_inverse(additive_inverse(additive_identity)))),
% 10.94/1.87 inference(resolution,[status(thm)],[f516,f49])).
% 10.94/1.87 fof(f874,plain,(
% 10.94/1.87 ![X0]: (less_or_equal(additive_inverse(additive_identity),X0)|less_or_equal(X0,additive_inverse(additive_identity))|~defined(X0))),
% 10.94/1.87 inference(resolution,[status(thm)],[f516,f58])).
% 10.94/1.87 fof(f946,plain,(
% 10.94/1.87 less_or_equal(additive_inverse(additive_identity),additive_inverse(additive_identity))|less_or_equal(additive_inverse(additive_identity),additive_inverse(additive_identity))),
% 10.94/1.87 inference(resolution,[status(thm)],[f874,f516])).
% 10.94/1.87 fof(f954,definition,(
% 10.94/1.87 sQ95_spl <=> (less_or_equal(additive_inverse(additive_identity),additive_inverse(additive_identity)))),
% 10.94/1.88 introduced(definition,[new_symbols(definition,[sQ95_spl])],[split_symbol_definition])).
% 10.94/1.88 fof(f957,plain,(
% 10.94/1.88 sQ95_spl),
% 10.94/1.88 inference(split_clause,[status(thm)],[f946,f954])).
% 10.94/1.88 fof(f976,plain,(
% 10.94/1.88 defined(add(a,a))),
% 10.94/1.88 inference(resolution,[status(thm)],[f689,f74])).
% 10.94/1.88 fof(f977,plain,(
% 10.94/1.88 defined(add(a,multiplicative_identity))),
% 10.94/1.88 inference(resolution,[status(thm)],[f689,f52])).
% 10.94/1.88 fof(f978,plain,(
% 10.94/1.88 defined(add(a,additive_identity))),
% 10.94/1.88 inference(resolution,[status(thm)],[f689,f48])).
% 10.94/1.88 fof(f984,plain,(
% 10.94/1.88 defined(add(multiplicative_identity,a))),
% 10.94/1.88 inference(resolution,[status(thm)],[f690,f74])).
% 10.94/1.88 fof(f985,plain,(
% 10.94/1.88 defined(add(multiplicative_identity,multiplicative_identity))),
% 10.94/1.88 inference(resolution,[status(thm)],[f690,f52])).
% 10.94/1.88 fof(f986,plain,(
% 10.94/1.88 defined(add(multiplicative_identity,additive_identity))),
% 10.94/1.88 inference(resolution,[status(thm)],[f690,f48])).
% 10.94/1.88 fof(f992,plain,(
% 10.94/1.88 defined(add(additive_identity,a))),
% 10.94/1.88 inference(resolution,[status(thm)],[f691,f74])).
% 10.94/1.88 fof(f993,plain,(
% 10.94/1.88 defined(add(additive_identity,multiplicative_identity))),
% 10.94/1.88 inference(resolution,[status(thm)],[f691,f52])).
% 10.94/1.88 fof(f994,plain,(
% 10.94/1.88 defined(add(additive_identity,additive_identity))),
% 10.94/1.88 inference(resolution,[status(thm)],[f691,f48])).
% 10.94/1.88 fof(f1000,plain,(
% 10.94/1.88 defined(multiply(a,a))),
% 10.94/1.88 inference(resolution,[status(thm)],[f696,f74])).
% 10.94/1.88 fof(f1001,plain,(
% 10.94/1.88 defined(multiply(a,multiplicative_identity))),
% 10.94/1.88 inference(resolution,[status(thm)],[f696,f52])).
% 10.94/1.88 fof(f1002,plain,(
% 10.94/1.88 defined(multiply(a,additive_identity))),
% 10.94/1.88 inference(resolution,[status(thm)],[f696,f48])).
% 10.94/1.88 fof(f1008,plain,(
% 10.94/1.88 defined(multiply(multiplicative_identity,a))),
% 10.94/1.88 inference(resolution,[status(thm)],[f697,f74])).
% 10.94/1.88 fof(f1009,plain,(
% 10.94/1.88 defined(multiply(multiplicative_identity,multiplicative_identity))),
% 10.94/1.88 inference(resolution,[status(thm)],[f697,f52])).
% 10.94/1.88 fof(f1010,plain,(
% 10.94/1.88 defined(multiply(multiplicative_identity,additive_identity))),
% 10.94/1.88 inference(resolution,[status(thm)],[f697,f48])).
% 10.94/1.88 fof(f1016,plain,(
% 10.94/1.88 defined(multiply(additive_identity,a))),
% 10.94/1.88 inference(resolution,[status(thm)],[f698,f74])).
% 10.94/1.88 fof(f1017,plain,(
% 10.94/1.88 defined(multiply(additive_identity,multiplicative_identity))),
% 10.94/1.88 inference(resolution,[status(thm)],[f698,f52])).
% 10.94/1.88 fof(f1018,plain,(
% 10.94/1.88 defined(multiply(additive_identity,additive_identity))),
% 10.94/1.88 inference(resolution,[status(thm)],[f698,f48])).
% 10.94/1.88 fof(f1707,plain,(
% 10.94/1.88 ![X0,X1]: (equalish(multiply(X0,a),multiply(X1,a))|~equalish(X0,X1))),
% 10.94/1.88 inference(resolution,[status(thm)],[f70,f74])).
% 10.94/1.88 fof(f1784,plain,(
% 10.94/1.88 equalish(multiply(multiplicative_inverse(a),a),multiply(multiplicative_identity,a))),
% 10.94/1.88 inference(resolution,[status(thm)],[f1707,f76])).
% 10.94/1.88 fof(f2051,plain,(
% 10.94/1.88 ![X0]: (equalish(multiply(multiplicative_inverse(a),a),X0)|~equalish(multiply(multiplicative_identity,a),X0))),
% 10.94/1.88 inference(resolution,[status(thm)],[f1784,f66])).
% 10.94/1.88 fof(f2548,plain,(
% 10.94/1.88 ![X0]: (less_or_equal(additive_inverse(additive_inverse(a)),X0)|less_or_equal(X0,additive_inverse(additive_inverse(a)))|~defined(X0))),
% 10.94/1.88 inference(resolution,[status(thm)],[f517,f58])).
% 10.94/1.88 fof(f2792,plain,(
% 10.94/1.88 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)))),
% 10.94/1.88 inference(resolution,[status(thm)],[f2548,f517])).
% 10.94/1.88 fof(f2804,definition,(
% 10.94/1.88 sQ191_spl <=> (less_or_equal(additive_inverse(additive_inverse(a)),additive_inverse(additive_inverse(a))))),
% 10.94/1.88 introduced(definition,[new_symbols(definition,[sQ191_spl])],[split_symbol_definition])).
% 10.94/1.88 fof(f2807,plain,(
% 10.94/1.88 sQ191_spl),
% 10.94/1.88 inference(split_clause,[status(thm)],[f2792,f2804])).
% 10.94/1.88 fof(f3015,plain,(
% 10.94/1.88 equalish(multiply(multiplicative_inverse(a),a),a)),
% 10.94/1.88 inference(resolution,[status(thm)],[f2051,f85])).
% 10.94/1.88 fof(f3095,plain,(
% 10.94/1.88 equalish(a,multiply(multiplicative_inverse(a),a))),
% 10.94/1.88 inference(resolution,[status(thm)],[f3015,f64])).
% 10.94/1.88 fof(f3104,plain,(
% 10.94/1.88 ![X0]: (equalish(a,X0)|~equalish(multiply(multiplicative_inverse(a),a),X0))),
% 10.94/1.88 inference(resolution,[status(thm)],[f3095,f66])).
% 10.94/1.88 fof(f3431,plain,(
% 10.94/1.88 ![X0]: (less_or_equal(additive_inverse(additive_inverse(multiplicative_identity)),X0)|less_or_equal(X0,additive_inverse(additive_inverse(multiplicative_identity)))|~defined(X0))),
% 10.94/1.88 inference(resolution,[status(thm)],[f601,f58])).
% 10.94/1.88 fof(f3680,plain,(
% 10.94/1.88 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)))),
% 10.94/1.88 inference(resolution,[status(thm)],[f3431,f601])).
% 10.94/1.88 fof(f3693,definition,(
% 10.94/1.88 sQ222_spl <=> (less_or_equal(additive_inverse(additive_inverse(multiplicative_identity)),additive_inverse(additive_inverse(multiplicative_identity))))),
% 10.94/1.88 introduced(definition,[new_symbols(definition,[sQ222_spl])],[split_symbol_definition])).
% 10.94/1.88 fof(f3696,plain,(
% 10.94/1.88 sQ222_spl),
% 10.94/1.88 inference(split_clause,[status(thm)],[f3680,f3693])).
% 10.94/1.88 fof(f4427,plain,(
% 10.94/1.88 ![X0]: (less_or_equal(additive_inverse(additive_inverse(additive_identity)),X0)|less_or_equal(X0,additive_inverse(additive_inverse(additive_identity)))|~defined(X0))),
% 10.94/1.88 inference(resolution,[status(thm)],[f848,f58])).
% 10.94/1.88 fof(f4583,plain,(
% 10.94/1.88 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)))),
% 10.94/1.88 inference(resolution,[status(thm)],[f4427,f848])).
% 10.94/1.88 fof(f4597,definition,(
% 10.94/1.88 sQ252_spl <=> (less_or_equal(additive_inverse(additive_inverse(additive_identity)),additive_inverse(additive_inverse(additive_identity))))),
% 10.94/1.88 introduced(definition,[new_symbols(definition,[sQ252_spl])],[split_symbol_definition])).
% 10.94/1.88 fof(f4600,plain,(
% 10.94/1.88 sQ252_spl),
% 10.94/1.88 inference(split_clause,[status(thm)],[f4583,f4597])).
% 10.94/1.88 fof(f5951,plain,(
% 10.94/1.88 ![X0]: (less_or_equal(add(a,a),X0)|less_or_equal(X0,add(a,a))|~defined(X0))),
% 10.94/1.88 inference(resolution,[status(thm)],[f976,f58])).
% 10.94/1.88 fof(f6135,plain,(
% 10.94/1.88 ![X0]: (less_or_equal(add(a,multiplicative_identity),X0)|less_or_equal(X0,add(a,multiplicative_identity))|~defined(X0))),
% 10.94/1.88 inference(resolution,[status(thm)],[f977,f58])).
% 10.94/1.88 fof(f6378,plain,(
% 10.94/1.88 ![X0]: (less_or_equal(add(a,additive_identity),X0)|less_or_equal(X0,add(a,additive_identity))|~defined(X0))),
% 10.94/1.88 inference(resolution,[status(thm)],[f978,f58])).
% 10.94/1.88 fof(f6565,plain,(
% 10.94/1.88 ![X0]: (less_or_equal(add(multiplicative_identity,a),X0)|less_or_equal(X0,add(multiplicative_identity,a))|~defined(X0))),
% 10.94/1.88 inference(resolution,[status(thm)],[f984,f58])).
% 10.94/1.88 fof(f6752,plain,(
% 10.94/1.88 ![X0]: (less_or_equal(add(multiplicative_identity,multiplicative_identity),X0)|less_or_equal(X0,add(multiplicative_identity,multiplicative_identity))|~defined(X0))),
% 10.94/1.88 inference(resolution,[status(thm)],[f985,f58])).
% 10.94/1.88 fof(f6980,plain,(
% 10.94/1.88 less_or_equal(add(a,a),add(a,a))|less_or_equal(add(a,a),add(a,a))),
% 10.94/1.88 inference(resolution,[status(thm)],[f5951,f976])).
% 10.94/1.88 fof(f7023,definition,(
% 10.94/1.88 sQ419_spl <=> (less_or_equal(add(a,a),add(a,a)))),
% 10.94/1.88 introduced(definition,[new_symbols(definition,[sQ419_spl])],[split_symbol_definition])).
% 10.94/1.88 fof(f7026,plain,(
% 10.94/1.88 sQ419_spl),
% 10.94/1.88 inference(split_clause,[status(thm)],[f6980,f7023])).
% 10.94/1.88 fof(f7044,plain,(
% 10.94/1.88 less_or_equal(add(a,multiplicative_identity),add(a,multiplicative_identity))|less_or_equal(add(a,multiplicative_identity),add(a,multiplicative_identity))),
% 10.94/1.88 inference(resolution,[status(thm)],[f6135,f977])).
% 10.94/1.88 fof(f7081,definition,(
% 10.94/1.88 sQ426_spl <=> (less_or_equal(add(a,multiplicative_identity),add(a,multiplicative_identity)))),
% 10.94/1.88 introduced(definition,[new_symbols(definition,[sQ426_spl])],[split_symbol_definition])).
% 10.94/1.88 fof(f7084,plain,(
% 10.94/1.88 sQ426_spl),
% 10.94/1.88 inference(split_clause,[status(thm)],[f7044,f7081])).
% 10.94/1.88 fof(f7102,plain,(
% 10.94/1.88 less_or_equal(add(a,additive_identity),add(a,additive_identity))|less_or_equal(add(a,additive_identity),add(a,additive_identity))),
% 10.94/1.88 inference(resolution,[status(thm)],[f6378,f978])).
% 10.94/1.88 fof(f7133,definition,(
% 10.94/1.88 sQ431_spl <=> (less_or_equal(add(a,additive_identity),add(a,additive_identity)))),
% 10.94/1.88 introduced(definition,[new_symbols(definition,[sQ431_spl])],[split_symbol_definition])).
% 10.94/1.88 fof(f7136,plain,(
% 10.94/1.88 sQ431_spl),
% 10.94/1.88 inference(split_clause,[status(thm)],[f7102,f7133])).
% 10.94/1.88 fof(f7154,plain,(
% 10.94/1.88 less_or_equal(add(multiplicative_identity,a),add(multiplicative_identity,a))|less_or_equal(add(multiplicative_identity,a),add(multiplicative_identity,a))),
% 10.94/1.88 inference(resolution,[status(thm)],[f6565,f984])).
% 10.94/1.88 fof(f7179,definition,(
% 10.94/1.88 sQ434_spl <=> (less_or_equal(add(multiplicative_identity,a),add(multiplicative_identity,a)))),
% 10.94/1.88 introduced(definition,[new_symbols(definition,[sQ434_spl])],[split_symbol_definition])).
% 10.94/1.88 fof(f7182,plain,(
% 10.94/1.88 sQ434_spl),
% 10.94/1.88 inference(split_clause,[status(thm)],[f7154,f7179])).
% 10.94/1.88 fof(f7200,plain,(
% 10.94/1.88 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))),
% 10.94/1.88 inference(resolution,[status(thm)],[f6752,f985])).
% 10.94/1.88 fof(f7219,definition,(
% 10.94/1.88 sQ435_spl <=> (less_or_equal(add(multiplicative_identity,multiplicative_identity),add(multiplicative_identity,multiplicative_identity)))),
% 10.94/1.88 introduced(definition,[new_symbols(definition,[sQ435_spl])],[split_symbol_definition])).
% 10.94/1.88 fof(f7222,plain,(
% 10.94/1.88 sQ435_spl),
% 10.94/1.88 inference(split_clause,[status(thm)],[f7200,f7219])).
% 10.94/1.88 fof(f7770,plain,(
% 10.94/1.88 ![X0]: (less_or_equal(add(multiplicative_identity,additive_identity),X0)|less_or_equal(X0,add(multiplicative_identity,additive_identity))|~defined(X0))),
% 10.94/1.88 inference(resolution,[status(thm)],[f986,f58])).
% 10.94/1.88 fof(f8002,plain,(
% 10.94/1.88 ![X0]: (less_or_equal(add(additive_identity,a),X0)|less_or_equal(X0,add(additive_identity,a))|~defined(X0))),
% 10.94/1.88 inference(resolution,[status(thm)],[f992,f58])).
% 10.94/1.88 fof(f8258,plain,(
% 10.94/1.88 ![X0]: (less_or_equal(add(additive_identity,multiplicative_identity),X0)|less_or_equal(X0,add(additive_identity,multiplicative_identity))|~defined(X0))),
% 10.94/1.88 inference(resolution,[status(thm)],[f993,f58])).
% 10.94/1.88 fof(f8490,plain,(
% 10.94/1.88 ![X0]: (less_or_equal(add(additive_identity,additive_identity),X0)|less_or_equal(X0,add(additive_identity,additive_identity))|~defined(X0))),
% 10.94/1.88 inference(resolution,[status(thm)],[f994,f58])).
% 10.94/1.88 fof(f8722,plain,(
% 10.94/1.88 ![X0]: (less_or_equal(multiply(a,a),X0)|less_or_equal(X0,multiply(a,a))|~defined(X0))),
% 10.94/1.88 inference(resolution,[status(thm)],[f1000,f58])).
% 10.94/1.88 fof(f9026,plain,(
% 10.94/1.88 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))),
% 10.94/1.88 inference(resolution,[status(thm)],[f7770,f986])).
% 10.94/1.88 fof(f9074,definition,(
% 10.94/1.88 sQ649_spl <=> (less_or_equal(add(multiplicative_identity,additive_identity),add(multiplicative_identity,additive_identity)))),
% 10.94/1.88 introduced(definition,[new_symbols(definition,[sQ649_spl])],[split_symbol_definition])).
% 10.94/1.88 fof(f9077,plain,(
% 10.94/1.88 sQ649_spl),
% 10.94/1.88 inference(split_clause,[status(thm)],[f9026,f9074])).
% 10.94/1.88 fof(f9100,plain,(
% 10.94/1.88 less_or_equal(add(additive_identity,a),add(additive_identity,a))|less_or_equal(add(additive_identity,a),add(additive_identity,a))),
% 10.94/1.88 inference(resolution,[status(thm)],[f8002,f992])).
% 10.94/1.88 fof(f9142,definition,(
% 10.94/1.88 sQ656_spl <=> (less_or_equal(add(additive_identity,a),add(additive_identity,a)))),
% 10.94/1.88 introduced(definition,[new_symbols(definition,[sQ656_spl])],[split_symbol_definition])).
% 10.94/1.88 fof(f9145,plain,(
% 10.94/1.88 sQ656_spl),
% 10.94/1.88 inference(split_clause,[status(thm)],[f9100,f9142])).
% 10.94/1.88 fof(f9168,plain,(
% 10.94/1.88 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))),
% 10.94/1.88 inference(resolution,[status(thm)],[f8258,f993])).
% 10.94/1.88 fof(f9204,definition,(
% 10.94/1.88 sQ661_spl <=> (less_or_equal(add(additive_identity,multiplicative_identity),add(additive_identity,multiplicative_identity)))),
% 10.94/1.88 introduced(definition,[new_symbols(definition,[sQ661_spl])],[split_symbol_definition])).
% 10.94/1.88 fof(f9207,plain,(
% 10.94/1.88 sQ661_spl),
% 10.94/1.88 inference(split_clause,[status(thm)],[f9168,f9204])).
% 10.94/1.88 fof(f9230,plain,(
% 10.94/1.88 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))),
% 10.94/1.88 inference(resolution,[status(thm)],[f8490,f994])).
% 10.94/1.88 fof(f9260,definition,(
% 10.94/1.88 sQ664_spl <=> (less_or_equal(add(additive_identity,additive_identity),add(additive_identity,additive_identity)))),
% 10.94/1.88 introduced(definition,[new_symbols(definition,[sQ664_spl])],[split_symbol_definition])).
% 10.94/1.88 fof(f9263,plain,(
% 10.94/1.88 sQ664_spl),
% 10.94/1.88 inference(split_clause,[status(thm)],[f9230,f9260])).
% 10.94/1.88 fof(f9286,plain,(
% 10.94/1.88 less_or_equal(multiply(a,a),multiply(a,a))|less_or_equal(multiply(a,a),multiply(a,a))),
% 10.94/1.88 inference(resolution,[status(thm)],[f8722,f1000])).
% 10.94/1.88 fof(f9310,definition,(
% 10.94/1.88 sQ665_spl <=> (less_or_equal(multiply(a,a),multiply(a,a)))),
% 10.94/1.88 introduced(definition,[new_symbols(definition,[sQ665_spl])],[split_symbol_definition])).
% 10.94/1.88 fof(f9313,plain,(
% 10.94/1.88 sQ665_spl),
% 10.94/1.88 inference(split_clause,[status(thm)],[f9286,f9310])).
% 10.94/1.88 fof(f9933,plain,(
% 10.94/1.88 ![X0]: (less_or_equal(multiply(a,multiplicative_identity),X0)|less_or_equal(X0,multiply(a,multiplicative_identity))|~defined(X0))),
% 10.94/1.88 inference(resolution,[status(thm)],[f1001,f58])).
% 10.94/1.88 fof(f10211,plain,(
% 10.94/1.88 ![X0]: (less_or_equal(multiply(a,additive_identity),X0)|less_or_equal(X0,multiply(a,additive_identity))|~defined(X0))),
% 10.94/1.88 inference(resolution,[status(thm)],[f1002,f58])).
% 10.94/1.88 fof(f10597,plain,(
% 10.94/1.88 ![X0]: (less_or_equal(multiply(multiplicative_identity,a),X0)|less_or_equal(X0,multiply(multiplicative_identity,a))|~defined(X0))),
% 10.94/1.88 inference(resolution,[status(thm)],[f1008,f58])).
% 10.94/1.88 fof(f10879,plain,(
% 10.94/1.88 ![X0]: (less_or_equal(multiply(multiplicative_identity,multiplicative_identity),X0)|less_or_equal(X0,multiply(multiplicative_identity,multiplicative_identity))|~defined(X0))),
% 10.94/1.88 inference(resolution,[status(thm)],[f1009,f58])).
% 10.94/1.88 fof(f11161,plain,(
% 10.94/1.88 ![X0]: (less_or_equal(multiply(multiplicative_identity,additive_identity),X0)|less_or_equal(X0,multiply(multiplicative_identity,additive_identity))|~defined(X0))),
% 10.94/1.88 inference(resolution,[status(thm)],[f1010,f58])).
% 10.94/1.88 fof(f11404,plain,(
% 10.94/1.88 less_or_equal(multiply(a,multiplicative_identity),multiply(a,multiplicative_identity))|less_or_equal(multiply(a,multiplicative_identity),multiply(a,multiplicative_identity))),
% 10.94/1.88 inference(resolution,[status(thm)],[f9933,f1001])).
% 10.94/1.88 fof(f11457,definition,(
% 10.94/1.88 sQ929_spl <=> (less_or_equal(multiply(a,multiplicative_identity),multiply(a,multiplicative_identity)))),
% 10.94/1.88 introduced(definition,[new_symbols(definition,[sQ929_spl])],[split_symbol_definition])).
% 10.94/1.88 fof(f11460,plain,(
% 10.94/1.88 sQ929_spl),
% 10.94/1.88 inference(split_clause,[status(thm)],[f11404,f11457])).
% 10.94/1.88 fof(f11488,plain,(
% 10.94/1.88 less_or_equal(multiply(a,additive_identity),multiply(a,additive_identity))|less_or_equal(multiply(a,additive_identity),multiply(a,additive_identity))),
% 10.94/1.88 inference(resolution,[status(thm)],[f10211,f1002])).
% 10.94/1.88 fof(f11535,definition,(
% 10.94/1.88 sQ936_spl <=> (less_or_equal(multiply(a,additive_identity),multiply(a,additive_identity)))),
% 10.94/1.88 introduced(definition,[new_symbols(definition,[sQ936_spl])],[split_symbol_definition])).
% 10.94/1.88 fof(f11538,plain,(
% 10.94/1.88 sQ936_spl),
% 10.94/1.88 inference(split_clause,[status(thm)],[f11488,f11535])).
% 10.94/1.88 fof(f11566,plain,(
% 10.94/1.88 less_or_equal(multiply(multiplicative_identity,a),multiply(multiplicative_identity,a))|less_or_equal(multiply(multiplicative_identity,a),multiply(multiplicative_identity,a))),
% 10.94/1.88 inference(resolution,[status(thm)],[f10597,f1008])).
% 10.94/1.88 fof(f11607,definition,(
% 10.94/1.88 sQ941_spl <=> (less_or_equal(multiply(multiplicative_identity,a),multiply(multiplicative_identity,a)))),
% 10.94/1.88 introduced(definition,[new_symbols(definition,[sQ941_spl])],[split_symbol_definition])).
% 10.94/1.88 fof(f11610,plain,(
% 10.94/1.88 sQ941_spl),
% 10.94/1.88 inference(split_clause,[status(thm)],[f11566,f11607])).
% 10.94/1.88 fof(f11638,plain,(
% 10.94/1.88 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))),
% 10.94/1.88 inference(resolution,[status(thm)],[f10879,f1009])).
% 10.94/1.88 fof(f11673,definition,(
% 10.94/1.88 sQ944_spl <=> (less_or_equal(multiply(multiplicative_identity,multiplicative_identity),multiply(multiplicative_identity,multiplicative_identity)))),
% 10.94/1.88 introduced(definition,[new_symbols(definition,[sQ944_spl])],[split_symbol_definition])).
% 10.94/1.88 fof(f11676,plain,(
% 10.94/1.88 sQ944_spl),
% 10.94/1.88 inference(split_clause,[status(thm)],[f11638,f11673])).
% 10.94/1.88 fof(f11704,plain,(
% 10.94/1.88 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))),
% 10.94/1.88 inference(resolution,[status(thm)],[f11161,f1010])).
% 10.94/1.88 fof(f11733,definition,(
% 10.94/1.88 sQ945_spl <=> (less_or_equal(multiply(multiplicative_identity,additive_identity),multiply(multiplicative_identity,additive_identity)))),
% 10.94/1.88 introduced(definition,[new_symbols(definition,[sQ945_spl])],[split_symbol_definition])).
% 10.94/1.88 fof(f11736,plain,(
% 10.94/1.88 sQ945_spl),
% 10.94/1.88 inference(split_clause,[status(thm)],[f11704,f11733])).
% 10.94/1.88 fof(f12306,plain,(
% 10.94/1.88 ![X0]: (less_or_equal(multiply(additive_identity,a),X0)|less_or_equal(X0,multiply(additive_identity,a))|~defined(X0))),
% 10.94/1.88 inference(resolution,[status(thm)],[f1016,f58])).
% 10.94/1.88 fof(f12628,plain,(
% 10.94/1.88 ![X0]: (less_or_equal(multiply(additive_identity,multiplicative_identity),X0)|less_or_equal(X0,multiply(additive_identity,multiplicative_identity))|~defined(X0))),
% 10.94/1.88 inference(resolution,[status(thm)],[f1017,f58])).
% 10.94/1.88 fof(f12976,plain,(
% 10.94/1.88 ![X0]: (less_or_equal(multiply(additive_identity,additive_identity),X0)|less_or_equal(X0,multiply(additive_identity,additive_identity))|~defined(X0))),
% 10.94/1.88 inference(resolution,[status(thm)],[f1018,f58])).
% 10.94/1.88 fof(f13301,plain,(
% 10.94/1.88 less_or_equal(multiply(additive_identity,a),multiply(additive_identity,a))|less_or_equal(multiply(additive_identity,a),multiply(additive_identity,a))),
% 10.94/1.88 inference(resolution,[status(thm)],[f12306,f1016])).
% 10.94/1.88 fof(f13345,definition,(
% 10.94/1.88 sQ1133_spl <=> (less_or_equal(multiply(additive_identity,a),multiply(additive_identity,a)))),
% 10.94/1.88 introduced(definition,[new_symbols(definition,[sQ1133_spl])],[split_symbol_definition])).
% 10.94/1.88 fof(f13348,plain,(
% 10.94/1.88 sQ1133_spl),
% 10.94/1.88 inference(split_clause,[status(thm)],[f13301,f13345])).
% 10.94/1.88 fof(f13379,plain,(
% 10.94/1.88 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))),
% 10.94/1.88 inference(resolution,[status(thm)],[f12628,f1017])).
% 10.94/1.88 fof(f13417,definition,(
% 10.94/1.88 sQ1136_spl <=> (less_or_equal(multiply(additive_identity,multiplicative_identity),multiply(additive_identity,multiplicative_identity)))),
% 10.94/1.88 introduced(definition,[new_symbols(definition,[sQ1136_spl])],[split_symbol_definition])).
% 10.94/1.88 fof(f13420,plain,(
% 10.94/1.88 sQ1136_spl),
% 10.94/1.88 inference(split_clause,[status(thm)],[f13379,f13417])).
% 10.94/1.88 fof(f13451,plain,(
% 10.94/1.88 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))),
% 10.94/1.88 inference(resolution,[status(thm)],[f12976,f1018])).
% 10.94/1.88 fof(f13483,definition,(
% 10.94/1.88 sQ1137_spl <=> (less_or_equal(multiply(additive_identity,additive_identity),multiply(additive_identity,additive_identity)))),
% 10.94/1.88 introduced(definition,[new_symbols(definition,[sQ1137_spl])],[split_symbol_definition])).
% 10.94/1.88 fof(f13486,plain,(
% 10.94/1.88 sQ1137_spl),
% 10.94/1.88 inference(split_clause,[status(thm)],[f13451,f13483])).
% 10.94/1.88 fof(f15429,plain,(
% 10.94/1.88 equalish(multiplicative_inverse(a),multiply(a,multiplicative_inverse(a)))|~sQ6_spl),
% 10.94/1.88 inference(resolution,[status(thm)],[f443,f199])).
% 10.94/1.88 fof(f15643,plain,(
% 10.94/1.88 ![X0]: (equalish(multiplicative_inverse(a),X0)|~equalish(multiply(a,multiplicative_inverse(a)),X0)|~sQ6_spl)),
% 10.94/1.88 inference(resolution,[status(thm)],[f15429,f66])).
% 10.94/1.88 fof(f19745,plain,(
% 10.94/1.88 equalish(multiplicative_inverse(a),multiply(multiplicative_inverse(a),a))|~sQ6_spl|~sQ0_spl),
% 10.94/1.88 inference(resolution,[status(thm)],[f15643,f413])).
% 10.94/1.88 fof(f24347,plain,(
% 10.94/1.88 equalish(multiplicative_identity,multiply(multiplicative_inverse(a),a))|~sQ6_spl|~sQ0_spl),
% 10.94/1.88 inference(resolution,[status(thm)],[f19745,f197])).
% 10.94/1.88 fof(f24376,plain,(
% 3.04/1.91 equalish(multiply(multiplicative_inverse(a),a),multiplicative_identity)|~sQ6_spl|~sQ0_spl),
% 3.04/1.91 inference(resolution,[status(thm)],[f24347,f64])).
% 3.04/1.91 fof(f24377,plain,(
% 3.04/1.91 equalish(a,multiplicative_identity)|~sQ6_spl|~sQ0_spl),
% 3.04/1.91 inference(resolution,[status(thm)],[f24376,f3104])).
% 3.04/1.91 fof(f24389,plain,(
% 3.04/1.91 sQ72_spl|~sQ6_spl|~sQ0_spl),
% 3.04/1.91 inference(split_clause,[status(thm)],[f24377,f736,f132,f108])).
% 3.04/1.91 fof(f24390,plain,(
% 3.04/1.91 $false),
% 3.04/1.91 inference(sat_refutation,[status(thm)],[f114,f135,f145,f746,f789,f805,f957,f2807,f3696,f4600,f7026,f7084,f7136,f7182,f7222,f9077,f9145,f9207,f9263,f9313,f11460,f11538,f11610,f11676,f11736,f13348,f13420,f13486,f24389])).
% 3.04/1.91 % SZS output end CNFRefutation for theBenchmark.p
% 3.04/1.92 % Elapsed time: 1.533556 seconds
% 3.04/1.92 % CPU time: 11.789139 seconds
% 3.04/1.92 % Total memory used: 169.876 MB
% 3.04/1.92 % Net memory used: 160.476 MB
%------------------------------------------------------------------------------