%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GRP325-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 : n010.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:27 PM UTC 2026
% Result : Unsatisfiable 0.10s 0.41s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP325-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.10/0.37 % Computer : n010.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Sun Sep 20 20:09:55 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.38 % Drodi V4.1.1
% 0.10/0.41 % Refutation found
% 0.10/0.41 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.10/0.41 % SZS output start CNFRefutation for theBenchmark
% 0.10/0.41 fof(f1,axiom,(
% 0.10/0.41 (![X]: (multiply(identity,X) = X ))),
% 0.10/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.41 fof(f2,axiom,(
% 0.10/0.41 (![X]: (multiply(inverse(X),X) = identity ))),
% 0.10/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.41 fof(f3,axiom,(
% 0.10/0.41 (![X,Y,Z]: (multiply(multiply(X,Y),Z) = multiply(X,multiply(Y,Z)) ))),
% 0.10/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.41 fof(f4,negated_conjecture,(
% 0.10/0.41 multiply(sk_c9,sk_c10) = sk_c8 ),
% 0.10/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.41 fof(f5,negated_conjecture,(
% 0.10/0.41 ( multiply(sk_c1,sk_c9) = sk_c10| multiply(sk_c4,sk_c10) = sk_c9 ) ),
% 0.10/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.41 fof(f6,negated_conjecture,(
% 0.10/0.41 ( multiply(sk_c1,sk_c9) = sk_c10| inverse(sk_c4) = sk_c10 ) ),
% 0.10/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.41 fof(f7,negated_conjecture,(
% 0.10/0.41 ( multiply(sk_c1,sk_c9) = sk_c10| inverse(sk_c9) = sk_c8 ) ),
% 0.10/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.41 fof(f8,negated_conjecture,(
% 0.10/0.41 ( multiply(sk_c1,sk_c9) = sk_c10| multiply(sk_c10,sk_c8) = sk_c9 ) ),
% 0.10/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.41 fof(f9,negated_conjecture,(
% 0.10/0.41 ( multiply(sk_c1,sk_c9) = sk_c10| inverse(sk_c5) = sk_c9 ) ),
% 0.10/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.41 fof(f10,negated_conjecture,(
% 0.10/0.41 ( multiply(sk_c1,sk_c9) = sk_c10| multiply(sk_c5,sk_c8) = sk_c9 ) ),
% 0.10/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.41 fof(f11,negated_conjecture,(
% 0.10/0.41 ( multiply(sk_c1,sk_c9) = sk_c10| inverse(sk_c7) = sk_c6 ) ),
% 0.10/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.41 fof(f12,negated_conjecture,(
% 0.10/0.41 ( multiply(sk_c1,sk_c9) = sk_c10| inverse(sk_c6) = sk_c10 ) ),
% 0.10/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.41 fof(f14,negated_conjecture,(
% 0.10/0.41 ( inverse(sk_c1) = sk_c9| multiply(sk_c4,sk_c10) = sk_c9 ) ),
% 0.10/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.41 fof(f15,negated_conjecture,(
% 0.10/0.41 ( inverse(sk_c1) = sk_c9| inverse(sk_c4) = sk_c10 ) ),
% 0.10/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.41 fof(f16,negated_conjecture,(
% 0.10/0.41 ( inverse(sk_c1) = sk_c9| inverse(sk_c9) = sk_c8 ) ),
% 0.10/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.41 fof(f17,negated_conjecture,(
% 0.10/0.41 ( inverse(sk_c1) = sk_c9| multiply(sk_c10,sk_c8) = sk_c9 ) ),
% 0.10/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.41 fof(f18,negated_conjecture,(
% 0.10/0.41 ( inverse(sk_c1) = sk_c9| inverse(sk_c5) = sk_c9 ) ),
% 0.10/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.41 fof(f19,negated_conjecture,(
% 0.10/0.41 ( inverse(sk_c1) = sk_c9| multiply(sk_c5,sk_c8) = sk_c9 ) ),
% 0.10/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.41 fof(f20,negated_conjecture,(
% 0.10/0.41 ( inverse(sk_c1) = sk_c9| inverse(sk_c7) = sk_c6 ) ),
% 0.10/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.41 fof(f21,negated_conjecture,(
% 0.10/0.41 ( inverse(sk_c1) = sk_c9| inverse(sk_c6) = sk_c10 ) ),
% 0.10/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.41 fof(f23,negated_conjecture,(
% 0.10/0.41 ( multiply(sk_c10,sk_c3) = sk_c9| multiply(sk_c4,sk_c10) = sk_c9 ) ),
% 0.10/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.41 fof(f24,negated_conjecture,(
% 0.10/0.41 ( multiply(sk_c10,sk_c3) = sk_c9| inverse(sk_c4) = sk_c10 ) ),
% 0.10/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.41 fof(f25,negated_conjecture,(
% 0.10/0.41 ( multiply(sk_c10,sk_c3) = sk_c9| inverse(sk_c9) = sk_c8 ) ),
% 0.10/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.41 fof(f26,negated_conjecture,(
% 0.10/0.41 ( multiply(sk_c10,sk_c3) = sk_c9| multiply(sk_c10,sk_c8) = sk_c9 ) ),
% 0.10/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.41 fof(f27,negated_conjecture,(
% 0.10/0.41 ( multiply(sk_c10,sk_c3) = sk_c9| inverse(sk_c5) = sk_c9 ) ),
% 0.10/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.41 fof(f28,negated_conjecture,(
% 0.10/0.41 ( multiply(sk_c10,sk_c3) = sk_c9| multiply(sk_c5,sk_c8) = sk_c9 ) ),
% 0.10/0.41 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.42 fof(f32,negated_conjecture,(
% 0.10/0.42 ( multiply(sk_c2,sk_c10) = sk_c3| multiply(sk_c4,sk_c10) = sk_c9 ) ),
% 0.10/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.42 fof(f33,negated_conjecture,(
% 0.10/0.42 ( multiply(sk_c2,sk_c10) = sk_c3| inverse(sk_c4) = sk_c10 ) ),
% 0.10/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.42 fof(f34,negated_conjecture,(
% 0.10/0.42 ( multiply(sk_c2,sk_c10) = sk_c3| inverse(sk_c9) = sk_c8 ) ),
% 0.10/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.42 fof(f35,negated_conjecture,(
% 0.10/0.42 ( multiply(sk_c2,sk_c10) = sk_c3| multiply(sk_c10,sk_c8) = sk_c9 ) ),
% 0.10/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.42 fof(f36,negated_conjecture,(
% 0.10/0.42 ( multiply(sk_c2,sk_c10) = sk_c3| inverse(sk_c5) = sk_c9 ) ),
% 0.10/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.42 fof(f37,negated_conjecture,(
% 0.10/0.42 ( multiply(sk_c2,sk_c10) = sk_c3| multiply(sk_c5,sk_c8) = sk_c9 ) ),
% 0.10/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.42 fof(f38,negated_conjecture,(
% 0.10/0.42 ( multiply(sk_c2,sk_c10) = sk_c3| inverse(sk_c7) = sk_c6 ) ),
% 0.10/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.42 fof(f39,negated_conjecture,(
% 0.10/0.42 ( multiply(sk_c2,sk_c10) = sk_c3| inverse(sk_c6) = sk_c10 ) ),
% 0.10/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.42 fof(f41,negated_conjecture,(
% 0.10/0.42 ( inverse(sk_c2) = sk_c10| multiply(sk_c4,sk_c10) = sk_c9 ) ),
% 0.10/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.42 fof(f42,negated_conjecture,(
% 0.10/0.42 ( inverse(sk_c2) = sk_c10| inverse(sk_c4) = sk_c10 ) ),
% 0.10/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.42 fof(f43,negated_conjecture,(
% 0.10/0.42 ( inverse(sk_c2) = sk_c10| inverse(sk_c9) = sk_c8 ) ),
% 0.10/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.42 fof(f44,negated_conjecture,(
% 0.10/0.42 ( inverse(sk_c2) = sk_c10| multiply(sk_c10,sk_c8) = sk_c9 ) ),
% 0.10/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.42 fof(f45,negated_conjecture,(
% 0.10/0.42 ( inverse(sk_c2) = sk_c10| inverse(sk_c5) = sk_c9 ) ),
% 0.10/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.42 fof(f46,negated_conjecture,(
% 0.10/0.42 ( inverse(sk_c2) = sk_c10| multiply(sk_c5,sk_c8) = sk_c9 ) ),
% 0.10/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.42 fof(f47,negated_conjecture,(
% 0.10/0.42 ( inverse(sk_c2) = sk_c10| inverse(sk_c7) = sk_c6 ) ),
% 0.10/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.42 fof(f48,negated_conjecture,(
% 0.10/0.42 ( inverse(sk_c2) = sk_c10| inverse(sk_c6) = sk_c10 ) ),
% 0.10/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.42 fof(f50,negated_conjecture,(
% 0.10/0.42 (![X4,X5,X6,X1,X2,X3,X7]: (( multiply(sk_c9,sk_c10) != sk_c8| multiply(X4,sk_c9) != sk_c10| inverse(X4) != sk_c9| multiply(sk_c10,X5) != sk_c9| multiply(X6,sk_c10) != X5| inverse(X6) != sk_c10| multiply(X1,sk_c10) != sk_c9| inverse(X1) != sk_c10| inverse(sk_c9) != sk_c8| multiply(sk_c10,sk_c8) != sk_c9| inverse(X2) != sk_c9| multiply(X2,sk_c8) != sk_c9| inverse(X3) != X7| inverse(X7) != sk_c10| multiply(X3,sk_c10) != X7 ) ))),
% 0.10/0.42 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.10/0.42 fof(f51,plain,(
% 0.10/0.42 ![X0]: (multiply(identity,X0)=X0)),
% 0.10/0.42 inference(cnf_transformation,[status(thm)],[f1])).
% 0.10/0.42 fof(f52,plain,(
% 0.10/0.42 ![X0]: (multiply(inverse(X0),X0)=identity)),
% 0.10/0.42 inference(cnf_transformation,[status(thm)],[f2])).
% 0.10/0.42 fof(f53,plain,(
% 0.10/0.42 ![X0,X1,X2]: (multiply(multiply(X0,X1),X2)=multiply(X0,multiply(X1,X2)))),
% 0.10/0.42 inference(cnf_transformation,[status(thm)],[f3])).
% 0.10/0.42 fof(f54,plain,(
% 0.10/0.42 multiply(sk_c9,sk_c10)=sk_c8),
% 0.10/0.42 inference(cnf_transformation,[status(thm)],[f4])).
% 0.10/0.42 fof(f55,plain,(
% 0.10/0.42 multiply(sk_c1,sk_c9)=sk_c10|multiply(sk_c4,sk_c10)=sk_c9),
% 0.10/0.42 inference(cnf_transformation,[status(thm)],[f5])).
% 0.10/0.42 fof(f56,plain,(
% 0.10/0.42 multiply(sk_c1,sk_c9)=sk_c10|inverse(sk_c4)=sk_c10),
% 0.10/0.42 inference(cnf_transformation,[status(thm)],[f6])).
% 0.10/0.42 fof(f57,plain,(
% 0.10/0.42 multiply(sk_c1,sk_c9)=sk_c10|inverse(sk_c9)=sk_c8),
% 0.10/0.42 inference(cnf_transformation,[status(thm)],[f7])).
% 0.10/0.42 fof(f58,plain,(
% 0.10/0.42 multiply(sk_c1,sk_c9)=sk_c10|multiply(sk_c10,sk_c8)=sk_c9),
% 0.10/0.42 inference(cnf_transformation,[status(thm)],[f8])).
% 0.10/0.42 fof(f59,plain,(
% 0.10/0.42 multiply(sk_c1,sk_c9)=sk_c10|inverse(sk_c5)=sk_c9),
% 0.10/0.42 inference(cnf_transformation,[status(thm)],[f9])).
% 0.10/0.42 fof(f60,plain,(
% 0.10/0.42 multiply(sk_c1,sk_c9)=sk_c10|multiply(sk_c5,sk_c8)=sk_c9),
% 0.10/0.42 inference(cnf_transformation,[status(thm)],[f10])).
% 0.10/0.42 fof(f61,plain,(
% 0.10/0.42 multiply(sk_c1,sk_c9)=sk_c10|inverse(sk_c7)=sk_c6),
% 0.10/0.42 inference(cnf_transformation,[status(thm)],[f11])).
% 0.10/0.42 fof(f62,plain,(
% 0.10/0.42 multiply(sk_c1,sk_c9)=sk_c10|inverse(sk_c6)=sk_c10),
% 0.10/0.42 inference(cnf_transformation,[status(thm)],[f12])).
% 0.10/0.42 fof(f64,plain,(
% 0.10/0.42 inverse(sk_c1)=sk_c9|multiply(sk_c4,sk_c10)=sk_c9),
% 0.10/0.42 inference(cnf_transformation,[status(thm)],[f14])).
% 0.10/0.42 fof(f65,plain,(
% 0.10/0.42 inverse(sk_c1)=sk_c9|inverse(sk_c4)=sk_c10),
% 0.10/0.42 inference(cnf_transformation,[status(thm)],[f15])).
% 0.10/0.42 fof(f66,plain,(
% 0.10/0.42 inverse(sk_c1)=sk_c9|inverse(sk_c9)=sk_c8),
% 0.10/0.42 inference(cnf_transformation,[status(thm)],[f16])).
% 0.10/0.42 fof(f67,plain,(
% 0.10/0.42 inverse(sk_c1)=sk_c9|multiply(sk_c10,sk_c8)=sk_c9),
% 0.10/0.42 inference(cnf_transformation,[status(thm)],[f17])).
% 0.10/0.42 fof(f68,plain,(
% 0.10/0.42 inverse(sk_c1)=sk_c9|inverse(sk_c5)=sk_c9),
% 0.10/0.42 inference(cnf_transformation,[status(thm)],[f18])).
% 0.10/0.42 fof(f69,plain,(
% 0.10/0.42 inverse(sk_c1)=sk_c9|multiply(sk_c5,sk_c8)=sk_c9),
% 0.10/0.42 inference(cnf_transformation,[status(thm)],[f19])).
% 0.10/0.42 fof(f70,plain,(
% 0.10/0.42 inverse(sk_c1)=sk_c9|inverse(sk_c7)=sk_c6),
% 0.10/0.42 inference(cnf_transformation,[status(thm)],[f20])).
% 0.10/0.42 fof(f71,plain,(
% 0.10/0.42 inverse(sk_c1)=sk_c9|inverse(sk_c6)=sk_c10),
% 0.10/0.42 inference(cnf_transformation,[status(thm)],[f21])).
% 0.10/0.42 fof(f73,plain,(
% 0.10/0.42 multiply(sk_c10,sk_c3)=sk_c9|multiply(sk_c4,sk_c10)=sk_c9),
% 0.10/0.42 inference(cnf_transformation,[status(thm)],[f23])).
% 0.10/0.42 fof(f74,plain,(
% 0.10/0.42 multiply(sk_c10,sk_c3)=sk_c9|inverse(sk_c4)=sk_c10),
% 0.10/0.42 inference(cnf_transformation,[status(thm)],[f24])).
% 0.10/0.42 fof(f75,plain,(
% 0.10/0.42 multiply(sk_c10,sk_c3)=sk_c9|inverse(sk_c9)=sk_c8),
% 0.10/0.42 inference(cnf_transformation,[status(thm)],[f25])).
% 0.10/0.42 fof(f76,plain,(
% 0.10/0.42 multiply(sk_c10,sk_c3)=sk_c9|multiply(sk_c10,sk_c8)=sk_c9),
% 0.10/0.42 inference(cnf_transformation,[status(thm)],[f26])).
% 0.10/0.42 fof(f77,plain,(
% 0.10/0.42 multiply(sk_c10,sk_c3)=sk_c9|inverse(sk_c5)=sk_c9),
% 0.10/0.42 inference(cnf_transformation,[status(thm)],[f27])).
% 0.10/0.42 fof(f78,plain,(
% 0.10/0.42 multiply(sk_c10,sk_c3)=sk_c9|multiply(sk_c5,sk_c8)=sk_c9),
% 0.10/0.42 inference(cnf_transformation,[status(thm)],[f28])).
% 0.10/0.42 fof(f82,plain,(
% 0.10/0.42 multiply(sk_c2,sk_c10)=sk_c3|multiply(sk_c4,sk_c10)=sk_c9),
% 0.10/0.42 inference(cnf_transformation,[status(thm)],[f32])).
% 0.10/0.42 fof(f83,plain,(
% 0.10/0.42 multiply(sk_c2,sk_c10)=sk_c3|inverse(sk_c4)=sk_c10),
% 0.10/0.42 inference(cnf_transformation,[status(thm)],[f33])).
% 0.10/0.42 fof(f84,plain,(
% 0.10/0.42 multiply(sk_c2,sk_c10)=sk_c3|inverse(sk_c9)=sk_c8),
% 0.10/0.42 inference(cnf_transformation,[status(thm)],[f34])).
% 0.10/0.42 fof(f85,plain,(
% 0.10/0.42 multiply(sk_c2,sk_c10)=sk_c3|multiply(sk_c10,sk_c8)=sk_c9),
% 0.10/0.42 inference(cnf_transformation,[status(thm)],[f35])).
% 0.10/0.42 fof(f86,plain,(
% 0.10/0.42 multiply(sk_c2,sk_c10)=sk_c3|inverse(sk_c5)=sk_c9),
% 0.10/0.42 inference(cnf_transformation,[status(thm)],[f36])).
% 0.10/0.42 fof(f87,plain,(
% 0.10/0.42 multiply(sk_c2,sk_c10)=sk_c3|multiply(sk_c5,sk_c8)=sk_c9),
% 0.10/0.42 inference(cnf_transformation,[status(thm)],[f37])).
% 0.10/0.42 fof(f88,plain,(
% 0.10/0.42 multiply(sk_c2,sk_c10)=sk_c3|inverse(sk_c7)=sk_c6),
% 0.10/0.42 inference(cnf_transformation,[status(thm)],[f38])).
% 0.10/0.42 fof(f89,plain,(
% 0.10/0.42 multiply(sk_c2,sk_c10)=sk_c3|inverse(sk_c6)=sk_c10),
% 0.10/0.42 inference(cnf_transformation,[status(thm)],[f39])).
% 0.10/0.42 fof(f91,plain,(
% 0.10/0.42 inverse(sk_c2)=sk_c10|multiply(sk_c4,sk_c10)=sk_c9),
% 0.10/0.42 inference(cnf_transformation,[status(thm)],[f41])).
% 0.10/0.42 fof(f92,plain,(
% 0.10/0.42 inverse(sk_c2)=sk_c10|inverse(sk_c4)=sk_c10),
% 0.10/0.42 inference(cnf_transformation,[status(thm)],[f42])).
% 0.10/0.42 fof(f93,plain,(
% 0.10/0.42 inverse(sk_c2)=sk_c10|inverse(sk_c9)=sk_c8),
% 0.10/0.42 inference(cnf_transformation,[status(thm)],[f43])).
% 0.10/0.42 fof(f94,plain,(
% 0.10/0.42 inverse(sk_c2)=sk_c10|multiply(sk_c10,sk_c8)=sk_c9),
% 0.10/0.42 inference(cnf_transformation,[status(thm)],[f44])).
% 0.10/0.42 fof(f95,plain,(
% 0.10/0.42 inverse(sk_c2)=sk_c10|inverse(sk_c5)=sk_c9),
% 0.10/0.42 inference(cnf_transformation,[status(thm)],[f45])).
% 0.10/0.42 fof(f96,plain,(
% 0.10/0.42 inverse(sk_c2)=sk_c10|multiply(sk_c5,sk_c8)=sk_c9),
% 0.10/0.42 inference(cnf_transformation,[status(thm)],[f46])).
% 0.10/0.42 fof(f97,plain,(
% 0.10/0.42 inverse(sk_c2)=sk_c10|inverse(sk_c7)=sk_c6),
% 0.10/0.42 inference(cnf_transformation,[status(thm)],[f47])).
% 0.10/0.42 fof(f98,plain,(
% 0.10/0.42 inverse(sk_c2)=sk_c10|inverse(sk_c6)=sk_c10),
% 0.10/0.42 inference(cnf_transformation,[status(thm)],[f48])).
% 0.10/0.42 fof(f100,plain,(
% 0.10/0.42 ![X3,X7]: ((((![X2]: (((((![X1]: (((![X6]: ((![X5]: (((![X4]: ((~multiply(sk_c9,sk_c10)=sk_c8|~multiply(X4,sk_c9)=sk_c10)|~inverse(X4)=sk_c9))|~multiply(sk_c10,X5)=sk_c9)|~multiply(X6,sk_c10)=X5))|~inverse(X6)=sk_c10))|~multiply(X1,sk_c10)=sk_c9)|~inverse(X1)=sk_c10))|~inverse(sk_c9)=sk_c8)|~multiply(sk_c10,sk_c8)=sk_c9)|~inverse(X2)=sk_c9)|~multiply(X2,sk_c8)=sk_c9))|~inverse(X3)=X7)|~inverse(X7)=sk_c10)|~multiply(X3,sk_c10)=X7)),
% 0.10/0.42 inference(miniscoping,[status(thm)],[f50])).
% 0.10/0.42 fof(f101,plain,(
% 0.10/0.42 ![X0,X1,X2,X3,X4,X5,X6]: (~multiply(sk_c9,sk_c10)=sk_c8|~multiply(X0,sk_c9)=sk_c10|~inverse(X0)=sk_c9|~multiply(sk_c10,X1)=sk_c9|~multiply(X2,sk_c10)=X1|~inverse(X2)=sk_c10|~multiply(X3,sk_c10)=sk_c9|~inverse(X3)=sk_c10|~inverse(sk_c9)=sk_c8|~multiply(sk_c10,sk_c8)=sk_c9|~inverse(X4)=sk_c9|~multiply(X4,sk_c8)=sk_c9|~inverse(X5)=X6|~inverse(X6)=sk_c10|~multiply(X5,sk_c10)=X6)),
% 0.10/0.42 inference(cnf_transformation,[status(thm)],[f100])).
% 0.10/0.42 fof(f102,definition,(
% 0.10/0.42 sQ0_spl <=> (multiply(sk_c1,sk_c9)=sk_c10)),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f103,plain,(
% 0.10/0.42 multiply(sk_c1,sk_c9)=sk_c10|~sQ0_spl),
% 0.10/0.42 inference(component_clause,[status(thm)],[f102])).
% 0.10/0.42 fof(f105,definition,(
% 0.10/0.42 sQ1_spl <=> (multiply(sk_c4,sk_c10)=sk_c9)),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f106,plain,(
% 0.10/0.42 multiply(sk_c4,sk_c10)=sk_c9|~sQ1_spl),
% 0.10/0.42 inference(component_clause,[status(thm)],[f105])).
% 0.10/0.42 fof(f108,plain,(
% 0.10/0.42 sQ0_spl|sQ1_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f55,f102,f105])).
% 0.10/0.42 fof(f109,definition,(
% 0.10/0.42 sQ2_spl <=> (inverse(sk_c4)=sk_c10)),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f112,plain,(
% 0.10/0.42 sQ0_spl|sQ2_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f56,f102,f109])).
% 0.10/0.42 fof(f113,definition,(
% 0.10/0.42 sQ3_spl <=> (inverse(sk_c9)=sk_c8)),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f114,plain,(
% 0.10/0.42 inverse(sk_c9)=sk_c8|~sQ3_spl),
% 0.10/0.42 inference(component_clause,[status(thm)],[f113])).
% 0.10/0.42 fof(f115,plain,(
% 0.10/0.42 ~inverse(sk_c9)=sk_c8|sQ3_spl),
% 0.10/0.42 inference(component_clause,[status(thm)],[f113])).
% 0.10/0.42 fof(f116,plain,(
% 0.10/0.42 sQ0_spl|sQ3_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f57,f102,f113])).
% 0.10/0.42 fof(f117,definition,(
% 0.10/0.42 sQ4_spl <=> (multiply(sk_c10,sk_c8)=sk_c9)),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f118,plain,(
% 0.10/0.42 multiply(sk_c10,sk_c8)=sk_c9|~sQ4_spl),
% 0.10/0.42 inference(component_clause,[status(thm)],[f117])).
% 0.10/0.42 fof(f119,plain,(
% 0.10/0.42 ~multiply(sk_c10,sk_c8)=sk_c9|sQ4_spl),
% 0.10/0.42 inference(component_clause,[status(thm)],[f117])).
% 0.10/0.42 fof(f120,plain,(
% 0.10/0.42 sQ0_spl|sQ4_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f58,f102,f117])).
% 0.10/0.42 fof(f121,definition,(
% 0.10/0.42 sQ5_spl <=> (inverse(sk_c5)=sk_c9)),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f122,plain,(
% 0.10/0.42 inverse(sk_c5)=sk_c9|~sQ5_spl),
% 0.10/0.42 inference(component_clause,[status(thm)],[f121])).
% 0.10/0.42 fof(f124,plain,(
% 0.10/0.42 sQ0_spl|sQ5_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f59,f102,f121])).
% 0.10/0.42 fof(f125,definition,(
% 0.10/0.42 sQ6_spl <=> (multiply(sk_c5,sk_c8)=sk_c9)),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f126,plain,(
% 0.10/0.42 multiply(sk_c5,sk_c8)=sk_c9|~sQ6_spl),
% 0.10/0.42 inference(component_clause,[status(thm)],[f125])).
% 0.10/0.42 fof(f128,plain,(
% 0.10/0.42 sQ0_spl|sQ6_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f60,f102,f125])).
% 0.10/0.42 fof(f129,definition,(
% 0.10/0.42 sQ7_spl <=> (inverse(sk_c7)=sk_c6)),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f130,plain,(
% 0.10/0.42 inverse(sk_c7)=sk_c6|~sQ7_spl),
% 0.10/0.42 inference(component_clause,[status(thm)],[f129])).
% 0.10/0.42 fof(f132,plain,(
% 0.10/0.42 sQ0_spl|sQ7_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f61,f102,f129])).
% 0.10/0.42 fof(f133,definition,(
% 0.10/0.42 sQ8_spl <=> (inverse(sk_c6)=sk_c10)),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f134,plain,(
% 0.10/0.42 inverse(sk_c6)=sk_c10|~sQ8_spl),
% 0.10/0.42 inference(component_clause,[status(thm)],[f133])).
% 0.10/0.42 fof(f136,plain,(
% 0.10/0.42 sQ0_spl|sQ8_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f62,f102,f133])).
% 0.10/0.42 fof(f141,definition,(
% 0.10/0.42 sQ10_spl <=> (inverse(sk_c1)=sk_c9)),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f142,plain,(
% 0.10/0.42 inverse(sk_c1)=sk_c9|~sQ10_spl),
% 0.10/0.42 inference(component_clause,[status(thm)],[f141])).
% 0.10/0.42 fof(f144,plain,(
% 0.10/0.42 sQ10_spl|sQ1_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f64,f141,f105])).
% 0.10/0.42 fof(f145,plain,(
% 0.10/0.42 sQ10_spl|sQ2_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f65,f141,f109])).
% 0.10/0.42 fof(f146,plain,(
% 0.10/0.42 sQ10_spl|sQ3_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f66,f141,f113])).
% 0.10/0.42 fof(f147,plain,(
% 0.10/0.42 sQ10_spl|sQ4_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f67,f141,f117])).
% 0.10/0.42 fof(f148,plain,(
% 0.10/0.42 sQ10_spl|sQ5_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f68,f141,f121])).
% 0.10/0.42 fof(f149,plain,(
% 0.10/0.42 sQ10_spl|sQ6_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f69,f141,f125])).
% 0.10/0.42 fof(f150,plain,(
% 0.10/0.42 sQ10_spl|sQ7_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f70,f141,f129])).
% 0.10/0.42 fof(f151,plain,(
% 0.10/0.42 sQ10_spl|sQ8_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f71,f141,f133])).
% 0.10/0.42 fof(f153,definition,(
% 0.10/0.42 sQ11_spl <=> (multiply(sk_c10,sk_c3)=sk_c9)),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f154,plain,(
% 0.10/0.42 multiply(sk_c10,sk_c3)=sk_c9|~sQ11_spl),
% 0.10/0.42 inference(component_clause,[status(thm)],[f153])).
% 0.10/0.42 fof(f155,plain,(
% 0.10/0.42 ~multiply(sk_c10,sk_c3)=sk_c9|sQ11_spl),
% 0.10/0.42 inference(component_clause,[status(thm)],[f153])).
% 0.10/0.42 fof(f156,plain,(
% 0.10/0.42 sQ11_spl|sQ1_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f73,f153,f105])).
% 0.10/0.42 fof(f157,plain,(
% 0.10/0.42 sQ11_spl|sQ2_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f74,f153,f109])).
% 0.10/0.42 fof(f158,plain,(
% 0.10/0.42 sQ11_spl|sQ3_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f75,f153,f113])).
% 0.10/0.42 fof(f159,plain,(
% 0.10/0.42 sQ11_spl|sQ4_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f76,f153,f117])).
% 0.10/0.42 fof(f160,plain,(
% 0.10/0.42 sQ11_spl|sQ5_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f77,f153,f121])).
% 0.10/0.42 fof(f161,plain,(
% 0.10/0.42 sQ11_spl|sQ6_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f78,f153,f125])).
% 0.10/0.42 fof(f165,definition,(
% 0.10/0.42 sQ12_spl <=> (multiply(sk_c2,sk_c10)=sk_c3)),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f166,plain,(
% 0.10/0.42 multiply(sk_c2,sk_c10)=sk_c3|~sQ12_spl),
% 0.10/0.42 inference(component_clause,[status(thm)],[f165])).
% 0.10/0.42 fof(f168,plain,(
% 0.10/0.42 sQ12_spl|sQ1_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f82,f165,f105])).
% 0.10/0.42 fof(f169,plain,(
% 0.10/0.42 sQ12_spl|sQ2_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f83,f165,f109])).
% 0.10/0.42 fof(f170,plain,(
% 0.10/0.42 sQ12_spl|sQ3_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f84,f165,f113])).
% 0.10/0.42 fof(f171,plain,(
% 0.10/0.42 sQ12_spl|sQ4_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f85,f165,f117])).
% 0.10/0.42 fof(f172,plain,(
% 0.10/0.42 sQ12_spl|sQ5_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f86,f165,f121])).
% 0.10/0.42 fof(f173,plain,(
% 0.10/0.42 sQ12_spl|sQ6_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f87,f165,f125])).
% 0.10/0.42 fof(f174,plain,(
% 0.10/0.42 sQ12_spl|sQ7_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f88,f165,f129])).
% 0.10/0.42 fof(f175,plain,(
% 0.10/0.42 sQ12_spl|sQ8_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f89,f165,f133])).
% 0.10/0.42 fof(f177,definition,(
% 0.10/0.42 sQ13_spl <=> (inverse(sk_c2)=sk_c10)),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f178,plain,(
% 0.10/0.42 inverse(sk_c2)=sk_c10|~sQ13_spl),
% 0.10/0.42 inference(component_clause,[status(thm)],[f177])).
% 0.10/0.42 fof(f180,plain,(
% 0.10/0.42 sQ13_spl|sQ1_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f91,f177,f105])).
% 0.10/0.42 fof(f181,plain,(
% 0.10/0.42 sQ13_spl|sQ2_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f92,f177,f109])).
% 0.10/0.42 fof(f182,plain,(
% 0.10/0.42 sQ13_spl|sQ3_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f93,f177,f113])).
% 0.10/0.42 fof(f183,plain,(
% 0.10/0.42 sQ13_spl|sQ4_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f94,f177,f117])).
% 0.10/0.42 fof(f184,plain,(
% 0.10/0.42 sQ13_spl|sQ5_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f95,f177,f121])).
% 0.10/0.42 fof(f185,plain,(
% 0.10/0.42 sQ13_spl|sQ6_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f96,f177,f125])).
% 0.10/0.42 fof(f186,plain,(
% 0.10/0.42 sQ13_spl|sQ7_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f97,f177,f129])).
% 0.10/0.42 fof(f187,plain,(
% 0.10/0.42 sQ13_spl|sQ8_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f98,f177,f133])).
% 0.10/0.42 fof(f189,definition,(
% 0.10/0.42 sQ14_spl <=> (multiply(sk_c9,sk_c10)=sk_c8)),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f191,plain,(
% 0.10/0.42 ~multiply(sk_c9,sk_c10)=sk_c8|sQ14_spl),
% 0.10/0.42 inference(component_clause,[status(thm)],[f189])).
% 0.10/0.42 fof(f192,definition,(
% 0.10/0.42 ![X0]: (sQ15_spl <=> (~multiply(X0,sk_c9)=sk_c10|~inverse(X0)=sk_c9))),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f193,plain,(
% 0.10/0.42 ![X0]: (~multiply(X0,sk_c9)=sk_c10|~inverse(X0)=sk_c9|~sQ15_spl)),
% 0.10/0.42 inference(component_clause,[status(thm)],[f192])).
% 0.10/0.42 fof(f195,definition,(
% 0.10/0.42 ![X1,X2]: (sQ16_spl <=> (~multiply(sk_c10,X1)=sk_c9|~multiply(X2,sk_c10)=X1|~inverse(X2)=sk_c10))),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f196,plain,(
% 0.10/0.42 ![X0,X1]: (~multiply(sk_c10,X0)=sk_c9|~multiply(X1,sk_c10)=X0|~inverse(X1)=sk_c10|~sQ16_spl)),
% 0.10/0.42 inference(component_clause,[status(thm)],[f195])).
% 0.10/0.42 fof(f198,definition,(
% 0.10/0.42 ![X3]: (sQ17_spl <=> (~multiply(X3,sk_c10)=sk_c9|~inverse(X3)=sk_c10))),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f199,plain,(
% 0.10/0.42 ![X0]: (~multiply(X0,sk_c10)=sk_c9|~inverse(X0)=sk_c10|~sQ17_spl)),
% 0.10/0.42 inference(component_clause,[status(thm)],[f198])).
% 0.10/0.42 fof(f201,definition,(
% 0.10/0.42 ![X4]: (sQ18_spl <=> (~inverse(X4)=sk_c9|~multiply(X4,sk_c8)=sk_c9))),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f202,plain,(
% 0.10/0.42 ![X0]: (~inverse(X0)=sk_c9|~multiply(X0,sk_c8)=sk_c9|~sQ18_spl)),
% 0.10/0.42 inference(component_clause,[status(thm)],[f201])).
% 0.10/0.42 fof(f204,definition,(
% 0.10/0.42 ![X5,X6]: (sQ19_spl <=> (~inverse(X5)=X6|~inverse(X6)=sk_c10|~multiply(X5,sk_c10)=X6))),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f205,plain,(
% 0.10/0.42 ![X0,X1]: (~inverse(X0)=X1|~inverse(X1)=sk_c10|~multiply(X0,sk_c10)=X1|~sQ19_spl)),
% 0.10/0.42 inference(component_clause,[status(thm)],[f204])).
% 0.10/0.42 fof(f207,plain,(
% 0.10/0.42 ~sQ14_spl|sQ15_spl|sQ16_spl|sQ17_spl|~sQ3_spl|~sQ4_spl|sQ18_spl|sQ19_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f101,f189,f192,f195,f198,f113,f117,f201,f204])).
% 0.10/0.42 fof(f209,plain,(
% 0.10/0.42 ![X0]: (multiply(sk_c8,X0)=multiply(sk_c9,multiply(sk_c10,X0)))),
% 0.10/0.42 inference(paramodulation,[status(thm)],[f54,f53])).
% 0.10/0.42 fof(f212,plain,(
% 0.10/0.42 ![X0]: (multiply(sk_c3,X0)=multiply(sk_c2,multiply(sk_c10,X0))|~sQ12_spl)),
% 0.10/0.42 inference(paramodulation,[status(thm)],[f166,f53])).
% 0.10/0.42 fof(f215,plain,(
% 0.10/0.42 multiply(sk_c6,sk_c7)=identity|~sQ7_spl),
% 0.10/0.42 inference(paramodulation,[status(thm)],[f130,f52])).
% 0.10/0.42 fof(f217,plain,(
% 0.10/0.42 multiply(sk_c9,sk_c1)=identity|~sQ10_spl),
% 0.10/0.42 inference(paramodulation,[status(thm)],[f142,f52])).
% 0.10/0.42 fof(f218,plain,(
% 0.10/0.42 multiply(sk_c10,sk_c2)=identity|~sQ13_spl),
% 0.10/0.42 inference(paramodulation,[status(thm)],[f178,f52])).
% 0.10/0.42 fof(f219,plain,(
% 0.10/0.42 ![X0,X1]: (multiply(identity,X0)=multiply(inverse(X1),multiply(X1,X0)))),
% 0.10/0.42 inference(paramodulation,[status(thm)],[f52,f53])).
% 0.10/0.42 fof(f220,plain,(
% 0.10/0.42 ![X0,X1]: (X0=multiply(inverse(X1),multiply(X1,X0)))),
% 0.10/0.42 inference(forward_demodulation,[status(thm)],[f51,f219])).
% 0.10/0.42 fof(f234,plain,(
% 0.10/0.42 ![X0]: (~inverse(X0)=sk_c1|~sk_c9=sk_c10|~multiply(X0,sk_c10)=sk_c1|~sQ19_spl|~sQ10_spl)),
% 0.10/0.42 inference(paramodulation,[status(thm)],[f142,f205])).
% 0.10/0.42 fof(f235,plain,(
% 0.10/0.42 ![X0]: (~inverse(X0)=sk_c2|~sk_c10=sk_c10|~multiply(X0,sk_c10)=sk_c2|~sQ19_spl|~sQ13_spl)),
% 0.10/0.42 inference(paramodulation,[status(thm)],[f178,f205])).
% 0.10/0.42 fof(f239,definition,(
% 0.10/0.42 sQ21_spl <=> (sk_c10=sk_c10)),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f241,plain,(
% 0.10/0.42 ~sk_c10=sk_c10|sQ21_spl),
% 0.10/0.42 inference(component_clause,[status(thm)],[f239])).
% 0.10/0.42 fof(f246,definition,(
% 0.10/0.42 sQ23_spl <=> (sk_c9=sk_c10)),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ23_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f248,plain,(
% 0.10/0.42 ~sk_c9=sk_c10|sQ23_spl),
% 0.10/0.42 inference(component_clause,[status(thm)],[f246])).
% 0.10/0.42 fof(f261,definition,(
% 0.10/0.42 ![X0]: (sQ27_spl <=> (~inverse(X0)=sk_c1|~multiply(X0,sk_c10)=sk_c1))),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ27_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f262,plain,(
% 0.10/0.42 ![X0]: (~inverse(X0)=sk_c1|~multiply(X0,sk_c10)=sk_c1|~sQ27_spl)),
% 0.10/0.42 inference(component_clause,[status(thm)],[f261])).
% 0.10/0.42 fof(f264,plain,(
% 0.10/0.42 sQ27_spl|~sQ23_spl|~sQ19_spl|~sQ10_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f234,f261,f246,f204,f141])).
% 0.10/0.42 fof(f265,definition,(
% 0.10/0.42 ![X0]: (sQ28_spl <=> (~inverse(X0)=sk_c2|~multiply(X0,sk_c10)=sk_c2))),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ28_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f266,plain,(
% 0.10/0.42 ![X0]: (~inverse(X0)=sk_c2|~multiply(X0,sk_c10)=sk_c2|~sQ28_spl)),
% 0.10/0.42 inference(component_clause,[status(thm)],[f265])).
% 0.10/0.42 fof(f268,plain,(
% 0.10/0.42 sQ28_spl|~sQ21_spl|~sQ19_spl|~sQ13_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f235,f265,f239,f204,f177])).
% 0.10/0.42 fof(f269,plain,(
% 0.10/0.42 $false|sQ21_spl),
% 0.10/0.42 inference(trivial_equality_resolution,[status(thm)],[f241])).
% 0.10/0.42 fof(f270,plain,(
% 0.10/0.42 sQ21_spl),
% 0.10/0.42 inference(contradiction_clause,[status(thm)],[f269])).
% 0.10/0.42 fof(f272,plain,(
% 0.10/0.42 ~inverse(sk_c5)=sk_c9|~sk_c9=sk_c9|~sQ18_spl|~sQ6_spl),
% 0.10/0.42 inference(paramodulation,[status(thm)],[f126,f202])).
% 0.10/0.42 fof(f276,definition,(
% 0.10/0.42 sQ29_spl <=> (sk_c9=sk_c9)),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f278,plain,(
% 0.10/0.42 ~sk_c9=sk_c9|sQ29_spl),
% 0.10/0.42 inference(component_clause,[status(thm)],[f276])).
% 0.10/0.42 fof(f279,plain,(
% 0.10/0.42 ~sQ5_spl|~sQ29_spl|~sQ18_spl|~sQ6_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f272,f121,f276,f201,f125])).
% 0.10/0.42 fof(f287,definition,(
% 0.10/0.42 sQ32_spl <=> (inverse(identity)=sk_c9)),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f294,plain,(
% 0.10/0.42 $false|sQ29_spl),
% 0.10/0.42 inference(trivial_equality_resolution,[status(thm)],[f278])).
% 0.10/0.42 fof(f295,plain,(
% 0.10/0.42 sQ29_spl),
% 0.10/0.42 inference(contradiction_clause,[status(thm)],[f294])).
% 0.10/0.42 fof(f296,plain,(
% 0.10/0.42 ~sk_c8=sk_c8|sQ14_spl),
% 0.10/0.42 inference(forward_demodulation,[status(thm)],[f54,f191])).
% 0.10/0.42 fof(f297,plain,(
% 0.10/0.42 $false|sQ14_spl),
% 0.10/0.42 inference(trivial_equality_resolution,[status(thm)],[f296])).
% 0.10/0.42 fof(f298,plain,(
% 0.10/0.42 sQ14_spl),
% 0.10/0.42 inference(contradiction_clause,[status(thm)],[f297])).
% 0.10/0.42 fof(f300,plain,(
% 0.10/0.42 ~sk_c9=sk_c9|~inverse(sk_c4)=sk_c10|~sQ17_spl|~sQ1_spl),
% 0.10/0.42 inference(paramodulation,[status(thm)],[f106,f199])).
% 0.10/0.42 fof(f304,plain,(
% 0.10/0.42 ~sk_c3=sk_c9|~inverse(sk_c2)=sk_c10|~sQ17_spl|~sQ12_spl),
% 0.10/0.42 inference(paramodulation,[status(thm)],[f166,f199])).
% 0.10/0.42 fof(f307,plain,(
% 0.10/0.42 ~sQ29_spl|~sQ2_spl|~sQ17_spl|~sQ1_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f300,f276,f109,f198,f105])).
% 0.10/0.42 fof(f323,definition,(
% 0.10/0.42 sQ38_spl <=> (sk_c3=sk_c9)),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f325,plain,(
% 0.10/0.42 ~sk_c3=sk_c9|sQ38_spl),
% 0.10/0.42 inference(component_clause,[status(thm)],[f323])).
% 0.10/0.42 fof(f326,plain,(
% 0.10/0.42 ~sQ38_spl|~sQ13_spl|~sQ17_spl|~sQ12_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f304,f323,f177,f198,f165])).
% 0.10/0.42 fof(f332,plain,(
% 0.10/0.42 ![X0]: (~sk_c9=sk_c9|~multiply(X0,sk_c10)=sk_c3|~inverse(X0)=sk_c10|~sQ16_spl|~sQ11_spl)),
% 0.10/0.42 inference(paramodulation,[status(thm)],[f154,f196])).
% 0.10/0.42 fof(f333,definition,(
% 0.10/0.42 ![X0]: (sQ40_spl <=> (~multiply(X0,sk_c10)=sk_c3|~inverse(X0)=sk_c10))),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ40_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f334,plain,(
% 0.10/0.42 ![X0]: (~multiply(X0,sk_c10)=sk_c3|~inverse(X0)=sk_c10|~sQ40_spl)),
% 0.10/0.42 inference(component_clause,[status(thm)],[f333])).
% 0.10/0.42 fof(f336,plain,(
% 0.10/0.42 ~sQ29_spl|sQ40_spl|~sQ16_spl|~sQ11_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f332,f276,f333,f195,f153])).
% 0.10/0.42 fof(f337,plain,(
% 0.10/0.42 ~inverse(sk_c1)=sk_c9|~sQ15_spl|~sQ0_spl),
% 0.10/0.42 inference(resolution,[status(thm)],[f193,f103])).
% 0.10/0.42 fof(f339,plain,(
% 0.10/0.42 ~identity=sk_c10|~inverse(inverse(sk_c9))=sk_c9|~sQ15_spl),
% 0.10/0.42 inference(paramodulation,[status(thm)],[f52,f193])).
% 0.10/0.42 fof(f340,plain,(
% 0.10/0.42 ~sk_c9=sk_c10|~inverse(identity)=sk_c9|~sQ15_spl),
% 0.10/0.42 inference(paramodulation,[status(thm)],[f51,f193])).
% 0.10/0.42 fof(f341,plain,(
% 0.10/0.42 ![X0,X1]: (~multiply(X0,multiply(X1,sk_c9))=sk_c10|~inverse(multiply(X0,X1))=sk_c9|~sQ15_spl)),
% 0.10/0.42 inference(paramodulation,[status(thm)],[f53,f193])).
% 0.10/0.42 fof(f342,plain,(
% 0.10/0.42 ~sk_c9=sk_c9|~sQ10_spl|~sQ15_spl|~sQ0_spl),
% 0.10/0.42 inference(forward_demodulation,[status(thm)],[f142,f337])).
% 0.10/0.42 fof(f343,plain,(
% 0.10/0.42 $false|~sQ10_spl|~sQ15_spl|~sQ0_spl),
% 0.10/0.42 inference(trivial_equality_resolution,[status(thm)],[f342])).
% 0.10/0.42 fof(f344,plain,(
% 0.10/0.42 ~sQ10_spl|~sQ15_spl|~sQ0_spl),
% 0.10/0.42 inference(contradiction_clause,[status(thm)],[f343])).
% 0.10/0.42 fof(f345,definition,(
% 0.10/0.42 sQ41_spl <=> (identity=sk_c10)),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f347,plain,(
% 0.10/0.42 ~identity=sk_c10|sQ41_spl),
% 0.10/0.42 inference(component_clause,[status(thm)],[f345])).
% 0.10/0.42 fof(f348,definition,(
% 0.10/0.42 sQ42_spl <=> (inverse(inverse(sk_c9))=sk_c9)),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f350,plain,(
% 0.10/0.42 ~inverse(inverse(sk_c9))=sk_c9|sQ42_spl),
% 0.10/0.42 inference(component_clause,[status(thm)],[f348])).
% 0.10/0.42 fof(f351,plain,(
% 0.10/0.42 ~sQ41_spl|~sQ42_spl|~sQ15_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f339,f345,f348,f192])).
% 0.10/0.42 fof(f352,plain,(
% 0.10/0.42 ~sQ23_spl|~sQ32_spl|~sQ15_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f340,f246,f287,f192])).
% 0.10/0.42 fof(f354,plain,(
% 0.10/0.42 multiply(sk_c8,sk_c9)=identity|~sQ3_spl),
% 0.10/0.42 inference(paramodulation,[status(thm)],[f114,f52])).
% 0.10/0.42 fof(f360,plain,(
% 0.10/0.42 multiply(sk_c8,sk_c8)=multiply(sk_c9,sk_c9)|~sQ4_spl),
% 0.10/0.42 inference(paramodulation,[status(thm)],[f118,f209])).
% 0.10/0.42 fof(f373,plain,(
% 0.10/0.42 multiply(sk_c8,sk_c2)=multiply(sk_c9,identity)|~sQ13_spl),
% 0.10/0.42 inference(paramodulation,[status(thm)],[f218,f209])).
% 0.10/0.42 fof(f389,plain,(
% 0.10/0.42 sk_c7=multiply(inverse(sk_c6),identity)|~sQ7_spl),
% 0.10/0.42 inference(paramodulation,[status(thm)],[f215,f220])).
% 0.10/0.42 fof(f390,plain,(
% 0.10/0.42 sk_c8=multiply(inverse(sk_c5),sk_c9)|~sQ6_spl),
% 0.10/0.42 inference(paramodulation,[status(thm)],[f126,f220])).
% 0.10/0.42 fof(f394,plain,(
% 0.10/0.42 sk_c2=multiply(inverse(sk_c10),identity)|~sQ13_spl),
% 0.10/0.42 inference(paramodulation,[status(thm)],[f218,f220])).
% 0.10/0.42 fof(f397,plain,(
% 0.10/0.42 ![X0,X1]: (multiply(X0,X1)=multiply(inverse(inverse(X0)),X1))),
% 0.10/0.42 inference(paramodulation,[status(thm)],[f220,f220])).
% 0.10/0.42 fof(f398,plain,(
% 0.10/0.42 ![X0]: (X0=multiply(inverse(inverse(X0)),identity))),
% 0.10/0.42 inference(paramodulation,[status(thm)],[f52,f220])).
% 0.10/0.42 fof(f399,plain,(
% 0.10/0.42 ![X0]: (X0=multiply(inverse(identity),X0))),
% 0.10/0.42 inference(paramodulation,[status(thm)],[f51,f220])).
% 0.10/0.42 fof(f401,plain,(
% 0.10/0.42 sk_c10=multiply(inverse(sk_c2),sk_c3)|~sQ12_spl),
% 0.10/0.42 inference(paramodulation,[status(thm)],[f166,f220])).
% 0.10/0.42 fof(f407,plain,(
% 0.10/0.42 sk_c7=multiply(sk_c10,identity)|~sQ8_spl|~sQ7_spl),
% 0.10/0.42 inference(forward_demodulation,[status(thm)],[f134,f389])).
% 0.10/0.42 fof(f408,plain,(
% 0.10/0.42 sk_c8=multiply(sk_c9,sk_c9)|~sQ5_spl|~sQ6_spl),
% 0.10/0.42 inference(forward_demodulation,[status(thm)],[f122,f390])).
% 0.10/0.42 fof(f412,plain,(
% 0.10/0.42 sk_c10=multiply(sk_c10,sk_c3)|~sQ13_spl|~sQ12_spl),
% 0.10/0.42 inference(forward_demodulation,[status(thm)],[f178,f401])).
% 0.10/0.42 fof(f413,plain,(
% 0.10/0.42 sk_c10=sk_c9|~sQ11_spl|~sQ13_spl|~sQ12_spl),
% 0.10/0.42 inference(forward_demodulation,[status(thm)],[f154,f412])).
% 0.10/0.42 fof(f414,plain,(
% 0.10/0.42 $false|sQ23_spl|~sQ11_spl|~sQ13_spl|~sQ12_spl),
% 0.10/0.42 inference(forward_subsumption_resolution,[status(thm)],[f413,f248])).
% 0.10/0.42 fof(f415,plain,(
% 0.10/0.42 sQ23_spl|~sQ11_spl|~sQ13_spl|~sQ12_spl),
% 0.10/0.42 inference(contradiction_clause,[status(thm)],[f414])).
% 0.10/0.42 fof(f463,plain,(
% 0.10/0.42 ![X0]: (~sk_c9=sk_c10|~inverse(multiply(inverse(X0),X0))=sk_c9|~sQ15_spl)),
% 0.10/0.42 inference(paramodulation,[status(thm)],[f220,f341])).
% 0.10/0.42 fof(f466,plain,(
% 0.10/0.42 ~multiply(sk_c3,sk_c9)=sk_c10|~inverse(multiply(sk_c2,sk_c10))=sk_c9|~sQ15_spl|~sQ12_spl),
% 0.10/0.42 inference(paramodulation,[status(thm)],[f212,f341])).
% 0.10/0.42 fof(f491,definition,(
% 0.10/0.42 ![X0]: (sQ49_spl <=> (~inverse(multiply(inverse(X0),X0))=sk_c9))),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f494,plain,(
% 0.10/0.42 ~sQ23_spl|sQ49_spl|~sQ15_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f463,f246,f491,f192])).
% 0.10/0.42 fof(f500,definition,(
% 0.10/0.42 sQ51_spl <=> (multiply(sk_c3,sk_c9)=sk_c10)),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f502,plain,(
% 0.10/0.42 ~multiply(sk_c3,sk_c9)=sk_c10|sQ51_spl),
% 0.10/0.42 inference(component_clause,[status(thm)],[f500])).
% 0.10/0.42 fof(f503,definition,(
% 0.10/0.42 sQ52_spl <=> (inverse(multiply(sk_c2,sk_c10))=sk_c9)),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f506,plain,(
% 0.10/0.42 ~sQ51_spl|~sQ52_spl|~sQ15_spl|~sQ12_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f466,f500,f503,f192,f165])).
% 0.10/0.42 fof(f550,plain,(
% 0.10/0.42 multiply(sk_c8,sk_c8)=sk_c8|~sQ5_spl|~sQ6_spl|~sQ4_spl),
% 0.10/0.42 inference(forward_demodulation,[status(thm)],[f408,f360])).
% 0.10/0.42 fof(f553,plain,(
% 0.10/0.42 sk_c8=multiply(inverse(sk_c8),sk_c8)|~sQ5_spl|~sQ6_spl|~sQ4_spl),
% 0.10/0.42 inference(paramodulation,[status(thm)],[f550,f220])).
% 0.10/0.42 fof(f557,plain,(
% 0.10/0.42 sk_c8=identity|~sQ5_spl|~sQ6_spl|~sQ4_spl),
% 0.10/0.42 inference(forward_demodulation,[status(thm)],[f52,f553])).
% 0.10/0.42 fof(f565,definition,(
% 0.10/0.42 sQ59_spl <=> (inverse(sk_c2)=sk_c9)),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f567,plain,(
% 0.10/0.42 ~inverse(sk_c2)=sk_c9|sQ59_spl),
% 0.10/0.42 inference(component_clause,[status(thm)],[f565])).
% 0.10/0.42 fof(f582,plain,(
% 0.10/0.42 multiply(identity,sk_c2)=multiply(sk_c9,identity)|~sQ5_spl|~sQ6_spl|~sQ4_spl|~sQ13_spl),
% 0.10/0.42 inference(backward_demodulation,[status(thm)],[f557,f373])).
% 0.10/0.42 fof(f589,plain,(
% 0.10/0.42 multiply(identity,sk_c9)=identity|~sQ5_spl|~sQ6_spl|~sQ4_spl|~sQ3_spl),
% 0.10/0.42 inference(backward_demodulation,[status(thm)],[f557,f354])).
% 0.10/0.42 fof(f591,plain,(
% 0.10/0.42 multiply(sk_c10,identity)=sk_c9|~sQ5_spl|~sQ6_spl|~sQ4_spl),
% 0.10/0.42 inference(backward_demodulation,[status(thm)],[f557,f118])).
% 0.10/0.42 fof(f592,plain,(
% 0.10/0.42 inverse(sk_c9)=identity|~sQ5_spl|~sQ6_spl|~sQ4_spl|~sQ3_spl),
% 0.10/0.42 inference(backward_demodulation,[status(thm)],[f557,f114])).
% 0.10/0.42 fof(f594,plain,(
% 0.10/0.42 multiply(sk_c9,sk_c10)=identity|~sQ5_spl|~sQ6_spl|~sQ4_spl),
% 0.10/0.42 inference(backward_demodulation,[status(thm)],[f557,f54])).
% 0.10/0.42 fof(f595,plain,(
% 0.10/0.42 sk_c2=multiply(sk_c9,identity)|~sQ5_spl|~sQ6_spl|~sQ4_spl|~sQ13_spl),
% 0.10/0.42 inference(forward_demodulation,[status(thm)],[f51,f582])).
% 0.10/0.42 fof(f600,plain,(
% 0.10/0.42 sk_c9=identity|~sQ5_spl|~sQ6_spl|~sQ4_spl|~sQ3_spl),
% 0.10/0.42 inference(forward_demodulation,[status(thm)],[f51,f589])).
% 0.10/0.42 fof(f605,plain,(
% 0.10/0.42 ~multiply(sk_c10,sk_c3)=identity|~sQ5_spl|~sQ6_spl|~sQ4_spl|~sQ3_spl|sQ11_spl),
% 0.10/0.42 inference(backward_demodulation,[status(thm)],[f600,f155])).
% 0.10/0.42 fof(f615,plain,(
% 0.10/0.42 sk_c7=identity|~sQ3_spl|~sQ5_spl|~sQ6_spl|~sQ4_spl|~sQ8_spl|~sQ7_spl),
% 0.10/0.42 inference(backward_demodulation,[status(thm)],[f616,f407])).
% 0.10/0.42 fof(f616,plain,(
% 0.10/0.42 multiply(sk_c10,identity)=identity|~sQ3_spl|~sQ5_spl|~sQ6_spl|~sQ4_spl),
% 0.10/0.42 inference(forward_demodulation,[status(thm)],[f600,f591])).
% 0.10/0.42 fof(f623,plain,(
% 0.10/0.42 inverse(identity)=identity|~sQ5_spl|~sQ6_spl|~sQ4_spl|~sQ3_spl),
% 0.10/0.42 inference(forward_demodulation,[status(thm)],[f600,f592])).
% 0.10/0.42 fof(f629,plain,(
% 0.10/0.42 inverse(identity)=sk_c6|~sQ3_spl|~sQ5_spl|~sQ6_spl|~sQ4_spl|~sQ8_spl|~sQ7_spl),
% 0.10/0.42 inference(backward_demodulation,[status(thm)],[f615,f130])).
% 0.10/0.42 fof(f632,plain,(
% 0.10/0.42 identity=sk_c6|~sQ3_spl|~sQ5_spl|~sQ6_spl|~sQ4_spl|~sQ8_spl|~sQ7_spl),
% 0.10/0.42 inference(forward_demodulation,[status(thm)],[f623,f629])).
% 0.10/0.42 fof(f635,plain,(
% 0.10/0.42 inverse(identity)=sk_c10|~sQ3_spl|~sQ5_spl|~sQ6_spl|~sQ4_spl|~sQ7_spl|~sQ8_spl),
% 0.10/0.42 inference(backward_demodulation,[status(thm)],[f632,f134])).
% 0.10/0.42 fof(f636,plain,(
% 0.10/0.42 identity=sk_c10|~sQ3_spl|~sQ5_spl|~sQ6_spl|~sQ4_spl|~sQ7_spl|~sQ8_spl),
% 0.10/0.42 inference(forward_demodulation,[status(thm)],[f623,f635])).
% 0.10/0.42 fof(f637,plain,(
% 0.10/0.42 $false|sQ41_spl|~sQ3_spl|~sQ5_spl|~sQ6_spl|~sQ4_spl|~sQ7_spl|~sQ8_spl),
% 0.10/0.42 inference(forward_subsumption_resolution,[status(thm)],[f636,f347])).
% 0.10/0.42 fof(f638,plain,(
% 0.10/0.42 sQ41_spl|~sQ3_spl|~sQ5_spl|~sQ6_spl|~sQ4_spl|~sQ7_spl|~sQ8_spl),
% 0.10/0.42 inference(contradiction_clause,[status(thm)],[f637])).
% 0.10/0.42 fof(f639,plain,(
% 0.10/0.42 ![X0,X1]: (~multiply(sk_c10,X0)=identity|~multiply(X1,sk_c10)=X0|~inverse(X1)=sk_c10|~sQ5_spl|~sQ6_spl|~sQ4_spl|~sQ3_spl|~sQ16_spl)),
% 0.10/0.42 inference(forward_demodulation,[status(thm)],[f600,f196])).
% 0.10/0.42 fof(f642,plain,(
% 0.10/0.42 multiply(identity,sk_c10)=identity|~sQ3_spl|~sQ5_spl|~sQ6_spl|~sQ4_spl),
% 0.10/0.42 inference(forward_demodulation,[status(thm)],[f600,f594])).
% 0.10/0.42 fof(f645,plain,(
% 0.10/0.42 multiply(identity,sk_c2)=identity|~sQ3_spl|~sQ5_spl|~sQ6_spl|~sQ4_spl|~sQ13_spl),
% 0.10/0.42 inference(backward_demodulation,[status(thm)],[f650,f218])).
% 0.10/0.42 fof(f648,plain,(
% 0.10/0.42 multiply(sk_c2,identity)=sk_c3|~sQ3_spl|~sQ5_spl|~sQ6_spl|~sQ4_spl|~sQ12_spl),
% 0.10/0.42 inference(backward_demodulation,[status(thm)],[f650,f166])).
% 0.10/0.42 fof(f650,plain,(
% 0.10/0.42 sk_c10=identity|~sQ3_spl|~sQ5_spl|~sQ6_spl|~sQ4_spl),
% 0.10/0.42 inference(forward_demodulation,[status(thm)],[f51,f642])).
% 0.10/0.42 fof(f652,plain,(
% 0.10/0.42 sk_c2=identity|~sQ3_spl|~sQ5_spl|~sQ6_spl|~sQ4_spl|~sQ13_spl),
% 0.10/0.42 inference(forward_demodulation,[status(thm)],[f51,f645])).
% 0.10/0.42 fof(f654,plain,(
% 0.10/0.42 ~multiply(identity,sk_c3)=identity|~sQ5_spl|~sQ6_spl|~sQ4_spl|~sQ3_spl|sQ11_spl),
% 0.10/0.42 inference(forward_demodulation,[status(thm)],[f650,f605])).
% 0.10/0.42 fof(f655,plain,(
% 0.10/0.42 ~sk_c3=identity|~sQ5_spl|~sQ6_spl|~sQ4_spl|~sQ3_spl|sQ11_spl),
% 0.10/0.42 inference(forward_demodulation,[status(thm)],[f51,f654])).
% 0.10/0.42 fof(f663,plain,(
% 0.10/0.42 ![X0,X1]: (~multiply(identity,X0)=identity|~multiply(X1,sk_c10)=X0|~inverse(X1)=sk_c10|~sQ5_spl|~sQ6_spl|~sQ4_spl|~sQ3_spl|~sQ16_spl)),
% 0.10/0.42 inference(forward_demodulation,[status(thm)],[f650,f639])).
% 0.10/0.42 fof(f664,plain,(
% 0.10/0.42 ![X0,X1]: (~X0=identity|~multiply(X1,sk_c10)=X0|~inverse(X1)=sk_c10|~sQ5_spl|~sQ6_spl|~sQ4_spl|~sQ3_spl|~sQ16_spl)),
% 0.10/0.42 inference(forward_demodulation,[status(thm)],[f51,f663])).
% 0.10/0.42 fof(f665,plain,(
% 0.10/0.42 ![X0,X1]: (~X0=identity|~multiply(X1,identity)=X0|~inverse(X1)=sk_c10|~sQ5_spl|~sQ6_spl|~sQ4_spl|~sQ3_spl|~sQ16_spl)),
% 0.10/0.42 inference(forward_demodulation,[status(thm)],[f650,f664])).
% 0.10/0.42 fof(f666,plain,(
% 0.10/0.42 ![X0,X1]: (~X0=identity|~multiply(X1,identity)=X0|~inverse(X1)=identity|~sQ5_spl|~sQ6_spl|~sQ4_spl|~sQ3_spl|~sQ16_spl)),
% 0.10/0.42 inference(forward_demodulation,[status(thm)],[f650,f665])).
% 0.10/0.42 fof(f668,plain,(
% 0.10/0.42 ~identity=identity|~inverse(inverse(identity))=identity|~sQ5_spl|~sQ6_spl|~sQ4_spl|~sQ3_spl|~sQ16_spl),
% 0.10/0.42 inference(resolution,[status(thm)],[f666,f52])).
% 0.10/0.42 fof(f680,definition,(
% 0.10/0.42 sQ60_spl <=> (identity=identity)),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ60_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f682,plain,(
% 0.10/0.42 ~identity=identity|sQ60_spl),
% 0.10/0.42 inference(component_clause,[status(thm)],[f680])).
% 0.10/0.42 fof(f687,definition,(
% 0.10/0.42 sQ62_spl <=> (inverse(inverse(identity))=identity)),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f689,plain,(
% 0.10/0.42 ~inverse(inverse(identity))=identity|sQ62_spl),
% 0.10/0.42 inference(component_clause,[status(thm)],[f687])).
% 0.10/0.42 fof(f690,plain,(
% 0.10/0.42 ~sQ60_spl|~sQ62_spl|~sQ5_spl|~sQ6_spl|~sQ4_spl|~sQ3_spl|~sQ16_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f668,f680,f687,f121,f125,f117,f113,f195])).
% 0.10/0.42 fof(f696,definition,(
% 0.10/0.42 sQ64_spl <=> (multiply(sk_c3,sk_c2)=identity)),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f698,plain,(
% 0.10/0.42 ~multiply(sk_c3,sk_c2)=identity|sQ64_spl),
% 0.10/0.42 inference(component_clause,[status(thm)],[f696])).
% 0.10/0.42 fof(f704,definition,(
% 0.10/0.42 ![X0]: (sQ66_spl <=> (~X0=identity|~identity=X0))),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ66_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f705,plain,(
% 0.10/0.42 ![X0]: (~X0=identity|~identity=X0|~sQ66_spl)),
% 0.10/0.42 inference(component_clause,[status(thm)],[f704])).
% 0.10/0.42 fof(f714,plain,(
% 0.10/0.42 $false|sQ60_spl),
% 0.10/0.42 inference(trivial_equality_resolution,[status(thm)],[f682])).
% 0.10/0.42 fof(f715,plain,(
% 0.10/0.42 sQ60_spl),
% 0.10/0.42 inference(contradiction_clause,[status(thm)],[f714])).
% 0.10/0.42 fof(f716,plain,(
% 0.10/0.42 ~inverse(identity)=identity|~sQ5_spl|~sQ6_spl|~sQ4_spl|~sQ3_spl|sQ62_spl),
% 0.10/0.42 inference(forward_demodulation,[status(thm)],[f623,f689])).
% 0.10/0.42 fof(f717,plain,(
% 0.10/0.42 ~identity=identity|~sQ5_spl|~sQ6_spl|~sQ4_spl|~sQ3_spl|sQ62_spl),
% 0.10/0.42 inference(forward_demodulation,[status(thm)],[f623,f716])).
% 0.10/0.42 fof(f718,plain,(
% 0.10/0.42 $false|~sQ5_spl|~sQ6_spl|~sQ4_spl|~sQ3_spl|sQ62_spl),
% 0.10/0.42 inference(trivial_equality_resolution,[status(thm)],[f717])).
% 0.10/0.42 fof(f719,plain,(
% 0.10/0.42 ~sQ5_spl|~sQ6_spl|~sQ4_spl|~sQ3_spl|sQ62_spl),
% 0.10/0.42 inference(contradiction_clause,[status(thm)],[f718])).
% 0.10/0.42 fof(f726,plain,(
% 0.10/0.42 ~inverse(inverse(identity))=sk_c9|~sQ5_spl|~sQ6_spl|~sQ4_spl|~sQ3_spl|sQ42_spl),
% 0.10/0.42 inference(forward_demodulation,[status(thm)],[f600,f350])).
% 0.10/0.42 fof(f727,plain,(
% 0.10/0.42 ~inverse(identity)=sk_c9|~sQ5_spl|~sQ6_spl|~sQ4_spl|~sQ3_spl|sQ42_spl),
% 0.10/0.42 inference(forward_demodulation,[status(thm)],[f623,f726])).
% 0.10/0.42 fof(f728,plain,(
% 0.10/0.42 ~identity=sk_c9|~sQ5_spl|~sQ6_spl|~sQ4_spl|~sQ3_spl|sQ42_spl),
% 0.10/0.42 inference(forward_demodulation,[status(thm)],[f623,f727])).
% 0.10/0.42 fof(f729,plain,(
% 0.10/0.42 ~identity=identity|~sQ5_spl|~sQ6_spl|~sQ4_spl|~sQ3_spl|sQ42_spl),
% 0.10/0.42 inference(forward_demodulation,[status(thm)],[f600,f728])).
% 0.10/0.42 fof(f730,plain,(
% 0.10/0.42 $false|~sQ5_spl|~sQ6_spl|~sQ4_spl|~sQ3_spl|sQ42_spl),
% 0.10/0.42 inference(trivial_equality_resolution,[status(thm)],[f729])).
% 0.10/0.42 fof(f731,plain,(
% 0.10/0.42 ~sQ5_spl|~sQ6_spl|~sQ4_spl|~sQ3_spl|sQ42_spl),
% 0.10/0.42 inference(contradiction_clause,[status(thm)],[f730])).
% 0.10/0.42 fof(f732,plain,(
% 0.10/0.42 ![X0]: (~X0=identity|~sQ66_spl)),
% 0.10/0.42 inference(duplicate_literals_removal,[status(thm)],[f705])).
% 0.10/0.42 fof(f734,plain,(
% 0.10/0.42 $false|~sQ66_spl),
% 0.10/0.42 inference(backward_subsumption_resolution,[status(thm)],[f52,f732])).
% 0.10/0.42 fof(f738,plain,(
% 0.10/0.42 ~sQ66_spl),
% 0.10/0.42 inference(contradiction_clause,[status(thm)],[f734])).
% 0.10/0.42 fof(f740,plain,(
% 0.10/0.42 ![X0]: (multiply(sk_c3,X0)=multiply(sk_c2,multiply(sk_c10,X0))|~sQ12_spl)),
% 0.10/0.42 inference(paramodulation,[status(thm)],[f166,f53])).
% 0.10/0.42 fof(f747,plain,(
% 0.10/0.42 multiply(sk_c1,sk_c9)=sk_c9|~sQ11_spl|~sQ13_spl|~sQ12_spl|~sQ0_spl),
% 0.10/0.42 inference(backward_demodulation,[status(thm)],[f413,f103])).
% 0.10/0.42 fof(f749,plain,(
% 0.10/0.42 ~multiply(sk_c9,sk_c8)=sk_c9|~sQ11_spl|~sQ13_spl|~sQ12_spl|sQ4_spl),
% 0.10/0.42 inference(backward_demodulation,[status(thm)],[f413,f119])).
% 0.10/0.42 fof(f750,plain,(
% 0.10/0.42 multiply(sk_c9,sk_c9)=sk_c8|~sQ11_spl|~sQ13_spl|~sQ12_spl),
% 0.10/0.42 inference(backward_demodulation,[status(thm)],[f413,f54])).
% 0.10/0.42 fof(f751,plain,(
% 0.10/0.42 inverse(sk_c2)=sk_c9|~sQ11_spl|~sQ12_spl|~sQ13_spl),
% 0.10/0.42 inference(backward_demodulation,[status(thm)],[f413,f178])).
% 0.10/0.42 fof(f752,plain,(
% 0.10/0.42 multiply(sk_c2,sk_c9)=sk_c3|~sQ11_spl|~sQ13_spl|~sQ12_spl),
% 0.10/0.42 inference(backward_demodulation,[status(thm)],[f413,f166])).
% 0.10/0.42 fof(f753,plain,(
% 0.10/0.42 multiply(sk_c9,sk_c3)=sk_c9|~sQ13_spl|~sQ12_spl|~sQ11_spl),
% 0.10/0.42 inference(forward_demodulation,[status(thm)],[f413,f154])).
% 0.10/0.42 fof(f754,plain,(
% 0.10/0.42 sk_c3=multiply(inverse(sk_c9),sk_c9)|~sQ13_spl|~sQ12_spl|~sQ11_spl),
% 0.10/0.42 inference(paramodulation,[status(thm)],[f753,f220])).
% 0.10/0.42 fof(f762,plain,(
% 0.10/0.42 ![X0]: (multiply(sk_c9,X0)=multiply(sk_c1,multiply(sk_c9,X0))|~sQ11_spl|~sQ13_spl|~sQ12_spl|~sQ0_spl)),
% 0.10/0.42 inference(paramodulation,[status(thm)],[f747,f53])).
% 0.10/0.42 fof(f766,plain,(
% 0.10/0.42 $false|sQ59_spl|~sQ11_spl|~sQ12_spl|~sQ13_spl),
% 0.10/0.42 inference(forward_subsumption_resolution,[status(thm)],[f751,f567])).
% 0.10/0.42 fof(f767,plain,(
% 0.10/0.42 sQ59_spl|~sQ11_spl|~sQ12_spl|~sQ13_spl),
% 0.10/0.42 inference(contradiction_clause,[status(thm)],[f766])).
% 0.10/0.42 fof(f773,plain,(
% 0.10/0.42 ![X0]: (~multiply(X0,sk_c9)=sk_c3|~inverse(X0)=sk_c10|~sQ11_spl|~sQ13_spl|~sQ12_spl|~sQ40_spl)),
% 0.10/0.42 inference(forward_demodulation,[status(thm)],[f413,f334])).
% 0.10/0.42 fof(f774,plain,(
% 0.10/0.42 ![X0]: (~multiply(X0,sk_c9)=sk_c3|~inverse(X0)=sk_c9|~sQ11_spl|~sQ13_spl|~sQ12_spl|~sQ40_spl)),
% 0.10/0.42 inference(forward_demodulation,[status(thm)],[f413,f773])).
% 0.10/0.42 fof(f775,plain,(
% 0.10/0.42 ~inverse(sk_c2)=sk_c9|~sQ40_spl|~sQ11_spl|~sQ13_spl|~sQ12_spl),
% 0.10/0.42 inference(resolution,[status(thm)],[f774,f752])).
% 0.10/0.42 fof(f782,plain,(
% 0.10/0.42 ~sQ59_spl|~sQ40_spl|~sQ11_spl|~sQ13_spl|~sQ12_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f775,f565,f333,f153,f177,f165])).
% 0.10/0.42 fof(f788,definition,(
% 0.10/0.42 sQ69_spl <=> (identity=sk_c3)),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ69_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f790,plain,(
% 0.10/0.42 ~identity=sk_c3|sQ69_spl),
% 0.10/0.42 inference(component_clause,[status(thm)],[f788])).
% 0.10/0.42 fof(f793,definition,(
% 0.10/0.42 sQ70_spl <=> (sk_c3=sk_c3)),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ70_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f795,plain,(
% 0.10/0.42 ~sk_c3=sk_c3|sQ70_spl),
% 0.10/0.42 inference(component_clause,[status(thm)],[f793])).
% 0.10/0.42 fof(f797,plain,(
% 0.10/0.42 $false|sQ70_spl),
% 0.10/0.42 inference(trivial_equality_resolution,[status(thm)],[f795])).
% 0.10/0.42 fof(f798,plain,(
% 0.10/0.42 sQ70_spl),
% 0.10/0.42 inference(contradiction_clause,[status(thm)],[f797])).
% 0.10/0.42 fof(f839,plain,(
% 0.10/0.42 ![X0]: (~inverse(X0)=sk_c2|~multiply(X0,sk_c9)=sk_c2|~sQ11_spl|~sQ13_spl|~sQ12_spl|~sQ28_spl)),
% 0.10/0.42 inference(forward_demodulation,[status(thm)],[f413,f266])).
% 0.10/0.42 fof(f842,plain,(
% 0.10/0.42 ~inverse(sk_c9)=sk_c2|~sk_c8=sk_c2|~sQ28_spl|~sQ11_spl|~sQ13_spl|~sQ12_spl),
% 0.10/0.42 inference(paramodulation,[status(thm)],[f750,f839])).
% 0.10/0.42 fof(f843,plain,(
% 0.10/0.42 ~inverse(inverse(identity))=sk_c2|~sk_c9=sk_c2|~sQ11_spl|~sQ13_spl|~sQ12_spl|~sQ28_spl),
% 0.10/0.42 inference(paramodulation,[status(thm)],[f399,f839])).
% 0.10/0.42 fof(f844,plain,(
% 0.10/0.42 ~inverse(inverse(sk_c9))=sk_c2|~identity=sk_c2|~sQ11_spl|~sQ13_spl|~sQ12_spl|~sQ28_spl),
% 0.10/0.42 inference(paramodulation,[status(thm)],[f52,f839])).
% 0.10/0.42 fof(f845,plain,(
% 0.10/0.42 ~inverse(identity)=sk_c2|~sk_c9=sk_c2|~sQ11_spl|~sQ13_spl|~sQ12_spl|~sQ28_spl),
% 0.10/0.42 inference(paramodulation,[status(thm)],[f51,f839])).
% 0.10/0.42 fof(f846,plain,(
% 0.10/0.42 ~inverse(sk_c2)=sk_c2|~sk_c3=sk_c2|~sQ28_spl|~sQ11_spl|~sQ13_spl|~sQ12_spl),
% 0.10/0.42 inference(paramodulation,[status(thm)],[f752,f839])).
% 0.10/0.42 fof(f851,definition,(
% 0.10/0.42 sQ72_spl <=> (sk_c9=sk_c2)),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ72_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f853,plain,(
% 0.10/0.42 ~sk_c9=sk_c2|sQ72_spl),
% 0.10/0.42 inference(component_clause,[status(thm)],[f851])).
% 0.10/0.42 fof(f859,definition,(
% 0.10/0.42 sQ74_spl <=> (inverse(sk_c9)=sk_c2)),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ74_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f861,plain,(
% 0.10/0.42 ~inverse(sk_c9)=sk_c2|sQ74_spl),
% 0.10/0.42 inference(component_clause,[status(thm)],[f859])).
% 0.10/0.42 fof(f862,definition,(
% 0.10/0.42 sQ75_spl <=> (sk_c8=sk_c2)),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ75_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f865,plain,(
% 0.10/0.42 ~sQ74_spl|~sQ75_spl|~sQ28_spl|~sQ11_spl|~sQ13_spl|~sQ12_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f842,f859,f862,f265,f153,f177,f165])).
% 0.10/0.42 fof(f866,definition,(
% 0.10/0.42 sQ76_spl <=> (inverse(inverse(identity))=sk_c2)),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ76_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f869,plain,(
% 0.10/0.42 ~sQ76_spl|~sQ72_spl|~sQ11_spl|~sQ13_spl|~sQ12_spl|~sQ28_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f843,f866,f851,f153,f177,f165,f265])).
% 0.10/0.42 fof(f870,definition,(
% 0.10/0.42 sQ77_spl <=> (inverse(inverse(sk_c9))=sk_c2)),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ77_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f873,definition,(
% 0.10/0.42 sQ78_spl <=> (identity=sk_c2)),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ78_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f875,plain,(
% 0.10/0.42 ~identity=sk_c2|sQ78_spl),
% 0.10/0.42 inference(component_clause,[status(thm)],[f873])).
% 0.10/0.42 fof(f876,plain,(
% 0.10/0.42 ~sQ77_spl|~sQ78_spl|~sQ11_spl|~sQ13_spl|~sQ12_spl|~sQ28_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f844,f870,f873,f153,f177,f165,f265])).
% 0.10/0.42 fof(f877,definition,(
% 0.10/0.42 sQ79_spl <=> (inverse(identity)=sk_c2)),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ79_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f880,plain,(
% 0.10/0.42 ~sQ79_spl|~sQ72_spl|~sQ11_spl|~sQ13_spl|~sQ12_spl|~sQ28_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f845,f877,f851,f153,f177,f165,f265])).
% 0.10/0.42 fof(f881,definition,(
% 0.10/0.42 sQ80_spl <=> (inverse(sk_c2)=sk_c2)),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ80_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f883,plain,(
% 0.10/0.42 ~inverse(sk_c2)=sk_c2|sQ80_spl),
% 0.10/0.42 inference(component_clause,[status(thm)],[f881])).
% 0.10/0.42 fof(f884,definition,(
% 0.10/0.42 sQ81_spl <=> (sk_c3=sk_c2)),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ81_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f886,plain,(
% 0.10/0.42 ~sk_c3=sk_c2|sQ81_spl),
% 0.10/0.42 inference(component_clause,[status(thm)],[f884])).
% 0.10/0.42 fof(f887,plain,(
% 0.10/0.42 ~sQ80_spl|~sQ81_spl|~sQ28_spl|~sQ11_spl|~sQ13_spl|~sQ12_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f846,f881,f884,f265,f153,f177,f165])).
% 0.10/0.42 fof(f906,plain,(
% 0.10/0.42 multiply(identity,identity)=sk_c3|~sQ13_spl|~sQ3_spl|~sQ5_spl|~sQ6_spl|~sQ4_spl|~sQ12_spl),
% 0.10/0.42 inference(backward_demodulation,[status(thm)],[f652,f648])).
% 0.10/0.42 fof(f907,plain,(
% 0.10/0.42 identity=sk_c3|~sQ13_spl|~sQ3_spl|~sQ5_spl|~sQ6_spl|~sQ4_spl|~sQ12_spl),
% 0.10/0.42 inference(forward_demodulation,[status(thm)],[f51,f906])).
% 0.10/0.42 fof(f915,plain,(
% 0.10/0.42 $false|sQ11_spl|~sQ13_spl|~sQ3_spl|~sQ5_spl|~sQ6_spl|~sQ4_spl|~sQ12_spl),
% 0.10/0.42 inference(forward_subsumption_resolution,[status(thm)],[f907,f655])).
% 0.10/0.42 fof(f916,plain,(
% 0.10/0.42 sQ11_spl|~sQ13_spl|~sQ3_spl|~sQ5_spl|~sQ6_spl|~sQ4_spl|~sQ12_spl),
% 0.10/0.42 inference(contradiction_clause,[status(thm)],[f915])).
% 0.10/0.42 fof(f917,plain,(
% 0.10/0.42 sk_c3=identity|~sQ13_spl|~sQ12_spl|~sQ11_spl),
% 0.10/0.42 inference(forward_demodulation,[status(thm)],[f52,f754])).
% 0.10/0.42 fof(f925,plain,(
% 0.10/0.42 sk_c3=multiply(inverse(sk_c9),sk_c9)|~sQ13_spl|~sQ12_spl|~sQ11_spl),
% 0.10/0.42 inference(paramodulation,[status(thm)],[f753,f220])).
% 0.10/0.42 fof(f927,plain,(
% 0.10/0.42 sk_c3=identity|~sQ13_spl|~sQ12_spl|~sQ11_spl),
% 0.10/0.42 inference(forward_demodulation,[status(thm)],[f52,f925])).
% 0.10/0.42 fof(f935,plain,(
% 0.10/0.42 sk_c9=sk_c10|~sQ11_spl|~sQ12_spl|~sQ13_spl),
% 0.10/0.42 inference(backward_demodulation,[status(thm)],[f751,f178])).
% 0.10/0.42 fof(f941,plain,(
% 0.10/0.42 sk_c9=sk_c10|~sQ11_spl|~sQ13_spl|~sQ12_spl|~sQ0_spl),
% 0.10/0.42 inference(forward_demodulation,[status(thm)],[f747,f103])).
% 0.10/0.42 fof(f1066,plain,(
% 0.10/0.42 multiply(sk_c9,sk_c2)=identity|~sQ11_spl|~sQ12_spl|~sQ0_spl|~sQ13_spl),
% 0.10/0.42 inference(forward_demodulation,[status(thm)],[f941,f218])).
% 0.10/0.42 fof(f1070,plain,(
% 0.10/0.42 $false|sQ69_spl|~sQ13_spl|~sQ12_spl|~sQ11_spl),
% 0.10/0.42 inference(forward_subsumption_resolution,[status(thm)],[f917,f790])).
% 0.10/0.42 fof(f1071,plain,(
% 0.10/0.42 sQ69_spl|~sQ13_spl|~sQ12_spl|~sQ11_spl),
% 0.10/0.42 inference(contradiction_clause,[status(thm)],[f1070])).
% 0.10/0.42 fof(f1083,plain,(
% 0.10/0.42 multiply(sk_c2,sk_c9)=identity|~sQ11_spl|~sQ13_spl|~sQ12_spl),
% 0.10/0.42 inference(backward_demodulation,[status(thm)],[f927,f752])).
% 0.10/0.42 fof(f1086,plain,(
% 0.10/0.42 ~identity=sk_c2|~sQ13_spl|~sQ12_spl|~sQ11_spl|sQ81_spl),
% 0.10/0.42 inference(backward_demodulation,[status(thm)],[f927,f886])).
% 0.10/0.42 fof(f1087,plain,(
% 0.10/0.42 ~identity=sk_c9|~sQ13_spl|~sQ12_spl|~sQ11_spl|sQ38_spl),
% 0.10/0.42 inference(backward_demodulation,[status(thm)],[f927,f325])).
% 0.10/0.42 fof(f1107,plain,(
% 0.10/0.42 ![X0]: (multiply(identity,X0)=multiply(sk_c2,multiply(sk_c10,X0))|~sQ13_spl|~sQ11_spl|~sQ12_spl)),
% 0.10/0.42 inference(forward_demodulation,[status(thm)],[f927,f740])).
% 0.10/0.42 fof(f1108,plain,(
% 0.10/0.42 ![X0]: (X0=multiply(sk_c2,multiply(sk_c10,X0))|~sQ13_spl|~sQ11_spl|~sQ12_spl)),
% 0.10/0.42 inference(forward_demodulation,[status(thm)],[f51,f1107])).
% 0.10/0.42 fof(f1109,plain,(
% 0.10/0.42 ![X0]: (X0=multiply(sk_c2,multiply(sk_c9,X0))|~sQ0_spl|~sQ13_spl|~sQ11_spl|~sQ12_spl)),
% 0.10/0.42 inference(forward_demodulation,[status(thm)],[f941,f1108])).
% 0.10/0.42 fof(f1174,plain,(
% 0.10/0.42 ![X0]: (~inverse(X0)=sk_c1|~multiply(X0,sk_c9)=sk_c1|~sQ11_spl|~sQ13_spl|~sQ12_spl|~sQ0_spl|~sQ27_spl)),
% 0.10/0.42 inference(forward_demodulation,[status(thm)],[f941,f262])).
% 0.10/0.42 fof(f1175,plain,(
% 0.10/0.42 ~inverse(sk_c2)=sk_c1|~identity=sk_c1|~sQ0_spl|~sQ27_spl|~sQ11_spl|~sQ13_spl|~sQ12_spl),
% 0.10/0.42 inference(paramodulation,[status(thm)],[f1083,f1174])).
% 0.10/0.42 fof(f1181,definition,(
% 0.10/0.42 sQ116_spl <=> (inverse(sk_c2)=sk_c1)),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ116_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f1183,plain,(
% 0.10/0.42 ~inverse(sk_c2)=sk_c1|sQ116_spl),
% 0.10/0.42 inference(component_clause,[status(thm)],[f1181])).
% 0.10/0.42 fof(f1184,definition,(
% 0.10/0.42 sQ117_spl <=> (identity=sk_c1)),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ117_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f1186,plain,(
% 0.10/0.42 ~identity=sk_c1|sQ117_spl),
% 0.10/0.42 inference(component_clause,[status(thm)],[f1184])).
% 0.10/0.42 fof(f1187,plain,(
% 0.10/0.42 ~sQ116_spl|~sQ117_spl|~sQ0_spl|~sQ27_spl|~sQ11_spl|~sQ13_spl|~sQ12_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f1175,f1181,f1184,f102,f261,f153,f177,f165])).
% 0.10/0.42 fof(f1191,definition,(
% 0.10/0.42 sQ119_spl <=> (sk_c9=sk_c1)),
% 0.10/0.42 introduced(definition,[new_symbols(definition,[sQ119_spl])],[split_symbol_definition])).
% 0.10/0.42 fof(f1193,plain,(
% 0.10/0.42 ~sk_c9=sk_c1|sQ119_spl),
% 0.10/0.42 inference(component_clause,[status(thm)],[f1191])).
% 0.10/0.42 fof(f1211,plain,(
% 0.10/0.42 ~sk_c9=sk_c1|~sQ11_spl|~sQ12_spl|~sQ13_spl|sQ116_spl),
% 0.10/0.42 inference(forward_demodulation,[status(thm)],[f751,f1183])).
% 0.10/0.42 fof(f1219,plain,(
% 0.10/0.42 multiply(sk_c9,sk_c2)=multiply(sk_c1,identity)|~sQ11_spl|~sQ12_spl|~sQ0_spl|~sQ13_spl),
% 0.10/0.42 inference(paramodulation,[status(thm)],[f1066,f762])).
% 0.10/0.42 fof(f1225,plain,(
% 0.10/0.42 identity=multiply(sk_c1,identity)|~sQ11_spl|~sQ12_spl|~sQ0_spl|~sQ13_spl),
% 0.10/0.42 inference(forward_demodulation,[status(thm)],[f1066,f1219])).
% 0.10/0.42 fof(f1234,plain,(
% 0.10/0.42 multiply(sk_c9,sk_c1)=multiply(sk_c1,identity)|~sQ11_spl|~sQ13_spl|~sQ12_spl|~sQ0_spl|~sQ10_spl),
% 0.10/0.42 inference(paramodulation,[status(thm)],[f217,f762])).
% 0.10/0.42 fof(f1235,plain,(
% 0.10/0.42 sk_c1=multiply(sk_c2,identity)|~sQ0_spl|~sQ13_spl|~sQ11_spl|~sQ12_spl|~sQ10_spl),
% 0.10/0.42 inference(paramodulation,[status(thm)],[f217,f1109])).
% 0.10/0.42 fof(f1239,plain,(
% 0.10/0.42 identity=multiply(sk_c1,identity)|~sQ11_spl|~sQ13_spl|~sQ12_spl|~sQ0_spl|~sQ10_spl),
% 0.10/0.42 inference(forward_demodulation,[status(thm)],[f217,f1234])).
% 0.10/0.42 fof(f1243,plain,(
% 0.10/0.42 ~sk_c9=sk_c2|~sQ11_spl|~sQ12_spl|~sQ13_spl|sQ80_spl),
% 0.10/0.42 inference(forward_demodulation,[status(thm)],[f751,f883])).
% 0.10/0.42 fof(f1264,plain,(
% 0.10/0.42 sk_c2=multiply(inverse(sk_c9),identity)|~sQ11_spl|~sQ12_spl|~sQ0_spl|~sQ13_spl),
% 0.10/0.42 inference(forward_demodulation,[status(thm)],[f941,f394])).
% 0.10/0.42 fof(f1280,plain,(
% 0.10/0.42 sk_c2=inverse(sk_c9)|~sQ11_spl|~sQ12_spl|~sQ0_spl|~sQ13_spl),
% 0.10/0.42 inference(backward_demodulation,[status(thm)],[f1281,f1264])).
% 0.10/0.42 fof(f1281,plain,(
% 0.10/0.42 ![X0]: (X0=multiply(X0,identity))),
% 0.10/0.42 inference(forward_demodulation,[status(thm)],[f397,f398])).
% 0.10/0.42 fof(f1296,plain,(
% 0.10/0.42 $false|sQ74_spl|~sQ11_spl|~sQ12_spl|~sQ0_spl|~sQ13_spl),
% 0.10/0.42 inference(forward_subsumption_resolution,[status(thm)],[f1280,f861])).
% 0.10/0.42 fof(f1297,plain,(
% 0.10/0.42 sQ74_spl|~sQ11_spl|~sQ12_spl|~sQ0_spl|~sQ13_spl),
% 0.10/0.42 inference(contradiction_clause,[status(thm)],[f1296])).
% 0.10/0.42 fof(f1316,plain,(
% 0.10/0.42 sk_c2=sk_c9|~sQ5_spl|~sQ6_spl|~sQ4_spl|~sQ13_spl),
% 0.10/0.42 inference(forward_demodulation,[status(thm)],[f1281,f595])).
% 0.10/0.42 fof(f1317,plain,(
% 0.10/0.42 $false|sQ72_spl|~sQ5_spl|~sQ6_spl|~sQ4_spl|~sQ13_spl),
% 0.10/0.42 inference(forward_subsumption_resolution,[status(thm)],[f1316,f853])).
% 0.10/0.42 fof(f1318,plain,(
% 0.10/0.42 sQ72_spl|~sQ5_spl|~sQ6_spl|~sQ4_spl|~sQ13_spl),
% 0.10/0.42 inference(contradiction_clause,[status(thm)],[f1317])).
% 0.10/0.42 fof(f1319,plain,(
% 0.10/0.42 ~multiply(identity,sk_c9)=sk_c10|~sQ13_spl|~sQ12_spl|~sQ11_spl|sQ51_spl),
% 0.10/0.42 inference(forward_demodulation,[status(thm)],[f927,f502])).
% 0.10/0.42 fof(f1320,plain,(
% 0.10/0.42 ~sk_c9=sk_c10|~sQ13_spl|~sQ12_spl|~sQ11_spl|sQ51_spl),
% 0.10/0.42 inference(forward_demodulation,[status(thm)],[f51,f1319])).
% 0.10/0.42 fof(f1325,plain,(
% 0.10/0.42 ~multiply(identity,sk_c2)=identity|~sQ13_spl|~sQ12_spl|~sQ11_spl|sQ64_spl),
% 0.10/0.42 inference(forward_demodulation,[status(thm)],[f927,f698])).
% 0.10/0.42 fof(f1326,plain,(
% 0.10/0.42 ~sk_c2=identity|~sQ13_spl|~sQ12_spl|~sQ11_spl|sQ64_spl),
% 0.10/0.42 inference(forward_demodulation,[status(thm)],[f51,f1325])).
% 0.10/0.42 fof(f1334,plain,(
% 0.10/0.42 identity=sk_c1|~sQ11_spl|~sQ12_spl|~sQ0_spl|~sQ13_spl),
% 0.10/0.42 inference(forward_demodulation,[status(thm)],[f1281,f1225])).
% 0.10/0.42 fof(f1335,plain,(
% 0.10/0.42 identity=sk_c1|~sQ11_spl|~sQ13_spl|~sQ12_spl|~sQ0_spl|~sQ10_spl),
% 0.10/0.42 inference(forward_demodulation,[status(thm)],[f1281,f1239])).
% 0.10/0.42 fof(f1336,plain,(
% 0.10/0.42 sk_c1=sk_c2|~sQ0_spl|~sQ13_spl|~sQ11_spl|~sQ12_spl|~sQ10_spl),
% 0.10/0.42 inference(forward_demodulation,[status(thm)],[f1281,f1235])).
% 0.10/0.42 fof(f1375,plain,(
% 0.10/0.42 ~inverse(sk_c2)=sk_c2|~identity=sk_c2|~sQ28_spl|~sQ11_spl|~sQ13_spl|~sQ12_spl),
% 0.10/0.42 inference(paramodulation,[status(thm)],[f1083,f839])).
% 0.10/0.42 fof(f1382,plain,(
% 0.10/0.42 ~sQ80_spl|~sQ78_spl|~sQ28_spl|~sQ11_spl|~sQ13_spl|~sQ12_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f1375,f881,f873,f265,f153,f177,f165])).
% 0.10/0.42 fof(f1394,plain,(
% 0.10/0.42 ~sk_c9=sk_c9|~sQ13_spl|~sQ12_spl|~sQ11_spl|sQ51_spl),
% 0.10/0.42 inference(forward_demodulation,[status(thm)],[f935,f1320])).
% 0.10/0.42 fof(f1395,plain,(
% 0.10/0.42 $false|~sQ13_spl|~sQ12_spl|~sQ11_spl|sQ51_spl),
% 0.10/0.42 inference(trivial_equality_resolution,[status(thm)],[f1394])).
% 0.10/0.42 fof(f1396,plain,(
% 0.10/0.42 ~sQ13_spl|~sQ12_spl|~sQ11_spl|sQ51_spl),
% 0.10/0.42 inference(contradiction_clause,[status(thm)],[f1395])).
% 0.10/0.42 fof(f1406,plain,(
% 0.10/0.42 $false|sQ117_spl|~sQ11_spl|~sQ12_spl|~sQ0_spl|~sQ13_spl),
% 0.10/0.42 inference(forward_subsumption_resolution,[status(thm)],[f1334,f1186])).
% 0.10/0.42 fof(f1407,plain,(
% 0.10/0.42 sQ117_spl|~sQ11_spl|~sQ12_spl|~sQ0_spl|~sQ13_spl),
% 0.10/0.42 inference(contradiction_clause,[status(thm)],[f1406])).
% 0.10/0.42 fof(f1409,plain,(
% 0.10/0.42 inverse(identity)=sk_c9|~sQ11_spl|~sQ13_spl|~sQ12_spl|~sQ0_spl|~sQ10_spl),
% 0.10/0.42 inference(backward_demodulation,[status(thm)],[f1335,f142])).
% 0.10/0.42 fof(f1410,plain,(
% 0.10/0.42 ~sk_c9=identity|~sQ11_spl|~sQ13_spl|~sQ12_spl|~sQ0_spl|~sQ10_spl|sQ119_spl),
% 0.10/0.42 inference(backward_demodulation,[status(thm)],[f1335,f1193])).
% 0.10/0.42 fof(f1418,plain,(
% 0.10/0.42 identity=sk_c2|~sQ0_spl|~sQ13_spl|~sQ11_spl|~sQ12_spl|~sQ10_spl),
% 0.10/0.42 inference(forward_demodulation,[status(thm)],[f1335,f1336])).
% 0.10/0.42 fof(f1419,plain,(
% 0.10/0.42 $false|sQ78_spl|~sQ0_spl|~sQ13_spl|~sQ11_spl|~sQ12_spl|~sQ10_spl),
% 0.10/0.42 inference(forward_subsumption_resolution,[status(thm)],[f1418,f875])).
% 0.10/0.42 fof(f1420,plain,(
% 0.10/0.42 sQ78_spl|~sQ0_spl|~sQ13_spl|~sQ11_spl|~sQ12_spl|~sQ10_spl),
% 0.10/0.42 inference(contradiction_clause,[status(thm)],[f1419])).
% 0.10/0.42 fof(f1421,plain,(
% 0.10/0.42 ~sQ78_spl|~sQ13_spl|~sQ12_spl|~sQ11_spl|sQ64_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f1326,f873,f177,f165,f153,f696])).
% 0.10/0.42 fof(f1422,plain,(
% 0.10/0.42 ~sQ78_spl|~sQ13_spl|~sQ12_spl|~sQ11_spl|sQ81_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f1086,f873,f177,f165,f153,f884])).
% 0.10/0.42 fof(f1428,plain,(
% 0.10/0.42 multiply(sk_c9,identity)=identity|~sQ11_spl|~sQ13_spl|~sQ12_spl|~sQ0_spl|~sQ10_spl),
% 0.10/0.42 inference(paramodulation,[status(thm)],[f1409,f52])).
% 0.10/0.42 fof(f1431,plain,(
% 0.10/0.42 sk_c9=identity|~sQ11_spl|~sQ13_spl|~sQ12_spl|~sQ0_spl|~sQ10_spl),
% 0.10/0.42 inference(forward_demodulation,[status(thm)],[f1281,f1428])).
% 0.10/0.42 fof(f1432,plain,(
% 0.10/0.42 $false|sQ38_spl|~sQ11_spl|~sQ13_spl|~sQ12_spl|~sQ0_spl|~sQ10_spl),
% 0.10/0.42 inference(forward_subsumption_resolution,[status(thm)],[f1431,f1087])).
% 0.10/0.42 fof(f1433,plain,(
% 0.10/0.42 sQ38_spl|~sQ11_spl|~sQ13_spl|~sQ12_spl|~sQ0_spl|~sQ10_spl),
% 0.10/0.42 inference(contradiction_clause,[status(thm)],[f1432])).
% 0.10/0.42 fof(f1439,plain,(
% 0.10/0.42 multiply(identity,sk_c9)=identity|~sQ0_spl|~sQ10_spl|~sQ11_spl|~sQ13_spl|~sQ12_spl),
% 0.10/0.42 inference(backward_demodulation,[status(thm)],[f1418,f1083])).
% 0.10/0.42 fof(f1446,plain,(
% 0.10/0.42 sk_c9=identity|~sQ0_spl|~sQ10_spl|~sQ11_spl|~sQ13_spl|~sQ12_spl),
% 0.10/0.42 inference(forward_demodulation,[status(thm)],[f51,f1439])).
% 0.10/0.42 fof(f1447,plain,(
% 0.10/0.42 inverse(identity)=identity|~sQ11_spl|~sQ13_spl|~sQ12_spl|~sQ0_spl|~sQ10_spl),
% 0.10/0.42 inference(backward_demodulation,[status(thm)],[f1446,f1409])).
% 0.10/0.42 fof(f1458,plain,(
% 0.10/0.42 ~multiply(sk_c9,sk_c8)=identity|~sQ0_spl|~sQ10_spl|~sQ11_spl|~sQ13_spl|~sQ12_spl|sQ4_spl),
% 0.10/0.42 inference(backward_demodulation,[status(thm)],[f1446,f749])).
% 0.10/0.42 fof(f1461,plain,(
% 0.10/0.42 multiply(sk_c9,identity)=sk_c8|~sQ0_spl|~sQ10_spl|~sQ11_spl|~sQ13_spl|~sQ12_spl),
% 0.10/0.42 inference(backward_demodulation,[status(thm)],[f1446,f750])).
% 0.10/0.42 fof(f1467,plain,(
% 0.10/0.42 ~multiply(identity,sk_c8)=identity|~sQ0_spl|~sQ10_spl|~sQ11_spl|~sQ13_spl|~sQ12_spl|sQ4_spl),
% 0.10/0.42 inference(forward_demodulation,[status(thm)],[f1446,f1458])).
% 0.10/0.42 fof(f1468,plain,(
% 0.10/0.42 ~sk_c8=identity|~sQ0_spl|~sQ10_spl|~sQ11_spl|~sQ13_spl|~sQ12_spl|sQ4_spl),
% 0.10/0.42 inference(forward_demodulation,[status(thm)],[f51,f1467])).
% 0.10/0.42 fof(f1469,plain,(
% 0.10/0.42 sk_c9=sk_c8|~sQ0_spl|~sQ10_spl|~sQ11_spl|~sQ13_spl|~sQ12_spl),
% 0.10/0.42 inference(forward_demodulation,[status(thm)],[f1281,f1461])).
% 0.10/0.42 fof(f1470,plain,(
% 0.10/0.42 identity=sk_c8|~sQ0_spl|~sQ10_spl|~sQ11_spl|~sQ13_spl|~sQ12_spl),
% 0.10/0.42 inference(forward_demodulation,[status(thm)],[f1446,f1469])).
% 0.10/0.42 fof(f1484,plain,(
% 0.10/0.42 ~identity=identity|~sQ0_spl|~sQ10_spl|~sQ11_spl|~sQ13_spl|~sQ12_spl|sQ4_spl),
% 0.10/0.42 inference(forward_demodulation,[status(thm)],[f1470,f1468])).
% 0.10/0.42 fof(f1485,plain,(
% 0.10/0.42 $false|~sQ0_spl|~sQ10_spl|~sQ11_spl|~sQ13_spl|~sQ12_spl|sQ4_spl),
% 0.10/0.42 inference(trivial_equality_resolution,[status(thm)],[f1484])).
% 0.10/0.42 fof(f1486,plain,(
% 0.10/0.42 ~sQ0_spl|~sQ10_spl|~sQ11_spl|~sQ13_spl|~sQ12_spl|sQ4_spl),
% 0.10/0.42 inference(contradiction_clause,[status(thm)],[f1485])).
% 0.10/0.42 fof(f1540,plain,(
% 0.10/0.42 ~inverse(identity)=sk_c8|~sQ0_spl|~sQ10_spl|~sQ11_spl|~sQ13_spl|~sQ12_spl|sQ3_spl),
% 0.10/0.42 inference(forward_demodulation,[status(thm)],[f1446,f115])).
% 0.10/0.42 fof(f1541,plain,(
% 0.10/0.42 ~identity=sk_c8|~sQ0_spl|~sQ10_spl|~sQ11_spl|~sQ13_spl|~sQ12_spl|sQ3_spl),
% 0.10/0.42 inference(forward_demodulation,[status(thm)],[f1447,f1540])).
% 0.10/0.42 fof(f1542,plain,(
% 0.10/0.42 ~identity=identity|~sQ0_spl|~sQ10_spl|~sQ11_spl|~sQ13_spl|~sQ12_spl|sQ3_spl),
% 0.10/0.42 inference(forward_demodulation,[status(thm)],[f1470,f1541])).
% 0.10/0.42 fof(f1543,plain,(
% 0.10/0.42 $false|~sQ0_spl|~sQ10_spl|~sQ11_spl|~sQ13_spl|~sQ12_spl|sQ3_spl),
% 0.10/0.42 inference(trivial_equality_resolution,[status(thm)],[f1542])).
% 0.10/0.42 fof(f1544,plain,(
% 0.10/0.42 ~sQ0_spl|~sQ10_spl|~sQ11_spl|~sQ13_spl|~sQ12_spl|sQ3_spl),
% 0.10/0.42 inference(contradiction_clause,[status(thm)],[f1543])).
% 0.10/0.42 fof(f1584,plain,(
% 0.10/0.42 ![X0]: (~inverse(X0)=identity|~multiply(X0,sk_c8)=sk_c9|~sQ0_spl|~sQ10_spl|~sQ11_spl|~sQ13_spl|~sQ12_spl|~sQ18_spl)),
% 0.10/0.42 inference(forward_demodulation,[status(thm)],[f1446,f202])).
% 0.10/0.42 fof(f1585,plain,(
% 0.10/0.42 ![X0]: (~inverse(X0)=identity|~multiply(X0,identity)=sk_c9|~sQ0_spl|~sQ10_spl|~sQ11_spl|~sQ13_spl|~sQ12_spl|~sQ18_spl)),
% 0.10/0.42 inference(forward_demodulation,[status(thm)],[f1470,f1584])).
% 0.10/0.42 fof(f1586,plain,(
% 0.10/0.42 ![X0]: (~inverse(X0)=identity|~X0=sk_c9|~sQ0_spl|~sQ10_spl|~sQ11_spl|~sQ13_spl|~sQ12_spl|~sQ18_spl)),
% 0.10/0.42 inference(forward_demodulation,[status(thm)],[f1281,f1585])).
% 0.10/0.42 fof(f1587,plain,(
% 0.10/0.42 ![X0]: (~inverse(X0)=identity|~X0=identity|~sQ0_spl|~sQ10_spl|~sQ11_spl|~sQ13_spl|~sQ12_spl|~sQ18_spl)),
% 0.10/0.42 inference(forward_demodulation,[status(thm)],[f1446,f1586])).
% 0.10/0.42 fof(f1597,plain,(
% 0.10/0.42 ~identity=identity|~sQ11_spl|~sQ13_spl|~sQ12_spl|~sQ0_spl|~sQ10_spl|sQ119_spl),
% 0.10/0.42 inference(forward_demodulation,[status(thm)],[f1446,f1410])).
% 0.10/0.42 fof(f1598,plain,(
% 0.10/0.42 $false|~sQ11_spl|~sQ13_spl|~sQ12_spl|~sQ0_spl|~sQ10_spl|sQ119_spl),
% 0.10/0.42 inference(trivial_equality_resolution,[status(thm)],[f1597])).
% 0.10/0.42 fof(f1599,plain,(
% 0.10/0.42 ~sQ11_spl|~sQ13_spl|~sQ12_spl|~sQ0_spl|~sQ10_spl|sQ119_spl),
% 0.10/0.42 inference(contradiction_clause,[status(thm)],[f1598])).
% 0.10/0.42 fof(f1600,plain,(
% 0.10/0.42 ~sQ119_spl|~sQ11_spl|~sQ12_spl|~sQ13_spl|sQ116_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f1211,f1191,f153,f165,f177,f1181])).
% 0.10/0.42 fof(f1607,plain,(
% 0.10/0.42 ~identity=identity|~sQ18_spl|~sQ11_spl|~sQ13_spl|~sQ12_spl|~sQ0_spl|~sQ10_spl),
% 0.10/0.42 inference(resolution,[status(thm)],[f1587,f1447])).
% 0.10/0.42 fof(f1609,plain,(
% 0.10/0.42 ~sQ60_spl|~sQ18_spl|~sQ11_spl|~sQ13_spl|~sQ12_spl|~sQ0_spl|~sQ10_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f1607,f680,f201,f153,f177,f165,f102,f141])).
% 0.10/0.42 fof(f1635,plain,(
% 0.10/0.42 sQ78_spl|~sQ3_spl|~sQ5_spl|~sQ6_spl|~sQ4_spl|~sQ13_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f652,f873,f113,f121,f125,f117,f177])).
% 0.10/0.42 fof(f1640,plain,(
% 0.10/0.42 ~sQ72_spl|~sQ11_spl|~sQ12_spl|~sQ13_spl|sQ80_spl),
% 0.10/0.42 inference(split_clause,[status(thm)],[f1243,f851,f153,f165,f177,f881])).
% 0.10/0.42 fof(f1698,plain,(
% 0.10/0.42 ![X0,X1]: (~inverse(X0)=X1|~inverse(X1)=identity|~multiply(X0,sk_c10)=X1|~sQ3_spl|~sQ5_spl|~sQ6_spl|~sQ4_spl|~sQ19_spl)),
% 0.10/0.42 inference(forward_demodulation,[status(thm)],[f650,f205])).
% 0.10/0.42 fof(f1699,plain,(
% 0.10/0.42 ![X0,X1]: (~inverse(X0)=X1|~inverse(X1)=identity|~multiply(X0,identity)=X1|~sQ3_spl|~sQ5_spl|~sQ6_spl|~sQ4_spl|~sQ19_spl)),
% 0.10/0.42 inference(forward_demodulation,[status(thm)],[f650,f1698])).
% 0.10/0.42 fof(f1700,plain,(
% 0.10/0.42 ![X0,X1]: (~inverse(X0)=X1|~inverse(X1)=identity|~X0=X1|~sQ3_spl|~sQ5_spl|~sQ6_spl|~sQ4_spl|~sQ19_spl)),
% 0.10/0.42 inference(forward_demodulation,[status(thm)],[f1281,f1699])).
% 0.10/0.42 fof(f1701,plain,(
% 0.10/0.42 ![X0]: (~inverse(X0)=X0|~inverse(X0)=identity|~sQ3_spl|~sQ5_spl|~sQ6_spl|~sQ4_spl|~sQ19_spl)),
% 0.10/0.42 inference(destructive_equality_resolution,[status(thm)],[f1700])).
% 0.10/0.42 fof(f1702,plain,(
% 0.10/0.42 ~inverse(identity)=identity|~sQ19_spl|~sQ5_spl|~sQ6_spl|~sQ4_spl|~sQ3_spl),
% 0.10/0.42 inference(resolution,[status(thm)],[f1701,f623])).
% 0.10/0.42 fof(f1704,plain,(
% 0.10/0.42 ~identity=identity|~sQ19_spl|~sQ5_spl|~sQ6_spl|~sQ4_spl|~sQ3_spl),
% 0.10/0.42 inference(forward_demodulation,[status(thm)],[f623,f1702])).
% 0.10/0.42 fof(f1705,plain,(
% 0.10/0.42 $false|~sQ19_spl|~sQ5_spl|~sQ6_spl|~sQ4_spl|~sQ3_spl),
% 0.10/0.42 inference(trivial_equality_resolution,[status(thm)],[f1704])).
% 0.10/0.42 fof(f1706,plain,(
% 0.10/0.42 ~sQ19_spl|~sQ5_spl|~sQ6_spl|~sQ4_spl|~sQ3_spl),
% 0.10/0.42 inference(contradiction_clause,[status(thm)],[f1705])).
% 0.10/0.42 fof(f1707,plain,(
% 0.10/0.42 $false),
% 0.10/0.42 inference(sat_refutation,[status(thm)],[f108,f112,f116,f120,f124,f128,f132,f136,f144,f145,f146,f147,f148,f149,f150,f151,f156,f157,f158,f159,f160,f161,f168,f169,f170,f171,f172,f173,f174,f175,f180,f181,f182,f183,f184,f185,f186,f187,f207,f264,f268,f270,f279,f295,f298,f307,f326,f336,f344,f351,f352,f415,f494,f506,f638,f690,f715,f719,f731,f738,f767,f782,f798,f865,f869,f876,f880,f887,f916,f1071,f1187,f1297,f1318,f1382,f1396,f1407,f1420,f1421,f1422,f1433,f1486,f1544,f1599,f1600,f1609,f1635,f1640,f1706])).
% 0.10/0.42 % SZS output end CNFRefutation for theBenchmark.p
% 0.10/0.44 % Elapsed time: 0.059580 seconds
% 0.10/0.44 % CPU time: 0.294572 seconds
% 0.10/0.44 % Total memory used: 60.662 MB
% 0.10/0.44 % Net memory used: 60.422 MB
%------------------------------------------------------------------------------