%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : GRP220-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 : n018.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:17 PM UTC 2026
% Result : Unsatisfiable 0.02s 0.44s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP220-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.09/0.36 % Computer : n018.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Sun Sep 20 20:08:43 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.02/0.37 % Drodi V4.1.1
% 0.02/0.44 % Refutation found
% 0.02/0.44 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.02/0.44 % SZS output start CNFRefutation for theBenchmark
% 0.02/0.44 fof(f1,axiom,(
% 0.02/0.44 (![X]: (multiply(identity,X) = X ))),
% 0.02/0.44 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.02/0.44 fof(f2,axiom,(
% 0.02/0.44 (![X]: (multiply(inverse(X),X) = identity ))),
% 0.02/0.44 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.02/0.44 fof(f3,axiom,(
% 0.02/0.44 (![X,Y,Z]: (multiply(multiply(X,Y),Z) = multiply(X,multiply(Y,Z)) ))),
% 0.02/0.44 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.02/0.44 fof(f5,negated_conjecture,(
% 0.02/0.44 ( inverse(sk_c1) = sk_c12| inverse(sk_c6) = sk_c12 ) ),
% 0.02/0.44 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.02/0.44 fof(f6,negated_conjecture,(
% 0.02/0.44 ( inverse(sk_c1) = sk_c12| multiply(sk_c6,sk_c11) = sk_c12 ) ),
% 0.02/0.44 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.02/0.44 fof(f7,negated_conjecture,(
% 0.02/0.44 ( inverse(sk_c1) = sk_c12| multiply(sk_c7,sk_c10) = sk_c12 ) ),
% 0.02/0.44 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.02/0.44 fof(f8,negated_conjecture,(
% 0.02/0.44 ( inverse(sk_c1) = sk_c12| inverse(sk_c7) = sk_c10 ) ),
% 0.02/0.44 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.02/0.44 fof(f14,negated_conjecture,(
% 0.02/0.44 ( multiply(sk_c1,sk_c11) = sk_c12| inverse(sk_c6) = sk_c12 ) ),
% 0.02/0.44 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.02/0.44 fof(f15,negated_conjecture,(
% 0.02/0.44 ( multiply(sk_c1,sk_c11) = sk_c12| multiply(sk_c6,sk_c11) = sk_c12 ) ),
% 0.02/0.44 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.02/0.44 fof(f16,negated_conjecture,(
% 0.02/0.44 ( multiply(sk_c1,sk_c11) = sk_c12| multiply(sk_c7,sk_c10) = sk_c12 ) ),
% 0.02/0.44 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.02/0.44 fof(f17,negated_conjecture,(
% 0.02/0.44 ( multiply(sk_c1,sk_c11) = sk_c12| inverse(sk_c7) = sk_c10 ) ),
% 0.02/0.44 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.02/0.44 fof(f22,negated_conjecture,(
% 0.02/0.44 ( multiply(sk_c2,sk_c3) = sk_c11| inverse(sk_c12) = sk_c11 ) ),
% 0.02/0.44 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.02/0.44 fof(f23,negated_conjecture,(
% 0.02/0.44 ( multiply(sk_c2,sk_c3) = sk_c11| inverse(sk_c6) = sk_c12 ) ),
% 0.02/0.44 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.02/0.44 fof(f25,negated_conjecture,(
% 0.02/0.44 ( multiply(sk_c2,sk_c3) = sk_c11| multiply(sk_c7,sk_c10) = sk_c12 ) ),
% 0.02/0.44 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.02/0.44 fof(f26,negated_conjecture,(
% 0.02/0.44 ( multiply(sk_c2,sk_c3) = sk_c11| inverse(sk_c7) = sk_c10 ) ),
% 0.02/0.44 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.02/0.44 fof(f31,negated_conjecture,(
% 0.02/0.44 ( inverse(sk_c2) = sk_c3| inverse(sk_c12) = sk_c11 ) ),
% 0.02/0.44 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.02/0.44 fof(f32,negated_conjecture,(
% 0.02/0.44 ( inverse(sk_c2) = sk_c3| inverse(sk_c6) = sk_c12 ) ),
% 0.02/0.44 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.02/0.44 fof(f34,negated_conjecture,(
% 0.02/0.44 ( inverse(sk_c2) = sk_c3| multiply(sk_c7,sk_c10) = sk_c12 ) ),
% 0.02/0.44 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.02/0.44 fof(f35,negated_conjecture,(
% 0.02/0.44 ( inverse(sk_c2) = sk_c3| inverse(sk_c7) = sk_c10 ) ),
% 0.02/0.44 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.02/0.44 fof(f40,negated_conjecture,(
% 0.02/0.44 ( multiply(sk_c3,sk_c12) = sk_c11| inverse(sk_c12) = sk_c11 ) ),
% 0.02/0.44 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.02/0.44 fof(f41,negated_conjecture,(
% 0.02/0.44 ( multiply(sk_c3,sk_c12) = sk_c11| inverse(sk_c6) = sk_c12 ) ),
% 0.02/0.44 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.02/0.44 fof(f43,negated_conjecture,(
% 0.02/0.44 ( multiply(sk_c3,sk_c12) = sk_c11| multiply(sk_c7,sk_c10) = sk_c12 ) ),
% 0.02/0.44 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.02/0.44 fof(f44,negated_conjecture,(
% 0.02/0.44 ( multiply(sk_c3,sk_c12) = sk_c11| inverse(sk_c7) = sk_c10 ) ),
% 0.02/0.44 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.02/0.44 fof(f49,negated_conjecture,(
% 0.02/0.44 ( multiply(sk_c12,sk_c5) = sk_c11| inverse(sk_c12) = sk_c11 ) ),
% 0.02/0.44 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.02/0.44 fof(f50,negated_conjecture,(
% 0.02/0.44 ( multiply(sk_c12,sk_c5) = sk_c11| inverse(sk_c6) = sk_c12 ) ),
% 0.02/0.44 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.02/0.44 fof(f52,negated_conjecture,(
% 0.02/0.44 ( multiply(sk_c12,sk_c5) = sk_c11| multiply(sk_c7,sk_c10) = sk_c12 ) ),
% 0.02/0.44 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.02/0.44 fof(f53,negated_conjecture,(
% 0.02/0.44 ( multiply(sk_c12,sk_c5) = sk_c11| inverse(sk_c7) = sk_c10 ) ),
% 0.02/0.44 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.02/0.44 fof(f54,negated_conjecture,(
% 0.02/0.44 ( multiply(sk_c12,sk_c5) = sk_c11| multiply(sk_c10,sk_c11) = sk_c12 ) ),
% 0.02/0.44 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.02/0.44 fof(f56,negated_conjecture,(
% 0.02/0.44 ( multiply(sk_c12,sk_c5) = sk_c11| inverse(sk_c8) = sk_c10 ) ),
% 0.02/0.44 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.02/0.44 fof(f58,negated_conjecture,(
% 0.02/0.44 ( multiply(sk_c4,sk_c12) = sk_c5| inverse(sk_c12) = sk_c11 ) ),
% 0.02/0.44 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.02/0.44 fof(f59,negated_conjecture,(
% 0.02/0.44 ( multiply(sk_c4,sk_c12) = sk_c5| inverse(sk_c6) = sk_c12 ) ),
% 0.02/0.44 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.02/0.44 fof(f61,negated_conjecture,(
% 0.02/0.44 ( multiply(sk_c4,sk_c12) = sk_c5| multiply(sk_c7,sk_c10) = sk_c12 ) ),
% 0.02/0.44 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.02/0.44 fof(f62,negated_conjecture,(
% 0.02/0.44 ( multiply(sk_c4,sk_c12) = sk_c5| inverse(sk_c7) = sk_c10 ) ),
% 0.02/0.44 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.02/0.44 fof(f63,negated_conjecture,(
% 0.02/0.44 ( multiply(sk_c4,sk_c12) = sk_c5| multiply(sk_c10,sk_c11) = sk_c12 ) ),
% 0.02/0.44 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.02/0.44 fof(f65,negated_conjecture,(
% 0.02/0.44 ( multiply(sk_c4,sk_c12) = sk_c5| inverse(sk_c8) = sk_c10 ) ),
% 0.02/0.44 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.02/0.44 fof(f67,negated_conjecture,(
% 0.02/0.44 ( inverse(sk_c4) = sk_c12| inverse(sk_c12) = sk_c11 ) ),
% 0.02/0.44 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.02/0.44 fof(f68,negated_conjecture,(
% 0.02/0.44 ( inverse(sk_c4) = sk_c12| inverse(sk_c6) = sk_c12 ) ),
% 0.02/0.44 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.02/0.44 fof(f70,negated_conjecture,(
% 0.02/0.44 ( inverse(sk_c4) = sk_c12| multiply(sk_c7,sk_c10) = sk_c12 ) ),
% 0.02/0.44 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.02/0.44 fof(f71,negated_conjecture,(
% 0.02/0.44 ( inverse(sk_c4) = sk_c12| inverse(sk_c7) = sk_c10 ) ),
% 0.02/0.44 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.02/0.44 fof(f72,negated_conjecture,(
% 0.02/0.44 ( inverse(sk_c4) = sk_c12| multiply(sk_c10,sk_c11) = sk_c12 ) ),
% 0.02/0.44 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.02/0.44 fof(f74,negated_conjecture,(
% 0.02/0.44 ( inverse(sk_c4) = sk_c12| inverse(sk_c8) = sk_c10 ) ),
% 0.02/0.44 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.02/0.44 fof(f76,negated_conjecture,(
% 0.02/0.44 (![X6,X7,X8,X9,X10,X1,X3,X2,X4,X5]: (( inverse(X6) != sk_c12| multiply(X6,sk_c11) != sk_c12| multiply(X7,X8) != sk_c11| inverse(X7) != X8| multiply(X8,sk_c12) != sk_c11| multiply(sk_c12,X9) != sk_c11| multiply(X10,sk_c12) != X9| inverse(X10) != sk_c12| inverse(sk_c12) != sk_c11| inverse(X1) != sk_c12| multiply(X1,sk_c11) != sk_c12| multiply(X3,X2) != sk_c12| inverse(X3) != X2| multiply(X2,sk_c11) != sk_c12| inverse(X4) != X5| inverse(X5) != X2| multiply(X4,X2) != X5 ) ))),
% 0.02/0.44 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.02/0.44 fof(f77,plain,(
% 0.02/0.44 ![X0]: (multiply(identity,X0)=X0)),
% 0.02/0.44 inference(cnf_transformation,[status(thm)],[f1])).
% 0.02/0.44 fof(f78,plain,(
% 0.02/0.44 ![X0]: (multiply(inverse(X0),X0)=identity)),
% 0.02/0.44 inference(cnf_transformation,[status(thm)],[f2])).
% 0.02/0.44 fof(f79,plain,(
% 0.02/0.44 ![X0,X1,X2]: (multiply(multiply(X0,X1),X2)=multiply(X0,multiply(X1,X2)))),
% 0.02/0.44 inference(cnf_transformation,[status(thm)],[f3])).
% 0.02/0.44 fof(f81,plain,(
% 0.02/0.44 inverse(sk_c1)=sk_c12|inverse(sk_c6)=sk_c12),
% 0.02/0.44 inference(cnf_transformation,[status(thm)],[f5])).
% 0.02/0.44 fof(f82,plain,(
% 0.02/0.44 inverse(sk_c1)=sk_c12|multiply(sk_c6,sk_c11)=sk_c12),
% 0.02/0.44 inference(cnf_transformation,[status(thm)],[f6])).
% 0.02/0.44 fof(f83,plain,(
% 0.02/0.44 inverse(sk_c1)=sk_c12|multiply(sk_c7,sk_c10)=sk_c12),
% 0.02/0.44 inference(cnf_transformation,[status(thm)],[f7])).
% 0.02/0.44 fof(f84,plain,(
% 0.02/0.44 inverse(sk_c1)=sk_c12|inverse(sk_c7)=sk_c10),
% 0.02/0.44 inference(cnf_transformation,[status(thm)],[f8])).
% 0.02/0.44 fof(f90,plain,(
% 0.02/0.44 multiply(sk_c1,sk_c11)=sk_c12|inverse(sk_c6)=sk_c12),
% 0.02/0.44 inference(cnf_transformation,[status(thm)],[f14])).
% 0.02/0.44 fof(f91,plain,(
% 0.02/0.44 multiply(sk_c1,sk_c11)=sk_c12|multiply(sk_c6,sk_c11)=sk_c12),
% 0.02/0.44 inference(cnf_transformation,[status(thm)],[f15])).
% 0.02/0.45 fof(f92,plain,(
% 0.02/0.45 multiply(sk_c1,sk_c11)=sk_c12|multiply(sk_c7,sk_c10)=sk_c12),
% 0.02/0.45 inference(cnf_transformation,[status(thm)],[f16])).
% 0.02/0.45 fof(f93,plain,(
% 0.02/0.45 multiply(sk_c1,sk_c11)=sk_c12|inverse(sk_c7)=sk_c10),
% 0.02/0.45 inference(cnf_transformation,[status(thm)],[f17])).
% 0.02/0.45 fof(f98,plain,(
% 0.02/0.45 multiply(sk_c2,sk_c3)=sk_c11|inverse(sk_c12)=sk_c11),
% 0.02/0.45 inference(cnf_transformation,[status(thm)],[f22])).
% 0.02/0.45 fof(f99,plain,(
% 0.02/0.45 multiply(sk_c2,sk_c3)=sk_c11|inverse(sk_c6)=sk_c12),
% 0.02/0.45 inference(cnf_transformation,[status(thm)],[f23])).
% 0.02/0.45 fof(f101,plain,(
% 0.02/0.45 multiply(sk_c2,sk_c3)=sk_c11|multiply(sk_c7,sk_c10)=sk_c12),
% 0.02/0.45 inference(cnf_transformation,[status(thm)],[f25])).
% 0.02/0.45 fof(f102,plain,(
% 0.02/0.45 multiply(sk_c2,sk_c3)=sk_c11|inverse(sk_c7)=sk_c10),
% 0.02/0.45 inference(cnf_transformation,[status(thm)],[f26])).
% 0.02/0.45 fof(f107,plain,(
% 0.02/0.45 inverse(sk_c2)=sk_c3|inverse(sk_c12)=sk_c11),
% 0.02/0.45 inference(cnf_transformation,[status(thm)],[f31])).
% 0.02/0.45 fof(f108,plain,(
% 0.02/0.45 inverse(sk_c2)=sk_c3|inverse(sk_c6)=sk_c12),
% 0.02/0.45 inference(cnf_transformation,[status(thm)],[f32])).
% 0.02/0.45 fof(f110,plain,(
% 0.02/0.45 inverse(sk_c2)=sk_c3|multiply(sk_c7,sk_c10)=sk_c12),
% 0.02/0.45 inference(cnf_transformation,[status(thm)],[f34])).
% 0.02/0.45 fof(f111,plain,(
% 0.02/0.45 inverse(sk_c2)=sk_c3|inverse(sk_c7)=sk_c10),
% 0.02/0.45 inference(cnf_transformation,[status(thm)],[f35])).
% 0.02/0.45 fof(f116,plain,(
% 0.02/0.45 multiply(sk_c3,sk_c12)=sk_c11|inverse(sk_c12)=sk_c11),
% 0.02/0.45 inference(cnf_transformation,[status(thm)],[f40])).
% 0.02/0.45 fof(f117,plain,(
% 0.02/0.45 multiply(sk_c3,sk_c12)=sk_c11|inverse(sk_c6)=sk_c12),
% 0.02/0.45 inference(cnf_transformation,[status(thm)],[f41])).
% 0.02/0.45 fof(f119,plain,(
% 0.02/0.45 multiply(sk_c3,sk_c12)=sk_c11|multiply(sk_c7,sk_c10)=sk_c12),
% 0.02/0.45 inference(cnf_transformation,[status(thm)],[f43])).
% 0.02/0.45 fof(f120,plain,(
% 0.02/0.45 multiply(sk_c3,sk_c12)=sk_c11|inverse(sk_c7)=sk_c10),
% 0.02/0.45 inference(cnf_transformation,[status(thm)],[f44])).
% 0.02/0.45 fof(f125,plain,(
% 0.02/0.45 multiply(sk_c12,sk_c5)=sk_c11|inverse(sk_c12)=sk_c11),
% 0.02/0.45 inference(cnf_transformation,[status(thm)],[f49])).
% 0.02/0.45 fof(f126,plain,(
% 0.02/0.45 multiply(sk_c12,sk_c5)=sk_c11|inverse(sk_c6)=sk_c12),
% 0.02/0.45 inference(cnf_transformation,[status(thm)],[f50])).
% 0.02/0.45 fof(f128,plain,(
% 0.02/0.45 multiply(sk_c12,sk_c5)=sk_c11|multiply(sk_c7,sk_c10)=sk_c12),
% 0.02/0.45 inference(cnf_transformation,[status(thm)],[f52])).
% 0.02/0.45 fof(f129,plain,(
% 0.02/0.45 multiply(sk_c12,sk_c5)=sk_c11|inverse(sk_c7)=sk_c10),
% 0.02/0.45 inference(cnf_transformation,[status(thm)],[f53])).
% 0.02/0.45 fof(f130,plain,(
% 0.02/0.45 multiply(sk_c12,sk_c5)=sk_c11|multiply(sk_c10,sk_c11)=sk_c12),
% 0.02/0.45 inference(cnf_transformation,[status(thm)],[f54])).
% 0.02/0.45 fof(f132,plain,(
% 0.02/0.45 multiply(sk_c12,sk_c5)=sk_c11|inverse(sk_c8)=sk_c10),
% 0.02/0.45 inference(cnf_transformation,[status(thm)],[f56])).
% 0.02/0.45 fof(f134,plain,(
% 0.02/0.45 multiply(sk_c4,sk_c12)=sk_c5|inverse(sk_c12)=sk_c11),
% 0.02/0.45 inference(cnf_transformation,[status(thm)],[f58])).
% 0.02/0.45 fof(f135,plain,(
% 0.02/0.45 multiply(sk_c4,sk_c12)=sk_c5|inverse(sk_c6)=sk_c12),
% 0.02/0.45 inference(cnf_transformation,[status(thm)],[f59])).
% 0.02/0.45 fof(f137,plain,(
% 0.02/0.45 multiply(sk_c4,sk_c12)=sk_c5|multiply(sk_c7,sk_c10)=sk_c12),
% 0.02/0.45 inference(cnf_transformation,[status(thm)],[f61])).
% 0.02/0.45 fof(f138,plain,(
% 0.02/0.45 multiply(sk_c4,sk_c12)=sk_c5|inverse(sk_c7)=sk_c10),
% 0.02/0.45 inference(cnf_transformation,[status(thm)],[f62])).
% 0.02/0.45 fof(f139,plain,(
% 0.02/0.45 multiply(sk_c4,sk_c12)=sk_c5|multiply(sk_c10,sk_c11)=sk_c12),
% 0.02/0.45 inference(cnf_transformation,[status(thm)],[f63])).
% 0.02/0.45 fof(f141,plain,(
% 0.02/0.45 multiply(sk_c4,sk_c12)=sk_c5|inverse(sk_c8)=sk_c10),
% 0.02/0.45 inference(cnf_transformation,[status(thm)],[f65])).
% 0.02/0.45 fof(f143,plain,(
% 0.02/0.45 inverse(sk_c4)=sk_c12|inverse(sk_c12)=sk_c11),
% 0.02/0.45 inference(cnf_transformation,[status(thm)],[f67])).
% 0.02/0.45 fof(f144,plain,(
% 0.02/0.45 inverse(sk_c4)=sk_c12|inverse(sk_c6)=sk_c12),
% 0.02/0.45 inference(cnf_transformation,[status(thm)],[f68])).
% 0.02/0.45 fof(f146,plain,(
% 0.02/0.45 inverse(sk_c4)=sk_c12|multiply(sk_c7,sk_c10)=sk_c12),
% 0.02/0.45 inference(cnf_transformation,[status(thm)],[f70])).
% 0.02/0.45 fof(f147,plain,(
% 0.02/0.45 inverse(sk_c4)=sk_c12|inverse(sk_c7)=sk_c10),
% 0.02/0.45 inference(cnf_transformation,[status(thm)],[f71])).
% 0.02/0.45 fof(f148,plain,(
% 0.02/0.45 inverse(sk_c4)=sk_c12|multiply(sk_c10,sk_c11)=sk_c12),
% 0.02/0.45 inference(cnf_transformation,[status(thm)],[f72])).
% 0.02/0.45 fof(f150,plain,(
% 0.02/0.45 inverse(sk_c4)=sk_c12|inverse(sk_c8)=sk_c10),
% 0.02/0.45 inference(cnf_transformation,[status(thm)],[f74])).
% 0.02/0.45 fof(f152,plain,(
% 0.02/0.45 ![X2,X4,X5]: (((((![X3]: (((![X1]: ((((![X10]: ((![X9]: (((![X8]: ((![X7]: (((![X6]: (~inverse(X6)=sk_c12|~multiply(X6,sk_c11)=sk_c12))|~multiply(X7,X8)=sk_c11)|~inverse(X7)=X8))|~multiply(X8,sk_c12)=sk_c11))|~multiply(sk_c12,X9)=sk_c11)|~multiply(X10,sk_c12)=X9))|~inverse(X10)=sk_c12))|~inverse(sk_c12)=sk_c11)|~inverse(X1)=sk_c12)|~multiply(X1,sk_c11)=sk_c12))|~multiply(X3,X2)=sk_c12)|~inverse(X3)=X2))|~multiply(X2,sk_c11)=sk_c12)|~inverse(X4)=X5)|~inverse(X5)=X2)|~multiply(X4,X2)=X5)),
% 0.02/0.45 inference(miniscoping,[status(thm)],[f76])).
% 0.02/0.45 fof(f153,plain,(
% 0.02/0.45 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9]: (~inverse(X0)=sk_c12|~multiply(X0,sk_c11)=sk_c12|~multiply(X1,X2)=sk_c11|~inverse(X1)=X2|~multiply(X2,sk_c12)=sk_c11|~multiply(sk_c12,X3)=sk_c11|~multiply(X4,sk_c12)=X3|~inverse(X4)=sk_c12|~inverse(sk_c12)=sk_c11|~inverse(X5)=sk_c12|~multiply(X5,sk_c11)=sk_c12|~multiply(X6,X7)=sk_c12|~inverse(X6)=X7|~multiply(X7,sk_c11)=sk_c12|~inverse(X8)=X9|~inverse(X9)=X7|~multiply(X8,X7)=X9)),
% 0.02/0.45 inference(cnf_transformation,[status(thm)],[f152])).
% 0.02/0.45 fof(f154,definition,(
% 0.02/0.45 sQ0_spl <=> (inverse(sk_c1)=sk_c12)),
% 0.02/0.45 introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.02/0.45 fof(f155,plain,(
% 0.02/0.45 inverse(sk_c1)=sk_c12|~sQ0_spl),
% 0.02/0.45 inference(component_clause,[status(thm)],[f154])).
% 0.02/0.45 fof(f157,definition,(
% 0.02/0.45 sQ1_spl <=> (inverse(sk_c12)=sk_c11)),
% 0.02/0.45 introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.02/0.45 fof(f158,plain,(
% 0.02/0.45 inverse(sk_c12)=sk_c11|~sQ1_spl),
% 0.02/0.45 inference(component_clause,[status(thm)],[f157])).
% 0.02/0.45 fof(f159,plain,(
% 0.02/0.45 ~inverse(sk_c12)=sk_c11|sQ1_spl),
% 0.02/0.45 inference(component_clause,[status(thm)],[f157])).
% 0.02/0.45 fof(f161,definition,(
% 0.02/0.45 sQ2_spl <=> (inverse(sk_c6)=sk_c12)),
% 0.02/0.45 introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.02/0.45 fof(f162,plain,(
% 0.02/0.45 inverse(sk_c6)=sk_c12|~sQ2_spl),
% 0.02/0.45 inference(component_clause,[status(thm)],[f161])).
% 0.02/0.45 fof(f164,plain,(
% 0.02/0.45 sQ0_spl|sQ2_spl),
% 0.02/0.45 inference(split_clause,[status(thm)],[f81,f154,f161])).
% 0.02/0.45 fof(f165,definition,(
% 0.02/0.45 sQ3_spl <=> (multiply(sk_c6,sk_c11)=sk_c12)),
% 0.02/0.45 introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.02/0.45 fof(f166,plain,(
% 0.02/0.45 multiply(sk_c6,sk_c11)=sk_c12|~sQ3_spl),
% 0.02/0.45 inference(component_clause,[status(thm)],[f165])).
% 0.02/0.45 fof(f168,plain,(
% 0.02/0.45 sQ0_spl|sQ3_spl),
% 0.02/0.45 inference(split_clause,[status(thm)],[f82,f154,f165])).
% 0.02/0.45 fof(f169,definition,(
% 0.02/0.45 sQ4_spl <=> (multiply(sk_c7,sk_c10)=sk_c12)),
% 0.02/0.45 introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.02/0.45 fof(f170,plain,(
% 0.02/0.45 multiply(sk_c7,sk_c10)=sk_c12|~sQ4_spl),
% 0.02/0.45 inference(component_clause,[status(thm)],[f169])).
% 0.02/0.45 fof(f172,plain,(
% 0.02/0.45 sQ0_spl|sQ4_spl),
% 0.02/0.45 inference(split_clause,[status(thm)],[f83,f154,f169])).
% 0.02/0.45 fof(f173,definition,(
% 0.02/0.45 sQ5_spl <=> (inverse(sk_c7)=sk_c10)),
% 0.02/0.45 introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.02/0.45 fof(f174,plain,(
% 0.02/0.45 inverse(sk_c7)=sk_c10|~sQ5_spl),
% 0.02/0.45 inference(component_clause,[status(thm)],[f173])).
% 0.02/0.45 fof(f176,plain,(
% 0.02/0.45 sQ0_spl|sQ5_spl),
% 0.02/0.45 inference(split_clause,[status(thm)],[f84,f154,f173])).
% 0.02/0.45 fof(f177,definition,(
% 0.02/0.45 sQ6_spl <=> (multiply(sk_c10,sk_c11)=sk_c12)),
% 0.02/0.45 introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 0.02/0.45 fof(f178,plain,(
% 0.02/0.45 multiply(sk_c10,sk_c11)=sk_c12|~sQ6_spl),
% 0.02/0.45 inference(component_clause,[status(thm)],[f177])).
% 0.02/0.45 fof(f185,definition,(
% 0.02/0.45 sQ8_spl <=> (inverse(sk_c8)=sk_c10)),
% 0.02/0.45 introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 0.02/0.45 fof(f186,plain,(
% 0.02/0.45 inverse(sk_c8)=sk_c10|~sQ8_spl),
% 0.02/0.45 inference(component_clause,[status(thm)],[f185])).
% 0.02/0.45 fof(f193,definition,(
% 0.02/0.45 sQ10_spl <=> (multiply(sk_c1,sk_c11)=sk_c12)),
% 0.02/0.45 introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 0.02/0.45 fof(f194,plain,(
% 0.02/0.45 multiply(sk_c1,sk_c11)=sk_c12|~sQ10_spl),
% 0.02/0.45 inference(component_clause,[status(thm)],[f193])).
% 0.02/0.45 fof(f197,plain,(
% 0.02/0.45 sQ10_spl|sQ2_spl),
% 0.02/0.45 inference(split_clause,[status(thm)],[f90,f193,f161])).
% 0.02/0.45 fof(f198,plain,(
% 0.02/0.45 sQ10_spl|sQ3_spl),
% 0.02/0.45 inference(split_clause,[status(thm)],[f91,f193,f165])).
% 0.02/0.45 fof(f199,plain,(
% 0.02/0.45 sQ10_spl|sQ4_spl),
% 0.02/0.45 inference(split_clause,[status(thm)],[f92,f193,f169])).
% 0.02/0.45 fof(f200,plain,(
% 0.02/0.45 sQ10_spl|sQ5_spl),
% 0.02/0.45 inference(split_clause,[status(thm)],[f93,f193,f173])).
% 0.02/0.45 fof(f205,definition,(
% 0.02/0.45 sQ11_spl <=> (multiply(sk_c2,sk_c3)=sk_c11)),
% 0.02/0.45 introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 0.02/0.45 fof(f206,plain,(
% 0.02/0.45 multiply(sk_c2,sk_c3)=sk_c11|~sQ11_spl),
% 0.02/0.45 inference(component_clause,[status(thm)],[f205])).
% 0.02/0.45 fof(f208,plain,(
% 0.02/0.45 sQ11_spl|sQ1_spl),
% 0.02/0.45 inference(split_clause,[status(thm)],[f98,f205,f157])).
% 0.02/0.45 fof(f209,plain,(
% 0.02/0.45 sQ11_spl|sQ2_spl),
% 0.02/0.45 inference(split_clause,[status(thm)],[f99,f205,f161])).
% 0.02/0.45 fof(f211,plain,(
% 0.02/0.45 sQ11_spl|sQ4_spl),
% 0.02/0.45 inference(split_clause,[status(thm)],[f101,f205,f169])).
% 0.02/0.45 fof(f212,plain,(
% 0.02/0.45 sQ11_spl|sQ5_spl),
% 0.02/0.45 inference(split_clause,[status(thm)],[f102,f205,f173])).
% 0.02/0.45 fof(f217,definition,(
% 0.02/0.45 sQ12_spl <=> (inverse(sk_c2)=sk_c3)),
% 0.02/0.45 introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 0.02/0.45 fof(f218,plain,(
% 0.02/0.45 inverse(sk_c2)=sk_c3|~sQ12_spl),
% 0.02/0.45 inference(component_clause,[status(thm)],[f217])).
% 0.02/0.45 fof(f220,plain,(
% 0.02/0.45 sQ12_spl|sQ1_spl),
% 0.02/0.45 inference(split_clause,[status(thm)],[f107,f217,f157])).
% 0.02/0.45 fof(f221,plain,(
% 0.02/0.45 sQ12_spl|sQ2_spl),
% 0.02/0.45 inference(split_clause,[status(thm)],[f108,f217,f161])).
% 0.02/0.45 fof(f223,plain,(
% 0.02/0.45 sQ12_spl|sQ4_spl),
% 0.02/0.45 inference(split_clause,[status(thm)],[f110,f217,f169])).
% 0.02/0.45 fof(f224,plain,(
% 0.02/0.45 sQ12_spl|sQ5_spl),
% 0.02/0.45 inference(split_clause,[status(thm)],[f111,f217,f173])).
% 0.02/0.45 fof(f229,definition,(
% 0.02/0.45 sQ13_spl <=> (multiply(sk_c3,sk_c12)=sk_c11)),
% 0.02/0.45 introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 0.02/0.45 fof(f230,plain,(
% 0.02/0.45 multiply(sk_c3,sk_c12)=sk_c11|~sQ13_spl),
% 0.02/0.45 inference(component_clause,[status(thm)],[f229])).
% 0.02/0.45 fof(f232,plain,(
% 0.02/0.45 sQ13_spl|sQ1_spl),
% 0.02/0.45 inference(split_clause,[status(thm)],[f116,f229,f157])).
% 0.02/0.45 fof(f233,plain,(
% 0.02/0.45 sQ13_spl|sQ2_spl),
% 0.02/0.45 inference(split_clause,[status(thm)],[f117,f229,f161])).
% 0.02/0.45 fof(f235,plain,(
% 0.02/0.45 sQ13_spl|sQ4_spl),
% 0.02/0.45 inference(split_clause,[status(thm)],[f119,f229,f169])).
% 0.02/0.45 fof(f236,plain,(
% 0.02/0.45 sQ13_spl|sQ5_spl),
% 0.02/0.45 inference(split_clause,[status(thm)],[f120,f229,f173])).
% 0.02/0.45 fof(f241,definition,(
% 0.02/0.45 sQ14_spl <=> (multiply(sk_c12,sk_c5)=sk_c11)),
% 0.02/0.45 introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 0.02/0.45 fof(f242,plain,(
% 0.02/0.45 multiply(sk_c12,sk_c5)=sk_c11|~sQ14_spl),
% 0.02/0.45 inference(component_clause,[status(thm)],[f241])).
% 0.02/0.45 fof(f244,plain,(
% 0.02/0.45 sQ14_spl|sQ1_spl),
% 0.02/0.45 inference(split_clause,[status(thm)],[f125,f241,f157])).
% 0.02/0.45 fof(f245,plain,(
% 0.02/0.45 sQ14_spl|sQ2_spl),
% 0.02/0.45 inference(split_clause,[status(thm)],[f126,f241,f161])).
% 0.02/0.45 fof(f247,plain,(
% 0.02/0.45 sQ14_spl|sQ4_spl),
% 0.02/0.45 inference(split_clause,[status(thm)],[f128,f241,f169])).
% 0.02/0.45 fof(f248,plain,(
% 0.02/0.45 sQ14_spl|sQ5_spl),
% 0.02/0.45 inference(split_clause,[status(thm)],[f129,f241,f173])).
% 0.02/0.45 fof(f249,plain,(
% 0.02/0.45 sQ14_spl|sQ6_spl),
% 0.02/0.45 inference(split_clause,[status(thm)],[f130,f241,f177])).
% 0.02/0.45 fof(f251,plain,(
% 0.02/0.45 sQ14_spl|sQ8_spl),
% 0.02/0.45 inference(split_clause,[status(thm)],[f132,f241,f185])).
% 0.02/0.45 fof(f253,definition,(
% 0.02/0.45 sQ15_spl <=> (multiply(sk_c4,sk_c12)=sk_c5)),
% 0.02/0.45 introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 0.02/0.45 fof(f254,plain,(
% 0.02/0.45 multiply(sk_c4,sk_c12)=sk_c5|~sQ15_spl),
% 0.02/0.45 inference(component_clause,[status(thm)],[f253])).
% 0.02/0.45 fof(f256,plain,(
% 0.02/0.45 sQ15_spl|sQ1_spl),
% 0.02/0.45 inference(split_clause,[status(thm)],[f134,f253,f157])).
% 0.02/0.45 fof(f257,plain,(
% 0.02/0.45 sQ15_spl|sQ2_spl),
% 0.02/0.45 inference(split_clause,[status(thm)],[f135,f253,f161])).
% 0.02/0.45 fof(f259,plain,(
% 0.02/0.45 sQ15_spl|sQ4_spl),
% 0.02/0.45 inference(split_clause,[status(thm)],[f137,f253,f169])).
% 0.02/0.45 fof(f260,plain,(
% 0.02/0.45 sQ15_spl|sQ5_spl),
% 0.02/0.45 inference(split_clause,[status(thm)],[f138,f253,f173])).
% 0.02/0.45 fof(f261,plain,(
% 0.02/0.45 sQ15_spl|sQ6_spl),
% 0.02/0.45 inference(split_clause,[status(thm)],[f139,f253,f177])).
% 0.02/0.45 fof(f263,plain,(
% 0.02/0.45 sQ15_spl|sQ8_spl),
% 0.02/0.45 inference(split_clause,[status(thm)],[f141,f253,f185])).
% 0.02/0.45 fof(f265,definition,(
% 0.02/0.45 sQ16_spl <=> (inverse(sk_c4)=sk_c12)),
% 0.02/0.45 introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 0.02/0.45 fof(f266,plain,(
% 0.02/0.45 inverse(sk_c4)=sk_c12|~sQ16_spl),
% 0.02/0.45 inference(component_clause,[status(thm)],[f265])).
% 0.02/0.45 fof(f268,plain,(
% 0.02/0.45 sQ16_spl|sQ1_spl),
% 0.02/0.45 inference(split_clause,[status(thm)],[f143,f265,f157])).
% 0.02/0.45 fof(f269,plain,(
% 0.02/0.45 sQ16_spl|sQ2_spl),
% 0.02/0.45 inference(split_clause,[status(thm)],[f144,f265,f161])).
% 0.02/0.45 fof(f271,plain,(
% 0.02/0.45 sQ16_spl|sQ4_spl),
% 0.02/0.45 inference(split_clause,[status(thm)],[f146,f265,f169])).
% 0.02/0.45 fof(f272,plain,(
% 0.02/0.45 sQ16_spl|sQ5_spl),
% 0.02/0.45 inference(split_clause,[status(thm)],[f147,f265,f173])).
% 0.02/0.45 fof(f273,plain,(
% 0.02/0.45 sQ16_spl|sQ6_spl),
% 0.02/0.45 inference(split_clause,[status(thm)],[f148,f265,f177])).
% 0.02/0.45 fof(f275,plain,(
% 0.02/0.45 sQ16_spl|sQ8_spl),
% 0.02/0.45 inference(split_clause,[status(thm)],[f150,f265,f185])).
% 0.02/0.45 fof(f277,definition,(
% 0.02/0.45 ![X0]: (sQ17_spl <=> (~inverse(X0)=sk_c12|~multiply(X0,sk_c11)=sk_c12))),
% 0.02/0.45 introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 0.02/0.45 fof(f278,plain,(
% 0.02/0.45 ![X0]: (~inverse(X0)=sk_c12|~multiply(X0,sk_c11)=sk_c12|~sQ17_spl)),
% 0.02/0.45 inference(component_clause,[status(thm)],[f277])).
% 0.02/0.45 fof(f280,definition,(
% 0.02/0.45 ![X1,X2]: (sQ18_spl <=> (~multiply(X1,X2)=sk_c11|~inverse(X1)=X2|~multiply(X2,sk_c12)=sk_c11))),
% 0.02/0.45 introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 0.02/0.45 fof(f281,plain,(
% 0.02/0.45 ![X0,X1]: (~multiply(X0,X1)=sk_c11|~inverse(X0)=X1|~multiply(X1,sk_c12)=sk_c11|~sQ18_spl)),
% 0.02/0.45 inference(component_clause,[status(thm)],[f280])).
% 0.02/0.45 fof(f283,definition,(
% 0.02/0.45 ![X3,X4]: (sQ19_spl <=> (~multiply(sk_c12,X3)=sk_c11|~multiply(X4,sk_c12)=X3|~inverse(X4)=sk_c12))),
% 0.02/0.45 introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 0.02/0.45 fof(f284,plain,(
% 0.02/0.45 ![X0,X1]: (~multiply(sk_c12,X0)=sk_c11|~multiply(X1,sk_c12)=X0|~inverse(X1)=sk_c12|~sQ19_spl)),
% 0.02/0.45 inference(component_clause,[status(thm)],[f283])).
% 0.02/0.45 fof(f286,definition,(
% 0.02/0.45 ![X6,X7,X8,X9]: (sQ20_spl <=> (~multiply(X6,X7)=sk_c12|~inverse(X6)=X7|~multiply(X7,sk_c11)=sk_c12|~inverse(X8)=X9|~inverse(X9)=X7|~multiply(X8,X7)=X9))),
% 0.02/0.45 introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 0.02/0.45 fof(f287,plain,(
% 0.02/0.45 ![X0,X1,X2,X3]: (~multiply(X0,X1)=sk_c12|~inverse(X0)=X1|~multiply(X1,sk_c11)=sk_c12|~inverse(X2)=X3|~inverse(X3)=X1|~multiply(X2,X1)=X3|~sQ20_spl)),
% 0.02/0.45 inference(component_clause,[status(thm)],[f286])).
% 0.02/0.45 fof(f289,plain,(
% 0.02/0.45 sQ17_spl|sQ18_spl|sQ19_spl|~sQ1_spl|sQ20_spl),
% 0.02/0.45 inference(split_clause,[status(thm)],[f153,f277,f280,f283,f157,f286])).
% 0.02/0.45 fof(f290,plain,(
% 0.02/0.45 ![X0,X1]: (~multiply(X0,inverse(X0))=sk_c12|~multiply(inverse(X0),sk_c11)=sk_c12|~inverse(inverse(X1))=inverse(X0)|~multiply(X1,inverse(X0))=inverse(X1)|~sQ20_spl)),
% 0.02/0.45 inference(destructive_equality_resolution,[status(thm)],[f287])).
% 0.02/0.45 fof(f305,plain,(
% 0.02/0.45 ![X0]: (~multiply(sk_c7,inverse(sk_c7))=sk_c12|~multiply(inverse(sk_c7),sk_c11)=sk_c12|~inverse(inverse(X0))=inverse(sk_c7)|~multiply(X0,sk_c10)=inverse(X0)|~sQ20_spl|~sQ5_spl)),
% 0.02/0.45 inference(paramodulation,[status(thm)],[f174,f290])).
% 0.02/0.45 fof(f307,plain,(
% 0.02/0.45 ![X0]: (~multiply(sk_c8,inverse(sk_c8))=sk_c12|~multiply(inverse(sk_c8),sk_c11)=sk_c12|~inverse(inverse(X0))=inverse(sk_c8)|~multiply(X0,sk_c10)=inverse(X0)|~sQ20_spl|~sQ8_spl)),
% 0.02/0.45 inference(paramodulation,[status(thm)],[f186,f290])).
% 0.02/0.45 fof(f321,definition,(
% 0.02/0.45 sQ24_spl <=> (multiply(sk_c7,inverse(sk_c7))=sk_c12)),
% 0.02/0.45 introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition])).
% 0.02/0.45 fof(f323,plain,(
% 0.02/0.45 ~multiply(sk_c7,inverse(sk_c7))=sk_c12|sQ24_spl),
% 0.02/0.45 inference(component_clause,[status(thm)],[f321])).
% 0.02/0.45 fof(f324,definition,(
% 0.02/0.45 sQ25_spl <=> (multiply(inverse(sk_c7),sk_c11)=sk_c12)),
% 0.02/0.45 introduced(definition,[new_symbols(definition,[sQ25_spl])],[split_symbol_definition])).
% 0.02/0.45 fof(f326,plain,(
% 0.02/0.45 ~multiply(inverse(sk_c7),sk_c11)=sk_c12|sQ25_spl),
% 0.02/0.45 inference(component_clause,[status(thm)],[f324])).
% 0.02/0.45 fof(f327,definition,(
% 0.02/0.45 ![X0]: (sQ26_spl <=> (~inverse(inverse(X0))=inverse(sk_c7)|~multiply(X0,sk_c10)=inverse(X0)))),
% 0.02/0.45 introduced(definition,[new_symbols(definition,[sQ26_spl])],[split_symbol_definition])).
% 0.02/0.45 fof(f330,plain,(
% 0.02/0.45 ~sQ24_spl|~sQ25_spl|sQ26_spl|~sQ20_spl|~sQ5_spl),
% 0.02/0.45 inference(split_clause,[status(thm)],[f305,f321,f324,f327,f286,f173])).
% 0.02/0.45 fof(f341,definition,(
% 0.02/0.45 sQ30_spl <=> (multiply(sk_c8,inverse(sk_c8))=sk_c12)),
% 0.02/0.45 introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition])).
% 0.02/0.45 fof(f344,definition,(
% 0.02/0.45 sQ31_spl <=> (multiply(inverse(sk_c8),sk_c11)=sk_c12)),
% 0.02/0.45 introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition])).
% 0.02/0.45 fof(f346,plain,(
% 0.02/0.45 ~multiply(inverse(sk_c8),sk_c11)=sk_c12|sQ31_spl),
% 0.02/0.45 inference(component_clause,[status(thm)],[f344])).
% 0.02/0.45 fof(f347,definition,(
% 0.02/0.45 ![X0]: (sQ32_spl <=> (~inverse(inverse(X0))=inverse(sk_c8)|~multiply(X0,sk_c10)=inverse(X0)))),
% 0.02/0.45 introduced(definition,[new_symbols(definition,[sQ32_spl])],[split_symbol_definition])).
% 0.02/0.45 fof(f350,plain,(
% 0.02/0.45 ~sQ30_spl|~sQ31_spl|sQ32_spl|~sQ20_spl|~sQ8_spl),
% 0.02/0.45 inference(split_clause,[status(thm)],[f307,f341,f344,f347,f286,f185])).
% 0.02/0.45 fof(f392,plain,(
% 0.02/0.45 ![X0]: (~multiply(sk_c12,multiply(X0,sk_c12))=sk_c11|~inverse(X0)=sk_c12|~sQ19_spl)),
% 0.02/0.45 inference(destructive_equality_resolution,[status(thm)],[f284])).
% 0.02/0.45 fof(f394,plain,(
% 0.02/0.45 multiply(sk_c12,sk_c1)=identity|~sQ0_spl),
% 0.02/0.45 inference(paramodulation,[status(thm)],[f155,f78])).
% 0.02/0.45 fof(f397,plain,(
% 0.02/0.45 ![X0,X1]: (multiply(identity,X0)=multiply(inverse(X1),multiply(X1,X0)))),
% 0.02/0.45 inference(paramodulation,[status(thm)],[f78,f79])).
% 0.02/0.45 fof(f398,plain,(
% 0.02/0.45 ![X0,X1]: (X0=multiply(inverse(X1),multiply(X1,X0)))),
% 0.02/0.45 inference(forward_demodulation,[status(thm)],[f77,f397])).
% 0.02/0.45 fof(f399,plain,(
% 0.02/0.45 ![X0]: (multiply(identity,X0)=multiply(sk_c12,multiply(sk_c1,X0))|~sQ0_spl)),
% 0.02/0.45 inference(paramodulation,[status(thm)],[f394,f79])).
% 0.02/0.45 fof(f400,plain,(
% 0.02/0.45 ![X0]: (X0=multiply(sk_c12,multiply(sk_c1,X0))|~sQ0_spl)),
% 0.02/0.45 inference(forward_demodulation,[status(thm)],[f77,f399])).
% 0.02/0.45 fof(f405,plain,(
% 0.02/0.45 ~multiply(sk_c12,identity)=sk_c11|~inverse(inverse(sk_c12))=sk_c12|~sQ19_spl),
% 0.02/0.45 inference(paramodulation,[status(thm)],[f78,f392])).
% 0.02/0.45 fof(f406,plain,(
% 0.02/0.45 ~multiply(sk_c12,sk_c12)=sk_c11|~inverse(identity)=sk_c12|~sQ19_spl),
% 0.02/0.45 inference(paramodulation,[status(thm)],[f77,f392])).
% 0.02/0.45 fof(f409,plain,(
% 0.02/0.45 ~multiply(sk_c12,sk_c5)=sk_c11|~inverse(sk_c4)=sk_c12|~sQ19_spl|~sQ15_spl),
% 0.02/0.45 inference(paramodulation,[status(thm)],[f254,f392])).
% 0.02/0.45 fof(f410,definition,(
% 0.02/0.45 sQ42_spl <=> (multiply(sk_c12,identity)=sk_c11)),
% 0.02/0.45 introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition])).
% 0.02/0.45 fof(f412,plain,(
% 0.02/0.45 ~multiply(sk_c12,identity)=sk_c11|sQ42_spl),
% 0.02/0.45 inference(component_clause,[status(thm)],[f410])).
% 0.02/0.45 fof(f413,definition,(
% 0.02/0.45 sQ43_spl <=> (inverse(inverse(sk_c12))=sk_c12)),
% 0.02/0.45 introduced(definition,[new_symbols(definition,[sQ43_spl])],[split_symbol_definition])).
% 0.02/0.45 fof(f416,plain,(
% 0.02/0.45 ~sQ42_spl|~sQ43_spl|~sQ19_spl),
% 0.02/0.45 inference(split_clause,[status(thm)],[f405,f410,f413,f283])).
% 0.02/0.45 fof(f417,definition,(
% 0.02/0.45 sQ44_spl <=> (multiply(sk_c12,sk_c12)=sk_c11)),
% 0.02/0.45 introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition])).
% 0.02/0.45 fof(f418,plain,(
% 0.02/0.45 multiply(sk_c12,sk_c12)=sk_c11|~sQ44_spl),
% 0.02/0.45 inference(component_clause,[status(thm)],[f417])).
% 0.02/0.45 fof(f419,plain,(
% 0.02/0.45 ~multiply(sk_c12,sk_c12)=sk_c11|sQ44_spl),
% 0.02/0.45 inference(component_clause,[status(thm)],[f417])).
% 0.02/0.45 fof(f420,definition,(
% 0.02/0.45 sQ45_spl <=> (inverse(identity)=sk_c12)),
% 0.02/0.45 introduced(definition,[new_symbols(definition,[sQ45_spl])],[split_symbol_definition])).
% 0.02/0.45 fof(f421,plain,(
% 0.02/0.45 inverse(identity)=sk_c12|~sQ45_spl),
% 0.02/0.45 inference(component_clause,[status(thm)],[f420])).
% 0.02/0.45 fof(f422,plain,(
% 0.02/0.45 ~inverse(identity)=sk_c12|sQ45_spl),
% 0.02/0.45 inference(component_clause,[status(thm)],[f420])).
% 0.02/0.45 fof(f423,plain,(
% 0.02/0.45 ~sQ44_spl|~sQ45_spl|~sQ19_spl),
% 0.02/0.45 inference(split_clause,[status(thm)],[f406,f417,f420,f283])).
% 0.02/0.45 fof(f431,plain,(
% 0.02/0.45 ~sQ14_spl|~sQ16_spl|~sQ19_spl|~sQ15_spl),
% 0.02/0.45 inference(split_clause,[status(thm)],[f409,f241,f265,f283,f253])).
% 0.02/0.45 fof(f432,plain,(
% 0.02/0.45 ![X0]: (~multiply(X0,inverse(X0))=sk_c11|~multiply(inverse(X0),sk_c12)=sk_c11|~sQ18_spl)),
% 0.02/0.45 inference(destructive_equality_resolution,[status(thm)],[f281])).
% 0.02/0.45 fof(f433,plain,(
% 0.02/0.45 ~multiply(sk_c12,inverse(sk_c12))=sk_c11|~identity=sk_c11|~sQ18_spl),
% 0.02/0.45 inference(paramodulation,[status(thm)],[f78,f432])).
% 0.02/0.45 fof(f435,definition,(
% 0.02/0.45 sQ48_spl <=> (multiply(sk_c12,inverse(sk_c12))=sk_c11)),
% 0.02/0.45 introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition])).
% 0.02/0.45 fof(f437,plain,(
% 0.02/0.45 ~multiply(sk_c12,inverse(sk_c12))=sk_c11|sQ48_spl),
% 0.02/0.45 inference(component_clause,[status(thm)],[f435])).
% 0.02/0.45 fof(f438,definition,(
% 0.02/0.45 sQ49_spl <=> (identity=sk_c11)),
% 0.02/0.45 introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition])).
% 0.02/0.45 fof(f439,plain,(
% 0.02/0.45 identity=sk_c11|~sQ49_spl),
% 0.02/0.45 inference(component_clause,[status(thm)],[f438])).
% 0.02/0.45 fof(f440,plain,(
% 0.02/0.45 ~identity=sk_c11|sQ49_spl),
% 0.02/0.45 inference(component_clause,[status(thm)],[f438])).
% 0.02/0.45 fof(f441,plain,(
% 0.02/0.45 ~sQ48_spl|~sQ49_spl|~sQ18_spl),
% 0.02/0.45 inference(split_clause,[status(thm)],[f433,f435,f438,f280])).
% 0.02/0.45 fof(f446,plain,(
% 0.02/0.45 multiply(sk_c11,sk_c12)=identity|~sQ1_spl),
% 0.02/0.45 inference(paramodulation,[status(thm)],[f158,f78])).
% 0.02/0.45 fof(f447,plain,(
% 0.02/0.45 multiply(sk_c12,sk_c6)=identity|~sQ2_spl),
% 0.02/0.45 inference(paramodulation,[status(thm)],[f162,f78])).
% 0.02/0.45 fof(f453,plain,(
% 0.02/0.45 ~multiply(sk_c10,sk_c11)=sk_c12|~sQ8_spl|sQ31_spl),
% 0.02/0.45 inference(backward_demodulation,[status(thm)],[f186,f346])).
% 0.02/0.45 fof(f455,plain,(
% 0.02/0.45 ~sk_c12=sk_c12|~sQ6_spl|~sQ8_spl|sQ31_spl),
% 0.02/0.45 inference(forward_demodulation,[status(thm)],[f178,f453])).
% 0.02/0.45 fof(f456,plain,(
% 0.02/0.45 $false|~sQ6_spl|~sQ8_spl|sQ31_spl),
% 0.02/0.45 inference(trivial_equality_resolution,[status(thm)],[f455])).
% 0.02/0.45 fof(f457,plain,(
% 0.02/0.45 ~sQ6_spl|~sQ8_spl|sQ31_spl),
% 0.02/0.45 inference(contradiction_clause,[status(thm)],[f456])).
% 0.02/0.45 fof(f463,plain,(
% 0.02/0.45 ~inverse(sk_c6)=sk_c12|~sQ17_spl|~sQ3_spl),
% 0.02/0.45 inference(resolution,[status(thm)],[f278,f166])).
% 0.02/0.45 fof(f465,plain,(
% 0.02/0.45 ~inverse(sk_c1)=sk_c12|~sQ17_spl|~sQ10_spl),
% 0.02/0.45 inference(resolution,[status(thm)],[f278,f194])).
% 0.02/0.45 fof(f472,plain,(
% 0.02/0.45 ~sk_c12=sk_c12|~sQ2_spl|~sQ17_spl|~sQ3_spl),
% 0.02/0.45 inference(forward_demodulation,[status(thm)],[f162,f463])).
% 0.02/0.45 fof(f473,plain,(
% 0.02/0.45 $false|~sQ2_spl|~sQ17_spl|~sQ3_spl),
% 0.02/0.45 inference(trivial_equality_resolution,[status(thm)],[f472])).
% 0.02/0.45 fof(f474,plain,(
% 0.02/0.45 ~sQ2_spl|~sQ17_spl|~sQ3_spl),
% 0.02/0.45 inference(contradiction_clause,[status(thm)],[f473])).
% 0.02/0.45 fof(f490,plain,(
% 0.02/0.45 ~multiply(sk_c12,identity)=sk_c11|~inverse(sk_c11)=sk_c12|~sQ19_spl|~sQ1_spl),
% 0.02/0.45 inference(paramodulation,[status(thm)],[f446,f392])).
% 0.02/0.45 fof(f496,definition,(
% 0.02/0.45 sQ51_spl <=> (inverse(sk_c11)=sk_c12)),
% 0.02/0.45 introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition])).
% 0.02/0.45 fof(f499,plain,(
% 0.02/0.45 ~sQ42_spl|~sQ51_spl|~sQ19_spl|~sQ1_spl),
% 0.02/0.45 inference(split_clause,[status(thm)],[f490,f410,f496,f283,f157])).
% 0.02/0.45 fof(f514,plain,(
% 0.02/0.45 ~multiply(sk_c10,sk_c11)=sk_c12|~sQ5_spl|sQ25_spl),
% 0.02/0.45 inference(forward_demodulation,[status(thm)],[f174,f326])).
% 0.02/0.45 fof(f515,plain,(
% 0.02/0.45 ~sk_c12=sk_c12|~sQ6_spl|~sQ5_spl|sQ25_spl),
% 0.02/0.45 inference(forward_demodulation,[status(thm)],[f178,f514])).
% 0.02/0.45 fof(f516,plain,(
% 0.02/0.45 $false|~sQ6_spl|~sQ5_spl|sQ25_spl),
% 0.02/0.45 inference(trivial_equality_resolution,[status(thm)],[f515])).
% 0.02/0.45 fof(f517,plain,(
% 0.02/0.45 ~sQ6_spl|~sQ5_spl|sQ25_spl),
% 0.02/0.45 inference(contradiction_clause,[status(thm)],[f516])).
% 0.02/0.45 fof(f519,plain,(
% 0.02/0.45 ~multiply(sk_c7,sk_c10)=sk_c12|~sQ5_spl|sQ24_spl),
% 0.02/0.45 inference(forward_demodulation,[status(thm)],[f174,f323])).
% 0.02/0.45 fof(f520,plain,(
% 0.02/0.45 ~sk_c12=sk_c12|~sQ4_spl|~sQ5_spl|sQ24_spl),
% 0.02/0.45 inference(forward_demodulation,[status(thm)],[f170,f519])).
% 0.02/0.45 fof(f521,plain,(
% 0.02/0.45 $false|~sQ4_spl|~sQ5_spl|sQ24_spl),
% 0.02/0.45 inference(trivial_equality_resolution,[status(thm)],[f520])).
% 0.02/0.45 fof(f522,plain,(
% 0.02/0.45 ~sQ4_spl|~sQ5_spl|sQ24_spl),
% 0.02/0.45 inference(contradiction_clause,[status(thm)],[f521])).
% 0.02/0.45 fof(f524,plain,(
% 0.02/0.45 sk_c11=multiply(sk_c12,sk_c12)|~sQ0_spl|~sQ10_spl),
% 0.02/0.45 inference(paramodulation,[status(thm)],[f194,f400])).
% 0.02/0.45 fof(f525,plain,(
% 0.02/0.45 ~sk_c12=sk_c11|~inverse(sk_c1)=sk_c12|~sQ19_spl|~sQ0_spl),
% 0.02/0.45 inference(paramodulation,[status(thm)],[f400,f392])).
% 0.02/0.45 fof(f527,plain,(
% 0.02/0.45 $false|sQ44_spl|~sQ0_spl|~sQ10_spl),
% 0.02/0.45 inference(forward_subsumption_resolution,[status(thm)],[f524,f419])).
% 0.02/0.45 fof(f528,plain,(
% 0.02/0.45 sQ44_spl|~sQ0_spl|~sQ10_spl),
% 0.02/0.45 inference(contradiction_clause,[status(thm)],[f527])).
% 0.02/0.45 fof(f529,definition,(
% 0.02/0.45 sQ52_spl <=> (sk_c12=sk_c11)),
% 0.02/0.45 introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition])).
% 0.02/0.45 fof(f530,plain,(
% 0.02/0.45 sk_c12=sk_c11|~sQ52_spl),
% 0.02/0.45 inference(component_clause,[status(thm)],[f529])).
% 0.02/0.45 fof(f531,plain,(
% 0.02/0.45 ~sk_c12=sk_c11|sQ52_spl),
% 0.02/0.45 inference(component_clause,[status(thm)],[f529])).
% 0.02/0.45 fof(f532,plain,(
% 0.02/0.45 ~sQ52_spl|~sQ0_spl|~sQ19_spl),
% 0.02/0.45 inference(split_clause,[status(thm)],[f525,f529,f154,f283])).
% 0.02/0.45 fof(f534,plain,(
% 0.02/0.45 ~multiply(sk_c12,sk_c11)=sk_c11|~sQ1_spl|sQ48_spl),
% 0.02/0.45 inference(forward_demodulation,[status(thm)],[f158,f437])).
% 0.02/0.45 fof(f565,plain,(
% 0.02/0.45 sk_c1=multiply(inverse(sk_c12),identity)|~sQ0_spl),
% 0.02/0.45 inference(paramodulation,[status(thm)],[f394,f398])).
% 0.02/0.45 fof(f566,plain,(
% 0.02/0.45 sk_c6=multiply(inverse(sk_c12),identity)|~sQ2_spl),
% 0.02/0.45 inference(paramodulation,[status(thm)],[f447,f398])).
% 0.02/0.45 fof(f570,plain,(
% 0.02/0.45 ![X0]: (X0=multiply(inverse(identity),X0))),
% 0.02/0.45 inference(paramodulation,[status(thm)],[f77,f398])).
% 0.02/0.45 fof(f573,plain,(
% 0.02/0.45 sk_c11=multiply(inverse(sk_c6),sk_c12)|~sQ3_spl),
% 0.02/0.45 inference(paramodulation,[status(thm)],[f166,f398])).
% 0.02/0.45 fof(f575,plain,(
% 0.02/0.45 sk_c10=multiply(inverse(sk_c7),sk_c12)|~sQ4_spl),
% 0.02/0.45 inference(paramodulation,[status(thm)],[f170,f398])).
% 0.02/0.45 fof(f581,plain,(
% 0.02/0.45 sk_c3=multiply(inverse(sk_c2),sk_c11)|~sQ11_spl),
% 0.02/0.45 inference(paramodulation,[status(thm)],[f206,f398])).
% 0.02/0.45 fof(f585,plain,(
% 0.02/0.45 sk_c1=multiply(sk_c11,identity)|~sQ1_spl|~sQ0_spl),
% 0.02/0.45 inference(forward_demodulation,[status(thm)],[f158,f565])).
% 0.02/0.45 fof(f586,plain,(
% 0.02/0.45 sk_c6=multiply(sk_c11,identity)|~sQ1_spl|~sQ2_spl),
% 0.02/0.45 inference(forward_demodulation,[status(thm)],[f158,f566])).
% 0.02/0.45 fof(f589,plain,(
% 0.02/0.45 sk_c11=multiply(sk_c12,sk_c12)|~sQ2_spl|~sQ3_spl),
% 0.02/0.45 inference(forward_demodulation,[status(thm)],[f162,f573])).
% 0.02/0.45 fof(f590,plain,(
% 0.02/0.45 $false|sQ44_spl|~sQ2_spl|~sQ3_spl),
% 0.02/0.45 inference(forward_subsumption_resolution,[status(thm)],[f589,f419])).
% 0.02/0.45 fof(f591,plain,(
% 0.02/0.45 sQ44_spl|~sQ2_spl|~sQ3_spl),
% 0.02/0.45 inference(contradiction_clause,[status(thm)],[f590])).
% 0.02/0.45 fof(f593,plain,(
% 0.02/0.45 sk_c10=multiply(sk_c10,sk_c12)|~sQ5_spl|~sQ4_spl),
% 0.02/0.45 inference(forward_demodulation,[status(thm)],[f174,f575])).
% 0.02/0.45 fof(f595,plain,(
% 0.02/0.45 sk_c3=multiply(sk_c3,sk_c11)|~sQ12_spl|~sQ11_spl),
% 0.02/0.45 inference(forward_demodulation,[status(thm)],[f218,f581])).
% 0.02/0.45 fof(f606,plain,(
% 0.02/0.45 sk_c1=sk_c6|~sQ2_spl|~sQ1_spl|~sQ0_spl),
% 0.02/0.45 inference(backward_demodulation,[status(thm)],[f586,f585])).
% 0.02/0.45 fof(f625,plain,(
% 0.02/0.45 sk_c12=multiply(inverse(sk_c4),sk_c5)|~sQ15_spl),
% 0.02/0.45 inference(paramodulation,[status(thm)],[f254,f398])).
% 0.02/0.45 fof(f627,plain,(
% 0.02/0.45 sk_c12=multiply(sk_c12,sk_c5)|~sQ16_spl|~sQ15_spl),
% 0.02/0.45 inference(forward_demodulation,[status(thm)],[f266,f625])).
% 0.02/0.45 fof(f628,plain,(
% 0.02/0.45 sk_c12=sk_c11|~sQ14_spl|~sQ16_spl|~sQ15_spl),
% 0.02/0.45 inference(forward_demodulation,[status(thm)],[f242,f627])).
% 0.02/0.45 fof(f634,plain,(
% 0.02/0.45 multiply(sk_c6,sk_c11)=sk_c12|~sQ2_spl|~sQ1_spl|~sQ0_spl|~sQ10_spl),
% 0.02/0.45 inference(backward_demodulation,[status(thm)],[f606,f194])).
% 0.02/0.45 fof(f642,plain,(
% 0.02/0.45 ~multiply(sk_c6,inverse(sk_c6))=sk_c11|~multiply(sk_c12,sk_c12)=sk_c11|~sQ18_spl|~sQ2_spl),
% 0.02/0.45 inference(paramodulation,[status(thm)],[f162,f432])).
% 0.02/0.45 fof(f645,plain,(
% 0.02/0.45 ~multiply(sk_c2,inverse(sk_c2))=sk_c11|~multiply(sk_c3,sk_c12)=sk_c11|~sQ18_spl|~sQ12_spl),
% 0.02/0.45 inference(paramodulation,[status(thm)],[f218,f432])).
% 0.02/0.45 fof(f649,definition,(
% 0.02/0.45 sQ53_spl <=> (multiply(sk_c6,inverse(sk_c6))=sk_c11)),
% 0.02/0.45 introduced(definition,[new_symbols(definition,[sQ53_spl])],[split_symbol_definition])).
% 0.02/0.45 fof(f652,plain,(
% 0.02/0.45 ~sQ53_spl|~sQ44_spl|~sQ18_spl|~sQ2_spl),
% 0.02/0.45 inference(split_clause,[status(thm)],[f642,f649,f417,f280,f161])).
% 0.02/0.45 fof(f664,definition,(
% 0.02/0.45 sQ57_spl <=> (multiply(sk_c2,inverse(sk_c2))=sk_c11)),
% 0.02/0.45 introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition])).
% 0.02/0.45 fof(f666,plain,(
% 0.02/0.45 ~multiply(sk_c2,inverse(sk_c2))=sk_c11|sQ57_spl),
% 0.02/0.45 inference(component_clause,[status(thm)],[f664])).
% 0.02/0.45 fof(f667,plain,(
% 0.02/0.45 ~sQ57_spl|~sQ13_spl|~sQ18_spl|~sQ12_spl),
% 0.02/0.45 inference(split_clause,[status(thm)],[f645,f664,f229,f280,f217])).
% 0.02/0.45 fof(f683,plain,(
% 0.02/0.45 ~multiply(sk_c2,sk_c3)=sk_c11|~sQ12_spl|sQ57_spl),
% 0.02/0.45 inference(forward_demodulation,[status(thm)],[f218,f666])).
% 0.02/0.45 fof(f684,plain,(
% 0.02/0.45 ~sk_c11=sk_c11|~sQ11_spl|~sQ12_spl|sQ57_spl),
% 0.02/0.45 inference(forward_demodulation,[status(thm)],[f206,f683])).
% 0.02/0.45 fof(f685,plain,(
% 0.02/0.45 $false|~sQ11_spl|~sQ12_spl|sQ57_spl),
% 0.02/0.45 inference(trivial_equality_resolution,[status(thm)],[f684])).
% 0.02/0.45 fof(f686,plain,(
% 0.02/0.45 ~sQ11_spl|~sQ12_spl|sQ57_spl),
% 0.02/0.45 inference(contradiction_clause,[status(thm)],[f685])).
% 0.02/0.45 fof(f697,plain,(
% 0.02/0.45 sk_c12=multiply(inverse(sk_c12),sk_c11)|~sQ44_spl),
% 0.02/0.45 inference(paramodulation,[status(thm)],[f418,f398])).
% 0.02/0.45 fof(f699,plain,(
% 0.02/0.45 sk_c12=multiply(sk_c11,sk_c11)|~sQ1_spl|~sQ44_spl),
% 0.02/0.45 inference(forward_demodulation,[status(thm)],[f158,f697])).
% 0.02/0.45 fof(f753,plain,(
% 0.02/0.45 sk_c12=multiply(inverse(sk_c10),sk_c10)|~sQ5_spl|~sQ4_spl),
% 0.02/0.45 inference(paramodulation,[status(thm)],[f593,f398])).
% 0.02/0.45 fof(f757,plain,(
% 0.02/0.45 sk_c12=identity|~sQ5_spl|~sQ4_spl),
% 0.02/0.45 inference(forward_demodulation,[status(thm)],[f78,f753])).
% 0.02/0.45 fof(f763,plain,(
% 0.02/0.45 ![X0]: (X0=multiply(inverse(sk_c12),X0)|~sQ5_spl|~sQ4_spl)),
% 0.02/0.45 inference(backward_demodulation,[status(thm)],[f757,f570])).
% 0.02/0.45 fof(f766,plain,(
% 0.02/0.45 ![X0]: (multiply(inverse(X0),X0)=sk_c12|~sQ5_spl|~sQ4_spl)),
% 0.02/0.45 inference(backward_demodulation,[status(thm)],[f757,f78])).
% 0.02/0.45 fof(f767,plain,(
% 0.02/0.45 ![X0]: (multiply(sk_c12,X0)=X0|~sQ5_spl|~sQ4_spl)),
% 0.02/0.45 inference(backward_demodulation,[status(thm)],[f757,f77])).
% 0.02/0.45 fof(f768,plain,(
% 0.02/0.45 ![X0]: (X0=multiply(sk_c11,X0)|~sQ1_spl|~sQ5_spl|~sQ4_spl)),
% 0.02/0.45 inference(forward_demodulation,[status(thm)],[f158,f763])).
% 0.02/0.45 fof(f773,plain,(
% 0.02/0.45 ~sk_c11=sk_c11|~sQ5_spl|~sQ4_spl|~sQ1_spl|sQ48_spl),
% 0.02/0.45 inference(backward_demodulation,[status(thm)],[f767,f534])).
% 0.02/0.45 fof(f774,plain,(
% 0.02/0.45 sk_c12=sk_c11|~sQ5_spl|~sQ4_spl|~sQ44_spl),
% 0.02/0.45 inference(backward_demodulation,[status(thm)],[f767,f418])).
% 0.02/0.45 fof(f778,plain,(
% 0.02/0.45 $false|~sQ5_spl|~sQ4_spl|~sQ1_spl|sQ48_spl),
% 0.02/0.45 inference(trivial_equality_resolution,[status(thm)],[f773])).
% 0.02/0.45 fof(f779,plain,(
% 0.02/0.45 ~sQ5_spl|~sQ4_spl|~sQ1_spl|sQ48_spl),
% 0.02/0.45 inference(contradiction_clause,[status(thm)],[f778])).
% 0.02/0.45 fof(f780,plain,(
% 0.02/0.45 $false|sQ52_spl|~sQ5_spl|~sQ4_spl|~sQ44_spl),
% 0.02/0.45 inference(forward_subsumption_resolution,[status(thm)],[f774,f531])).
% 0.02/0.45 fof(f781,plain,(
% 0.02/0.45 sQ52_spl|~sQ5_spl|~sQ4_spl|~sQ44_spl),
% 0.02/0.45 inference(contradiction_clause,[status(thm)],[f780])).
% 0.02/0.45 fof(f783,plain,(
% 0.02/0.45 ~sk_c12=sk_c11|~sQ5_spl|~sQ4_spl|sQ49_spl),
% 0.02/0.45 inference(forward_demodulation,[status(thm)],[f757,f440])).
% 0.02/0.45 fof(f792,plain,(
% 0.02/0.45 ~identity=sk_c11|~sQ5_spl|~sQ4_spl|sQ42_spl),
% 0.02/0.45 inference(forward_demodulation,[status(thm)],[f767,f412])).
% 0.02/0.45 fof(f793,plain,(
% 0.02/0.45 ~sk_c12=sk_c11|~sQ5_spl|~sQ4_spl|sQ42_spl),
% 0.02/0.45 inference(forward_demodulation,[status(thm)],[f757,f792])).
% 0.02/0.45 fof(f797,plain,(
% 0.02/0.45 ~inverse(sk_c12)=sk_c12|~sQ5_spl|~sQ4_spl|sQ45_spl),
% 0.02/0.45 inference(forward_demodulation,[status(thm)],[f757,f422])).
% 0.02/0.45 fof(f798,plain,(
% 0.02/0.45 ~sk_c11=sk_c12|~sQ1_spl|~sQ5_spl|~sQ4_spl|sQ45_spl),
% 0.02/0.45 inference(forward_demodulation,[status(thm)],[f158,f797])).
% 0.02/0.45 fof(f809,plain,(
% 0.02/0.45 $false|sQ49_spl|~sQ5_spl|~sQ4_spl|~sQ44_spl),
% 0.02/0.45 inference(forward_subsumption_resolution,[status(thm)],[f774,f783])).
% 0.02/0.45 fof(f810,plain,(
% 0.02/0.45 sQ49_spl|~sQ5_spl|~sQ4_spl|~sQ44_spl),
% 0.02/0.45 inference(contradiction_clause,[status(thm)],[f809])).
% 0.02/0.45 fof(f816,plain,(
% 0.02/0.45 inverse(sk_c6)=sk_c11|~sQ52_spl|~sQ2_spl),
% 0.02/0.45 inference(backward_demodulation,[status(thm)],[f530,f162])).
% 0.02/0.45 fof(f820,plain,(
% 0.02/0.45 multiply(sk_c10,sk_c11)=sk_c11|~sQ52_spl|~sQ6_spl),
% 0.02/0.45 inference(backward_demodulation,[status(thm)],[f530,f178])).
% 0.02/0.45 fof(f821,plain,(
% 0.02/0.45 ~sk_c11=sk_c11|~sQ52_spl|~sQ5_spl|~sQ4_spl|sQ42_spl),
% 0.02/0.45 inference(forward_demodulation,[status(thm)],[f530,f793])).
% 0.02/0.45 fof(f822,plain,(
% 0.02/0.45 $false|~sQ52_spl|~sQ5_spl|~sQ4_spl|sQ42_spl),
% 0.02/0.45 inference(trivial_equality_resolution,[status(thm)],[f821])).
% 0.02/0.45 fof(f823,plain,(
% 0.02/0.45 ~sQ52_spl|~sQ5_spl|~sQ4_spl|sQ42_spl),
% 0.02/0.45 inference(contradiction_clause,[status(thm)],[f822])).
% 0.02/0.45 fof(f830,plain,(
% 0.02/0.45 ~sk_c11=sk_c11|~sQ52_spl|~sQ1_spl|~sQ5_spl|~sQ4_spl|sQ45_spl),
% 0.02/0.45 inference(forward_demodulation,[status(thm)],[f530,f798])).
% 0.02/0.45 fof(f831,plain,(
% 0.02/0.45 $false|~sQ52_spl|~sQ1_spl|~sQ5_spl|~sQ4_spl|sQ45_spl),
% 0.02/0.45 inference(trivial_equality_resolution,[status(thm)],[f830])).
% 0.02/0.45 fof(f832,plain,(
% 0.02/0.45 ~sQ52_spl|~sQ1_spl|~sQ5_spl|~sQ4_spl|sQ45_spl),
% 0.02/0.45 inference(contradiction_clause,[status(thm)],[f831])).
% 0.02/0.45 fof(f833,plain,(
% 0.02/0.45 inverse(identity)=sk_c11|~sQ52_spl|~sQ45_spl),
% 0.02/0.45 inference(forward_demodulation,[status(thm)],[f530,f421])).
% 0.02/0.45 fof(f834,plain,(
% 0.02/0.45 ![X0]: (multiply(inverse(X0),X0)=sk_c11|~sQ52_spl|~sQ5_spl|~sQ4_spl)),
% 0.02/0.45 inference(forward_demodulation,[status(thm)],[f530,f766])).
% 0.02/0.45 fof(f841,plain,(
% 0.02/0.45 ![X0,X1]: (~multiply(X0,inverse(X0))=sk_c11|~multiply(inverse(X0),sk_c11)=sk_c12|~inverse(inverse(X1))=inverse(X0)|~multiply(X1,inverse(X0))=inverse(X1)|~sQ52_spl|~sQ20_spl)),
% 0.02/0.45 inference(forward_demodulation,[status(thm)],[f530,f290])).
% 0.02/0.45 fof(f842,plain,(
% 0.02/0.45 ![X0,X1]: (~multiply(X0,inverse(X0))=sk_c11|~multiply(inverse(X0),sk_c11)=sk_c11|~inverse(inverse(X1))=inverse(X0)|~multiply(X1,inverse(X0))=inverse(X1)|~sQ52_spl|~sQ20_spl)),
% 0.02/0.45 inference(forward_demodulation,[status(thm)],[f530,f841])).
% 0.02/0.45 fof(f880,plain,(
% 0.02/0.45 multiply(sk_c11,sk_c6)=sk_c11|~sQ5_spl|~sQ4_spl|~sQ52_spl|~sQ2_spl),
% 0.02/0.45 inference(paramodulation,[status(thm)],[f816,f834])).
% 0.02/0.45 fof(f881,plain,(
% 0.02/0.45 ![X0]: (X0=multiply(sk_c11,multiply(sk_c6,X0))|~sQ52_spl|~sQ2_spl)),
% 0.02/0.45 inference(paramodulation,[status(thm)],[f816,f398])).
% 0.02/0.45 fof(f889,plain,(
% 0.02/0.45 sk_c6=sk_c11|~sQ1_spl|~sQ5_spl|~sQ4_spl|~sQ52_spl|~sQ2_spl),
% 0.02/0.45 inference(forward_demodulation,[status(thm)],[f768,f880])).
% 0.02/0.45 fof(f890,plain,(
% 0.02/0.45 ![X0]: (X0=multiply(sk_c6,X0)|~sQ1_spl|~sQ5_spl|~sQ4_spl|~sQ52_spl|~sQ2_spl)),
% 0.02/0.45 inference(forward_demodulation,[status(thm)],[f768,f881])).
% 0.02/0.45 fof(f913,plain,(
% 0.02/0.45 identity=sk_c6|~sQ1_spl|~sQ5_spl|~sQ4_spl|~sQ52_spl|~sQ2_spl|~sQ49_spl),
% 0.02/0.45 inference(backward_demodulation,[status(thm)],[f889,f439])).
% 0.02/0.45 fof(f915,plain,(
% 0.02/0.45 ![X0,X1]: (~multiply(X0,inverse(X0))=sk_c11|~multiply(inverse(X0),sk_c11)=sk_c6|~inverse(inverse(X1))=inverse(X0)|~multiply(X1,inverse(X0))=inverse(X1)|~sQ1_spl|~sQ5_spl|~sQ4_spl|~sQ2_spl|~sQ52_spl|~sQ20_spl)),
% 0.02/0.45 inference(backward_demodulation,[status(thm)],[f889,f842])).
% 0.02/0.45 fof(f916,plain,(
% 0.02/0.45 ![X0]: (multiply(inverse(X0),X0)=sk_c6|~sQ1_spl|~sQ2_spl|~sQ52_spl|~sQ5_spl|~sQ4_spl)),
% 0.02/0.45 inference(backward_demodulation,[status(thm)],[f889,f834])).
% 0.02/0.45 fof(f921,plain,(
% 0.02/0.45 ![X0,X1]: (~multiply(X0,inverse(X0))=sk_c6|~multiply(inverse(X0),sk_c11)=sk_c6|~inverse(inverse(X1))=inverse(X0)|~multiply(X1,inverse(X0))=inverse(X1)|~sQ1_spl|~sQ5_spl|~sQ4_spl|~sQ2_spl|~sQ52_spl|~sQ20_spl)),
% 0.02/0.45 inference(forward_demodulation,[status(thm)],[f889,f915])).
% 0.02/0.45 fof(f922,plain,(
% 0.02/0.45 ![X0,X1]: (~multiply(X0,inverse(X0))=sk_c6|~multiply(inverse(X0),sk_c6)=sk_c6|~inverse(inverse(X1))=inverse(X0)|~multiply(X1,inverse(X0))=inverse(X1)|~sQ1_spl|~sQ5_spl|~sQ4_spl|~sQ2_spl|~sQ52_spl|~sQ20_spl)),
% 0.02/0.45 inference(forward_demodulation,[status(thm)],[f889,f921])).
% 0.02/0.45 fof(f980,plain,(
% 0.02/0.45 multiply(sk_c10,sk_c6)=sk_c11|~sQ1_spl|~sQ5_spl|~sQ4_spl|~sQ2_spl|~sQ52_spl|~sQ6_spl),
% 0.02/0.45 inference(forward_demodulation,[status(thm)],[f889,f820])).
% 0.02/0.45 fof(f981,plain,(
% 0.02/0.45 multiply(sk_c10,sk_c6)=sk_c6|~sQ1_spl|~sQ5_spl|~sQ4_spl|~sQ2_spl|~sQ52_spl|~sQ6_spl),
% 0.02/0.45 inference(forward_demodulation,[status(thm)],[f889,f980])).
% 0.02/0.45 fof(f984,plain,(
% 0.02/0.45 ![X0]: (multiply(sk_c6,X0)=multiply(sk_c10,multiply(sk_c6,X0))|~sQ1_spl|~sQ5_spl|~sQ4_spl|~sQ2_spl|~sQ52_spl|~sQ6_spl)),
% 0.02/0.45 inference(paramodulation,[status(thm)],[f981,f79])).
% 0.02/0.45 fof(f985,plain,(
% 0.02/0.45 ![X0]: (X0=multiply(sk_c10,multiply(sk_c6,X0))|~sQ1_spl|~sQ5_spl|~sQ4_spl|~sQ2_spl|~sQ52_spl|~sQ6_spl)),
% 0.02/0.45 inference(forward_demodulation,[status(thm)],[f890,f984])).
% 0.02/0.45 fof(f986,plain,(
% 0.02/0.45 ![X0]: (X0=multiply(sk_c10,X0)|~sQ1_spl|~sQ5_spl|~sQ4_spl|~sQ2_spl|~sQ52_spl|~sQ6_spl)),
% 0.02/0.45 inference(forward_demodulation,[status(thm)],[f890,f985])).
% 0.02/0.45 fof(f1034,plain,(
% 0.02/0.45 sQ52_spl|~sQ14_spl|~sQ16_spl|~sQ15_spl),
% 0.02/0.45 inference(split_clause,[status(thm)],[f628,f529,f241,f265,f253])).
% 0.02/0.45 fof(f1035,plain,(
% 0.02/0.45 sQ3_spl|~sQ2_spl|~sQ1_spl|~sQ0_spl|~sQ10_spl),
% 0.02/0.45 inference(split_clause,[status(thm)],[f634,f165,f161,f157,f154,f193])).
% 0.02/0.45 fof(f1048,plain,(
% 0.02/0.45 inverse(sk_c11)=sk_c11|~sQ52_spl|~sQ1_spl),
% 0.02/0.45 inference(forward_demodulation,[status(thm)],[f530,f158])).
% 0.02/0.45 fof(f1081,plain,(
% 0.02/0.45 multiply(sk_c3,sk_c11)=sk_c11|~sQ52_spl|~sQ13_spl),
% 0.02/0.45 inference(forward_demodulation,[status(thm)],[f530,f230])).
% 0.02/0.45 fof(f1086,plain,(
% 0.02/0.45 ![X0]: (X0=multiply(inverse(identity),X0))),
% 0.02/0.45 inference(paramodulation,[status(thm)],[f77,f398])).
% 0.02/0.45 fof(f1095,plain,(
% 0.02/0.45 sk_c11=multiply(sk_c11,sk_c11)|~sQ52_spl|~sQ1_spl|~sQ44_spl),
% 0.02/0.45 inference(forward_demodulation,[status(thm)],[f530,f699])).
% 0.02/0.45 fof(f1131,plain,(
% 0.02/0.45 multiply(sk_c11,sk_c11)=identity|~sQ52_spl|~sQ1_spl),
% 0.02/0.45 inference(forward_demodulation,[status(thm)],[f530,f446])).
% 0.02/0.45 fof(f1132,plain,(
% 0.02/0.45 ![X0]: (X0=multiply(inverse(sk_c11),X0)|~sQ44_spl|~sQ52_spl|~sQ1_spl)),
% 0.02/0.45 inference(backward_demodulation,[status(thm)],[f1136,f570])).
% 0.02/0.45 fof(f1136,plain,(
% 0.02/0.45 sk_c11=identity|~sQ44_spl|~sQ52_spl|~sQ1_spl),
% 0.02/0.45 inference(forward_demodulation,[status(thm)],[f1095,f1131])).
% 0.02/0.45 fof(f1137,plain,(
% 0.02/0.45 ![X0]: (X0=multiply(sk_c11,X0)|~sQ44_spl|~sQ52_spl|~sQ1_spl)),
% 0.02/0.45 inference(forward_demodulation,[status(thm)],[f1048,f1132])).
% 0.02/0.45 fof(f1138,plain,(
% 0.02/0.45 ![X0]: (multiply(inverse(X0),X0)=sk_c11|~sQ44_spl|~sQ52_spl|~sQ1_spl)),
% 0.02/0.45 inference(forward_demodulation,[status(thm)],[f1136,f78])).
% 0.02/0.45 fof(f1147,plain,(
% 0.02/0.45 multiply(sk_c11,sk_c5)=sk_c11|~sQ52_spl|~sQ14_spl),
% 0.02/0.45 inference(forward_demodulation,[status(thm)],[f530,f242])).
% 0.02/0.45 fof(f1148,plain,(
% 0.02/0.45 sk_c5=multiply(inverse(sk_c11),sk_c11)|~sQ52_spl|~sQ14_spl),
% 0.02/0.45 inference(paramodulation,[status(thm)],[f1147,f398])).
% 0.02/0.45 fof(f1150,plain,(
% 0.02/0.45 sk_c5=sk_c11|~sQ44_spl|~sQ1_spl|~sQ52_spl|~sQ14_spl),
% 0.02/0.45 inference(forward_demodulation,[status(thm)],[f1138,f1148])).
% 0.02/0.45 fof(f1168,plain,(
% 0.02/0.45 inverse(sk_c11)=sk_c5|~sQ44_spl|~sQ14_spl|~sQ52_spl|~sQ1_spl),
% 0.02/0.45 inference(backward_demodulation,[status(thm)],[f1150,f1048])).
% 0.02/0.45 fof(f1180,plain,(
% 0.02/0.45 inverse(sk_c5)=sk_c5|~sQ44_spl|~sQ14_spl|~sQ52_spl|~sQ1_spl),
% 0.02/0.45 inference(forward_demodulation,[status(thm)],[f1150,f1168])).
% 0.02/0.45 fof(f1183,plain,(
% 0.02/0.45 ![X0]: (X0=multiply(sk_c5,X0)|~sQ14_spl|~sQ44_spl|~sQ52_spl|~sQ1_spl)),
% 0.02/0.45 inference(forward_demodulation,[status(thm)],[f1150,f1137])).
% 0.02/0.45 fof(f1212,plain,(
% 0.02/0.45 ![X0,X1]: (~multiply(X0,inverse(X0))=sk_c5|~multiply(inverse(X0),sk_c11)=sk_c11|~inverse(inverse(X1))=inverse(X0)|~multiply(X1,inverse(X0))=inverse(X1)|~sQ44_spl|~sQ1_spl|~sQ14_spl|~sQ52_spl|~sQ20_spl)),
% 0.02/0.45 inference(forward_demodulation,[status(thm)],[f1150,f842])).
% 0.02/0.45 fof(f1213,plain,(
% 0.02/0.45 ![X0,X1]: (~multiply(X0,inverse(X0))=sk_c5|~multiply(inverse(X0),sk_c5)=sk_c11|~inverse(inverse(X1))=inverse(X0)|~multiply(X1,inverse(X0))=inverse(X1)|~sQ44_spl|~sQ1_spl|~sQ14_spl|~sQ52_spl|~sQ20_spl)),
% 0.02/0.45 inference(forward_demodulation,[status(thm)],[f1150,f1212])).
% 0.02/0.45 fof(f1214,plain,(
% 0.02/0.45 ![X0,X1]: (~multiply(X0,inverse(X0))=sk_c5|~multiply(inverse(X0),sk_c5)=sk_c5|~inverse(inverse(X1))=inverse(X0)|~multiply(X1,inverse(X0))=inverse(X1)|~sQ44_spl|~sQ1_spl|~sQ14_spl|~sQ52_spl|~sQ20_spl)),
% 0.02/0.45 inference(forward_demodulation,[status(thm)],[f1150,f1213])).
% 0.02/0.45 fof(f1217,plain,(
% 0.02/0.45 ~multiply(sk_c5,inverse(sk_c5))=sk_c5|~multiply(inverse(sk_c5),sk_c5)=sk_c5|~inverse(inverse(sk_c5))=inverse(sk_c5)|~sQ20_spl|~sQ14_spl|~sQ44_spl|~sQ52_spl|~sQ1_spl),
% 0.02/0.45 inference(resolution,[status(thm)],[f1214,f1183])).
% 0.02/0.45 fof(f1243,definition,(
% 0.02/0.45 sQ94_spl <=> (multiply(sk_c5,inverse(sk_c5))=sk_c5)),
% 0.02/0.45 introduced(definition,[new_symbols(definition,[sQ94_spl])],[split_symbol_definition])).
% 0.02/0.45 fof(f1245,plain,(
% 0.02/0.45 ~multiply(sk_c5,inverse(sk_c5))=sk_c5|sQ94_spl),
% 0.02/0.45 inference(component_clause,[status(thm)],[f1243])).
% 0.02/0.45 fof(f1246,definition,(
% 0.02/0.45 sQ95_spl <=> (multiply(inverse(sk_c5),sk_c5)=sk_c5)),
% 0.02/0.45 introduced(definition,[new_symbols(definition,[sQ95_spl])],[split_symbol_definition])).
% 0.02/0.45 fof(f1248,plain,(
% 0.02/0.45 ~multiply(inverse(sk_c5),sk_c5)=sk_c5|sQ95_spl),
% 0.02/0.45 inference(component_clause,[status(thm)],[f1246])).
% 0.02/0.45 fof(f1249,definition,(
% 0.02/0.45 sQ96_spl <=> (inverse(inverse(sk_c5))=inverse(sk_c5))),
% 0.02/0.45 introduced(definition,[new_symbols(definition,[sQ96_spl])],[split_symbol_definition])).
% 0.02/0.45 fof(f1251,plain,(
% 0.02/0.45 ~inverse(inverse(sk_c5))=inverse(sk_c5)|sQ96_spl),
% 0.02/0.45 inference(component_clause,[status(thm)],[f1249])).
% 0.02/0.45 fof(f1252,plain,(
% 0.02/0.45 ~sQ94_spl|~sQ95_spl|~sQ96_spl|~sQ20_spl|~sQ14_spl|~sQ44_spl|~sQ52_spl|~sQ1_spl),
% 0.02/0.45 inference(split_clause,[status(thm)],[f1217,f1243,f1246,f1249,f286,f241,f417,f529,f157])).
% 0.02/0.45 fof(f1292,plain,(
% 0.02/0.45 ~multiply(sk_c5,sk_c5)=sk_c5|~sQ44_spl|~sQ14_spl|~sQ52_spl|~sQ1_spl|sQ95_spl),
% 0.02/0.45 inference(forward_demodulation,[status(thm)],[f1180,f1248])).
% 0.02/0.45 fof(f1293,plain,(
% 0.02/0.45 ~sk_c5=sk_c5|~sQ44_spl|~sQ14_spl|~sQ52_spl|~sQ1_spl|sQ95_spl),
% 0.02/0.45 inference(forward_demodulation,[status(thm)],[f1183,f1292])).
% 0.02/0.45 fof(f1294,plain,(
% 0.02/0.45 $false|~sQ44_spl|~sQ14_spl|~sQ52_spl|~sQ1_spl|sQ95_spl),
% 0.02/0.45 inference(trivial_equality_resolution,[status(thm)],[f1293])).
% 0.02/0.45 fof(f1295,plain,(
% 0.02/0.45 ~sQ44_spl|~sQ14_spl|~sQ52_spl|~sQ1_spl|sQ95_spl),
% 0.02/0.45 inference(contradiction_clause,[status(thm)],[f1294])).
% 0.02/0.45 fof(f1296,plain,(
% 0.02/0.45 ~inverse(sk_c5)=sk_c5|~sQ14_spl|~sQ44_spl|~sQ52_spl|~sQ1_spl|sQ94_spl),
% 0.02/0.45 inference(forward_demodulation,[status(thm)],[f1183,f1245])).
% 0.02/0.45 fof(f1297,plain,(
% 0.02/0.45 ~sk_c5=sk_c5|~sQ14_spl|~sQ44_spl|~sQ52_spl|~sQ1_spl|sQ94_spl),
% 0.02/0.45 inference(forward_demodulation,[status(thm)],[f1180,f1296])).
% 0.02/0.45 fof(f1298,plain,(
% 0.02/0.45 $false|~sQ14_spl|~sQ44_spl|~sQ52_spl|~sQ1_spl|sQ94_spl),
% 0.02/0.45 inference(trivial_equality_resolution,[status(thm)],[f1297])).
% 0.02/0.45 fof(f1299,plain,(
% 0.02/0.45 ~sQ14_spl|~sQ44_spl|~sQ52_spl|~sQ1_spl|sQ94_spl),
% 0.02/0.45 inference(contradiction_clause,[status(thm)],[f1298])).
% 0.02/0.45 fof(f1313,plain,(
% 0.02/0.45 ~inverse(sk_c5)=inverse(sk_c5)|~sQ44_spl|~sQ14_spl|~sQ52_spl|~sQ1_spl|sQ96_spl),
% 0.02/0.45 inference(forward_demodulation,[status(thm)],[f1180,f1251])).
% 0.02/0.45 fof(f1314,plain,(
% 0.02/0.45 ~sk_c5=inverse(sk_c5)|~sQ44_spl|~sQ14_spl|~sQ52_spl|~sQ1_spl|sQ96_spl),
% 0.02/0.45 inference(forward_demodulation,[status(thm)],[f1180,f1313])).
% 0.02/0.45 fof(f1315,plain,(
% 0.02/0.45 ~sk_c5=sk_c5|~sQ44_spl|~sQ14_spl|~sQ52_spl|~sQ1_spl|sQ96_spl),
% 0.02/0.45 inference(forward_demodulation,[status(thm)],[f1180,f1314])).
% 0.02/0.45 fof(f1316,plain,(
% 0.02/0.45 $false|~sQ44_spl|~sQ14_spl|~sQ52_spl|~sQ1_spl|sQ96_spl),
% 0.02/0.45 inference(trivial_equality_resolution,[status(thm)],[f1315])).
% 0.02/0.45 fof(f1317,plain,(
% 0.02/0.45 ~sQ44_spl|~sQ14_spl|~sQ52_spl|~sQ1_spl|sQ96_spl),
% 0.02/0.45 inference(contradiction_clause,[status(thm)],[f1316])).
% 0.02/0.45 fof(f1337,plain,(
% 0.02/0.45 ![X0,X1]: (multiply(sk_c6,X0)=multiply(inverse(X1),multiply(X1,X0))|~sQ1_spl|~sQ2_spl|~sQ52_spl|~sQ5_spl|~sQ4_spl)),
% 0.02/0.45 inference(paramodulation,[status(thm)],[f916,f79])).
% 0.02/0.45 fof(f1338,plain,(
% 0.02/0.45 ![X0]: (multiply(sk_c6,X0)=X0|~sQ1_spl|~sQ2_spl|~sQ52_spl|~sQ5_spl|~sQ4_spl)),
% 0.02/0.45 inference(forward_demodulation,[status(thm)],[f398,f1337])).
% 0.02/0.45 fof(f1363,plain,(
% 0.02/0.45 multiply(sk_c10,sk_c8)=sk_c6|~sQ1_spl|~sQ2_spl|~sQ52_spl|~sQ5_spl|~sQ4_spl|~sQ8_spl),
% 0.02/0.45 inference(paramodulation,[status(thm)],[f186,f916])).
% 0.02/0.45 fof(f1365,plain,(
% 0.02/0.45 sk_c8=sk_c6|~sQ6_spl|~sQ1_spl|~sQ2_spl|~sQ52_spl|~sQ5_spl|~sQ4_spl|~sQ8_spl),
% 0.02/0.45 inference(forward_demodulation,[status(thm)],[f986,f1363])).
% 0.02/0.45 fof(f1375,plain,(
% 0.02/0.45 identity=sk_c8|~sQ6_spl|~sQ8_spl|~sQ1_spl|~sQ5_spl|~sQ4_spl|~sQ52_spl|~sQ2_spl|~sQ49_spl),
% 0.02/0.45 inference(backward_demodulation,[status(thm)],[f1365,f913])).
% 0.02/0.45 fof(f1376,plain,(
% 0.02/0.45 sk_c8=sk_c11|~sQ6_spl|~sQ8_spl|~sQ1_spl|~sQ5_spl|~sQ4_spl|~sQ52_spl|~sQ2_spl),
% 0.02/0.45 inference(backward_demodulation,[status(thm)],[f1365,f889])).
% 0.02/0.45 fof(f1389,plain,(
% 0.02/0.45 inverse(sk_c8)=sk_c11|~sQ6_spl|~sQ8_spl|~sQ1_spl|~sQ5_spl|~sQ4_spl|~sQ2_spl|~sQ49_spl|~sQ52_spl|~sQ45_spl),
% 0.02/0.45 inference(forward_demodulation,[status(thm)],[f1375,f833])).
% 0.02/0.45 fof(f1390,plain,(
% 0.02/0.45 inverse(sk_c8)=sk_c8|~sQ6_spl|~sQ8_spl|~sQ1_spl|~sQ5_spl|~sQ4_spl|~sQ2_spl|~sQ49_spl|~sQ52_spl|~sQ45_spl),
% 0.02/0.45 inference(forward_demodulation,[status(thm)],[f1376,f1389])).
% 0.02/0.45 fof(f1396,plain,(
% 0.02/0.45 ![X0]: (multiply(sk_c8,X0)=X0|~sQ6_spl|~sQ8_spl|~sQ1_spl|~sQ2_spl|~sQ52_spl|~sQ5_spl|~sQ4_spl)),
% 0.02/0.45 inference(forward_demodulation,[status(thm)],[f1365,f1338])).
% 0.02/0.45 fof(f1400,plain,(
% 0.02/0.45 ![X0,X1]: (~multiply(X0,inverse(X0))=sk_c8|~multiply(inverse(X0),sk_c6)=sk_c6|~inverse(inverse(X1))=inverse(X0)|~multiply(X1,inverse(X0))=inverse(X1)|~sQ6_spl|~sQ8_spl|~sQ1_spl|~sQ5_spl|~sQ4_spl|~sQ2_spl|~sQ52_spl|~sQ20_spl)),
% 0.02/0.45 inference(forward_demodulation,[status(thm)],[f1365,f922])).
% 0.02/0.45 fof(f1401,plain,(
% 0.02/0.45 ![X0,X1]: (~multiply(X0,inverse(X0))=sk_c8|~multiply(inverse(X0),sk_c8)=sk_c6|~inverse(inverse(X1))=inverse(X0)|~multiply(X1,inverse(X0))=inverse(X1)|~sQ6_spl|~sQ8_spl|~sQ1_spl|~sQ5_spl|~sQ4_spl|~sQ2_spl|~sQ52_spl|~sQ20_spl)),
% 0.02/0.45 inference(forward_demodulation,[status(thm)],[f1365,f1400])).
% 0.02/0.45 fof(f1402,plain,(
% 0.02/0.45 ![X0,X1]: (~multiply(X0,inverse(X0))=sk_c8|~multiply(inverse(X0),sk_c8)=sk_c8|~inverse(inverse(X1))=inverse(X0)|~multiply(X1,inverse(X0))=inverse(X1)|~sQ6_spl|~sQ8_spl|~sQ1_spl|~sQ5_spl|~sQ4_spl|~sQ2_spl|~sQ52_spl|~sQ20_spl)),
% 0.02/0.45 inference(forward_demodulation,[status(thm)],[f1365,f1401])).
% 0.02/0.45 fof(f1403,plain,(
% 0.02/0.45 ~multiply(sk_c8,inverse(sk_c8))=sk_c8|~multiply(inverse(sk_c8),sk_c8)=sk_c8|~inverse(inverse(sk_c8))=inverse(sk_c8)|~sQ20_spl|~sQ6_spl|~sQ8_spl|~sQ1_spl|~sQ2_spl|~sQ52_spl|~sQ5_spl|~sQ4_spl),
% 0.02/0.45 inference(resolution,[status(thm)],[f1402,f1396])).
% 0.02/0.45 fof(f1408,definition,(
% 0.02/0.45 sQ102_spl <=> (multiply(sk_c8,inverse(sk_c8))=sk_c8)),
% 0.02/0.45 introduced(definition,[new_symbols(definition,[sQ102_spl])],[split_symbol_definition])).
% 0.02/0.45 fof(f1410,plain,(
% 0.02/0.45 ~multiply(sk_c8,inverse(sk_c8))=sk_c8|sQ102_spl),
% 0.02/0.45 inference(component_clause,[status(thm)],[f1408])).
% 0.02/0.45 fof(f1411,definition,(
% 0.02/0.45 sQ103_spl <=> (multiply(inverse(sk_c8),sk_c8)=sk_c8)),
% 0.02/0.45 introduced(definition,[new_symbols(definition,[sQ103_spl])],[split_symbol_definition])).
% 0.02/0.45 fof(f1413,plain,(
% 0.02/0.45 ~multiply(inverse(sk_c8),sk_c8)=sk_c8|sQ103_spl),
% 0.02/0.45 inference(component_clause,[status(thm)],[f1411])).
% 0.02/0.45 fof(f1414,definition,(
% 0.02/0.45 sQ104_spl <=> (inverse(inverse(sk_c8))=inverse(sk_c8))),
% 0.02/0.45 introduced(definition,[new_symbols(definition,[sQ104_spl])],[split_symbol_definition])).
% 0.02/0.45 fof(f1416,plain,(
% 0.02/0.45 ~inverse(inverse(sk_c8))=inverse(sk_c8)|sQ104_spl),
% 0.02/0.45 inference(component_clause,[status(thm)],[f1414])).
% 0.02/0.45 fof(f1417,plain,(
% 0.02/0.45 ~sQ102_spl|~sQ103_spl|~sQ104_spl|~sQ20_spl|~sQ6_spl|~sQ8_spl|~sQ1_spl|~sQ2_spl|~sQ52_spl|~sQ5_spl|~sQ4_spl),
% 0.02/0.45 inference(split_clause,[status(thm)],[f1403,f1408,f1411,f1414,f286,f177,f185,f157,f161,f529,f173,f169])).
% 0.02/0.45 fof(f1433,plain,(
% 0.02/0.45 ~multiply(sk_c8,sk_c8)=sk_c8|~sQ6_spl|~sQ8_spl|~sQ1_spl|~sQ5_spl|~sQ4_spl|~sQ2_spl|~sQ49_spl|~sQ52_spl|~sQ45_spl|sQ103_spl),
% 0.02/0.45 inference(forward_demodulation,[status(thm)],[f1390,f1413])).
% 0.02/0.45 fof(f1434,plain,(
% 0.02/0.45 ~sk_c8=sk_c8|~sQ6_spl|~sQ8_spl|~sQ1_spl|~sQ5_spl|~sQ4_spl|~sQ2_spl|~sQ49_spl|~sQ52_spl|~sQ45_spl|sQ103_spl),
% 0.02/0.45 inference(forward_demodulation,[status(thm)],[f1396,f1433])).
% 0.02/0.45 fof(f1435,plain,(
% 0.02/0.45 $false|~sQ6_spl|~sQ8_spl|~sQ1_spl|~sQ5_spl|~sQ4_spl|~sQ2_spl|~sQ49_spl|~sQ52_spl|~sQ45_spl|sQ103_spl),
% 0.02/0.45 inference(trivial_equality_resolution,[status(thm)],[f1434])).
% 0.02/0.45 fof(f1436,plain,(
% 0.02/0.45 ~sQ6_spl|~sQ8_spl|~sQ1_spl|~sQ5_spl|~sQ4_spl|~sQ2_spl|~sQ49_spl|~sQ52_spl|~sQ45_spl|sQ103_spl),
% 0.02/0.45 inference(contradiction_clause,[status(thm)],[f1435])).
% 0.02/0.45 fof(f1437,plain,(
% 0.02/0.45 ~inverse(sk_c8)=sk_c8|~sQ6_spl|~sQ8_spl|~sQ1_spl|~sQ2_spl|~sQ52_spl|~sQ5_spl|~sQ4_spl|sQ102_spl),
% 0.02/0.45 inference(forward_demodulation,[status(thm)],[f1396,f1410])).
% 0.02/0.45 fof(f1438,plain,(
% 0.02/0.45 ~sk_c8=sk_c8|~sQ49_spl|~sQ45_spl|~sQ6_spl|~sQ8_spl|~sQ1_spl|~sQ2_spl|~sQ52_spl|~sQ5_spl|~sQ4_spl|sQ102_spl),
% 0.02/0.45 inference(forward_demodulation,[status(thm)],[f1390,f1437])).
% 0.02/0.45 fof(f1439,plain,(
% 0.02/0.45 $false|~sQ49_spl|~sQ45_spl|~sQ6_spl|~sQ8_spl|~sQ1_spl|~sQ2_spl|~sQ52_spl|~sQ5_spl|~sQ4_spl|sQ102_spl),
% 0.02/0.45 inference(trivial_equality_resolution,[status(thm)],[f1438])).
% 0.02/0.45 fof(f1440,plain,(
% 0.02/0.45 ~sQ49_spl|~sQ45_spl|~sQ6_spl|~sQ8_spl|~sQ1_spl|~sQ2_spl|~sQ52_spl|~sQ5_spl|~sQ4_spl|sQ102_spl),
% 0.02/0.45 inference(contradiction_clause,[status(thm)],[f1439])).
% 0.02/0.45 fof(f1447,plain,(
% 0.02/0.45 ~inverse(sk_c8)=inverse(sk_c8)|~sQ6_spl|~sQ8_spl|~sQ1_spl|~sQ5_spl|~sQ4_spl|~sQ2_spl|~sQ49_spl|~sQ52_spl|~sQ45_spl|sQ104_spl),
% 0.02/0.45 inference(forward_demodulation,[status(thm)],[f1390,f1416])).
% 0.02/0.45 fof(f1448,plain,(
% 0.02/0.45 ~sk_c8=inverse(sk_c8)|~sQ6_spl|~sQ8_spl|~sQ1_spl|~sQ5_spl|~sQ4_spl|~sQ2_spl|~sQ49_spl|~sQ52_spl|~sQ45_spl|sQ104_spl),
% 0.02/0.45 inference(forward_demodulation,[status(thm)],[f1390,f1447])).
% 0.02/0.45 fof(f1449,plain,(
% 0.02/0.45 ~sk_c8=sk_c8|~sQ6_spl|~sQ8_spl|~sQ1_spl|~sQ5_spl|~sQ4_spl|~sQ2_spl|~sQ49_spl|~sQ52_spl|~sQ45_spl|sQ104_spl),
% 0.02/0.45 inference(forward_demodulation,[status(thm)],[f1390,f1448])).
% 0.02/0.45 fof(f1450,plain,(
% 0.02/0.45 $false|~sQ6_spl|~sQ8_spl|~sQ1_spl|~sQ5_spl|~sQ4_spl|~sQ2_spl|~sQ49_spl|~sQ52_spl|~sQ45_spl|sQ104_spl),
% 0.02/0.45 inference(trivial_equality_resolution,[status(thm)],[f1449])).
% 0.02/0.45 fof(f1451,plain,(
% 0.02/0.45 ~sQ6_spl|~sQ8_spl|~sQ1_spl|~sQ5_spl|~sQ4_spl|~sQ2_spl|~sQ49_spl|~sQ52_spl|~sQ45_spl|sQ104_spl),
% 0.02/0.45 inference(contradiction_clause,[status(thm)],[f1450])).
% 0.02/0.45 fof(f1452,plain,(
% 0.02/0.45 ~sQ0_spl|~sQ17_spl|~sQ10_spl),
% 0.02/0.45 inference(split_clause,[status(thm)],[f465,f154,f277,f193])).
% 0.02/0.45 fof(f1477,plain,(
% 0.02/0.45 ~inverse(sk_c11)=sk_c11|~sQ52_spl|sQ1_spl),
% 0.02/0.45 inference(forward_demodulation,[status(thm)],[f530,f159])).
% 0.02/0.45 fof(f1478,plain,(
% 0.02/0.45 ![X0]: (multiply(identity,X0)=X0)),
% 0.02/0.45 inference(paramodulation,[status(thm)],[f398,f1086])).
% 0.02/0.45 fof(f1500,plain,(
% 0.02/0.45 sk_c3=sk_c11|~sQ12_spl|~sQ11_spl|~sQ52_spl|~sQ13_spl),
% 0.02/0.45 inference(backward_demodulation,[status(thm)],[f595,f1081])).
% 0.02/0.45 fof(f1503,plain,(
% 0.02/0.45 sk_c3=multiply(sk_c3,sk_c3)|~sQ52_spl|~sQ13_spl|~sQ12_spl|~sQ11_spl),
% 0.02/0.45 inference(backward_demodulation,[status(thm)],[f1500,f595])).
% 0.02/0.45 fof(f1510,plain,(
% 0.02/0.45 ~inverse(sk_c11)=sk_c3|~sQ12_spl|~sQ11_spl|~sQ13_spl|~sQ52_spl|sQ1_spl),
% 0.02/0.45 inference(backward_demodulation,[status(thm)],[f1500,f1477])).
% 0.02/0.45 fof(f1520,plain,(
% 0.02/0.45 ~inverse(sk_c3)=sk_c3|~sQ12_spl|~sQ11_spl|~sQ13_spl|~sQ52_spl|sQ1_spl),
% 0.02/0.45 inference(forward_demodulation,[status(thm)],[f1500,f1510])).
% 0.02/0.45 fof(f1529,plain,(
% 0.02/0.45 multiply(sk_c3,sk_c5)=sk_c11|~sQ12_spl|~sQ11_spl|~sQ13_spl|~sQ52_spl|~sQ14_spl),
% 0.02/0.45 inference(forward_demodulation,[status(thm)],[f1500,f1147])).
% 0.02/0.45 fof(f1531,plain,(
% 0.02/0.45 multiply(sk_c3,sk_c5)=sk_c3|~sQ12_spl|~sQ11_spl|~sQ13_spl|~sQ52_spl|~sQ14_spl),
% 0.02/0.45 inference(forward_demodulation,[status(thm)],[f1500,f1529])).
% 0.02/0.45 fof(f1580,plain,(
% 0.02/0.45 sk_c3=multiply(inverse(sk_c3),sk_c3)|~sQ52_spl|~sQ13_spl|~sQ12_spl|~sQ11_spl),
% 0.02/0.45 inference(paramodulation,[status(thm)],[f1503,f398])).
% 0.02/0.45 fof(f1582,plain,(
% 0.02/0.45 sk_c3=identity|~sQ52_spl|~sQ13_spl|~sQ12_spl|~sQ11_spl),
% 0.02/0.45 inference(forward_demodulation,[status(thm)],[f78,f1580])).
% 0.02/0.45 fof(f1588,plain,(
% 0.02/0.45 ![X0]: (multiply(inverse(X0),X0)=sk_c3|~sQ52_spl|~sQ13_spl|~sQ12_spl|~sQ11_spl)),
% 0.02/0.45 inference(backward_demodulation,[status(thm)],[f1582,f78])).
% 0.02/0.45 fof(f1589,plain,(
% 0.02/0.45 ![X0]: (multiply(sk_c3,X0)=X0|~sQ52_spl|~sQ13_spl|~sQ12_spl|~sQ11_spl)),
% 0.02/0.45 inference(backward_demodulation,[status(thm)],[f1582,f1478])).
% 0.02/0.45 fof(f1600,plain,(
% 0.02/0.45 sk_c5=sk_c3|~sQ12_spl|~sQ11_spl|~sQ13_spl|~sQ52_spl|~sQ14_spl),
% 0.02/0.45 inference(backward_demodulation,[status(thm)],[f1589,f1531])).
% 0.02/0.45 fof(f1606,plain,(
% 0.02/0.45 ![X0]: (multiply(sk_c5,X0)=X0|~sQ14_spl|~sQ52_spl|~sQ13_spl|~sQ12_spl|~sQ11_spl)),
% 0.02/0.45 inference(backward_demodulation,[status(thm)],[f1600,f1589])).
% 0.02/0.45 fof(f1615,plain,(
% 0.02/0.45 ~inverse(sk_c3)=sk_c5|~sQ14_spl|~sQ12_spl|~sQ11_spl|~sQ13_spl|~sQ52_spl|sQ1_spl),
% 0.02/0.45 inference(backward_demodulation,[status(thm)],[f1600,f1520])).
% 0.02/0.45 fof(f1618,plain,(
% 0.02/0.45 inverse(sk_c2)=sk_c5|~sQ11_spl|~sQ13_spl|~sQ52_spl|~sQ14_spl|~sQ12_spl),
% 0.02/0.45 inference(backward_demodulation,[status(thm)],[f1600,f218])).
% 0.02/0.45 fof(f1623,plain,(
% 0.02/0.45 ~inverse(sk_c5)=sk_c5|~sQ14_spl|~sQ12_spl|~sQ11_spl|~sQ13_spl|~sQ52_spl|sQ1_spl),
% 0.02/0.45 inference(forward_demodulation,[status(thm)],[f1600,f1615])).
% 0.02/0.45 fof(f1647,plain,(
% 0.02/0.45 ![X0]: (multiply(inverse(X0),X0)=sk_c5|~sQ14_spl|~sQ52_spl|~sQ13_spl|~sQ12_spl|~sQ11_spl)),
% 0.02/0.45 inference(forward_demodulation,[status(thm)],[f1600,f1588])).
% 0.02/0.45 fof(f1648,plain,(
% 0.02/0.45 multiply(sk_c5,sk_c2)=sk_c5|~sQ11_spl|~sQ13_spl|~sQ52_spl|~sQ14_spl|~sQ12_spl),
% 0.02/0.45 inference(paramodulation,[status(thm)],[f1618,f1647])).
% 0.02/0.45 fof(f1653,plain,(
% 0.02/0.45 sk_c2=sk_c5|~sQ11_spl|~sQ13_spl|~sQ52_spl|~sQ14_spl|~sQ12_spl),
% 0.02/0.45 inference(forward_demodulation,[status(thm)],[f1606,f1648])).
% 0.02/0.45 fof(f1658,plain,(
% 0.02/0.45 inverse(sk_c5)=sk_c5|~sQ11_spl|~sQ13_spl|~sQ52_spl|~sQ14_spl|~sQ12_spl),
% 0.02/0.45 inference(backward_demodulation,[status(thm)],[f1653,f1618])).
% 0.02/0.45 fof(f1659,plain,(
% 0.02/0.45 $false|sQ1_spl|~sQ11_spl|~sQ13_spl|~sQ52_spl|~sQ14_spl|~sQ12_spl),
% 0.02/0.45 inference(forward_subsumption_resolution,[status(thm)],[f1658,f1623])).
% 0.02/0.45 fof(f1660,plain,(
% 0.02/0.45 sQ1_spl|~sQ11_spl|~sQ13_spl|~sQ52_spl|~sQ14_spl|~sQ12_spl),
% 0.02/0.45 inference(contradiction_clause,[status(thm)],[f1659])).
% 0.02/0.45 fof(f1661,plain,(
% 0.02/0.45 $false),
% 0.02/0.45 inference(sat_refutation,[status(thm)],[f164,f168,f172,f176,f197,f198,f199,f200,f208,f209,f211,f212,f220,f221,f223,f224,f232,f233,f235,f236,f244,f245,f247,f248,f249,f251,f256,f257,f259,f260,f261,f263,f268,f269,f271,f272,f273,f275,f289,f330,f350,f416,f423,f431,f441,f457,f474,f499,f517,f522,f528,f532,f591,f652,f667,f686,f779,f781,f810,f823,f832,f1034,f1035,f1252,f1295,f1299,f1317,f1417,f1436,f1440,f1451,f1452,f1660])).
% 0.02/0.45 % SZS output end CNFRefutation for theBenchmark.p
% 0.02/0.47 % Elapsed time: 0.094915 seconds
% 0.02/0.47 % CPU time: 0.560043 seconds
% 0.02/0.47 % Total memory used: 116.815 MB
% 0.02/0.47 % Net memory used: 116.246 MB
%------------------------------------------------------------------------------