%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : FLD054-4 : 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 : n004.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:26 PM UTC 2026
% Result : Unsatisfiable 149.01s 19.20s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : FLD054-4 : 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.08/0.35 % Computer : n004.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Mon Sep 21 15:42:38 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.08/0.36 % Drodi V4.1.1
% 149.01/19.20 % Refutation found
% 149.01/19.20 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 149.01/19.20 % SZS output start CNFRefutation for theBenchmark
% 149.01/19.20 fof(f1,axiom,(
% 149.01/19.20 (![X,V,W,Y,U,Z]: (( sum(X,V,W)| ~ sum(X,Y,U)| ~ sum(Y,Z,V)| ~ sum(U,Z,W) ) ))),
% 149.01/19.20 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 149.01/19.20 fof(f2,axiom,(
% 149.01/19.20 (![U,Z,W,X,Y,V]: (( sum(U,Z,W)| ~ sum(X,Y,U)| ~ sum(Y,Z,V)| ~ sum(X,V,W) ) ))),
% 149.01/19.20 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 149.01/19.20 fof(f3,axiom,(
% 149.01/19.20 (![X]: (( sum(additive_identity,X,X)| ~ defined(X) ) ))),
% 149.01/19.20 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 149.01/19.20 fof(f4,axiom,(
% 149.01/19.20 (![X]: (( sum(additive_inverse(X),X,additive_identity)| ~ defined(X) ) ))),
% 149.01/19.20 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 149.01/19.20 fof(f5,axiom,(
% 149.01/19.20 (![Y,X,Z]: (( sum(Y,X,Z)| ~ sum(X,Y,Z) ) ))),
% 149.01/19.20 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 149.01/19.20 fof(f6,axiom,(
% 149.01/19.20 (![X,V,W,Y,U,Z]: (( product(X,V,W)| ~ product(X,Y,U)| ~ product(Y,Z,V)| ~ product(U,Z,W) ) ))),
% 149.01/19.20 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 149.01/19.20 fof(f8,axiom,(
% 149.01/19.20 (![X]: (( product(multiplicative_identity,X,X)| ~ defined(X) ) ))),
% 149.01/19.20 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 149.01/19.20 fof(f9,axiom,(
% 149.01/19.20 (![X]: (( product(multiplicative_inverse(X),X,multiplicative_identity)| sum(additive_identity,X,additive_identity)| ~ defined(X) ) ))),
% 149.01/19.20 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 149.01/19.20 fof(f10,axiom,(
% 149.01/19.20 (![Y,X,Z]: (( product(Y,X,Z)| ~ product(X,Y,Z) ) ))),
% 149.01/19.20 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 149.01/19.20 fof(f11,axiom,(
% 149.01/19.20 (![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) ) ))),
% 149.01/19.20 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 149.01/19.20 fof(f12,axiom,(
% 149.01/19.20 (![A,Z,B,X,Y,C,D]: (( product(A,Z,B)| ~ sum(X,Y,A)| ~ product(X,Z,C)| ~ product(Y,Z,D)| ~ sum(C,D,B) ) ))),
% 149.01/19.20 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 149.01/19.20 fof(f14,axiom,(
% 149.01/19.20 defined(additive_identity) ),
% 149.01/19.20 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 149.01/19.20 fof(f15,axiom,(
% 149.01/19.20 (![X]: (( defined(additive_inverse(X))| ~ defined(X) ) ))),
% 149.01/19.20 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 149.01/19.20 fof(f17,axiom,(
% 149.01/19.20 defined(multiplicative_identity) ),
% 149.01/19.20 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 149.01/19.20 fof(f23,axiom,(
% 149.01/19.20 (![X,Y]: (( less_or_equal(X,Y)| less_or_equal(Y,X)| ~ defined(X)| ~ defined(Y) ) ))),
% 149.01/19.20 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 149.01/19.20 fof(f26,axiom,(
% 149.01/19.20 ~ sum(additive_identity,additive_identity,multiplicative_identity) ),
% 149.01/19.20 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 149.01/19.20 fof(f27,hypothesis,(
% 149.01/19.20 defined(a) ),
% 149.01/19.20 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 149.01/19.20 fof(f28,hypothesis,(
% 149.01/19.20 defined(b) ),
% 149.01/19.20 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 149.01/19.20 fof(f29,hypothesis,(
% 149.01/19.20 defined(u) ),
% 149.01/19.20 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 149.01/19.20 fof(f30,hypothesis,(
% 149.01/19.20 defined(k) ),
% 149.01/19.20 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 149.01/19.20 fof(f31,hypothesis,(
% 149.01/19.20 defined(l) ),
% 149.01/19.20 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 149.01/19.20 fof(f32,negated_conjecture,(
% 149.01/19.20 ~ sum(additive_identity,a,additive_identity) ),
% 149.01/19.20 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 149.01/19.20 fof(f33,negated_conjecture,(
% 149.01/19.20 ~ sum(additive_identity,b,additive_identity) ),
% 149.01/19.20 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 149.01/19.20 fof(f34,negated_conjecture,(
% 149.01/19.20 sum(multiplicative_inverse(a),multiplicative_inverse(b),u) ),
% 149.01/19.20 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 149.01/19.20 fof(f35,negated_conjecture,(
% 149.01/19.20 sum(a,b,k) ),
% 149.01/19.20 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 149.01/19.20 fof(f36,negated_conjecture,(
% 149.01/19.20 product(a,b,l) ),
% 149.01/19.20 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 149.01/19.20 fof(f37,negated_conjecture,(
% 149.01/19.20 ~ product(k,multiplicative_inverse(l),u) ),
% 149.01/19.20 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 149.01/19.20 fof(f38,plain,(
% 149.01/19.20 ![W,U,Z]: ((![V,Y]: ((![X]: (sum(X,V,W)|~sum(X,Y,U)))|~sum(Y,Z,V)))|~sum(U,Z,W))),
% 149.01/19.20 inference(miniscoping,[status(thm)],[f1])).
% 149.01/19.20 fof(f39,plain,(
% 149.01/19.20 ![X0,X1,X2,X3,X4,X5]: (sum(X0,X1,X2)|~sum(X0,X3,X4)|~sum(X3,X5,X1)|~sum(X4,X5,X2))),
% 149.01/19.20 inference(cnf_transformation,[status(thm)],[f38])).
% 149.01/19.20 fof(f40,plain,(
% 149.01/19.20 ![W,X,V]: ((![Z,Y]: ((![U]: (sum(U,Z,W)|~sum(X,Y,U)))|~sum(Y,Z,V)))|~sum(X,V,W))),
% 149.01/19.20 inference(miniscoping,[status(thm)],[f2])).
% 149.01/19.20 fof(f41,plain,(
% 149.01/19.20 ![X0,X1,X2,X3,X4,X5]: (sum(X0,X1,X2)|~sum(X3,X4,X0)|~sum(X4,X1,X5)|~sum(X3,X5,X2))),
% 149.01/19.20 inference(cnf_transformation,[status(thm)],[f40])).
% 149.01/19.20 fof(f42,plain,(
% 149.01/19.20 ![X0]: (sum(additive_identity,X0,X0)|~defined(X0))),
% 149.01/19.20 inference(cnf_transformation,[status(thm)],[f3])).
% 149.01/19.20 fof(f43,plain,(
% 149.01/19.20 ![X0]: (sum(additive_inverse(X0),X0,additive_identity)|~defined(X0))),
% 149.01/19.20 inference(cnf_transformation,[status(thm)],[f4])).
% 149.01/19.20 fof(f44,plain,(
% 149.01/19.20 ![X0,X1,X2]: (sum(X0,X1,X2)|~sum(X1,X0,X2))),
% 149.01/19.20 inference(cnf_transformation,[status(thm)],[f5])).
% 149.01/19.20 fof(f45,plain,(
% 149.01/19.20 ![W,U,Z]: ((![V,Y]: ((![X]: (product(X,V,W)|~product(X,Y,U)))|~product(Y,Z,V)))|~product(U,Z,W))),
% 149.01/19.20 inference(miniscoping,[status(thm)],[f6])).
% 149.01/19.20 fof(f46,plain,(
% 149.01/19.20 ![X0,X1,X2,X3,X4,X5]: (product(X0,X1,X2)|~product(X0,X3,X4)|~product(X3,X5,X1)|~product(X4,X5,X2))),
% 149.01/19.20 inference(cnf_transformation,[status(thm)],[f45])).
% 149.01/19.20 fof(f49,plain,(
% 149.01/19.20 ![X0]: (product(multiplicative_identity,X0,X0)|~defined(X0))),
% 149.01/19.20 inference(cnf_transformation,[status(thm)],[f8])).
% 149.01/19.20 fof(f50,plain,(
% 149.01/19.20 ![X0]: (product(multiplicative_inverse(X0),X0,multiplicative_identity)|sum(additive_identity,X0,additive_identity)|~defined(X0))),
% 149.01/19.20 inference(cnf_transformation,[status(thm)],[f9])).
% 149.01/19.20 fof(f51,plain,(
% 149.01/19.20 ![X0,X1,X2]: (product(X0,X1,X2)|~product(X1,X0,X2))),
% 149.01/19.20 inference(cnf_transformation,[status(thm)],[f10])).
% 149.01/19.20 fof(f52,plain,(
% 149.01/19.20 ![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))),
% 149.01/19.20 inference(miniscoping,[status(thm)],[f11])).
% 149.01/19.20 fof(f53,plain,(
% 149.01/19.20 ![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))),
% 149.01/19.20 inference(cnf_transformation,[status(thm)],[f52])).
% 149.01/19.20 fof(f54,plain,(
% 149.01/19.20 ![B,C,D]: ((![Z,Y]: ((![X]: ((![A]: (product(A,Z,B)|~sum(X,Y,A)))|~product(X,Z,C)))|~product(Y,Z,D)))|~sum(C,D,B))),
% 149.01/19.20 inference(miniscoping,[status(thm)],[f12])).
% 149.01/19.20 fof(f55,plain,(
% 149.01/19.20 ![X0,X1,X2,X3,X4,X5,X6]: (product(X0,X1,X2)|~sum(X3,X4,X0)|~product(X3,X1,X5)|~product(X4,X1,X6)|~sum(X5,X6,X2))),
% 149.01/19.20 inference(cnf_transformation,[status(thm)],[f54])).
% 149.01/19.20 fof(f58,plain,(
% 149.01/19.20 defined(additive_identity)),
% 149.01/19.20 inference(cnf_transformation,[status(thm)],[f14])).
% 149.01/19.20 fof(f59,plain,(
% 149.01/19.20 ![X0]: (defined(additive_inverse(X0))|~defined(X0))),
% 149.01/19.20 inference(cnf_transformation,[status(thm)],[f15])).
% 149.01/19.20 fof(f62,plain,(
% 149.01/19.20 defined(multiplicative_identity)),
% 149.01/19.20 inference(cnf_transformation,[status(thm)],[f17])).
% 149.01/19.20 fof(f71,plain,(
% 149.01/19.20 ![Y]: ((![X]: ((less_or_equal(X,Y)|less_or_equal(Y,X))|~defined(X)))|~defined(Y))),
% 149.01/19.20 inference(miniscoping,[status(thm)],[f23])).
% 149.01/19.20 fof(f72,plain,(
% 149.01/19.20 ![X0,X1]: (less_or_equal(X0,X1)|less_or_equal(X1,X0)|~defined(X0)|~defined(X1))),
% 149.01/19.20 inference(cnf_transformation,[status(thm)],[f71])).
% 149.01/19.20 fof(f76,plain,(
% 149.01/19.20 ~sum(additive_identity,additive_identity,multiplicative_identity)),
% 149.01/19.20 inference(cnf_transformation,[status(thm)],[f26])).
% 149.01/19.20 fof(f77,plain,(
% 149.01/19.20 defined(a)),
% 149.01/19.20 inference(cnf_transformation,[status(thm)],[f27])).
% 149.01/19.20 fof(f78,plain,(
% 149.01/19.20 defined(b)),
% 149.01/19.20 inference(cnf_transformation,[status(thm)],[f28])).
% 149.01/19.20 fof(f79,plain,(
% 149.01/19.20 defined(u)),
% 149.01/19.20 inference(cnf_transformation,[status(thm)],[f29])).
% 149.01/19.20 fof(f80,plain,(
% 149.01/19.20 defined(k)),
% 149.01/19.20 inference(cnf_transformation,[status(thm)],[f30])).
% 149.01/19.20 fof(f81,plain,(
% 149.01/19.20 defined(l)),
% 149.01/19.20 inference(cnf_transformation,[status(thm)],[f31])).
% 149.01/19.20 fof(f82,plain,(
% 149.01/19.20 ~sum(additive_identity,a,additive_identity)),
% 149.01/19.20 inference(cnf_transformation,[status(thm)],[f32])).
% 149.01/19.20 fof(f83,plain,(
% 149.01/19.20 ~sum(additive_identity,b,additive_identity)),
% 149.01/19.20 inference(cnf_transformation,[status(thm)],[f33])).
% 149.01/19.20 fof(f84,plain,(
% 149.01/19.20 sum(multiplicative_inverse(a),multiplicative_inverse(b),u)),
% 149.01/19.20 inference(cnf_transformation,[status(thm)],[f34])).
% 149.01/19.20 fof(f85,plain,(
% 149.01/19.20 sum(a,b,k)),
% 149.01/19.20 inference(cnf_transformation,[status(thm)],[f35])).
% 149.01/19.20 fof(f86,plain,(
% 149.01/19.20 product(a,b,l)),
% 149.01/19.20 inference(cnf_transformation,[status(thm)],[f36])).
% 149.01/19.20 fof(f87,plain,(
% 149.01/19.20 ~product(k,multiplicative_inverse(l),u)),
% 149.01/19.20 inference(cnf_transformation,[status(thm)],[f37])).
% 149.01/19.20 fof(f88,plain,(
% 149.01/19.20 sum(additive_identity,u,u)),
% 149.01/19.20 inference(resolution,[status(thm)],[f42,f79])).
% 149.01/19.20 fof(f89,plain,(
% 149.01/19.20 sum(additive_identity,b,b)),
% 149.01/19.20 inference(resolution,[status(thm)],[f42,f78])).
% 149.01/19.20 fof(f90,plain,(
% 149.01/19.20 sum(additive_identity,multiplicative_identity,multiplicative_identity)),
% 149.01/19.20 inference(resolution,[status(thm)],[f42,f62])).
% 149.01/19.20 fof(f91,plain,(
% 149.01/19.20 sum(additive_identity,a,a)),
% 149.01/19.20 inference(resolution,[status(thm)],[f42,f77])).
% 149.01/19.20 fof(f94,plain,(
% 149.01/19.20 sum(additive_inverse(b),b,additive_identity)),
% 149.01/19.20 inference(resolution,[status(thm)],[f43,f78])).
% 149.01/19.20 fof(f96,plain,(
% 149.01/19.20 sum(additive_inverse(a),a,additive_identity)),
% 149.01/19.20 inference(resolution,[status(thm)],[f43,f77])).
% 149.01/19.20 fof(f113,definition,(
% 149.01/19.20 sQ3_spl <=> (sum(additive_identity,b,additive_identity))),
% 149.01/19.20 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 149.01/19.20 fof(f114,plain,(
% 149.01/19.20 sum(additive_identity,b,additive_identity)|~sQ3_spl),
% 149.01/19.20 inference(component_clause,[status(thm)],[f113])).
% 149.01/19.20 fof(f127,definition,(
% 149.01/19.20 sQ7_spl <=> (sum(additive_identity,a,additive_identity))),
% 149.01/19.20 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 149.01/19.20 fof(f128,plain,(
% 149.01/19.20 sum(additive_identity,a,additive_identity)|~sQ7_spl),
% 149.01/19.20 inference(component_clause,[status(thm)],[f127])).
% 149.01/19.20 fof(f140,plain,(
% 149.01/19.20 ![X0]: (less_or_equal(X0,multiplicative_identity)|less_or_equal(multiplicative_identity,X0)|~defined(X0))),
% 149.01/19.20 inference(resolution,[status(thm)],[f72,f62])).
% 149.01/19.20 fof(f256,plain,(
% 149.01/19.20 product(multiplicative_inverse(b),b,multiplicative_identity)|sum(additive_identity,b,additive_identity)),
% 149.01/19.20 inference(resolution,[status(thm)],[f50,f78])).
% 149.01/19.20 fof(f258,plain,(
% 149.01/19.20 product(multiplicative_inverse(a),a,multiplicative_identity)|sum(additive_identity,a,additive_identity)),
% 149.01/19.20 inference(resolution,[status(thm)],[f50,f77])).
% 149.01/19.20 fof(f264,definition,(
% 149.01/19.20 sQ35_spl <=> (product(multiplicative_inverse(b),b,multiplicative_identity))),
% 149.01/19.20 introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition])).
% 149.01/19.20 fof(f265,plain,(
% 149.01/19.20 product(multiplicative_inverse(b),b,multiplicative_identity)|~sQ35_spl),
% 149.01/19.20 inference(component_clause,[status(thm)],[f264])).
% 149.01/19.20 fof(f267,plain,(
% 149.01/19.20 sQ35_spl|sQ3_spl),
% 149.01/19.20 inference(split_clause,[status(thm)],[f256,f264,f113])).
% 149.01/19.20 fof(f272,definition,(
% 149.01/19.20 sQ37_spl <=> (product(multiplicative_inverse(a),a,multiplicative_identity))),
% 149.01/19.20 introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition])).
% 149.01/19.20 fof(f273,plain,(
% 149.01/19.20 product(multiplicative_inverse(a),a,multiplicative_identity)|~sQ37_spl),
% 149.01/19.20 inference(component_clause,[status(thm)],[f272])).
% 149.01/19.20 fof(f275,plain,(
% 149.01/19.20 sQ37_spl|sQ7_spl),
% 149.01/19.20 inference(split_clause,[status(thm)],[f258,f272,f127])).
% 149.01/19.20 fof(f280,plain,(
% 149.01/19.20 $false|~sQ7_spl),
% 149.01/19.20 inference(forward_subsumption_resolution,[status(thm)],[f128,f82])).
% 149.01/19.20 fof(f281,plain,(
% 149.01/19.20 ~sQ7_spl),
% 149.01/19.20 inference(contradiction_clause,[status(thm)],[f280])).
% 149.01/19.20 fof(f282,plain,(
% 149.01/19.20 $false|~sQ3_spl),
% 149.01/19.20 inference(forward_subsumption_resolution,[status(thm)],[f114,f83])).
% 149.01/19.20 fof(f283,plain,(
% 149.01/19.20 ~sQ3_spl),
% 149.01/19.20 inference(contradiction_clause,[status(thm)],[f282])).
% 149.01/19.20 fof(f286,plain,(
% 149.01/19.20 less_or_equal(multiplicative_identity,multiplicative_identity)|less_or_equal(multiplicative_identity,multiplicative_identity)),
% 149.01/19.20 inference(resolution,[status(thm)],[f140,f62])).
% 149.01/19.20 fof(f291,definition,(
% 149.01/19.20 sQ39_spl <=> (less_or_equal(multiplicative_identity,multiplicative_identity))),
% 149.01/19.20 introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition])).
% 149.01/19.20 fof(f294,plain,(
% 149.01/19.20 sQ39_spl),
% 149.01/19.20 inference(split_clause,[status(thm)],[f286,f291])).
% 149.01/19.20 fof(f297,plain,(
% 149.01/19.20 sum(b,a,k)),
% 149.01/19.20 inference(resolution,[status(thm)],[f85,f44])).
% 149.01/19.20 fof(f298,plain,(
% 149.01/19.20 ![X0,X1,X2]: (sum(X0,X1,k)|~sum(a,X2,X0)|~sum(X2,X1,b))),
% 149.01/19.20 inference(resolution,[status(thm)],[f85,f41])).
% 149.01/19.20 fof(f301,plain,(
% 149.01/19.20 ![X0,X1,X2]: (sum(X0,X1,k)|~sum(X0,X2,a)|~sum(X2,b,X1))),
% 149.01/19.20 inference(resolution,[status(thm)],[f85,f39])).
% 149.01/19.20 fof(f303,plain,(
% 149.01/19.20 ![X0,X1,X2]: (sum(X0,k,X1)|~sum(X0,a,X2)|~sum(X2,b,X1))),
% 149.01/19.20 inference(resolution,[status(thm)],[f85,f39])).
% 149.01/19.20 fof(f310,plain,(
% 149.01/19.20 ![X0,X1,X2]: (sum(X0,k,X1)|~sum(X0,b,X2)|~sum(X2,a,X1))),
% 149.01/19.20 inference(resolution,[status(thm)],[f297,f39])).
% 149.01/19.20 fof(f325,plain,(
% 149.01/19.20 ![X0]: (sum(k,X0,k)|~sum(b,X0,b))),
% 149.01/19.20 inference(resolution,[status(thm)],[f298,f85])).
% 149.01/19.20 fof(f340,plain,(
% 149.01/19.20 ![X0,X1,X2]: (product(X0,l,X1)|~product(X0,a,X2)|~product(X2,b,X1))),
% 149.01/19.20 inference(resolution,[status(thm)],[f46,f86])).
% 149.01/19.20 fof(f347,plain,(
% 149.01/19.20 product(b,a,l)),
% 149.01/19.20 inference(resolution,[status(thm)],[f51,f86])).
% 149.01/19.20 fof(f354,plain,(
% 149.01/19.20 ![X0,X1,X2]: (product(X0,l,X1)|~product(X0,b,X2)|~product(X2,a,X1))),
% 149.01/19.20 inference(resolution,[status(thm)],[f347,f46])).
% 149.01/19.20 fof(f362,plain,(
% 149.01/19.20 ![X0]: (less_or_equal(X0,k)|less_or_equal(k,X0)|~defined(X0))),
% 149.01/19.20 inference(resolution,[status(thm)],[f80,f72])).
% 149.01/19.20 fof(f413,plain,(
% 149.01/19.20 product(multiplicative_inverse(l),l,multiplicative_identity)|sum(additive_identity,l,additive_identity)),
% 149.01/19.20 inference(resolution,[status(thm)],[f81,f50])).
% 149.01/19.20 fof(f418,plain,(
% 149.01/19.20 ![X0]: (less_or_equal(X0,l)|less_or_equal(l,X0)|~defined(X0))),
% 149.01/19.20 inference(resolution,[status(thm)],[f81,f72])).
% 149.01/19.20 fof(f421,plain,(
% 149.01/19.20 sum(additive_identity,l,l)),
% 149.01/19.20 inference(resolution,[status(thm)],[f81,f42])).
% 149.01/19.20 fof(f429,definition,(
% 149.01/19.20 sQ55_spl <=> (product(multiplicative_inverse(l),l,multiplicative_identity))),
% 149.01/19.20 introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition])).
% 149.01/19.20 fof(f430,plain,(
% 149.01/19.20 product(multiplicative_inverse(l),l,multiplicative_identity)|~sQ55_spl),
% 149.01/19.20 inference(component_clause,[status(thm)],[f429])).
% 149.01/19.20 fof(f432,definition,(
% 149.01/19.20 sQ56_spl <=> (sum(additive_identity,l,additive_identity))),
% 149.01/19.20 introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition])).
% 149.01/19.20 fof(f433,plain,(
% 149.01/19.20 sum(additive_identity,l,additive_identity)|~sQ56_spl),
% 149.01/19.20 inference(component_clause,[status(thm)],[f432])).
% 149.01/19.20 fof(f435,plain,(
% 149.01/19.20 sQ55_spl|sQ56_spl),
% 149.01/19.20 inference(split_clause,[status(thm)],[f413,f429,f432])).
% 149.01/19.20 fof(f478,definition,(
% 149.01/19.20 sQ66_spl <=> (sum(l,l,l))),
% 149.01/19.20 introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition])).
% 149.01/19.20 fof(f485,definition,(
% 149.01/19.20 sQ68_spl <=> (sum(a,a,a))),
% 149.01/19.20 introduced(definition,[new_symbols(definition,[sQ68_spl])],[split_symbol_definition])).
% 149.01/19.20 fof(f486,plain,(
% 149.01/19.20 sum(a,a,a)|~sQ68_spl),
% 149.01/19.20 inference(component_clause,[status(thm)],[f485])).
% 149.01/19.20 fof(f497,plain,(
% 149.01/19.20 ![X0,X1,X2,X3]: (product(X0,X1,k)|~sum(X2,X3,X0)|~product(X2,X1,b)|~product(X3,X1,a))),
% 149.01/19.20 inference(resolution,[status(thm)],[f55,f297])).
% 149.01/19.20 fof(f501,plain,(
% 149.01/19.20 product(multiplicative_identity,u,u)),
% 149.01/19.20 inference(resolution,[status(thm)],[f49,f79])).
% 149.01/19.20 fof(f502,plain,(
% 149.01/19.20 product(multiplicative_identity,b,b)),
% 149.01/19.20 inference(resolution,[status(thm)],[f49,f78])).
% 149.01/19.20 fof(f504,plain,(
% 149.01/19.20 product(multiplicative_identity,a,a)),
% 149.01/19.20 inference(resolution,[status(thm)],[f49,f77])).
% 149.01/19.20 fof(f513,plain,(
% 149.01/19.20 defined(additive_inverse(l))),
% 149.01/19.20 inference(resolution,[status(thm)],[f59,f81])).
% 149.01/19.20 fof(f514,plain,(
% 149.01/19.20 defined(additive_inverse(k))),
% 149.01/19.20 inference(resolution,[status(thm)],[f59,f80])).
% 149.01/19.20 fof(f515,plain,(
% 149.01/19.20 defined(additive_inverse(u))),
% 149.01/19.20 inference(resolution,[status(thm)],[f59,f79])).
% 149.01/19.20 fof(f516,plain,(
% 149.01/19.20 defined(additive_inverse(b))),
% 149.01/19.20 inference(resolution,[status(thm)],[f59,f78])).
% 149.01/19.20 fof(f517,plain,(
% 149.01/19.20 defined(additive_inverse(multiplicative_identity))),
% 149.01/19.20 inference(resolution,[status(thm)],[f59,f62])).
% 149.01/19.20 fof(f518,plain,(
% 149.01/19.20 defined(additive_inverse(a))),
% 149.01/19.20 inference(resolution,[status(thm)],[f59,f77])).
% 149.01/19.20 fof(f519,plain,(
% 149.01/19.20 defined(additive_inverse(additive_identity))),
% 149.01/19.20 inference(resolution,[status(thm)],[f59,f58])).
% 149.01/19.20 fof(f521,plain,(
% 149.01/19.20 less_or_equal(k,k)|less_or_equal(k,k)),
% 149.01/19.20 inference(resolution,[status(thm)],[f362,f80])).
% 149.01/19.20 fof(f534,definition,(
% 149.01/19.20 sQ71_spl <=> (less_or_equal(k,k))),
% 149.01/19.20 introduced(definition,[new_symbols(definition,[sQ71_spl])],[split_symbol_definition])).
% 149.01/19.20 fof(f537,plain,(
% 149.01/19.20 sQ71_spl),
% 149.01/19.20 inference(split_clause,[status(thm)],[f521,f534])).
% 149.01/19.20 fof(f543,plain,(
% 149.01/19.20 less_or_equal(l,l)|less_or_equal(l,l)),
% 149.01/19.20 inference(resolution,[status(thm)],[f418,f81])).
% 149.01/19.20 fof(f550,definition,(
% 149.01/19.20 sQ72_spl <=> (less_or_equal(l,l))),
% 149.01/19.20 introduced(definition,[new_symbols(definition,[sQ72_spl])],[split_symbol_definition])).
% 149.01/19.20 fof(f553,plain,(
% 149.01/19.20 sQ72_spl),
% 149.01/19.20 inference(split_clause,[status(thm)],[f543,f550])).
% 149.01/19.20 fof(f634,plain,(
% 149.01/19.20 sum(u,additive_identity,u)),
% 149.01/19.20 inference(resolution,[status(thm)],[f88,f44])).
% 149.01/19.20 fof(f645,plain,(
% 149.01/19.20 ![X0]: (sum(X0,k,b)|~sum(X0,a,additive_identity))),
% 149.01/19.20 inference(resolution,[status(thm)],[f89,f303])).
% 149.01/19.20 fof(f659,plain,(
% 149.01/19.20 sum(multiplicative_identity,additive_identity,multiplicative_identity)),
% 149.01/19.20 inference(resolution,[status(thm)],[f90,f44])).
% 149.01/19.20 fof(f698,plain,(
% 149.01/19.20 ![X0]: (sum(additive_inverse(b),k,X0)|~sum(additive_identity,a,X0))),
% 149.01/19.20 inference(resolution,[status(thm)],[f94,f310])).
% 149.01/19.20 fof(f700,plain,(
% 149.01/19.20 ![X0]: (sum(X0,additive_identity,k)|~sum(X0,additive_inverse(b),a))),
% 149.01/19.20 inference(resolution,[status(thm)],[f94,f301])).
% 149.01/19.20 fof(f730,plain,(
% 149.01/19.20 sum(additive_inverse(b),k,a)),
% 149.01/19.20 inference(resolution,[status(thm)],[f698,f91])).
% 149.01/19.20 fof(f734,plain,(
% 149.01/19.20 sum(k,additive_inverse(b),a)),
% 149.01/19.20 inference(resolution,[status(thm)],[f730,f44])).
% 149.01/19.20 fof(f745,plain,(
% 149.01/19.20 ![X0]: (sum(X0,a,a)|~sum(X0,k,k))),
% 149.01/19.20 inference(resolution,[status(thm)],[f734,f39])).
% 149.01/19.20 fof(f749,plain,(
% 149.01/19.20 sum(k,additive_identity,k)),
% 149.01/19.20 inference(resolution,[status(thm)],[f700,f734])).
% 149.01/19.20 fof(f753,plain,(
% 149.01/19.20 ![X0,X1,X2]: (sum(X0,X1,k)|~sum(k,X2,X0)|~sum(X2,X1,additive_identity))),
% 149.01/19.20 inference(resolution,[status(thm)],[f749,f41])).
% 149.01/19.20 fof(f759,plain,(
% 149.01/19.20 ![X0]: (sum(k,X0,k)|~sum(additive_identity,X0,additive_identity))),
% 149.01/19.20 inference(resolution,[status(thm)],[f753,f749])).
% 149.01/19.20 fof(f777,plain,(
% 149.01/19.20 sum(additive_inverse(a),k,b)),
% 149.01/19.20 inference(resolution,[status(thm)],[f96,f645])).
% 149.01/19.20 fof(f793,plain,(
% 149.01/19.20 sum(k,additive_inverse(a),b)),
% 149.01/19.20 inference(resolution,[status(thm)],[f777,f44])).
% 149.01/19.20 fof(f794,plain,(
% 149.01/19.20 ![X0,X1,X2]: (sum(X0,X1,b)|~sum(additive_inverse(a),X2,X0)|~sum(X2,X1,k))),
% 149.01/19.20 inference(resolution,[status(thm)],[f777,f41])).
% 149.01/19.20 fof(f806,plain,(
% 149.01/19.20 ![X0,X1,X2]: (sum(X0,additive_inverse(a),X1)|~sum(X2,k,X0)|~sum(X2,b,X1))),
% 149.01/19.20 inference(resolution,[status(thm)],[f793,f41])).
% 149.01/19.20 fof(f811,plain,(
% 149.01/19.20 ![X0]: (sum(b,X0,b)|~sum(k,X0,k))),
% 149.01/19.20 inference(resolution,[status(thm)],[f794,f777])).
% 149.01/19.20 fof(f1023,definition,(
% 149.01/19.20 sQ111_spl <=> (sum(additive_identity,additive_identity,multiplicative_identity))),
% 149.01/19.20 introduced(definition,[new_symbols(definition,[sQ111_spl])],[split_symbol_definition])).
% 149.01/19.20 fof(f1024,plain,(
% 149.01/19.20 sum(additive_identity,additive_identity,multiplicative_identity)|~sQ111_spl),
% 149.01/19.20 inference(component_clause,[status(thm)],[f1023])).
% 149.01/19.20 fof(f1059,plain,(
% 149.01/19.20 $false|~sQ111_spl),
% 149.01/19.20 inference(forward_subsumption_resolution,[status(thm)],[f1024,f76])).
% 149.01/19.20 fof(f1060,plain,(
% 149.01/19.20 ~sQ111_spl),
% 149.01/19.20 inference(contradiction_clause,[status(thm)],[f1059])).
% 149.01/19.20 fof(f1229,plain,(
% 149.01/19.20 ![X0]: (sum(a,additive_inverse(a),X0)|~sum(additive_inverse(b),b,X0))),
% 149.01/19.20 inference(resolution,[status(thm)],[f806,f730])).
% 149.01/19.20 fof(f1290,plain,(
% 149.01/19.20 defined(additive_inverse(additive_inverse(l)))),
% 149.01/19.20 inference(resolution,[status(thm)],[f513,f59])).
% 149.01/19.20 fof(f1299,plain,(
% 149.01/19.20 ![X0]: (less_or_equal(X0,additive_inverse(l))|less_or_equal(additive_inverse(l),X0)|~defined(X0))),
% 149.01/19.20 inference(resolution,[status(thm)],[f513,f72])).
% 149.01/19.20 fof(f1377,plain,(
% 149.01/19.20 less_or_equal(additive_inverse(l),additive_inverse(l))|less_or_equal(additive_inverse(l),additive_inverse(l))),
% 149.01/19.20 inference(resolution,[status(thm)],[f1299,f513])).
% 149.01/19.20 fof(f1387,definition,(
% 149.01/19.20 sQ153_spl <=> (less_or_equal(additive_inverse(l),additive_inverse(l)))),
% 149.01/19.20 introduced(definition,[new_symbols(definition,[sQ153_spl])],[split_symbol_definition])).
% 149.01/19.20 fof(f1390,plain,(
% 149.01/19.20 sQ153_spl),
% 149.01/19.20 inference(split_clause,[status(thm)],[f1377,f1387])).
% 149.01/19.20 fof(f1519,plain,(
% 149.01/19.20 defined(additive_inverse(additive_inverse(k)))),
% 149.01/19.20 inference(resolution,[status(thm)],[f514,f59])).
% 149.01/19.20 fof(f1528,plain,(
% 149.01/19.20 ![X0]: (less_or_equal(X0,additive_inverse(k))|less_or_equal(additive_inverse(k),X0)|~defined(X0))),
% 149.01/19.20 inference(resolution,[status(thm)],[f514,f72])).
% 149.01/19.20 fof(f1621,plain,(
% 149.01/19.20 defined(additive_inverse(additive_inverse(u)))),
% 149.01/19.20 inference(resolution,[status(thm)],[f515,f59])).
% 149.01/19.20 fof(f1630,plain,(
% 149.01/19.20 ![X0]: (less_or_equal(X0,additive_inverse(u))|less_or_equal(additive_inverse(u),X0)|~defined(X0))),
% 149.01/19.20 inference(resolution,[status(thm)],[f515,f72])).
% 149.01/19.20 fof(f1805,plain,(
% 149.01/19.20 ![X0]: (product(multiplicative_inverse(b),l,X0)|~product(multiplicative_identity,a,X0)|~sQ35_spl)),
% 149.01/19.20 inference(resolution,[status(thm)],[f265,f354])).
% 149.01/19.20 fof(f1888,plain,(
% 149.01/19.20 ![X0]: (less_or_equal(X0,additive_inverse(b))|less_or_equal(additive_inverse(b),X0)|~defined(X0))),
% 149.01/19.20 inference(resolution,[status(thm)],[f516,f72])).
% 149.01/19.20 fof(f1987,plain,(
% 149.01/19.20 ![X0]: (less_or_equal(X0,additive_inverse(multiplicative_identity))|less_or_equal(additive_inverse(multiplicative_identity),X0)|~defined(X0))),
% 149.01/19.20 inference(resolution,[status(thm)],[f517,f72])).
% 149.01/19.20 fof(f2089,plain,(
% 149.01/19.20 ![X0]: (less_or_equal(X0,additive_inverse(a))|less_or_equal(additive_inverse(a),X0)|~defined(X0))),
% 149.01/19.20 inference(resolution,[status(thm)],[f518,f72])).
% 149.01/19.20 fof(f2192,plain,(
% 149.01/19.20 less_or_equal(additive_inverse(k),additive_inverse(k))|less_or_equal(additive_inverse(k),additive_inverse(k))),
% 149.01/19.20 inference(resolution,[status(thm)],[f1528,f514])).
% 149.01/19.20 fof(f2231,definition,(
% 149.01/19.20 sQ296_spl <=> (less_or_equal(additive_inverse(k),additive_inverse(k)))),
% 149.01/19.20 introduced(definition,[new_symbols(definition,[sQ296_spl])],[split_symbol_definition])).
% 149.01/19.20 fof(f2234,plain,(
% 149.01/19.20 sQ296_spl),
% 149.01/19.22 inference(split_clause,[status(thm)],[f2192,f2231])).
% 149.01/19.22 fof(f2248,plain,(
% 149.01/19.22 less_or_equal(additive_inverse(u),additive_inverse(u))|less_or_equal(additive_inverse(u),additive_inverse(u))),
% 149.01/19.22 inference(resolution,[status(thm)],[f1630,f515])).
% 149.01/19.22 fof(f2281,definition,(
% 149.01/19.22 sQ303_spl <=> (less_or_equal(additive_inverse(u),additive_inverse(u)))),
% 149.01/19.22 introduced(definition,[new_symbols(definition,[sQ303_spl])],[split_symbol_definition])).
% 149.01/19.22 fof(f2284,plain,(
% 149.01/19.22 sQ303_spl),
% 149.01/19.22 inference(split_clause,[status(thm)],[f2248,f2281])).
% 149.01/19.22 fof(f2298,plain,(
% 149.01/19.22 less_or_equal(additive_inverse(b),additive_inverse(b))|less_or_equal(additive_inverse(b),additive_inverse(b))),
% 149.01/19.22 inference(resolution,[status(thm)],[f1888,f516])).
% 149.01/19.22 fof(f2325,definition,(
% 149.01/19.22 sQ308_spl <=> (less_or_equal(additive_inverse(b),additive_inverse(b)))),
% 149.01/19.22 introduced(definition,[new_symbols(definition,[sQ308_spl])],[split_symbol_definition])).
% 149.01/19.22 fof(f2328,plain,(
% 149.01/19.22 sQ308_spl),
% 149.01/19.22 inference(split_clause,[status(thm)],[f2298,f2325])).
% 149.01/19.22 fof(f2341,plain,(
% 149.01/19.22 less_or_equal(additive_inverse(a),additive_inverse(a))|less_or_equal(additive_inverse(a),additive_inverse(a))),
% 149.01/19.22 inference(resolution,[status(thm)],[f2089,f518])).
% 149.01/19.22 fof(f2356,definition,(
% 149.01/19.22 sQ309_spl <=> (less_or_equal(additive_inverse(a),additive_inverse(a)))),
% 149.01/19.22 introduced(definition,[new_symbols(definition,[sQ309_spl])],[split_symbol_definition])).
% 149.01/19.22 fof(f2359,plain,(
% 149.01/19.22 sQ309_spl),
% 149.01/19.22 inference(split_clause,[status(thm)],[f2341,f2356])).
% 149.01/19.22 fof(f2381,plain,(
% 149.01/19.22 less_or_equal(additive_inverse(multiplicative_identity),additive_inverse(multiplicative_identity))|less_or_equal(additive_inverse(multiplicative_identity),additive_inverse(multiplicative_identity))),
% 149.01/19.22 inference(resolution,[status(thm)],[f1987,f517])).
% 149.01/19.22 fof(f2396,definition,(
% 149.01/19.22 sQ312_spl <=> (less_or_equal(additive_inverse(multiplicative_identity),additive_inverse(multiplicative_identity)))),
% 149.01/19.22 introduced(definition,[new_symbols(definition,[sQ312_spl])],[split_symbol_definition])).
% 149.01/19.22 fof(f2399,plain,(
% 149.01/19.22 sQ312_spl),
% 149.01/19.22 inference(split_clause,[status(thm)],[f2381,f2396])).
% 149.01/19.22 fof(f2565,plain,(
% 149.01/19.22 ![X0]: (less_or_equal(X0,additive_inverse(additive_identity))|less_or_equal(additive_inverse(additive_identity),X0)|~defined(X0))),
% 149.01/19.22 inference(resolution,[status(thm)],[f519,f72])).
% 149.01/19.22 fof(f2787,plain,(
% 149.01/19.22 less_or_equal(additive_inverse(additive_identity),additive_inverse(additive_identity))|less_or_equal(additive_inverse(additive_identity),additive_inverse(additive_identity))),
% 149.01/19.22 inference(resolution,[status(thm)],[f2565,f519])).
% 149.01/19.22 fof(f2803,definition,(
% 149.01/19.22 sQ348_spl <=> (less_or_equal(additive_inverse(additive_identity),additive_inverse(additive_identity)))),
% 149.01/19.22 introduced(definition,[new_symbols(definition,[sQ348_spl])],[split_symbol_definition])).
% 149.01/19.22 fof(f2806,plain,(
% 149.01/19.22 sQ348_spl),
% 149.01/19.22 inference(split_clause,[status(thm)],[f2787,f2803])).
% 149.01/19.22 fof(f3040,plain,(
% 149.01/19.22 sum(k,l,k)|~sQ56_spl),
% 149.01/19.22 inference(resolution,[status(thm)],[f433,f759])).
% 149.01/19.22 fof(f3176,plain,(
% 149.01/19.22 ![X0]: (product(X0,l,b)|~product(X0,a,multiplicative_identity))),
% 149.01/19.22 inference(resolution,[status(thm)],[f502,f340])).
% 149.01/19.22 fof(f3213,definition,(
% 149.01/19.22 sQ358_spl <=> (sum(b,l,b))),
% 149.01/19.22 introduced(definition,[new_symbols(definition,[sQ358_spl])],[split_symbol_definition])).
% 149.01/19.22 fof(f3214,plain,(
% 149.01/19.22 sum(b,l,b)|~sQ358_spl),
% 149.01/19.22 inference(component_clause,[status(thm)],[f3213])).
% 149.01/19.22 fof(f3438,plain,(
% 149.01/19.22 sum(k,l,k)|~sQ358_spl),
% 149.01/19.22 inference(resolution,[status(thm)],[f3214,f325])).
% 149.01/19.22 fof(f3453,plain,(
% 149.01/19.22 ![X0,X1,X2]: (sum(X0,b,X1)|~sum(X0,b,X2)|~sum(X2,l,X1)|~sQ358_spl)),
% 149.01/19.22 inference(resolution,[status(thm)],[f3214,f39])).
% 149.01/19.22 fof(f3545,plain,(
% 149.01/19.22 product(multiplicative_inverse(a),l,b)|~sQ37_spl),
% 149.01/19.22 inference(resolution,[status(thm)],[f3176,f273])).
% 149.01/19.22 fof(f4067,plain,(
% 149.01/19.22 product(multiplicative_inverse(b),l,a)|~sQ35_spl),
% 149.01/19.22 inference(resolution,[status(thm)],[f504,f1805])).
% 149.01/19.22 fof(f4391,plain,(
% 149.01/19.22 ![X0,X1,X2]: (sum(X0,a,X1)|~sum(X2,a,X0)|~sum(X2,a,X1)|~sQ68_spl)),
% 149.01/19.22 inference(resolution,[status(thm)],[f486,f41])).
% 149.01/19.22 fof(f4579,plain,(
% 149.01/19.22 ![X0]: (sum(X0,a,additive_identity)|~sum(additive_inverse(a),a,X0)|~sQ68_spl)),
% 149.01/19.22 inference(resolution,[status(thm)],[f4391,f96])).
% 149.01/19.22 fof(f5243,plain,(
% 149.01/19.22 sum(l,k,k)|~sQ358_spl),
% 149.01/19.22 inference(resolution,[status(thm)],[f3438,f44])).
% 149.01/19.22 fof(f5912,plain,(
% 149.01/19.22 sum(l,a,a)|~sQ358_spl),
% 149.01/19.22 inference(resolution,[status(thm)],[f5243,f745])).
% 149.01/19.22 fof(f6123,plain,(
% 149.01/19.22 sum(b,l,b)|~sQ56_spl),
% 149.01/19.22 inference(resolution,[status(thm)],[f3040,f811])).
% 149.01/19.22 fof(f6137,plain,(
% 149.01/19.22 sQ358_spl|~sQ56_spl),
% 149.01/19.22 inference(split_clause,[status(thm)],[f6123,f3213,f432])).
% 149.01/19.22 fof(f6523,plain,(
% 149.01/19.22 ![X0,X1]: (product(X0,l,k)|~sum(X1,multiplicative_inverse(b),X0)|~product(X1,l,b)|~sQ35_spl)),
% 149.01/19.22 inference(resolution,[status(thm)],[f4067,f497])).
% 149.01/19.22 fof(f6536,plain,(
% 149.01/19.22 product(l,multiplicative_inverse(b),a)|~sQ35_spl),
% 149.01/19.22 inference(resolution,[status(thm)],[f4067,f51])).
% 149.01/19.22 fof(f6567,plain,(
% 149.01/19.22 sum(a,a,a)|~sum(l,l,l)|~sQ35_spl),
% 149.01/19.22 inference(resolution,[status(thm)],[f6536,f53])).
% 149.01/19.22 fof(f6581,plain,(
% 149.01/19.22 sQ68_spl|~sQ66_spl|~sQ35_spl),
% 149.01/19.22 inference(split_clause,[status(thm)],[f6567,f485,f478,f264])).
% 149.01/19.22 fof(f7363,plain,(
% 149.01/19.22 sum(additive_identity,a,additive_identity)|~sQ68_spl),
% 149.01/19.22 inference(resolution,[status(thm)],[f4579,f96])).
% 149.01/19.22 fof(f7364,plain,(
% 149.01/19.22 sQ7_spl|~sQ68_spl),
% 149.01/19.22 inference(split_clause,[status(thm)],[f7363,f127,f485])).
% 149.01/19.22 fof(f7502,plain,(
% 149.01/19.22 ![X0]: (sum(X0,b,l)|~sum(X0,b,additive_identity)|~sQ358_spl)),
% 149.01/19.22 inference(resolution,[status(thm)],[f3453,f421])).
% 149.01/19.22 fof(f7686,definition,(
% 149.01/19.22 sQ564_spl <=> (product(u,l,k))),
% 149.01/19.22 introduced(definition,[new_symbols(definition,[sQ564_spl])],[split_symbol_definition])).
% 149.01/19.22 fof(f7687,plain,(
% 149.01/19.22 product(u,l,k)|~sQ564_spl),
% 149.01/19.22 inference(component_clause,[status(thm)],[f7686])).
% 149.01/19.22 fof(f7712,plain,(
% 149.01/19.22 product(l,u,k)|~sQ564_spl),
% 149.01/19.22 inference(resolution,[status(thm)],[f7687,f51])).
% 149.01/19.22 fof(f7841,plain,(
% 149.01/19.22 ![X0,X1,X2]: (product(X0,k,X1)|~product(X0,l,X2)|~product(X2,u,X1)|~sQ564_spl)),
% 149.01/19.22 inference(resolution,[status(thm)],[f7712,f46])).
% 149.01/19.22 fof(f9785,plain,(
% 149.01/19.22 product(u,l,k)|~product(multiplicative_inverse(a),l,b)|~sQ35_spl),
% 149.01/19.22 inference(resolution,[status(thm)],[f6523,f84])).
% 149.01/19.22 fof(f9786,definition,(
% 149.01/19.22 sQ578_spl <=> (product(multiplicative_inverse(a),l,b))),
% 149.01/19.22 introduced(definition,[new_symbols(definition,[sQ578_spl])],[split_symbol_definition])).
% 149.01/19.22 fof(f9788,plain,(
% 149.01/19.22 ~product(multiplicative_inverse(a),l,b)|sQ578_spl),
% 149.01/19.22 inference(component_clause,[status(thm)],[f9786])).
% 149.01/19.22 fof(f9789,plain,(
% 149.01/19.22 sQ564_spl|~sQ578_spl|~sQ35_spl),
% 149.01/19.22 inference(split_clause,[status(thm)],[f9785,f7686,f9786,f264])).
% 149.01/19.22 fof(f11897,plain,(
% 149.01/19.22 $false|~sQ37_spl|sQ578_spl),
% 149.01/19.22 inference(forward_subsumption_resolution,[status(thm)],[f9788,f3545])).
% 149.01/19.22 fof(f11898,plain,(
% 149.01/19.22 ~sQ37_spl|sQ578_spl),
% 149.01/19.22 inference(contradiction_clause,[status(thm)],[f11897])).
% 149.01/19.22 fof(f15201,plain,(
% 149.01/19.22 ![X0]: (product(multiplicative_inverse(l),k,X0)|~product(multiplicative_identity,u,X0)|~sQ564_spl|~sQ55_spl)),
% 149.01/19.22 inference(resolution,[status(thm)],[f7841,f430])).
% 149.01/19.22 fof(f21973,definition,(
% 149.01/19.22 sQ797_spl <=> (sum(u,additive_identity,u))),
% 149.01/19.22 introduced(definition,[new_symbols(definition,[sQ797_spl])],[split_symbol_definition])).
% 149.01/19.22 fof(f21975,plain,(
% 149.01/19.22 ~sum(u,additive_identity,u)|sQ797_spl),
% 149.01/19.22 inference(component_clause,[status(thm)],[f21973])).
% 149.01/19.22 fof(f21979,definition,(
% 149.01/19.22 sQ798_spl <=> (sum(multiplicative_identity,additive_identity,multiplicative_identity))),
% 149.01/19.22 introduced(definition,[new_symbols(definition,[sQ798_spl])],[split_symbol_definition])).
% 149.01/19.22 fof(f21981,plain,(
% 149.01/19.22 ~sum(multiplicative_identity,additive_identity,multiplicative_identity)|sQ798_spl),
% 149.01/19.22 inference(component_clause,[status(thm)],[f21979])).
% 149.01/19.22 fof(f21995,plain,(
% 149.01/19.22 $false|sQ797_spl),
% 149.01/19.22 inference(forward_subsumption_resolution,[status(thm)],[f21975,f634])).
% 149.01/19.22 fof(f21996,plain,(
% 149.01/19.22 sQ797_spl),
% 149.01/19.22 inference(contradiction_clause,[status(thm)],[f21995])).
% 149.01/19.22 fof(f21999,plain,(
% 149.01/19.22 $false|sQ798_spl),
% 149.01/19.22 inference(forward_subsumption_resolution,[status(thm)],[f21981,f659])).
% 149.01/19.22 fof(f22000,plain,(
% 149.01/19.22 sQ798_spl),
% 149.01/19.22 inference(contradiction_clause,[status(thm)],[f21999])).
% 149.01/19.22 fof(f22547,plain,(
% 149.01/19.22 sum(additive_inverse(b),b,l)|~sQ358_spl),
% 149.01/19.22 inference(resolution,[status(thm)],[f7502,f94])).
% 149.01/19.22 fof(f23822,plain,(
% 149.01/19.22 sum(a,additive_inverse(a),l)|~sQ358_spl),
% 149.01/19.22 inference(resolution,[status(thm)],[f22547,f1229])).
% 149.01/19.22 fof(f24230,plain,(
% 149.01/19.22 ![X0]: (sum(X0,l,l)|~sum(X0,a,a)|~sQ358_spl)),
% 149.01/19.22 inference(resolution,[status(thm)],[f23822,f39])).
% 149.01/19.22 fof(f26245,plain,(
% 149.01/19.22 ![X0]: (less_or_equal(X0,additive_inverse(additive_inverse(l)))|less_or_equal(additive_inverse(additive_inverse(l)),X0)|~defined(X0))),
% 149.01/19.22 inference(resolution,[status(thm)],[f1290,f72])).
% 149.01/19.22 fof(f26456,plain,(
% 149.01/19.22 less_or_equal(additive_inverse(additive_inverse(l)),additive_inverse(additive_inverse(l)))|less_or_equal(additive_inverse(additive_inverse(l)),additive_inverse(additive_inverse(l)))),
% 149.01/19.22 inference(resolution,[status(thm)],[f26245,f1290])).
% 149.01/19.22 fof(f26478,definition,(
% 149.01/19.22 sQ921_spl <=> (less_or_equal(additive_inverse(additive_inverse(l)),additive_inverse(additive_inverse(l))))),
% 149.01/19.22 introduced(definition,[new_symbols(definition,[sQ921_spl])],[split_symbol_definition])).
% 149.01/19.22 fof(f26481,plain,(
% 149.01/19.22 sQ921_spl),
% 149.01/19.22 inference(split_clause,[status(thm)],[f26456,f26478])).
% 149.01/19.22 fof(f26987,plain,(
% 149.01/19.22 ![X0]: (less_or_equal(X0,additive_inverse(additive_inverse(k)))|less_or_equal(additive_inverse(additive_inverse(k)),X0)|~defined(X0))),
% 149.01/19.22 inference(resolution,[status(thm)],[f1519,f72])).
% 149.01/19.22 fof(f27179,plain,(
% 149.01/19.22 less_or_equal(additive_inverse(additive_inverse(k)),additive_inverse(additive_inverse(k)))|less_or_equal(additive_inverse(additive_inverse(k)),additive_inverse(additive_inverse(k)))),
% 149.01/19.22 inference(resolution,[status(thm)],[f26987,f1519])).
% 149.01/19.22 fof(f27202,definition,(
% 149.01/19.22 sQ972_spl <=> (less_or_equal(additive_inverse(additive_inverse(k)),additive_inverse(additive_inverse(k))))),
% 149.01/19.22 introduced(definition,[new_symbols(definition,[sQ972_spl])],[split_symbol_definition])).
% 149.01/19.22 fof(f27205,plain,(
% 149.01/19.22 sQ972_spl),
% 149.01/19.22 inference(split_clause,[status(thm)],[f27179,f27202])).
% 149.01/19.22 fof(f27237,plain,(
% 149.01/19.22 sum(l,l,l)|~sQ358_spl),
% 149.01/19.22 inference(resolution,[status(thm)],[f24230,f5912])).
% 149.01/19.22 fof(f27240,plain,(
% 149.01/19.22 sQ66_spl|~sQ358_spl),
% 149.01/19.22 inference(split_clause,[status(thm)],[f27237,f478,f3213])).
% 149.01/19.22 fof(f28963,plain,(
% 149.01/19.22 ![X0]: (less_or_equal(X0,additive_inverse(additive_inverse(u)))|less_or_equal(additive_inverse(additive_inverse(u)),X0)|~defined(X0))),
% 149.01/19.22 inference(resolution,[status(thm)],[f1621,f72])).
% 149.01/19.22 fof(f29146,plain,(
% 149.01/19.22 less_or_equal(additive_inverse(additive_inverse(u)),additive_inverse(additive_inverse(u)))|less_or_equal(additive_inverse(additive_inverse(u)),additive_inverse(additive_inverse(u)))),
% 149.01/19.22 inference(resolution,[status(thm)],[f28963,f1621])).
% 149.01/19.22 fof(f29171,definition,(
% 149.01/19.22 sQ1081_spl <=> (less_or_equal(additive_inverse(additive_inverse(u)),additive_inverse(additive_inverse(u))))),
% 149.01/19.22 introduced(definition,[new_symbols(definition,[sQ1081_spl])],[split_symbol_definition])).
% 149.01/19.22 fof(f29174,plain,(
% 149.01/19.22 sQ1081_spl),
% 149.01/19.22 inference(split_clause,[status(thm)],[f29146,f29171])).
% 149.01/19.22 fof(f29485,plain,(
% 149.01/19.22 product(multiplicative_inverse(l),k,u)|~sQ564_spl|~sQ55_spl),
% 149.01/19.22 inference(resolution,[status(thm)],[f15201,f501])).
% 149.01/19.22 fof(f29752,plain,(
% 149.01/19.22 product(k,multiplicative_inverse(l),u)|~sQ564_spl|~sQ55_spl),
% 149.01/19.22 inference(resolution,[status(thm)],[f29485,f51])).
% 149.01/19.22 fof(f29763,plain,(
% 149.01/19.22 $false|~sQ564_spl|~sQ55_spl),
% 149.01/19.22 inference(forward_subsumption_resolution,[status(thm)],[f29752,f87])).
% 149.01/19.22 fof(f29764,plain,(
% 149.01/19.22 ~sQ564_spl|~sQ55_spl),
% 149.01/19.22 inference(contradiction_clause,[status(thm)],[f29763])).
% 130.54/19.30 fof(f29765,plain,(
% 130.54/19.30 $false),
% 130.54/19.30 inference(sat_refutation,[status(thm)],[f267,f275,f281,f283,f294,f435,f537,f553,f1060,f1390,f2234,f2284,f2328,f2359,f2399,f2806,f6137,f6581,f7364,f9789,f11898,f21996,f22000,f26481,f27205,f27240,f29174,f29764])).
% 130.54/19.30 % SZS output end CNFRefutation for theBenchmark.p
% 60.38/19.38 % Elapsed time: 19.010015 seconds
% 60.38/19.38 % CPU time: 150.375880 seconds
% 60.38/19.38 % Total memory used: 653.226 MB
% 60.38/19.38 % Net memory used: 619.790 MB
%------------------------------------------------------------------------------