%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : GRP382-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 : n026.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 01:33:36 PM UTC 2026
% Result : Unsatisfiable 78.16s 13.01s
% Output : CNFRefutation 78.16s
% Verified :
% SZS Type : Refutation
% Derivation depth : 47
% Number of leaves : 47
% Syntax : Number of formulae : 707 ( 81 unt; 0 def)
% Number of atoms : 1820 (1686 equ)
% Maximal formula atoms : 17 ( 2 avg)
% Number of connectives : 1895 ( 782 ~;1113 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 27 ( 4 avg)
% Maximal term depth : 6 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 7 ( 5 usr; 6 prp; 0-2 aty)
% Number of functors : 15 ( 15 usr; 13 con; 0-2 aty)
% Number of variables : 418 ( 0 sgn 418 !; 0 ?; 373 :)
% 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_c4,sk_c12) = sk_c11
| inverse(sk_c12) = sk_c11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_1) ).
fof(f6,plain,
( sk_c11 = multiply(sk_c4,sk_c12)
| inverse(sk_c12) = sk_c11 ),
inference(reorient_equations,[],[f5]) ).
fof(f7,negated_conjecture,
( inverse(sk_c4) = sk_c12
| inverse(sk_c12) = sk_c11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_2) ).
fof(f8,plain,
( sk_c12 = inverse(sk_c4)
| inverse(sk_c12) = sk_c11 ),
inference(reorient_equations,[],[f7]) ).
fof(f9,negated_conjecture,
( multiply(sk_c5,sk_c11) = sk_c10
| inverse(sk_c12) = sk_c11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_3) ).
fof(f10,negated_conjecture,
( inverse(sk_c5) = sk_c11
| inverse(sk_c12) = sk_c11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_4) ).
fof(f11,plain,
( sk_c11 = inverse(sk_c5)
| inverse(sk_c12) = sk_c11 ),
inference(reorient_equations,[],[f10]) ).
fof(f12,negated_conjecture,
( multiply(sk_c6,sk_c9) = sk_c12
| inverse(sk_c12) = sk_c11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_5) ).
fof(f13,plain,
( sk_c12 = multiply(sk_c6,sk_c9)
| inverse(sk_c12) = sk_c11 ),
inference(reorient_equations,[],[f12]) ).
fof(f14,negated_conjecture,
( inverse(sk_c6) = sk_c9
| inverse(sk_c12) = sk_c11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_6) ).
fof(f15,plain,
( sk_c9 = inverse(sk_c6)
| inverse(sk_c12) = sk_c11 ),
inference(reorient_equations,[],[f14]) ).
fof(f18,negated_conjecture,
( inverse(sk_c8) = sk_c7
| inverse(sk_c12) = sk_c11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_8) ).
fof(f19,negated_conjecture,
( inverse(sk_c7) = sk_c9
| inverse(sk_c12) = sk_c11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_9) ).
fof(f20,plain,
( sk_c9 = inverse(sk_c7)
| inverse(sk_c12) = sk_c11 ),
inference(reorient_equations,[],[f19]) ).
fof(f25,negated_conjecture,
( inverse(sk_c4) = sk_c12
| multiply(sk_c11,sk_c10) = sk_c12 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_12) ).
fof(f26,plain,
( sk_c12 = inverse(sk_c4)
| sk_c12 = multiply(sk_c11,sk_c10) ),
inference(reorient_equations,[],[f25]) ).
fof(f27,negated_conjecture,
( multiply(sk_c5,sk_c11) = sk_c10
| multiply(sk_c11,sk_c10) = sk_c12 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_13) ).
fof(f28,plain,
( multiply(sk_c5,sk_c11) = sk_c10
| sk_c12 = multiply(sk_c11,sk_c10) ),
inference(reorient_equations,[],[f27]) ).
fof(f29,negated_conjecture,
( inverse(sk_c5) = sk_c11
| multiply(sk_c11,sk_c10) = sk_c12 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_14) ).
fof(f30,plain,
( sk_c11 = inverse(sk_c5)
| sk_c12 = multiply(sk_c11,sk_c10) ),
inference(reorient_equations,[],[f29]) ).
fof(f33,negated_conjecture,
( inverse(sk_c6) = sk_c9
| multiply(sk_c11,sk_c10) = sk_c12 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_16) ).
fof(f34,plain,
( sk_c9 = inverse(sk_c6)
| sk_c12 = multiply(sk_c11,sk_c10) ),
inference(reorient_equations,[],[f33]) ).
fof(f43,negated_conjecture,
( multiply(sk_c4,sk_c12) = sk_c11
| inverse(sk_c1) = sk_c12 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_21) ).
fof(f44,plain,
( sk_c11 = multiply(sk_c4,sk_c12)
| sk_c12 = inverse(sk_c1) ),
inference(reorient_equations,[],[f43]) ).
fof(f45,negated_conjecture,
( inverse(sk_c4) = sk_c12
| inverse(sk_c1) = sk_c12 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_22) ).
fof(f46,plain,
( sk_c12 = inverse(sk_c4)
| sk_c12 = inverse(sk_c1) ),
inference(reorient_equations,[],[f45]) ).
fof(f47,negated_conjecture,
( multiply(sk_c5,sk_c11) = sk_c10
| inverse(sk_c1) = sk_c12 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_23) ).
fof(f48,plain,
( multiply(sk_c5,sk_c11) = sk_c10
| sk_c12 = inverse(sk_c1) ),
inference(reorient_equations,[],[f47]) ).
fof(f49,negated_conjecture,
( inverse(sk_c5) = sk_c11
| inverse(sk_c1) = sk_c12 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_24) ).
fof(f50,plain,
( sk_c11 = inverse(sk_c5)
| sk_c12 = inverse(sk_c1) ),
inference(reorient_equations,[],[f49]) ).
fof(f51,negated_conjecture,
( multiply(sk_c6,sk_c9) = sk_c12
| inverse(sk_c1) = sk_c12 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_25) ).
fof(f52,plain,
( sk_c12 = multiply(sk_c6,sk_c9)
| sk_c12 = inverse(sk_c1) ),
inference(reorient_equations,[],[f51]) ).
fof(f53,negated_conjecture,
( inverse(sk_c6) = sk_c9
| inverse(sk_c1) = sk_c12 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_26) ).
fof(f54,plain,
( sk_c9 = inverse(sk_c6)
| sk_c12 = inverse(sk_c1) ),
inference(reorient_equations,[],[f53]) ).
fof(f55,negated_conjecture,
( multiply(sk_c9,sk_c11) = sk_c12
| inverse(sk_c1) = sk_c12 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_27) ).
fof(f56,plain,
( sk_c12 = multiply(sk_c9,sk_c11)
| sk_c12 = inverse(sk_c1) ),
inference(reorient_equations,[],[f55]) ).
fof(f63,negated_conjecture,
( multiply(sk_c4,sk_c12) = sk_c11
| multiply(sk_c1,sk_c11) = sk_c12 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_31) ).
fof(f64,plain,
( sk_c11 = multiply(sk_c4,sk_c12)
| sk_c12 = multiply(sk_c1,sk_c11) ),
inference(reorient_equations,[],[f63]) ).
fof(f65,negated_conjecture,
( inverse(sk_c4) = sk_c12
| multiply(sk_c1,sk_c11) = sk_c12 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_32) ).
fof(f66,plain,
( sk_c12 = inverse(sk_c4)
| sk_c12 = multiply(sk_c1,sk_c11) ),
inference(reorient_equations,[],[f65]) ).
fof(f69,negated_conjecture,
( inverse(sk_c5) = sk_c11
| multiply(sk_c1,sk_c11) = sk_c12 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_34) ).
fof(f70,plain,
( sk_c11 = inverse(sk_c5)
| sk_c12 = multiply(sk_c1,sk_c11) ),
inference(reorient_equations,[],[f69]) ).
fof(f71,negated_conjecture,
( multiply(sk_c6,sk_c9) = sk_c12
| multiply(sk_c1,sk_c11) = sk_c12 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_35) ).
fof(f72,plain,
( sk_c12 = multiply(sk_c6,sk_c9)
| sk_c12 = multiply(sk_c1,sk_c11) ),
inference(reorient_equations,[],[f71]) ).
fof(f73,negated_conjecture,
( inverse(sk_c6) = sk_c9
| multiply(sk_c1,sk_c11) = sk_c12 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_36) ).
fof(f74,plain,
( sk_c9 = inverse(sk_c6)
| sk_c12 = multiply(sk_c1,sk_c11) ),
inference(reorient_equations,[],[f73]) ).
fof(f83,negated_conjecture,
( multiply(sk_c4,sk_c12) = sk_c11
| multiply(sk_c2,sk_c3) = sk_c11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_41) ).
fof(f84,plain,
( sk_c11 = multiply(sk_c4,sk_c12)
| sk_c11 = multiply(sk_c2,sk_c3) ),
inference(reorient_equations,[],[f83]) ).
fof(f85,negated_conjecture,
( inverse(sk_c4) = sk_c12
| multiply(sk_c2,sk_c3) = sk_c11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_42) ).
fof(f86,plain,
( sk_c12 = inverse(sk_c4)
| sk_c11 = multiply(sk_c2,sk_c3) ),
inference(reorient_equations,[],[f85]) ).
fof(f87,negated_conjecture,
( multiply(sk_c5,sk_c11) = sk_c10
| multiply(sk_c2,sk_c3) = sk_c11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_43) ).
fof(f88,plain,
( multiply(sk_c5,sk_c11) = sk_c10
| sk_c11 = multiply(sk_c2,sk_c3) ),
inference(reorient_equations,[],[f87]) ).
fof(f89,negated_conjecture,
( inverse(sk_c5) = sk_c11
| multiply(sk_c2,sk_c3) = sk_c11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_44) ).
fof(f90,plain,
( sk_c11 = inverse(sk_c5)
| sk_c11 = multiply(sk_c2,sk_c3) ),
inference(reorient_equations,[],[f89]) ).
fof(f93,negated_conjecture,
( inverse(sk_c6) = sk_c9
| multiply(sk_c2,sk_c3) = sk_c11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_46) ).
fof(f94,plain,
( sk_c9 = inverse(sk_c6)
| sk_c11 = multiply(sk_c2,sk_c3) ),
inference(reorient_equations,[],[f93]) ).
fof(f103,negated_conjecture,
( multiply(sk_c4,sk_c12) = sk_c11
| inverse(sk_c2) = sk_c3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_51) ).
fof(f104,plain,
( sk_c11 = multiply(sk_c4,sk_c12)
| sk_c3 = inverse(sk_c2) ),
inference(reorient_equations,[],[f103]) ).
fof(f105,negated_conjecture,
( inverse(sk_c4) = sk_c12
| inverse(sk_c2) = sk_c3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_52) ).
fof(f106,plain,
( sk_c12 = inverse(sk_c4)
| sk_c3 = inverse(sk_c2) ),
inference(reorient_equations,[],[f105]) ).
fof(f107,negated_conjecture,
( multiply(sk_c5,sk_c11) = sk_c10
| inverse(sk_c2) = sk_c3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_53) ).
fof(f108,plain,
( multiply(sk_c5,sk_c11) = sk_c10
| sk_c3 = inverse(sk_c2) ),
inference(reorient_equations,[],[f107]) ).
fof(f109,negated_conjecture,
( inverse(sk_c5) = sk_c11
| inverse(sk_c2) = sk_c3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_54) ).
fof(f110,plain,
( sk_c11 = inverse(sk_c5)
| sk_c3 = inverse(sk_c2) ),
inference(reorient_equations,[],[f109]) ).
fof(f111,negated_conjecture,
( multiply(sk_c6,sk_c9) = sk_c12
| inverse(sk_c2) = sk_c3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_55) ).
fof(f112,plain,
( sk_c12 = multiply(sk_c6,sk_c9)
| sk_c3 = inverse(sk_c2) ),
inference(reorient_equations,[],[f111]) ).
fof(f113,negated_conjecture,
( inverse(sk_c6) = sk_c9
| inverse(sk_c2) = sk_c3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_56) ).
fof(f114,plain,
( sk_c9 = inverse(sk_c6)
| sk_c3 = inverse(sk_c2) ),
inference(reorient_equations,[],[f113]) ).
fof(f115,negated_conjecture,
( multiply(sk_c9,sk_c11) = sk_c12
| inverse(sk_c2) = sk_c3 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_57) ).
fof(f116,plain,
( sk_c12 = multiply(sk_c9,sk_c11)
| sk_c3 = inverse(sk_c2) ),
inference(reorient_equations,[],[f115]) ).
fof(f125,negated_conjecture,
( inverse(sk_c4) = sk_c12
| multiply(sk_c3,sk_c12) = sk_c11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_62) ).
fof(f126,plain,
( sk_c12 = inverse(sk_c4)
| sk_c11 = multiply(sk_c3,sk_c12) ),
inference(reorient_equations,[],[f125]) ).
fof(f129,negated_conjecture,
( inverse(sk_c5) = sk_c11
| multiply(sk_c3,sk_c12) = sk_c11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_64) ).
fof(f130,plain,
( sk_c11 = inverse(sk_c5)
| sk_c11 = multiply(sk_c3,sk_c12) ),
inference(reorient_equations,[],[f129]) ).
fof(f133,negated_conjecture,
( inverse(sk_c6) = sk_c9
| multiply(sk_c3,sk_c12) = sk_c11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_66) ).
fof(f134,plain,
( sk_c9 = inverse(sk_c6)
| sk_c11 = multiply(sk_c3,sk_c12) ),
inference(reorient_equations,[],[f133]) ).
fof(f143,negated_conjecture,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( multiply(X7,X6) != X8
| inverse(X8) != X6
| inverse(X7) != X8
| multiply(X6,sk_c11) != sk_c12
| inverse(X5) != X6
| multiply(X5,X6) != sk_c12
| inverse(X4) != sk_c11
| multiply(X4,sk_c11) != sk_c10
| inverse(X3) != sk_c12
| multiply(X3,sk_c12) != sk_c11
| multiply(X2,sk_c12) != sk_c11
| inverse(X1) != X2
| multiply(X1,X2) != sk_c11
| multiply(X0,sk_c11) != sk_c12
| inverse(X0) != sk_c12
| multiply(sk_c11,sk_c10) != sk_c12
| inverse(sk_c12) != sk_c11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_71) ).
fof(f144,plain,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( multiply(X7,X6) != X8
| inverse(X8) != X6
| inverse(X7) != X8
| sk_c12 != multiply(X6,sk_c11)
| inverse(X5) != X6
| sk_c12 != multiply(X5,X6)
| sk_c11 != inverse(X4)
| sk_c10 != multiply(X4,sk_c11)
| sk_c12 != inverse(X3)
| sk_c11 != multiply(X3,sk_c12)
| sk_c11 != multiply(X2,sk_c12)
| inverse(X1) != X2
| multiply(X1,X2) != sk_c11
| sk_c12 != multiply(X0,sk_c11)
| inverse(X0) != sk_c12
| sk_c12 != multiply(sk_c11,sk_c10)
| inverse(sk_c12) != sk_c11 ),
inference(reorient_equations,[],[f143]) ).
fof(f145,plain,
! [X3,X0,X1,X8,X6,X7,X4,X5] :
( multiply(X7,X6) != X8
| inverse(X8) != X6
| inverse(X7) != X8
| sk_c12 != multiply(X6,sk_c11)
| inverse(X5) != X6
| sk_c12 != multiply(X5,X6)
| sk_c11 != inverse(X4)
| sk_c10 != multiply(X4,sk_c11)
| sk_c12 != inverse(X3)
| sk_c11 != multiply(X3,sk_c12)
| sk_c11 != multiply(inverse(X1),sk_c12)
| sk_c11 != multiply(X1,inverse(X1))
| sk_c12 != multiply(X0,sk_c11)
| inverse(X0) != sk_c12
| sk_c12 != multiply(sk_c11,sk_c10)
| inverse(sk_c12) != sk_c11 ),
inference(equality_resolution,[],[f144]) ).
fof(f146,plain,
! [X3,X0,X1,X8,X7,X4,X5] :
( multiply(X7,inverse(X5)) != X8
| inverse(X5) != inverse(X8)
| inverse(X7) != X8
| sk_c12 != multiply(inverse(X5),sk_c11)
| sk_c12 != multiply(X5,inverse(X5))
| sk_c11 != inverse(X4)
| sk_c10 != multiply(X4,sk_c11)
| sk_c12 != inverse(X3)
| sk_c11 != multiply(X3,sk_c12)
| sk_c11 != multiply(inverse(X1),sk_c12)
| sk_c11 != multiply(X1,inverse(X1))
| sk_c12 != multiply(X0,sk_c11)
| inverse(X0) != sk_c12
| sk_c12 != multiply(sk_c11,sk_c10)
| inverse(sk_c12) != sk_c11 ),
inference(equality_resolution,[],[f145]) ).
fof(f147,plain,
! [X3,X0,X1,X7,X4,X5] :
( inverse(X7) != multiply(X7,inverse(X5))
| inverse(X5) != inverse(inverse(X7))
| sk_c12 != multiply(inverse(X5),sk_c11)
| sk_c12 != multiply(X5,inverse(X5))
| sk_c11 != inverse(X4)
| sk_c10 != multiply(X4,sk_c11)
| sk_c12 != inverse(X3)
| sk_c11 != multiply(X3,sk_c12)
| sk_c11 != multiply(inverse(X1),sk_c12)
| sk_c11 != multiply(X1,inverse(X1))
| sk_c12 != multiply(X0,sk_c11)
| inverse(X0) != sk_c12
| sk_c12 != multiply(sk_c11,sk_c10)
| inverse(sk_c12) != sk_c11 ),
inference(equality_resolution,[],[f146]) ).
tcf(c_123,plain,
! [X0: $i] : multiply(identity,X0) = X0,
inference(cnf_transformation,[],[f1]) ).
tcf(c_124,plain,
! [X0: $i] : multiply(inverse(X0),X0) = identity,
inference(cnf_transformation,[],[f3]) ).
tcf(c_125,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(multiply(X0,X1),X2) = multiply(X0,multiply(X1,X2)),
inference(cnf_transformation,[],[f4]) ).
tcf(c_126,negated_conjecture,
( ( inverse(sk_c12) = sk_c11 )
| ( multiply(sk_c4,sk_c12) = sk_c11 ) ),
inference(cnf_transformation,[],[f6]) ).
tcf(c_127,negated_conjecture,
( ( inverse(sk_c4) = sk_c12 )
| ( inverse(sk_c12) = sk_c11 ) ),
inference(cnf_transformation,[],[f8]) ).
tcf(c_128,negated_conjecture,
( ( inverse(sk_c12) = sk_c11 )
| ( multiply(sk_c5,sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f9]) ).
tcf(c_129,negated_conjecture,
( ( inverse(sk_c5) = sk_c11 )
| ( inverse(sk_c12) = sk_c11 ) ),
inference(cnf_transformation,[],[f11]) ).
tcf(c_130,negated_conjecture,
( ( inverse(sk_c12) = sk_c11 )
| ( multiply(sk_c6,sk_c9) = sk_c12 ) ),
inference(cnf_transformation,[],[f13]) ).
tcf(c_131,negated_conjecture,
( ( inverse(sk_c6) = sk_c9 )
| ( inverse(sk_c12) = sk_c11 ) ),
inference(cnf_transformation,[],[f15]) ).
tcf(c_133,negated_conjecture,
( ( inverse(sk_c8) = sk_c7 )
| ( inverse(sk_c12) = sk_c11 ) ),
inference(cnf_transformation,[],[f18]) ).
tcf(c_134,negated_conjecture,
( ( inverse(sk_c7) = sk_c9 )
| ( inverse(sk_c12) = sk_c11 ) ),
inference(cnf_transformation,[],[f20]) ).
tcf(c_137,negated_conjecture,
( ( inverse(sk_c4) = sk_c12 )
| ( multiply(sk_c11,sk_c10) = sk_c12 ) ),
inference(cnf_transformation,[],[f26]) ).
tcf(c_138,negated_conjecture,
( ( multiply(sk_c5,sk_c11) = sk_c10 )
| ( multiply(sk_c11,sk_c10) = sk_c12 ) ),
inference(cnf_transformation,[],[f28]) ).
tcf(c_139,negated_conjecture,
( ( inverse(sk_c5) = sk_c11 )
| ( multiply(sk_c11,sk_c10) = sk_c12 ) ),
inference(cnf_transformation,[],[f30]) ).
tcf(c_141,negated_conjecture,
( ( inverse(sk_c6) = sk_c9 )
| ( multiply(sk_c11,sk_c10) = sk_c12 ) ),
inference(cnf_transformation,[],[f34]) ).
tcf(c_146,negated_conjecture,
( ( inverse(sk_c1) = sk_c12 )
| ( multiply(sk_c4,sk_c12) = sk_c11 ) ),
inference(cnf_transformation,[],[f44]) ).
tcf(c_147,negated_conjecture,
( ( inverse(sk_c1) = sk_c12 )
| ( inverse(sk_c4) = sk_c12 ) ),
inference(cnf_transformation,[],[f46]) ).
tcf(c_148,negated_conjecture,
( ( inverse(sk_c1) = sk_c12 )
| ( multiply(sk_c5,sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f48]) ).
tcf(c_149,negated_conjecture,
( ( inverse(sk_c1) = sk_c12 )
| ( inverse(sk_c5) = sk_c11 ) ),
inference(cnf_transformation,[],[f50]) ).
tcf(c_150,negated_conjecture,
( ( inverse(sk_c1) = sk_c12 )
| ( multiply(sk_c6,sk_c9) = sk_c12 ) ),
inference(cnf_transformation,[],[f52]) ).
tcf(c_151,negated_conjecture,
( ( inverse(sk_c1) = sk_c12 )
| ( inverse(sk_c6) = sk_c9 ) ),
inference(cnf_transformation,[],[f54]) ).
tcf(c_152,negated_conjecture,
( ( inverse(sk_c1) = sk_c12 )
| ( multiply(sk_c9,sk_c11) = sk_c12 ) ),
inference(cnf_transformation,[],[f56]) ).
tcf(c_156,negated_conjecture,
( ( multiply(sk_c1,sk_c11) = sk_c12 )
| ( multiply(sk_c4,sk_c12) = sk_c11 ) ),
inference(cnf_transformation,[],[f64]) ).
tcf(c_157,negated_conjecture,
( ( inverse(sk_c4) = sk_c12 )
| ( multiply(sk_c1,sk_c11) = sk_c12 ) ),
inference(cnf_transformation,[],[f66]) ).
tcf(c_159,negated_conjecture,
( ( inverse(sk_c5) = sk_c11 )
| ( multiply(sk_c1,sk_c11) = sk_c12 ) ),
inference(cnf_transformation,[],[f70]) ).
tcf(c_160,negated_conjecture,
( ( multiply(sk_c1,sk_c11) = sk_c12 )
| ( multiply(sk_c6,sk_c9) = sk_c12 ) ),
inference(cnf_transformation,[],[f72]) ).
tcf(c_161,negated_conjecture,
( ( inverse(sk_c6) = sk_c9 )
| ( multiply(sk_c1,sk_c11) = sk_c12 ) ),
inference(cnf_transformation,[],[f74]) ).
tcf(c_166,negated_conjecture,
( ( multiply(sk_c2,sk_c3) = sk_c11 )
| ( multiply(sk_c4,sk_c12) = sk_c11 ) ),
inference(cnf_transformation,[],[f84]) ).
tcf(c_167,negated_conjecture,
( ( inverse(sk_c4) = sk_c12 )
| ( multiply(sk_c2,sk_c3) = sk_c11 ) ),
inference(cnf_transformation,[],[f86]) ).
tcf(c_168,negated_conjecture,
( ( multiply(sk_c2,sk_c3) = sk_c11 )
| ( multiply(sk_c5,sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f88]) ).
tcf(c_169,negated_conjecture,
( ( inverse(sk_c5) = sk_c11 )
| ( multiply(sk_c2,sk_c3) = sk_c11 ) ),
inference(cnf_transformation,[],[f90]) ).
tcf(c_171,negated_conjecture,
( ( inverse(sk_c6) = sk_c9 )
| ( multiply(sk_c2,sk_c3) = sk_c11 ) ),
inference(cnf_transformation,[],[f94]) ).
tcf(c_176,negated_conjecture,
( ( inverse(sk_c2) = sk_c3 )
| ( multiply(sk_c4,sk_c12) = sk_c11 ) ),
inference(cnf_transformation,[],[f104]) ).
tcf(c_177,negated_conjecture,
( ( inverse(sk_c2) = sk_c3 )
| ( inverse(sk_c4) = sk_c12 ) ),
inference(cnf_transformation,[],[f106]) ).
tcf(c_178,negated_conjecture,
( ( inverse(sk_c2) = sk_c3 )
| ( multiply(sk_c5,sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f108]) ).
tcf(c_179,negated_conjecture,
( ( inverse(sk_c2) = sk_c3 )
| ( inverse(sk_c5) = sk_c11 ) ),
inference(cnf_transformation,[],[f110]) ).
tcf(c_180,negated_conjecture,
( ( inverse(sk_c2) = sk_c3 )
| ( multiply(sk_c6,sk_c9) = sk_c12 ) ),
inference(cnf_transformation,[],[f112]) ).
tcf(c_181,negated_conjecture,
( ( inverse(sk_c2) = sk_c3 )
| ( inverse(sk_c6) = sk_c9 ) ),
inference(cnf_transformation,[],[f114]) ).
tcf(c_182,negated_conjecture,
( ( inverse(sk_c2) = sk_c3 )
| ( multiply(sk_c9,sk_c11) = sk_c12 ) ),
inference(cnf_transformation,[],[f116]) ).
tcf(c_187,negated_conjecture,
( ( inverse(sk_c4) = sk_c12 )
| ( multiply(sk_c3,sk_c12) = sk_c11 ) ),
inference(cnf_transformation,[],[f126]) ).
tcf(c_189,negated_conjecture,
( ( inverse(sk_c5) = sk_c11 )
| ( multiply(sk_c3,sk_c12) = sk_c11 ) ),
inference(cnf_transformation,[],[f130]) ).
tcf(c_191,negated_conjecture,
( ( inverse(sk_c6) = sk_c9 )
| ( multiply(sk_c3,sk_c12) = sk_c11 ) ),
inference(cnf_transformation,[],[f134]) ).
tcf(c_196,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( ( inverse(sk_c12) != sk_c11 )
| ( inverse(X5) != sk_c11 )
| ( inverse(X3) != sk_c12 )
| ( inverse(X2) != sk_c12 )
| ( multiply(sk_c11,sk_c10) != sk_c12 )
| ( multiply(X5,sk_c11) != sk_c10 )
| ( multiply(X3,sk_c12) != sk_c11 )
| ( multiply(X2,sk_c11) != sk_c12 )
| ( inverse(inverse(X0)) != inverse(X1) )
| ( multiply(inverse(X4),sk_c12) != sk_c11 )
| ( multiply(inverse(X1),sk_c11) != sk_c12 )
| ( multiply(X4,inverse(X4)) != sk_c11 )
| ( multiply(X1,inverse(X1)) != sk_c12 )
| ( multiply(X0,inverse(X1)) != inverse(X0) ) ),
inference(cnf_transformation,[],[f147]) ).
tcf(c_825,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_10
| ( inverse(X0) != sk_c12 )
| ( multiply(X0,sk_c12) != sk_c11 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_10])],[c_196]) ).
tcf(c_826,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_11
| ( inverse(X0) != sk_c12 )
| ( multiply(X0,sk_c11) != sk_c12 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_11])],[c_196]) ).
tcf(c_827,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_12
| ( inverse(X0) != sk_c11 )
| ( multiply(X0,sk_c11) != sk_c10 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_12])],[c_196]) ).
tcf(c_828,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_13
| ( multiply(inverse(X0),sk_c12) != sk_c11 )
| ( multiply(X0,inverse(X0)) != sk_c11 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_13])],[c_196]) ).
tcf(c_829,negated_conjecture,
! [X0: $i,X1: $i] :
( ~ iPr_def_14
| ( inverse(inverse(X0)) != inverse(X1) )
| ( multiply(inverse(X1),sk_c11) != sk_c12 )
| ( multiply(X1,inverse(X1)) != sk_c12 )
| ( multiply(X0,inverse(X1)) != inverse(X0) ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_14])],[c_196]) ).
tcf(c_830,negated_conjecture,
( iPr_def_14
| iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( inverse(sk_c12) != sk_c11 )
| ( multiply(sk_c11,sk_c10) != sk_c12 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_196]) ).
tcf(c_831,plain,
! [X0: $i] : X0 = X0,
theory(equality) ).
tcf(c_832,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = X0 )
| ( X2 != X1 )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_833,plain,
! [X0: $i,X1: $i] :
( ( inverse(X0) = inverse(X1) )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_834,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( multiply(X0,X2) = multiply(X1,X3) )
| ( X2 != X3 )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_837,plain,
sk_c11 = sk_c11,
inference(instantiation,[status(thm)],[c_831]) ).
tcf(c_840,plain,
( ~ iPr_def_12
| ( inverse(sk_c11) != sk_c11 )
| ( multiply(sk_c11,sk_c11) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_827]) ).
tcf(c_1195,plain,
! [X0: $i] :
( ( inverse(sk_c12) = sk_c11 )
| ( sk_c11 != X0 )
| ( inverse(sk_c12) != X0 ) ),
inference(instantiation,[status(thm)],[c_832]) ).
tcf(c_1198,plain,
! [X0: $i,X1: $i] :
( ( inverse(sk_c12) = X1 )
| ( X1 != X0 )
| ( inverse(sk_c12) != X0 ) ),
inference(instantiation,[status(thm)],[c_832]) ).
tcf(c_1199,plain,
! [X0: $i] :
( ( inverse(sk_c12) = sk_c11 )
| ( sk_c11 != inverse(X0) )
| ( inverse(sk_c12) != inverse(X0) ) ),
inference(instantiation,[status(thm)],[c_1195]) ).
tcf(c_1200,plain,
! [X0: $i] :
( ( inverse(sk_c12) = inverse(X0) )
| ( sk_c12 != X0 ) ),
inference(instantiation,[status(thm)],[c_833]) ).
tcf(c_1201,plain,
( ( inverse(sk_c12) = sk_c11 )
| ( sk_c11 != inverse(sk_c11) )
| ( inverse(sk_c12) != inverse(sk_c11) ) ),
inference(instantiation,[status(thm)],[c_1199]) ).
tcf(c_1202,plain,
( ( inverse(sk_c12) = inverse(sk_c11) )
| ( sk_c12 != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_1200]) ).
tcf(c_1203,plain,
! [X0: $i] :
( ( sk_c11 = inverse(sk_c12) )
| ( sk_c11 != X0 )
| ( inverse(sk_c12) != X0 ) ),
inference(instantiation,[status(thm)],[c_832]) ).
tcf(c_1204,plain,
( ( sk_c11 = inverse(sk_c12) )
| ( sk_c11 != sk_c11 )
| ( inverse(sk_c12) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_1203]) ).
tcf(c_1206,plain,
! [X0: $i,X1: $i] :
( ( sk_c11 = inverse(X0) )
| ( sk_c11 != X1 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_832]) ).
tcf(c_1209,plain,
! [X0: $i,X1: $i] :
( ( sk_c12 = X0 )
| ( sk_c12 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_832]) ).
tcf(c_1224,plain,
! [X0: $i,X1: $i] :
( ( X1 = inverse(sk_c12) )
| ( X1 != X0 )
| ( inverse(sk_c12) != X0 ) ),
inference(instantiation,[status(thm)],[c_832]) ).
tcf(c_1226,plain,
! [X0: $i] :
( ( inverse(X0) = inverse(sk_c12) )
| ( X0 != sk_c12 ) ),
inference(instantiation,[status(thm)],[c_833]) ).
tcf(c_1236,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( inverse(X0) = X2 )
| ( X2 != X1 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_832]) ).
tcf(c_1239,plain,
! [X0: $i] :
( ( sk_c12 = X0 )
| ( sk_c12 != sk_c12 )
| ( X0 != sk_c12 ) ),
inference(instantiation,[status(thm)],[c_1209]) ).
tcf(c_1240,plain,
sk_c12 = sk_c12,
inference(instantiation,[status(thm)],[c_831]) ).
tcf(c_1259,plain,
( ( inverse(inverse(sk_c4)) = inverse(sk_c12) )
| ( inverse(sk_c4) != sk_c12 ) ),
inference(instantiation,[status(thm)],[c_1226]) ).
tcf(c_1263,plain,
multiply(identity,sk_c12) = sk_c12,
inference(instantiation,[status(thm)],[c_123]) ).
tcf(c_1265,plain,
! [X0: $i,X1: $i] :
( ( X0 = sk_c12 )
| ( sk_c12 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_832]) ).
tcf(c_1266,plain,
( ( sk_c11 = sk_c12 )
| ( sk_c11 != sk_c11 )
| ( sk_c12 != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_1265]) ).
tcf(c_1268,plain,
( ( sk_c12 = inverse(sk_c4) )
| ( sk_c12 != sk_c12 )
| ( inverse(sk_c4) != sk_c12 ) ),
inference(instantiation,[status(thm)],[c_1239]) ).
tcf(c_1295,plain,
! [X0: $i] :
( ( inverse(sk_c4) = X0 )
| ( X0 != sk_c12 )
| ( inverse(sk_c4) != sk_c12 ) ),
inference(instantiation,[status(thm)],[c_1236]) ).
tcf(c_1297,plain,
! [X0: $i] :
( ( inverse(sk_c5) = X0 )
| ( X0 != sk_c11 )
| ( inverse(sk_c5) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_1236]) ).
tcf(c_1304,plain,
! [X0: $i,X1: $i] :
( ( inverse(X0) = X1 )
| ( X1 != inverse(X0) )
| ( inverse(X0) != inverse(X0) ) ),
inference(instantiation,[status(thm)],[c_1236]) ).
tcf(c_1305,plain,
! [X0: $i] : inverse(X0) = inverse(X0),
inference(instantiation,[status(thm)],[c_831]) ).
tcf(c_1309,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( inverse(X0) = X2 )
| ( X2 != inverse(X1) )
| ( inverse(X0) != inverse(X1) ) ),
inference(instantiation,[status(thm)],[c_1236]) ).
tcf(c_1355,plain,
! [X0: $i] :
( ( sk_c12 = X0 )
| ( sk_c12 != multiply(sk_c6,sk_c9) )
| ( X0 != multiply(sk_c6,sk_c9) ) ),
inference(instantiation,[status(thm)],[c_1209]) ).
tcf(c_1356,plain,
( ( sk_c12 = sk_c11 )
| ( sk_c11 != multiply(sk_c6,sk_c9) )
| ( sk_c12 != multiply(sk_c6,sk_c9) ) ),
inference(instantiation,[status(thm)],[c_1355]) ).
tcf(c_1388,plain,
( ( inverse(sk_c5) = sk_c12 )
| ( sk_c12 != sk_c11 )
| ( inverse(sk_c5) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_1297]) ).
tcf(c_1389,plain,
( ( sk_c12 = inverse(sk_c5) )
| ( sk_c12 != sk_c12 )
| ( inverse(sk_c5) != sk_c12 ) ),
inference(instantiation,[status(thm)],[c_1239]) ).
tcf(c_1498,plain,
! [X0: $i] :
( ( inverse(sk_c6) = sk_c9 )
| ( multiply(sk_c2,multiply(sk_c3,X0)) = multiply(sk_c11,X0) ) ),
inference(superposition,[status(thm)],[c_171,c_125]) ).
tcf(c_1499,plain,
! [X0: $i] :
( ( inverse(sk_c5) = sk_c11 )
| ( multiply(sk_c2,multiply(sk_c3,X0)) = multiply(sk_c11,X0) ) ),
inference(superposition,[status(thm)],[c_169,c_125]) ).
tcf(c_1500,plain,
! [X0: $i] :
( ( inverse(sk_c4) = sk_c12 )
| ( multiply(sk_c2,multiply(sk_c3,X0)) = multiply(sk_c11,X0) ) ),
inference(superposition,[status(thm)],[c_167,c_125]) ).
tcf(c_1507,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(X0,X1)) = multiply(identity,X1),
inference(superposition,[status(thm)],[c_124,c_125]) ).
tcf(c_1586,plain,
! [X0: $i] :
( ( inverse(sk_c12) = X0 )
| ( X0 != sk_c11 )
| ( inverse(sk_c12) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_1236]) ).
tcf(c_1596,plain,
! [X0: $i] :
( ( inverse(sk_c1) = X0 )
| ( X0 != sk_c12 )
| ( inverse(sk_c1) != sk_c12 ) ),
inference(instantiation,[status(thm)],[c_1236]) ).
tcf(c_1620,plain,
! [X0: $i,X1: $i] :
( ( multiply(X0,sk_c12) = sk_c11 )
| ( sk_c11 != X1 )
| ( multiply(X0,sk_c12) != X1 ) ),
inference(instantiation,[status(thm)],[c_832]) ).
tcf(c_1657,plain,
! [X0: $i] :
( ( inverse(X0) = inverse(sk_c5) )
| ( X0 != sk_c5 ) ),
inference(instantiation,[status(thm)],[c_833]) ).
tcf(c_1675,plain,
! [X0: $i] :
( ( inverse(sk_c12) = sk_c12 )
| ( sk_c12 != X0 )
| ( inverse(sk_c12) != X0 ) ),
inference(instantiation,[status(thm)],[c_1198]) ).
tcf(c_1679,plain,
( ( inverse(sk_c12) = sk_c12 )
| ( sk_c12 != sk_c11 )
| ( inverse(sk_c12) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_1675]) ).
tcf(c_1746,plain,
! [X0: $i] :
( ( multiply(sk_c2,sk_c3) = sk_c11 )
| ( multiply(sk_c4,multiply(sk_c12,X0)) = multiply(sk_c11,X0) ) ),
inference(superposition,[status(thm)],[c_166,c_125]) ).
tcf(c_1769,plain,
! [X0: $i] :
( ( sk_c12 = inverse(sk_c12) )
| ( sk_c12 != X0 )
| ( inverse(sk_c12) != X0 ) ),
inference(instantiation,[status(thm)],[c_1224]) ).
tcf(c_1771,plain,
( ( sk_c12 = inverse(sk_c12) )
| ( sk_c12 != sk_c11 )
| ( inverse(sk_c12) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_1769]) ).
tcf(c_1773,plain,
! [X0: $i,X1: $i] :
( ( inverse(X0) = inverse(sk_c12) )
| ( inverse(sk_c12) != X1 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_1224]) ).
tcf(c_1810,plain,
( ( sk_c12 = multiply(identity,sk_c12) )
| ( sk_c12 != sk_c12 )
| ( multiply(identity,sk_c12) != sk_c12 ) ),
inference(instantiation,[status(thm)],[c_1239]) ).
tcf(c_1849,plain,
( ( inverse(sk_c4) = sk_c12 )
| ( sk_c12 != inverse(sk_c4) )
| ( inverse(sk_c4) != inverse(sk_c4) ) ),
inference(instantiation,[status(thm)],[c_1304]) ).
tcf(c_1850,plain,
( ( inverse(sk_c5) = sk_c11 )
| ( sk_c11 != inverse(sk_c5) )
| ( inverse(sk_c5) != inverse(sk_c5) ) ),
inference(instantiation,[status(thm)],[c_1304]) ).
tcf(c_1852,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = inverse(X0) )
| ( X2 != X1 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_832]) ).
tcf(c_1885,plain,
( ~ iPr_def_10
| ( sk_c11 != identity )
| ( inverse(inverse(sk_c12)) != sk_c12 ) ),
inference(superposition,[status(thm)],[c_124,c_825]) ).
tcf(c_1901,plain,
! [X0: $i] :
( ( inverse(X0) = sk_c11 )
| ( sk_c11 != inverse(sk_c12) )
| ( inverse(X0) != inverse(sk_c12) ) ),
inference(instantiation,[status(thm)],[c_1309]) ).
tcf(c_1902,plain,
( ( inverse(sk_c11) = sk_c11 )
| ( sk_c11 != inverse(sk_c12) )
| ( inverse(sk_c11) != inverse(sk_c12) ) ),
inference(instantiation,[status(thm)],[c_1901]) ).
tcf(c_1906,plain,
! [X0: $i,X1: $i] :
( ( inverse(X0) = X1 )
| ( X1 != inverse(sk_c12) )
| ( inverse(X0) != inverse(sk_c12) ) ),
inference(instantiation,[status(thm)],[c_1309]) ).
tcf(c_2250,plain,
! [X0: $i] :
( ( inverse(sk_c12) = sk_c11 )
| ( multiply(sk_c4,sk_c12) = X0 )
| ( X0 != sk_c11 ) ),
inference(resolution,[status(thm)],[c_832,c_126]) ).
tcf(c_2251,plain,
! [X0: $i] :
( ( inverse(sk_c1) = sk_c12 )
| ( multiply(sk_c4,sk_c12) = X0 )
| ( X0 != sk_c11 ) ),
inference(resolution,[status(thm)],[c_832,c_146]) ).
tcf(c_2252,plain,
! [X0: $i] :
( ( inverse(sk_c2) = sk_c3 )
| ( multiply(sk_c4,sk_c12) = X0 )
| ( X0 != sk_c11 ) ),
inference(resolution,[status(thm)],[c_832,c_176]) ).
tcf(c_2256,plain,
! [X0: $i] :
( ( inverse(sk_c12) = sk_c11 )
| ( multiply(sk_c5,sk_c11) = X0 )
| ( X0 != sk_c10 ) ),
inference(resolution,[status(thm)],[c_832,c_128]) ).
tcf(c_2296,plain,
! [X0: $i] :
( ( inverse(sk_c5) = sk_c11 )
| ( multiply(sk_c11,sk_c10) = X0 )
| ( X0 != sk_c12 ) ),
inference(resolution,[status(thm)],[c_832,c_139]) ).
tcf(c_2305,plain,
! [X0: $i] :
( ( inverse(sk_c1) = X0 )
| ( inverse(sk_c4) = sk_c12 )
| ( X0 != sk_c12 ) ),
inference(resolution,[status(thm)],[c_832,c_147]) ).
tcf(c_2306,plain,
! [X0: $i] :
( ( inverse(sk_c1) = X0 )
| ( inverse(sk_c5) = sk_c11 )
| ( X0 != sk_c12 ) ),
inference(resolution,[status(thm)],[c_832,c_149]) ).
tcf(c_2307,plain,
! [X0: $i] :
( ( inverse(sk_c1) = X0 )
| ( inverse(sk_c6) = sk_c9 )
| ( X0 != sk_c12 ) ),
inference(resolution,[status(thm)],[c_832,c_151]) ).
tcf(c_2365,plain,
! [X0: $i,X1: $i] :
( ( multiply(identity,X1) = X0 )
| ( X0 != X1 ) ),
inference(resolution,[status(thm)],[c_832,c_123]) ).
tcf(c_2366,plain,
! [X0: $i,X1: $i] :
( ( multiply(inverse(X1),X1) = X0 )
| ( X0 != identity ) ),
inference(resolution,[status(thm)],[c_832,c_124]) ).
tcf(c_2370,plain,
! [X0: $i,X1: $i] :
( ( X1 = X0 )
| ( X0 != X1 ) ),
inference(resolution,[status(thm)],[c_832,c_831]) ).
tcf(c_2371,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( inverse(X0) = X2 )
| ( X2 != inverse(X1) )
| ( X0 != X1 ) ),
inference(resolution,[status(thm)],[c_832,c_833]) ).
tcf(c_2546,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(X0,X1)) = X1,
inference(demodulation,[status(thm)],[c_1507,c_123]) ).
tcf(c_2562,plain,
( ( inverse(sk_c12) = sk_c11 )
| ( multiply(inverse(sk_c4),sk_c11) = sk_c12 ) ),
inference(superposition,[status(thm)],[c_126,c_2546]) ).
tcf(c_2567,plain,
( ( inverse(sk_c5) = sk_c11 )
| ( multiply(inverse(sk_c11),sk_c12) = sk_c10 ) ),
inference(superposition,[status(thm)],[c_139,c_2546]) ).
tcf(c_2568,plain,
( ( inverse(sk_c4) = sk_c12 )
| ( multiply(inverse(sk_c11),sk_c12) = sk_c10 ) ),
inference(superposition,[status(thm)],[c_137,c_2546]) ).
tcf(c_2569,plain,
! [X0: $i] : multiply(inverse(identity),X0) = X0,
inference(superposition,[status(thm)],[c_123,c_2546]) ).
tcf(c_2570,plain,
! [X0: $i] : multiply(inverse(inverse(X0)),identity) = X0,
inference(superposition,[status(thm)],[c_124,c_2546]) ).
tcf(c_2578,plain,
! [X0: $i,X1: $i] : multiply(inverse(inverse(X0)),X1) = multiply(X0,X1),
inference(superposition,[status(thm)],[c_2546,c_2546]) ).
tcf(c_2602,plain,
( ( multiply(inverse(sk_c12),sk_c12) = sk_c11 )
| ( sk_c11 != identity )
| ( multiply(inverse(sk_c12),sk_c12) != identity ) ),
inference(instantiation,[status(thm)],[c_1620]) ).
tcf(c_2603,plain,
multiply(inverse(sk_c12),sk_c12) = identity,
inference(instantiation,[status(thm)],[c_124]) ).
tcf(c_2612,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(X0,sk_c12) = X2 )
| ( X2 != X1 )
| ( multiply(X0,sk_c12) != X1 ) ),
inference(instantiation,[status(thm)],[c_832]) ).
tcf(c_2613,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(X0,sk_c12) = sk_c11 )
| ( sk_c11 != multiply(X1,X2) )
| ( multiply(X0,sk_c12) != multiply(X1,X2) ) ),
inference(instantiation,[status(thm)],[c_1620]) ).
tcf(c_2614,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(X0,sk_c12) = multiply(X1,X2) )
| ( sk_c12 != X2 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_834]) ).
tcf(c_2615,plain,
( ( multiply(sk_c11,sk_c12) = sk_c11 )
| ( sk_c11 != multiply(sk_c11,sk_c11) )
| ( multiply(sk_c11,sk_c12) != multiply(sk_c11,sk_c11) ) ),
inference(instantiation,[status(thm)],[c_2613]) ).
tcf(c_2616,plain,
( ( multiply(sk_c11,sk_c12) = multiply(sk_c11,sk_c11) )
| ( sk_c11 != sk_c11 )
| ( sk_c12 != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_2614]) ).
tcf(c_2758,plain,
! [X0: $i,X1: $i] :
( ( X1 = multiply(sk_c6,sk_c9) )
| ( X1 != X0 )
| ( multiply(sk_c6,sk_c9) != X0 ) ),
inference(instantiation,[status(thm)],[c_832]) ).
tcf(c_2760,plain,
! [X0: $i,X1: $i] :
( ( sk_c12 = multiply(X0,X1) )
| ( sk_c12 != multiply(sk_c6,sk_c9) )
| ( multiply(X0,X1) != multiply(sk_c6,sk_c9) ) ),
inference(instantiation,[status(thm)],[c_1355]) ).
tcf(c_2788,plain,
( ( inverse(sk_c6) = sk_c9 )
| ( multiply(inverse(sk_c11),sk_c12) = sk_c10 ) ),
inference(superposition,[status(thm)],[c_141,c_2546]) ).
tcf(c_2797,plain,
( ( inverse(sk_c1) = sk_c12 )
| ( multiply(inverse(sk_c4),sk_c11) = sk_c12 ) ),
inference(superposition,[status(thm)],[c_146,c_2546]) ).
tcf(c_2800,plain,
( ( inverse(sk_c1) = sk_c12 )
| ( multiply(inverse(sk_c5),sk_c10) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_148,c_2546]) ).
tcf(c_2805,plain,
! [X0: $i] :
( ( inverse(sk_c4) = inverse(X0) )
| ( sk_c4 != X0 ) ),
inference(instantiation,[status(thm)],[c_833]) ).
tcf(c_2814,plain,
( ( inverse(sk_c1) = sk_c12 )
| ( multiply(inverse(sk_c6),sk_c12) = sk_c9 ) ),
inference(superposition,[status(thm)],[c_150,c_2546]) ).
tcf(c_2856,plain,
( ( inverse(sk_c5) = sk_c11 )
| ( multiply(inverse(sk_c1),sk_c12) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_159,c_2546]) ).
tcf(c_2859,plain,
( ( inverse(sk_c6) = sk_c9 )
| ( multiply(inverse(sk_c1),sk_c12) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_161,c_2546]) ).
tcf(c_2907,plain,
inverse(sk_c4) = inverse(sk_c4),
inference(instantiation,[status(thm)],[c_1305]) ).
tcf(c_2967,plain,
( ( inverse(sk_c4) = sk_c12 )
| ( multiply(inverse(sk_c2),sk_c11) = sk_c3 ) ),
inference(superposition,[status(thm)],[c_167,c_2546]) ).
tcf(c_2970,plain,
( ( inverse(sk_c5) = sk_c11 )
| ( multiply(inverse(sk_c2),sk_c11) = sk_c3 ) ),
inference(superposition,[status(thm)],[c_169,c_2546]) ).
tcf(c_2973,plain,
( ( inverse(sk_c6) = sk_c9 )
| ( multiply(inverse(sk_c2),sk_c11) = sk_c3 ) ),
inference(superposition,[status(thm)],[c_171,c_2546]) ).
tcf(c_2982,plain,
( ( inverse(sk_c2) = sk_c3 )
| ( multiply(inverse(sk_c4),sk_c11) = sk_c12 ) ),
inference(superposition,[status(thm)],[c_176,c_2546]) ).
tcf(c_2985,plain,
( ( inverse(sk_c2) = sk_c3 )
| ( multiply(inverse(sk_c5),sk_c10) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_178,c_2546]) ).
tcf(c_3001,plain,
inverse(sk_c6) = inverse(sk_c6),
inference(instantiation,[status(thm)],[c_1305]) ).
tcf(c_3069,plain,
( ~ iPr_def_11
| ( inverse(sk_c1) != sk_c12 )
| ( multiply(sk_c1,sk_c11) != sk_c12 ) ),
inference(instantiation,[status(thm)],[c_826]) ).
tcf(c_3094,plain,
( ( multiply(sk_c11,sk_c10) = sk_c12 )
| ( multiply(inverse(sk_c5),sk_c10) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_138,c_2546]) ).
tcf(c_3171,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(inverse(multiply(X0,X1)),multiply(X0,multiply(X1,X2))) = X2,
inference(superposition,[status(thm)],[c_125,c_2546]) ).
tcf(c_3235,plain,
( ( multiply(sk_c1,sk_c11) = sk_c12 )
| ( multiply(inverse(sk_c4),sk_c11) = sk_c12 ) ),
inference(superposition,[status(thm)],[c_156,c_2546]) ).
tcf(c_3242,plain,
( ( inverse(sk_c5) = inverse(sk_c5) )
| ( sk_c5 != sk_c5 ) ),
inference(instantiation,[status(thm)],[c_1657]) ).
tcf(c_3243,plain,
sk_c5 = sk_c5,
inference(instantiation,[status(thm)],[c_831]) ).
tcf(c_3283,plain,
( ( multiply(sk_c2,sk_c3) = sk_c11 )
| ( multiply(inverse(sk_c4),sk_c11) = sk_c12 ) ),
inference(superposition,[status(thm)],[c_166,c_2546]) ).
tcf(c_3297,plain,
( ( multiply(sk_c2,sk_c3) = sk_c11 )
| ( multiply(inverse(sk_c5),sk_c10) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_168,c_2546]) ).
tcf(c_3445,plain,
( ( inverse(sk_c2) = sk_c3 )
| ~ iPr_def_11
| ( inverse(sk_c9) != sk_c12 ) ),
inference(superposition,[status(thm)],[c_182,c_826]) ).
tcf(c_3446,plain,
( ( inverse(sk_c1) = sk_c12 )
| ~ iPr_def_11
| ( inverse(sk_c9) != sk_c12 ) ),
inference(superposition,[status(thm)],[c_152,c_826]) ).
tcf(c_3451,plain,
( ( inverse(sk_c6) = sk_c9 )
| ~ iPr_def_11
| ( inverse(sk_c1) != sk_c12 ) ),
inference(superposition,[status(thm)],[c_161,c_826]) ).
tcf(c_3452,plain,
( ( inverse(sk_c5) = sk_c11 )
| ~ iPr_def_11
| ( inverse(sk_c1) != sk_c12 ) ),
inference(superposition,[status(thm)],[c_159,c_826]) ).
tcf(c_3453,plain,
( ( inverse(sk_c4) = sk_c12 )
| ~ iPr_def_11
| ( inverse(sk_c1) != sk_c12 ) ),
inference(superposition,[status(thm)],[c_157,c_826]) ).
tcf(c_3454,plain,
( ~ iPr_def_11
| ( sk_c12 != sk_c11 )
| ( inverse(identity) != sk_c12 ) ),
inference(superposition,[status(thm)],[c_123,c_826]) ).
tcf(c_3514,plain,
! [X0: $i,X1: $i] :
( ( X0 = identity )
| ( identity != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_832]) ).
tcf(c_3564,plain,
( ( inverse(sk_c2) = sk_c3 )
| ~ iPr_def_12
| ( inverse(sk_c5) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_178,c_827]) ).
tcf(c_3565,plain,
( ( inverse(sk_c1) = sk_c12 )
| ~ iPr_def_12
| ( inverse(sk_c5) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_148,c_827]) ).
tcf(c_3578,plain,
( ~ iPr_def_12
| ( sk_c10 != identity )
| ( inverse(inverse(sk_c11)) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_124,c_827]) ).
tcf(c_3589,plain,
! [X0: $i] :
( ( inverse(inverse(sk_c4)) = X0 )
| ( X0 != inverse(sk_c12) )
| ( inverse(inverse(sk_c4)) != inverse(sk_c12) ) ),
inference(instantiation,[status(thm)],[c_1906]) ).
tcf(c_3647,plain,
! [X0: $i] :
( ( X0 = inverse(sk_c12) )
| ( X0 != sk_c11 )
| ( inverse(sk_c12) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_1852]) ).
tcf(c_3653,plain,
! [X0: $i] :
( ( X0 = inverse(sk_c1) )
| ( X0 != sk_c12 )
| ( inverse(sk_c1) != sk_c12 ) ),
inference(instantiation,[status(thm)],[c_1852]) ).
tcf(c_3700,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( ( multiply(X0,X2) = X4 )
| ( X4 != multiply(X1,X3) )
| ( X2 != X3 )
| ( X0 != X1 ) ),
inference(resolution,[status(thm)],[c_834,c_832]) ).
tcf(c_3716,plain,
( ( sk_c12 = multiply(sk_c6,sk_c9) )
| ( inverse(sk_c12) = sk_c11 ) ),
inference(resolution,[status(thm)],[c_2370,c_130]) ).
tcf(c_3717,plain,
( ( sk_c12 = multiply(sk_c6,sk_c9) )
| ( inverse(sk_c1) = sk_c12 ) ),
inference(resolution,[status(thm)],[c_2370,c_150]) ).
tcf(c_3718,plain,
( ( sk_c12 = multiply(sk_c6,sk_c9) )
| ( inverse(sk_c2) = sk_c3 ) ),
inference(resolution,[status(thm)],[c_2370,c_180]) ).
tcf(c_3741,plain,
( ( sk_c12 = multiply(sk_c1,sk_c11) )
| ( inverse(sk_c4) = sk_c12 ) ),
inference(resolution,[status(thm)],[c_2370,c_157]) ).
tcf(c_3742,plain,
( ( sk_c12 = multiply(sk_c1,sk_c11) )
| ( inverse(sk_c5) = sk_c11 ) ),
inference(resolution,[status(thm)],[c_2370,c_159]) ).
tcf(c_3743,plain,
( ( sk_c12 = multiply(sk_c1,sk_c11) )
| ( inverse(sk_c6) = sk_c9 ) ),
inference(resolution,[status(thm)],[c_2370,c_161]) ).
tcf(c_3751,plain,
( ( sk_c11 = multiply(sk_c2,sk_c3) )
| ( inverse(sk_c4) = sk_c12 ) ),
inference(resolution,[status(thm)],[c_2370,c_167]) ).
tcf(c_3752,plain,
( ( sk_c11 = multiply(sk_c2,sk_c3) )
| ( inverse(sk_c5) = sk_c11 ) ),
inference(resolution,[status(thm)],[c_2370,c_169]) ).
tcf(c_3753,plain,
( ( sk_c11 = multiply(sk_c2,sk_c3) )
| ( inverse(sk_c6) = sk_c9 ) ),
inference(resolution,[status(thm)],[c_2370,c_171]) ).
tcf(c_3756,plain,
( ( sk_c11 = multiply(sk_c2,sk_c3) )
| ( multiply(sk_c4,sk_c12) = sk_c11 ) ),
inference(resolution,[status(thm)],[c_2370,c_166]) ).
tcf(c_3776,plain,
! [X0: $i] : X0 = multiply(identity,X0),
inference(resolution,[status(thm)],[c_2370,c_123]) ).
tcf(c_3778,plain,
! [X0: $i] : identity = multiply(inverse(X0),X0),
inference(resolution,[status(thm)],[c_2370,c_124]) ).
tcf(c_4022,plain,
! [X0: $i] : multiply(X0,inverse(X0)) = identity,
inference(superposition,[status(thm)],[c_2578,c_124]) ).
tcf(c_4023,plain,
multiply(sk_c11,inverse(sk_c11)) = identity,
inference(instantiation,[status(thm)],[c_4022]) ).
tcf(c_4288,plain,
( ( inverse(sk_c12) = sk_c11 )
| ( multiply(sk_c12,sk_c11) = sk_c12 ) ),
inference(superposition,[status(thm)],[c_127,c_2562]) ).
tcf(c_4484,plain,
! [X0: $i] :
( ~ iPr_def_13
| ( sk_c11 != identity )
| ( multiply(inverse(X0),sk_c12) != sk_c11 ) ),
inference(light_normalisation,[status(thm)],[c_828,c_4022]) ).
tcf(c_4491,plain,
( ~ iPr_def_13
| ( sk_c11 != identity ) ),
inference(superposition,[status(thm)],[c_124,c_4484]) ).
tcf(c_4514,plain,
( ( multiply(sk_c11,sk_c10) = inverse(sk_c1) )
| ( inverse(sk_c1) != sk_c12 )
| ( multiply(sk_c11,sk_c10) != sk_c12 ) ),
inference(instantiation,[status(thm)],[c_3653]) ).
tcf(c_4563,plain,
! [X0: $i] :
( ~ iPr_def_14
| ( inverse(X0) != inverse(identity) )
| ( inverse(inverse(identity)) != inverse(X0) )
| ( multiply(inverse(X0),sk_c11) != sk_c12 )
| ( multiply(X0,inverse(X0)) != sk_c12 ) ),
inference(superposition,[status(thm)],[c_123,c_829]) ).
tcf(c_4583,plain,
( ~ iPr_def_14
| ( inverse(sk_c11) != inverse(identity) )
| ( inverse(inverse(identity)) != inverse(sk_c11) )
| ( multiply(sk_c11,inverse(sk_c11)) != sk_c12 )
| ( multiply(inverse(sk_c11),sk_c11) != sk_c12 ) ),
inference(instantiation,[status(thm)],[c_4563]) ).
tcf(c_4670,plain,
! [X0: $i] :
( ( multiply(inverse(sk_c12),sk_c12) = X0 )
| ( X0 != identity )
| ( multiply(inverse(sk_c12),sk_c12) != identity ) ),
inference(instantiation,[status(thm)],[c_2612]) ).
tcf(c_4745,plain,
( ( inverse(sk_c2) = sk_c3 )
| ( multiply(sk_c4,sk_c12) = identity ) ),
inference(superposition,[status(thm)],[c_177,c_4022]) ).
tcf(c_4746,plain,
( ( inverse(sk_c1) = sk_c12 )
| ( multiply(sk_c4,sk_c12) = identity ) ),
inference(superposition,[status(thm)],[c_147,c_4022]) ).
tcf(c_4747,plain,
( ( inverse(sk_c12) = sk_c11 )
| ( multiply(sk_c4,sk_c12) = identity ) ),
inference(superposition,[status(thm)],[c_127,c_4022]) ).
tcf(c_4750,plain,
( ( inverse(sk_c12) = sk_c11 )
| ( multiply(sk_c5,sk_c11) = identity ) ),
inference(superposition,[status(thm)],[c_129,c_4022]) ).
tcf(c_4751,plain,
( ( inverse(sk_c2) = sk_c3 )
| ( multiply(sk_c6,sk_c9) = identity ) ),
inference(superposition,[status(thm)],[c_181,c_4022]) ).
tcf(c_4752,plain,
( ( inverse(sk_c1) = sk_c12 )
| ( multiply(sk_c6,sk_c9) = identity ) ),
inference(superposition,[status(thm)],[c_151,c_4022]) ).
tcf(c_4753,plain,
( ( inverse(sk_c12) = sk_c11 )
| ( multiply(sk_c6,sk_c9) = identity ) ),
inference(superposition,[status(thm)],[c_131,c_4022]) ).
tcf(c_4761,plain,
inverse(identity) = identity,
inference(superposition,[status(thm)],[c_4022,c_123]) ).
tcf(c_4791,plain,
! [X0: $i,X1: $i] :
( ( multiply(X0,sk_c12) = multiply(X1,sk_c12) )
| ( sk_c12 != sk_c12 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_2614]) ).
tcf(c_4800,plain,
! [X0: $i,X1: $i] :
( ( sk_c11 = multiply(X0,sk_c12) )
| ( sk_c11 != X1 )
| ( multiply(X0,sk_c12) != X1 ) ),
inference(instantiation,[status(thm)],[c_832]) ).
tcf(c_4801,plain,
( ( sk_c11 = multiply(sk_c11,sk_c12) )
| ( sk_c11 != sk_c11 )
| ( multiply(sk_c11,sk_c12) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_4800]) ).
tcf(c_4953,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(X0,X1)) = X1,
inference(demodulation,[status(thm)],[c_1507,c_123]) ).
tcf(c_5049,plain,
( ( inverse(sk_c12) = sk_c11 )
| ( multiply(inverse(sk_c12),sk_c12) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_4288,c_4953]) ).
tcf(c_5091,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( sk_c11 = multiply(X0,X1) )
| ( sk_c11 != X2 )
| ( multiply(X0,X1) != X2 ) ),
inference(instantiation,[status(thm)],[c_832]) ).
tcf(c_5092,plain,
( ( sk_c11 = multiply(sk_c11,sk_c11) )
| ( sk_c11 != sk_c11 )
| ( multiply(sk_c11,sk_c11) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_5091]) ).
tcf(c_5136,plain,
( ( sk_c11 = identity )
| ( inverse(sk_c2) = sk_c3 ) ),
inference(superposition,[status(thm)],[c_4745,c_176]) ).
tcf(c_5150,plain,
( ( sk_c11 = identity )
| ( multiply(sk_c2,sk_c3) = identity ) ),
inference(superposition,[status(thm)],[c_5136,c_4022]) ).
tcf(c_5221,plain,
( ( sk_c11 = identity )
| ( inverse(sk_c1) = sk_c12 ) ),
inference(superposition,[status(thm)],[c_4746,c_146]) ).
tcf(c_5257,plain,
! [X0: $i,X1: $i] :
( ( X1 = multiply(sk_c11,sk_c10) )
| ( X1 != X0 )
| ( multiply(sk_c11,sk_c10) != X0 ) ),
inference(instantiation,[status(thm)],[c_832]) ).
tcf(c_5284,plain,
( ( sk_c11 = identity )
| ( inverse(sk_c12) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_4747,c_126]) ).
tcf(c_5297,plain,
( ( sk_c11 = identity )
| ( multiply(sk_c11,sk_c12) = identity ) ),
inference(superposition,[status(thm)],[c_5284,c_124]) ).
tcf(c_5413,plain,
multiply(sk_c6,sk_c9) = multiply(sk_c6,sk_c9),
inference(instantiation,[status(thm)],[c_831]) ).
tcf(c_5464,plain,
! [X0: $i,X1: $i] :
( ( X0 = multiply(inverse(X1),X1) )
| ( X0 != identity ) ),
inference(resolution,[status(thm)],[c_2366,c_2370]) ).
tcf(c_5465,plain,
( ( sk_c11 = multiply(inverse(sk_c11),sk_c11) )
| ( sk_c11 != identity ) ),
inference(instantiation,[status(thm)],[c_5464]) ).
tcf(c_5667,plain,
( ( inverse(inverse(sk_c4)) = sk_c12 )
| ( sk_c12 != inverse(sk_c12) )
| ( inverse(inverse(sk_c4)) != inverse(sk_c12) ) ),
inference(instantiation,[status(thm)],[c_3589]) ).
tcf(c_5749,plain,
( ( inverse(sk_c12) = sk_c11 )
| ~ iPr_def_11
| ( sk_c12 != identity )
| ( inverse(sk_c5) != sk_c12 ) ),
inference(superposition,[status(thm)],[c_4750,c_826]) ).
tcf(c_5777,plain,
( ( sk_c12 = identity )
| ( inverse(sk_c2) = sk_c3 ) ),
inference(superposition,[status(thm)],[c_4751,c_180]) ).
tcf(c_5818,plain,
( ( sk_c12 = identity )
| ( inverse(sk_c1) = sk_c12 ) ),
inference(superposition,[status(thm)],[c_4752,c_150]) ).
tcf(c_5854,plain,
( iPr_def_14
| iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( inverse(sk_c5) = sk_c11 )
| ( inverse(sk_c12) != sk_c11 ) ),
inference(resolution,[status(thm)],[c_830,c_139]) ).
tcf(c_5855,plain,
( iPr_def_14
| iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( inverse(sk_c6) = sk_c9 )
| ( inverse(sk_c12) != sk_c11 ) ),
inference(resolution,[status(thm)],[c_830,c_141]) ).
tcf(c_5931,plain,
( ( sk_c12 = identity )
| ( inverse(sk_c12) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_4753,c_130]) ).
tcf(c_5943,plain,
( ( sk_c12 = identity )
| ( multiply(sk_c11,sk_c12) = identity ) ),
inference(superposition,[status(thm)],[c_5931,c_124]) ).
tcf(c_5978,plain,
! [X0: $i] :
( ~ iPr_def_14
| ( inverse(identity) != inverse(X0) )
| ( inverse(inverse(identity)) != inverse(X0) )
| ( multiply(inverse(X0),sk_c11) != sk_c12 )
| ( multiply(X0,inverse(X0)) != sk_c12 ) ),
inference(resolution,[status(thm)],[c_829,c_2365]) ).
tcf(c_5984,plain,
( ( inverse(sk_c1) = sk_c12 )
| ( multiply(sk_c12,sk_c11) = sk_c12 ) ),
inference(superposition,[status(thm)],[c_147,c_2797]) ).
tcf(c_6001,plain,
( ( inverse(sk_c4) = sk_c12 )
| ~ iPr_def_11
| ( inverse(sk_c1) != sk_c12 ) ),
inference(resolution,[status(thm)],[c_826,c_157]) ).
tcf(c_6002,plain,
( ( inverse(sk_c5) = sk_c11 )
| ~ iPr_def_11
| ( inverse(sk_c1) != sk_c12 ) ),
inference(resolution,[status(thm)],[c_826,c_159]) ).
tcf(c_6003,plain,
( ( inverse(sk_c6) = sk_c9 )
| ~ iPr_def_11
| ( inverse(sk_c1) != sk_c12 ) ),
inference(resolution,[status(thm)],[c_826,c_161]) ).
tcf(c_6008,plain,
( ( multiply(sk_c6,sk_c9) = sk_c12 )
| ~ iPr_def_11
| ( inverse(sk_c1) != sk_c12 ) ),
inference(resolution,[status(thm)],[c_826,c_160]) ).
tcf(c_6153,plain,
( ( inverse(sk_c1) = sk_c12 )
| ~ iPr_def_11
| ( inverse(sk_c12) != sk_c12 ) ),
inference(superposition,[status(thm)],[c_5984,c_826]) ).
tcf(c_6920,plain,
! [X0: $i] :
( ( X0 = inverse(sk_c1) )
| ( inverse(sk_c4) = sk_c12 )
| ( X0 != sk_c12 ) ),
inference(resolution,[status(thm)],[c_2305,c_2370]) ).
tcf(c_6984,plain,
! [X0: $i] :
( ( X0 = inverse(sk_c1) )
| ( inverse(sk_c5) = sk_c11 )
| ( X0 != sk_c12 ) ),
inference(resolution,[status(thm)],[c_2306,c_2370]) ).
tcf(c_6999,plain,
! [X0: $i] :
( ( X0 = inverse(sk_c1) )
| ( inverse(sk_c6) = sk_c9 )
| ( X0 != sk_c12 ) ),
inference(resolution,[status(thm)],[c_2307,c_2370]) ).
tcf(c_7696,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(X0,X1)) = X1,
inference(demodulation,[status(thm)],[c_1507,c_123]) ).
tcf(c_7930,plain,
( ( inverse(sk_c1) = sk_c12 )
| ( multiply(sk_c12,sk_c11) = sk_c12 ) ),
inference(superposition,[status(thm)],[c_147,c_2797]) ).
tcf(c_7940,plain,
( ( inverse(sk_c1) = sk_c12 )
| ( multiply(inverse(sk_c12),sk_c12) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_7930,c_7696]) ).
tcf(c_7945,plain,
( ( inverse(sk_c1) = sk_c12 )
| ( multiply(sk_c11,sk_c10) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_149,c_2800]) ).
tcf(c_7956,plain,
( iPr_def_14
| iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( inverse(sk_c1) = sk_c12 )
| ( sk_c12 != sk_c11 )
| ( inverse(sk_c12) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_7945,c_830]) ).
tcf(c_8167,plain,
( ( sk_c11 = identity )
| ( inverse(sk_c1) = sk_c12 ) ),
inference(demodulation,[status(thm)],[c_7940,c_124]) ).
tcf(c_8174,plain,
( ( sk_c11 = identity )
| ( inverse(sk_c6) = sk_c9 )
| ( multiply(sk_c12,sk_c12) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_8167,c_2859]) ).
tcf(c_8175,plain,
( ( sk_c11 = identity )
| ( inverse(sk_c5) = sk_c11 )
| ( multiply(sk_c12,sk_c12) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_8167,c_2856]) ).
tcf(c_8206,plain,
( ( inverse(sk_c2) = sk_c3 )
| ( multiply(sk_c11,sk_c10) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_179,c_2985]) ).
tcf(c_8219,plain,
( iPr_def_14
| iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( inverse(sk_c2) = sk_c3 )
| ( sk_c12 != sk_c11 )
| ( inverse(sk_c12) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_8206,c_830]) ).
tcf(c_8779,plain,
( ( multiply(sk_c1,sk_c11) = sk_c12 )
| ~ iPr_def_11
| ( inverse(inverse(sk_c4)) != sk_c12 ) ),
inference(superposition,[status(thm)],[c_3235,c_826]) ).
tcf(c_8846,plain,
( ( inverse(sk_c4) = inverse(inverse(sk_c12)) )
| ( sk_c4 != inverse(sk_c12) ) ),
inference(instantiation,[status(thm)],[c_2805]) ).
tcf(c_8848,plain,
( ( sk_c4 = inverse(sk_c12) )
| ( sk_c4 != sk_c11 )
| ( inverse(sk_c12) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_3647]) ).
tcf(c_9093,plain,
! [X0: $i,X1: $i] : multiply(inverse(multiply(inverse(multiply(X0,X1)),X0)),identity) = X1,
inference(superposition,[status(thm)],[c_124,c_3171]) ).
tcf(c_9175,plain,
! [X0: $i,X1: $i] : multiply(inverse(multiply(X0,identity)),multiply(X0,X1)) = X1,
inference(superposition,[status(thm)],[c_123,c_3171]) ).
tcf(c_10487,plain,
! [X0: $i] :
( ( X0 = multiply(sk_c4,sk_c12) )
| ( inverse(sk_c12) = sk_c11 )
| ( X0 != sk_c11 ) ),
inference(resolution,[status(thm)],[c_2250,c_2370]) ).
tcf(c_10497,plain,
! [X0: $i] :
( ( X0 = multiply(sk_c4,sk_c12) )
| ( inverse(sk_c1) = sk_c12 )
| ( X0 != sk_c11 ) ),
inference(resolution,[status(thm)],[c_2251,c_2370]) ).
tcf(c_10544,plain,
! [X0: $i] :
( ( X0 = multiply(sk_c4,sk_c12) )
| ( inverse(sk_c2) = sk_c3 )
| ( X0 != sk_c11 ) ),
inference(resolution,[status(thm)],[c_2252,c_2370]) ).
tcf(c_10586,plain,
( ( inverse(sk_c12) = sk_c11 )
| ~ iPr_def_11
| ( sk_c12 != sk_c10 )
| ( inverse(sk_c5) != sk_c12 ) ),
inference(resolution,[status(thm)],[c_2256,c_826]) ).
tcf(c_10867,plain,
( ( sk_c11 = multiply(sk_c2,sk_c3) )
| ( sk_c11 = multiply(sk_c4,sk_c12) ) ),
inference(resolution,[status(thm)],[c_3756,c_2370]) ).
tcf(c_10869,plain,
( ( sk_c11 = multiply(sk_c2,sk_c3) )
| ~ iPr_def_10
| ( inverse(sk_c4) != sk_c12 ) ),
inference(resolution,[status(thm)],[c_3756,c_825]) ).
tcf(c_11570,plain,
( ( inverse(sk_c4) = sk_c12 )
| ~ iPr_def_11 ),
inference(global_subsumption_just,[status(thm)],[c_6001,c_147,c_3453]) ).
tcf(c_11584,plain,
( ( inverse(sk_c5) = sk_c11 )
| ~ iPr_def_11 ),
inference(global_subsumption_just,[status(thm)],[c_6002,c_149,c_3452]) ).
tcf(c_11593,plain,
( iPr_def_14
| iPr_def_13
| iPr_def_12
| iPr_def_10
| ( inverse(sk_c5) = sk_c11 )
| ( inverse(sk_c12) != sk_c11 ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_5854,c_11584]) ).
tcf(c_11595,plain,
( ( sk_c11 = inverse(sk_c5) )
| ~ iPr_def_11 ),
inference(resolution,[status(thm)],[c_11584,c_2370]) ).
tcf(c_11597,plain,
( ( inverse(sk_c6) = sk_c9 )
| ~ iPr_def_11 ),
inference(global_subsumption_just,[status(thm)],[c_6003,c_151,c_3451]) ).
tcf(c_11702,plain,
( iPr_def_14
| iPr_def_13
| iPr_def_12
| iPr_def_10
| ( inverse(sk_c6) = sk_c9 )
| ( inverse(sk_c12) != sk_c11 ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_5855,c_11597]) ).
tcf(c_12024,plain,
( ( multiply(sk_c6,sk_c9) = sk_c12 )
| ~ iPr_def_11 ),
inference(global_subsumption_just,[status(thm)],[c_6008,c_150,c_6008]) ).
tcf(c_12034,plain,
( ( sk_c12 = multiply(sk_c6,sk_c9) )
| ~ iPr_def_11 ),
inference(resolution,[status(thm)],[c_12024,c_2370]) ).
tcf(c_12196,plain,
( ( sk_c11 = multiply(sk_c2,sk_c3) )
| ~ iPr_def_10 ),
inference(global_subsumption_just,[status(thm)],[c_10869,c_3751,c_10869]) ).
tcf(c_12349,plain,
! [X0: $i] : multiply(inverse(multiply(inverse(X0),identity)),identity) = X0,
inference(superposition,[status(thm)],[c_124,c_9175]) ).
tcf(c_12712,plain,
( ( sk_c11 = multiply(inverse(sk_c12),sk_c12) )
| ( sk_c11 != identity )
| ( multiply(inverse(sk_c12),sk_c12) != identity ) ),
inference(instantiation,[status(thm)],[c_4800]) ).
tcf(c_12745,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( multiply(X0,X1) = X3 )
| ( X3 != X2 )
| ( multiply(X0,X1) != X2 ) ),
inference(instantiation,[status(thm)],[c_832]) ).
tcf(c_12746,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_5091]) ).
tcf(c_12904,plain,
! [X0: $i,X1: $i] :
( ( inverse(sk_c5) = sk_c11 )
| ( inverse(X1) = multiply(sk_c11,sk_c10) )
| ( X1 != X0 )
| ( inverse(X0) != sk_c12 ) ),
inference(resolution,[status(thm)],[c_2371,c_2296]) ).
tcf(c_12911,plain,
( ( inverse(sk_c5) = sk_c11 )
| ( inverse(sk_c11) = multiply(sk_c11,sk_c10) )
| ( sk_c11 != sk_c11 )
| ( inverse(sk_c11) != sk_c12 ) ),
inference(instantiation,[status(thm)],[c_12904]) ).
tcf(c_12972,plain,
( ( multiply(inverse(sk_c12),sk_c12) = sk_c12 )
| ( sk_c12 != identity )
| ( multiply(inverse(sk_c12),sk_c12) != identity ) ),
inference(instantiation,[status(thm)],[c_4670]) ).
tcf(c_12979,plain,
( ( sk_c12 = multiply(inverse(sk_c12),sk_c12) )
| ( sk_c12 != sk_c12 )
| ( multiply(inverse(sk_c12),sk_c12) != sk_c12 ) ),
inference(instantiation,[status(thm)],[c_1239]) ).
tcf(c_12995,plain,
( ( multiply(inverse(sk_c12),sk_c12) = multiply(sk_c6,sk_c9) )
| ( multiply(sk_c6,sk_c9) != identity )
| ( multiply(inverse(sk_c12),sk_c12) != identity ) ),
inference(instantiation,[status(thm)],[c_4670]) ).
tcf(c_13004,plain,
! [X0: $i] :
( ( sk_c11 = multiply(inverse(sk_c12),sk_c12) )
| ( sk_c11 != X0 )
| ( multiply(inverse(sk_c12),sk_c12) != X0 ) ),
inference(instantiation,[status(thm)],[c_4800]) ).
tcf(c_13006,plain,
! [X0: $i,X1: $i] :
( ( multiply(inverse(sk_c12),sk_c12) = X1 )
| ( X1 != X0 )
| ( multiply(inverse(sk_c12),sk_c12) != X0 ) ),
inference(instantiation,[status(thm)],[c_2612]) ).
tcf(c_13009,plain,
( ( sk_c11 = multiply(inverse(sk_c12),sk_c12) )
| ( sk_c11 != sk_c11 )
| ( multiply(inverse(sk_c12),sk_c12) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_13004]) ).
tcf(c_13475,plain,
( ( inverse(sk_c6) = sk_c9 )
| ( sk_c9 != inverse(sk_c6) )
| ( inverse(sk_c6) != inverse(sk_c6) ) ),
inference(instantiation,[status(thm)],[c_1304]) ).
tcf(c_14314,plain,
! [X0: $i] :
( ( sk_c12 = X0 )
| ( sk_c12 != inverse(sk_c5) )
| ( X0 != inverse(sk_c5) ) ),
inference(instantiation,[status(thm)],[c_1209]) ).
tcf(c_14315,plain,
( ( sk_c12 = sk_c11 )
| ( sk_c11 != inverse(sk_c5) )
| ( sk_c12 != inverse(sk_c5) ) ),
inference(instantiation,[status(thm)],[c_14314]) ).
tcf(c_15501,plain,
! [X0: $i,X1: $i] : multiply(inverse(multiply(X0,X1)),X0) = multiply(inverse(X1),identity),
inference(superposition,[status(thm)],[c_9093,c_12349]) ).
tcf(c_16261,plain,
( ( inverse(sk_c12) = sk_c11 )
| ~ iPr_def_11
| ( inverse(sk_c5) != sk_c12 ) ),
inference(global_subsumption_just,[status(thm)],[c_10586,c_1240,c_1259,c_1389,c_1679,c_1771,c_3069,c_5667,c_5749,c_5931,c_6153,c_8779,c_11570,c_11595,c_14315]) ).
tcf(c_16263,plain,
( ( inverse(sk_c5) != sk_c12 )
| ~ iPr_def_11 ),
inference(global_subsumption_just,[status(thm)],[c_16261,c_1240,c_1259,c_1389,c_1679,c_1771,c_3069,c_5667,c_6153,c_8779,c_11570,c_11595,c_14315,c_16261]) ).
tcf(c_16264,plain,
( ~ iPr_def_11
| ( inverse(sk_c5) != sk_c12 ) ),
inference(renaming,[status(thm)],[c_16263]) ).
tcf(c_16647,plain,
! [X0: $i] :
( ( inverse(sk_c12) = multiply(X0,sk_c12) )
| ( inverse(sk_c12) != sk_c11 )
| ( multiply(X0,sk_c12) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_1586]) ).
tcf(c_16941,plain,
! [X0: $i] : multiply(inverse(identity),inverse(X0)) = multiply(inverse(X0),identity),
inference(superposition,[status(thm)],[c_124,c_15501]) ).
tcf(c_17420,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(X0,X1)) = X1,
inference(demodulation,[status(thm)],[c_1507,c_123]) ).
tcf(c_17511,plain,
! [X0: $i] : multiply(inverse(inverse(inverse(X0))),X0) = identity,
inference(superposition,[status(thm)],[c_2570,c_17420]) ).
tcf(c_17547,plain,
inverse(identity) = identity,
inference(superposition,[status(thm)],[c_17511,c_2570]) ).
tcf(c_17624,plain,
! [X0: $i] : multiply(inverse(X0),identity) = multiply(identity,inverse(X0)),
inference(light_normalisation,[status(thm)],[c_16941,c_17547]) ).
tcf(c_17625,plain,
! [X0: $i] : multiply(inverse(X0),identity) = inverse(X0),
inference(demodulation,[status(thm)],[c_17624,c_123]) ).
tcf(c_17626,plain,
! [X0: $i] : inverse(inverse(X0)) = X0,
inference(demodulation,[status(thm)],[c_2570,c_17625]) ).
tcf(c_17628,plain,
( ~ iPr_def_12
| ( sk_c10 != identity ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_3578,c_17626]) ).
tcf(c_17846,plain,
( ( inverse(sk_c1) = sk_c12 )
| ( multiply(sk_c11,sk_c10) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_149,c_2800]) ).
tcf(c_17892,plain,
( ( inverse(sk_c1) = sk_c12 )
| ( multiply(inverse(sk_c11),sk_c11) = sk_c10 ) ),
inference(superposition,[status(thm)],[c_17846,c_17420]) ).
tcf(c_17897,plain,
( ( inverse(sk_c1) = sk_c12 )
| ( multiply(sk_c9,sk_c12) = sk_c9 ) ),
inference(superposition,[status(thm)],[c_151,c_2814]) ).
tcf(c_17904,plain,
( ( inverse(sk_c1) = sk_c12 )
| ( multiply(inverse(sk_c9),sk_c9) = sk_c12 ) ),
inference(superposition,[status(thm)],[c_17897,c_17420]) ).
tcf(c_17962,plain,
( ( sk_c10 = identity )
| ( inverse(sk_c1) = sk_c12 ) ),
inference(demodulation,[status(thm)],[c_17892,c_124]) ).
tcf(c_17969,plain,
( ( sk_c10 = identity )
| ( inverse(sk_c6) = sk_c9 )
| ( multiply(sk_c12,sk_c12) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_17962,c_2859]) ).
tcf(c_17970,plain,
( ( sk_c10 = identity )
| ( inverse(sk_c5) = sk_c11 )
| ( multiply(sk_c12,sk_c12) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_17962,c_2856]) ).
tcf(c_17979,plain,
( ( sk_c12 = identity )
| ( inverse(sk_c1) = sk_c12 ) ),
inference(demodulation,[status(thm)],[c_17904,c_124]) ).
tcf(c_17986,plain,
( ( sk_c12 = identity )
| ( inverse(sk_c6) = sk_c9 )
| ( multiply(sk_c12,sk_c12) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_17979,c_2859]) ).
tcf(c_17987,plain,
( ( sk_c12 = identity )
| ( inverse(sk_c5) = sk_c11 )
| ( multiply(sk_c12,sk_c12) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_17979,c_2856]) ).
tcf(c_18055,plain,
( ( inverse(sk_c2) = sk_c3 )
| ( multiply(sk_c12,sk_c11) = sk_c12 ) ),
inference(superposition,[status(thm)],[c_177,c_2982]) ).
tcf(c_18074,plain,
( ( inverse(sk_c2) = sk_c3 )
| ( multiply(inverse(sk_c12),sk_c12) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_18055,c_17420]) ).
tcf(c_18107,plain,
( ( sk_c11 = identity )
| ( inverse(sk_c2) = sk_c3 ) ),
inference(demodulation,[status(thm)],[c_18074,c_124]) ).
tcf(c_18120,plain,
( ( sk_c11 = identity )
| ~ iPr_def_13
| ( multiply(sk_c2,sk_c3) != sk_c11 )
| ( multiply(inverse(sk_c2),sk_c12) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_18107,c_828]) ).
tcf(c_20089,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = multiply(sk_c11,sk_c10) )
| ( X2 != multiply(X0,X1) )
| ( multiply(sk_c11,sk_c10) != multiply(X0,X1) ) ),
inference(instantiation,[status(thm)],[c_5257]) ).
tcf(c_20091,plain,
( ( sk_c11 = multiply(sk_c11,sk_c10) )
| ( sk_c11 != multiply(sk_c11,sk_c11) )
| ( multiply(sk_c11,sk_c10) != multiply(sk_c11,sk_c11) ) ),
inference(instantiation,[status(thm)],[c_20089]) ).
tcf(c_20208,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( inverse(sk_c5) = sk_c11 )
| ( multiply(X2,X3) = inverse(sk_c1) )
| ( X3 != X1 )
| ( X2 != X0 )
| ( multiply(X0,X1) != sk_c12 ) ),
inference(resolution,[status(thm)],[c_3700,c_2306]) ).
tcf(c_20215,plain,
( ( inverse(sk_c5) = sk_c11 )
| ( multiply(sk_c11,sk_c11) = inverse(sk_c1) )
| ( sk_c11 != sk_c11 )
| ( multiply(sk_c11,sk_c11) != sk_c12 ) ),
inference(instantiation,[status(thm)],[c_20208]) ).
tcf(c_20428,plain,
sk_c10 = sk_c10,
inference(instantiation,[status(thm)],[c_831]) ).
tcf(c_22528,plain,
( ~ iPr_def_11
| ( sk_c12 != sk_c11 ) ),
inference(global_subsumption_just,[status(thm)],[c_3454,c_149,c_1388,c_3452,c_16264]) ).
tcf(c_22852,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(X2,X0) = X1 )
| ( X2 != identity )
| ( X0 != X1 ) ),
inference(resolution,[status(thm)],[c_3776,c_3700]) ).
tcf(c_22853,plain,
( ( multiply(sk_c11,sk_c11) = sk_c11 )
| ( sk_c11 != identity )
| ( sk_c11 != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_22852]) ).
tcf(c_22905,plain,
! [X0: $i,X1: $i] :
( ( identity = X0 )
| ( X0 != multiply(inverse(X1),X1) ) ),
inference(resolution,[status(thm)],[c_3778,c_832]) ).
tcf(c_22906,plain,
( ( identity = sk_c11 )
| ( sk_c11 != multiply(inverse(sk_c11),sk_c11) ) ),
inference(instantiation,[status(thm)],[c_22905]) ).
tcf(c_23453,plain,
( ~ iPr_def_14
| ( sk_c12 != identity )
| ( inverse(identity) != inverse(sk_c11) )
| ( inverse(inverse(identity)) != inverse(sk_c11) )
| ( multiply(sk_c11,inverse(sk_c11)) != sk_c12 ) ),
inference(resolution,[status(thm)],[c_5978,c_2366]) ).
tcf(c_23634,plain,
! [X0: $i] :
( ( multiply(X0,sk_c12) = sk_c11 )
| ( sk_c11 != multiply(sk_c4,sk_c12) )
| ( multiply(X0,sk_c12) != multiply(sk_c4,sk_c12) ) ),
inference(instantiation,[status(thm)],[c_2613]) ).
tcf(c_23635,plain,
( ( multiply(sk_c11,sk_c12) = sk_c11 )
| ( sk_c11 != multiply(sk_c4,sk_c12) )
| ( multiply(sk_c11,sk_c12) != multiply(sk_c4,sk_c12) ) ),
inference(instantiation,[status(thm)],[c_23634]) ).
tcf(c_23827,plain,
! [X0: $i] :
( ( multiply(sk_c11,sk_c10) = X0 )
| ( X0 != inverse(sk_c1) )
| ( multiply(sk_c11,sk_c10) != inverse(sk_c1) ) ),
inference(instantiation,[status(thm)],[c_12745]) ).
tcf(c_25538,plain,
! [X0: $i,X1: $i] :
( ( multiply(inverse(sk_c12),sk_c12) = multiply(X0,X1) )
| ( multiply(X0,X1) != identity )
| ( multiply(inverse(sk_c12),sk_c12) != identity ) ),
inference(instantiation,[status(thm)],[c_4670]) ).
tcf(c_25539,plain,
! [X0: $i,X1: $i] :
( ( multiply(inverse(sk_c12),sk_c12) = sk_c11 )
| ( sk_c11 != multiply(X0,X1) )
| ( multiply(inverse(sk_c12),sk_c12) != multiply(X0,X1) ) ),
inference(instantiation,[status(thm)],[c_2613]) ).
tcf(c_26168,plain,
! [X0: $i] :
( ( multiply(sk_c11,sk_c10) = sk_c12 )
| ( sk_c12 != X0 )
| ( multiply(sk_c11,sk_c10) != X0 ) ),
inference(instantiation,[status(thm)],[c_12745]) ).
tcf(c_26169,plain,
( ( multiply(sk_c11,sk_c10) = sk_c12 )
| ( sk_c12 != sk_c11 )
| ( multiply(sk_c11,sk_c10) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_26168]) ).
tcf(c_26186,plain,
! [X0: $i,X1: $i] :
( ( inverse(sk_c1) = multiply(X0,X1) )
| ( inverse(sk_c1) != sk_c12 )
| ( multiply(X0,X1) != sk_c12 ) ),
inference(instantiation,[status(thm)],[c_1596]) ).
tcf(c_26188,plain,
! [X0: $i,X1: $i] :
( ( sk_c12 = multiply(X0,X1) )
| ( sk_c12 != sk_c12 )
| ( multiply(X0,X1) != sk_c12 ) ),
inference(instantiation,[status(thm)],[c_1239]) ).
tcf(c_26191,plain,
( ( sk_c12 = multiply(sk_c11,sk_c11) )
| ( sk_c12 != sk_c12 )
| ( multiply(sk_c11,sk_c11) != sk_c12 ) ),
inference(instantiation,[status(thm)],[c_26188]) ).
tcf(c_26193,plain,
( ( inverse(sk_c1) = multiply(sk_c11,sk_c11) )
| ( inverse(sk_c1) != sk_c12 )
| ( multiply(sk_c11,sk_c11) != sk_c12 ) ),
inference(instantiation,[status(thm)],[c_26186]) ).
tcf(c_26579,plain,
! [X0: $i] :
( ( inverse(sk_c4) = sk_c12 )
| ~ iPr_def_14
| ( inverse(inverse(sk_c1)) != inverse(X0) )
| ( multiply(sk_c1,inverse(X0)) != sk_c12 )
| ( multiply(inverse(X0),sk_c11) != sk_c12 )
| ( multiply(X0,inverse(X0)) != sk_c12 ) ),
inference(resolution,[status(thm)],[c_6920,c_829]) ).
tcf(c_26635,plain,
! [X0: $i] :
( ( inverse(sk_c5) = sk_c11 )
| ~ iPr_def_14
| ( inverse(inverse(sk_c1)) != inverse(X0) )
| ( multiply(sk_c1,inverse(X0)) != sk_c12 )
| ( multiply(inverse(X0),sk_c11) != sk_c12 )
| ( multiply(X0,inverse(X0)) != sk_c12 ) ),
inference(resolution,[status(thm)],[c_6984,c_829]) ).
tcf(c_27266,plain,
! [X0: $i] :
( ( inverse(sk_c6) = sk_c9 )
| ~ iPr_def_14
| ( inverse(inverse(sk_c1)) != inverse(X0) )
| ( multiply(sk_c1,inverse(X0)) != sk_c12 )
| ( multiply(inverse(X0),sk_c11) != sk_c12 )
| ( multiply(X0,inverse(X0)) != sk_c12 ) ),
inference(resolution,[status(thm)],[c_6999,c_829]) ).
tcf(c_27625,plain,
( ( sk_c12 = multiply(inverse(sk_c12),sk_c12) )
| ( sk_c12 != multiply(sk_c6,sk_c9) )
| ( multiply(inverse(sk_c12),sk_c12) != multiply(sk_c6,sk_c9) ) ),
inference(instantiation,[status(thm)],[c_2760]) ).
tcf(c_27685,plain,
( ( inverse(sk_c4) = sk_c12 )
| ~ iPr_def_14
| ( sk_c12 != identity )
| ( inverse(inverse(sk_c1)) != inverse(sk_c11) )
| ( multiply(sk_c1,inverse(sk_c11)) != sk_c12 )
| ( multiply(sk_c11,inverse(sk_c11)) != sk_c12 ) ),
inference(resolution,[status(thm)],[c_26579,c_2366]) ).
tcf(c_27737,plain,
( ( inverse(sk_c5) = sk_c11 )
| ~ iPr_def_14
| ( sk_c12 != identity )
| ( inverse(inverse(sk_c1)) != inverse(sk_c11) )
| ( multiply(sk_c1,inverse(sk_c11)) != sk_c12 )
| ( multiply(sk_c11,inverse(sk_c11)) != sk_c12 ) ),
inference(resolution,[status(thm)],[c_26635,c_2366]) ).
tcf(c_27739,plain,
( ~ iPr_def_10
| ( inverse(inverse(sk_c12)) != sk_c12 )
| ( multiply(inverse(sk_c12),sk_c12) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_825]) ).
tcf(c_27778,plain,
( ( inverse(sk_c6) = sk_c9 )
| ~ iPr_def_14
| ( sk_c12 != identity )
| ( inverse(inverse(sk_c1)) != inverse(sk_c11) )
| ( multiply(sk_c1,inverse(sk_c11)) != sk_c12 )
| ( multiply(sk_c11,inverse(sk_c11)) != sk_c12 ) ),
inference(resolution,[status(thm)],[c_27266,c_2366]) ).
tcf(c_28364,plain,
! [X0: $i] :
( ( inverse(X0) = inverse(sk_c12) )
| ( inverse(sk_c12) != sk_c12 )
| ( inverse(X0) != sk_c12 ) ),
inference(instantiation,[status(thm)],[c_1773]) ).
tcf(c_28365,plain,
! [X0: $i,X1: $i] :
( ( inverse(X0) = X1 )
| ( X1 != sk_c12 )
| ( inverse(X0) != sk_c12 ) ),
inference(instantiation,[status(thm)],[c_1236]) ).
tcf(c_28366,plain,
! [X0: $i] :
( ( sk_c11 = inverse(X0) )
| ( sk_c11 != sk_c12 )
| ( inverse(X0) != sk_c12 ) ),
inference(instantiation,[status(thm)],[c_1206]) ).
tcf(c_28367,plain,
( ( sk_c11 = inverse(sk_c11) )
| ( sk_c11 != sk_c12 )
| ( inverse(sk_c11) != sk_c12 ) ),
inference(instantiation,[status(thm)],[c_28366]) ).
tcf(c_28368,plain,
( ( inverse(sk_c11) = sk_c11 )
| ( sk_c11 != sk_c12 )
| ( inverse(sk_c11) != sk_c12 ) ),
inference(instantiation,[status(thm)],[c_28365]) ).
tcf(c_28369,plain,
( ( inverse(sk_c11) = inverse(sk_c12) )
| ( inverse(sk_c11) != sk_c12 )
| ( inverse(sk_c12) != sk_c12 ) ),
inference(instantiation,[status(thm)],[c_28364]) ).
tcf(c_28379,plain,
! [X0: $i] :
( ( inverse(sk_c4) = inverse(X0) )
| ( inverse(sk_c4) != sk_c12 )
| ( inverse(X0) != sk_c12 ) ),
inference(instantiation,[status(thm)],[c_1295]) ).
tcf(c_28384,plain,
( ( inverse(sk_c4) = inverse(sk_c11) )
| ( inverse(sk_c4) != sk_c12 )
| ( inverse(sk_c11) != sk_c12 ) ),
inference(instantiation,[status(thm)],[c_28379]) ).
tcf(c_30104,plain,
! [X0: $i,X1: $i] :
( ( inverse(X0) = X1 )
| ( X1 != multiply(sk_c11,sk_c10) )
| ( inverse(X0) != multiply(sk_c11,sk_c10) ) ),
inference(instantiation,[status(thm)],[c_1236]) ).
tcf(c_30105,plain,
! [X0: $i] :
( ( sk_c11 = inverse(X0) )
| ( sk_c11 != multiply(sk_c11,sk_c10) )
| ( inverse(X0) != multiply(sk_c11,sk_c10) ) ),
inference(instantiation,[status(thm)],[c_1206]) ).
tcf(c_30106,plain,
( ( sk_c11 = inverse(sk_c11) )
| ( sk_c11 != multiply(sk_c11,sk_c10) )
| ( inverse(sk_c11) != multiply(sk_c11,sk_c10) ) ),
inference(instantiation,[status(thm)],[c_30105]) ).
tcf(c_30107,plain,
( ( inverse(sk_c11) = sk_c11 )
| ( sk_c11 != multiply(sk_c11,sk_c10) )
| ( inverse(sk_c11) != multiply(sk_c11,sk_c10) ) ),
inference(instantiation,[status(thm)],[c_30104]) ).
tcf(c_30693,plain,
( iPr_def_14
| iPr_def_13
| iPr_def_12
| iPr_def_10
| ( inverse(sk_c5) = sk_c11 ) ),
inference(global_subsumption_just,[status(thm)],[c_11593,c_129,c_11593]) ).
tcf(c_30715,plain,
( iPr_def_14
| iPr_def_13
| iPr_def_12
| iPr_def_10
| ( sk_c11 = inverse(sk_c5) ) ),
inference(resolution,[status(thm)],[c_30693,c_2370]) ).
tcf(c_30758,plain,
( ( inverse(sk_c12) = multiply(inverse(sk_c12),sk_c12) )
| ( inverse(sk_c12) != sk_c11 )
| ( multiply(inverse(sk_c12),sk_c12) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_16647]) ).
tcf(c_32488,plain,
( iPr_def_14
| iPr_def_13
| iPr_def_12
| iPr_def_10
| ( inverse(sk_c6) = sk_c9 ) ),
inference(global_subsumption_just,[status(thm)],[c_11702,c_151,c_131,c_141,c_830,c_3451]) ).
tcf(c_32510,plain,
( iPr_def_14
| iPr_def_13
| iPr_def_12
| iPr_def_10
| ( sk_c9 = inverse(sk_c6) ) ),
inference(resolution,[status(thm)],[c_32488,c_2370]) ).
tcf(c_32826,plain,
( ( inverse(sk_c12) = sk_c12 )
| ( sk_c12 != multiply(inverse(sk_c12),sk_c12) )
| ( inverse(sk_c12) != multiply(inverse(sk_c12),sk_c12) ) ),
inference(instantiation,[status(thm)],[c_1675]) ).
tcf(c_32829,plain,
! [X0: $i] :
( ( sk_c12 = X0 )
| ( sk_c12 != multiply(inverse(sk_c12),sk_c12) )
| ( X0 != multiply(inverse(sk_c12),sk_c12) ) ),
inference(instantiation,[status(thm)],[c_1209]) ).
tcf(c_32830,plain,
( ( sk_c12 = sk_c11 )
| ( sk_c11 != multiply(inverse(sk_c12),sk_c12) )
| ( sk_c12 != multiply(inverse(sk_c12),sk_c12) ) ),
inference(instantiation,[status(thm)],[c_32829]) ).
tcf(c_34055,plain,
! [X0: $i] :
( ( sk_c11 = inverse(X0) )
| ( sk_c11 != identity )
| ( inverse(X0) != identity ) ),
inference(instantiation,[status(thm)],[c_1206]) ).
tcf(c_34057,plain,
( ( sk_c11 = inverse(sk_c11) )
| ( sk_c11 != identity )
| ( inverse(sk_c11) != identity ) ),
inference(instantiation,[status(thm)],[c_34055]) ).
tcf(c_34066,plain,
( ( inverse(sk_c12) = inverse(identity) )
| ( sk_c12 != identity ) ),
inference(instantiation,[status(thm)],[c_1200]) ).
tcf(c_34088,plain,
! [X0: $i,X1: $i] :
( ( multiply(X0,sk_c12) = identity )
| ( identity != X1 )
| ( multiply(X0,sk_c12) != X1 ) ),
inference(instantiation,[status(thm)],[c_3514]) ).
tcf(c_34090,plain,
( ( multiply(sk_c11,sk_c12) = identity )
| ( identity != sk_c11 )
| ( multiply(sk_c11,sk_c12) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_34088]) ).
tcf(c_34098,plain,
! [X0: $i] :
( ( X0 = multiply(sk_c6,sk_c9) )
| ( X0 != identity )
| ( multiply(sk_c6,sk_c9) != identity ) ),
inference(instantiation,[status(thm)],[c_2758]) ).
tcf(c_34100,plain,
( ( sk_c11 = multiply(sk_c6,sk_c9) )
| ( sk_c11 != identity )
| ( multiply(sk_c6,sk_c9) != identity ) ),
inference(instantiation,[status(thm)],[c_34098]) ).
tcf(c_36118,plain,
! [X0: $i,X1: $i] :
( ( multiply(inverse(sk_c12),sk_c12) = X1 )
| ( X1 != multiply(X0,sk_c12) )
| ( multiply(inverse(sk_c12),sk_c12) != multiply(X0,sk_c12) ) ),
inference(instantiation,[status(thm)],[c_13006]) ).
tcf(c_36119,plain,
! [X0: $i] :
( ( multiply(inverse(sk_c12),sk_c12) = multiply(X0,sk_c12) )
| ( sk_c12 != sk_c12 )
| ( inverse(sk_c12) != X0 ) ),
inference(instantiation,[status(thm)],[c_4791]) ).
tcf(c_36120,plain,
( ( multiply(inverse(sk_c12),sk_c12) = sk_c11 )
| ( sk_c11 != multiply(sk_c11,sk_c12) )
| ( multiply(inverse(sk_c12),sk_c12) != multiply(sk_c11,sk_c12) ) ),
inference(instantiation,[status(thm)],[c_36118]) ).
tcf(c_36121,plain,
( ( multiply(inverse(sk_c12),sk_c12) = multiply(sk_c11,sk_c12) )
| ( sk_c12 != sk_c12 )
| ( inverse(sk_c12) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_36119]) ).
tcf(c_36291,plain,
! [X0: $i,X1: $i] :
( ( sk_c11 = multiply(X0,X1) )
| ( sk_c11 != multiply(sk_c2,sk_c3) )
| ( multiply(X0,X1) != multiply(sk_c2,sk_c3) ) ),
inference(instantiation,[status(thm)],[c_12746]) ).
tcf(c_36292,plain,
( ( sk_c11 = multiply(sk_c11,sk_c11) )
| ( sk_c11 != multiply(sk_c2,sk_c3) )
| ( multiply(sk_c11,sk_c11) != multiply(sk_c2,sk_c3) ) ),
inference(instantiation,[status(thm)],[c_36291]) ).
tcf(c_37810,plain,
( ( inverse(sk_c1) = sk_c12 )
| ( inverse(sk_c12) = sk_c4 ) ),
inference(superposition,[status(thm)],[c_147,c_17626]) ).
tcf(c_37811,plain,
( ( inverse(sk_c12) = sk_c4 )
| ( inverse(sk_c12) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_127,c_17626]) ).
tcf(c_37812,plain,
( ( inverse(sk_c1) = sk_c12 )
| ( inverse(sk_c11) = sk_c5 ) ),
inference(superposition,[status(thm)],[c_149,c_17626]) ).
tcf(c_37817,plain,
( ( inverse(sk_c7) = sk_c8 )
| ( inverse(sk_c12) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_133,c_17626]) ).
tcf(c_37820,plain,
! [X0: $i] : multiply(X0,inverse(X0)) = identity,
inference(superposition,[status(thm)],[c_17626,c_124]) ).
tcf(c_38151,plain,
! [X0: $i,X1: $i] :
( ~ iPr_def_14
| ( inverse(X1) != X0 )
| ( multiply(inverse(X1),sk_c11) != sk_c12 )
| ( multiply(X1,inverse(X1)) != sk_c12 )
| ( multiply(X0,inverse(X1)) != inverse(X0) ) ),
inference(light_normalisation,[status(thm)],[c_829,c_17626]) ).
tcf(c_38207,plain,
! [X0: $i,X1: $i] :
( ~ iPr_def_14
| ( sk_c12 != identity )
| ( inverse(X1) != X0 )
| ( multiply(inverse(X1),sk_c11) != sk_c12 )
| ( multiply(X0,inverse(X1)) != inverse(X0) ) ),
inference(demodulation,[status(thm)],[c_38151,c_37820]) ).
tcf(c_38208,plain,
( ~ iPr_def_14
| ( sk_c12 != identity )
| ( inverse(sk_c11) != sk_c11 )
| ( multiply(sk_c11,inverse(sk_c11)) != inverse(sk_c11) )
| ( multiply(inverse(sk_c11),sk_c11) != sk_c12 ) ),
inference(instantiation,[status(thm)],[c_38207]) ).
tcf(c_38212,plain,
( ( inverse(sk_c2) = sk_c3 )
| ( multiply(sk_c4,sk_c12) = identity ) ),
inference(superposition,[status(thm)],[c_177,c_37820]) ).
tcf(c_38213,plain,
( ( inverse(sk_c1) = sk_c12 )
| ( multiply(sk_c4,sk_c12) = identity ) ),
inference(superposition,[status(thm)],[c_147,c_37820]) ).
tcf(c_38231,plain,
! [X0: $i,X1: $i] : multiply(X0,multiply(X1,inverse(multiply(X0,X1)))) = identity,
inference(superposition,[status(thm)],[c_37820,c_125]) ).
tcf(c_38285,plain,
( ( sk_c9 = sk_c8 )
| ( inverse(sk_c12) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_134,c_37817]) ).
tcf(c_38296,plain,
( ( sk_c9 = sk_c8 )
| ( multiply(sk_c11,sk_c12) = identity ) ),
inference(superposition,[status(thm)],[c_38285,c_124]) ).
tcf(c_38377,plain,
multiply(sk_c11,sk_c12) = identity,
inference(global_subsumption_just,[status(thm)],[c_38296,c_837,c_1240,c_2603,c_2615,c_2616,c_5092,c_5297,c_5465,c_5943,c_12712,c_12972,c_12979,c_22853,c_22906,c_32830,c_34090]) ).
tcf(c_38379,plain,
! [X0: $i] : multiply(sk_c11,multiply(sk_c12,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_38377,c_125]) ).
tcf(c_38382,plain,
! [X0: $i] : multiply(sk_c11,multiply(sk_c12,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_38379,c_123]) ).
tcf(c_38395,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(X0,X1)) = X1,
inference(demodulation,[status(thm)],[c_1507,c_123]) ).
tcf(c_38397,plain,
! [X0: $i] :
( ( inverse(sk_c12) = sk_c11 )
| ( multiply(sk_c4,multiply(sk_c12,X0)) = X0 ) ),
inference(superposition,[status(thm)],[c_37811,c_38395]) ).
tcf(c_38416,plain,
! [X0: $i] :
( ( inverse(sk_c11) = sk_c5 )
| ( multiply(sk_c12,multiply(sk_c1,X0)) = X0 ) ),
inference(superposition,[status(thm)],[c_37812,c_38395]) ).
tcf(c_38417,plain,
! [X0: $i] :
( ( inverse(sk_c12) = sk_c4 )
| ( multiply(sk_c12,multiply(sk_c1,X0)) = X0 ) ),
inference(superposition,[status(thm)],[c_37810,c_38395]) ).
tcf(c_38563,plain,
! [X0: $i] :
( ( inverse(sk_c2) = sk_c3 )
| ( multiply(sk_c4,multiply(sk_c12,X0)) = multiply(identity,X0) ) ),
inference(superposition,[status(thm)],[c_38212,c_125]) ).
tcf(c_38585,plain,
( ( sk_c11 = identity )
| ( inverse(sk_c1) = sk_c12 ) ),
inference(superposition,[status(thm)],[c_38213,c_146]) ).
tcf(c_38592,plain,
! [X0: $i] :
( ( sk_c11 = identity )
| ( multiply(sk_c12,multiply(sk_c1,X0)) = X0 ) ),
inference(superposition,[status(thm)],[c_38585,c_38395]) ).
tcf(c_38916,plain,
( ( inverse(sk_c12) = sk_c11 )
| ( multiply(sk_c4,multiply(sk_c12,inverse(sk_c11))) = identity ) ),
inference(superposition,[status(thm)],[c_126,c_38231]) ).
tcf(c_38963,plain,
( ( inverse(sk_c6) = sk_c9 )
| ( multiply(sk_c2,multiply(sk_c3,inverse(sk_c11))) = identity ) ),
inference(superposition,[status(thm)],[c_171,c_38231]) ).
tcf(c_38964,plain,
( ( inverse(sk_c5) = sk_c11 )
| ( multiply(sk_c2,multiply(sk_c3,inverse(sk_c11))) = identity ) ),
inference(superposition,[status(thm)],[c_169,c_38231]) ).
tcf(c_38965,plain,
( ( inverse(sk_c4) = sk_c12 )
| ( multiply(sk_c2,multiply(sk_c3,inverse(sk_c11))) = identity ) ),
inference(superposition,[status(thm)],[c_167,c_38231]) ).
tcf(c_39387,plain,
( ( sk_c11 = identity )
| ( inverse(sk_c6) = sk_c9 )
| ( multiply(sk_c12,sk_c12) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_161,c_38592]) ).
tcf(c_40336,plain,
! [X0: $i] :
( ( multiply(sk_c2,sk_c3) = sk_c11 )
| ( multiply(inverse(multiply(X0,sk_c4)),multiply(X0,sk_c11)) = sk_c12 ) ),
inference(superposition,[status(thm)],[c_166,c_3171]) ).
tcf(c_40397,plain,
! [X0: $i] :
( ( inverse(sk_c6) = sk_c9 )
| ( multiply(inverse(multiply(X0,sk_c3)),multiply(X0,sk_c11)) = sk_c12 ) ),
inference(superposition,[status(thm)],[c_191,c_3171]) ).
tcf(c_40398,plain,
! [X0: $i] :
( ( inverse(sk_c5) = sk_c11 )
| ( multiply(inverse(multiply(X0,sk_c3)),multiply(X0,sk_c11)) = sk_c12 ) ),
inference(superposition,[status(thm)],[c_189,c_3171]) ).
tcf(c_40399,plain,
! [X0: $i] :
( ( inverse(sk_c4) = sk_c12 )
| ( multiply(inverse(multiply(X0,sk_c3)),multiply(X0,sk_c11)) = sk_c12 ) ),
inference(superposition,[status(thm)],[c_187,c_3171]) ).
tcf(c_40899,plain,
( ( inverse(sk_c2) = sk_c3 )
| ~ iPr_def_11 ),
inference(global_subsumption_just,[status(thm)],[c_3445,c_149,c_1356,c_1388,c_3452,c_4751,c_5136,c_12034,c_16264,c_34100]) ).
tcf(c_40903,plain,
( ( inverse(sk_c1) = sk_c12 )
| ~ iPr_def_11 ),
inference(global_subsumption_just,[status(thm)],[c_3446,c_1356,c_4752,c_5221,c_12034,c_22528,c_34100]) ).
tcf(c_41164,plain,
( ( inverse(sk_c12) = sk_c11 )
| ( multiply(sk_c4,identity) = inverse(sk_c12) ) ),
inference(superposition,[status(thm)],[c_37820,c_38397]) ).
tcf(c_41193,plain,
( ( inverse(sk_c11) = identity )
| ( inverse(sk_c12) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_38397,c_38916]) ).
tcf(c_41203,plain,
inverse(sk_c12) = sk_c11,
inference(global_subsumption_just,[status(thm)],[c_41164,c_837,c_1201,c_1202,c_2603,c_3716,c_4753,c_5049,c_5284,c_12995,c_13009,c_27625,c_32830,c_34057,c_41193]) ).
tcf(c_41267,plain,
multiply(sk_c12,sk_c11) = identity,
inference(superposition,[status(thm)],[c_41203,c_37820]) ).
tcf(c_41268,plain,
inverse(sk_c11) = sk_c12,
inference(superposition,[status(thm)],[c_41203,c_17626]) ).
tcf(c_41446,plain,
! [X0: $i] :
( ( sk_c12 = sk_c5 )
| ( multiply(sk_c12,multiply(sk_c1,X0)) = X0 ) ),
inference(light_normalisation,[status(thm)],[c_38416,c_41268]) ).
tcf(c_41456,plain,
( ( sk_c12 = sk_c5 )
| ( inverse(sk_c5) = sk_c11 )
| ( multiply(sk_c12,sk_c12) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_159,c_41446]) ).
tcf(c_41457,plain,
( ( sk_c12 = sk_c5 )
| ( inverse(sk_c4) = sk_c12 )
| ( multiply(sk_c12,sk_c12) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_157,c_41446]) ).
tcf(c_41479,plain,
! [X0: $i] :
( ( sk_c11 = sk_c4 )
| ( multiply(sk_c12,multiply(sk_c1,X0)) = X0 ) ),
inference(light_normalisation,[status(thm)],[c_38417,c_41203]) ).
tcf(c_41490,plain,
( ( sk_c11 = sk_c4 )
| ( inverse(sk_c4) = sk_c12 )
| ( multiply(sk_c12,sk_c12) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_157,c_41479]) ).
tcf(c_41710,plain,
( ( inverse(sk_c6) = sk_c9 )
| ( multiply(sk_c2,multiply(sk_c3,sk_c12)) = identity ) ),
inference(light_normalisation,[status(thm)],[c_38963,c_41268]) ).
tcf(c_41718,plain,
( ( inverse(sk_c6) = sk_c9 )
| ( multiply(sk_c2,sk_c11) = identity ) ),
inference(superposition,[status(thm)],[c_191,c_41710]) ).
tcf(c_41752,plain,
( ( inverse(sk_c5) = sk_c11 )
| ( multiply(sk_c2,multiply(sk_c3,sk_c12)) = identity ) ),
inference(light_normalisation,[status(thm)],[c_38964,c_41268]) ).
tcf(c_41761,plain,
( ( inverse(sk_c5) = sk_c11 )
| ( multiply(sk_c2,sk_c11) = identity ) ),
inference(superposition,[status(thm)],[c_189,c_41752]) ).
tcf(c_41794,plain,
( ( inverse(sk_c4) = sk_c12 )
| ( multiply(sk_c2,multiply(sk_c3,sk_c12)) = identity ) ),
inference(light_normalisation,[status(thm)],[c_38965,c_41268]) ).
tcf(c_41804,plain,
( ( inverse(sk_c4) = sk_c12 )
| ( multiply(sk_c2,sk_c11) = identity ) ),
inference(superposition,[status(thm)],[c_187,c_41794]) ).
tcf(c_45660,plain,
! [X0: $i,X1: $i] :
( ( multiply(sk_c11,sk_c10) = multiply(X0,X1) )
| ( multiply(sk_c11,sk_c10) != inverse(sk_c1) )
| ( multiply(X0,X1) != inverse(sk_c1) ) ),
inference(instantiation,[status(thm)],[c_23827]) ).
tcf(c_45668,plain,
( ( multiply(sk_c11,sk_c10) = multiply(sk_c11,sk_c11) )
| ( multiply(sk_c11,sk_c10) != inverse(sk_c1) )
| ( multiply(sk_c11,sk_c11) != inverse(sk_c1) ) ),
inference(instantiation,[status(thm)],[c_45660]) ).
tcf(c_45694,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( inverse(sk_c1) = X2 )
| ( X2 != multiply(X0,X1) )
| ( inverse(sk_c1) != multiply(X0,X1) ) ),
inference(instantiation,[status(thm)],[c_1236]) ).
tcf(c_45697,plain,
( ( inverse(sk_c1) = sk_c11 )
| ( sk_c11 != multiply(sk_c11,sk_c11) )
| ( inverse(sk_c1) != multiply(sk_c11,sk_c11) ) ),
inference(instantiation,[status(thm)],[c_45694]) ).
tcf(c_45838,plain,
( ( multiply(inverse(sk_c12),sk_c12) = multiply(sk_c2,sk_c3) )
| ( multiply(sk_c2,sk_c3) != identity )
| ( multiply(inverse(sk_c12),sk_c12) != identity ) ),
inference(instantiation,[status(thm)],[c_25538]) ).
tcf(c_45846,plain,
( ( multiply(inverse(sk_c12),sk_c12) = sk_c11 )
| ( sk_c11 != multiply(sk_c2,sk_c3) )
| ( multiply(inverse(sk_c12),sk_c12) != multiply(sk_c2,sk_c3) ) ),
inference(instantiation,[status(thm)],[c_25539]) ).
tcf(c_46043,plain,
inverse(sk_c12) = sk_c11,
inference(global_subsumption_just,[status(thm)],[c_10487,c_837,c_1201,c_1202,c_2603,c_3716,c_4753,c_5049,c_5284,c_12995,c_13009,c_27625,c_32830,c_34057,c_41193]) ).
tcf(c_46813,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X0 = sk_c12 )
| ( sk_c12 != multiply(X1,X2) )
| ( X0 != multiply(X1,X2) ) ),
inference(instantiation,[status(thm)],[c_1265]) ).
tcf(c_46814,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( sk_c12 = X0 )
| ( sk_c12 != multiply(X1,X2) )
| ( X0 != multiply(X1,X2) ) ),
inference(instantiation,[status(thm)],[c_1209]) ).
tcf(c_46815,plain,
( ( sk_c12 = sk_c11 )
| ( sk_c11 != multiply(sk_c11,sk_c11) )
| ( sk_c12 != multiply(sk_c11,sk_c11) ) ),
inference(instantiation,[status(thm)],[c_46814]) ).
tcf(c_46816,plain,
( ( sk_c11 = sk_c12 )
| ( sk_c11 != multiply(sk_c11,sk_c11) )
| ( sk_c12 != multiply(sk_c11,sk_c11) ) ),
inference(instantiation,[status(thm)],[c_46813]) ).
tcf(c_49436,plain,
! [X0: $i,X1: $i] :
( ( multiply(inverse(X0),sk_c11) = sk_c12 )
| ( sk_c12 != X1 )
| ( multiply(inverse(X0),sk_c11) != X1 ) ),
inference(instantiation,[status(thm)],[c_832]) ).
tcf(c_49446,plain,
! [X0: $i,X1: $i] :
( ( sk_c12 = X0 )
| ( sk_c12 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_832]) ).
tcf(c_49449,plain,
! [X0: $i] :
( ( sk_c12 = X0 )
| ( sk_c12 != sk_c12 )
| ( X0 != sk_c12 ) ),
inference(instantiation,[status(thm)],[c_49446]) ).
tcf(c_49462,plain,
! [X0: $i,X1: $i] :
( ( X0 = sk_c12 )
| ( sk_c12 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_832]) ).
tcf(c_49465,plain,
( ( sk_c12 = multiply(inverse(identity),sk_c12) )
| ( sk_c12 != sk_c12 )
| ( multiply(inverse(identity),sk_c12) != sk_c12 ) ),
inference(instantiation,[status(thm)],[c_49449]) ).
tcf(c_49466,plain,
multiply(inverse(identity),sk_c12) = sk_c12,
inference(instantiation,[status(thm)],[c_2569]) ).
tcf(c_49467,plain,
( ( sk_c12 = multiply(inverse(inverse(sk_c12)),identity) )
| ( sk_c12 != sk_c12 )
| ( multiply(inverse(inverse(sk_c12)),identity) != sk_c12 ) ),
inference(instantiation,[status(thm)],[c_49449]) ).
tcf(c_49468,plain,
multiply(inverse(inverse(sk_c12)),identity) = sk_c12,
inference(instantiation,[status(thm)],[c_2570]) ).
tcf(c_49473,plain,
( ( sk_c12 = inverse(inverse(sk_c12)) )
| ( sk_c12 != sk_c12 )
| ( inverse(inverse(sk_c12)) != sk_c12 ) ),
inference(instantiation,[status(thm)],[c_49449]) ).
tcf(c_49474,plain,
inverse(inverse(sk_c12)) = sk_c12,
inference(instantiation,[status(thm)],[c_17626]) ).
tcf(c_49503,plain,
! [X0: $i] :
( ( multiply(inverse(X0),sk_c11) = sk_c12 )
| ( sk_c12 != multiply(inverse(identity),sk_c12) )
| ( multiply(inverse(X0),sk_c11) != multiply(inverse(identity),sk_c12) ) ),
inference(instantiation,[status(thm)],[c_49436]) ).
tcf(c_49504,plain,
( ( multiply(inverse(sk_c11),sk_c11) = sk_c12 )
| ( sk_c12 != multiply(inverse(identity),sk_c12) )
| ( multiply(inverse(sk_c11),sk_c11) != multiply(inverse(identity),sk_c12) ) ),
inference(instantiation,[status(thm)],[c_49503]) ).
tcf(c_49509,plain,
! [X0: $i] :
( ( multiply(inverse(X0),sk_c11) = sk_c12 )
| ( sk_c12 != multiply(inverse(inverse(sk_c12)),identity) )
| ( multiply(inverse(X0),sk_c11) != multiply(inverse(inverse(sk_c12)),identity) ) ),
inference(instantiation,[status(thm)],[c_49436]) ).
tcf(c_49510,plain,
( ( multiply(inverse(sk_c11),sk_c11) = sk_c12 )
| ( sk_c12 != multiply(inverse(inverse(sk_c12)),identity) )
| ( multiply(inverse(sk_c11),sk_c11) != multiply(inverse(inverse(sk_c12)),identity) ) ),
inference(instantiation,[status(thm)],[c_49509]) ).
tcf(c_49517,plain,
! [X0: $i] :
( ( sk_c12 = X0 )
| ( sk_c12 != inverse(inverse(sk_c12)) )
| ( X0 != inverse(inverse(sk_c12)) ) ),
inference(instantiation,[status(thm)],[c_49446]) ).
tcf(c_49521,plain,
! [X0: $i] :
( ( X0 = sk_c12 )
| ( sk_c12 != inverse(sk_c4) )
| ( X0 != inverse(sk_c4) ) ),
inference(instantiation,[status(thm)],[c_49462]) ).
tcf(c_49522,plain,
! [X0: $i] :
( ( X0 = sk_c12 )
| ( sk_c12 != multiply(sk_c6,sk_c9) )
| ( X0 != multiply(sk_c6,sk_c9) ) ),
inference(instantiation,[status(thm)],[c_49462]) ).
tcf(c_49528,plain,
! [X0: $i] :
( ( X0 = sk_c12 )
| ( sk_c12 != multiply(identity,sk_c12) )
| ( X0 != multiply(identity,sk_c12) ) ),
inference(instantiation,[status(thm)],[c_49462]) ).
tcf(c_49563,plain,
! [X0: $i] :
( ( X0 = sk_c12 )
| ( sk_c12 != multiply(sk_c1,sk_c11) )
| ( X0 != multiply(sk_c1,sk_c11) ) ),
inference(instantiation,[status(thm)],[c_49462]) ).
tcf(c_49588,plain,
! [X0: $i,X1: $i] :
( ( X1 = multiply(sk_c6,sk_c9) )
| ( X1 != X0 )
| ( multiply(sk_c6,sk_c9) != X0 ) ),
inference(instantiation,[status(thm)],[c_832]) ).
tcf(c_49641,plain,
! [X0: $i] :
( ( multiply(inverse(X0),sk_c11) = multiply(inverse(identity),sk_c12) )
| ( sk_c11 != sk_c12 )
| ( inverse(X0) != inverse(identity) ) ),
inference(instantiation,[status(thm)],[c_834]) ).
tcf(c_49642,plain,
( ( multiply(inverse(sk_c11),sk_c11) = multiply(inverse(identity),sk_c12) )
| ( sk_c11 != sk_c12 )
| ( inverse(sk_c11) != inverse(identity) ) ),
inference(instantiation,[status(thm)],[c_49641]) ).
tcf(c_49645,plain,
! [X0: $i] :
( ( multiply(inverse(X0),sk_c11) = multiply(inverse(inverse(sk_c12)),identity) )
| ( sk_c11 != identity )
| ( inverse(X0) != inverse(inverse(sk_c12)) ) ),
inference(instantiation,[status(thm)],[c_834]) ).
tcf(c_49646,plain,
( ( multiply(inverse(sk_c11),sk_c11) = multiply(inverse(inverse(sk_c12)),identity) )
| ( sk_c11 != identity )
| ( inverse(sk_c11) != inverse(inverse(sk_c12)) ) ),
inference(instantiation,[status(thm)],[c_49645]) ).
tcf(c_49654,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(X0,inverse(X1)) = inverse(X0) )
| ( inverse(X0) != X2 )
| ( multiply(X0,inverse(X1)) != X2 ) ),
inference(instantiation,[status(thm)],[c_832]) ).
tcf(c_49697,plain,
( ( inverse(inverse(identity)) = inverse(identity) )
| ( inverse(identity) != identity ) ),
inference(instantiation,[status(thm)],[c_833]) ).
tcf(c_49718,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( multiply(X0,inverse(X1)) = X3 )
| ( X3 != X2 )
| ( multiply(X0,inverse(X1)) != X2 ) ),
inference(instantiation,[status(thm)],[c_832]) ).
tcf(c_49720,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( multiply(X2,inverse(X0)) = multiply(X3,X1) )
| ( X2 != X3 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_834]) ).
tcf(c_49722,plain,
( ( multiply(sk_c11,inverse(sk_c11)) = multiply(sk_c11,sk_c11) )
| ( sk_c11 != sk_c11 )
| ( inverse(sk_c11) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_49720]) ).
tcf(c_49723,plain,
! [X0: $i,X1: $i] :
( ( multiply(X0,inverse(X1)) = inverse(X0) )
| ( inverse(X0) != sk_c12 )
| ( multiply(X0,inverse(X1)) != sk_c12 ) ),
inference(instantiation,[status(thm)],[c_49654]) ).
tcf(c_49728,plain,
! [X0: $i,X1: $i] :
( ( multiply(X0,inverse(X1)) = sk_c12 )
| ( sk_c12 != multiply(identity,sk_c12) )
| ( multiply(X0,inverse(X1)) != multiply(identity,sk_c12) ) ),
inference(instantiation,[status(thm)],[c_49528]) ).
tcf(c_49729,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(X0,inverse(X1)) = sk_c12 )
| ( sk_c12 != X2 )
| ( multiply(X0,inverse(X1)) != X2 ) ),
inference(instantiation,[status(thm)],[c_49462]) ).
tcf(c_49732,plain,
! [X0: $i,X1: $i] :
( ( multiply(X0,inverse(X1)) = sk_c12 )
| ( sk_c12 != multiply(sk_c6,sk_c9) )
| ( multiply(X0,inverse(X1)) != multiply(sk_c6,sk_c9) ) ),
inference(instantiation,[status(thm)],[c_49522]) ).
tcf(c_49734,plain,
( ( multiply(sk_c11,inverse(sk_c11)) = inverse(sk_c11) )
| ( inverse(sk_c11) != sk_c12 )
| ( multiply(sk_c11,inverse(sk_c11)) != sk_c12 ) ),
inference(instantiation,[status(thm)],[c_49723]) ).
tcf(c_49736,plain,
( ( multiply(sk_c11,inverse(sk_c11)) = sk_c12 )
| ( sk_c12 != multiply(sk_c6,sk_c9) )
| ( multiply(sk_c11,inverse(sk_c11)) != multiply(sk_c6,sk_c9) ) ),
inference(instantiation,[status(thm)],[c_49732]) ).
tcf(c_49740,plain,
( ( multiply(sk_c11,inverse(sk_c11)) = sk_c12 )
| ( sk_c12 != multiply(identity,sk_c12) )
| ( multiply(sk_c11,inverse(sk_c11)) != multiply(identity,sk_c12) ) ),
inference(instantiation,[status(thm)],[c_49728]) ).
tcf(c_49919,plain,
sk_c4 = sk_c4,
inference(instantiation,[status(thm)],[c_831]) ).
tcf(c_49921,plain,
! [X0: $i,X1: $i] :
( ( sk_c4 = X0 )
| ( sk_c4 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_832]) ).
tcf(c_49954,plain,
! [X0: $i,X1: $i] :
( ( inverse(X0) = inverse(identity) )
| ( inverse(identity) != X1 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_832]) ).
tcf(c_49956,plain,
! [X0: $i] :
( ( inverse(X0) = inverse(identity) )
| ( X0 != identity ) ),
inference(instantiation,[status(thm)],[c_833]) ).
tcf(c_49957,plain,
( ( inverse(sk_c11) = inverse(identity) )
| ( sk_c11 != identity ) ),
inference(instantiation,[status(thm)],[c_49956]) ).
tcf(c_49964,plain,
! [X0: $i] :
( ( inverse(X0) = inverse(inverse(sk_c12)) )
| ( X0 != inverse(sk_c12) ) ),
inference(instantiation,[status(thm)],[c_833]) ).
tcf(c_49965,plain,
( ( inverse(sk_c11) = inverse(inverse(sk_c12)) )
| ( sk_c11 != inverse(sk_c12) ) ),
inference(instantiation,[status(thm)],[c_49964]) ).
tcf(c_50135,plain,
! [X0: $i] :
( ( inverse(inverse(sk_c12)) = multiply(sk_c6,sk_c9) )
| ( multiply(sk_c6,sk_c9) != X0 )
| ( inverse(inverse(sk_c12)) != X0 ) ),
inference(instantiation,[status(thm)],[c_49588]) ).
tcf(c_50186,plain,
! [X0: $i] :
( ( inverse(inverse(sk_c1)) = inverse(X0) )
| ( inverse(sk_c1) != X0 ) ),
inference(instantiation,[status(thm)],[c_833]) ).
tcf(c_50187,plain,
( ( inverse(inverse(sk_c1)) = inverse(sk_c11) )
| ( inverse(sk_c1) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_50186]) ).
tcf(c_50217,plain,
! [X0: $i] :
( ( inverse(X0) = sk_c12 )
| ( sk_c12 != inverse(sk_c4) )
| ( inverse(X0) != inverse(sk_c4) ) ),
inference(instantiation,[status(thm)],[c_49521]) ).
tcf(c_50405,plain,
! [X0: $i,X1: $i] :
( ( inverse(identity) = inverse(X0) )
| ( inverse(identity) != X1 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_832]) ).
tcf(c_50407,plain,
! [X0: $i] :
( ( inverse(identity) = inverse(X0) )
| ( identity != X0 ) ),
inference(instantiation,[status(thm)],[c_833]) ).
tcf(c_50408,plain,
( ( inverse(identity) = inverse(sk_c11) )
| ( identity != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_50407]) ).
tcf(c_50466,plain,
! [X0: $i,X1: $i] :
( ( inverse(inverse(identity)) = inverse(X1) )
| ( inverse(X1) != X0 )
| ( inverse(inverse(identity)) != X0 ) ),
inference(instantiation,[status(thm)],[c_832]) ).
tcf(c_50572,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( multiply(X0,inverse(X1)) = sk_c12 )
| ( sk_c12 != multiply(X2,X3) )
| ( multiply(X0,inverse(X1)) != multiply(X2,X3) ) ),
inference(instantiation,[status(thm)],[c_49729]) ).
tcf(c_50574,plain,
( ( multiply(sk_c11,inverse(sk_c11)) = sk_c12 )
| ( sk_c12 != multiply(sk_c11,sk_c11) )
| ( multiply(sk_c11,inverse(sk_c11)) != multiply(sk_c11,sk_c11) ) ),
inference(instantiation,[status(thm)],[c_50572]) ).
tcf(c_50581,plain,
! [X0: $i,X1: $i] :
( ( multiply(X1,inverse(X0)) = multiply(identity,sk_c12) )
| ( X1 != identity )
| ( inverse(X0) != sk_c12 ) ),
inference(instantiation,[status(thm)],[c_49720]) ).
tcf(c_50582,plain,
( ( multiply(sk_c11,inverse(sk_c11)) = multiply(identity,sk_c12) )
| ( sk_c11 != identity )
| ( inverse(sk_c11) != sk_c12 ) ),
inference(instantiation,[status(thm)],[c_50581]) ).
tcf(c_50591,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(sk_c1,inverse(X0)) = multiply(X2,X1) )
| ( sk_c1 != X2 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_49720]) ).
tcf(c_50678,plain,
! [X0: $i,X1: $i] :
( ( multiply(X0,sk_c11) = sk_c10 )
| ( sk_c10 != X1 )
| ( multiply(X0,sk_c11) != X1 ) ),
inference(instantiation,[status(thm)],[c_832]) ).
tcf(c_50792,plain,
! [X0: $i,X1: $i] :
( ( multiply(X0,inverse(X1)) = sk_c12 )
| ( sk_c12 != multiply(sk_c1,sk_c11) )
| ( multiply(X0,inverse(X1)) != multiply(sk_c1,sk_c11) ) ),
inference(instantiation,[status(thm)],[c_49563]) ).
tcf(c_51042,plain,
! [X0: $i] :
( ( inverse(sk_c4) = sk_c12 )
| ( sk_c12 != X0 )
| ( inverse(sk_c4) != X0 ) ),
inference(instantiation,[status(thm)],[c_49462]) ).
tcf(c_51079,plain,
! [X0: $i] :
( ( sk_c4 = X0 )
| ( sk_c4 != sk_c4 )
| ( X0 != sk_c4 ) ),
inference(instantiation,[status(thm)],[c_49921]) ).
tcf(c_51080,plain,
( ( sk_c4 = sk_c11 )
| ( sk_c4 != sk_c4 )
| ( sk_c11 != sk_c4 ) ),
inference(instantiation,[status(thm)],[c_51079]) ).
tcf(c_51156,plain,
( iPr_def_14
| iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( multiply(sk_c11,sk_c10) != sk_c12 ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_830,c_46043]) ).
tcf(c_51161,plain,
( ( multiply(sk_c12,sk_c12) = sk_c11 )
| ( inverse(sk_c6) = sk_c9 ) ),
inference(global_subsumption_just,[status(thm)],[c_39387,c_151,c_141,c_837,c_830,c_1201,c_1202,c_1204,c_1240,c_1263,c_1810,c_1885,c_1902,c_2602,c_2603,c_3451,c_3716,c_4491,c_4753,c_5049,c_5150,c_5284,c_8174,c_12196,c_12972,c_12979,c_12995,c_13009,c_17628,c_17969,c_17986,c_27625,c_27739,c_28369,c_30758,c_32826,c_32830,c_34057,c_38208,c_41193,c_41268,c_45838,c_45846,c_49467,c_49468,c_49474,c_49510,c_49646,c_49734,c_49740,c_49965,c_50582]) ).
tcf(c_51162,plain,
( ( inverse(sk_c6) = sk_c9 )
| ( multiply(sk_c12,sk_c12) = sk_c11 ) ),
inference(renaming,[status(thm)],[c_51161]) ).
tcf(c_51171,plain,
( ( inverse(sk_c6) = sk_c9 )
| ~ iPr_def_10
| ( inverse(sk_c12) != sk_c12 ) ),
inference(superposition,[status(thm)],[c_51162,c_825]) ).
tcf(c_51179,plain,
( ( inverse(sk_c6) = sk_c9 )
| ( multiply(sk_c11,sk_c11) = sk_c12 ) ),
inference(superposition,[status(thm)],[c_51162,c_38382]) ).
tcf(c_51412,plain,
! [X0: $i,X1: $i] :
( ( X1 = inverse(inverse(sk_c12)) )
| ( X1 != X0 )
| ( inverse(inverse(sk_c12)) != X0 ) ),
inference(instantiation,[status(thm)],[c_832]) ).
tcf(c_51520,plain,
! [X0: $i] :
( ( inverse(X0) = inverse(identity) )
| ( inverse(identity) != sk_c12 )
| ( inverse(X0) != sk_c12 ) ),
inference(instantiation,[status(thm)],[c_49954]) ).
tcf(c_51527,plain,
( ( inverse(sk_c11) = inverse(identity) )
| ( inverse(identity) != sk_c12 )
| ( inverse(sk_c11) != sk_c12 ) ),
inference(instantiation,[status(thm)],[c_51520]) ).
tcf(c_51793,plain,
! [X0: $i,X1: $i] :
( ( sk_c10 = X0 )
| ( sk_c10 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_832]) ).
tcf(c_52001,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(X0,inverse(X1)) = multiply(sk_c6,sk_c9) )
| ( multiply(sk_c6,sk_c9) != X2 )
| ( multiply(X0,inverse(X1)) != X2 ) ),
inference(instantiation,[status(thm)],[c_49718]) ).
tcf(c_52056,plain,
! [X0: $i,X1: $i] :
( ( X1 = inverse(inverse(identity)) )
| ( X1 != X0 )
| ( inverse(inverse(identity)) != X0 ) ),
inference(instantiation,[status(thm)],[c_832]) ).
tcf(c_52059,plain,
! [X0: $i] :
( ( inverse(X0) = inverse(inverse(identity)) )
| ( X0 != inverse(identity) ) ),
inference(instantiation,[status(thm)],[c_833]) ).
tcf(c_52088,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(X0,inverse(X1)) = inverse(inverse(identity)) )
| ( inverse(inverse(identity)) != X2 )
| ( multiply(X0,inverse(X1)) != X2 ) ),
inference(instantiation,[status(thm)],[c_49718]) ).
tcf(c_52207,plain,
! [X0: $i,X1: $i] :
( ( inverse(inverse(identity)) = X1 )
| ( X1 != X0 )
| ( inverse(inverse(identity)) != X0 ) ),
inference(instantiation,[status(thm)],[c_832]) ).
tcf(c_52210,plain,
! [X0: $i] :
( ( inverse(inverse(identity)) = inverse(X0) )
| ( inverse(X0) != sk_c12 )
| ( inverse(inverse(identity)) != sk_c12 ) ),
inference(instantiation,[status(thm)],[c_50466]) ).
tcf(c_52217,plain,
( ( inverse(inverse(identity)) = inverse(sk_c11) )
| ( inverse(sk_c11) != sk_c12 )
| ( inverse(inverse(identity)) != sk_c12 ) ),
inference(instantiation,[status(thm)],[c_52210]) ).
tcf(c_52227,plain,
! [X0: $i] :
( ( inverse(inverse(identity)) = inverse(X0) )
| ( inverse(X0) != inverse(identity) )
| ( inverse(inverse(identity)) != inverse(identity) ) ),
inference(instantiation,[status(thm)],[c_50466]) ).
tcf(c_52228,plain,
( ( inverse(inverse(identity)) = inverse(sk_c11) )
| ( inverse(sk_c11) != inverse(identity) )
| ( inverse(inverse(identity)) != inverse(identity) ) ),
inference(instantiation,[status(thm)],[c_52227]) ).
tcf(c_52230,plain,
inverse(inverse(identity)) = identity,
inference(instantiation,[status(thm)],[c_17626]) ).
tcf(c_52258,plain,
! [X0: $i,X1: $i] :
( ( multiply(sk_c1,inverse(X0)) = multiply(sk_c1,X1) )
| ( sk_c1 != sk_c1 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_50591]) ).
tcf(c_52259,plain,
sk_c1 = sk_c1,
inference(instantiation,[status(thm)],[c_831]) ).
tcf(c_52260,plain,
( ( multiply(sk_c1,inverse(sk_c11)) = multiply(sk_c1,sk_c11) )
| ( sk_c1 != sk_c1 )
| ( inverse(sk_c11) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_52258]) ).
tcf(c_52297,plain,
! [X0: $i] :
( ( sk_c12 = inverse(sk_c4) )
| ( sk_c12 != X0 )
| ( inverse(sk_c4) != X0 ) ),
inference(instantiation,[status(thm)],[c_49446]) ).
tcf(c_52298,plain,
( ( sk_c12 = inverse(sk_c4) )
| ( sk_c12 != sk_c11 )
| ( inverse(sk_c4) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_52297]) ).
tcf(c_52337,plain,
( ( sk_c12 = multiply(sk_c6,sk_c9) )
| ( sk_c12 != inverse(inverse(sk_c12)) )
| ( multiply(sk_c6,sk_c9) != inverse(inverse(sk_c12)) ) ),
inference(instantiation,[status(thm)],[c_49517]) ).
tcf(c_52674,plain,
( ( inverse(identity) = sk_c12 )
| ( sk_c12 != inverse(sk_c4) )
| ( inverse(identity) != inverse(sk_c4) ) ),
inference(instantiation,[status(thm)],[c_50217]) ).
tcf(c_52675,plain,
! [X0: $i] :
( ( inverse(identity) = inverse(sk_c4) )
| ( inverse(identity) != X0 )
| ( inverse(sk_c4) != X0 ) ),
inference(instantiation,[status(thm)],[c_50405]) ).
tcf(c_54800,plain,
( ( inverse(sk_c4) = sk_c12 )
| ( sk_c12 != inverse(inverse(sk_c12)) )
| ( inverse(sk_c4) != inverse(inverse(sk_c12)) ) ),
inference(instantiation,[status(thm)],[c_51042]) ).
tcf(c_55870,plain,
! [X0: $i] :
( ( multiply(sk_c6,sk_c9) = inverse(inverse(sk_c12)) )
| ( multiply(sk_c6,sk_c9) != X0 )
| ( inverse(inverse(sk_c12)) != X0 ) ),
inference(instantiation,[status(thm)],[c_51412]) ).
tcf(c_56589,plain,
! [X0: $i] :
( ( sk_c10 = X0 )
| ( sk_c10 != sk_c10 )
| ( X0 != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_51793]) ).
tcf(c_58804,plain,
! [X0: $i,X1: $i] :
( ( X1 = inverse(inverse(identity)) )
| ( X1 != inverse(X0) )
| ( inverse(inverse(identity)) != inverse(X0) ) ),
inference(instantiation,[status(thm)],[c_52056]) ).
tcf(c_58807,plain,
! [X0: $i] :
( ( X0 = inverse(inverse(identity)) )
| ( X0 != identity )
| ( inverse(inverse(identity)) != identity ) ),
inference(instantiation,[status(thm)],[c_52056]) ).
tcf(c_58847,plain,
! [X0: $i] :
( ( inverse(inverse(identity)) = X0 )
| ( X0 != identity )
| ( inverse(inverse(identity)) != identity ) ),
inference(instantiation,[status(thm)],[c_52207]) ).
tcf(c_58968,plain,
! [X0: $i] :
( ( multiply(sk_c1,inverse(X0)) = sk_c12 )
| ( sk_c12 != multiply(sk_c1,sk_c11) )
| ( multiply(sk_c1,inverse(X0)) != multiply(sk_c1,sk_c11) ) ),
inference(instantiation,[status(thm)],[c_50792]) ).
tcf(c_58969,plain,
( ( multiply(sk_c1,inverse(sk_c11)) = sk_c12 )
| ( sk_c12 != multiply(sk_c1,sk_c11) )
| ( multiply(sk_c1,inverse(sk_c11)) != multiply(sk_c1,sk_c11) ) ),
inference(instantiation,[status(thm)],[c_58968]) ).
tcf(c_59630,plain,
! [X0: $i,X1: $i] :
( ( multiply(X0,inverse(X1)) = inverse(inverse(identity)) )
| ( inverse(inverse(identity)) != identity )
| ( multiply(X0,inverse(X1)) != identity ) ),
inference(instantiation,[status(thm)],[c_52088]) ).
tcf(c_59631,plain,
( ( multiply(sk_c11,inverse(sk_c11)) = inverse(inverse(identity)) )
| ( inverse(inverse(identity)) != identity )
| ( multiply(sk_c11,inverse(sk_c11)) != identity ) ),
inference(instantiation,[status(thm)],[c_59630]) ).
tcf(c_61673,plain,
( ( inverse(inverse(sk_c12)) = multiply(sk_c6,sk_c9) )
| ( multiply(sk_c6,sk_c9) != inverse(inverse(identity)) )
| ( inverse(inverse(sk_c12)) != inverse(inverse(identity)) ) ),
inference(instantiation,[status(thm)],[c_50135]) ).
tcf(c_62105,plain,
( ( inverse(inverse(identity)) = sk_c12 )
| ( sk_c12 != multiply(sk_c6,sk_c9) )
| ( inverse(inverse(identity)) != multiply(sk_c6,sk_c9) ) ),
inference(instantiation,[status(thm)],[c_49522]) ).
tcf(c_62877,plain,
( ( sk_c10 = multiply(inverse(sk_c11),sk_c12) )
| ( sk_c10 != sk_c10 )
| ( multiply(inverse(sk_c11),sk_c12) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_56589]) ).
tcf(c_63335,plain,
( iPr_def_14
| iPr_def_13
| iPr_def_12
| iPr_def_11
| ( multiply(sk_c11,sk_c10) != sk_c12 ) ),
inference(global_subsumption_just,[status(thm)],[c_51156,c_837,c_830,c_1201,c_1202,c_1885,c_2603,c_3716,c_4753,c_5049,c_5150,c_5284,c_12196,c_12995,c_13009,c_27625,c_27739,c_32830,c_34057,c_41193,c_45838,c_45846,c_49474]) ).
tcf(c_63347,plain,
~ iPr_def_10,
inference(global_subsumption_just,[status(thm)],[c_51171,c_1885,c_2603,c_5150,c_12196,c_27739,c_45838,c_45846,c_49474]) ).
tcf(c_64867,plain,
( ( inverse(inverse(sk_c12)) = inverse(inverse(identity)) )
| ( inverse(sk_c12) != inverse(identity) ) ),
inference(instantiation,[status(thm)],[c_52059]) ).
tcf(c_67171,plain,
( ( inverse(identity) = inverse(sk_c4) )
| ( inverse(identity) != inverse(inverse(identity)) )
| ( inverse(sk_c4) != inverse(inverse(identity)) ) ),
inference(instantiation,[status(thm)],[c_52675]) ).
tcf(c_67188,plain,
( ( multiply(sk_c6,sk_c9) = inverse(inverse(identity)) )
| ( multiply(sk_c6,sk_c9) != identity )
| ( inverse(inverse(identity)) != identity ) ),
inference(instantiation,[status(thm)],[c_58807]) ).
tcf(c_67714,plain,
! [X0: $i] :
( ( inverse(sk_c4) = inverse(inverse(identity)) )
| ( inverse(sk_c4) != inverse(X0) )
| ( inverse(inverse(identity)) != inverse(X0) ) ),
inference(instantiation,[status(thm)],[c_58804]) ).
tcf(c_67717,plain,
( ( inverse(sk_c4) = inverse(inverse(identity)) )
| ( inverse(sk_c4) != inverse(sk_c11) )
| ( inverse(inverse(identity)) != inverse(sk_c11) ) ),
inference(instantiation,[status(thm)],[c_67714]) ).
tcf(c_70133,plain,
! [X0: $i,X1: $i] :
( ( multiply(X0,inverse(X1)) = multiply(sk_c6,sk_c9) )
| ( multiply(sk_c6,sk_c9) != inverse(inverse(identity)) )
| ( multiply(X0,inverse(X1)) != inverse(inverse(identity)) ) ),
inference(instantiation,[status(thm)],[c_52001]) ).
tcf(c_70135,plain,
( ( multiply(sk_c11,inverse(sk_c11)) = multiply(sk_c6,sk_c9) )
| ( multiply(sk_c6,sk_c9) != inverse(inverse(identity)) )
| ( multiply(sk_c11,inverse(sk_c11)) != inverse(inverse(identity)) ) ),
inference(instantiation,[status(thm)],[c_70133]) ).
tcf(c_71351,plain,
( ( inverse(inverse(identity)) = multiply(sk_c6,sk_c9) )
| ( multiply(sk_c6,sk_c9) != identity )
| ( inverse(inverse(identity)) != identity ) ),
inference(instantiation,[status(thm)],[c_58847]) ).
tcf(c_71767,plain,
( ( multiply(sk_c6,sk_c9) = inverse(inverse(sk_c12)) )
| ( multiply(sk_c6,sk_c9) != multiply(sk_c6,sk_c9) )
| ( inverse(inverse(sk_c12)) != multiply(sk_c6,sk_c9) ) ),
inference(instantiation,[status(thm)],[c_55870]) ).
tcf(c_73138,plain,
! [X0: $i] :
( ( multiply(X0,sk_c11) = sk_c10 )
| ( sk_c10 != multiply(inverse(sk_c11),sk_c12) )
| ( multiply(X0,sk_c11) != multiply(inverse(sk_c11),sk_c12) ) ),
inference(instantiation,[status(thm)],[c_50678]) ).
tcf(c_73139,plain,
( ( multiply(sk_c11,sk_c11) = sk_c10 )
| ( sk_c10 != multiply(inverse(sk_c11),sk_c12) )
| ( multiply(sk_c11,sk_c11) != multiply(inverse(sk_c11),sk_c12) ) ),
inference(instantiation,[status(thm)],[c_73138]) ).
tcf(c_73938,plain,
( iPr_def_14
| iPr_def_13
| iPr_def_12
| iPr_def_11
| ( inverse(sk_c4) = sk_c12 ) ),
inference(resolution,[status(thm)],[c_63335,c_137]) ).
tcf(c_73990,plain,
( iPr_def_14
| iPr_def_13
| iPr_def_12
| ( inverse(sk_c4) = sk_c12 ) ),
inference(global_subsumption_just,[status(thm)],[c_73938,c_149,c_137,c_837,c_830,c_1201,c_1202,c_1240,c_1263,c_1356,c_1810,c_1885,c_2603,c_3453,c_3565,c_3717,c_3716,c_4491,c_4761,c_4753,c_4752,c_5049,c_5150,c_5221,c_5284,c_5465,c_5818,c_7956,c_12196,c_12995,c_13009,c_22906,c_23453,c_27625,c_27739,c_32830,c_34057,c_34100,c_40903,c_41193,c_41268,c_45838,c_45846,c_49474,c_49697,c_49740,c_49957,c_50408,c_50582,c_52228]) ).
tcf(c_74061,plain,
! [X0: $i] :
( iPr_def_14
| iPr_def_13
| iPr_def_12
| ( inverse(sk_c4) = X0 )
| ( X0 != sk_c12 ) ),
inference(resolution,[status(thm)],[c_73990,c_832]) ).
tcf(c_74062,plain,
( iPr_def_14
| iPr_def_13
| iPr_def_12
| ( inverse(sk_c4) = sk_c11 )
| ( sk_c11 != sk_c12 ) ),
inference(instantiation,[status(thm)],[c_74061]) ).
tcf(c_74152,plain,
inverse(sk_c1) = sk_c12,
inference(global_subsumption_just,[status(thm)],[c_10497,c_149,c_837,c_1201,c_1202,c_1240,c_1263,c_1356,c_1810,c_1885,c_2603,c_3565,c_3717,c_3716,c_4491,c_4761,c_4753,c_4752,c_5049,c_5150,c_5221,c_5284,c_5465,c_5818,c_7956,c_12196,c_12995,c_13009,c_22906,c_23453,c_27625,c_27739,c_32830,c_34057,c_34100,c_40903,c_41193,c_41268,c_45838,c_45846,c_49474,c_49697,c_49740,c_49957,c_50408,c_50582,c_52228]) ).
tcf(c_74163,plain,
inverse(sk_c2) = sk_c3,
inference(global_subsumption_just,[status(thm)],[c_10544,c_179,c_837,c_1201,c_1202,c_1240,c_1263,c_1356,c_1810,c_1885,c_2603,c_3564,c_3718,c_3716,c_4491,c_4761,c_4753,c_4751,c_5049,c_5136,c_5150,c_5284,c_5465,c_5777,c_8219,c_12196,c_12995,c_13009,c_22906,c_23453,c_27625,c_27739,c_32830,c_34057,c_34100,c_40899,c_41193,c_41268,c_45838,c_45846,c_49474,c_49697,c_49740,c_49957,c_50408,c_50582,c_52228]) ).
tcf(c_74659,plain,
( ( inverse(identity) = inverse(inverse(identity)) )
| ( inverse(identity) != identity )
| ( inverse(inverse(identity)) != identity ) ),
inference(instantiation,[status(thm)],[c_58807]) ).
tcf(c_75595,plain,
( ( multiply(sk_c12,sk_c12) = sk_c11 )
| ( inverse(sk_c5) = sk_c11 ) ),
inference(global_subsumption_just,[status(thm)],[c_41456,c_1240,c_1263,c_1810,c_1885,c_2603,c_4491,c_4761,c_5150,c_5465,c_8175,c_12196,c_17628,c_17970,c_17987,c_22906,c_23453,c_27739,c_30693,c_41268,c_45838,c_45846,c_49474,c_49697,c_49740,c_49957,c_50408,c_50582,c_52228]) ).
tcf(c_75596,plain,
( ( inverse(sk_c5) = sk_c11 )
| ( multiply(sk_c12,sk_c12) = sk_c11 ) ),
inference(renaming,[status(thm)],[c_75595]) ).
tcf(c_75612,plain,
( ( inverse(sk_c5) = sk_c11 )
| ( multiply(sk_c11,sk_c11) = sk_c12 ) ),
inference(superposition,[status(thm)],[c_75596,c_38382]) ).
tcf(c_75627,plain,
( ( multiply(sk_c12,sk_c12) = sk_c11 )
| ( inverse(sk_c4) = sk_c12 ) ),
inference(global_subsumption_just,[status(thm)],[c_41457,c_837,c_1201,c_1202,c_1240,c_2603,c_3716,c_4753,c_5049,c_5284,c_8846,c_8848,c_12995,c_13009,c_27625,c_32830,c_34057,c_41193,c_41490,c_49473,c_49474,c_49919,c_51080,c_54800]) ).
tcf(c_75628,plain,
( ( inverse(sk_c4) = sk_c12 )
| ( multiply(sk_c12,sk_c12) = sk_c11 ) ),
inference(renaming,[status(thm)],[c_75627]) ).
tcf(c_75644,plain,
( ( inverse(sk_c4) = sk_c12 )
| ( multiply(sk_c11,sk_c11) = sk_c12 ) ),
inference(superposition,[status(thm)],[c_75628,c_38382]) ).
tcf(c_75659,plain,
inverse(sk_c2) = sk_c3,
inference(global_subsumption_just,[status(thm)],[c_38563,c_74163]) ).
tcf(c_75694,plain,
( ( inverse(sk_c6) = sk_c9 )
| ( multiply(sk_c3,sk_c11) = sk_c3 ) ),
inference(demodulation,[status(thm)],[c_2973,c_75659]) ).
tcf(c_75695,plain,
( ( inverse(sk_c5) = sk_c11 )
| ( multiply(sk_c3,sk_c11) = sk_c3 ) ),
inference(demodulation,[status(thm)],[c_2970,c_75659]) ).
tcf(c_75696,plain,
( ( inverse(sk_c4) = sk_c12 )
| ( multiply(sk_c3,sk_c11) = sk_c3 ) ),
inference(demodulation,[status(thm)],[c_2967,c_75659]) ).
tcf(c_75719,plain,
multiply(sk_c2,sk_c3) = identity,
inference(superposition,[status(thm)],[c_75659,c_37820]) ).
tcf(c_75720,plain,
inverse(sk_c3) = sk_c2,
inference(superposition,[status(thm)],[c_75659,c_17626]) ).
tcf(c_75857,plain,
( ( inverse(sk_c6) = sk_c9 )
| ( multiply(sk_c11,sk_c11) = multiply(sk_c2,sk_c3) ) ),
inference(superposition,[status(thm)],[c_75694,c_1498]) ).
tcf(c_75875,plain,
( ( inverse(sk_c5) = sk_c11 )
| ( multiply(sk_c11,sk_c11) = multiply(sk_c2,sk_c3) ) ),
inference(superposition,[status(thm)],[c_75695,c_1499]) ).
tcf(c_75893,plain,
( ( inverse(sk_c4) = sk_c12 )
| ( multiply(sk_c11,sk_c11) = multiply(sk_c2,sk_c3) ) ),
inference(superposition,[status(thm)],[c_75696,c_1500]) ).
tcf(c_76703,plain,
! [X0: $i] :
( ( sk_c11 = identity )
| ( multiply(sk_c4,multiply(sk_c12,X0)) = multiply(sk_c11,X0) ) ),
inference(light_normalisation,[status(thm)],[c_1746,c_75719]) ).
tcf(c_85393,plain,
! [X0: $i] :
( ( multiply(X0,sk_c11) = multiply(inverse(sk_c11),sk_c12) )
| ( sk_c11 != sk_c12 )
| ( X0 != inverse(sk_c11) ) ),
inference(instantiation,[status(thm)],[c_834]) ).
tcf(c_85394,plain,
( ( multiply(sk_c11,sk_c11) = multiply(inverse(sk_c11),sk_c12) )
| ( sk_c11 != sk_c12 )
| ( sk_c11 != inverse(sk_c11) ) ),
inference(instantiation,[status(thm)],[c_85393]) ).
tcf(c_87211,plain,
( ( inverse(sk_c6) = sk_c9 )
| ( multiply(inverse(sk_c3),multiply(identity,sk_c11)) = sk_c12 ) ),
inference(superposition,[status(thm)],[c_123,c_40397]) ).
tcf(c_87227,plain,
( ( inverse(sk_c6) = sk_c9 )
| ( multiply(inverse(multiply(identity,sk_c3)),sk_c11) = sk_c12 ) ),
inference(superposition,[status(thm)],[c_123,c_40397]) ).
tcf(c_87299,plain,
( ( inverse(sk_c5) = sk_c11 )
| ( multiply(inverse(sk_c3),multiply(identity,sk_c11)) = sk_c12 ) ),
inference(superposition,[status(thm)],[c_123,c_40398]) ).
tcf(c_87315,plain,
( ( inverse(sk_c5) = sk_c11 )
| ( multiply(inverse(multiply(identity,sk_c3)),sk_c11) = sk_c12 ) ),
inference(superposition,[status(thm)],[c_123,c_40398]) ).
tcf(c_87387,plain,
( ( inverse(sk_c4) = sk_c12 )
| ( multiply(inverse(sk_c3),multiply(identity,sk_c11)) = sk_c12 ) ),
inference(superposition,[status(thm)],[c_123,c_40399]) ).
tcf(c_87403,plain,
( ( inverse(sk_c4) = sk_c12 )
| ( multiply(inverse(multiply(identity,sk_c3)),sk_c11) = sk_c12 ) ),
inference(superposition,[status(thm)],[c_123,c_40399]) ).
tcf(c_87815,plain,
( ( inverse(sk_c6) = sk_c9 )
| ( multiply(sk_c2,multiply(identity,sk_c11)) = sk_c12 ) ),
inference(light_normalisation,[status(thm)],[c_87211,c_75720]) ).
tcf(c_87816,plain,
( ( inverse(sk_c6) = sk_c9 )
| ( multiply(sk_c2,sk_c11) = sk_c12 ) ),
inference(demodulation,[status(thm)],[c_87815,c_123]) ).
tcf(c_87837,plain,
( ( inverse(sk_c6) = sk_c9 )
| ( multiply(inverse(sk_c2),sk_c12) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_87816,c_38395]) ).
tcf(c_87846,plain,
( ( sk_c12 = identity )
| ( inverse(sk_c6) = sk_c9 ) ),
inference(superposition,[status(thm)],[c_87816,c_41718]) ).
tcf(c_87852,plain,
inverse(sk_c6) = sk_c9,
inference(global_subsumption_just,[status(thm)],[c_87227,c_149,c_171,c_837,c_840,c_1201,c_1202,c_1240,c_1263,c_1356,c_1810,c_1885,c_2603,c_2788,c_3001,c_3565,c_3717,c_3716,c_3743,c_3753,c_4491,c_4761,c_4753,c_4752,c_5049,c_5150,c_5221,c_5284,c_5465,c_5818,c_7956,c_12196,c_12995,c_13009,c_13475,c_18120,c_20428,c_22906,c_23453,c_26191,c_26193,c_27625,c_27739,c_27778,c_28367,c_28368,c_32510,c_32830,c_34057,c_34100,c_36292,c_40903,c_41193,c_41268,c_45697,c_45838,c_45846,c_46816,c_49474,c_49697,c_49722,c_49740,c_49957,c_50187,c_50408,c_50574,c_50582,c_51179,c_52228,c_52260,c_52259,c_58969,c_62877,c_73139,c_75857,c_85394,c_87846,c_87837]) ).
tcf(c_87891,plain,
multiply(sk_c6,sk_c9) = identity,
inference(superposition,[status(thm)],[c_87852,c_37820]) ).
tcf(c_88023,plain,
( ( inverse(sk_c5) = sk_c11 )
| ( multiply(sk_c2,multiply(identity,sk_c11)) = sk_c12 ) ),
inference(light_normalisation,[status(thm)],[c_87299,c_75720]) ).
tcf(c_88024,plain,
( ( inverse(sk_c5) = sk_c11 )
| ( multiply(sk_c2,sk_c11) = sk_c12 ) ),
inference(demodulation,[status(thm)],[c_88023,c_123]) ).
tcf(c_88042,plain,
( ( inverse(sk_c5) = sk_c11 )
| ( multiply(inverse(sk_c2),sk_c12) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_88024,c_38395]) ).
tcf(c_88049,plain,
( ( sk_c12 = identity )
| ( inverse(sk_c5) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_88024,c_41761]) ).
tcf(c_88055,plain,
inverse(sk_c5) = sk_c11,
inference(global_subsumption_just,[status(thm)],[c_87315,c_169,c_139,c_837,c_840,c_1240,c_1850,c_2567,c_3242,c_3243,c_3742,c_3752,c_4491,c_4514,c_12911,c_18120,c_20091,c_20215,c_20428,c_26191,c_26193,c_27737,c_30106,c_30107,c_30715,c_36292,c_41268,c_45668,c_45697,c_46816,c_49722,c_50187,c_50574,c_52260,c_52259,c_58969,c_62877,c_63347,c_73139,c_74152,c_75612,c_75875,c_85394,c_88049,c_88042]) ).
tcf(c_88085,plain,
( ( multiply(sk_c2,sk_c3) = sk_c11 )
| ( multiply(sk_c11,sk_c10) = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_3297,c_88055]) ).
tcf(c_88087,plain,
( ( multiply(sk_c11,sk_c10) = sk_c11 )
| ( multiply(sk_c11,sk_c10) = sk_c12 ) ),
inference(demodulation,[status(thm)],[c_3094,c_88055]) ).
tcf(c_88148,plain,
( ( sk_c11 = identity )
| ( multiply(sk_c11,sk_c10) = sk_c11 ) ),
inference(light_normalisation,[status(thm)],[c_88085,c_75719]) ).
tcf(c_88153,plain,
( ( sk_c11 = identity )
| ( sk_c12 = sk_c11 )
| ( inverse(sk_c4) = sk_c12 ) ),
inference(superposition,[status(thm)],[c_137,c_88148]) ).
tcf(c_88195,plain,
( ( inverse(sk_c4) = sk_c12 )
| ( sk_c12 = sk_c11 ) ),
inference(global_subsumption_just,[status(thm)],[c_88153,c_1240,c_3751,c_26191,c_36292,c_46815,c_75644,c_75893]) ).
tcf(c_88196,plain,
( ( sk_c12 = sk_c11 )
| ( inverse(sk_c4) = sk_c12 ) ),
inference(renaming,[status(thm)],[c_88195]) ).
tcf(c_88258,plain,
( ( inverse(sk_c4) = sk_c12 )
| ( multiply(sk_c2,multiply(identity,sk_c11)) = sk_c12 ) ),
inference(light_normalisation,[status(thm)],[c_87387,c_75720]) ).
tcf(c_88259,plain,
( ( inverse(sk_c4) = sk_c12 )
| ( multiply(sk_c2,sk_c11) = sk_c12 ) ),
inference(demodulation,[status(thm)],[c_88258,c_123]) ).
tcf(c_88274,plain,
( ( inverse(sk_c4) = sk_c12 )
| ( multiply(inverse(sk_c2),sk_c12) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_88259,c_38395]) ).
tcf(c_88279,plain,
( ( sk_c12 = identity )
| ( inverse(sk_c4) = sk_c12 ) ),
inference(superposition,[status(thm)],[c_88259,c_41804]) ).
tcf(c_88285,plain,
inverse(sk_c4) = sk_c12,
inference(global_subsumption_just,[status(thm)],[c_87403,c_149,c_167,c_837,c_840,c_1201,c_1202,c_1240,c_1263,c_1266,c_1356,c_1810,c_1849,c_1885,c_2568,c_2603,c_2907,c_3565,c_3717,c_3716,c_3741,c_3751,c_4491,c_4761,c_4753,c_4752,c_5049,c_5150,c_5221,c_5284,c_5465,c_5818,c_7956,c_12196,c_12995,c_13009,c_18120,c_20428,c_22906,c_23453,c_26191,c_26193,c_27625,c_27685,c_27739,c_28367,c_28368,c_32830,c_34057,c_34100,c_36292,c_40903,c_41193,c_41268,c_45697,c_45838,c_45846,c_49474,c_49697,c_49722,c_49740,c_49957,c_50187,c_50408,c_50574,c_50582,c_52228,c_52260,c_52259,c_52298,c_58969,c_62877,c_73139,c_74062,c_75644,c_75893,c_85394,c_88196,c_88279,c_88274]) ).
tcf(c_88314,plain,
( ( multiply(sk_c2,sk_c3) = sk_c11 )
| ( multiply(sk_c12,sk_c11) = sk_c12 ) ),
inference(demodulation,[status(thm)],[c_3283,c_88285]) ).
tcf(c_88548,plain,
( ( sk_c11 = identity )
| ( sk_c12 = identity ) ),
inference(light_normalisation,[status(thm)],[c_88314,c_41267,c_75719]) ).
tcf(c_88558,plain,
! [X0: $i] :
( ( sk_c12 = identity )
| ( multiply(sk_c11,X0) = X0 ) ),
inference(superposition,[status(thm)],[c_88548,c_123]) ).
tcf(c_88943,plain,
sk_c12 = identity,
inference(superposition,[status(thm)],[c_88558,c_38377]) ).
tcf(c_89642,plain,
! [X0: $i] :
( ( sk_c12 = sk_c11 )
| ( multiply(inverse(multiply(X0,sk_c4)),multiply(X0,sk_c11)) = sk_c12 ) ),
inference(light_normalisation,[status(thm)],[c_40336,c_75719,c_88943]) ).
tcf(c_89647,plain,
( ( sk_c12 = sk_c11 )
| ( multiply(inverse(sk_c4),multiply(identity,sk_c11)) = sk_c12 ) ),
inference(superposition,[status(thm)],[c_123,c_89642]) ).
tcf(c_89663,plain,
( ( sk_c12 = sk_c11 )
| ( multiply(inverse(multiply(identity,sk_c4)),sk_c11) = sk_c12 ) ),
inference(superposition,[status(thm)],[c_123,c_89642]) ).
tcf(c_89747,plain,
( ( sk_c12 = sk_c11 )
| ( multiply(sk_c12,sk_c12) = sk_c12 ) ),
inference(light_normalisation,[status(thm)],[c_89647,c_41267,c_88285,c_88943]) ).
tcf(c_89766,plain,
( ( sk_c11 = identity )
| ( sk_c12 = sk_c11 )
| ( multiply(sk_c11,sk_c12) = multiply(sk_c4,sk_c12) ) ),
inference(superposition,[status(thm)],[c_89747,c_76703]) ).
tcf(c_89780,plain,
sk_c12 = sk_c11,
inference(global_subsumption_just,[status(thm)],[c_89663,c_837,c_1201,c_1202,c_1240,c_1356,c_2603,c_3716,c_4753,c_4801,c_5049,c_5284,c_5413,c_10867,c_12972,c_12979,c_12995,c_13009,c_23635,c_27625,c_32830,c_34057,c_34066,c_34100,c_36120,c_36121,c_41193,c_45838,c_45846,c_49473,c_49474,c_52230,c_52337,c_61673,c_64867,c_67188,c_71767,c_75719,c_87891,c_88943,c_89766]) ).
tcf(c_89813,plain,
multiply(sk_c12,sk_c10) = sk_c12,
inference(demodulation,[status(thm)],[c_88087,c_89780]) ).
tcf(c_89877,plain,
inverse(sk_c12) = sk_c12,
inference(demodulation,[status(thm)],[c_41203,c_89780]) ).
tcf(c_89885,plain,
! [X0: $i] : multiply(sk_c12,multiply(sk_c12,X0)) = X0,
inference(demodulation,[status(thm)],[c_38382,c_89780]) ).
tcf(c_89886,plain,
multiply(sk_c12,sk_c12) = identity,
inference(demodulation,[status(thm)],[c_38377,c_89780]) ).
tcf(c_89889,plain,
! [X0: $i] :
( ~ iPr_def_12
| ( inverse(X0) != sk_c12 )
| ( multiply(X0,sk_c12) != sk_c10 ) ),
inference(demodulation,[status(thm)],[c_827,c_89780]) ).
tcf(c_89911,plain,
( ~ iPr_def_13
| ( sk_c12 != identity ) ),
inference(demodulation,[status(thm)],[c_4491,c_89780]) ).
tcf(c_89914,plain,
~ iPr_def_13,
inference(forward_subsumption_resolution,[status(thm)],[c_89911,c_88943]) ).
tcf(c_90016,plain,
multiply(sk_c12,sk_c12) = sk_c12,
inference(light_normalisation,[status(thm)],[c_89886,c_88943]) ).
tcf(c_90022,plain,
! [X0: $i] : multiply(sk_c12,multiply(sk_c12,X0)) = multiply(sk_c12,X0),
inference(superposition,[status(thm)],[c_90016,c_125]) ).
tcf(c_90043,plain,
! [X0: $i] :
( ( multiply(X0,sk_c12) != sk_c10 )
| ( inverse(X0) != sk_c12 ) ),
inference(global_subsumption_just,[status(thm)],[c_89889,c_149,c_167,c_837,c_840,c_1201,c_1202,c_1240,c_1263,c_1266,c_1268,c_1356,c_1388,c_1810,c_1849,c_1885,c_2568,c_2603,c_2907,c_3452,c_3565,c_3717,c_3716,c_3741,c_3751,c_4023,c_4491,c_4583,c_4761,c_4753,c_4752,c_4801,c_5049,c_5150,c_5221,c_5284,c_5413,c_5465,c_5818,c_7956,c_10867,c_12196,c_12972,c_12979,c_12995,c_13009,c_16264,c_18120,c_20428,c_22906,c_23453,c_23635,c_26169,c_26191,c_26193,c_27625,c_27685,c_27739,c_28367,c_28368,c_28384,c_32830,c_34057,c_34066,c_34100,c_36120,c_36121,c_36292,c_40903,c_41193,c_41268,c_45697,c_45838,c_45846,c_49465,c_49466,c_49473,c_49474,c_49504,c_49642,c_49697,c_49722,c_49736,c_49740,c_49957,c_50187,c_50408,c_50574,c_50582,c_51527,c_52217,c_52228,c_52230,c_52260,c_52259,c_52298,c_52337,c_52674,c_58969,c_59631,c_61673,c_62105,c_62877,c_63335,c_64867,c_67171,c_67188,c_67717,c_70135,c_71351,c_71767,c_73139,c_74062,c_74659,c_75644,c_75719,c_75893,c_85394,c_87891,c_88087,c_88196,c_88279,c_88274,c_88943,c_89766,c_89914,c_89889]) ).
tcf(c_90044,plain,
! [X0: $i] :
( ( inverse(X0) != sk_c12 )
| ( multiply(X0,sk_c12) != sk_c10 ) ),
inference(renaming,[status(thm)],[c_90043]) ).
tcf(c_90053,plain,
( ( sk_c12 != sk_c10 )
| ( inverse(sk_c12) != sk_c12 ) ),
inference(superposition,[status(thm)],[c_90016,c_90044]) ).
tcf(c_90054,plain,
sk_c12 != sk_c10,
inference(forward_subsumption_resolution,[status(thm)],[c_90053,c_89877]) ).
tcf(c_90278,plain,
! [X0: $i] : multiply(sk_c12,X0) = X0,
inference(demodulation,[status(thm)],[c_90022,c_89885]) ).
tcf(c_90282,plain,
sk_c12 = sk_c10,
inference(demodulation,[status(thm)],[c_89813,c_90278]) ).
tcf(c_90287,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[c_90282,c_90054]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP382-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.05 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.11/0.39 % Computer : n026.cluster.edu
% 0.11/0.39 % Model : x86_64 x86_64
% 0.11/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.39 % Memory : 8046.5625MB
% 0.11/0.39 % OS : Linux 6.8.0-71-generic
% 0.11/0.39 % CPULimit : 300
% 0.11/0.39 % WCLimit : 300
% 0.11/0.39 % DateTime : Wed Sep 23 14:40:23 UTC 2026
% 0.11/0.39 % CPUTime :
% 0.11/0.39 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.11/0.43 Running first-order theorem proving
% 0.11/0.43 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.11/0.44
% 0.11/0.44 % ======== iProver multi-core TPTP/SMT =========
% 0.11/0.44
% 0.11/0.45 % Detected problem language: tptp
% 0.11/0.46 % Proving...
% 78.16/13.01 % SZS status Started for theBenchmark.p
% 78.16/13.01 % SZS status Unsatisfiable for theBenchmark.p
% 78.16/13.01
% 78.16/13.01 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 78.16/13.01
% 78.16/13.01 % ------ iProver source info
% 78.16/13.01
% 78.16/13.01 % git: date: 2026-07-19 20:42:38 +0200
% 78.16/13.01 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 78.16/13.01 % git: non_committed_changes: false
% 78.16/13.01
% 78.16/13.01 % ------ Parsing...% successful
% 78.16/13.01
% 78.16/13.01
% 78.16/13.01 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 78.16/13.01
% 78.16/13.01 % ------ Preprocessing... sup_sim: 0 sf_s rm: 0 0s sf_e pe_s pe_e %
% 78.16/13.01
% 78.16/13.01 % ------ Preprocessing... gs_s sp: 5 0s gs_e snvd_s sp: 0 0s snvd_e %
% 78.16/13.01
% 78.16/13.01 % ------ Preprocessing... sf_s rm: 0 0s sf_e
% 78.16/13.01 % ------ Proving...
% 78.16/13.01 % ------ Problem Properties
% 78.16/13.01
% 78.16/13.01 %
% 78.16/13.01 % clauses 79
% 78.16/13.01 % conjectures 76
% 78.16/13.01 % EPR 0
% 78.16/13.01 % Horn 8
% 78.16/13.01 % unary 3
% 78.16/13.01 % binary 70
% 78.16/13.01 % lits 167
% 78.16/13.01 % lits eq 157
% 78.16/13.01 % fd_pure 0
% 78.16/13.01 % fd_pseudo 0
% 78.16/13.01 % fd_cond 0
% 78.16/13.01 % fd_pseudo_cond 0
% 78.16/13.01 % AC symbols 0
% 78.16/13.01
% 78.16/13.01 % ------ Input Options Time Limit: Unbounded
% 78.16/13.01
% 78.16/13.01
% 78.16/13.01 % ------
% 78.16/13.01 % Current options:
% 78.16/13.01 % ------
% 78.16/13.01
% 78.16/13.01
% 78.16/13.01 %
% 78.16/13.01
% 78.16/13.01 % ------ Proving...
% 78.16/13.01 %
% 78.16/13.01
% 78.16/13.01 % SZS status Unsatisfiable for theBenchmark.p
% 78.16/13.01
% 78.16/13.01 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 78.16/13.03
% 78.16/13.03
%------------------------------------------------------------------------------