%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GRP113-1 : TPTP v9.3.1. Released v1.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n011.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 12:35:39 PM UTC 2026
% Result : Unsatisfiable 2.51s 0.78s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GRP113-1 : TPTP v9.3.1. Released v1.1.0.
% 0.00/0.03 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.07/0.34 % Computer : n011.cluster.edu
% 0.07/0.34 % Model : x86_64 x86_64
% 0.07/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.34 % Memory : 8046.5625MB
% 0.07/0.34 % OS : Linux 6.8.0-71-generic
% 0.07/0.34 % CPULimit : 300
% 0.07/0.34 % WCLimit : 300
% 0.07/0.34 % DateTime : Sun Sep 20 19:58:09 UTC 2026
% 0.07/0.35 % CPUTime :
% 0.12/0.36 % Drodi V4.1.1
% 2.51/0.78 % Refutation found
% 2.51/0.78 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 2.51/0.78 % SZS output start CNFRefutation for theBenchmark
% 2.51/0.78 fof(f1,axiom,(
% 2.51/0.78 (![X]: (multiply(identity,X) = X ))),
% 2.51/0.78 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.51/0.78 fof(f2,axiom,(
% 2.51/0.78 (![X]: (multiply(inverse(X),X) = identity ))),
% 2.51/0.78 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.51/0.78 fof(f3,axiom,(
% 2.51/0.78 (![X,Y,Z]: (multiply(multiply(X,Y),Z) = multiply(X,multiply(Y,Z)) ))),
% 2.51/0.78 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.51/0.78 fof(f4,axiom,(
% 2.51/0.78 (![X]: (multiply(X,identity) = X ))),
% 2.51/0.78 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.51/0.78 fof(f5,axiom,(
% 2.51/0.78 (![X]: (multiply(X,inverse(X)) = identity ))),
% 2.51/0.78 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.51/0.78 fof(f6,hypothesis,(
% 2.51/0.78 (![X]: (( X = a| X = b| X = c| X = identity ) ))),
% 2.51/0.78 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.51/0.78 fof(f7,hypothesis,(
% 2.51/0.78 a != b ),
% 2.51/0.78 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.51/0.78 fof(f8,hypothesis,(
% 2.51/0.78 a != c ),
% 2.51/0.78 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.51/0.78 fof(f9,hypothesis,(
% 2.51/0.78 a != identity ),
% 2.51/0.78 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.51/0.78 fof(f10,hypothesis,(
% 2.51/0.78 b != c ),
% 2.51/0.78 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.51/0.78 fof(f11,hypothesis,(
% 2.51/0.78 b != identity ),
% 2.51/0.78 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.51/0.78 fof(f12,hypothesis,(
% 2.51/0.78 c != identity ),
% 2.51/0.78 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.51/0.78 fof(f13,negated_conjecture,(
% 2.51/0.78 ( multiply(a,a) != identity| multiply(b,b) != identity| multiply(c,c) != identity ) ),
% 2.51/0.78 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.51/0.78 fof(f14,negated_conjecture,(
% 2.51/0.78 ( multiply(a,a) != b| multiply(a,multiply(a,a)) != c| multiply(a,multiply(a,multiply(a,a))) != identity ) ),
% 2.51/0.78 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.51/0.78 fof(f15,negated_conjecture,(
% 2.51/0.78 ( multiply(b,b) != c| multiply(b,multiply(b,b)) != a| multiply(b,multiply(b,multiply(b,b))) != identity ) ),
% 2.51/0.78 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.51/0.78 fof(f16,negated_conjecture,(
% 2.51/0.78 ( multiply(c,c) != a| multiply(c,multiply(c,c)) != b| multiply(c,multiply(c,multiply(c,c))) != identity ) ),
% 2.51/0.78 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 2.51/0.78 fof(f17,plain,(
% 2.51/0.78 ![X0]: (multiply(identity,X0)=X0)),
% 2.51/0.78 inference(cnf_transformation,[status(thm)],[f1])).
% 2.51/0.78 fof(f18,plain,(
% 2.51/0.78 ![X0]: (multiply(inverse(X0),X0)=identity)),
% 2.51/0.78 inference(cnf_transformation,[status(thm)],[f2])).
% 2.51/0.78 fof(f19,plain,(
% 2.51/0.78 ![X0,X1,X2]: (multiply(multiply(X0,X1),X2)=multiply(X0,multiply(X1,X2)))),
% 2.51/0.78 inference(cnf_transformation,[status(thm)],[f3])).
% 2.51/0.78 fof(f20,plain,(
% 2.51/0.78 ![X0]: (multiply(X0,identity)=X0)),
% 2.51/0.78 inference(cnf_transformation,[status(thm)],[f4])).
% 2.51/0.78 fof(f21,plain,(
% 2.51/0.78 ![X0]: (multiply(X0,inverse(X0))=identity)),
% 2.51/0.78 inference(cnf_transformation,[status(thm)],[f5])).
% 2.51/0.78 fof(f22,plain,(
% 2.51/0.78 ![X0]: (X0=a|X0=b|X0=c|X0=identity)),
% 2.51/0.78 inference(cnf_transformation,[status(thm)],[f6])).
% 2.51/0.78 fof(f23,plain,(
% 2.51/0.78 ~a=b),
% 2.51/0.78 inference(cnf_transformation,[status(thm)],[f7])).
% 2.51/0.78 fof(f24,plain,(
% 2.51/0.78 ~a=c),
% 2.51/0.78 inference(cnf_transformation,[status(thm)],[f8])).
% 2.51/0.78 fof(f25,plain,(
% 2.51/0.78 ~a=identity),
% 2.51/0.78 inference(cnf_transformation,[status(thm)],[f9])).
% 2.51/0.78 fof(f26,plain,(
% 2.51/0.78 ~b=c),
% 2.51/0.78 inference(cnf_transformation,[status(thm)],[f10])).
% 2.51/0.78 fof(f27,plain,(
% 2.51/0.78 ~b=identity),
% 2.51/0.78 inference(cnf_transformation,[status(thm)],[f11])).
% 2.51/0.78 fof(f28,plain,(
% 2.51/0.78 ~c=identity),
% 2.51/0.78 inference(cnf_transformation,[status(thm)],[f12])).
% 2.51/0.78 fof(f29,plain,(
% 2.51/0.78 ~multiply(a,a)=identity|~multiply(b,b)=identity|~multiply(c,c)=identity),
% 2.51/0.78 inference(cnf_transformation,[status(thm)],[f13])).
% 2.51/0.78 fof(f30,plain,(
% 2.51/0.78 ~multiply(a,a)=b|~multiply(a,multiply(a,a))=c|~multiply(a,multiply(a,multiply(a,a)))=identity),
% 2.51/0.78 inference(cnf_transformation,[status(thm)],[f14])).
% 2.51/0.78 fof(f31,plain,(
% 2.51/0.78 ~multiply(b,b)=c|~multiply(b,multiply(b,b))=a|~multiply(b,multiply(b,multiply(b,b)))=identity),
% 2.51/0.78 inference(cnf_transformation,[status(thm)],[f15])).
% 2.51/0.78 fof(f32,plain,(
% 2.51/0.78 ~multiply(c,c)=a|~multiply(c,multiply(c,c))=b|~multiply(c,multiply(c,multiply(c,c)))=identity),
% 2.51/0.78 inference(cnf_transformation,[status(thm)],[f16])).
% 2.51/0.78 fof(f33,definition,(
% 2.51/0.78 sQ0_spl <=> (multiply(a,a)=identity)),
% 2.51/0.78 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 2.51/0.78 fof(f34,plain,(
% 2.51/0.78 multiply(a,a)=identity|~sQ0_spl),
% 2.51/0.78 inference(component_clause,[status(thm)],[f33])).
% 2.51/0.78 fof(f36,definition,(
% 2.51/0.78 sQ1_spl <=> (multiply(b,b)=identity)),
% 2.51/0.78 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 2.51/0.78 fof(f37,plain,(
% 2.51/0.78 multiply(b,b)=identity|~sQ1_spl),
% 2.51/0.78 inference(component_clause,[status(thm)],[f36])).
% 2.51/0.78 fof(f39,definition,(
% 2.51/0.78 sQ2_spl <=> (multiply(c,c)=identity)),
% 2.51/0.78 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 2.51/0.78 fof(f40,plain,(
% 2.51/0.78 multiply(c,c)=identity|~sQ2_spl),
% 2.51/0.78 inference(component_clause,[status(thm)],[f39])).
% 2.51/0.78 fof(f41,plain,(
% 2.51/0.78 ~multiply(c,c)=identity|sQ2_spl),
% 2.51/0.78 inference(component_clause,[status(thm)],[f39])).
% 2.51/0.78 fof(f42,plain,(
% 2.51/0.78 ~sQ0_spl|~sQ1_spl|~sQ2_spl),
% 2.51/0.78 inference(split_clause,[status(thm)],[f29,f33,f36,f39])).
% 2.51/0.78 fof(f43,definition,(
% 2.51/0.78 sQ3_spl <=> (multiply(a,a)=b)),
% 2.51/0.78 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 2.51/0.78 fof(f44,plain,(
% 2.51/0.78 multiply(a,a)=b|~sQ3_spl),
% 2.51/0.78 inference(component_clause,[status(thm)],[f43])).
% 2.51/0.78 fof(f45,plain,(
% 2.51/0.78 ~multiply(a,a)=b|sQ3_spl),
% 2.51/0.78 inference(component_clause,[status(thm)],[f43])).
% 2.51/0.78 fof(f46,definition,(
% 2.51/0.78 sQ4_spl <=> (multiply(a,multiply(a,a))=c)),
% 2.51/0.78 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 2.51/0.78 fof(f47,plain,(
% 2.51/0.78 multiply(a,multiply(a,a))=c|~sQ4_spl),
% 2.51/0.78 inference(component_clause,[status(thm)],[f46])).
% 2.51/0.78 fof(f48,plain,(
% 2.51/0.78 ~multiply(a,multiply(a,a))=c|sQ4_spl),
% 2.51/0.78 inference(component_clause,[status(thm)],[f46])).
% 2.51/0.78 fof(f49,definition,(
% 2.51/0.78 sQ5_spl <=> (multiply(a,multiply(a,multiply(a,a)))=identity)),
% 2.51/0.78 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 2.51/0.78 fof(f50,plain,(
% 2.51/0.78 multiply(a,multiply(a,multiply(a,a)))=identity|~sQ5_spl),
% 2.51/0.78 inference(component_clause,[status(thm)],[f49])).
% 2.51/0.78 fof(f51,plain,(
% 2.51/0.78 ~multiply(a,multiply(a,multiply(a,a)))=identity|sQ5_spl),
% 2.51/0.78 inference(component_clause,[status(thm)],[f49])).
% 2.51/0.78 fof(f52,plain,(
% 2.51/0.78 ~sQ3_spl|~sQ4_spl|~sQ5_spl),
% 2.51/0.78 inference(split_clause,[status(thm)],[f30,f43,f46,f49])).
% 2.51/0.78 fof(f53,definition,(
% 2.51/0.78 sQ6_spl <=> (multiply(b,b)=c)),
% 2.51/0.78 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 2.51/0.78 fof(f54,plain,(
% 2.51/0.78 multiply(b,b)=c|~sQ6_spl),
% 2.51/0.78 inference(component_clause,[status(thm)],[f53])).
% 2.51/0.78 fof(f55,plain,(
% 2.51/0.78 ~multiply(b,b)=c|sQ6_spl),
% 2.51/0.78 inference(component_clause,[status(thm)],[f53])).
% 2.51/0.78 fof(f56,definition,(
% 2.51/0.78 sQ7_spl <=> (multiply(b,multiply(b,b))=a)),
% 2.51/0.78 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 2.51/0.78 fof(f57,plain,(
% 2.51/0.78 multiply(b,multiply(b,b))=a|~sQ7_spl),
% 2.51/0.78 inference(component_clause,[status(thm)],[f56])).
% 2.51/0.78 fof(f58,plain,(
% 2.51/0.78 ~multiply(b,multiply(b,b))=a|sQ7_spl),
% 2.51/0.78 inference(component_clause,[status(thm)],[f56])).
% 2.51/0.78 fof(f59,definition,(
% 2.51/0.78 sQ8_spl <=> (multiply(b,multiply(b,multiply(b,b)))=identity)),
% 2.51/0.78 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 2.51/0.78 fof(f61,plain,(
% 2.51/0.78 ~multiply(b,multiply(b,multiply(b,b)))=identity|sQ8_spl),
% 2.51/0.78 inference(component_clause,[status(thm)],[f59])).
% 2.51/0.78 fof(f62,plain,(
% 2.51/0.78 ~sQ6_spl|~sQ7_spl|~sQ8_spl),
% 2.51/0.78 inference(split_clause,[status(thm)],[f31,f53,f56,f59])).
% 2.51/0.78 fof(f63,definition,(
% 2.51/0.78 sQ9_spl <=> (multiply(c,c)=a)),
% 2.51/0.78 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 2.51/0.78 fof(f64,plain,(
% 2.51/0.78 multiply(c,c)=a|~sQ9_spl),
% 2.51/0.78 inference(component_clause,[status(thm)],[f63])).
% 2.51/0.78 fof(f65,plain,(
% 2.51/0.78 ~multiply(c,c)=a|sQ9_spl),
% 2.51/0.78 inference(component_clause,[status(thm)],[f63])).
% 2.51/0.78 fof(f66,definition,(
% 2.51/0.78 sQ10_spl <=> (multiply(c,multiply(c,c))=b)),
% 2.51/0.78 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 2.51/0.78 fof(f67,plain,(
% 2.51/0.78 multiply(c,multiply(c,c))=b|~sQ10_spl),
% 2.51/0.78 inference(component_clause,[status(thm)],[f66])).
% 2.51/0.78 fof(f68,plain,(
% 2.51/0.78 ~multiply(c,multiply(c,c))=b|sQ10_spl),
% 2.51/0.78 inference(component_clause,[status(thm)],[f66])).
% 2.51/0.78 fof(f69,definition,(
% 2.51/0.78 sQ11_spl <=> (multiply(c,multiply(c,multiply(c,c)))=identity)),
% 2.51/0.78 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 2.51/0.78 fof(f71,plain,(
% 2.51/0.78 ~multiply(c,multiply(c,multiply(c,c)))=identity|sQ11_spl),
% 2.51/0.78 inference(component_clause,[status(thm)],[f69])).
% 2.51/0.78 fof(f72,plain,(
% 2.51/0.78 ~sQ9_spl|~sQ10_spl|~sQ11_spl),
% 2.51/0.78 inference(split_clause,[status(thm)],[f32,f63,f66,f69])).
% 2.51/0.78 fof(f82,plain,(
% 2.51/0.78 b=a|b=b|b=identity),
% 2.51/0.78 inference(resolution,[status(thm)],[f22,f26])).
% 2.51/0.78 fof(f83,plain,(
% 2.51/0.78 a=a|a=b|a=identity),
% 2.51/0.78 inference(resolution,[status(thm)],[f22,f24])).
% 2.51/0.78 fof(f84,plain,(
% 2.51/0.78 multiply(b,b)=a|multiply(b,b)=b|multiply(b,b)=identity|sQ6_spl),
% 2.51/0.78 inference(resolution,[status(thm)],[f22,f55])).
% 2.51/0.78 fof(f85,plain,(
% 2.51/0.78 identity=a|identity=b|identity=identity),
% 2.51/0.78 inference(resolution,[status(thm)],[f22,f28])).
% 2.51/0.78 fof(f86,plain,(
% 2.51/0.78 ![X0,X1]: (X0=a|X0=b|X0=X1|X0=identity|X1=a|X1=b|X1=identity)),
% 2.51/0.78 inference(paramodulation,[status(thm)],[f22,f22])).
% 2.51/0.78 fof(f94,plain,(
% 2.51/0.78 ![X0]: (~multiply(c,X0)=identity|X0=a|X0=b|X0=identity|sQ2_spl)),
% 2.51/0.78 inference(paramodulation,[status(thm)],[f22,f41])).
% 2.51/0.78 fof(f95,plain,(
% 2.51/0.78 ![X0]: (~multiply(X0,c)=identity|X0=a|X0=b|X0=identity|sQ2_spl)),
% 2.51/0.78 inference(paramodulation,[status(thm)],[f22,f41])).
% 2.51/0.78 fof(f96,plain,(
% 2.51/0.78 ![X0]: (~multiply(c,X0)=a|X0=a|X0=b|X0=identity|sQ9_spl)),
% 2.51/0.78 inference(paramodulation,[status(thm)],[f22,f65])).
% 2.51/0.78 fof(f97,plain,(
% 2.51/0.78 ![X0]: (~multiply(X0,c)=a|X0=a|X0=b|X0=identity|sQ9_spl)),
% 2.51/0.78 inference(paramodulation,[status(thm)],[f22,f65])).
% 2.51/0.78 fof(f98,plain,(
% 2.51/0.78 ![X0]: (X0=b|X0=identity|~c=a|X0=a)),
% 2.51/0.78 inference(equality_factoring,[status(thm)],[f22])).
% 2.51/0.78 fof(f99,plain,(
% 2.51/0.78 ![X0]: (X0=a|X0=identity|~c=b|X0=b)),
% 2.51/0.78 inference(equality_factoring,[status(thm)],[f22])).
% 2.51/0.78 fof(f101,definition,(
% 2.51/0.78 sQ12_spl <=> (b=a)),
% 2.51/0.78 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 2.51/0.78 fof(f102,plain,(
% 2.51/0.78 b=a|~sQ12_spl),
% 2.51/0.78 inference(component_clause,[status(thm)],[f101])).
% 2.51/0.78 fof(f104,definition,(
% 2.51/0.78 sQ13_spl <=> (b=b)),
% 2.51/0.78 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 2.51/0.78 fof(f107,definition,(
% 2.51/0.78 sQ14_spl <=> (b=identity)),
% 2.51/0.78 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 2.51/0.78 fof(f108,plain,(
% 2.51/0.78 b=identity|~sQ14_spl),
% 2.51/0.78 inference(component_clause,[status(thm)],[f107])).
% 2.51/0.78 fof(f110,plain,(
% 2.51/0.78 sQ12_spl|sQ13_spl|sQ14_spl),
% 2.51/0.78 inference(split_clause,[status(thm)],[f82,f101,f104,f107])).
% 2.51/0.78 fof(f111,definition,(
% 2.51/0.78 sQ15_spl <=> (a=a)),
% 2.51/0.78 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 2.51/0.78 fof(f114,definition,(
% 2.51/0.78 sQ16_spl <=> (a=identity)),
% 2.51/0.78 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 2.51/0.78 fof(f115,plain,(
% 2.51/0.78 a=identity|~sQ16_spl),
% 2.51/0.78 inference(component_clause,[status(thm)],[f114])).
% 2.51/0.78 fof(f117,plain,(
% 2.51/0.78 sQ15_spl|sQ12_spl|sQ16_spl),
% 2.51/0.78 inference(split_clause,[status(thm)],[f83,f111,f101,f114])).
% 2.51/0.78 fof(f118,definition,(
% 2.51/0.78 sQ17_spl <=> (multiply(b,b)=a)),
% 2.51/0.78 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 2.51/0.78 fof(f119,plain,(
% 2.51/0.78 multiply(b,b)=a|~sQ17_spl),
% 2.51/0.78 inference(component_clause,[status(thm)],[f118])).
% 2.51/0.78 fof(f121,definition,(
% 2.51/0.78 sQ18_spl <=> (multiply(b,b)=b)),
% 2.51/0.78 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 2.51/0.78 fof(f122,plain,(
% 2.51/0.78 multiply(b,b)=b|~sQ18_spl),
% 2.51/0.78 inference(component_clause,[status(thm)],[f121])).
% 2.51/0.78 fof(f124,plain,(
% 2.51/0.78 sQ17_spl|sQ18_spl|sQ1_spl|sQ6_spl),
% 2.51/0.78 inference(split_clause,[status(thm)],[f84,f118,f121,f36,f53])).
% 2.51/0.78 fof(f125,definition,(
% 2.51/0.78 sQ19_spl <=> (identity=identity)),
% 2.51/0.78 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 2.51/0.78 fof(f128,plain,(
% 2.51/0.78 sQ16_spl|sQ14_spl|sQ19_spl),
% 2.51/0.78 inference(split_clause,[status(thm)],[f85,f114,f107,f125])).
% 2.51/0.78 fof(f129,definition,(
% 2.51/0.78 ![X0]: (sQ20_spl <=> (X0=b|X0=identity|X0=a))),
% 2.51/0.78 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 2.51/0.78 fof(f130,plain,(
% 2.51/0.78 ![X0]: (X0=b|X0=identity|X0=a|~sQ20_spl)),
% 2.51/0.78 inference(component_clause,[status(thm)],[f129])).
% 2.51/0.78 fof(f132,definition,(
% 2.51/0.78 sQ21_spl <=> (c=a)),
% 2.51/0.78 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 2.51/0.78 fof(f135,plain,(
% 2.51/0.78 sQ20_spl|~sQ21_spl),
% 2.51/0.78 inference(split_clause,[status(thm)],[f98,f129,f132])).
% 2.51/0.78 fof(f136,definition,(
% 2.51/0.78 sQ22_spl <=> (c=b)),
% 2.51/0.78 introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition])).
% 2.51/0.78 fof(f139,plain,(
% 2.51/0.78 sQ20_spl|~sQ22_spl),
% 2.51/0.78 inference(split_clause,[status(thm)],[f99,f129,f136])).
% 2.51/0.78 fof(f140,definition,(
% 2.51/0.78 sQ23_spl <=> (c=identity)),
% 2.51/0.78 introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition])).
% 2.51/0.78 fof(f141,plain,(
% 2.51/0.78 c=identity|~sQ23_spl),
% 2.51/0.78 inference(component_clause,[status(thm)],[f140])).
% 2.51/0.78 fof(f144,plain,(
% 2.51/0.78 $false|~sQ14_spl),
% 2.51/0.78 inference(forward_subsumption_resolution,[status(thm)],[f108,f27])).
% 2.51/0.78 fof(f145,plain,(
% 2.51/0.78 ~sQ14_spl),
% 2.51/0.78 inference(contradiction_clause,[status(thm)],[f144])).
% 2.51/0.78 fof(f146,plain,(
% 2.51/0.78 $false|~sQ16_spl),
% 2.51/0.78 inference(forward_subsumption_resolution,[status(thm)],[f115,f25])).
% 2.51/0.78 fof(f147,plain,(
% 2.51/0.78 ~sQ16_spl),
% 2.51/0.78 inference(contradiction_clause,[status(thm)],[f146])).
% 2.51/0.78 fof(f148,plain,(
% 2.51/0.78 $false|~sQ12_spl),
% 2.51/0.78 inference(forward_subsumption_resolution,[status(thm)],[f102,f23])).
% 2.51/0.78 fof(f149,plain,(
% 2.51/0.78 ~sQ12_spl),
% 2.51/0.78 inference(contradiction_clause,[status(thm)],[f148])).
% 2.51/0.78 fof(f162,plain,(
% 2.51/0.78 ~multiply(b,a)=a|~sQ17_spl|sQ7_spl),
% 2.51/0.78 inference(backward_demodulation,[status(thm)],[f119,f58])).
% 2.51/0.78 fof(f163,plain,(
% 2.51/0.78 inverse(identity)=identity),
% 2.51/0.78 inference(paramodulation,[status(thm)],[f20,f18])).
% 2.51/0.78 fof(f165,plain,(
% 2.51/0.78 ![X0,X1]: (multiply(identity,X0)=multiply(inverse(X1),multiply(X1,X0)))),
% 2.51/0.78 inference(paramodulation,[status(thm)],[f18,f19])).
% 2.51/0.78 fof(f166,plain,(
% 2.51/0.78 ![X0,X1]: (X0=multiply(inverse(X1),multiply(X1,X0)))),
% 2.51/0.78 inference(forward_demodulation,[status(thm)],[f17,f165])).
% 2.51/0.78 fof(f168,plain,(
% 2.51/0.78 ![X0,X1]: (multiply(X0,multiply(X1,inverse(multiply(X0,X1))))=identity)),
% 2.51/0.78 inference(paramodulation,[status(thm)],[f19,f21])).
% 2.51/0.78 fof(f173,plain,(
% 2.51/0.78 ![X0,X1]: (multiply(identity,X0)=multiply(X1,multiply(inverse(X1),X0)))),
% 2.51/0.78 inference(paramodulation,[status(thm)],[f21,f19])).
% 2.51/0.78 fof(f174,plain,(
% 2.51/0.78 ![X0,X1]: (X0=multiply(X1,multiply(inverse(X1),X0)))),
% 2.51/0.78 inference(forward_demodulation,[status(thm)],[f17,f173])).
% 2.51/0.78 fof(f178,plain,(
% 2.51/0.78 multiply(a,a)=identity|multiply(a,a)=a|~sQ20_spl|sQ3_spl),
% 2.51/0.78 inference(resolution,[status(thm)],[f130,f45])).
% 2.51/0.78 fof(f180,plain,(
% 2.51/0.78 c=identity|c=a|~sQ20_spl),
% 2.51/0.78 inference(resolution,[status(thm)],[f130,f26])).
% 2.51/0.78 fof(f190,definition,(
% 2.51/0.78 sQ24_spl <=> (multiply(a,a)=a)),
% 2.51/0.78 introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition])).
% 2.51/0.78 fof(f191,plain,(
% 2.51/0.78 multiply(a,a)=a|~sQ24_spl),
% 2.51/0.78 inference(component_clause,[status(thm)],[f190])).
% 2.51/0.78 fof(f192,plain,(
% 2.51/0.78 ~multiply(a,a)=a|sQ24_spl),
% 2.51/0.78 inference(component_clause,[status(thm)],[f190])).
% 2.51/0.78 fof(f193,plain,(
% 2.51/0.78 sQ0_spl|sQ24_spl|~sQ20_spl|sQ3_spl),
% 2.51/0.78 inference(split_clause,[status(thm)],[f178,f33,f190,f129,f43])).
% 2.51/0.78 fof(f195,plain,(
% 2.51/0.78 sQ23_spl|sQ21_spl|~sQ20_spl),
% 2.51/0.78 inference(split_clause,[status(thm)],[f180,f140,f132,f129])).
% 2.51/0.78 fof(f196,definition,(
% 2.51/0.78 ![X0]: (sQ25_spl <=> (X0=a|X0=identity))),
% 2.51/0.78 introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 2.51/0.78 fof(f197,plain,(
% 2.51/0.78 ![X0]: (X0=a|X0=identity|~sQ25_spl)),
% 2.51/0.78 inference(component_clause,[status(thm)],[f196])).
% 2.51/0.78 fof(f203,plain,(
% 2.51/0.78 $false|~sQ23_spl),
% 2.51/0.78 inference(forward_subsumption_resolution,[status(thm)],[f141,f28])).
% 2.51/0.78 fof(f204,plain,(
% 2.51/0.78 ~sQ23_spl),
% 2.51/0.78 inference(contradiction_clause,[status(thm)],[f203])).
% 2.51/0.78 fof(f222,plain,(
% 2.51/0.78 b=identity|~sQ25_spl),
% 2.51/0.78 inference(resolution,[status(thm)],[f197,f23])).
% 2.51/0.78 fof(f229,plain,(
% 2.51/0.78 sQ14_spl|~sQ25_spl),
% 2.51/0.78 inference(split_clause,[status(thm)],[f222,f107,f196])).
% 2.51/0.78 fof(f234,plain,(
% 2.51/0.78 ~multiply(c,multiply(c,identity))=identity|~sQ2_spl|sQ11_spl),
% 2.51/0.78 inference(backward_demodulation,[status(thm)],[f40,f71])).
% 2.51/0.78 fof(f236,plain,(
% 2.51/0.78 ~multiply(c,c)=identity|~sQ2_spl|sQ11_spl),
% 2.51/0.78 inference(forward_demodulation,[status(thm)],[f20,f234])).
% 2.51/0.78 fof(f237,plain,(
% 2.51/0.78 ~identity=identity|~sQ2_spl|sQ11_spl),
% 2.51/0.78 inference(forward_demodulation,[status(thm)],[f40,f236])).
% 2.51/0.78 fof(f238,plain,(
% 2.51/0.78 $false|~sQ2_spl|sQ11_spl),
% 2.51/0.78 inference(trivial_equality_resolution,[status(thm)],[f237])).
% 2.51/0.78 fof(f239,plain,(
% 2.51/0.78 ~sQ2_spl|sQ11_spl),
% 2.51/0.78 inference(contradiction_clause,[status(thm)],[f238])).
% 2.51/0.78 fof(f240,plain,(
% 2.51/0.78 ![X0]: (multiply(identity,X0)=multiply(b,multiply(b,X0))|~sQ1_spl)),
% 2.51/0.78 inference(paramodulation,[status(thm)],[f37,f19])).
% 2.51/0.78 fof(f241,plain,(
% 2.51/0.78 ![X0]: (X0=multiply(b,multiply(b,X0))|~sQ1_spl)),
% 2.51/0.78 inference(forward_demodulation,[status(thm)],[f17,f240])).
% 2.51/0.78 fof(f242,plain,(
% 2.51/0.78 multiply(a,multiply(a,a))=a|multiply(a,multiply(a,a))=b|multiply(a,multiply(a,a))=identity|sQ4_spl),
% 2.51/0.78 inference(resolution,[status(thm)],[f22,f48])).
% 2.51/0.78 fof(f255,definition,(
% 2.51/0.78 sQ27_spl <=> (multiply(a,multiply(a,a))=a)),
% 2.51/0.78 introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition])).
% 2.51/0.78 fof(f256,plain,(
% 2.51/0.78 multiply(a,multiply(a,a))=a|~sQ27_spl),
% 2.51/0.78 inference(component_clause,[status(thm)],[f255])).
% 2.51/0.78 fof(f258,definition,(
% 2.51/0.78 sQ28_spl <=> (multiply(a,multiply(a,a))=b)),
% 2.51/0.78 introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition])).
% 2.51/0.78 fof(f259,plain,(
% 2.51/0.78 multiply(a,multiply(a,a))=b|~sQ28_spl),
% 2.51/0.78 inference(component_clause,[status(thm)],[f258])).
% 2.51/0.78 fof(f261,definition,(
% 2.51/0.78 sQ29_spl <=> (multiply(a,multiply(a,a))=identity)),
% 2.51/0.78 introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition])).
% 2.51/0.78 fof(f262,plain,(
% 2.51/0.78 multiply(a,multiply(a,a))=identity|~sQ29_spl),
% 2.51/0.78 inference(component_clause,[status(thm)],[f261])).
% 2.51/0.78 fof(f263,plain,(
% 2.51/0.78 ~multiply(a,multiply(a,a))=identity|sQ29_spl),
% 2.51/0.78 inference(component_clause,[status(thm)],[f261])).
% 2.51/0.78 fof(f264,plain,(
% 2.51/0.78 sQ27_spl|sQ28_spl|sQ29_spl|sQ4_spl),
% 2.51/0.78 inference(split_clause,[status(thm)],[f242,f255,f258,f261,f46])).
% 2.51/0.78 fof(f272,plain,(
% 2.51/0.78 identity=b|~sQ29_spl|~sQ28_spl),
% 2.51/0.78 inference(forward_demodulation,[status(thm)],[f262,f259])).
% 2.51/0.78 fof(f273,plain,(
% 2.51/0.78 $false|~sQ29_spl|~sQ28_spl),
% 2.51/0.78 inference(forward_subsumption_resolution,[status(thm)],[f272,f27])).
% 2.51/0.78 fof(f274,plain,(
% 2.51/0.78 ~sQ29_spl|~sQ28_spl),
% 2.51/0.78 inference(contradiction_clause,[status(thm)],[f273])).
% 2.51/0.78 fof(f281,plain,(
% 2.51/0.78 inverse(b)=multiply(b,identity)|~sQ1_spl),
% 2.51/0.78 inference(paramodulation,[status(thm)],[f21,f241])).
% 2.51/0.78 fof(f287,plain,(
% 2.51/0.78 inverse(b)=b|~sQ1_spl),
% 2.51/0.78 inference(forward_demodulation,[status(thm)],[f20,f281])).
% 2.51/0.78 fof(f292,definition,(
% 2.51/0.78 sQ30_spl <=> (inverse(b)=a)),
% 2.51/0.78 introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition])).
% 2.51/0.78 fof(f293,plain,(
% 2.51/0.78 inverse(b)=a|~sQ30_spl),
% 2.51/0.78 inference(component_clause,[status(thm)],[f292])).
% 2.51/0.78 fof(f294,plain,(
% 2.51/0.78 ~inverse(b)=a|sQ30_spl),
% 2.51/0.78 inference(component_clause,[status(thm)],[f292])).
% 2.51/0.78 fof(f295,definition,(
% 2.51/0.78 sQ31_spl <=> (inverse(b)=b)),
% 2.51/0.78 introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition])).
% 2.51/0.78 fof(f296,plain,(
% 2.51/0.78 inverse(b)=b|~sQ31_spl),
% 2.51/0.78 inference(component_clause,[status(thm)],[f295])).
% 2.51/0.78 fof(f298,definition,(
% 2.51/0.78 sQ32_spl <=> (inverse(b)=identity)),
% 2.51/0.78 introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition])).
% 2.51/0.78 fof(f299,plain,(
% 2.51/0.78 inverse(b)=identity|~sQ32_spl),
% 2.51/0.78 inference(component_clause,[status(thm)],[f298])).
% 2.51/0.78 fof(f312,plain,(
% 2.51/0.78 multiply(b,a)=identity|~sQ30_spl),
% 2.51/0.78 inference(paramodulation,[status(thm)],[f293,f21])).
% 2.51/0.78 fof(f313,plain,(
% 2.51/0.78 multiply(a,b)=identity|~sQ30_spl),
% 2.51/0.78 inference(paramodulation,[status(thm)],[f293,f18])).
% 2.51/0.78 fof(f322,plain,(
% 2.51/0.78 ![X0]: (~multiply(c,multiply(c,X0))=b|X0=a|X0=b|X0=identity|sQ10_spl)),
% 2.51/0.78 inference(paramodulation,[status(thm)],[f22,f68])).
% 2.51/0.78 fof(f323,definition,(
% 2.51/0.78 sQ33_spl <=> (multiply(c,multiply(c,c))=a)),
% 2.51/0.78 introduced(definition,[new_symbols(definition,[sQ33_spl])],[split_symbol_definition])).
% 2.51/0.78 fof(f324,plain,(
% 2.51/0.78 multiply(c,multiply(c,c))=a|~sQ33_spl),
% 2.51/0.78 inference(component_clause,[status(thm)],[f323])).
% 2.51/0.78 fof(f326,definition,(
% 2.51/0.78 sQ34_spl <=> (multiply(c,multiply(c,c))=identity)),
% 2.51/0.78 introduced(definition,[new_symbols(definition,[sQ34_spl])],[split_symbol_definition])).
% 2.51/0.78 fof(f327,plain,(
% 2.51/0.78 multiply(c,multiply(c,c))=identity|~sQ34_spl),
% 2.51/0.78 inference(component_clause,[status(thm)],[f326])).
% 2.51/0.78 fof(f328,plain,(
% 2.51/0.78 ~multiply(c,multiply(c,c))=identity|sQ34_spl),
% 2.51/0.78 inference(component_clause,[status(thm)],[f326])).
% 2.51/0.78 fof(f330,definition,(
% 2.51/0.78 sQ35_spl <=> (multiply(c,c)=b)),
% 2.51/0.78 introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition])).
% 2.51/0.78 fof(f331,plain,(
% 2.51/0.78 multiply(c,c)=b|~sQ35_spl),
% 2.51/0.78 inference(component_clause,[status(thm)],[f330])).
% 2.51/0.78 fof(f332,plain,(
% 2.51/0.78 ~multiply(c,c)=b|sQ35_spl),
% 2.51/0.78 inference(component_clause,[status(thm)],[f330])).
% 2.51/0.78 fof(f334,plain,(
% 2.51/0.78 identity=a|~sQ34_spl|~sQ33_spl),
% 2.51/0.78 inference(forward_demodulation,[status(thm)],[f327,f324])).
% 2.51/0.78 fof(f335,plain,(
% 2.51/0.78 $false|~sQ34_spl|~sQ33_spl),
% 2.51/0.78 inference(forward_subsumption_resolution,[status(thm)],[f334,f25])).
% 2.51/0.78 fof(f336,plain,(
% 2.51/0.78 ~sQ34_spl|~sQ33_spl),
% 2.51/0.78 inference(contradiction_clause,[status(thm)],[f335])).
% 2.51/0.78 fof(f342,definition,(
% 2.51/0.78 sQ36_spl <=> (multiply(b,a)=a)),
% 2.51/0.78 introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition])).
% 2.51/0.78 fof(f343,plain,(
% 2.51/0.78 multiply(b,a)=a|~sQ36_spl),
% 2.51/0.78 inference(component_clause,[status(thm)],[f342])).
% 2.51/0.78 fof(f344,plain,(
% 2.51/0.78 ~multiply(b,a)=a|sQ36_spl),
% 2.51/0.78 inference(component_clause,[status(thm)],[f342])).
% 2.51/0.78 fof(f345,definition,(
% 2.51/0.78 sQ37_spl <=> (multiply(b,a)=b)),
% 2.51/0.78 introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition])).
% 2.51/0.78 fof(f346,plain,(
% 2.51/0.78 multiply(b,a)=b|~sQ37_spl),
% 2.51/0.78 inference(component_clause,[status(thm)],[f345])).
% 2.51/0.78 fof(f347,plain,(
% 2.51/0.78 ~multiply(b,a)=b|sQ37_spl),
% 2.51/0.78 inference(component_clause,[status(thm)],[f345])).
% 2.51/0.78 fof(f348,definition,(
% 2.51/0.78 sQ38_spl <=> (multiply(b,a)=identity)),
% 2.51/0.78 introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition])).
% 2.51/0.78 fof(f349,plain,(
% 2.51/0.78 multiply(b,a)=identity|~sQ38_spl),
% 2.51/0.78 inference(component_clause,[status(thm)],[f348])).
% 2.51/0.78 fof(f366,plain,(
% 2.51/0.78 a=multiply(inverse(b),a)|~sQ36_spl),
% 2.51/0.78 inference(paramodulation,[status(thm)],[f343,f166])).
% 2.51/0.78 fof(f367,plain,(
% 2.51/0.78 b=multiply(inverse(b),b)|~sQ18_spl),
% 2.51/0.78 inference(paramodulation,[status(thm)],[f122,f166])).
% 2.51/0.78 fof(f369,plain,(
% 2.51/0.78 ![X0]: (X0=multiply(inverse(inverse(X0)),identity))),
% 2.51/0.78 inference(paramodulation,[status(thm)],[f18,f166])).
% 2.51/0.78 fof(f379,plain,(
% 2.51/0.78 b=identity|~sQ18_spl),
% 2.51/0.78 inference(forward_demodulation,[status(thm)],[f18,f367])).
% 2.51/0.78 fof(f380,plain,(
% 2.51/0.78 $false|~sQ18_spl),
% 2.51/0.78 inference(forward_subsumption_resolution,[status(thm)],[f379,f27])).
% 2.51/0.78 fof(f381,plain,(
% 2.51/0.78 ~sQ18_spl),
% 2.51/0.78 inference(contradiction_clause,[status(thm)],[f380])).
% 2.51/0.78 fof(f383,plain,(
% 2.51/0.78 ![X0]: (X0=inverse(inverse(X0)))),
% 2.51/0.78 inference(forward_demodulation,[status(thm)],[f20,f369])).
% 2.51/0.78 fof(f391,plain,(
% 2.51/0.78 a=b|~sQ30_spl|~sQ1_spl),
% 2.51/0.78 inference(backward_demodulation,[status(thm)],[f293,f287])).
% 2.51/0.78 fof(f392,plain,(
% 2.51/0.78 sQ38_spl|~sQ30_spl),
% 2.51/0.78 inference(split_clause,[status(thm)],[f312,f348,f292])).
% 2.51/0.78 fof(f395,plain,(
% 2.51/0.78 sQ12_spl|~sQ30_spl|~sQ1_spl),
% 2.51/0.78 inference(split_clause,[status(thm)],[f391,f101,f292,f36])).
% 2.51/0.78 fof(f416,plain,(
% 2.51/0.78 ~c=a|inverse(b)=a|inverse(b)=b|inverse(b)=identity|sQ30_spl),
% 2.51/0.78 inference(paramodulation,[status(thm)],[f22,f294])).
% 2.51/0.78 fof(f417,plain,(
% 2.51/0.78 ~sQ21_spl|sQ30_spl|sQ31_spl|sQ32_spl),
% 2.51/0.78 inference(split_clause,[status(thm)],[f416,f132,f292,f295,f298])).
% 2.51/0.78 fof(f423,plain,(
% 2.51/0.78 multiply(b,b)=identity|~sQ31_spl),
% 2.51/0.78 inference(paramodulation,[status(thm)],[f296,f21])).
% 2.51/0.78 fof(f427,plain,(
% 2.51/0.78 sQ1_spl|~sQ31_spl),
% 2.51/0.78 inference(split_clause,[status(thm)],[f423,f36,f295])).
% 2.51/0.78 fof(f442,plain,(
% 2.51/0.78 b=inverse(identity)|~sQ32_spl),
% 2.51/0.78 inference(paramodulation,[status(thm)],[f299,f383])).
% 2.51/0.78 fof(f447,plain,(
% 2.51/0.78 b=identity|~sQ32_spl),
% 2.51/0.78 inference(forward_demodulation,[status(thm)],[f163,f442])).
% 2.51/0.78 fof(f448,plain,(
% 2.51/0.78 $false|~sQ32_spl),
% 2.51/0.78 inference(forward_subsumption_resolution,[status(thm)],[f447,f27])).
% 2.51/0.78 fof(f449,plain,(
% 2.51/0.78 ~sQ32_spl),
% 2.51/0.78 inference(contradiction_clause,[status(thm)],[f448])).
% 2.51/0.78 fof(f475,plain,(
% 2.51/0.78 b=multiply(inverse(b),identity)|~sQ1_spl),
% 2.51/0.78 inference(paramodulation,[status(thm)],[f37,f166])).
% 2.51/0.78 fof(f478,plain,(
% 2.51/0.78 b=inverse(b)|~sQ1_spl),
% 2.51/0.78 inference(forward_demodulation,[status(thm)],[f20,f475])).
% 2.51/0.78 fof(f483,plain,(
% 2.51/0.78 multiply(a,b)=a|~sQ3_spl|~sQ27_spl),
% 2.51/0.78 inference(backward_demodulation,[status(thm)],[f44,f256])).
% 2.51/0.78 fof(f487,plain,(
% 2.51/0.78 ![X0]: (multiply(b,X0)=multiply(a,multiply(a,X0))|~sQ3_spl)),
% 2.51/0.78 inference(paramodulation,[status(thm)],[f44,f19])).
% 2.51/0.78 fof(f490,plain,(
% 2.51/0.78 b=multiply(inverse(a),a)|~sQ3_spl|~sQ27_spl),
% 2.51/0.78 inference(paramodulation,[status(thm)],[f483,f166])).
% 2.51/0.78 fof(f492,definition,(
% 2.51/0.78 sQ39_spl <=> (multiply(a,b)=a)),
% 2.51/0.78 introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition])).
% 2.51/0.78 fof(f493,plain,(
% 2.51/0.78 multiply(a,b)=a|~sQ39_spl),
% 2.51/0.78 inference(component_clause,[status(thm)],[f492])).
% 2.51/0.78 fof(f495,definition,(
% 2.51/0.78 sQ40_spl <=> (multiply(a,b)=b)),
% 2.51/0.78 introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition])).
% 2.51/0.78 fof(f496,plain,(
% 2.51/0.78 multiply(a,b)=b|~sQ40_spl),
% 2.51/0.78 inference(component_clause,[status(thm)],[f495])).
% 2.51/0.78 fof(f498,definition,(
% 2.51/0.78 sQ41_spl <=> (multiply(a,b)=identity)),
% 2.51/0.78 introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition])).
% 2.51/0.78 fof(f499,plain,(
% 2.51/0.78 multiply(a,b)=identity|~sQ41_spl),
% 2.51/0.78 inference(component_clause,[status(thm)],[f498])).
% 2.51/0.78 fof(f500,plain,(
% 2.51/0.78 ~multiply(a,b)=identity|sQ41_spl),
% 2.51/0.78 inference(component_clause,[status(thm)],[f498])).
% 2.51/0.78 fof(f502,plain,(
% 2.51/0.78 b=identity|~sQ3_spl|~sQ27_spl),
% 2.51/0.78 inference(forward_demodulation,[status(thm)],[f18,f490])).
% 2.51/0.78 fof(f503,plain,(
% 2.51/0.78 $false|~sQ3_spl|~sQ27_spl),
% 2.51/0.78 inference(forward_subsumption_resolution,[status(thm)],[f502,f27])).
% 2.51/0.78 fof(f504,plain,(
% 2.51/0.78 ~sQ3_spl|~sQ27_spl),
% 2.51/0.78 inference(contradiction_clause,[status(thm)],[f503])).
% 2.51/0.78 fof(f514,plain,(
% 2.51/0.78 b=multiply(inverse(a),a)|~sQ39_spl),
% 2.51/0.78 inference(paramodulation,[status(thm)],[f493,f166])).
% 2.51/0.78 fof(f517,plain,(
% 2.51/0.78 b=identity|~sQ39_spl),
% 2.51/0.78 inference(forward_demodulation,[status(thm)],[f18,f514])).
% 2.51/0.78 fof(f518,plain,(
% 2.51/0.78 $false|~sQ39_spl),
% 2.51/0.78 inference(forward_subsumption_resolution,[status(thm)],[f517,f27])).
% 2.51/0.78 fof(f519,plain,(
% 2.51/0.78 ~sQ39_spl),
% 2.51/0.78 inference(contradiction_clause,[status(thm)],[f518])).
% 2.51/0.78 fof(f530,plain,(
% 2.51/0.78 ![X0,X1]: (c=identity|multiply(X0,multiply(X1,inverse(multiply(X0,X1))))=a|multiply(X0,multiply(X1,inverse(multiply(X0,X1))))=b|multiply(X0,multiply(X1,inverse(multiply(X0,X1))))=identity)),
% 2.51/0.78 inference(paramodulation,[status(thm)],[f22,f168])).
% 2.51/0.78 fof(f550,plain,(
% 2.51/0.78 ![X0,X1]: (multiply(X0,inverse(multiply(X1,X0)))=multiply(inverse(X1),identity))),
% 2.51/0.78 inference(paramodulation,[status(thm)],[f168,f166])).
% 2.51/0.78 fof(f552,definition,(
% 2.51/0.78 ![X0,X1]: (sQ42_spl <=> (multiply(X0,multiply(X1,inverse(multiply(X0,X1))))=a|multiply(X0,multiply(X1,inverse(multiply(X0,X1))))=b|multiply(X0,multiply(X1,inverse(multiply(X0,X1))))=identity))),
% 2.51/0.78 introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition])).
% 2.51/0.78 fof(f555,plain,(
% 2.51/0.78 sQ23_spl|sQ42_spl),
% 2.51/0.78 inference(split_clause,[status(thm)],[f530,f140,f552])).
% 2.51/0.78 fof(f576,plain,(
% 2.51/0.78 ![X0,X1]: (multiply(X0,inverse(multiply(X1,X0)))=inverse(X1))),
% 2.51/0.78 inference(forward_demodulation,[status(thm)],[f20,f550])).
% 2.51/0.78 fof(f614,plain,(
% 2.51/0.78 ![X0]: (multiply(c,multiply(c,c))=a|multiply(c,multiply(c,c))=X0|multiply(c,multiply(c,c))=identity|X0=a|X0=b|X0=identity|sQ10_spl)),
% 2.51/0.78 inference(resolution,[status(thm)],[f86,f68])).
% 2.51/0.78 fof(f620,plain,(
% 2.51/0.78 ![X0]: (c=a|c=X0|c=identity|X0=a|X0=b|X0=identity)),
% 2.51/0.78 inference(resolution,[status(thm)],[f86,f26])).
% 2.51/0.78 fof(f665,plain,(
% 2.51/0.78 ![X0]: (X0=a|X0=X0|X0=identity|X0=a|X0=identity|~b=b|X0=b)),
% 2.51/0.78 inference(equality_factoring,[status(thm)],[f86])).
% 2.51/0.78 fof(f679,definition,(
% 2.51/0.78 ![X0]: (sQ44_spl <=> (multiply(c,multiply(c,c))=X0|X0=a|X0=b|X0=identity))),
% 2.51/0.78 introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition])).
% 2.51/0.78 fof(f680,plain,(
% 2.51/0.78 ![X0]: (multiply(c,multiply(c,c))=X0|X0=a|X0=b|X0=identity|~sQ44_spl)),
% 2.51/0.78 inference(component_clause,[status(thm)],[f679])).
% 2.51/0.78 fof(f682,plain,(
% 2.51/0.78 sQ33_spl|sQ44_spl|sQ34_spl|sQ10_spl),
% 2.51/0.78 inference(split_clause,[status(thm)],[f614,f323,f679,f326,f66])).
% 2.51/0.78 fof(f684,definition,(
% 2.51/0.78 ![X0]: (sQ45_spl <=> (a=X0|X0=a|X0=b|X0=identity))),
% 2.51/0.78 introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition])).
% 2.51/0.78 fof(f685,plain,(
% 2.51/0.78 ![X0]: (a=X0|X0=a|X0=b|X0=identity|~sQ45_spl)),
% 2.51/0.78 inference(component_clause,[status(thm)],[f684])).
% 2.51/0.78 fof(f689,definition,(
% 2.51/0.78 ![X0]: (sQ46_spl <=> (identity=X0|X0=a|X0=b|X0=identity))),
% 2.51/0.78 introduced(definition,[new_symbols(definition,[sQ46_spl])],[split_symbol_definition])).
% 2.51/0.78 fof(f690,plain,(
% 2.51/0.78 ![X0]: (identity=X0|X0=a|X0=b|X0=identity|~sQ46_spl)),
% 2.51/0.78 inference(component_clause,[status(thm)],[f689])).
% 2.51/0.78 fof(f694,definition,(
% 2.51/0.78 ![X0]: (sQ47_spl <=> (c=X0|X0=a|X0=b|X0=identity))),
% 2.51/0.78 introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition])).
% 2.51/0.78 fof(f697,plain,(
% 2.51/0.78 sQ21_spl|sQ47_spl|sQ23_spl),
% 2.51/0.78 inference(split_clause,[status(thm)],[f620,f132,f694,f140])).
% 2.51/0.78 fof(f735,definition,(
% 2.51/0.78 ![X0]: (sQ49_spl <=> (X0=a|X0=X0|X0=identity|X0=b|X0=identity|X0=a))),
% 2.51/0.78 introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition])).
% 2.51/0.78 fof(f739,plain,(
% 2.51/0.78 sQ49_spl|~sQ13_spl),
% 2.51/0.78 inference(split_clause,[status(thm)],[f665,f735,f104])).
% 2.51/0.78 fof(f741,definition,(
% 2.51/0.78 ![X0]: (sQ50_spl <=> (X0=a|X0=identity|~X0=X0|b=X0))),
% 2.51/0.78 introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition])).
% 2.51/0.78 fof(f742,plain,(
% 2.51/0.78 ![X0]: (X0=a|X0=identity|~X0=X0|b=X0|~sQ50_spl)),
% 2.51/0.78 inference(component_clause,[status(thm)],[f741])).
% 2.51/0.78 fof(f758,plain,(
% 2.51/0.78 ![X0]: (X0=a|X0=identity|b=X0|~sQ50_spl)),
% 2.51/0.78 inference(trivial_equality_resolution,[status(thm)],[f742])).
% 2.51/0.78 fof(f762,plain,(
% 2.51/0.78 ![X0]: (identity=X0|X0=a|X0=b|~sQ46_spl)),
% 2.51/0.78 inference(duplicate_literals_removal,[status(thm)],[f690])).
% 2.51/0.78 fof(f763,plain,(
% 2.51/0.78 ![X0]: (a=X0|X0=b|X0=identity|~sQ45_spl)),
% 2.51/0.78 inference(duplicate_literals_removal,[status(thm)],[f685])).
% 2.51/0.78 fof(f772,plain,(
% 2.51/0.78 a=b|~sQ9_spl|~sQ35_spl),
% 2.51/0.78 inference(backward_demodulation,[status(thm)],[f64,f331])).
% 2.51/0.78 fof(f775,plain,(
% 2.51/0.78 $false|~sQ17_spl|sQ7_spl|~sQ36_spl),
% 2.51/0.78 inference(forward_subsumption_resolution,[status(thm)],[f343,f162])).
% 2.51/0.78 fof(f776,plain,(
% 2.51/0.78 ~sQ17_spl|sQ7_spl|~sQ36_spl),
% 2.51/0.78 inference(contradiction_clause,[status(thm)],[f775])).
% 2.51/0.78 fof(f784,plain,(
% 2.51/0.78 sQ12_spl|~sQ9_spl|~sQ35_spl),
% 2.51/0.78 inference(split_clause,[status(thm)],[f772,f101,f63,f330])).
% 2.51/0.78 fof(f796,plain,(
% 2.51/0.78 ~multiply(b,multiply(a,a))=identity|~sQ3_spl|sQ5_spl),
% 2.51/0.78 inference(forward_demodulation,[status(thm)],[f487,f51])).
% 2.51/0.78 fof(f797,plain,(
% 2.51/0.78 ~multiply(b,b)=identity|~sQ3_spl|sQ5_spl),
% 2.51/0.78 inference(forward_demodulation,[status(thm)],[f44,f796])).
% 2.51/0.78 fof(f798,plain,(
% 2.51/0.78 ~identity=identity|~sQ1_spl|~sQ3_spl|sQ5_spl),
% 2.51/0.78 inference(forward_demodulation,[status(thm)],[f37,f797])).
% 2.51/0.78 fof(f799,plain,(
% 2.51/0.78 $false|~sQ1_spl|~sQ3_spl|sQ5_spl),
% 2.51/0.78 inference(trivial_equality_resolution,[status(thm)],[f798])).
% 2.51/0.78 fof(f800,plain,(
% 2.51/0.78 ~sQ1_spl|~sQ3_spl|sQ5_spl),
% 2.51/0.78 inference(contradiction_clause,[status(thm)],[f799])).
% 2.51/0.78 fof(f805,plain,(
% 2.51/0.78 multiply(a,identity)=identity|~sQ29_spl|~sQ5_spl),
% 2.51/0.78 inference(forward_demodulation,[status(thm)],[f262,f50])).
% 2.51/0.78 fof(f806,plain,(
% 2.51/0.78 a=identity|~sQ29_spl|~sQ5_spl),
% 2.51/0.78 inference(forward_demodulation,[status(thm)],[f20,f805])).
% 2.51/0.78 fof(f807,plain,(
% 2.51/0.78 $false|~sQ29_spl|~sQ5_spl),
% 2.51/0.78 inference(forward_subsumption_resolution,[status(thm)],[f806,f25])).
% 2.51/0.78 fof(f808,plain,(
% 2.51/0.78 ~sQ29_spl|~sQ5_spl),
% 2.51/0.78 inference(contradiction_clause,[status(thm)],[f807])).
% 2.51/0.78 fof(f816,plain,(
% 2.51/0.78 identity=b|~sQ34_spl|~sQ10_spl),
% 2.51/0.78 inference(backward_demodulation,[status(thm)],[f327,f67])).
% 2.51/0.78 fof(f817,plain,(
% 2.51/0.78 ![X0]: (identity=X0|X0=a|X0=b|X0=identity|~sQ34_spl|~sQ44_spl)),
% 2.51/0.78 inference(forward_demodulation,[status(thm)],[f327,f680])).
% 2.51/0.78 fof(f818,plain,(
% 2.51/0.78 ![X0]: (identity=X0|X0=a|X0=b|~sQ34_spl|~sQ44_spl)),
% 2.51/0.78 inference(duplicate_literals_removal,[status(thm)],[f817])).
% 2.51/0.78 fof(f819,plain,(
% 2.51/0.78 sQ14_spl|~sQ34_spl|~sQ10_spl),
% 2.51/0.78 inference(split_clause,[status(thm)],[f816,f107,f326,f66])).
% 2.51/0.78 fof(f823,plain,(
% 2.51/0.78 multiply(c,a)=identity|~sQ9_spl|~sQ34_spl),
% 2.51/0.78 inference(backward_demodulation,[status(thm)],[f64,f327])).
% 2.51/0.78 fof(f830,plain,(
% 2.51/0.78 b=multiply(inverse(a),b)|~sQ40_spl),
% 2.51/0.78 inference(paramodulation,[status(thm)],[f496,f166])).
% 2.51/0.78 fof(f832,plain,(
% 2.51/0.78 a=multiply(inverse(b),b)|~sQ37_spl),
% 2.51/0.78 inference(paramodulation,[status(thm)],[f346,f166])).
% 2.51/0.78 fof(f834,plain,(
% 2.51/0.78 a=identity|~sQ37_spl),
% 2.51/0.78 inference(forward_demodulation,[status(thm)],[f18,f832])).
% 2.51/0.78 fof(f835,plain,(
% 2.51/0.78 $false|~sQ37_spl),
% 2.51/0.78 inference(forward_subsumption_resolution,[status(thm)],[f834,f25])).
% 2.51/0.78 fof(f836,plain,(
% 2.51/0.78 ~sQ37_spl),
% 2.51/0.78 inference(contradiction_clause,[status(thm)],[f835])).
% 2.51/0.78 fof(f842,plain,(
% 2.51/0.78 c=multiply(inverse(c),a)|~sQ9_spl),
% 2.51/0.78 inference(paramodulation,[status(thm)],[f64,f166])).
% 2.51/0.78 fof(f843,plain,(
% 2.51/0.78 ![X0]: (multiply(a,X0)=multiply(c,multiply(c,X0))|~sQ9_spl)),
% 2.51/0.78 inference(paramodulation,[status(thm)],[f64,f19])).
% 2.51/0.78 fof(f844,plain,(
% 2.51/0.78 a=multiply(inverse(c),identity)|~sQ9_spl|~sQ34_spl),
% 2.51/0.78 inference(paramodulation,[status(thm)],[f823,f166])).
% 2.51/0.78 fof(f845,plain,(
% 2.51/0.78 ![X0]: (multiply(identity,X0)=multiply(c,multiply(a,X0))|~sQ9_spl|~sQ34_spl)),
% 2.51/0.78 inference(paramodulation,[status(thm)],[f823,f19])).
% 2.51/0.78 fof(f846,plain,(
% 2.51/0.78 c=multiply(a,a)|~sQ34_spl|~sQ9_spl),
% 2.51/0.78 inference(backward_demodulation,[status(thm)],[f847,f842])).
% 2.51/0.78 fof(f847,plain,(
% 2.51/0.78 a=inverse(c)|~sQ9_spl|~sQ34_spl),
% 2.51/0.78 inference(forward_demodulation,[status(thm)],[f20,f844])).
% 2.51/0.78 fof(f848,plain,(
% 2.51/0.78 ![X0]: (X0=multiply(c,multiply(a,X0))|~sQ9_spl|~sQ34_spl)),
% 2.51/0.78 inference(forward_demodulation,[status(thm)],[f17,f845])).
% 2.51/0.78 fof(f852,plain,(
% 2.51/0.78 multiply(a,c)=a|~sQ34_spl|~sQ9_spl|~sQ27_spl),
% 2.51/0.78 inference(backward_demodulation,[status(thm)],[f846,f256])).
% 2.51/0.78 fof(f854,plain,(
% 2.51/0.78 c=inverse(a)|~sQ9_spl|~sQ34_spl),
% 2.51/0.78 inference(paramodulation,[status(thm)],[f847,f383])).
% 2.51/0.78 fof(f855,plain,(
% 2.51/0.78 ![X0]: (X0=multiply(a,multiply(c,X0))|~sQ9_spl|~sQ34_spl)),
% 2.51/0.78 inference(paramodulation,[status(thm)],[f847,f166])).
% 2.51/0.78 fof(f857,plain,(
% 2.51/0.78 multiply(a,c)=identity|~sQ9_spl|~sQ34_spl),
% 2.51/0.78 inference(paramodulation,[status(thm)],[f847,f18])).
% 2.51/0.78 fof(f858,plain,(
% 2.51/0.78 b=multiply(c,b)|~sQ9_spl|~sQ34_spl|~sQ40_spl),
% 2.51/0.78 inference(backward_demodulation,[status(thm)],[f854,f830])).
% 2.51/0.78 fof(f859,plain,(
% 2.51/0.78 identity=a|~sQ34_spl|~sQ9_spl|~sQ27_spl),
% 2.51/0.78 inference(backward_demodulation,[status(thm)],[f857,f852])).
% 2.51/0.78 fof(f860,plain,(
% 2.51/0.78 sQ16_spl|~sQ34_spl|~sQ9_spl|~sQ27_spl),
% 2.51/0.78 inference(split_clause,[status(thm)],[f859,f114,f326,f63,f255])).
% 2.51/0.78 fof(f865,plain,(
% 2.51/0.78 a=multiply(inverse(b),identity)|~sQ38_spl),
% 2.51/0.78 inference(paramodulation,[status(thm)],[f349,f166])).
% 2.51/0.78 fof(f867,plain,(
% 2.51/0.78 b=a|~sQ38_spl|~sQ1_spl),
% 2.51/0.78 inference(backward_demodulation,[status(thm)],[f868,f478])).
% 2.51/0.78 fof(f868,plain,(
% 2.51/0.78 a=inverse(b)|~sQ38_spl),
% 2.51/0.78 inference(forward_demodulation,[status(thm)],[f20,f865])).
% 2.51/0.78 fof(f870,plain,(
% 2.51/0.78 sQ12_spl|~sQ38_spl|~sQ1_spl),
% 2.51/0.78 inference(split_clause,[status(thm)],[f867,f101,f348,f36])).
% 2.51/0.78 fof(f871,plain,(
% 2.51/0.78 ~a=a|~sQ38_spl|sQ30_spl),
% 2.51/0.78 inference(forward_demodulation,[status(thm)],[f868,f294])).
% 2.51/0.78 fof(f872,plain,(
% 2.51/0.78 $false|~sQ38_spl|sQ30_spl),
% 2.51/0.78 inference(trivial_equality_resolution,[status(thm)],[f871])).
% 2.51/0.78 fof(f873,plain,(
% 2.51/0.78 ~sQ38_spl|sQ30_spl),
% 2.51/0.78 inference(contradiction_clause,[status(thm)],[f872])).
% 2.51/0.78 fof(f886,plain,(
% 2.51/0.78 multiply(b,a)=a|~sQ17_spl|~sQ7_spl),
% 2.51/0.78 inference(backward_demodulation,[status(thm)],[f119,f57])).
% 2.51/0.78 fof(f896,plain,(
% 2.51/0.78 b=multiply(inverse(b),a)|~sQ17_spl),
% 2.51/0.78 inference(paramodulation,[status(thm)],[f119,f166])).
% 2.51/0.78 fof(f898,plain,(
% 2.51/0.78 a=multiply(inverse(b),a)|~sQ17_spl|~sQ7_spl),
% 2.51/0.78 inference(paramodulation,[status(thm)],[f886,f166])).
% 2.51/0.78 fof(f900,plain,(
% 2.51/0.78 b=a|~sQ7_spl|~sQ17_spl),
% 2.51/0.78 inference(backward_demodulation,[status(thm)],[f898,f896])).
% 2.51/0.78 fof(f901,plain,(
% 2.51/0.78 sQ12_spl|~sQ7_spl|~sQ17_spl),
% 2.51/0.78 inference(split_clause,[status(thm)],[f900,f101,f56,f118])).
% 2.51/0.78 fof(f902,plain,(
% 2.51/0.78 sQ20_spl|~sQ50_spl),
% 2.51/0.78 inference(split_clause,[status(thm)],[f758,f129,f741])).
% 2.51/0.78 fof(f903,plain,(
% 2.51/0.78 sQ20_spl|~sQ46_spl),
% 2.51/0.78 inference(split_clause,[status(thm)],[f762,f129,f689])).
% 2.51/0.78 fof(f904,plain,(
% 2.51/0.78 sQ20_spl|~sQ45_spl),
% 2.51/0.78 inference(split_clause,[status(thm)],[f763,f129,f684])).
% 2.51/0.78 fof(f915,plain,(
% 2.51/0.78 multiply(b,inverse(a))=inverse(b)|~sQ17_spl),
% 2.51/0.78 inference(paramodulation,[status(thm)],[f119,f576])).
% 2.51/0.78 fof(f916,plain,(
% 2.51/0.78 multiply(a,inverse(b))=inverse(inverse(b))|~sQ17_spl),
% 2.51/0.78 inference(paramodulation,[status(thm)],[f896,f576])).
% 2.51/0.78 fof(f931,plain,(
% 2.51/0.78 multiply(a,inverse(b))=b|~sQ17_spl),
% 2.51/0.78 inference(forward_demodulation,[status(thm)],[f383,f916])).
% 2.51/0.78 fof(f980,plain,(
% 2.51/0.78 multiply(a,c)=b|inverse(b)=a|inverse(b)=b|inverse(b)=identity|~sQ17_spl),
% 2.51/0.78 inference(paramodulation,[status(thm)],[f22,f931])).
% 2.51/0.78 fof(f983,plain,(
% 2.51/0.78 ![X0]: (multiply(b,X0)=multiply(a,multiply(inverse(b),X0))|~sQ17_spl)),
% 2.51/0.78 inference(paramodulation,[status(thm)],[f931,f19])).
% 2.51/0.78 fof(f994,definition,(
% 2.51/0.78 sQ57_spl <=> (multiply(a,c)=b)),
% 2.51/0.78 introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition])).
% 2.51/0.78 fof(f995,plain,(
% 2.51/0.78 multiply(a,c)=b|~sQ57_spl),
% 2.51/0.78 inference(component_clause,[status(thm)],[f994])).
% 2.51/0.78 fof(f997,plain,(
% 2.51/0.78 sQ57_spl|sQ30_spl|sQ31_spl|sQ32_spl|~sQ17_spl),
% 2.51/0.78 inference(split_clause,[status(thm)],[f980,f994,f292,f295,f298,f118])).
% 2.51/0.78 fof(f1008,plain,(
% 2.51/0.78 multiply(a,b)=identity|~sQ28_spl|~sQ5_spl),
% 2.51/0.78 inference(forward_demodulation,[status(thm)],[f259,f50])).
% 2.51/0.78 fof(f1009,plain,(
% 2.51/0.78 $false|sQ41_spl|~sQ28_spl|~sQ5_spl),
% 2.51/0.78 inference(forward_subsumption_resolution,[status(thm)],[f1008,f500])).
% 2.51/0.78 fof(f1010,plain,(
% 2.51/0.78 sQ41_spl|~sQ28_spl|~sQ5_spl),
% 2.51/0.78 inference(contradiction_clause,[status(thm)],[f1009])).
% 2.51/0.78 fof(f1052,plain,(
% 2.51/0.78 ![X0]: (~c=a|X0=a|X0=b|X0=identity|multiply(X0,c)=a|multiply(X0,c)=b|multiply(X0,c)=identity|sQ9_spl)),
% 2.51/0.78 inference(paramodulation,[status(thm)],[f22,f97])).
% 2.51/0.78 fof(f1057,definition,(
% 2.51/0.78 ![X0]: (sQ58_spl <=> (X0=a|X0=b|X0=identity|multiply(X0,c)=a|multiply(X0,c)=b|multiply(X0,c)=identity))),
% 2.51/0.78 introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition])).
% 2.51/0.78 fof(f1060,plain,(
% 2.51/0.78 ~sQ21_spl|sQ58_spl|sQ9_spl),
% 2.51/0.78 inference(split_clause,[status(thm)],[f1052,f132,f1057,f63])).
% 2.51/0.78 fof(f1061,definition,(
% 2.51/0.78 sQ59_spl <=> (inverse(c)=a)),
% 2.51/0.78 introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition])).
% 2.51/0.78 fof(f1062,plain,(
% 2.51/0.78 inverse(c)=a|~sQ59_spl),
% 2.51/0.78 inference(component_clause,[status(thm)],[f1061])).
% 2.51/0.78 fof(f1063,plain,(
% 2.51/0.78 ~inverse(c)=a|sQ59_spl),
% 2.51/0.78 inference(component_clause,[status(thm)],[f1061])).
% 2.51/0.78 fof(f1064,definition,(
% 2.51/0.78 sQ60_spl <=> (inverse(c)=b)),
% 2.51/0.78 introduced(definition,[new_symbols(definition,[sQ60_spl])],[split_symbol_definition])).
% 2.51/0.78 fof(f1065,plain,(
% 2.51/0.78 inverse(c)=b|~sQ60_spl),
% 2.51/0.78 inference(component_clause,[status(thm)],[f1064])).
% 2.51/0.78 fof(f1067,definition,(
% 2.51/0.78 sQ61_spl <=> (inverse(c)=identity)),
% 2.51/0.78 introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition])).
% 2.51/0.78 fof(f1068,plain,(
% 2.51/0.78 inverse(c)=identity|~sQ61_spl),
% 2.51/0.78 inference(component_clause,[status(thm)],[f1067])).
% 2.51/0.78 fof(f1074,plain,(
% 2.51/0.78 ![X0]: (multiply(a,X0)=b|X0=a|X0=b|X0=identity|~sQ57_spl)),
% 2.51/0.78 inference(paramodulation,[status(thm)],[f22,f995])).
% 2.51/0.78 fof(f1097,plain,(
% 2.51/0.78 ![X0]: (inverse(multiply(X0,b))=multiply(b,inverse(X0))|~sQ1_spl)),
% 2.51/0.78 inference(paramodulation,[status(thm)],[f576,f241])).
% 2.51/0.78 fof(f1122,definition,(
% 2.51/0.78 sQ66_spl <=> (multiply(c,b)=b)),
% 2.51/0.78 introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition])).
% 2.51/0.78 fof(f1123,plain,(
% 2.51/0.78 multiply(c,b)=b|~sQ66_spl),
% 2.51/0.78 inference(component_clause,[status(thm)],[f1122])).
% 2.51/0.78 fof(f1125,definition,(
% 2.51/0.78 sQ67_spl <=> (multiply(c,b)=identity)),
% 2.51/0.78 introduced(definition,[new_symbols(definition,[sQ67_spl])],[split_symbol_definition])).
% 2.51/0.78 fof(f1126,plain,(
% 2.51/0.78 multiply(c,b)=identity|~sQ67_spl),
% 2.51/0.78 inference(component_clause,[status(thm)],[f1125])).
% 2.51/0.78 fof(f1142,definition,(
% 2.51/0.78 sQ68_spl <=> (c=c)),
% 2.51/0.78 introduced(definition,[new_symbols(definition,[sQ68_spl])],[split_symbol_definition])).
% 2.51/0.78 fof(f1145,definition,(
% 2.51/0.78 sQ69_spl <=> (inverse(a)=a)),
% 2.51/0.78 introduced(definition,[new_symbols(definition,[sQ69_spl])],[split_symbol_definition])).
% 2.51/0.78 fof(f1146,plain,(
% 2.51/0.78 inverse(a)=a|~sQ69_spl),
% 2.51/0.78 inference(component_clause,[status(thm)],[f1145])).
% 2.51/0.78 fof(f1148,definition,(
% 2.51/0.78 sQ70_spl <=> (inverse(a)=b)),
% 2.51/0.78 introduced(definition,[new_symbols(definition,[sQ70_spl])],[split_symbol_definition])).
% 2.51/0.78 fof(f1149,plain,(
% 2.51/0.78 inverse(a)=b|~sQ70_spl),
% 2.51/0.78 inference(component_clause,[status(thm)],[f1148])).
% 2.51/0.78 fof(f1151,definition,(
% 2.51/0.78 sQ71_spl <=> (inverse(a)=identity)),
% 2.51/0.78 introduced(definition,[new_symbols(definition,[sQ71_spl])],[split_symbol_definition])).
% 2.51/0.78 fof(f1152,plain,(
% 2.51/0.78 inverse(a)=identity|~sQ71_spl),
% 2.51/0.78 inference(component_clause,[status(thm)],[f1151])).
% 2.51/0.78 fof(f1165,plain,(
% 2.51/0.78 multiply(a,a)=identity|~sQ69_spl),
% 2.51/0.78 inference(paramodulation,[status(thm)],[f1146,f21])).
% 2.51/0.78 fof(f1169,plain,(
% 2.51/0.78 sQ0_spl|~sQ69_spl),
% 2.51/0.78 inference(split_clause,[status(thm)],[f1165,f33,f1145])).
% 2.51/0.78 fof(f1177,plain,(
% 2.51/0.78 multiply(inverse(c),a)=a|multiply(inverse(c),a)=b|multiply(inverse(c),a)=identity|sQ9_spl),
% 2.51/0.78 inference(resolution,[status(thm)],[f96,f174])).
% 2.51/0.78 fof(f1178,plain,(
% 2.51/0.78 ![X0]: (~c=a|X0=a|X0=b|X0=identity|multiply(c,X0)=a|multiply(c,X0)=b|multiply(c,X0)=identity|sQ9_spl)),
% 2.51/0.78 inference(paramodulation,[status(thm)],[f22,f96])).
% 2.51/0.78 fof(f1184,definition,(
% 2.51/0.78 sQ72_spl <=> (multiply(inverse(c),a)=a)),
% 2.51/0.78 introduced(definition,[new_symbols(definition,[sQ72_spl])],[split_symbol_definition])).
% 2.51/0.78 fof(f1185,plain,(
% 2.51/0.78 multiply(inverse(c),a)=a|~sQ72_spl),
% 2.51/0.78 inference(component_clause,[status(thm)],[f1184])).
% 2.51/0.78 fof(f1186,plain,(
% 2.51/0.78 ~multiply(inverse(c),a)=a|sQ72_spl),
% 2.51/0.78 inference(component_clause,[status(thm)],[f1184])).
% 2.51/0.78 fof(f1187,definition,(
% 2.51/0.78 sQ73_spl <=> (multiply(inverse(c),a)=b)),
% 2.51/0.78 introduced(definition,[new_symbols(definition,[sQ73_spl])],[split_symbol_definition])).
% 2.51/0.78 fof(f1188,plain,(
% 2.51/0.78 multiply(inverse(c),a)=b|~sQ73_spl),
% 2.51/0.78 inference(component_clause,[status(thm)],[f1187])).
% 2.51/0.78 fof(f1190,definition,(
% 2.51/0.78 sQ74_spl <=> (multiply(inverse(c),a)=identity)),
% 2.51/0.78 introduced(definition,[new_symbols(definition,[sQ74_spl])],[split_symbol_definition])).
% 2.51/0.78 fof(f1191,plain,(
% 2.51/0.78 multiply(inverse(c),a)=identity|~sQ74_spl),
% 2.51/0.78 inference(component_clause,[status(thm)],[f1190])).
% 2.51/0.78 fof(f1193,plain,(
% 2.51/0.78 sQ72_spl|sQ73_spl|sQ74_spl|sQ9_spl),
% 2.51/0.78 inference(split_clause,[status(thm)],[f1177,f1184,f1187,f1190,f63])).
% 2.51/0.78 fof(f1194,definition,(
% 2.51/0.78 ![X0]: (sQ75_spl <=> (X0=a|X0=b|X0=identity|multiply(c,X0)=a|multiply(c,X0)=b|multiply(c,X0)=identity))),
% 2.51/0.78 introduced(definition,[new_symbols(definition,[sQ75_spl])],[split_symbol_definition])).
% 2.51/0.78 fof(f1197,plain,(
% 2.51/0.78 ~sQ21_spl|sQ75_spl|sQ9_spl),
% 2.51/0.78 inference(split_clause,[status(thm)],[f1178,f132,f1194,f63])).
% 2.51/0.78 fof(f1208,plain,(
% 2.51/0.78 inverse(c)=a|inverse(c)=b|inverse(c)=identity|sQ2_spl),
% 2.51/0.78 inference(resolution,[status(thm)],[f95,f18])).
% 2.51/0.78 fof(f1214,plain,(
% 2.51/0.78 sQ59_spl|sQ60_spl|sQ61_spl|sQ2_spl),
% 2.51/0.78 inference(split_clause,[status(thm)],[f1208,f1061,f1064,f1067,f39])).
% 2.51/0.78 fof(f1224,plain,(
% 2.51/0.78 multiply(a,a)=a|~sQ59_spl|~sQ72_spl),
% 2.51/0.78 inference(forward_demodulation,[status(thm)],[f1062,f1185])).
% 2.51/0.78 fof(f1225,plain,(
% 2.51/0.78 $false|sQ24_spl|~sQ59_spl|~sQ72_spl),
% 2.51/0.78 inference(forward_subsumption_resolution,[status(thm)],[f1224,f192])).
% 2.51/0.78 fof(f1226,plain,(
% 2.51/0.78 sQ24_spl|~sQ59_spl|~sQ72_spl),
% 2.51/0.78 inference(contradiction_clause,[status(thm)],[f1225])).
% 2.51/0.78 fof(f1246,plain,(
% 2.51/0.78 ~multiply(b,c)=a|~sQ6_spl|sQ7_spl),
% 2.51/0.78 inference(backward_demodulation,[status(thm)],[f54,f58])).
% 2.51/0.78 fof(f1250,plain,(
% 2.51/0.78 ~c=a|inverse(c)=a|inverse(c)=b|inverse(c)=identity|sQ59_spl),
% 2.51/0.78 inference(paramodulation,[status(thm)],[f22,f1063])).
% 2.51/0.78 fof(f1252,plain,(
% 2.51/0.78 ~sQ21_spl|sQ59_spl|sQ60_spl|sQ61_spl),
% 2.51/0.78 inference(split_clause,[status(thm)],[f1250,f132,f1061,f1064,f1067])).
% 2.51/0.78 fof(f1255,plain,(
% 2.51/0.78 multiply(b,a)=a|~sQ60_spl|~sQ72_spl),
% 2.51/0.78 inference(backward_demodulation,[status(thm)],[f1065,f1185])).
% 2.51/0.78 fof(f1270,plain,(
% 2.51/0.78 c=inverse(b)|~sQ60_spl),
% 2.51/0.78 inference(paramodulation,[status(thm)],[f1065,f383])).
% 2.51/0.78 fof(f1272,plain,(
% 2.51/0.78 multiply(c,b)=identity|~sQ60_spl),
% 2.51/0.78 inference(paramodulation,[status(thm)],[f1065,f21])).
% 2.51/0.78 fof(f1273,plain,(
% 2.51/0.78 multiply(b,c)=identity|~sQ60_spl),
% 2.51/0.78 inference(paramodulation,[status(thm)],[f1065,f18])).
% 2.51/0.78 fof(f1279,plain,(
% 2.51/0.78 sQ67_spl|~sQ60_spl),
% 2.51/0.78 inference(split_clause,[status(thm)],[f1272,f1125,f1064])).
% 2.51/0.78 fof(f1309,plain,(
% 2.51/0.78 c=inverse(identity)|~sQ61_spl),
% 2.51/0.78 inference(paramodulation,[status(thm)],[f1068,f383])).
% 2.51/0.78 fof(f1332,plain,(
% 2.51/0.78 c=identity|~sQ61_spl),
% 2.51/0.78 inference(forward_demodulation,[status(thm)],[f163,f1309])).
% 2.51/0.78 fof(f1333,plain,(
% 2.51/0.78 $false|~sQ61_spl),
% 2.51/0.78 inference(forward_subsumption_resolution,[status(thm)],[f1332,f28])).
% 2.51/0.78 fof(f1334,plain,(
% 2.51/0.78 ~sQ61_spl),
% 2.51/0.78 inference(contradiction_clause,[status(thm)],[f1333])).
% 2.51/0.78 fof(f1350,plain,(
% 2.51/0.78 multiply(b,inverse(c))=inverse(b)|~sQ6_spl),
% 2.51/0.78 inference(paramodulation,[status(thm)],[f54,f576])).
% 2.51/0.78 fof(f1351,plain,(
% 2.51/0.78 b=multiply(inverse(b),c)|~sQ6_spl),
% 2.51/0.78 inference(paramodulation,[status(thm)],[f54,f166])).
% 2.51/0.78 fof(f1352,plain,(
% 2.51/0.78 ![X0]: (multiply(c,X0)=multiply(b,multiply(b,X0))|~sQ6_spl)),
% 2.51/0.78 inference(paramodulation,[status(thm)],[f54,f19])).
% 2.51/0.78 fof(f1356,definition,(
% 2.51/0.78 sQ76_spl <=> (multiply(b,c)=a)),
% 2.51/0.78 introduced(definition,[new_symbols(definition,[sQ76_spl])],[split_symbol_definition])).
% 2.51/0.78 fof(f1357,plain,(
% 2.51/0.78 multiply(b,c)=a|~sQ76_spl),
% 2.51/0.78 inference(component_clause,[status(thm)],[f1356])).
% 2.51/0.78 fof(f1362,definition,(
% 2.51/0.78 sQ78_spl <=> (multiply(b,c)=identity)),
% 2.51/0.78 introduced(definition,[new_symbols(definition,[sQ78_spl])],[split_symbol_definition])).
% 2.51/0.78 fof(f1363,plain,(
% 2.51/0.78 multiply(b,c)=identity|~sQ78_spl),
% 2.51/0.78 inference(component_clause,[status(thm)],[f1362])).
% 2.51/0.78 fof(f1368,plain,(
% 2.51/0.78 ![X0]: (multiply(c,X0)=identity|X0=a|X0=b|X0=identity|~sQ2_spl)),
% 2.51/0.78 inference(paramodulation,[status(thm)],[f22,f40])).
% 2.51/0.78 fof(f1370,plain,(
% 2.51/0.78 multiply(c,inverse(identity))=inverse(c)|~sQ2_spl),
% 2.51/0.78 inference(paramodulation,[status(thm)],[f40,f576])).
% 2.51/0.78 fof(f1372,plain,(
% 2.51/0.78 ![X0]: (multiply(identity,X0)=multiply(c,multiply(c,X0))|~sQ2_spl)),
% 2.51/0.78 inference(paramodulation,[status(thm)],[f40,f19])).
% 2.51/0.78 fof(f1375,plain,(
% 2.51/0.78 multiply(c,identity)=inverse(c)|~sQ2_spl),
% 2.51/0.78 inference(forward_demodulation,[status(thm)],[f163,f1370])).
% 2.51/0.78 fof(f1377,plain,(
% 2.51/0.78 multiply(b,c)=inverse(b)|~sQ2_spl|~sQ6_spl),
% 2.51/0.78 inference(backward_demodulation,[status(thm)],[f1383,f1350])).
% 2.51/0.78 fof(f1383,plain,(
% 2.51/0.78 c=inverse(c)|~sQ2_spl),
% 2.51/0.78 inference(forward_demodulation,[status(thm)],[f20,f1375])).
% 2.51/0.78 fof(f1387,plain,(
% 2.51/0.78 ![X0]: (X0=multiply(c,multiply(c,X0))|~sQ2_spl)),
% 2.51/0.78 inference(forward_demodulation,[status(thm)],[f17,f1372])).
% 2.51/0.78 fof(f1389,plain,(
% 2.51/0.78 c=c|inverse(c)=a|inverse(c)=b|inverse(c)=identity|~sQ2_spl),
% 2.51/0.78 inference(paramodulation,[status(thm)],[f22,f1383])).
% 2.51/0.78 fof(f1396,plain,(
% 2.51/0.78 sQ68_spl|sQ59_spl|sQ60_spl|sQ61_spl|~sQ2_spl),
% 2.51/0.78 inference(split_clause,[status(thm)],[f1389,f1142,f1061,f1064,f1067,f39])).
% 2.51/0.78 fof(f1402,plain,(
% 2.51/0.78 b=multiply(c,c)|~sQ60_spl|~sQ6_spl),
% 2.51/0.78 inference(backward_demodulation,[status(thm)],[f1270,f1351])).
% 2.51/0.78 fof(f1414,plain,(
% 2.51/0.78 ~multiply(c,b)=identity|~sQ60_spl|~sQ6_spl|sQ34_spl),
% 2.51/0.78 inference(backward_demodulation,[status(thm)],[f1402,f328])).
% 2.51/0.78 fof(f1420,plain,(
% 2.51/0.78 ~sQ67_spl|~sQ60_spl|~sQ6_spl|sQ34_spl),
% 2.51/0.78 inference(split_clause,[status(thm)],[f1414,f1125,f1064,f53,f326])).
% 2.51/0.78 fof(f1436,plain,(
% 2.51/0.78 multiply(a,b)=b|~sQ59_spl|~sQ73_spl|~sQ28_spl),
% 2.51/0.78 inference(backward_demodulation,[status(thm)],[f1437,f259])).
% 2.51/0.78 fof(f1437,plain,(
% 2.51/0.78 multiply(a,a)=b|~sQ59_spl|~sQ73_spl),
% 2.51/0.78 inference(forward_demodulation,[status(thm)],[f1062,f1188])).
% 2.51/0.79 fof(f1442,plain,(
% 2.51/0.79 c=inverse(a)|~sQ59_spl),
% 2.51/0.79 inference(paramodulation,[status(thm)],[f1062,f383])).
% 2.51/0.79 fof(f1445,plain,(
% 2.51/0.79 multiply(a,c)=identity|~sQ59_spl),
% 2.51/0.79 inference(paramodulation,[status(thm)],[f1062,f18])).
% 2.51/0.79 fof(f1454,plain,(
% 2.51/0.79 a=multiply(inverse(a),b)|~sQ59_spl|~sQ73_spl),
% 2.51/0.79 inference(paramodulation,[status(thm)],[f1437,f166])).
% 2.51/0.79 fof(f1459,plain,(
% 2.51/0.79 a=multiply(c,b)|~sQ59_spl|~sQ73_spl),
% 2.51/0.79 inference(forward_demodulation,[status(thm)],[f1442,f1454])).
% 2.51/0.79 fof(f1461,plain,(
% 2.51/0.79 b=multiply(inverse(a),b)|~sQ59_spl|~sQ73_spl|~sQ28_spl),
% 2.51/0.79 inference(paramodulation,[status(thm)],[f1436,f166])).
% 2.51/0.79 fof(f1465,plain,(
% 2.51/0.79 b=multiply(c,b)|~sQ59_spl|~sQ73_spl|~sQ28_spl),
% 2.51/0.79 inference(forward_demodulation,[status(thm)],[f1442,f1461])).
% 2.51/0.79 fof(f1466,plain,(
% 2.51/0.79 b=a|~sQ59_spl|~sQ73_spl|~sQ28_spl),
% 2.51/0.79 inference(forward_demodulation,[status(thm)],[f1459,f1465])).
% 2.51/0.79 fof(f1467,plain,(
% 2.51/0.79 $false|~sQ59_spl|~sQ73_spl|~sQ28_spl),
% 2.51/0.79 inference(forward_subsumption_resolution,[status(thm)],[f1466,f23])).
% 2.51/0.79 fof(f1468,plain,(
% 2.51/0.79 ~sQ59_spl|~sQ73_spl|~sQ28_spl),
% 2.51/0.79 inference(contradiction_clause,[status(thm)],[f1467])).
% 2.51/0.79 fof(f1477,plain,(
% 2.51/0.79 ~b=b|~sQ59_spl|~sQ73_spl|sQ3_spl),
% 2.51/0.79 inference(forward_demodulation,[status(thm)],[f1437,f45])).
% 2.51/0.79 fof(f1478,plain,(
% 2.51/0.79 $false|~sQ59_spl|~sQ73_spl|sQ3_spl),
% 2.51/0.79 inference(trivial_equality_resolution,[status(thm)],[f1477])).
% 2.51/0.79 fof(f1479,plain,(
% 2.51/0.79 ~sQ59_spl|~sQ73_spl|sQ3_spl),
% 2.51/0.79 inference(contradiction_clause,[status(thm)],[f1478])).
% 2.51/0.79 fof(f1494,plain,(
% 2.51/0.79 multiply(c,a)=identity|~sQ2_spl|~sQ74_spl),
% 2.51/0.79 inference(forward_demodulation,[status(thm)],[f1383,f1191])).
% 2.51/0.79 fof(f1509,plain,(
% 2.51/0.79 ~multiply(c,a)=a|~sQ2_spl|sQ72_spl),
% 2.51/0.79 inference(forward_demodulation,[status(thm)],[f1383,f1186])).
% 2.51/0.79 fof(f1511,plain,(
% 2.51/0.79 multiply(c,a)=b|~sQ2_spl|~sQ73_spl),
% 2.51/0.79 inference(forward_demodulation,[status(thm)],[f1383,f1188])).
% 2.51/0.79 fof(f1512,plain,(
% 2.51/0.79 multiply(a,b)=identity|~sQ3_spl|~sQ29_spl),
% 2.51/0.79 inference(backward_demodulation,[status(thm)],[f44,f262])).
% 2.51/0.79 fof(f1520,plain,(
% 2.51/0.79 sQ41_spl|~sQ3_spl|~sQ29_spl),
% 2.51/0.79 inference(split_clause,[status(thm)],[f1512,f498,f43,f261])).
% 2.51/0.79 fof(f1536,plain,(
% 2.51/0.79 multiply(a,inverse(b))=inverse(c)|~sQ2_spl|~sQ73_spl),
% 2.51/0.79 inference(paramodulation,[status(thm)],[f1511,f576])).
% 2.51/0.79 fof(f1537,plain,(
% 2.51/0.79 a=multiply(inverse(c),b)|~sQ2_spl|~sQ73_spl),
% 2.51/0.79 inference(paramodulation,[status(thm)],[f1511,f166])).
% 2.51/0.79 fof(f1540,plain,(
% 2.51/0.79 multiply(a,inverse(b))=c|~sQ2_spl|~sQ73_spl),
% 2.51/0.79 inference(forward_demodulation,[status(thm)],[f1383,f1536])).
% 2.51/0.79 fof(f1542,plain,(
% 2.51/0.79 a=multiply(c,b)|~sQ2_spl|~sQ73_spl),
% 2.51/0.79 inference(forward_demodulation,[status(thm)],[f1383,f1537])).
% 2.51/0.79 fof(f1543,plain,(
% 2.51/0.79 multiply(b,inverse(identity))=inverse(a)|~sQ41_spl),
% 2.51/0.79 inference(paramodulation,[status(thm)],[f499,f576])).
% 2.51/0.79 fof(f1546,plain,(
% 2.51/0.79 multiply(b,identity)=inverse(a)|~sQ41_spl),
% 2.51/0.79 inference(forward_demodulation,[status(thm)],[f163,f1543])).
% 2.51/0.79 fof(f1549,plain,(
% 2.51/0.79 b=inverse(a)|~sQ41_spl),
% 2.51/0.79 inference(forward_demodulation,[status(thm)],[f20,f1546])).
% 2.51/0.79 fof(f1556,plain,(
% 2.51/0.79 multiply(b,a)=identity|~sQ41_spl),
% 2.51/0.79 inference(paramodulation,[status(thm)],[f1549,f18])).
% 2.51/0.79 fof(f1558,plain,(
% 2.51/0.79 sQ38_spl|~sQ41_spl),
% 2.51/0.79 inference(split_clause,[status(thm)],[f1556,f348,f498])).
% 2.51/0.79 fof(f1564,plain,(
% 2.51/0.79 multiply(c,a)=a|~sQ2_spl|~sQ72_spl),
% 2.51/0.79 inference(forward_demodulation,[status(thm)],[f1383,f1185])).
% 2.51/0.79 fof(f1568,plain,(
% 2.51/0.79 multiply(a,inverse(identity))=inverse(a)|~sQ0_spl),
% 2.51/0.79 inference(paramodulation,[status(thm)],[f34,f576])).
% 2.51/0.79 fof(f1571,plain,(
% 2.51/0.79 multiply(a,identity)=inverse(a)|~sQ0_spl),
% 2.51/0.79 inference(forward_demodulation,[status(thm)],[f163,f1568])).
% 2.51/0.79 fof(f1573,plain,(
% 2.51/0.79 a=inverse(a)|~sQ0_spl),
% 2.51/0.79 inference(forward_demodulation,[status(thm)],[f20,f1571])).
% 2.51/0.79 fof(f1603,plain,(
% 2.51/0.79 multiply(c,b)=multiply(b,c)|~sQ6_spl),
% 2.51/0.79 inference(paramodulation,[status(thm)],[f54,f1352])).
% 2.51/0.79 fof(f1616,plain,(
% 2.51/0.79 multiply(c,b)=inverse(b)|~sQ2_spl|~sQ6_spl),
% 2.51/0.79 inference(forward_demodulation,[status(thm)],[f1377,f1603])).
% 2.51/0.79 fof(f1654,plain,(
% 2.51/0.79 multiply(a,inverse(a))=inverse(c)|~sQ2_spl|~sQ72_spl),
% 2.51/0.79 inference(paramodulation,[status(thm)],[f1564,f576])).
% 2.51/0.79 fof(f1657,definition,(
% 2.51/0.79 sQ79_spl <=> (multiply(c,a)=a)),
% 2.51/0.79 introduced(definition,[new_symbols(definition,[sQ79_spl])],[split_symbol_definition])).
% 2.51/0.79 fof(f1658,plain,(
% 2.51/0.79 multiply(c,a)=a|~sQ79_spl),
% 2.51/0.79 inference(component_clause,[status(thm)],[f1657])).
% 2.51/0.79 fof(f1667,plain,(
% 2.51/0.79 c=identity|~sQ72_spl|~sQ2_spl),
% 2.51/0.79 inference(backward_demodulation,[status(thm)],[f1668,f1383])).
% 2.51/0.79 fof(f1668,plain,(
% 2.51/0.79 identity=inverse(c)|~sQ2_spl|~sQ72_spl),
% 2.51/0.79 inference(forward_demodulation,[status(thm)],[f21,f1654])).
% 2.51/0.79 fof(f1670,plain,(
% 2.51/0.79 sQ23_spl|~sQ72_spl|~sQ2_spl),
% 2.51/0.79 inference(split_clause,[status(thm)],[f1667,f140,f1184,f39])).
% 2.51/0.79 fof(f1676,plain,(
% 2.51/0.79 a=inverse(b)|~sQ73_spl|~sQ2_spl|~sQ6_spl),
% 2.51/0.79 inference(backward_demodulation,[status(thm)],[f1542,f1616])).
% 2.51/0.79 fof(f1678,plain,(
% 2.51/0.79 sQ30_spl|~sQ73_spl|~sQ2_spl|~sQ6_spl),
% 2.51/0.79 inference(split_clause,[status(thm)],[f1676,f292,f1187,f39,f53])).
% 2.51/0.79 fof(f1679,plain,(
% 2.51/0.79 identity=a|~sQ2_spl|~sQ9_spl),
% 2.51/0.79 inference(forward_demodulation,[status(thm)],[f40,f64])).
% 2.51/0.79 fof(f1680,plain,(
% 2.51/0.79 $false|~sQ2_spl|~sQ9_spl),
% 2.51/0.79 inference(forward_subsumption_resolution,[status(thm)],[f1679,f25])).
% 2.51/0.79 fof(f1681,plain,(
% 2.51/0.79 ~sQ2_spl|~sQ9_spl),
% 2.51/0.79 inference(contradiction_clause,[status(thm)],[f1680])).
% 2.51/0.79 fof(f1703,plain,(
% 2.51/0.79 a=b|~sQ0_spl|~sQ70_spl),
% 2.51/0.79 inference(forward_demodulation,[status(thm)],[f1573,f1149])).
% 2.51/0.79 fof(f1704,plain,(
% 2.51/0.79 $false|~sQ0_spl|~sQ70_spl),
% 2.51/0.79 inference(forward_subsumption_resolution,[status(thm)],[f1703,f23])).
% 2.51/0.79 fof(f1705,plain,(
% 2.51/0.79 ~sQ0_spl|~sQ70_spl),
% 2.51/0.79 inference(contradiction_clause,[status(thm)],[f1704])).
% 2.51/0.79 fof(f1718,plain,(
% 2.51/0.79 a=multiply(c,identity)|~sQ2_spl|~sQ74_spl),
% 2.51/0.79 inference(paramodulation,[status(thm)],[f1494,f1387])).
% 2.51/0.79 fof(f1723,plain,(
% 2.51/0.79 a=c|~sQ2_spl|~sQ74_spl),
% 2.51/0.79 inference(forward_demodulation,[status(thm)],[f20,f1718])).
% 2.51/0.79 fof(f1724,plain,(
% 2.51/0.79 $false|~sQ2_spl|~sQ74_spl),
% 2.51/0.79 inference(forward_subsumption_resolution,[status(thm)],[f1723,f24])).
% 2.51/0.79 fof(f1725,plain,(
% 2.51/0.79 ~sQ2_spl|~sQ74_spl),
% 2.51/0.79 inference(contradiction_clause,[status(thm)],[f1724])).
% 2.51/0.79 fof(f1729,plain,(
% 2.51/0.79 multiply(a,a)=identity|~sQ59_spl|~sQ74_spl),
% 2.51/0.79 inference(backward_demodulation,[status(thm)],[f1062,f1191])).
% 2.51/0.79 fof(f1739,plain,(
% 2.51/0.79 sQ0_spl|~sQ59_spl|~sQ74_spl),
% 2.51/0.79 inference(split_clause,[status(thm)],[f1729,f33,f1061,f1190])).
% 2.51/0.79 fof(f1744,plain,(
% 2.51/0.79 ~multiply(a,multiply(a,identity))=identity|~sQ0_spl|sQ5_spl),
% 2.51/0.79 inference(forward_demodulation,[status(thm)],[f34,f51])).
% 2.51/0.79 fof(f1745,plain,(
% 2.51/0.79 ~multiply(a,a)=identity|~sQ0_spl|sQ5_spl),
% 2.51/0.79 inference(forward_demodulation,[status(thm)],[f20,f1744])).
% 2.51/0.79 fof(f1746,plain,(
% 2.51/0.79 ~identity=identity|~sQ0_spl|sQ5_spl),
% 2.51/0.79 inference(forward_demodulation,[status(thm)],[f34,f1745])).
% 2.51/0.79 fof(f1747,plain,(
% 2.51/0.79 $false|~sQ0_spl|sQ5_spl),
% 2.51/0.79 inference(trivial_equality_resolution,[status(thm)],[f1746])).
% 2.51/0.79 fof(f1748,plain,(
% 2.51/0.79 ~sQ0_spl|sQ5_spl),
% 2.51/0.79 inference(contradiction_clause,[status(thm)],[f1747])).
% 2.51/0.79 fof(f1756,plain,(
% 2.51/0.79 c=a|~sQ0_spl|~sQ59_spl),
% 2.51/0.79 inference(backward_demodulation,[status(thm)],[f1573,f1442])).
% 2.51/0.79 fof(f1757,plain,(
% 2.51/0.79 sQ21_spl|~sQ0_spl|~sQ59_spl),
% 2.51/0.79 inference(split_clause,[status(thm)],[f1756,f132,f33,f1061])).
% 2.51/0.79 fof(f1761,plain,(
% 2.51/0.79 ~multiply(a,c)=identity|~sQ9_spl|sQ34_spl),
% 2.51/0.79 inference(backward_demodulation,[status(thm)],[f843,f328])).
% 2.51/0.79 fof(f1809,plain,(
% 2.51/0.79 ~identity=identity|~sQ59_spl|~sQ9_spl|sQ34_spl),
% 2.51/0.79 inference(forward_demodulation,[status(thm)],[f1445,f1761])).
% 2.51/0.79 fof(f1810,plain,(
% 2.51/0.79 $false|~sQ59_spl|~sQ9_spl|sQ34_spl),
% 2.51/0.79 inference(trivial_equality_resolution,[status(thm)],[f1809])).
% 2.51/0.79 fof(f1811,plain,(
% 2.51/0.79 ~sQ59_spl|~sQ9_spl|sQ34_spl),
% 2.51/0.79 inference(contradiction_clause,[status(thm)],[f1810])).
% 2.51/0.79 fof(f1842,plain,(
% 2.51/0.79 ~a=a|~sQ79_spl|~sQ2_spl|sQ72_spl),
% 2.51/0.79 inference(forward_demodulation,[status(thm)],[f1658,f1509])).
% 2.51/0.79 fof(f1843,plain,(
% 2.51/0.79 $false|~sQ79_spl|~sQ2_spl|sQ72_spl),
% 2.51/0.79 inference(trivial_equality_resolution,[status(thm)],[f1842])).
% 2.51/0.79 fof(f1844,plain,(
% 2.51/0.79 ~sQ79_spl|~sQ2_spl|sQ72_spl),
% 2.51/0.79 inference(contradiction_clause,[status(thm)],[f1843])).
% 2.51/0.79 fof(f1847,plain,(
% 2.51/0.79 multiply(a,b)=c|~sQ1_spl|~sQ2_spl|~sQ73_spl),
% 2.51/0.79 inference(forward_demodulation,[status(thm)],[f478,f1540])).
% 2.51/0.79 fof(f1901,plain,(
% 2.51/0.79 c=multiply(inverse(b),a)|~sQ76_spl),
% 2.51/0.79 inference(paramodulation,[status(thm)],[f1357,f166])).
% 2.51/0.79 fof(f1908,plain,(
% 2.51/0.79 c=multiply(b,a)|~sQ1_spl|~sQ76_spl),
% 2.51/0.79 inference(forward_demodulation,[status(thm)],[f478,f1901])).
% 2.51/0.79 fof(f1946,plain,(
% 2.51/0.79 b=multiply(inverse(a),c)|~sQ1_spl|~sQ2_spl|~sQ73_spl),
% 2.51/0.79 inference(paramodulation,[status(thm)],[f1847,f166])).
% 2.51/0.79 fof(f1947,plain,(
% 2.51/0.79 ![X0]: (multiply(c,X0)=multiply(a,multiply(b,X0))|~sQ1_spl|~sQ2_spl|~sQ73_spl)),
% 2.51/0.79 inference(paramodulation,[status(thm)],[f1847,f19])).
% 2.51/0.79 fof(f1957,plain,(
% 2.51/0.79 multiply(a,inverse(c))=inverse(b)|~sQ1_spl|~sQ76_spl),
% 2.51/0.79 inference(paramodulation,[status(thm)],[f1908,f576])).
% 2.51/0.79 fof(f1995,plain,(
% 2.51/0.79 a=multiply(c,b)|~sQ2_spl|~sQ73_spl),
% 2.51/0.79 inference(paramodulation,[status(thm)],[f1511,f1387])).
% 2.51/0.79 fof(f2015,plain,(
% 2.51/0.79 ![X0]: (c=identity|X0=a|X0=b|X0=identity|multiply(c,X0)=a|multiply(c,X0)=b|multiply(c,X0)=identity|~sQ2_spl)),
% 2.51/0.79 inference(paramodulation,[status(thm)],[f22,f1368])).
% 2.51/0.79 fof(f2037,plain,(
% 2.51/0.79 sQ23_spl|sQ75_spl|~sQ2_spl),
% 2.51/0.79 inference(split_clause,[status(thm)],[f2015,f140,f1194,f39])).
% 2.51/0.79 fof(f2067,plain,(
% 2.51/0.79 c=b|~sQ1_spl|~sQ60_spl),
% 2.51/0.79 inference(forward_demodulation,[status(thm)],[f478,f1270])).
% 2.51/0.79 fof(f2068,plain,(
% 2.51/0.79 $false|~sQ1_spl|~sQ60_spl),
% 2.51/0.79 inference(forward_subsumption_resolution,[status(thm)],[f2067,f26])).
% 2.51/0.79 fof(f2069,plain,(
% 2.51/0.79 ~sQ1_spl|~sQ60_spl),
% 2.51/0.79 inference(contradiction_clause,[status(thm)],[f2068])).
% 2.51/0.79 fof(f2078,plain,(
% 2.51/0.79 a=multiply(b,a)|~sQ1_spl|~sQ36_spl),
% 2.51/0.79 inference(forward_demodulation,[status(thm)],[f478,f366])).
% 2.51/0.79 fof(f2081,plain,(
% 2.51/0.79 a=b|~sQ2_spl|~sQ73_spl|~sQ66_spl),
% 2.51/0.79 inference(forward_demodulation,[status(thm)],[f1995,f1123])).
% 2.51/0.79 fof(f2082,plain,(
% 2.51/0.79 $false|~sQ2_spl|~sQ73_spl|~sQ66_spl),
% 2.51/0.79 inference(forward_subsumption_resolution,[status(thm)],[f2081,f23])).
% 2.51/0.79 fof(f2083,plain,(
% 2.51/0.79 ~sQ2_spl|~sQ73_spl|~sQ66_spl),
% 2.51/0.79 inference(contradiction_clause,[status(thm)],[f2082])).
% 2.51/0.79 fof(f2088,plain,(
% 2.51/0.79 a=identity|~sQ67_spl|~sQ2_spl|~sQ73_spl),
% 2.51/0.79 inference(backward_demodulation,[status(thm)],[f1126,f1995])).
% 2.51/0.79 fof(f2089,plain,(
% 2.51/0.79 sQ16_spl|~sQ67_spl|~sQ2_spl|~sQ73_spl),
% 2.51/0.79 inference(split_clause,[status(thm)],[f2088,f114,f1125,f39,f1187])).
% 2.51/0.79 fof(f2094,plain,(
% 2.51/0.79 c=b|~sQ2_spl|~sQ10_spl),
% 2.51/0.79 inference(forward_demodulation,[status(thm)],[f1387,f67])).
% 2.51/0.79 fof(f2095,plain,(
% 2.51/0.79 $false|~sQ2_spl|~sQ10_spl),
% 2.51/0.79 inference(forward_subsumption_resolution,[status(thm)],[f2094,f26])).
% 2.51/0.79 fof(f2096,plain,(
% 2.51/0.79 ~sQ2_spl|~sQ10_spl),
% 2.51/0.79 inference(contradiction_clause,[status(thm)],[f2095])).
% 2.51/0.79 fof(f2100,plain,(
% 2.51/0.79 c=a|~sQ2_spl|~sQ33_spl),
% 2.51/0.79 inference(forward_demodulation,[status(thm)],[f1387,f324])).
% 2.51/0.79 fof(f2101,plain,(
% 2.51/0.79 $false|~sQ2_spl|~sQ33_spl),
% 2.51/0.79 inference(forward_subsumption_resolution,[status(thm)],[f2100,f24])).
% 2.51/0.79 fof(f2102,plain,(
% 2.51/0.79 ~sQ2_spl|~sQ33_spl),
% 2.51/0.79 inference(contradiction_clause,[status(thm)],[f2101])).
% 2.51/0.79 fof(f2108,plain,(
% 2.51/0.79 ![X0]: (X0=multiply(a,multiply(b,X0))|~sQ70_spl)),
% 2.51/0.79 inference(paramodulation,[status(thm)],[f1149,f174])).
% 2.51/0.79 fof(f2109,plain,(
% 2.51/0.79 a=inverse(b)|~sQ70_spl),
% 2.51/0.79 inference(paramodulation,[status(thm)],[f1149,f383])).
% 2.51/0.79 fof(f2114,plain,(
% 2.51/0.79 ![X0]: (multiply(c,X0)=X0|~sQ70_spl|~sQ1_spl|~sQ2_spl|~sQ73_spl)),
% 2.51/0.79 inference(backward_demodulation,[status(thm)],[f2108,f1947])).
% 2.51/0.79 fof(f2115,plain,(
% 2.51/0.79 sQ30_spl|~sQ70_spl),
% 2.51/0.79 inference(split_clause,[status(thm)],[f2109,f292,f1148])).
% 2.51/0.79 fof(f2122,plain,(
% 2.51/0.79 ![X0]: (X0=identity|X0=a|X0=b|X0=identity|~sQ70_spl|~sQ1_spl|~sQ73_spl|~sQ2_spl)),
% 2.51/0.79 inference(backward_demodulation,[status(thm)],[f2114,f1368])).
% 2.51/0.79 fof(f2147,plain,(
% 2.51/0.79 sQ46_spl|~sQ70_spl|~sQ1_spl|~sQ73_spl|~sQ2_spl),
% 2.51/0.79 inference(split_clause,[status(thm)],[f2122,f689,f1148,f36,f1187,f39])).
% 2.51/0.79 fof(f2184,plain,(
% 2.51/0.79 multiply(a,inverse(b))=inverse(c)|~sQ2_spl|~sQ73_spl),
% 2.51/0.79 inference(paramodulation,[status(thm)],[f1511,f576])).
% 2.51/0.79 fof(f2190,plain,(
% 2.51/0.79 multiply(b,inverse(a))=inverse(c)|~sQ2_spl|~sQ73_spl),
% 2.51/0.79 inference(paramodulation,[status(thm)],[f1995,f576])).
% 2.51/0.79 fof(f2192,plain,(
% 2.51/0.79 ![X0]: (multiply(a,X0)=multiply(c,multiply(b,X0))|~sQ2_spl|~sQ73_spl)),
% 2.51/0.79 inference(paramodulation,[status(thm)],[f1995,f19])).
% 2.51/0.79 fof(f2208,plain,(
% 2.51/0.79 identity=b|~sQ2_spl|~sQ35_spl),
% 2.51/0.79 inference(forward_demodulation,[status(thm)],[f40,f331])).
% 2.51/0.79 fof(f2209,plain,(
% 2.51/0.79 $false|~sQ2_spl|~sQ35_spl),
% 2.51/0.79 inference(forward_subsumption_resolution,[status(thm)],[f2208,f27])).
% 2.51/0.79 fof(f2210,plain,(
% 2.51/0.79 ~sQ2_spl|~sQ35_spl),
% 2.51/0.79 inference(contradiction_clause,[status(thm)],[f2209])).
% 2.51/0.79 fof(f2258,plain,(
% 2.51/0.79 multiply(a,inverse(a))=inverse(b)|~sQ1_spl|~sQ36_spl),
% 2.51/0.79 inference(paramodulation,[status(thm)],[f2078,f576])).
% 2.51/0.79 fof(f2262,plain,(
% 2.51/0.79 b=identity|~sQ36_spl|~sQ1_spl),
% 2.51/0.79 inference(backward_demodulation,[status(thm)],[f2263,f478])).
% 2.51/0.79 fof(f2263,plain,(
% 2.51/0.79 identity=inverse(b)|~sQ1_spl|~sQ36_spl),
% 2.51/0.79 inference(forward_demodulation,[status(thm)],[f21,f2258])).
% 2.51/0.79 fof(f2265,plain,(
% 2.51/0.79 sQ14_spl|~sQ36_spl|~sQ1_spl),
% 2.51/0.79 inference(split_clause,[status(thm)],[f2262,f107,f342,f36])).
% 2.51/0.79 fof(f2280,plain,(
% 2.51/0.79 ~c=a|multiply(b,a)=a|multiply(b,a)=b|multiply(b,a)=identity|sQ36_spl),
% 2.51/0.79 inference(paramodulation,[status(thm)],[f22,f344])).
% 2.51/0.79 fof(f2281,plain,(
% 2.51/0.79 ~sQ21_spl|sQ36_spl|sQ37_spl|sQ38_spl),
% 2.51/0.79 inference(split_clause,[status(thm)],[f2280,f132,f342,f345,f348])).
% 2.51/0.79 fof(f2326,plain,(
% 2.51/0.79 b=multiply(c,c)|inverse(a)=a|inverse(a)=b|inverse(a)=identity|~sQ1_spl|~sQ2_spl|~sQ73_spl),
% 2.51/0.79 inference(paramodulation,[status(thm)],[f22,f1946])).
% 2.51/0.79 fof(f2342,plain,(
% 2.51/0.79 sQ35_spl|sQ69_spl|sQ70_spl|sQ71_spl|~sQ1_spl|~sQ2_spl|~sQ73_spl),
% 2.51/0.79 inference(split_clause,[status(thm)],[f2326,f330,f1145,f1148,f1151,f36,f39,f1187])).
% 2.51/0.79 fof(f2346,plain,(
% 2.51/0.79 multiply(b,inverse(a))=c|~sQ2_spl|~sQ73_spl),
% 2.51/0.79 inference(forward_demodulation,[status(thm)],[f1383,f2190])).
% 2.51/0.79 fof(f2347,plain,(
% 2.51/0.79 multiply(a,inverse(b))=c|~sQ2_spl|~sQ73_spl),
% 2.51/0.79 inference(forward_demodulation,[status(thm)],[f1383,f2184])).
% 2.51/0.79 fof(f2358,plain,(
% 2.51/0.79 multiply(a,c)=c|~sQ17_spl|~sQ2_spl|~sQ73_spl),
% 2.51/0.79 inference(backward_demodulation,[status(thm)],[f2359,f2347])).
% 2.51/0.79 fof(f2359,plain,(
% 2.51/0.79 c=inverse(b)|~sQ2_spl|~sQ73_spl|~sQ17_spl),
% 2.51/0.79 inference(forward_demodulation,[status(thm)],[f2346,f915])).
% 2.51/0.79 fof(f2360,plain,(
% 2.51/0.79 multiply(a,c)=b|~sQ2_spl|~sQ73_spl|~sQ17_spl),
% 2.51/0.79 inference(forward_demodulation,[status(thm)],[f2359,f931])).
% 2.51/0.79 fof(f2375,plain,(
% 2.51/0.79 b=c|~sQ17_spl|~sQ2_spl|~sQ73_spl),
% 2.51/0.79 inference(forward_demodulation,[status(thm)],[f2360,f2358])).
% 2.51/0.79 fof(f2376,plain,(
% 2.51/0.79 $false|~sQ17_spl|~sQ2_spl|~sQ73_spl),
% 2.51/0.79 inference(forward_subsumption_resolution,[status(thm)],[f2375,f26])).
% 2.51/0.79 fof(f2377,plain,(
% 2.51/0.79 ~sQ17_spl|~sQ2_spl|~sQ73_spl),
% 2.51/0.79 inference(contradiction_clause,[status(thm)],[f2376])).
% 2.51/0.79 fof(f2386,plain,(
% 2.51/0.79 a=multiply(b,c)|~sQ2_spl|~sQ73_spl|~sQ6_spl),
% 2.51/0.79 inference(forward_demodulation,[status(thm)],[f1995,f1603])).
% 2.51/0.79 fof(f2387,plain,(
% 2.51/0.79 $false|sQ7_spl|~sQ2_spl|~sQ73_spl|~sQ6_spl),
% 2.51/0.79 inference(forward_subsumption_resolution,[status(thm)],[f2386,f1246])).
% 2.51/0.79 fof(f2388,plain,(
% 2.51/0.79 sQ7_spl|~sQ2_spl|~sQ73_spl|~sQ6_spl),
% 2.51/0.79 inference(contradiction_clause,[status(thm)],[f2387])).
% 2.51/0.79 fof(f2403,plain,(
% 2.51/0.79 sQ41_spl|~sQ30_spl),
% 2.51/0.79 inference(split_clause,[status(thm)],[f313,f498,f292])).
% 2.51/0.79 fof(f2409,plain,(
% 2.51/0.79 ~multiply(c,multiply(b,b))=identity|~sQ6_spl|sQ8_spl),
% 2.51/0.79 inference(forward_demodulation,[status(thm)],[f1352,f61])).
% 2.51/0.79 fof(f2410,plain,(
% 2.51/0.79 ~multiply(a,b)=identity|~sQ2_spl|~sQ73_spl|~sQ6_spl|sQ8_spl),
% 2.51/0.79 inference(forward_demodulation,[status(thm)],[f2192,f2409])).
% 2.51/0.79 fof(f2416,plain,(
% 2.51/0.79 ~sQ41_spl|~sQ2_spl|~sQ73_spl|~sQ6_spl|sQ8_spl),
% 2.51/0.79 inference(split_clause,[status(thm)],[f2410,f498,f39,f1187,f53,f59])).
% 2.51/0.79 fof(f2418,plain,(
% 2.51/0.79 sQ70_spl|~sQ41_spl),
% 2.51/0.79 inference(split_clause,[status(thm)],[f1549,f1148,f498])).
% 2.51/0.79 fof(f2424,plain,(
% 2.51/0.79 multiply(b,identity)=c|~sQ71_spl|~sQ2_spl|~sQ73_spl),
% 2.51/0.79 inference(backward_demodulation,[status(thm)],[f1152,f2346])).
% 2.51/0.79 fof(f2429,plain,(
% 2.51/0.79 b=c|~sQ71_spl|~sQ2_spl|~sQ73_spl),
% 2.51/0.79 inference(forward_demodulation,[status(thm)],[f20,f2424])).
% 2.51/0.79 fof(f2430,plain,(
% 2.51/0.79 $false|~sQ71_spl|~sQ2_spl|~sQ73_spl),
% 2.51/0.79 inference(forward_subsumption_resolution,[status(thm)],[f2429,f26])).
% 2.51/0.79 fof(f2431,plain,(
% 2.51/0.79 ~sQ71_spl|~sQ2_spl|~sQ73_spl),
% 2.51/0.79 inference(contradiction_clause,[status(thm)],[f2430])).
% 2.51/0.79 fof(f2468,plain,(
% 2.51/0.79 sQ78_spl|~sQ60_spl),
% 2.51/0.79 inference(split_clause,[status(thm)],[f1273,f1362,f1064])).
% 2.51/0.79 fof(f2469,plain,(
% 2.51/0.79 multiply(b,a)=identity|~sQ60_spl|~sQ74_spl),
% 2.51/0.79 inference(backward_demodulation,[status(thm)],[f1065,f1191])).
% 2.51/0.79 fof(f2474,plain,(
% 2.51/0.79 c=a|~sQ38_spl|~sQ60_spl),
% 2.51/0.79 inference(forward_demodulation,[status(thm)],[f868,f1270])).
% 2.51/0.79 fof(f2475,plain,(
% 2.51/0.79 $false|~sQ38_spl|~sQ60_spl),
% 2.51/0.79 inference(forward_subsumption_resolution,[status(thm)],[f2474,f24])).
% 2.51/0.79 fof(f2476,plain,(
% 2.51/0.79 ~sQ38_spl|~sQ60_spl),
% 2.51/0.79 inference(contradiction_clause,[status(thm)],[f2475])).
% 2.51/0.79 fof(f2478,plain,(
% 2.51/0.79 sQ38_spl|~sQ60_spl|~sQ74_spl),
% 2.51/0.79 inference(split_clause,[status(thm)],[f2469,f348,f1064,f1190])).
% 2.51/0.79 fof(f2496,plain,(
% 2.51/0.79 ![X0]: (multiply(b,X0)=multiply(a,multiply(c,X0))|~sQ60_spl|~sQ17_spl)),
% 2.51/0.79 inference(forward_demodulation,[status(thm)],[f1270,f983])).
% 2.51/0.79 fof(f2514,plain,(
% 2.51/0.79 multiply(b,a)=b|~sQ60_spl|~sQ73_spl),
% 2.51/0.79 inference(forward_demodulation,[status(thm)],[f1065,f1188])).
% 2.51/0.79 fof(f2515,plain,(
% 2.51/0.79 $false|sQ37_spl|~sQ60_spl|~sQ73_spl),
% 2.51/0.79 inference(forward_subsumption_resolution,[status(thm)],[f2514,f347])).
% 2.51/0.79 fof(f2516,plain,(
% 2.51/0.79 sQ37_spl|~sQ60_spl|~sQ73_spl),
% 2.51/0.79 inference(contradiction_clause,[status(thm)],[f2515])).
% 2.51/0.79 fof(f2526,plain,(
% 2.51/0.79 ![X0]: (~multiply(a,X0)=b|X0=a|X0=b|X0=identity|~sQ9_spl|sQ10_spl)),
% 2.51/0.79 inference(backward_demodulation,[status(thm)],[f843,f322])).
% 2.51/0.79 fof(f2534,plain,(
% 2.51/0.79 ![X0]: (X0=a|X0=b|X0=identity|~sQ57_spl|~sQ9_spl|sQ10_spl)),
% 2.51/0.79 inference(forward_subsumption_resolution,[status(thm)],[f2526,f1074])).
% 2.51/0.79 fof(f2536,plain,(
% 2.51/0.79 multiply(b,a)=a|~sQ60_spl|~sQ72_spl),
% 2.51/0.79 inference(forward_demodulation,[status(thm)],[f1065,f1185])).
% 2.51/0.79 fof(f2537,plain,(
% 2.51/0.79 sQ36_spl|~sQ60_spl|~sQ72_spl),
% 2.51/0.79 inference(split_clause,[status(thm)],[f1255,f342,f1064,f1184])).
% 2.51/0.79 fof(f2568,plain,(
% 2.51/0.79 sQ20_spl|~sQ57_spl|~sQ9_spl|sQ10_spl),
% 2.51/0.79 inference(split_clause,[status(thm)],[f2534,f129,f994,f63,f66])).
% 2.51/0.79 fof(f2580,plain,(
% 2.51/0.79 ~multiply(a,multiply(c,c))=identity|~sQ9_spl|sQ11_spl),
% 2.51/0.79 inference(forward_demodulation,[status(thm)],[f843,f71])).
% 2.51/0.79 fof(f2581,plain,(
% 2.51/0.79 ~multiply(b,c)=identity|~sQ60_spl|~sQ17_spl|~sQ9_spl|sQ11_spl),
% 2.51/0.79 inference(forward_demodulation,[status(thm)],[f2496,f2580])).
% 2.51/0.79 fof(f2582,plain,(
% 2.51/0.79 ~identity=identity|~sQ78_spl|~sQ60_spl|~sQ17_spl|~sQ9_spl|sQ11_spl),
% 2.51/0.79 inference(forward_demodulation,[status(thm)],[f1363,f2581])).
% 2.51/0.79 fof(f2583,plain,(
% 2.51/0.79 $false|~sQ78_spl|~sQ60_spl|~sQ17_spl|~sQ9_spl|sQ11_spl),
% 2.51/0.79 inference(trivial_equality_resolution,[status(thm)],[f2582])).
% 2.51/0.79 fof(f2584,plain,(
% 2.51/0.79 ~sQ78_spl|~sQ60_spl|~sQ17_spl|~sQ9_spl|sQ11_spl),
% 2.51/0.79 inference(contradiction_clause,[status(thm)],[f2583])).
% 2.51/0.79 fof(f2613,plain,(
% 2.51/0.79 c=b|~sQ70_spl|~sQ59_spl),
% 2.51/0.79 inference(backward_demodulation,[status(thm)],[f1149,f1442])).
% 2.51/0.79 fof(f2638,plain,(
% 2.51/0.79 $false|~sQ70_spl|~sQ59_spl),
% 2.51/0.79 inference(forward_subsumption_resolution,[status(thm)],[f2613,f26])).
% 2.51/0.79 fof(f2639,plain,(
% 2.51/0.79 ~sQ70_spl|~sQ59_spl),
% 2.51/0.79 inference(contradiction_clause,[status(thm)],[f2638])).
% 2.51/0.79 fof(f2724,plain,(
% 2.51/0.79 ~multiply(a,c)=identity|~sQ4_spl|sQ5_spl),
% 2.51/0.79 inference(forward_demodulation,[status(thm)],[f47,f51])).
% 2.51/0.79 fof(f2725,plain,(
% 2.51/0.79 ~identity=identity|~sQ59_spl|~sQ4_spl|sQ5_spl),
% 2.51/0.79 inference(forward_demodulation,[status(thm)],[f1445,f2724])).
% 2.51/0.79 fof(f2726,plain,(
% 2.51/0.79 $false|~sQ59_spl|~sQ4_spl|sQ5_spl),
% 2.51/0.79 inference(trivial_equality_resolution,[status(thm)],[f2725])).
% 2.51/0.79 fof(f2727,plain,(
% 2.51/0.79 ~sQ59_spl|~sQ4_spl|sQ5_spl),
% 2.51/0.79 inference(contradiction_clause,[status(thm)],[f2726])).
% 2.51/0.79 fof(f2790,plain,(
% 2.51/0.79 ![X0]: (inverse(X0)=a|X0=a|X0=b|X0=identity|~sQ59_spl)),
% 2.51/0.79 inference(paramodulation,[status(thm)],[f22,f1062])).
% 2.51/0.79 fof(f2879,plain,(
% 2.51/0.79 a=multiply(inverse(a),a)|~sQ24_spl),
% 2.51/0.79 inference(paramodulation,[status(thm)],[f191,f166])).
% 2.51/0.79 fof(f2884,plain,(
% 2.51/0.79 a=identity|~sQ24_spl),
% 2.51/0.79 inference(forward_demodulation,[status(thm)],[f18,f2879])).
% 2.51/0.79 fof(f2885,plain,(
% 2.51/0.79 $false|~sQ24_spl),
% 2.51/0.79 inference(forward_subsumption_resolution,[status(thm)],[f2884,f25])).
% 2.51/0.79 fof(f2886,plain,(
% 2.51/0.79 ~sQ24_spl),
% 2.51/0.79 inference(contradiction_clause,[status(thm)],[f2885])).
% 2.51/0.79 fof(f2964,plain,(
% 2.51/0.79 multiply(b,inverse(c))=inverse(b)|~sQ6_spl),
% 2.51/0.79 inference(paramodulation,[status(thm)],[f54,f576])).
% 2.51/0.79 fof(f2986,plain,(
% 2.51/0.79 multiply(a,inverse(a))=inverse(b)|~sQ60_spl|~sQ72_spl),
% 2.51/0.79 inference(paramodulation,[status(thm)],[f2536,f576])).
% 2.51/0.79 fof(f2990,plain,(
% 2.51/0.79 c=identity|~sQ72_spl|~sQ60_spl),
% 2.51/0.79 inference(backward_demodulation,[status(thm)],[f2991,f1270])).
% 2.51/0.79 fof(f2991,plain,(
% 2.51/0.79 identity=inverse(b)|~sQ60_spl|~sQ72_spl),
% 2.51/0.79 inference(forward_demodulation,[status(thm)],[f21,f2986])).
% 2.51/0.79 fof(f2993,plain,(
% 2.51/0.79 sQ23_spl|~sQ72_spl|~sQ60_spl),
% 2.51/0.79 inference(split_clause,[status(thm)],[f2990,f140,f1184,f1064])).
% 2.51/0.79 fof(f2997,plain,(
% 2.51/0.79 ~b=b|~sQ60_spl|~sQ6_spl|sQ35_spl),
% 2.51/0.79 inference(forward_demodulation,[status(thm)],[f1402,f332])).
% 2.51/0.79 fof(f2998,plain,(
% 2.51/0.79 $false|~sQ60_spl|~sQ6_spl|sQ35_spl),
% 2.51/0.79 inference(trivial_equality_resolution,[status(thm)],[f2997])).
% 2.51/0.79 fof(f2999,plain,(
% 2.51/0.79 ~sQ60_spl|~sQ6_spl|sQ35_spl),
% 2.51/0.79 inference(contradiction_clause,[status(thm)],[f2998])).
% 2.51/0.79 fof(f3003,plain,(
% 2.51/0.79 multiply(a,c)=c|~sQ34_spl|~sQ9_spl|~sQ4_spl),
% 2.51/0.79 inference(backward_demodulation,[status(thm)],[f846,f47])).
% 2.51/0.79 fof(f3042,plain,(
% 2.51/0.79 identity=c|~sQ34_spl|~sQ9_spl|~sQ4_spl),
% 2.51/0.79 inference(forward_demodulation,[status(thm)],[f857,f3003])).
% 2.51/0.79 fof(f3043,plain,(
% 2.51/0.79 $false|~sQ34_spl|~sQ9_spl|~sQ4_spl),
% 2.51/0.79 inference(forward_subsumption_resolution,[status(thm)],[f3042,f28])).
% 2.51/0.79 fof(f3044,plain,(
% 2.51/0.79 ~sQ34_spl|~sQ9_spl|~sQ4_spl),
% 2.51/0.79 inference(contradiction_clause,[status(thm)],[f3043])).
% 2.51/0.79 fof(f3051,plain,(
% 2.51/0.79 ~multiply(a,c)=identity|~sQ34_spl|~sQ9_spl|sQ29_spl),
% 2.51/0.79 inference(forward_demodulation,[status(thm)],[f846,f263])).
% 2.51/0.79 fof(f3052,plain,(
% 2.51/0.79 ~identity=identity|~sQ34_spl|~sQ9_spl|sQ29_spl),
% 2.51/0.79 inference(forward_demodulation,[status(thm)],[f857,f3051])).
% 2.51/0.79 fof(f3053,plain,(
% 2.51/0.79 $false|~sQ34_spl|~sQ9_spl|sQ29_spl),
% 2.51/0.79 inference(trivial_equality_resolution,[status(thm)],[f3052])).
% 2.51/0.79 fof(f3054,plain,(
% 2.51/0.79 ~sQ34_spl|~sQ9_spl|sQ29_spl),
% 2.51/0.79 inference(contradiction_clause,[status(thm)],[f3053])).
% 2.51/0.79 fof(f3063,plain,(
% 2.51/0.79 multiply(b,a)=inverse(b)|~sQ9_spl|~sQ34_spl|~sQ6_spl),
% 2.51/0.79 inference(forward_demodulation,[status(thm)],[f847,f2964])).
% 2.51/0.79 fof(f3106,plain,(
% 2.51/0.79 multiply(inverse(c),identity)=a|multiply(inverse(c),identity)=b|multiply(inverse(c),identity)=identity|sQ2_spl),
% 2.51/0.79 inference(resolution,[status(thm)],[f94,f174])).
% 2.51/0.79 fof(f3115,definition,(
% 2.51/0.79 sQ85_spl <=> (multiply(inverse(c),identity)=a)),
% 2.51/0.79 introduced(definition,[new_symbols(definition,[sQ85_spl])],[split_symbol_definition])).
% 2.51/0.79 fof(f3116,plain,(
% 2.51/0.79 multiply(inverse(c),identity)=a|~sQ85_spl),
% 2.51/0.79 inference(component_clause,[status(thm)],[f3115])).
% 2.51/0.79 fof(f3118,definition,(
% 2.51/0.79 sQ86_spl <=> (multiply(inverse(c),identity)=b)),
% 2.51/0.79 introduced(definition,[new_symbols(definition,[sQ86_spl])],[split_symbol_definition])).
% 2.51/0.79 fof(f3119,plain,(
% 2.51/0.79 multiply(inverse(c),identity)=b|~sQ86_spl),
% 2.51/0.79 inference(component_clause,[status(thm)],[f3118])).
% 2.51/0.79 fof(f3121,definition,(
% 2.51/0.79 sQ87_spl <=> (multiply(inverse(c),identity)=identity)),
% 2.51/0.79 introduced(definition,[new_symbols(definition,[sQ87_spl])],[split_symbol_definition])).
% 2.51/0.79 fof(f3122,plain,(
% 2.51/0.79 multiply(inverse(c),identity)=identity|~sQ87_spl),
% 2.51/0.79 inference(component_clause,[status(thm)],[f3121])).
% 2.51/0.79 fof(f3124,plain,(
% 2.51/0.79 sQ85_spl|sQ86_spl|sQ87_spl|sQ2_spl),
% 2.51/0.79 inference(split_clause,[status(thm)],[f3106,f3115,f3118,f3121,f39])).
% 2.51/0.79 fof(f3136,plain,(
% 2.51/0.79 sQ20_spl|~sQ34_spl|~sQ44_spl),
% 2.51/0.79 inference(split_clause,[status(thm)],[f818,f129,f326,f679])).
% 2.51/0.79 fof(f3137,plain,(
% 2.51/0.79 a=identity|~sQ87_spl|~sQ9_spl|~sQ34_spl),
% 2.51/0.79 inference(backward_demodulation,[status(thm)],[f3138,f847])).
% 2.51/0.79 fof(f3138,plain,(
% 2.51/0.79 inverse(c)=identity|~sQ87_spl),
% 2.51/0.79 inference(forward_demodulation,[status(thm)],[f20,f3122])).
% 2.51/0.79 fof(f3139,plain,(
% 2.51/0.79 sQ16_spl|~sQ87_spl|~sQ9_spl|~sQ34_spl),
% 2.51/0.79 inference(split_clause,[status(thm)],[f3137,f114,f3121,f63,f326])).
% 2.51/0.79 fof(f3140,plain,(
% 2.51/0.79 inverse(c)=a|~sQ85_spl),
% 2.51/0.79 inference(forward_demodulation,[status(thm)],[f20,f3116])).
% 2.51/0.79 fof(f3270,plain,(
% 2.51/0.79 ![X0]: (inverse(multiply(X0,c))=multiply(a,inverse(X0))|~sQ9_spl|~sQ34_spl)),
% 2.51/0.79 inference(paramodulation,[status(thm)],[f576,f855])).
% 2.51/0.79 fof(f3271,plain,(
% 2.51/0.79 inverse(c)=multiply(a,identity)|~sQ9_spl|~sQ34_spl),
% 2.51/0.79 inference(paramodulation,[status(thm)],[f21,f855])).
% 2.51/0.79 fof(f3458,plain,(
% 2.51/0.79 inverse(multiply(c,b))=multiply(b,a)|~sQ1_spl|~sQ85_spl),
% 2.51/0.79 inference(paramodulation,[status(thm)],[f3140,f1097])).
% 2.51/0.79 fof(f3460,plain,(
% 2.51/0.79 inverse(multiply(a,b))=multiply(b,c)|~sQ1_spl|~sQ9_spl|~sQ34_spl),
% 2.51/0.79 inference(paramodulation,[status(thm)],[f854,f1097])).
% 2.51/0.79 fof(f3544,plain,(
% 2.51/0.79 inverse(c)=b|~sQ86_spl),
% 2.51/0.79 inference(forward_demodulation,[status(thm)],[f20,f3119])).
% 2.51/0.79 fof(f3547,plain,(
% 2.51/0.79 b=multiply(a,identity)|~sQ86_spl|~sQ9_spl|~sQ34_spl),
% 2.51/0.79 inference(forward_demodulation,[status(thm)],[f3544,f3271])).
% 2.51/0.79 fof(f3548,plain,(
% 2.51/0.79 b=a|~sQ86_spl|~sQ9_spl|~sQ34_spl),
% 2.51/0.79 inference(forward_demodulation,[status(thm)],[f20,f3547])).
% 2.51/0.79 fof(f3549,plain,(
% 2.51/0.79 $false|~sQ86_spl|~sQ9_spl|~sQ34_spl),
% 2.51/0.79 inference(forward_subsumption_resolution,[status(thm)],[f3548,f23])).
% 2.51/0.79 fof(f3550,plain,(
% 2.51/0.79 ~sQ86_spl|~sQ9_spl|~sQ34_spl),
% 2.51/0.79 inference(contradiction_clause,[status(thm)],[f3549])).
% 2.51/0.79 fof(f3816,plain,(
% 2.51/0.79 multiply(a,identity)=a|multiply(a,identity)=b|multiply(a,identity)=identity|sQ2_spl|~sQ9_spl|~sQ34_spl),
% 2.51/0.79 inference(resolution,[status(thm)],[f94,f848])).
% 2.51/0.79 fof(f3831,definition,(
% 2.51/0.79 sQ93_spl <=> (multiply(a,identity)=a)),
% 2.51/0.79 introduced(definition,[new_symbols(definition,[sQ93_spl])],[split_symbol_definition])).
% 2.51/0.79 fof(f3834,definition,(
% 2.51/0.79 sQ94_spl <=> (multiply(a,identity)=b)),
% 2.51/0.79 introduced(definition,[new_symbols(definition,[sQ94_spl])],[split_symbol_definition])).
% 2.51/0.79 fof(f3835,plain,(
% 2.51/0.79 multiply(a,identity)=b|~sQ94_spl),
% 2.51/0.79 inference(component_clause,[status(thm)],[f3834])).
% 2.51/0.79 fof(f3837,definition,(
% 2.51/0.79 sQ95_spl <=> (multiply(a,identity)=identity)),
% 2.51/0.79 introduced(definition,[new_symbols(definition,[sQ95_spl])],[split_symbol_definition])).
% 2.51/0.79 fof(f3838,plain,(
% 2.51/0.79 multiply(a,identity)=identity|~sQ95_spl),
% 2.51/0.79 inference(component_clause,[status(thm)],[f3837])).
% 2.51/0.79 fof(f3840,plain,(
% 2.51/0.79 sQ93_spl|sQ94_spl|sQ95_spl|sQ2_spl|~sQ9_spl|~sQ34_spl),
% 2.51/0.79 inference(split_clause,[status(thm)],[f3816,f3831,f3834,f3837,f39,f63,f326])).
% 2.51/0.79 fof(f3852,plain,(
% 2.51/0.79 a=identity|~sQ95_spl),
% 2.51/0.79 inference(forward_demodulation,[status(thm)],[f20,f3838])).
% 2.51/0.79 fof(f3853,plain,(
% 2.51/0.79 $false|~sQ95_spl),
% 2.51/0.79 inference(forward_subsumption_resolution,[status(thm)],[f3852,f25])).
% 2.51/0.79 fof(f3854,plain,(
% 2.51/0.79 ~sQ95_spl),
% 2.51/0.79 inference(contradiction_clause,[status(thm)],[f3853])).
% 2.51/0.79 fof(f3855,plain,(
% 2.51/0.79 a=b|~sQ94_spl),
% 2.51/0.79 inference(forward_demodulation,[status(thm)],[f20,f3835])).
% 2.51/0.79 fof(f3856,plain,(
% 2.51/0.79 $false|~sQ94_spl),
% 2.51/0.79 inference(forward_subsumption_resolution,[status(thm)],[f3855,f23])).
% 2.51/0.79 fof(f3857,plain,(
% 2.51/0.79 ~sQ94_spl),
% 2.51/0.79 inference(contradiction_clause,[status(thm)],[f3856])).
% 2.51/0.79 fof(f3986,plain,(
% 2.51/0.79 a=multiply(b,c)|multiply(a,b)=a|multiply(a,b)=b|multiply(a,b)=identity|~sQ1_spl|~sQ9_spl|~sQ34_spl|~sQ59_spl),
% 2.51/0.81 inference(paramodulation,[status(thm)],[f2790,f3460])).
% 2.51/0.81 fof(f4019,plain,(
% 2.51/0.81 sQ76_spl|sQ39_spl|sQ40_spl|sQ41_spl|~sQ1_spl|~sQ9_spl|~sQ34_spl|~sQ59_spl),
% 2.51/0.81 inference(split_clause,[status(thm)],[f3986,f1356,f492,f495,f498,f36,f63,f326,f1061])).
% 2.51/0.81 fof(f4085,plain,(
% 2.51/0.81 inverse(b)=multiply(b,a)|~sQ9_spl|~sQ34_spl|~sQ40_spl|~sQ1_spl|~sQ85_spl),
% 2.51/0.81 inference(backward_demodulation,[status(thm)],[f858,f3458])).
% 2.51/0.81 fof(f4106,plain,(
% 2.51/0.81 b=multiply(b,a)|~sQ9_spl|~sQ34_spl|~sQ40_spl|~sQ1_spl|~sQ85_spl),
% 2.51/0.81 inference(forward_demodulation,[status(thm)],[f478,f4085])).
% 2.51/0.81 fof(f4107,plain,(
% 2.51/0.81 $false|sQ37_spl|~sQ9_spl|~sQ34_spl|~sQ40_spl|~sQ1_spl|~sQ85_spl),
% 2.51/0.81 inference(forward_subsumption_resolution,[status(thm)],[f4106,f347])).
% 2.51/0.81 fof(f4108,plain,(
% 2.51/0.81 sQ37_spl|~sQ9_spl|~sQ34_spl|~sQ40_spl|~sQ1_spl|~sQ85_spl),
% 2.51/0.81 inference(contradiction_clause,[status(thm)],[f4107])).
% 2.51/0.81 fof(f4177,plain,(
% 2.51/0.81 c=inverse(b)|multiply(b,a)=a|multiply(b,a)=b|multiply(b,a)=identity|~sQ9_spl|~sQ34_spl|~sQ6_spl),
% 2.51/0.81 inference(paramodulation,[status(thm)],[f22,f3063])).
% 2.51/0.81 fof(f4182,definition,(
% 2.51/0.81 sQ104_spl <=> (c=inverse(b))),
% 2.51/0.81 introduced(definition,[new_symbols(definition,[sQ104_spl])],[split_symbol_definition])).
% 2.51/0.81 fof(f4183,plain,(
% 2.51/0.81 c=inverse(b)|~sQ104_spl),
% 2.51/0.81 inference(component_clause,[status(thm)],[f4182])).
% 2.51/0.81 fof(f4185,plain,(
% 2.51/0.81 sQ104_spl|sQ36_spl|sQ37_spl|sQ38_spl|~sQ9_spl|~sQ34_spl|~sQ6_spl),
% 2.51/0.81 inference(split_clause,[status(thm)],[f4177,f4182,f342,f345,f348,f63,f326,f53])).
% 2.51/0.81 fof(f4207,plain,(
% 2.51/0.81 a=inverse(b)|~sQ36_spl|~sQ9_spl|~sQ34_spl|~sQ6_spl),
% 2.51/0.81 inference(forward_demodulation,[status(thm)],[f343,f3063])).
% 2.51/0.81 fof(f4210,plain,(
% 2.51/0.81 ~a=a|~sQ36_spl|~sQ9_spl|~sQ34_spl|~sQ6_spl|sQ30_spl),
% 2.51/0.81 inference(forward_demodulation,[status(thm)],[f4207,f294])).
% 2.51/0.81 fof(f4211,plain,(
% 2.51/0.81 $false|~sQ36_spl|~sQ9_spl|~sQ34_spl|~sQ6_spl|sQ30_spl),
% 2.51/0.81 inference(trivial_equality_resolution,[status(thm)],[f4210])).
% 2.51/0.81 fof(f4212,plain,(
% 2.51/0.81 ~sQ36_spl|~sQ9_spl|~sQ34_spl|~sQ6_spl|sQ30_spl),
% 2.51/0.81 inference(contradiction_clause,[status(thm)],[f4211])).
% 2.51/0.81 fof(f4277,plain,(
% 2.51/0.81 b=inverse(c)|~sQ104_spl),
% 2.51/0.81 inference(paramodulation,[status(thm)],[f4183,f383])).
% 2.51/0.81 fof(f4297,plain,(
% 2.51/0.81 sQ60_spl|~sQ104_spl),
% 2.51/0.81 inference(split_clause,[status(thm)],[f4277,f1064,f4182])).
% 2.51/0.81 fof(f4322,plain,(
% 2.51/0.81 inverse(multiply(c,c))=inverse(b)|~sQ9_spl|~sQ34_spl|~sQ1_spl|~sQ76_spl),
% 2.51/0.81 inference(forward_demodulation,[status(thm)],[f3270,f1957])).
% 2.51/0.81 fof(f4323,plain,(
% 2.51/0.81 inverse(a)=inverse(b)|~sQ9_spl|~sQ34_spl|~sQ1_spl|~sQ76_spl),
% 2.51/0.81 inference(forward_demodulation,[status(thm)],[f64,f4322])).
% 2.51/0.81 fof(f4324,plain,(
% 2.51/0.81 c=inverse(b)|~sQ9_spl|~sQ34_spl|~sQ1_spl|~sQ76_spl),
% 2.51/0.81 inference(forward_demodulation,[status(thm)],[f854,f4323])).
% 2.51/0.81 fof(f4325,plain,(
% 2.51/0.81 c=b|~sQ9_spl|~sQ34_spl|~sQ1_spl|~sQ76_spl),
% 2.51/0.81 inference(forward_demodulation,[status(thm)],[f478,f4324])).
% 2.51/0.81 fof(f4326,plain,(
% 2.51/0.81 $false|~sQ9_spl|~sQ34_spl|~sQ1_spl|~sQ76_spl),
% 2.51/0.81 inference(forward_subsumption_resolution,[status(thm)],[f4325,f26])).
% 2.51/0.81 fof(f4327,plain,(
% 2.51/0.81 ~sQ9_spl|~sQ34_spl|~sQ1_spl|~sQ76_spl),
% 2.51/0.81 inference(contradiction_clause,[status(thm)],[f4326])).
% 2.51/0.81 fof(f4328,plain,(
% 2.51/0.81 $false),
% 2.51/0.81 inference(sat_refutation,[status(thm)],[f42,f52,f62,f72,f110,f117,f124,f128,f135,f139,f145,f147,f149,f193,f195,f204,f229,f239,f264,f274,f336,f381,f392,f395,f417,f427,f449,f504,f519,f555,f682,f697,f739,f776,f784,f800,f808,f819,f836,f860,f870,f873,f901,f902,f903,f904,f997,f1010,f1060,f1169,f1193,f1197,f1214,f1226,f1252,f1279,f1334,f1396,f1420,f1468,f1479,f1520,f1558,f1670,f1678,f1681,f1705,f1725,f1739,f1748,f1757,f1811,f1844,f2037,f2069,f2083,f2089,f2096,f2102,f2115,f2147,f2210,f2265,f2281,f2342,f2377,f2388,f2403,f2416,f2418,f2431,f2468,f2476,f2478,f2516,f2537,f2568,f2584,f2639,f2727,f2886,f2993,f2999,f3044,f3054,f3124,f3136,f3139,f3550,f3840,f3854,f3857,f4019,f4108,f4185,f4212,f4297,f4327])).
% 2.51/0.81 % SZS output end CNFRefutation for theBenchmark.p
% 2.51/0.82 % Elapsed time: 0.458199 seconds
% 2.51/0.82 % CPU time: 3.197891 seconds
% 2.51/0.82 % Total memory used: 136.157 MB
% 2.51/0.82 % Net memory used: 130.828 MB
%------------------------------------------------------------------------------