iProver---3.9.4.UNS-CRf.s

%------------------------------------------------------------------------------
% File     : iProver---3.9.4
% Problem  : GRP236-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 : n019.cluster.edu
% Model    : x86_64 x86_64
% CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory   : 8046.5625MB
% OS       : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit  : 300s
% DateTime : Fri Sep 25 01:32:05 PM UTC 2026

% Result   : Unsatisfiable 14.84s 12.83s
% Output   : CNFRefutation 14.84s
% Verified : 
% SZS Type : ERROR: Analysing output (MakeTreeStats ran out of CPU time)

% 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,
    inverse(sk_c8) = sk_c7,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_1) ).

fof(f6,negated_conjecture,
    ( inverse(sk_c4) = sk_c8
    | inverse(sk_c1) = sk_c8 ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_2) ).

fof(f7,plain,
    ( sk_c8 = inverse(sk_c4)
    | sk_c8 = inverse(sk_c1) ),
    inference(reorient_equations,[],[f6]) ).

fof(f8,negated_conjecture,
    ( multiply(sk_c4,sk_c7) = sk_c8
    | inverse(sk_c1) = sk_c8 ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_3) ).

fof(f9,plain,
    ( sk_c8 = multiply(sk_c4,sk_c7)
    | sk_c8 = inverse(sk_c1) ),
    inference(reorient_equations,[],[f8]) ).

fof(f10,negated_conjecture,
    ( multiply(sk_c8,sk_c6) = sk_c7
    | inverse(sk_c1) = sk_c8 ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_4) ).

fof(f11,plain,
    ( sk_c7 = multiply(sk_c8,sk_c6)
    | sk_c8 = inverse(sk_c1) ),
    inference(reorient_equations,[],[f10]) ).

fof(f12,negated_conjecture,
    ( multiply(sk_c5,sk_c8) = sk_c6
    | inverse(sk_c1) = sk_c8 ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_5) ).

fof(f13,plain,
    ( sk_c6 = multiply(sk_c5,sk_c8)
    | sk_c8 = inverse(sk_c1) ),
    inference(reorient_equations,[],[f12]) ).

fof(f14,negated_conjecture,
    ( inverse(sk_c5) = sk_c8
    | inverse(sk_c1) = sk_c8 ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_6) ).

fof(f15,plain,
    ( sk_c8 = inverse(sk_c5)
    | sk_c8 = inverse(sk_c1) ),
    inference(reorient_equations,[],[f14]) ).

fof(f16,negated_conjecture,
    ( inverse(sk_c4) = sk_c8
    | multiply(sk_c1,sk_c7) = sk_c8 ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_7) ).

fof(f17,plain,
    ( sk_c8 = inverse(sk_c4)
    | sk_c8 = multiply(sk_c1,sk_c7) ),
    inference(reorient_equations,[],[f16]) ).

fof(f18,negated_conjecture,
    ( multiply(sk_c4,sk_c7) = sk_c8
    | multiply(sk_c1,sk_c7) = sk_c8 ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_8) ).

fof(f19,plain,
    ( sk_c8 = multiply(sk_c4,sk_c7)
    | sk_c8 = multiply(sk_c1,sk_c7) ),
    inference(reorient_equations,[],[f18]) ).

fof(f20,negated_conjecture,
    ( multiply(sk_c8,sk_c6) = sk_c7
    | multiply(sk_c1,sk_c7) = sk_c8 ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_9) ).

fof(f21,plain,
    ( sk_c7 = multiply(sk_c8,sk_c6)
    | sk_c8 = multiply(sk_c1,sk_c7) ),
    inference(reorient_equations,[],[f20]) ).

fof(f24,negated_conjecture,
    ( inverse(sk_c5) = sk_c8
    | multiply(sk_c1,sk_c7) = sk_c8 ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_11) ).

fof(f25,plain,
    ( sk_c8 = inverse(sk_c5)
    | sk_c8 = multiply(sk_c1,sk_c7) ),
    inference(reorient_equations,[],[f24]) ).

fof(f26,negated_conjecture,
    ( inverse(sk_c4) = sk_c8
    | multiply(sk_c2,sk_c3) = sk_c7 ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_12) ).

fof(f27,plain,
    ( sk_c8 = inverse(sk_c4)
    | sk_c7 = multiply(sk_c2,sk_c3) ),
    inference(reorient_equations,[],[f26]) ).

fof(f28,negated_conjecture,
    ( multiply(sk_c4,sk_c7) = sk_c8
    | multiply(sk_c2,sk_c3) = sk_c7 ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_13) ).

fof(f29,plain,
    ( sk_c8 = multiply(sk_c4,sk_c7)
    | sk_c7 = multiply(sk_c2,sk_c3) ),
    inference(reorient_equations,[],[f28]) ).

fof(f30,negated_conjecture,
    ( multiply(sk_c8,sk_c6) = sk_c7
    | multiply(sk_c2,sk_c3) = sk_c7 ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_14) ).

fof(f31,plain,
    ( sk_c7 = multiply(sk_c8,sk_c6)
    | sk_c7 = multiply(sk_c2,sk_c3) ),
    inference(reorient_equations,[],[f30]) ).

fof(f32,negated_conjecture,
    ( multiply(sk_c5,sk_c8) = sk_c6
    | multiply(sk_c2,sk_c3) = sk_c7 ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_15) ).

fof(f33,plain,
    ( sk_c6 = multiply(sk_c5,sk_c8)
    | sk_c7 = multiply(sk_c2,sk_c3) ),
    inference(reorient_equations,[],[f32]) ).

fof(f34,negated_conjecture,
    ( inverse(sk_c5) = sk_c8
    | multiply(sk_c2,sk_c3) = sk_c7 ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_16) ).

fof(f35,plain,
    ( sk_c8 = inverse(sk_c5)
    | sk_c7 = multiply(sk_c2,sk_c3) ),
    inference(reorient_equations,[],[f34]) ).

fof(f36,negated_conjecture,
    ( inverse(sk_c4) = sk_c8
    | inverse(sk_c2) = sk_c3 ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_17) ).

fof(f37,plain,
    ( sk_c8 = inverse(sk_c4)
    | sk_c3 = inverse(sk_c2) ),
    inference(reorient_equations,[],[f36]) ).

fof(f38,negated_conjecture,
    ( multiply(sk_c4,sk_c7) = sk_c8
    | inverse(sk_c2) = sk_c3 ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_18) ).

fof(f39,plain,
    ( sk_c8 = multiply(sk_c4,sk_c7)
    | sk_c3 = inverse(sk_c2) ),
    inference(reorient_equations,[],[f38]) ).

fof(f40,negated_conjecture,
    ( multiply(sk_c8,sk_c6) = sk_c7
    | inverse(sk_c2) = sk_c3 ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_19) ).

fof(f41,plain,
    ( sk_c7 = multiply(sk_c8,sk_c6)
    | sk_c3 = inverse(sk_c2) ),
    inference(reorient_equations,[],[f40]) ).

fof(f42,negated_conjecture,
    ( multiply(sk_c5,sk_c8) = sk_c6
    | inverse(sk_c2) = sk_c3 ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_20) ).

fof(f43,plain,
    ( sk_c6 = multiply(sk_c5,sk_c8)
    | sk_c3 = inverse(sk_c2) ),
    inference(reorient_equations,[],[f42]) ).

fof(f44,negated_conjecture,
    ( inverse(sk_c5) = sk_c8
    | inverse(sk_c2) = sk_c3 ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_21) ).

fof(f45,plain,
    ( sk_c8 = inverse(sk_c5)
    | sk_c3 = inverse(sk_c2) ),
    inference(reorient_equations,[],[f44]) ).

fof(f46,negated_conjecture,
    ( inverse(sk_c4) = sk_c8
    | multiply(sk_c3,sk_c8) = sk_c7 ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_22) ).

fof(f47,plain,
    ( sk_c8 = inverse(sk_c4)
    | sk_c7 = multiply(sk_c3,sk_c8) ),
    inference(reorient_equations,[],[f46]) ).

fof(f48,negated_conjecture,
    ( multiply(sk_c4,sk_c7) = sk_c8
    | multiply(sk_c3,sk_c8) = sk_c7 ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_23) ).

fof(f49,plain,
    ( sk_c8 = multiply(sk_c4,sk_c7)
    | sk_c7 = multiply(sk_c3,sk_c8) ),
    inference(reorient_equations,[],[f48]) ).

fof(f50,negated_conjecture,
    ( multiply(sk_c8,sk_c6) = sk_c7
    | multiply(sk_c3,sk_c8) = sk_c7 ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_24) ).

fof(f51,plain,
    ( sk_c7 = multiply(sk_c8,sk_c6)
    | sk_c7 = multiply(sk_c3,sk_c8) ),
    inference(reorient_equations,[],[f50]) ).

fof(f52,negated_conjecture,
    ( multiply(sk_c5,sk_c8) = sk_c6
    | multiply(sk_c3,sk_c8) = sk_c7 ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_25) ).

fof(f53,plain,
    ( sk_c6 = multiply(sk_c5,sk_c8)
    | sk_c7 = multiply(sk_c3,sk_c8) ),
    inference(reorient_equations,[],[f52]) ).

fof(f54,negated_conjecture,
    ( inverse(sk_c5) = sk_c8
    | multiply(sk_c3,sk_c8) = sk_c7 ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_26) ).

fof(f55,plain,
    ( sk_c8 = inverse(sk_c5)
    | sk_c7 = multiply(sk_c3,sk_c8) ),
    inference(reorient_equations,[],[f54]) ).

fof(f56,negated_conjecture,
    ! [X2,X3,X0,X1,X4,X5] :
      ( inverse(X5) != sk_c8
      | multiply(X5,sk_c8) != X4
      | multiply(sk_c8,X4) != sk_c7
      | multiply(X3,sk_c7) != sk_c8
      | inverse(X3) != sk_c8
      | multiply(X2,sk_c8) != sk_c7
      | inverse(X1) != X2
      | multiply(X1,X2) != sk_c7
      | multiply(X0,sk_c7) != sk_c8
      | inverse(X0) != sk_c8
      | inverse(sk_c8) != sk_c7 ),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_this_27) ).

fof(f57,plain,
    ! [X2,X3,X0,X1,X4,X5] :
      ( sk_c8 != inverse(X5)
      | multiply(X5,sk_c8) != X4
      | sk_c7 != multiply(sk_c8,X4)
      | sk_c8 != multiply(X3,sk_c7)
      | sk_c8 != inverse(X3)
      | sk_c7 != multiply(X2,sk_c8)
      | inverse(X1) != X2
      | multiply(X1,X2) != sk_c7
      | sk_c8 != multiply(X0,sk_c7)
      | inverse(X0) != sk_c8
      | inverse(sk_c8) != sk_c7 ),
    inference(reorient_equations,[],[f56]) ).

fof(f58,plain,
    ! [X3,X0,X1,X4,X5] :
      ( sk_c8 != inverse(X5)
      | multiply(X5,sk_c8) != X4
      | sk_c7 != multiply(sk_c8,X4)
      | sk_c8 != multiply(X3,sk_c7)
      | sk_c8 != inverse(X3)
      | sk_c7 != multiply(inverse(X1),sk_c8)
      | sk_c7 != multiply(X1,inverse(X1))
      | sk_c8 != multiply(X0,sk_c7)
      | inverse(X0) != sk_c8
      | inverse(sk_c8) != sk_c7 ),
    inference(equality_resolution,[],[f57]) ).

fof(f59,plain,
    ! [X3,X0,X1,X5] :
      ( sk_c8 != inverse(X5)
      | sk_c7 != multiply(sk_c8,multiply(X5,sk_c8))
      | sk_c8 != multiply(X3,sk_c7)
      | sk_c8 != inverse(X3)
      | sk_c7 != multiply(inverse(X1),sk_c8)
      | sk_c7 != multiply(X1,inverse(X1))
      | sk_c8 != multiply(X0,sk_c7)
      | inverse(X0) != sk_c8
      | inverse(sk_c8) != sk_c7 ),
    inference(equality_resolution,[],[f58]) ).

tcf(c_79,plain,
    ! [X0: $i] : multiply(identity,X0) = X0,
    inference(cnf_transformation,[],[f1]) ).

tcf(c_80,plain,
    ! [X0: $i] : multiply(inverse(X0),X0) = identity,
    inference(cnf_transformation,[],[f3]) ).

tcf(c_81,plain,
    ! [X0: $i,X1: $i,X2: $i] : multiply(multiply(X0,X1),X2) = multiply(X0,multiply(X1,X2)),
    inference(cnf_transformation,[],[f4]) ).

tcf(c_82,negated_conjecture,
    inverse(sk_c8) = sk_c7,
    inference(cnf_transformation,[],[f5]) ).

tcf(c_83,negated_conjecture,
    ( ( inverse(sk_c4) = sk_c8 )
    | ( inverse(sk_c1) = sk_c8 ) ),
    inference(cnf_transformation,[],[f7]) ).

tcf(c_84,negated_conjecture,
    ( ( inverse(sk_c1) = sk_c8 )
    | ( multiply(sk_c4,sk_c7) = sk_c8 ) ),
    inference(cnf_transformation,[],[f9]) ).

tcf(c_85,negated_conjecture,
    ( ( inverse(sk_c1) = sk_c8 )
    | ( multiply(sk_c8,sk_c6) = sk_c7 ) ),
    inference(cnf_transformation,[],[f11]) ).

tcf(c_86,negated_conjecture,
    ( ( inverse(sk_c1) = sk_c8 )
    | ( multiply(sk_c5,sk_c8) = sk_c6 ) ),
    inference(cnf_transformation,[],[f13]) ).

tcf(c_87,negated_conjecture,
    ( ( inverse(sk_c5) = sk_c8 )
    | ( inverse(sk_c1) = sk_c8 ) ),
    inference(cnf_transformation,[],[f15]) ).

tcf(c_88,negated_conjecture,
    ( ( inverse(sk_c4) = sk_c8 )
    | ( multiply(sk_c1,sk_c7) = sk_c8 ) ),
    inference(cnf_transformation,[],[f17]) ).

tcf(c_89,negated_conjecture,
    ( ( multiply(sk_c4,sk_c7) = sk_c8 )
    | ( multiply(sk_c1,sk_c7) = sk_c8 ) ),
    inference(cnf_transformation,[],[f19]) ).

tcf(c_90,negated_conjecture,
    ( ( multiply(sk_c1,sk_c7) = sk_c8 )
    | ( multiply(sk_c8,sk_c6) = sk_c7 ) ),
    inference(cnf_transformation,[],[f21]) ).

tcf(c_92,negated_conjecture,
    ( ( inverse(sk_c5) = sk_c8 )
    | ( multiply(sk_c1,sk_c7) = sk_c8 ) ),
    inference(cnf_transformation,[],[f25]) ).

tcf(c_93,negated_conjecture,
    ( ( inverse(sk_c4) = sk_c8 )
    | ( multiply(sk_c2,sk_c3) = sk_c7 ) ),
    inference(cnf_transformation,[],[f27]) ).

tcf(c_94,negated_conjecture,
    ( ( multiply(sk_c2,sk_c3) = sk_c7 )
    | ( multiply(sk_c4,sk_c7) = sk_c8 ) ),
    inference(cnf_transformation,[],[f29]) ).

tcf(c_95,negated_conjecture,
    ( ( multiply(sk_c2,sk_c3) = sk_c7 )
    | ( multiply(sk_c8,sk_c6) = sk_c7 ) ),
    inference(cnf_transformation,[],[f31]) ).

tcf(c_96,negated_conjecture,
    ( ( multiply(sk_c2,sk_c3) = sk_c7 )
    | ( multiply(sk_c5,sk_c8) = sk_c6 ) ),
    inference(cnf_transformation,[],[f33]) ).

tcf(c_97,negated_conjecture,
    ( ( inverse(sk_c5) = sk_c8 )
    | ( multiply(sk_c2,sk_c3) = sk_c7 ) ),
    inference(cnf_transformation,[],[f35]) ).

tcf(c_98,negated_conjecture,
    ( ( inverse(sk_c2) = sk_c3 )
    | ( inverse(sk_c4) = sk_c8 ) ),
    inference(cnf_transformation,[],[f37]) ).

tcf(c_99,negated_conjecture,
    ( ( inverse(sk_c2) = sk_c3 )
    | ( multiply(sk_c4,sk_c7) = sk_c8 ) ),
    inference(cnf_transformation,[],[f39]) ).

tcf(c_100,negated_conjecture,
    ( ( inverse(sk_c2) = sk_c3 )
    | ( multiply(sk_c8,sk_c6) = sk_c7 ) ),
    inference(cnf_transformation,[],[f41]) ).

tcf(c_101,negated_conjecture,
    ( ( inverse(sk_c2) = sk_c3 )
    | ( multiply(sk_c5,sk_c8) = sk_c6 ) ),
    inference(cnf_transformation,[],[f43]) ).

tcf(c_102,negated_conjecture,
    ( ( inverse(sk_c2) = sk_c3 )
    | ( inverse(sk_c5) = sk_c8 ) ),
    inference(cnf_transformation,[],[f45]) ).

tcf(c_103,negated_conjecture,
    ( ( inverse(sk_c4) = sk_c8 )
    | ( multiply(sk_c3,sk_c8) = sk_c7 ) ),
    inference(cnf_transformation,[],[f47]) ).

tcf(c_104,negated_conjecture,
    ( ( multiply(sk_c3,sk_c8) = sk_c7 )
    | ( multiply(sk_c4,sk_c7) = sk_c8 ) ),
    inference(cnf_transformation,[],[f49]) ).

tcf(c_105,negated_conjecture,
    ( ( multiply(sk_c3,sk_c8) = sk_c7 )
    | ( multiply(sk_c8,sk_c6) = sk_c7 ) ),
    inference(cnf_transformation,[],[f51]) ).

tcf(c_106,negated_conjecture,
    ( ( multiply(sk_c3,sk_c8) = sk_c7 )
    | ( multiply(sk_c5,sk_c8) = sk_c6 ) ),
    inference(cnf_transformation,[],[f53]) ).

tcf(c_107,negated_conjecture,
    ( ( inverse(sk_c5) = sk_c8 )
    | ( multiply(sk_c3,sk_c8) = sk_c7 ) ),
    inference(cnf_transformation,[],[f55]) ).

tcf(c_108,negated_conjecture,
    ! [X0: $i,X1: $i,X2: $i,X3: $i] :
      ( ( inverse(sk_c8) != sk_c7 )
      | ( inverse(X2) != sk_c8 )
      | ( inverse(X1) != sk_c8 )
      | ( inverse(X0) != sk_c8 )
      | ( multiply(X1,sk_c7) != sk_c8 )
      | ( multiply(X0,sk_c7) != sk_c8 )
      | ( multiply(inverse(X3),sk_c8) != sk_c7 )
      | ( multiply(X3,inverse(X3)) != sk_c7 )
      | ( multiply(sk_c8,multiply(X2,sk_c8)) != sk_c7 ) ),
    inference(cnf_transformation,[],[f59]) ).

tcf(c_113,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i] :
      ( ( multiply(sk_c8,multiply(X2,sk_c8)) != sk_c7 )
      | ( multiply(X3,inverse(X3)) != sk_c7 )
      | ( multiply(inverse(X3),sk_c8) != sk_c7 )
      | ( multiply(X0,sk_c7) != sk_c8 )
      | ( multiply(X1,sk_c7) != sk_c8 )
      | ( inverse(X0) != sk_c8 )
      | ( inverse(X1) != sk_c8 )
      | ( inverse(X2) != sk_c8 ) ),
    inference(global_subsumption_just,[status(thm)],[c_108,c_82,c_108]) ).

tcf(c_114,negated_conjecture,
    ! [X0: $i,X1: $i,X2: $i,X3: $i] :
      ( ( inverse(X3) != sk_c8 )
      | ( inverse(X2) != sk_c8 )
      | ( inverse(X0) != sk_c8 )
      | ( multiply(X3,sk_c7) != sk_c8 )
      | ( multiply(X2,sk_c7) != sk_c8 )
      | ( multiply(inverse(X1),sk_c8) != sk_c7 )
      | ( multiply(X1,inverse(X1)) != sk_c7 )
      | ( multiply(sk_c8,multiply(X0,sk_c8)) != sk_c7 ) ),
    inference(renaming,[status(thm)],[c_113]) ).

tcf(c_358,negated_conjecture,
    ! [X0: $i] :
      ( ~ iPr_def_10
      | ( inverse(X0) != sk_c8 )
      | ( multiply(X0,sk_c7) != sk_c8 ) ),
    inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_10])],[c_114]) ).

tcf(c_359,negated_conjecture,
    ! [X0: $i] :
      ( ~ iPr_def_11
      | ( multiply(inverse(X0),sk_c8) != sk_c7 )
      | ( multiply(X0,inverse(X0)) != sk_c7 ) ),
    inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_11])],[c_114]) ).

tcf(c_360,negated_conjecture,
    ! [X0: $i] :
      ( ~ iPr_def_12
      | ( inverse(X0) != sk_c8 )
      | ( multiply(sk_c8,multiply(X0,sk_c8)) != sk_c7 ) ),
    inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_12])],[c_114]) ).

tcf(c_361,negated_conjecture,
    ( iPr_def_12
    | iPr_def_11
    | iPr_def_10 ),
    inference(splitting,[splitting(split),new_symbols(definition,[])],[c_114]) ).

tcf(c_362,definition,
    iPr_def_13 = multiply(sk_c3,sk_c8),
    introduced(definition,[new_symbols(definition,[iPr_def_13])],[]) ).

tcf(c_363,definition,
    iPr_def_14 = inverse(sk_c5),
    introduced(definition,[new_symbols(definition,[iPr_def_14])],[]) ).

