%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : GRP258-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 : n009.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:37 PM UTC 2026
% Result : Unsatisfiable 29.46s 4.80s
% Output : CNFRefutation 29.46s
% Verified :
% SZS Type : Refutation
% Derivation depth : 39
% Number of leaves : 77
% Syntax : Number of formulae : 760 ( 167 unt; 15 def)
% Number of atoms : 2693 (1507 equ)
% Maximal formula atoms : 17 ( 3 avg)
% Number of connectives : 1259 ( 411 ~; 848 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 27 ( 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 : 21 ( 19 usr; 20 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 12 con; 0-2 aty)
% Number of variables : 243 ( 0 sgn 243 !; 0 ?; 204 :)
% 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_c12) = sk_c11
| multiply(sk_c1,sk_c12) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_1) ).
fof(f6,plain,
( sk_c11 = multiply(sk_c4,sk_c12)
| multiply(sk_c1,sk_c12) = sk_c11 ),
inference(reorient_equations,[],[f5]) ).
fof(f7,negated_conjecture,
( inverse(sk_c4) = sk_c12
| multiply(sk_c1,sk_c12) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_2) ).
fof(f8,plain,
( sk_c12 = inverse(sk_c4)
| multiply(sk_c1,sk_c12) = sk_c11 ),
inference(reorient_equations,[],[f7]) ).
fof(f10,negated_conjecture,
( inverse(sk_c5) = sk_c11
| multiply(sk_c1,sk_c12) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_4) ).
fof(f11,plain,
( sk_c11 = inverse(sk_c5)
| multiply(sk_c1,sk_c12) = sk_c11 ),
inference(reorient_equations,[],[f10]) ).
fof(f12,negated_conjecture,
( multiply(sk_c6,sk_c9) = sk_c12
| multiply(sk_c1,sk_c12) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_5) ).
fof(f13,plain,
( sk_c12 = multiply(sk_c6,sk_c9)
| multiply(sk_c1,sk_c12) = sk_c11 ),
inference(reorient_equations,[],[f12]) ).
fof(f14,negated_conjecture,
( inverse(sk_c6) = sk_c9
| multiply(sk_c1,sk_c12) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_6) ).
fof(f15,plain,
( sk_c9 = inverse(sk_c6)
| multiply(sk_c1,sk_c12) = sk_c11 ),
inference(reorient_equations,[],[f14]) ).
fof(f16,negated_conjecture,
( multiply(sk_c9,sk_c11) = sk_c12
| multiply(sk_c1,sk_c12) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_7) ).
fof(f17,plain,
( sk_c12 = multiply(sk_c9,sk_c11)
| multiply(sk_c1,sk_c12) = sk_c11 ),
inference(reorient_equations,[],[f16]) ).
fof(f19,negated_conjecture,
( inverse(sk_c7) = sk_c9
| multiply(sk_c1,sk_c12) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_9) ).
fof(f20,plain,
( sk_c9 = inverse(sk_c7)
| multiply(sk_c1,sk_c12) = sk_c11 ),
inference(reorient_equations,[],[f19]) ).
fof(f23,negated_conjecture,
( multiply(sk_c4,sk_c12) = sk_c11
| inverse(sk_c1) = sk_c12 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_11) ).
fof(f24,plain,
( sk_c11 = multiply(sk_c4,sk_c12)
| sk_c12 = inverse(sk_c1) ),
inference(reorient_equations,[],[f23]) ).
fof(f25,negated_conjecture,
( inverse(sk_c4) = sk_c12
| inverse(sk_c1) = sk_c12 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_12) ).
fof(f26,plain,
( sk_c12 = inverse(sk_c4)
| sk_c12 = inverse(sk_c1) ),
inference(reorient_equations,[],[f25]) ).
fof(f29,negated_conjecture,
( inverse(sk_c5) = sk_c11
| inverse(sk_c1) = sk_c12 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_14) ).
fof(f30,plain,
( sk_c11 = inverse(sk_c5)
| sk_c12 = inverse(sk_c1) ),
inference(reorient_equations,[],[f29]) ).
fof(f31,negated_conjecture,
( multiply(sk_c6,sk_c9) = sk_c12
| inverse(sk_c1) = sk_c12 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_15) ).
fof(f32,plain,
( sk_c12 = multiply(sk_c6,sk_c9)
| sk_c12 = inverse(sk_c1) ),
inference(reorient_equations,[],[f31]) ).
fof(f33,negated_conjecture,
( inverse(sk_c6) = sk_c9
| inverse(sk_c1) = sk_c12 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_16) ).
fof(f34,plain,
( sk_c9 = inverse(sk_c6)
| sk_c12 = inverse(sk_c1) ),
inference(reorient_equations,[],[f33]) ).
fof(f35,negated_conjecture,
( multiply(sk_c9,sk_c11) = sk_c12
| inverse(sk_c1) = sk_c12 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_17) ).
fof(f36,plain,
( sk_c12 = multiply(sk_c9,sk_c11)
| sk_c12 = inverse(sk_c1) ),
inference(reorient_equations,[],[f35]) ).
fof(f39,negated_conjecture,
( inverse(sk_c7) = sk_c9
| inverse(sk_c1) = sk_c12 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_19) ).
fof(f40,plain,
( sk_c9 = inverse(sk_c7)
| sk_c12 = inverse(sk_c1) ),
inference(reorient_equations,[],[f39]) ).
fof(f43,negated_conjecture,
( multiply(sk_c4,sk_c12) = sk_c11
| multiply(sk_c2,sk_c11) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_21) ).
fof(f44,plain,
( sk_c11 = multiply(sk_c4,sk_c12)
| sk_c10 = multiply(sk_c2,sk_c11) ),
inference(reorient_equations,[],[f43]) ).
fof(f45,negated_conjecture,
( inverse(sk_c4) = sk_c12
| multiply(sk_c2,sk_c11) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_22) ).
fof(f46,plain,
( sk_c12 = inverse(sk_c4)
| sk_c10 = multiply(sk_c2,sk_c11) ),
inference(reorient_equations,[],[f45]) ).
fof(f47,negated_conjecture,
( multiply(sk_c5,sk_c11) = sk_c10
| multiply(sk_c2,sk_c11) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_23) ).
fof(f48,plain,
( multiply(sk_c5,sk_c11) = sk_c10
| sk_c10 = multiply(sk_c2,sk_c11) ),
inference(reorient_equations,[],[f47]) ).
fof(f49,negated_conjecture,
( inverse(sk_c5) = sk_c11
| multiply(sk_c2,sk_c11) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_24) ).
fof(f50,plain,
( sk_c11 = inverse(sk_c5)
| sk_c10 = multiply(sk_c2,sk_c11) ),
inference(reorient_equations,[],[f49]) ).
fof(f51,negated_conjecture,
( multiply(sk_c6,sk_c9) = sk_c12
| multiply(sk_c2,sk_c11) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_25) ).
fof(f52,plain,
( sk_c12 = multiply(sk_c6,sk_c9)
| sk_c10 = multiply(sk_c2,sk_c11) ),
inference(reorient_equations,[],[f51]) ).
fof(f53,negated_conjecture,
( inverse(sk_c6) = sk_c9
| multiply(sk_c2,sk_c11) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_26) ).
fof(f54,plain,
( sk_c9 = inverse(sk_c6)
| sk_c10 = multiply(sk_c2,sk_c11) ),
inference(reorient_equations,[],[f53]) ).
fof(f55,negated_conjecture,
( multiply(sk_c9,sk_c11) = sk_c12
| multiply(sk_c2,sk_c11) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_27) ).
fof(f56,plain,
( sk_c12 = multiply(sk_c9,sk_c11)
| sk_c10 = multiply(sk_c2,sk_c11) ),
inference(reorient_equations,[],[f55]) ).
fof(f59,negated_conjecture,
( inverse(sk_c7) = sk_c9
| multiply(sk_c2,sk_c11) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_29) ).
fof(f60,plain,
( sk_c9 = inverse(sk_c7)
| sk_c10 = multiply(sk_c2,sk_c11) ),
inference(reorient_equations,[],[f59]) ).
fof(f63,negated_conjecture,
( multiply(sk_c4,sk_c12) = sk_c11
| inverse(sk_c2) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_31) ).
fof(f64,plain,
( sk_c11 = multiply(sk_c4,sk_c12)
| sk_c11 = inverse(sk_c2) ),
inference(reorient_equations,[],[f63]) ).
fof(f65,negated_conjecture,
( inverse(sk_c4) = sk_c12
| inverse(sk_c2) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_32) ).
fof(f66,plain,
( sk_c12 = inverse(sk_c4)
| sk_c11 = inverse(sk_c2) ),
inference(reorient_equations,[],[f65]) ).
fof(f67,negated_conjecture,
( multiply(sk_c5,sk_c11) = sk_c10
| inverse(sk_c2) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_33) ).
fof(f68,plain,
( multiply(sk_c5,sk_c11) = sk_c10
| sk_c11 = inverse(sk_c2) ),
inference(reorient_equations,[],[f67]) ).
fof(f69,negated_conjecture,
( inverse(sk_c5) = sk_c11
| inverse(sk_c2) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_34) ).
fof(f70,plain,
( sk_c11 = inverse(sk_c5)
| sk_c11 = inverse(sk_c2) ),
inference(reorient_equations,[],[f69]) ).
fof(f71,negated_conjecture,
( multiply(sk_c6,sk_c9) = sk_c12
| inverse(sk_c2) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_35) ).
fof(f72,plain,
( sk_c12 = multiply(sk_c6,sk_c9)
| sk_c11 = inverse(sk_c2) ),
inference(reorient_equations,[],[f71]) ).
fof(f73,negated_conjecture,
( inverse(sk_c6) = sk_c9
| inverse(sk_c2) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_36) ).
fof(f74,plain,
( sk_c9 = inverse(sk_c6)
| sk_c11 = inverse(sk_c2) ),
inference(reorient_equations,[],[f73]) ).
fof(f75,negated_conjecture,
( multiply(sk_c9,sk_c11) = sk_c12
| inverse(sk_c2) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_37) ).
fof(f76,plain,
( sk_c12 = multiply(sk_c9,sk_c11)
| sk_c11 = inverse(sk_c2) ),
inference(reorient_equations,[],[f75]) ).
fof(f79,negated_conjecture,
( inverse(sk_c7) = sk_c9
| inverse(sk_c2) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_39) ).
fof(f80,plain,
( sk_c9 = inverse(sk_c7)
| sk_c11 = inverse(sk_c2) ),
inference(reorient_equations,[],[f79]) ).
fof(f83,negated_conjecture,
( multiply(sk_c4,sk_c12) = sk_c11
| multiply(sk_c10,sk_c12) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_41) ).
fof(f84,plain,
( sk_c11 = multiply(sk_c4,sk_c12)
| sk_c11 = multiply(sk_c10,sk_c12) ),
inference(reorient_equations,[],[f83]) ).
fof(f85,negated_conjecture,
( inverse(sk_c4) = sk_c12
| multiply(sk_c10,sk_c12) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_42) ).
fof(f86,plain,
( sk_c12 = inverse(sk_c4)
| sk_c11 = multiply(sk_c10,sk_c12) ),
inference(reorient_equations,[],[f85]) ).
fof(f87,negated_conjecture,
( multiply(sk_c5,sk_c11) = sk_c10
| multiply(sk_c10,sk_c12) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_43) ).
fof(f88,plain,
( multiply(sk_c5,sk_c11) = sk_c10
| sk_c11 = multiply(sk_c10,sk_c12) ),
inference(reorient_equations,[],[f87]) ).
fof(f89,negated_conjecture,
( inverse(sk_c5) = sk_c11
| multiply(sk_c10,sk_c12) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_44) ).
fof(f90,plain,
( sk_c11 = inverse(sk_c5)
| sk_c11 = multiply(sk_c10,sk_c12) ),
inference(reorient_equations,[],[f89]) ).
fof(f91,negated_conjecture,
( multiply(sk_c6,sk_c9) = sk_c12
| multiply(sk_c10,sk_c12) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_45) ).
fof(f92,plain,
( sk_c12 = multiply(sk_c6,sk_c9)
| sk_c11 = multiply(sk_c10,sk_c12) ),
inference(reorient_equations,[],[f91]) ).
fof(f93,negated_conjecture,
( inverse(sk_c6) = sk_c9
| multiply(sk_c10,sk_c12) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_46) ).
fof(f94,plain,
( sk_c9 = inverse(sk_c6)
| sk_c11 = multiply(sk_c10,sk_c12) ),
inference(reorient_equations,[],[f93]) ).
fof(f95,negated_conjecture,
( multiply(sk_c9,sk_c11) = sk_c12
| multiply(sk_c10,sk_c12) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_47) ).
fof(f96,plain,
( sk_c12 = multiply(sk_c9,sk_c11)
| sk_c11 = multiply(sk_c10,sk_c12) ),
inference(reorient_equations,[],[f95]) ).
fof(f99,negated_conjecture,
( inverse(sk_c7) = sk_c9
| multiply(sk_c10,sk_c12) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_49) ).
fof(f100,plain,
( sk_c9 = inverse(sk_c7)
| sk_c11 = multiply(sk_c10,sk_c12) ),
inference(reorient_equations,[],[f99]) ).
fof(f103,negated_conjecture,
( multiply(sk_c4,sk_c12) = sk_c11
| multiply(sk_c3,sk_c10) = sk_c12 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_51) ).
fof(f104,plain,
( sk_c11 = multiply(sk_c4,sk_c12)
| sk_c12 = multiply(sk_c3,sk_c10) ),
inference(reorient_equations,[],[f103]) ).
fof(f105,negated_conjecture,
( inverse(sk_c4) = sk_c12
| multiply(sk_c3,sk_c10) = sk_c12 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_52) ).
fof(f106,plain,
( sk_c12 = inverse(sk_c4)
| sk_c12 = multiply(sk_c3,sk_c10) ),
inference(reorient_equations,[],[f105]) ).
fof(f107,negated_conjecture,
( multiply(sk_c5,sk_c11) = sk_c10
| multiply(sk_c3,sk_c10) = sk_c12 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_53) ).
fof(f108,plain,
( multiply(sk_c5,sk_c11) = sk_c10
| sk_c12 = multiply(sk_c3,sk_c10) ),
inference(reorient_equations,[],[f107]) ).
fof(f109,negated_conjecture,
( inverse(sk_c5) = sk_c11
| multiply(sk_c3,sk_c10) = sk_c12 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_54) ).
fof(f110,plain,
( sk_c11 = inverse(sk_c5)
| sk_c12 = multiply(sk_c3,sk_c10) ),
inference(reorient_equations,[],[f109]) ).
fof(f111,negated_conjecture,
( multiply(sk_c6,sk_c9) = sk_c12
| multiply(sk_c3,sk_c10) = sk_c12 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_55) ).
fof(f112,plain,
( sk_c12 = multiply(sk_c6,sk_c9)
| sk_c12 = multiply(sk_c3,sk_c10) ),
inference(reorient_equations,[],[f111]) ).
fof(f113,negated_conjecture,
( inverse(sk_c6) = sk_c9
| multiply(sk_c3,sk_c10) = sk_c12 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_56) ).
fof(f114,plain,
( sk_c9 = inverse(sk_c6)
| sk_c12 = multiply(sk_c3,sk_c10) ),
inference(reorient_equations,[],[f113]) ).
fof(f115,negated_conjecture,
( multiply(sk_c9,sk_c11) = sk_c12
| multiply(sk_c3,sk_c10) = sk_c12 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_57) ).
fof(f116,plain,
( sk_c12 = multiply(sk_c9,sk_c11)
| sk_c12 = multiply(sk_c3,sk_c10) ),
inference(reorient_equations,[],[f115]) ).
fof(f119,negated_conjecture,
( inverse(sk_c7) = sk_c9
| multiply(sk_c3,sk_c10) = sk_c12 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_59) ).
fof(f120,plain,
( sk_c9 = inverse(sk_c7)
| sk_c12 = multiply(sk_c3,sk_c10) ),
inference(reorient_equations,[],[f119]) ).
fof(f123,negated_conjecture,
( multiply(sk_c4,sk_c12) = sk_c11
| inverse(sk_c3) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_61) ).
fof(f124,plain,
( sk_c11 = multiply(sk_c4,sk_c12)
| sk_c10 = inverse(sk_c3) ),
inference(reorient_equations,[],[f123]) ).
fof(f125,negated_conjecture,
( inverse(sk_c4) = sk_c12
| inverse(sk_c3) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_62) ).
fof(f126,plain,
( sk_c12 = inverse(sk_c4)
| sk_c10 = inverse(sk_c3) ),
inference(reorient_equations,[],[f125]) ).
fof(f127,negated_conjecture,
( multiply(sk_c5,sk_c11) = sk_c10
| inverse(sk_c3) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_63) ).
fof(f128,plain,
( multiply(sk_c5,sk_c11) = sk_c10
| sk_c10 = inverse(sk_c3) ),
inference(reorient_equations,[],[f127]) ).
fof(f129,negated_conjecture,
( inverse(sk_c5) = sk_c11
| inverse(sk_c3) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_64) ).
fof(f130,plain,
( sk_c11 = inverse(sk_c5)
| sk_c10 = inverse(sk_c3) ),
inference(reorient_equations,[],[f129]) ).
fof(f131,negated_conjecture,
( multiply(sk_c6,sk_c9) = sk_c12
| inverse(sk_c3) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_65) ).
fof(f132,plain,
( sk_c12 = multiply(sk_c6,sk_c9)
| sk_c10 = inverse(sk_c3) ),
inference(reorient_equations,[],[f131]) ).
fof(f133,negated_conjecture,
( inverse(sk_c6) = sk_c9
| inverse(sk_c3) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_66) ).
fof(f134,plain,
( sk_c9 = inverse(sk_c6)
| sk_c10 = inverse(sk_c3) ),
inference(reorient_equations,[],[f133]) ).
fof(f135,negated_conjecture,
( multiply(sk_c9,sk_c11) = sk_c12
| inverse(sk_c3) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_67) ).
fof(f136,plain,
( sk_c12 = multiply(sk_c9,sk_c11)
| sk_c10 = inverse(sk_c3) ),
inference(reorient_equations,[],[f135]) ).
fof(f139,negated_conjecture,
( inverse(sk_c7) = sk_c9
| inverse(sk_c3) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_69) ).
fof(f140,plain,
( sk_c9 = inverse(sk_c7)
| sk_c10 = inverse(sk_c3) ),
inference(reorient_equations,[],[f139]) ).
fof(f143,negated_conjecture,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( multiply(X7,X6) != X8
| inverse(X8) != X6
| inverse(X7) != X8
| multiply(X6,sk_c11) != sk_c12
| inverse(X5) != X6
| multiply(X5,X6) != sk_c12
| inverse(X4) != sk_c11
| multiply(X4,sk_c11) != sk_c10
| inverse(X3) != sk_c12
| multiply(X3,sk_c12) != sk_c11
| inverse(X2) != sk_c10
| multiply(X2,sk_c10) != sk_c12
| multiply(sk_c10,sk_c12) != sk_c11
| inverse(X1) != sk_c11
| multiply(X1,sk_c11) != sk_c10
| inverse(X0) != sk_c12
| multiply(X0,sk_c12) != sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_71) ).
fof(f144,plain,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] :
( multiply(X7,X6) != X8
| inverse(X8) != X6
| inverse(X7) != X8
| sk_c12 != multiply(X6,sk_c11)
| inverse(X5) != X6
| sk_c12 != multiply(X5,X6)
| sk_c11 != inverse(X4)
| sk_c10 != multiply(X4,sk_c11)
| sk_c12 != inverse(X3)
| sk_c11 != multiply(X3,sk_c12)
| sk_c10 != inverse(X2)
| sk_c12 != multiply(X2,sk_c10)
| sk_c11 != multiply(sk_c10,sk_c12)
| sk_c11 != inverse(X1)
| sk_c10 != multiply(X1,sk_c11)
| inverse(X0) != sk_c12
| sk_c11 != multiply(X0,sk_c12) ),
inference(reorient_equations,[],[f143]) ).
fof(f145,plain,
! [X2,X3,X0,X1,X8,X7,X4,X5] :
( multiply(X7,inverse(X5)) != X8
| inverse(X5) != inverse(X8)
| inverse(X7) != X8
| sk_c12 != multiply(inverse(X5),sk_c11)
| sk_c12 != multiply(X5,inverse(X5))
| sk_c11 != inverse(X4)
| sk_c10 != multiply(X4,sk_c11)
| sk_c12 != inverse(X3)
| sk_c11 != multiply(X3,sk_c12)
| sk_c10 != inverse(X2)
| sk_c12 != multiply(X2,sk_c10)
| sk_c11 != multiply(sk_c10,sk_c12)
| sk_c11 != inverse(X1)
| sk_c10 != multiply(X1,sk_c11)
| inverse(X0) != sk_c12
| sk_c11 != multiply(X0,sk_c12) ),
inference(equality_resolution,[],[f144]) ).
fof(f146,plain,
! [X2,X3,X0,X1,X7,X4,X5] :
( inverse(X7) != multiply(X7,inverse(X5))
| inverse(X5) != inverse(inverse(X7))
| sk_c12 != multiply(inverse(X5),sk_c11)
| sk_c12 != multiply(X5,inverse(X5))
| sk_c11 != inverse(X4)
| sk_c10 != multiply(X4,sk_c11)
| sk_c12 != inverse(X3)
| sk_c11 != multiply(X3,sk_c12)
| sk_c10 != inverse(X2)
| sk_c12 != multiply(X2,sk_c10)
| sk_c11 != multiply(sk_c10,sk_c12)
| sk_c11 != inverse(X1)
| sk_c10 != multiply(X1,sk_c11)
| inverse(X0) != sk_c12
| sk_c11 != multiply(X0,sk_c12) ),
inference(equality_resolution,[],[f145]) ).
tcf(c_123,plain,
! [X0: $i] : multiply(identity,X0) = X0,
inference(cnf_transformation,[],[f1]) ).
tcf(c_124,plain,
! [X0: $i] : multiply(inverse(X0),X0) = identity,
inference(cnf_transformation,[],[f3]) ).
tcf(c_125,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(multiply(X0,X1),X2) = multiply(X0,multiply(X1,X2)),
inference(cnf_transformation,[],[f4]) ).
tcf(c_126,negated_conjecture,
( ( multiply(sk_c4,sk_c12) = sk_c11 )
| ( multiply(sk_c1,sk_c12) = sk_c11 ) ),
inference(cnf_transformation,[],[f6]) ).
tcf(c_127,negated_conjecture,
( ( inverse(sk_c4) = sk_c12 )
| ( multiply(sk_c1,sk_c12) = sk_c11 ) ),
inference(cnf_transformation,[],[f8]) ).
tcf(c_129,negated_conjecture,
( ( inverse(sk_c5) = sk_c11 )
| ( multiply(sk_c1,sk_c12) = sk_c11 ) ),
inference(cnf_transformation,[],[f11]) ).
tcf(c_130,negated_conjecture,
( ( multiply(sk_c6,sk_c9) = sk_c12 )
| ( multiply(sk_c1,sk_c12) = sk_c11 ) ),
inference(cnf_transformation,[],[f13]) ).
tcf(c_131,negated_conjecture,
( ( inverse(sk_c6) = sk_c9 )
| ( multiply(sk_c1,sk_c12) = sk_c11 ) ),
inference(cnf_transformation,[],[f15]) ).
tcf(c_132,negated_conjecture,
( ( multiply(sk_c9,sk_c11) = sk_c12 )
| ( multiply(sk_c1,sk_c12) = sk_c11 ) ),
inference(cnf_transformation,[],[f17]) ).
tcf(c_134,negated_conjecture,
( ( inverse(sk_c7) = sk_c9 )
| ( multiply(sk_c1,sk_c12) = sk_c11 ) ),
inference(cnf_transformation,[],[f20]) ).
tcf(c_136,negated_conjecture,
( ( inverse(sk_c1) = sk_c12 )
| ( multiply(sk_c4,sk_c12) = sk_c11 ) ),
inference(cnf_transformation,[],[f24]) ).
tcf(c_137,negated_conjecture,
( ( inverse(sk_c4) = sk_c12 )
| ( inverse(sk_c1) = sk_c12 ) ),
inference(cnf_transformation,[],[f26]) ).
tcf(c_139,negated_conjecture,
( ( inverse(sk_c5) = sk_c11 )
| ( inverse(sk_c1) = sk_c12 ) ),
inference(cnf_transformation,[],[f30]) ).
tcf(c_140,negated_conjecture,
( ( inverse(sk_c1) = sk_c12 )
| ( multiply(sk_c6,sk_c9) = sk_c12 ) ),
inference(cnf_transformation,[],[f32]) ).
tcf(c_141,negated_conjecture,
( ( inverse(sk_c6) = sk_c9 )
| ( inverse(sk_c1) = sk_c12 ) ),
inference(cnf_transformation,[],[f34]) ).
tcf(c_142,negated_conjecture,
( ( inverse(sk_c1) = sk_c12 )
| ( multiply(sk_c9,sk_c11) = sk_c12 ) ),
inference(cnf_transformation,[],[f36]) ).
tcf(c_144,negated_conjecture,
( ( inverse(sk_c7) = sk_c9 )
| ( inverse(sk_c1) = sk_c12 ) ),
inference(cnf_transformation,[],[f40]) ).
tcf(c_146,negated_conjecture,
( ( multiply(sk_c2,sk_c11) = sk_c10 )
| ( multiply(sk_c4,sk_c12) = sk_c11 ) ),
inference(cnf_transformation,[],[f44]) ).
tcf(c_147,negated_conjecture,
( ( inverse(sk_c4) = sk_c12 )
| ( multiply(sk_c2,sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f46]) ).
tcf(c_148,negated_conjecture,
( ( multiply(sk_c2,sk_c11) = sk_c10 )
| ( multiply(sk_c5,sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f48]) ).
tcf(c_149,negated_conjecture,
( ( inverse(sk_c5) = sk_c11 )
| ( multiply(sk_c2,sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f50]) ).
tcf(c_150,negated_conjecture,
( ( multiply(sk_c2,sk_c11) = sk_c10 )
| ( multiply(sk_c6,sk_c9) = sk_c12 ) ),
inference(cnf_transformation,[],[f52]) ).
tcf(c_151,negated_conjecture,
( ( inverse(sk_c6) = sk_c9 )
| ( multiply(sk_c2,sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f54]) ).
tcf(c_152,negated_conjecture,
( ( multiply(sk_c2,sk_c11) = sk_c10 )
| ( multiply(sk_c9,sk_c11) = sk_c12 ) ),
inference(cnf_transformation,[],[f56]) ).
tcf(c_154,negated_conjecture,
( ( inverse(sk_c7) = sk_c9 )
| ( multiply(sk_c2,sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f60]) ).
tcf(c_156,negated_conjecture,
( ( inverse(sk_c2) = sk_c11 )
| ( multiply(sk_c4,sk_c12) = sk_c11 ) ),
inference(cnf_transformation,[],[f64]) ).
tcf(c_157,negated_conjecture,
( ( inverse(sk_c2) = sk_c11 )
| ( inverse(sk_c4) = sk_c12 ) ),
inference(cnf_transformation,[],[f66]) ).
tcf(c_158,negated_conjecture,
( ( inverse(sk_c2) = sk_c11 )
| ( multiply(sk_c5,sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f68]) ).
tcf(c_159,negated_conjecture,
( ( inverse(sk_c2) = sk_c11 )
| ( inverse(sk_c5) = sk_c11 ) ),
inference(cnf_transformation,[],[f70]) ).
tcf(c_160,negated_conjecture,
( ( inverse(sk_c2) = sk_c11 )
| ( multiply(sk_c6,sk_c9) = sk_c12 ) ),
inference(cnf_transformation,[],[f72]) ).
tcf(c_161,negated_conjecture,
( ( inverse(sk_c2) = sk_c11 )
| ( inverse(sk_c6) = sk_c9 ) ),
inference(cnf_transformation,[],[f74]) ).
tcf(c_162,negated_conjecture,
( ( inverse(sk_c2) = sk_c11 )
| ( multiply(sk_c9,sk_c11) = sk_c12 ) ),
inference(cnf_transformation,[],[f76]) ).
tcf(c_164,negated_conjecture,
( ( inverse(sk_c2) = sk_c11 )
| ( inverse(sk_c7) = sk_c9 ) ),
inference(cnf_transformation,[],[f80]) ).
tcf(c_166,negated_conjecture,
( ( multiply(sk_c10,sk_c12) = sk_c11 )
| ( multiply(sk_c4,sk_c12) = sk_c11 ) ),
inference(cnf_transformation,[],[f84]) ).
tcf(c_167,negated_conjecture,
( ( inverse(sk_c4) = sk_c12 )
| ( multiply(sk_c10,sk_c12) = sk_c11 ) ),
inference(cnf_transformation,[],[f86]) ).
tcf(c_168,negated_conjecture,
( ( multiply(sk_c10,sk_c12) = sk_c11 )
| ( multiply(sk_c5,sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f88]) ).
tcf(c_169,negated_conjecture,
( ( inverse(sk_c5) = sk_c11 )
| ( multiply(sk_c10,sk_c12) = sk_c11 ) ),
inference(cnf_transformation,[],[f90]) ).
tcf(c_170,negated_conjecture,
( ( multiply(sk_c6,sk_c9) = sk_c12 )
| ( multiply(sk_c10,sk_c12) = sk_c11 ) ),
inference(cnf_transformation,[],[f92]) ).
tcf(c_171,negated_conjecture,
( ( inverse(sk_c6) = sk_c9 )
| ( multiply(sk_c10,sk_c12) = sk_c11 ) ),
inference(cnf_transformation,[],[f94]) ).
tcf(c_172,negated_conjecture,
( ( multiply(sk_c9,sk_c11) = sk_c12 )
| ( multiply(sk_c10,sk_c12) = sk_c11 ) ),
inference(cnf_transformation,[],[f96]) ).
tcf(c_174,negated_conjecture,
( ( inverse(sk_c7) = sk_c9 )
| ( multiply(sk_c10,sk_c12) = sk_c11 ) ),
inference(cnf_transformation,[],[f100]) ).
tcf(c_176,negated_conjecture,
( ( multiply(sk_c3,sk_c10) = sk_c12 )
| ( multiply(sk_c4,sk_c12) = sk_c11 ) ),
inference(cnf_transformation,[],[f104]) ).
tcf(c_177,negated_conjecture,
( ( inverse(sk_c4) = sk_c12 )
| ( multiply(sk_c3,sk_c10) = sk_c12 ) ),
inference(cnf_transformation,[],[f106]) ).
tcf(c_178,negated_conjecture,
( ( multiply(sk_c3,sk_c10) = sk_c12 )
| ( multiply(sk_c5,sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f108]) ).
tcf(c_179,negated_conjecture,
( ( inverse(sk_c5) = sk_c11 )
| ( multiply(sk_c3,sk_c10) = sk_c12 ) ),
inference(cnf_transformation,[],[f110]) ).
tcf(c_180,negated_conjecture,
( ( multiply(sk_c3,sk_c10) = sk_c12 )
| ( multiply(sk_c6,sk_c9) = sk_c12 ) ),
inference(cnf_transformation,[],[f112]) ).
tcf(c_181,negated_conjecture,
( ( inverse(sk_c6) = sk_c9 )
| ( multiply(sk_c3,sk_c10) = sk_c12 ) ),
inference(cnf_transformation,[],[f114]) ).
tcf(c_182,negated_conjecture,
( ( multiply(sk_c3,sk_c10) = sk_c12 )
| ( multiply(sk_c9,sk_c11) = sk_c12 ) ),
inference(cnf_transformation,[],[f116]) ).
tcf(c_184,negated_conjecture,
( ( inverse(sk_c7) = sk_c9 )
| ( multiply(sk_c3,sk_c10) = sk_c12 ) ),
inference(cnf_transformation,[],[f120]) ).
tcf(c_186,negated_conjecture,
( ( inverse(sk_c3) = sk_c10 )
| ( multiply(sk_c4,sk_c12) = sk_c11 ) ),
inference(cnf_transformation,[],[f124]) ).
tcf(c_187,negated_conjecture,
( ( inverse(sk_c3) = sk_c10 )
| ( inverse(sk_c4) = sk_c12 ) ),
inference(cnf_transformation,[],[f126]) ).
tcf(c_188,negated_conjecture,
( ( inverse(sk_c3) = sk_c10 )
| ( multiply(sk_c5,sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f128]) ).
tcf(c_189,negated_conjecture,
( ( inverse(sk_c3) = sk_c10 )
| ( inverse(sk_c5) = sk_c11 ) ),
inference(cnf_transformation,[],[f130]) ).
tcf(c_190,negated_conjecture,
( ( inverse(sk_c3) = sk_c10 )
| ( multiply(sk_c6,sk_c9) = sk_c12 ) ),
inference(cnf_transformation,[],[f132]) ).
tcf(c_191,negated_conjecture,
( ( inverse(sk_c3) = sk_c10 )
| ( inverse(sk_c6) = sk_c9 ) ),
inference(cnf_transformation,[],[f134]) ).
tcf(c_192,negated_conjecture,
( ( inverse(sk_c3) = sk_c10 )
| ( multiply(sk_c9,sk_c11) = sk_c12 ) ),
inference(cnf_transformation,[],[f136]) ).
tcf(c_194,negated_conjecture,
( ( inverse(sk_c3) = sk_c10 )
| ( inverse(sk_c7) = sk_c9 ) ),
inference(cnf_transformation,[],[f140]) ).
tcf(c_196,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i] :
( ( inverse(X6) != sk_c11 )
| ( inverse(X5) != sk_c11 )
| ( inverse(X4) != sk_c12 )
| ( inverse(X3) != sk_c10 )
| ( inverse(X2) != sk_c12 )
| ( multiply(sk_c10,sk_c12) != sk_c11 )
| ( inverse(inverse(X0)) != inverse(X1) )
| ( multiply(X6,sk_c11) != sk_c10 )
| ( multiply(X5,sk_c11) != sk_c10 )
| ( multiply(X4,sk_c12) != sk_c11 )
| ( multiply(X3,sk_c10) != sk_c12 )
| ( multiply(X2,sk_c12) != sk_c11 )
| ( multiply(inverse(X1),sk_c11) != sk_c12 )
| ( multiply(X1,inverse(X1)) != sk_c12 )
| ( multiply(X0,inverse(X1)) != inverse(X0) ) ),
inference(cnf_transformation,[],[f146]) ).
tcf(c_198,plain,
multiply(inverse(sk_c11),sk_c11) = identity,
inference(instantiation,[status(thm)],[c_124]) ).
tcf(c_829,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_10
| ( inverse(X0) != sk_c12 )
| ( multiply(X0,sk_c12) != sk_c11 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_10])],[c_196]) ).
tcf(c_830,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_11
| ( inverse(X0) != sk_c11 )
| ( multiply(X0,sk_c11) != sk_c10 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_11])],[c_196]) ).
tcf(c_831,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_12
| ( inverse(X0) != sk_c10 )
| ( multiply(X0,sk_c10) != sk_c12 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_12])],[c_196]) ).
tcf(c_832,negated_conjecture,
! [X0: $i,X1: $i] :
( ~ iPr_def_13
| ( inverse(inverse(X0)) != inverse(X1) )
| ( multiply(inverse(X1),sk_c11) != sk_c12 )
| ( multiply(X1,inverse(X1)) != sk_c12 )
| ( multiply(X0,inverse(X1)) != inverse(X0) ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_13])],[c_196]) ).
tcf(c_833,negated_conjecture,
( iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( multiply(sk_c10,sk_c12) != sk_c11 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_196]) ).
tcf(c_834,definition,
iPr_def_14 = multiply(sk_c10,sk_c12),
introduced(definition,[new_symbols(definition,[iPr_def_14])],[]) ).
tcf(c_836,definition,
iPr_def_16 = inverse(sk_c3),
introduced(definition,[new_symbols(definition,[iPr_def_16])],[]) ).
tcf(c_837,definition,
iPr_def_17 = inverse(sk_c7),
introduced(definition,[new_symbols(definition,[iPr_def_17])],[]) ).
tcf(c_839,definition,
iPr_def_19 = multiply(sk_c9,sk_c11),
introduced(definition,[new_symbols(definition,[iPr_def_19])],[]) ).
tcf(c_840,definition,
iPr_def_20 = inverse(sk_c6),
introduced(definition,[new_symbols(definition,[iPr_def_20])],[]) ).
tcf(c_841,definition,
iPr_def_21 = multiply(sk_c6,sk_c9),
introduced(definition,[new_symbols(definition,[iPr_def_21])],[]) ).
tcf(c_842,definition,
iPr_def_22 = inverse(sk_c5),
introduced(definition,[new_symbols(definition,[iPr_def_22])],[]) ).
tcf(c_843,definition,
iPr_def_23 = multiply(sk_c5,sk_c11),
introduced(definition,[new_symbols(definition,[iPr_def_23])],[]) ).
tcf(c_844,definition,
iPr_def_24 = inverse(sk_c4),
introduced(definition,[new_symbols(definition,[iPr_def_24])],[]) ).
tcf(c_845,definition,
iPr_def_25 = multiply(sk_c4,sk_c12),
introduced(definition,[new_symbols(definition,[iPr_def_25])],[]) ).
tcf(c_846,definition,
iPr_def_26 = multiply(sk_c3,sk_c10),
introduced(definition,[new_symbols(definition,[iPr_def_26])],[]) ).
tcf(c_847,definition,
iPr_def_27 = inverse(sk_c2),
introduced(definition,[new_symbols(definition,[iPr_def_27])],[]) ).
tcf(c_848,definition,
iPr_def_28 = multiply(sk_c2,sk_c11),
introduced(definition,[new_symbols(definition,[iPr_def_28])],[]) ).
tcf(c_849,definition,
iPr_def_29 = inverse(sk_c1),
introduced(definition,[new_symbols(definition,[iPr_def_29])],[]) ).
tcf(c_850,definition,
iPr_def_30 = multiply(sk_c1,sk_c12),
introduced(definition,[new_symbols(definition,[iPr_def_30])],[]) ).
tcf(c_851,negated_conjecture,
( iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( iPr_def_14 != sk_c11 ) ),
inference(demodulation,[status(thm)],[c_833,c_834]) ).
tcf(c_852,negated_conjecture,
! [X0: $i,X1: $i] :
( ~ iPr_def_13
| ( inverse(inverse(X0)) != inverse(X1) )
| ( multiply(inverse(X1),sk_c11) != sk_c12 )
| ( multiply(X1,inverse(X1)) != sk_c12 )
| ( multiply(X0,inverse(X1)) != inverse(X0) ) ),
inference(demodulation,[status(thm)],[c_832]) ).
tcf(c_855,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_12
| ( inverse(X0) != sk_c10 )
| ( multiply(X0,sk_c10) != sk_c12 ) ),
inference(demodulation,[status(thm)],[c_831]) ).
tcf(c_856,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_11
| ( inverse(X0) != sk_c11 )
| ( multiply(X0,sk_c11) != sk_c10 ) ),
inference(demodulation,[status(thm)],[c_830]) ).
tcf(c_857,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_10
| ( inverse(X0) != sk_c12 )
| ( multiply(X0,sk_c12) != sk_c11 ) ),
inference(demodulation,[status(thm)],[c_829]) ).
tcf(c_859,negated_conjecture,
( ( iPr_def_17 = sk_c9 )
| ( iPr_def_16 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_194,c_837]) ).
tcf(c_861,negated_conjecture,
( ( iPr_def_19 = sk_c12 )
| ( iPr_def_16 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_192,c_839]) ).
tcf(c_862,negated_conjecture,
( ( iPr_def_20 = sk_c9 )
| ( iPr_def_16 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_191,c_840]) ).
tcf(c_863,negated_conjecture,
( ( iPr_def_21 = sk_c12 )
| ( iPr_def_16 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_190,c_841]) ).
tcf(c_864,negated_conjecture,
( ( iPr_def_22 = sk_c11 )
| ( iPr_def_16 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_189,c_842]) ).
tcf(c_865,negated_conjecture,
( ( iPr_def_23 = sk_c10 )
| ( iPr_def_16 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_188,c_843]) ).
tcf(c_866,negated_conjecture,
( ( iPr_def_24 = sk_c12 )
| ( iPr_def_16 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_187,c_844]) ).
tcf(c_867,negated_conjecture,
( ( iPr_def_25 = sk_c11 )
| ( iPr_def_16 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_186,c_845]) ).
tcf(c_869,negated_conjecture,
( ( iPr_def_26 = sk_c12 )
| ( iPr_def_17 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_184]) ).
tcf(c_871,negated_conjecture,
( ( iPr_def_26 = sk_c12 )
| ( iPr_def_19 = sk_c12 ) ),
inference(demodulation,[status(thm)],[c_182]) ).
tcf(c_872,negated_conjecture,
( ( iPr_def_26 = sk_c12 )
| ( iPr_def_20 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_181]) ).
tcf(c_873,negated_conjecture,
( ( iPr_def_26 = sk_c12 )
| ( iPr_def_21 = sk_c12 ) ),
inference(demodulation,[status(thm)],[c_180]) ).
tcf(c_874,negated_conjecture,
( ( iPr_def_26 = sk_c12 )
| ( iPr_def_22 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_179]) ).
tcf(c_875,negated_conjecture,
( ( iPr_def_26 = sk_c12 )
| ( iPr_def_23 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_178]) ).
tcf(c_876,negated_conjecture,
( ( iPr_def_26 = sk_c12 )
| ( iPr_def_24 = sk_c12 ) ),
inference(demodulation,[status(thm)],[c_177]) ).
tcf(c_877,negated_conjecture,
( ( iPr_def_26 = sk_c12 )
| ( iPr_def_25 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_176]) ).
tcf(c_879,negated_conjecture,
( ( iPr_def_17 = sk_c9 )
| ( iPr_def_14 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_174]) ).
tcf(c_881,negated_conjecture,
( ( iPr_def_19 = sk_c12 )
| ( iPr_def_14 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_172]) ).
tcf(c_882,negated_conjecture,
( ( iPr_def_20 = sk_c9 )
| ( iPr_def_14 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_171]) ).
tcf(c_883,negated_conjecture,
( ( iPr_def_21 = sk_c12 )
| ( iPr_def_14 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_170]) ).
tcf(c_884,negated_conjecture,
( ( iPr_def_22 = sk_c11 )
| ( iPr_def_14 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_169]) ).
tcf(c_885,negated_conjecture,
( ( iPr_def_23 = sk_c10 )
| ( iPr_def_14 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_168]) ).
tcf(c_886,negated_conjecture,
( ( iPr_def_24 = sk_c12 )
| ( iPr_def_14 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_167]) ).
tcf(c_887,negated_conjecture,
( ( iPr_def_25 = sk_c11 )
| ( iPr_def_14 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_166]) ).
tcf(c_889,negated_conjecture,
( ( iPr_def_27 = sk_c11 )
| ( iPr_def_17 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_164]) ).
tcf(c_891,negated_conjecture,
( ( iPr_def_27 = sk_c11 )
| ( iPr_def_19 = sk_c12 ) ),
inference(demodulation,[status(thm)],[c_162]) ).
tcf(c_892,negated_conjecture,
( ( iPr_def_27 = sk_c11 )
| ( iPr_def_20 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_161]) ).
tcf(c_893,negated_conjecture,
( ( iPr_def_27 = sk_c11 )
| ( iPr_def_21 = sk_c12 ) ),
inference(demodulation,[status(thm)],[c_160]) ).
tcf(c_894,negated_conjecture,
( ( iPr_def_27 = sk_c11 )
| ( iPr_def_22 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_159]) ).
tcf(c_895,negated_conjecture,
( ( iPr_def_27 = sk_c11 )
| ( iPr_def_23 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_158]) ).
tcf(c_896,negated_conjecture,
( ( iPr_def_27 = sk_c11 )
| ( iPr_def_24 = sk_c12 ) ),
inference(demodulation,[status(thm)],[c_157]) ).
tcf(c_897,negated_conjecture,
( ( iPr_def_27 = sk_c11 )
| ( iPr_def_25 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_156]) ).
tcf(c_899,negated_conjecture,
( ( iPr_def_28 = sk_c10 )
| ( iPr_def_17 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_154]) ).
tcf(c_901,negated_conjecture,
( ( iPr_def_28 = sk_c10 )
| ( iPr_def_19 = sk_c12 ) ),
inference(demodulation,[status(thm)],[c_152]) ).
tcf(c_902,negated_conjecture,
( ( iPr_def_28 = sk_c10 )
| ( iPr_def_20 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_151]) ).
tcf(c_903,negated_conjecture,
( ( iPr_def_28 = sk_c10 )
| ( iPr_def_21 = sk_c12 ) ),
inference(demodulation,[status(thm)],[c_150]) ).
tcf(c_904,negated_conjecture,
( ( iPr_def_28 = sk_c10 )
| ( iPr_def_22 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_149]) ).
tcf(c_905,negated_conjecture,
( ( iPr_def_28 = sk_c10 )
| ( iPr_def_23 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_148]) ).
tcf(c_906,negated_conjecture,
( ( iPr_def_28 = sk_c10 )
| ( iPr_def_24 = sk_c12 ) ),
inference(demodulation,[status(thm)],[c_147]) ).
tcf(c_907,negated_conjecture,
( ( iPr_def_28 = sk_c10 )
| ( iPr_def_25 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_146]) ).
tcf(c_909,negated_conjecture,
( ( iPr_def_29 = sk_c12 )
| ( iPr_def_17 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_144]) ).
tcf(c_911,negated_conjecture,
( ( iPr_def_29 = sk_c12 )
| ( iPr_def_19 = sk_c12 ) ),
inference(demodulation,[status(thm)],[c_142]) ).
tcf(c_912,negated_conjecture,
( ( iPr_def_29 = sk_c12 )
| ( iPr_def_20 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_141]) ).
tcf(c_913,negated_conjecture,
( ( iPr_def_29 = sk_c12 )
| ( iPr_def_21 = sk_c12 ) ),
inference(demodulation,[status(thm)],[c_140]) ).
tcf(c_914,negated_conjecture,
( ( iPr_def_29 = sk_c12 )
| ( iPr_def_22 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_139]) ).
tcf(c_916,negated_conjecture,
( ( iPr_def_29 = sk_c12 )
| ( iPr_def_24 = sk_c12 ) ),
inference(demodulation,[status(thm)],[c_137]) ).
tcf(c_917,negated_conjecture,
( ( iPr_def_29 = sk_c12 )
| ( iPr_def_25 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_136]) ).
tcf(c_919,negated_conjecture,
( ( iPr_def_30 = sk_c11 )
| ( iPr_def_17 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_134]) ).
tcf(c_921,negated_conjecture,
( ( iPr_def_30 = sk_c11 )
| ( iPr_def_19 = sk_c12 ) ),
inference(demodulation,[status(thm)],[c_132]) ).
tcf(c_922,negated_conjecture,
( ( iPr_def_30 = sk_c11 )
| ( iPr_def_20 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_131]) ).
tcf(c_923,negated_conjecture,
( ( iPr_def_30 = sk_c11 )
| ( iPr_def_21 = sk_c12 ) ),
inference(demodulation,[status(thm)],[c_130]) ).
tcf(c_924,negated_conjecture,
( ( iPr_def_30 = sk_c11 )
| ( iPr_def_22 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_129]) ).
tcf(c_926,negated_conjecture,
( ( iPr_def_30 = sk_c11 )
| ( iPr_def_24 = sk_c12 ) ),
inference(demodulation,[status(thm)],[c_127]) ).
tcf(c_927,negated_conjecture,
( ( iPr_def_30 = sk_c11 )
| ( iPr_def_25 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_126]) ).
tcf(c_928,plain,
! [X0: $i] : X0 = X0,
theory(equality) ).
tcf(c_929,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = X0 )
| ( X2 != X1 )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_930,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( multiply(X0,X2) = multiply(X1,X3) )
| ( X2 != X3 )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_931,plain,
! [X0: $i,X1: $i] :
( ( inverse(X0) = inverse(X1) )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_933,plain,
( ( inverse(sk_c11) = inverse(sk_c11) )
| ( sk_c11 != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_931]) ).
tcf(c_934,plain,
sk_c11 = sk_c11,
inference(instantiation,[status(thm)],[c_928]) ).
tcf(c_938,plain,
( ~ iPr_def_13
| ( inverse(inverse(sk_c11)) != inverse(sk_c11) )
| ( multiply(sk_c11,inverse(sk_c11)) != sk_c12 )
| ( multiply(sk_c11,inverse(sk_c11)) != inverse(sk_c11) )
| ( multiply(inverse(sk_c11),sk_c11) != sk_c12 ) ),
inference(instantiation,[status(thm)],[c_852]) ).
tcf(c_1337,plain,
( ( iPr_def_17 = iPr_def_20 )
| ( sk_c10 = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_859,c_862]) ).
tcf(c_1369,plain,
( ( sk_c11 = iPr_def_22 )
| ( multiply(iPr_def_16,sk_c12) = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_864,c_834]) ).
tcf(c_1370,plain,
( ( sk_c12 = iPr_def_21 )
| ( multiply(iPr_def_16,sk_c12) = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_863,c_834]) ).
tcf(c_1371,plain,
( ( sk_c12 = iPr_def_19 )
| ( multiply(iPr_def_16,sk_c12) = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_861,c_834]) ).
tcf(c_1391,plain,
( ( sk_c12 = iPr_def_24 )
| ( multiply(iPr_def_16,sk_c12) = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_866,c_834]) ).
tcf(c_1403,plain,
( ( sk_c11 = iPr_def_25 )
| ( multiply(iPr_def_16,sk_c12) = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_867,c_834]) ).
tcf(c_1451,plain,
( ( iPr_def_17 = iPr_def_20 )
| ( sk_c12 = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_872,c_869]) ).
tcf(c_1486,plain,
( ( sk_c12 = iPr_def_26 )
| ( multiply(sk_c6,iPr_def_20) = iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_872,c_841]) ).
tcf(c_1488,plain,
( ( sk_c10 = iPr_def_16 )
| ( multiply(sk_c6,iPr_def_20) = iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_862,c_841]) ).
tcf(c_1498,plain,
( ( sk_c12 = iPr_def_21 )
| ( multiply(sk_c4,iPr_def_26) = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_873,c_845]) ).
tcf(c_1499,plain,
( ( sk_c12 = iPr_def_19 )
| ( multiply(sk_c4,iPr_def_26) = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_871,c_845]) ).
tcf(c_1504,plain,
( ( sk_c11 = iPr_def_25 )
| ( multiply(sk_c3,iPr_def_16) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_867,c_846]) ).
tcf(c_1505,plain,
( ( sk_c12 = iPr_def_24 )
| ( multiply(sk_c3,iPr_def_16) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_866,c_846]) ).
tcf(c_1506,plain,
( ( sk_c10 = iPr_def_16 )
| ( multiply(sk_c3,iPr_def_23) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_865,c_846]) ).
tcf(c_1507,plain,
( ( sk_c11 = iPr_def_22 )
| ( multiply(sk_c3,iPr_def_16) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_864,c_846]) ).
tcf(c_1508,plain,
( ( sk_c12 = iPr_def_21 )
| ( multiply(sk_c3,iPr_def_16) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_863,c_846]) ).
tcf(c_1509,plain,
( ( sk_c12 = iPr_def_19 )
| ( multiply(sk_c3,iPr_def_16) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_861,c_846]) ).
tcf(c_1532,plain,
( ( sk_c12 = iPr_def_26 )
| ( multiply(sk_c2,iPr_def_22) = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_874,c_848]) ).
tcf(c_1550,plain,
( ( sk_c12 = iPr_def_26 )
| ( multiply(sk_c3,iPr_def_23) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_875,c_846]) ).
tcf(c_1580,plain,
( ( sk_c12 = iPr_def_24 )
| ( multiply(sk_c1,iPr_def_26) = iPr_def_30 ) ),
inference(superposition,[status(thm)],[c_876,c_850]) ).
tcf(c_1593,plain,
( ( iPr_def_22 = iPr_def_25 )
| ( sk_c12 = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_874,c_877]) ).
tcf(c_1595,plain,
( ( sk_c12 = iPr_def_26 )
| ( multiply(sk_c2,iPr_def_25) = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_877,c_848]) ).
tcf(c_1663,plain,
( ( sk_c12 = iPr_def_19 )
| ( multiply(sk_c2,iPr_def_14) = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_881,c_848]) ).
tcf(c_1685,plain,
( ( iPr_def_17 = iPr_def_20 )
| ( sk_c11 = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_882,c_879]) ).
tcf(c_1686,plain,
( ( sk_c11 = iPr_def_14 )
| ( multiply(sk_c6,iPr_def_20) = iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_882,c_841]) ).
tcf(c_1699,plain,
multiply(iPr_def_24,sk_c4) = identity,
inference(superposition,[status(thm)],[c_844,c_124]) ).
tcf(c_1700,plain,
multiply(iPr_def_22,sk_c5) = identity,
inference(superposition,[status(thm)],[c_842,c_124]) ).
tcf(c_1701,plain,
multiply(iPr_def_20,sk_c6) = identity,
inference(superposition,[status(thm)],[c_840,c_124]) ).
tcf(c_1703,plain,
multiply(iPr_def_17,sk_c7) = identity,
inference(superposition,[status(thm)],[c_837,c_124]) ).
tcf(c_1704,plain,
multiply(iPr_def_29,sk_c1) = identity,
inference(superposition,[status(thm)],[c_849,c_124]) ).
tcf(c_1705,plain,
multiply(iPr_def_27,sk_c2) = identity,
inference(superposition,[status(thm)],[c_847,c_124]) ).
tcf(c_1706,plain,
multiply(iPr_def_16,sk_c3) = identity,
inference(superposition,[status(thm)],[c_836,c_124]) ).
tcf(c_1707,plain,
! [X0: $i] :
( ( iPr_def_14 = sk_c11 )
| ( iPr_def_14 != X0 )
| ( sk_c11 != X0 ) ),
inference(instantiation,[status(thm)],[c_929]) ).
tcf(c_1708,plain,
( ( iPr_def_14 = sk_c11 )
| ( iPr_def_14 != iPr_def_14 )
| ( sk_c11 != iPr_def_14 ) ),
inference(instantiation,[status(thm)],[c_1707]) ).
tcf(c_1709,plain,
iPr_def_14 = iPr_def_14,
inference(instantiation,[status(thm)],[c_928]) ).
tcf(c_1710,plain,
! [X0: $i,X1: $i] :
( ( iPr_def_14 = X0 )
| ( iPr_def_14 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_929]) ).
tcf(c_1738,plain,
! [X0: $i] :
( ( sk_c11 = multiply(sk_c10,sk_c12) )
| ( sk_c11 != X0 )
| ( multiply(sk_c10,sk_c12) != X0 ) ),
inference(instantiation,[status(thm)],[c_929]) ).
tcf(c_1755,plain,
( ( sk_c11 = iPr_def_14 )
| ( multiply(sk_c2,iPr_def_22) = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_884,c_848]) ).
tcf(c_1778,plain,
! [X0: $i,X1: $i] :
( ( multiply(sk_c10,sk_c12) = X1 )
| ( X1 != X0 )
| ( multiply(sk_c10,sk_c12) != X0 ) ),
inference(instantiation,[status(thm)],[c_929]) ).
tcf(c_1780,plain,
! [X0: $i,X1: $i] :
( ( multiply(sk_c10,sk_c12) = multiply(X1,X0) )
| ( sk_c10 != X1 )
| ( sk_c12 != X0 ) ),
inference(instantiation,[status(thm)],[c_930]) ).
tcf(c_1795,plain,
( ( sk_c11 = iPr_def_14 )
| ( multiply(iPr_def_23,sk_c12) = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_885,c_834]) ).
tcf(c_1821,plain,
! [X0: $i,X1: $i] :
( ( X0 = iPr_def_14 )
| ( iPr_def_14 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_929]) ).
tcf(c_1824,plain,
multiply(identity,multiply(sk_c10,sk_c12)) = multiply(sk_c10,sk_c12),
inference(instantiation,[status(thm)],[c_123]) ).
tcf(c_1826,plain,
! [X0: $i,X1: $i] :
( ( X1 = multiply(sk_c10,sk_c12) )
| ( X1 != X0 )
| ( multiply(sk_c10,sk_c12) != X0 ) ),
inference(instantiation,[status(thm)],[c_929]) ).
tcf(c_1828,plain,
! [X0: $i,X1: $i] :
( ( multiply(X0,X1) = multiply(sk_c10,sk_c12) )
| ( X1 != sk_c12 )
| ( X0 != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_930]) ).
tcf(c_1830,plain,
( ( multiply(sk_c11,sk_c11) = multiply(sk_c10,sk_c12) )
| ( sk_c11 != sk_c10 )
| ( sk_c11 != sk_c12 ) ),
inference(instantiation,[status(thm)],[c_1828]) ).
tcf(c_1870,plain,
( ( iPr_def_22 = iPr_def_25 )
| ( sk_c11 = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_887,c_884]) ).
tcf(c_1874,plain,
( ( sk_c11 = iPr_def_14 )
| ( multiply(sk_c2,iPr_def_25) = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_887,c_848]) ).
tcf(c_1922,plain,
! [X0: $i] :
( ( multiply(sk_c10,sk_c12) = X0 )
| ( X0 != multiply(sk_c10,sk_c12) )
| ( multiply(sk_c10,sk_c12) != multiply(sk_c10,sk_c12) ) ),
inference(instantiation,[status(thm)],[c_1778]) ).
tcf(c_1923,plain,
multiply(sk_c10,sk_c12) = multiply(sk_c10,sk_c12),
inference(instantiation,[status(thm)],[c_928]) ).
tcf(c_1956,plain,
sk_c12 = sk_c12,
inference(instantiation,[status(thm)],[c_928]) ).
tcf(c_1958,plain,
! [X0: $i,X1: $i] :
( ( sk_c12 = X0 )
| ( sk_c12 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_929]) ).
tcf(c_1994,plain,
( ( sk_c12 = iPr_def_19 )
| ( multiply(sk_c2,iPr_def_27) = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_891,c_848]) ).
tcf(c_2025,plain,
! [X0: $i] :
( ( X0 = iPr_def_14 )
| ( iPr_def_14 != multiply(sk_c10,sk_c12) )
| ( X0 != multiply(sk_c10,sk_c12) ) ),
inference(instantiation,[status(thm)],[c_1821]) ).
tcf(c_2042,plain,
sk_c10 = sk_c10,
inference(instantiation,[status(thm)],[c_928]) ).
tcf(c_2044,plain,
! [X0: $i,X1: $i] :
( ( X0 = sk_c10 )
| ( sk_c10 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_929]) ).
tcf(c_2056,plain,
( ( iPr_def_17 = iPr_def_20 )
| ( sk_c11 = iPr_def_27 ) ),
inference(superposition,[status(thm)],[c_892,c_889]) ).
tcf(c_2058,plain,
( ( sk_c11 = iPr_def_27 )
| ( multiply(sk_c6,iPr_def_20) = iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_892,c_841]) ).
tcf(c_2089,plain,
( ( sk_c12 = iPr_def_21 )
| ( multiply(sk_c2,iPr_def_27) = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_893,c_848]) ).
tcf(c_2148,plain,
( ( sk_c11 = iPr_def_22 )
| ( multiply(sk_c2,iPr_def_27) = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_894,c_848]) ).
tcf(c_2183,plain,
! [X0: $i,X1: $i] :
( ( X1 = multiply(identity,multiply(sk_c10,sk_c12)) )
| ( X1 != X0 )
| ( multiply(identity,multiply(sk_c10,sk_c12)) != X0 ) ),
inference(instantiation,[status(thm)],[c_929]) ).
tcf(c_2186,plain,
! [X0: $i,X1: $i] :
( ( multiply(X0,X1) = multiply(identity,multiply(sk_c10,sk_c12)) )
| ( X1 != multiply(sk_c10,sk_c12) )
| ( X0 != identity ) ),
inference(instantiation,[status(thm)],[c_930]) ).
tcf(c_2188,plain,
( ( multiply(sk_c11,sk_c11) = multiply(identity,multiply(sk_c10,sk_c12)) )
| ( sk_c11 != identity )
| ( sk_c11 != multiply(sk_c10,sk_c12) ) ),
inference(instantiation,[status(thm)],[c_2186]) ).
tcf(c_2199,plain,
( ( sk_c11 = iPr_def_27 )
| ( multiply(sk_c3,iPr_def_23) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_895,c_846]) ).
tcf(c_2241,plain,
( ( multiply(sk_c10,sk_c12) = iPr_def_14 )
| ( iPr_def_14 != multiply(sk_c10,sk_c12) )
| ( multiply(sk_c10,sk_c12) != multiply(sk_c10,sk_c12) ) ),
inference(instantiation,[status(thm)],[c_1922]) ).
tcf(c_2271,plain,
( ( sk_c12 = iPr_def_24 )
| ( multiply(sk_c2,iPr_def_27) = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_896,c_848]) ).
tcf(c_2297,plain,
! [X0: $i] :
( ( sk_c12 = X0 )
| ( sk_c12 != sk_c12 )
| ( X0 != sk_c12 ) ),
inference(instantiation,[status(thm)],[c_1958]) ).
tcf(c_2300,plain,
! [X0: $i,X1: $i] :
( ( sk_c10 = X0 )
| ( sk_c10 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_929]) ).
tcf(c_2310,plain,
( ( multiply(identity,multiply(sk_c10,sk_c12)) = iPr_def_14 )
| ( iPr_def_14 != multiply(sk_c10,sk_c12) )
| ( multiply(identity,multiply(sk_c10,sk_c12)) != multiply(sk_c10,sk_c12) ) ),
inference(instantiation,[status(thm)],[c_2025]) ).
tcf(c_2332,plain,
( ( sk_c11 = iPr_def_25 )
| ( multiply(sk_c2,iPr_def_27) = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_897,c_848]) ).
tcf(c_2428,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( multiply(X0,X1) = X3 )
| ( X3 != X2 )
| ( multiply(X0,X1) != X2 ) ),
inference(instantiation,[status(thm)],[c_929]) ).
tcf(c_2465,plain,
! [X0: $i,X1: $i] :
( ( X0 = sk_c12 )
| ( sk_c12 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_929]) ).
tcf(c_2554,plain,
( ( sk_c12 = iPr_def_19 )
| ( multiply(sk_c3,iPr_def_28) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_901,c_846]) ).
tcf(c_2675,plain,
( ( iPr_def_17 = iPr_def_20 )
| ( sk_c10 = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_902,c_899]) ).
tcf(c_2678,plain,
( ( sk_c10 = iPr_def_28 )
| ( multiply(sk_c6,iPr_def_20) = iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_902,c_841]) ).
tcf(c_2770,plain,
( ( sk_c11 = iPr_def_22 )
| ( multiply(sk_c3,iPr_def_28) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_904,c_846]) ).
tcf(c_2826,plain,
( ( sk_c10 = iPr_def_23 )
| ( multiply(sk_c3,iPr_def_28) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_905,c_846]) ).
tcf(c_2970,plain,
( ( sk_c11 = multiply(sk_c10,sk_c12) )
| ( sk_c11 != iPr_def_14 )
| ( multiply(sk_c10,sk_c12) != iPr_def_14 ) ),
inference(instantiation,[status(thm)],[c_1738]) ).
tcf(c_2973,plain,
! [X0: $i] :
( ( sk_c10 = iPr_def_14 )
| ( iPr_def_14 != X0 )
| ( sk_c10 != X0 ) ),
inference(instantiation,[status(thm)],[c_1821]) ).
tcf(c_2976,plain,
! [X0: $i] :
( ( sk_c12 = iPr_def_14 )
| ( iPr_def_14 != X0 )
| ( sk_c12 != X0 ) ),
inference(instantiation,[status(thm)],[c_1821]) ).
tcf(c_2977,plain,
! [X0: $i] :
( ( X0 = sk_c12 )
| ( sk_c12 != iPr_def_14 )
| ( X0 != iPr_def_14 ) ),
inference(instantiation,[status(thm)],[c_2465]) ).
tcf(c_2978,plain,
! [X0: $i] :
( ( sk_c12 = X0 )
| ( sk_c12 != iPr_def_14 )
| ( X0 != iPr_def_14 ) ),
inference(instantiation,[status(thm)],[c_1958]) ).
tcf(c_2980,plain,
( ( sk_c12 = sk_c11 )
| ( sk_c11 != iPr_def_14 )
| ( sk_c12 != iPr_def_14 ) ),
inference(instantiation,[status(thm)],[c_2978]) ).
tcf(c_2981,plain,
( ( sk_c11 = sk_c12 )
| ( sk_c11 != iPr_def_14 )
| ( sk_c12 != iPr_def_14 ) ),
inference(instantiation,[status(thm)],[c_2977]) ).
tcf(c_3004,plain,
( ( sk_c11 = iPr_def_25 )
| ( multiply(sk_c3,iPr_def_28) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_907,c_846]) ).
tcf(c_3123,plain,
( ( sk_c12 = iPr_def_19 )
| ( multiply(sk_c1,iPr_def_29) = iPr_def_30 ) ),
inference(superposition,[status(thm)],[c_911,c_850]) ).
tcf(c_3155,plain,
! [X0: $i,X1: $i] :
( ( X0 = identity )
| ( identity != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_929]) ).
tcf(c_3172,plain,
( ( iPr_def_17 = iPr_def_20 )
| ( sk_c12 = iPr_def_29 ) ),
inference(superposition,[status(thm)],[c_912,c_909]) ).
tcf(c_3197,plain,
( ( sk_c12 = iPr_def_21 )
| ( multiply(sk_c1,iPr_def_29) = iPr_def_30 ) ),
inference(superposition,[status(thm)],[c_913,c_850]) ).
tcf(c_3364,plain,
! [X0: $i] :
( ( X0 = multiply(identity,multiply(sk_c10,sk_c12)) )
| ( X0 != iPr_def_14 )
| ( multiply(identity,multiply(sk_c10,sk_c12)) != iPr_def_14 ) ),
inference(instantiation,[status(thm)],[c_2183]) ).
tcf(c_3365,plain,
( ( sk_c11 = multiply(identity,multiply(sk_c10,sk_c12)) )
| ( sk_c11 != iPr_def_14 )
| ( multiply(identity,multiply(sk_c10,sk_c12)) != iPr_def_14 ) ),
inference(instantiation,[status(thm)],[c_3364]) ).
tcf(c_3480,plain,
( ( sk_c12 = iPr_def_26 )
| ( iPr_def_26 != sk_c12 )
| ( sk_c12 != sk_c12 ) ),
inference(instantiation,[status(thm)],[c_2297]) ).
tcf(c_3513,plain,
( ( sk_c12 = iPr_def_24 )
| ( multiply(sk_c1,iPr_def_29) = iPr_def_30 ) ),
inference(superposition,[status(thm)],[c_916,c_850]) ).
tcf(c_3539,plain,
! [X0: $i] :
( ( sk_c10 = X0 )
| ( sk_c10 != sk_c10 )
| ( X0 != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_2300]) ).
tcf(c_3562,plain,
( ( iPr_def_22 = iPr_def_25 )
| ( sk_c12 = iPr_def_29 ) ),
inference(superposition,[status(thm)],[c_917,c_914]) ).
tcf(c_3573,plain,
( ( sk_c12 = iPr_def_29 )
| ( multiply(sk_c2,iPr_def_25) = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_917,c_848]) ).
tcf(c_3610,plain,
! [X0: $i,X1: $i] :
( ( multiply(inverse(X0),X0) = X1 )
| ( X1 != identity )
| ( multiply(inverse(X0),X0) != identity ) ),
inference(instantiation,[status(thm)],[c_2428]) ).
tcf(c_3611,plain,
( ( multiply(inverse(sk_c11),sk_c11) = sk_c11 )
| ( sk_c11 != identity )
| ( multiply(inverse(sk_c11),sk_c11) != identity ) ),
inference(instantiation,[status(thm)],[c_3610]) ).
tcf(c_3619,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( ( multiply(X0,X1) = X4 )
| ( X4 != multiply(X2,X3) )
| ( multiply(X0,X1) != multiply(X2,X3) ) ),
inference(instantiation,[status(thm)],[c_2428]) ).
tcf(c_3840,plain,
( ( sk_c12 = iPr_def_19 )
| ( multiply(sk_c2,iPr_def_30) = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_921,c_848]) ).
tcf(c_3970,plain,
( ( iPr_def_17 = iPr_def_20 )
| ( sk_c11 = iPr_def_30 ) ),
inference(superposition,[status(thm)],[c_922,c_919]) ).
tcf(c_4041,plain,
( ( sk_c12 = iPr_def_21 )
| ( multiply(sk_c2,iPr_def_30) = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_923,c_848]) ).
tcf(c_4091,plain,
! [X0: $i] :
( ( sk_c12 = X0 )
| ( sk_c12 != iPr_def_29 )
| ( X0 != iPr_def_29 ) ),
inference(instantiation,[status(thm)],[c_1958]) ).
tcf(c_4094,plain,
! [X0: $i] :
( ( multiply(sk_c10,sk_c12) = multiply(X0,iPr_def_29) )
| ( sk_c10 != X0 )
| ( sk_c12 != iPr_def_29 ) ),
inference(instantiation,[status(thm)],[c_1780]) ).
tcf(c_4377,plain,
( ( sk_c12 = iPr_def_24 )
| ( multiply(sk_c2,iPr_def_30) = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_926,c_848]) ).
tcf(c_4475,plain,
( ( sk_c11 = iPr_def_25 )
| ( multiply(sk_c2,iPr_def_30) = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_927,c_848]) ).
tcf(c_4513,plain,
( ( sk_c12 = iPr_def_19 )
| ( iPr_def_19 != sk_c12 )
| ( sk_c12 != sk_c12 ) ),
inference(instantiation,[status(thm)],[c_2297]) ).
tcf(c_4517,plain,
( ( sk_c12 = iPr_def_21 )
| ( iPr_def_21 != sk_c12 )
| ( sk_c12 != sk_c12 ) ),
inference(instantiation,[status(thm)],[c_2297]) ).
tcf(c_4540,plain,
( ( sk_c12 = iPr_def_24 )
| ( iPr_def_24 != sk_c12 )
| ( sk_c12 != sk_c12 ) ),
inference(instantiation,[status(thm)],[c_2297]) ).
tcf(c_4574,plain,
! [X0: $i] : multiply(sk_c6,multiply(sk_c9,X0)) = multiply(iPr_def_21,X0),
inference(superposition,[status(thm)],[c_841,c_125]) ).
tcf(c_4581,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(X0,X1)) = multiply(identity,X1),
inference(superposition,[status(thm)],[c_124,c_125]) ).
tcf(c_4583,plain,
! [X0: $i] : multiply(iPr_def_24,multiply(sk_c4,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1699,c_125]) ).
tcf(c_4584,plain,
! [X0: $i] : multiply(iPr_def_22,multiply(sk_c5,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1700,c_125]) ).
tcf(c_4585,plain,
! [X0: $i] : multiply(iPr_def_20,multiply(sk_c6,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1701,c_125]) ).
tcf(c_4587,plain,
! [X0: $i] : multiply(iPr_def_17,multiply(sk_c7,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1703,c_125]) ).
tcf(c_4588,plain,
! [X0: $i] : multiply(iPr_def_29,multiply(sk_c1,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1704,c_125]) ).
tcf(c_4589,plain,
! [X0: $i] : multiply(iPr_def_27,multiply(sk_c2,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1705,c_125]) ).
tcf(c_4590,plain,
! [X0: $i] : multiply(iPr_def_16,multiply(sk_c3,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1706,c_125]) ).
tcf(c_4592,plain,
! [X0: $i] : multiply(iPr_def_16,multiply(sk_c3,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_4590,c_123]) ).
tcf(c_4593,plain,
! [X0: $i] : multiply(iPr_def_27,multiply(sk_c2,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_4589,c_123]) ).
tcf(c_4594,plain,
! [X0: $i] : multiply(iPr_def_29,multiply(sk_c1,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_4588,c_123]) ).
tcf(c_4595,plain,
! [X0: $i] : multiply(iPr_def_17,multiply(sk_c7,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_4587,c_123]) ).
tcf(c_4597,plain,
! [X0: $i] : multiply(iPr_def_20,multiply(sk_c6,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_4585,c_123]) ).
tcf(c_4598,plain,
! [X0: $i] : multiply(iPr_def_22,multiply(sk_c5,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_4584,c_123]) ).
tcf(c_4599,plain,
! [X0: $i] : multiply(iPr_def_24,multiply(sk_c4,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_4583,c_123]) ).
tcf(c_4772,plain,
( ( iPr_def_17 = iPr_def_20 )
| ( multiply(iPr_def_16,sk_c12) = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_1337,c_834]) ).
tcf(c_4962,plain,
( iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( sk_c12 = iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_881,c_851]) ).
tcf(c_5080,plain,
( ~ iPr_def_12
| ( sk_c12 != iPr_def_26 )
| ( inverse(sk_c3) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_846,c_855]) ).
tcf(c_5106,plain,
( ~ iPr_def_12
| ( sk_c10 != iPr_def_16 )
| ( sk_c12 != iPr_def_26 ) ),
inference(light_normalisation,[status(thm)],[c_5080,c_836]) ).
tcf(c_5283,plain,
( ~ iPr_def_11
| ( sk_c10 != iPr_def_23 )
| ( inverse(sk_c5) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_843,c_856]) ).
tcf(c_5285,plain,
( ~ iPr_def_11
| ( sk_c10 != iPr_def_28 )
| ( inverse(sk_c2) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_848,c_856]) ).
tcf(c_5311,plain,
( ~ iPr_def_11
| ( sk_c10 != iPr_def_28 )
| ( sk_c11 != iPr_def_27 ) ),
inference(light_normalisation,[status(thm)],[c_5285,c_847]) ).
tcf(c_5318,plain,
( ~ iPr_def_11
| ( sk_c10 != iPr_def_23 )
| ( sk_c11 != iPr_def_22 ) ),
inference(light_normalisation,[status(thm)],[c_5283,c_842]) ).
tcf(c_5430,plain,
( ( sk_c12 = iPr_def_14 )
| ( iPr_def_14 != iPr_def_26 )
| ( sk_c12 != iPr_def_26 ) ),
inference(instantiation,[status(thm)],[c_2976]) ).
tcf(c_5502,plain,
( ~ iPr_def_10
| ( sk_c11 != iPr_def_30 )
| ( inverse(sk_c1) != sk_c12 ) ),
inference(superposition,[status(thm)],[c_850,c_857]) ).
tcf(c_5503,plain,
( ~ iPr_def_10
| ( sk_c11 != iPr_def_25 )
| ( inverse(sk_c4) != sk_c12 ) ),
inference(superposition,[status(thm)],[c_845,c_857]) ).
tcf(c_5522,plain,
( ~ iPr_def_10
| ( sk_c11 != iPr_def_25 )
| ( sk_c12 != iPr_def_24 ) ),
inference(light_normalisation,[status(thm)],[c_5503,c_844]) ).
tcf(c_5526,plain,
( ~ iPr_def_10
| ( sk_c11 != iPr_def_30 )
| ( sk_c12 != iPr_def_29 ) ),
inference(light_normalisation,[status(thm)],[c_5502,c_849]) ).
tcf(c_5948,plain,
( iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( iPr_def_17 = iPr_def_20 ) ),
inference(superposition,[status(thm)],[c_1685,c_851]) ).
tcf(c_6146,plain,
( ( iPr_def_22 = iPr_def_25 )
| ( iPr_def_14 = iPr_def_30 )
| ( sk_c11 = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_1870,c_927]) ).
tcf(c_6148,plain,
( ( iPr_def_22 = iPr_def_25 )
| ( iPr_def_14 = iPr_def_30 )
| ( sk_c11 = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_1870,c_924]) ).
tcf(c_6442,plain,
( ( iPr_def_17 = iPr_def_20 )
| ( multiply(sk_c2,iPr_def_27) = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_2056,c_848]) ).
tcf(c_6934,plain,
( ( sk_c10 = iPr_def_16 )
| ( iPr_def_16 != sk_c10 )
| ( sk_c10 != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_3539]) ).
tcf(c_7915,plain,
( ( iPr_def_22 = iPr_def_25 )
| ( multiply(sk_c1,iPr_def_29) = iPr_def_30 ) ),
inference(superposition,[status(thm)],[c_3562,c_850]) ).
tcf(c_8511,plain,
! [X0: $i] :
( ( X0 = sk_c12 )
| ( sk_c12 != iPr_def_19 )
| ( X0 != iPr_def_19 ) ),
inference(instantiation,[status(thm)],[c_2465]) ).
tcf(c_8512,plain,
! [X0: $i] :
( ( sk_c12 = X0 )
| ( sk_c12 != iPr_def_19 )
| ( X0 != iPr_def_19 ) ),
inference(instantiation,[status(thm)],[c_1958]) ).
tcf(c_8513,plain,
( ( sk_c12 = sk_c11 )
| ( sk_c11 != iPr_def_19 )
| ( sk_c12 != iPr_def_19 ) ),
inference(instantiation,[status(thm)],[c_8512]) ).
tcf(c_8514,plain,
( ( sk_c11 = sk_c12 )
| ( sk_c11 != iPr_def_19 )
| ( sk_c12 != iPr_def_19 ) ),
inference(instantiation,[status(thm)],[c_8511]) ).
tcf(c_8515,plain,
( ( sk_c12 = iPr_def_14 )
| ( iPr_def_14 != iPr_def_19 )
| ( sk_c12 != iPr_def_19 ) ),
inference(instantiation,[status(thm)],[c_2976]) ).
tcf(c_8850,plain,
( ( sk_c10 = iPr_def_14 )
| ( iPr_def_14 != iPr_def_16 )
| ( sk_c10 != iPr_def_16 ) ),
inference(instantiation,[status(thm)],[c_2973]) ).
tcf(c_8970,plain,
! [X0: $i] :
( ( sk_c10 = X0 )
| ( sk_c10 != iPr_def_28 )
| ( X0 != iPr_def_28 ) ),
inference(instantiation,[status(thm)],[c_2300]) ).
tcf(c_8971,plain,
! [X0: $i] :
( ( X0 = sk_c10 )
| ( sk_c10 != iPr_def_28 )
| ( X0 != iPr_def_28 ) ),
inference(instantiation,[status(thm)],[c_2044]) ).
tcf(c_9340,plain,
( iPr_def_13
| ( sk_c12 = iPr_def_19 )
| iPr_def_10
| iPr_def_11 ),
inference(global_subsumption_just,[status(thm)],[c_4962,c_851,c_861,c_871,c_881,c_1956,c_2042,c_3480,c_4513,c_5106,c_6934]) ).
tcf(c_9341,plain,
( iPr_def_13
| iPr_def_11
| iPr_def_10
| ( sk_c12 = iPr_def_19 ) ),
inference(renaming,[status(thm)],[c_9340]) ).
tcf(c_9387,plain,
multiply(iPr_def_16,iPr_def_26) = sk_c10,
inference(superposition,[status(thm)],[c_846,c_4592]) ).
tcf(c_9390,plain,
! [X0: $i] : multiply(iPr_def_16,multiply(iPr_def_26,X0)) = multiply(sk_c10,X0),
inference(superposition,[status(thm)],[c_9387,c_125]) ).
tcf(c_9392,plain,
multiply(iPr_def_27,iPr_def_28) = sk_c11,
inference(superposition,[status(thm)],[c_848,c_4593]) ).
tcf(c_9432,plain,
multiply(iPr_def_29,iPr_def_30) = sk_c12,
inference(superposition,[status(thm)],[c_850,c_4594]) ).
tcf(c_9526,plain,
( iPr_def_13
| ( iPr_def_17 = iPr_def_20 ) ),
inference(global_subsumption_just,[status(thm)],[c_5948,c_851,c_1337,c_1451,c_1685,c_1708,c_1709,c_2056,c_2675,c_3172,c_3970,c_5106,c_5311,c_5526]) ).
tcf(c_9777,plain,
multiply(iPr_def_20,iPr_def_21) = sk_c9,
inference(superposition,[status(thm)],[c_841,c_4597]) ).
tcf(c_9835,plain,
multiply(iPr_def_24,iPr_def_25) = sk_c12,
inference(superposition,[status(thm)],[c_845,c_4599]) ).
tcf(c_9997,plain,
( ( iPr_def_22 = iPr_def_25 )
| ( sk_c11 = iPr_def_22 )
| ( multiply(iPr_def_16,iPr_def_26) = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_1593,c_1369]) ).
tcf(c_10039,plain,
( ( iPr_def_22 = iPr_def_25 )
| ( sk_c10 = iPr_def_14 )
| ( sk_c11 = iPr_def_22 ) ),
inference(light_normalisation,[status(thm)],[c_9997,c_9387]) ).
tcf(c_10147,plain,
( ( sk_c12 = iPr_def_21 )
| ( multiply(iPr_def_16,iPr_def_26) = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_873,c_1370]) ).
tcf(c_10151,plain,
( ( sk_c10 = iPr_def_14 )
| ( sk_c12 = iPr_def_21 ) ),
inference(light_normalisation,[status(thm)],[c_10147,c_9387]) ).
tcf(c_10252,plain,
( ( iPr_def_14 = iPr_def_28 )
| ( sk_c12 = iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_10151,c_903]) ).
tcf(c_10263,plain,
( ( iPr_def_14 = iPr_def_16 )
| ( sk_c12 = iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_10151,c_863]) ).
tcf(c_10766,plain,
( ( sk_c12 = iPr_def_19 )
| ( multiply(iPr_def_16,iPr_def_26) = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_871,c_1371]) ).
tcf(c_10768,plain,
! [X0: $i] :
( ( sk_c12 = iPr_def_19 )
| ( multiply(iPr_def_16,multiply(sk_c12,X0)) = multiply(iPr_def_14,X0) ) ),
inference(superposition,[status(thm)],[c_1371,c_125]) ).
tcf(c_10769,plain,
( ( sk_c10 = iPr_def_14 )
| ( sk_c12 = iPr_def_19 ) ),
inference(light_normalisation,[status(thm)],[c_10766,c_9387]) ).
tcf(c_10824,plain,
( ( sk_c12 = iPr_def_24 )
| ( multiply(iPr_def_16,iPr_def_26) = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_876,c_1391]) ).
tcf(c_10829,plain,
( ( sk_c10 = iPr_def_14 )
| ( sk_c12 = iPr_def_24 ) ),
inference(light_normalisation,[status(thm)],[c_10824,c_9387]) ).
tcf(c_10854,plain,
( ( iPr_def_14 = iPr_def_16 )
| ( sk_c11 = iPr_def_25 )
| ( multiply(iPr_def_16,iPr_def_21) = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_10263,c_1403]) ).
tcf(c_11359,plain,
( ( iPr_def_14 = iPr_def_28 )
| ( sk_c12 = iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_10769,c_901]) ).
tcf(c_11497,plain,
( ( iPr_def_14 = iPr_def_28 )
| ( sk_c12 = iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_10829,c_906]) ).
tcf(c_11507,plain,
( ( iPr_def_14 = iPr_def_16 )
| ( sk_c12 = iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_10829,c_866]) ).
tcf(c_11629,plain,
( ( iPr_def_19 = iPr_def_21 )
| ( iPr_def_14 = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_11359,c_10252]) ).
tcf(c_11978,plain,
( ( iPr_def_19 = iPr_def_24 )
| ( iPr_def_14 = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_11497,c_11359]) ).
tcf(c_12121,plain,
( ( iPr_def_21 = iPr_def_24 )
| ( iPr_def_14 = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_11507,c_10263]) ).
tcf(c_12948,plain,
! [X0: $i,X1: $i] :
( ( multiply(X0,X1) = sk_c11 )
| ( sk_c11 != multiply(sk_c10,sk_c12) )
| ( multiply(X0,X1) != multiply(sk_c10,sk_c12) ) ),
inference(instantiation,[status(thm)],[c_3619]) ).
tcf(c_12949,plain,
( ( multiply(sk_c11,sk_c11) = sk_c11 )
| ( sk_c11 != multiply(sk_c10,sk_c12) )
| ( multiply(sk_c11,sk_c11) != multiply(sk_c10,sk_c12) ) ),
inference(instantiation,[status(thm)],[c_12948]) ).
tcf(c_13202,plain,
( ( sk_c12 = iPr_def_21 )
| ( multiply(iPr_def_24,iPr_def_25) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_1498,c_4599]) ).
tcf(c_13203,plain,
( ( sk_c12 = iPr_def_26 )
| ( sk_c12 = iPr_def_21 ) ),
inference(light_normalisation,[status(thm)],[c_13202,c_9835]) ).
tcf(c_13222,plain,
( ( sk_c12 = iPr_def_19 )
| ( multiply(iPr_def_24,iPr_def_25) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_1499,c_4599]) ).
tcf(c_13223,plain,
( ( sk_c12 = iPr_def_26 )
| ( sk_c12 = iPr_def_19 ) ),
inference(light_normalisation,[status(thm)],[c_13222,c_9835]) ).
tcf(c_13234,plain,
( ( sk_c11 = iPr_def_25 )
| ( multiply(iPr_def_16,iPr_def_26) = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_1504,c_4592]) ).
tcf(c_13235,plain,
( ( sk_c10 = iPr_def_16 )
| ( sk_c11 = iPr_def_25 ) ),
inference(light_normalisation,[status(thm)],[c_13234,c_9387]) ).
tcf(c_13256,plain,
( ( sk_c10 = iPr_def_16 )
| ( multiply(iPr_def_16,iPr_def_26) = iPr_def_23 ) ),
inference(superposition,[status(thm)],[c_1506,c_4592]) ).
tcf(c_13257,plain,
( ( sk_c10 = iPr_def_23 )
| ( sk_c10 = iPr_def_16 ) ),
inference(light_normalisation,[status(thm)],[c_13256,c_9387]) ).
tcf(c_13320,plain,
( ( sk_c12 = iPr_def_26 )
| ( multiply(iPr_def_27,iPr_def_28) = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_1532,c_4593]) ).
tcf(c_13321,plain,
( ( sk_c11 = iPr_def_22 )
| ( sk_c12 = iPr_def_26 ) ),
inference(light_normalisation,[status(thm)],[c_13320,c_9392]) ).
tcf(c_13420,plain,
( ( sk_c12 = iPr_def_26 )
| ( multiply(iPr_def_16,iPr_def_26) = iPr_def_23 ) ),
inference(superposition,[status(thm)],[c_1550,c_4592]) ).
tcf(c_13421,plain,
( ( sk_c10 = iPr_def_23 )
| ( sk_c12 = iPr_def_26 ) ),
inference(light_normalisation,[status(thm)],[c_13420,c_9387]) ).
tcf(c_13561,plain,
( ( sk_c12 = multiply(identity,iPr_def_29) )
| ( sk_c12 != iPr_def_29 )
| ( multiply(identity,iPr_def_29) != iPr_def_29 ) ),
inference(instantiation,[status(thm)],[c_4091]) ).
tcf(c_13562,plain,
multiply(identity,iPr_def_29) = iPr_def_29,
inference(instantiation,[status(thm)],[c_123]) ).
tcf(c_13672,plain,
( ( sk_c12 = iPr_def_24 )
| ( multiply(iPr_def_29,iPr_def_30) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_1580,c_4594]) ).
tcf(c_13673,plain,
( ( sk_c12 = iPr_def_26 )
| ( sk_c12 = iPr_def_24 ) ),
inference(light_normalisation,[status(thm)],[c_13672,c_9432]) ).
tcf(c_13745,plain,
( ( sk_c12 = iPr_def_26 )
| ( multiply(iPr_def_27,iPr_def_28) = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_1595,c_4593]) ).
tcf(c_13746,plain,
( ( sk_c11 = iPr_def_25 )
| ( sk_c12 = iPr_def_26 ) ),
inference(light_normalisation,[status(thm)],[c_13745,c_9392]) ).
tcf(c_13903,plain,
( ( sk_c12 = iPr_def_19 )
| ( multiply(iPr_def_27,iPr_def_28) = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_1663,c_4593]) ).
tcf(c_13904,plain,
( ( sk_c11 = iPr_def_14 )
| ( sk_c12 = iPr_def_19 ) ),
inference(light_normalisation,[status(thm)],[c_13903,c_9392]) ).
tcf(c_14313,plain,
( ( sk_c11 = iPr_def_14 )
| ( multiply(iPr_def_27,iPr_def_28) = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_1755,c_4593]) ).
tcf(c_14314,plain,
( ( sk_c11 = iPr_def_22 )
| ( sk_c11 = iPr_def_14 ) ),
inference(light_normalisation,[status(thm)],[c_14313,c_9392]) ).
tcf(c_14787,plain,
( ( sk_c11 = iPr_def_14 )
| ( multiply(iPr_def_27,iPr_def_28) = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_1874,c_4593]) ).
tcf(c_14788,plain,
( ( sk_c11 = iPr_def_25 )
| ( sk_c11 = iPr_def_14 ) ),
inference(light_normalisation,[status(thm)],[c_14787,c_9392]) ).
tcf(c_14942,plain,
! [X0: $i] :
( ( X0 = sk_c12 )
| ( sk_c12 != multiply(sk_c10,sk_c12) )
| ( X0 != multiply(sk_c10,sk_c12) ) ),
inference(instantiation,[status(thm)],[c_2465]) ).
tcf(c_14943,plain,
! [X0: $i] :
( ( sk_c12 = X0 )
| ( sk_c12 != multiply(sk_c10,sk_c12) )
| ( X0 != multiply(sk_c10,sk_c12) ) ),
inference(instantiation,[status(thm)],[c_1958]) ).
tcf(c_14944,plain,
( ( sk_c12 = sk_c11 )
| ( sk_c11 != multiply(sk_c10,sk_c12) )
| ( sk_c12 != multiply(sk_c10,sk_c12) ) ),
inference(instantiation,[status(thm)],[c_14943]) ).
tcf(c_14945,plain,
( ( sk_c11 = sk_c12 )
| ( sk_c11 != multiply(sk_c10,sk_c12) )
| ( sk_c12 != multiply(sk_c10,sk_c12) ) ),
inference(instantiation,[status(thm)],[c_14942]) ).
tcf(c_15700,plain,
( ( sk_c11 = iPr_def_22 )
| ( multiply(iPr_def_27,iPr_def_28) = iPr_def_27 ) ),
inference(superposition,[status(thm)],[c_2148,c_4593]) ).
tcf(c_15701,plain,
( ( sk_c11 = iPr_def_27 )
| ( sk_c11 = iPr_def_22 ) ),
inference(light_normalisation,[status(thm)],[c_15700,c_9392]) ).
tcf(c_15807,plain,
! [X0: $i] :
( ( X0 = identity )
| ( identity != iPr_def_14 )
| ( X0 != iPr_def_14 ) ),
inference(instantiation,[status(thm)],[c_3155]) ).
tcf(c_15808,plain,
( ( sk_c11 = identity )
| ( identity != iPr_def_14 )
| ( sk_c11 != iPr_def_14 ) ),
inference(instantiation,[status(thm)],[c_15807]) ).
tcf(c_15888,plain,
! [X0: $i] :
( ( X0 = sk_c10 )
| ( sk_c10 != iPr_def_14 )
| ( X0 != iPr_def_14 ) ),
inference(instantiation,[status(thm)],[c_2044]) ).
tcf(c_15889,plain,
( ( sk_c11 = sk_c10 )
| ( sk_c10 != iPr_def_14 )
| ( sk_c11 != iPr_def_14 ) ),
inference(instantiation,[status(thm)],[c_15888]) ).
tcf(c_15905,plain,
( ( sk_c11 = iPr_def_27 )
| ( multiply(iPr_def_16,iPr_def_26) = iPr_def_23 ) ),
inference(superposition,[status(thm)],[c_2199,c_4592]) ).
tcf(c_15906,plain,
( ( sk_c10 = iPr_def_23 )
| ( sk_c11 = iPr_def_27 ) ),
inference(light_normalisation,[status(thm)],[c_15905,c_9387]) ).
tcf(c_17311,plain,
( ( sk_c12 = iPr_def_19 )
| ( multiply(iPr_def_16,iPr_def_26) = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_2554,c_4592]) ).
tcf(c_17312,plain,
( ( sk_c10 = iPr_def_28 )
| ( sk_c12 = iPr_def_19 ) ),
inference(light_normalisation,[status(thm)],[c_17311,c_9387]) ).
tcf(c_17866,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(X0,X1) = X2 )
| ( X2 != multiply(identity,multiply(sk_c10,sk_c12)) )
| ( multiply(X0,X1) != multiply(identity,multiply(sk_c10,sk_c12)) ) ),
inference(instantiation,[status(thm)],[c_3619]) ).
tcf(c_17867,plain,
( ( multiply(sk_c11,sk_c11) = sk_c11 )
| ( sk_c11 != multiply(identity,multiply(sk_c10,sk_c12)) )
| ( multiply(sk_c11,sk_c11) != multiply(identity,multiply(sk_c10,sk_c12)) ) ),
inference(instantiation,[status(thm)],[c_17866]) ).
tcf(c_17885,plain,
( ( sk_c11 = iPr_def_22 )
| ( multiply(iPr_def_16,iPr_def_26) = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_2770,c_4592]) ).
tcf(c_17886,plain,
( ( sk_c10 = iPr_def_28 )
| ( sk_c11 = iPr_def_22 ) ),
inference(light_normalisation,[status(thm)],[c_17885,c_9387]) ).
tcf(c_18127,plain,
( ( sk_c10 = iPr_def_23 )
| ( multiply(iPr_def_16,iPr_def_26) = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_2826,c_4592]) ).
tcf(c_18128,plain,
( ( sk_c10 = iPr_def_28 )
| ( sk_c10 = iPr_def_23 ) ),
inference(light_normalisation,[status(thm)],[c_18127,c_9387]) ).
tcf(c_18835,plain,
( ( sk_c11 = iPr_def_25 )
| ( multiply(iPr_def_16,iPr_def_26) = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_3004,c_4592]) ).
tcf(c_18836,plain,
( ( sk_c10 = iPr_def_28 )
| ( sk_c11 = iPr_def_25 ) ),
inference(light_normalisation,[status(thm)],[c_18835,c_9387]) ).
tcf(c_19712,plain,
( ( sk_c12 = iPr_def_19 )
| ( multiply(iPr_def_29,iPr_def_30) = iPr_def_29 ) ),
inference(superposition,[status(thm)],[c_3123,c_4594]) ).
tcf(c_19713,plain,
( ( sk_c12 = iPr_def_29 )
| ( sk_c12 = iPr_def_19 ) ),
inference(light_normalisation,[status(thm)],[c_19712,c_9432]) ).
tcf(c_19878,plain,
( ( sk_c12 = iPr_def_21 )
| ( multiply(iPr_def_29,iPr_def_30) = iPr_def_29 ) ),
inference(superposition,[status(thm)],[c_3197,c_4594]) ).
tcf(c_19879,plain,
( ( sk_c12 = iPr_def_29 )
| ( sk_c12 = iPr_def_21 ) ),
inference(light_normalisation,[status(thm)],[c_19878,c_9432]) ).
tcf(c_20586,plain,
( ( sk_c12 = iPr_def_24 )
| ( multiply(iPr_def_29,iPr_def_30) = iPr_def_29 ) ),
inference(superposition,[status(thm)],[c_3513,c_4594]) ).
tcf(c_20587,plain,
( ( sk_c12 = iPr_def_29 )
| ( sk_c12 = iPr_def_24 ) ),
inference(light_normalisation,[status(thm)],[c_20586,c_9432]) ).
tcf(c_20664,plain,
( ( sk_c12 = iPr_def_29 )
| ( multiply(iPr_def_27,iPr_def_28) = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_3573,c_4593]) ).
tcf(c_20665,plain,
( ( sk_c11 = iPr_def_25 )
| ( sk_c12 = iPr_def_29 ) ),
inference(light_normalisation,[status(thm)],[c_20664,c_9392]) ).
tcf(c_21115,plain,
( ( sk_c12 = iPr_def_19 )
| ( multiply(iPr_def_27,iPr_def_28) = iPr_def_30 ) ),
inference(superposition,[status(thm)],[c_3840,c_4593]) ).
tcf(c_21116,plain,
( ( sk_c11 = iPr_def_30 )
| ( sk_c12 = iPr_def_19 ) ),
inference(light_normalisation,[status(thm)],[c_21115,c_9392]) ).
tcf(c_21472,plain,
( ( sk_c12 = iPr_def_21 )
| ( multiply(iPr_def_27,iPr_def_28) = iPr_def_30 ) ),
inference(superposition,[status(thm)],[c_4041,c_4593]) ).
tcf(c_21473,plain,
( ( sk_c11 = iPr_def_30 )
| ( sk_c12 = iPr_def_21 ) ),
inference(light_normalisation,[status(thm)],[c_21472,c_9392]) ).
tcf(c_22216,plain,
( ( sk_c12 = iPr_def_24 )
| ( multiply(iPr_def_27,iPr_def_28) = iPr_def_30 ) ),
inference(superposition,[status(thm)],[c_4377,c_4593]) ).
tcf(c_22217,plain,
( ( sk_c11 = iPr_def_30 )
| ( sk_c12 = iPr_def_24 ) ),
inference(light_normalisation,[status(thm)],[c_22216,c_9392]) ).
tcf(c_22300,plain,
( ( sk_c11 = iPr_def_25 )
| ( multiply(iPr_def_27,iPr_def_28) = iPr_def_30 ) ),
inference(superposition,[status(thm)],[c_4475,c_4593]) ).
tcf(c_22301,plain,
( ( sk_c11 = iPr_def_30 )
| ( sk_c11 = iPr_def_25 ) ),
inference(light_normalisation,[status(thm)],[c_22300,c_9392]) ).
tcf(c_23376,plain,
multiply(sk_c6,iPr_def_19) = multiply(iPr_def_21,sk_c11),
inference(superposition,[status(thm)],[c_839,c_4574]) ).
tcf(c_25741,plain,
( ( iPr_def_17 = iPr_def_20 )
| ( multiply(iPr_def_16,iPr_def_26) = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_1451,c_4772]) ).
tcf(c_25751,plain,
( ( iPr_def_17 = iPr_def_20 )
| ( sk_c10 = iPr_def_14 ) ),
inference(light_normalisation,[status(thm)],[c_25741,c_9387]) ).
tcf(c_32249,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(X0,X1)) = X1,
inference(demodulation,[status(thm)],[c_4581,c_123]) ).
tcf(c_32281,plain,
! [X0: $i] : multiply(inverse(identity),X0) = X0,
inference(superposition,[status(thm)],[c_123,c_32249]) ).
tcf(c_32282,plain,
! [X0: $i] : multiply(inverse(inverse(X0)),identity) = X0,
inference(superposition,[status(thm)],[c_124,c_32249]) ).
tcf(c_32283,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(inverse(multiply(X0,X1)),multiply(X0,multiply(X1,X2))) = X2,
inference(superposition,[status(thm)],[c_125,c_32249]) ).
tcf(c_32550,plain,
! [X0: $i] : multiply(inverse(iPr_def_24),X0) = multiply(sk_c4,X0),
inference(superposition,[status(thm)],[c_4599,c_32249]) ).
tcf(c_32551,plain,
! [X0: $i] : multiply(inverse(iPr_def_22),X0) = multiply(sk_c5,X0),
inference(superposition,[status(thm)],[c_4598,c_32249]) ).
tcf(c_32552,plain,
! [X0: $i] : multiply(inverse(iPr_def_20),X0) = multiply(sk_c6,X0),
inference(superposition,[status(thm)],[c_4597,c_32249]) ).
tcf(c_32554,plain,
! [X0: $i] : multiply(inverse(iPr_def_17),X0) = multiply(sk_c7,X0),
inference(superposition,[status(thm)],[c_4595,c_32249]) ).
tcf(c_32555,plain,
! [X0: $i] : multiply(inverse(iPr_def_29),X0) = multiply(sk_c1,X0),
inference(superposition,[status(thm)],[c_4594,c_32249]) ).
tcf(c_32556,plain,
! [X0: $i] : multiply(inverse(iPr_def_27),X0) = multiply(sk_c2,X0),
inference(superposition,[status(thm)],[c_4593,c_32249]) ).
tcf(c_32557,plain,
! [X0: $i] : multiply(inverse(iPr_def_16),X0) = multiply(sk_c3,X0),
inference(superposition,[status(thm)],[c_4592,c_32249]) ).
tcf(c_32665,plain,
! [X0: $i,X1: $i] : multiply(inverse(inverse(X0)),X1) = multiply(X0,X1),
inference(superposition,[status(thm)],[c_32249,c_32249]) ).
tcf(c_34290,plain,
! [X0: $i] : multiply(X0,identity) = X0,
inference(demodulation,[status(thm)],[c_32282,c_32665]) ).
tcf(c_34322,plain,
inverse(identity) = identity,
inference(superposition,[status(thm)],[c_34290,c_32281]) ).
tcf(c_34639,plain,
( ( sk_c10 = iPr_def_23 )
| ~ iPr_def_12
| ( iPr_def_16 != iPr_def_28 )
| ( sk_c12 != iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_905,c_5106]) ).
tcf(c_34646,plain,
( ( sk_c11 = iPr_def_25 )
| ~ iPr_def_12
| ( sk_c12 != iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_867,c_5106]) ).
tcf(c_34647,plain,
( ( sk_c12 = iPr_def_24 )
| ~ iPr_def_12
| ( sk_c12 != iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_866,c_5106]) ).
tcf(c_34649,plain,
( ( sk_c11 = iPr_def_22 )
| ~ iPr_def_12
| ( sk_c12 != iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_864,c_5106]) ).
tcf(c_34650,plain,
( ( sk_c12 = iPr_def_21 )
| ~ iPr_def_12
| ( sk_c12 != iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_863,c_5106]) ).
tcf(c_34651,plain,
( ( sk_c12 = iPr_def_19 )
| ~ iPr_def_12
| ( sk_c12 != iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_861,c_5106]) ).
tcf(c_34821,plain,
( ~ iPr_def_11
| ( sk_c10 != iPr_def_28 ) ),
inference(global_subsumption_just,[status(thm)],[c_5311,c_5318,c_5311,c_15701,c_15906]) ).
tcf(c_34823,plain,
~ iPr_def_11,
inference(global_subsumption_just,[status(thm)],[c_34821,c_5318,c_17886,c_18128,c_34821]) ).
tcf(c_34825,plain,
( iPr_def_13
| iPr_def_10
| ( sk_c12 = iPr_def_19 ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_9341,c_34823]) ).
tcf(c_34829,plain,
( iPr_def_13
| iPr_def_12
| iPr_def_10
| ( sk_c11 != iPr_def_14 ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_851,c_34823]) ).
tcf(c_34898,plain,
( iPr_def_13
| iPr_def_12
| iPr_def_10
| ( sk_c12 = iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_886,c_34829]) ).
tcf(c_34900,plain,
( iPr_def_13
| iPr_def_12
| iPr_def_10
| ( sk_c12 = iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_883,c_34829]) ).
tcf(c_35102,plain,
( iPr_def_13
| ( sk_c12 = iPr_def_24 ) ),
inference(global_subsumption_just,[status(thm)],[c_34898,c_851,c_886,c_1956,c_4540,c_5318,c_5526,c_13673,c_17886,c_18128,c_20587,c_22217,c_34647,c_34821]) ).
tcf(c_35108,plain,
( iPr_def_13
| ( sk_c12 = iPr_def_21 ) ),
inference(global_subsumption_just,[status(thm)],[c_34900,c_851,c_883,c_1956,c_4517,c_5318,c_5526,c_13203,c_17886,c_18128,c_19879,c_21473,c_34650,c_34821]) ).
tcf(c_35126,plain,
( iPr_def_13
| ( sk_c12 = iPr_def_19 ) ),
inference(global_subsumption_just,[status(thm)],[c_34825,c_5526,c_13223,c_13904,c_19713,c_21116,c_34651,c_34829]) ).
tcf(c_35156,plain,
( ~ iPr_def_10
| ( sk_c11 != iPr_def_25 ) ),
inference(global_subsumption_just,[status(thm)],[c_5522,c_5526,c_5522,c_20587,c_22217]) ).
tcf(c_35158,plain,
~ iPr_def_10,
inference(global_subsumption_just,[status(thm)],[c_35156,c_5526,c_20665,c_22301,c_35156]) ).
tcf(c_35160,plain,
( iPr_def_13
| iPr_def_12
| ( sk_c11 != iPr_def_14 ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_34829,c_35158]) ).
tcf(c_35200,plain,
( iPr_def_13
| iPr_def_12
| ( sk_c11 = iPr_def_25 )
| ( iPr_def_14 != iPr_def_30 ) ),
inference(superposition,[status(thm)],[c_927,c_35160]) ).
tcf(c_35202,plain,
( iPr_def_13
| iPr_def_12
| ( sk_c11 = iPr_def_22 )
| ( iPr_def_14 != iPr_def_30 ) ),
inference(superposition,[status(thm)],[c_924,c_35160]) ).
tcf(c_35206,plain,
( iPr_def_13
| iPr_def_12
| ( sk_c12 = iPr_def_29 )
| ( iPr_def_14 != iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_914,c_35160]) ).
tcf(c_35214,plain,
( iPr_def_13
| iPr_def_12
| ( sk_c11 = iPr_def_14 )
| ( iPr_def_14 != iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_884,c_35160]) ).
tcf(c_35318,plain,
! [X0: $i] :
( ( iPr_def_14 = iPr_def_19 )
| ( iPr_def_19 != X0 )
| ( iPr_def_14 != X0 ) ),
inference(instantiation,[status(thm)],[c_1710]) ).
tcf(c_35336,plain,
( iPr_def_13
| ( sk_c11 = iPr_def_25 ) ),
inference(global_subsumption_just,[status(thm)],[c_35200,c_5526,c_13746,c_14788,c_20665,c_22301,c_34646,c_34829,c_35156]) ).
tcf(c_35342,plain,
( iPr_def_13
| ( sk_c11 = iPr_def_22 ) ),
inference(global_subsumption_just,[status(thm)],[c_35202,c_5526,c_13321,c_14314,c_20665,c_22301,c_34649,c_34829,c_35156]) ).
tcf(c_35356,plain,
( iPr_def_13
| iPr_def_12
| ( iPr_def_14 != iPr_def_22 ) ),
inference(global_subsumption_just,[status(thm)],[c_35206,c_35160,c_35214]) ).
tcf(c_35641,plain,
( ( iPr_def_22 = iPr_def_25 )
| ( iPr_def_14 = iPr_def_30 ) ),
inference(superposition,[status(thm)],[c_6148,c_6146]) ).
tcf(c_36269,plain,
multiply(sk_c4,iPr_def_24) = identity,
inference(superposition,[status(thm)],[c_32550,c_124]) ).
tcf(c_36271,plain,
( ~ iPr_def_12
| ( inverse(inverse(iPr_def_24)) != sk_c10 )
| ( multiply(sk_c4,sk_c10) != sk_c12 ) ),
inference(superposition,[status(thm)],[c_32550,c_855]) ).
tcf(c_36273,plain,
multiply(sk_c4,identity) = inverse(iPr_def_24),
inference(superposition,[status(thm)],[c_32550,c_34290]) ).
tcf(c_36637,plain,
inverse(iPr_def_24) = sk_c4,
inference(demodulation,[status(thm)],[c_36273,c_34290]) ).
tcf(c_36639,plain,
( ( iPr_def_14 = iPr_def_16 )
| ( inverse(iPr_def_21) = sk_c4 ) ),
inference(superposition,[status(thm)],[c_12121,c_36637]) ).
tcf(c_36906,plain,
multiply(sk_c5,identity) = inverse(iPr_def_22),
inference(superposition,[status(thm)],[c_32551,c_34290]) ).
tcf(c_36978,plain,
inverse(iPr_def_22) = sk_c5,
inference(demodulation,[status(thm)],[c_36906,c_34290]) ).
tcf(c_39163,plain,
multiply(sk_c6,iPr_def_20) = identity,
inference(superposition,[status(thm)],[c_32552,c_124]) ).
tcf(c_39167,plain,
multiply(sk_c6,identity) = inverse(iPr_def_20),
inference(superposition,[status(thm)],[c_32552,c_34290]) ).
tcf(c_39181,plain,
( ( identity = iPr_def_21 )
| ( sk_c10 = iPr_def_28 ) ),
inference(demodulation,[status(thm)],[c_2678,c_39163]) ).
tcf(c_39182,plain,
( ( identity = iPr_def_21 )
| ( sk_c11 = iPr_def_27 ) ),
inference(demodulation,[status(thm)],[c_2058,c_39163]) ).
tcf(c_39183,plain,
( ( identity = iPr_def_21 )
| ( sk_c11 = iPr_def_14 ) ),
inference(demodulation,[status(thm)],[c_1686,c_39163]) ).
tcf(c_39184,plain,
( ( identity = iPr_def_21 )
| ( sk_c10 = iPr_def_16 ) ),
inference(demodulation,[status(thm)],[c_1488,c_39163]) ).
tcf(c_39185,plain,
( ( identity = iPr_def_21 )
| ( sk_c12 = iPr_def_26 ) ),
inference(demodulation,[status(thm)],[c_1486,c_39163]) ).
tcf(c_40176,plain,
( ( identity = iPr_def_21 )
| ~ iPr_def_12
| ( iPr_def_16 != iPr_def_28 )
| ( sk_c12 != iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_39181,c_5106]) ).
tcf(c_40240,plain,
( ( identity = iPr_def_21 )
| ( multiply(iPr_def_28,sk_c12) = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_39181,c_834]) ).
tcf(c_40812,plain,
inverse(iPr_def_20) = sk_c6,
inference(demodulation,[status(thm)],[c_39167,c_34290]) ).
tcf(c_41161,plain,
( ( identity = iPr_def_21 )
| ( multiply(sk_c2,iPr_def_27) = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_39182,c_848]) ).
tcf(c_41371,plain,
( iPr_def_13
| iPr_def_12
| ( identity = iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_39183,c_35160]) ).
tcf(c_41549,plain,
( ( iPr_def_16 = iPr_def_28 )
| ( identity = iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_39184,c_39181]) ).
tcf(c_41619,plain,
( ( identity = iPr_def_21 )
| ( multiply(iPr_def_16,sk_c12) = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_39184,c_834]) ).
tcf(c_42606,plain,
( iPr_def_13
| ( identity = iPr_def_21 ) ),
inference(global_subsumption_just,[status(thm)],[c_41371,c_34829,c_35158,c_39185,c_39183,c_40176,c_41549]) ).
tcf(c_45697,plain,
multiply(sk_c7,iPr_def_17) = identity,
inference(superposition,[status(thm)],[c_32554,c_124]) ).
tcf(c_45700,plain,
! [X0: $i] : multiply(sk_c7,multiply(iPr_def_17,X0)) = X0,
inference(superposition,[status(thm)],[c_32554,c_32249]) ).
tcf(c_45701,plain,
multiply(sk_c7,identity) = inverse(iPr_def_17),
inference(superposition,[status(thm)],[c_32554,c_34290]) ).
tcf(c_46198,plain,
inverse(iPr_def_17) = sk_c7,
inference(demodulation,[status(thm)],[c_45701,c_34290]) ).
tcf(c_46867,plain,
( ( identity = iPr_def_21 )
| ( multiply(iPr_def_16,iPr_def_26) = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_39185,c_41619]) ).
tcf(c_46912,plain,
( ( identity = iPr_def_21 )
| ( sk_c10 = iPr_def_14 ) ),
inference(light_normalisation,[status(thm)],[c_46867,c_9387]) ).
tcf(c_46985,plain,
( ( iPr_def_14 = iPr_def_16 )
| ( identity = iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_46912,c_39184]) ).
tcf(c_47124,plain,
( ( iPr_def_14 = iPr_def_16 )
| ( inverse(iPr_def_21) = iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_46985,c_34322]) ).
tcf(c_47126,plain,
! [X0: $i] :
( ( iPr_def_14 = iPr_def_16 )
| ( multiply(iPr_def_21,X0) = X0 ) ),
inference(superposition,[status(thm)],[c_46985,c_123]) ).
tcf(c_47576,plain,
multiply(sk_c1,iPr_def_29) = identity,
inference(superposition,[status(thm)],[c_32555,c_124]) ).
tcf(c_47609,plain,
( ( iPr_def_22 = iPr_def_25 )
| ( identity = iPr_def_30 ) ),
inference(demodulation,[status(thm)],[c_7915,c_47576]) ).
tcf(c_49572,plain,
multiply(sk_c2,iPr_def_27) = identity,
inference(superposition,[status(thm)],[c_32556,c_124]) ).
tcf(c_49599,plain,
( ( identity = iPr_def_28 )
| ( identity = iPr_def_21 ) ),
inference(demodulation,[status(thm)],[c_41161,c_49572]) ).
tcf(c_49600,plain,
( ( iPr_def_17 = iPr_def_20 )
| ( identity = iPr_def_28 ) ),
inference(demodulation,[status(thm)],[c_6442,c_49572]) ).
tcf(c_49602,plain,
( ( identity = iPr_def_28 )
| ( sk_c11 = iPr_def_25 ) ),
inference(demodulation,[status(thm)],[c_2332,c_49572]) ).
tcf(c_49603,plain,
( ( identity = iPr_def_28 )
| ( sk_c12 = iPr_def_24 ) ),
inference(demodulation,[status(thm)],[c_2271,c_49572]) ).
tcf(c_49604,plain,
( ( identity = iPr_def_28 )
| ( sk_c11 = iPr_def_22 ) ),
inference(demodulation,[status(thm)],[c_2148,c_49572]) ).
tcf(c_49605,plain,
( ( identity = iPr_def_28 )
| ( sk_c12 = iPr_def_21 ) ),
inference(demodulation,[status(thm)],[c_2089,c_49572]) ).
tcf(c_49606,plain,
( ( identity = iPr_def_28 )
| ( sk_c12 = iPr_def_19 ) ),
inference(demodulation,[status(thm)],[c_1994,c_49572]) ).
tcf(c_49798,plain,
! [X0: $i] :
( ( identity = iPr_def_21 )
| ( multiply(iPr_def_28,X0) = X0 ) ),
inference(superposition,[status(thm)],[c_49599,c_123]) ).
tcf(c_51514,plain,
( ( iPr_def_22 = iPr_def_25 )
| ( identity = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_49604,c_49602]) ).
tcf(c_51894,plain,
( ( iPr_def_19 = iPr_def_21 )
| ( identity = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_49606,c_49605]) ).
tcf(c_51895,plain,
( ( iPr_def_19 = iPr_def_24 )
| ( identity = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_49606,c_49603]) ).
tcf(c_53852,plain,
( ( iPr_def_28 = iPr_def_30 )
| ( iPr_def_22 = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_51514,c_47609]) ).
tcf(c_56386,plain,
( ( sk_c10 = identity )
| ( identity != iPr_def_28 )
| ( sk_c10 != iPr_def_28 ) ),
inference(instantiation,[status(thm)],[c_8970]) ).
tcf(c_56690,plain,
( ( identity = sk_c10 )
| ( identity != iPr_def_28 )
| ( sk_c10 != iPr_def_28 ) ),
inference(instantiation,[status(thm)],[c_8971]) ).
tcf(c_56693,plain,
! [X0: $i] :
( ( X0 = identity )
| ( identity != sk_c10 )
| ( X0 != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_3155]) ).
tcf(c_56694,plain,
( ( sk_c11 = identity )
| ( identity != sk_c10 )
| ( sk_c11 != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_56693]) ).
tcf(c_57232,plain,
( ( iPr_def_22 = iPr_def_25 )
| ( iPr_def_14 = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_53852,c_35641]) ).
tcf(c_57671,plain,
! [X0: $i] :
( ( sk_c12 = multiply(sk_c10,sk_c12) )
| ( sk_c12 != X0 )
| ( multiply(sk_c10,sk_c12) != X0 ) ),
inference(instantiation,[status(thm)],[c_1826]) ).
tcf(c_63263,plain,
( ( identity = iPr_def_21 )
| ( sk_c12 = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_49798,c_40240]) ).
tcf(c_79602,plain,
multiply(sk_c3,iPr_def_16) = identity,
inference(superposition,[status(thm)],[c_32557,c_124]) ).
tcf(c_79619,plain,
( ( identity = iPr_def_26 )
| ( sk_c12 = iPr_def_19 ) ),
inference(demodulation,[status(thm)],[c_1509,c_79602]) ).
tcf(c_79620,plain,
( ( identity = iPr_def_26 )
| ( sk_c12 = iPr_def_21 ) ),
inference(demodulation,[status(thm)],[c_1508,c_79602]) ).
tcf(c_79621,plain,
( ( identity = iPr_def_26 )
| ( sk_c11 = iPr_def_22 ) ),
inference(demodulation,[status(thm)],[c_1507,c_79602]) ).
tcf(c_79622,plain,
( ( identity = iPr_def_26 )
| ( sk_c12 = iPr_def_24 ) ),
inference(demodulation,[status(thm)],[c_1505,c_79602]) ).
tcf(c_79623,plain,
( ( identity = iPr_def_26 )
| ( sk_c11 = iPr_def_25 ) ),
inference(demodulation,[status(thm)],[c_1504,c_79602]) ).
tcf(c_81139,plain,
( ( iPr_def_19 = iPr_def_21 )
| ( identity = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_79620,c_79619]) ).
tcf(c_81642,plain,
( ( iPr_def_19 = iPr_def_24 )
| ( identity = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_79622,c_79619]) ).
tcf(c_81881,plain,
( ( iPr_def_22 = iPr_def_25 )
| ( identity = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_79623,c_79621]) ).
tcf(c_85201,plain,
( ( iPr_def_26 = iPr_def_28 )
| ( iPr_def_19 = iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_81139,c_51894]) ).
tcf(c_86124,plain,
( ( sk_c12 = multiply(sk_c10,sk_c12) )
| ( sk_c12 != multiply(identity,iPr_def_29) )
| ( multiply(sk_c10,sk_c12) != multiply(identity,iPr_def_29) ) ),
inference(instantiation,[status(thm)],[c_57671]) ).
tcf(c_86323,plain,
( ( iPr_def_26 = iPr_def_28 )
| ( iPr_def_19 = iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_81642,c_51895]) ).
tcf(c_86747,plain,
( ( iPr_def_26 = iPr_def_28 )
| ( iPr_def_22 = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_81881,c_51514]) ).
tcf(c_87086,plain,
( ( multiply(sk_c10,sk_c12) = multiply(identity,iPr_def_29) )
| ( sk_c10 != identity )
| ( sk_c12 != iPr_def_29 ) ),
inference(instantiation,[status(thm)],[c_4094]) ).
tcf(c_89594,plain,
( ( iPr_def_19 = iPr_def_21 )
| ( iPr_def_14 = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_85201,c_11629]) ).
tcf(c_91280,plain,
( ( iPr_def_19 = iPr_def_24 )
| ( iPr_def_14 = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_86323,c_11978]) ).
tcf(c_91924,plain,
( ( iPr_def_22 = iPr_def_25 )
| ( iPr_def_14 = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_86747,c_57232]) ).
tcf(c_102264,plain,
( ( iPr_def_14 = iPr_def_19 )
| ( iPr_def_19 != iPr_def_26 )
| ( iPr_def_14 != iPr_def_26 ) ),
inference(instantiation,[status(thm)],[c_35318]) ).
tcf(c_104924,plain,
( ( iPr_def_14 = iPr_def_16 )
| ( sk_c4 = iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_47124,c_36639]) ).
tcf(c_104988,plain,
( ( iPr_def_14 = iPr_def_16 )
| ( multiply(iPr_def_21,sk_c12) = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_104924,c_845]) ).
tcf(c_106338,plain,
( ( iPr_def_14 = iPr_def_16 )
| ( sk_c12 = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_104988,c_47126]) ).
tcf(c_106732,plain,
( ( iPr_def_14 = iPr_def_16 )
| ( multiply(sk_c10,iPr_def_25) = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_106338,c_834]) ).
tcf(c_111013,plain,
! [X0: $i,X1: $i] :
( ( multiply(inverse(X0),sk_c11) = sk_c12 )
| ( sk_c12 != X1 )
| ( multiply(inverse(X0),sk_c11) != X1 ) ),
inference(instantiation,[status(thm)],[c_929]) ).
tcf(c_111014,plain,
( ( multiply(inverse(sk_c11),sk_c11) = sk_c12 )
| ( sk_c12 != sk_c11 )
| ( multiply(inverse(sk_c11),sk_c11) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_111013]) ).
tcf(c_111015,plain,
! [X0: $i,X1: $i] :
( ( multiply(X0,inverse(X0)) = sk_c12 )
| ( sk_c12 != X1 )
| ( multiply(X0,inverse(X0)) != X1 ) ),
inference(instantiation,[status(thm)],[c_929]) ).
tcf(c_111027,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(X0,inverse(X0)) = X2 )
| ( X2 != X1 )
| ( multiply(X0,inverse(X0)) != X1 ) ),
inference(instantiation,[status(thm)],[c_929]) ).
tcf(c_111028,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(X0,inverse(X0)) = sk_c12 )
| ( sk_c12 != multiply(X1,X2) )
| ( multiply(X0,inverse(X0)) != multiply(X1,X2) ) ),
inference(instantiation,[status(thm)],[c_111015]) ).
tcf(c_111029,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(X0,inverse(X0)) = multiply(X2,X1) )
| ( X0 != X2 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_930]) ).
tcf(c_111030,plain,
( ( multiply(sk_c11,inverse(sk_c11)) = sk_c12 )
| ( sk_c12 != multiply(sk_c11,sk_c11) )
| ( multiply(sk_c11,inverse(sk_c11)) != multiply(sk_c11,sk_c11) ) ),
inference(instantiation,[status(thm)],[c_111028]) ).
tcf(c_111031,plain,
( ( multiply(sk_c11,inverse(sk_c11)) = multiply(sk_c11,sk_c11) )
| ( sk_c11 != sk_c11 )
| ( inverse(sk_c11) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_111029]) ).
tcf(c_111057,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( sk_c12 = multiply(X0,X1) )
| ( sk_c12 != X2 )
| ( multiply(X0,X1) != X2 ) ),
inference(instantiation,[status(thm)],[c_929]) ).
tcf(c_111058,plain,
( ( sk_c12 = multiply(sk_c11,sk_c11) )
| ( sk_c12 != sk_c11 )
| ( multiply(sk_c11,sk_c11) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_111057]) ).
tcf(c_111061,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( inverse(X0) = X2 )
| ( X2 != X1 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_929]) ).
tcf(c_111062,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(X0,inverse(X0)) = multiply(X2,inverse(X1)) )
| ( X0 != X2 )
| ( inverse(X0) != inverse(X1) ) ),
inference(instantiation,[status(thm)],[c_111029]) ).
tcf(c_111076,plain,
! [X0: $i] :
( ( inverse(X0) = inverse(identity) )
| ( X0 != identity ) ),
inference(instantiation,[status(thm)],[c_931]) ).
tcf(c_111078,plain,
( ( inverse(sk_c11) = inverse(identity) )
| ( sk_c11 != identity ) ),
inference(instantiation,[status(thm)],[c_111076]) ).
tcf(c_111107,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( inverse(X0) = X2 )
| ( X2 != inverse(X1) )
| ( inverse(X0) != inverse(X1) ) ),
inference(instantiation,[status(thm)],[c_111061]) ).
tcf(c_111111,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(X0,inverse(X0)) = X2 )
| ( X2 != multiply(X1,inverse(X0)) )
| ( multiply(X0,inverse(X0)) != multiply(X1,inverse(X0)) ) ),
inference(instantiation,[status(thm)],[c_111027]) ).
tcf(c_111189,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( X3 = multiply(X0,inverse(X1)) )
| ( X3 != X2 )
| ( multiply(X0,inverse(X1)) != X2 ) ),
inference(instantiation,[status(thm)],[c_929]) ).
tcf(c_111225,plain,
! [X0: $i,X1: $i] :
( ( inverse(X1) = multiply(identity,inverse(X0)) )
| ( inverse(X1) != inverse(X0) )
| ( multiply(identity,inverse(X0)) != inverse(X0) ) ),
inference(instantiation,[status(thm)],[c_111107]) ).
tcf(c_111226,plain,
! [X0: $i] : multiply(identity,inverse(X0)) = inverse(X0),
inference(instantiation,[status(thm)],[c_123]) ).
tcf(c_111227,plain,
( ( inverse(sk_c11) = multiply(identity,inverse(sk_c11)) )
| ( inverse(sk_c11) != inverse(sk_c11) )
| ( multiply(identity,inverse(sk_c11)) != inverse(sk_c11) ) ),
inference(instantiation,[status(thm)],[c_111225]) ).
tcf(c_111228,plain,
multiply(identity,inverse(sk_c11)) = inverse(sk_c11),
inference(instantiation,[status(thm)],[c_111226]) ).
tcf(c_111500,plain,
! [X0: $i] : multiply(inverse(inverse(X0)),inverse(X0)) = identity,
inference(instantiation,[status(thm)],[c_124]) ).
tcf(c_111502,plain,
multiply(inverse(inverse(sk_c11)),inverse(sk_c11)) = identity,
inference(instantiation,[status(thm)],[c_111500]) ).
tcf(c_111508,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( multiply(X0,inverse(X1)) = X3 )
| ( X3 != X2 )
| ( multiply(X0,inverse(X1)) != X2 ) ),
inference(instantiation,[status(thm)],[c_929]) ).
tcf(c_111946,plain,
! [X0: $i,X1: $i] :
( ( multiply(X0,inverse(X0)) = inverse(X1) )
| ( inverse(X1) != multiply(identity,inverse(X0)) )
| ( multiply(X0,inverse(X0)) != multiply(identity,inverse(X0)) ) ),
inference(instantiation,[status(thm)],[c_111111]) ).
tcf(c_111947,plain,
( ( multiply(sk_c11,inverse(sk_c11)) = inverse(sk_c11) )
| ( inverse(sk_c11) != multiply(identity,inverse(sk_c11)) )
| ( multiply(sk_c11,inverse(sk_c11)) != multiply(identity,inverse(sk_c11)) ) ),
inference(instantiation,[status(thm)],[c_111946]) ).
tcf(c_113175,plain,
! [X0: $i,X1: $i] :
( ( X1 = multiply(inverse(inverse(X0)),inverse(X0)) )
| ( X1 != identity )
| ( multiply(inverse(inverse(X0)),inverse(X0)) != identity ) ),
inference(instantiation,[status(thm)],[c_111189]) ).
tcf(c_113177,plain,
( ( sk_c11 = multiply(inverse(inverse(sk_c11)),inverse(sk_c11)) )
| ( sk_c11 != identity )
| ( multiply(inverse(inverse(sk_c11)),inverse(sk_c11)) != identity ) ),
inference(instantiation,[status(thm)],[c_113175]) ).
tcf(c_113399,plain,
! [X0: $i,X1: $i] :
( ( multiply(X0,inverse(X0)) = multiply(identity,inverse(X1)) )
| ( X0 != identity )
| ( inverse(X0) != inverse(X1) ) ),
inference(instantiation,[status(thm)],[c_111062]) ).
tcf(c_113400,plain,
( ( multiply(sk_c11,inverse(sk_c11)) = multiply(identity,inverse(sk_c11)) )
| ( sk_c11 != identity )
| ( inverse(sk_c11) != inverse(sk_c11) ) ),
inference(instantiation,[status(thm)],[c_113399]) ).
tcf(c_113645,plain,
! [X0: $i,X1: $i] :
( ( multiply(inverse(inverse(X0)),inverse(X0)) = X1 )
| ( X1 != identity )
| ( multiply(inverse(inverse(X0)),inverse(X0)) != identity ) ),
inference(instantiation,[status(thm)],[c_111508]) ).
tcf(c_134225,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( inverse(X0) = X2 )
| ( X2 != multiply(inverse(inverse(X1)),inverse(X1)) )
| ( inverse(X0) != multiply(inverse(inverse(X1)),inverse(X1)) ) ),
inference(instantiation,[status(thm)],[c_111061]) ).
tcf(c_134229,plain,
( ( inverse(sk_c11) = sk_c11 )
| ( sk_c11 != multiply(inverse(inverse(sk_c11)),inverse(sk_c11)) )
| ( inverse(sk_c11) != multiply(inverse(inverse(sk_c11)),inverse(sk_c11)) ) ),
inference(instantiation,[status(thm)],[c_134225]) ).
tcf(c_135297,plain,
! [X0: $i] :
( ( multiply(inverse(inverse(X0)),inverse(X0)) = inverse(identity) )
| ( inverse(identity) != identity )
| ( multiply(inverse(inverse(X0)),inverse(X0)) != identity ) ),
inference(instantiation,[status(thm)],[c_113645]) ).
tcf(c_135300,plain,
( ( multiply(inverse(inverse(sk_c11)),inverse(sk_c11)) = inverse(identity) )
| ( inverse(identity) != identity )
| ( multiply(inverse(inverse(sk_c11)),inverse(sk_c11)) != identity ) ),
inference(instantiation,[status(thm)],[c_135297]) ).
tcf(c_146067,plain,
! [X0: $i] : multiply(inverse(multiply(X0,sk_c9)),multiply(X0,iPr_def_19)) = sk_c11,
inference(superposition,[status(thm)],[c_839,c_32283]) ).
tcf(c_158196,plain,
! [X0: $i,X1: $i] :
( ( inverse(X1) = multiply(inverse(inverse(X0)),inverse(X0)) )
| ( inverse(X1) != inverse(identity) )
| ( multiply(inverse(inverse(X0)),inverse(X0)) != inverse(identity) ) ),
inference(instantiation,[status(thm)],[c_111107]) ).
tcf(c_158197,plain,
( ( inverse(sk_c11) = multiply(inverse(inverse(sk_c11)),inverse(sk_c11)) )
| ( inverse(sk_c11) != inverse(identity) )
| ( multiply(inverse(inverse(sk_c11)),inverse(sk_c11)) != inverse(identity) ) ),
inference(instantiation,[status(thm)],[c_158196]) ).
tcf(c_163837,plain,
multiply(inverse(multiply(inverse(iPr_def_19),sk_c9)),identity) = sk_c11,
inference(superposition,[status(thm)],[c_124,c_146067]) ).
tcf(c_165907,plain,
inverse(multiply(inverse(iPr_def_19),sk_c9)) = sk_c11,
inference(demodulation,[status(thm)],[c_163837,c_34290]) ).
tcf(c_166369,plain,
! [X0: $i,X1: $i] :
( ( inverse(inverse(X0)) = inverse(X1) )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_931]) ).
tcf(c_166370,plain,
( ( inverse(inverse(sk_c11)) = inverse(sk_c11) )
| ( inverse(sk_c11) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_166369]) ).
tcf(c_167220,plain,
sk_c12 = iPr_def_19,
inference(global_subsumption_just,[status(thm)],[c_10768,c_198,c_933,c_934,c_938,c_834,c_1824,c_1923,c_2188,c_2241,c_2310,c_2970,c_3365,c_3611,c_10769,c_13561,c_13562,c_13904,c_14944,c_15889,c_17312,c_17867,c_19713,c_34322,c_35126,c_49606,c_56386,c_56690,c_56694,c_86124,c_87086,c_111014,c_111030,c_111031,c_111058,c_111078,c_111227,c_111228,c_111502,c_111947,c_113177,c_113400,c_134229,c_135300,c_158197,c_166370]) ).
tcf(c_167284,plain,
( ( iPr_def_19 = iPr_def_26 )
| ( identity = iPr_def_21 ) ),
inference(demodulation,[status(thm)],[c_39185,c_167220]) ).
tcf(c_167289,plain,
( iPr_def_13
| ( iPr_def_19 = iPr_def_21 ) ),
inference(demodulation,[status(thm)],[c_35108,c_167220]) ).
tcf(c_167290,plain,
( iPr_def_13
| ( iPr_def_19 = iPr_def_24 ) ),
inference(demodulation,[status(thm)],[c_35102,c_167220]) ).
tcf(c_167414,plain,
( ( sk_c11 = iPr_def_14 )
| ( multiply(iPr_def_23,iPr_def_19) = iPr_def_14 ) ),
inference(demodulation,[status(thm)],[c_1795,c_167220]) ).
tcf(c_167440,plain,
( ( iPr_def_19 = iPr_def_24 )
| ( sk_c10 = iPr_def_14 ) ),
inference(demodulation,[status(thm)],[c_10829,c_167220]) ).
tcf(c_167451,plain,
( ( iPr_def_19 = iPr_def_21 )
| ( sk_c10 = iPr_def_14 ) ),
inference(demodulation,[status(thm)],[c_10151,c_167220]) ).
tcf(c_167467,plain,
( ( iPr_def_19 = iPr_def_29 )
| ( iPr_def_17 = iPr_def_20 ) ),
inference(demodulation,[status(thm)],[c_3172,c_167220]) ).
tcf(c_167491,plain,
( ( iPr_def_19 = iPr_def_24 )
| ( sk_c10 = iPr_def_28 ) ),
inference(demodulation,[status(thm)],[c_906,c_167220]) ).
tcf(c_167492,plain,
( ( iPr_def_19 = iPr_def_21 )
| ( sk_c10 = iPr_def_28 ) ),
inference(demodulation,[status(thm)],[c_903,c_167220]) ).
tcf(c_167497,plain,
( ( iPr_def_19 = iPr_def_24 )
| ( sk_c11 = iPr_def_14 ) ),
inference(demodulation,[status(thm)],[c_886,c_167220]) ).
tcf(c_167498,plain,
( ( iPr_def_19 = iPr_def_21 )
| ( sk_c11 = iPr_def_14 ) ),
inference(demodulation,[status(thm)],[c_883,c_167220]) ).
tcf(c_167501,plain,
( ( iPr_def_19 = iPr_def_26 )
| ( iPr_def_19 = iPr_def_24 ) ),
inference(demodulation,[status(thm)],[c_876,c_167220]) ).
tcf(c_167505,plain,
multiply(sk_c4,iPr_def_19) = iPr_def_25,
inference(demodulation,[status(thm)],[c_845,c_167220]) ).
tcf(c_167506,plain,
( ( iPr_def_19 = iPr_def_26 )
| ( iPr_def_19 = iPr_def_21 ) ),
inference(demodulation,[status(thm)],[c_873,c_167220]) ).
tcf(c_167513,plain,
multiply(sk_c10,iPr_def_19) = iPr_def_14,
inference(demodulation,[status(thm)],[c_834,c_167220]) ).
tcf(c_167955,plain,
iPr_def_19 = iPr_def_21,
inference(global_subsumption_just,[status(thm)],[c_167289,c_198,c_933,c_934,c_938,c_834,c_1824,c_1923,c_2188,c_2241,c_2310,c_2970,c_2980,c_3365,c_3611,c_8515,c_10769,c_13561,c_13562,c_13904,c_14944,c_15889,c_17312,c_17867,c_19713,c_34322,c_35126,c_49606,c_51894,c_56386,c_56690,c_56694,c_86124,c_87086,c_89594,c_102264,c_111014,c_111030,c_111031,c_111058,c_111078,c_111227,c_111228,c_111502,c_111947,c_113177,c_113400,c_134229,c_135300,c_158197,c_166370,c_167289,c_167451,c_167506,c_167498,c_167492]) ).
tcf(c_168174,plain,
multiply(sk_c6,iPr_def_19) = multiply(iPr_def_19,sk_c11),
inference(demodulation,[status(thm)],[c_23376,c_167955]) ).
tcf(c_168193,plain,
multiply(iPr_def_20,iPr_def_19) = sk_c9,
inference(demodulation,[status(thm)],[c_9777,c_167955]) ).
tcf(c_168536,plain,
iPr_def_19 = iPr_def_24,
inference(global_subsumption_just,[status(thm)],[c_167290,c_198,c_933,c_934,c_938,c_834,c_1824,c_1923,c_2188,c_2241,c_2310,c_2970,c_2980,c_3365,c_3611,c_8515,c_10769,c_13561,c_13562,c_13904,c_14944,c_15889,c_17312,c_17867,c_19713,c_34322,c_35126,c_49606,c_51895,c_56386,c_56690,c_56694,c_86124,c_87086,c_91280,c_102264,c_111014,c_111030,c_111031,c_111058,c_111078,c_111227,c_111228,c_111502,c_111947,c_113177,c_113400,c_134229,c_135300,c_158197,c_166370,c_167290,c_167440,c_167501,c_167497,c_167491]) ).
tcf(c_168570,plain,
inverse(iPr_def_19) = sk_c4,
inference(demodulation,[status(thm)],[c_36637,c_168536]) ).
tcf(c_168571,plain,
multiply(sk_c4,iPr_def_19) = identity,
inference(demodulation,[status(thm)],[c_36269,c_168536]) ).
tcf(c_168597,plain,
identity = iPr_def_25,
inference(light_normalisation,[status(thm)],[c_168571,c_167505]) ).
tcf(c_168606,plain,
inverse(multiply(sk_c4,sk_c9)) = sk_c11,
inference(demodulation,[status(thm)],[c_165907,c_168570]) ).
tcf(c_168675,plain,
multiply(sk_c7,iPr_def_17) = iPr_def_25,
inference(demodulation,[status(thm)],[c_45697,c_168597]) ).
tcf(c_168692,plain,
inverse(iPr_def_25) = iPr_def_25,
inference(demodulation,[status(thm)],[c_34322,c_168597]) ).
tcf(c_168693,plain,
! [X0: $i] : multiply(X0,iPr_def_25) = X0,
inference(demodulation,[status(thm)],[c_34290,c_168597]) ).
tcf(c_168712,plain,
multiply(iPr_def_22,sk_c5) = iPr_def_25,
inference(demodulation,[status(thm)],[c_1700,c_168597]) ).
tcf(c_168744,plain,
( ( iPr_def_14 = iPr_def_16 )
| ( sk_c10 = iPr_def_14 ) ),
inference(demodulation,[status(thm)],[c_106732,c_168693]) ).
tcf(c_169360,plain,
multiply(inverse(multiply(sk_c4,sk_c9)),iPr_def_25) = sk_c11,
inference(superposition,[status(thm)],[c_167505,c_146067]) ).
tcf(c_169362,plain,
multiply(sk_c11,iPr_def_25) = sk_c11,
inference(light_normalisation,[status(thm)],[c_169360,c_168606]) ).
tcf(c_169726,plain,
multiply(iPr_def_17,iPr_def_25) = iPr_def_17,
inference(superposition,[status(thm)],[c_168675,c_4595]) ).
tcf(c_170679,plain,
( ( iPr_def_14 = iPr_def_16 )
| ( sk_c11 = iPr_def_25 ) ),
inference(global_subsumption_just,[status(thm)],[c_10854,c_198,c_933,c_934,c_938,c_834,c_1830,c_1923,c_2241,c_2970,c_3611,c_8850,c_12949,c_13235,c_13561,c_13562,c_14788,c_14944,c_14945,c_15889,c_18836,c_20665,c_34322,c_35336,c_49602,c_56386,c_56690,c_56694,c_86124,c_87086,c_111014,c_111030,c_111031,c_111058,c_111078,c_111227,c_111228,c_111502,c_111947,c_113177,c_113400,c_134229,c_135300,c_158197,c_166370,c_168744]) ).
tcf(c_170681,plain,
sk_c11 = iPr_def_25,
inference(global_subsumption_just,[status(thm)],[c_170679,c_198,c_933,c_934,c_938,c_834,c_1824,c_1923,c_2188,c_2241,c_2310,c_2970,c_3365,c_3611,c_8850,c_13235,c_13561,c_13562,c_14788,c_14944,c_15889,c_17867,c_18836,c_20665,c_34322,c_35336,c_49602,c_56386,c_56690,c_56694,c_86124,c_87086,c_111014,c_111030,c_111031,c_111058,c_111078,c_111227,c_111228,c_111502,c_111947,c_113177,c_113400,c_134229,c_135300,c_158197,c_166370,c_170679]) ).
tcf(c_170698,plain,
( ( iPr_def_22 = iPr_def_25 )
| ( sk_c10 = iPr_def_14 ) ),
inference(demodulation,[status(thm)],[c_10039,c_170681]) ).
tcf(c_170716,plain,
( iPr_def_13
| ( iPr_def_22 = iPr_def_25 ) ),
inference(demodulation,[status(thm)],[c_35342,c_170681]) ).
tcf(c_170804,plain,
( ( iPr_def_22 = iPr_def_25 )
| ( sk_c10 = iPr_def_28 ) ),
inference(demodulation,[status(thm)],[c_904,c_170681]) ).
tcf(c_170820,plain,
multiply(sk_c5,iPr_def_25) = iPr_def_23,
inference(demodulation,[status(thm)],[c_843,c_170681]) ).
tcf(c_170821,plain,
multiply(sk_c9,iPr_def_25) = iPr_def_19,
inference(demodulation,[status(thm)],[c_839,c_170681]) ).
tcf(c_171119,plain,
multiply(inverse(iPr_def_22),iPr_def_25) = sk_c5,
inference(superposition,[status(thm)],[c_168712,c_32249]) ).
tcf(c_171122,plain,
sk_c5 = iPr_def_23,
inference(light_normalisation,[status(thm)],[c_171119,c_36978,c_170820]) ).
tcf(c_171133,plain,
inverse(iPr_def_22) = iPr_def_23,
inference(demodulation,[status(thm)],[c_36978,c_171122]) ).
tcf(c_171134,plain,
inverse(iPr_def_23) = iPr_def_22,
inference(demodulation,[status(thm)],[c_842,c_171122]) ).
tcf(c_171231,plain,
iPr_def_22 = iPr_def_25,
inference(global_subsumption_just,[status(thm)],[c_170716,c_198,c_933,c_934,c_938,c_834,c_1593,c_1824,c_1870,c_1923,c_2188,c_2241,c_2310,c_2970,c_2980,c_3365,c_3611,c_5430,c_15889,c_17867,c_34322,c_51514,c_56690,c_56694,c_91924,c_111014,c_111030,c_111031,c_111058,c_111078,c_111227,c_111228,c_111502,c_111947,c_113177,c_113400,c_134229,c_135300,c_158197,c_166370,c_170716,c_170804,c_170698]) ).
tcf(c_171235,plain,
sk_c11 = iPr_def_22,
inference(demodulation,[status(thm)],[c_170681,c_171231]) ).
tcf(c_171240,plain,
! [X0: $i] : multiply(X0,iPr_def_22) = X0,
inference(demodulation,[status(thm)],[c_168693,c_171231]) ).
tcf(c_171252,plain,
inverse(iPr_def_22) = iPr_def_22,
inference(demodulation,[status(thm)],[c_168692,c_171231]) ).
tcf(c_171254,plain,
identity = iPr_def_22,
inference(demodulation,[status(thm)],[c_168597,c_171231]) ).
tcf(c_171636,plain,
identity = iPr_def_21,
inference(global_subsumption_just,[status(thm)],[c_167284,c_198,c_933,c_934,c_938,c_834,c_1830,c_1923,c_2241,c_2970,c_2980,c_2981,c_3611,c_12949,c_15889,c_34322,c_39183,c_39181,c_42606,c_46912,c_49599,c_56690,c_56694,c_63263,c_111014,c_111030,c_111031,c_111058,c_111078,c_111227,c_111228,c_111502,c_111947,c_113177,c_113400,c_134229,c_135300,c_158197,c_166370]) ).
tcf(c_171638,plain,
identity = iPr_def_19,
inference(light_normalisation,[status(thm)],[c_171636,c_167955,c_171254]) ).
tcf(c_171639,plain,
iPr_def_19 = iPr_def_22,
inference(demodulation,[status(thm)],[c_171254,c_171638]) ).
tcf(c_171646,plain,
sk_c11 = iPr_def_19,
inference(demodulation,[status(thm)],[c_171235,c_171639]) ).
tcf(c_171647,plain,
iPr_def_19 = iPr_def_25,
inference(demodulation,[status(thm)],[c_171231,c_171639]) ).
tcf(c_171650,plain,
( iPr_def_13
| iPr_def_12
| ( iPr_def_14 != iPr_def_19 ) ),
inference(demodulation,[status(thm)],[c_35356,c_171639]) ).
tcf(c_171743,plain,
iPr_def_19 = iPr_def_23,
inference(light_normalisation,[status(thm)],[c_171133,c_171252,c_171639]) ).
tcf(c_172017,plain,
sk_c4 = iPr_def_19,
inference(light_normalisation,[status(thm)],[c_171134,c_168570,c_171639,c_171743]) ).
tcf(c_172018,plain,
inverse(iPr_def_19) = iPr_def_19,
inference(demodulation,[status(thm)],[c_168570,c_172017]) ).
tcf(c_172232,plain,
iPr_def_17 = iPr_def_20,
inference(global_subsumption_just,[status(thm)],[c_167467,c_198,c_933,c_934,c_938,c_834,c_1685,c_1824,c_1830,c_1923,c_2188,c_2241,c_2310,c_2675,c_2970,c_3365,c_3611,c_8513,c_8514,c_9526,c_10769,c_12949,c_13561,c_13562,c_13904,c_14944,c_15889,c_17312,c_17867,c_19713,c_25751,c_34322,c_35126,c_49606,c_49600,c_56386,c_56690,c_56694,c_86124,c_87086,c_111014,c_111030,c_111031,c_111058,c_111078,c_111227,c_111228,c_111502,c_111947,c_113177,c_113400,c_134229,c_135300,c_158197,c_166370,c_171646]) ).
tcf(c_172238,plain,
multiply(iPr_def_17,iPr_def_19) = sk_c9,
inference(demodulation,[status(thm)],[c_168193,c_172232]) ).
tcf(c_172252,plain,
inverse(iPr_def_17) = sk_c6,
inference(demodulation,[status(thm)],[c_40812,c_172232]) ).
tcf(c_172273,plain,
sk_c6 = sk_c7,
inference(light_normalisation,[status(thm)],[c_172252,c_46198]) ).
tcf(c_172342,plain,
! [X0: $i] : multiply(iPr_def_19,multiply(iPr_def_19,X0)) = X0,
inference(superposition,[status(thm)],[c_172018,c_32249]) ).
tcf(c_172414,plain,
multiply(iPr_def_19,iPr_def_19) = iPr_def_19,
inference(light_normalisation,[status(thm)],[c_169362,c_171646,c_171647]) ).
tcf(c_172417,plain,
! [X0: $i] : multiply(iPr_def_19,multiply(iPr_def_19,X0)) = multiply(iPr_def_19,X0),
inference(superposition,[status(thm)],[c_172414,c_125]) ).
tcf(c_172420,plain,
! [X0: $i] : multiply(iPr_def_19,X0) = X0,
inference(light_normalisation,[status(thm)],[c_172417,c_172342]) ).
tcf(c_172475,plain,
sk_c9 = iPr_def_17,
inference(light_normalisation,[status(thm)],[c_169726,c_171647,c_172238]) ).
tcf(c_172477,plain,
multiply(iPr_def_17,iPr_def_19) = iPr_def_17,
inference(demodulation,[status(thm)],[c_172238,c_172475]) ).
tcf(c_172592,plain,
( ( sk_c10 = iPr_def_23 )
| ~ iPr_def_12 ),
inference(global_subsumption_just,[status(thm)],[c_34639,c_5106,c_13257,c_13421]) ).
tcf(c_172594,plain,
( ( sk_c10 = iPr_def_19 )
| ~ iPr_def_12 ),
inference(light_normalisation,[status(thm)],[c_172592,c_171743]) ).
tcf(c_172613,plain,
multiply(sk_c7,iPr_def_19) = multiply(iPr_def_19,iPr_def_19),
inference(light_normalisation,[status(thm)],[c_168174,c_171646,c_172273]) ).
tcf(c_172614,plain,
multiply(sk_c7,iPr_def_19) = iPr_def_19,
inference(demodulation,[status(thm)],[c_172613,c_172420]) ).
tcf(c_172625,plain,
! [X0: $i] : multiply(sk_c7,multiply(iPr_def_19,X0)) = multiply(iPr_def_19,X0),
inference(superposition,[status(thm)],[c_172614,c_125]) ).
tcf(c_172630,plain,
! [X0: $i] : multiply(sk_c7,X0) = X0,
inference(light_normalisation,[status(thm)],[c_172625,c_172420]) ).
tcf(c_172632,plain,
! [X0: $i] : multiply(iPr_def_17,X0) = X0,
inference(demodulation,[status(thm)],[c_45700,c_172630]) ).
tcf(c_172689,plain,
( ~ iPr_def_12
| ( sk_c10 != iPr_def_19 )
| ( multiply(iPr_def_19,sk_c10) != iPr_def_19 ) ),
inference(light_normalisation,[status(thm)],[c_36271,c_167220,c_168536,c_172017,c_172018]) ).
tcf(c_172690,plain,
( ~ iPr_def_12
| ( sk_c10 != iPr_def_19 ) ),
inference(demodulation,[status(thm)],[c_172689,c_172420]) ).
tcf(c_172693,plain,
~ iPr_def_12,
inference(forward_subsumption_resolution,[status(thm)],[c_172690,c_172594]) ).
tcf(c_172733,plain,
iPr_def_17 = iPr_def_19,
inference(light_normalisation,[status(thm)],[c_170821,c_171647,c_172475,c_172477]) ).
tcf(c_172749,plain,
iPr_def_17 = iPr_def_23,
inference(demodulation,[status(thm)],[c_171743,c_172733]) ).
tcf(c_172751,plain,
sk_c11 = iPr_def_17,
inference(demodulation,[status(thm)],[c_171646,c_172733]) ).
tcf(c_172752,plain,
iPr_def_17 = iPr_def_22,
inference(demodulation,[status(thm)],[c_171639,c_172733]) ).
tcf(c_172753,plain,
identity = iPr_def_17,
inference(demodulation,[status(thm)],[c_171638,c_172733]) ).
tcf(c_172757,plain,
multiply(sk_c10,iPr_def_17) = iPr_def_14,
inference(demodulation,[status(thm)],[c_167513,c_172733]) ).
tcf(c_172987,plain,
! [X0: $i] : multiply(X0,iPr_def_17) = X0,
inference(light_normalisation,[status(thm)],[c_171240,c_172752]) ).
tcf(c_172996,plain,
multiply(sk_c10,iPr_def_17) = multiply(iPr_def_16,iPr_def_26),
inference(superposition,[status(thm)],[c_172987,c_9390]) ).
tcf(c_172998,plain,
sk_c10 = iPr_def_14,
inference(light_normalisation,[status(thm)],[c_172996,c_9387,c_172757]) ).
tcf(c_173422,plain,
( iPr_def_13
| iPr_def_12
| ( iPr_def_14 != iPr_def_17 ) ),
inference(light_normalisation,[status(thm)],[c_171650,c_172733]) ).
tcf(c_173423,plain,
( iPr_def_13
| ( iPr_def_14 != iPr_def_17 ) ),
inference(forward_subsumption_resolution,[status(thm)],[c_173422,c_172693]) ).
tcf(c_173861,plain,
( ( iPr_def_14 = iPr_def_17 )
| ( multiply(iPr_def_17,iPr_def_17) = iPr_def_14 ) ),
inference(light_normalisation,[status(thm)],[c_167414,c_172733,c_172749,c_172751]) ).
tcf(c_173862,plain,
iPr_def_14 = iPr_def_17,
inference(demodulation,[status(thm)],[c_173861,c_172632]) ).
tcf(c_173866,plain,
( iPr_def_13
| ( iPr_def_14 != iPr_def_14 ) ),
inference(demodulation,[status(thm)],[c_173423,c_173862]) ).
tcf(c_173884,plain,
identity = iPr_def_14,
inference(demodulation,[status(thm)],[c_172753,c_173862]) ).
tcf(c_173886,plain,
sk_c11 = iPr_def_14,
inference(demodulation,[status(thm)],[c_172751,c_173862]) ).
tcf(c_173894,plain,
iPr_def_13,
inference(equality_resolution_simp,[status(thm)],[c_173866]) ).
tcf(c_173908,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_173884,c_173886,c_173894,c_172998,c_171646,c_167220,c_166370,c_158197,c_135300,c_134229,c_113400,c_113177,c_111947,c_111502,c_111228,c_111227,c_111078,c_111058,c_111031,c_111030,c_111014,c_34322,c_15889,c_15808,c_12949,c_8514,c_8513,c_3611,c_2970,c_2241,c_1923,c_1830,c_834,c_938,c_934,c_933,c_198]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GRP258-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.08/0.35 % Computer : n009.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Wed Sep 23 14:17:28 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.08/0.35 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.12/0.39 Running first-order theorem proving
% 0.12/0.39 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.12/0.40
% 0.12/0.40 % ======== iProver multi-core TPTP/SMT =========
% 0.12/0.40
% 0.12/0.40 % Detected problem language: tptp
% 0.12/0.41 % Proving...
% 29.46/4.80 % SZS status Started for theBenchmark.p
% 29.46/4.80 % SZS status Unsatisfiable for theBenchmark.p
% 29.46/4.80
% 29.46/4.80 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 29.46/4.80
% 29.46/4.80 % ------ iProver source info
% 29.46/4.80
% 29.46/4.80 % git: date: 2026-07-19 20:42:38 +0200
% 29.46/4.80 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 29.46/4.80 % git: non_committed_changes: false
% 29.46/4.80
% 29.46/4.80 % ------ Parsing...% successful
% 29.46/4.80
% 29.46/4.80
% 29.46/4.80 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 29.46/4.80
% 29.46/4.80 % ------ Preprocessing... sup_sim: 0 sf_s rm: 0 0s sf_e pe_s pe_e %
% 29.46/4.80
% 29.46/4.80 % ------ Preprocessing... gs_s sp: 6 0s gs_e snvd_s sp: 0 0s snvd_e %
% 29.46/4.80
% 29.46/4.80 % ------ Preprocessing... sf_s rm: 0 0s sf_e
% 29.46/4.80 % ------ Proving...
% 29.46/4.80 % ------ Problem Properties
% 29.46/4.80
% 29.46/4.80 %
% 29.46/4.80 % clauses 95
% 29.46/4.80 % conjectures 75
% 29.46/4.80 % EPR 71
% 29.46/4.80 % Horn 24
% 29.46/4.80 % unary 20
% 29.46/4.80 % binary 70
% 29.46/4.80 % lits 179
% 29.46/4.80 % lits eq 171
% 29.46/4.80 % fd_pure 0
% 29.46/4.80 % fd_pseudo 0
% 29.46/4.80 % fd_cond 0
% 29.46/4.80 % fd_pseudo_cond 0
% 29.46/4.80 % AC symbols 0
% 29.46/4.80
% 29.46/4.80 % ------ Schedule dynamic 5 is on
% 29.46/4.80
% 29.46/4.80 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 29.46/4.80
% 29.46/4.80
% 29.46/4.80 % ------
% 29.46/4.80 % Current options:
% 29.46/4.80 % ------
% 29.46/4.80
% 29.46/4.80
% 29.46/4.80 %
% 29.46/4.80
% 29.46/4.80 % ------ Proving...
% 29.46/4.80 %
% 29.46/4.80
% 29.46/4.80 % SZS status Unsatisfiable for theBenchmark.p
% 29.46/4.80
% 29.46/4.80 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 29.46/4.82
% 29.46/4.82
%------------------------------------------------------------------------------