%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : GRP221-1 : TPTP v9.3.1. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% Computer : n019.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:31:51 PM UTC 2026
% Result : Unsatisfiable 38.14s 7.95s
% Output : CNFRefutation 38.14s
% Verified :
% SZS Type : Refutation
% Derivation depth : 49
% Number of leaves : 66
% Syntax : Number of formulae : 1118 ( 191 unt; 14 def)
% Number of atoms : 4612 (2500 equ)
% Maximal formula atoms : 14 ( 4 avg)
% Number of connectives : 2557 (1043 ~;1514 |; 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 : 19 ( 17 usr; 18 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 11 con; 0-2 aty)
% Number of variables : 526 ( 0 sgn 526 !; 0 ?; 486 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0] : multiply(identity,X0) = X0,
file('/export/starexec/sandbox2/benchmark/Axioms/GRP004-0.ax',left_identity) ).
fof(f2,axiom,
! [X0] : multiply(inverse(X0),X0) = identity,
file('/export/starexec/sandbox2/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/sandbox2/benchmark/Axioms/GRP004-0.ax',associativity) ).
fof(f5,negated_conjecture,
( inverse(sk_c10) = sk_c9
| inverse(sk_c1) = sk_c10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_1) ).
fof(f6,negated_conjecture,
( inverse(sk_c6) = sk_c10
| inverse(sk_c1) = sk_c10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_2) ).
fof(f7,plain,
( sk_c10 = inverse(sk_c6)
| inverse(sk_c1) = sk_c10 ),
inference(reorient_equations,[],[f6]) ).
fof(f8,negated_conjecture,
( multiply(sk_c6,sk_c9) = sk_c10
| inverse(sk_c1) = sk_c10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_3) ).
fof(f9,plain,
( sk_c10 = multiply(sk_c6,sk_c9)
| inverse(sk_c1) = sk_c10 ),
inference(reorient_equations,[],[f8]) ).
fof(f10,negated_conjecture,
( multiply(sk_c10,sk_c8) = sk_c9
| inverse(sk_c1) = sk_c10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_4) ).
fof(f11,plain,
( sk_c9 = multiply(sk_c10,sk_c8)
| inverse(sk_c1) = sk_c10 ),
inference(reorient_equations,[],[f10]) ).
fof(f12,negated_conjecture,
( multiply(sk_c7,sk_c10) = sk_c8
| inverse(sk_c1) = sk_c10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_5) ).
fof(f13,plain,
( sk_c8 = multiply(sk_c7,sk_c10)
| inverse(sk_c1) = sk_c10 ),
inference(reorient_equations,[],[f12]) ).
fof(f14,negated_conjecture,
( inverse(sk_c7) = sk_c10
| inverse(sk_c1) = sk_c10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_6) ).
fof(f15,plain,
( sk_c10 = inverse(sk_c7)
| inverse(sk_c1) = sk_c10 ),
inference(reorient_equations,[],[f14]) ).
fof(f16,negated_conjecture,
( inverse(sk_c10) = sk_c9
| multiply(sk_c1,sk_c9) = sk_c10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_7) ).
fof(f17,plain,
( inverse(sk_c10) = sk_c9
| sk_c10 = multiply(sk_c1,sk_c9) ),
inference(reorient_equations,[],[f16]) ).
fof(f18,negated_conjecture,
( inverse(sk_c6) = sk_c10
| multiply(sk_c1,sk_c9) = sk_c10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_8) ).
fof(f19,plain,
( sk_c10 = inverse(sk_c6)
| sk_c10 = multiply(sk_c1,sk_c9) ),
inference(reorient_equations,[],[f18]) ).
fof(f20,negated_conjecture,
( multiply(sk_c6,sk_c9) = sk_c10
| multiply(sk_c1,sk_c9) = sk_c10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_9) ).
fof(f21,plain,
( sk_c10 = multiply(sk_c6,sk_c9)
| sk_c10 = multiply(sk_c1,sk_c9) ),
inference(reorient_equations,[],[f20]) ).
fof(f22,negated_conjecture,
( multiply(sk_c10,sk_c8) = sk_c9
| multiply(sk_c1,sk_c9) = sk_c10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_10) ).
fof(f23,plain,
( sk_c9 = multiply(sk_c10,sk_c8)
| sk_c10 = multiply(sk_c1,sk_c9) ),
inference(reorient_equations,[],[f22]) ).
fof(f24,negated_conjecture,
( multiply(sk_c7,sk_c10) = sk_c8
| multiply(sk_c1,sk_c9) = sk_c10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_11) ).
fof(f25,plain,
( sk_c8 = multiply(sk_c7,sk_c10)
| sk_c10 = multiply(sk_c1,sk_c9) ),
inference(reorient_equations,[],[f24]) ).
fof(f26,negated_conjecture,
( inverse(sk_c7) = sk_c10
| multiply(sk_c1,sk_c9) = sk_c10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_12) ).
fof(f27,plain,
( sk_c10 = inverse(sk_c7)
| sk_c10 = multiply(sk_c1,sk_c9) ),
inference(reorient_equations,[],[f26]) ).
fof(f28,negated_conjecture,
( inverse(sk_c10) = sk_c9
| multiply(sk_c2,sk_c3) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_13) ).
fof(f29,plain,
( inverse(sk_c10) = sk_c9
| sk_c9 = multiply(sk_c2,sk_c3) ),
inference(reorient_equations,[],[f28]) ).
fof(f30,negated_conjecture,
( inverse(sk_c6) = sk_c10
| multiply(sk_c2,sk_c3) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_14) ).
fof(f31,plain,
( sk_c10 = inverse(sk_c6)
| sk_c9 = multiply(sk_c2,sk_c3) ),
inference(reorient_equations,[],[f30]) ).
fof(f32,negated_conjecture,
( multiply(sk_c6,sk_c9) = sk_c10
| multiply(sk_c2,sk_c3) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_15) ).
fof(f33,plain,
( sk_c10 = multiply(sk_c6,sk_c9)
| sk_c9 = multiply(sk_c2,sk_c3) ),
inference(reorient_equations,[],[f32]) ).
fof(f34,negated_conjecture,
( multiply(sk_c10,sk_c8) = sk_c9
| multiply(sk_c2,sk_c3) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_16) ).
fof(f35,plain,
( sk_c9 = multiply(sk_c10,sk_c8)
| sk_c9 = multiply(sk_c2,sk_c3) ),
inference(reorient_equations,[],[f34]) ).
fof(f36,negated_conjecture,
( multiply(sk_c7,sk_c10) = sk_c8
| multiply(sk_c2,sk_c3) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_17) ).
fof(f37,plain,
( sk_c8 = multiply(sk_c7,sk_c10)
| sk_c9 = multiply(sk_c2,sk_c3) ),
inference(reorient_equations,[],[f36]) ).
fof(f38,negated_conjecture,
( inverse(sk_c7) = sk_c10
| multiply(sk_c2,sk_c3) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_18) ).
fof(f39,plain,
( sk_c10 = inverse(sk_c7)
| sk_c9 = multiply(sk_c2,sk_c3) ),
inference(reorient_equations,[],[f38]) ).
fof(f40,negated_conjecture,
( inverse(sk_c10) = sk_c9
| inverse(sk_c2) = sk_c3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_19) ).
fof(f41,plain,
( inverse(sk_c10) = sk_c9
| sk_c3 = inverse(sk_c2) ),
inference(reorient_equations,[],[f40]) ).
fof(f42,negated_conjecture,
( inverse(sk_c6) = sk_c10
| inverse(sk_c2) = sk_c3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_20) ).
fof(f43,plain,
( sk_c10 = inverse(sk_c6)
| sk_c3 = inverse(sk_c2) ),
inference(reorient_equations,[],[f42]) ).
fof(f44,negated_conjecture,
( multiply(sk_c6,sk_c9) = sk_c10
| inverse(sk_c2) = sk_c3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_21) ).
fof(f45,plain,
( sk_c10 = multiply(sk_c6,sk_c9)
| sk_c3 = inverse(sk_c2) ),
inference(reorient_equations,[],[f44]) ).
fof(f46,negated_conjecture,
( multiply(sk_c10,sk_c8) = sk_c9
| inverse(sk_c2) = sk_c3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_22) ).
fof(f47,plain,
( sk_c9 = multiply(sk_c10,sk_c8)
| sk_c3 = inverse(sk_c2) ),
inference(reorient_equations,[],[f46]) ).
fof(f48,negated_conjecture,
( multiply(sk_c7,sk_c10) = sk_c8
| inverse(sk_c2) = sk_c3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_23) ).
fof(f49,plain,
( sk_c8 = multiply(sk_c7,sk_c10)
| sk_c3 = inverse(sk_c2) ),
inference(reorient_equations,[],[f48]) ).
fof(f50,negated_conjecture,
( inverse(sk_c7) = sk_c10
| inverse(sk_c2) = sk_c3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_24) ).
fof(f51,plain,
( sk_c10 = inverse(sk_c7)
| sk_c3 = inverse(sk_c2) ),
inference(reorient_equations,[],[f50]) ).
fof(f54,negated_conjecture,
( inverse(sk_c6) = sk_c10
| multiply(sk_c3,sk_c10) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_26) ).
fof(f55,plain,
( sk_c10 = inverse(sk_c6)
| sk_c9 = multiply(sk_c3,sk_c10) ),
inference(reorient_equations,[],[f54]) ).
fof(f62,negated_conjecture,
( inverse(sk_c7) = sk_c10
| multiply(sk_c3,sk_c10) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_30) ).
fof(f63,plain,
( sk_c10 = inverse(sk_c7)
| sk_c9 = multiply(sk_c3,sk_c10) ),
inference(reorient_equations,[],[f62]) ).
fof(f64,negated_conjecture,
( inverse(sk_c10) = sk_c9
| multiply(sk_c10,sk_c5) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_31) ).
fof(f65,plain,
( inverse(sk_c10) = sk_c9
| sk_c9 = multiply(sk_c10,sk_c5) ),
inference(reorient_equations,[],[f64]) ).
fof(f66,negated_conjecture,
( inverse(sk_c6) = sk_c10
| multiply(sk_c10,sk_c5) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_32) ).
fof(f67,plain,
( sk_c10 = inverse(sk_c6)
| sk_c9 = multiply(sk_c10,sk_c5) ),
inference(reorient_equations,[],[f66]) ).
fof(f68,negated_conjecture,
( multiply(sk_c6,sk_c9) = sk_c10
| multiply(sk_c10,sk_c5) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_33) ).
fof(f69,plain,
( sk_c10 = multiply(sk_c6,sk_c9)
| sk_c9 = multiply(sk_c10,sk_c5) ),
inference(reorient_equations,[],[f68]) ).
fof(f70,negated_conjecture,
( multiply(sk_c10,sk_c8) = sk_c9
| multiply(sk_c10,sk_c5) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_34) ).
fof(f71,plain,
( sk_c9 = multiply(sk_c10,sk_c8)
| sk_c9 = multiply(sk_c10,sk_c5) ),
inference(reorient_equations,[],[f70]) ).
fof(f72,negated_conjecture,
( multiply(sk_c7,sk_c10) = sk_c8
| multiply(sk_c10,sk_c5) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_35) ).
fof(f73,plain,
( sk_c8 = multiply(sk_c7,sk_c10)
| sk_c9 = multiply(sk_c10,sk_c5) ),
inference(reorient_equations,[],[f72]) ).
fof(f74,negated_conjecture,
( inverse(sk_c7) = sk_c10
| multiply(sk_c10,sk_c5) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_36) ).
fof(f75,plain,
( sk_c10 = inverse(sk_c7)
| sk_c9 = multiply(sk_c10,sk_c5) ),
inference(reorient_equations,[],[f74]) ).
fof(f76,negated_conjecture,
( inverse(sk_c10) = sk_c9
| multiply(sk_c4,sk_c10) = sk_c5 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_37) ).
fof(f77,plain,
( inverse(sk_c10) = sk_c9
| sk_c5 = multiply(sk_c4,sk_c10) ),
inference(reorient_equations,[],[f76]) ).
fof(f78,negated_conjecture,
( inverse(sk_c6) = sk_c10
| multiply(sk_c4,sk_c10) = sk_c5 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_38) ).
fof(f79,plain,
( sk_c10 = inverse(sk_c6)
| sk_c5 = multiply(sk_c4,sk_c10) ),
inference(reorient_equations,[],[f78]) ).
fof(f80,negated_conjecture,
( multiply(sk_c6,sk_c9) = sk_c10
| multiply(sk_c4,sk_c10) = sk_c5 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_39) ).
fof(f81,plain,
( sk_c10 = multiply(sk_c6,sk_c9)
| sk_c5 = multiply(sk_c4,sk_c10) ),
inference(reorient_equations,[],[f80]) ).
fof(f82,negated_conjecture,
( multiply(sk_c10,sk_c8) = sk_c9
| multiply(sk_c4,sk_c10) = sk_c5 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_40) ).
fof(f83,plain,
( sk_c9 = multiply(sk_c10,sk_c8)
| sk_c5 = multiply(sk_c4,sk_c10) ),
inference(reorient_equations,[],[f82]) ).
fof(f84,negated_conjecture,
( multiply(sk_c7,sk_c10) = sk_c8
| multiply(sk_c4,sk_c10) = sk_c5 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_41) ).
fof(f85,plain,
( sk_c8 = multiply(sk_c7,sk_c10)
| sk_c5 = multiply(sk_c4,sk_c10) ),
inference(reorient_equations,[],[f84]) ).
fof(f86,negated_conjecture,
( inverse(sk_c7) = sk_c10
| multiply(sk_c4,sk_c10) = sk_c5 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_42) ).
fof(f87,plain,
( sk_c10 = inverse(sk_c7)
| sk_c5 = multiply(sk_c4,sk_c10) ),
inference(reorient_equations,[],[f86]) ).
fof(f88,negated_conjecture,
( inverse(sk_c10) = sk_c9
| inverse(sk_c4) = sk_c10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_43) ).
fof(f89,plain,
( inverse(sk_c10) = sk_c9
| sk_c10 = inverse(sk_c4) ),
inference(reorient_equations,[],[f88]) ).
fof(f90,negated_conjecture,
( inverse(sk_c6) = sk_c10
| inverse(sk_c4) = sk_c10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_44) ).
fof(f91,plain,
( sk_c10 = inverse(sk_c6)
| sk_c10 = inverse(sk_c4) ),
inference(reorient_equations,[],[f90]) ).
fof(f92,negated_conjecture,
( multiply(sk_c6,sk_c9) = sk_c10
| inverse(sk_c4) = sk_c10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_45) ).
fof(f93,plain,
( sk_c10 = multiply(sk_c6,sk_c9)
| sk_c10 = inverse(sk_c4) ),
inference(reorient_equations,[],[f92]) ).
fof(f94,negated_conjecture,
( multiply(sk_c10,sk_c8) = sk_c9
| inverse(sk_c4) = sk_c10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_46) ).
fof(f95,plain,
( sk_c9 = multiply(sk_c10,sk_c8)
| sk_c10 = inverse(sk_c4) ),
inference(reorient_equations,[],[f94]) ).
fof(f96,negated_conjecture,
( multiply(sk_c7,sk_c10) = sk_c8
| inverse(sk_c4) = sk_c10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_47) ).
fof(f97,plain,
( sk_c8 = multiply(sk_c7,sk_c10)
| sk_c10 = inverse(sk_c4) ),
inference(reorient_equations,[],[f96]) ).
fof(f98,negated_conjecture,
( inverse(sk_c7) = sk_c10
| inverse(sk_c4) = sk_c10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_48) ).
fof(f99,plain,
( sk_c10 = inverse(sk_c7)
| sk_c10 = inverse(sk_c4) ),
inference(reorient_equations,[],[f98]) ).
fof(f100,negated_conjecture,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( inverse(X7) != sk_c10
| multiply(X7,sk_c10) != X6
| multiply(sk_c10,X6) != sk_c9
| multiply(X5,sk_c9) != sk_c10
| inverse(X5) != sk_c10
| inverse(sk_c10) != sk_c9
| inverse(X4) != sk_c10
| multiply(X4,sk_c10) != X3
| multiply(sk_c10,X3) != sk_c9
| multiply(X2,sk_c10) != sk_c9
| inverse(X1) != X2
| multiply(X1,X2) != sk_c9
| multiply(X0,sk_c9) != sk_c10
| inverse(X0) != sk_c10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_49) ).
fof(f101,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( sk_c10 != inverse(X7)
| multiply(X7,sk_c10) != X6
| sk_c9 != multiply(sk_c10,X6)
| sk_c10 != multiply(X5,sk_c9)
| sk_c10 != inverse(X5)
| inverse(sk_c10) != sk_c9
| sk_c10 != inverse(X4)
| multiply(X4,sk_c10) != X3
| sk_c9 != multiply(sk_c10,X3)
| sk_c9 != multiply(X2,sk_c10)
| inverse(X1) != X2
| multiply(X1,X2) != sk_c9
| sk_c10 != multiply(X0,sk_c9)
| inverse(X0) != sk_c10 ),
inference(reorient_equations,[],[f100]) ).
fof(f102,plain,
! [X3,X0,X1,X6,X7,X4,X5] :
( sk_c10 != inverse(X7)
| multiply(X7,sk_c10) != X6
| sk_c9 != multiply(sk_c10,X6)
| sk_c10 != multiply(X5,sk_c9)
| sk_c10 != inverse(X5)
| inverse(sk_c10) != sk_c9
| sk_c10 != inverse(X4)
| multiply(X4,sk_c10) != X3
| sk_c9 != multiply(sk_c10,X3)
| sk_c9 != multiply(inverse(X1),sk_c10)
| sk_c9 != multiply(X1,inverse(X1))
| sk_c10 != multiply(X0,sk_c9)
| inverse(X0) != sk_c10 ),
inference(equality_resolution,[],[f101]) ).
fof(f103,plain,
! [X0,X1,X6,X7,X4,X5] :
( sk_c10 != inverse(X7)
| multiply(X7,sk_c10) != X6
| sk_c9 != multiply(sk_c10,X6)
| sk_c10 != multiply(X5,sk_c9)
| sk_c10 != inverse(X5)
| inverse(sk_c10) != sk_c9
| sk_c10 != inverse(X4)
| sk_c9 != multiply(sk_c10,multiply(X4,sk_c10))
| sk_c9 != multiply(inverse(X1),sk_c10)
| sk_c9 != multiply(X1,inverse(X1))
| sk_c10 != multiply(X0,sk_c9)
| inverse(X0) != sk_c10 ),
inference(equality_resolution,[],[f102]) ).
fof(f104,plain,
! [X0,X1,X7,X4,X5] :
( sk_c10 != inverse(X7)
| sk_c9 != multiply(sk_c10,multiply(X7,sk_c10))
| sk_c10 != multiply(X5,sk_c9)
| sk_c10 != inverse(X5)
| inverse(sk_c10) != sk_c9
| sk_c10 != inverse(X4)
| sk_c9 != multiply(sk_c10,multiply(X4,sk_c10))
| sk_c9 != multiply(inverse(X1),sk_c10)
| sk_c9 != multiply(X1,inverse(X1))
| sk_c10 != multiply(X0,sk_c9)
| inverse(X0) != sk_c10 ),
inference(equality_resolution,[],[f103]) ).
tcf(c_101,plain,
! [X0: $i] : multiply(identity,X0) = X0,
inference(cnf_transformation,[],[f1]) ).
tcf(c_102,plain,
! [X0: $i] : multiply(inverse(X0),X0) = identity,
inference(cnf_transformation,[],[f3]) ).
tcf(c_103,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(multiply(X0,X1),X2) = multiply(X0,multiply(X1,X2)),
inference(cnf_transformation,[],[f4]) ).
tcf(c_104,negated_conjecture,
( ( inverse(sk_c10) = sk_c9 )
| ( inverse(sk_c1) = sk_c10 ) ),
inference(cnf_transformation,[],[f5]) ).
tcf(c_105,negated_conjecture,
( ( inverse(sk_c6) = sk_c10 )
| ( inverse(sk_c1) = sk_c10 ) ),
inference(cnf_transformation,[],[f7]) ).
tcf(c_106,negated_conjecture,
( ( inverse(sk_c1) = sk_c10 )
| ( multiply(sk_c6,sk_c9) = sk_c10 ) ),
inference(cnf_transformation,[],[f9]) ).
tcf(c_107,negated_conjecture,
( ( inverse(sk_c1) = sk_c10 )
| ( multiply(sk_c10,sk_c8) = sk_c9 ) ),
inference(cnf_transformation,[],[f11]) ).
tcf(c_108,negated_conjecture,
( ( inverse(sk_c1) = sk_c10 )
| ( multiply(sk_c7,sk_c10) = sk_c8 ) ),
inference(cnf_transformation,[],[f13]) ).
tcf(c_109,negated_conjecture,
( ( inverse(sk_c7) = sk_c10 )
| ( inverse(sk_c1) = sk_c10 ) ),
inference(cnf_transformation,[],[f15]) ).
tcf(c_110,negated_conjecture,
( ( inverse(sk_c10) = sk_c9 )
| ( multiply(sk_c1,sk_c9) = sk_c10 ) ),
inference(cnf_transformation,[],[f17]) ).
tcf(c_111,negated_conjecture,
( ( inverse(sk_c6) = sk_c10 )
| ( multiply(sk_c1,sk_c9) = sk_c10 ) ),
inference(cnf_transformation,[],[f19]) ).
tcf(c_112,negated_conjecture,
( ( multiply(sk_c6,sk_c9) = sk_c10 )
| ( multiply(sk_c1,sk_c9) = sk_c10 ) ),
inference(cnf_transformation,[],[f21]) ).
tcf(c_113,negated_conjecture,
( ( multiply(sk_c10,sk_c8) = sk_c9 )
| ( multiply(sk_c1,sk_c9) = sk_c10 ) ),
inference(cnf_transformation,[],[f23]) ).
tcf(c_114,negated_conjecture,
( ( multiply(sk_c7,sk_c10) = sk_c8 )
| ( multiply(sk_c1,sk_c9) = sk_c10 ) ),
inference(cnf_transformation,[],[f25]) ).
tcf(c_115,negated_conjecture,
( ( inverse(sk_c7) = sk_c10 )
| ( multiply(sk_c1,sk_c9) = sk_c10 ) ),
inference(cnf_transformation,[],[f27]) ).
tcf(c_116,negated_conjecture,
( ( inverse(sk_c10) = sk_c9 )
| ( multiply(sk_c2,sk_c3) = sk_c9 ) ),
inference(cnf_transformation,[],[f29]) ).
tcf(c_117,negated_conjecture,
( ( inverse(sk_c6) = sk_c10 )
| ( multiply(sk_c2,sk_c3) = sk_c9 ) ),
inference(cnf_transformation,[],[f31]) ).
tcf(c_118,negated_conjecture,
( ( multiply(sk_c2,sk_c3) = sk_c9 )
| ( multiply(sk_c6,sk_c9) = sk_c10 ) ),
inference(cnf_transformation,[],[f33]) ).
tcf(c_119,negated_conjecture,
( ( multiply(sk_c2,sk_c3) = sk_c9 )
| ( multiply(sk_c10,sk_c8) = sk_c9 ) ),
inference(cnf_transformation,[],[f35]) ).
tcf(c_120,negated_conjecture,
( ( multiply(sk_c2,sk_c3) = sk_c9 )
| ( multiply(sk_c7,sk_c10) = sk_c8 ) ),
inference(cnf_transformation,[],[f37]) ).
tcf(c_121,negated_conjecture,
( ( inverse(sk_c7) = sk_c10 )
| ( multiply(sk_c2,sk_c3) = sk_c9 ) ),
inference(cnf_transformation,[],[f39]) ).
tcf(c_122,negated_conjecture,
( ( inverse(sk_c2) = sk_c3 )
| ( inverse(sk_c10) = sk_c9 ) ),
inference(cnf_transformation,[],[f41]) ).
tcf(c_123,negated_conjecture,
( ( inverse(sk_c2) = sk_c3 )
| ( inverse(sk_c6) = sk_c10 ) ),
inference(cnf_transformation,[],[f43]) ).
tcf(c_124,negated_conjecture,
( ( inverse(sk_c2) = sk_c3 )
| ( multiply(sk_c6,sk_c9) = sk_c10 ) ),
inference(cnf_transformation,[],[f45]) ).
tcf(c_125,negated_conjecture,
( ( inverse(sk_c2) = sk_c3 )
| ( multiply(sk_c10,sk_c8) = sk_c9 ) ),
inference(cnf_transformation,[],[f47]) ).
tcf(c_126,negated_conjecture,
( ( inverse(sk_c2) = sk_c3 )
| ( multiply(sk_c7,sk_c10) = sk_c8 ) ),
inference(cnf_transformation,[],[f49]) ).
tcf(c_127,negated_conjecture,
( ( inverse(sk_c2) = sk_c3 )
| ( inverse(sk_c7) = sk_c10 ) ),
inference(cnf_transformation,[],[f51]) ).
tcf(c_129,negated_conjecture,
( ( inverse(sk_c6) = sk_c10 )
| ( multiply(sk_c3,sk_c10) = sk_c9 ) ),
inference(cnf_transformation,[],[f55]) ).
tcf(c_133,negated_conjecture,
( ( inverse(sk_c7) = sk_c10 )
| ( multiply(sk_c3,sk_c10) = sk_c9 ) ),
inference(cnf_transformation,[],[f63]) ).
tcf(c_134,negated_conjecture,
( ( inverse(sk_c10) = sk_c9 )
| ( multiply(sk_c10,sk_c5) = sk_c9 ) ),
inference(cnf_transformation,[],[f65]) ).
tcf(c_135,negated_conjecture,
( ( inverse(sk_c6) = sk_c10 )
| ( multiply(sk_c10,sk_c5) = sk_c9 ) ),
inference(cnf_transformation,[],[f67]) ).
tcf(c_136,negated_conjecture,
( ( multiply(sk_c6,sk_c9) = sk_c10 )
| ( multiply(sk_c10,sk_c5) = sk_c9 ) ),
inference(cnf_transformation,[],[f69]) ).
tcf(c_137,negated_conjecture,
( ( multiply(sk_c10,sk_c5) = sk_c9 )
| ( multiply(sk_c10,sk_c8) = sk_c9 ) ),
inference(cnf_transformation,[],[f71]) ).
tcf(c_138,negated_conjecture,
( ( multiply(sk_c7,sk_c10) = sk_c8 )
| ( multiply(sk_c10,sk_c5) = sk_c9 ) ),
inference(cnf_transformation,[],[f73]) ).
tcf(c_139,negated_conjecture,
( ( inverse(sk_c7) = sk_c10 )
| ( multiply(sk_c10,sk_c5) = sk_c9 ) ),
inference(cnf_transformation,[],[f75]) ).
tcf(c_140,negated_conjecture,
( ( inverse(sk_c10) = sk_c9 )
| ( multiply(sk_c4,sk_c10) = sk_c5 ) ),
inference(cnf_transformation,[],[f77]) ).
tcf(c_141,negated_conjecture,
( ( inverse(sk_c6) = sk_c10 )
| ( multiply(sk_c4,sk_c10) = sk_c5 ) ),
inference(cnf_transformation,[],[f79]) ).
tcf(c_142,negated_conjecture,
( ( multiply(sk_c4,sk_c10) = sk_c5 )
| ( multiply(sk_c6,sk_c9) = sk_c10 ) ),
inference(cnf_transformation,[],[f81]) ).
tcf(c_143,negated_conjecture,
( ( multiply(sk_c4,sk_c10) = sk_c5 )
| ( multiply(sk_c10,sk_c8) = sk_c9 ) ),
inference(cnf_transformation,[],[f83]) ).
tcf(c_144,negated_conjecture,
( ( multiply(sk_c4,sk_c10) = sk_c5 )
| ( multiply(sk_c7,sk_c10) = sk_c8 ) ),
inference(cnf_transformation,[],[f85]) ).
tcf(c_145,negated_conjecture,
( ( inverse(sk_c7) = sk_c10 )
| ( multiply(sk_c4,sk_c10) = sk_c5 ) ),
inference(cnf_transformation,[],[f87]) ).
tcf(c_146,negated_conjecture,
( ( inverse(sk_c4) = sk_c10 )
| ( inverse(sk_c10) = sk_c9 ) ),
inference(cnf_transformation,[],[f89]) ).
tcf(c_147,negated_conjecture,
( ( inverse(sk_c4) = sk_c10 )
| ( inverse(sk_c6) = sk_c10 ) ),
inference(cnf_transformation,[],[f91]) ).
tcf(c_148,negated_conjecture,
( ( inverse(sk_c4) = sk_c10 )
| ( multiply(sk_c6,sk_c9) = sk_c10 ) ),
inference(cnf_transformation,[],[f93]) ).
tcf(c_149,negated_conjecture,
( ( inverse(sk_c4) = sk_c10 )
| ( multiply(sk_c10,sk_c8) = sk_c9 ) ),
inference(cnf_transformation,[],[f95]) ).
tcf(c_150,negated_conjecture,
( ( inverse(sk_c4) = sk_c10 )
| ( multiply(sk_c7,sk_c10) = sk_c8 ) ),
inference(cnf_transformation,[],[f97]) ).
tcf(c_151,negated_conjecture,
( ( inverse(sk_c4) = sk_c10 )
| ( inverse(sk_c7) = sk_c10 ) ),
inference(cnf_transformation,[],[f99]) ).
tcf(c_152,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( ( inverse(sk_c10) != sk_c9 )
| ( inverse(X3) != sk_c10 )
| ( inverse(X2) != sk_c10 )
| ( inverse(X1) != sk_c10 )
| ( inverse(X0) != sk_c10 )
| ( multiply(X1,sk_c9) != sk_c10 )
| ( multiply(X0,sk_c9) != sk_c10 )
| ( multiply(inverse(X4),sk_c10) != sk_c9 )
| ( multiply(X4,inverse(X4)) != sk_c9 )
| ( multiply(sk_c10,multiply(X3,sk_c10)) != sk_c9 )
| ( multiply(sk_c10,multiply(X2,sk_c10)) != sk_c9 ) ),
inference(cnf_transformation,[],[f104]) ).
tcf(c_153,plain,
multiply(identity,sk_c10) = sk_c10,
inference(instantiation,[status(thm)],[c_101]) ).
tcf(c_154,plain,
multiply(inverse(sk_c10),sk_c10) = identity,
inference(instantiation,[status(thm)],[c_102]) ).
tcf(c_593,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_10
| ( inverse(X0) != sk_c10 )
| ( multiply(X0,sk_c9) != sk_c10 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_10])],[c_152]) ).
tcf(c_594,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_11
| ( multiply(inverse(X0),sk_c10) != sk_c9 )
| ( multiply(X0,inverse(X0)) != sk_c9 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_11])],[c_152]) ).
tcf(c_595,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_12
| ( inverse(X0) != sk_c10 )
| ( multiply(sk_c10,multiply(X0,sk_c10)) != sk_c9 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_12])],[c_152]) ).
tcf(c_596,negated_conjecture,
( iPr_def_12
| iPr_def_11
| iPr_def_10
| ( inverse(sk_c10) != sk_c9 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_152]) ).
tcf(c_597,definition,
iPr_def_13 = inverse(sk_c10),
introduced(definition,[new_symbols(definition,[iPr_def_13])],[]) ).
tcf(c_598,definition,
iPr_def_14 = inverse(sk_c7),
introduced(definition,[new_symbols(definition,[iPr_def_14])],[]) ).
tcf(c_599,definition,
iPr_def_15 = inverse(sk_c4),
introduced(definition,[new_symbols(definition,[iPr_def_15])],[]) ).
tcf(c_600,definition,
iPr_def_16 = multiply(sk_c7,sk_c10),
introduced(definition,[new_symbols(definition,[iPr_def_16])],[]) ).
tcf(c_601,definition,
iPr_def_17 = multiply(sk_c10,sk_c8),
introduced(definition,[new_symbols(definition,[iPr_def_17])],[]) ).
tcf(c_602,definition,
iPr_def_18 = multiply(sk_c6,sk_c9),
introduced(definition,[new_symbols(definition,[iPr_def_18])],[]) ).
tcf(c_603,definition,
iPr_def_19 = inverse(sk_c6),
introduced(definition,[new_symbols(definition,[iPr_def_19])],[]) ).
tcf(c_604,definition,
iPr_def_20 = multiply(sk_c4,sk_c10),
introduced(definition,[new_symbols(definition,[iPr_def_20])],[]) ).
tcf(c_605,definition,
iPr_def_21 = multiply(sk_c10,sk_c5),
introduced(definition,[new_symbols(definition,[iPr_def_21])],[]) ).
tcf(c_606,definition,
iPr_def_22 = multiply(sk_c3,sk_c10),
introduced(definition,[new_symbols(definition,[iPr_def_22])],[]) ).
tcf(c_607,definition,
iPr_def_23 = inverse(sk_c2),
introduced(definition,[new_symbols(definition,[iPr_def_23])],[]) ).
tcf(c_608,definition,
iPr_def_24 = multiply(sk_c2,sk_c3),
introduced(definition,[new_symbols(definition,[iPr_def_24])],[]) ).
tcf(c_609,definition,
iPr_def_25 = multiply(sk_c1,sk_c9),
introduced(definition,[new_symbols(definition,[iPr_def_25])],[]) ).
tcf(c_610,definition,
iPr_def_26 = inverse(sk_c1),
introduced(definition,[new_symbols(definition,[iPr_def_26])],[]) ).
tcf(c_611,negated_conjecture,
( iPr_def_12
| iPr_def_11
| iPr_def_10
| ( iPr_def_13 != sk_c9 ) ),
inference(demodulation,[status(thm)],[c_596,c_597]) ).
tcf(c_613,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_12
| ( inverse(X0) != sk_c10 )
| ( multiply(sk_c10,multiply(X0,sk_c10)) != sk_c9 ) ),
inference(demodulation,[status(thm)],[c_595]) ).
tcf(c_614,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_11
| ( multiply(inverse(X0),sk_c10) != sk_c9 )
| ( multiply(X0,inverse(X0)) != sk_c9 ) ),
inference(demodulation,[status(thm)],[c_594]) ).
tcf(c_616,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_10
| ( inverse(X0) != sk_c10 )
| ( multiply(X0,sk_c9) != sk_c10 ) ),
inference(demodulation,[status(thm)],[c_593]) ).
tcf(c_617,negated_conjecture,
( ( iPr_def_15 = sk_c10 )
| ( iPr_def_14 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_151,c_599,c_598]) ).
tcf(c_618,negated_conjecture,
( ( iPr_def_16 = sk_c8 )
| ( iPr_def_15 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_150,c_600]) ).
tcf(c_619,negated_conjecture,
( ( iPr_def_17 = sk_c9 )
| ( iPr_def_15 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_149,c_601]) ).
tcf(c_620,negated_conjecture,
( ( iPr_def_18 = sk_c10 )
| ( iPr_def_15 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_148,c_602]) ).
tcf(c_621,negated_conjecture,
( ( iPr_def_19 = sk_c10 )
| ( iPr_def_15 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_147,c_603]) ).
tcf(c_622,negated_conjecture,
( ( iPr_def_15 = sk_c10 )
| ( iPr_def_13 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_146]) ).
tcf(c_623,negated_conjecture,
( ( iPr_def_20 = sk_c5 )
| ( iPr_def_14 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_145,c_604]) ).
tcf(c_624,negated_conjecture,
( ( iPr_def_20 = sk_c5 )
| ( iPr_def_16 = sk_c8 ) ),
inference(demodulation,[status(thm)],[c_144]) ).
tcf(c_625,negated_conjecture,
( ( iPr_def_20 = sk_c5 )
| ( iPr_def_17 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_143]) ).
tcf(c_626,negated_conjecture,
( ( iPr_def_20 = sk_c5 )
| ( iPr_def_18 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_142]) ).
tcf(c_627,negated_conjecture,
( ( iPr_def_20 = sk_c5 )
| ( iPr_def_19 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_141]) ).
tcf(c_628,negated_conjecture,
( ( iPr_def_20 = sk_c5 )
| ( iPr_def_13 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_140]) ).
tcf(c_629,negated_conjecture,
( ( iPr_def_21 = sk_c9 )
| ( iPr_def_14 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_139,c_605]) ).
tcf(c_630,negated_conjecture,
( ( iPr_def_21 = sk_c9 )
| ( iPr_def_16 = sk_c8 ) ),
inference(demodulation,[status(thm)],[c_138]) ).
tcf(c_631,negated_conjecture,
( ( iPr_def_21 = sk_c9 )
| ( iPr_def_17 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_137]) ).
tcf(c_632,negated_conjecture,
( ( iPr_def_21 = sk_c9 )
| ( iPr_def_18 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_136]) ).
tcf(c_633,negated_conjecture,
( ( iPr_def_21 = sk_c9 )
| ( iPr_def_19 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_135]) ).
tcf(c_634,negated_conjecture,
( ( iPr_def_21 = sk_c9 )
| ( iPr_def_13 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_134]) ).
tcf(c_635,negated_conjecture,
( ( iPr_def_22 = sk_c9 )
| ( iPr_def_14 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_133,c_606]) ).
tcf(c_639,negated_conjecture,
( ( iPr_def_22 = sk_c9 )
| ( iPr_def_19 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_129]) ).
tcf(c_641,negated_conjecture,
( ( iPr_def_23 = sk_c3 )
| ( iPr_def_14 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_127,c_607]) ).
tcf(c_642,negated_conjecture,
( ( iPr_def_23 = sk_c3 )
| ( iPr_def_16 = sk_c8 ) ),
inference(demodulation,[status(thm)],[c_126]) ).
tcf(c_643,negated_conjecture,
( ( iPr_def_23 = sk_c3 )
| ( iPr_def_17 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_125]) ).
tcf(c_644,negated_conjecture,
( ( iPr_def_23 = sk_c3 )
| ( iPr_def_18 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_124]) ).
tcf(c_645,negated_conjecture,
( ( iPr_def_23 = sk_c3 )
| ( iPr_def_19 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_123]) ).
tcf(c_646,negated_conjecture,
( ( iPr_def_23 = sk_c3 )
| ( iPr_def_13 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_122]) ).
tcf(c_647,negated_conjecture,
( ( iPr_def_24 = sk_c9 )
| ( iPr_def_14 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_121,c_608]) ).
tcf(c_648,negated_conjecture,
( ( iPr_def_24 = sk_c9 )
| ( iPr_def_16 = sk_c8 ) ),
inference(demodulation,[status(thm)],[c_120]) ).
tcf(c_649,negated_conjecture,
( ( iPr_def_24 = sk_c9 )
| ( iPr_def_17 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_119]) ).
tcf(c_650,negated_conjecture,
( ( iPr_def_24 = sk_c9 )
| ( iPr_def_18 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_118]) ).
tcf(c_651,negated_conjecture,
( ( iPr_def_24 = sk_c9 )
| ( iPr_def_19 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_117]) ).
tcf(c_652,negated_conjecture,
( ( iPr_def_24 = sk_c9 )
| ( iPr_def_13 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_116]) ).
tcf(c_653,negated_conjecture,
( ( iPr_def_25 = sk_c10 )
| ( iPr_def_14 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_115,c_609]) ).
tcf(c_654,negated_conjecture,
( ( iPr_def_25 = sk_c10 )
| ( iPr_def_16 = sk_c8 ) ),
inference(demodulation,[status(thm)],[c_114]) ).
tcf(c_655,negated_conjecture,
( ( iPr_def_25 = sk_c10 )
| ( iPr_def_17 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_113]) ).
tcf(c_656,negated_conjecture,
( ( iPr_def_25 = sk_c10 )
| ( iPr_def_18 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_112]) ).
tcf(c_657,negated_conjecture,
( ( iPr_def_25 = sk_c10 )
| ( iPr_def_19 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_111]) ).
tcf(c_658,negated_conjecture,
( ( iPr_def_25 = sk_c10 )
| ( iPr_def_13 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_110]) ).
tcf(c_659,negated_conjecture,
( ( iPr_def_26 = sk_c10 )
| ( iPr_def_14 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_109,c_610]) ).
tcf(c_660,negated_conjecture,
( ( iPr_def_26 = sk_c10 )
| ( iPr_def_16 = sk_c8 ) ),
inference(demodulation,[status(thm)],[c_108]) ).
tcf(c_661,negated_conjecture,
( ( iPr_def_26 = sk_c10 )
| ( iPr_def_17 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_107]) ).
tcf(c_662,negated_conjecture,
( ( iPr_def_26 = sk_c10 )
| ( iPr_def_18 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_106]) ).
tcf(c_663,negated_conjecture,
( ( iPr_def_26 = sk_c10 )
| ( iPr_def_19 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_105]) ).
tcf(c_664,negated_conjecture,
( ( iPr_def_26 = sk_c10 )
| ( iPr_def_13 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_104]) ).
tcf(c_665,plain,
! [X0: $i] : X0 = X0,
theory(equality) ).
tcf(c_666,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = X0 )
| ( X2 != X1 )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_667,plain,
! [X0: $i,X1: $i] :
( ( inverse(X0) = inverse(X1) )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_668,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( multiply(X0,X2) = multiply(X1,X3) )
| ( X2 != X3 )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_669,plain,
( ( inverse(sk_c10) = inverse(sk_c10) )
| ( sk_c10 != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_667]) ).
tcf(c_671,plain,
sk_c10 = sk_c10,
inference(instantiation,[status(thm)],[c_665]) ).
tcf(c_674,plain,
( ~ iPr_def_12
| ( inverse(sk_c10) != sk_c10 )
| ( multiply(sk_c10,multiply(sk_c10,sk_c10)) != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_613]) ).
tcf(c_982,plain,
( ( iPr_def_18 = iPr_def_19 )
| ( sk_c10 = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_621,c_620]) ).
tcf(c_983,plain,
( ( iPr_def_15 = iPr_def_19 )
| ( sk_c10 = iPr_def_15 )
| ( sk_c10 = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_621,c_617]) ).
tcf(c_993,plain,
( ( iPr_def_13 = iPr_def_17 )
| ( sk_c10 = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_619,c_622]) ).
tcf(c_995,plain,
( iPr_def_12
| iPr_def_11
| iPr_def_10
| ( sk_c10 = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_622,c_611]) ).
tcf(c_1006,plain,
( ( sk_c10 = iPr_def_15 )
| ( inverse(iPr_def_19) = iPr_def_13 ) ),
inference(superposition,[status(thm)],[c_621,c_597]) ).
tcf(c_1016,plain,
( ( sk_c10 = iPr_def_15 )
| ( multiply(sk_c7,iPr_def_18) = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_620,c_600]) ).
tcf(c_1017,plain,
( ( sk_c10 = iPr_def_14 )
| ( multiply(sk_c7,iPr_def_15) = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_617,c_600]) ).
tcf(c_1026,plain,
( ( sk_c10 = iPr_def_14 )
| ( multiply(iPr_def_15,sk_c8) = iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_617,c_601]) ).
tcf(c_1027,plain,
( ( sk_c10 = iPr_def_15 )
| ( multiply(sk_c10,iPr_def_16) = iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_618,c_601]) ).
tcf(c_1106,plain,
( ( sk_c10 = iPr_def_15 )
| ( multiply(sk_c6,iPr_def_17) = iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_619,c_602]) ).
tcf(c_1115,plain,
( ( sk_c10 = iPr_def_15 )
| ( multiply(sk_c4,iPr_def_19) = iPr_def_20 ) ),
inference(superposition,[status(thm)],[c_621,c_604]) ).
tcf(c_1126,plain,
( ( sk_c10 = iPr_def_14 )
| ( multiply(iPr_def_15,sk_c5) = iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_617,c_605]) ).
tcf(c_1127,plain,
( ( sk_c9 = iPr_def_13 )
| ( multiply(sk_c10,iPr_def_20) = iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_628,c_605]) ).
tcf(c_1161,plain,
( ( sk_c10 = iPr_def_14 )
| ( multiply(sk_c1,iPr_def_21) = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_629,c_609]) ).
tcf(c_1172,plain,
multiply(iPr_def_26,sk_c1) = identity,
inference(superposition,[status(thm)],[c_610,c_102]) ).
tcf(c_1173,plain,
multiply(iPr_def_13,sk_c10) = identity,
inference(superposition,[status(thm)],[c_597,c_102]) ).
tcf(c_1174,plain,
multiply(iPr_def_19,sk_c6) = identity,
inference(superposition,[status(thm)],[c_603,c_102]) ).
tcf(c_1175,plain,
multiply(iPr_def_14,sk_c7) = identity,
inference(superposition,[status(thm)],[c_598,c_102]) ).
tcf(c_1176,plain,
multiply(iPr_def_23,sk_c2) = identity,
inference(superposition,[status(thm)],[c_607,c_102]) ).
tcf(c_1177,plain,
multiply(iPr_def_15,sk_c4) = identity,
inference(superposition,[status(thm)],[c_599,c_102]) ).
tcf(c_1193,plain,
( ( sk_c10 = iPr_def_18 )
| ( multiply(sk_c1,iPr_def_21) = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_632,c_609]) ).
tcf(c_1213,plain,
! [X0: $i,X1: $i] :
( ( inverse(X0) = sk_c10 )
| ( sk_c10 != X1 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_666]) ).
tcf(c_1220,plain,
( ( sk_c10 = iPr_def_19 )
| ( multiply(sk_c1,iPr_def_21) = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_633,c_609]) ).
tcf(c_1241,plain,
! [X0: $i] : inverse(X0) = inverse(X0),
inference(instantiation,[status(thm)],[c_665]) ).
tcf(c_1244,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( inverse(X0) = X2 )
| ( X2 != X1 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_666]) ).
tcf(c_1256,plain,
( iPr_def_12
| iPr_def_11
| iPr_def_10
| ( sk_c9 = iPr_def_13 )
| ( iPr_def_13 != iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_634,c_611]) ).
tcf(c_1273,plain,
! [X0: $i,X1: $i] :
( ( sk_c10 = inverse(X0) )
| ( sk_c10 != X1 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_666]) ).
tcf(c_1279,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( inverse(X0) = X2 )
| ( X2 != inverse(X1) )
| ( inverse(X0) != inverse(X1) ) ),
inference(instantiation,[status(thm)],[c_1244]) ).
tcf(c_1283,plain,
! [X0: $i,X1: $i] :
( ( sk_c10 = inverse(X0) )
| ( sk_c10 != inverse(X1) )
| ( inverse(X0) != inverse(X1) ) ),
inference(instantiation,[status(thm)],[c_1273]) ).
tcf(c_1302,plain,
( ( iPr_def_21 = iPr_def_22 )
| ( sk_c10 = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_635,c_629]) ).
tcf(c_1340,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = inverse(X0) )
| ( X2 != X1 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_666]) ).
tcf(c_1342,plain,
! [X0: $i] :
( ( inverse(X0) = iPr_def_13 )
| ( iPr_def_13 != inverse(sk_c10) )
| ( inverse(X0) != inverse(sk_c10) ) ),
inference(instantiation,[status(thm)],[c_1279]) ).
tcf(c_1343,plain,
( ( inverse(sk_c10) = iPr_def_13 )
| ( iPr_def_13 != inverse(sk_c10) )
| ( inverse(sk_c10) != inverse(sk_c10) ) ),
inference(instantiation,[status(thm)],[c_1342]) ).
tcf(c_1344,plain,
! [X0: $i] :
( ( inverse(X0) = iPr_def_14 )
| ( iPr_def_14 != inverse(sk_c7) )
| ( inverse(X0) != inverse(sk_c7) ) ),
inference(instantiation,[status(thm)],[c_1279]) ).
tcf(c_1346,plain,
! [X0: $i] :
( ( inverse(X0) = iPr_def_15 )
| ( iPr_def_15 != inverse(sk_c4) )
| ( inverse(X0) != inverse(sk_c4) ) ),
inference(instantiation,[status(thm)],[c_1279]) ).
tcf(c_1348,plain,
! [X0: $i] :
( ( inverse(X0) = iPr_def_19 )
| ( iPr_def_19 != inverse(sk_c6) )
| ( inverse(X0) != inverse(sk_c6) ) ),
inference(instantiation,[status(thm)],[c_1279]) ).
tcf(c_1352,plain,
! [X0: $i] :
( ( inverse(X0) = iPr_def_26 )
| ( iPr_def_26 != inverse(sk_c1) )
| ( inverse(X0) != inverse(sk_c1) ) ),
inference(instantiation,[status(thm)],[c_1279]) ).
tcf(c_1401,plain,
! [X0: $i] :
( ( sk_c10 = inverse(X0) )
| ( sk_c10 != iPr_def_13 )
| ( inverse(X0) != iPr_def_13 ) ),
inference(instantiation,[status(thm)],[c_1273]) ).
tcf(c_1402,plain,
! [X0: $i,X1: $i] :
( ( inverse(X0) = X1 )
| ( X1 != iPr_def_13 )
| ( inverse(X0) != iPr_def_13 ) ),
inference(instantiation,[status(thm)],[c_1244]) ).
tcf(c_1403,plain,
! [X0: $i] :
( ( inverse(X0) = sk_c10 )
| ( sk_c10 != iPr_def_13 )
| ( inverse(X0) != iPr_def_13 ) ),
inference(instantiation,[status(thm)],[c_1213]) ).
tcf(c_1404,plain,
( ( inverse(sk_c10) = sk_c10 )
| ( sk_c10 != iPr_def_13 )
| ( inverse(sk_c10) != iPr_def_13 ) ),
inference(instantiation,[status(thm)],[c_1403]) ).
tcf(c_1405,plain,
( ( sk_c10 = inverse(sk_c10) )
| ( sk_c10 != iPr_def_13 )
| ( inverse(sk_c10) != iPr_def_13 ) ),
inference(instantiation,[status(thm)],[c_1401]) ).
tcf(c_1451,plain,
! [X0: $i,X1: $i] :
( ( inverse(X0) = X1 )
| ( X1 != iPr_def_14 )
| ( inverse(X0) != iPr_def_14 ) ),
inference(instantiation,[status(thm)],[c_1244]) ).
tcf(c_1455,plain,
! [X0: $i] :
( ( sk_c10 = inverse(X0) )
| ( sk_c10 != iPr_def_15 )
| ( inverse(X0) != iPr_def_15 ) ),
inference(instantiation,[status(thm)],[c_1273]) ).
tcf(c_1456,plain,
! [X0: $i,X1: $i] :
( ( inverse(X0) = X1 )
| ( X1 != iPr_def_15 )
| ( inverse(X0) != iPr_def_15 ) ),
inference(instantiation,[status(thm)],[c_1244]) ).
tcf(c_1457,plain,
! [X0: $i] :
( ( inverse(X0) = sk_c10 )
| ( sk_c10 != iPr_def_15 )
| ( inverse(X0) != iPr_def_15 ) ),
inference(instantiation,[status(thm)],[c_1213]) ).
tcf(c_1459,plain,
( ( sk_c10 = inverse(sk_c10) )
| ( sk_c10 != iPr_def_15 )
| ( inverse(sk_c10) != iPr_def_15 ) ),
inference(instantiation,[status(thm)],[c_1455]) ).
tcf(c_1472,plain,
( ( iPr_def_21 = iPr_def_22 )
| ( sk_c10 = iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_639,c_633]) ).
tcf(c_1502,plain,
! [X0: $i,X1: $i] :
( ( inverse(X0) = X1 )
| ( X1 != iPr_def_19 )
| ( inverse(X0) != iPr_def_19 ) ),
inference(instantiation,[status(thm)],[c_1244]) ).
tcf(c_1549,plain,
! [X0: $i] :
( ( sk_c10 = inverse(X0) )
| ( sk_c10 != iPr_def_26 )
| ( inverse(X0) != iPr_def_26 ) ),
inference(instantiation,[status(thm)],[c_1273]) ).
tcf(c_1550,plain,
! [X0: $i,X1: $i] :
( ( inverse(X0) = X1 )
| ( X1 != iPr_def_26 )
| ( inverse(X0) != iPr_def_26 ) ),
inference(instantiation,[status(thm)],[c_1244]) ).
tcf(c_1551,plain,
! [X0: $i] :
( ( inverse(X0) = sk_c10 )
| ( sk_c10 != iPr_def_26 )
| ( inverse(X0) != iPr_def_26 ) ),
inference(instantiation,[status(thm)],[c_1213]) ).
tcf(c_1558,plain,
( ( sk_c10 = iPr_def_14 )
| ( multiply(sk_c2,iPr_def_23) = iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_641,c_608]) ).
tcf(c_1568,plain,
( ( sk_c3 = iPr_def_23 )
| ( multiply(sk_c10,iPr_def_16) = iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_642,c_601]) ).
tcf(c_1575,plain,
( ( sk_c9 = iPr_def_17 )
| ( multiply(sk_c2,iPr_def_23) = iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_643,c_608]) ).
tcf(c_1591,plain,
( ( sk_c10 = iPr_def_18 )
| ( multiply(sk_c2,iPr_def_23) = iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_644,c_608]) ).
tcf(c_1601,plain,
( ( sk_c10 = iPr_def_19 )
| ( multiply(sk_c2,iPr_def_23) = iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_645,c_608]) ).
tcf(c_1609,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = inverse(X0) )
| ( X2 != inverse(X1) )
| ( inverse(X0) != inverse(X1) ) ),
inference(instantiation,[status(thm)],[c_1340]) ).
tcf(c_1612,plain,
! [X0: $i,X1: $i] :
( ( X1 = inverse(X0) )
| ( X1 != iPr_def_13 )
| ( inverse(X0) != iPr_def_13 ) ),
inference(instantiation,[status(thm)],[c_1340]) ).
tcf(c_1613,plain,
! [X0: $i,X1: $i] :
( ( X1 = inverse(X0) )
| ( X1 != iPr_def_14 )
| ( inverse(X0) != iPr_def_14 ) ),
inference(instantiation,[status(thm)],[c_1340]) ).
tcf(c_1614,plain,
! [X0: $i,X1: $i] :
( ( X1 = inverse(X0) )
| ( X1 != iPr_def_15 )
| ( inverse(X0) != iPr_def_15 ) ),
inference(instantiation,[status(thm)],[c_1340]) ).
tcf(c_1615,plain,
! [X0: $i,X1: $i] :
( ( X1 = inverse(X0) )
| ( X1 != iPr_def_19 )
| ( inverse(X0) != iPr_def_19 ) ),
inference(instantiation,[status(thm)],[c_1340]) ).
tcf(c_1617,plain,
! [X0: $i,X1: $i] :
( ( X1 = inverse(X0) )
| ( X1 != iPr_def_26 )
| ( inverse(X0) != iPr_def_26 ) ),
inference(instantiation,[status(thm)],[c_1340]) ).
tcf(c_1622,plain,
( ( sk_c9 = iPr_def_13 )
| ( multiply(sk_c2,iPr_def_23) = iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_646,c_608]) ).
tcf(c_1648,plain,
( ( iPr_def_22 = iPr_def_24 )
| ( sk_c10 = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_647,c_635]) ).
tcf(c_1655,plain,
( ( iPr_def_21 = iPr_def_24 )
| ( sk_c10 = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_647,c_629]) ).
tcf(c_1707,plain,
! [X0: $i] :
( ( sk_c10 = iPr_def_13 )
| ( iPr_def_13 != X0 )
| ( sk_c10 != X0 ) ),
inference(instantiation,[status(thm)],[c_666]) ).
tcf(c_1714,plain,
! [X0: $i] :
( ( sk_c10 = iPr_def_26 )
| ( iPr_def_26 != X0 )
| ( sk_c10 != X0 ) ),
inference(instantiation,[status(thm)],[c_666]) ).
tcf(c_1722,plain,
( ( sk_c9 = iPr_def_24 )
| ( multiply(sk_c10,iPr_def_16) = iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_648,c_601]) ).
tcf(c_1729,plain,
! [X0: $i,X1: $i] :
( ( X0 = iPr_def_13 )
| ( iPr_def_13 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_666]) ).
tcf(c_1730,plain,
! [X0: $i,X1: $i] :
( ( inverse(X0) = inverse(X1) )
| ( inverse(X1) != iPr_def_13 )
| ( inverse(X0) != iPr_def_13 ) ),
inference(instantiation,[status(thm)],[c_1402]) ).
tcf(c_1755,plain,
( ( sk_c9 = iPr_def_17 )
| ( multiply(sk_c1,iPr_def_24) = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_649,c_609]) ).
tcf(c_1757,plain,
( ( iPr_def_21 = iPr_def_24 )
| ( sk_c9 = iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_649,c_631]) ).
tcf(c_1788,plain,
! [X0: $i,X1: $i] :
( ( X0 = iPr_def_23 )
| ( iPr_def_23 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_666]) ).
tcf(c_1813,plain,
( ( sk_c10 = iPr_def_18 )
| ( multiply(sk_c1,iPr_def_24) = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_650,c_609]) ).
tcf(c_1855,plain,
! [X0: $i,X1: $i] :
( ( X0 = iPr_def_26 )
| ( iPr_def_26 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_666]) ).
tcf(c_1884,plain,
( ( iPr_def_22 = iPr_def_24 )
| ( sk_c10 = iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_651,c_639]) ).
tcf(c_1889,plain,
( ( iPr_def_21 = iPr_def_24 )
| ( sk_c10 = iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_651,c_633]) ).
tcf(c_1928,plain,
( ( inverse(sk_c7) = iPr_def_14 )
| ( iPr_def_14 != inverse(sk_c7) )
| ( inverse(sk_c7) != inverse(sk_c7) ) ),
inference(instantiation,[status(thm)],[c_1344]) ).
tcf(c_1929,plain,
inverse(sk_c7) = inverse(sk_c7),
inference(instantiation,[status(thm)],[c_1241]) ).
tcf(c_1953,plain,
( ( iPr_def_21 = iPr_def_24 )
| ( sk_c9 = iPr_def_13 ) ),
inference(superposition,[status(thm)],[c_652,c_634]) ).
tcf(c_1956,plain,
( ( sk_c9 = iPr_def_13 )
| ( multiply(sk_c1,iPr_def_24) = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_652,c_609]) ).
tcf(c_1962,plain,
( iPr_def_12
| iPr_def_11
| iPr_def_10
| ( sk_c9 = iPr_def_13 )
| ( iPr_def_13 != iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_652,c_611]) ).
tcf(c_1987,plain,
( ( inverse(sk_c4) = iPr_def_15 )
| ( iPr_def_15 != inverse(sk_c4) )
| ( inverse(sk_c4) != inverse(sk_c4) ) ),
inference(instantiation,[status(thm)],[c_1346]) ).
tcf(c_1988,plain,
inverse(sk_c4) = inverse(sk_c4),
inference(instantiation,[status(thm)],[c_1241]) ).
tcf(c_2007,plain,
( ( iPr_def_15 = iPr_def_25 )
| ( sk_c10 = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_653,c_617]) ).
tcf(c_2035,plain,
( ( inverse(sk_c6) = iPr_def_19 )
| ( iPr_def_19 != inverse(sk_c6) )
| ( inverse(sk_c6) != inverse(sk_c6) ) ),
inference(instantiation,[status(thm)],[c_1348]) ).
tcf(c_2036,plain,
inverse(sk_c6) = inverse(sk_c6),
inference(instantiation,[status(thm)],[c_1241]) ).
tcf(c_2093,plain,
( iPr_def_12
| iPr_def_11
| iPr_def_10
| ( sk_c10 = iPr_def_25 )
| ( iPr_def_13 != iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_655,c_611]) ).
tcf(c_2156,plain,
( ( inverse(sk_c1) = iPr_def_26 )
| ( iPr_def_26 != inverse(sk_c1) )
| ( inverse(sk_c1) != inverse(sk_c1) ) ),
inference(instantiation,[status(thm)],[c_1352]) ).
tcf(c_2157,plain,
inverse(sk_c1) = inverse(sk_c1),
inference(instantiation,[status(thm)],[c_1241]) ).
tcf(c_2170,plain,
iPr_def_13 = iPr_def_13,
inference(instantiation,[status(thm)],[c_665]) ).
tcf(c_2185,plain,
iPr_def_26 = iPr_def_26,
inference(instantiation,[status(thm)],[c_665]) ).
tcf(c_2197,plain,
! [X0: $i] :
( ( iPr_def_15 = inverse(X0) )
| ( iPr_def_15 != inverse(sk_c4) )
| ( inverse(X0) != inverse(sk_c4) ) ),
inference(instantiation,[status(thm)],[c_1609]) ).
tcf(c_2218,plain,
( ( sk_c10 = iPr_def_18 )
| ( multiply(sk_c4,iPr_def_25) = iPr_def_20 ) ),
inference(superposition,[status(thm)],[c_656,c_604]) ).
tcf(c_2262,plain,
( ( sk_c10 = iPr_def_19 )
| ( multiply(sk_c4,iPr_def_25) = iPr_def_20 ) ),
inference(superposition,[status(thm)],[c_657,c_604]) ).
tcf(c_2332,plain,
! [X0: $i] :
( ( X0 = inverse(sk_c7) )
| ( X0 != iPr_def_14 )
| ( inverse(sk_c7) != iPr_def_14 ) ),
inference(instantiation,[status(thm)],[c_1613]) ).
tcf(c_2334,plain,
! [X0: $i] :
( ( inverse(sk_c7) = X0 )
| ( X0 != iPr_def_14 )
| ( inverse(sk_c7) != iPr_def_14 ) ),
inference(instantiation,[status(thm)],[c_1451]) ).
tcf(c_2378,plain,
( ( iPr_def_13 = iPr_def_17 )
| ( sk_c10 = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_658,c_655]) ).
tcf(c_2392,plain,
( ( sk_c10 = iPr_def_25 )
| ( multiply(sk_c1,iPr_def_13) = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_658,c_609]) ).
tcf(c_2397,plain,
( iPr_def_12
| iPr_def_11
| iPr_def_10
| ( sk_c10 = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_658,c_611]) ).
tcf(c_2464,plain,
! [X0: $i] :
( ( X0 = inverse(sk_c4) )
| ( X0 != iPr_def_15 )
| ( inverse(sk_c4) != iPr_def_15 ) ),
inference(instantiation,[status(thm)],[c_1614]) ).
tcf(c_2465,plain,
( ( sk_c10 = inverse(sk_c4) )
| ( sk_c10 != iPr_def_15 )
| ( inverse(sk_c4) != iPr_def_15 ) ),
inference(instantiation,[status(thm)],[c_1455]) ).
tcf(c_2466,plain,
! [X0: $i] :
( ( inverse(sk_c4) = X0 )
| ( X0 != iPr_def_15 )
| ( inverse(sk_c4) != iPr_def_15 ) ),
inference(instantiation,[status(thm)],[c_1456]) ).
tcf(c_2467,plain,
( ( inverse(sk_c4) = sk_c10 )
| ( sk_c10 != iPr_def_15 )
| ( inverse(sk_c4) != iPr_def_15 ) ),
inference(instantiation,[status(thm)],[c_1457]) ).
tcf(c_2474,plain,
( iPr_def_12
| iPr_def_11
| iPr_def_10
| ( sk_c10 = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_622,c_611]) ).
tcf(c_2494,plain,
! [X0: $i] :
( ( inverse(sk_c6) = X0 )
| ( X0 != iPr_def_19 )
| ( inverse(sk_c6) != iPr_def_19 ) ),
inference(instantiation,[status(thm)],[c_1502]) ).
tcf(c_2551,plain,
( ( iPr_def_25 = iPr_def_26 )
| ( sk_c10 = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_659,c_653]) ).
tcf(c_2558,plain,
( ( sk_c10 = iPr_def_14 )
| ( inverse(iPr_def_26) = iPr_def_13 ) ),
inference(superposition,[status(thm)],[c_659,c_597]) ).
tcf(c_2561,plain,
( ( iPr_def_15 = iPr_def_26 )
| ( sk_c10 = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_659,c_617]) ).
tcf(c_2613,plain,
! [X0: $i,X1: $i] :
( ( iPr_def_13 = X0 )
| ( iPr_def_13 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_666]) ).
tcf(c_2671,plain,
( ( sk_c10 = iPr_def_26 )
| ( multiply(sk_c6,iPr_def_17) = iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_661,c_602]) ).
tcf(c_2675,plain,
( iPr_def_12
| iPr_def_11
| iPr_def_10
| ( sk_c10 = iPr_def_26 )
| ( iPr_def_13 != iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_661,c_611]) ).
tcf(c_2737,plain,
! [X0: $i,X1: $i] :
( ( iPr_def_26 = X0 )
| ( iPr_def_26 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_666]) ).
tcf(c_2738,plain,
( ( sk_c10 = iPr_def_26 )
| ( iPr_def_26 != inverse(sk_c1) )
| ( sk_c10 != inverse(sk_c1) ) ),
inference(instantiation,[status(thm)],[c_1714]) ).
tcf(c_2796,plain,
( ( sk_c10 = iPr_def_18 )
| ( multiply(sk_c4,iPr_def_26) = iPr_def_20 ) ),
inference(superposition,[status(thm)],[c_662,c_604]) ).
tcf(c_2799,plain,
( ( sk_c10 = iPr_def_18 )
| ( inverse(iPr_def_26) = iPr_def_13 ) ),
inference(superposition,[status(thm)],[c_662,c_597]) ).
tcf(c_2899,plain,
! [X0: $i] :
( ( inverse(X0) = inverse(sk_c1) )
| ( inverse(sk_c1) != iPr_def_13 )
| ( inverse(X0) != iPr_def_13 ) ),
inference(instantiation,[status(thm)],[c_1730]) ).
tcf(c_2900,plain,
( ( inverse(sk_c10) = inverse(sk_c1) )
| ( inverse(sk_c10) != iPr_def_13 )
| ( inverse(sk_c1) != iPr_def_13 ) ),
inference(instantiation,[status(thm)],[c_2899]) ).
tcf(c_2911,plain,
( ( iPr_def_25 = iPr_def_26 )
| ( sk_c10 = iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_663,c_657]) ).
tcf(c_2917,plain,
( ( sk_c10 = iPr_def_19 )
| ( multiply(sk_c4,iPr_def_26) = iPr_def_20 ) ),
inference(superposition,[status(thm)],[c_663,c_604]) ).
tcf(c_2920,plain,
( ( sk_c10 = iPr_def_19 )
| ( inverse(iPr_def_26) = iPr_def_13 ) ),
inference(superposition,[status(thm)],[c_663,c_597]) ).
tcf(c_2974,plain,
! [X0: $i] :
( ( X0 = iPr_def_26 )
| ( iPr_def_26 != inverse(sk_c1) )
| ( X0 != inverse(sk_c1) ) ),
inference(instantiation,[status(thm)],[c_1855]) ).
tcf(c_2997,plain,
( ( iPr_def_13 = iPr_def_17 )
| ( sk_c10 = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_664,c_661]) ).
tcf(c_3012,plain,
( ( sk_c10 = iPr_def_26 )
| ( multiply(sk_c1,iPr_def_13) = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_664,c_609]) ).
tcf(c_3087,plain,
multiply(identity,identity) = identity,
inference(instantiation,[status(thm)],[c_101]) ).
tcf(c_3092,plain,
identity = identity,
inference(instantiation,[status(thm)],[c_665]) ).
tcf(c_3094,plain,
! [X0: $i,X1: $i] :
( ( X0 = identity )
| ( identity != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_666]) ).
tcf(c_3130,plain,
( ~ iPr_def_10
| ( sk_c10 != iPr_def_18 )
| ( inverse(sk_c6) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_602,c_616]) ).
tcf(c_3131,plain,
( ~ iPr_def_10
| ( sk_c10 != iPr_def_25 )
| ( inverse(sk_c1) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_609,c_616]) ).
tcf(c_3158,plain,
( ~ iPr_def_10
| ( sk_c10 != iPr_def_26 )
| ( sk_c10 != iPr_def_25 ) ),
inference(light_normalisation,[status(thm)],[c_3131,c_610]) ).
tcf(c_3162,plain,
( ~ iPr_def_10
| ( sk_c10 != iPr_def_19 )
| ( sk_c10 != iPr_def_18 ) ),
inference(light_normalisation,[status(thm)],[c_3130,c_603]) ).
tcf(c_3282,plain,
! [X0: $i,X1: $i] :
( ( X0 = sk_c4 )
| ( sk_c4 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_666]) ).
tcf(c_3350,plain,
( ~ iPr_def_12
| ( inverse(sk_c7) != sk_c10 )
| ( multiply(sk_c10,iPr_def_16) != sk_c9 ) ),
inference(superposition,[status(thm)],[c_600,c_613]) ).
tcf(c_3352,plain,
( ~ iPr_def_12
| ( inverse(sk_c4) != sk_c10 )
| ( multiply(sk_c10,iPr_def_20) != sk_c9 ) ),
inference(superposition,[status(thm)],[c_604,c_613]) ).
tcf(c_3371,plain,
( ~ iPr_def_12
| ( sk_c10 != iPr_def_15 )
| ( multiply(sk_c10,iPr_def_20) != sk_c9 ) ),
inference(light_normalisation,[status(thm)],[c_3352,c_599]) ).
tcf(c_3378,plain,
( ~ iPr_def_12
| ( sk_c10 != iPr_def_14 )
| ( multiply(sk_c10,iPr_def_16) != sk_c9 ) ),
inference(light_normalisation,[status(thm)],[c_3350,c_598]) ).
tcf(c_3576,plain,
! [X0: $i] :
( ( inverse(sk_c1) = inverse(X0) )
| ( sk_c1 != X0 ) ),
inference(instantiation,[status(thm)],[c_667]) ).
tcf(c_3577,plain,
( ( inverse(sk_c1) = inverse(sk_c10) )
| ( sk_c1 != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_3576]) ).
tcf(c_3586,plain,
! [X0: $i] : multiply(sk_c7,multiply(sk_c10,X0)) = multiply(iPr_def_16,X0),
inference(superposition,[status(thm)],[c_600,c_103]) ).
tcf(c_3589,plain,
! [X0: $i] : multiply(sk_c3,multiply(sk_c10,X0)) = multiply(iPr_def_22,X0),
inference(superposition,[status(thm)],[c_606,c_103]) ).
tcf(c_3591,plain,
! [X0: $i] : multiply(sk_c4,multiply(sk_c10,X0)) = multiply(iPr_def_20,X0),
inference(superposition,[status(thm)],[c_604,c_103]) ).
tcf(c_3593,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(X0,X1)) = multiply(identity,X1),
inference(superposition,[status(thm)],[c_102,c_103]) ).
tcf(c_3595,plain,
! [X0: $i] : multiply(iPr_def_26,multiply(sk_c1,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1172,c_103]) ).
tcf(c_3596,plain,
! [X0: $i] : multiply(iPr_def_13,multiply(sk_c10,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1173,c_103]) ).
tcf(c_3597,plain,
! [X0: $i] : multiply(iPr_def_19,multiply(sk_c6,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1174,c_103]) ).
tcf(c_3598,plain,
! [X0: $i] : multiply(iPr_def_14,multiply(sk_c7,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1175,c_103]) ).
tcf(c_3599,plain,
! [X0: $i] : multiply(iPr_def_23,multiply(sk_c2,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1176,c_103]) ).
tcf(c_3600,plain,
! [X0: $i] : multiply(iPr_def_15,multiply(sk_c4,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1177,c_103]) ).
tcf(c_3605,plain,
! [X0: $i] : multiply(iPr_def_15,multiply(sk_c4,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_3600,c_101]) ).
tcf(c_3606,plain,
! [X0: $i] : multiply(iPr_def_23,multiply(sk_c2,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_3599,c_101]) ).
tcf(c_3607,plain,
! [X0: $i] : multiply(iPr_def_14,multiply(sk_c7,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_3598,c_101]) ).
tcf(c_3608,plain,
! [X0: $i] : multiply(iPr_def_19,multiply(sk_c6,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_3597,c_101]) ).
tcf(c_3609,plain,
! [X0: $i] : multiply(iPr_def_13,multiply(sk_c10,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_3596,c_101]) ).
tcf(c_3610,plain,
! [X0: $i] : multiply(iPr_def_26,multiply(sk_c1,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_3595,c_101]) ).
tcf(c_3689,plain,
! [X0: $i] :
( ( sk_c10 = iPr_def_13 )
| ( iPr_def_13 != inverse(X0) )
| ( sk_c10 != inverse(X0) ) ),
inference(instantiation,[status(thm)],[c_1707]) ).
tcf(c_3690,plain,
! [X0: $i,X1: $i] :
( ( X0 = iPr_def_13 )
| ( iPr_def_13 != inverse(X1) )
| ( X0 != inverse(X1) ) ),
inference(instantiation,[status(thm)],[c_1729]) ).
tcf(c_3786,plain,
! [X0: $i] :
( ( sk_c10 = sk_c9 )
| ( sk_c9 != X0 )
| ( sk_c10 != X0 ) ),
inference(instantiation,[status(thm)],[c_666]) ).
tcf(c_3799,plain,
sk_c9 = sk_c9,
inference(instantiation,[status(thm)],[c_665]) ).
tcf(c_3800,plain,
! [X0: $i,X1: $i] :
( ( X0 = sk_c9 )
| ( sk_c9 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_666]) ).
tcf(c_3816,plain,
( ( iPr_def_18 = iPr_def_19 )
| ( iPr_def_15 = iPr_def_26 )
| ( sk_c10 = iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_982,c_663]) ).
tcf(c_3817,plain,
( ( iPr_def_18 = iPr_def_19 )
| ( iPr_def_15 = iPr_def_26 )
| ( sk_c10 = iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_982,c_662]) ).
tcf(c_3819,plain,
( ( iPr_def_18 = iPr_def_19 )
| ( iPr_def_15 = iPr_def_25 )
| ( sk_c10 = iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_982,c_657]) ).
tcf(c_3820,plain,
( ( iPr_def_18 = iPr_def_19 )
| ( iPr_def_15 = iPr_def_25 )
| ( sk_c10 = iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_982,c_656]) ).
tcf(c_3825,plain,
( ( iPr_def_18 = iPr_def_19 )
| ( multiply(sk_c4,iPr_def_15) = iPr_def_20 ) ),
inference(superposition,[status(thm)],[c_982,c_604]) ).
tcf(c_3828,plain,
( ( iPr_def_18 = iPr_def_19 )
| ( inverse(iPr_def_15) = iPr_def_13 ) ),
inference(superposition,[status(thm)],[c_982,c_597]) ).
tcf(c_3950,plain,
! [X0: $i] :
( ( sk_c10 = iPr_def_15 )
| ( iPr_def_15 != X0 )
| ( sk_c10 != X0 ) ),
inference(instantiation,[status(thm)],[c_666]) ).
tcf(c_3951,plain,
( ( sk_c10 = iPr_def_15 )
| ( iPr_def_15 != sk_c10 )
| ( sk_c10 != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_3950]) ).
tcf(c_4220,plain,
! [X0: $i] :
( ( sk_c10 = inverse(X0) )
| ( sk_c10 != inverse(sk_c4) )
| ( inverse(X0) != inverse(sk_c4) ) ),
inference(instantiation,[status(thm)],[c_1283]) ).
tcf(c_4262,plain,
( ( inverse(sk_c1) = sk_c10 )
| ( sk_c10 != iPr_def_26 )
| ( inverse(sk_c1) != iPr_def_26 ) ),
inference(instantiation,[status(thm)],[c_1551]) ).
tcf(c_4348,plain,
! [X0: $i] :
( ( inverse(sk_c1) = X0 )
| ( X0 != iPr_def_26 )
| ( inverse(sk_c1) != iPr_def_26 ) ),
inference(instantiation,[status(thm)],[c_1550]) ).
tcf(c_4358,plain,
( ( sk_c10 = inverse(sk_c1) )
| ( sk_c10 != iPr_def_26 )
| ( inverse(sk_c1) != iPr_def_26 ) ),
inference(instantiation,[status(thm)],[c_1549]) ).
tcf(c_4429,plain,
( ( iPr_def_21 = iPr_def_22 )
| ( iPr_def_14 = iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_1472,c_1302]) ).
tcf(c_4510,plain,
( ( inverse(sk_c7) = inverse(sk_c4) )
| ( inverse(sk_c4) != iPr_def_14 )
| ( inverse(sk_c7) != iPr_def_14 ) ),
inference(instantiation,[status(thm)],[c_2334]) ).
tcf(c_5157,plain,
( ( inverse(sk_c4) = iPr_def_14 )
| ( iPr_def_14 != iPr_def_15 )
| ( inverse(sk_c4) != iPr_def_15 ) ),
inference(instantiation,[status(thm)],[c_2466]) ).
tcf(c_5573,plain,
( ( iPr_def_15 = iPr_def_26 )
| ( iPr_def_15 = iPr_def_19 )
| ( sk_c10 = iPr_def_19 )
| ( sk_c10 = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_983,c_663]) ).
tcf(c_5574,plain,
( ( iPr_def_15 = iPr_def_26 )
| ( iPr_def_15 = iPr_def_19 )
| ( sk_c10 = iPr_def_18 )
| ( sk_c10 = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_983,c_662]) ).
tcf(c_5694,plain,
( ( iPr_def_22 = iPr_def_24 )
| ( iPr_def_14 = iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_1884,c_1648]) ).
tcf(c_5823,plain,
( ( inverse(sk_c6) = iPr_def_14 )
| ( iPr_def_14 != iPr_def_19 )
| ( inverse(sk_c6) != iPr_def_19 ) ),
inference(instantiation,[status(thm)],[c_2494]) ).
tcf(c_5826,plain,
! [X0: $i] :
( ( inverse(sk_c6) = X0 )
| ( X0 != iPr_def_14 )
| ( inverse(sk_c6) != iPr_def_14 ) ),
inference(instantiation,[status(thm)],[c_1451]) ).
tcf(c_5835,plain,
( ( inverse(sk_c6) = sk_c10 )
| ( sk_c10 != iPr_def_15 )
| ( inverse(sk_c6) != iPr_def_15 ) ),
inference(instantiation,[status(thm)],[c_1457]) ).
tcf(c_5906,plain,
( ( iPr_def_21 = iPr_def_24 )
| ( iPr_def_14 = iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_1889,c_1655]) ).
tcf(c_6158,plain,
( iPr_def_12
| iPr_def_11
| iPr_def_10
| ( iPr_def_21 = iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_1953,c_611]) ).
tcf(c_6374,plain,
( ( iPr_def_15 = iPr_def_25 )
| ( multiply(sk_c7,iPr_def_14) = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_2007,c_600]) ).
tcf(c_6376,plain,
( ( iPr_def_15 = iPr_def_25 )
| ( iPr_def_14 = iPr_def_19 )
| ( sk_c10 = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_2007,c_621]) ).
tcf(c_6480,plain,
! [X0: $i] :
( ( X0 = inverse(sk_c1) )
| ( X0 != iPr_def_26 )
| ( inverse(sk_c1) != iPr_def_26 ) ),
inference(instantiation,[status(thm)],[c_1617]) ).
tcf(c_6561,plain,
( ( iPr_def_15 = iPr_def_25 )
| ( iPr_def_13 = iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_2378,c_993]) ).
tcf(c_6651,plain,
! [X0: $i] :
( ( iPr_def_13 = X0 )
| ( iPr_def_13 != iPr_def_13 )
| ( X0 != iPr_def_13 ) ),
inference(instantiation,[status(thm)],[c_2613]) ).
tcf(c_6719,plain,
! [X0: $i] :
( ( X0 = iPr_def_23 )
| ( iPr_def_23 != sk_c3 )
| ( X0 != sk_c3 ) ),
inference(instantiation,[status(thm)],[c_1788]) ).
tcf(c_6860,plain,
! [X0: $i] :
( ( inverse(X0) = iPr_def_26 )
| ( iPr_def_26 != iPr_def_13 )
| ( inverse(X0) != iPr_def_13 ) ),
inference(instantiation,[status(thm)],[c_1402]) ).
tcf(c_6862,plain,
( ( inverse(sk_c10) = iPr_def_26 )
| ( iPr_def_26 != iPr_def_13 )
| ( inverse(sk_c10) != iPr_def_13 ) ),
inference(instantiation,[status(thm)],[c_6860]) ).
tcf(c_6899,plain,
! [X0: $i] :
( ( iPr_def_26 = sk_c9 )
| ( iPr_def_26 != X0 )
| ( sk_c9 != X0 ) ),
inference(instantiation,[status(thm)],[c_2737]) ).
tcf(c_6953,plain,
( ( iPr_def_15 = iPr_def_26 )
| ( multiply(sk_c7,iPr_def_14) = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_2561,c_600]) ).
tcf(c_7325,plain,
( ( identity = inverse(sk_c7) )
| ( identity != iPr_def_14 )
| ( inverse(sk_c7) != iPr_def_14 ) ),
inference(instantiation,[status(thm)],[c_2332]) ).
tcf(c_7362,plain,
( ( iPr_def_25 = iPr_def_26 )
| ( iPr_def_14 = iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_2911,c_2551]) ).
tcf(c_7704,plain,
( ( inverse(sk_c1) = iPr_def_13 )
| ( iPr_def_13 != inverse(sk_c10) )
| ( inverse(sk_c1) != inverse(sk_c10) ) ),
inference(instantiation,[status(thm)],[c_1342]) ).
tcf(c_7811,plain,
multiply(iPr_def_15,iPr_def_20) = sk_c10,
inference(superposition,[status(thm)],[c_604,c_3605]) ).
tcf(c_7816,plain,
multiply(iPr_def_23,iPr_def_24) = sk_c3,
inference(superposition,[status(thm)],[c_608,c_3606]) ).
tcf(c_7821,plain,
multiply(iPr_def_14,iPr_def_16) = sk_c10,
inference(superposition,[status(thm)],[c_600,c_3607]) ).
tcf(c_7829,plain,
multiply(iPr_def_19,iPr_def_18) = sk_c9,
inference(superposition,[status(thm)],[c_602,c_3608]) ).
tcf(c_7856,plain,
( ( iPr_def_13 = iPr_def_26 )
| ( iPr_def_26 != inverse(sk_c1) )
| ( iPr_def_13 != inverse(sk_c1) ) ),
inference(instantiation,[status(thm)],[c_2974]) ).
tcf(c_7857,plain,
! [X0: $i] :
( ( iPr_def_13 = X0 )
| ( iPr_def_13 != iPr_def_26 )
| ( X0 != iPr_def_26 ) ),
inference(instantiation,[status(thm)],[c_2613]) ).
tcf(c_7859,plain,
( ( iPr_def_13 = sk_c10 )
| ( iPr_def_13 != iPr_def_26 )
| ( sk_c10 != iPr_def_26 ) ),
inference(instantiation,[status(thm)],[c_7857]) ).
tcf(c_7921,plain,
( ( sk_c10 = iPr_def_15 )
| ( multiply(iPr_def_14,iPr_def_16) = iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_1016,c_3607]) ).
tcf(c_7922,plain,
( ( sk_c10 = iPr_def_18 )
| ( sk_c10 = iPr_def_15 ) ),
inference(light_normalisation,[status(thm)],[c_7921,c_7821]) ).
tcf(c_7933,plain,
( ( sk_c10 = iPr_def_14 )
| ( multiply(iPr_def_14,iPr_def_16) = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_1017,c_3607]) ).
tcf(c_7934,plain,
( ( sk_c10 = iPr_def_15 )
| ( sk_c10 = iPr_def_14 ) ),
inference(light_normalisation,[status(thm)],[c_7933,c_7821]) ).
tcf(c_7957,plain,
multiply(iPr_def_13,iPr_def_17) = sk_c8,
inference(superposition,[status(thm)],[c_601,c_3609]) ).
tcf(c_7958,plain,
multiply(iPr_def_13,iPr_def_21) = sk_c5,
inference(superposition,[status(thm)],[c_605,c_3609]) ).
tcf(c_8144,plain,
multiply(iPr_def_26,iPr_def_25) = sk_c9,
inference(superposition,[status(thm)],[c_609,c_3610]) ).
tcf(c_8184,plain,
( ( sk_c9 = iPr_def_24 )
| ( sk_c10 = iPr_def_14 )
| ( multiply(iPr_def_15,iPr_def_16) = iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_648,c_1026]) ).
tcf(c_8346,plain,
( ( sk_c10 = iPr_def_15 )
| ( multiply(iPr_def_13,iPr_def_17) = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_1027,c_3609]) ).
tcf(c_8347,plain,
( ( sk_c8 = iPr_def_16 )
| ( sk_c10 = iPr_def_15 ) ),
inference(light_normalisation,[status(thm)],[c_8346,c_7957]) ).
tcf(c_8595,plain,
( ( sk_c10 = iPr_def_15 )
| ( multiply(iPr_def_19,iPr_def_18) = iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_1106,c_3608]) ).
tcf(c_8596,plain,
( ( sk_c9 = iPr_def_17 )
| ( sk_c10 = iPr_def_15 ) ),
inference(light_normalisation,[status(thm)],[c_8595,c_7829]) ).
tcf(c_8676,plain,
( ( sk_c10 = iPr_def_15 )
| ( multiply(iPr_def_15,iPr_def_20) = iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_1115,c_3605]) ).
tcf(c_8677,plain,
( ( sk_c10 = iPr_def_19 )
| ( sk_c10 = iPr_def_15 ) ),
inference(light_normalisation,[status(thm)],[c_8676,c_7811]) ).
tcf(c_8740,plain,
( ( sk_c10 = iPr_def_14 )
| ( multiply(iPr_def_15,iPr_def_20) = iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_623,c_1126]) ).
tcf(c_8742,plain,
( ( sk_c10 = iPr_def_21 )
| ( sk_c10 = iPr_def_14 ) ),
inference(light_normalisation,[status(thm)],[c_8740,c_7811]) ).
tcf(c_9003,plain,
( ( sk_c10 = iPr_def_14 )
| ( multiply(iPr_def_13,iPr_def_21) = identity ) ),
inference(superposition,[status(thm)],[c_8742,c_1173]) ).
tcf(c_9031,plain,
( ( sk_c5 = identity )
| ( sk_c10 = iPr_def_14 ) ),
inference(light_normalisation,[status(thm)],[c_9003,c_7958]) ).
tcf(c_9121,plain,
( ( sk_c4 = inverse(sk_c4) )
| ( sk_c4 != iPr_def_15 )
| ( inverse(sk_c4) != iPr_def_15 ) ),
inference(instantiation,[status(thm)],[c_2464]) ).
tcf(c_9300,plain,
( ( iPr_def_26 = iPr_def_13 )
| ( iPr_def_26 != inverse(sk_c1) )
| ( iPr_def_13 != inverse(sk_c1) ) ),
inference(instantiation,[status(thm)],[c_3690]) ).
tcf(c_9733,plain,
( iPr_def_12
| iPr_def_11
| ( sk_c10 = iPr_def_15 ) ),
inference(global_subsumption_just,[status(thm)],[c_2474,c_995,c_3162,c_7922,c_8677]) ).
tcf(c_10979,plain,
! [X0: $i] :
( ( sk_c10 = sk_c3 )
| ( sk_c3 != X0 )
| ( sk_c10 != X0 ) ),
inference(instantiation,[status(thm)],[c_666]) ).
tcf(c_10994,plain,
( ( sk_c3 = iPr_def_23 )
| ( iPr_def_23 != sk_c3 )
| ( sk_c3 != sk_c3 ) ),
inference(instantiation,[status(thm)],[c_6719]) ).
tcf(c_10995,plain,
sk_c3 = sk_c3,
inference(instantiation,[status(thm)],[c_665]) ).
tcf(c_11480,plain,
! [X0: $i] :
( ( sk_c9 = inverse(X0) )
| ( sk_c9 != iPr_def_13 )
| ( inverse(X0) != iPr_def_13 ) ),
inference(instantiation,[status(thm)],[c_1612]) ).
tcf(c_11481,plain,
! [X0: $i] :
( ( inverse(X0) = sk_c9 )
| ( sk_c9 != iPr_def_13 )
| ( inverse(X0) != iPr_def_13 ) ),
inference(instantiation,[status(thm)],[c_1402]) ).
tcf(c_11482,plain,
( ( inverse(sk_c10) = sk_c9 )
| ( sk_c9 != iPr_def_13 )
| ( inverse(sk_c10) != iPr_def_13 ) ),
inference(instantiation,[status(thm)],[c_11481]) ).
tcf(c_11483,plain,
( ( sk_c9 = inverse(sk_c10) )
| ( sk_c9 != iPr_def_13 )
| ( inverse(sk_c10) != iPr_def_13 ) ),
inference(instantiation,[status(thm)],[c_11480]) ).
tcf(c_11489,plain,
! [X0: $i] :
( ( inverse(sk_c1) = X0 )
| ( X0 != sk_c10 )
| ( inverse(sk_c1) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_1244]) ).
tcf(c_11515,plain,
( ( inverse(sk_c1) = iPr_def_15 )
| ( iPr_def_15 != iPr_def_26 )
| ( inverse(sk_c1) != iPr_def_26 ) ),
inference(instantiation,[status(thm)],[c_4348]) ).
tcf(c_11516,plain,
! [X0: $i] :
( ( X0 = inverse(sk_c1) )
| ( X0 != iPr_def_15 )
| ( inverse(sk_c1) != iPr_def_15 ) ),
inference(instantiation,[status(thm)],[c_1614]) ).
tcf(c_11517,plain,
( ( sk_c10 = inverse(sk_c1) )
| ( sk_c10 != iPr_def_15 )
| ( inverse(sk_c1) != iPr_def_15 ) ),
inference(instantiation,[status(thm)],[c_1455]) ).
tcf(c_11518,plain,
! [X0: $i] :
( ( inverse(sk_c1) = X0 )
| ( X0 != iPr_def_15 )
| ( inverse(sk_c1) != iPr_def_15 ) ),
inference(instantiation,[status(thm)],[c_1456]) ).
tcf(c_11519,plain,
( ( inverse(sk_c1) = sk_c10 )
| ( sk_c10 != iPr_def_15 )
| ( inverse(sk_c1) != iPr_def_15 ) ),
inference(instantiation,[status(thm)],[c_1457]) ).
tcf(c_11522,plain,
! [X0: $i] :
( ( X0 = inverse(sk_c1) )
| ( X0 != iPr_def_19 )
| ( inverse(sk_c1) != iPr_def_19 ) ),
inference(instantiation,[status(thm)],[c_1615]) ).
tcf(c_12419,plain,
( ( sk_c9 = iPr_def_17 )
| ( multiply(iPr_def_23,iPr_def_24) = iPr_def_23 ) ),
inference(superposition,[status(thm)],[c_1575,c_3606]) ).
tcf(c_12420,plain,
( ( sk_c3 = iPr_def_23 )
| ( sk_c9 = iPr_def_17 ) ),
inference(light_normalisation,[status(thm)],[c_12419,c_7816]) ).
tcf(c_12527,plain,
! [X0: $i,X1: $i] :
( ( sk_c9 = X0 )
| ( sk_c9 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_666]) ).
tcf(c_12528,plain,
( ( sk_c10 = sk_c9 )
| ( sk_c9 != iPr_def_13 )
| ( sk_c10 != iPr_def_13 ) ),
inference(instantiation,[status(thm)],[c_3786]) ).
tcf(c_12545,plain,
( ( sk_c10 = iPr_def_18 )
| ( multiply(iPr_def_23,iPr_def_24) = iPr_def_23 ) ),
inference(superposition,[status(thm)],[c_1591,c_3606]) ).
tcf(c_12546,plain,
( ( sk_c3 = iPr_def_23 )
| ( sk_c10 = iPr_def_18 ) ),
inference(light_normalisation,[status(thm)],[c_12545,c_7816]) ).
tcf(c_12641,plain,
( ( iPr_def_26 = sk_c9 )
| ( iPr_def_26 != iPr_def_13 )
| ( sk_c9 != iPr_def_13 ) ),
inference(instantiation,[status(thm)],[c_6899]) ).
tcf(c_12654,plain,
! [X0: $i] :
( ( X0 = sk_c9 )
| ( sk_c9 != iPr_def_13 )
| ( X0 != iPr_def_13 ) ),
inference(instantiation,[status(thm)],[c_3800]) ).
tcf(c_12680,plain,
! [X0: $i] :
( ( iPr_def_15 = iPr_def_14 )
| ( iPr_def_15 != X0 )
| ( iPr_def_14 != X0 ) ),
inference(instantiation,[status(thm)],[c_666]) ).
tcf(c_12702,plain,
! [X0: $i] :
( ( iPr_def_14 = iPr_def_15 )
| ( iPr_def_15 != X0 )
| ( iPr_def_14 != X0 ) ),
inference(instantiation,[status(thm)],[c_666]) ).
tcf(c_12809,plain,
( ( sk_c10 = iPr_def_13 )
| ( iPr_def_13 != inverse(sk_c1) )
| ( sk_c10 != inverse(sk_c1) ) ),
inference(instantiation,[status(thm)],[c_3689]) ).
tcf(c_12899,plain,
( ( sk_c9 = iPr_def_13 )
| ( multiply(iPr_def_23,iPr_def_24) = iPr_def_23 ) ),
inference(superposition,[status(thm)],[c_1622,c_3606]) ).
tcf(c_12900,plain,
( ( sk_c3 = iPr_def_23 )
| ( sk_c9 = iPr_def_13 ) ),
inference(light_normalisation,[status(thm)],[c_12899,c_7816]) ).
tcf(c_13039,plain,
( ( sk_c10 = sk_c9 )
| ( sk_c9 != inverse(sk_c1) )
| ( sk_c10 != inverse(sk_c1) ) ),
inference(instantiation,[status(thm)],[c_3786]) ).
tcf(c_13080,plain,
( ( identity = iPr_def_20 )
| ( sk_c10 = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_9031,c_623]) ).
tcf(c_13185,plain,
( ( identity = iPr_def_20 )
| ( multiply(sk_c7,iPr_def_14) = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_13080,c_600]) ).
tcf(c_13327,plain,
( iPr_def_12
| iPr_def_11
| iPr_def_10
| ( sk_c10 = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_664,c_611]) ).
tcf(c_13383,plain,
! [X0: $i] :
( ( iPr_def_14 = iPr_def_19 )
| ( iPr_def_19 != X0 )
| ( iPr_def_14 != X0 ) ),
inference(instantiation,[status(thm)],[c_666]) ).
tcf(c_13384,plain,
( ( iPr_def_14 = iPr_def_19 )
| ( iPr_def_19 != sk_c10 )
| ( iPr_def_14 != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_13383]) ).
tcf(c_13480,plain,
( ( iPr_def_15 = iPr_def_25 )
| ( sk_c9 = iPr_def_24 )
| ( multiply(iPr_def_14,iPr_def_16) = iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_2007,c_1722]) ).
tcf(c_13556,plain,
( ( iPr_def_15 = iPr_def_25 )
| ( sk_c9 = iPr_def_24 )
| ( sk_c10 = iPr_def_17 ) ),
inference(light_normalisation,[status(thm)],[c_13480,c_7821]) ).
tcf(c_13705,plain,
( ( sk_c9 = iPr_def_17 )
| ( multiply(iPr_def_26,iPr_def_25) = iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_1755,c_3610]) ).
tcf(c_13706,plain,
( ( sk_c9 = iPr_def_24 )
| ( sk_c9 = iPr_def_17 ) ),
inference(light_normalisation,[status(thm)],[c_13705,c_8144]) ).
tcf(c_13838,plain,
( ( sk_c10 = iPr_def_18 )
| ( multiply(iPr_def_26,iPr_def_25) = iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_1813,c_3610]) ).
tcf(c_13839,plain,
( ( sk_c9 = iPr_def_24 )
| ( sk_c10 = iPr_def_18 ) ),
inference(light_normalisation,[status(thm)],[c_13838,c_8144]) ).
tcf(c_13924,plain,
( ( sk_c9 = iPr_def_13 )
| ( multiply(iPr_def_26,iPr_def_25) = iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_1956,c_3610]) ).
tcf(c_13925,plain,
( ( sk_c9 = iPr_def_24 )
| ( sk_c9 = iPr_def_13 ) ),
inference(light_normalisation,[status(thm)],[c_13924,c_8144]) ).
tcf(c_14734,plain,
( ( sk_c10 = iPr_def_18 )
| ( multiply(iPr_def_15,iPr_def_20) = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_2218,c_3605]) ).
tcf(c_14735,plain,
( ( sk_c10 = iPr_def_25 )
| ( sk_c10 = iPr_def_18 ) ),
inference(light_normalisation,[status(thm)],[c_14734,c_7811]) ).
tcf(c_14841,plain,
( ( sk_c10 = iPr_def_19 )
| ( multiply(iPr_def_15,iPr_def_20) = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_2262,c_3605]) ).
tcf(c_14842,plain,
( ( sk_c10 = iPr_def_25 )
| ( sk_c10 = iPr_def_19 ) ),
inference(light_normalisation,[status(thm)],[c_14841,c_7811]) ).
tcf(c_14895,plain,
( ( sk_c10 = iPr_def_25 )
| ( multiply(iPr_def_26,iPr_def_25) = iPr_def_13 ) ),
inference(superposition,[status(thm)],[c_2392,c_3610]) ).
tcf(c_14896,plain,
( ( sk_c9 = iPr_def_13 )
| ( sk_c10 = iPr_def_25 ) ),
inference(light_normalisation,[status(thm)],[c_14895,c_8144]) ).
tcf(c_15430,plain,
( ( iPr_def_15 = inverse(sk_c1) )
| ( iPr_def_15 != inverse(sk_c4) )
| ( inverse(sk_c1) != inverse(sk_c4) ) ),
inference(instantiation,[status(thm)],[c_2197]) ).
tcf(c_15440,plain,
( ( inverse(sk_c1) = iPr_def_19 )
| ( iPr_def_19 != inverse(sk_c6) )
| ( inverse(sk_c1) != inverse(sk_c6) ) ),
inference(instantiation,[status(thm)],[c_1348]) ).
tcf(c_15655,plain,
( ( sk_c10 = iPr_def_18 )
| ( multiply(iPr_def_15,iPr_def_20) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_2796,c_3605]) ).
tcf(c_15656,plain,
( ( sk_c10 = iPr_def_26 )
| ( sk_c10 = iPr_def_18 ) ),
inference(light_normalisation,[status(thm)],[c_15655,c_7811]) ).
tcf(c_15769,plain,
( ( sk_c10 = iPr_def_19 )
| ( multiply(iPr_def_15,iPr_def_20) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_2917,c_3605]) ).
tcf(c_15770,plain,
( ( sk_c10 = iPr_def_26 )
| ( sk_c10 = iPr_def_19 ) ),
inference(light_normalisation,[status(thm)],[c_15769,c_7811]) ).
tcf(c_15822,plain,
( ( sk_c10 = iPr_def_26 )
| ( multiply(iPr_def_26,iPr_def_25) = iPr_def_13 ) ),
inference(superposition,[status(thm)],[c_3012,c_3610]) ).
tcf(c_15823,plain,
( ( sk_c9 = iPr_def_13 )
| ( sk_c10 = iPr_def_26 ) ),
inference(light_normalisation,[status(thm)],[c_15822,c_8144]) ).
tcf(c_17681,plain,
! [X0: $i] :
( ( X0 = identity )
| ( identity != inverse(sk_c7) )
| ( X0 != inverse(sk_c7) ) ),
inference(instantiation,[status(thm)],[c_3094]) ).
tcf(c_17682,plain,
( ( sk_c10 = identity )
| ( identity != inverse(sk_c7) )
| ( sk_c10 != inverse(sk_c7) ) ),
inference(instantiation,[status(thm)],[c_17681]) ).
tcf(c_18232,plain,
( iPr_def_12
| iPr_def_11
| ( iPr_def_13 != iPr_def_21 )
| ( sk_c9 = iPr_def_13 ) ),
inference(global_subsumption_just,[status(thm)],[c_1256,c_1256,c_3158,c_14896,c_15823]) ).
tcf(c_18233,plain,
( iPr_def_12
| iPr_def_11
| ( sk_c9 = iPr_def_13 )
| ( iPr_def_13 != iPr_def_21 ) ),
inference(renaming,[status(thm)],[c_18232]) ).
tcf(c_18322,plain,
( iPr_def_12
| iPr_def_11
| ( sk_c10 = iPr_def_26 ) ),
inference(global_subsumption_just,[status(thm)],[c_13327,c_2675,c_2997,c_3162,c_15656,c_15770]) ).
tcf(c_21284,plain,
( iPr_def_12
| iPr_def_11
| ( iPr_def_13 != iPr_def_24 )
| ( sk_c9 = iPr_def_13 ) ),
inference(global_subsumption_just,[status(thm)],[c_1962,c_1962,c_3158,c_14896,c_15823]) ).
tcf(c_21285,plain,
( iPr_def_12
| iPr_def_11
| ( sk_c9 = iPr_def_13 )
| ( iPr_def_13 != iPr_def_24 ) ),
inference(renaming,[status(thm)],[c_21284]) ).
tcf(c_21527,plain,
( iPr_def_12
| iPr_def_11
| ( sk_c10 = iPr_def_25 ) ),
inference(global_subsumption_just,[status(thm)],[c_2093,c_2397,c_3162,c_14735,c_14842]) ).
tcf(c_22649,plain,
! [X0: $i] :
( ( iPr_def_26 = X0 )
| ( iPr_def_26 != iPr_def_26 )
| ( X0 != iPr_def_26 ) ),
inference(instantiation,[status(thm)],[c_2737]) ).
tcf(c_22650,plain,
( ( iPr_def_26 = sk_c10 )
| ( iPr_def_26 != iPr_def_26 )
| ( sk_c10 != iPr_def_26 ) ),
inference(instantiation,[status(thm)],[c_22649]) ).
tcf(c_22713,plain,
( ( iPr_def_18 = iPr_def_19 )
| ( iPr_def_15 = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_3817,c_3816]) ).
tcf(c_23097,plain,
( ( iPr_def_18 = iPr_def_19 )
| ( iPr_def_15 = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_3820,c_3819]) ).
tcf(c_24266,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(X0,X1)) = X1,
inference(demodulation,[status(thm)],[c_3593,c_101]) ).
tcf(c_24313,plain,
! [X0: $i] : multiply(inverse(identity),X0) = X0,
inference(superposition,[status(thm)],[c_101,c_24266]) ).
tcf(c_24314,plain,
! [X0: $i] : multiply(inverse(inverse(X0)),identity) = X0,
inference(superposition,[status(thm)],[c_102,c_24266]) ).
tcf(c_24540,plain,
! [X0: $i] : multiply(inverse(iPr_def_26),X0) = multiply(sk_c1,X0),
inference(superposition,[status(thm)],[c_3610,c_24266]) ).
tcf(c_24541,plain,
! [X0: $i] : multiply(inverse(iPr_def_13),X0) = multiply(sk_c10,X0),
inference(superposition,[status(thm)],[c_3609,c_24266]) ).
tcf(c_24542,plain,
! [X0: $i] : multiply(inverse(iPr_def_19),X0) = multiply(sk_c6,X0),
inference(superposition,[status(thm)],[c_3608,c_24266]) ).
tcf(c_24543,plain,
! [X0: $i] : multiply(inverse(iPr_def_14),X0) = multiply(sk_c7,X0),
inference(superposition,[status(thm)],[c_3607,c_24266]) ).
tcf(c_24544,plain,
! [X0: $i] : multiply(inverse(iPr_def_23),X0) = multiply(sk_c2,X0),
inference(superposition,[status(thm)],[c_3606,c_24266]) ).
tcf(c_24545,plain,
! [X0: $i] : multiply(inverse(iPr_def_15),X0) = multiply(sk_c4,X0),
inference(superposition,[status(thm)],[c_3605,c_24266]) ).
tcf(c_24615,plain,
! [X0: $i,X1: $i] : multiply(inverse(inverse(X0)),X1) = multiply(X0,X1),
inference(superposition,[status(thm)],[c_24266,c_24266]) ).
tcf(c_26068,plain,
! [X0: $i] : multiply(X0,identity) = X0,
inference(demodulation,[status(thm)],[c_24314,c_24615]) ).
tcf(c_26097,plain,
inverse(identity) = identity,
inference(superposition,[status(thm)],[c_26068,c_24313]) ).
tcf(c_26157,plain,
( ~ iPr_def_11
| ( multiply(identity,identity) != sk_c9 )
| ( multiply(inverse(identity),sk_c10) != sk_c9 ) ),
inference(superposition,[status(thm)],[c_26097,c_614]) ).
tcf(c_26160,plain,
( ~ iPr_def_11
| ( multiply(identity,identity) != sk_c9 )
| ( multiply(identity,sk_c10) != sk_c9 ) ),
inference(light_normalisation,[status(thm)],[c_26157,c_26097]) ).
tcf(c_26721,plain,
multiply(sk_c1,identity) = inverse(iPr_def_26),
inference(superposition,[status(thm)],[c_24540,c_26068]) ).
tcf(c_26891,plain,
inverse(iPr_def_26) = sk_c1,
inference(demodulation,[status(thm)],[c_26721,c_26068]) ).
tcf(c_26894,plain,
( ( sk_c10 = iPr_def_19 )
| ( sk_c1 = iPr_def_13 ) ),
inference(demodulation,[status(thm)],[c_2920,c_26891]) ).
tcf(c_26895,plain,
( ( sk_c10 = iPr_def_18 )
| ( sk_c1 = iPr_def_13 ) ),
inference(demodulation,[status(thm)],[c_2799,c_26891]) ).
tcf(c_26896,plain,
( ( sk_c10 = iPr_def_14 )
| ( sk_c1 = iPr_def_13 ) ),
inference(demodulation,[status(thm)],[c_2558,c_26891]) ).
tcf(c_26905,plain,
( ( iPr_def_18 = iPr_def_19 )
| ( inverse(iPr_def_15) = sk_c1 ) ),
inference(superposition,[status(thm)],[c_22713,c_26891]) ).
tcf(c_27408,plain,
( ( sk_c10 = iPr_def_19 )
| ( multiply(iPr_def_13,iPr_def_21) = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_26894,c_1220]) ).
tcf(c_27424,plain,
( ( sk_c5 = iPr_def_25 )
| ( sk_c10 = iPr_def_19 ) ),
inference(light_normalisation,[status(thm)],[c_27408,c_7958]) ).
tcf(c_27585,plain,
( ( sk_c10 = iPr_def_18 )
| ( multiply(iPr_def_13,iPr_def_21) = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_26895,c_1193]) ).
tcf(c_27600,plain,
( ( sk_c5 = iPr_def_25 )
| ( sk_c10 = iPr_def_18 ) ),
inference(light_normalisation,[status(thm)],[c_27585,c_7958]) ).
tcf(c_27757,plain,
( ( sk_c10 = iPr_def_14 )
| ( multiply(iPr_def_13,iPr_def_21) = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_26896,c_1161]) ).
tcf(c_27769,plain,
( ( sk_c5 = iPr_def_25 )
| ( sk_c10 = iPr_def_14 ) ),
inference(light_normalisation,[status(thm)],[c_27757,c_7958]) ).
tcf(c_27858,plain,
( ( iPr_def_20 = iPr_def_25 )
| ( sk_c10 = iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_27424,c_627]) ).
tcf(c_28040,plain,
( ( iPr_def_20 = iPr_def_25 )
| ( sk_c10 = iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_27600,c_626]) ).
tcf(c_28282,plain,
( ( iPr_def_20 = iPr_def_25 )
| ( sk_c10 = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_27769,c_623]) ).
tcf(c_28705,plain,
( ( sk_c10 = inverse(sk_c7) )
| ( sk_c10 != inverse(sk_c4) )
| ( inverse(sk_c7) != inverse(sk_c4) ) ),
inference(instantiation,[status(thm)],[c_4220]) ).
tcf(c_28817,plain,
( ( iPr_def_20 = iPr_def_25 )
| ( iPr_def_18 = iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_28040,c_27858]) ).
tcf(c_29252,plain,
( ( iPr_def_20 = iPr_def_25 )
| ( iPr_def_14 = iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_28282,c_27858]) ).
tcf(c_29942,plain,
( ( inverse(sk_c6) = iPr_def_15 )
| ( iPr_def_15 != iPr_def_14 )
| ( inverse(sk_c6) != iPr_def_14 ) ),
inference(instantiation,[status(thm)],[c_5826]) ).
tcf(c_30063,plain,
( ( iPr_def_18 = iPr_def_19 )
| ( iPr_def_15 = iPr_def_20 ) ),
inference(superposition,[status(thm)],[c_28817,c_23097]) ).
tcf(c_30264,plain,
! [X0: $i] :
( ( X0 = sk_c4 )
| ( sk_c4 != inverse(sk_c4) )
| ( X0 != inverse(sk_c4) ) ),
inference(instantiation,[status(thm)],[c_3282]) ).
tcf(c_30265,plain,
( ( sk_c10 = sk_c4 )
| ( sk_c4 != inverse(sk_c4) )
| ( sk_c10 != inverse(sk_c4) ) ),
inference(instantiation,[status(thm)],[c_30264]) ).
tcf(c_31160,plain,
( ( iPr_def_13 = sk_c9 )
| ( iPr_def_13 != iPr_def_13 )
| ( sk_c9 != iPr_def_13 ) ),
inference(instantiation,[status(thm)],[c_6651]) ).
tcf(c_31355,plain,
multiply(sk_c10,iPr_def_13) = identity,
inference(superposition,[status(thm)],[c_24541,c_102]) ).
tcf(c_31358,plain,
! [X0: $i] : multiply(sk_c10,multiply(iPr_def_13,X0)) = X0,
inference(superposition,[status(thm)],[c_24541,c_24266]) ).
tcf(c_31359,plain,
multiply(sk_c10,identity) = inverse(iPr_def_13),
inference(superposition,[status(thm)],[c_24541,c_26068]) ).
tcf(c_31646,plain,
multiply(sk_c4,identity) = multiply(iPr_def_20,iPr_def_13),
inference(superposition,[status(thm)],[c_31355,c_3591]) ).
tcf(c_31647,plain,
multiply(sk_c3,identity) = multiply(iPr_def_22,iPr_def_13),
inference(superposition,[status(thm)],[c_31355,c_3589]) ).
tcf(c_31648,plain,
multiply(sk_c7,identity) = multiply(iPr_def_16,iPr_def_13),
inference(superposition,[status(thm)],[c_31355,c_3586]) ).
tcf(c_31827,plain,
inverse(iPr_def_13) = sk_c10,
inference(demodulation,[status(thm)],[c_31359,c_26068]) ).
tcf(c_31834,plain,
( ~ iPr_def_11
| ( multiply(iPr_def_13,sk_c10) != sk_c9 )
| ( multiply(inverse(iPr_def_13),sk_c10) != sk_c9 ) ),
inference(superposition,[status(thm)],[c_31827,c_614]) ).
tcf(c_31836,plain,
( ~ iPr_def_11
| ( sk_c9 != identity )
| ( multiply(sk_c10,sk_c10) != sk_c9 ) ),
inference(light_normalisation,[status(thm)],[c_31834,c_1173,c_31827]) ).
tcf(c_32404,plain,
multiply(sk_c10,sk_c8) = iPr_def_17,
inference(superposition,[status(thm)],[c_7957,c_31358]) ).
tcf(c_32405,plain,
multiply(sk_c10,sk_c5) = iPr_def_21,
inference(superposition,[status(thm)],[c_7958,c_31358]) ).
tcf(c_32412,plain,
( ~ iPr_def_12
| ( sk_c10 != sk_c9 )
| ( inverse(iPr_def_13) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_31358,c_613]) ).
tcf(c_32523,plain,
( ~ iPr_def_12
| ( sk_c10 != sk_c9 ) ),
inference(ground_joinability,[status(thm)],[c_32412,c_31827]) ).
tcf(c_32805,plain,
( ( sk_c10 = iPr_def_14 )
| ~ iPr_def_12
| ( sk_c10 != iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_647,c_32523]) ).
tcf(c_32815,plain,
( ( sk_c10 = iPr_def_14 )
| ~ iPr_def_12
| ( sk_c10 != iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_629,c_32523]) ).
tcf(c_34900,plain,
( ( sk_c10 = sk_c3 )
| ( sk_c3 != inverse(sk_c4) )
| ( sk_c10 != inverse(sk_c4) ) ),
inference(instantiation,[status(thm)],[c_10979]) ).
tcf(c_34903,plain,
( ( sk_c3 = inverse(sk_c4) )
| ( sk_c3 != iPr_def_15 )
| ( inverse(sk_c4) != iPr_def_15 ) ),
inference(instantiation,[status(thm)],[c_2464]) ).
tcf(c_35349,plain,
multiply(iPr_def_20,iPr_def_13) = sk_c4,
inference(demodulation,[status(thm)],[c_31646,c_26068]) ).
tcf(c_35484,plain,
multiply(iPr_def_22,iPr_def_13) = sk_c3,
inference(demodulation,[status(thm)],[c_31647,c_26068]) ).
tcf(c_35719,plain,
( ( sk_c10 = iPr_def_14 )
| ~ iPr_def_12 ),
inference(global_subsumption_just,[status(thm)],[c_32805,c_8742,c_32815]) ).
tcf(c_36249,plain,
( ( iPr_def_13 = iPr_def_21 )
| ( iPr_def_21 != iPr_def_13 )
| ( iPr_def_13 != iPr_def_13 ) ),
inference(instantiation,[status(thm)],[c_6651]) ).
tcf(c_36384,plain,
( ( iPr_def_13 = iPr_def_24 )
| ( iPr_def_24 != iPr_def_13 )
| ( iPr_def_13 != iPr_def_13 ) ),
inference(instantiation,[status(thm)],[c_6651]) ).
tcf(c_36798,plain,
! [X0: $i] :
( ( sk_c10 = sk_c9 )
| ( sk_c9 != inverse(X0) )
| ( sk_c10 != inverse(X0) ) ),
inference(instantiation,[status(thm)],[c_3786]) ).
tcf(c_36799,plain,
( ( sk_c10 = sk_c9 )
| ( sk_c9 != inverse(sk_c10) )
| ( sk_c10 != inverse(sk_c10) ) ),
inference(instantiation,[status(thm)],[c_36798]) ).
tcf(c_36802,plain,
( ( sk_c9 = inverse(sk_c1) )
| ( sk_c9 != iPr_def_13 )
| ( inverse(sk_c1) != iPr_def_13 ) ),
inference(instantiation,[status(thm)],[c_11480]) ).
tcf(c_36924,plain,
multiply(iPr_def_16,iPr_def_13) = sk_c7,
inference(demodulation,[status(thm)],[c_31648,c_26068]) ).
tcf(c_37364,plain,
! [X0: $i,X1: $i] :
( ( inverse(X0) = X1 )
| ( X1 != sk_c9 )
| ( inverse(X0) != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_1244]) ).
tcf(c_37711,plain,
multiply(sk_c6,iPr_def_19) = identity,
inference(superposition,[status(thm)],[c_24542,c_102]) ).
tcf(c_37714,plain,
! [X0: $i] : multiply(sk_c6,multiply(iPr_def_19,X0)) = X0,
inference(superposition,[status(thm)],[c_24542,c_24266]) ).
tcf(c_37715,plain,
multiply(sk_c6,identity) = inverse(iPr_def_19),
inference(superposition,[status(thm)],[c_24542,c_26068]) ).
tcf(c_37752,plain,
inverse(iPr_def_19) = sk_c6,
inference(demodulation,[status(thm)],[c_37715,c_26068]) ).
tcf(c_37759,plain,
( ( sk_c6 = iPr_def_13 )
| ( sk_c10 = iPr_def_15 ) ),
inference(demodulation,[status(thm)],[c_1006,c_37752]) ).
tcf(c_37911,plain,
( ( inverse(sk_c1) = inverse(sk_c4) )
| ( inverse(sk_c4) != sk_c10 )
| ( inverse(sk_c1) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_11489]) ).
tcf(c_37926,plain,
( ( inverse(sk_c1) = inverse(sk_c6) )
| ( inverse(sk_c6) != sk_c10 )
| ( inverse(sk_c1) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_11489]) ).
tcf(c_38190,plain,
multiply(sk_c6,sk_c9) = iPr_def_18,
inference(superposition,[status(thm)],[c_7829,c_37714]) ).
tcf(c_39264,plain,
( ( sk_c10 = iPr_def_15 )
| ( multiply(iPr_def_13,iPr_def_17) = iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_37759,c_1106]) ).
tcf(c_39277,plain,
( ( sk_c8 = iPr_def_18 )
| ( sk_c10 = iPr_def_15 ) ),
inference(light_normalisation,[status(thm)],[c_39264,c_7957]) ).
tcf(c_40036,plain,
! [X0: $i] :
( ( sk_c9 = X0 )
| ( sk_c9 != iPr_def_13 )
| ( X0 != iPr_def_13 ) ),
inference(instantiation,[status(thm)],[c_12527]) ).
tcf(c_40059,plain,
! [X0: $i] :
( ( sk_c9 = X0 )
| ( sk_c9 != sk_c9 )
| ( X0 != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_12527]) ).
tcf(c_40309,plain,
( ( iPr_def_16 = iPr_def_18 )
| ( sk_c10 = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_39277,c_618]) ).
tcf(c_40503,plain,
( ( iPr_def_16 = iPr_def_18 )
| ( iPr_def_15 = iPr_def_25 )
| ( sk_c10 = iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_40309,c_657]) ).
tcf(c_40825,negated_conjecture,
( iPr_def_12
| iPr_def_11
| ( iPr_def_13 != sk_c9 ) ),
inference(global_subsumption_just,[status(thm)],[c_611,c_611,c_3158,c_18322,c_21527]) ).
tcf(c_40936,plain,
( iPr_def_12
| iPr_def_11
| ( sk_c10 = iPr_def_14 )
| ( iPr_def_13 != iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_629,c_40825]) ).
tcf(c_41272,plain,
( ( sk_c10 = iPr_def_14 )
| ( multiply(iPr_def_15,sk_c5) = iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_617,c_605]) ).
tcf(c_41452,plain,
( ( iPr_def_21 = iPr_def_24 )
| ( sk_c10 = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_647,c_629]) ).
tcf(c_41455,plain,
( iPr_def_12
| iPr_def_11
| ( sk_c10 = iPr_def_14 )
| ( iPr_def_13 != iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_647,c_40825]) ).
tcf(c_41530,plain,
multiply(iPr_def_13,sk_c10) = identity,
inference(superposition,[status(thm)],[c_597,c_102]) ).
tcf(c_41534,plain,
multiply(iPr_def_15,sk_c4) = identity,
inference(superposition,[status(thm)],[c_599,c_102]) ).
tcf(c_41727,plain,
( ( iPr_def_21 = iPr_def_24 )
| ( sk_c10 = iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_651,c_633]) ).
tcf(c_42087,plain,
( iPr_def_12
| iPr_def_11
| ( sk_c10 = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_658,c_40825]) ).
tcf(c_42551,plain,
( ~ iPr_def_10
| ( sk_c10 != iPr_def_25 )
| ( inverse(sk_c1) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_609,c_616]) ).
tcf(c_42578,plain,
( ~ iPr_def_10
| ( sk_c10 != iPr_def_26 )
| ( sk_c10 != iPr_def_25 ) ),
inference(light_normalisation,[status(thm)],[c_42551,c_610]) ).
tcf(c_42689,plain,
( ~ iPr_def_12
| ( inverse(sk_c7) != sk_c10 )
| ( multiply(sk_c10,iPr_def_16) != sk_c9 ) ),
inference(superposition,[status(thm)],[c_600,c_613]) ).
tcf(c_42691,plain,
( ~ iPr_def_12
| ( inverse(sk_c4) != sk_c10 )
| ( multiply(sk_c10,iPr_def_20) != sk_c9 ) ),
inference(superposition,[status(thm)],[c_604,c_613]) ).
tcf(c_42707,plain,
( ~ iPr_def_12
| ( sk_c10 != iPr_def_15 )
| ( multiply(sk_c10,iPr_def_20) != sk_c9 ) ),
inference(light_normalisation,[status(thm)],[c_42691,c_599]) ).
tcf(c_42714,plain,
( ~ iPr_def_12
| ( sk_c10 != iPr_def_14 )
| ( multiply(sk_c10,iPr_def_16) != sk_c9 ) ),
inference(light_normalisation,[status(thm)],[c_42689,c_598]) ).
tcf(c_42766,plain,
( ~ iPr_def_11
| ( multiply(sk_c10,iPr_def_13) != sk_c9 )
| ( multiply(inverse(sk_c10),sk_c10) != sk_c9 ) ),
inference(superposition,[status(thm)],[c_597,c_614]) ).
tcf(c_42797,plain,
( ~ iPr_def_11
| ( sk_c9 != identity )
| ( multiply(sk_c10,iPr_def_13) != sk_c9 ) ),
inference(light_normalisation,[status(thm)],[c_42766,c_597,c_41530]) ).
tcf(c_42912,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(X0,X1)) = multiply(identity,X1),
inference(superposition,[status(thm)],[c_102,c_103]) ).
tcf(c_43865,plain,
! [X0: $i] : multiply(iPr_def_15,multiply(sk_c4,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_41534,c_103]) ).
tcf(c_43866,plain,
! [X0: $i] : multiply(iPr_def_15,multiply(sk_c4,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_43865,c_101]) ).
tcf(c_44689,plain,
( ( iPr_def_21 = iPr_def_24 )
| ( iPr_def_14 = iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_41727,c_41452]) ).
tcf(c_45140,plain,
multiply(sk_c7,iPr_def_14) = identity,
inference(superposition,[status(thm)],[c_24543,c_102]) ).
tcf(c_45144,plain,
multiply(sk_c7,identity) = inverse(iPr_def_14),
inference(superposition,[status(thm)],[c_24543,c_26068]) ).
tcf(c_45181,plain,
( ( identity = iPr_def_20 )
| ( identity = iPr_def_16 ) ),
inference(demodulation,[status(thm)],[c_13185,c_45140]) ).
tcf(c_45185,plain,
( ( iPr_def_15 = iPr_def_26 )
| ( identity = iPr_def_16 ) ),
inference(demodulation,[status(thm)],[c_6953,c_45140]) ).
tcf(c_45187,plain,
( ( iPr_def_15 = iPr_def_25 )
| ( identity = iPr_def_16 ) ),
inference(demodulation,[status(thm)],[c_6374,c_45140]) ).
tcf(c_45328,plain,
inverse(iPr_def_14) = sk_c7,
inference(demodulation,[status(thm)],[c_45144,c_26068]) ).
tcf(c_45367,plain,
( ~ iPr_def_11
| ( multiply(iPr_def_14,sk_c7) != sk_c9 )
| ( multiply(inverse(iPr_def_14),sk_c10) != sk_c9 ) ),
inference(superposition,[status(thm)],[c_45328,c_614]) ).
tcf(c_45369,plain,
( ~ iPr_def_11
| ( sk_c9 != iPr_def_16 )
| ( sk_c9 != identity ) ),
inference(light_normalisation,[status(thm)],[c_45367,c_600,c_1175,c_45328]) ).
tcf(c_45781,plain,
! [X0: $i] :
( ( identity = iPr_def_16 )
| ( multiply(iPr_def_20,X0) = X0 ) ),
inference(superposition,[status(thm)],[c_45181,c_101]) ).
tcf(c_45963,plain,
! [X0: $i] :
( ( iPr_def_15 = iPr_def_26 )
| ( multiply(X0,iPr_def_16) = X0 ) ),
inference(superposition,[status(thm)],[c_45185,c_26068]) ).
tcf(c_45972,plain,
( ( iPr_def_15 = iPr_def_26 )
| ( multiply(sk_c10,iPr_def_16) = sk_c10 ) ),
inference(instantiation,[status(thm)],[c_45963]) ).
tcf(c_46155,plain,
! [X0: $i] :
( ( iPr_def_15 = iPr_def_25 )
| ( multiply(X0,iPr_def_16) = X0 ) ),
inference(superposition,[status(thm)],[c_45187,c_26068]) ).
tcf(c_46164,plain,
( ( iPr_def_15 = iPr_def_25 )
| ( multiply(sk_c10,iPr_def_16) = sk_c10 ) ),
inference(instantiation,[status(thm)],[c_46155]) ).
tcf(c_47870,plain,
( ( iPr_def_13 = inverse(sk_c1) )
| ( iPr_def_13 != iPr_def_15 )
| ( inverse(sk_c1) != iPr_def_15 ) ),
inference(instantiation,[status(thm)],[c_11516]) ).
tcf(c_48416,plain,
( ( inverse(sk_c1) = iPr_def_13 )
| ( iPr_def_13 != iPr_def_15 )
| ( inverse(sk_c1) != iPr_def_15 ) ),
inference(instantiation,[status(thm)],[c_11518]) ).
tcf(c_48656,plain,
( ( iPr_def_13 = inverse(sk_c1) )
| ( iPr_def_13 != iPr_def_19 )
| ( inverse(sk_c1) != iPr_def_19 ) ),
inference(instantiation,[status(thm)],[c_11522]) ).
tcf(c_48919,plain,
( ( iPr_def_15 = iPr_def_14 )
| ( iPr_def_15 != iPr_def_15 )
| ( iPr_def_14 != iPr_def_15 ) ),
inference(instantiation,[status(thm)],[c_12680]) ).
tcf(c_48920,plain,
iPr_def_15 = iPr_def_15,
inference(instantiation,[status(thm)],[c_665]) ).
tcf(c_48924,plain,
( ( iPr_def_15 = iPr_def_26 )
| ( iPr_def_26 != inverse(sk_c1) )
| ( iPr_def_15 != inverse(sk_c1) ) ),
inference(instantiation,[status(thm)],[c_2974]) ).
tcf(c_49959,plain,
multiply(sk_c2,iPr_def_23) = identity,
inference(superposition,[status(thm)],[c_24544,c_102]) ).
tcf(c_49974,plain,
( ( identity = iPr_def_24 )
| ( sk_c10 = iPr_def_19 ) ),
inference(demodulation,[status(thm)],[c_1601,c_49959]) ).
tcf(c_49975,plain,
( ( identity = iPr_def_24 )
| ( sk_c10 = iPr_def_18 ) ),
inference(demodulation,[status(thm)],[c_1591,c_49959]) ).
tcf(c_49976,plain,
( ( identity = iPr_def_24 )
| ( sk_c9 = iPr_def_17 ) ),
inference(demodulation,[status(thm)],[c_1575,c_49959]) ).
tcf(c_49977,plain,
( ( identity = iPr_def_24 )
| ( sk_c10 = iPr_def_14 ) ),
inference(demodulation,[status(thm)],[c_1558,c_49959]) ).
tcf(c_50454,plain,
( ( identity = iPr_def_24 )
| ( inverse(iPr_def_19) = iPr_def_13 ) ),
inference(superposition,[status(thm)],[c_49974,c_597]) ).
tcf(c_50457,plain,
( ( identity = iPr_def_24 )
| ( sk_c6 = iPr_def_13 ) ),
inference(light_normalisation,[status(thm)],[c_50454,c_37752]) ).
tcf(c_51447,plain,
( ( identity = iPr_def_24 )
| ( multiply(sk_c6,iPr_def_17) = iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_49976,c_602]) ).
tcf(c_51618,plain,
( ( iPr_def_14 = iPr_def_19 )
| ( identity = iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_49977,c_49974]) ).
tcf(c_51710,plain,
( ( identity = iPr_def_24 )
| ( multiply(sk_c7,iPr_def_14) = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_49977,c_600]) ).
tcf(c_51722,plain,
( ( identity = iPr_def_24 )
| ( identity = iPr_def_16 ) ),
inference(light_normalisation,[status(thm)],[c_51710,c_45140]) ).
tcf(c_53251,plain,
( ( iPr_def_15 = iPr_def_26 )
| ( sk_c10 = iPr_def_19 ) ),
inference(global_subsumption_just,[status(thm)],[c_5573,c_599,c_610,c_1987,c_1988,c_2156,c_2157,c_2467,c_4262,c_8677,c_15430,c_15770,c_37911,c_48924]) ).
tcf(c_53375,plain,
( ( iPr_def_15 = iPr_def_26 )
| ( iPr_def_14 = iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_53251,c_2561]) ).
tcf(c_53400,plain,
( ( iPr_def_15 = iPr_def_26 )
| ( inverse(iPr_def_19) = iPr_def_13 ) ),
inference(superposition,[status(thm)],[c_53251,c_597]) ).
tcf(c_53405,plain,
( ( iPr_def_15 = iPr_def_26 )
| ( sk_c6 = iPr_def_13 ) ),
inference(light_normalisation,[status(thm)],[c_53400,c_37752]) ).
tcf(c_53598,plain,
( ( iPr_def_20 = iPr_def_24 )
| ( identity = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_51722,c_45181]) ).
tcf(c_54411,plain,
multiply(iPr_def_15,iPr_def_20) = sk_c10,
inference(superposition,[status(thm)],[c_604,c_43866]) ).
tcf(c_55108,plain,
( ( sk_c10 = iPr_def_15 )
| ( iPr_def_14 = iPr_def_19 ) ),
inference(global_subsumption_just,[status(thm)],[c_6376,c_671,c_617,c_621,c_3951,c_13384]) ).
tcf(c_55109,plain,
( ( iPr_def_14 = iPr_def_19 )
| ( sk_c10 = iPr_def_15 ) ),
inference(renaming,[status(thm)],[c_55108]) ).
tcf(c_55238,plain,
( ( iPr_def_14 = iPr_def_19 )
| ( sk_c9 = iPr_def_13 )
| ( multiply(iPr_def_15,iPr_def_20) = iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_55109,c_1127]) ).
tcf(c_55271,plain,
( ( iPr_def_14 = iPr_def_19 )
| ( inverse(iPr_def_15) = iPr_def_13 ) ),
inference(superposition,[status(thm)],[c_55109,c_597]) ).
tcf(c_55363,plain,
( ( iPr_def_14 = iPr_def_19 )
| ( sk_c9 = iPr_def_13 )
| ( sk_c10 = iPr_def_21 ) ),
inference(light_normalisation,[status(thm)],[c_55238,c_7811]) ).
tcf(c_55520,plain,
! [X0: $i,X1: $i] :
( ( inverse(X0) = iPr_def_15 )
| ( iPr_def_15 != X1 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_1244]) ).
tcf(c_56623,plain,
( ( sk_c10 = iPr_def_14 )
| ( multiply(iPr_def_15,iPr_def_20) = iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_623,c_41272]) ).
tcf(c_56625,plain,
( ( sk_c10 = iPr_def_21 )
| ( sk_c10 = iPr_def_14 ) ),
inference(light_normalisation,[status(thm)],[c_56623,c_54411]) ).
tcf(c_56731,plain,
( ( iPr_def_15 = iPr_def_26 )
| ( sk_c10 = iPr_def_18 ) ),
inference(global_subsumption_just,[status(thm)],[c_5574,c_599,c_610,c_1987,c_1988,c_2156,c_2157,c_2467,c_4262,c_7922,c_15430,c_15656,c_37911,c_48924]) ).
tcf(c_57601,plain,
( ( sk_c1 = sk_c9 )
| ( sk_c9 != iPr_def_13 )
| ( sk_c1 != iPr_def_13 ) ),
inference(instantiation,[status(thm)],[c_12654]) ).
tcf(c_57726,plain,
( ( iPr_def_14 = iPr_def_19 )
| ( inverse(iPr_def_15) = sk_c1 ) ),
inference(superposition,[status(thm)],[c_53375,c_26891]) ).
tcf(c_57760,plain,
( ( iPr_def_15 = iPr_def_25 )
| ( iPr_def_14 = iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_53375,c_7362]) ).
tcf(c_57899,plain,
( ( iPr_def_15 = iPr_def_26 )
| ( sk_c10 = iPr_def_26 )
| ( multiply(iPr_def_13,iPr_def_17) = iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_53405,c_2671]) ).
tcf(c_57954,plain,
( ( iPr_def_15 = iPr_def_26 )
| ( sk_c8 = iPr_def_18 )
| ( sk_c10 = iPr_def_26 ) ),
inference(light_normalisation,[status(thm)],[c_57899,c_7957]) ).
tcf(c_58910,plain,
( ( identity = iPr_def_16 )
| ( sk_c4 = iPr_def_13 ) ),
inference(superposition,[status(thm)],[c_45781,c_35349]) ).
tcf(c_59306,plain,
! [X0: $i] :
( ( iPr_def_20 = iPr_def_24 )
| ( multiply(iPr_def_16,X0) = X0 ) ),
inference(superposition,[status(thm)],[c_53598,c_101]) ).
tcf(c_59647,plain,
! [X0: $i] :
( ( iPr_def_21 = sk_c9 )
| ( iPr_def_21 != X0 )
| ( sk_c9 != X0 ) ),
inference(instantiation,[status(thm)],[c_3800]) ).
tcf(c_59659,plain,
! [X0: $i] :
( ( iPr_def_24 = sk_c9 )
| ( iPr_def_24 != X0 )
| ( sk_c9 != X0 ) ),
inference(instantiation,[status(thm)],[c_3800]) ).
tcf(c_59681,plain,
( ( iPr_def_15 = iPr_def_20 )
| ( iPr_def_14 = iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_57760,c_29252]) ).
tcf(c_60084,plain,
( ( iPr_def_14 = iPr_def_15 )
| ( iPr_def_15 != iPr_def_19 )
| ( iPr_def_14 != iPr_def_19 ) ),
inference(instantiation,[status(thm)],[c_12702]) ).
tcf(c_60205,plain,
( ( iPr_def_21 = iPr_def_26 )
| ( sk_c10 = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_56625,c_659]) ).
tcf(c_61795,plain,
( ( identity = iPr_def_16 )
| ( inverse(iPr_def_13) = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_58910,c_599]) ).
tcf(c_61796,plain,
( ( identity = iPr_def_16 )
| ( sk_c10 = iPr_def_15 ) ),
inference(light_normalisation,[status(thm)],[c_61795,c_31827]) ).
tcf(c_62128,plain,
( ( sk_c10 = iPr_def_13 )
| ( iPr_def_13 != iPr_def_17 )
| ( sk_c10 != iPr_def_17 ) ),
inference(instantiation,[status(thm)],[c_1707]) ).
tcf(c_62764,plain,
( ( iPr_def_21 = iPr_def_26 )
| ( iPr_def_14 = iPr_def_19 )
| ( sk_c10 = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_60205,c_621]) ).
tcf(c_62765,plain,
( ( iPr_def_21 = iPr_def_26 )
| ( iPr_def_14 = iPr_def_18 )
| ( sk_c10 = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_60205,c_620]) ).
tcf(c_63840,plain,
multiply(sk_c4,iPr_def_15) = identity,
inference(superposition,[status(thm)],[c_24545,c_102]) ).
tcf(c_63843,plain,
! [X0: $i] : multiply(sk_c4,multiply(iPr_def_15,X0)) = X0,
inference(superposition,[status(thm)],[c_24545,c_24266]) ).
tcf(c_63844,plain,
multiply(sk_c4,identity) = inverse(iPr_def_15),
inference(superposition,[status(thm)],[c_24545,c_26068]) ).
tcf(c_63869,plain,
( ( iPr_def_18 = iPr_def_19 )
| ( identity = iPr_def_20 ) ),
inference(demodulation,[status(thm)],[c_3825,c_63840]) ).
tcf(c_63892,plain,
inverse(iPr_def_15) = sk_c4,
inference(demodulation,[status(thm)],[c_63844,c_26068]) ).
tcf(c_63895,plain,
( ( iPr_def_14 = iPr_def_19 )
| ( sk_c4 = iPr_def_13 ) ),
inference(demodulation,[status(thm)],[c_55271,c_63892]) ).
tcf(c_63898,plain,
( ( iPr_def_18 = iPr_def_19 )
| ( sk_c4 = iPr_def_13 ) ),
inference(demodulation,[status(thm)],[c_3828,c_63892]) ).
tcf(c_63911,plain,
( ~ iPr_def_11
| ( multiply(iPr_def_15,sk_c4) != sk_c9 )
| ( multiply(inverse(iPr_def_15),sk_c10) != sk_c9 ) ),
inference(superposition,[status(thm)],[c_63892,c_614]) ).
tcf(c_63913,plain,
( ~ iPr_def_11
| ( sk_c9 != iPr_def_20 )
| ( sk_c9 != identity ) ),
inference(light_normalisation,[status(thm)],[c_63911,c_604,c_1177,c_63892]) ).
tcf(c_64448,plain,
( ( iPr_def_18 = iPr_def_19 )
| ( inverse(iPr_def_20) = iPr_def_20 ) ),
inference(superposition,[status(thm)],[c_63869,c_26097]) ).
tcf(c_64651,plain,
( ( iPr_def_14 = iPr_def_19 )
| ( multiply(iPr_def_13,sk_c10) = iPr_def_20 ) ),
inference(superposition,[status(thm)],[c_63895,c_604]) ).
tcf(c_64654,plain,
( ( iPr_def_14 = iPr_def_19 )
| ( identity = iPr_def_20 ) ),
inference(light_normalisation,[status(thm)],[c_64651,c_1173]) ).
tcf(c_65283,plain,
( ( iPr_def_20 = iPr_def_24 )
| ( iPr_def_14 = iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_64654,c_51618]) ).
tcf(c_65299,plain,
( ( iPr_def_14 = iPr_def_19 )
| ( inverse(iPr_def_20) = iPr_def_20 ) ),
inference(superposition,[status(thm)],[c_64654,c_26097]) ).
tcf(c_67016,plain,
( ( iPr_def_20 = iPr_def_21 )
| ( iPr_def_14 = iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_65283,c_5906]) ).
tcf(c_67018,plain,
( ( iPr_def_20 = iPr_def_22 )
| ( iPr_def_14 = iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_65283,c_5694]) ).
tcf(c_71305,plain,
( ( iPr_def_14 = iPr_def_19 )
| ( multiply(iPr_def_20,iPr_def_13) = sk_c3 ) ),
inference(superposition,[status(thm)],[c_67018,c_35484]) ).
tcf(c_71330,plain,
( ( iPr_def_14 = iPr_def_19 )
| ( sk_c3 = sk_c4 ) ),
inference(light_normalisation,[status(thm)],[c_71305,c_35349]) ).
tcf(c_72004,plain,
! [X0: $i] :
( ( inverse(X0) = iPr_def_21 )
| ( iPr_def_21 != sk_c9 )
| ( inverse(X0) != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_37364]) ).
tcf(c_72005,plain,
( ( inverse(sk_c10) = iPr_def_21 )
| ( iPr_def_21 != sk_c9 )
| ( inverse(sk_c10) != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_72004]) ).
tcf(c_72008,plain,
( ( sk_c9 = iPr_def_22 )
| ( iPr_def_22 != sk_c9 )
| ( sk_c9 != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_40059]) ).
tcf(c_72109,plain,
! [X0: $i] :
( ( inverse(X0) = iPr_def_24 )
| ( iPr_def_24 != sk_c9 )
| ( inverse(X0) != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_37364]) ).
tcf(c_72110,plain,
( ( inverse(sk_c10) = iPr_def_24 )
| ( iPr_def_24 != sk_c9 )
| ( inverse(sk_c10) != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_72109]) ).
tcf(c_72564,plain,
! [X0: $i] :
( ( X0 = iPr_def_13 )
| ( iPr_def_13 != iPr_def_24 )
| ( X0 != iPr_def_24 ) ),
inference(instantiation,[status(thm)],[c_1729]) ).
tcf(c_72858,plain,
! [X0: $i,X1: $i] :
( ( iPr_def_21 = inverse(X0) )
| ( iPr_def_21 != inverse(X1) )
| ( inverse(X0) != inverse(X1) ) ),
inference(instantiation,[status(thm)],[c_1609]) ).
tcf(c_72859,plain,
! [X0: $i,X1: $i] :
( ( inverse(X0) = iPr_def_21 )
| ( iPr_def_21 != inverse(X1) )
| ( inverse(X0) != inverse(X1) ) ),
inference(instantiation,[status(thm)],[c_1279]) ).
tcf(c_72860,plain,
( ( inverse(sk_c10) = iPr_def_21 )
| ( iPr_def_21 != inverse(sk_c10) )
| ( inverse(sk_c10) != inverse(sk_c10) ) ),
inference(instantiation,[status(thm)],[c_72859]) ).
tcf(c_72867,plain,
! [X0: $i,X1: $i] :
( ( X1 = inverse(X0) )
| ( X1 != iPr_def_21 )
| ( inverse(X0) != iPr_def_21 ) ),
inference(instantiation,[status(thm)],[c_1340]) ).
tcf(c_73406,plain,
! [X0: $i,X1: $i] :
( ( X1 = inverse(X0) )
| ( X1 != iPr_def_24 )
| ( inverse(X0) != iPr_def_24 ) ),
inference(instantiation,[status(thm)],[c_1340]) ).
tcf(c_73407,plain,
! [X0: $i,X1: $i] :
( ( inverse(X0) = X1 )
| ( X1 != iPr_def_24 )
| ( inverse(X0) != iPr_def_24 ) ),
inference(instantiation,[status(thm)],[c_1244]) ).
tcf(c_74515,plain,
! [X0: $i] :
( ( inverse(X0) = iPr_def_15 )
| ( iPr_def_15 != iPr_def_21 )
| ( inverse(X0) != iPr_def_21 ) ),
inference(instantiation,[status(thm)],[c_55520]) ).
tcf(c_74516,plain,
( ( inverse(sk_c10) = iPr_def_15 )
| ( iPr_def_15 != iPr_def_21 )
| ( inverse(sk_c10) != iPr_def_21 ) ),
inference(instantiation,[status(thm)],[c_74515]) ).
tcf(c_74519,plain,
! [X0: $i] :
( ( inverse(X0) = iPr_def_15 )
| ( iPr_def_15 != iPr_def_24 )
| ( inverse(X0) != iPr_def_24 ) ),
inference(instantiation,[status(thm)],[c_55520]) ).
tcf(c_74520,plain,
( ( inverse(sk_c10) = iPr_def_15 )
| ( iPr_def_15 != iPr_def_24 )
| ( inverse(sk_c10) != iPr_def_24 ) ),
inference(instantiation,[status(thm)],[c_74519]) ).
tcf(c_75105,plain,
! [X0: $i] : multiply(inverse(X0),sk_c10) = multiply(inverse(X0),sk_c10),
inference(instantiation,[status(thm)],[c_665]) ).
tcf(c_75107,plain,
multiply(inverse(sk_c10),sk_c10) = multiply(inverse(sk_c10),sk_c10),
inference(instantiation,[status(thm)],[c_75105]) ).
tcf(c_75131,plain,
( ( identity = iPr_def_24 )
| ( multiply(iPr_def_13,iPr_def_17) = iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_50457,c_51447]) ).
tcf(c_75142,plain,
( ( identity = iPr_def_24 )
| ( sk_c8 = iPr_def_18 ) ),
inference(light_normalisation,[status(thm)],[c_75131,c_7957]) ).
tcf(c_75893,plain,
( ( iPr_def_14 = iPr_def_19 )
| ( sk_c3 = iPr_def_13 ) ),
inference(superposition,[status(thm)],[c_71330,c_63895]) ).
tcf(c_76166,plain,
( ( iPr_def_16 = iPr_def_18 )
| ( identity = iPr_def_24 )
| ( sk_c3 = iPr_def_23 ) ),
inference(superposition,[status(thm)],[c_75142,c_642]) ).
tcf(c_78892,plain,
( ( sk_c9 = identity )
| ( identity != iPr_def_13 )
| ( sk_c9 != iPr_def_13 ) ),
inference(instantiation,[status(thm)],[c_40036]) ).
tcf(c_79716,plain,
! [X0: $i] :
( ( inverse(X0) = sk_c6 )
| ( sk_c6 != iPr_def_13 )
| ( inverse(X0) != iPr_def_13 ) ),
inference(instantiation,[status(thm)],[c_1402]) ).
tcf(c_79717,plain,
( ( inverse(sk_c10) = sk_c6 )
| ( sk_c6 != iPr_def_13 )
| ( inverse(sk_c10) != iPr_def_13 ) ),
inference(instantiation,[status(thm)],[c_79716]) ).
tcf(c_80136,plain,
( ( iPr_def_14 = iPr_def_19 )
| ( multiply(iPr_def_13,sk_c10) = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_75893,c_606]) ).
tcf(c_80137,plain,
( ( iPr_def_14 = iPr_def_19 )
| ( identity = iPr_def_22 ) ),
inference(light_normalisation,[status(thm)],[c_80136,c_1173]) ).
tcf(c_81907,plain,
( ( iPr_def_18 = iPr_def_19 )
| ( sk_c1 = sk_c4 ) ),
inference(light_normalisation,[status(thm)],[c_26905,c_63892]) ).
tcf(c_81929,plain,
( ( iPr_def_18 = iPr_def_19 )
| ( sk_c1 = iPr_def_13 ) ),
inference(superposition,[status(thm)],[c_81907,c_63898]) ).
tcf(c_82854,plain,
iPr_def_21 = iPr_def_21,
inference(instantiation,[status(thm)],[c_665]) ).
tcf(c_82855,plain,
! [X0: $i,X1: $i] :
( ( iPr_def_21 = X0 )
| ( iPr_def_21 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_666]) ).
tcf(c_82856,plain,
( ( iPr_def_21 = sk_c9 )
| ( iPr_def_21 != multiply(sk_c10,sk_c5) )
| ( sk_c9 != multiply(sk_c10,sk_c5) ) ),
inference(instantiation,[status(thm)],[c_59647]) ).
tcf(c_82860,plain,
! [X0: $i] :
( ( iPr_def_21 = iPr_def_26 )
| ( iPr_def_26 != X0 )
| ( iPr_def_21 != X0 ) ),
inference(instantiation,[status(thm)],[c_1855]) ).
tcf(c_82861,plain,
( ( iPr_def_21 = iPr_def_26 )
| ( iPr_def_26 != sk_c10 )
| ( iPr_def_21 != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_82860]) ).
tcf(c_83296,plain,
( ( iPr_def_24 = sk_c9 )
| ( iPr_def_24 != iPr_def_24 )
| ( sk_c9 != iPr_def_24 ) ),
inference(instantiation,[status(thm)],[c_59659]) ).
tcf(c_83297,plain,
iPr_def_24 = iPr_def_24,
inference(instantiation,[status(thm)],[c_665]) ).
tcf(c_85060,plain,
( ( identity = iPr_def_13 )
| ( iPr_def_13 != iPr_def_24 )
| ( identity != iPr_def_24 ) ),
inference(instantiation,[status(thm)],[c_72564]) ).
tcf(c_85558,plain,
! [X0: $i] :
( ( sk_c9 = multiply(inverse(X0),sk_c10) )
| ( sk_c9 != sk_c9 )
| ( multiply(inverse(X0),sk_c10) != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_40059]) ).
tcf(c_85561,plain,
( ( sk_c9 = multiply(inverse(sk_c10),sk_c10) )
| ( sk_c9 != sk_c9 )
| ( multiply(inverse(sk_c10),sk_c10) != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_85558]) ).
tcf(c_91650,plain,
! [X0: $i] :
( ( iPr_def_21 = iPr_def_13 )
| ( iPr_def_21 != X0 )
| ( iPr_def_13 != X0 ) ),
inference(instantiation,[status(thm)],[c_1729]) ).
tcf(c_91651,plain,
( ( iPr_def_21 = iPr_def_13 )
| ( iPr_def_21 != sk_c10 )
| ( iPr_def_13 != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_91650]) ).
tcf(c_91654,plain,
! [X0: $i] :
( ( iPr_def_24 = iPr_def_13 )
| ( iPr_def_24 != X0 )
| ( iPr_def_13 != X0 ) ),
inference(instantiation,[status(thm)],[c_1729]) ).
tcf(c_91702,plain,
! [X0: $i] :
( ( identity = iPr_def_13 )
| ( iPr_def_13 != X0 )
| ( identity != X0 ) ),
inference(instantiation,[status(thm)],[c_1729]) ).
tcf(c_91778,plain,
( iPr_def_12
| iPr_def_11
| ( iPr_def_13 != iPr_def_21 ) ),
inference(global_subsumption_just,[status(thm)],[c_40936,c_2170,c_18233,c_31160,c_40825]) ).
tcf(c_92865,plain,
( iPr_def_12
| iPr_def_11
| ( iPr_def_13 != iPr_def_24 ) ),
inference(global_subsumption_just,[status(thm)],[c_41455,c_2170,c_21285,c_31160,c_40825]) ).
tcf(c_95016,plain,
! [X0: $i] :
( ( iPr_def_21 = inverse(X0) )
| ( iPr_def_21 != iPr_def_26 )
| ( inverse(X0) != iPr_def_26 ) ),
inference(instantiation,[status(thm)],[c_1617]) ).
tcf(c_95024,plain,
( ( iPr_def_21 = inverse(sk_c10) )
| ( iPr_def_21 != iPr_def_26 )
| ( inverse(sk_c10) != iPr_def_26 ) ),
inference(instantiation,[status(thm)],[c_95016]) ).
tcf(c_95295,plain,
( ( iPr_def_20 = iPr_def_24 )
| ( sk_c7 = iPr_def_13 ) ),
inference(superposition,[status(thm)],[c_59306,c_36924]) ).
tcf(c_95508,plain,
( ( iPr_def_20 = iPr_def_24 )
| ( inverse(iPr_def_13) = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_95295,c_598]) ).
tcf(c_95509,plain,
( ( iPr_def_20 = iPr_def_24 )
| ( sk_c10 = iPr_def_14 ) ),
inference(light_normalisation,[status(thm)],[c_95508,c_31827]) ).
tcf(c_99164,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(X0,X1)) = X1,
inference(demodulation,[status(thm)],[c_42912,c_101]) ).
tcf(c_99213,plain,
! [X0: $i] : multiply(inverse(inverse(X0)),identity) = X0,
inference(superposition,[status(thm)],[c_102,c_99164]) ).
tcf(c_99507,plain,
! [X0: $i,X1: $i] : multiply(inverse(inverse(X0)),X1) = multiply(X0,X1),
inference(superposition,[status(thm)],[c_99164,c_99164]) ).
tcf(c_103996,plain,
! [X0: $i] :
( ( iPr_def_21 = inverse(X0) )
| ( iPr_def_21 != inverse(sk_c1) )
| ( inverse(X0) != inverse(sk_c1) ) ),
inference(instantiation,[status(thm)],[c_72858]) ).
tcf(c_103997,plain,
( ( iPr_def_21 = inverse(sk_c1) )
| ( iPr_def_21 != iPr_def_26 )
| ( inverse(sk_c1) != iPr_def_26 ) ),
inference(instantiation,[status(thm)],[c_6480]) ).
tcf(c_103999,plain,
( ( iPr_def_21 = inverse(sk_c10) )
| ( iPr_def_21 != inverse(sk_c1) )
| ( inverse(sk_c10) != inverse(sk_c1) ) ),
inference(instantiation,[status(thm)],[c_103996]) ).
tcf(c_104758,plain,
( ( iPr_def_14 = iPr_def_19 )
| ( sk_c1 = sk_c4 ) ),
inference(light_normalisation,[status(thm)],[c_57726,c_63892]) ).
tcf(c_104788,plain,
( ( iPr_def_14 = iPr_def_19 )
| ( sk_c1 = iPr_def_13 ) ),
inference(superposition,[status(thm)],[c_104758,c_63895]) ).
tcf(c_105175,plain,
( ( iPr_def_14 = iPr_def_19 )
| ( inverse(iPr_def_13) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_104788,c_610]) ).
tcf(c_105176,plain,
( ( iPr_def_14 = iPr_def_19 )
| ( sk_c10 = iPr_def_26 ) ),
inference(light_normalisation,[status(thm)],[c_105175,c_31827]) ).
tcf(c_106130,plain,
( ( iPr_def_16 = iPr_def_18 )
| ( iPr_def_15 = iPr_def_25 )
| ( inverse(iPr_def_19) = iPr_def_13 ) ),
inference(superposition,[status(thm)],[c_40503,c_597]) ).
tcf(c_106133,plain,
( ( iPr_def_16 = iPr_def_18 )
| ( iPr_def_15 = iPr_def_25 )
| ( sk_c6 = iPr_def_13 ) ),
inference(light_normalisation,[status(thm)],[c_106130,c_37752]) ).
tcf(c_110082,plain,
( ( iPr_def_16 = iPr_def_18 )
| ( identity = iPr_def_24 )
| ( multiply(sk_c2,iPr_def_23) = iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_76166,c_608]) ).
tcf(c_110087,plain,
( ( iPr_def_16 = iPr_def_18 )
| ( identity = iPr_def_24 ) ),
inference(light_normalisation,[status(thm)],[c_110082,c_49959]) ).
tcf(c_110559,plain,
! [X0: $i] :
( ( sk_c10 = iPr_def_21 )
| ( iPr_def_21 != X0 )
| ( sk_c10 != X0 ) ),
inference(instantiation,[status(thm)],[c_666]) ).
tcf(c_110560,plain,
( ( sk_c10 = iPr_def_21 )
| ( iPr_def_21 != sk_c10 )
| ( sk_c10 != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_110559]) ).
tcf(c_110840,plain,
( ~ iPr_def_10
| ( sk_c10 != iPr_def_26 ) ),
inference(global_subsumption_just,[status(thm)],[c_42578,c_3162,c_3158,c_14735,c_14842]) ).
tcf(c_110842,plain,
~ iPr_def_10,
inference(global_subsumption_just,[status(thm)],[c_110840,c_3162,c_15656,c_15770,c_110840]) ).
tcf(c_111746,plain,
! [X0: $i] : multiply(X0,identity) = X0,
inference(demodulation,[status(thm)],[c_99213,c_99507]) ).
tcf(c_111887,plain,
( ( iPr_def_21 = iPr_def_26 )
| ( iPr_def_26 != sk_c9 )
| ( iPr_def_21 != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_82860]) ).
tcf(c_113655,plain,
! [X0: $i] :
( ( identity = iPr_def_13 )
| ( iPr_def_13 != inverse(X0) )
| ( identity != inverse(X0) ) ),
inference(instantiation,[status(thm)],[c_91702]) ).
tcf(c_113656,plain,
! [X0: $i] :
( ( identity = inverse(X0) )
| ( identity != iPr_def_21 )
| ( inverse(X0) != iPr_def_21 ) ),
inference(instantiation,[status(thm)],[c_72867]) ).
tcf(c_113663,plain,
( ( identity = iPr_def_13 )
| ( iPr_def_13 != inverse(sk_c10) )
| ( identity != inverse(sk_c10) ) ),
inference(instantiation,[status(thm)],[c_113655]) ).
tcf(c_113664,plain,
( ( identity = inverse(sk_c10) )
| ( identity != iPr_def_21 )
| ( inverse(sk_c10) != iPr_def_21 ) ),
inference(instantiation,[status(thm)],[c_113656]) ).
tcf(c_116612,plain,
! [X0: $i] :
( ( iPr_def_24 = iPr_def_13 )
| ( iPr_def_24 != inverse(X0) )
| ( iPr_def_13 != inverse(X0) ) ),
inference(instantiation,[status(thm)],[c_91654]) ).
tcf(c_116621,plain,
( ( iPr_def_24 = iPr_def_13 )
| ( iPr_def_24 != inverse(sk_c10) )
| ( iPr_def_13 != inverse(sk_c10) ) ),
inference(instantiation,[status(thm)],[c_116612]) ).
tcf(c_118713,plain,
! [X0: $i] :
( ( iPr_def_24 = inverse(X0) )
| ( iPr_def_24 != iPr_def_24 )
| ( inverse(X0) != iPr_def_24 ) ),
inference(instantiation,[status(thm)],[c_73406]) ).
tcf(c_118714,plain,
( ( iPr_def_24 = inverse(sk_c10) )
| ( iPr_def_24 != iPr_def_24 )
| ( inverse(sk_c10) != iPr_def_24 ) ),
inference(instantiation,[status(thm)],[c_118713]) ).
tcf(c_119969,plain,
! [X0: $i] :
( ( inverse(X0) = identity )
| ( identity != iPr_def_24 )
| ( inverse(X0) != iPr_def_24 ) ),
inference(instantiation,[status(thm)],[c_73407]) ).
tcf(c_119970,plain,
( ( inverse(sk_c10) = identity )
| ( identity != iPr_def_24 )
| ( inverse(sk_c10) != iPr_def_24 ) ),
inference(instantiation,[status(thm)],[c_119969]) ).
tcf(c_120223,plain,
( ( iPr_def_18 = iPr_def_19 )
| ( inverse(iPr_def_15) = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_30063,c_64448]) ).
tcf(c_120228,plain,
( ( iPr_def_18 = iPr_def_19 )
| ( sk_c4 = iPr_def_15 ) ),
inference(light_normalisation,[status(thm)],[c_120223,c_63892]) ).
tcf(c_120279,plain,
( ( iPr_def_18 = iPr_def_19 )
| ( sk_c1 = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_120228,c_81907]) ).
tcf(c_120860,plain,
! [X0: $i,X1: $i] :
( ( iPr_def_21 = X0 )
| ( iPr_def_21 != inverse(X1) )
| ( X0 != inverse(X1) ) ),
inference(instantiation,[status(thm)],[c_82855]) ).
tcf(c_120870,plain,
( ( iPr_def_21 = sk_c10 )
| ( iPr_def_21 != inverse(sk_c10) )
| ( sk_c10 != inverse(sk_c10) ) ),
inference(instantiation,[status(thm)],[c_120860]) ).
tcf(c_120900,plain,
! [X0: $i] :
( ( iPr_def_21 = X0 )
| ( iPr_def_21 != iPr_def_21 )
| ( X0 != iPr_def_21 ) ),
inference(instantiation,[status(thm)],[c_82855]) ).
tcf(c_120901,plain,
( ( iPr_def_21 = sk_c10 )
| ( iPr_def_21 != iPr_def_21 )
| ( sk_c10 != iPr_def_21 ) ),
inference(instantiation,[status(thm)],[c_120900]) ).
tcf(c_120966,plain,
( ( iPr_def_18 = iPr_def_19 )
| ( inverse(iPr_def_15) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_120279,c_610]) ).
tcf(c_120967,plain,
( ( iPr_def_18 = iPr_def_19 )
| ( sk_c4 = iPr_def_26 ) ),
inference(light_normalisation,[status(thm)],[c_120966,c_63892]) ).
tcf(c_123507,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(X0,X2) = multiply(inverse(X1),sk_c10) )
| ( X2 != sk_c10 )
| ( X0 != inverse(X1) ) ),
inference(instantiation,[status(thm)],[c_668]) ).
tcf(c_123509,plain,
( ( multiply(sk_c10,sk_c10) = multiply(inverse(sk_c10),sk_c10) )
| ( sk_c10 != sk_c10 )
| ( sk_c10 != inverse(sk_c10) ) ),
inference(instantiation,[status(thm)],[c_123507]) ).
tcf(c_125934,plain,
( ( iPr_def_18 = iPr_def_19 )
| ( iPr_def_13 = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_120967,c_63898]) ).
tcf(c_129420,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(inverse(X0),sk_c10) = X2 )
| ( X2 != X1 )
| ( multiply(inverse(X0),sk_c10) != X1 ) ),
inference(instantiation,[status(thm)],[c_666]) ).
tcf(c_129422,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(inverse(X0),sk_c10) = multiply(X1,X2) )
| ( sk_c10 != X2 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_668]) ).
tcf(c_129423,plain,
! [X0: $i] :
( ( sk_c9 = identity )
| ( identity != X0 )
| ( sk_c9 != X0 ) ),
inference(instantiation,[status(thm)],[c_666]) ).
tcf(c_129434,plain,
! [X0: $i,X1: $i] :
( ( multiply(inverse(X0),sk_c10) = X1 )
| ( X1 != multiply(inverse(X0),sk_c10) )
| ( multiply(inverse(X0),sk_c10) != multiply(inverse(X0),sk_c10) ) ),
inference(instantiation,[status(thm)],[c_129420]) ).
tcf(c_129435,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( multiply(inverse(X0),sk_c10) = X3 )
| ( X3 != multiply(X1,X2) )
| ( multiply(inverse(X0),sk_c10) != multiply(X1,X2) ) ),
inference(instantiation,[status(thm)],[c_129420]) ).
tcf(c_129437,plain,
! [X0: $i,X1: $i] :
( ( sk_c9 = multiply(inverse(X0),sk_c10) )
| ( sk_c9 != X1 )
| ( multiply(inverse(X0),sk_c10) != X1 ) ),
inference(instantiation,[status(thm)],[c_666]) ).
tcf(c_129438,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( sk_c9 = multiply(X0,X1) )
| ( sk_c9 != X2 )
| ( multiply(X0,X1) != X2 ) ),
inference(instantiation,[status(thm)],[c_666]) ).
tcf(c_129440,plain,
! [X0: $i,X1: $i] :
( ( identity = X0 )
| ( identity != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_666]) ).
tcf(c_129446,plain,
! [X0: $i,X1: $i] :
( ( X0 = identity )
| ( identity != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_666]) ).
tcf(c_129455,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( sk_c9 = multiply(inverse(X0),sk_c10) )
| ( sk_c9 != multiply(X1,X2) )
| ( multiply(inverse(X0),sk_c10) != multiply(X1,X2) ) ),
inference(instantiation,[status(thm)],[c_129437]) ).
tcf(c_129459,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = multiply(inverse(X0),sk_c10) )
| ( X2 != X1 )
| ( multiply(inverse(X0),sk_c10) != X1 ) ),
inference(instantiation,[status(thm)],[c_666]) ).
tcf(c_129460,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(inverse(X0),sk_c10) = multiply(X1,X2) )
| ( multiply(X1,X2) != multiply(inverse(X0),sk_c10) )
| ( multiply(inverse(X0),sk_c10) != multiply(inverse(X0),sk_c10) ) ),
inference(instantiation,[status(thm)],[c_129434]) ).
tcf(c_129464,plain,
! [X0: $i] :
( ( sk_c9 = multiply(identity,X0) )
| ( sk_c9 != X0 )
| ( multiply(identity,X0) != X0 ) ),
inference(instantiation,[status(thm)],[c_129438]) ).
tcf(c_129469,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( multiply(X0,X1) = X3 )
| ( X3 != X2 )
| ( multiply(X0,X1) != X2 ) ),
inference(instantiation,[status(thm)],[c_666]) ).
tcf(c_129470,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( sk_c9 = multiply(X0,X1) )
| ( sk_c9 != multiply(X2,X3) )
| ( multiply(X0,X1) != multiply(X2,X3) ) ),
inference(instantiation,[status(thm)],[c_129438]) ).
tcf(c_129477,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( X3 = multiply(X0,X1) )
| ( X3 != X2 )
| ( multiply(X0,X1) != X2 ) ),
inference(instantiation,[status(thm)],[c_666]) ).
tcf(c_129511,plain,
! [X0: $i] :
( ( multiply(inverse(X0),sk_c10) = multiply(sk_c6,sk_c9) )
| ( sk_c10 != sk_c9 )
| ( inverse(X0) != sk_c6 ) ),
inference(instantiation,[status(thm)],[c_129422]) ).
tcf(c_129512,plain,
( ( multiply(inverse(sk_c10),sk_c10) = multiply(sk_c6,sk_c9) )
| ( sk_c10 != sk_c9 )
| ( inverse(sk_c10) != sk_c6 ) ),
inference(instantiation,[status(thm)],[c_129511]) ).
tcf(c_129546,plain,
! [X0: $i,X1: $i] :
( ( multiply(inverse(X0),sk_c10) = sk_c9 )
| ( sk_c9 != multiply(identity,X1) )
| ( multiply(inverse(X0),sk_c10) != multiply(identity,X1) ) ),
inference(instantiation,[status(thm)],[c_129435]) ).
tcf(c_129547,plain,
( ( multiply(inverse(sk_c10),sk_c10) = sk_c9 )
| ( sk_c9 != multiply(identity,sk_c10) )
| ( multiply(inverse(sk_c10),sk_c10) != multiply(identity,sk_c10) ) ),
inference(instantiation,[status(thm)],[c_129546]) ).
tcf(c_129548,plain,
! [X0: $i,X1: $i] :
( ( sk_c9 = multiply(inverse(X0),sk_c10) )
| ( sk_c9 != multiply(identity,X1) )
| ( multiply(inverse(X0),sk_c10) != multiply(identity,X1) ) ),
inference(instantiation,[status(thm)],[c_129455]) ).
tcf(c_129550,plain,
( ( sk_c9 = multiply(inverse(sk_c10),sk_c10) )
| ( sk_c9 != multiply(identity,sk_c10) )
| ( multiply(inverse(sk_c10),sk_c10) != multiply(identity,sk_c10) ) ),
inference(instantiation,[status(thm)],[c_129548]) ).
tcf(c_129554,plain,
! [X0: $i,X1: $i] :
( ( multiply(identity,X0) = X1 )
| ( X1 != X0 )
| ( multiply(identity,X0) != X0 ) ),
inference(instantiation,[status(thm)],[c_129469]) ).
tcf(c_129559,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_129469]) ).
tcf(c_129560,plain,
! [X0: $i,X1: $i] : multiply(X0,X1) = multiply(X0,X1),
inference(instantiation,[status(thm)],[c_665]) ).
tcf(c_129564,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( ( multiply(X0,X1) = X4 )
| ( X4 != multiply(X2,X3) )
| ( multiply(X0,X1) != multiply(X2,X3) ) ),
inference(instantiation,[status(thm)],[c_129469]) ).
tcf(c_129581,plain,
! [X0: $i] :
( ( X0 = multiply(inverse(sk_c10),sk_c10) )
| ( X0 != identity )
| ( multiply(inverse(sk_c10),sk_c10) != identity ) ),
inference(instantiation,[status(thm)],[c_129459]) ).
tcf(c_129588,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( X3 = multiply(inverse(X0),sk_c10) )
| ( X3 != multiply(X1,X2) )
| ( multiply(inverse(X0),sk_c10) != multiply(X1,X2) ) ),
inference(instantiation,[status(thm)],[c_129459]) ).
tcf(c_129628,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( sk_c9 = multiply(X0,X1) )
| ( sk_c9 != multiply(identity,X2) )
| ( multiply(X0,X1) != multiply(identity,X2) ) ),
inference(instantiation,[status(thm)],[c_129470]) ).
tcf(c_129630,plain,
! [X0: $i,X1: $i] :
( ( X1 = multiply(identity,X0) )
| ( X1 != X0 )
| ( multiply(identity,X0) != X0 ) ),
inference(instantiation,[status(thm)],[c_129477]) ).
tcf(c_129631,plain,
( ( sk_c10 = multiply(identity,sk_c10) )
| ( sk_c10 != sk_c10 )
| ( multiply(identity,sk_c10) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_129630]) ).
tcf(c_129638,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( ( X4 = multiply(X0,X1) )
| ( X4 != multiply(X2,X3) )
| ( multiply(X0,X1) != multiply(X2,X3) ) ),
inference(instantiation,[status(thm)],[c_129477]) ).
tcf(c_129712,plain,
! [X0: $i] :
( ( sk_c9 = iPr_def_16 )
| ( iPr_def_16 != X0 )
| ( sk_c9 != X0 ) ),
inference(instantiation,[status(thm)],[c_666]) ).
tcf(c_129722,plain,
! [X0: $i] :
( ( sk_c10 = sk_c8 )
| ( sk_c8 != X0 )
| ( sk_c10 != X0 ) ),
inference(instantiation,[status(thm)],[c_666]) ).
tcf(c_129746,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( ( multiply(X3,X4) = multiply(inverse(X0),sk_c10) )
| ( multiply(X3,X4) != multiply(X1,X2) )
| ( multiply(inverse(X0),sk_c10) != multiply(X1,X2) ) ),
inference(instantiation,[status(thm)],[c_129588]) ).
tcf(c_129778,plain,
( ( identity = multiply(inverse(sk_c10),sk_c10) )
| ( identity != identity )
| ( multiply(inverse(sk_c10),sk_c10) != identity ) ),
inference(instantiation,[status(thm)],[c_129581]) ).
tcf(c_129792,plain,
! [X0: $i,X1: $i] :
( ( multiply(inverse(X0),sk_c10) = multiply(identity,X1) )
| ( multiply(identity,X1) != multiply(inverse(X0),sk_c10) )
| ( multiply(inverse(X0),sk_c10) != multiply(inverse(X0),sk_c10) ) ),
inference(instantiation,[status(thm)],[c_129460]) ).
tcf(c_129793,plain,
! [X0: $i,X1: $i] :
( ( multiply(inverse(X0),sk_c10) = multiply(identity,X1) )
| ( sk_c10 != X1 )
| ( inverse(X0) != identity ) ),
inference(instantiation,[status(thm)],[c_129422]) ).
tcf(c_129794,plain,
( ( multiply(inverse(sk_c10),sk_c10) = multiply(identity,sk_c10) )
| ( sk_c10 != sk_c10 )
| ( inverse(sk_c10) != identity ) ),
inference(instantiation,[status(thm)],[c_129793]) ).
tcf(c_129795,plain,
( ( multiply(inverse(sk_c10),sk_c10) = multiply(identity,sk_c10) )
| ( multiply(identity,sk_c10) != multiply(inverse(sk_c10),sk_c10) )
| ( multiply(inverse(sk_c10),sk_c10) != multiply(inverse(sk_c10),sk_c10) ) ),
inference(instantiation,[status(thm)],[c_129792]) ).
tcf(c_129859,plain,
multiply(identity,iPr_def_16) = iPr_def_16,
inference(instantiation,[status(thm)],[c_101]) ).
tcf(c_129862,plain,
iPr_def_16 = iPr_def_16,
inference(instantiation,[status(thm)],[c_665]) ).
tcf(c_129864,plain,
! [X0: $i,X1: $i] :
( ( X0 = iPr_def_16 )
| ( iPr_def_16 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_666]) ).
tcf(c_129885,plain,
! [X0: $i,X1: $i] :
( ( sk_c9 = multiply(identity,X0) )
| ( sk_c9 != X1 )
| ( multiply(identity,X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_129438]) ).
tcf(c_129924,plain,
! [X0: $i] :
( ( identity = multiply(identity,X0) )
| ( identity != X0 )
| ( multiply(identity,X0) != X0 ) ),
inference(instantiation,[status(thm)],[c_129630]) ).
tcf(c_129925,plain,
! [X0: $i] :
( ( sk_c9 = identity )
| ( identity != multiply(identity,X0) )
| ( sk_c9 != multiply(identity,X0) ) ),
inference(instantiation,[status(thm)],[c_129423]) ).
tcf(c_129948,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_129630]) ).
tcf(c_129992,plain,
! [X0: $i,X1: $i] :
( ( multiply(sk_c10,sk_c5) = multiply(X0,X1) )
| ( sk_c5 != X1 )
| ( sk_c10 != X0 ) ),
inference(instantiation,[status(thm)],[c_668]) ).
tcf(c_130032,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( multiply(X0,X1) = multiply(X2,X3) )
| ( multiply(X2,X3) != multiply(X0,X1) )
| ( multiply(X0,X1) != multiply(X0,X1) ) ),
inference(instantiation,[status(thm)],[c_129559]) ).
tcf(c_130038,plain,
( ( multiply(sk_c3,sk_c10) = iPr_def_22 )
| ( iPr_def_22 != multiply(sk_c3,sk_c10) )
| ( multiply(sk_c3,sk_c10) != multiply(sk_c3,sk_c10) ) ),
inference(instantiation,[status(thm)],[c_129559]) ).
tcf(c_130049,plain,
! [X0: $i] :
( ( multiply(identity,X0) = sk_c9 )
| ( sk_c9 != multiply(identity,X0) )
| ( multiply(identity,X0) != multiply(identity,X0) ) ),
inference(instantiation,[status(thm)],[c_129559]) ).
tcf(c_130070,plain,
! [X0: $i,X1: $i] :
( ( multiply(X0,X1) = iPr_def_20 )
| ( iPr_def_20 != multiply(sk_c4,sk_c10) )
| ( multiply(X0,X1) != multiply(sk_c4,sk_c10) ) ),
inference(instantiation,[status(thm)],[c_129564]) ).
tcf(c_130071,plain,
( ( multiply(sk_c10,sk_c10) = iPr_def_20 )
| ( iPr_def_20 != multiply(sk_c4,sk_c10) )
| ( multiply(sk_c10,sk_c10) != multiply(sk_c4,sk_c10) ) ),
inference(instantiation,[status(thm)],[c_130070]) ).
tcf(c_130074,plain,
! [X0: $i,X1: $i] :
( ( multiply(X0,X1) = iPr_def_22 )
| ( iPr_def_22 != multiply(sk_c3,sk_c10) )
| ( multiply(X0,X1) != multiply(sk_c3,sk_c10) ) ),
inference(instantiation,[status(thm)],[c_129564]) ).
tcf(c_130075,plain,
( ( multiply(sk_c10,sk_c10) = iPr_def_22 )
| ( iPr_def_22 != multiply(sk_c3,sk_c10) )
| ( multiply(sk_c10,sk_c10) != multiply(sk_c3,sk_c10) ) ),
inference(instantiation,[status(thm)],[c_130074]) ).
tcf(c_130088,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(X0,X1) = sk_c9 )
| ( sk_c9 != multiply(identity,X2) )
| ( multiply(X0,X1) != multiply(identity,X2) ) ),
inference(instantiation,[status(thm)],[c_129564]) ).
tcf(c_130095,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( multiply(X0,X1) = X3 )
| ( X3 != multiply(identity,X2) )
| ( multiply(X0,X1) != multiply(identity,X2) ) ),
inference(instantiation,[status(thm)],[c_129564]) ).
tcf(c_130121,plain,
! [X0: $i,X1: $i] :
( ( iPr_def_17 = multiply(X0,X1) )
| ( iPr_def_17 != multiply(sk_c10,sk_c8) )
| ( multiply(X0,X1) != multiply(sk_c10,sk_c8) ) ),
inference(instantiation,[status(thm)],[c_129638]) ).
tcf(c_130174,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( ( multiply(X3,multiply(X0,X1)) = multiply(X4,X2) )
| ( X3 != X4 )
| ( multiply(X0,X1) != X2 ) ),
inference(instantiation,[status(thm)],[c_668]) ).
tcf(c_130230,plain,
! [X0: $i,X1: $i] :
( ( iPr_def_16 = X0 )
| ( iPr_def_16 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_666]) ).
tcf(c_130247,plain,
( ( sk_c9 = identity )
| ( identity != multiply(inverse(sk_c10),sk_c10) )
| ( sk_c9 != multiply(inverse(sk_c10),sk_c10) ) ),
inference(instantiation,[status(thm)],[c_129423]) ).
tcf(c_130261,plain,
! [X0: $i,X1: $i] :
( ( sk_c8 = X0 )
| ( sk_c8 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_666]) ).
tcf(c_130284,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(X0,X1) = iPr_def_16 )
| ( iPr_def_16 != multiply(inverse(X2),sk_c10) )
| ( multiply(X0,X1) != multiply(inverse(X2),sk_c10) ) ),
inference(instantiation,[status(thm)],[c_129564]) ).
tcf(c_130285,plain,
( ( multiply(sk_c10,sk_c10) = iPr_def_16 )
| ( iPr_def_16 != multiply(inverse(sk_c10),sk_c10) )
| ( multiply(sk_c10,sk_c10) != multiply(inverse(sk_c10),sk_c10) ) ),
inference(instantiation,[status(thm)],[c_130284]) ).
tcf(c_130359,plain,
! [X0: $i,X1: $i] :
( ( sk_c1 = X0 )
| ( sk_c1 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_666]) ).
tcf(c_130521,plain,
! [X0: $i] :
( ( sk_c9 = multiply(identity,identity) )
| ( sk_c9 != X0 )
| ( multiply(identity,identity) != X0 ) ),
inference(instantiation,[status(thm)],[c_129885]) ).
tcf(c_130654,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( multiply(identity,X3) = multiply(inverse(X0),sk_c10) )
| ( multiply(identity,X3) != multiply(X1,X2) )
| ( multiply(inverse(X0),sk_c10) != multiply(X1,X2) ) ),
inference(instantiation,[status(thm)],[c_129746]) ).
tcf(c_130841,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(identity,X2) = multiply(X0,X1) )
| ( multiply(identity,X2) != X2 )
| ( multiply(X0,X1) != X2 ) ),
inference(instantiation,[status(thm)],[c_129554]) ).
tcf(c_130890,plain,
! [X0: $i] :
( ( multiply(sk_c10,sk_c8) = X0 )
| ( X0 != iPr_def_17 )
| ( multiply(sk_c10,sk_c8) != iPr_def_17 ) ),
inference(instantiation,[status(thm)],[c_129469]) ).
tcf(c_130891,plain,
( ( sk_c9 = multiply(sk_c10,sk_c8) )
| ( sk_c9 != iPr_def_17 )
| ( multiply(sk_c10,sk_c8) != iPr_def_17 ) ),
inference(instantiation,[status(thm)],[c_129438]) ).
tcf(c_130894,plain,
! [X0: $i] :
( ( X0 = multiply(sk_c6,sk_c9) )
| ( X0 != iPr_def_18 )
| ( multiply(sk_c6,sk_c9) != iPr_def_18 ) ),
inference(instantiation,[status(thm)],[c_129477]) ).
tcf(c_130895,plain,
! [X0: $i] :
( ( multiply(sk_c6,sk_c9) = X0 )
| ( X0 != iPr_def_18 )
| ( multiply(sk_c6,sk_c9) != iPr_def_18 ) ),
inference(instantiation,[status(thm)],[c_129469]) ).
tcf(c_130897,plain,
( ( multiply(sk_c6,sk_c9) = sk_c10 )
| ( sk_c10 != iPr_def_18 )
| ( multiply(sk_c6,sk_c9) != iPr_def_18 ) ),
inference(instantiation,[status(thm)],[c_130895]) ).
tcf(c_130898,plain,
( ( sk_c10 = multiply(sk_c6,sk_c9) )
| ( sk_c10 != iPr_def_18 )
| ( multiply(sk_c6,sk_c9) != iPr_def_18 ) ),
inference(instantiation,[status(thm)],[c_130894]) ).
tcf(c_130930,plain,
! [X0: $i] :
( ( X0 = multiply(sk_c10,sk_c5) )
| ( X0 != iPr_def_21 )
| ( multiply(sk_c10,sk_c5) != iPr_def_21 ) ),
inference(instantiation,[status(thm)],[c_129477]) ).
tcf(c_130938,plain,
multiply(sk_c3,sk_c10) = multiply(sk_c3,sk_c10),
inference(instantiation,[status(thm)],[c_129560]) ).
tcf(c_131086,plain,
! [X0: $i] :
( ( multiply(sk_c10,sk_c5) = multiply(X0,sk_c5) )
| ( sk_c5 != sk_c5 )
| ( sk_c10 != X0 ) ),
inference(instantiation,[status(thm)],[c_129992]) ).
tcf(c_131087,plain,
sk_c5 = sk_c5,
inference(instantiation,[status(thm)],[c_665]) ).
tcf(c_131088,plain,
( ( multiply(sk_c10,sk_c5) = multiply(sk_c10,sk_c5) )
| ( sk_c5 != sk_c5 )
| ( sk_c10 != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_131086]) ).
tcf(c_131138,plain,
! [X0: $i,X1: $i] :
( ( multiply(X0,X1) = multiply(sk_c10,sk_c8) )
| ( X1 != sk_c8 )
| ( X0 != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_668]) ).
tcf(c_131139,plain,
( ( multiply(sk_c10,sk_c10) = multiply(sk_c10,sk_c8) )
| ( sk_c10 != sk_c8 )
| ( sk_c10 != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_131138]) ).
tcf(c_131201,plain,
! [X0: $i,X1: $i] :
( ( multiply(X0,X1) = multiply(sk_c4,sk_c10) )
| ( X1 != sk_c10 )
| ( X0 != sk_c4 ) ),
inference(instantiation,[status(thm)],[c_668]) ).
tcf(c_131202,plain,
( ( multiply(sk_c10,sk_c10) = multiply(sk_c4,sk_c10) )
| ( sk_c10 != sk_c4 )
| ( sk_c10 != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_131201]) ).
tcf(c_131231,plain,
! [X0: $i,X1: $i] :
( ( multiply(X0,X1) = multiply(sk_c3,sk_c10) )
| ( X1 != sk_c10 )
| ( X0 != sk_c3 ) ),
inference(instantiation,[status(thm)],[c_668]) ).
tcf(c_131232,plain,
( ( multiply(sk_c10,sk_c10) = multiply(sk_c3,sk_c10) )
| ( sk_c10 != sk_c3 )
| ( sk_c10 != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_131231]) ).
tcf(c_131813,plain,
! [X0: $i,X1: $i] :
( ( multiply(sk_c10,sk_c5) = multiply(X0,X1) )
| ( multiply(sk_c10,sk_c5) != multiply(sk_c10,sk_c5) )
| ( multiply(X0,X1) != multiply(sk_c10,sk_c5) ) ),
inference(instantiation,[status(thm)],[c_130032]) ).
tcf(c_132273,plain,
! [X0: $i] :
( ( sk_c9 = sk_c8 )
| ( sk_c8 != X0 )
| ( sk_c9 != X0 ) ),
inference(instantiation,[status(thm)],[c_666]) ).
tcf(c_132283,plain,
! [X0: $i,X1: $i] :
( ( X0 = sk_c8 )
| ( sk_c8 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_666]) ).
tcf(c_132287,plain,
! [X0: $i] :
( ( multiply(identity,X0) = sk_c8 )
| ( sk_c8 != X0 )
| ( multiply(identity,X0) != X0 ) ),
inference(instantiation,[status(thm)],[c_129554]) ).
tcf(c_132295,plain,
! [X0: $i] :
( ( sk_c9 = multiply(inverse(X0),sk_c10) )
| ( sk_c9 != multiply(sk_c10,sk_c8) )
| ( multiply(inverse(X0),sk_c10) != multiply(sk_c10,sk_c8) ) ),
inference(instantiation,[status(thm)],[c_129588]) ).
tcf(c_132298,plain,
( ( sk_c9 = multiply(inverse(sk_c10),sk_c10) )
| ( sk_c9 != multiply(sk_c10,sk_c8) )
| ( multiply(inverse(sk_c10),sk_c10) != multiply(sk_c10,sk_c8) ) ),
inference(instantiation,[status(thm)],[c_132295]) ).
tcf(c_132304,plain,
! [X0: $i,X1: $i] :
( ( sk_c9 = multiply(X0,X1) )
| ( sk_c9 != multiply(sk_c10,sk_c8) )
| ( multiply(X0,X1) != multiply(sk_c10,sk_c8) ) ),
inference(instantiation,[status(thm)],[c_129470]) ).
tcf(c_132307,plain,
! [X0: $i,X1: $i] :
( ( multiply(X0,X1) = sk_c9 )
| ( sk_c9 != multiply(sk_c10,sk_c8) )
| ( multiply(X0,X1) != multiply(sk_c10,sk_c8) ) ),
inference(instantiation,[status(thm)],[c_129564]) ).
tcf(c_132308,plain,
( ( multiply(sk_c10,sk_c10) = sk_c9 )
| ( sk_c9 != multiply(sk_c10,sk_c8) )
| ( multiply(sk_c10,sk_c10) != multiply(sk_c10,sk_c8) ) ),
inference(instantiation,[status(thm)],[c_132307]) ).
tcf(c_132311,plain,
! [X0: $i] :
( ( sk_c9 = iPr_def_20 )
| ( iPr_def_20 != X0 )
| ( sk_c9 != X0 ) ),
inference(instantiation,[status(thm)],[c_666]) ).
tcf(c_132409,plain,
! [X0: $i] :
( ( iPr_def_16 = X0 )
| ( iPr_def_16 != iPr_def_16 )
| ( X0 != iPr_def_16 ) ),
inference(instantiation,[status(thm)],[c_130230]) ).
tcf(c_132884,plain,
multiply(identity,identity) = multiply(identity,identity),
inference(instantiation,[status(thm)],[c_129560]) ).
tcf(c_132978,plain,
( ( multiply(identity,identity) = sk_c9 )
| ( sk_c9 != multiply(identity,identity) )
| ( multiply(identity,identity) != multiply(identity,identity) ) ),
inference(instantiation,[status(thm)],[c_130049]) ).
tcf(c_133244,plain,
! [X0: $i,X1: $i] :
( ( X1 = multiply(sk_c10,sk_c8) )
| ( X1 != X0 )
| ( multiply(sk_c10,sk_c8) != X0 ) ),
inference(instantiation,[status(thm)],[c_129477]) ).
tcf(c_133276,plain,
! [X0: $i] :
( ( multiply(sk_c10,sk_c8) = multiply(identity,X0) )
| ( multiply(sk_c10,sk_c8) != iPr_def_17 )
| ( multiply(identity,X0) != iPr_def_17 ) ),
inference(instantiation,[status(thm)],[c_130890]) ).
tcf(c_133278,plain,
! [X0: $i,X1: $i] :
( ( multiply(sk_c10,sk_c8) = X1 )
| ( X1 != multiply(identity,X0) )
| ( multiply(sk_c10,sk_c8) != multiply(identity,X0) ) ),
inference(instantiation,[status(thm)],[c_130095]) ).
tcf(c_133281,plain,
( ( multiply(sk_c10,sk_c8) = multiply(identity,sk_c10) )
| ( multiply(identity,sk_c10) != iPr_def_17 )
| ( multiply(sk_c10,sk_c8) != iPr_def_17 ) ),
inference(instantiation,[status(thm)],[c_133276]) ).
tcf(c_133284,plain,
( ( multiply(sk_c10,sk_c8) = sk_c10 )
| ( sk_c10 != multiply(identity,sk_c10) )
| ( multiply(sk_c10,sk_c8) != multiply(identity,sk_c10) ) ),
inference(instantiation,[status(thm)],[c_133278]) ).
tcf(c_133310,plain,
! [X0: $i,X1: $i] :
( ( multiply(inverse(X0),sk_c10) = X1 )
| ( X1 != multiply(sk_c6,sk_c9) )
| ( multiply(inverse(X0),sk_c10) != multiply(sk_c6,sk_c9) ) ),
inference(instantiation,[status(thm)],[c_129435]) ).
tcf(c_133311,plain,
( ( multiply(inverse(sk_c10),sk_c10) = sk_c10 )
| ( sk_c10 != multiply(sk_c6,sk_c9) )
| ( multiply(inverse(sk_c10),sk_c10) != multiply(sk_c6,sk_c9) ) ),
inference(instantiation,[status(thm)],[c_133310]) ).
tcf(c_133386,plain,
( ( iPr_def_16 = multiply(sk_c6,sk_c9) )
| ( iPr_def_16 != iPr_def_18 )
| ( multiply(sk_c6,sk_c9) != iPr_def_18 ) ),
inference(instantiation,[status(thm)],[c_130894]) ).
tcf(c_133389,plain,
( ( sk_c9 = iPr_def_16 )
| ( iPr_def_16 != multiply(sk_c6,sk_c9) )
| ( sk_c9 != multiply(sk_c6,sk_c9) ) ),
inference(instantiation,[status(thm)],[c_129712]) ).
tcf(c_133390,plain,
( ( sk_c8 = multiply(sk_c6,sk_c9) )
| ( sk_c8 != iPr_def_18 )
| ( multiply(sk_c6,sk_c9) != iPr_def_18 ) ),
inference(instantiation,[status(thm)],[c_130894]) ).
tcf(c_133391,plain,
( ( sk_c10 = sk_c8 )
| ( sk_c8 != multiply(sk_c6,sk_c9) )
| ( sk_c10 != multiply(sk_c6,sk_c9) ) ),
inference(instantiation,[status(thm)],[c_129722]) ).
tcf(c_133414,plain,
! [X0: $i] :
( ( multiply(sk_c6,sk_c9) = multiply(identity,X0) )
| ( multiply(sk_c6,sk_c9) != X0 )
| ( multiply(identity,X0) != X0 ) ),
inference(instantiation,[status(thm)],[c_129948]) ).
tcf(c_133415,plain,
! [X0: $i,X1: $i] :
( ( X1 = multiply(sk_c6,sk_c9) )
| ( X1 != X0 )
| ( multiply(sk_c6,sk_c9) != X0 ) ),
inference(instantiation,[status(thm)],[c_129477]) ).
tcf(c_133420,plain,
( ( multiply(sk_c6,sk_c9) = multiply(identity,sk_c10) )
| ( multiply(identity,sk_c10) != sk_c10 )
| ( multiply(sk_c6,sk_c9) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_133414]) ).
tcf(c_133451,plain,
! [X0: $i] :
( ( sk_c9 = multiply(sk_c6,sk_c9) )
| ( sk_c9 != multiply(identity,X0) )
| ( multiply(sk_c6,sk_c9) != multiply(identity,X0) ) ),
inference(instantiation,[status(thm)],[c_129628]) ).
tcf(c_133453,plain,
( ( sk_c9 = multiply(sk_c6,sk_c9) )
| ( sk_c9 != multiply(identity,sk_c10) )
| ( multiply(sk_c6,sk_c9) != multiply(identity,sk_c10) ) ),
inference(instantiation,[status(thm)],[c_133451]) ).
tcf(c_133476,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( multiply(X2,multiply(X0,X1)) = multiply(X3,iPr_def_16) )
| ( X2 != X3 )
| ( multiply(X0,X1) != iPr_def_16 ) ),
inference(instantiation,[status(thm)],[c_130174]) ).
tcf(c_133527,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X0 = iPr_def_16 )
| ( iPr_def_16 != multiply(X1,X2) )
| ( X0 != multiply(X1,X2) ) ),
inference(instantiation,[status(thm)],[c_129864]) ).
tcf(c_133534,plain,
multiply(identity,iPr_def_20) = iPr_def_20,
inference(instantiation,[status(thm)],[c_101]) ).
tcf(c_133631,plain,
( ( multiply(sk_c3,sk_c10) = multiply(sk_c10,sk_c5) )
| ( multiply(sk_c3,sk_c10) != iPr_def_21 )
| ( multiply(sk_c10,sk_c5) != iPr_def_21 ) ),
inference(instantiation,[status(thm)],[c_130930]) ).
tcf(c_133680,plain,
! [X0: $i] :
( ( sk_c9 = multiply(sk_c10,sk_c5) )
| ( sk_c9 != X0 )
| ( multiply(sk_c10,sk_c5) != X0 ) ),
inference(instantiation,[status(thm)],[c_129438]) ).
tcf(c_135341,plain,
! [X0: $i] :
( ( multiply(sk_c3,sk_c10) = X0 )
| ( X0 != iPr_def_22 )
| ( multiply(sk_c3,sk_c10) != iPr_def_22 ) ),
inference(instantiation,[status(thm)],[c_129469]) ).
tcf(c_135347,plain,
! [X0: $i,X1: $i] :
( ( multiply(X0,X1) = multiply(identity,iPr_def_22) )
| ( multiply(identity,iPr_def_22) != iPr_def_22 )
| ( multiply(X0,X1) != iPr_def_22 ) ),
inference(instantiation,[status(thm)],[c_129948]) ).
tcf(c_135354,plain,
( ( multiply(sk_c10,sk_c10) = multiply(identity,iPr_def_22) )
| ( multiply(identity,iPr_def_22) != iPr_def_22 )
| ( multiply(sk_c10,sk_c10) != iPr_def_22 ) ),
inference(instantiation,[status(thm)],[c_135347]) ).
tcf(c_135636,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( multiply(X2,multiply(X0,X1)) = multiply(X3,iPr_def_20) )
| ( X2 != X3 )
| ( multiply(X0,X1) != iPr_def_20 ) ),
inference(instantiation,[status(thm)],[c_130174]) ).
tcf(c_136773,plain,
( ( multiply(sk_c10,sk_c5) = multiply(sk_c3,sk_c10) )
| ( multiply(sk_c3,sk_c10) != multiply(sk_c10,sk_c5) )
| ( multiply(sk_c10,sk_c5) != multiply(sk_c10,sk_c5) ) ),
inference(instantiation,[status(thm)],[c_131813]) ).
tcf(c_138074,plain,
! [X0: $i] :
( ( sk_c8 = X0 )
| ( sk_c8 != iPr_def_16 )
| ( X0 != iPr_def_16 ) ),
inference(instantiation,[status(thm)],[c_130261]) ).
tcf(c_138120,plain,
! [X0: $i] :
( ( X0 = sk_c8 )
| ( sk_c8 != iPr_def_16 )
| ( X0 != iPr_def_16 ) ),
inference(instantiation,[status(thm)],[c_132283]) ).
tcf(c_138167,plain,
iPr_def_20 = iPr_def_20,
inference(instantiation,[status(thm)],[c_665]) ).
tcf(c_138394,plain,
! [X0: $i] :
( ( sk_c9 = multiply(inverse(X0),sk_c10) )
| ( sk_c9 != multiply(sk_c6,sk_c9) )
| ( multiply(inverse(X0),sk_c10) != multiply(sk_c6,sk_c9) ) ),
inference(instantiation,[status(thm)],[c_129455]) ).
tcf(c_138397,plain,
( ( sk_c9 = multiply(inverse(sk_c10),sk_c10) )
| ( sk_c9 != multiply(sk_c6,sk_c9) )
| ( multiply(inverse(sk_c10),sk_c10) != multiply(sk_c6,sk_c9) ) ),
inference(instantiation,[status(thm)],[c_138394]) ).
tcf(c_139769,plain,
( ( iPr_def_16 = multiply(inverse(sk_c10),sk_c10) )
| ( iPr_def_16 != identity )
| ( multiply(inverse(sk_c10),sk_c10) != identity ) ),
inference(instantiation,[status(thm)],[c_129581]) ).
tcf(c_140008,plain,
( ( identity = multiply(identity,iPr_def_16) )
| ( identity != iPr_def_16 )
| ( multiply(identity,iPr_def_16) != iPr_def_16 ) ),
inference(instantiation,[status(thm)],[c_129924]) ).
tcf(c_140010,plain,
( ( sk_c9 = identity )
| ( identity != iPr_def_16 )
| ( sk_c9 != iPr_def_16 ) ),
inference(instantiation,[status(thm)],[c_129423]) ).
tcf(c_140016,plain,
! [X0: $i] :
( ( identity = X0 )
| ( identity != iPr_def_16 )
| ( X0 != iPr_def_16 ) ),
inference(instantiation,[status(thm)],[c_129440]) ).
tcf(c_140017,plain,
( ( identity = sk_c10 )
| ( identity != iPr_def_16 )
| ( sk_c10 != iPr_def_16 ) ),
inference(instantiation,[status(thm)],[c_140016]) ).
tcf(c_140042,plain,
( ( sk_c9 = identity )
| ( identity != iPr_def_22 )
| ( sk_c9 != iPr_def_22 ) ),
inference(instantiation,[status(thm)],[c_129423]) ).
tcf(c_140048,plain,
! [X0: $i] :
( ( identity = X0 )
| ( identity != iPr_def_22 )
| ( X0 != iPr_def_22 ) ),
inference(instantiation,[status(thm)],[c_129440]) ).
tcf(c_140084,plain,
! [X0: $i] :
( ( X0 = identity )
| ( identity != iPr_def_20 )
| ( X0 != iPr_def_20 ) ),
inference(instantiation,[status(thm)],[c_129446]) ).
tcf(c_140217,plain,
( ( sk_c9 = iPr_def_20 )
| ( iPr_def_20 != identity )
| ( sk_c9 != identity ) ),
inference(instantiation,[status(thm)],[c_132311]) ).
tcf(c_140361,plain,
( ( iPr_def_16 = sk_c8 )
| ( iPr_def_16 != iPr_def_16 )
| ( sk_c8 != iPr_def_16 ) ),
inference(instantiation,[status(thm)],[c_132409]) ).
tcf(c_140366,plain,
( ( iPr_def_16 = identity )
| ( iPr_def_16 != iPr_def_16 )
| ( identity != iPr_def_16 ) ),
inference(instantiation,[status(thm)],[c_132409]) ).
tcf(c_140830,plain,
( ( sk_c9 = multiply(identity,iPr_def_16) )
| ( sk_c9 != iPr_def_16 )
| ( multiply(identity,iPr_def_16) != iPr_def_16 ) ),
inference(instantiation,[status(thm)],[c_129464]) ).
tcf(c_141011,plain,
! [X0: $i] :
( ( multiply(X0,iPr_def_16) = multiply(sk_c10,sk_c8) )
| ( iPr_def_16 != sk_c8 )
| ( X0 != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_131138]) ).
tcf(c_141012,plain,
( ( multiply(sk_c10,iPr_def_16) = multiply(sk_c10,sk_c8) )
| ( iPr_def_16 != sk_c8 )
| ( sk_c10 != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_141011]) ).
tcf(c_141033,plain,
multiply(identity,iPr_def_22) = iPr_def_22,
inference(instantiation,[status(thm)],[c_101]) ).
tcf(c_142229,plain,
! [X0: $i,X1: $i] :
( ( multiply(inverse(X0),sk_c10) = multiply(sk_c10,sk_c8) )
| ( multiply(sk_c10,sk_c8) != X1 )
| ( multiply(inverse(X0),sk_c10) != X1 ) ),
inference(instantiation,[status(thm)],[c_133244]) ).
tcf(c_142230,plain,
( ( multiply(inverse(sk_c10),sk_c10) = multiply(sk_c10,sk_c8) )
| ( multiply(sk_c10,sk_c8) != sk_c10 )
| ( multiply(inverse(sk_c10),sk_c10) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_142229]) ).
tcf(c_142509,plain,
( ( sk_c9 = sk_c8 )
| ( sk_c8 != multiply(sk_c6,sk_c9) )
| ( sk_c9 != multiply(sk_c6,sk_c9) ) ),
inference(instantiation,[status(thm)],[c_132273]) ).
tcf(c_142517,plain,
! [X0: $i,X1: $i] :
( ( multiply(identity,X0) = multiply(sk_c6,sk_c9) )
| ( multiply(sk_c6,sk_c9) != X1 )
| ( multiply(identity,X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_133415]) ).
tcf(c_142518,plain,
! [X0: $i,X1: $i] :
( ( multiply(identity,X1) = multiply(inverse(X0),sk_c10) )
| ( multiply(identity,X1) != multiply(sk_c6,sk_c9) )
| ( multiply(inverse(X0),sk_c10) != multiply(sk_c6,sk_c9) ) ),
inference(instantiation,[status(thm)],[c_130654]) ).
tcf(c_142520,plain,
( ( multiply(identity,sk_c10) = multiply(sk_c6,sk_c9) )
| ( multiply(identity,sk_c10) != sk_c10 )
| ( multiply(sk_c6,sk_c9) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_142517]) ).
tcf(c_142521,plain,
( ( multiply(identity,sk_c10) = multiply(inverse(sk_c10),sk_c10) )
| ( multiply(identity,sk_c10) != multiply(sk_c6,sk_c9) )
| ( multiply(inverse(sk_c10),sk_c10) != multiply(sk_c6,sk_c9) ) ),
inference(instantiation,[status(thm)],[c_142518]) ).
tcf(c_145013,plain,
( ( multiply(sk_c10,sk_c5) = iPr_def_22 )
| ( iPr_def_22 != multiply(sk_c3,sk_c10) )
| ( multiply(sk_c10,sk_c5) != multiply(sk_c3,sk_c10) ) ),
inference(instantiation,[status(thm)],[c_130074]) ).
tcf(c_145456,plain,
( ( sk_c10 = iPr_def_16 )
| ( iPr_def_16 != multiply(sk_c6,sk_c9) )
| ( sk_c10 != multiply(sk_c6,sk_c9) ) ),
inference(instantiation,[status(thm)],[c_133527]) ).
tcf(c_145753,plain,
! [X0: $i] :
( ( multiply(X0,iPr_def_16) = sk_c9 )
| ( sk_c9 != multiply(sk_c10,sk_c8) )
| ( multiply(X0,iPr_def_16) != multiply(sk_c10,sk_c8) ) ),
inference(instantiation,[status(thm)],[c_132307]) ).
tcf(c_145754,plain,
! [X0: $i] :
( ( sk_c9 = multiply(X0,iPr_def_16) )
| ( sk_c9 != multiply(sk_c10,sk_c8) )
| ( multiply(X0,iPr_def_16) != multiply(sk_c10,sk_c8) ) ),
inference(instantiation,[status(thm)],[c_132304]) ).
tcf(c_145756,plain,
! [X0: $i] :
( ( iPr_def_17 = multiply(X0,iPr_def_16) )
| ( iPr_def_17 != multiply(sk_c10,sk_c8) )
| ( multiply(X0,iPr_def_16) != multiply(sk_c10,sk_c8) ) ),
inference(instantiation,[status(thm)],[c_130121]) ).
tcf(c_145759,plain,
( ( iPr_def_17 = multiply(sk_c10,iPr_def_16) )
| ( iPr_def_17 != multiply(sk_c10,sk_c8) )
| ( multiply(sk_c10,iPr_def_16) != multiply(sk_c10,sk_c8) ) ),
inference(instantiation,[status(thm)],[c_145756]) ).
tcf(c_145761,plain,
( ( sk_c9 = multiply(sk_c10,iPr_def_16) )
| ( sk_c9 != multiply(sk_c10,sk_c8) )
| ( multiply(sk_c10,iPr_def_16) != multiply(sk_c10,sk_c8) ) ),
inference(instantiation,[status(thm)],[c_145754]) ).
tcf(c_145762,plain,
( ( multiply(sk_c10,iPr_def_16) = sk_c9 )
| ( sk_c9 != multiply(sk_c10,sk_c8) )
| ( multiply(sk_c10,iPr_def_16) != multiply(sk_c10,sk_c8) ) ),
inference(instantiation,[status(thm)],[c_145753]) ).
tcf(c_145763,plain,
( ( multiply(identity,iPr_def_16) = multiply(sk_c10,sk_c8) )
| ( iPr_def_16 != sk_c8 )
| ( identity != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_141011]) ).
tcf(c_146347,plain,
( ( sk_c8 = identity )
| ( identity != iPr_def_16 )
| ( sk_c8 != iPr_def_16 ) ),
inference(instantiation,[status(thm)],[c_138074]) ).
tcf(c_146458,plain,
( ( identity = sk_c8 )
| ( identity != iPr_def_16 )
| ( sk_c8 != iPr_def_16 ) ),
inference(instantiation,[status(thm)],[c_138120]) ).
tcf(c_146699,plain,
( ( sk_c9 = multiply(identity,identity) )
| ( sk_c9 != sk_c8 )
| ( multiply(identity,identity) != sk_c8 ) ),
inference(instantiation,[status(thm)],[c_130521]) ).
tcf(c_147613,plain,
( ( sk_c9 = identity )
| ( identity != multiply(identity,iPr_def_16) )
| ( sk_c9 != multiply(identity,iPr_def_16) ) ),
inference(instantiation,[status(thm)],[c_129925]) ).
tcf(c_148502,plain,
( ( iPr_def_20 = identity )
| ( iPr_def_20 != iPr_def_20 )
| ( identity != iPr_def_20 ) ),
inference(instantiation,[status(thm)],[c_140084]) ).
tcf(c_148700,plain,
( ( sk_c9 = multiply(identity,iPr_def_20) )
| ( sk_c9 != iPr_def_20 )
| ( multiply(identity,iPr_def_20) != iPr_def_20 ) ),
inference(instantiation,[status(thm)],[c_129464]) ).
tcf(c_155317,plain,
! [X0: $i,X1: $i] :
( ( X1 = multiply(X0,iPr_def_16) )
| ( X1 != sk_c9 )
| ( multiply(X0,iPr_def_16) != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_129477]) ).
tcf(c_155627,plain,
! [X0: $i] :
( ( multiply(X0,iPr_def_16) = sk_c9 )
| ( sk_c9 != multiply(X0,iPr_def_16) )
| ( multiply(X0,iPr_def_16) != multiply(X0,iPr_def_16) ) ),
inference(instantiation,[status(thm)],[c_129559]) ).
tcf(c_155628,plain,
( ( multiply(sk_c10,iPr_def_16) = sk_c9 )
| ( sk_c9 != multiply(sk_c10,iPr_def_16) )
| ( multiply(sk_c10,iPr_def_16) != multiply(sk_c10,iPr_def_16) ) ),
inference(instantiation,[status(thm)],[c_155627]) ).
tcf(c_155639,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( sk_c9 = multiply(X0,X1) )
| ( sk_c9 != multiply(X2,iPr_def_16) )
| ( multiply(X0,X1) != multiply(X2,iPr_def_16) ) ),
inference(instantiation,[status(thm)],[c_129470]) ).
tcf(c_155642,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(X0,X1) = sk_c9 )
| ( sk_c9 != multiply(X2,iPr_def_16) )
| ( multiply(X0,X1) != multiply(X2,iPr_def_16) ) ),
inference(instantiation,[status(thm)],[c_129564]) ).
tcf(c_155648,plain,
( ( sk_c9 = multiply(identity,iPr_def_16) )
| ( sk_c9 != multiply(sk_c10,sk_c8) )
| ( multiply(identity,iPr_def_16) != multiply(sk_c10,sk_c8) ) ),
inference(instantiation,[status(thm)],[c_145754]) ).
tcf(c_155699,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(X0,X1) = iPr_def_17 )
| ( iPr_def_17 != multiply(X2,iPr_def_16) )
| ( multiply(X0,X1) != multiply(X2,iPr_def_16) ) ),
inference(instantiation,[status(thm)],[c_129564]) ).
tcf(c_155726,plain,
! [X0: $i,X1: $i] :
( ( multiply(X0,iPr_def_16) = X1 )
| ( X1 != iPr_def_17 )
| ( multiply(X0,iPr_def_16) != iPr_def_17 ) ),
inference(instantiation,[status(thm)],[c_129469]) ).
tcf(c_155727,plain,
! [X0: $i] :
( ( sk_c9 = multiply(X0,iPr_def_16) )
| ( sk_c9 != iPr_def_17 )
| ( multiply(X0,iPr_def_16) != iPr_def_17 ) ),
inference(instantiation,[status(thm)],[c_129438]) ).
tcf(c_155728,plain,
( ( sk_c9 = multiply(sk_c10,iPr_def_16) )
| ( sk_c9 != iPr_def_17 )
| ( multiply(sk_c10,iPr_def_16) != iPr_def_17 ) ),
inference(instantiation,[status(thm)],[c_155727]) ).
tcf(c_159873,plain,
! [X0: $i] :
( ( identity = X0 )
| ( identity != sk_c8 )
| ( X0 != sk_c8 ) ),
inference(instantiation,[status(thm)],[c_129440]) ).
tcf(c_159874,plain,
( ( identity = sk_c10 )
| ( identity != sk_c8 )
| ( sk_c10 != sk_c8 ) ),
inference(instantiation,[status(thm)],[c_159873]) ).
tcf(c_159905,plain,
( ( multiply(identity,identity) = sk_c8 )
| ( sk_c8 != identity )
| ( multiply(identity,identity) != identity ) ),
inference(instantiation,[status(thm)],[c_132287]) ).
tcf(c_165971,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(X2,multiply(X0,X1)) = multiply(identity,iPr_def_16) )
| ( X2 != identity )
| ( multiply(X0,X1) != iPr_def_16 ) ),
inference(instantiation,[status(thm)],[c_133476]) ).
tcf(c_165974,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(X0,multiply(X1,X2)) = sk_c9 )
| ( sk_c9 != multiply(identity,iPr_def_16) )
| ( multiply(X0,multiply(X1,X2)) != multiply(identity,iPr_def_16) ) ),
inference(instantiation,[status(thm)],[c_130088]) ).
tcf(c_165976,plain,
( ( multiply(sk_c10,multiply(sk_c10,sk_c10)) = multiply(identity,iPr_def_16) )
| ( sk_c10 != identity )
| ( multiply(sk_c10,sk_c10) != iPr_def_16 ) ),
inference(instantiation,[status(thm)],[c_165971]) ).
tcf(c_165978,plain,
( ( multiply(sk_c10,multiply(sk_c10,sk_c10)) = sk_c9 )
| ( sk_c9 != multiply(identity,iPr_def_16) )
| ( multiply(sk_c10,multiply(sk_c10,sk_c10)) != multiply(identity,iPr_def_16) ) ),
inference(instantiation,[status(thm)],[c_165974]) ).
tcf(c_167992,plain,
! [X0: $i] :
( ( sk_c1 = multiply(X0,iPr_def_16) )
| ( sk_c1 != sk_c9 )
| ( multiply(X0,iPr_def_16) != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_155317]) ).
tcf(c_167995,plain,
( ( sk_c1 = multiply(sk_c10,iPr_def_16) )
| ( sk_c1 != sk_c9 )
| ( multiply(sk_c10,iPr_def_16) != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_167992]) ).
tcf(c_168283,plain,
! [X0: $i,X1: $i] :
( ( multiply(identity,X1) = multiply(X0,iPr_def_16) )
| ( multiply(identity,X1) != X1 )
| ( multiply(X0,iPr_def_16) != X1 ) ),
inference(instantiation,[status(thm)],[c_130841]) ).
tcf(c_168289,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = multiply(X0,iPr_def_16) )
| ( X2 != X1 )
| ( multiply(X0,iPr_def_16) != X1 ) ),
inference(instantiation,[status(thm)],[c_129477]) ).
tcf(c_168293,plain,
( ( sk_c10 = multiply(sk_c10,iPr_def_16) )
| ( sk_c10 != sk_c10 )
| ( multiply(sk_c10,iPr_def_16) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_168289]) ).
tcf(c_168298,plain,
( ( multiply(identity,sk_c10) = multiply(sk_c10,iPr_def_16) )
| ( multiply(identity,sk_c10) != sk_c10 )
| ( multiply(sk_c10,iPr_def_16) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_168283]) ).
tcf(c_169097,plain,
! [X0: $i,X1: $i] :
( ( sk_c1 = X0 )
| ( sk_c1 != multiply(X1,iPr_def_16) )
| ( X0 != multiply(X1,iPr_def_16) ) ),
inference(instantiation,[status(thm)],[c_130359]) ).
tcf(c_169101,plain,
( ( sk_c1 = sk_c10 )
| ( sk_c10 != multiply(sk_c10,iPr_def_16) )
| ( sk_c1 != multiply(sk_c10,iPr_def_16) ) ),
inference(instantiation,[status(thm)],[c_169097]) ).
tcf(c_170284,plain,
! [X0: $i,X1: $i] :
( ( multiply(X0,iPr_def_16) = multiply(X1,iPr_def_16) )
| ( multiply(X1,iPr_def_16) != iPr_def_17 )
| ( multiply(X0,iPr_def_16) != iPr_def_17 ) ),
inference(instantiation,[status(thm)],[c_155726]) ).
tcf(c_170287,plain,
( ( multiply(sk_c10,iPr_def_16) = multiply(sk_c10,iPr_def_16) )
| ( multiply(sk_c10,iPr_def_16) != iPr_def_17 ) ),
inference(instantiation,[status(thm)],[c_170284]) ).
tcf(c_170288,plain,
! [X0: $i,X1: $i] :
( ( sk_c9 = multiply(identity,X0) )
| ( sk_c9 != multiply(X1,iPr_def_16) )
| ( multiply(identity,X0) != multiply(X1,iPr_def_16) ) ),
inference(instantiation,[status(thm)],[c_155639]) ).
tcf(c_170289,plain,
( ( sk_c9 = multiply(identity,sk_c10) )
| ( sk_c9 != multiply(sk_c10,iPr_def_16) )
| ( multiply(identity,sk_c10) != multiply(sk_c10,iPr_def_16) ) ),
inference(instantiation,[status(thm)],[c_170288]) ).
tcf(c_170403,plain,
! [X0: $i,X1: $i] :
( ( multiply(identity,X0) = sk_c9 )
| ( sk_c9 != multiply(X1,iPr_def_16) )
| ( multiply(identity,X0) != multiply(X1,iPr_def_16) ) ),
inference(instantiation,[status(thm)],[c_155642]) ).
tcf(c_170404,plain,
( ( multiply(identity,sk_c10) = sk_c9 )
| ( sk_c9 != multiply(sk_c10,iPr_def_16) )
| ( multiply(identity,sk_c10) != multiply(sk_c10,iPr_def_16) ) ),
inference(instantiation,[status(thm)],[c_170403]) ).
tcf(c_170636,plain,
! [X0: $i,X1: $i] :
( ( multiply(identity,X0) = iPr_def_17 )
| ( iPr_def_17 != multiply(X1,iPr_def_16) )
| ( multiply(identity,X0) != multiply(X1,iPr_def_16) ) ),
inference(instantiation,[status(thm)],[c_155699]) ).
tcf(c_170637,plain,
( ( multiply(identity,sk_c10) = iPr_def_17 )
| ( iPr_def_17 != multiply(sk_c10,iPr_def_16) )
| ( multiply(identity,sk_c10) != multiply(sk_c10,iPr_def_16) ) ),
inference(instantiation,[status(thm)],[c_170636]) ).
tcf(c_170789,plain,
! [X0: $i,X1: $i] :
( ( multiply(X0,X1) = sk_c9 )
| ( sk_c9 != multiply(identity,iPr_def_22) )
| ( multiply(X0,X1) != multiply(identity,iPr_def_22) ) ),
inference(instantiation,[status(thm)],[c_130088]) ).
tcf(c_170792,plain,
( ( multiply(sk_c10,sk_c10) = sk_c9 )
| ( sk_c9 != multiply(identity,iPr_def_22) )
| ( multiply(sk_c10,sk_c10) != multiply(identity,iPr_def_22) ) ),
inference(instantiation,[status(thm)],[c_170789]) ).
tcf(c_171468,plain,
! [X0: $i] :
( ( X0 = identity )
| ( identity != iPr_def_21 )
| ( X0 != iPr_def_21 ) ),
inference(instantiation,[status(thm)],[c_129446]) ).
tcf(c_171471,plain,
( ( sk_c10 = identity )
| ( identity != iPr_def_21 )
| ( sk_c10 != iPr_def_21 ) ),
inference(instantiation,[status(thm)],[c_171468]) ).
tcf(c_171665,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(X2,multiply(X0,X1)) = multiply(identity,iPr_def_20) )
| ( X2 != identity )
| ( multiply(X0,X1) != iPr_def_20 ) ),
inference(instantiation,[status(thm)],[c_135636]) ).
tcf(c_171668,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(X0,multiply(X1,X2)) = sk_c9 )
| ( sk_c9 != multiply(identity,iPr_def_20) )
| ( multiply(X0,multiply(X1,X2)) != multiply(identity,iPr_def_20) ) ),
inference(instantiation,[status(thm)],[c_130088]) ).
tcf(c_171670,plain,
( ( multiply(sk_c10,multiply(sk_c10,sk_c10)) = multiply(identity,iPr_def_20) )
| ( sk_c10 != identity )
| ( multiply(sk_c10,sk_c10) != iPr_def_20 ) ),
inference(instantiation,[status(thm)],[c_171665]) ).
tcf(c_171672,plain,
( ( multiply(sk_c10,multiply(sk_c10,sk_c10)) = sk_c9 )
| ( sk_c9 != multiply(identity,iPr_def_20) )
| ( multiply(sk_c10,multiply(sk_c10,sk_c10)) != multiply(identity,iPr_def_20) ) ),
inference(instantiation,[status(thm)],[c_171668]) ).
tcf(c_173172,plain,
( ( sk_c9 = multiply(sk_c10,sk_c5) )
| ( sk_c9 != iPr_def_22 )
| ( multiply(sk_c10,sk_c5) != iPr_def_22 ) ),
inference(instantiation,[status(thm)],[c_133680]) ).
tcf(c_175927,plain,
( ( iPr_def_18 = iPr_def_19 )
| ( inverse(iPr_def_13) = sk_c1 ) ),
inference(superposition,[status(thm)],[c_125934,c_26891]) ).
tcf(c_175971,plain,
( ( iPr_def_18 = iPr_def_19 )
| ( sk_c1 = sk_c10 ) ),
inference(light_normalisation,[status(thm)],[c_175927,c_31827]) ).
tcf(c_177421,plain,
( ( iPr_def_18 = iPr_def_19 )
| ( sk_c10 = iPr_def_13 ) ),
inference(superposition,[status(thm)],[c_175971,c_81929]) ).
tcf(c_179725,plain,
( ( iPr_def_18 = iPr_def_19 )
| ( iPr_def_13 = iPr_def_19 )
| ( sk_c10 = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_177421,c_621]) ).
tcf(c_181674,plain,
( ( iPr_def_14 = iPr_def_19 )
| ( inverse(iPr_def_15) = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_59681,c_65299]) ).
tcf(c_181680,plain,
( ( iPr_def_14 = iPr_def_19 )
| ( sk_c4 = iPr_def_15 ) ),
inference(light_normalisation,[status(thm)],[c_181674,c_63892]) ).
tcf(c_182274,plain,
( ( sk_c9 = multiply(identity,iPr_def_22) )
| ( sk_c9 != iPr_def_22 )
| ( multiply(identity,iPr_def_22) != iPr_def_22 ) ),
inference(instantiation,[status(thm)],[c_129464]) ).
tcf(c_185814,plain,
( ( iPr_def_14 = iPr_def_19 )
| ( sk_c1 = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_181680,c_104758]) ).
tcf(c_185820,plain,
( ( iPr_def_14 = iPr_def_19 )
| ( sk_c3 = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_181680,c_71330]) ).
tcf(c_185830,plain,
( ( iPr_def_14 = iPr_def_19 )
| ( iPr_def_13 = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_181680,c_63895]) ).
tcf(c_186623,plain,
( ( iPr_def_14 = iPr_def_19 )
| ( inverse(iPr_def_15) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_185814,c_610]) ).
tcf(c_186624,plain,
( ( iPr_def_14 = iPr_def_19 )
| ( sk_c4 = iPr_def_26 ) ),
inference(light_normalisation,[status(thm)],[c_186623,c_63892]) ).
tcf(c_186697,plain,
( ( identity = iPr_def_21 )
| ( iPr_def_21 != iPr_def_22 )
| ( identity != iPr_def_22 ) ),
inference(instantiation,[status(thm)],[c_140048]) ).
tcf(c_186699,plain,
( ( multiply(sk_c3,sk_c10) = iPr_def_21 )
| ( iPr_def_21 != iPr_def_22 )
| ( multiply(sk_c3,sk_c10) != iPr_def_22 ) ),
inference(instantiation,[status(thm)],[c_135341]) ).
tcf(c_189724,plain,
( ( iPr_def_21 = iPr_def_26 )
| ( iPr_def_14 = iPr_def_19 ) ),
inference(global_subsumption_just,[status(thm)],[c_62764,c_669,c_671,c_674,c_597,c_599,c_604,c_605,c_606,c_610,c_635,c_639,c_1027,c_1343,c_1404,c_1405,c_1987,c_1988,c_2156,c_2157,c_2170,c_2185,c_2465,c_3378,c_3799,c_4358,c_4429,c_6862,c_7856,c_7859,c_7922,c_7934,c_8347,c_8596,c_9121,c_9300,c_9733,c_11515,c_12641,c_12809,c_13384,c_22650,c_30265,c_31836,c_32405,c_32404,c_34900,c_34903,c_36249,c_38190,c_39277,c_47870,c_53375,c_55363,c_61796,c_64654,c_72008,c_80137,c_82854,c_82856,c_82861,c_91651,c_91778,c_95024,c_105176,c_110560,c_111887,c_120870,c_120901,c_129859,c_129862,c_130038,c_130071,c_130075,c_130891,c_130898,c_130938,c_131088,c_131087,c_131139,c_131202,c_131232,c_132308,c_133390,c_133391,c_133534,c_133631,c_135354,c_136773,c_138167,c_140008,c_140042,c_140217,c_140361,c_141033,c_145013,c_145763,c_146458,c_147613,c_148502,c_148700,c_155628,c_155648,c_155728,c_159874,c_170287,c_170792,c_171471,c_171670,c_171672,c_173172,c_181680,c_182274,c_185830,c_185820,c_186699,c_186697]) ).
tcf(c_191312,plain,
sk_c10 = iPr_def_15,
inference(global_subsumption_just,[status(thm)],[c_62765,c_671,c_1027,c_3378,c_7922,c_7934,c_8347,c_8596,c_9733,c_31836,c_32404,c_38190,c_39277,c_61796,c_129859,c_129862,c_130891,c_130898,c_131139,c_132308,c_133390,c_133391,c_140008,c_140361,c_145763,c_146458,c_147613,c_155628,c_155648,c_155728,c_159874,c_170287]) ).
tcf(c_191444,plain,
( ( iPr_def_15 = iPr_def_21 )
| ( iPr_def_14 = iPr_def_15 ) ),
inference(demodulation,[status(thm)],[c_56625,c_191312]) ).
tcf(c_191469,plain,
multiply(iPr_def_15,iPr_def_20) = iPr_def_15,
inference(demodulation,[status(thm)],[c_54411,c_191312]) ).
tcf(c_191487,plain,
multiply(iPr_def_13,iPr_def_15) = identity,
inference(demodulation,[status(thm)],[c_41530,c_191312]) ).
tcf(c_191490,plain,
( iPr_def_12
| iPr_def_11
| ( iPr_def_15 = iPr_def_25 ) ),
inference(demodulation,[status(thm)],[c_42087,c_191312]) ).
tcf(c_191493,plain,
( ( iPr_def_15 = iPr_def_26 )
| ( sk_c9 = iPr_def_13 ) ),
inference(demodulation,[status(thm)],[c_664,c_191312]) ).
tcf(c_191500,plain,
( ( iPr_def_15 = iPr_def_26 )
| ( sk_c9 = iPr_def_17 ) ),
inference(demodulation,[status(thm)],[c_661,c_191312]) ).
tcf(c_191501,plain,
( ( iPr_def_15 = iPr_def_26 )
| ( sk_c8 = iPr_def_16 ) ),
inference(demodulation,[status(thm)],[c_660,c_191312]) ).
tcf(c_191503,plain,
( ( iPr_def_15 = iPr_def_25 )
| ( sk_c9 = iPr_def_13 ) ),
inference(demodulation,[status(thm)],[c_658,c_191312]) ).
tcf(c_191506,plain,
( ( iPr_def_15 = iPr_def_25 )
| ( sk_c9 = iPr_def_17 ) ),
inference(demodulation,[status(thm)],[c_655,c_191312]) ).
tcf(c_191507,plain,
( ( iPr_def_15 = iPr_def_25 )
| ( sk_c8 = iPr_def_16 ) ),
inference(demodulation,[status(thm)],[c_654,c_191312]) ).
tcf(c_191509,plain,
( ( iPr_def_15 = iPr_def_19 )
| ( sk_c9 = iPr_def_24 ) ),
inference(demodulation,[status(thm)],[c_651,c_191312]) ).
tcf(c_191540,plain,
inverse(iPr_def_15) = iPr_def_13,
inference(demodulation,[status(thm)],[c_597,c_191312]) ).
tcf(c_191902,plain,
iPr_def_15 = iPr_def_26,
inference(global_subsumption_just,[status(thm)],[c_191493,c_153,c_671,c_599,c_610,c_1027,c_1987,c_1988,c_2156,c_2157,c_2467,c_2561,c_3087,c_3378,c_4262,c_7922,c_7934,c_8347,c_8596,c_9733,c_15430,c_18322,c_26160,c_31836,c_32404,c_37911,c_38190,c_39277,c_45185,c_45972,c_48924,c_56731,c_57954,c_61796,c_129859,c_129862,c_130891,c_130897,c_130898,c_131139,c_132308,c_132884,c_132978,c_133390,c_133391,c_133420,c_133453,c_140008,c_140361,c_141012,c_142509,c_145761,c_145762,c_145763,c_146347,c_146458,c_146699,c_147613,c_155628,c_155648,c_155728,c_159874,c_159905,c_168298,c_170287,c_170289,c_170404,c_191501,c_191500]) ).
tcf(c_191904,plain,
( ( iPr_def_15 = iPr_def_21 )
| ( iPr_def_14 = iPr_def_19 ) ),
inference(demodulation,[status(thm)],[c_189724,c_191902]) ).
tcf(c_192004,plain,
multiply(inverse(iPr_def_15),iPr_def_15) = iPr_def_20,
inference(superposition,[status(thm)],[c_191469,c_99164]) ).
tcf(c_192006,plain,
identity = iPr_def_20,
inference(light_normalisation,[status(thm)],[c_192004,c_191487,c_191540]) ).
tcf(c_192007,plain,
! [X0: $i] : multiply(X0,iPr_def_20) = X0,
inference(demodulation,[status(thm)],[c_111746,c_192006]) ).
tcf(c_192080,plain,
( ( iPr_def_15 = iPr_def_25 )
| ( iPr_def_13 = iPr_def_24 )
| ( sk_c9 = iPr_def_13 ) ),
inference(superposition,[status(thm)],[c_191503,c_652]) ).
tcf(c_192334,plain,
( ( iPr_def_15 = iPr_def_25 )
| iPr_def_11 ),
inference(global_subsumption_just,[status(thm)],[c_191490,c_671,c_2007,c_3378,c_32404,c_129862,c_130891,c_140361,c_141012,c_145762,c_191490,c_191507,c_191506]) ).
tcf(c_192335,plain,
( iPr_def_11
| ( iPr_def_15 = iPr_def_25 ) ),
inference(renaming,[status(thm)],[c_192334]) ).
tcf(c_193056,plain,
( ~ iPr_def_12
| ( multiply(sk_c10,iPr_def_20) != sk_c9 ) ),
inference(global_subsumption_just,[status(thm)],[c_42707,c_671,c_1027,c_3378,c_3371,c_7922,c_7934,c_8347,c_8596,c_9733,c_31836,c_32404,c_38190,c_39277,c_61796,c_129859,c_129862,c_130891,c_130898,c_131139,c_132308,c_133390,c_133391,c_140008,c_140361,c_145763,c_146458,c_147613,c_155628,c_155648,c_155728,c_159874,c_170287]) ).
tcf(c_193058,plain,
( ~ iPr_def_12
| ( multiply(iPr_def_15,iPr_def_20) != sk_c9 ) ),
inference(light_normalisation,[status(thm)],[c_193056,c_191312]) ).
tcf(c_193059,plain,
( ~ iPr_def_12
| ( sk_c9 != iPr_def_15 ) ),
inference(demodulation,[status(thm)],[c_193058,c_192007]) ).
tcf(c_193083,plain,
( ( sk_c9 = iPr_def_13 )
| ~ iPr_def_12
| ( iPr_def_15 != iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_652,c_193059]) ).
tcf(c_193084,plain,
( ( sk_c9 = iPr_def_17 )
| ~ iPr_def_12
| ( iPr_def_15 != iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_649,c_193059]) ).
tcf(c_193087,plain,
( ( sk_c9 = iPr_def_13 )
| ~ iPr_def_12
| ( iPr_def_15 != iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_634,c_193059]) ).
tcf(c_193088,plain,
( ( sk_c9 = iPr_def_17 )
| ~ iPr_def_12
| ( iPr_def_15 != iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_631,c_193059]) ).
tcf(c_193158,plain,
( ~ iPr_def_12
| ( multiply(sk_c10,iPr_def_16) != sk_c9 ) ),
inference(global_subsumption_just,[status(thm)],[c_42714,c_3378,c_8742,c_32815]) ).
tcf(c_193167,plain,
( ~ iPr_def_11
| ( sk_c9 != identity ) ),
inference(global_subsumption_just,[status(thm)],[c_42797,c_63913,c_138167,c_140217,c_148502,c_192006]) ).
tcf(c_193169,plain,
( ~ iPr_def_11
| ( sk_c9 != iPr_def_20 ) ),
inference(light_normalisation,[status(thm)],[c_193167,c_192006]) ).
tcf(c_193184,plain,
( ( iPr_def_15 = iPr_def_19 )
| ~ iPr_def_11
| ( iPr_def_20 != iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_191509,c_193169]) ).
tcf(c_193197,plain,
( ( sk_c9 = iPr_def_13 )
| ~ iPr_def_11
| ( iPr_def_20 != iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_634,c_193169]) ).
tcf(c_193476,plain,
( iPr_def_12
| iPr_def_11
| ( iPr_def_14 = iPr_def_15 )
| ( iPr_def_13 != iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_191444,c_91778]) ).
tcf(c_193523,plain,
( ( iPr_def_15 != iPr_def_24 )
| ~ iPr_def_12 ),
inference(global_subsumption_just,[status(thm)],[c_193083,c_669,c_671,c_597,c_648,c_1027,c_1343,c_1459,c_3378,c_7922,c_7934,c_8347,c_8596,c_9733,c_11482,c_11483,c_31836,c_32404,c_32523,c_35719,c_36799,c_38190,c_39277,c_61796,c_72110,c_74520,c_129859,c_129862,c_130891,c_130898,c_131139,c_132308,c_133390,c_133391,c_140008,c_140361,c_141012,c_145762,c_145763,c_146458,c_147613,c_155628,c_155648,c_155728,c_159874,c_170287,c_193084,c_193083]) ).
tcf(c_193524,plain,
( ~ iPr_def_12
| ( iPr_def_15 != iPr_def_24 ) ),
inference(renaming,[status(thm)],[c_193523]) ).
tcf(c_193529,plain,
( ( iPr_def_14 = iPr_def_19 )
| ~ iPr_def_12
| ( iPr_def_15 != iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_44689,c_193524]) ).
tcf(c_193571,plain,
( ( iPr_def_15 != iPr_def_21 )
| ~ iPr_def_12 ),
inference(global_subsumption_just,[status(thm)],[c_193087,c_669,c_671,c_597,c_630,c_1027,c_1343,c_1459,c_3378,c_7922,c_7934,c_8347,c_8596,c_9733,c_11482,c_11483,c_31836,c_32404,c_32523,c_36799,c_38190,c_39277,c_61796,c_72005,c_74516,c_129859,c_129862,c_130891,c_130898,c_131139,c_132308,c_133390,c_133391,c_140008,c_140361,c_141012,c_145762,c_145763,c_146458,c_147613,c_155628,c_155648,c_155728,c_159874,c_170287,c_193088,c_193087,c_193158]) ).
tcf(c_193572,plain,
( ~ iPr_def_12
| ( iPr_def_15 != iPr_def_21 ) ),
inference(renaming,[status(thm)],[c_193571]) ).
tcf(c_193577,plain,
( ( iPr_def_14 = iPr_def_15 )
| ~ iPr_def_12 ),
inference(superposition,[status(thm)],[c_191444,c_193572]) ).
tcf(c_194253,plain,
iPr_def_14 = iPr_def_19,
inference(global_subsumption_just,[status(thm)],[c_191904,c_669,c_671,c_597,c_610,c_1027,c_1343,c_1405,c_2156,c_2157,c_2170,c_2738,c_2900,c_3378,c_4429,c_7856,c_7859,c_7922,c_7934,c_8347,c_8596,c_9733,c_11515,c_11517,c_12809,c_31836,c_32404,c_36249,c_38190,c_39277,c_47870,c_48416,c_61796,c_67016,c_72860,c_78892,c_80137,c_91651,c_91778,c_103999,c_103997,c_113663,c_113664,c_120870,c_129859,c_129862,c_130891,c_130898,c_131139,c_132308,c_133390,c_133391,c_140008,c_140361,c_145763,c_146458,c_147613,c_155628,c_155648,c_155728,c_159874,c_170287,c_185830,c_186697,c_189724,c_191902,c_191904,c_193167,c_193197,c_193529]) ).
tcf(c_194510,plain,
( ( iPr_def_15 = iPr_def_25 )
| ( iPr_def_13 = iPr_def_24 ) ),
inference(global_subsumption_just,[status(thm)],[c_192080,c_153,c_154,c_669,c_671,c_597,c_1343,c_2170,c_3092,c_3799,c_6561,c_11482,c_12528,c_13556,c_13839,c_32404,c_36384,c_38190,c_45187,c_46164,c_62128,c_72110,c_75107,c_79717,c_83296,c_83297,c_85561,c_106133,c_116621,c_118714,c_129512,c_129547,c_129778,c_129795,c_129859,c_129862,c_130247,c_130891,c_130897,c_130898,c_133386,c_140008,c_140017,c_140361,c_141012,c_142520,c_142521,c_145456,c_145761,c_145763,c_147613,c_155648,c_168298,c_170289,c_191507,c_191506,c_191503,c_192335,c_193167]) ).
tcf(c_194512,plain,
iPr_def_15 = iPr_def_25,
inference(global_subsumption_just,[status(thm)],[c_194510,c_32404,c_38190,c_45187,c_49975,c_75142,c_78892,c_85060,c_129859,c_129862,c_130891,c_130898,c_133390,c_133391,c_140008,c_140361,c_145763,c_146458,c_147613,c_155648,c_159874,c_191507,c_191506,c_191503,c_192335,c_193167,c_194510]) ).
tcf(c_196851,plain,
iPr_def_14 = iPr_def_19,
inference(global_subsumption_just,[status(thm)],[c_186624,c_194253]) ).
tcf(c_196983,plain,
inverse(iPr_def_14) = sk_c6,
inference(demodulation,[status(thm)],[c_37752,c_196851]) ).
tcf(c_196984,plain,
multiply(sk_c6,iPr_def_14) = identity,
inference(demodulation,[status(thm)],[c_37711,c_196851]) ).
tcf(c_197159,plain,
sk_c6 = sk_c7,
inference(demodulation,[status(thm)],[c_45328,c_196983]) ).
tcf(c_197186,plain,
multiply(iPr_def_16,iPr_def_13) = sk_c6,
inference(demodulation,[status(thm)],[c_36924,c_197159]) ).
tcf(c_197459,plain,
sk_c10 = iPr_def_15,
inference(global_subsumption_just,[status(thm)],[c_179725,c_191312]) ).
tcf(c_197474,plain,
( ( iPr_def_20 = iPr_def_24 )
| ( iPr_def_14 = iPr_def_15 ) ),
inference(demodulation,[status(thm)],[c_95509,c_197459]) ).
tcf(c_197548,plain,
( ( iPr_def_20 = iPr_def_25 )
| ( iPr_def_14 = iPr_def_15 ) ),
inference(demodulation,[status(thm)],[c_28282,c_197459]) ).
tcf(c_197575,plain,
! [X0: $i] : multiply(sk_c4,multiply(iPr_def_15,X0)) = multiply(iPr_def_20,X0),
inference(demodulation,[status(thm)],[c_3591,c_197459]) ).
tcf(c_197680,plain,
multiply(iPr_def_14,iPr_def_16) = iPr_def_15,
inference(demodulation,[status(thm)],[c_7821,c_197459]) ).
tcf(c_197698,plain,
( ( iPr_def_15 = iPr_def_26 )
| ( sk_c9 = iPr_def_13 ) ),
inference(demodulation,[status(thm)],[c_664,c_197459]) ).
tcf(c_197703,plain,
( ( iPr_def_15 = iPr_def_25 )
| ( sk_c9 = iPr_def_13 ) ),
inference(demodulation,[status(thm)],[c_658,c_197459]) ).
tcf(c_197708,plain,
( ( iPr_def_15 = iPr_def_18 )
| ( sk_c9 = iPr_def_24 ) ),
inference(demodulation,[status(thm)],[c_650,c_197459]) ).
tcf(c_197709,plain,
( ( iPr_def_14 = iPr_def_15 )
| ( sk_c9 = iPr_def_24 ) ),
inference(demodulation,[status(thm)],[c_647,c_197459]) ).
tcf(c_197717,plain,
multiply(iPr_def_15,sk_c5) = iPr_def_21,
inference(demodulation,[status(thm)],[c_605,c_197459]) ).
tcf(c_197718,plain,
multiply(sk_c4,iPr_def_15) = iPr_def_20,
inference(demodulation,[status(thm)],[c_604,c_197459]) ).
tcf(c_197722,plain,
inverse(iPr_def_15) = iPr_def_13,
inference(demodulation,[status(thm)],[c_597,c_197459]) ).
tcf(c_197957,plain,
! [X0: $i] : multiply(iPr_def_20,X0) = X0,
inference(light_normalisation,[status(thm)],[c_197575,c_63843]) ).
tcf(c_198132,plain,
identity = iPr_def_20,
inference(demodulation,[status(thm)],[c_63840,c_197718]) ).
tcf(c_198183,plain,
multiply(sk_c2,iPr_def_23) = iPr_def_20,
inference(demodulation,[status(thm)],[c_49959,c_198132]) ).
tcf(c_198200,plain,
inverse(iPr_def_20) = iPr_def_20,
inference(demodulation,[status(thm)],[c_26097,c_198132]) ).
tcf(c_198201,plain,
! [X0: $i] : multiply(X0,iPr_def_20) = X0,
inference(demodulation,[status(thm)],[c_26068,c_198132]) ).
tcf(c_198381,plain,
iPr_def_15 = iPr_def_26,
inference(global_subsumption_just,[status(thm)],[c_197698,c_153,c_671,c_599,c_610,c_1027,c_1987,c_1988,c_2156,c_2157,c_2467,c_2561,c_3087,c_3378,c_4262,c_7922,c_7934,c_8347,c_8596,c_9733,c_15430,c_18322,c_26160,c_31836,c_32404,c_37911,c_38190,c_39277,c_45185,c_45972,c_48924,c_56731,c_57954,c_61796,c_129859,c_129862,c_130891,c_130897,c_130898,c_131139,c_132308,c_132884,c_132978,c_133390,c_133391,c_133420,c_133453,c_140008,c_140361,c_141012,c_142509,c_145761,c_145762,c_145763,c_146347,c_146458,c_146699,c_147613,c_155628,c_155648,c_155728,c_159874,c_159905,c_168298,c_170287,c_170289,c_170404,c_191501,c_191500]) ).
tcf(c_198406,plain,
inverse(iPr_def_15) = sk_c1,
inference(demodulation,[status(thm)],[c_26891,c_198381]) ).
tcf(c_198430,plain,
sk_c1 = iPr_def_13,
inference(light_normalisation,[status(thm)],[c_198406,c_197722]) ).
tcf(c_198545,plain,
iPr_def_15 = iPr_def_25,
inference(global_subsumption_just,[status(thm)],[c_197703,c_194512]) ).
tcf(c_198650,plain,
multiply(inverse(iPr_def_14),iPr_def_15) = iPr_def_16,
inference(superposition,[status(thm)],[c_197680,c_24266]) ).
tcf(c_198653,plain,
multiply(sk_c6,iPr_def_15) = iPr_def_16,
inference(light_normalisation,[status(thm)],[c_198650,c_196983]) ).
tcf(c_198664,plain,
multiply(sk_c6,iPr_def_14) = iPr_def_20,
inference(light_normalisation,[status(thm)],[c_196984,c_198132]) ).
tcf(c_198713,plain,
( iPr_def_12
| iPr_def_11
| iPr_def_10
| ( iPr_def_15 = iPr_def_18 )
| ( iPr_def_13 != iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_197708,c_611]) ).
tcf(c_198773,plain,
( iPr_def_12
| iPr_def_11
| iPr_def_10
| ( iPr_def_14 = iPr_def_15 )
| ( iPr_def_13 != iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_197709,c_611]) ).
tcf(c_199699,plain,
( ( iPr_def_15 = iPr_def_20 )
| ( iPr_def_14 = iPr_def_15 ) ),
inference(light_normalisation,[status(thm)],[c_197548,c_198545]) ).
tcf(c_199708,plain,
( ( iPr_def_14 = iPr_def_15 )
| ( inverse(iPr_def_15) = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_199699,c_198200]) ).
tcf(c_199709,plain,
( ( iPr_def_14 = iPr_def_15 )
| ( iPr_def_13 = iPr_def_15 ) ),
inference(light_normalisation,[status(thm)],[c_199708,c_197722]) ).
tcf(c_199726,plain,
( iPr_def_12
| iPr_def_11
| ( iPr_def_13 != iPr_def_24 ) ),
inference(global_subsumption_just,[status(thm)],[c_198713,c_92865]) ).
tcf(c_199749,plain,
iPr_def_14 = iPr_def_15,
inference(global_subsumption_just,[status(thm)],[c_198773,c_669,c_671,c_674,c_597,c_599,c_604,c_605,c_606,c_610,c_635,c_639,c_1027,c_1343,c_1404,c_1405,c_1987,c_1988,c_2156,c_2157,c_2170,c_2185,c_2465,c_3378,c_3799,c_4358,c_4429,c_6862,c_7856,c_7859,c_7922,c_7934,c_8347,c_8596,c_9121,c_9300,c_9733,c_11515,c_12641,c_12809,c_13384,c_22650,c_30265,c_31836,c_32405,c_32404,c_34900,c_34903,c_36249,c_38190,c_39277,c_47870,c_53375,c_55363,c_60084,c_61796,c_64654,c_72008,c_80137,c_82854,c_82856,c_82861,c_91651,c_91778,c_95024,c_105176,c_110560,c_111887,c_120870,c_120901,c_129859,c_129862,c_130038,c_130071,c_130075,c_130891,c_130898,c_130938,c_131088,c_131087,c_131139,c_131202,c_131232,c_132308,c_133390,c_133391,c_133534,c_133631,c_135354,c_136773,c_138167,c_140008,c_140042,c_140217,c_140361,c_141033,c_145013,c_145763,c_146458,c_147613,c_148502,c_148700,c_155628,c_155648,c_155728,c_159874,c_170287,c_170792,c_171471,c_171670,c_171672,c_173172,c_181680,c_182274,c_185830,c_185820,c_186699,c_186697,c_193184,c_193476,c_193577,c_197474,c_199709]) ).
tcf(c_199751,plain,
multiply(sk_c6,iPr_def_14) = iPr_def_16,
inference(demodulation,[status(thm)],[c_198653,c_199749]) ).
tcf(c_199762,plain,
multiply(iPr_def_14,sk_c5) = iPr_def_21,
inference(demodulation,[status(thm)],[c_197717,c_199749]) ).
tcf(c_199773,plain,
inverse(iPr_def_14) = iPr_def_13,
inference(demodulation,[status(thm)],[c_197722,c_199749]) ).
tcf(c_199775,plain,
sk_c10 = iPr_def_14,
inference(demodulation,[status(thm)],[c_197459,c_199749]) ).
tcf(c_199796,plain,
iPr_def_16 = iPr_def_20,
inference(demodulation,[status(thm)],[c_198664,c_199751]) ).
tcf(c_199799,plain,
! [X0: $i] : multiply(X0,iPr_def_16) = X0,
inference(demodulation,[status(thm)],[c_198201,c_199796]) ).
tcf(c_199801,plain,
! [X0: $i] : multiply(iPr_def_16,X0) = X0,
inference(demodulation,[status(thm)],[c_197957,c_199796]) ).
tcf(c_199802,plain,
multiply(sk_c2,iPr_def_23) = iPr_def_16,
inference(demodulation,[status(thm)],[c_198183,c_199796]) ).
tcf(c_199804,plain,
inverse(iPr_def_16) = iPr_def_16,
inference(demodulation,[status(thm)],[c_198200,c_199796]) ).
tcf(c_199805,plain,
identity = iPr_def_16,
inference(demodulation,[status(thm)],[c_198132,c_199796]) ).
tcf(c_199817,plain,
( ( sk_c5 = iPr_def_16 )
| ( sk_c9 = iPr_def_13 ) ),
inference(demodulation,[status(thm)],[c_628,c_199796]) ).
tcf(c_199818,plain,
( ( sk_c5 = iPr_def_16 )
| ( sk_c9 = iPr_def_17 ) ),
inference(demodulation,[status(thm)],[c_625,c_199796]) ).
tcf(c_199819,plain,
( ( sk_c5 = iPr_def_16 )
| ( sk_c8 = iPr_def_16 ) ),
inference(demodulation,[status(thm)],[c_624,c_199796]) ).
tcf(c_199836,plain,
sk_c6 = iPr_def_13,
inference(demodulation,[status(thm)],[c_197186,c_199801]) ).
tcf(c_199844,plain,
multiply(sk_c10,iPr_def_16) = sk_c10,
inference(instantiation,[status(thm)],[c_199799]) ).
tcf(c_199846,plain,
sk_c5 = iPr_def_16,
inference(global_subsumption_just,[status(thm)],[c_199817,c_153,c_154,c_669,c_671,c_597,c_599,c_601,c_610,c_1027,c_1343,c_1987,c_1988,c_2156,c_2157,c_2170,c_2467,c_2561,c_3087,c_3092,c_3378,c_3577,c_4262,c_7704,c_7922,c_7934,c_8347,c_8596,c_8742,c_9733,c_11482,c_11515,c_11517,c_13039,c_13839,c_15430,c_18322,c_26160,c_31160,c_31836,c_32404,c_32815,c_36802,c_37911,c_38190,c_39277,c_40825,c_45185,c_45972,c_48924,c_49975,c_56731,c_57601,c_57954,c_61796,c_72110,c_79717,c_83296,c_83297,c_119970,c_129512,c_129550,c_129631,c_129778,c_129794,c_129859,c_129862,c_130247,c_130891,c_130897,c_130898,c_131139,c_132298,c_132308,c_132884,c_132978,c_133281,c_133284,c_133311,c_133390,c_133391,c_133420,c_133453,c_140008,c_140361,c_141012,c_142230,c_142509,c_145759,c_145761,c_145762,c_145763,c_146347,c_146458,c_146699,c_147613,c_155628,c_155648,c_155728,c_159874,c_159905,c_167995,c_168293,c_168298,c_169101,c_170287,c_170289,c_170404,c_170637,c_191501,c_191500,c_193167,c_198430,c_199836,c_199844,c_199817,c_199818,c_199819]) ).
tcf(c_199931,plain,
sk_c9 = iPr_def_24,
inference(global_subsumption_just,[status(thm)],[c_8184,c_153,c_154,c_669,c_671,c_597,c_599,c_610,c_1027,c_1343,c_1722,c_1987,c_1988,c_2156,c_2157,c_2170,c_2467,c_2561,c_3087,c_3092,c_3378,c_3577,c_4262,c_7704,c_7922,c_7934,c_8347,c_8596,c_8742,c_9733,c_11515,c_11517,c_13039,c_13706,c_13839,c_13925,c_15430,c_18322,c_26160,c_31160,c_31836,c_32404,c_32815,c_36802,c_37911,c_38190,c_39277,c_40825,c_45185,c_45972,c_48924,c_56731,c_57601,c_57954,c_61796,c_79717,c_129512,c_129778,c_129859,c_129862,c_130247,c_130891,c_130897,c_130898,c_131139,c_132308,c_132884,c_132978,c_133390,c_133391,c_133420,c_133453,c_138397,c_140008,c_140361,c_141012,c_142509,c_145761,c_145762,c_145763,c_146347,c_146458,c_146699,c_147613,c_155628,c_155648,c_155728,c_159874,c_159905,c_167995,c_168293,c_168298,c_169101,c_170287,c_170289,c_170404,c_191501,c_191500,c_193167,c_198430,c_199836,c_199844]) ).
tcf(c_199957,plain,
( ( iPr_def_13 = iPr_def_24 )
| ( sk_c3 = iPr_def_23 ) ),
inference(demodulation,[status(thm)],[c_646,c_199931]) ).
tcf(c_199962,plain,
( ( iPr_def_21 = iPr_def_24 )
| ( iPr_def_13 = iPr_def_24 ) ),
inference(demodulation,[status(thm)],[c_634,c_199931]) ).
tcf(c_199964,plain,
( ( iPr_def_21 = iPr_def_24 )
| ( sk_c8 = iPr_def_16 ) ),
inference(demodulation,[status(thm)],[c_630,c_199931]) ).
tcf(c_199993,plain,
sk_c3 = iPr_def_23,
inference(global_subsumption_just,[status(thm)],[c_199957,c_153,c_646,c_1568,c_3378,c_8742,c_10994,c_10995,c_12420,c_12546,c_12900,c_32815,c_38190,c_40825,c_78892,c_85060,c_110087,c_130897,c_133386,c_133389,c_133420,c_133453,c_140010,c_155628,c_155728,c_168298,c_170287,c_170289,c_193167,c_199805,c_199844,c_199957]) ).
tcf(c_200005,plain,
multiply(sk_c2,iPr_def_23) = iPr_def_24,
inference(demodulation,[status(thm)],[c_608,c_199993]) ).
tcf(c_200006,plain,
iPr_def_16 = iPr_def_24,
inference(light_normalisation,[status(thm)],[c_200005,c_199802]) ).
tcf(c_200008,plain,
sk_c9 = iPr_def_16,
inference(demodulation,[status(thm)],[c_199931,c_200006]) ).
tcf(c_200010,plain,
( iPr_def_12
| iPr_def_11
| ( iPr_def_13 != iPr_def_16 ) ),
inference(demodulation,[status(thm)],[c_199726,c_200006]) ).
tcf(c_200056,plain,
iPr_def_21 = iPr_def_24,
inference(global_subsumption_just,[status(thm)],[c_199962,c_671,c_1757,c_3378,c_6158,c_32404,c_110842,c_129862,c_130891,c_140010,c_140361,c_141012,c_145762,c_193167,c_199805,c_199775,c_199964,c_200008]) ).
tcf(c_200058,plain,
iPr_def_16 = iPr_def_21,
inference(light_normalisation,[status(thm)],[c_200056,c_200006]) ).
tcf(c_200121,plain,
multiply(iPr_def_14,iPr_def_16) = iPr_def_16,
inference(light_normalisation,[status(thm)],[c_199762,c_199846,c_200058]) ).
tcf(c_200122,plain,
iPr_def_14 = iPr_def_16,
inference(demodulation,[status(thm)],[c_200121,c_199799]) ).
tcf(c_200124,plain,
inverse(iPr_def_14) = iPr_def_14,
inference(demodulation,[status(thm)],[c_199804,c_200122]) ).
tcf(c_200129,plain,
identity = iPr_def_14,
inference(demodulation,[status(thm)],[c_199805,c_200122]) ).
tcf(c_200132,plain,
iPr_def_13 = iPr_def_14,
inference(light_normalisation,[status(thm)],[c_200124,c_199773]) ).
tcf(c_200133,plain,
iPr_def_13 = iPr_def_16,
inference(demodulation,[status(thm)],[c_200122,c_200132]) ).
tcf(c_200143,plain,
iPr_def_13 = iPr_def_19,
inference(demodulation,[status(thm)],[c_196851,c_200132]) ).
tcf(c_200144,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_200129,c_200133,c_200143,c_200010,c_200008,c_199805,c_199749,c_194253,c_191902,c_191312,c_165978,c_165976,c_140830,c_140366,c_140010,c_139769,c_130285,c_129862,c_129859,c_123509,c_48920,c_48919,c_48656,c_45369,c_37926,c_29942,c_28705,c_17682,c_15440,c_12809,c_11517,c_11519,c_11515,c_7325,c_5835,c_5823,c_5157,c_4510,c_2465,c_2157,c_2156,c_2036,c_2035,c_1988,c_1987,c_1929,c_1928,c_1405,c_1404,c_1343,c_610,c_603,c_599,c_598,c_597,c_674,c_671,c_669,c_154]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GRP221-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.10/0.36 % Computer : n019.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Wed Sep 23 14:10:49 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.37 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.14/0.40 Running first-order theorem proving
% 0.14/0.40 Running: /export/starexec/sandbox2/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.14/0.41
% 0.14/0.41 % ======== iProver multi-core TPTP/SMT =========
% 0.14/0.41
% 0.14/0.41 % Detected problem language: tptp
% 0.14/0.43 % Proving...
% 38.14/7.95 % SZS status Started for theBenchmark.p
% 38.14/7.95 % SZS status Unsatisfiable for theBenchmark.p
% 38.14/7.95
% 38.14/7.95 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 38.14/7.95
% 38.14/7.95 % ------ iProver source info
% 38.14/7.95
% 38.14/7.95 % git: date: 2026-07-19 20:42:38 +0200
% 38.14/7.95 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 38.14/7.95 % git: non_committed_changes: false
% 38.14/7.95
% 38.14/7.95 % ------ Parsing...% successful
% 38.14/7.95
% 38.14/7.95
% 38.14/7.95 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 38.14/7.95
% 38.14/7.95 % ------ Preprocessing... sup_sim: 0 sf_s rm: 0 0s sf_e pe_s pe_e %
% 38.14/7.95
% 38.14/7.95 % ------ Preprocessing... gs_s sp: 5 0s gs_e snvd_s sp: 0 0s snvd_e %
% 38.14/7.95
% 38.14/7.95 % ------ Preprocessing... sf_s rm: 0 0s sf_e
% 38.14/7.95 % ------ Proving...
% 38.14/7.95 % ------ Problem Properties
% 38.14/7.95
% 38.14/7.95 %
% 38.14/7.95 % clauses 69
% 38.14/7.95 % conjectures 52
% 38.14/7.95 % EPR 49
% 38.14/7.95 % Horn 20
% 38.14/7.95 % unary 17
% 38.14/7.95 % binary 48
% 38.14/7.95 % lits 126
% 38.14/7.95 % lits eq 120
% 38.14/7.96 % fd_pure 0
% 38.14/7.96 % fd_pseudo 0
% 38.14/7.96 % fd_cond 0
% 38.14/7.96 % fd_pseudo_cond 0
% 38.14/7.96 % AC symbols 0
% 38.14/7.96
% 38.14/7.96 % ------ Schedule dynamic 5 is on
% 38.14/7.96
% 38.14/7.96 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 38.14/7.96
% 38.14/7.96
% 38.14/7.96 % ------
% 38.14/7.96 % Current options:
% 38.14/7.96 % ------
% 38.14/7.96
% 38.14/7.96
% 38.14/7.96 %
% 38.14/7.96
% 38.14/7.96 % ------ Proving...
% 38.14/7.96 %
% 38.14/7.96
% 38.14/7.96 % SZS status Unsatisfiable for theBenchmark.p
% 38.14/7.96
% 38.14/7.96 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 38.14/7.97
% 38.14/7.97
%------------------------------------------------------------------------------