tcf(c_364,definition,
    iPr_def_15 = multiply(sk_c5,sk_c8),
    introduced(definition,[new_symbols(definition,[iPr_def_15])],[]) ).

tcf(c_365,definition,
    iPr_def_16 = multiply(sk_c8,sk_c6),
    introduced(definition,[new_symbols(definition,[iPr_def_16])],[]) ).

tcf(c_366,definition,
    iPr_def_17 = multiply(sk_c4,sk_c7),
    introduced(definition,[new_symbols(definition,[iPr_def_17])],[]) ).

tcf(c_367,definition,
    iPr_def_18 = inverse(sk_c4),
    introduced(definition,[new_symbols(definition,[iPr_def_18])],[]) ).

tcf(c_368,definition,
    iPr_def_19 = inverse(sk_c2),
    introduced(definition,[new_symbols(definition,[iPr_def_19])],[]) ).

tcf(c_369,definition,
    iPr_def_20 = multiply(sk_c2,sk_c3),
    introduced(definition,[new_symbols(definition,[iPr_def_20])],[]) ).

tcf(c_370,definition,
    iPr_def_21 = multiply(sk_c1,sk_c7),
    introduced(definition,[new_symbols(definition,[iPr_def_21])],[]) ).

tcf(c_371,definition,
    iPr_def_22 = inverse(sk_c1),
    introduced(definition,[new_symbols(definition,[iPr_def_22])],[]) ).

tcf(c_372,definition,
    iPr_def_23 = inverse(sk_c8),
    introduced(definition,[new_symbols(definition,[iPr_def_23])],[]) ).

tcf(c_373,negated_conjecture,
    ( iPr_def_12
    | iPr_def_11
    | iPr_def_10 ),
    inference(demodulation,[status(thm)],[c_361]) ).

tcf(c_374,negated_conjecture,
    ! [X0: $i] :
      ( ~ iPr_def_12
      | ( inverse(X0) != sk_c8 )
      | ( multiply(sk_c8,multiply(X0,sk_c8)) != sk_c7 ) ),
    inference(demodulation,[status(thm)],[c_360]) ).

tcf(c_376,negated_conjecture,
    ! [X0: $i] :
      ( ~ iPr_def_11
      | ( multiply(inverse(X0),sk_c8) != sk_c7 )
      | ( multiply(X0,inverse(X0)) != sk_c7 ) ),
    inference(demodulation,[status(thm)],[c_359]) ).

tcf(c_377,negated_conjecture,
    ! [X0: $i] :
      ( ~ iPr_def_10
      | ( inverse(X0) != sk_c8 )
      | ( multiply(X0,sk_c7) != sk_c8 ) ),
    inference(demodulation,[status(thm)],[c_358]) ).

tcf(c_378,negated_conjecture,
    ( ( iPr_def_14 = sk_c8 )
    | ( iPr_def_13 = sk_c7 ) ),
    inference(demodulation,[status(thm)],[c_107,c_363,c_362]) ).

tcf(c_379,negated_conjecture,
    ( ( iPr_def_15 = sk_c6 )
    | ( iPr_def_13 = sk_c7 ) ),
    inference(demodulation,[status(thm)],[c_106,c_364]) ).

tcf(c_380,negated_conjecture,
    ( ( iPr_def_16 = sk_c7 )
    | ( iPr_def_13 = sk_c7 ) ),
    inference(demodulation,[status(thm)],[c_105,c_365]) ).

tcf(c_381,negated_conjecture,
    ( ( iPr_def_17 = sk_c8 )
    | ( iPr_def_13 = sk_c7 ) ),
    inference(demodulation,[status(thm)],[c_104,c_366]) ).

tcf(c_382,negated_conjecture,
    ( ( iPr_def_18 = sk_c8 )
    | ( iPr_def_13 = sk_c7 ) ),
    inference(demodulation,[status(thm)],[c_103,c_367]) ).

tcf(c_383,negated_conjecture,
    ( ( iPr_def_19 = sk_c3 )
    | ( iPr_def_14 = sk_c8 ) ),
    inference(demodulation,[status(thm)],[c_102,c_368]) ).

tcf(c_384,negated_conjecture,
    ( ( iPr_def_19 = sk_c3 )
    | ( iPr_def_15 = sk_c6 ) ),
    inference(demodulation,[status(thm)],[c_101]) ).

tcf(c_385,negated_conjecture,
    ( ( iPr_def_19 = sk_c3 )
    | ( iPr_def_16 = sk_c7 ) ),
    inference(demodulation,[status(thm)],[c_100]) ).

tcf(c_386,negated_conjecture,
    ( ( iPr_def_19 = sk_c3 )
    | ( iPr_def_17 = sk_c8 ) ),
    inference(demodulation,[status(thm)],[c_99]) ).

tcf(c_387,negated_conjecture,
    ( ( iPr_def_19 = sk_c3 )
    | ( iPr_def_18 = sk_c8 ) ),
    inference(demodulation,[status(thm)],[c_98]) ).

tcf(c_388,negated_conjecture,
    ( ( iPr_def_20 = sk_c7 )
    | ( iPr_def_14 = sk_c8 ) ),
    inference(demodulation,[status(thm)],[c_97,c_369]) ).

tcf(c_389,negated_conjecture,
    ( ( iPr_def_20 = sk_c7 )
    | ( iPr_def_15 = sk_c6 ) ),
    inference(demodulation,[status(thm)],[c_96]) ).

tcf(c_390,negated_conjecture,
    ( ( iPr_def_20 = sk_c7 )
    | ( iPr_def_16 = sk_c7 ) ),
    inference(demodulation,[status(thm)],[c_95]) ).

tcf(c_391,negated_conjecture,
    ( ( iPr_def_20 = sk_c7 )
    | ( iPr_def_17 = sk_c8 ) ),
    inference(demodulation,[status(thm)],[c_94]) ).

tcf(c_392,negated_conjecture,
    ( ( iPr_def_20 = sk_c7 )
    | ( iPr_def_18 = sk_c8 ) ),
    inference(demodulation,[status(thm)],[c_93]) ).

tcf(c_393,negated_conjecture,
    ( ( iPr_def_21 = sk_c8 )
    | ( iPr_def_14 = sk_c8 ) ),
    inference(demodulation,[status(thm)],[c_92,c_370]) ).

tcf(c_395,negated_conjecture,
    ( ( iPr_def_21 = sk_c8 )
    | ( iPr_def_16 = sk_c7 ) ),
    inference(demodulation,[status(thm)],[c_90]) ).

tcf(c_396,negated_conjecture,
    ( ( iPr_def_21 = sk_c8 )
    | ( iPr_def_17 = sk_c8 ) ),
    inference(demodulation,[status(thm)],[c_89]) ).

tcf(c_397,negated_conjecture,
    ( ( iPr_def_21 = sk_c8 )
    | ( iPr_def_18 = sk_c8 ) ),
    inference(demodulation,[status(thm)],[c_88]) ).

tcf(c_398,negated_conjecture,
    ( ( iPr_def_22 = sk_c8 )
    | ( iPr_def_14 = sk_c8 ) ),
    inference(demodulation,[status(thm)],[c_87,c_371]) ).

tcf(c_399,negated_conjecture,
    ( ( iPr_def_22 = sk_c8 )
    | ( iPr_def_15 = sk_c6 ) ),
    inference(demodulation,[status(thm)],[c_86]) ).

tcf(c_400,negated_conjecture,
    ( ( iPr_def_22 = sk_c8 )
    | ( iPr_def_16 = sk_c7 ) ),
    inference(demodulation,[status(thm)],[c_85]) ).

tcf(c_401,negated_conjecture,
    ( ( iPr_def_22 = sk_c8 )
    | ( iPr_def_17 = sk_c8 ) ),
    inference(demodulation,[status(thm)],[c_84]) ).

tcf(c_402,negated_conjecture,
    ( ( iPr_def_22 = sk_c8 )
    | ( iPr_def_18 = sk_c8 ) ),
    inference(demodulation,[status(thm)],[c_83]) ).

tcf(c_403,negated_conjecture,
    iPr_def_23 = sk_c7,
    inference(demodulation,[status(thm)],[c_82,c_372]) ).

tcf(c_404,plain,
    ! [X0: $i] : X0 = X0,
    theory(equality) ).

tcf(c_405,plain,
    ! [X0: $i,X1: $i,X2: $i] :
      ( ( X2 = X0 )
      | ( X2 != X1 )
      | ( X0 != X1 ) ),
    theory(equality) ).

tcf(c_406,plain,
    ! [X0: $i,X1: $i] :
      ( ( inverse(X0) = inverse(X1) )
      | ( X0 != X1 ) ),
    theory(equality) ).

tcf(c_408,plain,
    ( ( inverse(sk_c8) = inverse(sk_c8) )
    | ( sk_c8 != sk_c8 ) ),
    inference(instantiation,[status(thm)],[c_406]) ).

tcf(c_410,plain,
    sk_c8 = sk_c8,
    inference(instantiation,[status(thm)],[c_404]) ).

tcf(c_589,plain,
    ( ( iPr_def_13 = iPr_def_23 )
    | ( sk_c8 = iPr_def_14 ) ),
    inference(light_normalisation,[status(thm)],[c_378,c_403]) ).

tcf(c_596,plain,
    ( ( iPr_def_13 = iPr_def_23 )
    | ( sk_c6 = iPr_def_15 ) ),
    inference(light_normalisation,[status(thm)],[c_379,c_403]) ).

tcf(c_603,plain,
    ( ( iPr_def_16 = iPr_def_23 )
    | ( iPr_def_13 = iPr_def_23 ) ),
    inference(light_normalisation,[status(thm)],[c_380,c_403]) ).

tcf(c_610,plain,
    ( ( iPr_def_13 = iPr_def_23 )
    | ( sk_c8 = iPr_def_17 ) ),
    inference(light_normalisation,[status(thm)],[c_381,c_403]) ).

tcf(c_617,plain,
    ( ( iPr_def_14 = iPr_def_17 )
    | ( iPr_def_13 = iPr_def_23 ) ),
    inference(superposition,[status(thm)],[c_589,c_610]) ).

tcf(c_621,plain,
    ( ( iPr_def_13 = iPr_def_23 )
    | ( sk_c8 = iPr_def_18 ) ),
    inference(light_normalisation,[status(thm)],[c_382,c_403]) ).

tcf(c_672,plain,
    ( ( iPr_def_13 = iPr_def_23 )
    | ( multiply(iPr_def_14,sk_c6) = iPr_def_16 ) ),
    inference(superposition,[status(thm)],[c_589,c_365]) ).

tcf(c_686,plain,
    ( ( sk_c3 = iPr_def_19 )
    | ( multiply(sk_c8,iPr_def_15) = iPr_def_16 ) ),
    inference(superposition,[status(thm)],[c_384,c_365]) ).

tcf(c_689,plain,
    ( ( iPr_def_16 = iPr_def_23 )
    | ( sk_c3 = iPr_def_19 ) ),
    inference(light_normalisation,[status(thm)],[c_385,c_403]) ).

tcf(c_696,plain,
    ( ( iPr_def_16 = iPr_def_23 )
    | ( multiply(iPr_def_19,sk_c8) = iPr_def_13 ) ),
    inference(superposition,[status(thm)],[c_689,c_362]) ).

tcf(c_713,plain,
    ( ( iPr_def_20 = iPr_def_23 )
    | ( sk_c8 = iPr_def_14 ) ),
    inference(light_normalisation,[status(thm)],[c_388,c_403]) ).

tcf(c_722,plain,
    ( ( iPr_def_20 = iPr_def_23 )
    | ( multiply(iPr_def_14,sk_c6) = iPr_def_16 ) ),
    inference(superposition,[status(thm)],[c_713,c_365]) ).

tcf(c_736,plain,
    ( ( iPr_def_20 = iPr_def_23 )
    | ( sk_c6 = iPr_def_15 ) ),
    inference(light_normalisation,[status(thm)],[c_389,c_403]) ).

tcf(c_746,plain,
    ( ( iPr_def_20 = iPr_def_23 )
    | ( iPr_def_16 = iPr_def_23 ) ),
    inference(light_normalisation,[status(thm)],[c_390,c_403]) ).

tcf(c_758,plain,
    ( ( iPr_def_20 = iPr_def_23 )
    | ( sk_c8 = iPr_def_17 ) ),
    inference(light_normalisation,[status(thm)],[c_391,c_403]) ).

tcf(c_768,plain,
    ( ( iPr_def_20 = iPr_def_23 )
    | ( iPr_def_14 = iPr_def_17 ) ),
    inference(superposition,[status(thm)],[c_758,c_713]) ).

tcf(c_785,plain,
    multiply(sk_c4,iPr_def_23) = iPr_def_17,
    inference(light_normalisation,[status(thm)],[c_366,c_403]) ).

tcf(c_792,plain,
    ( ( sk_c8 = iPr_def_18 )
    | ( multiply(sk_c2,iPr_def_19) = iPr_def_20 ) ),
    inference(superposition,[status(thm)],[c_387,c_369]) ).

tcf(c_793,plain,
    ( ( sk_c8 = iPr_def_17 )
    | ( multiply(sk_c2,iPr_def_19) = iPr_def_20 ) ),
    inference(superposition,[status(thm)],[c_386,c_369]) ).

tcf(c_794,plain,
    ( ( iPr_def_16 = iPr_def_23 )
    | ( multiply(sk_c2,iPr_def_19) = iPr_def_20 ) ),
    inference(superposition,[status(thm)],[c_689,c_369]) ).

tcf(c_795,plain,
    ( ( sk_c8 = iPr_def_14 )
    | ( multiply(sk_c2,iPr_def_19) = iPr_def_20 ) ),
    inference(superposition,[status(thm)],[c_383,c_369]) ).

tcf(c_804,plain,
    multiply(sk_c1,iPr_def_23) = iPr_def_21,
    inference(light_normalisation,[status(thm)],[c_370,c_403]) ).

tcf(c_811,plain,
    ! [X0: $i,X1: $i] :
      ( ( inverse(X0) = sk_c8 )
      | ( sk_c8 != X1 )
      | ( inverse(X0) != X1 ) ),
    inference(instantiation,[status(thm)],[c_405]) ).

tcf(c_812,plain,
    multiply(iPr_def_23,sk_c8) = identity,
    inference(superposition,[status(thm)],[c_372,c_80]) ).

tcf(c_813,plain,
    multiply(iPr_def_22,sk_c1) = identity,
    inference(superposition,[status(thm)],[c_371,c_80]) ).

tcf(c_814,plain,
    multiply(iPr_def_18,sk_c4) = identity,
    inference(superposition,[status(thm)],[c_367,c_80]) ).

tcf(c_815,plain,
    multiply(iPr_def_14,sk_c5) = identity,
    inference(superposition,[status(thm)],[c_363,c_80]) ).

tcf(c_816,plain,
    multiply(iPr_def_19,sk_c2) = identity,
    inference(superposition,[status(thm)],[c_368,c_80]) ).

tcf(c_818,plain,
    ! [X0: $i] : inverse(X0) = inverse(X0),
    inference(instantiation,[status(thm)],[c_404]) ).

tcf(c_821,plain,
    ! [X0: $i,X1: $i,X2: $i] :
      ( ( inverse(X0) = X2 )
      | ( X2 != X1 )
      | ( inverse(X0) != X1 ) ),
    inference(instantiation,[status(thm)],[c_405]) ).

tcf(c_823,plain,
    ( ( iPr_def_20 = iPr_def_23 )
    | ( sk_c8 = iPr_def_18 ) ),
    inference(light_normalisation,[status(thm)],[c_392,c_403]) ).

tcf(c_835,plain,
    ( ( iPr_def_20 = iPr_def_23 )
    | ( iPr_def_14 = iPr_def_18 ) ),
    inference(superposition,[status(thm)],[c_823,c_713]) ).

tcf(c_838,plain,
    ( ( iPr_def_20 = iPr_def_23 )
    | ( inverse(iPr_def_18) = iPr_def_23 ) ),
    inference(superposition,[status(thm)],[c_823,c_372]) ).

tcf(c_861,plain,
    ! [X0: $i,X1: $i,X2: $i] :
      ( ( inverse(X0) = X2 )
      | ( X2 != inverse(X1) )
      | ( inverse(X0) != inverse(X1) ) ),
    inference(instantiation,[status(thm)],[c_821]) ).

tcf(c_873,plain,
    ( ( iPr_def_13 = iPr_def_23 )
    | ( multiply(iPr_def_23,iPr_def_17) = identity ) ),
    inference(superposition,[status(thm)],[c_610,c_812]) ).

tcf(c_896,plain,
    ! [X0: $i,X1: $i,X2: $i] :
      ( ( X2 = inverse(X0) )
      | ( X2 != X1 )
      | ( inverse(X0) != X1 ) ),
    inference(instantiation,[status(thm)],[c_405]) ).

tcf(c_897,plain,
    ! [X0: $i,X1: $i,X2: $i] :
      ( ( inverse(X0) = inverse(X2) )
      | ( inverse(X2) != inverse(X1) )
      | ( inverse(X0) != inverse(X1) ) ),
    inference(instantiation,[status(thm)],[c_861]) ).

tcf(c_898,plain,
    ! [X0: $i] :
      ( ( inverse(X0) = iPr_def_14 )
      | ( iPr_def_14 != inverse(sk_c5) )
      | ( inverse(X0) != inverse(sk_c5) ) ),
    inference(instantiation,[status(thm)],[c_861]) ).

tcf(c_904,plain,
    ! [X0: $i] :
      ( ( inverse(X0) = iPr_def_22 )
      | ( iPr_def_22 != inverse(sk_c1) )
      | ( inverse(X0) != inverse(sk_c1) ) ),
    inference(instantiation,[status(thm)],[c_861]) ).

tcf(c_906,plain,
    ! [X0: $i] :
      ( ( inverse(X0) = iPr_def_23 )
      | ( iPr_def_23 != inverse(sk_c8) )
      | ( inverse(X0) != inverse(sk_c8) ) ),
    inference(instantiation,[status(thm)],[c_861]) ).

tcf(c_907,plain,
    ( ( inverse(sk_c8) = iPr_def_23 )
    | ( iPr_def_23 != inverse(sk_c8) )
    | ( inverse(sk_c8) != inverse(sk_c8) ) ),
    inference(instantiation,[status(thm)],[c_906]) ).

tcf(c_952,plain,
    ! [X0: $i] :
      ( ( inverse(X0) = sk_c8 )
      | ( sk_c8 != iPr_def_14 )
      | ( inverse(X0) != iPr_def_14 ) ),
    inference(instantiation,[status(thm)],[c_811]) ).

tcf(c_962,plain,
    ( ( iPr_def_16 = iPr_def_23 )
    | ( sk_c8 = iPr_def_21 ) ),
    inference(light_normalisation,[status(thm)],[c_395,c_403]) ).

tcf(c_1030,plain,
    ( ( sk_c8 = iPr_def_17 )
    | ( multiply(sk_c5,iPr_def_21) = iPr_def_15 ) ),
    inference(superposition,[status(thm)],[c_396,c_364]) ).

tcf(c_1062,plain,
    ! [X0: $i] :
      ( ( inverse(X0) = sk_c8 )
      | ( sk_c8 != iPr_def_23 )
      | ( inverse(X0) != iPr_def_23 ) ),
    inference(instantiation,[status(thm)],[c_811]) ).

tcf(c_1063,plain,
    ( ( inverse(sk_c8) = sk_c8 )
    | ( sk_c8 != iPr_def_23 )
    | ( inverse(sk_c8) != iPr_def_23 ) ),
    inference(instantiation,[status(thm)],[c_1062]) ).

tcf(c_1080,plain,
    ( ( sk_c8 = iPr_def_18 )
    | ( multiply(sk_c5,iPr_def_21) = iPr_def_15 ) ),
    inference(superposition,[status(thm)],[c_397,c_364]) ).

tcf(c_1134,plain,
    ( ( sk_c8 = iPr_def_14 )
    | ( multiply(sk_c5,iPr_def_22) = iPr_def_15 ) ),
    inference(superposition,[status(thm)],[c_398,c_364]) ).

tcf(c_1172,plain,
    ! [X0: $i,X1: $i,X2: $i] :
      ( ( X2 = inverse(X0) )
      | ( X2 != inverse(X1) )
      | ( inverse(X0) != inverse(X1) ) ),
    inference(instantiation,[status(thm)],[c_896]) ).

tcf(c_1175,plain,
    ! [X0: $i,X1: $i] :
      ( ( X1 = inverse(X0) )
      | ( X1 != iPr_def_14 )
      | ( inverse(X0) != iPr_def_14 ) ),
    inference(instantiation,[status(thm)],[c_896]) ).

tcf(c_1178,plain,
    ! [X0: $i,X1: $i] :
      ( ( X1 = inverse(X0) )
      | ( X1 != iPr_def_22 )
      | ( inverse(X0) != iPr_def_22 ) ),
    inference(instantiation,[status(thm)],[c_896]) ).

tcf(c_1179,plain,
    ! [X0: $i,X1: $i] :
      ( ( X1 = inverse(X0) )
      | ( X1 != iPr_def_23 )
      | ( inverse(X0) != iPr_def_23 ) ),
    inference(instantiation,[status(thm)],[c_896]) ).

tcf(c_1187,plain,
    ! [X0: $i] :
      ( ( sk_c8 = iPr_def_19 )
      | ( iPr_def_19 != X0 )
      | ( sk_c8 != X0 ) ),
    inference(instantiation,[status(thm)],[c_405]) ).

