%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : GRP307-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 : n002.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:32:47 PM UTC 2026
% Result : Unsatisfiable 73.90s 10.91s
% Output : CNFRefutation 73.90s
% Verified :
% SZS Type : Refutation
% Derivation depth : 46
% Number of leaves : 46
% Syntax : Number of formulae : 844 ( 102 unt; 0 def)
% Number of atoms : 2237 (2058 equ)
% Maximal formula atoms : 16 ( 2 avg)
% Number of connectives : 2448 (1055 ~;1393 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 25 ( 4 avg)
% Maximal term depth : 7 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 6 ( 4 usr; 5 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 12 con; 0-2 aty)
% Number of variables : 567 ( 0 sgn 567 !; 0 ?; 527 :)
% 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_c3,sk_c11) = sk_c10
| multiply(sk_c11,sk_c10) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_1) ).
fof(f6,plain,
( sk_c10 = multiply(sk_c3,sk_c11)
| multiply(sk_c11,sk_c10) = sk_c9 ),
inference(reorient_equations,[],[f5]) ).
fof(f7,negated_conjecture,
( inverse(sk_c3) = sk_c11
| multiply(sk_c11,sk_c10) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_2) ).
fof(f8,plain,
( sk_c11 = inverse(sk_c3)
| multiply(sk_c11,sk_c10) = sk_c9 ),
inference(reorient_equations,[],[f7]) ).
fof(f9,negated_conjecture,
( multiply(sk_c4,sk_c10) = sk_c9
| multiply(sk_c11,sk_c10) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_3) ).
fof(f10,plain,
( sk_c9 = multiply(sk_c4,sk_c10)
| multiply(sk_c11,sk_c10) = sk_c9 ),
inference(reorient_equations,[],[f9]) ).
fof(f11,negated_conjecture,
( inverse(sk_c4) = sk_c10
| multiply(sk_c11,sk_c10) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_4) ).
fof(f12,plain,
( sk_c10 = inverse(sk_c4)
| multiply(sk_c11,sk_c10) = sk_c9 ),
inference(reorient_equations,[],[f11]) ).
fof(f13,negated_conjecture,
( multiply(sk_c5,sk_c8) = sk_c11
| multiply(sk_c11,sk_c10) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_5) ).
fof(f14,plain,
( sk_c11 = multiply(sk_c5,sk_c8)
| multiply(sk_c11,sk_c10) = sk_c9 ),
inference(reorient_equations,[],[f13]) ).
fof(f15,negated_conjecture,
( inverse(sk_c5) = sk_c8
| multiply(sk_c11,sk_c10) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_6) ).
fof(f16,plain,
( sk_c8 = inverse(sk_c5)
| multiply(sk_c11,sk_c10) = sk_c9 ),
inference(reorient_equations,[],[f15]) ).
fof(f24,negated_conjecture,
( multiply(sk_c3,sk_c11) = sk_c10
| inverse(sk_c11) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_11) ).
fof(f25,plain,
( sk_c10 = multiply(sk_c3,sk_c11)
| sk_c9 = inverse(sk_c11) ),
inference(reorient_equations,[],[f24]) ).
fof(f26,negated_conjecture,
( inverse(sk_c3) = sk_c11
| inverse(sk_c11) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_12) ).
fof(f27,plain,
( sk_c11 = inverse(sk_c3)
| sk_c9 = inverse(sk_c11) ),
inference(reorient_equations,[],[f26]) ).
fof(f28,negated_conjecture,
( multiply(sk_c4,sk_c10) = sk_c9
| inverse(sk_c11) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_13) ).
fof(f29,plain,
( sk_c9 = multiply(sk_c4,sk_c10)
| sk_c9 = inverse(sk_c11) ),
inference(reorient_equations,[],[f28]) ).
fof(f30,negated_conjecture,
( inverse(sk_c4) = sk_c10
| inverse(sk_c11) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_14) ).
fof(f31,plain,
( sk_c10 = inverse(sk_c4)
| sk_c9 = inverse(sk_c11) ),
inference(reorient_equations,[],[f30]) ).
fof(f32,negated_conjecture,
( multiply(sk_c5,sk_c8) = sk_c11
| inverse(sk_c11) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_15) ).
fof(f33,plain,
( sk_c11 = multiply(sk_c5,sk_c8)
| sk_c9 = inverse(sk_c11) ),
inference(reorient_equations,[],[f32]) ).
fof(f34,negated_conjecture,
( inverse(sk_c5) = sk_c8
| inverse(sk_c11) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_16) ).
fof(f35,plain,
( sk_c8 = inverse(sk_c5)
| sk_c9 = inverse(sk_c11) ),
inference(reorient_equations,[],[f34]) ).
fof(f44,negated_conjecture,
( multiply(sk_c3,sk_c11) = sk_c10
| multiply(sk_c9,sk_c10) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_21) ).
fof(f45,plain,
( sk_c10 = multiply(sk_c3,sk_c11)
| sk_c11 = multiply(sk_c9,sk_c10) ),
inference(reorient_equations,[],[f44]) ).
fof(f46,negated_conjecture,
( inverse(sk_c3) = sk_c11
| multiply(sk_c9,sk_c10) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_22) ).
fof(f47,plain,
( sk_c11 = inverse(sk_c3)
| sk_c11 = multiply(sk_c9,sk_c10) ),
inference(reorient_equations,[],[f46]) ).
fof(f48,negated_conjecture,
( multiply(sk_c4,sk_c10) = sk_c9
| multiply(sk_c9,sk_c10) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_23) ).
fof(f49,plain,
( sk_c9 = multiply(sk_c4,sk_c10)
| sk_c11 = multiply(sk_c9,sk_c10) ),
inference(reorient_equations,[],[f48]) ).
fof(f50,negated_conjecture,
( inverse(sk_c4) = sk_c10
| multiply(sk_c9,sk_c10) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_24) ).
fof(f51,plain,
( sk_c10 = inverse(sk_c4)
| sk_c11 = multiply(sk_c9,sk_c10) ),
inference(reorient_equations,[],[f50]) ).
fof(f52,negated_conjecture,
( multiply(sk_c5,sk_c8) = sk_c11
| multiply(sk_c9,sk_c10) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_25) ).
fof(f53,plain,
( sk_c11 = multiply(sk_c5,sk_c8)
| sk_c11 = multiply(sk_c9,sk_c10) ),
inference(reorient_equations,[],[f52]) ).
fof(f54,negated_conjecture,
( inverse(sk_c5) = sk_c8
| multiply(sk_c9,sk_c10) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_26) ).
fof(f55,plain,
( sk_c8 = inverse(sk_c5)
| sk_c11 = multiply(sk_c9,sk_c10) ),
inference(reorient_equations,[],[f54]) ).
fof(f64,negated_conjecture,
( multiply(sk_c3,sk_c11) = sk_c10
| multiply(sk_c11,sk_c2) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_31) ).
fof(f65,plain,
( sk_c10 = multiply(sk_c3,sk_c11)
| sk_c10 = multiply(sk_c11,sk_c2) ),
inference(reorient_equations,[],[f64]) ).
fof(f66,negated_conjecture,
( inverse(sk_c3) = sk_c11
| multiply(sk_c11,sk_c2) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_32) ).
fof(f67,plain,
( sk_c11 = inverse(sk_c3)
| sk_c10 = multiply(sk_c11,sk_c2) ),
inference(reorient_equations,[],[f66]) ).
fof(f68,negated_conjecture,
( multiply(sk_c4,sk_c10) = sk_c9
| multiply(sk_c11,sk_c2) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_33) ).
fof(f69,plain,
( sk_c9 = multiply(sk_c4,sk_c10)
| sk_c10 = multiply(sk_c11,sk_c2) ),
inference(reorient_equations,[],[f68]) ).
fof(f70,negated_conjecture,
( inverse(sk_c4) = sk_c10
| multiply(sk_c11,sk_c2) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_34) ).
fof(f71,plain,
( sk_c10 = inverse(sk_c4)
| sk_c10 = multiply(sk_c11,sk_c2) ),
inference(reorient_equations,[],[f70]) ).
fof(f72,negated_conjecture,
( multiply(sk_c5,sk_c8) = sk_c11
| multiply(sk_c11,sk_c2) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_35) ).
fof(f73,plain,
( sk_c11 = multiply(sk_c5,sk_c8)
| sk_c10 = multiply(sk_c11,sk_c2) ),
inference(reorient_equations,[],[f72]) ).
fof(f74,negated_conjecture,
( inverse(sk_c5) = sk_c8
| multiply(sk_c11,sk_c2) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_36) ).
fof(f75,plain,
( sk_c8 = inverse(sk_c5)
| sk_c10 = multiply(sk_c11,sk_c2) ),
inference(reorient_equations,[],[f74]) ).
fof(f84,negated_conjecture,
( multiply(sk_c3,sk_c11) = sk_c10
| multiply(sk_c1,sk_c11) = sk_c2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_41) ).
fof(f85,plain,
( sk_c10 = multiply(sk_c3,sk_c11)
| sk_c2 = multiply(sk_c1,sk_c11) ),
inference(reorient_equations,[],[f84]) ).
fof(f86,negated_conjecture,
( inverse(sk_c3) = sk_c11
| multiply(sk_c1,sk_c11) = sk_c2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_42) ).
fof(f87,plain,
( sk_c11 = inverse(sk_c3)
| sk_c2 = multiply(sk_c1,sk_c11) ),
inference(reorient_equations,[],[f86]) ).
fof(f88,negated_conjecture,
( multiply(sk_c4,sk_c10) = sk_c9
| multiply(sk_c1,sk_c11) = sk_c2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_43) ).
fof(f89,plain,
( sk_c9 = multiply(sk_c4,sk_c10)
| sk_c2 = multiply(sk_c1,sk_c11) ),
inference(reorient_equations,[],[f88]) ).
fof(f90,negated_conjecture,
( inverse(sk_c4) = sk_c10
| multiply(sk_c1,sk_c11) = sk_c2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_44) ).
fof(f91,plain,
( sk_c10 = inverse(sk_c4)
| sk_c2 = multiply(sk_c1,sk_c11) ),
inference(reorient_equations,[],[f90]) ).
fof(f92,negated_conjecture,
( multiply(sk_c5,sk_c8) = sk_c11
| multiply(sk_c1,sk_c11) = sk_c2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_45) ).
fof(f93,plain,
( sk_c11 = multiply(sk_c5,sk_c8)
| sk_c2 = multiply(sk_c1,sk_c11) ),
inference(reorient_equations,[],[f92]) ).
fof(f94,negated_conjecture,
( inverse(sk_c5) = sk_c8
| multiply(sk_c1,sk_c11) = sk_c2 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_46) ).
fof(f95,plain,
( sk_c8 = inverse(sk_c5)
| sk_c2 = multiply(sk_c1,sk_c11) ),
inference(reorient_equations,[],[f94]) ).
fof(f104,negated_conjecture,
( multiply(sk_c3,sk_c11) = sk_c10
| inverse(sk_c1) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_51) ).
fof(f105,plain,
( sk_c10 = multiply(sk_c3,sk_c11)
| sk_c11 = inverse(sk_c1) ),
inference(reorient_equations,[],[f104]) ).
fof(f106,negated_conjecture,
( inverse(sk_c3) = sk_c11
| inverse(sk_c1) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_52) ).
fof(f107,plain,
( sk_c11 = inverse(sk_c3)
| sk_c11 = inverse(sk_c1) ),
inference(reorient_equations,[],[f106]) ).
fof(f108,negated_conjecture,
( multiply(sk_c4,sk_c10) = sk_c9
| inverse(sk_c1) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_53) ).
fof(f109,plain,
( sk_c9 = multiply(sk_c4,sk_c10)
| sk_c11 = inverse(sk_c1) ),
inference(reorient_equations,[],[f108]) ).
fof(f110,negated_conjecture,
( inverse(sk_c4) = sk_c10
| inverse(sk_c1) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_54) ).
fof(f111,plain,
( sk_c10 = inverse(sk_c4)
| sk_c11 = inverse(sk_c1) ),
inference(reorient_equations,[],[f110]) ).
fof(f112,negated_conjecture,
( multiply(sk_c5,sk_c8) = sk_c11
| inverse(sk_c1) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_55) ).
fof(f113,plain,
( sk_c11 = multiply(sk_c5,sk_c8)
| sk_c11 = inverse(sk_c1) ),
inference(reorient_equations,[],[f112]) ).
fof(f114,negated_conjecture,
( inverse(sk_c5) = sk_c8
| inverse(sk_c1) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_56) ).
fof(f115,plain,
( sk_c8 = inverse(sk_c5)
| sk_c11 = inverse(sk_c1) ),
inference(reorient_equations,[],[f114]) ).
fof(f118,negated_conjecture,
( inverse(sk_c7) = sk_c6
| inverse(sk_c1) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_58) ).
fof(f119,plain,
( inverse(sk_c7) = sk_c6
| sk_c11 = inverse(sk_c1) ),
inference(reorient_equations,[],[f118]) ).
fof(f120,negated_conjecture,
( inverse(sk_c6) = sk_c8
| inverse(sk_c1) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_59) ).
fof(f121,plain,
( sk_c8 = inverse(sk_c6)
| sk_c11 = inverse(sk_c1) ),
inference(reorient_equations,[],[f120]) ).
fof(f124,negated_conjecture,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( multiply(X6,X5) != X7
| inverse(X7) != X5
| inverse(X6) != X7
| multiply(X5,sk_c10) != sk_c11
| inverse(X4) != X5
| multiply(X4,X5) != sk_c11
| inverse(X3) != sk_c10
| multiply(X3,sk_c10) != sk_c9
| inverse(X2) != sk_c11
| multiply(X2,sk_c11) != sk_c10
| inverse(X1) != sk_c11
| multiply(X1,sk_c11) != X0
| multiply(sk_c11,X0) != sk_c10
| multiply(sk_c9,sk_c10) != sk_c11
| inverse(sk_c11) != sk_c9
| multiply(sk_c11,sk_c10) != sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_61) ).
fof(f125,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( multiply(X6,X5) != X7
| inverse(X7) != X5
| inverse(X6) != X7
| sk_c11 != multiply(X5,sk_c10)
| inverse(X4) != X5
| sk_c11 != multiply(X4,X5)
| sk_c10 != inverse(X3)
| sk_c9 != multiply(X3,sk_c10)
| sk_c11 != inverse(X2)
| sk_c10 != multiply(X2,sk_c11)
| sk_c11 != inverse(X1)
| multiply(X1,sk_c11) != X0
| sk_c10 != multiply(sk_c11,X0)
| sk_c11 != multiply(sk_c9,sk_c10)
| sk_c9 != inverse(sk_c11)
| multiply(sk_c11,sk_c10) != sk_c9 ),
inference(reorient_equations,[],[f124]) ).
fof(f126,plain,
! [X2,X3,X1,X6,X7,X4,X5] :
( multiply(X6,X5) != X7
| inverse(X7) != X5
| inverse(X6) != X7
| sk_c11 != multiply(X5,sk_c10)
| inverse(X4) != X5
| sk_c11 != multiply(X4,X5)
| sk_c10 != inverse(X3)
| sk_c9 != multiply(X3,sk_c10)
| sk_c11 != inverse(X2)
| sk_c10 != multiply(X2,sk_c11)
| sk_c11 != inverse(X1)
| sk_c10 != multiply(sk_c11,multiply(X1,sk_c11))
| sk_c11 != multiply(sk_c9,sk_c10)
| sk_c9 != inverse(sk_c11)
| multiply(sk_c11,sk_c10) != sk_c9 ),
inference(equality_resolution,[],[f125]) ).
fof(f127,plain,
! [X2,X3,X1,X6,X7,X4] :
( multiply(X6,inverse(X4)) != X7
| inverse(X4) != inverse(X7)
| inverse(X6) != X7
| sk_c11 != multiply(inverse(X4),sk_c10)
| sk_c11 != multiply(X4,inverse(X4))
| sk_c10 != inverse(X3)
| sk_c9 != multiply(X3,sk_c10)
| sk_c11 != inverse(X2)
| sk_c10 != multiply(X2,sk_c11)
| sk_c11 != inverse(X1)
| sk_c10 != multiply(sk_c11,multiply(X1,sk_c11))
| sk_c11 != multiply(sk_c9,sk_c10)
| sk_c9 != inverse(sk_c11)
| multiply(sk_c11,sk_c10) != sk_c9 ),
inference(equality_resolution,[],[f126]) ).
fof(f128,plain,
! [X2,X3,X1,X6,X4] :
( inverse(X6) != multiply(X6,inverse(X4))
| inverse(X4) != inverse(inverse(X6))
| sk_c11 != multiply(inverse(X4),sk_c10)
| sk_c11 != multiply(X4,inverse(X4))
| sk_c10 != inverse(X3)
| sk_c9 != multiply(X3,sk_c10)
| sk_c11 != inverse(X2)
| sk_c10 != multiply(X2,sk_c11)
| sk_c11 != inverse(X1)
| sk_c10 != multiply(sk_c11,multiply(X1,sk_c11))
| sk_c11 != multiply(sk_c9,sk_c10)
| sk_c9 != inverse(sk_c11)
| multiply(sk_c11,sk_c10) != sk_c9 ),
inference(equality_resolution,[],[f127]) ).
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_c3,sk_c11) = sk_c10 )
| ( multiply(sk_c11,sk_c10) = sk_c9 ) ),
inference(cnf_transformation,[],[f6]) ).
tcf(c_117,negated_conjecture,
( ( inverse(sk_c3) = sk_c11 )
| ( multiply(sk_c11,sk_c10) = sk_c9 ) ),
inference(cnf_transformation,[],[f8]) ).
tcf(c_118,negated_conjecture,
( ( multiply(sk_c4,sk_c10) = sk_c9 )
| ( multiply(sk_c11,sk_c10) = sk_c9 ) ),
inference(cnf_transformation,[],[f10]) ).
tcf(c_119,negated_conjecture,
( ( inverse(sk_c4) = sk_c10 )
| ( multiply(sk_c11,sk_c10) = sk_c9 ) ),
inference(cnf_transformation,[],[f12]) ).
tcf(c_120,negated_conjecture,
( ( multiply(sk_c5,sk_c8) = sk_c11 )
| ( multiply(sk_c11,sk_c10) = sk_c9 ) ),
inference(cnf_transformation,[],[f14]) ).
tcf(c_121,negated_conjecture,
( ( inverse(sk_c5) = sk_c8 )
| ( multiply(sk_c11,sk_c10) = sk_c9 ) ),
inference(cnf_transformation,[],[f16]) ).
tcf(c_126,negated_conjecture,
( ( inverse(sk_c11) = sk_c9 )
| ( multiply(sk_c3,sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f25]) ).
tcf(c_127,negated_conjecture,
( ( inverse(sk_c3) = sk_c11 )
| ( inverse(sk_c11) = sk_c9 ) ),
inference(cnf_transformation,[],[f27]) ).
tcf(c_128,negated_conjecture,
( ( inverse(sk_c11) = sk_c9 )
| ( multiply(sk_c4,sk_c10) = sk_c9 ) ),
inference(cnf_transformation,[],[f29]) ).
tcf(c_129,negated_conjecture,
( ( inverse(sk_c4) = sk_c10 )
| ( inverse(sk_c11) = sk_c9 ) ),
inference(cnf_transformation,[],[f31]) ).
tcf(c_130,negated_conjecture,
( ( inverse(sk_c11) = sk_c9 )
| ( multiply(sk_c5,sk_c8) = sk_c11 ) ),
inference(cnf_transformation,[],[f33]) ).
tcf(c_131,negated_conjecture,
( ( inverse(sk_c5) = sk_c8 )
| ( inverse(sk_c11) = sk_c9 ) ),
inference(cnf_transformation,[],[f35]) ).
tcf(c_136,negated_conjecture,
( ( multiply(sk_c3,sk_c11) = sk_c10 )
| ( multiply(sk_c9,sk_c10) = sk_c11 ) ),
inference(cnf_transformation,[],[f45]) ).
tcf(c_137,negated_conjecture,
( ( inverse(sk_c3) = sk_c11 )
| ( multiply(sk_c9,sk_c10) = sk_c11 ) ),
inference(cnf_transformation,[],[f47]) ).
tcf(c_138,negated_conjecture,
( ( multiply(sk_c4,sk_c10) = sk_c9 )
| ( multiply(sk_c9,sk_c10) = sk_c11 ) ),
inference(cnf_transformation,[],[f49]) ).
tcf(c_139,negated_conjecture,
( ( inverse(sk_c4) = sk_c10 )
| ( multiply(sk_c9,sk_c10) = sk_c11 ) ),
inference(cnf_transformation,[],[f51]) ).
tcf(c_140,negated_conjecture,
( ( multiply(sk_c5,sk_c8) = sk_c11 )
| ( multiply(sk_c9,sk_c10) = sk_c11 ) ),
inference(cnf_transformation,[],[f53]) ).
tcf(c_141,negated_conjecture,
( ( inverse(sk_c5) = sk_c8 )
| ( multiply(sk_c9,sk_c10) = sk_c11 ) ),
inference(cnf_transformation,[],[f55]) ).
tcf(c_146,negated_conjecture,
( ( multiply(sk_c3,sk_c11) = sk_c10 )
| ( multiply(sk_c11,sk_c2) = sk_c10 ) ),
inference(cnf_transformation,[],[f65]) ).
tcf(c_147,negated_conjecture,
( ( inverse(sk_c3) = sk_c11 )
| ( multiply(sk_c11,sk_c2) = sk_c10 ) ),
inference(cnf_transformation,[],[f67]) ).
tcf(c_148,negated_conjecture,
( ( multiply(sk_c4,sk_c10) = sk_c9 )
| ( multiply(sk_c11,sk_c2) = sk_c10 ) ),
inference(cnf_transformation,[],[f69]) ).
tcf(c_149,negated_conjecture,
( ( inverse(sk_c4) = sk_c10 )
| ( multiply(sk_c11,sk_c2) = sk_c10 ) ),
inference(cnf_transformation,[],[f71]) ).
tcf(c_150,negated_conjecture,
( ( multiply(sk_c5,sk_c8) = sk_c11 )
| ( multiply(sk_c11,sk_c2) = sk_c10 ) ),
inference(cnf_transformation,[],[f73]) ).
tcf(c_151,negated_conjecture,
( ( inverse(sk_c5) = sk_c8 )
| ( multiply(sk_c11,sk_c2) = sk_c10 ) ),
inference(cnf_transformation,[],[f75]) ).
tcf(c_156,negated_conjecture,
( ( multiply(sk_c1,sk_c11) = sk_c2 )
| ( multiply(sk_c3,sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f85]) ).
tcf(c_157,negated_conjecture,
( ( inverse(sk_c3) = sk_c11 )
| ( multiply(sk_c1,sk_c11) = sk_c2 ) ),
inference(cnf_transformation,[],[f87]) ).
tcf(c_158,negated_conjecture,
( ( multiply(sk_c1,sk_c11) = sk_c2 )
| ( multiply(sk_c4,sk_c10) = sk_c9 ) ),
inference(cnf_transformation,[],[f89]) ).
tcf(c_159,negated_conjecture,
( ( inverse(sk_c4) = sk_c10 )
| ( multiply(sk_c1,sk_c11) = sk_c2 ) ),
inference(cnf_transformation,[],[f91]) ).
tcf(c_160,negated_conjecture,
( ( multiply(sk_c1,sk_c11) = sk_c2 )
| ( multiply(sk_c5,sk_c8) = sk_c11 ) ),
inference(cnf_transformation,[],[f93]) ).
tcf(c_161,negated_conjecture,
( ( inverse(sk_c5) = sk_c8 )
| ( multiply(sk_c1,sk_c11) = sk_c2 ) ),
inference(cnf_transformation,[],[f95]) ).
tcf(c_166,negated_conjecture,
( ( inverse(sk_c1) = sk_c11 )
| ( multiply(sk_c3,sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f105]) ).
tcf(c_167,negated_conjecture,
( ( inverse(sk_c1) = sk_c11 )
| ( inverse(sk_c3) = sk_c11 ) ),
inference(cnf_transformation,[],[f107]) ).
tcf(c_168,negated_conjecture,
( ( inverse(sk_c1) = sk_c11 )
| ( multiply(sk_c4,sk_c10) = sk_c9 ) ),
inference(cnf_transformation,[],[f109]) ).
tcf(c_169,negated_conjecture,
( ( inverse(sk_c1) = sk_c11 )
| ( inverse(sk_c4) = sk_c10 ) ),
inference(cnf_transformation,[],[f111]) ).
tcf(c_170,negated_conjecture,
( ( inverse(sk_c1) = sk_c11 )
| ( multiply(sk_c5,sk_c8) = sk_c11 ) ),
inference(cnf_transformation,[],[f113]) ).
tcf(c_171,negated_conjecture,
( ( inverse(sk_c1) = sk_c11 )
| ( inverse(sk_c5) = sk_c8 ) ),
inference(cnf_transformation,[],[f115]) ).
tcf(c_173,negated_conjecture,
( ( inverse(sk_c1) = sk_c11 )
| ( inverse(sk_c7) = sk_c6 ) ),
inference(cnf_transformation,[],[f119]) ).
tcf(c_174,negated_conjecture,
( ( inverse(sk_c1) = sk_c11 )
| ( inverse(sk_c6) = sk_c8 ) ),
inference(cnf_transformation,[],[f121]) ).
tcf(c_176,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( ( inverse(sk_c11) != sk_c9 )
| ( inverse(X4) != sk_c10 )
| ( inverse(X3) != sk_c11 )
| ( inverse(X2) != sk_c11 )
| ( multiply(sk_c9,sk_c10) != sk_c11 )
| ( multiply(sk_c11,sk_c10) != sk_c9 )
| ( inverse(inverse(X0)) != inverse(X1) )
| ( multiply(X4,sk_c10) != sk_c9 )
| ( multiply(X3,sk_c11) != sk_c10 )
| ( multiply(inverse(X1),sk_c10) != sk_c11 )
| ( multiply(X1,inverse(X1)) != sk_c11 )
| ( multiply(X0,inverse(X1)) != inverse(X0) )
| ( multiply(sk_c11,multiply(X2,sk_c11)) != sk_c10 ) ),
inference(cnf_transformation,[],[f128]) ).
tcf(c_178,plain,
multiply(inverse(sk_c11),sk_c11) = identity,
inference(instantiation,[status(thm)],[c_114]) ).
tcf(c_721,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_10
| ( inverse(X0) != sk_c11 )
| ( multiply(X0,sk_c11) != sk_c10 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_10])],[c_176]) ).
tcf(c_722,negated_conjecture,
! [X0: $i,X1: $i] :
( ~ iPr_def_11
| ( inverse(inverse(X0)) != inverse(X1) )
| ( multiply(inverse(X1),sk_c10) != sk_c11 )
| ( multiply(X1,inverse(X1)) != sk_c11 )
| ( multiply(X0,inverse(X1)) != inverse(X0) ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_11])],[c_176]) ).
tcf(c_723,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_12
| ( inverse(X0) != sk_c10 )
| ( multiply(X0,sk_c10) != sk_c9 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_12])],[c_176]) ).
tcf(c_724,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_13
| ( inverse(X0) != sk_c11 )
| ( multiply(sk_c11,multiply(X0,sk_c11)) != sk_c10 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_13])],[c_176]) ).
tcf(c_725,negated_conjecture,
( iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( inverse(sk_c11) != sk_c9 )
| ( multiply(sk_c9,sk_c10) != sk_c11 )
| ( multiply(sk_c11,sk_c10) != sk_c9 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_176]) ).
tcf(c_726,plain,
! [X0: $i] : X0 = X0,
theory(equality) ).
tcf(c_727,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = X0 )
| ( X2 != X1 )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_728,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( multiply(X0,X2) = multiply(X1,X3) )
| ( X2 != X3 )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_729,plain,
! [X0: $i,X1: $i] :
( ( inverse(X0) = inverse(X1) )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_731,plain,
( ( inverse(sk_c11) = inverse(sk_c11) )
| ( sk_c11 != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_729]) ).
tcf(c_732,plain,
sk_c11 = sk_c11,
inference(instantiation,[status(thm)],[c_726]) ).
tcf(c_733,plain,
( ~ iPr_def_10
| ( inverse(sk_c11) != sk_c11 )
| ( multiply(sk_c11,sk_c11) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_721]) ).
tcf(c_735,plain,
( ~ iPr_def_12
| ( inverse(sk_c11) != sk_c10 )
| ( multiply(sk_c11,sk_c10) != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_723]) ).
tcf(c_1043,plain,
! [X0: $i] :
( ( inverse(sk_c11) = sk_c9 )
| ( sk_c9 != X0 )
| ( inverse(sk_c11) != X0 ) ),
inference(instantiation,[status(thm)],[c_727]) ).
tcf(c_1045,plain,
( ( inverse(sk_c11) = sk_c9 )
| ( sk_c9 != inverse(sk_c11) )
| ( inverse(sk_c11) != inverse(sk_c11) ) ),
inference(instantiation,[status(thm)],[c_1043]) ).
tcf(c_1047,plain,
! [X0: $i,X1: $i] :
( ( inverse(sk_c11) = X1 )
| ( X1 != X0 )
| ( inverse(sk_c11) != X0 ) ),
inference(instantiation,[status(thm)],[c_727]) ).
tcf(c_1049,plain,
! [X0: $i] :
( ( inverse(sk_c11) = inverse(X0) )
| ( sk_c11 != X0 ) ),
inference(instantiation,[status(thm)],[c_729]) ).
tcf(c_1050,plain,
! [X0: $i] :
( ( sk_c9 = inverse(sk_c11) )
| ( sk_c9 != X0 )
| ( inverse(sk_c11) != X0 ) ),
inference(instantiation,[status(thm)],[c_727]) ).
tcf(c_1053,plain,
! [X0: $i,X1: $i] :
( ( sk_c9 = inverse(X0) )
| ( sk_c9 != X1 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_727]) ).
tcf(c_1060,plain,
! [X0: $i] :
( ( inverse(sk_c11) = X0 )
| ( X0 != inverse(sk_c11) )
| ( inverse(sk_c11) != inverse(sk_c11) ) ),
inference(instantiation,[status(thm)],[c_1047]) ).
tcf(c_1063,plain,
( ( sk_c9 = inverse(sk_c11) )
| ( sk_c9 != sk_c9 )
| ( inverse(sk_c11) != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_1050]) ).
tcf(c_1064,plain,
sk_c9 = sk_c9,
inference(instantiation,[status(thm)],[c_726]) ).
tcf(c_1065,plain,
! [X0: $i,X1: $i] :
( ( sk_c9 = X0 )
| ( sk_c9 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_727]) ).
tcf(c_1069,plain,
( ( inverse(sk_c11) = multiply(identity,inverse(sk_c11)) )
| ( inverse(sk_c11) != inverse(sk_c11) )
| ( multiply(identity,inverse(sk_c11)) != inverse(sk_c11) ) ),
inference(instantiation,[status(thm)],[c_1060]) ).
tcf(c_1070,plain,
multiply(identity,inverse(sk_c11)) = inverse(sk_c11),
inference(instantiation,[status(thm)],[c_113]) ).
tcf(c_1072,plain,
! [X0: $i,X1: $i] :
( ( X1 = inverse(sk_c11) )
| ( X1 != X0 )
| ( inverse(sk_c11) != X0 ) ),
inference(instantiation,[status(thm)],[c_727]) ).
tcf(c_1079,plain,
! [X0: $i] : multiply(identity,inverse(X0)) = inverse(X0),
inference(instantiation,[status(thm)],[c_113]) ).
tcf(c_1081,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = inverse(X0) )
| ( X2 != X1 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_727]) ).
tcf(c_1105,plain,
! [X0: $i] :
( ( sk_c9 = X0 )
| ( sk_c9 != sk_c9 )
| ( X0 != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_1065]) ).
tcf(c_1113,plain,
! [X0: $i] :
( ( X0 = inverse(sk_c11) )
| ( X0 != multiply(identity,inverse(sk_c11)) )
| ( inverse(sk_c11) != multiply(identity,inverse(sk_c11)) ) ),
inference(instantiation,[status(thm)],[c_1072]) ).
tcf(c_1124,plain,
! [X0: $i] :
( ( X0 = inverse(sk_c3) )
| ( X0 != sk_c11 )
| ( inverse(sk_c3) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_1081]) ).
tcf(c_1125,plain,
( ( sk_c11 = inverse(sk_c3) )
| ( sk_c11 != sk_c11 )
| ( inverse(sk_c3) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_1124]) ).
tcf(c_1126,plain,
! [X0: $i] :
( ( X0 = inverse(sk_c4) )
| ( X0 != sk_c10 )
| ( inverse(sk_c4) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_1081]) ).
tcf(c_1135,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( inverse(X0) = X2 )
| ( X2 != X1 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_727]) ).
tcf(c_1136,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = inverse(X0) )
| ( X2 != inverse(X1) )
| ( inverse(X0) != inverse(X1) ) ),
inference(instantiation,[status(thm)],[c_1081]) ).
tcf(c_1307,plain,
! [X0: $i] :
( ( inverse(sk_c5) = sk_c8 )
| ( multiply(sk_c9,multiply(sk_c10,X0)) = multiply(sk_c11,X0) ) ),
inference(superposition,[status(thm)],[c_141,c_115]) ).
tcf(c_1308,plain,
! [X0: $i] :
( ( inverse(sk_c4) = sk_c10 )
| ( multiply(sk_c9,multiply(sk_c10,X0)) = multiply(sk_c11,X0) ) ),
inference(superposition,[status(thm)],[c_139,c_115]) ).
tcf(c_1309,plain,
! [X0: $i] :
( ( inverse(sk_c3) = sk_c11 )
| ( multiply(sk_c9,multiply(sk_c10,X0)) = multiply(sk_c11,X0) ) ),
inference(superposition,[status(thm)],[c_137,c_115]) ).
tcf(c_1321,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(X0,X1)) = multiply(identity,X1),
inference(superposition,[status(thm)],[c_114,c_115]) ).
tcf(c_1363,plain,
! [X0: $i,X1: $i] :
( ( multiply(X0,X1) = multiply(identity,inverse(sk_c11)) )
| ( X1 != inverse(sk_c11) )
| ( X0 != identity ) ),
inference(instantiation,[status(thm)],[c_728]) ).
tcf(c_1371,plain,
! [X0: $i] : inverse(X0) = inverse(X0),
inference(instantiation,[status(thm)],[c_726]) ).
tcf(c_1383,plain,
( ( multiply(identity,sk_c10) = inverse(sk_c4) )
| ( inverse(sk_c4) != sk_c10 )
| ( multiply(identity,sk_c10) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_1126]) ).
tcf(c_1384,plain,
multiply(identity,sk_c10) = sk_c10,
inference(instantiation,[status(thm)],[c_113]) ).
tcf(c_1385,plain,
( ( sk_c10 = inverse(sk_c4) )
| ( sk_c10 != sk_c10 )
| ( inverse(sk_c4) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_1126]) ).
tcf(c_1386,plain,
sk_c10 = sk_c10,
inference(instantiation,[status(thm)],[c_726]) ).
tcf(c_1387,plain,
! [X0: $i,X1: $i] :
( ( X0 = sk_c10 )
| ( sk_c10 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_727]) ).
tcf(c_1405,plain,
( ( sk_c9 = multiply(sk_c4,sk_c10) )
| ( sk_c9 != sk_c9 )
| ( multiply(sk_c4,sk_c10) != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_1105]) ).
tcf(c_1409,plain,
! [X0: $i,X1: $i] :
( ( X0 = sk_c9 )
| ( sk_c9 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_727]) ).
tcf(c_1413,plain,
! [X0: $i,X1: $i] :
( ( sk_c9 = X0 )
| ( sk_c9 != inverse(X1) )
| ( X0 != inverse(X1) ) ),
inference(instantiation,[status(thm)],[c_1065]) ).
tcf(c_1429,plain,
! [X0: $i] :
( ( inverse(sk_c11) = X0 )
| ( X0 != sk_c9 )
| ( inverse(sk_c11) != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_1047]) ).
tcf(c_1431,plain,
( ( inverse(sk_c11) = sk_c11 )
| ( sk_c11 != sk_c9 )
| ( inverse(sk_c11) != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_1429]) ).
tcf(c_1437,plain,
! [X0: $i] :
( ( multiply(sk_c9,sk_c10) = sk_c11 )
| ( sk_c11 != X0 )
| ( multiply(sk_c9,sk_c10) != X0 ) ),
inference(instantiation,[status(thm)],[c_727]) ).
tcf(c_1446,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = multiply(identity,inverse(X0)) )
| ( X2 != X1 )
| ( multiply(identity,inverse(X0)) != X1 ) ),
inference(instantiation,[status(thm)],[c_727]) ).
tcf(c_1448,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(X0,X1) = multiply(identity,inverse(X2)) )
| ( X1 != inverse(X2) )
| ( X0 != identity ) ),
inference(instantiation,[status(thm)],[c_728]) ).
tcf(c_1495,plain,
! [X0: $i] :
( ( inverse(sk_c3) = X0 )
| ( X0 != sk_c11 )
| ( inverse(sk_c3) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_1135]) ).
tcf(c_1496,plain,
! [X0: $i] :
( ( inverse(sk_c4) = X0 )
| ( X0 != sk_c10 )
| ( inverse(sk_c4) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_1135]) ).
tcf(c_1497,plain,
( ( inverse(sk_c4) = sk_c11 )
| ( sk_c11 != sk_c10 )
| ( inverse(sk_c4) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_1496]) ).
tcf(c_1508,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( inverse(X0) = X2 )
| ( X2 != inverse(X1) )
| ( inverse(X0) != inverse(X1) ) ),
inference(instantiation,[status(thm)],[c_1135]) ).
tcf(c_1600,plain,
! [X0: $i] :
( ( sk_c9 = X0 )
| ( sk_c9 != multiply(sk_c4,sk_c10) )
| ( X0 != multiply(sk_c4,sk_c10) ) ),
inference(instantiation,[status(thm)],[c_1065]) ).
tcf(c_1602,plain,
( ( sk_c9 = sk_c11 )
| ( sk_c9 != multiply(sk_c4,sk_c10) )
| ( sk_c11 != multiply(sk_c4,sk_c10) ) ),
inference(instantiation,[status(thm)],[c_1600]) ).
tcf(c_1627,plain,
! [X0: $i,X1: $i] :
( ( multiply(sk_c9,sk_c10) = X1 )
| ( X1 != X0 )
| ( multiply(sk_c9,sk_c10) != X0 ) ),
inference(instantiation,[status(thm)],[c_727]) ).
tcf(c_1628,plain,
! [X0: $i,X1: $i] :
( ( multiply(sk_c9,sk_c10) = sk_c11 )
| ( sk_c11 != multiply(X0,X1) )
| ( multiply(sk_c9,sk_c10) != multiply(X0,X1) ) ),
inference(instantiation,[status(thm)],[c_1437]) ).
tcf(c_1629,plain,
! [X0: $i,X1: $i] :
( ( multiply(sk_c9,sk_c10) = multiply(X1,X0) )
| ( sk_c9 != X1 )
| ( sk_c10 != X0 ) ),
inference(instantiation,[status(thm)],[c_728]) ).
tcf(c_1630,plain,
( ( multiply(sk_c9,sk_c10) = sk_c11 )
| ( sk_c11 != multiply(sk_c11,sk_c11) )
| ( multiply(sk_c9,sk_c10) != multiply(sk_c11,sk_c11) ) ),
inference(instantiation,[status(thm)],[c_1628]) ).
tcf(c_1631,plain,
( ( multiply(sk_c9,sk_c10) = multiply(sk_c11,sk_c11) )
| ( sk_c9 != sk_c11 )
| ( sk_c10 != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_1629]) ).
tcf(c_1650,plain,
! [X0: $i,X1: $i] :
( ( inverse(sk_c3) = X1 )
| ( X1 != X0 )
| ( inverse(sk_c3) != X0 ) ),
inference(instantiation,[status(thm)],[c_1135]) ).
tcf(c_1651,plain,
! [X0: $i,X1: $i] :
( ( X1 = inverse(sk_c3) )
| ( X1 != X0 )
| ( inverse(sk_c3) != X0 ) ),
inference(instantiation,[status(thm)],[c_1081]) ).
tcf(c_1752,plain,
( ( inverse(sk_c4) = multiply(sk_c3,sk_c11) )
| ( inverse(sk_c4) != sk_c10 )
| ( multiply(sk_c3,sk_c11) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_1496]) ).
tcf(c_2061,plain,
( ( inverse(sk_c1) = sk_c11 )
| ~ iPr_def_10
| ( inverse(sk_c3) != sk_c11 ) ),
inference(resolution,[status(thm)],[c_721,c_166]) ).
tcf(c_2062,plain,
( ( multiply(sk_c11,sk_c10) = sk_c9 )
| ~ iPr_def_10
| ( inverse(sk_c3) != sk_c11 ) ),
inference(resolution,[status(thm)],[c_721,c_116]) ).
tcf(c_2063,plain,
( ( multiply(sk_c9,sk_c10) = sk_c11 )
| ~ iPr_def_10
| ( inverse(sk_c3) != sk_c11 ) ),
inference(resolution,[status(thm)],[c_721,c_136]) ).
tcf(c_2064,plain,
( ( multiply(sk_c11,sk_c2) = sk_c10 )
| ~ iPr_def_10
| ( inverse(sk_c3) != sk_c11 ) ),
inference(resolution,[status(thm)],[c_721,c_146]) ).
tcf(c_2084,plain,
( ( inverse(sk_c4) = multiply(identity,sk_c10) )
| ( inverse(sk_c4) != sk_c10 )
| ( multiply(identity,sk_c10) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_1496]) ).
tcf(c_2092,plain,
! [X0: $i] :
( ( sk_c10 = inverse(X0) )
| ( sk_c10 != inverse(sk_c4) )
| ( inverse(X0) != inverse(sk_c4) ) ),
inference(instantiation,[status(thm)],[c_1136]) ).
tcf(c_2110,plain,
( ( inverse(sk_c3) = sk_c11 )
| ~ iPr_def_12
| ( inverse(sk_c11) != sk_c10 ) ),
inference(resolution,[status(thm)],[c_723,c_117]) ).
tcf(c_2111,plain,
( ( inverse(sk_c4) = sk_c10 )
| ~ iPr_def_12
| ( inverse(sk_c11) != sk_c10 ) ),
inference(resolution,[status(thm)],[c_723,c_119]) ).
tcf(c_2116,plain,
( ( inverse(sk_c1) = sk_c11 )
| ~ iPr_def_12
| ( inverse(sk_c4) != sk_c10 ) ),
inference(resolution,[status(thm)],[c_723,c_168]) ).
tcf(c_2117,plain,
( ( multiply(sk_c11,sk_c10) = sk_c9 )
| ~ iPr_def_12
| ( inverse(sk_c4) != sk_c10 ) ),
inference(resolution,[status(thm)],[c_723,c_118]) ).
tcf(c_2119,plain,
( ( multiply(sk_c11,sk_c2) = sk_c10 )
| ~ iPr_def_12
| ( inverse(sk_c4) != sk_c10 ) ),
inference(resolution,[status(thm)],[c_723,c_148]) ).
tcf(c_2181,plain,
( ( inverse(sk_c11) = inverse(sk_c4) )
| ( sk_c11 != sk_c4 ) ),
inference(instantiation,[status(thm)],[c_1049]) ).
tcf(c_2267,plain,
( iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( inverse(sk_c3) = sk_c11 )
| ( inverse(sk_c11) != sk_c9 )
| ( multiply(sk_c11,sk_c10) != sk_c9 ) ),
inference(resolution,[status(thm)],[c_725,c_137]) ).
tcf(c_2268,plain,
( iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( inverse(sk_c4) = sk_c10 )
| ( inverse(sk_c11) != sk_c9 )
| ( multiply(sk_c11,sk_c10) != sk_c9 ) ),
inference(resolution,[status(thm)],[c_725,c_139]) ).
tcf(c_2269,plain,
( iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( inverse(sk_c5) = sk_c8 )
| ( inverse(sk_c11) != sk_c9 )
| ( multiply(sk_c11,sk_c10) != sk_c9 ) ),
inference(resolution,[status(thm)],[c_725,c_141]) ).
tcf(c_2272,plain,
! [X0: $i] :
( ( X0 = sk_c10 )
| ( sk_c10 != inverse(sk_c4) )
| ( X0 != inverse(sk_c4) ) ),
inference(instantiation,[status(thm)],[c_1387]) ).
tcf(c_2273,plain,
( ( sk_c11 = sk_c10 )
| ( sk_c10 != inverse(sk_c4) )
| ( sk_c11 != inverse(sk_c4) ) ),
inference(instantiation,[status(thm)],[c_2272]) ).
tcf(c_2275,plain,
! [X0: $i,X1: $i] :
( ( sk_c10 = X0 )
| ( sk_c10 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_727]) ).
tcf(c_2276,plain,
! [X0: $i] :
( ( X0 = sk_c10 )
| ( sk_c10 != inverse(sk_c3) )
| ( X0 != inverse(sk_c3) ) ),
inference(instantiation,[status(thm)],[c_1387]) ).
tcf(c_2278,plain,
( ( sk_c11 = sk_c10 )
| ( sk_c10 != inverse(sk_c3) )
| ( sk_c11 != inverse(sk_c3) ) ),
inference(instantiation,[status(thm)],[c_2276]) ).
tcf(c_2422,plain,
( ( inverse(sk_c11) != sk_c10 )
| ~ iPr_def_12 ),
inference(global_subsumption_just,[status(thm)],[c_2110,c_735,c_2111,c_2117]) ).
tcf(c_2423,plain,
( ~ iPr_def_12
| ( inverse(sk_c11) != sk_c10 ) ),
inference(renaming,[status(thm)],[c_2422]) ).
tcf(c_2436,plain,
! [X0: $i] :
( ( inverse(sk_c3) = sk_c11 )
| ( multiply(sk_c11,sk_c10) = X0 )
| ( X0 != sk_c9 ) ),
inference(resolution,[status(thm)],[c_727,c_117]) ).
tcf(c_2450,plain,
! [X0: $i] :
( ( multiply(sk_c3,sk_c11) = X0 )
| ( multiply(sk_c11,sk_c2) = sk_c10 )
| ( X0 != sk_c10 ) ),
inference(resolution,[status(thm)],[c_727,c_146]) ).
tcf(c_2467,plain,
! [X0: $i] :
( ( inverse(sk_c4) = X0 )
| ( inverse(sk_c11) = sk_c9 )
| ( X0 != sk_c10 ) ),
inference(resolution,[status(thm)],[c_727,c_129]) ).
tcf(c_2502,plain,
! [X0: $i] :
( ( inverse(sk_c3) = sk_c11 )
| ( multiply(sk_c11,sk_c2) = X0 )
| ( X0 != sk_c10 ) ),
inference(resolution,[status(thm)],[c_727,c_147]) ).
tcf(c_2513,plain,
! [X0: $i] :
( ( inverse(sk_c4) = sk_c10 )
| ( multiply(sk_c1,sk_c11) = X0 )
| ( X0 != sk_c2 ) ),
inference(resolution,[status(thm)],[c_727,c_159]) ).
tcf(c_2514,plain,
! [X0: $i] :
( ( inverse(sk_c5) = sk_c8 )
| ( multiply(sk_c1,sk_c11) = X0 )
| ( X0 != sk_c2 ) ),
inference(resolution,[status(thm)],[c_727,c_161]) ).
tcf(c_2517,plain,
! [X0: $i] :
( ( multiply(sk_c1,sk_c11) = X0 )
| ( multiply(sk_c3,sk_c11) = sk_c10 )
| ( X0 != sk_c2 ) ),
inference(resolution,[status(thm)],[c_727,c_156]) ).
tcf(c_2518,plain,
! [X0: $i] :
( ( multiply(sk_c1,sk_c11) = X0 )
| ( multiply(sk_c4,sk_c10) = sk_c9 )
| ( X0 != sk_c2 ) ),
inference(resolution,[status(thm)],[c_727,c_158]) ).
tcf(c_2538,plain,
! [X0: $i,X1: $i] :
( ( multiply(identity,X1) = X0 )
| ( X0 != X1 ) ),
inference(resolution,[status(thm)],[c_727,c_113]) ).
tcf(c_2539,plain,
! [X0: $i,X1: $i] :
( ( multiply(inverse(X1),X1) = X0 )
| ( X0 != identity ) ),
inference(resolution,[status(thm)],[c_727,c_114]) ).
tcf(c_2543,plain,
! [X0: $i,X1: $i] :
( ( X1 = X0 )
| ( X0 != X1 ) ),
inference(resolution,[status(thm)],[c_727,c_726]) ).
tcf(c_2544,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( inverse(X0) = X2 )
| ( X2 != inverse(X1) )
| ( X0 != X1 ) ),
inference(resolution,[status(thm)],[c_727,c_729]) ).
tcf(c_2575,plain,
identity = identity,
inference(instantiation,[status(thm)],[c_726]) ).
tcf(c_2577,plain,
! [X0: $i,X1: $i] :
( ( X0 = identity )
| ( identity != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_727]) ).
tcf(c_2580,plain,
( ( inverse(sk_c3) = identity )
| ( identity != sk_c11 )
| ( inverse(sk_c3) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_1495]) ).
tcf(c_2631,plain,
! [X0: $i,X1: $i] :
( ( X1 = multiply(identity,inverse(X0)) )
| ( X1 != inverse(X0) )
| ( multiply(identity,inverse(X0)) != inverse(X0) ) ),
inference(instantiation,[status(thm)],[c_1446]) ).
tcf(c_2726,plain,
! [X0: $i] :
( ( X0 = sk_c9 )
| ( sk_c9 != multiply(sk_c4,sk_c10) )
| ( X0 != multiply(sk_c4,sk_c10) ) ),
inference(instantiation,[status(thm)],[c_1409]) ).
tcf(c_2727,plain,
( ( sk_c11 = sk_c9 )
| ( sk_c9 != multiply(sk_c4,sk_c10) )
| ( sk_c11 != multiply(sk_c4,sk_c10) ) ),
inference(instantiation,[status(thm)],[c_2726]) ).
tcf(c_2742,plain,
! [X0: $i,X1: $i] :
( ( X0 = sk_c9 )
| ( sk_c9 != inverse(X1) )
| ( X0 != inverse(X1) ) ),
inference(instantiation,[status(thm)],[c_1409]) ).
tcf(c_2923,plain,
! [X0: $i] :
( ( inverse(X0) = sk_c10 )
| ( sk_c10 != inverse(sk_c4) )
| ( inverse(X0) != inverse(sk_c4) ) ),
inference(instantiation,[status(thm)],[c_1508]) ).
tcf(c_2924,plain,
( ( inverse(sk_c11) = sk_c10 )
| ( sk_c10 != inverse(sk_c4) )
| ( inverse(sk_c11) != inverse(sk_c4) ) ),
inference(instantiation,[status(thm)],[c_2923]) ).
tcf(c_2938,plain,
! [X0: $i,X1: $i] :
( ( inverse(X0) = X1 )
| ( X1 != inverse(sk_c3) )
| ( inverse(X0) != inverse(sk_c3) ) ),
inference(instantiation,[status(thm)],[c_1508]) ).
tcf(c_3017,plain,
! [X0: $i] :
( ( X0 = inverse(sk_c4) )
| ( X0 != multiply(sk_c3,sk_c11) )
| ( inverse(sk_c4) != multiply(sk_c3,sk_c11) ) ),
inference(instantiation,[status(thm)],[c_1081]) ).
tcf(c_3018,plain,
( ( sk_c11 = inverse(sk_c4) )
| ( sk_c11 != multiply(sk_c3,sk_c11) )
| ( inverse(sk_c4) != multiply(sk_c3,sk_c11) ) ),
inference(instantiation,[status(thm)],[c_3017]) ).
tcf(c_3034,plain,
( ( inverse(sk_c11) = multiply(sk_c11,sk_c10) )
| ( inverse(sk_c11) != sk_c9 )
| ( multiply(sk_c11,sk_c10) != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_1429]) ).
tcf(c_3035,plain,
( ( sk_c9 = multiply(sk_c11,sk_c10) )
| ( sk_c9 != sk_c9 )
| ( multiply(sk_c11,sk_c10) != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_1105]) ).
tcf(c_3063,plain,
( ( inverse(sk_c4) = multiply(sk_c11,sk_c2) )
| ( inverse(sk_c4) != sk_c10 )
| ( multiply(sk_c11,sk_c2) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_1496]) ).
tcf(c_3066,plain,
! [X0: $i] :
( ( X0 = inverse(sk_c1) )
| ( X0 != sk_c11 )
| ( inverse(sk_c1) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_1081]) ).
tcf(c_3067,plain,
( ( sk_c11 = inverse(sk_c1) )
| ( sk_c11 != sk_c11 )
| ( inverse(sk_c1) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_3066]) ).
tcf(c_3068,plain,
( ~ iPr_def_10
| ( inverse(sk_c3) != sk_c11 )
| ( multiply(sk_c3,sk_c11) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_721]) ).
tcf(c_3187,plain,
! [X0: $i] :
( ( multiply(sk_c9,sk_c10) = sk_c10 )
| ( sk_c10 != X0 )
| ( multiply(sk_c9,sk_c10) != X0 ) ),
inference(instantiation,[status(thm)],[c_1627]) ).
tcf(c_3188,plain,
( ( inverse(sk_c4) = multiply(sk_c9,sk_c10) )
| ( inverse(sk_c4) != sk_c10 )
| ( multiply(sk_c9,sk_c10) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_1496]) ).
tcf(c_3230,plain,
( ~ iPr_def_10
| ( sk_c10 != identity )
| ( inverse(inverse(sk_c11)) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_114,c_721]) ).
tcf(c_3241,plain,
( ( multiply(sk_c1,sk_c11) = sk_c2 )
| ~ iPr_def_12
| ( inverse(sk_c4) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_158,c_723]) ).
tcf(c_3258,plain,
( ~ iPr_def_12
| ( sk_c9 != identity )
| ( inverse(inverse(sk_c10)) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_114,c_723]) ).
tcf(c_3268,plain,
! [X0: $i] :
( ( multiply(sk_c9,sk_c10) = multiply(X0,sk_c10) )
| ( sk_c9 != X0 )
| ( sk_c10 != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_1629]) ).
tcf(c_3280,plain,
! [X0: $i] :
( ( identity = sk_c11 )
| ( identity != X0 )
| ( sk_c11 != X0 ) ),
inference(instantiation,[status(thm)],[c_727]) ).
tcf(c_3315,plain,
! [X0: $i,X1: $i] :
( ( X1 = multiply(sk_c4,sk_c10) )
| ( X1 != X0 )
| ( multiply(sk_c4,sk_c10) != X0 ) ),
inference(instantiation,[status(thm)],[c_727]) ).
tcf(c_3316,plain,
( ( sk_c11 = multiply(sk_c4,sk_c10) )
| ( sk_c11 != sk_c11 )
| ( multiply(sk_c4,sk_c10) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_3315]) ).
tcf(c_3688,plain,
( ( inverse(sk_c5) = sk_c8 )
| ~ iPr_def_13
| ( inverse(sk_c1) != sk_c11 )
| ( multiply(sk_c11,sk_c2) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_161,c_724]) ).
tcf(c_3689,plain,
( ( inverse(sk_c4) = sk_c10 )
| ~ iPr_def_13
| ( inverse(sk_c1) != sk_c11 )
| ( multiply(sk_c11,sk_c2) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_159,c_724]) ).
tcf(c_3690,plain,
( ( inverse(sk_c3) = sk_c11 )
| ~ iPr_def_13
| ( inverse(sk_c1) != sk_c11 )
| ( multiply(sk_c11,sk_c2) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_157,c_724]) ).
tcf(c_3707,plain,
( iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( inverse(sk_c4) = sk_c10 )
| ( inverse(sk_c11) != sk_c9 )
| ( multiply(sk_c9,sk_c10) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_119,c_725]) ).
tcf(c_3708,plain,
( iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( inverse(sk_c3) = sk_c11 )
| ( inverse(sk_c11) != sk_c9 )
| ( multiply(sk_c9,sk_c10) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_117,c_725]) ).
tcf(c_3751,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(X0,X1)) = X1,
inference(demodulation,[status(thm)],[c_1321,c_113]) ).
tcf(c_3771,plain,
( ( inverse(sk_c1) = sk_c11 )
| ( multiply(inverse(sk_c3),sk_c10) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_166,c_3751]) ).
tcf(c_3812,plain,
! [X0: $i] : multiply(inverse(identity),X0) = X0,
inference(superposition,[status(thm)],[c_113,c_3751]) ).
tcf(c_3835,plain,
! [X0: $i,X1: $i] : multiply(inverse(inverse(X0)),X1) = multiply(X0,X1),
inference(superposition,[status(thm)],[c_3751,c_3751]) ).
tcf(c_3942,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_728,c_727]) ).
tcf(c_3949,plain,
( ( sk_c9 = multiply(sk_c11,sk_c10) )
| ( inverse(sk_c4) = sk_c10 ) ),
inference(resolution,[status(thm)],[c_2543,c_119]) ).
tcf(c_3950,plain,
( ( sk_c9 = multiply(sk_c11,sk_c10) )
| ( inverse(sk_c5) = sk_c8 ) ),
inference(resolution,[status(thm)],[c_2543,c_121]) ).
tcf(c_3953,plain,
( ( sk_c10 = multiply(sk_c3,sk_c11) )
| ( inverse(sk_c11) = sk_c9 ) ),
inference(resolution,[status(thm)],[c_2543,c_126]) ).
tcf(c_3955,plain,
( ( sk_c10 = multiply(sk_c3,sk_c11) )
| ( multiply(sk_c11,sk_c10) = sk_c9 ) ),
inference(resolution,[status(thm)],[c_2543,c_116]) ).
tcf(c_3956,plain,
( ( sk_c10 = multiply(sk_c3,sk_c11) )
| ( multiply(sk_c9,sk_c10) = sk_c11 ) ),
inference(resolution,[status(thm)],[c_2543,c_136]) ).
tcf(c_3957,plain,
( ( sk_c10 = multiply(sk_c3,sk_c11) )
| ( multiply(sk_c11,sk_c2) = sk_c10 ) ),
inference(resolution,[status(thm)],[c_2543,c_146]) ).
tcf(c_3959,plain,
( ( sk_c9 = multiply(sk_c4,sk_c10) )
| ( inverse(sk_c11) = sk_c9 ) ),
inference(resolution,[status(thm)],[c_2543,c_128]) ).
tcf(c_3961,plain,
( ( sk_c9 = multiply(sk_c4,sk_c10) )
| ( multiply(sk_c11,sk_c10) = sk_c9 ) ),
inference(resolution,[status(thm)],[c_2543,c_118]) ).
tcf(c_3962,plain,
( ( sk_c9 = multiply(sk_c4,sk_c10) )
| ( multiply(sk_c9,sk_c10) = sk_c11 ) ),
inference(resolution,[status(thm)],[c_2543,c_138]) ).
tcf(c_3967,plain,
( ( sk_c11 = multiply(sk_c5,sk_c8) )
| ( multiply(sk_c11,sk_c10) = sk_c9 ) ),
inference(resolution,[status(thm)],[c_2543,c_120]) ).
tcf(c_3968,plain,
( ( sk_c11 = multiply(sk_c5,sk_c8) )
| ( multiply(sk_c9,sk_c10) = sk_c11 ) ),
inference(resolution,[status(thm)],[c_2543,c_140]) ).
tcf(c_3969,plain,
( ( sk_c11 = multiply(sk_c5,sk_c8) )
| ( multiply(sk_c11,sk_c2) = sk_c10 ) ),
inference(resolution,[status(thm)],[c_2543,c_150]) ).
tcf(c_3989,plain,
( ( sk_c10 = multiply(sk_c11,sk_c2) )
| ( inverse(sk_c3) = sk_c11 ) ),
inference(resolution,[status(thm)],[c_2543,c_147]) ).
tcf(c_3994,plain,
( ( sk_c2 = multiply(sk_c1,sk_c11) )
| ( inverse(sk_c3) = sk_c11 ) ),
inference(resolution,[status(thm)],[c_2543,c_157]) ).
tcf(c_3995,plain,
( ( sk_c2 = multiply(sk_c1,sk_c11) )
| ( inverse(sk_c4) = sk_c10 ) ),
inference(resolution,[status(thm)],[c_2543,c_159]) ).
tcf(c_3999,plain,
( ( sk_c2 = multiply(sk_c1,sk_c11) )
| ( multiply(sk_c3,sk_c11) = sk_c10 ) ),
inference(resolution,[status(thm)],[c_2543,c_156]) ).
tcf(c_4000,plain,
( ( sk_c2 = multiply(sk_c1,sk_c11) )
| ( multiply(sk_c4,sk_c10) = sk_c9 ) ),
inference(resolution,[status(thm)],[c_2543,c_158]) ).
tcf(c_4001,plain,
( ( sk_c2 = multiply(sk_c1,sk_c11) )
| ( multiply(sk_c5,sk_c8) = sk_c11 ) ),
inference(resolution,[status(thm)],[c_2543,c_160]) ).
tcf(c_4010,plain,
! [X0: $i] : X0 = multiply(identity,X0),
inference(resolution,[status(thm)],[c_2543,c_113]) ).
tcf(c_4011,plain,
sk_c11 = multiply(identity,sk_c11),
inference(instantiation,[status(thm)],[c_4010]) ).
tcf(c_4012,plain,
! [X0: $i] : identity = multiply(inverse(X0),X0),
inference(resolution,[status(thm)],[c_2543,c_114]) ).
tcf(c_4071,plain,
! [X0: $i] :
( ( inverse(sk_c3) = X0 )
| ( X0 != inverse(sk_c3) )
| ( inverse(sk_c3) != inverse(sk_c3) ) ),
inference(instantiation,[status(thm)],[c_2938]) ).
tcf(c_4072,plain,
inverse(sk_c3) = inverse(sk_c3),
inference(instantiation,[status(thm)],[c_1371]) ).
tcf(c_4073,plain,
( ( inverse(sk_c3) = sk_c11 )
| ( sk_c11 != inverse(sk_c3) )
| ( inverse(sk_c3) != inverse(sk_c3) ) ),
inference(instantiation,[status(thm)],[c_4071]) ).
tcf(c_4132,plain,
( ~ iPr_def_13
| ( inverse(inverse(identity)) != sk_c11 )
| ( multiply(sk_c11,sk_c11) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_3812,c_724]) ).
tcf(c_4133,plain,
( ~ iPr_def_10
| ( sk_c11 != sk_c10 )
| ( inverse(inverse(identity)) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_3812,c_721]) ).
tcf(c_4159,plain,
! [X0: $i] :
( ( sk_c11 = sk_c4 )
| ( sk_c4 != X0 )
| ( sk_c11 != X0 ) ),
inference(instantiation,[status(thm)],[c_727]) ).
tcf(c_4195,plain,
! [X0: $i] : multiply(X0,inverse(X0)) = identity,
inference(superposition,[status(thm)],[c_3835,c_114]) ).
tcf(c_4302,plain,
! [X0: $i] :
( ( inverse(sk_c3) = inverse(sk_c4) )
| ( inverse(sk_c4) != X0 )
| ( inverse(sk_c3) != X0 ) ),
inference(instantiation,[status(thm)],[c_1650]) ).
tcf(c_4387,plain,
( ( inverse(sk_c1) = sk_c11 )
| ( multiply(sk_c11,sk_c10) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_167,c_3771]) ).
tcf(c_4422,plain,
( iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( inverse(sk_c1) = sk_c11 )
| ( sk_c11 != sk_c9 )
| ( inverse(sk_c11) != sk_c9 )
| ( multiply(sk_c9,sk_c10) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_4387,c_725]) ).
tcf(c_4524,plain,
! [X0: $i] :
( ( sk_c10 = X0 )
| ( sk_c10 != inverse(sk_c4) )
| ( X0 != inverse(sk_c4) ) ),
inference(instantiation,[status(thm)],[c_2275]) ).
tcf(c_4525,plain,
( ( sk_c10 = sk_c11 )
| ( sk_c10 != inverse(sk_c4) )
| ( sk_c11 != inverse(sk_c4) ) ),
inference(instantiation,[status(thm)],[c_4524]) ).
tcf(c_4533,plain,
! [X0: $i] :
( ( sk_c10 = X0 )
| ( sk_c10 != sk_c10 )
| ( X0 != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_2275]) ).
tcf(c_4534,plain,
( ( sk_c10 = sk_c11 )
| ( sk_c10 != sk_c10 )
| ( sk_c11 != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_4533]) ).
tcf(c_4605,plain,
( ( inverse(sk_c1) = sk_c11 )
| ( multiply(sk_c3,sk_c11) = identity ) ),
inference(superposition,[status(thm)],[c_167,c_4195]) ).
tcf(c_4606,plain,
( ( inverse(sk_c11) = sk_c9 )
| ( multiply(sk_c3,sk_c11) = identity ) ),
inference(superposition,[status(thm)],[c_127,c_4195]) ).
tcf(c_4607,plain,
( ( inverse(sk_c1) = sk_c11 )
| ( multiply(sk_c4,sk_c10) = identity ) ),
inference(superposition,[status(thm)],[c_169,c_4195]) ).
tcf(c_4608,plain,
( ( inverse(sk_c11) = sk_c9 )
| ( multiply(sk_c4,sk_c10) = identity ) ),
inference(superposition,[status(thm)],[c_129,c_4195]) ).
tcf(c_4609,plain,
( ( inverse(sk_c1) = sk_c11 )
| ( multiply(sk_c5,sk_c8) = identity ) ),
inference(superposition,[status(thm)],[c_171,c_4195]) ).
tcf(c_4610,plain,
( ( inverse(sk_c11) = sk_c9 )
| ( multiply(sk_c5,sk_c8) = identity ) ),
inference(superposition,[status(thm)],[c_131,c_4195]) ).
tcf(c_4783,plain,
( ( sk_c10 = identity )
| ( inverse(sk_c1) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_4605,c_166]) ).
tcf(c_5072,plain,
( ( sk_c10 = identity )
| ( inverse(sk_c11) = sk_c9 ) ),
inference(superposition,[status(thm)],[c_4606,c_126]) ).
tcf(c_5203,plain,
( ( sk_c9 = identity )
| ( inverse(sk_c1) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_4607,c_168]) ).
tcf(c_5265,plain,
( ( sk_c9 = identity )
| ( inverse(sk_c11) = sk_c9 ) ),
inference(superposition,[status(thm)],[c_4608,c_128]) ).
tcf(c_5300,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(identity,X1) = X2 )
| ( X2 != X0 )
| ( X0 != X1 ) ),
inference(resolution,[status(thm)],[c_2538,c_727]) ).
tcf(c_5369,plain,
( ( sk_c11 = identity )
| ( inverse(sk_c1) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_4609,c_170]) ).
tcf(c_5379,plain,
! [X0: $i,X1: $i] :
( ( X0 = multiply(inverse(X1),X1) )
| ( X0 != identity ) ),
inference(resolution,[status(thm)],[c_2539,c_2543]) ).
tcf(c_5380,plain,
( ( sk_c11 = multiply(inverse(sk_c11),sk_c11) )
| ( sk_c11 != identity ) ),
inference(instantiation,[status(thm)],[c_5379]) ).
tcf(c_5569,plain,
( ( sk_c11 = identity )
| ( inverse(sk_c11) = sk_c9 ) ),
inference(superposition,[status(thm)],[c_4610,c_130]) ).
tcf(c_5938,plain,
! [X0: $i] :
( ( X0 = inverse(sk_c4) )
| ( inverse(sk_c11) = sk_c9 )
| ( X0 != sk_c10 ) ),
inference(resolution,[status(thm)],[c_2467,c_2543]) ).
tcf(c_6253,plain,
( ( multiply(sk_c11,sk_c10) = sk_c9 )
| ( sk_c9 != inverse(sk_c11) )
| ( multiply(sk_c11,sk_c10) != inverse(sk_c11) ) ),
inference(instantiation,[status(thm)],[c_2742]) ).
tcf(c_6254,plain,
( ( sk_c9 = multiply(sk_c11,sk_c10) )
| ( sk_c9 != inverse(sk_c11) )
| ( multiply(sk_c11,sk_c10) != inverse(sk_c11) ) ),
inference(instantiation,[status(thm)],[c_1413]) ).
tcf(c_6513,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(X0,X1)) = X1,
inference(demodulation,[status(thm)],[c_1321,c_113]) ).
tcf(c_6575,plain,
! [X0: $i] : multiply(inverse(inverse(X0)),identity) = X0,
inference(superposition,[status(thm)],[c_114,c_6513]) ).
tcf(c_6576,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(inverse(multiply(X0,X1)),multiply(X0,multiply(X1,X2))) = X2,
inference(superposition,[status(thm)],[c_115,c_6513]) ).
tcf(c_6629,plain,
( ~ iPr_def_10
| ( sk_c10 != identity )
| ( inverse(inverse(sk_c11)) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_114,c_721]) ).
tcf(c_6656,plain,
( ~ iPr_def_12
| ( sk_c9 != identity )
| ( inverse(inverse(sk_c10)) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_114,c_723]) ).
tcf(c_6732,plain,
! [X0: $i] : multiply(inverse(inverse(inverse(X0))),X0) = identity,
inference(superposition,[status(thm)],[c_6575,c_6513]) ).
tcf(c_7307,plain,
! [X0: $i] :
( ( inverse(sk_c11) = X0 )
| ( X0 != multiply(sk_c11,sk_c10) )
| ( inverse(sk_c11) != multiply(sk_c11,sk_c10) ) ),
inference(instantiation,[status(thm)],[c_1135]) ).
tcf(c_7308,plain,
! [X0: $i] :
( ( X0 = inverse(sk_c11) )
| ( X0 != multiply(sk_c11,sk_c10) )
| ( inverse(sk_c11) != multiply(sk_c11,sk_c10) ) ),
inference(instantiation,[status(thm)],[c_1081]) ).
tcf(c_7309,plain,
( ( sk_c11 = inverse(sk_c11) )
| ( sk_c11 != multiply(sk_c11,sk_c10) )
| ( inverse(sk_c11) != multiply(sk_c11,sk_c10) ) ),
inference(instantiation,[status(thm)],[c_7308]) ).
tcf(c_7310,plain,
( ( inverse(sk_c11) = sk_c11 )
| ( sk_c11 != multiply(sk_c11,sk_c10) )
| ( inverse(sk_c11) != multiply(sk_c11,sk_c10) ) ),
inference(instantiation,[status(thm)],[c_7307]) ).
tcf(c_7322,plain,
! [X0: $i] :
( ( X0 = sk_c9 )
| ( sk_c9 != multiply(sk_c11,sk_c10) )
| ( X0 != multiply(sk_c11,sk_c10) ) ),
inference(instantiation,[status(thm)],[c_1409]) ).
tcf(c_7323,plain,
! [X0: $i] :
( ( sk_c9 = X0 )
| ( sk_c9 != multiply(sk_c11,sk_c10) )
| ( X0 != multiply(sk_c11,sk_c10) ) ),
inference(instantiation,[status(thm)],[c_1065]) ).
tcf(c_7325,plain,
( ( sk_c9 = sk_c11 )
| ( sk_c9 != multiply(sk_c11,sk_c10) )
| ( sk_c11 != multiply(sk_c11,sk_c10) ) ),
inference(instantiation,[status(thm)],[c_7323]) ).
tcf(c_7326,plain,
( ( sk_c11 = sk_c9 )
| ( sk_c9 != multiply(sk_c11,sk_c10) )
| ( sk_c11 != multiply(sk_c11,sk_c10) ) ),
inference(instantiation,[status(thm)],[c_7322]) ).
tcf(c_7620,plain,
! [X0: $i] :
( ( X0 = multiply(identity,inverse(sk_c1)) )
| ( X0 != inverse(sk_c1) )
| ( multiply(identity,inverse(sk_c1)) != inverse(sk_c1) ) ),
inference(instantiation,[status(thm)],[c_2631]) ).
tcf(c_7627,plain,
( ( sk_c11 = multiply(identity,inverse(sk_c1)) )
| ( sk_c11 != inverse(sk_c1) )
| ( multiply(identity,inverse(sk_c1)) != inverse(sk_c1) ) ),
inference(instantiation,[status(thm)],[c_7620]) ).
tcf(c_7985,plain,
! [X0: $i,X1: $i] : multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,identity)) = X1,
inference(superposition,[status(thm)],[c_114,c_6576]) ).
tcf(c_8081,plain,
! [X0: $i,X1: $i] : multiply(inverse(multiply(X0,inverse(inverse(inverse(X1))))),multiply(X0,identity)) = X1,
inference(superposition,[status(thm)],[c_6732,c_6576]) ).
tcf(c_8093,plain,
! [X0: $i] : inverse(inverse(X0)) = X0,
inference(demodulation,[status(thm)],[c_8081,c_7985]) ).
tcf(c_8164,plain,
( ~ iPr_def_12
| ( sk_c9 != identity ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_6656,c_8093]) ).
tcf(c_8165,plain,
( ~ iPr_def_10
| ( sk_c10 != identity ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_6629,c_8093]) ).
tcf(c_8166,plain,
inverse(inverse(sk_c11)) = sk_c11,
inference(instantiation,[status(thm)],[c_8093]) ).
tcf(c_8669,plain,
! [X0: $i,X1: $i] :
( ( multiply(X0,X1) = multiply(sk_c3,sk_c11) )
| ( X1 != sk_c11 )
| ( X0 != sk_c3 ) ),
inference(instantiation,[status(thm)],[c_728]) ).
tcf(c_8679,plain,
multiply(sk_c3,sk_c11) = multiply(sk_c3,sk_c11),
inference(instantiation,[status(thm)],[c_726]) ).
tcf(c_9243,plain,
( ( multiply(sk_c9,sk_c10) = multiply(inverse(sk_c11),sk_c10) )
| ( sk_c9 != inverse(sk_c11) )
| ( sk_c10 != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_3268]) ).
tcf(c_9304,plain,
! [X0: $i] :
( ( sk_c10 = multiply(sk_c3,sk_c11) )
| ( multiply(sk_c11,sk_c10) = X0 )
| ( X0 != sk_c9 ) ),
inference(resolution,[status(thm)],[c_3955,c_727]) ).
tcf(c_9324,plain,
( iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( sk_c10 = multiply(sk_c3,sk_c11) )
| ( inverse(sk_c11) != sk_c9 )
| ( multiply(sk_c11,sk_c10) != sk_c9 ) ),
inference(resolution,[status(thm)],[c_3956,c_725]) ).
tcf(c_9381,plain,
( ( identity = sk_c11 )
| ( identity != identity )
| ( sk_c11 != identity ) ),
inference(instantiation,[status(thm)],[c_3280]) ).
tcf(c_9469,plain,
( iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( sk_c9 = multiply(sk_c4,sk_c10) )
| ( inverse(sk_c11) != sk_c9 )
| ( multiply(sk_c11,sk_c10) != sk_c9 ) ),
inference(resolution,[status(thm)],[c_3962,c_725]) ).
tcf(c_9554,plain,
! [X0: $i] :
( ( sk_c11 = multiply(sk_c5,sk_c8) )
| ( multiply(sk_c11,sk_c10) = X0 )
| ( X0 != sk_c9 ) ),
inference(resolution,[status(thm)],[c_3967,c_727]) ).
tcf(c_9795,plain,
( ( sk_c2 = multiply(sk_c1,sk_c11) )
| ( sk_c10 = multiply(sk_c3,sk_c11) ) ),
inference(resolution,[status(thm)],[c_3999,c_2543]) ).
tcf(c_9796,plain,
! [X0: $i] :
( ( sk_c2 = multiply(sk_c1,sk_c11) )
| ( multiply(sk_c3,sk_c11) = X0 )
| ( X0 != sk_c10 ) ),
inference(resolution,[status(thm)],[c_3999,c_727]) ).
tcf(c_9798,plain,
( ( sk_c2 = multiply(sk_c1,sk_c11) )
| ~ iPr_def_10
| ( inverse(sk_c3) != sk_c11 ) ),
inference(resolution,[status(thm)],[c_3999,c_721]) ).
tcf(c_9806,plain,
( ( sk_c2 = multiply(sk_c1,sk_c11) )
| ~ iPr_def_12
| ( inverse(sk_c4) != sk_c10 ) ),
inference(resolution,[status(thm)],[c_4000,c_723]) ).
tcf(c_9811,plain,
( ( sk_c2 = multiply(sk_c1,sk_c11) )
| ( sk_c11 = multiply(sk_c5,sk_c8) ) ),
inference(resolution,[status(thm)],[c_4001,c_2543]) ).
tcf(c_9830,plain,
! [X0: $i,X1: $i] :
( ( multiply(inverse(X0),sk_c10) = sk_c11 )
| ( sk_c11 != X1 )
| ( multiply(inverse(X0),sk_c10) != X1 ) ),
inference(instantiation,[status(thm)],[c_727]) ).
tcf(c_10080,plain,
! [X0: $i] :
( ( identity = inverse(sk_c3) )
| ( identity != X0 )
| ( inverse(sk_c3) != X0 ) ),
inference(instantiation,[status(thm)],[c_1651]) ).
tcf(c_10082,plain,
! [X0: $i] :
( ( X0 = identity )
| ( identity != inverse(sk_c3) )
| ( X0 != inverse(sk_c3) ) ),
inference(instantiation,[status(thm)],[c_2577]) ).
tcf(c_10083,plain,
( ( sk_c11 = identity )
| ( identity != inverse(sk_c3) )
| ( sk_c11 != inverse(sk_c3) ) ),
inference(instantiation,[status(thm)],[c_10082]) ).
tcf(c_10139,plain,
( ( sk_c10 = inverse(sk_c3) )
| ( sk_c10 != inverse(sk_c4) )
| ( inverse(sk_c3) != inverse(sk_c4) ) ),
inference(instantiation,[status(thm)],[c_2092]) ).
tcf(c_10257,plain,
( ( multiply(sk_c11,sk_c10) = sk_c9 )
| ~ iPr_def_10 ),
inference(global_subsumption_just,[status(thm)],[c_2062,c_117,c_2062]) ).
tcf(c_10268,plain,
! [X0: $i] :
( ( multiply(sk_c11,sk_c10) = X0 )
| ~ iPr_def_10
| ( X0 != sk_c9 ) ),
inference(resolution,[status(thm)],[c_10257,c_727]) ).
tcf(c_10273,plain,
( ( multiply(sk_c9,sk_c10) = sk_c11 )
| ~ iPr_def_10 ),
inference(global_subsumption_just,[status(thm)],[c_2063,c_137,c_2063]) ).
tcf(c_10503,plain,
! [X0: $i] :
( ( multiply(sk_c9,sk_c10) = X0 )
| ~ iPr_def_10
| ( X0 != sk_c11 ) ),
inference(resolution,[status(thm)],[c_10273,c_727]) ).
tcf(c_10547,plain,
( ( multiply(sk_c11,sk_c10) = sk_c9 )
| ~ iPr_def_12 ),
inference(global_subsumption_just,[status(thm)],[c_2117,c_119,c_2117]) ).
tcf(c_10557,plain,
( ( sk_c9 = multiply(sk_c11,sk_c10) )
| ~ iPr_def_12 ),
inference(resolution,[status(thm)],[c_10547,c_2543]) ).
tcf(c_10558,plain,
! [X0: $i] :
( ( multiply(sk_c11,sk_c10) = X0 )
| ~ iPr_def_12
| ( X0 != sk_c9 ) ),
inference(resolution,[status(thm)],[c_10547,c_727]) ).
tcf(c_10561,plain,
( ( sk_c10 = multiply(sk_c11,sk_c2) )
| ( sk_c10 != sk_c10 )
| ( multiply(sk_c11,sk_c2) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_4533]) ).
tcf(c_10566,plain,
( ( sk_c10 = multiply(identity,sk_c10) )
| ( sk_c10 != sk_c10 )
| ( multiply(identity,sk_c10) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_4533]) ).
tcf(c_10658,plain,
( ( multiply(sk_c11,sk_c2) = sk_c10 )
| ~ iPr_def_12 ),
inference(global_subsumption_just,[status(thm)],[c_2119,c_149,c_2119]) ).
tcf(c_10680,plain,
( ( sk_c10 = multiply(sk_c11,sk_c2) )
| ~ iPr_def_12 ),
inference(resolution,[status(thm)],[c_10658,c_2543]) ).
tcf(c_10733,plain,
( ( sk_c2 = multiply(sk_c1,sk_c11) )
| ~ iPr_def_10 ),
inference(global_subsumption_just,[status(thm)],[c_9798,c_3994,c_9798]) ).
tcf(c_10739,plain,
( ( sk_c2 = multiply(sk_c1,sk_c11) )
| ~ iPr_def_12 ),
inference(global_subsumption_just,[status(thm)],[c_9806,c_3995,c_9806]) ).
tcf(c_10758,plain,
! [X0: $i] :
( ( multiply(X0,sk_c9) = multiply(identity,inverse(sk_c11)) )
| ( sk_c9 != inverse(sk_c11) )
| ( X0 != identity ) ),
inference(instantiation,[status(thm)],[c_1363]) ).
tcf(c_10759,plain,
( ( multiply(sk_c11,sk_c9) = multiply(identity,inverse(sk_c11)) )
| ( sk_c9 != inverse(sk_c11) )
| ( sk_c11 != identity ) ),
inference(instantiation,[status(thm)],[c_10758]) ).
tcf(c_10765,plain,
! [X0: $i] :
( ( multiply(X0,inverse(sk_c11)) = multiply(identity,inverse(sk_c11)) )
| ( X0 != identity )
| ( inverse(sk_c11) != inverse(sk_c11) ) ),
inference(instantiation,[status(thm)],[c_1363]) ).
tcf(c_10766,plain,
( ( multiply(sk_c11,inverse(sk_c11)) = multiply(identity,inverse(sk_c11)) )
| ( sk_c11 != identity )
| ( inverse(sk_c11) != inverse(sk_c11) ) ),
inference(instantiation,[status(thm)],[c_10765]) ).
tcf(c_11259,plain,
! [X0: $i] :
( ( X0 = multiply(sk_c11,sk_c2) )
| ( inverse(sk_c3) = sk_c11 )
| ( X0 != sk_c10 ) ),
inference(resolution,[status(thm)],[c_2502,c_2543]) ).
tcf(c_11512,plain,
! [X0: $i] :
( ( X0 = multiply(sk_c1,sk_c11) )
| ( inverse(sk_c4) = sk_c10 )
| ( X0 != sk_c2 ) ),
inference(resolution,[status(thm)],[c_2513,c_2543]) ).
tcf(c_11513,plain,
( ( sk_c11 = multiply(sk_c1,sk_c11) )
| ( inverse(sk_c4) = sk_c10 )
| ( sk_c11 != sk_c2 ) ),
inference(instantiation,[status(thm)],[c_11512]) ).
tcf(c_11676,plain,
! [X0: $i] :
( ( X0 = multiply(sk_c1,sk_c11) )
| ( inverse(sk_c5) = sk_c8 )
| ( X0 != sk_c2 ) ),
inference(resolution,[status(thm)],[c_2514,c_2543]) ).
tcf(c_11677,plain,
( ( sk_c11 = multiply(sk_c1,sk_c11) )
| ( inverse(sk_c5) = sk_c8 )
| ( sk_c11 != sk_c2 ) ),
inference(instantiation,[status(thm)],[c_11676]) ).
tcf(c_11895,plain,
( ( sk_c10 = sk_c9 )
| ( sk_c9 != inverse(sk_c4) )
| ( sk_c10 != inverse(sk_c4) ) ),
inference(instantiation,[status(thm)],[c_4524]) ).
tcf(c_12106,plain,
! [X0: $i,X1: $i] :
( ( multiply(sk_c3,sk_c11) = X0 )
| ( multiply(sk_c11,sk_c2) = sk_c10 )
| ( X1 != sk_c10 )
| ( X0 != X1 ) ),
inference(resolution,[status(thm)],[c_2450,c_727]) ).
tcf(c_12343,plain,
! [X0: $i,X1: $i] :
( ( inverse(sk_c3) = sk_c11 )
| ( inverse(X1) = multiply(sk_c11,sk_c10) )
| ( X1 != X0 )
| ( inverse(X0) != sk_c9 ) ),
inference(resolution,[status(thm)],[c_2544,c_2436]) ).
tcf(c_12352,plain,
( ( inverse(sk_c3) = sk_c11 )
| ( inverse(sk_c11) = multiply(sk_c11,sk_c10) )
| ( sk_c11 != sk_c11 )
| ( inverse(sk_c11) != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_12343]) ).
tcf(c_13959,plain,
! [X0: $i,X1: $i] :
( ( multiply(sk_c1,sk_c11) = X0 )
| ( multiply(sk_c3,sk_c11) = sk_c10 )
| ( X1 != sk_c2 )
| ( X0 != X1 ) ),
inference(resolution,[status(thm)],[c_2517,c_727]) ).
tcf(c_14004,plain,
! [X0: $i,X1: $i] :
( ( multiply(sk_c1,sk_c11) = X0 )
| ( multiply(sk_c4,sk_c10) = sk_c9 )
| ( X1 != sk_c2 )
| ( X0 != X1 ) ),
inference(resolution,[status(thm)],[c_2518,c_727]) ).
tcf(c_14247,plain,
( ( inverse(sk_c11) = sk_c3 )
| ( inverse(sk_c11) = sk_c9 ) ),
inference(superposition,[status(thm)],[c_127,c_8093]) ).
tcf(c_14256,plain,
! [X0: $i] : multiply(X0,inverse(X0)) = identity,
inference(superposition,[status(thm)],[c_8093,c_114]) ).
tcf(c_14314,plain,
( ( inverse(sk_c11) = sk_c9 )
| ( multiply(sk_c3,sk_c11) = identity ) ),
inference(superposition,[status(thm)],[c_14247,c_114]) ).
tcf(c_14520,plain,
( ( multiply(sk_c1,sk_c11) = sk_c2 )
| ~ iPr_def_12
| ( inverse(sk_c4) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_158,c_723]) ).
tcf(c_14571,plain,
! [X0: $i,X1: $i] :
( ~ iPr_def_11
| ( inverse(X1) != X0 )
| ( multiply(inverse(X1),sk_c10) != sk_c11 )
| ( multiply(X1,inverse(X1)) != sk_c11 )
| ( multiply(X0,inverse(X1)) != inverse(X0) ) ),
inference(light_normalisation,[status(thm)],[c_722,c_8093]) ).
tcf(c_14638,plain,
! [X0: $i,X1: $i] :
( ~ iPr_def_11
| ( sk_c11 != identity )
| ( inverse(X1) != X0 )
| ( multiply(inverse(X1),sk_c10) != sk_c11 )
| ( multiply(X0,inverse(X1)) != inverse(X0) ) ),
inference(demodulation,[status(thm)],[c_14571,c_14256]) ).
tcf(c_14639,plain,
( ~ iPr_def_11
| ( sk_c11 != identity )
| ( inverse(sk_c11) != sk_c11 )
| ( multiply(sk_c11,inverse(sk_c11)) != inverse(sk_c11) )
| ( multiply(inverse(sk_c11),sk_c10) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_14638]) ).
tcf(c_14642,plain,
( ( inverse(sk_c1) = sk_c11 )
| ( multiply(sk_c3,sk_c11) = identity ) ),
inference(superposition,[status(thm)],[c_167,c_14256]) ).
tcf(c_14662,plain,
! [X0: $i,X1: $i] : multiply(X0,multiply(X1,inverse(multiply(X0,X1)))) = identity,
inference(superposition,[status(thm)],[c_14256,c_115]) ).
tcf(c_14735,plain,
( ( sk_c10 = identity )
| ( inverse(sk_c1) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_14642,c_166]) ).
tcf(c_14745,plain,
( ( sk_c10 = identity )
| ( multiply(sk_c11,sk_c1) = identity ) ),
inference(superposition,[status(thm)],[c_14735,c_114]) ).
tcf(c_14861,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(X0,X1)) = X1,
inference(demodulation,[status(thm)],[c_1321,c_113]) ).
tcf(c_14945,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(inverse(multiply(X0,X1)),multiply(X0,multiply(X1,X2))) = X2,
inference(superposition,[status(thm)],[c_115,c_14861]) ).
tcf(c_15125,plain,
( ( sk_c10 = identity )
| ( inverse(sk_c11) = sk_c9 ) ),
inference(superposition,[status(thm)],[c_14314,c_126]) ).
tcf(c_15140,plain,
! [X0: $i] :
( ( sk_c10 = identity )
| ( multiply(sk_c9,multiply(sk_c11,X0)) = X0 ) ),
inference(superposition,[status(thm)],[c_15125,c_14861]) ).
tcf(c_15171,plain,
( ( sk_c10 = identity )
| ( multiply(sk_c9,identity) = sk_c1 ) ),
inference(superposition,[status(thm)],[c_14745,c_15140]) ).
tcf(c_15181,plain,
! [X0: $i] :
( ( sk_c10 = identity )
| ( multiply(sk_c9,multiply(identity,X0)) = multiply(sk_c1,X0) ) ),
inference(superposition,[status(thm)],[c_15171,c_115]) ).
tcf(c_15509,plain,
! [X0: $i] : multiply(X0,inverse(multiply(X0,identity))) = identity,
inference(superposition,[status(thm)],[c_113,c_14662]) ).
tcf(c_15690,plain,
! [X0: $i,X1: $i] : multiply(multiply(X0,X1),inverse(multiply(X0,multiply(X1,identity)))) = identity,
inference(superposition,[status(thm)],[c_115,c_15509]) ).
tcf(c_17509,plain,
! [X0: $i] :
( ( sk_c10 = X0 )
| ( sk_c10 != multiply(sk_c11,sk_c2) )
| ( X0 != multiply(sk_c11,sk_c2) ) ),
inference(instantiation,[status(thm)],[c_2275]) ).
tcf(c_17510,plain,
! [X0: $i] :
( ( X0 = sk_c10 )
| ( sk_c10 != multiply(sk_c11,sk_c2) )
| ( X0 != multiply(sk_c11,sk_c2) ) ),
inference(instantiation,[status(thm)],[c_1387]) ).
tcf(c_17576,plain,
multiply(inverse(sk_c10),sk_c10) = identity,
inference(instantiation,[status(thm)],[c_114]) ).
tcf(c_17578,plain,
! [X0: $i] : multiply(inverse(X0),sk_c10) = multiply(inverse(X0),sk_c10),
inference(instantiation,[status(thm)],[c_726]) ).
tcf(c_17580,plain,
multiply(inverse(sk_c11),sk_c10) = multiply(inverse(sk_c11),sk_c10),
inference(instantiation,[status(thm)],[c_17578]) ).
tcf(c_17581,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(inverse(X0),sk_c10) = X2 )
| ( X2 != X1 )
| ( multiply(inverse(X0),sk_c10) != X1 ) ),
inference(instantiation,[status(thm)],[c_727]) ).
tcf(c_17582,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(inverse(X0),sk_c10) = sk_c11 )
| ( sk_c11 != multiply(X1,X2) )
| ( multiply(inverse(X0),sk_c10) != multiply(X1,X2) ) ),
inference(instantiation,[status(thm)],[c_9830]) ).
tcf(c_17583,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(inverse(X0),sk_c10) = multiply(X1,X2) )
| ( sk_c10 != X2 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_728]) ).
tcf(c_17584,plain,
( ( multiply(inverse(sk_c11),sk_c10) = sk_c11 )
| ( sk_c11 != multiply(sk_c11,sk_c11) )
| ( multiply(inverse(sk_c11),sk_c10) != multiply(sk_c11,sk_c11) ) ),
inference(instantiation,[status(thm)],[c_17582]) ).
tcf(c_17585,plain,
( ( multiply(inverse(sk_c11),sk_c10) = multiply(sk_c11,sk_c11) )
| ( sk_c10 != sk_c11 )
| ( inverse(sk_c11) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_17583]) ).
tcf(c_17593,plain,
( ( multiply(sk_c11,sk_c10) = inverse(sk_c11) )
| ( inverse(sk_c11) != multiply(sk_c11,sk_c10) )
| ( multiply(sk_c11,sk_c10) != multiply(sk_c11,sk_c10) ) ),
inference(instantiation,[status(thm)],[c_7308]) ).
tcf(c_17594,plain,
multiply(sk_c11,sk_c10) = multiply(sk_c11,sk_c10),
inference(instantiation,[status(thm)],[c_726]) ).
tcf(c_17595,plain,
! [X0: $i,X1: $i] :
( ( X1 = multiply(sk_c11,sk_c10) )
| ( X1 != X0 )
| ( multiply(sk_c11,sk_c10) != X0 ) ),
inference(instantiation,[status(thm)],[c_727]) ).
tcf(c_17596,plain,
( ( sk_c11 = multiply(sk_c11,sk_c10) )
| ( sk_c11 != sk_c11 )
| ( multiply(sk_c11,sk_c10) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_17595]) ).
tcf(c_17597,plain,
! [X0: $i,X1: $i] :
( ( multiply(X0,X1) = inverse(sk_c11) )
| ( inverse(sk_c11) != multiply(sk_c11,sk_c10) )
| ( multiply(X0,X1) != multiply(sk_c11,sk_c10) ) ),
inference(instantiation,[status(thm)],[c_7308]) ).
tcf(c_17598,plain,
! [X0: $i,X1: $i] :
( ( multiply(X0,X1) = multiply(sk_c11,sk_c10) )
| ( X1 != sk_c10 )
| ( X0 != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_728]) ).
tcf(c_17599,plain,
( ( multiply(sk_c11,sk_c11) = inverse(sk_c11) )
| ( inverse(sk_c11) != multiply(sk_c11,sk_c10) )
| ( multiply(sk_c11,sk_c11) != multiply(sk_c11,sk_c10) ) ),
inference(instantiation,[status(thm)],[c_17597]) ).
tcf(c_17600,plain,
( ( multiply(sk_c11,sk_c11) = multiply(sk_c11,sk_c10) )
| ( sk_c11 != sk_c10 )
| ( sk_c11 != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_17598]) ).
tcf(c_17678,plain,
! [X0: $i,X1: $i] :
( ( inverse(sk_c3) = sk_c11 )
| ( multiply(X1,X0) = sk_c10 )
| ( X1 != sk_c11 )
| ( X0 != sk_c2 ) ),
inference(resolution,[status(thm)],[c_3942,c_3989]) ).
tcf(c_17687,plain,
( ( inverse(sk_c3) = sk_c11 )
| ( multiply(sk_c11,sk_c11) = sk_c10 )
| ( sk_c11 != sk_c2 )
| ( sk_c11 != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_17678]) ).
tcf(c_19019,plain,
multiply(identity,inverse(sk_c1)) = inverse(sk_c1),
inference(instantiation,[status(thm)],[c_1079]) ).
tcf(c_19073,plain,
! [X0: $i,X1: $i] :
( ( multiply(X0,X1) = multiply(identity,inverse(sk_c1)) )
| ( X1 != inverse(sk_c1) )
| ( X0 != identity ) ),
inference(instantiation,[status(thm)],[c_1448]) ).
tcf(c_19074,plain,
( ( multiply(sk_c11,sk_c11) = multiply(identity,inverse(sk_c1)) )
| ( sk_c11 != identity )
| ( sk_c11 != inverse(sk_c1) ) ),
inference(instantiation,[status(thm)],[c_19073]) ).
tcf(c_19740,plain,
( ( multiply(sk_c9,sk_c10) = multiply(identity,sk_c10) )
| ( sk_c9 != identity )
| ( sk_c10 != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_3268]) ).
tcf(c_19742,plain,
( ( sk_c9 = inverse(sk_c11) )
| ( sk_c9 != identity )
| ( inverse(sk_c11) != identity ) ),
inference(instantiation,[status(thm)],[c_1050]) ).
tcf(c_19780,plain,
! [X0: $i] :
( ( X0 = multiply(sk_c4,sk_c10) )
| ( X0 != identity )
| ( multiply(sk_c4,sk_c10) != identity ) ),
inference(instantiation,[status(thm)],[c_3315]) ).
tcf(c_19783,plain,
( ( sk_c11 = multiply(sk_c4,sk_c10) )
| ( sk_c11 != identity )
| ( multiply(sk_c4,sk_c10) != identity ) ),
inference(instantiation,[status(thm)],[c_19780]) ).
tcf(c_19796,plain,
( ( sk_c11 = sk_c4 )
| ( sk_c4 != identity )
| ( sk_c11 != identity ) ),
inference(instantiation,[status(thm)],[c_4159]) ).
tcf(c_19826,plain,
( ( multiply(sk_c1,sk_c11) = sk_c2 )
| ~ iPr_def_12 ),
inference(global_subsumption_just,[status(thm)],[c_14520,c_159,c_3241]) ).
tcf(c_19849,plain,
! [X0: $i,X1: $i] : multiply(X0,multiply(X1,inverse(multiply(X0,multiply(X1,identity))))) = identity,
inference(demodulation,[status(thm)],[c_15690,c_115]) ).
tcf(c_19907,plain,
! [X0: $i,X1: $i] : multiply(X0,inverse(multiply(X1,multiply(X0,identity)))) = multiply(inverse(X1),identity),
inference(superposition,[status(thm)],[c_19849,c_14861]) ).
tcf(c_19912,plain,
! [X0: $i,X1: $i] : multiply(inverse(multiply(X0,X1)),identity) = inverse(multiply(X0,multiply(X1,identity))),
inference(superposition,[status(thm)],[c_19849,c_14945]) ).
tcf(c_19941,plain,
! [X0: $i,X1: $i] : multiply(X0,multiply(inverse(multiply(X1,X0)),identity)) = multiply(inverse(X1),identity),
inference(demodulation,[status(thm)],[c_19907,c_19912]) ).
tcf(c_19997,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(X2,X0) = X1 )
| ( X2 != identity )
| ( X0 != X1 ) ),
inference(resolution,[status(thm)],[c_4010,c_3942]) ).
tcf(c_19998,plain,
( ( multiply(sk_c11,sk_c11) = sk_c11 )
| ( sk_c11 != identity )
| ( sk_c11 != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_19997]) ).
tcf(c_20006,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(X2,X0) = identity )
| ( X2 != inverse(X1) )
| ( X0 != X1 ) ),
inference(resolution,[status(thm)],[c_4012,c_3942]) ).
tcf(c_20007,plain,
( ( multiply(sk_c11,sk_c11) = identity )
| ( sk_c11 != sk_c11 )
| ( sk_c11 != inverse(sk_c11) ) ),
inference(instantiation,[status(thm)],[c_20006]) ).
tcf(c_20036,plain,
( ( inverse(sk_c3) = sk_c11 )
| iPr_def_10
| iPr_def_11
| iPr_def_12 ),
inference(global_subsumption_just,[status(thm)],[c_2267,c_167,c_127,c_147,c_117,c_2267,c_3690]) ).
tcf(c_20037,plain,
( iPr_def_12
| iPr_def_11
| iPr_def_10
| ( inverse(sk_c3) = sk_c11 ) ),
inference(renaming,[status(thm)],[c_20036]) ).
tcf(c_20055,plain,
! [X0: $i] :
( iPr_def_12
| iPr_def_11
| iPr_def_10
| ( inverse(sk_c3) = X0 )
| ( X0 != sk_c11 ) ),
inference(resolution,[status(thm)],[c_20037,c_727]) ).
tcf(c_20056,plain,
( ( inverse(sk_c4) = sk_c10 )
| iPr_def_10
| iPr_def_11
| iPr_def_12 ),
inference(global_subsumption_just,[status(thm)],[c_2268,c_169,c_129,c_149,c_139,c_3689,c_3707]) ).
tcf(c_20057,plain,
( iPr_def_12
| iPr_def_11
| iPr_def_10
| ( inverse(sk_c4) = sk_c10 ) ),
inference(renaming,[status(thm)],[c_20056]) ).
tcf(c_20385,plain,
( iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( sk_c10 = multiply(sk_c3,sk_c11) ) ),
inference(global_subsumption_just,[status(thm)],[c_9324,c_725,c_3956,c_3955,c_3953]) ).
tcf(c_20397,plain,
( iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( sk_c9 = multiply(sk_c4,sk_c10) ) ),
inference(global_subsumption_just,[status(thm)],[c_9469,c_725,c_3962,c_3961,c_3959]) ).
tcf(c_20743,plain,
! [X0: $i] :
( ( inverse(sk_c11) = identity )
| ( identity != X0 )
| ( inverse(sk_c11) != X0 ) ),
inference(instantiation,[status(thm)],[c_2577]) ).
tcf(c_20751,plain,
( ( inverse(sk_c11) = identity )
| ( identity != sk_c11 )
| ( inverse(sk_c11) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_20743]) ).
tcf(c_20752,plain,
! [X0: $i] :
( ( sk_c9 = identity )
| ( identity != X0 )
| ( sk_c9 != X0 ) ),
inference(instantiation,[status(thm)],[c_2577]) ).
tcf(c_20753,plain,
! [X0: $i] :
( ( X0 = sk_c9 )
| ( sk_c9 != identity )
| ( X0 != identity ) ),
inference(instantiation,[status(thm)],[c_1409]) ).
tcf(c_20754,plain,
! [X0: $i] :
( ( sk_c9 = X0 )
| ( sk_c9 != identity )
| ( X0 != identity ) ),
inference(instantiation,[status(thm)],[c_1065]) ).
tcf(c_20756,plain,
( ( sk_c9 = identity )
| ( identity != sk_c11 )
| ( sk_c9 != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_20752]) ).
tcf(c_20757,plain,
( ( sk_c9 = sk_c11 )
| ( sk_c9 != identity )
| ( sk_c11 != identity ) ),
inference(instantiation,[status(thm)],[c_20754]) ).
tcf(c_20758,plain,
( ( sk_c11 = sk_c9 )
| ( sk_c9 != identity )
| ( sk_c11 != identity ) ),
inference(instantiation,[status(thm)],[c_20753]) ).
tcf(c_20774,plain,
! [X0: $i] :
( ( sk_c10 = identity )
| ( identity != X0 )
| ( sk_c10 != X0 ) ),
inference(instantiation,[status(thm)],[c_2577]) ).
tcf(c_20775,plain,
! [X0: $i] :
( ( sk_c10 = X0 )
| ( sk_c10 != identity )
| ( X0 != identity ) ),
inference(instantiation,[status(thm)],[c_2275]) ).
tcf(c_20776,plain,
! [X0: $i] :
( ( X0 = sk_c10 )
| ( sk_c10 != identity )
| ( X0 != identity ) ),
inference(instantiation,[status(thm)],[c_1387]) ).
tcf(c_20778,plain,
( ( sk_c11 = sk_c10 )
| ( sk_c10 != identity )
| ( sk_c11 != identity ) ),
inference(instantiation,[status(thm)],[c_20776]) ).
tcf(c_20779,plain,
( ( sk_c10 = sk_c11 )
| ( sk_c10 != identity )
| ( sk_c11 != identity ) ),
inference(instantiation,[status(thm)],[c_20775]) ).
tcf(c_20802,plain,
( ( inverse(sk_c3) = inverse(sk_c4) )
| ( inverse(sk_c4) != identity )
| ( inverse(sk_c3) != identity ) ),
inference(instantiation,[status(thm)],[c_4302]) ).
tcf(c_20867,plain,
! [X0: $i,X1: $i] :
( ( inverse(sk_c11) = sk_c9 )
| ( inverse(X0) = X1 )
| ( X1 != sk_c10 )
| ( X0 != sk_c4 ) ),
inference(resolution,[status(thm)],[c_5938,c_2544]) ).
tcf(c_20868,plain,
( ( inverse(sk_c11) = sk_c9 )
| ( inverse(sk_c11) = sk_c11 )
| ( sk_c11 != sk_c4 )
| ( sk_c11 != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_20867]) ).
tcf(c_21341,plain,
! [X0: $i] :
( ( sk_c2 = X0 )
| ~ iPr_def_10
| ( X0 != multiply(sk_c1,sk_c11) ) ),
inference(resolution,[status(thm)],[c_10733,c_727]) ).
tcf(c_21585,plain,
! [X0: $i] :
( iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( sk_c10 = X0 )
| ( X0 != multiply(sk_c3,sk_c11) ) ),
inference(resolution,[status(thm)],[c_20385,c_727]) ).
tcf(c_22080,plain,
! [X0: $i] :
( ( multiply(X0,sk_c9) = inverse(sk_c11) )
| ( inverse(sk_c11) != multiply(identity,inverse(sk_c11)) )
| ( multiply(X0,sk_c9) != multiply(identity,inverse(sk_c11)) ) ),
inference(instantiation,[status(thm)],[c_1113]) ).
tcf(c_22082,plain,
( ( multiply(sk_c11,sk_c9) = inverse(sk_c11) )
| ( inverse(sk_c11) != multiply(identity,inverse(sk_c11)) )
| ( multiply(sk_c11,sk_c9) != multiply(identity,inverse(sk_c11)) ) ),
inference(instantiation,[status(thm)],[c_22080]) ).
tcf(c_22518,plain,
! [X0: $i] :
( ( multiply(X0,inverse(sk_c11)) = inverse(sk_c11) )
| ( inverse(sk_c11) != multiply(identity,inverse(sk_c11)) )
| ( multiply(X0,inverse(sk_c11)) != multiply(identity,inverse(sk_c11)) ) ),
inference(instantiation,[status(thm)],[c_1113]) ).
tcf(c_22520,plain,
( ( multiply(sk_c11,inverse(sk_c11)) = inverse(sk_c11) )
| ( inverse(sk_c11) != multiply(identity,inverse(sk_c11)) )
| ( multiply(sk_c11,inverse(sk_c11)) != multiply(identity,inverse(sk_c11)) ) ),
inference(instantiation,[status(thm)],[c_22518]) ).
tcf(c_22911,plain,
( ( multiply(sk_c9,sk_c10) = sk_c10 )
| ( sk_c10 != multiply(identity,sk_c10) )
| ( multiply(sk_c9,sk_c10) != multiply(identity,sk_c10) ) ),
inference(instantiation,[status(thm)],[c_3187]) ).
tcf(c_23012,plain,
! [X0: $i] :
( ( sk_c10 = identity )
| ( multiply(sk_c9,X0) = multiply(sk_c1,X0) ) ),
inference(light_normalisation,[status(thm)],[c_15181,c_113]) ).
tcf(c_23042,plain,
( ( sk_c10 = identity )
| ~ iPr_def_10
| ( inverse(sk_c1) != sk_c11 )
| ( multiply(sk_c9,sk_c11) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_23012,c_721]) ).
tcf(c_24110,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( ( multiply(identity,X2) = multiply(X3,X4) )
| ( X4 != X1 )
| ( X3 != X0 )
| ( multiply(X0,X1) != X2 ) ),
inference(resolution,[status(thm)],[c_5300,c_728]) ).
tcf(c_24111,plain,
( ( multiply(identity,sk_c11) = multiply(sk_c11,sk_c11) )
| ( sk_c11 != sk_c11 )
| ( multiply(sk_c11,sk_c11) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_24110]) ).
tcf(c_24329,plain,
( ( identity = inverse(sk_c3) )
| ( identity != identity )
| ( inverse(sk_c3) != identity ) ),
inference(instantiation,[status(thm)],[c_10080]) ).
tcf(c_26389,plain,
! [X0: $i] :
( ( multiply(inverse(sk_c10),sk_c10) = X0 )
| ( X0 != identity )
| ( multiply(inverse(sk_c10),sk_c10) != identity ) ),
inference(instantiation,[status(thm)],[c_17581]) ).
tcf(c_26390,plain,
! [X0: $i,X1: $i] :
( ( multiply(inverse(X0),sk_c10) = X1 )
| ( X1 != multiply(inverse(X0),sk_c10) )
| ( multiply(inverse(X0),sk_c10) != multiply(inverse(X0),sk_c10) ) ),
inference(instantiation,[status(thm)],[c_17581]) ).
tcf(c_26517,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( sk_c11 = multiply(X0,X1) )
| ( sk_c11 != X2 )
| ( multiply(X0,X1) != X2 ) ),
inference(instantiation,[status(thm)],[c_727]) ).
tcf(c_26518,plain,
( ( sk_c11 = multiply(sk_c11,sk_c11) )
| ( sk_c11 != sk_c11 )
| ( multiply(sk_c11,sk_c11) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_26517]) ).
tcf(c_26763,plain,
! [X0: $i,X1: $i] :
( ( sk_c10 = multiply(X0,X1) )
| ( sk_c10 != multiply(sk_c11,sk_c2) )
| ( multiply(X0,X1) != multiply(sk_c11,sk_c2) ) ),
inference(instantiation,[status(thm)],[c_17509]) ).
tcf(c_26764,plain,
! [X0: $i,X1: $i] :
( ( multiply(X0,X1) = multiply(sk_c11,sk_c2) )
| ( X1 != sk_c2 )
| ( X0 != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_728]) ).
tcf(c_26765,plain,
( ( sk_c10 = multiply(sk_c11,sk_c11) )
| ( sk_c10 != multiply(sk_c11,sk_c2) )
| ( multiply(sk_c11,sk_c11) != multiply(sk_c11,sk_c2) ) ),
inference(instantiation,[status(thm)],[c_26763]) ).
tcf(c_26766,plain,
( ( multiply(sk_c11,sk_c11) = multiply(sk_c11,sk_c2) )
| ( sk_c11 != sk_c2 )
| ( sk_c11 != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_26764]) ).
tcf(c_27297,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = multiply(sk_c11,sk_c10) )
| ( X2 != multiply(X0,X1) )
| ( multiply(sk_c11,sk_c10) != multiply(X0,X1) ) ),
inference(instantiation,[status(thm)],[c_17595]) ).
tcf(c_27298,plain,
! [X0: $i,X1: $i] :
( ( multiply(sk_c11,sk_c10) = multiply(X0,X1) )
| ( sk_c10 != X1 )
| ( sk_c11 != X0 ) ),
inference(instantiation,[status(thm)],[c_728]) ).
tcf(c_27299,plain,
( ( sk_c11 = multiply(sk_c11,sk_c10) )
| ( sk_c11 != multiply(sk_c11,sk_c11) )
| ( multiply(sk_c11,sk_c10) != multiply(sk_c11,sk_c11) ) ),
inference(instantiation,[status(thm)],[c_27297]) ).
tcf(c_27300,plain,
( ( multiply(sk_c11,sk_c10) = multiply(sk_c11,sk_c11) )
| ( sk_c10 != sk_c11 )
| ( sk_c11 != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_27298]) ).
tcf(c_30320,plain,
( ( inverse(sk_c10) = sk_c4 )
| ( inverse(sk_c11) = sk_c9 ) ),
inference(superposition,[status(thm)],[c_129,c_8093]) ).
tcf(c_30323,plain,
( ( inverse(sk_c1) = sk_c11 )
| ( inverse(sk_c6) = sk_c7 ) ),
inference(superposition,[status(thm)],[c_173,c_8093]) ).
tcf(c_30328,plain,
! [X0: $i] : multiply(X0,inverse(X0)) = identity,
inference(superposition,[status(thm)],[c_8093,c_114]) ).
tcf(c_30338,plain,
( ( inverse(sk_c5) = sk_c8 )
| ( multiply(sk_c10,multiply(inverse(sk_c9),identity)) = multiply(inverse(sk_c11),identity) ) ),
inference(superposition,[status(thm)],[c_121,c_19941]) ).
tcf(c_30367,plain,
( ( inverse(sk_c1) = sk_c11 )
| ( multiply(sk_c3,sk_c11) = identity ) ),
inference(superposition,[status(thm)],[c_167,c_30328]) ).
tcf(c_30369,plain,
( ( inverse(sk_c1) = sk_c11 )
| ( multiply(sk_c4,sk_c10) = identity ) ),
inference(superposition,[status(thm)],[c_169,c_30328]) ).
tcf(c_30371,plain,
( ( inverse(sk_c1) = sk_c11 )
| ( multiply(sk_c5,sk_c8) = identity ) ),
inference(superposition,[status(thm)],[c_171,c_30328]) ).
tcf(c_30467,plain,
( ( multiply(sk_c11,sk_c10) = sk_c9 )
| ( multiply(sk_c10,multiply(inverse(sk_c9),identity)) = multiply(inverse(sk_c4),identity) ) ),
inference(superposition,[status(thm)],[c_118,c_19941]) ).
tcf(c_30507,plain,
! [X0: $i,X1: $i] : multiply(X0,multiply(inverse(X0),X1)) = multiply(identity,X1),
inference(superposition,[status(thm)],[c_30328,c_115]) ).
tcf(c_30513,plain,
! [X0: $i,X1: $i] : multiply(X0,multiply(X1,inverse(multiply(X0,X1)))) = identity,
inference(superposition,[status(thm)],[c_115,c_30328]) ).
tcf(c_30552,plain,
! [X0: $i,X1: $i] : multiply(X0,multiply(inverse(X0),X1)) = X1,
inference(demodulation,[status(thm)],[c_30507,c_113]) ).
tcf(c_30555,plain,
! [X0: $i] : multiply(X0,identity) = X0,
inference(superposition,[status(thm)],[c_114,c_30552]) ).
tcf(c_30560,plain,
! [X0: $i] :
( ( inverse(sk_c11) = sk_c9 )
| ( multiply(sk_c3,multiply(sk_c11,X0)) = X0 ) ),
inference(superposition,[status(thm)],[c_127,c_30552]) ).
tcf(c_30570,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(X0,X1)) = X1,
inference(superposition,[status(thm)],[c_8093,c_30552]) ).
tcf(c_30576,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(X0,multiply(X1,multiply(inverse(multiply(X0,X1)),X2))) = X2,
inference(superposition,[status(thm)],[c_30552,c_115]) ).
tcf(c_30641,plain,
( ( multiply(sk_c1,sk_c11) = sk_c2 )
| ( multiply(sk_c11,multiply(inverse(sk_c10),identity)) = multiply(inverse(sk_c3),identity) ) ),
inference(superposition,[status(thm)],[c_156,c_19941]) ).
tcf(c_30660,plain,
! [X0: $i] :
( ( inverse(sk_c11) = sk_c9 )
| ( multiply(inverse(sk_c11),X0) = multiply(sk_c3,X0) ) ),
inference(superposition,[status(thm)],[c_30552,c_30560]) ).
tcf(c_30752,plain,
( ( inverse(sk_c5) = sk_c8 )
| ~ iPr_def_12
| ( sk_c11 != sk_c9 )
| ( inverse(sk_c9) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_141,c_723]) ).
tcf(c_30753,plain,
( ( inverse(sk_c4) = sk_c10 )
| ~ iPr_def_12
| ( sk_c11 != sk_c9 )
| ( inverse(sk_c9) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_139,c_723]) ).
tcf(c_30754,plain,
( ( inverse(sk_c3) = sk_c11 )
| ~ iPr_def_12
| ( sk_c11 != sk_c9 )
| ( inverse(sk_c9) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_137,c_723]) ).
tcf(c_30762,plain,
( ~ iPr_def_13
| ( sk_c11 != sk_c10 )
| ( inverse(inverse(sk_c11)) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_30552,c_724]) ).
tcf(c_30763,plain,
( ( multiply(sk_c1,sk_c11) = sk_c2 )
| ~ iPr_def_13
| ( inverse(sk_c3) != sk_c11 )
| ( multiply(sk_c11,sk_c10) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_156,c_724]) ).
tcf(c_30764,plain,
( ( multiply(sk_c11,sk_c2) = sk_c10 )
| ~ iPr_def_13
| ( inverse(sk_c3) != sk_c11 )
| ( multiply(sk_c11,sk_c10) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_146,c_724]) ).
tcf(c_30766,plain,
( ( multiply(sk_c11,sk_c10) = sk_c9 )
| ~ iPr_def_13
| ( inverse(sk_c3) != sk_c11 )
| ( multiply(sk_c11,sk_c10) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_116,c_724]) ).
tcf(c_30773,plain,
( ( inverse(sk_c5) = sk_c8 )
| ~ iPr_def_13
| ( inverse(sk_c1) != sk_c11 )
| ( multiply(sk_c11,sk_c2) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_161,c_724]) ).
tcf(c_30781,plain,
( ~ iPr_def_13
| ( sk_c11 != sk_c10 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_30762,c_8093]) ).
tcf(c_30795,plain,
! [X0: $i,X1: $i] :
( ~ iPr_def_11
| ( inverse(X1) != X0 )
| ( multiply(inverse(X1),sk_c10) != sk_c11 )
| ( multiply(X1,inverse(X1)) != sk_c11 )
| ( multiply(X0,inverse(X1)) != inverse(X0) ) ),
inference(light_normalisation,[status(thm)],[c_722,c_8093]) ).
tcf(c_30796,plain,
! [X0: $i,X1: $i] :
( ~ iPr_def_11
| ( sk_c11 != identity )
| ( inverse(X1) != X0 )
| ( multiply(inverse(X1),sk_c10) != sk_c11 )
| ( multiply(X0,inverse(X1)) != inverse(X0) ) ),
inference(demodulation,[status(thm)],[c_30795,c_30328]) ).
tcf(c_30807,plain,
! [X0: $i] :
( ~ iPr_def_11
| ( sk_c11 != identity )
| ( inverse(X0) != identity )
| ( inverse(X0) != inverse(identity) )
| ( multiply(inverse(X0),sk_c10) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_113,c_30796]) ).
tcf(c_30822,plain,
! [X0: $i,X1: $i] :
( ~ iPr_def_11
| ( sk_c11 != identity )
| ( inverse(inverse(X0)) != X1 )
| ( multiply(X1,X0) != inverse(X1) )
| ( multiply(inverse(inverse(X0)),sk_c10) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_8093,c_30796]) ).
tcf(c_30827,plain,
( ~ iPr_def_11
| ( sk_c11 != identity )
| ( inverse(sk_c11) != identity )
| ( inverse(sk_c11) != inverse(identity) )
| ( multiply(inverse(sk_c11),sk_c10) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_30807]) ).
tcf(c_30829,plain,
( ~ iPr_def_11
| ( sk_c11 != identity )
| ( inverse(inverse(sk_c11)) != sk_c11 )
| ( multiply(sk_c11,sk_c11) != inverse(sk_c11) )
| ( multiply(inverse(inverse(sk_c11)),sk_c10) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_30822]) ).
tcf(c_30926,plain,
( ( sk_c8 = sk_c7 )
| ( inverse(sk_c1) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_30323,c_174]) ).
tcf(c_30938,plain,
( ( sk_c8 = sk_c7 )
| ( multiply(sk_c1,sk_c11) = identity ) ),
inference(superposition,[status(thm)],[c_30926,c_30328]) ).
tcf(c_31078,plain,
( ( sk_c10 = identity )
| ( inverse(sk_c1) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_30367,c_166]) ).
tcf(c_31087,plain,
( ( sk_c10 = identity )
| ( multiply(sk_c1,sk_c11) = identity ) ),
inference(superposition,[status(thm)],[c_31078,c_30328]) ).
tcf(c_31130,plain,
( ( sk_c2 = identity )
| ( sk_c8 = sk_c7 )
| ( inverse(sk_c5) = sk_c8 ) ),
inference(superposition,[status(thm)],[c_30938,c_161]) ).
tcf(c_31132,plain,
( ( sk_c2 = identity )
| ( sk_c8 = sk_c7 )
| ( inverse(sk_c3) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_30938,c_157]) ).
tcf(c_31183,plain,
( ( sk_c9 = identity )
| ( inverse(sk_c1) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_30369,c_168]) ).
tcf(c_31191,plain,
( ( sk_c9 = identity )
| ( multiply(sk_c1,sk_c11) = identity ) ),
inference(superposition,[status(thm)],[c_31183,c_30328]) ).
tcf(c_31241,plain,
( ( sk_c11 = identity )
| ( inverse(sk_c1) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_30371,c_170]) ).
tcf(c_31248,plain,
( ( sk_c11 = identity )
| ( multiply(sk_c1,sk_c11) = identity ) ),
inference(superposition,[status(thm)],[c_31241,c_30328]) ).
tcf(c_31458,plain,
( ( sk_c2 = identity )
| ( sk_c10 = identity )
| ( inverse(sk_c5) = sk_c8 ) ),
inference(superposition,[status(thm)],[c_31087,c_161]) ).
tcf(c_31460,plain,
( ( sk_c2 = identity )
| ( sk_c10 = identity )
| ( inverse(sk_c3) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_31087,c_157]) ).
tcf(c_31585,plain,
( ( inverse(sk_c11) = sk_c9 )
| ( multiply(sk_c3,multiply(sk_c11,inverse(sk_c10))) = identity ) ),
inference(superposition,[status(thm)],[c_126,c_30513]) ).
tcf(c_31600,plain,
( ( inverse(sk_c1) = sk_c11 )
| ( multiply(sk_c5,multiply(sk_c8,inverse(sk_c11))) = identity ) ),
inference(superposition,[status(thm)],[c_170,c_30513]) ).
tcf(c_31621,plain,
( ( inverse(sk_c4) = sk_c10 )
| ( multiply(sk_c11,multiply(sk_c2,inverse(sk_c10))) = identity ) ),
inference(superposition,[status(thm)],[c_149,c_30513]) ).
tcf(c_31622,plain,
( ( inverse(sk_c3) = sk_c11 )
| ( multiply(sk_c11,multiply(sk_c2,inverse(sk_c10))) = identity ) ),
inference(superposition,[status(thm)],[c_147,c_30513]) ).
tcf(c_31748,plain,
( ( sk_c2 = identity )
| ( sk_c9 = identity )
| ( inverse(sk_c5) = sk_c8 ) ),
inference(superposition,[status(thm)],[c_31191,c_161]) ).
tcf(c_31750,plain,
( ( sk_c2 = identity )
| ( sk_c9 = identity )
| ( inverse(sk_c3) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_31191,c_157]) ).
tcf(c_31774,plain,
( ( sk_c2 = identity )
| ( sk_c11 = identity )
| ( inverse(sk_c5) = sk_c8 ) ),
inference(superposition,[status(thm)],[c_31248,c_161]) ).
tcf(c_31776,plain,
( ( sk_c2 = identity )
| ( sk_c11 = identity )
| ( inverse(sk_c3) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_31248,c_157]) ).
tcf(c_31920,plain,
( ( sk_c2 = identity )
| ( inverse(sk_c5) = sk_c8 ) ),
inference(global_subsumption_just,[status(thm)],[c_31130,c_171,c_131,c_151,c_141,c_121,c_731,c_732,c_725,c_1069,c_1070,c_1431,c_3688,c_8165,c_8164,c_10766,c_14639,c_17584,c_17585,c_19998,c_20758,c_20779,c_22520,c_26518,c_31458,c_31748,c_31774]) ).
tcf(c_31928,plain,
( ( sk_c2 = identity )
| ( multiply(sk_c8,sk_c5) = identity ) ),
inference(superposition,[status(thm)],[c_31920,c_114]) ).
tcf(c_31942,plain,
( ( sk_c2 = identity )
| ( inverse(sk_c3) = sk_c11 ) ),
inference(global_subsumption_just,[status(thm)],[c_31132,c_127,c_731,c_732,c_1069,c_1070,c_1431,c_8165,c_8164,c_10766,c_14639,c_17584,c_17585,c_19998,c_20037,c_20758,c_20779,c_22520,c_26518,c_31460,c_31750,c_31776]) ).
tcf(c_31950,plain,
( ( sk_c2 = identity )
| ( multiply(sk_c11,sk_c3) = identity ) ),
inference(superposition,[status(thm)],[c_31942,c_114]) ).
tcf(c_31976,plain,
! [X0: $i] :
( ( sk_c2 = identity )
| ( multiply(sk_c8,multiply(sk_c5,X0)) = multiply(identity,X0) ) ),
inference(superposition,[status(thm)],[c_31928,c_115]) ).
tcf(c_32082,plain,
! [X0: $i] :
( ( sk_c2 = identity )
| ( multiply(sk_c11,multiply(sk_c3,X0)) = multiply(identity,X0) ) ),
inference(superposition,[status(thm)],[c_31950,c_115]) ).
tcf(c_32466,plain,
! [X0: $i] :
( ( inverse(sk_c5) = sk_c8 )
| ( multiply(sk_c9,multiply(sk_c10,multiply(inverse(sk_c11),X0))) = X0 ) ),
inference(superposition,[status(thm)],[c_141,c_30576]) ).
tcf(c_32467,plain,
! [X0: $i] :
( ( inverse(sk_c4) = sk_c10 )
| ( multiply(sk_c9,multiply(sk_c10,multiply(inverse(sk_c11),X0))) = X0 ) ),
inference(superposition,[status(thm)],[c_139,c_30576]) ).
tcf(c_32468,plain,
! [X0: $i] :
( ( inverse(sk_c3) = sk_c11 )
| ( multiply(sk_c9,multiply(sk_c10,multiply(inverse(sk_c11),X0))) = X0 ) ),
inference(superposition,[status(thm)],[c_137,c_30576]) ).
tcf(c_32857,plain,
( ( inverse(sk_c11) = sk_c9 )
| ( multiply(sk_c3,multiply(sk_c11,sk_c4)) = identity ) ),
inference(superposition,[status(thm)],[c_30320,c_31585]) ).
tcf(c_32917,plain,
( ( sk_c4 = identity )
| ( inverse(sk_c11) = sk_c9 ) ),
inference(superposition,[status(thm)],[c_32857,c_30560]) ).
tcf(c_32920,plain,
inverse(sk_c11) = sk_c9,
inference(global_subsumption_just,[status(thm)],[c_30660,c_731,c_732,c_1045,c_2575,c_5072,c_5265,c_5569,c_9381,c_19742,c_19796,c_20751,c_20778,c_20868,c_32917]) ).
tcf(c_32956,plain,
( iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( sk_c9 != sk_c9 )
| ( multiply(sk_c9,sk_c10) != sk_c11 )
| ( multiply(sk_c11,sk_c10) != sk_c9 ) ),
inference(demodulation,[status(thm)],[c_725,c_32920]) ).
tcf(c_32974,plain,
( iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( multiply(sk_c9,sk_c10) != sk_c11 )
| ( multiply(sk_c11,sk_c10) != sk_c9 ) ),
inference(equality_resolution_simp,[status(thm)],[c_32956]) ).
tcf(c_32975,plain,
! [X0: $i] :
( ~ iPr_def_11
| ( sk_c11 != identity )
| ( inverse(sk_c11) != X0 )
| ( multiply(X0,sk_c9) != inverse(X0) )
| ( multiply(inverse(sk_c11),sk_c10) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_32920,c_30796]) ).
tcf(c_32978,plain,
inverse(sk_c9) = sk_c11,
inference(superposition,[status(thm)],[c_32920,c_8093]) ).
tcf(c_32979,plain,
multiply(sk_c9,sk_c11) = identity,
inference(superposition,[status(thm)],[c_32920,c_114]) ).
tcf(c_32980,plain,
! [X0: $i] :
( ~ iPr_def_11
| ( sk_c11 != identity )
| ( X0 != sk_c9 )
| ( multiply(sk_c9,sk_c10) != sk_c11 )
| ( multiply(X0,sk_c9) != inverse(X0) ) ),
inference(light_normalisation,[status(thm)],[c_32975,c_32920]) ).
tcf(c_32986,plain,
( ~ iPr_def_11
| ( sk_c11 != identity )
| ( sk_c11 != sk_c9 )
| ( multiply(sk_c9,sk_c10) != sk_c11 )
| ( multiply(sk_c11,sk_c9) != inverse(sk_c11) ) ),
inference(instantiation,[status(thm)],[c_32980]) ).
tcf(c_32987,plain,
inverse(sk_c1) = sk_c11,
inference(global_subsumption_just,[status(thm)],[c_31600,c_169,c_167,c_731,c_732,c_1045,c_1063,c_1064,c_1069,c_1070,c_1630,c_1631,c_2061,c_2116,c_2575,c_4422,c_4783,c_5072,c_5203,c_5265,c_5369,c_5569,c_9381,c_10759,c_19742,c_19796,c_19998,c_20751,c_20757,c_20758,c_20778,c_20779,c_20868,c_22082,c_26518,c_30781,c_32917,c_32986]) ).
tcf(c_33039,plain,
( ( inverse(sk_c5) = sk_c8 )
| ~ iPr_def_13
| ( multiply(sk_c11,sk_c2) != sk_c10 ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_30773,c_32987]) ).
tcf(c_33049,plain,
! [X0: $i] :
( ~ iPr_def_11
| ( sk_c11 != identity )
| ( inverse(sk_c1) != X0 )
| ( multiply(X0,sk_c11) != inverse(X0) )
| ( multiply(inverse(sk_c1),sk_c10) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_32987,c_30796]) ).
tcf(c_33051,plain,
multiply(sk_c1,sk_c11) = identity,
inference(superposition,[status(thm)],[c_32987,c_30328]) ).
tcf(c_33053,plain,
multiply(sk_c11,sk_c1) = identity,
inference(superposition,[status(thm)],[c_32987,c_114]) ).
tcf(c_33054,plain,
! [X0: $i] :
( ~ iPr_def_11
| ( sk_c11 != identity )
| ( X0 != sk_c11 )
| ( multiply(sk_c11,sk_c10) != sk_c11 )
| ( multiply(X0,sk_c11) != inverse(X0) ) ),
inference(light_normalisation,[status(thm)],[c_33049,c_32987]) ).
tcf(c_33056,plain,
( ~ iPr_def_11
| ( sk_c11 != identity )
| ( sk_c11 != sk_c11 )
| ( multiply(sk_c11,sk_c10) != sk_c11 )
| ( multiply(sk_c11,sk_c11) != inverse(sk_c11) ) ),
inference(instantiation,[status(thm)],[c_33054]) ).
tcf(c_33079,plain,
! [X0: $i] : multiply(sk_c9,multiply(sk_c11,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_32979,c_115]) ).
tcf(c_33088,plain,
! [X0: $i] : multiply(sk_c11,multiply(sk_c1,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_33053,c_115]) ).
tcf(c_33091,plain,
! [X0: $i] : multiply(sk_c9,multiply(sk_c11,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_33079,c_113]) ).
tcf(c_33101,plain,
( ( inverse(sk_c5) = sk_c8 )
| ( multiply(sk_c9,sk_c10) = sk_c2 ) ),
inference(superposition,[status(thm)],[c_151,c_33091]) ).
tcf(c_33102,plain,
( ( inverse(sk_c4) = sk_c10 )
| ( multiply(sk_c9,sk_c10) = sk_c2 ) ),
inference(superposition,[status(thm)],[c_149,c_33091]) ).
tcf(c_33103,plain,
( ( inverse(sk_c3) = sk_c11 )
| ( multiply(sk_c9,sk_c10) = sk_c2 ) ),
inference(superposition,[status(thm)],[c_147,c_33091]) ).
tcf(c_33107,plain,
! [X0: $i] : multiply(inverse(sk_c11),X0) = multiply(sk_c9,X0),
inference(superposition,[status(thm)],[c_30552,c_33091]) ).
tcf(c_33140,plain,
! [X0: $i] : multiply(sk_c11,multiply(sk_c1,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_33088,c_113]) ).
tcf(c_33146,plain,
( ( inverse(sk_c5) = sk_c8 )
| ( multiply(sk_c11,sk_c2) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_161,c_33140]) ).
tcf(c_33147,plain,
( ( inverse(sk_c4) = sk_c10 )
| ( multiply(sk_c11,sk_c2) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_159,c_33140]) ).
tcf(c_33148,plain,
( ( inverse(sk_c3) = sk_c11 )
| ( multiply(sk_c11,sk_c2) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_157,c_33140]) ).
tcf(c_33287,plain,
( ( sk_c11 = sk_c2 )
| ( inverse(sk_c5) = sk_c8 ) ),
inference(superposition,[status(thm)],[c_33101,c_141]) ).
tcf(c_33315,plain,
( ( sk_c11 = sk_c2 )
| ( inverse(sk_c4) = sk_c10 ) ),
inference(superposition,[status(thm)],[c_33102,c_139]) ).
tcf(c_33343,plain,
( ( sk_c11 = sk_c2 )
| ( inverse(sk_c3) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_33103,c_137]) ).
tcf(c_33444,plain,
( ( sk_c11 = sk_c10 )
| ( inverse(sk_c5) = sk_c8 ) ),
inference(superposition,[status(thm)],[c_33146,c_151]) ).
tcf(c_33472,plain,
( ( sk_c11 = sk_c10 )
| ( inverse(sk_c4) = sk_c10 ) ),
inference(superposition,[status(thm)],[c_33147,c_149]) ).
tcf(c_33500,plain,
( ( sk_c11 = sk_c10 )
| ( inverse(sk_c3) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_33148,c_147]) ).
tcf(c_33511,plain,
( ( sk_c11 = sk_c10 )
| ( multiply(sk_c3,sk_c11) = identity ) ),
inference(superposition,[status(thm)],[c_33500,c_30328]) ).
tcf(c_33608,plain,
! [X0: $i] :
( ( inverse(sk_c4) = sk_c10 )
| ( multiply(sk_c11,multiply(multiply(sk_c2,inverse(sk_c10)),X0)) = multiply(identity,X0) ) ),
inference(superposition,[status(thm)],[c_31621,c_115]) ).
tcf(c_33615,plain,
! [X0: $i] :
( ( inverse(sk_c3) = sk_c11 )
| ( multiply(sk_c11,multiply(multiply(sk_c2,inverse(sk_c10)),X0)) = multiply(identity,X0) ) ),
inference(superposition,[status(thm)],[c_31622,c_115]) ).
tcf(c_33928,plain,
! [X0: $i] :
( ( sk_c2 = identity )
| ( multiply(sk_c8,multiply(sk_c5,X0)) = X0 ) ),
inference(light_normalisation,[status(thm)],[c_31976,c_113]) ).
tcf(c_33935,plain,
( ( sk_c2 = identity )
| ( multiply(sk_c1,sk_c11) = sk_c2 )
| ( multiply(sk_c8,sk_c11) = sk_c8 ) ),
inference(superposition,[status(thm)],[c_160,c_33928]) ).
tcf(c_34117,plain,
! [X0: $i] :
( ( sk_c2 = identity )
| ( multiply(sk_c11,multiply(sk_c3,X0)) = X0 ) ),
inference(light_normalisation,[status(thm)],[c_32082,c_113]) ).
tcf(c_34124,plain,
( ( sk_c2 = identity )
| ( multiply(sk_c1,sk_c11) = sk_c2 )
| ( multiply(sk_c11,sk_c10) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_156,c_34117]) ).
tcf(c_38539,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( inverse(sk_c3) = sk_c11 )
| ( multiply(X2,X0) = X1 )
| ( X2 != sk_c11 )
| ( X1 != sk_c10 )
| ( X0 != sk_c2 ) ),
inference(resolution,[status(thm)],[c_11259,c_3942]) ).
tcf(c_38540,plain,
( ( inverse(sk_c3) = sk_c11 )
| ( multiply(sk_c11,sk_c11) = sk_c11 )
| ( sk_c11 != sk_c2 )
| ( sk_c11 != sk_c10 )
| ( sk_c11 != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_38539]) ).
tcf(c_38867,plain,
! [X0: $i,X1: $i] :
( ( X1 = inverse(sk_c4) )
| ( X1 != X0 )
| ( inverse(sk_c4) != X0 ) ),
inference(instantiation,[status(thm)],[c_1081]) ).
tcf(c_38868,plain,
( ( sk_c11 = inverse(sk_c4) )
| ( sk_c11 != sk_c11 )
| ( inverse(sk_c4) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_38867]) ).
tcf(c_39170,plain,
! [X0: $i,X1: $i] :
( ( inverse(X1) = multiply(sk_c11,sk_c10) )
| ~ iPr_def_12
| ( X1 != X0 )
| ( inverse(X0) != sk_c9 ) ),
inference(resolution,[status(thm)],[c_10558,c_2544]) ).
tcf(c_39171,plain,
( ( inverse(sk_c11) = multiply(sk_c11,sk_c10) )
| ~ iPr_def_12
| ( sk_c11 != sk_c11 )
| ( inverse(sk_c11) != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_39170]) ).
tcf(c_39216,plain,
! [X0: $i] :
( iPr_def_12
| iPr_def_11
| ( X0 != sk_c11 )
| ( inverse(sk_c3) = X0 ) ),
inference(global_subsumption_just,[status(thm)],[c_20055,c_169,c_167,c_147,c_137,c_731,c_732,c_733,c_1045,c_1063,c_1064,c_1069,c_1070,c_1124,c_1386,c_1630,c_1631,c_2061,c_2116,c_2575,c_3690,c_3708,c_4071,c_4072,c_4422,c_4534,c_4783,c_5072,c_5203,c_5265,c_5369,c_5569,c_7310,c_9381,c_10759,c_12352,c_17687,c_19742,c_19796,c_19998,c_20751,c_20757,c_20758,c_20778,c_20779,c_20868,c_22082,c_26518,c_27299,c_27300,c_30781,c_32917,c_32986,c_33343,c_33500,c_38540]) ).
tcf(c_39217,plain,
! [X0: $i] :
( iPr_def_12
| iPr_def_11
| ( inverse(sk_c3) = X0 )
| ( X0 != sk_c11 ) ),
inference(renaming,[status(thm)],[c_39216]) ).
tcf(c_39235,plain,
! [X0: $i] :
( iPr_def_12
| iPr_def_11
| ( X0 = inverse(sk_c3) )
| ( X0 != sk_c11 ) ),
inference(resolution,[status(thm)],[c_39217,c_2543]) ).
tcf(c_39236,plain,
( iPr_def_12
| iPr_def_11
| ( sk_c11 = inverse(sk_c3) )
| ( sk_c11 != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_39235]) ).
tcf(c_41775,plain,
! [X0: $i] :
( ( inverse(sk_c11) = sk_c10 )
| ( sk_c10 != X0 )
| ( inverse(sk_c11) != X0 ) ),
inference(instantiation,[status(thm)],[c_1387]) ).
tcf(c_41784,plain,
( ( inverse(sk_c11) = sk_c10 )
| ( sk_c10 != sk_c11 )
| ( inverse(sk_c11) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_41775]) ).
tcf(c_41930,plain,
! [X0: $i] :
( ( multiply(X0,sk_c11) = sk_c10 )
| ( sk_c10 != multiply(sk_c11,sk_c2) )
| ( multiply(X0,sk_c11) != multiply(sk_c11,sk_c2) ) ),
inference(instantiation,[status(thm)],[c_17510]) ).
tcf(c_41931,plain,
( ( multiply(sk_c11,sk_c11) = sk_c10 )
| ( sk_c10 != multiply(sk_c11,sk_c2) )
| ( multiply(sk_c11,sk_c11) != multiply(sk_c11,sk_c2) ) ),
inference(instantiation,[status(thm)],[c_41930]) ).
tcf(c_42429,plain,
( ( sk_c11 = multiply(sk_c5,sk_c8) )
| ( sk_c11 != sk_c11 )
| ( multiply(sk_c5,sk_c8) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_26517]) ).
tcf(c_42431,plain,
( ( sk_c11 = multiply(sk_c9,sk_c10) )
| ( sk_c11 != sk_c11 )
| ( multiply(sk_c9,sk_c10) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_26517]) ).
tcf(c_42433,plain,
( ( sk_c11 = multiply(sk_c1,sk_c11) )
| ( sk_c11 != sk_c2 )
| ( multiply(sk_c1,sk_c11) != sk_c2 ) ),
inference(instantiation,[status(thm)],[c_26517]) ).
tcf(c_42439,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( multiply(X0,X1) = X3 )
| ( X3 != X2 )
| ( multiply(X0,X1) != X2 ) ),
inference(instantiation,[status(thm)],[c_727]) ).
tcf(c_42440,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( sk_c11 = multiply(X0,X1) )
| ( sk_c11 != multiply(X2,X3) )
| ( multiply(X0,X1) != multiply(X2,X3) ) ),
inference(instantiation,[status(thm)],[c_26517]) ).
tcf(c_42441,plain,
! [X0: $i] :
( ( sk_c11 = multiply(X0,sk_c11) )
| ( sk_c11 != sk_c10 )
| ( multiply(X0,sk_c11) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_26517]) ).
tcf(c_42442,plain,
( ( sk_c11 = multiply(sk_c11,sk_c11) )
| ( sk_c11 != sk_c10 )
| ( multiply(sk_c11,sk_c11) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_42441]) ).
tcf(c_43225,plain,
! [X0: $i] :
( ( multiply(inverse(sk_c11),X0) = multiply(sk_c3,sk_c11) )
| ( X0 != sk_c11 )
| ( inverse(sk_c11) != sk_c3 ) ),
inference(instantiation,[status(thm)],[c_8669]) ).
tcf(c_43228,plain,
( ( multiply(inverse(sk_c11),sk_c11) = multiply(sk_c3,sk_c11) )
| ( sk_c11 != sk_c11 )
| ( inverse(sk_c11) != sk_c3 ) ),
inference(instantiation,[status(thm)],[c_43225]) ).
tcf(c_44232,plain,
! [X0: $i,X1: $i] :
( ( sk_c11 = multiply(inverse(X0),sk_c10) )
| ( sk_c11 != X1 )
| ( multiply(inverse(X0),sk_c10) != X1 ) ),
inference(instantiation,[status(thm)],[c_26517]) ).
tcf(c_44236,plain,
! [X0: $i] :
( ( multiply(inverse(sk_c10),sk_c10) = multiply(inverse(X0),X0) )
| ( multiply(inverse(sk_c10),sk_c10) != identity )
| ( multiply(inverse(X0),X0) != identity ) ),
inference(instantiation,[status(thm)],[c_26389]) ).
tcf(c_44237,plain,
( ( multiply(inverse(sk_c10),sk_c10) = multiply(inverse(sk_c11),sk_c11) )
| ( multiply(inverse(sk_c10),sk_c10) != identity )
| ( multiply(inverse(sk_c11),sk_c11) != identity ) ),
inference(instantiation,[status(thm)],[c_44236]) ).
tcf(c_44338,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(inverse(X0),sk_c10) = multiply(X1,X2) )
| ( multiply(X1,X2) != multiply(inverse(X0),sk_c10) )
| ( multiply(inverse(X0),sk_c10) != multiply(inverse(X0),sk_c10) ) ),
inference(instantiation,[status(thm)],[c_26390]) ).
tcf(c_44854,plain,
! [X0: $i] :
( ( identity = inverse(sk_c11) )
| ( identity != X0 )
| ( inverse(sk_c11) != X0 ) ),
inference(instantiation,[status(thm)],[c_1072]) ).
tcf(c_44856,plain,
( ( sk_c9 = identity )
| ( identity != inverse(sk_c11) )
| ( sk_c9 != inverse(sk_c11) ) ),
inference(instantiation,[status(thm)],[c_20752]) ).
tcf(c_46098,plain,
! [X0: $i] :
( ( inverse(sk_c5) = sk_c8 )
| ( multiply(sk_c9,multiply(sk_c10,multiply(sk_c9,X0))) = X0 ) ),
inference(light_normalisation,[status(thm)],[c_32466,c_33107]) ).
tcf(c_46119,plain,
( ( inverse(sk_c5) = sk_c8 )
| ( multiply(sk_c9,multiply(sk_c10,sk_c11)) = sk_c10 ) ),
inference(superposition,[status(thm)],[c_141,c_46098]) ).
tcf(c_46335,plain,
( ( inverse(sk_c5) = sk_c8 )
| ( multiply(sk_c11,sk_c11) = sk_c10 ) ),
inference(superposition,[status(thm)],[c_46119,c_1307]) ).
tcf(c_46341,plain,
! [X0: $i] :
( ( inverse(sk_c4) = sk_c10 )
| ( multiply(sk_c9,multiply(sk_c10,multiply(sk_c9,X0))) = X0 ) ),
inference(light_normalisation,[status(thm)],[c_32467,c_33107]) ).
tcf(c_46363,plain,
( ( inverse(sk_c4) = sk_c10 )
| ( multiply(sk_c9,multiply(sk_c10,sk_c11)) = sk_c10 ) ),
inference(superposition,[status(thm)],[c_139,c_46341]) ).
tcf(c_46537,plain,
( ( inverse(sk_c4) = sk_c10 )
| ( multiply(sk_c11,sk_c11) = sk_c10 ) ),
inference(superposition,[status(thm)],[c_46363,c_1308]) ).
tcf(c_46544,plain,
! [X0: $i] :
( ( inverse(sk_c3) = sk_c11 )
| ( multiply(sk_c9,multiply(sk_c10,multiply(sk_c9,X0))) = X0 ) ),
inference(light_normalisation,[status(thm)],[c_32468,c_33107]) ).
tcf(c_46567,plain,
( ( inverse(sk_c3) = sk_c11 )
| ( multiply(sk_c9,multiply(sk_c10,sk_c11)) = sk_c10 ) ),
inference(superposition,[status(thm)],[c_137,c_46544]) ).
tcf(c_46662,plain,
( ( inverse(sk_c3) = sk_c11 )
| ( multiply(sk_c11,sk_c11) = sk_c10 ) ),
inference(superposition,[status(thm)],[c_46567,c_1309]) ).
tcf(c_49982,plain,
( ( sk_c2 = identity )
| ( multiply(sk_c8,sk_c11) = sk_c8 ) ),
inference(light_normalisation,[status(thm)],[c_33935,c_33051]) ).
tcf(c_49992,plain,
( ( sk_c2 = identity )
| ~ iPr_def_10
| ( sk_c10 != sk_c8 )
| ( inverse(sk_c8) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_49982,c_721]) ).
tcf(c_50263,plain,
( ( sk_c2 = identity )
| ( multiply(sk_c11,sk_c10) = sk_c11 ) ),
inference(light_normalisation,[status(thm)],[c_34124,c_33051]) ).
tcf(c_50292,plain,
( ( sk_c2 = identity )
| ( multiply(sk_c9,sk_c11) = sk_c10 ) ),
inference(superposition,[status(thm)],[c_50263,c_33091]) ).
tcf(c_50686,plain,
! [X0: $i] :
( ( sk_c9 = inverse(sk_c4) )
| ( sk_c9 != X0 )
| ( inverse(sk_c4) != X0 ) ),
inference(instantiation,[status(thm)],[c_1053]) ).
tcf(c_50695,plain,
( ( sk_c9 = inverse(sk_c4) )
| ( sk_c9 != sk_c11 )
| ( inverse(sk_c4) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_50686]) ).
tcf(c_50826,plain,
! [X0: $i] :
( ( multiply(inverse(X0),sk_c10) = sk_c11 )
| ( sk_c11 != multiply(sk_c9,sk_c10) )
| ( multiply(inverse(X0),sk_c10) != multiply(sk_c9,sk_c10) ) ),
inference(instantiation,[status(thm)],[c_17582]) ).
tcf(c_50827,plain,
( ( multiply(inverse(sk_c11),sk_c10) = sk_c11 )
| ( sk_c11 != multiply(sk_c9,sk_c10) )
| ( multiply(inverse(sk_c11),sk_c10) != multiply(sk_c9,sk_c10) ) ),
inference(instantiation,[status(thm)],[c_50826]) ).
tcf(c_52162,plain,
! [X0: $i] :
( ( multiply(sk_c11,sk_c10) = X0 )
| ( X0 != sk_c9 )
| ( multiply(sk_c11,sk_c10) != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_42439]) ).
tcf(c_52972,plain,
( ( inverse(sk_c5) = sk_c8 )
| ~ iPr_def_12 ),
inference(global_subsumption_just,[status(thm)],[c_30752,c_731,c_732,c_735,c_1045,c_1386,c_2111,c_2117,c_2575,c_4534,c_5072,c_5265,c_5569,c_7310,c_9381,c_19742,c_19796,c_20751,c_20778,c_20868,c_27299,c_27300,c_32917,c_33444,c_39171,c_41784,c_42442,c_46335]) ).
tcf(c_52976,plain,
( ( inverse(sk_c4) = sk_c10 )
| ~ iPr_def_12 ),
inference(global_subsumption_just,[status(thm)],[c_30753,c_731,c_732,c_1045,c_1386,c_2423,c_2575,c_4534,c_5072,c_5265,c_5569,c_7310,c_9381,c_19742,c_19796,c_20751,c_20778,c_20868,c_27299,c_27300,c_32917,c_33472,c_39171,c_41784,c_42442,c_46537]) ).
tcf(c_52980,plain,
( ( inverse(sk_c3) = sk_c11 )
| ~ iPr_def_12 ),
inference(global_subsumption_just,[status(thm)],[c_30754,c_731,c_732,c_735,c_1045,c_1386,c_2111,c_2117,c_2575,c_4534,c_5072,c_5265,c_5569,c_7310,c_9381,c_19742,c_19796,c_20751,c_20778,c_20868,c_27299,c_27300,c_32917,c_33500,c_39171,c_41784,c_42442,c_46662]) ).
tcf(c_53684,plain,
( ( sk_c10 = identity )
| ( identity != multiply(sk_c3,sk_c11) )
| ( sk_c10 != multiply(sk_c3,sk_c11) ) ),
inference(instantiation,[status(thm)],[c_20774]) ).
tcf(c_54586,plain,
( ( sk_c11 = multiply(inverse(sk_c10),sk_c10) )
| ( sk_c11 != identity )
| ( multiply(inverse(sk_c10),sk_c10) != identity ) ),
inference(instantiation,[status(thm)],[c_44232]) ).
tcf(c_55397,plain,
( ( identity = inverse(sk_c11) )
| ( identity != identity )
| ( inverse(sk_c11) != identity ) ),
inference(instantiation,[status(thm)],[c_44854]) ).
tcf(c_55749,plain,
! [X0: $i,X1: $i] :
( ( sk_c11 = multiply(X0,X1) )
| ( sk_c11 != multiply(identity,inverse(sk_c1)) )
| ( multiply(X0,X1) != multiply(identity,inverse(sk_c1)) ) ),
inference(instantiation,[status(thm)],[c_42440]) ).
tcf(c_55752,plain,
( ( sk_c11 = multiply(sk_c11,sk_c11) )
| ( sk_c11 != multiply(identity,inverse(sk_c1)) )
| ( multiply(sk_c11,sk_c11) != multiply(identity,inverse(sk_c1)) ) ),
inference(instantiation,[status(thm)],[c_55749]) ).
tcf(c_57237,plain,
! [X0: $i] :
( ( inverse(sk_c3) = multiply(sk_c11,X0) )
| ( inverse(sk_c3) != sk_c11 )
| ( multiply(sk_c11,X0) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_1495]) ).
tcf(c_57239,plain,
( ( inverse(sk_c3) = multiply(sk_c11,sk_c11) )
| ( inverse(sk_c3) != sk_c11 )
| ( multiply(sk_c11,sk_c11) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_57237]) ).
tcf(c_57387,plain,
( ( sk_c2 = multiply(sk_c9,sk_c10) )
| ~ iPr_def_10
| ( multiply(sk_c1,sk_c11) != sk_c11 ) ),
inference(resolution,[status(thm)],[c_21341,c_10503]) ).
tcf(c_58662,plain,
! [X0: $i] :
( ( multiply(inverse(X0),sk_c10) = multiply(sk_c9,sk_c10) )
| ( multiply(sk_c9,sk_c10) != multiply(inverse(X0),sk_c10) )
| ( multiply(inverse(X0),sk_c10) != multiply(inverse(X0),sk_c10) ) ),
inference(instantiation,[status(thm)],[c_44338]) ).
tcf(c_58664,plain,
( ( multiply(inverse(sk_c11),sk_c10) = multiply(sk_c9,sk_c10) )
| ( multiply(sk_c9,sk_c10) != multiply(inverse(sk_c11),sk_c10) )
| ( multiply(inverse(sk_c11),sk_c10) != multiply(inverse(sk_c11),sk_c10) ) ),
inference(instantiation,[status(thm)],[c_58662]) ).
tcf(c_59650,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(inverse(X0),sk_c10) = X2 )
| ( X2 != X1 )
| ( multiply(inverse(X0),sk_c10) != X1 ) ),
inference(instantiation,[status(thm)],[c_727]) ).
tcf(c_59652,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(inverse(X0),sk_c10) = multiply(X1,X2) )
| ( sk_c10 != X2 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_728]) ).
tcf(c_59653,plain,
! [X0: $i] :
( ( sk_c11 = identity )
| ( identity != X0 )
| ( sk_c11 != X0 ) ),
inference(instantiation,[status(thm)],[c_727]) ).
tcf(c_59656,plain,
! [X0: $i,X1: $i] :
( ( sk_c11 = multiply(inverse(X0),sk_c10) )
| ( sk_c11 != X1 )
| ( multiply(inverse(X0),sk_c10) != X1 ) ),
inference(instantiation,[status(thm)],[c_727]) ).
tcf(c_59664,plain,
! [X0: $i] :
( ( multiply(inverse(sk_c10),sk_c10) = X0 )
| ( X0 != identity )
| ( multiply(inverse(sk_c10),sk_c10) != identity ) ),
inference(instantiation,[status(thm)],[c_59650]) ).
tcf(c_59666,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( sk_c11 = multiply(X0,X1) )
| ( sk_c11 != X2 )
| ( multiply(X0,X1) != X2 ) ),
inference(instantiation,[status(thm)],[c_727]) ).
tcf(c_59667,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( multiply(inverse(X0),sk_c10) = X3 )
| ( X3 != multiply(X1,X2) )
| ( multiply(inverse(X0),sk_c10) != multiply(X1,X2) ) ),
inference(instantiation,[status(thm)],[c_59650]) ).
tcf(c_59670,plain,
! [X0: $i,X1: $i] :
( ( identity = X0 )
| ( identity != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_727]) ).
tcf(c_59677,plain,
inverse(inverse(identity)) = identity,
inference(instantiation,[status(thm)],[c_8093]) ).
tcf(c_59689,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( sk_c11 = multiply(inverse(X0),sk_c10) )
| ( sk_c11 != multiply(X1,X2) )
| ( multiply(inverse(X0),sk_c10) != multiply(X1,X2) ) ),
inference(instantiation,[status(thm)],[c_59656]) ).
tcf(c_59693,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = multiply(inverse(X0),sk_c10) )
| ( X2 != X1 )
| ( multiply(inverse(X0),sk_c10) != X1 ) ),
inference(instantiation,[status(thm)],[c_727]) ).
tcf(c_59713,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( multiply(X0,X1) = X3 )
| ( X3 != X2 )
| ( multiply(X0,X1) != X2 ) ),
inference(instantiation,[status(thm)],[c_727]) ).
tcf(c_59735,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( X3 = multiply(X0,X1) )
| ( X3 != X2 )
| ( multiply(X0,X1) != X2 ) ),
inference(instantiation,[status(thm)],[c_727]) ).
tcf(c_59736,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( ( multiply(inverse(X0),sk_c10) = multiply(X3,X4) )
| ( multiply(X3,X4) != multiply(X1,X2) )
| ( multiply(inverse(X0),sk_c10) != multiply(X1,X2) ) ),
inference(instantiation,[status(thm)],[c_59667]) ).
tcf(c_59794,plain,
! [X0: $i] :
( ( identity = X0 )
| ( identity != identity )
| ( X0 != identity ) ),
inference(instantiation,[status(thm)],[c_59670]) ).
tcf(c_59806,plain,
! [X0: $i,X1: $i] :
( ( multiply(inverse(X0),sk_c10) = sk_c11 )
| ( sk_c11 != multiply(identity,X1) )
| ( multiply(inverse(X0),sk_c10) != multiply(identity,X1) ) ),
inference(instantiation,[status(thm)],[c_59667]) ).
tcf(c_59832,plain,
! [X0: $i] :
( ( X0 = multiply(inverse(sk_c10),sk_c10) )
| ( X0 != identity )
| ( multiply(inverse(sk_c10),sk_c10) != identity ) ),
inference(instantiation,[status(thm)],[c_59693]) ).
tcf(c_59834,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( X3 = multiply(inverse(X0),sk_c10) )
| ( X3 != multiply(X1,X2) )
| ( multiply(inverse(X0),sk_c10) != multiply(X1,X2) ) ),
inference(instantiation,[status(thm)],[c_59693]) ).
tcf(c_59885,plain,
! [X0: $i] :
( ( multiply(sk_c1,sk_c11) = X0 )
| ( X0 != sk_c2 )
| ( multiply(sk_c1,sk_c11) != sk_c2 ) ),
inference(instantiation,[status(thm)],[c_59713]) ).
tcf(c_59889,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(X0,X1) = X2 )
| ( X2 != multiply(X0,X1) )
| ( multiply(X0,X1) != multiply(X0,X1) ) ),
inference(instantiation,[status(thm)],[c_59713]) ).
tcf(c_59890,plain,
! [X0: $i,X1: $i] : multiply(X0,X1) = multiply(X0,X1),
inference(instantiation,[status(thm)],[c_726]) ).
tcf(c_59937,plain,
! [X0: $i] :
( ( X0 = multiply(sk_c1,sk_c11) )
| ( X0 != sk_c2 )
| ( multiply(sk_c1,sk_c11) != sk_c2 ) ),
inference(instantiation,[status(thm)],[c_59735]) ).
tcf(c_59943,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( ( X4 = multiply(X0,X1) )
| ( X4 != multiply(X2,X3) )
| ( multiply(X0,X1) != multiply(X2,X3) ) ),
inference(instantiation,[status(thm)],[c_59735]) ).
tcf(c_60015,plain,
! [X0: $i,X1: $i] :
( ( X1 = multiply(sk_c3,sk_c11) )
| ( X1 != X0 )
| ( multiply(sk_c3,sk_c11) != X0 ) ),
inference(instantiation,[status(thm)],[c_59735]) ).
tcf(c_60017,plain,
! [X0: $i] :
( ( sk_c11 = multiply(sk_c3,sk_c11) )
| ( sk_c11 != X0 )
| ( multiply(sk_c3,sk_c11) != X0 ) ),
inference(instantiation,[status(thm)],[c_59666]) ).
tcf(c_60046,plain,
! [X0: $i,X1: $i] :
( ( X1 = multiply(sk_c5,sk_c8) )
| ( X1 != X0 )
| ( multiply(sk_c5,sk_c8) != X0 ) ),
inference(instantiation,[status(thm)],[c_59735]) ).
tcf(c_60095,plain,
( ( multiply(inverse(sk_c10),sk_c10) = multiply(sk_c1,sk_c11) )
| ( multiply(sk_c1,sk_c11) != identity )
| ( multiply(inverse(sk_c10),sk_c10) != identity ) ),
inference(instantiation,[status(thm)],[c_59664]) ).
tcf(c_60102,plain,
! [X0: $i,X1: $i] :
( ( X1 = multiply(sk_c1,sk_c11) )
| ( X1 != X0 )
| ( multiply(sk_c1,sk_c11) != X0 ) ),
inference(instantiation,[status(thm)],[c_59735]) ).
tcf(c_60104,plain,
! [X0: $i] :
( ( sk_c11 = multiply(sk_c1,sk_c11) )
| ( sk_c11 != X0 )
| ( multiply(sk_c1,sk_c11) != X0 ) ),
inference(instantiation,[status(thm)],[c_59666]) ).
tcf(c_60105,plain,
( ( sk_c11 = multiply(sk_c1,sk_c11) )
| ( sk_c11 != sk_c11 )
| ( multiply(sk_c1,sk_c11) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_60104]) ).
tcf(c_60108,plain,
! [X0: $i] :
( ( multiply(sk_c1,sk_c11) = multiply(inverse(X0),sk_c10) )
| ( multiply(sk_c1,sk_c11) != sk_c2 )
| ( multiply(inverse(X0),sk_c10) != sk_c2 ) ),
inference(instantiation,[status(thm)],[c_59885]) ).
tcf(c_60110,plain,
( ( multiply(sk_c1,sk_c11) = multiply(inverse(sk_c11),sk_c10) )
| ( multiply(sk_c1,sk_c11) != sk_c2 )
| ( multiply(inverse(sk_c11),sk_c10) != sk_c2 ) ),
inference(instantiation,[status(thm)],[c_60108]) ).
tcf(c_60147,plain,
( ( sk_c11 = identity )
| ( identity != multiply(sk_c5,sk_c8) )
| ( sk_c11 != multiply(sk_c5,sk_c8) ) ),
inference(instantiation,[status(thm)],[c_59653]) ).
tcf(c_60266,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( inverse(X0) = X2 )
| ( X2 != X1 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_727]) ).
tcf(c_60282,plain,
! [X0: $i,X1: $i] :
( ( multiply(inverse(inverse(X0)),sk_c10) = multiply(X0,X1) )
| ( sk_c10 != X1 )
| ( inverse(inverse(X0)) != X0 ) ),
inference(instantiation,[status(thm)],[c_59652]) ).
tcf(c_60283,plain,
( ( multiply(inverse(inverse(sk_c11)),sk_c10) = multiply(sk_c11,sk_c11) )
| ( sk_c10 != sk_c11 )
| ( inverse(inverse(sk_c11)) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_60282]) ).
tcf(c_60426,plain,
( ( inverse(inverse(identity)) = multiply(inverse(sk_c10),sk_c10) )
| ( inverse(inverse(identity)) != identity )
| ( multiply(inverse(sk_c10),sk_c10) != identity ) ),
inference(instantiation,[status(thm)],[c_59832]) ).
tcf(c_60488,plain,
! [X0: $i,X1: $i] :
( ( X1 = multiply(inverse(sk_c10),sk_c10) )
| ( X1 != multiply(inverse(X0),X0) )
| ( multiply(inverse(sk_c10),sk_c10) != multiply(inverse(X0),X0) ) ),
inference(instantiation,[status(thm)],[c_59834]) ).
tcf(c_60564,plain,
( ( identity = multiply(inverse(sk_c10),sk_c10) )
| ( identity != identity )
| ( multiply(inverse(sk_c10),sk_c10) != identity ) ),
inference(instantiation,[status(thm)],[c_59832]) ).
tcf(c_61180,plain,
! [X0: $i] :
( ( multiply(sk_c3,sk_c11) = X0 )
| ( X0 != multiply(sk_c3,sk_c11) )
| ( multiply(sk_c3,sk_c11) != multiply(sk_c3,sk_c11) ) ),
inference(instantiation,[status(thm)],[c_59889]) ).
tcf(c_61477,plain,
! [X0: $i] :
( ( inverse(inverse(identity)) = X0 )
| ( X0 != identity )
| ( inverse(inverse(identity)) != identity ) ),
inference(instantiation,[status(thm)],[c_60266]) ).
tcf(c_61478,plain,
( ( inverse(inverse(identity)) = sk_c11 )
| ( sk_c11 != identity )
| ( inverse(inverse(identity)) != identity ) ),
inference(instantiation,[status(thm)],[c_61477]) ).
tcf(c_61934,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( multiply(inverse(inverse(X0)),sk_c10) = multiply(X2,X3) )
| ( multiply(X2,X3) != multiply(X0,X1) )
| ( multiply(inverse(inverse(X0)),sk_c10) != multiply(X0,X1) ) ),
inference(instantiation,[status(thm)],[c_59736]) ).
tcf(c_62116,plain,
! [X0: $i] :
( ( X0 = multiply(inverse(sk_c10),sk_c10) )
| ( X0 != multiply(sk_c1,sk_c11) )
| ( multiply(inverse(sk_c10),sk_c10) != multiply(sk_c1,sk_c11) ) ),
inference(instantiation,[status(thm)],[c_59834]) ).
tcf(c_62119,plain,
( ( sk_c11 = multiply(inverse(sk_c10),sk_c10) )
| ( sk_c11 != multiply(sk_c1,sk_c11) )
| ( multiply(inverse(sk_c10),sk_c10) != multiply(sk_c1,sk_c11) ) ),
inference(instantiation,[status(thm)],[c_62116]) ).
tcf(c_62384,plain,
inverse(inverse(sk_c10)) = sk_c10,
inference(instantiation,[status(thm)],[c_8093]) ).
tcf(c_62667,plain,
( ( identity = multiply(sk_c3,sk_c11) )
| ( identity != identity )
| ( multiply(sk_c3,sk_c11) != identity ) ),
inference(instantiation,[status(thm)],[c_59794]) ).
tcf(c_62740,plain,
( ( identity = multiply(sk_c5,sk_c8) )
| ( identity != identity )
| ( multiply(sk_c5,sk_c8) != identity ) ),
inference(instantiation,[status(thm)],[c_59794]) ).
tcf(c_62741,plain,
( ( multiply(sk_c5,sk_c8) = multiply(inverse(sk_c10),sk_c10) )
| ( multiply(sk_c5,sk_c8) != identity )
| ( multiply(inverse(sk_c10),sk_c10) != identity ) ),
inference(instantiation,[status(thm)],[c_59832]) ).
tcf(c_63070,plain,
! [X0: $i] :
( ( identity = X0 )
| ( identity != multiply(sk_c5,sk_c8) )
| ( X0 != multiply(sk_c5,sk_c8) ) ),
inference(instantiation,[status(thm)],[c_59670]) ).
tcf(c_63071,plain,
( ( identity = sk_c11 )
| ( identity != multiply(sk_c5,sk_c8) )
| ( sk_c11 != multiply(sk_c5,sk_c8) ) ),
inference(instantiation,[status(thm)],[c_63070]) ).
tcf(c_63390,plain,
multiply(sk_c1,sk_c11) = multiply(sk_c1,sk_c11),
inference(instantiation,[status(thm)],[c_59890]) ).
tcf(c_64687,plain,
! [X0: $i] :
( ( inverse(inverse(identity)) = X0 )
| ( X0 != multiply(inverse(sk_c10),sk_c10) )
| ( inverse(inverse(identity)) != multiply(inverse(sk_c10),sk_c10) ) ),
inference(instantiation,[status(thm)],[c_60266]) ).
tcf(c_64692,plain,
( ( inverse(inverse(identity)) = sk_c11 )
| ( sk_c11 != multiply(inverse(sk_c10),sk_c10) )
| ( inverse(inverse(identity)) != multiply(inverse(sk_c10),sk_c10) ) ),
inference(instantiation,[status(thm)],[c_64687]) ).
tcf(c_64714,plain,
( ( sk_c11 = identity )
| ( identity != multiply(inverse(sk_c10),sk_c10) )
| ( sk_c11 != multiply(inverse(sk_c10),sk_c10) ) ),
inference(instantiation,[status(thm)],[c_59653]) ).
tcf(c_64716,plain,
! [X0: $i] :
( ( identity = X0 )
| ( identity != multiply(inverse(sk_c10),sk_c10) )
| ( X0 != multiply(inverse(sk_c10),sk_c10) ) ),
inference(instantiation,[status(thm)],[c_59670]) ).
tcf(c_64717,plain,
( ( identity = sk_c11 )
| ( identity != multiply(inverse(sk_c10),sk_c10) )
| ( sk_c11 != multiply(inverse(sk_c10),sk_c10) ) ),
inference(instantiation,[status(thm)],[c_64716]) ).
tcf(c_64802,plain,
! [X0: $i] :
( ( inverse(X0) = inverse(identity) )
| ( X0 != identity ) ),
inference(instantiation,[status(thm)],[c_729]) ).
tcf(c_64804,plain,
( ( inverse(sk_c11) = inverse(identity) )
| ( sk_c11 != identity ) ),
inference(instantiation,[status(thm)],[c_64802]) ).
tcf(c_65170,plain,
! [X0: $i] :
( ( multiply(sk_c3,sk_c11) = multiply(inverse(sk_c10),sk_c10) )
| ( multiply(sk_c3,sk_c11) != multiply(inverse(X0),X0) )
| ( multiply(inverse(sk_c10),sk_c10) != multiply(inverse(X0),X0) ) ),
inference(instantiation,[status(thm)],[c_60488]) ).
tcf(c_65171,plain,
! [X0: $i] :
( ( multiply(sk_c3,sk_c11) = multiply(inverse(X0),X0) )
| ( multiply(sk_c3,sk_c11) != multiply(sk_c3,sk_c11) )
| ( multiply(inverse(X0),X0) != multiply(sk_c3,sk_c11) ) ),
inference(instantiation,[status(thm)],[c_61180]) ).
tcf(c_65173,plain,
( ( multiply(sk_c3,sk_c11) = multiply(inverse(sk_c10),sk_c10) )
| ( multiply(sk_c3,sk_c11) != multiply(inverse(sk_c11),sk_c11) )
| ( multiply(inverse(sk_c10),sk_c10) != multiply(inverse(sk_c11),sk_c11) ) ),
inference(instantiation,[status(thm)],[c_65170]) ).
tcf(c_65174,plain,
( ( multiply(sk_c3,sk_c11) = multiply(inverse(sk_c11),sk_c11) )
| ( multiply(sk_c3,sk_c11) != multiply(sk_c3,sk_c11) )
| ( multiply(inverse(sk_c11),sk_c11) != multiply(sk_c3,sk_c11) ) ),
inference(instantiation,[status(thm)],[c_65171]) ).
tcf(c_66613,plain,
! [X0: $i,X1: $i] :
( ( inverse(sk_c3) = X1 )
| ( X1 != X0 )
| ( inverse(sk_c3) != X0 ) ),
inference(instantiation,[status(thm)],[c_60266]) ).
tcf(c_66691,plain,
! [X0: $i,X1: $i] :
( ( inverse(sk_c4) = X1 )
| ( X1 != X0 )
| ( inverse(sk_c4) != X0 ) ),
inference(instantiation,[status(thm)],[c_60266]) ).
tcf(c_70899,plain,
! [X0: $i] :
( ( inverse(sk_c3) = identity )
| ( identity != X0 )
| ( inverse(sk_c3) != X0 ) ),
inference(instantiation,[status(thm)],[c_66613]) ).
tcf(c_71101,plain,
! [X0: $i] :
( ( inverse(sk_c4) = identity )
| ( identity != X0 )
| ( inverse(sk_c4) != X0 ) ),
inference(instantiation,[status(thm)],[c_66691]) ).
tcf(c_71123,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(inverse(X0),sk_c10) = inverse(sk_c4) )
| ( inverse(sk_c4) != multiply(X1,X2) )
| ( multiply(inverse(X0),sk_c10) != multiply(X1,X2) ) ),
inference(instantiation,[status(thm)],[c_59667]) ).
tcf(c_71125,plain,
( ( multiply(inverse(sk_c11),sk_c10) = inverse(sk_c4) )
| ( inverse(sk_c4) != multiply(sk_c11,sk_c11) )
| ( multiply(inverse(sk_c11),sk_c10) != multiply(sk_c11,sk_c11) ) ),
inference(instantiation,[status(thm)],[c_71123]) ).
tcf(c_76052,plain,
inverse(sk_c5) = sk_c8,
inference(global_subsumption_just,[status(thm)],[c_30338,c_151,c_141,c_121,c_731,c_732,c_1045,c_1063,c_1064,c_1069,c_1070,c_1386,c_2269,c_2575,c_3950,c_4133,c_4534,c_5072,c_5265,c_5569,c_7326,c_9381,c_10759,c_11677,c_17576,c_19742,c_19796,c_20751,c_20778,c_20868,c_22082,c_27299,c_27300,c_32917,c_32986,c_33039,c_33051,c_33287,c_33444,c_42442,c_46335,c_52972,c_59677,c_60095,c_60426,c_60564,c_62119,c_64692,c_64714]) ).
tcf(c_76090,plain,
multiply(sk_c5,sk_c8) = identity,
inference(superposition,[status(thm)],[c_76052,c_30328]) ).
tcf(c_76092,plain,
multiply(sk_c8,sk_c5) = identity,
inference(superposition,[status(thm)],[c_76052,c_114]) ).
tcf(c_76355,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(inverse(inverse(X0)),sk_c10) = multiply(identity,X2) )
| ( multiply(identity,X2) != multiply(X0,X1) )
| ( multiply(inverse(inverse(X0)),sk_c10) != multiply(X0,X1) ) ),
inference(instantiation,[status(thm)],[c_61934]) ).
tcf(c_76359,plain,
! [X0: $i,X1: $i] :
( ( multiply(inverse(inverse(X0)),sk_c10) = sk_c11 )
| ( sk_c11 != multiply(identity,X1) )
| ( multiply(inverse(inverse(X0)),sk_c10) != multiply(identity,X1) ) ),
inference(instantiation,[status(thm)],[c_59806]) ).
tcf(c_76360,plain,
( ( multiply(inverse(inverse(sk_c11)),sk_c10) = multiply(identity,sk_c11) )
| ( multiply(identity,sk_c11) != multiply(sk_c11,sk_c11) )
| ( multiply(inverse(inverse(sk_c11)),sk_c10) != multiply(sk_c11,sk_c11) ) ),
inference(instantiation,[status(thm)],[c_76355]) ).
tcf(c_76361,plain,
( ( multiply(inverse(inverse(sk_c11)),sk_c10) = sk_c11 )
| ( sk_c11 != multiply(identity,sk_c11) )
| ( multiply(inverse(inverse(sk_c11)),sk_c10) != multiply(identity,sk_c11) ) ),
inference(instantiation,[status(thm)],[c_76359]) ).
tcf(c_77073,plain,
! [X0: $i] :
( ( X0 = multiply(sk_c9,sk_c10) )
| ( X0 != sk_c11 )
| ( multiply(sk_c9,sk_c10) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_59735]) ).
tcf(c_77090,plain,
! [X0: $i] :
( ( sk_c11 = sk_c2 )
| ( sk_c2 != X0 )
| ( sk_c11 != X0 ) ),
inference(instantiation,[status(thm)],[c_727]) ).
tcf(c_77159,plain,
( ( sk_c2 = multiply(sk_c1,sk_c11) )
| ( sk_c2 != sk_c2 )
| ( multiply(sk_c1,sk_c11) != sk_c2 ) ),
inference(instantiation,[status(thm)],[c_59937]) ).
tcf(c_77160,plain,
sk_c2 = sk_c2,
inference(instantiation,[status(thm)],[c_726]) ).
tcf(c_77276,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( multiply(inverse(X0),sk_c10) = multiply(X2,X3) )
| ( multiply(X2,X3) != X1 )
| ( multiply(inverse(X0),sk_c10) != X1 ) ),
inference(instantiation,[status(thm)],[c_59650]) ).
tcf(c_77277,plain,
( ( multiply(inverse(sk_c11),sk_c10) = multiply(sk_c11,sk_c11) )
| ( multiply(sk_c11,sk_c11) != sk_c11 )
| ( multiply(inverse(sk_c11),sk_c10) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_77276]) ).
tcf(c_77731,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( inverse(X2) = multiply(inverse(X0),sk_c10) )
| ( inverse(X2) != X1 )
| ( multiply(inverse(X0),sk_c10) != X1 ) ),
inference(instantiation,[status(thm)],[c_59693]) ).
tcf(c_77795,plain,
! [X0: $i,X1: $i] :
( ( X1 = multiply(sk_c1,sk_c11) )
| ( X1 != multiply(inverse(X0),sk_c10) )
| ( multiply(sk_c1,sk_c11) != multiply(inverse(X0),sk_c10) ) ),
inference(instantiation,[status(thm)],[c_60102]) ).
tcf(c_77798,plain,
( ( sk_c11 = multiply(sk_c1,sk_c11) )
| ( sk_c11 != multiply(inverse(sk_c11),sk_c10) )
| ( multiply(sk_c1,sk_c11) != multiply(inverse(sk_c11),sk_c10) ) ),
inference(instantiation,[status(thm)],[c_77795]) ).
tcf(c_78368,plain,
! [X0: $i] :
( ( X0 = multiply(sk_c3,sk_c11) )
| ( X0 != multiply(inverse(sk_c10),sk_c10) )
| ( multiply(sk_c3,sk_c11) != multiply(inverse(sk_c10),sk_c10) ) ),
inference(instantiation,[status(thm)],[c_60015]) ).
tcf(c_78370,plain,
( ( sk_c11 = multiply(sk_c3,sk_c11) )
| ( sk_c11 != multiply(inverse(sk_c10),sk_c10) )
| ( multiply(sk_c3,sk_c11) != multiply(inverse(sk_c10),sk_c10) ) ),
inference(instantiation,[status(thm)],[c_78368]) ).
tcf(c_79483,plain,
( ( sk_c11 = multiply(sk_c3,sk_c11) )
| ( sk_c11 != identity )
| ( multiply(sk_c3,sk_c11) != identity ) ),
inference(instantiation,[status(thm)],[c_60017]) ).
tcf(c_79592,plain,
! [X0: $i] :
( ( X0 = multiply(sk_c5,sk_c8) )
| ( X0 != multiply(inverse(sk_c10),sk_c10) )
| ( multiply(sk_c5,sk_c8) != multiply(inverse(sk_c10),sk_c10) ) ),
inference(instantiation,[status(thm)],[c_60046]) ).
tcf(c_79594,plain,
( ( sk_c11 = multiply(sk_c5,sk_c8) )
| ( sk_c11 != multiply(inverse(sk_c10),sk_c10) )
| ( multiply(sk_c5,sk_c8) != multiply(inverse(sk_c10),sk_c10) ) ),
inference(instantiation,[status(thm)],[c_79592]) ).
tcf(c_84125,plain,
! [X0: $i] :
( ( sk_c11 = multiply(inverse(X0),sk_c10) )
| ( sk_c11 != multiply(sk_c9,sk_c10) )
| ( multiply(inverse(X0),sk_c10) != multiply(sk_c9,sk_c10) ) ),
inference(instantiation,[status(thm)],[c_59689]) ).
tcf(c_84127,plain,
( ( sk_c11 = multiply(inverse(sk_c11),sk_c10) )
| ( sk_c11 != multiply(sk_c9,sk_c10) )
| ( multiply(inverse(sk_c11),sk_c10) != multiply(sk_c9,sk_c10) ) ),
inference(instantiation,[status(thm)],[c_84125]) ).
tcf(c_84133,plain,
! [X0: $i] :
( ( sk_c11 = sk_c10 )
| ( sk_c10 != X0 )
| ( sk_c11 != X0 ) ),
inference(instantiation,[status(thm)],[c_727]) ).
tcf(c_84172,plain,
! [X0: $i,X1: $i] :
( ( inverse(sk_c4) = multiply(X0,X1) )
| ( inverse(sk_c4) != multiply(sk_c11,sk_c2) )
| ( multiply(X0,X1) != multiply(sk_c11,sk_c2) ) ),
inference(instantiation,[status(thm)],[c_59943]) ).
tcf(c_84175,plain,
( ( inverse(sk_c4) = multiply(sk_c11,sk_c11) )
| ( inverse(sk_c4) != multiply(sk_c11,sk_c2) )
| ( multiply(sk_c11,sk_c11) != multiply(sk_c11,sk_c2) ) ),
inference(instantiation,[status(thm)],[c_84172]) ).
tcf(c_84425,plain,
! [X0: $i] :
( ( X0 = multiply(sk_c1,sk_c11) )
| ( X0 != multiply(sk_c9,sk_c10) )
| ( multiply(sk_c1,sk_c11) != multiply(sk_c9,sk_c10) ) ),
inference(instantiation,[status(thm)],[c_60102]) ).
tcf(c_84427,plain,
( ( sk_c11 = multiply(sk_c1,sk_c11) )
| ( sk_c11 != multiply(sk_c9,sk_c10) )
| ( multiply(sk_c1,sk_c11) != multiply(sk_c9,sk_c10) ) ),
inference(instantiation,[status(thm)],[c_84425]) ).
tcf(c_84430,plain,
( ( identity = multiply(sk_c9,sk_c10) )
| ( identity != sk_c11 )
| ( multiply(sk_c9,sk_c10) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_77073]) ).
tcf(c_84432,plain,
( ( inverse(sk_c4) = identity )
| ( identity != multiply(sk_c9,sk_c10) )
| ( inverse(sk_c4) != multiply(sk_c9,sk_c10) ) ),
inference(instantiation,[status(thm)],[c_71101]) ).
tcf(c_84521,plain,
( ( multiply(sk_c1,sk_c11) = multiply(sk_c9,sk_c10) )
| ( multiply(sk_c1,sk_c11) != sk_c2 )
| ( multiply(sk_c9,sk_c10) != sk_c2 ) ),
inference(instantiation,[status(thm)],[c_59885]) ).
tcf(c_84913,plain,
( ( multiply(sk_c1,sk_c11) = sk_c2 )
| ( sk_c2 != multiply(sk_c1,sk_c11) )
| ( multiply(sk_c1,sk_c11) != multiply(sk_c1,sk_c11) ) ),
inference(instantiation,[status(thm)],[c_59889]) ).
tcf(c_85152,plain,
( ( sk_c11 = sk_c2 )
| ( sk_c2 != multiply(sk_c1,sk_c11) )
| ( sk_c11 != multiply(sk_c1,sk_c11) ) ),
inference(instantiation,[status(thm)],[c_77090]) ).
tcf(c_85163,plain,
( ( sk_c11 = sk_c2 )
| ( sk_c2 != multiply(sk_c9,sk_c10) )
| ( sk_c11 != multiply(sk_c9,sk_c10) ) ),
inference(instantiation,[status(thm)],[c_77090]) ).
tcf(c_85405,plain,
! [X0: $i,X1: $i] :
( ( inverse(sk_c4) = X1 )
| ( X1 != multiply(inverse(X0),sk_c10) )
| ( inverse(sk_c4) != multiply(inverse(X0),sk_c10) ) ),
inference(instantiation,[status(thm)],[c_66691]) ).
tcf(c_85406,plain,
( ( inverse(sk_c4) = sk_c11 )
| ( sk_c11 != multiply(inverse(sk_c11),sk_c10) )
| ( inverse(sk_c4) != multiply(inverse(sk_c11),sk_c10) ) ),
inference(instantiation,[status(thm)],[c_85405]) ).
tcf(c_85770,plain,
! [X0: $i] : multiply(sk_c8,multiply(sk_c5,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_76092,c_115]) ).
tcf(c_85808,plain,
! [X0: $i] : multiply(sk_c8,multiply(sk_c5,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_85770,c_113]) ).
tcf(c_85814,plain,
( ( multiply(sk_c8,sk_c11) = sk_c8 )
| ( multiply(sk_c9,sk_c10) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_140,c_85808]) ).
tcf(c_85815,plain,
( ( multiply(sk_c8,sk_c11) = sk_c8 )
| ( multiply(sk_c11,sk_c10) = sk_c9 ) ),
inference(superposition,[status(thm)],[c_120,c_85808]) ).
tcf(c_85880,plain,
inverse(sk_c4) = sk_c10,
inference(global_subsumption_just,[status(thm)],[c_33608,c_139,c_731,c_732,c_1045,c_1063,c_1064,c_1069,c_1070,c_1386,c_2575,c_3949,c_4133,c_4534,c_5072,c_5265,c_5569,c_7326,c_9381,c_10759,c_11513,c_17576,c_19742,c_19796,c_20057,c_20751,c_20778,c_20868,c_22082,c_27299,c_27300,c_32917,c_32986,c_33051,c_33315,c_33472,c_42442,c_46537,c_52976,c_59677,c_60095,c_60426,c_60564,c_62119,c_64692,c_64714]) ).
tcf(c_85922,plain,
! [X0: $i] : multiply(sk_c4,multiply(sk_c10,X0)) = X0,
inference(superposition,[status(thm)],[c_85880,c_30552]) ).
tcf(c_85923,plain,
multiply(sk_c4,sk_c10) = identity,
inference(superposition,[status(thm)],[c_85880,c_30328]) ).
tcf(c_85924,plain,
inverse(sk_c10) = sk_c4,
inference(superposition,[status(thm)],[c_85880,c_8093]) ).
tcf(c_85925,plain,
multiply(sk_c10,sk_c4) = identity,
inference(superposition,[status(thm)],[c_85880,c_114]) ).
tcf(c_85950,plain,
multiply(sk_c9,sk_c10) = sk_c11,
inference(global_subsumption_just,[status(thm)],[c_85814,c_732,c_1386,c_1602,c_1630,c_1631,c_2575,c_3956,c_3962,c_3968,c_4534,c_19783,c_19998,c_20779,c_26518,c_33511,c_53684,c_60147,c_62667,c_62740,c_76090,c_85923]) ).
tcf(c_85970,plain,
! [X0: $i] :
( ~ iPr_def_11
| ( sk_c11 != identity )
| ( X0 != sk_c9 )
| ( multiply(X0,sk_c9) != inverse(X0) ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_32980,c_85950]) ).
tcf(c_85971,plain,
( iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( multiply(sk_c11,sk_c10) != sk_c9 ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_32974,c_85950]) ).
tcf(c_85973,plain,
( ~ iPr_def_11
| ( sk_c11 != identity )
| ( sk_c11 != sk_c9 )
| ( multiply(sk_c11,sk_c9) != inverse(sk_c11) ) ),
inference(instantiation,[status(thm)],[c_85970]) ).
tcf(c_86009,plain,
! [X0: $i] : multiply(sk_c10,multiply(sk_c4,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_85925,c_115]) ).
tcf(c_86189,plain,
inverse(sk_c3) = sk_c11,
inference(global_subsumption_just,[status(thm)],[c_33615,c_157,c_731,c_732,c_1045,c_1386,c_2575,c_4011,c_4073,c_4072,c_4534,c_5072,c_5265,c_5569,c_8166,c_9381,c_12352,c_17576,c_17599,c_17600,c_19742,c_19796,c_20751,c_20778,c_20868,c_24111,c_30829,c_32917,c_33051,c_33343,c_33500,c_38540,c_39236,c_42433,c_52980,c_60095,c_60283,c_60564,c_62119,c_64714,c_76360,c_76361]) ).
tcf(c_86216,plain,
( ( multiply(sk_c11,sk_c10) = sk_c9 )
| ~ iPr_def_13
| ( multiply(sk_c11,sk_c10) != sk_c10 ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_30766,c_86189]) ).
tcf(c_86217,plain,
( ( multiply(sk_c11,sk_c2) = sk_c10 )
| ~ iPr_def_13
| ( multiply(sk_c11,sk_c10) != sk_c10 ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_30764,c_86189]) ).
tcf(c_86218,plain,
( ( multiply(sk_c1,sk_c11) = sk_c2 )
| ~ iPr_def_13
| ( multiply(sk_c11,sk_c10) != sk_c10 ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_30763,c_86189]) ).
tcf(c_86226,plain,
multiply(sk_c3,sk_c11) = identity,
inference(superposition,[status(thm)],[c_86189,c_30328]) ).
tcf(c_86227,plain,
inverse(sk_c11) = sk_c3,
inference(superposition,[status(thm)],[c_86189,c_8093]) ).
tcf(c_86228,plain,
multiply(sk_c11,sk_c3) = identity,
inference(superposition,[status(thm)],[c_86189,c_114]) ).
tcf(c_86258,plain,
! [X0: $i] : multiply(sk_c11,multiply(sk_c3,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_86228,c_115]) ).
tcf(c_86263,plain,
! [X0: $i] : multiply(sk_c10,multiply(sk_c4,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_86009,c_113]) ).
tcf(c_86276,plain,
multiply(sk_c10,identity) = inverse(sk_c4),
inference(superposition,[status(thm)],[c_30328,c_86263]) ).
tcf(c_86327,plain,
! [X0: $i] : multiply(sk_c11,multiply(sk_c3,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_86258,c_113]) ).
tcf(c_86331,plain,
( ( multiply(sk_c1,sk_c11) = sk_c2 )
| ( multiply(sk_c11,sk_c10) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_156,c_86327]) ).
tcf(c_86332,plain,
( ( multiply(sk_c11,sk_c2) = sk_c10 )
| ( multiply(sk_c11,sk_c10) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_146,c_86327]) ).
tcf(c_86337,plain,
multiply(sk_c11,identity) = inverse(sk_c3),
inference(superposition,[status(thm)],[c_30328,c_86327]) ).
tcf(c_86427,plain,
( ( multiply(sk_c9,sk_c10) = sk_c2 )
| ( multiply(sk_c11,sk_c10) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_86332,c_33091]) ).
tcf(c_87210,plain,
( ( multiply(sk_c11,sk_c10) = sk_c9 )
| ~ iPr_def_13 ),
inference(global_subsumption_just,[status(thm)],[c_86216,c_2575,c_3955,c_3967,c_20778,c_30781,c_53684,c_60147,c_62667,c_62740,c_76090,c_86226]) ).
tcf(c_87214,plain,
( ( multiply(sk_c11,sk_c2) = sk_c10 )
| ~ iPr_def_13 ),
inference(global_subsumption_just,[status(thm)],[c_86217,c_2575,c_3957,c_3969,c_20778,c_30781,c_53684,c_60147,c_62667,c_62740,c_76090,c_86226]) ).
tcf(c_87218,plain,
( ( multiply(sk_c1,sk_c11) = sk_c2 )
| ~ iPr_def_13 ),
inference(global_subsumption_just,[status(thm)],[c_86218,c_139,c_160,c_156,c_731,c_732,c_1045,c_1063,c_1064,c_1069,c_1070,c_1385,c_1386,c_1752,c_2273,c_2575,c_3018,c_3949,c_4133,c_4534,c_5072,c_5265,c_5569,c_7326,c_9381,c_10759,c_11513,c_17576,c_19742,c_19796,c_20057,c_20751,c_20778,c_20868,c_22082,c_27299,c_27300,c_30781,c_32917,c_32986,c_33051,c_33315,c_33472,c_42429,c_42442,c_46537,c_52976,c_59677,c_60095,c_60147,c_60426,c_60564,c_62119,c_62740,c_64692,c_64714,c_76090,c_79483,c_86226]) ).
tcf(c_87321,plain,
( ( sk_c2 = identity )
| ~ iPr_def_10 ),
inference(global_subsumption_just,[status(thm)],[c_49992,c_169,c_167,c_731,c_732,c_1045,c_1063,c_1064,c_1069,c_1070,c_1630,c_1631,c_2061,c_2116,c_2575,c_3230,c_4422,c_4783,c_5072,c_5203,c_5265,c_5369,c_5569,c_8166,c_9381,c_10759,c_19742,c_19796,c_19998,c_20751,c_20757,c_20758,c_20778,c_20779,c_20868,c_22082,c_23042,c_26518,c_30781,c_32917,c_32986,c_50292]) ).
tcf(c_87347,plain,
( ( multiply(sk_c10,sk_c11) = sk_c10 )
| ( multiply(sk_c11,sk_c10) = sk_c9 ) ),
inference(light_normalisation,[status(thm)],[c_30467,c_32978,c_85880,c_86189,c_86276,c_86337]) ).
tcf(c_87579,plain,
( ( sk_c2 = identity )
| ( multiply(sk_c11,multiply(sk_c4,identity)) = sk_c11 ) ),
inference(light_normalisation,[status(thm)],[c_30641,c_33051,c_85924,c_86189,c_86337]) ).
tcf(c_87580,plain,
( ( sk_c2 = identity )
| ( multiply(sk_c11,sk_c4) = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_87579,c_30555]) ).
tcf(c_90003,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(inverse(multiply(X0,X1)),multiply(X0,multiply(X1,X2))) = X2,
inference(superposition,[status(thm)],[c_115,c_30570]) ).
tcf(c_90027,plain,
( ( multiply(sk_c11,sk_c10) = sk_c9 )
| ( multiply(inverse(sk_c10),sk_c10) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_87347,c_30570]) ).
tcf(c_90038,plain,
! [X0: $i] : multiply(inverse(sk_c10),X0) = multiply(sk_c4,X0),
inference(superposition,[status(thm)],[c_86263,c_30570]) ).
tcf(c_90177,plain,
( ( multiply(sk_c4,sk_c10) = sk_c11 )
| ( multiply(sk_c11,sk_c10) = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_90027,c_90038]) ).
tcf(c_90660,plain,
! [X0: $i] :
( ( multiply(sk_c1,sk_c11) = sk_c2 )
| ( multiply(inverse(sk_c9),multiply(sk_c4,multiply(sk_c10,X0))) = X0 ) ),
inference(superposition,[status(thm)],[c_158,c_90003]) ).
tcf(c_90661,plain,
! [X0: $i] :
( ( multiply(sk_c11,sk_c2) = sk_c10 )
| ( multiply(inverse(sk_c9),multiply(sk_c4,multiply(sk_c10,X0))) = X0 ) ),
inference(superposition,[status(thm)],[c_148,c_90003]) ).
tcf(c_90662,plain,
! [X0: $i] :
( ( multiply(sk_c11,sk_c10) = sk_c9 )
| ( multiply(inverse(sk_c9),multiply(sk_c4,multiply(sk_c10,X0))) = X0 ) ),
inference(superposition,[status(thm)],[c_118,c_90003]) ).
tcf(c_90925,plain,
! [X0: $i,X1: $i] : multiply(inverse(multiply(X0,X1)),multiply(X0,identity)) = inverse(X1),
inference(superposition,[status(thm)],[c_30328,c_90003]) ).
tcf(c_91374,plain,
! [X0: $i,X1: $i] : multiply(inverse(multiply(X0,X1)),X0) = inverse(X1),
inference(light_normalisation,[status(thm)],[c_90925,c_30555]) ).
tcf(c_91382,plain,
( ( multiply(sk_c1,sk_c11) = sk_c2 )
| ( multiply(inverse(sk_c9),sk_c4) = inverse(sk_c10) ) ),
inference(superposition,[status(thm)],[c_158,c_91374]) ).
tcf(c_91421,plain,
( ( multiply(sk_c11,sk_c10) = sk_c9 )
| ( multiply(inverse(sk_c8),sk_c8) = inverse(sk_c11) ) ),
inference(superposition,[status(thm)],[c_85815,c_91374]) ).
tcf(c_91452,plain,
! [X0: $i] : multiply(inverse(X0),X0) = inverse(identity),
inference(superposition,[status(thm)],[c_30555,c_91374]) ).
tcf(c_91558,plain,
( ( inverse(sk_c11) = inverse(identity) )
| ( multiply(sk_c11,sk_c10) = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_91421,c_91452]) ).
tcf(c_91874,plain,
( ( sk_c2 = identity )
| ( multiply(sk_c11,sk_c4) = sk_c4 ) ),
inference(light_normalisation,[status(thm)],[c_91382,c_32978,c_33051,c_85924]) ).
tcf(c_91898,plain,
( ( sk_c2 = identity )
| ( sk_c11 = sk_c4 ) ),
inference(superposition,[status(thm)],[c_91874,c_87580]) ).
tcf(c_95448,plain,
! [X0: $i] :
( ( sk_c2 = identity )
| ( multiply(sk_c11,X0) = X0 ) ),
inference(light_normalisation,[status(thm)],[c_90660,c_32978,c_33051,c_85922]) ).
tcf(c_95480,plain,
( ( sk_c2 = identity )
| ( sk_c11 = sk_c10 ) ),
inference(superposition,[status(thm)],[c_95448,c_50263]) ).
tcf(c_95525,plain,
( ( sk_c2 = identity )
| ( inverse(sk_c11) = identity ) ),
inference(superposition,[status(thm)],[c_95448,c_30328]) ).
tcf(c_96164,plain,
! [X0: $i] :
( ( multiply(sk_c11,sk_c2) = sk_c10 )
| ( multiply(sk_c11,X0) = X0 ) ),
inference(light_normalisation,[status(thm)],[c_90661,c_32978,c_85922]) ).
tcf(c_96209,plain,
! [X0: $i] :
( ( multiply(sk_c11,X0) = X0 )
| ( multiply(inverse(sk_c11),sk_c10) = sk_c2 ) ),
inference(superposition,[status(thm)],[c_96164,c_30570]) ).
tcf(c_96262,plain,
( ( inverse(sk_c11) = identity )
| ( multiply(sk_c11,sk_c2) = sk_c10 ) ),
inference(superposition,[status(thm)],[c_96164,c_30328]) ).
tcf(c_96297,plain,
( ( multiply(sk_c11,sk_c11) = sk_c11 )
| ( multiply(inverse(sk_c11),sk_c10) = sk_c2 ) ),
inference(instantiation,[status(thm)],[c_96209]) ).
tcf(c_96656,plain,
! [X0: $i] :
( ( inverse(sk_c4) = multiply(inverse(X0),sk_c10) )
| ( inverse(sk_c4) != multiply(identity,sk_c10) )
| ( multiply(inverse(X0),sk_c10) != multiply(identity,sk_c10) ) ),
inference(instantiation,[status(thm)],[c_77731]) ).
tcf(c_96657,plain,
( ( inverse(sk_c4) = multiply(inverse(sk_c11),sk_c10) )
| ( inverse(sk_c4) != multiply(identity,sk_c10) )
| ( multiply(inverse(sk_c11),sk_c10) != multiply(identity,sk_c10) ) ),
inference(instantiation,[status(thm)],[c_96656]) ).
tcf(c_96829,plain,
! [X0: $i] :
( ( multiply(sk_c11,sk_c10) = sk_c9 )
| ( multiply(sk_c11,X0) = X0 ) ),
inference(light_normalisation,[status(thm)],[c_90662,c_32978,c_85922]) ).
tcf(c_96887,plain,
! [X0: $i] :
( ( multiply(sk_c11,X0) = X0 )
| ~ iPr_def_12
| ( inverse(sk_c11) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_96829,c_723]) ).
tcf(c_96938,plain,
( ( inverse(sk_c11) = identity )
| ( multiply(sk_c11,sk_c10) = sk_c9 ) ),
inference(superposition,[status(thm)],[c_96829,c_30328]) ).
tcf(c_96967,plain,
( ( multiply(sk_c11,sk_c10) = sk_c9 )
| ( sk_c10 != sk_c9 ) ),
inference(equality_factoring,[status(thm)],[c_96829]) ).
tcf(c_97454,plain,
! [X0: $i] :
( ( multiply(inverse(X0),sk_c10) = multiply(identity,sk_c10) )
| ( multiply(identity,sk_c10) != inverse(sk_c4) )
| ( multiply(inverse(X0),sk_c10) != inverse(sk_c4) ) ),
inference(instantiation,[status(thm)],[c_77276]) ).
tcf(c_97455,plain,
( ( multiply(inverse(sk_c11),sk_c10) = multiply(identity,sk_c10) )
| ( multiply(identity,sk_c10) != inverse(sk_c4) )
| ( multiply(inverse(sk_c11),sk_c10) != inverse(sk_c4) ) ),
inference(instantiation,[status(thm)],[c_97454]) ).
tcf(c_97877,plain,
! [X0: $i] :
( ( multiply(sk_c11,X0) = X0 )
| ~ iPr_def_12 ),
inference(global_subsumption_just,[status(thm)],[c_96887,c_159,c_149,c_139,c_731,c_732,c_1045,c_1063,c_1064,c_1069,c_1070,c_1383,c_1384,c_1385,c_1386,c_1602,c_1630,c_1631,c_2084,c_2119,c_2575,c_3063,c_3241,c_3949,c_3956,c_3962,c_3968,c_3995,c_4133,c_4525,c_4534,c_5072,c_5265,c_5569,c_7325,c_7326,c_8164,c_9243,c_9381,c_9806,c_10557,c_10759,c_11513,c_17576,c_17580,c_19742,c_19783,c_19796,c_19998,c_20057,c_20751,c_20756,c_20778,c_20779,c_20868,c_22082,c_26518,c_26766,c_27299,c_27300,c_32917,c_32986,c_33051,c_33315,c_33472,c_33511,c_38868,c_42431,c_42442,c_46537,c_50827,c_52976,c_53684,c_58664,c_59677,c_60095,c_60110,c_60147,c_60426,c_60564,c_62119,c_62667,c_62740,c_64692,c_64714,c_64717,c_71125,c_76090,c_77277,c_77798,c_84127,c_84175,c_85152,c_85406,c_85923,c_96209,c_96657,c_97455]) ).
tcf(c_97879,plain,
( ( multiply(sk_c11,sk_c11) = sk_c11 )
| ~ iPr_def_12 ),
inference(instantiation,[status(thm)],[c_97877]) ).
tcf(c_100673,plain,
! [X0: $i,X1: $i] :
( ( identity = multiply(X0,X1) )
| ( identity != identity )
| ( multiply(X0,X1) != identity ) ),
inference(instantiation,[status(thm)],[c_59794]) ).
tcf(c_100677,plain,
( ( identity = multiply(sk_c11,sk_c11) )
| ( identity != identity )
| ( multiply(sk_c11,sk_c11) != identity ) ),
inference(instantiation,[status(thm)],[c_100673]) ).
tcf(c_101089,plain,
! [X0: $i,X1: $i] :
( ( sk_c11 = sk_c10 )
| ( sk_c10 != multiply(X0,X1) )
| ( sk_c11 != multiply(X0,X1) ) ),
inference(instantiation,[status(thm)],[c_84133]) ).
tcf(c_101093,plain,
( ( sk_c11 = sk_c10 )
| ( sk_c10 != multiply(sk_c11,sk_c11) )
| ( sk_c11 != multiply(sk_c11,sk_c11) ) ),
inference(instantiation,[status(thm)],[c_101089]) ).
tcf(c_101156,plain,
! [X0: $i,X1: $i] :
( ( inverse(sk_c3) = identity )
| ( identity != multiply(X0,X1) )
| ( inverse(sk_c3) != multiply(X0,X1) ) ),
inference(instantiation,[status(thm)],[c_70899]) ).
tcf(c_101170,plain,
( ( inverse(sk_c3) = identity )
| ( identity != multiply(sk_c11,sk_c11) )
| ( inverse(sk_c3) != multiply(sk_c11,sk_c11) ) ),
inference(instantiation,[status(thm)],[c_101156]) ).
tcf(c_101394,plain,
( iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10 ),
inference(global_subsumption_just,[status(thm)],[c_21585,c_157,c_139,c_731,c_732,c_725,c_1045,c_1063,c_1064,c_1069,c_1070,c_1125,c_1384,c_1385,c_1386,c_1497,c_1602,c_1630,c_1631,c_2278,c_2575,c_2580,c_3035,c_3034,c_3188,c_3316,c_3949,c_3956,c_3955,c_3962,c_3968,c_3967,c_4011,c_4073,c_4072,c_4133,c_4132,c_4534,c_5072,c_5265,c_5569,c_7309,c_7310,c_7325,c_7326,c_8166,c_8164,c_9243,c_9381,c_10083,c_10139,c_10561,c_10566,c_10680,c_10739,c_10759,c_11513,c_11895,c_12352,c_17576,c_17580,c_17596,c_17599,c_17600,c_19742,c_19740,c_19783,c_19796,c_19826,c_19998,c_20007,c_20057,c_20397,c_20751,c_20756,c_20778,c_20779,c_20802,c_20868,c_22082,c_22911,c_24111,c_24329,c_26518,c_26765,c_26766,c_27299,c_27300,c_30781,c_30829,c_32917,c_32986,c_33051,c_33315,c_33343,c_33472,c_33500,c_33511,c_38540,c_39171,c_39236,c_41931,c_42431,c_42433,c_42442,c_44856,c_46537,c_50695,c_52976,c_52980,c_53684,c_54586,c_55397,c_57239,c_58664,c_59677,c_60095,c_60110,c_60147,c_60283,c_60426,c_60564,c_62119,c_62667,c_62740,c_64692,c_64714,c_64717,c_76090,c_76360,c_76361,c_77159,c_77160,c_77798,c_84127,c_84427,c_84430,c_84432,c_84521,c_85152,c_85923,c_86226,c_86427,c_87210,c_87214,c_87218,c_90177,c_96297,c_96967,c_97879,c_100677,c_101093,c_101170]) ).
tcf(c_101838,plain,
! [X0: $i] :
( ( X0 != sk_c9 )
| ( multiply(sk_c11,sk_c10) = X0 ) ),
inference(global_subsumption_just,[status(thm)],[c_9304,c_731,c_732,c_1045,c_1063,c_1064,c_1386,c_1602,c_1630,c_1631,c_2575,c_3956,c_3962,c_3968,c_4534,c_5072,c_5265,c_5569,c_9243,c_9381,c_9554,c_10268,c_10558,c_17580,c_19742,c_19783,c_19796,c_19998,c_20751,c_20778,c_20779,c_20868,c_26518,c_30827,c_32917,c_33511,c_42431,c_50827,c_52162,c_53684,c_58664,c_60147,c_62667,c_62740,c_76090,c_85923,c_87210,c_91558,c_96938,c_101394]) ).
tcf(c_101839,plain,
! [X0: $i] :
( ( multiply(sk_c11,sk_c10) = X0 )
| ( X0 != sk_c9 ) ),
inference(renaming,[status(thm)],[c_101838]) ).
tcf(c_101857,plain,
! [X0: $i,X1: $i] :
( ( inverse(X1) = multiply(sk_c11,sk_c10) )
| ( X1 != X0 )
| ( inverse(X0) != sk_c9 ) ),
inference(resolution,[status(thm)],[c_101839,c_2544]) ).
tcf(c_101858,plain,
( ( inverse(sk_c11) = multiply(sk_c11,sk_c10) )
| ( sk_c11 != sk_c11 )
| ( inverse(sk_c11) != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_101857]) ).
tcf(c_101921,plain,
sk_c2 = multiply(sk_c1,sk_c11),
inference(global_subsumption_just,[status(thm)],[c_9796,c_157,c_139,c_731,c_732,c_725,c_1045,c_1063,c_1064,c_1069,c_1070,c_1125,c_1384,c_1385,c_1386,c_1497,c_1602,c_1630,c_1631,c_2278,c_2575,c_2580,c_3035,c_3034,c_3188,c_3316,c_3949,c_3956,c_3955,c_3962,c_3968,c_3967,c_4011,c_4073,c_4072,c_4133,c_4132,c_4534,c_5072,c_5265,c_5569,c_7309,c_7310,c_7325,c_7326,c_8166,c_8164,c_9243,c_9381,c_9795,c_9811,c_10083,c_10139,c_10561,c_10566,c_10680,c_10733,c_10739,c_10759,c_11513,c_11895,c_12352,c_17576,c_17580,c_17596,c_17599,c_17600,c_19742,c_19740,c_19783,c_19796,c_19826,c_19998,c_20007,c_20057,c_20397,c_20751,c_20756,c_20778,c_20779,c_20802,c_20868,c_22082,c_22911,c_24111,c_24329,c_26518,c_26765,c_26766,c_27299,c_27300,c_30781,c_30829,c_32917,c_32986,c_33051,c_33056,c_33315,c_33343,c_33472,c_33500,c_33511,c_38540,c_39171,c_39236,c_41931,c_42431,c_42433,c_42442,c_44856,c_46537,c_50695,c_52976,c_52980,c_53684,c_54586,c_55397,c_57239,c_58664,c_59677,c_60095,c_60110,c_60147,c_60283,c_60426,c_60564,c_62119,c_62667,c_62740,c_64692,c_64714,c_64717,c_76090,c_76360,c_76361,c_77159,c_77160,c_77798,c_84127,c_84427,c_84430,c_84432,c_84521,c_85152,c_85923,c_86226,c_86331,c_86427,c_87210,c_87214,c_87218,c_90177,c_96297,c_96967,c_97879,c_100677,c_101093,c_101170,c_101858]) ).
tcf(c_101998,plain,
multiply(sk_c11,sk_c2) = sk_c10,
inference(global_subsumption_just,[status(thm)],[c_12106,c_157,c_139,c_731,c_732,c_725,c_1045,c_1063,c_1064,c_1069,c_1070,c_1125,c_1384,c_1385,c_1386,c_1497,c_1602,c_1630,c_1631,c_2064,c_2278,c_2575,c_2580,c_3035,c_3034,c_3188,c_3316,c_3949,c_3956,c_3955,c_3962,c_3968,c_3967,c_4011,c_4073,c_4072,c_4133,c_4132,c_4534,c_5072,c_5265,c_5569,c_7309,c_7310,c_7325,c_7326,c_8166,c_8164,c_9243,c_9381,c_9795,c_9811,c_10083,c_10139,c_10561,c_10566,c_10680,c_10733,c_10739,c_10759,c_11513,c_11895,c_12352,c_17576,c_17580,c_17596,c_17599,c_17600,c_19742,c_19740,c_19783,c_19796,c_19826,c_19998,c_20007,c_20057,c_20397,c_20751,c_20756,c_20778,c_20779,c_20802,c_20868,c_22082,c_22911,c_24111,c_24329,c_26518,c_26765,c_26766,c_27299,c_27300,c_30781,c_30827,c_30829,c_32917,c_32986,c_33051,c_33056,c_33315,c_33343,c_33472,c_33500,c_33511,c_38540,c_39171,c_39236,c_41931,c_42431,c_42433,c_42442,c_44856,c_46537,c_50695,c_50827,c_52976,c_52980,c_53684,c_54586,c_55397,c_57239,c_58664,c_59677,c_60095,c_60110,c_60147,c_60283,c_60426,c_60564,c_62119,c_62667,c_62740,c_63390,c_64692,c_64714,c_64717,c_64804,c_76090,c_76360,c_76361,c_77159,c_77160,c_77798,c_84127,c_84427,c_84430,c_84432,c_84521,c_84913,c_85152,c_85923,c_86226,c_86331,c_86427,c_87210,c_87214,c_87218,c_90177,c_96262,c_96297,c_96967,c_97879,c_100677,c_101093,c_101170,c_101858]) ).
tcf(c_102008,plain,
! [X0: $i,X1: $i] :
( ( multiply(sk_c1,sk_c11) = X0 )
| ( X0 != X1 )
| ( X1 != sk_c2 ) ),
inference(global_subsumption_just,[status(thm)],[c_13959,c_178,c_731,c_732,c_1063,c_1064,c_1069,c_1070,c_1125,c_1385,c_1386,c_1405,c_1602,c_1752,c_2273,c_2575,c_2727,c_3018,c_3068,c_6253,c_7309,c_8164,c_8679,c_9243,c_10083,c_10759,c_13959,c_14004,c_17576,c_17580,c_17593,c_17594,c_17596,c_19783,c_20007,c_20756,c_22082,c_24329,c_30781,c_32920,c_33051,c_42431,c_43228,c_44237,c_54586,c_57239,c_58664,c_60095,c_60110,c_60564,c_62119,c_63390,c_64714,c_64717,c_65173,c_65174,c_77798,c_78370,c_84127,c_84427,c_84521,c_84913,c_85880,c_85923,c_85950,c_85971,c_85973,c_86189,c_86227,c_86427,c_96297,c_100677,c_101170,c_101858,c_101921]) ).
tcf(c_102009,plain,
! [X0: $i,X1: $i] :
( ( multiply(sk_c1,sk_c11) = X0 )
| ( X1 != sk_c2 )
| ( X0 != X1 ) ),
inference(renaming,[status(thm)],[c_102008]) ).
tcf(c_102058,plain,
! [X0: $i,X1: $i] :
( ( multiply(sk_c1,sk_c11) = X0 )
| ( sk_c2 != identity )
| ( X0 != multiply(inverse(X1),X1) ) ),
inference(resolution,[status(thm)],[c_102009,c_2539]) ).
tcf(c_102059,plain,
( ( multiply(sk_c1,sk_c11) = sk_c11 )
| ( sk_c2 != identity )
| ( sk_c11 != multiply(inverse(sk_c11),sk_c11) ) ),
inference(instantiation,[status(thm)],[c_102058]) ).
tcf(c_102502,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_102059,c_101998,c_101921,c_101858,c_101170,c_101093,c_100677,c_96297,c_95525,c_95480,c_91898,c_87321,c_86427,c_86189,c_85971,c_85950,c_85880,c_85163,c_85152,c_84913,c_84521,c_84427,c_84127,c_79594,c_77798,c_76090,c_64804,c_63390,c_63071,c_62740,c_62741,c_62384,c_62119,c_61478,c_60147,c_60110,c_60105,c_60095,c_59677,c_58664,c_57387,c_57239,c_55752,c_54586,c_50827,c_42431,c_41931,c_33051,c_32987,c_32986,c_32920,c_30827,c_30781,c_27300,c_27299,c_26766,c_26765,c_24329,c_22082,c_20756,c_20007,c_19074,c_19019,c_17596,c_17594,c_17593,c_17580,c_17576,c_10759,c_10561,c_10083,c_9243,c_7627,c_7326,c_7325,c_7309,c_6253,c_6254,c_5380,c_4534,c_4132,c_4133,c_3258,c_3067,c_2924,c_2575,c_2423,c_2181,c_1386,c_1385,c_1125,c_1070,c_1069,c_1064,c_1063,c_732,c_731]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GRP307-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.07/0.35 % Computer : n002.cluster.edu
% 0.07/0.35 % Model : x86_64 x86_64
% 0.07/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.35 % Memory : 8046.5625MB
% 0.07/0.35 % OS : Linux 6.8.0-71-generic
% 0.07/0.35 % CPULimit : 300
% 0.07/0.35 % WCLimit : 300
% 0.07/0.35 % DateTime : Wed Sep 23 14:28:05 UTC 2026
% 0.07/0.35 % CPUTime :
% 0.07/0.35 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.12/0.39 Running first-order theorem proving
% 0.12/0.39 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.12/0.40
% 0.12/0.40 % ======== iProver multi-core TPTP/SMT =========
% 0.12/0.40
% 0.12/0.40 % Detected problem language: tptp
% 0.12/0.42 % Proving...
% 73.90/10.91 % SZS status Started for theBenchmark.p
% 73.90/10.91 % SZS status Unsatisfiable for theBenchmark.p
% 73.90/10.91
% 73.90/10.91 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 73.90/10.91
% 73.90/10.91 % ------ iProver source info
% 73.90/10.91
% 73.90/10.91 % git: date: 2026-07-19 20:42:38 +0200
% 73.90/10.91 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 73.90/10.91 % git: non_committed_changes: false
% 73.90/10.91
% 73.90/10.91 % ------ Parsing...% successful
% 73.90/10.91
% 73.90/10.91
% 73.90/10.91 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 73.90/10.91
% 73.90/10.91 % ------ Preprocessing... sup_sim: 0 sf_s rm: 0 0s sf_e pe_s pe_e %
% 73.90/10.91
% 73.90/10.91 % ------ Preprocessing... gs_s sp: 4 0s gs_e snvd_s sp: 0 0s snvd_e %
% 73.90/10.91
% 73.90/10.91 % ------ Preprocessing... sf_s rm: 0 0s sf_e
% 73.90/10.91 % ------ Proving...
% 73.90/10.91 % ------ Problem Properties
% 73.90/10.91
% 73.90/10.91 %
% 73.90/10.91 % clauses 68
% 73.90/10.91 % conjectures 65
% 73.90/10.91 % EPR 0
% 73.90/10.91 % Horn 7
% 73.90/10.91 % unary 3
% 73.90/10.91 % binary 60
% 73.90/10.91 % lits 144
% 73.90/10.91 % lits eq 136
% 73.90/10.91 % fd_pure 0
% 73.90/10.91 % fd_pseudo 0
% 73.90/10.91 % fd_cond 0
% 73.90/10.91 % fd_pseudo_cond 0
% 73.90/10.91 % AC symbols 0
% 73.90/10.91
% 73.90/10.91 % ------ Input Options Time Limit: Unbounded
% 73.90/10.91
% 73.90/10.91
% 73.90/10.91 % ------
% 73.90/10.91 % Current options:
% 73.90/10.91 % ------
% 73.90/10.91
% 73.90/10.91
% 73.90/10.91 %
% 73.90/10.91
% 73.90/10.91 % ------ Proving...
% 73.90/10.91 %
% 73.90/10.91
% 73.90/10.91 % SZS status Unsatisfiable for theBenchmark.p
% 73.90/10.91
% 73.90/10.91 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 73.90/10.93
% 73.90/10.93
%------------------------------------------------------------------------------