Drodi-SAT---4.1.1.UNS-Ass.s

%------------------------------------------------------------------------------
% File     : Drodi-SAT---4.1.1
% Problem  : GRP307-1 : TPTP v9.3.1. Released v2.5.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p

% Computer : n011.cluster.edu
% Model    : x86_64 x86_64
% CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory   : 8046.5625MB
% OS       : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit  : 300s
% DateTime : Thu Sep 24 12:36:25 PM UTC 2026

% Result   : Unsatisfiable 0.10s 0.50s
% Output   : Assurance 0s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03  % Problem  : GRP307-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.04  % Command  : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.37  % Computer : n011.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:08:55 UTC 2026
% 0.10/0.37  % CPUTime  : 
% 0.10/0.38  % Drodi V4.1.1
% 0.10/0.50  % Refutation found
% 0.10/0.50  % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.10/0.50  % SZS output start CNFRefutation for theBenchmark
% 0.10/0.50  fof(f1,axiom,(
% 0.10/0.50    (![X]: (multiply(identity,X) = X ))),
% 0.10/0.50    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.50  fof(f2,axiom,(
% 0.10/0.50    (![X]: (multiply(inverse(X),X) = identity ))),
% 0.10/0.50    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.50  fof(f3,axiom,(
% 0.10/0.50    (![X,Y,Z]: (multiply(multiply(X,Y),Z) = multiply(X,multiply(Y,Z)) ))),
% 0.10/0.50    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.50  fof(f4,negated_conjecture,(
% 0.10/0.50    ( multiply(sk_c11,sk_c10) = sk_c9| multiply(sk_c3,sk_c11) = sk_c10 ) ),
% 0.10/0.50    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.50  fof(f5,negated_conjecture,(
% 0.10/0.50    ( multiply(sk_c11,sk_c10) = sk_c9| inverse(sk_c3) = sk_c11 ) ),
% 0.10/0.50    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.50  fof(f6,negated_conjecture,(
% 0.10/0.50    ( multiply(sk_c11,sk_c10) = sk_c9| multiply(sk_c4,sk_c10) = sk_c9 ) ),
% 0.10/0.50    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.50  fof(f7,negated_conjecture,(
% 0.10/0.50    ( multiply(sk_c11,sk_c10) = sk_c9| inverse(sk_c4) = sk_c10 ) ),
% 0.10/0.50    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.50  fof(f8,negated_conjecture,(
% 0.10/0.50    ( multiply(sk_c11,sk_c10) = sk_c9| multiply(sk_c5,sk_c8) = sk_c11 ) ),
% 0.10/0.50    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.50  fof(f9,negated_conjecture,(
% 0.10/0.50    ( multiply(sk_c11,sk_c10) = sk_c9| inverse(sk_c5) = sk_c8 ) ),
% 0.10/0.50    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.50  fof(f10,negated_conjecture,(
% 0.10/0.50    ( multiply(sk_c11,sk_c10) = sk_c9| multiply(sk_c8,sk_c10) = sk_c11 ) ),
% 0.10/0.50    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.50  fof(f11,negated_conjecture,(
% 0.10/0.50    ( multiply(sk_c11,sk_c10) = sk_c9| inverse(sk_c7) = sk_c6 ) ),
% 0.10/0.50    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.50  fof(f12,negated_conjecture,(
% 0.10/0.50    ( multiply(sk_c11,sk_c10) = sk_c9| inverse(sk_c6) = sk_c8 ) ),
% 0.10/0.50    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.50  fof(f14,negated_conjecture,(
% 0.10/0.50    ( inverse(sk_c11) = sk_c9| multiply(sk_c3,sk_c11) = sk_c10 ) ),
% 0.10/0.50    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.50  fof(f15,negated_conjecture,(
% 0.10/0.50    ( inverse(sk_c11) = sk_c9| inverse(sk_c3) = sk_c11 ) ),
% 0.10/0.50    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.50  fof(f16,negated_conjecture,(
% 0.10/0.50    ( inverse(sk_c11) = sk_c9| multiply(sk_c4,sk_c10) = sk_c9 ) ),
% 0.10/0.50    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.50  fof(f17,negated_conjecture,(
% 0.10/0.50    ( inverse(sk_c11) = sk_c9| inverse(sk_c4) = sk_c10 ) ),
% 0.10/0.50    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.50  fof(f18,negated_conjecture,(
% 0.10/0.50    ( inverse(sk_c11) = sk_c9| multiply(sk_c5,sk_c8) = sk_c11 ) ),
% 0.10/0.50    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.50  fof(f19,negated_conjecture,(
% 0.10/0.50    ( inverse(sk_c11) = sk_c9| inverse(sk_c5) = sk_c8 ) ),
% 0.10/0.50    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.50  fof(f20,negated_conjecture,(
% 0.10/0.50    ( inverse(sk_c11) = sk_c9| multiply(sk_c8,sk_c10) = sk_c11 ) ),
% 0.10/0.50    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.50  fof(f22,negated_conjecture,(
% 0.10/0.50    ( inverse(sk_c11) = sk_c9| inverse(sk_c6) = sk_c8 ) ),
% 0.10/0.50    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.50  fof(f24,negated_conjecture,(
% 0.10/0.50    ( multiply(sk_c9,sk_c10) = sk_c11| multiply(sk_c3,sk_c11) = sk_c10 ) ),
% 0.10/0.50    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.50  fof(f25,negated_conjecture,(
% 0.10/0.50    ( multiply(sk_c9,sk_c10) = sk_c11| inverse(sk_c3) = sk_c11 ) ),
% 0.10/0.50    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.50  fof(f28,negated_conjecture,(
% 0.10/0.50    ( multiply(sk_c9,sk_c10) = sk_c11| multiply(sk_c5,sk_c8) = sk_c11 ) ),
% 0.10/0.50    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.50  fof(f29,negated_conjecture,(
% 0.10/0.50    ( multiply(sk_c9,sk_c10) = sk_c11| inverse(sk_c5) = sk_c8 ) ),
% 0.10/0.50    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.50  fof(f30,negated_conjecture,(
% 0.10/0.50    ( multiply(sk_c9,sk_c10) = sk_c11| multiply(sk_c8,sk_c10) = sk_c11 ) ),
% 0.10/0.50    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.50  fof(f32,negated_conjecture,(
% 0.10/0.50    ( multiply(sk_c9,sk_c10) = sk_c11| inverse(sk_c6) = sk_c8 ) ),
% 0.10/0.50    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.50  fof(f34,negated_conjecture,(
% 0.10/0.50    ( multiply(sk_c11,sk_c2) = sk_c10| multiply(sk_c3,sk_c11) = sk_c10 ) ),
% 0.10/0.50    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.50  fof(f35,negated_conjecture,(
% 0.10/0.50    ( multiply(sk_c11,sk_c2) = sk_c10| inverse(sk_c3) = sk_c11 ) ),
% 0.10/0.50    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.50  fof(f37,negated_conjecture,(
% 0.10/0.50    ( multiply(sk_c11,sk_c2) = sk_c10| inverse(sk_c4) = sk_c10 ) ),
% 0.10/0.50    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.50  fof(f38,negated_conjecture,(
% 0.10/0.50    ( multiply(sk_c11,sk_c2) = sk_c10| multiply(sk_c5,sk_c8) = sk_c11 ) ),
% 0.10/0.50    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.50  fof(f39,negated_conjecture,(
% 0.10/0.50    ( multiply(sk_c11,sk_c2) = sk_c10| inverse(sk_c5) = sk_c8 ) ),
% 0.10/0.50    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.50  fof(f40,negated_conjecture,(
% 0.10/0.50    ( multiply(sk_c11,sk_c2) = sk_c10| multiply(sk_c8,sk_c10) = sk_c11 ) ),
% 0.10/0.50    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.50  fof(f41,negated_conjecture,(
% 0.10/0.50    ( multiply(sk_c11,sk_c2) = sk_c10| inverse(sk_c7) = sk_c6 ) ),
% 0.10/0.50    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.50  fof(f42,negated_conjecture,(
% 0.10/0.50    ( multiply(sk_c11,sk_c2) = sk_c10| inverse(sk_c6) = sk_c8 ) ),
% 0.10/0.50    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.50  fof(f43,negated_conjecture,(
% 0.10/0.50    ( multiply(sk_c11,sk_c2) = sk_c10| multiply(sk_c7,sk_c8) = sk_c6 ) ),
% 0.10/0.50    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.50  fof(f44,negated_conjecture,(
% 0.10/0.50    ( multiply(sk_c1,sk_c11) = sk_c2| multiply(sk_c3,sk_c11) = sk_c10 ) ),
% 0.10/0.50    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.50  fof(f45,negated_conjecture,(
% 0.10/0.50    ( multiply(sk_c1,sk_c11) = sk_c2| inverse(sk_c3) = sk_c11 ) ),
% 0.10/0.50    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.50  fof(f47,negated_conjecture,(
% 0.10/0.50    ( multiply(sk_c1,sk_c11) = sk_c2| inverse(sk_c4) = sk_c10 ) ),
% 0.10/0.50    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.50  fof(f48,negated_conjecture,(
% 0.10/0.50    ( multiply(sk_c1,sk_c11) = sk_c2| multiply(sk_c5,sk_c8) = sk_c11 ) ),
% 0.10/0.50    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.50  fof(f49,negated_conjecture,(
% 0.10/0.50    ( multiply(sk_c1,sk_c11) = sk_c2| inverse(sk_c5) = sk_c8 ) ),
% 0.10/0.50    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.50  fof(f50,negated_conjecture,(
% 0.10/0.50    ( multiply(sk_c1,sk_c11) = sk_c2| multiply(sk_c8,sk_c10) = sk_c11 ) ),
% 0.10/0.50    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.50  fof(f52,negated_conjecture,(
% 0.10/0.50    ( multiply(sk_c1,sk_c11) = sk_c2| inverse(sk_c6) = sk_c8 ) ),
% 0.10/0.50    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.50  fof(f54,negated_conjecture,(
% 0.10/0.50    ( inverse(sk_c1) = sk_c11| multiply(sk_c3,sk_c11) = sk_c10 ) ),
% 0.10/0.50    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.50  fof(f55,negated_conjecture,(
% 0.10/0.50    ( inverse(sk_c1) = sk_c11| inverse(sk_c3) = sk_c11 ) ),
% 0.10/0.50    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.50  fof(f57,negated_conjecture,(
% 0.10/0.50    ( inverse(sk_c1) = sk_c11| inverse(sk_c4) = sk_c10 ) ),
% 0.10/0.50    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.50  fof(f58,negated_conjecture,(
% 0.10/0.50    ( inverse(sk_c1) = sk_c11| multiply(sk_c5,sk_c8) = sk_c11 ) ),
% 0.10/0.50    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.50  fof(f59,negated_conjecture,(
% 0.10/0.50    ( inverse(sk_c1) = sk_c11| inverse(sk_c5) = sk_c8 ) ),
% 0.10/0.50    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.50  fof(f60,negated_conjecture,(
% 0.10/0.50    ( inverse(sk_c1) = sk_c11| multiply(sk_c8,sk_c10) = sk_c11 ) ),
% 0.10/0.50    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.50  fof(f62,negated_conjecture,(
% 0.10/0.50    ( inverse(sk_c1) = sk_c11| inverse(sk_c6) = sk_c8 ) ),
% 0.10/0.50    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.50  fof(f64,negated_conjecture,(
% 0.10/0.50    (![X3,X4,X1,X2,X5,X6,X7,X8]: (( multiply(sk_c11,sk_c10) != sk_c9| inverse(sk_c11) != sk_c9| multiply(sk_c9,sk_c10) != sk_c11| multiply(sk_c11,X3) != sk_c10| multiply(X4,sk_c11) != X3| inverse(X4) != sk_c11| multiply(X1,sk_c11) != sk_c10| inverse(X1) != sk_c11| multiply(X2,sk_c10) != sk_c9| inverse(X2) != sk_c10| multiply(X5,X6) != sk_c11| inverse(X5) != X6| multiply(X6,sk_c10) != sk_c11| inverse(X7) != X8| inverse(X8) != X6| multiply(X7,X6) != X8 ) ))),
% 0.10/0.50    file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 0.10/0.50  fof(f65,plain,(
% 0.10/0.50    ![X0]: (multiply(identity,X0)=X0)),
% 0.10/0.50    inference(cnf_transformation,[status(thm)],[f1])).
% 0.10/0.50  fof(f66,plain,(
% 0.10/0.50    ![X0]: (multiply(inverse(X0),X0)=identity)),
% 0.10/0.50    inference(cnf_transformation,[status(thm)],[f2])).
% 0.10/0.50  fof(f67,plain,(
% 0.10/0.50    ![X0,X1,X2]: (multiply(multiply(X0,X1),X2)=multiply(X0,multiply(X1,X2)))),
% 0.10/0.50    inference(cnf_transformation,[status(thm)],[f3])).
% 0.10/0.50  fof(f68,plain,(
% 0.10/0.50    multiply(sk_c11,sk_c10)=sk_c9|multiply(sk_c3,sk_c11)=sk_c10),
% 0.10/0.50    inference(cnf_transformation,[status(thm)],[f4])).
% 0.10/0.50  fof(f69,plain,(
% 0.10/0.50    multiply(sk_c11,sk_c10)=sk_c9|inverse(sk_c3)=sk_c11),
% 0.10/0.50    inference(cnf_transformation,[status(thm)],[f5])).
% 0.10/0.50  fof(f70,plain,(
% 0.10/0.50    multiply(sk_c11,sk_c10)=sk_c9|multiply(sk_c4,sk_c10)=sk_c9),
% 0.10/0.50    inference(cnf_transformation,[status(thm)],[f6])).
% 0.10/0.50  fof(f71,plain,(
% 0.10/0.50    multiply(sk_c11,sk_c10)=sk_c9|inverse(sk_c4)=sk_c10),
% 0.10/0.50    inference(cnf_transformation,[status(thm)],[f7])).
% 0.10/0.50  fof(f72,plain,(
% 0.10/0.50    multiply(sk_c11,sk_c10)=sk_c9|multiply(sk_c5,sk_c8)=sk_c11),
% 0.10/0.50    inference(cnf_transformation,[status(thm)],[f8])).
% 0.10/0.50  fof(f73,plain,(
% 0.10/0.50    multiply(sk_c11,sk_c10)=sk_c9|inverse(sk_c5)=sk_c8),
% 0.10/0.50    inference(cnf_transformation,[status(thm)],[f9])).
% 0.10/0.50  fof(f74,plain,(
% 0.10/0.50    multiply(sk_c11,sk_c10)=sk_c9|multiply(sk_c8,sk_c10)=sk_c11),
% 0.10/0.50    inference(cnf_transformation,[status(thm)],[f10])).
% 0.10/0.50  fof(f75,plain,(
% 0.10/0.50    multiply(sk_c11,sk_c10)=sk_c9|inverse(sk_c7)=sk_c6),
% 0.10/0.50    inference(cnf_transformation,[status(thm)],[f11])).
% 0.10/0.50  fof(f76,plain,(
% 0.10/0.50    multiply(sk_c11,sk_c10)=sk_c9|inverse(sk_c6)=sk_c8),
% 0.10/0.50    inference(cnf_transformation,[status(thm)],[f12])).
% 0.10/0.50  fof(f78,plain,(
% 0.10/0.50    inverse(sk_c11)=sk_c9|multiply(sk_c3,sk_c11)=sk_c10),
% 0.10/0.50    inference(cnf_transformation,[status(thm)],[f14])).
% 0.10/0.50  fof(f79,plain,(
% 0.10/0.50    inverse(sk_c11)=sk_c9|inverse(sk_c3)=sk_c11),
% 0.10/0.50    inference(cnf_transformation,[status(thm)],[f15])).
% 0.10/0.50  fof(f80,plain,(
% 0.10/0.50    inverse(sk_c11)=sk_c9|multiply(sk_c4,sk_c10)=sk_c9),
% 0.10/0.50    inference(cnf_transformation,[status(thm)],[f16])).
% 0.10/0.50  fof(f81,plain,(
% 0.10/0.50    inverse(sk_c11)=sk_c9|inverse(sk_c4)=sk_c10),
% 0.10/0.50    inference(cnf_transformation,[status(thm)],[f17])).
% 0.10/0.50  fof(f82,plain,(
% 0.10/0.50    inverse(sk_c11)=sk_c9|multiply(sk_c5,sk_c8)=sk_c11),
% 0.10/0.50    inference(cnf_transformation,[status(thm)],[f18])).
% 0.10/0.50  fof(f83,plain,(
% 0.10/0.50    inverse(sk_c11)=sk_c9|inverse(sk_c5)=sk_c8),
% 0.10/0.50    inference(cnf_transformation,[status(thm)],[f19])).
% 0.10/0.50  fof(f84,plain,(
% 0.10/0.50    inverse(sk_c11)=sk_c9|multiply(sk_c8,sk_c10)=sk_c11),
% 0.10/0.50    inference(cnf_transformation,[status(thm)],[f20])).
% 0.10/0.50  fof(f86,plain,(
% 0.10/0.50    inverse(sk_c11)=sk_c9|inverse(sk_c6)=sk_c8),
% 0.10/0.50    inference(cnf_transformation,[status(thm)],[f22])).
% 0.10/0.50  fof(f88,plain,(
% 0.10/0.50    multiply(sk_c9,sk_c10)=sk_c11|multiply(sk_c3,sk_c11)=sk_c10),
% 0.10/0.50    inference(cnf_transformation,[status(thm)],[f24])).
% 0.10/0.50  fof(f89,plain,(
% 0.10/0.50    multiply(sk_c9,sk_c10)=sk_c11|inverse(sk_c3)=sk_c11),
% 0.10/0.50    inference(cnf_transformation,[status(thm)],[f25])).
% 0.10/0.50  fof(f92,plain,(
% 0.10/0.50    multiply(sk_c9,sk_c10)=sk_c11|multiply(sk_c5,sk_c8)=sk_c11),
% 0.10/0.50    inference(cnf_transformation,[status(thm)],[f28])).
% 0.10/0.50  fof(f93,plain,(
% 0.10/0.50    multiply(sk_c9,sk_c10)=sk_c11|inverse(sk_c5)=sk_c8),
% 0.10/0.50    inference(cnf_transformation,[status(thm)],[f29])).
% 0.10/0.50  fof(f94,plain,(
% 0.10/0.50    multiply(sk_c9,sk_c10)=sk_c11|multiply(sk_c8,sk_c10)=sk_c11),
% 0.10/0.50    inference(cnf_transformation,[status(thm)],[f30])).
% 0.10/0.50  fof(f96,plain,(
% 0.10/0.50    multiply(sk_c9,sk_c10)=sk_c11|inverse(sk_c6)=sk_c8),
% 0.10/0.50    inference(cnf_transformation,[status(thm)],[f32])).
% 0.10/0.50  fof(f98,plain,(
% 0.10/0.50    multiply(sk_c11,sk_c2)=sk_c10|multiply(sk_c3,sk_c11)=sk_c10),
% 0.10/0.50    inference(cnf_transformation,[status(thm)],[f34])).
% 0.10/0.50  fof(f99,plain,(
% 0.10/0.50    multiply(sk_c11,sk_c2)=sk_c10|inverse(sk_c3)=sk_c11),
% 0.10/0.50    inference(cnf_transformation,[status(thm)],[f35])).
% 0.10/0.50  fof(f101,plain,(
% 0.10/0.50    multiply(sk_c11,sk_c2)=sk_c10|inverse(sk_c4)=sk_c10),
% 0.10/0.50    inference(cnf_transformation,[status(thm)],[f37])).
% 0.10/0.50  fof(f102,plain,(
% 0.10/0.50    multiply(sk_c11,sk_c2)=sk_c10|multiply(sk_c5,sk_c8)=sk_c11),
% 0.10/0.50    inference(cnf_transformation,[status(thm)],[f38])).
% 0.10/0.50  fof(f103,plain,(
% 0.10/0.50    multiply(sk_c11,sk_c2)=sk_c10|inverse(sk_c5)=sk_c8),
% 0.10/0.50    inference(cnf_transformation,[status(thm)],[f39])).
% 0.10/0.50  fof(f104,plain,(
% 0.10/0.50    multiply(sk_c11,sk_c2)=sk_c10|multiply(sk_c8,sk_c10)=sk_c11),
% 0.10/0.50    inference(cnf_transformation,[status(thm)],[f40])).
% 0.10/0.50  fof(f105,plain,(
% 0.10/0.50    multiply(sk_c11,sk_c2)=sk_c10|inverse(sk_c7)=sk_c6),
% 0.10/0.50    inference(cnf_transformation,[status(thm)],[f41])).
% 0.10/0.50  fof(f106,plain,(
% 0.10/0.50    multiply(sk_c11,sk_c2)=sk_c10|inverse(sk_c6)=sk_c8),
% 0.10/0.50    inference(cnf_transformation,[status(thm)],[f42])).
% 0.10/0.50  fof(f107,plain,(
% 0.10/0.50    multiply(sk_c11,sk_c2)=sk_c10|multiply(sk_c7,sk_c8)=sk_c6),
% 0.10/0.50    inference(cnf_transformation,[status(thm)],[f43])).
% 0.10/0.50  fof(f108,plain,(
% 0.10/0.50    multiply(sk_c1,sk_c11)=sk_c2|multiply(sk_c3,sk_c11)=sk_c10),
% 0.10/0.50    inference(cnf_transformation,[status(thm)],[f44])).
% 0.10/0.50  fof(f109,plain,(
% 0.10/0.50    multiply(sk_c1,sk_c11)=sk_c2|inverse(sk_c3)=sk_c11),
% 0.10/0.50    inference(cnf_transformation,[status(thm)],[f45])).
% 0.10/0.50  fof(f111,plain,(
% 0.10/0.50    multiply(sk_c1,sk_c11)=sk_c2|inverse(sk_c4)=sk_c10),
% 0.10/0.50    inference(cnf_transformation,[status(thm)],[f47])).
% 0.10/0.50  fof(f112,plain,(
% 0.10/0.50    multiply(sk_c1,sk_c11)=sk_c2|multiply(sk_c5,sk_c8)=sk_c11),
% 0.10/0.50    inference(cnf_transformation,[status(thm)],[f48])).
% 0.10/0.50  fof(f113,plain,(
% 0.10/0.50    multiply(sk_c1,sk_c11)=sk_c2|inverse(sk_c5)=sk_c8),
% 0.10/0.50    inference(cnf_transformation,[status(thm)],[f49])).
% 0.10/0.50  fof(f114,plain,(
% 0.10/0.50    multiply(sk_c1,sk_c11)=sk_c2|multiply(sk_c8,sk_c10)=sk_c11),
% 0.10/0.50    inference(cnf_transformation,[status(thm)],[f50])).
% 0.10/0.50  fof(f116,plain,(
% 0.10/0.50    multiply(sk_c1,sk_c11)=sk_c2|inverse(sk_c6)=sk_c8),
% 0.10/0.50    inference(cnf_transformation,[status(thm)],[f52])).
% 0.10/0.50  fof(f118,plain,(
% 0.10/0.50    inverse(sk_c1)=sk_c11|multiply(sk_c3,sk_c11)=sk_c10),
% 0.10/0.50    inference(cnf_transformation,[status(thm)],[f54])).
% 0.10/0.50  fof(f119,plain,(
% 0.10/0.50    inverse(sk_c1)=sk_c11|inverse(sk_c3)=sk_c11),
% 0.10/0.50    inference(cnf_transformation,[status(thm)],[f55])).
% 0.10/0.50  fof(f121,plain,(
% 0.10/0.50    inverse(sk_c1)=sk_c11|inverse(sk_c4)=sk_c10),
% 0.10/0.50    inference(cnf_transformation,[status(thm)],[f57])).
% 0.10/0.50  fof(f122,plain,(
% 0.10/0.50    inverse(sk_c1)=sk_c11|multiply(sk_c5,sk_c8)=sk_c11),
% 0.10/0.50    inference(cnf_transformation,[status(thm)],[f58])).
% 0.10/0.50  fof(f123,plain,(
% 0.10/0.50    inverse(sk_c1)=sk_c11|inverse(sk_c5)=sk_c8),
% 0.10/0.50    inference(cnf_transformation,[status(thm)],[f59])).
% 0.10/0.50  fof(f124,plain,(
% 0.10/0.50    inverse(sk_c1)=sk_c11|multiply(sk_c8,sk_c10)=sk_c11),
% 0.10/0.50    inference(cnf_transformation,[status(thm)],[f60])).
% 0.10/0.50  fof(f126,plain,(
% 0.10/0.50    inverse(sk_c1)=sk_c11|inverse(sk_c6)=sk_c8),
% 0.10/0.50    inference(cnf_transformation,[status(thm)],[f62])).
% 0.10/0.50  fof(f128,plain,(
% 0.10/0.50    ![X6,X7,X8]: (((((![X5]: (((![X2]: (((![X1]: (((![X4]: ((![X3]: ((((~multiply(sk_c11,sk_c10)=sk_c9|~inverse(sk_c11)=sk_c9)|~multiply(sk_c9,sk_c10)=sk_c11)|~multiply(sk_c11,X3)=sk_c10)|~multiply(X4,sk_c11)=X3))|~inverse(X4)=sk_c11))|~multiply(X1,sk_c11)=sk_c10)|~inverse(X1)=sk_c11))|~multiply(X2,sk_c10)=sk_c9)|~inverse(X2)=sk_c10))|~multiply(X5,X6)=sk_c11)|~inverse(X5)=X6))|~multiply(X6,sk_c10)=sk_c11)|~inverse(X7)=X8)|~inverse(X8)=X6)|~multiply(X7,X6)=X8)),
% 0.10/0.50    inference(miniscoping,[status(thm)],[f64])).
% 0.10/0.50  fof(f129,plain,(
% 0.10/0.50    ![X0,X1,X2,X3,X4,X5,X6,X7]: (~multiply(sk_c11,sk_c10)=sk_c9|~inverse(sk_c11)=sk_c9|~multiply(sk_c9,sk_c10)=sk_c11|~multiply(sk_c11,X0)=sk_c10|~multiply(X1,sk_c11)=X0|~inverse(X1)=sk_c11|~multiply(X2,sk_c11)=sk_c10|~inverse(X2)=sk_c11|~multiply(X3,sk_c10)=sk_c9|~inverse(X3)=sk_c10|~multiply(X4,X5)=sk_c11|~inverse(X4)=X5|~multiply(X5,sk_c10)=sk_c11|~inverse(X6)=X7|~inverse(X7)=X5|~multiply(X6,X5)=X7)),
% 0.10/0.50    inference(cnf_transformation,[status(thm)],[f128])).
% 0.10/0.50  fof(f130,definition,(
% 0.10/0.50    sQ0_spl <=> (multiply(sk_c11,sk_c10)=sk_c9)),
% 0.10/0.50    introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition])).
% 0.10/0.50  fof(f131,plain,(
% 0.10/0.50    multiply(sk_c11,sk_c10)=sk_c9|~sQ0_spl),
% 0.10/0.50    inference(component_clause,[status(thm)],[f130])).
% 0.10/0.50  fof(f132,plain,(
% 0.10/0.50    ~multiply(sk_c11,sk_c10)=sk_c9|sQ0_spl),
% 0.10/0.50    inference(component_clause,[status(thm)],[f130])).
% 0.10/0.50  fof(f133,definition,(
% 0.10/0.50    sQ1_spl <=> (multiply(sk_c3,sk_c11)=sk_c10)),
% 0.10/0.50    introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition])).
% 0.10/0.50  fof(f134,plain,(
% 0.10/0.50    multiply(sk_c3,sk_c11)=sk_c10|~sQ1_spl),
% 0.10/0.50    inference(component_clause,[status(thm)],[f133])).
% 0.10/0.50  fof(f136,plain,(
% 0.10/0.50    sQ0_spl|sQ1_spl),
% 0.10/0.50    inference(split_clause,[status(thm)],[f68,f130,f133])).
% 0.10/0.50  fof(f137,definition,(
% 0.10/0.50    sQ2_spl <=> (inverse(sk_c3)=sk_c11)),
% 0.10/0.50    introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition])).
% 0.10/0.50  fof(f138,plain,(
% 0.10/0.50    inverse(sk_c3)=sk_c11|~sQ2_spl),
% 0.10/0.50    inference(component_clause,[status(thm)],[f137])).
% 0.10/0.50  fof(f140,plain,(
% 0.10/0.50    sQ0_spl|sQ2_spl),
% 0.10/0.50    inference(split_clause,[status(thm)],[f69,f130,f137])).
% 0.10/0.50  fof(f141,definition,(
% 0.10/0.50    sQ3_spl <=> (multiply(sk_c4,sk_c10)=sk_c9)),
% 0.10/0.50    introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition])).
% 0.10/0.50  fof(f142,plain,(
% 0.10/0.50    multiply(sk_c4,sk_c10)=sk_c9|~sQ3_spl),
% 0.10/0.50    inference(component_clause,[status(thm)],[f141])).
% 0.10/0.50  fof(f144,plain,(
% 0.10/0.50    sQ0_spl|sQ3_spl),
% 0.10/0.50    inference(split_clause,[status(thm)],[f70,f130,f141])).
% 0.10/0.50  fof(f145,definition,(
% 0.10/0.50    sQ4_spl <=> (inverse(sk_c4)=sk_c10)),
% 0.10/0.50    introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition])).
% 0.10/0.50  fof(f146,plain,(
% 0.10/0.50    inverse(sk_c4)=sk_c10|~sQ4_spl),
% 0.10/0.50    inference(component_clause,[status(thm)],[f145])).
% 0.10/0.50  fof(f148,plain,(
% 0.10/0.50    sQ0_spl|sQ4_spl),
% 0.10/0.50    inference(split_clause,[status(thm)],[f71,f130,f145])).
% 0.10/0.50  fof(f149,definition,(
% 0.10/0.50    sQ5_spl <=> (multiply(sk_c5,sk_c8)=sk_c11)),
% 0.10/0.50    introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition])).
% 0.10/0.50  fof(f150,plain,(
% 0.10/0.50    multiply(sk_c5,sk_c8)=sk_c11|~sQ5_spl),
% 0.10/0.50    inference(component_clause,[status(thm)],[f149])).
% 0.10/0.50  fof(f152,plain,(
% 0.10/0.50    sQ0_spl|sQ5_spl),
% 0.10/0.50    inference(split_clause,[status(thm)],[f72,f130,f149])).
% 0.10/0.50  fof(f153,definition,(
% 0.10/0.50    sQ6_spl <=> (inverse(sk_c5)=sk_c8)),
% 0.10/0.50    introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition])).
% 0.10/0.50  fof(f154,plain,(
% 0.10/0.50    inverse(sk_c5)=sk_c8|~sQ6_spl),
% 0.10/0.50    inference(component_clause,[status(thm)],[f153])).
% 0.10/0.50  fof(f156,plain,(
% 0.10/0.50    sQ0_spl|sQ6_spl),
% 0.10/0.50    inference(split_clause,[status(thm)],[f73,f130,f153])).
% 0.10/0.50  fof(f157,definition,(
% 0.10/0.50    sQ7_spl <=> (multiply(sk_c8,sk_c10)=sk_c11)),
% 0.10/0.50    introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition])).
% 0.10/0.50  fof(f158,plain,(
% 0.10/0.50    multiply(sk_c8,sk_c10)=sk_c11|~sQ7_spl),
% 0.10/0.50    inference(component_clause,[status(thm)],[f157])).
% 0.10/0.50  fof(f160,plain,(
% 0.10/0.50    sQ0_spl|sQ7_spl),
% 0.10/0.50    inference(split_clause,[status(thm)],[f74,f130,f157])).
% 0.10/0.50  fof(f161,definition,(
% 0.10/0.50    sQ8_spl <=> (inverse(sk_c7)=sk_c6)),
% 0.10/0.50    introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition])).
% 0.10/0.50  fof(f162,plain,(
% 0.10/0.50    inverse(sk_c7)=sk_c6|~sQ8_spl),
% 0.10/0.50    inference(component_clause,[status(thm)],[f161])).
% 0.10/0.50  fof(f164,plain,(
% 0.10/0.50    sQ0_spl|sQ8_spl),
% 0.10/0.50    inference(split_clause,[status(thm)],[f75,f130,f161])).
% 0.10/0.50  fof(f165,definition,(
% 0.10/0.50    sQ9_spl <=> (inverse(sk_c6)=sk_c8)),
% 0.10/0.50    introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition])).
% 0.10/0.50  fof(f166,plain,(
% 0.10/0.50    inverse(sk_c6)=sk_c8|~sQ9_spl),
% 0.10/0.50    inference(component_clause,[status(thm)],[f165])).
% 0.10/0.50  fof(f168,plain,(
% 0.10/0.50    sQ0_spl|sQ9_spl),
% 0.10/0.50    inference(split_clause,[status(thm)],[f76,f130,f165])).
% 0.10/0.50  fof(f169,definition,(
% 0.10/0.50    sQ10_spl <=> (multiply(sk_c7,sk_c8)=sk_c6)),
% 0.10/0.50    introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition])).
% 0.10/0.50  fof(f170,plain,(
% 0.10/0.50    multiply(sk_c7,sk_c8)=sk_c6|~sQ10_spl),
% 0.10/0.50    inference(component_clause,[status(thm)],[f169])).
% 0.10/0.50  fof(f173,definition,(
% 0.10/0.50    sQ11_spl <=> (inverse(sk_c11)=sk_c9)),
% 0.10/0.50    introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition])).
% 0.10/0.50  fof(f174,plain,(
% 0.10/0.50    inverse(sk_c11)=sk_c9|~sQ11_spl),
% 0.10/0.50    inference(component_clause,[status(thm)],[f173])).
% 0.10/0.50  fof(f175,plain,(
% 0.10/0.50    ~inverse(sk_c11)=sk_c9|sQ11_spl),
% 0.10/0.50    inference(component_clause,[status(thm)],[f173])).
% 0.10/0.50  fof(f176,plain,(
% 0.10/0.50    sQ11_spl|sQ1_spl),
% 0.10/0.50    inference(split_clause,[status(thm)],[f78,f173,f133])).
% 0.10/0.50  fof(f177,plain,(
% 0.10/0.50    sQ11_spl|sQ2_spl),
% 0.10/0.50    inference(split_clause,[status(thm)],[f79,f173,f137])).
% 0.10/0.50  fof(f178,plain,(
% 0.10/0.50    sQ11_spl|sQ3_spl),
% 0.10/0.50    inference(split_clause,[status(thm)],[f80,f173,f141])).
% 0.10/0.50  fof(f179,plain,(
% 0.10/0.50    sQ11_spl|sQ4_spl),
% 0.10/0.50    inference(split_clause,[status(thm)],[f81,f173,f145])).
% 0.10/0.50  fof(f180,plain,(
% 0.10/0.50    sQ11_spl|sQ5_spl),
% 0.10/0.50    inference(split_clause,[status(thm)],[f82,f173,f149])).
% 0.10/0.50  fof(f181,plain,(
% 0.10/0.50    sQ11_spl|sQ6_spl),
% 0.10/0.50    inference(split_clause,[status(thm)],[f83,f173,f153])).
% 0.10/0.50  fof(f182,plain,(
% 0.10/0.50    sQ11_spl|sQ7_spl),
% 0.10/0.50    inference(split_clause,[status(thm)],[f84,f173,f157])).
% 0.10/0.50  fof(f184,plain,(
% 0.10/0.50    sQ11_spl|sQ9_spl),
% 0.10/0.50    inference(split_clause,[status(thm)],[f86,f173,f165])).
% 0.10/0.50  fof(f186,definition,(
% 0.10/0.50    sQ12_spl <=> (multiply(sk_c9,sk_c10)=sk_c11)),
% 0.10/0.50    introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition])).
% 0.10/0.50  fof(f187,plain,(
% 0.10/0.50    multiply(sk_c9,sk_c10)=sk_c11|~sQ12_spl),
% 0.10/0.50    inference(component_clause,[status(thm)],[f186])).
% 0.10/0.50  fof(f188,plain,(
% 0.10/0.50    ~multiply(sk_c9,sk_c10)=sk_c11|sQ12_spl),
% 0.10/0.50    inference(component_clause,[status(thm)],[f186])).
% 0.10/0.50  fof(f189,plain,(
% 0.10/0.50    sQ12_spl|sQ1_spl),
% 0.10/0.50    inference(split_clause,[status(thm)],[f88,f186,f133])).
% 0.10/0.50  fof(f190,plain,(
% 0.10/0.50    sQ12_spl|sQ2_spl),
% 0.10/0.50    inference(split_clause,[status(thm)],[f89,f186,f137])).
% 0.10/0.50  fof(f193,plain,(
% 0.10/0.50    sQ12_spl|sQ5_spl),
% 0.10/0.50    inference(split_clause,[status(thm)],[f92,f186,f149])).
% 0.10/0.50  fof(f194,plain,(
% 0.10/0.50    sQ12_spl|sQ6_spl),
% 0.10/0.50    inference(split_clause,[status(thm)],[f93,f186,f153])).
% 0.10/0.50  fof(f195,plain,(
% 0.10/0.50    sQ12_spl|sQ7_spl),
% 0.10/0.50    inference(split_clause,[status(thm)],[f94,f186,f157])).
% 0.10/0.50  fof(f197,plain,(
% 0.10/0.50    sQ12_spl|sQ9_spl),
% 0.10/0.50    inference(split_clause,[status(thm)],[f96,f186,f165])).
% 0.10/0.50  fof(f199,definition,(
% 0.10/0.50    sQ13_spl <=> (multiply(sk_c11,sk_c2)=sk_c10)),
% 0.10/0.50    introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition])).
% 0.10/0.50  fof(f200,plain,(
% 0.10/0.50    multiply(sk_c11,sk_c2)=sk_c10|~sQ13_spl),
% 0.10/0.50    inference(component_clause,[status(thm)],[f199])).
% 0.10/0.50  fof(f202,plain,(
% 0.10/0.50    sQ13_spl|sQ1_spl),
% 0.10/0.50    inference(split_clause,[status(thm)],[f98,f199,f133])).
% 0.10/0.50  fof(f203,plain,(
% 0.10/0.50    sQ13_spl|sQ2_spl),
% 0.10/0.50    inference(split_clause,[status(thm)],[f99,f199,f137])).
% 0.10/0.50  fof(f205,plain,(
% 0.10/0.50    sQ13_spl|sQ4_spl),
% 0.10/0.50    inference(split_clause,[status(thm)],[f101,f199,f145])).
% 0.10/0.50  fof(f206,plain,(
% 0.10/0.50    sQ13_spl|sQ5_spl),
% 0.10/0.50    inference(split_clause,[status(thm)],[f102,f199,f149])).
% 0.10/0.50  fof(f207,plain,(
% 0.10/0.50    sQ13_spl|sQ6_spl),
% 0.10/0.50    inference(split_clause,[status(thm)],[f103,f199,f153])).
% 0.10/0.50  fof(f208,plain,(
% 0.10/0.50    sQ13_spl|sQ7_spl),
% 0.10/0.50    inference(split_clause,[status(thm)],[f104,f199,f157])).
% 0.10/0.50  fof(f209,plain,(
% 0.10/0.50    sQ13_spl|sQ8_spl),
% 0.10/0.50    inference(split_clause,[status(thm)],[f105,f199,f161])).
% 0.10/0.50  fof(f210,plain,(
% 0.10/0.50    sQ13_spl|sQ9_spl),
% 0.10/0.50    inference(split_clause,[status(thm)],[f106,f199,f165])).
% 0.10/0.50  fof(f211,plain,(
% 0.10/0.50    sQ13_spl|sQ10_spl),
% 0.10/0.50    inference(split_clause,[status(thm)],[f107,f199,f169])).
% 0.10/0.50  fof(f212,definition,(
% 0.10/0.50    sQ14_spl <=> (multiply(sk_c1,sk_c11)=sk_c2)),
% 0.10/0.50    introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition])).
% 0.10/0.50  fof(f213,plain,(
% 0.10/0.50    multiply(sk_c1,sk_c11)=sk_c2|~sQ14_spl),
% 0.10/0.50    inference(component_clause,[status(thm)],[f212])).
% 0.10/0.50  fof(f215,plain,(
% 0.10/0.50    sQ14_spl|sQ1_spl),
% 0.10/0.50    inference(split_clause,[status(thm)],[f108,f212,f133])).
% 0.10/0.50  fof(f216,plain,(
% 0.10/0.50    sQ14_spl|sQ2_spl),
% 0.10/0.50    inference(split_clause,[status(thm)],[f109,f212,f137])).
% 0.10/0.50  fof(f218,plain,(
% 0.10/0.50    sQ14_spl|sQ4_spl),
% 0.10/0.50    inference(split_clause,[status(thm)],[f111,f212,f145])).
% 0.10/0.50  fof(f219,plain,(
% 0.10/0.50    sQ14_spl|sQ5_spl),
% 0.10/0.50    inference(split_clause,[status(thm)],[f112,f212,f149])).
% 0.10/0.50  fof(f220,plain,(
% 0.10/0.50    sQ14_spl|sQ6_spl),
% 0.10/0.50    inference(split_clause,[status(thm)],[f113,f212,f153])).
% 0.10/0.50  fof(f221,plain,(
% 0.10/0.50    sQ14_spl|sQ7_spl),
% 0.10/0.50    inference(split_clause,[status(thm)],[f114,f212,f157])).
% 0.10/0.50  fof(f223,plain,(
% 0.10/0.50    sQ14_spl|sQ9_spl),
% 0.10/0.50    inference(split_clause,[status(thm)],[f116,f212,f165])).
% 0.10/0.50  fof(f225,definition,(
% 0.10/0.50    sQ15_spl <=> (inverse(sk_c1)=sk_c11)),
% 0.10/0.50    introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition])).
% 0.10/0.50  fof(f226,plain,(
% 0.10/0.50    inverse(sk_c1)=sk_c11|~sQ15_spl),
% 0.10/0.50    inference(component_clause,[status(thm)],[f225])).
% 0.10/0.50  fof(f228,plain,(
% 0.10/0.50    sQ15_spl|sQ1_spl),
% 0.10/0.50    inference(split_clause,[status(thm)],[f118,f225,f133])).
% 0.10/0.50  fof(f229,plain,(
% 0.10/0.50    sQ15_spl|sQ2_spl),
% 0.10/0.50    inference(split_clause,[status(thm)],[f119,f225,f137])).
% 0.10/0.50  fof(f231,plain,(
% 0.10/0.50    sQ15_spl|sQ4_spl),
% 0.10/0.50    inference(split_clause,[status(thm)],[f121,f225,f145])).
% 0.10/0.50  fof(f232,plain,(
% 0.10/0.50    sQ15_spl|sQ5_spl),
% 0.10/0.50    inference(split_clause,[status(thm)],[f122,f225,f149])).
% 0.10/0.50  fof(f233,plain,(
% 0.10/0.50    sQ15_spl|sQ6_spl),
% 0.10/0.50    inference(split_clause,[status(thm)],[f123,f225,f153])).
% 0.10/0.50  fof(f234,plain,(
% 0.10/0.50    sQ15_spl|sQ7_spl),
% 0.10/0.50    inference(split_clause,[status(thm)],[f124,f225,f157])).
% 0.10/0.50  fof(f236,plain,(
% 0.10/0.50    sQ15_spl|sQ9_spl),
% 0.10/0.50    inference(split_clause,[status(thm)],[f126,f225,f165])).
% 0.10/0.50  fof(f238,definition,(
% 0.10/0.50    ![X0,X1]: (sQ16_spl <=> (~multiply(sk_c11,X0)=sk_c10|~multiply(X1,sk_c11)=X0|~inverse(X1)=sk_c11))),
% 0.10/0.50    introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition])).
% 0.10/0.50  fof(f239,plain,(
% 0.10/0.50    ![X0,X1]: (~multiply(sk_c11,X0)=sk_c10|~multiply(X1,sk_c11)=X0|~inverse(X1)=sk_c11|~sQ16_spl)),
% 0.10/0.50    inference(component_clause,[status(thm)],[f238])).
% 0.10/0.50  fof(f241,definition,(
% 0.10/0.50    ![X2]: (sQ17_spl <=> (~multiply(X2,sk_c11)=sk_c10|~inverse(X2)=sk_c11))),
% 0.10/0.50    introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition])).
% 0.10/0.50  fof(f242,plain,(
% 0.10/0.50    ![X0]: (~multiply(X0,sk_c11)=sk_c10|~inverse(X0)=sk_c11|~sQ17_spl)),
% 0.10/0.50    inference(component_clause,[status(thm)],[f241])).
% 0.10/0.50  fof(f244,definition,(
% 0.10/0.50    ![X3]: (sQ18_spl <=> (~multiply(X3,sk_c10)=sk_c9|~inverse(X3)=sk_c10))),
% 0.10/0.50    introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition])).
% 0.10/0.50  fof(f245,plain,(
% 0.10/0.50    ![X0]: (~multiply(X0,sk_c10)=sk_c9|~inverse(X0)=sk_c10|~sQ18_spl)),
% 0.10/0.50    inference(component_clause,[status(thm)],[f244])).
% 0.10/0.50  fof(f247,definition,(
% 0.10/0.50    ![X4,X5,X6,X7]: (sQ19_spl <=> (~multiply(X4,X5)=sk_c11|~inverse(X4)=X5|~multiply(X5,sk_c10)=sk_c11|~inverse(X6)=X7|~inverse(X7)=X5|~multiply(X6,X5)=X7))),
% 0.10/0.50    introduced(definition,[new_symbols(definition,[sQ19_spl])],[split_symbol_definition])).
% 0.10/0.50  fof(f248,plain,(
% 0.10/0.50    ![X0,X1,X2,X3]: (~multiply(X0,X1)=sk_c11|~inverse(X0)=X1|~multiply(X1,sk_c10)=sk_c11|~inverse(X2)=X3|~inverse(X3)=X1|~multiply(X2,X1)=X3|~sQ19_spl)),
% 0.10/0.50    inference(component_clause,[status(thm)],[f247])).
% 0.10/0.50  fof(f250,plain,(
% 0.10/0.50    ~sQ0_spl|~sQ11_spl|~sQ12_spl|sQ16_spl|sQ17_spl|sQ18_spl|sQ19_spl),
% 0.10/0.50    inference(split_clause,[status(thm)],[f129,f130,f173,f186,f238,f241,f244,f247])).
% 0.10/0.50  fof(f251,plain,(
% 0.10/0.50    ![X0,X1]: (~multiply(X0,inverse(X0))=sk_c11|~multiply(inverse(X0),sk_c10)=sk_c11|~inverse(inverse(X1))=inverse(X0)|~multiply(X1,inverse(X0))=inverse(X1)|~sQ19_spl)),
% 0.10/0.50    inference(destructive_equality_resolution,[status(thm)],[f248])).
% 0.10/0.50  fof(f253,plain,(
% 0.10/0.50    ![X0]: (multiply(sk_c11,X0)=multiply(sk_c9,multiply(sk_c10,X0))|~sQ12_spl)),
% 0.10/0.50    inference(paramodulation,[status(thm)],[f187,f67])).
% 0.10/0.50  fof(f265,plain,(
% 0.10/0.50    ![X0]: (~multiply(sk_c11,inverse(sk_c11))=sk_c11|~multiply(inverse(sk_c11),sk_c10)=sk_c11|~inverse(inverse(X0))=inverse(sk_c11)|~multiply(X0,sk_c9)=inverse(X0)|~sQ19_spl|~sQ11_spl)),
% 0.10/0.50    inference(paramodulation,[status(thm)],[f174,f251])).
% 0.10/0.50  fof(f268,plain,(
% 0.10/0.50    ![X0]: (~multiply(sk_c5,inverse(sk_c5))=sk_c11|~multiply(inverse(sk_c5),sk_c10)=sk_c11|~inverse(inverse(X0))=inverse(sk_c5)|~multiply(X0,sk_c8)=inverse(X0)|~sQ19_spl|~sQ6_spl)),
% 0.10/0.50    inference(paramodulation,[status(thm)],[f154,f251])).
% 0.10/0.50  fof(f270,plain,(
% 0.10/0.50    ![X0]: (~multiply(sk_c6,inverse(sk_c6))=sk_c11|~multiply(inverse(sk_c6),sk_c10)=sk_c11|~inverse(inverse(X0))=inverse(sk_c6)|~multiply(X0,sk_c8)=inverse(X0)|~sQ19_spl|~sQ9_spl)),
% 0.10/0.50    inference(paramodulation,[status(thm)],[f166,f251])).
% 0.10/0.50  fof(f272,definition,(
% 0.10/0.50    sQ20_spl <=> (multiply(sk_c11,inverse(sk_c11))=sk_c11)),
% 0.10/0.50    introduced(definition,[new_symbols(definition,[sQ20_spl])],[split_symbol_definition])).
% 0.10/0.50  fof(f275,definition,(
% 0.10/0.50    sQ21_spl <=> (multiply(inverse(sk_c11),sk_c10)=sk_c11)),
% 0.10/0.50    introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition])).
% 0.10/0.50  fof(f277,plain,(
% 0.10/0.50    ~multiply(inverse(sk_c11),sk_c10)=sk_c11|sQ21_spl),
% 0.10/0.50    inference(component_clause,[status(thm)],[f275])).
% 0.10/0.50  fof(f278,definition,(
% 0.10/0.50    ![X0]: (sQ22_spl <=> (~inverse(inverse(X0))=inverse(sk_c11)|~multiply(X0,sk_c9)=inverse(X0)))),
% 0.10/0.50    introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition])).
% 0.10/0.50  fof(f281,plain,(
% 0.10/0.50    ~sQ20_spl|~sQ21_spl|sQ22_spl|~sQ19_spl|~sQ11_spl),
% 0.10/0.50    inference(split_clause,[status(thm)],[f265,f272,f275,f278,f247,f173])).
% 0.10/0.50  fof(f302,definition,(
% 0.10/0.50    sQ29_spl <=> (multiply(sk_c5,inverse(sk_c5))=sk_c11)),
% 0.10/0.50    introduced(definition,[new_symbols(definition,[sQ29_spl])],[split_symbol_definition])).
% 0.10/0.50  fof(f304,plain,(
% 0.10/0.50    ~multiply(sk_c5,inverse(sk_c5))=sk_c11|sQ29_spl),
% 0.10/0.50    inference(component_clause,[status(thm)],[f302])).
% 0.10/0.50  fof(f305,definition,(
% 0.10/0.50    sQ30_spl <=> (multiply(inverse(sk_c5),sk_c10)=sk_c11)),
% 0.10/0.50    introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition])).
% 0.10/0.50  fof(f307,plain,(
% 0.10/0.50    ~multiply(inverse(sk_c5),sk_c10)=sk_c11|sQ30_spl),
% 0.10/0.50    inference(component_clause,[status(thm)],[f305])).
% 0.10/0.50  fof(f308,definition,(
% 0.10/0.50    ![X0]: (sQ31_spl <=> (~inverse(inverse(X0))=inverse(sk_c5)|~multiply(X0,sk_c8)=inverse(X0)))),
% 0.10/0.50    introduced(definition,[new_symbols(definition,[sQ31_spl])],[split_symbol_definition])).
% 0.10/0.50  fof(f311,plain,(
% 0.10/0.50    ~sQ29_spl|~sQ30_spl|sQ31_spl|~sQ19_spl|~sQ6_spl),
% 0.10/0.50    inference(split_clause,[status(thm)],[f268,f302,f305,f308,f247,f153])).
% 0.10/0.50  fof(f322,definition,(
% 0.10/0.50    sQ35_spl <=> (multiply(sk_c6,inverse(sk_c6))=sk_c11)),
% 0.10/0.50    introduced(definition,[new_symbols(definition,[sQ35_spl])],[split_symbol_definition])).
% 0.10/0.50  fof(f325,definition,(
% 0.10/0.50    sQ36_spl <=> (multiply(inverse(sk_c6),sk_c10)=sk_c11)),
% 0.10/0.50    introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition])).
% 0.10/0.50  fof(f327,plain,(
% 0.10/0.50    ~multiply(inverse(sk_c6),sk_c10)=sk_c11|sQ36_spl),
% 0.10/0.50    inference(component_clause,[status(thm)],[f325])).
% 0.10/0.50  fof(f328,definition,(
% 0.10/0.50    ![X0]: (sQ37_spl <=> (~inverse(inverse(X0))=inverse(sk_c6)|~multiply(X0,sk_c8)=inverse(X0)))),
% 0.10/0.50    introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition])).
% 0.10/0.50  fof(f331,plain,(
% 0.10/0.50    ~sQ35_spl|~sQ36_spl|sQ37_spl|~sQ19_spl|~sQ9_spl),
% 0.10/0.50    inference(split_clause,[status(thm)],[f270,f322,f325,f328,f247,f165])).
% 0.10/0.50  fof(f348,plain,(
% 0.10/0.50    ~multiply(sk_c9,sk_c10)=sk_c11|~sQ11_spl|sQ21_spl),
% 0.10/0.50    inference(forward_demodulation,[status(thm)],[f174,f277])).
% 0.10/0.50  fof(f349,plain,(
% 0.10/0.50    ~sk_c11=sk_c11|~sQ12_spl|~sQ11_spl|sQ21_spl),
% 0.10/0.50    inference(forward_demodulation,[status(thm)],[f187,f348])).
% 0.10/0.50  fof(f350,plain,(
% 0.10/0.50    $false|~sQ12_spl|~sQ11_spl|sQ21_spl),
% 0.10/0.50    inference(trivial_equality_resolution,[status(thm)],[f349])).
% 0.10/0.50  fof(f351,plain,(
% 0.10/0.50    ~sQ12_spl|~sQ11_spl|sQ21_spl),
% 0.10/0.50    inference(contradiction_clause,[status(thm)],[f350])).
% 0.10/0.50  fof(f354,plain,(
% 0.10/0.50    multiply(sk_c6,sk_c7)=identity|~sQ8_spl),
% 0.10/0.50    inference(paramodulation,[status(thm)],[f162,f66])).
% 0.10/0.50  fof(f356,plain,(
% 0.10/0.50    multiply(sk_c10,sk_c4)=identity|~sQ4_spl),
% 0.10/0.50    inference(paramodulation,[status(thm)],[f146,f66])).
% 0.10/0.50  fof(f358,plain,(
% 0.10/0.50    multiply(sk_c11,sk_c1)=identity|~sQ15_spl),
% 0.10/0.50    inference(paramodulation,[status(thm)],[f226,f66])).
% 0.10/0.50  fof(f359,plain,(
% 0.10/0.50    ![X0,X1]: (multiply(identity,X0)=multiply(inverse(X1),multiply(X1,X0)))),
% 0.10/0.50    inference(paramodulation,[status(thm)],[f66,f67])).
% 0.10/0.50  fof(f360,plain,(
% 0.10/0.50    ![X0,X1]: (X0=multiply(inverse(X1),multiply(X1,X0)))),
% 0.10/0.50    inference(forward_demodulation,[status(thm)],[f65,f359])).
% 0.10/0.50  fof(f371,plain,(
% 0.10/0.50    multiply(sk_c11,sk_c4)=multiply(sk_c9,identity)|~sQ12_spl|~sQ4_spl),
% 0.10/0.50    inference(paramodulation,[status(thm)],[f356,f253])).
% 0.10/0.50  fof(f387,plain,(
% 0.10/0.50    ~multiply(sk_c8,sk_c10)=sk_c11|~sQ9_spl|sQ36_spl),
% 0.10/0.50    inference(forward_demodulation,[status(thm)],[f166,f327])).
% 0.10/0.50  fof(f388,plain,(
% 0.10/0.50    ~sk_c11=sk_c11|~sQ7_spl|~sQ9_spl|sQ36_spl),
% 0.10/0.50    inference(forward_demodulation,[status(thm)],[f158,f387])).
% 0.10/0.50  fof(f389,plain,(
% 0.10/0.50    $false|~sQ7_spl|~sQ9_spl|sQ36_spl),
% 0.10/0.50    inference(trivial_equality_resolution,[status(thm)],[f388])).
% 0.10/0.50  fof(f390,plain,(
% 0.10/0.50    ~sQ7_spl|~sQ9_spl|sQ36_spl),
% 0.10/0.50    inference(contradiction_clause,[status(thm)],[f389])).
% 0.10/0.50  fof(f401,plain,(
% 0.10/0.50    ~multiply(sk_c8,sk_c10)=sk_c11|~sQ6_spl|sQ30_spl),
% 0.10/0.51    inference(forward_demodulation,[status(thm)],[f154,f307])).
% 0.10/0.51  fof(f402,plain,(
% 0.10/0.51    ~sk_c11=sk_c11|~sQ7_spl|~sQ6_spl|sQ30_spl),
% 0.10/0.51    inference(forward_demodulation,[status(thm)],[f158,f401])).
% 0.10/0.51  fof(f403,plain,(
% 0.10/0.51    $false|~sQ7_spl|~sQ6_spl|sQ30_spl),
% 0.10/0.51    inference(trivial_equality_resolution,[status(thm)],[f402])).
% 0.10/0.51  fof(f404,plain,(
% 0.10/0.51    ~sQ7_spl|~sQ6_spl|sQ30_spl),
% 0.10/0.51    inference(contradiction_clause,[status(thm)],[f403])).
% 0.10/0.51  fof(f406,plain,(
% 0.10/0.51    ~multiply(sk_c5,sk_c8)=sk_c11|~sQ6_spl|sQ29_spl),
% 0.10/0.51    inference(forward_demodulation,[status(thm)],[f154,f304])).
% 0.10/0.51  fof(f407,plain,(
% 0.10/0.51    ~sk_c11=sk_c11|~sQ5_spl|~sQ6_spl|sQ29_spl),
% 0.10/0.51    inference(forward_demodulation,[status(thm)],[f150,f406])).
% 0.10/0.51  fof(f408,plain,(
% 0.10/0.51    $false|~sQ5_spl|~sQ6_spl|sQ29_spl),
% 0.10/0.51    inference(trivial_equality_resolution,[status(thm)],[f407])).
% 0.10/0.51  fof(f409,plain,(
% 0.10/0.51    ~sQ5_spl|~sQ6_spl|sQ29_spl),
% 0.10/0.51    inference(contradiction_clause,[status(thm)],[f408])).
% 0.10/0.51  fof(f418,plain,(
% 0.10/0.51    sk_c7=multiply(inverse(sk_c6),identity)|~sQ8_spl),
% 0.10/0.51    inference(paramodulation,[status(thm)],[f354,f360])).
% 0.10/0.51  fof(f421,plain,(
% 0.10/0.51    ![X0]: (X0=multiply(inverse(identity),X0))),
% 0.10/0.51    inference(paramodulation,[status(thm)],[f65,f360])).
% 0.10/0.51  fof(f426,plain,(
% 0.10/0.51    sk_c11=multiply(inverse(sk_c3),sk_c10)|~sQ1_spl),
% 0.10/0.51    inference(paramodulation,[status(thm)],[f134,f360])).
% 0.10/0.51  fof(f430,plain,(
% 0.10/0.51    sk_c8=multiply(inverse(sk_c5),sk_c11)|~sQ5_spl),
% 0.10/0.51    inference(paramodulation,[status(thm)],[f150,f360])).
% 0.10/0.51  fof(f434,plain,(
% 0.10/0.51    sk_c8=multiply(inverse(sk_c7),sk_c6)|~sQ10_spl),
% 0.10/0.51    inference(paramodulation,[status(thm)],[f170,f360])).
% 0.10/0.51  fof(f438,plain,(
% 0.10/0.51    sk_c11=multiply(inverse(sk_c1),sk_c2)|~sQ14_spl),
% 0.10/0.51    inference(paramodulation,[status(thm)],[f213,f360])).
% 0.10/0.51  fof(f440,plain,(
% 0.10/0.51    sk_c7=multiply(sk_c8,identity)|~sQ9_spl|~sQ8_spl),
% 0.10/0.51    inference(forward_demodulation,[status(thm)],[f166,f418])).
% 0.10/0.51  fof(f442,plain,(
% 0.10/0.51    sk_c11=multiply(sk_c11,sk_c10)|~sQ2_spl|~sQ1_spl),
% 0.10/0.51    inference(forward_demodulation,[status(thm)],[f138,f426])).
% 0.10/0.51  fof(f446,plain,(
% 0.10/0.51    sk_c8=multiply(sk_c8,sk_c11)|~sQ6_spl|~sQ5_spl),
% 0.10/0.51    inference(forward_demodulation,[status(thm)],[f154,f430])).
% 0.10/0.51  fof(f447,plain,(
% 0.10/0.51    sk_c8=multiply(sk_c6,sk_c6)|~sQ8_spl|~sQ10_spl),
% 0.10/0.51    inference(forward_demodulation,[status(thm)],[f162,f434])).
% 0.10/0.51  fof(f448,plain,(
% 0.10/0.51    sk_c11=multiply(sk_c11,sk_c2)|~sQ15_spl|~sQ14_spl),
% 0.10/0.51    inference(forward_demodulation,[status(thm)],[f226,f438])).
% 0.10/0.51  fof(f449,plain,(
% 0.10/0.51    sk_c11=sk_c10|~sQ13_spl|~sQ15_spl|~sQ14_spl),
% 0.10/0.51    inference(forward_demodulation,[status(thm)],[f200,f448])).
% 0.10/0.51  fof(f452,plain,(
% 0.10/0.51    multiply(sk_c10,sk_c1)=identity|~sQ13_spl|~sQ14_spl|~sQ15_spl),
% 0.10/0.51    inference(backward_demodulation,[status(thm)],[f449,f358])).
% 0.10/0.51  fof(f459,plain,(
% 0.10/0.51    multiply(sk_c3,sk_c10)=sk_c10|~sQ13_spl|~sQ15_spl|~sQ14_spl|~sQ1_spl),
% 0.10/0.51    inference(backward_demodulation,[status(thm)],[f449,f134])).
% 0.10/0.51  fof(f462,plain,(
% 0.10/0.51    multiply(sk_c10,sk_c2)=sk_c10|~sQ15_spl|~sQ14_spl|~sQ13_spl),
% 0.10/0.51    inference(backward_demodulation,[status(thm)],[f449,f200])).
% 0.10/0.51  fof(f464,plain,(
% 0.10/0.51    inverse(sk_c1)=sk_c10|~sQ13_spl|~sQ14_spl|~sQ15_spl),
% 0.10/0.51    inference(backward_demodulation,[status(thm)],[f449,f226])).
% 0.10/0.51  fof(f478,plain,(
% 0.10/0.51    sk_c10=multiply(sk_c11,sk_c10)|~sQ13_spl|~sQ15_spl|~sQ14_spl|~sQ2_spl|~sQ1_spl),
% 0.10/0.51    inference(forward_demodulation,[status(thm)],[f449,f442])).
% 0.10/0.51  fof(f479,plain,(
% 0.10/0.51    sk_c10=multiply(sk_c10,sk_c10)|~sQ13_spl|~sQ15_spl|~sQ14_spl|~sQ2_spl|~sQ1_spl),
% 0.10/0.51    inference(forward_demodulation,[status(thm)],[f449,f478])).
% 0.10/0.51  fof(f481,plain,(
% 0.10/0.51    sk_c10=multiply(inverse(sk_c10),sk_c10)|~sQ13_spl|~sQ15_spl|~sQ14_spl|~sQ2_spl|~sQ1_spl),
% 0.10/0.51    inference(paramodulation,[status(thm)],[f479,f360])).
% 0.10/0.51  fof(f484,plain,(
% 0.10/0.51    sk_c10=identity|~sQ13_spl|~sQ15_spl|~sQ14_spl|~sQ2_spl|~sQ1_spl),
% 0.10/0.51    inference(forward_demodulation,[status(thm)],[f66,f481])).
% 0.10/0.51  fof(f497,plain,(
% 0.10/0.51    ![X0]: (multiply(sk_c10,X0)=X0|~sQ13_spl|~sQ15_spl|~sQ14_spl|~sQ2_spl|~sQ1_spl)),
% 0.10/0.51    inference(backward_demodulation,[status(thm)],[f484,f65])).
% 0.10/0.51  fof(f535,plain,(
% 0.10/0.51    sk_c6=multiply(inverse(sk_c6),sk_c8)|~sQ8_spl|~sQ10_spl),
% 0.10/0.51    inference(paramodulation,[status(thm)],[f447,f360])).
% 0.10/0.51  fof(f537,plain,(
% 0.10/0.51    sk_c6=multiply(sk_c8,sk_c8)|~sQ9_spl|~sQ8_spl|~sQ10_spl),
% 0.10/0.51    inference(forward_demodulation,[status(thm)],[f166,f535])).
% 0.10/0.51  fof(f624,plain,(
% 0.10/0.51    ![X0]: (~multiply(sk_c11,multiply(X0,sk_c11))=sk_c10|~inverse(X0)=sk_c11|~sQ16_spl)),
% 0.10/0.51    inference(destructive_equality_resolution,[status(thm)],[f239])).
% 0.10/0.51  fof(f626,plain,(
% 0.10/0.51    inverse(sk_c10)=sk_c9|~sQ13_spl|~sQ15_spl|~sQ14_spl|~sQ11_spl),
% 0.10/0.51    inference(forward_demodulation,[status(thm)],[f449,f174])).
% 0.10/0.51  fof(f629,plain,(
% 0.10/0.51    ![X0]: (X0=multiply(inverse(sk_c10),X0)|~sQ13_spl|~sQ15_spl|~sQ14_spl|~sQ2_spl|~sQ1_spl)),
% 0.10/0.51    inference(paramodulation,[status(thm)],[f497,f360])).
% 0.10/0.51  fof(f631,plain,(
% 0.10/0.51    ![X0]: (X0=multiply(sk_c9,X0)|~sQ11_spl|~sQ13_spl|~sQ15_spl|~sQ14_spl|~sQ2_spl|~sQ1_spl)),
% 0.10/0.51    inference(forward_demodulation,[status(thm)],[f626,f629])).
% 0.10/0.51  fof(f632,plain,(
% 0.10/0.51    ![X0]: (X0=multiply(sk_c10,multiply(sk_c1,X0))|~sQ13_spl|~sQ14_spl|~sQ15_spl)),
% 0.10/0.51    inference(paramodulation,[status(thm)],[f464,f360])).
% 0.10/0.51  fof(f633,plain,(
% 0.10/0.51    ![X0]: (X0=multiply(sk_c1,X0)|~sQ2_spl|~sQ1_spl|~sQ13_spl|~sQ14_spl|~sQ15_spl)),
% 0.10/0.51    inference(forward_demodulation,[status(thm)],[f497,f632])).
% 0.10/0.51  fof(f642,plain,(
% 0.10/0.51    sk_c2=sk_c10|~sQ2_spl|~sQ1_spl|~sQ15_spl|~sQ14_spl|~sQ13_spl),
% 0.10/0.51    inference(forward_demodulation,[status(thm)],[f497,f462])).
% 0.10/0.51  fof(f654,plain,(
% 0.10/0.51    multiply(sk_c10,sk_c10)=sk_c9|~sQ13_spl|~sQ15_spl|~sQ14_spl|~sQ0_spl),
% 0.10/0.51    inference(forward_demodulation,[status(thm)],[f449,f131])).
% 0.10/0.51  fof(f677,plain,(
% 0.10/0.51    ![X0]: (~multiply(sk_c10,multiply(X0,sk_c11))=sk_c10|~inverse(X0)=sk_c11|~sQ13_spl|~sQ15_spl|~sQ14_spl|~sQ16_spl)),
% 0.10/0.51    inference(forward_demodulation,[status(thm)],[f449,f624])).
% 0.10/0.51  fof(f678,plain,(
% 0.10/0.51    ![X0]: (~multiply(sk_c10,multiply(X0,sk_c10))=sk_c10|~inverse(X0)=sk_c11|~sQ13_spl|~sQ15_spl|~sQ14_spl|~sQ16_spl)),
% 0.10/0.51    inference(forward_demodulation,[status(thm)],[f449,f677])).
% 0.10/0.51  fof(f679,plain,(
% 0.10/0.51    ![X0]: (~multiply(sk_c10,multiply(X0,sk_c10))=sk_c10|~inverse(X0)=sk_c10|~sQ13_spl|~sQ15_spl|~sQ14_spl|~sQ16_spl)),
% 0.10/0.51    inference(forward_demodulation,[status(thm)],[f449,f678])).
% 0.10/0.51  fof(f682,plain,(
% 0.10/0.51    ~multiply(sk_c10,sk_c10)=sk_c10|~inverse(sk_c3)=sk_c10|~sQ16_spl|~sQ13_spl|~sQ15_spl|~sQ14_spl|~sQ1_spl),
% 0.10/0.51    inference(paramodulation,[status(thm)],[f459,f679])).
% 0.10/0.51  fof(f684,plain,(
% 0.10/0.51    ~multiply(sk_c10,sk_c9)=sk_c10|~inverse(sk_c10)=sk_c10|~sQ16_spl|~sQ13_spl|~sQ15_spl|~sQ14_spl|~sQ0_spl),
% 0.10/0.51    inference(paramodulation,[status(thm)],[f654,f679])).
% 0.10/0.51  fof(f686,definition,(
% 0.10/0.51    sQ41_spl <=> (multiply(sk_c10,sk_c9)=sk_c10)),
% 0.10/0.51    introduced(definition,[new_symbols(definition,[sQ41_spl])],[split_symbol_definition])).
% 0.10/0.51  fof(f688,plain,(
% 0.10/0.51    ~multiply(sk_c10,sk_c9)=sk_c10|sQ41_spl),
% 0.10/0.51    inference(component_clause,[status(thm)],[f686])).
% 0.10/0.51  fof(f690,definition,(
% 0.10/0.51    sQ42_spl <=> (multiply(sk_c10,sk_c10)=sk_c10)),
% 0.10/0.51    introduced(definition,[new_symbols(definition,[sQ42_spl])],[split_symbol_definition])).
% 0.10/0.51  fof(f692,plain,(
% 0.10/0.51    ~multiply(sk_c10,sk_c10)=sk_c10|sQ42_spl),
% 0.10/0.51    inference(component_clause,[status(thm)],[f690])).
% 0.10/0.51  fof(f697,definition,(
% 0.10/0.51    sQ44_spl <=> (inverse(sk_c3)=sk_c10)),
% 0.10/0.51    introduced(definition,[new_symbols(definition,[sQ44_spl])],[split_symbol_definition])).
% 0.10/0.51  fof(f699,plain,(
% 0.10/0.51    ~inverse(sk_c3)=sk_c10|sQ44_spl),
% 0.10/0.51    inference(component_clause,[status(thm)],[f697])).
% 0.10/0.51  fof(f700,plain,(
% 0.10/0.51    ~sQ42_spl|~sQ44_spl|~sQ16_spl|~sQ13_spl|~sQ15_spl|~sQ14_spl|~sQ1_spl),
% 0.10/0.51    inference(split_clause,[status(thm)],[f682,f690,f697,f238,f199,f225,f212,f133])).
% 0.10/0.51  fof(f708,definition,(
% 0.10/0.51    sQ47_spl <=> (inverse(sk_c10)=sk_c10)),
% 0.10/0.51    introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition])).
% 0.10/0.51  fof(f709,plain,(
% 0.10/0.51    inverse(sk_c10)=sk_c10|~sQ47_spl),
% 0.10/0.51    inference(component_clause,[status(thm)],[f708])).
% 0.10/0.51  fof(f710,plain,(
% 0.10/0.51    ~inverse(sk_c10)=sk_c10|sQ47_spl),
% 0.10/0.51    inference(component_clause,[status(thm)],[f708])).
% 0.10/0.51  fof(f711,plain,(
% 0.10/0.51    ~sQ41_spl|~sQ47_spl|~sQ16_spl|~sQ13_spl|~sQ15_spl|~sQ14_spl|~sQ0_spl),
% 0.10/0.51    inference(split_clause,[status(thm)],[f684,f686,f708,f238,f199,f225,f212,f130])).
% 0.10/0.51  fof(f712,plain,(
% 0.10/0.51    ~sk_c9=sk_c10|~sQ13_spl|~sQ15_spl|~sQ14_spl|~sQ0_spl|sQ42_spl),
% 0.10/0.51    inference(forward_demodulation,[status(thm)],[f654,f692])).
% 0.10/0.51  fof(f718,plain,(
% 0.10/0.51    ~sk_c11=sk_c10|~inverse(identity)=sk_c11|~sQ17_spl),
% 0.10/0.51    inference(paramodulation,[status(thm)],[f65,f242])).
% 0.10/0.51  fof(f721,definition,(
% 0.10/0.51    sQ48_spl <=> (sk_c11=sk_c10)),
% 0.10/0.51    introduced(definition,[new_symbols(definition,[sQ48_spl])],[split_symbol_definition])).
% 0.10/0.51  fof(f722,plain,(
% 0.10/0.51    sk_c11=sk_c10|~sQ48_spl),
% 0.10/0.51    inference(component_clause,[status(thm)],[f721])).
% 0.10/0.51  fof(f723,plain,(
% 0.10/0.51    ~sk_c11=sk_c10|sQ48_spl),
% 0.10/0.51    inference(component_clause,[status(thm)],[f721])).
% 0.10/0.51  fof(f724,definition,(
% 0.10/0.51    sQ49_spl <=> (inverse(identity)=sk_c11)),
% 0.10/0.51    introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition])).
% 0.10/0.51  fof(f725,plain,(
% 0.10/0.51    inverse(identity)=sk_c11|~sQ49_spl),
% 0.10/0.51    inference(component_clause,[status(thm)],[f724])).
% 0.10/0.51  fof(f726,plain,(
% 0.10/0.51    ~inverse(identity)=sk_c11|sQ49_spl),
% 0.10/0.51    inference(component_clause,[status(thm)],[f724])).
% 0.10/0.51  fof(f727,plain,(
% 0.10/0.51    ~sQ48_spl|~sQ49_spl|~sQ17_spl),
% 0.10/0.51    inference(split_clause,[status(thm)],[f718,f721,f724,f241])).
% 0.10/0.51  fof(f731,plain,(
% 0.10/0.51    ~sk_c11=sk_c10|~sQ2_spl|sQ44_spl),
% 0.10/0.51    inference(backward_demodulation,[status(thm)],[f138,f699])).
% 0.10/0.51  fof(f747,plain,(
% 0.10/0.51    ~inverse(sk_c4)=sk_c10|~sQ18_spl|~sQ3_spl),
% 0.10/0.51    inference(resolution,[status(thm)],[f245,f142])).
% 0.10/0.51  fof(f748,plain,(
% 0.10/0.51    ~sk_c10=sk_c9|~inverse(identity)=sk_c10|~sQ18_spl),
% 0.10/0.51    inference(paramodulation,[status(thm)],[f65,f245])).
% 0.10/0.51  fof(f752,plain,(
% 0.10/0.51    ~sQ4_spl|~sQ18_spl|~sQ3_spl),
% 0.10/0.51    inference(split_clause,[status(thm)],[f747,f145,f244,f141])).
% 0.10/0.51  fof(f753,definition,(
% 0.10/0.51    sQ50_spl <=> (sk_c10=sk_c9)),
% 0.10/0.51    introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition])).
% 0.10/0.51  fof(f754,plain,(
% 0.10/0.51    sk_c10=sk_c9|~sQ50_spl),
% 0.10/0.51    inference(component_clause,[status(thm)],[f753])).
% 0.10/0.51  fof(f755,plain,(
% 0.10/0.51    ~sk_c10=sk_c9|sQ50_spl),
% 0.10/0.51    inference(component_clause,[status(thm)],[f753])).
% 0.10/0.51  fof(f756,definition,(
% 0.10/0.51    sQ51_spl <=> (inverse(identity)=sk_c10)),
% 0.10/0.51    introduced(definition,[new_symbols(definition,[sQ51_spl])],[split_symbol_definition])).
% 0.10/0.51  fof(f758,plain,(
% 0.10/0.51    ~inverse(identity)=sk_c10|sQ51_spl),
% 0.10/0.51    inference(component_clause,[status(thm)],[f756])).
% 0.10/0.51  fof(f759,plain,(
% 0.10/0.51    ~sQ50_spl|~sQ51_spl|~sQ18_spl),
% 0.10/0.51    inference(split_clause,[status(thm)],[f748,f753,f756,f244])).
% 0.10/0.51  fof(f760,definition,(
% 0.10/0.51    sQ52_spl <=> (sk_c9=sk_c9)),
% 0.10/0.51    introduced(definition,[new_symbols(definition,[sQ52_spl])],[split_symbol_definition])).
% 0.10/0.51  fof(f762,plain,(
% 0.10/0.51    ~sk_c9=sk_c9|sQ52_spl),
% 0.10/0.51    inference(component_clause,[status(thm)],[f760])).
% 0.10/0.51  fof(f768,plain,(
% 0.10/0.51    $false|sQ52_spl),
% 0.10/0.51    inference(trivial_equality_resolution,[status(thm)],[f762])).
% 0.10/0.51  fof(f769,plain,(
% 0.10/0.51    sQ52_spl),
% 0.10/0.51    inference(contradiction_clause,[status(thm)],[f768])).
% 0.10/0.51  fof(f783,plain,(
% 0.10/0.51    sk_c10=multiply(inverse(sk_c11),sk_c9)|~sQ0_spl),
% 0.10/0.51    inference(paramodulation,[status(thm)],[f131,f360])).
% 0.10/0.51  fof(f785,plain,(
% 0.10/0.51    sk_c10=multiply(sk_c9,sk_c9)|~sQ11_spl|~sQ0_spl),
% 0.10/0.51    inference(forward_demodulation,[status(thm)],[f174,f783])).
% 0.10/0.51  fof(f789,plain,(
% 0.10/0.51    sk_c11=multiply(inverse(sk_c8),sk_c8)|~sQ6_spl|~sQ5_spl),
% 0.10/0.51    inference(paramodulation,[status(thm)],[f446,f360])).
% 0.10/0.51  fof(f791,plain,(
% 0.10/0.51    sk_c11=identity|~sQ6_spl|~sQ5_spl),
% 0.10/0.51    inference(forward_demodulation,[status(thm)],[f66,f789])).
% 0.10/0.51  fof(f793,plain,(
% 0.10/0.51    ~inverse(sk_c11)=sk_c10|~sQ6_spl|~sQ5_spl|sQ51_spl),
% 0.10/0.51    inference(backward_demodulation,[status(thm)],[f791,f758])).
% 0.10/0.51  fof(f794,plain,(
% 0.10/0.51    ![X0]: (multiply(inverse(X0),X0)=sk_c11|~sQ6_spl|~sQ5_spl)),
% 0.10/0.51    inference(backward_demodulation,[status(thm)],[f791,f66])).
% 0.10/0.51  fof(f797,plain,(
% 0.10/0.51    sk_c7=multiply(sk_c8,sk_c11)|~sQ6_spl|~sQ5_spl|~sQ9_spl|~sQ8_spl),
% 0.10/0.51    inference(backward_demodulation,[status(thm)],[f791,f440])).
% 0.10/0.51  fof(f798,plain,(
% 0.10/0.51    ![X0]: (X0=multiply(inverse(sk_c11),X0)|~sQ6_spl|~sQ5_spl)),
% 0.10/0.51    inference(backward_demodulation,[status(thm)],[f791,f421])).
% 0.10/0.51  fof(f799,plain,(
% 0.10/0.51    ~inverse(sk_c11)=sk_c11|~sQ6_spl|~sQ5_spl|sQ49_spl),
% 0.10/0.51    inference(backward_demodulation,[status(thm)],[f791,f726])).
% 0.10/0.51  fof(f800,plain,(
% 0.10/0.51    ![X0]: (multiply(sk_c11,X0)=X0|~sQ6_spl|~sQ5_spl)),
% 0.10/0.51    inference(backward_demodulation,[status(thm)],[f791,f65])).
% 0.10/0.51  fof(f801,plain,(
% 0.10/0.51    ~sk_c9=sk_c10|~sQ11_spl|~sQ6_spl|~sQ5_spl|sQ51_spl),
% 0.10/0.51    inference(forward_demodulation,[status(thm)],[f174,f793])).
% 0.10/0.51  fof(f802,plain,(
% 0.10/0.51    ![X0]: (X0=multiply(sk_c9,X0)|~sQ11_spl|~sQ6_spl|~sQ5_spl)),
% 0.10/0.51    inference(forward_demodulation,[status(thm)],[f174,f798])).
% 0.10/0.51  fof(f803,plain,(
% 0.10/0.51    ~sk_c9=sk_c11|~sQ11_spl|~sQ6_spl|~sQ5_spl|sQ49_spl),
% 0.10/0.51    inference(forward_demodulation,[status(thm)],[f174,f799])).
% 0.10/0.51  fof(f804,plain,(
% 0.10/0.51    ~sk_c10=sk_c11|~sQ11_spl|~sQ6_spl|~sQ5_spl|sQ12_spl),
% 0.10/0.51    inference(backward_demodulation,[status(thm)],[f802,f188])).
% 0.10/0.51  fof(f807,plain,(
% 0.10/0.51    sk_c10=sk_c9|~sQ6_spl|~sQ5_spl|~sQ0_spl),
% 0.10/0.51    inference(backward_demodulation,[status(thm)],[f800,f131])).
% 0.10/0.51  fof(f810,plain,(
% 0.10/0.51    $false|sQ50_spl|~sQ6_spl|~sQ5_spl|~sQ0_spl),
% 0.10/0.51    inference(forward_subsumption_resolution,[status(thm)],[f807,f755])).
% 0.10/0.51  fof(f811,plain,(
% 0.10/0.51    sQ50_spl|~sQ6_spl|~sQ5_spl|~sQ0_spl),
% 0.10/0.51    inference(contradiction_clause,[status(thm)],[f810])).
% 0.10/0.51  fof(f813,plain,(
% 0.10/0.51    ~sQ50_spl|~sQ11_spl|~sQ6_spl|~sQ5_spl|sQ51_spl),
% 0.10/0.51    inference(split_clause,[status(thm)],[f801,f753,f173,f153,f149,f756])).
% 0.10/0.51  fof(f818,plain,(
% 0.10/0.51    inverse(sk_c4)=sk_c9|~sQ6_spl|~sQ5_spl|~sQ0_spl|~sQ4_spl),
% 0.10/0.51    inference(backward_demodulation,[status(thm)],[f807,f146])).
% 0.10/0.51  fof(f825,plain,(
% 0.10/0.51    multiply(sk_c3,sk_c11)=sk_c9|~sQ6_spl|~sQ5_spl|~sQ0_spl|~sQ1_spl),
% 0.10/0.51    inference(forward_demodulation,[status(thm)],[f807,f134])).
% 0.10/0.51  fof(f826,plain,(
% 0.10/0.51    sk_c11=multiply(inverse(sk_c3),sk_c9)|~sQ6_spl|~sQ5_spl|~sQ0_spl|~sQ1_spl),
% 0.10/0.51    inference(paramodulation,[status(thm)],[f825,f360])).
% 0.10/0.51  fof(f828,plain,(
% 0.10/0.51    sk_c11=multiply(sk_c11,sk_c9)|~sQ2_spl|~sQ6_spl|~sQ5_spl|~sQ0_spl|~sQ1_spl),
% 0.10/0.51    inference(forward_demodulation,[status(thm)],[f138,f826])).
% 0.10/0.51  fof(f829,plain,(
% 0.10/0.51    sk_c11=sk_c9|~sQ2_spl|~sQ6_spl|~sQ5_spl|~sQ0_spl|~sQ1_spl),
% 0.10/0.51    inference(forward_demodulation,[status(thm)],[f800,f828])).
% 0.10/0.51  fof(f830,plain,(
% 0.10/0.51    $false|~sQ11_spl|sQ49_spl|~sQ2_spl|~sQ6_spl|~sQ5_spl|~sQ0_spl|~sQ1_spl),
% 0.10/0.51    inference(forward_subsumption_resolution,[status(thm)],[f829,f803])).
% 0.10/0.51  fof(f831,plain,(
% 0.10/0.51    ~sQ11_spl|sQ49_spl|~sQ2_spl|~sQ6_spl|~sQ5_spl|~sQ0_spl|~sQ1_spl),
% 0.10/0.51    inference(contradiction_clause,[status(thm)],[f830])).
% 0.10/0.51  fof(f834,plain,(
% 0.10/0.51    inverse(sk_c11)=sk_c11|~sQ6_spl|~sQ5_spl|~sQ49_spl),
% 0.10/0.51    inference(forward_demodulation,[status(thm)],[f791,f725])).
% 0.10/0.51  fof(f835,plain,(
% 0.10/0.51    sk_c9=sk_c11|~sQ11_spl|~sQ6_spl|~sQ5_spl|~sQ49_spl),
% 0.10/0.51    inference(forward_demodulation,[status(thm)],[f174,f834])).
% 0.10/0.51  fof(f836,plain,(
% 0.10/0.51    sk_c8=multiply(inverse(sk_c5),sk_c11)|~sQ5_spl),
% 0.10/0.51    inference(paramodulation,[status(thm)],[f150,f360])).
% 0.10/0.51  fof(f843,plain,(
% 0.10/0.51    sk_c9=identity|~sQ2_spl|~sQ0_spl|~sQ1_spl|~sQ6_spl|~sQ5_spl),
% 0.10/0.51    inference(backward_demodulation,[status(thm)],[f829,f791])).
% 0.10/0.51  fof(f851,plain,(
% 0.10/0.51    ~sQ48_spl|~sQ11_spl|~sQ6_spl|~sQ5_spl|sQ12_spl),
% 0.10/0.51    inference(split_clause,[status(thm)],[f804,f721,f173,f153,f149,f186])).
% 0.10/0.51  fof(f852,plain,(
% 0.10/0.51    ~sQ48_spl|~sQ2_spl|sQ44_spl),
% 0.10/0.51    inference(split_clause,[status(thm)],[f731,f721,f137,f697])).
% 0.10/0.51  fof(f859,plain,(
% 0.10/0.51    multiply(sk_c9,sk_c4)=multiply(sk_c9,identity)|~sQ2_spl|~sQ6_spl|~sQ5_spl|~sQ0_spl|~sQ1_spl|~sQ12_spl|~sQ4_spl),
% 0.10/0.51    inference(forward_demodulation,[status(thm)],[f829,f371])).
% 0.10/0.51  fof(f860,plain,(
% 0.10/0.51    sk_c4=multiply(sk_c9,identity)|~sQ11_spl|~sQ2_spl|~sQ6_spl|~sQ5_spl|~sQ0_spl|~sQ1_spl|~sQ12_spl|~sQ4_spl),
% 0.10/0.51    inference(forward_demodulation,[status(thm)],[f802,f859])).
% 0.10/0.51  fof(f861,plain,(
% 0.10/0.51    sk_c4=identity|~sQ11_spl|~sQ2_spl|~sQ6_spl|~sQ5_spl|~sQ0_spl|~sQ1_spl|~sQ12_spl|~sQ4_spl),
% 0.10/0.51    inference(forward_demodulation,[status(thm)],[f802,f860])).
% 0.10/0.51  fof(f868,plain,(
% 0.10/0.51    ![X0]: (~multiply(sk_c9,multiply(X0,sk_c11))=sk_c10|~inverse(X0)=sk_c11|~sQ2_spl|~sQ6_spl|~sQ5_spl|~sQ0_spl|~sQ1_spl|~sQ16_spl)),
% 0.10/0.51    inference(forward_demodulation,[status(thm)],[f829,f624])).
% 0.10/0.51  fof(f869,plain,(
% 0.10/0.51    ![X0]: (~multiply(X0,sk_c11)=sk_c10|~inverse(X0)=sk_c11|~sQ11_spl|~sQ2_spl|~sQ6_spl|~sQ5_spl|~sQ0_spl|~sQ1_spl|~sQ16_spl)),
% 0.10/0.51    inference(forward_demodulation,[status(thm)],[f802,f868])).
% 0.10/0.51  fof(f870,plain,(
% 0.10/0.51    ![X0]: (~multiply(X0,sk_c9)=sk_c10|~inverse(X0)=sk_c11|~sQ11_spl|~sQ2_spl|~sQ6_spl|~sQ5_spl|~sQ0_spl|~sQ1_spl|~sQ16_spl)),
% 0.10/0.51    inference(forward_demodulation,[status(thm)],[f829,f869])).
% 0.10/0.51  fof(f871,plain,(
% 0.10/0.51    ![X0]: (~multiply(X0,sk_c9)=sk_c9|~inverse(X0)=sk_c11|~sQ11_spl|~sQ2_spl|~sQ6_spl|~sQ5_spl|~sQ0_spl|~sQ1_spl|~sQ16_spl)),
% 0.10/0.51    inference(forward_demodulation,[status(thm)],[f807,f870])).
% 0.10/0.51  fof(f872,plain,(
% 0.10/0.51    ![X0]: (~multiply(X0,sk_c9)=sk_c9|~inverse(X0)=sk_c9|~sQ11_spl|~sQ2_spl|~sQ6_spl|~sQ5_spl|~sQ0_spl|~sQ1_spl|~sQ16_spl)),
% 0.10/0.51    inference(forward_demodulation,[status(thm)],[f829,f871])).
% 0.10/0.51  fof(f877,plain,(
% 0.10/0.51    sk_c9=sk_c4|~sQ11_spl|~sQ12_spl|~sQ4_spl|~sQ2_spl|~sQ0_spl|~sQ1_spl|~sQ6_spl|~sQ5_spl),
% 0.10/0.51    inference(backward_demodulation,[status(thm)],[f861,f843])).
% 0.10/0.51  fof(f878,plain,(
% 0.10/0.51    sk_c11=sk_c4|~sQ11_spl|~sQ12_spl|~sQ4_spl|~sQ2_spl|~sQ6_spl|~sQ5_spl|~sQ0_spl|~sQ1_spl),
% 0.10/0.51    inference(backward_demodulation,[status(thm)],[f877,f829])).
% 0.10/0.51  fof(f879,plain,(
% 0.10/0.51    sk_c10=sk_c4|~sQ11_spl|~sQ12_spl|~sQ4_spl|~sQ2_spl|~sQ1_spl|~sQ6_spl|~sQ5_spl|~sQ0_spl),
% 0.10/0.51    inference(backward_demodulation,[status(thm)],[f877,f807])).
% 0.10/0.51  fof(f880,plain,(
% 0.10/0.51    ![X0]: (X0=multiply(sk_c4,X0)|~sQ12_spl|~sQ4_spl|~sQ2_spl|~sQ0_spl|~sQ1_spl|~sQ11_spl|~sQ6_spl|~sQ5_spl)),
% 0.10/0.51    inference(backward_demodulation,[status(thm)],[f877,f802])).
% 0.10/0.51  fof(f881,plain,(
% 0.10/0.51    inverse(sk_c4)=sk_c4|~sQ11_spl|~sQ12_spl|~sQ2_spl|~sQ1_spl|~sQ6_spl|~sQ5_spl|~sQ0_spl|~sQ4_spl),
% 0.10/0.51    inference(forward_demodulation,[status(thm)],[f877,f818])).
% 0.10/0.51  fof(f895,plain,(
% 0.10/0.51    multiply(sk_c8,sk_c4)=sk_c11|~sQ11_spl|~sQ12_spl|~sQ4_spl|~sQ2_spl|~sQ1_spl|~sQ6_spl|~sQ5_spl|~sQ0_spl|~sQ7_spl),
% 0.10/0.51    inference(forward_demodulation,[status(thm)],[f879,f158])).
% 0.10/0.51  fof(f896,plain,(
% 0.10/0.51    multiply(sk_c8,sk_c4)=sk_c4|~sQ11_spl|~sQ12_spl|~sQ4_spl|~sQ2_spl|~sQ1_spl|~sQ6_spl|~sQ5_spl|~sQ0_spl|~sQ7_spl),
% 0.10/0.51    inference(forward_demodulation,[status(thm)],[f878,f895])).
% 0.10/0.51  fof(f898,plain,(
% 0.10/0.51    ![X0]: (multiply(sk_c4,X0)=multiply(sk_c8,multiply(sk_c4,X0))|~sQ11_spl|~sQ12_spl|~sQ4_spl|~sQ2_spl|~sQ1_spl|~sQ6_spl|~sQ5_spl|~sQ0_spl|~sQ7_spl)),
% 0.10/0.51    inference(paramodulation,[status(thm)],[f896,f67])).
% 0.10/0.51  fof(f899,plain,(
% 0.10/0.51    ![X0]: (X0=multiply(sk_c8,multiply(sk_c4,X0))|~sQ11_spl|~sQ12_spl|~sQ4_spl|~sQ2_spl|~sQ1_spl|~sQ6_spl|~sQ5_spl|~sQ0_spl|~sQ7_spl)),
% 0.10/0.51    inference(forward_demodulation,[status(thm)],[f880,f898])).
% 0.10/0.51  fof(f900,plain,(
% 0.10/0.51    ![X0]: (X0=multiply(sk_c8,X0)|~sQ11_spl|~sQ12_spl|~sQ4_spl|~sQ2_spl|~sQ1_spl|~sQ6_spl|~sQ5_spl|~sQ0_spl|~sQ7_spl)),
% 0.10/0.51    inference(forward_demodulation,[status(thm)],[f880,f899])).
% 0.10/0.51  fof(f901,plain,(
% 0.10/0.51    multiply(sk_c4,sk_c2)=sk_c10|~sQ11_spl|~sQ12_spl|~sQ4_spl|~sQ2_spl|~sQ6_spl|~sQ5_spl|~sQ0_spl|~sQ1_spl|~sQ13_spl),
% 0.10/0.51    inference(forward_demodulation,[status(thm)],[f878,f200])).
% 0.10/0.51  fof(f902,plain,(
% 0.10/0.51    sk_c2=sk_c4|~sQ13_spl|~sQ11_spl|~sQ12_spl|~sQ4_spl|~sQ2_spl|~sQ1_spl|~sQ6_spl|~sQ5_spl|~sQ0_spl),
% 0.10/0.51    inference(backward_demodulation,[status(thm)],[f903,f879])).
% 0.10/0.51  fof(f903,plain,(
% 0.10/0.51    sk_c2=sk_c10|~sQ11_spl|~sQ12_spl|~sQ4_spl|~sQ2_spl|~sQ6_spl|~sQ5_spl|~sQ0_spl|~sQ1_spl|~sQ13_spl),
% 0.10/0.51    inference(forward_demodulation,[status(thm)],[f880,f901])).
% 0.10/0.51  fof(f913,plain,(
% 0.10/0.51    inverse(sk_c4)=sk_c2|~sQ13_spl|~sQ11_spl|~sQ12_spl|~sQ2_spl|~sQ1_spl|~sQ6_spl|~sQ5_spl|~sQ0_spl|~sQ4_spl),
% 0.10/0.51    inference(backward_demodulation,[status(thm)],[f902,f881])).
% 0.10/0.51  fof(f914,plain,(
% 0.10/0.51    sk_c11=sk_c2|~sQ13_spl|~sQ11_spl|~sQ12_spl|~sQ4_spl|~sQ2_spl|~sQ6_spl|~sQ5_spl|~sQ0_spl|~sQ1_spl),
% 0.10/0.51    inference(backward_demodulation,[status(thm)],[f902,f878])).
% 0.10/0.51  fof(f915,plain,(
% 0.10/0.51    sk_c9=sk_c2|~sQ13_spl|~sQ11_spl|~sQ12_spl|~sQ4_spl|~sQ2_spl|~sQ0_spl|~sQ1_spl|~sQ6_spl|~sQ5_spl),
% 0.10/0.51    inference(backward_demodulation,[status(thm)],[f902,f877])).
% 0.10/0.51  fof(f916,plain,(
% 0.10/0.51    sk_c2=identity|~sQ13_spl|~sQ11_spl|~sQ2_spl|~sQ6_spl|~sQ5_spl|~sQ0_spl|~sQ1_spl|~sQ12_spl|~sQ4_spl),
% 0.10/0.51    inference(backward_demodulation,[status(thm)],[f902,f861])).
% 0.10/0.51  fof(f918,plain,(
% 0.10/0.51    inverse(sk_c2)=sk_c2|~sQ13_spl|~sQ11_spl|~sQ12_spl|~sQ2_spl|~sQ1_spl|~sQ6_spl|~sQ5_spl|~sQ0_spl|~sQ4_spl),
% 0.10/0.51    inference(forward_demodulation,[status(thm)],[f902,f913])).
% 0.10/0.51  fof(f922,plain,(
% 0.10/0.51    ![X0]: (multiply(inverse(X0),X0)=sk_c2|~sQ13_spl|~sQ11_spl|~sQ12_spl|~sQ4_spl|~sQ2_spl|~sQ0_spl|~sQ1_spl|~sQ6_spl|~sQ5_spl)),
% 0.10/0.51    inference(forward_demodulation,[status(thm)],[f914,f794])).
% 0.10/0.51  fof(f929,plain,(
% 0.10/0.51    sk_c6=sk_c8|~sQ11_spl|~sQ12_spl|~sQ4_spl|~sQ2_spl|~sQ1_spl|~sQ6_spl|~sQ5_spl|~sQ0_spl|~sQ7_spl|~sQ9_spl|~sQ8_spl|~sQ10_spl),
% 0.10/0.51    inference(backward_demodulation,[status(thm)],[f900,f537])).
% 0.10/0.51  fof(f933,plain,(
% 0.10/0.51    inverse(sk_c5)=sk_c6|~sQ11_spl|~sQ12_spl|~sQ4_spl|~sQ2_spl|~sQ1_spl|~sQ5_spl|~sQ0_spl|~sQ7_spl|~sQ9_spl|~sQ8_spl|~sQ10_spl|~sQ6_spl),
% 0.10/0.51    inference(backward_demodulation,[status(thm)],[f929,f154])).
% 0.10/0.51  fof(f992,plain,(
% 0.10/0.51    ![X0]: (~multiply(X0,sk_c2)=sk_c9|~inverse(X0)=sk_c9|~sQ13_spl|~sQ12_spl|~sQ4_spl|~sQ11_spl|~sQ2_spl|~sQ6_spl|~sQ5_spl|~sQ0_spl|~sQ1_spl|~sQ16_spl)),
% 0.10/0.51    inference(forward_demodulation,[status(thm)],[f915,f872])).
% 0.10/0.51  fof(f993,plain,(
% 0.10/0.51    ![X0]: (~multiply(X0,sk_c2)=sk_c2|~inverse(X0)=sk_c9|~sQ13_spl|~sQ12_spl|~sQ4_spl|~sQ11_spl|~sQ2_spl|~sQ6_spl|~sQ5_spl|~sQ0_spl|~sQ1_spl|~sQ16_spl)),
% 0.10/0.51    inference(forward_demodulation,[status(thm)],[f915,f992])).
% 0.10/0.51  fof(f994,plain,(
% 0.10/0.51    ![X0]: (~multiply(X0,sk_c2)=sk_c2|~inverse(X0)=sk_c2|~sQ13_spl|~sQ12_spl|~sQ4_spl|~sQ11_spl|~sQ2_spl|~sQ6_spl|~sQ5_spl|~sQ0_spl|~sQ1_spl|~sQ16_spl)),
% 0.10/0.51    inference(forward_demodulation,[status(thm)],[f915,f993])).
% 0.10/0.51  fof(f995,plain,(
% 0.10/0.51    ~inverse(inverse(sk_c2))=sk_c2|~sQ16_spl|~sQ13_spl|~sQ11_spl|~sQ12_spl|~sQ4_spl|~sQ2_spl|~sQ0_spl|~sQ1_spl|~sQ6_spl|~sQ5_spl),
% 0.10/0.51    inference(resolution,[status(thm)],[f994,f922])).
% 0.10/0.51  fof(f1000,plain,(
% 0.10/0.51    ~inverse(sk_c2)=sk_c2|~sQ16_spl|~sQ13_spl|~sQ11_spl|~sQ12_spl|~sQ4_spl|~sQ2_spl|~sQ0_spl|~sQ1_spl|~sQ6_spl|~sQ5_spl),
% 0.10/0.51    inference(forward_demodulation,[status(thm)],[f918,f995])).
% 0.10/0.51  fof(f1001,plain,(
% 0.10/0.51    ~sk_c2=sk_c2|~sQ16_spl|~sQ13_spl|~sQ11_spl|~sQ12_spl|~sQ4_spl|~sQ2_spl|~sQ0_spl|~sQ1_spl|~sQ6_spl|~sQ5_spl),
% 0.10/0.51    inference(forward_demodulation,[status(thm)],[f918,f1000])).
% 0.10/0.51  fof(f1002,plain,(
% 0.10/0.51    $false|~sQ16_spl|~sQ13_spl|~sQ11_spl|~sQ12_spl|~sQ4_spl|~sQ2_spl|~sQ0_spl|~sQ1_spl|~sQ6_spl|~sQ5_spl),
% 0.10/0.51    inference(trivial_equality_resolution,[status(thm)],[f1001])).
% 0.10/0.51  fof(f1003,plain,(
% 0.10/0.51    ~sQ16_spl|~sQ13_spl|~sQ11_spl|~sQ12_spl|~sQ4_spl|~sQ2_spl|~sQ0_spl|~sQ1_spl|~sQ6_spl|~sQ5_spl),
% 0.10/0.51    inference(contradiction_clause,[status(thm)],[f1002])).
% 0.10/0.51  fof(f1004,plain,(
% 0.10/0.51    sQ48_spl|~sQ13_spl|~sQ15_spl|~sQ14_spl),
% 0.10/0.51    inference(split_clause,[status(thm)],[f449,f721,f199,f225,f212])).
% 0.10/0.51  fof(f1006,plain,(
% 0.10/0.51    sk_c2=identity|~sQ13_spl|~sQ15_spl|~sQ14_spl|~sQ2_spl|~sQ1_spl),
% 0.10/0.51    inference(backward_demodulation,[status(thm)],[f642,f484])).
% 0.10/0.51  fof(f1007,plain,(
% 0.10/0.51    ~sk_c9=sk_c2|~sQ2_spl|~sQ1_spl|~sQ13_spl|~sQ15_spl|~sQ14_spl|~sQ0_spl|sQ42_spl),
% 0.10/0.51    inference(backward_demodulation,[status(thm)],[f642,f712])).
% 0.10/0.51  fof(f1011,plain,(
% 0.10/0.51    sk_c11=sk_c2|~sQ2_spl|~sQ1_spl|~sQ15_spl|~sQ14_spl|~sQ13_spl|~sQ48_spl),
% 0.10/0.51    inference(forward_demodulation,[status(thm)],[f642,f722])).
% 0.10/0.51  fof(f1015,plain,(
% 0.10/0.51    inverse(sk_c2)=sk_c9|~sQ2_spl|~sQ1_spl|~sQ15_spl|~sQ14_spl|~sQ13_spl|~sQ48_spl|~sQ11_spl),
% 0.10/0.51    inference(forward_demodulation,[status(thm)],[f1011,f174])).
% 0.10/0.51  fof(f1031,plain,(
% 0.10/0.51    ![X0]: (multiply(sk_c2,X0)=X0|~sQ13_spl|~sQ15_spl|~sQ14_spl|~sQ2_spl|~sQ1_spl)),
% 0.10/0.51    inference(forward_demodulation,[status(thm)],[f1006,f65])).
% 0.10/0.51  fof(f1036,plain,(
% 0.10/0.51    inverse(sk_c1)=sk_c2|~sQ2_spl|~sQ1_spl|~sQ13_spl|~sQ14_spl|~sQ15_spl),
% 0.10/0.51    inference(forward_demodulation,[status(thm)],[f642,f464])).
% 0.10/0.51  fof(f1057,plain,(
% 0.10/0.51    sk_c2=multiply(sk_c9,sk_c9)|~sQ2_spl|~sQ1_spl|~sQ15_spl|~sQ14_spl|~sQ13_spl|~sQ11_spl|~sQ0_spl),
% 0.10/0.51    inference(forward_demodulation,[status(thm)],[f642,f785])).
% 0.10/0.51  fof(f1058,plain,(
% 0.10/0.51    sk_c2=sk_c9|~sQ2_spl|~sQ1_spl|~sQ15_spl|~sQ14_spl|~sQ13_spl|~sQ11_spl|~sQ0_spl),
% 0.10/0.51    inference(forward_demodulation,[status(thm)],[f631,f1057])).
% 0.10/0.51  fof(f1059,plain,(
% 0.10/0.51    $false|sQ42_spl|~sQ2_spl|~sQ1_spl|~sQ15_spl|~sQ14_spl|~sQ13_spl|~sQ11_spl|~sQ0_spl),
% 0.10/0.51    inference(forward_subsumption_resolution,[status(thm)],[f1058,f1007])).
% 0.10/0.51  fof(f1060,plain,(
% 0.10/0.51    sQ42_spl|~sQ2_spl|~sQ1_spl|~sQ15_spl|~sQ14_spl|~sQ13_spl|~sQ11_spl|~sQ0_spl),
% 0.10/0.51    inference(contradiction_clause,[status(thm)],[f1059])).
% 0.10/0.51  fof(f1068,plain,(
% 0.10/0.51    multiply(sk_c2,sk_c10)=sk_c9|~sQ2_spl|~sQ1_spl|~sQ15_spl|~sQ14_spl|~sQ13_spl|~sQ48_spl|~sQ0_spl),
% 0.10/0.51    inference(forward_demodulation,[status(thm)],[f1011,f131])).
% 0.10/0.51  fof(f1069,plain,(
% 0.10/0.51    sk_c10=sk_c9|~sQ2_spl|~sQ1_spl|~sQ15_spl|~sQ14_spl|~sQ13_spl|~sQ48_spl|~sQ0_spl),
% 0.10/0.51    inference(forward_demodulation,[status(thm)],[f1031,f1068])).
% 0.10/0.51  fof(f1072,plain,(
% 0.10/0.51    inverse(sk_c2)=sk_c2|~sQ0_spl|~sQ2_spl|~sQ1_spl|~sQ15_spl|~sQ14_spl|~sQ13_spl|~sQ48_spl|~sQ11_spl),
% 0.10/0.51    inference(backward_demodulation,[status(thm)],[f1073,f1015])).
% 0.10/0.51  fof(f1073,plain,(
% 0.10/0.51    sk_c2=sk_c9|~sQ2_spl|~sQ1_spl|~sQ15_spl|~sQ14_spl|~sQ13_spl|~sQ48_spl|~sQ0_spl),
% 0.10/0.51    inference(forward_demodulation,[status(thm)],[f642,f1069])).
% 0.10/0.51  fof(f1094,plain,(
% 0.10/0.51    sk_c11=multiply(inverse(sk_c3),sk_c10)|~sQ1_spl),
% 0.10/0.51    inference(paramodulation,[status(thm)],[f134,f360])).
% 0.55/0.51  fof(f1096,plain,(
% 0.55/0.51    sk_c11=multiply(sk_c11,sk_c10)|~sQ2_spl|~sQ1_spl),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f138,f1094])).
% 0.55/0.51  fof(f1097,plain,(
% 0.55/0.51    sk_c11=sk_c10|~sQ6_spl|~sQ5_spl|~sQ2_spl|~sQ1_spl),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f800,f1096])).
% 0.55/0.51  fof(f1098,plain,(
% 0.55/0.51    $false|sQ48_spl|~sQ6_spl|~sQ5_spl|~sQ2_spl|~sQ1_spl),
% 0.55/0.51    inference(forward_subsumption_resolution,[status(thm)],[f1097,f723])).
% 0.55/0.51  fof(f1099,plain,(
% 0.55/0.51    sQ48_spl|~sQ6_spl|~sQ5_spl|~sQ2_spl|~sQ1_spl),
% 0.55/0.51    inference(contradiction_clause,[status(thm)],[f1098])).
% 0.55/0.51  fof(f1109,plain,(
% 0.55/0.51    multiply(sk_c3,sk_c11)=sk_c9|~sQ50_spl|~sQ1_spl),
% 0.55/0.51    inference(backward_demodulation,[status(thm)],[f754,f134])).
% 0.55/0.51  fof(f1113,plain,(
% 0.55/0.51    inverse(sk_c4)=sk_c9|~sQ50_spl|~sQ4_spl),
% 0.55/0.51    inference(backward_demodulation,[status(thm)],[f754,f146])).
% 0.55/0.51  fof(f1114,plain,(
% 0.55/0.51    ~inverse(sk_c10)=sk_c9|~sQ50_spl|sQ47_spl),
% 0.55/0.51    inference(backward_demodulation,[status(thm)],[f754,f710])).
% 0.55/0.51  fof(f1116,plain,(
% 0.55/0.51    ~inverse(sk_c9)=sk_c9|~sQ50_spl|sQ47_spl),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f754,f1114])).
% 0.55/0.51  fof(f1119,plain,(
% 0.55/0.51    ~inverse(sk_c9)=sk_c9|~sQ50_spl|~sQ6_spl|~sQ5_spl|~sQ2_spl|~sQ1_spl|sQ11_spl),
% 0.55/0.51    inference(backward_demodulation,[status(thm)],[f1123,f175])).
% 0.55/0.51  fof(f1120,plain,(
% 0.55/0.51    inverse(sk_c3)=sk_c9|~sQ50_spl|~sQ6_spl|~sQ5_spl|~sQ1_spl|~sQ2_spl),
% 0.55/0.51    inference(backward_demodulation,[status(thm)],[f1123,f138])).
% 0.55/0.51  fof(f1123,plain,(
% 0.55/0.51    sk_c11=sk_c9|~sQ50_spl|~sQ6_spl|~sQ5_spl|~sQ2_spl|~sQ1_spl),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f754,f1097])).
% 0.55/0.51  fof(f1125,plain,(
% 0.55/0.51    ![X0]: (multiply(sk_c9,X0)=X0|~sQ2_spl|~sQ0_spl|~sQ1_spl|~sQ6_spl|~sQ5_spl)),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f843,f65])).
% 0.55/0.51  fof(f1136,plain,(
% 0.55/0.51    ![X0]: (multiply(inverse(X0),X0)=sk_c9|~sQ2_spl|~sQ0_spl|~sQ1_spl|~sQ6_spl|~sQ5_spl)),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f843,f66])).
% 0.55/0.51  fof(f1137,plain,(
% 0.55/0.51    multiply(sk_c9,sk_c4)=sk_c9|~sQ2_spl|~sQ1_spl|~sQ6_spl|~sQ5_spl|~sQ0_spl|~sQ4_spl),
% 0.55/0.51    inference(paramodulation,[status(thm)],[f818,f1136])).
% 0.55/0.51  fof(f1144,plain,(
% 0.55/0.51    sk_c4=sk_c9|~sQ2_spl|~sQ1_spl|~sQ6_spl|~sQ5_spl|~sQ0_spl|~sQ4_spl),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f1125,f1137])).
% 0.55/0.51  fof(f1153,plain,(
% 0.55/0.51    ![X0]: (multiply(inverse(X0),X0)=sk_c4|~sQ4_spl|~sQ2_spl|~sQ0_spl|~sQ1_spl|~sQ6_spl|~sQ5_spl)),
% 0.55/0.51    inference(backward_demodulation,[status(thm)],[f1144,f1136])).
% 0.55/0.51  fof(f1180,plain,(
% 0.55/0.51    inverse(sk_c4)=sk_c4|~sQ2_spl|~sQ1_spl|~sQ6_spl|~sQ5_spl|~sQ0_spl|~sQ50_spl|~sQ4_spl),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f1144,f1113])).
% 0.55/0.51  fof(f1183,plain,(
% 0.55/0.51    ~inverse(sk_c4)=sk_c9|~sQ2_spl|~sQ1_spl|~sQ6_spl|~sQ5_spl|~sQ0_spl|~sQ4_spl|~sQ50_spl|sQ47_spl),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f1144,f1116])).
% 0.55/0.51  fof(f1184,plain,(
% 0.55/0.51    ~sk_c4=sk_c9|~sQ2_spl|~sQ1_spl|~sQ6_spl|~sQ5_spl|~sQ0_spl|~sQ4_spl|~sQ50_spl|sQ47_spl),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f1180,f1183])).
% 0.55/0.51  fof(f1185,plain,(
% 0.55/0.51    ~sk_c4=sk_c4|~sQ2_spl|~sQ1_spl|~sQ6_spl|~sQ5_spl|~sQ0_spl|~sQ4_spl|~sQ50_spl|sQ47_spl),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f1144,f1184])).
% 0.55/0.51  fof(f1186,plain,(
% 0.55/0.51    $false|~sQ2_spl|~sQ1_spl|~sQ6_spl|~sQ5_spl|~sQ0_spl|~sQ4_spl|~sQ50_spl|sQ47_spl),
% 0.55/0.51    inference(trivial_equality_resolution,[status(thm)],[f1185])).
% 0.55/0.51  fof(f1187,plain,(
% 0.55/0.51    ~sQ2_spl|~sQ1_spl|~sQ6_spl|~sQ5_spl|~sQ0_spl|~sQ4_spl|~sQ50_spl|sQ47_spl),
% 0.55/0.51    inference(contradiction_clause,[status(thm)],[f1186])).
% 0.55/0.51  fof(f1202,plain,(
% 0.55/0.51    sk_c10=identity|~sQ48_spl|~sQ6_spl|~sQ5_spl),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f722,f791])).
% 0.55/0.51  fof(f1207,plain,(
% 0.55/0.51    ![X0]: (multiply(sk_c10,X0)=X0|~sQ48_spl|~sQ6_spl|~sQ5_spl)),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f722,f800])).
% 0.55/0.51  fof(f1211,plain,(
% 0.55/0.51    inverse(sk_c3)=sk_c10|~sQ48_spl|~sQ2_spl),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f722,f138])).
% 0.55/0.51  fof(f1212,plain,(
% 0.55/0.51    ![X0]: (X0=multiply(sk_c10,multiply(sk_c3,X0))|~sQ48_spl|~sQ2_spl)),
% 0.55/0.51    inference(paramodulation,[status(thm)],[f1211,f360])).
% 0.55/0.51  fof(f1213,plain,(
% 0.55/0.51    ![X0]: (X0=multiply(sk_c3,X0)|~sQ6_spl|~sQ5_spl|~sQ48_spl|~sQ2_spl)),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f1207,f1212])).
% 0.55/0.51  fof(f1214,plain,(
% 0.55/0.51    ![X0]: (X0=multiply(sk_c10,multiply(sk_c4,X0))|~sQ4_spl)),
% 0.55/0.51    inference(paramodulation,[status(thm)],[f146,f360])).
% 0.55/0.51  fof(f1215,plain,(
% 0.55/0.51    ![X0]: (X0=multiply(sk_c4,X0)|~sQ48_spl|~sQ6_spl|~sQ5_spl|~sQ4_spl)),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f1207,f1214])).
% 0.55/0.51  fof(f1220,plain,(
% 0.55/0.51    sk_c10=sk_c9|~sQ48_spl|~sQ6_spl|~sQ5_spl|~sQ4_spl|~sQ3_spl),
% 0.55/0.51    inference(backward_demodulation,[status(thm)],[f1215,f142])).
% 0.55/0.51  fof(f1223,plain,(
% 0.55/0.51    sQ50_spl|~sQ48_spl|~sQ6_spl|~sQ5_spl|~sQ4_spl|~sQ3_spl),
% 0.55/0.51    inference(split_clause,[status(thm)],[f1220,f753,f721,f153,f149,f145,f141])).
% 0.55/0.51  fof(f1225,plain,(
% 0.55/0.51    sk_c11=sk_c9|~sQ6_spl|~sQ5_spl|~sQ48_spl|~sQ2_spl|~sQ50_spl|~sQ1_spl),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f1213,f1109])).
% 0.55/0.51  fof(f1231,plain,(
% 0.55/0.51    ![X0]: (multiply(inverse(X0),X0)=sk_c9|~sQ48_spl|~sQ2_spl|~sQ50_spl|~sQ1_spl|~sQ6_spl|~sQ5_spl)),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f1225,f794])).
% 0.55/0.51  fof(f1232,plain,(
% 0.55/0.51    multiply(sk_c10,sk_c4)=sk_c9|~sQ48_spl|~sQ2_spl|~sQ50_spl|~sQ1_spl|~sQ6_spl|~sQ5_spl|~sQ4_spl),
% 0.55/0.51    inference(paramodulation,[status(thm)],[f146,f1231])).
% 0.55/0.51  fof(f1233,plain,(
% 0.55/0.51    multiply(sk_c10,sk_c3)=sk_c9|~sQ50_spl|~sQ1_spl|~sQ6_spl|~sQ5_spl|~sQ48_spl|~sQ2_spl),
% 0.55/0.51    inference(paramodulation,[status(thm)],[f1211,f1231])).
% 0.55/0.51  fof(f1239,plain,(
% 0.55/0.51    sk_c4=sk_c9|~sQ48_spl|~sQ2_spl|~sQ50_spl|~sQ1_spl|~sQ6_spl|~sQ5_spl|~sQ4_spl),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f1207,f1232])).
% 0.55/0.51  fof(f1240,plain,(
% 0.55/0.51    sk_c3=sk_c9|~sQ50_spl|~sQ1_spl|~sQ6_spl|~sQ5_spl|~sQ48_spl|~sQ2_spl),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f1207,f1233])).
% 0.55/0.51  fof(f1242,plain,(
% 0.55/0.51    sk_c11=sk_c10|~sQ6_spl|~sQ5_spl|~sQ48_spl|~sQ2_spl|~sQ1_spl),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f1213,f134])).
% 0.55/0.51  fof(f1249,plain,(
% 0.55/0.51    sk_c9=identity|~sQ50_spl|~sQ2_spl|~sQ1_spl|~sQ48_spl|~sQ6_spl|~sQ5_spl),
% 0.55/0.51    inference(backward_demodulation,[status(thm)],[f1251,f1202])).
% 0.55/0.51  fof(f1251,plain,(
% 0.55/0.51    sk_c9=sk_c10|~sQ50_spl|~sQ6_spl|~sQ5_spl|~sQ48_spl|~sQ2_spl|~sQ1_spl),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f1225,f1242])).
% 0.55/0.51  fof(f1254,plain,(
% 0.55/0.51    sk_c4=sk_c10|~sQ4_spl|~sQ50_spl|~sQ6_spl|~sQ5_spl|~sQ48_spl|~sQ2_spl|~sQ1_spl),
% 0.55/0.51    inference(backward_demodulation,[status(thm)],[f1239,f1251])).
% 0.55/0.51  fof(f1256,plain,(
% 0.55/0.51    sk_c11=sk_c4|~sQ4_spl|~sQ6_spl|~sQ5_spl|~sQ48_spl|~sQ2_spl|~sQ50_spl|~sQ1_spl),
% 0.55/0.51    inference(backward_demodulation,[status(thm)],[f1239,f1225])).
% 0.55/0.51  fof(f1258,plain,(
% 0.55/0.51    sk_c3=sk_c4|~sQ4_spl|~sQ50_spl|~sQ1_spl|~sQ6_spl|~sQ5_spl|~sQ48_spl|~sQ2_spl),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f1239,f1240])).
% 0.55/0.51  fof(f1261,plain,(
% 0.55/0.51    sk_c4=identity|~sQ4_spl|~sQ50_spl|~sQ2_spl|~sQ1_spl|~sQ48_spl|~sQ6_spl|~sQ5_spl),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f1239,f1249])).
% 0.55/0.51  fof(f1262,plain,(
% 0.55/0.51    multiply(sk_c8,sk_c4)=sk_c11|~sQ4_spl|~sQ50_spl|~sQ6_spl|~sQ5_spl|~sQ48_spl|~sQ2_spl|~sQ1_spl|~sQ7_spl),
% 0.55/0.51    inference(backward_demodulation,[status(thm)],[f1254,f158])).
% 0.55/0.51  fof(f1263,plain,(
% 0.55/0.51    inverse(sk_c4)=sk_c9|~sQ4_spl|~sQ48_spl|~sQ50_spl|~sQ6_spl|~sQ5_spl|~sQ1_spl|~sQ2_spl),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f1258,f1120])).
% 0.55/0.51  fof(f1264,plain,(
% 0.55/0.51    inverse(sk_c4)=sk_c4|~sQ4_spl|~sQ48_spl|~sQ50_spl|~sQ6_spl|~sQ5_spl|~sQ1_spl|~sQ2_spl),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f1239,f1263])).
% 0.55/0.51  fof(f1267,plain,(
% 0.55/0.51    ~inverse(sk_c4)=sk_c9|~sQ48_spl|~sQ4_spl|~sQ50_spl|~sQ6_spl|~sQ5_spl|~sQ2_spl|~sQ1_spl|sQ11_spl),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f1239,f1119])).
% 0.55/0.51  fof(f1268,plain,(
% 0.55/0.51    ~sk_c4=sk_c9|~sQ48_spl|~sQ4_spl|~sQ50_spl|~sQ6_spl|~sQ5_spl|~sQ2_spl|~sQ1_spl|sQ11_spl),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f1264,f1267])).
% 0.55/0.51  fof(f1269,plain,(
% 0.55/0.51    ~sk_c4=sk_c4|~sQ48_spl|~sQ4_spl|~sQ50_spl|~sQ6_spl|~sQ5_spl|~sQ2_spl|~sQ1_spl|sQ11_spl),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f1239,f1268])).
% 0.55/0.51  fof(f1270,plain,(
% 0.55/0.51    $false|~sQ48_spl|~sQ4_spl|~sQ50_spl|~sQ6_spl|~sQ5_spl|~sQ2_spl|~sQ1_spl|sQ11_spl),
% 0.55/0.51    inference(trivial_equality_resolution,[status(thm)],[f1269])).
% 0.55/0.51  fof(f1271,plain,(
% 0.55/0.51    ~sQ48_spl|~sQ4_spl|~sQ50_spl|~sQ6_spl|~sQ5_spl|~sQ2_spl|~sQ1_spl|sQ11_spl),
% 0.55/0.51    inference(contradiction_clause,[status(thm)],[f1270])).
% 0.55/0.51  fof(f1286,plain,(
% 0.55/0.51    ~sk_c4=sk_c11|~sQ48_spl|~sQ2_spl|~sQ50_spl|~sQ1_spl|~sQ4_spl|~sQ11_spl|~sQ6_spl|~sQ5_spl|sQ49_spl),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f1239,f803])).
% 0.55/0.51  fof(f1287,plain,(
% 0.55/0.51    ~sk_c4=sk_c4|~sQ48_spl|~sQ2_spl|~sQ50_spl|~sQ1_spl|~sQ4_spl|~sQ11_spl|~sQ6_spl|~sQ5_spl|sQ49_spl),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f1256,f1286])).
% 0.55/0.51  fof(f1288,plain,(
% 0.55/0.51    $false|~sQ48_spl|~sQ2_spl|~sQ50_spl|~sQ1_spl|~sQ4_spl|~sQ11_spl|~sQ6_spl|~sQ5_spl|sQ49_spl),
% 0.55/0.51    inference(trivial_equality_resolution,[status(thm)],[f1287])).
% 0.55/0.51  fof(f1289,plain,(
% 0.55/0.51    ~sQ48_spl|~sQ2_spl|~sQ50_spl|~sQ1_spl|~sQ4_spl|~sQ11_spl|~sQ6_spl|~sQ5_spl|sQ49_spl),
% 0.55/0.51    inference(contradiction_clause,[status(thm)],[f1288])).
% 0.55/0.51  fof(f1306,plain,(
% 0.55/0.51    ![X0]: (multiply(sk_c2,X0)=X0|~sQ13_spl|~sQ15_spl|~sQ14_spl|~sQ2_spl|~sQ1_spl)),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f1006,f65])).
% 0.55/0.51  fof(f1310,plain,(
% 0.55/0.51    ![X0]: (multiply(inverse(X0),X0)=sk_c2|~sQ13_spl|~sQ15_spl|~sQ14_spl|~sQ2_spl|~sQ1_spl)),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f1006,f66])).
% 0.55/0.51  fof(f1329,plain,(
% 0.55/0.51    multiply(sk_c2,sk_c1)=sk_c2|~sQ2_spl|~sQ1_spl|~sQ13_spl|~sQ14_spl|~sQ15_spl),
% 0.55/0.51    inference(paramodulation,[status(thm)],[f1036,f1310])).
% 0.55/0.51  fof(f1331,plain,(
% 0.55/0.51    sk_c1=sk_c2|~sQ2_spl|~sQ1_spl|~sQ13_spl|~sQ14_spl|~sQ15_spl),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f1306,f1329])).
% 0.55/0.51  fof(f1339,plain,(
% 0.55/0.51    sk_c1=identity|~sQ13_spl|~sQ15_spl|~sQ14_spl|~sQ2_spl|~sQ1_spl),
% 0.55/0.51    inference(backward_demodulation,[status(thm)],[f1331,f1006])).
% 0.55/0.51  fof(f1340,plain,(
% 0.55/0.51    sk_c11=sk_c1|~sQ2_spl|~sQ1_spl|~sQ15_spl|~sQ14_spl|~sQ13_spl|~sQ48_spl),
% 0.55/0.51    inference(backward_demodulation,[status(thm)],[f1331,f1011])).
% 0.55/0.51  fof(f1341,plain,(
% 0.55/0.51    sk_c1=sk_c10|~sQ2_spl|~sQ1_spl|~sQ15_spl|~sQ14_spl|~sQ13_spl),
% 0.55/0.51    inference(backward_demodulation,[status(thm)],[f1331,f642])).
% 0.55/0.51  fof(f1346,plain,(
% 0.55/0.51    inverse(sk_c1)=sk_c2|~sQ0_spl|~sQ2_spl|~sQ1_spl|~sQ15_spl|~sQ14_spl|~sQ13_spl|~sQ48_spl|~sQ11_spl),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f1331,f1072])).
% 0.55/0.51  fof(f1347,plain,(
% 0.55/0.51    inverse(sk_c1)=sk_c1|~sQ0_spl|~sQ2_spl|~sQ1_spl|~sQ15_spl|~sQ14_spl|~sQ13_spl|~sQ48_spl|~sQ11_spl),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f1331,f1346])).
% 0.55/0.51  fof(f1355,plain,(
% 0.55/0.51    ![X0,X1]: (~multiply(X0,inverse(X0))=sk_c1|~multiply(inverse(X0),sk_c10)=sk_c11|~inverse(inverse(X1))=inverse(X0)|~multiply(X1,inverse(X0))=inverse(X1)|~sQ2_spl|~sQ1_spl|~sQ15_spl|~sQ14_spl|~sQ13_spl|~sQ48_spl|~sQ19_spl)),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f1340,f251])).
% 0.55/0.51  fof(f1356,plain,(
% 0.55/0.51    ![X0,X1]: (~multiply(X0,inverse(X0))=sk_c1|~multiply(inverse(X0),sk_c1)=sk_c11|~inverse(inverse(X1))=inverse(X0)|~multiply(X1,inverse(X0))=inverse(X1)|~sQ2_spl|~sQ1_spl|~sQ15_spl|~sQ14_spl|~sQ13_spl|~sQ48_spl|~sQ19_spl)),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f1341,f1355])).
% 0.55/0.51  fof(f1357,plain,(
% 0.55/0.51    ![X0,X1]: (~multiply(X0,inverse(X0))=sk_c1|~multiply(inverse(X0),sk_c1)=sk_c1|~inverse(inverse(X1))=inverse(X0)|~multiply(X1,inverse(X0))=inverse(X1)|~sQ2_spl|~sQ1_spl|~sQ15_spl|~sQ14_spl|~sQ13_spl|~sQ48_spl|~sQ19_spl)),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f1340,f1356])).
% 0.55/0.51  fof(f1358,plain,(
% 0.55/0.51    ~multiply(sk_c1,inverse(sk_c1))=sk_c1|~multiply(inverse(sk_c1),sk_c1)=sk_c1|~inverse(inverse(sk_c1))=inverse(sk_c1)|~sQ48_spl|~sQ19_spl|~sQ2_spl|~sQ1_spl|~sQ13_spl|~sQ14_spl|~sQ15_spl),
% 0.55/0.51    inference(resolution,[status(thm)],[f1357,f633])).
% 0.55/0.51  fof(f1363,definition,(
% 0.55/0.51    sQ54_spl <=> (multiply(sk_c1,inverse(sk_c1))=sk_c1)),
% 0.55/0.51    introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition])).
% 0.55/0.51  fof(f1365,plain,(
% 0.55/0.51    ~multiply(sk_c1,inverse(sk_c1))=sk_c1|sQ54_spl),
% 0.55/0.51    inference(component_clause,[status(thm)],[f1363])).
% 0.55/0.51  fof(f1366,definition,(
% 0.55/0.51    sQ55_spl <=> (multiply(inverse(sk_c1),sk_c1)=sk_c1)),
% 0.55/0.51    introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition])).
% 0.55/0.51  fof(f1368,plain,(
% 0.55/0.51    ~multiply(inverse(sk_c1),sk_c1)=sk_c1|sQ55_spl),
% 0.55/0.51    inference(component_clause,[status(thm)],[f1366])).
% 0.55/0.51  fof(f1369,definition,(
% 0.55/0.51    sQ56_spl <=> (inverse(inverse(sk_c1))=inverse(sk_c1))),
% 0.55/0.51    introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition])).
% 0.55/0.51  fof(f1371,plain,(
% 0.55/0.51    ~inverse(inverse(sk_c1))=inverse(sk_c1)|sQ56_spl),
% 0.55/0.51    inference(component_clause,[status(thm)],[f1369])).
% 0.55/0.51  fof(f1372,plain,(
% 0.55/0.51    ~sQ54_spl|~sQ55_spl|~sQ56_spl|~sQ48_spl|~sQ19_spl|~sQ2_spl|~sQ1_spl|~sQ13_spl|~sQ14_spl|~sQ15_spl),
% 0.55/0.51    inference(split_clause,[status(thm)],[f1358,f1363,f1366,f1369,f721,f247,f137,f133,f199,f212,f225])).
% 0.55/0.51  fof(f1388,plain,(
% 0.55/0.51    ~multiply(sk_c1,sk_c1)=sk_c1|~sQ0_spl|~sQ2_spl|~sQ1_spl|~sQ15_spl|~sQ14_spl|~sQ13_spl|~sQ48_spl|~sQ11_spl|sQ55_spl),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f1347,f1368])).
% 0.55/0.51  fof(f1389,plain,(
% 0.55/0.51    ~sk_c1=sk_c1|~sQ0_spl|~sQ2_spl|~sQ1_spl|~sQ15_spl|~sQ14_spl|~sQ13_spl|~sQ48_spl|~sQ11_spl|sQ55_spl),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f633,f1388])).
% 0.55/0.51  fof(f1390,plain,(
% 0.55/0.51    $false|~sQ0_spl|~sQ2_spl|~sQ1_spl|~sQ15_spl|~sQ14_spl|~sQ13_spl|~sQ48_spl|~sQ11_spl|sQ55_spl),
% 0.55/0.51    inference(trivial_equality_resolution,[status(thm)],[f1389])).
% 0.55/0.51  fof(f1391,plain,(
% 0.55/0.51    ~sQ0_spl|~sQ2_spl|~sQ1_spl|~sQ15_spl|~sQ14_spl|~sQ13_spl|~sQ48_spl|~sQ11_spl|sQ55_spl),
% 0.55/0.51    inference(contradiction_clause,[status(thm)],[f1390])).
% 0.55/0.51  fof(f1392,plain,(
% 0.55/0.51    ~inverse(sk_c1)=sk_c1|~sQ2_spl|~sQ1_spl|~sQ13_spl|~sQ14_spl|~sQ15_spl|sQ54_spl),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f633,f1365])).
% 0.55/0.51  fof(f1393,plain,(
% 0.55/0.51    ~sk_c1=sk_c1|~sQ0_spl|~sQ48_spl|~sQ11_spl|~sQ2_spl|~sQ1_spl|~sQ13_spl|~sQ14_spl|~sQ15_spl|sQ54_spl),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f1347,f1392])).
% 0.55/0.51  fof(f1394,plain,(
% 0.55/0.51    $false|~sQ0_spl|~sQ48_spl|~sQ11_spl|~sQ2_spl|~sQ1_spl|~sQ13_spl|~sQ14_spl|~sQ15_spl|sQ54_spl),
% 0.55/0.51    inference(trivial_equality_resolution,[status(thm)],[f1393])).
% 0.55/0.51  fof(f1395,plain,(
% 0.55/0.51    ~sQ0_spl|~sQ48_spl|~sQ11_spl|~sQ2_spl|~sQ1_spl|~sQ13_spl|~sQ14_spl|~sQ15_spl|sQ54_spl),
% 0.55/0.51    inference(contradiction_clause,[status(thm)],[f1394])).
% 0.55/0.51  fof(f1404,plain,(
% 0.55/0.51    ~inverse(sk_c1)=sk_c10|~sQ13_spl|~sQ15_spl|~sQ14_spl|~sQ2_spl|~sQ1_spl|sQ51_spl),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f1339,f758])).
% 0.55/0.51  fof(f1405,plain,(
% 0.55/0.51    ~sk_c1=sk_c10|~sQ0_spl|~sQ48_spl|~sQ11_spl|~sQ13_spl|~sQ15_spl|~sQ14_spl|~sQ2_spl|~sQ1_spl|sQ51_spl),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f1347,f1404])).
% 0.55/0.51  fof(f1406,plain,(
% 0.55/0.51    ~sk_c1=sk_c1|~sQ0_spl|~sQ48_spl|~sQ11_spl|~sQ13_spl|~sQ15_spl|~sQ14_spl|~sQ2_spl|~sQ1_spl|sQ51_spl),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f1341,f1405])).
% 0.55/0.51  fof(f1407,plain,(
% 0.55/0.51    $false|~sQ0_spl|~sQ48_spl|~sQ11_spl|~sQ13_spl|~sQ15_spl|~sQ14_spl|~sQ2_spl|~sQ1_spl|sQ51_spl),
% 0.55/0.51    inference(trivial_equality_resolution,[status(thm)],[f1406])).
% 0.55/0.51  fof(f1408,plain,(
% 0.55/0.51    ~sQ0_spl|~sQ48_spl|~sQ11_spl|~sQ13_spl|~sQ15_spl|~sQ14_spl|~sQ2_spl|~sQ1_spl|sQ51_spl),
% 0.55/0.51    inference(contradiction_clause,[status(thm)],[f1407])).
% 0.55/0.51  fof(f1417,plain,(
% 0.55/0.51    sk_c8=multiply(sk_c8,sk_c11)|~sQ6_spl|~sQ5_spl),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f154,f430])).
% 0.55/0.51  fof(f1419,plain,(
% 0.55/0.51    sk_c8=multiply(sk_c8,sk_c11)|~sQ6_spl|~sQ5_spl),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f154,f836])).
% 0.55/0.51  fof(f1424,plain,(
% 0.55/0.51    multiply(sk_c11,sk_c2)=sk_c9|~sQ50_spl|~sQ13_spl),
% 0.55/0.51    inference(backward_demodulation,[status(thm)],[f754,f200])).
% 0.55/0.51  fof(f1425,plain,(
% 0.55/0.51    sk_c11=sk_c9|~sQ50_spl|~sQ48_spl),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f754,f722])).
% 0.55/0.51  fof(f1426,plain,(
% 0.55/0.51    sk_c11=sk_c4|~sQ2_spl|~sQ1_spl|~sQ6_spl|~sQ5_spl|~sQ4_spl|~sQ50_spl|~sQ48_spl),
% 0.55/0.51    inference(backward_demodulation,[status(thm)],[f1239,f1425])).
% 0.55/0.51  fof(f1427,plain,(
% 0.55/0.51    sk_c10=sk_c4|~sQ48_spl|~sQ2_spl|~sQ1_spl|~sQ6_spl|~sQ5_spl|~sQ4_spl|~sQ50_spl),
% 0.55/0.51    inference(backward_demodulation,[status(thm)],[f1239,f754])).
% 0.55/0.51  fof(f1441,plain,(
% 0.55/0.51    ![X0,X1]: (~multiply(X0,inverse(X0))=sk_c4|~multiply(inverse(X0),sk_c10)=sk_c11|~inverse(inverse(X1))=inverse(X0)|~multiply(X1,inverse(X0))=inverse(X1)|~sQ4_spl|~sQ6_spl|~sQ5_spl|~sQ48_spl|~sQ2_spl|~sQ50_spl|~sQ1_spl|~sQ19_spl)),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f1256,f251])).
% 0.55/0.51  fof(f1442,plain,(
% 0.55/0.51    ![X0,X1]: (~multiply(X0,inverse(X0))=sk_c4|~multiply(inverse(X0),sk_c4)=sk_c11|~inverse(inverse(X1))=inverse(X0)|~multiply(X1,inverse(X0))=inverse(X1)|~sQ4_spl|~sQ6_spl|~sQ5_spl|~sQ48_spl|~sQ2_spl|~sQ50_spl|~sQ1_spl|~sQ19_spl)),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f1254,f1441])).
% 0.55/0.51  fof(f1443,plain,(
% 0.55/0.51    ![X0,X1]: (~multiply(X0,inverse(X0))=sk_c4|~multiply(inverse(X0),sk_c4)=sk_c4|~inverse(inverse(X1))=inverse(X0)|~multiply(X1,inverse(X0))=inverse(X1)|~sQ4_spl|~sQ6_spl|~sQ5_spl|~sQ48_spl|~sQ2_spl|~sQ50_spl|~sQ1_spl|~sQ19_spl)),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f1256,f1442])).
% 0.55/0.51  fof(f1470,plain,(
% 0.55/0.51    ![X0,X1]: (~multiply(X0,inverse(X0))=sk_c4|~multiply(inverse(X0),sk_c4)=sk_c2|~inverse(inverse(X1))=inverse(X0)|~multiply(X1,inverse(X0))=inverse(X1)|~sQ13_spl|~sQ11_spl|~sQ12_spl|~sQ0_spl|~sQ4_spl|~sQ6_spl|~sQ5_spl|~sQ48_spl|~sQ2_spl|~sQ50_spl|~sQ1_spl|~sQ19_spl)),
% 0.55/0.51    inference(backward_demodulation,[status(thm)],[f902,f1443])).
% 0.55/0.51  fof(f1478,plain,(
% 0.55/0.51    ![X0,X1]: (~multiply(X0,inverse(X0))=sk_c2|~multiply(inverse(X0),sk_c4)=sk_c2|~inverse(inverse(X1))=inverse(X0)|~multiply(X1,inverse(X0))=inverse(X1)|~sQ13_spl|~sQ11_spl|~sQ12_spl|~sQ0_spl|~sQ4_spl|~sQ6_spl|~sQ5_spl|~sQ48_spl|~sQ2_spl|~sQ50_spl|~sQ1_spl|~sQ19_spl)),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f902,f1470])).
% 0.55/0.51  fof(f1479,plain,(
% 0.55/0.51    ![X0,X1]: (~multiply(X0,inverse(X0))=sk_c2|~multiply(inverse(X0),sk_c2)=sk_c2|~inverse(inverse(X1))=inverse(X0)|~multiply(X1,inverse(X0))=inverse(X1)|~sQ13_spl|~sQ11_spl|~sQ12_spl|~sQ0_spl|~sQ4_spl|~sQ6_spl|~sQ5_spl|~sQ48_spl|~sQ2_spl|~sQ50_spl|~sQ1_spl|~sQ19_spl)),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f902,f1478])).
% 0.55/0.51  fof(f1500,plain,(
% 0.55/0.51    ![X0]: (multiply(inverse(X0),X0)=sk_c2|~sQ13_spl|~sQ11_spl|~sQ2_spl|~sQ6_spl|~sQ5_spl|~sQ0_spl|~sQ1_spl|~sQ12_spl|~sQ4_spl)),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f916,f66])).
% 0.55/0.51  fof(f1504,plain,(
% 0.55/0.51    ![X0]: (multiply(sk_c2,X0)=X0|~sQ13_spl|~sQ11_spl|~sQ2_spl|~sQ6_spl|~sQ5_spl|~sQ0_spl|~sQ1_spl|~sQ12_spl|~sQ4_spl)),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f916,f65])).
% 0.55/0.51  fof(f1512,plain,(
% 0.55/0.51    inverse(sk_c2)=sk_c9|~sQ13_spl|~sQ12_spl|~sQ4_spl|~sQ2_spl|~sQ6_spl|~sQ5_spl|~sQ0_spl|~sQ1_spl|~sQ11_spl),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f914,f174])).
% 0.55/0.51  fof(f1513,plain,(
% 0.55/0.51    inverse(sk_c2)=sk_c2|~sQ13_spl|~sQ12_spl|~sQ4_spl|~sQ2_spl|~sQ6_spl|~sQ5_spl|~sQ0_spl|~sQ1_spl|~sQ11_spl),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f915,f1512])).
% 0.55/0.51  fof(f1875,plain,(
% 0.55/0.51    ~multiply(sk_c2,inverse(sk_c2))=sk_c2|~multiply(inverse(sk_c2),sk_c2)=sk_c2|~inverse(inverse(sk_c2))=inverse(sk_c2)|~sQ48_spl|~sQ50_spl|~sQ19_spl|~sQ13_spl|~sQ11_spl|~sQ2_spl|~sQ6_spl|~sQ5_spl|~sQ0_spl|~sQ1_spl|~sQ12_spl|~sQ4_spl),
% 0.55/0.51    inference(resolution,[status(thm)],[f1479,f1504])).
% 0.55/0.51  fof(f1882,definition,(
% 0.55/0.51    sQ62_spl <=> (multiply(sk_c2,inverse(sk_c2))=sk_c2)),
% 0.55/0.51    introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition])).
% 0.55/0.51  fof(f1884,plain,(
% 0.55/0.51    ~multiply(sk_c2,inverse(sk_c2))=sk_c2|sQ62_spl),
% 0.55/0.51    inference(component_clause,[status(thm)],[f1882])).
% 0.55/0.51  fof(f1885,definition,(
% 0.55/0.51    sQ63_spl <=> (multiply(inverse(sk_c2),sk_c2)=sk_c2)),
% 0.55/0.51    introduced(definition,[new_symbols(definition,[sQ63_spl])],[split_symbol_definition])).
% 0.55/0.51  fof(f1887,plain,(
% 0.55/0.51    ~multiply(inverse(sk_c2),sk_c2)=sk_c2|sQ63_spl),
% 0.55/0.51    inference(component_clause,[status(thm)],[f1885])).
% 0.55/0.51  fof(f1888,definition,(
% 0.55/0.51    sQ64_spl <=> (inverse(inverse(sk_c2))=inverse(sk_c2))),
% 0.55/0.51    introduced(definition,[new_symbols(definition,[sQ64_spl])],[split_symbol_definition])).
% 0.55/0.51  fof(f1890,plain,(
% 0.55/0.51    ~inverse(inverse(sk_c2))=inverse(sk_c2)|sQ64_spl),
% 0.55/0.51    inference(component_clause,[status(thm)],[f1888])).
% 0.55/0.51  fof(f1891,plain,(
% 0.55/0.51    ~sQ62_spl|~sQ63_spl|~sQ64_spl|~sQ48_spl|~sQ50_spl|~sQ19_spl|~sQ13_spl|~sQ11_spl|~sQ2_spl|~sQ6_spl|~sQ5_spl|~sQ0_spl|~sQ1_spl|~sQ12_spl|~sQ4_spl),
% 0.55/0.51    inference(split_clause,[status(thm)],[f1875,f1882,f1885,f1888,f721,f753,f247,f199,f173,f137,f153,f149,f130,f133,f186,f145])).
% 0.55/0.51  fof(f1907,plain,(
% 0.55/0.51    ~sk_c2=sk_c2|~sQ13_spl|~sQ11_spl|~sQ2_spl|~sQ6_spl|~sQ5_spl|~sQ0_spl|~sQ1_spl|~sQ12_spl|~sQ4_spl|sQ63_spl),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f1500,f1887])).
% 0.55/0.51  fof(f1908,plain,(
% 0.55/0.51    $false|~sQ13_spl|~sQ11_spl|~sQ2_spl|~sQ6_spl|~sQ5_spl|~sQ0_spl|~sQ1_spl|~sQ12_spl|~sQ4_spl|sQ63_spl),
% 0.55/0.51    inference(trivial_equality_resolution,[status(thm)],[f1907])).
% 0.55/0.51  fof(f1909,plain,(
% 0.55/0.51    ~sQ13_spl|~sQ11_spl|~sQ2_spl|~sQ6_spl|~sQ5_spl|~sQ0_spl|~sQ1_spl|~sQ12_spl|~sQ4_spl|sQ63_spl),
% 0.55/0.51    inference(contradiction_clause,[status(thm)],[f1908])).
% 0.55/0.51  fof(f1910,plain,(
% 0.55/0.51    ~inverse(sk_c2)=sk_c2|~sQ13_spl|~sQ11_spl|~sQ2_spl|~sQ6_spl|~sQ5_spl|~sQ0_spl|~sQ1_spl|~sQ12_spl|~sQ4_spl|sQ62_spl),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f1504,f1884])).
% 0.55/0.51  fof(f1911,plain,(
% 0.55/0.51    ~sk_c2=sk_c2|~sQ13_spl|~sQ11_spl|~sQ2_spl|~sQ6_spl|~sQ5_spl|~sQ0_spl|~sQ1_spl|~sQ12_spl|~sQ4_spl|sQ62_spl),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f1513,f1910])).
% 0.55/0.51  fof(f1912,plain,(
% 0.55/0.51    $false|~sQ13_spl|~sQ11_spl|~sQ2_spl|~sQ6_spl|~sQ5_spl|~sQ0_spl|~sQ1_spl|~sQ12_spl|~sQ4_spl|sQ62_spl),
% 0.55/0.51    inference(trivial_equality_resolution,[status(thm)],[f1911])).
% 0.55/0.51  fof(f1913,plain,(
% 0.55/0.51    ~sQ13_spl|~sQ11_spl|~sQ2_spl|~sQ6_spl|~sQ5_spl|~sQ0_spl|~sQ1_spl|~sQ12_spl|~sQ4_spl|sQ62_spl),
% 0.55/0.51    inference(contradiction_clause,[status(thm)],[f1912])).
% 0.55/0.51  fof(f1916,plain,(
% 0.55/0.51    ~inverse(sk_c2)=inverse(sk_c2)|~sQ13_spl|~sQ12_spl|~sQ4_spl|~sQ2_spl|~sQ6_spl|~sQ5_spl|~sQ0_spl|~sQ1_spl|~sQ11_spl|sQ64_spl),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f1513,f1890])).
% 0.55/0.51  fof(f1917,plain,(
% 0.55/0.51    ~sk_c2=inverse(sk_c2)|~sQ13_spl|~sQ12_spl|~sQ4_spl|~sQ2_spl|~sQ6_spl|~sQ5_spl|~sQ0_spl|~sQ1_spl|~sQ11_spl|sQ64_spl),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f1513,f1916])).
% 0.55/0.51  fof(f1918,plain,(
% 0.55/0.51    ~sk_c2=sk_c2|~sQ13_spl|~sQ12_spl|~sQ4_spl|~sQ2_spl|~sQ6_spl|~sQ5_spl|~sQ0_spl|~sQ1_spl|~sQ11_spl|sQ64_spl),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f1513,f1917])).
% 0.55/0.51  fof(f1919,plain,(
% 0.55/0.51    $false|~sQ13_spl|~sQ12_spl|~sQ4_spl|~sQ2_spl|~sQ6_spl|~sQ5_spl|~sQ0_spl|~sQ1_spl|~sQ11_spl|sQ64_spl),
% 0.55/0.51    inference(trivial_equality_resolution,[status(thm)],[f1918])).
% 0.55/0.51  fof(f1920,plain,(
% 0.55/0.51    ~sQ13_spl|~sQ12_spl|~sQ4_spl|~sQ2_spl|~sQ6_spl|~sQ5_spl|~sQ0_spl|~sQ1_spl|~sQ11_spl|sQ64_spl),
% 0.55/0.51    inference(contradiction_clause,[status(thm)],[f1919])).
% 0.55/0.51  fof(f1924,plain,(
% 0.55/0.51    sk_c9=sk_c4|~sQ2_spl|~sQ1_spl|~sQ4_spl|~sQ50_spl|~sQ48_spl|~sQ11_spl|~sQ6_spl|~sQ5_spl|~sQ49_spl),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f1426,f835])).
% 0.55/0.51  fof(f1935,plain,(
% 0.55/0.51    inverse(sk_c4)=sk_c10|~sQ48_spl|~sQ2_spl|~sQ1_spl|~sQ6_spl|~sQ5_spl|~sQ4_spl|~sQ50_spl|~sQ47_spl),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f1427,f709])).
% 0.55/0.51  fof(f1936,plain,(
% 0.55/0.51    inverse(sk_c4)=sk_c4|~sQ48_spl|~sQ2_spl|~sQ1_spl|~sQ6_spl|~sQ5_spl|~sQ4_spl|~sQ50_spl|~sQ47_spl),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f1427,f1935])).
% 0.55/0.51  fof(f1940,plain,(
% 0.55/0.51    inverse(sk_c6)=sk_c6|~sQ11_spl|~sQ12_spl|~sQ4_spl|~sQ2_spl|~sQ1_spl|~sQ6_spl|~sQ5_spl|~sQ0_spl|~sQ7_spl|~sQ8_spl|~sQ10_spl|~sQ9_spl),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f929,f166])).
% 0.55/0.51  fof(f1957,plain,(
% 0.55/0.51    ![X0]: (X0=multiply(sk_c6,X0)|~sQ9_spl|~sQ8_spl|~sQ10_spl|~sQ11_spl|~sQ12_spl|~sQ4_spl|~sQ2_spl|~sQ1_spl|~sQ6_spl|~sQ5_spl|~sQ0_spl|~sQ7_spl)),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f929,f900])).
% 0.55/0.51  fof(f1964,plain,(
% 0.55/0.51    ![X0]: (multiply(inverse(X0),X0)=sk_c4|~sQ4_spl|~sQ50_spl|~sQ48_spl|~sQ11_spl|~sQ49_spl|~sQ2_spl|~sQ0_spl|~sQ1_spl|~sQ6_spl|~sQ5_spl)),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f1924,f1136])).
% 0.55/0.51  fof(f1965,plain,(
% 0.55/0.51    multiply(sk_c6,sk_c5)=sk_c4|~sQ50_spl|~sQ48_spl|~sQ49_spl|~sQ11_spl|~sQ12_spl|~sQ4_spl|~sQ2_spl|~sQ1_spl|~sQ5_spl|~sQ0_spl|~sQ7_spl|~sQ9_spl|~sQ8_spl|~sQ10_spl|~sQ6_spl),
% 0.55/0.51    inference(paramodulation,[status(thm)],[f933,f1964])).
% 0.55/0.51  fof(f1967,plain,(
% 0.55/0.51    multiply(sk_c6,sk_c6)=sk_c4|~sQ50_spl|~sQ48_spl|~sQ49_spl|~sQ11_spl|~sQ12_spl|~sQ4_spl|~sQ2_spl|~sQ1_spl|~sQ6_spl|~sQ5_spl|~sQ0_spl|~sQ7_spl|~sQ8_spl|~sQ10_spl|~sQ9_spl),
% 0.55/0.51    inference(paramodulation,[status(thm)],[f1940,f1964])).
% 0.55/0.51  fof(f1971,plain,(
% 0.55/0.51    sk_c5=sk_c4|~sQ50_spl|~sQ48_spl|~sQ49_spl|~sQ11_spl|~sQ12_spl|~sQ4_spl|~sQ2_spl|~sQ1_spl|~sQ5_spl|~sQ0_spl|~sQ7_spl|~sQ9_spl|~sQ8_spl|~sQ10_spl|~sQ6_spl),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f1957,f1965])).
% 0.55/0.51  fof(f1973,plain,(
% 0.55/0.51    sk_c6=sk_c4|~sQ50_spl|~sQ48_spl|~sQ49_spl|~sQ11_spl|~sQ12_spl|~sQ4_spl|~sQ2_spl|~sQ1_spl|~sQ6_spl|~sQ5_spl|~sQ0_spl|~sQ7_spl|~sQ8_spl|~sQ10_spl|~sQ9_spl),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f1957,f1967])).
% 0.55/0.51  fof(f1985,plain,(
% 0.55/0.51    inverse(sk_c4)=sk_c5|~sQ49_spl|~sQ11_spl|~sQ12_spl|~sQ0_spl|~sQ7_spl|~sQ9_spl|~sQ8_spl|~sQ10_spl|~sQ48_spl|~sQ2_spl|~sQ1_spl|~sQ6_spl|~sQ5_spl|~sQ4_spl|~sQ50_spl|~sQ47_spl),
% 0.55/0.51    inference(backward_demodulation,[status(thm)],[f1971,f1936])).
% 0.55/0.51  fof(f1989,plain,(
% 0.55/0.51    sk_c9=sk_c5|~sQ12_spl|~sQ0_spl|~sQ7_spl|~sQ9_spl|~sQ8_spl|~sQ10_spl|~sQ2_spl|~sQ1_spl|~sQ4_spl|~sQ50_spl|~sQ48_spl|~sQ11_spl|~sQ6_spl|~sQ5_spl|~sQ49_spl),
% 0.55/0.51    inference(backward_demodulation,[status(thm)],[f1971,f1924])).
% 0.55/0.51  fof(f1992,plain,(
% 0.55/0.51    inverse(sk_c5)=sk_c5|~sQ49_spl|~sQ11_spl|~sQ12_spl|~sQ0_spl|~sQ7_spl|~sQ9_spl|~sQ8_spl|~sQ10_spl|~sQ48_spl|~sQ2_spl|~sQ1_spl|~sQ6_spl|~sQ5_spl|~sQ4_spl|~sQ50_spl|~sQ47_spl),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f1971,f1985])).
% 0.55/0.51  fof(f1993,plain,(
% 0.55/0.51    sk_c6=sk_c5|~sQ49_spl|~sQ11_spl|~sQ12_spl|~sQ0_spl|~sQ7_spl|~sQ9_spl|~sQ8_spl|~sQ10_spl|~sQ48_spl|~sQ2_spl|~sQ1_spl|~sQ6_spl|~sQ5_spl|~sQ4_spl|~sQ50_spl|~sQ47_spl),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f933,f1992])).
% 0.55/0.51  fof(f2000,plain,(
% 0.55/0.51    sk_c9=sk_c6|~sQ47_spl|~sQ12_spl|~sQ0_spl|~sQ7_spl|~sQ9_spl|~sQ8_spl|~sQ10_spl|~sQ2_spl|~sQ1_spl|~sQ4_spl|~sQ50_spl|~sQ48_spl|~sQ11_spl|~sQ6_spl|~sQ5_spl|~sQ49_spl),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f1993,f1989])).
% 0.55/0.51  fof(f2006,plain,(
% 0.55/0.51    ![X0]: (multiply(inverse(X0),X0)=sk_c6|~sQ50_spl|~sQ48_spl|~sQ49_spl|~sQ11_spl|~sQ12_spl|~sQ7_spl|~sQ8_spl|~sQ10_spl|~sQ9_spl|~sQ4_spl|~sQ2_spl|~sQ0_spl|~sQ1_spl|~sQ6_spl|~sQ5_spl)),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f1973,f1153])).
% 0.55/0.51  fof(f2188,plain,(
% 0.55/0.51    ![X0,X1]: (~multiply(X0,inverse(X0))=sk_c6|~multiply(inverse(X0),sk_c4)=sk_c4|~inverse(inverse(X1))=inverse(X0)|~multiply(X1,inverse(X0))=inverse(X1)|~sQ49_spl|~sQ11_spl|~sQ12_spl|~sQ0_spl|~sQ7_spl|~sQ8_spl|~sQ10_spl|~sQ9_spl|~sQ4_spl|~sQ6_spl|~sQ5_spl|~sQ48_spl|~sQ2_spl|~sQ50_spl|~sQ1_spl|~sQ19_spl)),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f1973,f1443])).
% 0.55/0.51  fof(f2189,plain,(
% 0.55/0.51    ![X0,X1]: (~multiply(X0,inverse(X0))=sk_c6|~multiply(inverse(X0),sk_c6)=sk_c4|~inverse(inverse(X1))=inverse(X0)|~multiply(X1,inverse(X0))=inverse(X1)|~sQ49_spl|~sQ11_spl|~sQ12_spl|~sQ0_spl|~sQ7_spl|~sQ8_spl|~sQ10_spl|~sQ9_spl|~sQ4_spl|~sQ6_spl|~sQ5_spl|~sQ48_spl|~sQ2_spl|~sQ50_spl|~sQ1_spl|~sQ19_spl)),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f1973,f2188])).
% 0.55/0.51  fof(f2190,plain,(
% 0.55/0.51    ![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)|~sQ49_spl|~sQ11_spl|~sQ12_spl|~sQ0_spl|~sQ7_spl|~sQ8_spl|~sQ10_spl|~sQ9_spl|~sQ4_spl|~sQ6_spl|~sQ5_spl|~sQ48_spl|~sQ2_spl|~sQ50_spl|~sQ1_spl|~sQ19_spl)),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f1973,f2189])).
% 0.55/0.51  fof(f2191,plain,(
% 0.55/0.51    ~multiply(sk_c6,inverse(sk_c6))=sk_c6|~multiply(inverse(sk_c6),sk_c6)=sk_c6|~inverse(inverse(sk_c6))=inverse(sk_c6)|~sQ49_spl|~sQ48_spl|~sQ50_spl|~sQ19_spl|~sQ9_spl|~sQ8_spl|~sQ10_spl|~sQ11_spl|~sQ12_spl|~sQ4_spl|~sQ2_spl|~sQ1_spl|~sQ6_spl|~sQ5_spl|~sQ0_spl|~sQ7_spl),
% 0.55/0.51    inference(resolution,[status(thm)],[f2190,f1957])).
% 0.55/0.51  fof(f2196,definition,(
% 0.55/0.51    sQ68_spl <=> (multiply(sk_c6,inverse(sk_c6))=sk_c6)),
% 0.55/0.51    introduced(definition,[new_symbols(definition,[sQ68_spl])],[split_symbol_definition])).
% 0.55/0.51  fof(f2198,plain,(
% 0.55/0.51    ~multiply(sk_c6,inverse(sk_c6))=sk_c6|sQ68_spl),
% 0.55/0.51    inference(component_clause,[status(thm)],[f2196])).
% 0.55/0.51  fof(f2199,definition,(
% 0.55/0.51    sQ69_spl <=> (multiply(inverse(sk_c6),sk_c6)=sk_c6)),
% 0.55/0.51    introduced(definition,[new_symbols(definition,[sQ69_spl])],[split_symbol_definition])).
% 0.55/0.51  fof(f2201,plain,(
% 0.55/0.51    ~multiply(inverse(sk_c6),sk_c6)=sk_c6|sQ69_spl),
% 0.55/0.51    inference(component_clause,[status(thm)],[f2199])).
% 0.55/0.51  fof(f2202,definition,(
% 0.55/0.51    sQ70_spl <=> (inverse(inverse(sk_c6))=inverse(sk_c6))),
% 0.55/0.51    introduced(definition,[new_symbols(definition,[sQ70_spl])],[split_symbol_definition])).
% 0.55/0.51  fof(f2204,plain,(
% 0.55/0.51    ~inverse(inverse(sk_c6))=inverse(sk_c6)|sQ70_spl),
% 0.55/0.51    inference(component_clause,[status(thm)],[f2202])).
% 0.55/0.51  fof(f2205,plain,(
% 0.55/0.51    ~sQ68_spl|~sQ69_spl|~sQ70_spl|~sQ49_spl|~sQ48_spl|~sQ50_spl|~sQ19_spl|~sQ9_spl|~sQ8_spl|~sQ10_spl|~sQ11_spl|~sQ12_spl|~sQ4_spl|~sQ2_spl|~sQ1_spl|~sQ6_spl|~sQ5_spl|~sQ0_spl|~sQ7_spl),
% 0.55/0.51    inference(split_clause,[status(thm)],[f2191,f2196,f2199,f2202,f724,f721,f753,f247,f165,f161,f169,f173,f186,f145,f137,f133,f153,f149,f130,f157])).
% 0.55/0.51  fof(f2214,plain,(
% 0.55/0.51    ~sk_c6=sk_c6|~sQ50_spl|~sQ48_spl|~sQ49_spl|~sQ11_spl|~sQ12_spl|~sQ7_spl|~sQ8_spl|~sQ10_spl|~sQ9_spl|~sQ4_spl|~sQ2_spl|~sQ0_spl|~sQ1_spl|~sQ6_spl|~sQ5_spl|sQ69_spl),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f2006,f2201])).
% 0.55/0.51  fof(f2215,plain,(
% 0.55/0.51    $false|~sQ50_spl|~sQ48_spl|~sQ49_spl|~sQ11_spl|~sQ12_spl|~sQ7_spl|~sQ8_spl|~sQ10_spl|~sQ9_spl|~sQ4_spl|~sQ2_spl|~sQ0_spl|~sQ1_spl|~sQ6_spl|~sQ5_spl|sQ69_spl),
% 0.55/0.51    inference(trivial_equality_resolution,[status(thm)],[f2214])).
% 0.55/0.51  fof(f2216,plain,(
% 0.55/0.51    ~sQ50_spl|~sQ48_spl|~sQ49_spl|~sQ11_spl|~sQ12_spl|~sQ7_spl|~sQ8_spl|~sQ10_spl|~sQ9_spl|~sQ4_spl|~sQ2_spl|~sQ0_spl|~sQ1_spl|~sQ6_spl|~sQ5_spl|sQ69_spl),
% 0.55/0.51    inference(contradiction_clause,[status(thm)],[f2215])).
% 0.55/0.51  fof(f2217,plain,(
% 0.55/0.51    ~inverse(sk_c6)=sk_c6|~sQ9_spl|~sQ8_spl|~sQ10_spl|~sQ11_spl|~sQ12_spl|~sQ4_spl|~sQ2_spl|~sQ1_spl|~sQ6_spl|~sQ5_spl|~sQ0_spl|~sQ7_spl|sQ68_spl),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f1957,f2198])).
% 0.55/0.51  fof(f2218,plain,(
% 0.55/0.51    ~sk_c6=sk_c6|~sQ9_spl|~sQ8_spl|~sQ10_spl|~sQ11_spl|~sQ12_spl|~sQ4_spl|~sQ2_spl|~sQ1_spl|~sQ6_spl|~sQ5_spl|~sQ0_spl|~sQ7_spl|sQ68_spl),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f1940,f2217])).
% 0.55/0.51  fof(f2219,plain,(
% 0.55/0.51    $false|~sQ9_spl|~sQ8_spl|~sQ10_spl|~sQ11_spl|~sQ12_spl|~sQ4_spl|~sQ2_spl|~sQ1_spl|~sQ6_spl|~sQ5_spl|~sQ0_spl|~sQ7_spl|sQ68_spl),
% 0.55/0.51    inference(trivial_equality_resolution,[status(thm)],[f2218])).
% 0.55/0.51  fof(f2220,plain,(
% 0.55/0.51    ~sQ9_spl|~sQ8_spl|~sQ10_spl|~sQ11_spl|~sQ12_spl|~sQ4_spl|~sQ2_spl|~sQ1_spl|~sQ6_spl|~sQ5_spl|~sQ0_spl|~sQ7_spl|sQ68_spl),
% 0.55/0.51    inference(contradiction_clause,[status(thm)],[f2219])).
% 0.55/0.51  fof(f2222,plain,(
% 0.55/0.51    ~inverse(sk_c6)=inverse(sk_c6)|~sQ11_spl|~sQ12_spl|~sQ4_spl|~sQ2_spl|~sQ1_spl|~sQ6_spl|~sQ5_spl|~sQ0_spl|~sQ7_spl|~sQ8_spl|~sQ10_spl|~sQ9_spl|sQ70_spl),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f1940,f2204])).
% 0.55/0.51  fof(f2223,plain,(
% 0.55/0.51    ~sk_c6=inverse(sk_c6)|~sQ11_spl|~sQ12_spl|~sQ4_spl|~sQ2_spl|~sQ1_spl|~sQ6_spl|~sQ5_spl|~sQ0_spl|~sQ7_spl|~sQ8_spl|~sQ10_spl|~sQ9_spl|sQ70_spl),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f1940,f2222])).
% 0.55/0.51  fof(f2224,plain,(
% 0.55/0.51    ~sk_c6=sk_c6|~sQ11_spl|~sQ12_spl|~sQ4_spl|~sQ2_spl|~sQ1_spl|~sQ6_spl|~sQ5_spl|~sQ0_spl|~sQ7_spl|~sQ8_spl|~sQ10_spl|~sQ9_spl|sQ70_spl),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f1940,f2223])).
% 0.55/0.51  fof(f2225,plain,(
% 0.55/0.51    $false|~sQ11_spl|~sQ12_spl|~sQ4_spl|~sQ2_spl|~sQ1_spl|~sQ6_spl|~sQ5_spl|~sQ0_spl|~sQ7_spl|~sQ8_spl|~sQ10_spl|~sQ9_spl|sQ70_spl),
% 0.55/0.51    inference(trivial_equality_resolution,[status(thm)],[f2224])).
% 0.55/0.51  fof(f2226,plain,(
% 0.55/0.51    ~sQ11_spl|~sQ12_spl|~sQ4_spl|~sQ2_spl|~sQ1_spl|~sQ6_spl|~sQ5_spl|~sQ0_spl|~sQ7_spl|~sQ8_spl|~sQ10_spl|~sQ9_spl|sQ70_spl),
% 0.55/0.51    inference(contradiction_clause,[status(thm)],[f2225])).
% 0.55/0.51  fof(f2228,plain,(
% 0.55/0.51    ![X0]: (~multiply(X0,sk_c6)=sk_c9|~inverse(X0)=sk_c9|~sQ47_spl|~sQ12_spl|~sQ7_spl|~sQ9_spl|~sQ8_spl|~sQ10_spl|~sQ4_spl|~sQ50_spl|~sQ48_spl|~sQ49_spl|~sQ11_spl|~sQ2_spl|~sQ6_spl|~sQ5_spl|~sQ0_spl|~sQ1_spl|~sQ16_spl)),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f2000,f872])).
% 0.55/0.51  fof(f2229,plain,(
% 0.55/0.51    ![X0]: (~multiply(X0,sk_c6)=sk_c6|~inverse(X0)=sk_c9|~sQ47_spl|~sQ12_spl|~sQ7_spl|~sQ9_spl|~sQ8_spl|~sQ10_spl|~sQ4_spl|~sQ50_spl|~sQ48_spl|~sQ49_spl|~sQ11_spl|~sQ2_spl|~sQ6_spl|~sQ5_spl|~sQ0_spl|~sQ1_spl|~sQ16_spl)),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f2000,f2228])).
% 0.55/0.51  fof(f2230,plain,(
% 0.55/0.51    ![X0]: (~multiply(X0,sk_c6)=sk_c6|~inverse(X0)=sk_c6|~sQ47_spl|~sQ12_spl|~sQ7_spl|~sQ9_spl|~sQ8_spl|~sQ10_spl|~sQ4_spl|~sQ50_spl|~sQ48_spl|~sQ49_spl|~sQ11_spl|~sQ2_spl|~sQ6_spl|~sQ5_spl|~sQ0_spl|~sQ1_spl|~sQ16_spl)),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f2000,f2229])).
% 0.55/0.51  fof(f2333,plain,(
% 0.55/0.51    ~inverse(inverse(sk_c6))=sk_c6|~sQ47_spl|~sQ16_spl|~sQ50_spl|~sQ48_spl|~sQ49_spl|~sQ11_spl|~sQ12_spl|~sQ7_spl|~sQ8_spl|~sQ10_spl|~sQ9_spl|~sQ4_spl|~sQ2_spl|~sQ0_spl|~sQ1_spl|~sQ6_spl|~sQ5_spl),
% 0.55/0.51    inference(resolution,[status(thm)],[f2230,f2006])).
% 0.55/0.51  fof(f2340,plain,(
% 0.55/0.51    ~inverse(sk_c6)=sk_c6|~sQ47_spl|~sQ16_spl|~sQ50_spl|~sQ48_spl|~sQ49_spl|~sQ11_spl|~sQ12_spl|~sQ7_spl|~sQ8_spl|~sQ10_spl|~sQ9_spl|~sQ4_spl|~sQ2_spl|~sQ0_spl|~sQ1_spl|~sQ6_spl|~sQ5_spl),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f1940,f2333])).
% 0.55/0.51  fof(f2341,plain,(
% 0.55/0.51    ~sk_c6=sk_c6|~sQ47_spl|~sQ16_spl|~sQ50_spl|~sQ48_spl|~sQ49_spl|~sQ11_spl|~sQ12_spl|~sQ7_spl|~sQ8_spl|~sQ10_spl|~sQ9_spl|~sQ4_spl|~sQ2_spl|~sQ0_spl|~sQ1_spl|~sQ6_spl|~sQ5_spl),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f1940,f2340])).
% 0.55/0.51  fof(f2342,plain,(
% 0.55/0.51    $false|~sQ47_spl|~sQ16_spl|~sQ50_spl|~sQ48_spl|~sQ49_spl|~sQ11_spl|~sQ12_spl|~sQ7_spl|~sQ8_spl|~sQ10_spl|~sQ9_spl|~sQ4_spl|~sQ2_spl|~sQ0_spl|~sQ1_spl|~sQ6_spl|~sQ5_spl),
% 0.55/0.51    inference(trivial_equality_resolution,[status(thm)],[f2341])).
% 0.55/0.51  fof(f2343,plain,(
% 0.55/0.51    ~sQ47_spl|~sQ16_spl|~sQ50_spl|~sQ48_spl|~sQ49_spl|~sQ11_spl|~sQ12_spl|~sQ7_spl|~sQ8_spl|~sQ10_spl|~sQ9_spl|~sQ4_spl|~sQ2_spl|~sQ0_spl|~sQ1_spl|~sQ6_spl|~sQ5_spl),
% 0.55/0.51    inference(contradiction_clause,[status(thm)],[f2342])).
% 0.55/0.51  fof(f2347,plain,(
% 0.55/0.51    ![X0]: (multiply(sk_c4,X0)=X0|~sQ4_spl|~sQ50_spl|~sQ2_spl|~sQ1_spl|~sQ48_spl|~sQ6_spl|~sQ5_spl)),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f1261,f65])).
% 0.55/0.51  fof(f2350,plain,(
% 0.55/0.51    inverse(sk_c4)=sk_c10|~sQ4_spl|~sQ50_spl|~sQ1_spl|~sQ6_spl|~sQ5_spl|~sQ48_spl|~sQ2_spl),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f1258,f1211])).
% 0.55/0.51  fof(f2351,plain,(
% 0.55/0.51    inverse(sk_c4)=sk_c4|~sQ4_spl|~sQ50_spl|~sQ1_spl|~sQ6_spl|~sQ5_spl|~sQ48_spl|~sQ2_spl),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f1427,f2350])).
% 0.55/0.51  fof(f2432,plain,(
% 0.55/0.51    sk_c7=multiply(sk_c8,sk_c4)|~sQ2_spl|~sQ1_spl|~sQ4_spl|~sQ50_spl|~sQ48_spl|~sQ6_spl|~sQ5_spl|~sQ9_spl|~sQ8_spl),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f1426,f797])).
% 0.55/0.51  fof(f2436,plain,(
% 0.55/0.51    sk_c8=multiply(sk_c8,sk_c4)|~sQ2_spl|~sQ1_spl|~sQ4_spl|~sQ50_spl|~sQ48_spl|~sQ6_spl|~sQ5_spl),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f1426,f1417])).
% 0.55/0.51  fof(f2444,plain,(
% 0.55/0.51    sk_c8=sk_c7|~sQ9_spl|~sQ8_spl|~sQ2_spl|~sQ1_spl|~sQ4_spl|~sQ50_spl|~sQ48_spl|~sQ6_spl|~sQ5_spl),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f2432,f2436])).
% 0.55/0.51  fof(f2459,plain,(
% 0.55/0.51    sk_c7=multiply(sk_c8,sk_c11)|~sQ9_spl|~sQ8_spl|~sQ2_spl|~sQ1_spl|~sQ4_spl|~sQ50_spl|~sQ48_spl|~sQ6_spl|~sQ5_spl),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f2444,f1419])).
% 0.55/0.51  fof(f2460,plain,(
% 0.55/0.51    sk_c7=multiply(sk_c7,sk_c11)|~sQ9_spl|~sQ8_spl|~sQ2_spl|~sQ1_spl|~sQ4_spl|~sQ50_spl|~sQ48_spl|~sQ6_spl|~sQ5_spl),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f2444,f2459])).
% 0.55/0.51  fof(f2461,plain,(
% 0.55/0.51    sk_c7=multiply(sk_c7,sk_c4)|~sQ9_spl|~sQ8_spl|~sQ2_spl|~sQ1_spl|~sQ4_spl|~sQ50_spl|~sQ48_spl|~sQ6_spl|~sQ5_spl),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f1426,f2460])).
% 0.55/0.51  fof(f2507,plain,(
% 0.55/0.51    multiply(sk_c7,sk_c4)=sk_c11|~sQ9_spl|~sQ8_spl|~sQ4_spl|~sQ50_spl|~sQ6_spl|~sQ5_spl|~sQ48_spl|~sQ2_spl|~sQ1_spl|~sQ7_spl),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f2444,f1262])).
% 0.55/0.51  fof(f2508,plain,(
% 0.55/0.51    sk_c7=sk_c4|~sQ9_spl|~sQ8_spl|~sQ7_spl|~sQ2_spl|~sQ1_spl|~sQ6_spl|~sQ5_spl|~sQ4_spl|~sQ50_spl|~sQ48_spl),
% 0.55/0.51    inference(backward_demodulation,[status(thm)],[f2509,f1426])).
% 0.55/0.51  fof(f2509,plain,(
% 0.55/0.51    sk_c7=sk_c11|~sQ9_spl|~sQ8_spl|~sQ4_spl|~sQ50_spl|~sQ6_spl|~sQ5_spl|~sQ48_spl|~sQ2_spl|~sQ1_spl|~sQ7_spl),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f2461,f2507])).
% 0.55/0.51  fof(f2517,plain,(
% 0.55/0.51    inverse(sk_c4)=sk_c7|~sQ9_spl|~sQ8_spl|~sQ7_spl|~sQ4_spl|~sQ50_spl|~sQ1_spl|~sQ6_spl|~sQ5_spl|~sQ48_spl|~sQ2_spl),
% 0.55/0.51    inference(backward_demodulation,[status(thm)],[f2508,f2351])).
% 0.55/0.51  fof(f2518,plain,(
% 0.55/0.51    ![X0]: (multiply(sk_c7,X0)=X0|~sQ9_spl|~sQ8_spl|~sQ7_spl|~sQ4_spl|~sQ50_spl|~sQ2_spl|~sQ1_spl|~sQ48_spl|~sQ6_spl|~sQ5_spl)),
% 0.55/0.51    inference(backward_demodulation,[status(thm)],[f2508,f2347])).
% 0.55/0.51  fof(f2520,plain,(
% 0.55/0.51    sk_c10=sk_c7|~sQ9_spl|~sQ8_spl|~sQ7_spl|~sQ48_spl|~sQ2_spl|~sQ1_spl|~sQ6_spl|~sQ5_spl|~sQ4_spl|~sQ50_spl),
% 0.55/0.51    inference(backward_demodulation,[status(thm)],[f2508,f1427])).
% 0.55/0.51  fof(f2521,plain,(
% 0.55/0.51    sk_c9=sk_c7|~sQ9_spl|~sQ8_spl|~sQ7_spl|~sQ2_spl|~sQ1_spl|~sQ4_spl|~sQ50_spl|~sQ48_spl|~sQ11_spl|~sQ6_spl|~sQ5_spl|~sQ49_spl),
% 0.55/0.51    inference(backward_demodulation,[status(thm)],[f2508,f1924])).
% 0.55/0.51  fof(f2523,plain,(
% 0.55/0.51    inverse(sk_c7)=sk_c7|~sQ9_spl|~sQ8_spl|~sQ7_spl|~sQ4_spl|~sQ50_spl|~sQ1_spl|~sQ6_spl|~sQ5_spl|~sQ48_spl|~sQ2_spl),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f2508,f2517])).
% 0.55/0.51  fof(f2524,plain,(
% 0.55/0.51    sk_c6=sk_c7|~sQ9_spl|~sQ8_spl|~sQ7_spl|~sQ4_spl|~sQ50_spl|~sQ1_spl|~sQ6_spl|~sQ5_spl|~sQ48_spl|~sQ2_spl),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f162,f2523])).
% 0.55/0.51  fof(f2527,plain,(
% 0.55/0.51    sk_c6=sk_c11|~sQ9_spl|~sQ8_spl|~sQ4_spl|~sQ50_spl|~sQ6_spl|~sQ5_spl|~sQ48_spl|~sQ2_spl|~sQ1_spl|~sQ7_spl),
% 0.55/0.51    inference(backward_demodulation,[status(thm)],[f2524,f2509])).
% 0.55/0.51  fof(f2533,plain,(
% 0.55/0.51    sk_c10=sk_c6|~sQ9_spl|~sQ8_spl|~sQ7_spl|~sQ48_spl|~sQ2_spl|~sQ1_spl|~sQ6_spl|~sQ5_spl|~sQ4_spl|~sQ50_spl),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f2524,f2520])).
% 0.55/0.51  fof(f2534,plain,(
% 0.55/0.51    sk_c9=sk_c6|~sQ9_spl|~sQ8_spl|~sQ7_spl|~sQ2_spl|~sQ1_spl|~sQ4_spl|~sQ50_spl|~sQ48_spl|~sQ11_spl|~sQ6_spl|~sQ5_spl|~sQ49_spl),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f2524,f2521])).
% 0.55/0.51  fof(f2536,plain,(
% 0.55/0.51    ![X0]: (multiply(sk_c6,X0)=X0|~sQ9_spl|~sQ8_spl|~sQ7_spl|~sQ4_spl|~sQ50_spl|~sQ2_spl|~sQ1_spl|~sQ48_spl|~sQ6_spl|~sQ5_spl)),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f2524,f2518])).
% 0.55/0.51  fof(f2596,plain,(
% 0.55/0.51    ~multiply(sk_c6,sk_c10)=sk_c9|~sQ9_spl|~sQ8_spl|~sQ4_spl|~sQ50_spl|~sQ6_spl|~sQ5_spl|~sQ48_spl|~sQ2_spl|~sQ1_spl|~sQ7_spl|sQ0_spl),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f2527,f132])).
% 0.55/0.51  fof(f2597,plain,(
% 0.55/0.51    ~sk_c10=sk_c9|~sQ9_spl|~sQ8_spl|~sQ4_spl|~sQ50_spl|~sQ6_spl|~sQ5_spl|~sQ48_spl|~sQ2_spl|~sQ1_spl|~sQ7_spl|sQ0_spl),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f2536,f2596])).
% 0.55/0.51  fof(f2598,plain,(
% 0.55/0.51    ~sk_c6=sk_c9|~sQ9_spl|~sQ8_spl|~sQ4_spl|~sQ50_spl|~sQ6_spl|~sQ5_spl|~sQ48_spl|~sQ2_spl|~sQ1_spl|~sQ7_spl|sQ0_spl),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f2533,f2597])).
% 0.55/0.51  fof(f2599,plain,(
% 0.55/0.51    ~sk_c6=sk_c6|~sQ11_spl|~sQ49_spl|~sQ9_spl|~sQ8_spl|~sQ4_spl|~sQ50_spl|~sQ6_spl|~sQ5_spl|~sQ48_spl|~sQ2_spl|~sQ1_spl|~sQ7_spl|sQ0_spl),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f2534,f2598])).
% 0.55/0.51  fof(f2600,plain,(
% 0.55/0.51    $false|~sQ11_spl|~sQ49_spl|~sQ9_spl|~sQ8_spl|~sQ4_spl|~sQ50_spl|~sQ6_spl|~sQ5_spl|~sQ48_spl|~sQ2_spl|~sQ1_spl|~sQ7_spl|sQ0_spl),
% 0.55/0.51    inference(trivial_equality_resolution,[status(thm)],[f2599])).
% 0.55/0.51  fof(f2601,plain,(
% 0.55/0.51    ~sQ11_spl|~sQ49_spl|~sQ9_spl|~sQ8_spl|~sQ4_spl|~sQ50_spl|~sQ6_spl|~sQ5_spl|~sQ48_spl|~sQ2_spl|~sQ1_spl|~sQ7_spl|sQ0_spl),
% 0.55/0.51    inference(contradiction_clause,[status(thm)],[f2600])).
% 0.55/0.51  fof(f2602,plain,(
% 0.55/0.51    inverse(sk_c10)=sk_c9|~sQ48_spl|~sQ11_spl),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f722,f174])).
% 0.55/0.51  fof(f2609,plain,(
% 0.55/0.51    ~inverse(identity)=sk_c10|~sQ48_spl|sQ49_spl),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f722,f726])).
% 0.55/0.51  fof(f2610,plain,(
% 0.55/0.51    multiply(sk_c9,sk_c10)=sk_c10|~sQ48_spl|~sQ12_spl),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f722,f187])).
% 0.55/0.51  fof(f2614,plain,(
% 0.55/0.51    multiply(sk_c9,sk_c10)=identity|~sQ48_spl|~sQ11_spl),
% 0.55/0.51    inference(paramodulation,[status(thm)],[f2602,f66])).
% 0.55/0.51  fof(f2617,plain,(
% 0.55/0.51    sk_c10=identity|~sQ12_spl|~sQ48_spl|~sQ11_spl),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f2610,f2614])).
% 0.55/0.51  fof(f2622,plain,(
% 0.55/0.51    multiply(sk_c10,sk_c10)=sk_c9|~sQ48_spl|~sQ0_spl),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f722,f131])).
% 0.55/0.51  fof(f2630,plain,(
% 0.55/0.51    ![X0]: (multiply(inverse(X0),X0)=sk_c10|~sQ12_spl|~sQ48_spl|~sQ11_spl)),
% 0.55/0.51    inference(backward_demodulation,[status(thm)],[f2617,f66])).
% 0.55/0.51  fof(f2631,plain,(
% 0.55/0.51    ~inverse(sk_c10)=sk_c10|~sQ12_spl|~sQ11_spl|~sQ48_spl|sQ49_spl),
% 0.55/0.51    inference(backward_demodulation,[status(thm)],[f2617,f2609])).
% 0.55/0.51  fof(f2632,plain,(
% 0.55/0.51    ![X0]: (multiply(sk_c10,X0)=X0|~sQ12_spl|~sQ48_spl|~sQ11_spl)),
% 0.55/0.51    inference(backward_demodulation,[status(thm)],[f2617,f65])).
% 0.55/0.51  fof(f2633,plain,(
% 0.55/0.51    ~sk_c9=sk_c10|~sQ12_spl|~sQ11_spl|~sQ48_spl|sQ49_spl),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f2602,f2631])).
% 0.55/0.51  fof(f2634,plain,(
% 0.55/0.51    sk_c10=sk_c9|~sQ12_spl|~sQ11_spl|~sQ48_spl|~sQ0_spl),
% 0.55/0.51    inference(backward_demodulation,[status(thm)],[f2632,f2622])).
% 0.55/0.51  fof(f2635,plain,(
% 0.55/0.51    ![X0]: (X0=multiply(inverse(sk_c10),X0)|~sQ12_spl|~sQ48_spl|~sQ11_spl)),
% 0.55/0.51    inference(paramodulation,[status(thm)],[f2632,f360])).
% 0.55/0.51  fof(f2637,plain,(
% 0.55/0.51    sQ50_spl|~sQ12_spl|~sQ11_spl|~sQ48_spl|~sQ0_spl),
% 0.55/0.51    inference(split_clause,[status(thm)],[f2634,f753,f186,f173,f721,f130])).
% 0.55/0.51  fof(f2638,plain,(
% 0.55/0.51    ![X0]: (X0=multiply(sk_c9,X0)|~sQ12_spl|~sQ48_spl|~sQ11_spl)),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f2602,f2635])).
% 0.55/0.51  fof(f2641,plain,(
% 0.55/0.51    ![X0,X1]: (~multiply(X0,inverse(X0))=sk_c10|~multiply(inverse(X0),sk_c10)=sk_c11|~inverse(inverse(X1))=inverse(X0)|~multiply(X1,inverse(X0))=inverse(X1)|~sQ48_spl|~sQ19_spl)),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f722,f251])).
% 0.55/0.51  fof(f2642,plain,(
% 0.55/0.51    ![X0,X1]: (~multiply(X0,inverse(X0))=sk_c10|~multiply(inverse(X0),sk_c10)=sk_c10|~inverse(inverse(X1))=inverse(X0)|~multiply(X1,inverse(X0))=inverse(X1)|~sQ48_spl|~sQ19_spl)),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f722,f2641])).
% 0.55/0.51  fof(f2643,plain,(
% 0.55/0.51    ~sQ50_spl|~sQ12_spl|~sQ11_spl|~sQ48_spl|sQ49_spl),
% 0.55/0.51    inference(split_clause,[status(thm)],[f2633,f753,f186,f173,f721,f724])).
% 0.55/0.51  fof(f2645,plain,(
% 0.55/0.51    multiply(sk_c10,sk_c2)=sk_c9|~sQ48_spl|~sQ50_spl|~sQ13_spl),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f722,f1424])).
% 0.55/0.51  fof(f2646,plain,(
% 0.55/0.51    sk_c2=sk_c9|~sQ12_spl|~sQ11_spl|~sQ48_spl|~sQ50_spl|~sQ13_spl),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f2632,f2645])).
% 0.55/0.51  fof(f2654,plain,(
% 0.55/0.51    sk_c2=identity|~sQ13_spl|~sQ50_spl|~sQ12_spl|~sQ48_spl|~sQ11_spl),
% 0.55/0.51    inference(backward_demodulation,[status(thm)],[f2660,f2617])).
% 0.55/0.51  fof(f2659,plain,(
% 0.55/0.51    inverse(sk_c1)=sk_c2|~sQ12_spl|~sQ11_spl|~sQ48_spl|~sQ50_spl|~sQ13_spl|~sQ14_spl|~sQ15_spl),
% 0.55/0.51    inference(backward_demodulation,[status(thm)],[f2660,f464])).
% 0.55/0.51  fof(f2660,plain,(
% 0.55/0.51    sk_c10=sk_c2|~sQ12_spl|~sQ11_spl|~sQ48_spl|~sQ13_spl|~sQ50_spl),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f2646,f754])).
% 0.55/0.51  fof(f2664,plain,(
% 0.55/0.51    ![X0]: (X0=multiply(sk_c2,X0)|~sQ50_spl|~sQ13_spl|~sQ12_spl|~sQ48_spl|~sQ11_spl)),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f2646,f2638])).
% 0.55/0.51  fof(f2670,plain,(
% 0.55/0.51    ![X0]: (X0=multiply(sk_c2,multiply(sk_c1,X0))|~sQ12_spl|~sQ11_spl|~sQ48_spl|~sQ50_spl|~sQ13_spl|~sQ14_spl|~sQ15_spl)),
% 0.55/0.51    inference(paramodulation,[status(thm)],[f2659,f360])).
% 0.55/0.51  fof(f2671,plain,(
% 0.55/0.51    ![X0]: (X0=multiply(sk_c1,X0)|~sQ12_spl|~sQ11_spl|~sQ48_spl|~sQ50_spl|~sQ13_spl|~sQ14_spl|~sQ15_spl)),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f2664,f2670])).
% 0.55/0.51  fof(f2693,plain,(
% 0.55/0.51    multiply(sk_c2,sk_c1)=identity|~sQ12_spl|~sQ11_spl|~sQ48_spl|~sQ50_spl|~sQ13_spl|~sQ14_spl|~sQ15_spl),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f2660,f452])).
% 0.55/0.51  fof(f2694,plain,(
% 0.55/0.51    sk_c2=sk_c1|~sQ14_spl|~sQ15_spl|~sQ13_spl|~sQ50_spl|~sQ12_spl|~sQ48_spl|~sQ11_spl),
% 0.55/0.51    inference(backward_demodulation,[status(thm)],[f2695,f2654])).
% 0.55/0.51  fof(f2695,plain,(
% 0.55/0.51    sk_c1=identity|~sQ12_spl|~sQ11_spl|~sQ48_spl|~sQ50_spl|~sQ13_spl|~sQ14_spl|~sQ15_spl),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f2664,f2693])).
% 0.55/0.51  fof(f2697,plain,(
% 0.55/0.51    inverse(sk_c1)=sk_c1|~sQ12_spl|~sQ11_spl|~sQ48_spl|~sQ50_spl|~sQ13_spl|~sQ14_spl|~sQ15_spl),
% 0.55/0.51    inference(backward_demodulation,[status(thm)],[f2694,f2659])).
% 0.55/0.51  fof(f2703,plain,(
% 0.55/0.51    sk_c10=sk_c1|~sQ14_spl|~sQ15_spl|~sQ12_spl|~sQ11_spl|~sQ48_spl|~sQ13_spl|~sQ50_spl),
% 0.55/0.51    inference(backward_demodulation,[status(thm)],[f2694,f2660])).
% 0.55/0.51  fof(f2705,plain,(
% 0.55/0.51    sk_c1=sk_c9|~sQ14_spl|~sQ15_spl|~sQ12_spl|~sQ11_spl|~sQ48_spl|~sQ50_spl|~sQ13_spl),
% 0.55/0.51    inference(backward_demodulation,[status(thm)],[f2694,f2646])).
% 0.55/0.51  fof(f2753,plain,(
% 0.55/0.51    ![X0]: (multiply(inverse(X0),X0)=sk_c1|~sQ14_spl|~sQ15_spl|~sQ13_spl|~sQ50_spl|~sQ12_spl|~sQ48_spl|~sQ11_spl)),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f2703,f2630])).
% 0.55/0.51  fof(f2761,plain,(
% 0.55/0.51    ![X0,X1]: (~multiply(X0,inverse(X0))=sk_c1|~multiply(inverse(X0),sk_c10)=sk_c10|~inverse(inverse(X1))=inverse(X0)|~multiply(X1,inverse(X0))=inverse(X1)|~sQ14_spl|~sQ15_spl|~sQ12_spl|~sQ11_spl|~sQ13_spl|~sQ50_spl|~sQ48_spl|~sQ19_spl)),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f2703,f2642])).
% 0.55/0.51  fof(f2762,plain,(
% 0.55/0.51    ![X0,X1]: (~multiply(X0,inverse(X0))=sk_c1|~multiply(inverse(X0),sk_c1)=sk_c10|~inverse(inverse(X1))=inverse(X0)|~multiply(X1,inverse(X0))=inverse(X1)|~sQ14_spl|~sQ15_spl|~sQ12_spl|~sQ11_spl|~sQ13_spl|~sQ50_spl|~sQ48_spl|~sQ19_spl)),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f2703,f2761])).
% 0.55/0.51  fof(f2763,plain,(
% 0.55/0.51    ![X0,X1]: (~multiply(X0,inverse(X0))=sk_c1|~multiply(inverse(X0),sk_c1)=sk_c1|~inverse(inverse(X1))=inverse(X0)|~multiply(X1,inverse(X0))=inverse(X1)|~sQ14_spl|~sQ15_spl|~sQ12_spl|~sQ11_spl|~sQ13_spl|~sQ50_spl|~sQ48_spl|~sQ19_spl)),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f2703,f2762])).
% 0.55/0.51  fof(f2765,plain,(
% 0.55/0.51    ~multiply(sk_c1,inverse(sk_c1))=sk_c1|~multiply(inverse(sk_c1),sk_c1)=sk_c1|~inverse(inverse(sk_c1))=inverse(sk_c1)|~sQ19_spl|~sQ12_spl|~sQ11_spl|~sQ48_spl|~sQ50_spl|~sQ13_spl|~sQ14_spl|~sQ15_spl),
% 0.55/0.51    inference(resolution,[status(thm)],[f2763,f2671])).
% 0.55/0.51  fof(f2781,plain,(
% 0.55/0.51    ~sQ54_spl|~sQ55_spl|~sQ56_spl|~sQ19_spl|~sQ12_spl|~sQ11_spl|~sQ48_spl|~sQ50_spl|~sQ13_spl|~sQ14_spl|~sQ15_spl),
% 0.55/0.51    inference(split_clause,[status(thm)],[f2765,f1363,f1366,f1369,f247,f186,f173,f721,f753,f199,f212,f225])).
% 0.55/0.51  fof(f2788,plain,(
% 0.55/0.51    ~sk_c1=sk_c1|~sQ14_spl|~sQ15_spl|~sQ13_spl|~sQ50_spl|~sQ12_spl|~sQ48_spl|~sQ11_spl|sQ55_spl),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f2753,f1368])).
% 0.55/0.51  fof(f2789,plain,(
% 0.55/0.51    $false|~sQ14_spl|~sQ15_spl|~sQ13_spl|~sQ50_spl|~sQ12_spl|~sQ48_spl|~sQ11_spl|sQ55_spl),
% 0.55/0.51    inference(trivial_equality_resolution,[status(thm)],[f2788])).
% 0.55/0.51  fof(f2790,plain,(
% 0.55/0.51    ~sQ14_spl|~sQ15_spl|~sQ13_spl|~sQ50_spl|~sQ12_spl|~sQ48_spl|~sQ11_spl|sQ55_spl),
% 0.55/0.51    inference(contradiction_clause,[status(thm)],[f2789])).
% 0.55/0.51  fof(f2791,plain,(
% 0.55/0.51    ~inverse(sk_c1)=sk_c1|~sQ12_spl|~sQ11_spl|~sQ48_spl|~sQ50_spl|~sQ13_spl|~sQ14_spl|~sQ15_spl|sQ54_spl),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f2671,f1365])).
% 0.55/0.51  fof(f2792,plain,(
% 0.55/0.51    ~sk_c1=sk_c1|~sQ12_spl|~sQ11_spl|~sQ48_spl|~sQ50_spl|~sQ13_spl|~sQ14_spl|~sQ15_spl|sQ54_spl),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f2697,f2791])).
% 0.55/0.51  fof(f2793,plain,(
% 0.55/0.51    $false|~sQ12_spl|~sQ11_spl|~sQ48_spl|~sQ50_spl|~sQ13_spl|~sQ14_spl|~sQ15_spl|sQ54_spl),
% 0.55/0.51    inference(trivial_equality_resolution,[status(thm)],[f2792])).
% 0.55/0.51  fof(f2794,plain,(
% 0.55/0.51    ~sQ12_spl|~sQ11_spl|~sQ48_spl|~sQ50_spl|~sQ13_spl|~sQ14_spl|~sQ15_spl|sQ54_spl),
% 0.55/0.51    inference(contradiction_clause,[status(thm)],[f2793])).
% 0.55/0.51  fof(f2811,plain,(
% 0.55/0.51    ~multiply(sk_c1,sk_c10)=sk_c10|~sQ14_spl|~sQ15_spl|~sQ12_spl|~sQ11_spl|~sQ48_spl|~sQ13_spl|~sQ50_spl|sQ42_spl),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f2703,f692])).
% 0.55/0.51  fof(f2812,plain,(
% 0.55/0.51    ~sk_c10=sk_c10|~sQ14_spl|~sQ15_spl|~sQ12_spl|~sQ11_spl|~sQ48_spl|~sQ13_spl|~sQ50_spl|sQ42_spl),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f2671,f2811])).
% 0.55/0.51  fof(f2813,plain,(
% 0.55/0.51    ~sk_c1=sk_c10|~sQ14_spl|~sQ15_spl|~sQ12_spl|~sQ11_spl|~sQ48_spl|~sQ13_spl|~sQ50_spl|sQ42_spl),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f2703,f2812])).
% 0.55/0.51  fof(f2814,plain,(
% 0.55/0.51    ~sk_c1=sk_c1|~sQ14_spl|~sQ15_spl|~sQ12_spl|~sQ11_spl|~sQ48_spl|~sQ13_spl|~sQ50_spl|sQ42_spl),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f2703,f2813])).
% 0.55/0.51  fof(f2815,plain,(
% 0.55/0.51    $false|~sQ14_spl|~sQ15_spl|~sQ12_spl|~sQ11_spl|~sQ48_spl|~sQ13_spl|~sQ50_spl|sQ42_spl),
% 0.55/0.51    inference(trivial_equality_resolution,[status(thm)],[f2814])).
% 0.55/0.51  fof(f2816,plain,(
% 0.55/0.51    ~sQ14_spl|~sQ15_spl|~sQ12_spl|~sQ11_spl|~sQ48_spl|~sQ13_spl|~sQ50_spl|sQ42_spl),
% 0.55/0.51    inference(contradiction_clause,[status(thm)],[f2815])).
% 0.55/0.51  fof(f2820,plain,(
% 0.55/0.51    ~inverse(sk_c1)=inverse(sk_c1)|~sQ12_spl|~sQ11_spl|~sQ48_spl|~sQ50_spl|~sQ13_spl|~sQ14_spl|~sQ15_spl|sQ56_spl),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f2697,f1371])).
% 0.55/0.51  fof(f2821,plain,(
% 0.55/0.51    ~sk_c1=inverse(sk_c1)|~sQ12_spl|~sQ11_spl|~sQ48_spl|~sQ50_spl|~sQ13_spl|~sQ14_spl|~sQ15_spl|sQ56_spl),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f2697,f2820])).
% 0.55/0.51  fof(f2822,plain,(
% 0.55/0.51    ~sk_c1=sk_c1|~sQ12_spl|~sQ11_spl|~sQ48_spl|~sQ50_spl|~sQ13_spl|~sQ14_spl|~sQ15_spl|sQ56_spl),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f2697,f2821])).
% 0.55/0.51  fof(f2823,plain,(
% 0.55/0.51    $false|~sQ12_spl|~sQ11_spl|~sQ48_spl|~sQ50_spl|~sQ13_spl|~sQ14_spl|~sQ15_spl|sQ56_spl),
% 0.55/0.51    inference(trivial_equality_resolution,[status(thm)],[f2822])).
% 0.55/0.51  fof(f2824,plain,(
% 0.55/0.51    ~sQ12_spl|~sQ11_spl|~sQ48_spl|~sQ50_spl|~sQ13_spl|~sQ14_spl|~sQ15_spl|sQ56_spl),
% 0.55/0.51    inference(contradiction_clause,[status(thm)],[f2823])).
% 0.55/0.51  fof(f2827,plain,(
% 0.55/0.51    ~multiply(sk_c1,sk_c9)=sk_c10|~sQ14_spl|~sQ15_spl|~sQ12_spl|~sQ11_spl|~sQ48_spl|~sQ13_spl|~sQ50_spl|sQ41_spl),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f2703,f688])).
% 0.55/0.51  fof(f2828,plain,(
% 0.55/0.51    ~sk_c9=sk_c10|~sQ14_spl|~sQ15_spl|~sQ12_spl|~sQ11_spl|~sQ48_spl|~sQ13_spl|~sQ50_spl|sQ41_spl),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f2671,f2827])).
% 0.55/0.51  fof(f2829,plain,(
% 0.55/0.51    ~sk_c1=sk_c10|~sQ14_spl|~sQ15_spl|~sQ12_spl|~sQ11_spl|~sQ48_spl|~sQ13_spl|~sQ50_spl|sQ41_spl),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f2705,f2828])).
% 0.55/0.51  fof(f2830,plain,(
% 0.55/0.51    ~sk_c1=sk_c1|~sQ14_spl|~sQ15_spl|~sQ12_spl|~sQ11_spl|~sQ48_spl|~sQ13_spl|~sQ50_spl|sQ41_spl),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f2703,f2829])).
% 0.55/0.51  fof(f2831,plain,(
% 0.55/0.51    $false|~sQ14_spl|~sQ15_spl|~sQ12_spl|~sQ11_spl|~sQ48_spl|~sQ13_spl|~sQ50_spl|sQ41_spl),
% 0.55/0.51    inference(trivial_equality_resolution,[status(thm)],[f2830])).
% 0.55/0.51  fof(f2832,plain,(
% 0.55/0.51    ~sQ14_spl|~sQ15_spl|~sQ12_spl|~sQ11_spl|~sQ48_spl|~sQ13_spl|~sQ50_spl|sQ41_spl),
% 0.55/0.51    inference(contradiction_clause,[status(thm)],[f2831])).
% 0.55/0.51  fof(f2839,plain,(
% 0.55/0.51    ~inverse(sk_c1)=sk_c10|~sQ12_spl|~sQ11_spl|~sQ48_spl|~sQ50_spl|~sQ13_spl|~sQ14_spl|~sQ15_spl|sQ51_spl),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f2695,f758])).
% 0.55/0.51  fof(f2840,plain,(
% 0.55/0.51    ~sk_c1=sk_c10|~sQ12_spl|~sQ11_spl|~sQ48_spl|~sQ50_spl|~sQ13_spl|~sQ14_spl|~sQ15_spl|sQ51_spl),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f2697,f2839])).
% 0.55/0.51  fof(f2841,plain,(
% 0.55/0.51    ~sk_c1=sk_c1|~sQ12_spl|~sQ11_spl|~sQ48_spl|~sQ50_spl|~sQ13_spl|~sQ14_spl|~sQ15_spl|sQ51_spl),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f2703,f2840])).
% 0.55/0.51  fof(f2842,plain,(
% 0.55/0.51    $false|~sQ12_spl|~sQ11_spl|~sQ48_spl|~sQ50_spl|~sQ13_spl|~sQ14_spl|~sQ15_spl|sQ51_spl),
% 0.55/0.51    inference(trivial_equality_resolution,[status(thm)],[f2841])).
% 0.55/0.51  fof(f2843,plain,(
% 0.55/0.51    ~sQ12_spl|~sQ11_spl|~sQ48_spl|~sQ50_spl|~sQ13_spl|~sQ14_spl|~sQ15_spl|sQ51_spl),
% 0.55/0.51    inference(contradiction_clause,[status(thm)],[f2842])).
% 0.55/0.51  fof(f2849,plain,(
% 0.55/0.51    ~inverse(sk_c1)=sk_c9|~sQ14_spl|~sQ15_spl|~sQ12_spl|~sQ11_spl|~sQ48_spl|~sQ13_spl|~sQ50_spl|sQ47_spl),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f2705,f1116])).
% 0.55/0.51  fof(f2850,plain,(
% 0.55/0.51    ~sk_c1=sk_c9|~sQ14_spl|~sQ15_spl|~sQ12_spl|~sQ11_spl|~sQ48_spl|~sQ13_spl|~sQ50_spl|sQ47_spl),
% 0.55/0.51    inference(forward_demodulation,[status(thm)],[f2697,f2849])).
% 0.55/0.52  fof(f2851,plain,(
% 0.55/0.52    ~sk_c1=sk_c1|~sQ14_spl|~sQ15_spl|~sQ12_spl|~sQ11_spl|~sQ48_spl|~sQ13_spl|~sQ50_spl|sQ47_spl),
% 0.55/0.52    inference(forward_demodulation,[status(thm)],[f2705,f2850])).
% 0.55/0.52  fof(f2852,plain,(
% 0.55/0.52    $false|~sQ14_spl|~sQ15_spl|~sQ12_spl|~sQ11_spl|~sQ48_spl|~sQ13_spl|~sQ50_spl|sQ47_spl),
% 0.55/0.52    inference(trivial_equality_resolution,[status(thm)],[f2851])).
% 0.55/0.52  fof(f2853,plain,(
% 0.55/0.52    ~sQ14_spl|~sQ15_spl|~sQ12_spl|~sQ11_spl|~sQ48_spl|~sQ13_spl|~sQ50_spl|sQ47_spl),
% 0.55/0.52    inference(contradiction_clause,[status(thm)],[f2852])).
% 0.55/0.52  fof(f2854,plain,(
% 0.55/0.52    $false),
% 0.55/0.52    inference(sat_refutation,[status(thm)],[f136,f140,f144,f148,f152,f156,f160,f164,f168,f176,f177,f178,f179,f180,f181,f182,f184,f189,f190,f193,f194,f195,f197,f202,f203,f205,f206,f207,f208,f209,f210,f211,f215,f216,f218,f219,f220,f221,f223,f228,f229,f231,f232,f233,f234,f236,f250,f281,f311,f331,f351,f390,f404,f409,f700,f711,f727,f752,f759,f769,f811,f813,f831,f851,f852,f1003,f1004,f1060,f1099,f1187,f1223,f1271,f1289,f1372,f1391,f1395,f1408,f1891,f1909,f1913,f1920,f2205,f2216,f2220,f2226,f2343,f2601,f2637,f2643,f2781,f2790,f2794,f2816,f2824,f2832,f2843,f2853])).
% 0.55/0.52  % SZS output end CNFRefutation for theBenchmark.p
% 0.55/0.52  % Elapsed time: 0.139093 seconds
% 0.55/0.52  % CPU time: 0.785250 seconds
% 0.55/0.52  % Total memory used: 121.392 MB
% 0.55/0.52  % Net memory used: 120.757 MB
%------------------------------------------------------------------------------