tcf(c_1198,plain,
    ( ( iPr_def_16 = iPr_def_23 )
    | ( sk_c8 = iPr_def_22 ) ),
    inference(light_normalisation,[status(thm)],[c_400,c_403]) ).

tcf(c_1217,plain,
    ( ( iPr_def_21 = iPr_def_22 )
    | ( iPr_def_16 = iPr_def_23 ) ),
    inference(superposition,[status(thm)],[c_1198,c_962]) ).

tcf(c_1225,plain,
    ( ( iPr_def_16 = iPr_def_23 )
    | ( inverse(iPr_def_22) = iPr_def_23 ) ),
    inference(superposition,[status(thm)],[c_1198,c_372]) ).

tcf(c_1251,plain,
    ! [X0: $i] :
      ( ( sk_c8 = iPr_def_23 )
      | ( iPr_def_23 != X0 )
      | ( sk_c8 != X0 ) ),
    inference(instantiation,[status(thm)],[c_405]) ).

tcf(c_1261,plain,
    ! [X0: $i,X1: $i] :
      ( ( X0 = iPr_def_19 )
      | ( iPr_def_19 != X1 )
      | ( X0 != X1 ) ),
    inference(instantiation,[status(thm)],[c_405]) ).

tcf(c_1290,plain,
    ( ( sk_c8 = iPr_def_17 )
    | ( multiply(sk_c5,iPr_def_22) = iPr_def_15 ) ),
    inference(superposition,[status(thm)],[c_401,c_364]) ).

tcf(c_1324,plain,
    ! [X0: $i,X1: $i] :
      ( ( X0 = iPr_def_23 )
      | ( iPr_def_23 != X1 )
      | ( X0 != X1 ) ),
    inference(instantiation,[status(thm)],[c_405]) ).

tcf(c_1360,plain,
    ( ( sk_c8 = iPr_def_18 )
    | ( multiply(sk_c5,iPr_def_22) = iPr_def_15 ) ),
    inference(superposition,[status(thm)],[c_402,c_364]) ).

tcf(c_1395,plain,
    ( ( inverse(sk_c5) = iPr_def_14 )
    | ( iPr_def_14 != inverse(sk_c5) )
    | ( inverse(sk_c5) != inverse(sk_c5) ) ),
    inference(instantiation,[status(thm)],[c_898]) ).

tcf(c_1396,plain,
    inverse(sk_c5) = inverse(sk_c5),
    inference(instantiation,[status(thm)],[c_818]) ).

tcf(c_1400,plain,
    ! [X0: $i] : multiply(sk_c5,multiply(sk_c8,X0)) = multiply(iPr_def_15,X0),
    inference(superposition,[status(thm)],[c_364,c_81]) ).

tcf(c_1401,plain,
    ! [X0: $i] : multiply(sk_c2,multiply(sk_c3,X0)) = multiply(iPr_def_20,X0),
    inference(superposition,[status(thm)],[c_369,c_81]) ).

tcf(c_1402,plain,
    ! [X0: $i] : multiply(sk_c3,multiply(sk_c8,X0)) = multiply(iPr_def_13,X0),
    inference(superposition,[status(thm)],[c_362,c_81]) ).

tcf(c_1404,plain,
    ! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(X0,X1)) = multiply(identity,X1),
    inference(superposition,[status(thm)],[c_80,c_81]) ).

tcf(c_1406,plain,
    ! [X0: $i] : multiply(sk_c4,multiply(iPr_def_23,X0)) = multiply(iPr_def_17,X0),
    inference(superposition,[status(thm)],[c_785,c_81]) ).

tcf(c_1407,plain,
    ! [X0: $i] : multiply(sk_c1,multiply(iPr_def_23,X0)) = multiply(iPr_def_21,X0),
    inference(superposition,[status(thm)],[c_804,c_81]) ).

tcf(c_1408,plain,
    ! [X0: $i] : multiply(iPr_def_23,multiply(sk_c8,X0)) = multiply(identity,X0),
    inference(superposition,[status(thm)],[c_812,c_81]) ).

tcf(c_1409,plain,
    ! [X0: $i] : multiply(iPr_def_22,multiply(sk_c1,X0)) = multiply(identity,X0),
    inference(superposition,[status(thm)],[c_813,c_81]) ).

tcf(c_1410,plain,
    ! [X0: $i] : multiply(iPr_def_18,multiply(sk_c4,X0)) = multiply(identity,X0),
    inference(superposition,[status(thm)],[c_814,c_81]) ).

tcf(c_1411,plain,
    ! [X0: $i] : multiply(iPr_def_14,multiply(sk_c5,X0)) = multiply(identity,X0),
    inference(superposition,[status(thm)],[c_815,c_81]) ).

tcf(c_1413,plain,
    ! [X0: $i] : multiply(iPr_def_14,multiply(sk_c5,X0)) = X0,
    inference(light_normalisation,[status(thm)],[c_1411,c_79]) ).

tcf(c_1414,plain,
    ! [X0: $i] : multiply(iPr_def_18,multiply(sk_c4,X0)) = X0,
    inference(light_normalisation,[status(thm)],[c_1410,c_79]) ).

tcf(c_1415,plain,
    ! [X0: $i] : multiply(iPr_def_22,multiply(sk_c1,X0)) = X0,
    inference(light_normalisation,[status(thm)],[c_1409,c_79]) ).

tcf(c_1416,plain,
    ! [X0: $i] : multiply(iPr_def_23,multiply(sk_c8,X0)) = X0,
    inference(light_normalisation,[status(thm)],[c_1408,c_79]) ).

tcf(c_1492,plain,
    ! [X0: $i] :
      ( ( inverse(X0) = inverse(sk_c2) )
      | ( X0 != sk_c2 ) ),
    inference(instantiation,[status(thm)],[c_406]) ).

tcf(c_1493,plain,
    ( ( inverse(sk_c8) = inverse(sk_c2) )
    | ( sk_c8 != sk_c2 ) ),
    inference(instantiation,[status(thm)],[c_1492]) ).

tcf(c_1495,plain,
    inverse(sk_c2) = inverse(sk_c2),
    inference(instantiation,[status(thm)],[c_818]) ).

tcf(c_1498,plain,
    ! [X0: $i] : multiply(iPr_def_19,multiply(sk_c2,X0)) = multiply(identity,X0),
    inference(superposition,[status(thm)],[c_816,c_81]) ).

tcf(c_1499,plain,
    ! [X0: $i] : multiply(iPr_def_19,multiply(sk_c2,X0)) = X0,
    inference(light_normalisation,[status(thm)],[c_1498,c_79]) ).

tcf(c_1556,plain,
    ! [X0: $i] :
      ( ( inverse(X0) = inverse(sk_c1) )
      | ( X0 != sk_c1 ) ),
    inference(instantiation,[status(thm)],[c_406]) ).

tcf(c_1557,plain,
    ( ( inverse(sk_c8) = inverse(sk_c1) )
    | ( sk_c8 != sk_c1 ) ),
    inference(instantiation,[status(thm)],[c_1556]) ).

tcf(c_1558,plain,
    ( ( inverse(sk_c1) = iPr_def_22 )
    | ( iPr_def_22 != inverse(sk_c1) )
    | ( inverse(sk_c1) != inverse(sk_c1) ) ),
    inference(instantiation,[status(thm)],[c_904]) ).

tcf(c_1559,plain,
    inverse(sk_c1) = inverse(sk_c1),
    inference(instantiation,[status(thm)],[c_818]) ).

tcf(c_1592,plain,
    ( ( iPr_def_14 = iPr_def_17 )
    | ( iPr_def_13 = iPr_def_20 ) ),
    inference(superposition,[status(thm)],[c_768,c_617]) ).

tcf(c_1593,plain,
    ( ( iPr_def_14 = iPr_def_17 )
    | ( multiply(iPr_def_20,sk_c8) = identity ) ),
    inference(superposition,[status(thm)],[c_768,c_812]) ).

tcf(c_1666,plain,
    iPr_def_23 = iPr_def_23,
    inference(instantiation,[status(thm)],[c_404]) ).

tcf(c_1669,plain,
    ! [X0: $i] :
      ( ~ iPr_def_10
      | ( inverse(X0) != sk_c8 )
      | ( multiply(X0,iPr_def_23) != sk_c8 ) ),
    inference(light_normalisation,[status(thm)],[c_377,c_403]) ).

tcf(c_1682,plain,
    ( ~ iPr_def_10
    | ( sk_c8 != iPr_def_17 )
    | ( inverse(sk_c4) != sk_c8 ) ),
    inference(superposition,[status(thm)],[c_785,c_1669]) ).

tcf(c_1683,plain,
    ( ~ iPr_def_10
    | ( sk_c8 != iPr_def_21 )
    | ( inverse(sk_c1) != sk_c8 ) ),
    inference(superposition,[status(thm)],[c_804,c_1669]) ).

tcf(c_1685,plain,
    ! [X0: $i] :
      ( ( iPr_def_14 = iPr_def_17 )
      | ~ iPr_def_10
      | ( inverse(X0) != sk_c8 )
      | ( multiply(X0,iPr_def_20) != sk_c8 ) ),
    inference(superposition,[status(thm)],[c_768,c_1669]) ).

tcf(c_1691,plain,
    ( ~ iPr_def_10
    | ( sk_c8 != iPr_def_22 )
    | ( sk_c8 != iPr_def_21 ) ),
    inference(light_normalisation,[status(thm)],[c_1683,c_371]) ).

tcf(c_1695,plain,
    ( ~ iPr_def_10
    | ( sk_c8 != iPr_def_18 )
    | ( sk_c8 != iPr_def_17 ) ),
    inference(light_normalisation,[status(thm)],[c_1682,c_367]) ).

tcf(c_1741,plain,
    ( ( iPr_def_14 = iPr_def_17 )
    | ~ iPr_def_10
    | ( inverse(sk_c8) != sk_c8 )
    | ( multiply(sk_c8,iPr_def_20) != sk_c8 ) ),
    inference(instantiation,[status(thm)],[c_1685]) ).

tcf(c_1758,plain,
    ! [X0: $i] :
      ( ( iPr_def_23 = inverse(X0) )
      | ( iPr_def_23 != inverse(sk_c8) )
      | ( inverse(X0) != inverse(sk_c8) ) ),
    inference(instantiation,[status(thm)],[c_1172]) ).

tcf(c_1771,plain,
    ! [X0: $i] :
      ( ~ iPr_def_12
      | ( inverse(X0) != sk_c8 )
      | ( multiply(sk_c8,multiply(X0,sk_c8)) != iPr_def_23 ) ),
    inference(light_normalisation,[status(thm)],[c_374,c_403]) ).

tcf(c_1795,plain,
    ( ~ iPr_def_12
    | ( inverse(sk_c5) != sk_c8 )
    | ( multiply(sk_c8,iPr_def_15) != iPr_def_23 ) ),
    inference(superposition,[status(thm)],[c_364,c_1771]) ).

tcf(c_1824,plain,
    ( ~ iPr_def_12
    | ( sk_c8 != iPr_def_14 )
    | ( multiply(sk_c8,iPr_def_15) != iPr_def_23 ) ),
    inference(light_normalisation,[status(thm)],[c_1795,c_363]) ).

tcf(c_1916,plain,
    ! [X0: $i] :
      ( ( X0 = inverse(sk_c5) )
      | ( X0 != iPr_def_14 )
      | ( inverse(sk_c5) != iPr_def_14 ) ),
    inference(instantiation,[status(thm)],[c_1175]) ).

tcf(c_1919,plain,
    ( ( inverse(sk_c5) = sk_c8 )
    | ( sk_c8 != iPr_def_14 )
    | ( inverse(sk_c5) != iPr_def_14 ) ),
    inference(instantiation,[status(thm)],[c_952]) ).

tcf(c_1947,plain,
    ! [X0: $i] :
      ( ~ iPr_def_11
      | ( multiply(inverse(X0),sk_c8) != iPr_def_23 )
      | ( multiply(X0,inverse(X0)) != iPr_def_23 ) ),
    inference(light_normalisation,[status(thm)],[c_376,c_403]) ).

tcf(c_1959,plain,
    ( ~ iPr_def_11
    | ( multiply(sk_c8,iPr_def_23) != iPr_def_23 )
    | ( multiply(inverse(sk_c8),sk_c8) != iPr_def_23 ) ),
    inference(superposition,[status(thm)],[c_372,c_1947]) ).

tcf(c_1983,plain,
    ( ~ iPr_def_11
    | ( identity != iPr_def_23 )
    | ( multiply(sk_c8,iPr_def_23) != iPr_def_23 ) ),
    inference(light_normalisation,[status(thm)],[c_1959,c_372,c_812]) ).

tcf(c_2119,plain,
    ! [X0: $i,X1: $i] :
      ( ( iPr_def_23 = X0 )
      | ( iPr_def_23 != X1 )
      | ( X0 != X1 ) ),
    inference(instantiation,[status(thm)],[c_405]) ).

tcf(c_2420,plain,
    ! [X0: $i] :
      ( ( X0 = iPr_def_19 )
      | ( iPr_def_19 != inverse(sk_c2) )
      | ( X0 != inverse(sk_c2) ) ),
    inference(instantiation,[status(thm)],[c_1261]) ).

tcf(c_2471,plain,
    ! [X0: $i] :
      ( ( X0 = iPr_def_23 )
      | ( iPr_def_23 != sk_c7 )
      | ( X0 != sk_c7 ) ),
    inference(instantiation,[status(thm)],[c_1324]) ).

tcf(c_2484,plain,
    ( ( iPr_def_14 = iPr_def_18 )
    | ( multiply(iPr_def_20,sk_c8) = identity ) ),
    inference(superposition,[status(thm)],[c_835,c_812]) ).

tcf(c_2567,plain,
    multiply(iPr_def_14,iPr_def_15) = sk_c8,
    inference(superposition,[status(thm)],[c_364,c_1413]) ).

tcf(c_2572,plain,
    multiply(iPr_def_18,iPr_def_17) = iPr_def_23,
    inference(superposition,[status(thm)],[c_785,c_1414]) ).

tcf(c_2602,plain,
    identity = identity,
    inference(instantiation,[status(thm)],[c_404]) ).

tcf(c_2606,plain,
    multiply(iPr_def_22,iPr_def_21) = iPr_def_23,
    inference(superposition,[status(thm)],[c_804,c_1415]) ).

tcf(c_2609,plain,
    ! [X0: $i] : multiply(iPr_def_22,multiply(iPr_def_21,X0)) = multiply(iPr_def_23,X0),
    inference(superposition,[status(thm)],[c_2606,c_81]) ).

tcf(c_2669,plain,
    ( ( iPr_def_13 = iPr_def_23 )
    | ( sk_c3 = iPr_def_19 )
    | ( multiply(iPr_def_18,iPr_def_15) = iPr_def_16 ) ),
    inference(superposition,[status(thm)],[c_621,c_686]) ).

tcf(c_2758,plain,
    ! [X0: $i,X1: $i] :
      ( ( X0 = sk_c1 )
      | ( sk_c1 != X1 )
      | ( X0 != X1 ) ),
    inference(instantiation,[status(thm)],[c_405]) ).

tcf(c_2876,plain,
    ! [X0: $i] :
      ( ( iPr_def_14 = iPr_def_18 )
      | ( multiply(iPr_def_20,multiply(sk_c8,X0)) = X0 ) ),
    inference(superposition,[status(thm)],[c_835,c_1416]) ).

tcf(c_2878,plain,
    ! [X0: $i] :
      ( ( iPr_def_14 = iPr_def_17 )
      | ( multiply(iPr_def_20,multiply(sk_c8,X0)) = X0 ) ),
    inference(superposition,[status(thm)],[c_768,c_1416]) ).

tcf(c_2882,plain,
    ! [X0: $i] :
      ( ( iPr_def_16 = iPr_def_23 )
      | ( multiply(iPr_def_20,multiply(sk_c8,X0)) = X0 ) ),
    inference(superposition,[status(thm)],[c_746,c_1416]) ).

tcf(c_2884,plain,
    multiply(iPr_def_23,iPr_def_16) = sk_c6,
    inference(superposition,[status(thm)],[c_365,c_1416]) ).

tcf(c_2892,plain,
    ! [X0: $i] :
      ( ( sk_c8 = iPr_def_14 )
      | ( multiply(iPr_def_23,multiply(iPr_def_22,X0)) = X0 ) ),
    inference(superposition,[status(thm)],[c_398,c_1416]) ).

tcf(c_2993,plain,
    ! [X0: $i,X1: $i] :
      ( ( inverse(sk_c2) = inverse(X0) )
      | ( inverse(sk_c2) != inverse(X1) )
      | ( inverse(X0) != inverse(X1) ) ),
    inference(instantiation,[status(thm)],[c_897]) ).

tcf(c_3091,plain,
    ( ( iPr_def_14 = iPr_def_18 )
    | ( multiply(iPr_def_20,iPr_def_16) = sk_c6 ) ),
    inference(superposition,[status(thm)],[c_835,c_2884]) ).

tcf(c_3190,plain,
    ( ( sk_c7 = iPr_def_23 )
    | ( iPr_def_23 != sk_c7 )
    | ( sk_c7 != sk_c7 ) ),
    inference(instantiation,[status(thm)],[c_2471]) ).

tcf(c_3191,plain,
    sk_c7 = sk_c7,
    inference(instantiation,[status(thm)],[c_404]) ).

tcf(c_3192,plain,
    ! [X0: $i,X1: $i] :
      ( ( X0 = sk_c7 )
      | ( sk_c7 != X1 )
      | ( X0 != X1 ) ),
    inference(instantiation,[status(thm)],[c_405]) ).

tcf(c_3193,plain,
    ( ( iPr_def_16 = iPr_def_23 )
    | ( iPr_def_23 != sk_c7 )
    | ( iPr_def_16 != sk_c7 ) ),
    inference(instantiation,[status(thm)],[c_2471]) ).

tcf(c_3219,plain,
    multiply(iPr_def_19,iPr_def_20) = sk_c3,
    inference(superposition,[status(thm)],[c_369,c_1499]) ).

tcf(c_3225,plain,
    ! [X0: $i] : multiply(iPr_def_19,multiply(iPr_def_20,X0)) = multiply(sk_c3,X0),
    inference(superposition,[status(thm)],[c_3219,c_81]) ).

tcf(c_3263,plain,
    ! [X0: $i] :
      ( ( X0 = inverse(sk_c5) )
      | ( X0 != sk_c8 )
      | ( inverse(sk_c5) != sk_c8 ) ),
    inference(instantiation,[status(thm)],[c_896]) ).

tcf(c_3736,plain,
    ( ( sk_c8 = iPr_def_17 )
    | ( multiply(iPr_def_14,iPr_def_15) = iPr_def_21 ) ),
    inference(superposition,[status(thm)],[c_1030,c_1413]) ).

tcf(c_3737,plain,
    ( ( sk_c8 = iPr_def_21 )
    | ( sk_c8 = iPr_def_17 ) ),
    inference(light_normalisation,[status(thm)],[c_3736,c_2567]) ).

tcf(c_3914,plain,
    ( ( sk_c8 = iPr_def_18 )
    | ( multiply(iPr_def_14,iPr_def_15) = iPr_def_21 ) ),
    inference(superposition,[status(thm)],[c_1080,c_1413]) ).

tcf(c_3915,plain,
    ( ( sk_c8 = iPr_def_21 )
    | ( sk_c8 = iPr_def_18 ) ),
    inference(light_normalisation,[status(thm)],[c_3914,c_2567]) ).

tcf(c_4199,plain,
    ( ( sk_c8 = iPr_def_14 )
    | ( multiply(iPr_def_14,iPr_def_15) = iPr_def_22 ) ),
    inference(superposition,[status(thm)],[c_1134,c_1413]) ).

tcf(c_4200,plain,
    ( ( sk_c8 = iPr_def_22 )
    | ( sk_c8 = iPr_def_14 ) ),
    inference(light_normalisation,[status(thm)],[c_4199,c_2567]) ).

tcf(c_4395,plain,
    ( ( sk_c8 = iPr_def_17 )
    | ( multiply(iPr_def_14,iPr_def_15) = iPr_def_22 ) ),
    inference(superposition,[status(thm)],[c_1290,c_1413]) ).

tcf(c_4396,plain,
    ( ( sk_c8 = iPr_def_22 )
    | ( sk_c8 = iPr_def_17 ) ),
    inference(light_normalisation,[status(thm)],[c_4395,c_2567]) ).

tcf(c_4699,plain,
    ( ( sk_c8 = iPr_def_18 )
    | ( multiply(iPr_def_14,iPr_def_15) = iPr_def_22 ) ),
    inference(superposition,[status(thm)],[c_1360,c_1413]) ).

tcf(c_4700,plain,
    ( ( sk_c8 = iPr_def_22 )
    | ( sk_c8 = iPr_def_18 ) ),
    inference(light_normalisation,[status(thm)],[c_4699,c_2567]) ).

tcf(c_4863,plain,
    ( ( iPr_def_13 = iPr_def_23 )
    | ( multiply(iPr_def_14,iPr_def_15) = iPr_def_16 ) ),
    inference(superposition,[status(thm)],[c_596,c_672]) ).

tcf(c_4865,plain,
    ( ( iPr_def_13 = iPr_def_23 )
    | ( sk_c8 = iPr_def_16 ) ),
    inference(light_normalisation,[status(thm)],[c_4863,c_2567]) ).

tcf(c_4922,plain,
    ( ( iPr_def_13 = iPr_def_23 )
    | ( multiply(iPr_def_23,iPr_def_16) = identity ) ),
    inference(superposition,[status(thm)],[c_4865,c_812]) ).

