%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : GRP238-1 : TPTP v9.3.1. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% Computer : n004.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 01:32:15 PM UTC 2026
% Result : Unsatisfiable 62.81s 9.40s
% Output : CNFRefutation 62.81s
% Verified :
% SZS Type : Refutation
% Derivation depth : 36
% Number of leaves : 68
% Syntax : Number of formulae : 735 ( 142 unt; 15 def)
% Number of atoms : 2949 (1586 equ)
% Maximal formula atoms : 16 ( 4 avg)
% Number of connectives : 1545 ( 604 ~; 941 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 26 ( 3 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 23 ( 21 usr; 22 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 12 con; 0-2 aty)
% Number of variables : 285 ( 0 sgn 285 !; 0 ?; 240 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0] : multiply(identity,X0) = X0,
file('/export/starexec/sandbox/benchmark/Axioms/GRP004-0.ax',left_identity) ).
fof(f2,axiom,
! [X0] : multiply(inverse(X0),X0) = identity,
file('/export/starexec/sandbox/benchmark/Axioms/GRP004-0.ax',left_inverse) ).
fof(f3,plain,
! [X0] : identity = multiply(inverse(X0),X0),
inference(reorient_equations,[],[f2]) ).
fof(f4,axiom,
! [X2,X0,X1] : multiply(multiply(X0,X1),X2) = multiply(X0,multiply(X1,X2)),
file('/export/starexec/sandbox/benchmark/Axioms/GRP004-0.ax',associativity) ).
fof(f5,negated_conjecture,
( multiply(sk_c4,sk_c5) = sk_c11
| inverse(sk_c11) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_1) ).
fof(f6,plain,
( sk_c11 = multiply(sk_c4,sk_c5)
| inverse(sk_c11) = sk_c10 ),
inference(reorient_equations,[],[f5]) ).
fof(f7,negated_conjecture,
( inverse(sk_c4) = sk_c5
| inverse(sk_c11) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_2) ).
fof(f8,plain,
( sk_c5 = inverse(sk_c4)
| inverse(sk_c11) = sk_c10 ),
inference(reorient_equations,[],[f7]) ).
fof(f13,negated_conjecture,
( multiply(sk_c6,sk_c10) = sk_c11
| inverse(sk_c11) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_5) ).
fof(f14,plain,
( sk_c11 = multiply(sk_c6,sk_c10)
| inverse(sk_c11) = sk_c10 ),
inference(reorient_equations,[],[f13]) ).
fof(f15,negated_conjecture,
( multiply(sk_c7,sk_c8) = sk_c10
| inverse(sk_c11) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_6) ).
fof(f16,plain,
( sk_c10 = multiply(sk_c7,sk_c8)
| inverse(sk_c11) = sk_c10 ),
inference(reorient_equations,[],[f15]) ).
fof(f17,negated_conjecture,
( inverse(sk_c7) = sk_c8
| inverse(sk_c11) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_7) ).
fof(f18,plain,
( sk_c8 = inverse(sk_c7)
| inverse(sk_c11) = sk_c10 ),
inference(reorient_equations,[],[f17]) ).
fof(f19,negated_conjecture,
( multiply(sk_c8,sk_c11) = sk_c10
| inverse(sk_c11) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_8) ).
fof(f20,plain,
( sk_c10 = multiply(sk_c8,sk_c11)
| inverse(sk_c11) = sk_c10 ),
inference(reorient_equations,[],[f19]) ).
fof(f21,negated_conjecture,
( inverse(sk_c9) = sk_c10
| inverse(sk_c11) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_9) ).
fof(f22,plain,
( sk_c10 = inverse(sk_c9)
| inverse(sk_c11) = sk_c10 ),
inference(reorient_equations,[],[f21]) ).
fof(f23,negated_conjecture,
( multiply(sk_c9,sk_c11) = sk_c10
| inverse(sk_c11) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_10) ).
fof(f24,plain,
( sk_c10 = multiply(sk_c9,sk_c11)
| inverse(sk_c11) = sk_c10 ),
inference(reorient_equations,[],[f23]) ).
fof(f25,negated_conjecture,
( multiply(sk_c4,sk_c5) = sk_c11
| inverse(sk_c1) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_11) ).
fof(f26,plain,
( sk_c11 = multiply(sk_c4,sk_c5)
| sk_c11 = inverse(sk_c1) ),
inference(reorient_equations,[],[f25]) ).
fof(f27,negated_conjecture,
( inverse(sk_c4) = sk_c5
| inverse(sk_c1) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_12) ).
fof(f28,plain,
( sk_c5 = inverse(sk_c4)
| sk_c11 = inverse(sk_c1) ),
inference(reorient_equations,[],[f27]) ).
fof(f29,negated_conjecture,
( multiply(sk_c5,sk_c10) = sk_c11
| inverse(sk_c1) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_13) ).
fof(f30,plain,
( sk_c11 = multiply(sk_c5,sk_c10)
| sk_c11 = inverse(sk_c1) ),
inference(reorient_equations,[],[f29]) ).
fof(f31,negated_conjecture,
( inverse(sk_c6) = sk_c11
| inverse(sk_c1) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_14) ).
fof(f32,plain,
( sk_c11 = inverse(sk_c6)
| sk_c11 = inverse(sk_c1) ),
inference(reorient_equations,[],[f31]) ).
fof(f33,negated_conjecture,
( multiply(sk_c6,sk_c10) = sk_c11
| inverse(sk_c1) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_15) ).
fof(f34,plain,
( sk_c11 = multiply(sk_c6,sk_c10)
| sk_c11 = inverse(sk_c1) ),
inference(reorient_equations,[],[f33]) ).
fof(f35,negated_conjecture,
( multiply(sk_c7,sk_c8) = sk_c10
| inverse(sk_c1) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_16) ).
fof(f36,plain,
( sk_c10 = multiply(sk_c7,sk_c8)
| sk_c11 = inverse(sk_c1) ),
inference(reorient_equations,[],[f35]) ).
fof(f37,negated_conjecture,
( inverse(sk_c7) = sk_c8
| inverse(sk_c1) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_17) ).
fof(f38,plain,
( sk_c8 = inverse(sk_c7)
| sk_c11 = inverse(sk_c1) ),
inference(reorient_equations,[],[f37]) ).
fof(f39,negated_conjecture,
( multiply(sk_c8,sk_c11) = sk_c10
| inverse(sk_c1) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_18) ).
fof(f40,plain,
( sk_c10 = multiply(sk_c8,sk_c11)
| sk_c11 = inverse(sk_c1) ),
inference(reorient_equations,[],[f39]) ).
fof(f41,negated_conjecture,
( inverse(sk_c9) = sk_c10
| inverse(sk_c1) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_19) ).
fof(f42,plain,
( sk_c10 = inverse(sk_c9)
| sk_c11 = inverse(sk_c1) ),
inference(reorient_equations,[],[f41]) ).
fof(f43,negated_conjecture,
( multiply(sk_c9,sk_c11) = sk_c10
| inverse(sk_c1) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_20) ).
fof(f44,plain,
( sk_c10 = multiply(sk_c9,sk_c11)
| sk_c11 = inverse(sk_c1) ),
inference(reorient_equations,[],[f43]) ).
fof(f45,negated_conjecture,
( multiply(sk_c4,sk_c5) = sk_c11
| multiply(sk_c1,sk_c10) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_21) ).
fof(f46,plain,
( sk_c11 = multiply(sk_c4,sk_c5)
| sk_c11 = multiply(sk_c1,sk_c10) ),
inference(reorient_equations,[],[f45]) ).
fof(f47,negated_conjecture,
( inverse(sk_c4) = sk_c5
| multiply(sk_c1,sk_c10) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_22) ).
fof(f48,plain,
( sk_c5 = inverse(sk_c4)
| sk_c11 = multiply(sk_c1,sk_c10) ),
inference(reorient_equations,[],[f47]) ).
fof(f49,negated_conjecture,
( multiply(sk_c5,sk_c10) = sk_c11
| multiply(sk_c1,sk_c10) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_23) ).
fof(f50,plain,
( sk_c11 = multiply(sk_c5,sk_c10)
| sk_c11 = multiply(sk_c1,sk_c10) ),
inference(reorient_equations,[],[f49]) ).
fof(f51,negated_conjecture,
( inverse(sk_c6) = sk_c11
| multiply(sk_c1,sk_c10) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_24) ).
fof(f52,plain,
( sk_c11 = inverse(sk_c6)
| sk_c11 = multiply(sk_c1,sk_c10) ),
inference(reorient_equations,[],[f51]) ).
fof(f53,negated_conjecture,
( multiply(sk_c6,sk_c10) = sk_c11
| multiply(sk_c1,sk_c10) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_25) ).
fof(f54,plain,
( sk_c11 = multiply(sk_c6,sk_c10)
| sk_c11 = multiply(sk_c1,sk_c10) ),
inference(reorient_equations,[],[f53]) ).
fof(f55,negated_conjecture,
( multiply(sk_c7,sk_c8) = sk_c10
| multiply(sk_c1,sk_c10) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_26) ).
fof(f56,plain,
( sk_c10 = multiply(sk_c7,sk_c8)
| sk_c11 = multiply(sk_c1,sk_c10) ),
inference(reorient_equations,[],[f55]) ).
fof(f57,negated_conjecture,
( inverse(sk_c7) = sk_c8
| multiply(sk_c1,sk_c10) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_27) ).
fof(f58,plain,
( sk_c8 = inverse(sk_c7)
| sk_c11 = multiply(sk_c1,sk_c10) ),
inference(reorient_equations,[],[f57]) ).
fof(f59,negated_conjecture,
( multiply(sk_c8,sk_c11) = sk_c10
| multiply(sk_c1,sk_c10) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_28) ).
fof(f60,plain,
( sk_c10 = multiply(sk_c8,sk_c11)
| sk_c11 = multiply(sk_c1,sk_c10) ),
inference(reorient_equations,[],[f59]) ).
fof(f61,negated_conjecture,
( inverse(sk_c9) = sk_c10
| multiply(sk_c1,sk_c10) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_29) ).
fof(f62,plain,
( sk_c10 = inverse(sk_c9)
| sk_c11 = multiply(sk_c1,sk_c10) ),
inference(reorient_equations,[],[f61]) ).
fof(f63,negated_conjecture,
( multiply(sk_c9,sk_c11) = sk_c10
| multiply(sk_c1,sk_c10) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_30) ).
fof(f64,plain,
( sk_c10 = multiply(sk_c9,sk_c11)
| sk_c11 = multiply(sk_c1,sk_c10) ),
inference(reorient_equations,[],[f63]) ).
fof(f65,negated_conjecture,
( multiply(sk_c4,sk_c5) = sk_c11
| multiply(sk_c11,sk_c3) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_31) ).
fof(f66,plain,
( sk_c11 = multiply(sk_c4,sk_c5)
| sk_c10 = multiply(sk_c11,sk_c3) ),
inference(reorient_equations,[],[f65]) ).
fof(f67,negated_conjecture,
( inverse(sk_c4) = sk_c5
| multiply(sk_c11,sk_c3) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_32) ).
fof(f68,plain,
( sk_c5 = inverse(sk_c4)
| sk_c10 = multiply(sk_c11,sk_c3) ),
inference(reorient_equations,[],[f67]) ).
fof(f75,negated_conjecture,
( multiply(sk_c7,sk_c8) = sk_c10
| multiply(sk_c11,sk_c3) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_36) ).
fof(f76,plain,
( sk_c10 = multiply(sk_c7,sk_c8)
| sk_c10 = multiply(sk_c11,sk_c3) ),
inference(reorient_equations,[],[f75]) ).
fof(f77,negated_conjecture,
( inverse(sk_c7) = sk_c8
| multiply(sk_c11,sk_c3) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_37) ).
fof(f78,plain,
( sk_c8 = inverse(sk_c7)
| sk_c10 = multiply(sk_c11,sk_c3) ),
inference(reorient_equations,[],[f77]) ).
fof(f81,negated_conjecture,
( inverse(sk_c9) = sk_c10
| multiply(sk_c11,sk_c3) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_39) ).
fof(f82,plain,
( sk_c10 = inverse(sk_c9)
| sk_c10 = multiply(sk_c11,sk_c3) ),
inference(reorient_equations,[],[f81]) ).
fof(f83,negated_conjecture,
( multiply(sk_c9,sk_c11) = sk_c10
| multiply(sk_c11,sk_c3) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_40) ).
fof(f84,plain,
( sk_c10 = multiply(sk_c9,sk_c11)
| sk_c10 = multiply(sk_c11,sk_c3) ),
inference(reorient_equations,[],[f83]) ).
fof(f85,negated_conjecture,
( multiply(sk_c4,sk_c5) = sk_c11
| multiply(sk_c2,sk_c11) = sk_c3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_41) ).
fof(f86,plain,
( sk_c11 = multiply(sk_c4,sk_c5)
| sk_c3 = multiply(sk_c2,sk_c11) ),
inference(reorient_equations,[],[f85]) ).
fof(f87,negated_conjecture,
( inverse(sk_c4) = sk_c5
| multiply(sk_c2,sk_c11) = sk_c3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_42) ).
fof(f88,plain,
( sk_c5 = inverse(sk_c4)
| sk_c3 = multiply(sk_c2,sk_c11) ),
inference(reorient_equations,[],[f87]) ).
fof(f95,negated_conjecture,
( multiply(sk_c7,sk_c8) = sk_c10
| multiply(sk_c2,sk_c11) = sk_c3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_46) ).
fof(f96,plain,
( sk_c10 = multiply(sk_c7,sk_c8)
| sk_c3 = multiply(sk_c2,sk_c11) ),
inference(reorient_equations,[],[f95]) ).
fof(f97,negated_conjecture,
( inverse(sk_c7) = sk_c8
| multiply(sk_c2,sk_c11) = sk_c3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_47) ).
fof(f98,plain,
( sk_c8 = inverse(sk_c7)
| sk_c3 = multiply(sk_c2,sk_c11) ),
inference(reorient_equations,[],[f97]) ).
fof(f99,negated_conjecture,
( multiply(sk_c8,sk_c11) = sk_c10
| multiply(sk_c2,sk_c11) = sk_c3 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_48) ).
fof(f100,plain,
( sk_c10 = multiply(sk_c8,sk_c11)
| sk_c3 = multiply(sk_c2,sk_c11) ),
inference(reorient_equations,[],[f99]) ).
fof(f105,negated_conjecture,
( multiply(sk_c4,sk_c5) = sk_c11
| inverse(sk_c2) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_51) ).
fof(f106,plain,
( sk_c11 = multiply(sk_c4,sk_c5)
| sk_c11 = inverse(sk_c2) ),
inference(reorient_equations,[],[f105]) ).
fof(f107,negated_conjecture,
( inverse(sk_c4) = sk_c5
| inverse(sk_c2) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_52) ).
fof(f108,plain,
( sk_c5 = inverse(sk_c4)
| sk_c11 = inverse(sk_c2) ),
inference(reorient_equations,[],[f107]) ).
fof(f115,negated_conjecture,
( multiply(sk_c7,sk_c8) = sk_c10
| inverse(sk_c2) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_56) ).
fof(f116,plain,
( sk_c10 = multiply(sk_c7,sk_c8)
| sk_c11 = inverse(sk_c2) ),
inference(reorient_equations,[],[f115]) ).
fof(f117,negated_conjecture,
( inverse(sk_c7) = sk_c8
| inverse(sk_c2) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_57) ).
fof(f118,plain,
( sk_c8 = inverse(sk_c7)
| sk_c11 = inverse(sk_c2) ),
inference(reorient_equations,[],[f117]) ).
fof(f121,negated_conjecture,
( inverse(sk_c9) = sk_c10
| inverse(sk_c2) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_59) ).
fof(f122,plain,
( sk_c10 = inverse(sk_c9)
| sk_c11 = inverse(sk_c2) ),
inference(reorient_equations,[],[f121]) ).
fof(f123,negated_conjecture,
( multiply(sk_c9,sk_c11) = sk_c10
| inverse(sk_c2) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_60) ).
fof(f124,plain,
( sk_c10 = multiply(sk_c9,sk_c11)
| sk_c11 = inverse(sk_c2) ),
inference(reorient_equations,[],[f123]) ).
fof(f125,negated_conjecture,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( multiply(X8,sk_c11) != sk_c10
| inverse(X8) != sk_c10
| multiply(X7,sk_c11) != sk_c10
| inverse(X6) != X7
| multiply(X6,X7) != sk_c10
| multiply(X5,sk_c10) != sk_c11
| inverse(X5) != sk_c11
| multiply(X4,sk_c10) != sk_c11
| inverse(X3) != X4
| multiply(X3,X4) != sk_c11
| inverse(X2) != sk_c11
| multiply(X2,sk_c11) != X1
| multiply(sk_c11,X1) != sk_c10
| multiply(X0,sk_c10) != sk_c11
| inverse(X0) != sk_c11
| inverse(sk_c11) != sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_61) ).
fof(f126,plain,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( sk_c10 != multiply(X8,sk_c11)
| sk_c10 != inverse(X8)
| sk_c10 != multiply(X7,sk_c11)
| inverse(X6) != X7
| sk_c10 != multiply(X6,X7)
| sk_c11 != multiply(X5,sk_c10)
| sk_c11 != inverse(X5)
| sk_c11 != multiply(X4,sk_c10)
| inverse(X3) != X4
| sk_c11 != multiply(X3,X4)
| sk_c11 != inverse(X2)
| multiply(X2,sk_c11) != X1
| sk_c10 != multiply(sk_c11,X1)
| sk_c11 != multiply(X0,sk_c10)
| inverse(X0) != sk_c11
| inverse(sk_c11) != sk_c10 ),
inference(reorient_equations,[],[f125]) ).
fof(f127,plain,
! [X2,X3,X0,X8,X6,X7,X4,X5] :
( sk_c10 != multiply(X8,sk_c11)
| sk_c10 != inverse(X8)
| sk_c10 != multiply(X7,sk_c11)
| inverse(X6) != X7
| sk_c10 != multiply(X6,X7)
| sk_c11 != multiply(X5,sk_c10)
| sk_c11 != inverse(X5)
| sk_c11 != multiply(X4,sk_c10)
| inverse(X3) != X4
| sk_c11 != multiply(X3,X4)
| sk_c11 != inverse(X2)
| sk_c10 != multiply(sk_c11,multiply(X2,sk_c11))
| sk_c11 != multiply(X0,sk_c10)
| inverse(X0) != sk_c11
| inverse(sk_c11) != sk_c10 ),
inference(equality_resolution,[],[f126]) ).
fof(f128,plain,
! [X2,X3,X0,X8,X6,X7,X5] :
( sk_c10 != multiply(X8,sk_c11)
| sk_c10 != inverse(X8)
| sk_c10 != multiply(X7,sk_c11)
| inverse(X6) != X7
| sk_c10 != multiply(X6,X7)
| sk_c11 != multiply(X5,sk_c10)
| sk_c11 != inverse(X5)
| sk_c11 != multiply(inverse(X3),sk_c10)
| sk_c11 != multiply(X3,inverse(X3))
| sk_c11 != inverse(X2)
| sk_c10 != multiply(sk_c11,multiply(X2,sk_c11))
| sk_c11 != multiply(X0,sk_c10)
| inverse(X0) != sk_c11
| inverse(sk_c11) != sk_c10 ),
inference(equality_resolution,[],[f127]) ).
fof(f129,plain,
! [X2,X3,X0,X8,X6,X5] :
( sk_c10 != multiply(X8,sk_c11)
| sk_c10 != inverse(X8)
| sk_c10 != multiply(inverse(X6),sk_c11)
| sk_c10 != multiply(X6,inverse(X6))
| sk_c11 != multiply(X5,sk_c10)
| sk_c11 != inverse(X5)
| sk_c11 != multiply(inverse(X3),sk_c10)
| sk_c11 != multiply(X3,inverse(X3))
| sk_c11 != inverse(X2)
| sk_c10 != multiply(sk_c11,multiply(X2,sk_c11))
| sk_c11 != multiply(X0,sk_c10)
| inverse(X0) != sk_c11
| inverse(sk_c11) != sk_c10 ),
inference(equality_resolution,[],[f128]) ).
tcf(c_113,plain,
! [X0: $i] : multiply(identity,X0) = X0,
inference(cnf_transformation,[],[f1]) ).
tcf(c_114,plain,
! [X0: $i] : multiply(inverse(X0),X0) = identity,
inference(cnf_transformation,[],[f3]) ).
tcf(c_115,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(multiply(X0,X1),X2) = multiply(X0,multiply(X1,X2)),
inference(cnf_transformation,[],[f4]) ).
tcf(c_116,negated_conjecture,
( ( inverse(sk_c11) = sk_c10 )
| ( multiply(sk_c4,sk_c5) = sk_c11 ) ),
inference(cnf_transformation,[],[f6]) ).
tcf(c_117,negated_conjecture,
( ( inverse(sk_c4) = sk_c5 )
| ( inverse(sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f8]) ).
tcf(c_120,negated_conjecture,
( ( inverse(sk_c11) = sk_c10 )
| ( multiply(sk_c6,sk_c10) = sk_c11 ) ),
inference(cnf_transformation,[],[f14]) ).
tcf(c_121,negated_conjecture,
( ( inverse(sk_c11) = sk_c10 )
| ( multiply(sk_c7,sk_c8) = sk_c10 ) ),
inference(cnf_transformation,[],[f16]) ).
tcf(c_122,negated_conjecture,
( ( inverse(sk_c7) = sk_c8 )
| ( inverse(sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f18]) ).
tcf(c_123,negated_conjecture,
( ( inverse(sk_c11) = sk_c10 )
| ( multiply(sk_c8,sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f20]) ).
tcf(c_124,negated_conjecture,
( ( inverse(sk_c9) = sk_c10 )
| ( inverse(sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f22]) ).
tcf(c_125,negated_conjecture,
( ( inverse(sk_c11) = sk_c10 )
| ( multiply(sk_c9,sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f24]) ).
tcf(c_126,negated_conjecture,
( ( inverse(sk_c1) = sk_c11 )
| ( multiply(sk_c4,sk_c5) = sk_c11 ) ),
inference(cnf_transformation,[],[f26]) ).
tcf(c_127,negated_conjecture,
( ( inverse(sk_c1) = sk_c11 )
| ( inverse(sk_c4) = sk_c5 ) ),
inference(cnf_transformation,[],[f28]) ).
tcf(c_128,negated_conjecture,
( ( inverse(sk_c1) = sk_c11 )
| ( multiply(sk_c5,sk_c10) = sk_c11 ) ),
inference(cnf_transformation,[],[f30]) ).
tcf(c_129,negated_conjecture,
( ( inverse(sk_c1) = sk_c11 )
| ( inverse(sk_c6) = sk_c11 ) ),
inference(cnf_transformation,[],[f32]) ).
tcf(c_130,negated_conjecture,
( ( inverse(sk_c1) = sk_c11 )
| ( multiply(sk_c6,sk_c10) = sk_c11 ) ),
inference(cnf_transformation,[],[f34]) ).
tcf(c_131,negated_conjecture,
( ( inverse(sk_c1) = sk_c11 )
| ( multiply(sk_c7,sk_c8) = sk_c10 ) ),
inference(cnf_transformation,[],[f36]) ).
tcf(c_132,negated_conjecture,
( ( inverse(sk_c1) = sk_c11 )
| ( inverse(sk_c7) = sk_c8 ) ),
inference(cnf_transformation,[],[f38]) ).
tcf(c_133,negated_conjecture,
( ( inverse(sk_c1) = sk_c11 )
| ( multiply(sk_c8,sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f40]) ).
tcf(c_134,negated_conjecture,
( ( inverse(sk_c1) = sk_c11 )
| ( inverse(sk_c9) = sk_c10 ) ),
inference(cnf_transformation,[],[f42]) ).
tcf(c_135,negated_conjecture,
( ( inverse(sk_c1) = sk_c11 )
| ( multiply(sk_c9,sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f44]) ).
tcf(c_136,negated_conjecture,
( ( multiply(sk_c1,sk_c10) = sk_c11 )
| ( multiply(sk_c4,sk_c5) = sk_c11 ) ),
inference(cnf_transformation,[],[f46]) ).
tcf(c_137,negated_conjecture,
( ( inverse(sk_c4) = sk_c5 )
| ( multiply(sk_c1,sk_c10) = sk_c11 ) ),
inference(cnf_transformation,[],[f48]) ).
tcf(c_138,negated_conjecture,
( ( multiply(sk_c1,sk_c10) = sk_c11 )
| ( multiply(sk_c5,sk_c10) = sk_c11 ) ),
inference(cnf_transformation,[],[f50]) ).
tcf(c_139,negated_conjecture,
( ( inverse(sk_c6) = sk_c11 )
| ( multiply(sk_c1,sk_c10) = sk_c11 ) ),
inference(cnf_transformation,[],[f52]) ).
tcf(c_140,negated_conjecture,
( ( multiply(sk_c1,sk_c10) = sk_c11 )
| ( multiply(sk_c6,sk_c10) = sk_c11 ) ),
inference(cnf_transformation,[],[f54]) ).
tcf(c_141,negated_conjecture,
( ( multiply(sk_c1,sk_c10) = sk_c11 )
| ( multiply(sk_c7,sk_c8) = sk_c10 ) ),
inference(cnf_transformation,[],[f56]) ).
tcf(c_142,negated_conjecture,
( ( inverse(sk_c7) = sk_c8 )
| ( multiply(sk_c1,sk_c10) = sk_c11 ) ),
inference(cnf_transformation,[],[f58]) ).
tcf(c_143,negated_conjecture,
( ( multiply(sk_c1,sk_c10) = sk_c11 )
| ( multiply(sk_c8,sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f60]) ).
tcf(c_144,negated_conjecture,
( ( inverse(sk_c9) = sk_c10 )
| ( multiply(sk_c1,sk_c10) = sk_c11 ) ),
inference(cnf_transformation,[],[f62]) ).
tcf(c_145,negated_conjecture,
( ( multiply(sk_c1,sk_c10) = sk_c11 )
| ( multiply(sk_c9,sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f64]) ).
tcf(c_146,negated_conjecture,
( ( multiply(sk_c4,sk_c5) = sk_c11 )
| ( multiply(sk_c11,sk_c3) = sk_c10 ) ),
inference(cnf_transformation,[],[f66]) ).
tcf(c_147,negated_conjecture,
( ( inverse(sk_c4) = sk_c5 )
| ( multiply(sk_c11,sk_c3) = sk_c10 ) ),
inference(cnf_transformation,[],[f68]) ).
tcf(c_151,negated_conjecture,
( ( multiply(sk_c7,sk_c8) = sk_c10 )
| ( multiply(sk_c11,sk_c3) = sk_c10 ) ),
inference(cnf_transformation,[],[f76]) ).
tcf(c_152,negated_conjecture,
( ( inverse(sk_c7) = sk_c8 )
| ( multiply(sk_c11,sk_c3) = sk_c10 ) ),
inference(cnf_transformation,[],[f78]) ).
tcf(c_154,negated_conjecture,
( ( inverse(sk_c9) = sk_c10 )
| ( multiply(sk_c11,sk_c3) = sk_c10 ) ),
inference(cnf_transformation,[],[f82]) ).
tcf(c_155,negated_conjecture,
( ( multiply(sk_c9,sk_c11) = sk_c10 )
| ( multiply(sk_c11,sk_c3) = sk_c10 ) ),
inference(cnf_transformation,[],[f84]) ).
tcf(c_156,negated_conjecture,
( ( multiply(sk_c2,sk_c11) = sk_c3 )
| ( multiply(sk_c4,sk_c5) = sk_c11 ) ),
inference(cnf_transformation,[],[f86]) ).
tcf(c_157,negated_conjecture,
( ( inverse(sk_c4) = sk_c5 )
| ( multiply(sk_c2,sk_c11) = sk_c3 ) ),
inference(cnf_transformation,[],[f88]) ).
tcf(c_161,negated_conjecture,
( ( multiply(sk_c2,sk_c11) = sk_c3 )
| ( multiply(sk_c7,sk_c8) = sk_c10 ) ),
inference(cnf_transformation,[],[f96]) ).
tcf(c_162,negated_conjecture,
( ( inverse(sk_c7) = sk_c8 )
| ( multiply(sk_c2,sk_c11) = sk_c3 ) ),
inference(cnf_transformation,[],[f98]) ).
tcf(c_163,negated_conjecture,
( ( multiply(sk_c2,sk_c11) = sk_c3 )
| ( multiply(sk_c8,sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f100]) ).
tcf(c_166,negated_conjecture,
( ( inverse(sk_c2) = sk_c11 )
| ( multiply(sk_c4,sk_c5) = sk_c11 ) ),
inference(cnf_transformation,[],[f106]) ).
tcf(c_167,negated_conjecture,
( ( inverse(sk_c2) = sk_c11 )
| ( inverse(sk_c4) = sk_c5 ) ),
inference(cnf_transformation,[],[f108]) ).
tcf(c_171,negated_conjecture,
( ( inverse(sk_c2) = sk_c11 )
| ( multiply(sk_c7,sk_c8) = sk_c10 ) ),
inference(cnf_transformation,[],[f116]) ).
tcf(c_172,negated_conjecture,
( ( inverse(sk_c2) = sk_c11 )
| ( inverse(sk_c7) = sk_c8 ) ),
inference(cnf_transformation,[],[f118]) ).
tcf(c_174,negated_conjecture,
( ( inverse(sk_c2) = sk_c11 )
| ( inverse(sk_c9) = sk_c10 ) ),
inference(cnf_transformation,[],[f122]) ).
tcf(c_175,negated_conjecture,
( ( inverse(sk_c2) = sk_c11 )
| ( multiply(sk_c9,sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f124]) ).
tcf(c_176,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( ( inverse(sk_c11) != sk_c10 )
| ( inverse(X5) != sk_c10 )
| ( inverse(X3) != sk_c11 )
| ( inverse(X2) != sk_c11 )
| ( inverse(X0) != sk_c11 )
| ( multiply(X5,sk_c11) != sk_c10 )
| ( multiply(X2,sk_c10) != sk_c11 )
| ( multiply(X0,sk_c10) != sk_c11 )
| ( multiply(inverse(X4),sk_c11) != sk_c10 )
| ( multiply(inverse(X1),sk_c10) != sk_c11 )
| ( multiply(X4,inverse(X4)) != sk_c10 )
| ( multiply(X1,inverse(X1)) != sk_c11 )
| ( multiply(sk_c11,multiply(X3,sk_c11)) != sk_c10 ) ),
inference(cnf_transformation,[],[f129]) ).
tcf(c_178,plain,
multiply(inverse(sk_c11),sk_c11) = identity,
inference(instantiation,[status(thm)],[c_114]) ).
tcf(c_721,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_10
| ( inverse(X0) != sk_c11 )
| ( multiply(X0,sk_c10) != sk_c11 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_10])],[c_176]) ).
tcf(c_722,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_11
| ( multiply(inverse(X0),sk_c11) != sk_c10 )
| ( multiply(X0,inverse(X0)) != sk_c10 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_11])],[c_176]) ).
tcf(c_723,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_12
| ( multiply(inverse(X0),sk_c10) != sk_c11 )
| ( multiply(X0,inverse(X0)) != sk_c11 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_12])],[c_176]) ).
tcf(c_724,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_13
| ( inverse(X0) != sk_c10 )
| ( multiply(X0,sk_c11) != sk_c10 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_13])],[c_176]) ).
tcf(c_725,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_14
| ( inverse(X0) != sk_c11 )
| ( multiply(sk_c11,multiply(X0,sk_c11)) != sk_c10 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_14])],[c_176]) ).
tcf(c_726,negated_conjecture,
( iPr_def_14
| iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( inverse(sk_c11) != sk_c10 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_176]) ).
tcf(c_727,definition,
iPr_def_15 = inverse(sk_c11),
introduced(definition,[new_symbols(definition,[iPr_def_15])],[]) ).
tcf(c_728,definition,
iPr_def_16 = multiply(sk_c9,sk_c11),
introduced(definition,[new_symbols(definition,[iPr_def_16])],[]) ).
tcf(c_729,definition,
iPr_def_17 = inverse(sk_c2),
introduced(definition,[new_symbols(definition,[iPr_def_17])],[]) ).
tcf(c_730,definition,
iPr_def_18 = inverse(sk_c9),
introduced(definition,[new_symbols(definition,[iPr_def_18])],[]) ).
tcf(c_731,definition,
iPr_def_19 = multiply(sk_c8,sk_c11),
introduced(definition,[new_symbols(definition,[iPr_def_19])],[]) ).
tcf(c_732,definition,
iPr_def_20 = inverse(sk_c7),
introduced(definition,[new_symbols(definition,[iPr_def_20])],[]) ).
tcf(c_733,definition,
iPr_def_21 = multiply(sk_c7,sk_c8),
introduced(definition,[new_symbols(definition,[iPr_def_21])],[]) ).
tcf(c_734,definition,
iPr_def_22 = multiply(sk_c6,sk_c10),
introduced(definition,[new_symbols(definition,[iPr_def_22])],[]) ).
tcf(c_735,definition,
iPr_def_23 = inverse(sk_c6),
introduced(definition,[new_symbols(definition,[iPr_def_23])],[]) ).
tcf(c_737,definition,
iPr_def_25 = inverse(sk_c4),
introduced(definition,[new_symbols(definition,[iPr_def_25])],[]) ).
tcf(c_738,definition,
iPr_def_26 = multiply(sk_c4,sk_c5),
introduced(definition,[new_symbols(definition,[iPr_def_26])],[]) ).
tcf(c_739,definition,
iPr_def_27 = multiply(sk_c2,sk_c11),
introduced(definition,[new_symbols(definition,[iPr_def_27])],[]) ).
tcf(c_740,definition,
iPr_def_28 = multiply(sk_c11,sk_c3),
introduced(definition,[new_symbols(definition,[iPr_def_28])],[]) ).
tcf(c_741,definition,
iPr_def_29 = multiply(sk_c1,sk_c10),
introduced(definition,[new_symbols(definition,[iPr_def_29])],[]) ).
tcf(c_742,definition,
iPr_def_30 = inverse(sk_c1),
introduced(definition,[new_symbols(definition,[iPr_def_30])],[]) ).
tcf(c_743,negated_conjecture,
( iPr_def_14
| iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( iPr_def_15 != sk_c10 ) ),
inference(demodulation,[status(thm)],[c_726,c_727]) ).
tcf(c_744,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_14
| ( inverse(X0) != sk_c11 )
| ( multiply(sk_c11,multiply(X0,sk_c11)) != sk_c10 ) ),
inference(demodulation,[status(thm)],[c_725]) ).
tcf(c_745,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_13
| ( inverse(X0) != sk_c10 )
| ( multiply(X0,sk_c11) != sk_c10 ) ),
inference(demodulation,[status(thm)],[c_724]) ).
tcf(c_746,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_12
| ( multiply(inverse(X0),sk_c10) != sk_c11 )
| ( multiply(X0,inverse(X0)) != sk_c11 ) ),
inference(demodulation,[status(thm)],[c_723]) ).
tcf(c_748,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_11
| ( multiply(inverse(X0),sk_c11) != sk_c10 )
| ( multiply(X0,inverse(X0)) != sk_c10 ) ),
inference(demodulation,[status(thm)],[c_722]) ).
tcf(c_749,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_10
| ( inverse(X0) != sk_c11 )
| ( multiply(X0,sk_c10) != sk_c11 ) ),
inference(demodulation,[status(thm)],[c_721]) ).
tcf(c_750,negated_conjecture,
( ( iPr_def_17 = sk_c11 )
| ( iPr_def_16 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_175,c_729,c_728]) ).
tcf(c_751,negated_conjecture,
( ( iPr_def_18 = sk_c10 )
| ( iPr_def_17 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_174,c_730]) ).
tcf(c_753,negated_conjecture,
( ( iPr_def_20 = sk_c8 )
| ( iPr_def_17 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_172,c_732]) ).
tcf(c_754,negated_conjecture,
( ( iPr_def_21 = sk_c10 )
| ( iPr_def_17 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_171,c_733]) ).
tcf(c_758,negated_conjecture,
( ( iPr_def_25 = sk_c5 )
| ( iPr_def_17 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_167,c_737]) ).
tcf(c_759,negated_conjecture,
( ( iPr_def_26 = sk_c11 )
| ( iPr_def_17 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_166,c_738]) ).
tcf(c_762,negated_conjecture,
( ( iPr_def_27 = sk_c3 )
| ( iPr_def_19 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_163]) ).
tcf(c_763,negated_conjecture,
( ( iPr_def_27 = sk_c3 )
| ( iPr_def_20 = sk_c8 ) ),
inference(demodulation,[status(thm)],[c_162]) ).
tcf(c_764,negated_conjecture,
( ( iPr_def_27 = sk_c3 )
| ( iPr_def_21 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_161]) ).
tcf(c_768,negated_conjecture,
( ( iPr_def_27 = sk_c3 )
| ( iPr_def_25 = sk_c5 ) ),
inference(demodulation,[status(thm)],[c_157]) ).
tcf(c_769,negated_conjecture,
( ( iPr_def_27 = sk_c3 )
| ( iPr_def_26 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_156]) ).
tcf(c_770,negated_conjecture,
( ( iPr_def_28 = sk_c10 )
| ( iPr_def_16 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_155,c_740]) ).
tcf(c_771,negated_conjecture,
( ( iPr_def_28 = sk_c10 )
| ( iPr_def_18 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_154]) ).
tcf(c_773,negated_conjecture,
( ( iPr_def_28 = sk_c10 )
| ( iPr_def_20 = sk_c8 ) ),
inference(demodulation,[status(thm)],[c_152]) ).
tcf(c_774,negated_conjecture,
( ( iPr_def_28 = sk_c10 )
| ( iPr_def_21 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_151]) ).
tcf(c_778,negated_conjecture,
( ( iPr_def_28 = sk_c10 )
| ( iPr_def_25 = sk_c5 ) ),
inference(demodulation,[status(thm)],[c_147]) ).
tcf(c_779,negated_conjecture,
( ( iPr_def_28 = sk_c10 )
| ( iPr_def_26 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_146]) ).
tcf(c_780,negated_conjecture,
( ( iPr_def_29 = sk_c11 )
| ( iPr_def_16 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_145,c_741]) ).
tcf(c_781,negated_conjecture,
( ( iPr_def_29 = sk_c11 )
| ( iPr_def_18 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_144]) ).
tcf(c_782,negated_conjecture,
( ( iPr_def_29 = sk_c11 )
| ( iPr_def_19 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_143]) ).
tcf(c_783,negated_conjecture,
( ( iPr_def_29 = sk_c11 )
| ( iPr_def_20 = sk_c8 ) ),
inference(demodulation,[status(thm)],[c_142]) ).
tcf(c_784,negated_conjecture,
( ( iPr_def_29 = sk_c11 )
| ( iPr_def_21 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_141]) ).
tcf(c_785,negated_conjecture,
( ( iPr_def_29 = sk_c11 )
| ( iPr_def_22 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_140]) ).
tcf(c_786,negated_conjecture,
( ( iPr_def_29 = sk_c11 )
| ( iPr_def_23 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_139]) ).
tcf(c_787,negated_conjecture,
( ( iPr_def_29 = sk_c11 )
| ( iPr_def_24 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_138]) ).
tcf(c_788,negated_conjecture,
( ( iPr_def_29 = sk_c11 )
| ( iPr_def_25 = sk_c5 ) ),
inference(demodulation,[status(thm)],[c_137]) ).
tcf(c_789,negated_conjecture,
( ( iPr_def_29 = sk_c11 )
| ( iPr_def_26 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_136]) ).
tcf(c_790,negated_conjecture,
( ( iPr_def_30 = sk_c11 )
| ( iPr_def_16 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_135,c_742]) ).
tcf(c_791,negated_conjecture,
( ( iPr_def_30 = sk_c11 )
| ( iPr_def_18 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_134]) ).
tcf(c_792,negated_conjecture,
( ( iPr_def_30 = sk_c11 )
| ( iPr_def_19 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_133]) ).
tcf(c_793,negated_conjecture,
( ( iPr_def_30 = sk_c11 )
| ( iPr_def_20 = sk_c8 ) ),
inference(demodulation,[status(thm)],[c_132]) ).
tcf(c_794,negated_conjecture,
( ( iPr_def_30 = sk_c11 )
| ( iPr_def_21 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_131]) ).
tcf(c_795,negated_conjecture,
( ( iPr_def_30 = sk_c11 )
| ( iPr_def_22 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_130]) ).
tcf(c_796,negated_conjecture,
( ( iPr_def_30 = sk_c11 )
| ( iPr_def_23 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_129]) ).
tcf(c_797,negated_conjecture,
( ( iPr_def_30 = sk_c11 )
| ( iPr_def_24 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_128]) ).
tcf(c_798,negated_conjecture,
( ( iPr_def_30 = sk_c11 )
| ( iPr_def_25 = sk_c5 ) ),
inference(demodulation,[status(thm)],[c_127]) ).
tcf(c_799,negated_conjecture,
( ( iPr_def_30 = sk_c11 )
| ( iPr_def_26 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_126]) ).
tcf(c_800,negated_conjecture,
( ( iPr_def_16 = sk_c10 )
| ( iPr_def_15 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_125]) ).
tcf(c_801,negated_conjecture,
( ( iPr_def_18 = sk_c10 )
| ( iPr_def_15 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_124]) ).
tcf(c_802,negated_conjecture,
( ( iPr_def_19 = sk_c10 )
| ( iPr_def_15 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_123]) ).
tcf(c_803,negated_conjecture,
( ( iPr_def_20 = sk_c8 )
| ( iPr_def_15 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_122]) ).
tcf(c_804,negated_conjecture,
( ( iPr_def_21 = sk_c10 )
| ( iPr_def_15 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_121]) ).
tcf(c_805,negated_conjecture,
( ( iPr_def_22 = sk_c11 )
| ( iPr_def_15 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_120]) ).
tcf(c_808,negated_conjecture,
( ( iPr_def_25 = sk_c5 )
| ( iPr_def_15 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_117]) ).
tcf(c_809,negated_conjecture,
( ( iPr_def_26 = sk_c11 )
| ( iPr_def_15 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_116]) ).
tcf(c_810,plain,
! [X0: $i] : X0 = X0,
theory(equality) ).
tcf(c_811,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = X0 )
| ( X2 != X1 )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_812,plain,
! [X0: $i,X1: $i] :
( ( inverse(X0) = inverse(X1) )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_813,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( multiply(X0,X2) = multiply(X1,X3) )
| ( X2 != X3 )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_814,plain,
( ( inverse(sk_c11) = inverse(sk_c11) )
| ( sk_c11 != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_812]) ).
tcf(c_816,plain,
sk_c11 = sk_c11,
inference(instantiation,[status(thm)],[c_810]) ).
tcf(c_818,plain,
( ~ iPr_def_11
| ( multiply(sk_c11,inverse(sk_c11)) != sk_c10 )
| ( multiply(inverse(sk_c11),sk_c11) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_748]) ).
tcf(c_820,plain,
( ~ iPr_def_13
| ( inverse(sk_c11) != sk_c10 )
| ( multiply(sk_c11,sk_c11) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_745]) ).
tcf(c_1195,plain,
( ( iPr_def_16 = iPr_def_21 )
| ( sk_c11 = iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_754,c_750]) ).
tcf(c_1256,plain,
( ( sk_c11 = iPr_def_17 )
| ( inverse(iPr_def_26) = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_759,c_727]) ).
tcf(c_1312,plain,
( ( sk_c3 = iPr_def_27 )
| ( multiply(sk_c7,iPr_def_20) = iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_763,c_733]) ).
tcf(c_1313,plain,
( ( sk_c11 = iPr_def_17 )
| ( multiply(sk_c7,iPr_def_20) = iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_753,c_733]) ).
tcf(c_1318,plain,
( ( sk_c11 = iPr_def_17 )
| ( multiply(sk_c6,iPr_def_21) = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_754,c_734]) ).
tcf(c_1320,plain,
( ( sk_c11 = iPr_def_17 )
| ( multiply(sk_c6,iPr_def_18) = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_751,c_734]) ).
tcf(c_1321,plain,
( ( sk_c11 = iPr_def_17 )
| ( multiply(sk_c6,iPr_def_16) = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_750,c_734]) ).
tcf(c_1345,plain,
( ( sk_c11 = iPr_def_17 )
| ( multiply(sk_c4,iPr_def_25) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_758,c_738]) ).
tcf(c_1365,plain,
( ( sk_c10 = iPr_def_21 )
| ( multiply(sk_c11,iPr_def_27) = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_764,c_740]) ).
tcf(c_1366,plain,
( ( sk_c10 = iPr_def_19 )
| ( multiply(sk_c11,iPr_def_27) = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_762,c_740]) ).
tcf(c_1399,plain,
multiply(iPr_def_15,sk_c11) = identity,
inference(superposition,[status(thm)],[c_727,c_114]) ).
tcf(c_1400,plain,
multiply(iPr_def_25,sk_c4) = identity,
inference(superposition,[status(thm)],[c_737,c_114]) ).
tcf(c_1401,plain,
multiply(iPr_def_23,sk_c6) = identity,
inference(superposition,[status(thm)],[c_735,c_114]) ).
tcf(c_1402,plain,
multiply(iPr_def_20,sk_c7) = identity,
inference(superposition,[status(thm)],[c_732,c_114]) ).
tcf(c_1403,plain,
multiply(iPr_def_18,sk_c9) = identity,
inference(superposition,[status(thm)],[c_730,c_114]) ).
tcf(c_1404,plain,
multiply(iPr_def_30,sk_c1) = identity,
inference(superposition,[status(thm)],[c_742,c_114]) ).
tcf(c_1405,plain,
multiply(iPr_def_17,sk_c2) = identity,
inference(superposition,[status(thm)],[c_729,c_114]) ).
tcf(c_1424,plain,
( ( sk_c3 = iPr_def_27 )
| ( multiply(sk_c4,iPr_def_25) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_768,c_738]) ).
tcf(c_1434,plain,
( ( sk_c11 = iPr_def_26 )
| ( multiply(sk_c11,iPr_def_27) = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_769,c_740]) ).
tcf(c_1470,plain,
! [X0: $i] :
( ( iPr_def_15 = sk_c10 )
| ( iPr_def_15 != X0 )
| ( sk_c10 != X0 ) ),
inference(instantiation,[status(thm)],[c_811]) ).
tcf(c_1471,plain,
( ( iPr_def_15 = sk_c10 )
| ( iPr_def_15 != sk_c11 )
| ( sk_c10 != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_1470]) ).
tcf(c_1473,plain,
! [X0: $i,X1: $i] :
( ( sk_c10 = X0 )
| ( sk_c10 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_811]) ).
tcf(c_1474,plain,
! [X0: $i] :
( ( sk_c10 = X0 )
| ( sk_c10 != sk_c10 )
| ( X0 != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_1473]) ).
tcf(c_1475,plain,
sk_c10 = sk_c10,
inference(instantiation,[status(thm)],[c_810]) ).
tcf(c_1516,plain,
! [X0: $i,X1: $i] :
( ( X0 = sk_c10 )
| ( sk_c10 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_811]) ).
tcf(c_1518,plain,
( ( sk_c10 = iPr_def_16 )
| ( iPr_def_16 != sk_c10 )
| ( sk_c10 != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_1474]) ).
tcf(c_1519,plain,
( ( sk_c10 = iPr_def_18 )
| ( iPr_def_18 != sk_c10 )
| ( sk_c10 != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_1474]) ).
tcf(c_1521,plain,
( ( sk_c10 = iPr_def_21 )
| ( iPr_def_21 != sk_c10 )
| ( sk_c10 != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_1474]) ).
tcf(c_1557,plain,
! [X0: $i] :
( ( sk_c10 = X0 )
| ( sk_c10 != iPr_def_16 )
| ( X0 != iPr_def_16 ) ),
inference(instantiation,[status(thm)],[c_1473]) ).
tcf(c_1563,plain,
( ( sk_c10 = iPr_def_28 )
| ( multiply(sk_c7,iPr_def_20) = iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_773,c_733]) ).
tcf(c_1603,plain,
! [X0: $i] :
( ( sk_c10 = X0 )
| ( sk_c10 != iPr_def_18 )
| ( X0 != iPr_def_18 ) ),
inference(instantiation,[status(thm)],[c_1473]) ).
tcf(c_1609,plain,
! [X0: $i] :
( ( sk_c10 = X0 )
| ( sk_c10 != iPr_def_21 )
| ( X0 != iPr_def_21 ) ),
inference(instantiation,[status(thm)],[c_1473]) ).
tcf(c_1610,plain,
( ( sk_c10 = sk_c11 )
| ( sk_c10 != iPr_def_21 )
| ( sk_c11 != iPr_def_21 ) ),
inference(instantiation,[status(thm)],[c_1609]) ).
tcf(c_1650,plain,
! [X0: $i] :
( ( X0 = sk_c10 )
| ( sk_c10 != iPr_def_21 )
| ( X0 != iPr_def_21 ) ),
inference(instantiation,[status(thm)],[c_1516]) ).
tcf(c_1651,plain,
( ( sk_c11 = sk_c10 )
| ( sk_c10 != iPr_def_21 )
| ( sk_c11 != iPr_def_21 ) ),
inference(instantiation,[status(thm)],[c_1650]) ).
tcf(c_1652,plain,
! [X0: $i] :
( ( X0 = sk_c10 )
| ( sk_c10 != iPr_def_19 )
| ( X0 != iPr_def_19 ) ),
inference(instantiation,[status(thm)],[c_1516]) ).
tcf(c_1654,plain,
! [X0: $i] :
( ( X0 = sk_c10 )
| ( sk_c10 != iPr_def_18 )
| ( X0 != iPr_def_18 ) ),
inference(instantiation,[status(thm)],[c_1516]) ).
tcf(c_1656,plain,
! [X0: $i] :
( ( X0 = sk_c10 )
| ( sk_c10 != iPr_def_16 )
| ( X0 != iPr_def_16 ) ),
inference(instantiation,[status(thm)],[c_1516]) ).
tcf(c_1657,plain,
( ( sk_c11 = sk_c10 )
| ( sk_c10 != iPr_def_16 )
| ( sk_c11 != iPr_def_16 ) ),
inference(instantiation,[status(thm)],[c_1656]) ).
tcf(c_1740,plain,
! [X0: $i,X1: $i] :
( ( X0 = iPr_def_16 )
| ( iPr_def_16 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_811]) ).
tcf(c_1747,plain,
( ( sk_c10 = iPr_def_28 )
| ( multiply(sk_c4,iPr_def_25) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_778,c_738]) ).
tcf(c_1768,plain,
! [X0: $i,X1: $i] :
( ( X0 = iPr_def_18 )
| ( iPr_def_18 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_811]) ).
tcf(c_1779,plain,
( ( sk_c11 = iPr_def_26 )
| ( multiply(sk_c1,iPr_def_28) = iPr_def_29 ) ),
inference(superposition,[status(thm)],[c_779,c_741]) ).
tcf(c_1810,plain,
( ( sk_c10 = multiply(identity,iPr_def_21) )
| ( sk_c10 != iPr_def_21 )
| ( multiply(identity,iPr_def_21) != iPr_def_21 ) ),
inference(instantiation,[status(thm)],[c_1609]) ).
tcf(c_1811,plain,
multiply(identity,iPr_def_21) = iPr_def_21,
inference(instantiation,[status(thm)],[c_113]) ).
tcf(c_1813,plain,
! [X0: $i,X1: $i] :
( ( X0 = iPr_def_21 )
| ( iPr_def_21 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_811]) ).
tcf(c_1887,plain,
iPr_def_21 = iPr_def_21,
inference(instantiation,[status(thm)],[c_810]) ).
tcf(c_1892,plain,
( ( iPr_def_19 = sk_c10 )
| ( iPr_def_19 != iPr_def_19 )
| ( sk_c10 != iPr_def_19 ) ),
inference(instantiation,[status(thm)],[c_1652]) ).
tcf(c_1893,plain,
iPr_def_19 = iPr_def_19,
inference(instantiation,[status(thm)],[c_810]) ).
tcf(c_1899,plain,
iPr_def_18 = iPr_def_18,
inference(instantiation,[status(thm)],[c_810]) ).
tcf(c_1905,plain,
iPr_def_16 = iPr_def_16,
inference(instantiation,[status(thm)],[c_810]) ).
tcf(c_1924,plain,
( ( iPr_def_16 = iPr_def_18 )
| ( sk_c11 = iPr_def_29 ) ),
inference(superposition,[status(thm)],[c_781,c_780]) ).
tcf(c_2018,plain,
( ( iPr_def_18 = iPr_def_19 )
| ( sk_c11 = iPr_def_29 ) ),
inference(superposition,[status(thm)],[c_782,c_781]) ).
tcf(c_2094,plain,
( ( sk_c11 = iPr_def_29 )
| ( multiply(sk_c7,iPr_def_20) = iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_783,c_733]) ).
tcf(c_2119,plain,
( ( iPr_def_18 = iPr_def_21 )
| ( sk_c11 = iPr_def_29 ) ),
inference(superposition,[status(thm)],[c_784,c_781]) ).
tcf(c_2120,plain,
( ( iPr_def_16 = iPr_def_21 )
| ( sk_c11 = iPr_def_29 ) ),
inference(superposition,[status(thm)],[c_784,c_780]) ).
tcf(c_2187,plain,
! [X0: $i,X1: $i] :
( ( iPr_def_15 = X0 )
| ( iPr_def_15 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_811]) ).
tcf(c_2209,plain,
( ( sk_c11 = iPr_def_22 )
| ( multiply(sk_c2,iPr_def_29) = iPr_def_27 ) ),
inference(superposition,[status(thm)],[c_785,c_739]) ).
tcf(c_2250,plain,
! [X0: $i,X1: $i] :
( ( iPr_def_16 = X0 )
| ( iPr_def_16 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_811]) ).
tcf(c_2257,plain,
! [X0: $i,X1: $i] :
( ( iPr_def_18 = X0 )
| ( iPr_def_18 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_811]) ).
tcf(c_2273,plain,
( ( sk_c11 = iPr_def_23 )
| ( multiply(sk_c2,iPr_def_29) = iPr_def_27 ) ),
inference(superposition,[status(thm)],[c_786,c_739]) ).
tcf(c_2316,plain,
( ( sk_c10 = iPr_def_15 )
| ( iPr_def_15 != sk_c10 )
| ( sk_c10 != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_1474]) ).
tcf(c_2321,plain,
( ( sk_c11 = iPr_def_29 )
| ( multiply(sk_c4,iPr_def_25) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_788,c_738]) ).
tcf(c_2374,plain,
! [X0: $i,X1: $i] :
( ( iPr_def_21 = X0 )
| ( iPr_def_21 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_811]) ).
tcf(c_2377,plain,
! [X0: $i] :
( ( X0 = iPr_def_21 )
| ( iPr_def_21 != sk_c10 )
| ( X0 != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_1813]) ).
tcf(c_2531,plain,
identity = identity,
inference(instantiation,[status(thm)],[c_810]) ).
tcf(c_2533,plain,
! [X0: $i,X1: $i] :
( ( X0 = identity )
| ( identity != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_811]) ).
tcf(c_2544,plain,
! [X0: $i] : inverse(X0) = inverse(X0),
inference(instantiation,[status(thm)],[c_810]) ).
tcf(c_2547,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( inverse(X0) = X2 )
| ( X2 != X1 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_811]) ).
tcf(c_2581,plain,
( ( iPr_def_16 = iPr_def_18 )
| ( sk_c11 = iPr_def_30 ) ),
inference(superposition,[status(thm)],[c_791,c_790]) ).
tcf(c_2661,plain,
( ( iPr_def_19 = iPr_def_21 )
| ( iPr_def_21 != sk_c10 )
| ( iPr_def_19 != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_2377]) ).
tcf(c_2705,plain,
( ( iPr_def_18 = iPr_def_19 )
| ( sk_c11 = iPr_def_30 ) ),
inference(superposition,[status(thm)],[c_792,c_791]) ).
tcf(c_2820,plain,
! [X0: $i] :
( ( sk_c10 = X0 )
| ( sk_c10 != iPr_def_28 )
| ( X0 != iPr_def_28 ) ),
inference(instantiation,[status(thm)],[c_1473]) ).
tcf(c_2821,plain,
( ( sk_c10 = sk_c11 )
| ( sk_c10 != iPr_def_28 )
| ( sk_c11 != iPr_def_28 ) ),
inference(instantiation,[status(thm)],[c_2820]) ).
tcf(c_2827,plain,
( ( sk_c11 = iPr_def_30 )
| ( multiply(sk_c7,iPr_def_20) = iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_793,c_733]) ).
tcf(c_2859,plain,
( ( iPr_def_18 = iPr_def_21 )
| ( sk_c11 = iPr_def_30 ) ),
inference(superposition,[status(thm)],[c_794,c_791]) ).
tcf(c_2860,plain,
( ( iPr_def_16 = iPr_def_21 )
| ( sk_c11 = iPr_def_30 ) ),
inference(superposition,[status(thm)],[c_794,c_790]) ).
tcf(c_2970,plain,
! [X0: $i] :
( ( X0 = sk_c10 )
| ( sk_c10 != iPr_def_15 )
| ( X0 != iPr_def_15 ) ),
inference(instantiation,[status(thm)],[c_1516]) ).
tcf(c_2971,plain,
! [X0: $i] :
( ( sk_c10 = X0 )
| ( sk_c10 != iPr_def_15 )
| ( X0 != iPr_def_15 ) ),
inference(instantiation,[status(thm)],[c_1473]) ).
tcf(c_2998,plain,
( ( iPr_def_29 = iPr_def_30 )
| ( sk_c11 = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_795,c_785]) ).
tcf(c_3001,plain,
( ( sk_c11 = iPr_def_22 )
| ( multiply(sk_c2,iPr_def_30) = iPr_def_27 ) ),
inference(superposition,[status(thm)],[c_795,c_739]) ).
tcf(c_3103,plain,
( ( iPr_def_29 = iPr_def_30 )
| ( sk_c11 = iPr_def_23 ) ),
inference(superposition,[status(thm)],[c_796,c_786]) ).
tcf(c_3107,plain,
( ( sk_c11 = iPr_def_23 )
| ( multiply(sk_c2,iPr_def_30) = iPr_def_27 ) ),
inference(superposition,[status(thm)],[c_796,c_739]) ).
tcf(c_3200,plain,
( ( iPr_def_29 = iPr_def_30 )
| ( sk_c11 = iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_797,c_787]) ).
tcf(c_3266,plain,
( ( sk_c11 = iPr_def_30 )
| ( multiply(sk_c4,iPr_def_25) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_798,c_738]) ).
tcf(c_3284,plain,
( ( iPr_def_29 = iPr_def_30 )
| ( sk_c11 = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_799,c_789]) ).
tcf(c_3294,plain,
( ( sk_c11 = iPr_def_26 )
| ( inverse(iPr_def_30) = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_799,c_727]) ).
tcf(c_3372,plain,
! [X0: $i,X1: $i] :
( ( multiply(X0,X1) = multiply(identity,iPr_def_21) )
| ( X1 != iPr_def_21 )
| ( X0 != identity ) ),
inference(instantiation,[status(thm)],[c_813]) ).
tcf(c_3374,plain,
( ( multiply(sk_c11,sk_c11) = multiply(identity,iPr_def_21) )
| ( sk_c11 != iPr_def_21 )
| ( sk_c11 != identity ) ),
inference(instantiation,[status(thm)],[c_3372]) ).
tcf(c_3558,plain,
( ( iPr_def_16 = iPr_def_18 )
| ( sk_c10 = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_801,c_800]) ).
tcf(c_3687,plain,
( ( iPr_def_18 = iPr_def_19 )
| ( sk_c10 = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_802,c_801]) ).
tcf(c_3793,plain,
( ( sk_c10 = iPr_def_15 )
| ( multiply(sk_c7,iPr_def_20) = iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_803,c_733]) ).
tcf(c_3825,plain,
( ( iPr_def_16 = iPr_def_21 )
| ( sk_c10 = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_804,c_800]) ).
tcf(c_3840,plain,
( ( sk_c10 = iPr_def_15 )
| ( multiply(sk_c1,iPr_def_21) = iPr_def_29 ) ),
inference(superposition,[status(thm)],[c_804,c_741]) ).
tcf(c_3954,plain,
( ( iPr_def_15 = iPr_def_28 )
| ( sk_c10 = iPr_def_21 )
| ( sk_c11 = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_805,c_774]) ).
tcf(c_3956,plain,
( ( iPr_def_15 = iPr_def_28 )
| ( sk_c10 = iPr_def_18 )
| ( sk_c11 = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_805,c_771]) ).
tcf(c_3957,plain,
( ( iPr_def_15 = iPr_def_28 )
| ( sk_c10 = iPr_def_16 )
| ( sk_c11 = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_805,c_770]) ).
tcf(c_4058,plain,
! [X0: $i] :
( ( iPr_def_15 = X0 )
| ( iPr_def_15 != sk_c10 )
| ( X0 != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_2187]) ).
tcf(c_4098,plain,
! [X0: $i] :
( ( iPr_def_16 = X0 )
| ( iPr_def_16 != iPr_def_16 )
| ( X0 != iPr_def_16 ) ),
inference(instantiation,[status(thm)],[c_2250]) ).
tcf(c_4105,plain,
! [X0: $i] :
( ( iPr_def_18 = X0 )
| ( iPr_def_18 != iPr_def_18 )
| ( X0 != iPr_def_18 ) ),
inference(instantiation,[status(thm)],[c_2257]) ).
tcf(c_4250,plain,
! [X0: $i] :
( ( iPr_def_21 = X0 )
| ( iPr_def_21 != iPr_def_21 )
| ( X0 != iPr_def_21 ) ),
inference(instantiation,[status(thm)],[c_2374]) ).
tcf(c_4443,plain,
! [X0: $i,X1: $i] :
( ( identity = X0 )
| ( identity != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_811]) ).
tcf(c_4459,plain,
( ( sk_c10 = iPr_def_15 )
| ( multiply(sk_c4,iPr_def_25) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_808,c_738]) ).
tcf(c_4518,plain,
( ( iPr_def_15 = iPr_def_28 )
| ( sk_c11 = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_809,c_779]) ).
tcf(c_4945,plain,
! [X0: $i] :
( ( iPr_def_16 = X0 )
| ( iPr_def_16 != iPr_def_18 )
| ( X0 != iPr_def_18 ) ),
inference(instantiation,[status(thm)],[c_2250]) ).
tcf(c_4964,plain,
( ~ iPr_def_13
| ( sk_c10 != iPr_def_16 )
| ( inverse(sk_c9) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_728,c_745]) ).
tcf(c_4991,plain,
( ~ iPr_def_13
| ( sk_c10 != iPr_def_18 )
| ( sk_c10 != iPr_def_16 ) ),
inference(light_normalisation,[status(thm)],[c_4964,c_730]) ).
tcf(c_5061,plain,
! [X0: $i] :
( ( iPr_def_18 = X0 )
| ( iPr_def_18 != iPr_def_21 )
| ( X0 != iPr_def_21 ) ),
inference(instantiation,[status(thm)],[c_2257]) ).
tcf(c_5064,plain,
( ( iPr_def_18 = sk_c11 )
| ( iPr_def_18 != iPr_def_21 )
| ( sk_c11 != iPr_def_21 ) ),
inference(instantiation,[status(thm)],[c_5061]) ).
tcf(c_5114,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( inverse(X0) = X2 )
| ( X2 != inverse(X1) )
| ( inverse(X0) != inverse(X1) ) ),
inference(instantiation,[status(thm)],[c_2547]) ).
tcf(c_5126,plain,
( ~ iPr_def_10
| ( sk_c11 != iPr_def_22 )
| ( inverse(sk_c6) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_734,c_749]) ).
tcf(c_5127,plain,
( ~ iPr_def_10
| ( sk_c11 != iPr_def_29 )
| ( inverse(sk_c1) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_741,c_749]) ).
tcf(c_5161,plain,
( ~ iPr_def_10
| ( sk_c11 != iPr_def_30 )
| ( sk_c11 != iPr_def_29 ) ),
inference(light_normalisation,[status(thm)],[c_5127,c_742]) ).
tcf(c_5165,plain,
( ~ iPr_def_10
| ( sk_c11 != iPr_def_23 )
| ( sk_c11 != iPr_def_22 ) ),
inference(light_normalisation,[status(thm)],[c_5126,c_735]) ).
tcf(c_5333,plain,
( ( iPr_def_15 = iPr_def_28 )
| ( iPr_def_28 != sk_c10 )
| ( iPr_def_15 != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_4058]) ).
tcf(c_5399,plain,
( ( sk_c10 = iPr_def_15 )
| ( iPr_def_15 != iPr_def_18 )
| ( sk_c10 != iPr_def_18 ) ),
inference(instantiation,[status(thm)],[c_1603]) ).
tcf(c_5422,plain,
( ~ iPr_def_14
| ( inverse(sk_c2) != sk_c11 )
| ( multiply(sk_c11,iPr_def_27) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_739,c_744]) ).
tcf(c_5444,plain,
( ~ iPr_def_14
| ( sk_c11 != iPr_def_17 )
| ( multiply(sk_c11,iPr_def_27) != sk_c10 ) ),
inference(light_normalisation,[status(thm)],[c_5422,c_729]) ).
tcf(c_5586,plain,
! [X0: $i,X1: $i] :
( ( sk_c11 = inverse(X0) )
| ( sk_c11 != X1 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_811]) ).
tcf(c_5638,plain,
multiply(identity,iPr_def_28) = iPr_def_28,
inference(instantiation,[status(thm)],[c_113]) ).
tcf(c_5640,plain,
iPr_def_28 = iPr_def_28,
inference(instantiation,[status(thm)],[c_810]) ).
tcf(c_5641,plain,
! [X0: $i,X1: $i] :
( ( X0 = iPr_def_28 )
| ( iPr_def_28 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_811]) ).
tcf(c_5705,plain,
multiply(identity,iPr_def_15) = iPr_def_15,
inference(instantiation,[status(thm)],[c_113]) ).
tcf(c_5707,plain,
! [X0: $i,X1: $i] :
( ( X0 = iPr_def_15 )
| ( iPr_def_15 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_811]) ).
tcf(c_6161,plain,
! [X0: $i] : multiply(sk_c7,multiply(sk_c8,X0)) = multiply(iPr_def_21,X0),
inference(superposition,[status(thm)],[c_733,c_115]) ).
tcf(c_6163,plain,
! [X0: $i] : multiply(sk_c9,multiply(sk_c11,X0)) = multiply(iPr_def_16,X0),
inference(superposition,[status(thm)],[c_728,c_115]) ).
tcf(c_6168,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(X0,X1)) = multiply(identity,X1),
inference(superposition,[status(thm)],[c_114,c_115]) ).
tcf(c_6170,plain,
! [X0: $i] : multiply(iPr_def_15,multiply(sk_c11,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1399,c_115]) ).
tcf(c_6171,plain,
! [X0: $i] : multiply(iPr_def_25,multiply(sk_c4,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1400,c_115]) ).
tcf(c_6172,plain,
! [X0: $i] : multiply(iPr_def_23,multiply(sk_c6,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1401,c_115]) ).
tcf(c_6173,plain,
! [X0: $i] : multiply(iPr_def_20,multiply(sk_c7,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1402,c_115]) ).
tcf(c_6174,plain,
! [X0: $i] : multiply(iPr_def_18,multiply(sk_c9,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1403,c_115]) ).
tcf(c_6175,plain,
! [X0: $i] : multiply(iPr_def_30,multiply(sk_c1,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1404,c_115]) ).
tcf(c_6176,plain,
! [X0: $i] : multiply(iPr_def_17,multiply(sk_c2,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1405,c_115]) ).
tcf(c_6183,plain,
! [X0: $i] : multiply(iPr_def_17,multiply(sk_c2,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_6176,c_113]) ).
tcf(c_6184,plain,
! [X0: $i] : multiply(iPr_def_30,multiply(sk_c1,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_6175,c_113]) ).
tcf(c_6185,plain,
! [X0: $i] : multiply(iPr_def_18,multiply(sk_c9,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_6174,c_113]) ).
tcf(c_6186,plain,
! [X0: $i] : multiply(iPr_def_20,multiply(sk_c7,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_6173,c_113]) ).
tcf(c_6187,plain,
! [X0: $i] : multiply(iPr_def_23,multiply(sk_c6,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_6172,c_113]) ).
tcf(c_6188,plain,
! [X0: $i] : multiply(iPr_def_25,multiply(sk_c4,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_6171,c_113]) ).
tcf(c_6189,plain,
! [X0: $i] : multiply(iPr_def_15,multiply(sk_c11,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_6170,c_113]) ).
tcf(c_6232,plain,
( ( iPr_def_18 = iPr_def_16 )
| ( iPr_def_18 != iPr_def_18 )
| ( iPr_def_16 != iPr_def_18 ) ),
inference(instantiation,[status(thm)],[c_4105]) ).
tcf(c_6247,plain,
( ( iPr_def_21 = iPr_def_19 )
| ( iPr_def_21 != iPr_def_21 )
| ( iPr_def_19 != iPr_def_21 ) ),
inference(instantiation,[status(thm)],[c_4250]) ).
tcf(c_6249,plain,
( ( iPr_def_21 = iPr_def_16 )
| ( iPr_def_21 != iPr_def_21 )
| ( iPr_def_16 != iPr_def_21 ) ),
inference(instantiation,[status(thm)],[c_4250]) ).
tcf(c_7861,plain,
! [X0: $i] :
( ( iPr_def_16 = iPr_def_18 )
| ~ iPr_def_13
| ( inverse(X0) != sk_c10 )
| ( multiply(X0,iPr_def_29) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_1924,c_745]) ).
tcf(c_7916,plain,
( ( iPr_def_16 = iPr_def_18 )
| ~ iPr_def_13
| ( inverse(sk_c11) != sk_c10 )
| ( multiply(sk_c11,iPr_def_29) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_7861]) ).
tcf(c_7921,plain,
! [X0: $i] :
( ( identity = X0 )
| ( identity != identity )
| ( X0 != identity ) ),
inference(instantiation,[status(thm)],[c_4443]) ).
tcf(c_7922,plain,
( ( identity = sk_c11 )
| ( identity != identity )
| ( sk_c11 != identity ) ),
inference(instantiation,[status(thm)],[c_7921]) ).
tcf(c_8039,plain,
! [X0: $i] :
( ( iPr_def_18 = iPr_def_19 )
| ~ iPr_def_13
| ( inverse(X0) != sk_c10 )
| ( multiply(X0,iPr_def_29) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_2018,c_745]) ).
tcf(c_8088,plain,
( ( iPr_def_18 = iPr_def_19 )
| ~ iPr_def_13
| ( inverse(sk_c11) != sk_c10 )
| ( multiply(sk_c11,iPr_def_29) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_8039]) ).
tcf(c_8369,plain,
( ( sk_c10 = iPr_def_18 )
| ( iPr_def_18 != iPr_def_16 )
| ( sk_c10 != iPr_def_16 ) ),
inference(instantiation,[status(thm)],[c_1557]) ).
tcf(c_8370,plain,
! [X0: $i] :
( ( iPr_def_18 = X0 )
| ( iPr_def_18 != iPr_def_16 )
| ( X0 != iPr_def_16 ) ),
inference(instantiation,[status(thm)],[c_2257]) ).
tcf(c_8470,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = inverse(X0) )
| ( X2 != X1 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_811]) ).
tcf(c_8472,plain,
! [X0: $i] :
( ( inverse(X0) = iPr_def_15 )
| ( iPr_def_15 != inverse(sk_c11) )
| ( inverse(X0) != inverse(sk_c11) ) ),
inference(instantiation,[status(thm)],[c_5114]) ).
tcf(c_8473,plain,
( ( inverse(sk_c11) = iPr_def_15 )
| ( iPr_def_15 != inverse(sk_c11) )
| ( inverse(sk_c11) != inverse(sk_c11) ) ),
inference(instantiation,[status(thm)],[c_8472]) ).
tcf(c_8483,plain,
! [X0: $i] :
( ( inverse(X0) = iPr_def_30 )
| ( iPr_def_30 != inverse(sk_c1) )
| ( inverse(X0) != inverse(sk_c1) ) ),
inference(instantiation,[status(thm)],[c_5114]) ).
tcf(c_8539,plain,
! [X0: $i] :
( ( iPr_def_16 = iPr_def_21 )
| ~ iPr_def_13
| ( inverse(X0) != sk_c10 )
| ( multiply(X0,iPr_def_29) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_2120,c_745]) ).
tcf(c_8588,plain,
( ( iPr_def_16 = iPr_def_21 )
| ~ iPr_def_13
| ( inverse(sk_c11) != sk_c10 )
| ( multiply(sk_c11,iPr_def_29) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_8539]) ).
tcf(c_8738,plain,
( ( iPr_def_16 = iPr_def_18 )
| ( inverse(iPr_def_30) = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_2581,c_727]) ).
tcf(c_8789,plain,
( ( iPr_def_16 = iPr_def_21 )
| ( iPr_def_21 != iPr_def_16 )
| ( iPr_def_16 != iPr_def_16 ) ),
inference(instantiation,[status(thm)],[c_4098]) ).
tcf(c_8793,plain,
! [X0: $i] :
( ( X0 = iPr_def_21 )
| ( iPr_def_21 != iPr_def_16 )
| ( X0 != iPr_def_16 ) ),
inference(instantiation,[status(thm)],[c_1813]) ).
tcf(c_8794,plain,
( ( sk_c11 = iPr_def_21 )
| ( iPr_def_21 != iPr_def_16 )
| ( sk_c11 != iPr_def_16 ) ),
inference(instantiation,[status(thm)],[c_8793]) ).
tcf(c_8863,plain,
( ( iPr_def_18 = iPr_def_19 )
| ( inverse(iPr_def_30) = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_2705,c_727]) ).
tcf(c_9266,plain,
( ( iPr_def_29 = iPr_def_30 )
| ( iPr_def_18 = iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_2859,c_2119]) ).
tcf(c_9408,plain,
( ( iPr_def_16 = iPr_def_21 )
| ( inverse(iPr_def_30) = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_2860,c_727]) ).
tcf(c_9509,plain,
! [X0: $i] :
( ( iPr_def_29 = iPr_def_30 )
| ~ iPr_def_13
| ( inverse(X0) != sk_c10 )
| ( multiply(X0,iPr_def_22) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_2998,c_745]) ).
tcf(c_9634,plain,
( ( iPr_def_29 = iPr_def_30 )
| ~ iPr_def_13
| ( inverse(sk_c11) != sk_c10 )
| ( multiply(sk_c11,iPr_def_22) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_9509]) ).
tcf(c_9799,plain,
( ( iPr_def_29 = iPr_def_30 )
| ( inverse(iPr_def_23) = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_3103,c_727]) ).
tcf(c_9989,plain,
( ( sk_c10 = multiply(identity,iPr_def_28) )
| ( sk_c10 != iPr_def_28 )
| ( multiply(identity,iPr_def_28) != iPr_def_28 ) ),
inference(instantiation,[status(thm)],[c_2820]) ).
tcf(c_10363,plain,
( ( iPr_def_16 = iPr_def_19 )
| ( iPr_def_19 != iPr_def_18 )
| ( iPr_def_16 != iPr_def_18 ) ),
inference(instantiation,[status(thm)],[c_4945]) ).
tcf(c_10532,plain,
( ( iPr_def_29 = iPr_def_30 )
| ( inverse(iPr_def_26) = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_3284,c_727]) ).
tcf(c_13106,plain,
( ( iPr_def_15 = iPr_def_28 )
| ( inverse(iPr_def_26) = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_4518,c_727]) ).
tcf(c_13334,plain,
! [X0: $i] :
( ( X0 = iPr_def_28 )
| ( iPr_def_28 != sk_c10 )
| ( X0 != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_5641]) ).
tcf(c_13339,plain,
multiply(iPr_def_17,iPr_def_27) = sk_c11,
inference(superposition,[status(thm)],[c_739,c_6183]) ).
tcf(c_13344,plain,
multiply(iPr_def_30,iPr_def_29) = sk_c10,
inference(superposition,[status(thm)],[c_741,c_6184]) ).
tcf(c_13629,plain,
multiply(iPr_def_20,iPr_def_21) = sk_c8,
inference(superposition,[status(thm)],[c_733,c_6186]) ).
tcf(c_13634,plain,
multiply(iPr_def_23,iPr_def_22) = sk_c10,
inference(superposition,[status(thm)],[c_734,c_6187]) ).
tcf(c_13777,plain,
multiply(iPr_def_15,iPr_def_28) = sk_c3,
inference(superposition,[status(thm)],[c_740,c_6189]) ).
tcf(c_13782,plain,
! [X0: $i] :
( ( iPr_def_29 = iPr_def_30 )
| ( multiply(iPr_def_15,multiply(iPr_def_26,X0)) = X0 ) ),
inference(superposition,[status(thm)],[c_3284,c_6189]) ).
tcf(c_13783,plain,
! [X0: $i] :
( ( iPr_def_29 = iPr_def_30 )
| ( multiply(iPr_def_15,multiply(iPr_def_24,X0)) = X0 ) ),
inference(superposition,[status(thm)],[c_3200,c_6189]) ).
tcf(c_13790,plain,
! [X0: $i] :
( ( iPr_def_18 = iPr_def_19 )
| ( multiply(iPr_def_15,multiply(iPr_def_30,X0)) = X0 ) ),
inference(superposition,[status(thm)],[c_2705,c_6189]) ).
tcf(c_13791,plain,
! [X0: $i] :
( ( iPr_def_16 = iPr_def_18 )
| ( multiply(iPr_def_15,multiply(iPr_def_30,X0)) = X0 ) ),
inference(superposition,[status(thm)],[c_2581,c_6189]) ).
tcf(c_13792,plain,
! [X0: $i] :
( ( iPr_def_16 = iPr_def_21 )
| ( multiply(iPr_def_15,multiply(iPr_def_29,X0)) = X0 ) ),
inference(superposition,[status(thm)],[c_2120,c_6189]) ).
tcf(c_14829,plain,
( ( sk_c11 = iPr_def_17 )
| ( multiply(iPr_def_23,iPr_def_22) = iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_1318,c_6187]) ).
tcf(c_14830,plain,
( ( sk_c10 = iPr_def_21 )
| ( sk_c11 = iPr_def_17 ) ),
inference(light_normalisation,[status(thm)],[c_14829,c_13634]) ).
tcf(c_14853,plain,
( ( sk_c11 = iPr_def_17 )
| ( multiply(iPr_def_23,iPr_def_22) = iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_1320,c_6187]) ).
tcf(c_14854,plain,
( ( sk_c10 = iPr_def_18 )
| ( sk_c11 = iPr_def_17 ) ),
inference(light_normalisation,[status(thm)],[c_14853,c_13634]) ).
tcf(c_14865,plain,
( ( sk_c11 = iPr_def_17 )
| ( multiply(iPr_def_23,iPr_def_22) = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_1321,c_6187]) ).
tcf(c_14866,plain,
( ( sk_c10 = iPr_def_16 )
| ( sk_c11 = iPr_def_17 ) ),
inference(light_normalisation,[status(thm)],[c_14865,c_13634]) ).
tcf(c_15265,plain,
! [X0: $i] :
( ( X0 = iPr_def_15 )
| ( iPr_def_15 != iPr_def_28 )
| ( X0 != iPr_def_28 ) ),
inference(instantiation,[status(thm)],[c_5707]) ).
tcf(c_15936,plain,
( ( iPr_def_16 = iPr_def_21 )
| ( sk_c10 = iPr_def_19 )
| ( multiply(iPr_def_17,iPr_def_27) = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_1195,c_1366]) ).
tcf(c_15999,plain,
( ( iPr_def_16 = iPr_def_21 )
| ( sk_c10 = iPr_def_19 )
| ( sk_c11 = iPr_def_28 ) ),
inference(light_normalisation,[status(thm)],[c_15936,c_13339]) ).
tcf(c_21039,plain,
( ( sk_c11 = iPr_def_22 )
| ( multiply(iPr_def_17,iPr_def_27) = iPr_def_29 ) ),
inference(superposition,[status(thm)],[c_2209,c_6183]) ).
tcf(c_21040,plain,
( ( sk_c11 = iPr_def_29 )
| ( sk_c11 = iPr_def_22 ) ),
inference(light_normalisation,[status(thm)],[c_21039,c_13339]) ).
tcf(c_21413,plain,
( ( sk_c11 = iPr_def_23 )
| ( multiply(iPr_def_17,iPr_def_27) = iPr_def_29 ) ),
inference(superposition,[status(thm)],[c_2273,c_6183]) ).
tcf(c_21414,plain,
( ( sk_c11 = iPr_def_29 )
| ( sk_c11 = iPr_def_23 ) ),
inference(light_normalisation,[status(thm)],[c_21413,c_13339]) ).
tcf(c_22807,plain,
( ( sk_c11 = iPr_def_22 )
| ( multiply(iPr_def_17,iPr_def_27) = iPr_def_30 ) ),
inference(superposition,[status(thm)],[c_3001,c_6183]) ).
tcf(c_22808,plain,
( ( sk_c11 = iPr_def_30 )
| ( sk_c11 = iPr_def_22 ) ),
inference(light_normalisation,[status(thm)],[c_22807,c_13339]) ).
tcf(c_23202,plain,
( ( sk_c11 = iPr_def_23 )
| ( multiply(iPr_def_17,iPr_def_27) = iPr_def_30 ) ),
inference(superposition,[status(thm)],[c_3107,c_6183]) ).
tcf(c_23203,plain,
( ( sk_c11 = iPr_def_30 )
| ( sk_c11 = iPr_def_23 ) ),
inference(light_normalisation,[status(thm)],[c_23202,c_13339]) ).
tcf(c_24504,plain,
( ( sk_c10 = iPr_def_15 )
| ( multiply(iPr_def_30,iPr_def_29) = iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_3840,c_6184]) ).
tcf(c_24505,plain,
( ( sk_c10 = iPr_def_21 )
| ( sk_c10 = iPr_def_15 ) ),
inference(light_normalisation,[status(thm)],[c_24504,c_13344]) ).
tcf(c_27248,plain,
multiply(sk_c7,iPr_def_19) = multiply(iPr_def_21,sk_c11),
inference(superposition,[status(thm)],[c_731,c_6161]) ).
tcf(c_27692,plain,
! [X0: $i,X1: $i] :
( ( inverse(X0) = X1 )
| ( X1 != iPr_def_21 )
| ( inverse(X0) != iPr_def_21 ) ),
inference(instantiation,[status(thm)],[c_2547]) ).
tcf(c_28953,plain,
! [X0: $i] :
( ( sk_c10 = iPr_def_18 )
| ( iPr_def_18 != X0 )
| ( sk_c10 != X0 ) ),
inference(instantiation,[status(thm)],[c_1473]) ).
tcf(c_28954,plain,
( ( sk_c10 = iPr_def_18 )
| ( iPr_def_18 != sk_c11 )
| ( sk_c10 != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_28953]) ).
tcf(c_28956,plain,
! [X0: $i] :
( ( sk_c10 = identity )
| ( identity != X0 )
| ( sk_c10 != X0 ) ),
inference(instantiation,[status(thm)],[c_1473]) ).
tcf(c_28963,plain,
( ( sk_c10 = identity )
| ( identity != sk_c11 )
| ( sk_c10 != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_28956]) ).
tcf(c_28993,plain,
! [X0: $i,X1: $i] :
( ( sk_c10 = inverse(X0) )
| ( sk_c10 != X1 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_1473]) ).
tcf(c_32460,plain,
( ( iPr_def_15 = iPr_def_28 )
| ( sk_c10 = iPr_def_21 ) ),
inference(global_subsumption_just,[status(thm)],[c_3954,c_774,c_804,c_1475,c_1521,c_5333]) ).
tcf(c_32561,plain,
( ( iPr_def_15 = iPr_def_28 )
| ( iPr_def_15 = iPr_def_21 )
| ( sk_c11 = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_32460,c_809]) ).
tcf(c_32710,plain,
( ( identity = iPr_def_28 )
| ( iPr_def_28 != sk_c10 )
| ( identity != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_13334]) ).
tcf(c_33335,plain,
( ( iPr_def_15 = iPr_def_28 )
| ( sk_c10 = iPr_def_18 ) ),
inference(global_subsumption_just,[status(thm)],[c_3956,c_771,c_801,c_1475,c_1519,c_5333]) ).
tcf(c_33540,plain,
( ( iPr_def_15 = iPr_def_28 )
| ( sk_c10 = iPr_def_16 ) ),
inference(global_subsumption_just,[status(thm)],[c_3957,c_770,c_800,c_1475,c_1518,c_5333]) ).
tcf(c_34502,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = inverse(X0) )
| ( X2 != inverse(X1) )
| ( inverse(X0) != inverse(X1) ) ),
inference(instantiation,[status(thm)],[c_8470]) ).
tcf(c_34535,plain,
! [X0: $i,X1: $i] :
( ( X1 = inverse(X0) )
| ( X1 != iPr_def_15 )
| ( inverse(X0) != iPr_def_15 ) ),
inference(instantiation,[status(thm)],[c_8470]) ).
tcf(c_34691,plain,
( ( inverse(sk_c1) = iPr_def_30 )
| ( iPr_def_30 != inverse(sk_c1) )
| ( inverse(sk_c1) != inverse(sk_c1) ) ),
inference(instantiation,[status(thm)],[c_8483]) ).
tcf(c_34692,plain,
inverse(sk_c1) = inverse(sk_c1),
inference(instantiation,[status(thm)],[c_2544]) ).
tcf(c_35254,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(X0,X1)) = X1,
inference(demodulation,[status(thm)],[c_6168,c_113]) ).
tcf(c_35310,plain,
multiply(inverse(sk_c8),iPr_def_19) = sk_c11,
inference(superposition,[status(thm)],[c_731,c_35254]) ).
tcf(c_35315,plain,
! [X0: $i] : multiply(inverse(identity),X0) = X0,
inference(superposition,[status(thm)],[c_113,c_35254]) ).
tcf(c_35316,plain,
! [X0: $i] : multiply(inverse(inverse(X0)),identity) = X0,
inference(superposition,[status(thm)],[c_114,c_35254]) ).
tcf(c_35701,plain,
! [X0: $i] : multiply(inverse(iPr_def_15),X0) = multiply(sk_c11,X0),
inference(superposition,[status(thm)],[c_6189,c_35254]) ).
tcf(c_35702,plain,
! [X0: $i] : multiply(inverse(iPr_def_25),X0) = multiply(sk_c4,X0),
inference(superposition,[status(thm)],[c_6188,c_35254]) ).
tcf(c_35703,plain,
! [X0: $i] : multiply(inverse(iPr_def_23),X0) = multiply(sk_c6,X0),
inference(superposition,[status(thm)],[c_6187,c_35254]) ).
tcf(c_35704,plain,
! [X0: $i] : multiply(inverse(iPr_def_20),X0) = multiply(sk_c7,X0),
inference(superposition,[status(thm)],[c_6186,c_35254]) ).
tcf(c_35705,plain,
! [X0: $i] : multiply(inverse(iPr_def_18),X0) = multiply(sk_c9,X0),
inference(superposition,[status(thm)],[c_6185,c_35254]) ).
tcf(c_35706,plain,
! [X0: $i] : multiply(inverse(iPr_def_30),X0) = multiply(sk_c1,X0),
inference(superposition,[status(thm)],[c_6184,c_35254]) ).
tcf(c_35707,plain,
! [X0: $i] : multiply(inverse(iPr_def_17),X0) = multiply(sk_c2,X0),
inference(superposition,[status(thm)],[c_6183,c_35254]) ).
tcf(c_35767,plain,
! [X0: $i,X1: $i] : multiply(inverse(inverse(X0)),X1) = multiply(X0,X1),
inference(superposition,[status(thm)],[c_35254,c_35254]) ).
tcf(c_36609,plain,
( ( identity = sk_c10 )
| ( identity != iPr_def_21 )
| ( sk_c10 != iPr_def_21 ) ),
inference(instantiation,[status(thm)],[c_1650]) ).
tcf(c_36888,plain,
! [X0: $i] :
( ( identity = X0 )
| ( identity != iPr_def_21 )
| ( X0 != iPr_def_21 ) ),
inference(instantiation,[status(thm)],[c_4443]) ).
tcf(c_36889,plain,
! [X0: $i] :
( ( X0 = identity )
| ( identity != iPr_def_21 )
| ( X0 != iPr_def_21 ) ),
inference(instantiation,[status(thm)],[c_2533]) ).
tcf(c_36890,plain,
( ( sk_c11 = identity )
| ( identity != iPr_def_21 )
| ( sk_c11 != iPr_def_21 ) ),
inference(instantiation,[status(thm)],[c_36889]) ).
tcf(c_36891,plain,
( ( identity = sk_c11 )
| ( identity != iPr_def_21 )
| ( sk_c11 != iPr_def_21 ) ),
inference(instantiation,[status(thm)],[c_36888]) ).
tcf(c_37078,plain,
! [X0: $i] :
( ( X0 = iPr_def_18 )
| ( iPr_def_18 != iPr_def_19 )
| ( X0 != iPr_def_19 ) ),
inference(instantiation,[status(thm)],[c_1768]) ).
tcf(c_38439,plain,
! [X0: $i] : multiply(X0,identity) = X0,
inference(demodulation,[status(thm)],[c_35316,c_35767]) ).
tcf(c_38479,plain,
inverse(identity) = identity,
inference(superposition,[status(thm)],[c_38439,c_35315]) ).
tcf(c_38808,plain,
( ( iPr_def_15 = iPr_def_28 )
| ~ iPr_def_13
| ( sk_c10 != iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_33540,c_4991]) ).
tcf(c_38873,plain,
( ( sk_c11 = iPr_def_17 )
| ~ iPr_def_13
| ( sk_c10 != iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_750,c_4991]) ).
tcf(c_39176,plain,
( ~ iPr_def_10
| ( sk_c11 != iPr_def_30 ) ),
inference(global_subsumption_just,[status(thm)],[c_5161,c_5165,c_5161,c_21040,c_21414]) ).
tcf(c_39178,plain,
~ iPr_def_10,
inference(global_subsumption_just,[status(thm)],[c_39176,c_5165,c_22808,c_23203,c_39176]) ).
tcf(c_39184,plain,
( iPr_def_14
| iPr_def_13
| iPr_def_12
| iPr_def_11
| ( sk_c10 != iPr_def_15 ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_743,c_39178]) ).
tcf(c_39253,plain,
( iPr_def_14
| iPr_def_13
| iPr_def_12
| iPr_def_11
| ( iPr_def_15 = iPr_def_28 )
| ( iPr_def_15 != iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_32460,c_39184]) ).
tcf(c_39312,plain,
( iPr_def_14
| iPr_def_13
| iPr_def_12
| iPr_def_11
| ( sk_c11 = iPr_def_17 )
| ( iPr_def_15 != iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_754,c_39184]) ).
tcf(c_39565,plain,
multiply(sk_c11,iPr_def_15) = identity,
inference(superposition,[status(thm)],[c_35701,c_114]) ).
tcf(c_39570,plain,
! [X0: $i] : multiply(sk_c11,multiply(iPr_def_15,X0)) = X0,
inference(superposition,[status(thm)],[c_35701,c_35254]) ).
tcf(c_39571,plain,
multiply(sk_c11,identity) = inverse(iPr_def_15),
inference(superposition,[status(thm)],[c_35701,c_38439]) ).
tcf(c_39646,plain,
multiply(sk_c9,identity) = multiply(iPr_def_16,iPr_def_15),
inference(superposition,[status(thm)],[c_39565,c_6163]) ).
tcf(c_39874,plain,
inverse(iPr_def_15) = sk_c11,
inference(demodulation,[status(thm)],[c_39571,c_38439]) ).
tcf(c_39877,plain,
( ~ iPr_def_11
| ( multiply(iPr_def_15,sk_c11) != sk_c10 )
| ( multiply(inverse(iPr_def_15),sk_c11) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_39874,c_748]) ).
tcf(c_39884,plain,
( ~ iPr_def_11
| ( sk_c10 != identity )
| ( multiply(sk_c11,sk_c11) != sk_c10 ) ),
inference(light_normalisation,[status(thm)],[c_39877,c_1399,c_39874]) ).
tcf(c_39994,plain,
( ~ iPr_def_14
| ( sk_c11 != sk_c10 )
| ( inverse(iPr_def_15) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_39570,c_744]) ).
tcf(c_40175,plain,
( ~ iPr_def_14
| ( sk_c11 != sk_c10 ) ),
inference(ground_joinability,[status(thm)],[c_39994,c_39874]) ).
tcf(c_40928,plain,
( ( iPr_def_15 = iPr_def_28 )
| ~ iPr_def_14
| ( sk_c11 != iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_32460,c_40175]) ).
tcf(c_40967,plain,
( ( sk_c10 = iPr_def_15 )
| ~ iPr_def_14
| ( sk_c11 != iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_804,c_40175]) ).
tcf(c_40987,plain,
( ( sk_c11 = iPr_def_17 )
| ~ iPr_def_14
| ( sk_c11 != iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_754,c_40175]) ).
tcf(c_41710,plain,
! [X0: $i] :
( ( inverse(X0) = sk_c10 )
| ( sk_c10 != iPr_def_18 )
| ( inverse(X0) != iPr_def_18 ) ),
inference(instantiation,[status(thm)],[c_1654]) ).
tcf(c_41714,plain,
( ( inverse(sk_c11) = sk_c10 )
| ( sk_c10 != iPr_def_18 )
| ( inverse(sk_c11) != iPr_def_18 ) ),
inference(instantiation,[status(thm)],[c_41710]) ).
tcf(c_43287,plain,
( ( iPr_def_18 = iPr_def_21 )
| ( iPr_def_21 != iPr_def_16 )
| ( iPr_def_18 != iPr_def_16 ) ),
inference(instantiation,[status(thm)],[c_8370]) ).
tcf(c_43317,plain,
multiply(iPr_def_16,iPr_def_15) = sk_c9,
inference(demodulation,[status(thm)],[c_39646,c_38439]) ).
tcf(c_45821,plain,
multiply(sk_c4,iPr_def_25) = identity,
inference(superposition,[status(thm)],[c_35702,c_114]) ).
tcf(c_45840,plain,
( ( identity = iPr_def_26 )
| ( sk_c10 = iPr_def_15 ) ),
inference(demodulation,[status(thm)],[c_4459,c_45821]) ).
tcf(c_45841,plain,
( ( identity = iPr_def_26 )
| ( sk_c11 = iPr_def_30 ) ),
inference(demodulation,[status(thm)],[c_3266,c_45821]) ).
tcf(c_45842,plain,
( ( identity = iPr_def_26 )
| ( sk_c11 = iPr_def_29 ) ),
inference(demodulation,[status(thm)],[c_2321,c_45821]) ).
tcf(c_45843,plain,
( ( identity = iPr_def_26 )
| ( sk_c10 = iPr_def_28 ) ),
inference(demodulation,[status(thm)],[c_1747,c_45821]) ).
tcf(c_45844,plain,
( ( identity = iPr_def_26 )
| ( sk_c3 = iPr_def_27 ) ),
inference(demodulation,[status(thm)],[c_1424,c_45821]) ).
tcf(c_45845,plain,
( ( identity = iPr_def_26 )
| ( sk_c11 = iPr_def_17 ) ),
inference(demodulation,[status(thm)],[c_1345,c_45821]) ).
tcf(c_45919,plain,
( ( sk_c11 = iPr_def_17 )
| ~ iPr_def_14
| ( iPr_def_21 != iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_759,c_40987]) ).
tcf(c_46291,plain,
( iPr_def_14
| iPr_def_13
| iPr_def_12
| iPr_def_11
| ( identity = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_45840,c_39184]) ).
tcf(c_46567,plain,
( ( identity = iPr_def_26 )
| ( inverse(iPr_def_30) = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_45841,c_727]) ).
tcf(c_46860,plain,
! [X0: $i] :
( ( identity = iPr_def_26 )
| ~ iPr_def_13
| ( inverse(X0) != sk_c10 )
| ( multiply(X0,iPr_def_29) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_45842,c_745]) ).
tcf(c_46866,plain,
( ( identity = iPr_def_26 )
| ( multiply(iPr_def_29,sk_c3) = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_45842,c_740]) ).
tcf(c_46987,plain,
( ( identity = iPr_def_26 )
| ~ iPr_def_13
| ( inverse(sk_c11) != sk_c10 )
| ( multiply(sk_c11,iPr_def_29) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_46860]) ).
tcf(c_52115,plain,
( ( identity = iPr_def_26 )
| ~ iPr_def_14
| ( sk_c11 != iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_45843,c_40175]) ).
tcf(c_52174,plain,
( ( identity = iPr_def_26 )
| ( multiply(sk_c1,iPr_def_28) = iPr_def_29 ) ),
inference(superposition,[status(thm)],[c_45843,c_741]) ).
tcf(c_52375,plain,
( ( identity = iPr_def_26 )
| ( multiply(sk_c11,iPr_def_27) = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_45844,c_740]) ).
tcf(c_53400,plain,
multiply(sk_c6,identity) = inverse(iPr_def_23),
inference(superposition,[status(thm)],[c_35703,c_38439]) ).
tcf(c_53430,plain,
inverse(iPr_def_23) = sk_c6,
inference(demodulation,[status(thm)],[c_53400,c_38439]) ).
tcf(c_53433,plain,
( ( iPr_def_29 = iPr_def_30 )
| ( sk_c6 = iPr_def_15 ) ),
inference(demodulation,[status(thm)],[c_9799,c_53430]) ).
tcf(c_53443,plain,
( ~ iPr_def_12
| ( multiply(iPr_def_23,sk_c6) != sk_c11 )
| ( multiply(inverse(iPr_def_23),sk_c10) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_53430,c_746]) ).
tcf(c_53445,plain,
( ~ iPr_def_12
| ( sk_c11 != iPr_def_22 )
| ( sk_c11 != identity ) ),
inference(light_normalisation,[status(thm)],[c_53443,c_734,c_1401,c_53430]) ).
tcf(c_53896,plain,
! [X0: $i,X1: $i] :
( ( inverse(X0) = iPr_def_18 )
| ( iPr_def_18 != X1 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_2547]) ).
tcf(c_53920,plain,
! [X0: $i,X1: $i] :
( ( inverse(X0) = iPr_def_21 )
| ( iPr_def_21 != X1 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_2547]) ).
tcf(c_54030,plain,
( ( iPr_def_29 = iPr_def_30 )
| ( multiply(iPr_def_15,sk_c10) = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_53433,c_734]) ).
tcf(c_54438,plain,
multiply(sk_c7,iPr_def_20) = identity,
inference(superposition,[status(thm)],[c_35704,c_114]) ).
tcf(c_54444,plain,
multiply(sk_c7,identity) = inverse(iPr_def_20),
inference(superposition,[status(thm)],[c_35704,c_38439]) ).
tcf(c_54457,plain,
( ( identity = iPr_def_21 )
| ( sk_c10 = iPr_def_15 ) ),
inference(demodulation,[status(thm)],[c_3793,c_54438]) ).
tcf(c_54458,plain,
( ( identity = iPr_def_21 )
| ( sk_c11 = iPr_def_30 ) ),
inference(demodulation,[status(thm)],[c_2827,c_54438]) ).
tcf(c_54459,plain,
( ( identity = iPr_def_21 )
| ( sk_c11 = iPr_def_29 ) ),
inference(demodulation,[status(thm)],[c_2094,c_54438]) ).
tcf(c_54460,plain,
( ( identity = iPr_def_21 )
| ( sk_c10 = iPr_def_28 ) ),
inference(demodulation,[status(thm)],[c_1563,c_54438]) ).
tcf(c_54461,plain,
( ( identity = iPr_def_21 )
| ( sk_c11 = iPr_def_17 ) ),
inference(demodulation,[status(thm)],[c_1313,c_54438]) ).
tcf(c_54462,plain,
( ( identity = iPr_def_21 )
| ( sk_c3 = iPr_def_27 ) ),
inference(demodulation,[status(thm)],[c_1312,c_54438]) ).
tcf(c_54483,plain,
inverse(iPr_def_20) = sk_c7,
inference(demodulation,[status(thm)],[c_54444,c_38439]) ).
tcf(c_54583,plain,
( iPr_def_14
| iPr_def_13
| iPr_def_12
| iPr_def_11
| ( identity = iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_54457,c_39184]) ).
tcf(c_55023,plain,
! [X0: $i,X1: $i] :
( ( X0 = iPr_def_28 )
| ( iPr_def_28 != inverse(X1) )
| ( X0 != inverse(X1) ) ),
inference(instantiation,[status(thm)],[c_5641]) ).
tcf(c_55025,plain,
( ( sk_c11 = iPr_def_28 )
| ( iPr_def_28 != inverse(sk_c11) )
| ( sk_c11 != inverse(sk_c11) ) ),
inference(instantiation,[status(thm)],[c_55023]) ).
tcf(c_55178,plain,
( ( identity = iPr_def_21 )
| ( inverse(iPr_def_30) = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_54458,c_727]) ).
tcf(c_55443,plain,
! [X0: $i] :
( ( identity = iPr_def_21 )
| ~ iPr_def_13
| ( inverse(X0) != sk_c10 )
| ( multiply(X0,iPr_def_29) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_54459,c_745]) ).
tcf(c_55449,plain,
( ( identity = iPr_def_21 )
| ( multiply(iPr_def_29,sk_c3) = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_54459,c_740]) ).
tcf(c_55570,plain,
( ( identity = iPr_def_21 )
| ~ iPr_def_13
| ( inverse(sk_c11) != sk_c10 )
| ( multiply(sk_c11,iPr_def_29) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_55443]) ).
tcf(c_55838,plain,
( ( identity = iPr_def_21 )
| ~ iPr_def_14
| ( sk_c11 != iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_54460,c_40175]) ).
tcf(c_55897,plain,
( ( identity = iPr_def_21 )
| ( multiply(sk_c1,iPr_def_28) = iPr_def_29 ) ),
inference(superposition,[status(thm)],[c_54460,c_741]) ).
tcf(c_56144,plain,
( ( identity = iPr_def_21 )
| ( multiply(iPr_def_17,sk_c3) = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_54461,c_740]) ).
tcf(c_56388,plain,
( ( iPr_def_18 = iPr_def_15 )
| ( iPr_def_18 != iPr_def_21 )
| ( iPr_def_15 != iPr_def_21 ) ),
inference(instantiation,[status(thm)],[c_5061]) ).
tcf(c_56392,plain,
( ( sk_c10 = iPr_def_15 )
| ( iPr_def_15 != iPr_def_21 )
| ( sk_c10 != iPr_def_21 ) ),
inference(instantiation,[status(thm)],[c_1609]) ).
tcf(c_56564,plain,
! [X0: $i] :
( ( sk_c10 = inverse(X0) )
| ( sk_c10 != iPr_def_15 )
| ( inverse(X0) != iPr_def_15 ) ),
inference(instantiation,[status(thm)],[c_28993]) ).
tcf(c_56567,plain,
( ( sk_c10 = inverse(sk_c11) )
| ( sk_c10 != iPr_def_15 )
| ( inverse(sk_c11) != iPr_def_15 ) ),
inference(instantiation,[status(thm)],[c_56564]) ).
tcf(c_57100,plain,
( ( sk_c10 = multiply(identity,iPr_def_15) )
| ( sk_c10 != iPr_def_18 )
| ( multiply(identity,iPr_def_15) != iPr_def_18 ) ),
inference(instantiation,[status(thm)],[c_1603]) ).
tcf(c_57183,plain,
( ( identity = iPr_def_26 )
| ( multiply(iPr_def_17,iPr_def_27) = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_45845,c_52375]) ).
tcf(c_57249,plain,
( ( identity = iPr_def_26 )
| ( sk_c11 = iPr_def_28 ) ),
inference(light_normalisation,[status(thm)],[c_57183,c_13339]) ).
tcf(c_58313,plain,
( ( identity = iPr_def_26 )
| ( multiply(iPr_def_15,iPr_def_28) = identity ) ),
inference(superposition,[status(thm)],[c_57249,c_1399]) ).
tcf(c_58342,plain,
( ( identity = iPr_def_26 )
| ( sk_c3 = identity ) ),
inference(light_normalisation,[status(thm)],[c_58313,c_13777]) ).
tcf(c_61541,plain,
( ( iPr_def_21 = sk_c10 )
| ( iPr_def_21 != iPr_def_15 )
| ( sk_c10 != iPr_def_15 ) ),
inference(instantiation,[status(thm)],[c_2970]) ).
tcf(c_61544,plain,
( ( iPr_def_28 = sk_c10 )
| ( iPr_def_28 != iPr_def_15 )
| ( sk_c10 != iPr_def_15 ) ),
inference(instantiation,[status(thm)],[c_2970]) ).
tcf(c_61546,plain,
! [X0: $i] :
( ( inverse(X0) = sk_c10 )
| ( sk_c10 != iPr_def_15 )
| ( inverse(X0) != iPr_def_15 ) ),
inference(instantiation,[status(thm)],[c_2970]) ).
tcf(c_61547,plain,
( ( inverse(sk_c11) = sk_c10 )
| ( sk_c10 != iPr_def_15 )
| ( inverse(sk_c11) != iPr_def_15 ) ),
inference(instantiation,[status(thm)],[c_61546]) ).
tcf(c_61942,plain,
( ( sk_c10 = iPr_def_21 )
| ( iPr_def_21 != iPr_def_15 )
| ( sk_c10 != iPr_def_15 ) ),
inference(instantiation,[status(thm)],[c_2971]) ).
tcf(c_64867,plain,
( ( iPr_def_28 = iPr_def_15 )
| ( iPr_def_28 != iPr_def_28 )
| ( iPr_def_15 != iPr_def_28 ) ),
inference(instantiation,[status(thm)],[c_15265]) ).
tcf(c_64879,plain,
! [X0: $i] :
( ( iPr_def_28 = inverse(X0) )
| ( iPr_def_28 != iPr_def_15 )
| ( inverse(X0) != iPr_def_15 ) ),
inference(instantiation,[status(thm)],[c_34535]) ).
tcf(c_64880,plain,
( ( iPr_def_28 = inverse(sk_c11) )
| ( iPr_def_28 != iPr_def_15 )
| ( inverse(sk_c11) != iPr_def_15 ) ),
inference(instantiation,[status(thm)],[c_64879]) ).
tcf(c_65346,plain,
( ( iPr_def_29 = iPr_def_30 )
| ( multiply(sk_c11,iPr_def_22) = sk_c10 ) ),
inference(superposition,[status(thm)],[c_54030,c_39570]) ).
tcf(c_66357,plain,
multiply(sk_c9,identity) = inverse(iPr_def_18),
inference(superposition,[status(thm)],[c_35705,c_38439]) ).
tcf(c_66380,plain,
inverse(iPr_def_18) = sk_c9,
inference(demodulation,[status(thm)],[c_66357,c_38439]) ).
tcf(c_66383,plain,
( ~ iPr_def_11
| ( multiply(iPr_def_18,sk_c9) != sk_c10 )
| ( multiply(inverse(iPr_def_18),sk_c11) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_66380,c_748]) ).
tcf(c_66390,plain,
( ~ iPr_def_11
| ( sk_c10 != iPr_def_16 )
| ( sk_c10 != identity ) ),
inference(light_normalisation,[status(thm)],[c_66383,c_728,c_1403,c_66380]) ).
tcf(c_69020,plain,
( ( sk_c11 = inverse(sk_c1) )
| ( sk_c11 != iPr_def_30 )
| ( inverse(sk_c1) != iPr_def_30 ) ),
inference(instantiation,[status(thm)],[c_5586]) ).
tcf(c_69022,plain,
! [X0: $i] :
( ( inverse(sk_c1) = X0 )
| ( X0 != iPr_def_30 )
| ( inverse(sk_c1) != iPr_def_30 ) ),
inference(instantiation,[status(thm)],[c_2547]) ).
tcf(c_69509,plain,
( ( iPr_def_19 = iPr_def_18 )
| ( iPr_def_19 != iPr_def_19 )
| ( iPr_def_18 != iPr_def_19 ) ),
inference(instantiation,[status(thm)],[c_37078]) ).
tcf(c_71806,plain,
multiply(sk_c1,identity) = inverse(iPr_def_30),
inference(superposition,[status(thm)],[c_35706,c_38439]) ).
tcf(c_72314,plain,
( ( identity = iPr_def_21 )
| ( multiply(iPr_def_17,iPr_def_27) = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_54462,c_56144]) ).
tcf(c_72334,plain,
( ( identity = iPr_def_21 )
| ( sk_c11 = iPr_def_28 ) ),
inference(light_normalisation,[status(thm)],[c_72314,c_13339]) ).
tcf(c_72374,plain,
inverse(iPr_def_30) = sk_c1,
inference(demodulation,[status(thm)],[c_71806,c_38439]) ).
tcf(c_72376,plain,
( ( identity = iPr_def_21 )
| ( sk_c1 = iPr_def_15 ) ),
inference(demodulation,[status(thm)],[c_55178,c_72374]) ).
tcf(c_72377,plain,
( ( identity = iPr_def_26 )
| ( sk_c1 = iPr_def_15 ) ),
inference(demodulation,[status(thm)],[c_46567,c_72374]) ).
tcf(c_72378,plain,
( ( iPr_def_16 = iPr_def_21 )
| ( sk_c1 = iPr_def_15 ) ),
inference(demodulation,[status(thm)],[c_9408,c_72374]) ).
tcf(c_72382,plain,
( ( iPr_def_18 = iPr_def_19 )
| ( sk_c1 = iPr_def_15 ) ),
inference(demodulation,[status(thm)],[c_8863,c_72374]) ).
tcf(c_72383,plain,
( ( iPr_def_16 = iPr_def_18 )
| ( sk_c1 = iPr_def_15 ) ),
inference(demodulation,[status(thm)],[c_8738,c_72374]) ).
tcf(c_72384,plain,
( ( sk_c1 = iPr_def_15 )
| ( sk_c11 = iPr_def_26 ) ),
inference(demodulation,[status(thm)],[c_3294,c_72374]) ).
tcf(c_72438,plain,
( ~ iPr_def_12
| ( multiply(iPr_def_30,sk_c1) != sk_c11 )
| ( multiply(inverse(iPr_def_30),sk_c10) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_72374,c_746]) ).
tcf(c_72488,plain,
( ~ iPr_def_12
| ( sk_c11 != iPr_def_29 )
| ( sk_c11 != identity ) ),
inference(light_normalisation,[status(thm)],[c_72438,c_741,c_1404,c_72374]) ).
tcf(c_73222,plain,
( ( identity = iPr_def_21 )
| ( multiply(iPr_def_15,iPr_def_28) = identity ) ),
inference(superposition,[status(thm)],[c_72334,c_1399]) ).
tcf(c_73251,plain,
( ( identity = iPr_def_21 )
| ( sk_c3 = identity ) ),
inference(light_normalisation,[status(thm)],[c_73222,c_13777]) ).
tcf(c_75319,plain,
! [X0: $i] :
( ( X0 = iPr_def_16 )
| ( iPr_def_16 != iPr_def_19 )
| ( X0 != iPr_def_19 ) ),
inference(instantiation,[status(thm)],[c_1740]) ).
tcf(c_75910,plain,
! [X0: $i,X1: $i] :
( ( X0 = sk_c10 )
| ( sk_c10 != inverse(X1) )
| ( X0 != inverse(X1) ) ),
inference(instantiation,[status(thm)],[c_1516]) ).
tcf(c_75913,plain,
( ( sk_c11 = sk_c10 )
| ( sk_c10 != inverse(sk_c11) )
| ( sk_c11 != inverse(sk_c11) ) ),
inference(instantiation,[status(thm)],[c_75910]) ).
tcf(c_76423,plain,
( ( identity = iPr_def_21 )
| ( multiply(iPr_def_15,iPr_def_28) = iPr_def_29 ) ),
inference(superposition,[status(thm)],[c_72376,c_55897]) ).
tcf(c_76471,plain,
( ( identity = iPr_def_21 )
| ( multiply(iPr_def_15,sk_c10) = iPr_def_29 ) ),
inference(superposition,[status(thm)],[c_72376,c_741]) ).
tcf(c_76478,plain,
( ( identity = iPr_def_21 )
| ( sk_c3 = iPr_def_29 ) ),
inference(light_normalisation,[status(thm)],[c_76423,c_13777]) ).
tcf(c_76553,plain,
( ( identity = iPr_def_26 )
| ( multiply(iPr_def_15,iPr_def_28) = iPr_def_29 ) ),
inference(superposition,[status(thm)],[c_72377,c_52174]) ).
tcf(c_76599,plain,
( ( identity = iPr_def_26 )
| ( multiply(iPr_def_15,sk_c10) = iPr_def_29 ) ),
inference(superposition,[status(thm)],[c_72377,c_741]) ).
tcf(c_76606,plain,
( ( identity = iPr_def_26 )
| ( sk_c3 = iPr_def_29 ) ),
inference(light_normalisation,[status(thm)],[c_76553,c_13777]) ).
tcf(c_76687,plain,
( ( iPr_def_16 = iPr_def_21 )
| ( multiply(iPr_def_15,sk_c10) = iPr_def_29 ) ),
inference(superposition,[status(thm)],[c_72378,c_741]) ).
tcf(c_79518,plain,
( ( iPr_def_18 = iPr_def_19 )
| ( multiply(iPr_def_15,sk_c10) = iPr_def_29 ) ),
inference(superposition,[status(thm)],[c_72382,c_741]) ).
tcf(c_79656,plain,
( ( iPr_def_16 = iPr_def_18 )
| ( multiply(iPr_def_15,sk_c10) = iPr_def_29 ) ),
inference(superposition,[status(thm)],[c_72383,c_741]) ).
tcf(c_79777,plain,
( ( iPr_def_21 = iPr_def_16 )
| ( iPr_def_21 != iPr_def_19 )
| ( iPr_def_16 != iPr_def_19 ) ),
inference(instantiation,[status(thm)],[c_75319]) ).
tcf(c_82185,plain,
( ( sk_c11 = iPr_def_26 )
| ( multiply(iPr_def_15,iPr_def_28) = iPr_def_29 ) ),
inference(superposition,[status(thm)],[c_72384,c_1779]) ).
tcf(c_82204,plain,
( ( sk_c3 = iPr_def_29 )
| ( sk_c11 = iPr_def_26 ) ),
inference(light_normalisation,[status(thm)],[c_82185,c_13777]) ).
tcf(c_84127,plain,
( ( identity = iPr_def_29 )
| ( identity = iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_76478,c_73251]) ).
tcf(c_84358,plain,
( ( identity = iPr_def_29 )
| ( identity = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_76606,c_58342]) ).
tcf(c_84788,plain,
( ( identity = iPr_def_21 )
| ( multiply(sk_c11,iPr_def_29) = sk_c10 ) ),
inference(superposition,[status(thm)],[c_76471,c_39570]) ).
tcf(c_84874,plain,
( ( identity = iPr_def_26 )
| ( multiply(sk_c11,iPr_def_29) = sk_c10 ) ),
inference(superposition,[status(thm)],[c_76599,c_39570]) ).
tcf(c_85413,plain,
( ( iPr_def_27 = iPr_def_29 )
| ( sk_c11 = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_82204,c_769]) ).
tcf(c_85418,plain,
( ( iPr_def_27 = iPr_def_29 )
| ( sk_c10 = iPr_def_21 )
| ( sk_c11 = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_82204,c_764]) ).
tcf(c_86238,plain,
( ( iPr_def_27 = iPr_def_29 )
| ( inverse(iPr_def_26) = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_85413,c_727]) ).
tcf(c_88003,plain,
( ( iPr_def_16 = iPr_def_21 )
| ( multiply(sk_c11,iPr_def_29) = sk_c10 ) ),
inference(superposition,[status(thm)],[c_76687,c_39570]) ).
tcf(c_90201,plain,
! [X0: $i] :
( ( inverse(X0) = iPr_def_18 )
| ( iPr_def_18 != iPr_def_15 )
| ( inverse(X0) != iPr_def_15 ) ),
inference(instantiation,[status(thm)],[c_53896]) ).
tcf(c_90204,plain,
( ( inverse(sk_c11) = iPr_def_18 )
| ( iPr_def_18 != iPr_def_15 )
| ( inverse(sk_c11) != iPr_def_15 ) ),
inference(instantiation,[status(thm)],[c_90201]) ).
tcf(c_90232,plain,
! [X0: $i] :
( ( inverse(X0) = iPr_def_21 )
| ( iPr_def_21 != iPr_def_15 )
| ( inverse(X0) != iPr_def_15 ) ),
inference(instantiation,[status(thm)],[c_53920]) ).
tcf(c_90235,plain,
( ( inverse(sk_c11) = iPr_def_21 )
| ( iPr_def_21 != iPr_def_15 )
| ( inverse(sk_c11) != iPr_def_15 ) ),
inference(instantiation,[status(thm)],[c_90232]) ).
tcf(c_92503,plain,
( ( iPr_def_18 = iPr_def_19 )
| ( multiply(sk_c11,iPr_def_29) = sk_c10 ) ),
inference(superposition,[status(thm)],[c_79518,c_39570]) ).
tcf(c_93161,plain,
! [X0: $i] :
( ( identity = iPr_def_21 )
| ( multiply(iPr_def_29,X0) = X0 ) ),
inference(superposition,[status(thm)],[c_84127,c_113]) ).
tcf(c_93342,plain,
( ( iPr_def_16 = iPr_def_18 )
| ( multiply(sk_c11,iPr_def_29) = sk_c10 ) ),
inference(superposition,[status(thm)],[c_79656,c_39570]) ).
tcf(c_93870,plain,
! [X0: $i] :
( ( identity = iPr_def_26 )
| ( multiply(iPr_def_29,X0) = X0 ) ),
inference(superposition,[status(thm)],[c_84358,c_113]) ).
tcf(c_95948,plain,
! [X0: $i,X1: $i] :
( ( X1 = inverse(X0) )
| ( X1 != inverse(sk_c1) )
| ( inverse(X0) != inverse(sk_c1) ) ),
inference(instantiation,[status(thm)],[c_34502]) ).
tcf(c_95951,plain,
( ( sk_c11 = inverse(sk_c11) )
| ( sk_c11 != inverse(sk_c1) )
| ( inverse(sk_c11) != inverse(sk_c1) ) ),
inference(instantiation,[status(thm)],[c_95948]) ).
tcf(c_96827,plain,
( ( inverse(sk_c1) = iPr_def_21 )
| ( iPr_def_21 != iPr_def_30 )
| ( inverse(sk_c1) != iPr_def_30 ) ),
inference(instantiation,[status(thm)],[c_69022]) ).
tcf(c_96828,plain,
! [X0: $i] :
( ( inverse(X0) = inverse(sk_c1) )
| ( inverse(sk_c1) != iPr_def_21 )
| ( inverse(X0) != iPr_def_21 ) ),
inference(instantiation,[status(thm)],[c_27692]) ).
tcf(c_96829,plain,
( ( inverse(sk_c11) = inverse(sk_c1) )
| ( inverse(sk_c1) != iPr_def_21 )
| ( inverse(sk_c11) != iPr_def_21 ) ),
inference(instantiation,[status(thm)],[c_96828]) ).
tcf(c_98864,plain,
! [X0: $i,X1: $i] :
( ( multiply(inverse(X0),sk_c11) = sk_c10 )
| ( sk_c10 != X1 )
| ( multiply(inverse(X0),sk_c11) != X1 ) ),
inference(instantiation,[status(thm)],[c_811]) ).
tcf(c_98865,plain,
( ( multiply(inverse(sk_c11),sk_c11) = sk_c10 )
| ( sk_c10 != sk_c11 )
| ( multiply(inverse(sk_c11),sk_c11) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_98864]) ).
tcf(c_98867,plain,
! [X0: $i,X1: $i] :
( ( sk_c10 = X0 )
| ( sk_c10 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_811]) ).
tcf(c_98876,plain,
! [X0: $i,X1: $i] :
( ( X0 = sk_c10 )
| ( sk_c10 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_811]) ).
tcf(c_98895,plain,
! [X0: $i] :
( ( X0 = sk_c10 )
| ( sk_c10 != iPr_def_15 )
| ( X0 != iPr_def_15 ) ),
inference(instantiation,[status(thm)],[c_98876]) ).
tcf(c_98899,plain,
! [X0: $i,X1: $i] :
( ( X0 = iPr_def_15 )
| ( iPr_def_15 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_811]) ).
tcf(c_98944,plain,
! [X0: $i] :
( ( sk_c10 = X0 )
| ( sk_c10 != multiply(identity,iPr_def_28) )
| ( X0 != multiply(identity,iPr_def_28) ) ),
inference(instantiation,[status(thm)],[c_98867]) ).
tcf(c_98957,plain,
! [X0: $i,X1: $i] :
( ( iPr_def_15 = X0 )
| ( iPr_def_15 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_811]) ).
tcf(c_98988,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X0 = sk_c10 )
| ( sk_c10 != multiply(X1,X2) )
| ( X0 != multiply(X1,X2) ) ),
inference(instantiation,[status(thm)],[c_98876]) ).
tcf(c_99066,plain,
! [X0: $i,X1: $i] :
( ( multiply(X0,X1) = multiply(identity,iPr_def_15) )
| ( X1 != iPr_def_15 )
| ( X0 != identity ) ),
inference(instantiation,[status(thm)],[c_813]) ).
tcf(c_99071,plain,
( ( sk_c10 = multiply(identity,multiply(identity,iPr_def_28)) )
| ( sk_c10 != multiply(identity,iPr_def_28) )
| ( multiply(identity,multiply(identity,iPr_def_28)) != multiply(identity,iPr_def_28) ) ),
inference(instantiation,[status(thm)],[c_98944]) ).
tcf(c_99072,plain,
multiply(identity,multiply(identity,iPr_def_28)) = multiply(identity,iPr_def_28),
inference(instantiation,[status(thm)],[c_113]) ).
tcf(c_99074,plain,
! [X0: $i,X1: $i] :
( ( X1 = multiply(identity,iPr_def_28) )
| ( X1 != X0 )
| ( multiply(identity,iPr_def_28) != X0 ) ),
inference(instantiation,[status(thm)],[c_811]) ).
tcf(c_99077,plain,
! [X0: $i,X1: $i] :
( ( multiply(X0,X1) = multiply(identity,iPr_def_28) )
| ( X1 != iPr_def_28 )
| ( X0 != identity ) ),
inference(instantiation,[status(thm)],[c_813]) ).
tcf(c_99079,plain,
( ( multiply(sk_c11,sk_c11) = multiply(identity,iPr_def_28) )
| ( sk_c11 != iPr_def_28 )
| ( sk_c11 != identity ) ),
inference(instantiation,[status(thm)],[c_99077]) ).
tcf(c_99231,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( multiply(X0,X1) = sk_c10 )
| ( sk_c10 != multiply(X2,X3) )
| ( multiply(X0,X1) != multiply(X2,X3) ) ),
inference(instantiation,[status(thm)],[c_98988]) ).
tcf(c_99255,plain,
! [X0: $i] :
( ( X0 = iPr_def_15 )
| ( iPr_def_15 != iPr_def_28 )
| ( X0 != iPr_def_28 ) ),
inference(instantiation,[status(thm)],[c_98899]) ).
tcf(c_99330,plain,
! [X0: $i,X1: $i] :
( ( multiply(X0,X1) = sk_c10 )
| ( sk_c10 != iPr_def_15 )
| ( multiply(X0,X1) != iPr_def_15 ) ),
inference(instantiation,[status(thm)],[c_98895]) ).
tcf(c_99414,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(inverse(X0),sk_c11) = X2 )
| ( X2 != X1 )
| ( multiply(inverse(X0),sk_c11) != X1 ) ),
inference(instantiation,[status(thm)],[c_811]) ).
tcf(c_99490,plain,
! [X0: $i] :
( ( sk_c10 = X0 )
| ( sk_c10 != iPr_def_22 )
| ( X0 != iPr_def_22 ) ),
inference(instantiation,[status(thm)],[c_98867]) ).
tcf(c_99493,plain,
( ( sk_c10 = sk_c11 )
| ( sk_c10 != iPr_def_22 )
| ( sk_c11 != iPr_def_22 ) ),
inference(instantiation,[status(thm)],[c_99490]) ).
tcf(c_99644,plain,
! [X0: $i] :
( ( X0 = multiply(identity,iPr_def_28) )
| ( X0 != iPr_def_28 )
| ( multiply(identity,iPr_def_28) != iPr_def_28 ) ),
inference(instantiation,[status(thm)],[c_99074]) ).
tcf(c_99645,plain,
( ( sk_c11 = multiply(identity,iPr_def_28) )
| ( sk_c11 != iPr_def_28 )
| ( multiply(identity,iPr_def_28) != iPr_def_28 ) ),
inference(instantiation,[status(thm)],[c_99644]) ).
tcf(c_99665,plain,
! [X0: $i,X1: $i] :
( ( X0 = identity )
| ( identity != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_811]) ).
tcf(c_99740,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( multiply(X0,X1) = X3 )
| ( X3 != X2 )
| ( multiply(X0,X1) != X2 ) ),
inference(instantiation,[status(thm)],[c_811]) ).
tcf(c_99822,plain,
! [X0: $i] :
( ( multiply(X0,inverse(sk_c11)) = multiply(identity,iPr_def_15) )
| ( X0 != identity )
| ( inverse(sk_c11) != iPr_def_15 ) ),
inference(instantiation,[status(thm)],[c_99066]) ).
tcf(c_99823,plain,
( ( multiply(sk_c11,inverse(sk_c11)) = multiply(identity,iPr_def_15) )
| ( sk_c11 != identity )
| ( inverse(sk_c11) != iPr_def_15 ) ),
inference(instantiation,[status(thm)],[c_99822]) ).
tcf(c_100094,plain,
! [X0: $i,X1: $i] :
( ( multiply(X0,X1) = sk_c10 )
| ( sk_c10 != multiply(identity,iPr_def_28) )
| ( multiply(X0,X1) != multiply(identity,iPr_def_28) ) ),
inference(instantiation,[status(thm)],[c_99231]) ).
tcf(c_100095,plain,
( ( multiply(sk_c11,sk_c11) = sk_c10 )
| ( sk_c10 != multiply(identity,iPr_def_28) )
| ( multiply(sk_c11,sk_c11) != multiply(identity,iPr_def_28) ) ),
inference(instantiation,[status(thm)],[c_100094]) ).
tcf(c_100098,plain,
! [X0: $i,X1: $i] :
( ( multiply(X0,X1) = sk_c10 )
| ( sk_c10 != multiply(identity,multiply(identity,iPr_def_28)) )
| ( multiply(X0,X1) != multiply(identity,multiply(identity,iPr_def_28)) ) ),
inference(instantiation,[status(thm)],[c_99231]) ).
tcf(c_100099,plain,
( ( multiply(sk_c11,sk_c11) = sk_c10 )
| ( sk_c10 != multiply(identity,multiply(identity,iPr_def_28)) )
| ( multiply(sk_c11,sk_c11) != multiply(identity,multiply(identity,iPr_def_28)) ) ),
inference(instantiation,[status(thm)],[c_100098]) ).
tcf(c_101198,plain,
! [X0: $i] :
( ( multiply(inverse(sk_c11),sk_c11) = X0 )
| ( X0 != identity )
| ( multiply(inverse(sk_c11),sk_c11) != identity ) ),
inference(instantiation,[status(thm)],[c_99414]) ).
tcf(c_101199,plain,
( ( multiply(inverse(sk_c11),sk_c11) = sk_c11 )
| ( sk_c11 != identity )
| ( multiply(inverse(sk_c11),sk_c11) != identity ) ),
inference(instantiation,[status(thm)],[c_101198]) ).
tcf(c_102096,plain,
! [X0: $i,X1: $i] :
( ( multiply(X0,X1) = multiply(identity,multiply(identity,iPr_def_28)) )
| ( X1 != multiply(identity,iPr_def_28) )
| ( X0 != identity ) ),
inference(instantiation,[status(thm)],[c_813]) ).
tcf(c_102097,plain,
( ( multiply(sk_c11,sk_c11) = multiply(identity,multiply(identity,iPr_def_28)) )
| ( sk_c11 != identity )
| ( sk_c11 != multiply(identity,iPr_def_28) ) ),
inference(instantiation,[status(thm)],[c_102096]) ).
tcf(c_103128,plain,
! [X0: $i] :
( ( iPr_def_15 = X0 )
| ( iPr_def_15 != iPr_def_21 )
| ( X0 != iPr_def_21 ) ),
inference(instantiation,[status(thm)],[c_98957]) ).
tcf(c_103129,plain,
! [X0: $i] :
( ( X0 = iPr_def_15 )
| ( iPr_def_15 != iPr_def_21 )
| ( X0 != iPr_def_21 ) ),
inference(instantiation,[status(thm)],[c_98899]) ).
tcf(c_103130,plain,
( ( iPr_def_15 = sk_c11 )
| ( iPr_def_15 != iPr_def_21 )
| ( sk_c11 != iPr_def_21 ) ),
inference(instantiation,[status(thm)],[c_103128]) ).
tcf(c_103255,plain,
! [X0: $i] :
( ( multiply(X0,iPr_def_27) = iPr_def_15 )
| ( iPr_def_15 != iPr_def_28 )
| ( multiply(X0,iPr_def_27) != iPr_def_28 ) ),
inference(instantiation,[status(thm)],[c_99255]) ).
tcf(c_103262,plain,
( ( multiply(sk_c11,iPr_def_27) = iPr_def_15 )
| ( iPr_def_15 != iPr_def_28 )
| ( multiply(sk_c11,iPr_def_27) != iPr_def_28 ) ),
inference(instantiation,[status(thm)],[c_103255]) ).
tcf(c_106991,plain,
! [X0: $i,X1: $i] :
( ( X0 = iPr_def_18 )
| ( iPr_def_18 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_811]) ).
tcf(c_111332,plain,
! [X0: $i] :
( ( multiply(X0,iPr_def_27) = sk_c10 )
| ( sk_c10 != iPr_def_15 )
| ( multiply(X0,iPr_def_27) != iPr_def_15 ) ),
inference(instantiation,[status(thm)],[c_99330]) ).
tcf(c_111333,plain,
( ( multiply(sk_c11,iPr_def_27) = sk_c10 )
| ( sk_c10 != iPr_def_15 )
| ( multiply(sk_c11,iPr_def_27) != iPr_def_15 ) ),
inference(instantiation,[status(thm)],[c_111332]) ).
tcf(c_114651,plain,
! [X0: $i] :
( ( X0 = iPr_def_18 )
| ( iPr_def_18 != iPr_def_15 )
| ( X0 != iPr_def_15 ) ),
inference(instantiation,[status(thm)],[c_106991]) ).
tcf(c_117621,plain,
! [X0: $i] :
( ( X0 = identity )
| ( identity != iPr_def_28 )
| ( X0 != iPr_def_28 ) ),
inference(instantiation,[status(thm)],[c_99665]) ).
tcf(c_117622,plain,
( ( sk_c11 = identity )
| ( identity != iPr_def_28 )
| ( sk_c11 != iPr_def_28 ) ),
inference(instantiation,[status(thm)],[c_117621]) ).
tcf(c_121903,plain,
( ( iPr_def_21 = iPr_def_15 )
| ( iPr_def_21 != iPr_def_21 )
| ( iPr_def_15 != iPr_def_21 ) ),
inference(instantiation,[status(thm)],[c_103129]) ).
tcf(c_122441,plain,
( ( multiply(identity,iPr_def_15) = iPr_def_18 )
| ( iPr_def_18 != iPr_def_15 )
| ( multiply(identity,iPr_def_15) != iPr_def_15 ) ),
inference(instantiation,[status(thm)],[c_114651]) ).
tcf(c_127001,plain,
! [X0: $i,X1: $i] :
( ( multiply(X0,X1) = sk_c10 )
| ( sk_c10 != multiply(identity,iPr_def_21) )
| ( multiply(X0,X1) != multiply(identity,iPr_def_21) ) ),
inference(instantiation,[status(thm)],[c_99231]) ).
tcf(c_127003,plain,
( ( multiply(sk_c11,sk_c11) = sk_c10 )
| ( sk_c10 != multiply(identity,iPr_def_21) )
| ( multiply(sk_c11,sk_c11) != multiply(identity,iPr_def_21) ) ),
inference(instantiation,[status(thm)],[c_127001]) ).
tcf(c_127764,plain,
! [X0: $i,X1: $i] :
( ( multiply(X0,inverse(X0)) = sk_c10 )
| ( sk_c10 != X1 )
| ( multiply(X0,inverse(X0)) != X1 ) ),
inference(instantiation,[status(thm)],[c_99740]) ).
tcf(c_132213,plain,
multiply(sk_c2,iPr_def_17) = identity,
inference(superposition,[status(thm)],[c_35707,c_114]) ).
tcf(c_135214,plain,
! [X0: $i] :
( ( multiply(X0,inverse(X0)) = sk_c10 )
| ( sk_c10 != multiply(identity,iPr_def_15) )
| ( multiply(X0,inverse(X0)) != multiply(identity,iPr_def_15) ) ),
inference(instantiation,[status(thm)],[c_127764]) ).
tcf(c_135215,plain,
( ( multiply(sk_c11,inverse(sk_c11)) = sk_c10 )
| ( sk_c10 != multiply(identity,iPr_def_15) )
| ( multiply(sk_c11,inverse(sk_c11)) != multiply(identity,iPr_def_15) ) ),
inference(instantiation,[status(thm)],[c_135214]) ).
tcf(c_137461,plain,
( ( identity = iPr_def_21 )
| ( sk_c3 = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_93161,c_55449]) ).
tcf(c_137714,plain,
( ( identity = iPr_def_26 )
| ( sk_c3 = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_93870,c_46866]) ).
tcf(c_138931,plain,
( ( identity = iPr_def_28 )
| ( identity = iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_137461,c_73251]) ).
tcf(c_139598,plain,
( ( identity = iPr_def_28 )
| ( identity = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_137714,c_58342]) ).
tcf(c_139661,plain,
( ( identity = iPr_def_26 )
| ( multiply(sk_c11,iPr_def_28) = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_137714,c_740]) ).
tcf(c_140434,plain,
identity = iPr_def_21,
inference(global_subsumption_just,[status(thm)],[c_138931,c_814,c_816,c_727,c_2531,c_2821,c_5638,c_7922,c_8473,c_9989,c_21040,c_28963,c_39884,c_53445,c_54460,c_54457,c_54583,c_55570,c_55838,c_61547,c_72334,c_72488,c_84788,c_99071,c_99072,c_99645,c_100099,c_102097,c_117622,c_138931]) ).
tcf(c_140454,plain,
multiply(sk_c2,iPr_def_17) = iPr_def_21,
inference(demodulation,[status(thm)],[c_132213,c_140434]) ).
tcf(c_140558,plain,
inverse(iPr_def_21) = iPr_def_21,
inference(demodulation,[status(thm)],[c_38479,c_140434]) ).
tcf(c_140559,plain,
! [X0: $i] : multiply(X0,iPr_def_21) = X0,
inference(demodulation,[status(thm)],[c_38439,c_140434]) ).
tcf(c_140615,plain,
! [X0: $i] : multiply(iPr_def_21,X0) = X0,
inference(demodulation,[status(thm)],[c_113,c_140434]) ).
tcf(c_140862,plain,
sk_c8 = iPr_def_20,
inference(demodulation,[status(thm)],[c_13629,c_140559]) ).
tcf(c_140882,plain,
multiply(inverse(iPr_def_20),iPr_def_19) = sk_c11,
inference(demodulation,[status(thm)],[c_35310,c_140862]) ).
tcf(c_141020,plain,
multiply(iPr_def_21,sk_c11) = sk_c11,
inference(light_normalisation,[status(thm)],[c_140882,c_27248,c_54483]) ).
tcf(c_141333,plain,
( ~ iPr_def_11
| ( multiply(iPr_def_21,iPr_def_21) != sk_c10 )
| ( multiply(inverse(iPr_def_21),sk_c11) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_140558,c_748]) ).
tcf(c_141340,plain,
( ~ iPr_def_11
| ( sk_c11 != sk_c10 )
| ( multiply(iPr_def_21,iPr_def_21) != sk_c10 ) ),
inference(light_normalisation,[status(thm)],[c_141333,c_140558,c_141020]) ).
tcf(c_143320,plain,
identity = iPr_def_26,
inference(global_subsumption_just,[status(thm)],[c_139661,c_814,c_816,c_727,c_2531,c_2821,c_5638,c_7922,c_8473,c_9989,c_21040,c_28963,c_39884,c_45843,c_45840,c_46291,c_46987,c_52115,c_53445,c_57249,c_61547,c_72488,c_84874,c_99079,c_100095,c_117622,c_139598]) ).
tcf(c_143322,plain,
iPr_def_21 = iPr_def_26,
inference(light_normalisation,[status(thm)],[c_143320,c_140434]) ).
tcf(c_143348,plain,
( ( iPr_def_27 = iPr_def_29 )
| ( inverse(iPr_def_21) = iPr_def_15 ) ),
inference(demodulation,[status(thm)],[c_86238,c_143322]) ).
tcf(c_143349,plain,
( ( iPr_def_27 = iPr_def_29 )
| ( sk_c11 = iPr_def_21 ) ),
inference(demodulation,[status(thm)],[c_85413,c_143322]) ).
tcf(c_143371,plain,
( ( sk_c11 = iPr_def_17 )
| ~ iPr_def_14
| ( iPr_def_21 != iPr_def_21 ) ),
inference(demodulation,[status(thm)],[c_45919,c_143322]) ).
tcf(c_143416,plain,
( ( iPr_def_15 = iPr_def_28 )
| ( inverse(iPr_def_21) = iPr_def_15 ) ),
inference(demodulation,[status(thm)],[c_13106,c_143322]) ).
tcf(c_143419,plain,
( ( iPr_def_29 = iPr_def_30 )
| ( inverse(iPr_def_21) = iPr_def_15 ) ),
inference(demodulation,[status(thm)],[c_10532,c_143322]) ).
tcf(c_143424,plain,
( ( sk_c11 = iPr_def_21 )
| ( multiply(sk_c11,iPr_def_27) = iPr_def_28 ) ),
inference(demodulation,[status(thm)],[c_1434,c_143322]) ).
tcf(c_143430,plain,
( ( sk_c11 = iPr_def_17 )
| ( inverse(iPr_def_21) = iPr_def_15 ) ),
inference(demodulation,[status(thm)],[c_1256,c_143322]) ).
tcf(c_143431,plain,
( ( iPr_def_15 = iPr_def_28 )
| ( sk_c11 = iPr_def_21 ) ),
inference(demodulation,[status(thm)],[c_4518,c_143322]) ).
tcf(c_143432,plain,
( ( iPr_def_29 = iPr_def_30 )
| ( sk_c11 = iPr_def_21 ) ),
inference(demodulation,[status(thm)],[c_3284,c_143322]) ).
tcf(c_143436,plain,
( ( sk_c10 = iPr_def_15 )
| ( sk_c11 = iPr_def_21 ) ),
inference(demodulation,[status(thm)],[c_809,c_143322]) ).
tcf(c_143442,plain,
( ( sk_c11 = iPr_def_21 )
| ( sk_c11 = iPr_def_17 ) ),
inference(demodulation,[status(thm)],[c_759,c_143322]) ).
tcf(c_143519,plain,
( ( iPr_def_15 = iPr_def_21 )
| ( sk_c11 = iPr_def_17 ) ),
inference(light_normalisation,[status(thm)],[c_143430,c_140558]) ).
tcf(c_143524,plain,
( ( iPr_def_29 = iPr_def_30 )
| ( iPr_def_15 = iPr_def_21 ) ),
inference(light_normalisation,[status(thm)],[c_143419,c_140558]) ).
tcf(c_143527,plain,
( ( iPr_def_15 = iPr_def_28 )
| ( iPr_def_15 = iPr_def_21 ) ),
inference(light_normalisation,[status(thm)],[c_143416,c_140558]) ).
tcf(c_143530,plain,
( ( iPr_def_27 = iPr_def_29 )
| ( iPr_def_15 = iPr_def_21 ) ),
inference(light_normalisation,[status(thm)],[c_143348,c_140558]) ).
tcf(c_143640,plain,
( ( sk_c11 = iPr_def_17 )
| ~ iPr_def_14 ),
inference(equality_resolution_simp,[status(thm)],[c_143371]) ).
tcf(c_143992,plain,
( ( sk_c10 = iPr_def_15 )
| ~ iPr_def_14 ),
inference(backward_subsumption_resolution,[status(thm)],[c_40967,c_143436]) ).
tcf(c_144779,plain,
sk_c11 = iPr_def_17,
inference(global_subsumption_just,[status(thm)],[c_143442,c_814,c_816,c_727,c_1610,c_2531,c_2821,c_5638,c_7922,c_8473,c_9989,c_14830,c_14854,c_14866,c_21040,c_28963,c_36890,c_36891,c_38873,c_39312,c_39884,c_53445,c_54460,c_54457,c_54583,c_55570,c_55838,c_61547,c_66390,c_72334,c_72488,c_84788,c_99071,c_99072,c_99645,c_100099,c_102097,c_117622,c_138931,c_143640,c_143519,c_143442]) ).
tcf(c_144868,plain,
inverse(iPr_def_15) = iPr_def_17,
inference(demodulation,[status(thm)],[c_39874,c_144779]) ).
tcf(c_145038,plain,
multiply(sk_c2,iPr_def_17) = iPr_def_27,
inference(demodulation,[status(thm)],[c_739,c_144779]) ).
tcf(c_145049,plain,
iPr_def_21 = iPr_def_27,
inference(light_normalisation,[status(thm)],[c_145038,c_140454]) ).
tcf(c_148534,plain,
iPr_def_15 = iPr_def_28,
inference(global_subsumption_just,[status(thm)],[c_32561,c_814,c_816,c_727,c_1610,c_2531,c_2821,c_5638,c_7922,c_8473,c_9989,c_21040,c_28963,c_32460,c_33335,c_33540,c_36890,c_36891,c_38808,c_39253,c_39884,c_40928,c_53445,c_54460,c_54457,c_54583,c_55570,c_55838,c_61547,c_66390,c_72334,c_72488,c_84788,c_99071,c_99072,c_99645,c_100099,c_102097,c_117622,c_138931,c_143527,c_143431]) ).
tcf(c_149200,plain,
~ iPr_def_14,
inference(global_subsumption_just,[status(thm)],[c_143992,c_814,c_816,c_727,c_1365,c_1610,c_1651,c_2531,c_2821,c_5444,c_5638,c_7922,c_8473,c_9989,c_21040,c_28963,c_32460,c_33335,c_33540,c_36890,c_36891,c_38808,c_39253,c_39884,c_40175,c_40928,c_53445,c_54460,c_54457,c_54583,c_55570,c_55838,c_61547,c_66390,c_72334,c_72488,c_84788,c_99071,c_99072,c_99645,c_100099,c_102097,c_103262,c_111333,c_117622,c_138931,c_143527,c_143431,c_143424,c_143992,c_144779]) ).
tcf(c_149519,plain,
! [X0: $i] :
( ( iPr_def_29 = iPr_def_30 )
| ( multiply(iPr_def_15,X0) = X0 ) ),
inference(light_normalisation,[status(thm)],[c_13782,c_140615,c_143322]) ).
tcf(c_149545,plain,
( ( iPr_def_29 = iPr_def_30 )
| ( sk_c10 = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_149519,c_54030]) ).
tcf(c_149832,plain,
iPr_def_29 = iPr_def_30,
inference(global_subsumption_just,[status(thm)],[c_13783,c_178,c_814,c_816,c_818,c_727,c_1365,c_1471,c_1475,c_1610,c_1651,c_2316,c_2531,c_2821,c_2998,c_5064,c_5444,c_5638,c_5705,c_7922,c_8473,c_9266,c_9634,c_9989,c_14830,c_14854,c_14866,c_21040,c_28954,c_28963,c_32460,c_33335,c_33540,c_36890,c_36891,c_38873,c_38808,c_39184,c_39312,c_39253,c_39884,c_40175,c_40928,c_41714,c_53445,c_54460,c_54457,c_54583,c_55570,c_55838,c_56388,c_57100,c_61547,c_65346,c_66390,c_72334,c_72488,c_84788,c_90204,c_98865,c_99071,c_99072,c_99493,c_99645,c_99823,c_100099,c_101199,c_102097,c_103130,c_103262,c_111333,c_117622,c_122441,c_135215,c_138931,c_143640,c_143527,c_143524,c_143519,c_143432,c_143431,c_143442,c_143424,c_143992,c_149545]) ).
tcf(c_149862,plain,
inverse(iPr_def_29) = sk_c1,
inference(demodulation,[status(thm)],[c_72374,c_149832]) ).
tcf(c_149901,plain,
multiply(iPr_def_29,iPr_def_29) = sk_c10,
inference(demodulation,[status(thm)],[c_13344,c_149832]) ).
tcf(c_150660,plain,
( ( iPr_def_27 = iPr_def_29 )
| ( sk_c10 = iPr_def_21 ) ),
inference(global_subsumption_just,[status(thm)],[c_85418,c_1475,c_1521,c_1887,c_24505,c_61541,c_121903,c_143530]) ).
tcf(c_150662,plain,
iPr_def_27 = iPr_def_29,
inference(global_subsumption_just,[status(thm)],[c_150660,c_814,c_816,c_820,c_727,c_1365,c_1610,c_1651,c_1810,c_1811,c_2531,c_2821,c_3374,c_5444,c_5638,c_7922,c_8473,c_9989,c_14830,c_14854,c_14866,c_21040,c_28963,c_32460,c_33335,c_33540,c_36890,c_36891,c_38873,c_38808,c_39184,c_39312,c_39253,c_39884,c_40175,c_40928,c_53445,c_54460,c_54457,c_54583,c_55570,c_55838,c_56392,c_61547,c_66390,c_72334,c_72488,c_84788,c_99071,c_99072,c_99645,c_100099,c_102097,c_103262,c_111333,c_117622,c_127003,c_138931,c_143640,c_143530,c_143527,c_143519,c_143431,c_143442,c_143349,c_143424,c_143992,c_150660]) ).
tcf(c_150664,plain,
iPr_def_21 = iPr_def_29,
inference(light_normalisation,[status(thm)],[c_150662,c_145049]) ).
tcf(c_150665,plain,
multiply(iPr_def_21,iPr_def_21) = sk_c10,
inference(demodulation,[status(thm)],[c_149901,c_150664]) ).
tcf(c_150675,plain,
inverse(iPr_def_21) = sk_c1,
inference(demodulation,[status(thm)],[c_149862,c_150664]) ).
tcf(c_150678,plain,
iPr_def_21 = iPr_def_30,
inference(demodulation,[status(thm)],[c_149832,c_150664]) ).
tcf(c_150732,plain,
sk_c1 = iPr_def_21,
inference(light_normalisation,[status(thm)],[c_150675,c_140558]) ).
tcf(c_150842,plain,
( ( iPr_def_16 = iPr_def_18 )
| ( iPr_def_15 = iPr_def_21 ) ),
inference(demodulation,[status(thm)],[c_72383,c_150732]) ).
tcf(c_150843,plain,
( ( iPr_def_18 = iPr_def_19 )
| ( iPr_def_15 = iPr_def_21 ) ),
inference(demodulation,[status(thm)],[c_72382,c_150732]) ).
tcf(c_150847,plain,
( ( iPr_def_16 = iPr_def_21 )
| ( iPr_def_15 = iPr_def_21 ) ),
inference(demodulation,[status(thm)],[c_72378,c_150732]) ).
tcf(c_150873,plain,
iPr_def_18 = iPr_def_19,
inference(global_subsumption_just,[status(thm)],[c_13790,c_814,c_816,c_727,c_742,c_1365,c_1610,c_1651,c_1887,c_2531,c_2705,c_2821,c_3687,c_5444,c_5638,c_5640,c_7922,c_8088,c_8473,c_9989,c_14830,c_14854,c_14866,c_21040,c_28963,c_32460,c_32710,c_33335,c_33540,c_34691,c_34692,c_36609,c_36890,c_36891,c_38873,c_38808,c_39184,c_39312,c_39253,c_39884,c_40175,c_40928,c_53445,c_54460,c_54457,c_54583,c_55025,c_55570,c_55838,c_56567,c_61544,c_61547,c_61942,c_64867,c_64880,c_66390,c_69020,c_72334,c_72488,c_75913,c_84788,c_90235,c_92503,c_95951,c_96827,c_96829,c_99071,c_99072,c_99645,c_100099,c_102097,c_103262,c_111333,c_117622,c_121903,c_138931,c_141340,c_143640,c_143527,c_143519,c_143431,c_143442,c_143424,c_143992,c_150678,c_150665,c_150843]) ).
tcf(c_150907,plain,
sk_c10 = iPr_def_21,
inference(demodulation,[status(thm)],[c_150665,c_140615]) ).
tcf(c_150921,plain,
( ~ iPr_def_13
| ( iPr_def_18 != iPr_def_21 )
| ( iPr_def_16 != iPr_def_21 ) ),
inference(demodulation,[status(thm)],[c_4991,c_150907]) ).
tcf(c_150997,plain,
iPr_def_16 = iPr_def_18,
inference(global_subsumption_just,[status(thm)],[c_13791,c_814,c_816,c_727,c_742,c_1887,c_2581,c_3558,c_5640,c_7916,c_8473,c_21040,c_32710,c_34691,c_34692,c_36609,c_39184,c_53445,c_55025,c_56567,c_61544,c_61547,c_61942,c_64867,c_64880,c_69020,c_72488,c_75913,c_90235,c_93342,c_95951,c_96827,c_96829,c_117622,c_121903,c_140434,c_141340,c_148534,c_149200,c_150678,c_150665,c_150842]) ).
tcf(c_151005,plain,
inverse(iPr_def_16) = sk_c9,
inference(demodulation,[status(thm)],[c_66380,c_150997]) ).
tcf(c_151007,plain,
inverse(sk_c9) = iPr_def_16,
inference(demodulation,[status(thm)],[c_730,c_150997]) ).
tcf(c_151042,plain,
iPr_def_16 = iPr_def_21,
inference(global_subsumption_just,[status(thm)],[c_13792,c_814,c_816,c_727,c_742,c_1365,c_1610,c_1651,c_1887,c_1892,c_1893,c_1905,c_2531,c_2581,c_2661,c_2821,c_2860,c_3558,c_3825,c_5444,c_5638,c_5640,c_6247,c_7916,c_7922,c_8473,c_8588,c_8789,c_9989,c_10363,c_14830,c_14854,c_14866,c_15999,c_21040,c_28963,c_32460,c_32710,c_33335,c_33540,c_34691,c_34692,c_36609,c_36890,c_36891,c_38873,c_38808,c_39184,c_39312,c_39253,c_39884,c_40175,c_40928,c_53445,c_54460,c_54457,c_54583,c_55025,c_55570,c_55838,c_56567,c_61541,c_61544,c_61547,c_61942,c_64867,c_64880,c_66390,c_69020,c_69509,c_72334,c_72488,c_75913,c_79777,c_84788,c_88003,c_90235,c_93342,c_95951,c_96827,c_96829,c_99071,c_99072,c_99645,c_100099,c_102097,c_103262,c_111333,c_117622,c_121903,c_138931,c_141340,c_143640,c_143527,c_143519,c_143431,c_143442,c_143424,c_143992,c_150678,c_150665,c_150847,c_150842,c_150873]) ).
tcf(c_151044,plain,
sk_c10 = iPr_def_16,
inference(demodulation,[status(thm)],[c_150907,c_151042]) ).
tcf(c_151054,plain,
! [X0: $i] : multiply(iPr_def_16,X0) = X0,
inference(demodulation,[status(thm)],[c_140615,c_151042]) ).
tcf(c_151063,plain,
inverse(iPr_def_16) = iPr_def_16,
inference(demodulation,[status(thm)],[c_140558,c_151042]) ).
tcf(c_151072,plain,
sk_c9 = iPr_def_15,
inference(demodulation,[status(thm)],[c_43317,c_151054]) ).
tcf(c_151074,plain,
inverse(iPr_def_15) = iPr_def_16,
inference(demodulation,[status(thm)],[c_151007,c_151072]) ).
tcf(c_151075,plain,
inverse(iPr_def_16) = iPr_def_15,
inference(demodulation,[status(thm)],[c_151005,c_151072]) ).
tcf(c_151077,plain,
iPr_def_16 = iPr_def_17,
inference(demodulation,[status(thm)],[c_144868,c_151074]) ).
tcf(c_151081,plain,
sk_c11 = iPr_def_16,
inference(demodulation,[status(thm)],[c_144779,c_151077]) ).
tcf(c_151157,plain,
iPr_def_15 = iPr_def_16,
inference(demodulation,[status(thm)],[c_151063,c_151075]) ).
tcf(c_151169,plain,
iPr_def_15 = iPr_def_18,
inference(demodulation,[status(thm)],[c_150997,c_151157]) ).
tcf(c_151170,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_151169,c_151044,c_151081,c_151042,c_150997,c_150921,c_150665,c_149200,c_141340,c_140434,c_72488,c_53445,c_43287,c_39184,c_36890,c_21040,c_8794,c_8369,c_6249,c_6232,c_5399,c_1899,c_1887,c_1657]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GRP238-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.03 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.08/0.34 % Computer : n004.cluster.edu
% 0.08/0.34 % Model : x86_64 x86_64
% 0.08/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.34 % Memory : 8046.5625MB
% 0.08/0.34 % OS : Linux 6.8.0-71-generic
% 0.08/0.34 % CPULimit : 300
% 0.08/0.34 % WCLimit : 300
% 0.08/0.34 % DateTime : Wed Sep 23 14:13:39 UTC 2026
% 0.08/0.34 % CPUTime :
% 0.08/0.35 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.13/0.38 Running first-order theorem proving
% 0.13/0.38 Running: /export/starexec/sandbox/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.13/0.39
% 0.13/0.39 % ======== iProver multi-core TPTP/SMT =========
% 0.13/0.39
% 0.13/0.39 % Detected problem language: tptp
% 0.13/0.40 % Proving...
% 62.81/9.40 % SZS status Started for theBenchmark.p
% 62.81/9.40 % SZS status Unsatisfiable for theBenchmark.p
% 62.81/9.40
% 62.81/9.40 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 62.81/9.40
% 62.81/9.40 % ------ iProver source info
% 62.81/9.40
% 62.81/9.40 % git: date: 2026-07-19 20:42:38 +0200
% 62.81/9.40 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 62.81/9.40 % git: non_committed_changes: false
% 62.81/9.40
% 62.81/9.40 % ------ Parsing...% successful
% 62.81/9.40
% 62.81/9.40
% 62.81/9.40 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 62.81/9.40
% 62.81/9.40 % ------ Preprocessing... sup_sim: 0 sf_s rm: 0 0s sf_e pe_s pe_e %
% 62.81/9.40
% 62.81/9.40 % ------ Preprocessing... gs_s sp: 6 0s gs_e snvd_s sp: 0 0s snvd_e %
% 62.81/9.40
% 62.81/9.40 % ------ Preprocessing... sf_s rm: 0 0s sf_e
% 62.81/9.40 % ------ Proving...
% 62.81/9.40 % ------ Problem Properties
% 62.81/9.40
% 62.81/9.40 %
% 62.81/9.40 % clauses 85
% 62.81/9.40 % conjectures 66
% 62.81/9.40 % EPR 61
% 62.81/9.40 % Horn 24
% 62.81/9.40 % unary 19
% 62.81/9.40 % binary 60
% 62.81/9.40 % lits 160
% 62.81/9.40 % lits eq 150
% 62.81/9.40 % fd_pure 0
% 62.81/9.40 % fd_pseudo 0
% 62.81/9.40 % fd_cond 0
% 62.81/9.40 % fd_pseudo_cond 0
% 62.81/9.40 % AC symbols 0
% 62.81/9.40
% 62.81/9.40 % ------ Schedule dynamic 5 is on
% 62.81/9.40
% 62.81/9.40 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 62.81/9.40
% 62.81/9.40
% 62.81/9.40 % ------
% 62.81/9.40 % Current options:
% 62.81/9.40 % ------
% 62.81/9.40
% 62.81/9.40
% 62.81/9.40 %
% 62.81/9.40
% 62.81/9.40 % ------ Proving...
% 62.81/9.40 %
% 62.81/9.40
% 62.81/9.40 % SZS status Unsatisfiable for theBenchmark.p
% 62.81/9.40
% 62.81/9.40 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 62.81/9.41
% 62.81/9.41
%------------------------------------------------------------------------------