%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : GRP375-1 : TPTP v9.3.1. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% Computer : n026.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 01:33:26 PM UTC 2026
% Result : Unsatisfiable 26.35s 6.00s
% Output : CNFRefutation 27.25s
% Verified :
% SZS Type : Refutation
% Derivation depth : 46
% Number of leaves : 57
% Syntax : Number of formulae : 810 ( 162 unt; 13 def)
% Number of atoms : 3375 (1690 equ)
% Maximal formula atoms : 14 ( 4 avg)
% Number of connectives : 1576 ( 575 ~;1001 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 22 ( 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 : 19 ( 17 usr; 18 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 11 con; 0-2 aty)
% Number of variables : 252 ( 0 sgn 252 !; 0 ?; 221 :)
% 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_c2,sk_c10) = sk_c9
| inverse(sk_c10) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_1) ).
fof(f6,plain,
( sk_c9 = multiply(sk_c2,sk_c10)
| inverse(sk_c10) = sk_c9 ),
inference(reorient_equations,[],[f5]) ).
fof(f7,negated_conjecture,
( inverse(sk_c2) = sk_c10
| inverse(sk_c10) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_2) ).
fof(f8,plain,
( sk_c10 = inverse(sk_c2)
| inverse(sk_c10) = sk_c9 ),
inference(reorient_equations,[],[f7]) ).
fof(f9,negated_conjecture,
( multiply(sk_c3,sk_c9) = sk_c8
| inverse(sk_c10) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_3) ).
fof(f10,negated_conjecture,
( inverse(sk_c3) = sk_c9
| inverse(sk_c10) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_4) ).
fof(f11,plain,
( sk_c9 = inverse(sk_c3)
| inverse(sk_c10) = sk_c9 ),
inference(reorient_equations,[],[f10]) ).
fof(f12,negated_conjecture,
( multiply(sk_c4,sk_c7) = sk_c10
| inverse(sk_c10) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_5) ).
fof(f13,plain,
( sk_c10 = multiply(sk_c4,sk_c7)
| inverse(sk_c10) = sk_c9 ),
inference(reorient_equations,[],[f12]) ).
fof(f14,negated_conjecture,
( inverse(sk_c4) = sk_c7
| inverse(sk_c10) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_6) ).
fof(f15,plain,
( sk_c7 = inverse(sk_c4)
| inverse(sk_c10) = sk_c9 ),
inference(reorient_equations,[],[f14]) ).
fof(f16,negated_conjecture,
( multiply(sk_c7,sk_c9) = sk_c10
| inverse(sk_c10) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_7) ).
fof(f17,plain,
( sk_c10 = multiply(sk_c7,sk_c9)
| inverse(sk_c10) = sk_c9 ),
inference(reorient_equations,[],[f16]) ).
fof(f18,negated_conjecture,
( inverse(sk_c6) = sk_c5
| inverse(sk_c10) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_8) ).
fof(f21,negated_conjecture,
( multiply(sk_c6,sk_c7) = sk_c5
| inverse(sk_c10) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_10) ).
fof(f22,plain,
( sk_c5 = multiply(sk_c6,sk_c7)
| inverse(sk_c10) = sk_c9 ),
inference(reorient_equations,[],[f21]) ).
fof(f23,negated_conjecture,
( multiply(sk_c2,sk_c10) = sk_c9
| multiply(sk_c1,sk_c10) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_11) ).
fof(f24,plain,
( sk_c9 = multiply(sk_c2,sk_c10)
| sk_c9 = multiply(sk_c1,sk_c10) ),
inference(reorient_equations,[],[f23]) ).
fof(f25,negated_conjecture,
( inverse(sk_c2) = sk_c10
| multiply(sk_c1,sk_c10) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_12) ).
fof(f26,plain,
( sk_c10 = inverse(sk_c2)
| sk_c9 = multiply(sk_c1,sk_c10) ),
inference(reorient_equations,[],[f25]) ).
fof(f27,negated_conjecture,
( multiply(sk_c3,sk_c9) = sk_c8
| multiply(sk_c1,sk_c10) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_13) ).
fof(f28,plain,
( multiply(sk_c3,sk_c9) = sk_c8
| sk_c9 = multiply(sk_c1,sk_c10) ),
inference(reorient_equations,[],[f27]) ).
fof(f29,negated_conjecture,
( inverse(sk_c3) = sk_c9
| multiply(sk_c1,sk_c10) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_14) ).
fof(f30,plain,
( sk_c9 = inverse(sk_c3)
| sk_c9 = multiply(sk_c1,sk_c10) ),
inference(reorient_equations,[],[f29]) ).
fof(f31,negated_conjecture,
( multiply(sk_c4,sk_c7) = sk_c10
| multiply(sk_c1,sk_c10) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_15) ).
fof(f32,plain,
( sk_c10 = multiply(sk_c4,sk_c7)
| sk_c9 = multiply(sk_c1,sk_c10) ),
inference(reorient_equations,[],[f31]) ).
fof(f33,negated_conjecture,
( inverse(sk_c4) = sk_c7
| multiply(sk_c1,sk_c10) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_16) ).
fof(f34,plain,
( sk_c7 = inverse(sk_c4)
| sk_c9 = multiply(sk_c1,sk_c10) ),
inference(reorient_equations,[],[f33]) ).
fof(f35,negated_conjecture,
( multiply(sk_c7,sk_c9) = sk_c10
| multiply(sk_c1,sk_c10) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_17) ).
fof(f36,plain,
( sk_c10 = multiply(sk_c7,sk_c9)
| sk_c9 = multiply(sk_c1,sk_c10) ),
inference(reorient_equations,[],[f35]) ).
fof(f37,negated_conjecture,
( inverse(sk_c6) = sk_c5
| multiply(sk_c1,sk_c10) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_18) ).
fof(f38,plain,
( inverse(sk_c6) = sk_c5
| sk_c9 = multiply(sk_c1,sk_c10) ),
inference(reorient_equations,[],[f37]) ).
fof(f39,negated_conjecture,
( inverse(sk_c5) = sk_c7
| multiply(sk_c1,sk_c10) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_19) ).
fof(f40,plain,
( sk_c7 = inverse(sk_c5)
| sk_c9 = multiply(sk_c1,sk_c10) ),
inference(reorient_equations,[],[f39]) ).
fof(f41,negated_conjecture,
( multiply(sk_c6,sk_c7) = sk_c5
| multiply(sk_c1,sk_c10) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_20) ).
fof(f42,plain,
( sk_c5 = multiply(sk_c6,sk_c7)
| sk_c9 = multiply(sk_c1,sk_c10) ),
inference(reorient_equations,[],[f41]) ).
fof(f43,negated_conjecture,
( multiply(sk_c2,sk_c10) = sk_c9
| inverse(sk_c1) = sk_c10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_21) ).
fof(f44,plain,
( sk_c9 = multiply(sk_c2,sk_c10)
| sk_c10 = inverse(sk_c1) ),
inference(reorient_equations,[],[f43]) ).
fof(f45,negated_conjecture,
( inverse(sk_c2) = sk_c10
| inverse(sk_c1) = sk_c10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_22) ).
fof(f46,plain,
( sk_c10 = inverse(sk_c2)
| sk_c10 = inverse(sk_c1) ),
inference(reorient_equations,[],[f45]) ).
fof(f47,negated_conjecture,
( multiply(sk_c3,sk_c9) = sk_c8
| inverse(sk_c1) = sk_c10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_23) ).
fof(f48,plain,
( multiply(sk_c3,sk_c9) = sk_c8
| sk_c10 = inverse(sk_c1) ),
inference(reorient_equations,[],[f47]) ).
fof(f49,negated_conjecture,
( inverse(sk_c3) = sk_c9
| inverse(sk_c1) = sk_c10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_24) ).
fof(f50,plain,
( sk_c9 = inverse(sk_c3)
| sk_c10 = inverse(sk_c1) ),
inference(reorient_equations,[],[f49]) ).
fof(f51,negated_conjecture,
( multiply(sk_c4,sk_c7) = sk_c10
| inverse(sk_c1) = sk_c10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_25) ).
fof(f52,plain,
( sk_c10 = multiply(sk_c4,sk_c7)
| sk_c10 = inverse(sk_c1) ),
inference(reorient_equations,[],[f51]) ).
fof(f53,negated_conjecture,
( inverse(sk_c4) = sk_c7
| inverse(sk_c1) = sk_c10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_26) ).
fof(f54,plain,
( sk_c7 = inverse(sk_c4)
| sk_c10 = inverse(sk_c1) ),
inference(reorient_equations,[],[f53]) ).
fof(f55,negated_conjecture,
( multiply(sk_c7,sk_c9) = sk_c10
| inverse(sk_c1) = sk_c10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_27) ).
fof(f56,plain,
( sk_c10 = multiply(sk_c7,sk_c9)
| sk_c10 = inverse(sk_c1) ),
inference(reorient_equations,[],[f55]) ).
fof(f57,negated_conjecture,
( inverse(sk_c6) = sk_c5
| inverse(sk_c1) = sk_c10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_28) ).
fof(f58,plain,
( inverse(sk_c6) = sk_c5
| sk_c10 = inverse(sk_c1) ),
inference(reorient_equations,[],[f57]) ).
fof(f61,negated_conjecture,
( multiply(sk_c6,sk_c7) = sk_c5
| inverse(sk_c1) = sk_c10 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_30) ).
fof(f62,plain,
( sk_c5 = multiply(sk_c6,sk_c7)
| sk_c10 = inverse(sk_c1) ),
inference(reorient_equations,[],[f61]) ).
fof(f63,negated_conjecture,
( multiply(sk_c2,sk_c10) = sk_c9
| multiply(sk_c8,sk_c10) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_31) ).
fof(f64,plain,
( sk_c9 = multiply(sk_c2,sk_c10)
| sk_c9 = multiply(sk_c8,sk_c10) ),
inference(reorient_equations,[],[f63]) ).
fof(f65,negated_conjecture,
( inverse(sk_c2) = sk_c10
| multiply(sk_c8,sk_c10) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_32) ).
fof(f66,plain,
( sk_c10 = inverse(sk_c2)
| sk_c9 = multiply(sk_c8,sk_c10) ),
inference(reorient_equations,[],[f65]) ).
fof(f67,negated_conjecture,
( multiply(sk_c3,sk_c9) = sk_c8
| multiply(sk_c8,sk_c10) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_33) ).
fof(f68,plain,
( multiply(sk_c3,sk_c9) = sk_c8
| sk_c9 = multiply(sk_c8,sk_c10) ),
inference(reorient_equations,[],[f67]) ).
fof(f69,negated_conjecture,
( inverse(sk_c3) = sk_c9
| multiply(sk_c8,sk_c10) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_34) ).
fof(f70,plain,
( sk_c9 = inverse(sk_c3)
| sk_c9 = multiply(sk_c8,sk_c10) ),
inference(reorient_equations,[],[f69]) ).
fof(f71,negated_conjecture,
( multiply(sk_c4,sk_c7) = sk_c10
| multiply(sk_c8,sk_c10) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_35) ).
fof(f72,plain,
( sk_c10 = multiply(sk_c4,sk_c7)
| sk_c9 = multiply(sk_c8,sk_c10) ),
inference(reorient_equations,[],[f71]) ).
fof(f73,negated_conjecture,
( inverse(sk_c4) = sk_c7
| multiply(sk_c8,sk_c10) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_36) ).
fof(f74,plain,
( sk_c7 = inverse(sk_c4)
| sk_c9 = multiply(sk_c8,sk_c10) ),
inference(reorient_equations,[],[f73]) ).
fof(f75,negated_conjecture,
( multiply(sk_c7,sk_c9) = sk_c10
| multiply(sk_c8,sk_c10) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_37) ).
fof(f76,plain,
( sk_c10 = multiply(sk_c7,sk_c9)
| sk_c9 = multiply(sk_c8,sk_c10) ),
inference(reorient_equations,[],[f75]) ).
fof(f77,negated_conjecture,
( inverse(sk_c6) = sk_c5
| multiply(sk_c8,sk_c10) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_38) ).
fof(f78,plain,
( inverse(sk_c6) = sk_c5
| sk_c9 = multiply(sk_c8,sk_c10) ),
inference(reorient_equations,[],[f77]) ).
fof(f81,negated_conjecture,
( multiply(sk_c6,sk_c7) = sk_c5
| multiply(sk_c8,sk_c10) = sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_40) ).
fof(f82,plain,
( sk_c5 = multiply(sk_c6,sk_c7)
| sk_c9 = multiply(sk_c8,sk_c10) ),
inference(reorient_equations,[],[f81]) ).
fof(f83,negated_conjecture,
! [X2,X3,X0,X1,X6,X4,X5] :
( multiply(X5,X4) != X6
| inverse(X6) != X4
| inverse(X5) != X6
| multiply(X4,sk_c9) != sk_c10
| inverse(X3) != X4
| multiply(X3,X4) != sk_c10
| inverse(X2) != sk_c9
| multiply(X2,sk_c9) != sk_c8
| inverse(X1) != sk_c10
| multiply(X1,sk_c10) != sk_c9
| multiply(sk_c8,sk_c10) != sk_c9
| inverse(X0) != sk_c10
| multiply(X0,sk_c10) != sk_c9
| inverse(sk_c10) != sk_c9 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_this_41) ).
fof(f84,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( multiply(X5,X4) != X6
| inverse(X6) != X4
| inverse(X5) != X6
| sk_c10 != multiply(X4,sk_c9)
| inverse(X3) != X4
| sk_c10 != multiply(X3,X4)
| sk_c9 != inverse(X2)
| sk_c8 != multiply(X2,sk_c9)
| sk_c10 != inverse(X1)
| sk_c9 != multiply(X1,sk_c10)
| sk_c9 != multiply(sk_c8,sk_c10)
| inverse(X0) != sk_c10
| sk_c9 != multiply(X0,sk_c10)
| inverse(sk_c10) != sk_c9 ),
inference(reorient_equations,[],[f83]) ).
fof(f85,plain,
! [X2,X3,X0,X1,X6,X5] :
( multiply(X5,inverse(X3)) != X6
| inverse(X3) != inverse(X6)
| inverse(X5) != X6
| sk_c10 != multiply(inverse(X3),sk_c9)
| sk_c10 != multiply(X3,inverse(X3))
| sk_c9 != inverse(X2)
| sk_c8 != multiply(X2,sk_c9)
| sk_c10 != inverse(X1)
| sk_c9 != multiply(X1,sk_c10)
| sk_c9 != multiply(sk_c8,sk_c10)
| inverse(X0) != sk_c10
| sk_c9 != multiply(X0,sk_c10)
| inverse(sk_c10) != sk_c9 ),
inference(equality_resolution,[],[f84]) ).
fof(f86,plain,
! [X2,X3,X0,X1,X5] :
( inverse(X5) != multiply(X5,inverse(X3))
| inverse(X3) != inverse(inverse(X5))
| sk_c10 != multiply(inverse(X3),sk_c9)
| sk_c10 != multiply(X3,inverse(X3))
| sk_c9 != inverse(X2)
| sk_c8 != multiply(X2,sk_c9)
| sk_c10 != inverse(X1)
| sk_c9 != multiply(X1,sk_c10)
| sk_c9 != multiply(sk_c8,sk_c10)
| inverse(X0) != sk_c10
| sk_c9 != multiply(X0,sk_c10)
| inverse(sk_c10) != sk_c9 ),
inference(equality_resolution,[],[f85]) ).
tcf(c_93,plain,
! [X0: $i] : multiply(identity,X0) = X0,
inference(cnf_transformation,[],[f1]) ).
tcf(c_94,plain,
! [X0: $i] : multiply(inverse(X0),X0) = identity,
inference(cnf_transformation,[],[f3]) ).
tcf(c_95,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(multiply(X0,X1),X2) = multiply(X0,multiply(X1,X2)),
inference(cnf_transformation,[],[f4]) ).
tcf(c_96,negated_conjecture,
( ( inverse(sk_c10) = sk_c9 )
| ( multiply(sk_c2,sk_c10) = sk_c9 ) ),
inference(cnf_transformation,[],[f6]) ).
tcf(c_97,negated_conjecture,
( ( inverse(sk_c2) = sk_c10 )
| ( inverse(sk_c10) = sk_c9 ) ),
inference(cnf_transformation,[],[f8]) ).
tcf(c_98,negated_conjecture,
( ( inverse(sk_c10) = sk_c9 )
| ( multiply(sk_c3,sk_c9) = sk_c8 ) ),
inference(cnf_transformation,[],[f9]) ).
tcf(c_99,negated_conjecture,
( ( inverse(sk_c3) = sk_c9 )
| ( inverse(sk_c10) = sk_c9 ) ),
inference(cnf_transformation,[],[f11]) ).
tcf(c_100,negated_conjecture,
( ( inverse(sk_c10) = sk_c9 )
| ( multiply(sk_c4,sk_c7) = sk_c10 ) ),
inference(cnf_transformation,[],[f13]) ).
tcf(c_101,negated_conjecture,
( ( inverse(sk_c4) = sk_c7 )
| ( inverse(sk_c10) = sk_c9 ) ),
inference(cnf_transformation,[],[f15]) ).
tcf(c_102,negated_conjecture,
( ( inverse(sk_c10) = sk_c9 )
| ( multiply(sk_c7,sk_c9) = sk_c10 ) ),
inference(cnf_transformation,[],[f17]) ).
tcf(c_103,negated_conjecture,
( ( inverse(sk_c6) = sk_c5 )
| ( inverse(sk_c10) = sk_c9 ) ),
inference(cnf_transformation,[],[f18]) ).
tcf(c_105,negated_conjecture,
( ( inverse(sk_c10) = sk_c9 )
| ( multiply(sk_c6,sk_c7) = sk_c5 ) ),
inference(cnf_transformation,[],[f22]) ).
tcf(c_106,negated_conjecture,
( ( multiply(sk_c1,sk_c10) = sk_c9 )
| ( multiply(sk_c2,sk_c10) = sk_c9 ) ),
inference(cnf_transformation,[],[f24]) ).
tcf(c_107,negated_conjecture,
( ( inverse(sk_c2) = sk_c10 )
| ( multiply(sk_c1,sk_c10) = sk_c9 ) ),
inference(cnf_transformation,[],[f26]) ).
tcf(c_108,negated_conjecture,
( ( multiply(sk_c1,sk_c10) = sk_c9 )
| ( multiply(sk_c3,sk_c9) = sk_c8 ) ),
inference(cnf_transformation,[],[f28]) ).
tcf(c_109,negated_conjecture,
( ( inverse(sk_c3) = sk_c9 )
| ( multiply(sk_c1,sk_c10) = sk_c9 ) ),
inference(cnf_transformation,[],[f30]) ).
tcf(c_110,negated_conjecture,
( ( multiply(sk_c1,sk_c10) = sk_c9 )
| ( multiply(sk_c4,sk_c7) = sk_c10 ) ),
inference(cnf_transformation,[],[f32]) ).
tcf(c_111,negated_conjecture,
( ( inverse(sk_c4) = sk_c7 )
| ( multiply(sk_c1,sk_c10) = sk_c9 ) ),
inference(cnf_transformation,[],[f34]) ).
tcf(c_112,negated_conjecture,
( ( multiply(sk_c1,sk_c10) = sk_c9 )
| ( multiply(sk_c7,sk_c9) = sk_c10 ) ),
inference(cnf_transformation,[],[f36]) ).
tcf(c_113,negated_conjecture,
( ( inverse(sk_c6) = sk_c5 )
| ( multiply(sk_c1,sk_c10) = sk_c9 ) ),
inference(cnf_transformation,[],[f38]) ).
tcf(c_114,negated_conjecture,
( ( inverse(sk_c5) = sk_c7 )
| ( multiply(sk_c1,sk_c10) = sk_c9 ) ),
inference(cnf_transformation,[],[f40]) ).
tcf(c_115,negated_conjecture,
( ( multiply(sk_c1,sk_c10) = sk_c9 )
| ( multiply(sk_c6,sk_c7) = sk_c5 ) ),
inference(cnf_transformation,[],[f42]) ).
tcf(c_116,negated_conjecture,
( ( inverse(sk_c1) = sk_c10 )
| ( multiply(sk_c2,sk_c10) = sk_c9 ) ),
inference(cnf_transformation,[],[f44]) ).
tcf(c_117,negated_conjecture,
( ( inverse(sk_c1) = sk_c10 )
| ( inverse(sk_c2) = sk_c10 ) ),
inference(cnf_transformation,[],[f46]) ).
tcf(c_118,negated_conjecture,
( ( inverse(sk_c1) = sk_c10 )
| ( multiply(sk_c3,sk_c9) = sk_c8 ) ),
inference(cnf_transformation,[],[f48]) ).
tcf(c_119,negated_conjecture,
( ( inverse(sk_c1) = sk_c10 )
| ( inverse(sk_c3) = sk_c9 ) ),
inference(cnf_transformation,[],[f50]) ).
tcf(c_120,negated_conjecture,
( ( inverse(sk_c1) = sk_c10 )
| ( multiply(sk_c4,sk_c7) = sk_c10 ) ),
inference(cnf_transformation,[],[f52]) ).
tcf(c_121,negated_conjecture,
( ( inverse(sk_c1) = sk_c10 )
| ( inverse(sk_c4) = sk_c7 ) ),
inference(cnf_transformation,[],[f54]) ).
tcf(c_122,negated_conjecture,
( ( inverse(sk_c1) = sk_c10 )
| ( multiply(sk_c7,sk_c9) = sk_c10 ) ),
inference(cnf_transformation,[],[f56]) ).
tcf(c_123,negated_conjecture,
( ( inverse(sk_c1) = sk_c10 )
| ( inverse(sk_c6) = sk_c5 ) ),
inference(cnf_transformation,[],[f58]) ).
tcf(c_125,negated_conjecture,
( ( inverse(sk_c1) = sk_c10 )
| ( multiply(sk_c6,sk_c7) = sk_c5 ) ),
inference(cnf_transformation,[],[f62]) ).
tcf(c_126,negated_conjecture,
( ( multiply(sk_c8,sk_c10) = sk_c9 )
| ( multiply(sk_c2,sk_c10) = sk_c9 ) ),
inference(cnf_transformation,[],[f64]) ).
tcf(c_127,negated_conjecture,
( ( inverse(sk_c2) = sk_c10 )
| ( multiply(sk_c8,sk_c10) = sk_c9 ) ),
inference(cnf_transformation,[],[f66]) ).
tcf(c_128,negated_conjecture,
( ( multiply(sk_c8,sk_c10) = sk_c9 )
| ( multiply(sk_c3,sk_c9) = sk_c8 ) ),
inference(cnf_transformation,[],[f68]) ).
tcf(c_129,negated_conjecture,
( ( inverse(sk_c3) = sk_c9 )
| ( multiply(sk_c8,sk_c10) = sk_c9 ) ),
inference(cnf_transformation,[],[f70]) ).
tcf(c_130,negated_conjecture,
( ( multiply(sk_c4,sk_c7) = sk_c10 )
| ( multiply(sk_c8,sk_c10) = sk_c9 ) ),
inference(cnf_transformation,[],[f72]) ).
tcf(c_131,negated_conjecture,
( ( inverse(sk_c4) = sk_c7 )
| ( multiply(sk_c8,sk_c10) = sk_c9 ) ),
inference(cnf_transformation,[],[f74]) ).
tcf(c_132,negated_conjecture,
( ( multiply(sk_c7,sk_c9) = sk_c10 )
| ( multiply(sk_c8,sk_c10) = sk_c9 ) ),
inference(cnf_transformation,[],[f76]) ).
tcf(c_133,negated_conjecture,
( ( inverse(sk_c6) = sk_c5 )
| ( multiply(sk_c8,sk_c10) = sk_c9 ) ),
inference(cnf_transformation,[],[f78]) ).
tcf(c_135,negated_conjecture,
( ( multiply(sk_c6,sk_c7) = sk_c5 )
| ( multiply(sk_c8,sk_c10) = sk_c9 ) ),
inference(cnf_transformation,[],[f82]) ).
tcf(c_136,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( ( inverse(sk_c10) != sk_c9 )
| ( inverse(X4) != sk_c9 )
| ( inverse(X3) != sk_c10 )
| ( inverse(X2) != sk_c10 )
| ( multiply(sk_c8,sk_c10) != sk_c9 )
| ( multiply(X4,sk_c9) != sk_c8 )
| ( multiply(X3,sk_c10) != sk_c9 )
| ( multiply(X2,sk_c10) != sk_c9 )
| ( inverse(inverse(X0)) != inverse(X1) )
| ( multiply(inverse(X1),sk_c9) != sk_c10 )
| ( multiply(X1,inverse(X1)) != sk_c10 )
| ( multiply(X0,inverse(X1)) != inverse(X0) ) ),
inference(cnf_transformation,[],[f86]) ).
tcf(c_517,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_10
| ( inverse(X0) != sk_c10 )
| ( multiply(X0,sk_c10) != sk_c9 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_10])],[c_136]) ).
tcf(c_518,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_11
| ( inverse(X0) != sk_c9 )
| ( multiply(X0,sk_c9) != sk_c8 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_11])],[c_136]) ).
tcf(c_519,negated_conjecture,
! [X0: $i,X1: $i] :
( ~ iPr_def_12
| ( inverse(inverse(X0)) != inverse(X1) )
| ( multiply(inverse(X1),sk_c9) != sk_c10 )
| ( multiply(X1,inverse(X1)) != sk_c10 )
| ( multiply(X0,inverse(X1)) != inverse(X0) ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_12])],[c_136]) ).
tcf(c_520,negated_conjecture,
( iPr_def_12
| iPr_def_11
| iPr_def_10
| ( inverse(sk_c10) != sk_c9 )
| ( multiply(sk_c8,sk_c10) != sk_c9 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_136]) ).
tcf(c_521,definition,
iPr_def_13 = multiply(sk_c8,sk_c10),
introduced(definition,[new_symbols(definition,[iPr_def_13])],[]) ).
tcf(c_522,definition,
iPr_def_14 = inverse(sk_c10),
introduced(definition,[new_symbols(definition,[iPr_def_14])],[]) ).
tcf(c_523,definition,
iPr_def_15 = multiply(sk_c6,sk_c7),
introduced(definition,[new_symbols(definition,[iPr_def_15])],[]) ).
tcf(c_525,definition,
iPr_def_17 = inverse(sk_c6),
introduced(definition,[new_symbols(definition,[iPr_def_17])],[]) ).
tcf(c_526,definition,
iPr_def_18 = multiply(sk_c7,sk_c9),
introduced(definition,[new_symbols(definition,[iPr_def_18])],[]) ).
tcf(c_527,definition,
iPr_def_19 = inverse(sk_c4),
introduced(definition,[new_symbols(definition,[iPr_def_19])],[]) ).
tcf(c_528,definition,
iPr_def_20 = multiply(sk_c4,sk_c7),
introduced(definition,[new_symbols(definition,[iPr_def_20])],[]) ).
tcf(c_529,definition,
iPr_def_21 = inverse(sk_c3),
introduced(definition,[new_symbols(definition,[iPr_def_21])],[]) ).
tcf(c_530,definition,
iPr_def_22 = multiply(sk_c3,sk_c9),
introduced(definition,[new_symbols(definition,[iPr_def_22])],[]) ).
tcf(c_531,definition,
iPr_def_23 = inverse(sk_c2),
introduced(definition,[new_symbols(definition,[iPr_def_23])],[]) ).
tcf(c_532,definition,
iPr_def_24 = multiply(sk_c2,sk_c10),
introduced(definition,[new_symbols(definition,[iPr_def_24])],[]) ).
tcf(c_533,definition,
iPr_def_25 = inverse(sk_c1),
introduced(definition,[new_symbols(definition,[iPr_def_25])],[]) ).
tcf(c_534,definition,
iPr_def_26 = multiply(sk_c1,sk_c10),
introduced(definition,[new_symbols(definition,[iPr_def_26])],[]) ).
tcf(c_535,negated_conjecture,
( iPr_def_12
| iPr_def_11
| iPr_def_10
| ( iPr_def_14 != sk_c9 )
| ( iPr_def_13 != sk_c9 ) ),
inference(demodulation,[status(thm)],[c_520,c_522,c_521]) ).
tcf(c_536,negated_conjecture,
! [X0: $i,X1: $i] :
( ~ iPr_def_12
| ( inverse(inverse(X0)) != inverse(X1) )
| ( multiply(inverse(X1),sk_c9) != sk_c10 )
| ( multiply(X1,inverse(X1)) != sk_c10 )
| ( multiply(X0,inverse(X1)) != inverse(X0) ) ),
inference(demodulation,[status(thm)],[c_519]) ).
tcf(c_538,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_11
| ( inverse(X0) != sk_c9 )
| ( multiply(X0,sk_c9) != sk_c8 ) ),
inference(demodulation,[status(thm)],[c_518]) ).
tcf(c_539,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_10
| ( inverse(X0) != sk_c10 )
| ( multiply(X0,sk_c10) != sk_c9 ) ),
inference(demodulation,[status(thm)],[c_517]) ).
tcf(c_540,negated_conjecture,
( ( iPr_def_15 = sk_c5 )
| ( iPr_def_13 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_135,c_523]) ).
tcf(c_542,negated_conjecture,
( ( iPr_def_17 = sk_c5 )
| ( iPr_def_13 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_133,c_525]) ).
tcf(c_543,negated_conjecture,
( ( iPr_def_18 = sk_c10 )
| ( iPr_def_13 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_132,c_526]) ).
tcf(c_544,negated_conjecture,
( ( iPr_def_19 = sk_c7 )
| ( iPr_def_13 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_131,c_527]) ).
tcf(c_545,negated_conjecture,
( ( iPr_def_20 = sk_c10 )
| ( iPr_def_13 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_130,c_528]) ).
tcf(c_546,negated_conjecture,
( ( iPr_def_21 = sk_c9 )
| ( iPr_def_13 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_129,c_529]) ).
tcf(c_547,negated_conjecture,
( ( iPr_def_22 = sk_c8 )
| ( iPr_def_13 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_128,c_530]) ).
tcf(c_548,negated_conjecture,
( ( iPr_def_23 = sk_c10 )
| ( iPr_def_13 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_127,c_531]) ).
tcf(c_549,negated_conjecture,
( ( iPr_def_24 = sk_c9 )
| ( iPr_def_13 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_126,c_532]) ).
tcf(c_550,negated_conjecture,
( ( iPr_def_25 = sk_c10 )
| ( iPr_def_15 = sk_c5 ) ),
inference(demodulation,[status(thm)],[c_125,c_533]) ).
tcf(c_552,negated_conjecture,
( ( iPr_def_25 = sk_c10 )
| ( iPr_def_17 = sk_c5 ) ),
inference(demodulation,[status(thm)],[c_123]) ).
tcf(c_553,negated_conjecture,
( ( iPr_def_25 = sk_c10 )
| ( iPr_def_18 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_122]) ).
tcf(c_554,negated_conjecture,
( ( iPr_def_25 = sk_c10 )
| ( iPr_def_19 = sk_c7 ) ),
inference(demodulation,[status(thm)],[c_121]) ).
tcf(c_555,negated_conjecture,
( ( iPr_def_25 = sk_c10 )
| ( iPr_def_20 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_120]) ).
tcf(c_556,negated_conjecture,
( ( iPr_def_25 = sk_c10 )
| ( iPr_def_21 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_119]) ).
tcf(c_557,negated_conjecture,
( ( iPr_def_25 = sk_c10 )
| ( iPr_def_22 = sk_c8 ) ),
inference(demodulation,[status(thm)],[c_118]) ).
tcf(c_558,negated_conjecture,
( ( iPr_def_25 = sk_c10 )
| ( iPr_def_23 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_117]) ).
tcf(c_559,negated_conjecture,
( ( iPr_def_25 = sk_c10 )
| ( iPr_def_24 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_116]) ).
tcf(c_560,negated_conjecture,
( ( iPr_def_26 = sk_c9 )
| ( iPr_def_15 = sk_c5 ) ),
inference(demodulation,[status(thm)],[c_115,c_534]) ).
tcf(c_561,negated_conjecture,
( ( iPr_def_26 = sk_c9 )
| ( iPr_def_16 = sk_c7 ) ),
inference(demodulation,[status(thm)],[c_114]) ).
tcf(c_562,negated_conjecture,
( ( iPr_def_26 = sk_c9 )
| ( iPr_def_17 = sk_c5 ) ),
inference(demodulation,[status(thm)],[c_113]) ).
tcf(c_563,negated_conjecture,
( ( iPr_def_26 = sk_c9 )
| ( iPr_def_18 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_112]) ).
tcf(c_564,negated_conjecture,
( ( iPr_def_26 = sk_c9 )
| ( iPr_def_19 = sk_c7 ) ),
inference(demodulation,[status(thm)],[c_111]) ).
tcf(c_565,negated_conjecture,
( ( iPr_def_26 = sk_c9 )
| ( iPr_def_20 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_110]) ).
tcf(c_566,negated_conjecture,
( ( iPr_def_26 = sk_c9 )
| ( iPr_def_21 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_109]) ).
tcf(c_567,negated_conjecture,
( ( iPr_def_26 = sk_c9 )
| ( iPr_def_22 = sk_c8 ) ),
inference(demodulation,[status(thm)],[c_108]) ).
tcf(c_568,negated_conjecture,
( ( iPr_def_26 = sk_c9 )
| ( iPr_def_23 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_107]) ).
tcf(c_569,negated_conjecture,
( ( iPr_def_26 = sk_c9 )
| ( iPr_def_24 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_106]) ).
tcf(c_570,negated_conjecture,
( ( iPr_def_15 = sk_c5 )
| ( iPr_def_14 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_105]) ).
tcf(c_572,negated_conjecture,
( ( iPr_def_17 = sk_c5 )
| ( iPr_def_14 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_103]) ).
tcf(c_573,negated_conjecture,
( ( iPr_def_18 = sk_c10 )
| ( iPr_def_14 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_102]) ).
tcf(c_574,negated_conjecture,
( ( iPr_def_19 = sk_c7 )
| ( iPr_def_14 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_101]) ).
tcf(c_575,negated_conjecture,
( ( iPr_def_20 = sk_c10 )
| ( iPr_def_14 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_100]) ).
tcf(c_576,negated_conjecture,
( ( iPr_def_21 = sk_c9 )
| ( iPr_def_14 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_99]) ).
tcf(c_577,negated_conjecture,
( ( iPr_def_22 = sk_c8 )
| ( iPr_def_14 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_98]) ).
tcf(c_578,negated_conjecture,
( ( iPr_def_23 = sk_c10 )
| ( iPr_def_14 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_97]) ).
tcf(c_579,negated_conjecture,
( ( iPr_def_24 = sk_c9 )
| ( iPr_def_14 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_96]) ).
tcf(c_580,plain,
! [X0: $i] : X0 = X0,
theory(equality) ).
tcf(c_581,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = X0 )
| ( X2 != X1 )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_582,plain,
! [X0: $i,X1: $i] :
( ( inverse(X0) = inverse(X1) )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_584,plain,
( ( inverse(sk_c10) = inverse(sk_c10) )
| ( sk_c10 != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_582]) ).
tcf(c_586,plain,
sk_c10 = sk_c10,
inference(instantiation,[status(thm)],[c_580]) ).
tcf(c_844,plain,
( ( iPr_def_15 = iPr_def_17 )
| ( sk_c9 = iPr_def_13 ) ),
inference(superposition,[status(thm)],[c_540,c_542]) ).
tcf(c_871,plain,
( ( iPr_def_13 = iPr_def_21 )
| ( sk_c9 = iPr_def_13 )
| ( sk_c10 = iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_546,c_543]) ).
tcf(c_882,plain,
( ( sk_c9 = iPr_def_13 )
| ( multiply(iPr_def_22,sk_c10) = iPr_def_13 ) ),
inference(superposition,[status(thm)],[c_547,c_521]) ).
tcf(c_909,plain,
( ( iPr_def_21 = iPr_def_24 )
| ( sk_c9 = iPr_def_13 ) ),
inference(superposition,[status(thm)],[c_549,c_546]) ).
tcf(c_944,plain,
( ( iPr_def_15 = iPr_def_17 )
| ( sk_c10 = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_552,c_550]) ).
tcf(c_1020,plain,
( ( sk_c10 = iPr_def_25 )
| ( multiply(sk_c4,iPr_def_19) = iPr_def_20 ) ),
inference(superposition,[status(thm)],[c_554,c_528]) ).
tcf(c_1022,plain,
( ( sk_c9 = iPr_def_13 )
| ( multiply(sk_c4,iPr_def_19) = iPr_def_20 ) ),
inference(superposition,[status(thm)],[c_544,c_528]) ).
tcf(c_1032,plain,
( ( sk_c9 = iPr_def_13 )
| ( multiply(sk_c3,iPr_def_24) = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_549,c_530]) ).
tcf(c_1034,plain,
( ( sk_c9 = iPr_def_13 )
| ( multiply(sk_c3,iPr_def_21) = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_546,c_530]) ).
tcf(c_1047,plain,
( ( sk_c10 = iPr_def_20 )
| ( multiply(sk_c2,iPr_def_25) = iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_555,c_532]) ).
tcf(c_1059,plain,
multiply(iPr_def_14,sk_c10) = identity,
inference(superposition,[status(thm)],[c_522,c_94]) ).
tcf(c_1060,plain,
multiply(iPr_def_23,sk_c2) = identity,
inference(superposition,[status(thm)],[c_531,c_94]) ).
tcf(c_1061,plain,
multiply(iPr_def_21,sk_c3) = identity,
inference(superposition,[status(thm)],[c_529,c_94]) ).
tcf(c_1062,plain,
multiply(iPr_def_19,sk_c4) = identity,
inference(superposition,[status(thm)],[c_527,c_94]) ).
tcf(c_1065,plain,
multiply(iPr_def_25,sk_c1) = identity,
inference(superposition,[status(thm)],[c_533,c_94]) ).
tcf(c_1066,plain,
! [X0: $i] :
( ( iPr_def_13 = sk_c9 )
| ( iPr_def_13 != X0 )
| ( sk_c9 != X0 ) ),
inference(instantiation,[status(thm)],[c_581]) ).
tcf(c_1075,plain,
! [X0: $i,X1: $i] :
( ( sk_c9 = X0 )
| ( sk_c9 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_581]) ).
tcf(c_1103,plain,
! [X0: $i] :
( ( sk_c9 = X0 )
| ( sk_c9 != sk_c9 )
| ( X0 != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_1075]) ).
tcf(c_1104,plain,
sk_c9 = sk_c9,
inference(instantiation,[status(thm)],[c_580]) ).
tcf(c_1110,plain,
multiply(identity,sk_c9) = sk_c9,
inference(instantiation,[status(thm)],[c_93]) ).
tcf(c_1112,plain,
! [X0: $i,X1: $i] :
( ( X0 = sk_c9 )
| ( sk_c9 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_581]) ).
tcf(c_1114,plain,
( ( sk_c9 = iPr_def_21 )
| ( iPr_def_21 != sk_c9 )
| ( sk_c9 != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_1103]) ).
tcf(c_1129,plain,
( ( sk_c10 = iPr_def_23 )
| ( multiply(sk_c1,iPr_def_25) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_558,c_534]) ).
tcf(c_1143,plain,
( ( iPr_def_13 = sk_c9 )
| ( iPr_def_13 != iPr_def_21 )
| ( sk_c9 != iPr_def_21 ) ),
inference(instantiation,[status(thm)],[c_1066]) ).
tcf(c_1144,plain,
! [X0: $i] :
( ( sk_c9 = X0 )
| ( sk_c9 != iPr_def_21 )
| ( X0 != iPr_def_21 ) ),
inference(instantiation,[status(thm)],[c_1075]) ).
tcf(c_1155,plain,
( ( iPr_def_21 = iPr_def_24 )
| ( sk_c10 = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_559,c_556]) ).
tcf(c_1156,plain,
( ( sk_c10 = iPr_def_25 )
| ( multiply(sk_c3,iPr_def_24) = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_559,c_530]) ).
tcf(c_1178,plain,
! [X0: $i] :
( ( sk_c9 = X0 )
| ( sk_c9 != iPr_def_24 )
| ( X0 != iPr_def_24 ) ),
inference(instantiation,[status(thm)],[c_1075]) ).
tcf(c_1206,plain,
! [X0: $i] :
( ( X0 = sk_c9 )
| ( sk_c9 != iPr_def_21 )
| ( X0 != iPr_def_21 ) ),
inference(instantiation,[status(thm)],[c_1112]) ).
tcf(c_1208,plain,
! [X0: $i] :
( ( X0 = sk_c9 )
| ( sk_c9 != iPr_def_24 )
| ( X0 != iPr_def_24 ) ),
inference(instantiation,[status(thm)],[c_1112]) ).
tcf(c_1233,plain,
! [X0: $i] :
( ( iPr_def_13 = iPr_def_21 )
| ( iPr_def_21 != X0 )
| ( iPr_def_13 != X0 ) ),
inference(instantiation,[status(thm)],[c_581]) ).
tcf(c_1242,plain,
( ( iPr_def_15 = iPr_def_17 )
| ( sk_c9 = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_562,c_560]) ).
tcf(c_1250,plain,
! [X0: $i] :
( ( iPr_def_13 = iPr_def_24 )
| ( iPr_def_24 != X0 )
| ( iPr_def_13 != X0 ) ),
inference(instantiation,[status(thm)],[c_581]) ).
tcf(c_1251,plain,
( ( iPr_def_13 = iPr_def_24 )
| ( iPr_def_24 != sk_c10 )
| ( iPr_def_13 != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_1250]) ).
tcf(c_1271,plain,
( ( iPr_def_13 = iPr_def_26 )
| ( sk_c10 = iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_563,c_543]) ).
tcf(c_1296,plain,
( ( sk_c9 = iPr_def_13 )
| ( iPr_def_13 != sk_c9 )
| ( sk_c9 != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_1103]) ).
tcf(c_1313,plain,
! [X0: $i,X1: $i] :
( ( X1 = multiply(identity,sk_c9) )
| ( X1 != X0 )
| ( multiply(identity,sk_c9) != X0 ) ),
inference(instantiation,[status(thm)],[c_581]) ).
tcf(c_1328,plain,
( ( sk_c9 = iPr_def_26 )
| ( multiply(sk_c4,iPr_def_19) = iPr_def_20 ) ),
inference(superposition,[status(thm)],[c_564,c_528]) ).
tcf(c_1354,plain,
( ( sk_c10 = iPr_def_20 )
| ( multiply(sk_c3,iPr_def_26) = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_565,c_530]) ).
tcf(c_1359,plain,
( ( iPr_def_13 = iPr_def_26 )
| ( sk_c10 = iPr_def_20 ) ),
inference(superposition,[status(thm)],[c_565,c_545]) ).
tcf(c_1405,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( inverse(X0) = X2 )
| ( X2 != X1 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_581]) ).
tcf(c_1410,plain,
! [X0: $i,X1: $i] :
( ( X0 = iPr_def_21 )
| ( iPr_def_21 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_581]) ).
tcf(c_1426,plain,
( ( sk_c9 = iPr_def_21 )
| ( multiply(sk_c3,iPr_def_26) = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_566,c_530]) ).
tcf(c_1461,plain,
! [X0: $i,X1: $i] :
( ( X0 = iPr_def_24 )
| ( iPr_def_24 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_581]) ).
tcf(c_1466,plain,
( ( iPr_def_21 = sk_c9 )
| ( iPr_def_21 != iPr_def_21 )
| ( sk_c9 != iPr_def_21 ) ),
inference(instantiation,[status(thm)],[c_1206]) ).
tcf(c_1467,plain,
iPr_def_21 = iPr_def_21,
inference(instantiation,[status(thm)],[c_580]) ).
tcf(c_1490,plain,
( ( sk_c10 = iPr_def_23 )
| ( multiply(sk_c3,iPr_def_26) = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_568,c_530]) ).
tcf(c_1493,plain,
( ( iPr_def_13 = iPr_def_26 )
| ( sk_c10 = iPr_def_23 ) ),
inference(superposition,[status(thm)],[c_568,c_548]) ).
tcf(c_1517,plain,
( ( iPr_def_24 = sk_c9 )
| ( iPr_def_24 != iPr_def_24 )
| ( sk_c9 != iPr_def_24 ) ),
inference(instantiation,[status(thm)],[c_1208]) ).
tcf(c_1518,plain,
iPr_def_24 = iPr_def_24,
inference(instantiation,[status(thm)],[c_580]) ).
tcf(c_1521,plain,
( ( iPr_def_13 = sk_c9 )
| ( iPr_def_13 != iPr_def_13 )
| ( sk_c9 != iPr_def_13 ) ),
inference(instantiation,[status(thm)],[c_1066]) ).
tcf(c_1522,plain,
! [X0: $i] :
( ( X0 = sk_c9 )
| ( sk_c9 != iPr_def_13 )
| ( X0 != iPr_def_13 ) ),
inference(instantiation,[status(thm)],[c_1112]) ).
tcf(c_1523,plain,
! [X0: $i] :
( ( sk_c9 = X0 )
| ( sk_c9 != iPr_def_13 )
| ( X0 != iPr_def_13 ) ),
inference(instantiation,[status(thm)],[c_1075]) ).
tcf(c_1524,plain,
( ( sk_c9 = sk_c10 )
| ( sk_c9 != iPr_def_13 )
| ( sk_c10 != iPr_def_13 ) ),
inference(instantiation,[status(thm)],[c_1523]) ).
tcf(c_1525,plain,
( ( sk_c10 = sk_c9 )
| ( sk_c9 != iPr_def_13 )
| ( sk_c10 != iPr_def_13 ) ),
inference(instantiation,[status(thm)],[c_1522]) ).
tcf(c_1545,plain,
iPr_def_13 = iPr_def_13,
inference(instantiation,[status(thm)],[c_580]) ).
tcf(c_1546,plain,
! [X0: $i,X1: $i] :
( ( iPr_def_13 = X0 )
| ( iPr_def_13 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_581]) ).
tcf(c_1562,plain,
( ( sk_c9 = iPr_def_24 )
| ( multiply(sk_c3,iPr_def_26) = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_569,c_530]) ).
tcf(c_1598,plain,
( ( iPr_def_13 = iPr_def_24 )
| ( iPr_def_24 != sk_c9 )
| ( iPr_def_13 != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_1250]) ).
tcf(c_1631,plain,
! [X0: $i,X1: $i] :
( ( multiply(identity,sk_c9) = X1 )
| ( X1 != X0 )
| ( multiply(identity,sk_c9) != X0 ) ),
inference(instantiation,[status(thm)],[c_581]) ).
tcf(c_1671,plain,
( ( iPr_def_15 = iPr_def_17 )
| ( sk_c9 = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_572,c_570]) ).
tcf(c_1689,plain,
multiply(identity,identity) = identity,
inference(instantiation,[status(thm)],[c_93]) ).
tcf(c_1696,plain,
! [X0: $i,X1: $i] :
( ( X0 = identity )
| ( identity != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_581]) ).
tcf(c_1718,plain,
( ( iPr_def_14 = iPr_def_26 )
| ( sk_c10 = iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_573,c_563]) ).
tcf(c_1721,plain,
( ( sk_c10 = iPr_def_18 )
| ( multiply(sk_c3,iPr_def_14) = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_573,c_530]) ).
tcf(c_1770,plain,
! [X0: $i] :
( ( X0 = sk_c9 )
| ( sk_c9 != iPr_def_26 )
| ( X0 != iPr_def_26 ) ),
inference(instantiation,[status(thm)],[c_1112]) ).
tcf(c_1771,plain,
! [X0: $i] :
( ( sk_c9 = X0 )
| ( sk_c9 != iPr_def_26 )
| ( X0 != iPr_def_26 ) ),
inference(instantiation,[status(thm)],[c_1075]) ).
tcf(c_1774,plain,
( ( iPr_def_13 = sk_c9 )
| ( iPr_def_13 != iPr_def_14 )
| ( sk_c9 != iPr_def_14 ) ),
inference(instantiation,[status(thm)],[c_1066]) ).
tcf(c_1775,plain,
! [X0: $i] :
( ( X0 = sk_c9 )
| ( sk_c9 != iPr_def_14 )
| ( X0 != iPr_def_14 ) ),
inference(instantiation,[status(thm)],[c_1112]) ).
tcf(c_1776,plain,
! [X0: $i] :
( ( sk_c9 = X0 )
| ( sk_c9 != iPr_def_14 )
| ( X0 != iPr_def_14 ) ),
inference(instantiation,[status(thm)],[c_1075]) ).
tcf(c_1789,plain,
( ( sk_c9 = iPr_def_14 )
| ( multiply(sk_c4,iPr_def_19) = iPr_def_20 ) ),
inference(superposition,[status(thm)],[c_574,c_528]) ).
tcf(c_1818,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( inverse(X0) = X2 )
| ( X2 != inverse(X1) )
| ( inverse(X0) != inverse(X1) ) ),
inference(instantiation,[status(thm)],[c_1405]) ).
tcf(c_1843,plain,
( ( iPr_def_14 = iPr_def_26 )
| ( sk_c10 = iPr_def_20 ) ),
inference(superposition,[status(thm)],[c_575,c_565]) ).
tcf(c_1847,plain,
( ( sk_c10 = iPr_def_20 )
| ( multiply(sk_c3,iPr_def_14) = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_575,c_530]) ).
tcf(c_1852,plain,
( ( iPr_def_13 = iPr_def_14 )
| ( sk_c10 = iPr_def_20 ) ),
inference(superposition,[status(thm)],[c_575,c_545]) ).
tcf(c_1899,plain,
! [X0: $i,X1: $i] :
( ( X0 = iPr_def_13 )
| ( iPr_def_13 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_581]) ).
tcf(c_1938,plain,
( ( sk_c9 = iPr_def_14 )
| ( multiply(sk_c3,iPr_def_21) = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_576,c_530]) ).
tcf(c_1985,plain,
! [X0: $i,X1: $i] :
( ( iPr_def_21 = X0 )
| ( iPr_def_21 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_581]) ).
tcf(c_1992,plain,
! [X0: $i,X1: $i] :
( ( iPr_def_24 = X0 )
| ( iPr_def_24 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_581]) ).
tcf(c_2037,plain,
! [X0: $i] :
( ( iPr_def_13 = X0 )
| ( iPr_def_13 != sk_c9 )
| ( X0 != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_1546]) ).
tcf(c_2039,plain,
! [X0: $i] :
( ( iPr_def_13 = X0 )
| ( iPr_def_13 != iPr_def_13 )
| ( X0 != iPr_def_13 ) ),
inference(instantiation,[status(thm)],[c_1546]) ).
tcf(c_2040,plain,
( ( iPr_def_13 = sk_c10 )
| ( iPr_def_13 != iPr_def_13 )
| ( sk_c10 != iPr_def_13 ) ),
inference(instantiation,[status(thm)],[c_2039]) ).
tcf(c_2045,plain,
( ( sk_c9 = iPr_def_14 )
| ( multiply(iPr_def_22,sk_c10) = iPr_def_13 ) ),
inference(superposition,[status(thm)],[c_577,c_521]) ).
tcf(c_2071,plain,
( ( iPr_def_14 = iPr_def_26 )
| ( sk_c10 = iPr_def_23 ) ),
inference(superposition,[status(thm)],[c_578,c_568]) ).
tcf(c_2080,plain,
( ( iPr_def_13 = iPr_def_14 )
| ( sk_c10 = iPr_def_23 ) ),
inference(superposition,[status(thm)],[c_578,c_548]) ).
tcf(c_2176,plain,
( ( iPr_def_21 = iPr_def_24 )
| ( sk_c9 = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_579,c_576]) ).
tcf(c_2185,plain,
( ( sk_c9 = iPr_def_14 )
| ( multiply(sk_c3,iPr_def_24) = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_579,c_530]) ).
tcf(c_2294,plain,
! [X0: $i] : multiply(sk_c1,multiply(sk_c10,X0)) = multiply(iPr_def_26,X0),
inference(superposition,[status(thm)],[c_534,c_95]) ).
tcf(c_2295,plain,
! [X0: $i] : multiply(sk_c8,multiply(sk_c10,X0)) = multiply(iPr_def_13,X0),
inference(superposition,[status(thm)],[c_521,c_95]) ).
tcf(c_2297,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(X0,X1)) = multiply(identity,X1),
inference(superposition,[status(thm)],[c_94,c_95]) ).
tcf(c_2299,plain,
! [X0: $i] : multiply(iPr_def_14,multiply(sk_c10,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1059,c_95]) ).
tcf(c_2300,plain,
! [X0: $i] : multiply(iPr_def_23,multiply(sk_c2,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1060,c_95]) ).
tcf(c_2301,plain,
! [X0: $i] : multiply(iPr_def_21,multiply(sk_c3,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1061,c_95]) ).
tcf(c_2302,plain,
! [X0: $i] : multiply(iPr_def_19,multiply(sk_c4,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1062,c_95]) ).
tcf(c_2308,plain,
! [X0: $i] : multiply(iPr_def_19,multiply(sk_c4,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_2302,c_93]) ).
tcf(c_2309,plain,
! [X0: $i] : multiply(iPr_def_21,multiply(sk_c3,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_2301,c_93]) ).
tcf(c_2310,plain,
! [X0: $i] : multiply(iPr_def_23,multiply(sk_c2,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_2300,c_93]) ).
tcf(c_2311,plain,
! [X0: $i] : multiply(iPr_def_14,multiply(sk_c10,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_2299,c_93]) ).
tcf(c_2335,plain,
! [X0: $i] :
( ( multiply(identity,sk_c9) = X0 )
| ( X0 != sk_c9 )
| ( multiply(identity,sk_c9) != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_1631]) ).
tcf(c_2336,plain,
( ( multiply(identity,sk_c9) = sk_c10 )
| ( sk_c10 != sk_c9 )
| ( multiply(identity,sk_c9) != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_2335]) ).
tcf(c_2352,plain,
! [X0: $i] : multiply(iPr_def_25,multiply(sk_c1,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1065,c_95]) ).
tcf(c_2353,plain,
! [X0: $i] : multiply(iPr_def_25,multiply(sk_c1,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_2352,c_93]) ).
tcf(c_2433,plain,
! [X0: $i,X1: $i] :
( ( identity = X0 )
| ( identity != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_581]) ).
tcf(c_2547,plain,
! [X0: $i] :
( ( X0 = iPr_def_21 )
| ( iPr_def_21 != sk_c9 )
| ( X0 != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_1410]) ).
tcf(c_2572,plain,
( ( iPr_def_21 = iPr_def_24 )
| ( iPr_def_13 = iPr_def_26 )
| ( sk_c9 = iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_909,c_569]) ).
tcf(c_2574,plain,
( ( iPr_def_21 = iPr_def_24 )
| ( iPr_def_13 = iPr_def_26 )
| ( sk_c9 = iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_909,c_566]) ).
tcf(c_2637,plain,
! [X0: $i] :
( ( X0 = iPr_def_24 )
| ( iPr_def_24 != sk_c9 )
| ( X0 != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_1461]) ).
tcf(c_2656,plain,
( ( iPr_def_15 = iPr_def_17 )
| ( multiply(sk_c1,iPr_def_25) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_944,c_534]) ).
tcf(c_2658,plain,
( ( iPr_def_15 = iPr_def_17 )
| ( inverse(iPr_def_25) = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_944,c_522]) ).
tcf(c_2687,plain,
( iPr_def_12
| iPr_def_11
| iPr_def_10
| ( iPr_def_21 = iPr_def_24 )
| ( sk_c9 != iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_909,c_535]) ).
tcf(c_2689,plain,
( iPr_def_12
| iPr_def_11
| iPr_def_10
| ( iPr_def_15 = iPr_def_17 )
| ( sk_c9 != iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_844,c_535]) ).
tcf(c_2705,plain,
( iPr_def_12
| iPr_def_11
| iPr_def_10
| ( sk_c10 = iPr_def_20 )
| ( sk_c9 != iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_545,c_535]) ).
tcf(c_2867,plain,
! [X0: $i] :
( ( inverse(X0) = iPr_def_14 )
| ( iPr_def_14 != inverse(sk_c10) )
| ( inverse(X0) != inverse(sk_c10) ) ),
inference(instantiation,[status(thm)],[c_1818]) ).
tcf(c_2868,plain,
( ( inverse(sk_c10) = iPr_def_14 )
| ( iPr_def_14 != inverse(sk_c10) )
| ( inverse(sk_c10) != inverse(sk_c10) ) ),
inference(instantiation,[status(thm)],[c_2867]) ).
tcf(c_2875,plain,
! [X0: $i] :
( ( inverse(X0) = iPr_def_21 )
| ( iPr_def_21 != inverse(sk_c3) )
| ( inverse(X0) != inverse(sk_c3) ) ),
inference(instantiation,[status(thm)],[c_1818]) ).
tcf(c_2876,plain,
( ( inverse(sk_c10) = iPr_def_21 )
| ( iPr_def_21 != inverse(sk_c3) )
| ( inverse(sk_c10) != inverse(sk_c3) ) ),
inference(instantiation,[status(thm)],[c_2875]) ).
tcf(c_2915,plain,
( ~ iPr_def_11
| ( sk_c8 != iPr_def_22 )
| ( inverse(sk_c3) != sk_c9 ) ),
inference(superposition,[status(thm)],[c_530,c_538]) ).
tcf(c_2917,plain,
( ~ iPr_def_11
| ( sk_c9 != sk_c8 )
| ( inverse(identity) != sk_c9 ) ),
inference(superposition,[status(thm)],[c_93,c_538]) ).
tcf(c_2920,plain,
! [X0: $i] :
( ( iPr_def_21 = iPr_def_24 )
| ~ iPr_def_11
| ( inverse(X0) != sk_c9 )
| ( multiply(X0,iPr_def_13) != sk_c8 ) ),
inference(superposition,[status(thm)],[c_909,c_538]) ).
tcf(c_2922,plain,
! [X0: $i] :
( ( iPr_def_15 = iPr_def_17 )
| ~ iPr_def_11
| ( inverse(X0) != sk_c9 )
| ( multiply(X0,iPr_def_13) != sk_c8 ) ),
inference(superposition,[status(thm)],[c_844,c_538]) ).
tcf(c_2938,plain,
! [X0: $i] :
( ( sk_c10 = iPr_def_20 )
| ~ iPr_def_11
| ( inverse(X0) != sk_c9 )
| ( multiply(X0,iPr_def_13) != sk_c8 ) ),
inference(superposition,[status(thm)],[c_545,c_538]) ).
tcf(c_2946,plain,
( ~ iPr_def_11
| ( sk_c8 != iPr_def_22 )
| ( sk_c9 != iPr_def_21 ) ),
inference(light_normalisation,[status(thm)],[c_2915,c_529]) ).
tcf(c_3062,plain,
( ( iPr_def_26 = sk_c9 )
| ( iPr_def_26 != iPr_def_26 )
| ( sk_c9 != iPr_def_26 ) ),
inference(instantiation,[status(thm)],[c_1770]) ).
tcf(c_3063,plain,
iPr_def_26 = iPr_def_26,
inference(instantiation,[status(thm)],[c_580]) ).
tcf(c_3064,plain,
! [X0: $i,X1: $i] :
( ( X0 = iPr_def_26 )
| ( iPr_def_26 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_581]) ).
tcf(c_3074,plain,
( ( iPr_def_14 = sk_c9 )
| ( iPr_def_14 != iPr_def_14 )
| ( sk_c9 != iPr_def_14 ) ),
inference(instantiation,[status(thm)],[c_1775]) ).
tcf(c_3075,plain,
iPr_def_14 = iPr_def_14,
inference(instantiation,[status(thm)],[c_580]) ).
tcf(c_3076,plain,
! [X0: $i,X1: $i] :
( ( X0 = iPr_def_14 )
| ( iPr_def_14 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_581]) ).
tcf(c_3106,plain,
( ~ iPr_def_10
| ( sk_c9 != iPr_def_24 )
| ( inverse(sk_c2) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_532,c_539]) ).
tcf(c_3107,plain,
( ~ iPr_def_10
| ( sk_c9 != iPr_def_26 )
| ( inverse(sk_c1) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_534,c_539]) ).
tcf(c_3126,plain,
( ~ iPr_def_10
| ( sk_c9 != iPr_def_26 )
| ( sk_c10 != iPr_def_25 ) ),
inference(light_normalisation,[status(thm)],[c_3107,c_533]) ).
tcf(c_3130,plain,
( ~ iPr_def_10
| ( sk_c9 != iPr_def_24 )
| ( sk_c10 != iPr_def_23 ) ),
inference(light_normalisation,[status(thm)],[c_3106,c_531]) ).
tcf(c_3206,plain,
! [X0: $i] :
( ~ iPr_def_12
| ( inverse(X0) != inverse(identity) )
| ( inverse(inverse(identity)) != inverse(X0) )
| ( multiply(inverse(X0),sk_c9) != sk_c10 )
| ( multiply(X0,inverse(X0)) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_93,c_536]) ).
tcf(c_3335,plain,
( ( iPr_def_21 = iPr_def_24 )
| ( multiply(sk_c1,iPr_def_25) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_1155,c_534]) ).
tcf(c_3337,plain,
( ( iPr_def_21 = iPr_def_24 )
| ( inverse(iPr_def_25) = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_1155,c_522]) ).
tcf(c_3387,plain,
( ( iPr_def_15 = iPr_def_17 )
| ( iPr_def_13 = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_1242,c_844]) ).
tcf(c_3536,plain,
! [X0: $i] :
( ( iPr_def_21 = X0 )
| ( iPr_def_21 != iPr_def_21 )
| ( X0 != iPr_def_21 ) ),
inference(instantiation,[status(thm)],[c_1985]) ).
tcf(c_3606,plain,
( ( iPr_def_18 = iPr_def_20 )
| ( iPr_def_13 = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_1359,c_1271]) ).
tcf(c_3652,plain,
! [X0: $i] :
( ( iPr_def_24 = X0 )
| ( iPr_def_24 != iPr_def_24 )
| ( X0 != iPr_def_24 ) ),
inference(instantiation,[status(thm)],[c_1992]) ).
tcf(c_3653,plain,
( ( iPr_def_24 = sk_c10 )
| ( iPr_def_24 != iPr_def_24 )
| ( sk_c10 != iPr_def_24 ) ),
inference(instantiation,[status(thm)],[c_3652]) ).
tcf(c_3666,plain,
( ( iPr_def_20 = iPr_def_23 )
| ( iPr_def_13 = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_1493,c_1359]) ).
tcf(c_3675,plain,
( ( iPr_def_13 = iPr_def_26 )
| ( multiply(sk_c2,iPr_def_23) = iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_1493,c_532]) ).
tcf(c_4082,plain,
( ( multiply(identity,sk_c9) = iPr_def_24 )
| ( iPr_def_24 != sk_c9 )
| ( multiply(identity,sk_c9) != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_2335]) ).
tcf(c_4130,plain,
( ( iPr_def_18 = iPr_def_20 )
| ( iPr_def_14 = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_1843,c_1718]) ).
tcf(c_4143,plain,
( ( iPr_def_14 = iPr_def_26 )
| ( inverse(iPr_def_20) = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_1843,c_522]) ).
tcf(c_4314,plain,
( ( iPr_def_20 = iPr_def_23 )
| ( iPr_def_14 = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_2071,c_1843]) ).
tcf(c_4326,plain,
( ( iPr_def_14 = iPr_def_26 )
| ( multiply(sk_c2,iPr_def_23) = iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_2071,c_532]) ).
tcf(c_4382,plain,
( ( iPr_def_13 = iPr_def_14 )
| ( multiply(sk_c2,iPr_def_23) = iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_2080,c_532]) ).
tcf(c_4484,plain,
( ( iPr_def_21 = iPr_def_24 )
| ( iPr_def_13 = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_2176,c_909]) ).
tcf(c_4489,plain,
( ( iPr_def_21 = iPr_def_24 )
| ( iPr_def_14 = iPr_def_26 )
| ( sk_c9 = iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_2176,c_569]) ).
tcf(c_4491,plain,
( ( iPr_def_21 = iPr_def_24 )
| ( iPr_def_14 = iPr_def_26 )
| ( sk_c9 = iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_2176,c_566]) ).
tcf(c_4611,plain,
( ( sk_c10 = iPr_def_18 )
| ( sk_c9 = iPr_def_13 ) ),
inference(global_subsumption_just,[status(thm)],[c_871,c_546,c_871,c_1104,c_1114,c_1143,c_1296]) ).
tcf(c_4612,plain,
( ( sk_c9 = iPr_def_13 )
| ( sk_c10 = iPr_def_18 ) ),
inference(renaming,[status(thm)],[c_4611]) ).
tcf(c_4702,plain,
multiply(iPr_def_19,iPr_def_20) = sk_c7,
inference(superposition,[status(thm)],[c_528,c_2308]) ).
tcf(c_4728,plain,
multiply(iPr_def_21,iPr_def_22) = sk_c9,
inference(superposition,[status(thm)],[c_530,c_2309]) ).
tcf(c_4740,plain,
multiply(iPr_def_23,iPr_def_24) = sk_c10,
inference(superposition,[status(thm)],[c_532,c_2310]) ).
tcf(c_4869,plain,
( ( iPr_def_13 = iPr_def_14 )
| ( sk_c9 = iPr_def_13 )
| ( multiply(iPr_def_22,iPr_def_20) = iPr_def_13 ) ),
inference(superposition,[status(thm)],[c_1852,c_882]) ).
tcf(c_4919,plain,
! [X0: $i] :
( ( multiply(identity,sk_c9) = X0 )
| ( X0 != iPr_def_24 )
| ( multiply(identity,sk_c9) != iPr_def_24 ) ),
inference(instantiation,[status(thm)],[c_1631]) ).
tcf(c_4920,plain,
! [X0: $i] :
( ( X0 = multiply(identity,sk_c9) )
| ( X0 != iPr_def_24 )
| ( multiply(identity,sk_c9) != iPr_def_24 ) ),
inference(instantiation,[status(thm)],[c_1313]) ).
tcf(c_4922,plain,
( ( multiply(identity,sk_c9) = sk_c10 )
| ( sk_c10 != iPr_def_24 )
| ( multiply(identity,sk_c9) != iPr_def_24 ) ),
inference(instantiation,[status(thm)],[c_4919]) ).
tcf(c_4927,plain,
( ( iPr_def_24 = iPr_def_21 )
| ( iPr_def_24 != sk_c9 )
| ( iPr_def_21 != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_2547]) ).
tcf(c_4995,plain,
! [X0: $i] :
( ( sk_c10 = iPr_def_23 )
| ( multiply(iPr_def_14,multiply(iPr_def_25,X0)) = X0 ) ),
inference(superposition,[status(thm)],[c_558,c_2311]) ).
tcf(c_4996,plain,
! [X0: $i] :
( ( sk_c10 = iPr_def_20 )
| ( multiply(iPr_def_14,multiply(iPr_def_25,X0)) = X0 ) ),
inference(superposition,[status(thm)],[c_555,c_2311]) ).
tcf(c_4997,plain,
! [X0: $i] :
( ( sk_c10 = iPr_def_18 )
| ( multiply(iPr_def_14,multiply(iPr_def_25,X0)) = X0 ) ),
inference(superposition,[status(thm)],[c_553,c_2311]) ).
tcf(c_5048,plain,
( ( iPr_def_21 = iPr_def_24 )
| ( iPr_def_24 != sk_c9 )
| ( iPr_def_21 != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_2637]) ).
tcf(c_5080,plain,
multiply(iPr_def_25,iPr_def_26) = sk_c10,
inference(superposition,[status(thm)],[c_534,c_2353]) ).
tcf(c_5143,plain,
( ( iPr_def_15 = iPr_def_17 )
| ( multiply(iPr_def_25,iPr_def_13) = sk_c10 ) ),
inference(superposition,[status(thm)],[c_3387,c_5080]) ).
tcf(c_5157,plain,
( ( iPr_def_18 = iPr_def_20 )
| ( multiply(iPr_def_25,iPr_def_13) = sk_c10 ) ),
inference(superposition,[status(thm)],[c_3606,c_5080]) ).
tcf(c_5665,plain,
! [X0: $i] :
( ( X0 = iPr_def_14 )
| ( iPr_def_14 != inverse(sk_c10) )
| ( X0 != inverse(sk_c10) ) ),
inference(instantiation,[status(thm)],[c_3076]) ).
tcf(c_5996,plain,
! [X0: $i,X1: $i] :
( ( inverse(X0) = X1 )
| ( X1 != iPr_def_14 )
| ( inverse(X0) != iPr_def_14 ) ),
inference(instantiation,[status(thm)],[c_1405]) ).
tcf(c_6177,plain,
( ( sk_c9 = iPr_def_13 )
| ( multiply(iPr_def_21,iPr_def_22) = iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_1032,c_2309]) ).
tcf(c_6178,plain,
( ( sk_c9 = iPr_def_24 )
| ( sk_c9 = iPr_def_13 ) ),
inference(light_normalisation,[status(thm)],[c_6177,c_4728]) ).
tcf(c_6198,plain,
! [X0: $i] :
( ( sk_c9 = iPr_def_13 )
| ( multiply(sk_c3,multiply(iPr_def_21,X0)) = multiply(iPr_def_22,X0) ) ),
inference(superposition,[status(thm)],[c_1034,c_95]) ).
tcf(c_6199,plain,
( ( sk_c9 = iPr_def_13 )
| ( multiply(iPr_def_21,iPr_def_22) = iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_1034,c_2309]) ).
tcf(c_6200,plain,
( ( sk_c9 = iPr_def_21 )
| ( sk_c9 = iPr_def_13 ) ),
inference(light_normalisation,[status(thm)],[c_6199,c_4728]) ).
tcf(c_6307,plain,
! [X0: $i] :
( ( inverse(X0) = inverse(sk_c3) )
| ( X0 != sk_c3 ) ),
inference(instantiation,[status(thm)],[c_582]) ).
tcf(c_6308,plain,
( ( inverse(sk_c10) = inverse(sk_c3) )
| ( sk_c10 != sk_c3 ) ),
inference(instantiation,[status(thm)],[c_6307]) ).
tcf(c_6368,plain,
( ( sk_c10 = iPr_def_20 )
| ( multiply(iPr_def_23,iPr_def_24) = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_1047,c_2310]) ).
tcf(c_6369,plain,
( ( sk_c10 = iPr_def_25 )
| ( sk_c10 = iPr_def_20 ) ),
inference(light_normalisation,[status(thm)],[c_6368,c_4740]) ).
tcf(c_6642,plain,
( ( sk_c10 = iPr_def_23 )
| ( multiply(iPr_def_25,iPr_def_26) = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_1129,c_2353]) ).
tcf(c_6643,plain,
( ( sk_c10 = iPr_def_25 )
| ( sk_c10 = iPr_def_23 ) ),
inference(light_normalisation,[status(thm)],[c_6642,c_5080]) ).
tcf(c_6784,plain,
( ( sk_c10 = iPr_def_25 )
| ( multiply(iPr_def_21,iPr_def_22) = iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_1156,c_2309]) ).
tcf(c_6785,plain,
( ( sk_c9 = iPr_def_24 )
| ( sk_c10 = iPr_def_25 ) ),
inference(light_normalisation,[status(thm)],[c_6784,c_4728]) ).
tcf(c_7165,plain,
( ( sk_c10 = iPr_def_20 )
| ( multiply(iPr_def_21,iPr_def_22) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_1354,c_2309]) ).
tcf(c_7166,plain,
( ( sk_c9 = iPr_def_26 )
| ( sk_c10 = iPr_def_20 ) ),
inference(light_normalisation,[status(thm)],[c_7165,c_4728]) ).
tcf(c_7415,plain,
( ( sk_c9 = iPr_def_21 )
| ( multiply(iPr_def_21,iPr_def_22) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_1426,c_2309]) ).
tcf(c_7416,plain,
( ( sk_c9 = iPr_def_26 )
| ( sk_c9 = iPr_def_21 ) ),
inference(light_normalisation,[status(thm)],[c_7415,c_4728]) ).
tcf(c_7679,plain,
( ( sk_c10 = iPr_def_23 )
| ( multiply(iPr_def_21,iPr_def_22) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_1490,c_2309]) ).
tcf(c_7680,plain,
( ( sk_c9 = iPr_def_26 )
| ( sk_c10 = iPr_def_23 ) ),
inference(light_normalisation,[status(thm)],[c_7679,c_4728]) ).
tcf(c_8000,plain,
( ( sk_c9 = iPr_def_24 )
| ( multiply(iPr_def_21,iPr_def_22) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_1562,c_2309]) ).
tcf(c_8001,plain,
( ( sk_c9 = iPr_def_26 )
| ( sk_c9 = iPr_def_24 ) ),
inference(light_normalisation,[status(thm)],[c_8000,c_4728]) ).
tcf(c_8341,plain,
( ( sk_c10 = iPr_def_18 )
| ( multiply(iPr_def_21,iPr_def_22) = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_1721,c_2309]) ).
tcf(c_8342,plain,
( ( sk_c9 = iPr_def_14 )
| ( sk_c10 = iPr_def_18 ) ),
inference(light_normalisation,[status(thm)],[c_8341,c_4728]) ).
tcf(c_8691,plain,
( ( sk_c10 = iPr_def_20 )
| ( multiply(iPr_def_21,iPr_def_22) = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_1847,c_2309]) ).
tcf(c_8692,plain,
( ( sk_c9 = iPr_def_14 )
| ( sk_c10 = iPr_def_20 ) ),
inference(light_normalisation,[status(thm)],[c_8691,c_4728]) ).
tcf(c_8937,plain,
( ( sk_c9 = iPr_def_14 )
| ( multiply(iPr_def_21,iPr_def_22) = iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_2185,c_2309]) ).
tcf(c_8938,plain,
( ( sk_c9 = iPr_def_24 )
| ( sk_c9 = iPr_def_14 ) ),
inference(light_normalisation,[status(thm)],[c_8937,c_4728]) ).
tcf(c_11392,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(X0,X1)) = X1,
inference(demodulation,[status(thm)],[c_2297,c_93]) ).
tcf(c_11430,plain,
! [X0: $i] : multiply(inverse(identity),X0) = X0,
inference(superposition,[status(thm)],[c_93,c_11392]) ).
tcf(c_11431,plain,
! [X0: $i] : multiply(inverse(inverse(X0)),identity) = X0,
inference(superposition,[status(thm)],[c_94,c_11392]) ).
tcf(c_11558,plain,
! [X0: $i] : multiply(inverse(iPr_def_14),X0) = multiply(sk_c10,X0),
inference(superposition,[status(thm)],[c_2311,c_11392]) ).
tcf(c_11559,plain,
! [X0: $i] : multiply(inverse(iPr_def_23),X0) = multiply(sk_c2,X0),
inference(superposition,[status(thm)],[c_2310,c_11392]) ).
tcf(c_11560,plain,
! [X0: $i] : multiply(inverse(iPr_def_21),X0) = multiply(sk_c3,X0),
inference(superposition,[status(thm)],[c_2309,c_11392]) ).
tcf(c_11561,plain,
! [X0: $i] : multiply(inverse(iPr_def_19),X0) = multiply(sk_c4,X0),
inference(superposition,[status(thm)],[c_2308,c_11392]) ).
tcf(c_11564,plain,
! [X0: $i] : multiply(inverse(iPr_def_25),X0) = multiply(sk_c1,X0),
inference(superposition,[status(thm)],[c_2353,c_11392]) ).
tcf(c_11623,plain,
! [X0: $i,X1: $i] : multiply(inverse(inverse(X0)),X1) = multiply(X0,X1),
inference(superposition,[status(thm)],[c_11392,c_11392]) ).
tcf(c_12187,plain,
( ( iPr_def_21 = iPr_def_24 )
| ( iPr_def_24 != iPr_def_21 )
| ( iPr_def_21 != iPr_def_21 ) ),
inference(instantiation,[status(thm)],[c_3536]) ).
tcf(c_12190,plain,
! [X0: $i] :
( ( iPr_def_24 = X0 )
| ( iPr_def_24 != iPr_def_21 )
| ( X0 != iPr_def_21 ) ),
inference(instantiation,[status(thm)],[c_1992]) ).
tcf(c_12191,plain,
! [X0: $i] :
( ( X0 = iPr_def_24 )
| ( iPr_def_24 != iPr_def_21 )
| ( X0 != iPr_def_21 ) ),
inference(instantiation,[status(thm)],[c_1461]) ).
tcf(c_12194,plain,
( ( iPr_def_24 = iPr_def_21 )
| ( iPr_def_24 != iPr_def_24 )
| ( iPr_def_21 != iPr_def_24 ) ),
inference(instantiation,[status(thm)],[c_3652]) ).
tcf(c_12198,plain,
! [X0: $i] :
( ( X0 = iPr_def_21 )
| ( iPr_def_21 != iPr_def_24 )
| ( X0 != iPr_def_24 ) ),
inference(instantiation,[status(thm)],[c_1410]) ).
tcf(c_12245,plain,
! [X0: $i] : multiply(X0,identity) = X0,
inference(demodulation,[status(thm)],[c_11431,c_11623]) ).
tcf(c_12270,plain,
inverse(identity) = identity,
inference(superposition,[status(thm)],[c_12245,c_11430]) ).
tcf(c_12439,plain,
( ( iPr_def_21 = iPr_def_24 )
| ( iPr_def_13 = iPr_def_26 ) ),
inference(global_subsumption_just,[status(thm)],[c_2572,c_1466,c_1467,c_1517,c_1518,c_2574,c_2572,c_4927,c_12187]) ).
tcf(c_12498,plain,
( iPr_def_12
| iPr_def_11
| ( iPr_def_21 = iPr_def_24 ) ),
inference(global_subsumption_just,[status(thm)],[c_2687,c_1155,c_2176,c_2687,c_3130,c_3126,c_7680,c_8001]) ).
tcf(c_12514,plain,
( iPr_def_12
| iPr_def_11
| ( iPr_def_15 = iPr_def_17 ) ),
inference(global_subsumption_just,[status(thm)],[c_2689,c_535,c_844,c_944,c_1242,c_1521,c_1545,c_1671,c_3074,c_3075,c_3126]) ).
tcf(c_12530,plain,
( iPr_def_12
| iPr_def_11
| ( sk_c10 = iPr_def_20 ) ),
inference(global_subsumption_just,[status(thm)],[c_2705,c_2705,c_3126,c_6369,c_7166,c_8692]) ).
tcf(c_12581,plain,
( ( sk_c9 = iPr_def_14 )
| ~ iPr_def_11
| ( sk_c8 != iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_576,c_2946]) ).
tcf(c_12590,plain,
( ( sk_c10 = iPr_def_25 )
| ~ iPr_def_11
| ( sk_c8 != iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_556,c_2946]) ).
tcf(c_12793,plain,
( ( sk_c9 = iPr_def_14 )
| ~ iPr_def_11 ),
inference(superposition,[status(thm)],[c_577,c_12581]) ).
tcf(c_12814,plain,
( ( sk_c10 = iPr_def_25 )
| ~ iPr_def_11 ),
inference(superposition,[status(thm)],[c_557,c_12590]) ).
tcf(c_12852,plain,
( ~ iPr_def_10
| ( sk_c9 != iPr_def_26 ) ),
inference(global_subsumption_just,[status(thm)],[c_3126,c_3130,c_3126,c_6643,c_6785]) ).
tcf(c_12854,plain,
~ iPr_def_10,
inference(global_subsumption_just,[status(thm)],[c_12852,c_3130,c_7680,c_8001,c_12852]) ).
tcf(c_12856,plain,
( iPr_def_12
| iPr_def_11
| ( sk_c9 != iPr_def_14 )
| ( sk_c9 != iPr_def_13 ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_535,c_12854]) ).
tcf(c_12872,plain,
multiply(sk_c10,iPr_def_14) = identity,
inference(superposition,[status(thm)],[c_11558,c_94]) ).
tcf(c_12876,plain,
multiply(sk_c10,identity) = inverse(iPr_def_14),
inference(superposition,[status(thm)],[c_11558,c_12245]) ).
tcf(c_12909,plain,
multiply(sk_c8,identity) = multiply(iPr_def_13,iPr_def_14),
inference(superposition,[status(thm)],[c_12872,c_2295]) ).
tcf(c_12910,plain,
multiply(sk_c1,identity) = multiply(iPr_def_26,iPr_def_14),
inference(superposition,[status(thm)],[c_12872,c_2294]) ).
tcf(c_13014,plain,
inverse(iPr_def_14) = sk_c10,
inference(demodulation,[status(thm)],[c_12876,c_12245]) ).
tcf(c_13280,plain,
( ( iPr_def_21 = iPr_def_24 )
| ( iPr_def_14 = iPr_def_26 ) ),
inference(global_subsumption_just,[status(thm)],[c_4489,c_1466,c_1467,c_1517,c_1518,c_4491,c_4489,c_4927,c_12187]) ).
tcf(c_13343,plain,
multiply(iPr_def_13,iPr_def_14) = sk_c8,
inference(demodulation,[status(thm)],[c_12909,c_12245]) ).
tcf(c_13344,plain,
multiply(inverse(iPr_def_13),sk_c8) = iPr_def_14,
inference(superposition,[status(thm)],[c_13343,c_11392]) ).
tcf(c_13347,plain,
( ( sk_c9 = iPr_def_26 )
| ( multiply(inverse(iPr_def_13),iPr_def_22) = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_567,c_13344]) ).
tcf(c_13350,plain,
multiply(inverse(inverse(iPr_def_13)),iPr_def_14) = sk_c8,
inference(superposition,[status(thm)],[c_13344,c_11392]) ).
tcf(c_13367,plain,
multiply(iPr_def_26,iPr_def_14) = sk_c1,
inference(demodulation,[status(thm)],[c_12910,c_12245]) ).
tcf(c_13369,plain,
( ( iPr_def_21 = iPr_def_24 )
| ( multiply(iPr_def_13,iPr_def_14) = sk_c1 ) ),
inference(superposition,[status(thm)],[c_12439,c_13367]) ).
tcf(c_13376,plain,
( ( iPr_def_20 = iPr_def_23 )
| ( multiply(iPr_def_13,iPr_def_14) = sk_c1 ) ),
inference(superposition,[status(thm)],[c_3666,c_13367]) ).
tcf(c_13377,plain,
( ( iPr_def_18 = iPr_def_20 )
| ( multiply(iPr_def_13,iPr_def_14) = sk_c1 ) ),
inference(superposition,[status(thm)],[c_3606,c_13367]) ).
tcf(c_13379,plain,
( ( iPr_def_15 = iPr_def_17 )
| ( multiply(iPr_def_13,iPr_def_14) = sk_c1 ) ),
inference(superposition,[status(thm)],[c_3387,c_13367]) ).
tcf(c_13384,plain,
( ( iPr_def_15 = iPr_def_17 )
| ( sk_c8 = sk_c1 ) ),
inference(light_normalisation,[status(thm)],[c_13379,c_13343]) ).
tcf(c_13390,plain,
( ( iPr_def_18 = iPr_def_20 )
| ( sk_c8 = sk_c1 ) ),
inference(light_normalisation,[status(thm)],[c_13377,c_13343]) ).
tcf(c_13393,plain,
( ( iPr_def_20 = iPr_def_23 )
| ( sk_c8 = sk_c1 ) ),
inference(light_normalisation,[status(thm)],[c_13376,c_13343]) ).
tcf(c_13409,plain,
( ( iPr_def_21 = iPr_def_24 )
| ( sk_c8 = sk_c1 ) ),
inference(light_normalisation,[status(thm)],[c_13369,c_13343]) ).
tcf(c_13575,plain,
( ( sk_c9 = iPr_def_26 )
| ( multiply(inverse(inverse(iPr_def_13)),iPr_def_14) = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_13347,c_11392]) ).
tcf(c_13577,plain,
( ( sk_c8 = iPr_def_22 )
| ( sk_c9 = iPr_def_26 ) ),
inference(light_normalisation,[status(thm)],[c_13575,c_13350]) ).
tcf(c_13767,plain,
( ( multiply(identity,sk_c9) = iPr_def_13 )
| ( iPr_def_13 != sk_c9 )
| ( multiply(identity,sk_c9) != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_2335]) ).
tcf(c_13840,plain,
( ( iPr_def_21 = iPr_def_13 )
| ( iPr_def_21 != iPr_def_21 )
| ( iPr_def_13 != iPr_def_21 ) ),
inference(instantiation,[status(thm)],[c_3536]) ).
tcf(c_13842,plain,
( ( sk_c9 = iPr_def_13 )
| ( iPr_def_13 != iPr_def_21 )
| ( sk_c9 != iPr_def_21 ) ),
inference(instantiation,[status(thm)],[c_1144]) ).
tcf(c_13972,plain,
( ( iPr_def_24 = iPr_def_13 )
| ( iPr_def_24 != iPr_def_24 )
| ( iPr_def_13 != iPr_def_24 ) ),
inference(instantiation,[status(thm)],[c_3652]) ).
tcf(c_13974,plain,
( ( sk_c9 = iPr_def_13 )
| ( iPr_def_13 != iPr_def_24 )
| ( sk_c9 != iPr_def_24 ) ),
inference(instantiation,[status(thm)],[c_1178]) ).
tcf(c_14342,plain,
( ( sk_c10 = iPr_def_23 )
| ( multiply(iPr_def_14,sk_c10) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_5080,c_4995]) ).
tcf(c_14351,plain,
( ( identity = iPr_def_26 )
| ( sk_c10 = iPr_def_23 ) ),
inference(light_normalisation,[status(thm)],[c_14342,c_1059]) ).
tcf(c_14387,plain,
( ( sk_c10 = iPr_def_20 )
| ( multiply(iPr_def_14,sk_c10) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_5080,c_4996]) ).
tcf(c_14396,plain,
( ( identity = iPr_def_26 )
| ( sk_c10 = iPr_def_20 ) ),
inference(light_normalisation,[status(thm)],[c_14387,c_1059]) ).
tcf(c_14511,plain,
( ( sk_c10 = iPr_def_18 )
| ( multiply(iPr_def_14,sk_c10) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_5080,c_4997]) ).
tcf(c_14520,plain,
( ( identity = iPr_def_26 )
| ( sk_c10 = iPr_def_18 ) ),
inference(light_normalisation,[status(thm)],[c_14511,c_1059]) ).
tcf(c_14585,plain,
( iPr_def_12
| iPr_def_11
| ( sk_c10 = iPr_def_25 )
| ( iPr_def_13 != iPr_def_24 )
| ( sk_c9 != iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_559,c_12856]) ).
tcf(c_14586,plain,
( iPr_def_12
| iPr_def_11
| ( sk_c10 = iPr_def_25 )
| ( iPr_def_13 != iPr_def_21 )
| ( sk_c9 != iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_556,c_12856]) ).
tcf(c_14587,plain,
( iPr_def_12
| iPr_def_11
| ( sk_c9 = iPr_def_13 )
| ( iPr_def_13 != iPr_def_24 )
| ( sk_c9 != iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_549,c_12856]) ).
tcf(c_14589,plain,
( iPr_def_12
| iPr_def_11
| ( sk_c9 = iPr_def_13 )
| ( iPr_def_13 != iPr_def_21 )
| ( sk_c9 != iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_546,c_12856]) ).
tcf(c_15246,plain,
( ( iPr_def_21 = iPr_def_24 )
| ( sk_c1 = iPr_def_22 )
| ( sk_c9 = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_13409,c_567]) ).
tcf(c_16190,plain,
( ( identity = iPr_def_26 )
| ( multiply(sk_c2,iPr_def_23) = iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_14351,c_532]) ).
tcf(c_16452,plain,
( ( iPr_def_21 = iPr_def_24 )
| ( sk_c9 = iPr_def_26 ) ),
inference(global_subsumption_just,[status(thm)],[c_15246,c_1466,c_1467,c_1517,c_1518,c_5048,c_7416,c_8001]) ).
tcf(c_16594,plain,
( ~ iPr_def_11
| ( sk_c9 != identity )
| ( sk_c9 != sk_c8 ) ),
inference(light_normalisation,[status(thm)],[c_2917,c_12270]) ).
tcf(c_16608,plain,
( ( iPr_def_21 = iPr_def_24 )
| ~ iPr_def_11
| ( sk_c9 != identity )
| ( sk_c9 != sk_c1 ) ),
inference(superposition,[status(thm)],[c_13409,c_16594]) ).
tcf(c_16610,plain,
( ( iPr_def_20 = iPr_def_23 )
| ~ iPr_def_11
| ( sk_c9 != identity )
| ( sk_c9 != sk_c1 ) ),
inference(superposition,[status(thm)],[c_13393,c_16594]) ).
tcf(c_16611,plain,
( ( iPr_def_18 = iPr_def_20 )
| ~ iPr_def_11
| ( sk_c9 != identity )
| ( sk_c9 != sk_c1 ) ),
inference(superposition,[status(thm)],[c_13390,c_16594]) ).
tcf(c_16613,plain,
( ( iPr_def_15 = iPr_def_17 )
| ~ iPr_def_11
| ( sk_c9 != identity )
| ( sk_c9 != sk_c1 ) ),
inference(superposition,[status(thm)],[c_13384,c_16594]) ).
tcf(c_16615,plain,
( ( sk_c9 = iPr_def_26 )
| ~ iPr_def_11
| ( sk_c9 != iPr_def_22 )
| ( sk_c9 != identity ) ),
inference(superposition,[status(thm)],[c_567,c_16594]) ).
tcf(c_16986,plain,
( ( iPr_def_20 = iPr_def_23 )
| ( identity = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_14396,c_14351]) ).
tcf(c_17118,plain,
( ( iPr_def_18 = iPr_def_20 )
| ( identity = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_14520,c_14396]) ).
tcf(c_17251,plain,
( ( iPr_def_20 = iPr_def_23 )
| ( inverse(iPr_def_26) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_16986,c_12270]) ).
tcf(c_17253,plain,
! [X0: $i] :
( ( iPr_def_20 = iPr_def_23 )
| ( multiply(iPr_def_26,X0) = X0 ) ),
inference(superposition,[status(thm)],[c_16986,c_93]) ).
tcf(c_17271,plain,
( ( iPr_def_18 = iPr_def_20 )
| ( inverse(iPr_def_26) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_17118,c_12270]) ).
tcf(c_17273,plain,
! [X0: $i] :
( ( iPr_def_18 = iPr_def_20 )
| ( multiply(iPr_def_26,X0) = X0 ) ),
inference(superposition,[status(thm)],[c_17118,c_93]) ).
tcf(c_17777,plain,
multiply(sk_c2,iPr_def_23) = identity,
inference(superposition,[status(thm)],[c_11559,c_94]) ).
tcf(c_17802,plain,
( ( identity = iPr_def_26 )
| ( identity = iPr_def_24 ) ),
inference(demodulation,[status(thm)],[c_16190,c_17777]) ).
tcf(c_17803,plain,
( ( iPr_def_13 = iPr_def_14 )
| ( identity = iPr_def_24 ) ),
inference(demodulation,[status(thm)],[c_4382,c_17777]) ).
tcf(c_17804,plain,
( ( iPr_def_14 = iPr_def_26 )
| ( identity = iPr_def_24 ) ),
inference(demodulation,[status(thm)],[c_4326,c_17777]) ).
tcf(c_17805,plain,
( ( iPr_def_13 = iPr_def_26 )
| ( identity = iPr_def_24 ) ),
inference(demodulation,[status(thm)],[c_3675,c_17777]) ).
tcf(c_18030,plain,
! [X0: $i] :
( ( identity = iPr_def_24 )
| ( multiply(iPr_def_26,X0) = X0 ) ),
inference(superposition,[status(thm)],[c_17802,c_93]) ).
tcf(c_18051,plain,
( ( iPr_def_13 = iPr_def_14 )
| ( inverse(iPr_def_24) = iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_17803,c_12270]) ).
tcf(c_18076,plain,
! [X0: $i] :
( ( iPr_def_14 = iPr_def_26 )
| ( multiply(iPr_def_24,X0) = X0 ) ),
inference(superposition,[status(thm)],[c_17804,c_93]) ).
tcf(c_18104,plain,
! [X0: $i] :
( ( iPr_def_13 = iPr_def_26 )
| ( multiply(iPr_def_24,X0) = X0 ) ),
inference(superposition,[status(thm)],[c_17805,c_93]) ).
tcf(c_18618,plain,
multiply(sk_c3,iPr_def_21) = identity,
inference(superposition,[status(thm)],[c_11560,c_94]) ).
tcf(c_18621,plain,
! [X0: $i] : multiply(sk_c3,multiply(iPr_def_21,X0)) = X0,
inference(superposition,[status(thm)],[c_11560,c_11392]) ).
tcf(c_18622,plain,
multiply(sk_c3,identity) = inverse(iPr_def_21),
inference(superposition,[status(thm)],[c_11560,c_12245]) ).
tcf(c_18632,plain,
( ( identity = iPr_def_22 )
| ( sk_c9 = iPr_def_14 ) ),
inference(demodulation,[status(thm)],[c_1938,c_18618]) ).
tcf(c_18634,plain,
( ( identity = iPr_def_22 )
| ( sk_c9 = iPr_def_13 ) ),
inference(demodulation,[status(thm)],[c_1034,c_18618]) ).
tcf(c_18710,plain,
( ( iPr_def_13 = iPr_def_26 )
| ( iPr_def_26 != sk_c9 )
| ( iPr_def_13 != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_2037]) ).
tcf(c_18716,plain,
( ( multiply(identity,sk_c9) = iPr_def_26 )
| ( iPr_def_26 != sk_c9 )
| ( multiply(identity,sk_c9) != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_2335]) ).
tcf(c_18722,plain,
! [X0: $i] :
( ( X0 = iPr_def_26 )
| ( iPr_def_26 != sk_c9 )
| ( X0 != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_3064]) ).
tcf(c_18917,plain,
( ( iPr_def_13 = iPr_def_14 )
| ( iPr_def_14 != sk_c9 )
| ( iPr_def_13 != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_2037]) ).
tcf(c_19116,plain,
( ( iPr_def_13 = iPr_def_14 )
| ( identity = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_18634,c_18632]) ).
tcf(c_19156,plain,
( ( iPr_def_13 = iPr_def_26 )
| ( identity = iPr_def_22 )
| ( sk_c9 = iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_18634,c_569]) ).
tcf(c_19279,plain,
inverse(iPr_def_21) = sk_c3,
inference(demodulation,[status(thm)],[c_18622,c_12245]) ).
tcf(c_19368,plain,
! [X0: $i] :
( ( iPr_def_13 = iPr_def_14 )
| ( multiply(iPr_def_22,X0) = X0 ) ),
inference(superposition,[status(thm)],[c_19116,c_93]) ).
tcf(c_19884,plain,
( ( iPr_def_20 = iPr_def_23 )
| ( sk_c1 = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_17253,c_13367]) ).
tcf(c_20216,plain,
( ( iPr_def_20 = iPr_def_23 )
| ( inverse(iPr_def_14) = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_19884,c_533]) ).
tcf(c_20217,plain,
( ( iPr_def_20 = iPr_def_23 )
| ( sk_c10 = iPr_def_25 ) ),
inference(light_normalisation,[status(thm)],[c_20216,c_13014]) ).
tcf(c_20365,plain,
! [X0: $i,X1: $i] :
( ( X0 = sk_c3 )
| ( sk_c3 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_581]) ).
tcf(c_20539,plain,
( ( iPr_def_13 = iPr_def_26 )
| ( sk_c9 = iPr_def_24 ) ),
inference(global_subsumption_just,[status(thm)],[c_19156,c_1521,c_1545,c_3062,c_3063,c_6178,c_8001,c_18710]) ).
tcf(c_21038,plain,
( ( iPr_def_18 = iPr_def_20 )
| ( sk_c1 = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_17273,c_13367]) ).
tcf(c_21253,plain,
( ( identity = iPr_def_24 )
| ( sk_c1 = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_18030,c_13367]) ).
tcf(c_21649,plain,
( ( iPr_def_18 = iPr_def_20 )
| ( inverse(iPr_def_14) = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_21038,c_533]) ).
tcf(c_21650,plain,
( ( iPr_def_18 = iPr_def_20 )
| ( sk_c10 = iPr_def_25 ) ),
inference(light_normalisation,[status(thm)],[c_21649,c_13014]) ).
tcf(c_21960,plain,
( ( iPr_def_14 = iPr_def_26 )
| ~ iPr_def_11
| ( sk_c9 != sk_c8 )
| ( inverse(iPr_def_24) != sk_c9 ) ),
inference(superposition,[status(thm)],[c_18076,c_538]) ).
tcf(c_22055,plain,
( ( iPr_def_13 = iPr_def_26 )
| ~ iPr_def_11
| ( sk_c9 != sk_c8 )
| ( inverse(iPr_def_24) != sk_c9 ) ),
inference(superposition,[status(thm)],[c_18104,c_538]) ).
tcf(c_22164,plain,
( ( identity = iPr_def_24 )
| ( inverse(iPr_def_14) = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_21253,c_533]) ).
tcf(c_22165,plain,
( ( identity = iPr_def_24 )
| ( sk_c10 = iPr_def_25 ) ),
inference(light_normalisation,[status(thm)],[c_22164,c_13014]) ).
tcf(c_23447,plain,
multiply(sk_c4,iPr_def_19) = identity,
inference(superposition,[status(thm)],[c_11561,c_94]) ).
tcf(c_23450,plain,
! [X0: $i] : multiply(sk_c4,multiply(iPr_def_19,X0)) = X0,
inference(superposition,[status(thm)],[c_11561,c_11392]) ).
tcf(c_23463,plain,
( ( identity = iPr_def_20 )
| ( sk_c9 = iPr_def_14 ) ),
inference(demodulation,[status(thm)],[c_1789,c_23447]) ).
tcf(c_23464,plain,
( ( identity = iPr_def_20 )
| ( sk_c9 = iPr_def_26 ) ),
inference(demodulation,[status(thm)],[c_1328,c_23447]) ).
tcf(c_23465,plain,
( ( identity = iPr_def_20 )
| ( sk_c9 = iPr_def_13 ) ),
inference(demodulation,[status(thm)],[c_1022,c_23447]) ).
tcf(c_23466,plain,
( ( identity = iPr_def_20 )
| ( sk_c10 = iPr_def_25 ) ),
inference(demodulation,[status(thm)],[c_1020,c_23447]) ).
tcf(c_23750,plain,
( ( iPr_def_14 = iPr_def_26 )
| ( identity = iPr_def_20 ) ),
inference(superposition,[status(thm)],[c_23464,c_23463]) ).
tcf(c_23915,plain,
( ( iPr_def_13 = iPr_def_26 )
| ( identity = iPr_def_20 ) ),
inference(superposition,[status(thm)],[c_23465,c_23464]) ).
tcf(c_23916,plain,
( ( iPr_def_13 = iPr_def_14 )
| ( identity = iPr_def_20 ) ),
inference(superposition,[status(thm)],[c_23465,c_23463]) ).
tcf(c_24200,plain,
( ( sk_c9 = iPr_def_14 )
| ( iPr_def_14 != inverse(sk_c10) )
| ( sk_c9 != inverse(sk_c10) ) ),
inference(instantiation,[status(thm)],[c_5665]) ).
tcf(c_24216,plain,
multiply(sk_c4,sk_c7) = iPr_def_20,
inference(superposition,[status(thm)],[c_4702,c_23450]) ).
tcf(c_24354,plain,
( ( iPr_def_14 = iPr_def_26 )
| ( inverse(iPr_def_20) = iPr_def_20 ) ),
inference(superposition,[status(thm)],[c_23750,c_12270]) ).
tcf(c_24640,plain,
( ( iPr_def_20 = iPr_def_24 )
| ( iPr_def_13 = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_23916,c_17803]) ).
tcf(c_25277,plain,
( ( iPr_def_13 = iPr_def_14 )
| ( sk_c9 = iPr_def_14 )
| ( sk_c10 = iPr_def_13 ) ),
inference(superposition,[status(thm)],[c_19368,c_2045]) ).
tcf(c_25287,plain,
( ( iPr_def_13 = iPr_def_20 )
| ( iPr_def_13 = iPr_def_14 )
| ( sk_c9 = iPr_def_13 ) ),
inference(superposition,[status(thm)],[c_19368,c_4869]) ).
tcf(c_29435,plain,
( ( iPr_def_13 = iPr_def_21 )
| ( iPr_def_21 != iPr_def_26 )
| ( iPr_def_13 != iPr_def_26 ) ),
inference(instantiation,[status(thm)],[c_1233]) ).
tcf(c_29436,plain,
! [X0: $i] :
( ( X0 = iPr_def_13 )
| ( iPr_def_13 != iPr_def_26 )
| ( X0 != iPr_def_26 ) ),
inference(instantiation,[status(thm)],[c_1899]) ).
tcf(c_29707,plain,
multiply(sk_c1,iPr_def_25) = identity,
inference(superposition,[status(thm)],[c_11564,c_94]) ).
tcf(c_29711,plain,
multiply(sk_c1,identity) = inverse(iPr_def_25),
inference(superposition,[status(thm)],[c_11564,c_12245]) ).
tcf(c_29743,plain,
( ( iPr_def_21 = iPr_def_24 )
| ( identity = iPr_def_26 ) ),
inference(demodulation,[status(thm)],[c_3335,c_29707]) ).
tcf(c_29745,plain,
( ( iPr_def_15 = iPr_def_17 )
| ( identity = iPr_def_26 ) ),
inference(demodulation,[status(thm)],[c_2656,c_29707]) ).
tcf(c_30125,plain,
( ( iPr_def_21 = iPr_def_24 )
| ( inverse(iPr_def_26) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_29743,c_12270]) ).
tcf(c_30145,plain,
! [X0: $i] :
( ( multiply(identity,sk_c9) = X0 )
| ( X0 != iPr_def_26 )
| ( multiply(identity,sk_c9) != iPr_def_26 ) ),
inference(instantiation,[status(thm)],[c_1631]) ).
tcf(c_30148,plain,
( ( multiply(identity,sk_c9) = sk_c10 )
| ( sk_c10 != iPr_def_26 )
| ( multiply(identity,sk_c9) != iPr_def_26 ) ),
inference(instantiation,[status(thm)],[c_30145]) ).
tcf(c_30282,plain,
( ( iPr_def_15 = iPr_def_17 )
| ( inverse(iPr_def_26) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_29745,c_12270]) ).
tcf(c_30295,plain,
! [X0: $i] :
( ( X0 = iPr_def_13 )
| ( iPr_def_13 != iPr_def_14 )
| ( X0 != iPr_def_14 ) ),
inference(instantiation,[status(thm)],[c_1899]) ).
tcf(c_30299,plain,
( ( sk_c9 = iPr_def_13 )
| ( iPr_def_13 != iPr_def_14 )
| ( sk_c9 != iPr_def_14 ) ),
inference(instantiation,[status(thm)],[c_1776]) ).
tcf(c_30301,plain,
! [X0: $i] :
( ( inverse(X0) = iPr_def_13 )
| ( iPr_def_13 != iPr_def_14 )
| ( inverse(X0) != iPr_def_14 ) ),
inference(instantiation,[status(thm)],[c_5996]) ).
tcf(c_30304,plain,
( ( inverse(sk_c10) = iPr_def_13 )
| ( iPr_def_13 != iPr_def_14 )
| ( inverse(sk_c10) != iPr_def_14 ) ),
inference(instantiation,[status(thm)],[c_30301]) ).
tcf(c_30305,plain,
inverse(iPr_def_25) = sk_c1,
inference(demodulation,[status(thm)],[c_29711,c_12245]) ).
tcf(c_30313,plain,
( ( iPr_def_21 = iPr_def_24 )
| ( sk_c1 = iPr_def_14 ) ),
inference(demodulation,[status(thm)],[c_3337,c_30305]) ).
tcf(c_30315,plain,
( ( iPr_def_15 = iPr_def_17 )
| ( sk_c1 = iPr_def_14 ) ),
inference(demodulation,[status(thm)],[c_2658,c_30305]) ).
tcf(c_30901,plain,
( ( iPr_def_14 = iPr_def_26 )
| ( iPr_def_26 != sk_c9 )
| ( iPr_def_14 != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_18722]) ).
tcf(c_32552,plain,
( ( iPr_def_20 = iPr_def_23 )
| ( inverse(iPr_def_14) = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_4314,c_17251]) ).
tcf(c_32570,plain,
( ( iPr_def_20 = iPr_def_23 )
| ( sk_c10 = iPr_def_14 ) ),
inference(light_normalisation,[status(thm)],[c_32552,c_13014]) ).
tcf(c_33049,plain,
( ( iPr_def_24 = sk_c9 )
| ( iPr_def_24 != iPr_def_13 )
| ( sk_c9 != iPr_def_13 ) ),
inference(instantiation,[status(thm)],[c_1522]) ).
tcf(c_33050,plain,
( ( sk_c9 = iPr_def_24 )
| ( iPr_def_24 != iPr_def_13 )
| ( sk_c9 != iPr_def_13 ) ),
inference(instantiation,[status(thm)],[c_1523]) ).
tcf(c_33057,plain,
( ( sk_c9 = iPr_def_21 )
| ( iPr_def_21 != iPr_def_13 )
| ( sk_c9 != iPr_def_13 ) ),
inference(instantiation,[status(thm)],[c_1523]) ).
tcf(c_33124,plain,
! [X0: $i] :
( ( multiply(identity,sk_c9) = X0 )
| ( X0 != iPr_def_13 )
| ( multiply(identity,sk_c9) != iPr_def_13 ) ),
inference(instantiation,[status(thm)],[c_1631]) ).
tcf(c_33125,plain,
! [X0: $i] :
( ( X0 = multiply(identity,sk_c9) )
| ( X0 != iPr_def_13 )
| ( multiply(identity,sk_c9) != iPr_def_13 ) ),
inference(instantiation,[status(thm)],[c_1313]) ).
tcf(c_33126,plain,
( ( sk_c10 = multiply(identity,sk_c9) )
| ( sk_c10 != iPr_def_13 )
| ( multiply(identity,sk_c9) != iPr_def_13 ) ),
inference(instantiation,[status(thm)],[c_33125]) ).
tcf(c_33127,plain,
( ( multiply(identity,sk_c9) = sk_c10 )
| ( sk_c10 != iPr_def_13 )
| ( multiply(identity,sk_c9) != iPr_def_13 ) ),
inference(instantiation,[status(thm)],[c_33124]) ).
tcf(c_34007,plain,
( ( sk_c10 = iPr_def_25 )
| ( multiply(iPr_def_22,sk_c10) = iPr_def_13 ) ),
inference(superposition,[status(thm)],[c_557,c_521]) ).
tcf(c_34014,plain,
( ( sk_c10 = iPr_def_23 )
| ( multiply(sk_c8,iPr_def_25) = iPr_def_13 ) ),
inference(superposition,[status(thm)],[c_558,c_521]) ).
tcf(c_34015,plain,
( ( sk_c10 = iPr_def_23 )
| ( inverse(iPr_def_25) = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_558,c_522]) ).
tcf(c_34032,plain,
( ( iPr_def_21 = iPr_def_24 )
| ( sk_c10 = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_559,c_556]) ).
tcf(c_34138,plain,
( ( sk_c9 = iPr_def_26 )
| ( multiply(iPr_def_16,sk_c9) = iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_561,c_526]) ).
tcf(c_34390,plain,
( ( iPr_def_13 = iPr_def_26 )
| ( sk_c10 = iPr_def_23 ) ),
inference(superposition,[status(thm)],[c_568,c_548]) ).
tcf(c_34516,plain,
multiply(iPr_def_23,sk_c2) = identity,
inference(superposition,[status(thm)],[c_531,c_94]) ).
tcf(c_34521,plain,
multiply(iPr_def_25,sk_c1) = identity,
inference(superposition,[status(thm)],[c_533,c_94]) ).
tcf(c_34558,plain,
( ( iPr_def_14 = iPr_def_26 )
| ( sk_c9 = iPr_def_24 )
| ( sk_c10 = iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_573,c_569]) ).
tcf(c_34574,plain,
( ( iPr_def_13 = iPr_def_14 )
| ( sk_c10 = iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_573,c_543]) ).
tcf(c_34847,plain,
( ( iPr_def_14 = iPr_def_26 )
| ( sk_c10 = iPr_def_23 ) ),
inference(superposition,[status(thm)],[c_578,c_568]) ).
tcf(c_34902,plain,
( ( iPr_def_21 = iPr_def_24 )
| ( sk_c9 = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_579,c_576]) ).
tcf(c_34959,plain,
( iPr_def_12
| iPr_def_11
| ( iPr_def_13 != sk_c9 )
| ( iPr_def_14 != sk_c9 ) ),
inference(global_subsumption_just,[status(thm)],[c_535,c_535,c_12854]) ).
tcf(c_34960,negated_conjecture,
( iPr_def_12
| iPr_def_11
| ( iPr_def_14 != sk_c9 )
| ( iPr_def_13 != sk_c9 ) ),
inference(renaming,[status(thm)],[c_34959]) ).
tcf(c_34988,plain,
( iPr_def_12
| iPr_def_11
| ( sk_c10 = iPr_def_18 )
| ( sk_c9 != iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_543,c_34960]) ).
tcf(c_35067,plain,
( ~ iPr_def_11
| ( sk_c8 != iPr_def_22 )
| ( inverse(sk_c3) != sk_c9 ) ),
inference(superposition,[status(thm)],[c_530,c_538]) ).
tcf(c_35097,plain,
( ~ iPr_def_11
| ( sk_c8 != iPr_def_22 )
| ( sk_c9 != iPr_def_21 ) ),
inference(light_normalisation,[status(thm)],[c_35067,c_529]) ).
tcf(c_35184,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(X0,X1)) = multiply(identity,X1),
inference(superposition,[status(thm)],[c_94,c_95]) ).
tcf(c_35237,plain,
! [X0: $i] : multiply(iPr_def_23,multiply(sk_c2,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_34516,c_95]) ).
tcf(c_35238,plain,
! [X0: $i] : multiply(iPr_def_23,multiply(sk_c2,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_35237,c_93]) ).
tcf(c_35741,plain,
! [X0: $i] : multiply(iPr_def_25,multiply(sk_c1,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_34521,c_95]) ).
tcf(c_35742,plain,
! [X0: $i] : multiply(iPr_def_25,multiply(sk_c1,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_35741,c_93]) ).
tcf(c_36260,plain,
( ( iPr_def_21 = iPr_def_24 )
| ( iPr_def_18 = iPr_def_25 )
| ( iPr_def_13 = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_34574,c_34032]) ).
tcf(c_36880,plain,
multiply(iPr_def_23,iPr_def_24) = sk_c10,
inference(superposition,[status(thm)],[c_532,c_35238]) ).
tcf(c_37321,plain,
( ( iPr_def_14 = iPr_def_26 )
| ( sk_c10 = iPr_def_25 )
| ( multiply(iPr_def_22,iPr_def_23) = iPr_def_13 ) ),
inference(superposition,[status(thm)],[c_34847,c_34007]) ).
tcf(c_37326,plain,
( ( iPr_def_13 = iPr_def_26 )
| ( sk_c10 = iPr_def_25 )
| ( multiply(iPr_def_22,iPr_def_23) = iPr_def_13 ) ),
inference(superposition,[status(thm)],[c_34390,c_34007]) ).
tcf(c_37338,plain,
! [X0: $i] :
( ( sk_c10 = iPr_def_25 )
| ( multiply(iPr_def_22,multiply(sk_c10,X0)) = multiply(iPr_def_13,X0) ) ),
inference(superposition,[status(thm)],[c_34007,c_95]) ).
tcf(c_37376,plain,
! [X0: $i] :
( ( sk_c10 = iPr_def_23 )
| ( multiply(sk_c8,multiply(iPr_def_25,X0)) = multiply(iPr_def_13,X0) ) ),
inference(superposition,[status(thm)],[c_34014,c_95]) ).
tcf(c_37394,plain,
( ( iPr_def_21 = iPr_def_24 )
| ( sk_c9 = iPr_def_26 )
| ( multiply(iPr_def_16,iPr_def_14) = iPr_def_18 ) ),
inference(superposition,[status(thm)],[c_34902,c_34138]) ).
tcf(c_37488,plain,
multiply(iPr_def_25,iPr_def_26) = sk_c10,
inference(superposition,[status(thm)],[c_534,c_35742]) ).
tcf(c_39072,plain,
( ( iPr_def_20 = iPr_def_23 )
| ( iPr_def_14 = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_32570,c_20217]) ).
tcf(c_39246,plain,
( ( iPr_def_20 = iPr_def_23 )
| ( inverse(iPr_def_14) = sk_c1 ) ),
inference(superposition,[status(thm)],[c_39072,c_30305]) ).
tcf(c_39285,plain,
( ( iPr_def_20 = iPr_def_23 )
| ( sk_c10 = sk_c1 ) ),
inference(light_normalisation,[status(thm)],[c_39246,c_13014]) ).
tcf(c_39734,plain,
( ( iPr_def_20 = iPr_def_23 )
| ( multiply(sk_c10,sk_c10) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_39285,c_534]) ).
tcf(c_39884,plain,
( ( iPr_def_18 = iPr_def_20 )
| ( inverse(iPr_def_14) = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_4130,c_17271]) ).
tcf(c_39902,plain,
( ( iPr_def_18 = iPr_def_20 )
| ( sk_c10 = iPr_def_14 ) ),
inference(light_normalisation,[status(thm)],[c_39884,c_13014]) ).
tcf(c_40673,plain,
( ( iPr_def_18 = iPr_def_20 )
| ( iPr_def_14 = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_39902,c_21650]) ).
tcf(c_40892,plain,
( ( iPr_def_18 = iPr_def_20 )
| ( inverse(iPr_def_14) = sk_c1 ) ),
inference(superposition,[status(thm)],[c_40673,c_30305]) ).
tcf(c_40931,plain,
( ( iPr_def_18 = iPr_def_20 )
| ( sk_c10 = sk_c1 ) ),
inference(light_normalisation,[status(thm)],[c_40892,c_13014]) ).
tcf(c_41168,plain,
( ( iPr_def_18 = iPr_def_20 )
| ( multiply(sk_c10,sk_c10) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_40931,c_534]) ).
tcf(c_41380,plain,
( iPr_def_12
| iPr_def_11
| ( sk_c9 != iPr_def_14 )
| ( iPr_def_13 != iPr_def_24 ) ),
inference(global_subsumption_just,[status(thm)],[c_14585,c_6178,c_12856,c_13974]) ).
tcf(c_41381,plain,
( iPr_def_12
| iPr_def_11
| ( iPr_def_13 != iPr_def_24 )
| ( sk_c9 != iPr_def_14 ) ),
inference(renaming,[status(thm)],[c_41380]) ).
tcf(c_41390,plain,
( iPr_def_12
| iPr_def_11
| ( iPr_def_13 = iPr_def_14 )
| ( iPr_def_13 != iPr_def_20 )
| ( sk_c9 != iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_24640,c_41381]) ).
tcf(c_41436,plain,
( iPr_def_12
| iPr_def_11
| ( sk_c9 != iPr_def_14 ) ),
inference(global_subsumption_just,[status(thm)],[c_14586,c_12856,c_25287,c_30299,c_41390]) ).
tcf(c_41477,plain,
( iPr_def_12
| iPr_def_11
| ( sk_c9 = iPr_def_14 )
| ( iPr_def_14 != iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_579,c_41436]) ).
tcf(c_41853,plain,
( iPr_def_12
| iPr_def_11
| ( iPr_def_14 != iPr_def_24 ) ),
inference(global_subsumption_just,[status(thm)],[c_41477,c_41436,c_41477]) ).
tcf(c_42829,plain,
( ( sk_c9 = iPr_def_13 )
| ( iPr_def_13 != iPr_def_24 ) ),
inference(global_subsumption_just,[status(thm)],[c_14587,c_6178,c_13974]) ).
tcf(c_42835,plain,
( ( iPr_def_13 = iPr_def_14 )
| ( sk_c9 = iPr_def_13 )
| ( iPr_def_13 != iPr_def_20 ) ),
inference(superposition,[status(thm)],[c_24640,c_42829]) ).
tcf(c_42847,plain,
( ( sk_c9 = iPr_def_13 )
| ( iPr_def_13 != iPr_def_21 ) ),
inference(global_subsumption_just,[status(thm)],[c_14589,c_6200,c_13842]) ).
tcf(c_42854,plain,
( ( sk_c9 = iPr_def_26 )
| ~ iPr_def_11 ),
inference(global_subsumption_just,[status(thm)],[c_16615,c_2946,c_7416,c_13577]) ).
tcf(c_43799,plain,
! [X0: $i] :
( ( sk_c9 = iPr_def_13 )
| ( iPr_def_13 != X0 )
| ( sk_c9 != X0 ) ),
inference(instantiation,[status(thm)],[c_1075]) ).
tcf(c_43800,plain,
( ( sk_c9 = iPr_def_13 )
| ( iPr_def_13 != sk_c10 )
| ( sk_c9 != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_43799]) ).
tcf(c_43805,plain,
! [X0: $i] :
( ( sk_c9 = identity )
| ( identity != X0 )
| ( sk_c9 != X0 ) ),
inference(instantiation,[status(thm)],[c_1075]) ).
tcf(c_43812,plain,
( ( sk_c9 = identity )
| ( identity != sk_c10 )
| ( sk_c9 != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_43805]) ).
tcf(c_43846,plain,
! [X0: $i] :
( ( sk_c9 = sk_c1 )
| ( sk_c1 != X0 )
| ( sk_c9 != X0 ) ),
inference(instantiation,[status(thm)],[c_1075]) ).
tcf(c_44347,plain,
( iPr_def_12
| iPr_def_11
| ( sk_c10 = iPr_def_18 ) ),
inference(global_subsumption_just,[status(thm)],[c_34988,c_4612,c_8342,c_12856]) ).
tcf(c_46771,plain,
( ( iPr_def_14 = iPr_def_26 )
| ( sk_c9 = iPr_def_24 ) ),
inference(global_subsumption_just,[status(thm)],[c_34558,c_3062,c_3063,c_3074,c_3075,c_8001,c_8938,c_30901]) ).
tcf(c_47210,plain,
( ( iPr_def_13 = iPr_def_14 )
| ( inverse(iPr_def_21) = iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_4484,c_18051]) ).
tcf(c_47219,plain,
( ( iPr_def_13 = iPr_def_14 )
| ( sk_c3 = iPr_def_21 ) ),
inference(light_normalisation,[status(thm)],[c_47210,c_19279]) ).
tcf(c_47809,plain,
( ( iPr_def_13 = iPr_def_14 )
| ( multiply(iPr_def_21,sk_c9) = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_47219,c_530]) ).
tcf(c_49319,plain,
( ( iPr_def_13 = iPr_def_14 )
| ( sk_c9 = iPr_def_13 )
| ( multiply(iPr_def_21,iPr_def_21) = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_546,c_47809]) ).
tcf(c_49437,plain,
! [X0: $i] :
( ( sk_c9 = inverse(X0) )
| ( sk_c9 != iPr_def_21 )
| ( inverse(X0) != iPr_def_21 ) ),
inference(instantiation,[status(thm)],[c_1144]) ).
tcf(c_49439,plain,
! [X0: $i,X1: $i] :
( ( sk_c9 = inverse(X0) )
| ( sk_c9 != X1 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_1075]) ).
tcf(c_49440,plain,
( ( sk_c9 = inverse(sk_c10) )
| ( sk_c9 != sk_c10 )
| ( inverse(sk_c10) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_49439]) ).
tcf(c_49441,plain,
( ( sk_c9 = inverse(sk_c10) )
| ( sk_c9 != iPr_def_21 )
| ( inverse(sk_c10) != iPr_def_21 ) ),
inference(instantiation,[status(thm)],[c_49437]) ).
tcf(c_49569,plain,
( ( iPr_def_14 = iPr_def_26 )
| ( iPr_def_14 = iPr_def_20 ) ),
inference(superposition,[status(thm)],[c_24354,c_4143]) ).
tcf(c_49825,plain,
( ( iPr_def_13 = iPr_def_14 )
| ( sk_c9 = iPr_def_13 ) ),
inference(global_subsumption_just,[status(thm)],[c_49319,c_25287,c_42835]) ).
tcf(c_49920,plain,
( ( iPr_def_13 = iPr_def_24 )
| ( iPr_def_13 = iPr_def_14 )
| ( sk_c9 = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_49825,c_579]) ).
tcf(c_49932,plain,
( ( iPr_def_13 = iPr_def_14 )
| ( multiply(sk_c3,iPr_def_13) = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_49825,c_530]) ).
tcf(c_50046,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(X0,X1)) = X1,
inference(demodulation,[status(thm)],[c_35184,c_93]) ).
tcf(c_50083,plain,
multiply(inverse(sk_c8),iPr_def_13) = sk_c10,
inference(superposition,[status(thm)],[c_521,c_50046]) ).
tcf(c_50085,plain,
! [X0: $i] : multiply(inverse(inverse(X0)),identity) = X0,
inference(superposition,[status(thm)],[c_94,c_50046]) ).
tcf(c_50086,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(inverse(multiply(X0,X1)),multiply(X0,multiply(X1,X2))) = X2,
inference(superposition,[status(thm)],[c_95,c_50046]) ).
tcf(c_50288,plain,
! [X0: $i,X1: $i] : multiply(inverse(inverse(X0)),X1) = multiply(X0,X1),
inference(superposition,[status(thm)],[c_50046,c_50046]) ).
tcf(c_50572,plain,
( ( iPr_def_13 = iPr_def_24 )
| ( iPr_def_13 = iPr_def_14 ) ),
inference(global_subsumption_just,[status(thm)],[c_49920,c_579,c_1521,c_1545,c_1598,c_18917,c_49825]) ).
tcf(c_50610,plain,
( ( iPr_def_13 = iPr_def_21 )
| ( iPr_def_13 = iPr_def_14 ) ),
inference(superposition,[status(thm)],[c_50572,c_4484]) ).
tcf(c_51816,plain,
( ( sk_c3 = iPr_def_24 )
| ( iPr_def_24 != iPr_def_21 )
| ( sk_c3 != iPr_def_21 ) ),
inference(instantiation,[status(thm)],[c_12191]) ).
tcf(c_51821,plain,
! [X0: $i] :
( ( X0 = sk_c3 )
| ( sk_c3 != multiply(identity,sk_c9) )
| ( X0 != multiply(identity,sk_c9) ) ),
inference(instantiation,[status(thm)],[c_20365]) ).
tcf(c_51822,plain,
( ( sk_c3 = multiply(identity,sk_c9) )
| ( sk_c3 != iPr_def_24 )
| ( multiply(identity,sk_c9) != iPr_def_24 ) ),
inference(instantiation,[status(thm)],[c_4920]) ).
tcf(c_51824,plain,
( ( sk_c10 = sk_c3 )
| ( sk_c3 != multiply(identity,sk_c9) )
| ( sk_c10 != multiply(identity,sk_c9) ) ),
inference(instantiation,[status(thm)],[c_51821]) ).
tcf(c_51861,plain,
iPr_def_13 = iPr_def_14,
inference(global_subsumption_just,[status(thm)],[c_49932,c_522,c_529,c_1110,c_1467,c_1518,c_1521,c_1545,c_2876,c_3074,c_3075,c_4082,c_4484,c_6308,c_12194,c_13767,c_13840,c_13972,c_18917,c_24200,c_25277,c_33049,c_33057,c_33126,c_47219,c_49441,c_49825,c_50572,c_50610,c_51816,c_51824,c_51822]) ).
tcf(c_51894,plain,
( iPr_def_12
| iPr_def_11
| ( iPr_def_13 != iPr_def_24 ) ),
inference(demodulation,[status(thm)],[c_41853,c_51861]) ).
tcf(c_51895,plain,
( iPr_def_12
| iPr_def_11
| ( sk_c9 != iPr_def_13 ) ),
inference(demodulation,[status(thm)],[c_41436,c_51861]) ).
tcf(c_51897,plain,
( ( iPr_def_18 = iPr_def_20 )
| ( iPr_def_13 = iPr_def_25 ) ),
inference(demodulation,[status(thm)],[c_40673,c_51861]) ).
tcf(c_51898,plain,
( ( iPr_def_18 = iPr_def_20 )
| ( sk_c10 = iPr_def_13 ) ),
inference(demodulation,[status(thm)],[c_39902,c_51861]) ).
tcf(c_51903,plain,
( ( iPr_def_20 = iPr_def_23 )
| ( sk_c10 = iPr_def_13 ) ),
inference(demodulation,[status(thm)],[c_32570,c_51861]) ).
tcf(c_51982,plain,
multiply(iPr_def_13,iPr_def_13) = sk_c8,
inference(demodulation,[status(thm)],[c_13343,c_51861]) ).
tcf(c_51988,plain,
inverse(iPr_def_13) = sk_c10,
inference(demodulation,[status(thm)],[c_13014,c_51861]) ).
tcf(c_52081,plain,
multiply(iPr_def_13,sk_c10) = identity,
inference(demodulation,[status(thm)],[c_1059,c_51861]) ).
tcf(c_52082,plain,
inverse(sk_c10) = iPr_def_13,
inference(demodulation,[status(thm)],[c_522,c_51861]) ).
tcf(c_53906,plain,
( ( sk_c9 = iPr_def_24 )
| ~ iPr_def_11
| ( iPr_def_21 != iPr_def_26 )
| ( sk_c8 != iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_569,c_35097]) ).
tcf(c_54101,plain,
! [X0: $i] :
( ( sk_c9 = inverse(X0) )
| ( sk_c9 != iPr_def_13 )
| ( inverse(X0) != iPr_def_13 ) ),
inference(instantiation,[status(thm)],[c_1523]) ).
tcf(c_54102,plain,
( ( sk_c9 = inverse(sk_c10) )
| ( sk_c9 != iPr_def_13 )
| ( inverse(sk_c10) != iPr_def_13 ) ),
inference(instantiation,[status(thm)],[c_54101]) ).
tcf(c_54105,plain,
( ( sk_c9 = iPr_def_14 )
| ( iPr_def_14 != iPr_def_13 )
| ( sk_c9 != iPr_def_13 ) ),
inference(instantiation,[status(thm)],[c_1523]) ).
tcf(c_54718,plain,
( ( identity = iPr_def_21 )
| ( iPr_def_21 != iPr_def_24 )
| ( identity != iPr_def_24 ) ),
inference(instantiation,[status(thm)],[c_12198]) ).
tcf(c_55048,plain,
( ( iPr_def_18 = iPr_def_20 )
| ( multiply(iPr_def_13,iPr_def_13) = sk_c10 ) ),
inference(superposition,[status(thm)],[c_51897,c_5157]) ).
tcf(c_55094,plain,
( ( iPr_def_18 = iPr_def_20 )
| ( sk_c10 = sk_c8 ) ),
inference(light_normalisation,[status(thm)],[c_55048,c_51982]) ).
tcf(c_55519,plain,
( ( iPr_def_18 = iPr_def_20 )
| ( multiply(iPr_def_13,iPr_def_13) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_51898,c_41168]) ).
tcf(c_55561,plain,
( ( iPr_def_18 = iPr_def_20 )
| ( sk_c8 = iPr_def_26 ) ),
inference(light_normalisation,[status(thm)],[c_55519,c_51982]) ).
tcf(c_56261,plain,
( ( iPr_def_20 = iPr_def_23 )
| ( multiply(iPr_def_13,iPr_def_13) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_51903,c_39734]) ).
tcf(c_56301,plain,
( ( iPr_def_20 = iPr_def_23 )
| ( sk_c8 = iPr_def_26 ) ),
inference(light_normalisation,[status(thm)],[c_56261,c_51982]) ).
tcf(c_56879,plain,
! [X0: $i] :
( ( X0 = iPr_def_26 )
| ( iPr_def_26 != iPr_def_13 )
| ( X0 != iPr_def_13 ) ),
inference(instantiation,[status(thm)],[c_3064]) ).
tcf(c_56880,plain,
( ( sk_c10 = iPr_def_26 )
| ( iPr_def_26 != iPr_def_13 )
| ( sk_c10 != iPr_def_13 ) ),
inference(instantiation,[status(thm)],[c_56879]) ).
tcf(c_59441,plain,
! [X0: $i] : multiply(X0,identity) = X0,
inference(demodulation,[status(thm)],[c_50085,c_50288]) ).
tcf(c_60729,plain,
( ( iPr_def_14 = iPr_def_26 )
| ~ iPr_def_11 ),
inference(global_subsumption_just,[status(thm)],[c_21960,c_3062,c_3063,c_3074,c_3075,c_12793,c_30901,c_42854]) ).
tcf(c_60740,plain,
( ( iPr_def_13 = iPr_def_26 )
| ~ iPr_def_11 ),
inference(global_subsumption_just,[status(thm)],[c_22055,c_522,c_529,c_1110,c_1467,c_1518,c_1521,c_1545,c_1774,c_2876,c_2946,c_3062,c_3063,c_3074,c_3075,c_4082,c_4484,c_6308,c_7416,c_12194,c_12793,c_13577,c_13767,c_13840,c_13972,c_18710,c_18917,c_24200,c_25277,c_33049,c_33057,c_33126,c_47219,c_49441,c_49825,c_50572,c_50610,c_51816,c_51824,c_51822]) ).
tcf(c_61424,plain,
! [X0: $i] :
( ( identity = X0 )
| ( identity != iPr_def_13 )
| ( X0 != iPr_def_13 ) ),
inference(instantiation,[status(thm)],[c_2433]) ).
tcf(c_61425,plain,
! [X0: $i] :
( ( X0 = identity )
| ( identity != iPr_def_13 )
| ( X0 != iPr_def_13 ) ),
inference(instantiation,[status(thm)],[c_1696]) ).
tcf(c_61426,plain,
( ( sk_c10 = identity )
| ( identity != iPr_def_13 )
| ( sk_c10 != iPr_def_13 ) ),
inference(instantiation,[status(thm)],[c_61425]) ).
tcf(c_61427,plain,
( ( identity = sk_c10 )
| ( identity != iPr_def_13 )
| ( sk_c10 != iPr_def_13 ) ),
inference(instantiation,[status(thm)],[c_61424]) ).
tcf(c_61658,plain,
iPr_def_13 = iPr_def_14,
inference(global_subsumption_just,[status(thm)],[c_36260,c_51861]) ).
tcf(c_61744,plain,
( ( sk_c10 = iPr_def_23 )
| ( inverse(iPr_def_25) = iPr_def_13 ) ),
inference(demodulation,[status(thm)],[c_34015,c_61658]) ).
tcf(c_61768,plain,
( iPr_def_12
| iPr_def_11
| ( sk_c9 != iPr_def_13 ) ),
inference(demodulation,[status(thm)],[c_34960,c_61658]) ).
tcf(c_61781,plain,
inverse(sk_c10) = iPr_def_13,
inference(demodulation,[status(thm)],[c_522,c_61658]) ).
tcf(c_61860,plain,
( iPr_def_12
| iPr_def_11
| ( sk_c10 = iPr_def_25 )
| ( iPr_def_13 != iPr_def_21 ) ),
inference(superposition,[status(thm)],[c_556,c_61768]) ).
tcf(c_61969,plain,
( iPr_def_12
| iPr_def_11
| ( iPr_def_13 != iPr_def_21 ) ),
inference(global_subsumption_just,[status(thm)],[c_61860,c_584,c_586,c_522,c_535,c_1521,c_1545,c_2868,c_3074,c_3075,c_12854,c_24200,c_30304,c_42847,c_51861,c_54102]) ).
tcf(c_62422,plain,
! [X0: $i] : multiply(inverse(multiply(X0,sk_c2)),multiply(X0,iPr_def_24)) = sk_c10,
inference(superposition,[status(thm)],[c_532,c_50086]) ).
tcf(c_62425,plain,
! [X0: $i] : multiply(inverse(multiply(X0,sk_c7)),multiply(X0,iPr_def_18)) = sk_c9,
inference(superposition,[status(thm)],[c_526,c_50086]) ).
tcf(c_64503,plain,
! [X0: $i] :
( ( identity = X0 )
| ( identity != iPr_def_26 )
| ( X0 != iPr_def_26 ) ),
inference(instantiation,[status(thm)],[c_2433]) ).
tcf(c_64506,plain,
( ( identity = sk_c10 )
| ( identity != iPr_def_26 )
| ( sk_c10 != iPr_def_26 ) ),
inference(instantiation,[status(thm)],[c_64503]) ).
tcf(c_64508,plain,
( ( sk_c9 = identity )
| ( identity != iPr_def_26 )
| ( sk_c9 != iPr_def_26 ) ),
inference(instantiation,[status(thm)],[c_1771]) ).
tcf(c_65801,plain,
( ( iPr_def_18 = iPr_def_20 )
| ( sk_c10 = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_55561,c_55094]) ).
tcf(c_65840,plain,
( ( iPr_def_18 = iPr_def_20 )
| ( sk_c1 = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_55561,c_13390]) ).
tcf(c_66205,plain,
( ( iPr_def_20 = iPr_def_23 )
| ( sk_c1 = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_56301,c_13393]) ).
tcf(c_66221,plain,
( ( iPr_def_20 = iPr_def_23 )
| ( multiply(iPr_def_26,sk_c10) = iPr_def_13 ) ),
inference(superposition,[status(thm)],[c_56301,c_521]) ).
tcf(c_67185,plain,
( ( sk_c9 = sk_c1 )
| ( sk_c1 != iPr_def_13 )
| ( sk_c9 != iPr_def_13 ) ),
inference(instantiation,[status(thm)],[c_43846]) ).
tcf(c_67189,plain,
( ( sk_c9 = sk_c1 )
| ( sk_c1 != iPr_def_14 )
| ( sk_c9 != iPr_def_14 ) ),
inference(instantiation,[status(thm)],[c_43846]) ).
tcf(c_67245,plain,
( ( iPr_def_20 = iPr_def_23 )
| ( multiply(iPr_def_13,sk_c10) = iPr_def_13 ) ),
inference(superposition,[status(thm)],[c_3666,c_66221]) ).
tcf(c_67285,plain,
( ( iPr_def_20 = iPr_def_23 )
| ( identity = iPr_def_13 ) ),
inference(light_normalisation,[status(thm)],[c_67245,c_52081]) ).
tcf(c_67799,plain,
( ( iPr_def_24 = identity )
| ( iPr_def_24 != iPr_def_21 )
| ( identity != iPr_def_21 ) ),
inference(instantiation,[status(thm)],[c_12190]) ).
tcf(c_68459,plain,
( ( iPr_def_18 = iPr_def_20 )
| ( multiply(iPr_def_25,iPr_def_26) = identity ) ),
inference(superposition,[status(thm)],[c_65840,c_1065]) ).
tcf(c_68464,plain,
( ( iPr_def_18 = iPr_def_20 )
| ( sk_c10 = identity ) ),
inference(light_normalisation,[status(thm)],[c_68459,c_5080]) ).
tcf(c_69535,plain,
( ( iPr_def_20 = iPr_def_23 )
| ( multiply(iPr_def_25,iPr_def_26) = identity ) ),
inference(superposition,[status(thm)],[c_66205,c_1065]) ).
tcf(c_69540,plain,
( ( iPr_def_20 = iPr_def_23 )
| ( sk_c10 = identity ) ),
inference(light_normalisation,[status(thm)],[c_69535,c_5080]) ).
tcf(c_70969,plain,
( ( iPr_def_26 = iPr_def_13 )
| ( iPr_def_26 != iPr_def_26 )
| ( iPr_def_13 != iPr_def_26 ) ),
inference(instantiation,[status(thm)],[c_29436]) ).
tcf(c_72823,plain,
( ( iPr_def_24 = iPr_def_13 )
| ( iPr_def_24 != iPr_def_21 )
| ( iPr_def_13 != iPr_def_21 ) ),
inference(instantiation,[status(thm)],[c_12190]) ).
tcf(c_74119,plain,
( ( sk_c9 = identity )
| ( identity != iPr_def_24 )
| ( sk_c9 != iPr_def_24 ) ),
inference(instantiation,[status(thm)],[c_1178]) ).
tcf(c_74641,plain,
multiply(inverse(multiply(inverse(iPr_def_24),sk_c2)),identity) = sk_c10,
inference(superposition,[status(thm)],[c_94,c_62422]) ).
tcf(c_75317,plain,
inverse(multiply(inverse(iPr_def_24),sk_c2)) = sk_c10,
inference(demodulation,[status(thm)],[c_74641,c_59441]) ).
tcf(c_75319,plain,
multiply(sk_c10,multiply(inverse(iPr_def_24),sk_c2)) = identity,
inference(superposition,[status(thm)],[c_75317,c_94]) ).
tcf(c_75619,plain,
( ( sk_c10 = iPr_def_20 )
| ( multiply(iPr_def_25,multiply(inverse(iPr_def_24),sk_c2)) = identity ) ),
inference(superposition,[status(thm)],[c_555,c_75319]) ).
tcf(c_75622,plain,
multiply(inverse(sk_c10),identity) = multiply(inverse(iPr_def_24),sk_c2),
inference(superposition,[status(thm)],[c_75319,c_50046]) ).
tcf(c_75629,plain,
multiply(inverse(iPr_def_24),sk_c2) = multiply(iPr_def_13,identity),
inference(light_normalisation,[status(thm)],[c_75622,c_61781]) ).
tcf(c_77714,plain,
( ( sk_c10 = iPr_def_20 )
| ( multiply(iPr_def_25,multiply(iPr_def_13,identity)) = identity ) ),
inference(light_normalisation,[status(thm)],[c_75619,c_75629]) ).
tcf(c_77715,plain,
( ( sk_c10 = iPr_def_20 )
| ( multiply(iPr_def_25,iPr_def_13) = identity ) ),
inference(demodulation,[status(thm)],[c_77714,c_59441]) ).
tcf(c_78151,plain,
! [X0: $i] :
( ( X0 = iPr_def_24 )
| ( iPr_def_24 != identity )
| ( X0 != identity ) ),
inference(instantiation,[status(thm)],[c_1461]) ).
tcf(c_78152,plain,
( ( sk_c10 = iPr_def_24 )
| ( iPr_def_24 != identity )
| ( sk_c10 != identity ) ),
inference(instantiation,[status(thm)],[c_78151]) ).
tcf(c_79314,plain,
( ( iPr_def_21 = iPr_def_24 )
| ~ iPr_def_11 ),
inference(global_subsumption_just,[status(thm)],[c_2920,c_2946,c_7416,c_12793,c_13577,c_16608,c_29743,c_30313,c_64508,c_67189]) ).
tcf(c_79320,plain,
( iPr_def_12
| ( iPr_def_21 = iPr_def_24 ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_12498,c_79314]) ).
tcf(c_79332,plain,
( ( iPr_def_15 = iPr_def_17 )
| ~ iPr_def_11 ),
inference(global_subsumption_just,[status(thm)],[c_2922,c_2946,c_7416,c_12793,c_13577,c_16613,c_29745,c_30315,c_64508,c_67189]) ).
tcf(c_79338,plain,
( iPr_def_12
| ( iPr_def_15 = iPr_def_17 ) ),
inference(backward_subsumption_resolution,[status(thm)],[c_12514,c_79332]) ).
tcf(c_80909,plain,
( ( iPr_def_21 = iPr_def_24 )
| ( inverse(iPr_def_13) = iPr_def_13 ) ),
inference(superposition,[status(thm)],[c_12439,c_30125]) ).
tcf(c_80933,plain,
( ( iPr_def_21 = iPr_def_24 )
| ( sk_c10 = iPr_def_13 ) ),
inference(light_normalisation,[status(thm)],[c_80909,c_51988]) ).
tcf(c_81063,plain,
( ( iPr_def_21 = iPr_def_24 )
| ( multiply(iPr_def_13,iPr_def_13) = identity ) ),
inference(superposition,[status(thm)],[c_80933,c_52081]) ).
tcf(c_81100,plain,
( ( iPr_def_21 = iPr_def_24 )
| ( iPr_def_13 = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_80933,c_1155]) ).
tcf(c_81120,plain,
( ( iPr_def_21 = iPr_def_24 )
| ( sk_c8 = identity ) ),
inference(light_normalisation,[status(thm)],[c_81063,c_51982]) ).
tcf(c_81262,plain,
( ( iPr_def_21 = iPr_def_24 )
| ( inverse(iPr_def_13) = sk_c1 ) ),
inference(superposition,[status(thm)],[c_81100,c_30305]) ).
tcf(c_81289,plain,
( ( iPr_def_21 = iPr_def_24 )
| ( sk_c10 = sk_c1 ) ),
inference(light_normalisation,[status(thm)],[c_81262,c_51988]) ).
tcf(c_81775,plain,
( ( sk_c10 = iPr_def_20 )
| ~ iPr_def_11
| ( inverse(iPr_def_13) != sk_c9 ) ),
inference(superposition,[status(thm)],[c_51982,c_2938]) ).
tcf(c_81782,plain,
( ( sk_c10 = iPr_def_20 )
| ~ iPr_def_11
| ( sk_c10 != sk_c9 ) ),
inference(light_normalisation,[status(thm)],[c_81775,c_51988]) ).
tcf(c_81959,plain,
( ( iPr_def_14 = iPr_def_13 )
| ( iPr_def_14 != iPr_def_14 )
| ( iPr_def_13 != iPr_def_14 ) ),
inference(instantiation,[status(thm)],[c_30295]) ).
tcf(c_82331,plain,
( ( iPr_def_21 = iPr_def_24 )
| ( sk_c1 = identity ) ),
inference(superposition,[status(thm)],[c_81120,c_13409]) ).
tcf(c_82796,plain,
( ( iPr_def_21 = iPr_def_24 )
| ( sk_c10 = identity ) ),
inference(superposition,[status(thm)],[c_82331,c_81289]) ).
tcf(c_84022,plain,
multiply(inverse(multiply(inverse(iPr_def_18),sk_c7)),identity) = sk_c9,
inference(superposition,[status(thm)],[c_94,c_62425]) ).
tcf(c_87577,plain,
inverse(multiply(inverse(iPr_def_18),sk_c7)) = sk_c9,
inference(demodulation,[status(thm)],[c_84022,c_59441]) ).
tcf(c_87587,plain,
multiply(sk_c9,multiply(inverse(iPr_def_18),sk_c7)) = identity,
inference(superposition,[status(thm)],[c_87577,c_94]) ).
tcf(c_87829,plain,
( ( sk_c10 = iPr_def_20 )
| ( multiply(iPr_def_13,multiply(inverse(iPr_def_18),sk_c7)) = identity ) ),
inference(superposition,[status(thm)],[c_545,c_87587]) ).
tcf(c_91201,plain,
( ( iPr_def_15 = iPr_def_17 )
| ( inverse(iPr_def_13) = iPr_def_13 ) ),
inference(superposition,[status(thm)],[c_3387,c_30282]) ).
tcf(c_91221,plain,
( ( iPr_def_15 = iPr_def_17 )
| ( sk_c10 = iPr_def_13 ) ),
inference(light_normalisation,[status(thm)],[c_91201,c_51988]) ).
tcf(c_91759,plain,
( ( iPr_def_15 = iPr_def_17 )
| ( multiply(iPr_def_13,iPr_def_13) = identity ) ),
inference(superposition,[status(thm)],[c_91221,c_52081]) ).
tcf(c_91798,plain,
( ( iPr_def_15 = iPr_def_17 )
| ( iPr_def_13 = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_91221,c_944]) ).
tcf(c_91816,plain,
( ( iPr_def_15 = iPr_def_17 )
| ( sk_c8 = identity ) ),
inference(light_normalisation,[status(thm)],[c_91759,c_51982]) ).
tcf(c_91947,plain,
( ( iPr_def_15 = iPr_def_17 )
| ( multiply(iPr_def_13,iPr_def_13) = sk_c10 ) ),
inference(superposition,[status(thm)],[c_91798,c_5143]) ).
tcf(c_91994,plain,
( ( iPr_def_15 = iPr_def_17 )
| ( sk_c10 = sk_c8 ) ),
inference(light_normalisation,[status(thm)],[c_91947,c_51982]) ).
tcf(c_92293,plain,
( ( iPr_def_15 = iPr_def_17 )
| ( sk_c1 = identity ) ),
inference(superposition,[status(thm)],[c_91816,c_13384]) ).
tcf(c_97610,plain,
( ( iPr_def_15 = iPr_def_17 )
| ( sk_c10 = identity ) ),
inference(superposition,[status(thm)],[c_91994,c_91816]) ).
tcf(c_98024,plain,
( ( iPr_def_15 = iPr_def_17 )
| ( inverse(identity) = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_92293,c_533]) ).
tcf(c_98027,plain,
( ( iPr_def_15 = iPr_def_17 )
| ( identity = iPr_def_25 ) ),
inference(light_normalisation,[status(thm)],[c_98024,c_12270]) ).
tcf(c_98881,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( sk_c10 = multiply(X0,X1) )
| ( sk_c10 != X2 )
| ( multiply(X0,X1) != X2 ) ),
inference(instantiation,[status(thm)],[c_581]) ).
tcf(c_98886,plain,
! [X0: $i,X1: $i] :
( ( sk_c9 = X0 )
| ( sk_c9 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_581]) ).
tcf(c_98900,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( multiply(X0,X1) = X3 )
| ( X3 != X2 )
| ( multiply(X0,X1) != X2 ) ),
inference(instantiation,[status(thm)],[c_581]) ).
tcf(c_98985,plain,
! [X0: $i] :
( ( sk_c10 = identity )
| ( identity != X0 )
| ( sk_c10 != X0 ) ),
inference(instantiation,[status(thm)],[c_581]) ).
tcf(c_99003,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( inverse(X0) = X2 )
| ( X2 != X1 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_581]) ).
tcf(c_99017,plain,
! [X0: $i,X1: $i] :
( ( X0 = sk_c9 )
| ( sk_c9 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_581]) ).
tcf(c_99040,plain,
! [X0: $i,X1: $i] :
( ( multiply(identity,X0) = X1 )
| ( X1 != X0 )
| ( multiply(identity,X0) != X0 ) ),
inference(instantiation,[status(thm)],[c_98900]) ).
tcf(c_99162,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = inverse(X0) )
| ( X2 != X1 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_581]) ).
tcf(c_99353,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( inverse(X0) = X2 )
| ( X2 != inverse(X1) )
| ( inverse(X0) != inverse(X1) ) ),
inference(instantiation,[status(thm)],[c_99003]) ).
tcf(c_99468,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( X3 = multiply(X0,X1) )
| ( X3 != X2 )
| ( multiply(X0,X1) != X2 ) ),
inference(instantiation,[status(thm)],[c_581]) ).
tcf(c_101016,plain,
! [X0: $i] :
( ( multiply(sk_c4,sk_c7) = X0 )
| ( X0 != iPr_def_20 )
| ( multiply(sk_c4,sk_c7) != iPr_def_20 ) ),
inference(instantiation,[status(thm)],[c_98900]) ).
tcf(c_101017,plain,
( ( sk_c10 = multiply(sk_c4,sk_c7) )
| ( sk_c10 != iPr_def_20 )
| ( multiply(sk_c4,sk_c7) != iPr_def_20 ) ),
inference(instantiation,[status(thm)],[c_98881]) ).
tcf(c_101220,plain,
! [X0: $i] :
( ( X0 = multiply(sk_c4,sk_c7) )
| ( X0 != iPr_def_20 )
| ( multiply(sk_c4,sk_c7) != iPr_def_20 ) ),
inference(instantiation,[status(thm)],[c_99468]) ).
tcf(c_102199,plain,
! [X0: $i,X1: $i] :
( ( X1 = inverse(X0) )
| ( X1 != iPr_def_14 )
| ( inverse(X0) != iPr_def_14 ) ),
inference(instantiation,[status(thm)],[c_99162]) ).
tcf(c_103562,plain,
! [X0: $i] :
( ( multiply(identity,identity) = X0 )
| ( X0 != identity )
| ( multiply(identity,identity) != identity ) ),
inference(instantiation,[status(thm)],[c_99040]) ).
tcf(c_103563,plain,
( ( multiply(identity,identity) = sk_c10 )
| ( sk_c10 != identity )
| ( multiply(identity,identity) != identity ) ),
inference(instantiation,[status(thm)],[c_103562]) ).
tcf(c_104874,plain,
! [X0: $i,X1: $i] :
( ( inverse(X1) = multiply(sk_c4,sk_c7) )
| ( inverse(X1) != inverse(X0) )
| ( multiply(sk_c4,sk_c7) != inverse(X0) ) ),
inference(instantiation,[status(thm)],[c_99353]) ).
tcf(c_104876,plain,
( ( inverse(sk_c10) = multiply(sk_c4,sk_c7) )
| ( inverse(sk_c10) != inverse(sk_c10) )
| ( multiply(sk_c4,sk_c7) != inverse(sk_c10) ) ),
inference(instantiation,[status(thm)],[c_104874]) ).
tcf(c_112010,plain,
! [X0: $i] :
( ( multiply(sk_c4,sk_c7) = inverse(X0) )
| ( inverse(X0) != iPr_def_14 )
| ( multiply(sk_c4,sk_c7) != iPr_def_14 ) ),
inference(instantiation,[status(thm)],[c_102199]) ).
tcf(c_112011,plain,
( ( multiply(sk_c4,sk_c7) = iPr_def_14 )
| ( iPr_def_14 != iPr_def_20 )
| ( multiply(sk_c4,sk_c7) != iPr_def_20 ) ),
inference(instantiation,[status(thm)],[c_101016]) ).
tcf(c_112012,plain,
( ( multiply(sk_c4,sk_c7) = inverse(sk_c10) )
| ( inverse(sk_c10) != iPr_def_14 )
| ( multiply(sk_c4,sk_c7) != iPr_def_14 ) ),
inference(instantiation,[status(thm)],[c_112010]) ).
tcf(c_117566,plain,
! [X0: $i,X1: $i] :
( ( inverse(X0) = X1 )
| ( X1 != multiply(sk_c4,sk_c7) )
| ( inverse(X0) != multiply(sk_c4,sk_c7) ) ),
inference(instantiation,[status(thm)],[c_99003]) ).
tcf(c_117570,plain,
( ( inverse(sk_c10) = sk_c10 )
| ( sk_c10 != multiply(sk_c4,sk_c7) )
| ( inverse(sk_c10) != multiply(sk_c4,sk_c7) ) ),
inference(instantiation,[status(thm)],[c_117566]) ).
tcf(c_117600,plain,
( ( identity = multiply(sk_c4,sk_c7) )
| ( identity != iPr_def_20 )
| ( multiply(sk_c4,sk_c7) != iPr_def_20 ) ),
inference(instantiation,[status(thm)],[c_101220]) ).
tcf(c_117605,plain,
( ( sk_c10 = identity )
| ( identity != multiply(sk_c4,sk_c7) )
| ( sk_c10 != multiply(sk_c4,sk_c7) ) ),
inference(instantiation,[status(thm)],[c_98985]) ).
tcf(c_121408,plain,
! [X0: $i] :
( ( X0 = sk_c9 )
| ( sk_c9 != identity )
| ( X0 != identity ) ),
inference(instantiation,[status(thm)],[c_99017]) ).
tcf(c_121410,plain,
! [X0: $i] :
( ( sk_c9 = X0 )
| ( sk_c9 != identity )
| ( X0 != identity ) ),
inference(instantiation,[status(thm)],[c_98886]) ).
tcf(c_121411,plain,
( ( sk_c9 = sk_c10 )
| ( sk_c9 != identity )
| ( sk_c10 != identity ) ),
inference(instantiation,[status(thm)],[c_121410]) ).
tcf(c_121413,plain,
( ( sk_c10 = sk_c9 )
| ( sk_c9 != identity )
| ( sk_c10 != identity ) ),
inference(instantiation,[status(thm)],[c_121408]) ).
tcf(c_122975,plain,
! [X0: $i] :
( ~ iPr_def_12
| ( inverse(X0) != identity )
| ( multiply(inverse(X0),sk_c9) != sk_c10 )
| ( multiply(X0,inverse(X0)) != sk_c10 ) ),
inference(light_normalisation,[status(thm)],[c_3206,c_12270]) ).
tcf(c_122988,plain,
( ~ iPr_def_12
| ( inverse(identity) != identity )
| ( inverse(identity) != sk_c10 )
| ( multiply(inverse(identity),sk_c9) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_93,c_122975]) ).
tcf(c_123018,plain,
( ~ iPr_def_12
| ( inverse(identity) != identity )
| ( multiply(identity,identity) != sk_c10 )
| ( multiply(inverse(identity),sk_c9) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_12270,c_122975]) ).
tcf(c_123053,plain,
( ~ iPr_def_12
| ( inverse(identity) != sk_c10 )
| ( multiply(inverse(identity),sk_c9) != sk_c10 ) ),
inference(ground_joinability,[status(thm)],[c_122988,c_12270]) ).
tcf(c_123054,plain,
( ~ iPr_def_12
| ( sk_c10 != identity )
| ( multiply(identity,sk_c9) != sk_c10 ) ),
inference(light_normalisation,[status(thm)],[c_123053,c_12270]) ).
tcf(c_123082,plain,
( ~ iPr_def_12
| ( multiply(identity,identity) != sk_c10 )
| ( multiply(inverse(identity),sk_c9) != sk_c10 ) ),
inference(ground_joinability,[status(thm)],[c_123018,c_12270]) ).
tcf(c_123083,plain,
( ~ iPr_def_12
| ( multiply(identity,identity) != sk_c10 )
| ( multiply(identity,sk_c9) != sk_c10 ) ),
inference(light_normalisation,[status(thm)],[c_123082,c_12270]) ).
tcf(c_124164,plain,
! [X0: $i] :
( ( sk_c9 = iPr_def_13 )
| ( multiply(iPr_def_22,X0) = X0 ) ),
inference(light_normalisation,[status(thm)],[c_6198,c_18621]) ).
tcf(c_124189,plain,
( ( sk_c9 = iPr_def_13 )
| ( sk_c10 = iPr_def_13 ) ),
inference(superposition,[status(thm)],[c_124164,c_882]) ).
tcf(c_124443,plain,
iPr_def_15 = iPr_def_17,
inference(global_subsumption_just,[status(thm)],[c_98027,c_1110,c_1242,c_3062,c_3063,c_3387,c_18716,c_30148,c_56880,c_70969,c_79338,c_91221,c_97610,c_123054]) ).
tcf(c_124497,plain,
( ( sk_c5 = iPr_def_15 )
| ( sk_c10 = iPr_def_25 ) ),
inference(demodulation,[status(thm)],[c_552,c_124443]) ).
tcf(c_124564,plain,
sk_c10 = iPr_def_25,
inference(global_subsumption_just,[status(thm)],[c_124497,c_1110,c_1155,c_1251,c_1517,c_1518,c_1545,c_2040,c_3653,c_4082,c_4922,c_6369,c_6785,c_12194,c_12814,c_22165,c_23466,c_24216,c_51895,c_51894,c_54718,c_67799,c_78152,c_101017,c_117600,c_117605,c_123054,c_124189]) ).
tcf(c_124668,plain,
inverse(iPr_def_25) = iPr_def_13,
inference(demodulation,[status(thm)],[c_52082,c_124564]) ).
tcf(c_124712,plain,
! [X0: $i] : multiply(sk_c8,multiply(iPr_def_25,X0)) = multiply(iPr_def_13,X0),
inference(demodulation,[status(thm)],[c_2295,c_124564]) ).
tcf(c_125039,plain,
sk_c1 = iPr_def_13,
inference(demodulation,[status(thm)],[c_30305,c_124668]) ).
tcf(c_130873,plain,
iPr_def_14 = iPr_def_26,
inference(global_subsumption_just,[status(thm)],[c_37321,c_584,c_586,c_522,c_1110,c_1517,c_1518,c_1843,c_2868,c_4082,c_4922,c_12194,c_13280,c_17804,c_23750,c_24200,c_24216,c_41436,c_46771,c_49440,c_49569,c_54718,c_60729,c_67799,c_74119,c_78152,c_101017,c_104876,c_112012,c_112011,c_117570,c_117600,c_117605,c_121411,c_123054]) ).
tcf(c_130875,plain,
iPr_def_13 = iPr_def_26,
inference(light_normalisation,[status(thm)],[c_130873,c_61658]) ).
tcf(c_130937,plain,
multiply(iPr_def_25,iPr_def_13) = sk_c10,
inference(demodulation,[status(thm)],[c_37488,c_130875]) ).
tcf(c_130988,plain,
( ( sk_c10 = iPr_def_20 )
| ( sk_c10 = identity ) ),
inference(demodulation,[status(thm)],[c_77715,c_130937]) ).
tcf(c_131060,plain,
sk_c10 = iPr_def_20,
inference(global_subsumption_just,[status(thm)],[c_87829,c_1110,c_1689,c_2336,c_7166,c_12530,c_14396,c_64508,c_81782,c_103563,c_121413,c_123083,c_130988]) ).
tcf(c_131078,plain,
multiply(inverse(sk_c8),iPr_def_13) = iPr_def_20,
inference(demodulation,[status(thm)],[c_50083,c_131060]) ).
tcf(c_131081,plain,
( iPr_def_12
| iPr_def_11
| ( iPr_def_18 = iPr_def_20 ) ),
inference(demodulation,[status(thm)],[c_44347,c_131060]) ).
tcf(c_131111,plain,
multiply(iPr_def_23,iPr_def_24) = iPr_def_20,
inference(demodulation,[status(thm)],[c_36880,c_131060]) ).
tcf(c_131124,plain,
( ( iPr_def_20 = iPr_def_25 )
| ( iPr_def_20 = iPr_def_23 ) ),
inference(demodulation,[status(thm)],[c_558,c_131060]) ).
tcf(c_131129,plain,
multiply(sk_c8,iPr_def_20) = iPr_def_13,
inference(demodulation,[status(thm)],[c_521,c_131060]) ).
tcf(c_131136,plain,
( ( iPr_def_20 = iPr_def_23 )
| ( sk_c9 = iPr_def_13 ) ),
inference(demodulation,[status(thm)],[c_548,c_131060]) ).
tcf(c_131142,plain,
( ( iPr_def_18 = iPr_def_20 )
| ( sk_c9 = iPr_def_13 ) ),
inference(demodulation,[status(thm)],[c_543,c_131060]) ).
tcf(c_131310,plain,
iPr_def_20 = iPr_def_23,
inference(global_subsumption_just,[status(thm)],[c_131124,c_1110,c_1524,c_1525,c_2336,c_16610,c_43812,c_51895,c_51903,c_61427,c_67185,c_67285,c_69540,c_123054,c_125039,c_131136]) ).
tcf(c_131407,plain,
iPr_def_18 = iPr_def_20,
inference(global_subsumption_just,[status(thm)],[c_131081,c_522,c_529,c_1110,c_1467,c_1518,c_1521,c_1524,c_1525,c_1545,c_2336,c_2876,c_3074,c_3075,c_4082,c_4484,c_6308,c_12194,c_12856,c_13767,c_13840,c_13972,c_16611,c_17118,c_18917,c_24200,c_25277,c_33049,c_33057,c_33126,c_43812,c_47219,c_49441,c_49825,c_50572,c_50610,c_51816,c_51824,c_51822,c_51898,c_54105,c_64506,c_65801,c_67185,c_68464,c_81959,c_123054,c_125039,c_131142]) ).
tcf(c_131414,plain,
iPr_def_18 = iPr_def_23,
inference(demodulation,[status(thm)],[c_131310,c_131407]) ).
tcf(c_131416,plain,
sk_c10 = iPr_def_18,
inference(demodulation,[status(thm)],[c_131060,c_131407]) ).
tcf(c_131446,plain,
iPr_def_13 = iPr_def_26,
inference(global_subsumption_just,[status(thm)],[c_37326,c_1110,c_1466,c_1467,c_1517,c_1518,c_1545,c_1689,c_2040,c_2336,c_2574,c_2572,c_4082,c_4922,c_4927,c_7166,c_12187,c_12194,c_12530,c_14396,c_17805,c_20539,c_23915,c_24216,c_43800,c_51895,c_54718,c_60740,c_64508,c_67799,c_74119,c_78152,c_81782,c_101017,c_103563,c_117600,c_117605,c_121411,c_121413,c_123054,c_123083,c_124189,c_130988]) ).
tcf(c_131568,plain,
multiply(iPr_def_18,iPr_def_24) = iPr_def_18,
inference(light_normalisation,[status(thm)],[c_131111,c_131407,c_131414]) ).
tcf(c_131570,plain,
multiply(inverse(iPr_def_18),iPr_def_18) = iPr_def_24,
inference(superposition,[status(thm)],[c_131568,c_50046]) ).
tcf(c_131576,plain,
sk_c10 = iPr_def_25,
inference(global_subsumption_just,[status(thm)],[c_37338,c_1110,c_1155,c_1251,c_1517,c_1518,c_1545,c_2040,c_3653,c_4082,c_4922,c_6369,c_6785,c_12194,c_12814,c_22165,c_23466,c_24216,c_51895,c_51894,c_54718,c_67799,c_78152,c_101017,c_117600,c_117605,c_123054,c_124189]) ).
tcf(c_131578,plain,
iPr_def_18 = iPr_def_25,
inference(light_normalisation,[status(thm)],[c_131576,c_131416]) ).
tcf(c_131614,plain,
! [X0: $i] : multiply(sk_c8,multiply(iPr_def_25,X0)) = multiply(iPr_def_13,X0),
inference(global_subsumption_just,[status(thm)],[c_37376,c_124712]) ).
tcf(c_131616,plain,
! [X0: $i] : multiply(sk_c8,multiply(iPr_def_18,X0)) = multiply(iPr_def_13,X0),
inference(light_normalisation,[status(thm)],[c_131614,c_131578]) ).
tcf(c_131619,plain,
multiply(sk_c8,iPr_def_18) = multiply(iPr_def_13,iPr_def_24),
inference(superposition,[status(thm)],[c_131568,c_131616]) ).
tcf(c_131635,plain,
iPr_def_21 = iPr_def_24,
inference(global_subsumption_just,[status(thm)],[c_37394,c_1110,c_3062,c_3063,c_16452,c_18716,c_30148,c_56880,c_70969,c_79320,c_80933,c_82796,c_123054,c_131446]) ).
tcf(c_131734,plain,
multiply(iPr_def_13,iPr_def_21) = iPr_def_13,
inference(light_normalisation,[status(thm)],[c_131129,c_131407,c_131619,c_131635]) ).
tcf(c_131938,plain,
multiply(inverse(sk_c8),iPr_def_13) = iPr_def_18,
inference(light_normalisation,[status(thm)],[c_131078,c_131407]) ).
tcf(c_132547,plain,
( ( sk_c9 = iPr_def_24 )
| ( iPr_def_21 != iPr_def_26 ) ),
inference(global_subsumption_just,[status(thm)],[c_53906,c_1110,c_1466,c_1467,c_1517,c_1518,c_1545,c_1689,c_2040,c_2336,c_2574,c_2572,c_3062,c_3063,c_4082,c_4922,c_4927,c_6200,c_7166,c_12187,c_12194,c_12530,c_13842,c_14396,c_16452,c_17805,c_18716,c_20539,c_23915,c_24216,c_29435,c_30148,c_33050,c_43800,c_51895,c_54718,c_56880,c_60740,c_64508,c_67799,c_70969,c_72823,c_74119,c_78152,c_79320,c_80933,c_81782,c_82796,c_101017,c_103563,c_117600,c_117605,c_121411,c_121413,c_123054,c_123083,c_124189,c_130988]) ).
tcf(c_132549,plain,
( ( sk_c9 = iPr_def_21 )
| ( iPr_def_13 != iPr_def_21 ) ),
inference(light_normalisation,[status(thm)],[c_132547,c_130875,c_131635]) ).
tcf(c_133484,plain,
inverse(iPr_def_25) = iPr_def_13,
inference(global_subsumption_just,[status(thm)],[c_61744,c_124668]) ).
tcf(c_133486,plain,
inverse(iPr_def_18) = iPr_def_13,
inference(light_normalisation,[status(thm)],[c_133484,c_131578]) ).
tcf(c_133490,plain,
multiply(iPr_def_13,iPr_def_18) = identity,
inference(superposition,[status(thm)],[c_133486,c_94]) ).
tcf(c_133755,plain,
multiply(iPr_def_18,iPr_def_13) = iPr_def_18,
inference(light_normalisation,[status(thm)],[c_130937,c_131416,c_131578]) ).
tcf(c_133757,plain,
multiply(inverse(iPr_def_18),iPr_def_18) = iPr_def_13,
inference(superposition,[status(thm)],[c_133755,c_50046]) ).
tcf(c_133764,plain,
identity = iPr_def_13,
inference(light_normalisation,[status(thm)],[c_133757,c_131570,c_133486,c_133490]) ).
tcf(c_133774,plain,
multiply(iPr_def_13,iPr_def_18) = iPr_def_13,
inference(demodulation,[status(thm)],[c_133490,c_133764]) ).
tcf(c_133781,plain,
! [X0: $i] : multiply(X0,iPr_def_13) = X0,
inference(demodulation,[status(thm)],[c_59441,c_133764]) ).
tcf(c_133786,plain,
! [X0: $i] : multiply(iPr_def_13,X0) = X0,
inference(demodulation,[status(thm)],[c_93,c_133764]) ).
tcf(c_133791,plain,
iPr_def_13 = iPr_def_21,
inference(demodulation,[status(thm)],[c_131734,c_133786]) ).
tcf(c_133792,plain,
sk_c9 = iPr_def_21,
inference(backward_subsumption_resolution,[status(thm)],[c_132549,c_133791]) ).
tcf(c_133793,plain,
( iPr_def_12
| iPr_def_11 ),
inference(backward_subsumption_resolution,[status(thm)],[c_61969,c_133791]) ).
tcf(c_133800,plain,
iPr_def_13 = iPr_def_24,
inference(demodulation,[status(thm)],[c_131635,c_133791]) ).
tcf(c_133839,plain,
! [X0: $i] :
( ~ iPr_def_11
| ( inverse(X0) != iPr_def_21 )
| ( multiply(X0,iPr_def_21) != sk_c8 ) ),
inference(demodulation,[status(thm)],[c_538,c_133792]) ).
tcf(c_133880,plain,
inverse(sk_c8) = iPr_def_18,
inference(demodulation,[status(thm)],[c_131938,c_133781]) ).
tcf(c_133914,plain,
! [X0: $i] :
( ~ iPr_def_11
| ( X0 != sk_c8 )
| ( inverse(X0) != iPr_def_13 ) ),
inference(light_normalisation,[status(thm)],[c_133839,c_133781,c_133791]) ).
tcf(c_134126,plain,
iPr_def_13 = iPr_def_18,
inference(demodulation,[status(thm)],[c_133774,c_133786]) ).
tcf(c_134129,plain,
inverse(sk_c8) = iPr_def_13,
inference(demodulation,[status(thm)],[c_133880,c_134126]) ).
tcf(c_134140,plain,
sk_c10 = iPr_def_13,
inference(demodulation,[status(thm)],[c_131416,c_134126]) ).
tcf(c_134255,plain,
( ~ iPr_def_11
| ( sk_c8 != sk_c8 ) ),
inference(superposition,[status(thm)],[c_134129,c_133914]) ).
tcf(c_134257,plain,
~ iPr_def_11,
inference(equality_resolution_simp,[status(thm)],[c_134255]) ).
tcf(c_134258,plain,
iPr_def_12,
inference(backward_subsumption_resolution,[status(thm)],[c_133793,c_134257]) ).
tcf(c_134259,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_134258,c_134140,c_133764,c_133800,c_123054,c_61426,c_42829,c_33127,c_13767,c_1545,c_1521,c_1110]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : GRP375-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.14/0.42 % Computer : n026.cluster.edu
% 0.14/0.42 % Model : x86_64 x86_64
% 0.14/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.42 % Memory : 8046.5625MB
% 0.14/0.42 % OS : Linux 6.8.0-71-generic
% 0.14/0.42 % CPULimit : 300
% 0.14/0.42 % WCLimit : 300
% 0.14/0.43 % DateTime : Wed Sep 23 14:39:40 UTC 2026
% 0.14/0.43 % CPUTime :
% 0.14/0.43 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.14/0.48 Running first-order theorem proving
% 0.14/0.49 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.14/0.50
% 0.23/0.50 % ======== iProver multi-core TPTP/SMT =========
% 0.23/0.50
% 0.23/0.50 % Detected problem language: tptp
% 0.23/0.52 % Proving...
% 26.35/6.00 % SZS status Started for theBenchmark.p
% 26.35/6.00 % SZS status Unsatisfiable for theBenchmark.p
% 26.35/6.00
% 26.35/6.00 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 26.35/6.00
% 26.35/6.00 % ------ iProver source info
% 26.35/6.00
% 26.35/6.00 % git: date: 2026-07-19 20:42:38 +0200
% 26.35/6.00 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 26.35/6.00 % git: non_committed_changes: false
% 26.35/6.00
% 26.35/6.00 % ------ Parsing...% successful
% 26.35/6.00
% 26.35/6.00
% 26.35/6.00 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 26.35/6.00
% 26.35/6.00 % ------ Preprocessing... sup_sim: 0 sf_s rm: 0 0s sf_e pe_s pe_e %
% 26.35/6.00
% 26.35/6.00 % ------ Preprocessing... gs_s sp: 4 0s gs_e snvd_s sp: 0 0s snvd_e %
% 26.35/6.00
% 26.35/6.00 % ------ Preprocessing... sf_s rm: 0 0s sf_e
% 26.35/6.00 % ------ Proving...
% 26.35/6.00 % ------ Problem Properties
% 26.35/6.00
% 26.35/6.00 %
% 26.35/6.00 % clauses 61
% 26.35/6.00 % conjectures 44
% 26.35/6.00 % EPR 41
% 26.35/6.00 % Horn 20
% 26.35/6.00 % unary 17
% 26.35/6.00 % binary 40
% 26.35/6.00 % lits 113
% 26.35/6.00 % lits eq 107
% 26.35/6.00 % fd_pure 0
% 26.35/6.00 % fd_pseudo 0
% 26.35/6.00 % fd_cond 0
% 26.35/6.00 % fd_pseudo_cond 0
% 26.35/6.00 % AC symbols 0
% 26.35/6.00
% 26.35/6.00 % ------ Schedule dynamic 5 is on
% 26.35/6.00
% 26.35/6.00 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 26.35/6.00
% 26.35/6.00
% 26.35/6.00 % ------
% 26.35/6.00 % Current options:
% 26.35/6.00 % ------
% 26.35/6.00
% 26.35/6.00
% 26.35/6.00 %
% 26.35/6.00
% 26.35/6.00 % ------ Proving...
% 26.35/6.00 %
% 26.35/6.00
% 26.35/6.00 % SZS status Unsatisfiable for theBenchmark.p
% 26.35/6.00
% 26.35/6.00 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 27.25/6.02
% 27.25/6.02
%------------------------------------------------------------------------------