tcf(c_4928,plain,
    ( ( iPr_def_13 = iPr_def_23 )
    | ( inverse(iPr_def_16) = iPr_def_23 ) ),
    inference(superposition,[status(thm)],[c_4865,c_372]) ).

tcf(c_4947,plain,
    ( ( iPr_def_13 = iPr_def_23 )
    | ( sk_c6 = identity ) ),
    inference(light_normalisation,[status(thm)],[c_4922,c_2884]) ).

tcf(c_5356,plain,
    ! [X0: $i] :
      ( ( iPr_def_23 = X0 )
      | ( iPr_def_23 != iPr_def_23 )
      | ( X0 != iPr_def_23 ) ),
    inference(instantiation,[status(thm)],[c_2119]) ).

tcf(c_5397,plain,
    ( ( iPr_def_13 = iPr_def_23 )
    | ( identity = iPr_def_15 ) ),
    inference(superposition,[status(thm)],[c_4947,c_596]) ).

tcf(c_5579,plain,
    ( ( iPr_def_16 = iPr_def_23 )
    | ( multiply(iPr_def_19,iPr_def_21) = iPr_def_13 ) ),
    inference(superposition,[status(thm)],[c_962,c_696]) ).

tcf(c_5609,plain,
    ( ( iPr_def_20 = iPr_def_23 )
    | ( multiply(iPr_def_14,iPr_def_15) = iPr_def_16 ) ),
    inference(superposition,[status(thm)],[c_736,c_722]) ).

tcf(c_5613,plain,
    ( ( iPr_def_20 = iPr_def_23 )
    | ( sk_c8 = iPr_def_16 ) ),
    inference(light_normalisation,[status(thm)],[c_5609,c_2567]) ).

tcf(c_5675,plain,
    ( ( iPr_def_20 = iPr_def_23 )
    | ( multiply(iPr_def_23,iPr_def_16) = identity ) ),
    inference(superposition,[status(thm)],[c_5613,c_812]) ).

tcf(c_5700,plain,
    ( ( iPr_def_20 = iPr_def_23 )
    | ( sk_c6 = identity ) ),
    inference(light_normalisation,[status(thm)],[c_5675,c_2884]) ).

tcf(c_5741,plain,
    ! [X0: $i,X1: $i] :
      ( ( identity = X0 )
      | ( identity != X1 )
      | ( X0 != X1 ) ),
    inference(instantiation,[status(thm)],[c_405]) ).

tcf(c_5743,plain,
    ( ( identity = inverse(sk_c5) )
    | ( identity != iPr_def_14 )
    | ( inverse(sk_c5) != iPr_def_14 ) ),
    inference(instantiation,[status(thm)],[c_1916]) ).

tcf(c_5788,plain,
    ( ( iPr_def_23 = iPr_def_19 )
    | ( iPr_def_23 != inverse(sk_c2) )
    | ( iPr_def_19 != inverse(sk_c2) ) ),
    inference(instantiation,[status(thm)],[c_2420]) ).

tcf(c_5789,plain,
    ( ( iPr_def_23 = inverse(sk_c2) )
    | ( iPr_def_23 != inverse(sk_c8) )
    | ( inverse(sk_c2) != inverse(sk_c8) ) ),
    inference(instantiation,[status(thm)],[c_1758]) ).

tcf(c_7345,plain,
    ! [X0: $i] :
      ( ( inverse(sk_c2) = inverse(X0) )
      | ( inverse(sk_c2) != inverse(sk_c2) )
      | ( inverse(X0) != inverse(sk_c2) ) ),
    inference(instantiation,[status(thm)],[c_2993]) ).

tcf(c_7346,plain,
    ( ( inverse(sk_c2) = inverse(sk_c8) )
    | ( inverse(sk_c2) != inverse(sk_c2) )
    | ( inverse(sk_c8) != inverse(sk_c2) ) ),
    inference(instantiation,[status(thm)],[c_7345]) ).

tcf(c_8127,plain,
    multiply(sk_c2,iPr_def_13) = multiply(iPr_def_20,sk_c8),
    inference(superposition,[status(thm)],[c_362,c_1401]) ).

tcf(c_8326,plain,
    ! [X0: $i] : multiply(sk_c2,multiply(iPr_def_13,X0)) = multiply(iPr_def_20,multiply(sk_c8,X0)),
    inference(superposition,[status(thm)],[c_1402,c_1401]) ).

tcf(c_8425,plain,
    ! [X0: $i] :
      ( ( sk_c7 = inverse(X0) )
      | ( sk_c7 != iPr_def_23 )
      | ( inverse(X0) != iPr_def_23 ) ),
    inference(instantiation,[status(thm)],[c_1179]) ).

tcf(c_8427,plain,
    ( ( sk_c7 = inverse(sk_c8) )
    | ( sk_c7 != iPr_def_23 )
    | ( inverse(sk_c8) != iPr_def_23 ) ),
    inference(instantiation,[status(thm)],[c_8425]) ).

tcf(c_8457,plain,
    ! [X0: $i,X1: $i] :
      ( ( sk_c7 = X0 )
      | ( sk_c7 != X1 )
      | ( X0 != X1 ) ),
    inference(instantiation,[status(thm)],[c_405]) ).

tcf(c_8478,plain,
    ! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(X0,X1)) = X1,
    inference(demodulation,[status(thm)],[c_1404,c_79]) ).

tcf(c_8506,plain,
    multiply(inverse(sk_c3),iPr_def_13) = sk_c8,
    inference(superposition,[status(thm)],[c_362,c_8478]) ).

tcf(c_8507,plain,
    ! [X0: $i] : multiply(inverse(identity),X0) = X0,
    inference(superposition,[status(thm)],[c_79,c_8478]) ).

tcf(c_8508,plain,
    ! [X0: $i] : multiply(inverse(inverse(X0)),identity) = X0,
    inference(superposition,[status(thm)],[c_80,c_8478]) ).

tcf(c_8549,plain,
    multiply(inverse(iPr_def_18),identity) = sk_c4,
    inference(superposition,[status(thm)],[c_814,c_8478]) ).

tcf(c_8597,plain,
    ! [X0: $i] : multiply(inverse(iPr_def_23),X0) = multiply(sk_c8,X0),
    inference(superposition,[status(thm)],[c_1416,c_8478]) ).

tcf(c_8598,plain,
    ! [X0: $i] : multiply(inverse(iPr_def_22),X0) = multiply(sk_c1,X0),
    inference(superposition,[status(thm)],[c_1415,c_8478]) ).

tcf(c_8599,plain,
    ! [X0: $i] : multiply(inverse(iPr_def_18),X0) = multiply(sk_c4,X0),
    inference(superposition,[status(thm)],[c_1414,c_8478]) ).

tcf(c_8600,plain,
    ! [X0: $i] : multiply(inverse(iPr_def_14),X0) = multiply(sk_c5,X0),
    inference(superposition,[status(thm)],[c_1413,c_8478]) ).

tcf(c_8601,plain,
    ! [X0: $i] : multiply(inverse(iPr_def_19),X0) = multiply(sk_c2,X0),
    inference(superposition,[status(thm)],[c_1499,c_8478]) ).

tcf(c_8624,plain,
    ! [X0: $i,X1: $i] : multiply(inverse(inverse(X0)),X1) = multiply(X0,X1),
    inference(superposition,[status(thm)],[c_8478,c_8478]) ).

tcf(c_9166,plain,
    ! [X0: $i] :
      ( ( X0 = inverse(sk_c1) )
      | ( X0 != iPr_def_22 )
      | ( inverse(sk_c1) != iPr_def_22 ) ),
    inference(instantiation,[status(thm)],[c_1178]) ).

tcf(c_9167,plain,
    ( ( sk_c8 = inverse(sk_c1) )
    | ( sk_c8 != iPr_def_22 )
    | ( inverse(sk_c1) != iPr_def_22 ) ),
    inference(instantiation,[status(thm)],[c_9166]) ).

tcf(c_9233,plain,
    ! [X0: $i] : multiply(X0,identity) = X0,
    inference(demodulation,[status(thm)],[c_8508,c_8624]) ).

tcf(c_9258,plain,
    inverse(identity) = identity,
    inference(superposition,[status(thm)],[c_9233,c_8507]) ).

tcf(c_9315,plain,
    multiply(sk_c4,identity) = multiply(iPr_def_17,sk_c8),
    inference(superposition,[status(thm)],[c_812,c_1406]) ).

tcf(c_9722,plain,
    multiply(iPr_def_17,sk_c8) = sk_c4,
    inference(demodulation,[status(thm)],[c_8549,c_8599,c_9315]) ).

tcf(c_9748,plain,
    multiply(inverse(iPr_def_17),sk_c4) = sk_c8,
    inference(superposition,[status(thm)],[c_9722,c_8478]) ).

tcf(c_9909,plain,
    multiply(sk_c1,identity) = multiply(iPr_def_21,sk_c8),
    inference(superposition,[status(thm)],[c_812,c_1407]) ).

tcf(c_10958,plain,
    ( ( sk_c7 = inverse(sk_c5) )
    | ( sk_c7 != sk_c8 )
    | ( inverse(sk_c5) != sk_c8 ) ),
    inference(instantiation,[status(thm)],[c_3263]) ).

tcf(c_10959,plain,
    ! [X0: $i] :
      ( ( X0 = sk_c7 )
      | ( sk_c7 != inverse(sk_c5) )
      | ( X0 != inverse(sk_c5) ) ),
    inference(instantiation,[status(thm)],[c_3192]) ).

tcf(c_11471,plain,
    multiply(iPr_def_21,sk_c8) = sk_c1,
    inference(demodulation,[status(thm)],[c_9909,c_9233]) ).

tcf(c_11497,plain,
    multiply(inverse(iPr_def_21),sk_c1) = sk_c8,
    inference(superposition,[status(thm)],[c_11471,c_8478]) ).

tcf(c_11570,plain,
    ( ( sk_c8 = iPr_def_19 )
    | ( iPr_def_19 != iPr_def_22 )
    | ( sk_c8 != iPr_def_22 ) ),
    inference(instantiation,[status(thm)],[c_1187]) ).

tcf(c_12797,plain,
    multiply(sk_c8,iPr_def_23) = identity,
    inference(superposition,[status(thm)],[c_8597,c_80]) ).

tcf(c_12800,plain,
    ! [X0: $i] : multiply(sk_c8,multiply(iPr_def_23,X0)) = X0,
    inference(superposition,[status(thm)],[c_8597,c_8478]) ).

tcf(c_12808,plain,
    multiply(sk_c8,identity) = inverse(iPr_def_23),
    inference(superposition,[status(thm)],[c_8597,c_9233]) ).

tcf(c_12912,plain,
    ( ( iPr_def_16 = iPr_def_23 )
    | ( multiply(iPr_def_22,iPr_def_23) = identity ) ),
    inference(superposition,[status(thm)],[c_1198,c_12797]) ).

tcf(c_12914,plain,
    ( ( sk_c8 = iPr_def_18 )
    | ( multiply(iPr_def_21,iPr_def_23) = identity ) ),
    inference(superposition,[status(thm)],[c_397,c_12797]) ).

tcf(c_12923,plain,
    ( ( iPr_def_13 = iPr_def_23 )
    | ( multiply(iPr_def_14,iPr_def_23) = identity ) ),
    inference(superposition,[status(thm)],[c_589,c_12797]) ).

tcf(c_12941,plain,
    multiply(sk_c3,identity) = multiply(iPr_def_13,iPr_def_23),
    inference(superposition,[status(thm)],[c_12797,c_1402]) ).

tcf(c_12942,plain,
    multiply(sk_c5,identity) = multiply(iPr_def_15,iPr_def_23),
    inference(superposition,[status(thm)],[c_12797,c_1400]) ).

tcf(c_13200,plain,
    inverse(iPr_def_23) = sk_c8,
    inference(demodulation,[status(thm)],[c_12808,c_9233]) ).

tcf(c_13216,plain,
    ( ( iPr_def_13 = iPr_def_23 )
    | ( inverse(iPr_def_16) = sk_c8 ) ),
    inference(superposition,[status(thm)],[c_603,c_13200]) ).

tcf(c_13218,plain,
    ( ~ iPr_def_11
    | ( multiply(iPr_def_23,sk_c8) != iPr_def_23 )
    | ( multiply(inverse(iPr_def_23),sk_c8) != iPr_def_23 ) ),
    inference(superposition,[status(thm)],[c_13200,c_1947]) ).

tcf(c_13250,plain,
    ( ~ iPr_def_11
    | ( identity != iPr_def_23 )
    | ( multiply(sk_c8,sk_c8) != iPr_def_23 ) ),
    inference(light_normalisation,[status(thm)],[c_13218,c_812,c_13200]) ).

tcf(c_13822,plain,
    ( ( sk_c8 = iPr_def_18 )
    | ( multiply(iPr_def_22,identity) = multiply(iPr_def_23,iPr_def_23) ) ),
    inference(superposition,[status(thm)],[c_12914,c_2609]) ).

tcf(c_14424,plain,
    ( ( iPr_def_13 = iPr_def_23 )
    | ( sk_c8 = iPr_def_23 ) ),
    inference(superposition,[status(thm)],[c_13216,c_4928]) ).

tcf(c_14692,plain,
    multiply(sk_c3,identity) = multiply(iPr_def_19,iPr_def_20),
    inference(superposition,[status(thm)],[c_9233,c_3225]) ).

tcf(c_14701,plain,
    multiply(iPr_def_13,iPr_def_23) = sk_c3,
    inference(light_normalisation,[status(thm)],[c_14692,c_3219,c_12941]) ).

tcf(c_14791,plain,
    multiply(inverse(iPr_def_13),sk_c3) = iPr_def_23,
    inference(superposition,[status(thm)],[c_14701,c_8478]) ).

tcf(c_14903,plain,
    ! [X0: $i] :
      ( ( X0 = sk_c1 )
      | ( sk_c1 != iPr_def_22 )
      | ( X0 != iPr_def_22 ) ),
    inference(instantiation,[status(thm)],[c_2758]) ).

tcf(c_14904,plain,
    ( ( sk_c8 = sk_c1 )
    | ( sk_c1 != iPr_def_22 )
    | ( sk_c8 != iPr_def_22 ) ),
    inference(instantiation,[status(thm)],[c_14903]) ).

tcf(c_14980,plain,
    ( ~ iPr_def_12
    | ( sk_c8 != iPr_def_23 )
    | ( inverse(iPr_def_23) != sk_c8 ) ),
    inference(superposition,[status(thm)],[c_12800,c_1771]) ).

tcf(c_15082,plain,
    ( ~ iPr_def_12
    | ( sk_c8 != iPr_def_23 ) ),
    inference(ground_joinability,[status(thm)],[c_14980,c_13200]) ).

tcf(c_15586,plain,
    ( ( iPr_def_20 = iPr_def_23 )
    | ~ iPr_def_12
    | ( iPr_def_16 != iPr_def_23 ) ),
    inference(superposition,[status(thm)],[c_5613,c_15082]) ).

tcf(c_15605,plain,
    ( ( iPr_def_20 = iPr_def_23 )
    | ~ iPr_def_12
    | ( iPr_def_18 != iPr_def_23 ) ),
    inference(superposition,[status(thm)],[c_823,c_15082]) ).

tcf(c_15678,plain,
    ! [X0: $i,X1: $i] :
      ( ( X1 = inverse(X0) )
      | ( X1 != inverse(sk_c1) )
      | ( inverse(X0) != inverse(sk_c1) ) ),
    inference(instantiation,[status(thm)],[c_1172]) ).

tcf(c_15681,plain,
    ( ( sk_c8 = inverse(sk_c8) )
    | ( sk_c8 != inverse(sk_c1) )
    | ( inverse(sk_c8) != inverse(sk_c1) ) ),
    inference(instantiation,[status(thm)],[c_15678]) ).

tcf(c_15751,plain,
    multiply(iPr_def_15,iPr_def_23) = sk_c5,
    inference(demodulation,[status(thm)],[c_12942,c_9233]) ).

tcf(c_16953,plain,
    ( ( iPr_def_13 = iPr_def_23 )
    | ~ iPr_def_12 ),
    inference(superposition,[status(thm)],[c_14424,c_15082]) ).

tcf(c_17008,plain,
    ( ( iPr_def_18 = iPr_def_23 )
    | ( iPr_def_13 = iPr_def_23 ) ),
    inference(superposition,[status(thm)],[c_14424,c_621]) ).

tcf(c_17010,plain,
    ( ( iPr_def_14 = iPr_def_23 )
    | ( iPr_def_13 = iPr_def_23 ) ),
    inference(superposition,[status(thm)],[c_14424,c_589]) ).

tcf(c_17199,plain,
    ( ( iPr_def_13 = iPr_def_23 )
    | ( multiply(iPr_def_18,iPr_def_17) = identity ) ),
    inference(superposition,[status(thm)],[c_17008,c_873]) ).

tcf(c_17243,plain,
    ( ( iPr_def_13 = iPr_def_23 )
    | ( identity = iPr_def_23 ) ),
    inference(light_normalisation,[status(thm)],[c_17199,c_2572]) ).

tcf(c_17646,plain,
    ( ( iPr_def_13 = iPr_def_23 )
    | ( inverse(iPr_def_14) = sk_c8 ) ),
    inference(superposition,[status(thm)],[c_17010,c_13200]) ).

tcf(c_17938,plain,
    ! [X0: $i] :
      ( ( identity = X0 )
      | ( identity != identity )
      | ( X0 != identity ) ),
    inference(instantiation,[status(thm)],[c_5741]) ).

tcf(c_17939,plain,
    ( ( identity = sk_c8 )
    | ( identity != identity )
    | ( sk_c8 != identity ) ),
    inference(instantiation,[status(thm)],[c_17938]) ).

tcf(c_18242,plain,
    ( ( iPr_def_15 = iPr_def_23 )
    | ( iPr_def_13 = iPr_def_23 ) ),
    inference(superposition,[status(thm)],[c_17243,c_5397]) ).

tcf(c_21501,plain,
    multiply(sk_c1,identity) = inverse(iPr_def_22),
    inference(superposition,[status(thm)],[c_8598,c_9233]) ).

tcf(c_22044,plain,
    ( ( iPr_def_16 = iPr_def_23 )
    | ( iPr_def_13 = iPr_def_23 ) ),
    inference(light_normalisation,[status(thm)],[c_380,c_403]) ).

tcf(c_22051,plain,
    ( ( iPr_def_13 = iPr_def_23 )
    | ( sk_c8 = iPr_def_17 ) ),
    inference(light_normalisation,[status(thm)],[c_381,c_403]) ).

tcf(c_22062,plain,
    ( ( iPr_def_13 = iPr_def_23 )
    | ( sk_c8 = iPr_def_18 ) ),
    inference(light_normalisation,[status(thm)],[c_382,c_403]) ).

tcf(c_22071,plain,
    ( ( iPr_def_17 = iPr_def_18 )
    | ( iPr_def_13 = iPr_def_23 ) ),
    inference(superposition,[status(thm)],[c_22062,c_22051]) ).

tcf(c_22106,plain,
    ( ( iPr_def_16 = iPr_def_23 )
    | ( sk_c3 = iPr_def_19 ) ),
    inference(light_normalisation,[status(thm)],[c_385,c_403]) ).

tcf(c_22130,plain,
    ( ( iPr_def_20 = iPr_def_23 )
    | ( sk_c8 = iPr_def_14 ) ),
    inference(light_normalisation,[status(thm)],[c_388,c_403]) ).

tcf(c_22141,plain,
    ( ( iPr_def_20 = iPr_def_23 )
    | ( sk_c6 = iPr_def_15 ) ),
    inference(light_normalisation,[status(thm)],[c_389,c_403]) ).

tcf(c_22211,plain,
    ( ( iPr_def_16 = iPr_def_23 )
    | ( multiply(iPr_def_19,sk_c8) = iPr_def_13 ) ),
    inference(superposition,[status(thm)],[c_22106,c_362]) ).

tcf(c_22212,plain,
    ( ( sk_c8 = iPr_def_14 )
    | ( multiply(iPr_def_19,sk_c8) = iPr_def_13 ) ),
    inference(superposition,[status(thm)],[c_383,c_362]) ).

tcf(c_22252,plain,
    ( ( iPr_def_20 = iPr_def_23 )
    | ( multiply(iPr_def_14,sk_c6) = iPr_def_16 ) ),
    inference(superposition,[status(thm)],[c_22130,c_365]) ).

tcf(c_22257,plain,
    ( ( sk_c3 = iPr_def_19 )
    | ( multiply(sk_c8,iPr_def_15) = iPr_def_16 ) ),
    inference(superposition,[status(thm)],[c_384,c_365]) ).

tcf(c_22310,plain,
    ( ( iPr_def_20 = iPr_def_23 )
    | ( sk_c8 = iPr_def_18 ) ),
    inference(light_normalisation,[status(thm)],[c_392,c_403]) ).

tcf(c_22327,plain,
    ( ( iPr_def_20 = iPr_def_23 )
    | ( iPr_def_14 = iPr_def_18 ) ),
    inference(superposition,[status(thm)],[c_22310,c_22130]) ).

tcf(c_22532,plain,
    ( ( iPr_def_21 = iPr_def_22 )
    | ( sk_c8 = iPr_def_14 ) ),
    inference(superposition,[status(thm)],[c_398,c_393]) ).

tcf(c_22579,plain,
    ( ( sk_c8 = iPr_def_22 )
    | ( multiply(sk_c8,iPr_def_15) = iPr_def_16 ) ),
    inference(superposition,[status(thm)],[c_399,c_365]) ).

