%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : GRP378-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 : n007.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 01:33:27 PM UTC 2026
% Result : Unsatisfiable 53.54s 9.83s
% Output : CNFRefutation 53.54s
% Verified :
% SZS Type : Refutation
% Derivation depth : 49
% Number of leaves : 48
% Syntax : Number of formulae : 840 ( 172 unt; 11 def)
% Number of atoms : 3274 (1856 equ)
% Maximal formula atoms : 15 ( 3 avg)
% Number of connectives : 2096 ( 892 ~;1204 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 24 ( 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 : 18 ( 16 usr; 17 prp; 0-2 aty)
% Number of functors : 12 ( 12 usr; 10 con; 0-2 aty)
% Number of variables : 419 ( 0 sgn 419 !; 0 ?; 379 :)
% 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,
( multiply(sk_c3,sk_c11) = sk_c10
| inverse(sk_c11) = sk_c10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_1) ).
fof(f6,plain,
( sk_c10 = multiply(sk_c3,sk_c11)
| inverse(sk_c11) = sk_c10 ),
inference(reorient_equations,[],[f5]) ).
fof(f7,negated_conjecture,
( inverse(sk_c3) = sk_c11
| inverse(sk_c11) = sk_c10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_2) ).
fof(f8,plain,
( sk_c11 = inverse(sk_c3)
| inverse(sk_c11) = sk_c10 ),
inference(reorient_equations,[],[f7]) ).
fof(f9,negated_conjecture,
( multiply(sk_c4,sk_c10) = sk_c9
| inverse(sk_c11) = sk_c10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_3) ).
fof(f10,negated_conjecture,
( inverse(sk_c4) = sk_c10
| inverse(sk_c11) = sk_c10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_4) ).
fof(f11,plain,
( sk_c10 = inverse(sk_c4)
| inverse(sk_c11) = sk_c10 ),
inference(reorient_equations,[],[f10]) ).
fof(f12,negated_conjecture,
( multiply(sk_c5,sk_c8) = sk_c11
| inverse(sk_c11) = sk_c10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_5) ).
fof(f13,plain,
( sk_c11 = multiply(sk_c5,sk_c8)
| inverse(sk_c11) = sk_c10 ),
inference(reorient_equations,[],[f12]) ).
fof(f14,negated_conjecture,
( inverse(sk_c5) = sk_c8
| inverse(sk_c11) = sk_c10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_6) ).
fof(f15,plain,
( sk_c8 = inverse(sk_c5)
| inverse(sk_c11) = sk_c10 ),
inference(reorient_equations,[],[f14]) ).
fof(f16,negated_conjecture,
( multiply(sk_c8,sk_c10) = sk_c11
| inverse(sk_c11) = sk_c10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_7) ).
fof(f17,plain,
( sk_c11 = multiply(sk_c8,sk_c10)
| inverse(sk_c11) = sk_c10 ),
inference(reorient_equations,[],[f16]) ).
fof(f23,negated_conjecture,
( multiply(sk_c3,sk_c11) = sk_c10
| multiply(sk_c11,sk_c9) = sk_c10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_11) ).
fof(f24,plain,
( sk_c10 = multiply(sk_c3,sk_c11)
| sk_c10 = multiply(sk_c11,sk_c9) ),
inference(reorient_equations,[],[f23]) ).
fof(f25,negated_conjecture,
( inverse(sk_c3) = sk_c11
| multiply(sk_c11,sk_c9) = sk_c10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_12) ).
fof(f26,plain,
( sk_c11 = inverse(sk_c3)
| sk_c10 = multiply(sk_c11,sk_c9) ),
inference(reorient_equations,[],[f25]) ).
fof(f27,negated_conjecture,
( multiply(sk_c4,sk_c10) = sk_c9
| multiply(sk_c11,sk_c9) = sk_c10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_13) ).
fof(f28,plain,
( multiply(sk_c4,sk_c10) = sk_c9
| sk_c10 = multiply(sk_c11,sk_c9) ),
inference(reorient_equations,[],[f27]) ).
fof(f29,negated_conjecture,
( inverse(sk_c4) = sk_c10
| multiply(sk_c11,sk_c9) = sk_c10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_14) ).
fof(f30,plain,
( sk_c10 = inverse(sk_c4)
| sk_c10 = multiply(sk_c11,sk_c9) ),
inference(reorient_equations,[],[f29]) ).
fof(f31,negated_conjecture,
( multiply(sk_c5,sk_c8) = sk_c11
| multiply(sk_c11,sk_c9) = sk_c10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_15) ).
fof(f32,plain,
( sk_c11 = multiply(sk_c5,sk_c8)
| sk_c10 = multiply(sk_c11,sk_c9) ),
inference(reorient_equations,[],[f31]) ).
fof(f33,negated_conjecture,
( inverse(sk_c5) = sk_c8
| multiply(sk_c11,sk_c9) = sk_c10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_16) ).
fof(f34,plain,
( sk_c8 = inverse(sk_c5)
| sk_c10 = multiply(sk_c11,sk_c9) ),
inference(reorient_equations,[],[f33]) ).
fof(f35,negated_conjecture,
( multiply(sk_c8,sk_c10) = sk_c11
| multiply(sk_c11,sk_c9) = sk_c10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_17) ).
fof(f36,plain,
( sk_c11 = multiply(sk_c8,sk_c10)
| sk_c10 = multiply(sk_c11,sk_c9) ),
inference(reorient_equations,[],[f35]) ).
fof(f43,negated_conjecture,
( multiply(sk_c3,sk_c11) = sk_c10
| multiply(sk_c1,sk_c2) = sk_c11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_21) ).
fof(f44,plain,
( sk_c10 = multiply(sk_c3,sk_c11)
| sk_c11 = multiply(sk_c1,sk_c2) ),
inference(reorient_equations,[],[f43]) ).
fof(f45,negated_conjecture,
( inverse(sk_c3) = sk_c11
| multiply(sk_c1,sk_c2) = sk_c11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_22) ).
fof(f46,plain,
( sk_c11 = inverse(sk_c3)
| sk_c11 = multiply(sk_c1,sk_c2) ),
inference(reorient_equations,[],[f45]) ).
fof(f49,negated_conjecture,
( inverse(sk_c4) = sk_c10
| multiply(sk_c1,sk_c2) = sk_c11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_24) ).
fof(f50,plain,
( sk_c10 = inverse(sk_c4)
| sk_c11 = multiply(sk_c1,sk_c2) ),
inference(reorient_equations,[],[f49]) ).
fof(f51,negated_conjecture,
( multiply(sk_c5,sk_c8) = sk_c11
| multiply(sk_c1,sk_c2) = sk_c11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_25) ).
fof(f52,plain,
( sk_c11 = multiply(sk_c5,sk_c8)
| sk_c11 = multiply(sk_c1,sk_c2) ),
inference(reorient_equations,[],[f51]) ).
fof(f53,negated_conjecture,
( inverse(sk_c5) = sk_c8
| multiply(sk_c1,sk_c2) = sk_c11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_26) ).
fof(f54,plain,
( sk_c8 = inverse(sk_c5)
| sk_c11 = multiply(sk_c1,sk_c2) ),
inference(reorient_equations,[],[f53]) ).
fof(f63,negated_conjecture,
( multiply(sk_c3,sk_c11) = sk_c10
| inverse(sk_c1) = sk_c2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_31) ).
fof(f64,plain,
( sk_c10 = multiply(sk_c3,sk_c11)
| sk_c2 = inverse(sk_c1) ),
inference(reorient_equations,[],[f63]) ).
fof(f65,negated_conjecture,
( inverse(sk_c3) = sk_c11
| inverse(sk_c1) = sk_c2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_32) ).
fof(f66,plain,
( sk_c11 = inverse(sk_c3)
| sk_c2 = inverse(sk_c1) ),
inference(reorient_equations,[],[f65]) ).
fof(f69,negated_conjecture,
( inverse(sk_c4) = sk_c10
| inverse(sk_c1) = sk_c2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_34) ).
fof(f70,plain,
( sk_c10 = inverse(sk_c4)
| sk_c2 = inverse(sk_c1) ),
inference(reorient_equations,[],[f69]) ).
fof(f73,negated_conjecture,
( inverse(sk_c5) = sk_c8
| inverse(sk_c1) = sk_c2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_36) ).
fof(f74,plain,
( sk_c8 = inverse(sk_c5)
| sk_c2 = inverse(sk_c1) ),
inference(reorient_equations,[],[f73]) ).
fof(f83,negated_conjecture,
( multiply(sk_c3,sk_c11) = sk_c10
| multiply(sk_c2,sk_c10) = sk_c11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_41) ).
fof(f84,plain,
( sk_c10 = multiply(sk_c3,sk_c11)
| sk_c11 = multiply(sk_c2,sk_c10) ),
inference(reorient_equations,[],[f83]) ).
fof(f85,negated_conjecture,
( inverse(sk_c3) = sk_c11
| multiply(sk_c2,sk_c10) = sk_c11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_42) ).
fof(f86,plain,
( sk_c11 = inverse(sk_c3)
| sk_c11 = multiply(sk_c2,sk_c10) ),
inference(reorient_equations,[],[f85]) ).
fof(f87,negated_conjecture,
( multiply(sk_c4,sk_c10) = sk_c9
| multiply(sk_c2,sk_c10) = sk_c11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_43) ).
fof(f88,plain,
( multiply(sk_c4,sk_c10) = sk_c9
| sk_c11 = multiply(sk_c2,sk_c10) ),
inference(reorient_equations,[],[f87]) ).
fof(f89,negated_conjecture,
( inverse(sk_c4) = sk_c10
| multiply(sk_c2,sk_c10) = sk_c11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_44) ).
fof(f90,plain,
( sk_c10 = inverse(sk_c4)
| sk_c11 = multiply(sk_c2,sk_c10) ),
inference(reorient_equations,[],[f89]) ).
fof(f91,negated_conjecture,
( multiply(sk_c5,sk_c8) = sk_c11
| multiply(sk_c2,sk_c10) = sk_c11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_45) ).
fof(f92,plain,
( sk_c11 = multiply(sk_c5,sk_c8)
| sk_c11 = multiply(sk_c2,sk_c10) ),
inference(reorient_equations,[],[f91]) ).
fof(f93,negated_conjecture,
( inverse(sk_c5) = sk_c8
| multiply(sk_c2,sk_c10) = sk_c11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_46) ).
fof(f94,plain,
( sk_c8 = inverse(sk_c5)
| sk_c11 = multiply(sk_c2,sk_c10) ),
inference(reorient_equations,[],[f93]) ).
fof(f103,negated_conjecture,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( multiply(X6,X5) != X7
| inverse(X7) != X5
| inverse(X6) != X7
| multiply(X5,sk_c10) != sk_c11
| inverse(X4) != X5
| multiply(X4,X5) != sk_c11
| inverse(X3) != sk_c10
| multiply(X3,sk_c10) != sk_c9
| inverse(X2) != sk_c11
| multiply(X2,sk_c11) != sk_c10
| multiply(X1,sk_c10) != sk_c11
| inverse(X0) != X1
| multiply(X0,X1) != sk_c11
| multiply(sk_c11,sk_c9) != sk_c10
| inverse(sk_c11) != sk_c10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_51) ).
fof(f104,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( multiply(X6,X5) != X7
| inverse(X7) != X5
| inverse(X6) != X7
| sk_c11 != multiply(X5,sk_c10)
| inverse(X4) != X5
| sk_c11 != multiply(X4,X5)
| sk_c10 != inverse(X3)
| sk_c9 != multiply(X3,sk_c10)
| sk_c11 != inverse(X2)
| sk_c10 != multiply(X2,sk_c11)
| sk_c11 != multiply(X1,sk_c10)
| inverse(X0) != X1
| multiply(X0,X1) != sk_c11
| sk_c10 != multiply(sk_c11,sk_c9)
| inverse(sk_c11) != sk_c10 ),
inference(reorient_equations,[],[f103]) ).
fof(f105,plain,
! [X2,X3,X0,X6,X7,X4,X5] :
( multiply(X6,X5) != X7
| inverse(X7) != X5
| inverse(X6) != X7
| sk_c11 != multiply(X5,sk_c10)
| inverse(X4) != X5
| sk_c11 != multiply(X4,X5)
| sk_c10 != inverse(X3)
| sk_c9 != multiply(X3,sk_c10)
| sk_c11 != inverse(X2)
| sk_c10 != multiply(X2,sk_c11)
| sk_c11 != multiply(inverse(X0),sk_c10)
| sk_c11 != multiply(X0,inverse(X0))
| sk_c10 != multiply(sk_c11,sk_c9)
| inverse(sk_c11) != sk_c10 ),
inference(equality_resolution,[],[f104]) ).
fof(f106,plain,
! [X2,X3,X0,X6,X7,X4] :
( multiply(X6,inverse(X4)) != X7
| inverse(X4) != inverse(X7)
| inverse(X6) != X7
| sk_c11 != multiply(inverse(X4),sk_c10)
| sk_c11 != multiply(X4,inverse(X4))
| sk_c10 != inverse(X3)
| sk_c9 != multiply(X3,sk_c10)
| sk_c11 != inverse(X2)
| sk_c10 != multiply(X2,sk_c11)
| sk_c11 != multiply(inverse(X0),sk_c10)
| sk_c11 != multiply(X0,inverse(X0))
| sk_c10 != multiply(sk_c11,sk_c9)
| inverse(sk_c11) != sk_c10 ),
inference(equality_resolution,[],[f105]) ).
fof(f107,plain,
! [X2,X3,X0,X6,X4] :
( inverse(X6) != multiply(X6,inverse(X4))
| inverse(X4) != inverse(inverse(X6))
| sk_c11 != multiply(inverse(X4),sk_c10)
| sk_c11 != multiply(X4,inverse(X4))
| sk_c10 != inverse(X3)
| sk_c9 != multiply(X3,sk_c10)
| sk_c11 != inverse(X2)
| sk_c10 != multiply(X2,sk_c11)
| sk_c11 != multiply(inverse(X0),sk_c10)
| sk_c11 != multiply(X0,inverse(X0))
| sk_c10 != multiply(sk_c11,sk_c9)
| inverse(sk_c11) != sk_c10 ),
inference(equality_resolution,[],[f106]) ).
tcf(c_103,plain,
! [X0: $i] : multiply(identity,X0) = X0,
inference(cnf_transformation,[],[f1]) ).
tcf(c_104,plain,
! [X0: $i] : multiply(inverse(X0),X0) = identity,
inference(cnf_transformation,[],[f3]) ).
tcf(c_105,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(multiply(X0,X1),X2) = multiply(X0,multiply(X1,X2)),
inference(cnf_transformation,[],[f4]) ).
tcf(c_106,negated_conjecture,
( ( inverse(sk_c11) = sk_c10 )
| ( multiply(sk_c3,sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f6]) ).
tcf(c_107,negated_conjecture,
( ( inverse(sk_c3) = sk_c11 )
| ( inverse(sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f8]) ).
tcf(c_108,negated_conjecture,
( ( inverse(sk_c11) = sk_c10 )
| ( multiply(sk_c4,sk_c10) = sk_c9 ) ),
inference(cnf_transformation,[],[f9]) ).
tcf(c_109,negated_conjecture,
( ( inverse(sk_c4) = sk_c10 )
| ( inverse(sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f11]) ).
tcf(c_110,negated_conjecture,
( ( inverse(sk_c11) = sk_c10 )
| ( multiply(sk_c5,sk_c8) = sk_c11 ) ),
inference(cnf_transformation,[],[f13]) ).
tcf(c_111,negated_conjecture,
( ( inverse(sk_c5) = sk_c8 )
| ( inverse(sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f15]) ).
tcf(c_112,negated_conjecture,
( ( inverse(sk_c11) = sk_c10 )
| ( multiply(sk_c8,sk_c10) = sk_c11 ) ),
inference(cnf_transformation,[],[f17]) ).
tcf(c_116,negated_conjecture,
( ( multiply(sk_c3,sk_c11) = sk_c10 )
| ( multiply(sk_c11,sk_c9) = sk_c10 ) ),
inference(cnf_transformation,[],[f24]) ).
tcf(c_117,negated_conjecture,
( ( inverse(sk_c3) = sk_c11 )
| ( multiply(sk_c11,sk_c9) = sk_c10 ) ),
inference(cnf_transformation,[],[f26]) ).
tcf(c_118,negated_conjecture,
( ( multiply(sk_c4,sk_c10) = sk_c9 )
| ( multiply(sk_c11,sk_c9) = sk_c10 ) ),
inference(cnf_transformation,[],[f28]) ).
tcf(c_119,negated_conjecture,
( ( inverse(sk_c4) = sk_c10 )
| ( multiply(sk_c11,sk_c9) = sk_c10 ) ),
inference(cnf_transformation,[],[f30]) ).
tcf(c_120,negated_conjecture,
( ( multiply(sk_c5,sk_c8) = sk_c11 )
| ( multiply(sk_c11,sk_c9) = sk_c10 ) ),
inference(cnf_transformation,[],[f32]) ).
tcf(c_121,negated_conjecture,
( ( inverse(sk_c5) = sk_c8 )
| ( multiply(sk_c11,sk_c9) = sk_c10 ) ),
inference(cnf_transformation,[],[f34]) ).
tcf(c_122,negated_conjecture,
( ( multiply(sk_c8,sk_c10) = sk_c11 )
| ( multiply(sk_c11,sk_c9) = sk_c10 ) ),
inference(cnf_transformation,[],[f36]) ).
tcf(c_126,negated_conjecture,
( ( multiply(sk_c1,sk_c2) = sk_c11 )
| ( multiply(sk_c3,sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f44]) ).
tcf(c_127,negated_conjecture,
( ( inverse(sk_c3) = sk_c11 )
| ( multiply(sk_c1,sk_c2) = sk_c11 ) ),
inference(cnf_transformation,[],[f46]) ).
tcf(c_129,negated_conjecture,
( ( inverse(sk_c4) = sk_c10 )
| ( multiply(sk_c1,sk_c2) = sk_c11 ) ),
inference(cnf_transformation,[],[f50]) ).
tcf(c_130,negated_conjecture,
( ( multiply(sk_c1,sk_c2) = sk_c11 )
| ( multiply(sk_c5,sk_c8) = sk_c11 ) ),
inference(cnf_transformation,[],[f52]) ).
tcf(c_131,negated_conjecture,
( ( inverse(sk_c5) = sk_c8 )
| ( multiply(sk_c1,sk_c2) = sk_c11 ) ),
inference(cnf_transformation,[],[f54]) ).
tcf(c_136,negated_conjecture,
( ( inverse(sk_c1) = sk_c2 )
| ( multiply(sk_c3,sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f64]) ).
tcf(c_137,negated_conjecture,
( ( inverse(sk_c1) = sk_c2 )
| ( inverse(sk_c3) = sk_c11 ) ),
inference(cnf_transformation,[],[f66]) ).
tcf(c_139,negated_conjecture,
( ( inverse(sk_c1) = sk_c2 )
| ( inverse(sk_c4) = sk_c10 ) ),
inference(cnf_transformation,[],[f70]) ).
tcf(c_141,negated_conjecture,
( ( inverse(sk_c1) = sk_c2 )
| ( inverse(sk_c5) = sk_c8 ) ),
inference(cnf_transformation,[],[f74]) ).
tcf(c_146,negated_conjecture,
( ( multiply(sk_c2,sk_c10) = sk_c11 )
| ( multiply(sk_c3,sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f84]) ).
tcf(c_147,negated_conjecture,
( ( inverse(sk_c3) = sk_c11 )
| ( multiply(sk_c2,sk_c10) = sk_c11 ) ),
inference(cnf_transformation,[],[f86]) ).
tcf(c_148,negated_conjecture,
( ( multiply(sk_c2,sk_c10) = sk_c11 )
| ( multiply(sk_c4,sk_c10) = sk_c9 ) ),
inference(cnf_transformation,[],[f88]) ).
tcf(c_149,negated_conjecture,
( ( inverse(sk_c4) = sk_c10 )
| ( multiply(sk_c2,sk_c10) = sk_c11 ) ),
inference(cnf_transformation,[],[f90]) ).
tcf(c_150,negated_conjecture,
( ( multiply(sk_c2,sk_c10) = sk_c11 )
| ( multiply(sk_c5,sk_c8) = sk_c11 ) ),
inference(cnf_transformation,[],[f92]) ).
tcf(c_151,negated_conjecture,
( ( inverse(sk_c5) = sk_c8 )
| ( multiply(sk_c2,sk_c10) = sk_c11 ) ),
inference(cnf_transformation,[],[f94]) ).
tcf(c_156,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( ( inverse(sk_c11) != sk_c10 )
| ( inverse(X4) != sk_c10 )
| ( inverse(X3) != sk_c11 )
| ( multiply(sk_c11,sk_c9) != sk_c10 )
| ( multiply(X4,sk_c10) != sk_c9 )
| ( multiply(X3,sk_c11) != sk_c10 )
| ( inverse(inverse(X0)) != inverse(X1) )
| ( multiply(inverse(X2),sk_c10) != sk_c11 )
| ( multiply(inverse(X1),sk_c10) != sk_c11 )
| ( multiply(X2,inverse(X2)) != sk_c11 )
| ( multiply(X1,inverse(X1)) != sk_c11 )
| ( multiply(X0,inverse(X1)) != inverse(X0) ) ),
inference(cnf_transformation,[],[f107]) ).
tcf(c_157,plain,
multiply(identity,sk_c11) = sk_c11,
inference(instantiation,[status(thm)],[c_103]) ).
tcf(c_158,plain,
multiply(inverse(sk_c11),sk_c11) = identity,
inference(instantiation,[status(thm)],[c_104]) ).
tcf(c_617,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_10
| ( inverse(X0) != sk_c11 )
| ( multiply(X0,sk_c11) != sk_c10 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_10])],[c_156]) ).
tcf(c_618,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_11
| ( inverse(X0) != sk_c10 )
| ( multiply(X0,sk_c10) != sk_c9 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_11])],[c_156]) ).
tcf(c_619,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_12
| ( multiply(inverse(X0),sk_c10) != sk_c11 )
| ( multiply(X0,inverse(X0)) != sk_c11 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_12])],[c_156]) ).
tcf(c_620,negated_conjecture,
! [X0: $i,X1: $i] :
( ~ iPr_def_13
| ( inverse(inverse(X0)) != inverse(X1) )
| ( multiply(inverse(X1),sk_c10) != sk_c11 )
| ( multiply(X1,inverse(X1)) != sk_c11 )
| ( multiply(X0,inverse(X1)) != inverse(X0) ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_13])],[c_156]) ).
tcf(c_621,negated_conjecture,
( iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( inverse(sk_c11) != sk_c10 )
| ( multiply(sk_c11,sk_c9) != sk_c10 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_156]) ).
tcf(c_622,definition,
iPr_def_14 = multiply(sk_c11,sk_c9),
introduced(definition,[new_symbols(definition,[iPr_def_14])],[]) ).
tcf(c_623,definition,
iPr_def_15 = inverse(sk_c11),
introduced(definition,[new_symbols(definition,[iPr_def_15])],[]) ).
tcf(c_625,definition,
iPr_def_17 = multiply(sk_c2,sk_c10),
introduced(definition,[new_symbols(definition,[iPr_def_17])],[]) ).
tcf(c_629,definition,
iPr_def_21 = inverse(sk_c5),
introduced(definition,[new_symbols(definition,[iPr_def_21])],[]) ).
tcf(c_630,definition,
iPr_def_22 = multiply(sk_c5,sk_c8),
introduced(definition,[new_symbols(definition,[iPr_def_22])],[]) ).
tcf(c_631,definition,
iPr_def_23 = inverse(sk_c4),
introduced(definition,[new_symbols(definition,[iPr_def_23])],[]) ).
tcf(c_632,definition,
iPr_def_24 = multiply(sk_c4,sk_c10),
introduced(definition,[new_symbols(definition,[iPr_def_24])],[]) ).
tcf(c_633,definition,
iPr_def_25 = inverse(sk_c3),
introduced(definition,[new_symbols(definition,[iPr_def_25])],[]) ).
tcf(c_634,definition,
iPr_def_26 = multiply(sk_c3,sk_c11),
introduced(definition,[new_symbols(definition,[iPr_def_26])],[]) ).
tcf(c_635,definition,
iPr_def_27 = inverse(sk_c1),
introduced(definition,[new_symbols(definition,[iPr_def_27])],[]) ).
tcf(c_636,definition,
iPr_def_28 = multiply(sk_c1,sk_c2),
introduced(definition,[new_symbols(definition,[iPr_def_28])],[]) ).
tcf(c_637,negated_conjecture,
( iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( iPr_def_15 != sk_c10 )
| ( iPr_def_14 != sk_c10 ) ),
inference(demodulation,[status(thm)],[c_621,c_623,c_622]) ).
tcf(c_638,negated_conjecture,
! [X0: $i,X1: $i] :
( ~ iPr_def_13
| ( inverse(inverse(X0)) != inverse(X1) )
| ( multiply(inverse(X1),sk_c10) != sk_c11 )
| ( multiply(X1,inverse(X1)) != sk_c11 )
| ( multiply(X0,inverse(X1)) != inverse(X0) ) ),
inference(demodulation,[status(thm)],[c_620]) ).
tcf(c_639,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_12
| ( multiply(inverse(X0),sk_c10) != sk_c11 )
| ( multiply(X0,inverse(X0)) != sk_c11 ) ),
inference(demodulation,[status(thm)],[c_619]) ).
tcf(c_640,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_11
| ( inverse(X0) != sk_c10 )
| ( multiply(X0,sk_c10) != sk_c9 ) ),
inference(demodulation,[status(thm)],[c_618]) ).
tcf(c_641,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_10
| ( inverse(X0) != sk_c11 )
| ( multiply(X0,sk_c11) != sk_c10 ) ),
inference(demodulation,[status(thm)],[c_617]) ).
tcf(c_646,negated_conjecture,
( ( iPr_def_21 = sk_c8 )
| ( iPr_def_17 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_151,c_629]) ).
tcf(c_647,negated_conjecture,
( ( iPr_def_22 = sk_c11 )
| ( iPr_def_17 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_150,c_630]) ).
tcf(c_648,negated_conjecture,
( ( iPr_def_23 = sk_c10 )
| ( iPr_def_17 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_149,c_631]) ).
tcf(c_649,negated_conjecture,
( ( iPr_def_24 = sk_c9 )
| ( iPr_def_17 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_148,c_632]) ).
tcf(c_650,negated_conjecture,
( ( iPr_def_25 = sk_c11 )
| ( iPr_def_17 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_147,c_633]) ).
tcf(c_651,negated_conjecture,
( ( iPr_def_26 = sk_c10 )
| ( iPr_def_17 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_146,c_634]) ).
tcf(c_656,negated_conjecture,
( ( iPr_def_27 = sk_c2 )
| ( iPr_def_21 = sk_c8 ) ),
inference(demodulation,[status(thm)],[c_141]) ).
tcf(c_658,negated_conjecture,
( ( iPr_def_27 = sk_c2 )
| ( iPr_def_23 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_139]) ).
tcf(c_660,negated_conjecture,
( ( iPr_def_27 = sk_c2 )
| ( iPr_def_25 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_137]) ).
tcf(c_661,negated_conjecture,
( ( iPr_def_27 = sk_c2 )
| ( iPr_def_26 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_136]) ).
tcf(c_666,negated_conjecture,
( ( iPr_def_28 = sk_c11 )
| ( iPr_def_21 = sk_c8 ) ),
inference(demodulation,[status(thm)],[c_131]) ).
tcf(c_667,negated_conjecture,
( ( iPr_def_28 = sk_c11 )
| ( iPr_def_22 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_130]) ).
tcf(c_668,negated_conjecture,
( ( iPr_def_28 = sk_c11 )
| ( iPr_def_23 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_129]) ).
tcf(c_670,negated_conjecture,
( ( iPr_def_28 = sk_c11 )
| ( iPr_def_25 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_127]) ).
tcf(c_671,negated_conjecture,
( ( iPr_def_28 = sk_c11 )
| ( iPr_def_26 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_126]) ).
tcf(c_675,negated_conjecture,
( ( iPr_def_20 = sk_c11 )
| ( iPr_def_14 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_122]) ).
tcf(c_676,negated_conjecture,
( ( iPr_def_21 = sk_c8 )
| ( iPr_def_14 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_121]) ).
tcf(c_677,negated_conjecture,
( ( iPr_def_22 = sk_c11 )
| ( iPr_def_14 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_120]) ).
tcf(c_678,negated_conjecture,
( ( iPr_def_23 = sk_c10 )
| ( iPr_def_14 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_119]) ).
tcf(c_679,negated_conjecture,
( ( iPr_def_24 = sk_c9 )
| ( iPr_def_14 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_118]) ).
tcf(c_680,negated_conjecture,
( ( iPr_def_25 = sk_c11 )
| ( iPr_def_14 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_117]) ).
tcf(c_681,negated_conjecture,
( ( iPr_def_26 = sk_c10 )
| ( iPr_def_14 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_116]) ).
tcf(c_685,negated_conjecture,
( ( iPr_def_20 = sk_c11 )
| ( iPr_def_15 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_112]) ).
tcf(c_686,negated_conjecture,
( ( iPr_def_21 = sk_c8 )
| ( iPr_def_15 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_111]) ).
tcf(c_687,negated_conjecture,
( ( iPr_def_22 = sk_c11 )
| ( iPr_def_15 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_110]) ).
tcf(c_688,negated_conjecture,
( ( iPr_def_23 = sk_c10 )
| ( iPr_def_15 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_109]) ).
tcf(c_689,negated_conjecture,
( ( iPr_def_24 = sk_c9 )
| ( iPr_def_15 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_108]) ).
tcf(c_690,negated_conjecture,
( ( iPr_def_25 = sk_c11 )
| ( iPr_def_15 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_107]) ).
tcf(c_691,negated_conjecture,
( ( iPr_def_26 = sk_c10 )
| ( iPr_def_15 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_106]) ).
tcf(c_692,plain,
! [X0: $i] : X0 = X0,
theory(equality) ).
tcf(c_693,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = X0 )
| ( X2 != X1 )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_694,plain,
! [X0: $i,X1: $i] :
( ( inverse(X0) = inverse(X1) )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_695,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( multiply(X0,X2) = multiply(X1,X3) )
| ( X2 != X3 )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_696,plain,
( ( inverse(sk_c11) = inverse(sk_c11) )
| ( sk_c11 != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_694]) ).
tcf(c_698,plain,
sk_c11 = sk_c11,
inference(instantiation,[status(thm)],[c_692]) ).
tcf(c_1082,plain,
( ( iPr_def_23 = iPr_def_26 )
| ( sk_c11 = iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_648,c_651]) ).
tcf(c_1180,plain,
( ( sk_c2 = iPr_def_27 )
| ( multiply(sk_c5,iPr_def_21) = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_656,c_630]) ).
tcf(c_1182,plain,
( ( sk_c11 = iPr_def_17 )
| ( multiply(sk_c5,iPr_def_21) = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_646,c_630]) ).
tcf(c_1192,plain,
( ( sk_c11 = iPr_def_17 )
| ( multiply(sk_c4,iPr_def_26) = iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_651,c_632]) ).
tcf(c_1193,plain,
( ( sk_c11 = iPr_def_17 )
| ( multiply(sk_c4,iPr_def_23) = iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_648,c_632]) ).
tcf(c_1198,plain,
( ( sk_c11 = iPr_def_17 )
| ( multiply(sk_c3,iPr_def_25) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_650,c_634]) ).
tcf(c_1199,plain,
( ( sk_c11 = iPr_def_17 )
| ( multiply(sk_c3,iPr_def_22) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_647,c_634]) ).
tcf(c_1213,plain,
multiply(iPr_def_15,sk_c11) = identity,
inference(superposition,[status(thm)],[c_623,c_104]) ).
tcf(c_1214,plain,
multiply(iPr_def_25,sk_c3) = identity,
inference(superposition,[status(thm)],[c_633,c_104]) ).
tcf(c_1215,plain,
multiply(iPr_def_23,sk_c4) = identity,
inference(superposition,[status(thm)],[c_631,c_104]) ).
tcf(c_1216,plain,
multiply(iPr_def_21,sk_c5) = identity,
inference(superposition,[status(thm)],[c_629,c_104]) ).
tcf(c_1219,plain,
multiply(iPr_def_27,sk_c1) = identity,
inference(superposition,[status(thm)],[c_635,c_104]) ).
tcf(c_1233,plain,
( ( sk_c10 = iPr_def_23 )
| ( multiply(sk_c1,iPr_def_27) = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_658,c_636]) ).
tcf(c_1250,plain,
( ( sk_c11 = iPr_def_25 )
| ( multiply(sk_c1,iPr_def_27) = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_660,c_636]) ).
tcf(c_1260,plain,
( ( sk_c10 = iPr_def_26 )
| ( multiply(sk_c1,iPr_def_27) = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_661,c_636]) ).
tcf(c_1266,plain,
! [X0: $i] :
( ( iPr_def_14 = sk_c10 )
| ( iPr_def_14 != X0 )
| ( sk_c10 != X0 ) ),
inference(instantiation,[status(thm)],[c_693]) ).
tcf(c_1283,plain,
! [X0: $i,X1: $i] :
( ( sk_c10 = X0 )
| ( sk_c10 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_693]) ).
tcf(c_1284,plain,
! [X0: $i] :
( ( sk_c10 = X0 )
| ( sk_c10 != sk_c10 )
| ( X0 != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_1283]) ).
tcf(c_1285,plain,
sk_c10 = sk_c10,
inference(instantiation,[status(thm)],[c_692]) ).
tcf(c_1286,plain,
( ( sk_c10 = sk_c11 )
| ( sk_c10 != sk_c10 )
| ( sk_c11 != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_1284]) ).
tcf(c_1310,plain,
( ( sk_c10 = multiply(identity,sk_c10) )
| ( sk_c10 != sk_c10 )
| ( multiply(identity,sk_c10) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_1284]) ).
tcf(c_1311,plain,
multiply(identity,sk_c10) = sk_c10,
inference(instantiation,[status(thm)],[c_103]) ).
tcf(c_1313,plain,
! [X0: $i,X1: $i] :
( ( X0 = sk_c10 )
| ( sk_c10 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_693]) ).
tcf(c_1365,plain,
( ( sk_c10 = iPr_def_14 )
| ( iPr_def_14 != sk_c10 )
| ( sk_c10 != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_1284]) ).
tcf(c_1366,plain,
( ( sk_c10 = iPr_def_15 )
| ( iPr_def_15 != sk_c10 )
| ( sk_c10 != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_1284]) ).
tcf(c_1367,plain,
! [X0: $i,X1: $i] :
( ( inverse(X0) = sk_c11 )
| ( sk_c11 != X1 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_693]) ).
tcf(c_1376,plain,
( ( sk_c11 = iPr_def_28 )
| ( multiply(sk_c5,iPr_def_21) = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_666,c_630]) ).
tcf(c_1432,plain,
( ( iPr_def_14 = sk_c10 )
| ( iPr_def_14 != iPr_def_14 )
| ( sk_c10 != iPr_def_14 ) ),
inference(instantiation,[status(thm)],[c_1266]) ).
tcf(c_1433,plain,
! [X0: $i] :
( ( X0 = sk_c10 )
| ( sk_c10 != iPr_def_14 )
| ( X0 != iPr_def_14 ) ),
inference(instantiation,[status(thm)],[c_1313]) ).
tcf(c_1434,plain,
! [X0: $i] :
( ( sk_c10 = X0 )
| ( sk_c10 != iPr_def_14 )
| ( X0 != iPr_def_14 ) ),
inference(instantiation,[status(thm)],[c_1283]) ).
tcf(c_1435,plain,
( ( sk_c10 = sk_c11 )
| ( sk_c10 != iPr_def_14 )
| ( sk_c11 != iPr_def_14 ) ),
inference(instantiation,[status(thm)],[c_1434]) ).
tcf(c_1436,plain,
( ( sk_c11 = sk_c10 )
| ( sk_c10 != iPr_def_14 )
| ( sk_c11 != iPr_def_14 ) ),
inference(instantiation,[status(thm)],[c_1433]) ).
tcf(c_1437,plain,
( ( iPr_def_14 = sk_c10 )
| ( iPr_def_14 != iPr_def_15 )
| ( sk_c10 != iPr_def_15 ) ),
inference(instantiation,[status(thm)],[c_1266]) ).
tcf(c_1438,plain,
! [X0: $i] :
( ( X0 = sk_c10 )
| ( sk_c10 != iPr_def_15 )
| ( X0 != iPr_def_15 ) ),
inference(instantiation,[status(thm)],[c_1313]) ).
tcf(c_1439,plain,
! [X0: $i] :
( ( sk_c10 = X0 )
| ( sk_c10 != iPr_def_15 )
| ( X0 != iPr_def_15 ) ),
inference(instantiation,[status(thm)],[c_1283]) ).
tcf(c_1440,plain,
( ( sk_c10 = sk_c11 )
| ( sk_c10 != iPr_def_15 )
| ( sk_c11 != iPr_def_15 ) ),
inference(instantiation,[status(thm)],[c_1439]) ).
tcf(c_1441,plain,
( ( sk_c11 = sk_c10 )
| ( sk_c10 != iPr_def_15 )
| ( sk_c11 != iPr_def_15 ) ),
inference(instantiation,[status(thm)],[c_1438]) ).
tcf(c_1447,plain,
( ( sk_c11 = iPr_def_28 )
| ( multiply(sk_c4,iPr_def_23) = iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_668,c_632]) ).
tcf(c_1461,plain,
! [X0: $i] : inverse(X0) = inverse(X0),
inference(instantiation,[status(thm)],[c_692]) ).
tcf(c_1464,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( inverse(X0) = X2 )
| ( X2 != X1 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_693]) ).
tcf(c_1521,plain,
( ( iPr_def_23 = iPr_def_26 )
| ( sk_c11 = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_671,c_668]) ).
tcf(c_1565,plain,
! [X0: $i] :
( ( X0 = sk_c10 )
| ( sk_c10 != iPr_def_23 )
| ( X0 != iPr_def_23 ) ),
inference(instantiation,[status(thm)],[c_1313]) ).
tcf(c_1566,plain,
! [X0: $i] :
( ( sk_c10 = X0 )
| ( sk_c10 != iPr_def_23 )
| ( X0 != iPr_def_23 ) ),
inference(instantiation,[status(thm)],[c_1283]) ).
tcf(c_1595,plain,
! [X0: $i] :
( ( X0 = sk_c10 )
| ( sk_c10 != iPr_def_26 )
| ( X0 != iPr_def_26 ) ),
inference(instantiation,[status(thm)],[c_1313]) ).
tcf(c_1596,plain,
! [X0: $i] :
( ( sk_c10 = X0 )
| ( sk_c10 != iPr_def_26 )
| ( X0 != iPr_def_26 ) ),
inference(instantiation,[status(thm)],[c_1283]) ).
tcf(c_1665,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( inverse(X0) = X2 )
| ( X2 != inverse(X1) )
| ( inverse(X0) != inverse(X1) ) ),
inference(instantiation,[status(thm)],[c_1464]) ).
tcf(c_1682,plain,
( ( sk_c10 = iPr_def_14 )
| ( multiply(sk_c5,iPr_def_21) = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_676,c_630]) ).
tcf(c_1700,plain,
! [X0: $i,X1: $i] :
( ( multiply(identity,sk_c10) = X1 )
| ( X1 != X0 )
| ( multiply(identity,sk_c10) != X0 ) ),
inference(instantiation,[status(thm)],[c_693]) ).
tcf(c_1717,plain,
( ( sk_c11 = iPr_def_22 )
| ( multiply(sk_c4,iPr_def_14) = iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_677,c_632]) ).
tcf(c_1746,plain,
multiply(identity,identity) = identity,
inference(instantiation,[status(thm)],[c_103]) ).
tcf(c_1751,plain,
identity = identity,
inference(instantiation,[status(thm)],[c_692]) ).
tcf(c_1766,plain,
( ( sk_c10 = iPr_def_14 )
| ( multiply(sk_c4,iPr_def_23) = iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_678,c_632]) ).
tcf(c_1788,plain,
! [X0: $i] :
( ( iPr_def_14 = iPr_def_23 )
| ( iPr_def_23 != X0 )
| ( iPr_def_14 != X0 ) ),
inference(instantiation,[status(thm)],[c_693]) ).
tcf(c_1789,plain,
( ( iPr_def_14 = iPr_def_23 )
| ( iPr_def_23 != sk_c11 )
| ( iPr_def_14 != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_1788]) ).
tcf(c_1811,plain,
( ( sk_c11 = iPr_def_25 )
| ( multiply(sk_c4,iPr_def_14) = iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_680,c_632]) ).
tcf(c_1841,plain,
( ( iPr_def_23 = sk_c10 )
| ( iPr_def_23 != iPr_def_23 )
| ( sk_c10 != iPr_def_23 ) ),
inference(instantiation,[status(thm)],[c_1565]) ).
tcf(c_1842,plain,
iPr_def_23 = iPr_def_23,
inference(instantiation,[status(thm)],[c_692]) ).
tcf(c_1843,plain,
! [X0: $i,X1: $i] :
( ( X0 = iPr_def_23 )
| ( iPr_def_23 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_693]) ).
tcf(c_1857,plain,
( ( iPr_def_23 = iPr_def_26 )
| ( sk_c10 = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_681,c_678]) ).
tcf(c_1861,plain,
( ( sk_c10 = iPr_def_14 )
| ( multiply(sk_c4,iPr_def_26) = iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_681,c_632]) ).
tcf(c_1896,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = inverse(X0) )
| ( X2 != X1 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_693]) ).
tcf(c_1898,plain,
! [X0: $i] :
( ( inverse(X0) = iPr_def_15 )
| ( iPr_def_15 != inverse(sk_c11) )
| ( inverse(X0) != inverse(sk_c11) ) ),
inference(instantiation,[status(thm)],[c_1665]) ).
tcf(c_1899,plain,
( ( inverse(sk_c11) = iPr_def_15 )
| ( iPr_def_15 != inverse(sk_c11) )
| ( inverse(sk_c11) != inverse(sk_c11) ) ),
inference(instantiation,[status(thm)],[c_1898]) ).
tcf(c_1906,plain,
! [X0: $i] :
( ( inverse(X0) = iPr_def_23 )
| ( iPr_def_23 != inverse(sk_c4) )
| ( inverse(X0) != inverse(sk_c4) ) ),
inference(instantiation,[status(thm)],[c_1665]) ).
tcf(c_1908,plain,
! [X0: $i] :
( ( inverse(X0) = iPr_def_25 )
| ( iPr_def_25 != inverse(sk_c3) )
| ( inverse(X0) != inverse(sk_c3) ) ),
inference(instantiation,[status(thm)],[c_1665]) ).
tcf(c_1909,plain,
( ( inverse(sk_c11) = iPr_def_25 )
| ( iPr_def_25 != inverse(sk_c3) )
| ( inverse(sk_c11) != inverse(sk_c3) ) ),
inference(instantiation,[status(thm)],[c_1908]) ).
tcf(c_1996,plain,
( ( iPr_def_26 = sk_c10 )
| ( iPr_def_26 != iPr_def_26 )
| ( sk_c10 != iPr_def_26 ) ),
inference(instantiation,[status(thm)],[c_1595]) ).
tcf(c_1997,plain,
iPr_def_26 = iPr_def_26,
inference(instantiation,[status(thm)],[c_692]) ).
tcf(c_1998,plain,
! [X0: $i,X1: $i] :
( ( X0 = iPr_def_26 )
| ( iPr_def_26 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_693]) ).
tcf(c_2122,plain,
( ( sk_c10 = iPr_def_15 )
| ( multiply(sk_c5,iPr_def_21) = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_686,c_630]) ).
tcf(c_2160,plain,
( ( iPr_def_14 = iPr_def_15 )
| ( sk_c11 = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_687,c_677]) ).
tcf(c_2164,plain,
( ( sk_c11 = iPr_def_22 )
| ( multiply(sk_c4,iPr_def_15) = iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_687,c_632]) ).
tcf(c_2217,plain,
! [X0: $i,X1: $i] :
( ( X0 = iPr_def_14 )
| ( iPr_def_14 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_693]) ).
tcf(c_2227,plain,
( ( iPr_def_15 = sk_c10 )
| ( iPr_def_15 != iPr_def_15 )
| ( sk_c10 != iPr_def_15 ) ),
inference(instantiation,[status(thm)],[c_1438]) ).
tcf(c_2228,plain,
iPr_def_15 = iPr_def_15,
inference(instantiation,[status(thm)],[c_692]) ).
tcf(c_2229,plain,
! [X0: $i,X1: $i] :
( ( X0 = iPr_def_15 )
| ( iPr_def_15 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_693]) ).
tcf(c_2251,plain,
( ( sk_c10 = iPr_def_15 )
| ( multiply(sk_c4,iPr_def_23) = iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_688,c_632]) ).
tcf(c_2338,plain,
( ( sk_c11 = iPr_def_25 )
| ( multiply(sk_c4,iPr_def_15) = iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_690,c_632]) ).
tcf(c_2380,plain,
! [X0: $i] :
( ( multiply(identity,sk_c10) = X0 )
| ( X0 != sk_c10 )
| ( multiply(identity,sk_c10) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_1700]) ).
tcf(c_2436,plain,
( ( iPr_def_23 = iPr_def_26 )
| ( sk_c10 = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_691,c_688]) ).
tcf(c_2444,plain,
( ( sk_c10 = iPr_def_15 )
| ( multiply(sk_c4,iPr_def_26) = iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_691,c_632]) ).
tcf(c_2502,plain,
! [X0: $i,X1: $i] :
( ( identity = X0 )
| ( identity != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_693]) ).
tcf(c_2648,plain,
( ~ iPr_def_11
| ( sk_c9 != iPr_def_24 )
| ( inverse(sk_c4) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_632,c_640]) ).
tcf(c_2651,plain,
( ~ iPr_def_11
| ( sk_c10 != sk_c9 )
| ( inverse(identity) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_103,c_640]) ).
tcf(c_2652,plain,
( ~ iPr_def_11
| ( sk_c9 != identity )
| ( inverse(inverse(sk_c10)) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_104,c_640]) ).
tcf(c_2676,plain,
( ~ iPr_def_11
| ( sk_c9 != iPr_def_24 )
| ( sk_c10 != iPr_def_23 ) ),
inference(light_normalisation,[status(thm)],[c_2648,c_631]) ).
tcf(c_2873,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = inverse(X0) )
| ( X2 != inverse(X1) )
| ( inverse(X0) != inverse(X1) ) ),
inference(instantiation,[status(thm)],[c_1896]) ).
tcf(c_2891,plain,
! [X0: $i] : multiply(sk_c3,multiply(sk_c11,X0)) = multiply(iPr_def_26,X0),
inference(superposition,[status(thm)],[c_634,c_105]) ).
tcf(c_2900,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(X0,X1)) = multiply(identity,X1),
inference(superposition,[status(thm)],[c_104,c_105]) ).
tcf(c_2902,plain,
! [X0: $i] : multiply(iPr_def_15,multiply(sk_c11,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1213,c_105]) ).
tcf(c_2903,plain,
! [X0: $i] : multiply(iPr_def_25,multiply(sk_c3,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1214,c_105]) ).
tcf(c_2904,plain,
! [X0: $i] : multiply(iPr_def_23,multiply(sk_c4,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1215,c_105]) ).
tcf(c_2905,plain,
! [X0: $i] : multiply(iPr_def_21,multiply(sk_c5,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1216,c_105]) ).
tcf(c_2908,plain,
! [X0: $i] : multiply(iPr_def_27,multiply(sk_c1,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1219,c_105]) ).
tcf(c_2911,plain,
! [X0: $i] : multiply(iPr_def_27,multiply(sk_c1,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_2908,c_103]) ).
tcf(c_2914,plain,
! [X0: $i] : multiply(iPr_def_21,multiply(sk_c5,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_2905,c_103]) ).
tcf(c_2915,plain,
! [X0: $i] : multiply(iPr_def_23,multiply(sk_c4,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_2904,c_103]) ).
tcf(c_2916,plain,
! [X0: $i] : multiply(iPr_def_25,multiply(sk_c3,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_2903,c_103]) ).
tcf(c_2917,plain,
! [X0: $i] : multiply(iPr_def_15,multiply(sk_c11,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_2902,c_103]) ).
tcf(c_2958,plain,
iPr_def_14 = iPr_def_14,
inference(instantiation,[status(thm)],[c_692]) ).
tcf(c_2959,plain,
! [X0: $i,X1: $i] :
( ( iPr_def_14 = X0 )
| ( iPr_def_14 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_693]) ).
tcf(c_3050,plain,
! [X0: $i,X1: $i] :
( ( iPr_def_23 = X0 )
| ( iPr_def_23 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_693]) ).
tcf(c_3057,plain,
! [X0: $i,X1: $i] :
( ( iPr_def_26 = X0 )
| ( iPr_def_26 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_693]) ).
tcf(c_3060,plain,
! [X0: $i] :
( ( X0 = iPr_def_26 )
| ( iPr_def_26 != sk_c10 )
| ( X0 != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_1998]) ).
tcf(c_3083,plain,
! [X0: $i] :
( ( X0 = iPr_def_14 )
| ( iPr_def_14 != multiply(sk_c11,sk_c9) )
| ( X0 != multiply(sk_c11,sk_c9) ) ),
inference(instantiation,[status(thm)],[c_2217]) ).
tcf(c_3144,plain,
! [X0: $i,X1: $i] :
( ( iPr_def_15 = X0 )
| ( iPr_def_15 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_693]) ).
tcf(c_3286,plain,
! [X0: $i,X1: $i] :
( ( X1 = inverse(X0) )
| ( X1 != iPr_def_15 )
| ( inverse(X0) != iPr_def_15 ) ),
inference(instantiation,[status(thm)],[c_1896]) ).
tcf(c_3293,plain,
! [X0: $i] :
( ( inverse(X0) = sk_c10 )
| ( sk_c10 != iPr_def_15 )
| ( inverse(X0) != iPr_def_15 ) ),
inference(instantiation,[status(thm)],[c_1438]) ).
tcf(c_3294,plain,
( ( inverse(sk_c11) = sk_c10 )
| ( sk_c10 != iPr_def_15 )
| ( inverse(sk_c11) != iPr_def_15 ) ),
inference(instantiation,[status(thm)],[c_3293]) ).
tcf(c_3407,plain,
( ~ iPr_def_10
| ( sk_c10 != iPr_def_26 )
| ( inverse(sk_c3) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_634,c_641]) ).
tcf(c_3411,plain,
( ~ iPr_def_10
| ( sk_c10 != identity )
| ( inverse(iPr_def_15) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_1213,c_641]) ).
tcf(c_3430,plain,
( ~ iPr_def_10
| ( sk_c10 != iPr_def_26 )
| ( sk_c11 != iPr_def_25 ) ),
inference(light_normalisation,[status(thm)],[c_3407,c_633]) ).
tcf(c_3504,plain,
( ( inverse(sk_c4) = iPr_def_23 )
| ( iPr_def_23 != inverse(sk_c4) )
| ( inverse(sk_c4) != inverse(sk_c4) ) ),
inference(instantiation,[status(thm)],[c_1906]) ).
tcf(c_3505,plain,
inverse(sk_c4) = inverse(sk_c4),
inference(instantiation,[status(thm)],[c_1461]) ).
tcf(c_3509,plain,
! [X0: $i] :
( ( inverse(X0) = inverse(sk_c3) )
| ( X0 != sk_c3 ) ),
inference(instantiation,[status(thm)],[c_694]) ).
tcf(c_3511,plain,
( ( inverse(sk_c3) = iPr_def_25 )
| ( iPr_def_25 != inverse(sk_c3) )
| ( inverse(sk_c3) != inverse(sk_c3) ) ),
inference(instantiation,[status(thm)],[c_1908]) ).
tcf(c_3512,plain,
inverse(sk_c3) = inverse(sk_c3),
inference(instantiation,[status(thm)],[c_1461]) ).
tcf(c_3516,plain,
! [X0: $i] :
( ( inverse(X0) = inverse(sk_c1) )
| ( X0 != sk_c1 ) ),
inference(instantiation,[status(thm)],[c_694]) ).
tcf(c_3517,plain,
( ( inverse(sk_c11) = inverse(sk_c1) )
| ( sk_c11 != sk_c1 ) ),
inference(instantiation,[status(thm)],[c_3516]) ).
tcf(c_3538,plain,
( ~ iPr_def_12
| ( inverse(identity) != sk_c11 )
| ( multiply(inverse(identity),sk_c10) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_103,c_639]) ).
tcf(c_3633,plain,
! [X0: $i] :
( ~ iPr_def_13
| ( multiply(X0,iPr_def_27) != inverse(X0) )
| ( inverse(inverse(X0)) != inverse(sk_c1) )
| ( multiply(sk_c1,inverse(sk_c1)) != sk_c11 )
| ( multiply(inverse(sk_c1),sk_c10) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_635,c_638]) ).
tcf(c_3639,plain,
! [X0: $i] :
( ~ iPr_def_13
| ( multiply(iPr_def_27,sk_c10) != sk_c11 )
| ( multiply(sk_c1,iPr_def_27) != sk_c11 )
| ( multiply(X0,iPr_def_27) != inverse(X0) )
| ( inverse(inverse(X0)) != iPr_def_27 ) ),
inference(light_normalisation,[status(thm)],[c_3633,c_635]) ).
tcf(c_3848,plain,
( ( iPr_def_23 = iPr_def_26 )
| ( iPr_def_17 = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_1521,c_1082]) ).
tcf(c_3858,plain,
( ( iPr_def_23 = iPr_def_26 )
| ( multiply(iPr_def_28,sk_c9) = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_1521,c_622]) ).
tcf(c_4126,plain,
! [X0: $i] :
( ( identity = X0 )
| ( identity != identity )
| ( X0 != identity ) ),
inference(instantiation,[status(thm)],[c_2502]) ).
tcf(c_4127,plain,
( ( identity = sk_c11 )
| ( identity != identity )
| ( sk_c11 != identity ) ),
inference(instantiation,[status(thm)],[c_4126]) ).
tcf(c_4583,plain,
( ( iPr_def_23 = iPr_def_26 )
| ( iPr_def_26 != sk_c10 )
| ( iPr_def_23 != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_3060]) ).
tcf(c_4626,plain,
( ( iPr_def_14 = iPr_def_15 )
| ( inverse(iPr_def_22) = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_2160,c_623]) ).
tcf(c_4627,plain,
( ( iPr_def_14 = iPr_def_15 )
| ( multiply(iPr_def_22,sk_c9) = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_2160,c_622]) ).
tcf(c_4925,plain,
multiply(iPr_def_27,iPr_def_28) = sk_c2,
inference(superposition,[status(thm)],[c_636,c_2911]) ).
tcf(c_5042,plain,
( ( inverse(sk_c4) = sk_c10 )
| ( sk_c10 != iPr_def_23 )
| ( inverse(sk_c4) != iPr_def_23 ) ),
inference(instantiation,[status(thm)],[c_1565]) ).
tcf(c_5139,plain,
( ( inverse(sk_c3) = sk_c11 )
| ( sk_c11 != iPr_def_25 )
| ( inverse(sk_c3) != iPr_def_25 ) ),
inference(instantiation,[status(thm)],[c_1367]) ).
tcf(c_5248,plain,
multiply(iPr_def_21,iPr_def_22) = sk_c8,
inference(superposition,[status(thm)],[c_630,c_2914]) ).
tcf(c_5253,plain,
multiply(iPr_def_23,iPr_def_24) = sk_c10,
inference(superposition,[status(thm)],[c_632,c_2915]) ).
tcf(c_5488,plain,
multiply(iPr_def_25,iPr_def_26) = sk_c11,
inference(superposition,[status(thm)],[c_634,c_2916]) ).
tcf(c_5504,plain,
multiply(iPr_def_15,iPr_def_14) = sk_c9,
inference(superposition,[status(thm)],[c_622,c_2917]) ).
tcf(c_5521,plain,
! [X0: $i] :
( ( sk_c11 = iPr_def_17 )
| ( multiply(iPr_def_15,multiply(iPr_def_25,X0)) = X0 ) ),
inference(superposition,[status(thm)],[c_650,c_2917]) ).
tcf(c_5942,plain,
( ( multiply(sk_c11,sk_c9) = iPr_def_14 )
| ( iPr_def_14 != multiply(sk_c11,sk_c9) )
| ( multiply(sk_c11,sk_c9) != multiply(sk_c11,sk_c9) ) ),
inference(instantiation,[status(thm)],[c_3083]) ).
tcf(c_5943,plain,
multiply(sk_c11,sk_c9) = multiply(sk_c11,sk_c9),
inference(instantiation,[status(thm)],[c_692]) ).
tcf(c_6130,plain,
! [X0: $i] :
( ( iPr_def_14 = X0 )
| ( iPr_def_14 != iPr_def_14 )
| ( X0 != iPr_def_14 ) ),
inference(instantiation,[status(thm)],[c_2959]) ).
tcf(c_6131,plain,
( ( iPr_def_14 = sk_c11 )
| ( iPr_def_14 != iPr_def_14 )
| ( sk_c11 != iPr_def_14 ) ),
inference(instantiation,[status(thm)],[c_6130]) ).
tcf(c_6190,plain,
! [X0: $i] :
( ( iPr_def_23 = X0 )
| ( iPr_def_23 != sk_c10 )
| ( X0 != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_3050]) ).
tcf(c_6191,plain,
( ( iPr_def_23 = sk_c11 )
| ( iPr_def_23 != sk_c10 )
| ( sk_c11 != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_6190]) ).
tcf(c_6192,plain,
! [X0: $i] :
( ( iPr_def_23 = X0 )
| ( iPr_def_23 != iPr_def_23 )
| ( X0 != iPr_def_23 ) ),
inference(instantiation,[status(thm)],[c_3050]) ).
tcf(c_6277,plain,
! [X0: $i] :
( ( iPr_def_26 = X0 )
| ( iPr_def_26 != iPr_def_26 )
| ( X0 != iPr_def_26 ) ),
inference(instantiation,[status(thm)],[c_3057]) ).
tcf(c_6328,plain,
! [X0: $i] :
( ( iPr_def_15 = X0 )
| ( iPr_def_15 != iPr_def_15 )
| ( X0 != iPr_def_15 ) ),
inference(instantiation,[status(thm)],[c_3144]) ).
tcf(c_7007,plain,
! [X0: $i] :
( ( sk_c11 = iPr_def_17 )
| ( multiply(sk_c5,multiply(iPr_def_21,X0)) = multiply(iPr_def_22,X0) ) ),
inference(superposition,[status(thm)],[c_1182,c_105]) ).
tcf(c_7029,plain,
( ( sk_c11 = iPr_def_17 )
| ( multiply(iPr_def_23,iPr_def_24) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_1192,c_2915]) ).
tcf(c_7030,plain,
( ( sk_c10 = iPr_def_26 )
| ( sk_c11 = iPr_def_17 ) ),
inference(light_normalisation,[status(thm)],[c_7029,c_5253]) ).
tcf(c_7073,plain,
( ( sk_c11 = iPr_def_17 )
| ( multiply(iPr_def_25,iPr_def_26) = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_1199,c_2916]) ).
tcf(c_7074,plain,
( ( sk_c11 = iPr_def_22 )
| ( sk_c11 = iPr_def_17 ) ),
inference(light_normalisation,[status(thm)],[c_7073,c_5488]) ).
tcf(c_7469,plain,
! [X0: $i,X1: $i] :
( ( X0 = sk_c1 )
| ( sk_c1 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_693]) ).
tcf(c_9085,plain,
( ( sk_c11 = iPr_def_22 )
| ( multiply(iPr_def_23,iPr_def_24) = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_1717,c_2915]) ).
tcf(c_9086,plain,
( ( sk_c10 = iPr_def_14 )
| ( sk_c11 = iPr_def_22 ) ),
inference(light_normalisation,[status(thm)],[c_9085,c_5253]) ).
tcf(c_9147,plain,
( ( sk_c10 = iPr_def_14 )
| ( multiply(iPr_def_23,iPr_def_24) = iPr_def_23 ) ),
inference(superposition,[status(thm)],[c_1766,c_2915]) ).
tcf(c_9148,plain,
( ( sk_c10 = iPr_def_23 )
| ( sk_c10 = iPr_def_14 ) ),
inference(light_normalisation,[status(thm)],[c_9147,c_5253]) ).
tcf(c_9276,plain,
! [X0: $i] :
( ( iPr_def_27 = inverse(X0) )
| ( iPr_def_27 != inverse(sk_c1) )
| ( inverse(X0) != inverse(sk_c1) ) ),
inference(instantiation,[status(thm)],[c_2873]) ).
tcf(c_9277,plain,
( ( iPr_def_27 = inverse(sk_c11) )
| ( iPr_def_27 != inverse(sk_c1) )
| ( inverse(sk_c11) != inverse(sk_c1) ) ),
inference(instantiation,[status(thm)],[c_9276]) ).
tcf(c_9461,plain,
( ( sk_c11 = iPr_def_25 )
| ( multiply(iPr_def_23,iPr_def_24) = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_1811,c_2915]) ).
tcf(c_9462,plain,
( ( sk_c10 = iPr_def_14 )
| ( sk_c11 = iPr_def_25 ) ),
inference(light_normalisation,[status(thm)],[c_9461,c_5253]) ).
tcf(c_9524,plain,
( ( sk_c10 = iPr_def_14 )
| ( multiply(iPr_def_23,iPr_def_24) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_1861,c_2915]) ).
tcf(c_9525,plain,
( ( sk_c10 = iPr_def_26 )
| ( sk_c10 = iPr_def_14 ) ),
inference(light_normalisation,[status(thm)],[c_9524,c_5253]) ).
tcf(c_10325,plain,
( ( sk_c11 = iPr_def_22 )
| ( multiply(iPr_def_23,iPr_def_24) = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_2164,c_2915]) ).
tcf(c_10326,plain,
( ( sk_c10 = iPr_def_15 )
| ( sk_c11 = iPr_def_22 ) ),
inference(light_normalisation,[status(thm)],[c_10325,c_5253]) ).
tcf(c_10552,plain,
( ( sk_c11 = iPr_def_25 )
| ( multiply(iPr_def_23,iPr_def_24) = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_2338,c_2915]) ).
tcf(c_10553,plain,
( ( sk_c10 = iPr_def_15 )
| ( sk_c11 = iPr_def_25 ) ),
inference(light_normalisation,[status(thm)],[c_10552,c_5253]) ).
tcf(c_10611,plain,
( ( sk_c10 = iPr_def_15 )
| ( multiply(iPr_def_23,iPr_def_24) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_2444,c_2915]) ).
tcf(c_10612,plain,
( ( sk_c10 = iPr_def_26 )
| ( sk_c10 = iPr_def_15 ) ),
inference(light_normalisation,[status(thm)],[c_10611,c_5253]) ).
tcf(c_12026,plain,
( ( iPr_def_14 = iPr_def_23 )
| ( iPr_def_23 != sk_c10 )
| ( iPr_def_14 != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_1788]) ).
tcf(c_12043,plain,
( ( multiply(identity,sk_c10) = iPr_def_15 )
| ( iPr_def_15 != sk_c10 )
| ( multiply(identity,sk_c10) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_2380]) ).
tcf(c_12050,plain,
! [X0: $i] :
( ( X0 = iPr_def_15 )
| ( iPr_def_15 != sk_c10 )
| ( X0 != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_2229]) ).
tcf(c_13260,plain,
( ( iPr_def_23 = sk_c10 )
| ( iPr_def_23 != iPr_def_26 )
| ( sk_c10 != iPr_def_26 ) ),
inference(instantiation,[status(thm)],[c_1595]) ).
tcf(c_13261,plain,
! [X0: $i] :
( ( iPr_def_23 = X0 )
| ( iPr_def_23 != iPr_def_26 )
| ( X0 != iPr_def_26 ) ),
inference(instantiation,[status(thm)],[c_3050]) ).
tcf(c_13262,plain,
! [X0: $i] :
( ( X0 = iPr_def_23 )
| ( iPr_def_23 != iPr_def_26 )
| ( X0 != iPr_def_26 ) ),
inference(instantiation,[status(thm)],[c_1843]) ).
tcf(c_13392,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(X0,X1)) = X1,
inference(demodulation,[status(thm)],[c_2900,c_103]) ).
tcf(c_13436,plain,
! [X0: $i] : multiply(inverse(identity),X0) = X0,
inference(superposition,[status(thm)],[c_103,c_13392]) ).
tcf(c_13437,plain,
! [X0: $i] : multiply(inverse(inverse(X0)),identity) = X0,
inference(superposition,[status(thm)],[c_104,c_13392]) ).
tcf(c_13438,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(inverse(multiply(X0,X1)),multiply(X0,multiply(X1,X2))) = X2,
inference(superposition,[status(thm)],[c_105,c_13392]) ).
tcf(c_13628,plain,
! [X0: $i] : multiply(inverse(iPr_def_15),X0) = multiply(sk_c11,X0),
inference(superposition,[status(thm)],[c_2917,c_13392]) ).
tcf(c_13629,plain,
! [X0: $i] : multiply(inverse(iPr_def_25),X0) = multiply(sk_c3,X0),
inference(superposition,[status(thm)],[c_2916,c_13392]) ).
tcf(c_13630,plain,
! [X0: $i] : multiply(inverse(iPr_def_23),X0) = multiply(sk_c4,X0),
inference(superposition,[status(thm)],[c_2915,c_13392]) ).
tcf(c_13631,plain,
! [X0: $i] : multiply(inverse(iPr_def_21),X0) = multiply(sk_c5,X0),
inference(superposition,[status(thm)],[c_2914,c_13392]) ).
tcf(c_13634,plain,
! [X0: $i] : multiply(inverse(iPr_def_27),X0) = multiply(sk_c1,X0),
inference(superposition,[status(thm)],[c_2911,c_13392]) ).
tcf(c_13679,plain,
! [X0: $i,X1: $i] : multiply(inverse(inverse(X0)),X1) = multiply(X0,X1),
inference(superposition,[status(thm)],[c_13392,c_13392]) ).
tcf(c_14918,plain,
! [X0: $i] : multiply(X0,identity) = X0,
inference(demodulation,[status(thm)],[c_13437,c_13679]) ).
tcf(c_14947,plain,
inverse(identity) = identity,
inference(superposition,[status(thm)],[c_14918,c_13436]) ).
tcf(c_14966,plain,
( ~ iPr_def_12
| ( multiply(identity,identity) != sk_c11 )
| ( multiply(inverse(identity),sk_c10) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_14947,c_639]) ).
tcf(c_14970,plain,
( ~ iPr_def_12
| ( multiply(identity,identity) != sk_c11 )
| ( multiply(identity,sk_c10) != sk_c11 ) ),
inference(light_normalisation,[status(thm)],[c_14966,c_14947]) ).
tcf(c_14995,plain,
( ( multiply(identity,sk_c10) = inverse(sk_c4) )
| ( inverse(sk_c4) != sk_c10 )
| ( multiply(identity,sk_c10) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_2380]) ).
tcf(c_15568,plain,
( ( sk_c11 = iPr_def_17 )
| ~ iPr_def_11
| ( sk_c9 != iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_648,c_2676]) ).
tcf(c_16203,plain,
( ( sk_c11 = iPr_def_17 )
| ~ iPr_def_10
| ( sk_c10 != iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_650,c_3430]) ).
tcf(c_16396,plain,
( ( sk_c11 = iPr_def_17 )
| ~ iPr_def_10 ),
inference(global_subsumption_just,[status(thm)],[c_16203,c_7030,c_16203]) ).
tcf(c_16705,plain,
multiply(sk_c11,iPr_def_15) = identity,
inference(superposition,[status(thm)],[c_13628,c_104]) ).
tcf(c_16710,plain,
! [X0: $i] : multiply(sk_c11,multiply(iPr_def_15,X0)) = X0,
inference(superposition,[status(thm)],[c_13628,c_13392]) ).
tcf(c_16711,plain,
multiply(sk_c11,identity) = inverse(iPr_def_15),
inference(superposition,[status(thm)],[c_13628,c_14918]) ).
tcf(c_16748,plain,
( ( sk_c11 = iPr_def_25 )
| ( multiply(iPr_def_28,iPr_def_15) = identity ) ),
inference(superposition,[status(thm)],[c_670,c_16705]) ).
tcf(c_16749,plain,
( ( sk_c11 = iPr_def_22 )
| ( multiply(iPr_def_28,iPr_def_15) = identity ) ),
inference(superposition,[status(thm)],[c_667,c_16705]) ).
tcf(c_16756,plain,
multiply(sk_c3,identity) = multiply(iPr_def_26,iPr_def_15),
inference(superposition,[status(thm)],[c_16705,c_2891]) ).
tcf(c_16842,plain,
inverse(iPr_def_15) = sk_c11,
inference(demodulation,[status(thm)],[c_16711,c_14918]) ).
tcf(c_17308,plain,
multiply(iPr_def_26,iPr_def_15) = sk_c3,
inference(demodulation,[status(thm)],[c_16756,c_14918]) ).
tcf(c_17310,plain,
multiply(inverse(iPr_def_26),sk_c3) = iPr_def_15,
inference(superposition,[status(thm)],[c_17308,c_13392]) ).
tcf(c_17318,plain,
! [X0: $i] : multiply(inverse(iPr_def_26),multiply(sk_c3,X0)) = multiply(iPr_def_15,X0),
inference(superposition,[status(thm)],[c_17310,c_105]) ).
tcf(c_17497,plain,
multiply(sk_c3,iPr_def_25) = identity,
inference(superposition,[status(thm)],[c_13629,c_104]) ).
tcf(c_17502,plain,
! [X0: $i] : multiply(sk_c3,multiply(iPr_def_25,X0)) = X0,
inference(superposition,[status(thm)],[c_13629,c_13392]) ).
tcf(c_17528,plain,
( ( identity = iPr_def_26 )
| ( sk_c11 = iPr_def_17 ) ),
inference(demodulation,[status(thm)],[c_1198,c_17497]) ).
tcf(c_17562,plain,
multiply(inverse(iPr_def_26),identity) = multiply(iPr_def_15,iPr_def_25),
inference(superposition,[status(thm)],[c_17497,c_17318]) ).
tcf(c_17632,plain,
! [X0: $i] : multiply(iPr_def_15,multiply(iPr_def_25,X0)) = multiply(inverse(iPr_def_26),X0),
inference(superposition,[status(thm)],[c_17502,c_17318]) ).
tcf(c_17843,plain,
( ( iPr_def_17 = iPr_def_28 )
| ( identity = iPr_def_26 )
| ( sk_c11 = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_17528,c_670]) ).
tcf(c_18289,plain,
multiply(sk_c4,iPr_def_23) = identity,
inference(superposition,[status(thm)],[c_13630,c_104]) ).
tcf(c_18311,plain,
( ( identity = iPr_def_24 )
| ( sk_c10 = iPr_def_15 ) ),
inference(demodulation,[status(thm)],[c_2251,c_18289]) ).
tcf(c_18312,plain,
( ( identity = iPr_def_24 )
| ( sk_c10 = iPr_def_14 ) ),
inference(demodulation,[status(thm)],[c_1766,c_18289]) ).
tcf(c_18313,plain,
( ( identity = iPr_def_24 )
| ( sk_c11 = iPr_def_28 ) ),
inference(demodulation,[status(thm)],[c_1447,c_18289]) ).
tcf(c_18314,plain,
( ( identity = iPr_def_24 )
| ( sk_c11 = iPr_def_17 ) ),
inference(demodulation,[status(thm)],[c_1193,c_18289]) ).
tcf(c_18890,plain,
( ( iPr_def_14 = iPr_def_15 )
| ( identity = iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_18312,c_18311]) ).
tcf(c_18927,plain,
( iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( identity = iPr_def_24 )
| ( sk_c10 != iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_18312,c_637]) ).
tcf(c_19120,plain,
( ( identity = iPr_def_24 )
| ( multiply(iPr_def_28,sk_c9) = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_18313,c_622]) ).
tcf(c_19277,plain,
( ( iPr_def_17 = iPr_def_28 )
| ( identity = iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_18314,c_18313]) ).
tcf(c_19354,plain,
( ( iPr_def_26 = iPr_def_23 )
| ( iPr_def_26 != iPr_def_26 )
| ( iPr_def_23 != iPr_def_26 ) ),
inference(instantiation,[status(thm)],[c_6277]) ).
tcf(c_19538,plain,
! [X0: $i] :
( ( sk_c11 = iPr_def_17 )
| ( multiply(inverse(iPr_def_26),X0) = X0 ) ),
inference(light_normalisation,[status(thm)],[c_5521,c_17632]) ).
tcf(c_19559,plain,
( ( sk_c11 = iPr_def_17 )
| ( inverse(iPr_def_26) = identity ) ),
inference(superposition,[status(thm)],[c_19538,c_14918]) ).
tcf(c_19828,plain,
! [X0: $i] :
( ( iPr_def_17 = iPr_def_28 )
| ( multiply(iPr_def_24,X0) = X0 ) ),
inference(superposition,[status(thm)],[c_19277,c_103]) ).
tcf(c_20904,plain,
( ( iPr_def_17 = iPr_def_28 )
| ( identity = iPr_def_26 )
| ( multiply(sk_c3,iPr_def_25) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_17843,c_634]) ).
tcf(c_20919,plain,
( ( iPr_def_17 = iPr_def_28 )
| ( identity = iPr_def_26 ) ),
inference(light_normalisation,[status(thm)],[c_20904,c_17497]) ).
tcf(c_20936,plain,
! [X0: $i] :
( ( iPr_def_17 = iPr_def_28 )
| ( multiply(iPr_def_26,X0) = X0 ) ),
inference(superposition,[status(thm)],[c_20919,c_103]) ).
tcf(c_21183,plain,
multiply(sk_c5,iPr_def_21) = identity,
inference(superposition,[status(thm)],[c_13631,c_104]) ).
tcf(c_21188,plain,
! [X0: $i] : multiply(sk_c5,multiply(iPr_def_21,X0)) = X0,
inference(superposition,[status(thm)],[c_13631,c_13392]) ).
tcf(c_21207,plain,
( ( identity = iPr_def_22 )
| ( sk_c10 = iPr_def_15 ) ),
inference(demodulation,[status(thm)],[c_2122,c_21183]) ).
tcf(c_21208,plain,
( ( identity = iPr_def_22 )
| ( sk_c10 = iPr_def_14 ) ),
inference(demodulation,[status(thm)],[c_1682,c_21183]) ).
tcf(c_21209,plain,
( ( identity = iPr_def_22 )
| ( sk_c11 = iPr_def_28 ) ),
inference(demodulation,[status(thm)],[c_1376,c_21183]) ).
tcf(c_21210,plain,
( ( identity = iPr_def_22 )
| ( sk_c11 = iPr_def_17 ) ),
inference(demodulation,[status(thm)],[c_1182,c_21183]) ).
tcf(c_21211,plain,
( ( identity = iPr_def_22 )
| ( sk_c2 = iPr_def_27 ) ),
inference(demodulation,[status(thm)],[c_1180,c_21183]) ).
tcf(c_21518,plain,
( iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( identity = iPr_def_22 )
| ( iPr_def_14 != iPr_def_15 )
| ( sk_c10 != iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_21207,c_637]) ).
tcf(c_21774,plain,
( ( iPr_def_14 = iPr_def_15 )
| ( identity = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_21208,c_21207]) ).
tcf(c_21813,plain,
( iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( identity = iPr_def_22 )
| ( sk_c10 != iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_21208,c_637]) ).
tcf(c_21925,plain,
( ( identity = iPr_def_22 )
| ( multiply(iPr_def_28,sk_c9) = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_21209,c_622]) ).
tcf(c_22092,plain,
multiply(sk_c5,sk_c8) = iPr_def_22,
inference(superposition,[status(thm)],[c_5248,c_21188]) ).
tcf(c_22299,plain,
( ( identity = iPr_def_22 )
| ( multiply(sk_c1,iPr_def_27) = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_21211,c_636]) ).
tcf(c_22353,plain,
( ( iPr_def_22 = iPr_def_24 )
| ( iPr_def_14 = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_21774,c_18890]) ).
tcf(c_22355,plain,
( ( iPr_def_14 = iPr_def_15 )
| ( inverse(iPr_def_22) = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_21774,c_14947]) ).
tcf(c_22357,plain,
! [X0: $i] :
( ( iPr_def_14 = iPr_def_15 )
| ( multiply(iPr_def_22,X0) = X0 ) ),
inference(superposition,[status(thm)],[c_21774,c_103]) ).
tcf(c_22423,plain,
( ~ iPr_def_11
| ( sk_c10 != identity )
| ( sk_c10 != sk_c9 ) ),
inference(light_normalisation,[status(thm)],[c_2651,c_14947]) ).
tcf(c_22608,plain,
( ~ iPr_def_10
| ( sk_c10 != identity ) ),
inference(ground_joinability,[status(thm)],[c_3411,c_16842]) ).
tcf(c_22636,plain,
( ( iPr_def_23 = iPr_def_26 )
| ~ iPr_def_10
| ( identity != iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_1857,c_22608]) ).
tcf(c_22639,plain,
( ( sk_c10 = iPr_def_15 )
| ~ iPr_def_10
| ( identity != iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_691,c_22608]) ).
tcf(c_22640,plain,
( ( sk_c11 = iPr_def_25 )
| ~ iPr_def_10
| ( identity != iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_690,c_22608]) ).
tcf(c_22644,plain,
( ( sk_c10 = iPr_def_14 )
| ~ iPr_def_10
| ( identity != iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_681,c_22608]) ).
tcf(c_22645,plain,
( ( sk_c11 = iPr_def_25 )
| ~ iPr_def_10
| ( identity != iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_680,c_22608]) ).
tcf(c_22828,plain,
( ( sk_c10 = iPr_def_15 )
| ~ iPr_def_10 ),
inference(global_subsumption_just,[status(thm)],[c_22639,c_3430,c_10553,c_10612]) ).
tcf(c_23675,plain,
( ( sk_c10 = iPr_def_14 )
| ~ iPr_def_10 ),
inference(global_subsumption_just,[status(thm)],[c_22644,c_3430,c_9462,c_9525]) ).
tcf(c_24318,plain,
( iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( identity = iPr_def_24 ) ),
inference(global_subsumption_just,[status(thm)],[c_18927,c_637,c_1432,c_2227,c_2228,c_2958,c_18312,c_18311]) ).
tcf(c_24405,plain,
( iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( identity = iPr_def_22 ) ),
inference(global_subsumption_just,[status(thm)],[c_21813,c_21207,c_21518,c_21774]) ).
tcf(c_24782,plain,
( ( iPr_def_23 = iPr_def_26 )
| ~ iPr_def_11
| ( sk_c9 != identity )
| ( inverse(inverse(iPr_def_15)) != iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_2436,c_2652]) ).
tcf(c_24846,plain,
( ( iPr_def_23 = iPr_def_26 )
| ~ iPr_def_11
| ( sk_c9 != identity ) ),
inference(ground_joinability,[status(thm)],[c_24782,c_623,c_16842]) ).
tcf(c_26855,plain,
multiply(sk_c1,iPr_def_27) = identity,
inference(superposition,[status(thm)],[c_13634,c_104]) ).
tcf(c_26861,plain,
multiply(sk_c1,identity) = inverse(iPr_def_27),
inference(superposition,[status(thm)],[c_13634,c_14918]) ).
tcf(c_26876,plain,
( ( identity = iPr_def_28 )
| ( identity = iPr_def_22 ) ),
inference(demodulation,[status(thm)],[c_22299,c_26855]) ).
tcf(c_26879,plain,
( ( identity = iPr_def_28 )
| ( sk_c10 = iPr_def_26 ) ),
inference(demodulation,[status(thm)],[c_1260,c_26855]) ).
tcf(c_26880,plain,
( ( identity = iPr_def_28 )
| ( sk_c11 = iPr_def_25 ) ),
inference(demodulation,[status(thm)],[c_1250,c_26855]) ).
tcf(c_26881,plain,
( ( identity = iPr_def_28 )
| ( sk_c10 = iPr_def_23 ) ),
inference(demodulation,[status(thm)],[c_1233,c_26855]) ).
tcf(c_27049,plain,
! [X0: $i] :
( ( identity = iPr_def_22 )
| ( multiply(iPr_def_28,X0) = X0 ) ),
inference(superposition,[status(thm)],[c_26876,c_103]) ).
tcf(c_27196,plain,
inverse(iPr_def_27) = sk_c1,
inference(demodulation,[status(thm)],[c_26861,c_14918]) ).
tcf(c_27405,plain,
( ( iPr_def_23 = iPr_def_26 )
| ( identity = iPr_def_28 )
| ( sk_c10 = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_26879,c_688]) ).
tcf(c_27640,plain,
( ( iPr_def_23 = iPr_def_26 )
| ( identity = iPr_def_28 ) ),
inference(global_subsumption_just,[status(thm)],[c_27405,c_1841,c_1842,c_1996,c_1997,c_4583,c_26881,c_26879]) ).
tcf(c_27666,plain,
! [X0: $i] :
( ( iPr_def_23 = iPr_def_26 )
| ( multiply(iPr_def_28,X0) = X0 ) ),
inference(superposition,[status(thm)],[c_27640,c_103]) ).
tcf(c_27931,plain,
( ( identity = iPr_def_28 )
| ( multiply(sk_c3,iPr_def_25) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_26880,c_634]) ).
tcf(c_27941,plain,
( ( identity = iPr_def_28 )
| ( identity = iPr_def_26 ) ),
inference(light_normalisation,[status(thm)],[c_27931,c_17497]) ).
tcf(c_28180,plain,
( ( identity = iPr_def_28 )
| ( multiply(sk_c4,iPr_def_23) = iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_26881,c_632]) ).
tcf(c_28188,plain,
( ( identity = iPr_def_28 )
| ( identity = iPr_def_24 ) ),
inference(light_normalisation,[status(thm)],[c_28180,c_18289]) ).
tcf(c_28882,plain,
! [X0: $i] :
( ( identity = iPr_def_26 )
| ( multiply(iPr_def_28,X0) = X0 ) ),
inference(superposition,[status(thm)],[c_27941,c_103]) ).
tcf(c_28950,plain,
! [X0: $i] :
( ( identity = iPr_def_24 )
| ( multiply(iPr_def_28,X0) = X0 ) ),
inference(superposition,[status(thm)],[c_28188,c_103]) ).
tcf(c_29228,plain,
( ( iPr_def_14 = iPr_def_15 )
| ( sk_c9 = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_22357,c_4627]) ).
tcf(c_29509,plain,
( ( iPr_def_14 = iPr_def_24 )
| ( iPr_def_14 = iPr_def_15 )
| ( sk_c10 = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_29228,c_689]) ).
tcf(c_29510,plain,
( ( iPr_def_14 = iPr_def_24 )
| ( iPr_def_14 = iPr_def_15 )
| ( sk_c10 = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_29228,c_679]) ).
tcf(c_29574,plain,
multiply(iPr_def_15,iPr_def_25) = inverse(iPr_def_26),
inference(demodulation,[status(thm)],[c_17562,c_14918]) ).
tcf(c_29589,plain,
multiply(sk_c11,inverse(iPr_def_26)) = iPr_def_25,
inference(superposition,[status(thm)],[c_29574,c_16710]) ).
tcf(c_29638,plain,
! [X0: $i] :
( ( X0 = iPr_def_14 )
| ( iPr_def_14 != iPr_def_23 )
| ( X0 != iPr_def_23 ) ),
inference(instantiation,[status(thm)],[c_2217]) ).
tcf(c_29870,plain,
( ( iPr_def_14 = iPr_def_24 )
| ( iPr_def_14 = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_29510,c_29509]) ).
tcf(c_30138,plain,
( ( identity = iPr_def_22 )
| ( sk_c9 = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_27049,c_21925]) ).
tcf(c_30260,plain,
( ( iPr_def_23 = iPr_def_15 )
| ( iPr_def_23 != iPr_def_23 )
| ( iPr_def_15 != iPr_def_23 ) ),
inference(instantiation,[status(thm)],[c_6192]) ).
tcf(c_30293,plain,
! [X0: $i] :
( ( multiply(identity,sk_c10) = X0 )
| ( X0 != iPr_def_15 )
| ( multiply(identity,sk_c10) != iPr_def_15 ) ),
inference(instantiation,[status(thm)],[c_1700]) ).
tcf(c_30296,plain,
( ( multiply(identity,sk_c10) = sk_c11 )
| ( sk_c11 != iPr_def_15 )
| ( multiply(identity,sk_c10) != iPr_def_15 ) ),
inference(instantiation,[status(thm)],[c_30293]) ).
tcf(c_30531,plain,
multiply(iPr_def_26,inverse(iPr_def_26)) = multiply(sk_c3,iPr_def_25),
inference(superposition,[status(thm)],[c_29589,c_2891]) ).
tcf(c_30534,plain,
multiply(iPr_def_26,inverse(iPr_def_26)) = identity,
inference(light_normalisation,[status(thm)],[c_30531,c_17497]) ).
tcf(c_30739,plain,
( ~ iPr_def_12
| ( sk_c11 != identity )
| ( multiply(inverse(iPr_def_26),sk_c10) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_30534,c_639]) ).
tcf(c_30740,plain,
( ( iPr_def_17 = iPr_def_28 )
| ( inverse(iPr_def_26) = identity ) ),
inference(superposition,[status(thm)],[c_30534,c_20936]) ).
tcf(c_30771,plain,
( ( iPr_def_14 = iPr_def_22 )
| ( iPr_def_14 = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_29870,c_22353]) ).
tcf(c_30832,plain,
( ( identity = iPr_def_22 )
| ~ iPr_def_11
| ( sk_c10 != iPr_def_14 )
| ( sk_c10 != identity ) ),
inference(superposition,[status(thm)],[c_30138,c_22423]) ).
tcf(c_30865,plain,
( ( identity = iPr_def_22 )
| ( multiply(sk_c11,iPr_def_14) = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_30138,c_622]) ).
tcf(c_31104,plain,
( ( inverse(sk_c4) = iPr_def_15 )
| ( iPr_def_15 != sk_c10 )
| ( inverse(sk_c4) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_12050]) ).
tcf(c_32051,plain,
( ( iPr_def_23 = iPr_def_26 )
| ( sk_c9 = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_27666,c_3858]) ).
tcf(c_32501,plain,
( ( iPr_def_23 = iPr_def_26 )
| ( multiply(sk_c11,iPr_def_14) = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_32051,c_622]) ).
tcf(c_33441,plain,
( ( identity = iPr_def_26 )
| ( identity = iPr_def_15 )
| ( sk_c11 = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_28882,c_16749]) ).
tcf(c_33442,plain,
( ( identity = iPr_def_26 )
| ( identity = iPr_def_15 )
| ( sk_c11 = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_28882,c_16748]) ).
tcf(c_33654,plain,
( ( sk_c10 = iPr_def_26 )
| ( iPr_def_26 != iPr_def_23 )
| ( sk_c10 != iPr_def_23 ) ),
inference(instantiation,[status(thm)],[c_1566]) ).
tcf(c_33655,plain,
( ( iPr_def_26 = sk_c10 )
| ( iPr_def_26 != iPr_def_23 )
| ( sk_c10 != iPr_def_23 ) ),
inference(instantiation,[status(thm)],[c_1565]) ).
tcf(c_33704,plain,
( ( identity = iPr_def_24 )
| ( sk_c9 = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_28950,c_19120]) ).
tcf(c_34215,plain,
( ( identity = iPr_def_24 )
| ( multiply(sk_c11,iPr_def_14) = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_33704,c_622]) ).
tcf(c_34254,plain,
! [X0: $i] :
( ( sk_c11 = iPr_def_17 )
| ~ iPr_def_13
| ( multiply(X0,identity) != inverse(X0) )
| ( inverse(inverse(X0)) != inverse(iPr_def_26) )
| ( multiply(iPr_def_26,inverse(iPr_def_26)) != sk_c11 )
| ( multiply(inverse(iPr_def_26),sk_c10) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_19559,c_638]) ).
tcf(c_34290,plain,
! [X0: $i] :
( ( sk_c11 = iPr_def_17 )
| ~ iPr_def_13
| ( sk_c11 != identity )
| ( inverse(X0) != X0 )
| ( inverse(inverse(X0)) != inverse(iPr_def_26) )
| ( multiply(inverse(iPr_def_26),sk_c10) != sk_c11 ) ),
inference(light_normalisation,[status(thm)],[c_34254,c_14918,c_30534]) ).
tcf(c_34299,plain,
( ( sk_c11 = iPr_def_17 )
| ~ iPr_def_13
| ( sk_c11 != identity )
| ( inverse(sk_c11) != sk_c11 )
| ( inverse(inverse(sk_c11)) != inverse(iPr_def_26) )
| ( multiply(inverse(iPr_def_26),sk_c10) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_34290]) ).
tcf(c_35166,plain,
( ( iPr_def_15 = iPr_def_22 )
| ( iPr_def_14 = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_22355,c_4626]) ).
tcf(c_36502,plain,
iPr_def_14 = iPr_def_15,
inference(superposition,[status(thm)],[c_35166,c_30771]) ).
tcf(c_36573,plain,
multiply(iPr_def_26,iPr_def_14) = sk_c3,
inference(demodulation,[status(thm)],[c_17308,c_36502]) ).
tcf(c_36580,plain,
! [X0: $i] : multiply(sk_c11,multiply(iPr_def_14,X0)) = X0,
inference(demodulation,[status(thm)],[c_16710,c_36502]) ).
tcf(c_36581,plain,
inverse(iPr_def_14) = sk_c11,
inference(demodulation,[status(thm)],[c_16842,c_36502]) ).
tcf(c_36582,plain,
multiply(sk_c11,iPr_def_14) = identity,
inference(demodulation,[status(thm)],[c_16705,c_36502]) ).
tcf(c_36654,plain,
multiply(iPr_def_14,iPr_def_14) = sk_c9,
inference(demodulation,[status(thm)],[c_5504,c_36502]) ).
tcf(c_36665,plain,
( iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( sk_c10 != iPr_def_14 ) ),
inference(demodulation,[status(thm)],[c_637,c_36502]) ).
tcf(c_36676,plain,
multiply(iPr_def_14,sk_c11) = identity,
inference(demodulation,[status(thm)],[c_1213,c_36502]) ).
tcf(c_36677,plain,
inverse(sk_c11) = iPr_def_14,
inference(demodulation,[status(thm)],[c_623,c_36502]) ).
tcf(c_36741,plain,
( ( iPr_def_23 = iPr_def_26 )
| ( identity = iPr_def_14 ) ),
inference(demodulation,[status(thm)],[c_32501,c_36582]) ).
tcf(c_36744,plain,
( ( identity = iPr_def_22 )
| ( identity = iPr_def_14 ) ),
inference(demodulation,[status(thm)],[c_30865,c_36582]) ).
tcf(c_36908,plain,
( iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( sk_c10 = iPr_def_14 )
| ( iPr_def_14 != iPr_def_23 ) ),
inference(superposition,[status(thm)],[c_678,c_36665]) ).
tcf(c_36975,plain,
( iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( iPr_def_14 != iPr_def_23 ) ),
inference(global_subsumption_just,[status(thm)],[c_36908,c_36665,c_36908]) ).
tcf(c_37034,plain,
( ( identity = iPr_def_24 )
| ( identity = iPr_def_14 ) ),
inference(light_normalisation,[status(thm)],[c_34215,c_36582]) ).
tcf(c_37068,plain,
! [X0: $i] :
( ( identity = iPr_def_14 )
| ( multiply(iPr_def_24,X0) = X0 ) ),
inference(superposition,[status(thm)],[c_37034,c_103]) ).
tcf(c_38001,plain,
( ( iPr_def_23 = iPr_def_26 )
| ( inverse(iPr_def_14) = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_36741,c_14947]) ).
tcf(c_38003,plain,
! [X0: $i] :
( ( iPr_def_23 = iPr_def_26 )
| ( multiply(iPr_def_14,X0) = X0 ) ),
inference(superposition,[status(thm)],[c_36741,c_103]) ).
tcf(c_38006,plain,
( ( iPr_def_23 = iPr_def_26 )
| ( sk_c11 = iPr_def_14 ) ),
inference(light_normalisation,[status(thm)],[c_38001,c_36581]) ).
tcf(c_38196,plain,
( ( iPr_def_23 = iPr_def_26 )
| ( sk_c11 = identity ) ),
inference(superposition,[status(thm)],[c_38003,c_36676]) ).
tcf(c_38759,plain,
( ( iPr_def_23 = iPr_def_26 )
| ( multiply(iPr_def_14,iPr_def_14) = identity ) ),
inference(superposition,[status(thm)],[c_38006,c_36676]) ).
tcf(c_38808,plain,
( ( iPr_def_23 = iPr_def_26 )
| ( sk_c9 = identity ) ),
inference(light_normalisation,[status(thm)],[c_38759,c_36654]) ).
tcf(c_40344,plain,
( ( sk_c11 = iPr_def_17 )
| ( multiply(sk_c11,iPr_def_24) = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_649,c_622]) ).
tcf(c_40948,plain,
( ( iPr_def_23 = iPr_def_26 )
| ( sk_c10 = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_681,c_678]) ).
tcf(c_40979,plain,
multiply(iPr_def_15,sk_c11) = identity,
inference(superposition,[status(thm)],[c_623,c_104]) ).
tcf(c_41139,plain,
( ( iPr_def_14 = iPr_def_15 )
| ( sk_c11 = iPr_def_20 ) ),
inference(superposition,[status(thm)],[c_685,c_675]) ).
tcf(c_41480,negated_conjecture,
( iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( iPr_def_15 != sk_c10 ) ),
inference(global_subsumption_just,[status(thm)],[c_637,c_1285,c_1365,c_1366,c_1437,c_36502,c_36665]) ).
tcf(c_41494,plain,
( iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( sk_c10 = iPr_def_15 )
| ( iPr_def_15 != iPr_def_23 ) ),
inference(superposition,[status(thm)],[c_688,c_41480]) ).
tcf(c_41495,plain,
( iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( sk_c11 = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_687,c_41480]) ).
tcf(c_41580,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(X0,X1)) = multiply(identity,X1),
inference(superposition,[status(thm)],[c_104,c_105]) ).
tcf(c_41741,plain,
( ~ iPr_def_11
| ( sk_c9 != iPr_def_24 )
| ( inverse(sk_c4) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_632,c_640]) ).
tcf(c_41764,plain,
! [X0: $i] :
( ( sk_c11 = iPr_def_17 )
| ~ iPr_def_11
| ( inverse(X0) != sk_c10 )
| ( multiply(X0,iPr_def_23) != sk_c9 ) ),
inference(superposition,[status(thm)],[c_648,c_640]) ).
tcf(c_41774,plain,
( ~ iPr_def_11
| ( sk_c9 != iPr_def_24 )
| ( sk_c10 != iPr_def_23 ) ),
inference(light_normalisation,[status(thm)],[c_41741,c_631]) ).
tcf(c_41979,plain,
! [X0: $i] :
( ~ iPr_def_13
| ( multiply(X0,iPr_def_27) != inverse(X0) )
| ( inverse(inverse(X0)) != inverse(sk_c1) )
| ( multiply(sk_c1,inverse(sk_c1)) != sk_c11 )
| ( multiply(inverse(sk_c1),sk_c10) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_635,c_638]) ).
tcf(c_41985,plain,
! [X0: $i] :
( ~ iPr_def_13
| ( multiply(iPr_def_27,sk_c10) != sk_c11 )
| ( multiply(sk_c1,iPr_def_27) != sk_c11 )
| ( multiply(X0,iPr_def_27) != inverse(X0) )
| ( inverse(inverse(X0)) != iPr_def_27 ) ),
inference(light_normalisation,[status(thm)],[c_41979,c_635]) ).
tcf(c_42809,plain,
( iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( iPr_def_23 = iPr_def_26 )
| ( iPr_def_14 != iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_40948,c_41480]) ).
tcf(c_42969,plain,
iPr_def_14 = iPr_def_15,
inference(global_subsumption_just,[status(thm)],[c_41139,c_36502]) ).
tcf(c_42974,plain,
multiply(iPr_def_14,sk_c11) = identity,
inference(demodulation,[status(thm)],[c_40979,c_42969]) ).
tcf(c_42975,plain,
( iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( sk_c10 != iPr_def_14 ) ),
inference(demodulation,[status(thm)],[c_41480,c_42969]) ).
tcf(c_43090,plain,
! [X0: $i] : multiply(iPr_def_14,multiply(sk_c11,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_42974,c_105]) ).
tcf(c_43091,plain,
( ~ iPr_def_10
| ( sk_c10 != identity )
| ( inverse(iPr_def_14) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_42974,c_641]) ).
tcf(c_43092,plain,
! [X0: $i] : multiply(iPr_def_14,multiply(sk_c11,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_43090,c_103]) ).
tcf(c_43696,plain,
multiply(iPr_def_14,iPr_def_14) = sk_c9,
inference(superposition,[status(thm)],[c_622,c_43092]) ).
tcf(c_44367,plain,
( ( sk_c11 = iPr_def_17 )
| ( multiply(iPr_def_14,iPr_def_14) = iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_40344,c_43092]) ).
tcf(c_44368,plain,
( ( sk_c9 = iPr_def_24 )
| ( sk_c11 = iPr_def_17 ) ),
inference(light_normalisation,[status(thm)],[c_44367,c_43696]) ).
tcf(c_47792,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(X0,X1)) = X1,
inference(demodulation,[status(thm)],[c_41580,c_103]) ).
tcf(c_47823,plain,
! [X0: $i] : multiply(inverse(identity),X0) = X0,
inference(superposition,[status(thm)],[c_103,c_47792]) ).
tcf(c_47824,plain,
! [X0: $i] : multiply(inverse(inverse(X0)),identity) = X0,
inference(superposition,[status(thm)],[c_104,c_47792]) ).
tcf(c_48007,plain,
! [X0: $i,X1: $i] : multiply(inverse(inverse(X0)),X1) = multiply(X0,X1),
inference(superposition,[status(thm)],[c_47792,c_47792]) ).
tcf(c_51102,plain,
! [X0: $i] :
( ( sk_c10 = identity )
| ( identity != X0 )
| ( sk_c10 != X0 ) ),
inference(instantiation,[status(thm)],[c_1283]) ).
tcf(c_51108,plain,
( ( sk_c10 = identity )
| ( identity != sk_c11 )
| ( sk_c10 != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_51102]) ).
tcf(c_51118,plain,
( ( sk_c10 = iPr_def_14 )
| ( iPr_def_14 != multiply(sk_c11,sk_c9) )
| ( sk_c10 != multiply(sk_c11,sk_c9) ) ),
inference(instantiation,[status(thm)],[c_3083]) ).
tcf(c_51139,plain,
! [X0: $i] :
( ( sk_c10 = sk_c3 )
| ( sk_c3 != X0 )
| ( sk_c10 != X0 ) ),
inference(instantiation,[status(thm)],[c_1283]) ).
tcf(c_51141,plain,
( ( inverse(sk_c10) = inverse(sk_c3) )
| ( sk_c10 != sk_c3 ) ),
inference(instantiation,[status(thm)],[c_3509]) ).
tcf(c_51748,plain,
! [X0: $i] :
( ( identity = X0 )
| ( identity != iPr_def_23 )
| ( X0 != iPr_def_23 ) ),
inference(instantiation,[status(thm)],[c_2502]) ).
tcf(c_52788,plain,
( ~ iPr_def_10
| ( sk_c11 != sk_c10 )
| ( inverse(inverse(identity)) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_47823,c_641]) ).
tcf(c_53000,plain,
! [X0: $i] : multiply(X0,identity) = X0,
inference(demodulation,[status(thm)],[c_47824,c_48007]) ).
tcf(c_53029,plain,
inverse(identity) = identity,
inference(superposition,[status(thm)],[c_53000,c_47823]) ).
tcf(c_53115,plain,
( ( sk_c11 = iPr_def_17 )
| ~ iPr_def_11
| ( sk_c9 != iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_648,c_41774]) ).
tcf(c_54651,plain,
( ( iPr_def_14 = iPr_def_23 )
| ( iPr_def_23 != iPr_def_15 )
| ( iPr_def_14 != iPr_def_15 ) ),
inference(instantiation,[status(thm)],[c_1788]) ).
tcf(c_54652,plain,
( ( iPr_def_15 = iPr_def_14 )
| ( iPr_def_15 != iPr_def_15 )
| ( iPr_def_14 != iPr_def_15 ) ),
inference(instantiation,[status(thm)],[c_6328]) ).
tcf(c_54655,plain,
! [X0: $i] :
( ( iPr_def_14 = X0 )
| ( iPr_def_14 != iPr_def_15 )
| ( X0 != iPr_def_15 ) ),
inference(instantiation,[status(thm)],[c_2959]) ).
tcf(c_54656,plain,
! [X0: $i] :
( ( X0 = iPr_def_14 )
| ( iPr_def_14 != iPr_def_15 )
| ( X0 != iPr_def_15 ) ),
inference(instantiation,[status(thm)],[c_2217]) ).
tcf(c_54657,plain,
( ( sk_c11 = iPr_def_14 )
| ( iPr_def_14 != iPr_def_15 )
| ( sk_c11 != iPr_def_15 ) ),
inference(instantiation,[status(thm)],[c_54656]) ).
tcf(c_54659,plain,
! [X0: $i] :
( ( iPr_def_14 = inverse(X0) )
| ( iPr_def_14 != iPr_def_15 )
| ( inverse(X0) != iPr_def_15 ) ),
inference(instantiation,[status(thm)],[c_3286]) ).
tcf(c_54661,plain,
( ( iPr_def_14 = inverse(sk_c11) )
| ( iPr_def_14 != iPr_def_15 )
| ( inverse(sk_c11) != iPr_def_15 ) ),
inference(instantiation,[status(thm)],[c_54659]) ).
tcf(c_54706,plain,
( ( sk_c11 = iPr_def_17 )
| ~ iPr_def_11 ),
inference(global_subsumption_just,[status(thm)],[c_53115,c_15568,c_44368]) ).
tcf(c_54737,plain,
( ( sk_c10 = iPr_def_15 )
| ( iPr_def_15 != iPr_def_14 )
| ( sk_c10 != iPr_def_14 ) ),
inference(instantiation,[status(thm)],[c_1434]) ).
tcf(c_54738,plain,
( ( iPr_def_15 = sk_c10 )
| ( iPr_def_15 != iPr_def_14 )
| ( sk_c10 != iPr_def_14 ) ),
inference(instantiation,[status(thm)],[c_1433]) ).
tcf(c_54739,plain,
! [X0: $i] :
( ( iPr_def_15 = X0 )
| ( iPr_def_15 != iPr_def_14 )
| ( X0 != iPr_def_14 ) ),
inference(instantiation,[status(thm)],[c_3144]) ).
tcf(c_54740,plain,
! [X0: $i] :
( ( X0 = iPr_def_15 )
| ( iPr_def_15 != iPr_def_14 )
| ( X0 != iPr_def_14 ) ),
inference(instantiation,[status(thm)],[c_2229]) ).
tcf(c_58205,plain,
! [X0: $i] :
( ( iPr_def_17 = iPr_def_28 )
| ~ iPr_def_13
| ( multiply(X0,identity) != inverse(X0) )
| ( inverse(inverse(X0)) != inverse(iPr_def_26) )
| ( multiply(iPr_def_26,inverse(iPr_def_26)) != sk_c11 )
| ( multiply(inverse(iPr_def_26),sk_c10) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_30740,c_638]) ).
tcf(c_58251,plain,
! [X0: $i] :
( ( iPr_def_17 = iPr_def_28 )
| ~ iPr_def_13
| ( sk_c11 != identity )
| ( inverse(X0) != X0 )
| ( inverse(inverse(X0)) != inverse(iPr_def_26) )
| ( multiply(inverse(iPr_def_26),sk_c10) != sk_c11 ) ),
inference(light_normalisation,[status(thm)],[c_58205,c_14918,c_30534]) ).
tcf(c_58261,plain,
( ( iPr_def_17 = iPr_def_28 )
| ~ iPr_def_13
| ( sk_c11 != identity )
| ( inverse(sk_c11) != sk_c11 )
| ( inverse(inverse(sk_c11)) != inverse(iPr_def_26) )
| ( multiply(inverse(iPr_def_26),sk_c10) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_58251]) ).
tcf(c_58932,plain,
( ~ iPr_def_12
| ( sk_c11 != identity )
| ( multiply(identity,sk_c10) != sk_c11 ) ),
inference(light_normalisation,[status(thm)],[c_3538,c_14947]) ).
tcf(c_58933,plain,
( ~ iPr_def_12
| ( sk_c11 != identity )
| ( sk_c11 != sk_c10 ) ),
inference(demodulation,[status(thm)],[c_58932,c_103]) ).
tcf(c_58946,plain,
( ( identity = iPr_def_22 )
| ~ iPr_def_12
| ( sk_c11 != iPr_def_14 )
| ( sk_c11 != identity ) ),
inference(superposition,[status(thm)],[c_21208,c_58933]) ).
tcf(c_58957,plain,
( ( iPr_def_23 = iPr_def_26 )
| ~ iPr_def_12
| ( sk_c11 != iPr_def_14 )
| ( sk_c11 != identity ) ),
inference(superposition,[status(thm)],[c_1857,c_58933]) ).
tcf(c_59603,plain,
! [X0: $i] : multiply(inverse(multiply(X0,sk_c2)),multiply(X0,iPr_def_17)) = sk_c10,
inference(superposition,[status(thm)],[c_625,c_13438]) ).
tcf(c_59668,plain,
! [X0: $i] : multiply(inverse(multiply(X0,sk_c4)),multiply(X0,identity)) = iPr_def_23,
inference(superposition,[status(thm)],[c_18289,c_13438]) ).
tcf(c_59674,plain,
! [X0: $i] : multiply(inverse(multiply(X0,sk_c1)),multiply(X0,identity)) = iPr_def_27,
inference(superposition,[status(thm)],[c_26855,c_13438]) ).
tcf(c_59781,plain,
! [X0: $i] : multiply(inverse(multiply(X0,iPr_def_14)),multiply(X0,identity)) = sk_c11,
inference(superposition,[status(thm)],[c_36676,c_13438]) ).
tcf(c_59945,plain,
! [X0: $i] : multiply(inverse(multiply(X0,iPr_def_14)),X0) = sk_c11,
inference(light_normalisation,[status(thm)],[c_59781,c_14918]) ).
tcf(c_59953,plain,
! [X0: $i] : multiply(inverse(multiply(X0,sk_c1)),X0) = iPr_def_27,
inference(light_normalisation,[status(thm)],[c_59674,c_14918]) ).
tcf(c_59955,plain,
! [X0: $i] : multiply(inverse(multiply(X0,sk_c4)),X0) = iPr_def_23,
inference(light_normalisation,[status(thm)],[c_59668,c_14918]) ).
tcf(c_62516,plain,
( ( sk_c10 = sk_c3 )
| ( sk_c3 != iPr_def_26 )
| ( sk_c10 != iPr_def_26 ) ),
inference(instantiation,[status(thm)],[c_51139]) ).
tcf(c_62751,plain,
( iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( iPr_def_15 != iPr_def_23 ) ),
inference(global_subsumption_just,[status(thm)],[c_41494,c_1842,c_30260,c_36502,c_36975,c_54651]) ).
tcf(c_62753,plain,
( iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( iPr_def_14 != iPr_def_23 ) ),
inference(light_normalisation,[status(thm)],[c_62751,c_42969]) ).
tcf(c_63002,plain,
( iPr_def_13
| ( iPr_def_23 = iPr_def_26 ) ),
inference(global_subsumption_just,[status(thm)],[c_42809,c_1857,c_22636,c_24846,c_36741,c_36665,c_38006,c_38196,c_38808,c_58957]) ).
tcf(c_65642,plain,
! [X0: $i,X1: $i] :
( ( inverse(X0) = inverse(sk_c3) )
| ( inverse(sk_c3) != X1 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_1464]) ).
tcf(c_65643,plain,
( ( inverse(sk_c11) = inverse(sk_c3) )
| ( inverse(sk_c3) != sk_c11 )
| ( inverse(sk_c11) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_65642]) ).
tcf(c_66485,plain,
( ( iPr_def_26 = sk_c10 )
| ( iPr_def_26 != iPr_def_14 )
| ( sk_c10 != iPr_def_14 ) ),
inference(instantiation,[status(thm)],[c_1433]) ).
tcf(c_66962,plain,
multiply(inverse(multiply(inverse(iPr_def_17),sk_c2)),identity) = sk_c10,
inference(superposition,[status(thm)],[c_104,c_59603]) ).
tcf(c_68156,plain,
! [X0: $i] :
( ( X0 = sk_c1 )
| ( sk_c1 != iPr_def_14 )
| ( X0 != iPr_def_14 ) ),
inference(instantiation,[status(thm)],[c_7469]) ).
tcf(c_68157,plain,
( ( sk_c11 = sk_c1 )
| ( sk_c1 != iPr_def_14 )
| ( sk_c11 != iPr_def_14 ) ),
inference(instantiation,[status(thm)],[c_68156]) ).
tcf(c_68409,plain,
inverse(multiply(inverse(iPr_def_17),sk_c2)) = sk_c10,
inference(demodulation,[status(thm)],[c_66962,c_14918]) ).
tcf(c_68432,plain,
multiply(sk_c10,multiply(inverse(iPr_def_17),sk_c2)) = identity,
inference(superposition,[status(thm)],[c_68409,c_104]) ).
tcf(c_68501,plain,
( ( iPr_def_23 = identity )
| ( iPr_def_23 != iPr_def_26 )
| ( identity != iPr_def_26 ) ),
inference(instantiation,[status(thm)],[c_13261]) ).
tcf(c_68594,plain,
( ( identity = iPr_def_23 )
| ( iPr_def_23 != iPr_def_26 )
| ( identity != iPr_def_26 ) ),
inference(instantiation,[status(thm)],[c_13262]) ).
tcf(c_68981,plain,
( ( iPr_def_26 = iPr_def_14 )
| ( iPr_def_26 != iPr_def_23 )
| ( iPr_def_14 != iPr_def_23 ) ),
inference(instantiation,[status(thm)],[c_29638]) ).
tcf(c_72407,plain,
( ( sk_c10 = identity )
| ( identity != iPr_def_26 )
| ( sk_c10 != iPr_def_26 ) ),
inference(instantiation,[status(thm)],[c_1596]) ).
tcf(c_74661,plain,
! [X0: $i,X1: $i] :
( ( inverse(X0) = X1 )
| ( X1 != iPr_def_14 )
| ( inverse(X0) != iPr_def_14 ) ),
inference(instantiation,[status(thm)],[c_1464]) ).
tcf(c_74662,plain,
( ( inverse(sk_c11) = sk_c11 )
| ( sk_c11 != iPr_def_14 )
| ( inverse(sk_c11) != iPr_def_14 ) ),
inference(instantiation,[status(thm)],[c_74661]) ).
tcf(c_79775,plain,
! [X0: $i] :
( ( iPr_def_14 = iPr_def_23 )
| ( iPr_def_23 != inverse(X0) )
| ( iPr_def_14 != inverse(X0) ) ),
inference(instantiation,[status(thm)],[c_1788]) ).
tcf(c_79776,plain,
( ( iPr_def_14 = iPr_def_23 )
| ( iPr_def_23 != inverse(sk_c11) )
| ( iPr_def_14 != inverse(sk_c11) ) ),
inference(instantiation,[status(thm)],[c_79775]) ).
tcf(c_84276,plain,
multiply(inverse(sk_c9),iPr_def_14) = sk_c11,
inference(superposition,[status(thm)],[c_36654,c_59945]) ).
tcf(c_84289,plain,
multiply(inverse(sk_c11),inverse(multiply(iPr_def_14,iPr_def_14))) = sk_c11,
inference(superposition,[status(thm)],[c_59945,c_59945]) ).
tcf(c_84303,plain,
multiply(iPr_def_14,inverse(sk_c9)) = sk_c11,
inference(light_normalisation,[status(thm)],[c_84289,c_36654,c_36677]) ).
tcf(c_84474,plain,
multiply(inverse(sk_c10),sk_c10) = identity,
inference(instantiation,[status(thm)],[c_104]) ).
tcf(c_84759,plain,
( ( identity = iPr_def_24 )
| ( multiply(inverse(iPr_def_14),iPr_def_14) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_33704,c_84276]) ).
tcf(c_84763,plain,
( ( identity = iPr_def_22 )
| ( multiply(inverse(iPr_def_14),iPr_def_14) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_30138,c_84276]) ).
tcf(c_84774,plain,
multiply(inverse(inverse(sk_c9)),sk_c11) = iPr_def_14,
inference(superposition,[status(thm)],[c_84276,c_13392]) ).
tcf(c_84787,plain,
( ( identity = iPr_def_22 )
| ( sk_c11 = identity ) ),
inference(light_normalisation,[status(thm)],[c_84763,c_36581,c_36582]) ).
tcf(c_84790,plain,
( ( identity = iPr_def_24 )
| ( sk_c11 = identity ) ),
inference(light_normalisation,[status(thm)],[c_84759,c_36581,c_36582]) ).
tcf(c_84866,plain,
multiply(sk_c11,sk_c11) = inverse(sk_c9),
inference(superposition,[status(thm)],[c_84303,c_36580]) ).
tcf(c_88446,plain,
! [X0: $i,X1: $i] :
( ( inverse(X0) = sk_c10 )
| ( sk_c10 != X1 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_1313]) ).
tcf(c_88452,plain,
( ( inverse(sk_c11) = sk_c10 )
| ( sk_c10 != sk_c11 )
| ( inverse(sk_c11) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_88446]) ).
tcf(c_90174,plain,
multiply(sk_c9,sk_c11) = iPr_def_14,
inference(demodulation,[status(thm)],[c_84774,c_13679]) ).
tcf(c_90189,plain,
( ( sk_c10 = iPr_def_14 )
| ( multiply(iPr_def_24,sk_c11) = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_679,c_90174]) ).
tcf(c_90244,plain,
! [X0: $i] : multiply(sk_c9,multiply(sk_c11,X0)) = multiply(iPr_def_14,X0),
inference(superposition,[status(thm)],[c_90174,c_105]) ).
tcf(c_90246,plain,
( ~ iPr_def_10
| ( sk_c10 != iPr_def_14 )
| ( inverse(sk_c9) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_90174,c_641]) ).
tcf(c_90934,plain,
( ( identity = iPr_def_24 )
| ( identity = iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_84790,c_18314]) ).
tcf(c_91120,plain,
( ( identity = iPr_def_14 )
| ( sk_c10 = iPr_def_14 )
| ( sk_c11 = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_90189,c_37068]) ).
tcf(c_91375,plain,
( ( identity = iPr_def_14 )
| ( iPr_def_14 != iPr_def_23 )
| ( identity != iPr_def_23 ) ),
inference(instantiation,[status(thm)],[c_51748]) ).
tcf(c_91376,plain,
( ( identity = iPr_def_15 )
| ( iPr_def_15 != iPr_def_14 )
| ( identity != iPr_def_14 ) ),
inference(instantiation,[status(thm)],[c_54740]) ).
tcf(c_91377,plain,
( ( iPr_def_15 = identity )
| ( iPr_def_15 != iPr_def_14 )
| ( identity != iPr_def_14 ) ),
inference(instantiation,[status(thm)],[c_54739]) ).
tcf(c_91380,plain,
( ( identity = iPr_def_14 )
| ( iPr_def_14 != iPr_def_15 )
| ( identity != iPr_def_15 ) ),
inference(instantiation,[status(thm)],[c_54656]) ).
tcf(c_91381,plain,
( ( iPr_def_14 = identity )
| ( iPr_def_14 != iPr_def_15 )
| ( identity != iPr_def_15 ) ),
inference(instantiation,[status(thm)],[c_54655]) ).
tcf(c_92345,plain,
( ( iPr_def_14 = iPr_def_23 )
| ( iPr_def_23 != identity )
| ( iPr_def_14 != identity ) ),
inference(instantiation,[status(thm)],[c_1788]) ).
tcf(c_92348,plain,
! [X0: $i] :
( ( X0 = iPr_def_15 )
| ( iPr_def_15 != identity )
| ( X0 != identity ) ),
inference(instantiation,[status(thm)],[c_2229]) ).
tcf(c_92349,plain,
( ( sk_c11 = iPr_def_15 )
| ( iPr_def_15 != identity )
| ( sk_c11 != identity ) ),
inference(instantiation,[status(thm)],[c_92348]) ).
tcf(c_92918,plain,
multiply(sk_c9,inverse(sk_c9)) = multiply(iPr_def_14,sk_c11),
inference(superposition,[status(thm)],[c_84866,c_90244]) ).
tcf(c_92994,plain,
multiply(sk_c9,inverse(sk_c9)) = identity,
inference(light_normalisation,[status(thm)],[c_92918,c_36676]) ).
tcf(c_93569,plain,
( ~ iPr_def_12
| ( sk_c11 != identity )
| ( multiply(inverse(sk_c9),sk_c10) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_92994,c_639]) ).
tcf(c_93850,plain,
! [X0: $i] :
( ( identity = iPr_def_17 )
| ( multiply(iPr_def_24,X0) = X0 ) ),
inference(superposition,[status(thm)],[c_90934,c_103]) ).
tcf(c_99967,plain,
! [X0: $i,X1: $i] :
( ( multiply(inverse(X0),sk_c10) = sk_c11 )
| ( sk_c11 != X1 )
| ( multiply(inverse(X0),sk_c10) != X1 ) ),
inference(instantiation,[status(thm)],[c_693]) ).
tcf(c_99971,plain,
! [X0: $i] : multiply(inverse(X0),sk_c10) = multiply(inverse(X0),sk_c10),
inference(instantiation,[status(thm)],[c_692]) ).
tcf(c_99972,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_693]) ).
tcf(c_99973,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(inverse(X0),sk_c10) = sk_c11 )
| ( sk_c11 != multiply(X1,X2) )
| ( multiply(inverse(X0),sk_c10) != multiply(X1,X2) ) ),
inference(instantiation,[status(thm)],[c_99967]) ).
tcf(c_99974,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_695]) ).
tcf(c_99980,plain,
! [X0: $i,X1: $i] :
( ( sk_c11 = multiply(inverse(X0),sk_c10) )
| ( sk_c11 != X1 )
| ( multiply(inverse(X0),sk_c10) != X1 ) ),
inference(instantiation,[status(thm)],[c_693]) ).
tcf(c_99989,plain,
! [X0: $i] :
( ( multiply(inverse(sk_c10),sk_c10) = X0 )
| ( X0 != identity )
| ( multiply(inverse(sk_c10),sk_c10) != identity ) ),
inference(instantiation,[status(thm)],[c_99972]) ).
tcf(c_99990,plain,
! [X0: $i] :
( ( multiply(inverse(sk_c10),sk_c10) = X0 )
| ( X0 != sk_c11 )
| ( multiply(inverse(sk_c10),sk_c10) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_99972]) ).
tcf(c_99992,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( sk_c11 = multiply(X0,X1) )
| ( sk_c11 != X2 )
| ( multiply(X0,X1) != X2 ) ),
inference(instantiation,[status(thm)],[c_693]) ).
tcf(c_99994,plain,
! [X0: $i,X1: $i] :
( ( multiply(inverse(X0),sk_c10) = multiply(X1,sk_c10) )
| ( sk_c10 != sk_c10 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_99974]) ).
tcf(c_99997,plain,
! [X0: $i,X1: $i] :
( ( sk_c10 = X0 )
| ( sk_c10 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_693]) ).
tcf(c_100001,plain,
! [X0: $i,X1: $i] :
( ( multiply(inverse(sk_c10),sk_c10) = X1 )
| ( X1 != X0 )
| ( multiply(inverse(sk_c10),sk_c10) != X0 ) ),
inference(instantiation,[status(thm)],[c_99972]) ).
tcf(c_100002,plain,
! [X0: $i] :
( ( multiply(inverse(sk_c10),sk_c10) = sk_c11 )
| ( sk_c11 != X0 )
| ( multiply(inverse(sk_c10),sk_c10) != X0 ) ),
inference(instantiation,[status(thm)],[c_99967]) ).
tcf(c_100013,plain,
( ( sk_c11 = multiply(inverse(sk_c10),sk_c10) )
| ( sk_c11 != sk_c11 )
| ( multiply(inverse(sk_c10),sk_c10) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_99980]) ).
tcf(c_100017,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(inverse(X0),sk_c10) = X2 )
| ( X2 != multiply(X1,sk_c10) )
| ( multiply(inverse(X0),sk_c10) != multiply(X1,sk_c10) ) ),
inference(instantiation,[status(thm)],[c_99972]) ).
tcf(c_100024,plain,
! [X0: $i] :
( ( sk_c10 = X0 )
| ( sk_c10 != sk_c10 )
| ( X0 != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_99997]) ).
tcf(c_100030,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_693]) ).
tcf(c_100038,plain,
! [X0: $i] :
( ( sk_c11 = multiply(identity,X0) )
| ( sk_c11 != X0 )
| ( multiply(identity,X0) != X0 ) ),
inference(instantiation,[status(thm)],[c_99992]) ).
tcf(c_100039,plain,
( ( sk_c11 = multiply(identity,sk_c11) )
| ( sk_c11 != sk_c11 )
| ( multiply(identity,sk_c11) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_100038]) ).
tcf(c_100045,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( multiply(X0,X1) = X3 )
| ( X3 != X2 )
| ( multiply(X0,X1) != X2 ) ),
inference(instantiation,[status(thm)],[c_693]) ).
tcf(c_100046,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( sk_c11 = multiply(X0,X1) )
| ( sk_c11 != multiply(X2,X3) )
| ( multiply(X0,X1) != multiply(X2,X3) ) ),
inference(instantiation,[status(thm)],[c_99992]) ).
tcf(c_100064,plain,
! [X0: $i,X1: $i] :
( ( X0 = sk_c10 )
| ( sk_c10 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_693]) ).
tcf(c_100068,plain,
( ( sk_c10 = multiply(inverse(sk_c10),sk_c10) )
| ( sk_c10 != sk_c10 )
| ( multiply(inverse(sk_c10),sk_c10) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_100024]) ).
tcf(c_100070,plain,
( ( multiply(inverse(sk_c10),sk_c10) = sk_c10 )
| ( sk_c10 != identity )
| ( multiply(inverse(sk_c10),sk_c10) != identity ) ),
inference(instantiation,[status(thm)],[c_99989]) ).
tcf(c_100076,plain,
! [X0: $i] :
( ( multiply(inverse(X0),sk_c10) = sk_c11 )
| ( sk_c11 != multiply(inverse(sk_c10),sk_c10) )
| ( multiply(inverse(X0),sk_c10) != multiply(inverse(sk_c10),sk_c10) ) ),
inference(instantiation,[status(thm)],[c_99973]) ).
tcf(c_100097,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = multiply(X0,sk_c10) )
| ( X2 != X1 )
| ( multiply(X0,sk_c10) != X1 ) ),
inference(instantiation,[status(thm)],[c_693]) ).
tcf(c_100100,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(X0,X2) = multiply(X1,sk_c10) )
| ( X2 != sk_c10 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_695]) ).
tcf(c_100112,plain,
! [X0: $i] :
( ( sk_c11 = identity )
| ( identity != X0 )
| ( sk_c11 != X0 ) ),
inference(instantiation,[status(thm)],[c_693]) ).
tcf(c_100122,plain,
! [X0: $i] :
( ( multiply(inverse(sk_c10),sk_c10) = sk_c11 )
| ( sk_c11 != multiply(X0,sk_c10) )
| ( multiply(inverse(sk_c10),sk_c10) != multiply(X0,sk_c10) ) ),
inference(instantiation,[status(thm)],[c_100002]) ).
tcf(c_100123,plain,
! [X0: $i] :
( ( multiply(inverse(sk_c10),sk_c10) = multiply(X0,sk_c10) )
| ( sk_c10 != sk_c10 )
| ( inverse(sk_c10) != X0 ) ),
inference(instantiation,[status(thm)],[c_99994]) ).
tcf(c_100128,plain,
! [X0: $i] :
( ( multiply(inverse(sk_c10),sk_c10) = multiply(inverse(X0),X0) )
| ( multiply(inverse(sk_c10),sk_c10) != identity )
| ( multiply(inverse(X0),X0) != identity ) ),
inference(instantiation,[status(thm)],[c_99989]) ).
tcf(c_100129,plain,
( ( multiply(inverse(sk_c10),sk_c10) = multiply(inverse(sk_c11),sk_c11) )
| ( multiply(inverse(sk_c10),sk_c10) != identity )
| ( multiply(inverse(sk_c11),sk_c11) != identity ) ),
inference(instantiation,[status(thm)],[c_100128]) ).
tcf(c_100131,plain,
! [X0: $i,X1: $i] :
( ( X0 = identity )
| ( identity != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_693]) ).
tcf(c_100141,plain,
! [X0: $i] :
( ( multiply(inverse(sk_c10),sk_c10) = X0 )
| ( X0 != multiply(inverse(sk_c10),sk_c10) )
| ( multiply(inverse(sk_c10),sk_c10) != multiply(inverse(sk_c10),sk_c10) ) ),
inference(instantiation,[status(thm)],[c_100001]) ).
tcf(c_100142,plain,
multiply(inverse(sk_c10),sk_c10) = multiply(inverse(sk_c10),sk_c10),
inference(instantiation,[status(thm)],[c_99971]) ).
tcf(c_100178,plain,
! [X0: $i] :
( ( X0 = multiply(inverse(sk_c10),sk_c10) )
| ( X0 != identity )
| ( multiply(inverse(sk_c10),sk_c10) != identity ) ),
inference(instantiation,[status(thm)],[c_100030]) ).
tcf(c_100180,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = multiply(inverse(X0),sk_c10) )
| ( X2 != multiply(X1,sk_c10) )
| ( multiply(inverse(X0),sk_c10) != multiply(X1,sk_c10) ) ),
inference(instantiation,[status(thm)],[c_100030]) ).
tcf(c_100199,plain,
! [X0: $i,X1: $i] :
( ( multiply(inverse(X0),sk_c10) = multiply(inverse(X1),sk_c10) )
| ( sk_c10 != sk_c10 )
| ( inverse(X0) != inverse(X1) ) ),
inference(instantiation,[status(thm)],[c_99994]) ).
tcf(c_100201,plain,
! [X0: $i,X1: $i] :
( ( multiply(identity,X0) = X1 )
| ( X1 != X0 )
| ( multiply(identity,X0) != X0 ) ),
inference(instantiation,[status(thm)],[c_100045]) ).
tcf(c_100206,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_100045]) ).
tcf(c_100207,plain,
! [X0: $i,X1: $i] : multiply(X0,X1) = multiply(X0,X1),
inference(instantiation,[status(thm)],[c_692]) ).
tcf(c_100211,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_100045]) ).
tcf(c_100218,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( sk_c11 = multiply(X0,X1) )
| ( sk_c11 != multiply(identity,X2) )
| ( multiply(X0,X1) != multiply(identity,X2) ) ),
inference(instantiation,[status(thm)],[c_100046]) ).
tcf(c_100226,plain,
! [X0: $i,X1: $i] :
( ( multiply(inverse(X0),sk_c10) = multiply(X1,iPr_def_23) )
| ( sk_c10 != iPr_def_23 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_99974]) ).
tcf(c_100235,plain,
! [X0: $i,X1: $i] :
( ( identity = X0 )
| ( identity != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_693]) ).
tcf(c_100242,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = inverse(X0) )
| ( X2 != X1 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_693]) ).
tcf(c_100294,plain,
! [X0: $i] :
( ( multiply(inverse(sk_c10),sk_c10) = multiply(inverse(X0),sk_c10) )
| ( sk_c10 != sk_c10 )
| ( inverse(sk_c10) != inverse(X0) ) ),
inference(instantiation,[status(thm)],[c_100123]) ).
tcf(c_100295,plain,
! [X0: $i] :
( ( inverse(sk_c10) = inverse(X0) )
| ( sk_c10 != X0 ) ),
inference(instantiation,[status(thm)],[c_694]) ).
tcf(c_100296,plain,
( ( multiply(inverse(sk_c10),sk_c10) = multiply(inverse(sk_c11),sk_c10) )
| ( sk_c10 != sk_c10 )
| ( inverse(sk_c10) != inverse(sk_c11) ) ),
inference(instantiation,[status(thm)],[c_100294]) ).
tcf(c_100297,plain,
( ( inverse(sk_c10) = inverse(sk_c11) )
| ( sk_c10 != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_100295]) ).
tcf(c_100310,plain,
( ( identity = multiply(inverse(sk_c10),sk_c10) )
| ( identity != identity )
| ( multiply(inverse(sk_c10),sk_c10) != identity ) ),
inference(instantiation,[status(thm)],[c_100178]) ).
tcf(c_100316,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( inverse(X0) = X2 )
| ( X2 != X1 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_693]) ).
tcf(c_100351,plain,
! [X0: $i] :
( ( sk_c10 = X0 )
| ( sk_c10 != multiply(inverse(sk_c10),sk_c10) )
| ( X0 != multiply(inverse(sk_c10),sk_c10) ) ),
inference(instantiation,[status(thm)],[c_99997]) ).
tcf(c_100366,plain,
! [X0: $i] :
( ( X0 = multiply(inverse(sk_c10),sk_c10) )
| ( X0 != sk_c10 )
| ( multiply(inverse(sk_c10),sk_c10) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_100030]) ).
tcf(c_100370,plain,
( ( sk_c11 = multiply(inverse(sk_c10),sk_c10) )
| ( sk_c11 != sk_c10 )
| ( multiply(inverse(sk_c10),sk_c10) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_100366]) ).
tcf(c_100416,plain,
! [X0: $i,X1: $i] :
( ( multiply(inverse(sk_c10),sk_c10) = X1 )
| ( X1 != multiply(inverse(X0),X0) )
| ( multiply(inverse(sk_c10),sk_c10) != multiply(inverse(X0),X0) ) ),
inference(instantiation,[status(thm)],[c_100001]) ).
tcf(c_100458,plain,
! [X0: $i] :
( ( multiply(inverse(X0),sk_c10) = multiply(inverse(sk_c10),sk_c10) )
| ( sk_c10 != sk_c10 )
| ( inverse(X0) != inverse(sk_c10) ) ),
inference(instantiation,[status(thm)],[c_100199]) ).
tcf(c_100479,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(X0,sk_c10) = multiply(X1,X2) )
| ( sk_c10 != X2 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_695]) ).
tcf(c_100500,plain,
! [X0: $i,X1: $i] :
( ( multiply(X0,sk_c10) = multiply(X1,sk_c10) )
| ( sk_c10 != sk_c10 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_100100]) ).
tcf(c_100552,plain,
! [X0: $i] :
( ( sk_c10 = X0 )
| ( sk_c10 != multiply(identity,sk_c10) )
| ( X0 != multiply(identity,sk_c10) ) ),
inference(instantiation,[status(thm)],[c_99997]) ).
tcf(c_100556,plain,
! [X0: $i] :
( ( sk_c10 = multiply(inverse(X0),sk_c10) )
| ( sk_c10 != multiply(identity,sk_c10) )
| ( multiply(inverse(X0),sk_c10) != multiply(identity,sk_c10) ) ),
inference(instantiation,[status(thm)],[c_100180]) ).
tcf(c_100557,plain,
! [X0: $i] :
( ( multiply(inverse(X0),sk_c10) = sk_c10 )
| ( sk_c10 != multiply(identity,sk_c10) )
| ( multiply(inverse(X0),sk_c10) != multiply(identity,sk_c10) ) ),
inference(instantiation,[status(thm)],[c_100017]) ).
tcf(c_100559,plain,
( ( sk_c10 = multiply(inverse(sk_c11),sk_c10) )
| ( sk_c10 != multiply(identity,sk_c10) )
| ( multiply(inverse(sk_c11),sk_c10) != multiply(identity,sk_c10) ) ),
inference(instantiation,[status(thm)],[c_100556]) ).
tcf(c_100571,plain,
! [X0: $i] :
( ( X0 = sk_c10 )
| ( sk_c10 != multiply(inverse(sk_c10),sk_c10) )
| ( X0 != multiply(inverse(sk_c10),sk_c10) ) ),
inference(instantiation,[status(thm)],[c_100064]) ).
tcf(c_100572,plain,
( ( sk_c11 = sk_c10 )
| ( sk_c10 != multiply(inverse(sk_c10),sk_c10) )
| ( sk_c11 != multiply(inverse(sk_c10),sk_c10) ) ),
inference(instantiation,[status(thm)],[c_100571]) ).
tcf(c_100582,plain,
! [X0: $i] : multiply(X0,sk_c10) = multiply(X0,sk_c10),
inference(instantiation,[status(thm)],[c_100207]) ).
tcf(c_100683,plain,
( ( multiply(sk_c2,sk_c10) = iPr_def_17 )
| ( iPr_def_17 != multiply(sk_c2,sk_c10) )
| ( multiply(sk_c2,sk_c10) != multiply(sk_c2,sk_c10) ) ),
inference(instantiation,[status(thm)],[c_100206]) ).
tcf(c_100711,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( ( multiply(X0,X1) = multiply(X4,X5) )
| ( multiply(X4,X5) != multiply(X2,X3) )
| ( multiply(X0,X1) != multiply(X2,X3) ) ),
inference(instantiation,[status(thm)],[c_100211]) ).
tcf(c_100942,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( inverse(X0) = X2 )
| ( X2 != inverse(X1) )
| ( inverse(X0) != inverse(X1) ) ),
inference(instantiation,[status(thm)],[c_100316]) ).
tcf(c_101096,plain,
( ( sk_c11 = identity )
| ( identity != multiply(inverse(sk_c10),sk_c10) )
| ( sk_c11 != multiply(inverse(sk_c10),sk_c10) ) ),
inference(instantiation,[status(thm)],[c_100112]) ).
tcf(c_101098,plain,
! [X0: $i] :
( ( X0 = identity )
| ( identity != multiply(inverse(sk_c10),sk_c10) )
| ( X0 != multiply(inverse(sk_c10),sk_c10) ) ),
inference(instantiation,[status(thm)],[c_100131]) ).
tcf(c_101208,plain,
! [X0: $i] :
( ( inverse(X0) = inverse(sk_c10) )
| ( X0 != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_694]) ).
tcf(c_101383,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(X0,X2) = multiply(inverse(X1),X1) )
| ( X2 != X1 )
| ( X0 != inverse(X1) ) ),
inference(instantiation,[status(thm)],[c_695]) ).
tcf(c_101469,plain,
! [X0: $i,X1: $i] :
( ( multiply(inverse(sk_c10),sk_c10) = multiply(identity,X1) )
| ( multiply(identity,X1) != multiply(inverse(X0),X0) )
| ( multiply(inverse(sk_c10),sk_c10) != multiply(inverse(X0),X0) ) ),
inference(instantiation,[status(thm)],[c_100416]) ).
tcf(c_101471,plain,
( ( multiply(inverse(sk_c10),sk_c10) = multiply(identity,sk_c11) )
| ( multiply(identity,sk_c11) != multiply(inverse(sk_c11),sk_c11) )
| ( multiply(inverse(sk_c10),sk_c10) != multiply(inverse(sk_c11),sk_c11) ) ),
inference(instantiation,[status(thm)],[c_101469]) ).
tcf(c_101765,plain,
! [X0: $i] :
( ( multiply(identity,sk_c10) = multiply(X0,sk_c10) )
| ( identity != X0 )
| ( sk_c10 != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_100500]) ).
tcf(c_101819,plain,
! [X0: $i,X1: $i] :
( ( multiply(X0,sk_c10) = multiply(X1,iPr_def_23) )
| ( sk_c10 != iPr_def_23 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_100479]) ).
tcf(c_102236,plain,
! [X0: $i] :
( ( multiply(sk_c11,sk_c9) = X0 )
| ( X0 != iPr_def_14 )
| ( multiply(sk_c11,sk_c9) != iPr_def_14 ) ),
inference(instantiation,[status(thm)],[c_100045]) ).
tcf(c_102281,plain,
multiply(sk_c2,sk_c10) = multiply(sk_c2,sk_c10),
inference(instantiation,[status(thm)],[c_100582]) ).
tcf(c_102289,plain,
! [X0: $i] :
( ( multiply(sk_c5,sk_c8) = X0 )
| ( X0 != iPr_def_22 )
| ( multiply(sk_c5,sk_c8) != iPr_def_22 ) ),
inference(instantiation,[status(thm)],[c_100045]) ).
tcf(c_102290,plain,
( ( sk_c11 = multiply(sk_c5,sk_c8) )
| ( sk_c11 != iPr_def_22 )
| ( multiply(sk_c5,sk_c8) != iPr_def_22 ) ),
inference(instantiation,[status(thm)],[c_99992]) ).
tcf(c_102961,plain,
! [X0: $i] :
( ( multiply(sk_c2,sk_c10) = X0 )
| ( X0 != iPr_def_17 )
| ( multiply(sk_c2,sk_c10) != iPr_def_17 ) ),
inference(instantiation,[status(thm)],[c_100045]) ).
tcf(c_102962,plain,
( ( sk_c11 = multiply(sk_c2,sk_c10) )
| ( sk_c11 != iPr_def_17 )
| ( multiply(sk_c2,sk_c10) != iPr_def_17 ) ),
inference(instantiation,[status(thm)],[c_99992]) ).
tcf(c_102991,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( ( multiply(inverse(X0),sk_c10) = multiply(X3,X4) )
| ( multiply(X3,X4) != multiply(X1,X2) )
| ( multiply(inverse(X0),sk_c10) != multiply(X1,X2) ) ),
inference(instantiation,[status(thm)],[c_100711]) ).
tcf(c_103329,plain,
! [X0: $i] :
( ( inverse(X0) = iPr_def_15 )
| ( iPr_def_15 != inverse(sk_c11) )
| ( inverse(X0) != inverse(sk_c11) ) ),
inference(instantiation,[status(thm)],[c_100942]) ).
tcf(c_103334,plain,
! [X0: $i] :
( ( inverse(X0) = iPr_def_25 )
| ( iPr_def_25 != inverse(sk_c3) )
| ( inverse(X0) != inverse(sk_c3) ) ),
inference(instantiation,[status(thm)],[c_100942]) ).
tcf(c_103573,plain,
! [X0: $i,X1: $i] :
( ( multiply(inverse(sk_c11),sk_c10) = multiply(X0,X1) )
| ( multiply(X0,X1) != multiply(iPr_def_15,iPr_def_23) )
| ( multiply(inverse(sk_c11),sk_c10) != multiply(iPr_def_15,iPr_def_23) ) ),
inference(instantiation,[status(thm)],[c_102991]) ).
tcf(c_104985,plain,
! [X0: $i] :
( ( multiply(inverse(X0),sk_c10) = sk_c11 )
| ( sk_c11 != multiply(sk_c5,sk_c8) )
| ( multiply(inverse(X0),sk_c10) != multiply(sk_c5,sk_c8) ) ),
inference(instantiation,[status(thm)],[c_99973]) ).
tcf(c_105017,plain,
( ( multiply(inverse(sk_c10),sk_c10) = sk_c11 )
| ( sk_c11 != multiply(sk_c2,sk_c10) )
| ( multiply(inverse(sk_c10),sk_c10) != multiply(sk_c2,sk_c10) ) ),
inference(instantiation,[status(thm)],[c_100122]) ).
tcf(c_105068,plain,
! [X0: $i] :
( ( multiply(identity,identity) = X0 )
| ( X0 != identity )
| ( multiply(identity,identity) != identity ) ),
inference(instantiation,[status(thm)],[c_100201]) ).
tcf(c_105069,plain,
( ( multiply(identity,identity) = sk_c11 )
| ( sk_c11 != identity )
| ( multiply(identity,identity) != identity ) ),
inference(instantiation,[status(thm)],[c_105068]) ).
tcf(c_106017,plain,
( ( inverse(iPr_def_26) = inverse(sk_c10) )
| ( iPr_def_26 != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_101208]) ).
tcf(c_106076,plain,
! [X0: $i] :
( ( multiply(identity,sk_c10) = multiply(X0,iPr_def_23) )
| ( identity != X0 )
| ( sk_c10 != iPr_def_23 ) ),
inference(instantiation,[status(thm)],[c_101819]) ).
tcf(c_106124,plain,
( ( multiply(identity,sk_c10) = multiply(inverse(sk_c10),sk_c10) )
| ( identity != inverse(sk_c10) )
| ( sk_c10 != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_101765]) ).
tcf(c_106127,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_100141]) ).
tcf(c_106208,plain,
( ( sk_c10 = identity )
| ( identity != multiply(inverse(sk_c10),sk_c10) )
| ( sk_c10 != multiply(inverse(sk_c10),sk_c10) ) ),
inference(instantiation,[status(thm)],[c_101098]) ).
tcf(c_106631,plain,
( ( multiply(sk_c11,sk_c9) = identity )
| ( identity != iPr_def_14 )
| ( multiply(sk_c11,sk_c9) != iPr_def_14 ) ),
inference(instantiation,[status(thm)],[c_102236]) ).
tcf(c_106639,plain,
( ( multiply(sk_c11,sk_c9) = multiply(inverse(sk_c10),sk_c10) )
| ( multiply(sk_c11,sk_c9) != identity )
| ( multiply(inverse(sk_c10),sk_c10) != identity ) ),
inference(instantiation,[status(thm)],[c_100178]) ).
tcf(c_106970,plain,
! [X0: $i] :
( ( inverse(X0) = multiply(inverse(sk_c10),sk_c10) )
| ( inverse(X0) != sk_c10 )
| ( multiply(inverse(sk_c10),sk_c10) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_100366]) ).
tcf(c_106972,plain,
! [X0: $i] :
( ( inverse(inverse(X0)) = inverse(sk_c10) )
| ( inverse(X0) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_101208]) ).
tcf(c_106976,plain,
( ( inverse(inverse(sk_c11)) = inverse(sk_c10) )
| ( inverse(sk_c11) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_106972]) ).
tcf(c_106978,plain,
( ( inverse(sk_c11) = multiply(inverse(sk_c10),sk_c10) )
| ( inverse(sk_c11) != sk_c10 )
| ( multiply(inverse(sk_c10),sk_c10) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_106970]) ).
tcf(c_107145,plain,
! [X0: $i,X1: $i] :
( ( identity = inverse(X0) )
| ( identity != X1 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_100242]) ).
tcf(c_107147,plain,
! [X0: $i,X1: $i] :
( ( identity = X0 )
| ( identity != inverse(X1) )
| ( X0 != inverse(X1) ) ),
inference(instantiation,[status(thm)],[c_100235]) ).
tcf(c_107156,plain,
! [X0: $i,X1: $i] :
( ( iPr_def_23 = inverse(X0) )
| ( iPr_def_23 != X1 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_100242]) ).
tcf(c_107181,plain,
! [X0: $i,X1: $i] :
( ( inverse(sk_c10) = inverse(X0) )
| ( inverse(sk_c10) != X1 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_100242]) ).
tcf(c_107961,plain,
( ( multiply(sk_c5,sk_c8) = identity )
| ( identity != iPr_def_22 )
| ( multiply(sk_c5,sk_c8) != iPr_def_22 ) ),
inference(instantiation,[status(thm)],[c_102289]) ).
tcf(c_107970,plain,
( ( multiply(inverse(sk_c10),sk_c10) = multiply(sk_c5,sk_c8) )
| ( multiply(sk_c5,sk_c8) != identity )
| ( multiply(inverse(sk_c10),sk_c10) != identity ) ),
inference(instantiation,[status(thm)],[c_99989]) ).
tcf(c_108269,plain,
! [X0: $i,X1: $i] :
( ( multiply(identity,X0) = multiply(inverse(X1),X1) )
| ( identity != inverse(X1) )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_101383]) ).
tcf(c_108270,plain,
( ( multiply(identity,sk_c11) = multiply(inverse(sk_c11),sk_c11) )
| ( identity != inverse(sk_c11) )
| ( sk_c11 != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_108269]) ).
tcf(c_108372,plain,
( ( multiply(sk_c2,sk_c10) = identity )
| ( identity != iPr_def_17 )
| ( multiply(sk_c2,sk_c10) != iPr_def_17 ) ),
inference(instantiation,[status(thm)],[c_102961]) ).
tcf(c_108381,plain,
( ( multiply(inverse(sk_c10),sk_c10) = multiply(sk_c2,sk_c10) )
| ( multiply(sk_c2,sk_c10) != identity )
| ( multiply(inverse(sk_c10),sk_c10) != identity ) ),
inference(instantiation,[status(thm)],[c_99989]) ).
tcf(c_109729,plain,
( ( multiply(inverse(iPr_def_26),sk_c10) = multiply(inverse(sk_c10),sk_c10) )
| ( sk_c10 != sk_c10 )
| ( inverse(iPr_def_26) != inverse(sk_c10) ) ),
inference(instantiation,[status(thm)],[c_100458]) ).
tcf(c_110495,plain,
! [X0: $i,X1: $i] :
( ( X1 = inverse(X0) )
| ( X1 != iPr_def_15 )
| ( inverse(X0) != iPr_def_15 ) ),
inference(instantiation,[status(thm)],[c_100242]) ).
tcf(c_110497,plain,
( ( inverse(sk_c10) = iPr_def_15 )
| ( iPr_def_15 != inverse(sk_c11) )
| ( inverse(sk_c10) != inverse(sk_c11) ) ),
inference(instantiation,[status(thm)],[c_103329]) ).
tcf(c_112998,plain,
( ( multiply(inverse(sk_c11),sk_c10) = multiply(identity,sk_c10) )
| ( multiply(identity,sk_c10) != multiply(iPr_def_15,iPr_def_23) )
| ( multiply(inverse(sk_c11),sk_c10) != multiply(iPr_def_15,iPr_def_23) ) ),
inference(instantiation,[status(thm)],[c_103573]) ).
tcf(c_112999,plain,
( ( multiply(identity,sk_c10) = multiply(iPr_def_15,iPr_def_23) )
| ( identity != iPr_def_15 )
| ( sk_c10 != iPr_def_23 ) ),
inference(instantiation,[status(thm)],[c_106076]) ).
tcf(c_113011,plain,
! [X0: $i] :
( ( multiply(inverse(X0),sk_c10) = multiply(iPr_def_15,iPr_def_23) )
| ( sk_c10 != iPr_def_23 )
| ( inverse(X0) != iPr_def_15 ) ),
inference(instantiation,[status(thm)],[c_100226]) ).
tcf(c_113012,plain,
( ( multiply(inverse(sk_c11),sk_c10) = multiply(iPr_def_15,iPr_def_23) )
| ( sk_c10 != iPr_def_23 )
| ( inverse(sk_c11) != iPr_def_15 ) ),
inference(instantiation,[status(thm)],[c_113011]) ).
tcf(c_113181,plain,
( ( multiply(inverse(sk_c10),sk_c10) = sk_c10 )
| ( sk_c10 != multiply(identity,sk_c10) )
| ( multiply(inverse(sk_c10),sk_c10) != multiply(identity,sk_c10) ) ),
inference(instantiation,[status(thm)],[c_100557]) ).
tcf(c_113518,plain,
! [X0: $i] :
( ( sk_c11 = multiply(inverse(sk_c10),sk_c10) )
| ( sk_c11 != multiply(identity,X0) )
| ( multiply(inverse(sk_c10),sk_c10) != multiply(identity,X0) ) ),
inference(instantiation,[status(thm)],[c_100218]) ).
tcf(c_113520,plain,
( ( sk_c11 = multiply(inverse(sk_c10),sk_c10) )
| ( sk_c11 != multiply(identity,sk_c11) )
| ( multiply(inverse(sk_c10),sk_c10) != multiply(identity,sk_c11) ) ),
inference(instantiation,[status(thm)],[c_113518]) ).
tcf(c_113579,plain,
( ( multiply(inverse(sk_c10),sk_c10) = sk_c11 )
| ( sk_c11 != multiply(sk_c5,sk_c8) )
| ( multiply(inverse(sk_c10),sk_c10) != multiply(sk_c5,sk_c8) ) ),
inference(instantiation,[status(thm)],[c_104985]) ).
tcf(c_113962,plain,
! [X0: $i] :
( ( identity = inverse(X0) )
| ( identity != multiply(inverse(sk_c10),sk_c10) )
| ( inverse(X0) != multiply(inverse(sk_c10),sk_c10) ) ),
inference(instantiation,[status(thm)],[c_107145]) ).
tcf(c_113963,plain,
( ( identity = inverse(sk_c11) )
| ( identity != multiply(inverse(sk_c10),sk_c10) )
| ( inverse(sk_c11) != multiply(inverse(sk_c10),sk_c10) ) ),
inference(instantiation,[status(thm)],[c_113962]) ).
tcf(c_116634,plain,
( ( sk_c10 = multiply(sk_c11,sk_c9) )
| ( sk_c10 != multiply(inverse(sk_c10),sk_c10) )
| ( multiply(sk_c11,sk_c9) != multiply(inverse(sk_c10),sk_c10) ) ),
inference(instantiation,[status(thm)],[c_100351]) ).
tcf(c_118165,plain,
! [X0: $i] :
( ( X0 = multiply(inverse(sk_c10),sk_c10) )
| ( X0 != sk_c11 )
| ( multiply(inverse(sk_c10),sk_c10) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_100097]) ).
tcf(c_118530,plain,
! [X0: $i] :
( ( multiply(inverse(sk_c10),sk_c10) = inverse(X0) )
| ( inverse(X0) != sk_c11 )
| ( multiply(inverse(sk_c10),sk_c10) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_99990]) ).
tcf(c_118532,plain,
( ( multiply(inverse(sk_c10),sk_c10) = inverse(sk_c11) )
| ( inverse(sk_c11) != sk_c11 )
| ( multiply(inverse(sk_c10),sk_c10) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_118530]) ).
tcf(c_118714,plain,
! [X0: $i,X1: $i] :
( ( iPr_def_23 = inverse(X0) )
| ( iPr_def_23 != multiply(X1,sk_c10) )
| ( inverse(X0) != multiply(X1,sk_c10) ) ),
inference(instantiation,[status(thm)],[c_107156]) ).
tcf(c_119608,plain,
! [X0: $i] :
( ( multiply(inverse(sk_c10),sk_c10) = sk_c10 )
| ( sk_c10 != X0 )
| ( multiply(inverse(sk_c10),sk_c10) != X0 ) ),
inference(instantiation,[status(thm)],[c_100001]) ).
tcf(c_120115,plain,
( ( sk_c10 = identity )
| ( identity != multiply(identity,sk_c10) )
| ( sk_c10 != multiply(identity,sk_c10) ) ),
inference(instantiation,[status(thm)],[c_100552]) ).
tcf(c_120154,plain,
! [X0: $i,X1: $i] :
( ( identity = multiply(X0,sk_c10) )
| ( identity != X1 )
| ( multiply(X0,sk_c10) != X1 ) ),
inference(instantiation,[status(thm)],[c_100235]) ).
tcf(c_120431,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( inverse(X2) = multiply(inverse(X0),sk_c10) )
| ( inverse(X2) != inverse(X1) )
| ( multiply(inverse(X0),sk_c10) != inverse(X1) ) ),
inference(instantiation,[status(thm)],[c_100942]) ).
tcf(c_120650,plain,
( ( sk_c10 = multiply(inverse(sk_c10),sk_c10) )
| ( sk_c10 != identity )
| ( multiply(inverse(sk_c10),sk_c10) != identity ) ),
inference(instantiation,[status(thm)],[c_100178]) ).
tcf(c_121152,plain,
( ( multiply(inverse(iPr_def_26),sk_c10) = sk_c11 )
| ( sk_c11 != multiply(inverse(sk_c10),sk_c10) )
| ( multiply(inverse(iPr_def_26),sk_c10) != multiply(inverse(sk_c10),sk_c10) ) ),
inference(instantiation,[status(thm)],[c_100076]) ).
tcf(c_126003,plain,
! [X0: $i] :
( ( multiply(inverse(sk_c10),sk_c10) = sk_c10 )
| ( sk_c10 != multiply(inverse(X0),sk_c10) )
| ( multiply(inverse(sk_c10),sk_c10) != multiply(inverse(X0),sk_c10) ) ),
inference(instantiation,[status(thm)],[c_119608]) ).
tcf(c_126004,plain,
( ( multiply(inverse(sk_c10),sk_c10) = sk_c10 )
| ( sk_c10 != multiply(inverse(sk_c11),sk_c10) )
| ( multiply(inverse(sk_c10),sk_c10) != multiply(inverse(sk_c11),sk_c10) ) ),
inference(instantiation,[status(thm)],[c_126003]) ).
tcf(c_129466,plain,
! [X0: $i] :
( ( identity = iPr_def_27 )
| ( iPr_def_27 != inverse(X0) )
| ( identity != inverse(X0) ) ),
inference(instantiation,[status(thm)],[c_107147]) ).
tcf(c_129469,plain,
( ( identity = iPr_def_27 )
| ( iPr_def_27 != inverse(sk_c11) )
| ( identity != inverse(sk_c11) ) ),
inference(instantiation,[status(thm)],[c_129466]) ).
tcf(c_131998,plain,
( ( sk_c10 = multiply(inverse(sk_c10),sk_c10) )
| ( sk_c10 != sk_c11 )
| ( multiply(inverse(sk_c10),sk_c10) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_118165]) ).
tcf(c_132171,plain,
( ( iPr_def_23 = multiply(inverse(sk_c10),sk_c10) )
| ( iPr_def_23 != identity )
| ( multiply(inverse(sk_c10),sk_c10) != identity ) ),
inference(instantiation,[status(thm)],[c_100178]) ).
tcf(c_135012,plain,
( ( inverse(sk_c10) = iPr_def_25 )
| ( iPr_def_25 != inverse(sk_c3) )
| ( inverse(sk_c10) != inverse(sk_c3) ) ),
inference(instantiation,[status(thm)],[c_103334]) ).
tcf(c_135014,plain,
! [X0: $i] :
( ( inverse(sk_c10) = inverse(X0) )
| ( inverse(sk_c10) != iPr_def_25 )
| ( inverse(X0) != iPr_def_25 ) ),
inference(instantiation,[status(thm)],[c_107181]) ).
tcf(c_135015,plain,
( ( inverse(sk_c10) = inverse(sk_c11) )
| ( inverse(sk_c10) != iPr_def_25 )
| ( inverse(sk_c11) != iPr_def_25 ) ),
inference(instantiation,[status(thm)],[c_135014]) ).
tcf(c_135421,plain,
( ( identity = multiply(identity,sk_c10) )
| ( identity != inverse(sk_c4) )
| ( multiply(identity,sk_c10) != inverse(sk_c4) ) ),
inference(instantiation,[status(thm)],[c_120154]) ).
tcf(c_139050,plain,
( ( identity = inverse(sk_c10) )
| ( identity != iPr_def_15 )
| ( inverse(sk_c10) != iPr_def_15 ) ),
inference(instantiation,[status(thm)],[c_110495]) ).
tcf(c_142323,plain,
! [X0: $i] :
( ( iPr_def_23 = inverse(X0) )
| ( iPr_def_23 != multiply(inverse(sk_c10),sk_c10) )
| ( inverse(X0) != multiply(inverse(sk_c10),sk_c10) ) ),
inference(instantiation,[status(thm)],[c_118714]) ).
tcf(c_142327,plain,
( ( iPr_def_23 = inverse(sk_c11) )
| ( iPr_def_23 != multiply(inverse(sk_c10),sk_c10) )
| ( inverse(sk_c11) != multiply(inverse(sk_c10),sk_c10) ) ),
inference(instantiation,[status(thm)],[c_142323]) ).
tcf(c_146810,plain,
( ~ iPr_def_10
| ( inverse(sk_c9) != sk_c11 ) ),
inference(global_subsumption_just,[status(thm)],[c_90246,c_23675,c_90246]) ).
tcf(c_146821,plain,
( ( identity = iPr_def_24 )
| ~ iPr_def_10
| ( inverse(iPr_def_14) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_33704,c_146810]) ).
tcf(c_146822,plain,
( ( iPr_def_23 = iPr_def_26 )
| ~ iPr_def_10
| ( inverse(iPr_def_14) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_32051,c_146810]) ).
tcf(c_146825,plain,
( ( identity = iPr_def_22 )
| ~ iPr_def_10
| ( inverse(iPr_def_14) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_30138,c_146810]) ).
tcf(c_146837,plain,
( ( identity = iPr_def_22 )
| ~ iPr_def_10 ),
inference(ground_joinability,[status(thm)],[c_146825,c_36581]) ).
tcf(c_146846,plain,
( ( iPr_def_23 = iPr_def_26 )
| ~ iPr_def_10 ),
inference(ground_joinability,[status(thm)],[c_146822,c_36581]) ).
tcf(c_146849,plain,
( ( identity = iPr_def_24 )
| ~ iPr_def_10 ),
inference(ground_joinability,[status(thm)],[c_146821,c_36581]) ).
tcf(c_149266,plain,
! [X0: $i,X1: $i] :
( ( inverse(inverse(X0)) = inverse(iPr_def_26) )
| ( inverse(iPr_def_26) != X1 )
| ( inverse(inverse(X0)) != X1 ) ),
inference(instantiation,[status(thm)],[c_100316]) ).
tcf(c_149931,plain,
( ( identity = inverse(sk_c4) )
| ( identity != iPr_def_15 )
| ( inverse(sk_c4) != iPr_def_15 ) ),
inference(instantiation,[status(thm)],[c_110495]) ).
tcf(c_152844,plain,
( iPr_def_13
| iPr_def_12
| iPr_def_11
| ( identity = iPr_def_22 ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_24405,c_146837]) ).
tcf(c_156597,plain,
( iPr_def_13
| iPr_def_12
| iPr_def_11
| ( identity = iPr_def_24 ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_24318,c_146849]) ).
tcf(c_156606,plain,
( iPr_def_13
| ( identity = iPr_def_22 ) ),
inference(global_subsumption_just,[status(thm)],[c_152844,c_1440,c_1751,c_2228,c_4127,c_21208,c_21207,c_30832,c_36502,c_36744,c_51108,c_54652,c_54657,c_58946,c_84787,c_91377,c_92349,c_152844]) ).
tcf(c_156640,plain,
( ( identity = iPr_def_24 )
| ~ iPr_def_12
| ( sk_c11 != identity )
| ( multiply(inverse(sk_c9),iPr_def_14) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_18312,c_93569]) ).
tcf(c_156656,plain,
( ( sk_c11 = iPr_def_22 )
| ~ iPr_def_12
| ( sk_c11 != identity )
| ( multiply(inverse(sk_c9),iPr_def_14) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_677,c_93569]) ).
tcf(c_156682,plain,
( ( sk_c11 = iPr_def_22 )
| ~ iPr_def_12
| ( sk_c11 != identity ) ),
inference(ground_joinability,[status(thm)],[c_156656,c_84276]) ).
tcf(c_156710,plain,
( ( identity = iPr_def_24 )
| ~ iPr_def_12
| ( sk_c11 != identity ) ),
inference(ground_joinability,[status(thm)],[c_156640,c_84276]) ).
tcf(c_156955,plain,
( iPr_def_13
| ( identity = iPr_def_24 )
| iPr_def_11 ),
inference(global_subsumption_just,[status(thm)],[c_156597,c_637,c_1432,c_2228,c_2958,c_18312,c_36502,c_54652,c_54738,c_84790,c_146849,c_156710]) ).
tcf(c_156956,plain,
( iPr_def_13
| iPr_def_11
| ( identity = iPr_def_24 ) ),
inference(renaming,[status(thm)],[c_156955]) ).
tcf(c_160754,plain,
! [X0: $i] :
( ( inverse(inverse(X0)) = inverse(iPr_def_26) )
| ( inverse(iPr_def_26) != inverse(sk_c10) )
| ( inverse(inverse(X0)) != inverse(sk_c10) ) ),
inference(instantiation,[status(thm)],[c_149266]) ).
tcf(c_160755,plain,
( ( inverse(inverse(sk_c11)) = inverse(iPr_def_26) )
| ( inverse(iPr_def_26) != inverse(sk_c10) )
| ( inverse(inverse(sk_c11)) != inverse(sk_c10) ) ),
inference(instantiation,[status(thm)],[c_160754]) ).
tcf(c_165420,plain,
! [X0: $i,X1: $i] :
( ( inverse(X1) = multiply(inverse(sk_c10),sk_c10) )
| ( inverse(X1) != inverse(X0) )
| ( multiply(inverse(sk_c10),sk_c10) != inverse(X0) ) ),
inference(instantiation,[status(thm)],[c_120431]) ).
tcf(c_165426,plain,
( ( inverse(sk_c11) = multiply(inverse(sk_c10),sk_c10) )
| ( inverse(sk_c11) != inverse(sk_c11) )
| ( multiply(inverse(sk_c10),sk_c10) != inverse(sk_c11) ) ),
inference(instantiation,[status(thm)],[c_165420]) ).
tcf(c_169211,plain,
( ( identity = iPr_def_17 )
| ( multiply(inverse(sk_c4),iPr_def_24) = iPr_def_23 ) ),
inference(superposition,[status(thm)],[c_93850,c_59955]) ).
tcf(c_169213,plain,
( ( identity = iPr_def_14 )
| ( multiply(inverse(sk_c4),iPr_def_24) = iPr_def_23 ) ),
inference(superposition,[status(thm)],[c_37068,c_59955]) ).
tcf(c_169214,plain,
( ( iPr_def_17 = iPr_def_28 )
| ( multiply(inverse(sk_c4),iPr_def_24) = iPr_def_23 ) ),
inference(superposition,[status(thm)],[c_19828,c_59955]) ).
tcf(c_169380,plain,
( ( iPr_def_17 = iPr_def_28 )
| ( sk_c10 = iPr_def_23 ) ),
inference(light_normalisation,[status(thm)],[c_169214,c_631,c_5253]) ).
tcf(c_169383,plain,
( ( identity = iPr_def_14 )
| ( sk_c10 = iPr_def_23 ) ),
inference(light_normalisation,[status(thm)],[c_169213,c_631,c_5253]) ).
tcf(c_169389,plain,
( ( identity = iPr_def_17 )
| ( sk_c10 = iPr_def_23 ) ),
inference(light_normalisation,[status(thm)],[c_169211,c_631,c_5253]) ).
tcf(c_177096,plain,
( ( iPr_def_14 = iPr_def_23 )
| ( identity = iPr_def_14 )
| ( sk_c11 = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_169383,c_680]) ).
tcf(c_177097,plain,
( ( iPr_def_14 = iPr_def_23 )
| ( identity = iPr_def_14 )
| ( sk_c11 = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_169383,c_677]) ).
tcf(c_177304,plain,
( ~ iPr_def_10
| ( sk_c11 != sk_c10 ) ),
inference(global_subsumption_just,[status(thm)],[c_52788,c_625,c_1286,c_1285,c_1751,c_1997,c_3430,c_16396,c_19354,c_22645,c_22640,c_33442,c_33654,c_36581,c_43091,c_68594,c_84474,c_91375,c_100310,c_100683,c_102281,c_102962,c_105017,c_106208,c_108372,c_108381,c_131998,c_146846,c_169389,c_177096]) ).
tcf(c_177319,plain,
( ( sk_c11 = iPr_def_25 )
| ~ iPr_def_10
| ( sk_c11 != iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_680,c_177304]) ).
tcf(c_177421,plain,
( ( sk_c11 = iPr_def_25 )
| ~ iPr_def_10 ),
inference(global_subsumption_just,[status(thm)],[c_177319,c_698,c_625,c_1441,c_1751,c_1997,c_2228,c_3430,c_16396,c_19354,c_22645,c_22640,c_22828,c_33442,c_33654,c_36502,c_54652,c_68594,c_84474,c_91375,c_91377,c_92349,c_100013,c_100310,c_100683,c_101096,c_102281,c_102962,c_105017,c_108372,c_108381,c_146846,c_169389,c_169383,c_177096,c_177304]) ).
tcf(c_177423,plain,
~ iPr_def_10,
inference(global_subsumption_just,[status(thm)],[c_177421,c_698,c_625,c_1441,c_1751,c_1997,c_2228,c_3430,c_16396,c_19354,c_22828,c_33654,c_36502,c_54652,c_84474,c_91377,c_92349,c_100013,c_100310,c_100683,c_101096,c_102281,c_102962,c_105017,c_108372,c_108381,c_146846,c_169389,c_169383,c_177304,c_177421]) ).
tcf(c_177425,plain,
( iPr_def_13
| iPr_def_12
| iPr_def_11
| ( iPr_def_14 != iPr_def_23 ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_62753,c_177423]) ).
tcf(c_177427,plain,
( iPr_def_13
| iPr_def_12
| iPr_def_11
| ( sk_c10 != iPr_def_14 ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_42975,c_177423]) ).
tcf(c_177429,plain,
( iPr_def_13
| iPr_def_12
| iPr_def_11
| ( sk_c11 = iPr_def_22 ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_41495,c_177423]) ).
tcf(c_177474,plain,
( iPr_def_13
| ( sk_c11 = iPr_def_22 )
| iPr_def_11 ),
inference(global_subsumption_just,[status(thm)],[c_177429,c_157,c_158,c_696,c_698,c_623,c_625,c_631,c_1285,c_1310,c_1311,c_1751,c_1899,c_1997,c_2228,c_3294,c_3504,c_3505,c_5042,c_7074,c_9086,c_10326,c_14995,c_19354,c_31104,c_33441,c_33654,c_36502,c_54652,c_54738,c_63002,c_72407,c_84474,c_100013,c_100039,c_100070,c_100129,c_100310,c_100683,c_101096,c_101471,c_102281,c_102962,c_105017,c_106978,c_108270,c_108372,c_108381,c_113520,c_113963,c_120115,c_135421,c_149931,c_156682,c_169389,c_177429]) ).
tcf(c_177475,plain,
( iPr_def_13
| iPr_def_11
| ( sk_c11 = iPr_def_22 ) ),
inference(renaming,[status(thm)],[c_177474]) ).
tcf(c_177490,plain,
( iPr_def_13
| ( iPr_def_14 != iPr_def_23 )
| iPr_def_11 ),
inference(global_subsumption_just,[status(thm)],[c_177425,c_698,c_681,c_1285,c_1365,c_1751,c_1997,c_19354,c_22092,c_30739,c_63002,c_66485,c_68981,c_84474,c_100013,c_100310,c_101096,c_102290,c_106017,c_107961,c_107970,c_109729,c_113579,c_121152,c_156606,c_177425,c_177475]) ).
tcf(c_177491,plain,
( iPr_def_13
| iPr_def_11
| ( iPr_def_14 != iPr_def_23 ) ),
inference(renaming,[status(thm)],[c_177490]) ).
tcf(c_177632,plain,
( iPr_def_13
| ( sk_c10 != iPr_def_14 )
| iPr_def_11 ),
inference(global_subsumption_just,[status(thm)],[c_177427,c_698,c_1311,c_1432,c_1746,c_1751,c_1841,c_1842,c_2228,c_2958,c_12026,c_12043,c_14970,c_22092,c_30296,c_36502,c_54652,c_54738,c_84474,c_91377,c_92349,c_100013,c_100310,c_101096,c_102290,c_105069,c_107961,c_107970,c_113579,c_156606,c_169383,c_177427,c_177475,c_177491]) ).
tcf(c_177633,plain,
( iPr_def_13
| iPr_def_11
| ( sk_c10 != iPr_def_14 ) ),
inference(renaming,[status(thm)],[c_177632]) ).
tcf(c_177655,plain,
( iPr_def_13
| iPr_def_11
| ( sk_c11 = iPr_def_17 )
| ( iPr_def_14 != iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_651,c_177633]) ).
tcf(c_178261,plain,
( iPr_def_13
| ( sk_c11 = iPr_def_17 ) ),
inference(global_subsumption_just,[status(thm)],[c_177655,c_698,c_1082,c_1789,c_2228,c_2958,c_6131,c_6191,c_7030,c_7074,c_13260,c_17528,c_21210,c_22092,c_36502,c_54652,c_54706,c_68501,c_72407,c_84474,c_91120,c_91376,c_91381,c_92345,c_100013,c_100572,c_102290,c_107961,c_107970,c_113579,c_120650,c_177491,c_177633]) ).
tcf(c_179117,plain,
( ( sk_c11 = iPr_def_25 )
| ( identity = iPr_def_14 ) ),
inference(global_subsumption_just,[status(thm)],[c_177096,c_33442,c_36502,c_36741,c_68594,c_91375,c_91380,c_177096]) ).
tcf(c_179118,plain,
( ( identity = iPr_def_14 )
| ( sk_c11 = iPr_def_25 ) ),
inference(renaming,[status(thm)],[c_179117]) ).
tcf(c_179248,plain,
( ( identity = iPr_def_14 )
| ( multiply(sk_c3,iPr_def_25) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_179118,c_634]) ).
tcf(c_179257,plain,
( ( identity = iPr_def_26 )
| ( identity = iPr_def_14 ) ),
inference(light_normalisation,[status(thm)],[c_179248,c_17497]) ).
tcf(c_179548,plain,
identity = iPr_def_14,
inference(global_subsumption_just,[status(thm)],[c_177097,c_696,c_698,c_623,c_1432,c_1841,c_1842,c_1899,c_2958,c_12026,c_22092,c_36502,c_36677,c_36744,c_36741,c_54661,c_68501,c_68594,c_74662,c_79776,c_84474,c_91120,c_91375,c_102290,c_107961,c_107970,c_113579,c_118532,c_132171,c_142327,c_165426,c_169383,c_177097,c_179257]) ).
tcf(c_179556,plain,
( iPr_def_13
| iPr_def_11
| ( iPr_def_14 = iPr_def_24 ) ),
inference(demodulation,[status(thm)],[c_156956,c_179548]) ).
tcf(c_179622,plain,
multiply(sk_c10,multiply(inverse(iPr_def_17),sk_c2)) = iPr_def_14,
inference(demodulation,[status(thm)],[c_68432,c_179548]) ).
tcf(c_179630,plain,
( ~ iPr_def_12
| ( sk_c11 != iPr_def_14 )
| ( sk_c11 != sk_c10 ) ),
inference(demodulation,[status(thm)],[c_58933,c_179548]) ).
tcf(c_179697,plain,
multiply(sk_c1,iPr_def_27) = iPr_def_14,
inference(demodulation,[status(thm)],[c_26855,c_179548]) ).
tcf(c_179730,plain,
( ( iPr_def_17 = iPr_def_28 )
| ( iPr_def_14 = iPr_def_26 ) ),
inference(demodulation,[status(thm)],[c_20919,c_179548]) ).
tcf(c_179740,plain,
inverse(iPr_def_14) = iPr_def_14,
inference(demodulation,[status(thm)],[c_14947,c_179548]) ).
tcf(c_179741,plain,
! [X0: $i] : multiply(X0,iPr_def_14) = X0,
inference(demodulation,[status(thm)],[c_14918,c_179548]) ).
tcf(c_179750,plain,
multiply(iPr_def_27,sk_c1) = iPr_def_14,
inference(demodulation,[status(thm)],[c_1219,c_179548]) ).
tcf(c_180082,plain,
sk_c11 = iPr_def_14,
inference(demodulation,[status(thm)],[c_36581,c_179740]) ).
tcf(c_180084,plain,
( ~ iPr_def_12
| ( sk_c11 != sk_c10 ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_179630,c_180082]) ).
tcf(c_180361,plain,
( ( iPr_def_14 = iPr_def_25 )
| ( sk_c10 = iPr_def_14 ) ),
inference(demodulation,[status(thm)],[c_680,c_180082]) ).
tcf(c_180787,plain,
sk_c9 = iPr_def_14,
inference(demodulation,[status(thm)],[c_36654,c_179741]) ).
tcf(c_180790,plain,
sk_c3 = iPr_def_26,
inference(demodulation,[status(thm)],[c_36573,c_179741]) ).
tcf(c_180851,plain,
! [X0: $i] :
( ~ iPr_def_11
| ( inverse(X0) != sk_c10 )
| ( multiply(X0,sk_c10) != iPr_def_14 ) ),
inference(demodulation,[status(thm)],[c_640,c_180787]) ).
tcf(c_180968,plain,
sk_c10 = iPr_def_14,
inference(global_subsumption_just,[status(thm)],[c_180361,c_696,c_698,c_622,c_623,c_633,c_1285,c_1310,c_1311,c_1432,c_1841,c_1842,c_1899,c_1909,c_2228,c_2958,c_3511,c_3512,c_5139,c_5942,c_5943,c_9148,c_9462,c_9525,c_12026,c_22092,c_36502,c_36677,c_36744,c_36741,c_51118,c_51141,c_54652,c_54661,c_62516,c_65643,c_68501,c_68594,c_74662,c_79776,c_84474,c_91120,c_91375,c_91376,c_100068,c_100296,c_100559,c_102290,c_106631,c_106639,c_107961,c_107970,c_112998,c_112999,c_113012,c_113579,c_116634,c_118532,c_126004,c_132171,c_135012,c_135015,c_142327,c_165426,c_169383,c_177097,c_179257,c_180790,c_180082]) ).
tcf(c_181150,plain,
sk_c11 = iPr_def_17,
inference(global_subsumption_just,[status(thm)],[c_7007,c_696,c_698,c_622,c_623,c_633,c_1285,c_1310,c_1311,c_1432,c_1435,c_1436,c_1751,c_1841,c_1842,c_1899,c_1909,c_1996,c_1997,c_2228,c_2958,c_3294,c_3511,c_3512,c_5139,c_5942,c_5943,c_7030,c_9148,c_9462,c_9525,c_12026,c_22092,c_34299,c_36502,c_36677,c_36744,c_36741,c_51118,c_51141,c_54652,c_54661,c_54737,c_62516,c_65643,c_68501,c_68594,c_74662,c_79776,c_84474,c_91120,c_91375,c_91376,c_100068,c_100142,c_100296,c_100297,c_100310,c_100370,c_100559,c_101096,c_102290,c_106017,c_106124,c_106127,c_106631,c_106639,c_106976,c_107961,c_107970,c_109729,c_110497,c_112998,c_112999,c_113012,c_113181,c_113579,c_116634,c_118532,c_121152,c_126004,c_132171,c_135012,c_135015,c_139050,c_142327,c_160755,c_165426,c_169383,c_177097,c_178261,c_179257,c_180790,c_180082]) ).
tcf(c_181152,plain,
iPr_def_14 = iPr_def_17,
inference(light_normalisation,[status(thm)],[c_181150,c_180082]) ).
tcf(c_181208,plain,
multiply(iPr_def_27,iPr_def_14) = iPr_def_27,
inference(superposition,[status(thm)],[c_179697,c_2911]) ).
tcf(c_181416,plain,
multiply(inverse(iPr_def_14),iPr_def_27) = iPr_def_27,
inference(superposition,[status(thm)],[c_179750,c_59953]) ).
tcf(c_181417,plain,
multiply(iPr_def_14,iPr_def_27) = iPr_def_27,
inference(light_normalisation,[status(thm)],[c_181416,c_179740]) ).
tcf(c_181669,plain,
( iPr_def_13
| iPr_def_11 ),
inference(global_subsumption_just,[status(thm)],[c_179556,c_637,c_1432,c_1436,c_2228,c_2958,c_36502,c_54652,c_54738,c_177423,c_180082,c_180084,c_180968]) ).
tcf(c_181681,plain,
! [X0: $i] :
( ~ iPr_def_11
| ( X0 != iPr_def_14 )
| ( inverse(X0) != iPr_def_14 ) ),
inference(light_normalisation,[status(thm)],[c_180851,c_179741,c_180968]) ).
tcf(c_181713,plain,
( ~ iPr_def_11
| ( iPr_def_14 != iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_179740,c_181681]) ).
tcf(c_181714,plain,
~ iPr_def_11,
inference(equality_resolution_simp,[status(thm)],[c_181713]) ).
tcf(c_181715,plain,
iPr_def_13,
inference(backward_subsumption_resolution,[status(thm)],[c_181669,c_181714]) ).
tcf(c_181895,plain,
iPr_def_17 = iPr_def_28,
inference(global_subsumption_just,[status(thm)],[c_179730,c_696,c_698,c_622,c_623,c_633,c_1285,c_1310,c_1311,c_1432,c_1435,c_1436,c_1751,c_1841,c_1842,c_1899,c_1909,c_1997,c_2228,c_2958,c_3294,c_3511,c_3512,c_3848,c_5139,c_5942,c_5943,c_9148,c_9462,c_9525,c_12026,c_19354,c_22092,c_33655,c_36502,c_36677,c_36744,c_36741,c_51118,c_51141,c_54652,c_54661,c_54737,c_58261,c_62516,c_65643,c_68501,c_68594,c_74662,c_79776,c_84474,c_91120,c_91375,c_91376,c_100068,c_100142,c_100296,c_100297,c_100310,c_100370,c_100559,c_101096,c_102290,c_106017,c_106124,c_106127,c_106631,c_106639,c_106976,c_107961,c_107970,c_109729,c_110497,c_112998,c_112999,c_113012,c_113181,c_113579,c_116634,c_118532,c_121152,c_126004,c_132171,c_135012,c_135015,c_139050,c_142327,c_160755,c_165426,c_169383,c_169380,c_177097,c_179257,c_180790,c_180082,c_181715]) ).
tcf(c_181897,plain,
iPr_def_14 = iPr_def_28,
inference(light_normalisation,[status(thm)],[c_181895,c_181152]) ).
tcf(c_181925,plain,
multiply(iPr_def_27,iPr_def_14) = sk_c2,
inference(demodulation,[status(thm)],[c_4925,c_181897]) ).
tcf(c_181927,plain,
sk_c2 = iPr_def_27,
inference(light_normalisation,[status(thm)],[c_181925,c_181208]) ).
tcf(c_181966,plain,
iPr_def_14 = iPr_def_27,
inference(light_normalisation,[status(thm)],[c_179622,c_179740,c_180968,c_181152,c_181417,c_181927]) ).
tcf(c_181974,plain,
inverse(iPr_def_14) = sk_c1,
inference(demodulation,[status(thm)],[c_27196,c_181966]) ).
tcf(c_181977,plain,
sk_c1 = iPr_def_14,
inference(light_normalisation,[status(thm)],[c_181974,c_179740]) ).
tcf(c_185791,plain,
sk_c11 = iPr_def_17,
inference(global_subsumption_just,[status(thm)],[c_41764,c_181150]) ).
tcf(c_186019,plain,
( ( iPr_def_17 = iPr_def_25 )
| ( sk_c10 = iPr_def_14 ) ),
inference(demodulation,[status(thm)],[c_680,c_185791]) ).
tcf(c_186025,plain,
( ( iPr_def_17 = iPr_def_28 )
| ( sk_c10 = iPr_def_26 ) ),
inference(demodulation,[status(thm)],[c_671,c_185791]) ).
tcf(c_186039,plain,
( ( iPr_def_17 = iPr_def_25 )
| ( sk_c2 = iPr_def_27 ) ),
inference(demodulation,[status(thm)],[c_660,c_185791]) ).
tcf(c_186453,plain,
sk_c10 = iPr_def_14,
inference(global_subsumption_just,[status(thm)],[c_186019,c_696,c_698,c_622,c_623,c_633,c_1285,c_1310,c_1311,c_1432,c_1841,c_1842,c_1899,c_1909,c_2228,c_2958,c_3511,c_3512,c_5139,c_5942,c_5943,c_9148,c_9462,c_9525,c_12026,c_22092,c_36502,c_36677,c_36744,c_36741,c_51118,c_51141,c_54652,c_54661,c_62516,c_65643,c_68501,c_68594,c_74662,c_79776,c_84474,c_91120,c_91375,c_91376,c_100068,c_100296,c_100559,c_102290,c_106631,c_106639,c_107961,c_107970,c_112998,c_112999,c_113012,c_113579,c_116634,c_118532,c_126004,c_132171,c_135012,c_135015,c_142327,c_165426,c_169383,c_177097,c_179257,c_180790,c_180082]) ).
tcf(c_186540,plain,
multiply(sk_c2,iPr_def_14) = iPr_def_17,
inference(demodulation,[status(thm)],[c_625,c_186453]) ).
tcf(c_186621,plain,
iPr_def_17 = iPr_def_28,
inference(global_subsumption_just,[status(thm)],[c_186025,c_696,c_698,c_622,c_623,c_633,c_1285,c_1310,c_1311,c_1432,c_1435,c_1436,c_1751,c_1841,c_1842,c_1899,c_1909,c_1997,c_2228,c_2958,c_3294,c_3511,c_3512,c_3848,c_5139,c_5942,c_5943,c_9148,c_9462,c_9525,c_12026,c_19354,c_22092,c_33655,c_36502,c_36677,c_36744,c_36741,c_51118,c_51141,c_54652,c_54661,c_54737,c_58261,c_62516,c_65643,c_68501,c_68594,c_74662,c_79776,c_84474,c_91120,c_91375,c_91376,c_100068,c_100142,c_100296,c_100297,c_100310,c_100370,c_100559,c_101096,c_102290,c_106017,c_106124,c_106127,c_106631,c_106639,c_106976,c_107961,c_107970,c_109729,c_110497,c_112998,c_112999,c_113012,c_113181,c_113579,c_116634,c_118532,c_121152,c_126004,c_132171,c_135012,c_135015,c_139050,c_142327,c_160755,c_165426,c_169383,c_169380,c_177097,c_179257,c_180790,c_180082,c_181715]) ).
tcf(c_186639,plain,
multiply(sk_c1,sk_c2) = iPr_def_17,
inference(demodulation,[status(thm)],[c_636,c_186621]) ).
tcf(c_186697,plain,
sk_c2 = iPr_def_27,
inference(global_subsumption_just,[status(thm)],[c_186039,c_181927]) ).
tcf(c_186846,plain,
multiply(iPr_def_27,iPr_def_14) = iPr_def_17,
inference(light_normalisation,[status(thm)],[c_186540,c_186697]) ).
tcf(c_186863,plain,
multiply(sk_c1,iPr_def_27) = iPr_def_17,
inference(light_normalisation,[status(thm)],[c_186639,c_186697]) ).
tcf(c_187201,plain,
! [X0: $i] :
( ( inverse(inverse(X0)) != iPr_def_27 )
| ( multiply(X0,iPr_def_27) != inverse(X0) )
| ( multiply(sk_c1,iPr_def_27) != sk_c11 )
| ( multiply(iPr_def_27,sk_c10) != sk_c11 ) ),
inference(global_subsumption_just,[status(thm)],[c_41985,c_3639,c_181715]) ).
tcf(c_187202,plain,
! [X0: $i] :
( ( multiply(iPr_def_27,sk_c10) != sk_c11 )
| ( multiply(sk_c1,iPr_def_27) != sk_c11 )
| ( multiply(X0,iPr_def_27) != inverse(X0) )
| ( inverse(inverse(X0)) != iPr_def_27 ) ),
inference(renaming,[status(thm)],[c_187201]) ).
tcf(c_187204,plain,
! [X0: $i] :
( ( multiply(X0,iPr_def_27) != inverse(X0) )
| ( inverse(inverse(X0)) != iPr_def_27 ) ),
inference(ground_joinability,[status(thm)],[c_187202,c_186453,c_185791,c_186846,c_186863]) ).
tcf(c_187211,plain,
( ( inverse(identity) != iPr_def_27 )
| ( inverse(inverse(identity)) != iPr_def_27 ) ),
inference(superposition,[status(thm)],[c_103,c_187204]) ).
tcf(c_187221,plain,
identity != iPr_def_27,
inference(light_normalisation,[status(thm)],[c_187211,c_53029]) ).
tcf(c_187222,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_187221,c_181977,c_180968,c_180082,c_179548,c_139050,c_129469,c_113963,c_113181,c_110497,c_106978,c_106127,c_106124,c_100310,c_100297,c_100142,c_91376,c_88452,c_84474,c_74662,c_68157,c_54652,c_36677,c_36502,c_9277,c_3517,c_2228,c_1751,c_1435,c_1311,c_1310,c_1285,c_635,c_623]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GRP378-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.08/0.35 % Computer : n007.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Wed Sep 23 14:35:22 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.36 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.12/0.39 Running first-order theorem proving
% 0.12/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.12/0.41
% 0.12/0.41 % ======== iProver multi-core TPTP/SMT =========
% 0.12/0.41
% 0.12/0.41 % Detected problem language: tptp
% 0.12/0.42 % Proving...
% 53.54/9.83 % SZS status Started for theBenchmark.p
% 53.54/9.83 ERROR - "ProverProcess:heur/330959:296.0" ran with exit code 2 and error: iprover.ml: Unexpected exception: Failure("Clause.get_demod_eqs: not a demod/lightnorm conclusion ( multiply(X0,sk_c11) != inverse(X0) | X0 != sk_c11 | ~iPr_def_13 )")
% 53.54/9.83 Fatal error: exception Failure("Clause.get_demod_eqs: not a demod/lightnorm conclusion ( multiply(X0,sk_c11) != inverse(X0) | X0 != sk_c11 | ~iPr_def_13 )")
% 53.54/9.83 ERROR - cmd was: ulimit -v 4023281; ./res/iproveropt --abstr_ref "[]" --abstr_ref_af_restrict_to_split_sk false --abstr_ref_prep false --abstr_ref_sig_restrict funpre --abstr_ref_under "[]" --abstr_ref_until_sat false --add_important_lit false --bc_imp_inh "[conj_cone]" --brand_transform false --clause_weak_htbl true --comb_inst_mult 3 --comb_mode clause_based --comb_res_mult 1 --comb_sup_deep_mult 2 --comb_sup_mult 0 --conj_cone_tolerance 3. --demod_completeness_check fast --demod_use_ground true --eq_ax_congr_red true --extra_neg_conj none --gc_record_bc_elim false --inst_activity_threshold 500 --inst_dismatching true --inst_eager_unprocessed_to_passive true --inst_eq_res_simp false --inst_learning_factor 2 --inst_learning_loop_flag true --inst_learning_start 3000 --inst_lit_activity_flag true --inst_lit_sel "[+prop;+sign;+ground;-num_var;-num_symb]" --inst_lit_sel_side num_symb --inst_orphan_elimination true --inst_passive_queue_type priority_queues --inst_passive_queues "[[-conj_dist;+conj_symb;-num_var];[+age;-num_symb]]" --inst_passive_queues_freq "[25;2]" --inst_prop_sim_given true --inst_prop_sim_new false --inst_restr_to_given false --inst_sel_renew solver --inst_solver_calls_frac 1. --inst_solver_per_active 1400 --inst_sos_flag false --inst_sos_phase true --inst_sos_sth_lit_sel "[+prop;+non_prol_conj_symb;-eq;+ground;-num_var]" --inst_start_prop_sim_after_learn 3 --inst_subs_given false --inst_subs_new false --instantiation_flag true --large_theory_mode true --lt_threshold 2000 --min_unsat_core false --non_eq_to_eq false --pred_elim true --prep_def_merge true --prep_def_merge_mbd true --prep_def_merge_prop_impl false --prep_def_merge_tr_cl false --prep_def_merge_tr_red false --prep_gs_sim true --prep_res_sim true --prep_sem_filter exhaustive --prep_sem_filter_out false --prep_sup_sim_all true --prep_sup_sim_sup false --prep_unflatten true --prep_upred true --preprocessed_out false --preprocessed_stats false --preprocessing_flag true --prolific_symb_bound 256 --prop_impl_unit "[]" --prop_impl_unit_size 0 --prop_solver_per_cl 1024 --pure_diseq_elim true --res_backward_subs full --res_backward_subs_resolution true --res_forward_subs full --res_forward_subs_resolution true --res_lit_sel adaptive --res_lit_sel_side none --res_ordering kbo --res_orphan_elimination true --res_passive_queue_type priority_queues --res_passive_queues "[[-conj_dist;+conj_symb;-num_symb];[+age;-num_symb]]" --res_passive_queues_freq "[15;5]" --res_prop_simpl_given true --res_prop_simpl_new false --res_sim_input true --res_time_limit 300. --res_to_prop_solver active --reset_solvers false --resolution_flag true --schedule none --share_sel_clauses true --smt_ac_axioms fast --smt_preprocessing true --soft_assumptions false --soft_lemma_size 3 --splitting_cvd false --splitting_cvd_svl false --splitting_grd true --splitting_mode input --splitting_nvd 32 --stats_out none --sub_typing true --subs_bck_mult 8 --sup_full_bw "[BwDemod;BwUnitSubsAndRes]" --sup_full_fw "[FwDemodLightNormLoopTriv;FwUnitSubsAndRes;FwSubsumption;FwSubsumptionRes]" --sup_full_triv "[PropSubs]" --sup_fun_splitting false --sup_immed_bw_immed "[BwUnitSubsAndRes]" --sup_immed_bw_main "[BwUnitSubsAndRes]" --sup_immed_fw_immed "[ACNormalisation;FwDemodLightNormLoopTriv;FwUnitSubsAndRes]" --sup_immed_fw_main "[FwUnitSubsAndRes]" --sup_immed_triv "[]" --sup_indices_passive "[LightNormIndex;UnitSubsumptionIndex]" --sup_input_bw "[BwDemod;BwUnitSubsAndRes;BwSubsumption;BwSubsumptionRes]" --sup_input_fw "[ACNormalisation;FwDemodLightNormLoopTriv;FwUnitSubsAndRes;FwSubsumption;FwSubsumptionRes]" --sup_input_triv "[Unflattening]" --sup_iter_deepening 2 --sup_passive_queue_type priority_queues --sup_passive_queues "[[-conj_dist;-num_symb];[+age;-num_symb];[+score;-num_symb]]" --sup_passive_queues_freq "[8;4;4]" --sup_prop_simpl_given true --sup_prop_simpl_new true --sup_restarts_mult 2 --sup_score sim_d_gen --sup_share_max_num_cl 500 --sup_share_score_frac 0.2 --sup_smt_interval 10000 --sup_symb_ordering invfreq --sup_to_prop_solver passive --superposition_flag true --time_out_prep_mult 0.1 --suppress_sat_res true --tptp_safe_out true --out_options none --proof_out true --sat_out_model pos --clausifier res/vclausify_rel --clausifier_options "--mode clausify -t 98.67" --time_out_real 296.00 /export/starexec/sandbox2/benchmark/theBenchmark.p 1>> /export/starexec/sandbox2/tmp/iprover_out_n48aelaz/i5gnefiw 2>> /export/starexec/sandbox2/tmp/iprover_out_n48aelaz/i5gnefiw_error
% 53.54/9.83 % SZS status Unsatisfiable for theBenchmark.p
% 53.54/9.83
% 53.54/9.83 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 53.54/9.83
% 53.54/9.83 % ------ iProver source info
% 53.54/9.83
% 53.54/9.83 % git: date: 2026-07-19 20:42:38 +0200
% 53.54/9.83 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 53.54/9.83 % git: non_committed_changes: false
% 53.54/9.83
% 53.54/9.83 % ------ Parsing...% successful
% 53.54/9.83
% 53.54/9.83
% 53.54/9.83 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 53.54/9.83
% 53.54/9.83 % ------ Preprocessing... sup_sim: 0 sf_s rm: 0 0s sf_e pe_s pe_e %
% 53.54/9.83
% 53.54/9.83 % ------ Preprocessing... gs_s sp: 4 0s gs_e snvd_s sp: 0 0s snvd_e %
% 53.54/9.83
% 53.54/9.83 % ------ Preprocessing... sf_s rm: 0 0s sf_e
% 53.54/9.83 % ------ Proving...
% 53.54/9.83 % ------ Problem Properties
% 53.54/9.83
% 53.54/9.83 %
% 53.54/9.83 % clauses 73
% 53.54/9.83 % conjectures 55
% 53.54/9.83 % EPR 51
% 53.54/9.83 % Horn 22
% 53.54/9.83 % unary 18
% 53.54/9.83 % binary 50
% 53.54/9.83 % lits 138
% 53.54/9.83 % lits eq 130
% 53.54/9.83 % fd_pure 0
% 53.54/9.83 % fd_pseudo 0
% 53.54/9.83 % fd_cond 0
% 53.54/9.83 % fd_pseudo_cond 0
% 53.54/9.83 % AC symbols 0
% 53.54/9.83
% 53.54/9.83 % ------ Schedule dynamic 5 is on
% 53.54/9.83
% 53.54/9.83 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 53.54/9.83
% 53.54/9.83
% 53.54/9.83 % ------
% 53.54/9.83 % Current options:
% 53.54/9.83 % ------
% 53.54/9.83
% 53.54/9.83
% 53.54/9.83 %
% 53.54/9.83
% 53.54/9.83 % ------ Proving...
% 53.54/9.83 %
% 53.54/9.83
% 53.54/9.83 % SZS status Unsatisfiable for theBenchmark.p
% 53.54/9.83
% 53.54/9.83 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 53.54/9.85
% 53.54/9.85
%------------------------------------------------------------------------------