%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : GRP350-1 : TPTP v9.3.1. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% Computer : 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:19 PM UTC 2026
% Result : Unsatisfiable 55.46s 11.96s
% Output : CNFRefutation 55.46s
% Verified :
% SZS Type : Refutation
% Derivation depth : 31
% Number of leaves : 58
% Syntax : Number of formulae : 676 ( 180 unt; 14 def)
% Number of atoms : 2604 (1334 equ)
% Maximal formula atoms : 17 ( 3 avg)
% Number of connectives : 1173 ( 428 ~; 745 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 26 ( 3 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 21 ( 19 usr; 20 prp; 0-2 aty)
% Number of functors : 12 ( 12 usr; 10 con; 0-2 aty)
% Number of variables : 194 ( 0 sgn 194 !; 0 ?; 159 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0] : multiply(identity,X0) = X0,
file('/export/starexec/sandbox/benchmark/Axioms/GRP004-0.ax',left_identity) ).
fof(f2,axiom,
! [X0] : multiply(inverse(X0),X0) = identity,
file('/export/starexec/sandbox/benchmark/Axioms/GRP004-0.ax',left_inverse) ).
fof(f3,plain,
! [X0] : identity = multiply(inverse(X0),X0),
inference(reorient_equations,[],[f2]) ).
fof(f4,axiom,
! [X2,X0,X1] : multiply(multiply(X0,X1),X2) = multiply(X0,multiply(X1,X2)),
file('/export/starexec/sandbox/benchmark/Axioms/GRP004-0.ax',associativity) ).
fof(f5,negated_conjecture,
( multiply(sk_c3,sk_c11) = sk_c10
| multiply(sk_c10,sk_c11) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_1) ).
fof(f6,plain,
( sk_c10 = multiply(sk_c3,sk_c11)
| multiply(sk_c10,sk_c11) = sk_c9 ),
inference(reorient_equations,[],[f5]) ).
fof(f7,negated_conjecture,
( inverse(sk_c3) = sk_c11
| multiply(sk_c10,sk_c11) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_2) ).
fof(f8,plain,
( sk_c11 = inverse(sk_c3)
| multiply(sk_c10,sk_c11) = sk_c9 ),
inference(reorient_equations,[],[f7]) ).
fof(f9,negated_conjecture,
( multiply(sk_c4,sk_c10) = sk_c9
| multiply(sk_c10,sk_c11) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_3) ).
fof(f10,plain,
( sk_c9 = multiply(sk_c4,sk_c10)
| multiply(sk_c10,sk_c11) = sk_c9 ),
inference(reorient_equations,[],[f9]) ).
fof(f11,negated_conjecture,
( inverse(sk_c4) = sk_c10
| multiply(sk_c10,sk_c11) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_4) ).
fof(f12,plain,
( sk_c10 = inverse(sk_c4)
| multiply(sk_c10,sk_c11) = sk_c9 ),
inference(reorient_equations,[],[f11]) ).
fof(f13,negated_conjecture,
( multiply(sk_c5,sk_c8) = sk_c11
| multiply(sk_c10,sk_c11) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_5) ).
fof(f14,plain,
( sk_c11 = multiply(sk_c5,sk_c8)
| multiply(sk_c10,sk_c11) = sk_c9 ),
inference(reorient_equations,[],[f13]) ).
fof(f15,negated_conjecture,
( inverse(sk_c5) = sk_c8
| multiply(sk_c10,sk_c11) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_6) ).
fof(f16,plain,
( sk_c8 = inverse(sk_c5)
| multiply(sk_c10,sk_c11) = sk_c9 ),
inference(reorient_equations,[],[f15]) ).
fof(f24,negated_conjecture,
( multiply(sk_c3,sk_c11) = sk_c10
| inverse(sk_c10) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_11) ).
fof(f25,plain,
( sk_c10 = multiply(sk_c3,sk_c11)
| sk_c9 = inverse(sk_c10) ),
inference(reorient_equations,[],[f24]) ).
fof(f26,negated_conjecture,
( inverse(sk_c3) = sk_c11
| inverse(sk_c10) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_12) ).
fof(f27,plain,
( sk_c11 = inverse(sk_c3)
| sk_c9 = inverse(sk_c10) ),
inference(reorient_equations,[],[f26]) ).
fof(f32,negated_conjecture,
( multiply(sk_c5,sk_c8) = sk_c11
| inverse(sk_c10) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_15) ).
fof(f33,plain,
( sk_c11 = multiply(sk_c5,sk_c8)
| sk_c9 = inverse(sk_c10) ),
inference(reorient_equations,[],[f32]) ).
fof(f34,negated_conjecture,
( inverse(sk_c5) = sk_c8
| inverse(sk_c10) = sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_16) ).
fof(f35,plain,
( sk_c8 = inverse(sk_c5)
| sk_c9 = inverse(sk_c10) ),
inference(reorient_equations,[],[f34]) ).
fof(f44,negated_conjecture,
( multiply(sk_c3,sk_c11) = sk_c10
| multiply(sk_c9,sk_c11) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_21) ).
fof(f45,plain,
( sk_c10 = multiply(sk_c3,sk_c11)
| sk_c10 = multiply(sk_c9,sk_c11) ),
inference(reorient_equations,[],[f44]) ).
fof(f46,negated_conjecture,
( inverse(sk_c3) = sk_c11
| multiply(sk_c9,sk_c11) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_22) ).
fof(f47,plain,
( sk_c11 = inverse(sk_c3)
| sk_c10 = multiply(sk_c9,sk_c11) ),
inference(reorient_equations,[],[f46]) ).
fof(f50,negated_conjecture,
( inverse(sk_c4) = sk_c10
| multiply(sk_c9,sk_c11) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_24) ).
fof(f51,plain,
( sk_c10 = inverse(sk_c4)
| sk_c10 = multiply(sk_c9,sk_c11) ),
inference(reorient_equations,[],[f50]) ).
fof(f52,negated_conjecture,
( multiply(sk_c5,sk_c8) = sk_c11
| multiply(sk_c9,sk_c11) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_25) ).
fof(f53,plain,
( sk_c11 = multiply(sk_c5,sk_c8)
| sk_c10 = multiply(sk_c9,sk_c11) ),
inference(reorient_equations,[],[f52]) ).
fof(f54,negated_conjecture,
( inverse(sk_c5) = sk_c8
| multiply(sk_c9,sk_c11) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_26) ).
fof(f55,plain,
( sk_c8 = inverse(sk_c5)
| sk_c10 = multiply(sk_c9,sk_c11) ),
inference(reorient_equations,[],[f54]) ).
fof(f56,negated_conjecture,
( multiply(sk_c8,sk_c10) = sk_c11
| multiply(sk_c9,sk_c11) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_27) ).
fof(f57,plain,
( sk_c11 = multiply(sk_c8,sk_c10)
| sk_c10 = multiply(sk_c9,sk_c11) ),
inference(reorient_equations,[],[f56]) ).
fof(f64,negated_conjecture,
( multiply(sk_c3,sk_c11) = sk_c10
| inverse(sk_c1) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_31) ).
fof(f65,plain,
( sk_c10 = multiply(sk_c3,sk_c11)
| sk_c11 = inverse(sk_c1) ),
inference(reorient_equations,[],[f64]) ).
fof(f66,negated_conjecture,
( inverse(sk_c3) = sk_c11
| inverse(sk_c1) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_32) ).
fof(f67,plain,
( sk_c11 = inverse(sk_c3)
| sk_c11 = inverse(sk_c1) ),
inference(reorient_equations,[],[f66]) ).
fof(f70,negated_conjecture,
( inverse(sk_c4) = sk_c10
| inverse(sk_c1) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_34) ).
fof(f71,plain,
( sk_c10 = inverse(sk_c4)
| sk_c11 = inverse(sk_c1) ),
inference(reorient_equations,[],[f70]) ).
fof(f72,negated_conjecture,
( multiply(sk_c5,sk_c8) = sk_c11
| inverse(sk_c1) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_35) ).
fof(f73,plain,
( sk_c11 = multiply(sk_c5,sk_c8)
| sk_c11 = inverse(sk_c1) ),
inference(reorient_equations,[],[f72]) ).
fof(f76,negated_conjecture,
( multiply(sk_c8,sk_c10) = sk_c11
| inverse(sk_c1) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_37) ).
fof(f77,plain,
( sk_c11 = multiply(sk_c8,sk_c10)
| sk_c11 = inverse(sk_c1) ),
inference(reorient_equations,[],[f76]) ).
fof(f84,negated_conjecture,
( multiply(sk_c3,sk_c11) = sk_c10
| multiply(sk_c1,sk_c10) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_41) ).
fof(f85,plain,
( sk_c10 = multiply(sk_c3,sk_c11)
| sk_c11 = multiply(sk_c1,sk_c10) ),
inference(reorient_equations,[],[f84]) ).
fof(f86,negated_conjecture,
( inverse(sk_c3) = sk_c11
| multiply(sk_c1,sk_c10) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_42) ).
fof(f87,plain,
( sk_c11 = inverse(sk_c3)
| sk_c11 = multiply(sk_c1,sk_c10) ),
inference(reorient_equations,[],[f86]) ).
fof(f90,negated_conjecture,
( inverse(sk_c4) = sk_c10
| multiply(sk_c1,sk_c10) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_44) ).
fof(f91,plain,
( sk_c10 = inverse(sk_c4)
| sk_c11 = multiply(sk_c1,sk_c10) ),
inference(reorient_equations,[],[f90]) ).
fof(f96,negated_conjecture,
( multiply(sk_c8,sk_c10) = sk_c11
| multiply(sk_c1,sk_c10) = sk_c11 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_47) ).
fof(f97,plain,
( sk_c11 = multiply(sk_c8,sk_c10)
| sk_c11 = multiply(sk_c1,sk_c10) ),
inference(reorient_equations,[],[f96]) ).
fof(f104,negated_conjecture,
( multiply(sk_c3,sk_c11) = sk_c10
| inverse(sk_c2) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_51) ).
fof(f105,plain,
( sk_c10 = multiply(sk_c3,sk_c11)
| sk_c10 = inverse(sk_c2) ),
inference(reorient_equations,[],[f104]) ).
fof(f106,negated_conjecture,
( inverse(sk_c3) = sk_c11
| inverse(sk_c2) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_52) ).
fof(f107,plain,
( sk_c11 = inverse(sk_c3)
| sk_c10 = inverse(sk_c2) ),
inference(reorient_equations,[],[f106]) ).
fof(f108,negated_conjecture,
( multiply(sk_c4,sk_c10) = sk_c9
| inverse(sk_c2) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_53) ).
fof(f109,plain,
( sk_c9 = multiply(sk_c4,sk_c10)
| sk_c10 = inverse(sk_c2) ),
inference(reorient_equations,[],[f108]) ).
fof(f110,negated_conjecture,
( inverse(sk_c4) = sk_c10
| inverse(sk_c2) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_54) ).
fof(f111,plain,
( sk_c10 = inverse(sk_c4)
| sk_c10 = inverse(sk_c2) ),
inference(reorient_equations,[],[f110]) ).
fof(f124,negated_conjecture,
( multiply(sk_c3,sk_c11) = sk_c10
| multiply(sk_c2,sk_c9) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_61) ).
fof(f125,plain,
( sk_c10 = multiply(sk_c3,sk_c11)
| sk_c10 = multiply(sk_c2,sk_c9) ),
inference(reorient_equations,[],[f124]) ).
fof(f126,negated_conjecture,
( inverse(sk_c3) = sk_c11
| multiply(sk_c2,sk_c9) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_62) ).
fof(f127,plain,
( sk_c11 = inverse(sk_c3)
| sk_c10 = multiply(sk_c2,sk_c9) ),
inference(reorient_equations,[],[f126]) ).
fof(f128,negated_conjecture,
( multiply(sk_c4,sk_c10) = sk_c9
| multiply(sk_c2,sk_c9) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_63) ).
fof(f129,plain,
( sk_c9 = multiply(sk_c4,sk_c10)
| sk_c10 = multiply(sk_c2,sk_c9) ),
inference(reorient_equations,[],[f128]) ).
fof(f130,negated_conjecture,
( inverse(sk_c4) = sk_c10
| multiply(sk_c2,sk_c9) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_64) ).
fof(f131,plain,
( sk_c10 = inverse(sk_c4)
| sk_c10 = multiply(sk_c2,sk_c9) ),
inference(reorient_equations,[],[f130]) ).
fof(f132,negated_conjecture,
( multiply(sk_c5,sk_c8) = sk_c11
| multiply(sk_c2,sk_c9) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_65) ).
fof(f133,plain,
( sk_c11 = multiply(sk_c5,sk_c8)
| sk_c10 = multiply(sk_c2,sk_c9) ),
inference(reorient_equations,[],[f132]) ).
fof(f134,negated_conjecture,
( inverse(sk_c5) = sk_c8
| multiply(sk_c2,sk_c9) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_66) ).
fof(f135,plain,
( sk_c8 = inverse(sk_c5)
| sk_c10 = multiply(sk_c2,sk_c9) ),
inference(reorient_equations,[],[f134]) ).
fof(f136,negated_conjecture,
( multiply(sk_c8,sk_c10) = sk_c11
| multiply(sk_c2,sk_c9) = sk_c10 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_67) ).
fof(f137,plain,
( sk_c11 = multiply(sk_c8,sk_c10)
| sk_c10 = multiply(sk_c2,sk_c9) ),
inference(reorient_equations,[],[f136]) ).
fof(f144,negated_conjecture,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( multiply(X6,X5) != X7
| inverse(X7) != X5
| inverse(X6) != X7
| multiply(X5,sk_c10) != sk_c11
| inverse(X4) != X5
| multiply(X4,X5) != sk_c11
| inverse(X3) != sk_c10
| multiply(X3,sk_c10) != sk_c9
| inverse(X2) != sk_c11
| multiply(X2,sk_c11) != sk_c10
| multiply(X1,sk_c9) != sk_c10
| inverse(X1) != sk_c10
| multiply(X0,sk_c10) != sk_c11
| inverse(X0) != sk_c11
| multiply(sk_c9,sk_c11) != sk_c10
| inverse(sk_c10) != sk_c9
| multiply(sk_c10,sk_c11) != sk_c9 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_71) ).
fof(f145,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( multiply(X6,X5) != X7
| inverse(X7) != X5
| inverse(X6) != X7
| sk_c11 != multiply(X5,sk_c10)
| inverse(X4) != X5
| sk_c11 != multiply(X4,X5)
| sk_c10 != inverse(X3)
| sk_c9 != multiply(X3,sk_c10)
| sk_c11 != inverse(X2)
| sk_c10 != multiply(X2,sk_c11)
| sk_c10 != multiply(X1,sk_c9)
| sk_c10 != inverse(X1)
| sk_c11 != multiply(X0,sk_c10)
| inverse(X0) != sk_c11
| sk_c10 != multiply(sk_c9,sk_c11)
| sk_c9 != inverse(sk_c10)
| multiply(sk_c10,sk_c11) != sk_c9 ),
inference(reorient_equations,[],[f144]) ).
fof(f146,plain,
! [X2,X3,X0,X1,X6,X7,X4] :
( multiply(X6,inverse(X4)) != X7
| inverse(X4) != inverse(X7)
| inverse(X6) != X7
| sk_c11 != multiply(inverse(X4),sk_c10)
| sk_c11 != multiply(X4,inverse(X4))
| sk_c10 != inverse(X3)
| sk_c9 != multiply(X3,sk_c10)
| sk_c11 != inverse(X2)
| sk_c10 != multiply(X2,sk_c11)
| sk_c10 != multiply(X1,sk_c9)
| sk_c10 != inverse(X1)
| sk_c11 != multiply(X0,sk_c10)
| inverse(X0) != sk_c11
| sk_c10 != multiply(sk_c9,sk_c11)
| sk_c9 != inverse(sk_c10)
| multiply(sk_c10,sk_c11) != sk_c9 ),
inference(equality_resolution,[],[f145]) ).
fof(f147,plain,
! [X2,X3,X0,X1,X6,X4] :
( inverse(X6) != multiply(X6,inverse(X4))
| inverse(X4) != inverse(inverse(X6))
| sk_c11 != multiply(inverse(X4),sk_c10)
| sk_c11 != multiply(X4,inverse(X4))
| sk_c10 != inverse(X3)
| sk_c9 != multiply(X3,sk_c10)
| sk_c11 != inverse(X2)
| sk_c10 != multiply(X2,sk_c11)
| sk_c10 != multiply(X1,sk_c9)
| sk_c10 != inverse(X1)
| sk_c11 != multiply(X0,sk_c10)
| inverse(X0) != sk_c11
| sk_c10 != multiply(sk_c9,sk_c11)
| sk_c9 != inverse(sk_c10)
| multiply(sk_c10,sk_c11) != sk_c9 ),
inference(equality_resolution,[],[f146]) ).
tcf(c_123,plain,
! [X0: $i] : multiply(identity,X0) = X0,
inference(cnf_transformation,[],[f1]) ).
tcf(c_124,plain,
! [X0: $i] : multiply(inverse(X0),X0) = identity,
inference(cnf_transformation,[],[f3]) ).
tcf(c_125,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(multiply(X0,X1),X2) = multiply(X0,multiply(X1,X2)),
inference(cnf_transformation,[],[f4]) ).
tcf(c_126,negated_conjecture,
( ( multiply(sk_c3,sk_c11) = sk_c10 )
| ( multiply(sk_c10,sk_c11) = sk_c9 ) ),
inference(cnf_transformation,[],[f6]) ).
tcf(c_127,negated_conjecture,
( ( inverse(sk_c3) = sk_c11 )
| ( multiply(sk_c10,sk_c11) = sk_c9 ) ),
inference(cnf_transformation,[],[f8]) ).
tcf(c_128,negated_conjecture,
( ( multiply(sk_c4,sk_c10) = sk_c9 )
| ( multiply(sk_c10,sk_c11) = sk_c9 ) ),
inference(cnf_transformation,[],[f10]) ).
tcf(c_129,negated_conjecture,
( ( inverse(sk_c4) = sk_c10 )
| ( multiply(sk_c10,sk_c11) = sk_c9 ) ),
inference(cnf_transformation,[],[f12]) ).
tcf(c_130,negated_conjecture,
( ( multiply(sk_c5,sk_c8) = sk_c11 )
| ( multiply(sk_c10,sk_c11) = sk_c9 ) ),
inference(cnf_transformation,[],[f14]) ).
tcf(c_131,negated_conjecture,
( ( inverse(sk_c5) = sk_c8 )
| ( multiply(sk_c10,sk_c11) = sk_c9 ) ),
inference(cnf_transformation,[],[f16]) ).
tcf(c_136,negated_conjecture,
( ( inverse(sk_c10) = sk_c9 )
| ( multiply(sk_c3,sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f25]) ).
tcf(c_137,negated_conjecture,
( ( inverse(sk_c3) = sk_c11 )
| ( inverse(sk_c10) = sk_c9 ) ),
inference(cnf_transformation,[],[f27]) ).
tcf(c_140,negated_conjecture,
( ( inverse(sk_c10) = sk_c9 )
| ( multiply(sk_c5,sk_c8) = sk_c11 ) ),
inference(cnf_transformation,[],[f33]) ).
tcf(c_141,negated_conjecture,
( ( inverse(sk_c5) = sk_c8 )
| ( inverse(sk_c10) = sk_c9 ) ),
inference(cnf_transformation,[],[f35]) ).
tcf(c_146,negated_conjecture,
( ( multiply(sk_c3,sk_c11) = sk_c10 )
| ( multiply(sk_c9,sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f45]) ).
tcf(c_147,negated_conjecture,
( ( inverse(sk_c3) = sk_c11 )
| ( multiply(sk_c9,sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f47]) ).
tcf(c_149,negated_conjecture,
( ( inverse(sk_c4) = sk_c10 )
| ( multiply(sk_c9,sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f51]) ).
tcf(c_150,negated_conjecture,
( ( multiply(sk_c5,sk_c8) = sk_c11 )
| ( multiply(sk_c9,sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f53]) ).
tcf(c_151,negated_conjecture,
( ( inverse(sk_c5) = sk_c8 )
| ( multiply(sk_c9,sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f55]) ).
tcf(c_152,negated_conjecture,
( ( multiply(sk_c8,sk_c10) = sk_c11 )
| ( multiply(sk_c9,sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f57]) ).
tcf(c_156,negated_conjecture,
( ( inverse(sk_c1) = sk_c11 )
| ( multiply(sk_c3,sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f65]) ).
tcf(c_157,negated_conjecture,
( ( inverse(sk_c1) = sk_c11 )
| ( inverse(sk_c3) = sk_c11 ) ),
inference(cnf_transformation,[],[f67]) ).
tcf(c_159,negated_conjecture,
( ( inverse(sk_c1) = sk_c11 )
| ( inverse(sk_c4) = sk_c10 ) ),
inference(cnf_transformation,[],[f71]) ).
tcf(c_160,negated_conjecture,
( ( inverse(sk_c1) = sk_c11 )
| ( multiply(sk_c5,sk_c8) = sk_c11 ) ),
inference(cnf_transformation,[],[f73]) ).
tcf(c_162,negated_conjecture,
( ( inverse(sk_c1) = sk_c11 )
| ( multiply(sk_c8,sk_c10) = sk_c11 ) ),
inference(cnf_transformation,[],[f77]) ).
tcf(c_166,negated_conjecture,
( ( multiply(sk_c1,sk_c10) = sk_c11 )
| ( multiply(sk_c3,sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f85]) ).
tcf(c_167,negated_conjecture,
( ( inverse(sk_c3) = sk_c11 )
| ( multiply(sk_c1,sk_c10) = sk_c11 ) ),
inference(cnf_transformation,[],[f87]) ).
tcf(c_169,negated_conjecture,
( ( inverse(sk_c4) = sk_c10 )
| ( multiply(sk_c1,sk_c10) = sk_c11 ) ),
inference(cnf_transformation,[],[f91]) ).
tcf(c_172,negated_conjecture,
( ( multiply(sk_c1,sk_c10) = sk_c11 )
| ( multiply(sk_c8,sk_c10) = sk_c11 ) ),
inference(cnf_transformation,[],[f97]) ).
tcf(c_176,negated_conjecture,
( ( inverse(sk_c2) = sk_c10 )
| ( multiply(sk_c3,sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f105]) ).
tcf(c_177,negated_conjecture,
( ( inverse(sk_c2) = sk_c10 )
| ( inverse(sk_c3) = sk_c11 ) ),
inference(cnf_transformation,[],[f107]) ).
tcf(c_178,negated_conjecture,
( ( inverse(sk_c2) = sk_c10 )
| ( multiply(sk_c4,sk_c10) = sk_c9 ) ),
inference(cnf_transformation,[],[f109]) ).
tcf(c_179,negated_conjecture,
( ( inverse(sk_c2) = sk_c10 )
| ( inverse(sk_c4) = sk_c10 ) ),
inference(cnf_transformation,[],[f111]) ).
tcf(c_186,negated_conjecture,
( ( multiply(sk_c2,sk_c9) = sk_c10 )
| ( multiply(sk_c3,sk_c11) = sk_c10 ) ),
inference(cnf_transformation,[],[f125]) ).
tcf(c_187,negated_conjecture,
( ( inverse(sk_c3) = sk_c11 )
| ( multiply(sk_c2,sk_c9) = sk_c10 ) ),
inference(cnf_transformation,[],[f127]) ).
tcf(c_188,negated_conjecture,
( ( multiply(sk_c2,sk_c9) = sk_c10 )
| ( multiply(sk_c4,sk_c10) = sk_c9 ) ),
inference(cnf_transformation,[],[f129]) ).
tcf(c_189,negated_conjecture,
( ( inverse(sk_c4) = sk_c10 )
| ( multiply(sk_c2,sk_c9) = sk_c10 ) ),
inference(cnf_transformation,[],[f131]) ).
tcf(c_190,negated_conjecture,
( ( multiply(sk_c2,sk_c9) = sk_c10 )
| ( multiply(sk_c5,sk_c8) = sk_c11 ) ),
inference(cnf_transformation,[],[f133]) ).
tcf(c_191,negated_conjecture,
( ( inverse(sk_c5) = sk_c8 )
| ( multiply(sk_c2,sk_c9) = sk_c10 ) ),
inference(cnf_transformation,[],[f135]) ).
tcf(c_192,negated_conjecture,
( ( multiply(sk_c2,sk_c9) = sk_c10 )
| ( multiply(sk_c8,sk_c10) = sk_c11 ) ),
inference(cnf_transformation,[],[f137]) ).
tcf(c_196,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( ( inverse(sk_c10) != sk_c9 )
| ( inverse(X5) != sk_c10 )
| ( inverse(X4) != sk_c11 )
| ( inverse(X3) != sk_c10 )
| ( inverse(X2) != sk_c11 )
| ( multiply(sk_c9,sk_c11) != sk_c10 )
| ( multiply(sk_c10,sk_c11) != sk_c9 )
| ( inverse(inverse(X0)) != inverse(X1) )
| ( multiply(X5,sk_c10) != sk_c9 )
| ( multiply(X4,sk_c11) != sk_c10 )
| ( multiply(X3,sk_c9) != sk_c10 )
| ( multiply(X2,sk_c10) != sk_c11 )
| ( multiply(inverse(X1),sk_c10) != sk_c11 )
| ( multiply(X1,inverse(X1)) != sk_c11 )
| ( multiply(X0,inverse(X1)) != inverse(X0) ) ),
inference(cnf_transformation,[],[f147]) ).
tcf(c_198,plain,
multiply(inverse(sk_c10),sk_c10) = identity,
inference(instantiation,[status(thm)],[c_124]) ).
tcf(c_829,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_10
| ( inverse(X0) != sk_c11 )
| ( multiply(X0,sk_c11) != sk_c10 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_10])],[c_196]) ).
tcf(c_830,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_11
| ( inverse(X0) != sk_c10 )
| ( multiply(X0,sk_c9) != sk_c10 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_11])],[c_196]) ).
tcf(c_831,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_12
| ( inverse(X0) != sk_c10 )
| ( multiply(X0,sk_c10) != sk_c9 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_12])],[c_196]) ).
tcf(c_832,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_13
| ( inverse(X0) != sk_c11 )
| ( multiply(X0,sk_c10) != sk_c11 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_13])],[c_196]) ).
tcf(c_833,negated_conjecture,
! [X0: $i,X1: $i] :
( ~ iPr_def_14
| ( inverse(inverse(X0)) != inverse(X1) )
| ( multiply(inverse(X1),sk_c10) != sk_c11 )
| ( multiply(X1,inverse(X1)) != sk_c11 )
| ( multiply(X0,inverse(X1)) != inverse(X0) ) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_14])],[c_196]) ).
tcf(c_834,negated_conjecture,
( iPr_def_14
| iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( inverse(sk_c10) != sk_c9 )
| ( multiply(sk_c9,sk_c11) != sk_c10 )
| ( multiply(sk_c10,sk_c11) != sk_c9 ) ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_196]) ).
tcf(c_835,definition,
iPr_def_15 = multiply(sk_c10,sk_c11),
introduced(definition,[new_symbols(definition,[iPr_def_15])],[]) ).
tcf(c_836,definition,
iPr_def_16 = multiply(sk_c9,sk_c11),
introduced(definition,[new_symbols(definition,[iPr_def_16])],[]) ).
tcf(c_837,definition,
iPr_def_17 = inverse(sk_c10),
introduced(definition,[new_symbols(definition,[iPr_def_17])],[]) ).
tcf(c_839,definition,
iPr_def_19 = multiply(sk_c2,sk_c9),
introduced(definition,[new_symbols(definition,[iPr_def_19])],[]) ).
tcf(c_842,definition,
iPr_def_22 = multiply(sk_c8,sk_c10),
introduced(definition,[new_symbols(definition,[iPr_def_22])],[]) ).
tcf(c_843,definition,
iPr_def_23 = inverse(sk_c5),
introduced(definition,[new_symbols(definition,[iPr_def_23])],[]) ).
tcf(c_844,definition,
iPr_def_24 = multiply(sk_c5,sk_c8),
introduced(definition,[new_symbols(definition,[iPr_def_24])],[]) ).
tcf(c_845,definition,
iPr_def_25 = inverse(sk_c4),
introduced(definition,[new_symbols(definition,[iPr_def_25])],[]) ).
tcf(c_846,definition,
iPr_def_26 = multiply(sk_c4,sk_c10),
introduced(definition,[new_symbols(definition,[iPr_def_26])],[]) ).
tcf(c_847,definition,
iPr_def_27 = inverse(sk_c3),
introduced(definition,[new_symbols(definition,[iPr_def_27])],[]) ).
tcf(c_848,definition,
iPr_def_28 = multiply(sk_c3,sk_c11),
introduced(definition,[new_symbols(definition,[iPr_def_28])],[]) ).
tcf(c_849,definition,
iPr_def_29 = inverse(sk_c2),
introduced(definition,[new_symbols(definition,[iPr_def_29])],[]) ).
tcf(c_850,definition,
iPr_def_30 = multiply(sk_c1,sk_c10),
introduced(definition,[new_symbols(definition,[iPr_def_30])],[]) ).
tcf(c_851,definition,
iPr_def_31 = inverse(sk_c1),
introduced(definition,[new_symbols(definition,[iPr_def_31])],[]) ).
tcf(c_852,negated_conjecture,
( iPr_def_14
| iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( iPr_def_17 != sk_c9 )
| ( iPr_def_16 != sk_c10 )
| ( iPr_def_15 != sk_c9 ) ),
inference(demodulation,[status(thm)],[c_834,c_837,c_836,c_835]) ).
tcf(c_853,negated_conjecture,
! [X0: $i,X1: $i] :
( ~ iPr_def_14
| ( inverse(inverse(X0)) != inverse(X1) )
| ( multiply(inverse(X1),sk_c10) != sk_c11 )
| ( multiply(X1,inverse(X1)) != sk_c11 )
| ( multiply(X0,inverse(X1)) != inverse(X0) ) ),
inference(demodulation,[status(thm)],[c_833]) ).
tcf(c_854,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_13
| ( inverse(X0) != sk_c11 )
| ( multiply(X0,sk_c10) != sk_c11 ) ),
inference(demodulation,[status(thm)],[c_832]) ).
tcf(c_855,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_12
| ( inverse(X0) != sk_c10 )
| ( multiply(X0,sk_c10) != sk_c9 ) ),
inference(demodulation,[status(thm)],[c_831]) ).
tcf(c_856,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_11
| ( inverse(X0) != sk_c10 )
| ( multiply(X0,sk_c9) != sk_c10 ) ),
inference(demodulation,[status(thm)],[c_830]) ).
tcf(c_857,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_10
| ( inverse(X0) != sk_c11 )
| ( multiply(X0,sk_c11) != sk_c10 ) ),
inference(demodulation,[status(thm)],[c_829]) ).
tcf(c_861,negated_conjecture,
( ( iPr_def_22 = sk_c11 )
| ( iPr_def_19 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_192,c_842]) ).
tcf(c_862,negated_conjecture,
( ( iPr_def_23 = sk_c8 )
| ( iPr_def_19 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_191,c_843]) ).
tcf(c_863,negated_conjecture,
( ( iPr_def_24 = sk_c11 )
| ( iPr_def_19 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_190,c_844]) ).
tcf(c_864,negated_conjecture,
( ( iPr_def_25 = sk_c10 )
| ( iPr_def_19 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_189,c_845]) ).
tcf(c_865,negated_conjecture,
( ( iPr_def_26 = sk_c9 )
| ( iPr_def_19 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_188,c_846]) ).
tcf(c_866,negated_conjecture,
( ( iPr_def_27 = sk_c11 )
| ( iPr_def_19 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_187,c_847]) ).
tcf(c_867,negated_conjecture,
( ( iPr_def_28 = sk_c10 )
| ( iPr_def_19 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_186,c_848]) ).
tcf(c_874,negated_conjecture,
( ( iPr_def_29 = sk_c10 )
| ( iPr_def_25 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_179]) ).
tcf(c_875,negated_conjecture,
( ( iPr_def_29 = sk_c10 )
| ( iPr_def_26 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_178]) ).
tcf(c_876,negated_conjecture,
( ( iPr_def_29 = sk_c10 )
| ( iPr_def_27 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_177]) ).
tcf(c_877,negated_conjecture,
( ( iPr_def_29 = sk_c10 )
| ( iPr_def_28 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_176]) ).
tcf(c_881,negated_conjecture,
( ( iPr_def_30 = sk_c11 )
| ( iPr_def_22 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_172]) ).
tcf(c_884,negated_conjecture,
( ( iPr_def_30 = sk_c11 )
| ( iPr_def_25 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_169]) ).
tcf(c_886,negated_conjecture,
( ( iPr_def_30 = sk_c11 )
| ( iPr_def_27 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_167]) ).
tcf(c_887,negated_conjecture,
( ( iPr_def_30 = sk_c11 )
| ( iPr_def_28 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_166]) ).
tcf(c_891,negated_conjecture,
( ( iPr_def_31 = sk_c11 )
| ( iPr_def_22 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_162]) ).
tcf(c_893,negated_conjecture,
( ( iPr_def_31 = sk_c11 )
| ( iPr_def_24 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_160]) ).
tcf(c_894,negated_conjecture,
( ( iPr_def_31 = sk_c11 )
| ( iPr_def_25 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_159]) ).
tcf(c_896,negated_conjecture,
( ( iPr_def_31 = sk_c11 )
| ( iPr_def_27 = sk_c11 ) ),
inference(demodulation,[status(thm)],[c_157]) ).
tcf(c_897,negated_conjecture,
( ( iPr_def_31 = sk_c11 )
| ( iPr_def_28 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_156]) ).
tcf(c_901,negated_conjecture,
( ( iPr_def_22 = sk_c11 )
| ( iPr_def_16 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_152]) ).
tcf(c_902,negated_conjecture,
( ( iPr_def_23 = sk_c8 )
| ( iPr_def_16 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_151]) ).
tcf(c_903,negated_conjecture,
( ( iPr_def_24 = sk_c11 )
| ( iPr_def_16 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_150]) ).
tcf(c_904,negated_conjecture,
( ( iPr_def_25 = sk_c10 )
| ( iPr_def_16 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_149]) ).
tcf(c_906,negated_conjecture,
( ( iPr_def_27 = sk_c11 )
| ( iPr_def_16 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_147]) ).
tcf(c_907,negated_conjecture,
( ( iPr_def_28 = sk_c10 )
| ( iPr_def_16 = sk_c10 ) ),
inference(demodulation,[status(thm)],[c_146]) ).
tcf(c_912,negated_conjecture,
( ( iPr_def_23 = sk_c8 )
| ( iPr_def_17 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_141]) ).
tcf(c_913,negated_conjecture,
( ( iPr_def_24 = sk_c11 )
| ( iPr_def_17 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_140]) ).
tcf(c_916,negated_conjecture,
( ( iPr_def_27 = sk_c11 )
| ( iPr_def_17 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_137]) ).
tcf(c_917,negated_conjecture,
( ( iPr_def_28 = sk_c10 )
| ( iPr_def_17 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_136]) ).
tcf(c_922,negated_conjecture,
( ( iPr_def_23 = sk_c8 )
| ( iPr_def_15 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_131]) ).
tcf(c_923,negated_conjecture,
( ( iPr_def_24 = sk_c11 )
| ( iPr_def_15 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_130]) ).
tcf(c_924,negated_conjecture,
( ( iPr_def_25 = sk_c10 )
| ( iPr_def_15 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_129]) ).
tcf(c_925,negated_conjecture,
( ( iPr_def_26 = sk_c9 )
| ( iPr_def_15 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_128]) ).
tcf(c_926,negated_conjecture,
( ( iPr_def_27 = sk_c11 )
| ( iPr_def_15 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_127]) ).
tcf(c_927,negated_conjecture,
( ( iPr_def_28 = sk_c10 )
| ( iPr_def_15 = sk_c9 ) ),
inference(demodulation,[status(thm)],[c_126]) ).
tcf(c_928,plain,
! [X0: $i] : X0 = X0,
theory(equality) ).
tcf(c_929,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = X0 )
| ( X2 != X1 )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_930,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( multiply(X0,X2) = multiply(X1,X3) )
| ( X2 != X3 )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_931,plain,
! [X0: $i,X1: $i] :
( ( inverse(X0) = inverse(X1) )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_933,plain,
( ( inverse(sk_c10) = inverse(sk_c10) )
| ( sk_c10 != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_931]) ).
tcf(c_934,plain,
sk_c10 = sk_c10,
inference(instantiation,[status(thm)],[c_928]) ).
tcf(c_1358,plain,
( ( iPr_def_22 = iPr_def_24 )
| ( sk_c10 = iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_861,c_863]) ).
tcf(c_1394,plain,
( ( sk_c10 = iPr_def_19 )
| ( multiply(sk_c10,iPr_def_27) = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_866,c_835]) ).
tcf(c_1395,plain,
( ( iPr_def_24 = iPr_def_27 )
| ( sk_c10 = iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_866,c_863]) ).
tcf(c_1410,plain,
( ( iPr_def_25 = iPr_def_28 )
| ( sk_c10 = iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_867,c_864]) ).
tcf(c_1549,plain,
( ( sk_c10 = iPr_def_19 )
| ( multiply(sk_c5,iPr_def_23) = iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_862,c_844]) ).
tcf(c_1559,plain,
( ( sk_c10 = iPr_def_19 )
| ( multiply(sk_c4,iPr_def_28) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_867,c_846]) ).
tcf(c_1560,plain,
( ( sk_c10 = iPr_def_19 )
| ( multiply(sk_c4,iPr_def_25) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_864,c_846]) ).
tcf(c_1567,plain,
( ( sk_c10 = iPr_def_19 )
| ( multiply(sk_c3,iPr_def_27) = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_866,c_848]) ).
tcf(c_1596,plain,
( ( sk_c10 = iPr_def_25 )
| ( inverse(iPr_def_29) = iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_874,c_837]) ).
tcf(c_1633,plain,
( ( sk_c10 = iPr_def_29 )
| ( multiply(sk_c3,iPr_def_27) = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_876,c_848]) ).
tcf(c_1660,plain,
( ( sk_c10 = iPr_def_28 )
| ( inverse(iPr_def_29) = iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_877,c_837]) ).
tcf(c_1696,plain,
! [X0: $i] :
( ( iPr_def_15 = sk_c9 )
| ( iPr_def_15 != X0 )
| ( sk_c9 != X0 ) ),
inference(instantiation,[status(thm)],[c_929]) ).
tcf(c_1699,plain,
! [X0: $i,X1: $i] :
( ( sk_c9 = X0 )
| ( sk_c9 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_929]) ).
tcf(c_1723,plain,
! [X0: $i] :
( ( sk_c9 = X0 )
| ( sk_c9 != sk_c9 )
| ( X0 != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_1699]) ).
tcf(c_1724,plain,
sk_c9 = sk_c9,
inference(instantiation,[status(thm)],[c_928]) ).
tcf(c_1795,plain,
! [X0: $i] :
( ( sk_c9 = X0 )
| ( sk_c9 != iPr_def_26 )
| ( X0 != iPr_def_26 ) ),
inference(instantiation,[status(thm)],[c_1699]) ).
tcf(c_1829,plain,
( ( sk_c9 = iPr_def_15 )
| ( iPr_def_15 != sk_c9 )
| ( sk_c9 != sk_c9 ) ),
inference(instantiation,[status(thm)],[c_1723]) ).
tcf(c_1832,plain,
multiply(iPr_def_27,sk_c3) = identity,
inference(superposition,[status(thm)],[c_847,c_124]) ).
tcf(c_1833,plain,
multiply(iPr_def_25,sk_c4) = identity,
inference(superposition,[status(thm)],[c_845,c_124]) ).
tcf(c_1834,plain,
multiply(iPr_def_23,sk_c5) = identity,
inference(superposition,[status(thm)],[c_843,c_124]) ).
tcf(c_1837,plain,
multiply(iPr_def_17,sk_c10) = identity,
inference(superposition,[status(thm)],[c_837,c_124]) ).
tcf(c_1838,plain,
multiply(iPr_def_31,sk_c1) = identity,
inference(superposition,[status(thm)],[c_851,c_124]) ).
tcf(c_1839,plain,
multiply(iPr_def_29,sk_c2) = identity,
inference(superposition,[status(thm)],[c_849,c_124]) ).
tcf(c_1912,plain,
! [X0: $i] : inverse(X0) = inverse(X0),
inference(instantiation,[status(thm)],[c_928]) ).
tcf(c_1915,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( inverse(X0) = X2 )
| ( X2 != X1 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_929]) ).
tcf(c_1933,plain,
( ( sk_c10 = iPr_def_25 )
| ( multiply(sk_c10,iPr_def_30) = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_884,c_835]) ).
tcf(c_2120,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( inverse(X0) = X2 )
| ( X2 != inverse(X1) )
| ( inverse(X0) != inverse(X1) ) ),
inference(instantiation,[status(thm)],[c_1915]) ).
tcf(c_2211,plain,
( ( iPr_def_30 = iPr_def_31 )
| ( sk_c11 = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_891,c_881]) ).
tcf(c_2416,plain,
( ( iPr_def_30 = iPr_def_31 )
| ( sk_c10 = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_894,c_884]) ).
tcf(c_2511,plain,
( ( iPr_def_30 = iPr_def_31 )
| ( sk_c11 = iPr_def_27 ) ),
inference(superposition,[status(thm)],[c_896,c_886]) ).
tcf(c_2516,plain,
( ( sk_c11 = iPr_def_27 )
| ( multiply(sk_c3,iPr_def_31) = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_896,c_848]) ).
tcf(c_2517,plain,
( ( sk_c11 = iPr_def_27 )
| ( multiply(sk_c9,iPr_def_31) = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_896,c_836]) ).
tcf(c_2600,plain,
( ( iPr_def_30 = iPr_def_31 )
| ( sk_c10 = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_897,c_887]) ).
tcf(c_2870,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = inverse(X0) )
| ( X2 != X1 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_929]) ).
tcf(c_2873,plain,
! [X0: $i] :
( ( inverse(X0) = iPr_def_17 )
| ( iPr_def_17 != inverse(sk_c10) )
| ( inverse(X0) != inverse(sk_c10) ) ),
inference(instantiation,[status(thm)],[c_2120]) ).
tcf(c_2874,plain,
( ( inverse(sk_c10) = iPr_def_17 )
| ( iPr_def_17 != inverse(sk_c10) )
| ( inverse(sk_c10) != inverse(sk_c10) ) ),
inference(instantiation,[status(thm)],[c_2873]) ).
tcf(c_2881,plain,
! [X0: $i] :
( ( inverse(X0) = iPr_def_25 )
| ( iPr_def_25 != inverse(sk_c4) )
| ( inverse(X0) != inverse(sk_c4) ) ),
inference(instantiation,[status(thm)],[c_2120]) ).
tcf(c_2883,plain,
! [X0: $i] :
( ( inverse(X0) = iPr_def_27 )
| ( iPr_def_27 != inverse(sk_c3) )
| ( inverse(X0) != inverse(sk_c3) ) ),
inference(instantiation,[status(thm)],[c_2120]) ).
tcf(c_2884,plain,
( ( inverse(sk_c10) = iPr_def_27 )
| ( iPr_def_27 != inverse(sk_c3) )
| ( inverse(sk_c10) != inverse(sk_c3) ) ),
inference(instantiation,[status(thm)],[c_2883]) ).
tcf(c_2902,plain,
( ( sk_c10 = iPr_def_16 )
| ( multiply(sk_c5,iPr_def_23) = iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_902,c_844]) ).
tcf(c_2934,plain,
( ( iPr_def_22 = iPr_def_24 )
| ( sk_c10 = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_903,c_901]) ).
tcf(c_3026,plain,
( ( sk_c10 = iPr_def_16 )
| ( multiply(sk_c4,iPr_def_25) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_904,c_846]) ).
tcf(c_3108,plain,
( ( iPr_def_24 = iPr_def_27 )
| ( sk_c10 = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_906,c_903]) ).
tcf(c_3120,plain,
( ( sk_c10 = iPr_def_16 )
| ( multiply(sk_c3,iPr_def_27) = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_906,c_848]) ).
tcf(c_3217,plain,
( ( iPr_def_25 = iPr_def_28 )
| ( sk_c10 = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_907,c_904]) ).
tcf(c_3221,plain,
( ( sk_c10 = iPr_def_16 )
| ( multiply(sk_c1,iPr_def_28) = iPr_def_30 ) ),
inference(superposition,[status(thm)],[c_907,c_850]) ).
tcf(c_3502,plain,
( ( sk_c9 = iPr_def_17 )
| ( multiply(sk_c5,iPr_def_23) = iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_912,c_844]) ).
tcf(c_4116,plain,
( ( sk_c9 = iPr_def_15 )
| ( multiply(sk_c5,iPr_def_23) = iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_922,c_844]) ).
tcf(c_4148,plain,
( ( iPr_def_15 = iPr_def_17 )
| ( sk_c11 = iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_923,c_913]) ).
tcf(c_4154,plain,
( ( sk_c11 = iPr_def_24 )
| ( multiply(sk_c2,iPr_def_15) = iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_923,c_839]) ).
tcf(c_4253,plain,
( ( sk_c10 = iPr_def_25 )
| ( multiply(sk_c2,iPr_def_15) = iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_924,c_839]) ).
tcf(c_4373,plain,
( ( sk_c9 = iPr_def_15 )
| ( multiply(sk_c2,iPr_def_26) = iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_925,c_839]) ).
tcf(c_4447,plain,
( ( iPr_def_15 = iPr_def_17 )
| ( sk_c11 = iPr_def_27 ) ),
inference(superposition,[status(thm)],[c_926,c_916]) ).
tcf(c_4456,plain,
( ( sk_c11 = iPr_def_27 )
| ( multiply(sk_c2,iPr_def_15) = iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_926,c_839]) ).
tcf(c_4508,plain,
! [X0: $i,X1: $i] :
( ( inverse(X0) = X1 )
| ( X1 != iPr_def_17 )
| ( inverse(X0) != iPr_def_17 ) ),
inference(instantiation,[status(thm)],[c_1915]) ).
tcf(c_4555,plain,
( ( iPr_def_15 = iPr_def_17 )
| ( sk_c10 = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_927,c_917]) ).
tcf(c_4565,plain,
( ( sk_c10 = iPr_def_28 )
| ( multiply(sk_c2,iPr_def_15) = iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_927,c_839]) ).
tcf(c_4611,plain,
! [X0: $i] : multiply(sk_c10,multiply(sk_c11,X0)) = multiply(iPr_def_15,X0),
inference(superposition,[status(thm)],[c_835,c_125]) ).
tcf(c_4612,plain,
! [X0: $i] : multiply(sk_c3,multiply(sk_c11,X0)) = multiply(iPr_def_28,X0),
inference(superposition,[status(thm)],[c_848,c_125]) ).
tcf(c_4613,plain,
! [X0: $i] : multiply(sk_c4,multiply(sk_c10,X0)) = multiply(iPr_def_26,X0),
inference(superposition,[status(thm)],[c_846,c_125]) ).
tcf(c_4615,plain,
! [X0: $i] : multiply(sk_c8,multiply(sk_c10,X0)) = multiply(iPr_def_22,X0),
inference(superposition,[status(thm)],[c_842,c_125]) ).
tcf(c_4617,plain,
! [X0: $i] : multiply(sk_c9,multiply(sk_c11,X0)) = multiply(iPr_def_16,X0),
inference(superposition,[status(thm)],[c_836,c_125]) ).
tcf(c_4618,plain,
! [X0: $i] : multiply(sk_c1,multiply(sk_c10,X0)) = multiply(iPr_def_30,X0),
inference(superposition,[status(thm)],[c_850,c_125]) ).
tcf(c_4619,plain,
! [X0: $i] : multiply(sk_c2,multiply(sk_c9,X0)) = multiply(iPr_def_19,X0),
inference(superposition,[status(thm)],[c_839,c_125]) ).
tcf(c_4621,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(X0,X1)) = multiply(identity,X1),
inference(superposition,[status(thm)],[c_124,c_125]) ).
tcf(c_4623,plain,
! [X0: $i] : multiply(iPr_def_27,multiply(sk_c3,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1832,c_125]) ).
tcf(c_4624,plain,
! [X0: $i] : multiply(iPr_def_25,multiply(sk_c4,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1833,c_125]) ).
tcf(c_4625,plain,
! [X0: $i] : multiply(iPr_def_23,multiply(sk_c5,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1834,c_125]) ).
tcf(c_4628,plain,
! [X0: $i] : multiply(iPr_def_17,multiply(sk_c10,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1837,c_125]) ).
tcf(c_4629,plain,
! [X0: $i] : multiply(iPr_def_31,multiply(sk_c1,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1838,c_125]) ).
tcf(c_4630,plain,
! [X0: $i] : multiply(iPr_def_29,multiply(sk_c2,X0)) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_1839,c_125]) ).
tcf(c_4632,plain,
! [X0: $i] : multiply(iPr_def_29,multiply(sk_c2,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_4630,c_123]) ).
tcf(c_4633,plain,
! [X0: $i] : multiply(iPr_def_31,multiply(sk_c1,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_4629,c_123]) ).
tcf(c_4634,plain,
! [X0: $i] : multiply(iPr_def_17,multiply(sk_c10,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_4628,c_123]) ).
tcf(c_4637,plain,
! [X0: $i] : multiply(iPr_def_23,multiply(sk_c5,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_4625,c_123]) ).
tcf(c_4638,plain,
! [X0: $i] : multiply(iPr_def_25,multiply(sk_c4,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_4624,c_123]) ).
tcf(c_4639,plain,
! [X0: $i] : multiply(iPr_def_27,multiply(sk_c3,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_4623,c_123]) ).
tcf(c_4977,plain,
( ( inverse(sk_c4) = iPr_def_25 )
| ( iPr_def_25 != inverse(sk_c4) )
| ( inverse(sk_c4) != inverse(sk_c4) ) ),
inference(instantiation,[status(thm)],[c_2881]) ).
tcf(c_4978,plain,
inverse(sk_c4) = inverse(sk_c4),
inference(instantiation,[status(thm)],[c_1912]) ).
tcf(c_4988,plain,
! [X0: $i] :
( ( inverse(X0) = inverse(sk_c3) )
| ( X0 != sk_c3 ) ),
inference(instantiation,[status(thm)],[c_931]) ).
tcf(c_4989,plain,
( ( inverse(sk_c10) = inverse(sk_c3) )
| ( sk_c10 != sk_c3 ) ),
inference(instantiation,[status(thm)],[c_4988]) ).
tcf(c_4990,plain,
( ( inverse(sk_c3) = iPr_def_27 )
| ( iPr_def_27 != inverse(sk_c3) )
| ( inverse(sk_c3) != inverse(sk_c3) ) ),
inference(instantiation,[status(thm)],[c_2883]) ).
tcf(c_4991,plain,
inverse(sk_c3) = inverse(sk_c3),
inference(instantiation,[status(thm)],[c_1912]) ).
tcf(c_5029,plain,
( ~ iPr_def_13
| ( sk_c11 != iPr_def_30 )
| ( inverse(sk_c1) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_850,c_854]) ).
tcf(c_5030,plain,
( ~ iPr_def_13
| ( sk_c10 != sk_c11 )
| ( inverse(identity) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_123,c_854]) ).
tcf(c_5031,plain,
( ~ iPr_def_13
| ( sk_c11 != identity )
| ( inverse(inverse(sk_c10)) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_124,c_854]) ).
tcf(c_5050,plain,
( ~ iPr_def_13
| ( sk_c11 != iPr_def_31 )
| ( sk_c11 != iPr_def_30 ) ),
inference(light_normalisation,[status(thm)],[c_5029,c_851]) ).
tcf(c_5157,plain,
( ~ iPr_def_12
| ( sk_c10 != sk_c9 )
| ( inverse(identity) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_123,c_855]) ).
tcf(c_5160,plain,
( ~ iPr_def_12
| ( sk_c9 != identity )
| ( inverse(iPr_def_17) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_1837,c_855]) ).
tcf(c_5282,plain,
( ~ iPr_def_11
| ( sk_c10 != iPr_def_19 )
| ( inverse(sk_c2) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_839,c_856]) ).
tcf(c_5283,plain,
( ~ iPr_def_11
| ( sk_c10 != sk_c9 )
| ( inverse(identity) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_123,c_856]) ).
tcf(c_5306,plain,
( ~ iPr_def_11
| ( sk_c10 != iPr_def_29 )
| ( sk_c10 != iPr_def_19 ) ),
inference(light_normalisation,[status(thm)],[c_5282,c_849]) ).
tcf(c_5464,plain,
( ~ iPr_def_10
| ( sk_c10 != iPr_def_28 )
| ( inverse(sk_c3) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_848,c_857]) ).
tcf(c_5465,plain,
( ~ iPr_def_10
| ( sk_c10 != iPr_def_16 )
| ( inverse(sk_c9) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_836,c_857]) ).
tcf(c_5466,plain,
( ~ iPr_def_10
| ( sk_c10 != sk_c11 )
| ( inverse(identity) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_123,c_857]) ).
tcf(c_5467,plain,
( ~ iPr_def_10
| ( sk_c10 != identity )
| ( inverse(inverse(sk_c11)) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_124,c_857]) ).
tcf(c_5494,plain,
( ~ iPr_def_10
| ( sk_c11 != iPr_def_27 )
| ( sk_c10 != iPr_def_28 ) ),
inference(light_normalisation,[status(thm)],[c_5464,c_847]) ).
tcf(c_7423,plain,
( ( iPr_def_30 = iPr_def_31 )
| ( multiply(sk_c4,iPr_def_25) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_2416,c_846]) ).
tcf(c_7561,plain,
( ( iPr_def_30 = iPr_def_31 )
| ( multiply(sk_c3,iPr_def_27) = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_2511,c_848]) ).
tcf(c_7764,plain,
( ( iPr_def_30 = iPr_def_31 )
| ( multiply(iPr_def_28,sk_c11) = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_2600,c_835]) ).
tcf(c_8175,plain,
( ( iPr_def_22 = iPr_def_24 )
| ( iPr_def_16 = iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_2934,c_1358]) ).
tcf(c_8320,plain,
( ( iPr_def_24 = iPr_def_27 )
| ( iPr_def_16 = iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_3108,c_1395]) ).
tcf(c_8577,plain,
( ( iPr_def_25 = iPr_def_28 )
| ( iPr_def_16 = iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_3217,c_1410]) ).
tcf(c_9667,plain,
( ( iPr_def_15 = iPr_def_17 )
| ( multiply(sk_c3,iPr_def_27) = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_4447,c_848]) ).
tcf(c_9745,plain,
( ( iPr_def_15 = iPr_def_17 )
| ( inverse(iPr_def_28) = iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_4555,c_837]) ).
tcf(c_9746,plain,
( ( iPr_def_15 = iPr_def_17 )
| ( multiply(iPr_def_28,sk_c11) = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_4555,c_835]) ).
tcf(c_10012,plain,
multiply(iPr_def_29,iPr_def_19) = sk_c9,
inference(superposition,[status(thm)],[c_839,c_4632]) ).
tcf(c_10015,plain,
! [X0: $i] : multiply(iPr_def_29,multiply(iPr_def_19,X0)) = multiply(sk_c9,X0),
inference(superposition,[status(thm)],[c_10012,c_125]) ).
tcf(c_10017,plain,
multiply(iPr_def_31,iPr_def_30) = sk_c10,
inference(superposition,[status(thm)],[c_850,c_4633]) ).
tcf(c_10020,plain,
! [X0: $i] : multiply(iPr_def_31,multiply(iPr_def_30,X0)) = multiply(sk_c10,X0),
inference(superposition,[status(thm)],[c_10017,c_125]) ).
tcf(c_10022,plain,
multiply(iPr_def_17,iPr_def_15) = sk_c11,
inference(superposition,[status(thm)],[c_835,c_4634]) ).
tcf(c_10485,plain,
( ( sk_c10 = iPr_def_19 )
| ( multiply(iPr_def_17,iPr_def_15) = iPr_def_27 ) ),
inference(superposition,[status(thm)],[c_1394,c_4634]) ).
tcf(c_10486,plain,
( ( sk_c11 = iPr_def_27 )
| ( sk_c10 = iPr_def_19 ) ),
inference(light_normalisation,[status(thm)],[c_10485,c_10022]) ).
tcf(c_10505,plain,
multiply(iPr_def_23,iPr_def_24) = sk_c8,
inference(superposition,[status(thm)],[c_844,c_4637]) ).
tcf(c_10510,plain,
multiply(iPr_def_25,iPr_def_26) = sk_c10,
inference(superposition,[status(thm)],[c_846,c_4638]) ).
tcf(c_10513,plain,
! [X0: $i] : multiply(iPr_def_25,multiply(iPr_def_26,X0)) = multiply(sk_c10,X0),
inference(superposition,[status(thm)],[c_10510,c_125]) ).
tcf(c_10515,plain,
multiply(iPr_def_27,iPr_def_28) = sk_c11,
inference(superposition,[status(thm)],[c_848,c_4639]) ).
tcf(c_10518,plain,
! [X0: $i] : multiply(iPr_def_27,multiply(iPr_def_28,X0)) = multiply(sk_c11,X0),
inference(superposition,[status(thm)],[c_10515,c_125]) ).
tcf(c_11142,plain,
! [X0: $i] :
( ( X0 = inverse(sk_c4) )
| ( X0 != iPr_def_25 )
| ( inverse(sk_c4) != iPr_def_25 ) ),
inference(instantiation,[status(thm)],[c_2870]) ).
tcf(c_11486,plain,
! [X0: $i] :
( ( iPr_def_15 = sk_c9 )
| ( iPr_def_15 != inverse(X0) )
| ( sk_c9 != inverse(X0) ) ),
inference(instantiation,[status(thm)],[c_1696]) ).
tcf(c_12863,plain,
( ( sk_c10 = iPr_def_19 )
| ( multiply(iPr_def_25,iPr_def_26) = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_1559,c_4638]) ).
tcf(c_12864,plain,
( ( sk_c10 = iPr_def_28 )
| ( sk_c10 = iPr_def_19 ) ),
inference(light_normalisation,[status(thm)],[c_12863,c_10510]) ).
tcf(c_18057,plain,
( ( sk_c11 = iPr_def_27 )
| ( multiply(iPr_def_27,iPr_def_28) = iPr_def_31 ) ),
inference(superposition,[status(thm)],[c_2516,c_4639]) ).
tcf(c_18058,plain,
( ( sk_c11 = iPr_def_31 )
| ( sk_c11 = iPr_def_27 ) ),
inference(light_normalisation,[status(thm)],[c_18057,c_10515]) ).
tcf(c_20078,plain,
( ( sk_c10 = iPr_def_16 )
| ( multiply(iPr_def_27,iPr_def_28) = iPr_def_27 ) ),
inference(superposition,[status(thm)],[c_3120,c_4639]) ).
tcf(c_20079,plain,
( ( sk_c11 = iPr_def_27 )
| ( sk_c10 = iPr_def_16 ) ),
inference(light_normalisation,[status(thm)],[c_20078,c_10515]) ).
tcf(c_20423,plain,
( ( sk_c10 = iPr_def_16 )
| ( multiply(iPr_def_31,iPr_def_30) = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_3221,c_4633]) ).
tcf(c_20424,plain,
( ( sk_c10 = iPr_def_28 )
| ( sk_c10 = iPr_def_16 ) ),
inference(light_normalisation,[status(thm)],[c_20423,c_10017]) ).
tcf(c_22746,plain,
( ( sk_c11 = iPr_def_24 )
| ( multiply(iPr_def_29,iPr_def_19) = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_4154,c_4632]) ).
tcf(c_22747,plain,
( ( sk_c9 = iPr_def_15 )
| ( sk_c11 = iPr_def_24 ) ),
inference(light_normalisation,[status(thm)],[c_22746,c_10012]) ).
tcf(c_22818,plain,
( ( sk_c10 = iPr_def_25 )
| ( multiply(iPr_def_29,iPr_def_19) = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_4253,c_4632]) ).
tcf(c_22819,plain,
( ( sk_c9 = iPr_def_15 )
| ( sk_c10 = iPr_def_25 ) ),
inference(light_normalisation,[status(thm)],[c_22818,c_10012]) ).
tcf(c_22890,plain,
( ( sk_c9 = iPr_def_15 )
| ( multiply(iPr_def_29,iPr_def_19) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_4373,c_4632]) ).
tcf(c_22891,plain,
( ( sk_c9 = iPr_def_26 )
| ( sk_c9 = iPr_def_15 ) ),
inference(light_normalisation,[status(thm)],[c_22890,c_10012]) ).
tcf(c_22980,plain,
( ( sk_c11 = iPr_def_27 )
| ( multiply(iPr_def_29,iPr_def_19) = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_4456,c_4632]) ).
tcf(c_22981,plain,
( ( sk_c9 = iPr_def_15 )
| ( sk_c11 = iPr_def_27 ) ),
inference(light_normalisation,[status(thm)],[c_22980,c_10012]) ).
tcf(c_23868,plain,
multiply(sk_c4,iPr_def_15) = multiply(iPr_def_26,sk_c11),
inference(superposition,[status(thm)],[c_835,c_4613]) ).
tcf(c_24614,plain,
multiply(sk_c8,iPr_def_15) = multiply(iPr_def_22,sk_c11),
inference(superposition,[status(thm)],[c_835,c_4615]) ).
tcf(c_25525,plain,
multiply(sk_c1,iPr_def_15) = multiply(iPr_def_30,sk_c11),
inference(superposition,[status(thm)],[c_835,c_4618]) ).
tcf(c_25797,plain,
multiply(sk_c2,iPr_def_16) = multiply(iPr_def_19,sk_c11),
inference(superposition,[status(thm)],[c_836,c_4619]) ).
tcf(c_29955,plain,
! [X0: $i] :
( ( inverse(X0) = iPr_def_15 )
| ( iPr_def_15 != iPr_def_17 )
| ( inverse(X0) != iPr_def_17 ) ),
inference(instantiation,[status(thm)],[c_4508]) ).
tcf(c_29956,plain,
( ( inverse(sk_c10) = iPr_def_15 )
| ( iPr_def_15 != iPr_def_17 )
| ( inverse(sk_c10) != iPr_def_17 ) ),
inference(instantiation,[status(thm)],[c_29955]) ).
tcf(c_32231,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(X0,X1)) = X1,
inference(demodulation,[status(thm)],[c_4621,c_123]) ).
tcf(c_32281,plain,
multiply(inverse(sk_c10),iPr_def_15) = sk_c11,
inference(superposition,[status(thm)],[c_835,c_32231]) ).
tcf(c_32283,plain,
multiply(inverse(sk_c4),iPr_def_26) = sk_c10,
inference(superposition,[status(thm)],[c_846,c_32231]) ).
tcf(c_32287,plain,
multiply(inverse(sk_c9),iPr_def_16) = sk_c11,
inference(superposition,[status(thm)],[c_836,c_32231]) ).
tcf(c_32290,plain,
! [X0: $i] : multiply(inverse(identity),X0) = X0,
inference(superposition,[status(thm)],[c_123,c_32231]) ).
tcf(c_32291,plain,
! [X0: $i] : multiply(inverse(inverse(X0)),identity) = X0,
inference(superposition,[status(thm)],[c_124,c_32231]) ).
tcf(c_32292,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(inverse(multiply(X0,X1)),multiply(X0,multiply(X1,X2))) = X2,
inference(superposition,[status(thm)],[c_125,c_32231]) ).
tcf(c_32472,plain,
( ( sk_c10 = iPr_def_25 )
| ( multiply(inverse(sk_c10),iPr_def_15) = iPr_def_30 ) ),
inference(superposition,[status(thm)],[c_1933,c_32231]) ).
tcf(c_32571,plain,
! [X0: $i] : multiply(inverse(iPr_def_27),X0) = multiply(sk_c3,X0),
inference(superposition,[status(thm)],[c_4639,c_32231]) ).
tcf(c_32572,plain,
! [X0: $i] : multiply(inverse(iPr_def_25),X0) = multiply(sk_c4,X0),
inference(superposition,[status(thm)],[c_4638,c_32231]) ).
tcf(c_32573,plain,
! [X0: $i] : multiply(inverse(iPr_def_23),X0) = multiply(sk_c5,X0),
inference(superposition,[status(thm)],[c_4637,c_32231]) ).
tcf(c_32576,plain,
! [X0: $i] : multiply(inverse(iPr_def_17),X0) = multiply(sk_c10,X0),
inference(superposition,[status(thm)],[c_4634,c_32231]) ).
tcf(c_32577,plain,
! [X0: $i] : multiply(inverse(iPr_def_31),X0) = multiply(sk_c1,X0),
inference(superposition,[status(thm)],[c_4633,c_32231]) ).
tcf(c_32578,plain,
! [X0: $i] : multiply(inverse(iPr_def_29),X0) = multiply(sk_c2,X0),
inference(superposition,[status(thm)],[c_4632,c_32231]) ).
tcf(c_32712,plain,
! [X0: $i,X1: $i] : multiply(inverse(inverse(X0)),X1) = multiply(X0,X1),
inference(superposition,[status(thm)],[c_32231,c_32231]) ).
tcf(c_33898,plain,
! [X0: $i,X1: $i] :
( ( inverse(X0) = X1 )
| ( X1 != iPr_def_15 )
| ( inverse(X0) != iPr_def_15 ) ),
inference(instantiation,[status(thm)],[c_1915]) ).
tcf(c_33901,plain,
( ( inverse(sk_c10) = sk_c10 )
| ( sk_c10 != iPr_def_15 )
| ( inverse(sk_c10) != iPr_def_15 ) ),
inference(instantiation,[status(thm)],[c_33898]) ).
tcf(c_34466,plain,
! [X0: $i] : multiply(X0,identity) = X0,
inference(demodulation,[status(thm)],[c_32291,c_32712]) ).
tcf(c_34478,plain,
multiply(sk_c9,sk_c11) = multiply(iPr_def_16,identity),
inference(superposition,[status(thm)],[c_34466,c_4617]) ).
tcf(c_34481,plain,
multiply(sk_c11,identity) = multiply(iPr_def_27,iPr_def_28),
inference(superposition,[status(thm)],[c_34466,c_10518]) ).
tcf(c_34485,plain,
multiply(sk_c4,sk_c10) = multiply(iPr_def_26,identity),
inference(superposition,[status(thm)],[c_34466,c_4613]) ).
tcf(c_34501,plain,
inverse(identity) = identity,
inference(superposition,[status(thm)],[c_34466,c_32290]) ).
tcf(c_34509,plain,
multiply(iPr_def_26,identity) = iPr_def_26,
inference(light_normalisation,[status(thm)],[c_34485,c_846]) ).
tcf(c_34513,plain,
multiply(sk_c11,identity) = sk_c11,
inference(light_normalisation,[status(thm)],[c_34481,c_10515]) ).
tcf(c_34522,plain,
multiply(identity,identity) = identity,
inference(superposition,[status(thm)],[c_34501,c_124]) ).
tcf(c_34623,plain,
( ( sk_c11 = iPr_def_27 )
| ~ iPr_def_13
| ( sk_c11 != iPr_def_31 ) ),
inference(superposition,[status(thm)],[c_886,c_5050]) ).
tcf(c_34817,plain,
( ( sk_c11 = iPr_def_27 )
| ~ iPr_def_13 ),
inference(global_subsumption_just,[status(thm)],[c_34623,c_18058,c_34623]) ).
tcf(c_34840,plain,
multiply(sk_c3,iPr_def_27) = identity,
inference(superposition,[status(thm)],[c_32571,c_124]) ).
tcf(c_34844,plain,
! [X0: $i] : multiply(sk_c3,multiply(iPr_def_27,X0)) = X0,
inference(superposition,[status(thm)],[c_32571,c_32231]) ).
tcf(c_34845,plain,
multiply(sk_c3,identity) = inverse(iPr_def_27),
inference(superposition,[status(thm)],[c_32571,c_34466]) ).
tcf(c_34872,plain,
( ( iPr_def_15 = iPr_def_17 )
| ( identity = iPr_def_28 ) ),
inference(demodulation,[status(thm)],[c_9667,c_34840]) ).
tcf(c_34873,plain,
( ( iPr_def_30 = iPr_def_31 )
| ( identity = iPr_def_28 ) ),
inference(demodulation,[status(thm)],[c_7561,c_34840]) ).
tcf(c_34874,plain,
( ( identity = iPr_def_28 )
| ( sk_c10 = iPr_def_16 ) ),
inference(demodulation,[status(thm)],[c_3120,c_34840]) ).
tcf(c_34875,plain,
( ( identity = iPr_def_28 )
| ( sk_c10 = iPr_def_29 ) ),
inference(demodulation,[status(thm)],[c_1633,c_34840]) ).
tcf(c_34876,plain,
( ( identity = iPr_def_28 )
| ( sk_c10 = iPr_def_19 ) ),
inference(demodulation,[status(thm)],[c_1567,c_34840]) ).
tcf(c_34947,plain,
inverse(iPr_def_27) = sk_c3,
inference(demodulation,[status(thm)],[c_34845,c_34466]) ).
tcf(c_34952,plain,
( ( iPr_def_16 = iPr_def_19 )
| ( inverse(iPr_def_24) = sk_c3 ) ),
inference(superposition,[status(thm)],[c_8320,c_34947]) ).
tcf(c_35144,plain,
multiply(sk_c3,sk_c11) = iPr_def_28,
inference(superposition,[status(thm)],[c_10515,c_34844]) ).
tcf(c_35704,plain,
( ( iPr_def_15 = iPr_def_17 )
| ( inverse(iPr_def_28) = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_34872,c_34501]) ).
tcf(c_35706,plain,
! [X0: $i] :
( ( iPr_def_15 = iPr_def_17 )
| ( multiply(iPr_def_28,X0) = X0 ) ),
inference(superposition,[status(thm)],[c_34872,c_123]) ).
tcf(c_35721,plain,
! [X0: $i] :
( ( iPr_def_30 = iPr_def_31 )
| ( multiply(iPr_def_28,X0) = X0 ) ),
inference(superposition,[status(thm)],[c_34873,c_123]) ).
tcf(c_36182,plain,
( ( identity = iPr_def_28 )
| ( multiply(sk_c4,iPr_def_29) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_34875,c_846]) ).
tcf(c_36432,plain,
( ( iPr_def_19 = iPr_def_29 )
| ( identity = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_34876,c_34875]) ).
tcf(c_36433,plain,
( ( iPr_def_16 = iPr_def_19 )
| ( identity = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_34876,c_34874]) ).
tcf(c_37271,plain,
( ( iPr_def_15 = iPr_def_17 )
| ( sk_c11 = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_35706,c_9746]) ).
tcf(c_37342,plain,
( ( iPr_def_19 = iPr_def_29 )
| ( inverse(iPr_def_28) = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_36432,c_34501]) ).
tcf(c_37357,plain,
( ( iPr_def_16 = iPr_def_19 )
| ( inverse(iPr_def_28) = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_36433,c_34501]) ).
tcf(c_37492,plain,
( ( iPr_def_15 = iPr_def_24 )
| ( iPr_def_15 = iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_37271,c_4148]) ).
tcf(c_37716,plain,
( ( iPr_def_30 = iPr_def_31 )
| ( sk_c11 = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_35721,c_7764]) ).
tcf(c_38187,plain,
( ( iPr_def_30 = iPr_def_31 )
| ( multiply(sk_c10,iPr_def_15) = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_37716,c_835]) ).
tcf(c_38581,plain,
( ( identity = iPr_def_28 )
| ( multiply(inverse(sk_c4),iPr_def_26) = iPr_def_29 ) ),
inference(superposition,[status(thm)],[c_36182,c_32231]) ).
tcf(c_38851,plain,
multiply(sk_c4,iPr_def_25) = identity,
inference(superposition,[status(thm)],[c_32572,c_124]) ).
tcf(c_38855,plain,
! [X0: $i] : multiply(sk_c4,multiply(iPr_def_25,X0)) = X0,
inference(superposition,[status(thm)],[c_32572,c_32231]) ).
tcf(c_38856,plain,
multiply(sk_c4,identity) = inverse(iPr_def_25),
inference(superposition,[status(thm)],[c_32572,c_34466]) ).
tcf(c_38885,plain,
( ( iPr_def_30 = iPr_def_31 )
| ( identity = iPr_def_26 ) ),
inference(demodulation,[status(thm)],[c_7423,c_38851]) ).
tcf(c_38886,plain,
( ( identity = iPr_def_26 )
| ( sk_c10 = iPr_def_16 ) ),
inference(demodulation,[status(thm)],[c_3026,c_38851]) ).
tcf(c_38887,plain,
( ( identity = iPr_def_26 )
| ( sk_c10 = iPr_def_19 ) ),
inference(demodulation,[status(thm)],[c_1560,c_38851]) ).
tcf(c_39151,plain,
! [X0: $i] :
( ( iPr_def_30 = iPr_def_31 )
| ( multiply(iPr_def_26,X0) = X0 ) ),
inference(superposition,[status(thm)],[c_38885,c_123]) ).
tcf(c_39444,plain,
( ( iPr_def_16 = iPr_def_19 )
| ( identity = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_38887,c_38886]) ).
tcf(c_39522,plain,
( ( iPr_def_19 = iPr_def_29 )
| ( identity = iPr_def_26 )
| ( sk_c10 = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_38887,c_874]) ).
tcf(c_39780,plain,
inverse(iPr_def_25) = sk_c4,
inference(demodulation,[status(thm)],[c_38856,c_34466]) ).
tcf(c_39815,plain,
multiply(sk_c4,sk_c10) = iPr_def_26,
inference(superposition,[status(thm)],[c_10510,c_38855]) ).
tcf(c_40372,plain,
( ( iPr_def_26 = iPr_def_28 )
| ( iPr_def_16 = iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_39444,c_36433]) ).
tcf(c_40379,plain,
! [X0: $i] :
( ( iPr_def_16 = iPr_def_19 )
| ( multiply(iPr_def_26,X0) = X0 ) ),
inference(superposition,[status(thm)],[c_39444,c_123]) ).
tcf(c_41001,plain,
( ( iPr_def_25 = iPr_def_26 )
| ( iPr_def_16 = iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_40372,c_8577]) ).
tcf(c_41593,plain,
multiply(sk_c5,iPr_def_23) = identity,
inference(superposition,[status(thm)],[c_32573,c_124]) ).
tcf(c_41597,plain,
! [X0: $i] : multiply(sk_c5,multiply(iPr_def_23,X0)) = X0,
inference(superposition,[status(thm)],[c_32573,c_32231]) ).
tcf(c_41622,plain,
( ( identity = iPr_def_24 )
| ( sk_c9 = iPr_def_15 ) ),
inference(demodulation,[status(thm)],[c_4116,c_41593]) ).
tcf(c_41623,plain,
( ( identity = iPr_def_24 )
| ( sk_c9 = iPr_def_17 ) ),
inference(demodulation,[status(thm)],[c_3502,c_41593]) ).
tcf(c_41624,plain,
( ( identity = iPr_def_24 )
| ( sk_c10 = iPr_def_16 ) ),
inference(demodulation,[status(thm)],[c_2902,c_41593]) ).
tcf(c_41627,plain,
( ( identity = iPr_def_24 )
| ( sk_c10 = iPr_def_19 ) ),
inference(demodulation,[status(thm)],[c_1549,c_41593]) ).
tcf(c_42042,plain,
( ( iPr_def_15 = iPr_def_17 )
| ( identity = iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_41623,c_41622]) ).
tcf(c_42949,plain,
multiply(sk_c5,sk_c8) = iPr_def_24,
inference(superposition,[status(thm)],[c_10505,c_41597]) ).
tcf(c_43443,plain,
( ( iPr_def_16 = iPr_def_19 )
| ( identity = iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_41627,c_41624]) ).
tcf(c_44728,plain,
( ( iPr_def_24 = iPr_def_28 )
| ( iPr_def_15 = iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_42042,c_34872]) ).
tcf(c_44829,plain,
( ( iPr_def_24 = iPr_def_26 )
| ( iPr_def_16 = iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_43443,c_39444]) ).
tcf(c_46072,plain,
( ( iPr_def_15 = inverse(sk_c4) )
| ( iPr_def_15 != iPr_def_25 )
| ( inverse(sk_c4) != iPr_def_25 ) ),
inference(instantiation,[status(thm)],[c_11142]) ).
tcf(c_46139,plain,
( ( sk_c9 = inverse(sk_c4) )
| ( sk_c9 != iPr_def_25 )
| ( inverse(sk_c4) != iPr_def_25 ) ),
inference(instantiation,[status(thm)],[c_11142]) ).
tcf(c_46140,plain,
( ( iPr_def_15 = sk_c9 )
| ( iPr_def_15 != inverse(sk_c4) )
| ( sk_c9 != inverse(sk_c4) ) ),
inference(instantiation,[status(thm)],[c_11486]) ).
tcf(c_46486,plain,
( ( iPr_def_24 = iPr_def_25 )
| ( iPr_def_16 = iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_44829,c_41001]) ).
tcf(c_52333,plain,
multiply(sk_c10,iPr_def_17) = identity,
inference(superposition,[status(thm)],[c_32576,c_124]) ).
tcf(c_52337,plain,
! [X0: $i] : multiply(sk_c10,multiply(iPr_def_17,X0)) = X0,
inference(superposition,[status(thm)],[c_32576,c_32231]) ).
tcf(c_52338,plain,
multiply(sk_c10,identity) = inverse(iPr_def_17),
inference(superposition,[status(thm)],[c_32576,c_34466]) ).
tcf(c_52959,plain,
multiply(sk_c1,identity) = multiply(iPr_def_30,iPr_def_17),
inference(superposition,[status(thm)],[c_52333,c_4618]) ).
tcf(c_52960,plain,
multiply(sk_c8,identity) = multiply(iPr_def_22,iPr_def_17),
inference(superposition,[status(thm)],[c_52333,c_4615]) ).
tcf(c_52961,plain,
multiply(sk_c4,identity) = multiply(iPr_def_26,iPr_def_17),
inference(superposition,[status(thm)],[c_52333,c_4613]) ).
tcf(c_53363,plain,
inverse(iPr_def_17) = sk_c10,
inference(demodulation,[status(thm)],[c_52338,c_34466]) ).
tcf(c_53456,plain,
multiply(sk_c10,sk_c11) = iPr_def_15,
inference(superposition,[status(thm)],[c_10022,c_52337]) ).
tcf(c_53944,plain,
multiply(iPr_def_30,iPr_def_17) = sk_c1,
inference(demodulation,[status(thm)],[c_52959,c_34466]) ).
tcf(c_53945,plain,
multiply(inverse(iPr_def_30),sk_c1) = iPr_def_17,
inference(superposition,[status(thm)],[c_53944,c_32231]) ).
tcf(c_54422,plain,
multiply(iPr_def_22,iPr_def_17) = sk_c8,
inference(demodulation,[status(thm)],[c_52960,c_34466]) ).
tcf(c_54490,plain,
multiply(iPr_def_26,iPr_def_17) = sk_c4,
inference(demodulation,[status(thm)],[c_52961,c_34466]) ).
tcf(c_54498,plain,
multiply(inverse(iPr_def_26),sk_c4) = iPr_def_17,
inference(superposition,[status(thm)],[c_54490,c_32231]) ).
tcf(c_54500,plain,
( ( iPr_def_16 = iPr_def_19 )
| ( sk_c4 = iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_54490,c_40379]) ).
tcf(c_61848,plain,
( ~ iPr_def_13
| ( inverse(inverse(iPr_def_31)) != sk_c11 )
| ( multiply(sk_c1,sk_c10) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_32577,c_854]) ).
tcf(c_61851,plain,
multiply(sk_c1,iPr_def_31) = identity,
inference(superposition,[status(thm)],[c_32577,c_124]) ).
tcf(c_61853,plain,
( ~ iPr_def_10
| ( inverse(inverse(iPr_def_31)) != sk_c11 )
| ( multiply(sk_c1,sk_c11) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_32577,c_857]) ).
tcf(c_61855,plain,
! [X0: $i] : multiply(sk_c1,multiply(iPr_def_31,X0)) = X0,
inference(superposition,[status(thm)],[c_32577,c_32231]) ).
tcf(c_61856,plain,
multiply(sk_c1,identity) = inverse(iPr_def_31),
inference(superposition,[status(thm)],[c_32577,c_34466]) ).
tcf(c_61887,plain,
( ~ iPr_def_13
| ( sk_c11 != iPr_def_30 )
| ( inverse(inverse(iPr_def_31)) != sk_c11 ) ),
inference(light_normalisation,[status(thm)],[c_61848,c_850]) ).
tcf(c_62523,plain,
inverse(iPr_def_31) = sk_c1,
inference(demodulation,[status(thm)],[c_61856,c_34466]) ).
tcf(c_62572,plain,
multiply(sk_c1,sk_c10) = iPr_def_30,
inference(superposition,[status(thm)],[c_10017,c_61855]) ).
tcf(c_62826,plain,
( ~ iPr_def_12
| ( inverse(inverse(iPr_def_29)) != sk_c10 )
| ( multiply(sk_c2,sk_c10) != sk_c9 ) ),
inference(superposition,[status(thm)],[c_32578,c_855]) ).
tcf(c_62830,plain,
multiply(sk_c2,iPr_def_29) = identity,
inference(superposition,[status(thm)],[c_32578,c_124]) ).
tcf(c_62833,plain,
( ~ iPr_def_11
| ( inverse(inverse(iPr_def_29)) != sk_c10 )
| ( multiply(sk_c2,sk_c9) != sk_c10 ) ),
inference(superposition,[status(thm)],[c_32578,c_856]) ).
tcf(c_62835,plain,
multiply(sk_c2,identity) = inverse(iPr_def_29),
inference(superposition,[status(thm)],[c_32578,c_34466]) ).
tcf(c_64202,plain,
( ( iPr_def_19 = iPr_def_29 )
| ( identity = iPr_def_26 )
| ( multiply(sk_c4,iPr_def_25) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_39522,c_846]) ).
tcf(c_64223,plain,
( ( iPr_def_19 = iPr_def_29 )
| ( identity = iPr_def_26 ) ),
inference(light_normalisation,[status(thm)],[c_64202,c_38851]) ).
tcf(c_64253,plain,
multiply(iPr_def_29,identity) = iPr_def_29,
inference(superposition,[status(thm)],[c_62830,c_4632]) ).
tcf(c_64423,plain,
inverse(iPr_def_29) = sk_c2,
inference(demodulation,[status(thm)],[c_62835,c_34466]) ).
tcf(c_64432,plain,
( ( sk_c2 = iPr_def_17 )
| ( sk_c10 = iPr_def_28 ) ),
inference(demodulation,[status(thm)],[c_1660,c_64423]) ).
tcf(c_64433,plain,
( ( sk_c2 = iPr_def_17 )
| ( sk_c10 = iPr_def_25 ) ),
inference(demodulation,[status(thm)],[c_1596,c_64423]) ).
tcf(c_68896,plain,
( ( sk_c10 = iPr_def_28 )
| ( multiply(iPr_def_17,iPr_def_15) = iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_64432,c_4565]) ).
tcf(c_68920,plain,
( ( sk_c11 = iPr_def_19 )
| ( sk_c10 = iPr_def_28 ) ),
inference(light_normalisation,[status(thm)],[c_68896,c_10022]) ).
tcf(c_68950,plain,
( ( sk_c10 = iPr_def_25 )
| ( multiply(iPr_def_17,iPr_def_15) = iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_64433,c_4253]) ).
tcf(c_68971,plain,
( ( sk_c11 = iPr_def_19 )
| ( sk_c10 = iPr_def_25 ) ),
inference(light_normalisation,[status(thm)],[c_68950,c_10022]) ).
tcf(c_69745,plain,
iPr_def_27 = iPr_def_27,
inference(instantiation,[status(thm)],[c_928]) ).
tcf(c_73131,plain,
( ( iPr_def_19 = iPr_def_31 )
| ( sk_c10 = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_68971,c_894]) ).
tcf(c_73136,plain,
( ( iPr_def_19 = iPr_def_30 )
| ( sk_c10 = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_68971,c_884]) ).
tcf(c_74957,plain,
( ( iPr_def_19 = iPr_def_31 )
| ( multiply(sk_c4,iPr_def_25) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_73131,c_846]) ).
tcf(c_74971,plain,
( ( iPr_def_19 = iPr_def_31 )
| ( identity = iPr_def_26 ) ),
inference(light_normalisation,[status(thm)],[c_74957,c_38851]) ).
tcf(c_75401,plain,
( ( iPr_def_19 = iPr_def_30 )
| ( multiply(sk_c4,iPr_def_25) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_73136,c_846]) ).
tcf(c_75415,plain,
( ( iPr_def_19 = iPr_def_30 )
| ( identity = iPr_def_26 ) ),
inference(light_normalisation,[status(thm)],[c_75401,c_38851]) ).
tcf(c_75795,plain,
( ( sk_c9 = iPr_def_25 )
| ( iPr_def_25 != iPr_def_26 )
| ( sk_c9 != iPr_def_26 ) ),
inference(instantiation,[status(thm)],[c_1795]) ).
tcf(c_81180,plain,
( ~ iPr_def_13
| ( sk_c11 != identity )
| ( sk_c10 != sk_c11 ) ),
inference(light_normalisation,[status(thm)],[c_5030,c_34501]) ).
tcf(c_81224,plain,
( ( iPr_def_30 = iPr_def_31 )
| ~ iPr_def_13
| ( sk_c11 != identity )
| ( sk_c10 != iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_2211,c_81180]) ).
tcf(c_81579,plain,
( ~ iPr_def_12
| ( sk_c10 != identity )
| ( sk_c10 != sk_c9 ) ),
inference(light_normalisation,[status(thm)],[c_5157,c_34501]) ).
tcf(c_81721,plain,
( ~ iPr_def_12
| ( sk_c9 != identity ) ),
inference(ground_joinability,[status(thm)],[c_5160,c_53363]) ).
tcf(c_84113,plain,
( ( iPr_def_17 = iPr_def_28 )
| ( iPr_def_15 = iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_35704,c_9745]) ).
tcf(c_84228,plain,
( ( iPr_def_17 = iPr_def_24 )
| ( iPr_def_15 = iPr_def_17 ) ),
inference(superposition,[status(thm)],[c_84113,c_44728]) ).
tcf(c_84954,plain,
( ~ iPr_def_11
| ( sk_c10 != identity )
| ( sk_c10 != sk_c9 ) ),
inference(light_normalisation,[status(thm)],[c_5283,c_34501]) ).
tcf(c_85490,plain,
iPr_def_15 = iPr_def_17,
inference(superposition,[status(thm)],[c_84228,c_37492]) ).
tcf(c_85566,plain,
( ( iPr_def_16 = iPr_def_19 )
| ( sk_c4 = iPr_def_15 ) ),
inference(demodulation,[status(thm)],[c_54500,c_85490]) ).
tcf(c_85567,plain,
multiply(inverse(iPr_def_26),sk_c4) = iPr_def_15,
inference(demodulation,[status(thm)],[c_54498,c_85490]) ).
tcf(c_85576,plain,
multiply(iPr_def_26,iPr_def_15) = sk_c4,
inference(demodulation,[status(thm)],[c_54490,c_85490]) ).
tcf(c_85578,plain,
multiply(iPr_def_22,iPr_def_15) = sk_c8,
inference(demodulation,[status(thm)],[c_54422,c_85490]) ).
tcf(c_85579,plain,
multiply(inverse(iPr_def_30),sk_c1) = iPr_def_15,
inference(demodulation,[status(thm)],[c_53945,c_85490]) ).
tcf(c_85584,plain,
multiply(iPr_def_30,iPr_def_15) = sk_c1,
inference(demodulation,[status(thm)],[c_53944,c_85490]) ).
tcf(c_85585,plain,
! [X0: $i] : multiply(sk_c10,multiply(iPr_def_15,X0)) = X0,
inference(demodulation,[status(thm)],[c_52337,c_85490]) ).
tcf(c_85586,plain,
inverse(iPr_def_15) = sk_c10,
inference(demodulation,[status(thm)],[c_53363,c_85490]) ).
tcf(c_85587,plain,
multiply(sk_c10,iPr_def_15) = identity,
inference(demodulation,[status(thm)],[c_52333,c_85490]) ).
tcf(c_85696,plain,
multiply(iPr_def_15,iPr_def_15) = sk_c11,
inference(demodulation,[status(thm)],[c_10022,c_85490]) ).
tcf(c_85700,plain,
( iPr_def_14
| iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10
| ( sk_c9 != iPr_def_15 )
| ( sk_c10 != iPr_def_16 ) ),
inference(demodulation,[status(thm)],[c_852,c_85490]) ).
tcf(c_85711,plain,
multiply(iPr_def_15,sk_c10) = identity,
inference(demodulation,[status(thm)],[c_1837,c_85490]) ).
tcf(c_85712,plain,
inverse(sk_c10) = iPr_def_15,
inference(demodulation,[status(thm)],[c_837,c_85490]) ).
tcf(c_85832,plain,
( ( iPr_def_30 = iPr_def_31 )
| ( identity = iPr_def_15 ) ),
inference(demodulation,[status(thm)],[c_38187,c_85587]) ).
tcf(c_85998,plain,
( ~ iPr_def_10
| ( inverse(sk_c9) != sk_c11 ) ),
inference(global_subsumption_just,[status(thm)],[c_5465,c_5494,c_5465,c_20079,c_20424]) ).
tcf(c_86018,plain,
( ( sk_c10 = iPr_def_28 )
| ~ iPr_def_10
| ( inverse(iPr_def_15) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_927,c_85998]) ).
tcf(c_86019,plain,
( ( sk_c11 = iPr_def_27 )
| ~ iPr_def_10
| ( inverse(iPr_def_15) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_926,c_85998]) ).
tcf(c_86028,plain,
( ( sk_c10 = iPr_def_19 )
| ~ iPr_def_10
| ( inverse(iPr_def_26) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_865,c_85998]) ).
tcf(c_86059,plain,
( ( sk_c11 = iPr_def_27 )
| ~ iPr_def_10
| ( sk_c10 != sk_c11 ) ),
inference(light_normalisation,[status(thm)],[c_86019,c_85586]) ).
tcf(c_86063,plain,
( ( sk_c10 = iPr_def_28 )
| ~ iPr_def_10
| ( sk_c10 != sk_c11 ) ),
inference(light_normalisation,[status(thm)],[c_86018,c_85586]) ).
tcf(c_86109,plain,
( ( sk_c10 = iPr_def_19 )
| ~ iPr_def_10 ),
inference(global_subsumption_just,[status(thm)],[c_86028,c_5494,c_10486,c_12864]) ).
tcf(c_86423,plain,
! [X0: $i] : multiply(iPr_def_26,multiply(iPr_def_15,X0)) = multiply(sk_c4,X0),
inference(superposition,[status(thm)],[c_85576,c_125]) ).
tcf(c_86447,plain,
! [X0: $i] : multiply(iPr_def_30,multiply(iPr_def_15,X0)) = multiply(sk_c1,X0),
inference(superposition,[status(thm)],[c_85584,c_125]) ).
tcf(c_86459,plain,
( ~ iPr_def_10
| ( sk_c10 != sk_c11 ) ),
inference(global_subsumption_just,[status(thm)],[c_5466,c_5494,c_86063,c_86059]) ).
tcf(c_86466,plain,
( ( sk_c10 = iPr_def_28 )
| ~ iPr_def_10
| ( sk_c10 != iPr_def_19 ) ),
inference(superposition,[status(thm)],[c_68920,c_86459]) ).
tcf(c_86502,plain,
( ( sk_c10 = iPr_def_28 )
| ~ iPr_def_10
| ( sk_c10 != iPr_def_31 ) ),
inference(superposition,[status(thm)],[c_897,c_86459]) ).
tcf(c_86593,plain,
( ( sk_c10 = iPr_def_28 )
| ~ iPr_def_10 ),
inference(global_subsumption_just,[status(thm)],[c_86502,c_86109,c_86466]) ).
tcf(c_87238,plain,
multiply(sk_c4,identity) = multiply(iPr_def_26,iPr_def_15),
inference(superposition,[status(thm)],[c_85587,c_4613]) ).
tcf(c_87378,plain,
( ~ iPr_def_13
| ( sk_c11 != identity )
| ( inverse(iPr_def_15) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_85711,c_854]) ).
tcf(c_87560,plain,
! [X0: $i] : multiply(inverse(iPr_def_26),multiply(sk_c4,X0)) = multiply(iPr_def_15,X0),
inference(superposition,[status(thm)],[c_85567,c_125]) ).
tcf(c_87980,plain,
! [X0: $i] : multiply(inverse(iPr_def_30),multiply(sk_c1,X0)) = multiply(iPr_def_15,X0),
inference(superposition,[status(thm)],[c_85579,c_125]) ).
tcf(c_89312,plain,
! [X0: $i,X1: $i] :
( ( inverse(X0) = sk_c3 )
| ( sk_c3 != X1 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_1915]) ).
tcf(c_89314,plain,
( ( inverse(sk_c10) = sk_c3 )
| ( sk_c3 != sk_c10 )
| ( inverse(sk_c10) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_89312]) ).
tcf(c_89714,plain,
multiply(inverse(iPr_def_26),identity) = multiply(iPr_def_15,iPr_def_25),
inference(superposition,[status(thm)],[c_38851,c_87560]) ).
tcf(c_91398,plain,
multiply(inverse(iPr_def_30),identity) = multiply(iPr_def_15,iPr_def_31),
inference(superposition,[status(thm)],[c_61851,c_87980]) ).
tcf(c_91408,plain,
multiply(inverse(iPr_def_30),multiply(iPr_def_30,sk_c11)) = multiply(iPr_def_15,iPr_def_15),
inference(superposition,[status(thm)],[c_25525,c_87980]) ).
tcf(c_91415,plain,
multiply(inverse(iPr_def_30),multiply(iPr_def_30,sk_c11)) = sk_c11,
inference(light_normalisation,[status(thm)],[c_91408,c_85696]) ).
tcf(c_94017,plain,
( ~ iPr_def_10
| ( sk_c11 != iPr_def_27 ) ),
inference(global_subsumption_just,[status(thm)],[c_5494,c_5494,c_86593]) ).
tcf(c_94050,plain,
( ( iPr_def_30 = iPr_def_31 )
| ~ iPr_def_10 ),
inference(superposition,[status(thm)],[c_2511,c_94017]) ).
tcf(c_94066,plain,
( ( sk_c11 = iPr_def_27 )
| ~ iPr_def_10
| ( iPr_def_27 != iPr_def_30 ) ),
inference(superposition,[status(thm)],[c_886,c_94017]) ).
tcf(c_94446,plain,
( ( iPr_def_27 != iPr_def_30 )
| ~ iPr_def_10 ),
inference(global_subsumption_just,[status(thm)],[c_94066,c_94017,c_94066]) ).
tcf(c_94447,plain,
( ~ iPr_def_10
| ( iPr_def_27 != iPr_def_30 ) ),
inference(renaming,[status(thm)],[c_94446]) ).
tcf(c_95092,plain,
( ( iPr_def_30 = iPr_def_31 )
| ( inverse(iPr_def_15) = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_85832,c_34501]) ).
tcf(c_95094,plain,
! [X0: $i] :
( ( iPr_def_30 = iPr_def_31 )
| ( multiply(iPr_def_15,X0) = X0 ) ),
inference(superposition,[status(thm)],[c_85832,c_123]) ).
tcf(c_95099,plain,
( ( iPr_def_30 = iPr_def_31 )
| ( sk_c10 = iPr_def_15 ) ),
inference(light_normalisation,[status(thm)],[c_95092,c_85586]) ).
tcf(c_95357,plain,
( ( iPr_def_30 = iPr_def_31 )
| ( sk_c10 = identity ) ),
inference(superposition,[status(thm)],[c_95094,c_85711]) ).
tcf(c_96051,plain,
( ( iPr_def_30 = iPr_def_31 )
| ( multiply(iPr_def_15,iPr_def_15) = identity ) ),
inference(superposition,[status(thm)],[c_95099,c_85711]) ).
tcf(c_96141,plain,
( ( iPr_def_30 = iPr_def_31 )
| ( iPr_def_15 = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_95099,c_2416]) ).
tcf(c_96161,plain,
( ( iPr_def_30 = iPr_def_31 )
| ( multiply(sk_c8,iPr_def_15) = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_95099,c_842]) ).
tcf(c_96169,plain,
( ( iPr_def_30 = iPr_def_31 )
| ( multiply(iPr_def_22,sk_c11) = iPr_def_22 ) ),
inference(light_normalisation,[status(thm)],[c_96161,c_24614]) ).
tcf(c_96184,plain,
( ( iPr_def_30 = iPr_def_31 )
| ( sk_c11 = identity ) ),
inference(light_normalisation,[status(thm)],[c_96051,c_85696]) ).
tcf(c_97244,plain,
( ( iPr_def_30 = iPr_def_31 )
| ( multiply(iPr_def_22,iPr_def_15) = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_37716,c_96169]) ).
tcf(c_97306,plain,
( ( iPr_def_30 = iPr_def_31 )
| ( sk_c8 = iPr_def_22 ) ),
inference(light_normalisation,[status(thm)],[c_97244,c_85578]) ).
tcf(c_97875,plain,
( ( iPr_def_30 = iPr_def_31 )
| ( identity = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_95357,c_2416]) ).
tcf(c_98695,plain,
( ( iPr_def_30 = iPr_def_31 )
| ( identity = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_96184,c_2211]) ).
tcf(c_98715,plain,
( ( iPr_def_30 = iPr_def_31 )
| ( multiply(sk_c3,identity) = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_96184,c_848]) ).
tcf(c_98716,plain,
( ( iPr_def_30 = iPr_def_31 )
| ( multiply(sk_c9,identity) = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_96184,c_836]) ).
tcf(c_99255,plain,
( ( iPr_def_30 = iPr_def_31 )
| ( multiply(iPr_def_22,sk_c10) = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_97306,c_842]) ).
tcf(c_100924,plain,
! [X0: $i,X1: $i] :
( ( multiply(inverse(X0),sk_c10) = sk_c11 )
| ( sk_c11 != X1 )
| ( multiply(inverse(X0),sk_c10) != X1 ) ),
inference(instantiation,[status(thm)],[c_929]) ).
tcf(c_100927,plain,
! [X0: $i,X1: $i] :
( ( sk_c11 = X0 )
| ( sk_c11 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_929]) ).
tcf(c_100936,plain,
! [X0: $i,X1: $i] :
( ( X0 = sk_c11 )
| ( sk_c11 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_929]) ).
tcf(c_100941,plain,
! [X0: $i] :
( ( sk_c11 = X0 )
| ( sk_c11 != iPr_def_22 )
| ( X0 != iPr_def_22 ) ),
inference(instantiation,[status(thm)],[c_100927]) ).
tcf(c_100950,plain,
! [X0: $i] :
( ( sk_c11 = X0 )
| ( sk_c11 != iPr_def_24 )
| ( X0 != iPr_def_24 ) ),
inference(instantiation,[status(thm)],[c_100927]) ).
tcf(c_100954,plain,
! [X0: $i] :
( ( sk_c11 = X0 )
| ( sk_c11 != iPr_def_27 )
| ( X0 != iPr_def_27 ) ),
inference(instantiation,[status(thm)],[c_100927]) ).
tcf(c_100989,plain,
! [X0: $i,X1: $i] :
( ( X0 = iPr_def_27 )
| ( iPr_def_27 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_929]) ).
tcf(c_101059,plain,
! [X0: $i,X1: $i] :
( ( iPr_def_27 = X0 )
| ( iPr_def_27 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_929]) ).
tcf(c_101060,plain,
! [X0: $i] :
( ( X0 = iPr_def_27 )
| ( iPr_def_27 != inverse(sk_c3) )
| ( X0 != inverse(sk_c3) ) ),
inference(instantiation,[status(thm)],[c_100989]) ).
tcf(c_101105,plain,
! [X0: $i,X1: $i] :
( ( X0 = identity )
| ( identity != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_929]) ).
tcf(c_101257,plain,
! [X0: $i] :
( ( iPr_def_27 = X0 )
| ( iPr_def_27 != iPr_def_27 )
| ( X0 != iPr_def_27 ) ),
inference(instantiation,[status(thm)],[c_101059]) ).
tcf(c_101405,plain,
( ( sk_c11 = iPr_def_22 )
| ( iPr_def_22 != iPr_def_24 )
| ( sk_c11 != iPr_def_24 ) ),
inference(instantiation,[status(thm)],[c_100950]) ).
tcf(c_101414,plain,
! [X0: $i] :
( ( X0 = iPr_def_27 )
| ( iPr_def_27 != iPr_def_24 )
| ( X0 != iPr_def_24 ) ),
inference(instantiation,[status(thm)],[c_100989]) ).
tcf(c_101427,plain,
( ( sk_c11 = iPr_def_24 )
| ( iPr_def_24 != iPr_def_27 )
| ( sk_c11 != iPr_def_27 ) ),
inference(instantiation,[status(thm)],[c_100954]) ).
tcf(c_101743,plain,
( ( iPr_def_27 = iPr_def_24 )
| ( iPr_def_27 != iPr_def_27 )
| ( iPr_def_24 != iPr_def_27 ) ),
inference(instantiation,[status(thm)],[c_101257]) ).
tcf(c_103411,plain,
! [X0: $i,X1: $i] :
( ( sk_c3 = X0 )
| ( sk_c3 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_929]) ).
tcf(c_103608,plain,
( ( sk_c11 = iPr_def_27 )
| ( iPr_def_27 != inverse(sk_c3) )
| ( sk_c11 != inverse(sk_c3) ) ),
inference(instantiation,[status(thm)],[c_101060]) ).
tcf(c_111177,plain,
! [X0: $i] :
( ( sk_c3 = X0 )
| ( sk_c3 != sk_c3 )
| ( X0 != sk_c3 ) ),
inference(instantiation,[status(thm)],[c_103411]) ).
tcf(c_111178,plain,
sk_c3 = sk_c3,
inference(instantiation,[status(thm)],[c_928]) ).
tcf(c_111179,plain,
( ( sk_c3 = sk_c10 )
| ( sk_c3 != sk_c3 )
| ( sk_c10 != sk_c3 ) ),
inference(instantiation,[status(thm)],[c_111177]) ).
tcf(c_112244,plain,
( ( multiply(inverse(sk_c10),sk_c10) = sk_c11 )
| ( sk_c11 != identity )
| ( multiply(inverse(sk_c10),sk_c10) != identity ) ),
inference(instantiation,[status(thm)],[c_100924]) ).
tcf(c_112424,plain,
( ( iPr_def_30 = iPr_def_31 )
| ( inverse(iPr_def_25) = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_97875,c_34501]) ).
tcf(c_112431,plain,
( ( iPr_def_30 = iPr_def_31 )
| ( sk_c4 = iPr_def_25 ) ),
inference(light_normalisation,[status(thm)],[c_112424,c_39780]) ).
tcf(c_113468,plain,
( ( identity = iPr_def_27 )
| ( iPr_def_27 != iPr_def_24 )
| ( identity != iPr_def_24 ) ),
inference(instantiation,[status(thm)],[c_101414]) ).
tcf(c_115328,plain,
! [X0: $i,X1: $i] :
( ( multiply(X0,inverse(X0)) = sk_c11 )
| ( sk_c11 != X1 )
| ( multiply(X0,inverse(X0)) != X1 ) ),
inference(instantiation,[status(thm)],[c_100936]) ).
tcf(c_116330,plain,
! [X0: $i,X1: $i] :
( ( inverse(X0) = identity )
| ( identity != X1 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_101105]) ).
tcf(c_118671,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(X0,inverse(X0)) = sk_c11 )
| ( sk_c11 != multiply(X1,X2) )
| ( multiply(X0,inverse(X0)) != multiply(X1,X2) ) ),
inference(instantiation,[status(thm)],[c_115328]) ).
tcf(c_118672,plain,
( ( multiply(sk_c10,inverse(sk_c10)) = sk_c11 )
| ( sk_c11 != multiply(sk_c10,sk_c10) )
| ( multiply(sk_c10,inverse(sk_c10)) != multiply(sk_c10,sk_c10) ) ),
inference(instantiation,[status(thm)],[c_118671]) ).
tcf(c_120803,plain,
( ( iPr_def_30 = iPr_def_31 )
| ( sk_c3 = iPr_def_28 ) ),
inference(demodulation,[status(thm)],[c_98715,c_34466]) ).
tcf(c_120846,plain,
( ( iPr_def_30 = iPr_def_31 )
| ( multiply(iPr_def_28,sk_c11) = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_120803,c_848]) ).
tcf(c_121193,plain,
! [X0: $i] :
( ( iPr_def_30 = iPr_def_31 )
| ( multiply(iPr_def_22,X0) = X0 ) ),
inference(superposition,[status(thm)],[c_98695,c_123]) ).
tcf(c_121407,plain,
( ( iPr_def_30 = iPr_def_31 )
| ( sk_c9 = iPr_def_16 ) ),
inference(demodulation,[status(thm)],[c_98716,c_34466]) ).
tcf(c_121447,plain,
( ( iPr_def_30 = iPr_def_31 )
| ~ iPr_def_12
| ( sk_c10 != iPr_def_16 )
| ( sk_c10 != identity ) ),
inference(superposition,[status(thm)],[c_121407,c_81579]) ).
tcf(c_122756,plain,
( ( iPr_def_30 = iPr_def_31 )
| ( multiply(iPr_def_25,iPr_def_15) = multiply(iPr_def_26,sk_c11) ) ),
inference(superposition,[status(thm)],[c_112431,c_23868]) ).
tcf(c_126166,plain,
( ( iPr_def_30 = iPr_def_31 )
| ( sk_c11 = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_120846,c_35721]) ).
tcf(c_129394,plain,
( ( iPr_def_30 = iPr_def_31 )
| ( sk_c10 = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_121193,c_99255]) ).
tcf(c_132583,plain,
( ( iPr_def_19 = iPr_def_29 )
| ( multiply(iPr_def_28,iPr_def_28) = identity ) ),
inference(superposition,[status(thm)],[c_37342,c_124]) ).
tcf(c_132609,plain,
( ( iPr_def_16 = iPr_def_19 )
| ( inverse(iPr_def_25) = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_8577,c_37357]) ).
tcf(c_132614,plain,
( ( iPr_def_16 = iPr_def_19 )
| ( sk_c4 = iPr_def_25 ) ),
inference(light_normalisation,[status(thm)],[c_132609,c_39780]) ).
tcf(c_133274,plain,
( ( iPr_def_16 = iPr_def_19 )
| ( iPr_def_15 = iPr_def_25 ) ),
inference(superposition,[status(thm)],[c_132614,c_85566]) ).
tcf(c_133417,plain,
( ( iPr_def_16 = iPr_def_19 )
| ( iPr_def_15 = iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_133274,c_46486]) ).
tcf(c_133419,plain,
( ( iPr_def_16 = iPr_def_19 )
| ( inverse(iPr_def_15) = sk_c4 ) ),
inference(superposition,[status(thm)],[c_133274,c_39780]) ).
tcf(c_133446,plain,
( ( iPr_def_16 = iPr_def_19 )
| ( sk_c10 = sk_c4 ) ),
inference(light_normalisation,[status(thm)],[c_133419,c_85586]) ).
tcf(c_133644,plain,
( ( iPr_def_16 = iPr_def_19 )
| ( inverse(iPr_def_15) = sk_c3 ) ),
inference(superposition,[status(thm)],[c_133417,c_34952]) ).
tcf(c_133670,plain,
( ( iPr_def_16 = iPr_def_19 )
| ( iPr_def_15 = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_133417,c_8175]) ).
tcf(c_133678,plain,
( ( iPr_def_16 = iPr_def_19 )
| ( sk_c10 = sk_c3 ) ),
inference(light_normalisation,[status(thm)],[c_133644,c_85586]) ).
tcf(c_134053,plain,
( ( iPr_def_16 = iPr_def_19 )
| ( sk_c10 = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_133446,c_85566]) ).
tcf(c_134708,plain,
( ( iPr_def_16 = iPr_def_19 )
| ( multiply(iPr_def_15,iPr_def_15) = sk_c8 ) ),
inference(superposition,[status(thm)],[c_133670,c_85578]) ).
tcf(c_134748,plain,
( ( iPr_def_16 = iPr_def_19 )
| ( sk_c11 = sk_c8 ) ),
inference(light_normalisation,[status(thm)],[c_134708,c_85696]) ).
tcf(c_134891,plain,
( ( iPr_def_16 = iPr_def_19 )
| ( multiply(sk_c10,sk_c11) = iPr_def_28 ) ),
inference(superposition,[status(thm)],[c_133678,c_848]) ).
tcf(c_134896,plain,
( ( iPr_def_16 = iPr_def_19 )
| ( iPr_def_15 = iPr_def_28 ) ),
inference(light_normalisation,[status(thm)],[c_134891,c_53456]) ).
tcf(c_135129,plain,
( ( iPr_def_16 = iPr_def_19 )
| ( multiply(iPr_def_15,iPr_def_15) = identity ) ),
inference(superposition,[status(thm)],[c_134053,c_85711]) ).
tcf(c_135247,plain,
( ( iPr_def_16 = iPr_def_19 )
| ( sk_c11 = identity ) ),
inference(light_normalisation,[status(thm)],[c_135129,c_85696]) ).
tcf(c_137105,plain,
( ( inverse(sk_c3) = identity )
| ( identity != iPr_def_27 )
| ( inverse(sk_c3) != iPr_def_27 ) ),
inference(instantiation,[status(thm)],[c_116330]) ).
tcf(c_139011,plain,
! [X0: $i] :
( ( sk_c11 = X0 )
| ( sk_c11 != identity )
| ( X0 != identity ) ),
inference(instantiation,[status(thm)],[c_100927]) ).
tcf(c_141428,plain,
( ( iPr_def_16 = iPr_def_19 )
| ( sk_c9 = iPr_def_15 )
| ( sk_c11 = iPr_def_23 ) ),
inference(superposition,[status(thm)],[c_134748,c_922]) ).
tcf(c_141437,plain,
( ( iPr_def_16 = iPr_def_19 )
| ( multiply(sk_c11,sk_c10) = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_134748,c_842]) ).
tcf(c_141599,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( multiply(X0,inverse(X0)) = multiply(X2,X1) )
| ( X0 != X2 )
| ( inverse(X0) != X1 ) ),
inference(instantiation,[status(thm)],[c_930]) ).
tcf(c_141601,plain,
( ( multiply(sk_c10,inverse(sk_c10)) = multiply(sk_c10,sk_c10) )
| ( sk_c10 != sk_c10 )
| ( inverse(sk_c10) != sk_c10 ) ),
inference(instantiation,[status(thm)],[c_141599]) ).
tcf(c_142065,plain,
( ( iPr_def_16 = iPr_def_19 )
| ( sk_c9 = iPr_def_15 ) ),
inference(global_subsumption_just,[status(thm)],[c_141428,c_845,c_1724,c_1829,c_4977,c_4978,c_22891,c_41001,c_46072,c_46139,c_46140,c_75795,c_133274]) ).
tcf(c_142092,plain,
( ( iPr_def_16 = iPr_def_19 )
| ~ iPr_def_11
| ( sk_c10 != iPr_def_15 )
| ( sk_c10 != identity ) ),
inference(superposition,[status(thm)],[c_142065,c_84954]) ).
tcf(c_142146,plain,
( ( iPr_def_16 = iPr_def_19 )
| ( multiply(iPr_def_15,sk_c11) = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_142065,c_836]) ).
tcf(c_142759,plain,
( ( iPr_def_16 = iPr_def_19 )
| ( iPr_def_15 = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_134896,c_40372]) ).
tcf(c_142993,plain,
( ( iPr_def_16 = iPr_def_19 )
| ( identity = iPr_def_27 )
| ( sk_c10 = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_135247,c_906]) ).
tcf(c_142997,plain,
( ( iPr_def_16 = iPr_def_19 )
| ( identity = iPr_def_31 )
| ( sk_c11 = iPr_def_27 ) ),
inference(superposition,[status(thm)],[c_135247,c_896]) ).
tcf(c_142999,plain,
( ( iPr_def_16 = iPr_def_19 )
| ( identity = iPr_def_31 )
| ( sk_c11 = iPr_def_24 ) ),
inference(superposition,[status(thm)],[c_135247,c_893]) ).
tcf(c_143000,plain,
( ( iPr_def_16 = iPr_def_19 )
| ( identity = iPr_def_31 )
| ( sk_c11 = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_135247,c_891]) ).
tcf(c_143008,plain,
( ( iPr_def_16 = iPr_def_19 )
| ( multiply(sk_c9,identity) = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_135247,c_836]) ).
tcf(c_143356,plain,
( ( iPr_def_16 = iPr_def_19 )
| ( multiply(iPr_def_15,iPr_def_15) = sk_c4 ) ),
inference(superposition,[status(thm)],[c_142759,c_85576]) ).
tcf(c_143388,plain,
( ( iPr_def_16 = iPr_def_19 )
| ( sk_c11 = sk_c4 ) ),
inference(light_normalisation,[status(thm)],[c_143356,c_85696]) ).
tcf(c_149165,plain,
( ( iPr_def_16 = iPr_def_19 )
| ( sk_c10 = sk_c11 ) ),
inference(superposition,[status(thm)],[c_143388,c_133446]) ).
tcf(c_149175,plain,
( ( iPr_def_16 = iPr_def_19 )
| ( sk_c11 = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_143388,c_85566]) ).
tcf(c_154285,plain,
( ( iPr_def_16 = iPr_def_19 )
| ( sk_c10 = identity ) ),
inference(superposition,[status(thm)],[c_149165,c_135247]) ).
tcf(c_154307,plain,
( ( iPr_def_16 = iPr_def_19 )
| ~ iPr_def_10 ),
inference(superposition,[status(thm)],[c_149165,c_86459]) ).
tcf(c_154427,plain,
( ( iPr_def_16 = iPr_def_19 )
| ( multiply(sk_c10,sk_c10) = iPr_def_15 ) ),
inference(superposition,[status(thm)],[c_149165,c_835]) ).
tcf(c_156620,plain,
( ( iPr_def_16 = iPr_def_19 )
| ( identity = iPr_def_27 ) ),
inference(global_subsumption_just,[status(thm)],[c_142993,c_8320,c_43443,c_69745,c_101743,c_113468]) ).
tcf(c_156675,plain,
! [X0: $i] :
( ( iPr_def_16 = iPr_def_19 )
| ( multiply(iPr_def_27,X0) = X0 ) ),
inference(superposition,[status(thm)],[c_156620,c_123]) ).
tcf(c_157965,plain,
( ( sk_c11 = inverse(sk_c3) )
| ( sk_c11 != identity )
| ( inverse(sk_c3) != identity ) ),
inference(instantiation,[status(thm)],[c_139011]) ).
tcf(c_157976,plain,
( ( iPr_def_16 = iPr_def_19 )
| ( sk_c11 = iPr_def_27 ) ),
inference(global_subsumption_just,[status(thm)],[c_142997,c_847,c_4990,c_4991,c_103608,c_135247,c_137105,c_156620,c_157965]) ).
tcf(c_158194,plain,
( ( iPr_def_16 = iPr_def_19 )
| ( multiply(sk_c9,iPr_def_27) = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_157976,c_836]) ).
tcf(c_158683,plain,
( ( iPr_def_16 = iPr_def_19 )
| ( sk_c11 = iPr_def_24 ) ),
inference(global_subsumption_just,[status(thm)],[c_142999,c_8320,c_101427,c_157976]) ).
tcf(c_159155,plain,
! [X0: $i,X1: $i] :
( ( sk_c11 = multiply(X0,X1) )
| ( sk_c11 != iPr_def_22 )
| ( multiply(X0,X1) != iPr_def_22 ) ),
inference(instantiation,[status(thm)],[c_100941]) ).
tcf(c_159157,plain,
( ( sk_c11 = multiply(sk_c10,sk_c10) )
| ( sk_c11 != iPr_def_22 )
| ( multiply(sk_c10,sk_c10) != iPr_def_22 ) ),
inference(instantiation,[status(thm)],[c_159155]) ).
tcf(c_159556,plain,
( ( iPr_def_16 = iPr_def_19 )
| ( sk_c11 = iPr_def_22 ) ),
inference(global_subsumption_just,[status(thm)],[c_143000,c_8175,c_101405,c_158683]) ).
tcf(c_167069,plain,
( ( iPr_def_16 = iPr_def_19 )
| ( multiply(sk_c10,sk_c10) = iPr_def_22 ) ),
inference(superposition,[status(thm)],[c_149165,c_141437]) ).
tcf(c_169429,plain,
( ( iPr_def_16 = iPr_def_19 )
| ( multiply(iPr_def_15,iPr_def_15) = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_149175,c_142146]) ).
tcf(c_169431,plain,
( ( iPr_def_16 = iPr_def_19 )
| ( multiply(iPr_def_15,sk_c10) = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_149165,c_142146]) ).
tcf(c_169513,plain,
( ( iPr_def_16 = iPr_def_19 )
| ( identity = iPr_def_16 ) ),
inference(light_normalisation,[status(thm)],[c_169431,c_85711]) ).
tcf(c_169518,plain,
( ( iPr_def_16 = iPr_def_19 )
| ( sk_c11 = iPr_def_16 ) ),
inference(light_normalisation,[status(thm)],[c_169429,c_85696]) ).
tcf(c_180957,plain,
( ( iPr_def_16 = iPr_def_19 )
| ( sk_c9 = iPr_def_16 ) ),
inference(demodulation,[status(thm)],[c_143008,c_34466]) ).
tcf(c_181000,plain,
( ( iPr_def_16 = iPr_def_19 )
| ~ iPr_def_12
| ( identity != iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_180957,c_81721]) ).
tcf(c_187738,plain,
( ( iPr_def_16 = iPr_def_19 )
| ( sk_c10 = iPr_def_16 ) ),
inference(superposition,[status(thm)],[c_169518,c_149165]) ).
tcf(c_191208,plain,
( ( iPr_def_16 = iPr_def_19 )
| ~ iPr_def_13
| ( sk_c11 != iPr_def_15 )
| ( inverse(sk_c10) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_154427,c_854]) ).
tcf(c_191293,plain,
( ( iPr_def_16 = iPr_def_19 )
| ~ iPr_def_13
| ( sk_c11 != iPr_def_15 ) ),
inference(light_normalisation,[status(thm)],[c_191208,c_85712]) ).
tcf(c_193476,plain,
! [X0: $i] :
( ( iPr_def_16 = iPr_def_19 )
| ~ iPr_def_14
| ( inverse(X0) != inverse(iPr_def_27) )
| ( inverse(inverse(iPr_def_27)) != inverse(X0) )
| ( multiply(inverse(X0),sk_c10) != sk_c11 )
| ( multiply(X0,inverse(X0)) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_156675,c_853]) ).
tcf(c_193509,plain,
! [X0: $i] :
( ( iPr_def_16 = iPr_def_19 )
| ~ iPr_def_14
| ( inverse(X0) != iPr_def_27 )
| ( inverse(X0) != sk_c3 )
| ( multiply(inverse(X0),sk_c10) != sk_c11 )
| ( multiply(X0,inverse(X0)) != sk_c11 ) ),
inference(light_normalisation,[status(thm)],[c_193476,c_847,c_34947]) ).
tcf(c_193519,plain,
( ( iPr_def_16 = iPr_def_19 )
| ~ iPr_def_14
| ( inverse(sk_c10) != iPr_def_27 )
| ( inverse(sk_c10) != sk_c3 )
| ( multiply(sk_c10,inverse(sk_c10)) != sk_c11 )
| ( multiply(inverse(sk_c10),sk_c10) != sk_c11 ) ),
inference(instantiation,[status(thm)],[c_193509]) ).
tcf(c_193520,plain,
iPr_def_16 = iPr_def_19,
inference(global_subsumption_just,[status(thm)],[c_158194,c_198,c_933,c_934,c_837,c_847,c_2874,c_2884,c_4989,c_29956,c_33901,c_85490,c_85700,c_89314,c_111179,c_111178,c_112244,c_118672,c_133678,c_134053,c_135247,c_141601,c_142065,c_142092,c_149175,c_154307,c_154285,c_159157,c_159556,c_167069,c_169513,c_181000,c_187738,c_191293,c_193519]) ).
tcf(c_193634,plain,
( ~ iPr_def_11
| ( sk_c10 != iPr_def_29 )
| ( sk_c10 != iPr_def_16 ) ),
inference(demodulation,[status(thm)],[c_5306,c_193520]) ).
tcf(c_193689,plain,
( ( iPr_def_16 = iPr_def_30 )
| ( identity = iPr_def_26 ) ),
inference(demodulation,[status(thm)],[c_75415,c_193520]) ).
tcf(c_193690,plain,
( ( iPr_def_16 = iPr_def_31 )
| ( identity = iPr_def_26 ) ),
inference(demodulation,[status(thm)],[c_74971,c_193520]) ).
tcf(c_193757,plain,
! [X0: $i] : multiply(iPr_def_29,multiply(iPr_def_16,X0)) = multiply(sk_c9,X0),
inference(demodulation,[status(thm)],[c_10015,c_193520]) ).
tcf(c_193784,plain,
multiply(sk_c2,iPr_def_16) = multiply(iPr_def_16,sk_c11),
inference(demodulation,[status(thm)],[c_25797,c_193520]) ).
tcf(c_193785,plain,
! [X0: $i] : multiply(sk_c2,multiply(sk_c9,X0)) = multiply(iPr_def_16,X0),
inference(demodulation,[status(thm)],[c_4619,c_193520]) ).
tcf(c_193843,plain,
multiply(iPr_def_29,iPr_def_16) = sk_c9,
inference(demodulation,[status(thm)],[c_10012,c_193520]) ).
tcf(c_193854,plain,
multiply(sk_c2,sk_c9) = iPr_def_16,
inference(demodulation,[status(thm)],[c_839,c_193520]) ).
tcf(c_194176,plain,
! [X0: $i] :
( ( iPr_def_16 = iPr_def_30 )
| ( multiply(iPr_def_26,X0) = X0 ) ),
inference(superposition,[status(thm)],[c_193689,c_123]) ).
tcf(c_194232,plain,
( ( iPr_def_16 = iPr_def_31 )
| ( inverse(iPr_def_26) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_193690,c_34501]) ).
tcf(c_195489,plain,
multiply(iPr_def_29,multiply(iPr_def_16,sk_c11)) = iPr_def_16,
inference(superposition,[status(thm)],[c_193784,c_4632]) ).
tcf(c_201719,plain,
multiply(sk_c9,identity) = multiply(iPr_def_29,iPr_def_16),
inference(superposition,[status(thm)],[c_34466,c_193757]) ).
tcf(c_201901,plain,
( ( sk_c11 = iPr_def_27 )
| ( multiply(sk_c2,iPr_def_16) = multiply(iPr_def_16,iPr_def_31) ) ),
inference(superposition,[status(thm)],[c_2517,c_193785]) ).
tcf(c_201908,plain,
multiply(sk_c2,sk_c9) = multiply(iPr_def_16,identity),
inference(superposition,[status(thm)],[c_34466,c_193785]) ).
tcf(c_201979,plain,
( ( sk_c11 = iPr_def_27 )
| ( multiply(iPr_def_16,sk_c11) = multiply(iPr_def_16,iPr_def_31) ) ),
inference(light_normalisation,[status(thm)],[c_201901,c_193784]) ).
tcf(c_205954,plain,
! [X0: $i] : multiply(inverse(multiply(X0,sk_c9)),multiply(X0,iPr_def_16)) = sk_c11,
inference(superposition,[status(thm)],[c_836,c_32292]) ).
tcf(c_229920,plain,
multiply(iPr_def_15,iPr_def_25) = inverse(iPr_def_26),
inference(demodulation,[status(thm)],[c_89714,c_34466]) ).
tcf(c_229928,plain,
multiply(sk_c10,inverse(iPr_def_26)) = iPr_def_25,
inference(superposition,[status(thm)],[c_229920,c_85585]) ).
tcf(c_229931,plain,
multiply(iPr_def_26,inverse(iPr_def_26)) = multiply(sk_c4,iPr_def_25),
inference(superposition,[status(thm)],[c_229920,c_86423]) ).
tcf(c_229933,plain,
multiply(iPr_def_26,inverse(iPr_def_26)) = identity,
inference(light_normalisation,[status(thm)],[c_229931,c_38851]) ).
tcf(c_230230,plain,
( ~ iPr_def_14
| ( inverse(sk_c10) != iPr_def_25 )
| ( inverse(inverse(sk_c10)) != inverse(iPr_def_26) )
| ( multiply(iPr_def_26,inverse(iPr_def_26)) != sk_c11 )
| ( multiply(inverse(iPr_def_26),sk_c10) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_229928,c_853]) ).
tcf(c_230309,plain,
( ~ iPr_def_14
| ( iPr_def_15 != iPr_def_25 )
| ( sk_c11 != identity )
| ( inverse(iPr_def_26) != sk_c10 )
| ( multiply(inverse(iPr_def_26),sk_c10) != sk_c11 ) ),
inference(light_normalisation,[status(thm)],[c_230230,c_85586,c_85712,c_229933]) ).
tcf(c_231273,plain,
multiply(inverse(iPr_def_26),identity) = inverse(iPr_def_26),
inference(superposition,[status(thm)],[c_229933,c_32231]) ).
tcf(c_231276,plain,
( ~ iPr_def_14
| ( inverse(iPr_def_26) != identity )
| ( inverse(inverse(iPr_def_26)) != inverse(iPr_def_26) )
| ( multiply(iPr_def_26,inverse(iPr_def_26)) != sk_c11 )
| ( multiply(inverse(iPr_def_26),sk_c10) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_229933,c_853]) ).
tcf(c_231278,plain,
( ( iPr_def_16 = iPr_def_30 )
| ( inverse(iPr_def_26) = identity ) ),
inference(superposition,[status(thm)],[c_229933,c_194176]) ).
tcf(c_231280,plain,
( ( iPr_def_30 = iPr_def_31 )
| ( inverse(iPr_def_26) = identity ) ),
inference(superposition,[status(thm)],[c_229933,c_39151]) ).
tcf(c_231281,plain,
multiply(sk_c10,inverse(iPr_def_26)) = multiply(iPr_def_25,identity),
inference(superposition,[status(thm)],[c_229933,c_10513]) ).
tcf(c_231294,plain,
( ~ iPr_def_14
| ( sk_c11 != identity )
| ( inverse(iPr_def_26) != identity )
| ( inverse(inverse(iPr_def_26)) != inverse(iPr_def_26) )
| ( multiply(inverse(iPr_def_26),sk_c10) != sk_c11 ) ),
inference(light_normalisation,[status(thm)],[c_231276,c_229933]) ).
tcf(c_231619,plain,
multiply(iPr_def_15,iPr_def_31) = inverse(iPr_def_30),
inference(demodulation,[status(thm)],[c_91398,c_34466]) ).
tcf(c_231684,plain,
multiply(sk_c10,inverse(iPr_def_30)) = iPr_def_31,
inference(superposition,[status(thm)],[c_231619,c_85585]) ).
tcf(c_231685,plain,
multiply(iPr_def_30,inverse(iPr_def_30)) = multiply(sk_c1,iPr_def_31),
inference(superposition,[status(thm)],[c_231619,c_86447]) ).
tcf(c_231689,plain,
multiply(iPr_def_30,inverse(iPr_def_30)) = identity,
inference(light_normalisation,[status(thm)],[c_231685,c_61851]) ).
tcf(c_234784,plain,
multiply(inverse(iPr_def_16),multiply(sk_c2,iPr_def_16)) = sk_c11,
inference(superposition,[status(thm)],[c_193854,c_205954]) ).
tcf(c_234831,plain,
multiply(inverse(multiply(inverse(iPr_def_16),sk_c9)),identity) = sk_c11,
inference(superposition,[status(thm)],[c_124,c_205954]) ).
tcf(c_234899,plain,
multiply(inverse(iPr_def_16),multiply(iPr_def_16,sk_c11)) = sk_c11,
inference(light_normalisation,[status(thm)],[c_234784,c_193784]) ).
tcf(c_236148,plain,
( ~ iPr_def_14
| ( inverse(sk_c10) != iPr_def_31 )
| ( inverse(inverse(sk_c10)) != inverse(iPr_def_30) )
| ( multiply(iPr_def_30,inverse(iPr_def_30)) != sk_c11 )
| ( multiply(inverse(iPr_def_30),sk_c10) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_231684,c_853]) ).
tcf(c_236256,plain,
( ~ iPr_def_14
| ( iPr_def_15 != iPr_def_31 )
| ( sk_c11 != identity )
| ( inverse(iPr_def_30) != sk_c10 )
| ( multiply(inverse(iPr_def_30),sk_c10) != sk_c11 ) ),
inference(light_normalisation,[status(thm)],[c_236148,c_85586,c_85712,c_231689]) ).
tcf(c_236290,plain,
( ~ iPr_def_14
| ( inverse(iPr_def_30) != identity )
| ( inverse(inverse(iPr_def_30)) != inverse(iPr_def_30) )
| ( multiply(iPr_def_30,inverse(iPr_def_30)) != sk_c11 )
| ( multiply(inverse(iPr_def_30),sk_c10) != sk_c11 ) ),
inference(superposition,[status(thm)],[c_231689,c_853]) ).
tcf(c_236291,plain,
multiply(sk_c10,inverse(iPr_def_30)) = multiply(iPr_def_31,identity),
inference(superposition,[status(thm)],[c_231689,c_10020]) ).
tcf(c_236304,plain,
( ~ iPr_def_14
| ( sk_c11 != identity )
| ( inverse(iPr_def_30) != identity )
| ( inverse(inverse(iPr_def_30)) != inverse(iPr_def_30) )
| ( multiply(inverse(iPr_def_30),sk_c10) != sk_c11 ) ),
inference(light_normalisation,[status(thm)],[c_236290,c_231689]) ).
tcf(c_237366,plain,
inverse(multiply(inverse(iPr_def_16),sk_c9)) = sk_c11,
inference(demodulation,[status(thm)],[c_234831,c_34466]) ).
tcf(c_237401,plain,
( ( sk_c9 = iPr_def_15 )
| ( inverse(multiply(inverse(iPr_def_16),iPr_def_26)) = sk_c11 ) ),
inference(superposition,[status(thm)],[c_925,c_237366]) ).
tcf(c_237410,plain,
multiply(sk_c11,multiply(inverse(iPr_def_16),sk_c9)) = identity,
inference(superposition,[status(thm)],[c_237366,c_124]) ).
tcf(c_237413,plain,
multiply(sk_c11,multiply(inverse(iPr_def_16),iPr_def_16)) = sk_c11,
inference(superposition,[status(thm)],[c_237366,c_205954]) ).
tcf(c_238821,plain,
( ( sk_c9 = iPr_def_15 )
| ( multiply(sk_c11,multiply(inverse(iPr_def_16),iPr_def_26)) = identity ) ),
inference(superposition,[status(thm)],[c_237401,c_124]) ).
tcf(c_239673,plain,
( ( iPr_def_30 = iPr_def_31 )
| ( multiply(iPr_def_28,multiply(inverse(iPr_def_16),sk_c9)) = identity ) ),
inference(superposition,[status(thm)],[c_126166,c_237410]) ).
tcf(c_239678,plain,
( ( iPr_def_30 = iPr_def_31 )
| ( multiply(iPr_def_15,multiply(inverse(iPr_def_16),sk_c9)) = identity ) ),
inference(superposition,[status(thm)],[c_37716,c_237410]) ).
tcf(c_239711,plain,
( ( sk_c11 = iPr_def_27 )
| ( multiply(iPr_def_30,multiply(inverse(iPr_def_16),sk_c9)) = identity ) ),
inference(superposition,[status(thm)],[c_886,c_237410]) ).
tcf(c_239736,plain,
( ( iPr_def_30 = iPr_def_31 )
| ( multiply(sk_c11,multiply(inverse(iPr_def_16),iPr_def_16)) = identity ) ),
inference(superposition,[status(thm)],[c_121407,c_237410]) ).
tcf(c_239764,plain,
multiply(inverse(multiply(sk_c11,inverse(iPr_def_16))),identity) = sk_c9,
inference(superposition,[status(thm)],[c_237410,c_32292]) ).
tcf(c_239765,plain,
multiply(iPr_def_16,multiply(inverse(iPr_def_16),sk_c9)) = multiply(sk_c9,identity),
inference(superposition,[status(thm)],[c_237410,c_4617]) ).
tcf(c_239766,plain,
multiply(iPr_def_28,multiply(inverse(iPr_def_16),sk_c9)) = multiply(sk_c3,identity),
inference(superposition,[status(thm)],[c_237410,c_4612]) ).
tcf(c_239767,plain,
multiply(iPr_def_15,multiply(inverse(iPr_def_16),sk_c9)) = multiply(sk_c10,identity),
inference(superposition,[status(thm)],[c_237410,c_4611]) ).
tcf(c_244907,plain,
( ( sk_c11 = iPr_def_27 )
| ( multiply(iPr_def_30,multiply(inverse(iPr_def_16),iPr_def_15)) = identity ) ),
inference(superposition,[status(thm)],[c_926,c_239711]) ).
tcf(c_249681,plain,
( ( sk_c11 = iPr_def_27 )
| ( multiply(sk_c10,multiply(inverse(iPr_def_16),iPr_def_15)) = multiply(iPr_def_31,identity) ) ),
inference(superposition,[status(thm)],[c_244907,c_10020]) ).
tcf(c_253254,plain,
( ( sk_c9 = iPr_def_15 )
| ( multiply(inverse(multiply(sk_c11,inverse(iPr_def_16))),identity) = iPr_def_26 ) ),
inference(superposition,[status(thm)],[c_238821,c_32292]) ).
tcf(c_259165,plain,
$false,
inference(smt_impl_just,[status(thm)],[c_253254,c_249681,c_239767,c_239766,c_239765,c_239764,c_239736,c_239678,c_239673,c_237413,c_236304,c_236291,c_236256,c_236148,c_234899,c_231689,c_231685,c_231684,c_231619,c_231294,c_231281,c_231273,c_231280,c_231278,c_230309,c_229933,c_229931,c_229928,c_201979,c_201908,c_201719,c_195489,c_194232,c_193843,c_193784,c_193854,c_193634,c_193520,c_132583,c_129394,c_122756,c_121447,c_96184,c_96141,c_95357,c_94447,c_94050,c_94017,c_91415,c_91408,c_87378,c_87238,c_85832,c_85712,c_85700,c_85587,c_85586,c_85584,c_85576,c_81721,c_81224,c_64423,c_64253,c_64223,c_62833,c_62826,c_62830,c_62572,c_62523,c_61887,c_61853,c_53456,c_53363,c_52338,c_42949,c_41622,c_41593,c_39815,c_39780,c_38581,c_35144,c_34947,c_34845,c_34840,c_34817,c_34513,c_34509,c_34481,c_34478,c_34501,c_32472,c_32287,c_32283,c_32281,c_23868,c_22981,c_22819,c_22747,c_18058,c_5467,c_5031,c_2600,c_34522,c_927,c_897,c_877,c_875,c_867,c_866,c_865,c_864,c_863,c_862,c_851,c_849,c_847,c_845]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP350-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.11/0.38 % Computer : n026.cluster.edu
% 0.11/0.38 % Model : x86_64 x86_64
% 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.38 % Memory : 8046.5625MB
% 0.11/0.38 % OS : Linux 6.8.0-71-generic
% 0.11/0.38 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.38 % DateTime : Wed Sep 23 14:35:25 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.38 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.11/0.42 Running first-order theorem proving
% 0.11/0.42 Running: /export/starexec/sandbox/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/0.43
% 0.11/0.43 % ======== iProver multi-core TPTP/SMT =========
% 0.11/0.43
% 0.11/0.43 % Detected problem language: tptp
% 0.11/0.44 % Proving...
% 55.46/11.96 % SZS status Started for theBenchmark.p
% 55.46/11.96 % SZS status Unsatisfiable for theBenchmark.p
% 55.46/11.96
% 55.46/11.96 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 55.46/11.96
% 55.46/11.96 % ------ iProver source info
% 55.46/11.96
% 55.46/11.96 % git: date: 2026-07-19 20:42:38 +0200
% 55.46/11.96 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 55.46/11.96 % git: non_committed_changes: false
% 55.46/11.96
% 55.46/11.96 % ------ Parsing...% successful
% 55.46/11.96
% 55.46/11.96
% 55.46/11.96 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 55.46/11.96
% 55.46/11.96 % ------ Preprocessing... sup_sim: 0 sf_s rm: 0 0s sf_e pe_s pe_e %
% 55.46/11.96
% 55.46/11.96 % ------ Preprocessing... gs_s sp: 5 0s gs_e snvd_s sp: 0 0s snvd_e %
% 55.46/11.96
% 55.46/11.96 % ------ Preprocessing... sf_s rm: 0 0s sf_e
% 55.46/11.96 % ------ Proving...
% 55.46/11.96 % ------ Problem Properties
% 55.46/11.96
% 55.46/11.96 %
% 55.46/11.96 % clauses 96
% 55.46/11.96 % conjectures 76
% 55.46/11.96 % EPR 71
% 55.46/11.96 % Horn 25
% 55.46/11.96 % unary 20
% 55.46/11.96 % binary 70
% 55.46/11.96 % lits 185
% 55.46/11.96 % lits eq 175
% 55.46/11.97 % fd_pure 0
% 55.46/11.97 % fd_pseudo 0
% 55.46/11.97 % fd_cond 0
% 55.46/11.97 % fd_pseudo_cond 0
% 55.46/11.97 % AC symbols 0
% 55.46/11.97
% 55.46/11.97 % ------ Schedule dynamic 5 is on
% 55.46/11.97
% 55.46/11.97 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 55.46/11.97
% 55.46/11.97
% 55.46/11.97 % ------
% 55.46/11.97 % Current options:
% 55.46/11.97 % ------
% 55.46/11.97
% 55.46/11.97
% 55.46/11.97 %
% 55.46/11.97
% 55.46/11.97 % ------ Proving...
% 55.46/11.97 %
% 55.46/11.97
% 55.46/11.97 % SZS status Unsatisfiable for theBenchmark.p
% 55.46/11.97
% 55.46/11.97 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 55.46/11.99
% 55.46/11.99
%------------------------------------------------------------------------------