tcf(c_22586,plain,
    multiply(sk_c4,iPr_def_23) = iPr_def_17,
    inference(light_normalisation,[status(thm)],[c_366,c_403]) ).

tcf(c_22602,plain,
    multiply(sk_c1,iPr_def_23) = iPr_def_21,
    inference(light_normalisation,[status(thm)],[c_370,c_403]) ).

tcf(c_22618,plain,
    multiply(iPr_def_23,sk_c8) = identity,
    inference(superposition,[status(thm)],[c_372,c_80]) ).

tcf(c_22619,plain,
    multiply(iPr_def_22,sk_c1) = identity,
    inference(superposition,[status(thm)],[c_371,c_80]) ).

tcf(c_22621,plain,
    multiply(iPr_def_14,sk_c5) = identity,
    inference(superposition,[status(thm)],[c_363,c_80]) ).

tcf(c_22622,plain,
    multiply(iPr_def_19,sk_c2) = identity,
    inference(superposition,[status(thm)],[c_368,c_80]) ).

tcf(c_22716,plain,
    ( ( iPr_def_21 = iPr_def_22 )
    | ( sk_c8 = iPr_def_17 ) ),
    inference(superposition,[status(thm)],[c_401,c_396]) ).

tcf(c_22769,plain,
    ( ( iPr_def_21 = iPr_def_22 )
    | ( sk_c8 = iPr_def_18 ) ),
    inference(superposition,[status(thm)],[c_402,c_397]) ).

tcf(c_22806,plain,
    ! [X0: $i] :
      ( ~ iPr_def_10
      | ( inverse(X0) != sk_c8 )
      | ( multiply(X0,iPr_def_23) != sk_c8 ) ),
    inference(light_normalisation,[status(thm)],[c_377,c_403]) ).

tcf(c_22819,plain,
    ( ~ iPr_def_10
    | ( sk_c8 != iPr_def_21 )
    | ( inverse(sk_c1) != sk_c8 ) ),
    inference(superposition,[status(thm)],[c_22602,c_22806]) ).

tcf(c_22825,plain,
    ( ~ iPr_def_10
    | ( sk_c8 != iPr_def_22 )
    | ( sk_c8 != iPr_def_21 ) ),
    inference(light_normalisation,[status(thm)],[c_22819,c_371]) ).

tcf(c_22859,plain,
    ! [X0: $i] :
      ( ~ iPr_def_12
      | ( inverse(X0) != sk_c8 )
      | ( multiply(sk_c8,multiply(X0,sk_c8)) != iPr_def_23 ) ),
    inference(light_normalisation,[status(thm)],[c_374,c_403]) ).

tcf(c_22883,plain,
    ( ~ iPr_def_12
    | ( inverse(sk_c5) != sk_c8 )
    | ( multiply(sk_c8,iPr_def_15) != iPr_def_23 ) ),
    inference(superposition,[status(thm)],[c_364,c_22859]) ).

tcf(c_22908,plain,
    ( ~ iPr_def_12
    | ( sk_c8 != iPr_def_14 )
    | ( multiply(sk_c8,iPr_def_15) != iPr_def_23 ) ),
    inference(light_normalisation,[status(thm)],[c_22883,c_363]) ).

tcf(c_22976,plain,
    ! [X0: $i] :
      ( ~ iPr_def_11
      | ( multiply(inverse(X0),sk_c8) != iPr_def_23 )
      | ( multiply(X0,inverse(X0)) != iPr_def_23 ) ),
    inference(light_normalisation,[status(thm)],[c_376,c_403]) ).

tcf(c_22987,plain,
    ( ~ iPr_def_11
    | ( multiply(sk_c8,iPr_def_23) != iPr_def_23 )
    | ( multiply(inverse(sk_c8),sk_c8) != iPr_def_23 ) ),
    inference(superposition,[status(thm)],[c_372,c_22976]) ).

tcf(c_23014,plain,
    ( ~ iPr_def_11
    | ( identity != iPr_def_23 )
    | ( multiply(sk_c8,iPr_def_23) != iPr_def_23 ) ),
    inference(light_normalisation,[status(thm)],[c_22987,c_372,c_22618]) ).

tcf(c_23111,plain,
    ( ( iPr_def_21 = iPr_def_22 )
    | ( iPr_def_14 = iPr_def_17 ) ),
    inference(superposition,[status(thm)],[c_22716,c_22532]) ).

tcf(c_23187,plain,
    ( ( iPr_def_21 = iPr_def_22 )
    | ( iPr_def_14 = iPr_def_18 ) ),
    inference(superposition,[status(thm)],[c_22769,c_22532]) ).

tcf(c_23252,plain,
    ! [X0: $i] : multiply(sk_c2,multiply(sk_c3,X0)) = multiply(iPr_def_20,X0),
    inference(superposition,[status(thm)],[c_369,c_81]) ).

tcf(c_23253,plain,
    ! [X0: $i] : multiply(sk_c3,multiply(sk_c8,X0)) = multiply(iPr_def_13,X0),
    inference(superposition,[status(thm)],[c_362,c_81]) ).

tcf(c_23255,plain,
    ! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(X0,X1)) = multiply(identity,X1),
    inference(superposition,[status(thm)],[c_80,c_81]) ).

tcf(c_23297,plain,
    ( ( iPr_def_17 = iPr_def_18 )
    | ( multiply(iPr_def_13,sk_c8) = identity ) ),
    inference(superposition,[status(thm)],[c_22071,c_22618]) ).

tcf(c_23300,plain,
    ( ( iPr_def_13 = iPr_def_23 )
    | ( multiply(iPr_def_16,sk_c8) = identity ) ),
    inference(superposition,[status(thm)],[c_22044,c_22618]) ).

tcf(c_23359,plain,
    ! [X0: $i] : multiply(iPr_def_22,multiply(sk_c1,X0)) = multiply(identity,X0),
    inference(superposition,[status(thm)],[c_22619,c_81]) ).

tcf(c_23360,plain,
    ! [X0: $i] : multiply(iPr_def_22,multiply(sk_c1,X0)) = X0,
    inference(light_normalisation,[status(thm)],[c_23359,c_79]) ).

tcf(c_23402,plain,
    ( ( iPr_def_20 = iPr_def_23 )
    | ( multiply(iPr_def_14,iPr_def_15) = iPr_def_16 ) ),
    inference(superposition,[status(thm)],[c_22141,c_22252]) ).

tcf(c_23587,plain,
    ! [X0: $i] : multiply(iPr_def_14,multiply(sk_c5,X0)) = multiply(identity,X0),
    inference(superposition,[status(thm)],[c_22621,c_81]) ).

tcf(c_23588,plain,
    ! [X0: $i] : multiply(iPr_def_14,multiply(sk_c5,X0)) = X0,
    inference(light_normalisation,[status(thm)],[c_23587,c_79]) ).

tcf(c_23589,plain,
    ! [X0: $i] : multiply(iPr_def_19,multiply(sk_c2,X0)) = multiply(identity,X0),
    inference(superposition,[status(thm)],[c_22622,c_81]) ).

tcf(c_23590,plain,
    ! [X0: $i] : multiply(iPr_def_19,multiply(sk_c2,X0)) = X0,
    inference(light_normalisation,[status(thm)],[c_23589,c_79]) ).

tcf(c_23913,plain,
    ( ( iPr_def_14 = iPr_def_18 )
    | ( multiply(iPr_def_20,sk_c8) = identity ) ),
    inference(superposition,[status(thm)],[c_22327,c_22618]) ).

tcf(c_24479,plain,
    multiply(iPr_def_14,iPr_def_15) = sk_c8,
    inference(superposition,[status(thm)],[c_364,c_23588]) ).

tcf(c_24509,plain,
    multiply(iPr_def_19,iPr_def_20) = sk_c3,
    inference(superposition,[status(thm)],[c_369,c_23590]) ).

tcf(c_24524,plain,
    ! [X0: $i] : multiply(iPr_def_19,multiply(iPr_def_20,X0)) = multiply(sk_c3,X0),
    inference(superposition,[status(thm)],[c_24509,c_81]) ).

tcf(c_25840,plain,
    inverse(iPr_def_22) = sk_c1,
    inference(demodulation,[status(thm)],[c_21501,c_9233]) ).

tcf(c_25842,plain,
    ( ( iPr_def_16 = iPr_def_23 )
    | ( sk_c1 = iPr_def_23 ) ),
    inference(demodulation,[status(thm)],[c_1225,c_25840]) ).

tcf(c_26158,plain,
    multiply(sk_c4,identity) = inverse(iPr_def_18),
    inference(superposition,[status(thm)],[c_8599,c_9233]) ).

tcf(c_26213,plain,
    ( ( iPr_def_20 = iPr_def_23 )
    | ( iPr_def_23 != sk_c7 )
    | ( iPr_def_20 != sk_c7 ) ),
    inference(instantiation,[status(thm)],[c_2471]) ).

tcf(c_26507,plain,
    inverse(iPr_def_18) = sk_c4,
    inference(demodulation,[status(thm)],[c_26158,c_9233]) ).

tcf(c_26510,plain,
    ( ( iPr_def_20 = iPr_def_23 )
    | ( sk_c4 = iPr_def_23 ) ),
    inference(demodulation,[status(thm)],[c_838,c_26507]) ).

tcf(c_27275,plain,
    ( ( iPr_def_16 = iPr_def_23 )
    | ( multiply(iPr_def_22,iPr_def_20) = identity ) ),
    inference(superposition,[status(thm)],[c_746,c_12912]) ).

tcf(c_27346,plain,
    multiply(sk_c2,iPr_def_13) = multiply(iPr_def_20,sk_c8),
    inference(superposition,[status(thm)],[c_362,c_23252]) ).

tcf(c_27949,plain,
    ! [X0: $i] : multiply(sk_c2,multiply(iPr_def_13,X0)) = multiply(iPr_def_20,multiply(sk_c8,X0)),
    inference(superposition,[status(thm)],[c_23253,c_23252]) ).

tcf(c_28863,plain,
    ( ( iPr_def_13 = iPr_def_23 )
    | ( multiply(iPr_def_14,iPr_def_15) = identity ) ),
    inference(superposition,[status(thm)],[c_18242,c_12923]) ).

tcf(c_28884,plain,
    ( ( iPr_def_13 = iPr_def_23 )
    | ~ iPr_def_10
    | ( sk_c8 != identity )
    | ( inverse(iPr_def_14) != sk_c8 ) ),
    inference(superposition,[status(thm)],[c_12923,c_1669]) ).

tcf(c_28887,plain,
    ( ( iPr_def_13 = iPr_def_23 )
    | ( sk_c8 = identity ) ),
    inference(light_normalisation,[status(thm)],[c_28863,c_2567]) ).

tcf(c_29096,plain,
    ! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(X0,X1)) = X1,
    inference(demodulation,[status(thm)],[c_23255,c_79]) ).

tcf(c_29124,plain,
    ! [X0: $i] : multiply(inverse(inverse(X0)),identity) = X0,
    inference(superposition,[status(thm)],[c_80,c_29096]) ).

tcf(c_29126,plain,
    ( ( sk_c8 = iPr_def_14 )
    | ( multiply(inverse(iPr_def_19),iPr_def_13) = sk_c8 ) ),
    inference(superposition,[status(thm)],[c_22212,c_29096]) ).

tcf(c_29213,plain,
    ! [X0: $i] : multiply(inverse(iPr_def_19),X0) = multiply(sk_c2,X0),
    inference(superposition,[status(thm)],[c_23590,c_29096]) ).

tcf(c_29240,plain,
    ! [X0: $i,X1: $i] : multiply(inverse(inverse(X0)),X1) = multiply(X0,X1),
    inference(superposition,[status(thm)],[c_29096,c_29096]) ).

tcf(c_29491,plain,
    multiply(sk_c5,identity) = inverse(iPr_def_14),
    inference(superposition,[status(thm)],[c_8600,c_9233]) ).

tcf(c_29827,plain,
    ! [X0: $i] :
      ( ( sk_c7 = X0 )
      | ( sk_c7 != iPr_def_23 )
      | ( X0 != iPr_def_23 ) ),
    inference(instantiation,[status(thm)],[c_8457]) ).

tcf(c_29828,plain,
    ( ( sk_c7 = sk_c8 )
    | ( sk_c7 != iPr_def_23 )
    | ( sk_c8 != iPr_def_23 ) ),
    inference(instantiation,[status(thm)],[c_29827]) ).

tcf(c_29833,plain,
    ! [X0: $i,X1: $i] :
      ( ( sk_c7 = X0 )
      | ( sk_c7 != inverse(X1) )
      | ( X0 != inverse(X1) ) ),
    inference(instantiation,[status(thm)],[c_8457]) ).

tcf(c_29834,plain,
    ( ( sk_c7 = sk_c8 )
    | ( sk_c7 != inverse(sk_c8) )
    | ( sk_c8 != inverse(sk_c8) ) ),
    inference(instantiation,[status(thm)],[c_29833]) ).

tcf(c_30203,plain,
    inverse(iPr_def_14) = sk_c5,
    inference(demodulation,[status(thm)],[c_29491,c_9233]) ).

tcf(c_30211,plain,
    ( ~ iPr_def_11
    | ( multiply(iPr_def_14,sk_c5) != iPr_def_23 )
    | ( multiply(inverse(iPr_def_14),sk_c8) != iPr_def_23 ) ),
    inference(superposition,[status(thm)],[c_30203,c_1947]) ).

tcf(c_30213,plain,
    ( ~ iPr_def_11
    | ( iPr_def_15 != iPr_def_23 )
    | ( identity != iPr_def_23 ) ),
    inference(light_normalisation,[status(thm)],[c_30211,c_364,c_815,c_30203]) ).

tcf(c_31348,plain,
    iPr_def_13 = iPr_def_23,
    inference(global_subsumption_just,[status(thm)],[c_2669,c_373,c_16953,c_17243,c_17646,c_18242,c_28887,c_28884,c_30213]) ).

tcf(c_31385,plain,
    ( ( iPr_def_13 = iPr_def_20 )
    | ( sk_c4 = iPr_def_13 ) ),
    inference(demodulation,[status(thm)],[c_26510,c_31348]) ).

tcf(c_31395,plain,
    ( ( iPr_def_13 = iPr_def_16 )
    | ( sk_c1 = iPr_def_13 ) ),
    inference(demodulation,[status(thm)],[c_25842,c_31348]) ).

tcf(c_31421,plain,
    ( ( iPr_def_13 = iPr_def_16 )
    | ( multiply(iPr_def_19,iPr_def_21) = iPr_def_13 ) ),
    inference(demodulation,[status(thm)],[c_5579,c_31348]) ).

tcf(c_31433,plain,
    multiply(iPr_def_15,iPr_def_13) = sk_c5,
    inference(demodulation,[status(thm)],[c_15751,c_31348]) ).

tcf(c_31434,plain,
    ( ~ iPr_def_12
    | ( sk_c8 != iPr_def_13 ) ),
    inference(demodulation,[status(thm)],[c_15082,c_31348]) ).

tcf(c_31442,plain,
    ! [X0: $i] : multiply(sk_c8,multiply(iPr_def_13,X0)) = X0,
    inference(demodulation,[status(thm)],[c_12800,c_31348]) ).

tcf(c_31443,plain,
    multiply(inverse(iPr_def_13),sk_c3) = iPr_def_13,
    inference(demodulation,[status(thm)],[c_14791,c_31348]) ).

tcf(c_31444,plain,
    multiply(iPr_def_13,iPr_def_13) = sk_c3,
    inference(demodulation,[status(thm)],[c_14701,c_31348]) ).

tcf(c_31456,plain,
    inverse(iPr_def_13) = sk_c8,
    inference(demodulation,[status(thm)],[c_13200,c_31348]) ).

tcf(c_31457,plain,
    multiply(sk_c8,iPr_def_13) = identity,
    inference(demodulation,[status(thm)],[c_12797,c_31348]) ).

tcf(c_31475,plain,
    ! [X0: $i] :
      ( ( sk_c8 = iPr_def_14 )
      | ( multiply(iPr_def_13,multiply(iPr_def_22,X0)) = X0 ) ),
    inference(demodulation,[status(thm)],[c_2892,c_31348]) ).

tcf(c_31499,plain,
    ( ( iPr_def_13 = iPr_def_16 )
    | ( multiply(sk_c2,iPr_def_19) = iPr_def_20 ) ),
    inference(demodulation,[status(thm)],[c_794,c_31348]) ).

tcf(c_31505,plain,
    ( ( iPr_def_13 = iPr_def_20 )
    | ( sk_c6 = identity ) ),
    inference(demodulation,[status(thm)],[c_5700,c_31348]) ).

tcf(c_31513,plain,
    ( ( iPr_def_13 = iPr_def_20 )
    | ( sk_c8 = iPr_def_16 ) ),
    inference(demodulation,[status(thm)],[c_5613,c_31348]) ).

tcf(c_31538,plain,
    multiply(iPr_def_13,iPr_def_16) = sk_c6,
    inference(demodulation,[status(thm)],[c_2884,c_31348]) ).

tcf(c_31539,plain,
    ! [X0: $i] : multiply(iPr_def_13,multiply(sk_c8,X0)) = X0,
    inference(demodulation,[status(thm)],[c_1416,c_31348]) ).

tcf(c_31543,plain,
    multiply(iPr_def_18,iPr_def_17) = iPr_def_13,
    inference(demodulation,[status(thm)],[c_2572,c_31348]) ).

tcf(c_31544,plain,
    ( ( iPr_def_21 = iPr_def_22 )
    | ( iPr_def_13 = iPr_def_16 ) ),
    inference(demodulation,[status(thm)],[c_1217,c_31348]) ).

tcf(c_31553,plain,
    ( ( iPr_def_13 = iPr_def_16 )
    | ( sk_c8 = iPr_def_22 ) ),
    inference(demodulation,[status(thm)],[c_1198,c_31348]) ).

tcf(c_31554,plain,
    ( ( iPr_def_13 = iPr_def_16 )
    | ( sk_c8 = iPr_def_21 ) ),
    inference(demodulation,[status(thm)],[c_962,c_31348]) ).

tcf(c_31555,plain,
    multiply(iPr_def_13,sk_c8) = identity,
    inference(demodulation,[status(thm)],[c_812,c_31348]) ).

tcf(c_31556,plain,
    ( ( iPr_def_13 = iPr_def_20 )
    | ( sk_c8 = iPr_def_18 ) ),
    inference(demodulation,[status(thm)],[c_823,c_31348]) ).

tcf(c_31557,plain,
    multiply(sk_c1,iPr_def_13) = iPr_def_21,
    inference(demodulation,[status(thm)],[c_804,c_31348]) ).

tcf(c_31558,plain,
    multiply(sk_c4,iPr_def_13) = iPr_def_17,
    inference(demodulation,[status(thm)],[c_785,c_31348]) ).

tcf(c_31559,plain,
    ( ( iPr_def_13 = iPr_def_20 )
    | ( sk_c8 = iPr_def_17 ) ),
    inference(demodulation,[status(thm)],[c_758,c_31348]) ).

tcf(c_31560,plain,
    ( ( iPr_def_13 = iPr_def_20 )
    | ( iPr_def_13 = iPr_def_16 ) ),
    inference(demodulation,[status(thm)],[c_746,c_31348]) ).

tcf(c_31561,plain,
    ( ( iPr_def_13 = iPr_def_20 )
    | ( sk_c6 = iPr_def_15 ) ),
    inference(demodulation,[status(thm)],[c_736,c_31348]) ).

tcf(c_31563,plain,
    ( ( iPr_def_13 = iPr_def_16 )
    | ( sk_c3 = iPr_def_19 ) ),
    inference(demodulation,[status(thm)],[c_689,c_31348]) ).

tcf(c_31564,plain,
    inverse(sk_c8) = iPr_def_13,
    inference(demodulation,[status(thm)],[c_372,c_31348]) ).

tcf(c_31944,plain,
    ! [X0: $i] : multiply(iPr_def_13,multiply(iPr_def_13,X0)) = multiply(sk_c3,X0),
    inference(superposition,[status(thm)],[c_31444,c_81]) ).

tcf(c_32462,plain,
    ( ( iPr_def_13 = iPr_def_20 )
    | ~ iPr_def_12
    | ( iPr_def_13 != iPr_def_16 ) ),
    inference(superposition,[status(thm)],[c_31513,c_31434]) ).

tcf(c_32506,plain,
    multiply(sk_c8,sk_c3) = iPr_def_13,
    inference(light_normalisation,[status(thm)],[c_31443,c_31456]) ).

tcf(c_32526,plain,
    ( ( sk_c8 = iPr_def_14 )
    | ( multiply(iPr_def_21,sk_c3) = iPr_def_13 ) ),
    inference(superposition,[status(thm)],[c_393,c_32506]) ).

tcf(c_32536,plain,
    multiply(sk_c3,iPr_def_13) = multiply(iPr_def_13,sk_c3),
    inference(superposition,[status(thm)],[c_32506,c_1402]) ).

tcf(c_32537,plain,
    multiply(sk_c5,iPr_def_13) = multiply(iPr_def_15,sk_c3),
    inference(superposition,[status(thm)],[c_32506,c_1400]) ).

tcf(c_32757,plain,
    ( ( sk_c8 = iPr_def_14 )
    | ( multiply(iPr_def_21,iPr_def_19) = iPr_def_13 ) ),
    inference(superposition,[status(thm)],[c_383,c_32526]) ).

tcf(c_32991,plain,
    ( ( iPr_def_13 = iPr_def_16 )
    | ( inverse(iPr_def_21) = sk_c1 ) ),
    inference(superposition,[status(thm)],[c_31544,c_25840]) ).

