%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : GRP366-1 : TPTP v9.3.1. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 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 : Fri Sep 25 01:33:24 PM UTC 2026
% Result : Unsatisfiable 39.01s 25.69s
% Output : CNFRefutation 39.01s
% Verified :
% SZS Type : Refutation
% Derivation depth : 49
% Number of leaves : 64
% Syntax : Number of formulae : 771 ( 127 unt; 0 def)
% Number of atoms : 1881 (1706 equ)
% Maximal formula atoms : 16 ( 2 avg)
% Number of connectives : 1890 ( 780 ~;1110 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 24 ( 3 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 7 ( 5 usr; 6 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 11 con; 0-2 aty)
% Number of variables : 359 ( 0 sgn 359 !; 0 ?; 328 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0] : multiply(identity,X0) = X0,
file('/export/starexec/sandbox/benchmark/Axioms/GRP004-0.ax',left_identity) ).
fof(f2,axiom,
! [X0] : multiply(inverse(X0),X0) = identity,
file('/export/starexec/sandbox/benchmark/Axioms/GRP004-0.ax',left_inverse) ).
fof(f3,plain,
! [X0] : identity = multiply(inverse(X0),X0),
inference(reorient_equations,[],[f2]) ).
fof(f4,axiom,
! [X2,X0,X1] : multiply(multiply(X0,X1),X2) = multiply(X0,multiply(X1,X2)),
file('/export/starexec/sandbox/benchmark/Axioms/GRP004-0.ax',associativity) ).
fof(f5,negated_conjecture,
( multiply(sk_c9,sk_c10) = sk_c8
| multiply(sk_c8,sk_c10) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_1) ).
fof(f6,plain,
( sk_c8 = multiply(sk_c9,sk_c10)
| multiply(sk_c8,sk_c10) = sk_c9 ),
inference(reorient_equations,[],[f5]) ).
fof(f7,negated_conjecture,
( multiply(sk_c4,sk_c10) = sk_c9
| multiply(sk_c8,sk_c10) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_2) ).
fof(f8,plain,
( sk_c9 = multiply(sk_c4,sk_c10)
| multiply(sk_c8,sk_c10) = sk_c9 ),
inference(reorient_equations,[],[f7]) ).
fof(f9,negated_conjecture,
( inverse(sk_c4) = sk_c10
| multiply(sk_c8,sk_c10) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_3) ).
fof(f10,plain,
( sk_c10 = inverse(sk_c4)
| multiply(sk_c8,sk_c10) = sk_c9 ),
inference(reorient_equations,[],[f9]) ).
fof(f11,negated_conjecture,
( inverse(sk_c9) = sk_c8
| multiply(sk_c8,sk_c10) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_4) ).
fof(f12,plain,
( sk_c8 = inverse(sk_c9)
| multiply(sk_c8,sk_c10) = sk_c9 ),
inference(reorient_equations,[],[f11]) ).
fof(f13,negated_conjecture,
( multiply(sk_c10,sk_c8) = sk_c9
| multiply(sk_c8,sk_c10) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_5) ).
fof(f14,plain,
( sk_c9 = multiply(sk_c10,sk_c8)
| multiply(sk_c8,sk_c10) = sk_c9 ),
inference(reorient_equations,[],[f13]) ).
fof(f15,negated_conjecture,
( inverse(sk_c5) = sk_c9
| multiply(sk_c8,sk_c10) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_6) ).
fof(f16,plain,
( sk_c9 = inverse(sk_c5)
| multiply(sk_c8,sk_c10) = sk_c9 ),
inference(reorient_equations,[],[f15]) ).
fof(f17,negated_conjecture,
( multiply(sk_c5,sk_c8) = sk_c9
| multiply(sk_c8,sk_c10) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_7) ).
fof(f18,plain,
( sk_c9 = multiply(sk_c5,sk_c8)
| multiply(sk_c8,sk_c10) = sk_c9 ),
inference(reorient_equations,[],[f17]) ).
fof(f20,negated_conjecture,
( inverse(sk_c6) = sk_c10
| multiply(sk_c8,sk_c10) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_9) ).
fof(f21,plain,
( sk_c10 = inverse(sk_c6)
| multiply(sk_c8,sk_c10) = sk_c9 ),
inference(reorient_equations,[],[f20]) ).
fof(f24,negated_conjecture,
( multiply(sk_c9,sk_c10) = sk_c8
| multiply(sk_c10,sk_c2) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_11) ).
fof(f25,plain,
( sk_c8 = multiply(sk_c9,sk_c10)
| sk_c9 = multiply(sk_c10,sk_c2) ),
inference(reorient_equations,[],[f24]) ).
fof(f26,negated_conjecture,
( multiply(sk_c4,sk_c10) = sk_c9
| multiply(sk_c10,sk_c2) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_12) ).
fof(f27,plain,
( sk_c9 = multiply(sk_c4,sk_c10)
| sk_c9 = multiply(sk_c10,sk_c2) ),
inference(reorient_equations,[],[f26]) ).
fof(f28,negated_conjecture,
( inverse(sk_c4) = sk_c10
| multiply(sk_c10,sk_c2) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_13) ).
fof(f29,plain,
( sk_c10 = inverse(sk_c4)
| sk_c9 = multiply(sk_c10,sk_c2) ),
inference(reorient_equations,[],[f28]) ).
fof(f30,negated_conjecture,
( inverse(sk_c9) = sk_c8
| multiply(sk_c10,sk_c2) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_14) ).
fof(f31,plain,
( sk_c8 = inverse(sk_c9)
| sk_c9 = multiply(sk_c10,sk_c2) ),
inference(reorient_equations,[],[f30]) ).
fof(f32,negated_conjecture,
( multiply(sk_c10,sk_c8) = sk_c9
| multiply(sk_c10,sk_c2) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_15) ).
fof(f33,plain,
( sk_c9 = multiply(sk_c10,sk_c8)
| sk_c9 = multiply(sk_c10,sk_c2) ),
inference(reorient_equations,[],[f32]) ).
fof(f34,negated_conjecture,
( inverse(sk_c5) = sk_c9
| multiply(sk_c10,sk_c2) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_16) ).
fof(f35,plain,
( sk_c9 = inverse(sk_c5)
| sk_c9 = multiply(sk_c10,sk_c2) ),
inference(reorient_equations,[],[f34]) ).
fof(f36,negated_conjecture,
( multiply(sk_c5,sk_c8) = sk_c9
| multiply(sk_c10,sk_c2) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_17) ).
fof(f37,plain,
( sk_c9 = multiply(sk_c5,sk_c8)
| sk_c9 = multiply(sk_c10,sk_c2) ),
inference(reorient_equations,[],[f36]) ).
fof(f38,negated_conjecture,
( inverse(sk_c7) = sk_c6
| multiply(sk_c10,sk_c2) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_18) ).
fof(f39,plain,
( inverse(sk_c7) = sk_c6
| sk_c9 = multiply(sk_c10,sk_c2) ),
inference(reorient_equations,[],[f38]) ).
fof(f40,negated_conjecture,
( inverse(sk_c6) = sk_c10
| multiply(sk_c10,sk_c2) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_19) ).
fof(f41,plain,
( sk_c10 = inverse(sk_c6)
| sk_c9 = multiply(sk_c10,sk_c2) ),
inference(reorient_equations,[],[f40]) ).
fof(f42,negated_conjecture,
( multiply(sk_c7,sk_c10) = sk_c6
| multiply(sk_c10,sk_c2) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_20) ).
fof(f43,plain,
( sk_c6 = multiply(sk_c7,sk_c10)
| sk_c9 = multiply(sk_c10,sk_c2) ),
inference(reorient_equations,[],[f42]) ).
fof(f44,negated_conjecture,
( multiply(sk_c9,sk_c10) = sk_c8
| multiply(sk_c1,sk_c10) = sk_c2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_21) ).
fof(f45,plain,
( sk_c8 = multiply(sk_c9,sk_c10)
| sk_c2 = multiply(sk_c1,sk_c10) ),
inference(reorient_equations,[],[f44]) ).
fof(f46,negated_conjecture,
( multiply(sk_c4,sk_c10) = sk_c9
| multiply(sk_c1,sk_c10) = sk_c2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_22) ).
fof(f47,plain,
( sk_c9 = multiply(sk_c4,sk_c10)
| sk_c2 = multiply(sk_c1,sk_c10) ),
inference(reorient_equations,[],[f46]) ).
fof(f48,negated_conjecture,
( inverse(sk_c4) = sk_c10
| multiply(sk_c1,sk_c10) = sk_c2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_23) ).
fof(f49,plain,
( sk_c10 = inverse(sk_c4)
| sk_c2 = multiply(sk_c1,sk_c10) ),
inference(reorient_equations,[],[f48]) ).
fof(f50,negated_conjecture,
( inverse(sk_c9) = sk_c8
| multiply(sk_c1,sk_c10) = sk_c2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_24) ).
fof(f51,plain,
( sk_c8 = inverse(sk_c9)
| sk_c2 = multiply(sk_c1,sk_c10) ),
inference(reorient_equations,[],[f50]) ).
fof(f52,negated_conjecture,
( multiply(sk_c10,sk_c8) = sk_c9
| multiply(sk_c1,sk_c10) = sk_c2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_25) ).
fof(f53,plain,
( sk_c9 = multiply(sk_c10,sk_c8)
| sk_c2 = multiply(sk_c1,sk_c10) ),
inference(reorient_equations,[],[f52]) ).
fof(f54,negated_conjecture,
( inverse(sk_c5) = sk_c9
| multiply(sk_c1,sk_c10) = sk_c2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_26) ).
fof(f55,plain,
( sk_c9 = inverse(sk_c5)
| sk_c2 = multiply(sk_c1,sk_c10) ),
inference(reorient_equations,[],[f54]) ).
fof(f56,negated_conjecture,
( multiply(sk_c5,sk_c8) = sk_c9
| multiply(sk_c1,sk_c10) = sk_c2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_27) ).
fof(f57,plain,
( sk_c9 = multiply(sk_c5,sk_c8)
| sk_c2 = multiply(sk_c1,sk_c10) ),
inference(reorient_equations,[],[f56]) ).
fof(f58,negated_conjecture,
( inverse(sk_c7) = sk_c6
| multiply(sk_c1,sk_c10) = sk_c2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_28) ).
fof(f59,plain,
( inverse(sk_c7) = sk_c6
| sk_c2 = multiply(sk_c1,sk_c10) ),
inference(reorient_equations,[],[f58]) ).
fof(f60,negated_conjecture,
( inverse(sk_c6) = sk_c10
| multiply(sk_c1,sk_c10) = sk_c2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_29) ).
fof(f61,plain,
( sk_c10 = inverse(sk_c6)
| sk_c2 = multiply(sk_c1,sk_c10) ),
inference(reorient_equations,[],[f60]) ).
fof(f62,negated_conjecture,
( multiply(sk_c7,sk_c10) = sk_c6
| multiply(sk_c1,sk_c10) = sk_c2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_30) ).
fof(f63,plain,
( sk_c6 = multiply(sk_c7,sk_c10)
| sk_c2 = multiply(sk_c1,sk_c10) ),
inference(reorient_equations,[],[f62]) ).
fof(f64,negated_conjecture,
( multiply(sk_c9,sk_c10) = sk_c8
| inverse(sk_c1) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_31) ).
fof(f65,plain,
( sk_c8 = multiply(sk_c9,sk_c10)
| sk_c10 = inverse(sk_c1) ),
inference(reorient_equations,[],[f64]) ).
fof(f66,negated_conjecture,
( multiply(sk_c4,sk_c10) = sk_c9
| inverse(sk_c1) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_32) ).
fof(f67,plain,
( sk_c9 = multiply(sk_c4,sk_c10)
| sk_c10 = inverse(sk_c1) ),
inference(reorient_equations,[],[f66]) ).
fof(f68,negated_conjecture,
( inverse(sk_c4) = sk_c10
| inverse(sk_c1) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_33) ).
fof(f69,plain,
( sk_c10 = inverse(sk_c4)
| sk_c10 = inverse(sk_c1) ),
inference(reorient_equations,[],[f68]) ).
fof(f70,negated_conjecture,
( inverse(sk_c9) = sk_c8
| inverse(sk_c1) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_34) ).
fof(f71,plain,
( sk_c8 = inverse(sk_c9)
| sk_c10 = inverse(sk_c1) ),
inference(reorient_equations,[],[f70]) ).
fof(f72,negated_conjecture,
( multiply(sk_c10,sk_c8) = sk_c9
| inverse(sk_c1) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_35) ).
fof(f73,plain,
( sk_c9 = multiply(sk_c10,sk_c8)
| sk_c10 = inverse(sk_c1) ),
inference(reorient_equations,[],[f72]) ).
fof(f74,negated_conjecture,
( inverse(sk_c5) = sk_c9
| inverse(sk_c1) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_36) ).
fof(f75,plain,
( sk_c9 = inverse(sk_c5)
| sk_c10 = inverse(sk_c1) ),
inference(reorient_equations,[],[f74]) ).
fof(f76,negated_conjecture,
( multiply(sk_c5,sk_c8) = sk_c9
| inverse(sk_c1) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_37) ).
fof(f77,plain,
( sk_c9 = multiply(sk_c5,sk_c8)
| sk_c10 = inverse(sk_c1) ),
inference(reorient_equations,[],[f76]) ).
fof(f78,negated_conjecture,
( inverse(sk_c7) = sk_c6
| inverse(sk_c1) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_38) ).
fof(f79,plain,
( inverse(sk_c7) = sk_c6
| sk_c10 = inverse(sk_c1) ),
inference(reorient_equations,[],[f78]) ).
fof(f80,negated_conjecture,
( inverse(sk_c6) = sk_c10
| inverse(sk_c1) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_39) ).
fof(f81,plain,
( sk_c10 = inverse(sk_c6)
| sk_c10 = inverse(sk_c1) ),
inference(reorient_equations,[],[f80]) ).
fof(f82,negated_conjecture,
( multiply(sk_c7,sk_c10) = sk_c6
| inverse(sk_c1) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_40) ).
fof(f83,plain,
( sk_c6 = multiply(sk_c7,sk_c10)
| sk_c10 = inverse(sk_c1) ),
inference(reorient_equations,[],[f82]) ).
fof(f84,negated_conjecture,
( multiply(sk_c9,sk_c10) = sk_c8
| multiply(sk_c3,sk_c8) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_41) ).
fof(f85,plain,
( sk_c8 = multiply(sk_c9,sk_c10)
| sk_c10 = multiply(sk_c3,sk_c8) ),
inference(reorient_equations,[],[f84]) ).
fof(f86,negated_conjecture,
( multiply(sk_c4,sk_c10) = sk_c9
| multiply(sk_c3,sk_c8) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_42) ).
fof(f87,plain,
( sk_c9 = multiply(sk_c4,sk_c10)
| sk_c10 = multiply(sk_c3,sk_c8) ),
inference(reorient_equations,[],[f86]) ).
fof(f88,negated_conjecture,
( inverse(sk_c4) = sk_c10
| multiply(sk_c3,sk_c8) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_43) ).
fof(f89,plain,
( sk_c10 = inverse(sk_c4)
| sk_c10 = multiply(sk_c3,sk_c8) ),
inference(reorient_equations,[],[f88]) ).
fof(f90,negated_conjecture,
( inverse(sk_c9) = sk_c8
| multiply(sk_c3,sk_c8) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_44) ).
fof(f91,plain,
( sk_c8 = inverse(sk_c9)
| sk_c10 = multiply(sk_c3,sk_c8) ),
inference(reorient_equations,[],[f90]) ).
fof(f92,negated_conjecture,
( multiply(sk_c10,sk_c8) = sk_c9
| multiply(sk_c3,sk_c8) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_45) ).
fof(f93,plain,
( sk_c9 = multiply(sk_c10,sk_c8)
| sk_c10 = multiply(sk_c3,sk_c8) ),
inference(reorient_equations,[],[f92]) ).
fof(f94,negated_conjecture,
( inverse(sk_c5) = sk_c9
| multiply(sk_c3,sk_c8) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_46) ).
fof(f95,plain,
( sk_c9 = inverse(sk_c5)
| sk_c10 = multiply(sk_c3,sk_c8) ),
inference(reorient_equations,[],[f94]) ).
fof(f96,negated_conjecture,
( multiply(sk_c5,sk_c8) = sk_c9
| multiply(sk_c3,sk_c8) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_47) ).
fof(f97,plain,
( sk_c9 = multiply(sk_c5,sk_c8)
| sk_c10 = multiply(sk_c3,sk_c8) ),
inference(reorient_equations,[],[f96]) ).
fof(f102,negated_conjecture,
( multiply(sk_c7,sk_c10) = sk_c6
| multiply(sk_c3,sk_c8) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_50) ).
fof(f103,plain,
( sk_c6 = multiply(sk_c7,sk_c10)
| sk_c10 = multiply(sk_c3,sk_c8) ),
inference(reorient_equations,[],[f102]) ).
fof(f104,negated_conjecture,
( multiply(sk_c9,sk_c10) = sk_c8
| inverse(sk_c3) = sk_c8 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_51) ).
fof(f105,plain,
( sk_c8 = multiply(sk_c9,sk_c10)
| sk_c8 = inverse(sk_c3) ),
inference(reorient_equations,[],[f104]) ).
fof(f106,negated_conjecture,
( multiply(sk_c4,sk_c10) = sk_c9
| inverse(sk_c3) = sk_c8 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_52) ).
fof(f107,plain,
( sk_c9 = multiply(sk_c4,sk_c10)
| sk_c8 = inverse(sk_c3) ),
inference(reorient_equations,[],[f106]) ).
fof(f108,negated_conjecture,
( inverse(sk_c4) = sk_c10
| inverse(sk_c3) = sk_c8 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_53) ).
fof(f109,plain,
( sk_c10 = inverse(sk_c4)
| sk_c8 = inverse(sk_c3) ),
inference(reorient_equations,[],[f108]) ).
fof(f110,negated_conjecture,
( inverse(sk_c9) = sk_c8
| inverse(sk_c3) = sk_c8 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_54) ).
fof(f111,plain,
( sk_c8 = inverse(sk_c9)
| sk_c8 = inverse(sk_c3) ),
inference(reorient_equations,[],[f110]) ).
fof(f112,negated_conjecture,
( multiply(sk_c10,sk_c8) = sk_c9
| inverse(sk_c3) = sk_c8 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_55) ).
fof(f113,plain,
( sk_c9 = multiply(sk_c10,sk_c8)
| sk_c8 = inverse(sk_c3) ),
inference(reorient_equations,[],[f112]) ).
fof(f114,negated_conjecture,
( inverse(sk_c5) = sk_c9
| inverse(sk_c3) = sk_c8 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_56) ).
fof(f115,plain,
( sk_c9 = inverse(sk_c5)
| sk_c8 = inverse(sk_c3) ),
inference(reorient_equations,[],[f114]) ).
fof(f116,negated_conjecture,
( multiply(sk_c5,sk_c8) = sk_c9
| inverse(sk_c3) = sk_c8 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_57) ).
fof(f117,plain,
( sk_c9 = multiply(sk_c5,sk_c8)
| sk_c8 = inverse(sk_c3) ),
inference(reorient_equations,[],[f116]) ).
fof(f118,negated_conjecture,
( inverse(sk_c7) = sk_c6
| inverse(sk_c3) = sk_c8 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_58) ).
fof(f119,plain,
( inverse(sk_c7) = sk_c6
| sk_c8 = inverse(sk_c3) ),
inference(reorient_equations,[],[f118]) ).
fof(f120,negated_conjecture,
( inverse(sk_c6) = sk_c10
| inverse(sk_c3) = sk_c8 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_59) ).
fof(f121,plain,
( sk_c10 = inverse(sk_c6)
| sk_c8 = inverse(sk_c3) ),
inference(reorient_equations,[],[f120]) ).
fof(f122,negated_conjecture,
( multiply(sk_c7,sk_c10) = sk_c6
| inverse(sk_c3) = sk_c8 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_60) ).
fof(f123,plain,
( sk_c6 = multiply(sk_c7,sk_c10)
| sk_c8 = inverse(sk_c3) ),
inference(reorient_equations,[],[f122]) ).
fof(f124,negated_conjecture,
! [X2,X3,X0,X1,X6,X4,X5] :
( multiply(X5,sk_c10) != X6
| inverse(X6) != sk_c10
| inverse(X5) != X6
| multiply(X4,sk_c8) != sk_c9
| inverse(X4) != sk_c9
| multiply(sk_c10,sk_c8) != sk_c9
| inverse(sk_c9) != sk_c8
| inverse(X3) != sk_c10
| multiply(X3,sk_c10) != sk_c9
| multiply(sk_c9,sk_c10) != sk_c8
| inverse(X2) != sk_c8
| multiply(X2,sk_c8) != sk_c10
| inverse(X1) != sk_c10
| multiply(X1,sk_c10) != X0
| multiply(sk_c10,X0) != sk_c9
| multiply(sk_c8,sk_c10) != sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_61) ).
fof(f125,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( multiply(X5,sk_c10) != X6
| sk_c10 != inverse(X6)
| inverse(X5) != X6
| sk_c9 != multiply(X4,sk_c8)
| sk_c9 != inverse(X4)
| sk_c9 != multiply(sk_c10,sk_c8)
| sk_c8 != inverse(sk_c9)
| sk_c10 != inverse(X3)
| sk_c9 != multiply(X3,sk_c10)
| sk_c8 != multiply(sk_c9,sk_c10)
| sk_c8 != inverse(X2)
| sk_c10 != multiply(X2,sk_c8)
| sk_c10 != inverse(X1)
| multiply(X1,sk_c10) != X0
| sk_c9 != multiply(sk_c10,X0)
| multiply(sk_c8,sk_c10) != sk_c9 ),
inference(reorient_equations,[],[f124]) ).
fof(f126,plain,
! [X2,X3,X1,X6,X4,X5] :
( multiply(X5,sk_c10) != X6
| sk_c10 != inverse(X6)
| inverse(X5) != X6
| sk_c9 != multiply(X4,sk_c8)
| sk_c9 != inverse(X4)
| sk_c9 != multiply(sk_c10,sk_c8)
| sk_c8 != inverse(sk_c9)
| sk_c10 != inverse(X3)
| sk_c9 != multiply(X3,sk_c10)
| sk_c8 != multiply(sk_c9,sk_c10)
| sk_c8 != inverse(X2)
| sk_c10 != multiply(X2,sk_c8)
| sk_c10 != inverse(X1)
| sk_c9 != multiply(sk_c10,multiply(X1,sk_c10))
| multiply(sk_c8,sk_c10) != sk_c9 ),
inference(equality_resolution,[],[f125]) ).
fof(f127,plain,
! [X2,X3,X1,X4,X5] :
( inverse(X5) != multiply(X5,sk_c10)
| sk_c10 != inverse(inverse(X5))
| sk_c9 != multiply(X4,sk_c8)
| sk_c9 != inverse(X4)
| sk_c9 != multiply(sk_c10,sk_c8)
| sk_c8 != inverse(sk_c9)
| sk_c10 != inverse(X3)
| sk_c9 != multiply(X3,sk_c10)
| sk_c8 != multiply(sk_c9,sk_c10)
| sk_c8 != inverse(X2)
| sk_c10 != multiply(X2,sk_c8)
| sk_c10 != inverse(X1)
| sk_c9 != multiply(sk_c10,multiply(X1,sk_c10))
| multiply(sk_c8,sk_c10) != sk_c9 ),
inference(equality_resolution,[],[f126]) ).
tcf(c_113,plain,
! [X0: $i] : multiply(identity,X0) = X0,
inference(cnf_transformation,[],[f1]) ).
tcf(c_114,plain,
! [X0: $i] : multiply(inverse(X0),X0) = identity,
inference(cnf_transformation,[],[f3]) ).
tcf(c_115,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(multiply(X0,X1),X2) = multiply(X0,multiply(X1,X2)),
inference(cnf_transformation,[],[f4]) ).
tcf(c_116,negated_conjecture,
( ( multiply(sk_c9,sk_c10) = sk_c8 )
| ( multiply(sk_c8,sk_c10) = sk_c9 ) ),
inference(cnf_transformation,[],[f6]) ).
tcf(c_117,negated_conjecture,
( ( multiply(sk_c4,sk_c10) = sk_c9 )
| ( multiply(sk_c8,sk_c10) = sk_c9 ) ),
inference(cnf_transformation,[],[f8]) ).
tcf(c_118,negated_conjecture,
( ( inverse(sk_c4) = sk_c10 )
| ( multiply(sk_c8,sk_c10) = sk_c9 ) ),
inference(cnf_transformation,[],[f10]) ).
tcf(c_119,negated_conjecture,
( ( inverse(sk_c9) = sk_c8 )
| ( multiply(sk_c8,sk_c10) = sk_c9 ) ),
inference(cnf_transformation,[],[f12]) ).
tcf(c_120,negated_conjecture,
( ( multiply(sk_c10,sk_c8) = sk_c9 )
| ( multiply(sk_c8,sk_c10) = sk_c9 ) ),
inference(cnf_transformation,[],[f14]) ).
tcf(c_121,negated_conjecture,
( ( inverse(sk_c5) = sk_c9 )
| ( multiply(sk_c8,sk_c10) = sk_c9 ) ),
inference(cnf_transformation,[],[f16]) ).
tcf(c_122,negated_conjecture,
( ( multiply(sk_c5,sk_c8) = sk_c9 )
| ( multiply(sk_c8,sk_c10) = sk_c9 ) ),
inference(cnf_transformation,[],[f18]) ).
tcf(c_124,negated_conjecture,
( ( inverse(sk_c6) = sk_c10 )
| ( multiply(sk_c8,sk_c10) = sk_c9 ) ),
inference(cnf_transformation,[],[f21]) ).
tcf(c_126,negated_conjecture,
( ( multiply(sk_c9,sk_c10) = sk_c8 )
| ( multiply(sk_c10,sk_c2) = sk_c9 ) ),
inference(cnf_transformation,[],[f25]) ).
tcf(c_127,negated_conjecture,
( ( multiply(sk_c4,sk_c10) = sk_c9 )
| ( multiply(sk_c10,sk_c2) = sk_c9 ) ),
inference(cnf_transformation,[],[f27]) ).
tcf(c_128,negated_conjecture,
( ( inverse(sk_c4) = sk_c10 )
| ( multiply(sk_c10,sk_c2) = sk_c9 ) ),
inference(cnf_transformation,[],[f29]) ).
tcf(c_129,negated_conjecture,
( ( inverse(sk_c9) = sk_c8 )
| ( multiply(sk_c10,sk_c2) = sk_c9 ) ),
inference(cnf_transformation,[],[f31]) ).
tcf(c_130,negated_conjecture,
( ( multiply(sk_c10,sk_c2) = sk_c9 )
| ( multiply(sk_c10,sk_c8) = sk_c9 ) ),
inference(cnf_transformation,[],[f33]) ).
tcf(c_131,negated_conjecture,
( ( inverse(sk_c5) = sk_c9 )
| ( multiply(sk_c10,sk_c2) = sk_c9 ) ),
inference(cnf_transformation,[],[f35]) ).
tcf(c_132,negated_conjecture,
( ( multiply(sk_c5,sk_c8) = sk_c9 )
| ( multiply(sk_c10,sk_c2) = sk_c9 ) ),
inference(cnf_transformation,[],[f37]) ).
tcf(c_133,negated_conjecture,
( ( inverse(sk_c7) = sk_c6 )
| ( multiply(sk_c10,sk_c2) = sk_c9 ) ),
inference(cnf_transformation,[],[f39]) ).
tcf(c_134,negated_conjecture,
( ( inverse(sk_c6) = sk_c10 )
| ( multiply(sk_c10,sk_c2) = sk_c9 ) ),
inference(cnf_transformation,[],[f41]) ).
tcf(c_135,negated_conjecture,
( ( multiply(sk_c7,sk_c10) = sk_c6 )
| ( multiply(sk_c10,sk_c2) = sk_c9 ) ),
inference(cnf_transformation,[],[f43]) ).
tcf(c_136,negated_conjecture,
( ( multiply(sk_c1,sk_c10) = sk_c2 )
| ( multiply(sk_c9,sk_c10) = sk_c8 ) ),
inference(cnf_transformation,[],[f45]) ).
tcf(c_137,negated_conjecture,
( ( multiply(sk_c1,sk_c10) = sk_c2 )
| ( multiply(sk_c4,sk_c10) = sk_c9 ) ),
inference(cnf_transformation,[],[f47]) ).
tcf(c_138,negated_conjecture,
( ( inverse(sk_c4) = sk_c10 )
| ( multiply(sk_c1,sk_c10) = sk_c2 ) ),
inference(cnf_transformation,[],[f49]) ).
tcf(c_139,negated_conjecture,
( ( inverse(sk_c9) = sk_c8 )
| ( multiply(sk_c1,sk_c10) = sk_c2 ) ),
inference(cnf_transformation,[],[f51]) ).
tcf(c_140,negated_conjecture,
( ( multiply(sk_c1,sk_c10) = sk_c2 )
| ( multiply(sk_c10,sk_c8) = sk_c9 ) ),
inference(cnf_transformation,[],[f53]) ).
tcf(c_141,negated_conjecture,
( ( inverse(sk_c5) = sk_c9 )
| ( multiply(sk_c1,sk_c10) = sk_c2 ) ),
inference(cnf_transformation,[],[f55]) ).
tcf(c_142,negated_conjecture,
( ( multiply(sk_c1,sk_c10) = sk_c2 )
| ( multiply(sk_c5,sk_c8) = sk_c9 ) ),
inference(cnf_transformation,[],[f57]) ).
tcf(c_143,negated_conjecture,
( ( inverse(sk_c7) = sk_c6 )
| ( multiply(sk_c1,sk_c10) = sk_c2 ) ),
inference(cnf_transformation,[],[f59]) ).
tcf(c_144,negated_conjecture,
( ( inverse(sk_c6) = sk_c10 )
| ( multiply(sk_c1,sk_c10) = sk_c2 ) ),
inference(cnf_transformation,[],[f61]) ).
tcf(c_145,negated_conjecture,
( ( multiply(sk_c1,sk_c10) = sk_c2 )
| ( multiply(sk_c7,sk_c10) = sk_c6 ) ),
inference(cnf_transformation,[],[f63]) ).
tcf(c_146,negated_conjecture,
( ( inverse(sk_c1) = sk_c10 )
| ( multiply(sk_c9,sk_c10) = sk_c8 ) ),
inference(cnf_transformation,[],[f65]) ).
tcf(c_147,negated_conjecture,
( ( inverse(sk_c1) = sk_c10 )
| ( multiply(sk_c4,sk_c10) = sk_c9 ) ),
inference(cnf_transformation,[],[f67]) ).
tcf(c_148,negated_conjecture,
( ( inverse(sk_c1) = sk_c10 )
| ( inverse(sk_c4) = sk_c10 ) ),
inference(cnf_transformation,[],[f69]) ).
tcf(c_149,negated_conjecture,
( ( inverse(sk_c1) = sk_c10 )
| ( inverse(sk_c9) = sk_c8 ) ),
inference(cnf_transformation,[],[f71]) ).
tcf(c_150,negated_conjecture,
( ( inverse(sk_c1) = sk_c10 )
| ( multiply(sk_c10,sk_c8) = sk_c9 ) ),
inference(cnf_transformation,[],[f73]) ).
tcf(c_151,negated_conjecture,
( ( inverse(sk_c1) = sk_c10 )
| ( inverse(sk_c5) = sk_c9 ) ),
inference(cnf_transformation,[],[f75]) ).
tcf(c_152,negated_conjecture,
( ( inverse(sk_c1) = sk_c10 )
| ( multiply(sk_c5,sk_c8) = sk_c9 ) ),
inference(cnf_transformation,[],[f77]) ).
tcf(c_153,negated_conjecture,
( ( inverse(sk_c1) = sk_c10 )
| ( inverse(sk_c7) = sk_c6 ) ),
inference(cnf_transformation,[],[f79]) ).
tcf(c_154,negated_conjecture,
( ( inverse(sk_c1) = sk_c10 )
| ( inverse(sk_c6) = sk_c10 ) ),
inference(cnf_transformation,[],[f81]) ).
tcf(c_155,negated_conjecture,
( ( inverse(sk_c1) = sk_c10 )
| ( multiply(sk_c7,sk_c10) = sk_c6 ) ),
inference(cnf_transformation,[],[f83]) ).
tcf(c_156,negated_conjecture,
( ( multiply(sk_c3,sk_c8) = sk_c10 )
| ( multiply(sk_c9,sk_c10) = sk_c8 ) ),
inference(cnf_transformation,[],[f85]) ).
tcf(c_157,negated_conjecture,
( ( multiply(sk_c3,sk_c8) = sk_c10 )
| ( multiply(sk_c4,sk_c10) = sk_c9 ) ),
inference(cnf_transformation,[],[f87]) ).
tcf(c_158,negated_conjecture,
( ( inverse(sk_c4) = sk_c10 )
| ( multiply(sk_c3,sk_c8) = sk_c10 ) ),
inference(cnf_transformation,[],[f89]) ).
tcf(c_159,negated_conjecture,
( ( inverse(sk_c9) = sk_c8 )
| ( multiply(sk_c3,sk_c8) = sk_c10 ) ),
inference(cnf_transformation,[],[f91]) ).
tcf(c_160,negated_conjecture,
( ( multiply(sk_c3,sk_c8) = sk_c10 )
| ( multiply(sk_c10,sk_c8) = sk_c9 ) ),
inference(cnf_transformation,[],[f93]) ).
tcf(c_161,negated_conjecture,
( ( inverse(sk_c5) = sk_c9 )
| ( multiply(sk_c3,sk_c8) = sk_c10 ) ),
inference(cnf_transformation,[],[f95]) ).
tcf(c_162,negated_conjecture,
( ( multiply(sk_c3,sk_c8) = sk_c10 )
| ( multiply(sk_c5,sk_c8) = sk_c9 ) ),
inference(cnf_transformation,[],[f97]) ).
tcf(c_165,negated_conjecture,
( ( multiply(sk_c3,sk_c8) = sk_c10 )
| ( multiply(sk_c7,sk_c10) = sk_c6 ) ),
inference(cnf_transformation,[],[f103]) ).
tcf(c_166,negated_conjecture,
( ( inverse(sk_c3) = sk_c8 )
| ( multiply(sk_c9,sk_c10) = sk_c8 ) ),
inference(cnf_transformation,[],[f105]) ).
tcf(c_167,negated_conjecture,
( ( inverse(sk_c3) = sk_c8 )
| ( multiply(sk_c4,sk_c10) = sk_c9 ) ),
inference(cnf_transformation,[],[f107]) ).
tcf(c_168,negated_conjecture,
( ( inverse(sk_c3) = sk_c8 )
| ( inverse(sk_c4) = sk_c10 ) ),
inference(cnf_transformation,[],[f109]) ).
tcf(c_169,negated_conjecture,
( ( inverse(sk_c3) = sk_c8 )
| ( inverse(sk_c9) = sk_c8 ) ),
inference(cnf_transformation,[],[f111]) ).
tcf(c_170,negated_conjecture,
( ( inverse(sk_c3) = sk_c8 )
| ( multiply(sk_c10,sk_c8) = sk_c9 ) ),
inference(cnf_transformation,[],[f113]) ).
tcf(c_171,negated_conjecture,
( ( inverse(sk_c3) = sk_c8 )
| ( inverse(sk_c5) = sk_c9 ) ),
inference(cnf_transformation,[],[f115]) ).
tcf(c_172,negated_conjecture,
( ( inverse(sk_c3) = sk_c8 )
| ( multiply(sk_c5,sk_c8) = sk_c9 ) ),
inference(cnf_transformation,[],[f117]) ).
tcf(c_173,negated_conjecture,
( ( inverse(sk_c3) = sk_c8 )
| ( inverse(sk_c7) = sk_c6 ) ),
inference(cnf_transformation,[],[f119]) ).
tcf(c_174,negated_conjecture,
( ( inverse(sk_c3) = sk_c8 )
| ( inverse(sk_c6) = sk_c10 ) ),
inference(cnf_transformation,[],[f121]) ).
tcf(c_175,negated_conjecture,
( ( inverse(sk_c3) = sk_c8 )
| ( multiply(sk_c7,sk_c10) = sk_c6 ) ),
inference(cnf_transformation,[],[f123]) ).
tcf(c_176,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( ( inverse(sk_c9) != sk_c8 )
| ( inverse(X4) != sk_c9 )
| ( inverse(X3) != sk_c10 )
| ( inverse(X2) != sk_c10 )
| ( inverse(X1) != sk_c8 )
| ( multiply(sk_c9,sk_c10) != sk_c8 )
| ( multiply(sk_c10,sk_c8) != sk_c9 )
| ( multiply(sk_c8,sk_c10) != sk_c9 )
| ( inverse(inverse(X0)) != sk_c10 )
| ( multiply(X4,sk_c8) != sk_c9 )
| ( multiply(X3,sk_c10) != sk_c9 )
| ( multiply(X1,sk_c8) != sk_c10 )
| ( multiply(X0,sk_c10) != inverse(X0) )
| ( multiply(sk_c10,multiply(X2,sk_c10)) != sk_c9 ) ),
inference(cnf_transformation,[],[f127]) ).
tcf(c_725,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_10
| ( inverse(X0) != sk_c8 )
| ( multiply(X0,sk_c8) != sk_c10 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_10])],[c_176]) ).
tcf(c_726,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_11
| ( inverse(X0) != sk_c10 )
| ( multiply(X0,sk_c10) != sk_c9 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_11])],[c_176]) ).
tcf(c_727,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_12
| ( inverse(inverse(X0)) != sk_c10 )
| ( multiply(X0,sk_c10) != inverse(X0) ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_12])],[c_176]) ).
tcf(c_728,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_13
| ( inverse(X0) != sk_c9 )
| ( multiply(X0,sk_c8) != sk_c9 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_13])],[c_176]) ).
tcf(c_729,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_14
| ( inverse(X0) != sk_c10 )
| ( multiply(sk_c10,multiply(X0,sk_c10)) != sk_c9 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_14])],[c_176]) ).
tcf(c_730,negated_conjecture,
( iPr_def_14
| iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( inverse(sk_c9) != sk_c8 )
| ( multiply(sk_c9,sk_c10) != sk_c8 )
| ( multiply(sk_c10,sk_c8) != sk_c9 )
| ( multiply(sk_c8,sk_c10) != sk_c9 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_176]) ).
tcf(c_731,plain,
! [X0: $i] : X0 = X0,
theory(equality) ).
tcf(c_732,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = X0 )
| ( X2 != X1 )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_733,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( multiply(X0,X2) = multiply(X1,X3) )
| ( X2 != X3 )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_734,plain,
! [X0: $i,X1: $i] :
( ( inverse(X0) = inverse(X1) )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_736,plain,
( ( inverse(sk_c10) = inverse(sk_c10) )
| ( sk_c10 != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_734]) ).
tcf(c_737,plain,
sk_c10 = sk_c10,
inference(instantiation,[status(thm)],[c_731]) ).
tcf(c_738,plain,
( ~ iPr_def_10
| ( inverse(sk_c10) != sk_c8 )
| ( multiply(sk_c10,sk_c8) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_725]) ).
tcf(c_741,plain,
( ~ iPr_def_13
| ( inverse(sk_c10) != sk_c9 )
| ( multiply(sk_c10,sk_c8) != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_728]) ).
tcf(c_1055,plain,
! [X0: $i] :
( ( multiply(sk_c8,sk_c10) = sk_c9 )
| ( sk_c9 != X0 )
| ( multiply(sk_c8,sk_c10) != X0 ) ),
inference(instantiation,[status(thm)],[c_732]) ).
tcf(c_1058,plain,
! [X0: $i,X1: $i] :
( ( sk_c9 = X0 )
| ( sk_c9 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_732]) ).
tcf(c_1059,plain,
! [X0: $i] :
( ( sk_c9 = X0 )
| ( sk_c9 != sk_c9 )
| ( X0 != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_1058]) ).
tcf(c_1060,plain,
sk_c9 = sk_c9,
inference(instantiation,[status(thm)],[c_731]) ).
tcf(c_1061,plain,
( ( sk_c9 = sk_c10 )
| ( sk_c9 != sk_c9 )
| ( sk_c10 != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_1059]) ).
tcf(c_1066,plain,
( ( sk_c9 = multiply(sk_c10,sk_c8) )
| ( sk_c9 != sk_c9 )
| ( multiply(sk_c10,sk_c8) != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_1059]) ).
tcf(c_1067,plain,
( ( sk_c9 = inverse(sk_c5) )
| ( sk_c9 != sk_c9 )
| ( inverse(sk_c5) != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_1059]) ).
tcf(c_1068,plain,
( ( sk_c9 = multiply(sk_c5,sk_c8) )
| ( sk_c9 != sk_c9 )
| ( multiply(sk_c5,sk_c8) != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_1059]) ).
tcf(c_1069,plain,
( ( sk_c9 = multiply(identity,sk_c9) )
| ( sk_c9 != sk_c9 )
| ( multiply(identity,sk_c9) != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_1059]) ).
tcf(c_1070,plain,
multiply(identity,sk_c9) = sk_c9,
inference(instantiation,[status(thm)],[c_113]) ).
tcf(c_1072,plain,
! [X0: $i,X1: $i] :
( ( X0 = sk_c9 )
| ( sk_c9 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_732]) ).
tcf(c_1078,plain,
( ( multiply(sk_c8,sk_c10) = sk_c9 )
| ( sk_c9 != multiply(sk_c10,sk_c8) )
| ( multiply(sk_c8,sk_c10) != multiply(sk_c10,sk_c8) ) ),
inference(instantiation,[status(thm)],[c_1055]) ).
tcf(c_1079,plain,
! [X0: $i] :
( ( sk_c9 = X0 )
| ( sk_c9 != multiply(sk_c10,sk_c8) )
| ( X0 != multiply(sk_c10,sk_c8) ) ),
inference(instantiation,[status(thm)],[c_1058]) ).
tcf(c_1084,plain,
! [X0: $i] :
( ( X0 = sk_c9 )
| ( sk_c9 != multiply(sk_c10,sk_c8) )
| ( X0 != multiply(sk_c10,sk_c8) ) ),
inference(instantiation,[status(thm)],[c_1072]) ).
tcf(c_1090,plain,
! [X0: $i] :
( ( X0 = sk_c9 )
| ( sk_c9 != inverse(sk_c5) )
| ( X0 != inverse(sk_c5) ) ),
inference(instantiation,[status(thm)],[c_1072]) ).
tcf(c_1093,plain,
( ( sk_c10 = sk_c9 )
| ( sk_c9 != inverse(sk_c5) )
| ( sk_c10 != inverse(sk_c5) ) ),
inference(instantiation,[status(thm)],[c_1090]) ).
tcf(c_1095,plain,
! [X0: $i] :
( ( X0 = sk_c9 )
| ( sk_c9 != multiply(sk_c5,sk_c8) )
| ( X0 != multiply(sk_c5,sk_c8) ) ),
inference(instantiation,[status(thm)],[c_1072]) ).
tcf(c_1106,plain,
( ( sk_c9 = multiply(sk_c8,sk_c10) )
| ( sk_c9 != sk_c9 )
| ( multiply(sk_c8,sk_c10) != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_1059]) ).
tcf(c_1107,plain,
( ( sk_c9 = multiply(sk_c10,sk_c2) )
| ( sk_c9 != sk_c9 )
| ( multiply(sk_c10,sk_c2) != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_1059]) ).
tcf(c_1133,plain,
! [X0: $i,X1: $i] :
( ( X1 = multiply(identity,sk_c9) )
| ( X1 != X0 )
| ( multiply(identity,sk_c9) != X0 ) ),
inference(instantiation,[status(thm)],[c_732]) ).
tcf(c_1149,plain,
! [X0: $i] :
( ( sk_c9 = X0 )
| ( sk_c9 != multiply(sk_c8,sk_c10) )
| ( X0 != multiply(sk_c8,sk_c10) ) ),
inference(instantiation,[status(thm)],[c_1058]) ).
tcf(c_1153,plain,
! [X0: $i] :
( ( X0 = sk_c9 )
| ( sk_c9 != multiply(sk_c10,sk_c2) )
| ( X0 != multiply(sk_c10,sk_c2) ) ),
inference(instantiation,[status(thm)],[c_1072]) ).
tcf(c_1154,plain,
! [X0: $i] :
( ( sk_c9 = X0 )
| ( sk_c9 != multiply(sk_c10,sk_c2) )
| ( X0 != multiply(sk_c10,sk_c2) ) ),
inference(instantiation,[status(thm)],[c_1058]) ).
tcf(c_1155,plain,
( ( sk_c9 = sk_c10 )
| ( sk_c9 != multiply(sk_c10,sk_c2) )
| ( sk_c10 != multiply(sk_c10,sk_c2) ) ),
inference(instantiation,[status(thm)],[c_1154]) ).
tcf(c_1156,plain,
( ( sk_c10 = sk_c9 )
| ( sk_c9 != multiply(sk_c10,sk_c2) )
| ( sk_c10 != multiply(sk_c10,sk_c2) ) ),
inference(instantiation,[status(thm)],[c_1153]) ).
tcf(c_1189,plain,
! [X0: $i,X1: $i] :
( ( multiply(identity,sk_c9) = X1 )
| ( X1 != X0 )
| ( multiply(identity,sk_c9) != X0 ) ),
inference(instantiation,[status(thm)],[c_732]) ).
tcf(c_1208,plain,
( ( inverse(sk_c3) = sk_c8 )
| ( multiply(sk_c6,sk_c7) = identity ) ),
inference(superposition,[status(thm)],[c_173,c_114]) ).
tcf(c_1211,plain,
( ( inverse(sk_c3) = sk_c8 )
| ( multiply(sk_c10,sk_c6) = identity ) ),
inference(superposition,[status(thm)],[c_174,c_114]) ).
tcf(c_1302,plain,
! [X0: $i] :
( ( inverse(sk_c9) = sk_c8 )
| ( multiply(sk_c8,multiply(sk_c10,X0)) = multiply(sk_c9,X0) ) ),
inference(superposition,[status(thm)],[c_119,c_115]) ).
tcf(c_1330,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(X0,X1)) = multiply(identity,X1),
inference(superposition,[status(thm)],[c_114,c_115]) ).
tcf(c_1366,plain,
( ( multiply(sk_c8,sk_c10) = multiply(sk_c10,sk_c8) )
| ( sk_c10 != sk_c8 )
| ( sk_c8 != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_733]) ).
tcf(c_1399,plain,
! [X0: $i,X1: $i] :
( ( sk_c9 = multiply(X0,X1) )
| ( sk_c9 != multiply(sk_c10,sk_c8) )
| ( multiply(X0,X1) != multiply(sk_c10,sk_c8) ) ),
inference(instantiation,[status(thm)],[c_1079]) ).
tcf(c_1400,plain,
! [X0: $i,X1: $i] :
( ( multiply(X0,X1) = multiply(sk_c10,sk_c8) )
| ( X1 != sk_c8 )
| ( X0 != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_733]) ).
tcf(c_1401,plain,
( ( sk_c9 = multiply(sk_c10,sk_c10) )
| ( sk_c9 != multiply(sk_c10,sk_c8) )
| ( multiply(sk_c10,sk_c10) != multiply(sk_c10,sk_c8) ) ),
inference(instantiation,[status(thm)],[c_1399]) ).
tcf(c_1402,plain,
( ( multiply(sk_c10,sk_c10) = multiply(sk_c10,sk_c8) )
| ( sk_c10 != sk_c10 )
| ( sk_c10 != sk_c8 ) ),
inference(instantiation,[status(thm)],[c_1400]) ).
tcf(c_1408,plain,
! [X0: $i,X1: $i] :
( ( X1 = inverse(sk_c5) )
| ( X1 != X0 )
| ( inverse(sk_c5) != X0 ) ),
inference(instantiation,[status(thm)],[c_732]) ).
tcf(c_1409,plain,
( ( sk_c10 = inverse(sk_c5) )
| ( sk_c10 != sk_c10 )
| ( inverse(sk_c5) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_1408]) ).
tcf(c_1410,plain,
! [X0: $i] :
( ( inverse(X0) = sk_c9 )
| ( sk_c9 != inverse(sk_c5) )
| ( inverse(X0) != inverse(sk_c5) ) ),
inference(instantiation,[status(thm)],[c_1090]) ).
tcf(c_1412,plain,
( ( inverse(sk_c10) = sk_c9 )
| ( sk_c9 != inverse(sk_c5) )
| ( inverse(sk_c10) != inverse(sk_c5) ) ),
inference(instantiation,[status(thm)],[c_1410]) ).
tcf(c_1442,plain,
! [X0: $i,X1: $i] :
( ( multiply(X0,X1) = sk_c9 )
| ( sk_c9 != multiply(sk_c5,sk_c8) )
| ( multiply(X0,X1) != multiply(sk_c5,sk_c8) ) ),
inference(instantiation,[status(thm)],[c_1095]) ).
tcf(c_1443,plain,
! [X0: $i,X1: $i] :
( ( multiply(X0,X1) = multiply(sk_c5,sk_c8) )
| ( X1 != sk_c8 )
| ( X0 != sk_c5 ) ),
inference(instantiation,[status(thm)],[c_733]) ).
tcf(c_1456,plain,
! [X0: $i,X1: $i] :
( ( X1 = multiply(sk_c8,sk_c10) )
| ( X1 != X0 )
| ( multiply(sk_c8,sk_c10) != X0 ) ),
inference(instantiation,[status(thm)],[c_732]) ).
tcf(c_1475,plain,
! [X0: $i,X1: $i] :
( ( X1 = multiply(sk_c10,sk_c2) )
| ( X1 != X0 )
| ( multiply(sk_c10,sk_c2) != X0 ) ),
inference(instantiation,[status(thm)],[c_732]) ).
tcf(c_1476,plain,
( ( sk_c10 = multiply(sk_c10,sk_c2) )
| ( sk_c10 != sk_c10 )
| ( multiply(sk_c10,sk_c2) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_1475]) ).
tcf(c_1639,plain,
! [X0: $i] :
( ( multiply(identity,sk_c9) = X0 )
| ( X0 != sk_c9 )
| ( multiply(identity,sk_c9) != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_1189]) ).
tcf(c_1647,plain,
! [X0: $i] :
( ( multiply(sk_c1,sk_c10) = sk_c2 )
| ( multiply(sk_c7,multiply(sk_c10,X0)) = multiply(sk_c6,X0) ) ),
inference(superposition,[status(thm)],[c_145,c_115]) ).
tcf(c_1692,plain,
! [X0: $i] :
( ( multiply(sk_c3,sk_c8) = sk_c10 )
| ( multiply(sk_c7,multiply(sk_c10,X0)) = multiply(sk_c6,X0) ) ),
inference(superposition,[status(thm)],[c_165,c_115]) ).
tcf(c_1712,plain,
( ( multiply(sk_c10,sk_c8) = sk_c9 )
| ~ iPr_def_10
| ( inverse(sk_c3) != sk_c8 ) ),
inference(superposition,[status(thm)],[c_160,c_725]) ).
tcf(c_1713,plain,
( ( multiply(sk_c9,sk_c10) = sk_c8 )
| ~ iPr_def_10
| ( inverse(sk_c3) != sk_c8 ) ),
inference(superposition,[status(thm)],[c_156,c_725]) ).
tcf(c_1716,plain,
( ( inverse(sk_c5) = sk_c9 )
| ~ iPr_def_10
| ( inverse(sk_c3) != sk_c8 ) ),
inference(superposition,[status(thm)],[c_161,c_725]) ).
tcf(c_1717,plain,
( ( inverse(sk_c9) = sk_c8 )
| ~ iPr_def_10
| ( inverse(sk_c3) != sk_c8 ) ),
inference(superposition,[status(thm)],[c_159,c_725]) ).
tcf(c_1718,plain,
( ( inverse(sk_c4) = sk_c10 )
| ~ iPr_def_10
| ( inverse(sk_c3) != sk_c8 ) ),
inference(superposition,[status(thm)],[c_158,c_725]) ).
tcf(c_1720,plain,
( ~ iPr_def_10
| ( sk_c10 != identity )
| ( inverse(inverse(sk_c8)) != sk_c8 ) ),
inference(superposition,[status(thm)],[c_114,c_725]) ).
tcf(c_2050,plain,
( ( inverse(sk_c9) = sk_c8 )
| ~ iPr_def_10
| ( inverse(sk_c3) != sk_c8 ) ),
inference(resolution,[status(thm)],[c_725,c_159]) ).
tcf(c_2056,plain,
( ( multiply(sk_c10,sk_c8) = sk_c9 )
| ~ iPr_def_10
| ( inverse(sk_c3) != sk_c8 ) ),
inference(resolution,[status(thm)],[c_725,c_160]) ).
tcf(c_2074,plain,
( ( multiply(sk_c10,sk_c8) = sk_c9 )
| ( sk_c9 != multiply(sk_c10,sk_c8) )
| ( multiply(sk_c10,sk_c8) != multiply(sk_c10,sk_c8) ) ),
inference(instantiation,[status(thm)],[c_1084]) ).
tcf(c_2075,plain,
multiply(sk_c10,sk_c8) = multiply(sk_c10,sk_c8),
inference(instantiation,[status(thm)],[c_731]) ).
tcf(c_2081,plain,
! [X0: $i] :
( ( sk_c10 = sk_c8 )
| ( sk_c10 != X0 )
| ( sk_c8 != X0 ) ),
inference(instantiation,[status(thm)],[c_732]) ).
tcf(c_2122,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(X0,X1)) = X1,
inference(demodulation,[status(thm)],[c_1330,c_113]) ).
tcf(c_2134,plain,
! [X0: $i] : multiply(inverse(inverse(X0)),identity) = X0,
inference(superposition,[status(thm)],[c_114,c_2122]) ).
tcf(c_2140,plain,
multiply(inverse(inverse(sk_c10)),identity) = sk_c10,
inference(instantiation,[status(thm)],[c_2134]) ).
tcf(c_2193,plain,
( ( inverse(sk_c1) = sk_c10 )
| ~ iPr_def_11
| ( inverse(sk_c4) != sk_c10 ) ),
inference(resolution,[status(thm)],[c_726,c_147]) ).
tcf(c_2194,plain,
( ( inverse(sk_c3) = sk_c8 )
| ~ iPr_def_11
| ( inverse(sk_c4) != sk_c10 ) ),
inference(resolution,[status(thm)],[c_726,c_167]) ).
tcf(c_2195,plain,
( ( multiply(sk_c8,sk_c10) = sk_c9 )
| ~ iPr_def_11
| ( inverse(sk_c4) != sk_c10 ) ),
inference(resolution,[status(thm)],[c_726,c_117]) ).
tcf(c_2196,plain,
( ( multiply(sk_c10,sk_c2) = sk_c9 )
| ~ iPr_def_11
| ( inverse(sk_c4) != sk_c10 ) ),
inference(resolution,[status(thm)],[c_726,c_127]) ).
tcf(c_2219,plain,
! [X0: $i,X1: $i] :
( ( multiply(sk_c8,sk_c10) = multiply(X0,X1) )
| ( sk_c10 != X1 )
| ( sk_c8 != X0 ) ),
inference(instantiation,[status(thm)],[c_733]) ).
tcf(c_2221,plain,
( ( multiply(sk_c8,sk_c10) = multiply(sk_c10,sk_c10) )
| ( sk_c10 != sk_c10 )
| ( sk_c8 != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_2219]) ).
tcf(c_2308,plain,
! [X0: $i,X1: $i] :
( ( multiply(sk_c10,sk_c8) = X1 )
| ( X1 != X0 )
| ( multiply(sk_c10,sk_c8) != X0 ) ),
inference(instantiation,[status(thm)],[c_732]) ).
tcf(c_2330,plain,
( ( inverse(sk_c3) = sk_c8 )
| ~ iPr_def_13
| ( inverse(sk_c10) != sk_c9 ) ),
inference(resolution,[status(thm)],[c_728,c_170]) ).
tcf(c_2332,plain,
( ( inverse(sk_c1) = sk_c10 )
| ~ iPr_def_13
| ( inverse(sk_c5) != sk_c9 ) ),
inference(resolution,[status(thm)],[c_728,c_152]) ).
tcf(c_2333,plain,
( ( inverse(sk_c3) = sk_c8 )
| ~ iPr_def_13
| ( inverse(sk_c5) != sk_c9 ) ),
inference(resolution,[status(thm)],[c_728,c_172]) ).
tcf(c_2335,plain,
( ( multiply(sk_c10,sk_c2) = sk_c9 )
| ~ iPr_def_13
| ( inverse(sk_c5) != sk_c9 ) ),
inference(resolution,[status(thm)],[c_728,c_132]) ).
tcf(c_2351,plain,
sk_c8 = sk_c8,
inference(instantiation,[status(thm)],[c_731]) ).
tcf(c_2352,plain,
! [X0: $i,X1: $i] :
( ( X0 = sk_c8 )
| ( sk_c8 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_732]) ).
tcf(c_2357,plain,
( ( inverse(sk_c9) = sk_c8 )
| ~ iPr_def_10 ),
inference(global_subsumption_just,[status(thm)],[c_1717,c_169,c_1717]) ).
tcf(c_2368,plain,
! [X0: $i] :
( ( X0 = inverse(sk_c5) )
| ( X0 != sk_c9 )
| ( inverse(sk_c5) != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_1408]) ).
tcf(c_2369,plain,
( ( sk_c10 = inverse(sk_c5) )
| ( sk_c10 != sk_c9 )
| ( inverse(sk_c5) != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_2368]) ).
tcf(c_2413,plain,
! [X0: $i] :
( ( multiply(sk_c5,X0) = multiply(sk_c5,sk_c8) )
| ( sk_c5 != sk_c5 )
| ( X0 != sk_c8 ) ),
inference(instantiation,[status(thm)],[c_1443]) ).
tcf(c_2414,plain,
sk_c5 = sk_c5,
inference(instantiation,[status(thm)],[c_731]) ).
tcf(c_2415,plain,
( ( multiply(sk_c5,sk_c10) = multiply(sk_c5,sk_c8) )
| ( sk_c5 != sk_c5 )
| ( sk_c10 != sk_c8 ) ),
inference(instantiation,[status(thm)],[c_2413]) ).
tcf(c_2453,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = multiply(sk_c10,sk_c2) )
| ( X2 != multiply(X0,X1) )
| ( multiply(sk_c10,sk_c2) != multiply(X0,X1) ) ),
inference(instantiation,[status(thm)],[c_1475]) ).
tcf(c_2454,plain,
! [X0: $i,X1: $i] :
( ( multiply(sk_c10,sk_c2) = multiply(X0,X1) )
| ( sk_c2 != X1 )
| ( sk_c10 != X0 ) ),
inference(instantiation,[status(thm)],[c_733]) ).
tcf(c_2455,plain,
( ( sk_c10 = multiply(sk_c10,sk_c2) )
| ( sk_c10 != multiply(sk_c10,sk_c10) )
| ( multiply(sk_c10,sk_c2) != multiply(sk_c10,sk_c10) ) ),
inference(instantiation,[status(thm)],[c_2453]) ).
tcf(c_2456,plain,
( ( multiply(sk_c10,sk_c2) = multiply(sk_c10,sk_c10) )
| ( sk_c2 != sk_c10 )
| ( sk_c10 != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_2454]) ).
tcf(c_2488,plain,
( iPr_def_14
| iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( multiply(sk_c10,sk_c2) = sk_c9 )
| ( inverse(sk_c9) != sk_c8 )
| ( multiply(sk_c10,sk_c8) != sk_c9 )
| ( multiply(sk_c8,sk_c10) != sk_c9 ) ),
inference(resolution,[status(thm)],[c_730,c_126]) ).
tcf(c_2501,plain,
( ( multiply(sk_c10,sk_c8) = sk_c9 )
| ~ iPr_def_10 ),
inference(global_subsumption_just,[status(thm)],[c_1712,c_170,c_1712]) ).
tcf(c_2540,plain,
( ( inverse(sk_c9) = sk_c8 )
| ~ iPr_def_10 ),
inference(global_subsumption_just,[status(thm)],[c_2050,c_2357]) ).
tcf(c_2566,plain,
! [X0: $i] :
( ( inverse(sk_c1) = sk_c10 )
| ( multiply(sk_c9,sk_c10) = X0 )
| ( X0 != sk_c8 ) ),
inference(resolution,[status(thm)],[c_732,c_146]) ).
tcf(c_2567,plain,
! [X0: $i] :
( ( inverse(sk_c3) = sk_c8 )
| ( multiply(sk_c9,sk_c10) = X0 )
| ( X0 != sk_c8 ) ),
inference(resolution,[status(thm)],[c_732,c_166]) ).
tcf(c_2577,plain,
! [X0: $i] :
( ( multiply(sk_c4,sk_c10) = X0 )
| ( multiply(sk_c10,sk_c2) = sk_c9 )
| ( X0 != sk_c9 ) ),
inference(resolution,[status(thm)],[c_732,c_127]) ).
tcf(c_2585,plain,
! [X0: $i] :
( ( inverse(sk_c1) = sk_c10 )
| ( multiply(sk_c10,sk_c8) = X0 )
| ( X0 != sk_c9 ) ),
inference(resolution,[status(thm)],[c_732,c_150]) ).
tcf(c_2599,plain,
! [X0: $i] :
( ( inverse(sk_c1) = sk_c10 )
| ( multiply(sk_c7,sk_c10) = X0 )
| ( X0 != sk_c6 ) ),
inference(resolution,[status(thm)],[c_732,c_155]) ).
tcf(c_2608,plain,
! [X0: $i] :
( ( inverse(sk_c9) = sk_c8 )
| ( multiply(sk_c10,sk_c2) = X0 )
| ( X0 != sk_c9 ) ),
inference(resolution,[status(thm)],[c_732,c_129]) ).
tcf(c_2619,plain,
! [X0: $i] :
( ( inverse(sk_c4) = sk_c10 )
| ( multiply(sk_c1,sk_c10) = X0 )
| ( X0 != sk_c2 ) ),
inference(resolution,[status(thm)],[c_732,c_138]) ).
tcf(c_2621,plain,
! [X0: $i] :
( ( inverse(sk_c5) = sk_c9 )
| ( multiply(sk_c1,sk_c10) = X0 )
| ( X0 != sk_c2 ) ),
inference(resolution,[status(thm)],[c_732,c_141]) ).
tcf(c_2625,plain,
! [X0: $i] :
( ( multiply(sk_c1,sk_c10) = X0 )
| ( multiply(sk_c4,sk_c10) = sk_c9 )
| ( X0 != sk_c2 ) ),
inference(resolution,[status(thm)],[c_732,c_137]) ).
tcf(c_2644,plain,
! [X0: $i] :
( ( inverse(sk_c4) = sk_c10 )
| ( multiply(sk_c3,sk_c8) = X0 )
| ( X0 != sk_c10 ) ),
inference(resolution,[status(thm)],[c_732,c_158]) ).
tcf(c_2646,plain,
! [X0: $i] :
( ( inverse(sk_c5) = sk_c9 )
| ( multiply(sk_c3,sk_c8) = X0 )
| ( X0 != sk_c10 ) ),
inference(resolution,[status(thm)],[c_732,c_161]) ).
tcf(c_2654,plain,
! [X0: $i] :
( ( inverse(sk_c3) = X0 )
| ( inverse(sk_c4) = sk_c10 )
| ( X0 != sk_c8 ) ),
inference(resolution,[status(thm)],[c_732,c_168]) ).
tcf(c_2656,plain,
! [X0: $i] :
( ( inverse(sk_c3) = X0 )
| ( inverse(sk_c5) = sk_c9 )
| ( X0 != sk_c8 ) ),
inference(resolution,[status(thm)],[c_732,c_171]) ).
tcf(c_2669,plain,
! [X0: $i,X1: $i] :
( ( X1 = X0 )
| ( X0 != X1 ) ),
inference(resolution,[status(thm)],[c_732,c_731]) ).
tcf(c_2670,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( inverse(X0) = X2 )
| ( X2 != inverse(X1) )
| ( X0 != X1 ) ),
inference(resolution,[status(thm)],[c_732,c_734]) ).
tcf(c_2813,plain,
( ( multiply(sk_c8,sk_c10) = sk_c9 )
| ( multiply(inverse(sk_c5),sk_c9) = sk_c8 ) ),
inference(superposition,[status(thm)],[c_122,c_2122]) ).
tcf(c_2930,plain,
( ( inverse(sk_c9) = sk_c8 )
| ( multiply(sk_c8,sk_c9) = multiply(sk_c9,sk_c2) ) ),
inference(superposition,[status(thm)],[c_129,c_1302]) ).
tcf(c_2980,plain,
( ( multiply(sk_c10,sk_c2) = sk_c9 )
| ( multiply(inverse(sk_c5),sk_c9) = sk_c8 ) ),
inference(superposition,[status(thm)],[c_132,c_2122]) ).
tcf(c_3212,plain,
( ( inverse(sk_c5) = sk_c9 )
| ~ iPr_def_11
| ( sk_c9 != sk_c2 )
| ( inverse(sk_c1) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_141,c_726]) ).
tcf(c_3214,plain,
( ( inverse(sk_c4) = sk_c10 )
| ~ iPr_def_11
| ( sk_c9 != sk_c2 )
| ( inverse(sk_c1) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_138,c_726]) ).
tcf(c_3660,plain,
! [X0: $i] :
( ( inverse(sk_c3) = sk_c8 )
| ( multiply(sk_c10,multiply(sk_c6,X0)) = multiply(identity,X0) ) ),
inference(superposition,[status(thm)],[c_1211,c_115]) ).
tcf(c_3661,plain,
! [X0: $i] :
( ( inverse(sk_c3) = sk_c8 )
| ( multiply(sk_c10,multiply(sk_c6,X0)) = X0 ) ),
inference(light_normalisation,[status(thm)],[c_3660,c_113]) ).
tcf(c_3792,plain,
( ( multiply(sk_c10,sk_c2) = sk_c9 )
| ~ iPr_def_12
| ( inverse(sk_c7) != sk_c6 )
| ( inverse(inverse(sk_c7)) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_135,c_727]) ).
tcf(c_3795,plain,
( ( inverse(sk_c1) = sk_c10 )
| ~ iPr_def_12
| ( inverse(sk_c7) != sk_c6 )
| ( inverse(inverse(sk_c7)) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_155,c_727]) ).
tcf(c_3810,plain,
( ( inverse(sk_c3) = sk_c8 )
| ~ iPr_def_14
| ( sk_c10 != sk_c9 )
| ( inverse(sk_c6) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_3661,c_729]) ).
tcf(c_3837,plain,
( ( inverse(sk_c5) = sk_c9 )
| ~ iPr_def_14
| ( inverse(sk_c1) != sk_c10 )
| ( multiply(sk_c10,sk_c2) != sk_c9 ) ),
inference(superposition,[status(thm)],[c_141,c_729]) ).
tcf(c_3875,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(X0,X1)) = X1,
inference(demodulation,[status(thm)],[c_1330,c_113]) ).
tcf(c_3937,plain,
! [X0: $i] : multiply(inverse(inverse(X0)),identity) = X0,
inference(superposition,[status(thm)],[c_114,c_3875]) ).
tcf(c_3956,plain,
! [X0: $i,X1: $i] : multiply(inverse(inverse(X0)),X1) = multiply(X0,X1),
inference(superposition,[status(thm)],[c_3875,c_3875]) ).
tcf(c_4009,plain,
( ( multiply(identity,sk_c9) = multiply(sk_c10,sk_c2) )
| ( multiply(identity,sk_c9) != sk_c9 )
| ( multiply(sk_c10,sk_c2) != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_1639]) ).
tcf(c_4269,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( ( multiply(X0,X2) = X4 )
| ( X4 != multiply(X1,X3) )
| ( X2 != X3 )
| ( X0 != X1 ) ),
inference(resolution,[status(thm)],[c_733,c_732]) ).
tcf(c_4301,plain,
( ( sk_c8 = multiply(sk_c9,sk_c10) )
| ( inverse(sk_c1) = sk_c10 ) ),
inference(resolution,[status(thm)],[c_2669,c_146]) ).
tcf(c_4302,plain,
( ( sk_c8 = multiply(sk_c9,sk_c10) )
| ( inverse(sk_c3) = sk_c8 ) ),
inference(resolution,[status(thm)],[c_2669,c_166]) ).
tcf(c_4310,plain,
( ( sk_c8 = inverse(sk_c9) )
| ~ iPr_def_10 ),
inference(resolution,[status(thm)],[c_2669,c_2540]) ).
tcf(c_4311,plain,
( ( sk_c9 = multiply(sk_c10,sk_c8) )
| ( inverse(sk_c1) = sk_c10 ) ),
inference(resolution,[status(thm)],[c_2669,c_150]) ).
tcf(c_4312,plain,
( ( sk_c9 = multiply(sk_c10,sk_c8) )
| ( inverse(sk_c3) = sk_c8 ) ),
inference(resolution,[status(thm)],[c_2669,c_170]) ).
tcf(c_4323,plain,
( ( sk_c9 = multiply(sk_c10,sk_c2) )
| ( inverse(sk_c9) = sk_c8 ) ),
inference(resolution,[status(thm)],[c_2669,c_129]) ).
tcf(c_4327,plain,
( ( sk_c9 = multiply(sk_c10,sk_c2) )
| ( multiply(sk_c10,sk_c8) = sk_c9 ) ),
inference(resolution,[status(thm)],[c_2669,c_130]) ).
tcf(c_4339,plain,
( ( sk_c10 = inverse(sk_c1) )
| ( inverse(sk_c9) = sk_c8 ) ),
inference(resolution,[status(thm)],[c_2669,c_149]) ).
tcf(c_4358,plain,
! [X0: $i] : X0 = multiply(identity,X0),
inference(resolution,[status(thm)],[c_2669,c_113]) ).
tcf(c_4497,plain,
! [X0: $i,X1: $i] :
( ( sk_c8 = X0 )
| ( sk_c8 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_732]) ).
tcf(c_4648,plain,
! [X0: $i] : multiply(X0,identity) = X0,
inference(demodulation,[status(thm)],[c_3937,c_3956]) ).
tcf(c_4665,plain,
! [X0: $i] : multiply(X0,inverse(X0)) = identity,
inference(superposition,[status(thm)],[c_3956,c_114]) ).
tcf(c_4707,plain,
! [X0: $i,X1: $i] :
( ( sk_c2 = X0 )
| ( sk_c2 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_732]) ).
tcf(c_4951,plain,
( ( inverse(sk_c3) = sk_c8 )
| ( multiply(sk_c4,sk_c10) = identity ) ),
inference(superposition,[status(thm)],[c_168,c_4665]) ).
tcf(c_4952,plain,
( ( inverse(sk_c1) = sk_c10 )
| ( multiply(sk_c4,sk_c10) = identity ) ),
inference(superposition,[status(thm)],[c_148,c_4665]) ).
tcf(c_5030,plain,
( ( sk_c9 = identity )
| ( inverse(sk_c3) = sk_c8 ) ),
inference(superposition,[status(thm)],[c_4951,c_167]) ).
tcf(c_5154,plain,
( ( sk_c9 = identity )
| ( inverse(sk_c1) = sk_c10 ) ),
inference(superposition,[status(thm)],[c_4952,c_147]) ).
tcf(c_5399,plain,
( ( sk_c10 = inverse(sk_c1) )
| ( sk_c8 = inverse(sk_c9) ) ),
inference(resolution,[status(thm)],[c_4339,c_2669]) ).
tcf(c_5660,plain,
! [X0: $i] :
( ( multiply(identity,sk_c9) = X0 )
| ( X0 != multiply(sk_c10,sk_c2) )
| ( multiply(identity,sk_c9) != multiply(sk_c10,sk_c2) ) ),
inference(instantiation,[status(thm)],[c_1189]) ).
tcf(c_5662,plain,
( ( multiply(identity,sk_c9) = sk_c10 )
| ( sk_c10 != multiply(sk_c10,sk_c2) )
| ( multiply(identity,sk_c9) != multiply(sk_c10,sk_c2) ) ),
inference(instantiation,[status(thm)],[c_5660]) ).
tcf(c_5976,plain,
! [X0: $i] :
( ( inverse(sk_c3) = sk_c8 )
| ( multiply(sk_c6,multiply(sk_c7,X0)) = multiply(identity,X0) ) ),
inference(superposition,[status(thm)],[c_1208,c_115]) ).
tcf(c_5977,plain,
! [X0: $i] :
( ( inverse(sk_c3) = sk_c8 )
| ( multiply(sk_c10,multiply(sk_c6,X0)) = multiply(identity,X0) ) ),
inference(superposition,[status(thm)],[c_1211,c_115]) ).
tcf(c_5995,plain,
! [X0: $i] :
( ( inverse(sk_c3) = sk_c8 )
| ( multiply(sk_c6,multiply(sk_c7,X0)) = X0 ) ),
inference(light_normalisation,[status(thm)],[c_5976,c_113]) ).
tcf(c_6005,plain,
! [X0: $i] :
( ( inverse(sk_c3) = sk_c8 )
| ( multiply(sk_c10,multiply(sk_c6,X0)) = X0 ) ),
inference(light_normalisation,[status(thm)],[c_5977,c_113]) ).
tcf(c_6011,plain,
! [X0: $i] :
( ( inverse(sk_c3) = sk_c8 )
| ( multiply(sk_c10,X0) = multiply(sk_c7,X0) ) ),
inference(superposition,[status(thm)],[c_5995,c_6005]) ).
tcf(c_6027,plain,
( ( inverse(sk_c3) = sk_c8 )
| ( multiply(sk_c10,sk_c10) = sk_c6 ) ),
inference(superposition,[status(thm)],[c_6011,c_175]) ).
tcf(c_6161,plain,
( ~ iPr_def_11
| ( sk_c9 != identity )
| ( inverse(inverse(sk_c10)) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_114,c_726]) ).
tcf(c_6222,plain,
( ( inverse(sk_c3) = sk_c8 )
| ~ iPr_def_12
| ( inverse(sk_c10) != sk_c6 )
| ( inverse(inverse(sk_c10)) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_6027,c_727]) ).
tcf(c_6266,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(X0,X1)) = X1,
inference(demodulation,[status(thm)],[c_1330,c_113]) ).
tcf(c_6319,plain,
( ( inverse(sk_c5) = sk_c9 )
| ( multiply(inverse(sk_c1),sk_c2) = sk_c10 ) ),
inference(superposition,[status(thm)],[c_141,c_6266]) ).
tcf(c_6320,plain,
( ( inverse(sk_c9) = sk_c8 )
| ( multiply(inverse(sk_c1),sk_c2) = sk_c10 ) ),
inference(superposition,[status(thm)],[c_139,c_6266]) ).
tcf(c_6321,plain,
( ( inverse(sk_c4) = sk_c10 )
| ( multiply(inverse(sk_c1),sk_c2) = sk_c10 ) ),
inference(superposition,[status(thm)],[c_138,c_6266]) ).
tcf(c_6327,plain,
( ( inverse(sk_c9) = sk_c8 )
| ( multiply(inverse(sk_c3),sk_c10) = sk_c8 ) ),
inference(superposition,[status(thm)],[c_159,c_6266]) ).
tcf(c_6330,plain,
! [X0: $i] : multiply(inverse(inverse(X0)),identity) = X0,
inference(superposition,[status(thm)],[c_114,c_6266]) ).
tcf(c_6368,plain,
( ( inverse(sk_c9) = sk_c8 )
| ( multiply(sk_c10,sk_c2) = sk_c10 ) ),
inference(superposition,[status(thm)],[c_149,c_6320]) ).
tcf(c_6418,plain,
( ( sk_c10 = sk_c9 )
| ( inverse(sk_c9) = sk_c8 ) ),
inference(superposition,[status(thm)],[c_6368,c_129]) ).
tcf(c_6433,plain,
! [X0: $i] : inverse(inverse(X0)) = X0,
inference(demodulation,[status(thm)],[c_6330,c_4648]) ).
tcf(c_6434,plain,
( ~ iPr_def_10
| ( sk_c10 != identity )
| ( sk_c8 != sk_c8 ) ),
inference(demodulation,[status(thm)],[c_1720,c_6433]) ).
tcf(c_6436,plain,
( ( inverse(sk_c3) = sk_c8 )
| ~ iPr_def_12
| ( inverse(sk_c10) != sk_c6 ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_6222,c_6433]) ).
tcf(c_6438,plain,
( ~ iPr_def_11
| ( sk_c9 != identity ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_6161,c_6433]) ).
tcf(c_6439,plain,
( ~ iPr_def_10
| ( sk_c10 != identity ) ),
inference(equality_resolution_simp,[status(thm)],[c_6434]) ).
tcf(c_6448,plain,
( ( inverse(sk_c3) = sk_c8 )
| ( inverse(sk_c10) = sk_c6 ) ),
inference(superposition,[status(thm)],[c_174,c_6433]) ).
tcf(c_6453,plain,
! [X0: $i,X1: $i] : multiply(X0,multiply(inverse(X0),X1)) = X1,
inference(superposition,[status(thm)],[c_6433,c_6266]) ).
tcf(c_6454,plain,
! [X0: $i] : multiply(X0,inverse(X0)) = identity,
inference(superposition,[status(thm)],[c_6433,c_114]) ).
tcf(c_6458,plain,
( ( inverse(sk_c3) = sk_c8 )
| ( multiply(sk_c4,sk_c10) = identity ) ),
inference(superposition,[status(thm)],[c_168,c_6454]) ).
tcf(c_6459,plain,
( ( inverse(sk_c1) = sk_c10 )
| ( multiply(sk_c4,sk_c10) = identity ) ),
inference(superposition,[status(thm)],[c_148,c_6454]) ).
tcf(c_6475,plain,
! [X0: $i,X1: $i] : multiply(X0,multiply(X1,inverse(multiply(X0,X1)))) = identity,
inference(superposition,[status(thm)],[c_6454,c_115]) ).
tcf(c_6496,plain,
! [X0: $i] : multiply(X0,identity) = inverse(inverse(X0)),
inference(superposition,[status(thm)],[c_6454,c_6453]) ).
tcf(c_6515,plain,
( ~ iPr_def_14
| ( sk_c10 != sk_c9 )
| ( inverse(inverse(sk_c10)) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_6453,c_729]) ).
tcf(c_6521,plain,
( ~ iPr_def_14
| ( sk_c10 != sk_c9 )
| ( multiply(sk_c10,identity) != sk_c10 ) ),
inference(demodulation,[status(thm)],[c_6515,c_6496]) ).
tcf(c_6522,plain,
( ~ iPr_def_14
| ( sk_c10 != sk_c9 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_6521,c_4648]) ).
tcf(c_6636,plain,
! [X0: $i,X1: $i] : multiply(X0,inverse(multiply(X1,X0))) = multiply(inverse(X1),identity),
inference(superposition,[status(thm)],[c_6475,c_6266]) ).
tcf(c_6764,plain,
! [X0: $i] :
( ( sk_c8 = X0 )
| ( sk_c8 != sk_c8 )
| ( X0 != sk_c8 ) ),
inference(instantiation,[status(thm)],[c_4497]) ).
tcf(c_6765,plain,
( ( sk_c8 = sk_c10 )
| ( sk_c10 != sk_c8 )
| ( sk_c8 != sk_c8 ) ),
inference(instantiation,[status(thm)],[c_6764]) ).
tcf(c_6938,plain,
! [X0: $i] :
( ( sk_c8 = X0 )
| ( inverse(sk_c1) = sk_c10 )
| ( X0 != multiply(sk_c9,sk_c10) ) ),
inference(resolution,[status(thm)],[c_4301,c_732]) ).
tcf(c_6939,plain,
( ( sk_c8 = sk_c10 )
| ( inverse(sk_c1) = sk_c10 )
| ( sk_c10 != multiply(sk_c9,sk_c10) ) ),
inference(instantiation,[status(thm)],[c_6938]) ).
tcf(c_6945,plain,
! [X0: $i] :
( ( sk_c8 = X0 )
| ( inverse(sk_c3) = sk_c8 )
| ( X0 != multiply(sk_c9,sk_c10) ) ),
inference(resolution,[status(thm)],[c_4302,c_732]) ).
tcf(c_6946,plain,
( ( sk_c8 = sk_c10 )
| ( inverse(sk_c3) = sk_c8 )
| ( sk_c10 != multiply(sk_c9,sk_c10) ) ),
inference(instantiation,[status(thm)],[c_6945]) ).
tcf(c_7613,plain,
( ( inverse(sk_c9) = sk_c8 )
| ( multiply(sk_c8,sk_c10) = sk_c8 ) ),
inference(superposition,[status(thm)],[c_169,c_6327]) ).
tcf(c_7701,plain,
( ( sk_c9 = identity )
| ( inverse(sk_c3) = sk_c8 ) ),
inference(superposition,[status(thm)],[c_6458,c_167]) ).
tcf(c_7723,plain,
( ( sk_c9 = identity )
| ( multiply(sk_c3,sk_c8) = identity ) ),
inference(superposition,[status(thm)],[c_7701,c_6454]) ).
tcf(c_7786,plain,
( ( sk_c9 = identity )
| ( inverse(sk_c1) = sk_c10 ) ),
inference(superposition,[status(thm)],[c_6459,c_147]) ).
tcf(c_7835,plain,
( ( sk_c9 = identity )
| ( inverse(sk_c4) = sk_c10 )
| ( multiply(sk_c10,sk_c2) = sk_c10 ) ),
inference(superposition,[status(thm)],[c_7786,c_6321]) ).
tcf(c_7837,plain,
( ( sk_c9 = identity )
| ( inverse(sk_c5) = sk_c9 )
| ( multiply(sk_c10,sk_c2) = sk_c10 ) ),
inference(superposition,[status(thm)],[c_7786,c_6319]) ).
tcf(c_7840,plain,
( ( sk_c9 = identity )
| ( multiply(sk_c1,sk_c10) = identity ) ),
inference(superposition,[status(thm)],[c_7786,c_6454]) ).
tcf(c_7979,plain,
( ( sk_c9 = identity )
| ( sk_c10 = identity )
| ( multiply(sk_c9,sk_c10) = sk_c8 ) ),
inference(superposition,[status(thm)],[c_7723,c_156]) ).
tcf(c_7982,plain,
( ( sk_c9 = identity )
| ( sk_c10 = identity )
| ( inverse(sk_c5) = sk_c9 ) ),
inference(superposition,[status(thm)],[c_7723,c_161]) ).
tcf(c_7984,plain,
( ( sk_c9 = identity )
| ( sk_c10 = identity )
| ( inverse(sk_c4) = sk_c10 ) ),
inference(superposition,[status(thm)],[c_7723,c_158]) ).
tcf(c_8086,plain,
( ( sk_c2 = identity )
| ( sk_c9 = identity )
| ( inverse(sk_c5) = sk_c9 ) ),
inference(superposition,[status(thm)],[c_7840,c_141]) ).
tcf(c_8088,plain,
( ( sk_c2 = identity )
| ( sk_c9 = identity )
| ( inverse(sk_c4) = sk_c10 ) ),
inference(superposition,[status(thm)],[c_7840,c_138]) ).
tcf(c_8668,plain,
! [X0: $i] :
( ( sk_c9 = sk_c2 )
| ( sk_c2 != X0 )
| ( sk_c9 != X0 ) ),
inference(instantiation,[status(thm)],[c_1058]) ).
tcf(c_8670,plain,
( ( sk_c9 = sk_c2 )
| ( sk_c2 != sk_c10 )
| ( sk_c9 != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_8668]) ).
tcf(c_8732,plain,
! [X0: $i] :
( ( X0 = multiply(sk_c9,sk_c10) )
| ( inverse(sk_c1) = sk_c10 )
| ( X0 != sk_c8 ) ),
inference(resolution,[status(thm)],[c_2566,c_2669]) ).
tcf(c_8756,plain,
( ( sk_c8 = sk_c9 )
| ( inverse(sk_c9) = sk_c8 ) ),
inference(superposition,[status(thm)],[c_7613,c_119]) ).
tcf(c_8781,plain,
( ( sk_c9 = sk_c8 )
| ( sk_c9 != sk_c9 )
| ( sk_c8 != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_1059]) ).
tcf(c_8801,plain,
! [X0: $i] :
( ( sk_c8 = sk_c9 )
| ( sk_c9 != X0 )
| ( sk_c8 != X0 ) ),
inference(instantiation,[status(thm)],[c_1072]) ).
tcf(c_8805,plain,
( ( sk_c10 = sk_c8 )
| ( sk_c10 != sk_c9 )
| ( sk_c8 != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_2081]) ).
tcf(c_8806,plain,
( ( sk_c8 = sk_c9 )
| ( sk_c9 != sk_c10 )
| ( sk_c8 != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_8801]) ).
tcf(c_8831,plain,
( ( inverse(sk_c3) = sk_c8 )
| ~ iPr_def_12
| ( inverse(sk_c9) != sk_c8 )
| ( inverse(inverse(sk_c9)) != sk_c10 ) ),
inference(resolution,[status(thm)],[c_2567,c_727]) ).
tcf(c_8832,plain,
! [X0: $i] :
( ( X0 = multiply(sk_c9,sk_c10) )
| ( inverse(sk_c3) = sk_c8 )
| ( X0 != sk_c8 ) ),
inference(resolution,[status(thm)],[c_2567,c_2669]) ).
tcf(c_9008,plain,
( ( inverse(sk_c1) = sk_c10 )
| ~ iPr_def_10
| ( sk_c10 != sk_c9 )
| ( inverse(sk_c10) != sk_c8 ) ),
inference(resolution,[status(thm)],[c_2585,c_725]) ).
tcf(c_9313,plain,
! [X0: $i] :
( ( X0 = multiply(sk_c8,sk_c10) )
| ( X0 != multiply(sk_c10,sk_c8) )
| ( multiply(sk_c8,sk_c10) != multiply(sk_c10,sk_c8) ) ),
inference(instantiation,[status(thm)],[c_1456]) ).
tcf(c_9323,plain,
( ( inverse(sk_c1) = sk_c10 )
| ~ iPr_def_11 ),
inference(global_subsumption_just,[status(thm)],[c_2193,c_5154,c_6438]) ).
tcf(c_9341,plain,
( ( inverse(sk_c3) = sk_c8 )
| ~ iPr_def_11 ),
inference(global_subsumption_just,[status(thm)],[c_2194,c_5030,c_6438]) ).
tcf(c_9889,plain,
( ( inverse(sk_c1) = sk_c10 )
| ~ iPr_def_12
| ( inverse(sk_c7) != sk_c6 )
| ( inverse(inverse(sk_c7)) != sk_c10 ) ),
inference(resolution,[status(thm)],[c_2599,c_727]) ).
tcf(c_10008,plain,
( ( inverse(sk_c3) = sk_c8 )
| ~ iPr_def_13 ),
inference(global_subsumption_just,[status(thm)],[c_2330,c_171,c_2333]) ).
tcf(c_10181,plain,
( ( multiply(sk_c10,sk_c8) = sk_c9 )
| ~ iPr_def_10 ),
inference(global_subsumption_just,[status(thm)],[c_2056,c_2501]) ).
tcf(c_10249,plain,
! [X0: $i] :
( ( X0 = multiply(sk_c10,sk_c2) )
| ( inverse(sk_c9) = sk_c8 )
| ( X0 != sk_c9 ) ),
inference(resolution,[status(thm)],[c_2608,c_2669]) ).
tcf(c_10250,plain,
( ( sk_c10 = multiply(sk_c10,sk_c2) )
| ( inverse(sk_c9) = sk_c8 )
| ( sk_c10 != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_10249]) ).
tcf(c_10414,plain,
! [X0: $i] :
( ( multiply(sk_c10,sk_c8) = X0 )
| ~ iPr_def_10
| ( X0 != sk_c9 ) ),
inference(resolution,[status(thm)],[c_10181,c_732]) ).
tcf(c_10415,plain,
( ( multiply(sk_c10,sk_c8) = sk_c10 )
| ~ iPr_def_10
| ( sk_c10 != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_10414]) ).
tcf(c_10634,plain,
( ( multiply(sk_c8,sk_c10) = sk_c9 )
| ~ iPr_def_11 ),
inference(global_subsumption_just,[status(thm)],[c_2195,c_118,c_2195]) ).
tcf(c_10647,plain,
( ~ iPr_def_11
| ( inverse(sk_c8) != sk_c10 ) ),
inference(resolution,[status(thm)],[c_10634,c_726]) ).
tcf(c_10652,plain,
( ( multiply(sk_c10,sk_c2) = sk_c9 )
| ~ iPr_def_11 ),
inference(global_subsumption_just,[status(thm)],[c_2196,c_128,c_2196]) ).
tcf(c_10661,plain,
( iPr_def_14
| iPr_def_13
| iPr_def_12
| iPr_def_10
| ( multiply(sk_c10,sk_c2) = sk_c9 )
| ( inverse(sk_c9) != sk_c8 )
| ( multiply(sk_c10,sk_c8) != sk_c9 )
| ( multiply(sk_c8,sk_c10) != sk_c9 ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_2488,c_10652]) ).
tcf(c_10663,plain,
( ( sk_c9 = multiply(sk_c10,sk_c2) )
| ~ iPr_def_11 ),
inference(resolution,[status(thm)],[c_10652,c_2669]) ).
tcf(c_10691,plain,
( ( inverse(sk_c4) = sk_c10 )
| ~ iPr_def_11
| ( sk_c9 != sk_c2 )
| ( inverse(sk_c1) != sk_c10 ) ),
inference(resolution,[status(thm)],[c_2619,c_726]) ).
tcf(c_10715,plain,
( ( inverse(sk_c5) = sk_c9 )
| ~ iPr_def_11
| ( sk_c9 != sk_c2 )
| ( inverse(sk_c1) != sk_c10 ) ),
inference(resolution,[status(thm)],[c_2621,c_726]) ).
tcf(c_10831,plain,
( ( multiply(sk_c10,sk_c2) = sk_c9 )
| ~ iPr_def_13 ),
inference(global_subsumption_just,[status(thm)],[c_2335,c_131,c_2335]) ).
tcf(c_10866,plain,
( iPr_def_14
| iPr_def_12
| iPr_def_10
| ( multiply(sk_c10,sk_c2) = sk_c9 )
| ( inverse(sk_c9) != sk_c8 )
| ( multiply(sk_c10,sk_c8) != sk_c9 )
| ( multiply(sk_c8,sk_c10) != sk_c9 ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_10661,c_10831]) ).
tcf(c_10868,plain,
( ( sk_c9 = multiply(sk_c10,sk_c2) )
| ~ iPr_def_13 ),
inference(resolution,[status(thm)],[c_10831,c_2669]) ).
tcf(c_10967,plain,
( ( inverse(sk_c4) = sk_c10 )
| ~ iPr_def_13
| ( sk_c9 != sk_c10 )
| ( inverse(sk_c3) != sk_c9 ) ),
inference(resolution,[status(thm)],[c_2644,c_728]) ).
tcf(c_11050,plain,
( ( inverse(sk_c5) = sk_c9 )
| ~ iPr_def_13
| ( sk_c9 != sk_c10 )
| ( inverse(sk_c3) != sk_c9 ) ),
inference(resolution,[status(thm)],[c_2646,c_728]) ).
tcf(c_11317,plain,
( ( multiply(sk_c10,sk_c2) = sk_c9 )
| ~ iPr_def_12
| ( inverse(sk_c4) != sk_c9 )
| ( inverse(inverse(sk_c4)) != sk_c10 ) ),
inference(resolution,[status(thm)],[c_2577,c_727]) ).
tcf(c_11607,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( inverse(X0) = inverse(X2) )
| ( X2 != X1 )
| ( X0 != X1 ) ),
inference(resolution,[status(thm)],[c_2670,c_734]) ).
tcf(c_12278,plain,
! [X0: $i] : multiply(X0,inverse(X0)) = multiply(inverse(identity),identity),
inference(superposition,[status(thm)],[c_113,c_6636]) ).
tcf(c_12290,plain,
inverse(identity) = identity,
inference(superposition,[status(thm)],[c_114,c_4648]) ).
tcf(c_12532,plain,
( ( inverse(sk_c6) = sk_c10 )
| ~ iPr_def_11
| ( inverse(sk_c8) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_124,c_726]) ).
tcf(c_12673,plain,
! [X0: $i] : multiply(X0,inverse(X0)) = multiply(identity,identity),
inference(light_normalisation,[status(thm)],[c_12278,c_12290]) ).
tcf(c_12674,plain,
! [X0: $i] : multiply(X0,inverse(X0)) = identity,
inference(demodulation,[status(thm)],[c_12673,c_113]) ).
tcf(c_12685,plain,
( ( inverse(sk_c9) = sk_c8 )
| ( multiply(sk_c1,sk_c10) = identity ) ),
inference(superposition,[status(thm)],[c_149,c_12674]) ).
tcf(c_12687,plain,
( ( inverse(sk_c9) = sk_c8 )
| ( multiply(sk_c3,sk_c8) = identity ) ),
inference(superposition,[status(thm)],[c_169,c_12674]) ).
tcf(c_12698,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(X0,X1)) = X1,
inference(demodulation,[status(thm)],[c_1330,c_113]) ).
tcf(c_12762,plain,
! [X0: $i] : multiply(inverse(inverse(X0)),identity) = X0,
inference(superposition,[status(thm)],[c_114,c_12698]) ).
tcf(c_12782,plain,
! [X0: $i] : inverse(inverse(X0)) = X0,
inference(demodulation,[status(thm)],[c_12762,c_4648]) ).
tcf(c_13055,plain,
( ( sk_c2 = identity )
| ( inverse(sk_c9) = sk_c8 ) ),
inference(superposition,[status(thm)],[c_12685,c_139]) ).
tcf(c_13063,plain,
( ( sk_c2 = identity )
| ( inverse(sk_c8) = sk_c9 ) ),
inference(superposition,[status(thm)],[c_13055,c_12782]) ).
tcf(c_13081,plain,
( ( sk_c10 = identity )
| ( inverse(sk_c9) = sk_c8 ) ),
inference(superposition,[status(thm)],[c_12687,c_159]) ).
tcf(c_13089,plain,
( ( sk_c10 = identity )
| ( inverse(sk_c8) = sk_c9 ) ),
inference(superposition,[status(thm)],[c_13081,c_12782]) ).
tcf(c_14068,plain,
( ( inverse(sk_c8) != sk_c10 )
| ~ iPr_def_11 ),
inference(global_subsumption_just,[status(thm)],[c_12532,c_10647]) ).
tcf(c_14069,plain,
( ~ iPr_def_11
| ( inverse(sk_c8) != sk_c10 ) ),
inference(renaming,[status(thm)],[c_14068]) ).
tcf(c_14077,plain,
( ( sk_c10 = identity )
| ~ iPr_def_11
| ( sk_c10 != sk_c9 ) ),
inference(superposition,[status(thm)],[c_13089,c_14069]) ).
tcf(c_14078,plain,
( ( sk_c2 = identity )
| ~ iPr_def_11
| ( sk_c10 != sk_c9 ) ),
inference(superposition,[status(thm)],[c_13063,c_14069]) ).
tcf(c_14521,plain,
( ( multiply(sk_c4,sk_c10) = sk_c9 )
| ~ iPr_def_11
| ( sk_c9 != sk_c2 )
| ( inverse(sk_c1) != sk_c10 ) ),
inference(resolution,[status(thm)],[c_2625,c_726]) ).
tcf(c_15279,plain,
( ( inverse(sk_c10) != sk_c8 )
| ( sk_c10 != sk_c9 )
| ~ iPr_def_10 ),
inference(global_subsumption_just,[status(thm)],[c_9008,c_738,c_10415]) ).
tcf(c_15280,plain,
( ~ iPr_def_10
| ( sk_c10 != sk_c9 )
| ( inverse(sk_c10) != sk_c8 ) ),
inference(renaming,[status(thm)],[c_15279]) ).
tcf(c_15333,plain,
( ( inverse(sk_c4) = sk_c10 )
| ~ iPr_def_11
| ( sk_c9 != sk_c2 ) ),
inference(global_subsumption_just,[status(thm)],[c_10691,c_3214,c_9323]) ).
tcf(c_15669,plain,
( ( sk_c9 = multiply(sk_c10,sk_c8) )
| ( sk_c9 != multiply(sk_c8,sk_c10) )
| ( multiply(sk_c10,sk_c8) != multiply(sk_c8,sk_c10) ) ),
inference(instantiation,[status(thm)],[c_1149]) ).
tcf(c_16559,plain,
! [X0: $i] :
( ( sk_c2 = multiply(identity,sk_c9) )
| ( sk_c2 != X0 )
| ( multiply(identity,sk_c9) != X0 ) ),
inference(instantiation,[status(thm)],[c_1133]) ).
tcf(c_16563,plain,
( ( sk_c2 = multiply(identity,sk_c9) )
| ( sk_c2 != sk_c10 )
| ( multiply(identity,sk_c9) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_16559]) ).
tcf(c_19271,plain,
! [X0: $i] :
( ( sk_c2 = X0 )
| ( sk_c2 != identity )
| ( X0 != identity ) ),
inference(instantiation,[status(thm)],[c_4707]) ).
tcf(c_19277,plain,
( ( sk_c2 = sk_c10 )
| ( sk_c2 != identity )
| ( sk_c10 != identity ) ),
inference(instantiation,[status(thm)],[c_19271]) ).
tcf(c_19610,plain,
! [X0: $i] :
( ( multiply(sk_c9,sk_c10) = sk_c8 )
| ( sk_c8 != X0 )
| ( multiply(sk_c9,sk_c10) != X0 ) ),
inference(instantiation,[status(thm)],[c_2352]) ).
tcf(c_20066,plain,
( ( sk_c9 = sk_c2 )
| ( sk_c2 != multiply(identity,sk_c9) )
| ( sk_c9 != multiply(identity,sk_c9) ) ),
inference(instantiation,[status(thm)],[c_8668]) ).
tcf(c_20115,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(X2,X0) = X1 )
| ( X2 != identity )
| ( X0 != X1 ) ),
inference(resolution,[status(thm)],[c_4358,c_4269]) ).
tcf(c_20116,plain,
( ( multiply(sk_c10,sk_c10) = sk_c10 )
| ( sk_c10 != identity )
| ( sk_c10 != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_20115]) ).
tcf(c_20968,plain,
( ( multiply(sk_c10,sk_c8) = multiply(sk_c8,sk_c10) )
| ( multiply(sk_c10,sk_c8) != multiply(sk_c10,sk_c8) )
| ( multiply(sk_c8,sk_c10) != multiply(sk_c10,sk_c8) ) ),
inference(instantiation,[status(thm)],[c_9313]) ).
tcf(c_20998,plain,
( ( inverse(sk_c4) = sk_c10 )
| ~ iPr_def_11 ),
inference(global_subsumption_just,[status(thm)],[c_15333,c_737,c_1155,c_1476,c_3214,c_6438,c_7835,c_7984,c_8088,c_8670,c_9323,c_10663,c_19277]) ).
tcf(c_21072,plain,
( ( inverse(sk_c5) = sk_c9 )
| ~ iPr_def_11 ),
inference(global_subsumption_just,[status(thm)],[c_10715,c_128,c_737,c_1060,c_1069,c_1070,c_1476,c_2196,c_3212,c_4009,c_5662,c_6438,c_7837,c_7982,c_8086,c_9323,c_16563,c_19277,c_20066]) ).
tcf(c_21170,plain,
( ( inverse(sk_c4) = sk_c10 )
| ~ iPr_def_13
| ( sk_c9 != sk_c10 )
| ( sk_c9 != sk_c8 ) ),
inference(resolution,[status(thm)],[c_10967,c_2654]) ).
tcf(c_21246,plain,
! [X0: $i] :
( ( multiply(sk_c5,X0) = sk_c9 )
| ( sk_c9 != multiply(sk_c5,sk_c8) )
| ( multiply(sk_c5,X0) != multiply(sk_c5,sk_c8) ) ),
inference(instantiation,[status(thm)],[c_1442]) ).
tcf(c_21247,plain,
( ( multiply(sk_c5,sk_c10) = sk_c9 )
| ( sk_c9 != multiply(sk_c5,sk_c8) )
| ( multiply(sk_c5,sk_c10) != multiply(sk_c5,sk_c8) ) ),
inference(instantiation,[status(thm)],[c_21246]) ).
tcf(c_21259,plain,
( ( inverse(sk_c5) = sk_c9 )
| ~ iPr_def_13
| ( sk_c9 != sk_c10 )
| ( sk_c9 != sk_c8 ) ),
inference(resolution,[status(thm)],[c_11050,c_2656]) ).
tcf(c_21812,plain,
( ( multiply(sk_c4,sk_c10) = sk_c9 )
| ~ iPr_def_11
| ( sk_c9 != sk_c2 ) ),
inference(global_subsumption_just,[status(thm)],[c_14521,c_9323,c_14521]) ).
tcf(c_21837,plain,
( ~ iPr_def_11
| ( sk_c9 != sk_c2 )
| ( inverse(sk_c4) != sk_c10 ) ),
inference(resolution,[status(thm)],[c_21812,c_726]) ).
tcf(c_21994,plain,
( ~ iPr_def_11
| ( sk_c9 != sk_c2 ) ),
inference(global_subsumption_just,[status(thm)],[c_21837,c_15333,c_21837]) ).
tcf(c_22240,plain,
! [X0: $i] :
( ( multiply(sk_c10,sk_c8) = X0 )
| ( X0 != sk_c9 )
| ( multiply(sk_c10,sk_c8) != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_2308]) ).
tcf(c_22242,plain,
( ( multiply(sk_c10,sk_c8) = sk_c10 )
| ( sk_c10 != sk_c9 )
| ( multiply(sk_c10,sk_c8) != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_22240]) ).
tcf(c_22344,plain,
! [X0: $i,X1: $i] :
( ( multiply(sk_c8,sk_c10) = sk_c9 )
| ( sk_c9 != multiply(X0,X1) )
| ( multiply(sk_c8,sk_c10) != multiply(X0,X1) ) ),
inference(instantiation,[status(thm)],[c_1055]) ).
tcf(c_22345,plain,
( ( multiply(sk_c8,sk_c10) = sk_c9 )
| ( sk_c9 != multiply(sk_c10,sk_c10) )
| ( multiply(sk_c8,sk_c10) != multiply(sk_c10,sk_c10) ) ),
inference(instantiation,[status(thm)],[c_22344]) ).
tcf(c_22772,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X0 = sk_c9 )
| ( sk_c9 != multiply(X1,X2) )
| ( X0 != multiply(X1,X2) ) ),
inference(instantiation,[status(thm)],[c_1072]) ).
tcf(c_22773,plain,
( ( sk_c10 = sk_c9 )
| ( sk_c9 != multiply(sk_c10,sk_c10) )
| ( sk_c10 != multiply(sk_c10,sk_c10) ) ),
inference(instantiation,[status(thm)],[c_22772]) ).
tcf(c_23288,plain,
( ( inverse(sk_c3) = sk_c8 )
| ~ iPr_def_12 ),
inference(global_subsumption_just,[status(thm)],[c_8831,c_6436,c_6448]) ).
tcf(c_23398,plain,
( ( inverse(sk_c1) = sk_c10 )
| ~ iPr_def_12
| ( inverse(inverse(sk_c7)) != sk_c10 ) ),
inference(global_subsumption_just,[status(thm)],[c_9889,c_153,c_3795]) ).
tcf(c_26355,plain,
! [X0: $i,X1: $i] :
( ( multiply(sk_c9,sk_c10) = multiply(X1,X0) )
| ( sk_c9 != X1 )
| ( sk_c10 != X0 ) ),
inference(instantiation,[status(thm)],[c_733]) ).
tcf(c_26357,plain,
( ( multiply(sk_c9,sk_c10) = multiply(sk_c10,sk_c10) )
| ( sk_c9 != sk_c10 )
| ( sk_c10 != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_26355]) ).
tcf(c_26454,plain,
! [X0: $i] :
( ( multiply(sk_c9,sk_c10) = sk_c9 )
| ( sk_c9 != X0 )
| ( multiply(sk_c9,sk_c10) != X0 ) ),
inference(instantiation,[status(thm)],[c_1072]) ).
tcf(c_26455,plain,
( ( multiply(sk_c9,sk_c10) = sk_c8 )
| ( sk_c8 != sk_c9 )
| ( multiply(sk_c9,sk_c10) != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_19610]) ).
tcf(c_26456,plain,
( ( multiply(sk_c9,sk_c10) = sk_c9 )
| ( sk_c9 != sk_c10 )
| ( multiply(sk_c9,sk_c10) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_26454]) ).
tcf(c_30567,plain,
inverse(identity) = identity,
inference(superposition,[status(thm)],[c_114,c_4648]) ).
tcf(c_30727,plain,
! [X0: $i,X1: $i] : multiply(X0,inverse(multiply(X1,X0))) = inverse(X1),
inference(demodulation,[status(thm)],[c_6636,c_4648]) ).
tcf(c_30747,plain,
( ( inverse(sk_c1) = sk_c10 )
| ( multiply(sk_c8,inverse(sk_c9)) = inverse(sk_c10) ) ),
inference(superposition,[status(thm)],[c_150,c_30727]) ).
tcf(c_30752,plain,
( ( inverse(sk_c1) = sk_c10 )
| ( multiply(sk_c8,inverse(sk_c9)) = inverse(sk_c5) ) ),
inference(superposition,[status(thm)],[c_152,c_30727]) ).
tcf(c_30778,plain,
! [X0: $i] : multiply(X0,inverse(X0)) = inverse(identity),
inference(superposition,[status(thm)],[c_113,c_30727]) ).
tcf(c_30779,plain,
! [X0: $i] : multiply(X0,inverse(identity)) = inverse(inverse(X0)),
inference(superposition,[status(thm)],[c_114,c_30727]) ).
tcf(c_30780,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(X0,inverse(multiply(X1,multiply(X2,X0)))) = inverse(multiply(X1,X2)),
inference(superposition,[status(thm)],[c_115,c_30727]) ).
tcf(c_30889,plain,
( ~ iPr_def_11
| ( sk_c10 != sk_c9 )
| ( inverse(identity) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_113,c_726]) ).
tcf(c_30979,plain,
( ( inverse(sk_c4) = sk_c10 )
| ~ iPr_def_14
| ( inverse(sk_c1) != sk_c10 )
| ( multiply(sk_c10,sk_c2) != sk_c9 ) ),
inference(superposition,[status(thm)],[c_138,c_729]) ).
tcf(c_30987,plain,
! [X0: $i] : multiply(X0,inverse(X0)) = identity,
inference(light_normalisation,[status(thm)],[c_30778,c_30567]) ).
tcf(c_30997,plain,
( ( inverse(sk_c1) = sk_c10 )
| ( multiply(sk_c7,sk_c6) = identity ) ),
inference(superposition,[status(thm)],[c_153,c_30987]) ).
tcf(c_31005,plain,
! [X0: $i,X1: $i] : multiply(X0,multiply(inverse(X0),X1)) = multiply(identity,X1),
inference(superposition,[status(thm)],[c_30987,c_115]) ).
tcf(c_31010,plain,
! [X0: $i] : inverse(inverse(X0)) = X0,
inference(light_normalisation,[status(thm)],[c_30779,c_4648,c_30567]) ).
tcf(c_31011,plain,
! [X0: $i] :
( ~ iPr_def_12
| ( X0 != sk_c10 )
| ( multiply(X0,sk_c10) != inverse(X0) ) ),
inference(demodulation,[status(thm)],[c_727,c_31010]) ).
tcf(c_31020,plain,
( ( inverse(sk_c3) = sk_c8 )
| ( inverse(sk_c6) = sk_c7 ) ),
inference(superposition,[status(thm)],[c_173,c_31010]) ).
tcf(c_31041,plain,
! [X0: $i,X1: $i] : multiply(X0,multiply(inverse(X0),X1)) = X1,
inference(demodulation,[status(thm)],[c_31005,c_113]) ).
tcf(c_31053,plain,
! [X0: $i] :
( ( inverse(sk_c3) = sk_c8 )
| ( multiply(sk_c5,multiply(sk_c9,X0)) = X0 ) ),
inference(superposition,[status(thm)],[c_171,c_31041]) ).
tcf(c_31054,plain,
! [X0: $i] :
( ( inverse(sk_c1) = sk_c10 )
| ( multiply(sk_c5,multiply(sk_c9,X0)) = X0 ) ),
inference(superposition,[status(thm)],[c_151,c_31041]) ).
tcf(c_31056,plain,
! [X0: $i] :
( ( inverse(sk_c1) = sk_c10 )
| ( multiply(sk_c7,multiply(sk_c6,X0)) = X0 ) ),
inference(superposition,[status(thm)],[c_153,c_31041]) ).
tcf(c_31102,plain,
( ( sk_c10 = sk_c7 )
| ( inverse(sk_c3) = sk_c8 ) ),
inference(superposition,[status(thm)],[c_31020,c_174]) ).
tcf(c_31113,plain,
( ( sk_c10 = sk_c7 )
| ( multiply(sk_c8,sk_c3) = identity ) ),
inference(superposition,[status(thm)],[c_31102,c_114]) ).
tcf(c_31158,plain,
! [X0: $i] :
( ( sk_c10 = sk_c7 )
| ( multiply(sk_c8,multiply(sk_c3,X0)) = multiply(identity,X0) ) ),
inference(superposition,[status(thm)],[c_31113,c_115]) ).
tcf(c_31513,plain,
( ~ iPr_def_11
| ( sk_c10 != sk_c9 ) ),
inference(global_subsumption_just,[status(thm)],[c_30889,c_1061,c_1060,c_8670,c_14078,c_14077,c_19277,c_21994]) ).
tcf(c_31679,plain,
( ( inverse(sk_c1) = sk_c10 )
| ( inverse(sk_c10) = inverse(sk_c5) ) ),
inference(superposition,[status(thm)],[c_30752,c_30747]) ).
tcf(c_31848,plain,
! [X0: $i] :
( ( inverse(sk_c1) = sk_c10 )
| ( multiply(inverse(sk_c6),X0) = multiply(sk_c7,X0) ) ),
inference(superposition,[status(thm)],[c_31041,c_31056]) ).
tcf(c_32161,plain,
( ( inverse(sk_c3) = sk_c8 )
| ( multiply(sk_c5,sk_c8) = sk_c10 ) ),
inference(superposition,[status(thm)],[c_166,c_31053]) ).
tcf(c_32191,plain,
( ( sk_c10 = sk_c9 )
| ( inverse(sk_c3) = sk_c8 ) ),
inference(superposition,[status(thm)],[c_32161,c_172]) ).
tcf(c_32195,plain,
( ( inverse(sk_c3) = sk_c8 )
| ~ iPr_def_10
| ( inverse(sk_c5) != sk_c8 ) ),
inference(superposition,[status(thm)],[c_32161,c_725]) ).
tcf(c_32209,plain,
( ( inverse(sk_c1) = sk_c10 )
| ( multiply(sk_c5,sk_c8) = sk_c10 ) ),
inference(superposition,[status(thm)],[c_146,c_31054]) ).
tcf(c_32239,plain,
( ( sk_c10 = sk_c9 )
| ( inverse(sk_c1) = sk_c10 ) ),
inference(superposition,[status(thm)],[c_32209,c_152]) ).
tcf(c_33266,plain,
( ( inverse(sk_c3) = sk_c8 )
| ~ iPr_def_10
| ( sk_c8 != sk_c9 ) ),
inference(superposition,[status(thm)],[c_171,c_32195]) ).
tcf(c_33271,plain,
( ( inverse(sk_c3) = sk_c8 )
| ( sk_c8 != sk_c9 ) ),
inference(global_subsumption_just,[status(thm)],[c_33266,c_174,c_169,c_170,c_166,c_730,c_1078,c_1366,c_2351,c_3810,c_4312,c_6765,c_8805,c_9341,c_10008,c_23288,c_32191,c_33266]) ).
tcf(c_33702,plain,
! [X0: $i,X1: $i] : inverse(multiply(inverse(multiply(X0,X1)),X0)) = multiply(X1,inverse(identity)),
inference(superposition,[status(thm)],[c_114,c_30780]) ).
tcf(c_34360,plain,
! [X0: $i,X1: $i] : inverse(multiply(inverse(multiply(X0,X1)),X0)) = multiply(X1,identity),
inference(light_normalisation,[status(thm)],[c_33702,c_30567]) ).
tcf(c_34361,plain,
! [X0: $i,X1: $i] : inverse(multiply(inverse(multiply(X0,X1)),X0)) = X1,
inference(demodulation,[status(thm)],[c_34360,c_4648]) ).
tcf(c_34555,plain,
! [X0: $i,X1: $i] : multiply(inverse(multiply(X0,X1)),X0) = inverse(X1),
inference(superposition,[status(thm)],[c_34361,c_31010]) ).
tcf(c_34896,plain,
! [X0: $i] : multiply(inverse(identity),X0) = inverse(inverse(X0)),
inference(superposition,[status(thm)],[c_30987,c_34555]) ).
tcf(c_34901,plain,
( ( inverse(sk_c1) = sk_c10 )
| ( multiply(inverse(identity),sk_c7) = inverse(sk_c6) ) ),
inference(superposition,[status(thm)],[c_30997,c_34555]) ).
tcf(c_34987,plain,
( ( inverse(sk_c1) = sk_c10 )
| ( inverse(inverse(sk_c7)) = inverse(sk_c6) ) ),
inference(demodulation,[status(thm)],[c_34901,c_34896]) ).
tcf(c_36690,plain,
! [X0: $i] : inverse(inverse(X0)) = inverse(inverse(X0)),
inference(instantiation,[status(thm)],[c_731]) ).
tcf(c_36692,plain,
inverse(inverse(sk_c10)) = inverse(inverse(sk_c10)),
inference(instantiation,[status(thm)],[c_36690]) ).
tcf(c_36693,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( inverse(inverse(X0)) = X2 )
| ( X2 != X1 )
| ( inverse(inverse(X0)) != X1 ) ),
inference(instantiation,[status(thm)],[c_732]) ).
tcf(c_36695,plain,
! [X0: $i,X1: $i] :
( ( inverse(inverse(X0)) = inverse(X1) )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_734]) ).
tcf(c_36702,plain,
! [X0: $i,X1: $i] :
( ( sk_c10 = inverse(X0) )
| ( sk_c10 != X1 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_732]) ).
tcf(c_36709,plain,
! [X0: $i,X1: $i] :
( ( inverse(inverse(X0)) = X1 )
| ( X1 != inverse(inverse(X0)) )
| ( inverse(inverse(X0)) != inverse(inverse(X0)) ) ),
inference(instantiation,[status(thm)],[c_36693]) ).
tcf(c_36713,plain,
( ( inverse(inverse(sk_c7)) = inverse(sk_c6) )
| ( inverse(sk_c7) != sk_c6 ) ),
inference(instantiation,[status(thm)],[c_36695]) ).
tcf(c_36716,plain,
( ( inverse(inverse(sk_c3)) = inverse(sk_c8) )
| ( inverse(sk_c3) != sk_c8 ) ),
inference(instantiation,[status(thm)],[c_36695]) ).
tcf(c_36718,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( inverse(X0) = X2 )
| ( X2 != X1 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_732]) ).
tcf(c_36734,plain,
! [X0: $i] :
( ( inverse(inverse(sk_c7)) = X0 )
| ( X0 != inverse(sk_c6) )
| ( inverse(inverse(sk_c7)) != inverse(sk_c6) ) ),
inference(instantiation,[status(thm)],[c_36693]) ).
tcf(c_36736,plain,
( ( inverse(inverse(sk_c7)) = sk_c10 )
| ( sk_c10 != inverse(sk_c6) )
| ( inverse(inverse(sk_c7)) != inverse(sk_c6) ) ),
inference(instantiation,[status(thm)],[c_36734]) ).
tcf(c_36765,plain,
( ( sk_c10 = inverse(sk_c6) )
| ( sk_c10 != sk_c10 )
| ( inverse(sk_c6) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_36702]) ).
tcf(c_36770,plain,
! [X0: $i,X1: $i] :
( ( sk_c10 = inverse(X0) )
| ( sk_c10 != inverse(X1) )
| ( inverse(X0) != inverse(X1) ) ),
inference(instantiation,[status(thm)],[c_36702]) ).
tcf(c_36784,plain,
! [X0: $i] :
( ( inverse(inverse(X0)) = multiply(identity,inverse(inverse(X0))) )
| ( inverse(inverse(X0)) != inverse(inverse(X0)) )
| ( multiply(identity,inverse(inverse(X0))) != inverse(inverse(X0)) ) ),
inference(instantiation,[status(thm)],[c_36709]) ).
tcf(c_36785,plain,
! [X0: $i] : multiply(identity,inverse(inverse(X0))) = inverse(inverse(X0)),
inference(instantiation,[status(thm)],[c_113]) ).
tcf(c_36786,plain,
( ( inverse(inverse(sk_c10)) = multiply(identity,inverse(inverse(sk_c10))) )
| ( inverse(inverse(sk_c10)) != inverse(inverse(sk_c10)) )
| ( multiply(identity,inverse(inverse(sk_c10))) != inverse(inverse(sk_c10)) ) ),
inference(instantiation,[status(thm)],[c_36784]) ).
tcf(c_36787,plain,
multiply(identity,inverse(inverse(sk_c10))) = inverse(inverse(sk_c10)),
inference(instantiation,[status(thm)],[c_36785]) ).
tcf(c_36789,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = inverse(inverse(X0)) )
| ( X2 != X1 )
| ( inverse(inverse(X0)) != X1 ) ),
inference(instantiation,[status(thm)],[c_732]) ).
tcf(c_36791,plain,
! [X0: $i,X1: $i] :
( ( inverse(X0) = inverse(inverse(X1)) )
| ( X0 != inverse(X1) ) ),
inference(instantiation,[status(thm)],[c_734]) ).
tcf(c_36794,plain,
! [X0: $i] :
( ( inverse(inverse(X0)) = multiply(inverse(inverse(X0)),identity) )
| ( inverse(inverse(X0)) != inverse(inverse(X0)) )
| ( multiply(inverse(inverse(X0)),identity) != inverse(inverse(X0)) ) ),
inference(instantiation,[status(thm)],[c_36709]) ).
tcf(c_36795,plain,
! [X0: $i] : multiply(inverse(inverse(X0)),identity) = inverse(inverse(X0)),
inference(instantiation,[status(thm)],[c_4648]) ).
tcf(c_36796,plain,
( ( inverse(inverse(sk_c10)) = multiply(inverse(inverse(sk_c10)),identity) )
| ( inverse(inverse(sk_c10)) != inverse(inverse(sk_c10)) )
| ( multiply(inverse(inverse(sk_c10)),identity) != inverse(inverse(sk_c10)) ) ),
inference(instantiation,[status(thm)],[c_36794]) ).
tcf(c_36797,plain,
multiply(inverse(inverse(sk_c10)),identity) = inverse(inverse(sk_c10)),
inference(instantiation,[status(thm)],[c_36795]) ).
tcf(c_36803,plain,
! [X0: $i] :
( ( inverse(sk_c5) = X0 )
| ( X0 != sk_c9 )
| ( inverse(sk_c5) != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_36718]) ).
tcf(c_36804,plain,
! [X0: $i] :
( ( inverse(sk_c7) = X0 )
| ( X0 != sk_c6 )
| ( inverse(sk_c7) != sk_c6 ) ),
inference(instantiation,[status(thm)],[c_36718]) ).
tcf(c_36808,plain,
! [X0: $i] :
( ( inverse(sk_c3) = X0 )
| ( X0 != sk_c8 )
| ( inverse(sk_c3) != sk_c8 ) ),
inference(instantiation,[status(thm)],[c_36718]) ).
tcf(c_36810,plain,
! [X0: $i,X1: $i] :
( ( inverse(X0) = X1 )
| ( X1 != inverse(X0) )
| ( inverse(X0) != inverse(X0) ) ),
inference(instantiation,[status(thm)],[c_36718]) ).
tcf(c_36811,plain,
! [X0: $i] : inverse(X0) = inverse(X0),
inference(instantiation,[status(thm)],[c_731]) ).
tcf(c_36815,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( inverse(X0) = X2 )
| ( X2 != inverse(X1) )
| ( inverse(X0) != inverse(X1) ) ),
inference(instantiation,[status(thm)],[c_36718]) ).
tcf(c_36844,plain,
! [X0: $i,X1: $i] :
( ( inverse(sk_c5) = X1 )
| ( X1 != X0 )
| ( inverse(sk_c5) != X0 ) ),
inference(instantiation,[status(thm)],[c_36718]) ).
tcf(c_36862,plain,
! [X0: $i] :
( ( sk_c10 = inverse(sk_c3) )
| ( sk_c10 != X0 )
| ( inverse(sk_c3) != X0 ) ),
inference(instantiation,[status(thm)],[c_36702]) ).
tcf(c_36865,plain,
( ( sk_c10 = inverse(sk_c3) )
| ( sk_c10 != sk_c10 )
| ( inverse(sk_c3) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_36862]) ).
tcf(c_36880,plain,
! [X0: $i,X1: $i] :
( ( X1 = inverse(sk_c10) )
| ( X1 != X0 )
| ( inverse(sk_c10) != X0 ) ),
inference(instantiation,[status(thm)],[c_732]) ).
tcf(c_36914,plain,
! [X0: $i,X1: $i] :
( ( X1 = inverse(sk_c9) )
| ( X1 != X0 )
| ( inverse(sk_c9) != X0 ) ),
inference(instantiation,[status(thm)],[c_732]) ).
tcf(c_36917,plain,
! [X0: $i] :
( ( inverse(X0) = inverse(sk_c9) )
| ( X0 != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_734]) ).
tcf(c_36919,plain,
( ( inverse(sk_c10) = inverse(sk_c9) )
| ( sk_c10 != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_36917]) ).
tcf(c_36979,plain,
( ( inverse(sk_c5) = inverse(sk_c8) )
| ( inverse(sk_c5) != sk_c9 )
| ( inverse(sk_c8) != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_36803]) ).
tcf(c_37048,plain,
! [X0: $i] :
( ( sk_c10 = inverse(X0) )
| ( sk_c10 != inverse(sk_c5) )
| ( inverse(X0) != inverse(sk_c5) ) ),
inference(instantiation,[status(thm)],[c_36770]) ).
tcf(c_37049,plain,
( ( sk_c10 = inverse(sk_c10) )
| ( sk_c10 != inverse(sk_c5) )
| ( inverse(sk_c10) != inverse(sk_c5) ) ),
inference(instantiation,[status(thm)],[c_37048]) ).
tcf(c_37060,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = inverse(X0) )
| ( X2 != X1 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_732]) ).
tcf(c_37071,plain,
( ( inverse(sk_c10) = inverse(inverse(sk_c3)) )
| ( sk_c10 != inverse(sk_c3) ) ),
inference(instantiation,[status(thm)],[c_36791]) ).
tcf(c_37096,plain,
! [X0: $i] :
( ( X0 = inverse(inverse(sk_c3)) )
| ( X0 != inverse(sk_c8) )
| ( inverse(inverse(sk_c3)) != inverse(sk_c8) ) ),
inference(instantiation,[status(thm)],[c_36789]) ).
tcf(c_37102,plain,
! [X0: $i,X1: $i] :
( ( X1 = inverse(inverse(X0)) )
| ( X1 != multiply(identity,inverse(inverse(X0))) )
| ( inverse(inverse(X0)) != multiply(identity,inverse(inverse(X0))) ) ),
inference(instantiation,[status(thm)],[c_36789]) ).
tcf(c_37109,plain,
! [X0: $i] :
( ( inverse(sk_c10) = X0 )
| ( X0 != sk_c1 )
| ( inverse(sk_c10) != sk_c1 ) ),
inference(instantiation,[status(thm)],[c_36718]) ).
tcf(c_37110,plain,
( ( sk_c10 = inverse(sk_c10) )
| ( sk_c10 != sk_c1 )
| ( inverse(sk_c10) != sk_c1 ) ),
inference(instantiation,[status(thm)],[c_36702]) ).
tcf(c_37112,plain,
( ( inverse(sk_c10) = sk_c10 )
| ( sk_c10 != sk_c1 )
| ( inverse(sk_c10) != sk_c1 ) ),
inference(instantiation,[status(thm)],[c_37109]) ).
tcf(c_37121,plain,
( ( inverse(sk_c1) = sk_c10 )
| ( sk_c10 != inverse(sk_c1) )
| ( inverse(sk_c1) != inverse(sk_c1) ) ),
inference(instantiation,[status(thm)],[c_36810]) ).
tcf(c_37124,plain,
! [X0: $i,X1: $i] :
( ( inverse(X0) = inverse(X1) )
| ( inverse(X1) != inverse(X0) )
| ( inverse(X0) != inverse(X0) ) ),
inference(instantiation,[status(thm)],[c_36810]) ).
tcf(c_37151,plain,
! [X0: $i,X1: $i] :
( ( inverse(inverse(X0)) = X1 )
| ( X1 != multiply(inverse(inverse(X0)),identity) )
| ( inverse(inverse(X0)) != multiply(inverse(inverse(X0)),identity) ) ),
inference(instantiation,[status(thm)],[c_36718]) ).
tcf(c_37152,plain,
! [X0: $i] :
( ( sk_c10 = inverse(inverse(X0)) )
| ( sk_c10 != multiply(inverse(inverse(X0)),identity) )
| ( inverse(inverse(X0)) != multiply(inverse(inverse(X0)),identity) ) ),
inference(instantiation,[status(thm)],[c_36702]) ).
tcf(c_37155,plain,
( ( sk_c10 = inverse(inverse(sk_c10)) )
| ( sk_c10 != multiply(inverse(inverse(sk_c10)),identity) )
| ( inverse(inverse(sk_c10)) != multiply(inverse(inverse(sk_c10)),identity) ) ),
inference(instantiation,[status(thm)],[c_37152]) ).
tcf(c_37156,plain,
( ( inverse(inverse(sk_c10)) = sk_c10 )
| ( sk_c10 != multiply(inverse(inverse(sk_c10)),identity) )
| ( inverse(inverse(sk_c10)) != multiply(inverse(inverse(sk_c10)),identity) ) ),
inference(instantiation,[status(thm)],[c_37151]) ).
tcf(c_37157,plain,
! [X0: $i,X1: $i] :
( ( X1 = inverse(inverse(X0)) )
| ( X1 != multiply(inverse(inverse(X0)),identity) )
| ( inverse(inverse(X0)) != multiply(inverse(inverse(X0)),identity) ) ),
inference(instantiation,[status(thm)],[c_36789]) ).
tcf(c_37167,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( inverse(X0) = inverse(X2) )
| ( inverse(X2) != inverse(X1) )
| ( inverse(X0) != inverse(X1) ) ),
inference(instantiation,[status(thm)],[c_36815]) ).
tcf(c_37691,plain,
! [X0: $i,X1: $i] :
( ( sk_c10 = multiply(inverse(inverse(X0)),identity) )
| ( sk_c10 != X1 )
| ( multiply(inverse(inverse(X0)),identity) != X1 ) ),
inference(instantiation,[status(thm)],[c_732]) ).
tcf(c_37692,plain,
( ( sk_c10 = multiply(inverse(inverse(sk_c10)),identity) )
| ( sk_c10 != sk_c10 )
| ( multiply(inverse(inverse(sk_c10)),identity) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_37691]) ).
tcf(c_37758,plain,
! [X0: $i] :
( ( inverse(sk_c5) = X0 )
| ( X0 != inverse(sk_c10) )
| ( inverse(sk_c5) != inverse(sk_c10) ) ),
inference(instantiation,[status(thm)],[c_36844]) ).
tcf(c_37761,plain,
( ( inverse(sk_c5) = sk_c10 )
| ( sk_c10 != inverse(sk_c10) )
| ( inverse(sk_c5) != inverse(sk_c10) ) ),
inference(instantiation,[status(thm)],[c_37758]) ).
tcf(c_37871,plain,
! [X0: $i] :
( ( inverse(X0) = inverse(inverse(sk_c3)) )
| ( inverse(X0) != inverse(sk_c8) )
| ( inverse(inverse(sk_c3)) != inverse(sk_c8) ) ),
inference(instantiation,[status(thm)],[c_37096]) ).
tcf(c_37931,plain,
! [X0: $i] :
( ( multiply(sk_c9,sk_c10) = inverse(sk_c9) )
| ( inverse(sk_c9) != X0 )
| ( multiply(sk_c9,sk_c10) != X0 ) ),
inference(instantiation,[status(thm)],[c_36914]) ).
tcf(c_37948,plain,
! [X0: $i,X1: $i] :
( ( inverse(X0) = X1 )
| ( X1 != inverse(sk_c9) )
| ( inverse(X0) != inverse(sk_c9) ) ),
inference(instantiation,[status(thm)],[c_36815]) ).
tcf(c_37958,plain,
! [X0: $i] :
( ( sk_c10 = inverse(sk_c9) )
| ( sk_c10 != X0 )
| ( inverse(sk_c9) != X0 ) ),
inference(instantiation,[status(thm)],[c_36914]) ).
tcf(c_38161,plain,
! [X0: $i] :
( ( X0 = inverse(sk_c3) )
| ( X0 != sk_c8 )
| ( inverse(sk_c3) != sk_c8 ) ),
inference(instantiation,[status(thm)],[c_37060]) ).
tcf(c_38162,plain,
! [X0: $i,X1: $i] :
( ( X1 = inverse(inverse(X0)) )
| ( X1 != sk_c10 )
| ( inverse(inverse(X0)) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_37060]) ).
tcf(c_38349,plain,
! [X0: $i] :
( ( inverse(sk_c5) = inverse(sk_c10) )
| ( inverse(sk_c5) != inverse(X0) )
| ( inverse(sk_c10) != inverse(X0) ) ),
inference(instantiation,[status(thm)],[c_37167]) ).
tcf(c_38563,plain,
! [X0: $i,X1: $i] :
( ( multiply(sk_c9,sk_c10) = X1 )
| ( X1 != X0 )
| ( multiply(sk_c9,sk_c10) != X0 ) ),
inference(instantiation,[status(thm)],[c_732]) ).
tcf(c_38565,plain,
! [X0: $i,X1: $i] :
( ( multiply(sk_c9,sk_c10) = multiply(X1,X0) )
| ( sk_c9 != X1 )
| ( sk_c10 != X0 ) ),
inference(instantiation,[status(thm)],[c_733]) ).
tcf(c_38883,plain,
( ( inverse(sk_c7) = multiply(sk_c6,identity) )
| ( inverse(sk_c7) != sk_c6 )
| ( multiply(sk_c6,identity) != sk_c6 ) ),
inference(instantiation,[status(thm)],[c_36804]) ).
tcf(c_38884,plain,
multiply(sk_c6,identity) = sk_c6,
inference(instantiation,[status(thm)],[c_4648]) ).
tcf(c_39829,plain,
! [X0: $i] :
( ( inverse(X0) = inverse(sk_c5) )
| ( inverse(sk_c5) != inverse(X0) )
| ( inverse(X0) != inverse(X0) ) ),
inference(instantiation,[status(thm)],[c_37124]) ).
tcf(c_39831,plain,
( ( inverse(sk_c10) = inverse(sk_c5) )
| ( inverse(sk_c5) != inverse(sk_c10) )
| ( inverse(sk_c10) != inverse(sk_c10) ) ),
inference(instantiation,[status(thm)],[c_39829]) ).
tcf(c_40086,plain,
! [X0: $i] :
( ( inverse(sk_c5) = inverse(sk_c10) )
| ( inverse(sk_c5) != inverse(inverse(X0)) )
| ( inverse(sk_c10) != inverse(inverse(X0)) ) ),
inference(instantiation,[status(thm)],[c_38349]) ).
tcf(c_40383,plain,
! [X0: $i] :
( ( multiply(sk_c9,sk_c10) = inverse(sk_c10) )
| ( inverse(sk_c10) != X0 )
| ( multiply(sk_c9,sk_c10) != X0 ) ),
inference(instantiation,[status(thm)],[c_36880]) ).
tcf(c_40384,plain,
( ( multiply(sk_c9,sk_c10) = inverse(sk_c9) )
| ( inverse(sk_c9) != inverse(sk_c10) )
| ( multiply(sk_c9,sk_c10) != inverse(sk_c10) ) ),
inference(instantiation,[status(thm)],[c_37931]) ).
tcf(c_40385,plain,
( ( multiply(sk_c9,sk_c10) = inverse(sk_c10) )
| ( inverse(sk_c10) != sk_c10 )
| ( multiply(sk_c9,sk_c10) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_40383]) ).
tcf(c_40836,plain,
! [X0: $i,X1: $i] :
( ( multiply(X0,sk_c10) = inverse(X0) )
| ( inverse(X0) != X1 )
| ( multiply(X0,sk_c10) != X1 ) ),
inference(instantiation,[status(thm)],[c_37060]) ).
tcf(c_41237,plain,
inverse(sk_c9) = inverse(sk_c9),
inference(instantiation,[status(thm)],[c_36811]) ).
tcf(c_41571,plain,
( ( inverse(sk_c10) = sk_c8 )
| ( sk_c8 != inverse(sk_c9) )
| ( inverse(sk_c10) != inverse(sk_c9) ) ),
inference(instantiation,[status(thm)],[c_37948]) ).
tcf(c_42108,plain,
! [X0: $i,X1: $i] :
( ( X0 = sk_c8 )
| ( sk_c8 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_732]) ).
tcf(c_42112,plain,
multiply(sk_c8,identity) = sk_c8,
inference(instantiation,[status(thm)],[c_4648]) ).
tcf(c_42143,plain,
( ( inverse(sk_c3) = multiply(sk_c9,sk_c10) )
| ( inverse(sk_c3) != sk_c8 )
| ( multiply(sk_c9,sk_c10) != sk_c8 ) ),
inference(instantiation,[status(thm)],[c_36808]) ).
tcf(c_42144,plain,
( ( inverse(sk_c3) = inverse(sk_c9) )
| ( inverse(sk_c3) != sk_c8 )
| ( inverse(sk_c9) != sk_c8 ) ),
inference(instantiation,[status(thm)],[c_36808]) ).
tcf(c_42650,plain,
( ( inverse(sk_c5) = inverse(inverse(sk_c3)) )
| ( inverse(sk_c5) != inverse(sk_c8) )
| ( inverse(inverse(sk_c3)) != inverse(sk_c8) ) ),
inference(instantiation,[status(thm)],[c_37871]) ).
tcf(c_43370,plain,
! [X0: $i] :
( ( sk_c10 = inverse(sk_c9) )
| ( sk_c10 != inverse(X0) )
| ( inverse(sk_c9) != inverse(X0) ) ),
inference(instantiation,[status(thm)],[c_37958]) ).
tcf(c_43371,plain,
! [X0: $i] :
( ( inverse(sk_c9) = inverse(X0) )
| ( inverse(sk_c9) != inverse(sk_c9) )
| ( inverse(X0) != inverse(sk_c9) ) ),
inference(instantiation,[status(thm)],[c_37124]) ).
tcf(c_43372,plain,
! [X0: $i] :
( ( inverse(sk_c9) = inverse(X0) )
| ( sk_c9 != X0 ) ),
inference(instantiation,[status(thm)],[c_734]) ).
tcf(c_43373,plain,
( ( sk_c10 = inverse(sk_c9) )
| ( sk_c10 != inverse(sk_c10) )
| ( inverse(sk_c9) != inverse(sk_c10) ) ),
inference(instantiation,[status(thm)],[c_43370]) ).
tcf(c_43374,plain,
( ( inverse(sk_c9) = inverse(sk_c10) )
| ( sk_c9 != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_43372]) ).
tcf(c_43375,plain,
( ( inverse(sk_c9) = inverse(sk_c10) )
| ( inverse(sk_c9) != inverse(sk_c9) )
| ( inverse(sk_c10) != inverse(sk_c9) ) ),
inference(instantiation,[status(thm)],[c_43371]) ).
tcf(c_43521,plain,
( ( sk_c8 = inverse(sk_c3) )
| ( sk_c8 != sk_c8 )
| ( inverse(sk_c3) != sk_c8 ) ),
inference(instantiation,[status(thm)],[c_38161]) ).
tcf(c_44406,plain,
! [X0: $i,X1: $i] :
( ( inverse(X0) = X1 )
| ( X1 != inverse(sk_c3) )
| ( inverse(X0) != inverse(sk_c3) ) ),
inference(instantiation,[status(thm)],[c_36815]) ).
tcf(c_44657,plain,
! [X0: $i] :
( ( inverse(X0) = multiply(sk_c9,sk_c10) )
| ( inverse(X0) != inverse(sk_c9) )
| ( multiply(sk_c9,sk_c10) != inverse(sk_c9) ) ),
inference(instantiation,[status(thm)],[c_37948]) ).
tcf(c_44664,plain,
! [X0: $i] :
( ( inverse(sk_c9) = X0 )
| ( X0 != multiply(sk_c9,sk_c10) )
| ( inverse(sk_c9) != multiply(sk_c9,sk_c10) ) ),
inference(instantiation,[status(thm)],[c_36718]) ).
tcf(c_45360,plain,
( ( multiply(sk_c7,sk_c10) = inverse(sk_c7) )
| ( inverse(sk_c7) != multiply(sk_c6,identity) )
| ( multiply(sk_c7,sk_c10) != multiply(sk_c6,identity) ) ),
inference(instantiation,[status(thm)],[c_40836]) ).
tcf(c_45471,plain,
( ( multiply(sk_c8,identity) = inverse(sk_c3) )
| ( inverse(sk_c3) != sk_c8 )
| ( multiply(sk_c8,identity) != sk_c8 ) ),
inference(instantiation,[status(thm)],[c_38161]) ).
tcf(c_45805,plain,
( ( sk_c10 = inverse(sk_c3) )
| ( sk_c10 != inverse(sk_c9) )
| ( inverse(sk_c3) != inverse(sk_c9) ) ),
inference(instantiation,[status(thm)],[c_36862]) ).
tcf(c_45820,plain,
( ( sk_c10 = inverse(sk_c3) )
| ( sk_c10 != multiply(sk_c9,sk_c10) )
| ( inverse(sk_c3) != multiply(sk_c9,sk_c10) ) ),
inference(instantiation,[status(thm)],[c_36862]) ).
tcf(c_46138,plain,
inverse(sk_c1) = inverse(sk_c1),
inference(instantiation,[status(thm)],[c_36811]) ).
tcf(c_46206,plain,
! [X0: $i] :
( ( multiply(sk_c9,sk_c10) = inverse(inverse(X0)) )
| ( multiply(sk_c9,sk_c10) != multiply(inverse(inverse(X0)),identity) )
| ( inverse(inverse(X0)) != multiply(inverse(inverse(X0)),identity) ) ),
inference(instantiation,[status(thm)],[c_37157]) ).
tcf(c_46208,plain,
( ( multiply(sk_c9,sk_c10) = inverse(inverse(sk_c10)) )
| ( inverse(inverse(sk_c10)) != multiply(inverse(inverse(sk_c10)),identity) )
| ( multiply(sk_c9,sk_c10) != multiply(inverse(inverse(sk_c10)),identity) ) ),
inference(instantiation,[status(thm)],[c_46206]) ).
tcf(c_46300,plain,
! [X0: $i] :
( ( X0 = sk_c8 )
| ( sk_c8 != inverse(sk_c3) )
| ( X0 != inverse(sk_c3) ) ),
inference(instantiation,[status(thm)],[c_42108]) ).
tcf(c_46301,plain,
( ( sk_c10 = sk_c8 )
| ( sk_c10 != inverse(sk_c3) )
| ( sk_c8 != inverse(sk_c3) ) ),
inference(instantiation,[status(thm)],[c_46300]) ).
tcf(c_46793,plain,
! [X0: $i] :
( ( sk_c9 = inverse(inverse(X0)) )
| ( sk_c9 != sk_c10 )
| ( inverse(inverse(X0)) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_38162]) ).
tcf(c_46795,plain,
( ( sk_c9 = inverse(inverse(sk_c10)) )
| ( sk_c9 != sk_c10 )
| ( inverse(inverse(sk_c10)) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_46793]) ).
tcf(c_46890,plain,
! [X0: $i] :
( ( multiply(sk_c9,sk_c10) = X0 )
| ( X0 != sk_c8 )
| ( multiply(sk_c9,sk_c10) != sk_c8 ) ),
inference(instantiation,[status(thm)],[c_38563]) ).
tcf(c_46891,plain,
( ( multiply(sk_c9,sk_c10) = sk_c10 )
| ( sk_c10 != sk_c8 )
| ( multiply(sk_c9,sk_c10) != sk_c8 ) ),
inference(instantiation,[status(thm)],[c_46890]) ).
tcf(c_46925,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(sk_c9,sk_c10) = X2 )
| ( X2 != multiply(X0,X1) )
| ( multiply(sk_c9,sk_c10) != multiply(X0,X1) ) ),
inference(instantiation,[status(thm)],[c_38563]) ).
tcf(c_46929,plain,
( ( multiply(sk_c9,sk_c10) = sk_c10 )
| ( sk_c10 != multiply(sk_c10,sk_c10) )
| ( multiply(sk_c9,sk_c10) != multiply(sk_c10,sk_c10) ) ),
inference(instantiation,[status(thm)],[c_46925]) ).
tcf(c_47077,plain,
! [X0: $i] :
( ( inverse(sk_c9) = X0 )
| ( X0 != inverse(sk_c3) )
| ( inverse(sk_c9) != inverse(sk_c3) ) ),
inference(instantiation,[status(thm)],[c_44406]) ).
tcf(c_48246,plain,
! [X0: $i] :
( ( multiply(sk_c9,sk_c10) = inverse(inverse(X0)) )
| ( multiply(sk_c9,sk_c10) != multiply(identity,inverse(inverse(X0))) )
| ( inverse(inverse(X0)) != multiply(identity,inverse(inverse(X0))) ) ),
inference(instantiation,[status(thm)],[c_37102]) ).
tcf(c_48248,plain,
! [X0: $i,X1: $i] :
( ( multiply(sk_c9,sk_c10) = X1 )
| ( X1 != inverse(inverse(X0)) )
| ( multiply(sk_c9,sk_c10) != inverse(inverse(X0)) ) ),
inference(instantiation,[status(thm)],[c_38563]) ).
tcf(c_48251,plain,
( ( multiply(sk_c9,sk_c10) = inverse(inverse(sk_c10)) )
| ( inverse(inverse(sk_c10)) != multiply(identity,inverse(inverse(sk_c10))) )
| ( multiply(sk_c9,sk_c10) != multiply(identity,inverse(inverse(sk_c10))) ) ),
inference(instantiation,[status(thm)],[c_48246]) ).
tcf(c_48253,plain,
( ( multiply(sk_c9,sk_c10) = sk_c10 )
| ( sk_c10 != inverse(inverse(sk_c10)) )
| ( multiply(sk_c9,sk_c10) != inverse(inverse(sk_c10)) ) ),
inference(instantiation,[status(thm)],[c_48248]) ).
tcf(c_50025,plain,
( ( inverse(sk_c5) = inverse(sk_c10) )
| ( inverse(sk_c5) != inverse(inverse(sk_c3)) )
| ( inverse(sk_c10) != inverse(inverse(sk_c3)) ) ),
inference(instantiation,[status(thm)],[c_40086]) ).
tcf(c_53138,plain,
! [X0: $i] :
( ( sk_c10 = multiply(sk_c9,sk_c10) )
| ( sk_c10 != X0 )
| ( multiply(sk_c9,sk_c10) != X0 ) ),
inference(instantiation,[status(thm)],[c_732]) ).
tcf(c_53139,plain,
( ( sk_c10 = multiply(sk_c9,sk_c10) )
| ( sk_c10 != sk_c10 )
| ( multiply(sk_c9,sk_c10) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_53138]) ).
tcf(c_54145,plain,
( ( inverse(sk_c9) = multiply(sk_c9,sk_c10) )
| ( inverse(sk_c9) != inverse(sk_c9) )
| ( multiply(sk_c9,sk_c10) != inverse(sk_c9) ) ),
inference(instantiation,[status(thm)],[c_44657]) ).
tcf(c_54243,plain,
( ( inverse(sk_c9) = inverse(sk_c3) )
| ( inverse(sk_c3) != multiply(sk_c9,sk_c10) )
| ( inverse(sk_c9) != multiply(sk_c9,sk_c10) ) ),
inference(instantiation,[status(thm)],[c_44664]) ).
tcf(c_54882,plain,
( ( inverse(sk_c9) = sk_c8 )
| ( sk_c8 != inverse(sk_c3) )
| ( inverse(sk_c9) != inverse(sk_c3) ) ),
inference(instantiation,[status(thm)],[c_47077]) ).
tcf(c_55563,plain,
! [X0: $i] :
( ( multiply(sk_c9,sk_c10) = multiply(identity,inverse(inverse(X0))) )
| ( sk_c9 != identity )
| ( sk_c10 != inverse(inverse(X0)) ) ),
inference(instantiation,[status(thm)],[c_38565]) ).
tcf(c_55564,plain,
( ( multiply(sk_c9,sk_c10) = multiply(identity,inverse(inverse(sk_c10))) )
| ( sk_c9 != identity )
| ( sk_c10 != inverse(inverse(sk_c10)) ) ),
inference(instantiation,[status(thm)],[c_55563]) ).
tcf(c_55663,plain,
! [X0: $i] :
( ( multiply(sk_c9,sk_c10) = multiply(inverse(inverse(X0)),identity) )
| ( sk_c9 != inverse(inverse(X0)) )
| ( sk_c10 != identity ) ),
inference(instantiation,[status(thm)],[c_38565]) ).
tcf(c_55665,plain,
( ( multiply(sk_c9,sk_c10) = multiply(inverse(inverse(sk_c10)),identity) )
| ( sk_c9 != inverse(inverse(sk_c10)) )
| ( sk_c10 != identity ) ),
inference(instantiation,[status(thm)],[c_55663]) ).
tcf(c_59294,plain,
inverse(sk_c1) = sk_c10,
inference(global_subsumption_just,[status(thm)],[c_8732,c_154,c_151,c_149,c_150,c_146,c_737,c_738,c_730,c_1061,c_1060,c_1078,c_1366,c_2140,c_2332,c_2351,c_2369,c_4311,c_5030,c_5154,c_5399,c_6522,c_6939,c_6946,c_8806,c_9323,c_22242,c_23398,c_31679,c_32191,c_32239,c_33271,c_34987,c_36692,c_36736,c_36765,c_36786,c_36787,c_36796,c_36797,c_36919,c_37049,c_37121,c_37155,c_37692,c_41571,c_42144,c_43373,c_43374,c_43521,c_45805,c_46138,c_46301,c_48251,c_48253,c_53139,c_55564]) ).
tcf(c_59304,plain,
inverse(sk_c3) = sk_c8,
inference(global_subsumption_just,[status(thm)],[c_8832,c_737,c_1061,c_1060,c_2140,c_5030,c_6946,c_8806,c_32191,c_33271,c_36692,c_36786,c_36787,c_36796,c_36797,c_37155,c_37692,c_48251,c_48253,c_53139,c_55564]) ).
tcf(c_59852,plain,
( ( multiply(sk_c10,sk_c2) = sk_c9 )
| ~ iPr_def_12 ),
inference(global_subsumption_just,[status(thm)],[c_11317,c_134,c_133,c_737,c_3792,c_36713,c_36736,c_36765]) ).
tcf(c_59861,plain,
( iPr_def_14
| iPr_def_10
| ( multiply(sk_c10,sk_c2) = sk_c9 )
| ( inverse(sk_c9) != sk_c8 )
| ( multiply(sk_c10,sk_c8) != sk_c9 )
| ( multiply(sk_c8,sk_c10) != sk_c9 ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_10866,c_59852]) ).
tcf(c_60387,plain,
! [X0: $i] :
( ( inverse(X0) = inverse(multiply(sk_c10,sk_c2)) )
| ( multiply(sk_c10,sk_c8) = sk_c9 )
| ( X0 != sk_c9 ) ),
inference(resolution,[status(thm)],[c_11607,c_130]) ).
tcf(c_60460,plain,
! [X0: $i] :
( ( inverse(sk_c9) = sk_c8 )
| ( inverse(X0) = inverse(sk_c9) )
| ( X0 != multiply(sk_c10,sk_c2) ) ),
inference(resolution,[status(thm)],[c_11607,c_4323]) ).
tcf(c_60467,plain,
( ( inverse(sk_c9) = sk_c8 )
| ( inverse(sk_c10) = inverse(sk_c9) )
| ( sk_c10 != multiply(sk_c10,sk_c2) ) ),
inference(instantiation,[status(thm)],[c_60460]) ).
tcf(c_62034,plain,
! [X0: $i] :
( ( sk_c10 = sk_c7 )
| ( multiply(sk_c8,multiply(sk_c3,X0)) = X0 ) ),
inference(light_normalisation,[status(thm)],[c_31158,c_113]) ).
tcf(c_62049,plain,
( ( sk_c10 = sk_c7 )
| ( multiply(sk_c8,identity) = inverse(sk_c3) ) ),
inference(superposition,[status(thm)],[c_30987,c_62034]) ).
tcf(c_62234,plain,
multiply(sk_c8,identity) = inverse(sk_c3),
inference(global_subsumption_just,[status(thm)],[c_62049,c_737,c_1061,c_1060,c_2140,c_5030,c_6946,c_8806,c_32191,c_33271,c_36692,c_36786,c_36787,c_36796,c_36797,c_37155,c_37692,c_42112,c_45471,c_48251,c_48253,c_53139,c_55564]) ).
tcf(c_62236,plain,
inverse(sk_c3) = sk_c8,
inference(demodulation,[status(thm)],[c_62234,c_4648]) ).
tcf(c_62301,plain,
multiply(sk_c3,sk_c8) = identity,
inference(superposition,[status(thm)],[c_62236,c_30987]) ).
tcf(c_62302,plain,
multiply(sk_c8,sk_c3) = identity,
inference(superposition,[status(thm)],[c_62236,c_114]) ).
tcf(c_62432,plain,
! [X0: $i] : multiply(sk_c8,multiply(sk_c3,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_62302,c_115]) ).
tcf(c_62442,plain,
! [X0: $i] : multiply(sk_c8,multiply(sk_c3,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_62432,c_113]) ).
tcf(c_62443,plain,
( ( multiply(sk_c10,sk_c8) = sk_c9 )
| ( multiply(sk_c8,sk_c10) = sk_c8 ) ),
inference(superposition,[status(thm)],[c_160,c_62442]) ).
tcf(c_62444,plain,
( ( multiply(sk_c9,sk_c10) = sk_c8 )
| ( multiply(sk_c8,sk_c10) = sk_c8 ) ),
inference(superposition,[status(thm)],[c_156,c_62442]) ).
tcf(c_62447,plain,
( ( inverse(sk_c5) = sk_c9 )
| ( multiply(sk_c8,sk_c10) = sk_c8 ) ),
inference(superposition,[status(thm)],[c_161,c_62442]) ).
tcf(c_62449,plain,
( ( inverse(sk_c4) = sk_c10 )
| ( multiply(sk_c8,sk_c10) = sk_c8 ) ),
inference(superposition,[status(thm)],[c_158,c_62442]) ).
tcf(c_62653,plain,
( ( sk_c8 = sk_c9 )
| ( inverse(sk_c5) = sk_c9 ) ),
inference(superposition,[status(thm)],[c_62447,c_121]) ).
tcf(c_62769,plain,
( ( sk_c8 = sk_c9 )
| ( inverse(sk_c4) = sk_c10 ) ),
inference(superposition,[status(thm)],[c_62449,c_118]) ).
tcf(c_62980,plain,
( ( sk_c8 = sk_c9 )
| ( multiply(sk_c10,sk_c8) = sk_c9 ) ),
inference(superposition,[status(thm)],[c_62443,c_120]) ).
tcf(c_63029,plain,
( ( sk_c8 = sk_c9 )
| ( multiply(sk_c9,sk_c10) = sk_c8 ) ),
inference(superposition,[status(thm)],[c_62444,c_116]) ).
tcf(c_63134,plain,
inverse(sk_c1) = sk_c10,
inference(global_subsumption_just,[status(thm)],[c_31848,c_59294]) ).
tcf(c_63195,plain,
( ( inverse(sk_c4) = sk_c10 )
| ~ iPr_def_14
| ( multiply(sk_c10,sk_c2) != sk_c9 ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_30979,c_63134]) ).
tcf(c_63210,plain,
inverse(sk_c10) = sk_c1,
inference(superposition,[status(thm)],[c_63134,c_31010]) ).
tcf(c_63211,plain,
multiply(sk_c1,sk_c10) = identity,
inference(superposition,[status(thm)],[c_63134,c_30987]) ).
tcf(c_63212,plain,
multiply(sk_c10,sk_c1) = identity,
inference(superposition,[status(thm)],[c_63134,c_114]) ).
tcf(c_63351,plain,
! [X0: $i] : multiply(sk_c10,multiply(sk_c1,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_63212,c_115]) ).
tcf(c_63358,plain,
! [X0: $i] : multiply(sk_c10,multiply(sk_c1,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_63351,c_113]) ).
tcf(c_63359,plain,
( ( multiply(sk_c10,sk_c2) = sk_c10 )
| ( multiply(sk_c10,sk_c8) = sk_c9 ) ),
inference(superposition,[status(thm)],[c_140,c_63358]) ).
tcf(c_63360,plain,
( ( multiply(sk_c9,sk_c10) = sk_c8 )
| ( multiply(sk_c10,sk_c2) = sk_c10 ) ),
inference(superposition,[status(thm)],[c_136,c_63358]) ).
tcf(c_63361,plain,
( ( inverse(sk_c6) = sk_c10 )
| ( multiply(sk_c10,sk_c2) = sk_c10 ) ),
inference(superposition,[status(thm)],[c_144,c_63358]) ).
tcf(c_63362,plain,
( ( inverse(sk_c7) = sk_c6 )
| ( multiply(sk_c10,sk_c2) = sk_c10 ) ),
inference(superposition,[status(thm)],[c_143,c_63358]) ).
tcf(c_63363,plain,
( ( inverse(sk_c5) = sk_c9 )
| ( multiply(sk_c10,sk_c2) = sk_c10 ) ),
inference(superposition,[status(thm)],[c_141,c_63358]) ).
tcf(c_63365,plain,
( ( inverse(sk_c4) = sk_c10 )
| ( multiply(sk_c10,sk_c2) = sk_c10 ) ),
inference(superposition,[status(thm)],[c_138,c_63358]) ).
tcf(c_63398,plain,
( ( sk_c10 = sk_c9 )
| ( inverse(sk_c6) = sk_c10 ) ),
inference(superposition,[status(thm)],[c_63361,c_134]) ).
tcf(c_63436,plain,
( ( sk_c10 = sk_c9 )
| ( inverse(sk_c7) = sk_c6 ) ),
inference(superposition,[status(thm)],[c_63362,c_133]) ).
tcf(c_63466,plain,
( ( sk_c10 = sk_c9 )
| ( inverse(sk_c5) = sk_c9 ) ),
inference(superposition,[status(thm)],[c_63363,c_131]) ).
tcf(c_63566,plain,
( ( sk_c10 = sk_c9 )
| ( inverse(sk_c4) = sk_c10 ) ),
inference(superposition,[status(thm)],[c_63365,c_128]) ).
tcf(c_63683,plain,
multiply(sk_c10,sk_c8) = sk_c9,
inference(global_subsumption_just,[status(thm)],[c_63359,c_120,c_737,c_1060,c_1106,c_1156,c_1366,c_1476,c_2074,c_2075,c_2351,c_4327,c_6765,c_8805,c_15669,c_20968,c_62980,c_63359]) ).
tcf(c_63692,plain,
( iPr_def_14
| iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( sk_c9 != sk_c9 )
| ( inverse(sk_c9) != sk_c8 )
| ( multiply(sk_c9,sk_c10) != sk_c8 )
| ( multiply(sk_c8,sk_c10) != sk_c9 ) ),
inference(demodulation,[status(thm)],[c_730,c_63683]) ).
tcf(c_63714,plain,
( iPr_def_14
| iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( inverse(sk_c9) != sk_c8 )
| ( multiply(sk_c9,sk_c10) != sk_c8 )
| ( multiply(sk_c8,sk_c10) != sk_c9 ) ),
inference(equality_resolution_simp,[status(thm)],[c_63692]) ).
tcf(c_63718,plain,
( ~ iPr_def_10
| ( sk_c10 != sk_c9 )
| ( inverse(sk_c10) != sk_c8 ) ),
inference(superposition,[status(thm)],[c_63683,c_725]) ).
tcf(c_63725,plain,
multiply(sk_c9,sk_c10) = sk_c8,
inference(global_subsumption_just,[status(thm)],[c_63360,c_126,c_737,c_1060,c_1107,c_1155,c_1476,c_2140,c_7979,c_26456,c_26455,c_36692,c_36786,c_36787,c_36796,c_36797,c_37155,c_37156,c_37692,c_46208,c_46795,c_48251,c_48253,c_55564,c_55665,c_63029,c_63360]) ).
tcf(c_63755,plain,
( ~ iPr_def_10
| ( sk_c10 != sk_c9 ) ),
inference(global_subsumption_just,[status(thm)],[c_63718,c_4310,c_15280,c_36919,c_41571]) ).
tcf(c_64128,plain,
( ~ iPr_def_12
| ( sk_c10 != sk_c9 )
| ( inverse(sk_c9) != sk_c8 ) ),
inference(superposition,[status(thm)],[c_63725,c_31011]) ).
tcf(c_67078,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = multiply(sk_c10,X0) )
| ( X2 != X1 )
| ( multiply(sk_c10,X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_732]) ).
tcf(c_67079,plain,
( ( sk_c10 = multiply(sk_c10,sk_c10) )
| ( sk_c10 != sk_c10 )
| ( multiply(sk_c10,sk_c10) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_67078]) ).
tcf(c_72206,plain,
( ~ iPr_def_12
| ( inverse(inverse(sk_c7)) != sk_c10 )
| ( multiply(sk_c7,sk_c10) != inverse(sk_c7) ) ),
inference(instantiation,[status(thm)],[c_727]) ).
tcf(c_74726,plain,
multiply(sk_c10,sk_c8) = sk_c9,
inference(global_subsumption_just,[status(thm)],[c_60387,c_120,c_737,c_1060,c_1106,c_1156,c_1366,c_1476,c_2074,c_2075,c_2351,c_4327,c_6765,c_8805,c_15669,c_20968,c_62980,c_63359]) ).
tcf(c_75193,plain,
( iPr_def_14
| iPr_def_10
| ( multiply(sk_c10,sk_c2) = sk_c9 )
| ( inverse(sk_c9) != sk_c8 )
| ( multiply(sk_c8,sk_c10) != sk_c9 ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_59861,c_74726]) ).
tcf(c_76353,plain,
! [X0: $i] :
( ( sk_c2 = identity )
| ( multiply(sk_c7,multiply(sk_c10,X0)) = multiply(sk_c6,X0) ) ),
inference(light_normalisation,[status(thm)],[c_1647,c_63211]) ).
tcf(c_76412,plain,
( ( sk_c2 = identity )
| ( multiply(sk_c7,sk_c10) = multiply(sk_c6,identity) ) ),
inference(superposition,[status(thm)],[c_4648,c_76353]) ).
tcf(c_77551,plain,
! [X0: $i] :
( ( sk_c10 = identity )
| ( multiply(sk_c7,multiply(sk_c10,X0)) = multiply(sk_c6,X0) ) ),
inference(light_normalisation,[status(thm)],[c_1692,c_62301]) ).
tcf(c_77610,plain,
( ( sk_c10 = identity )
| ( multiply(sk_c7,sk_c10) = multiply(sk_c6,identity) ) ),
inference(superposition,[status(thm)],[c_4648,c_77551]) ).
tcf(c_89852,negated_conjecture,
inverse(sk_c1) = sk_c10,
inference(global_subsumption_just,[status(thm)],[c_148,c_154,c_151,c_149,c_150,c_146,c_737,c_738,c_730,c_1061,c_1060,c_1078,c_1366,c_2140,c_2332,c_2351,c_2369,c_4311,c_5030,c_5154,c_5399,c_6522,c_6939,c_6946,c_8806,c_9323,c_22242,c_23398,c_31679,c_32191,c_32239,c_33271,c_34987,c_36692,c_36736,c_36765,c_36786,c_36787,c_36796,c_36797,c_36919,c_37049,c_37121,c_37155,c_37692,c_41571,c_42144,c_43373,c_43374,c_43521,c_45805,c_46138,c_46301,c_48251,c_48253,c_53139,c_55564]) ).
tcf(c_89854,negated_conjecture,
inverse(sk_c3) = sk_c8,
inference(global_subsumption_just,[status(thm)],[c_168,c_59304]) ).
tcf(c_89861,plain,
( ( multiply(sk_c9,sk_c10) = sk_c8 )
| ~ iPr_def_10 ),
inference(backward_subsumption_resolution,[status(thm)],[c_1713,c_89854]) ).
tcf(c_89862,plain,
( ( multiply(sk_c10,sk_c8) = sk_c9 )
| ~ iPr_def_10 ),
inference(backward_subsumption_resolution,[status(thm)],[c_1712,c_89854]) ).
tcf(c_89863,plain,
multiply(sk_c10,sk_c1) = identity,
inference(superposition,[status(thm)],[c_89852,c_114]) ).
tcf(c_89864,plain,
multiply(sk_c8,sk_c3) = identity,
inference(superposition,[status(thm)],[c_89854,c_114]) ).
tcf(c_89865,plain,
multiply(sk_c1,sk_c10) = identity,
inference(superposition,[status(thm)],[c_63210,c_114]) ).
tcf(c_89934,plain,
multiply(sk_c9,sk_c10) = sk_c8,
inference(global_subsumption_just,[status(thm)],[c_89861,c_63725]) ).
tcf(c_89936,plain,
( iPr_def_14
| iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( inverse(sk_c9) != sk_c8 )
| ( multiply(sk_c10,sk_c8) != sk_c9 )
| ( multiply(sk_c8,sk_c10) != sk_c9 ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_730,c_89934]) ).
tcf(c_89937,plain,
multiply(sk_c10,sk_c8) = sk_c9,
inference(global_subsumption_just,[status(thm)],[c_89862,c_63683]) ).
tcf(c_89939,plain,
( iPr_def_14
| iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( inverse(sk_c9) != sk_c8 )
| ( multiply(sk_c8,sk_c10) != sk_c9 ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_89936,c_89937]) ).
tcf(c_89940,plain,
( iPr_def_14
| iPr_def_13
| ( multiply(sk_c8,sk_c10) != sk_c9 )
| ( inverse(sk_c9) != sk_c8 )
| iPr_def_10
| iPr_def_11 ),
inference(global_subsumption_just,[status(thm)],[c_89939,c_737,c_1060,c_1107,c_1156,c_2455,c_2456,c_19277,c_20116,c_36713,c_36736,c_36765,c_38883,c_38884,c_45360,c_63398,c_63436,c_63714,c_63725,c_64128,c_67079,c_72206,c_75193,c_76412,c_77610]) ).
tcf(c_89941,plain,
( iPr_def_14
| iPr_def_13
| iPr_def_11
| iPr_def_10
| ( inverse(sk_c9) != sk_c8 )
| ( multiply(sk_c8,sk_c10) != sk_c9 ) ),
inference(renaming,[status(thm)],[c_89940]) ).
tcf(c_89952,plain,
( iPr_def_14
| iPr_def_13
| iPr_def_11
| iPr_def_10
| ( inverse(sk_c4) = sk_c10 )
| ( inverse(sk_c9) != sk_c8 ) ),
inference(superposition,[status(thm)],[c_118,c_89941]) ).
tcf(c_89965,plain,
! [X0: $i] : multiply(sk_c9,multiply(sk_c10,X0)) = multiply(sk_c8,X0),
inference(superposition,[status(thm)],[c_89934,c_115]) ).
tcf(c_89967,plain,
! [X0: $i] : multiply(sk_c10,multiply(sk_c8,X0)) = multiply(sk_c9,X0),
inference(superposition,[status(thm)],[c_89937,c_115]) ).
tcf(c_90012,plain,
( ( sk_c2 = identity )
| ( multiply(sk_c5,sk_c8) = sk_c9 ) ),
inference(light_normalisation,[status(thm)],[c_142,c_89865]) ).
tcf(c_90087,plain,
( ( multiply(sk_c3,sk_c8) = sk_c10 )
| ~ iPr_def_13
| ( inverse(sk_c5) != sk_c9 ) ),
inference(superposition,[status(thm)],[c_162,c_728]) ).
tcf(c_90088,plain,
( ( sk_c2 = identity )
| ~ iPr_def_13
| ( inverse(sk_c5) != sk_c9 ) ),
inference(superposition,[status(thm)],[c_90012,c_728]) ).
tcf(c_90128,plain,
( ~ iPr_def_14
| ( inverse(sk_c9) != sk_c10 )
| ( multiply(sk_c10,sk_c8) != sk_c9 ) ),
inference(superposition,[status(thm)],[c_89934,c_729]) ).
tcf(c_90142,plain,
( ~ iPr_def_14
| ( inverse(sk_c9) != sk_c10 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_90128,c_89937]) ).
tcf(c_90144,plain,
! [X0: $i] : multiply(sk_c8,multiply(sk_c3,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_89864,c_115]) ).
tcf(c_90194,plain,
multiply(sk_c8,sk_c1) = multiply(sk_c9,identity),
inference(superposition,[status(thm)],[c_89863,c_89965]) ).
tcf(c_90209,plain,
multiply(sk_c10,sk_c8) = multiply(sk_c9,identity),
inference(superposition,[status(thm)],[c_4648,c_89967]) ).
tcf(c_90219,plain,
multiply(sk_c8,sk_c1) = sk_c9,
inference(light_normalisation,[status(thm)],[c_90194,c_89937,c_90209]) ).
tcf(c_90281,plain,
! [X0: $i] : multiply(sk_c8,multiply(sk_c3,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_90144,c_113]) ).
tcf(c_90284,plain,
( ( inverse(sk_c5) = sk_c9 )
| ( multiply(sk_c8,sk_c10) = sk_c8 ) ),
inference(superposition,[status(thm)],[c_161,c_90281]) ).
tcf(c_90286,plain,
( ( inverse(sk_c4) = sk_c10 )
| ( multiply(sk_c8,sk_c10) = sk_c8 ) ),
inference(superposition,[status(thm)],[c_158,c_90281]) ).
tcf(c_90300,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(X0,X1)) = X1,
inference(demodulation,[status(thm)],[c_1330,c_113]) ).
tcf(c_90313,plain,
( ( inverse(sk_c9) = sk_c8 )
| ( multiply(inverse(sk_c8),sk_c9) = sk_c10 ) ),
inference(superposition,[status(thm)],[c_119,c_90300]) ).
tcf(c_90316,plain,
( ( multiply(sk_c3,sk_c8) = sk_c10 )
| ( multiply(inverse(sk_c4),sk_c9) = sk_c10 ) ),
inference(superposition,[status(thm)],[c_157,c_90300]) ).
tcf(c_90321,plain,
( ( multiply(sk_c3,sk_c8) = sk_c10 )
| ( multiply(inverse(sk_c5),sk_c9) = sk_c8 ) ),
inference(superposition,[status(thm)],[c_162,c_90300]) ).
tcf(c_90322,plain,
( ( sk_c2 = identity )
| ( multiply(inverse(sk_c5),sk_c9) = sk_c8 ) ),
inference(superposition,[status(thm)],[c_90012,c_90300]) ).
tcf(c_90341,plain,
! [X0: $i] : multiply(inverse(inverse(X0)),identity) = X0,
inference(superposition,[status(thm)],[c_114,c_90300]) ).
tcf(c_90354,plain,
! [X0: $i] : multiply(inverse(sk_c8),X0) = multiply(sk_c3,X0),
inference(superposition,[status(thm)],[c_90281,c_90300]) ).
tcf(c_90356,plain,
( ( inverse(sk_c9) = sk_c8 )
| ( multiply(inverse(sk_c8),multiply(sk_c9,sk_c2)) = sk_c9 ) ),
inference(superposition,[status(thm)],[c_2930,c_90300]) ).
tcf(c_90362,plain,
multiply(inverse(sk_c8),sk_c9) = sk_c1,
inference(superposition,[status(thm)],[c_90219,c_90300]) ).
tcf(c_90375,plain,
( ( sk_c10 = sk_c1 )
| ( inverse(sk_c9) = sk_c8 ) ),
inference(light_normalisation,[status(thm)],[c_90313,c_90362]) ).
tcf(c_90379,plain,
( ( inverse(sk_c9) = sk_c8 )
| ( multiply(sk_c3,multiply(sk_c9,sk_c2)) = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_90356,c_90354]) ).
tcf(c_90583,plain,
inverse(sk_c9) = sk_c8,
inference(global_subsumption_just,[status(thm)],[c_90379,c_126,c_737,c_1061,c_1060,c_1107,c_1155,c_1476,c_2140,c_2351,c_5030,c_6418,c_6946,c_7979,c_8756,c_8806,c_8805,c_10250,c_26456,c_26455,c_32191,c_33271,c_36692,c_36786,c_36787,c_36796,c_36797,c_37112,c_37155,c_37156,c_37692,c_40385,c_40384,c_41237,c_42143,c_43375,c_43521,c_46208,c_46795,c_46891,c_48251,c_48253,c_53139,c_54145,c_54243,c_54882,c_55564,c_55665,c_60467,c_63029,c_63210,c_63360,c_90375]) ).
tcf(c_90587,plain,
( ~ iPr_def_14
| ( sk_c8 != sk_c10 ) ),
inference(demodulation,[status(thm)],[c_90142,c_90583]) ).
tcf(c_90590,plain,
( iPr_def_14
| iPr_def_13
| iPr_def_11
| iPr_def_10
| ( sk_c8 != sk_c8 )
| ( multiply(sk_c8,sk_c10) != sk_c9 ) ),
inference(demodulation,[status(thm)],[c_89941,c_90583]) ).
tcf(c_90595,plain,
( iPr_def_14
| iPr_def_13
| iPr_def_11
| iPr_def_10
| ( inverse(sk_c4) = sk_c10 ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_89952,c_90583]) ).
tcf(c_90601,plain,
( iPr_def_14
| iPr_def_13
| iPr_def_11
| iPr_def_10
| ( multiply(sk_c8,sk_c10) != sk_c9 ) ),
inference(equality_resolution_simp,[status(thm)],[c_90590]) ).
tcf(c_90603,plain,
multiply(sk_c8,sk_c9) = identity,
inference(superposition,[status(thm)],[c_90583,c_114]) ).
tcf(c_90631,plain,
inverse(sk_c5) = sk_c9,
inference(global_subsumption_just,[status(thm)],[c_90284,c_154,c_151,c_149,c_150,c_146,c_131,c_121,c_126,c_737,c_738,c_730,c_1061,c_1060,c_1078,c_1107,c_1155,c_1156,c_1366,c_1476,c_1716,c_2140,c_2332,c_2351,c_2369,c_2455,c_2456,c_3837,c_4311,c_5030,c_5154,c_5399,c_6418,c_6522,c_6939,c_6946,c_7979,c_8756,c_8781,c_8806,c_8805,c_9323,c_10250,c_19277,c_20116,c_21072,c_21259,c_22242,c_23398,c_26456,c_26455,c_31679,c_32191,c_32239,c_33271,c_34987,c_36692,c_36713,c_36736,c_36765,c_36786,c_36787,c_36796,c_36797,c_36919,c_37049,c_37112,c_37121,c_37155,c_37156,c_37692,c_38883,c_38884,c_40385,c_40384,c_41237,c_41571,c_42143,c_42144,c_43373,c_43374,c_43375,c_43521,c_45360,c_45805,c_46138,c_46208,c_46301,c_46795,c_46891,c_48251,c_48253,c_53139,c_54145,c_54243,c_54882,c_55564,c_55665,c_60467,c_62653,c_63029,c_63210,c_63360,c_63398,c_63436,c_63466,c_63714,c_64128,c_67079,c_72206,c_75193,c_76412,c_77610,c_90375]) ).
tcf(c_90639,plain,
( ( multiply(sk_c3,sk_c8) = sk_c10 )
| ~ iPr_def_13 ),
inference(backward_subsumption_resolution,[status(thm)],[c_90087,c_90631]) ).
tcf(c_90645,plain,
inverse(sk_c4) = sk_c10,
inference(global_subsumption_just,[status(thm)],[c_90286,c_128,c_737,c_1061,c_1060,c_1718,c_2140,c_5030,c_6946,c_8781,c_8806,c_20998,c_21170,c_32191,c_33271,c_36692,c_36786,c_36787,c_36796,c_36797,c_37155,c_37692,c_48251,c_48253,c_53139,c_55564,c_62769,c_63195,c_63566,c_90595]) ).
tcf(c_90667,plain,
multiply(sk_c10,identity) = multiply(sk_c9,sk_c9),
inference(superposition,[status(thm)],[c_90603,c_89967]) ).
tcf(c_90721,plain,
! [X0: $i] : inverse(inverse(X0)) = X0,
inference(demodulation,[status(thm)],[c_90341,c_4648]) ).
tcf(c_90726,plain,
inverse(sk_c8) = sk_c9,
inference(superposition,[status(thm)],[c_90583,c_90721]) ).
tcf(c_90731,plain,
inverse(sk_c8) = sk_c3,
inference(superposition,[status(thm)],[c_89854,c_90721]) ).
tcf(c_90738,plain,
! [X0: $i] : multiply(sk_c3,multiply(sk_c8,X0)) = X0,
inference(superposition,[status(thm)],[c_90731,c_90300]) ).
tcf(c_90739,plain,
multiply(sk_c3,sk_c8) = identity,
inference(superposition,[status(thm)],[c_90731,c_114]) ).
tcf(c_90740,plain,
( ( sk_c10 = identity )
| ~ iPr_def_13 ),
inference(demodulation,[status(thm)],[c_90639,c_90739]) ).
tcf(c_90742,plain,
( ( sk_c10 = identity )
| ( multiply(sk_c5,sk_c8) = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_162,c_90739]) ).
tcf(c_90746,plain,
! [X0: $i] : multiply(sk_c3,multiply(sk_c8,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_90739,c_115]) ).
tcf(c_90755,plain,
multiply(sk_c3,identity) = sk_c3,
inference(superposition,[status(thm)],[c_89864,c_90738]) ).
tcf(c_90756,plain,
multiply(sk_c3,identity) = sk_c9,
inference(superposition,[status(thm)],[c_90603,c_90738]) ).
tcf(c_90766,plain,
sk_c9 = sk_c3,
inference(light_normalisation,[status(thm)],[c_90755,c_90756]) ).
tcf(c_90800,plain,
( ( sk_c10 = identity )
| ( multiply(inverse(sk_c5),sk_c9) = sk_c8 ) ),
inference(superposition,[status(thm)],[c_90742,c_90300]) ).
tcf(c_90823,plain,
~ iPr_def_13,
inference(global_subsumption_just,[status(thm)],[c_90740,c_126,c_120,c_736,c_737,c_741,c_1061,c_1060,c_1067,c_1106,c_1107,c_1155,c_1156,c_1366,c_1412,c_1476,c_2074,c_2075,c_2140,c_2351,c_2455,c_2456,c_4327,c_5030,c_6765,c_6946,c_7979,c_8806,c_8805,c_10868,c_15669,c_19277,c_20116,c_20968,c_26357,c_26456,c_26455,c_32191,c_33271,c_36692,c_36716,c_36786,c_36787,c_36796,c_36797,c_36979,c_37071,c_37155,c_37156,c_37692,c_39831,c_42143,c_42650,c_45820,c_46208,c_46795,c_46929,c_48251,c_48253,c_50025,c_53139,c_55564,c_55665,c_62980,c_63029,c_63360,c_63359,c_67079,c_90088,c_90631,c_90726,c_90740]) ).
tcf(c_90825,plain,
( iPr_def_14
| iPr_def_11
| iPr_def_10
| ( multiply(sk_c8,sk_c10) != sk_c9 ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_90601,c_90823]) ).
tcf(c_90879,plain,
( ( sk_c10 = identity )
| ( multiply(sk_c10,sk_c9) = sk_c10 ) ),
inference(light_normalisation,[status(thm)],[c_90316,c_90739,c_90645]) ).
tcf(c_91060,plain,
multiply(inverse(sk_c5),sk_c9) = sk_c8,
inference(global_subsumption_just,[status(thm)],[c_90321,c_737,c_1060,c_1107,c_1156,c_2455,c_2456,c_2813,c_2980,c_6439,c_6522,c_19277,c_20116,c_31513,c_67079,c_90322,c_90800,c_90825]) ).
tcf(c_91062,plain,
multiply(sk_c10,identity) = sk_c8,
inference(light_normalisation,[status(thm)],[c_91060,c_90631,c_90667]) ).
tcf(c_91063,plain,
sk_c8 = sk_c10,
inference(demodulation,[status(thm)],[c_91062,c_4648]) ).
tcf(c_91078,plain,
! [X0: $i] : multiply(sk_c9,multiply(sk_c10,X0)) = multiply(sk_c10,X0),
inference(demodulation,[status(thm)],[c_89965,c_91063]) ).
tcf(c_91082,plain,
( ( multiply(sk_c5,sk_c10) = sk_c9 )
| ( multiply(sk_c10,sk_c2) = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_132,c_91063]) ).
tcf(c_91088,plain,
inverse(sk_c3) = sk_c10,
inference(demodulation,[status(thm)],[c_89854,c_91063]) ).
tcf(c_91089,plain,
~ iPr_def_14,
inference(backward_subsumption_resolution,[status(thm)],[c_90587,c_91063]) ).
tcf(c_91096,plain,
( iPr_def_11
| iPr_def_10
| ( multiply(sk_c8,sk_c10) != sk_c9 ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_90825,c_91089]) ).
tcf(c_91104,plain,
multiply(sk_c5,sk_c10) = sk_c9,
inference(global_subsumption_just,[status(thm)],[c_91082,c_154,c_151,c_149,c_150,c_146,c_131,c_121,c_126,c_120,c_736,c_737,c_738,c_741,c_730,c_1061,c_1060,c_1066,c_1067,c_1068,c_1078,c_1106,c_1107,c_1155,c_1156,c_1366,c_1401,c_1402,c_1412,c_1476,c_1716,c_2074,c_2075,c_2140,c_2221,c_2332,c_2351,c_2369,c_2415,c_2414,c_2455,c_2456,c_3837,c_4311,c_4327,c_5030,c_5154,c_5399,c_6418,c_6439,c_6522,c_6765,c_6939,c_6946,c_7979,c_8756,c_8781,c_8806,c_8805,c_9323,c_10250,c_10868,c_15669,c_19277,c_20116,c_20968,c_21072,c_21247,c_21259,c_22242,c_22345,c_22773,c_23398,c_26357,c_26456,c_26455,c_31513,c_31679,c_32191,c_32239,c_33271,c_34987,c_36692,c_36713,c_36716,c_36736,c_36765,c_36786,c_36787,c_36796,c_36797,c_36865,c_36919,c_36979,c_37049,c_37071,c_37112,c_37121,c_37155,c_37156,c_37692,c_38883,c_38884,c_39831,c_40385,c_40384,c_41237,c_41571,c_42143,c_42144,c_42650,c_43373,c_43374,c_43375,c_43521,c_45360,c_45805,c_45820,c_46138,c_46208,c_46301,c_46795,c_46891,c_46929,c_48251,c_48253,c_50025,c_53139,c_54145,c_54243,c_54882,c_55564,c_55665,c_60467,c_62653,c_62980,c_63029,c_63210,c_63360,c_63359,c_63398,c_63436,c_63466,c_63714,c_64128,c_67079,c_72206,c_75193,c_76412,c_77610,c_90088,c_90375,c_90726,c_90740,c_90742,c_91089,c_91088]) ).
tcf(c_91106,plain,
( ~ iPr_def_11
| ( inverse(sk_c5) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_91104,c_726]) ).
tcf(c_91115,plain,
inverse(sk_c5) != sk_c10,
inference(global_subsumption_just,[status(thm)],[c_91106,c_154,c_151,c_149,c_150,c_146,c_131,c_121,c_126,c_120,c_737,c_738,c_730,c_1061,c_1060,c_1066,c_1067,c_1078,c_1093,c_1106,c_1107,c_1155,c_1156,c_1366,c_1401,c_1402,c_1409,c_1476,c_1716,c_2074,c_2075,c_2140,c_2221,c_2332,c_2351,c_2369,c_2455,c_2456,c_3837,c_4311,c_4327,c_5030,c_5154,c_5399,c_6418,c_6522,c_6765,c_6939,c_6946,c_7979,c_8756,c_8781,c_8806,c_8805,c_9323,c_10250,c_15669,c_19277,c_20116,c_20968,c_21072,c_21259,c_22242,c_22345,c_23398,c_26456,c_26455,c_31679,c_32191,c_32239,c_33271,c_34987,c_36692,c_36713,c_36736,c_36765,c_36786,c_36787,c_36796,c_36797,c_36865,c_36919,c_37049,c_37112,c_37121,c_37155,c_37156,c_37692,c_38883,c_38884,c_40385,c_40384,c_41237,c_41571,c_42143,c_42144,c_43373,c_43374,c_43375,c_43521,c_45360,c_45805,c_46138,c_46208,c_46301,c_46795,c_46891,c_48251,c_48253,c_53139,c_54145,c_54243,c_54882,c_55564,c_55665,c_60467,c_62653,c_62980,c_63029,c_63210,c_63360,c_63359,c_63398,c_63436,c_63466,c_63714,c_63755,c_64128,c_67079,c_72206,c_75193,c_76412,c_77610,c_90375,c_91088,c_91096,c_91106]) ).
tcf(c_91117,plain,
sk_c10 != sk_c9,
inference(light_normalisation,[status(thm)],[c_91115,c_90631]) ).
tcf(c_91140,plain,
! [X0: $i] : multiply(sk_c10,X0) = X0,
inference(light_normalisation,[status(thm)],[c_90746,c_113,c_90766,c_91063,c_91078]) ).
tcf(c_91141,plain,
( ( sk_c10 = identity )
| ( sk_c10 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_90879,c_91140]) ).
tcf(c_91145,plain,
sk_c1 = identity,
inference(demodulation,[status(thm)],[c_89863,c_91140]) ).
tcf(c_91152,plain,
( ( sk_c10 = sk_c1 )
| ( sk_c10 = sk_c9 ) ),
inference(light_normalisation,[status(thm)],[c_91141,c_91145]) ).
tcf(c_91153,plain,
sk_c10 = sk_c1,
inference(forward_subsumption_resolution,[status(thm)],[c_91152,c_91117]) ).
tcf(c_91155,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_91153,c_91115,c_91088,c_90726,c_90631,c_63210,c_59304,c_50025,c_42650,c_37761,c_37110,c_37071,c_36979,c_36865,c_36716,c_737]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GRP366-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.08/0.34 % Computer : n011.cluster.edu
% 0.08/0.34 % Model : x86_64 x86_64
% 0.08/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.34 % Memory : 8046.5625MB
% 0.08/0.34 % OS : Linux 6.8.0-71-generic
% 0.09/15.61 % CPULimit : 300
% 0.09/15.61 % WCLimit : 300
% 0.09/15.61 % DateTime : Wed Sep 23 14:36:13 UTC 2026
% 0.09/15.61 % CPUTime :
% 0.09/15.61 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.09/15.65 Running first-order theorem proving
% 0.09/15.65 Running: /export/starexec/sandbox/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/15.66
% 0.09/15.66 % ======== iProver multi-core TPTP/SMT =========
% 0.09/15.66
% 0.09/15.66 % Detected problem language: tptp
% 0.09/15.67 % Proving...
% 39.01/25.69 % SZS status Started for theBenchmark.p
% 39.01/25.69 % SZS status Unsatisfiable for theBenchmark.p
% 39.01/25.69
% 39.01/25.69 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 39.01/25.69
% 39.01/25.69 % ------ iProver source info
% 39.01/25.69
% 39.01/25.69 % git: date: 2026-07-19 20:42:38 +0200
% 39.01/25.69 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 39.01/25.69 % git: non_committed_changes: false
% 39.01/25.69
% 39.01/25.69 % ------ Parsing...% successful
% 39.01/25.69
% 39.01/25.69
% 39.01/25.69 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 39.01/25.69
% 39.01/25.69 % ------ Preprocessing... sup_sim: 0 sf_s rm: 0 0s sf_e pe_s pe_e %
% 39.01/25.69
% 39.01/25.69 % ------ Preprocessing... gs_s sp: 5 0s gs_e snvd_s sp: 0 0s snvd_e %
% 39.01/25.69
% 39.01/25.69 % ------ Preprocessing... sf_s rm: 0 0s sf_e
% 39.01/25.69 % ------ Proving...
% 39.01/25.69 % ------ Problem Properties
% 39.01/25.69
% 39.01/25.69 %
% 39.01/25.69 % clauses 69
% 39.01/25.69 % conjectures 66
% 39.01/25.69 % EPR 0
% 39.01/25.69 % Horn 8
% 39.01/25.69 % unary 3
% 39.01/25.69 % binary 60
% 39.01/25.69 % lits 147
% 39.01/25.69 % lits eq 137
% 39.01/25.69 % fd_pure 0
% 39.01/25.69 % fd_pseudo 0
% 39.01/25.69 % fd_cond 0
% 39.01/25.69 % fd_pseudo_cond 0
% 39.01/25.69 % AC symbols 0
% 39.01/25.69
% 39.01/25.69 % ------ Input Options Time Limit: Unbounded
% 39.01/25.69
% 39.01/25.69
% 39.01/25.69 % ------
% 39.01/25.69 % Current options:
% 39.01/25.69 % ------
% 39.01/25.69
% 39.01/25.69
% 39.01/25.69 %
% 39.01/25.69
% 39.01/25.69 % ------ Proving...
% 39.01/25.69 %
% 39.01/25.69
% 39.01/25.69 % SZS status Unsatisfiable for theBenchmark.p
% 39.01/25.69
% 39.01/25.69 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 39.01/25.70
% 39.01/25.70
%------------------------------------------------------------------------------