%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : GRP386-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 : n026.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 01:33:37 PM UTC 2026
% Result : Unsatisfiable 72.69s 18.68s
% Output : CNFRefutation 93.44s
% Verified :
% SZS Type : Refutation
% Derivation depth : 50
% Number of leaves : 59
% Syntax : Number of formulae : 1031 ( 189 unt; 14 def)
% Number of atoms : 3976 (2295 equ)
% Maximal formula atoms : 15 ( 3 avg)
% Number of connectives : 2380 ( 980 ~;1400 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 23 ( 3 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 20 ( 18 usr; 19 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 11 con; 0-2 aty)
% Number of variables : 503 ( 0 sgn 503 !; 0 ?; 472 :)
% 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_c2,sk_c10) = sk_c9
| inverse(sk_c10) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_1) ).
fof(f6,plain,
( sk_c9 = multiply(sk_c2,sk_c10)
| inverse(sk_c10) = sk_c9 ),
inference(reorient_equations,[],[f5]) ).
fof(f9,negated_conjecture,
( multiply(sk_c3,sk_c9) = sk_c8
| inverse(sk_c10) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_3) ).
fof(f10,negated_conjecture,
( inverse(sk_c3) = sk_c9
| inverse(sk_c10) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_4) ).
fof(f11,plain,
( sk_c9 = inverse(sk_c3)
| inverse(sk_c10) = sk_c9 ),
inference(reorient_equations,[],[f10]) ).
fof(f12,negated_conjecture,
( multiply(sk_c4,sk_c7) = sk_c10
| inverse(sk_c10) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_5) ).
fof(f13,plain,
( sk_c10 = multiply(sk_c4,sk_c7)
| inverse(sk_c10) = sk_c9 ),
inference(reorient_equations,[],[f12]) ).
fof(f14,negated_conjecture,
( inverse(sk_c4) = sk_c7
| inverse(sk_c10) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_6) ).
fof(f15,plain,
( sk_c7 = inverse(sk_c4)
| inverse(sk_c10) = sk_c9 ),
inference(reorient_equations,[],[f14]) ).
fof(f16,negated_conjecture,
( multiply(sk_c7,sk_c9) = sk_c10
| inverse(sk_c10) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_7) ).
fof(f17,plain,
( sk_c10 = multiply(sk_c7,sk_c9)
| inverse(sk_c10) = sk_c9 ),
inference(reorient_equations,[],[f16]) ).
fof(f23,negated_conjecture,
( multiply(sk_c2,sk_c10) = sk_c9
| multiply(sk_c9,sk_c8) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_11) ).
fof(f24,plain,
( sk_c9 = multiply(sk_c2,sk_c10)
| sk_c10 = multiply(sk_c9,sk_c8) ),
inference(reorient_equations,[],[f23]) ).
fof(f25,negated_conjecture,
( inverse(sk_c2) = sk_c10
| multiply(sk_c9,sk_c8) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_12) ).
fof(f26,plain,
( sk_c10 = inverse(sk_c2)
| sk_c10 = multiply(sk_c9,sk_c8) ),
inference(reorient_equations,[],[f25]) ).
fof(f27,negated_conjecture,
( multiply(sk_c3,sk_c9) = sk_c8
| multiply(sk_c9,sk_c8) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_13) ).
fof(f28,plain,
( multiply(sk_c3,sk_c9) = sk_c8
| sk_c10 = multiply(sk_c9,sk_c8) ),
inference(reorient_equations,[],[f27]) ).
fof(f29,negated_conjecture,
( inverse(sk_c3) = sk_c9
| multiply(sk_c9,sk_c8) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_14) ).
fof(f30,plain,
( sk_c9 = inverse(sk_c3)
| sk_c10 = multiply(sk_c9,sk_c8) ),
inference(reorient_equations,[],[f29]) ).
fof(f31,negated_conjecture,
( multiply(sk_c4,sk_c7) = sk_c10
| multiply(sk_c9,sk_c8) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_15) ).
fof(f32,plain,
( sk_c10 = multiply(sk_c4,sk_c7)
| sk_c10 = multiply(sk_c9,sk_c8) ),
inference(reorient_equations,[],[f31]) ).
fof(f33,negated_conjecture,
( inverse(sk_c4) = sk_c7
| multiply(sk_c9,sk_c8) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_16) ).
fof(f34,plain,
( sk_c7 = inverse(sk_c4)
| sk_c10 = multiply(sk_c9,sk_c8) ),
inference(reorient_equations,[],[f33]) ).
fof(f37,negated_conjecture,
( inverse(sk_c6) = sk_c5
| multiply(sk_c9,sk_c8) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_18) ).
fof(f38,plain,
( inverse(sk_c6) = sk_c5
| sk_c10 = multiply(sk_c9,sk_c8) ),
inference(reorient_equations,[],[f37]) ).
fof(f41,negated_conjecture,
( multiply(sk_c6,sk_c7) = sk_c5
| multiply(sk_c9,sk_c8) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_20) ).
fof(f42,plain,
( sk_c5 = multiply(sk_c6,sk_c7)
| sk_c10 = multiply(sk_c9,sk_c8) ),
inference(reorient_equations,[],[f41]) ).
fof(f43,negated_conjecture,
( multiply(sk_c2,sk_c10) = sk_c9
| multiply(sk_c10,sk_c8) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_21) ).
fof(f44,plain,
( sk_c9 = multiply(sk_c2,sk_c10)
| sk_c9 = multiply(sk_c10,sk_c8) ),
inference(reorient_equations,[],[f43]) ).
fof(f45,negated_conjecture,
( inverse(sk_c2) = sk_c10
| multiply(sk_c10,sk_c8) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_22) ).
fof(f46,plain,
( sk_c10 = inverse(sk_c2)
| sk_c9 = multiply(sk_c10,sk_c8) ),
inference(reorient_equations,[],[f45]) ).
fof(f47,negated_conjecture,
( multiply(sk_c3,sk_c9) = sk_c8
| multiply(sk_c10,sk_c8) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_23) ).
fof(f48,plain,
( multiply(sk_c3,sk_c9) = sk_c8
| sk_c9 = multiply(sk_c10,sk_c8) ),
inference(reorient_equations,[],[f47]) ).
fof(f49,negated_conjecture,
( inverse(sk_c3) = sk_c9
| multiply(sk_c10,sk_c8) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_24) ).
fof(f50,plain,
( sk_c9 = inverse(sk_c3)
| sk_c9 = multiply(sk_c10,sk_c8) ),
inference(reorient_equations,[],[f49]) ).
fof(f51,negated_conjecture,
( multiply(sk_c4,sk_c7) = sk_c10
| multiply(sk_c10,sk_c8) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_25) ).
fof(f52,plain,
( sk_c10 = multiply(sk_c4,sk_c7)
| sk_c9 = multiply(sk_c10,sk_c8) ),
inference(reorient_equations,[],[f51]) ).
fof(f53,negated_conjecture,
( inverse(sk_c4) = sk_c7
| multiply(sk_c10,sk_c8) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_26) ).
fof(f54,plain,
( sk_c7 = inverse(sk_c4)
| sk_c9 = multiply(sk_c10,sk_c8) ),
inference(reorient_equations,[],[f53]) ).
fof(f55,negated_conjecture,
( multiply(sk_c7,sk_c9) = sk_c10
| multiply(sk_c10,sk_c8) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_27) ).
fof(f56,plain,
( sk_c10 = multiply(sk_c7,sk_c9)
| sk_c9 = multiply(sk_c10,sk_c8) ),
inference(reorient_equations,[],[f55]) ).
fof(f63,negated_conjecture,
( multiply(sk_c2,sk_c10) = sk_c9
| inverse(sk_c1) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_31) ).
fof(f64,plain,
( sk_c9 = multiply(sk_c2,sk_c10)
| sk_c10 = inverse(sk_c1) ),
inference(reorient_equations,[],[f63]) ).
fof(f65,negated_conjecture,
( inverse(sk_c2) = sk_c10
| inverse(sk_c1) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_32) ).
fof(f66,plain,
( sk_c10 = inverse(sk_c2)
| sk_c10 = inverse(sk_c1) ),
inference(reorient_equations,[],[f65]) ).
fof(f67,negated_conjecture,
( multiply(sk_c3,sk_c9) = sk_c8
| inverse(sk_c1) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_33) ).
fof(f68,plain,
( multiply(sk_c3,sk_c9) = sk_c8
| sk_c10 = inverse(sk_c1) ),
inference(reorient_equations,[],[f67]) ).
fof(f69,negated_conjecture,
( inverse(sk_c3) = sk_c9
| inverse(sk_c1) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_34) ).
fof(f70,plain,
( sk_c9 = inverse(sk_c3)
| sk_c10 = inverse(sk_c1) ),
inference(reorient_equations,[],[f69]) ).
fof(f71,negated_conjecture,
( multiply(sk_c4,sk_c7) = sk_c10
| inverse(sk_c1) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_35) ).
fof(f72,plain,
( sk_c10 = multiply(sk_c4,sk_c7)
| sk_c10 = inverse(sk_c1) ),
inference(reorient_equations,[],[f71]) ).
fof(f73,negated_conjecture,
( inverse(sk_c4) = sk_c7
| inverse(sk_c1) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_36) ).
fof(f74,plain,
( sk_c7 = inverse(sk_c4)
| sk_c10 = inverse(sk_c1) ),
inference(reorient_equations,[],[f73]) ).
fof(f75,negated_conjecture,
( multiply(sk_c7,sk_c9) = sk_c10
| inverse(sk_c1) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_37) ).
fof(f76,plain,
( sk_c10 = multiply(sk_c7,sk_c9)
| sk_c10 = inverse(sk_c1) ),
inference(reorient_equations,[],[f75]) ).
fof(f83,negated_conjecture,
( multiply(sk_c2,sk_c10) = sk_c9
| multiply(sk_c1,sk_c9) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_41) ).
fof(f84,plain,
( sk_c9 = multiply(sk_c2,sk_c10)
| sk_c10 = multiply(sk_c1,sk_c9) ),
inference(reorient_equations,[],[f83]) ).
fof(f85,negated_conjecture,
( inverse(sk_c2) = sk_c10
| multiply(sk_c1,sk_c9) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_42) ).
fof(f86,plain,
( sk_c10 = inverse(sk_c2)
| sk_c10 = multiply(sk_c1,sk_c9) ),
inference(reorient_equations,[],[f85]) ).
fof(f87,negated_conjecture,
( multiply(sk_c3,sk_c9) = sk_c8
| multiply(sk_c1,sk_c9) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_43) ).
fof(f88,plain,
( multiply(sk_c3,sk_c9) = sk_c8
| sk_c10 = multiply(sk_c1,sk_c9) ),
inference(reorient_equations,[],[f87]) ).
fof(f89,negated_conjecture,
( inverse(sk_c3) = sk_c9
| multiply(sk_c1,sk_c9) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_44) ).
fof(f90,plain,
( sk_c9 = inverse(sk_c3)
| sk_c10 = multiply(sk_c1,sk_c9) ),
inference(reorient_equations,[],[f89]) ).
fof(f91,negated_conjecture,
( multiply(sk_c4,sk_c7) = sk_c10
| multiply(sk_c1,sk_c9) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_45) ).
fof(f92,plain,
( sk_c10 = multiply(sk_c4,sk_c7)
| sk_c10 = multiply(sk_c1,sk_c9) ),
inference(reorient_equations,[],[f91]) ).
fof(f93,negated_conjecture,
( inverse(sk_c4) = sk_c7
| multiply(sk_c1,sk_c9) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_46) ).
fof(f94,plain,
( sk_c7 = inverse(sk_c4)
| sk_c10 = multiply(sk_c1,sk_c9) ),
inference(reorient_equations,[],[f93]) ).
fof(f95,negated_conjecture,
( multiply(sk_c7,sk_c9) = sk_c10
| multiply(sk_c1,sk_c9) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_47) ).
fof(f96,plain,
( sk_c10 = multiply(sk_c7,sk_c9)
| sk_c10 = multiply(sk_c1,sk_c9) ),
inference(reorient_equations,[],[f95]) ).
fof(f97,negated_conjecture,
( inverse(sk_c6) = sk_c5
| multiply(sk_c1,sk_c9) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_48) ).
fof(f98,plain,
( inverse(sk_c6) = sk_c5
| sk_c10 = multiply(sk_c1,sk_c9) ),
inference(reorient_equations,[],[f97]) ).
fof(f101,negated_conjecture,
( multiply(sk_c6,sk_c7) = sk_c5
| multiply(sk_c1,sk_c9) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_50) ).
fof(f102,plain,
( sk_c5 = multiply(sk_c6,sk_c7)
| sk_c10 = multiply(sk_c1,sk_c9) ),
inference(reorient_equations,[],[f101]) ).
fof(f103,negated_conjecture,
! [X2,X3,X0,X1,X6,X4,X5] :
( multiply(X5,X4) != X6
| inverse(X6) != X4
| inverse(X5) != X6
| multiply(X4,sk_c9) != sk_c10
| inverse(X3) != X4
| multiply(X3,X4) != sk_c10
| inverse(X2) != sk_c9
| multiply(X2,sk_c9) != sk_c8
| inverse(X1) != sk_c10
| multiply(X1,sk_c10) != sk_c9
| multiply(X0,sk_c9) != sk_c10
| inverse(X0) != sk_c10
| multiply(sk_c10,sk_c8) != sk_c9
| multiply(sk_c9,sk_c8) != sk_c10
| inverse(sk_c10) != sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_51) ).
fof(f104,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( multiply(X5,X4) != X6
| inverse(X6) != X4
| inverse(X5) != X6
| sk_c10 != multiply(X4,sk_c9)
| inverse(X3) != X4
| sk_c10 != multiply(X3,X4)
| sk_c9 != inverse(X2)
| sk_c8 != multiply(X2,sk_c9)
| sk_c10 != inverse(X1)
| sk_c9 != multiply(X1,sk_c10)
| sk_c10 != multiply(X0,sk_c9)
| inverse(X0) != sk_c10
| sk_c9 != multiply(sk_c10,sk_c8)
| sk_c10 != multiply(sk_c9,sk_c8)
| inverse(sk_c10) != sk_c9 ),
inference(reorient_equations,[],[f103]) ).
fof(f105,plain,
! [X2,X3,X0,X1,X6,X5] :
( multiply(X5,inverse(X3)) != X6
| inverse(X3) != inverse(X6)
| inverse(X5) != X6
| sk_c10 != multiply(inverse(X3),sk_c9)
| sk_c10 != multiply(X3,inverse(X3))
| sk_c9 != inverse(X2)
| sk_c8 != multiply(X2,sk_c9)
| sk_c10 != inverse(X1)
| sk_c9 != multiply(X1,sk_c10)
| sk_c10 != multiply(X0,sk_c9)
| inverse(X0) != sk_c10
| sk_c9 != multiply(sk_c10,sk_c8)
| sk_c10 != multiply(sk_c9,sk_c8)
| inverse(sk_c10) != sk_c9 ),
inference(equality_resolution,[],[f104]) ).
fof(f106,plain,
! [X2,X3,X0,X1,X5] :
( inverse(X5) != multiply(X5,inverse(X3))
| inverse(X3) != inverse(inverse(X5))
| sk_c10 != multiply(inverse(X3),sk_c9)
| sk_c10 != multiply(X3,inverse(X3))
| sk_c9 != inverse(X2)
| sk_c8 != multiply(X2,sk_c9)
| sk_c10 != inverse(X1)
| sk_c9 != multiply(X1,sk_c10)
| sk_c10 != multiply(X0,sk_c9)
| inverse(X0) != sk_c10
| sk_c9 != multiply(sk_c10,sk_c8)
| sk_c10 != multiply(sk_c9,sk_c8)
| inverse(sk_c10) != sk_c9 ),
inference(equality_resolution,[],[f105]) ).
tcf(c_103,plain,
! [X0: $i] : multiply(identity,X0) = X0,
inference(cnf_transformation,[],[f1]) ).
tcf(c_104,plain,
! [X0: $i] : multiply(inverse(X0),X0) = identity,
inference(cnf_transformation,[],[f3]) ).
tcf(c_105,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(multiply(X0,X1),X2) = multiply(X0,multiply(X1,X2)),
inference(cnf_transformation,[],[f4]) ).
tcf(c_106,negated_conjecture,
( ( inverse(sk_c10) = sk_c9 )
| ( multiply(sk_c2,sk_c10) = sk_c9 ) ),
inference(cnf_transformation,[],[f6]) ).
tcf(c_108,negated_conjecture,
( ( inverse(sk_c10) = sk_c9 )
| ( multiply(sk_c3,sk_c9) = sk_c8 ) ),
inference(cnf_transformation,[],[f9]) ).
tcf(c_109,negated_conjecture,
( ( inverse(sk_c3) = sk_c9 )
| ( inverse(sk_c10) = sk_c9 ) ),
inference(cnf_transformation,[],[f11]) ).
tcf(c_110,negated_conjecture,
( ( inverse(sk_c10) = sk_c9 )
| ( multiply(sk_c4,sk_c7) = sk_c10 ) ),
inference(cnf_transformation,[],[f13]) ).
tcf(c_111,negated_conjecture,
( ( inverse(sk_c4) = sk_c7 )
| ( inverse(sk_c10) = sk_c9 ) ),
inference(cnf_transformation,[],[f15]) ).
tcf(c_112,negated_conjecture,
( ( inverse(sk_c10) = sk_c9 )
| ( multiply(sk_c7,sk_c9) = sk_c10 ) ),
inference(cnf_transformation,[],[f17]) ).
tcf(c_116,negated_conjecture,
( ( multiply(sk_c2,sk_c10) = sk_c9 )
| ( multiply(sk_c9,sk_c8) = sk_c10 ) ),
inference(cnf_transformation,[],[f24]) ).
tcf(c_117,negated_conjecture,
( ( inverse(sk_c2) = sk_c10 )
| ( multiply(sk_c9,sk_c8) = sk_c10 ) ),
inference(cnf_transformation,[],[f26]) ).
tcf(c_118,negated_conjecture,
( ( multiply(sk_c3,sk_c9) = sk_c8 )
| ( multiply(sk_c9,sk_c8) = sk_c10 ) ),
inference(cnf_transformation,[],[f28]) ).
tcf(c_119,negated_conjecture,
( ( inverse(sk_c3) = sk_c9 )
| ( multiply(sk_c9,sk_c8) = sk_c10 ) ),
inference(cnf_transformation,[],[f30]) ).
tcf(c_120,negated_conjecture,
( ( multiply(sk_c4,sk_c7) = sk_c10 )
| ( multiply(sk_c9,sk_c8) = sk_c10 ) ),
inference(cnf_transformation,[],[f32]) ).
tcf(c_121,negated_conjecture,
( ( inverse(sk_c4) = sk_c7 )
| ( multiply(sk_c9,sk_c8) = sk_c10 ) ),
inference(cnf_transformation,[],[f34]) ).
tcf(c_123,negated_conjecture,
( ( inverse(sk_c6) = sk_c5 )
| ( multiply(sk_c9,sk_c8) = sk_c10 ) ),
inference(cnf_transformation,[],[f38]) ).
tcf(c_125,negated_conjecture,
( ( multiply(sk_c6,sk_c7) = sk_c5 )
| ( multiply(sk_c9,sk_c8) = sk_c10 ) ),
inference(cnf_transformation,[],[f42]) ).
tcf(c_126,negated_conjecture,
( ( multiply(sk_c2,sk_c10) = sk_c9 )
| ( multiply(sk_c10,sk_c8) = sk_c9 ) ),
inference(cnf_transformation,[],[f44]) ).
tcf(c_127,negated_conjecture,
( ( inverse(sk_c2) = sk_c10 )
| ( multiply(sk_c10,sk_c8) = sk_c9 ) ),
inference(cnf_transformation,[],[f46]) ).
tcf(c_128,negated_conjecture,
( ( multiply(sk_c3,sk_c9) = sk_c8 )
| ( multiply(sk_c10,sk_c8) = sk_c9 ) ),
inference(cnf_transformation,[],[f48]) ).
tcf(c_129,negated_conjecture,
( ( inverse(sk_c3) = sk_c9 )
| ( multiply(sk_c10,sk_c8) = sk_c9 ) ),
inference(cnf_transformation,[],[f50]) ).
tcf(c_130,negated_conjecture,
( ( multiply(sk_c4,sk_c7) = sk_c10 )
| ( multiply(sk_c10,sk_c8) = sk_c9 ) ),
inference(cnf_transformation,[],[f52]) ).
tcf(c_131,negated_conjecture,
( ( inverse(sk_c4) = sk_c7 )
| ( multiply(sk_c10,sk_c8) = sk_c9 ) ),
inference(cnf_transformation,[],[f54]) ).
tcf(c_132,negated_conjecture,
( ( multiply(sk_c7,sk_c9) = sk_c10 )
| ( multiply(sk_c10,sk_c8) = sk_c9 ) ),
inference(cnf_transformation,[],[f56]) ).
tcf(c_136,negated_conjecture,
( ( inverse(sk_c1) = sk_c10 )
| ( multiply(sk_c2,sk_c10) = sk_c9 ) ),
inference(cnf_transformation,[],[f64]) ).
tcf(c_137,negated_conjecture,
( ( inverse(sk_c1) = sk_c10 )
| ( inverse(sk_c2) = sk_c10 ) ),
inference(cnf_transformation,[],[f66]) ).
tcf(c_138,negated_conjecture,
( ( inverse(sk_c1) = sk_c10 )
| ( multiply(sk_c3,sk_c9) = sk_c8 ) ),
inference(cnf_transformation,[],[f68]) ).
tcf(c_139,negated_conjecture,
( ( inverse(sk_c1) = sk_c10 )
| ( inverse(sk_c3) = sk_c9 ) ),
inference(cnf_transformation,[],[f70]) ).
tcf(c_140,negated_conjecture,
( ( inverse(sk_c1) = sk_c10 )
| ( multiply(sk_c4,sk_c7) = sk_c10 ) ),
inference(cnf_transformation,[],[f72]) ).
tcf(c_141,negated_conjecture,
( ( inverse(sk_c1) = sk_c10 )
| ( inverse(sk_c4) = sk_c7 ) ),
inference(cnf_transformation,[],[f74]) ).
tcf(c_142,negated_conjecture,
( ( inverse(sk_c1) = sk_c10 )
| ( multiply(sk_c7,sk_c9) = sk_c10 ) ),
inference(cnf_transformation,[],[f76]) ).
tcf(c_146,negated_conjecture,
( ( multiply(sk_c1,sk_c9) = sk_c10 )
| ( multiply(sk_c2,sk_c10) = sk_c9 ) ),
inference(cnf_transformation,[],[f84]) ).
tcf(c_147,negated_conjecture,
( ( inverse(sk_c2) = sk_c10 )
| ( multiply(sk_c1,sk_c9) = sk_c10 ) ),
inference(cnf_transformation,[],[f86]) ).
tcf(c_148,negated_conjecture,
( ( multiply(sk_c1,sk_c9) = sk_c10 )
| ( multiply(sk_c3,sk_c9) = sk_c8 ) ),
inference(cnf_transformation,[],[f88]) ).
tcf(c_149,negated_conjecture,
( ( inverse(sk_c3) = sk_c9 )
| ( multiply(sk_c1,sk_c9) = sk_c10 ) ),
inference(cnf_transformation,[],[f90]) ).
tcf(c_150,negated_conjecture,
( ( multiply(sk_c1,sk_c9) = sk_c10 )
| ( multiply(sk_c4,sk_c7) = sk_c10 ) ),
inference(cnf_transformation,[],[f92]) ).
tcf(c_151,negated_conjecture,
( ( inverse(sk_c4) = sk_c7 )
| ( multiply(sk_c1,sk_c9) = sk_c10 ) ),
inference(cnf_transformation,[],[f94]) ).
tcf(c_152,negated_conjecture,
( ( multiply(sk_c1,sk_c9) = sk_c10 )
| ( multiply(sk_c7,sk_c9) = sk_c10 ) ),
inference(cnf_transformation,[],[f96]) ).
tcf(c_153,negated_conjecture,
( ( inverse(sk_c6) = sk_c5 )
| ( multiply(sk_c1,sk_c9) = sk_c10 ) ),
inference(cnf_transformation,[],[f98]) ).
tcf(c_155,negated_conjecture,
( ( multiply(sk_c1,sk_c9) = sk_c10 )
| ( multiply(sk_c6,sk_c7) = sk_c5 ) ),
inference(cnf_transformation,[],[f102]) ).
tcf(c_156,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( ( inverse(sk_c10) != sk_c9 )
| ( inverse(X4) != sk_c9 )
| ( inverse(X3) != sk_c10 )
| ( inverse(X2) != sk_c10 )
| ( multiply(sk_c9,sk_c8) != sk_c10 )
| ( multiply(sk_c10,sk_c8) != sk_c9 )
| ( multiply(X4,sk_c9) != sk_c8 )
| ( multiply(X3,sk_c10) != sk_c9 )
| ( multiply(X2,sk_c9) != sk_c10 )
| ( inverse(inverse(X0)) != inverse(X1) )
| ( multiply(inverse(X1),sk_c9) != sk_c10 )
| ( multiply(X1,inverse(X1)) != sk_c10 )
| ( multiply(X0,inverse(X1)) != inverse(X0) ) ),
inference(cnf_transformation,[],[f106]) ).
tcf(c_157,plain,
multiply(identity,sk_c10) = sk_c10,
inference(instantiation,[status(thm)],[c_103]) ).
tcf(c_621,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_10
| ( inverse(X0) != sk_c10 )
| ( multiply(X0,sk_c10) != sk_c9 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_10])],[c_156]) ).
tcf(c_622,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_11
| ( inverse(X0) != sk_c9 )
| ( multiply(X0,sk_c9) != sk_c8 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_11])],[c_156]) ).
tcf(c_623,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_12
| ( inverse(X0) != sk_c10 )
| ( multiply(X0,sk_c9) != sk_c10 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_12])],[c_156]) ).
tcf(c_624,negated_conjecture,
! [X0: $i,X1: $i] :
( ~ iPr_def_13
| ( inverse(inverse(X0)) != inverse(X1) )
| ( multiply(inverse(X1),sk_c9) != sk_c10 )
| ( multiply(X1,inverse(X1)) != sk_c10 )
| ( multiply(X0,inverse(X1)) != inverse(X0) ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_13])],[c_156]) ).
tcf(c_625,negated_conjecture,
( iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( inverse(sk_c10) != sk_c9 )
| ( multiply(sk_c9,sk_c8) != sk_c10 )
| ( multiply(sk_c10,sk_c8) != sk_c9 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_156]) ).
tcf(c_626,definition,
iPr_def_14 = multiply(sk_c10,sk_c8),
introduced(definition,[new_symbols(definition,[iPr_def_14])],[]) ).
tcf(c_627,definition,
iPr_def_15 = multiply(sk_c9,sk_c8),
introduced(definition,[new_symbols(definition,[iPr_def_15])],[]) ).
tcf(c_628,definition,
iPr_def_16 = inverse(sk_c10),
introduced(definition,[new_symbols(definition,[iPr_def_16])],[]) ).
tcf(c_629,definition,
iPr_def_17 = multiply(sk_c6,sk_c7),
introduced(definition,[new_symbols(definition,[iPr_def_17])],[]) ).
tcf(c_630,definition,
iPr_def_18 = multiply(sk_c1,sk_c9),
introduced(definition,[new_symbols(definition,[iPr_def_18])],[]) ).
tcf(c_632,definition,
iPr_def_20 = inverse(sk_c6),
introduced(definition,[new_symbols(definition,[iPr_def_20])],[]) ).
tcf(c_633,definition,
iPr_def_21 = multiply(sk_c7,sk_c9),
introduced(definition,[new_symbols(definition,[iPr_def_21])],[]) ).
tcf(c_634,definition,
iPr_def_22 = inverse(sk_c4),
introduced(definition,[new_symbols(definition,[iPr_def_22])],[]) ).
tcf(c_635,definition,
iPr_def_23 = multiply(sk_c4,sk_c7),
introduced(definition,[new_symbols(definition,[iPr_def_23])],[]) ).
tcf(c_636,definition,
iPr_def_24 = inverse(sk_c3),
introduced(definition,[new_symbols(definition,[iPr_def_24])],[]) ).
tcf(c_637,definition,
iPr_def_25 = multiply(sk_c3,sk_c9),
introduced(definition,[new_symbols(definition,[iPr_def_25])],[]) ).
tcf(c_638,definition,
iPr_def_26 = inverse(sk_c2),
introduced(definition,[new_symbols(definition,[iPr_def_26])],[]) ).
tcf(c_639,definition,
iPr_def_27 = multiply(sk_c2,sk_c10),
introduced(definition,[new_symbols(definition,[iPr_def_27])],[]) ).
tcf(c_640,definition,
iPr_def_28 = inverse(sk_c1),
introduced(definition,[new_symbols(definition,[iPr_def_28])],[]) ).
tcf(c_641,negated_conjecture,
( iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( iPr_def_16 != sk_c9 )
| ( iPr_def_15 != sk_c10 )
| ( iPr_def_14 != sk_c9 ) ),
inference(demodulation,[status(thm)],[c_625,c_628,c_627,c_626]) ).
tcf(c_642,negated_conjecture,
! [X0: $i,X1: $i] :
( ~ iPr_def_13
| ( inverse(inverse(X0)) != inverse(X1) )
| ( multiply(inverse(X1),sk_c9) != sk_c10 )
| ( multiply(X1,inverse(X1)) != sk_c10 )
| ( multiply(X0,inverse(X1)) != inverse(X0) ) ),
inference(demodulation,[status(thm)],[c_624]) ).
tcf(c_643,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_12
| ( inverse(X0) != sk_c10 )
| ( multiply(X0,sk_c9) != sk_c10 ) ),
inference(demodulation,[status(thm)],[c_623]) ).
tcf(c_644,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_11
| ( inverse(X0) != sk_c9 )
| ( multiply(X0,sk_c9) != sk_c8 ) ),
inference(demodulation,[status(thm)],[c_622]) ).
tcf(c_645,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_10
| ( inverse(X0) != sk_c10 )
| ( multiply(X0,sk_c10) != sk_c9 ) ),
inference(demodulation,[status(thm)],[c_621]) ).
tcf(c_646,negated_conjecture,
( ( iPr_def_18 = sk_c10 )
| ( iPr_def_17 = sk_c5 ) ),
inference(demodulation,[status(thm)],[c_155,c_630,c_629]) ).
tcf(c_648,negated_conjecture,
( ( iPr_def_20 = sk_c5 )
| ( iPr_def_18 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_153,c_632]) ).
tcf(c_649,negated_conjecture,
( ( iPr_def_21 = sk_c10 )
| ( iPr_def_18 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_152,c_633]) ).
tcf(c_650,negated_conjecture,
( ( iPr_def_22 = sk_c7 )
| ( iPr_def_18 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_151,c_634]) ).
tcf(c_651,negated_conjecture,
( ( iPr_def_23 = sk_c10 )
| ( iPr_def_18 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_150,c_635]) ).
tcf(c_652,negated_conjecture,
( ( iPr_def_24 = sk_c9 )
| ( iPr_def_18 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_149,c_636]) ).
tcf(c_653,negated_conjecture,
( ( iPr_def_25 = sk_c8 )
| ( iPr_def_18 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_148,c_637]) ).
tcf(c_654,negated_conjecture,
( ( iPr_def_26 = sk_c10 )
| ( iPr_def_18 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_147,c_638]) ).
tcf(c_655,negated_conjecture,
( ( iPr_def_27 = sk_c9 )
| ( iPr_def_18 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_146,c_639]) ).
tcf(c_659,negated_conjecture,
( ( iPr_def_28 = sk_c10 )
| ( iPr_def_21 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_142]) ).
tcf(c_660,negated_conjecture,
( ( iPr_def_28 = sk_c10 )
| ( iPr_def_22 = sk_c7 ) ),
inference(demodulation,[status(thm)],[c_141]) ).
tcf(c_661,negated_conjecture,
( ( iPr_def_28 = sk_c10 )
| ( iPr_def_23 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_140]) ).
tcf(c_662,negated_conjecture,
( ( iPr_def_28 = sk_c10 )
| ( iPr_def_24 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_139]) ).
tcf(c_663,negated_conjecture,
( ( iPr_def_28 = sk_c10 )
| ( iPr_def_25 = sk_c8 ) ),
inference(demodulation,[status(thm)],[c_138]) ).
tcf(c_664,negated_conjecture,
( ( iPr_def_28 = sk_c10 )
| ( iPr_def_26 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_137]) ).
tcf(c_665,negated_conjecture,
( ( iPr_def_28 = sk_c10 )
| ( iPr_def_27 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_136]) ).
tcf(c_669,negated_conjecture,
( ( iPr_def_21 = sk_c10 )
| ( iPr_def_14 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_132]) ).
tcf(c_670,negated_conjecture,
( ( iPr_def_22 = sk_c7 )
| ( iPr_def_14 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_131]) ).
tcf(c_671,negated_conjecture,
( ( iPr_def_23 = sk_c10 )
| ( iPr_def_14 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_130]) ).
tcf(c_672,negated_conjecture,
( ( iPr_def_24 = sk_c9 )
| ( iPr_def_14 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_129]) ).
tcf(c_673,negated_conjecture,
( ( iPr_def_25 = sk_c8 )
| ( iPr_def_14 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_128]) ).
tcf(c_674,negated_conjecture,
( ( iPr_def_26 = sk_c10 )
| ( iPr_def_14 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_127]) ).
tcf(c_675,negated_conjecture,
( ( iPr_def_27 = sk_c9 )
| ( iPr_def_14 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_126]) ).
tcf(c_676,negated_conjecture,
( ( iPr_def_17 = sk_c5 )
| ( iPr_def_15 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_125]) ).
tcf(c_678,negated_conjecture,
( ( iPr_def_20 = sk_c5 )
| ( iPr_def_15 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_123]) ).
tcf(c_680,negated_conjecture,
( ( iPr_def_22 = sk_c7 )
| ( iPr_def_15 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_121]) ).
tcf(c_681,negated_conjecture,
( ( iPr_def_23 = sk_c10 )
| ( iPr_def_15 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_120]) ).
tcf(c_682,negated_conjecture,
( ( iPr_def_24 = sk_c9 )
| ( iPr_def_15 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_119]) ).
tcf(c_683,negated_conjecture,
( ( iPr_def_25 = sk_c8 )
| ( iPr_def_15 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_118]) ).
tcf(c_684,negated_conjecture,
( ( iPr_def_26 = sk_c10 )
| ( iPr_def_15 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_117]) ).
tcf(c_685,negated_conjecture,
( ( iPr_def_27 = sk_c9 )
| ( iPr_def_15 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_116]) ).
tcf(c_689,negated_conjecture,
( ( iPr_def_21 = sk_c10 )
| ( iPr_def_16 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_112]) ).
tcf(c_690,negated_conjecture,
( ( iPr_def_22 = sk_c7 )
| ( iPr_def_16 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_111]) ).
tcf(c_691,negated_conjecture,
( ( iPr_def_23 = sk_c10 )
| ( iPr_def_16 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_110]) ).
tcf(c_692,negated_conjecture,
( ( iPr_def_24 = sk_c9 )
| ( iPr_def_16 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_109]) ).
tcf(c_693,negated_conjecture,
( ( iPr_def_25 = sk_c8 )
| ( iPr_def_16 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_108]) ).
tcf(c_695,negated_conjecture,
( ( iPr_def_27 = sk_c9 )
| ( iPr_def_16 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_106]) ).
tcf(c_696,plain,
! [X0: $i] : X0 = X0,
theory(equality) ).
tcf(c_697,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = X0 )
| ( X2 != X1 )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_698,plain,
! [X0: $i,X1: $i] :
( ( inverse(X0) = inverse(X1) )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_699,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( multiply(X0,X2) = multiply(X1,X3) )
| ( X2 != X3 )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_700,plain,
( ( inverse(sk_c10) = inverse(sk_c10) )
| ( sk_c10 != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_698]) ).
tcf(c_702,plain,
sk_c10 = sk_c10,
inference(instantiation,[status(thm)],[c_696]) ).
tcf(c_706,plain,
( ~ iPr_def_13
| ( inverse(inverse(sk_c10)) != inverse(sk_c10) )
| ( multiply(sk_c10,inverse(sk_c10)) != sk_c10 )
| ( multiply(sk_c10,inverse(sk_c10)) != inverse(sk_c10) )
| ( multiply(inverse(sk_c10),sk_c9) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_642]) ).
tcf(c_1074,plain,
( ( iPr_def_23 = iPr_def_26 )
| ( sk_c10 = iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_654,c_651]) ).
tcf(c_1088,plain,
( ( iPr_def_24 = iPr_def_27 )
| ( sk_c10 = iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_652,c_655]) ).
tcf(c_1134,plain,
( ( sk_c10 = iPr_def_21 )
| ( inverse(iPr_def_28) = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_659,c_628]) ).
tcf(c_1169,plain,
( ( sk_c10 = iPr_def_23 )
| ( inverse(iPr_def_28) = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_661,c_628]) ).
tcf(c_1187,plain,
( ( sk_c10 = iPr_def_18 )
| ( multiply(iPr_def_24,sk_c8) = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_652,c_627]) ).
tcf(c_1208,plain,
( ( sk_c10 = iPr_def_18 )
| ( multiply(sk_c1,iPr_def_24) = iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_652,c_630]) ).
tcf(c_1231,plain,
( ( sk_c10 = iPr_def_28 )
| ( multiply(sk_c4,iPr_def_22) = iPr_def_23 ) ),
inference(superposition,[status(thm)],[c_660,c_635]) ).
tcf(c_1233,plain,
( ( sk_c10 = iPr_def_18 )
| ( multiply(sk_c4,iPr_def_22) = iPr_def_23 ) ),
inference(superposition,[status(thm)],[c_650,c_635]) ).
tcf(c_1249,plain,
( ( sk_c10 = iPr_def_23 )
| ( multiply(sk_c2,iPr_def_28) = iPr_def_27 ) ),
inference(superposition,[status(thm)],[c_661,c_639]) ).
tcf(c_1251,plain,
( ( sk_c10 = iPr_def_18 )
| ( multiply(sk_c2,iPr_def_26) = iPr_def_27 ) ),
inference(superposition,[status(thm)],[c_654,c_639]) ).
tcf(c_1252,plain,
( ( sk_c10 = iPr_def_18 )
| ( multiply(sk_c2,iPr_def_23) = iPr_def_27 ) ),
inference(superposition,[status(thm)],[c_651,c_639]) ).
tcf(c_1253,plain,
( ( sk_c10 = iPr_def_18 )
| ( multiply(sk_c2,iPr_def_21) = iPr_def_27 ) ),
inference(superposition,[status(thm)],[c_649,c_639]) ).
tcf(c_1264,plain,
multiply(iPr_def_16,sk_c10) = identity,
inference(superposition,[status(thm)],[c_628,c_104]) ).
tcf(c_1265,plain,
multiply(iPr_def_26,sk_c2) = identity,
inference(superposition,[status(thm)],[c_638,c_104]) ).
tcf(c_1266,plain,
multiply(iPr_def_24,sk_c3) = identity,
inference(superposition,[status(thm)],[c_636,c_104]) ).
tcf(c_1267,plain,
multiply(iPr_def_22,sk_c4) = identity,
inference(superposition,[status(thm)],[c_634,c_104]) ).
tcf(c_1270,plain,
multiply(iPr_def_28,sk_c1) = identity,
inference(superposition,[status(thm)],[c_640,c_104]) ).
tcf(c_1271,plain,
! [X0: $i] :
( ( iPr_def_14 = sk_c9 )
| ( iPr_def_14 != X0 )
| ( sk_c9 != X0 ) ),
inference(instantiation,[status(thm)],[c_697]) ).
tcf(c_1274,plain,
! [X0: $i,X1: $i] :
( ( sk_c9 = X0 )
| ( sk_c9 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_697]) ).
tcf(c_1290,plain,
! [X0: $i] :
( ( sk_c9 = X0 )
| ( sk_c9 != sk_c9 )
| ( X0 != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_1274]) ).
tcf(c_1291,plain,
sk_c9 = sk_c9,
inference(instantiation,[status(thm)],[c_696]) ).
tcf(c_1292,plain,
( ( sk_c9 = sk_c10 )
| ( sk_c9 != sk_c9 )
| ( sk_c10 != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_1290]) ).
tcf(c_1296,plain,
( ( sk_c9 = multiply(identity,sk_c9) )
| ( sk_c9 != sk_c9 )
| ( multiply(identity,sk_c9) != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_1290]) ).
tcf(c_1297,plain,
multiply(identity,sk_c9) = sk_c9,
inference(instantiation,[status(thm)],[c_103]) ).
tcf(c_1299,plain,
! [X0: $i,X1: $i] :
( ( X0 = sk_c9 )
| ( sk_c9 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_697]) ).
tcf(c_1302,plain,
( ( sk_c9 = iPr_def_27 )
| ( iPr_def_27 != sk_c9 )
| ( sk_c9 != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_1290]) ).
tcf(c_1312,plain,
( ( sk_c10 = iPr_def_28 )
| ( multiply(iPr_def_24,sk_c8) = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_662,c_627]) ).
tcf(c_1330,plain,
( ( sk_c10 = iPr_def_28 )
| ( multiply(sk_c10,iPr_def_25) = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_663,c_626]) ).
tcf(c_1336,plain,
! [X0: $i] :
( ( sk_c9 = X0 )
| ( sk_c9 != iPr_def_24 )
| ( X0 != iPr_def_24 ) ),
inference(instantiation,[status(thm)],[c_1274]) ).
tcf(c_1346,plain,
( ( sk_c10 = iPr_def_26 )
| ( multiply(sk_c2,iPr_def_28) = iPr_def_27 ) ),
inference(superposition,[status(thm)],[c_664,c_639]) ).
tcf(c_1370,plain,
! [X0: $i] :
( ( sk_c9 = X0 )
| ( sk_c9 != iPr_def_27 )
| ( X0 != iPr_def_27 ) ),
inference(instantiation,[status(thm)],[c_1274]) ).
tcf(c_1373,plain,
! [X0: $i] :
( ( sk_c9 = X0 )
| ( sk_c9 != multiply(identity,sk_c9) )
| ( X0 != multiply(identity,sk_c9) ) ),
inference(instantiation,[status(thm)],[c_1274]) ).
tcf(c_1382,plain,
( ( sk_c10 = iPr_def_28 )
| ( multiply(sk_c3,iPr_def_27) = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_665,c_637]) ).
tcf(c_1401,plain,
! [X0: $i] :
( ( X0 = sk_c9 )
| ( sk_c9 != multiply(identity,sk_c9) )
| ( X0 != multiply(identity,sk_c9) ) ),
inference(instantiation,[status(thm)],[c_1299]) ).
tcf(c_1403,plain,
! [X0: $i] :
( ( X0 = sk_c9 )
| ( sk_c9 != iPr_def_24 )
| ( X0 != iPr_def_24 ) ),
inference(instantiation,[status(thm)],[c_1299]) ).
tcf(c_1405,plain,
! [X0: $i] :
( ( X0 = sk_c9 )
| ( sk_c9 != iPr_def_27 )
| ( X0 != iPr_def_27 ) ),
inference(instantiation,[status(thm)],[c_1299]) ).
tcf(c_1424,plain,
( ( sk_c9 = iPr_def_14 )
| ( iPr_def_14 != sk_c9 )
| ( sk_c9 != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_1290]) ).
tcf(c_1425,plain,
! [X0: $i,X1: $i] :
( ( inverse(X0) = sk_c10 )
| ( sk_c10 != X1 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_697]) ).
tcf(c_1454,plain,
( ( sk_c9 = iPr_def_16 )
| ( iPr_def_16 != sk_c9 )
| ( sk_c9 != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_1290]) ).
tcf(c_1466,plain,
! [X0: $i,X1: $i] :
( ( sk_c9 = multiply(X0,X1) )
| ( sk_c9 != multiply(identity,sk_c9) )
| ( multiply(X0,X1) != multiply(identity,sk_c9) ) ),
inference(instantiation,[status(thm)],[c_1373]) ).
tcf(c_1529,plain,
( ( iPr_def_14 = sk_c9 )
| ( iPr_def_14 != iPr_def_16 )
| ( sk_c9 != iPr_def_16 ) ),
inference(instantiation,[status(thm)],[c_1271]) ).
tcf(c_1530,plain,
! [X0: $i] :
( ( X0 = sk_c9 )
| ( sk_c9 != iPr_def_16 )
| ( X0 != iPr_def_16 ) ),
inference(instantiation,[status(thm)],[c_1299]) ).
tcf(c_1538,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( inverse(X0) = X2 )
| ( X2 != X1 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_697]) ).
tcf(c_1548,plain,
( ( sk_c9 = iPr_def_14 )
| ( multiply(sk_c4,iPr_def_22) = iPr_def_23 ) ),
inference(superposition,[status(thm)],[c_670,c_635]) ).
tcf(c_1571,plain,
( ( sk_c10 = iPr_def_23 )
| ( multiply(sk_c3,iPr_def_14) = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_671,c_637]) ).
tcf(c_1608,plain,
! [X0: $i] :
( ( iPr_def_14 = iPr_def_27 )
| ( iPr_def_27 != X0 )
| ( iPr_def_14 != X0 ) ),
inference(instantiation,[status(thm)],[c_697]) ).
tcf(c_1609,plain,
( ( iPr_def_14 = iPr_def_27 )
| ( iPr_def_27 != sk_c10 )
| ( iPr_def_14 != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_1608]) ).
tcf(c_1614,plain,
! [X0: $i,X1: $i] :
( ( X0 = iPr_def_24 )
| ( iPr_def_24 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_697]) ).
tcf(c_1628,plain,
( ( sk_c9 = iPr_def_14 )
| ( multiply(sk_c3,iPr_def_24) = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_672,c_637]) ).
tcf(c_1631,plain,
( ( sk_c9 = iPr_def_14 )
| ( multiply(iPr_def_24,sk_c8) = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_672,c_627]) ).
tcf(c_1653,plain,
( ( sk_c9 = multiply(identity,iPr_def_27) )
| ( sk_c9 != iPr_def_27 )
| ( multiply(identity,iPr_def_27) != iPr_def_27 ) ),
inference(instantiation,[status(thm)],[c_1370]) ).
tcf(c_1654,plain,
multiply(identity,iPr_def_27) = iPr_def_27,
inference(instantiation,[status(thm)],[c_103]) ).
tcf(c_1656,plain,
! [X0: $i,X1: $i] :
( ( X0 = iPr_def_27 )
| ( iPr_def_27 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_697]) ).
tcf(c_1661,plain,
( ( iPr_def_24 = sk_c9 )
| ( iPr_def_24 != iPr_def_24 )
| ( sk_c9 != iPr_def_24 ) ),
inference(instantiation,[status(thm)],[c_1403]) ).
tcf(c_1662,plain,
iPr_def_24 = iPr_def_24,
inference(instantiation,[status(thm)],[c_696]) ).
tcf(c_1693,plain,
( ( sk_c10 = iPr_def_26 )
| ( multiply(sk_c3,iPr_def_14) = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_674,c_637]) ).
tcf(c_1750,plain,
( ( iPr_def_24 = iPr_def_27 )
| ( sk_c9 = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_675,c_672]) ).
tcf(c_1754,plain,
( ( sk_c9 = iPr_def_14 )
| ( multiply(sk_c3,iPr_def_27) = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_675,c_637]) ).
tcf(c_1784,plain,
multiply(identity,identity) = identity,
inference(instantiation,[status(thm)],[c_103]) ).
tcf(c_1789,plain,
identity = identity,
inference(instantiation,[status(thm)],[c_696]) ).
tcf(c_1791,plain,
! [X0: $i,X1: $i] :
( ( X0 = identity )
| ( identity != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_697]) ).
tcf(c_1851,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( inverse(X0) = X2 )
| ( X2 != inverse(X1) )
| ( inverse(X0) != inverse(X1) ) ),
inference(instantiation,[status(thm)],[c_1538]) ).
tcf(c_1890,plain,
( ( iPr_def_16 = sk_c9 )
| ( iPr_def_16 != iPr_def_16 )
| ( sk_c9 != iPr_def_16 ) ),
inference(instantiation,[status(thm)],[c_1530]) ).
tcf(c_1891,plain,
iPr_def_16 = iPr_def_16,
inference(instantiation,[status(thm)],[c_696]) ).
tcf(c_1892,plain,
! [X0: $i,X1: $i] :
( ( X0 = iPr_def_16 )
| ( iPr_def_16 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_697]) ).
tcf(c_1904,plain,
( ( sk_c10 = iPr_def_15 )
| ( multiply(sk_c4,iPr_def_22) = iPr_def_23 ) ),
inference(superposition,[status(thm)],[c_680,c_635]) ).
tcf(c_1921,plain,
! [X0: $i,X1: $i] :
( ( sk_c10 = inverse(X0) )
| ( sk_c10 != X1 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_697]) ).
tcf(c_1924,plain,
( ( iPr_def_14 = sk_c9 )
| ( iPr_def_14 != iPr_def_14 )
| ( sk_c9 != iPr_def_14 ) ),
inference(instantiation,[status(thm)],[c_1271]) ).
tcf(c_1925,plain,
! [X0: $i] :
( ( X0 = sk_c9 )
| ( sk_c9 != iPr_def_14 )
| ( X0 != iPr_def_14 ) ),
inference(instantiation,[status(thm)],[c_1299]) ).
tcf(c_1926,plain,
! [X0: $i] :
( ( sk_c9 = X0 )
| ( sk_c9 != iPr_def_14 )
| ( X0 != iPr_def_14 ) ),
inference(instantiation,[status(thm)],[c_1274]) ).
tcf(c_1927,plain,
( ( sk_c9 = sk_c10 )
| ( sk_c9 != iPr_def_14 )
| ( sk_c10 != iPr_def_14 ) ),
inference(instantiation,[status(thm)],[c_1926]) ).
tcf(c_1928,plain,
( ( sk_c10 = sk_c9 )
| ( sk_c9 != iPr_def_14 )
| ( sk_c10 != iPr_def_14 ) ),
inference(instantiation,[status(thm)],[c_1925]) ).
tcf(c_1942,plain,
( ( sk_c10 = iPr_def_15 )
| ( multiply(sk_c2,iPr_def_23) = iPr_def_27 ) ),
inference(superposition,[status(thm)],[c_681,c_639]) ).
tcf(c_1993,plain,
iPr_def_14 = iPr_def_14,
inference(instantiation,[status(thm)],[c_696]) ).
tcf(c_1994,plain,
! [X0: $i,X1: $i] :
( ( iPr_def_14 = X0 )
| ( iPr_def_14 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_697]) ).
tcf(c_2012,plain,
( ( sk_c10 = iPr_def_15 )
| ( multiply(sk_c3,iPr_def_24) = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_682,c_637]) ).
tcf(c_2015,plain,
( ( sk_c10 = iPr_def_15 )
| ( multiply(iPr_def_24,sk_c8) = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_682,c_627]) ).
tcf(c_2072,plain,
( ( iPr_def_23 = iPr_def_26 )
| ( sk_c10 = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_684,c_681]) ).
tcf(c_2076,plain,
( ( sk_c10 = iPr_def_15 )
| ( multiply(sk_c2,iPr_def_26) = iPr_def_27 ) ),
inference(superposition,[status(thm)],[c_684,c_639]) ).
tcf(c_2079,plain,
( ( sk_c10 = iPr_def_15 )
| ( inverse(iPr_def_26) = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_684,c_628]) ).
tcf(c_2115,plain,
( ( iPr_def_24 = iPr_def_27 )
| ( sk_c10 = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_685,c_682]) ).
tcf(c_2121,plain,
( ( sk_c10 = iPr_def_15 )
| ( multiply(sk_c3,iPr_def_27) = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_685,c_637]) ).
tcf(c_2146,plain,
! [X0: $i,X1: $i] :
( ( iPr_def_24 = X0 )
| ( iPr_def_24 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_697]) ).
tcf(c_2151,plain,
! [X0: $i,X1: $i] :
( ( iPr_def_27 = X0 )
| ( iPr_def_27 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_697]) ).
tcf(c_2152,plain,
! [X0: $i] :
( ( X0 = iPr_def_27 )
| ( iPr_def_27 != multiply(sk_c2,sk_c10) )
| ( X0 != multiply(sk_c2,sk_c10) ) ),
inference(instantiation,[status(thm)],[c_1656]) ).
tcf(c_2338,plain,
( ( iPr_def_14 = iPr_def_16 )
| ( sk_c10 = iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_689,c_669]) ).
tcf(c_2433,plain,
! [X0: $i,X1: $i] :
( ( identity = X0 )
| ( identity != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_697]) ).
tcf(c_2482,plain,
( ( sk_c9 = iPr_def_16 )
| ( multiply(sk_c4,iPr_def_22) = iPr_def_23 ) ),
inference(superposition,[status(thm)],[c_690,c_635]) ).
tcf(c_2515,plain,
( ( iPr_def_14 = iPr_def_16 )
| ( sk_c10 = iPr_def_23 ) ),
inference(superposition,[status(thm)],[c_691,c_671]) ).
tcf(c_2521,plain,
( ( sk_c10 = iPr_def_23 )
| ( multiply(sk_c1,iPr_def_16) = iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_691,c_630]) ).
tcf(c_2571,plain,
! [X0: $i] :
( ( X0 = iPr_def_24 )
| ( iPr_def_24 != sk_c9 )
| ( X0 != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_1614]) ).
tcf(c_2572,plain,
( ( sk_c10 = iPr_def_24 )
| ( iPr_def_24 != sk_c9 )
| ( sk_c10 != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_2571]) ).
tcf(c_2617,plain,
( ( sk_c9 = iPr_def_16 )
| ( multiply(iPr_def_24,sk_c8) = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_692,c_627]) ).
tcf(c_2694,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = inverse(X0) )
| ( X2 != X1 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_697]) ).
tcf(c_2696,plain,
! [X0: $i] :
( ( inverse(X0) = iPr_def_16 )
| ( iPr_def_16 != inverse(sk_c10) )
| ( inverse(X0) != inverse(sk_c10) ) ),
inference(instantiation,[status(thm)],[c_1851]) ).
tcf(c_2697,plain,
( ( inverse(sk_c10) = iPr_def_16 )
| ( iPr_def_16 != inverse(sk_c10) )
| ( inverse(sk_c10) != inverse(sk_c10) ) ),
inference(instantiation,[status(thm)],[c_2696]) ).
tcf(c_2907,plain,
! [X0: $i] :
( ( sk_c9 = X0 )
| ( sk_c9 != multiply(identity,iPr_def_27) )
| ( X0 != multiply(identity,iPr_def_27) ) ),
inference(instantiation,[status(thm)],[c_1274]) ).
tcf(c_2944,plain,
( ~ iPr_def_12
| ( sk_c10 != iPr_def_21 )
| ( inverse(sk_c7) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_633,c_643]) ).
tcf(c_2945,plain,
( ~ iPr_def_12
| ( sk_c10 != iPr_def_18 )
| ( inverse(sk_c1) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_630,c_643]) ).
tcf(c_2946,plain,
( ~ iPr_def_12
| ( sk_c10 != sk_c9 )
| ( inverse(identity) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_103,c_643]) ).
tcf(c_2967,plain,
( ~ iPr_def_12
| ( sk_c10 != iPr_def_28 )
| ( sk_c10 != iPr_def_18 ) ),
inference(light_normalisation,[status(thm)],[c_2945,c_640]) ).
tcf(c_3122,plain,
( ~ iPr_def_11
| ( sk_c8 != iPr_def_25 )
| ( inverse(sk_c3) != sk_c9 ) ),
inference(superposition,[status(thm)],[c_637,c_644]) ).
tcf(c_3125,plain,
( ~ iPr_def_11
| ( sk_c9 != sk_c8 )
| ( inverse(identity) != sk_c9 ) ),
inference(superposition,[status(thm)],[c_103,c_644]) ).
tcf(c_3126,plain,
( ~ iPr_def_11
| ( sk_c8 != identity )
| ( inverse(inverse(sk_c9)) != sk_c9 ) ),
inference(superposition,[status(thm)],[c_104,c_644]) ).
tcf(c_3153,plain,
( ~ iPr_def_11
| ( sk_c8 != iPr_def_25 )
| ( sk_c9 != iPr_def_24 ) ),
inference(light_normalisation,[status(thm)],[c_3122,c_636]) ).
tcf(c_3242,plain,
! [X0: $i,X1: $i] :
( ( iPr_def_16 = X0 )
| ( iPr_def_16 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_697]) ).
tcf(c_3256,plain,
! [X0: $i] :
( ( iPr_def_14 = X0 )
| ( iPr_def_14 != iPr_def_14 )
| ( X0 != iPr_def_14 ) ),
inference(instantiation,[status(thm)],[c_1994]) ).
tcf(c_3257,plain,
( ( iPr_def_14 = sk_c10 )
| ( iPr_def_14 != iPr_def_14 )
| ( sk_c10 != iPr_def_14 ) ),
inference(instantiation,[status(thm)],[c_3256]) ).
tcf(c_3364,plain,
! [X0: $i] : multiply(sk_c2,multiply(sk_c10,X0)) = multiply(iPr_def_27,X0),
inference(superposition,[status(thm)],[c_639,c_105]) ).
tcf(c_3367,plain,
! [X0: $i] : multiply(sk_c7,multiply(sk_c9,X0)) = multiply(iPr_def_21,X0),
inference(superposition,[status(thm)],[c_633,c_105]) ).
tcf(c_3373,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(X0,X1)) = multiply(identity,X1),
inference(superposition,[status(thm)],[c_104,c_105]) ).
tcf(c_3375,plain,
! [X0: $i] : multiply(iPr_def_16,multiply(sk_c10,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1264,c_105]) ).
tcf(c_3376,plain,
! [X0: $i] : multiply(iPr_def_26,multiply(sk_c2,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1265,c_105]) ).
tcf(c_3377,plain,
! [X0: $i] : multiply(iPr_def_24,multiply(sk_c3,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1266,c_105]) ).
tcf(c_3378,plain,
! [X0: $i] : multiply(iPr_def_22,multiply(sk_c4,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1267,c_105]) ).
tcf(c_3381,plain,
! [X0: $i] : multiply(iPr_def_28,multiply(sk_c1,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1270,c_105]) ).
tcf(c_3385,plain,
! [X0: $i] : multiply(iPr_def_28,multiply(sk_c1,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_3381,c_103]) ).
tcf(c_3388,plain,
! [X0: $i] : multiply(iPr_def_22,multiply(sk_c4,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_3378,c_103]) ).
tcf(c_3389,plain,
! [X0: $i] : multiply(iPr_def_24,multiply(sk_c3,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_3377,c_103]) ).
tcf(c_3390,plain,
! [X0: $i] : multiply(iPr_def_26,multiply(sk_c2,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_3376,c_103]) ).
tcf(c_3391,plain,
! [X0: $i] : multiply(iPr_def_16,multiply(sk_c10,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_3375,c_103]) ).
tcf(c_3437,plain,
! [X0: $i,X1: $i] :
( ( multiply(X0,X1) = iPr_def_27 )
| ( iPr_def_27 != multiply(sk_c2,sk_c10) )
| ( multiply(X0,X1) != multiply(sk_c2,sk_c10) ) ),
inference(instantiation,[status(thm)],[c_2152]) ).
tcf(c_3438,plain,
! [X0: $i,X1: $i] :
( ( multiply(X0,X1) = multiply(sk_c2,sk_c10) )
| ( X1 != sk_c10 )
| ( X0 != sk_c2 ) ),
inference(instantiation,[status(thm)],[c_699]) ).
tcf(c_3439,plain,
( ( multiply(sk_c10,sk_c10) = iPr_def_27 )
| ( iPr_def_27 != multiply(sk_c2,sk_c10) )
| ( multiply(sk_c10,sk_c10) != multiply(sk_c2,sk_c10) ) ),
inference(instantiation,[status(thm)],[c_3437]) ).
tcf(c_3440,plain,
( ( multiply(sk_c10,sk_c10) = multiply(sk_c2,sk_c10) )
| ( sk_c10 != sk_c2 )
| ( sk_c10 != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_3438]) ).
tcf(c_3564,plain,
! [X0: $i] :
( ( iPr_def_24 = X0 )
| ( iPr_def_24 != iPr_def_24 )
| ( X0 != iPr_def_24 ) ),
inference(instantiation,[status(thm)],[c_2146]) ).
tcf(c_3571,plain,
! [X0: $i] :
( ( iPr_def_27 = X0 )
| ( iPr_def_27 != sk_c9 )
| ( X0 != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_2151]) ).
tcf(c_3572,plain,
( ( iPr_def_27 = sk_c10 )
| ( iPr_def_27 != sk_c9 )
| ( sk_c10 != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_3571]) ).
tcf(c_3936,plain,
! [X0: $i] :
( ( identity = X0 )
| ( identity != identity )
| ( X0 != identity ) ),
inference(instantiation,[status(thm)],[c_2433]) ).
tcf(c_3937,plain,
( ( identity = sk_c10 )
| ( identity != identity )
| ( sk_c10 != identity ) ),
inference(instantiation,[status(thm)],[c_3936]) ).
tcf(c_4071,plain,
( ~ iPr_def_10
| ( sk_c9 != iPr_def_27 )
| ( inverse(sk_c2) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_639,c_645]) ).
tcf(c_4099,plain,
( ~ iPr_def_10
| ( sk_c9 != iPr_def_27 )
| ( sk_c10 != iPr_def_26 ) ),
inference(light_normalisation,[status(thm)],[c_4071,c_638]) ).
tcf(c_4210,plain,
! [X0: $i] :
( ( iPr_def_14 = X0 )
| ( iPr_def_14 != sk_c9 )
| ( X0 != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_1994]) ).
tcf(c_4800,plain,
! [X0: $i,X1: $i] :
( ( X1 = inverse(X0) )
| ( X1 != iPr_def_16 )
| ( inverse(X0) != iPr_def_16 ) ),
inference(instantiation,[status(thm)],[c_2694]) ).
tcf(c_4802,plain,
! [X0: $i,X1: $i] :
( ( inverse(X0) = X1 )
| ( X1 != iPr_def_16 )
| ( inverse(X0) != iPr_def_16 ) ),
inference(instantiation,[status(thm)],[c_1538]) ).
tcf(c_4922,plain,
! [X0: $i,X1: $i] :
( ( X0 = iPr_def_14 )
| ( iPr_def_14 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_697]) ).
tcf(c_5064,plain,
! [X0: $i,X1: $i] :
( ( sk_c9 = multiply(X0,X1) )
| ( sk_c9 != multiply(identity,iPr_def_27) )
| ( multiply(X0,X1) != multiply(identity,iPr_def_27) ) ),
inference(instantiation,[status(thm)],[c_2907]) ).
tcf(c_5066,plain,
( ( sk_c9 = multiply(sk_c10,sk_c10) )
| ( sk_c9 != multiply(identity,iPr_def_27) )
| ( multiply(sk_c10,sk_c10) != multiply(identity,iPr_def_27) ) ),
inference(instantiation,[status(thm)],[c_5064]) ).
tcf(c_5522,plain,
( ( iPr_def_23 = iPr_def_26 )
| ( iPr_def_15 = iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_2072,c_1074]) ).
tcf(c_5815,plain,
( ( iPr_def_24 = iPr_def_27 )
| ( iPr_def_15 = iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_2115,c_1088]) ).
tcf(c_5891,plain,
! [X0: $i] :
( ( iPr_def_16 = X0 )
| ( iPr_def_16 != iPr_def_16 )
| ( X0 != iPr_def_16 ) ),
inference(instantiation,[status(thm)],[c_3242]) ).
tcf(c_6102,plain,
( ( iPr_def_14 = iPr_def_16 )
| ( multiply(iPr_def_21,sk_c8) = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_2338,c_626]) ).
tcf(c_6391,plain,
( ( iPr_def_21 = iPr_def_23 )
| ( iPr_def_14 = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_2515,c_2338]) ).
tcf(c_6416,plain,
( ( iPr_def_14 = iPr_def_16 )
| ( inverse(iPr_def_23) = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_2515,c_628]) ).
tcf(c_6485,plain,
! [X0: $i,X1: $i] :
( ( X1 = multiply(sk_c10,sk_c8) )
| ( X1 != X0 )
| ( multiply(sk_c10,sk_c8) != X0 ) ),
inference(instantiation,[status(thm)],[c_697]) ).
tcf(c_6982,plain,
multiply(iPr_def_28,iPr_def_18) = sk_c9,
inference(superposition,[status(thm)],[c_630,c_3385]) ).
tcf(c_7034,plain,
multiply(iPr_def_22,iPr_def_23) = sk_c7,
inference(superposition,[status(thm)],[c_635,c_3388]) ).
tcf(c_7078,plain,
multiply(iPr_def_24,iPr_def_25) = sk_c9,
inference(superposition,[status(thm)],[c_637,c_3389]) ).
tcf(c_7275,plain,
! [X0: $i,X1: $i] :
( ( X0 = sk_c2 )
| ( sk_c2 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_697]) ).
tcf(c_7279,plain,
multiply(iPr_def_26,iPr_def_27) = sk_c10,
inference(superposition,[status(thm)],[c_639,c_3390]) ).
tcf(c_7282,plain,
! [X0: $i] : multiply(iPr_def_26,multiply(iPr_def_27,X0)) = multiply(sk_c10,X0),
inference(superposition,[status(thm)],[c_7279,c_105]) ).
tcf(c_7284,plain,
multiply(iPr_def_16,iPr_def_14) = sk_c8,
inference(superposition,[status(thm)],[c_626,c_3391]) ).
tcf(c_8143,plain,
( ( sk_c10 = iPr_def_18 )
| ( multiply(iPr_def_24,iPr_def_25) = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_653,c_1187]) ).
tcf(c_8145,plain,
( ( sk_c9 = iPr_def_15 )
| ( sk_c10 = iPr_def_18 ) ),
inference(light_normalisation,[status(thm)],[c_8143,c_7078]) ).
tcf(c_8378,plain,
( ( iPr_def_15 = iPr_def_27 )
| ( sk_c10 = iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_8145,c_655]) ).
tcf(c_8379,plain,
( ( iPr_def_15 = iPr_def_24 )
| ( sk_c10 = iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_8145,c_652]) ).
tcf(c_8597,plain,
! [X0: $i] :
( ( iPr_def_15 = iPr_def_27 )
| ~ iPr_def_10
| ( inverse(X0) != sk_c10 )
| ( multiply(X0,iPr_def_18) != sk_c9 ) ),
inference(superposition,[status(thm)],[c_8378,c_645]) ).
tcf(c_8673,plain,
( ( iPr_def_15 = iPr_def_27 )
| ~ iPr_def_10
| ( inverse(sk_c10) != sk_c10 )
| ( multiply(sk_c10,iPr_def_18) != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_8597]) ).
tcf(c_8791,plain,
! [X0: $i] :
( ( iPr_def_15 = iPr_def_24 )
| ~ iPr_def_10
| ( inverse(X0) != sk_c10 )
| ( multiply(X0,iPr_def_18) != sk_c9 ) ),
inference(superposition,[status(thm)],[c_8379,c_645]) ).
tcf(c_8867,plain,
( ( iPr_def_15 = iPr_def_24 )
| ~ iPr_def_10
| ( inverse(sk_c10) != sk_c10 )
| ( multiply(sk_c10,iPr_def_18) != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_8791]) ).
tcf(c_9064,plain,
( ( sk_c10 = iPr_def_18 )
| ( multiply(iPr_def_28,iPr_def_18) = iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_1208,c_3385]) ).
tcf(c_9065,plain,
( ( sk_c9 = iPr_def_24 )
| ( sk_c10 = iPr_def_18 ) ),
inference(light_normalisation,[status(thm)],[c_9064,c_6982]) ).
tcf(c_9213,plain,
( ( iPr_def_14 = iPr_def_16 )
| ( iPr_def_16 != sk_c9 )
| ( iPr_def_14 != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_4210]) ).
tcf(c_10010,plain,
( ( sk_c10 = iPr_def_23 )
| ( multiply(iPr_def_26,iPr_def_27) = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_1249,c_3390]) ).
tcf(c_10011,plain,
( ( sk_c10 = iPr_def_28 )
| ( sk_c10 = iPr_def_23 ) ),
inference(light_normalisation,[status(thm)],[c_10010,c_7279]) ).
tcf(c_10403,plain,
( ( sk_c10 = iPr_def_18 )
| ( multiply(iPr_def_26,iPr_def_27) = iPr_def_23 ) ),
inference(superposition,[status(thm)],[c_1252,c_3390]) ).
tcf(c_10404,plain,
( ( sk_c10 = iPr_def_23 )
| ( sk_c10 = iPr_def_18 ) ),
inference(light_normalisation,[status(thm)],[c_10403,c_7279]) ).
tcf(c_10415,plain,
( ( sk_c10 = iPr_def_18 )
| ( multiply(iPr_def_26,iPr_def_27) = iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_1253,c_3390]) ).
tcf(c_10416,plain,
( ( sk_c10 = iPr_def_21 )
| ( sk_c10 = iPr_def_18 ) ),
inference(light_normalisation,[status(thm)],[c_10415,c_7279]) ).
tcf(c_10728,plain,
( ( sk_c10 = iPr_def_28 )
| ( multiply(iPr_def_24,iPr_def_25) = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_663,c_1312]) ).
tcf(c_10731,plain,
( ( sk_c9 = iPr_def_15 )
| ( sk_c10 = iPr_def_28 ) ),
inference(light_normalisation,[status(thm)],[c_10728,c_7078]) ).
tcf(c_10845,plain,
( ( sk_c10 = iPr_def_28 )
| ( multiply(iPr_def_16,iPr_def_14) = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_1330,c_3391]) ).
tcf(c_10846,plain,
( ( sk_c8 = iPr_def_25 )
| ( sk_c10 = iPr_def_28 ) ),
inference(light_normalisation,[status(thm)],[c_10845,c_7284]) ).
tcf(c_10970,plain,
( ( sk_c10 = iPr_def_26 )
| ( multiply(iPr_def_26,iPr_def_27) = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_1346,c_3390]) ).
tcf(c_10971,plain,
( ( sk_c10 = iPr_def_28 )
| ( sk_c10 = iPr_def_26 ) ),
inference(light_normalisation,[status(thm)],[c_10970,c_7279]) ).
tcf(c_11103,plain,
( ( iPr_def_15 = iPr_def_27 )
| ( sk_c10 = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_10731,c_665]) ).
tcf(c_11104,plain,
( ( iPr_def_15 = iPr_def_24 )
| ( sk_c10 = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_10731,c_662]) ).
tcf(c_11243,plain,
( ( iPr_def_15 = iPr_def_27 )
| ( inverse(iPr_def_28) = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_11103,c_628]) ).
tcf(c_11382,plain,
( ( iPr_def_15 = iPr_def_24 )
| ( inverse(iPr_def_28) = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_11104,c_628]) ).
tcf(c_11836,plain,
( ( sk_c10 = iPr_def_28 )
| ( multiply(iPr_def_24,iPr_def_25) = iPr_def_27 ) ),
inference(superposition,[status(thm)],[c_1382,c_3389]) ).
tcf(c_11837,plain,
( ( sk_c9 = iPr_def_27 )
| ( sk_c10 = iPr_def_28 ) ),
inference(light_normalisation,[status(thm)],[c_11836,c_7078]) ).
tcf(c_12643,plain,
( ( sk_c10 = iPr_def_23 )
| ( multiply(iPr_def_24,iPr_def_25) = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_1571,c_3389]) ).
tcf(c_12644,plain,
( ( sk_c9 = iPr_def_14 )
| ( sk_c10 = iPr_def_23 ) ),
inference(light_normalisation,[status(thm)],[c_12643,c_7078]) ).
tcf(c_12762,plain,
( ( sk_c9 = iPr_def_14 )
| ( multiply(iPr_def_24,iPr_def_25) = iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_1628,c_3389]) ).
tcf(c_12763,plain,
( ( sk_c9 = iPr_def_24 )
| ( sk_c9 = iPr_def_14 ) ),
inference(light_normalisation,[status(thm)],[c_12762,c_7078]) ).
tcf(c_13118,plain,
( ( sk_c9 = iPr_def_14 )
| ( multiply(iPr_def_24,iPr_def_25) = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_673,c_1631]) ).
tcf(c_13122,plain,
( ( sk_c9 = iPr_def_15 )
| ( sk_c9 = iPr_def_14 ) ),
inference(light_normalisation,[status(thm)],[c_13118,c_7078]) ).
tcf(c_13396,plain,
( ( sk_c10 = iPr_def_26 )
| ( multiply(iPr_def_24,iPr_def_25) = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_1693,c_3389]) ).
tcf(c_13397,plain,
( ( sk_c9 = iPr_def_14 )
| ( sk_c10 = iPr_def_26 ) ),
inference(light_normalisation,[status(thm)],[c_13396,c_7078]) ).
tcf(c_13503,plain,
( ( iPr_def_15 = iPr_def_24 )
| ( sk_c9 = iPr_def_16 )
| ( sk_c9 = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_13122,c_692]) ).
tcf(c_13508,plain,
( ( iPr_def_15 = iPr_def_27 )
| ( sk_c9 = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_13122,c_675]) ).
tcf(c_13510,plain,
( ( iPr_def_15 = iPr_def_24 )
| ( sk_c9 = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_13122,c_672]) ).
tcf(c_13518,plain,
( ( sk_c9 = iPr_def_14 )
| ( multiply(iPr_def_15,sk_c8) = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_13122,c_627]) ).
tcf(c_13627,plain,
( iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( iPr_def_15 = iPr_def_27 )
| ( sk_c9 != iPr_def_16 )
| ( sk_c10 != iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_13508,c_641]) ).
tcf(c_13643,plain,
( ( iPr_def_15 = iPr_def_27 )
| ( multiply(sk_c1,iPr_def_14) = iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_13508,c_630]) ).
tcf(c_13865,plain,
( ( iPr_def_15 = iPr_def_24 )
| ( multiply(sk_c1,iPr_def_14) = iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_13510,c_630]) ).
tcf(c_14204,plain,
( ( sk_c9 = iPr_def_14 )
| ( multiply(iPr_def_24,iPr_def_25) = iPr_def_27 ) ),
inference(superposition,[status(thm)],[c_1754,c_3389]) ).
tcf(c_14205,plain,
( ( sk_c9 = iPr_def_27 )
| ( sk_c9 = iPr_def_14 ) ),
inference(light_normalisation,[status(thm)],[c_14204,c_7078]) ).
tcf(c_14879,plain,
( ( sk_c10 = iPr_def_15 )
| ( multiply(iPr_def_26,iPr_def_27) = iPr_def_23 ) ),
inference(superposition,[status(thm)],[c_1942,c_3390]) ).
tcf(c_14880,plain,
( ( sk_c10 = iPr_def_23 )
| ( sk_c10 = iPr_def_15 ) ),
inference(light_normalisation,[status(thm)],[c_14879,c_7279]) ).
tcf(c_14910,plain,
( ( sk_c10 = iPr_def_15 )
| ( multiply(iPr_def_24,iPr_def_25) = iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_2012,c_3389]) ).
tcf(c_14911,plain,
( ( sk_c9 = iPr_def_24 )
| ( sk_c10 = iPr_def_15 ) ),
inference(light_normalisation,[status(thm)],[c_14910,c_7078]) ).
tcf(c_14958,plain,
( ( sk_c10 = iPr_def_15 )
| ( multiply(iPr_def_24,iPr_def_25) = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_683,c_2015]) ).
tcf(c_14963,plain,
( ( sk_c9 = iPr_def_15 )
| ( sk_c10 = iPr_def_15 ) ),
inference(light_normalisation,[status(thm)],[c_14958,c_7078]) ).
tcf(c_15043,plain,
( ( iPr_def_15 = iPr_def_27 )
| ( sk_c10 = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_14963,c_685]) ).
tcf(c_15044,plain,
( ( iPr_def_15 = iPr_def_24 )
| ( sk_c10 = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_14963,c_682]) ).
tcf(c_15844,plain,
( ( sk_c10 = iPr_def_15 )
| ( multiply(iPr_def_24,iPr_def_25) = iPr_def_27 ) ),
inference(superposition,[status(thm)],[c_2121,c_3389]) ).
tcf(c_15845,plain,
( ( sk_c9 = iPr_def_27 )
| ( sk_c10 = iPr_def_15 ) ),
inference(light_normalisation,[status(thm)],[c_15844,c_7078]) ).
tcf(c_17323,plain,
( ( sk_c9 = iPr_def_16 )
| ( multiply(iPr_def_24,iPr_def_25) = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_693,c_2617]) ).
tcf(c_17329,plain,
( ( sk_c9 = iPr_def_16 )
| ( sk_c9 = iPr_def_15 ) ),
inference(light_normalisation,[status(thm)],[c_17323,c_7078]) ).
tcf(c_17667,plain,
( ( iPr_def_14 = iPr_def_16 )
| ( sk_c9 = iPr_def_15 )
| ( sk_c10 = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_17329,c_674]) ).
tcf(c_18240,plain,
multiply(sk_c2,iPr_def_14) = multiply(iPr_def_27,sk_c8),
inference(superposition,[status(thm)],[c_626,c_3364]) ).
tcf(c_18374,plain,
! [X0: $i,X1: $i] :
( ( X0 = sk_c9 )
| ( sk_c9 != inverse(X1) )
| ( X0 != inverse(X1) ) ),
inference(instantiation,[status(thm)],[c_1299]) ).
tcf(c_18377,plain,
( ( sk_c10 = sk_c9 )
| ( sk_c9 != inverse(sk_c10) )
| ( sk_c10 != inverse(sk_c10) ) ),
inference(instantiation,[status(thm)],[c_18374]) ).
tcf(c_18842,plain,
multiply(sk_c7,iPr_def_15) = multiply(iPr_def_21,sk_c8),
inference(superposition,[status(thm)],[c_627,c_3367]) ).
tcf(c_21441,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(X0,X1)) = X1,
inference(demodulation,[status(thm)],[c_3373,c_103]) ).
tcf(c_21500,plain,
! [X0: $i] : multiply(inverse(identity),X0) = X0,
inference(superposition,[status(thm)],[c_103,c_21441]) ).
tcf(c_21501,plain,
! [X0: $i] : multiply(inverse(inverse(X0)),identity) = X0,
inference(superposition,[status(thm)],[c_104,c_21441]) ).
tcf(c_21502,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(inverse(multiply(X0,X1)),multiply(X0,multiply(X1,X2))) = X2,
inference(superposition,[status(thm)],[c_105,c_21441]) ).
tcf(c_21720,plain,
! [X0: $i] : multiply(inverse(iPr_def_16),X0) = multiply(sk_c10,X0),
inference(superposition,[status(thm)],[c_3391,c_21441]) ).
tcf(c_21721,plain,
! [X0: $i] : multiply(inverse(iPr_def_26),X0) = multiply(sk_c2,X0),
inference(superposition,[status(thm)],[c_3390,c_21441]) ).
tcf(c_21722,plain,
! [X0: $i] : multiply(inverse(iPr_def_24),X0) = multiply(sk_c3,X0),
inference(superposition,[status(thm)],[c_3389,c_21441]) ).
tcf(c_21723,plain,
! [X0: $i] : multiply(inverse(iPr_def_22),X0) = multiply(sk_c4,X0),
inference(superposition,[status(thm)],[c_3388,c_21441]) ).
tcf(c_21726,plain,
! [X0: $i] : multiply(inverse(iPr_def_28),X0) = multiply(sk_c1,X0),
inference(superposition,[status(thm)],[c_3385,c_21441]) ).
tcf(c_21794,plain,
! [X0: $i,X1: $i] : multiply(inverse(inverse(X0)),X1) = multiply(X0,X1),
inference(superposition,[status(thm)],[c_21441,c_21441]) ).
tcf(c_22915,plain,
! [X0: $i] : multiply(X0,identity) = X0,
inference(demodulation,[status(thm)],[c_21501,c_21794]) ).
tcf(c_22944,plain,
inverse(identity) = identity,
inference(superposition,[status(thm)],[c_22915,c_21500]) ).
tcf(c_26049,plain,
multiply(sk_c10,iPr_def_16) = identity,
inference(superposition,[status(thm)],[c_21720,c_104]) ).
tcf(c_26052,plain,
! [X0: $i] : multiply(sk_c10,multiply(iPr_def_16,X0)) = X0,
inference(superposition,[status(thm)],[c_21720,c_21441]) ).
tcf(c_26053,plain,
multiply(sk_c10,identity) = inverse(iPr_def_16),
inference(superposition,[status(thm)],[c_21720,c_22915]) ).
tcf(c_26117,plain,
multiply(sk_c2,identity) = multiply(iPr_def_27,iPr_def_16),
inference(superposition,[status(thm)],[c_26049,c_3364]) ).
tcf(c_26334,plain,
inverse(iPr_def_16) = sk_c10,
inference(demodulation,[status(thm)],[c_26053,c_22915]) ).
tcf(c_26819,plain,
multiply(sk_c10,sk_c8) = iPr_def_14,
inference(superposition,[status(thm)],[c_7284,c_26052]) ).
tcf(c_27116,plain,
( ( iPr_def_24 = iPr_def_14 )
| ( iPr_def_24 != iPr_def_24 )
| ( iPr_def_14 != iPr_def_24 ) ),
inference(instantiation,[status(thm)],[c_3564]) ).
tcf(c_27118,plain,
( ( sk_c9 = iPr_def_14 )
| ( iPr_def_14 != iPr_def_24 )
| ( sk_c9 != iPr_def_24 ) ),
inference(instantiation,[status(thm)],[c_1336]) ).
tcf(c_27119,plain,
! [X0: $i] :
( ( X0 = iPr_def_14 )
| ( iPr_def_14 != iPr_def_24 )
| ( X0 != iPr_def_24 ) ),
inference(instantiation,[status(thm)],[c_4922]) ).
tcf(c_27127,plain,
( ( sk_c9 = iPr_def_14 )
| ( iPr_def_14 != iPr_def_27 )
| ( sk_c9 != iPr_def_27 ) ),
inference(instantiation,[status(thm)],[c_1370]) ).
tcf(c_27293,plain,
multiply(iPr_def_27,iPr_def_16) = sk_c2,
inference(demodulation,[status(thm)],[c_26117,c_22915]) ).
tcf(c_27563,plain,
multiply(sk_c2,iPr_def_26) = identity,
inference(superposition,[status(thm)],[c_21721,c_104]) ).
tcf(c_27567,plain,
multiply(sk_c2,identity) = inverse(iPr_def_26),
inference(superposition,[status(thm)],[c_21721,c_22915]) ).
tcf(c_27598,plain,
( ( identity = iPr_def_27 )
| ( sk_c10 = iPr_def_15 ) ),
inference(demodulation,[status(thm)],[c_2076,c_27563]) ).
tcf(c_27599,plain,
( ( identity = iPr_def_27 )
| ( sk_c10 = iPr_def_18 ) ),
inference(demodulation,[status(thm)],[c_1251,c_27563]) ).
tcf(c_27678,plain,
inverse(iPr_def_26) = sk_c2,
inference(demodulation,[status(thm)],[c_27567,c_22915]) ).
tcf(c_27681,plain,
( ( sk_c2 = iPr_def_16 )
| ( sk_c10 = iPr_def_15 ) ),
inference(demodulation,[status(thm)],[c_2079,c_27678]) ).
tcf(c_27692,plain,
( ( iPr_def_15 = iPr_def_18 )
| ( inverse(iPr_def_23) = sk_c2 ) ),
inference(superposition,[status(thm)],[c_5522,c_27678]) ).
tcf(c_27910,plain,
( ( identity = iPr_def_27 )
| ( multiply(iPr_def_15,sk_c8) = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_27598,c_626]) ).
tcf(c_28027,plain,
( ( iPr_def_15 = iPr_def_18 )
| ( identity = iPr_def_27 ) ),
inference(superposition,[status(thm)],[c_27599,c_27598]) ).
tcf(c_28689,plain,
! [X0: $i] :
( ( iPr_def_15 = iPr_def_18 )
| ( multiply(iPr_def_27,X0) = X0 ) ),
inference(superposition,[status(thm)],[c_28027,c_103]) ).
tcf(c_29023,plain,
( ( iPr_def_16 = iPr_def_14 )
| ( iPr_def_16 != iPr_def_16 )
| ( iPr_def_14 != iPr_def_16 ) ),
inference(instantiation,[status(thm)],[c_5891]) ).
tcf(c_29030,plain,
! [X0: $i] :
( ( iPr_def_14 = inverse(X0) )
| ( iPr_def_14 != iPr_def_16 )
| ( inverse(X0) != iPr_def_16 ) ),
inference(instantiation,[status(thm)],[c_4800]) ).
tcf(c_29031,plain,
! [X0: $i] :
( ( inverse(X0) = iPr_def_14 )
| ( iPr_def_14 != iPr_def_16 )
| ( inverse(X0) != iPr_def_16 ) ),
inference(instantiation,[status(thm)],[c_4802]) ).
tcf(c_29032,plain,
( ( inverse(sk_c10) = iPr_def_14 )
| ( iPr_def_14 != iPr_def_16 )
| ( inverse(sk_c10) != iPr_def_16 ) ),
inference(instantiation,[status(thm)],[c_29031]) ).
tcf(c_29033,plain,
( ( iPr_def_14 = inverse(sk_c10) )
| ( iPr_def_14 != iPr_def_16 )
| ( inverse(sk_c10) != iPr_def_16 ) ),
inference(instantiation,[status(thm)],[c_29030]) ).
tcf(c_29344,plain,
multiply(sk_c3,identity) = inverse(iPr_def_24),
inference(superposition,[status(thm)],[c_21722,c_22915]) ).
tcf(c_29404,plain,
inverse(iPr_def_24) = sk_c3,
inference(demodulation,[status(thm)],[c_29344,c_22915]) ).
tcf(c_29649,plain,
! [X0: $i] :
( ( X0 = iPr_def_24 )
| ( iPr_def_24 != iPr_def_27 )
| ( X0 != iPr_def_27 ) ),
inference(instantiation,[status(thm)],[c_1614]) ).
tcf(c_29657,plain,
( ( iPr_def_24 = sk_c9 )
| ( iPr_def_24 != iPr_def_14 )
| ( sk_c9 != iPr_def_14 ) ),
inference(instantiation,[status(thm)],[c_1925]) ).
tcf(c_30218,plain,
! [X0: $i] :
( ( X0 = iPr_def_16 )
| ( iPr_def_16 != iPr_def_14 )
| ( X0 != iPr_def_14 ) ),
inference(instantiation,[status(thm)],[c_1892]) ).
tcf(c_30223,plain,
( ( sk_c9 = iPr_def_16 )
| ( iPr_def_16 != iPr_def_14 )
| ( sk_c9 != iPr_def_14 ) ),
inference(instantiation,[status(thm)],[c_1926]) ).
tcf(c_32886,plain,
multiply(sk_c4,iPr_def_22) = identity,
inference(superposition,[status(thm)],[c_21723,c_104]) ).
tcf(c_32889,plain,
! [X0: $i] : multiply(sk_c4,multiply(iPr_def_22,X0)) = X0,
inference(superposition,[status(thm)],[c_21723,c_21441]) ).
tcf(c_32911,plain,
( ( identity = iPr_def_23 )
| ( sk_c9 = iPr_def_16 ) ),
inference(demodulation,[status(thm)],[c_2482,c_32886]) ).
tcf(c_32912,plain,
( ( identity = iPr_def_23 )
| ( sk_c10 = iPr_def_15 ) ),
inference(demodulation,[status(thm)],[c_1904,c_32886]) ).
tcf(c_32913,plain,
( ( identity = iPr_def_23 )
| ( sk_c9 = iPr_def_14 ) ),
inference(demodulation,[status(thm)],[c_1548,c_32886]) ).
tcf(c_32914,plain,
( ( identity = iPr_def_23 )
| ( sk_c10 = iPr_def_18 ) ),
inference(demodulation,[status(thm)],[c_1233,c_32886]) ).
tcf(c_32915,plain,
( ( identity = iPr_def_23 )
| ( sk_c10 = iPr_def_28 ) ),
inference(demodulation,[status(thm)],[c_1231,c_32886]) ).
tcf(c_33551,plain,
( ( identity = iPr_def_23 )
| ( multiply(sk_c1,iPr_def_16) = iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_32911,c_630]) ).
tcf(c_34045,plain,
( ( iPr_def_14 = iPr_def_16 )
| ( identity = iPr_def_23 ) ),
inference(superposition,[status(thm)],[c_32913,c_32911]) ).
tcf(c_34183,plain,
multiply(sk_c4,sk_c7) = iPr_def_23,
inference(superposition,[status(thm)],[c_7034,c_32889]) ).
tcf(c_34361,plain,
( ( iPr_def_15 = iPr_def_18 )
| ( identity = iPr_def_23 ) ),
inference(superposition,[status(thm)],[c_32914,c_32912]) ).
tcf(c_35239,plain,
( ( identity = iPr_def_23 )
| ( inverse(iPr_def_28) = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_32915,c_628]) ).
tcf(c_35808,plain,
( ( iPr_def_14 = iPr_def_16 )
| ( inverse(iPr_def_23) = iPr_def_23 ) ),
inference(superposition,[status(thm)],[c_34045,c_22944]) ).
tcf(c_35950,plain,
( ( iPr_def_15 = iPr_def_18 )
| ( inverse(iPr_def_23) = iPr_def_23 ) ),
inference(superposition,[status(thm)],[c_34361,c_22944]) ).
tcf(c_35952,plain,
! [X0: $i] :
( ( iPr_def_15 = iPr_def_18 )
| ( multiply(iPr_def_23,X0) = X0 ) ),
inference(superposition,[status(thm)],[c_34361,c_103]) ).
tcf(c_37980,plain,
( ( iPr_def_14 = iPr_def_15 )
| ( identity = iPr_def_27 )
| ( sk_c9 = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_27910,c_13518]) ).
tcf(c_38104,plain,
( ( iPr_def_15 = iPr_def_18 )
| ( sk_c2 = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_28689,c_27293]) ).
tcf(c_38836,plain,
( ( iPr_def_15 = iPr_def_18 )
| ( inverse(iPr_def_16) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_38104,c_638]) ).
tcf(c_38837,plain,
( ( iPr_def_15 = iPr_def_18 )
| ( sk_c10 = iPr_def_26 ) ),
inference(light_normalisation,[status(thm)],[c_38836,c_26334]) ).
tcf(c_41015,plain,
( ~ iPr_def_12
| ( sk_c10 != iPr_def_21 )
| ( inverse(sk_c7) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_633,c_643]) ).
tcf(c_41231,plain,
( ~ iPr_def_10
| ( sk_c10 != sk_c9 )
| ( inverse(identity) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_103,c_645]) ).
tcf(c_41314,plain,
( iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( sk_c10 = iPr_def_23 )
| ( sk_c9 != iPr_def_16 )
| ( sk_c10 != iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_671,c_641]) ).
tcf(c_45440,plain,
! [X0: $i,X1: $i] :
( ( X0 = iPr_def_14 )
| ( iPr_def_14 != inverse(X1) )
| ( X0 != inverse(X1) ) ),
inference(instantiation,[status(thm)],[c_4922]) ).
tcf(c_45443,plain,
( ( sk_c10 = iPr_def_14 )
| ( iPr_def_14 != inverse(sk_c10) )
| ( sk_c10 != inverse(sk_c10) ) ),
inference(instantiation,[status(thm)],[c_45440]) ).
tcf(c_46550,plain,
! [X0: $i] : multiply(sk_c1,multiply(iPr_def_28,X0)) = X0,
inference(superposition,[status(thm)],[c_21726,c_21441]) ).
tcf(c_46551,plain,
multiply(sk_c1,identity) = inverse(iPr_def_28),
inference(superposition,[status(thm)],[c_21726,c_22915]) ).
tcf(c_47022,plain,
inverse(iPr_def_28) = sk_c1,
inference(demodulation,[status(thm)],[c_46551,c_22915]) ).
tcf(c_47024,plain,
( ( identity = iPr_def_23 )
| ( sk_c1 = iPr_def_16 ) ),
inference(demodulation,[status(thm)],[c_35239,c_47022]) ).
tcf(c_47026,plain,
( ( iPr_def_15 = iPr_def_24 )
| ( sk_c1 = iPr_def_16 ) ),
inference(demodulation,[status(thm)],[c_11382,c_47022]) ).
tcf(c_47027,plain,
( ( iPr_def_15 = iPr_def_27 )
| ( sk_c1 = iPr_def_16 ) ),
inference(demodulation,[status(thm)],[c_11243,c_47022]) ).
tcf(c_47032,plain,
( ( sk_c1 = iPr_def_16 )
| ( sk_c10 = iPr_def_23 ) ),
inference(demodulation,[status(thm)],[c_1169,c_47022]) ).
tcf(c_47033,plain,
( ( sk_c1 = iPr_def_16 )
| ( sk_c10 = iPr_def_21 ) ),
inference(demodulation,[status(thm)],[c_1134,c_47022]) ).
tcf(c_47206,plain,
multiply(sk_c1,sk_c9) = iPr_def_18,
inference(superposition,[status(thm)],[c_6982,c_46550]) ).
tcf(c_47602,plain,
( ( identity = iPr_def_23 )
| ( multiply(iPr_def_16,iPr_def_16) = iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_47024,c_33551]) ).
tcf(c_47751,plain,
( ( iPr_def_15 = iPr_def_24 )
| ( multiply(iPr_def_16,iPr_def_14) = iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_47026,c_13865]) ).
tcf(c_47779,plain,
( ( iPr_def_15 = iPr_def_24 )
| ( multiply(iPr_def_16,sk_c9) = iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_47026,c_630]) ).
tcf(c_47784,plain,
( ( iPr_def_15 = iPr_def_24 )
| ( sk_c8 = iPr_def_18 ) ),
inference(light_normalisation,[status(thm)],[c_47751,c_7284]) ).
tcf(c_47873,plain,
( ( iPr_def_15 = iPr_def_27 )
| ( multiply(iPr_def_16,iPr_def_14) = iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_47027,c_13643]) ).
tcf(c_47900,plain,
( ( iPr_def_15 = iPr_def_27 )
| ( multiply(iPr_def_16,sk_c9) = iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_47027,c_630]) ).
tcf(c_47905,plain,
( ( iPr_def_15 = iPr_def_27 )
| ( sk_c8 = iPr_def_18 ) ),
inference(light_normalisation,[status(thm)],[c_47873,c_7284]) ).
tcf(c_48444,plain,
( ( sk_c10 = iPr_def_23 )
| ( multiply(iPr_def_16,iPr_def_16) = iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_47032,c_2521]) ).
tcf(c_50344,plain,
! [X0: $i,X1: $i] :
( ( multiply(inverse(X0),sk_c9) = sk_c10 )
| ( sk_c10 != X1 )
| ( multiply(inverse(X0),sk_c9) != X1 ) ),
inference(instantiation,[status(thm)],[c_697]) ).
tcf(c_52632,plain,
( ( iPr_def_15 = iPr_def_24 )
| ~ iPr_def_11
| ( sk_c8 != iPr_def_18 )
| ( inverse(iPr_def_16) != sk_c9 ) ),
inference(superposition,[status(thm)],[c_47779,c_644]) ).
tcf(c_52636,plain,
( ( iPr_def_15 = iPr_def_24 )
| ( multiply(sk_c10,iPr_def_18) = sk_c9 ) ),
inference(superposition,[status(thm)],[c_47779,c_26052]) ).
tcf(c_52650,plain,
( ( iPr_def_15 = iPr_def_24 )
| ~ iPr_def_11
| ( sk_c8 != iPr_def_18 )
| ( sk_c10 != sk_c9 ) ),
inference(light_normalisation,[status(thm)],[c_52632,c_26334]) ).
tcf(c_54204,plain,
( ( iPr_def_15 = iPr_def_27 )
| ~ iPr_def_11
| ( sk_c8 != iPr_def_18 )
| ( inverse(iPr_def_16) != sk_c9 ) ),
inference(superposition,[status(thm)],[c_47900,c_644]) ).
tcf(c_54208,plain,
( ( iPr_def_15 = iPr_def_27 )
| ( multiply(sk_c10,iPr_def_18) = sk_c9 ) ),
inference(superposition,[status(thm)],[c_47900,c_26052]) ).
tcf(c_54222,plain,
( ( iPr_def_15 = iPr_def_27 )
| ~ iPr_def_11
| ( sk_c8 != iPr_def_18 )
| ( sk_c10 != sk_c9 ) ),
inference(light_normalisation,[status(thm)],[c_54204,c_26334]) ).
tcf(c_54556,plain,
( ( iPr_def_14 = iPr_def_16 )
| ( sk_c9 = iPr_def_15 ) ),
inference(global_subsumption_just,[status(thm)],[c_17667,c_1890,c_1891,c_1924,c_1993,c_9213,c_13122,c_17329]) ).
tcf(c_54691,plain,
( ( iPr_def_14 = iPr_def_16 )
| ( multiply(sk_c7,iPr_def_15) = iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_54556,c_633]) ).
tcf(c_54701,plain,
( ( iPr_def_14 = iPr_def_16 )
| ( multiply(iPr_def_21,sk_c8) = iPr_def_21 ) ),
inference(light_normalisation,[status(thm)],[c_54691,c_18842]) ).
tcf(c_58770,plain,
( ( iPr_def_16 = iPr_def_23 )
| ( iPr_def_14 = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_35808,c_6416]) ).
tcf(c_59084,plain,
( ( iPr_def_16 = iPr_def_21 )
| ( iPr_def_14 = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_58770,c_6391]) ).
tcf(c_64013,plain,
( ( iPr_def_14 = iPr_def_21 )
| ( iPr_def_14 = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_54701,c_6102]) ).
tcf(c_64096,plain,
iPr_def_14 = iPr_def_16,
inference(superposition,[status(thm)],[c_64013,c_59084]) ).
tcf(c_64152,plain,
( ( sk_c1 = iPr_def_14 )
| ( sk_c10 = iPr_def_21 ) ),
inference(demodulation,[status(thm)],[c_47033,c_64096]) ).
tcf(c_64184,plain,
( ( iPr_def_15 = iPr_def_18 )
| ( sk_c2 = iPr_def_14 ) ),
inference(demodulation,[status(thm)],[c_38104,c_64096]) ).
tcf(c_64200,plain,
( ( sk_c2 = iPr_def_14 )
| ( sk_c10 = iPr_def_15 ) ),
inference(demodulation,[status(thm)],[c_27681,c_64096]) ).
tcf(c_64207,plain,
multiply(iPr_def_27,iPr_def_14) = sk_c2,
inference(demodulation,[status(thm)],[c_27293,c_64096]) ).
tcf(c_64214,plain,
inverse(iPr_def_14) = sk_c10,
inference(demodulation,[status(thm)],[c_26334,c_64096]) ).
tcf(c_64215,plain,
multiply(sk_c10,iPr_def_14) = identity,
inference(demodulation,[status(thm)],[c_26049,c_64096]) ).
tcf(c_64315,plain,
multiply(iPr_def_14,iPr_def_14) = sk_c8,
inference(demodulation,[status(thm)],[c_7284,c_64096]) ).
tcf(c_64322,plain,
( iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( sk_c9 != iPr_def_14 )
| ( sk_c10 != iPr_def_15 ) ),
inference(demodulation,[status(thm)],[c_641,c_64096]) ).
tcf(c_64333,plain,
multiply(iPr_def_14,sk_c10) = identity,
inference(demodulation,[status(thm)],[c_1264,c_64096]) ).
tcf(c_64334,plain,
inverse(sk_c10) = iPr_def_14,
inference(demodulation,[status(thm)],[c_628,c_64096]) ).
tcf(c_65600,plain,
( ~ iPr_def_10
| ( sk_c9 != identity )
| ( inverse(iPr_def_14) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_64333,c_645]) ).
tcf(c_65637,plain,
( ~ iPr_def_10
| ( sk_c9 != identity ) ),
inference(ground_joinability,[status(thm)],[c_65600,c_64214]) ).
tcf(c_65711,plain,
( ( sk_c9 = iPr_def_14 )
| ~ iPr_def_10
| ( identity != iPr_def_27 ) ),
inference(superposition,[status(thm)],[c_675,c_65637]) ).
tcf(c_65716,plain,
( ( sk_c10 = iPr_def_28 )
| ~ iPr_def_10
| ( identity != iPr_def_27 ) ),
inference(superposition,[status(thm)],[c_665,c_65637]) ).
tcf(c_65718,plain,
( ( sk_c10 = iPr_def_18 )
| ~ iPr_def_10
| ( identity != iPr_def_27 ) ),
inference(superposition,[status(thm)],[c_655,c_65637]) ).
tcf(c_65815,plain,
( ( sk_c10 = iPr_def_21 )
| ( multiply(iPr_def_14,sk_c9) = iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_64152,c_630]) ).
tcf(c_65843,plain,
( ( sk_c9 = iPr_def_14 )
| ~ iPr_def_10 ),
inference(global_subsumption_just,[status(thm)],[c_65711,c_4099,c_13397,c_14205]) ).
tcf(c_65992,plain,
( ( sk_c10 = iPr_def_28 )
| ~ iPr_def_10 ),
inference(global_subsumption_just,[status(thm)],[c_65716,c_4099,c_10971,c_11837]) ).
tcf(c_66346,plain,
( ( sk_c10 = iPr_def_18 )
| ~ iPr_def_10 ),
inference(global_subsumption_just,[status(thm)],[c_65718,c_27599,c_65718]) ).
tcf(c_67076,plain,
( ( sk_c10 = iPr_def_21 )
| ~ iPr_def_12
| ( sk_c10 != iPr_def_18 )
| ( inverse(iPr_def_14) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_65815,c_643]) ).
tcf(c_67085,plain,
( ( sk_c10 = iPr_def_21 )
| ~ iPr_def_12
| ( sk_c10 != iPr_def_18 ) ),
inference(ground_joinability,[status(thm)],[c_67076,c_64214]) ).
tcf(c_67890,plain,
( ( identity = iPr_def_23 )
| ~ iPr_def_12
| ( sk_c10 != iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_32914,c_2967]) ).
tcf(c_67896,plain,
( ( identity = iPr_def_27 )
| ~ iPr_def_12
| ( sk_c10 != iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_27599,c_2967]) ).
tcf(c_67923,plain,
( ( iPr_def_24 = iPr_def_27 )
| ~ iPr_def_12
| ( sk_c10 != iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_1088,c_2967]) ).
tcf(c_68132,plain,
( ( iPr_def_14 = sk_c9 )
| ( iPr_def_14 != multiply(sk_c10,sk_c8) )
| ( sk_c9 != multiply(sk_c10,sk_c8) ) ),
inference(instantiation,[status(thm)],[c_1271]) ).
tcf(c_69638,plain,
( ( sk_c10 = iPr_def_28 )
| ~ iPr_def_11
| ( sk_c8 != iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_662,c_3153]) ).
tcf(c_70012,plain,
! [X0: $i] :
( ( sk_c9 = identity )
| ( identity != X0 )
| ( sk_c9 != X0 ) ),
inference(instantiation,[status(thm)],[c_1274]) ).
tcf(c_70019,plain,
( ( sk_c9 = identity )
| ( identity != sk_c10 )
| ( sk_c9 != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_70012]) ).
tcf(c_70499,plain,
( ( iPr_def_15 = iPr_def_18 )
| ( sk_c2 = iPr_def_23 ) ),
inference(superposition,[status(thm)],[c_35950,c_27692]) ).
tcf(c_71142,plain,
! [X0: $i,X1: $i] :
( ( inverse(X0) = identity )
| ( identity != X1 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_1538]) ).
tcf(c_71149,plain,
( ( inverse(sk_c10) = identity )
| ( identity != sk_c10 )
| ( inverse(sk_c10) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_71142]) ).
tcf(c_71160,plain,
! [X0: $i] :
( ( inverse(X0) = sk_c9 )
| ( sk_c9 != iPr_def_14 )
| ( inverse(X0) != iPr_def_14 ) ),
inference(instantiation,[status(thm)],[c_1925]) ).
tcf(c_71161,plain,
! [X0: $i] :
( ( sk_c9 = inverse(X0) )
| ( sk_c9 != iPr_def_14 )
| ( inverse(X0) != iPr_def_14 ) ),
inference(instantiation,[status(thm)],[c_1926]) ).
tcf(c_71162,plain,
( ( sk_c9 = inverse(sk_c10) )
| ( sk_c9 != iPr_def_14 )
| ( inverse(sk_c10) != iPr_def_14 ) ),
inference(instantiation,[status(thm)],[c_71161]) ).
tcf(c_71163,plain,
( ( inverse(sk_c10) = sk_c9 )
| ( sk_c9 != iPr_def_14 )
| ( inverse(sk_c10) != iPr_def_14 ) ),
inference(instantiation,[status(thm)],[c_71160]) ).
tcf(c_71436,plain,
( ( iPr_def_15 = iPr_def_18 )
| ( iPr_def_14 = iPr_def_23 ) ),
inference(superposition,[status(thm)],[c_70499,c_64184]) ).
tcf(c_71483,plain,
( ( iPr_def_15 = iPr_def_18 )
| ( multiply(iPr_def_23,sk_c10) = iPr_def_27 ) ),
inference(superposition,[status(thm)],[c_70499,c_639]) ).
tcf(c_71536,plain,
( ( iPr_def_15 = iPr_def_18 )
| ( inverse(iPr_def_14) = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_71436,c_35950]) ).
tcf(c_71552,plain,
( ( iPr_def_15 = iPr_def_18 )
| ( sk_c10 = iPr_def_14 ) ),
inference(light_normalisation,[status(thm)],[c_71536,c_64214]) ).
tcf(c_71638,plain,
( ( iPr_def_15 = iPr_def_18 )
| ( multiply(iPr_def_14,iPr_def_14) = identity ) ),
inference(superposition,[status(thm)],[c_71552,c_64215]) ).
tcf(c_71709,plain,
( ( iPr_def_15 = iPr_def_18 )
| ( multiply(sk_c2,iPr_def_14) = iPr_def_27 ) ),
inference(superposition,[status(thm)],[c_71552,c_639]) ).
tcf(c_71720,plain,
( ( iPr_def_15 = iPr_def_18 )
| ( multiply(iPr_def_27,sk_c8) = iPr_def_27 ) ),
inference(light_normalisation,[status(thm)],[c_71709,c_18240]) ).
tcf(c_71723,plain,
( ( iPr_def_15 = iPr_def_18 )
| ( sk_c8 = identity ) ),
inference(light_normalisation,[status(thm)],[c_71638,c_64315]) ).
tcf(c_73161,plain,
( ( identity = sk_c9 )
| ( identity != iPr_def_24 )
| ( sk_c9 != iPr_def_24 ) ),
inference(instantiation,[status(thm)],[c_1403]) ).
tcf(c_73781,plain,
( ~ iPr_def_12
| ( inverse(sk_c7) != sk_c10 ) ),
inference(global_subsumption_just,[status(thm)],[c_2944,c_2944,c_10416,c_67085]) ).
tcf(c_74018,plain,
( ~ iPr_def_12
| ( sk_c10 != identity )
| ( sk_c10 != sk_c9 ) ),
inference(light_normalisation,[status(thm)],[c_2946,c_22944]) ).
tcf(c_74044,plain,
( ( sk_c10 = iPr_def_28 )
| ~ iPr_def_12
| ( sk_c10 != iPr_def_15 )
| ( sk_c10 != identity ) ),
inference(superposition,[status(thm)],[c_10731,c_74018]) ).
tcf(c_74046,plain,
( ( sk_c10 = iPr_def_18 )
| ~ iPr_def_12
| ( sk_c10 != iPr_def_15 )
| ( sk_c10 != identity ) ),
inference(superposition,[status(thm)],[c_8145,c_74018]) ).
tcf(c_74051,plain,
( ( sk_c10 = iPr_def_15 )
| ~ iPr_def_12
| ( sk_c10 != iPr_def_24 )
| ( sk_c10 != identity ) ),
inference(superposition,[status(thm)],[c_682,c_74018]) ).
tcf(c_74163,plain,
( ( identity = sk_c9 )
| ( identity != iPr_def_27 )
| ( sk_c9 != iPr_def_27 ) ),
inference(instantiation,[status(thm)],[c_1405]) ).
tcf(c_74166,plain,
! [X0: $i] :
( ( X0 = identity )
| ( identity != sk_c9 )
| ( X0 != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_1791]) ).
tcf(c_74167,plain,
( ( sk_c10 = identity )
| ( identity != sk_c9 )
| ( sk_c10 != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_74166]) ).
tcf(c_74346,plain,
( ( iPr_def_15 = iPr_def_18 )
| ( sk_c10 = iPr_def_27 ) ),
inference(superposition,[status(thm)],[c_71483,c_35952]) ).
tcf(c_74401,plain,
multiply(inverse(sk_c9),sk_c9) = identity,
inference(instantiation,[status(thm)],[c_104]) ).
tcf(c_74406,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(inverse(X0),sk_c9) = X2 )
| ( X2 != X1 )
| ( multiply(inverse(X0),sk_c9) != X1 ) ),
inference(instantiation,[status(thm)],[c_697]) ).
tcf(c_74407,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(inverse(X0),sk_c9) = sk_c10 )
| ( sk_c10 != multiply(X1,X2) )
| ( multiply(inverse(X0),sk_c9) != multiply(X1,X2) ) ),
inference(instantiation,[status(thm)],[c_50344]) ).
tcf(c_74408,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(inverse(X0),sk_c9) = multiply(X1,X2) )
| ( sk_c9 != X2 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_699]) ).
tcf(c_74409,plain,
( ( multiply(inverse(sk_c10),sk_c9) = sk_c10 )
| ( sk_c10 != multiply(sk_c10,sk_c10) )
| ( multiply(inverse(sk_c10),sk_c9) != multiply(sk_c10,sk_c10) ) ),
inference(instantiation,[status(thm)],[c_74407]) ).
tcf(c_74410,plain,
( ( multiply(inverse(sk_c10),sk_c9) = multiply(sk_c10,sk_c10) )
| ( sk_c9 != sk_c10 )
| ( inverse(sk_c10) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_74408]) ).
tcf(c_74953,plain,
( ( sk_c9 = multiply(sk_c10,sk_c8) )
| ( sk_c9 != sk_c9 )
| ( multiply(sk_c10,sk_c8) != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_1290]) ).
tcf(c_75547,plain,
( ( iPr_def_15 = iPr_def_18 )
| ( iPr_def_14 = iPr_def_27 ) ),
inference(superposition,[status(thm)],[c_74346,c_71552]) ).
tcf(c_75559,plain,
( ( iPr_def_15 = iPr_def_18 )
| ( multiply(iPr_def_27,iPr_def_14) = identity ) ),
inference(superposition,[status(thm)],[c_74346,c_64215]) ).
tcf(c_75576,plain,
( ( iPr_def_26 = iPr_def_27 )
| ( iPr_def_15 = iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_74346,c_38837]) ).
tcf(c_75634,plain,
( ( iPr_def_15 = iPr_def_18 )
| ( multiply(iPr_def_27,sk_c8) = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_74346,c_626]) ).
tcf(c_75647,plain,
( ( iPr_def_15 = iPr_def_18 )
| ( sk_c2 = identity ) ),
inference(light_normalisation,[status(thm)],[c_75559,c_64207]) ).
tcf(c_75774,plain,
! [X0: $i] :
( ( multiply(sk_c10,sk_c8) = sk_c9 )
| ( sk_c9 != X0 )
| ( multiply(sk_c10,sk_c8) != X0 ) ),
inference(instantiation,[status(thm)],[c_1299]) ).
tcf(c_75775,plain,
( ( multiply(sk_c10,sk_c8) = sk_c9 )
| ( sk_c9 != sk_c10 )
| ( multiply(sk_c10,sk_c8) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_75774]) ).
tcf(c_79384,plain,
( ( iPr_def_15 = iPr_def_18 )
| ( sk_c8 = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_75634,c_28689]) ).
tcf(c_79506,plain,
( ( iPr_def_15 = iPr_def_18 )
| ( multiply(iPr_def_14,iPr_def_14) = sk_c2 ) ),
inference(superposition,[status(thm)],[c_75547,c_64207]) ).
tcf(c_79539,plain,
( ( iPr_def_15 = iPr_def_18 )
| ( iPr_def_14 = iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_75547,c_5815]) ).
tcf(c_79550,plain,
( ( iPr_def_15 = iPr_def_18 )
| ( sk_c2 = sk_c8 ) ),
inference(light_normalisation,[status(thm)],[c_79506,c_64315]) ).
tcf(c_80285,plain,
( ( iPr_def_24 = iPr_def_26 )
| ( iPr_def_15 = iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_75576,c_5815]) ).
tcf(c_80437,plain,
! [X0: $i] :
( ( inverse(X0) = sk_c10 )
| ( sk_c10 != iPr_def_14 )
| ( inverse(X0) != iPr_def_14 ) ),
inference(instantiation,[status(thm)],[c_1425]) ).
tcf(c_80438,plain,
! [X0: $i] :
( ( sk_c10 = inverse(X0) )
| ( sk_c10 != iPr_def_14 )
| ( inverse(X0) != iPr_def_14 ) ),
inference(instantiation,[status(thm)],[c_1921]) ).
tcf(c_80439,plain,
( ( sk_c10 = inverse(sk_c10) )
| ( sk_c10 != iPr_def_14 )
| ( inverse(sk_c10) != iPr_def_14 ) ),
inference(instantiation,[status(thm)],[c_80438]) ).
tcf(c_80440,plain,
( ( inverse(sk_c10) = sk_c10 )
| ( sk_c10 != iPr_def_14 )
| ( inverse(sk_c10) != iPr_def_14 ) ),
inference(instantiation,[status(thm)],[c_80437]) ).
tcf(c_80477,plain,
( ( iPr_def_15 = iPr_def_18 )
| ( identity = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_75647,c_64184]) ).
tcf(c_81973,plain,
( ( iPr_def_15 = iPr_def_18 )
| ( multiply(iPr_def_27,iPr_def_14) = iPr_def_27 ) ),
inference(superposition,[status(thm)],[c_79384,c_71720]) ).
tcf(c_82083,plain,
( ( iPr_def_15 = iPr_def_18 )
| ( sk_c2 = iPr_def_27 ) ),
inference(light_normalisation,[status(thm)],[c_81973,c_64207]) ).
tcf(c_82487,plain,
( ( iPr_def_15 = iPr_def_18 )
| ( inverse(iPr_def_14) = sk_c3 ) ),
inference(superposition,[status(thm)],[c_79539,c_29404]) ).
tcf(c_82514,plain,
( ( iPr_def_15 = iPr_def_18 )
| ( sk_c10 = sk_c3 ) ),
inference(light_normalisation,[status(thm)],[c_82487,c_64214]) ).
tcf(c_82602,plain,
( ( iPr_def_15 = iPr_def_18 )
| ( inverse(sk_c8) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_79550,c_638]) ).
tcf(c_82727,plain,
( ( iPr_def_15 = iPr_def_18 )
| ( sk_c9 = iPr_def_14 )
| ( inverse(iPr_def_25) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_673,c_82602]) ).
tcf(c_83389,plain,
( ( iPr_def_15 = iPr_def_18 )
| ( inverse(iPr_def_24) = sk_c2 ) ),
inference(superposition,[status(thm)],[c_80285,c_27678]) ).
tcf(c_83401,plain,
( ( iPr_def_15 = iPr_def_18 )
| ( sk_c2 = sk_c3 ) ),
inference(light_normalisation,[status(thm)],[c_83389,c_29404]) ).
tcf(c_83585,plain,
( ( iPr_def_15 = iPr_def_18 )
| ( sk_c9 = iPr_def_14 ) ),
inference(global_subsumption_just,[status(thm)],[c_82727,c_12763,c_27118,c_79539]) ).
tcf(c_83613,plain,
( ( iPr_def_15 = iPr_def_18 )
| ~ iPr_def_11
| ( sk_c8 != identity )
| ( inverse(inverse(iPr_def_14)) != iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_83585,c_3126]) ).
tcf(c_83623,plain,
( ( iPr_def_15 = iPr_def_18 )
| ~ iPr_def_10
| ( identity != iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_83585,c_65637]) ).
tcf(c_83677,plain,
( ( iPr_def_15 = iPr_def_18 )
| ( multiply(iPr_def_14,sk_c8) = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_83585,c_627]) ).
tcf(c_83725,plain,
( ( iPr_def_15 = iPr_def_18 )
| ~ iPr_def_11
| ( sk_c8 != identity ) ),
inference(ground_joinability,[status(thm)],[c_83613,c_64214,c_64334]) ).
tcf(c_84075,plain,
( ( iPr_def_15 = iPr_def_18 )
| ( multiply(iPr_def_14,iPr_def_14) = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_79384,c_83677]) ).
tcf(c_84105,plain,
( ( iPr_def_15 = iPr_def_18 )
| ( sk_c8 = iPr_def_15 ) ),
inference(light_normalisation,[status(thm)],[c_84075,c_64315]) ).
tcf(c_84545,plain,
! [X0: $i] :
( ( iPr_def_15 = iPr_def_18 )
| ( multiply(iPr_def_26,multiply(iPr_def_27,X0)) = X0 ) ),
inference(superposition,[status(thm)],[c_82083,c_3390]) ).
tcf(c_84556,plain,
! [X0: $i] :
( ( iPr_def_15 = iPr_def_18 )
| ( multiply(sk_c10,X0) = X0 ) ),
inference(light_normalisation,[status(thm)],[c_84545,c_7282]) ).
tcf(c_84586,plain,
( ( iPr_def_15 = iPr_def_18 )
| ( multiply(sk_c10,sk_c10) = sk_c10 ) ),
inference(instantiation,[status(thm)],[c_84556]) ).
tcf(c_85526,plain,
! [X0: $i] :
( ( X0 = multiply(sk_c10,sk_c8) )
| ( X0 != iPr_def_14 )
| ( multiply(sk_c10,sk_c8) != iPr_def_14 ) ),
inference(instantiation,[status(thm)],[c_6485]) ).
tcf(c_85527,plain,
( ( sk_c10 = multiply(sk_c10,sk_c8) )
| ( sk_c10 != iPr_def_14 )
| ( multiply(sk_c10,sk_c8) != iPr_def_14 ) ),
inference(instantiation,[status(thm)],[c_85526]) ).
tcf(c_85567,plain,
( ( iPr_def_15 = iPr_def_18 )
| ( sk_c10 = sk_c2 ) ),
inference(superposition,[status(thm)],[c_83401,c_82514]) ).
tcf(c_87116,plain,
( ( iPr_def_15 = iPr_def_18 )
| ( sk_c10 = sk_c8 ) ),
inference(superposition,[status(thm)],[c_85567,c_79550]) ).
tcf(c_87252,plain,
! [X0: $i,X1: $i] :
( ( X1 = multiply(sk_c10,sk_c8) )
| ( X1 != inverse(X0) )
| ( multiply(sk_c10,sk_c8) != inverse(X0) ) ),
inference(instantiation,[status(thm)],[c_6485]) ).
tcf(c_87254,plain,
( ( sk_c10 = multiply(sk_c10,sk_c8) )
| ( sk_c10 != inverse(sk_c10) )
| ( multiply(sk_c10,sk_c8) != inverse(sk_c10) ) ),
inference(instantiation,[status(thm)],[c_87252]) ).
tcf(c_88690,plain,
( ( iPr_def_15 = iPr_def_18 )
| ( sk_c10 = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_87116,c_84105]) ).
tcf(c_93686,plain,
! [X0: $i] :
( ( sk_c2 = inverse(X0) )
| ( sk_c2 != iPr_def_16 )
| ( inverse(X0) != iPr_def_16 ) ),
inference(instantiation,[status(thm)],[c_4800]) ).
tcf(c_93687,plain,
! [X0: $i,X1: $i] :
( ( X0 = sk_c2 )
| ( sk_c2 != inverse(X1) )
| ( X0 != inverse(X1) ) ),
inference(instantiation,[status(thm)],[c_7275]) ).
tcf(c_93688,plain,
( ( sk_c2 = inverse(sk_c10) )
| ( sk_c2 != iPr_def_16 )
| ( inverse(sk_c10) != iPr_def_16 ) ),
inference(instantiation,[status(thm)],[c_93686]) ).
tcf(c_93689,plain,
( ( sk_c10 = sk_c2 )
| ( sk_c2 != inverse(sk_c10) )
| ( sk_c10 != inverse(sk_c10) ) ),
inference(instantiation,[status(thm)],[c_93687]) ).
tcf(c_94423,plain,
! [X0: $i] : multiply(inverse(multiply(X0,sk_c9)),multiply(X0,iPr_def_15)) = sk_c8,
inference(superposition,[status(thm)],[c_627,c_21502]) ).
tcf(c_97627,plain,
! [X0: $i] :
( ( X0 = sk_c2 )
| ( sk_c2 != iPr_def_14 )
| ( X0 != iPr_def_14 ) ),
inference(instantiation,[status(thm)],[c_7275]) ).
tcf(c_97628,plain,
( ( sk_c10 = sk_c2 )
| ( sk_c2 != iPr_def_14 )
| ( sk_c10 != iPr_def_14 ) ),
inference(instantiation,[status(thm)],[c_97627]) ).
tcf(c_98368,plain,
( ( identity = iPr_def_24 )
| ( iPr_def_24 != iPr_def_27 )
| ( identity != iPr_def_27 ) ),
inference(instantiation,[status(thm)],[c_29649]) ).
tcf(c_98647,plain,
( ( identity = iPr_def_16 )
| ( iPr_def_16 != iPr_def_14 )
| ( identity != iPr_def_14 ) ),
inference(instantiation,[status(thm)],[c_30218]) ).
tcf(c_101076,plain,
! [X0: $i] :
( ( multiply(inverse(X0),sk_c9) = sk_c9 )
| ( sk_c9 != multiply(identity,sk_c9) )
| ( multiply(inverse(X0),sk_c9) != multiply(identity,sk_c9) ) ),
inference(instantiation,[status(thm)],[c_1401]) ).
tcf(c_101082,plain,
( ( multiply(inverse(sk_c10),sk_c9) = sk_c9 )
| ( sk_c9 != multiply(identity,sk_c9) )
| ( multiply(inverse(sk_c10),sk_c9) != multiply(identity,sk_c9) ) ),
inference(instantiation,[status(thm)],[c_101076]) ).
tcf(c_101123,plain,
! [X0: $i,X1: $i] :
( ( multiply(inverse(X0),sk_c9) = X1 )
| ( X1 != multiply(sk_c10,sk_c8) )
| ( multiply(inverse(X0),sk_c9) != multiply(sk_c10,sk_c8) ) ),
inference(instantiation,[status(thm)],[c_74406]) ).
tcf(c_101127,plain,
( ( multiply(inverse(sk_c10),sk_c9) = sk_c10 )
| ( sk_c10 != multiply(sk_c10,sk_c8) )
| ( multiply(inverse(sk_c10),sk_c9) != multiply(sk_c10,sk_c8) ) ),
inference(instantiation,[status(thm)],[c_101123]) ).
tcf(c_101262,plain,
! [X0: $i] :
( ( multiply(inverse(X0),sk_c9) = multiply(identity,sk_c9) )
| ( sk_c9 != sk_c9 )
| ( inverse(X0) != identity ) ),
inference(instantiation,[status(thm)],[c_74408]) ).
tcf(c_101263,plain,
! [X0: $i] :
( ( sk_c9 = multiply(inverse(X0),sk_c9) )
| ( sk_c9 != multiply(identity,sk_c9) )
| ( multiply(inverse(X0),sk_c9) != multiply(identity,sk_c9) ) ),
inference(instantiation,[status(thm)],[c_1466]) ).
tcf(c_101264,plain,
( ( multiply(inverse(sk_c10),sk_c9) = multiply(identity,sk_c9) )
| ( sk_c9 != sk_c9 )
| ( inverse(sk_c10) != identity ) ),
inference(instantiation,[status(thm)],[c_101262]) ).
tcf(c_101265,plain,
( ( sk_c9 = multiply(inverse(sk_c10),sk_c9) )
| ( sk_c9 != multiply(identity,sk_c9) )
| ( multiply(inverse(sk_c10),sk_c9) != multiply(identity,sk_c9) ) ),
inference(instantiation,[status(thm)],[c_101263]) ).
tcf(c_101287,plain,
! [X0: $i] :
( ( multiply(inverse(X0),sk_c9) = multiply(identity,identity) )
| ( sk_c9 != identity )
| ( inverse(X0) != identity ) ),
inference(instantiation,[status(thm)],[c_74408]) ).
tcf(c_101292,plain,
( ( multiply(inverse(sk_c10),sk_c9) = multiply(identity,identity) )
| ( sk_c9 != identity )
| ( inverse(sk_c10) != identity ) ),
inference(instantiation,[status(thm)],[c_101287]) ).
tcf(c_101372,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( sk_c10 = multiply(X0,X1) )
| ( sk_c10 != X2 )
| ( multiply(X0,X1) != X2 ) ),
inference(instantiation,[status(thm)],[c_697]) ).
tcf(c_101373,plain,
( ( sk_c10 = multiply(sk_c10,sk_c10) )
| ( sk_c10 != sk_c10 )
| ( multiply(sk_c10,sk_c10) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_101372]) ).
tcf(c_101544,plain,
( ( identity = iPr_def_14 )
| ( iPr_def_14 != iPr_def_24 )
| ( identity != iPr_def_24 ) ),
inference(instantiation,[status(thm)],[c_27119]) ).
tcf(c_103257,plain,
! [X0: $i] :
( ( inverse(X0) = identity )
| ( identity != iPr_def_16 )
| ( inverse(X0) != iPr_def_16 ) ),
inference(instantiation,[status(thm)],[c_4802]) ).
tcf(c_103259,plain,
( ( inverse(sk_c10) = identity )
| ( identity != iPr_def_16 )
| ( inverse(sk_c10) != iPr_def_16 ) ),
inference(instantiation,[status(thm)],[c_103257]) ).
tcf(c_103270,plain,
( ( sk_c9 = identity )
| ( identity != iPr_def_24 )
| ( sk_c9 != iPr_def_24 ) ),
inference(instantiation,[status(thm)],[c_1336]) ).
tcf(c_103271,plain,
( ( sk_c9 = identity )
| ( identity != sk_c9 )
| ( sk_c9 != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_1290]) ).
tcf(c_104625,plain,
multiply(inverse(multiply(inverse(iPr_def_15),sk_c9)),identity) = sk_c8,
inference(superposition,[status(thm)],[c_104,c_94423]) ).
tcf(c_105058,plain,
inverse(multiply(inverse(iPr_def_15),sk_c9)) = sk_c8,
inference(demodulation,[status(thm)],[c_104625,c_22915]) ).
tcf(c_105108,plain,
multiply(sk_c8,multiply(inverse(iPr_def_15),sk_c9)) = identity,
inference(superposition,[status(thm)],[c_105058,c_104]) ).
tcf(c_105111,plain,
multiply(sk_c8,multiply(inverse(iPr_def_15),iPr_def_15)) = sk_c8,
inference(superposition,[status(thm)],[c_105058,c_94423]) ).
tcf(c_105207,plain,
! [X0: $i,X1: $i] :
( ( multiply(inverse(X0),sk_c9) = sk_c10 )
| ( sk_c10 != X1 )
| ( multiply(inverse(X0),sk_c9) != X1 ) ),
inference(instantiation,[status(thm)],[c_697]) ).
tcf(c_105212,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(inverse(X0),sk_c9) = X2 )
| ( X2 != X1 )
| ( multiply(inverse(X0),sk_c9) != X1 ) ),
inference(instantiation,[status(thm)],[c_697]) ).
tcf(c_105213,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(inverse(X0),sk_c9) = sk_c10 )
| ( sk_c10 != multiply(X1,X2) )
| ( multiply(inverse(X0),sk_c9) != multiply(X1,X2) ) ),
inference(instantiation,[status(thm)],[c_105207]) ).
tcf(c_105214,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(inverse(X0),sk_c9) = multiply(X1,X2) )
| ( sk_c9 != X2 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_699]) ).
tcf(c_105217,plain,
! [X0: $i] :
( ( sk_c10 = identity )
| ( identity != X0 )
| ( sk_c10 != X0 ) ),
inference(instantiation,[status(thm)],[c_697]) ).
tcf(c_105218,plain,
! [X0: $i,X1: $i] :
( ( sk_c10 = multiply(inverse(X0),sk_c9) )
| ( sk_c10 != X1 )
| ( multiply(inverse(X0),sk_c9) != X1 ) ),
inference(instantiation,[status(thm)],[c_697]) ).
tcf(c_105219,plain,
( ( sk_c10 = multiply(inverse(sk_c10),sk_c9) )
| ( sk_c10 != sk_c10 )
| ( multiply(inverse(sk_c10),sk_c9) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_105218]) ).
tcf(c_105227,plain,
! [X0: $i] :
( ( multiply(inverse(sk_c9),sk_c9) = X0 )
| ( X0 != identity )
| ( multiply(inverse(sk_c9),sk_c9) != identity ) ),
inference(instantiation,[status(thm)],[c_105212]) ).
tcf(c_105229,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( sk_c10 = multiply(X0,X1) )
| ( sk_c10 != X2 )
| ( multiply(X0,X1) != X2 ) ),
inference(instantiation,[status(thm)],[c_697]) ).
tcf(c_105230,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( multiply(inverse(X0),sk_c9) = X3 )
| ( X3 != multiply(X1,X2) )
| ( multiply(inverse(X0),sk_c9) != multiply(X1,X2) ) ),
inference(instantiation,[status(thm)],[c_105212]) ).
tcf(c_105233,plain,
! [X0: $i,X1: $i] :
( ( identity = X0 )
| ( identity != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_697]) ).
tcf(c_105234,plain,
( ( multiply(inverse(sk_c9),sk_c9) = multiply(identity,identity) )
| ( multiply(identity,identity) != identity )
| ( multiply(inverse(sk_c9),sk_c9) != identity ) ),
inference(instantiation,[status(thm)],[c_105227]) ).
tcf(c_105236,plain,
! [X0: $i] :
( ( multiply(inverse(sk_c9),sk_c9) = multiply(inverse(X0),X0) )
| ( multiply(inverse(sk_c9),sk_c9) != identity )
| ( multiply(inverse(X0),X0) != identity ) ),
inference(instantiation,[status(thm)],[c_105227]) ).
tcf(c_105247,plain,
( ( sk_c10 = multiply(inverse(sk_c9),sk_c9) )
| ( sk_c10 != identity )
| ( multiply(inverse(sk_c9),sk_c9) != identity ) ),
inference(instantiation,[status(thm)],[c_105218]) ).
tcf(c_105249,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( sk_c10 = multiply(inverse(X0),sk_c9) )
| ( sk_c10 != multiply(X1,X2) )
| ( multiply(inverse(X0),sk_c9) != multiply(X1,X2) ) ),
inference(instantiation,[status(thm)],[c_105218]) ).
tcf(c_105256,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = multiply(inverse(X0),sk_c9) )
| ( X2 != X1 )
| ( multiply(inverse(X0),sk_c9) != X1 ) ),
inference(instantiation,[status(thm)],[c_697]) ).
tcf(c_105258,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(X0,X2) = multiply(inverse(X1),sk_c9) )
| ( X2 != sk_c9 )
| ( X0 != inverse(X1) ) ),
inference(instantiation,[status(thm)],[c_699]) ).
tcf(c_105260,plain,
( ( multiply(sk_c10,sk_c10) = multiply(inverse(sk_c10),sk_c9) )
| ( sk_c10 != sk_c9 )
| ( sk_c10 != inverse(sk_c10) ) ),
inference(instantiation,[status(thm)],[c_105258]) ).
tcf(c_105263,plain,
! [X0: $i] :
( ( sk_c10 = multiply(identity,X0) )
| ( sk_c10 != X0 )
| ( multiply(identity,X0) != X0 ) ),
inference(instantiation,[status(thm)],[c_105229]) ).
tcf(c_105264,plain,
( ( sk_c10 = multiply(identity,sk_c10) )
| ( sk_c10 != sk_c10 )
| ( multiply(identity,sk_c10) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_105263]) ).
tcf(c_105270,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( multiply(X0,X1) = X3 )
| ( X3 != X2 )
| ( multiply(X0,X1) != X2 ) ),
inference(instantiation,[status(thm)],[c_697]) ).
tcf(c_105271,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( sk_c10 = multiply(X0,X1) )
| ( sk_c10 != multiply(X2,X3) )
| ( multiply(X0,X1) != multiply(X2,X3) ) ),
inference(instantiation,[status(thm)],[c_105229]) ).
tcf(c_105282,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( X3 = multiply(X0,X1) )
| ( X3 != X2 )
| ( multiply(X0,X1) != X2 ) ),
inference(instantiation,[status(thm)],[c_697]) ).
tcf(c_105283,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( ( multiply(inverse(X0),sk_c9) = multiply(X3,X4) )
| ( multiply(X3,X4) != multiply(X1,X2) )
| ( multiply(inverse(X0),sk_c9) != multiply(X1,X2) ) ),
inference(instantiation,[status(thm)],[c_105230]) ).
tcf(c_105303,plain,
! [X0: $i] :
( ( multiply(inverse(X0),sk_c9) = sk_c10 )
| ( sk_c10 != multiply(inverse(sk_c9),sk_c9) )
| ( multiply(inverse(X0),sk_c9) != multiply(inverse(sk_c9),sk_c9) ) ),
inference(instantiation,[status(thm)],[c_105213]) ).
tcf(c_105304,plain,
( ( multiply(inverse(sk_c10),sk_c9) = sk_c10 )
| ( sk_c10 != multiply(inverse(sk_c9),sk_c9) )
| ( multiply(inverse(sk_c10),sk_c9) != multiply(inverse(sk_c9),sk_c9) ) ),
inference(instantiation,[status(thm)],[c_105303]) ).
tcf(c_105308,plain,
! [X0: $i] :
( ( sk_c10 = multiply(inverse(X0),sk_c9) )
| ( sk_c10 != multiply(inverse(sk_c9),sk_c9) )
| ( multiply(inverse(X0),sk_c9) != multiply(inverse(sk_c9),sk_c9) ) ),
inference(instantiation,[status(thm)],[c_105249]) ).
tcf(c_105309,plain,
( ( sk_c10 = multiply(inverse(sk_c10),sk_c9) )
| ( sk_c10 != multiply(inverse(sk_c9),sk_c9) )
| ( multiply(inverse(sk_c10),sk_c9) != multiply(inverse(sk_c9),sk_c9) ) ),
inference(instantiation,[status(thm)],[c_105308]) ).
tcf(c_105322,plain,
! [X0: $i] :
( ( multiply(inverse(X0),sk_c9) = multiply(sk_c10,sk_c8) )
| ( sk_c9 != sk_c8 )
| ( inverse(X0) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_105214]) ).
tcf(c_105323,plain,
( ( multiply(inverse(sk_c10),sk_c9) = multiply(sk_c10,sk_c8) )
| ( sk_c9 != sk_c8 )
| ( inverse(sk_c10) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_105322]) ).
tcf(c_105324,plain,
! [X0: $i] :
( ( sk_c10 = multiply(inverse(X0),sk_c9) )
| ( sk_c10 != iPr_def_15 )
| ( multiply(inverse(X0),sk_c9) != iPr_def_15 ) ),
inference(instantiation,[status(thm)],[c_105229]) ).
tcf(c_105362,plain,
! [X0: $i,X1: $i] :
( ( multiply(inverse(X0),sk_c9) = multiply(X1,sk_c9) )
| ( sk_c9 != sk_c9 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_105214]) ).
tcf(c_105398,plain,
! [X0: $i] :
( ( X0 = multiply(inverse(sk_c9),sk_c9) )
| ( X0 != identity )
| ( multiply(inverse(sk_c9),sk_c9) != identity ) ),
inference(instantiation,[status(thm)],[c_105256]) ).
tcf(c_105400,plain,
! [X0: $i] :
( ( X0 = multiply(inverse(sk_c9),sk_c9) )
| ( X0 != multiply(identity,identity) )
| ( multiply(inverse(sk_c9),sk_c9) != multiply(identity,identity) ) ),
inference(instantiation,[status(thm)],[c_105256]) ).
tcf(c_105402,plain,
! [X0: $i,X1: $i] :
( ( X1 = multiply(inverse(sk_c9),sk_c9) )
| ( X1 != multiply(inverse(X0),X0) )
| ( multiply(inverse(sk_c9),sk_c9) != multiply(inverse(X0),X0) ) ),
inference(instantiation,[status(thm)],[c_105256]) ).
tcf(c_105423,plain,
! [X0: $i,X1: $i] :
( ( X0 = sk_c9 )
| ( sk_c9 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_697]) ).
tcf(c_105438,plain,
! [X0: $i,X1: $i] :
( ( multiply(identity,X0) = X1 )
| ( X1 != X0 )
| ( multiply(identity,X0) != X0 ) ),
inference(instantiation,[status(thm)],[c_105270]) ).
tcf(c_105443,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_105270]) ).
tcf(c_105444,plain,
! [X0: $i,X1: $i] : multiply(X0,X1) = multiply(X0,X1),
inference(instantiation,[status(thm)],[c_696]) ).
tcf(c_105458,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( sk_c10 = multiply(X0,X1) )
| ( sk_c10 != multiply(identity,X2) )
| ( multiply(X0,X1) != multiply(identity,X2) ) ),
inference(instantiation,[status(thm)],[c_105271]) ).
tcf(c_105459,plain,
( ( sk_c10 = multiply(sk_c10,sk_c10) )
| ( sk_c10 != multiply(identity,sk_c10) )
| ( multiply(sk_c10,sk_c10) != multiply(identity,sk_c10) ) ),
inference(instantiation,[status(thm)],[c_105458]) ).
tcf(c_105461,plain,
! [X0: $i,X1: $i] :
( ( X1 = multiply(identity,X0) )
| ( X1 != X0 )
| ( multiply(identity,X0) != X0 ) ),
inference(instantiation,[status(thm)],[c_105282]) ).
tcf(c_105490,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(inverse(sk_c9),sk_c9) = multiply(X1,X2) )
| ( multiply(X1,X2) != multiply(inverse(X0),X0) )
| ( multiply(inverse(sk_c9),sk_c9) != multiply(inverse(X0),X0) ) ),
inference(instantiation,[status(thm)],[c_105283]) ).
tcf(c_105513,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = inverse(X0) )
| ( X2 != X1 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_697]) ).
tcf(c_105570,plain,
! [X0: $i] :
( ( multiply(inverse(X0),X0) = multiply(inverse(sk_c9),sk_c9) )
| ( multiply(inverse(sk_c9),sk_c9) != identity )
| ( multiply(inverse(X0),X0) != identity ) ),
inference(instantiation,[status(thm)],[c_105398]) ).
tcf(c_105592,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( inverse(X0) = X2 )
| ( X2 != X1 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_697]) ).
tcf(c_105593,plain,
! [X0: $i,X1: $i] :
( ( multiply(inverse(X0),sk_c9) = multiply(inverse(X1),sk_c9) )
| ( sk_c9 != sk_c9 )
| ( inverse(X0) != inverse(X1) ) ),
inference(instantiation,[status(thm)],[c_105362]) ).
tcf(c_105606,plain,
( ( identity = multiply(inverse(sk_c9),sk_c9) )
| ( identity != identity )
| ( multiply(inverse(sk_c9),sk_c9) != identity ) ),
inference(instantiation,[status(thm)],[c_105398]) ).
tcf(c_105647,plain,
! [X0: $i,X1: $i] :
( ( multiply(X0,X1) = multiply(inverse(sk_c9),sk_c9) )
| ( multiply(X0,X1) != multiply(identity,identity) )
| ( multiply(inverse(sk_c9),sk_c9) != multiply(identity,identity) ) ),
inference(instantiation,[status(thm)],[c_105400]) ).
tcf(c_105685,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = multiply(inverse(sk_c9),sk_c9) )
| ( X2 != multiply(X0,X1) )
| ( multiply(inverse(sk_c9),sk_c9) != multiply(X0,X1) ) ),
inference(instantiation,[status(thm)],[c_105256]) ).
tcf(c_105735,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(X1,X2) = multiply(inverse(sk_c9),sk_c9) )
| ( multiply(X1,X2) != multiply(inverse(X0),X0) )
| ( multiply(inverse(sk_c9),sk_c9) != multiply(inverse(X0),X0) ) ),
inference(instantiation,[status(thm)],[c_105402]) ).
tcf(c_105873,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(X0,X1) = multiply(identity,X2) )
| ( X1 != X2 )
| ( X0 != identity ) ),
inference(instantiation,[status(thm)],[c_699]) ).
tcf(c_105874,plain,
( ( multiply(sk_c10,sk_c10) = multiply(identity,sk_c10) )
| ( sk_c10 != identity )
| ( sk_c10 != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_105873]) ).
tcf(c_105944,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(X0,X1) = multiply(identity,X2) )
| ( multiply(identity,X2) != X2 )
| ( multiply(X0,X1) != X2 ) ),
inference(instantiation,[status(thm)],[c_105461]) ).
tcf(c_105992,plain,
! [X0: $i] :
( ( multiply(inverse(sk_c9),sk_c9) = multiply(inverse(sk_c9),sk_c9) )
| ( multiply(inverse(sk_c9),sk_c9) != multiply(inverse(X0),X0) ) ),
inference(instantiation,[status(thm)],[c_105490]) ).
tcf(c_106027,plain,
( ( multiply(sk_c9,sk_c8) = iPr_def_15 )
| ( iPr_def_15 != multiply(sk_c9,sk_c8) )
| ( multiply(sk_c9,sk_c8) != multiply(sk_c9,sk_c8) ) ),
inference(instantiation,[status(thm)],[c_105443]) ).
tcf(c_106411,plain,
! [X0: $i] :
( ( multiply(inverse(sk_c9),sk_c9) = multiply(inverse(X0),iPr_def_14) )
| ( multiply(inverse(sk_c9),sk_c9) != multiply(inverse(sk_c9),sk_c9) )
| ( multiply(inverse(X0),iPr_def_14) != multiply(inverse(sk_c9),sk_c9) ) ),
inference(instantiation,[status(thm)],[c_105490]) ).
tcf(c_106532,plain,
! [X0: $i] :
( ( identity = X0 )
| ( identity != multiply(inverse(sk_c9),sk_c9) )
| ( X0 != multiply(inverse(sk_c9),sk_c9) ) ),
inference(instantiation,[status(thm)],[c_105233]) ).
tcf(c_106533,plain,
( ( identity = sk_c10 )
| ( identity != multiply(inverse(sk_c9),sk_c9) )
| ( sk_c10 != multiply(inverse(sk_c9),sk_c9) ) ),
inference(instantiation,[status(thm)],[c_106532]) ).
tcf(c_106550,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = multiply(inverse(X0),sk_c9) )
| ( X2 != multiply(inverse(X1),sk_c9) )
| ( multiply(inverse(X0),sk_c9) != multiply(inverse(X1),sk_c9) ) ),
inference(instantiation,[status(thm)],[c_105256]) ).
tcf(c_106563,plain,
! [X0: $i] :
( ( multiply(inverse(X0),sk_c9) = multiply(inverse(sk_c9),sk_c9) )
| ( sk_c9 != sk_c9 )
| ( inverse(X0) != inverse(sk_c9) ) ),
inference(instantiation,[status(thm)],[c_105593]) ).
tcf(c_106565,plain,
( ( multiply(inverse(sk_c10),sk_c9) = multiply(inverse(sk_c9),sk_c9) )
| ( sk_c9 != sk_c9 )
| ( inverse(sk_c10) != inverse(sk_c9) ) ),
inference(instantiation,[status(thm)],[c_106563]) ).
tcf(c_107736,plain,
! [X0: $i] :
( ( multiply(sk_c10,sk_c8) = X0 )
| ( X0 != iPr_def_14 )
| ( multiply(sk_c10,sk_c8) != iPr_def_14 ) ),
inference(instantiation,[status(thm)],[c_105270]) ).
tcf(c_107738,plain,
( ( multiply(sk_c10,sk_c8) = sk_c10 )
| ( sk_c10 != iPr_def_14 )
| ( multiply(sk_c10,sk_c8) != iPr_def_14 ) ),
inference(instantiation,[status(thm)],[c_107736]) ).
tcf(c_107742,plain,
multiply(sk_c9,sk_c8) = multiply(sk_c9,sk_c8),
inference(instantiation,[status(thm)],[c_105444]) ).
tcf(c_107749,plain,
! [X0: $i] :
( ( X0 = multiply(sk_c1,sk_c9) )
| ( X0 != iPr_def_18 )
| ( multiply(sk_c1,sk_c9) != iPr_def_18 ) ),
inference(instantiation,[status(thm)],[c_105282]) ).
tcf(c_107750,plain,
! [X0: $i] :
( ( multiply(sk_c1,sk_c9) = X0 )
| ( X0 != iPr_def_18 )
| ( multiply(sk_c1,sk_c9) != iPr_def_18 ) ),
inference(instantiation,[status(thm)],[c_105270]) ).
tcf(c_107751,plain,
( ( sk_c10 = multiply(sk_c1,sk_c9) )
| ( sk_c10 != iPr_def_18 )
| ( multiply(sk_c1,sk_c9) != iPr_def_18 ) ),
inference(instantiation,[status(thm)],[c_105229]) ).
tcf(c_107757,plain,
! [X0: $i] :
( ( X0 = multiply(sk_c4,sk_c7) )
| ( X0 != iPr_def_23 )
| ( multiply(sk_c4,sk_c7) != iPr_def_23 ) ),
inference(instantiation,[status(thm)],[c_105282]) ).
tcf(c_107759,plain,
( ( sk_c10 = multiply(sk_c4,sk_c7) )
| ( sk_c10 != iPr_def_23 )
| ( multiply(sk_c4,sk_c7) != iPr_def_23 ) ),
inference(instantiation,[status(thm)],[c_105229]) ).
tcf(c_108629,plain,
! [X0: $i,X1: $i] :
( ( multiply(X0,X1) = multiply(identity,iPr_def_27) )
| ( multiply(identity,iPr_def_27) != iPr_def_27 )
| ( multiply(X0,X1) != iPr_def_27 ) ),
inference(instantiation,[status(thm)],[c_105944]) ).
tcf(c_108630,plain,
( ( multiply(sk_c10,sk_c10) = multiply(identity,iPr_def_27) )
| ( multiply(identity,iPr_def_27) != iPr_def_27 )
| ( multiply(sk_c10,sk_c10) != iPr_def_27 ) ),
inference(instantiation,[status(thm)],[c_108629]) ).
tcf(c_109097,plain,
! [X0: $i] :
( ( X0 = multiply(sk_c9,sk_c8) )
| ( X0 != iPr_def_15 )
| ( multiply(sk_c9,sk_c8) != iPr_def_15 ) ),
inference(instantiation,[status(thm)],[c_105282]) ).
tcf(c_109098,plain,
! [X0: $i] :
( ( multiply(sk_c9,sk_c8) = X0 )
| ( X0 != iPr_def_15 )
| ( multiply(sk_c9,sk_c8) != iPr_def_15 ) ),
inference(instantiation,[status(thm)],[c_105270]) ).
tcf(c_109099,plain,
( ( sk_c10 = multiply(sk_c9,sk_c8) )
| ( sk_c10 != iPr_def_15 )
| ( multiply(sk_c9,sk_c8) != iPr_def_15 ) ),
inference(instantiation,[status(thm)],[c_105229]) ).
tcf(c_109421,plain,
! [X0: $i,X1: $i] :
( ( multiply(inverse(X0),sk_c9) = multiply(X1,iPr_def_14) )
| ( sk_c9 != iPr_def_14 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_105214]) ).
tcf(c_109427,plain,
! [X0: $i,X1: $i] :
( ( multiply(inverse(X0),sk_c9) = multiply(X1,iPr_def_16) )
| ( sk_c9 != iPr_def_16 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_105214]) ).
tcf(c_109436,plain,
! [X0: $i] :
( ( sk_c10 = sk_c8 )
| ( sk_c8 != X0 )
| ( sk_c10 != X0 ) ),
inference(instantiation,[status(thm)],[c_697]) ).
tcf(c_109447,plain,
sk_c8 = sk_c8,
inference(instantiation,[status(thm)],[c_696]) ).
tcf(c_109448,plain,
! [X0: $i,X1: $i] :
( ( X0 = sk_c8 )
| ( sk_c8 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_697]) ).
tcf(c_109570,plain,
! [X0: $i] :
( ( identity = multiply(inverse(X0),sk_c9) )
| ( identity != multiply(inverse(sk_c9),sk_c9) )
| ( multiply(inverse(X0),sk_c9) != multiply(inverse(sk_c9),sk_c9) ) ),
inference(instantiation,[status(thm)],[c_106550]) ).
tcf(c_109571,plain,
( ( identity = multiply(inverse(sk_c10),sk_c9) )
| ( identity != multiply(inverse(sk_c9),sk_c9) )
| ( multiply(inverse(sk_c10),sk_c9) != multiply(inverse(sk_c9),sk_c9) ) ),
inference(instantiation,[status(thm)],[c_109570]) ).
tcf(c_109670,plain,
! [X0: $i,X1: $i] :
( ( multiply(inverse(sk_c10),sk_c9) = multiply(X0,X1) )
| ( multiply(X0,X1) != multiply(iPr_def_16,iPr_def_16) )
| ( multiply(inverse(sk_c10),sk_c9) != multiply(iPr_def_16,iPr_def_16) ) ),
inference(instantiation,[status(thm)],[c_105283]) ).
tcf(c_110429,plain,
! [X0: $i] :
( ( inverse(X0) = inverse(sk_c9) )
| ( X0 != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_698]) ).
tcf(c_110430,plain,
( ( inverse(sk_c10) = inverse(sk_c9) )
| ( sk_c10 != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_110429]) ).
tcf(c_110437,plain,
( ( multiply(inverse(sk_c9),sk_c9) = multiply(inverse(iPr_def_14),iPr_def_14) )
| ( multiply(inverse(iPr_def_14),iPr_def_14) != multiply(inverse(sk_c9),sk_c9) )
| ( multiply(inverse(sk_c9),sk_c9) != multiply(inverse(sk_c9),sk_c9) ) ),
inference(instantiation,[status(thm)],[c_106411]) ).
tcf(c_110438,plain,
( ( multiply(inverse(iPr_def_14),iPr_def_14) = multiply(inverse(sk_c9),sk_c9) )
| ( multiply(inverse(iPr_def_14),iPr_def_14) != identity )
| ( multiply(inverse(sk_c9),sk_c9) != identity ) ),
inference(instantiation,[status(thm)],[c_105570]) ).
tcf(c_110788,plain,
! [X0: $i] :
( ( multiply(inverse(X0),sk_c9) = multiply(inverse(sk_c9),sk_c9) )
| ( multiply(inverse(sk_c9),sk_c9) != multiply(inverse(iPr_def_14),iPr_def_14) )
| ( multiply(inverse(X0),sk_c9) != multiply(inverse(iPr_def_14),iPr_def_14) ) ),
inference(instantiation,[status(thm)],[c_105735]) ).
tcf(c_110789,plain,
! [X0: $i] :
( ( multiply(inverse(sk_c9),sk_c9) = multiply(inverse(X0),sk_c9) )
| ( multiply(inverse(sk_c9),sk_c9) != multiply(inverse(iPr_def_14),iPr_def_14) )
| ( multiply(inverse(X0),sk_c9) != multiply(inverse(iPr_def_14),iPr_def_14) ) ),
inference(instantiation,[status(thm)],[c_105490]) ).
tcf(c_110791,plain,
( ( multiply(inverse(sk_c9),sk_c9) = multiply(inverse(sk_c10),sk_c9) )
| ( multiply(inverse(sk_c9),sk_c9) != multiply(inverse(iPr_def_14),iPr_def_14) )
| ( multiply(inverse(sk_c10),sk_c9) != multiply(inverse(iPr_def_14),iPr_def_14) ) ),
inference(instantiation,[status(thm)],[c_110789]) ).
tcf(c_110792,plain,
( ( multiply(inverse(sk_c10),sk_c9) = multiply(inverse(sk_c9),sk_c9) )
| ( multiply(inverse(sk_c9),sk_c9) != multiply(inverse(iPr_def_14),iPr_def_14) )
| ( multiply(inverse(sk_c10),sk_c9) != multiply(inverse(iPr_def_14),iPr_def_14) ) ),
inference(instantiation,[status(thm)],[c_110788]) ).
tcf(c_111170,plain,
! [X0: $i] :
( ( sk_c10 = multiply(inverse(X0),sk_c9) )
| ( sk_c10 != multiply(sk_c1,sk_c9) )
| ( multiply(inverse(X0),sk_c9) != multiply(sk_c1,sk_c9) ) ),
inference(instantiation,[status(thm)],[c_105249]) ).
tcf(c_111173,plain,
( ( sk_c10 = multiply(inverse(sk_c10),sk_c9) )
| ( sk_c10 != multiply(sk_c1,sk_c9) )
| ( multiply(inverse(sk_c10),sk_c9) != multiply(sk_c1,sk_c9) ) ),
inference(instantiation,[status(thm)],[c_111170]) ).
tcf(c_112617,plain,
( ( identity = multiply(sk_c4,sk_c7) )
| ( identity != iPr_def_23 )
| ( multiply(sk_c4,sk_c7) != iPr_def_23 ) ),
inference(instantiation,[status(thm)],[c_107757]) ).
tcf(c_112620,plain,
( ( sk_c10 = identity )
| ( identity != multiply(sk_c4,sk_c7) )
| ( sk_c10 != multiply(sk_c4,sk_c7) ) ),
inference(instantiation,[status(thm)],[c_105217]) ).
tcf(c_112987,plain,
! [X0: $i] :
( ( multiply(sk_c9,sk_c8) = multiply(identity,X0) )
| ( multiply(sk_c9,sk_c8) != iPr_def_15 )
| ( multiply(identity,X0) != iPr_def_15 ) ),
inference(instantiation,[status(thm)],[c_109098]) ).
tcf(c_112991,plain,
! [X0: $i] :
( ( sk_c10 = multiply(sk_c9,sk_c8) )
| ( sk_c10 != multiply(identity,X0) )
| ( multiply(sk_c9,sk_c8) != multiply(identity,X0) ) ),
inference(instantiation,[status(thm)],[c_105458]) ).
tcf(c_112992,plain,
( ( multiply(sk_c9,sk_c8) = multiply(identity,sk_c10) )
| ( multiply(identity,sk_c10) != iPr_def_15 )
| ( multiply(sk_c9,sk_c8) != iPr_def_15 ) ),
inference(instantiation,[status(thm)],[c_112987]) ).
tcf(c_112993,plain,
( ( sk_c10 = multiply(sk_c9,sk_c8) )
| ( sk_c10 != multiply(identity,sk_c10) )
| ( multiply(sk_c9,sk_c8) != multiply(identity,sk_c10) ) ),
inference(instantiation,[status(thm)],[c_112991]) ).
tcf(c_113901,plain,
! [X0: $i,X1: $i] :
( ( sk_c8 = X0 )
| ( sk_c8 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_697]) ).
tcf(c_113909,plain,
( ( sk_c10 = sk_c8 )
| ( sk_c8 != multiply(sk_c1,sk_c9) )
| ( sk_c10 != multiply(sk_c1,sk_c9) ) ),
inference(instantiation,[status(thm)],[c_109436]) ).
tcf(c_113910,plain,
( ( sk_c8 = multiply(sk_c1,sk_c9) )
| ( sk_c8 != iPr_def_18 )
| ( multiply(sk_c1,sk_c9) != iPr_def_18 ) ),
inference(instantiation,[status(thm)],[c_107749]) ).
tcf(c_113913,plain,
( ( sk_c10 = sk_c8 )
| ( sk_c8 != multiply(sk_c9,sk_c8) )
| ( sk_c10 != multiply(sk_c9,sk_c8) ) ),
inference(instantiation,[status(thm)],[c_109436]) ).
tcf(c_113914,plain,
( ( sk_c8 = multiply(sk_c9,sk_c8) )
| ( sk_c8 != iPr_def_15 )
| ( multiply(sk_c9,sk_c8) != iPr_def_15 ) ),
inference(instantiation,[status(thm)],[c_109097]) ).
tcf(c_113958,plain,
! [X0: $i,X1: $i] :
( ( multiply(inverse(X0),sk_c9) = multiply(inverse(X1),iPr_def_14) )
| ( sk_c9 != iPr_def_14 )
| ( inverse(X0) != inverse(X1) ) ),
inference(instantiation,[status(thm)],[c_109421]) ).
tcf(c_113997,plain,
! [X0: $i,X1: $i] :
( ( inverse(X0) = sk_c8 )
| ( sk_c8 != X1 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_109448]) ).
tcf(c_114001,plain,
! [X0: $i,X1: $i] :
( ( X1 = inverse(X0) )
| ( X1 != sk_c8 )
| ( inverse(X0) != sk_c8 ) ),
inference(instantiation,[status(thm)],[c_105513]) ).
tcf(c_114002,plain,
! [X0: $i,X1: $i] :
( ( inverse(X0) = X1 )
| ( X1 != sk_c8 )
| ( inverse(X0) != sk_c8 ) ),
inference(instantiation,[status(thm)],[c_105592]) ).
tcf(c_114006,plain,
( ( inverse(sk_c10) = sk_c10 )
| ( sk_c10 != sk_c8 )
| ( inverse(sk_c10) != sk_c8 ) ),
inference(instantiation,[status(thm)],[c_114002]) ).
tcf(c_114007,plain,
( ( sk_c10 = inverse(sk_c10) )
| ( sk_c10 != sk_c8 )
| ( inverse(sk_c10) != sk_c8 ) ),
inference(instantiation,[status(thm)],[c_114001]) ).
tcf(c_114013,plain,
! [X0: $i] :
( ( sk_c9 = sk_c8 )
| ( sk_c8 != X0 )
| ( sk_c9 != X0 ) ),
inference(instantiation,[status(thm)],[c_109448]) ).
tcf(c_114016,plain,
( ( sk_c9 = sk_c8 )
| ( sk_c8 != sk_c10 )
| ( sk_c9 != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_114013]) ).
tcf(c_114055,plain,
! [X0: $i] :
( ( multiply(inverse(X0),sk_c9) = multiply(iPr_def_16,iPr_def_16) )
| ( sk_c9 != iPr_def_16 )
| ( inverse(X0) != iPr_def_16 ) ),
inference(instantiation,[status(thm)],[c_109427]) ).
tcf(c_114062,plain,
( ( multiply(inverse(sk_c10),sk_c9) = multiply(iPr_def_16,iPr_def_16) )
| ( sk_c9 != iPr_def_16 )
| ( inverse(sk_c10) != iPr_def_16 ) ),
inference(instantiation,[status(thm)],[c_114055]) ).
tcf(c_116404,plain,
! [X0: $i,X1: $i] :
( ( X1 = multiply(inverse(sk_c9),sk_c9) )
| ( X1 != multiply(inverse(X0),sk_c9) )
| ( multiply(inverse(sk_c9),sk_c9) != multiply(inverse(X0),sk_c9) ) ),
inference(instantiation,[status(thm)],[c_105685]) ).
tcf(c_116405,plain,
( ( sk_c10 = multiply(inverse(sk_c9),sk_c9) )
| ( sk_c10 != multiply(inverse(sk_c10),sk_c9) )
| ( multiply(inverse(sk_c9),sk_c9) != multiply(inverse(sk_c10),sk_c9) ) ),
inference(instantiation,[status(thm)],[c_116404]) ).
tcf(c_118742,plain,
multiply(inverse(iPr_def_14),iPr_def_14) = identity,
inference(instantiation,[status(thm)],[c_104]) ).
tcf(c_120664,plain,
! [X0: $i,X1: $i] :
( ( sk_c10 = multiply(X0,X1) )
| ( sk_c10 != iPr_def_14 )
| ( multiply(X0,X1) != iPr_def_14 ) ),
inference(instantiation,[status(thm)],[c_105229]) ).
tcf(c_120665,plain,
( ( sk_c10 = multiply(sk_c10,sk_c10) )
| ( sk_c10 != iPr_def_14 )
| ( multiply(sk_c10,sk_c10) != iPr_def_14 ) ),
inference(instantiation,[status(thm)],[c_120664]) ).
tcf(c_120947,plain,
( ( multiply(inverse(sk_c10),sk_c9) = multiply(sk_c1,sk_c9) )
| ( multiply(sk_c1,sk_c9) != multiply(iPr_def_16,iPr_def_16) )
| ( multiply(inverse(sk_c10),sk_c9) != multiply(iPr_def_16,iPr_def_16) ) ),
inference(instantiation,[status(thm)],[c_109670]) ).
tcf(c_120948,plain,
( ( multiply(sk_c1,sk_c9) = multiply(iPr_def_16,iPr_def_16) )
| ( multiply(iPr_def_16,iPr_def_16) != iPr_def_18 )
| ( multiply(sk_c1,sk_c9) != iPr_def_18 ) ),
inference(instantiation,[status(thm)],[c_107750]) ).
tcf(c_121711,plain,
! [X0: $i,X1: $i] :
( ( multiply(inverse(X0),sk_c9) = iPr_def_24 )
| ( iPr_def_24 != X1 )
| ( multiply(inverse(X0),sk_c9) != X1 ) ),
inference(instantiation,[status(thm)],[c_105212]) ).
tcf(c_121794,plain,
! [X0: $i,X1: $i] :
( ( multiply(inverse(X0),sk_c9) = iPr_def_15 )
| ( iPr_def_15 != X1 )
| ( multiply(inverse(X0),sk_c9) != X1 ) ),
inference(instantiation,[status(thm)],[c_105212]) ).
tcf(c_122129,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( sk_c10 = multiply(X0,X1) )
| ( sk_c10 != multiply(inverse(X2),sk_c9) )
| ( multiply(X0,X1) != multiply(inverse(X2),sk_c9) ) ),
inference(instantiation,[status(thm)],[c_105271]) ).
tcf(c_122130,plain,
( ( sk_c10 = multiply(sk_c10,sk_c10) )
| ( sk_c10 != multiply(inverse(sk_c10),sk_c9) )
| ( multiply(sk_c10,sk_c10) != multiply(inverse(sk_c10),sk_c9) ) ),
inference(instantiation,[status(thm)],[c_122129]) ).
tcf(c_122923,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( inverse(X2) = multiply(inverse(X0),sk_c9) )
| ( inverse(X2) != X1 )
| ( multiply(inverse(X0),sk_c9) != X1 ) ),
inference(instantiation,[status(thm)],[c_105256]) ).
tcf(c_122927,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = inverse(X0) )
| ( X2 != multiply(inverse(X1),sk_c9) )
| ( inverse(X0) != multiply(inverse(X1),sk_c9) ) ),
inference(instantiation,[status(thm)],[c_105513]) ).
tcf(c_122933,plain,
( ( sk_c10 = inverse(sk_c10) )
| ( sk_c10 != multiply(inverse(sk_c10),sk_c9) )
| ( inverse(sk_c10) != multiply(inverse(sk_c10),sk_c9) ) ),
inference(instantiation,[status(thm)],[c_122927]) ).
tcf(c_123553,plain,
( ( sk_c9 = sk_c8 )
| ( sk_c8 != iPr_def_14 )
| ( sk_c9 != iPr_def_14 ) ),
inference(instantiation,[status(thm)],[c_114013]) ).
tcf(c_123901,plain,
! [X0: $i] :
( ( inverse(X0) = inverse(iPr_def_14) )
| ( X0 != iPr_def_14 ) ),
inference(instantiation,[status(thm)],[c_698]) ).
tcf(c_123902,plain,
( ( inverse(sk_c10) = inverse(iPr_def_14) )
| ( sk_c10 != iPr_def_14 ) ),
inference(instantiation,[status(thm)],[c_123901]) ).
tcf(c_124018,plain,
! [X0: $i] :
( ( multiply(inverse(X0),sk_c9) = multiply(inverse(sk_c9),sk_c9) )
| ( multiply(inverse(sk_c9),sk_c9) != multiply(identity,identity) )
| ( multiply(inverse(X0),sk_c9) != multiply(identity,identity) ) ),
inference(instantiation,[status(thm)],[c_105647]) ).
tcf(c_124021,plain,
( ( multiply(inverse(sk_c10),sk_c9) = multiply(inverse(sk_c9),sk_c9) )
| ( multiply(inverse(sk_c9),sk_c9) != multiply(identity,identity) )
| ( multiply(inverse(sk_c10),sk_c9) != multiply(identity,identity) ) ),
inference(instantiation,[status(thm)],[c_124018]) ).
tcf(c_124574,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X0 = sk_c9 )
| ( sk_c9 != multiply(X1,X2) )
| ( X0 != multiply(X1,X2) ) ),
inference(instantiation,[status(thm)],[c_105423]) ).
tcf(c_124577,plain,
( ( sk_c10 = sk_c9 )
| ( sk_c9 != multiply(sk_c10,sk_c10) )
| ( sk_c10 != multiply(sk_c10,sk_c10) ) ),
inference(instantiation,[status(thm)],[c_124574]) ).
tcf(c_124807,plain,
! [X0: $i] :
( ( sk_c8 = X0 )
| ( sk_c8 != sk_c8 )
| ( X0 != sk_c8 ) ),
inference(instantiation,[status(thm)],[c_113901]) ).
tcf(c_124808,plain,
( ( sk_c8 = sk_c10 )
| ( sk_c8 != sk_c8 )
| ( sk_c10 != sk_c8 ) ),
inference(instantiation,[status(thm)],[c_124807]) ).
tcf(c_124881,plain,
! [X0: $i,X1: $i] :
( ( identity = X0 )
| ( identity != multiply(inverse(X1),sk_c9) )
| ( X0 != multiply(inverse(X1),sk_c9) ) ),
inference(instantiation,[status(thm)],[c_105233]) ).
tcf(c_124882,plain,
( ( identity = sk_c10 )
| ( identity != multiply(inverse(sk_c10),sk_c9) )
| ( sk_c10 != multiply(inverse(sk_c10),sk_c9) ) ),
inference(instantiation,[status(thm)],[c_124881]) ).
tcf(c_125234,plain,
! [X0: $i] :
( ( multiply(inverse(X0),sk_c9) = multiply(inverse(iPr_def_14),iPr_def_14) )
| ( sk_c9 != iPr_def_14 )
| ( inverse(X0) != inverse(iPr_def_14) ) ),
inference(instantiation,[status(thm)],[c_113958]) ).
tcf(c_125235,plain,
( ( multiply(inverse(sk_c10),sk_c9) = multiply(inverse(iPr_def_14),iPr_def_14) )
| ( sk_c9 != iPr_def_14 )
| ( inverse(sk_c10) != inverse(iPr_def_14) ) ),
inference(instantiation,[status(thm)],[c_125234]) ).
tcf(c_132051,plain,
! [X0: $i,X1: $i] :
( ( inverse(X1) = multiply(inverse(X0),sk_c9) )
| ( inverse(X1) != sk_c9 )
| ( multiply(inverse(X0),sk_c9) != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_122923]) ).
tcf(c_132052,plain,
( ( inverse(sk_c10) = multiply(inverse(sk_c10),sk_c9) )
| ( inverse(sk_c10) != sk_c9 )
| ( multiply(inverse(sk_c10),sk_c9) != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_132051]) ).
tcf(c_134092,plain,
! [X0: $i] :
( ( multiply(sk_c10,sk_c8) = inverse(X0) )
| ( inverse(X0) != iPr_def_14 )
| ( multiply(sk_c10,sk_c8) != iPr_def_14 ) ),
inference(instantiation,[status(thm)],[c_107736]) ).
tcf(c_134095,plain,
( ( multiply(sk_c10,sk_c8) = inverse(sk_c10) )
| ( inverse(sk_c10) != iPr_def_14 )
| ( multiply(sk_c10,sk_c8) != iPr_def_14 ) ),
inference(instantiation,[status(thm)],[c_134092]) ).
tcf(c_134962,plain,
! [X0: $i] :
( ( inverse(X0) = sk_c8 )
| ( sk_c8 != iPr_def_14 )
| ( inverse(X0) != iPr_def_14 ) ),
inference(instantiation,[status(thm)],[c_113997]) ).
tcf(c_134963,plain,
( ( inverse(sk_c10) = sk_c8 )
| ( sk_c8 != iPr_def_14 )
| ( inverse(sk_c10) != iPr_def_14 ) ),
inference(instantiation,[status(thm)],[c_134962]) ).
tcf(c_135245,plain,
! [X0: $i] :
( ( multiply(inverse(X0),sk_c9) = iPr_def_24 )
| ( iPr_def_24 != sk_c9 )
| ( multiply(inverse(X0),sk_c9) != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_121711]) ).
tcf(c_135853,plain,
( ( sk_c10 = multiply(inverse(identity),sk_c9) )
| ( sk_c10 != iPr_def_15 )
| ( multiply(inverse(identity),sk_c9) != iPr_def_15 ) ),
inference(instantiation,[status(thm)],[c_105324]) ).
tcf(c_135859,plain,
! [X0: $i] :
( ( sk_c10 = multiply(inverse(identity),sk_c9) )
| ( sk_c10 != X0 )
| ( multiply(inverse(identity),sk_c9) != X0 ) ),
inference(instantiation,[status(thm)],[c_105218]) ).
tcf(c_135860,plain,
( ( sk_c10 = multiply(inverse(identity),sk_c9) )
| ( sk_c10 != sk_c10 )
| ( multiply(inverse(identity),sk_c9) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_135859]) ).
tcf(c_136411,plain,
! [X0: $i] :
( ( multiply(inverse(identity),sk_c9) = iPr_def_15 )
| ( iPr_def_15 != X0 )
| ( multiply(inverse(identity),sk_c9) != X0 ) ),
inference(instantiation,[status(thm)],[c_121794]) ).
tcf(c_137122,plain,
( ( sk_c9 = iPr_def_14 )
| ( multiply(sk_c8,multiply(inverse(iPr_def_15),iPr_def_15)) = identity ) ),
inference(superposition,[status(thm)],[c_13122,c_105108]) ).
tcf(c_137128,plain,
( ( sk_c10 = iPr_def_18 )
| ( multiply(sk_c8,multiply(inverse(iPr_def_15),iPr_def_15)) = identity ) ),
inference(superposition,[status(thm)],[c_8145,c_105108]) ).
tcf(c_137199,plain,
( ( sk_c8 = identity )
| ( sk_c10 = iPr_def_18 ) ),
inference(light_normalisation,[status(thm)],[c_137128,c_105111]) ).
tcf(c_137205,plain,
( ( sk_c8 = identity )
| ( sk_c9 = iPr_def_14 ) ),
inference(light_normalisation,[status(thm)],[c_137122,c_105111]) ).
tcf(c_137949,plain,
( ( sk_c10 = iPr_def_18 )
| ( multiply(sk_c10,identity) = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_137199,c_626]) ).
tcf(c_138616,plain,
( ( sk_c9 = iPr_def_14 )
| ( multiply(sk_c10,identity) = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_137205,c_626]) ).
tcf(c_139928,plain,
( ( sk_c10 = iPr_def_18 )
| ( sk_c10 = iPr_def_14 ) ),
inference(demodulation,[status(thm)],[c_137949,c_22915]) ).
tcf(c_140016,plain,
( ( sk_c10 = iPr_def_14 )
| ~ iPr_def_12
| ( sk_c10 != iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_139928,c_2967]) ).
tcf(c_144722,plain,
( ( sk_c9 = iPr_def_14 )
| ( sk_c10 = iPr_def_14 ) ),
inference(demodulation,[status(thm)],[c_138616,c_22915]) ).
tcf(c_144816,plain,
( ( iPr_def_14 = iPr_def_24 )
| ( sk_c10 = iPr_def_15 )
| ( sk_c10 = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_144722,c_682]) ).
tcf(c_154046,plain,
( ~ iPr_def_12
| ( inverse(sk_c7) != sk_c10 ) ),
inference(global_subsumption_just,[status(thm)],[c_41015,c_73781]) ).
tcf(c_154052,plain,
( ( sk_c10 = iPr_def_15 )
| ~ iPr_def_12
| ( inverse(iPr_def_22) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_680,c_154046]) ).
tcf(c_154054,plain,
( ( sk_c9 = iPr_def_14 )
| ~ iPr_def_12
| ( inverse(iPr_def_22) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_670,c_154046]) ).
tcf(c_154056,plain,
( ( sk_c10 = iPr_def_28 )
| ~ iPr_def_12
| ( inverse(iPr_def_22) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_660,c_154046]) ).
tcf(c_155627,plain,
( ~ iPr_def_10
| ( sk_c10 != sk_c9 ) ),
inference(global_subsumption_just,[status(thm)],[c_41231,c_700,c_702,c_628,c_1292,c_1291,c_1789,c_1891,c_2697,c_3937,c_29023,c_30223,c_34183,c_47206,c_47602,c_48444,c_64096,c_65637,c_65843,c_66346,c_70019,c_74401,c_105606,c_106565,c_107751,c_107759,c_109571,c_110430,c_111173,c_112617,c_112620,c_114062,c_120947,c_120948,c_124882]) ).
tcf(c_155645,plain,
( ( sk_c10 = iPr_def_26 )
| ~ iPr_def_10
| ( sk_c10 != iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_674,c_155627]) ).
tcf(c_156618,plain,
( ( sk_c10 != iPr_def_14 )
| ~ iPr_def_10 ),
inference(global_subsumption_just,[status(thm)],[c_155645,c_1928,c_65843,c_155627]) ).
tcf(c_156619,plain,
( ~ iPr_def_10
| ( sk_c10 != iPr_def_14 ) ),
inference(renaming,[status(thm)],[c_156618]) ).
tcf(c_166731,plain,
( ( sk_c10 = iPr_def_15 )
| ~ iPr_def_12 ),
inference(global_subsumption_just,[status(thm)],[c_154052,c_157,c_700,c_702,c_628,c_639,c_1291,c_1296,c_1297,c_1653,c_1654,c_1661,c_1662,c_1784,c_1891,c_2115,c_2572,c_2697,c_2967,c_3439,c_3440,c_5066,c_10011,c_10404,c_14880,c_14911,c_15845,c_27118,c_27598,c_27681,c_29023,c_29032,c_32915,c_32912,c_34183,c_64096,c_64200,c_67890,c_71163,c_74046,c_74044,c_74051,c_74163,c_74401,c_93688,c_93689,c_97628,c_98368,c_98647,c_101082,c_101264,c_101292,c_101544,c_103259,c_103271,c_105234,c_105247,c_105264,c_105309,c_105459,c_105874,c_107759,c_108630,c_112617,c_112620,c_122933,c_124021,c_124577,c_132052,c_144816]) ).
tcf(c_167097,plain,
( iPr_def_13
| ( sk_c10 = iPr_def_23 )
| iPr_def_10
| iPr_def_11 ),
inference(global_subsumption_just,[status(thm)],[c_41314,c_157,c_700,c_702,c_628,c_639,c_1291,c_1296,c_1297,c_1653,c_1654,c_1661,c_1662,c_1784,c_1891,c_2115,c_2572,c_2697,c_2967,c_3439,c_3440,c_5066,c_10011,c_10404,c_12644,c_14880,c_14911,c_15845,c_27118,c_27598,c_27681,c_29023,c_29032,c_32915,c_32912,c_34183,c_64096,c_64200,c_64322,c_67890,c_71163,c_74046,c_74044,c_74051,c_74163,c_74401,c_93688,c_93689,c_97628,c_98368,c_98647,c_101082,c_101264,c_101292,c_101544,c_103259,c_103271,c_105234,c_105247,c_105264,c_105309,c_105459,c_105874,c_107759,c_108630,c_112617,c_112620,c_122933,c_124021,c_124577,c_132052,c_144816]) ).
tcf(c_167098,plain,
( iPr_def_13
| iPr_def_11
| iPr_def_10
| ( sk_c10 = iPr_def_23 ) ),
inference(renaming,[status(thm)],[c_167097]) ).
tcf(c_167119,plain,
( ( sk_c9 = iPr_def_14 )
| ~ iPr_def_12 ),
inference(global_subsumption_just,[status(thm)],[c_154054,c_157,c_700,c_702,c_628,c_639,c_1291,c_1296,c_1297,c_1653,c_1654,c_1661,c_1662,c_1784,c_1891,c_2115,c_2572,c_2697,c_2967,c_3439,c_3440,c_5066,c_10011,c_10404,c_14880,c_14911,c_15845,c_27118,c_27598,c_27681,c_29023,c_29032,c_32915,c_32912,c_34183,c_64096,c_64200,c_67890,c_71163,c_74046,c_74044,c_74051,c_74163,c_74401,c_93688,c_93689,c_97628,c_98368,c_98647,c_101082,c_101264,c_101292,c_101544,c_103259,c_103271,c_105234,c_105247,c_105264,c_105309,c_105459,c_105874,c_107759,c_108630,c_112617,c_112620,c_122933,c_124021,c_124577,c_132052,c_144816]) ).
tcf(c_167127,plain,
( ( sk_c10 = iPr_def_28 )
| ~ iPr_def_12 ),
inference(global_subsumption_just,[status(thm)],[c_154056,c_1928,c_2967,c_9065,c_10011,c_32915,c_34183,c_67923,c_67896,c_73161,c_74046,c_74044,c_74167,c_98368,c_107759,c_112617,c_112620,c_140016,c_166731,c_167119]) ).
tcf(c_167129,plain,
~ iPr_def_12,
inference(global_subsumption_just,[status(thm)],[c_167127,c_1928,c_2967,c_9065,c_67923,c_67896,c_73161,c_74046,c_74167,c_98368,c_140016,c_166731,c_167119,c_167127]) ).
tcf(c_170966,plain,
( iPr_def_13
| ( sk_c10 != iPr_def_15 )
| ( sk_c9 != iPr_def_14 )
| iPr_def_10
| iPr_def_11 ),
inference(global_subsumption_just,[status(thm)],[c_64322,c_157,c_700,c_702,c_628,c_639,c_1291,c_1296,c_1297,c_1653,c_1654,c_1661,c_1662,c_1784,c_1891,c_2115,c_2572,c_2697,c_2967,c_3439,c_3440,c_5066,c_10011,c_10404,c_14880,c_14911,c_15845,c_27118,c_27598,c_27681,c_29023,c_29032,c_32915,c_32912,c_34183,c_64096,c_64200,c_64322,c_67890,c_71163,c_74046,c_74044,c_74051,c_74163,c_74401,c_93688,c_93689,c_97628,c_98368,c_98647,c_101082,c_101264,c_101292,c_101544,c_103259,c_103271,c_105234,c_105247,c_105264,c_105309,c_105459,c_105874,c_107759,c_108630,c_112617,c_112620,c_122933,c_124021,c_124577,c_132052,c_144816]) ).
tcf(c_170967,plain,
( iPr_def_13
| iPr_def_11
| iPr_def_10
| ( sk_c9 != iPr_def_14 )
| ( sk_c10 != iPr_def_15 ) ),
inference(renaming,[status(thm)],[c_170966]) ).
tcf(c_170980,plain,
( iPr_def_13
| iPr_def_11
| iPr_def_10
| ( sk_c10 = iPr_def_14 )
| ( sk_c10 != iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_144722,c_170967]) ).
tcf(c_170984,plain,
( iPr_def_13
| iPr_def_11
| iPr_def_10
| ( identity = iPr_def_23 )
| ( sk_c10 != iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_32913,c_170967]) ).
tcf(c_170994,plain,
( iPr_def_13
| iPr_def_11
| iPr_def_10
| ( iPr_def_15 = iPr_def_24 )
| ( sk_c10 != iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_13510,c_170967]) ).
tcf(c_170996,plain,
( iPr_def_13
| iPr_def_11
| iPr_def_10
| ( sk_c9 = iPr_def_14 )
| ( iPr_def_14 != iPr_def_15 )
| ( sk_c10 != iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_13122,c_170967]) ).
tcf(c_171003,plain,
( iPr_def_13
| iPr_def_11
| iPr_def_10
| ( iPr_def_24 = iPr_def_27 )
| ( sk_c10 != iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_1750,c_170967]) ).
tcf(c_173175,plain,
! [X0: $i] :
( ( multiply(identity,X0) = iPr_def_15 )
| ( iPr_def_15 != X0 )
| ( multiply(identity,X0) != X0 ) ),
inference(instantiation,[status(thm)],[c_105438]) ).
tcf(c_173177,plain,
( ( multiply(identity,sk_c10) = iPr_def_15 )
| ( iPr_def_15 != sk_c10 )
| ( multiply(identity,sk_c10) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_173175]) ).
tcf(c_180038,plain,
( ( multiply(inverse(identity),sk_c9) = iPr_def_24 )
| ( iPr_def_24 != sk_c9 )
| ( multiply(inverse(identity),sk_c9) != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_135245]) ).
tcf(c_180039,plain,
( ( multiply(inverse(identity),sk_c9) = iPr_def_15 )
| ( iPr_def_15 != iPr_def_24 )
| ( multiply(inverse(identity),sk_c9) != iPr_def_24 ) ),
inference(instantiation,[status(thm)],[c_136411]) ).
tcf(c_180805,plain,
( ( iPr_def_17 = iPr_def_20 )
| ( sk_c10 = iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_646,c_648]) ).
tcf(c_180846,plain,
inverse(sk_c10) = iPr_def_14,
inference(light_normalisation,[status(thm)],[c_628,c_64096]) ).
tcf(c_180980,plain,
( ( sk_c10 = iPr_def_18 )
| ( multiply(iPr_def_24,sk_c8) = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_652,c_627]) ).
tcf(c_181057,plain,
multiply(iPr_def_14,sk_c10) = identity,
inference(superposition,[status(thm)],[c_180846,c_104]) ).
tcf(c_181058,plain,
multiply(iPr_def_26,sk_c2) = identity,
inference(superposition,[status(thm)],[c_638,c_104]) ).
tcf(c_181059,plain,
multiply(iPr_def_24,sk_c3) = identity,
inference(superposition,[status(thm)],[c_636,c_104]) ).
tcf(c_181060,plain,
multiply(iPr_def_22,sk_c4) = identity,
inference(superposition,[status(thm)],[c_634,c_104]) ).
tcf(c_181063,plain,
multiply(iPr_def_28,sk_c1) = identity,
inference(superposition,[status(thm)],[c_640,c_104]) ).
tcf(c_181069,plain,
( ( sk_c10 = iPr_def_28 )
| ( multiply(sk_c3,iPr_def_24) = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_662,c_637]) ).
tcf(c_181072,plain,
( ( sk_c10 = iPr_def_28 )
| ( multiply(iPr_def_24,sk_c8) = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_662,c_627]) ).
tcf(c_181149,plain,
! [X0: $i,X1: $i] :
( ( inverse(inverse(X0)) = inverse(X1) )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_698]) ).
tcf(c_181150,plain,
( ( inverse(inverse(sk_c10)) = inverse(sk_c10) )
| ( inverse(sk_c10) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_181149]) ).
tcf(c_181170,plain,
! [X0: $i,X1: $i] :
( ( multiply(X0,inverse(X0)) = sk_c10 )
| ( sk_c10 != X1 )
| ( multiply(X0,inverse(X0)) != X1 ) ),
inference(instantiation,[status(thm)],[c_697]) ).
tcf(c_181183,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(X0,inverse(X0)) = sk_c10 )
| ( sk_c10 != multiply(X1,X2) )
| ( multiply(X0,inverse(X0)) != multiply(X1,X2) ) ),
inference(instantiation,[status(thm)],[c_181170]) ).
tcf(c_181184,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(X0,inverse(X0)) = multiply(X2,X1) )
| ( X0 != X2 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_699]) ).
tcf(c_181185,plain,
( ( multiply(sk_c10,inverse(sk_c10)) = sk_c10 )
| ( sk_c10 != multiply(sk_c10,sk_c10) )
| ( multiply(sk_c10,inverse(sk_c10)) != multiply(sk_c10,sk_c10) ) ),
inference(instantiation,[status(thm)],[c_181183]) ).
tcf(c_181186,plain,
( ( multiply(sk_c10,inverse(sk_c10)) = multiply(sk_c10,sk_c10) )
| ( sk_c10 != sk_c10 )
| ( inverse(sk_c10) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_181184]) ).
tcf(c_181265,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(inverse(inverse(X0)),sk_c9) = X2 )
| ( X2 != X1 )
| ( multiply(inverse(inverse(X0)),sk_c9) != X1 ) ),
inference(instantiation,[status(thm)],[c_697]) ).
tcf(c_181267,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(inverse(inverse(X0)),sk_c9) = multiply(X1,X2) )
| ( sk_c9 != X2 )
| ( inverse(inverse(X0)) != X1 ) ),
inference(instantiation,[status(thm)],[c_699]) ).
tcf(c_181327,plain,
! [X0: $i] :
( ( sk_c10 = inverse(identity) )
| ( sk_c10 != X0 )
| ( inverse(identity) != X0 ) ),
inference(instantiation,[status(thm)],[c_697]) ).
tcf(c_181331,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(X0,inverse(X1)) = inverse(X0) )
| ( inverse(X0) != X2 )
| ( multiply(X0,inverse(X1)) != X2 ) ),
inference(instantiation,[status(thm)],[c_697]) ).
tcf(c_181332,plain,
( ( multiply(sk_c10,inverse(sk_c10)) = inverse(sk_c10) )
| ( inverse(sk_c10) != sk_c10 )
| ( multiply(sk_c10,inverse(sk_c10)) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_181331]) ).
tcf(c_181348,plain,
( ( sk_c9 = iPr_def_14 )
| ( multiply(sk_c3,iPr_def_24) = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_672,c_637]) ).
tcf(c_181386,plain,
! [X0: $i,X1: $i] :
( ( multiply(inverse(inverse(X0)),sk_c9) = multiply(X1,sk_c9) )
| ( sk_c9 != sk_c9 )
| ( inverse(inverse(X0)) != X1 ) ),
inference(instantiation,[status(thm)],[c_181267]) ).
tcf(c_181389,plain,
! [X0: $i,X1: $i] :
( ( sk_c9 = X0 )
| ( sk_c9 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_697]) ).
tcf(c_181444,plain,
! [X0: $i,X1: $i] :
( ( inverse(identity) = X1 )
| ( X1 != X0 )
| ( inverse(identity) != X0 ) ),
inference(instantiation,[status(thm)],[c_697]) ).
tcf(c_181445,plain,
! [X0: $i] :
( ( sk_c10 = inverse(identity) )
| ( sk_c10 != inverse(X0) )
| ( inverse(identity) != inverse(X0) ) ),
inference(instantiation,[status(thm)],[c_181327]) ).
tcf(c_181446,plain,
! [X0: $i] :
( ( inverse(identity) = inverse(X0) )
| ( identity != X0 ) ),
inference(instantiation,[status(thm)],[c_698]) ).
tcf(c_181447,plain,
( ( sk_c10 = inverse(identity) )
| ( sk_c10 != inverse(sk_c10) )
| ( inverse(identity) != inverse(sk_c10) ) ),
inference(instantiation,[status(thm)],[c_181445]) ).
tcf(c_181448,plain,
( ( inverse(identity) = inverse(sk_c10) )
| ( identity != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_181446]) ).
tcf(c_181487,plain,
! [X0: $i,X1: $i] :
( ( multiply(inverse(inverse(X0)),sk_c9) = multiply(inverse(X1),sk_c9) )
| ( sk_c9 != sk_c9 )
| ( inverse(inverse(X0)) != inverse(X1) ) ),
inference(instantiation,[status(thm)],[c_181386]) ).
tcf(c_181488,plain,
( ( multiply(inverse(inverse(sk_c10)),sk_c9) = multiply(inverse(sk_c10),sk_c9) )
| ( sk_c9 != sk_c9 )
| ( inverse(inverse(sk_c10)) != inverse(sk_c10) ) ),
inference(instantiation,[status(thm)],[c_181487]) ).
tcf(c_181536,plain,
! [X0: $i] :
( ( sk_c9 = X0 )
| ( sk_c9 != sk_c9 )
| ( X0 != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_181389]) ).
tcf(c_181587,plain,
! [X0: $i,X1: $i] :
( ( multiply(inverse(identity),sk_c9) = X1 )
| ( X1 != X0 )
| ( multiply(inverse(identity),sk_c9) != X0 ) ),
inference(instantiation,[status(thm)],[c_697]) ).
tcf(c_181589,plain,
! [X0: $i,X1: $i] :
( ( multiply(inverse(identity),sk_c9) = multiply(X0,X1) )
| ( sk_c9 != X1 )
| ( inverse(identity) != X0 ) ),
inference(instantiation,[status(thm)],[c_699]) ).
tcf(c_181599,plain,
( ( iPr_def_17 = iPr_def_20 )
| ( sk_c10 = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_678,c_676]) ).
tcf(c_181644,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(inverse(inverse(X0)),sk_c9) = X2 )
| ( X2 != multiply(inverse(X1),sk_c9) )
| ( multiply(inverse(inverse(X0)),sk_c9) != multiply(inverse(X1),sk_c9) ) ),
inference(instantiation,[status(thm)],[c_181265]) ).
tcf(c_181646,plain,
( ( multiply(inverse(inverse(sk_c10)),sk_c9) = sk_c10 )
| ( sk_c10 != multiply(inverse(sk_c10),sk_c9) )
| ( multiply(inverse(inverse(sk_c10)),sk_c9) != multiply(inverse(sk_c10),sk_c9) ) ),
inference(instantiation,[status(thm)],[c_181644]) ).
tcf(c_181661,plain,
( ( sk_c10 = iPr_def_15 )
| ( multiply(sk_c4,iPr_def_22) = iPr_def_23 ) ),
inference(superposition,[status(thm)],[c_680,c_635]) ).
tcf(c_181684,plain,
! [X0: $i,X1: $i] :
( ( inverse(identity) = X1 )
| ( X1 != inverse(X0) )
| ( inverse(identity) != inverse(X0) ) ),
inference(instantiation,[status(thm)],[c_181444]) ).
tcf(c_181685,plain,
( ( inverse(identity) = sk_c10 )
| ( sk_c10 != inverse(sk_c10) )
| ( inverse(identity) != inverse(sk_c10) ) ),
inference(instantiation,[status(thm)],[c_181684]) ).
tcf(c_181704,plain,
( ( sk_c10 = iPr_def_15 )
| ( multiply(iPr_def_23,sk_c8) = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_681,c_626]) ).
tcf(c_181759,plain,
( ( sk_c10 = iPr_def_15 )
| ( multiply(sk_c3,iPr_def_24) = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_682,c_637]) ).
tcf(c_181833,plain,
( ( sk_c10 = iPr_def_15 )
| ( multiply(sk_c2,iPr_def_26) = iPr_def_27 ) ),
inference(superposition,[status(thm)],[c_684,c_639]) ).
tcf(c_181907,plain,
! [X0: $i,X1: $i] :
( ( X0 = sk_c9 )
| ( sk_c9 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_697]) ).
tcf(c_181975,plain,
! [X0: $i] :
( ( sk_c9 = multiply(inverse(inverse(X0)),sk_c9) )
| ( sk_c9 != sk_c9 )
| ( multiply(inverse(inverse(X0)),sk_c9) != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_181536]) ).
tcf(c_181977,plain,
( ( sk_c9 = multiply(inverse(inverse(sk_c10)),sk_c9) )
| ( sk_c9 != sk_c9 )
| ( multiply(inverse(inverse(sk_c10)),sk_c9) != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_181975]) ).
tcf(c_182230,plain,
! [X0: $i] : multiply(sk_c2,multiply(sk_c10,X0)) = multiply(iPr_def_27,X0),
inference(superposition,[status(thm)],[c_639,c_105]) ).
tcf(c_182231,plain,
! [X0: $i] : multiply(sk_c3,multiply(sk_c9,X0)) = multiply(iPr_def_25,X0),
inference(superposition,[status(thm)],[c_637,c_105]) ).
tcf(c_182236,plain,
! [X0: $i] : multiply(sk_c10,multiply(sk_c8,X0)) = multiply(iPr_def_14,X0),
inference(superposition,[status(thm)],[c_626,c_105]) ).
tcf(c_182239,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(X0,X1)) = multiply(identity,X1),
inference(superposition,[status(thm)],[c_104,c_105]) ).
tcf(c_182241,plain,
! [X0: $i] : multiply(iPr_def_26,multiply(sk_c2,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_181058,c_105]) ).
tcf(c_182242,plain,
! [X0: $i] : multiply(iPr_def_24,multiply(sk_c3,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_181059,c_105]) ).
tcf(c_182243,plain,
! [X0: $i] : multiply(iPr_def_22,multiply(sk_c4,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_181060,c_105]) ).
tcf(c_182246,plain,
! [X0: $i] : multiply(iPr_def_28,multiply(sk_c1,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_181063,c_105]) ).
tcf(c_182247,plain,
! [X0: $i] : multiply(iPr_def_14,multiply(sk_c10,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_181057,c_105]) ).
tcf(c_182249,plain,
! [X0: $i] : multiply(iPr_def_14,multiply(sk_c10,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_182247,c_103]) ).
tcf(c_182250,plain,
! [X0: $i] : multiply(iPr_def_28,multiply(sk_c1,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_182246,c_103]) ).
tcf(c_182253,plain,
! [X0: $i] : multiply(iPr_def_22,multiply(sk_c4,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_182243,c_103]) ).
tcf(c_182254,plain,
! [X0: $i] : multiply(iPr_def_24,multiply(sk_c3,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_182242,c_103]) ).
tcf(c_182255,plain,
! [X0: $i] : multiply(iPr_def_26,multiply(sk_c2,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_182241,c_103]) ).
tcf(c_182278,plain,
! [X0: $i] :
( ( inverse(identity) = sk_c9 )
| ( sk_c9 != X0 )
| ( inverse(identity) != X0 ) ),
inference(instantiation,[status(thm)],[c_181444]) ).
tcf(c_182279,plain,
( ( sk_c9 = inverse(identity) )
| ( sk_c9 != sk_c9 )
| ( inverse(identity) != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_181536]) ).
tcf(c_182547,plain,
! [X0: $i] :
( ( multiply(inverse(identity),sk_c9) = sk_c9 )
| ( sk_c9 != X0 )
| ( multiply(inverse(identity),sk_c9) != X0 ) ),
inference(instantiation,[status(thm)],[c_181587]) ).
tcf(c_182554,plain,
! [X0: $i] :
( ( multiply(inverse(identity),sk_c9) = multiply(X0,sk_c9) )
| ( sk_c9 != sk_c9 )
| ( inverse(identity) != X0 ) ),
inference(instantiation,[status(thm)],[c_181589]) ).
tcf(c_182558,plain,
! [X0: $i] :
( ( multiply(inverse(identity),sk_c9) = multiply(X0,iPr_def_27) )
| ( sk_c9 != iPr_def_27 )
| ( inverse(identity) != X0 ) ),
inference(instantiation,[status(thm)],[c_181589]) ).
tcf(c_182559,plain,
( ( multiply(inverse(identity),sk_c9) = multiply(sk_c10,iPr_def_27) )
| ( sk_c9 != iPr_def_27 )
| ( inverse(identity) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_182558]) ).
tcf(c_182675,plain,
! [X0: $i,X1: $i] :
( ( multiply(inverse(inverse(X0)),sk_c9) = sk_c9 )
| ( sk_c9 != multiply(inverse(X1),sk_c9) )
| ( multiply(inverse(inverse(X0)),sk_c9) != multiply(inverse(X1),sk_c9) ) ),
inference(instantiation,[status(thm)],[c_181644]) ).
tcf(c_182677,plain,
( ( multiply(inverse(inverse(sk_c10)),sk_c9) = sk_c9 )
| ( sk_c9 != multiply(inverse(sk_c10),sk_c9) )
| ( multiply(inverse(inverse(sk_c10)),sk_c9) != multiply(inverse(sk_c10),sk_c9) ) ),
inference(instantiation,[status(thm)],[c_182675]) ).
tcf(c_182801,plain,
! [X0: $i] :
( ( inverse(identity) = sk_c9 )
| ( sk_c9 != inverse(X0) )
| ( inverse(identity) != inverse(X0) ) ),
inference(instantiation,[status(thm)],[c_181684]) ).
tcf(c_182802,plain,
( ( inverse(identity) = sk_c9 )
| ( sk_c9 != inverse(sk_c10) )
| ( inverse(identity) != inverse(sk_c10) ) ),
inference(instantiation,[status(thm)],[c_182801]) ).
tcf(c_183320,plain,
( iPr_def_13
| ( iPr_def_15 != sk_c10 )
| ( iPr_def_16 != sk_c9 )
| iPr_def_10
| iPr_def_11 ),
inference(global_subsumption_just,[status(thm)],[c_641,c_157,c_700,c_702,c_628,c_639,c_641,c_1291,c_1296,c_1297,c_1454,c_1529,c_1653,c_1654,c_1661,c_1662,c_1784,c_1891,c_2115,c_2572,c_2697,c_2967,c_3439,c_3440,c_5066,c_10011,c_10404,c_14880,c_14911,c_15845,c_27118,c_27598,c_27681,c_29023,c_29032,c_32915,c_32912,c_34183,c_64096,c_64200,c_67890,c_71163,c_74046,c_74044,c_74051,c_74163,c_74401,c_93688,c_93689,c_97628,c_98368,c_98647,c_101082,c_101264,c_101292,c_101544,c_103259,c_103271,c_105234,c_105247,c_105264,c_105309,c_105459,c_105874,c_107759,c_108630,c_112617,c_112620,c_122933,c_124021,c_124577,c_132052,c_144816]) ).
tcf(c_183321,negated_conjecture,
( iPr_def_13
| iPr_def_11
| iPr_def_10
| ( iPr_def_16 != sk_c9 )
| ( iPr_def_15 != sk_c10 ) ),
inference(renaming,[status(thm)],[c_183320]) ).
tcf(c_183322,plain,
( iPr_def_13
| iPr_def_11
| iPr_def_10
| ( sk_c9 != iPr_def_14 )
| ( sk_c10 != iPr_def_15 ) ),
inference(light_normalisation,[status(thm)],[c_183321,c_64096]) ).
tcf(c_183944,plain,
! [X0: $i] :
( ( sk_c9 = X0 )
| ( sk_c9 != multiply(identity,sk_c9) )
| ( X0 != multiply(identity,sk_c9) ) ),
inference(instantiation,[status(thm)],[c_181389]) ).
tcf(c_184020,plain,
( ( iPr_def_17 = iPr_def_20 )
| ( iPr_def_15 = iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_181599,c_180805]) ).
tcf(c_184785,plain,
multiply(iPr_def_14,iPr_def_14) = sk_c8,
inference(superposition,[status(thm)],[c_626,c_182249]) ).
tcf(c_184955,plain,
! [X0: $i] : multiply(iPr_def_14,multiply(iPr_def_14,X0)) = multiply(sk_c8,X0),
inference(superposition,[status(thm)],[c_184785,c_105]) ).
tcf(c_185129,plain,
multiply(iPr_def_28,iPr_def_18) = sk_c9,
inference(superposition,[status(thm)],[c_630,c_182250]) ).
tcf(c_185214,plain,
multiply(iPr_def_24,iPr_def_25) = sk_c9,
inference(superposition,[status(thm)],[c_637,c_182254]) ).
tcf(c_185721,plain,
! [X0: $i] :
( ( X0 = iPr_def_14 )
| ( X0 != multiply(sk_c10,sk_c8) ) ),
inference(resolution,[status(thm)],[c_697,c_626]) ).
tcf(c_185723,plain,
! [X0: $i] :
( ( X0 = iPr_def_15 )
| ( X0 != multiply(sk_c9,sk_c8) ) ),
inference(resolution,[status(thm)],[c_697,c_627]) ).
tcf(c_185724,plain,
( ( sk_c10 = iPr_def_15 )
| ( sk_c10 != multiply(sk_c9,sk_c8) ) ),
inference(instantiation,[status(thm)],[c_185723]) ).
tcf(c_185784,plain,
! [X0: $i] :
( ( iPr_def_14 = sk_c9 )
| ( X0 = iPr_def_22 )
| ( X0 != sk_c7 ) ),
inference(resolution,[status(thm)],[c_697,c_670]) ).
tcf(c_185792,plain,
! [X0: $i] :
( ( iPr_def_14 = sk_c9 )
| ( X0 = iPr_def_23 )
| ( X0 != sk_c10 ) ),
inference(resolution,[status(thm)],[c_697,c_671]) ).
tcf(c_185797,plain,
( ( iPr_def_14 = sk_c9 )
| ( sk_c10 = iPr_def_23 )
| ( sk_c10 != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_185792]) ).
tcf(c_185854,plain,
multiply(iPr_def_26,iPr_def_27) = sk_c10,
inference(superposition,[status(thm)],[c_639,c_182255]) ).
tcf(c_186138,plain,
( ( sk_c10 = iPr_def_18 )
| ( multiply(iPr_def_24,iPr_def_25) = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_653,c_180980]) ).
tcf(c_186140,plain,
( ( sk_c9 = iPr_def_15 )
| ( sk_c10 = iPr_def_18 ) ),
inference(light_normalisation,[status(thm)],[c_186138,c_185214]) ).
tcf(c_186262,plain,
( ( iPr_def_15 = iPr_def_27 )
| ( sk_c10 = iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_186140,c_655]) ).
tcf(c_186263,plain,
( ( iPr_def_15 = iPr_def_24 )
| ( sk_c10 = iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_186140,c_652]) ).
tcf(c_186731,plain,
iPr_def_15 = iPr_def_18,
inference(global_subsumption_just,[status(thm)],[c_184020,c_700,c_702,c_706,c_628,c_1927,c_2697,c_29032,c_64096,c_64322,c_71552,c_71723,c_74409,c_74410,c_80440,c_80477,c_83585,c_83725,c_83623,c_84586,c_88690,c_101373,c_167129,c_181150,c_181185,c_181186,c_181332]) ).
tcf(c_186734,plain,
( ( iPr_def_15 = iPr_def_24 )
| ( sk_c10 = iPr_def_15 ) ),
inference(demodulation,[status(thm)],[c_186263,c_186731]) ).
tcf(c_186735,plain,
( ( iPr_def_15 = iPr_def_27 )
| ( sk_c10 = iPr_def_15 ) ),
inference(demodulation,[status(thm)],[c_186262,c_186731]) ).
tcf(c_186745,plain,
multiply(iPr_def_28,iPr_def_15) = sk_c9,
inference(demodulation,[status(thm)],[c_185129,c_186731]) ).
tcf(c_186759,plain,
multiply(sk_c1,sk_c9) = iPr_def_15,
inference(demodulation,[status(thm)],[c_630,c_186731]) ).
tcf(c_187483,plain,
( ( sk_c10 = iPr_def_28 )
| ( multiply(iPr_def_24,iPr_def_25) = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_663,c_181072]) ).
tcf(c_187485,plain,
( ( sk_c9 = iPr_def_15 )
| ( sk_c10 = iPr_def_28 ) ),
inference(light_normalisation,[status(thm)],[c_187483,c_185214]) ).
tcf(c_187540,plain,
( ( iPr_def_15 = iPr_def_27 )
| ( sk_c10 = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_187485,c_665]) ).
tcf(c_187541,plain,
( ( iPr_def_15 = iPr_def_24 )
| ( sk_c10 = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_187485,c_662]) ).
tcf(c_187785,plain,
( ( iPr_def_15 = iPr_def_28 )
| ( iPr_def_15 = iPr_def_24 )
| ( sk_c10 = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_186734,c_664]) ).
tcf(c_187849,plain,
( ( iPr_def_15 = iPr_def_27 )
| ( iPr_def_15 = iPr_def_26 )
| ( sk_c10 = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_186735,c_684]) ).
tcf(c_190891,plain,
multiply(sk_c3,iPr_def_15) = multiply(iPr_def_25,sk_c8),
inference(superposition,[status(thm)],[c_627,c_182231]) ).
tcf(c_192315,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(X0,X1)) = X1,
inference(demodulation,[status(thm)],[c_182239,c_103]) ).
tcf(c_192357,plain,
! [X0: $i] : multiply(inverse(inverse(X0)),identity) = X0,
inference(superposition,[status(thm)],[c_104,c_192315]) ).
tcf(c_192466,plain,
! [X0: $i] : multiply(inverse(iPr_def_26),X0) = multiply(sk_c2,X0),
inference(superposition,[status(thm)],[c_182255,c_192315]) ).
tcf(c_192467,plain,
! [X0: $i] : multiply(inverse(iPr_def_24),X0) = multiply(sk_c3,X0),
inference(superposition,[status(thm)],[c_182254,c_192315]) ).
tcf(c_192468,plain,
! [X0: $i] : multiply(inverse(iPr_def_22),X0) = multiply(sk_c4,X0),
inference(superposition,[status(thm)],[c_182253,c_192315]) ).
tcf(c_192471,plain,
! [X0: $i] : multiply(inverse(iPr_def_28),X0) = multiply(sk_c1,X0),
inference(superposition,[status(thm)],[c_182250,c_192315]) ).
tcf(c_192522,plain,
! [X0: $i,X1: $i] : multiply(inverse(inverse(X0)),X1) = multiply(X0,X1),
inference(superposition,[status(thm)],[c_192315,c_192315]) ).
tcf(c_193441,plain,
! [X0: $i] : multiply(X0,identity) = X0,
inference(demodulation,[status(thm)],[c_192357,c_192522]) ).
tcf(c_193480,plain,
! [X0: $i] :
( ( sk_c9 = X0 )
| ( sk_c9 != multiply(inverse(identity),sk_c9) )
| ( X0 != multiply(inverse(identity),sk_c9) ) ),
inference(instantiation,[status(thm)],[c_181389]) ).
tcf(c_193481,plain,
( ( sk_c9 = sk_c10 )
| ( sk_c9 != multiply(inverse(identity),sk_c9) )
| ( sk_c10 != multiply(inverse(identity),sk_c9) ) ),
inference(instantiation,[status(thm)],[c_193480]) ).
tcf(c_193616,plain,
! [X0: $i,X1: $i] :
( ( inverse(identity) = multiply(inverse(inverse(X0)),sk_c9) )
| ( inverse(identity) != X1 )
| ( multiply(inverse(inverse(X0)),sk_c9) != X1 ) ),
inference(instantiation,[status(thm)],[c_181444]) ).
tcf(c_193618,plain,
( ( inverse(identity) = multiply(inverse(inverse(sk_c10)),sk_c9) )
| ( inverse(identity) != sk_c10 )
| ( multiply(inverse(inverse(sk_c10)),sk_c9) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_193616]) ).
tcf(c_193877,plain,
multiply(sk_c8,sk_c10) = multiply(iPr_def_14,identity),
inference(superposition,[status(thm)],[c_181057,c_184955]) ).
tcf(c_193879,plain,
multiply(sk_c8,iPr_def_14) = multiply(iPr_def_14,sk_c8),
inference(superposition,[status(thm)],[c_184785,c_184955]) ).
tcf(c_193950,plain,
( ( sk_c9 = multiply(inverse(identity),sk_c9) )
| ( sk_c9 != multiply(identity,sk_c9) )
| ( multiply(inverse(identity),sk_c9) != multiply(identity,sk_c9) ) ),
inference(instantiation,[status(thm)],[c_183944]) ).
tcf(c_194220,plain,
! [X0: $i] :
( ( X0 = sk_c9 )
| ( sk_c9 != multiply(inverse(identity),sk_c9) )
| ( X0 != multiply(inverse(identity),sk_c9) ) ),
inference(instantiation,[status(thm)],[c_181907]) ).
tcf(c_194221,plain,
( ( sk_c10 = sk_c9 )
| ( sk_c9 != multiply(inverse(identity),sk_c9) )
| ( sk_c10 != multiply(inverse(identity),sk_c9) ) ),
inference(instantiation,[status(thm)],[c_194220]) ).
tcf(c_194226,plain,
! [X0: $i] :
( ( X0 = sk_c9 )
| ( sk_c9 != inverse(identity) )
| ( X0 != inverse(identity) ) ),
inference(instantiation,[status(thm)],[c_181907]) ).
tcf(c_194227,plain,
( ( sk_c10 = sk_c9 )
| ( sk_c9 != inverse(identity) )
| ( sk_c10 != inverse(identity) ) ),
inference(instantiation,[status(thm)],[c_194226]) ).
tcf(c_194390,plain,
multiply(sk_c8,sk_c10) = iPr_def_14,
inference(demodulation,[status(thm)],[c_193877,c_193441]) ).
tcf(c_194394,plain,
( ( sk_c10 = iPr_def_15 )
| ( multiply(iPr_def_25,sk_c10) = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_683,c_194390]) ).
tcf(c_194395,plain,
( ( sk_c9 = iPr_def_14 )
| ( multiply(iPr_def_25,sk_c10) = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_673,c_194390]) ).
tcf(c_194396,plain,
( ( sk_c10 = iPr_def_28 )
| ( multiply(iPr_def_25,sk_c10) = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_663,c_194390]) ).
tcf(c_194425,plain,
multiply(sk_c10,iPr_def_14) = multiply(iPr_def_14,sk_c10),
inference(superposition,[status(thm)],[c_194390,c_182236]) ).
tcf(c_194427,plain,
multiply(sk_c10,iPr_def_14) = identity,
inference(light_normalisation,[status(thm)],[c_194425,c_181057]) ).
tcf(c_194618,plain,
! [X0: $i] : multiply(sk_c10,multiply(iPr_def_14,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_194427,c_105]) ).
tcf(c_194619,plain,
multiply(sk_c2,identity) = multiply(iPr_def_27,iPr_def_14),
inference(superposition,[status(thm)],[c_194427,c_182230]) ).
tcf(c_194622,plain,
! [X0: $i] : multiply(sk_c10,multiply(iPr_def_14,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_194618,c_103]) ).
tcf(c_196129,plain,
! [X0: $i,X1: $i] :
( ( sk_c10 = multiply(X0,iPr_def_27) )
| ( sk_c10 != X1 )
| ( multiply(X0,iPr_def_27) != X1 ) ),
inference(instantiation,[status(thm)],[c_697]) ).
tcf(c_196130,plain,
( ( sk_c10 = multiply(sk_c10,iPr_def_27) )
| ( sk_c10 != sk_c10 )
| ( multiply(sk_c10,iPr_def_27) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_196129]) ).
tcf(c_196707,plain,
multiply(iPr_def_27,iPr_def_14) = sk_c2,
inference(demodulation,[status(thm)],[c_194619,c_193441]) ).
tcf(c_197180,plain,
multiply(sk_c2,iPr_def_26) = identity,
inference(superposition,[status(thm)],[c_192466,c_104]) ).
tcf(c_197199,plain,
( ( identity = iPr_def_27 )
| ( sk_c10 = iPr_def_15 ) ),
inference(demodulation,[status(thm)],[c_181833,c_197180]) ).
tcf(c_197318,plain,
! [X0: $i] :
( ( sk_c10 = iPr_def_15 )
| ( multiply(X0,iPr_def_27) = X0 ) ),
inference(superposition,[status(thm)],[c_197199,c_193441]) ).
tcf(c_197326,plain,
( ( sk_c10 = iPr_def_15 )
| ( multiply(sk_c10,iPr_def_27) = sk_c10 ) ),
inference(instantiation,[status(thm)],[c_197318]) ).
tcf(c_197488,plain,
! [X0: $i,X1: $i] :
( ( multiply(X1,X0) = iPr_def_14 )
| ( X1 != sk_c10 )
| ( X0 != sk_c8 ) ),
inference(resolution,[status(thm)],[c_185721,c_699]) ).
tcf(c_197489,plain,
( ( multiply(sk_c10,sk_c10) = iPr_def_14 )
| ( sk_c10 != sk_c8 )
| ( sk_c10 != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_197488]) ).
tcf(c_197497,plain,
multiply(sk_c3,iPr_def_24) = identity,
inference(superposition,[status(thm)],[c_192467,c_104]) ).
tcf(c_197501,plain,
multiply(sk_c3,identity) = inverse(iPr_def_24),
inference(superposition,[status(thm)],[c_192467,c_193441]) ).
tcf(c_197514,plain,
( ( identity = iPr_def_25 )
| ( sk_c10 = iPr_def_15 ) ),
inference(demodulation,[status(thm)],[c_181759,c_197497]) ).
tcf(c_197515,plain,
( ( identity = iPr_def_25 )
| ( sk_c9 = iPr_def_14 ) ),
inference(demodulation,[status(thm)],[c_181348,c_197497]) ).
tcf(c_197516,plain,
( ( identity = iPr_def_25 )
| ( sk_c10 = iPr_def_28 ) ),
inference(demodulation,[status(thm)],[c_181069,c_197497]) ).
tcf(c_197568,plain,
! [X0: $i] :
( ( sk_c10 = iPr_def_15 )
| ( multiply(iPr_def_25,X0) = X0 ) ),
inference(superposition,[status(thm)],[c_197514,c_103]) ).
tcf(c_197591,plain,
! [X0: $i] :
( ( inverse(identity) = sk_c9 )
| ( sk_c9 != multiply(inverse(inverse(X0)),sk_c9) )
| ( inverse(identity) != multiply(inverse(inverse(X0)),sk_c9) ) ),
inference(instantiation,[status(thm)],[c_182278]) ).
tcf(c_197592,plain,
( ( inverse(identity) = sk_c9 )
| ( sk_c9 != multiply(inverse(inverse(sk_c10)),sk_c9) )
| ( inverse(identity) != multiply(inverse(inverse(sk_c10)),sk_c9) ) ),
inference(instantiation,[status(thm)],[c_197591]) ).
tcf(c_197603,plain,
! [X0: $i] :
( ( sk_c9 = iPr_def_14 )
| ( multiply(iPr_def_25,X0) = X0 ) ),
inference(superposition,[status(thm)],[c_197515,c_103]) ).
tcf(c_197647,plain,
! [X0: $i] :
( ( sk_c10 = iPr_def_28 )
| ( multiply(iPr_def_25,X0) = X0 ) ),
inference(superposition,[status(thm)],[c_197516,c_103]) ).
tcf(c_197681,plain,
inverse(iPr_def_24) = sk_c3,
inference(demodulation,[status(thm)],[c_197501,c_193441]) ).
tcf(c_198096,plain,
multiply(sk_c4,iPr_def_22) = identity,
inference(superposition,[status(thm)],[c_192468,c_104]) ).
tcf(c_198112,plain,
( ( identity = iPr_def_23 )
| ( sk_c10 = iPr_def_15 ) ),
inference(demodulation,[status(thm)],[c_181661,c_198096]) ).
tcf(c_198121,plain,
( iPr_def_13
| ( iPr_def_15 != sk_c10 )
| iPr_def_10
| iPr_def_11 ),
inference(global_subsumption_just,[status(thm)],[c_641,c_157,c_700,c_702,c_627,c_628,c_639,c_695,c_1291,c_1296,c_1297,c_1609,c_1653,c_1654,c_1661,c_1662,c_1784,c_1789,c_1891,c_1993,c_2115,c_2572,c_2697,c_2967,c_3257,c_3439,c_3440,c_3572,c_3937,c_5066,c_10011,c_10404,c_12763,c_14205,c_14880,c_14911,c_15845,c_27118,c_27127,c_27598,c_27681,c_29023,c_29032,c_32915,c_32912,c_34183,c_37980,c_64096,c_64200,c_64322,c_67890,c_71149,c_71163,c_74046,c_74044,c_74051,c_74163,c_74401,c_80439,c_80440,c_93688,c_93689,c_97628,c_98368,c_98647,c_101082,c_101264,c_101265,c_101292,c_101544,c_103259,c_103271,c_103270,c_105234,c_105247,c_105264,c_105309,c_105459,c_105874,c_106027,c_107742,c_107759,c_108630,c_112617,c_112620,c_112992,c_112993,c_122933,c_124021,c_124577,c_132052,c_144816,c_167098,c_171003,c_170984,c_170980,c_170996,c_173177,c_181150,c_181447,c_181448,c_181488,c_181646,c_181685,c_181977,c_182279,c_182677,c_183321,c_185724,c_193618,c_194227,c_197592]) ).
tcf(c_198122,negated_conjecture,
( iPr_def_13
| iPr_def_11
| iPr_def_10
| ( iPr_def_15 != sk_c10 ) ),
inference(renaming,[status(thm)],[c_198121]) ).
tcf(c_198140,plain,
( iPr_def_13
| iPr_def_11
| iPr_def_10
| ( sk_c10 = iPr_def_15 )
| ( iPr_def_15 != iPr_def_23 ) ),
inference(superposition,[status(thm)],[c_681,c_198122]) ).
tcf(c_198319,plain,
( ( iPr_def_23 = iPr_def_27 )
| ( sk_c10 = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_198112,c_197199]) ).
tcf(c_198322,plain,
! [X0: $i] :
( ( sk_c10 = iPr_def_15 )
| ( multiply(iPr_def_23,X0) = X0 ) ),
inference(superposition,[status(thm)],[c_198112,c_103]) ).
tcf(c_199617,plain,
( ( multiply(inverse(identity),sk_c9) = sk_c9 )
| ( sk_c9 != multiply(identity,sk_c9) )
| ( multiply(inverse(identity),sk_c9) != multiply(identity,sk_c9) ) ),
inference(instantiation,[status(thm)],[c_182547]) ).
tcf(c_200440,plain,
( ( multiply(inverse(identity),sk_c9) = multiply(identity,sk_c9) )
| ( sk_c9 != sk_c9 )
| ( inverse(identity) != identity ) ),
inference(instantiation,[status(thm)],[c_182554]) ).
tcf(c_200855,plain,
multiply(sk_c1,identity) = inverse(iPr_def_28),
inference(superposition,[status(thm)],[c_192471,c_193441]) ).
tcf(c_201234,plain,
inverse(iPr_def_28) = sk_c1,
inference(demodulation,[status(thm)],[c_200855,c_193441]) ).
tcf(c_204571,plain,
! [X0: $i,X1: $i] :
( ( multiply(inverse(identity),sk_c9) = X1 )
| ( X1 != multiply(X0,iPr_def_27) )
| ( multiply(inverse(identity),sk_c9) != multiply(X0,iPr_def_27) ) ),
inference(instantiation,[status(thm)],[c_181587]) ).
tcf(c_204572,plain,
( ( multiply(inverse(identity),sk_c9) = sk_c10 )
| ( sk_c10 != multiply(sk_c10,iPr_def_27) )
| ( multiply(inverse(identity),sk_c9) != multiply(sk_c10,iPr_def_27) ) ),
inference(instantiation,[status(thm)],[c_204571]) ).
tcf(c_205420,plain,
( ( sk_c10 = iPr_def_15 )
| ( sk_c10 = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_197568,c_194394]) ).
tcf(c_205570,plain,
( ( sk_c9 = iPr_def_14 )
| ( sk_c10 = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_197603,c_194395]) ).
tcf(c_205734,plain,
( ( sk_c10 = iPr_def_28 )
| ( sk_c10 = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_197647,c_194396]) ).
tcf(c_206395,plain,
iPr_def_14 = sk_c9,
inference(global_subsumption_just,[status(thm)],[c_185784,c_700,c_702,c_626,c_628,c_672,c_675,c_1291,c_1296,c_1297,c_1302,c_1529,c_1789,c_1924,c_1993,c_2697,c_3937,c_13503,c_22944,c_26819,c_29032,c_32911,c_34183,c_64096,c_68132,c_74953,c_75775,c_80439,c_107738,c_107759,c_112617,c_112620,c_135860,c_135853,c_180038,c_180039,c_181448,c_181685,c_182559,c_185797,c_193481,c_193950,c_196130,c_197326,c_199617,c_200440,c_204572,c_205570]) ).
tcf(c_206401,plain,
! [X0: $i] :
( ( X0 = iPr_def_14 )
| ( X0 != sk_c9 ) ),
inference(resolution,[status(thm)],[c_206395,c_697]) ).
tcf(c_206402,plain,
( ( sk_c10 = iPr_def_14 )
| ( sk_c10 != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_206401]) ).
tcf(c_206845,plain,
sk_c9 = iPr_def_14,
inference(global_subsumption_just,[status(thm)],[c_205570,c_1291,c_1424,c_206395]) ).
tcf(c_206902,plain,
multiply(sk_c1,iPr_def_14) = iPr_def_15,
inference(demodulation,[status(thm)],[c_186759,c_206845]) ).
tcf(c_206903,plain,
multiply(iPr_def_28,iPr_def_15) = iPr_def_14,
inference(demodulation,[status(thm)],[c_186745,c_206845]) ).
tcf(c_206907,plain,
( iPr_def_13
| iPr_def_11
| iPr_def_10
| ( iPr_def_14 != iPr_def_14 )
| ( sk_c10 != iPr_def_15 ) ),
inference(demodulation,[status(thm)],[c_183322,c_206845]) ).
tcf(c_206929,plain,
multiply(iPr_def_14,sk_c8) = iPr_def_15,
inference(demodulation,[status(thm)],[c_627,c_206845]) ).
tcf(c_206955,plain,
( iPr_def_13
| iPr_def_11
| iPr_def_10
| ( sk_c10 != iPr_def_15 ) ),
inference(equality_resolution_simp,[status(thm)],[c_206907]) ).
tcf(c_206971,plain,
multiply(sk_c8,iPr_def_14) = iPr_def_15,
inference(demodulation,[status(thm)],[c_193879,c_206929]) ).
tcf(c_207468,plain,
( ( sk_c8 = iPr_def_14 )
| ( sk_c10 = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_198322,c_181704]) ).
tcf(c_207753,plain,
multiply(sk_c10,iPr_def_15) = sk_c8,
inference(superposition,[status(thm)],[c_206929,c_194622]) ).
tcf(c_208034,plain,
( ( iPr_def_15 = iPr_def_24 )
| ( multiply(iPr_def_28,iPr_def_15) = sk_c8 ) ),
inference(superposition,[status(thm)],[c_187541,c_207753]) ).
tcf(c_208037,plain,
( ( iPr_def_15 = iPr_def_27 )
| ( multiply(iPr_def_28,iPr_def_15) = sk_c8 ) ),
inference(superposition,[status(thm)],[c_187540,c_207753]) ).
tcf(c_208085,plain,
( ( iPr_def_15 = iPr_def_27 )
| ( sk_c8 = iPr_def_14 ) ),
inference(light_normalisation,[status(thm)],[c_208037,c_206903]) ).
tcf(c_208088,plain,
( ( iPr_def_15 = iPr_def_24 )
| ( sk_c8 = iPr_def_14 ) ),
inference(light_normalisation,[status(thm)],[c_208034,c_206903]) ).
tcf(c_208229,plain,
iPr_def_15 = iPr_def_24,
inference(global_subsumption_just,[status(thm)],[c_187785,c_700,c_702,c_706,c_626,c_628,c_672,c_675,c_1291,c_1296,c_1297,c_1302,c_1424,c_1529,c_1789,c_1924,c_1993,c_2697,c_3937,c_8379,c_8867,c_13503,c_15044,c_18377,c_22944,c_26819,c_29032,c_29033,c_32911,c_34183,c_45443,c_47206,c_47784,c_52636,c_52650,c_64096,c_68132,c_71162,c_74953,c_75775,c_80439,c_87254,c_101127,c_105323,c_107738,c_107751,c_107759,c_112617,c_112620,c_113909,c_113910,c_114006,c_114007,c_120665,c_123553,c_134095,c_134963,c_135860,c_135853,c_170994,c_180038,c_180039,c_181150,c_181185,c_181186,c_181332,c_181448,c_181685,c_182559,c_185797,c_193481,c_193950,c_196130,c_197326,c_197489,c_199617,c_200440,c_204572,c_205570,c_208088]) ).
tcf(c_208243,plain,
inverse(iPr_def_15) = sk_c3,
inference(demodulation,[status(thm)],[c_197681,c_208229]) ).
tcf(c_208244,plain,
multiply(sk_c3,iPr_def_15) = identity,
inference(demodulation,[status(thm)],[c_197497,c_208229]) ).
tcf(c_208294,plain,
multiply(iPr_def_25,sk_c8) = identity,
inference(demodulation,[status(thm)],[c_190891,c_208244]) ).
tcf(c_208303,plain,
iPr_def_15 = iPr_def_27,
inference(global_subsumption_just,[status(thm)],[c_187849,c_157,c_700,c_702,c_706,c_626,c_628,c_639,c_672,c_675,c_1291,c_1296,c_1297,c_1302,c_1424,c_1529,c_1653,c_1654,c_1661,c_1662,c_1784,c_1789,c_1891,c_1924,c_1993,c_2115,c_2572,c_2697,c_2967,c_3439,c_3440,c_3937,c_5066,c_8378,c_8673,c_10011,c_10404,c_13503,c_13627,c_14880,c_14911,c_15043,c_15845,c_18377,c_22944,c_26819,c_27118,c_27598,c_27681,c_29023,c_29032,c_29033,c_30223,c_32915,c_32912,c_32911,c_34183,c_45443,c_47206,c_47905,c_54208,c_54222,c_64096,c_64200,c_67890,c_68132,c_71162,c_71163,c_74046,c_74044,c_74051,c_74163,c_74401,c_74953,c_75775,c_80439,c_87254,c_93688,c_93689,c_97628,c_98368,c_98647,c_101082,c_101127,c_101264,c_101292,c_101544,c_103259,c_103271,c_105234,c_105247,c_105264,c_105309,c_105323,c_105459,c_105874,c_107738,c_107751,c_107759,c_108630,c_112617,c_112620,c_113909,c_113910,c_114006,c_114007,c_120665,c_122933,c_123553,c_124021,c_124577,c_132052,c_134095,c_134963,c_135860,c_135853,c_144816,c_180038,c_180039,c_181150,c_181185,c_181186,c_181332,c_181448,c_181685,c_182559,c_185797,c_193481,c_193950,c_196130,c_197326,c_197489,c_199617,c_200440,c_204572,c_205570,c_208085]) ).
tcf(c_208317,plain,
( ( iPr_def_15 = iPr_def_23 )
| ( sk_c10 = iPr_def_15 ) ),
inference(demodulation,[status(thm)],[c_198319,c_208303]) ).
tcf(c_208326,plain,
multiply(iPr_def_15,iPr_def_14) = sk_c2,
inference(demodulation,[status(thm)],[c_196707,c_208303]) ).
tcf(c_208358,plain,
multiply(iPr_def_26,iPr_def_15) = sk_c10,
inference(demodulation,[status(thm)],[c_185854,c_208303]) ).
tcf(c_208446,plain,
( ( sk_c10 = iPr_def_28 )
| ( multiply(iPr_def_25,iPr_def_25) = identity ) ),
inference(superposition,[status(thm)],[c_663,c_208294]) ).
tcf(c_208539,plain,
sk_c10 = iPr_def_28,
inference(global_subsumption_just,[status(thm)],[c_208446,c_157,c_104,c_700,c_702,c_706,c_626,c_628,c_639,c_672,c_675,c_1291,c_1296,c_1297,c_1302,c_1424,c_1529,c_1653,c_1654,c_1661,c_1662,c_1784,c_1789,c_1891,c_1924,c_1928,c_1993,c_2115,c_2572,c_2697,c_2967,c_3125,c_3439,c_3440,c_3937,c_5066,c_10011,c_10404,c_10846,c_13503,c_14880,c_14911,c_15845,c_22944,c_26819,c_27118,c_27598,c_27681,c_29023,c_29032,c_32915,c_32912,c_32911,c_34183,c_64096,c_64200,c_64322,c_65992,c_67890,c_68132,c_69638,c_71162,c_71163,c_74046,c_74044,c_74051,c_74163,c_74401,c_74953,c_75775,c_80439,c_80440,c_85527,c_93688,c_93689,c_97628,c_98368,c_98647,c_101082,c_101127,c_101264,c_101292,c_101544,c_103259,c_103271,c_105219,c_105234,c_105236,c_105247,c_105260,c_105264,c_105304,c_105309,c_105323,c_105459,c_105606,c_105874,c_105992,c_106533,c_107738,c_107759,c_108630,c_110437,c_110438,c_110791,c_110792,c_112617,c_112620,c_116405,c_118742,c_122130,c_122933,c_123553,c_123902,c_124021,c_124577,c_125235,c_132052,c_135860,c_135853,c_144816,c_156619,c_180038,c_180039,c_181150,c_181185,c_181186,c_181332,c_181448,c_181685,c_182559,c_182802,c_185797,c_193481,c_193950,c_196130,c_197326,c_198140,c_199617,c_200440,c_204572,c_205570,c_205734,c_206955,c_207468,c_208317]) ).
tcf(c_208689,plain,
inverse(iPr_def_28) = iPr_def_14,
inference(demodulation,[status(thm)],[c_180846,c_208539]) ).
tcf(c_208850,plain,
sk_c1 = iPr_def_14,
inference(demodulation,[status(thm)],[c_201234,c_208689]) ).
tcf(c_208851,plain,
multiply(iPr_def_14,iPr_def_14) = iPr_def_15,
inference(demodulation,[status(thm)],[c_206902,c_208850]) ).
tcf(c_208879,plain,
sk_c8 = iPr_def_15,
inference(demodulation,[status(thm)],[c_184785,c_208851]) ).
tcf(c_208881,plain,
multiply(iPr_def_15,iPr_def_14) = iPr_def_15,
inference(demodulation,[status(thm)],[c_206971,c_208879]) ).
tcf(c_208900,plain,
sk_c2 = iPr_def_15,
inference(demodulation,[status(thm)],[c_208326,c_208881]) ).
tcf(c_208906,plain,
inverse(iPr_def_15) = iPr_def_26,
inference(demodulation,[status(thm)],[c_638,c_208900]) ).
tcf(c_208907,plain,
sk_c3 = iPr_def_26,
inference(demodulation,[status(thm)],[c_208243,c_208906]) ).
tcf(c_208909,plain,
multiply(iPr_def_26,iPr_def_15) = identity,
inference(demodulation,[status(thm)],[c_208244,c_208907]) ).
tcf(c_208912,plain,
identity = iPr_def_28,
inference(light_normalisation,[status(thm)],[c_208909,c_208358,c_208539]) ).
tcf(c_208922,plain,
! [X0: $i] : multiply(iPr_def_28,X0) = X0,
inference(demodulation,[status(thm)],[c_103,c_208912]) ).
tcf(c_208923,plain,
iPr_def_14 = iPr_def_15,
inference(demodulation,[status(thm)],[c_206903,c_208922]) ).
tcf(c_208926,plain,
iPr_def_14 = iPr_def_24,
inference(demodulation,[status(thm)],[c_208229,c_208923]) ).
tcf(c_208984,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_208879,c_208926,c_208317,c_208229,c_207468,c_206402,c_206395,c_205420,c_200440,c_199617,c_198140,c_194221,c_193950,c_182802,c_181448,c_181332,c_181186,c_181185,c_181150,c_180039,c_180038,c_167129,c_156619,c_135853,c_125235,c_124808,c_123902,c_123553,c_122130,c_118742,c_116405,c_114016,c_113914,c_113913,c_110791,c_110438,c_110437,c_109447,c_109099,c_107742,c_106533,c_106027,c_105992,c_105606,c_105323,c_105260,c_105236,c_105219,c_101127,c_85527,c_80440,c_80439,c_74401,c_71162,c_64322,c_64096,c_29657,c_29032,c_27116,c_26819,c_22944,c_3125,c_2697,c_1928,c_1927,c_1789,c_1662,c_1424,c_1297,c_1296,c_1291,c_628,c_627,c_706,c_702,c_700,c_104]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : GRP386-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.07 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.15/5.43 % Computer : n026.cluster.edu
% 0.15/5.43 % Model : x86_64 x86_64
% 0.15/5.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/5.43 % Memory : 8046.5625MB
% 0.15/5.43 % OS : Linux 6.8.0-71-generic
% 0.15/5.43 % CPULimit : 300
% 0.15/5.43 % WCLimit : 300
% 0.15/5.43 % DateTime : Wed Sep 23 14:41:14 UTC 2026
% 0.15/5.43 % CPUTime :
% 0.15/5.43 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.15/5.49 Running first-order theorem proving
% 0.15/5.49 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.20/5.51
% 0.20/5.51 % ======== iProver multi-core TPTP/SMT =========
% 0.20/5.51
% 0.20/5.51 % Detected problem language: tptp
% 0.20/5.53 % Proving...
% 72.69/18.68 % SZS status Started for theBenchmark.p
% 72.69/18.68 % SZS status Unsatisfiable for theBenchmark.p
% 72.69/18.68
% 72.69/18.68 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 72.69/18.68
% 72.69/18.68 % ------ iProver source info
% 72.69/18.68
% 72.69/18.68 % git: date: 2026-07-19 20:42:38 +0200
% 72.69/18.68 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 72.69/18.68 % git: non_committed_changes: false
% 72.69/18.68
% 72.69/18.68 % ------ Parsing...% successful
% 72.69/18.68
% 72.69/18.68
% 72.69/18.68 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 72.69/18.68
% 72.69/18.68 % ------ Preprocessing... sup_sim: 0 sf_s rm: 0 0s sf_e pe_s pe_e %
% 72.69/18.68
% 72.69/18.68 % ------ Preprocessing... gs_s sp: 4 0s gs_e snvd_s sp: 0 0s snvd_e %
% 72.69/18.68
% 72.69/18.68 % ------ Preprocessing... sf_s rm: 0 0s sf_e
% 72.69/18.68 % ------ Proving...
% 72.69/18.68 % ------ Problem Properties
% 72.69/18.68
% 72.69/18.68 %
% 72.69/18.68 % clauses 73
% 72.69/18.68 % conjectures 55
% 72.69/18.68 % EPR 51
% 72.69/18.68 % Horn 22
% 72.69/18.68 % unary 18
% 72.69/18.68 % binary 50
% 72.69/18.68 % lits 139
% 72.69/18.68 % lits eq 131
% 72.69/18.68 % fd_pure 0
% 72.69/18.68 % fd_pseudo 0
% 72.69/18.68 % fd_cond 0
% 72.69/18.68 % fd_pseudo_cond 0
% 72.69/18.68 % AC symbols 0
% 72.69/18.68
% 72.69/18.68 % ------ Schedule dynamic 5 is on
% 72.69/18.68
% 72.69/18.68 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 72.69/18.68
% 72.69/18.68
% 72.69/18.68 % ------
% 72.69/18.68 % Current options:
% 72.69/18.68 % ------
% 72.69/18.68
% 72.69/18.68
% 72.69/18.68 %
% 72.69/18.68
% 72.69/18.68 % ------ Proving...
% 72.69/18.68 % Proof_search_loop: time out after: 7517 full_loop iterations
% 72.69/18.68
% 72.69/18.68 % ------ Input Options"1. --res_lit_sel adaptive --res_lit_sel_side num_symb" Time Limit: 15.
% 72.69/18.68
% 72.69/18.68
% 72.69/18.68 % ------
% 72.69/18.68 % Current options:
% 72.69/18.68 % ------
% 72.69/18.68
% 72.69/18.68
% 72.69/18.68 %
% 72.69/18.68
% 72.69/18.68 % ------ Proving...
% 72.69/18.68 %
% 72.69/18.68
% 72.69/18.68 % SZS status Unsatisfiable for theBenchmark.p
% 72.69/18.68
% 72.69/18.68 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 93.44/18.72
% 93.44/18.72
%------------------------------------------------------------------------------