tcf(c_33178,plain,
    ( ( iPr_def_13 = iPr_def_20 )
    | ( multiply(iPr_def_13,iPr_def_13) = iPr_def_17 ) ),
    inference(superposition,[status(thm)],[c_31385,c_31558]) ).

tcf(c_33197,plain,
    ( ( iPr_def_13 = iPr_def_20 )
    | ( sk_c3 = iPr_def_17 ) ),
    inference(light_normalisation,[status(thm)],[c_33178,c_31444]) ).

tcf(c_33276,plain,
    ( ( iPr_def_13 = iPr_def_16 )
    | ( multiply(iPr_def_13,iPr_def_13) = iPr_def_21 ) ),
    inference(superposition,[status(thm)],[c_31395,c_31557]) ).

tcf(c_33295,plain,
    ( ( iPr_def_13 = iPr_def_16 )
    | ( sk_c3 = iPr_def_21 ) ),
    inference(light_normalisation,[status(thm)],[c_33276,c_31444]) ).

tcf(c_33702,plain,
    ! [X0: $i] :
      ( ( sk_c8 = iPr_def_14 )
      | ( multiply(iPr_def_21,multiply(iPr_def_13,X0)) = X0 ) ),
    inference(superposition,[status(thm)],[c_393,c_31442]) ).

tcf(c_33886,plain,
    ( ( sk_c8 = iPr_def_17 )
    | ( multiply(iPr_def_13,iPr_def_19) = multiply(iPr_def_19,iPr_def_13) ) ),
    inference(superposition,[status(thm)],[c_386,c_32536]) ).

tcf(c_34525,plain,
    ( ( iPr_def_19 = iPr_def_21 )
    | ( iPr_def_13 = iPr_def_16 ) ),
    inference(superposition,[status(thm)],[c_33295,c_31563]) ).

tcf(c_36028,plain,
    multiply(sk_c2,iPr_def_19) = identity,
    inference(superposition,[status(thm)],[c_8601,c_80]) ).

tcf(c_36029,plain,
    ! [X0: $i] : multiply(sk_c2,multiply(iPr_def_19,X0)) = X0,
    inference(superposition,[status(thm)],[c_8601,c_8478]) ).

tcf(c_36030,plain,
    multiply(sk_c2,identity) = inverse(iPr_def_19),
    inference(superposition,[status(thm)],[c_8601,c_9233]) ).

tcf(c_36031,plain,
    ( ( identity = iPr_def_20 )
    | ( sk_c8 = iPr_def_14 ) ),
    inference(demodulation,[status(thm)],[c_795,c_36028]) ).

tcf(c_36032,plain,
    ( ( identity = iPr_def_20 )
    | ( sk_c8 = iPr_def_17 ) ),
    inference(demodulation,[status(thm)],[c_793,c_36028]) ).

tcf(c_36033,plain,
    ( ( identity = iPr_def_20 )
    | ( sk_c8 = iPr_def_18 ) ),
    inference(demodulation,[status(thm)],[c_792,c_36028]) ).

tcf(c_36068,plain,
    inverse(iPr_def_19) = sk_c2,
    inference(demodulation,[status(thm)],[c_36030,c_9233]) ).

tcf(c_36343,plain,
    ( ( iPr_def_14 = iPr_def_17 )
    | ( identity = iPr_def_20 ) ),
    inference(superposition,[status(thm)],[c_36032,c_36031]) ).

tcf(c_36814,plain,
    ( ( iPr_def_14 = iPr_def_18 )
    | ( identity = iPr_def_20 ) ),
    inference(superposition,[status(thm)],[c_36033,c_36031]) ).

tcf(c_36834,plain,
    ( ( identity = iPr_def_20 )
    | ( inverse(iPr_def_18) = iPr_def_13 ) ),
    inference(superposition,[status(thm)],[c_36033,c_31564]) ).

tcf(c_36874,plain,
    ( ( identity = iPr_def_20 )
    | ( sk_c4 = iPr_def_13 ) ),
    inference(light_normalisation,[status(thm)],[c_36834,c_26507]) ).

tcf(c_37253,plain,
    ( ( iPr_def_13 = iPr_def_16 )
    | ( multiply(iPr_def_22,iPr_def_20) = identity ) ),
    inference(light_normalisation,[status(thm)],[c_27275,c_31348]) ).

tcf(c_37304,plain,
    ( ( sk_c8 = iPr_def_17 )
    | ( multiply(sk_c2,multiply(iPr_def_13,iPr_def_19)) = iPr_def_13 ) ),
    inference(superposition,[status(thm)],[c_33886,c_36029]) ).

tcf(c_37674,plain,
    ( ( iPr_def_14 = iPr_def_17 )
    | ( inverse(iPr_def_20) = iPr_def_20 ) ),
    inference(superposition,[status(thm)],[c_36343,c_9258]) ).

tcf(c_37675,plain,
    ! [X0: $i] :
      ( ( iPr_def_14 = iPr_def_17 )
      | ( multiply(X0,iPr_def_20) = X0 ) ),
    inference(superposition,[status(thm)],[c_36343,c_9233]) ).

tcf(c_37676,plain,
    ! [X0: $i] :
      ( ( iPr_def_14 = iPr_def_17 )
      | ( multiply(iPr_def_20,X0) = X0 ) ),
    inference(superposition,[status(thm)],[c_36343,c_79]) ).

tcf(c_37690,plain,
    ( ( iPr_def_14 = iPr_def_17 )
    | ( multiply(sk_c8,iPr_def_20) = sk_c8 ) ),
    inference(instantiation,[status(thm)],[c_37675]) ).

tcf(c_38120,plain,
    ! [X0: $i] :
      ( ( iPr_def_14 = iPr_def_18 )
      | ( multiply(iPr_def_20,X0) = X0 ) ),
    inference(superposition,[status(thm)],[c_36814,c_79]) ).

tcf(c_40408,plain,
    ! [X0: $i] :
      ( ( iPr_def_13 = iPr_def_16 )
      | ( multiply(iPr_def_20,multiply(sk_c8,X0)) = X0 ) ),
    inference(light_normalisation,[status(thm)],[c_2882,c_31348]) ).

tcf(c_41091,plain,
    ! [X0: $i] : multiply(X0,identity) = X0,
    inference(demodulation,[status(thm)],[c_29124,c_29240]) ).

tcf(c_41929,plain,
    multiply(iPr_def_13,sk_c8) = identity,
    inference(global_subsumption_just,[status(thm)],[c_23297,c_31555]) ).

tcf(c_41950,plain,
    ! [X0: $i] : multiply(iPr_def_13,multiply(sk_c8,X0)) = multiply(identity,X0),
    inference(superposition,[status(thm)],[c_41929,c_81]) ).

tcf(c_41952,plain,
    ! [X0: $i] : multiply(iPr_def_13,multiply(sk_c8,X0)) = X0,
    inference(light_normalisation,[status(thm)],[c_41950,c_79]) ).

tcf(c_42074,plain,
    iPr_def_13 = iPr_def_23,
    inference(global_subsumption_just,[status(thm)],[c_23300,c_31348]) ).

tcf(c_42151,plain,
    multiply(sk_c4,iPr_def_13) = iPr_def_17,
    inference(demodulation,[status(thm)],[c_22586,c_42074]) ).

tcf(c_42157,plain,
    ( ( iPr_def_13 = iPr_def_16 )
    | ( multiply(iPr_def_19,sk_c8) = iPr_def_13 ) ),
    inference(demodulation,[status(thm)],[c_22211,c_42074]) ).

tcf(c_42158,plain,
    inverse(sk_c8) = iPr_def_13,
    inference(demodulation,[status(thm)],[c_372,c_42074]) ).

tcf(c_44031,plain,
    ( ( iPr_def_20 = iPr_def_23 )
    | ~ iPr_def_12 ),
    inference(global_subsumption_just,[status(thm)],[c_15605,c_390,c_403,c_3193,c_15586,c_26213]) ).

tcf(c_44033,plain,
    ( ( iPr_def_13 = iPr_def_20 )
    | ~ iPr_def_12 ),
    inference(light_normalisation,[status(thm)],[c_44031,c_31348]) ).

tcf(c_44040,plain,
    ( iPr_def_11
    | iPr_def_10
    | ( iPr_def_13 = iPr_def_20 ) ),
    inference(superposition,[status(thm)],[c_373,c_44033]) ).

tcf(c_44055,plain,
    ( iPr_def_11
    | ( iPr_def_13 = iPr_def_20 ) ),
    inference(global_subsumption_just,[status(thm)],[c_44040,c_373,c_1695,c_31560,c_31559,c_31556,c_32462]) ).

tcf(c_44233,plain,
    ( ( iPr_def_13 = iPr_def_16 )
    | ( inverse(iPr_def_19) = sk_c1 ) ),
    inference(superposition,[status(thm)],[c_34525,c_32991]) ).

tcf(c_44244,plain,
    ( ( iPr_def_13 = iPr_def_16 )
    | ( sk_c1 = sk_c2 ) ),
    inference(light_normalisation,[status(thm)],[c_44233,c_36068]) ).

tcf(c_44261,plain,
    ( ( iPr_def_13 = iPr_def_16 )
    | ( inverse(sk_c1) = iPr_def_19 ) ),
    inference(superposition,[status(thm)],[c_44244,c_368]) ).

tcf(c_44262,plain,
    ( ( iPr_def_19 = iPr_def_22 )
    | ( iPr_def_13 = iPr_def_16 ) ),
    inference(light_normalisation,[status(thm)],[c_44261,c_371]) ).

tcf(c_44338,plain,
    ( ( iPr_def_13 = iPr_def_16 )
    | ( multiply(iPr_def_19,iPr_def_20) = identity ) ),
    inference(superposition,[status(thm)],[c_44262,c_37253]) ).

tcf(c_44374,plain,
    ( ( iPr_def_13 = iPr_def_16 )
    | ( sk_c3 = identity ) ),
    inference(light_normalisation,[status(thm)],[c_44338,c_3219]) ).

tcf(c_44421,plain,
    ( ( iPr_def_13 = iPr_def_16 )
    | ( identity = iPr_def_21 ) ),
    inference(superposition,[status(thm)],[c_44374,c_33295]) ).

tcf(c_44429,plain,
    ( ( iPr_def_13 = iPr_def_16 )
    | ( identity = iPr_def_19 ) ),
    inference(superposition,[status(thm)],[c_44374,c_31563]) ).

tcf(c_45117,plain,
    ( ( iPr_def_13 = iPr_def_16 )
    | ( inverse(iPr_def_19) = iPr_def_19 ) ),
    inference(superposition,[status(thm)],[c_44429,c_9258]) ).

tcf(c_45120,plain,
    ( ( iPr_def_13 = iPr_def_16 )
    | ( sk_c2 = iPr_def_19 ) ),
    inference(light_normalisation,[status(thm)],[c_45117,c_36068]) ).

tcf(c_45155,plain,
    ( ( iPr_def_13 = iPr_def_16 )
    | ( sk_c1 = iPr_def_19 ) ),
    inference(superposition,[status(thm)],[c_45120,c_44244]) ).

tcf(c_45166,plain,
    ( ( iPr_def_13 = iPr_def_16 )
    | ( multiply(iPr_def_19,sk_c3) = iPr_def_20 ) ),
    inference(superposition,[status(thm)],[c_45120,c_369]) ).

tcf(c_45291,plain,
    ( ( iPr_def_13 = iPr_def_19 )
    | ( iPr_def_13 = iPr_def_16 ) ),
    inference(superposition,[status(thm)],[c_45155,c_31395]) ).

tcf(c_45474,plain,
    ( ( iPr_def_13 = iPr_def_16 )
    | ( identity = iPr_def_20 ) ),
    inference(light_normalisation,[status(thm)],[c_31499,c_36028]) ).

tcf(c_45487,plain,
    ( ( iPr_def_20 = iPr_def_21 )
    | ( iPr_def_13 = iPr_def_16 ) ),
    inference(superposition,[status(thm)],[c_45474,c_44421]) ).

tcf(c_45493,plain,
    ! [X0: $i] :
      ( ( iPr_def_13 = iPr_def_16 )
      | ( multiply(iPr_def_20,X0) = X0 ) ),
    inference(superposition,[status(thm)],[c_45474,c_79]) ).

tcf(c_45548,plain,
    ( ( iPr_def_13 = iPr_def_16 )
    | ( inverse(iPr_def_13) = sk_c2 ) ),
    inference(superposition,[status(thm)],[c_45291,c_36068]) ).

tcf(c_45578,plain,
    ( ( iPr_def_13 = iPr_def_16 )
    | ( sk_c8 = sk_c2 ) ),
    inference(light_normalisation,[status(thm)],[c_45548,c_31456]) ).

tcf(c_46089,plain,
    ( ( iPr_def_13 = iPr_def_16 )
    | ( multiply(iPr_def_19,iPr_def_20) = iPr_def_13 ) ),
    inference(superposition,[status(thm)],[c_45487,c_31421]) ).

tcf(c_46176,plain,
    ( ( iPr_def_13 = iPr_def_16 )
    | ( sk_c3 = iPr_def_13 ) ),
    inference(light_normalisation,[status(thm)],[c_46089,c_3219]) ).

tcf(c_47460,plain,
    ( ( iPr_def_13 = iPr_def_16 )
    | ( sk_c8 = iPr_def_19 ) ),
    inference(superposition,[status(thm)],[c_45578,c_45120]) ).

tcf(c_47461,plain,
    ( ( iPr_def_13 = iPr_def_16 )
    | ( sk_c8 = sk_c1 ) ),
    inference(superposition,[status(thm)],[c_45578,c_44244]) ).

tcf(c_47783,plain,
    ( ( iPr_def_13 = iPr_def_16 )
    | ( multiply(inverse(iPr_def_13),iPr_def_13) = sk_c8 ) ),
    inference(superposition,[status(thm)],[c_46176,c_8506]) ).

tcf(c_47809,plain,
    ( ( iPr_def_13 = iPr_def_16 )
    | ( sk_c8 = identity ) ),
    inference(light_normalisation,[status(thm)],[c_47783,c_31456,c_31457]) ).

tcf(c_47978,plain,
    ( ( iPr_def_13 = iPr_def_16 )
    | ~ iPr_def_12
    | ( iPr_def_13 != iPr_def_19 ) ),
    inference(superposition,[status(thm)],[c_47460,c_31434]) ).

tcf(c_48096,plain,
    ! [X0: $i] :
      ( ( iPr_def_14 = iPr_def_17 )
      | ( multiply(iPr_def_21,multiply(sk_c1,X0)) = X0 ) ),
    inference(superposition,[status(thm)],[c_23111,c_23360]) ).

tcf(c_48527,plain,
    ! [X0: $i] :
      ( ( iPr_def_14 = iPr_def_18 )
      | ( multiply(iPr_def_21,multiply(sk_c1,X0)) = X0 ) ),
    inference(superposition,[status(thm)],[c_23187,c_23360]) ).

tcf(c_48568,plain,
    ( ( iPr_def_13 = iPr_def_16 )
    | ( sk_c8 = iPr_def_13 ) ),
    inference(superposition,[status(thm)],[c_47461,c_31395]) ).

tcf(c_49315,plain,
    ( ( iPr_def_13 = iPr_def_20 )
    | ( sk_c8 = iPr_def_16 ) ),
    inference(light_normalisation,[status(thm)],[c_23402,c_24479,c_42074]) ).

tcf(c_49369,plain,
    ( ( iPr_def_13 = iPr_def_20 )
    | ( multiply(iPr_def_16,sk_c6) = iPr_def_16 ) ),
    inference(superposition,[status(thm)],[c_49315,c_365]) ).

tcf(c_50553,plain,
    ( ( iPr_def_13 = iPr_def_16 )
    | ~ iPr_def_12 ),
    inference(superposition,[status(thm)],[c_48568,c_31434]) ).

tcf(c_50728,plain,
    ( iPr_def_11
    | iPr_def_10
    | ( iPr_def_13 = iPr_def_16 ) ),
    inference(superposition,[status(thm)],[c_373,c_50553]) ).

tcf(c_50732,plain,
    ( iPr_def_11
    | ( iPr_def_13 = iPr_def_16 ) ),
    inference(global_subsumption_just,[status(thm)],[c_50728,c_373,c_1691,c_31554,c_31553,c_45291,c_47978]) ).

tcf(c_51818,plain,
    ( ( sk_c8 = iPr_def_23 )
    | ( iPr_def_23 != iPr_def_13 )
    | ( sk_c8 != iPr_def_13 ) ),
    inference(instantiation,[status(thm)],[c_1251]) ).

tcf(c_51893,plain,
    ( ( iPr_def_23 = iPr_def_13 )
    | ( iPr_def_23 != iPr_def_23 )
    | ( iPr_def_13 != iPr_def_23 ) ),
    inference(instantiation,[status(thm)],[c_5356]) ).

tcf(c_52627,plain,
    ( ( identity = iPr_def_23 )
    | ( iPr_def_23 != sk_c7 )
    | ( identity != sk_c7 ) ),
    inference(instantiation,[status(thm)],[c_2471]) ).

tcf(c_52659,plain,
    ! [X0: $i,X1: $i] :
      ( ( multiply(X0,X1) = iPr_def_23 )
      | ( iPr_def_23 != sk_c7 )
      | ( multiply(X0,X1) != sk_c7 ) ),
    inference(instantiation,[status(thm)],[c_2471]) ).

tcf(c_52661,plain,
    ( ( multiply(sk_c8,sk_c8) = iPr_def_23 )
    | ( iPr_def_23 != sk_c7 )
    | ( multiply(sk_c8,sk_c8) != sk_c7 ) ),
    inference(instantiation,[status(thm)],[c_52659]) ).

tcf(c_53958,plain,
    ( ( sk_c8 = iPr_def_14 )
    | ( multiply(iPr_def_20,sk_c8) = sk_c8 ) ),
    inference(demodulation,[status(thm)],[c_29126,c_27346,c_29213]) ).

tcf(c_53988,plain,
    ( ( iPr_def_14 = iPr_def_18 )
    | ( sk_c8 = iPr_def_14 )
    | ( sk_c8 = identity ) ),
    inference(superposition,[status(thm)],[c_53958,c_23913]) ).

tcf(c_54242,plain,
    ( ( iPr_def_14 = iPr_def_17 )
    | ( inverse(iPr_def_13) = iPr_def_13 ) ),
    inference(superposition,[status(thm)],[c_1592,c_37674]) ).

tcf(c_54254,plain,
    ( ( iPr_def_14 = iPr_def_17 )
    | ( sk_c8 = iPr_def_13 ) ),
    inference(light_normalisation,[status(thm)],[c_54242,c_31456]) ).

tcf(c_54600,plain,
    ! [X0: $i] :
      ( ( identity = sk_c7 )
      | ( identity != X0 )
      | ( sk_c7 != X0 ) ),
    inference(instantiation,[status(thm)],[c_3192]) ).

tcf(c_54604,plain,
    ( ( identity = sk_c7 )
    | ( identity != sk_c8 )
    | ( sk_c7 != sk_c8 ) ),
    inference(instantiation,[status(thm)],[c_54600]) ).

tcf(c_54636,plain,
    ! [X0: $i,X1: $i,X2: $i] :
      ( ( multiply(X0,X1) = sk_c7 )
      | ( sk_c7 != X2 )
      | ( multiply(X0,X1) != X2 ) ),
    inference(instantiation,[status(thm)],[c_3192]) ).

tcf(c_54638,plain,
    ( ( multiply(sk_c8,sk_c8) = sk_c7 )
    | ( sk_c7 != sk_c8 )
    | ( multiply(sk_c8,sk_c8) != sk_c8 ) ),
    inference(instantiation,[status(thm)],[c_54636]) ).

tcf(c_54777,plain,
    ( ( iPr_def_14 = iPr_def_17 )
    | ~ iPr_def_12 ),
    inference(superposition,[status(thm)],[c_54254,c_31434]) ).

tcf(c_54817,plain,
    ( ( iPr_def_14 = iPr_def_17 )
    | ( iPr_def_13 = iPr_def_21 )
    | ( sk_c8 = iPr_def_17 ) ),
    inference(superposition,[status(thm)],[c_54254,c_396]) ).

tcf(c_54818,plain,
    ( ( iPr_def_14 = iPr_def_17 )
    | ( iPr_def_13 = iPr_def_21 )
    | ( sk_c8 = iPr_def_14 ) ),
    inference(superposition,[status(thm)],[c_54254,c_393]) ).

tcf(c_55091,plain,
    ( iPr_def_11
    | iPr_def_10
    | ( iPr_def_14 = iPr_def_17 ) ),
    inference(superposition,[status(thm)],[c_373,c_54777]) ).

tcf(c_55095,plain,
    ( iPr_def_11
    | ( iPr_def_14 = iPr_def_17 ) ),
    inference(global_subsumption_just,[status(thm)],[c_55091,c_408,c_410,c_373,c_372,c_907,c_1063,c_1666,c_1741,c_16953,c_17243,c_17646,c_18242,c_28887,c_28884,c_30213,c_37690,c_51818,c_51893,c_54254,c_55091]) ).

tcf(c_56713,plain,
    ( ( identity = sk_c7 )
    | ( identity != inverse(sk_c5) )
    | ( sk_c7 != inverse(sk_c5) ) ),
    inference(instantiation,[status(thm)],[c_10959]) ).

tcf(c_57759,plain,
    ( ~ iPr_def_10
    | ( sk_c8 != iPr_def_22 ) ),
    inference(global_subsumption_just,[status(thm)],[c_22825,c_1695,c_1691,c_3737,c_3915]) ).

