%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : FLD009-3 : 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 : n014.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 12:22:17 PM UTC 2026
% Result : Unsatisfiable 11.30s 1.88s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : FLD009-3 : TPTP v9.3.1. Bugfixed v2.1.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.37 % Computer : n014.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Mon Sep 21 15:36:49 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.38 % Drodi V4.1.1
% 11.30/1.88 % Refutation found
% 11.30/1.88 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 11.30/1.88 % SZS output start CNFRefutation for theBenchmark
% 11.30/1.88 fof(f6,axiom,(
% 11.30/1.88 (![X,V,W,Y,U,Z]: (( product(X,V,W)| ~ product(X,Y,U)| ~ product(Y,Z,V)| ~ product(U,Z,W) ) ))),
% 11.30/1.88 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 11.30/1.88 fof(f8,axiom,(
% 11.30/1.88 (![X]: (( product(multiplicative_identity,X,X)| ~ defined(X) ) ))),
% 11.30/1.88 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 11.30/1.88 fof(f9,axiom,(
% 11.30/1.88 (![X]: (( product(multiplicative_inverse(X),X,multiplicative_identity)| sum(additive_identity,X,additive_identity)| ~ defined(X) ) ))),
% 11.30/1.88 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 11.30/1.88 fof(f10,axiom,(
% 11.30/1.88 (![Y,X,Z]: (( product(Y,X,Z)| ~ product(X,Y,Z) ) ))),
% 11.30/1.88 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 11.30/1.88 fof(f14,axiom,(
% 11.30/1.88 defined(additive_identity) ),
% 11.30/1.88 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 11.30/1.88 fof(f15,axiom,(
% 11.30/1.88 (![X]: (( defined(additive_inverse(X))| ~ defined(X) ) ))),
% 11.30/1.88 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 11.30/1.88 fof(f17,axiom,(
% 11.30/1.88 defined(multiplicative_identity) ),
% 11.30/1.88 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 11.30/1.88 fof(f18,axiom,(
% 11.30/1.88 (![X]: (( defined(multiplicative_inverse(X))| ~ defined(X)| sum(additive_identity,X,additive_identity) ) ))),
% 11.30/1.88 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 11.30/1.88 fof(f20,axiom,(
% 11.30/1.88 (![X,Y]: (( product(X,Y,multiply(X,Y))| ~ defined(X)| ~ defined(Y) ) ))),
% 11.30/1.88 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 11.30/1.88 fof(f23,axiom,(
% 11.30/1.88 (![X,Y]: (( less_or_equal(X,Y)| less_or_equal(Y,X)| ~ defined(X)| ~ defined(Y) ) ))),
% 11.30/1.88 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 11.30/1.88 fof(f27,hypothesis,(
% 11.30/1.88 defined(a) ),
% 11.30/1.88 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 11.30/1.88 fof(f28,hypothesis,(
% 11.30/1.88 defined(b) ),
% 11.30/1.88 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 11.30/1.88 fof(f29,negated_conjecture,(
% 11.30/1.88 ~ sum(additive_identity,a,additive_identity) ),
% 11.30/1.88 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 11.30/1.88 fof(f30,negated_conjecture,(
% 11.30/1.88 (![X]: (~ product(a,X,b) ))),
% 11.30/1.88 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 11.30/1.88 fof(f38,plain,(
% 11.30/1.88 ![W,U,Z]: ((![V,Y]: ((![X]: (product(X,V,W)|~product(X,Y,U)))|~product(Y,Z,V)))|~product(U,Z,W))),
% 11.30/1.88 inference(miniscoping,[status(thm)],[f6])).
% 11.30/1.88 fof(f39,plain,(
% 11.30/1.88 ![X0,X1,X2,X3,X4,X5]: (product(X0,X1,X2)|~product(X0,X3,X4)|~product(X3,X5,X1)|~product(X4,X5,X2))),
% 11.30/1.88 inference(cnf_transformation,[status(thm)],[f38])).
% 11.30/1.88 fof(f42,plain,(
% 11.30/1.88 ![X0]: (product(multiplicative_identity,X0,X0)|~defined(X0))),
% 11.30/1.88 inference(cnf_transformation,[status(thm)],[f8])).
% 11.30/1.88 fof(f43,plain,(
% 11.30/1.88 ![X0]: (product(multiplicative_inverse(X0),X0,multiplicative_identity)|sum(additive_identity,X0,additive_identity)|~defined(X0))),
% 11.30/1.88 inference(cnf_transformation,[status(thm)],[f9])).
% 11.30/1.88 fof(f44,plain,(
% 11.30/1.88 ![X0,X1,X2]: (product(X0,X1,X2)|~product(X1,X0,X2))),
% 11.30/1.88 inference(cnf_transformation,[status(thm)],[f10])).
% 11.30/1.88 fof(f51,plain,(
% 11.30/1.88 defined(additive_identity)),
% 11.30/1.88 inference(cnf_transformation,[status(thm)],[f14])).
% 11.30/1.88 fof(f52,plain,(
% 11.30/1.88 ![X0]: (defined(additive_inverse(X0))|~defined(X0))),
% 11.30/1.88 inference(cnf_transformation,[status(thm)],[f15])).
% 11.30/1.88 fof(f55,plain,(
% 11.30/1.88 defined(multiplicative_identity)),
% 11.30/1.88 inference(cnf_transformation,[status(thm)],[f17])).
% 11.30/1.88 fof(f56,plain,(
% 11.30/1.88 ![X0]: (defined(multiplicative_inverse(X0))|~defined(X0)|sum(additive_identity,X0,additive_identity))),
% 11.30/1.88 inference(cnf_transformation,[status(thm)],[f18])).
% 11.30/1.88 fof(f59,plain,(
% 11.30/1.88 ![Y]: ((![X]: (product(X,Y,multiply(X,Y))|~defined(X)))|~defined(Y))),
% 11.30/1.88 inference(miniscoping,[status(thm)],[f20])).
% 11.30/1.88 fof(f60,plain,(
% 11.30/1.88 ![X0,X1]: (product(X0,X1,multiply(X0,X1))|~defined(X0)|~defined(X1))),
% 11.30/1.88 inference(cnf_transformation,[status(thm)],[f59])).
% 11.30/1.88 fof(f64,plain,(
% 11.30/1.88 ![Y]: ((![X]: ((less_or_equal(X,Y)|less_or_equal(Y,X))|~defined(X)))|~defined(Y))),
% 11.30/1.88 inference(miniscoping,[status(thm)],[f23])).
% 11.30/1.88 fof(f65,plain,(
% 11.30/1.88 ![X0,X1]: (less_or_equal(X0,X1)|less_or_equal(X1,X0)|~defined(X0)|~defined(X1))),
% 11.30/1.88 inference(cnf_transformation,[status(thm)],[f64])).
% 11.30/1.88 fof(f70,plain,(
% 11.30/1.88 defined(a)),
% 11.30/1.88 inference(cnf_transformation,[status(thm)],[f27])).
% 11.30/1.88 fof(f71,plain,(
% 11.30/1.88 defined(b)),
% 11.30/1.88 inference(cnf_transformation,[status(thm)],[f28])).
% 11.30/1.88 fof(f72,plain,(
% 11.30/1.88 ~sum(additive_identity,a,additive_identity)),
% 11.30/1.88 inference(cnf_transformation,[status(thm)],[f29])).
% 11.30/1.88 fof(f73,plain,(
% 11.30/1.88 ![X0]: (~product(a,X0,b))),
% 11.30/1.88 inference(cnf_transformation,[status(thm)],[f30])).
% 11.30/1.88 fof(f98,plain,(
% 11.30/1.88 product(multiplicative_identity,b,b)),
% 11.30/1.88 inference(resolution,[status(thm)],[f42,f71])).
% 11.30/1.88 fof(f102,plain,(
% 11.30/1.88 product(multiplicative_inverse(a),a,multiplicative_identity)|sum(additive_identity,a,additive_identity)),
% 11.30/1.88 inference(resolution,[status(thm)],[f43,f70])).
% 11.30/1.88 fof(f111,definition,(
% 11.30/1.88 sQ2_spl <=> (product(multiplicative_inverse(a),a,multiplicative_identity))),
% 11.30/1.88 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 11.30/1.88 fof(f112,plain,(
% 11.30/1.88 product(multiplicative_inverse(a),a,multiplicative_identity)|~sQ2_spl),
% 11.30/1.88 inference(component_clause,[status(thm)],[f111])).
% 11.30/1.88 fof(f114,definition,(
% 11.30/1.88 sQ3_spl <=> (sum(additive_identity,a,additive_identity))),
% 11.30/1.88 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 11.30/1.88 fof(f115,plain,(
% 11.30/1.88 sum(additive_identity,a,additive_identity)|~sQ3_spl),
% 11.30/1.88 inference(component_clause,[status(thm)],[f114])).
% 11.30/1.88 fof(f117,plain,(
% 11.30/1.88 sQ2_spl|sQ3_spl),
% 11.30/1.88 inference(split_clause,[status(thm)],[f102,f111,f114])).
% 11.30/1.88 fof(f179,plain,(
% 11.30/1.88 ![X0,X1,X2]: (product(X0,X1,b)|~product(X0,X2,multiplicative_identity)|~product(X2,b,X1))),
% 11.30/1.88 inference(resolution,[status(thm)],[f98,f39])).
% 11.30/1.88 fof(f217,plain,(
% 11.30/1.88 defined(additive_inverse(b))),
% 11.30/1.88 inference(resolution,[status(thm)],[f52,f71])).
% 11.30/1.88 fof(f218,plain,(
% 11.30/1.88 defined(additive_inverse(a))),
% 11.30/1.88 inference(resolution,[status(thm)],[f52,f70])).
% 11.30/1.88 fof(f219,plain,(
% 11.30/1.88 defined(additive_inverse(additive_identity))),
% 11.30/1.88 inference(resolution,[status(thm)],[f52,f51])).
% 11.30/1.88 fof(f239,plain,(
% 11.30/1.88 defined(multiplicative_inverse(a))|sum(additive_identity,a,additive_identity)),
% 11.30/1.88 inference(resolution,[status(thm)],[f56,f70])).
% 11.30/1.88 fof(f249,definition,(
% 11.30/1.88 sQ10_spl <=> (defined(multiplicative_inverse(a)))),
% 11.30/1.88 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 11.30/1.88 fof(f252,plain,(
% 11.30/1.88 sQ10_spl|sQ3_spl),
% 11.30/1.88 inference(split_clause,[status(thm)],[f239,f249,f114])).
% 11.30/1.88 fof(f257,plain,(
% 11.30/1.88 $false|~sQ3_spl),
% 11.30/1.88 inference(forward_subsumption_resolution,[status(thm)],[f115,f72])).
% 11.30/1.88 fof(f258,plain,(
% 11.30/1.88 ~sQ3_spl),
% 11.30/1.88 inference(contradiction_clause,[status(thm)],[f257])).
% 11.30/1.88 fof(f428,plain,(
% 11.30/1.88 ![X0,X1]: (~defined(X0)|~defined(X1)|product(X1,X0,multiply(X0,X1)))),
% 11.30/1.88 inference(resolution,[status(thm)],[f60,f44])).
% 11.30/1.88 fof(f437,plain,(
% 11.30/1.88 ![X0]: (less_or_equal(X0,additive_inverse(additive_identity))|less_or_equal(additive_inverse(additive_identity),X0)|~defined(X0))),
% 11.30/1.88 inference(resolution,[status(thm)],[f65,f219])).
% 11.30/1.88 fof(f438,plain,(
% 11.30/1.88 ![X0]: (less_or_equal(X0,additive_inverse(a))|less_or_equal(additive_inverse(a),X0)|~defined(X0))),
% 11.30/1.88 inference(resolution,[status(thm)],[f65,f218])).
% 11.30/1.88 fof(f439,plain,(
% 11.30/1.88 ![X0]: (less_or_equal(X0,additive_inverse(b))|less_or_equal(additive_inverse(b),X0)|~defined(X0))),
% 11.30/1.88 inference(resolution,[status(thm)],[f65,f217])).
% 11.30/1.88 fof(f440,plain,(
% 11.30/1.88 ![X0]: (less_or_equal(X0,multiplicative_identity)|less_or_equal(multiplicative_identity,X0)|~defined(X0))),
% 11.30/1.88 inference(resolution,[status(thm)],[f65,f55])).
% 11.30/1.88 fof(f441,plain,(
% 11.30/1.88 ![X0]: (less_or_equal(X0,b)|less_or_equal(b,X0)|~defined(X0))),
% 11.30/1.88 inference(resolution,[status(thm)],[f65,f71])).
% 11.30/1.88 fof(f442,plain,(
% 11.30/1.88 ![X0]: (less_or_equal(X0,a)|less_or_equal(a,X0)|~defined(X0))),
% 11.30/1.88 inference(resolution,[status(thm)],[f65,f70])).
% 11.30/1.88 fof(f443,plain,(
% 11.30/1.88 ![X0]: (less_or_equal(X0,additive_identity)|less_or_equal(additive_identity,X0)|~defined(X0))),
% 11.30/1.88 inference(resolution,[status(thm)],[f65,f51])).
% 11.30/1.88 fof(f545,plain,(
% 11.30/1.88 product(a,multiplicative_inverse(a),multiplicative_identity)|~sQ2_spl),
% 11.30/1.88 inference(resolution,[status(thm)],[f112,f44])).
% 11.30/1.88 fof(f858,definition,(
% 11.30/1.88 sQ57_spl <=> (defined(multiplicative_identity))),
% 11.30/1.88 introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition])).
% 11.30/1.88 fof(f860,plain,(
% 11.30/1.88 ~defined(multiplicative_identity)|sQ57_spl),
% 11.30/1.88 inference(component_clause,[status(thm)],[f858])).
% 11.30/1.88 fof(f865,definition,(
% 11.30/1.88 sQ59_spl <=> (defined(additive_identity))),
% 11.30/1.88 introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition])).
% 11.30/1.88 fof(f867,plain,(
% 11.30/1.88 ~defined(additive_identity)|sQ59_spl),
% 11.30/1.88 inference(component_clause,[status(thm)],[f865])).
% 11.30/1.88 fof(f872,definition,(
% 11.30/1.88 sQ61_spl <=> (defined(a))),
% 11.30/1.88 introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition])).
% 11.30/1.88 fof(f874,plain,(
% 11.30/1.88 ~defined(a)|sQ61_spl),
% 11.30/1.88 inference(component_clause,[status(thm)],[f872])).
% 11.30/1.88 fof(f879,definition,(
% 11.30/1.88 sQ63_spl <=> (defined(b))),
% 11.30/1.88 introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition])).
% 11.30/1.88 fof(f881,plain,(
% 11.30/1.88 ~defined(b)|sQ63_spl),
% 11.30/1.88 inference(component_clause,[status(thm)],[f879])).
% 11.30/1.88 fof(f887,plain,(
% 11.30/1.88 $false|sQ63_spl),
% 11.30/1.88 inference(forward_subsumption_resolution,[status(thm)],[f881,f71])).
% 11.30/1.88 fof(f888,plain,(
% 11.30/1.88 sQ63_spl),
% 11.30/1.88 inference(contradiction_clause,[status(thm)],[f887])).
% 11.30/1.88 fof(f889,plain,(
% 11.30/1.88 $false|sQ61_spl),
% 11.30/1.88 inference(forward_subsumption_resolution,[status(thm)],[f874,f70])).
% 11.30/1.88 fof(f890,plain,(
% 11.30/1.88 sQ61_spl),
% 11.30/1.88 inference(contradiction_clause,[status(thm)],[f889])).
% 11.30/1.88 fof(f891,plain,(
% 11.30/1.88 $false|sQ59_spl),
% 11.30/1.88 inference(forward_subsumption_resolution,[status(thm)],[f867,f51])).
% 11.30/1.88 fof(f892,plain,(
% 11.30/1.88 sQ59_spl),
% 11.30/1.88 inference(contradiction_clause,[status(thm)],[f891])).
% 11.30/1.88 fof(f893,plain,(
% 11.30/1.88 $false|sQ57_spl),
% 11.30/1.88 inference(forward_subsumption_resolution,[status(thm)],[f860,f55])).
% 11.30/1.88 fof(f894,plain,(
% 11.30/1.88 sQ57_spl),
% 11.30/1.88 inference(contradiction_clause,[status(thm)],[f893])).
% 11.30/1.88 fof(f1074,plain,(
% 11.30/1.88 less_or_equal(multiplicative_identity,multiplicative_identity)|less_or_equal(multiplicative_identity,multiplicative_identity)),
% 11.30/1.88 inference(resolution,[status(thm)],[f440,f55])).
% 11.30/1.88 fof(f1204,definition,(
% 11.30/1.88 sQ120_spl <=> (less_or_equal(multiplicative_identity,multiplicative_identity))),
% 11.30/1.88 introduced(definition,[new_symbols(definition,[sQ120_spl])],[split_symbol_definition])).
% 11.30/1.88 fof(f1207,plain,(
% 11.30/1.88 sQ120_spl),
% 11.30/1.88 inference(split_clause,[status(thm)],[f1074,f1204])).
% 11.30/1.88 fof(f1286,plain,(
% 11.30/1.88 less_or_equal(b,b)|less_or_equal(b,b)),
% 11.30/1.88 inference(resolution,[status(thm)],[f441,f71])).
% 11.30/1.88 fof(f1423,definition,(
% 11.30/1.88 sQ170_spl <=> (less_or_equal(b,b))),
% 11.30/1.88 introduced(definition,[new_symbols(definition,[sQ170_spl])],[split_symbol_definition])).
% 11.30/1.88 fof(f1426,plain,(
% 11.30/1.88 sQ170_spl),
% 11.30/1.88 inference(split_clause,[status(thm)],[f1286,f1423])).
% 11.30/1.88 fof(f1462,plain,(
% 11.30/1.88 less_or_equal(a,a)|less_or_equal(a,a)),
% 11.30/1.88 inference(resolution,[status(thm)],[f442,f70])).
% 11.30/1.88 fof(f1599,definition,(
% 11.30/1.88 sQ213_spl <=> (less_or_equal(a,a))),
% 11.30/1.88 introduced(definition,[new_symbols(definition,[sQ213_spl])],[split_symbol_definition])).
% 11.30/1.88 fof(f1602,plain,(
% 11.30/1.88 sQ213_spl),
% 11.30/1.88 inference(split_clause,[status(thm)],[f1462,f1599])).
% 11.30/1.88 fof(f1740,plain,(
% 11.30/1.88 less_or_equal(additive_identity,additive_identity)|less_or_equal(additive_identity,additive_identity)),
% 11.30/1.88 inference(resolution,[status(thm)],[f443,f51])).
% 11.30/1.88 fof(f1891,definition,(
% 11.30/1.88 sQ276_spl <=> (less_or_equal(additive_identity,additive_identity))),
% 11.30/1.88 introduced(definition,[new_symbols(definition,[sQ276_spl])],[split_symbol_definition])).
% 11.30/1.88 fof(f1894,plain,(
% 11.30/1.88 sQ276_spl),
% 11.30/1.88 inference(split_clause,[status(thm)],[f1740,f1891])).
% 11.30/1.88 fof(f2808,definition,(
% 11.30/1.88 sQ413_spl <=> (defined(additive_inverse(additive_identity)))),
% 11.30/1.88 introduced(definition,[new_symbols(definition,[sQ413_spl])],[split_symbol_definition])).
% 11.30/1.88 fof(f2810,plain,(
% 11.30/1.88 ~defined(additive_inverse(additive_identity))|sQ413_spl),
% 11.30/1.88 inference(component_clause,[status(thm)],[f2808])).
% 11.30/1.88 fof(f2824,plain,(
% 11.30/1.88 $false|sQ413_spl),
% 11.30/1.88 inference(forward_subsumption_resolution,[status(thm)],[f2810,f219])).
% 11.30/1.88 fof(f2825,plain,(
% 11.30/1.88 sQ413_spl),
% 11.30/1.88 inference(contradiction_clause,[status(thm)],[f2824])).
% 11.30/1.88 fof(f3909,definition,(
% 11.30/1.88 sQ589_spl <=> (defined(additive_inverse(b)))),
% 11.30/1.88 introduced(definition,[new_symbols(definition,[sQ589_spl])],[split_symbol_definition])).
% 11.30/1.88 fof(f3911,plain,(
% 11.30/1.88 ~defined(additive_inverse(b))|sQ589_spl),
% 11.30/1.88 inference(component_clause,[status(thm)],[f3909])).
% 11.30/1.88 fof(f3921,plain,(
% 11.30/1.88 $false|sQ589_spl),
% 11.30/1.88 inference(forward_subsumption_resolution,[status(thm)],[f3911,f217])).
% 11.30/1.91 fof(f3922,plain,(
% 11.30/1.91 sQ589_spl),
% 11.30/1.91 inference(contradiction_clause,[status(thm)],[f3921])).
% 11.30/1.91 fof(f4698,definition,(
% 11.30/1.91 sQ712_spl <=> (defined(additive_inverse(a)))),
% 11.30/1.91 introduced(definition,[new_symbols(definition,[sQ712_spl])],[split_symbol_definition])).
% 11.30/1.91 fof(f4700,plain,(
% 11.30/1.91 ~defined(additive_inverse(a))|sQ712_spl),
% 11.30/1.91 inference(component_clause,[status(thm)],[f4698])).
% 11.30/1.91 fof(f4710,plain,(
% 11.30/1.91 $false|sQ712_spl),
% 11.30/1.91 inference(forward_subsumption_resolution,[status(thm)],[f4700,f218])).
% 11.30/1.91 fof(f4711,plain,(
% 11.30/1.91 sQ712_spl),
% 11.30/1.91 inference(contradiction_clause,[status(thm)],[f4710])).
% 11.30/1.91 fof(f6432,plain,(
% 11.30/1.91 less_or_equal(additive_inverse(additive_identity),additive_inverse(additive_identity))|less_or_equal(additive_inverse(additive_identity),additive_inverse(additive_identity))),
% 11.30/1.91 inference(resolution,[status(thm)],[f437,f219])).
% 11.30/1.91 fof(f6902,definition,(
% 11.30/1.91 sQ1141_spl <=> (less_or_equal(additive_inverse(additive_identity),additive_inverse(additive_identity)))),
% 11.30/1.91 introduced(definition,[new_symbols(definition,[sQ1141_spl])],[split_symbol_definition])).
% 11.30/1.91 fof(f6905,plain,(
% 11.30/1.91 sQ1141_spl),
% 11.30/1.91 inference(split_clause,[status(thm)],[f6432,f6902])).
% 11.30/1.91 fof(f7000,plain,(
% 11.30/1.91 less_or_equal(additive_inverse(a),additive_inverse(a))|less_or_equal(additive_inverse(a),additive_inverse(a))),
% 11.30/1.91 inference(resolution,[status(thm)],[f438,f218])).
% 11.30/1.91 fof(f7470,definition,(
% 11.30/1.91 sQ1278_spl <=> (less_or_equal(additive_inverse(a),additive_inverse(a)))),
% 11.30/1.91 introduced(definition,[new_symbols(definition,[sQ1278_spl])],[split_symbol_definition])).
% 11.30/1.91 fof(f7473,plain,(
% 11.30/1.91 sQ1278_spl),
% 11.30/1.91 inference(split_clause,[status(thm)],[f7000,f7470])).
% 11.30/1.91 fof(f7583,plain,(
% 11.30/1.91 less_or_equal(additive_inverse(b),additive_inverse(b))|less_or_equal(additive_inverse(b),additive_inverse(b))),
% 11.30/1.91 inference(resolution,[status(thm)],[f439,f217])).
% 11.30/1.91 fof(f8053,definition,(
% 11.30/1.91 sQ1416_spl <=> (less_or_equal(additive_inverse(b),additive_inverse(b)))),
% 11.30/1.91 introduced(definition,[new_symbols(definition,[sQ1416_spl])],[split_symbol_definition])).
% 11.30/1.91 fof(f8056,plain,(
% 11.30/1.91 sQ1416_spl),
% 11.30/1.91 inference(split_clause,[status(thm)],[f7583,f8053])).
% 11.30/1.91 fof(f8253,plain,(
% 11.30/1.91 ![X0]: (product(a,X0,b)|~product(multiplicative_inverse(a),b,X0)|~sQ2_spl)),
% 11.30/1.91 inference(resolution,[status(thm)],[f545,f179])).
% 11.30/1.91 fof(f8265,plain,(
% 11.30/1.91 ![X0]: (~product(multiplicative_inverse(a),b,X0)|~sQ2_spl)),
% 11.30/1.91 inference(forward_subsumption_resolution,[status(thm)],[f8253,f73])).
% 11.30/1.91 fof(f8292,plain,(
% 11.30/1.91 ~defined(b)|~defined(multiplicative_inverse(a))|~sQ2_spl),
% 11.30/1.91 inference(resolution,[status(thm)],[f8265,f428])).
% 11.30/1.91 fof(f8294,plain,(
% 11.30/1.91 ~sQ63_spl|~sQ10_spl|~sQ2_spl),
% 11.30/1.91 inference(split_clause,[status(thm)],[f8292,f879,f249,f111])).
% 11.30/1.91 fof(f8296,plain,(
% 11.30/1.91 $false),
% 11.30/1.91 inference(sat_refutation,[status(thm)],[f117,f252,f258,f888,f890,f892,f894,f1207,f1426,f1602,f1894,f2825,f3922,f4711,f6905,f7473,f8056,f8294])).
% 11.30/1.91 % SZS output end CNFRefutation for theBenchmark.p
% 1.32/1.94 % Elapsed time: 1.556660 seconds
% 1.32/1.94 % CPU time: 11.974630 seconds
% 1.32/1.94 % Total memory used: 131.927 MB
% 1.32/1.94 % Net memory used: 127.004 MB
%------------------------------------------------------------------------------