%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : GRP208-1 : TPTP v9.3.1. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% Computer : n014.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 01:31:48 PM UTC 2026
% Result : Unsatisfiable 17.74s 5.41s
% Output : CNFRefutation 17.74s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 65
% Syntax : Number of formulae : 584 ( 98 unt; 15 def)
% Number of atoms : 2123 (1305 equ)
% Maximal formula atoms : 16 ( 3 avg)
% Number of connectives : 1290 ( 513 ~; 777 |; 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 : 22 ( 20 usr; 21 prp; 0-2 aty)
% Number of functors : 15 ( 15 usr; 13 con; 0-2 aty)
% Number of variables : 236 ( 0 sgn 236 !; 0 ?; 180 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0] : multiply(identity,X0) = X0,
file('/export/starexec/sandbox2/benchmark/Axioms/GRP004-0.ax',left_identity) ).
fof(f2,axiom,
! [X0] : multiply(inverse(X0),X0) = identity,
file('/export/starexec/sandbox2/benchmark/Axioms/GRP004-0.ax',left_inverse) ).
fof(f3,plain,
! [X0] : identity = multiply(inverse(X0),X0),
inference(reorient_equations,[],[f2]) ).
fof(f4,axiom,
! [X2,X0,X1] : multiply(multiply(X0,X1),X2) = multiply(X0,multiply(X1,X2)),
file('/export/starexec/sandbox2/benchmark/Axioms/GRP004-0.ax',associativity) ).
fof(f5,negated_conjecture,
( multiply(sk_c5,sk_c6) = sk_c12
| multiply(sk_c1,sk_c2) = sk_c12 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_1) ).
fof(f6,plain,
( sk_c12 = multiply(sk_c5,sk_c6)
| multiply(sk_c1,sk_c2) = sk_c12 ),
inference(reorient_equations,[],[f5]) ).
fof(f7,negated_conjecture,
( inverse(sk_c5) = sk_c6
| multiply(sk_c1,sk_c2) = sk_c12 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_2) ).
fof(f8,plain,
( sk_c6 = inverse(sk_c5)
| multiply(sk_c1,sk_c2) = sk_c12 ),
inference(reorient_equations,[],[f7]) ).
fof(f11,negated_conjecture,
( inverse(sk_c7) = sk_c12
| multiply(sk_c1,sk_c2) = sk_c12 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_4) ).
fof(f12,plain,
( sk_c12 = inverse(sk_c7)
| multiply(sk_c1,sk_c2) = sk_c12 ),
inference(reorient_equations,[],[f11]) ).
fof(f13,negated_conjecture,
( multiply(sk_c7,sk_c11) = sk_c12
| multiply(sk_c1,sk_c2) = sk_c12 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_5) ).
fof(f14,plain,
( sk_c12 = multiply(sk_c7,sk_c11)
| multiply(sk_c1,sk_c2) = sk_c12 ),
inference(reorient_equations,[],[f13]) ).
fof(f15,negated_conjecture,
( multiply(sk_c8,sk_c9) = sk_c11
| multiply(sk_c1,sk_c2) = sk_c12 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_6) ).
fof(f16,plain,
( sk_c11 = multiply(sk_c8,sk_c9)
| multiply(sk_c1,sk_c2) = sk_c12 ),
inference(reorient_equations,[],[f15]) ).
fof(f17,negated_conjecture,
( inverse(sk_c8) = sk_c9
| multiply(sk_c1,sk_c2) = sk_c12 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_7) ).
fof(f18,plain,
( sk_c9 = inverse(sk_c8)
| multiply(sk_c1,sk_c2) = sk_c12 ),
inference(reorient_equations,[],[f17]) ).
fof(f19,negated_conjecture,
( multiply(sk_c9,sk_c12) = sk_c11
| multiply(sk_c1,sk_c2) = sk_c12 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_8) ).
fof(f20,plain,
( sk_c11 = multiply(sk_c9,sk_c12)
| multiply(sk_c1,sk_c2) = sk_c12 ),
inference(reorient_equations,[],[f19]) ).
fof(f21,negated_conjecture,
( inverse(sk_c10) = sk_c11
| multiply(sk_c1,sk_c2) = sk_c12 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_9) ).
fof(f22,plain,
( sk_c11 = inverse(sk_c10)
| multiply(sk_c1,sk_c2) = sk_c12 ),
inference(reorient_equations,[],[f21]) ).
fof(f23,negated_conjecture,
( multiply(sk_c10,sk_c12) = sk_c11
| multiply(sk_c1,sk_c2) = sk_c12 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_10) ).
fof(f24,plain,
( sk_c11 = multiply(sk_c10,sk_c12)
| multiply(sk_c1,sk_c2) = sk_c12 ),
inference(reorient_equations,[],[f23]) ).
fof(f25,negated_conjecture,
( multiply(sk_c5,sk_c6) = sk_c12
| inverse(sk_c1) = sk_c2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_11) ).
fof(f26,plain,
( sk_c12 = multiply(sk_c5,sk_c6)
| sk_c2 = inverse(sk_c1) ),
inference(reorient_equations,[],[f25]) ).
fof(f27,negated_conjecture,
( inverse(sk_c5) = sk_c6
| inverse(sk_c1) = sk_c2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_12) ).
fof(f28,plain,
( sk_c6 = inverse(sk_c5)
| sk_c2 = inverse(sk_c1) ),
inference(reorient_equations,[],[f27]) ).
fof(f31,negated_conjecture,
( inverse(sk_c7) = sk_c12
| inverse(sk_c1) = sk_c2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_14) ).
fof(f32,plain,
( sk_c12 = inverse(sk_c7)
| sk_c2 = inverse(sk_c1) ),
inference(reorient_equations,[],[f31]) ).
fof(f33,negated_conjecture,
( multiply(sk_c7,sk_c11) = sk_c12
| inverse(sk_c1) = sk_c2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_15) ).
fof(f34,plain,
( sk_c12 = multiply(sk_c7,sk_c11)
| sk_c2 = inverse(sk_c1) ),
inference(reorient_equations,[],[f33]) ).
fof(f45,negated_conjecture,
( multiply(sk_c5,sk_c6) = sk_c12
| multiply(sk_c2,sk_c11) = sk_c12 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_21) ).
fof(f46,plain,
( sk_c12 = multiply(sk_c5,sk_c6)
| sk_c12 = multiply(sk_c2,sk_c11) ),
inference(reorient_equations,[],[f45]) ).
fof(f51,negated_conjecture,
( inverse(sk_c7) = sk_c12
| multiply(sk_c2,sk_c11) = sk_c12 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_24) ).
fof(f52,plain,
( sk_c12 = inverse(sk_c7)
| sk_c12 = multiply(sk_c2,sk_c11) ),
inference(reorient_equations,[],[f51]) ).
fof(f53,negated_conjecture,
( multiply(sk_c7,sk_c11) = sk_c12
| multiply(sk_c2,sk_c11) = sk_c12 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_25) ).
fof(f54,plain,
( sk_c12 = multiply(sk_c7,sk_c11)
| sk_c12 = multiply(sk_c2,sk_c11) ),
inference(reorient_equations,[],[f53]) ).
fof(f55,negated_conjecture,
( multiply(sk_c8,sk_c9) = sk_c11
| multiply(sk_c2,sk_c11) = sk_c12 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_26) ).
fof(f56,plain,
( sk_c11 = multiply(sk_c8,sk_c9)
| sk_c12 = multiply(sk_c2,sk_c11) ),
inference(reorient_equations,[],[f55]) ).
fof(f57,negated_conjecture,
( inverse(sk_c8) = sk_c9
| multiply(sk_c2,sk_c11) = sk_c12 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_27) ).
fof(f58,plain,
( sk_c9 = inverse(sk_c8)
| sk_c12 = multiply(sk_c2,sk_c11) ),
inference(reorient_equations,[],[f57]) ).
fof(f61,negated_conjecture,
( inverse(sk_c10) = sk_c11
| multiply(sk_c2,sk_c11) = sk_c12 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_29) ).
fof(f62,plain,
( sk_c11 = inverse(sk_c10)
| sk_c12 = multiply(sk_c2,sk_c11) ),
inference(reorient_equations,[],[f61]) ).
fof(f63,negated_conjecture,
( multiply(sk_c10,sk_c12) = sk_c11
| multiply(sk_c2,sk_c11) = sk_c12 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_30) ).
fof(f64,plain,
( sk_c11 = multiply(sk_c10,sk_c12)
| sk_c12 = multiply(sk_c2,sk_c11) ),
inference(reorient_equations,[],[f63]) ).
fof(f65,negated_conjecture,
( multiply(sk_c5,sk_c6) = sk_c12
| multiply(sk_c12,sk_c4) = sk_c11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_31) ).
fof(f66,plain,
( sk_c12 = multiply(sk_c5,sk_c6)
| sk_c11 = multiply(sk_c12,sk_c4) ),
inference(reorient_equations,[],[f65]) ).
fof(f71,negated_conjecture,
( inverse(sk_c7) = sk_c12
| multiply(sk_c12,sk_c4) = sk_c11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_34) ).
fof(f72,plain,
( sk_c12 = inverse(sk_c7)
| sk_c11 = multiply(sk_c12,sk_c4) ),
inference(reorient_equations,[],[f71]) ).
fof(f73,negated_conjecture,
( multiply(sk_c7,sk_c11) = sk_c12
| multiply(sk_c12,sk_c4) = sk_c11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_35) ).
fof(f74,plain,
( sk_c12 = multiply(sk_c7,sk_c11)
| sk_c11 = multiply(sk_c12,sk_c4) ),
inference(reorient_equations,[],[f73]) ).
fof(f75,negated_conjecture,
( multiply(sk_c8,sk_c9) = sk_c11
| multiply(sk_c12,sk_c4) = sk_c11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_36) ).
fof(f76,plain,
( sk_c11 = multiply(sk_c8,sk_c9)
| sk_c11 = multiply(sk_c12,sk_c4) ),
inference(reorient_equations,[],[f75]) ).
fof(f77,negated_conjecture,
( inverse(sk_c8) = sk_c9
| multiply(sk_c12,sk_c4) = sk_c11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_37) ).
fof(f78,plain,
( sk_c9 = inverse(sk_c8)
| sk_c11 = multiply(sk_c12,sk_c4) ),
inference(reorient_equations,[],[f77]) ).
fof(f79,negated_conjecture,
( multiply(sk_c9,sk_c12) = sk_c11
| multiply(sk_c12,sk_c4) = sk_c11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_38) ).
fof(f80,plain,
( sk_c11 = multiply(sk_c9,sk_c12)
| sk_c11 = multiply(sk_c12,sk_c4) ),
inference(reorient_equations,[],[f79]) ).
fof(f81,negated_conjecture,
( inverse(sk_c10) = sk_c11
| multiply(sk_c12,sk_c4) = sk_c11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_39) ).
fof(f82,plain,
( sk_c11 = inverse(sk_c10)
| sk_c11 = multiply(sk_c12,sk_c4) ),
inference(reorient_equations,[],[f81]) ).
fof(f83,negated_conjecture,
( multiply(sk_c10,sk_c12) = sk_c11
| multiply(sk_c12,sk_c4) = sk_c11 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_40) ).
fof(f84,plain,
( sk_c11 = multiply(sk_c10,sk_c12)
| sk_c11 = multiply(sk_c12,sk_c4) ),
inference(reorient_equations,[],[f83]) ).
fof(f85,negated_conjecture,
( multiply(sk_c5,sk_c6) = sk_c12
| multiply(sk_c3,sk_c12) = sk_c4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_41) ).
fof(f86,plain,
( sk_c12 = multiply(sk_c5,sk_c6)
| sk_c4 = multiply(sk_c3,sk_c12) ),
inference(reorient_equations,[],[f85]) ).
fof(f87,negated_conjecture,
( inverse(sk_c5) = sk_c6
| multiply(sk_c3,sk_c12) = sk_c4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_42) ).
fof(f88,plain,
( sk_c6 = inverse(sk_c5)
| sk_c4 = multiply(sk_c3,sk_c12) ),
inference(reorient_equations,[],[f87]) ).
fof(f93,negated_conjecture,
( multiply(sk_c7,sk_c11) = sk_c12
| multiply(sk_c3,sk_c12) = sk_c4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_45) ).
fof(f94,plain,
( sk_c12 = multiply(sk_c7,sk_c11)
| sk_c4 = multiply(sk_c3,sk_c12) ),
inference(reorient_equations,[],[f93]) ).
fof(f95,negated_conjecture,
( multiply(sk_c8,sk_c9) = sk_c11
| multiply(sk_c3,sk_c12) = sk_c4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_46) ).
fof(f96,plain,
( sk_c11 = multiply(sk_c8,sk_c9)
| sk_c4 = multiply(sk_c3,sk_c12) ),
inference(reorient_equations,[],[f95]) ).
fof(f97,negated_conjecture,
( inverse(sk_c8) = sk_c9
| multiply(sk_c3,sk_c12) = sk_c4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_47) ).
fof(f98,plain,
( sk_c9 = inverse(sk_c8)
| sk_c4 = multiply(sk_c3,sk_c12) ),
inference(reorient_equations,[],[f97]) ).
fof(f101,negated_conjecture,
( inverse(sk_c10) = sk_c11
| multiply(sk_c3,sk_c12) = sk_c4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_49) ).
fof(f102,plain,
( sk_c11 = inverse(sk_c10)
| sk_c4 = multiply(sk_c3,sk_c12) ),
inference(reorient_equations,[],[f101]) ).
fof(f103,negated_conjecture,
( multiply(sk_c10,sk_c12) = sk_c11
| multiply(sk_c3,sk_c12) = sk_c4 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_50) ).
fof(f104,plain,
( sk_c11 = multiply(sk_c10,sk_c12)
| sk_c4 = multiply(sk_c3,sk_c12) ),
inference(reorient_equations,[],[f103]) ).
fof(f105,negated_conjecture,
( multiply(sk_c5,sk_c6) = sk_c12
| inverse(sk_c3) = sk_c12 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_51) ).
fof(f106,plain,
( sk_c12 = multiply(sk_c5,sk_c6)
| sk_c12 = inverse(sk_c3) ),
inference(reorient_equations,[],[f105]) ).
fof(f111,negated_conjecture,
( inverse(sk_c7) = sk_c12
| inverse(sk_c3) = sk_c12 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_54) ).
fof(f112,plain,
( sk_c12 = inverse(sk_c7)
| sk_c12 = inverse(sk_c3) ),
inference(reorient_equations,[],[f111]) ).
fof(f113,negated_conjecture,
( multiply(sk_c7,sk_c11) = sk_c12
| inverse(sk_c3) = sk_c12 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_55) ).
fof(f114,plain,
( sk_c12 = multiply(sk_c7,sk_c11)
| sk_c12 = inverse(sk_c3) ),
inference(reorient_equations,[],[f113]) ).
fof(f115,negated_conjecture,
( multiply(sk_c8,sk_c9) = sk_c11
| inverse(sk_c3) = sk_c12 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_56) ).
fof(f116,plain,
( sk_c11 = multiply(sk_c8,sk_c9)
| sk_c12 = inverse(sk_c3) ),
inference(reorient_equations,[],[f115]) ).
fof(f117,negated_conjecture,
( inverse(sk_c8) = sk_c9
| inverse(sk_c3) = sk_c12 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_57) ).
fof(f118,plain,
( sk_c9 = inverse(sk_c8)
| sk_c12 = inverse(sk_c3) ),
inference(reorient_equations,[],[f117]) ).
fof(f119,negated_conjecture,
( multiply(sk_c9,sk_c12) = sk_c11
| inverse(sk_c3) = sk_c12 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_58) ).
fof(f120,plain,
( sk_c11 = multiply(sk_c9,sk_c12)
| sk_c12 = inverse(sk_c3) ),
inference(reorient_equations,[],[f119]) ).
fof(f121,negated_conjecture,
( inverse(sk_c10) = sk_c11
| inverse(sk_c3) = sk_c12 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_59) ).
fof(f122,plain,
( sk_c11 = inverse(sk_c10)
| sk_c12 = inverse(sk_c3) ),
inference(reorient_equations,[],[f121]) ).
fof(f123,negated_conjecture,
( multiply(sk_c10,sk_c12) = sk_c11
| inverse(sk_c3) = sk_c12 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_60) ).
fof(f124,plain,
( sk_c11 = multiply(sk_c10,sk_c12)
| sk_c12 = inverse(sk_c3) ),
inference(reorient_equations,[],[f123]) ).
fof(f125,negated_conjecture,
! [X2,X3,X0,X1,X8,X6,X9,X7,X4,X5] :
( multiply(X9,sk_c12) != sk_c11
| inverse(X9) != sk_c11
| multiply(X8,sk_c12) != sk_c11
| inverse(X7) != X8
| multiply(X7,X8) != sk_c11
| multiply(X6,sk_c11) != sk_c12
| inverse(X6) != sk_c12
| multiply(X5,sk_c11) != sk_c12
| inverse(X4) != X5
| multiply(X4,X5) != sk_c12
| inverse(X3) != sk_c12
| multiply(X3,sk_c12) != X2
| multiply(sk_c12,X2) != sk_c11
| multiply(X1,sk_c11) != sk_c12
| inverse(X0) != X1
| multiply(X0,X1) != sk_c12 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_61) ).
fof(f126,plain,
! [X2,X3,X0,X1,X8,X6,X9,X7,X4,X5] :
( sk_c11 != multiply(X9,sk_c12)
| sk_c11 != inverse(X9)
| sk_c11 != multiply(X8,sk_c12)
| inverse(X7) != X8
| sk_c11 != multiply(X7,X8)
| sk_c12 != multiply(X6,sk_c11)
| sk_c12 != inverse(X6)
| sk_c12 != multiply(X5,sk_c11)
| inverse(X4) != X5
| sk_c12 != multiply(X4,X5)
| sk_c12 != inverse(X3)
| multiply(X3,sk_c12) != X2
| sk_c11 != multiply(sk_c12,X2)
| sk_c12 != multiply(X1,sk_c11)
| inverse(X0) != X1
| multiply(X0,X1) != sk_c12 ),
inference(reorient_equations,[],[f125]) ).
fof(f127,plain,
! [X2,X3,X0,X8,X6,X9,X7,X4,X5] :
( sk_c11 != multiply(X9,sk_c12)
| sk_c11 != inverse(X9)
| sk_c11 != multiply(X8,sk_c12)
| inverse(X7) != X8
| sk_c11 != multiply(X7,X8)
| sk_c12 != multiply(X6,sk_c11)
| sk_c12 != inverse(X6)
| sk_c12 != multiply(X5,sk_c11)
| inverse(X4) != X5
| sk_c12 != multiply(X4,X5)
| sk_c12 != inverse(X3)
| multiply(X3,sk_c12) != X2
| sk_c11 != multiply(sk_c12,X2)
| sk_c12 != multiply(inverse(X0),sk_c11)
| sk_c12 != multiply(X0,inverse(X0)) ),
inference(equality_resolution,[],[f126]) ).
fof(f128,plain,
! [X3,X0,X8,X6,X9,X7,X4,X5] :
( sk_c11 != multiply(X9,sk_c12)
| sk_c11 != inverse(X9)
| sk_c11 != multiply(X8,sk_c12)
| inverse(X7) != X8
| sk_c11 != multiply(X7,X8)
| sk_c12 != multiply(X6,sk_c11)
| sk_c12 != inverse(X6)
| sk_c12 != multiply(X5,sk_c11)
| inverse(X4) != X5
| sk_c12 != multiply(X4,X5)
| sk_c12 != inverse(X3)
| sk_c11 != multiply(sk_c12,multiply(X3,sk_c12))
| sk_c12 != multiply(inverse(X0),sk_c11)
| sk_c12 != multiply(X0,inverse(X0)) ),
inference(equality_resolution,[],[f127]) ).
fof(f129,plain,
! [X3,X0,X8,X6,X9,X7,X4] :
( sk_c11 != multiply(X9,sk_c12)
| sk_c11 != inverse(X9)
| sk_c11 != multiply(X8,sk_c12)
| inverse(X7) != X8
| sk_c11 != multiply(X7,X8)
| sk_c12 != multiply(X6,sk_c11)
| sk_c12 != inverse(X6)
| sk_c12 != multiply(inverse(X4),sk_c11)
| sk_c12 != multiply(X4,inverse(X4))
| sk_c12 != inverse(X3)
| sk_c11 != multiply(sk_c12,multiply(X3,sk_c12))
| sk_c12 != multiply(inverse(X0),sk_c11)
| sk_c12 != multiply(X0,inverse(X0)) ),
inference(equality_resolution,[],[f128]) ).
fof(f130,plain,
! [X3,X0,X6,X9,X7,X4] :
( sk_c11 != multiply(X9,sk_c12)
| sk_c11 != inverse(X9)
| sk_c11 != multiply(inverse(X7),sk_c12)
| sk_c11 != multiply(X7,inverse(X7))
| sk_c12 != multiply(X6,sk_c11)
| sk_c12 != inverse(X6)
| sk_c12 != multiply(inverse(X4),sk_c11)
| sk_c12 != multiply(X4,inverse(X4))
| sk_c12 != inverse(X3)
| sk_c11 != multiply(sk_c12,multiply(X3,sk_c12))
| sk_c12 != multiply(inverse(X0),sk_c11)
| sk_c12 != multiply(X0,inverse(X0)) ),
inference(equality_resolution,[],[f129]) ).
tcf(c_113,plain,
! [X0: $i] : multiply(identity,X0) = X0,
inference(cnf_transformation,[],[f1]) ).
tcf(c_114,plain,
! [X0: $i] : multiply(inverse(X0),X0) = identity,
inference(cnf_transformation,[],[f3]) ).
tcf(c_115,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(multiply(X0,X1),X2) = multiply(X0,multiply(X1,X2)),
inference(cnf_transformation,[],[f4]) ).
tcf(c_116,negated_conjecture,
( ( multiply(sk_c5,sk_c6) = sk_c12 )
| ( multiply(sk_c1,sk_c2) = sk_c12 ) ),
inference(cnf_transformation,[],[f6]) ).
tcf(c_117,negated_conjecture,
( ( inverse(sk_c5) = sk_c6 )
| ( multiply(sk_c1,sk_c2) = sk_c12 ) ),
inference(cnf_transformation,[],[f8]) ).
tcf(c_119,negated_conjecture,
( ( inverse(sk_c7) = sk_c12 )
| ( multiply(sk_c1,sk_c2) = sk_c12 ) ),
inference(cnf_transformation,[],[f12]) ).
tcf(c_120,negated_conjecture,
( ( multiply(sk_c7,sk_c11) = sk_c12 )
| ( multiply(sk_c1,sk_c2) = sk_c12 ) ),
inference(cnf_transformation,[],[f14]) ).
tcf(c_121,negated_conjecture,
( ( multiply(sk_c8,sk_c9) = sk_c11 )
| ( multiply(sk_c1,sk_c2) = sk_c12 ) ),
inference(cnf_transformation,[],[f16]) ).
tcf(c_122,negated_conjecture,
( ( inverse(sk_c8) = sk_c9 )
| ( multiply(sk_c1,sk_c2) = sk_c12 ) ),
inference(cnf_transformation,[],[f18]) ).
tcf(c_123,negated_conjecture,
( ( multiply(sk_c9,sk_c12) = sk_c11 )
| ( multiply(sk_c1,sk_c2) = sk_c12 ) ),
inference(cnf_transformation,[],[f20]) ).
tcf(c_124,negated_conjecture,
( ( inverse(sk_c10) = sk_c11 )
| ( multiply(sk_c1,sk_c2) = sk_c12 ) ),
inference(cnf_transformation,[],[f22]) ).
tcf(c_125,negated_conjecture,
( ( multiply(sk_c10,sk_c12) = sk_c11 )
| ( multiply(sk_c1,sk_c2) = sk_c12 ) ),
inference(cnf_transformation,[],[f24]) ).
tcf(c_126,negated_conjecture,
( ( inverse(sk_c1) = sk_c2 )
| ( multiply(sk_c5,sk_c6) = sk_c12 ) ),
inference(cnf_transformation,[],[f26]) ).
tcf(c_127,negated_conjecture,
( ( inverse(sk_c5) = sk_c6 )
| ( inverse(sk_c1) = sk_c2 ) ),
inference(cnf_transformation,[],[f28]) ).
tcf(c_129,negated_conjecture,
( ( inverse(sk_c7) = sk_c12 )
| ( inverse(sk_c1) = sk_c2 ) ),
inference(cnf_transformation,[],[f32]) ).
tcf(c_130,negated_conjecture,
( ( inverse(sk_c1) = sk_c2 )
| ( multiply(sk_c7,sk_c11) = sk_c12 ) ),
inference(cnf_transformation,[],[f34]) ).
tcf(c_136,negated_conjecture,
( ( multiply(sk_c5,sk_c6) = sk_c12 )
| ( multiply(sk_c2,sk_c11) = sk_c12 ) ),
inference(cnf_transformation,[],[f46]) ).
tcf(c_139,negated_conjecture,
( ( inverse(sk_c7) = sk_c12 )
| ( multiply(sk_c2,sk_c11) = sk_c12 ) ),
inference(cnf_transformation,[],[f52]) ).
tcf(c_140,negated_conjecture,
( ( multiply(sk_c7,sk_c11) = sk_c12 )
| ( multiply(sk_c2,sk_c11) = sk_c12 ) ),
inference(cnf_transformation,[],[f54]) ).
tcf(c_141,negated_conjecture,
( ( multiply(sk_c8,sk_c9) = sk_c11 )
| ( multiply(sk_c2,sk_c11) = sk_c12 ) ),
inference(cnf_transformation,[],[f56]) ).
tcf(c_142,negated_conjecture,
( ( inverse(sk_c8) = sk_c9 )
| ( multiply(sk_c2,sk_c11) = sk_c12 ) ),
inference(cnf_transformation,[],[f58]) ).
tcf(c_144,negated_conjecture,
( ( inverse(sk_c10) = sk_c11 )
| ( multiply(sk_c2,sk_c11) = sk_c12 ) ),
inference(cnf_transformation,[],[f62]) ).
tcf(c_145,negated_conjecture,
( ( multiply(sk_c10,sk_c12) = sk_c11 )
| ( multiply(sk_c2,sk_c11) = sk_c12 ) ),
inference(cnf_transformation,[],[f64]) ).
tcf(c_146,negated_conjecture,
( ( multiply(sk_c5,sk_c6) = sk_c12 )
| ( multiply(sk_c12,sk_c4) = sk_c11 ) ),
inference(cnf_transformation,[],[f66]) ).
tcf(c_149,negated_conjecture,
( ( inverse(sk_c7) = sk_c12 )
| ( multiply(sk_c12,sk_c4) = sk_c11 ) ),
inference(cnf_transformation,[],[f72]) ).
tcf(c_150,negated_conjecture,
( ( multiply(sk_c7,sk_c11) = sk_c12 )
| ( multiply(sk_c12,sk_c4) = sk_c11 ) ),
inference(cnf_transformation,[],[f74]) ).
tcf(c_151,negated_conjecture,
( ( multiply(sk_c8,sk_c9) = sk_c11 )
| ( multiply(sk_c12,sk_c4) = sk_c11 ) ),
inference(cnf_transformation,[],[f76]) ).
tcf(c_152,negated_conjecture,
( ( inverse(sk_c8) = sk_c9 )
| ( multiply(sk_c12,sk_c4) = sk_c11 ) ),
inference(cnf_transformation,[],[f78]) ).
tcf(c_153,negated_conjecture,
( ( multiply(sk_c9,sk_c12) = sk_c11 )
| ( multiply(sk_c12,sk_c4) = sk_c11 ) ),
inference(cnf_transformation,[],[f80]) ).
tcf(c_154,negated_conjecture,
( ( inverse(sk_c10) = sk_c11 )
| ( multiply(sk_c12,sk_c4) = sk_c11 ) ),
inference(cnf_transformation,[],[f82]) ).
tcf(c_155,negated_conjecture,
( ( multiply(sk_c10,sk_c12) = sk_c11 )
| ( multiply(sk_c12,sk_c4) = sk_c11 ) ),
inference(cnf_transformation,[],[f84]) ).
tcf(c_156,negated_conjecture,
( ( multiply(sk_c3,sk_c12) = sk_c4 )
| ( multiply(sk_c5,sk_c6) = sk_c12 ) ),
inference(cnf_transformation,[],[f86]) ).
tcf(c_157,negated_conjecture,
( ( inverse(sk_c5) = sk_c6 )
| ( multiply(sk_c3,sk_c12) = sk_c4 ) ),
inference(cnf_transformation,[],[f88]) ).
tcf(c_160,negated_conjecture,
( ( multiply(sk_c3,sk_c12) = sk_c4 )
| ( multiply(sk_c7,sk_c11) = sk_c12 ) ),
inference(cnf_transformation,[],[f94]) ).
tcf(c_161,negated_conjecture,
( ( multiply(sk_c3,sk_c12) = sk_c4 )
| ( multiply(sk_c8,sk_c9) = sk_c11 ) ),
inference(cnf_transformation,[],[f96]) ).
tcf(c_162,negated_conjecture,
( ( inverse(sk_c8) = sk_c9 )
| ( multiply(sk_c3,sk_c12) = sk_c4 ) ),
inference(cnf_transformation,[],[f98]) ).
tcf(c_164,negated_conjecture,
( ( inverse(sk_c10) = sk_c11 )
| ( multiply(sk_c3,sk_c12) = sk_c4 ) ),
inference(cnf_transformation,[],[f102]) ).
tcf(c_165,negated_conjecture,
( ( multiply(sk_c3,sk_c12) = sk_c4 )
| ( multiply(sk_c10,sk_c12) = sk_c11 ) ),
inference(cnf_transformation,[],[f104]) ).
tcf(c_166,negated_conjecture,
( ( inverse(sk_c3) = sk_c12 )
| ( multiply(sk_c5,sk_c6) = sk_c12 ) ),
inference(cnf_transformation,[],[f106]) ).
tcf(c_169,negated_conjecture,
( ( inverse(sk_c3) = sk_c12 )
| ( inverse(sk_c7) = sk_c12 ) ),
inference(cnf_transformation,[],[f112]) ).
tcf(c_170,negated_conjecture,
( ( inverse(sk_c3) = sk_c12 )
| ( multiply(sk_c7,sk_c11) = sk_c12 ) ),
inference(cnf_transformation,[],[f114]) ).
tcf(c_171,negated_conjecture,
( ( inverse(sk_c3) = sk_c12 )
| ( multiply(sk_c8,sk_c9) = sk_c11 ) ),
inference(cnf_transformation,[],[f116]) ).
tcf(c_172,negated_conjecture,
( ( inverse(sk_c3) = sk_c12 )
| ( inverse(sk_c8) = sk_c9 ) ),
inference(cnf_transformation,[],[f118]) ).
tcf(c_173,negated_conjecture,
( ( inverse(sk_c3) = sk_c12 )
| ( multiply(sk_c9,sk_c12) = sk_c11 ) ),
inference(cnf_transformation,[],[f120]) ).
tcf(c_174,negated_conjecture,
( ( inverse(sk_c3) = sk_c12 )
| ( inverse(sk_c10) = sk_c11 ) ),
inference(cnf_transformation,[],[f122]) ).
tcf(c_175,negated_conjecture,
( ( inverse(sk_c3) = sk_c12 )
| ( multiply(sk_c10,sk_c12) = sk_c11 ) ),
inference(cnf_transformation,[],[f124]) ).
tcf(c_176,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( ( inverse(X5) != sk_c11 )
| ( inverse(X3) != sk_c12 )
| ( inverse(X2) != sk_c12 )
| ( multiply(X5,sk_c12) != sk_c11 )
| ( multiply(X2,sk_c11) != sk_c12 )
| ( multiply(inverse(X4),sk_c12) != sk_c11 )
| ( multiply(inverse(X1),sk_c11) != sk_c12 )
| ( multiply(inverse(X0),sk_c11) != sk_c12 )
| ( multiply(X4,inverse(X4)) != sk_c11 )
| ( multiply(X1,inverse(X1)) != sk_c12 )
| ( multiply(X0,inverse(X0)) != sk_c12 )
| ( multiply(sk_c12,multiply(X3,sk_c12)) != sk_c11 ) ),
inference(cnf_transformation,[],[f130]) ).
tcf(c_717,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_10
| ( multiply(inverse(X0),sk_c12) != sk_c11 )
| ( multiply(X0,inverse(X0)) != sk_c11 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_10])],[c_176]) ).
tcf(c_718,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_11
| ( multiply(inverse(X0),sk_c11) != sk_c12 )
| ( multiply(X0,inverse(X0)) != sk_c12 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_11])],[c_176]) ).
tcf(c_719,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_12
| ( inverse(X0) != sk_c12 )
| ( multiply(X0,sk_c11) != sk_c12 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_12])],[c_176]) ).
tcf(c_720,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_13
| ( inverse(X0) != sk_c11 )
| ( multiply(X0,sk_c12) != sk_c11 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_13])],[c_176]) ).
tcf(c_721,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_14
| ( inverse(X0) != sk_c12 )
| ( multiply(sk_c12,multiply(X0,sk_c12)) != sk_c11 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_14])],[c_176]) ).
tcf(c_722,negated_conjecture,
( iPr_def_14
| iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_176]) ).
tcf(c_723,definition,
iPr_def_15 = multiply(sk_c10,sk_c12),
introduced(definition,[new_symbols(definition,[iPr_def_15])],[]) ).
tcf(c_724,definition,
iPr_def_16 = inverse(sk_c3),
introduced(definition,[new_symbols(definition,[iPr_def_16])],[]) ).
tcf(c_725,definition,
iPr_def_17 = inverse(sk_c10),
introduced(definition,[new_symbols(definition,[iPr_def_17])],[]) ).
tcf(c_726,definition,
iPr_def_18 = multiply(sk_c9,sk_c12),
introduced(definition,[new_symbols(definition,[iPr_def_18])],[]) ).
tcf(c_727,definition,
iPr_def_19 = inverse(sk_c8),
introduced(definition,[new_symbols(definition,[iPr_def_19])],[]) ).
tcf(c_728,definition,
iPr_def_20 = multiply(sk_c8,sk_c9),
introduced(definition,[new_symbols(definition,[iPr_def_20])],[]) ).
tcf(c_729,definition,
iPr_def_21 = multiply(sk_c7,sk_c11),
introduced(definition,[new_symbols(definition,[iPr_def_21])],[]) ).
tcf(c_730,definition,
iPr_def_22 = inverse(sk_c7),
introduced(definition,[new_symbols(definition,[iPr_def_22])],[]) ).
tcf(c_732,definition,
iPr_def_24 = inverse(sk_c5),
introduced(definition,[new_symbols(definition,[iPr_def_24])],[]) ).
tcf(c_733,definition,
iPr_def_25 = multiply(sk_c5,sk_c6),
introduced(definition,[new_symbols(definition,[iPr_def_25])],[]) ).
tcf(c_734,definition,
iPr_def_26 = multiply(sk_c3,sk_c12),
introduced(definition,[new_symbols(definition,[iPr_def_26])],[]) ).
tcf(c_735,definition,
iPr_def_27 = multiply(sk_c12,sk_c4),
introduced(definition,[new_symbols(definition,[iPr_def_27])],[]) ).
tcf(c_736,definition,
iPr_def_28 = multiply(sk_c2,sk_c11),
introduced(definition,[new_symbols(definition,[iPr_def_28])],[]) ).
tcf(c_737,definition,
iPr_def_29 = inverse(sk_c1),
introduced(definition,[new_symbols(definition,[iPr_def_29])],[]) ).
tcf(c_738,definition,
iPr_def_30 = multiply(sk_c1,sk_c2),
introduced(definition,[new_symbols(definition,[iPr_def_30])],[]) ).
tcf(c_739,negated_conjecture,
( iPr_def_14
| iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10 ),
inference(demodulation,[status(thm)],[c_722]) ).
tcf(c_740,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_14
| ( inverse(X0) != sk_c12 )
| ( multiply(sk_c12,multiply(X0,sk_c12)) != sk_c11 ) ),
inference(demodulation,[status(thm)],[c_721]) ).
tcf(c_741,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_13
| ( inverse(X0) != sk_c11 )
| ( multiply(X0,sk_c12) != sk_c11 ) ),
inference(demodulation,[status(thm)],[c_720]) ).
tcf(c_743,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_12
| ( inverse(X0) != sk_c12 )
| ( multiply(X0,sk_c11) != sk_c12 ) ),
inference(demodulation,[status(thm)],[c_719]) ).
tcf(c_744,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_11
| ( multiply(inverse(X0),sk_c11) != sk_c12 )
| ( multiply(X0,inverse(X0)) != sk_c12 ) ),
inference(demodulation,[status(thm)],[c_718]) ).
tcf(c_745,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_10
| ( multiply(inverse(X0),sk_c12) != sk_c11 )
| ( multiply(X0,inverse(X0)) != sk_c11 ) ),
inference(demodulation,[status(thm)],[c_717]) ).
tcf(c_746,negated_conjecture,
( ( iPr_def_16 = sk_c12 )
| ( iPr_def_15 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_175,c_724,c_723]) ).
tcf(c_747,negated_conjecture,
( ( iPr_def_17 = sk_c11 )
| ( iPr_def_16 = sk_c12 ) ),
inference(demodulation,[status(thm)],[c_174,c_725]) ).
tcf(c_748,negated_conjecture,
( ( iPr_def_18 = sk_c11 )
| ( iPr_def_16 = sk_c12 ) ),
inference(demodulation,[status(thm)],[c_173,c_726]) ).
tcf(c_749,negated_conjecture,
( ( iPr_def_19 = sk_c9 )
| ( iPr_def_16 = sk_c12 ) ),
inference(demodulation,[status(thm)],[c_172,c_727]) ).
tcf(c_750,negated_conjecture,
( ( iPr_def_20 = sk_c11 )
| ( iPr_def_16 = sk_c12 ) ),
inference(demodulation,[status(thm)],[c_171,c_728]) ).
tcf(c_751,negated_conjecture,
( ( iPr_def_21 = sk_c12 )
| ( iPr_def_16 = sk_c12 ) ),
inference(demodulation,[status(thm)],[c_170,c_729]) ).
tcf(c_752,negated_conjecture,
( ( iPr_def_22 = sk_c12 )
| ( iPr_def_16 = sk_c12 ) ),
inference(demodulation,[status(thm)],[c_169,c_730]) ).
tcf(c_755,negated_conjecture,
( ( iPr_def_25 = sk_c12 )
| ( iPr_def_16 = sk_c12 ) ),
inference(demodulation,[status(thm)],[c_166,c_733]) ).
tcf(c_756,negated_conjecture,
( ( iPr_def_26 = sk_c4 )
| ( iPr_def_15 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_165,c_734]) ).
tcf(c_757,negated_conjecture,
( ( iPr_def_26 = sk_c4 )
| ( iPr_def_17 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_164]) ).
tcf(c_759,negated_conjecture,
( ( iPr_def_26 = sk_c4 )
| ( iPr_def_19 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_162]) ).
tcf(c_760,negated_conjecture,
( ( iPr_def_26 = sk_c4 )
| ( iPr_def_20 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_161]) ).
tcf(c_761,negated_conjecture,
( ( iPr_def_26 = sk_c4 )
| ( iPr_def_21 = sk_c12 ) ),
inference(demodulation,[status(thm)],[c_160]) ).
tcf(c_764,negated_conjecture,
( ( iPr_def_26 = sk_c4 )
| ( iPr_def_24 = sk_c6 ) ),
inference(demodulation,[status(thm)],[c_157]) ).
tcf(c_765,negated_conjecture,
( ( iPr_def_26 = sk_c4 )
| ( iPr_def_25 = sk_c12 ) ),
inference(demodulation,[status(thm)],[c_156]) ).
tcf(c_766,negated_conjecture,
( ( iPr_def_27 = sk_c11 )
| ( iPr_def_15 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_155,c_735]) ).
tcf(c_767,negated_conjecture,
( ( iPr_def_27 = sk_c11 )
| ( iPr_def_17 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_154]) ).
tcf(c_768,negated_conjecture,
( ( iPr_def_27 = sk_c11 )
| ( iPr_def_18 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_153]) ).
tcf(c_769,negated_conjecture,
( ( iPr_def_27 = sk_c11 )
| ( iPr_def_19 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_152]) ).
tcf(c_770,negated_conjecture,
( ( iPr_def_27 = sk_c11 )
| ( iPr_def_20 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_151]) ).
tcf(c_771,negated_conjecture,
( ( iPr_def_27 = sk_c11 )
| ( iPr_def_21 = sk_c12 ) ),
inference(demodulation,[status(thm)],[c_150]) ).
tcf(c_772,negated_conjecture,
( ( iPr_def_27 = sk_c11 )
| ( iPr_def_22 = sk_c12 ) ),
inference(demodulation,[status(thm)],[c_149]) ).
tcf(c_775,negated_conjecture,
( ( iPr_def_27 = sk_c11 )
| ( iPr_def_25 = sk_c12 ) ),
inference(demodulation,[status(thm)],[c_146]) ).
tcf(c_776,negated_conjecture,
( ( iPr_def_28 = sk_c12 )
| ( iPr_def_15 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_145,c_736]) ).
tcf(c_777,negated_conjecture,
( ( iPr_def_28 = sk_c12 )
| ( iPr_def_17 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_144]) ).
tcf(c_779,negated_conjecture,
( ( iPr_def_28 = sk_c12 )
| ( iPr_def_19 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_142]) ).
tcf(c_780,negated_conjecture,
( ( iPr_def_28 = sk_c12 )
| ( iPr_def_20 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_141]) ).
tcf(c_781,negated_conjecture,
( ( iPr_def_28 = sk_c12 )
| ( iPr_def_21 = sk_c12 ) ),
inference(demodulation,[status(thm)],[c_140]) ).
tcf(c_782,negated_conjecture,
( ( iPr_def_28 = sk_c12 )
| ( iPr_def_22 = sk_c12 ) ),
inference(demodulation,[status(thm)],[c_139]) ).
tcf(c_785,negated_conjecture,
( ( iPr_def_28 = sk_c12 )
| ( iPr_def_25 = sk_c12 ) ),
inference(demodulation,[status(thm)],[c_136]) ).
tcf(c_791,negated_conjecture,
( ( iPr_def_29 = sk_c2 )
| ( iPr_def_21 = sk_c12 ) ),
inference(demodulation,[status(thm)],[c_130]) ).
tcf(c_792,negated_conjecture,
( ( iPr_def_29 = sk_c2 )
| ( iPr_def_22 = sk_c12 ) ),
inference(demodulation,[status(thm)],[c_129]) ).
tcf(c_794,negated_conjecture,
( ( iPr_def_29 = sk_c2 )
| ( iPr_def_24 = sk_c6 ) ),
inference(demodulation,[status(thm)],[c_127]) ).
tcf(c_795,negated_conjecture,
( ( iPr_def_29 = sk_c2 )
| ( iPr_def_25 = sk_c12 ) ),
inference(demodulation,[status(thm)],[c_126]) ).
tcf(c_796,negated_conjecture,
( ( iPr_def_30 = sk_c12 )
| ( iPr_def_15 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_125,c_738]) ).
tcf(c_797,negated_conjecture,
( ( iPr_def_30 = sk_c12 )
| ( iPr_def_17 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_124]) ).
tcf(c_798,negated_conjecture,
( ( iPr_def_30 = sk_c12 )
| ( iPr_def_18 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_123]) ).
tcf(c_799,negated_conjecture,
( ( iPr_def_30 = sk_c12 )
| ( iPr_def_19 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_122]) ).
tcf(c_800,negated_conjecture,
( ( iPr_def_30 = sk_c12 )
| ( iPr_def_20 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_121]) ).
tcf(c_801,negated_conjecture,
( ( iPr_def_30 = sk_c12 )
| ( iPr_def_21 = sk_c12 ) ),
inference(demodulation,[status(thm)],[c_120]) ).
tcf(c_802,negated_conjecture,
( ( iPr_def_30 = sk_c12 )
| ( iPr_def_22 = sk_c12 ) ),
inference(demodulation,[status(thm)],[c_119]) ).
tcf(c_804,negated_conjecture,
( ( iPr_def_30 = sk_c12 )
| ( iPr_def_24 = sk_c6 ) ),
inference(demodulation,[status(thm)],[c_117]) ).
tcf(c_805,negated_conjecture,
( ( iPr_def_30 = sk_c12 )
| ( iPr_def_25 = sk_c12 ) ),
inference(demodulation,[status(thm)],[c_116]) ).
tcf(c_806,plain,
! [X0: $i] : X0 = X0,
theory(equality) ).
tcf(c_807,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = X0 )
| ( X2 != X1 )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_808,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( multiply(X0,X2) = multiply(X1,X3) )
| ( X2 != X3 )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_812,plain,
sk_c12 = sk_c12,
inference(instantiation,[status(thm)],[c_806]) ).
tcf(c_1167,plain,
( ( iPr_def_15 = iPr_def_17 )
| ( sk_c12 = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_746,c_747]) ).
tcf(c_1221,plain,
( ( sk_c12 = iPr_def_16 )
| ( multiply(iPr_def_19,sk_c12) = iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_749,c_726]) ).
tcf(c_1297,plain,
( ( sk_c4 = iPr_def_26 )
| ( multiply(sk_c8,iPr_def_19) = iPr_def_20 ) ),
inference(superposition,[status(thm)],[c_759,c_728]) ).
tcf(c_1298,plain,
( ( sk_c12 = iPr_def_16 )
| ( multiply(sk_c8,iPr_def_19) = iPr_def_20 ) ),
inference(superposition,[status(thm)],[c_749,c_728]) ).
tcf(c_1335,plain,
( ( sk_c12 = iPr_def_16 )
| ( multiply(sk_c3,iPr_def_22) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_752,c_734]) ).
tcf(c_1336,plain,
( ( sk_c12 = iPr_def_16 )
| ( multiply(sk_c3,iPr_def_21) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_751,c_734]) ).
tcf(c_1352,plain,
( ( sk_c11 = iPr_def_15 )
| ( multiply(sk_c12,iPr_def_26) = iPr_def_27 ) ),
inference(superposition,[status(thm)],[c_756,c_735]) ).
tcf(c_1381,plain,
multiply(iPr_def_24,sk_c5) = identity,
inference(superposition,[status(thm)],[c_732,c_114]) ).
tcf(c_1382,plain,
multiply(iPr_def_22,sk_c7) = identity,
inference(superposition,[status(thm)],[c_730,c_114]) ).
tcf(c_1383,plain,
multiply(iPr_def_19,sk_c8) = identity,
inference(superposition,[status(thm)],[c_727,c_114]) ).
tcf(c_1384,plain,
multiply(iPr_def_17,sk_c10) = identity,
inference(superposition,[status(thm)],[c_725,c_114]) ).
tcf(c_1385,plain,
multiply(iPr_def_29,sk_c1) = identity,
inference(superposition,[status(thm)],[c_737,c_114]) ).
tcf(c_1386,plain,
multiply(iPr_def_16,sk_c3) = identity,
inference(superposition,[status(thm)],[c_724,c_114]) ).
tcf(c_1412,plain,
( ( sk_c4 = iPr_def_26 )
| ( multiply(sk_c5,iPr_def_24) = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_764,c_733]) ).
tcf(c_1422,plain,
( ( sk_c12 = iPr_def_25 )
| ( multiply(sk_c12,iPr_def_26) = iPr_def_27 ) ),
inference(superposition,[status(thm)],[c_765,c_735]) ).
tcf(c_1435,plain,
( ( sk_c11 = iPr_def_15 )
| ( multiply(sk_c7,iPr_def_27) = iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_766,c_729]) ).
tcf(c_1436,plain,
( ( iPr_def_20 = iPr_def_27 )
| ( sk_c11 = iPr_def_15 )
| ( sk_c12 = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_766,c_750]) ).
tcf(c_1439,plain,
( ( iPr_def_15 = iPr_def_27 )
| ( sk_c11 = iPr_def_15 )
| ( sk_c12 = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_766,c_746]) ).
tcf(c_1468,plain,
( ( sk_c11 = iPr_def_17 )
| ( multiply(sk_c7,iPr_def_27) = iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_767,c_729]) ).
tcf(c_1469,plain,
( ( iPr_def_20 = iPr_def_27 )
| ( sk_c11 = iPr_def_17 )
| ( sk_c12 = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_767,c_750]) ).
tcf(c_1471,plain,
( ( iPr_def_17 = iPr_def_27 )
| ( sk_c11 = iPr_def_17 )
| ( sk_c12 = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_767,c_747]) ).
tcf(c_1494,plain,
! [X0: $i,X1: $i] :
( ( sk_c11 = X0 )
| ( sk_c11 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_807]) ).
tcf(c_1495,plain,
! [X0: $i] :
( ( sk_c11 = X0 )
| ( sk_c11 != sk_c11 )
| ( X0 != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_1494]) ).
tcf(c_1496,plain,
sk_c11 = sk_c11,
inference(instantiation,[status(thm)],[c_806]) ).
tcf(c_1501,plain,
( ( sk_c11 = multiply(identity,sk_c11) )
| ( sk_c11 != sk_c11 )
| ( multiply(identity,sk_c11) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_1495]) ).
tcf(c_1502,plain,
multiply(identity,sk_c11) = sk_c11,
inference(instantiation,[status(thm)],[c_113]) ).
tcf(c_1504,plain,
! [X0: $i,X1: $i] :
( ( X0 = sk_c11 )
| ( sk_c11 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_807]) ).
tcf(c_1506,plain,
( ( sk_c11 = iPr_def_15 )
| ( iPr_def_15 != sk_c11 )
| ( sk_c11 != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_1495]) ).
tcf(c_1507,plain,
( ( sk_c11 = iPr_def_17 )
| ( iPr_def_17 != sk_c11 )
| ( sk_c11 != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_1495]) ).
tcf(c_1508,plain,
( ( sk_c11 = iPr_def_18 )
| ( iPr_def_18 != sk_c11 )
| ( sk_c11 != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_1495]) ).
tcf(c_1509,plain,
( ( sk_c11 = iPr_def_20 )
| ( iPr_def_20 != sk_c11 )
| ( sk_c11 != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_1495]) ).
tcf(c_1521,plain,
( ( sk_c11 = iPr_def_18 )
| ( multiply(sk_c7,iPr_def_27) = iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_768,c_729]) ).
tcf(c_1522,plain,
( ( iPr_def_20 = iPr_def_27 )
| ( sk_c11 = iPr_def_18 )
| ( sk_c12 = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_768,c_750]) ).
tcf(c_1523,plain,
( ( iPr_def_18 = iPr_def_27 )
| ( sk_c11 = iPr_def_18 )
| ( sk_c12 = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_768,c_748]) ).
tcf(c_1548,plain,
( ( sk_c11 = iPr_def_27 )
| ( multiply(sk_c8,iPr_def_19) = iPr_def_20 ) ),
inference(superposition,[status(thm)],[c_769,c_728]) ).
tcf(c_1549,plain,
( ( sk_c11 = iPr_def_27 )
| ( multiply(iPr_def_19,sk_c12) = iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_769,c_726]) ).
tcf(c_1564,plain,
( ( sk_c11 = iPr_def_20 )
| ( multiply(sk_c7,iPr_def_27) = iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_770,c_729]) ).
tcf(c_1565,plain,
( ( iPr_def_20 = iPr_def_27 )
| ( sk_c11 = iPr_def_20 )
| ( sk_c12 = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_770,c_750]) ).
tcf(c_1591,plain,
! [X0: $i] :
( ( sk_c11 = X0 )
| ( sk_c11 != iPr_def_17 )
| ( X0 != iPr_def_17 ) ),
inference(instantiation,[status(thm)],[c_1494]) ).
tcf(c_1605,plain,
( ( sk_c12 = iPr_def_21 )
| ( multiply(sk_c7,iPr_def_27) = iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_771,c_729]) ).
tcf(c_1646,plain,
( ( sk_c12 = iPr_def_22 )
| ( multiply(sk_c7,iPr_def_27) = iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_772,c_729]) ).
tcf(c_1669,plain,
! [X0: $i] :
( ( sk_c11 = X0 )
| ( sk_c11 != multiply(identity,sk_c11) )
| ( X0 != multiply(identity,sk_c11) ) ),
inference(instantiation,[status(thm)],[c_1494]) ).
tcf(c_1672,plain,
( ( sk_c11 = sk_c12 )
| ( sk_c11 != multiply(identity,sk_c11) )
| ( sk_c12 != multiply(identity,sk_c11) ) ),
inference(instantiation,[status(thm)],[c_1669]) ).
tcf(c_1676,plain,
! [X0: $i] :
( ( X0 = sk_c11 )
| ( sk_c11 != iPr_def_20 )
| ( X0 != iPr_def_20 ) ),
inference(instantiation,[status(thm)],[c_1504]) ).
tcf(c_1678,plain,
! [X0: $i] :
( ( X0 = sk_c11 )
| ( sk_c11 != iPr_def_18 )
| ( X0 != iPr_def_18 ) ),
inference(instantiation,[status(thm)],[c_1504]) ).
tcf(c_1680,plain,
! [X0: $i] :
( ( X0 = sk_c11 )
| ( sk_c11 != iPr_def_17 )
| ( X0 != iPr_def_17 ) ),
inference(instantiation,[status(thm)],[c_1504]) ).
tcf(c_1682,plain,
! [X0: $i] :
( ( X0 = sk_c11 )
| ( sk_c11 != iPr_def_15 )
| ( X0 != iPr_def_15 ) ),
inference(instantiation,[status(thm)],[c_1504]) ).
tcf(c_1685,plain,
! [X0: $i] :
( ( X0 = sk_c11 )
| ( sk_c11 != multiply(identity,sk_c11) )
| ( X0 != multiply(identity,sk_c11) ) ),
inference(instantiation,[status(thm)],[c_1504]) ).
tcf(c_1686,plain,
( ( sk_c12 = sk_c11 )
| ( sk_c11 != multiply(identity,sk_c11) )
| ( sk_c12 != multiply(identity,sk_c11) ) ),
inference(instantiation,[status(thm)],[c_1685]) ).
tcf(c_1723,plain,
! [X0: $i,X1: $i] :
( ( X0 = iPr_def_15 )
| ( iPr_def_15 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_807]) ).
tcf(c_1730,plain,
! [X0: $i,X1: $i] :
( ( X0 = iPr_def_17 )
| ( iPr_def_17 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_807]) ).
tcf(c_1891,plain,
( ( iPr_def_15 = iPr_def_17 )
| ( sk_c12 = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_777,c_776]) ).
tcf(c_1950,plain,
( ( sk_c11 = multiply(identity,multiply(identity,sk_c11)) )
| ( sk_c11 != multiply(identity,sk_c11) )
| ( multiply(identity,multiply(identity,sk_c11)) != multiply(identity,sk_c11) ) ),
inference(instantiation,[status(thm)],[c_1669]) ).
tcf(c_1951,plain,
multiply(identity,multiply(identity,sk_c11)) = multiply(identity,sk_c11),
inference(instantiation,[status(thm)],[c_113]) ).
tcf(c_1953,plain,
! [X0: $i,X1: $i] :
( ( X1 = multiply(identity,sk_c11) )
| ( X1 != X0 )
| ( multiply(identity,sk_c11) != X0 ) ),
inference(instantiation,[status(thm)],[c_807]) ).
tcf(c_1967,plain,
! [X0: $i] :
( ( X0 = sk_c11 )
| ( sk_c11 != iPr_def_27 )
| ( X0 != iPr_def_27 ) ),
inference(instantiation,[status(thm)],[c_1504]) ).
tcf(c_1968,plain,
! [X0: $i] :
( ( sk_c11 = X0 )
| ( sk_c11 != iPr_def_27 )
| ( X0 != iPr_def_27 ) ),
inference(instantiation,[status(thm)],[c_1494]) ).
tcf(c_1971,plain,
( ( sk_c11 = sk_c12 )
| ( sk_c11 != iPr_def_27 )
| ( sk_c12 != iPr_def_27 ) ),
inference(instantiation,[status(thm)],[c_1968]) ).
tcf(c_2066,plain,
! [X0: $i] :
( ( X0 = iPr_def_15 )
| ( iPr_def_15 != multiply(sk_c10,sk_c12) )
| ( X0 != multiply(sk_c10,sk_c12) ) ),
inference(instantiation,[status(thm)],[c_1723]) ).
tcf(c_2069,plain,
! [X0: $i,X1: $i] :
( ( iPr_def_17 = X0 )
| ( iPr_def_17 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_807]) ).
tcf(c_2070,plain,
! [X0: $i] :
( ( X0 = iPr_def_17 )
| ( iPr_def_17 != inverse(sk_c10) )
| ( X0 != inverse(sk_c10) ) ),
inference(instantiation,[status(thm)],[c_1730]) ).
tcf(c_2088,plain,
( ( sk_c12 = iPr_def_28 )
| ( multiply(sk_c8,iPr_def_19) = iPr_def_20 ) ),
inference(superposition,[status(thm)],[c_779,c_728]) ).
tcf(c_2097,plain,
! [X0: $i,X1: $i] :
( ( multiply(identity,sk_c11) = X1 )
| ( X1 != X0 )
| ( multiply(identity,sk_c11) != X0 ) ),
inference(instantiation,[status(thm)],[c_807]) ).
tcf(c_2187,plain,
! [X0: $i] :
( ( X0 = multiply(identity,sk_c11) )
| ( X0 != sk_c11 )
| ( multiply(identity,sk_c11) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_1953]) ).
tcf(c_2195,plain,
multiply(identity,identity) = identity,
inference(instantiation,[status(thm)],[c_113]) ).
tcf(c_2200,plain,
identity = identity,
inference(instantiation,[status(thm)],[c_806]) ).
tcf(c_2242,plain,
( ( iPr_def_27 = sk_c11 )
| ( iPr_def_27 != iPr_def_27 )
| ( sk_c11 != iPr_def_27 ) ),
inference(instantiation,[status(thm)],[c_1967]) ).
tcf(c_2243,plain,
iPr_def_27 = iPr_def_27,
inference(instantiation,[status(thm)],[c_806]) ).
tcf(c_2244,plain,
! [X0: $i,X1: $i] :
( ( X0 = iPr_def_27 )
| ( iPr_def_27 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_807]) ).
tcf(c_2339,plain,
! [X0: $i,X1: $i] :
( ( multiply(X0,X1) = multiply(identity,multiply(identity,sk_c11)) )
| ( X1 != multiply(identity,sk_c11) )
| ( X0 != identity ) ),
inference(instantiation,[status(thm)],[c_808]) ).
tcf(c_2399,plain,
( ( iPr_def_15 = iPr_def_15 )
| ( iPr_def_15 != multiply(sk_c10,sk_c12) ) ),
inference(instantiation,[status(thm)],[c_2066]) ).
tcf(c_2440,plain,
( ( iPr_def_17 = iPr_def_17 )
| ( iPr_def_17 != inverse(sk_c10) ) ),
inference(instantiation,[status(thm)],[c_2070]) ).
tcf(c_2465,plain,
( ( sk_c12 = iPr_def_21 )
| ( multiply(sk_c1,iPr_def_29) = iPr_def_30 ) ),
inference(superposition,[status(thm)],[c_791,c_738]) ).
tcf(c_2475,plain,
( ( sk_c12 = iPr_def_22 )
| ( multiply(sk_c1,iPr_def_29) = iPr_def_30 ) ),
inference(superposition,[status(thm)],[c_792,c_738]) ).
tcf(c_2495,plain,
( ( sk_c2 = iPr_def_29 )
| ( multiply(sk_c5,iPr_def_24) = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_794,c_733]) ).
tcf(c_2505,plain,
( ( sk_c12 = iPr_def_25 )
| ( multiply(sk_c1,iPr_def_29) = iPr_def_30 ) ),
inference(superposition,[status(thm)],[c_795,c_738]) ).
tcf(c_2553,plain,
( ( sk_c12 = iPr_def_30 )
| ( multiply(sk_c7,iPr_def_15) = iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_796,c_729]) ).
tcf(c_2635,plain,
( ( iPr_def_15 = iPr_def_17 )
| ( sk_c12 = iPr_def_30 ) ),
inference(superposition,[status(thm)],[c_797,c_796]) ).
tcf(c_2649,plain,
( ( sk_c12 = iPr_def_30 )
| ( multiply(sk_c7,iPr_def_17) = iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_797,c_729]) ).
tcf(c_2704,plain,
! [X0: $i] :
( ( iPr_def_17 = X0 )
| ( iPr_def_17 != iPr_def_17 )
| ( X0 != iPr_def_17 ) ),
inference(instantiation,[status(thm)],[c_2069]) ).
tcf(c_2792,plain,
( ( sk_c12 = iPr_def_30 )
| ( multiply(sk_c7,iPr_def_18) = iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_798,c_729]) ).
tcf(c_2838,plain,
! [X0: $i] :
( ( multiply(identity,sk_c11) = X0 )
| ( X0 != multiply(identity,sk_c11) )
| ( multiply(identity,sk_c11) != multiply(identity,sk_c11) ) ),
inference(instantiation,[status(thm)],[c_2097]) ).
tcf(c_2839,plain,
multiply(identity,sk_c11) = multiply(identity,sk_c11),
inference(instantiation,[status(thm)],[c_806]) ).
tcf(c_2840,plain,
( ( multiply(identity,sk_c11) = sk_c12 )
| ( sk_c12 != multiply(identity,sk_c11) )
| ( multiply(identity,sk_c11) != multiply(identity,sk_c11) ) ),
inference(instantiation,[status(thm)],[c_2838]) ).
tcf(c_2844,plain,
! [X0: $i] :
( ( multiply(identity,sk_c11) = X0 )
| ( X0 != sk_c11 )
| ( multiply(identity,sk_c11) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_2097]) ).
tcf(c_2883,plain,
! [X0: $i] :
( ( X0 = iPr_def_17 )
| ( iPr_def_17 != sk_c11 )
| ( X0 != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_1730]) ).
tcf(c_2884,plain,
( ( sk_c12 = iPr_def_17 )
| ( iPr_def_17 != sk_c11 )
| ( sk_c12 != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_2883]) ).
tcf(c_2898,plain,
( ( sk_c12 = iPr_def_30 )
| ( multiply(sk_c8,iPr_def_19) = iPr_def_20 ) ),
inference(superposition,[status(thm)],[c_799,c_728]) ).
tcf(c_2899,plain,
( ( sk_c12 = iPr_def_30 )
| ( multiply(iPr_def_19,sk_c12) = iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_799,c_726]) ).
tcf(c_2947,plain,
( ( sk_c12 = iPr_def_30 )
| ( multiply(sk_c7,iPr_def_20) = iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_800,c_729]) ).
tcf(c_3047,plain,
( ( iPr_def_28 = iPr_def_30 )
| ( sk_c12 = iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_801,c_781]) ).
tcf(c_3049,plain,
( ( sk_c12 = iPr_def_21 )
| ( multiply(sk_c3,iPr_def_30) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_801,c_734]) ).
tcf(c_3149,plain,
( ( iPr_def_28 = iPr_def_30 )
| ( sk_c12 = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_802,c_782]) ).
tcf(c_3152,plain,
( ( sk_c12 = iPr_def_22 )
| ( multiply(sk_c3,iPr_def_30) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_802,c_734]) ).
tcf(c_3294,plain,
( ( sk_c12 = iPr_def_30 )
| ( multiply(sk_c5,iPr_def_24) = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_804,c_733]) ).
tcf(c_3329,plain,
( ( sk_c12 = iPr_def_25 )
| ( multiply(sk_c3,iPr_def_30) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_805,c_734]) ).
tcf(c_3362,plain,
( ( iPr_def_17 = multiply(identity,sk_c11) )
| ( iPr_def_17 != sk_c11 )
| ( multiply(identity,sk_c11) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_2187]) ).
tcf(c_3381,plain,
( ~ iPr_def_13
| ( sk_c11 != iPr_def_15 )
| ( inverse(sk_c10) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_723,c_741]) ).
tcf(c_3383,plain,
( ~ iPr_def_13
| ( sk_c12 != sk_c11 )
| ( inverse(identity) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_113,c_741]) ).
tcf(c_3404,plain,
( ~ iPr_def_13
| ( sk_c11 != iPr_def_17 )
| ( sk_c11 != iPr_def_15 ) ),
inference(light_normalisation,[status(thm)],[c_3381,c_725]) ).
tcf(c_3544,plain,
( ~ iPr_def_12
| ( sk_c12 != iPr_def_21 )
| ( inverse(sk_c7) != sk_c12 ) ),
inference(superposition,[status(thm)],[c_729,c_743]) ).
tcf(c_3546,plain,
( ~ iPr_def_12
| ( sk_c12 != sk_c11 )
| ( inverse(identity) != sk_c12 ) ),
inference(superposition,[status(thm)],[c_113,c_743]) ).
tcf(c_3574,plain,
( ~ iPr_def_12
| ( sk_c12 != iPr_def_22 )
| ( sk_c12 != iPr_def_21 ) ),
inference(light_normalisation,[status(thm)],[c_3544,c_730]) ).
tcf(c_3685,plain,
! [X0: $i,X1: $i] :
( ( identity = X0 )
| ( identity != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_807]) ).
tcf(c_3744,plain,
( ~ iPr_def_14
| ( inverse(sk_c10) != sk_c12 )
| ( multiply(sk_c12,iPr_def_15) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_723,c_740]) ).
tcf(c_3745,plain,
( ~ iPr_def_14
| ( inverse(sk_c3) != sk_c12 )
| ( multiply(sk_c12,iPr_def_26) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_734,c_740]) ).
tcf(c_3763,plain,
( ~ iPr_def_14
| ( sk_c12 != iPr_def_16 )
| ( multiply(sk_c12,iPr_def_26) != sk_c11 ) ),
inference(light_normalisation,[status(thm)],[c_3745,c_724]) ).
tcf(c_3767,plain,
( ~ iPr_def_14
| ( sk_c12 != iPr_def_17 )
| ( multiply(sk_c12,iPr_def_15) != sk_c11 ) ),
inference(light_normalisation,[status(thm)],[c_3744,c_725]) ).
tcf(c_3853,plain,
! [X0: $i] :
( ( X0 = iPr_def_17 )
| ( iPr_def_17 != multiply(identity,sk_c11) )
| ( X0 != multiply(identity,sk_c11) ) ),
inference(instantiation,[status(thm)],[c_1730]) ).
tcf(c_3854,plain,
( ( sk_c12 = iPr_def_17 )
| ( iPr_def_17 != multiply(identity,sk_c11) )
| ( sk_c12 != multiply(identity,sk_c11) ) ),
inference(instantiation,[status(thm)],[c_3853]) ).
tcf(c_3953,plain,
( ~ iPr_def_10
| ( multiply(sk_c8,iPr_def_19) != sk_c11 )
| ( multiply(inverse(sk_c8),sk_c12) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_727,c_745]) ).
tcf(c_3972,plain,
( ~ iPr_def_10
| ( multiply(iPr_def_19,sk_c12) != sk_c11 )
| ( multiply(sk_c8,iPr_def_19) != sk_c11 ) ),
inference(light_normalisation,[status(thm)],[c_3953,c_727]) ).
tcf(c_4427,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(X0,X1)) = multiply(identity,X1),
inference(superposition,[status(thm)],[c_114,c_115]) ).
tcf(c_4429,plain,
! [X0: $i] : multiply(iPr_def_24,multiply(sk_c5,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1381,c_115]) ).
tcf(c_4430,plain,
! [X0: $i] : multiply(iPr_def_22,multiply(sk_c7,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1382,c_115]) ).
tcf(c_4431,plain,
! [X0: $i] : multiply(iPr_def_19,multiply(sk_c8,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1383,c_115]) ).
tcf(c_4432,plain,
! [X0: $i] : multiply(iPr_def_17,multiply(sk_c10,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1384,c_115]) ).
tcf(c_4433,plain,
! [X0: $i] : multiply(iPr_def_29,multiply(sk_c1,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1385,c_115]) ).
tcf(c_4434,plain,
! [X0: $i] : multiply(iPr_def_16,multiply(sk_c3,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1386,c_115]) ).
tcf(c_4441,plain,
! [X0: $i] : multiply(iPr_def_16,multiply(sk_c3,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_4434,c_113]) ).
tcf(c_4442,plain,
! [X0: $i] : multiply(iPr_def_29,multiply(sk_c1,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_4433,c_113]) ).
tcf(c_4443,plain,
! [X0: $i] : multiply(iPr_def_17,multiply(sk_c10,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_4432,c_113]) ).
tcf(c_4444,plain,
! [X0: $i] : multiply(iPr_def_19,multiply(sk_c8,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_4431,c_113]) ).
tcf(c_4445,plain,
! [X0: $i] : multiply(iPr_def_22,multiply(sk_c7,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_4430,c_113]) ).
tcf(c_4446,plain,
! [X0: $i] : multiply(iPr_def_24,multiply(sk_c5,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_4429,c_113]) ).
tcf(c_4565,plain,
( ( iPr_def_27 = multiply(identity,sk_c11) )
| ( iPr_def_27 != sk_c11 )
| ( multiply(identity,sk_c11) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_2187]) ).
tcf(c_4809,plain,
! [X0: $i] :
( ( X0 = iPr_def_27 )
| ( iPr_def_27 != multiply(sk_c12,sk_c4) )
| ( X0 != multiply(sk_c12,sk_c4) ) ),
inference(instantiation,[status(thm)],[c_2244]) ).
tcf(c_5714,plain,
( ( iPr_def_15 = sk_c11 )
| ( iPr_def_15 != iPr_def_15 )
| ( sk_c11 != iPr_def_15 ) ),
inference(instantiation,[status(thm)],[c_1682]) ).
tcf(c_5836,plain,
! [X0: $i] :
( ( multiply(identity,X0) = multiply(identity,multiply(identity,sk_c11)) )
| ( identity != identity )
| ( X0 != multiply(identity,sk_c11) ) ),
inference(instantiation,[status(thm)],[c_2339]) ).
tcf(c_5837,plain,
( ( multiply(identity,sk_c12) = multiply(identity,multiply(identity,sk_c11)) )
| ( identity != identity )
| ( sk_c12 != multiply(identity,sk_c11) ) ),
inference(instantiation,[status(thm)],[c_5836]) ).
tcf(c_5976,plain,
( ( iPr_def_17 = sk_c11 )
| ( iPr_def_17 != iPr_def_17 )
| ( sk_c11 != iPr_def_17 ) ),
inference(instantiation,[status(thm)],[c_1680]) ).
tcf(c_6476,plain,
( ( multiply(identity,sk_c11) = iPr_def_27 )
| ( iPr_def_27 != sk_c11 )
| ( multiply(identity,sk_c11) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_2844]) ).
tcf(c_6516,plain,
( ( iPr_def_28 = iPr_def_30 )
| ( iPr_def_15 = iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_2635,c_1891]) ).
tcf(c_6602,plain,
! [X0: $i] :
( ( identity = X0 )
| ( identity != identity )
| ( X0 != identity ) ),
inference(instantiation,[status(thm)],[c_3685]) ).
tcf(c_7453,plain,
( ( iPr_def_17 = iPr_def_15 )
| ( iPr_def_17 != iPr_def_17 )
| ( iPr_def_15 != iPr_def_17 ) ),
inference(instantiation,[status(thm)],[c_2704]) ).
tcf(c_7454,plain,
( ( iPr_def_15 = sk_c11 )
| ( iPr_def_15 != iPr_def_17 )
| ( sk_c11 != iPr_def_17 ) ),
inference(instantiation,[status(thm)],[c_1680]) ).
tcf(c_7455,plain,
( ( sk_c11 = iPr_def_15 )
| ( iPr_def_15 != iPr_def_17 )
| ( sk_c11 != iPr_def_17 ) ),
inference(instantiation,[status(thm)],[c_1591]) ).
tcf(c_7968,plain,
( ( sk_c11 = iPr_def_20 )
| ( iPr_def_20 != iPr_def_27 )
| ( sk_c11 != iPr_def_27 ) ),
inference(instantiation,[status(thm)],[c_1968]) ).
tcf(c_7969,plain,
( ( iPr_def_20 = sk_c11 )
| ( iPr_def_20 != iPr_def_27 )
| ( sk_c11 != iPr_def_27 ) ),
inference(instantiation,[status(thm)],[c_1967]) ).
tcf(c_7982,plain,
( ( iPr_def_18 = sk_c11 )
| ( iPr_def_18 != iPr_def_27 )
| ( sk_c11 != iPr_def_27 ) ),
inference(instantiation,[status(thm)],[c_1967]) ).
tcf(c_8244,plain,
( ( iPr_def_17 = sk_c11 )
| ( iPr_def_17 != iPr_def_27 )
| ( sk_c11 != iPr_def_27 ) ),
inference(instantiation,[status(thm)],[c_1967]) ).
tcf(c_8257,plain,
( ( iPr_def_15 = sk_c11 )
| ( iPr_def_15 != iPr_def_27 )
| ( sk_c11 != iPr_def_27 ) ),
inference(instantiation,[status(thm)],[c_1967]) ).
tcf(c_8270,plain,
! [X0: $i] :
( ( X0 = iPr_def_27 )
| ( iPr_def_27 != multiply(identity,sk_c11) )
| ( X0 != multiply(identity,sk_c11) ) ),
inference(instantiation,[status(thm)],[c_2244]) ).
tcf(c_8271,plain,
( ( sk_c12 = iPr_def_27 )
| ( iPr_def_27 != multiply(identity,sk_c11) )
| ( sk_c12 != multiply(identity,sk_c11) ) ),
inference(instantiation,[status(thm)],[c_8270]) ).
tcf(c_8372,plain,
! [X0: $i] :
( ( X0 = multiply(identity,sk_c11) )
| ( X0 != iPr_def_27 )
| ( multiply(identity,sk_c11) != iPr_def_27 ) ),
inference(instantiation,[status(thm)],[c_1953]) ).
tcf(c_8373,plain,
( ( sk_c12 = multiply(identity,sk_c11) )
| ( sk_c12 != iPr_def_27 )
| ( multiply(identity,sk_c11) != iPr_def_27 ) ),
inference(instantiation,[status(thm)],[c_8372]) ).
tcf(c_8574,plain,
multiply(iPr_def_16,iPr_def_26) = sk_c12,
inference(superposition,[status(thm)],[c_734,c_4441]) ).
tcf(c_8581,plain,
( ( multiply(sk_c12,sk_c4) = iPr_def_27 )
| ( iPr_def_27 != multiply(sk_c12,sk_c4) )
| ( multiply(sk_c12,sk_c4) != multiply(sk_c12,sk_c4) ) ),
inference(instantiation,[status(thm)],[c_4809]) ).
tcf(c_8582,plain,
multiply(sk_c12,sk_c4) = multiply(sk_c12,sk_c4),
inference(instantiation,[status(thm)],[c_806]) ).
tcf(c_8586,plain,
! [X0: $i,X1: $i] :
( ( multiply(X0,X1) = multiply(sk_c12,sk_c4) )
| ( X1 != sk_c4 )
| ( X0 != sk_c12 ) ),
inference(instantiation,[status(thm)],[c_808]) ).
tcf(c_8590,plain,
multiply(iPr_def_29,iPr_def_30) = sk_c2,
inference(superposition,[status(thm)],[c_738,c_4442]) ).
tcf(c_9049,plain,
multiply(iPr_def_22,iPr_def_21) = sk_c11,
inference(superposition,[status(thm)],[c_729,c_4445]) ).
tcf(c_9082,plain,
multiply(iPr_def_24,iPr_def_25) = sk_c6,
inference(superposition,[status(thm)],[c_733,c_4446]) ).
tcf(c_9195,plain,
( ( sk_c12 = iPr_def_16 )
| ( multiply(iPr_def_16,iPr_def_26) = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_1335,c_4441]) ).
tcf(c_9196,plain,
( ( sk_c12 = iPr_def_22 )
| ( sk_c12 = iPr_def_16 ) ),
inference(light_normalisation,[status(thm)],[c_9195,c_8574]) ).
tcf(c_9207,plain,
( ( sk_c12 = iPr_def_16 )
| ( multiply(iPr_def_16,iPr_def_26) = iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_1336,c_4441]) ).
tcf(c_9208,plain,
( ( sk_c12 = iPr_def_21 )
| ( sk_c12 = iPr_def_16 ) ),
inference(light_normalisation,[status(thm)],[c_9207,c_8574]) ).
tcf(c_10107,plain,
( ( iPr_def_15 = iPr_def_17 )
| ( sk_c11 = iPr_def_15 )
| ( multiply(iPr_def_16,iPr_def_26) = iPr_def_27 ) ),
inference(superposition,[status(thm)],[c_1167,c_1352]) ).
tcf(c_10147,plain,
( ( iPr_def_15 = iPr_def_17 )
| ( sk_c11 = iPr_def_15 )
| ( sk_c12 = iPr_def_27 ) ),
inference(light_normalisation,[status(thm)],[c_10107,c_8574]) ).
tcf(c_11237,plain,
( ( sk_c11 = iPr_def_15 )
| ( multiply(iPr_def_22,iPr_def_21) = iPr_def_27 ) ),
inference(superposition,[status(thm)],[c_1435,c_4445]) ).
tcf(c_11238,plain,
( ( sk_c11 = iPr_def_27 )
| ( sk_c11 = iPr_def_15 ) ),
inference(light_normalisation,[status(thm)],[c_11237,c_9049]) ).
tcf(c_11315,plain,
( ( sk_c11 = iPr_def_17 )
| ( multiply(iPr_def_22,iPr_def_21) = iPr_def_27 ) ),
inference(superposition,[status(thm)],[c_1468,c_4445]) ).
tcf(c_11316,plain,
( ( sk_c11 = iPr_def_27 )
| ( sk_c11 = iPr_def_17 ) ),
inference(light_normalisation,[status(thm)],[c_11315,c_9049]) ).
tcf(c_11487,plain,
( ( sk_c12 = iPr_def_16 )
| ( sk_c11 = iPr_def_15 ) ),
inference(global_subsumption_just,[status(thm)],[c_1436,c_1439,c_1496,c_1506,c_8257,c_11238]) ).
tcf(c_11488,plain,
( ( sk_c11 = iPr_def_15 )
| ( sk_c12 = iPr_def_16 ) ),
inference(renaming,[status(thm)],[c_11487]) ).
tcf(c_11538,plain,
( ( sk_c11 = iPr_def_18 )
| ( multiply(iPr_def_22,iPr_def_21) = iPr_def_27 ) ),
inference(superposition,[status(thm)],[c_1521,c_4445]) ).
tcf(c_11539,plain,
( ( sk_c11 = iPr_def_27 )
| ( sk_c11 = iPr_def_18 ) ),
inference(light_normalisation,[status(thm)],[c_11538,c_9049]) ).
tcf(c_11970,plain,
( ( sk_c11 = iPr_def_20 )
| ( multiply(iPr_def_22,iPr_def_21) = iPr_def_27 ) ),
inference(superposition,[status(thm)],[c_1564,c_4445]) ).
tcf(c_11971,plain,
( ( sk_c11 = iPr_def_27 )
| ( sk_c11 = iPr_def_20 ) ),
inference(light_normalisation,[status(thm)],[c_11970,c_9049]) ).
tcf(c_12036,plain,
( ( sk_c12 = iPr_def_21 )
| ( multiply(iPr_def_22,iPr_def_21) = iPr_def_27 ) ),
inference(superposition,[status(thm)],[c_1605,c_4445]) ).
tcf(c_12037,plain,
( ( sk_c11 = iPr_def_27 )
| ( sk_c12 = iPr_def_21 ) ),
inference(light_normalisation,[status(thm)],[c_12036,c_9049]) ).
tcf(c_12092,plain,
( ( sk_c12 = iPr_def_22 )
| ( multiply(iPr_def_22,iPr_def_21) = iPr_def_27 ) ),
inference(superposition,[status(thm)],[c_1646,c_4445]) ).
tcf(c_12093,plain,
( ( sk_c11 = iPr_def_27 )
| ( sk_c12 = iPr_def_22 ) ),
inference(light_normalisation,[status(thm)],[c_12092,c_9049]) ).
tcf(c_13820,plain,
( ( sk_c12 = iPr_def_16 )
| ( sk_c11 = iPr_def_17 ) ),
inference(global_subsumption_just,[status(thm)],[c_1469,c_1471,c_1496,c_1507,c_8244,c_11316]) ).
tcf(c_13821,plain,
( ( sk_c11 = iPr_def_17 )
| ( sk_c12 = iPr_def_16 ) ),
inference(renaming,[status(thm)],[c_13820]) ).
tcf(c_15606,plain,
( ( sk_c12 = iPr_def_30 )
| ( multiply(iPr_def_22,iPr_def_21) = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_2553,c_4445]) ).
tcf(c_15607,plain,
( ( sk_c11 = iPr_def_15 )
| ( sk_c12 = iPr_def_30 ) ),
inference(light_normalisation,[status(thm)],[c_15606,c_9049]) ).
tcf(c_15848,plain,
( ( sk_c12 = iPr_def_30 )
| ( multiply(iPr_def_22,iPr_def_21) = iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_2649,c_4445]) ).
tcf(c_15849,plain,
( ( sk_c11 = iPr_def_17 )
| ( sk_c12 = iPr_def_30 ) ),
inference(light_normalisation,[status(thm)],[c_15848,c_9049]) ).
tcf(c_15894,plain,
( ( sk_c12 = iPr_def_30 )
| ( multiply(iPr_def_22,iPr_def_21) = iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_2792,c_4445]) ).
tcf(c_15895,plain,
( ( sk_c11 = iPr_def_18 )
| ( sk_c12 = iPr_def_30 ) ),
inference(light_normalisation,[status(thm)],[c_15894,c_9049]) ).
tcf(c_16078,plain,
( ( sk_c12 = iPr_def_30 )
| ( multiply(iPr_def_22,iPr_def_21) = iPr_def_20 ) ),
inference(superposition,[status(thm)],[c_2947,c_4445]) ).
tcf(c_16079,plain,
( ( sk_c11 = iPr_def_20 )
| ( sk_c12 = iPr_def_30 ) ),
inference(light_normalisation,[status(thm)],[c_16078,c_9049]) ).
tcf(c_16146,plain,
( ( sk_c12 = iPr_def_21 )
| ( multiply(iPr_def_16,iPr_def_26) = iPr_def_30 ) ),
inference(superposition,[status(thm)],[c_3049,c_4441]) ).
tcf(c_16147,plain,
( ( sk_c12 = iPr_def_30 )
| ( sk_c12 = iPr_def_21 ) ),
inference(light_normalisation,[status(thm)],[c_16146,c_8574]) ).
tcf(c_16502,plain,
( ( sk_c12 = iPr_def_22 )
| ( multiply(iPr_def_16,iPr_def_26) = iPr_def_30 ) ),
inference(superposition,[status(thm)],[c_3152,c_4441]) ).
tcf(c_16503,plain,
( ( sk_c12 = iPr_def_30 )
| ( sk_c12 = iPr_def_22 ) ),
inference(light_normalisation,[status(thm)],[c_16502,c_8574]) ).
tcf(c_16636,plain,
( ( sk_c12 = iPr_def_16 )
| ( sk_c11 = iPr_def_18 ) ),
inference(global_subsumption_just,[status(thm)],[c_1522,c_1496,c_1508,c_1523,c_7982,c_11539]) ).
tcf(c_16637,plain,
( ( sk_c11 = iPr_def_18 )
| ( sk_c12 = iPr_def_16 ) ),
inference(renaming,[status(thm)],[c_16636]) ).
tcf(c_17168,plain,
( ( sk_c12 = iPr_def_25 )
| ( multiply(iPr_def_16,iPr_def_26) = iPr_def_30 ) ),
inference(superposition,[status(thm)],[c_3329,c_4441]) ).
tcf(c_17169,plain,
( ( sk_c12 = iPr_def_30 )
| ( sk_c12 = iPr_def_25 ) ),
inference(light_normalisation,[status(thm)],[c_17168,c_8574]) ).
tcf(c_18434,plain,
( ( sk_c12 = iPr_def_16 )
| ( sk_c11 = iPr_def_20 ) ),
inference(global_subsumption_just,[status(thm)],[c_1565,c_1496,c_1509,c_1565,c_7969,c_11971]) ).
tcf(c_18435,plain,
( ( sk_c11 = iPr_def_20 )
| ( sk_c12 = iPr_def_16 ) ),
inference(renaming,[status(thm)],[c_18434]) ).
tcf(c_23274,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(X0,X1)) = X1,
inference(demodulation,[status(thm)],[c_4427,c_113]) ).
tcf(c_23291,plain,
! [X0: $i] : multiply(inverse(identity),X0) = X0,
inference(superposition,[status(thm)],[c_113,c_23274]) ).
tcf(c_23292,plain,
! [X0: $i] : multiply(inverse(inverse(X0)),identity) = X0,
inference(superposition,[status(thm)],[c_114,c_23274]) ).
tcf(c_23579,plain,
! [X0: $i] : multiply(inverse(iPr_def_24),X0) = multiply(sk_c5,X0),
inference(superposition,[status(thm)],[c_4446,c_23274]) ).
tcf(c_23580,plain,
! [X0: $i] : multiply(inverse(iPr_def_22),X0) = multiply(sk_c7,X0),
inference(superposition,[status(thm)],[c_4445,c_23274]) ).
tcf(c_23581,plain,
! [X0: $i] : multiply(inverse(iPr_def_19),X0) = multiply(sk_c8,X0),
inference(superposition,[status(thm)],[c_4444,c_23274]) ).
tcf(c_23582,plain,
! [X0: $i] : multiply(inverse(iPr_def_17),X0) = multiply(sk_c10,X0),
inference(superposition,[status(thm)],[c_4443,c_23274]) ).
tcf(c_23583,plain,
! [X0: $i] : multiply(inverse(iPr_def_29),X0) = multiply(sk_c1,X0),
inference(superposition,[status(thm)],[c_4442,c_23274]) ).
tcf(c_23635,plain,
! [X0: $i,X1: $i] : multiply(inverse(inverse(X0)),X1) = multiply(X0,X1),
inference(superposition,[status(thm)],[c_23274,c_23274]) ).
tcf(c_24441,plain,
( ( identity = multiply(identity,identity) )
| ( identity != identity )
| ( multiply(identity,identity) != identity ) ),
inference(instantiation,[status(thm)],[c_6602]) ).
tcf(c_24871,plain,
! [X0: $i] : multiply(X0,identity) = X0,
inference(demodulation,[status(thm)],[c_23292,c_23635]) ).
tcf(c_24903,plain,
inverse(identity) = identity,
inference(superposition,[status(thm)],[c_24871,c_23291]) ).
tcf(c_25093,plain,
( ~ iPr_def_10
| ( multiply(identity,identity) != sk_c11 )
| ( multiply(inverse(identity),sk_c12) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_24903,c_745]) ).
tcf(c_25094,plain,
( ~ iPr_def_11
| ( multiply(identity,identity) != sk_c12 )
| ( multiply(inverse(identity),sk_c11) != sk_c12 ) ),
inference(superposition,[status(thm)],[c_24903,c_744]) ).
tcf(c_25097,plain,
( ~ iPr_def_11
| ( multiply(identity,identity) != sk_c12 )
| ( multiply(identity,sk_c11) != sk_c12 ) ),
inference(light_normalisation,[status(thm)],[c_25094,c_24903]) ).
tcf(c_25101,plain,
( ~ iPr_def_10
| ( multiply(identity,identity) != sk_c11 )
| ( multiply(identity,sk_c12) != sk_c11 ) ),
inference(light_normalisation,[status(thm)],[c_25093,c_24903]) ).
tcf(c_25184,plain,
( ( sk_c12 = iPr_def_30 )
| ~ iPr_def_13
| ( sk_c11 != iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_796,c_3404]) ).
tcf(c_25200,plain,
( ( sk_c12 = iPr_def_16 )
| ~ iPr_def_13
| ( sk_c11 != iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_746,c_3404]) ).
tcf(c_25274,plain,
( ( sk_c12 = iPr_def_30 )
| ~ iPr_def_13 ),
inference(global_subsumption_just,[status(thm)],[c_25184,c_15849,c_25184]) ).
tcf(c_25329,plain,
( ( iPr_def_28 = iPr_def_30 )
| ~ iPr_def_12
| ( sk_c12 != iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_3047,c_3574]) ).
tcf(c_25365,plain,
( ( sk_c12 = iPr_def_16 )
| ~ iPr_def_12
| ( sk_c12 != iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_751,c_3574]) ).
tcf(c_27320,plain,
( ( iPr_def_17 = sk_c11 )
| ( iPr_def_17 != iPr_def_15 )
| ( sk_c11 != iPr_def_15 ) ),
inference(instantiation,[status(thm)],[c_1682]) ).
tcf(c_28307,plain,
multiply(sk_c5,iPr_def_24) = identity,
inference(superposition,[status(thm)],[c_23579,c_114]) ).
tcf(c_28313,plain,
! [X0: $i] : multiply(sk_c5,multiply(iPr_def_24,X0)) = X0,
inference(superposition,[status(thm)],[c_23579,c_23274]) ).
tcf(c_28330,plain,
( ( identity = iPr_def_25 )
| ( sk_c12 = iPr_def_30 ) ),
inference(demodulation,[status(thm)],[c_3294,c_28307]) ).
tcf(c_28331,plain,
( ( identity = iPr_def_25 )
| ( sk_c2 = iPr_def_29 ) ),
inference(demodulation,[status(thm)],[c_2495,c_28307]) ).
tcf(c_28334,plain,
( ( identity = iPr_def_25 )
| ( sk_c4 = iPr_def_26 ) ),
inference(demodulation,[status(thm)],[c_1412,c_28307]) ).
tcf(c_30407,plain,
( ( identity = iPr_def_25 )
| ( multiply(sk_c1,iPr_def_29) = iPr_def_30 ) ),
inference(superposition,[status(thm)],[c_28331,c_738]) ).
tcf(c_30840,plain,
multiply(sk_c5,sk_c6) = iPr_def_25,
inference(superposition,[status(thm)],[c_9082,c_28313]) ).
tcf(c_31063,plain,
( ( identity = iPr_def_25 )
| ( multiply(sk_c12,iPr_def_26) = iPr_def_27 ) ),
inference(superposition,[status(thm)],[c_28334,c_735]) ).
tcf(c_35207,plain,
multiply(sk_c7,identity) = inverse(iPr_def_22),
inference(superposition,[status(thm)],[c_23580,c_24871]) ).
tcf(c_35246,plain,
inverse(iPr_def_22) = sk_c7,
inference(demodulation,[status(thm)],[c_35207,c_24871]) ).
tcf(c_35250,plain,
( ~ iPr_def_11
| ( multiply(iPr_def_22,sk_c7) != sk_c12 )
| ( multiply(inverse(iPr_def_22),sk_c11) != sk_c12 ) ),
inference(superposition,[status(thm)],[c_35246,c_744]) ).
tcf(c_35252,plain,
( ~ iPr_def_11
| ( sk_c12 != iPr_def_21 )
| ( sk_c12 != identity ) ),
inference(light_normalisation,[status(thm)],[c_35250,c_729,c_1382,c_35246]) ).
tcf(c_40049,plain,
multiply(sk_c8,iPr_def_19) = identity,
inference(superposition,[status(thm)],[c_23581,c_114]) ).
tcf(c_40072,plain,
( ( identity = iPr_def_20 )
| ( sk_c12 = iPr_def_30 ) ),
inference(demodulation,[status(thm)],[c_2898,c_40049]) ).
tcf(c_40074,plain,
( ( identity = iPr_def_20 )
| ( sk_c12 = iPr_def_28 ) ),
inference(demodulation,[status(thm)],[c_2088,c_40049]) ).
tcf(c_40075,plain,
( ( identity = iPr_def_20 )
| ( sk_c11 = iPr_def_27 ) ),
inference(demodulation,[status(thm)],[c_1548,c_40049]) ).
tcf(c_40076,plain,
( ( identity = iPr_def_20 )
| ( sk_c12 = iPr_def_16 ) ),
inference(demodulation,[status(thm)],[c_1298,c_40049]) ).
tcf(c_40077,plain,
( ( identity = iPr_def_20 )
| ( sk_c4 = iPr_def_26 ) ),
inference(demodulation,[status(thm)],[c_1297,c_40049]) ).
tcf(c_40513,plain,
( ( iPr_def_28 = iPr_def_30 )
| ( identity = iPr_def_20 ) ),
inference(superposition,[status(thm)],[c_40074,c_40072]) ).
tcf(c_41202,plain,
( ( identity = iPr_def_20 )
| ( multiply(iPr_def_16,sk_c4) = iPr_def_27 ) ),
inference(superposition,[status(thm)],[c_40076,c_735]) ).
tcf(c_42138,plain,
! [X0: $i] :
( ( multiply(X0,iPr_def_26) = multiply(sk_c12,sk_c4) )
| ( iPr_def_26 != sk_c4 )
| ( X0 != sk_c12 ) ),
inference(instantiation,[status(thm)],[c_8586]) ).
tcf(c_42139,plain,
( ( multiply(sk_c12,iPr_def_26) = multiply(sk_c12,sk_c4) )
| ( iPr_def_26 != sk_c4 )
| ( sk_c12 != sk_c12 ) ),
inference(instantiation,[status(thm)],[c_42138]) ).
tcf(c_42612,plain,
multiply(sk_c10,identity) = inverse(iPr_def_17),
inference(superposition,[status(thm)],[c_23582,c_24871]) ).
tcf(c_42823,plain,
inverse(iPr_def_17) = sk_c10,
inference(demodulation,[status(thm)],[c_42612,c_24871]) ).
tcf(c_42826,plain,
( ~ iPr_def_10
| ( multiply(iPr_def_17,sk_c10) != sk_c11 )
| ( multiply(inverse(iPr_def_17),sk_c12) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_42823,c_745]) ).
tcf(c_42833,plain,
( ~ iPr_def_10
| ( sk_c11 != iPr_def_15 )
| ( sk_c11 != identity ) ),
inference(light_normalisation,[status(thm)],[c_42826,c_723,c_1384,c_42823]) ).
tcf(c_42914,plain,
multiply(sk_c1,iPr_def_29) = identity,
inference(superposition,[status(thm)],[c_23583,c_114]) ).
tcf(c_42920,plain,
! [X0: $i] : multiply(sk_c1,multiply(iPr_def_29,X0)) = X0,
inference(superposition,[status(thm)],[c_23583,c_23274]) ).
tcf(c_42937,plain,
( ( identity = iPr_def_30 )
| ( identity = iPr_def_25 ) ),
inference(demodulation,[status(thm)],[c_30407,c_42914]) ).
tcf(c_42938,plain,
( ( identity = iPr_def_30 )
| ( sk_c12 = iPr_def_25 ) ),
inference(demodulation,[status(thm)],[c_2505,c_42914]) ).
tcf(c_42940,plain,
( ( identity = iPr_def_30 )
| ( sk_c12 = iPr_def_22 ) ),
inference(demodulation,[status(thm)],[c_2475,c_42914]) ).
tcf(c_42941,plain,
( ( identity = iPr_def_30 )
| ( sk_c12 = iPr_def_21 ) ),
inference(demodulation,[status(thm)],[c_2465,c_42914]) ).
tcf(c_43959,plain,
multiply(sk_c1,sk_c2) = iPr_def_30,
inference(superposition,[status(thm)],[c_8590,c_42920]) ).
tcf(c_44662,plain,
( ( identity = iPr_def_30 )
| ~ iPr_def_12
| ( sk_c12 != iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_42941,c_3574]) ).
tcf(c_46797,plain,
( ( identity = iPr_def_20 )
| ( multiply(iPr_def_16,iPr_def_26) = iPr_def_27 ) ),
inference(superposition,[status(thm)],[c_40077,c_41202]) ).
tcf(c_46810,plain,
( ( identity = iPr_def_20 )
| ( sk_c12 = iPr_def_27 ) ),
inference(light_normalisation,[status(thm)],[c_46797,c_8574]) ).
tcf(c_48852,plain,
( ( iPr_def_17 = iPr_def_18 )
| ( sk_c12 = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_748,c_747]) ).
tcf(c_49197,plain,
( ( sk_c12 = iPr_def_21 )
| ( multiply(sk_c12,iPr_def_26) = iPr_def_27 ) ),
inference(superposition,[status(thm)],[c_761,c_735]) ).
tcf(c_49613,plain,
multiply(iPr_def_16,sk_c3) = identity,
inference(superposition,[status(thm)],[c_724,c_114]) ).
tcf(c_50275,plain,
( ( iPr_def_15 = iPr_def_20 )
| ( sk_c12 = iPr_def_30 )
| ( sk_c12 = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_796,c_780]) ).
tcf(c_50927,plain,
( ~ iPr_def_13
| ( sk_c11 != iPr_def_15 )
| ( inverse(sk_c10) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_723,c_741]) ).
tcf(c_50952,plain,
( ~ iPr_def_13
| ( sk_c11 != iPr_def_17 )
| ( sk_c11 != iPr_def_15 ) ),
inference(light_normalisation,[status(thm)],[c_50927,c_725]) ).
tcf(c_51610,plain,
( ( iPr_def_17 = iPr_def_18 )
| ( iPr_def_16 = iPr_def_25 )
| ( sk_c12 = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_48852,c_755]) ).
tcf(c_52240,plain,
! [X0: $i] : multiply(iPr_def_16,multiply(sk_c3,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_49613,c_115]) ).
tcf(c_52241,plain,
! [X0: $i] : multiply(iPr_def_16,multiply(sk_c3,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_52240,c_113]) ).
tcf(c_54589,plain,
( ( multiply(sk_c8,iPr_def_19) = sk_c11 )
| ( sk_c11 != iPr_def_20 )
| ( multiply(sk_c8,iPr_def_19) != iPr_def_20 ) ),
inference(instantiation,[status(thm)],[c_1676]) ).
tcf(c_55556,plain,
( ( sk_c11 = multiply(sk_c12,sk_c4) )
| ( sk_c11 != iPr_def_27 )
| ( multiply(sk_c12,sk_c4) != iPr_def_27 ) ),
inference(instantiation,[status(thm)],[c_1968]) ).
tcf(c_57372,plain,
! [X0: $i] :
( ( multiply(iPr_def_19,X0) = sk_c11 )
| ( sk_c11 != iPr_def_18 )
| ( multiply(iPr_def_19,X0) != iPr_def_18 ) ),
inference(instantiation,[status(thm)],[c_1678]) ).
tcf(c_57375,plain,
( ( multiply(iPr_def_19,sk_c12) = sk_c11 )
| ( sk_c11 != iPr_def_18 )
| ( multiply(iPr_def_19,sk_c12) != iPr_def_18 ) ),
inference(instantiation,[status(thm)],[c_57372]) ).
tcf(c_58778,plain,
( ~ iPr_def_13
| ( sk_c11 != identity )
| ( sk_c12 != sk_c11 ) ),
inference(light_normalisation,[status(thm)],[c_3383,c_24903]) ).
tcf(c_58832,plain,
( ( sk_c11 = iPr_def_17 )
| ~ iPr_def_13
| ( sk_c11 != identity )
| ( sk_c12 != iPr_def_27 ) ),
inference(superposition,[status(thm)],[c_767,c_58778]) ).
tcf(c_58833,plain,
( ( sk_c11 = iPr_def_15 )
| ~ iPr_def_13
| ( sk_c11 != identity )
| ( sk_c12 != iPr_def_27 ) ),
inference(superposition,[status(thm)],[c_766,c_58778]) ).
tcf(c_58996,plain,
( ~ iPr_def_12
| ( sk_c12 != identity )
| ( sk_c12 != sk_c11 ) ),
inference(light_normalisation,[status(thm)],[c_3546,c_24903]) ).
tcf(c_59046,plain,
( ( sk_c12 = iPr_def_22 )
| ~ iPr_def_12
| ( sk_c12 != iPr_def_27 )
| ( sk_c12 != identity ) ),
inference(superposition,[status(thm)],[c_772,c_58996]) ).
tcf(c_59047,plain,
( ( sk_c12 = iPr_def_21 )
| ~ iPr_def_12
| ( sk_c12 != iPr_def_27 )
| ( sk_c12 != identity ) ),
inference(superposition,[status(thm)],[c_771,c_58996]) ).
tcf(c_59876,plain,
multiply(iPr_def_16,iPr_def_26) = sk_c12,
inference(superposition,[status(thm)],[c_734,c_52241]) ).
tcf(c_61810,plain,
( ( sk_c12 = iPr_def_21 )
| ( multiply(iPr_def_28,iPr_def_26) = iPr_def_27 ) ),
inference(superposition,[status(thm)],[c_781,c_49197]) ).
tcf(c_71015,plain,
! [X0: $i] :
( ( sk_c11 = identity )
| ( identity != X0 )
| ( sk_c11 != X0 ) ),
inference(instantiation,[status(thm)],[c_1494]) ).
tcf(c_71017,plain,
( ( sk_c11 = identity )
| ( identity != sk_c12 )
| ( sk_c11 != sk_c12 ) ),
inference(instantiation,[status(thm)],[c_71015]) ).
tcf(c_81889,plain,
! [X0: $i] :
( ( multiply(X0,iPr_def_26) = sk_c11 )
| ( sk_c11 != iPr_def_27 )
| ( multiply(X0,iPr_def_26) != iPr_def_27 ) ),
inference(instantiation,[status(thm)],[c_1967]) ).
tcf(c_81890,plain,
( ( multiply(sk_c12,iPr_def_26) = sk_c11 )
| ( sk_c11 != iPr_def_27 )
| ( multiply(sk_c12,iPr_def_26) != iPr_def_27 ) ),
inference(instantiation,[status(thm)],[c_81889]) ).
tcf(c_93684,plain,
( ( sk_c11 = identity )
| ( identity != iPr_def_20 )
| ( sk_c11 != iPr_def_20 ) ),
inference(instantiation,[status(thm)],[c_71015]) ).
tcf(c_98290,plain,
! [X0: $i] :
( ( sk_c12 = identity )
| ( identity != X0 )
| ( sk_c12 != X0 ) ),
inference(instantiation,[status(thm)],[c_807]) ).
tcf(c_98291,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( sk_c12 = multiply(X0,X1) )
| ( sk_c12 != X2 )
| ( multiply(X0,X1) != X2 ) ),
inference(instantiation,[status(thm)],[c_807]) ).
tcf(c_98307,plain,
! [X0: $i,X1: $i] :
( ( identity = X0 )
| ( identity != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_807]) ).
tcf(c_98332,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( multiply(X0,X1) = X3 )
| ( X3 != X2 )
| ( multiply(X0,X1) != X2 ) ),
inference(instantiation,[status(thm)],[c_807]) ).
tcf(c_98358,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = multiply(X0,sk_c11) )
| ( X2 != X1 )
| ( multiply(X0,sk_c11) != X1 ) ),
inference(instantiation,[status(thm)],[c_807]) ).
tcf(c_98361,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(X0,X2) = multiply(X1,sk_c11) )
| ( X2 != sk_c11 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_808]) ).
tcf(c_98373,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( inverse(X0) = X2 )
| ( X2 != X1 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_807]) ).
tcf(c_98385,plain,
! [X0: $i,X1: $i] :
( ( X0 = sk_c11 )
| ( sk_c11 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_807]) ).
tcf(c_98440,plain,
! [X0: $i,X1: $i] :
( ( multiply(identity,X0) = X1 )
| ( X1 != X0 )
| ( multiply(identity,X0) != X0 ) ),
inference(instantiation,[status(thm)],[c_98332]) ).
tcf(c_98448,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_98332]) ).
tcf(c_98481,plain,
! [X0: $i,X1: $i] :
( ( inverse(X0) = X1 )
| ( X1 != inverse(X0) )
| ( inverse(X0) != inverse(X0) ) ),
inference(instantiation,[status(thm)],[c_98373]) ).
tcf(c_98482,plain,
! [X0: $i] : inverse(X0) = inverse(X0),
inference(instantiation,[status(thm)],[c_806]) ).
tcf(c_98498,plain,
! [X0: $i,X1: $i] :
( ( X1 = multiply(identity,identity) )
| ( X1 != X0 )
| ( multiply(identity,identity) != X0 ) ),
inference(instantiation,[status(thm)],[c_807]) ).
tcf(c_98499,plain,
( ( sk_c12 = multiply(identity,identity) )
| ( sk_c12 != sk_c12 )
| ( multiply(identity,identity) != sk_c12 ) ),
inference(instantiation,[status(thm)],[c_98498]) ).
tcf(c_98542,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = inverse(X0) )
| ( X2 != X1 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_807]) ).
tcf(c_98728,plain,
! [X0: $i] :
( ( multiply(identity,X0) = sk_c11 )
| ( sk_c11 != X0 )
| ( multiply(identity,X0) != X0 ) ),
inference(instantiation,[status(thm)],[c_98440]) ).
tcf(c_98740,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(identity,X0) = X2 )
| ( X2 != X1 )
| ( multiply(identity,X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_98332]) ).
tcf(c_98762,plain,
! [X0: $i] :
( ( multiply(identity,sk_c11) = X0 )
| ( X0 != sk_c11 )
| ( multiply(identity,sk_c11) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_98440]) ).
tcf(c_98763,plain,
! [X0: $i,X1: $i] :
( ( X1 = multiply(identity,sk_c11) )
| ( X1 != X0 )
| ( multiply(identity,sk_c11) != X0 ) ),
inference(instantiation,[status(thm)],[c_98358]) ).
tcf(c_98811,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( X3 = multiply(X0,X1) )
| ( X3 != X2 )
| ( multiply(X0,X1) != X2 ) ),
inference(instantiation,[status(thm)],[c_807]) ).
tcf(c_98857,plain,
! [X0: $i,X1: $i] :
( ( multiply(X0,X1) = sk_c11 )
| ( sk_c11 != multiply(identity,sk_c11) )
| ( multiply(X0,X1) != multiply(identity,sk_c11) ) ),
inference(instantiation,[status(thm)],[c_98448]) ).
tcf(c_99006,plain,
( ( inverse(sk_c3) = iPr_def_16 )
| ( iPr_def_16 != inverse(sk_c3) )
| ( inverse(sk_c3) != inverse(sk_c3) ) ),
inference(instantiation,[status(thm)],[c_98481]) ).
tcf(c_99210,plain,
! [X0: $i] :
( ( multiply(identity,identity) = X0 )
| ( X0 != identity )
| ( multiply(identity,identity) != identity ) ),
inference(instantiation,[status(thm)],[c_98440]) ).
tcf(c_99211,plain,
( ( multiply(identity,identity) = sk_c12 )
| ( sk_c12 != identity )
| ( multiply(identity,identity) != identity ) ),
inference(instantiation,[status(thm)],[c_99210]) ).
tcf(c_99356,plain,
! [X0: $i,X1: $i] :
( ( multiply(X0,iPr_def_15) = multiply(X1,sk_c11) )
| ( iPr_def_15 != sk_c11 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_98361]) ).
tcf(c_99729,plain,
( ( sk_c12 = identity )
| ( identity != multiply(identity,identity) )
| ( sk_c12 != multiply(identity,identity) ) ),
inference(instantiation,[status(thm)],[c_98290]) ).
tcf(c_99730,plain,
! [X0: $i] :
( ( identity = X0 )
| ( identity != multiply(identity,identity) )
| ( X0 != multiply(identity,identity) ) ),
inference(instantiation,[status(thm)],[c_98307]) ).
tcf(c_99732,plain,
( ( identity = sk_c12 )
| ( identity != multiply(identity,identity) )
| ( sk_c12 != multiply(identity,identity) ) ),
inference(instantiation,[status(thm)],[c_99730]) ).
tcf(c_99977,plain,
! [X0: $i,X1: $i] :
( ( multiply(identity,X0) = sk_c11 )
| ( sk_c11 != X1 )
| ( multiply(identity,X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_98740]) ).
tcf(c_100034,plain,
! [X0: $i,X1: $i] :
( ( multiply(identity,identity) = X1 )
| ( X1 != X0 )
| ( multiply(identity,identity) != X0 ) ),
inference(instantiation,[status(thm)],[c_98740]) ).
tcf(c_100299,plain,
( ( sk_c12 = multiply(sk_c5,sk_c6) )
| ( sk_c12 != iPr_def_25 )
| ( multiply(sk_c5,sk_c6) != iPr_def_25 ) ),
inference(instantiation,[status(thm)],[c_98291]) ).
tcf(c_100314,plain,
! [X0: $i] :
( ( multiply(sk_c1,sk_c2) = X0 )
| ( X0 != iPr_def_30 )
| ( multiply(sk_c1,sk_c2) != iPr_def_30 ) ),
inference(instantiation,[status(thm)],[c_98332]) ).
tcf(c_100315,plain,
( ( sk_c12 = multiply(sk_c1,sk_c2) )
| ( sk_c12 != iPr_def_30 )
| ( multiply(sk_c1,sk_c2) != iPr_def_30 ) ),
inference(instantiation,[status(thm)],[c_98291]) ).
tcf(c_100750,plain,
! [X0: $i] :
( ( X0 = multiply(sk_c5,sk_c6) )
| ( X0 != iPr_def_25 )
| ( multiply(sk_c5,sk_c6) != iPr_def_25 ) ),
inference(instantiation,[status(thm)],[c_98811]) ).
tcf(c_100752,plain,
! [X0: $i] :
( ( X0 = multiply(sk_c1,sk_c2) )
| ( X0 != iPr_def_30 )
| ( multiply(sk_c1,sk_c2) != iPr_def_30 ) ),
inference(instantiation,[status(thm)],[c_98811]) ).
tcf(c_101235,plain,
! [X0: $i] :
( ( X0 = sk_c11 )
| ( sk_c11 != iPr_def_20 )
| ( X0 != iPr_def_20 ) ),
inference(instantiation,[status(thm)],[c_98385]) ).
tcf(c_101308,plain,
! [X0: $i] :
( ( multiply(X0,iPr_def_15) = multiply(identity,sk_c11) )
| ( iPr_def_15 != sk_c11 )
| ( X0 != identity ) ),
inference(instantiation,[status(thm)],[c_99356]) ).
tcf(c_101309,plain,
! [X0: $i] :
( ( multiply(X0,iPr_def_15) = sk_c11 )
| ( sk_c11 != multiply(identity,sk_c11) )
| ( multiply(X0,iPr_def_15) != multiply(identity,sk_c11) ) ),
inference(instantiation,[status(thm)],[c_98857]) ).
tcf(c_101310,plain,
( ( multiply(sk_c12,iPr_def_15) = multiply(identity,sk_c11) )
| ( iPr_def_15 != sk_c11 )
| ( sk_c12 != identity ) ),
inference(instantiation,[status(thm)],[c_101308]) ).
tcf(c_101311,plain,
( ( multiply(sk_c12,iPr_def_15) = sk_c11 )
| ( sk_c11 != multiply(identity,sk_c11) )
| ( multiply(sk_c12,iPr_def_15) != multiply(identity,sk_c11) ) ),
inference(instantiation,[status(thm)],[c_101309]) ).
tcf(c_101544,plain,
inverse(sk_c3) = inverse(sk_c3),
inference(instantiation,[status(thm)],[c_98482]) ).
tcf(c_101648,plain,
! [X0: $i,X1: $i] :
( ( multiply(X0,X1) = sk_c11 )
| ( sk_c11 != multiply(sk_c12,sk_c4) )
| ( multiply(X0,X1) != multiply(sk_c12,sk_c4) ) ),
inference(instantiation,[status(thm)],[c_98448]) ).
tcf(c_104298,plain,
( ( multiply(sk_c1,sk_c2) = identity )
| ( identity != iPr_def_30 )
| ( multiply(sk_c1,sk_c2) != iPr_def_30 ) ),
inference(instantiation,[status(thm)],[c_100314]) ).
tcf(c_104303,plain,
( ( multiply(identity,identity) = multiply(sk_c1,sk_c2) )
| ( multiply(identity,identity) != identity )
| ( multiply(sk_c1,sk_c2) != identity ) ),
inference(instantiation,[status(thm)],[c_99210]) ).
tcf(c_107498,plain,
! [X0: $i] :
( ( X0 = inverse(sk_c3) )
| ( X0 != iPr_def_16 )
| ( inverse(sk_c3) != iPr_def_16 ) ),
inference(instantiation,[status(thm)],[c_98542]) ).
tcf(c_107500,plain,
! [X0: $i] :
( ( inverse(sk_c3) = X0 )
| ( X0 != iPr_def_16 )
| ( inverse(sk_c3) != iPr_def_16 ) ),
inference(instantiation,[status(thm)],[c_98373]) ).
tcf(c_107503,plain,
( ( sk_c12 = inverse(sk_c3) )
| ( sk_c12 != iPr_def_16 )
| ( inverse(sk_c3) != iPr_def_16 ) ),
inference(instantiation,[status(thm)],[c_107498]) ).
tcf(c_113058,plain,
! [X0: $i] :
( ( X0 = multiply(identity,sk_c11) )
| ( X0 != inverse(sk_c3) )
| ( multiply(identity,sk_c11) != inverse(sk_c3) ) ),
inference(instantiation,[status(thm)],[c_98763]) ).
tcf(c_113059,plain,
( ( sk_c12 = multiply(identity,sk_c11) )
| ( sk_c12 != inverse(sk_c3) )
| ( multiply(identity,sk_c11) != inverse(sk_c3) ) ),
inference(instantiation,[status(thm)],[c_113058]) ).
tcf(c_113142,plain,
( ( inverse(sk_c3) = sk_c11 )
| ( sk_c11 != iPr_def_16 )
| ( inverse(sk_c3) != iPr_def_16 ) ),
inference(instantiation,[status(thm)],[c_107500]) ).
tcf(c_113145,plain,
( ( multiply(identity,sk_c11) = inverse(sk_c3) )
| ( inverse(sk_c3) != sk_c11 )
| ( multiply(identity,sk_c11) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_98762]) ).
tcf(c_118429,plain,
! [X0: $i] :
( ( multiply(identity,X0) = sk_c11 )
| ( sk_c11 != multiply(identity,multiply(identity,sk_c11)) )
| ( multiply(identity,X0) != multiply(identity,multiply(identity,sk_c11)) ) ),
inference(instantiation,[status(thm)],[c_99977]) ).
tcf(c_118430,plain,
( ( multiply(identity,sk_c12) = sk_c11 )
| ( sk_c11 != multiply(identity,multiply(identity,sk_c11)) )
| ( multiply(identity,sk_c12) != multiply(identity,multiply(identity,sk_c11)) ) ),
inference(instantiation,[status(thm)],[c_118429]) ).
tcf(c_121738,plain,
( ( identity = multiply(sk_c5,sk_c6) )
| ( identity != iPr_def_25 )
| ( multiply(sk_c5,sk_c6) != iPr_def_25 ) ),
inference(instantiation,[status(thm)],[c_100750]) ).
tcf(c_121742,plain,
( ( sk_c12 = identity )
| ( identity != multiply(sk_c5,sk_c6) )
| ( sk_c12 != multiply(sk_c5,sk_c6) ) ),
inference(instantiation,[status(thm)],[c_98290]) ).
tcf(c_122534,plain,
( ( identity = multiply(sk_c1,sk_c2) )
| ( identity != iPr_def_30 )
| ( multiply(sk_c1,sk_c2) != iPr_def_30 ) ),
inference(instantiation,[status(thm)],[c_100752]) ).
tcf(c_122538,plain,
( ( sk_c12 = identity )
| ( identity != multiply(sk_c1,sk_c2) )
| ( sk_c12 != multiply(sk_c1,sk_c2) ) ),
inference(instantiation,[status(thm)],[c_98290]) ).
tcf(c_122574,plain,
! [X0: $i] :
( ( multiply(identity,identity) = X0 )
| ( X0 != multiply(sk_c1,sk_c2) )
| ( multiply(identity,identity) != multiply(sk_c1,sk_c2) ) ),
inference(instantiation,[status(thm)],[c_100034]) ).
tcf(c_122578,plain,
( ( multiply(identity,identity) = sk_c12 )
| ( sk_c12 != multiply(sk_c1,sk_c2) )
| ( multiply(identity,identity) != multiply(sk_c1,sk_c2) ) ),
inference(instantiation,[status(thm)],[c_122574]) ).
tcf(c_133175,plain,
( ( multiply(identity,sk_c11) = identity )
| ( identity != sk_c11 )
| ( multiply(identity,sk_c11) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_98762]) ).
tcf(c_133200,plain,
( ( identity = sk_c11 )
| ( identity != iPr_def_20 )
| ( sk_c11 != iPr_def_20 ) ),
inference(instantiation,[status(thm)],[c_101235]) ).
tcf(c_134026,plain,
! [X0: $i] :
( ( multiply(X0,iPr_def_26) = sk_c11 )
| ( sk_c11 != multiply(sk_c12,sk_c4) )
| ( multiply(X0,iPr_def_26) != multiply(sk_c12,sk_c4) ) ),
inference(instantiation,[status(thm)],[c_101648]) ).
tcf(c_134028,plain,
( ( multiply(sk_c12,iPr_def_26) = sk_c11 )
| ( sk_c11 != multiply(sk_c12,sk_c4) )
| ( multiply(sk_c12,iPr_def_26) != multiply(sk_c12,sk_c4) ) ),
inference(instantiation,[status(thm)],[c_134026]) ).
tcf(c_134622,plain,
( ( multiply(identity,identity) = sk_c11 )
| ( sk_c11 != identity )
| ( multiply(identity,identity) != identity ) ),
inference(instantiation,[status(thm)],[c_98728]) ).
tcf(c_134631,plain,
! [X0: $i] :
( ( X0 = multiply(identity,sk_c11) )
| ( X0 != identity )
| ( multiply(identity,sk_c11) != identity ) ),
inference(instantiation,[status(thm)],[c_98763]) ).
tcf(c_134633,plain,
( ( sk_c12 = multiply(identity,sk_c11) )
| ( sk_c12 != identity )
| ( multiply(identity,sk_c11) != identity ) ),
inference(instantiation,[status(thm)],[c_134631]) ).
tcf(c_134742,plain,
sk_c12 = iPr_def_30,
inference(global_subsumption_just,[status(thm)],[c_50275,c_739,c_723,c_725,c_1496,c_1501,c_1502,c_2399,c_2440,c_2899,c_2898,c_3362,c_3574,c_3767,c_3854,c_3972,c_5714,c_5976,c_15607,c_15849,c_15895,c_16079,c_16147,c_16503,c_17169,c_25274,c_28330,c_30840,c_35252,c_40072,c_54589,c_57375,c_100299,c_101310,c_101311,c_121738,c_121742,c_133175,c_133200,c_134633]) ).
tcf(c_134762,plain,
( ( iPr_def_21 = iPr_def_30 )
| ( multiply(iPr_def_28,iPr_def_26) = iPr_def_27 ) ),
inference(demodulation,[status(thm)],[c_61810,c_134742]) ).
tcf(c_134883,plain,
multiply(iPr_def_16,iPr_def_26) = iPr_def_30,
inference(demodulation,[status(thm)],[c_59876,c_134742]) ).
tcf(c_134944,plain,
( ( iPr_def_28 = iPr_def_30 )
| ( iPr_def_25 = iPr_def_30 ) ),
inference(demodulation,[status(thm)],[c_785,c_134742]) ).
tcf(c_134949,plain,
( ( iPr_def_28 = iPr_def_30 )
| ( sk_c11 = iPr_def_20 ) ),
inference(demodulation,[status(thm)],[c_780,c_134742]) ).
tcf(c_134954,plain,
( ( iPr_def_28 = iPr_def_30 )
| ( sk_c11 = iPr_def_17 ) ),
inference(demodulation,[status(thm)],[c_777,c_134742]) ).
tcf(c_134955,plain,
( ( iPr_def_28 = iPr_def_30 )
| ( sk_c11 = iPr_def_15 ) ),
inference(demodulation,[status(thm)],[c_776,c_134742]) ).
tcf(c_134956,plain,
( ( iPr_def_25 = iPr_def_30 )
| ( sk_c11 = iPr_def_27 ) ),
inference(demodulation,[status(thm)],[c_775,c_134742]) ).
tcf(c_134962,plain,
multiply(iPr_def_30,sk_c4) = iPr_def_27,
inference(demodulation,[status(thm)],[c_735,c_134742]) ).
tcf(c_135468,plain,
iPr_def_28 = iPr_def_30,
inference(global_subsumption_just,[status(thm)],[c_134944,c_812,c_739,c_723,c_725,c_1496,c_1501,c_1502,c_2195,c_2200,c_2399,c_2440,c_2899,c_2898,c_3047,c_3149,c_3362,c_3404,c_3574,c_3767,c_3854,c_3972,c_5714,c_5976,c_6516,c_7453,c_15607,c_15849,c_15895,c_16079,c_16147,c_16503,c_17169,c_24441,c_25274,c_25329,c_27320,c_28330,c_30840,c_35252,c_40072,c_40513,c_42833,c_42938,c_42937,c_43959,c_54589,c_57375,c_93684,c_98499,c_99211,c_99729,c_100299,c_100315,c_101310,c_101311,c_104298,c_104303,c_121738,c_121742,c_122578,c_133175,c_133200,c_134633,c_134955,c_134954,c_134949]) ).
tcf(c_135471,plain,
multiply(iPr_def_28,sk_c4) = iPr_def_27,
inference(demodulation,[status(thm)],[c_134962,c_135468]) ).
tcf(c_135473,plain,
multiply(iPr_def_16,iPr_def_26) = iPr_def_28,
inference(demodulation,[status(thm)],[c_134883,c_135468]) ).
tcf(c_135474,plain,
sk_c12 = iPr_def_28,
inference(demodulation,[status(thm)],[c_134742,c_135468]) ).
tcf(c_135559,plain,
sk_c11 = iPr_def_27,
inference(global_subsumption_just,[status(thm)],[c_134956,c_812,c_739,c_723,c_725,c_1496,c_1501,c_1502,c_1549,c_1548,c_2195,c_2200,c_2399,c_2440,c_3362,c_3404,c_3574,c_3767,c_3854,c_3972,c_5714,c_5976,c_11238,c_11316,c_11539,c_11971,c_12037,c_12093,c_24441,c_30840,c_35252,c_40075,c_42938,c_42937,c_43959,c_54589,c_57375,c_98499,c_99211,c_99729,c_100299,c_100315,c_101310,c_101311,c_104298,c_104303,c_121738,c_121742,c_122578,c_133175,c_133200,c_134633,c_134742]) ).
tcf(c_135590,plain,
( ( iPr_def_20 = iPr_def_27 )
| ( sk_c4 = iPr_def_26 ) ),
inference(demodulation,[status(thm)],[c_760,c_135559]) ).
tcf(c_136321,plain,
( ( iPr_def_20 = iPr_def_27 )
| ( multiply(iPr_def_28,iPr_def_26) = iPr_def_27 ) ),
inference(superposition,[status(thm)],[c_135590,c_135471]) ).
tcf(c_136993,plain,
( ~ iPr_def_13
| ( sk_c11 != iPr_def_17 ) ),
inference(global_subsumption_just,[status(thm)],[c_50952,c_812,c_739,c_723,c_725,c_1496,c_1501,c_1502,c_1549,c_1548,c_1971,c_2195,c_2200,c_2399,c_2440,c_2899,c_2898,c_3362,c_3404,c_3574,c_3767,c_3854,c_3972,c_5714,c_5976,c_7455,c_10147,c_11238,c_11316,c_11539,c_11971,c_12037,c_12093,c_15607,c_15849,c_15895,c_16079,c_16147,c_16503,c_17169,c_24441,c_25274,c_28330,c_30840,c_35252,c_40075,c_40072,c_42938,c_42937,c_43959,c_54589,c_57375,c_58833,c_71017,c_98499,c_99211,c_99729,c_99732,c_100299,c_100315,c_101310,c_101311,c_104298,c_104303,c_121738,c_121742,c_122578,c_133175,c_133200,c_134633]) ).
tcf(c_137077,plain,
sk_c12 = iPr_def_16,
inference(global_subsumption_just,[status(thm)],[c_51610,c_812,c_739,c_723,c_725,c_1167,c_1221,c_1298,c_1496,c_1501,c_1502,c_2195,c_2200,c_2399,c_2440,c_2899,c_2898,c_3362,c_3574,c_3767,c_3854,c_3972,c_5714,c_5976,c_7454,c_7453,c_9196,c_9208,c_11488,c_13821,c_15607,c_15849,c_15895,c_16079,c_16147,c_16503,c_16637,c_17169,c_18435,c_24441,c_25200,c_25274,c_25365,c_27320,c_28330,c_30840,c_35252,c_40076,c_40072,c_42938,c_42937,c_43959,c_54589,c_57375,c_98499,c_99211,c_99729,c_100299,c_100315,c_101310,c_101311,c_104298,c_104303,c_121738,c_121742,c_122578,c_133175,c_133200,c_134633]) ).
tcf(c_137079,plain,
iPr_def_16 = iPr_def_28,
inference(demodulation,[status(thm)],[c_135474,c_137077]) ).
tcf(c_137083,plain,
multiply(iPr_def_16,iPr_def_26) = iPr_def_16,
inference(demodulation,[status(thm)],[c_135473,c_137079]) ).
tcf(c_137286,plain,
multiply(iPr_def_28,iPr_def_26) = iPr_def_27,
inference(global_subsumption_just,[status(thm)],[c_134762,c_812,c_739,c_723,c_725,c_735,c_756,c_757,c_1422,c_1496,c_1501,c_1502,c_1549,c_1548,c_1672,c_1686,c_1950,c_1951,c_2195,c_2200,c_2242,c_2243,c_2399,c_2440,c_2840,c_2839,c_2884,c_2899,c_2898,c_3362,c_3404,c_3574,c_3767,c_3763,c_3854,c_3972,c_4565,c_5714,c_5837,c_5976,c_6476,c_7968,c_8271,c_8373,c_8581,c_8582,c_11238,c_11316,c_11539,c_11971,c_12037,c_12093,c_15607,c_15849,c_15895,c_16079,c_16147,c_16503,c_17169,c_24441,c_25101,c_25097,c_25274,c_28330,c_30840,c_31063,c_35252,c_40075,c_40072,c_42139,c_42940,c_42938,c_42937,c_43959,c_44662,c_46810,c_54589,c_55556,c_57375,c_58832,c_59047,c_59046,c_71017,c_81890,c_98499,c_99211,c_99729,c_99732,c_100299,c_100315,c_101310,c_101311,c_104298,c_104303,c_118430,c_121738,c_121742,c_122534,c_122538,c_122578,c_133175,c_133200,c_134028,c_134622,c_134633,c_136321,c_136993,c_137077]) ).
tcf(c_137288,plain,
iPr_def_16 = iPr_def_27,
inference(light_normalisation,[status(thm)],[c_137286,c_137079,c_137083]) ).
tcf(c_137302,plain,
sk_c11 = iPr_def_16,
inference(demodulation,[status(thm)],[c_135559,c_137288]) ).
tcf(c_137846,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_137302,c_137077,c_136993,c_135559,c_134742,c_134622,c_134028,c_122578,c_122538,c_122534,c_121742,c_121738,c_118430,c_113145,c_113142,c_113059,c_107503,c_104303,c_104298,c_101544,c_101311,c_101310,c_100315,c_100299,c_99732,c_99211,c_99006,c_98499,c_81890,c_71017,c_59046,c_59047,c_58832,c_55556,c_44662,c_43959,c_42937,c_42938,c_42940,c_42139,c_31063,c_30840,c_25097,c_25101,c_24441,c_8582,c_8581,c_8271,c_5837,c_4565,c_3763,c_3767,c_3574,c_2884,c_2839,c_2840,c_2243,c_2242,c_2200,c_2195,c_1951,c_1950,c_1686,c_1672,c_1502,c_1501,c_1496,c_1422,c_757,c_756,c_735,c_724,c_739,c_812]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : GRP208-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.07 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.17/0.43 % Computer : n014.cluster.edu
% 0.17/0.43 % Model : x86_64 x86_64
% 0.17/0.43 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.43 % Memory : 8046.5625MB
% 0.17/0.43 % OS : Linux 6.8.0-71-generic
% 0.17/0.44 % CPULimit : 300
% 0.17/0.44 % WCLimit : 300
% 0.17/0.44 % DateTime : Wed Sep 23 14:08:19 UTC 2026
% 0.17/0.44 % CPUTime :
% 0.17/0.44 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.25/0.50 Running first-order theorem proving
% 0.25/0.50 Running: /export/starexec/sandbox2/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.25/0.51
% 0.25/0.51 % ======== iProver multi-core TPTP/SMT =========
% 0.25/0.51
% 0.25/0.51 % Detected problem language: tptp
% 0.25/0.53 % Proving...
% 17.74/5.41 % SZS status Started for theBenchmark.p
% 17.74/5.41 % SZS status Unsatisfiable for theBenchmark.p
% 17.74/5.41
% 17.74/5.41 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 17.74/5.41
% 17.74/5.41 % ------ iProver source info
% 17.74/5.41
% 17.74/5.41 % git: date: 2026-07-19 20:42:38 +0200
% 17.74/5.41 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 17.74/5.41 % git: non_committed_changes: false
% 17.74/5.41
% 17.74/5.41 % ------ Parsing...% successful
% 17.74/5.41
% 17.74/5.41
% 17.74/5.41 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 17.74/5.41
% 17.74/5.41 % ------ Preprocessing... sup_sim: 0 sf_s rm: 0 0s sf_e pe_s pe_e %
% 17.74/5.41
% 17.74/5.41 % ------ Preprocessing... gs_s sp: 6 0s gs_e snvd_s sp: 0 0s snvd_e %
% 17.74/5.41
% 17.74/5.41 % ------ Preprocessing... sf_s rm: 0 0s sf_e
% 17.74/5.41 % ------ Proving...
% 17.74/5.41 % ------ Problem Properties
% 17.74/5.41
% 17.74/5.41 %
% 17.74/5.41 % clauses 85
% 17.74/5.41 % conjectures 66
% 17.74/5.41 % EPR 61
% 17.74/5.41 % Horn 24
% 17.74/5.41 % unary 19
% 17.74/5.41 % binary 60
% 17.74/5.41 % lits 159
% 17.74/5.41 % lits eq 149
% 17.74/5.41 % fd_pure 0
% 17.74/5.41 % fd_pseudo 0
% 17.74/5.41 % fd_cond 0
% 17.74/5.41 % fd_pseudo_cond 0
% 17.74/5.41 % AC symbols 0
% 17.74/5.41
% 17.74/5.41 % ------ Schedule dynamic 5 is on
% 17.74/5.41
% 17.74/5.41 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 17.74/5.41
% 17.74/5.41
% 17.74/5.41 % ------
% 17.74/5.41 % Current options:
% 17.74/5.41 % ------
% 17.74/5.41
% 17.74/5.41
% 17.74/5.41 %
% 17.74/5.41
% 17.74/5.41 % ------ Proving...
% 17.74/5.41 %
% 17.74/5.41
% 17.74/5.41 % SZS status Unsatisfiable for theBenchmark.p
% 17.74/5.41
% 17.74/5.41 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 17.74/5.43
% 17.74/5.43
%------------------------------------------------------------------------------