tcf(c_57761,plain,
    ~ iPr_def_10,
    inference(global_subsumption_just,[status(thm)],[c_57759,c_1695,c_4396,c_4700,c_57759]) ).

tcf(c_60989,plain,
    ( ( iPr_def_14 = iPr_def_17 )
    | ( iPr_def_13 = iPr_def_21 ) ),
    inference(superposition,[status(thm)],[c_54818,c_54817]) ).

tcf(c_63219,plain,
    ( ( iPr_def_14 = iPr_def_17 )
    | ( sk_c8 = identity ) ),
    inference(superposition,[status(thm)],[c_37676,c_1593]) ).

tcf(c_63222,plain,
    ! [X0: $i] :
      ( ( iPr_def_14 = iPr_def_17 )
      | ( multiply(sk_c8,X0) = X0 ) ),
    inference(superposition,[status(thm)],[c_37676,c_2878]) ).

tcf(c_63289,plain,
    ( ( iPr_def_14 = iPr_def_17 )
    | ( multiply(sk_c8,sk_c8) = sk_c8 ) ),
    inference(instantiation,[status(thm)],[c_63222]) ).

tcf(c_64195,plain,
    ( ( iPr_def_14 = iPr_def_18 )
    | ( sk_c8 = identity ) ),
    inference(superposition,[status(thm)],[c_38120,c_2484]) ).

tcf(c_64202,plain,
    ! [X0: $i] :
      ( ( iPr_def_14 = iPr_def_18 )
      | ( multiply(sk_c8,X0) = X0 ) ),
    inference(superposition,[status(thm)],[c_38120,c_2876]) ).

tcf(c_64205,plain,
    ( ( iPr_def_14 = iPr_def_18 )
    | ( sk_c6 = iPr_def_16 ) ),
    inference(superposition,[status(thm)],[c_38120,c_3091]) ).

tcf(c_64264,plain,
    ( ( iPr_def_14 = iPr_def_18 )
    | ( multiply(sk_c8,sk_c8) = sk_c8 ) ),
    inference(instantiation,[status(thm)],[c_64202]) ).

tcf(c_64289,plain,
    iPr_def_14 = iPr_def_17,
    inference(global_subsumption_just,[status(thm)],[c_60989,c_373,c_403,c_1666,c_2602,c_3190,c_3191,c_13250,c_16953,c_17243,c_17646,c_17939,c_18242,c_28887,c_28884,c_29828,c_30213,c_51818,c_51893,c_52627,c_52661,c_54254,c_54604,c_54638,c_55095,c_63219,c_63289]) ).

tcf(c_64379,plain,
    ( ( iPr_def_13 = iPr_def_20 )
    | ( sk_c3 = iPr_def_14 ) ),
    inference(demodulation,[status(thm)],[c_33197,c_64289]) ).

tcf(c_64392,plain,
    multiply(iPr_def_18,iPr_def_14) = iPr_def_13,
    inference(demodulation,[status(thm)],[c_31543,c_64289]) ).

tcf(c_64394,plain,
    multiply(sk_c4,iPr_def_13) = iPr_def_14,
    inference(demodulation,[status(thm)],[c_31558,c_64289]) ).

tcf(c_64421,plain,
    multiply(inverse(iPr_def_14),sk_c4) = sk_c8,
    inference(demodulation,[status(thm)],[c_9748,c_64289]) ).

tcf(c_64430,plain,
    multiply(iPr_def_14,sk_c8) = sk_c4,
    inference(demodulation,[status(thm)],[c_9722,c_64289]) ).

tcf(c_64452,plain,
    multiply(sk_c5,sk_c4) = sk_c8,
    inference(light_normalisation,[status(thm)],[c_64421,c_30203]) ).

tcf(c_65075,plain,
    ( ( iPr_def_13 = iPr_def_16 )
    | ( sk_c8 = iPr_def_18 )
    | ( multiply(iPr_def_19,iPr_def_19) = iPr_def_20 ) ),
    inference(superposition,[status(thm)],[c_387,c_45166]) ).

tcf(c_65133,plain,
    ! [X0: $i] :
      ( ( iPr_def_13 = iPr_def_16 )
      | ( multiply(sk_c8,X0) = X0 ) ),
    inference(superposition,[status(thm)],[c_45493,c_40408]) ).

tcf(c_65168,plain,
    ( ( iPr_def_13 = iPr_def_16 )
    | ( multiply(sk_c8,sk_c8) = sk_c8 ) ),
    inference(instantiation,[status(thm)],[c_65133]) ).

tcf(c_65234,plain,
    ( ( iPr_def_14 = iPr_def_18 )
    | ~ iPr_def_12
    | ( identity != iPr_def_13 ) ),
    inference(superposition,[status(thm)],[c_64195,c_31434]) ).

tcf(c_65241,plain,
    ( ( iPr_def_14 = iPr_def_18 )
    | ( inverse(identity) = iPr_def_13 ) ),
    inference(superposition,[status(thm)],[c_64195,c_31564]) ).

tcf(c_65262,plain,
    ( ( iPr_def_14 = iPr_def_18 )
    | ( identity = iPr_def_22 )
    | ( sk_c8 = iPr_def_18 ) ),
    inference(superposition,[status(thm)],[c_64195,c_402]) ).

tcf(c_65263,plain,
    ( ( iPr_def_14 = iPr_def_18 )
    | ( identity = iPr_def_22 )
    | ( sk_c8 = iPr_def_14 ) ),
    inference(superposition,[status(thm)],[c_64195,c_398]) ).

tcf(c_65269,plain,
    ( ( iPr_def_14 = iPr_def_18 )
    | ( identity = iPr_def_13 ) ),
    inference(light_normalisation,[status(thm)],[c_65241,c_9258]) ).

tcf(c_65665,plain,
    ( ( iPr_def_14 = iPr_def_18 )
    | ( identity = iPr_def_22 ) ),
    inference(superposition,[status(thm)],[c_65263,c_65262]) ).

tcf(c_66966,plain,
    iPr_def_13 = iPr_def_16,
    inference(global_subsumption_just,[status(thm)],[c_65075,c_373,c_403,c_1666,c_2602,c_3190,c_3191,c_13250,c_16953,c_17243,c_17646,c_17939,c_18242,c_28887,c_28884,c_29828,c_30213,c_47809,c_48568,c_50732,c_51818,c_51893,c_52627,c_52661,c_54604,c_54638,c_65168]) ).

tcf(c_66971,plain,
    ( ( iPr_def_14 = iPr_def_18 )
    | ( sk_c6 = iPr_def_13 ) ),
    inference(demodulation,[status(thm)],[c_64205,c_66966]) ).

tcf(c_67057,plain,
    ( ( iPr_def_13 = iPr_def_20 )
    | ( sk_c8 = iPr_def_13 ) ),
    inference(demodulation,[status(thm)],[c_31513,c_66966]) ).

tcf(c_67060,plain,
    multiply(iPr_def_13,iPr_def_13) = sk_c6,
    inference(demodulation,[status(thm)],[c_31538,c_66966]) ).

tcf(c_67088,plain,
    sk_c6 = sk_c3,
    inference(light_normalisation,[status(thm)],[c_67060,c_31444]) ).

tcf(c_67191,plain,
    ( ( iPr_def_13 = iPr_def_20 )
    | ( sk_c3 = identity ) ),
    inference(demodulation,[status(thm)],[c_31505,c_67088]) ).

tcf(c_67192,plain,
    ( ( iPr_def_13 = iPr_def_20 )
    | ( sk_c3 = iPr_def_15 ) ),
    inference(demodulation,[status(thm)],[c_31561,c_67088]) ).

tcf(c_67198,plain,
    ( ( sk_c3 = iPr_def_19 )
    | ( sk_c3 = iPr_def_15 ) ),
    inference(demodulation,[status(thm)],[c_384,c_67088]) ).

tcf(c_67751,plain,
    ( ( sk_c3 = iPr_def_15 )
    | ( multiply(sk_c2,iPr_def_19) = iPr_def_20 ) ),
    inference(superposition,[status(thm)],[c_67198,c_369]) ).

tcf(c_67755,plain,
    ( ( identity = iPr_def_20 )
    | ( sk_c3 = iPr_def_15 ) ),
    inference(light_normalisation,[status(thm)],[c_67751,c_36028]) ).

tcf(c_68153,plain,
    ( ( iPr_def_14 = iPr_def_18 )
    | ( inverse(iPr_def_22) = iPr_def_22 ) ),
    inference(superposition,[status(thm)],[c_65665,c_9258]) ).

tcf(c_68158,plain,
    ( ( iPr_def_14 = iPr_def_18 )
    | ( sk_c1 = iPr_def_22 ) ),
    inference(light_normalisation,[status(thm)],[c_68153,c_25840]) ).

tcf(c_68208,plain,
    ( ( iPr_def_14 = iPr_def_18 )
    | ( sk_c3 = iPr_def_13 ) ),
    inference(light_normalisation,[status(thm)],[c_66971,c_67088]) ).

tcf(c_68268,plain,
    ( ( iPr_def_14 = iPr_def_18 )
    | ( iPr_def_13 = iPr_def_19 )
    | ( sk_c8 = iPr_def_18 ) ),
    inference(superposition,[status(thm)],[c_68208,c_387]) ).

tcf(c_68270,plain,
    ( ( iPr_def_14 = iPr_def_18 )
    | ( iPr_def_13 = iPr_def_19 )
    | ( sk_c8 = iPr_def_14 ) ),
    inference(superposition,[status(thm)],[c_68208,c_383]) ).

tcf(c_68401,plain,
    ( ( iPr_def_14 = iPr_def_18 )
    | ( sk_c8 = iPr_def_18 ) ),
    inference(global_subsumption_just,[status(thm)],[c_68268,c_408,c_410,c_373,c_371,c_372,c_403,c_907,c_1557,c_1558,c_1559,c_1695,c_2602,c_3190,c_3191,c_4396,c_4700,c_8427,c_9167,c_13250,c_14904,c_15681,c_17939,c_29834,c_52627,c_52661,c_54604,c_54638,c_57759,c_64195,c_64264,c_65269,c_65234,c_68158]) ).

tcf(c_68750,plain,
    ( ( iPr_def_14 = iPr_def_18 )
    | ( sk_c8 = iPr_def_14 ) ),
    inference(global_subsumption_just,[status(thm)],[c_68270,c_408,c_410,c_373,c_371,c_372,c_403,c_907,c_1557,c_1558,c_1559,c_2602,c_3190,c_3191,c_4200,c_8427,c_9167,c_13250,c_14904,c_15681,c_17939,c_29834,c_52627,c_52661,c_53988,c_54604,c_54638,c_57761,c_64264,c_65269,c_65234,c_68158]) ).

tcf(c_68771,plain,
    iPr_def_14 = iPr_def_18,
    inference(superposition,[status(thm)],[c_68750,c_68401]) ).

tcf(c_68815,plain,
    multiply(iPr_def_14,iPr_def_14) = iPr_def_13,
    inference(demodulation,[status(thm)],[c_64392,c_68771]) ).

tcf(c_68857,plain,
    inverse(iPr_def_14) = sk_c4,
    inference(demodulation,[status(thm)],[c_26507,c_68771]) ).

tcf(c_68878,plain,
    multiply(iPr_def_14,sk_c4) = identity,
    inference(demodulation,[status(thm)],[c_814,c_68771]) ).

tcf(c_68880,plain,
    inverse(sk_c4) = iPr_def_14,
    inference(demodulation,[status(thm)],[c_367,c_68771]) ).

tcf(c_68881,plain,
    sk_c4 = sk_c5,
    inference(demodulation,[status(thm)],[c_30203,c_68857]) ).

tcf(c_68882,plain,
    multiply(sk_c4,sk_c4) = sk_c8,
    inference(demodulation,[status(thm)],[c_64452,c_68881]) ).

tcf(c_68886,plain,
    multiply(sk_c4,iPr_def_13) = multiply(iPr_def_15,sk_c3),
    inference(demodulation,[status(thm)],[c_32537,c_68881]) ).

tcf(c_68890,plain,
    multiply(iPr_def_15,iPr_def_13) = sk_c4,
    inference(demodulation,[status(thm)],[c_31433,c_68881]) ).

tcf(c_68905,plain,
    multiply(iPr_def_15,sk_c3) = iPr_def_14,
    inference(light_normalisation,[status(thm)],[c_68886,c_64394]) ).

tcf(c_69031,plain,
    ! [X0: $i] : multiply(iPr_def_14,multiply(iPr_def_14,X0)) = multiply(iPr_def_13,X0),
    inference(superposition,[status(thm)],[c_68815,c_81]) ).

tcf(c_69054,plain,
    ( ( identity = iPr_def_20 )
    | ( multiply(iPr_def_13,iPr_def_13) = sk_c8 ) ),
    inference(superposition,[status(thm)],[c_36874,c_68882]) ).

tcf(c_69057,plain,
    ( ( iPr_def_13 = iPr_def_20 )
    | ( multiply(iPr_def_13,iPr_def_13) = sk_c8 ) ),
    inference(superposition,[status(thm)],[c_31385,c_68882]) ).

tcf(c_69059,plain,
    ! [X0: $i] : multiply(sk_c4,multiply(sk_c4,X0)) = multiply(sk_c8,X0),
    inference(superposition,[status(thm)],[c_68882,c_81]) ).

tcf(c_69061,plain,
    ( ( iPr_def_13 = iPr_def_20 )
    | ( sk_c8 = sk_c3 ) ),
    inference(light_normalisation,[status(thm)],[c_69057,c_31444]) ).

tcf(c_69070,plain,
    ( ( identity = iPr_def_20 )
    | ( sk_c8 = sk_c3 ) ),
    inference(light_normalisation,[status(thm)],[c_69054,c_31444]) ).

tcf(c_69189,plain,
    ! [X0: $i] : multiply(iPr_def_15,multiply(sk_c3,X0)) = multiply(iPr_def_14,X0),
    inference(superposition,[status(thm)],[c_68905,c_81]) ).

tcf(c_69789,plain,
    ( ( iPr_def_13 = iPr_def_20 )
    | ( identity = iPr_def_14 ) ),
    inference(superposition,[status(thm)],[c_67191,c_64379]) ).

tcf(c_70044,plain,
    multiply(iPr_def_13,iPr_def_15) = multiply(iPr_def_14,sk_c8),
    inference(superposition,[status(thm)],[c_2567,c_69031]) ).

tcf(c_70053,plain,
    multiply(iPr_def_13,sk_c4) = multiply(iPr_def_14,identity),
    inference(superposition,[status(thm)],[c_68878,c_69031]) ).

tcf(c_70059,plain,
    multiply(iPr_def_13,iPr_def_15) = sk_c4,
    inference(light_normalisation,[status(thm)],[c_70044,c_64430]) ).

tcf(c_70131,plain,
    multiply(iPr_def_14,identity) = multiply(iPr_def_15,sk_c3),
    inference(superposition,[status(thm)],[c_9233,c_69189]) ).

tcf(c_70151,plain,
    multiply(iPr_def_13,sk_c4) = iPr_def_14,
    inference(light_normalisation,[status(thm)],[c_70131,c_68905,c_70053]) ).

tcf(c_70199,plain,
    multiply(sk_c3,iPr_def_15) = multiply(iPr_def_13,sk_c4),
    inference(superposition,[status(thm)],[c_70059,c_31944]) ).

tcf(c_70204,plain,
    multiply(sk_c3,iPr_def_15) = iPr_def_14,
    inference(light_normalisation,[status(thm)],[c_70199,c_70151]) ).

tcf(c_72174,plain,
    ( ( sk_c8 = iPr_def_14 )
    | ( multiply(iPr_def_22,identity) = sk_c3 ) ),
    inference(light_normalisation,[status(thm)],[c_13822,c_31348,c_31444,c_68771]) ).

tcf(c_72175,plain,
    ( ( sk_c3 = iPr_def_22 )
    | ( sk_c8 = iPr_def_14 ) ),
    inference(demodulation,[status(thm)],[c_72174,c_9233]) ).

tcf(c_72227,plain,
    ( ( sk_c8 = iPr_def_14 )
    | ( multiply(iPr_def_22,sk_c8) = iPr_def_13 ) ),
    inference(superposition,[status(thm)],[c_72175,c_362]) ).

tcf(c_72228,plain,
    ( ( iPr_def_19 = iPr_def_22 )
    | ( sk_c8 = iPr_def_14 ) ),
    inference(superposition,[status(thm)],[c_72175,c_383]) ).

tcf(c_72395,plain,
    ( ( iPr_def_19 = iPr_def_22 )
    | ~ iPr_def_12
    | ( iPr_def_13 != iPr_def_14 ) ),
    inference(superposition,[status(thm)],[c_72228,c_31434]) ).

tcf(c_73130,plain,
    ( ( iPr_def_13 = iPr_def_20 )
    | ( sk_c8 = iPr_def_15 ) ),
    inference(superposition,[status(thm)],[c_69061,c_67192]) ).

tcf(c_73131,plain,
    ( ( iPr_def_13 = iPr_def_20 )
    | ( sk_c8 = identity ) ),
    inference(superposition,[status(thm)],[c_69061,c_67191]) ).

tcf(c_74117,plain,
    ( ( identity = iPr_def_20 )
    | ( sk_c8 = iPr_def_15 ) ),
    inference(superposition,[status(thm)],[c_69070,c_67755]) ).

tcf(c_74886,plain,
    ! [X0: $i] :
      ( ( iPr_def_13 = iPr_def_20 )
      | ( multiply(iPr_def_14,X0) = X0 ) ),
    inference(superposition,[status(thm)],[c_69789,c_79]) ).

tcf(c_75048,plain,
    ( ( iPr_def_13 = iPr_def_20 )
    | ( sk_c4 = identity ) ),
    inference(superposition,[status(thm)],[c_74886,c_68878]) ).

tcf(c_75850,plain,
    ( ( sk_c8 = iPr_def_23 )
    | ( iPr_def_23 != iPr_def_19 )
    | ( sk_c8 != iPr_def_19 ) ),
    inference(instantiation,[status(thm)],[c_1251]) ).

tcf(c_76118,plain,
    ( ( sk_c8 = iPr_def_14 )
    | ( multiply(iPr_def_13,iPr_def_13) = sk_c8 ) ),
    inference(superposition,[status(thm)],[c_72227,c_31475]) ).

tcf(c_76137,plain,
    ( ( sk_c8 = iPr_def_14 )
    | ( sk_c8 = sk_c3 ) ),
    inference(light_normalisation,[status(thm)],[c_76118,c_31444]) ).

tcf(c_76219,plain,
    iPr_def_13 = iPr_def_16,
    inference(global_subsumption_just,[status(thm)],[c_42157,c_66966]) ).

tcf(c_76279,plain,
    ( ( sk_c8 = iPr_def_22 )
    | ( multiply(sk_c8,iPr_def_15) = iPr_def_13 ) ),
    inference(demodulation,[status(thm)],[c_22579,c_76219]) ).

tcf(c_76285,plain,
    ( ( sk_c3 = iPr_def_19 )
    | ( multiply(sk_c8,iPr_def_15) = iPr_def_13 ) ),
    inference(demodulation,[status(thm)],[c_22257,c_76219]) ).

tcf(c_77361,plain,
    ( ( iPr_def_13 = iPr_def_20 )
    | ( iPr_def_13 = iPr_def_15 ) ),
    inference(superposition,[status(thm)],[c_73130,c_67057]) ).

tcf(c_77732,plain,
    ( ( identity = iPr_def_20 )
    | ( multiply(iPr_def_15,iPr_def_13) = identity ) ),
    inference(superposition,[status(thm)],[c_74117,c_31457]) ).

tcf(c_77743,plain,
    ( ( identity = iPr_def_20 )
    | ( multiply(sk_c3,iPr_def_15) = iPr_def_13 ) ),
    inference(superposition,[status(thm)],[c_74117,c_362]) ).

tcf(c_77746,plain,
    ( ( iPr_def_13 = iPr_def_14 )
    | ( identity = iPr_def_20 ) ),
    inference(light_normalisation,[status(thm)],[c_77743,c_70204]) ).

tcf(c_77751,plain,
    ( ( identity = iPr_def_20 )
    | ( sk_c4 = identity ) ),
    inference(light_normalisation,[status(thm)],[c_77732,c_68890]) ).

tcf(c_78207,plain,
    ( ( sk_c8 = iPr_def_14 )
    | ( multiply(sk_c2,multiply(iPr_def_13,iPr_def_19)) = iPr_def_13 ) ),
    inference(light_normalisation,[status(thm)],[c_37304,c_64289]) ).

tcf(c_78208,plain,
    ( ( sk_c8 = iPr_def_14 )
    | ( multiply(iPr_def_20,multiply(sk_c8,iPr_def_19)) = iPr_def_13 ) ),
    inference(demodulation,[status(thm)],[c_78207,c_8326]) ).

tcf(c_78236,plain,
    ( ( sk_c8 = iPr_def_14 )
    | ( multiply(iPr_def_20,multiply(iPr_def_21,iPr_def_19)) = iPr_def_13 ) ),
    inference(superposition,[status(thm)],[c_393,c_78208]) ).

tcf(c_78522,plain,
    ! [X0: $i] :
      ( ( iPr_def_13 = iPr_def_20 )
      | ( multiply(identity,multiply(identity,X0)) = multiply(sk_c8,X0) ) ),
    inference(superposition,[status(thm)],[c_75048,c_69059]) ).

tcf(c_78564,plain,
    ! [X0: $i] :
      ( ( iPr_def_13 = iPr_def_20 )
      | ( multiply(sk_c8,X0) = X0 ) ),
    inference(light_normalisation,[status(thm)],[c_78522,c_79]) ).

