%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GRP238-1 : TPTP v9.3.1. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n017.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:36:18 PM UTC 2026
% Result : Unsatisfiable 0.13s 0.39s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP238-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.36 % Computer : n017.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Sun Sep 20 20:02:26 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.37 % Drodi V4.1.1
% 0.13/0.39 % Refutation found
% 0.13/0.39 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.13/0.39 % SZS output start CNFRefutation for theBenchmark
% 0.13/0.39 fof(f1,axiom,(
% 0.13/0.39 (![X]: (multiply(identity,X) = X ))),
% 0.13/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.39 fof(f2,axiom,(
% 0.13/0.39 (![X]: (multiply(inverse(X),X) = identity ))),
% 0.13/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.39 fof(f3,axiom,(
% 0.13/0.39 (![X,Y,Z]: (multiply(multiply(X,Y),Z) = multiply(X,multiply(Y,Z)) ))),
% 0.13/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.39 fof(f4,negated_conjecture,(
% 0.13/0.39 ( inverse(sk_c11) = sk_c10| multiply(sk_c4,sk_c5) = sk_c11 ) ),
% 0.13/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.39 fof(f5,negated_conjecture,(
% 0.13/0.39 ( inverse(sk_c11) = sk_c10| inverse(sk_c4) = sk_c5 ) ),
% 0.13/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.39 fof(f6,negated_conjecture,(
% 0.13/0.39 ( inverse(sk_c11) = sk_c10| multiply(sk_c5,sk_c10) = sk_c11 ) ),
% 0.13/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.39 fof(f7,negated_conjecture,(
% 0.13/0.39 ( inverse(sk_c11) = sk_c10| inverse(sk_c6) = sk_c11 ) ),
% 0.13/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.39 fof(f8,negated_conjecture,(
% 0.13/0.39 ( inverse(sk_c11) = sk_c10| multiply(sk_c6,sk_c10) = sk_c11 ) ),
% 0.13/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.39 fof(f9,negated_conjecture,(
% 0.13/0.39 ( inverse(sk_c11) = sk_c10| multiply(sk_c7,sk_c8) = sk_c10 ) ),
% 0.13/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.39 fof(f10,negated_conjecture,(
% 0.13/0.39 ( inverse(sk_c11) = sk_c10| inverse(sk_c7) = sk_c8 ) ),
% 0.13/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.39 fof(f11,negated_conjecture,(
% 0.13/0.39 ( inverse(sk_c11) = sk_c10| multiply(sk_c8,sk_c11) = sk_c10 ) ),
% 0.13/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.39 fof(f14,negated_conjecture,(
% 0.13/0.39 ( inverse(sk_c1) = sk_c11| multiply(sk_c4,sk_c5) = sk_c11 ) ),
% 0.13/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.39 fof(f15,negated_conjecture,(
% 0.13/0.39 ( inverse(sk_c1) = sk_c11| inverse(sk_c4) = sk_c5 ) ),
% 0.13/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.39 fof(f16,negated_conjecture,(
% 0.13/0.39 ( inverse(sk_c1) = sk_c11| multiply(sk_c5,sk_c10) = sk_c11 ) ),
% 0.13/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.39 fof(f17,negated_conjecture,(
% 0.13/0.39 ( inverse(sk_c1) = sk_c11| inverse(sk_c6) = sk_c11 ) ),
% 0.13/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.39 fof(f18,negated_conjecture,(
% 0.13/0.39 ( inverse(sk_c1) = sk_c11| multiply(sk_c6,sk_c10) = sk_c11 ) ),
% 0.13/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.39 fof(f19,negated_conjecture,(
% 0.13/0.39 ( inverse(sk_c1) = sk_c11| multiply(sk_c7,sk_c8) = sk_c10 ) ),
% 0.13/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.39 fof(f20,negated_conjecture,(
% 0.13/0.39 ( inverse(sk_c1) = sk_c11| inverse(sk_c7) = sk_c8 ) ),
% 0.13/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.39 fof(f21,negated_conjecture,(
% 0.13/0.39 ( inverse(sk_c1) = sk_c11| multiply(sk_c8,sk_c11) = sk_c10 ) ),
% 0.13/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.39 fof(f22,negated_conjecture,(
% 0.13/0.39 ( inverse(sk_c1) = sk_c11| inverse(sk_c9) = sk_c10 ) ),
% 0.13/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.39 fof(f24,negated_conjecture,(
% 0.13/0.39 ( multiply(sk_c1,sk_c10) = sk_c11| multiply(sk_c4,sk_c5) = sk_c11 ) ),
% 0.13/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.39 fof(f25,negated_conjecture,(
% 0.13/0.39 ( multiply(sk_c1,sk_c10) = sk_c11| inverse(sk_c4) = sk_c5 ) ),
% 0.13/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.39 fof(f34,negated_conjecture,(
% 0.13/0.39 ( multiply(sk_c11,sk_c3) = sk_c10| multiply(sk_c4,sk_c5) = sk_c11 ) ),
% 0.13/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.39 fof(f35,negated_conjecture,(
% 0.13/0.39 ( multiply(sk_c11,sk_c3) = sk_c10| inverse(sk_c4) = sk_c5 ) ),
% 0.13/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.39 fof(f42,negated_conjecture,(
% 0.13/0.39 ( multiply(sk_c11,sk_c3) = sk_c10| inverse(sk_c9) = sk_c10 ) ),
% 0.13/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.39 fof(f43,negated_conjecture,(
% 0.13/0.39 ( multiply(sk_c11,sk_c3) = sk_c10| multiply(sk_c9,sk_c11) = sk_c10 ) ),
% 0.13/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.39 fof(f44,negated_conjecture,(
% 0.13/0.39 ( multiply(sk_c2,sk_c11) = sk_c3| multiply(sk_c4,sk_c5) = sk_c11 ) ),
% 0.13/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.39 fof(f45,negated_conjecture,(
% 0.13/0.39 ( multiply(sk_c2,sk_c11) = sk_c3| inverse(sk_c4) = sk_c5 ) ),
% 0.13/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.39 fof(f52,negated_conjecture,(
% 0.13/0.39 ( multiply(sk_c2,sk_c11) = sk_c3| inverse(sk_c9) = sk_c10 ) ),
% 0.13/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.39 fof(f53,negated_conjecture,(
% 0.13/0.39 ( multiply(sk_c2,sk_c11) = sk_c3| multiply(sk_c9,sk_c11) = sk_c10 ) ),
% 0.13/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.39 fof(f54,negated_conjecture,(
% 0.13/0.39 ( inverse(sk_c2) = sk_c11| multiply(sk_c4,sk_c5) = sk_c11 ) ),
% 0.13/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.39 fof(f55,negated_conjecture,(
% 0.13/0.39 ( inverse(sk_c2) = sk_c11| inverse(sk_c4) = sk_c5 ) ),
% 0.13/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.39 fof(f62,negated_conjecture,(
% 0.13/0.39 ( inverse(sk_c2) = sk_c11| inverse(sk_c9) = sk_c10 ) ),
% 0.13/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.39 fof(f63,negated_conjecture,(
% 0.13/0.39 ( inverse(sk_c2) = sk_c11| multiply(sk_c9,sk_c11) = sk_c10 ) ),
% 0.13/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.39 fof(f64,negated_conjecture,(
% 0.13/0.39 (![X4,X5,X6,X2,X1,X3,X7,X8,X9]: (( inverse(sk_c11) != sk_c10| inverse(X4) != sk_c11| multiply(X4,sk_c10) != sk_c11| multiply(sk_c11,X5) != sk_c10| multiply(X6,sk_c11) != X5| inverse(X6) != sk_c11| multiply(X2,X1) != sk_c11| inverse(X2) != X1| multiply(X1,sk_c10) != sk_c11| inverse(X3) != sk_c11| multiply(X3,sk_c10) != sk_c11| multiply(X7,X8) != sk_c10| inverse(X7) != X8| multiply(X8,sk_c11) != sk_c10| inverse(X9) != sk_c10| multiply(X9,sk_c11) != sk_c10 ) ))),
% 0.13/0.39 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.13/0.39 fof(f65,plain,(
% 0.13/0.39 ![X0]: (multiply(identity,X0)=X0)),
% 0.13/0.39 inference(cnf_transformation,[status(thm)],[f1])).
% 0.13/0.39 fof(f66,plain,(
% 0.13/0.39 ![X0]: (multiply(inverse(X0),X0)=identity)),
% 0.13/0.39 inference(cnf_transformation,[status(thm)],[f2])).
% 0.13/0.39 fof(f67,plain,(
% 0.13/0.39 ![X0,X1,X2]: (multiply(multiply(X0,X1),X2)=multiply(X0,multiply(X1,X2)))),
% 0.13/0.39 inference(cnf_transformation,[status(thm)],[f3])).
% 0.13/0.39 fof(f68,plain,(
% 0.13/0.39 inverse(sk_c11)=sk_c10|multiply(sk_c4,sk_c5)=sk_c11),
% 0.13/0.39 inference(cnf_transformation,[status(thm)],[f4])).
% 0.13/0.39 fof(f69,plain,(
% 0.13/0.39 inverse(sk_c11)=sk_c10|inverse(sk_c4)=sk_c5),
% 0.13/0.39 inference(cnf_transformation,[status(thm)],[f5])).
% 0.13/0.39 fof(f70,plain,(
% 0.13/0.39 inverse(sk_c11)=sk_c10|multiply(sk_c5,sk_c10)=sk_c11),
% 0.13/0.39 inference(cnf_transformation,[status(thm)],[f6])).
% 0.13/0.39 fof(f71,plain,(
% 0.13/0.39 inverse(sk_c11)=sk_c10|inverse(sk_c6)=sk_c11),
% 0.13/0.39 inference(cnf_transformation,[status(thm)],[f7])).
% 0.13/0.39 fof(f72,plain,(
% 0.13/0.39 inverse(sk_c11)=sk_c10|multiply(sk_c6,sk_c10)=sk_c11),
% 0.13/0.39 inference(cnf_transformation,[status(thm)],[f8])).
% 0.13/0.39 fof(f73,plain,(
% 0.13/0.39 inverse(sk_c11)=sk_c10|multiply(sk_c7,sk_c8)=sk_c10),
% 0.13/0.39 inference(cnf_transformation,[status(thm)],[f9])).
% 0.13/0.39 fof(f74,plain,(
% 0.13/0.39 inverse(sk_c11)=sk_c10|inverse(sk_c7)=sk_c8),
% 0.13/0.39 inference(cnf_transformation,[status(thm)],[f10])).
% 0.13/0.39 fof(f75,plain,(
% 0.13/0.39 inverse(sk_c11)=sk_c10|multiply(sk_c8,sk_c11)=sk_c10),
% 0.13/0.39 inference(cnf_transformation,[status(thm)],[f11])).
% 0.13/0.39 fof(f78,plain,(
% 0.13/0.39 inverse(sk_c1)=sk_c11|multiply(sk_c4,sk_c5)=sk_c11),
% 0.13/0.39 inference(cnf_transformation,[status(thm)],[f14])).
% 0.13/0.39 fof(f79,plain,(
% 0.13/0.39 inverse(sk_c1)=sk_c11|inverse(sk_c4)=sk_c5),
% 0.13/0.39 inference(cnf_transformation,[status(thm)],[f15])).
% 0.13/0.39 fof(f80,plain,(
% 0.13/0.39 inverse(sk_c1)=sk_c11|multiply(sk_c5,sk_c10)=sk_c11),
% 0.13/0.39 inference(cnf_transformation,[status(thm)],[f16])).
% 0.13/0.39 fof(f81,plain,(
% 0.13/0.39 inverse(sk_c1)=sk_c11|inverse(sk_c6)=sk_c11),
% 0.13/0.39 inference(cnf_transformation,[status(thm)],[f17])).
% 0.13/0.39 fof(f82,plain,(
% 0.13/0.39 inverse(sk_c1)=sk_c11|multiply(sk_c6,sk_c10)=sk_c11),
% 0.13/0.39 inference(cnf_transformation,[status(thm)],[f18])).
% 0.13/0.39 fof(f83,plain,(
% 0.13/0.39 inverse(sk_c1)=sk_c11|multiply(sk_c7,sk_c8)=sk_c10),
% 0.13/0.39 inference(cnf_transformation,[status(thm)],[f19])).
% 0.13/0.39 fof(f84,plain,(
% 0.13/0.39 inverse(sk_c1)=sk_c11|inverse(sk_c7)=sk_c8),
% 0.13/0.39 inference(cnf_transformation,[status(thm)],[f20])).
% 0.13/0.39 fof(f85,plain,(
% 0.13/0.39 inverse(sk_c1)=sk_c11|multiply(sk_c8,sk_c11)=sk_c10),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f21])).
% 0.13/0.40 fof(f86,plain,(
% 0.13/0.40 inverse(sk_c1)=sk_c11|inverse(sk_c9)=sk_c10),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f22])).
% 0.13/0.40 fof(f88,plain,(
% 0.13/0.40 multiply(sk_c1,sk_c10)=sk_c11|multiply(sk_c4,sk_c5)=sk_c11),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f24])).
% 0.13/0.40 fof(f89,plain,(
% 0.13/0.40 multiply(sk_c1,sk_c10)=sk_c11|inverse(sk_c4)=sk_c5),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f25])).
% 0.13/0.40 fof(f98,plain,(
% 0.13/0.40 multiply(sk_c11,sk_c3)=sk_c10|multiply(sk_c4,sk_c5)=sk_c11),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f34])).
% 0.13/0.40 fof(f99,plain,(
% 0.13/0.40 multiply(sk_c11,sk_c3)=sk_c10|inverse(sk_c4)=sk_c5),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f35])).
% 0.13/0.40 fof(f106,plain,(
% 0.13/0.40 multiply(sk_c11,sk_c3)=sk_c10|inverse(sk_c9)=sk_c10),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f42])).
% 0.13/0.40 fof(f107,plain,(
% 0.13/0.40 multiply(sk_c11,sk_c3)=sk_c10|multiply(sk_c9,sk_c11)=sk_c10),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f43])).
% 0.13/0.40 fof(f108,plain,(
% 0.13/0.40 multiply(sk_c2,sk_c11)=sk_c3|multiply(sk_c4,sk_c5)=sk_c11),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f44])).
% 0.13/0.40 fof(f109,plain,(
% 0.13/0.40 multiply(sk_c2,sk_c11)=sk_c3|inverse(sk_c4)=sk_c5),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f45])).
% 0.13/0.40 fof(f116,plain,(
% 0.13/0.40 multiply(sk_c2,sk_c11)=sk_c3|inverse(sk_c9)=sk_c10),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f52])).
% 0.13/0.40 fof(f117,plain,(
% 0.13/0.40 multiply(sk_c2,sk_c11)=sk_c3|multiply(sk_c9,sk_c11)=sk_c10),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f53])).
% 0.13/0.40 fof(f118,plain,(
% 0.13/0.40 inverse(sk_c2)=sk_c11|multiply(sk_c4,sk_c5)=sk_c11),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f54])).
% 0.13/0.40 fof(f119,plain,(
% 0.13/0.40 inverse(sk_c2)=sk_c11|inverse(sk_c4)=sk_c5),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f55])).
% 0.13/0.40 fof(f126,plain,(
% 0.13/0.40 inverse(sk_c2)=sk_c11|inverse(sk_c9)=sk_c10),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f62])).
% 0.13/0.40 fof(f127,plain,(
% 0.13/0.40 inverse(sk_c2)=sk_c11|multiply(sk_c9,sk_c11)=sk_c10),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f63])).
% 0.13/0.40 fof(f128,plain,(
% 0.13/0.40 ![X9]: (((![X8]: ((![X7]: (((![X3]: (((![X1]: ((![X2]: (((![X6]: ((![X5]: (((![X4]: ((~inverse(sk_c11)=sk_c10|~inverse(X4)=sk_c11)|~multiply(X4,sk_c10)=sk_c11))|~multiply(sk_c11,X5)=sk_c10)|~multiply(X6,sk_c11)=X5))|~inverse(X6)=sk_c11))|~multiply(X2,X1)=sk_c11)|~inverse(X2)=X1))|~multiply(X1,sk_c10)=sk_c11))|~inverse(X3)=sk_c11)|~multiply(X3,sk_c10)=sk_c11))|~multiply(X7,X8)=sk_c10)|~inverse(X7)=X8))|~multiply(X8,sk_c11)=sk_c10))|~inverse(X9)=sk_c10)|~multiply(X9,sk_c11)=sk_c10)),
% 0.13/0.40 inference(miniscoping,[status(thm)],[f64])).
% 0.13/0.40 fof(f129,plain,(
% 0.13/0.40 ![X0,X1,X2,X3,X4,X5,X6,X7,X8]: (~inverse(sk_c11)=sk_c10|~inverse(X0)=sk_c11|~multiply(X0,sk_c10)=sk_c11|~multiply(sk_c11,X1)=sk_c10|~multiply(X2,sk_c11)=X1|~inverse(X2)=sk_c11|~multiply(X3,X4)=sk_c11|~inverse(X3)=X4|~multiply(X4,sk_c10)=sk_c11|~inverse(X5)=sk_c11|~multiply(X5,sk_c10)=sk_c11|~multiply(X6,X7)=sk_c10|~inverse(X6)=X7|~multiply(X7,sk_c11)=sk_c10|~inverse(X8)=sk_c10|~multiply(X8,sk_c11)=sk_c10)),
% 0.13/0.40 inference(cnf_transformation,[status(thm)],[f128])).
% 0.13/0.40 fof(f130,definition,(
% 0.13/0.40 sQ0_spl <=> (inverse(sk_c11)=sk_c10)),
% 0.13/0.40 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.13/0.40 fof(f131,plain,(
% 0.13/0.40 inverse(sk_c11)=sk_c10|~sQ0_spl),
% 0.13/0.40 inference(component_clause,[status(thm)],[f130])).
% 0.13/0.40 fof(f132,plain,(
% 0.13/0.40 ~inverse(sk_c11)=sk_c10|sQ0_spl),
% 0.13/0.40 inference(component_clause,[status(thm)],[f130])).
% 0.13/0.40 fof(f133,definition,(
% 0.13/0.40 sQ1_spl <=> (multiply(sk_c4,sk_c5)=sk_c11)),
% 0.13/0.40 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.13/0.40 fof(f134,plain,(
% 0.13/0.40 multiply(sk_c4,sk_c5)=sk_c11|~sQ1_spl),
% 0.13/0.40 inference(component_clause,[status(thm)],[f133])).
% 0.13/0.40 fof(f136,plain,(
% 0.13/0.40 sQ0_spl|sQ1_spl),
% 0.13/0.40 inference(split_clause,[status(thm)],[f68,f130,f133])).
% 0.13/0.40 fof(f137,definition,(
% 0.13/0.40 sQ2_spl <=> (inverse(sk_c4)=sk_c5)),
% 0.13/0.40 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.13/0.40 fof(f138,plain,(
% 0.13/0.40 inverse(sk_c4)=sk_c5|~sQ2_spl),
% 0.13/0.40 inference(component_clause,[status(thm)],[f137])).
% 0.13/0.40 fof(f140,plain,(
% 0.13/0.40 sQ0_spl|sQ2_spl),
% 0.13/0.40 inference(split_clause,[status(thm)],[f69,f130,f137])).
% 0.13/0.40 fof(f141,definition,(
% 0.13/0.40 sQ3_spl <=> (multiply(sk_c5,sk_c10)=sk_c11)),
% 0.13/0.40 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.13/0.40 fof(f142,plain,(
% 0.13/0.40 multiply(sk_c5,sk_c10)=sk_c11|~sQ3_spl),
% 0.13/0.40 inference(component_clause,[status(thm)],[f141])).
% 0.13/0.40 fof(f144,plain,(
% 0.13/0.40 sQ0_spl|sQ3_spl),
% 0.13/0.40 inference(split_clause,[status(thm)],[f70,f130,f141])).
% 0.13/0.40 fof(f145,definition,(
% 0.13/0.40 sQ4_spl <=> (inverse(sk_c6)=sk_c11)),
% 0.13/0.40 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.13/0.40 fof(f146,plain,(
% 0.13/0.40 inverse(sk_c6)=sk_c11|~sQ4_spl),
% 0.13/0.40 inference(component_clause,[status(thm)],[f145])).
% 0.13/0.40 fof(f148,plain,(
% 0.13/0.40 sQ0_spl|sQ4_spl),
% 0.13/0.40 inference(split_clause,[status(thm)],[f71,f130,f145])).
% 0.13/0.40 fof(f149,definition,(
% 0.13/0.40 sQ5_spl <=> (multiply(sk_c6,sk_c10)=sk_c11)),
% 0.13/0.40 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.13/0.40 fof(f150,plain,(
% 0.13/0.40 multiply(sk_c6,sk_c10)=sk_c11|~sQ5_spl),
% 0.13/0.40 inference(component_clause,[status(thm)],[f149])).
% 0.13/0.40 fof(f152,plain,(
% 0.13/0.40 sQ0_spl|sQ5_spl),
% 0.13/0.40 inference(split_clause,[status(thm)],[f72,f130,f149])).
% 0.13/0.40 fof(f153,definition,(
% 0.13/0.40 sQ6_spl <=> (multiply(sk_c7,sk_c8)=sk_c10)),
% 0.13/0.40 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 0.13/0.40 fof(f154,plain,(
% 0.13/0.40 multiply(sk_c7,sk_c8)=sk_c10|~sQ6_spl),
% 0.13/0.40 inference(component_clause,[status(thm)],[f153])).
% 0.13/0.40 fof(f156,plain,(
% 0.13/0.40 sQ0_spl|sQ6_spl),
% 0.13/0.40 inference(split_clause,[status(thm)],[f73,f130,f153])).
% 0.13/0.40 fof(f157,definition,(
% 0.13/0.40 sQ7_spl <=> (inverse(sk_c7)=sk_c8)),
% 0.13/0.40 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.13/0.40 fof(f158,plain,(
% 0.13/0.40 inverse(sk_c7)=sk_c8|~sQ7_spl),
% 0.13/0.40 inference(component_clause,[status(thm)],[f157])).
% 0.13/0.40 fof(f160,plain,(
% 0.13/0.40 sQ0_spl|sQ7_spl),
% 0.13/0.40 inference(split_clause,[status(thm)],[f74,f130,f157])).
% 0.13/0.40 fof(f161,definition,(
% 0.13/0.40 sQ8_spl <=> (multiply(sk_c8,sk_c11)=sk_c10)),
% 0.13/0.40 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 0.13/0.40 fof(f162,plain,(
% 0.13/0.40 multiply(sk_c8,sk_c11)=sk_c10|~sQ8_spl),
% 0.13/0.40 inference(component_clause,[status(thm)],[f161])).
% 0.13/0.40 fof(f164,plain,(
% 0.13/0.40 sQ0_spl|sQ8_spl),
% 0.13/0.40 inference(split_clause,[status(thm)],[f75,f130,f161])).
% 0.13/0.40 fof(f165,definition,(
% 0.13/0.40 sQ9_spl <=> (inverse(sk_c9)=sk_c10)),
% 0.13/0.40 introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 0.13/0.40 fof(f166,plain,(
% 0.13/0.40 inverse(sk_c9)=sk_c10|~sQ9_spl),
% 0.13/0.40 inference(component_clause,[status(thm)],[f165])).
% 0.13/0.40 fof(f169,definition,(
% 0.13/0.40 sQ10_spl <=> (multiply(sk_c9,sk_c11)=sk_c10)),
% 0.13/0.40 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 0.13/0.40 fof(f170,plain,(
% 0.13/0.40 multiply(sk_c9,sk_c11)=sk_c10|~sQ10_spl),
% 0.13/0.40 inference(component_clause,[status(thm)],[f169])).
% 0.13/0.40 fof(f171,plain,(
% 0.13/0.40 ~multiply(sk_c9,sk_c11)=sk_c10|sQ10_spl),
% 0.13/0.40 inference(component_clause,[status(thm)],[f169])).
% 0.13/0.40 fof(f173,definition,(
% 0.13/0.40 sQ11_spl <=> (inverse(sk_c1)=sk_c11)),
% 0.13/0.40 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 0.13/0.40 fof(f174,plain,(
% 0.13/0.40 inverse(sk_c1)=sk_c11|~sQ11_spl),
% 0.13/0.40 inference(component_clause,[status(thm)],[f173])).
% 0.13/0.40 fof(f176,plain,(
% 0.13/0.40 sQ11_spl|sQ1_spl),
% 0.13/0.40 inference(split_clause,[status(thm)],[f78,f173,f133])).
% 0.13/0.40 fof(f177,plain,(
% 0.13/0.40 sQ11_spl|sQ2_spl),
% 0.13/0.40 inference(split_clause,[status(thm)],[f79,f173,f137])).
% 0.13/0.40 fof(f178,plain,(
% 0.13/0.40 sQ11_spl|sQ3_spl),
% 0.13/0.40 inference(split_clause,[status(thm)],[f80,f173,f141])).
% 0.13/0.40 fof(f179,plain,(
% 0.13/0.40 sQ11_spl|sQ4_spl),
% 0.13/0.40 inference(split_clause,[status(thm)],[f81,f173,f145])).
% 0.13/0.40 fof(f180,plain,(
% 0.13/0.40 sQ11_spl|sQ5_spl),
% 0.13/0.40 inference(split_clause,[status(thm)],[f82,f173,f149])).
% 0.13/0.40 fof(f181,plain,(
% 0.13/0.40 sQ11_spl|sQ6_spl),
% 0.13/0.40 inference(split_clause,[status(thm)],[f83,f173,f153])).
% 0.13/0.40 fof(f182,plain,(
% 0.13/0.40 sQ11_spl|sQ7_spl),
% 0.13/0.40 inference(split_clause,[status(thm)],[f84,f173,f157])).
% 0.13/0.40 fof(f183,plain,(
% 0.13/0.40 sQ11_spl|sQ8_spl),
% 0.13/0.40 inference(split_clause,[status(thm)],[f85,f173,f161])).
% 0.13/0.40 fof(f184,plain,(
% 0.13/0.40 sQ11_spl|sQ9_spl),
% 0.13/0.40 inference(split_clause,[status(thm)],[f86,f173,f165])).
% 0.13/0.40 fof(f186,definition,(
% 0.13/0.40 sQ12_spl <=> (multiply(sk_c1,sk_c10)=sk_c11)),
% 0.13/0.40 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 0.13/0.40 fof(f187,plain,(
% 0.13/0.40 multiply(sk_c1,sk_c10)=sk_c11|~sQ12_spl),
% 0.13/0.40 inference(component_clause,[status(thm)],[f186])).
% 0.13/0.40 fof(f188,plain,(
% 0.13/0.40 ~multiply(sk_c1,sk_c10)=sk_c11|sQ12_spl),
% 0.13/0.40 inference(component_clause,[status(thm)],[f186])).
% 0.13/0.40 fof(f189,plain,(
% 0.13/0.40 sQ12_spl|sQ1_spl),
% 0.13/0.40 inference(split_clause,[status(thm)],[f88,f186,f133])).
% 0.13/0.40 fof(f190,plain,(
% 0.13/0.40 sQ12_spl|sQ2_spl),
% 0.13/0.40 inference(split_clause,[status(thm)],[f89,f186,f137])).
% 0.13/0.40 fof(f199,definition,(
% 0.13/0.40 sQ13_spl <=> (multiply(sk_c11,sk_c3)=sk_c10)),
% 0.13/0.40 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 0.13/0.40 fof(f200,plain,(
% 0.13/0.40 multiply(sk_c11,sk_c3)=sk_c10|~sQ13_spl),
% 0.13/0.40 inference(component_clause,[status(thm)],[f199])).
% 0.13/0.40 fof(f202,plain,(
% 0.13/0.40 sQ13_spl|sQ1_spl),
% 0.13/0.40 inference(split_clause,[status(thm)],[f98,f199,f133])).
% 0.13/0.40 fof(f203,plain,(
% 0.13/0.40 sQ13_spl|sQ2_spl),
% 0.13/0.40 inference(split_clause,[status(thm)],[f99,f199,f137])).
% 0.13/0.40 fof(f210,plain,(
% 0.13/0.40 sQ13_spl|sQ9_spl),
% 0.13/0.40 inference(split_clause,[status(thm)],[f106,f199,f165])).
% 0.13/0.40 fof(f211,plain,(
% 0.13/0.40 sQ13_spl|sQ10_spl),
% 0.13/0.40 inference(split_clause,[status(thm)],[f107,f199,f169])).
% 0.13/0.40 fof(f212,definition,(
% 0.13/0.40 sQ14_spl <=> (multiply(sk_c2,sk_c11)=sk_c3)),
% 0.13/0.40 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 0.13/0.40 fof(f213,plain,(
% 0.13/0.40 multiply(sk_c2,sk_c11)=sk_c3|~sQ14_spl),
% 0.13/0.40 inference(component_clause,[status(thm)],[f212])).
% 0.13/0.40 fof(f215,plain,(
% 0.13/0.40 sQ14_spl|sQ1_spl),
% 0.13/0.40 inference(split_clause,[status(thm)],[f108,f212,f133])).
% 0.13/0.40 fof(f216,plain,(
% 0.13/0.40 sQ14_spl|sQ2_spl),
% 0.13/0.40 inference(split_clause,[status(thm)],[f109,f212,f137])).
% 0.13/0.40 fof(f223,plain,(
% 0.13/0.40 sQ14_spl|sQ9_spl),
% 0.13/0.40 inference(split_clause,[status(thm)],[f116,f212,f165])).
% 0.13/0.40 fof(f224,plain,(
% 0.13/0.40 sQ14_spl|sQ10_spl),
% 0.13/0.40 inference(split_clause,[status(thm)],[f117,f212,f169])).
% 0.13/0.40 fof(f225,definition,(
% 0.13/0.40 sQ15_spl <=> (inverse(sk_c2)=sk_c11)),
% 0.13/0.40 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 0.13/0.40 fof(f226,plain,(
% 0.13/0.40 inverse(sk_c2)=sk_c11|~sQ15_spl),
% 0.13/0.40 inference(component_clause,[status(thm)],[f225])).
% 0.13/0.40 fof(f228,plain,(
% 0.13/0.40 sQ15_spl|sQ1_spl),
% 0.13/0.40 inference(split_clause,[status(thm)],[f118,f225,f133])).
% 0.13/0.40 fof(f229,plain,(
% 0.13/0.40 sQ15_spl|sQ2_spl),
% 0.13/0.40 inference(split_clause,[status(thm)],[f119,f225,f137])).
% 0.13/0.40 fof(f236,plain,(
% 0.13/0.40 sQ15_spl|sQ9_spl),
% 0.13/0.40 inference(split_clause,[status(thm)],[f126,f225,f165])).
% 0.13/0.40 fof(f237,plain,(
% 0.13/0.40 sQ15_spl|sQ10_spl),
% 0.13/0.40 inference(split_clause,[status(thm)],[f127,f225,f169])).
% 0.13/0.40 fof(f238,definition,(
% 0.13/0.40 ![X0]: (sQ16_spl <=> (~inverse(X0)=sk_c11|~multiply(X0,sk_c10)=sk_c11))),
% 0.13/0.40 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 0.13/0.40 fof(f239,plain,(
% 0.13/0.40 ![X0]: (~inverse(X0)=sk_c11|~multiply(X0,sk_c10)=sk_c11|~sQ16_spl)),
% 0.13/0.40 inference(component_clause,[status(thm)],[f238])).
% 0.13/0.40 fof(f241,definition,(
% 0.13/0.40 ![X1,X2]: (sQ17_spl <=> (~multiply(sk_c11,X1)=sk_c10|~multiply(X2,sk_c11)=X1|~inverse(X2)=sk_c11))),
% 0.13/0.40 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 0.13/0.40 fof(f242,plain,(
% 0.13/0.40 ![X0,X1]: (~multiply(sk_c11,X0)=sk_c10|~multiply(X1,sk_c11)=X0|~inverse(X1)=sk_c11|~sQ17_spl)),
% 0.13/0.40 inference(component_clause,[status(thm)],[f241])).
% 0.13/0.40 fof(f244,definition,(
% 0.13/0.40 ![X3,X4]: (sQ18_spl <=> (~multiply(X3,X4)=sk_c11|~inverse(X3)=X4|~multiply(X4,sk_c10)=sk_c11))),
% 0.13/0.40 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 0.13/0.40 fof(f245,plain,(
% 0.13/0.40 ![X0,X1]: (~multiply(X0,X1)=sk_c11|~inverse(X0)=X1|~multiply(X1,sk_c10)=sk_c11|~sQ18_spl)),
% 0.13/0.40 inference(component_clause,[status(thm)],[f244])).
% 0.13/0.40 fof(f247,definition,(
% 0.13/0.40 ![X6,X7]: (sQ19_spl <=> (~multiply(X6,X7)=sk_c10|~inverse(X6)=X7|~multiply(X7,sk_c11)=sk_c10))),
% 0.13/0.40 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 0.13/0.40 fof(f248,plain,(
% 0.13/0.40 ![X0,X1]: (~multiply(X0,X1)=sk_c10|~inverse(X0)=X1|~multiply(X1,sk_c11)=sk_c10|~sQ19_spl)),
% 0.13/0.40 inference(component_clause,[status(thm)],[f247])).
% 0.13/0.40 fof(f250,definition,(
% 0.13/0.40 ![X8]: (sQ20_spl <=> (~inverse(X8)=sk_c10|~multiply(X8,sk_c11)=sk_c10))),
% 0.13/0.40 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 0.13/0.40 fof(f251,plain,(
% 0.13/0.40 ![X0]: (~inverse(X0)=sk_c10|~multiply(X0,sk_c11)=sk_c10|~sQ20_spl)),
% 0.13/0.40 inference(component_clause,[status(thm)],[f250])).
% 0.13/0.40 fof(f253,plain,(
% 0.13/0.40 ~sQ0_spl|sQ16_spl|sQ17_spl|sQ18_spl|sQ19_spl|sQ20_spl),
% 0.13/0.40 inference(split_clause,[status(thm)],[f129,f130,f238,f241,f244,f247,f250])).
% 0.13/0.40 fof(f267,plain,(
% 0.13/0.40 ~inverse(sk_c9)=sk_c10|~sQ20_spl|~sQ10_spl),
% 0.13/0.40 inference(resolution,[status(thm)],[f251,f170])).
% 0.13/0.40 fof(f269,plain,(
% 0.13/0.40 ~inverse(sk_c8)=sk_c10|~sk_c10=sk_c10|~sQ20_spl|~sQ8_spl),
% 0.13/0.40 inference(paramodulation,[status(thm)],[f162,f251])).
% 0.13/0.40 fof(f271,plain,(
% 0.13/0.40 ~inverse(sk_c2)=sk_c10|~sk_c3=sk_c10|~sQ20_spl|~sQ14_spl),
% 0.13/0.40 inference(paramodulation,[status(thm)],[f213,f251])).
% 0.13/0.40 fof(f272,plain,(
% 0.13/0.40 ~sk_c10=sk_c10|~sQ9_spl|~sQ20_spl|~sQ10_spl),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f166,f267])).
% 0.13/0.40 fof(f273,plain,(
% 0.13/0.40 $false|~sQ9_spl|~sQ20_spl|~sQ10_spl),
% 0.13/0.40 inference(trivial_equality_resolution,[status(thm)],[f272])).
% 0.13/0.40 fof(f274,plain,(
% 0.13/0.40 ~sQ9_spl|~sQ20_spl|~sQ10_spl),
% 0.13/0.40 inference(contradiction_clause,[status(thm)],[f273])).
% 0.13/0.40 fof(f275,plain,(
% 0.13/0.40 ![X0]: (~multiply(X0,inverse(X0))=sk_c10|~multiply(inverse(X0),sk_c11)=sk_c10|~sQ19_spl)),
% 0.13/0.40 inference(destructive_equality_resolution,[status(thm)],[f248])).
% 0.13/0.40 fof(f276,plain,(
% 0.13/0.40 ![X0]: (~multiply(X0,inverse(X0))=sk_c11|~multiply(inverse(X0),sk_c10)=sk_c11|~sQ18_spl)),
% 0.13/0.40 inference(destructive_equality_resolution,[status(thm)],[f245])).
% 0.13/0.40 fof(f277,plain,(
% 0.13/0.40 ![X0]: (~multiply(sk_c11,multiply(X0,sk_c11))=sk_c10|~inverse(X0)=sk_c11|~sQ17_spl)),
% 0.13/0.40 inference(destructive_equality_resolution,[status(thm)],[f242])).
% 0.13/0.40 fof(f284,plain,(
% 0.13/0.40 multiply(sk_c11,sk_c2)=identity|~sQ15_spl),
% 0.13/0.40 inference(paramodulation,[status(thm)],[f226,f66])).
% 0.13/0.40 fof(f285,plain,(
% 0.13/0.40 ![X0,X1]: (multiply(identity,X0)=multiply(inverse(X1),multiply(X1,X0)))),
% 0.13/0.40 inference(paramodulation,[status(thm)],[f66,f67])).
% 0.13/0.40 fof(f286,plain,(
% 0.13/0.40 ![X0,X1]: (X0=multiply(inverse(X1),multiply(X1,X0)))),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f65,f285])).
% 0.13/0.40 fof(f308,plain,(
% 0.13/0.40 ![X0]: (X0=multiply(inverse(identity),X0))),
% 0.13/0.40 inference(paramodulation,[status(thm)],[f65,f286])).
% 0.13/0.40 fof(f310,plain,(
% 0.13/0.40 sk_c5=multiply(inverse(sk_c4),sk_c11)|~sQ1_spl),
% 0.13/0.40 inference(paramodulation,[status(thm)],[f134,f286])).
% 0.13/0.40 fof(f318,plain,(
% 0.13/0.40 sk_c10=multiply(inverse(sk_c1),sk_c11)|~sQ12_spl),
% 0.13/0.40 inference(paramodulation,[status(thm)],[f187,f286])).
% 0.13/0.40 fof(f319,plain,(
% 0.13/0.40 sk_c2=multiply(inverse(sk_c11),identity)|~sQ15_spl),
% 0.13/0.40 inference(paramodulation,[status(thm)],[f284,f286])).
% 0.13/0.40 fof(f322,plain,(
% 0.13/0.40 sk_c3=multiply(inverse(sk_c11),sk_c10)|~sQ13_spl),
% 0.13/0.40 inference(paramodulation,[status(thm)],[f200,f286])).
% 0.13/0.40 fof(f323,plain,(
% 0.13/0.40 sk_c11=multiply(inverse(sk_c2),sk_c3)|~sQ14_spl),
% 0.13/0.40 inference(paramodulation,[status(thm)],[f213,f286])).
% 0.13/0.40 fof(f325,plain,(
% 0.13/0.40 sk_c5=multiply(sk_c5,sk_c11)|~sQ2_spl|~sQ1_spl),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f138,f310])).
% 0.13/0.40 fof(f328,plain,(
% 0.13/0.40 sk_c10=multiply(sk_c11,sk_c11)|~sQ11_spl|~sQ12_spl),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f174,f318])).
% 0.13/0.40 fof(f329,plain,(
% 0.13/0.40 sk_c2=multiply(sk_c10,identity)|~sQ0_spl|~sQ15_spl),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f131,f319])).
% 0.13/0.40 fof(f332,plain,(
% 0.13/0.40 sk_c3=multiply(sk_c10,sk_c10)|~sQ0_spl|~sQ13_spl),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f131,f322])).
% 0.13/0.40 fof(f333,plain,(
% 0.13/0.40 sk_c11=multiply(sk_c11,sk_c3)|~sQ15_spl|~sQ14_spl),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f226,f323])).
% 0.13/0.40 fof(f334,plain,(
% 0.13/0.40 sk_c11=sk_c10|~sQ13_spl|~sQ15_spl|~sQ14_spl),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f200,f333])).
% 0.13/0.40 fof(f347,plain,(
% 0.13/0.40 inverse(sk_c10)=sk_c10|~sQ13_spl|~sQ15_spl|~sQ14_spl|~sQ0_spl),
% 0.13/0.40 inference(backward_demodulation,[status(thm)],[f334,f131])).
% 0.13/0.40 fof(f351,plain,(
% 0.13/0.40 inverse(sk_c2)=sk_c10|~sQ13_spl|~sQ14_spl|~sQ15_spl),
% 0.13/0.40 inference(backward_demodulation,[status(thm)],[f334,f226])).
% 0.13/0.40 fof(f360,plain,(
% 0.13/0.40 ![X0]: (~multiply(X0,inverse(X0))=sk_c10|~multiply(inverse(X0),sk_c10)=sk_c10|~sQ13_spl|~sQ15_spl|~sQ14_spl|~sQ19_spl)),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f334,f275])).
% 0.13/0.40 fof(f365,plain,(
% 0.13/0.40 ~multiply(sk_c10,inverse(sk_c10))=sk_c10|~multiply(sk_c10,sk_c10)=sk_c10|~sQ19_spl|~sQ13_spl|~sQ15_spl|~sQ14_spl|~sQ0_spl),
% 0.13/0.40 inference(paramodulation,[status(thm)],[f347,f360])).
% 0.13/0.40 fof(f368,definition,(
% 0.13/0.40 sQ21_spl <=> (multiply(sk_c10,inverse(sk_c10))=sk_c10)),
% 0.13/0.40 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 0.13/0.40 fof(f370,plain,(
% 0.13/0.40 ~multiply(sk_c10,inverse(sk_c10))=sk_c10|sQ21_spl),
% 0.13/0.40 inference(component_clause,[status(thm)],[f368])).
% 0.13/0.40 fof(f378,definition,(
% 0.13/0.40 sQ24_spl <=> (multiply(sk_c10,sk_c10)=sk_c10)),
% 0.13/0.40 introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition])).
% 0.13/0.40 fof(f380,plain,(
% 0.13/0.40 ~multiply(sk_c10,sk_c10)=sk_c10|sQ24_spl),
% 0.13/0.40 inference(component_clause,[status(thm)],[f378])).
% 0.13/0.40 fof(f390,plain,(
% 0.13/0.40 ~sQ21_spl|~sQ24_spl|~sQ19_spl|~sQ13_spl|~sQ15_spl|~sQ14_spl|~sQ0_spl),
% 0.13/0.40 inference(split_clause,[status(thm)],[f365,f368,f378,f247,f199,f225,f212,f130])).
% 0.13/0.40 fof(f405,plain,(
% 0.13/0.40 ~multiply(sk_c10,sk_c10)=sk_c10|~sQ13_spl|~sQ15_spl|~sQ14_spl|~sQ0_spl|sQ21_spl),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f347,f370])).
% 0.13/0.40 fof(f414,plain,(
% 0.13/0.40 ~multiply(sk_c9,sk_c10)=sk_c10|~sQ13_spl|~sQ15_spl|~sQ14_spl|sQ10_spl),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f334,f171])).
% 0.13/0.40 fof(f415,plain,(
% 0.13/0.40 ![X0]: (~multiply(sk_c10,multiply(X0,sk_c11))=sk_c10|~inverse(X0)=sk_c11|~sQ13_spl|~sQ15_spl|~sQ14_spl|~sQ17_spl)),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f334,f277])).
% 0.13/0.40 fof(f416,plain,(
% 0.13/0.40 ![X0]: (~multiply(sk_c10,multiply(X0,sk_c10))=sk_c10|~inverse(X0)=sk_c11|~sQ13_spl|~sQ15_spl|~sQ14_spl|~sQ17_spl)),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f334,f415])).
% 0.13/0.40 fof(f417,plain,(
% 0.13/0.40 ![X0]: (~multiply(sk_c10,multiply(X0,sk_c10))=sk_c10|~inverse(X0)=sk_c10|~sQ13_spl|~sQ15_spl|~sQ14_spl|~sQ17_spl)),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f334,f416])).
% 0.13/0.40 fof(f420,plain,(
% 0.13/0.40 ![X0]: (~multiply(X0,inverse(X0))=sk_c10|~multiply(inverse(X0),sk_c10)=sk_c11|~sQ13_spl|~sQ15_spl|~sQ14_spl|~sQ18_spl)),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f334,f276])).
% 0.13/0.40 fof(f421,plain,(
% 0.13/0.40 ![X0]: (~multiply(X0,inverse(X0))=sk_c10|~multiply(inverse(X0),sk_c10)=sk_c10|~sQ13_spl|~sQ15_spl|~sQ14_spl|~sQ18_spl)),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f334,f420])).
% 0.13/0.40 fof(f426,plain,(
% 0.13/0.40 ~multiply(sk_c10,inverse(sk_c10))=sk_c10|~multiply(sk_c10,sk_c10)=sk_c10|~sQ18_spl|~sQ13_spl|~sQ15_spl|~sQ14_spl|~sQ0_spl),
% 0.13/0.40 inference(paramodulation,[status(thm)],[f347,f421])).
% 0.13/0.40 fof(f432,plain,(
% 0.13/0.40 ~sQ21_spl|~sQ24_spl|~sQ18_spl|~sQ13_spl|~sQ15_spl|~sQ14_spl|~sQ0_spl),
% 0.13/0.40 inference(split_clause,[status(thm)],[f426,f368,f378,f244,f199,f225,f212,f130])).
% 0.13/0.40 fof(f455,plain,(
% 0.13/0.40 sk_c10=multiply(sk_c10,sk_c11)|~sQ13_spl|~sQ15_spl|~sQ14_spl|~sQ11_spl|~sQ12_spl),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f334,f328])).
% 0.13/0.40 fof(f456,plain,(
% 0.13/0.40 sk_c10=multiply(sk_c10,sk_c10)|~sQ13_spl|~sQ15_spl|~sQ14_spl|~sQ11_spl|~sQ12_spl),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f334,f455])).
% 0.13/0.40 fof(f457,plain,(
% 0.13/0.40 sk_c10=multiply(inverse(sk_c10),sk_c10)|~sQ13_spl|~sQ15_spl|~sQ14_spl|~sQ11_spl|~sQ12_spl),
% 0.13/0.40 inference(paramodulation,[status(thm)],[f456,f286])).
% 0.13/0.40 fof(f459,plain,(
% 0.13/0.40 sk_c10=identity|~sQ13_spl|~sQ15_spl|~sQ14_spl|~sQ11_spl|~sQ12_spl),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f66,f457])).
% 0.13/0.40 fof(f460,plain,(
% 0.13/0.40 ![X0]: (X0=multiply(inverse(sk_c10),X0)|~sQ13_spl|~sQ15_spl|~sQ14_spl|~sQ11_spl|~sQ12_spl)),
% 0.13/0.40 inference(backward_demodulation,[status(thm)],[f459,f308])).
% 0.13/0.40 fof(f463,plain,(
% 0.13/0.40 ![X0]: (X0=multiply(sk_c10,X0)|~sQ0_spl|~sQ13_spl|~sQ15_spl|~sQ14_spl|~sQ11_spl|~sQ12_spl)),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f347,f460])).
% 0.13/0.40 fof(f468,plain,(
% 0.13/0.40 sk_c10=sk_c2|~sQ0_spl|~sQ13_spl|~sQ15_spl|~sQ14_spl|~sQ11_spl|~sQ12_spl),
% 0.13/0.40 inference(backward_demodulation,[status(thm)],[f469,f459])).
% 0.13/0.40 fof(f469,plain,(
% 0.13/0.40 sk_c2=identity|~sQ13_spl|~sQ14_spl|~sQ11_spl|~sQ12_spl|~sQ0_spl|~sQ15_spl),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f463,f329])).
% 0.13/0.40 fof(f470,plain,(
% 0.13/0.40 ![X0]: (X0=multiply(sk_c2,X0)|~sQ0_spl|~sQ13_spl|~sQ15_spl|~sQ14_spl|~sQ11_spl|~sQ12_spl)),
% 0.13/0.40 inference(backward_demodulation,[status(thm)],[f468,f463])).
% 0.13/0.40 fof(f472,plain,(
% 0.13/0.40 inverse(sk_c9)=sk_c2|~sQ0_spl|~sQ13_spl|~sQ15_spl|~sQ14_spl|~sQ11_spl|~sQ12_spl|~sQ9_spl),
% 0.13/0.40 inference(backward_demodulation,[status(thm)],[f468,f166])).
% 0.13/0.40 fof(f474,plain,(
% 0.13/0.40 inverse(sk_c2)=sk_c2|~sQ0_spl|~sQ11_spl|~sQ12_spl|~sQ13_spl|~sQ14_spl|~sQ15_spl),
% 0.13/0.40 inference(backward_demodulation,[status(thm)],[f468,f351])).
% 0.13/0.40 fof(f483,plain,(
% 0.13/0.40 ![X0]: (X0=multiply(sk_c2,multiply(sk_c9,X0))|~sQ0_spl|~sQ13_spl|~sQ15_spl|~sQ14_spl|~sQ11_spl|~sQ12_spl|~sQ9_spl)),
% 0.13/0.40 inference(paramodulation,[status(thm)],[f472,f286])).
% 0.13/0.40 fof(f484,plain,(
% 0.13/0.40 ![X0]: (X0=multiply(sk_c9,X0)|~sQ0_spl|~sQ13_spl|~sQ15_spl|~sQ14_spl|~sQ11_spl|~sQ12_spl|~sQ9_spl)),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f470,f483])).
% 0.13/0.40 fof(f518,plain,(
% 0.13/0.40 sk_c3=multiply(sk_c2,sk_c10)|~sQ15_spl|~sQ14_spl|~sQ11_spl|~sQ12_spl|~sQ0_spl|~sQ13_spl),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f468,f332])).
% 0.13/0.40 fof(f519,plain,(
% 0.13/0.40 sk_c3=sk_c10|~sQ15_spl|~sQ14_spl|~sQ11_spl|~sQ12_spl|~sQ0_spl|~sQ13_spl),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f470,f518])).
% 0.13/0.40 fof(f520,plain,(
% 0.13/0.40 sk_c3=sk_c2|~sQ15_spl|~sQ14_spl|~sQ11_spl|~sQ12_spl|~sQ0_spl|~sQ13_spl),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f468,f519])).
% 0.13/0.40 fof(f535,plain,(
% 0.13/0.40 ~sk_c10=sk_c10|~sQ0_spl|~sQ11_spl|~sQ12_spl|~sQ9_spl|~sQ13_spl|~sQ15_spl|~sQ14_spl|sQ10_spl),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f484,f414])).
% 0.13/0.40 fof(f536,plain,(
% 0.13/0.40 ~sk_c2=sk_c10|~sQ0_spl|~sQ11_spl|~sQ12_spl|~sQ9_spl|~sQ13_spl|~sQ15_spl|~sQ14_spl|sQ10_spl),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f468,f535])).
% 0.13/0.40 fof(f537,plain,(
% 0.13/0.40 ~sk_c2=sk_c2|~sQ0_spl|~sQ11_spl|~sQ12_spl|~sQ9_spl|~sQ13_spl|~sQ15_spl|~sQ14_spl|sQ10_spl),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f468,f536])).
% 0.13/0.40 fof(f538,plain,(
% 0.13/0.40 $false|~sQ0_spl|~sQ11_spl|~sQ12_spl|~sQ9_spl|~sQ13_spl|~sQ15_spl|~sQ14_spl|sQ10_spl),
% 0.13/0.40 inference(trivial_equality_resolution,[status(thm)],[f537])).
% 0.13/0.40 fof(f539,plain,(
% 0.13/0.40 ~sQ0_spl|~sQ11_spl|~sQ12_spl|~sQ9_spl|~sQ13_spl|~sQ15_spl|~sQ14_spl|sQ10_spl),
% 0.13/0.40 inference(contradiction_clause,[status(thm)],[f538])).
% 0.13/0.40 fof(f549,plain,(
% 0.13/0.40 ![X0]: (~multiply(sk_c2,multiply(X0,sk_c10))=sk_c10|~inverse(X0)=sk_c10|~sQ0_spl|~sQ11_spl|~sQ12_spl|~sQ13_spl|~sQ15_spl|~sQ14_spl|~sQ17_spl)),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f468,f417])).
% 0.13/0.40 fof(f550,plain,(
% 0.13/0.40 ![X0]: (~multiply(X0,sk_c10)=sk_c10|~inverse(X0)=sk_c10|~sQ0_spl|~sQ11_spl|~sQ12_spl|~sQ13_spl|~sQ15_spl|~sQ14_spl|~sQ17_spl)),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f470,f549])).
% 0.13/0.40 fof(f551,plain,(
% 0.13/0.40 ![X0]: (~multiply(X0,sk_c2)=sk_c10|~inverse(X0)=sk_c10|~sQ0_spl|~sQ11_spl|~sQ12_spl|~sQ13_spl|~sQ15_spl|~sQ14_spl|~sQ17_spl)),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f468,f550])).
% 0.13/0.40 fof(f552,plain,(
% 0.13/0.40 ![X0]: (~multiply(X0,sk_c2)=sk_c2|~inverse(X0)=sk_c10|~sQ0_spl|~sQ11_spl|~sQ12_spl|~sQ13_spl|~sQ15_spl|~sQ14_spl|~sQ17_spl)),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f468,f551])).
% 0.13/0.40 fof(f553,plain,(
% 0.13/0.40 ![X0]: (~multiply(X0,sk_c2)=sk_c2|~inverse(X0)=sk_c2|~sQ0_spl|~sQ11_spl|~sQ12_spl|~sQ13_spl|~sQ15_spl|~sQ14_spl|~sQ17_spl)),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f468,f552])).
% 0.13/0.40 fof(f556,plain,(
% 0.13/0.40 ~inverse(sk_c2)=sk_c2|~sQ17_spl|~sQ0_spl|~sQ13_spl|~sQ15_spl|~sQ14_spl|~sQ11_spl|~sQ12_spl),
% 0.13/0.40 inference(resolution,[status(thm)],[f553,f470])).
% 0.13/0.40 fof(f561,plain,(
% 0.13/0.40 ~sk_c2=sk_c2|~sQ17_spl|~sQ0_spl|~sQ13_spl|~sQ15_spl|~sQ14_spl|~sQ11_spl|~sQ12_spl),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f474,f556])).
% 0.13/0.40 fof(f562,plain,(
% 0.13/0.40 $false|~sQ17_spl|~sQ0_spl|~sQ13_spl|~sQ15_spl|~sQ14_spl|~sQ11_spl|~sQ12_spl),
% 0.13/0.40 inference(trivial_equality_resolution,[status(thm)],[f561])).
% 0.13/0.40 fof(f563,plain,(
% 0.13/0.40 ~sQ17_spl|~sQ0_spl|~sQ13_spl|~sQ15_spl|~sQ14_spl|~sQ11_spl|~sQ12_spl),
% 0.13/0.40 inference(contradiction_clause,[status(thm)],[f562])).
% 0.13/0.40 fof(f569,plain,(
% 0.13/0.40 sk_c8=multiply(inverse(sk_c7),sk_c10)|~sQ6_spl),
% 0.13/0.40 inference(paramodulation,[status(thm)],[f154,f286])).
% 0.13/0.40 fof(f571,plain,(
% 0.13/0.40 sk_c8=multiply(sk_c8,sk_c10)|~sQ7_spl|~sQ6_spl),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f158,f569])).
% 0.13/0.40 fof(f573,plain,(
% 0.13/0.40 ~sk_c3=sk_c10|~sQ0_spl|~sQ13_spl|sQ24_spl),
% 0.13/0.40 inference(backward_demodulation,[status(thm)],[f332,f380])).
% 0.13/0.40 fof(f578,plain,(
% 0.13/0.40 ![X0]: (multiply(identity,X0)=X0)),
% 0.13/0.40 inference(paramodulation,[status(thm)],[f286,f308])).
% 0.13/0.40 fof(f584,plain,(
% 0.13/0.40 ~inverse(identity)=sk_c11|~sk_c10=sk_c11|~sQ16_spl),
% 0.13/0.40 inference(paramodulation,[status(thm)],[f578,f239])).
% 0.13/0.40 fof(f586,plain,(
% 0.13/0.40 ~inverse(inverse(identity))=sk_c11|~sk_c10=sk_c11|~sQ16_spl),
% 0.13/0.40 inference(paramodulation,[status(thm)],[f308,f239])).
% 0.13/0.40 fof(f588,definition,(
% 0.13/0.40 sQ31_spl <=> (inverse(identity)=sk_c11)),
% 0.13/0.40 introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition])).
% 0.13/0.40 fof(f590,plain,(
% 0.13/0.40 ~inverse(identity)=sk_c11|sQ31_spl),
% 0.13/0.40 inference(component_clause,[status(thm)],[f588])).
% 0.13/0.40 fof(f591,definition,(
% 0.13/0.40 sQ32_spl <=> (sk_c10=sk_c11)),
% 0.13/0.40 introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition])).
% 0.13/0.40 fof(f593,plain,(
% 0.13/0.40 ~sk_c10=sk_c11|sQ32_spl),
% 0.13/0.40 inference(component_clause,[status(thm)],[f591])).
% 0.13/0.40 fof(f594,plain,(
% 0.13/0.40 ~sQ31_spl|~sQ32_spl|~sQ16_spl),
% 0.13/0.40 inference(split_clause,[status(thm)],[f584,f588,f591,f238])).
% 0.13/0.40 fof(f602,definition,(
% 0.13/0.40 sQ35_spl <=> (inverse(inverse(identity))=sk_c11)),
% 0.13/0.40 introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition])).
% 0.13/0.40 fof(f605,plain,(
% 0.13/0.40 ~sQ35_spl|~sQ32_spl|~sQ16_spl),
% 0.13/0.40 inference(split_clause,[status(thm)],[f586,f602,f591,f238])).
% 0.13/0.40 fof(f606,plain,(
% 0.13/0.40 sk_c5=multiply(inverse(sk_c4),sk_c11)|~sQ1_spl),
% 0.13/0.40 inference(paramodulation,[status(thm)],[f134,f286])).
% 0.13/0.40 fof(f608,plain,(
% 0.13/0.40 sk_c5=multiply(sk_c5,sk_c11)|~sQ2_spl|~sQ1_spl),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f138,f606])).
% 0.13/0.40 fof(f612,plain,(
% 0.13/0.40 multiply(sk_c11,sk_c1)=identity|~sQ11_spl),
% 0.13/0.40 inference(paramodulation,[status(thm)],[f174,f66])).
% 0.13/0.40 fof(f617,plain,(
% 0.13/0.40 ~inverse(inverse(sk_c10))=sk_c11|~identity=sk_c11|~sQ16_spl),
% 0.13/0.40 inference(paramodulation,[status(thm)],[f66,f239])).
% 0.13/0.40 fof(f620,definition,(
% 0.13/0.40 sQ36_spl <=> (inverse(inverse(sk_c10))=sk_c11)),
% 0.13/0.40 introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition])).
% 0.13/0.40 fof(f622,plain,(
% 0.13/0.40 ~inverse(inverse(sk_c10))=sk_c11|sQ36_spl),
% 0.13/0.40 inference(component_clause,[status(thm)],[f620])).
% 0.13/0.40 fof(f623,definition,(
% 0.13/0.40 sQ37_spl <=> (identity=sk_c11)),
% 0.13/0.40 introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition])).
% 0.13/0.40 fof(f625,plain,(
% 0.13/0.40 ~identity=sk_c11|sQ37_spl),
% 0.13/0.40 inference(component_clause,[status(thm)],[f623])).
% 0.13/0.40 fof(f626,plain,(
% 0.13/0.40 ~sQ36_spl|~sQ37_spl|~sQ16_spl),
% 0.13/0.40 inference(split_clause,[status(thm)],[f617,f620,f623,f238])).
% 0.13/0.40 fof(f628,plain,(
% 0.13/0.40 sk_c11=multiply(inverse(sk_c11),sk_c10)|~sQ11_spl|~sQ12_spl),
% 0.13/0.40 inference(paramodulation,[status(thm)],[f328,f286])).
% 0.13/0.40 fof(f630,plain,(
% 0.13/0.40 sk_c11=multiply(sk_c10,sk_c10)|~sQ0_spl|~sQ11_spl|~sQ12_spl),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f131,f628])).
% 0.13/0.40 fof(f631,plain,(
% 0.13/0.40 sk_c11=sk_c3|~sQ13_spl|~sQ0_spl|~sQ11_spl|~sQ12_spl),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f332,f630])).
% 0.13/0.40 fof(f634,plain,(
% 0.13/0.40 sk_c11=multiply(inverse(sk_c5),sk_c5)|~sQ2_spl|~sQ1_spl),
% 0.13/0.40 inference(paramodulation,[status(thm)],[f325,f286])).
% 0.13/0.40 fof(f636,plain,(
% 0.13/0.40 sk_c11=identity|~sQ2_spl|~sQ1_spl),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f66,f634])).
% 0.13/0.40 fof(f637,plain,(
% 0.13/0.40 $false|sQ37_spl|~sQ2_spl|~sQ1_spl),
% 0.13/0.40 inference(forward_subsumption_resolution,[status(thm)],[f636,f625])).
% 0.13/0.40 fof(f638,plain,(
% 0.13/0.40 sQ37_spl|~sQ2_spl|~sQ1_spl),
% 0.13/0.40 inference(contradiction_clause,[status(thm)],[f637])).
% 0.13/0.40 fof(f640,plain,(
% 0.13/0.40 ~inverse(identity)=sk_c3|~sQ13_spl|~sQ0_spl|~sQ11_spl|~sQ12_spl|sQ31_spl),
% 0.13/0.40 inference(backward_demodulation,[status(thm)],[f631,f590])).
% 0.13/0.40 fof(f642,plain,(
% 0.13/0.40 ~sk_c10=sk_c3|~sQ13_spl|~sQ0_spl|~sQ11_spl|~sQ12_spl|sQ32_spl),
% 0.13/0.40 inference(backward_demodulation,[status(thm)],[f631,f593])).
% 0.13/0.40 fof(f651,plain,(
% 0.13/0.40 ~sk_c3=sk_c2|~sQ15_spl|~sQ14_spl|~sQ11_spl|~sQ12_spl|~sQ0_spl|~sQ13_spl|sQ24_spl),
% 0.13/0.40 inference(backward_demodulation,[status(thm)],[f468,f573])).
% 0.13/0.40 fof(f671,plain,(
% 0.13/0.40 ~sk_c2=sk_c2|~sQ15_spl|~sQ14_spl|~sQ11_spl|~sQ12_spl|~sQ0_spl|~sQ13_spl|sQ24_spl),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f520,f651])).
% 0.13/0.40 fof(f672,plain,(
% 0.13/0.40 $false|~sQ15_spl|~sQ14_spl|~sQ11_spl|~sQ12_spl|~sQ0_spl|~sQ13_spl|sQ24_spl),
% 0.13/0.40 inference(trivial_equality_resolution,[status(thm)],[f671])).
% 0.13/0.40 fof(f673,plain,(
% 0.13/0.40 ~sQ15_spl|~sQ14_spl|~sQ11_spl|~sQ12_spl|~sQ0_spl|~sQ13_spl|sQ24_spl),
% 0.13/0.40 inference(contradiction_clause,[status(thm)],[f672])).
% 0.13/0.40 fof(f674,plain,(
% 0.13/0.40 ~sk_c2=sk_c3|~sQ15_spl|~sQ14_spl|~sQ13_spl|~sQ0_spl|~sQ11_spl|~sQ12_spl|sQ32_spl),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f468,f642])).
% 0.13/0.40 fof(f675,plain,(
% 0.13/0.40 ~sk_c2=sk_c2|~sQ15_spl|~sQ14_spl|~sQ13_spl|~sQ0_spl|~sQ11_spl|~sQ12_spl|sQ32_spl),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f520,f674])).
% 0.13/0.40 fof(f676,plain,(
% 0.13/0.40 $false|~sQ15_spl|~sQ14_spl|~sQ13_spl|~sQ0_spl|~sQ11_spl|~sQ12_spl|sQ32_spl),
% 0.13/0.40 inference(trivial_equality_resolution,[status(thm)],[f675])).
% 0.13/0.40 fof(f677,plain,(
% 0.13/0.40 ~sQ15_spl|~sQ14_spl|~sQ13_spl|~sQ0_spl|~sQ11_spl|~sQ12_spl|sQ32_spl),
% 0.13/0.40 inference(contradiction_clause,[status(thm)],[f676])).
% 0.13/0.40 fof(f710,plain,(
% 0.13/0.40 ~inverse(sk_c2)=sk_c3|~sQ14_spl|~sQ15_spl|~sQ13_spl|~sQ0_spl|~sQ11_spl|~sQ12_spl|sQ31_spl),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f469,f640])).
% 0.13/0.40 fof(f711,plain,(
% 0.13/0.40 ~sk_c2=sk_c3|~sQ14_spl|~sQ15_spl|~sQ13_spl|~sQ0_spl|~sQ11_spl|~sQ12_spl|sQ31_spl),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f474,f710])).
% 0.13/0.40 fof(f712,plain,(
% 0.13/0.40 ~sk_c2=sk_c2|~sQ14_spl|~sQ15_spl|~sQ13_spl|~sQ0_spl|~sQ11_spl|~sQ12_spl|sQ31_spl),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f520,f711])).
% 0.13/0.40 fof(f713,plain,(
% 0.13/0.40 $false|~sQ14_spl|~sQ15_spl|~sQ13_spl|~sQ0_spl|~sQ11_spl|~sQ12_spl|sQ31_spl),
% 0.13/0.40 inference(trivial_equality_resolution,[status(thm)],[f712])).
% 0.13/0.40 fof(f714,plain,(
% 0.13/0.40 ~sQ14_spl|~sQ15_spl|~sQ13_spl|~sQ0_spl|~sQ11_spl|~sQ12_spl|sQ31_spl),
% 0.13/0.40 inference(contradiction_clause,[status(thm)],[f713])).
% 0.13/0.40 fof(f786,plain,(
% 0.13/0.40 ~multiply(sk_c2,sk_c10)=sk_c10|~sQ11_spl|~sQ12_spl|~sQ13_spl|~sQ15_spl|~sQ14_spl|~sQ0_spl|sQ21_spl),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f468,f405])).
% 0.13/0.40 fof(f787,plain,(
% 0.13/0.40 ~sk_c10=sk_c10|~sQ11_spl|~sQ12_spl|~sQ13_spl|~sQ15_spl|~sQ14_spl|~sQ0_spl|sQ21_spl),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f470,f786])).
% 0.13/0.40 fof(f788,plain,(
% 0.13/0.40 ~sk_c2=sk_c10|~sQ11_spl|~sQ12_spl|~sQ13_spl|~sQ15_spl|~sQ14_spl|~sQ0_spl|sQ21_spl),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f468,f787])).
% 0.13/0.40 fof(f789,plain,(
% 0.13/0.40 ~sk_c2=sk_c2|~sQ11_spl|~sQ12_spl|~sQ13_spl|~sQ15_spl|~sQ14_spl|~sQ0_spl|sQ21_spl),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f468,f788])).
% 0.13/0.40 fof(f790,plain,(
% 0.13/0.40 $false|~sQ11_spl|~sQ12_spl|~sQ13_spl|~sQ15_spl|~sQ14_spl|~sQ0_spl|sQ21_spl),
% 0.13/0.40 inference(trivial_equality_resolution,[status(thm)],[f789])).
% 0.13/0.40 fof(f791,plain,(
% 0.13/0.40 ~sQ11_spl|~sQ12_spl|~sQ13_spl|~sQ15_spl|~sQ14_spl|~sQ0_spl|sQ21_spl),
% 0.13/0.40 inference(contradiction_clause,[status(thm)],[f790])).
% 0.13/0.40 fof(f806,definition,(
% 0.13/0.40 sQ38_spl <=> (inverse(sk_c8)=sk_c10)),
% 0.13/0.40 introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition])).
% 0.13/0.40 fof(f808,plain,(
% 0.13/0.40 ~inverse(sk_c8)=sk_c10|sQ38_spl),
% 0.13/0.40 inference(component_clause,[status(thm)],[f806])).
% 0.13/0.40 fof(f809,definition,(
% 0.13/0.40 sQ39_spl <=> (sk_c10=sk_c10)),
% 0.13/0.40 introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition])).
% 0.13/0.40 fof(f811,plain,(
% 0.13/0.40 ~sk_c10=sk_c10|sQ39_spl),
% 0.13/0.40 inference(component_clause,[status(thm)],[f809])).
% 0.13/0.40 fof(f812,plain,(
% 0.13/0.40 ~sQ38_spl|~sQ39_spl|~sQ20_spl|~sQ8_spl),
% 0.13/0.40 inference(split_clause,[status(thm)],[f269,f806,f809,f250,f161])).
% 0.13/0.40 fof(f813,definition,(
% 0.13/0.40 sQ40_spl <=> (inverse(sk_c2)=sk_c10)),
% 0.13/0.40 introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition])).
% 0.13/0.40 fof(f815,plain,(
% 0.13/0.40 ~inverse(sk_c2)=sk_c10|sQ40_spl),
% 0.13/0.40 inference(component_clause,[status(thm)],[f813])).
% 0.13/0.40 fof(f816,definition,(
% 0.13/0.40 sQ41_spl <=> (sk_c3=sk_c10)),
% 0.13/0.40 introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition])).
% 0.13/0.40 fof(f818,plain,(
% 0.13/0.40 ~sk_c3=sk_c10|sQ41_spl),
% 0.13/0.40 inference(component_clause,[status(thm)],[f816])).
% 0.13/0.40 fof(f819,plain,(
% 0.13/0.40 ~sQ40_spl|~sQ41_spl|~sQ20_spl|~sQ14_spl),
% 0.13/0.40 inference(split_clause,[status(thm)],[f271,f813,f816,f250,f212])).
% 0.13/0.40 fof(f821,plain,(
% 0.13/0.40 ~sk_c2=sk_c10|~sQ0_spl|~sQ11_spl|~sQ12_spl|~sQ13_spl|~sQ14_spl|~sQ15_spl|sQ40_spl),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f474,f815])).
% 0.13/0.40 fof(f822,plain,(
% 0.13/0.40 ~sk_c2=sk_c2|~sQ0_spl|~sQ11_spl|~sQ12_spl|~sQ13_spl|~sQ14_spl|~sQ15_spl|sQ40_spl),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f468,f821])).
% 0.13/0.40 fof(f823,plain,(
% 0.13/0.40 $false|~sQ0_spl|~sQ11_spl|~sQ12_spl|~sQ13_spl|~sQ14_spl|~sQ15_spl|sQ40_spl),
% 0.13/0.40 inference(trivial_equality_resolution,[status(thm)],[f822])).
% 0.13/0.40 fof(f824,plain,(
% 0.13/0.40 ~sQ0_spl|~sQ11_spl|~sQ12_spl|~sQ13_spl|~sQ14_spl|~sQ15_spl|sQ40_spl),
% 0.13/0.40 inference(contradiction_clause,[status(thm)],[f823])).
% 0.13/0.40 fof(f825,plain,(
% 0.13/0.40 ~sk_c2=sk_c10|~sQ15_spl|~sQ14_spl|~sQ11_spl|~sQ12_spl|~sQ0_spl|~sQ13_spl|sQ41_spl),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f520,f818])).
% 0.13/0.40 fof(f826,plain,(
% 0.13/0.40 ~sk_c2=sk_c2|~sQ15_spl|~sQ14_spl|~sQ11_spl|~sQ12_spl|~sQ0_spl|~sQ13_spl|sQ41_spl),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f468,f825])).
% 0.13/0.40 fof(f827,plain,(
% 0.13/0.40 $false|~sQ15_spl|~sQ14_spl|~sQ11_spl|~sQ12_spl|~sQ0_spl|~sQ13_spl|sQ41_spl),
% 0.13/0.40 inference(trivial_equality_resolution,[status(thm)],[f826])).
% 0.13/0.40 fof(f828,plain,(
% 0.13/0.40 ~sQ15_spl|~sQ14_spl|~sQ11_spl|~sQ12_spl|~sQ0_spl|~sQ13_spl|sQ41_spl),
% 0.13/0.40 inference(contradiction_clause,[status(thm)],[f827])).
% 0.13/0.40 fof(f829,plain,(
% 0.13/0.40 $false|sQ39_spl),
% 0.13/0.40 inference(trivial_equality_resolution,[status(thm)],[f811])).
% 0.13/0.40 fof(f830,plain,(
% 0.13/0.40 sQ39_spl),
% 0.13/0.40 inference(contradiction_clause,[status(thm)],[f829])).
% 0.13/0.40 fof(f833,plain,(
% 0.13/0.40 ![X0]: (multiply(sk_c11,X0)=X0|~sQ2_spl|~sQ1_spl)),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f636,f578])).
% 0.13/0.40 fof(f836,plain,(
% 0.13/0.40 ![X0]: (X0=multiply(sk_c11,multiply(sk_c1,X0))|~sQ11_spl)),
% 0.13/0.40 inference(paramodulation,[status(thm)],[f174,f286])).
% 0.13/0.40 fof(f837,plain,(
% 0.13/0.40 ![X0]: (X0=multiply(sk_c1,X0)|~sQ2_spl|~sQ1_spl|~sQ11_spl)),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f833,f836])).
% 0.13/0.40 fof(f838,plain,(
% 0.13/0.40 ![X0]: (X0=multiply(sk_c10,multiply(sk_c11,X0))|~sQ0_spl)),
% 0.13/0.40 inference(paramodulation,[status(thm)],[f131,f286])).
% 0.13/0.40 fof(f839,plain,(
% 0.13/0.40 ![X0]: (X0=multiply(sk_c10,X0)|~sQ2_spl|~sQ1_spl|~sQ0_spl)),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f833,f838])).
% 0.13/0.40 fof(f840,plain,(
% 0.13/0.40 ![X0]: (X0=multiply(sk_c11,multiply(sk_c6,X0))|~sQ4_spl)),
% 0.13/0.40 inference(paramodulation,[status(thm)],[f146,f286])).
% 0.13/0.40 fof(f841,plain,(
% 0.13/0.40 ![X0]: (X0=multiply(sk_c6,X0)|~sQ2_spl|~sQ1_spl|~sQ4_spl)),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f833,f840])).
% 0.13/0.40 fof(f851,plain,(
% 0.13/0.40 ~multiply(sk_c6,inverse(sk_c6))=sk_c11|~multiply(sk_c11,sk_c10)=sk_c11|~sQ18_spl|~sQ4_spl),
% 0.13/0.40 inference(paramodulation,[status(thm)],[f146,f276])).
% 0.13/0.40 fof(f853,plain,(
% 0.13/0.40 ~multiply(sk_c1,inverse(sk_c1))=sk_c11|~multiply(sk_c11,sk_c10)=sk_c11|~sQ18_spl|~sQ11_spl),
% 0.13/0.40 inference(paramodulation,[status(thm)],[f174,f276])).
% 0.13/0.40 fof(f872,definition,(
% 0.13/0.40 sQ47_spl <=> (multiply(sk_c6,inverse(sk_c6))=sk_c11)),
% 0.13/0.40 introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition])).
% 0.13/0.40 fof(f874,plain,(
% 0.13/0.40 ~multiply(sk_c6,inverse(sk_c6))=sk_c11|sQ47_spl),
% 0.13/0.40 inference(component_clause,[status(thm)],[f872])).
% 0.13/0.40 fof(f875,definition,(
% 0.13/0.40 sQ48_spl <=> (multiply(sk_c11,sk_c10)=sk_c11)),
% 0.13/0.40 introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition])).
% 0.13/0.40 fof(f876,plain,(
% 0.13/0.40 multiply(sk_c11,sk_c10)=sk_c11|~sQ48_spl),
% 0.13/0.40 inference(component_clause,[status(thm)],[f875])).
% 0.13/0.40 fof(f877,plain,(
% 0.13/0.40 ~multiply(sk_c11,sk_c10)=sk_c11|sQ48_spl),
% 0.13/0.40 inference(component_clause,[status(thm)],[f875])).
% 0.13/0.40 fof(f878,plain,(
% 0.13/0.40 ~sQ47_spl|~sQ48_spl|~sQ18_spl|~sQ4_spl),
% 0.13/0.40 inference(split_clause,[status(thm)],[f851,f872,f875,f244,f145])).
% 0.13/0.40 fof(f883,definition,(
% 0.13/0.40 sQ50_spl <=> (multiply(sk_c1,inverse(sk_c1))=sk_c11)),
% 0.13/0.40 introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition])).
% 0.13/0.40 fof(f885,plain,(
% 0.13/0.40 ~multiply(sk_c1,inverse(sk_c1))=sk_c11|sQ50_spl),
% 0.13/0.40 inference(component_clause,[status(thm)],[f883])).
% 0.13/0.40 fof(f886,plain,(
% 0.13/0.40 ~sQ50_spl|~sQ48_spl|~sQ18_spl|~sQ11_spl),
% 0.13/0.40 inference(split_clause,[status(thm)],[f853,f883,f875,f244,f173])).
% 0.13/0.40 fof(f887,plain,(
% 0.13/0.40 ~sk_c10=sk_c11|~sQ2_spl|~sQ1_spl|sQ48_spl),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f833,f877])).
% 0.13/0.40 fof(f888,plain,(
% 0.13/0.40 ~inverse(sk_c1)=sk_c11|~sQ2_spl|~sQ1_spl|~sQ11_spl|sQ50_spl),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f837,f885])).
% 0.13/0.40 fof(f889,plain,(
% 0.13/0.40 ~sk_c11=sk_c11|~sQ2_spl|~sQ1_spl|~sQ11_spl|sQ50_spl),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f174,f888])).
% 0.13/0.40 fof(f890,plain,(
% 0.13/0.40 $false|~sQ2_spl|~sQ1_spl|~sQ11_spl|sQ50_spl),
% 0.13/0.40 inference(trivial_equality_resolution,[status(thm)],[f889])).
% 0.13/0.40 fof(f891,plain,(
% 0.13/0.40 ~sQ2_spl|~sQ1_spl|~sQ11_spl|sQ50_spl),
% 0.13/0.40 inference(contradiction_clause,[status(thm)],[f890])).
% 0.13/0.40 fof(f894,plain,(
% 0.13/0.40 ~multiply(sk_c6,sk_c11)=sk_c11|~sQ4_spl|sQ47_spl),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f146,f874])).
% 0.13/0.40 fof(f908,plain,(
% 0.13/0.40 sk_c11=sk_c1|~sQ11_spl|~sQ2_spl|~sQ1_spl),
% 0.13/0.40 inference(backward_demodulation,[status(thm)],[f909,f636])).
% 0.13/0.40 fof(f909,plain,(
% 0.13/0.40 sk_c1=identity|~sQ2_spl|~sQ1_spl|~sQ11_spl),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f833,f612])).
% 0.13/0.40 fof(f910,plain,(
% 0.13/0.40 ~sk_c10=sk_c1|~sQ11_spl|~sQ2_spl|~sQ1_spl|sQ48_spl),
% 0.13/0.40 inference(backward_demodulation,[status(thm)],[f908,f887])).
% 0.13/0.40 fof(f913,plain,(
% 0.13/0.40 inverse(sk_c1)=sk_c10|~sQ11_spl|~sQ2_spl|~sQ1_spl|~sQ0_spl),
% 0.13/0.40 inference(backward_demodulation,[status(thm)],[f908,f131])).
% 0.13/0.40 fof(f914,plain,(
% 0.13/0.40 inverse(sk_c1)=sk_c1|~sQ2_spl|~sQ1_spl|~sQ11_spl),
% 0.13/0.40 inference(backward_demodulation,[status(thm)],[f908,f174])).
% 0.13/0.40 fof(f921,plain,(
% 0.13/0.40 sk_c1=sk_c10|~sQ11_spl|~sQ2_spl|~sQ1_spl|~sQ0_spl),
% 0.13/0.40 inference(backward_demodulation,[status(thm)],[f914,f913])).
% 0.13/0.40 fof(f923,plain,(
% 0.13/0.40 $false|sQ48_spl|~sQ11_spl|~sQ2_spl|~sQ1_spl|~sQ0_spl),
% 0.13/0.40 inference(forward_subsumption_resolution,[status(thm)],[f921,f910])).
% 0.13/0.40 fof(f924,plain,(
% 0.13/0.40 sQ48_spl|~sQ11_spl|~sQ2_spl|~sQ1_spl|~sQ0_spl),
% 0.13/0.40 inference(contradiction_clause,[status(thm)],[f923])).
% 0.13/0.40 fof(f933,plain,(
% 0.13/0.40 sk_c1=multiply(sk_c10,sk_c10)|~sQ2_spl|~sQ1_spl|~sQ0_spl|~sQ11_spl|~sQ12_spl),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f908,f630])).
% 0.13/0.40 fof(f934,plain,(
% 0.13/0.40 sk_c1=sk_c10|~sQ2_spl|~sQ1_spl|~sQ0_spl|~sQ11_spl|~sQ12_spl),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f839,f933])).
% 0.13/0.40 fof(f940,plain,(
% 0.13/0.40 multiply(sk_c1,sk_c10)=sk_c11|~sQ11_spl|~sQ2_spl|~sQ1_spl|~sQ48_spl),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f908,f876])).
% 0.13/0.40 fof(f941,plain,(
% 0.13/0.40 sk_c10=sk_c11|~sQ11_spl|~sQ2_spl|~sQ1_spl|~sQ48_spl),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f837,f940])).
% 0.13/0.40 fof(f942,plain,(
% 0.13/0.40 sk_c10=sk_c1|~sQ11_spl|~sQ2_spl|~sQ1_spl|~sQ48_spl),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f908,f941])).
% 0.13/0.40 fof(f945,plain,(
% 0.13/0.40 sk_c10=sk_c11|~sQ2_spl|~sQ1_spl|~sQ4_spl|~sQ5_spl),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f841,f150])).
% 0.13/0.40 fof(f1003,plain,(
% 0.13/0.40 ![X0]: (~multiply(X0,inverse(X0))=sk_c1|~multiply(inverse(X0),sk_c11)=sk_c10|~sQ2_spl|~sQ1_spl|~sQ0_spl|~sQ11_spl|~sQ12_spl|~sQ19_spl)),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f934,f275])).
% 0.13/0.40 fof(f1004,plain,(
% 0.13/0.40 ![X0]: (~multiply(X0,inverse(X0))=sk_c1|~multiply(inverse(X0),sk_c1)=sk_c10|~sQ2_spl|~sQ1_spl|~sQ0_spl|~sQ11_spl|~sQ12_spl|~sQ19_spl)),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f908,f1003])).
% 0.13/0.40 fof(f1005,plain,(
% 0.13/0.40 ![X0]: (~multiply(X0,inverse(X0))=sk_c1|~multiply(inverse(X0),sk_c1)=sk_c1|~sQ2_spl|~sQ1_spl|~sQ0_spl|~sQ11_spl|~sQ12_spl|~sQ19_spl)),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f934,f1004])).
% 0.13/0.40 fof(f1008,plain,(
% 0.13/0.40 ~multiply(sk_c1,inverse(sk_c1))=sk_c1|~multiply(sk_c1,sk_c1)=sk_c1|~sQ0_spl|~sQ12_spl|~sQ19_spl|~sQ2_spl|~sQ1_spl|~sQ11_spl),
% 0.13/0.40 inference(paramodulation,[status(thm)],[f914,f1005])).
% 0.13/0.40 fof(f1013,definition,(
% 0.13/0.40 sQ52_spl <=> (multiply(sk_c1,sk_c1)=sk_c1)),
% 0.13/0.40 introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition])).
% 0.13/0.40 fof(f1015,plain,(
% 0.13/0.40 ~multiply(sk_c1,sk_c1)=sk_c1|sQ52_spl),
% 0.13/0.40 inference(component_clause,[status(thm)],[f1013])).
% 0.13/0.40 fof(f1021,definition,(
% 0.13/0.40 sQ54_spl <=> (multiply(sk_c1,inverse(sk_c1))=sk_c1)),
% 0.13/0.40 introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition])).
% 0.13/0.40 fof(f1023,plain,(
% 0.13/0.40 ~multiply(sk_c1,inverse(sk_c1))=sk_c1|sQ54_spl),
% 0.13/0.40 inference(component_clause,[status(thm)],[f1021])).
% 0.13/0.40 fof(f1024,plain,(
% 0.13/0.40 ~sQ54_spl|~sQ52_spl|~sQ0_spl|~sQ12_spl|~sQ19_spl|~sQ2_spl|~sQ1_spl|~sQ11_spl),
% 0.13/0.40 inference(split_clause,[status(thm)],[f1008,f1021,f1013,f130,f186,f247,f137,f133,f173])).
% 0.13/0.40 fof(f1032,plain,(
% 0.13/0.40 ~sk_c1=sk_c1|~sQ2_spl|~sQ1_spl|~sQ11_spl|sQ52_spl),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f837,f1015])).
% 0.13/0.40 fof(f1033,plain,(
% 0.13/0.40 $false|~sQ2_spl|~sQ1_spl|~sQ11_spl|sQ52_spl),
% 0.13/0.40 inference(trivial_equality_resolution,[status(thm)],[f1032])).
% 0.13/0.40 fof(f1034,plain,(
% 0.13/0.40 ~sQ2_spl|~sQ1_spl|~sQ11_spl|sQ52_spl),
% 0.13/0.40 inference(contradiction_clause,[status(thm)],[f1033])).
% 0.13/0.40 fof(f1041,plain,(
% 0.13/0.40 ~sk_c1=sk_c11|~sQ2_spl|~sQ1_spl|~sQ0_spl|~sQ11_spl|~sQ12_spl|sQ32_spl),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f934,f593])).
% 0.13/0.40 fof(f1042,plain,(
% 0.13/0.40 ~sk_c1=sk_c1|~sQ2_spl|~sQ1_spl|~sQ0_spl|~sQ11_spl|~sQ12_spl|sQ32_spl),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f908,f1041])).
% 0.13/0.40 fof(f1043,plain,(
% 0.13/0.40 $false|~sQ2_spl|~sQ1_spl|~sQ0_spl|~sQ11_spl|~sQ12_spl|sQ32_spl),
% 0.13/0.40 inference(trivial_equality_resolution,[status(thm)],[f1042])).
% 0.13/0.40 fof(f1044,plain,(
% 0.13/0.40 ~sQ2_spl|~sQ1_spl|~sQ0_spl|~sQ11_spl|~sQ12_spl|sQ32_spl),
% 0.13/0.40 inference(contradiction_clause,[status(thm)],[f1043])).
% 0.13/0.40 fof(f1045,plain,(
% 0.13/0.40 ~inverse(inverse(sk_c1))=sk_c11|~sQ2_spl|~sQ1_spl|~sQ0_spl|~sQ11_spl|~sQ12_spl|sQ36_spl),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f934,f622])).
% 0.13/0.40 fof(f1046,plain,(
% 0.13/0.40 ~inverse(sk_c1)=sk_c11|~sQ2_spl|~sQ1_spl|~sQ0_spl|~sQ11_spl|~sQ12_spl|sQ36_spl),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f914,f1045])).
% 0.13/0.40 fof(f1047,plain,(
% 0.13/0.40 ~sk_c1=sk_c11|~sQ2_spl|~sQ1_spl|~sQ0_spl|~sQ11_spl|~sQ12_spl|sQ36_spl),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f914,f1046])).
% 0.13/0.40 fof(f1048,plain,(
% 0.13/0.40 ~sk_c1=sk_c1|~sQ2_spl|~sQ1_spl|~sQ0_spl|~sQ11_spl|~sQ12_spl|sQ36_spl),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f908,f1047])).
% 0.13/0.40 fof(f1049,plain,(
% 0.13/0.40 $false|~sQ2_spl|~sQ1_spl|~sQ0_spl|~sQ11_spl|~sQ12_spl|sQ36_spl),
% 0.13/0.40 inference(trivial_equality_resolution,[status(thm)],[f1048])).
% 0.13/0.40 fof(f1050,plain,(
% 0.13/0.40 ~sQ2_spl|~sQ1_spl|~sQ0_spl|~sQ11_spl|~sQ12_spl|sQ36_spl),
% 0.13/0.40 inference(contradiction_clause,[status(thm)],[f1049])).
% 0.13/0.40 fof(f1060,plain,(
% 0.13/0.40 ![X0]: (~multiply(sk_c1,multiply(X0,sk_c11))=sk_c10|~inverse(X0)=sk_c11|~sQ11_spl|~sQ2_spl|~sQ1_spl|~sQ17_spl)),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f908,f277])).
% 0.13/0.40 fof(f1061,plain,(
% 0.13/0.40 ![X0]: (~multiply(X0,sk_c11)=sk_c10|~inverse(X0)=sk_c11|~sQ11_spl|~sQ2_spl|~sQ1_spl|~sQ17_spl)),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f837,f1060])).
% 0.13/0.40 fof(f1062,plain,(
% 0.13/0.40 ![X0]: (~multiply(X0,sk_c1)=sk_c10|~inverse(X0)=sk_c11|~sQ11_spl|~sQ2_spl|~sQ1_spl|~sQ17_spl)),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f908,f1061])).
% 0.13/0.40 fof(f1063,plain,(
% 0.13/0.40 ![X0]: (~multiply(X0,sk_c1)=sk_c1|~inverse(X0)=sk_c11|~sQ0_spl|~sQ12_spl|~sQ11_spl|~sQ2_spl|~sQ1_spl|~sQ17_spl)),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f934,f1062])).
% 0.13/0.40 fof(f1064,plain,(
% 0.13/0.40 ![X0]: (~multiply(X0,sk_c1)=sk_c1|~inverse(X0)=sk_c1|~sQ0_spl|~sQ12_spl|~sQ11_spl|~sQ2_spl|~sQ1_spl|~sQ17_spl)),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f908,f1063])).
% 0.13/0.40 fof(f1073,plain,(
% 0.13/0.40 ![X0]: (multiply(inverse(X0),X0)=sk_c1|~sQ2_spl|~sQ1_spl|~sQ11_spl)),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f909,f66])).
% 0.13/0.40 fof(f1120,plain,(
% 0.13/0.40 ~inverse(inverse(sk_c1))=sk_c1|~sQ0_spl|~sQ12_spl|~sQ17_spl|~sQ2_spl|~sQ1_spl|~sQ11_spl),
% 0.13/0.40 inference(resolution,[status(thm)],[f1064,f1073])).
% 0.13/0.40 fof(f1125,plain,(
% 0.13/0.40 ~inverse(sk_c1)=sk_c1|~sQ0_spl|~sQ12_spl|~sQ17_spl|~sQ2_spl|~sQ1_spl|~sQ11_spl),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f914,f1120])).
% 0.13/0.40 fof(f1126,plain,(
% 0.13/0.40 ~sk_c1=sk_c1|~sQ0_spl|~sQ12_spl|~sQ17_spl|~sQ2_spl|~sQ1_spl|~sQ11_spl),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f914,f1125])).
% 0.13/0.40 fof(f1127,plain,(
% 0.13/0.40 $false|~sQ0_spl|~sQ12_spl|~sQ17_spl|~sQ2_spl|~sQ1_spl|~sQ11_spl),
% 0.13/0.40 inference(trivial_equality_resolution,[status(thm)],[f1126])).
% 0.13/0.40 fof(f1128,plain,(
% 0.13/0.40 ~sQ0_spl|~sQ12_spl|~sQ17_spl|~sQ2_spl|~sQ1_spl|~sQ11_spl),
% 0.13/0.40 inference(contradiction_clause,[status(thm)],[f1127])).
% 0.13/0.40 fof(f1136,plain,(
% 0.13/0.40 ~inverse(sk_c1)=sk_c1|~sQ2_spl|~sQ1_spl|~sQ11_spl|sQ54_spl),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f837,f1023])).
% 0.13/0.40 fof(f1137,plain,(
% 0.13/0.40 ~sk_c1=sk_c1|~sQ2_spl|~sQ1_spl|~sQ11_spl|sQ54_spl),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f914,f1136])).
% 0.13/0.40 fof(f1138,plain,(
% 0.13/0.40 $false|~sQ2_spl|~sQ1_spl|~sQ11_spl|sQ54_spl),
% 0.13/0.40 inference(trivial_equality_resolution,[status(thm)],[f1137])).
% 0.13/0.40 fof(f1139,plain,(
% 0.13/0.40 ~sQ2_spl|~sQ1_spl|~sQ11_spl|sQ54_spl),
% 0.13/0.40 inference(contradiction_clause,[status(thm)],[f1138])).
% 0.13/0.40 fof(f1166,plain,(
% 0.13/0.40 ~sk_c10=sk_c11|~sQ2_spl|~sQ1_spl|~sQ11_spl|sQ12_spl),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f837,f188])).
% 0.13/0.40 fof(f1167,plain,(
% 0.13/0.40 ~sk_c10=sk_c1|~sQ2_spl|~sQ1_spl|~sQ11_spl|sQ12_spl),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f908,f1166])).
% 0.13/0.40 fof(f1182,plain,(
% 0.13/0.40 ~sk_c1=sk_c1|~sQ48_spl|~sQ2_spl|~sQ1_spl|~sQ11_spl|sQ12_spl),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f942,f1167])).
% 0.13/0.40 fof(f1183,plain,(
% 0.13/0.40 $false|~sQ48_spl|~sQ2_spl|~sQ1_spl|~sQ11_spl|sQ12_spl),
% 0.13/0.40 inference(trivial_equality_resolution,[status(thm)],[f1182])).
% 0.13/0.40 fof(f1184,plain,(
% 0.13/0.40 ~sQ48_spl|~sQ2_spl|~sQ1_spl|~sQ11_spl|sQ12_spl),
% 0.13/0.40 inference(contradiction_clause,[status(thm)],[f1183])).
% 0.13/0.40 fof(f1191,plain,(
% 0.13/0.40 sk_c10=identity|~sQ4_spl|~sQ5_spl|~sQ2_spl|~sQ1_spl),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f945,f636])).
% 0.13/0.40 fof(f1205,plain,(
% 0.13/0.40 inverse(sk_c10)=sk_c10|~sQ2_spl|~sQ1_spl|~sQ4_spl|~sQ5_spl|~sQ0_spl),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f945,f131])).
% 0.13/0.40 fof(f1210,plain,(
% 0.13/0.40 sk_c5=multiply(sk_c5,sk_c10)|~sQ4_spl|~sQ5_spl|~sQ2_spl|~sQ1_spl),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f945,f608])).
% 0.13/0.40 fof(f1222,plain,(
% 0.13/0.40 sk_c10=sk_c5|~sQ3_spl|~sQ2_spl|~sQ1_spl|~sQ4_spl|~sQ5_spl),
% 0.13/0.40 inference(backward_demodulation,[status(thm)],[f1223,f945])).
% 0.13/0.40 fof(f1223,plain,(
% 0.13/0.40 sk_c5=sk_c11|~sQ4_spl|~sQ5_spl|~sQ2_spl|~sQ1_spl|~sQ3_spl),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f1210,f142])).
% 0.13/0.40 fof(f1227,plain,(
% 0.13/0.40 ![X0]: (~multiply(X0,inverse(X0))=sk_c10|~multiply(inverse(X0),sk_c5)=sk_c10|~sQ4_spl|~sQ5_spl|~sQ2_spl|~sQ1_spl|~sQ3_spl|~sQ19_spl)),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f1223,f275])).
% 0.13/0.40 fof(f1256,plain,(
% 0.13/0.40 ~inverse(sk_c10)=sk_c11|~sQ2_spl|~sQ1_spl|~sQ4_spl|~sQ5_spl|~sQ0_spl|sQ36_spl),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f1205,f622])).
% 0.13/0.40 fof(f1257,plain,(
% 0.13/0.40 ~sk_c10=sk_c11|~sQ2_spl|~sQ1_spl|~sQ4_spl|~sQ5_spl|~sQ0_spl|sQ36_spl),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f1205,f1256])).
% 0.13/0.40 fof(f1258,plain,(
% 0.13/0.40 ~sk_c10=sk_c5|~sQ3_spl|~sQ2_spl|~sQ1_spl|~sQ4_spl|~sQ5_spl|~sQ0_spl|sQ36_spl),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f1223,f1257])).
% 0.13/0.40 fof(f1266,plain,(
% 0.13/0.40 ![X0]: (multiply(inverse(X0),X0)=sk_c10|~sQ4_spl|~sQ5_spl|~sQ2_spl|~sQ1_spl)),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f1191,f66])).
% 0.13/0.40 fof(f1269,plain,(
% 0.13/0.40 multiply(sk_c10,sk_c9)=sk_c10|~sQ4_spl|~sQ5_spl|~sQ2_spl|~sQ1_spl|~sQ9_spl),
% 0.13/0.40 inference(paramodulation,[status(thm)],[f166,f1266])).
% 0.13/0.40 fof(f1273,plain,(
% 0.13/0.40 ![X0,X1]: (multiply(sk_c10,X0)=multiply(inverse(X1),multiply(X1,X0))|~sQ4_spl|~sQ5_spl|~sQ2_spl|~sQ1_spl)),
% 0.13/0.40 inference(paramodulation,[status(thm)],[f1266,f67])).
% 0.13/0.40 fof(f1275,plain,(
% 0.13/0.40 sk_c9=sk_c10|~sQ0_spl|~sQ4_spl|~sQ5_spl|~sQ2_spl|~sQ1_spl|~sQ9_spl),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f839,f1269])).
% 0.13/0.40 fof(f1277,plain,(
% 0.13/0.40 ![X0]: (multiply(inverse(X0),X0)=sk_c5|~sQ3_spl|~sQ4_spl|~sQ5_spl|~sQ2_spl|~sQ1_spl)),
% 0.13/0.40 inference(backward_demodulation,[status(thm)],[f1222,f1266])).
% 0.13/0.40 fof(f1286,plain,(
% 0.13/0.40 inverse(sk_c9)=sk_c5|~sQ3_spl|~sQ2_spl|~sQ1_spl|~sQ4_spl|~sQ5_spl|~sQ9_spl),
% 0.13/0.40 inference(backward_demodulation,[status(thm)],[f1222,f166])).
% 0.13/0.40 fof(f1288,plain,(
% 0.13/0.40 ~inverse(sk_c8)=sk_c5|~sQ3_spl|~sQ2_spl|~sQ1_spl|~sQ4_spl|~sQ5_spl|sQ38_spl),
% 0.13/0.40 inference(backward_demodulation,[status(thm)],[f1222,f808])).
% 0.13/0.40 fof(f1297,plain,(
% 0.13/0.40 ~sk_c5=sk_c5|~sQ3_spl|~sQ2_spl|~sQ1_spl|~sQ4_spl|~sQ5_spl|~sQ0_spl|sQ36_spl),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f1222,f1258])).
% 0.13/0.40 fof(f1298,plain,(
% 0.13/0.40 $false|~sQ3_spl|~sQ2_spl|~sQ1_spl|~sQ4_spl|~sQ5_spl|~sQ0_spl|sQ36_spl),
% 0.13/0.40 inference(trivial_equality_resolution,[status(thm)],[f1297])).
% 0.13/0.40 fof(f1299,plain,(
% 0.13/0.40 ~sQ3_spl|~sQ2_spl|~sQ1_spl|~sQ4_spl|~sQ5_spl|~sQ0_spl|sQ36_spl),
% 0.13/0.40 inference(contradiction_clause,[status(thm)],[f1298])).
% 0.13/0.40 fof(f1305,plain,(
% 0.13/0.40 ~sk_c5=sk_c11|~sQ3_spl|~sQ4_spl|~sQ5_spl|~sQ2_spl|~sQ1_spl|sQ48_spl),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f1222,f887])).
% 0.13/0.40 fof(f1306,plain,(
% 0.13/0.40 ~sk_c5=sk_c5|~sQ3_spl|~sQ4_spl|~sQ5_spl|~sQ2_spl|~sQ1_spl|sQ48_spl),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f1223,f1305])).
% 0.13/0.40 fof(f1307,plain,(
% 0.13/0.40 $false|~sQ3_spl|~sQ4_spl|~sQ5_spl|~sQ2_spl|~sQ1_spl|sQ48_spl),
% 0.13/0.40 inference(trivial_equality_resolution,[status(thm)],[f1306])).
% 0.13/0.40 fof(f1308,plain,(
% 0.13/0.40 ~sQ3_spl|~sQ4_spl|~sQ5_spl|~sQ2_spl|~sQ1_spl|sQ48_spl),
% 0.13/0.40 inference(contradiction_clause,[status(thm)],[f1307])).
% 0.13/0.40 fof(f1309,plain,(
% 0.13/0.40 ![X0,X1]: (multiply(sk_c5,X0)=multiply(inverse(X1),multiply(X1,X0))|~sQ3_spl|~sQ4_spl|~sQ5_spl|~sQ2_spl|~sQ1_spl)),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f1222,f1273])).
% 0.13/0.40 fof(f1310,plain,(
% 0.13/0.40 ![X0]: (multiply(sk_c5,X0)=X0|~sQ3_spl|~sQ4_spl|~sQ5_spl|~sQ2_spl|~sQ1_spl)),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f286,f1309])).
% 0.13/0.40 fof(f1322,plain,(
% 0.13/0.40 ~inverse(sk_c5)=sk_c10|~sQ4_spl|~sQ5_spl|~sQ2_spl|~sQ1_spl|~sQ3_spl|sQ0_spl),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f1223,f132])).
% 0.13/0.40 fof(f1323,plain,(
% 0.13/0.40 ~inverse(sk_c5)=sk_c5|~sQ4_spl|~sQ5_spl|~sQ2_spl|~sQ1_spl|~sQ3_spl|sQ0_spl),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f1222,f1322])).
% 0.13/0.40 fof(f1341,plain,(
% 0.13/0.40 multiply(sk_c8,sk_c5)=sk_c10|~sQ4_spl|~sQ5_spl|~sQ2_spl|~sQ1_spl|~sQ3_spl|~sQ8_spl),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f1223,f162])).
% 0.13/0.40 fof(f1342,plain,(
% 0.13/0.40 multiply(sk_c8,sk_c5)=sk_c5|~sQ4_spl|~sQ5_spl|~sQ2_spl|~sQ1_spl|~sQ3_spl|~sQ8_spl),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f1222,f1341])).
% 0.13/0.40 fof(f1344,plain,(
% 0.13/0.40 ![X0]: (multiply(sk_c5,X0)=multiply(sk_c8,multiply(sk_c5,X0))|~sQ4_spl|~sQ5_spl|~sQ2_spl|~sQ1_spl|~sQ3_spl|~sQ8_spl)),
% 0.13/0.40 inference(paramodulation,[status(thm)],[f1342,f67])).
% 0.13/0.40 fof(f1345,plain,(
% 0.13/0.40 ![X0]: (X0=multiply(sk_c8,multiply(sk_c5,X0))|~sQ4_spl|~sQ5_spl|~sQ2_spl|~sQ1_spl|~sQ3_spl|~sQ8_spl)),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f1310,f1344])).
% 0.13/0.40 fof(f1346,plain,(
% 0.13/0.40 ![X0]: (X0=multiply(sk_c8,X0)|~sQ4_spl|~sQ5_spl|~sQ2_spl|~sQ1_spl|~sQ3_spl|~sQ8_spl)),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f1310,f1345])).
% 0.13/0.40 fof(f1357,plain,(
% 0.13/0.40 sk_c8=sk_c5|~sQ8_spl|~sQ7_spl|~sQ6_spl|~sQ3_spl|~sQ2_spl|~sQ1_spl|~sQ4_spl|~sQ5_spl),
% 0.13/0.40 inference(backward_demodulation,[status(thm)],[f1358,f1222])).
% 0.13/0.40 fof(f1358,plain,(
% 0.13/0.40 sk_c8=sk_c10|~sQ4_spl|~sQ5_spl|~sQ2_spl|~sQ1_spl|~sQ3_spl|~sQ8_spl|~sQ7_spl|~sQ6_spl),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f1346,f571])).
% 0.13/0.40 fof(f1359,plain,(
% 0.13/0.40 ~inverse(sk_c5)=sk_c8|~sQ8_spl|~sQ7_spl|~sQ6_spl|~sQ4_spl|~sQ5_spl|~sQ2_spl|~sQ1_spl|~sQ3_spl|sQ0_spl),
% 0.13/0.40 inference(backward_demodulation,[status(thm)],[f1357,f1323])).
% 0.13/0.40 fof(f1362,plain,(
% 0.13/0.40 ~inverse(sk_c8)=sk_c8|~sQ8_spl|~sQ7_spl|~sQ6_spl|~sQ3_spl|~sQ2_spl|~sQ1_spl|~sQ4_spl|~sQ5_spl|sQ38_spl),
% 0.13/0.40 inference(backward_demodulation,[status(thm)],[f1357,f1288])).
% 0.13/0.40 fof(f1363,plain,(
% 0.13/0.40 inverse(sk_c9)=sk_c8|~sQ8_spl|~sQ7_spl|~sQ6_spl|~sQ3_spl|~sQ2_spl|~sQ1_spl|~sQ4_spl|~sQ5_spl|~sQ9_spl),
% 0.13/0.40 inference(backward_demodulation,[status(thm)],[f1357,f1286])).
% 0.13/0.40 fof(f1367,plain,(
% 0.13/0.40 sk_c8=sk_c11|~sQ8_spl|~sQ7_spl|~sQ6_spl|~sQ4_spl|~sQ5_spl|~sQ2_spl|~sQ1_spl|~sQ3_spl),
% 0.13/0.40 inference(backward_demodulation,[status(thm)],[f1357,f1223])).
% 0.13/0.40 fof(f1368,plain,(
% 0.13/0.40 inverse(sk_c4)=sk_c8|~sQ8_spl|~sQ7_spl|~sQ6_spl|~sQ3_spl|~sQ1_spl|~sQ4_spl|~sQ5_spl|~sQ2_spl),
% 0.13/0.40 inference(backward_demodulation,[status(thm)],[f1357,f138])).
% 0.13/0.40 fof(f1369,plain,(
% 0.13/0.40 ~inverse(sk_c8)=sk_c8|~sQ8_spl|~sQ7_spl|~sQ6_spl|~sQ4_spl|~sQ5_spl|~sQ2_spl|~sQ1_spl|~sQ3_spl|sQ0_spl),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f1357,f1359])).
% 0.13/0.40 fof(f1370,plain,(
% 0.13/0.40 ![X0]: (X0=multiply(sk_c8,multiply(sk_c9,X0))|~sQ8_spl|~sQ7_spl|~sQ6_spl|~sQ3_spl|~sQ2_spl|~sQ1_spl|~sQ4_spl|~sQ5_spl|~sQ9_spl)),
% 0.13/0.40 inference(paramodulation,[status(thm)],[f1363,f286])).
% 0.13/0.40 fof(f1371,plain,(
% 0.13/0.40 ![X0]: (X0=multiply(sk_c9,X0)|~sQ8_spl|~sQ7_spl|~sQ6_spl|~sQ3_spl|~sQ2_spl|~sQ1_spl|~sQ4_spl|~sQ5_spl|~sQ9_spl)),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f1346,f1370])).
% 0.13/0.40 fof(f1382,plain,(
% 0.13/0.40 ![X0]: (multiply(inverse(X0),X0)=sk_c8|~sQ8_spl|~sQ7_spl|~sQ6_spl|~sQ3_spl|~sQ4_spl|~sQ5_spl|~sQ2_spl|~sQ1_spl)),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f1357,f1277])).
% 0.13/0.40 fof(f1383,plain,(
% 0.13/0.40 multiply(sk_c8,sk_c4)=sk_c8|~sQ8_spl|~sQ7_spl|~sQ6_spl|~sQ3_spl|~sQ1_spl|~sQ4_spl|~sQ5_spl|~sQ2_spl),
% 0.13/0.40 inference(paramodulation,[status(thm)],[f1368,f1382])).
% 0.13/0.40 fof(f1385,plain,(
% 0.13/0.40 multiply(sk_c8,sk_c9)=sk_c8|~sQ8_spl|~sQ7_spl|~sQ6_spl|~sQ3_spl|~sQ2_spl|~sQ1_spl|~sQ4_spl|~sQ5_spl|~sQ9_spl),
% 0.13/0.40 inference(paramodulation,[status(thm)],[f1363,f1382])).
% 0.13/0.40 fof(f1389,plain,(
% 0.13/0.40 sk_c4=sk_c8|~sQ8_spl|~sQ7_spl|~sQ6_spl|~sQ3_spl|~sQ1_spl|~sQ4_spl|~sQ5_spl|~sQ2_spl),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f1346,f1383])).
% 0.13/0.40 fof(f1391,plain,(
% 0.13/0.40 sk_c9=sk_c8|~sQ8_spl|~sQ7_spl|~sQ6_spl|~sQ3_spl|~sQ2_spl|~sQ1_spl|~sQ4_spl|~sQ5_spl|~sQ9_spl),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f1346,f1385])).
% 0.13/0.40 fof(f1400,plain,(
% 0.13/0.40 inverse(sk_c8)=sk_c8|~sQ8_spl|~sQ7_spl|~sQ6_spl|~sQ3_spl|~sQ1_spl|~sQ4_spl|~sQ5_spl|~sQ2_spl),
% 0.13/0.40 inference(backward_demodulation,[status(thm)],[f1389,f1368])).
% 0.13/0.40 fof(f1402,plain,(
% 0.13/0.40 $false|sQ0_spl|~sQ8_spl|~sQ7_spl|~sQ6_spl|~sQ3_spl|~sQ1_spl|~sQ4_spl|~sQ5_spl|~sQ2_spl),
% 0.13/0.40 inference(forward_subsumption_resolution,[status(thm)],[f1400,f1369])).
% 0.13/0.40 fof(f1403,plain,(
% 0.13/0.40 sQ0_spl|~sQ8_spl|~sQ7_spl|~sQ6_spl|~sQ3_spl|~sQ1_spl|~sQ4_spl|~sQ5_spl|~sQ2_spl),
% 0.13/0.40 inference(contradiction_clause,[status(thm)],[f1402])).
% 0.13/0.40 fof(f1440,plain,(
% 0.13/0.40 ~sk_c11=sk_c11|~sQ2_spl|~sQ1_spl|~sQ4_spl|sQ47_spl),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f841,f894])).
% 0.13/0.40 fof(f1441,plain,(
% 0.13/0.40 ~sk_c8=sk_c11|~sQ8_spl|~sQ7_spl|~sQ6_spl|~sQ5_spl|~sQ3_spl|~sQ2_spl|~sQ1_spl|~sQ4_spl|sQ47_spl),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f1367,f1440])).
% 0.13/0.40 fof(f1442,plain,(
% 0.13/0.40 ~sk_c8=sk_c8|~sQ8_spl|~sQ7_spl|~sQ6_spl|~sQ5_spl|~sQ3_spl|~sQ2_spl|~sQ1_spl|~sQ4_spl|sQ47_spl),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f1367,f1441])).
% 0.13/0.40 fof(f1443,plain,(
% 0.13/0.40 $false|~sQ8_spl|~sQ7_spl|~sQ6_spl|~sQ5_spl|~sQ3_spl|~sQ2_spl|~sQ1_spl|~sQ4_spl|sQ47_spl),
% 0.13/0.40 inference(trivial_equality_resolution,[status(thm)],[f1442])).
% 0.13/0.40 fof(f1444,plain,(
% 0.13/0.40 ~sQ8_spl|~sQ7_spl|~sQ6_spl|~sQ5_spl|~sQ3_spl|~sQ2_spl|~sQ1_spl|~sQ4_spl|sQ47_spl),
% 0.13/0.40 inference(contradiction_clause,[status(thm)],[f1443])).
% 0.13/0.40 fof(f1445,plain,(
% 0.13/0.40 ![X0]: (~multiply(X0,inverse(X0))=sk_c8|~multiply(inverse(X0),sk_c5)=sk_c10|~sQ8_spl|~sQ7_spl|~sQ6_spl|~sQ4_spl|~sQ5_spl|~sQ2_spl|~sQ1_spl|~sQ3_spl|~sQ19_spl)),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f1358,f1227])).
% 0.13/0.40 fof(f1446,plain,(
% 0.13/0.40 ![X0]: (~multiply(X0,inverse(X0))=sk_c8|~multiply(inverse(X0),sk_c8)=sk_c10|~sQ8_spl|~sQ7_spl|~sQ6_spl|~sQ4_spl|~sQ5_spl|~sQ2_spl|~sQ1_spl|~sQ3_spl|~sQ19_spl)),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f1357,f1445])).
% 0.13/0.40 fof(f1447,plain,(
% 0.13/0.40 ![X0]: (~multiply(X0,inverse(X0))=sk_c8|~multiply(inverse(X0),sk_c8)=sk_c8|~sQ8_spl|~sQ7_spl|~sQ6_spl|~sQ4_spl|~sQ5_spl|~sQ2_spl|~sQ1_spl|~sQ3_spl|~sQ19_spl)),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f1358,f1446])).
% 0.13/0.40 fof(f1459,plain,(
% 0.13/0.40 ![X0]: (multiply(inverse(X0),X0)=sk_c9|~sQ9_spl|~sQ8_spl|~sQ7_spl|~sQ6_spl|~sQ3_spl|~sQ4_spl|~sQ5_spl|~sQ2_spl|~sQ1_spl)),
% 0.13/0.40 inference(backward_demodulation,[status(thm)],[f1391,f1382])).
% 0.13/0.40 fof(f1462,plain,(
% 0.13/0.40 sk_c9=sk_c11|~sQ9_spl|~sQ8_spl|~sQ7_spl|~sQ6_spl|~sQ4_spl|~sQ5_spl|~sQ2_spl|~sQ1_spl|~sQ3_spl),
% 0.13/0.40 inference(backward_demodulation,[status(thm)],[f1391,f1367])).
% 0.13/0.40 fof(f1472,plain,(
% 0.13/0.40 inverse(sk_c9)=sk_c8|~sQ9_spl|~sQ8_spl|~sQ7_spl|~sQ6_spl|~sQ3_spl|~sQ1_spl|~sQ4_spl|~sQ5_spl|~sQ2_spl),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f1391,f1400])).
% 0.13/0.40 fof(f1473,plain,(
% 0.13/0.40 inverse(sk_c9)=sk_c9|~sQ9_spl|~sQ8_spl|~sQ7_spl|~sQ6_spl|~sQ3_spl|~sQ1_spl|~sQ4_spl|~sQ5_spl|~sQ2_spl),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f1391,f1472])).
% 0.13/0.40 fof(f1480,plain,(
% 0.13/0.40 ![X0]: (~multiply(X0,inverse(X0))=sk_c9|~multiply(inverse(X0),sk_c8)=sk_c8|~sQ9_spl|~sQ8_spl|~sQ7_spl|~sQ6_spl|~sQ4_spl|~sQ5_spl|~sQ2_spl|~sQ1_spl|~sQ3_spl|~sQ19_spl)),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f1391,f1447])).
% 0.13/0.40 fof(f1481,plain,(
% 0.13/0.40 ![X0]: (~multiply(X0,inverse(X0))=sk_c9|~multiply(inverse(X0),sk_c9)=sk_c8|~sQ9_spl|~sQ8_spl|~sQ7_spl|~sQ6_spl|~sQ4_spl|~sQ5_spl|~sQ2_spl|~sQ1_spl|~sQ3_spl|~sQ19_spl)),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f1391,f1480])).
% 0.13/0.40 fof(f1482,plain,(
% 0.13/0.40 ![X0]: (~multiply(X0,inverse(X0))=sk_c9|~multiply(inverse(X0),sk_c9)=sk_c9|~sQ9_spl|~sQ8_spl|~sQ7_spl|~sQ6_spl|~sQ4_spl|~sQ5_spl|~sQ2_spl|~sQ1_spl|~sQ3_spl|~sQ19_spl)),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f1391,f1481])).
% 0.13/0.40 fof(f1483,plain,(
% 0.13/0.40 ~multiply(sk_c9,inverse(sk_c9))=sk_c9|~multiply(sk_c9,sk_c9)=sk_c9|~sQ19_spl|~sQ9_spl|~sQ8_spl|~sQ7_spl|~sQ6_spl|~sQ3_spl|~sQ1_spl|~sQ4_spl|~sQ5_spl|~sQ2_spl),
% 0.13/0.40 inference(paramodulation,[status(thm)],[f1473,f1482])).
% 0.13/0.40 fof(f1484,definition,(
% 0.13/0.40 sQ61_spl <=> (multiply(sk_c9,inverse(sk_c9))=sk_c9)),
% 0.13/0.40 introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition])).
% 0.13/0.40 fof(f1486,plain,(
% 0.13/0.40 ~multiply(sk_c9,inverse(sk_c9))=sk_c9|sQ61_spl),
% 0.13/0.40 inference(component_clause,[status(thm)],[f1484])).
% 0.13/0.40 fof(f1487,definition,(
% 0.13/0.40 sQ62_spl <=> (multiply(sk_c9,sk_c9)=sk_c9)),
% 0.13/0.40 introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition])).
% 0.13/0.40 fof(f1489,plain,(
% 0.13/0.40 ~multiply(sk_c9,sk_c9)=sk_c9|sQ62_spl),
% 0.13/0.40 inference(component_clause,[status(thm)],[f1487])).
% 0.13/0.40 fof(f1490,plain,(
% 0.13/0.40 ~sQ61_spl|~sQ62_spl|~sQ19_spl|~sQ9_spl|~sQ8_spl|~sQ7_spl|~sQ6_spl|~sQ3_spl|~sQ1_spl|~sQ4_spl|~sQ5_spl|~sQ2_spl),
% 0.13/0.40 inference(split_clause,[status(thm)],[f1483,f1484,f1487,f247,f165,f161,f157,f153,f141,f133,f145,f149,f137])).
% 0.13/0.40 fof(f1491,plain,(
% 0.13/0.40 ~inverse(sk_c9)=sk_c9|~sQ8_spl|~sQ7_spl|~sQ6_spl|~sQ3_spl|~sQ2_spl|~sQ1_spl|~sQ4_spl|~sQ5_spl|~sQ9_spl|sQ61_spl),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f1371,f1486])).
% 0.13/0.40 fof(f1492,plain,(
% 0.13/0.40 ~sk_c9=sk_c9|~sQ8_spl|~sQ7_spl|~sQ6_spl|~sQ3_spl|~sQ2_spl|~sQ1_spl|~sQ4_spl|~sQ5_spl|~sQ9_spl|sQ61_spl),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f1473,f1491])).
% 0.13/0.40 fof(f1493,plain,(
% 0.13/0.40 $false|~sQ8_spl|~sQ7_spl|~sQ6_spl|~sQ3_spl|~sQ2_spl|~sQ1_spl|~sQ4_spl|~sQ5_spl|~sQ9_spl|sQ61_spl),
% 0.13/0.40 inference(trivial_equality_resolution,[status(thm)],[f1492])).
% 0.13/0.40 fof(f1494,plain,(
% 0.13/0.40 ~sQ8_spl|~sQ7_spl|~sQ6_spl|~sQ3_spl|~sQ2_spl|~sQ1_spl|~sQ4_spl|~sQ5_spl|~sQ9_spl|sQ61_spl),
% 0.13/0.40 inference(contradiction_clause,[status(thm)],[f1493])).
% 0.13/0.40 fof(f1495,plain,(
% 0.13/0.40 ~sk_c9=sk_c9|~sQ8_spl|~sQ7_spl|~sQ6_spl|~sQ3_spl|~sQ2_spl|~sQ1_spl|~sQ4_spl|~sQ5_spl|~sQ9_spl|sQ62_spl),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f1371,f1489])).
% 0.13/0.40 fof(f1496,plain,(
% 0.13/0.40 $false|~sQ8_spl|~sQ7_spl|~sQ6_spl|~sQ3_spl|~sQ2_spl|~sQ1_spl|~sQ4_spl|~sQ5_spl|~sQ9_spl|sQ62_spl),
% 0.13/0.40 inference(trivial_equality_resolution,[status(thm)],[f1495])).
% 0.13/0.40 fof(f1497,plain,(
% 0.13/0.40 ~sQ8_spl|~sQ7_spl|~sQ6_spl|~sQ3_spl|~sQ2_spl|~sQ1_spl|~sQ4_spl|~sQ5_spl|~sQ9_spl|sQ62_spl),
% 0.13/0.40 inference(contradiction_clause,[status(thm)],[f1496])).
% 0.13/0.40 fof(f1499,plain,(
% 0.13/0.40 ![X0]: (~multiply(sk_c9,multiply(X0,sk_c11))=sk_c10|~inverse(X0)=sk_c11|~sQ9_spl|~sQ8_spl|~sQ7_spl|~sQ6_spl|~sQ4_spl|~sQ5_spl|~sQ2_spl|~sQ1_spl|~sQ3_spl|~sQ17_spl)),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f1462,f277])).
% 0.13/0.40 fof(f1500,plain,(
% 0.13/0.40 ![X0]: (~multiply(X0,sk_c11)=sk_c10|~inverse(X0)=sk_c11|~sQ9_spl|~sQ8_spl|~sQ7_spl|~sQ6_spl|~sQ4_spl|~sQ5_spl|~sQ2_spl|~sQ1_spl|~sQ3_spl|~sQ17_spl)),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f1371,f1499])).
% 0.13/0.40 fof(f1501,plain,(
% 0.13/0.40 ![X0]: (~multiply(X0,sk_c9)=sk_c10|~inverse(X0)=sk_c11|~sQ9_spl|~sQ8_spl|~sQ7_spl|~sQ6_spl|~sQ4_spl|~sQ5_spl|~sQ2_spl|~sQ1_spl|~sQ3_spl|~sQ17_spl)),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f1462,f1500])).
% 0.13/0.40 fof(f1502,plain,(
% 0.13/0.40 ![X0]: (~multiply(X0,sk_c9)=sk_c9|~inverse(X0)=sk_c11|~sQ0_spl|~sQ9_spl|~sQ8_spl|~sQ7_spl|~sQ6_spl|~sQ4_spl|~sQ5_spl|~sQ2_spl|~sQ1_spl|~sQ3_spl|~sQ17_spl)),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f1275,f1501])).
% 0.13/0.40 fof(f1503,plain,(
% 0.13/0.40 ![X0]: (~multiply(X0,sk_c9)=sk_c9|~inverse(X0)=sk_c9|~sQ0_spl|~sQ9_spl|~sQ8_spl|~sQ7_spl|~sQ6_spl|~sQ4_spl|~sQ5_spl|~sQ2_spl|~sQ1_spl|~sQ3_spl|~sQ17_spl)),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f1462,f1502])).
% 0.13/0.40 fof(f1504,plain,(
% 0.13/0.40 ~inverse(sk_c9)=sk_c8|~sQ9_spl|~sQ8_spl|~sQ7_spl|~sQ6_spl|~sQ3_spl|~sQ2_spl|~sQ1_spl|~sQ4_spl|~sQ5_spl|sQ38_spl),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f1391,f1362])).
% 0.13/0.40 fof(f1505,plain,(
% 0.13/0.40 ~sk_c9=sk_c8|~sQ9_spl|~sQ8_spl|~sQ7_spl|~sQ6_spl|~sQ3_spl|~sQ2_spl|~sQ1_spl|~sQ4_spl|~sQ5_spl|sQ38_spl),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f1473,f1504])).
% 0.13/0.40 fof(f1506,plain,(
% 0.13/0.40 ~sk_c9=sk_c9|~sQ9_spl|~sQ8_spl|~sQ7_spl|~sQ6_spl|~sQ3_spl|~sQ2_spl|~sQ1_spl|~sQ4_spl|~sQ5_spl|sQ38_spl),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f1391,f1505])).
% 0.13/0.40 fof(f1507,plain,(
% 0.13/0.40 $false|~sQ9_spl|~sQ8_spl|~sQ7_spl|~sQ6_spl|~sQ3_spl|~sQ2_spl|~sQ1_spl|~sQ4_spl|~sQ5_spl|sQ38_spl),
% 0.13/0.40 inference(trivial_equality_resolution,[status(thm)],[f1506])).
% 0.13/0.40 fof(f1508,plain,(
% 0.13/0.40 ~sQ9_spl|~sQ8_spl|~sQ7_spl|~sQ6_spl|~sQ3_spl|~sQ2_spl|~sQ1_spl|~sQ4_spl|~sQ5_spl|sQ38_spl),
% 0.13/0.40 inference(contradiction_clause,[status(thm)],[f1507])).
% 0.13/0.40 fof(f1564,plain,(
% 0.13/0.40 ~inverse(inverse(sk_c9))=sk_c9|~sQ0_spl|~sQ17_spl|~sQ9_spl|~sQ8_spl|~sQ7_spl|~sQ6_spl|~sQ3_spl|~sQ4_spl|~sQ5_spl|~sQ2_spl|~sQ1_spl),
% 0.13/0.40 inference(resolution,[status(thm)],[f1503,f1459])).
% 0.13/0.40 fof(f1569,plain,(
% 0.13/0.40 ~inverse(sk_c9)=sk_c9|~sQ0_spl|~sQ17_spl|~sQ9_spl|~sQ8_spl|~sQ7_spl|~sQ6_spl|~sQ3_spl|~sQ4_spl|~sQ5_spl|~sQ2_spl|~sQ1_spl),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f1473,f1564])).
% 0.13/0.40 fof(f1570,plain,(
% 0.13/0.40 ~sk_c9=sk_c9|~sQ0_spl|~sQ17_spl|~sQ9_spl|~sQ8_spl|~sQ7_spl|~sQ6_spl|~sQ3_spl|~sQ4_spl|~sQ5_spl|~sQ2_spl|~sQ1_spl),
% 0.13/0.40 inference(forward_demodulation,[status(thm)],[f1473,f1569])).
% 0.13/0.40 fof(f1571,plain,(
% 0.13/0.40 $false|~sQ0_spl|~sQ17_spl|~sQ9_spl|~sQ8_spl|~sQ7_spl|~sQ6_spl|~sQ3_spl|~sQ4_spl|~sQ5_spl|~sQ2_spl|~sQ1_spl),
% 0.13/0.40 inference(trivial_equality_resolution,[status(thm)],[f1570])).
% 0.13/0.40 fof(f1572,plain,(
% 0.13/0.40 ~sQ0_spl|~sQ17_spl|~sQ9_spl|~sQ8_spl|~sQ7_spl|~sQ6_spl|~sQ3_spl|~sQ4_spl|~sQ5_spl|~sQ2_spl|~sQ1_spl),
% 0.13/0.40 inference(contradiction_clause,[status(thm)],[f1571])).
% 0.13/0.40 fof(f1573,plain,(
% 0.13/0.40 $false),
% 0.13/0.40 inference(sat_refutation,[status(thm)],[f136,f140,f144,f148,f152,f156,f160,f164,f176,f177,f178,f179,f180,f181,f182,f183,f184,f189,f190,f202,f203,f210,f211,f215,f216,f223,f224,f228,f229,f236,f237,f253,f274,f390,f432,f539,f563,f594,f605,f626,f638,f673,f677,f714,f791,f812,f819,f824,f828,f830,f878,f886,f891,f924,f1024,f1034,f1044,f1050,f1128,f1139,f1184,f1299,f1308,f1403,f1444,f1490,f1494,f1497,f1508,f1572])).
% 0.13/0.40 % SZS output end CNFRefutation for theBenchmark.p
% 0.13/0.42 % Elapsed time: 0.053757 seconds
% 0.13/0.42 % CPU time: 0.195255 seconds
% 0.13/0.42 % Total memory used: 35.434 MB
% 0.13/0.42 % Net memory used: 35.359 MB
%------------------------------------------------------------------------------