tcf(c_78571,plain,
    ( ( iPr_def_13 = iPr_def_20 )
    | ( multiply(sk_c8,sk_c8) = sk_c8 ) ),
    inference(instantiation,[status(thm)],[c_78564]) ).

tcf(c_78806,plain,
    ( ( sk_c8 = iPr_def_19 )
    | ( sk_c8 = iPr_def_14 ) ),
    inference(superposition,[status(thm)],[c_76137,c_383]) ).

tcf(c_79001,plain,
    ( ( sk_c8 = iPr_def_14 )
    | ~ iPr_def_12
    | ( iPr_def_13 != iPr_def_19 ) ),
    inference(superposition,[status(thm)],[c_78806,c_31434]) ).

tcf(c_79006,plain,
    ( ( sk_c8 = iPr_def_14 )
    | ( multiply(iPr_def_21,iPr_def_19) = sk_c1 ) ),
    inference(superposition,[status(thm)],[c_78806,c_11471]) ).

tcf(c_79226,plain,
    ( ( sk_c8 = iPr_def_14 )
    | ( multiply(iPr_def_20,sk_c1) = iPr_def_13 ) ),
    inference(superposition,[status(thm)],[c_79006,c_78236]) ).

tcf(c_79332,plain,
    iPr_def_13 = iPr_def_20,
    inference(global_subsumption_just,[status(thm)],[c_77361,c_373,c_403,c_1666,c_2602,c_3190,c_3191,c_13250,c_16953,c_17243,c_17646,c_17939,c_18242,c_28887,c_28884,c_29828,c_30213,c_44055,c_51818,c_51893,c_52627,c_52661,c_54604,c_54638,c_67057,c_73131,c_78571]) ).

tcf(c_79397,plain,
    ( ( identity = iPr_def_13 )
    | ( sk_c8 = iPr_def_14 ) ),
    inference(demodulation,[status(thm)],[c_36031,c_79332]) ).

tcf(c_79402,plain,
    multiply(sk_c2,iPr_def_13) = multiply(iPr_def_13,sk_c8),
    inference(demodulation,[status(thm)],[c_8127,c_79332]) ).

tcf(c_79406,plain,
    multiply(sk_c2,iPr_def_13) = identity,
    inference(light_normalisation,[status(thm)],[c_79402,c_31555]) ).

tcf(c_79516,plain,
    ( ( sk_c8 = iPr_def_14 )
    | ( multiply(iPr_def_13,sk_c1) = iPr_def_13 ) ),
    inference(light_normalisation,[status(thm)],[c_79226,c_79332]) ).

tcf(c_79528,plain,
    ( ( sk_c8 = iPr_def_14 )
    | ( multiply(iPr_def_21,iPr_def_13) = sk_c1 ) ),
    inference(superposition,[status(thm)],[c_79516,c_33702]) ).

tcf(c_79554,plain,
    ( ( sk_c8 = iPr_def_14 )
    | ( multiply(inverse(iPr_def_21),sk_c1) = iPr_def_13 ) ),
    inference(superposition,[status(thm)],[c_79528,c_8478]) ).

tcf(c_79563,plain,
    ( ( sk_c8 = iPr_def_14 )
    | ( sk_c8 = iPr_def_13 ) ),
    inference(light_normalisation,[status(thm)],[c_79554,c_11497]) ).

tcf(c_79580,plain,
    ( ( sk_c8 = iPr_def_14 )
    | ~ iPr_def_12 ),
    inference(global_subsumption_just,[status(thm)],[c_79001,c_31434,c_79563]) ).

tcf(c_79606,plain,
    multiply(iPr_def_19,identity) = iPr_def_13,
    inference(superposition,[status(thm)],[c_79406,c_1499]) ).

tcf(c_79618,plain,
    iPr_def_13 = iPr_def_19,
    inference(demodulation,[status(thm)],[c_79606,c_9233]) ).

tcf(c_79651,plain,
    inverse(iPr_def_13) = sk_c2,
    inference(demodulation,[status(thm)],[c_36068,c_79618]) ).

tcf(c_79656,plain,
    ( ( sk_c8 = iPr_def_14 )
    | ( multiply(iPr_def_21,iPr_def_13) = iPr_def_13 ) ),
    inference(demodulation,[status(thm)],[c_32757,c_79618]) ).

tcf(c_79668,plain,
    sk_c8 = sk_c2,
    inference(light_normalisation,[status(thm)],[c_79651,c_31456]) ).

tcf(c_80111,plain,
    ( ( iPr_def_13 = iPr_def_14 )
    | ( identity = iPr_def_13 ) ),
    inference(light_normalisation,[status(thm)],[c_77746,c_79332]) ).

tcf(c_80120,plain,
    ( ( iPr_def_13 = iPr_def_14 )
    | ( inverse(iPr_def_13) = iPr_def_13 ) ),
    inference(superposition,[status(thm)],[c_80111,c_9258]) ).

tcf(c_80122,plain,
    ! [X0: $i] :
      ( ( iPr_def_13 = iPr_def_14 )
      | ( multiply(iPr_def_13,X0) = X0 ) ),
    inference(superposition,[status(thm)],[c_80111,c_79]) ).

tcf(c_80123,plain,
    ( ( iPr_def_13 = iPr_def_14 )
    | ( sk_c8 = iPr_def_13 ) ),
    inference(light_normalisation,[status(thm)],[c_80120,c_31456]) ).

tcf(c_80135,plain,
    ( ( identity = iPr_def_13 )
    | ( sk_c4 = identity ) ),
    inference(light_normalisation,[status(thm)],[c_77751,c_79332]) ).

tcf(c_80156,plain,
    ! [X0: $i] :
      ( ( identity = iPr_def_13 )
      | ( multiply(identity,multiply(identity,X0)) = multiply(sk_c8,X0) ) ),
    inference(superposition,[status(thm)],[c_80135,c_69059]) ).

tcf(c_80164,plain,
    ( ( identity = iPr_def_13 )
    | ( inverse(identity) = iPr_def_14 ) ),
    inference(superposition,[status(thm)],[c_80135,c_68880]) ).

tcf(c_80169,plain,
    ( ( identity = iPr_def_14 )
    | ( identity = iPr_def_13 ) ),
    inference(light_normalisation,[status(thm)],[c_80164,c_9258]) ).

tcf(c_80202,plain,
    ! [X0: $i] :
      ( ( identity = iPr_def_13 )
      | ( multiply(sk_c8,X0) = X0 ) ),
    inference(light_normalisation,[status(thm)],[c_80156,c_79]) ).

tcf(c_80211,plain,
    ( ( identity = iPr_def_13 )
    | ( multiply(sk_c8,sk_c8) = sk_c8 ) ),
    inference(instantiation,[status(thm)],[c_80202]) ).

tcf(c_80313,plain,
    ( ( iPr_def_13 = iPr_def_14 )
    | ( sk_c8 = identity ) ),
    inference(superposition,[status(thm)],[c_80122,c_31555]) ).

tcf(c_80314,plain,
    ! [X0: $i] :
      ( ( iPr_def_13 = iPr_def_14 )
      | ( multiply(sk_c8,X0) = X0 ) ),
    inference(superposition,[status(thm)],[c_80122,c_31539]) ).

tcf(c_80362,plain,
    ( ( iPr_def_13 = iPr_def_14 )
    | ( multiply(sk_c8,sk_c8) = sk_c8 ) ),
    inference(instantiation,[status(thm)],[c_80314]) ).

tcf(c_83546,plain,
    iPr_def_13 = iPr_def_20,
    inference(global_subsumption_just,[status(thm)],[c_49369,c_373,c_403,c_1666,c_2602,c_3190,c_3191,c_13250,c_16953,c_17243,c_17646,c_17939,c_18242,c_28887,c_28884,c_29828,c_30213,c_44055,c_51818,c_51893,c_52627,c_52661,c_54604,c_54638,c_67057,c_73131,c_78571]) ).

tcf(c_83591,plain,
    ! [X0: $i] : multiply(iPr_def_19,multiply(iPr_def_13,X0)) = multiply(sk_c3,X0),
    inference(demodulation,[status(thm)],[c_24524,c_83546]) ).

tcf(c_83621,plain,
    ! [X0: $i] : multiply(sk_c2,multiply(sk_c3,X0)) = multiply(iPr_def_13,X0),
    inference(demodulation,[status(thm)],[c_23252,c_83546]) ).

tcf(c_83983,plain,
    iPr_def_14 = iPr_def_17,
    inference(global_subsumption_just,[status(thm)],[c_48096,c_64289]) ).

tcf(c_84006,plain,
    multiply(sk_c4,iPr_def_13) = iPr_def_14,
    inference(demodulation,[status(thm)],[c_42151,c_83983]) ).

tcf(c_84029,plain,
    iPr_def_14 = iPr_def_18,
    inference(global_subsumption_just,[status(thm)],[c_48527,c_68771]) ).

tcf(c_84067,plain,
    inverse(sk_c4) = iPr_def_14,
    inference(demodulation,[status(thm)],[c_367,c_84029]) ).

tcf(c_84173,plain,
    ( ~ iPr_def_12
    | ( multiply(sk_c8,iPr_def_15) != iPr_def_23 ) ),
    inference(global_subsumption_just,[status(thm)],[c_22908,c_1824,c_79580]) ).

tcf(c_84175,plain,
    ( ~ iPr_def_12
    | ( multiply(sk_c8,iPr_def_15) != iPr_def_13 ) ),
    inference(light_normalisation,[status(thm)],[c_84173,c_42074]) ).

tcf(c_84184,plain,
    ( ( sk_c8 = iPr_def_22 )
    | ~ iPr_def_12 ),
    inference(superposition,[status(thm)],[c_76279,c_84175]) ).

tcf(c_84186,plain,
    ( ( sk_c8 = iPr_def_14 )
    | ~ iPr_def_12
    | ( multiply(iPr_def_22,iPr_def_15) != iPr_def_13 ) ),
    inference(superposition,[status(thm)],[c_398,c_84175]) ).

tcf(c_84204,plain,
    ( ( multiply(sk_c8,iPr_def_23) != iPr_def_23 )
    | ( identity != iPr_def_23 ) ),
    inference(global_subsumption_just,[status(thm)],[c_23014,c_373,c_368,c_372,c_1493,c_1495,c_1695,c_1983,c_4396,c_4700,c_5788,c_5789,c_7346,c_11570,c_15082,c_31434,c_57759,c_72395,c_75850,c_79668,c_80123,c_84184]) ).

tcf(c_84205,plain,
    ( ( identity != iPr_def_23 )
    | ( multiply(sk_c8,iPr_def_23) != iPr_def_23 ) ),
    inference(renaming,[status(thm)],[c_84204]) ).

tcf(c_84206,plain,
    ( ( identity != iPr_def_13 )
    | ( multiply(sk_c8,iPr_def_13) != iPr_def_13 ) ),
    inference(light_normalisation,[status(thm)],[c_84205,c_42074]) ).

tcf(c_84215,plain,
    ( ( sk_c8 = iPr_def_14 )
    | ( identity != iPr_def_13 )
    | ( multiply(iPr_def_21,iPr_def_13) != iPr_def_13 ) ),
    inference(superposition,[status(thm)],[c_393,c_84206]) ).

tcf(c_84225,plain,
    sk_c8 = iPr_def_14,
    inference(global_subsumption_just,[status(thm)],[c_84186,c_79397,c_79656,c_84215]) ).

tcf(c_84227,plain,
    ( ( identity != iPr_def_13 )
    | ( multiply(iPr_def_14,iPr_def_13) != iPr_def_13 ) ),
    inference(demodulation,[status(thm)],[c_84206,c_84225]) ).

tcf(c_84228,plain,
    ( ~ iPr_def_12
    | ( multiply(iPr_def_14,iPr_def_15) != iPr_def_13 ) ),
    inference(demodulation,[status(thm)],[c_84175,c_84225]) ).

tcf(c_84237,plain,
    ( ( sk_c3 = iPr_def_19 )
    | ( multiply(iPr_def_14,iPr_def_15) = iPr_def_13 ) ),
    inference(demodulation,[status(thm)],[c_76285,c_84225]) ).

tcf(c_84250,plain,
    ! [X0: $i] : multiply(iPr_def_13,multiply(iPr_def_14,X0)) = X0,
    inference(demodulation,[status(thm)],[c_41952,c_84225]) ).

tcf(c_84252,plain,
    inverse(iPr_def_14) = iPr_def_13,
    inference(demodulation,[status(thm)],[c_42158,c_84225]) ).

tcf(c_84255,plain,
    multiply(iPr_def_13,iPr_def_14) = identity,
    inference(demodulation,[status(thm)],[c_41929,c_84225]) ).

tcf(c_84257,plain,
    ! [X0: $i] : multiply(sk_c3,multiply(iPr_def_14,X0)) = multiply(iPr_def_13,X0),
    inference(demodulation,[status(thm)],[c_23253,c_84225]) ).

tcf(c_84259,plain,
    multiply(iPr_def_14,iPr_def_15) = iPr_def_14,
    inference(demodulation,[status(thm)],[c_24479,c_84225]) ).

tcf(c_84317,plain,
    multiply(inverse(iPr_def_14),iPr_def_14) = iPr_def_15,
    inference(superposition,[status(thm)],[c_84259,c_29096]) ).

tcf(c_84319,plain,
    identity = iPr_def_15,
    inference(light_normalisation,[status(thm)],[c_84317,c_84252,c_84255]) ).

tcf(c_84320,plain,
    ! [X0: $i] : multiply(X0,iPr_def_15) = X0,
    inference(demodulation,[status(thm)],[c_41091,c_84319]) ).

tcf(c_84368,plain,
    multiply(iPr_def_13,iPr_def_14) = iPr_def_15,
    inference(light_normalisation,[status(thm)],[c_84255,c_84319]) ).

tcf(c_84387,plain,
    ~ iPr_def_12,
    inference(global_subsumption_just,[status(thm)],[c_84228,c_368,c_372,c_1493,c_1495,c_5788,c_5789,c_7346,c_11570,c_15082,c_31434,c_72395,c_75850,c_79668,c_80123,c_84184]) ).

tcf(c_84412,plain,
    ( ( iPr_def_13 = iPr_def_14 )
    | ( sk_c3 = iPr_def_19 ) ),
    inference(demodulation,[status(thm)],[c_84237,c_84320]) ).

tcf(c_84516,plain,
    ! [X0: $i] : multiply(sk_c3,multiply(iPr_def_14,X0)) = multiply(iPr_def_19,X0),
    inference(superposition,[status(thm)],[c_84250,c_83591]) ).

tcf(c_84521,plain,
    ! [X0: $i] : multiply(iPr_def_13,X0) = multiply(iPr_def_19,X0),
    inference(light_normalisation,[status(thm)],[c_84516,c_84257]) ).

tcf(c_84547,plain,
    ! [X0: $i] :
      ( ( iPr_def_13 = iPr_def_14 )
      | ( multiply(sk_c2,multiply(iPr_def_19,X0)) = multiply(iPr_def_13,X0) ) ),
    inference(superposition,[status(thm)],[c_84412,c_83621]) ).

tcf(c_84553,plain,
    ! [X0: $i] :
      ( ( iPr_def_13 = iPr_def_14 )
      | ( multiply(iPr_def_13,X0) = X0 ) ),
    inference(light_normalisation,[status(thm)],[c_84547,c_27949,c_83546,c_84225,c_84250,c_84521]) ).

tcf(c_84663,plain,
    iPr_def_13 = iPr_def_14,
    inference(global_subsumption_just,[status(thm)],[c_84553,c_373,c_403,c_1666,c_2602,c_3190,c_3191,c_13250,c_16953,c_17243,c_17646,c_17939,c_18242,c_28887,c_28884,c_29828,c_30213,c_51818,c_51893,c_52627,c_52661,c_54604,c_54638,c_57761,c_80123,c_80313,c_80362,c_84387]) ).

tcf(c_84671,plain,
    multiply(iPr_def_13,iPr_def_13) = iPr_def_15,
    inference(demodulation,[status(thm)],[c_84368,c_84663]) ).

tcf(c_84676,plain,
    sk_c8 = iPr_def_13,
    inference(demodulation,[status(thm)],[c_84225,c_84663]) ).

tcf(c_84874,plain,
    multiply(iPr_def_14,iPr_def_13) != iPr_def_13,
    inference(global_subsumption_just,[status(thm)],[c_84227,c_373,c_363,c_368,c_372,c_403,c_1395,c_1396,c_1493,c_1495,c_1666,c_1695,c_1919,c_3190,c_3191,c_4396,c_4700,c_5743,c_5788,c_5789,c_7346,c_10958,c_11570,c_13250,c_15082,c_16953,c_17243,c_17646,c_18242,c_28887,c_28884,c_29828,c_30213,c_31434,c_51818,c_51893,c_52627,c_52661,c_54638,c_56713,c_57759,c_72395,c_75850,c_79397,c_79668,c_79656,c_80123,c_80169,c_80211,c_84184,c_84215,c_84227,c_84676]) ).

tcf(c_84876,plain,
    iPr_def_13 != iPr_def_15,
    inference(light_normalisation,[status(thm)],[c_84874,c_84663,c_84671]) ).

tcf(c_85317,plain,
    inverse(sk_c4) = iPr_def_13,
    inference(light_normalisation,[status(thm)],[c_84067,c_84663]) ).

tcf(c_85340,plain,
    multiply(sk_c4,iPr_def_13) = iPr_def_13,
    inference(light_normalisation,[status(thm)],[c_84006,c_84663]) ).

tcf(c_85344,plain,
    multiply(inverse(sk_c4),iPr_def_13) = iPr_def_13,
    inference(superposition,[status(thm)],[c_85340,c_29096]) ).

tcf(c_85346,plain,
    iPr_def_13 = iPr_def_15,
    inference(light_normalisation,[status(thm)],[c_85344,c_84671,c_85317]) ).

tcf(c_85347,plain,
    $false,
    inference(forward_subsumption_resolution,[status(thm)],[c_85346,c_84876]) ).


%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02  % Problem  : GRP236-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.04  % Command  : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.08/10.37  % Computer : n019.cluster.edu
% 0.08/10.37  % Model    : x86_64 x86_64
% 0.08/10.37  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/10.37  % Memory   : 8046.5625MB
% 0.08/10.37  % OS       : Linux 6.8.0-71-generic
% 0.08/10.37  % CPULimit : 300
% 0.08/10.37  % WCLimit  : 300
% 0.08/10.37  % DateTime : Wed Sep 23 14:13:30 UTC 2026
% 0.08/10.38  % CPUTime  : 
% 0.08/10.38  Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.13/10.41  Running first-order theorem proving
% 0.13/10.41  Running: /export/starexec/sandbox/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.13/10.42  
% 0.13/10.42  % ======== iProver multi-core TPTP/SMT =========
% 0.13/10.42  
% 0.13/10.43  % Detected problem language: tptp
% 0.13/10.44  % Proving...
% 14.84/12.83  % SZS status Started for theBenchmark.p
% 14.84/12.83  % SZS status Unsatisfiable for theBenchmark.p
% 14.84/12.83  
% 14.84/12.83  %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 14.84/12.83  
% 14.84/12.83  % ------  iProver source info
% 14.84/12.83  
% 14.84/12.83  % git: date: 2026-07-19 20:42:38 +0200
% 14.84/12.83  % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 14.84/12.83  % git: non_committed_changes: false
% 14.84/12.83  
% 14.84/12.83  % ------ Parsing...% successful
% 14.84/12.83  
% 14.84/12.83  
% 14.84/12.83  % ------ Clausification by vclausify_rel  & Parsing by iProver...% 
% 14.84/12.83  
% 14.84/12.83  % ------ Preprocessing... sup_sim: 0  sf_s  rm: 0 0s  sf_e  pe_s  pe_e % 
% 14.84/12.83  
% 14.84/12.83  % ------ Preprocessing... gs_s  sp: 4 0s  gs_e  snvd_s sp: 0 0s snvd_e % 
% 14.84/12.83  
% 14.84/12.83  % ------ Preprocessing... sf_s  rm: 0 0s  sf_e 
% 14.84/12.83  % ------ Proving...
% 14.84/12.83  % ------ Problem Properties 
% 14.84/12.83  
% 14.84/12.83  % 
% 14.84/12.83  % clauses                               44
% 14.84/12.83  % conjectures                           30
% 14.84/12.83  % EPR                                   27
% 14.84/12.83  % Horn                                  18
% 14.84/12.83  % unary                                 15
% 14.84/12.83  % binary                                25
% 14.84/12.83  % lits                                  77
% 14.84/12.83  % lits eq                               71
% 14.84/12.83  % fd_pure                               0
% 14.84/12.83  % fd_pseudo                             0
% 14.84/12.83  % fd_cond                               0
% 14.84/12.83  % fd_pseudo_cond                        0
% 14.84/12.83  % AC symbols                            0
% 14.84/12.83  
% 14.84/12.83  % ------ Schedule dynamic 5 is on 
% 14.84/12.83  
% 14.84/12.83  % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 14.84/12.83  
% 14.84/12.83  
% 14.84/12.83  % ------ 
% 14.84/12.83  % Current options:
% 14.84/12.83  % ------ 
% 14.84/12.83  
% 14.84/12.83  
% 14.84/12.83  % 
% 14.84/12.83  
% 14.84/12.83  % ------ Proving...
% 14.84/12.83  % 
% 14.84/12.83  
% 14.84/12.83  % SZS status Unsatisfiable for theBenchmark.p
% 14.84/12.83  
% 14.84/12.83  % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 14.84/12.85  
% 14.84/12.85  
%------------------------------------------------------------------------------