iProver---3.9.4.UNS-CRf.s

View TPTP
Problem Process solution in
SystemOnTSTP Download .tgz
%------------------------------------------------------------------------------
% File     : iProver---3.9.4
% Problem  : GRP426-1 : TPTP v9.3.1. Released v2.6.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM

% Computer : n026.cluster.edu
% Model    : x86_64 x86_64
% CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory   : 8046.5625MB
% OS       : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit  : 300s
% DateTime : Fri Sep 25 01:33:53 PM UTC 2026

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

% Comments : 
%------------------------------------------------------------------------------
fof(f1,axiom,
    ! [X2,X0,X1] : multiply(inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),X2)))),multiply(X0,inverse(X2)))),inverse(multiply(inverse(X2),X2))) = X1,
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',single_axiom) ).

fof(f2,negated_conjecture,
    multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3)),
    file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_these_axioms_3) ).

tcf(c_51,plain,
    ! [X0: $i,X1: $i,X2: $i] : multiply(inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),X2)))),multiply(X0,inverse(X2)))),inverse(multiply(inverse(X2),X2))) = X1,
    inference(cnf_transformation,[],[f1]) ).

tcf(c_52,negated_conjecture,
    multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3)),
    inference(cnf_transformation,[],[f2]) ).

tcf(c_62,definition,
    iPr_def_10 = multiply(a3,b3),
    introduced(definition,[new_symbols(definition,[iPr_def_10])],[]) ).

tcf(c_63,definition,
    iPr_def_11 = multiply(iPr_def_10,c3),
    introduced(definition,[new_symbols(definition,[iPr_def_11])],[]) ).

tcf(c_64,definition,
    iPr_def_12 = multiply(b3,c3),
    introduced(definition,[new_symbols(definition,[iPr_def_12])],[]) ).

tcf(c_65,definition,
    iPr_def_13 = multiply(a3,iPr_def_12),
    introduced(definition,[new_symbols(definition,[iPr_def_13])],[]) ).

tcf(c_66,negated_conjecture,
    iPr_def_11 != iPr_def_13,
    inference(demodulation,[status(thm)],[c_52,c_64,c_65,c_62,c_63]) ).

tcf(c_67,plain,
    ! [X0: $i,X1: $i,X2: $i] : multiply(inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),X2)))),multiply(X0,inverse(X2)))),inverse(multiply(inverse(X2),X2))) = X1,
    inference(demodulation,[status(thm)],[c_51]) ).

tcf(c_108,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i] : multiply(inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(inverse(multiply(inverse(X2),X2)))))),inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2))))) = multiply(inverse(multiply(X3,inverse(multiply(inverse(X1),X2)))),multiply(X3,inverse(X2))),
    inference(superposition,[status(thm)],[c_67,c_67]) ).

tcf(c_111,plain,
    ! [X0: $i,X1: $i,X2: $i] : multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),X2)))),multiply(X0,inverse(X2))) = iPr_def_14(X1,X2),
    inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_14])],[c_108]) ).

tcf(c_112,plain,
    ! [X0: $i,X1: $i,X2: $i] : multiply(inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(inverse(multiply(inverse(X2),X2)))))),inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2))))) = iPr_def_14(X1,X2),
    inference(splitting,[splitting(split),new_symbols(definition,[])],[c_108]) ).

tcf(c_113,plain,
    ! [X0: $i,X1: $i] : multiply(inverse(iPr_def_14(X0,X1)),inverse(multiply(inverse(X1),X1))) = X0,
    inference(demodulation,[status(thm)],[c_67,c_111]) ).

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

tcf(c_119,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i] : multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),X2)))),multiply(X0,inverse(X2)))),inverse(multiply(inverse(X3),multiply(inverse(X2),X2))))),X1)),inverse(multiply(inverse(multiply(inverse(X2),X2)),multiply(inverse(X2),X2)))) = X3,
    inference(superposition,[status(thm)],[c_67,c_67]) ).

tcf(c_121,plain,
    ! [X0: $i,X1: $i] : multiply(inverse(iPr_def_14(X0,X1)),inverse(multiply(inverse(X1),X1))) = X0,
    inference(demodulation,[status(thm)],[c_67,c_111]) ).

tcf(c_126,plain,
    ! [X0: $i,X1: $i,X2: $i] : multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(inverse(multiply(inverse(X2),X2))))) = iPr_def_14(iPr_def_14(X1,X2),inverse(multiply(inverse(X2),X2))),
    inference(superposition,[status(thm)],[c_113,c_111]) ).

tcf(c_129,plain,
    ! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(inverse(iPr_def_14(X0,X1)),inverse(X1))) = iPr_def_14(X1,X1),
    inference(superposition,[status(thm)],[c_121,c_111]) ).

tcf(c_131,plain,
    ! [X0: $i,X1: $i,X2: $i] : multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(inverse(multiply(inverse(X2),X2))))) = iPr_def_14(iPr_def_14(X1,X2),inverse(multiply(inverse(X2),X2))),
    inference(superposition,[status(thm)],[c_121,c_111]) ).

tcf(c_132,plain,
    ! [X0: $i,X1: $i,X2: $i] : multiply(inverse(multiply(inverse(iPr_def_14(X0,X1)),inverse(multiply(inverse(X2),multiply(inverse(X1),X1))))),X0) = iPr_def_14(X2,multiply(inverse(X1),X1)),
    inference(superposition,[status(thm)],[c_121,c_111]) ).

tcf(c_148,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i] : multiply(inverse(multiply(inverse(multiply(inverse(iPr_def_14(inverse(X0),X1)),inverse(multiply(inverse(X2),multiply(inverse(X1),X1))))),inverse(multiply(inverse(X3),X0)))),iPr_def_14(X2,multiply(inverse(X1),X1))) = iPr_def_14(X3,X0),
    inference(superposition,[status(thm)],[c_132,c_111]) ).

tcf(c_170,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i] : multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(inverse(multiply(inverse(X2),X2))))) = multiply(inverse(multiply(X3,inverse(X1))),multiply(X3,inverse(inverse(multiply(inverse(X2),X2))))),
    inference(superposition,[status(thm)],[c_126,c_126]) ).

tcf(c_171,plain,
    ! [X0: $i,X1: $i,X2: $i] : multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(inverse(multiply(inverse(X2),X2))))) = iPr_def_15(X1,X2),
    inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_15])],[c_170]) ).

tcf(c_178,plain,
    ! [X0: $i,X1: $i,X2: $i] : multiply(inverse(X0),multiply(inverse(iPr_def_14(X0,X1)),inverse(inverse(multiply(inverse(X2),X2))))) = iPr_def_14(iPr_def_14(multiply(inverse(X1),X1),X2),inverse(multiply(inverse(X2),X2))),
    inference(superposition,[status(thm)],[c_121,c_131]) ).

tcf(c_190,plain,
    ! [X0: $i,X1: $i,X2: $i] : multiply(inverse(iPr_def_14(X0,multiply(X1,inverse(inverse(multiply(inverse(X2),X2)))))),inverse(iPr_def_14(iPr_def_14(inverse(multiply(inverse(X2),X2)),X2),inverse(multiply(inverse(X2),X2))))) = X0,
    inference(superposition,[status(thm)],[c_131,c_121]) ).

tcf(c_201,plain,
    ! [X0: $i,X1: $i] : iPr_def_14(iPr_def_14(X0,X1),inverse(multiply(inverse(X1),X1))) = iPr_def_15(X0,X1),
    inference(demodulation,[status(thm)],[c_131,c_171]) ).

tcf(c_210,plain,
    ! [X0: $i,X1: $i,X2: $i] : multiply(inverse(X0),multiply(inverse(iPr_def_14(X0,X1)),inverse(inverse(multiply(inverse(X2),X2))))) = iPr_def_15(multiply(inverse(X1),X1),X2),
    inference(superposition,[status(thm)],[c_113,c_171]) ).

tcf(c_225,plain,
    ! [X0: $i,X1: $i] : multiply(inverse(iPr_def_15(X0,X1)),inverse(multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(multiply(inverse(X1),X1))))) = iPr_def_14(X0,X1),
    inference(superposition,[status(thm)],[c_201,c_121]) ).

tcf(c_227,plain,
    ! [X0: $i,X1: $i,X2: $i] : multiply(inverse(X0),multiply(inverse(iPr_def_14(X0,X1)),inverse(inverse(multiply(inverse(X2),X2))))) = iPr_def_15(multiply(inverse(X1),X1),X2),
    inference(superposition,[status(thm)],[c_121,c_171]) ).

tcf(c_232,plain,
    ! [X0: $i,X1: $i] : iPr_def_15(multiply(inverse(X0),inverse(multiply(inverse(X1),X1))),X1) = iPr_def_14(X0,inverse(multiply(inverse(X1),X1))),
    inference(superposition,[status(thm)],[c_171,c_111]) ).

tcf(c_236,plain,
    ! [X0: $i,X1: $i,X2: $i] : multiply(inverse(iPr_def_14(X0,multiply(X1,inverse(inverse(multiply(inverse(X2),X2)))))),inverse(iPr_def_15(inverse(multiply(inverse(X2),X2)),X2))) = X0,
    inference(superposition,[status(thm)],[c_171,c_121]) ).

tcf(c_252,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i] : multiply(inverse(X0),multiply(inverse(iPr_def_14(X0,X1)),inverse(inverse(multiply(inverse(X2),X2))))) = multiply(inverse(X3),multiply(inverse(iPr_def_14(X3,X1)),inverse(inverse(multiply(inverse(X2),X2))))),
    inference(superposition,[status(thm)],[c_210,c_210]) ).

tcf(c_253,plain,
    ! [X0: $i,X1: $i,X2: $i] : multiply(inverse(X0),multiply(inverse(iPr_def_14(X0,X1)),inverse(inverse(multiply(inverse(X2),X2))))) = iPr_def_16(X1,X2),
    inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_16])],[c_252]) ).

tcf(c_266,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i] : multiply(inverse(X0),multiply(inverse(iPr_def_14(X0,multiply(X1,inverse(inverse(multiply(inverse(X2),X2)))))),inverse(inverse(multiply(inverse(X3),X3))))) = iPr_def_15(iPr_def_15(inverse(multiply(inverse(X2),X2)),X2),X3),
    inference(superposition,[status(thm)],[c_171,c_227]) ).

tcf(c_267,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i] : multiply(inverse(multiply(X0,inverse(iPr_def_15(multiply(inverse(X1),X1),X2)))),multiply(X0,inverse(multiply(inverse(iPr_def_14(X3,X1)),inverse(inverse(multiply(inverse(X2),X2))))))) = iPr_def_14(X3,multiply(inverse(iPr_def_14(X3,X1)),inverse(inverse(multiply(inverse(X2),X2))))),
    inference(superposition,[status(thm)],[c_227,c_111]) ).

tcf(c_273,plain,
    ! [X0: $i,X1: $i,X2: $i] : iPr_def_16(multiply(X0,inverse(inverse(multiply(inverse(X1),X1)))),X2) = iPr_def_15(iPr_def_15(inverse(multiply(inverse(X1),X1)),X1),X2),
    inference(demodulation,[status(thm)],[c_266,c_253]) ).

tcf(c_274,plain,
    ! [X0: $i,X1: $i] : iPr_def_15(multiply(inverse(X0),X0),X1) = iPr_def_16(X0,X1),
    inference(demodulation,[status(thm)],[c_227,c_253]) ).

tcf(c_299,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i] : multiply(inverse(multiply(X0,inverse(iPr_def_16(X1,X2)))),multiply(X0,inverse(multiply(inverse(iPr_def_14(X3,X1)),inverse(inverse(multiply(inverse(X2),X2))))))) = iPr_def_14(X3,multiply(inverse(iPr_def_14(X3,X1)),inverse(inverse(multiply(inverse(X2),X2))))),
    inference(superposition,[status(thm)],[c_253,c_111]) ).

tcf(c_323,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i] : iPr_def_15(iPr_def_15(inverse(multiply(inverse(X0),X0)),X0),X1) = iPr_def_16(iPr_def_14(X2,multiply(inverse(X3),X3)),X1),
    inference(superposition,[status(thm)],[c_132,c_273]) ).

tcf(c_333,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] : iPr_def_16(multiply(X0,inverse(inverse(multiply(inverse(X1),X1)))),X2) = iPr_def_16(iPr_def_14(X3,multiply(inverse(X4),X4)),X2),
    inference(superposition,[status(thm)],[c_323,c_273]) ).

tcf(c_335,plain,
    ! [X0: $i,X1: $i,X2: $i] : iPr_def_15(iPr_def_15(inverse(multiply(inverse(X0),X0)),X0),X1) = iPr_def_15(iPr_def_15(inverse(multiply(inverse(X2),X2)),X2),X1),
    inference(superposition,[status(thm)],[c_323,c_323]) ).

tcf(c_411,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i] : iPr_def_16(multiply(X0,inverse(inverse(multiply(inverse(X1),X1)))),X2) = iPr_def_15(iPr_def_15(inverse(multiply(inverse(X3),X3)),X3),X2),
    inference(superposition,[status(thm)],[c_333,c_323]) ).

tcf(c_466,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i] : multiply(inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(inverse(multiply(inverse(X2),X2)))))),inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2))))) = multiply(inverse(multiply(X3,inverse(multiply(inverse(X1),X2)))),multiply(X3,inverse(X2))),
    inference(superposition,[status(thm)],[c_67,c_67]) ).

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

tcf(c_468,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i] : multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),X2)))),multiply(X0,inverse(X2)))),inverse(multiply(inverse(X3),multiply(inverse(X2),X2))))),X1)),inverse(multiply(inverse(multiply(inverse(X2),X2)),multiply(inverse(X2),X2)))) = X3,
    inference(superposition,[status(thm)],[c_67,c_67]) ).

tcf(c_469,plain,
    ! [X0: $i,X1: $i,X2: $i] : multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),X2)))),multiply(X0,inverse(X2))) = iPr_def_14(X1,X2),
    inference(demodulation,[status(thm)],[c_466,c_112]) ).

tcf(c_470,plain,
    ! [X0: $i,X1: $i] : multiply(inverse(iPr_def_14(X0,X1)),inverse(multiply(inverse(X1),X1))) = X0,
    inference(demodulation,[status(thm)],[c_67,c_469]) ).

tcf(c_471,plain,
    ! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(inverse(iPr_def_14(X0,X1)),inverse(X1))) = iPr_def_14(X1,X1),
    inference(superposition,[status(thm)],[c_470,c_469]) ).

tcf(c_473,plain,
    ! [X0: $i,X1: $i,X2: $i] : multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(inverse(multiply(inverse(X2),X2))))) = iPr_def_14(iPr_def_14(X1,X2),inverse(multiply(inverse(X2),X2))),
    inference(superposition,[status(thm)],[c_470,c_469]) ).

tcf(c_474,plain,
    ! [X0: $i,X1: $i,X2: $i] : multiply(inverse(multiply(inverse(iPr_def_14(X0,X1)),inverse(multiply(inverse(X2),multiply(inverse(X1),X1))))),X0) = iPr_def_14(X2,multiply(inverse(X1),X1)),
    inference(superposition,[status(thm)],[c_470,c_469]) ).

tcf(c_491,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i] : multiply(inverse(multiply(X0,inverse(iPr_def_14(iPr_def_14(X1,X2),inverse(multiply(inverse(X2),X2)))))),multiply(X0,inverse(multiply(X3,inverse(inverse(multiply(inverse(X2),X2))))))) = iPr_def_14(multiply(X3,inverse(X1)),multiply(X3,inverse(inverse(multiply(inverse(X2),X2))))),
    inference(superposition,[status(thm)],[c_473,c_469]) ).

tcf(c_508,plain,
    ! [X0: $i,X1: $i] : iPr_def_14(iPr_def_14(X0,X1),inverse(multiply(inverse(X1),X1))) = iPr_def_15(X0,X1),
    inference(demodulation,[status(thm)],[c_473,c_171]) ).

tcf(c_513,plain,
    ! [X0: $i,X1: $i] : multiply(inverse(iPr_def_15(X0,X1)),inverse(multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(multiply(inverse(X1),X1))))) = iPr_def_14(X0,X1),
    inference(superposition,[status(thm)],[c_508,c_470]) ).

tcf(c_515,plain,
    ! [X0: $i,X1: $i,X2: $i] : multiply(inverse(X0),multiply(inverse(iPr_def_14(X0,X1)),inverse(inverse(multiply(inverse(X2),X2))))) = iPr_def_15(multiply(inverse(X1),X1),X2),
    inference(superposition,[status(thm)],[c_470,c_171]) ).

tcf(c_520,plain,
    ! [X0: $i,X1: $i] : iPr_def_15(multiply(inverse(X0),inverse(multiply(inverse(X1),X1))),X1) = iPr_def_14(X0,inverse(multiply(inverse(X1),X1))),
    inference(superposition,[status(thm)],[c_171,c_469]) ).

tcf(c_524,plain,
    ! [X0: $i,X1: $i,X2: $i] : multiply(inverse(iPr_def_14(X0,multiply(X1,inverse(inverse(multiply(inverse(X2),X2)))))),inverse(iPr_def_15(inverse(multiply(inverse(X2),X2)),X2))) = X0,
    inference(superposition,[status(thm)],[c_171,c_470]) ).

tcf(c_534,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i] : multiply(inverse(X0),multiply(inverse(iPr_def_14(X0,multiply(X1,inverse(inverse(multiply(inverse(X2),X2)))))),inverse(inverse(multiply(inverse(X3),X3))))) = iPr_def_15(iPr_def_15(inverse(multiply(inverse(X2),X2)),X2),X3),
    inference(superposition,[status(thm)],[c_171,c_515]) ).

tcf(c_541,plain,
    ! [X0: $i,X1: $i,X2: $i] : iPr_def_16(multiply(X0,inverse(inverse(multiply(inverse(X1),X1)))),X2) = iPr_def_15(iPr_def_15(inverse(multiply(inverse(X1),X1)),X1),X2),
    inference(demodulation,[status(thm)],[c_534,c_253]) ).

tcf(c_542,plain,
    ! [X0: $i,X1: $i] : iPr_def_15(multiply(inverse(X0),X0),X1) = iPr_def_16(X0,X1),
    inference(demodulation,[status(thm)],[c_515,c_253]) ).

tcf(c_558,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i] : iPr_def_15(iPr_def_15(inverse(multiply(inverse(X0),X0)),X0),X1) = iPr_def_16(iPr_def_14(X2,multiply(inverse(X3),X3)),X1),
    inference(superposition,[status(thm)],[c_474,c_541]) ).

tcf(c_568,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] : iPr_def_16(multiply(X0,inverse(inverse(multiply(inverse(X1),X1)))),X2) = iPr_def_16(iPr_def_14(X3,multiply(inverse(X4),X4)),X2),
    inference(superposition,[status(thm)],[c_558,c_541]) ).

tcf(c_570,plain,
    ! [X0: $i,X1: $i,X2: $i] : iPr_def_15(iPr_def_15(inverse(multiply(inverse(X0),X0)),X0),X1) = iPr_def_15(iPr_def_15(inverse(multiply(inverse(X2),X2)),X2),X1),
    inference(superposition,[status(thm)],[c_558,c_558]) ).

tcf(c_596,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i] : iPr_def_16(multiply(X0,inverse(inverse(multiply(inverse(X1),X1)))),X2) = iPr_def_15(iPr_def_15(inverse(multiply(inverse(X3),X3)),X3),X2),
    inference(superposition,[status(thm)],[c_568,c_558]) ).

tcf(c_791,plain,
    ! [X0: $i,X1: $i] : multiply(inverse(iPr_def_14(X0,inverse(multiply(inverse(X1),X1)))),inverse(multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(multiply(inverse(X1),X1))))) = iPr_def_14(multiply(inverse(X0),inverse(multiply(inverse(X1),X1))),X1),
    inference(superposition,[status(thm)],[c_520,c_513]) ).

tcf(c_797,plain,
    ! [X0: $i,X1: $i,X2: $i] : multiply(inverse(iPr_def_15(iPr_def_15(inverse(multiply(inverse(X0),X0)),X0),X1)),inverse(multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(multiply(inverse(X1),X1))))) = iPr_def_14(iPr_def_15(inverse(multiply(inverse(X2),X2)),X2),X1),
    inference(superposition,[status(thm)],[c_570,c_513]) ).

tcf(c_805,plain,
    ! [X0: $i,X1: $i] : iPr_def_14(multiply(inverse(X0),inverse(multiply(inverse(X1),X1))),X1) = X0,
    inference(demodulation,[status(thm)],[c_791,c_470]) ).

tcf(c_806,plain,
    ! [X0: $i,X1: $i,X2: $i] : iPr_def_14(iPr_def_15(inverse(multiply(inverse(X0),X0)),X0),X1) = iPr_def_14(iPr_def_15(inverse(multiply(inverse(X2),X2)),X2),X1),
    inference(demodulation,[status(thm)],[c_797,c_513]) ).

tcf(c_808,plain,
    ! [X0: $i,X1: $i] : multiply(inverse(iPr_def_14(X0,inverse(multiply(inverse(X1),X1)))),inverse(multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(multiply(inverse(X1),X1))))) = iPr_def_14(multiply(inverse(X0),inverse(multiply(inverse(X1),X1))),X1),
    inference(superposition,[status(thm)],[c_232,c_225]) ).

tcf(c_814,plain,
    ! [X0: $i,X1: $i,X2: $i] : multiply(inverse(iPr_def_15(iPr_def_15(inverse(multiply(inverse(X0),X0)),X0),X1)),inverse(multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(multiply(inverse(X1),X1))))) = iPr_def_14(iPr_def_15(inverse(multiply(inverse(X2),X2)),X2),X1),
    inference(superposition,[status(thm)],[c_335,c_225]) ).

tcf(c_822,plain,
    ! [X0: $i,X1: $i] : iPr_def_14(multiply(inverse(X0),inverse(multiply(inverse(X1),X1))),X1) = X0,
    inference(demodulation,[status(thm)],[c_808,c_121]) ).

tcf(c_823,plain,
    ! [X0: $i,X1: $i,X2: $i] : iPr_def_14(iPr_def_15(inverse(multiply(inverse(X0),X0)),X0),X1) = iPr_def_14(iPr_def_15(inverse(multiply(inverse(X2),X2)),X2),X1),
    inference(demodulation,[status(thm)],[c_814,c_225]) ).

tcf(c_1030,plain,
    ! [X0: $i,X1: $i,X2: $i] : multiply(inverse(iPr_def_14(iPr_def_15(inverse(multiply(inverse(X0),X0)),X0),X1)),inverse(multiply(inverse(X1),X1))) = iPr_def_15(inverse(multiply(inverse(X2),X2)),X2),
    inference(superposition,[status(thm)],[c_806,c_470]) ).

tcf(c_1034,plain,
    ! [X0: $i,X1: $i] : iPr_def_15(inverse(multiply(inverse(X0),X0)),X0) = iPr_def_15(inverse(multiply(inverse(X1),X1)),X1),
    inference(demodulation,[status(thm)],[c_1030,c_470]) ).

tcf(c_1054,plain,
    ! [X0: $i,X1: $i,X2: $i] : multiply(inverse(iPr_def_14(iPr_def_15(inverse(multiply(inverse(X0),X0)),X0),X1)),inverse(multiply(inverse(X1),X1))) = iPr_def_15(inverse(multiply(inverse(X2),X2)),X2),
    inference(superposition,[status(thm)],[c_823,c_121]) ).

tcf(c_1058,plain,
    ! [X0: $i,X1: $i] : iPr_def_15(inverse(multiply(inverse(X0),X0)),X0) = iPr_def_15(inverse(multiply(inverse(X1),X1)),X1),
    inference(demodulation,[status(thm)],[c_1054,c_121]) ).

tcf(c_1123,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i] : multiply(inverse(iPr_def_14(X0,multiply(X1,inverse(inverse(multiply(inverse(X2),X2)))))),inverse(iPr_def_15(inverse(multiply(inverse(X3),X3)),X3))) = X0,
    inference(superposition,[status(thm)],[c_1034,c_524]) ).

tcf(c_1135,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i] : multiply(inverse(iPr_def_14(X0,multiply(X1,inverse(inverse(multiply(inverse(X2),X2)))))),inverse(iPr_def_15(inverse(multiply(inverse(X3),X3)),X3))) = X0,
    inference(superposition,[status(thm)],[c_1058,c_236]) ).

tcf(c_1169,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i] : multiply(inverse(X0),inverse(multiply(inverse(multiply(X1,inverse(inverse(multiply(inverse(X2),X2))))),multiply(X1,inverse(inverse(multiply(inverse(X2),X2))))))) = multiply(inverse(X0),inverse(iPr_def_15(inverse(multiply(inverse(X3),X3)),X3))),
    inference(superposition,[status(thm)],[c_805,c_1123]) ).

tcf(c_1182,plain,
    ! [X0: $i,X1: $i,X2: $i] : multiply(inverse(X0),inverse(iPr_def_15(inverse(multiply(inverse(X1),X1)),X1))) = multiply(inverse(X0),inverse(iPr_def_15(inverse(multiply(inverse(X2),X2)),X2))),
    inference(demodulation,[status(thm)],[c_1169,c_171]) ).

tcf(c_1183,plain,
    ! [X0: $i,X1: $i] : multiply(inverse(X0),inverse(iPr_def_15(inverse(multiply(inverse(X1),X1)),X1))) = iPr_def_17(X0),
    inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_17])],[c_1182]) ).

tcf(c_1185,plain,
    ! [X0: $i,X1: $i,X2: $i] : iPr_def_17(iPr_def_14(X0,multiply(X1,inverse(inverse(multiply(inverse(X2),X2)))))) = X0,
    inference(demodulation,[status(thm)],[c_1123,c_1183]) ).

tcf(c_1194,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] : iPr_def_14(iPr_def_14(X0,multiply(X1,inverse(inverse(multiply(inverse(X2),X2))))),inverse(iPr_def_15(inverse(multiply(inverse(X3),X3)),X3))) = multiply(inverse(multiply(X4,inverse(X0))),multiply(X4,inverse(inverse(iPr_def_15(inverse(multiply(inverse(X3),X3)),X3))))),
    inference(superposition,[status(thm)],[c_1135,c_111]) ).

tcf(c_1195,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] : multiply(inverse(multiply(inverse(iPr_def_14(X0,multiply(X1,inverse(inverse(multiply(inverse(X2),X2)))))),inverse(multiply(inverse(X3),iPr_def_15(inverse(multiply(inverse(X4),X4)),X4))))),X0) = iPr_def_14(X3,iPr_def_15(inverse(multiply(inverse(X4),X4)),X4)),
    inference(superposition,[status(thm)],[c_1135,c_111]) ).

tcf(c_1201,plain,
    ! [X0: $i,X1: $i,X2: $i] : iPr_def_17(iPr_def_14(X0,multiply(X1,inverse(inverse(multiply(inverse(X2),X2)))))) = X0,
    inference(demodulation,[status(thm)],[c_1135,c_1183]) ).

tcf(c_1206,plain,
    ! [X0: $i,X1: $i,X2: $i] : iPr_def_17(iPr_def_14(X0,iPr_def_14(X1,multiply(inverse(X2),X2)))) = X0,
    inference(superposition,[status(thm)],[c_474,c_1185]) ).

tcf(c_1212,plain,
    ! [X0: $i,X1: $i,X2: $i] : iPr_def_17(iPr_def_14(X0,iPr_def_14(X1,multiply(inverse(X2),X2)))) = X0,
    inference(superposition,[status(thm)],[c_132,c_1201]) ).

tcf(c_1219,plain,
    ! [X0: $i,X1: $i] : iPr_def_17(iPr_def_14(X0,X1)) = X0,
    inference(superposition,[status(thm)],[c_805,c_1206]) ).

tcf(c_1228,plain,
    ! [X0: $i,X1: $i] : iPr_def_17(iPr_def_14(X0,X1)) = X0,
    inference(superposition,[status(thm)],[c_822,c_1212]) ).

tcf(c_1235,plain,
    ! [X0: $i,X1: $i] : iPr_def_17(iPr_def_15(X0,X1)) = iPr_def_14(X0,X1),
    inference(superposition,[status(thm)],[c_508,c_1219]) ).

tcf(c_1236,plain,
    ! [X0: $i,X1: $i] : multiply(inverse(X0),inverse(multiply(inverse(X1),X1))) = iPr_def_17(X0),
    inference(superposition,[status(thm)],[c_805,c_1219]) ).

tcf(c_1241,plain,
    ! [X0: $i,X1: $i] : iPr_def_14(iPr_def_17(X0),X1) = X0,
    inference(demodulation,[status(thm)],[c_805,c_1236]) ).

tcf(c_1247,plain,
    ! [X0: $i,X1: $i] : iPr_def_17(iPr_def_15(X0,X1)) = iPr_def_14(X0,X1),
    inference(superposition,[status(thm)],[c_201,c_1228]) ).

tcf(c_1248,plain,
    ! [X0: $i,X1: $i] : multiply(inverse(X0),inverse(multiply(inverse(X1),X1))) = iPr_def_17(X0),
    inference(superposition,[status(thm)],[c_822,c_1228]) ).

tcf(c_1253,plain,
    ! [X0: $i,X1: $i] : iPr_def_14(iPr_def_17(X0),X1) = X0,
    inference(demodulation,[status(thm)],[c_822,c_1248]) ).

tcf(c_1260,plain,
    ! [X0: $i,X1: $i,X2: $i] : iPr_def_14(X0,X1) = iPr_def_14(X0,X2),
    inference(superposition,[status(thm)],[c_1219,c_1241]) ).

tcf(c_1265,plain,
    ! [X0: $i,X1: $i,X2: $i] : iPr_def_14(X0,X1) = iPr_def_14(X0,X2),
    inference(superposition,[status(thm)],[c_1228,c_1253]) ).

tcf(c_1295,plain,
    ! [X0: $i,X1: $i,X2: $i] : multiply(inverse(X0),multiply(inverse(iPr_def_14(X0,X1)),inverse(X2))) = iPr_def_14(X2,X2),
    inference(superposition,[status(thm)],[c_1260,c_471]) ).

tcf(c_1326,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i] : multiply(inverse(multiply(inverse(iPr_def_14(X0,X1)),inverse(multiply(inverse(X2),multiply(inverse(X3),X3))))),X0) = iPr_def_14(X2,multiply(inverse(X3),X3)),
    inference(superposition,[status(thm)],[c_1265,c_132]) ).

tcf(c_1327,plain,
    ! [X0: $i,X1: $i,X2: $i] : multiply(inverse(X0),multiply(inverse(iPr_def_14(X0,X1)),inverse(X2))) = iPr_def_14(X2,X2),
    inference(superposition,[status(thm)],[c_1265,c_129]) ).

tcf(c_1344,plain,
    ! [X0: $i,X1: $i,X2: $i] : iPr_def_14(iPr_def_14(X0,X1),X2) = iPr_def_15(X0,X1),
    inference(superposition,[status(thm)],[c_1235,c_1241]) ).

tcf(c_1357,plain,
    ! [X0: $i,X1: $i,X2: $i] : iPr_def_14(iPr_def_14(X0,X1),X2) = iPr_def_15(X0,X1),
    inference(superposition,[status(thm)],[c_1247,c_1253]) ).

tcf(c_1369,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i] : iPr_def_14(iPr_def_14(X0,X1),X2) = iPr_def_15(X0,X3),
    inference(superposition,[status(thm)],[c_1260,c_1344]) ).

tcf(c_1383,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i] : iPr_def_14(iPr_def_14(X0,X1),X2) = iPr_def_15(X0,X3),
    inference(superposition,[status(thm)],[c_1265,c_1357]) ).

tcf(c_1397,plain,
    ! [X0: $i,X1: $i,X2: $i] : iPr_def_15(iPr_def_17(X0),X1) = iPr_def_14(X0,X2),
    inference(superposition,[status(thm)],[c_1241,c_1369]) ).

tcf(c_1411,plain,
    ! [X0: $i,X1: $i,X2: $i] : iPr_def_17(iPr_def_15(X0,X1)) = iPr_def_14(X0,X2),
    inference(superposition,[status(thm)],[c_1369,c_1219]) ).

tcf(c_1417,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] : iPr_def_14(iPr_def_14(X0,X1),X2) = iPr_def_14(iPr_def_14(X0,X3),X4),
    inference(superposition,[status(thm)],[c_1369,c_1369]) ).

tcf(c_1442,plain,
    ! [X0: $i,X1: $i,X2: $i] : iPr_def_15(iPr_def_17(X0),X1) = iPr_def_14(X0,X2),
    inference(superposition,[status(thm)],[c_1253,c_1383]) ).

tcf(c_1456,plain,
    ! [X0: $i,X1: $i,X2: $i] : iPr_def_17(iPr_def_15(X0,X1)) = iPr_def_14(X0,X2),
    inference(superposition,[status(thm)],[c_1383,c_1228]) ).

tcf(c_1721,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i] : iPr_def_14(iPr_def_15(iPr_def_17(X0),X1),X2) = iPr_def_15(X0,X3),
    inference(superposition,[status(thm)],[c_1397,c_1369]) ).

tcf(c_1728,plain,
    ! [X0: $i,X1: $i] : iPr_def_15(iPr_def_17(iPr_def_17(X0)),X1) = X0,
    inference(superposition,[status(thm)],[c_1397,c_1241]) ).

tcf(c_1753,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i] : iPr_def_14(iPr_def_15(iPr_def_17(X0),X1),X2) = iPr_def_15(X0,X3),
    inference(superposition,[status(thm)],[c_1442,c_1383]) ).

tcf(c_1760,plain,
    ! [X0: $i,X1: $i] : iPr_def_15(iPr_def_17(iPr_def_17(X0)),X1) = X0,
    inference(superposition,[status(thm)],[c_1442,c_1253]) ).

tcf(c_1820,plain,
    ! [X0: $i,X1: $i] : iPr_def_17(iPr_def_17(iPr_def_15(X0,X1))) = X0,
    inference(superposition,[status(thm)],[c_1411,c_1219]) ).

tcf(c_1826,plain,
    ! [X0: $i,X1: $i,X2: $i] : iPr_def_17(iPr_def_15(X0,X1)) = iPr_def_17(iPr_def_15(X0,X2)),
    inference(superposition,[status(thm)],[c_1411,c_1411]) ).

tcf(c_1827,plain,
    ! [X0: $i,X1: $i,X2: $i] : iPr_def_15(iPr_def_17(X0),X1) = iPr_def_17(iPr_def_15(X0,X2)),
    inference(superposition,[status(thm)],[c_1411,c_1397]) ).

tcf(c_1859,plain,
    ! [X0: $i,X1: $i] : iPr_def_17(iPr_def_17(iPr_def_15(X0,X1))) = X0,
    inference(superposition,[status(thm)],[c_1456,c_1228]) ).

tcf(c_1866,plain,
    ! [X0: $i,X1: $i,X2: $i] : iPr_def_15(iPr_def_17(X0),X1) = iPr_def_17(iPr_def_15(X0,X2)),
    inference(superposition,[status(thm)],[c_1456,c_1442]) ).

tcf(c_1875,plain,
    ! [X0: $i,X1: $i] : iPr_def_17(iPr_def_17(iPr_def_16(X0,X1))) = multiply(inverse(X0),X0),
    inference(superposition,[status(thm)],[c_542,c_1820]) ).

tcf(c_1876,plain,
    ! [X0: $i,X1: $i] : iPr_def_17(iPr_def_17(iPr_def_15(inverse(multiply(inverse(X0),X0)),X0))) = inverse(multiply(inverse(X1),X1)),
    inference(superposition,[status(thm)],[c_1034,c_1820]) ).

tcf(c_1888,plain,
    ! [X0: $i,X1: $i] : inverse(multiply(inverse(X0),X0)) = inverse(multiply(inverse(X1),X1)),
    inference(demodulation,[status(thm)],[c_1876,c_1820]) ).

tcf(c_1889,plain,
    ! [X0: $i] : inverse(multiply(inverse(X0),X0)) = iPr_def_18,
    inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_18])],[c_1888]) ).

tcf(c_1897,plain,
    ! [X0: $i,X1: $i,X2: $i] : iPr_def_15(iPr_def_15(inverse(multiply(inverse(X0),X0)),X0),X1) = iPr_def_16(multiply(X2,inverse(iPr_def_18)),X1),
    inference(demodulation,[status(thm)],[c_596,c_1889]) ).

tcf(c_1900,plain,
    ! [X0: $i,X1: $i,X2: $i] : multiply(inverse(X0),multiply(inverse(iPr_def_14(X0,X1)),inverse(iPr_def_18))) = iPr_def_16(X1,X2),
    inference(demodulation,[status(thm)],[c_253,c_1889]) ).

tcf(c_1903,plain,
    ! [X0: $i,X1: $i] : iPr_def_16(X0,X1) = iPr_def_14(iPr_def_18,iPr_def_18),
    inference(demodulation,[status(thm)],[c_1900,c_1295]) ).

tcf(c_1908,plain,
    ! [X0: $i,X1: $i] : iPr_def_15(iPr_def_15(iPr_def_18,X0),X1) = iPr_def_14(iPr_def_18,iPr_def_18),
    inference(demodulation,[status(thm)],[c_1897,c_1889,c_1903]) ).

tcf(c_1914,plain,
    ! [X0: $i,X1: $i] : iPr_def_17(iPr_def_17(iPr_def_16(X0,X1))) = multiply(inverse(X0),X0),
    inference(superposition,[status(thm)],[c_274,c_1859]) ).

tcf(c_1935,plain,
    ! [X0: $i,X1: $i,X2: $i] : iPr_def_15(iPr_def_15(inverse(multiply(inverse(X0),X0)),X0),X1) = iPr_def_16(multiply(X2,inverse(iPr_def_18)),X1),
    inference(demodulation,[status(thm)],[c_411,c_1889]) ).

tcf(c_1938,plain,
    ! [X0: $i,X1: $i,X2: $i] : multiply(inverse(X0),multiply(inverse(iPr_def_14(X0,X1)),inverse(iPr_def_18))) = iPr_def_16(X1,X2),
    inference(demodulation,[status(thm)],[c_253,c_1889]) ).

tcf(c_1941,plain,
    ! [X0: $i,X1: $i] : iPr_def_16(X0,X1) = iPr_def_14(iPr_def_18,iPr_def_18),
    inference(demodulation,[status(thm)],[c_1938,c_1327]) ).

tcf(c_1946,plain,
    ! [X0: $i,X1: $i] : iPr_def_15(iPr_def_15(iPr_def_18,X0),X1) = iPr_def_14(iPr_def_18,iPr_def_18),
    inference(demodulation,[status(thm)],[c_1935,c_1889,c_1941]) ).

tcf(c_1958,plain,
    ! [X0: $i,X1: $i] : multiply(iPr_def_18,multiply(inverse(inverse(multiply(inverse(X0),X1))),inverse(X1))) = iPr_def_14(X0,X1),
    inference(superposition,[status(thm)],[c_1889,c_111]) ).

tcf(c_1959,plain,
    ! [X0: $i,X1: $i,X2: $i] : multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),multiply(inverse(X2),X2))))),multiply(X0,iPr_def_18)) = iPr_def_14(X1,multiply(inverse(X2),X2)),
    inference(superposition,[status(thm)],[c_1889,c_111]) ).

tcf(c_1960,plain,
    ! [X0: $i] : inverse(multiply(iPr_def_18,multiply(inverse(X0),X0))) = iPr_def_18,
    inference(superposition,[status(thm)],[c_1889,c_1889]) ).

tcf(c_2065,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] : iPr_def_15(iPr_def_15(iPr_def_17(X0),X1),X2) = iPr_def_14(iPr_def_15(X0,X3),X4),
    inference(superposition,[status(thm)],[c_1827,c_1397]) ).

tcf(c_2110,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] : iPr_def_15(iPr_def_15(iPr_def_17(X0),X1),X2) = iPr_def_14(iPr_def_15(X0,X3),X4),
    inference(superposition,[status(thm)],[c_1866,c_1442]) ).

tcf(c_2130,plain,
    ! [X0: $i] : iPr_def_17(iPr_def_17(iPr_def_14(iPr_def_18,iPr_def_18))) = iPr_def_15(iPr_def_18,X0),
    inference(superposition,[status(thm)],[c_1908,c_1820]) ).

tcf(c_2137,plain,
    ! [X0: $i] : iPr_def_15(iPr_def_18,X0) = iPr_def_17(iPr_def_18),
    inference(demodulation,[status(thm)],[c_2130,c_1219]) ).

tcf(c_2153,plain,
    ! [X0: $i] : iPr_def_17(iPr_def_17(iPr_def_14(iPr_def_18,iPr_def_18))) = iPr_def_15(iPr_def_18,X0),
    inference(superposition,[status(thm)],[c_1946,c_1859]) ).

tcf(c_2160,plain,
    ! [X0: $i] : iPr_def_15(iPr_def_18,X0) = iPr_def_17(iPr_def_18),
    inference(demodulation,[status(thm)],[c_2153,c_1228]) ).

tcf(c_2174,plain,
    ! [X0: $i] : iPr_def_14(iPr_def_18,X0) = iPr_def_17(iPr_def_17(iPr_def_18)),
    inference(superposition,[status(thm)],[c_2137,c_1411]) ).

tcf(c_2176,plain,
    ! [X0: $i,X1: $i] : iPr_def_14(iPr_def_14(iPr_def_18,X0),X1) = iPr_def_17(iPr_def_18),
    inference(superposition,[status(thm)],[c_2137,c_1369]) ).

tcf(c_2185,plain,
    ! [X0: $i] : iPr_def_14(iPr_def_18,X0) = iPr_def_17(iPr_def_17(iPr_def_18)),
    inference(superposition,[status(thm)],[c_2160,c_1456]) ).

tcf(c_2187,plain,
    ! [X0: $i,X1: $i] : iPr_def_14(iPr_def_14(iPr_def_18,X0),X1) = iPr_def_17(iPr_def_18),
    inference(superposition,[status(thm)],[c_2160,c_1383]) ).

tcf(c_2353,plain,
    ! [X0: $i,X1: $i,X2: $i] : multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),multiply(iPr_def_18,multiply(inverse(X2),X2)))))),multiply(X0,iPr_def_18)) = iPr_def_14(X1,multiply(iPr_def_18,multiply(inverse(X2),X2))),
    inference(superposition,[status(thm)],[c_1960,c_111]) ).

tcf(c_2392,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i] : iPr_def_17(iPr_def_15(iPr_def_15(iPr_def_17(X0),X1),X2)) = iPr_def_15(X0,X3),
    inference(superposition,[status(thm)],[c_1721,c_1411]) ).

tcf(c_2457,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i] : iPr_def_17(iPr_def_15(iPr_def_15(iPr_def_17(X0),X1),X2)) = iPr_def_15(X0,X3),
    inference(superposition,[status(thm)],[c_1753,c_1456]) ).

tcf(c_2629,plain,
    ! [X0: $i] : iPr_def_17(iPr_def_17(iPr_def_14(iPr_def_18,iPr_def_18))) = multiply(inverse(X0),X0),
    inference(light_normalisation,[status(thm)],[c_1875,c_1903]) ).

tcf(c_2631,plain,
    ! [X0: $i] : multiply(inverse(X0),X0) = iPr_def_17(iPr_def_18),
    inference(superposition,[status(thm)],[c_1219,c_2629]) ).

tcf(c_2634,plain,
    ! [X0: $i] : multiply(iPr_def_18,multiply(inverse(X0),X0)) = iPr_def_17(iPr_def_17(iPr_def_14(iPr_def_18,iPr_def_18))),
    inference(superposition,[status(thm)],[c_1889,c_2629]) ).

tcf(c_2647,plain,
    inverse(iPr_def_17(iPr_def_17(iPr_def_14(iPr_def_18,iPr_def_18)))) = iPr_def_18,
    inference(superposition,[status(thm)],[c_2629,c_1889]) ).

tcf(c_2648,plain,
    inverse(iPr_def_17(iPr_def_18)) = iPr_def_18,
    inference(demodulation,[status(thm)],[c_2647,c_1219]) ).

tcf(c_2653,plain,
    iPr_def_17(iPr_def_17(iPr_def_14(iPr_def_18,iPr_def_18))) = multiply(iPr_def_18,iPr_def_17(iPr_def_18)),
    inference(demodulation,[status(thm)],[c_2634,c_2631]) ).

tcf(c_2654,plain,
    multiply(iPr_def_18,iPr_def_17(iPr_def_18)) = iPr_def_17(iPr_def_18),
    inference(demodulation,[status(thm)],[c_2653,c_1219]) ).

tcf(c_2666,plain,
    ! [X0: $i] : iPr_def_17(iPr_def_17(iPr_def_14(iPr_def_18,iPr_def_18))) = multiply(inverse(X0),X0),
    inference(light_normalisation,[status(thm)],[c_1914,c_1941]) ).

tcf(c_2668,plain,
    ! [X0: $i] : multiply(inverse(X0),X0) = iPr_def_17(iPr_def_18),
    inference(superposition,[status(thm)],[c_1228,c_2666]) ).

tcf(c_2671,plain,
    ! [X0: $i] : multiply(iPr_def_18,multiply(inverse(X0),X0)) = iPr_def_17(iPr_def_17(iPr_def_14(iPr_def_18,iPr_def_18))),
    inference(superposition,[status(thm)],[c_1889,c_2666]) ).

tcf(c_2684,plain,
    inverse(iPr_def_17(iPr_def_17(iPr_def_14(iPr_def_18,iPr_def_18)))) = iPr_def_18,
    inference(superposition,[status(thm)],[c_2666,c_1889]) ).

tcf(c_2685,plain,
    inverse(iPr_def_17(iPr_def_18)) = iPr_def_18,
    inference(demodulation,[status(thm)],[c_2684,c_1228]) ).

tcf(c_2690,plain,
    iPr_def_17(iPr_def_17(iPr_def_14(iPr_def_18,iPr_def_18))) = multiply(iPr_def_18,iPr_def_17(iPr_def_18)),
    inference(demodulation,[status(thm)],[c_2671,c_2668]) ).

tcf(c_2691,plain,
    multiply(iPr_def_18,iPr_def_17(iPr_def_18)) = iPr_def_17(iPr_def_18),
    inference(demodulation,[status(thm)],[c_2690,c_1228]) ).

tcf(c_2703,plain,
    ! [X0: $i,X1: $i] : multiply(inverse(multiply(X0,inverse(multiply(iPr_def_18,X1)))),multiply(X0,inverse(X1))) = iPr_def_14(iPr_def_17(iPr_def_18),X1),
    inference(superposition,[status(thm)],[c_2648,c_469]) ).

tcf(c_2704,plain,
    ! [X0: $i,X1: $i] : multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),iPr_def_17(iPr_def_18))))),multiply(X0,iPr_def_18)) = iPr_def_14(X1,iPr_def_17(iPr_def_18)),
    inference(superposition,[status(thm)],[c_2648,c_469]) ).

tcf(c_2705,plain,
    ! [X0: $i,X1: $i] : multiply(inverse(multiply(X0,inverse(multiply(iPr_def_18,X1)))),multiply(X0,inverse(X1))) = iPr_def_18,
    inference(demodulation,[status(thm)],[c_2703,c_1241]) ).

tcf(c_2706,plain,
    ! [X0: $i,X1: $i] : multiply(inverse(multiply(X0,inverse(multiply(iPr_def_18,X1)))),multiply(X0,inverse(X1))) = iPr_def_14(iPr_def_17(iPr_def_18),X1),
    inference(superposition,[status(thm)],[c_2685,c_111]) ).

tcf(c_2707,plain,
    ! [X0: $i,X1: $i] : multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),iPr_def_17(iPr_def_18))))),multiply(X0,iPr_def_18)) = iPr_def_14(X1,iPr_def_17(iPr_def_18)),
    inference(superposition,[status(thm)],[c_2685,c_111]) ).

tcf(c_2708,plain,
    ! [X0: $i,X1: $i] : multiply(inverse(multiply(X0,inverse(multiply(iPr_def_18,X1)))),multiply(X0,inverse(X1))) = iPr_def_18,
    inference(demodulation,[status(thm)],[c_2706,c_1253]) ).

tcf(c_2724,plain,
    ! [X0: $i] : multiply(iPr_def_18,inverse(multiply(inverse(X0),X0))) = iPr_def_17(iPr_def_17(iPr_def_18)),
    inference(superposition,[status(thm)],[c_2648,c_1236]) ).

tcf(c_2725,plain,
    ! [X0: $i] : multiply(inverse(X0),inverse(iPr_def_17(iPr_def_18))) = iPr_def_17(X0),
    inference(superposition,[status(thm)],[c_2631,c_1236]) ).

tcf(c_2733,plain,
    ! [X0: $i] : multiply(inverse(X0),iPr_def_18) = iPr_def_17(X0),
    inference(demodulation,[status(thm)],[c_2725,c_2648]) ).

tcf(c_2735,plain,
    multiply(iPr_def_18,iPr_def_18) = iPr_def_17(iPr_def_17(iPr_def_18)),
    inference(demodulation,[status(thm)],[c_2724,c_2631,c_2648]) ).

tcf(c_2740,plain,
    ! [X0: $i] : multiply(iPr_def_18,inverse(multiply(inverse(X0),X0))) = iPr_def_17(iPr_def_17(iPr_def_18)),
    inference(superposition,[status(thm)],[c_2685,c_1248]) ).

tcf(c_2741,plain,
    ! [X0: $i] : multiply(inverse(X0),inverse(iPr_def_17(iPr_def_18))) = iPr_def_17(X0),
    inference(superposition,[status(thm)],[c_2668,c_1248]) ).

tcf(c_2749,plain,
    ! [X0: $i] : multiply(inverse(X0),iPr_def_18) = iPr_def_17(X0),
    inference(demodulation,[status(thm)],[c_2741,c_2685]) ).

tcf(c_2751,plain,
    multiply(iPr_def_18,iPr_def_18) = iPr_def_17(iPr_def_17(iPr_def_18)),
    inference(demodulation,[status(thm)],[c_2740,c_2668,c_2685]) ).

tcf(c_6833,plain,
    ! [X0: $i,X1: $i] : multiply(inverse(multiply(iPr_def_18,multiply(inverse(multiply(inverse(multiply(X0,inverse(multiply(iPr_def_18,X1)))),multiply(X0,inverse(X1)))),inverse(X1)))),inverse(multiply(inverse(X1),X1))) = X1,
    inference(superposition,[status(thm)],[c_2648,c_467]) ).

tcf(c_6842,plain,
    ! [X0: $i,X1: $i] : multiply(inverse(multiply(inverse(X0),multiply(inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(X0),iPr_def_17(iPr_def_18))))),multiply(X1,iPr_def_18))),iPr_def_18))),inverse(multiply(iPr_def_18,iPr_def_17(iPr_def_18)))) = iPr_def_17(iPr_def_18),
    inference(superposition,[status(thm)],[c_2648,c_467]) ).

tcf(c_6852,plain,
    ! [X0: $i] : iPr_def_17(multiply(iPr_def_18,multiply(inverse(iPr_def_18),inverse(X0)))) = X0,
    inference(demodulation,[status(thm)],[c_6833,c_1236,c_2705]) ).

tcf(c_6853,plain,
    iPr_def_17(iPr_def_17(iPr_def_18)) = iPr_def_17(iPr_def_18),
    inference(demodulation,[status(thm)],[c_6842,c_1219,c_2631,c_2648,c_2654,c_2704,c_2733,c_2735]) ).

tcf(c_6864,plain,
    ! [X0: $i] : iPr_def_14(iPr_def_18,X0) = iPr_def_17(iPr_def_18),
    inference(demodulation,[status(thm)],[c_2174,c_6853]) ).

tcf(c_6866,plain,
    ! [X0: $i] : iPr_def_14(iPr_def_17(iPr_def_18),X0) = iPr_def_17(iPr_def_18),
    inference(demodulation,[status(thm)],[c_2176,c_6864]) ).

tcf(c_6871,plain,
    iPr_def_17(iPr_def_18) = iPr_def_18,
    inference(demodulation,[status(thm)],[c_6866,c_1241]) ).

tcf(c_6873,plain,
    ! [X0: $i] : multiply(inverse(X0),X0) = iPr_def_18,
    inference(demodulation,[status(thm)],[c_2631,c_6871]) ).

tcf(c_6874,plain,
    inverse(iPr_def_18) = iPr_def_18,
    inference(demodulation,[status(thm)],[c_2648,c_6871]) ).

tcf(c_6894,plain,
    ! [X0: $i,X1: $i] : multiply(inverse(multiply(iPr_def_18,multiply(inverse(multiply(inverse(multiply(X0,inverse(multiply(iPr_def_18,X1)))),multiply(X0,inverse(X1)))),inverse(X1)))),inverse(multiply(inverse(X1),X1))) = X1,
    inference(superposition,[status(thm)],[c_2685,c_118]) ).

tcf(c_6903,plain,
    ! [X0: $i,X1: $i] : multiply(inverse(multiply(inverse(X0),multiply(inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(X0),iPr_def_17(iPr_def_18))))),multiply(X1,iPr_def_18))),iPr_def_18))),inverse(multiply(iPr_def_18,iPr_def_17(iPr_def_18)))) = iPr_def_17(iPr_def_18),
    inference(superposition,[status(thm)],[c_2685,c_118]) ).

tcf(c_6913,plain,
    ! [X0: $i] : iPr_def_17(multiply(iPr_def_18,multiply(inverse(iPr_def_18),inverse(X0)))) = X0,
    inference(demodulation,[status(thm)],[c_6894,c_1248,c_2708]) ).

tcf(c_6914,plain,
    iPr_def_17(iPr_def_17(iPr_def_18)) = iPr_def_17(iPr_def_18),
    inference(demodulation,[status(thm)],[c_6903,c_1228,c_2668,c_2685,c_2691,c_2707,c_2749,c_2751]) ).

tcf(c_6925,plain,
    ! [X0: $i] : iPr_def_14(iPr_def_18,X0) = iPr_def_17(iPr_def_18),
    inference(demodulation,[status(thm)],[c_2185,c_6914]) ).

tcf(c_6927,plain,
    ! [X0: $i] : iPr_def_14(iPr_def_17(iPr_def_18),X0) = iPr_def_17(iPr_def_18),
    inference(demodulation,[status(thm)],[c_2187,c_6925]) ).

tcf(c_6929,plain,
    ! [X0: $i,X1: $i] : iPr_def_16(X0,X1) = iPr_def_17(iPr_def_18),
    inference(demodulation,[status(thm)],[c_1941,c_6925]) ).

tcf(c_6932,plain,
    iPr_def_17(iPr_def_18) = iPr_def_18,
    inference(demodulation,[status(thm)],[c_6927,c_1253]) ).

tcf(c_6934,plain,
    ! [X0: $i] : multiply(inverse(X0),X0) = iPr_def_18,
    inference(demodulation,[status(thm)],[c_2668,c_6932]) ).

tcf(c_6935,plain,
    inverse(iPr_def_18) = iPr_def_18,
    inference(demodulation,[status(thm)],[c_2685,c_6932]) ).

tcf(c_6936,plain,
    ! [X0: $i] : iPr_def_15(iPr_def_18,X0) = iPr_def_18,
    inference(demodulation,[status(thm)],[c_2160,c_6932]) ).

tcf(c_6944,plain,
    ! [X0: $i,X1: $i,X2: $i] : multiply(inverse(multiply(inverse(multiply(inverse(iPr_def_14(X0,X1)),inverse(multiply(inverse(X2),multiply(inverse(X1),X1))))),X0)),inverse(multiply(inverse(multiply(inverse(X1),X1)),multiply(inverse(X1),X1)))) = X2,
    inference(light_normalisation,[status(thm)],[c_468,c_469]) ).

tcf(c_6945,plain,
    ! [X0: $i,X1: $i] : multiply(inverse(iPr_def_17(multiply(inverse(iPr_def_14(iPr_def_18,X0)),inverse(multiply(inverse(X1),multiply(inverse(X0),X0)))))),inverse(multiply(inverse(multiply(inverse(X0),X0)),multiply(inverse(X0),X0)))) = X1,
    inference(superposition,[status(thm)],[c_2733,c_6944]) ).

tcf(c_6973,plain,
    ! [X0: $i] : iPr_def_17(iPr_def_17(multiply(iPr_def_18,inverse(iPr_def_17(X0))))) = X0,
    inference(demodulation,[status(thm)],[c_6945,c_2733,c_6864,c_6871,c_6873,c_6874]) ).

tcf(c_6991,plain,
    ! [X0: $i,X1: $i,X2: $i] : multiply(inverse(multiply(inverse(multiply(inverse(iPr_def_14(X0,X1)),inverse(multiply(inverse(X2),multiply(inverse(X1),X1))))),X0)),inverse(multiply(inverse(multiply(inverse(X1),X1)),multiply(inverse(X1),X1)))) = X2,
    inference(light_normalisation,[status(thm)],[c_119,c_111]) ).

tcf(c_6992,plain,
    ! [X0: $i,X1: $i] : multiply(inverse(iPr_def_17(multiply(inverse(iPr_def_14(iPr_def_18,X0)),inverse(multiply(inverse(X1),multiply(inverse(X0),X0)))))),inverse(multiply(inverse(multiply(inverse(X0),X0)),multiply(inverse(X0),X0)))) = X1,
    inference(superposition,[status(thm)],[c_2749,c_6991]) ).

tcf(c_7016,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i] : iPr_def_14(multiply(inverse(multiply(inverse(iPr_def_14(X0,X1)),inverse(multiply(inverse(X2),multiply(inverse(X1),X1))))),X0),inverse(multiply(inverse(multiply(inverse(X1),X1)),multiply(inverse(X1),X1)))) = multiply(inverse(multiply(X3,inverse(X2))),multiply(X3,inverse(inverse(multiply(inverse(multiply(inverse(X1),X1)),multiply(inverse(X1),X1)))))),
    inference(superposition,[status(thm)],[c_6991,c_111]) ).

tcf(c_7020,plain,
    ! [X0: $i] : iPr_def_17(iPr_def_17(multiply(iPr_def_18,inverse(iPr_def_17(X0))))) = X0,
    inference(demodulation,[status(thm)],[c_6992,c_2749,c_6925,c_6932,c_6934,c_6935]) ).

tcf(c_7037,plain,
    ! [X0: $i,X1: $i] : multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,iPr_def_18)) = iPr_def_14(iPr_def_14(X1,iPr_def_18),iPr_def_18),
    inference(demodulation,[status(thm)],[c_7016,c_1326,c_6934,c_6935]) ).

tcf(c_8119,plain,
    ! [X0: $i] : iPr_def_17(multiply(iPr_def_18,inverse(iPr_def_17(X0)))) = iPr_def_17(iPr_def_17(multiply(iPr_def_18,inverse(X0)))),
    inference(superposition,[status(thm)],[c_6973,c_6973]) ).

tcf(c_8126,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i] : iPr_def_15(iPr_def_17(multiply(iPr_def_18,inverse(iPr_def_17(X0)))),X1) = iPr_def_14(iPr_def_15(X0,X2),X3),
    inference(superposition,[status(thm)],[c_6973,c_1721]) ).

tcf(c_8131,plain,
    ! [X0: $i,X1: $i] : multiply(iPr_def_18,inverse(iPr_def_17(X0))) = iPr_def_15(X0,X1),
    inference(superposition,[status(thm)],[c_6973,c_1728]) ).

tcf(c_8135,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i] : iPr_def_15(iPr_def_17(iPr_def_17(multiply(iPr_def_18,inverse(X0)))),X1) = iPr_def_14(iPr_def_15(X0,X2),X3),
    inference(demodulation,[status(thm)],[c_8126,c_8119]) ).

tcf(c_8136,plain,
    ! [X0: $i,X1: $i,X2: $i] : iPr_def_14(iPr_def_15(X0,X1),X2) = multiply(iPr_def_18,inverse(X0)),
    inference(demodulation,[status(thm)],[c_8135,c_1728]) ).

tcf(c_8154,plain,
    ! [X0: $i,X1: $i,X2: $i] : iPr_def_15(iPr_def_15(iPr_def_17(X0),X1),X2) = multiply(iPr_def_18,inverse(X0)),
    inference(demodulation,[status(thm)],[c_2065,c_8136]) ).

tcf(c_8158,plain,
    ! [X0: $i,X1: $i] : iPr_def_17(multiply(iPr_def_18,inverse(X0))) = iPr_def_15(X0,X1),
    inference(demodulation,[status(thm)],[c_2392,c_8154]) ).

tcf(c_8199,plain,
    ! [X0: $i] : multiply(iPr_def_18,inverse(iPr_def_17(iPr_def_17(iPr_def_17(X0))))) = X0,
    inference(superposition,[status(thm)],[c_8131,c_1728]) ).

tcf(c_8273,plain,
    ! [X0: $i] : iPr_def_17(multiply(iPr_def_18,multiply(iPr_def_18,inverse(X0)))) = X0,
    inference(light_normalisation,[status(thm)],[c_6852,c_6874]) ).

tcf(c_8275,plain,
    ! [X0: $i] : iPr_def_17(multiply(iPr_def_18,X0)) = iPr_def_17(iPr_def_17(iPr_def_17(X0))),
    inference(superposition,[status(thm)],[c_8199,c_8273]) ).

tcf(c_8285,plain,
    ! [X0: $i,X1: $i] : iPr_def_17(iPr_def_17(iPr_def_17(inverse(X0)))) = iPr_def_15(X0,X1),
    inference(demodulation,[status(thm)],[c_8158,c_8275]) ).

tcf(c_8293,plain,
    ! [X0: $i,X1: $i] : multiply(iPr_def_18,inverse(iPr_def_17(iPr_def_17(iPr_def_17(X0))))) = iPr_def_15(multiply(iPr_def_18,X0),X1),
    inference(superposition,[status(thm)],[c_8275,c_8131]) ).

tcf(c_8297,plain,
    ! [X0: $i,X1: $i] : iPr_def_14(iPr_def_17(iPr_def_17(iPr_def_17(X0))),X1) = multiply(iPr_def_18,X0),
    inference(superposition,[status(thm)],[c_8275,c_1241]) ).

tcf(c_8298,plain,
    ! [X0: $i] : multiply(iPr_def_18,X0) = iPr_def_17(iPr_def_17(X0)),
    inference(demodulation,[status(thm)],[c_8297,c_1241]) ).

tcf(c_8302,plain,
    ! [X0: $i,X1: $i] : iPr_def_17(iPr_def_17(inverse(iPr_def_17(iPr_def_17(iPr_def_17(X0)))))) = iPr_def_15(iPr_def_17(iPr_def_17(X0)),X1),
    inference(demodulation,[status(thm)],[c_8293,c_8298]) ).

tcf(c_8303,plain,
    ! [X0: $i] : iPr_def_17(iPr_def_17(inverse(iPr_def_17(iPr_def_17(iPr_def_17(X0)))))) = X0,
    inference(demodulation,[status(thm)],[c_8302,c_1728]) ).

tcf(c_8305,plain,
    ! [X0: $i,X1: $i] : iPr_def_17(iPr_def_17(inverse(iPr_def_17(X0)))) = iPr_def_15(X0,X1),
    inference(demodulation,[status(thm)],[c_8131,c_8298]) ).

tcf(c_8328,plain,
    ! [X0: $i,X1: $i,X2: $i] : iPr_def_15(iPr_def_15(X0,X1),X2) = iPr_def_17(inverse(X0)),
    inference(superposition,[status(thm)],[c_8285,c_1728]) ).

tcf(c_8384,plain,
    ! [X0: $i,X1: $i] : inverse(iPr_def_17(iPr_def_17(iPr_def_17(X0)))) = iPr_def_15(X0,X1),
    inference(superposition,[status(thm)],[c_8303,c_1728]) ).

tcf(c_8421,plain,
    ! [X0: $i,X1: $i,X2: $i] : iPr_def_15(iPr_def_15(X0,X1),X2) = inverse(iPr_def_17(X0)),
    inference(superposition,[status(thm)],[c_8305,c_1728]) ).

tcf(c_8438,plain,
    ! [X0: $i] : inverse(iPr_def_17(X0)) = iPr_def_17(inverse(X0)),
    inference(demodulation,[status(thm)],[c_8421,c_8328]) ).

tcf(c_8453,plain,
    ! [X0: $i,X1: $i] : iPr_def_17(inverse(iPr_def_14(X0,X1))) = inverse(X0),
    inference(superposition,[status(thm)],[c_1219,c_8438]) ).

tcf(c_8482,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i] : iPr_def_17(inverse(iPr_def_14(iPr_def_14(X0,X1),X2))) = inverse(iPr_def_14(X0,X3)),
    inference(superposition,[status(thm)],[c_1417,c_8453]) ).

tcf(c_8491,plain,
    ! [X0: $i,X1: $i,X2: $i] : inverse(iPr_def_14(X0,X1)) = inverse(iPr_def_14(X0,X2)),
    inference(demodulation,[status(thm)],[c_8482,c_8453]) ).

tcf(c_8492,plain,
    ! [X0: $i,X1: $i] : inverse(iPr_def_14(X0,X1)) = iPr_def_21(X0),
    inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_21])],[c_8491]) ).

tcf(c_8574,plain,
    ! [X0: $i] : iPr_def_21(iPr_def_17(X0)) = inverse(X0),
    inference(superposition,[status(thm)],[c_1241,c_8492]) ).

tcf(c_8587,plain,
    ! [X0: $i,X1: $i] : iPr_def_17(iPr_def_14(X0,X1)) = multiply(iPr_def_21(X0),iPr_def_18),
    inference(superposition,[status(thm)],[c_8492,c_2733]) ).

tcf(c_8590,plain,
    ! [X0: $i] : multiply(iPr_def_21(X0),iPr_def_18) = X0,
    inference(demodulation,[status(thm)],[c_8587,c_1219]) ).

tcf(c_8600,plain,
    ! [X0: $i,X1: $i,X2: $i] : iPr_def_21(iPr_def_17(iPr_def_15(X0,X1))) = inverse(iPr_def_15(X0,X2)),
    inference(superposition,[status(thm)],[c_1826,c_8574]) ).

tcf(c_8609,plain,
    ! [X0: $i,X1: $i,X2: $i] : inverse(iPr_def_15(X0,X1)) = inverse(iPr_def_15(X0,X2)),
    inference(demodulation,[status(thm)],[c_8600,c_8574]) ).

tcf(c_8610,plain,
    ! [X0: $i,X1: $i] : inverse(iPr_def_15(X0,X1)) = iPr_def_22(X0),
    inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_22])],[c_8609]) ).

tcf(c_8655,plain,
    ! [X0: $i] : iPr_def_14(iPr_def_18,X0) = iPr_def_18,
    inference(superposition,[status(thm)],[c_6932,c_1253]) ).

tcf(c_8681,plain,
    ! [X0: $i,X1: $i,X2: $i] : inverse(iPr_def_14(iPr_def_14(X0,X1),X2)) = iPr_def_22(X0),
    inference(superposition,[status(thm)],[c_1369,c_8610]) ).

tcf(c_8685,plain,
    ! [X0: $i] : iPr_def_22(iPr_def_17(iPr_def_17(X0))) = inverse(X0),
    inference(superposition,[status(thm)],[c_1728,c_8610]) ).

tcf(c_8697,plain,
    ! [X0: $i,X1: $i] : iPr_def_21(iPr_def_14(X0,X1)) = iPr_def_22(X0),
    inference(demodulation,[status(thm)],[c_8681,c_8492]) ).

tcf(c_8781,plain,
    ! [X0: $i,X1: $i] : iPr_def_16(X0,X1) = iPr_def_18,
    inference(light_normalisation,[status(thm)],[c_6929,c_6932]) ).

tcf(c_8797,plain,
    ! [X0: $i,X1: $i] : iPr_def_17(iPr_def_17(multiply(iPr_def_18,inverse(X0)))) = iPr_def_14(X0,X1),
    inference(superposition,[status(thm)],[c_1228,c_7020]) ).

tcf(c_8811,plain,
    ! [X0: $i] : iPr_def_17(multiply(iPr_def_18,inverse(iPr_def_17(X0)))) = iPr_def_17(iPr_def_17(multiply(iPr_def_18,inverse(X0)))),
    inference(superposition,[status(thm)],[c_7020,c_7020]) ).

tcf(c_8818,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i] : iPr_def_15(iPr_def_17(multiply(iPr_def_18,inverse(iPr_def_17(X0)))),X1) = iPr_def_14(iPr_def_15(X0,X2),X3),
    inference(superposition,[status(thm)],[c_7020,c_1753]) ).

tcf(c_8823,plain,
    ! [X0: $i,X1: $i] : multiply(iPr_def_18,inverse(iPr_def_17(X0))) = iPr_def_15(X0,X1),
    inference(superposition,[status(thm)],[c_7020,c_1760]) ).

tcf(c_8827,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i] : iPr_def_15(iPr_def_17(iPr_def_17(multiply(iPr_def_18,inverse(X0)))),X1) = iPr_def_14(iPr_def_15(X0,X2),X3),
    inference(demodulation,[status(thm)],[c_8818,c_8811]) ).

tcf(c_8828,plain,
    ! [X0: $i,X1: $i,X2: $i] : iPr_def_14(iPr_def_15(X0,X1),X2) = multiply(iPr_def_18,inverse(X0)),
    inference(demodulation,[status(thm)],[c_8827,c_1760]) ).

tcf(c_8842,plain,
    ! [X0: $i] : iPr_def_17(iPr_def_17(iPr_def_17(multiply(iPr_def_18,inverse(X0))))) = X0,
    inference(demodulation,[status(thm)],[c_7020,c_8811]) ).

tcf(c_8846,plain,
    ! [X0: $i,X1: $i,X2: $i] : iPr_def_15(iPr_def_15(iPr_def_17(X0),X1),X2) = multiply(iPr_def_18,inverse(X0)),
    inference(demodulation,[status(thm)],[c_2110,c_8828]) ).

tcf(c_8850,plain,
    ! [X0: $i,X1: $i] : iPr_def_17(multiply(iPr_def_18,inverse(X0))) = iPr_def_15(X0,X1),
    inference(demodulation,[status(thm)],[c_2457,c_8846]) ).

tcf(c_8886,plain,
    ! [X0: $i,X1: $i] : multiply(iPr_def_18,inverse(iPr_def_17(iPr_def_17(X0)))) = iPr_def_14(X0,X1),
    inference(superposition,[status(thm)],[c_8823,c_1442]) ).

tcf(c_8890,plain,
    ! [X0: $i] : multiply(iPr_def_18,inverse(iPr_def_17(iPr_def_17(iPr_def_17(X0))))) = X0,
    inference(superposition,[status(thm)],[c_8823,c_1760]) ).

tcf(c_9011,plain,
    ! [X0: $i] : iPr_def_17(multiply(iPr_def_18,multiply(iPr_def_18,inverse(X0)))) = X0,
    inference(light_normalisation,[status(thm)],[c_6913,c_6935]) ).

tcf(c_9013,plain,
    ! [X0: $i] : iPr_def_17(multiply(iPr_def_18,X0)) = iPr_def_17(iPr_def_17(iPr_def_17(X0))),
    inference(superposition,[status(thm)],[c_8890,c_9011]) ).

tcf(c_9023,plain,
    ! [X0: $i,X1: $i] : iPr_def_17(iPr_def_17(iPr_def_17(inverse(X0)))) = iPr_def_15(X0,X1),
    inference(demodulation,[status(thm)],[c_8850,c_9013]) ).

tcf(c_9024,plain,
    ! [X0: $i] : iPr_def_17(iPr_def_17(iPr_def_17(iPr_def_17(iPr_def_17(inverse(X0)))))) = X0,
    inference(demodulation,[status(thm)],[c_8842,c_9013]) ).

tcf(c_9038,plain,
    ! [X0: $i,X1: $i] : multiply(iPr_def_22(X0),iPr_def_18) = iPr_def_14(X0,X1),
    inference(superposition,[status(thm)],[c_8697,c_8590]) ).

tcf(c_9073,plain,
    ! [X0: $i,X1: $i] : multiply(iPr_def_18,inverse(iPr_def_17(iPr_def_17(iPr_def_17(X0))))) = iPr_def_15(multiply(iPr_def_18,X0),X1),
    inference(superposition,[status(thm)],[c_9013,c_8823]) ).

tcf(c_9077,plain,
    ! [X0: $i,X1: $i] : iPr_def_14(iPr_def_17(iPr_def_17(iPr_def_17(X0))),X1) = multiply(iPr_def_18,X0),
    inference(superposition,[status(thm)],[c_9013,c_1253]) ).

tcf(c_9078,plain,
    ! [X0: $i] : multiply(iPr_def_18,X0) = iPr_def_17(iPr_def_17(X0)),
    inference(demodulation,[status(thm)],[c_9077,c_1253]) ).

tcf(c_9082,plain,
    ! [X0: $i,X1: $i] : iPr_def_17(iPr_def_17(inverse(iPr_def_17(iPr_def_17(iPr_def_17(X0)))))) = iPr_def_15(iPr_def_17(iPr_def_17(X0)),X1),
    inference(demodulation,[status(thm)],[c_9073,c_9078]) ).

tcf(c_9083,plain,
    ! [X0: $i] : iPr_def_17(iPr_def_17(inverse(iPr_def_17(iPr_def_17(iPr_def_17(X0)))))) = X0,
    inference(demodulation,[status(thm)],[c_9082,c_1760]) ).

tcf(c_9085,plain,
    ! [X0: $i,X1: $i] : iPr_def_17(iPr_def_17(inverse(iPr_def_17(X0)))) = iPr_def_15(X0,X1),
    inference(demodulation,[status(thm)],[c_8823,c_9078]) ).

tcf(c_9106,plain,
    ! [X0: $i,X1: $i,X2: $i] : iPr_def_15(iPr_def_15(X0,X1),X2) = iPr_def_17(inverse(X0)),
    inference(superposition,[status(thm)],[c_9023,c_1760]) ).

tcf(c_9114,plain,
    ! [X0: $i,X1: $i,X2: $i] : iPr_def_14(iPr_def_14(X0,X1),X2) = iPr_def_17(iPr_def_17(iPr_def_17(inverse(X0)))),
    inference(superposition,[status(thm)],[c_9023,c_1383]) ).

tcf(c_9205,plain,
    ! [X0: $i] : iPr_def_17(iPr_def_17(inverse(iPr_def_17(X0)))) = iPr_def_17(iPr_def_17(iPr_def_17(inverse(X0)))),
    inference(superposition,[status(thm)],[c_9024,c_9083]) ).

tcf(c_9222,plain,
    ! [X0: $i] : inverse(iPr_def_17(iPr_def_17(iPr_def_17(X0)))) = iPr_def_17(iPr_def_17(inverse(iPr_def_17(X0)))),
    inference(superposition,[status(thm)],[c_9083,c_9083]) ).

tcf(c_9381,plain,
    ! [X0: $i,X1: $i,X2: $i] : iPr_def_15(iPr_def_15(X0,X1),X2) = inverse(iPr_def_17(X0)),
    inference(superposition,[status(thm)],[c_9085,c_1760]) ).

tcf(c_9398,plain,
    ! [X0: $i] : inverse(iPr_def_17(X0)) = iPr_def_17(inverse(X0)),
    inference(demodulation,[status(thm)],[c_9381,c_9106]) ).

tcf(c_9412,plain,
    ! [X0: $i,X1: $i] : iPr_def_17(inverse(iPr_def_14(X0,X1))) = inverse(X0),
    inference(superposition,[status(thm)],[c_1228,c_9398]) ).

tcf(c_9518,plain,
    ! [X0: $i] : iPr_def_17(iPr_def_21(X0)) = inverse(X0),
    inference(demodulation,[status(thm)],[c_9412,c_8492]) ).

tcf(c_9586,plain,
    ! [X0: $i,X1: $i] : iPr_def_14(inverse(X0),X1) = iPr_def_21(X0),
    inference(superposition,[status(thm)],[c_9518,c_1253]) ).

tcf(c_9603,plain,
    ! [X0: $i] : iPr_def_21(iPr_def_17(X0)) = inverse(X0),
    inference(superposition,[status(thm)],[c_1253,c_8492]) ).

tcf(c_9610,plain,
    inverse(iPr_def_18) = iPr_def_21(iPr_def_18),
    inference(superposition,[status(thm)],[c_8655,c_8492]) ).

tcf(c_9612,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i] : multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),iPr_def_14(X2,X3))))),multiply(X0,iPr_def_21(X2))) = iPr_def_14(X1,iPr_def_14(X2,X3)),
    inference(superposition,[status(thm)],[c_8492,c_111]) ).

tcf(c_9616,plain,
    ! [X0: $i,X1: $i] : iPr_def_17(iPr_def_14(X0,X1)) = multiply(iPr_def_21(X0),iPr_def_18),
    inference(superposition,[status(thm)],[c_8492,c_2749]) ).

tcf(c_9617,plain,
    iPr_def_21(iPr_def_18) = iPr_def_18,
    inference(demodulation,[status(thm)],[c_9610,c_6935]) ).

tcf(c_9619,plain,
    ! [X0: $i] : multiply(iPr_def_21(X0),iPr_def_18) = X0,
    inference(demodulation,[status(thm)],[c_9616,c_1228]) ).

tcf(c_9805,plain,
    ! [X0: $i,X1: $i,X2: $i] : iPr_def_21(iPr_def_15(iPr_def_17(X0),X1)) = inverse(iPr_def_15(X0,X2)),
    inference(superposition,[status(thm)],[c_1866,c_9603]) ).

tcf(c_9811,plain,
    ! [X0: $i] : inverse(iPr_def_21(X0)) = iPr_def_21(inverse(X0)),
    inference(superposition,[status(thm)],[c_9518,c_9603]) ).

tcf(c_9817,plain,
    ! [X0: $i,X1: $i] : iPr_def_21(iPr_def_15(iPr_def_17(X0),X1)) = iPr_def_22(X0),
    inference(demodulation,[status(thm)],[c_9805,c_8610]) ).

tcf(c_10021,plain,
    ! [X0: $i] : inverse(iPr_def_17(iPr_def_17(iPr_def_17(inverse(X0))))) = iPr_def_22(X0),
    inference(superposition,[status(thm)],[c_9023,c_8610]) ).

tcf(c_10023,plain,
    ! [X0: $i,X1: $i,X2: $i] : inverse(iPr_def_14(iPr_def_14(X0,X1),X2)) = iPr_def_22(X0),
    inference(superposition,[status(thm)],[c_1383,c_8610]) ).

tcf(c_10025,plain,
    ! [X0: $i,X1: $i] : inverse(iPr_def_14(X0,X1)) = iPr_def_22(iPr_def_17(X0)),
    inference(superposition,[status(thm)],[c_1442,c_8610]) ).

tcf(c_10028,plain,
    inverse(iPr_def_18) = iPr_def_22(iPr_def_18),
    inference(superposition,[status(thm)],[c_6936,c_8610]) ).

tcf(c_10035,plain,
    iPr_def_22(iPr_def_18) = iPr_def_18,
    inference(demodulation,[status(thm)],[c_10028,c_6935]) ).

tcf(c_10036,plain,
    ! [X0: $i] : iPr_def_22(iPr_def_17(X0)) = iPr_def_21(X0),
    inference(demodulation,[status(thm)],[c_10025,c_8492]) ).

tcf(c_10038,plain,
    ! [X0: $i,X1: $i] : iPr_def_21(iPr_def_14(X0,X1)) = iPr_def_22(X0),
    inference(demodulation,[status(thm)],[c_10023,c_8492]) ).

tcf(c_10039,plain,
    ! [X0: $i] : iPr_def_17(iPr_def_17(iPr_def_17(inverse(inverse(X0))))) = iPr_def_22(X0),
    inference(demodulation,[status(thm)],[c_10021,c_9205,c_9222]) ).

tcf(c_10357,plain,
    ! [X0: $i,X1: $i] : iPr_def_21(iPr_def_17(iPr_def_17(inverse(X0)))) = iPr_def_22(iPr_def_15(X0,X1)),
    inference(superposition,[status(thm)],[c_9023,c_10036]) ).

tcf(c_10359,plain,
    ! [X0: $i] : iPr_def_21(iPr_def_21(X0)) = iPr_def_22(inverse(X0)),
    inference(superposition,[status(thm)],[c_9518,c_10036]) ).

tcf(c_10360,plain,
    ! [X0: $i,X1: $i] : iPr_def_22(iPr_def_15(X0,X1)) = iPr_def_17(inverse(inverse(X0))),
    inference(demodulation,[status(thm)],[c_10357,c_9398,c_9603]) ).

tcf(c_10404,plain,
    ! [X0: $i,X1: $i,X2: $i] : iPr_def_14(iPr_def_21(X0),X1) = iPr_def_21(iPr_def_14(X0,X2)),
    inference(superposition,[status(thm)],[c_8492,c_9586]) ).

tcf(c_10417,plain,
    ! [X0: $i,X1: $i] : iPr_def_14(iPr_def_21(X0),X1) = iPr_def_22(X0),
    inference(demodulation,[status(thm)],[c_10404,c_10038]) ).

tcf(c_10454,plain,
    ! [X0: $i] : iPr_def_17(iPr_def_17(iPr_def_17(iPr_def_17(iPr_def_17(iPr_def_21(inverse(X0))))))) = iPr_def_21(X0),
    inference(superposition,[status(thm)],[c_9811,c_9024]) ).

tcf(c_10459,plain,
    ! [X0: $i] : iPr_def_17(iPr_def_22(X0)) = iPr_def_21(X0),
    inference(demodulation,[status(thm)],[c_10454,c_9518,c_10039]) ).

tcf(c_10613,plain,
    ! [X0: $i] : iPr_def_21(iPr_def_22(X0)) = iPr_def_22(iPr_def_21(X0)),
    inference(superposition,[status(thm)],[c_10459,c_10036]) ).

tcf(c_10614,plain,
    ! [X0: $i] : inverse(iPr_def_22(X0)) = iPr_def_21(iPr_def_21(X0)),
    inference(superposition,[status(thm)],[c_10459,c_9603]) ).

tcf(c_10617,plain,
    ! [X0: $i,X1: $i] : iPr_def_15(iPr_def_17(iPr_def_21(X0)),X1) = iPr_def_22(X0),
    inference(superposition,[status(thm)],[c_10459,c_1760]) ).

tcf(c_10618,plain,
    ! [X0: $i,X1: $i,X2: $i] : iPr_def_14(iPr_def_22(X0),X1) = iPr_def_15(iPr_def_21(X0),X2),
    inference(superposition,[status(thm)],[c_10459,c_1442]) ).

tcf(c_10620,plain,
    ! [X0: $i,X1: $i] : iPr_def_15(inverse(X0),X1) = iPr_def_22(X0),
    inference(demodulation,[status(thm)],[c_10617,c_9518]) ).

tcf(c_10747,plain,
    ! [X0: $i,X1: $i] : multiply(iPr_def_22(X0),iPr_def_18) = iPr_def_14(X0,X1),
    inference(superposition,[status(thm)],[c_10038,c_9619]) ).

tcf(c_11326,plain,
    ! [X0: $i,X1: $i,X2: $i] : iPr_def_14(iPr_def_22(X0),X1) = iPr_def_22(iPr_def_14(X0,X2)),
    inference(superposition,[status(thm)],[c_10038,c_10417]) ).

tcf(c_11335,plain,
    ! [X0: $i,X1: $i] : iPr_def_17(iPr_def_15(iPr_def_21(X0),X1)) = iPr_def_22(X0),
    inference(superposition,[status(thm)],[c_10417,c_1456]) ).

tcf(c_12180,plain,
    ! [X0: $i,X1: $i] : iPr_def_15(iPr_def_21(iPr_def_21(X0)),X1) = iPr_def_22(iPr_def_22(X0)),
    inference(superposition,[status(thm)],[c_10614,c_10620]) ).

tcf(c_12316,plain,
    ! [X0: $i,X1: $i] : iPr_def_21(iPr_def_22(iPr_def_15(iPr_def_17(X0),X1))) = iPr_def_22(iPr_def_22(X0)),
    inference(superposition,[status(thm)],[c_9817,c_10613]) ).

tcf(c_12322,plain,
    ! [X0: $i] : iPr_def_17(inverse(inverse(inverse(X0)))) = iPr_def_22(iPr_def_22(X0)),
    inference(demodulation,[status(thm)],[c_12316,c_9398,c_9603,c_10360]) ).

tcf(c_12375,plain,
    ! [X0: $i] : inverse(multiply(iPr_def_22(X0),iPr_def_18)) = iPr_def_21(X0),
    inference(superposition,[status(thm)],[c_10747,c_8492]) ).

tcf(c_12379,plain,
    ! [X0: $i] : iPr_def_17(multiply(iPr_def_22(X0),iPr_def_18)) = X0,
    inference(superposition,[status(thm)],[c_10747,c_1228]) ).

tcf(c_12654,plain,
    ! [X0: $i,X1: $i] : iPr_def_15(multiply(iPr_def_22(X0),iPr_def_18),X1) = iPr_def_17(iPr_def_17(iPr_def_17(iPr_def_21(X0)))),
    inference(superposition,[status(thm)],[c_12375,c_9023]) ).

tcf(c_12657,plain,
    ! [X0: $i,X1: $i] : iPr_def_15(multiply(iPr_def_22(X0),iPr_def_18),X1) = iPr_def_17(iPr_def_17(inverse(X0))),
    inference(demodulation,[status(thm)],[c_12654,c_9518]) ).

tcf(c_14885,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i] : multiply(inverse(multiply(inverse(multiply(iPr_def_21(inverse(X0)),inverse(multiply(inverse(X1),multiply(inverse(X2),X2))))),inverse(multiply(inverse(X3),X0)))),iPr_def_14(X1,multiply(inverse(X2),X2))) = iPr_def_14(X3,X0),
    inference(light_normalisation,[status(thm)],[c_148,c_9586,c_9811]) ).

tcf(c_15136,plain,
    ! [X0: $i,X1: $i,X2: $i] : iPr_def_14(iPr_def_14(multiply(inverse(X0),X0),X1),inverse(multiply(inverse(X1),X1))) = multiply(inverse(X2),multiply(iPr_def_21(X2),inverse(inverse(multiply(inverse(X1),X1))))),
    inference(light_normalisation,[status(thm)],[c_178,c_8492]) ).

tcf(c_15137,plain,
    ! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(iPr_def_21(X0),inverse(inverse(multiply(inverse(X1),X1))))) = iPr_def_14(iPr_def_14(iPr_def_18,X1),inverse(multiply(inverse(X1),X1))),
    inference(light_normalisation,[status(thm)],[c_15136,c_6934]) ).

tcf(c_15325,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] : multiply(inverse(multiply(X0,inverse(iPr_def_14(iPr_def_14(iPr_def_17(iPr_def_17(iPr_def_17(X1))),X2),inverse(multiply(inverse(X2),X2)))))),multiply(X0,inverse(multiply(X3,inverse(inverse(multiply(inverse(X2),X2))))))) = iPr_def_14(multiply(X3,iPr_def_15(X1,X4)),multiply(X3,inverse(inverse(multiply(inverse(X2),X2))))),
    inference(superposition,[status(thm)],[c_8384,c_491]) ).

tcf(c_15439,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i] : multiply(inverse(multiply(X0,iPr_def_17(inverse(X1)))),multiply(X0,inverse(multiply(X2,iPr_def_18)))) = multiply(iPr_def_22(multiply(X2,iPr_def_15(X1,X3))),iPr_def_18),
    inference(demodulation,[status(thm)],[c_15325,c_6873,c_6874,c_8438,c_8492,c_8685,c_8697,c_9038]) ).

tcf(c_15440,plain,
    ! [X0: $i,X1: $i,X2: $i] : multiply(iPr_def_22(multiply(X0,iPr_def_15(X1,X2))),iPr_def_18) = iPr_def_29(X0,X1),
    inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_29])],[c_15439]) ).

tcf(c_15853,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] : multiply(inverse(multiply(inverse(multiply(iPr_def_21(inverse(inverse(iPr_def_14(iPr_def_14(inverse(multiply(inverse(X0),X0)),X0),inverse(multiply(inverse(X0),X0)))))),inverse(multiply(inverse(X1),multiply(inverse(X2),X2))))),inverse(X3))),iPr_def_14(X1,multiply(inverse(X2),X2))) = iPr_def_14(iPr_def_14(X3,multiply(X4,inverse(inverse(multiply(inverse(X0),X0))))),inverse(iPr_def_14(iPr_def_14(inverse(multiply(inverse(X0),X0)),X0),inverse(multiply(inverse(X0),X0))))),
    inference(superposition,[status(thm)],[c_190,c_14885]) ).

tcf(c_15859,plain,
    ! [X0: $i] : iPr_def_14(iPr_def_14(X0,iPr_def_18),iPr_def_18) = iPr_def_17(iPr_def_17(iPr_def_17(inverse(X0)))),
    inference(demodulation,[status(thm)],[c_15853,c_2749,c_6934,c_6935,c_7037,c_9078,c_9114,c_9205,c_9222,c_9398,c_8492,c_9617,c_10038,c_10039,c_10359,c_10747]) ).

tcf(c_16212,plain,
    ! [X0: $i,X1: $i,X2: $i] : multiply(inverse(multiply(inverse(inverse(multiply(inverse(iPr_def_14(X0,X1)),inverse(inverse(multiply(inverse(X2),X2)))))),inverse(iPr_def_15(multiply(inverse(X1),X1),X2)))),iPr_def_18) = iPr_def_14(X0,multiply(inverse(iPr_def_14(X0,X1)),inverse(inverse(multiply(inverse(X2),X2))))),
    inference(superposition,[status(thm)],[c_6934,c_267]) ).

tcf(c_16369,plain,
    ! [X0: $i] : multiply(iPr_def_22(X0),iPr_def_18) = iPr_def_17(iPr_def_17(inverse(X0))),
    inference(demodulation,[status(thm)],[c_16212,c_2749,c_6934,c_6935,c_8492,c_9619,c_8610,c_10035,c_10747]) ).

tcf(c_16392,plain,
    ! [X0: $i] : iPr_def_17(iPr_def_17(iPr_def_17(inverse(X0)))) = X0,
    inference(demodulation,[status(thm)],[c_12379,c_16369]) ).

tcf(c_16393,plain,
    ! [X0: $i,X1: $i] : iPr_def_15(X0,X1) = X0,
    inference(demodulation,[status(thm)],[c_9023,c_16392]) ).

tcf(c_16428,plain,
    ! [X0: $i] : iPr_def_17(iPr_def_21(X0)) = iPr_def_22(X0),
    inference(demodulation,[status(thm)],[c_11335,c_16393]) ).

tcf(c_16429,plain,
    ! [X0: $i,X1: $i] : iPr_def_14(iPr_def_22(X0),X1) = iPr_def_21(X0),
    inference(demodulation,[status(thm)],[c_10618,c_16393]) ).

tcf(c_16432,plain,
    ! [X0: $i] : iPr_def_21(iPr_def_21(X0)) = iPr_def_22(iPr_def_22(X0)),
    inference(demodulation,[status(thm)],[c_12180,c_16393]) ).

tcf(c_16433,plain,
    ! [X0: $i] : iPr_def_17(inverse(inverse(inverse(X0)))) = iPr_def_21(iPr_def_21(X0)),
    inference(demodulation,[status(thm)],[c_12322,c_16432]) ).

tcf(c_16439,plain,
    ! [X0: $i,X1: $i] : iPr_def_22(iPr_def_14(X0,X1)) = iPr_def_21(X0),
    inference(demodulation,[status(thm)],[c_11326,c_16429]) ).

tcf(c_16441,plain,
    ! [X0: $i] : inverse(X0) = iPr_def_22(X0),
    inference(demodulation,[status(thm)],[c_9518,c_16428]) ).

tcf(c_16444,plain,
    ! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(iPr_def_21(X0),inverse(inverse(multiply(iPr_def_22(X1),X1))))) = iPr_def_14(iPr_def_14(iPr_def_18,X1),inverse(multiply(iPr_def_22(X1),X1))),
    inference(demodulation,[status(thm)],[c_15137,c_16441]) ).

tcf(c_16448,plain,
    ! [X0: $i,X1: $i] : iPr_def_17(iPr_def_17(multiply(iPr_def_18,iPr_def_22(X0)))) = iPr_def_14(X0,X1),
    inference(demodulation,[status(thm)],[c_8797,c_16441]) ).

tcf(c_16456,plain,
    ! [X0: $i] : multiply(iPr_def_22(X0),X0) = iPr_def_18,
    inference(demodulation,[status(thm)],[c_6934,c_16441]) ).

tcf(c_16457,plain,
    ! [X0: $i] : multiply(iPr_def_22(X0),iPr_def_18) = iPr_def_17(X0),
    inference(demodulation,[status(thm)],[c_2749,c_16441]) ).

tcf(c_16460,plain,
    ! [X0: $i,X1: $i] : multiply(iPr_def_18,iPr_def_22(iPr_def_17(iPr_def_17(X0)))) = iPr_def_14(X0,X1),
    inference(demodulation,[status(thm)],[c_8886,c_16441]) ).

tcf(c_16463,plain,
    ! [X0: $i,X1: $i] : iPr_def_17(iPr_def_21(iPr_def_17(iPr_def_17(X0)))) = iPr_def_14(X0,X1),
    inference(demodulation,[status(thm)],[c_16460,c_9078,c_10459]) ).

tcf(c_16465,plain,
    ! [X0: $i,X1: $i] : iPr_def_14(X0,X1) = iPr_def_17(X0),
    inference(demodulation,[status(thm)],[c_10747,c_16457]) ).

tcf(c_16471,plain,
    ! [X0: $i] : iPr_def_17(iPr_def_17(X0)) = X0,
    inference(demodulation,[status(thm)],[c_1253,c_16465]) ).

tcf(c_16474,plain,
    ! [X0: $i] : multiply(iPr_def_18,X0) = X0,
    inference(demodulation,[status(thm)],[c_9078,c_16471]) ).

tcf(c_16478,plain,
    ! [X0: $i] : iPr_def_17(X0) = iPr_def_22(X0),
    inference(demodulation,[status(thm)],[c_16448,c_16471,c_16465,c_16474]) ).

tcf(c_16482,plain,
    ! [X0: $i] : iPr_def_17(iPr_def_17(X0)) = iPr_def_21(X0),
    inference(demodulation,[status(thm)],[c_10036,c_16478]) ).

tcf(c_16484,plain,
    ! [X0: $i] : iPr_def_21(X0) = X0,
    inference(demodulation,[status(thm)],[c_16482,c_16471]) ).

tcf(c_16485,plain,
    ! [X0: $i] : multiply(X0,iPr_def_18) = X0,
    inference(demodulation,[status(thm)],[c_9619,c_16484]) ).

tcf(c_16489,plain,
    ! [X0: $i] : multiply(iPr_def_17(X0),X0) = iPr_def_18,
    inference(demodulation,[status(thm)],[c_16444,c_16456,c_16441,c_16471,c_16465,c_16478,c_16484,c_16485]) ).

tcf(c_16496,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i] : multiply(inverse(multiply(X0,inverse(iPr_def_18))),multiply(X0,inverse(multiply(inverse(iPr_def_14(X1,X2)),inverse(inverse(multiply(inverse(X3),X3))))))) = iPr_def_14(X1,multiply(inverse(iPr_def_14(X1,X2)),inverse(inverse(multiply(inverse(X3),X3))))),
    inference(superposition,[status(thm)],[c_8781,c_299]) ).

tcf(c_16501,plain,
    ! [X0: $i,X1: $i] : multiply(iPr_def_17(X0),multiply(X0,iPr_def_17(X1))) = iPr_def_17(X1),
    inference(demodulation,[status(thm)],[c_16496,c_6932,c_16439,c_16441,c_16471,c_16428,c_16463,c_16478,c_16484,c_16485,c_16489]) ).

tcf(c_16510,plain,
    ! [X0: $i] : inverse(X0) = iPr_def_17(X0),
    inference(light_normalisation,[status(thm)],[c_16441,c_16478]) ).

tcf(c_16572,plain,
    ! [X0: $i] : iPr_def_17(inverse(inverse(iPr_def_17(X0)))) = X0,
    inference(light_normalisation,[status(thm)],[c_16433,c_16484,c_16510]) ).

tcf(c_16986,plain,
    ! [X0: $i,X1: $i] : multiply(iPr_def_17(X0),multiply(X0,X1)) = X1,
    inference(superposition,[status(thm)],[c_16572,c_16501]) ).

tcf(c_16989,plain,
    ! [X0: $i,X1: $i] : multiply(X0,multiply(iPr_def_17(X0),X1)) = X1,
    inference(superposition,[status(thm)],[c_16471,c_16986]) ).

tcf(c_16996,plain,
    multiply(iPr_def_17(a3),iPr_def_10) = b3,
    inference(superposition,[status(thm)],[c_62,c_16986]) ).

tcf(c_16997,plain,
    multiply(iPr_def_17(b3),iPr_def_12) = c3,
    inference(superposition,[status(thm)],[c_64,c_16986]) ).

tcf(c_16998,plain,
    multiply(iPr_def_17(iPr_def_10),iPr_def_11) = c3,
    inference(superposition,[status(thm)],[c_63,c_16986]) ).

tcf(c_17029,plain,
    multiply(a3,b3) = iPr_def_10,
    inference(superposition,[status(thm)],[c_16996,c_16989]) ).

tcf(c_17030,plain,
    multiply(b3,c3) = iPr_def_12,
    inference(superposition,[status(thm)],[c_16997,c_16989]) ).

tcf(c_17142,plain,
    ! [X0: $i,X1: $i,X2: $i] : iPr_def_15(iPr_def_15(iPr_def_17(X0),X1),X2) = multiply(iPr_def_18,iPr_def_17(X0)),
    inference(light_normalisation,[status(thm)],[c_8846,c_16510]) ).

tcf(c_17407,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] : iPr_def_14(iPr_def_14(X0,multiply(X1,inverse(inverse(multiply(inverse(X2),X2))))),inverse(iPr_def_15(inverse(multiply(inverse(X3),X3)),X3))) = multiply(inverse(multiply(X4,iPr_def_17(X0))),multiply(X4,inverse(inverse(iPr_def_15(inverse(multiply(inverse(X3),X3)),X3))))),
    inference(light_normalisation,[status(thm)],[c_1194,c_16510]) ).

tcf(c_17465,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] : multiply(iPr_def_17(inverse(multiply(X0,iPr_def_17(X1)))),iPr_def_14(iPr_def_14(X1,multiply(X2,inverse(inverse(multiply(inverse(X3),X3))))),inverse(iPr_def_15(inverse(multiply(inverse(X4),X4)),X4)))) = multiply(X0,inverse(inverse(iPr_def_15(inverse(multiply(inverse(X4),X4)),X4)))),
    inference(superposition,[status(thm)],[c_17407,c_16986]) ).

tcf(c_17491,plain,
    ! [X0: $i,X1: $i] : multiply(multiply(X0,iPr_def_17(X1)),X1) = X0,
    inference(demodulation,[status(thm)],[c_17465,c_6932,c_9114,c_15859,c_16393,c_16471,c_16465,c_16485,c_16489,c_16510]) ).

tcf(c_17539,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] : multiply(iPr_def_17(inverse(multiply(inverse(iPr_def_14(X0,multiply(X1,inverse(inverse(multiply(inverse(X2),X2)))))),inverse(multiply(inverse(X3),iPr_def_15(inverse(multiply(inverse(X4),X4)),X4)))))),iPr_def_14(X3,iPr_def_15(inverse(multiply(inverse(X4),X4)),X4))) = X0,
    inference(superposition,[status(thm)],[c_1195,c_16986]) ).

tcf(c_17541,plain,
    ! [X0: $i,X1: $i] : multiply(multiply(X0,X1),iPr_def_17(X1)) = X0,
    inference(demodulation,[status(thm)],[c_17539,c_6932,c_16393,c_16471,c_16465,c_16485,c_16489,c_16510]) ).

tcf(c_17588,plain,
    ! [X0: $i,X1: $i] : multiply(iPr_def_18,multiply(inverse(inverse(multiply(iPr_def_17(X0),X1))),inverse(X1))) = iPr_def_17(X0),
    inference(light_normalisation,[status(thm)],[c_1958,c_16465,c_16510]) ).

tcf(c_17598,plain,
    ! [X0: $i,X1: $i] : multiply(iPr_def_18,multiply(inverse(inverse(X0)),inverse(multiply(X1,X0)))) = iPr_def_17(X1),
    inference(superposition,[status(thm)],[c_16986,c_17588]) ).

tcf(c_17623,plain,
    ! [X0: $i,X1: $i] : multiply(X0,iPr_def_17(multiply(X1,X0))) = iPr_def_17(X1),
    inference(demodulation,[status(thm)],[c_17598,c_16471,c_16474,c_16510]) ).

tcf(c_17627,plain,
    ! [X0: $i,X1: $i,X2: $i] : multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),multiply(inverse(X2),X2))))),X0) = iPr_def_14(X1,multiply(inverse(X2),X2)),
    inference(light_normalisation,[status(thm)],[c_1959,c_16485]) ).

tcf(c_17686,plain,
    ! [X0: $i,X1: $i,X2: $i] : inverse(multiply(iPr_def_17(X0),inverse(multiply(inverse(X1),multiply(inverse(X2),X2))))) = multiply(iPr_def_14(X1,multiply(inverse(X2),X2)),X0),
    inference(superposition,[status(thm)],[c_17627,c_17491]) ).

tcf(c_17706,plain,
    ! [X0: $i,X1: $i] : iPr_def_17(multiply(iPr_def_17(X0),X1)) = multiply(iPr_def_17(X1),X0),
    inference(demodulation,[status(thm)],[c_17686,c_16471,c_16465,c_16485,c_16489,c_16510]) ).

tcf(c_17737,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] : multiply(iPr_def_14(iPr_def_14(X0,multiply(X1,inverse(inverse(multiply(inverse(X2),X2))))),inverse(iPr_def_15(inverse(multiply(inverse(X3),X3)),X3))),iPr_def_17(multiply(X4,inverse(inverse(iPr_def_15(inverse(multiply(inverse(X3),X3)),X3)))))) = inverse(multiply(X4,iPr_def_17(X0))),
    inference(superposition,[status(thm)],[c_17407,c_17541]) ).

tcf(c_17761,plain,
    ! [X0: $i,X1: $i] : iPr_def_17(multiply(X0,iPr_def_17(X1))) = multiply(X1,iPr_def_17(X0)),
    inference(demodulation,[status(thm)],[c_17737,c_6932,c_9114,c_15859,c_16393,c_16471,c_16465,c_16485,c_16489,c_16510]) ).

tcf(c_18372,plain,
    ! [X0: $i,X1: $i] : iPr_def_15(multiply(iPr_def_17(X0),iPr_def_18),X1) = iPr_def_17(X0),
    inference(light_normalisation,[status(thm)],[c_12657,c_16471,c_16478,c_16510]) ).

tcf(c_19173,plain,
    ! [X0: $i,X1: $i] : iPr_def_29(iPr_def_17(iPr_def_15(X0,X1)),X0) = multiply(iPr_def_22(iPr_def_18),iPr_def_18),
    inference(superposition,[status(thm)],[c_16489,c_15440]) ).

tcf(c_19190,plain,
    ! [X0: $i,X1: $i] : multiply(iPr_def_22(multiply(X0,iPr_def_17(X1))),iPr_def_18) = iPr_def_29(X0,multiply(iPr_def_17(X1),iPr_def_18)),
    inference(superposition,[status(thm)],[c_18372,c_15440]) ).

tcf(c_19191,plain,
    ! [X0: $i,X1: $i,X2: $i] : iPr_def_22(multiply(X0,iPr_def_15(X1,X2))) = iPr_def_29(X0,X1),
    inference(superposition,[status(thm)],[c_15440,c_16485]) ).

tcf(c_19192,plain,
    ! [X0: $i,X1: $i,X2: $i] : iPr_def_17(iPr_def_22(multiply(X0,iPr_def_15(X1,X2)))) = multiply(iPr_def_18,iPr_def_17(iPr_def_29(X0,X1))),
    inference(superposition,[status(thm)],[c_15440,c_17623]) ).

tcf(c_19196,plain,
    ! [X0: $i,X1: $i] : iPr_def_17(multiply(X0,X1)) = iPr_def_29(X0,X1),
    inference(demodulation,[status(thm)],[c_19191,c_16393,c_16478]) ).

tcf(c_19199,plain,
    ! [X0: $i] : iPr_def_29(iPr_def_17(X0),X0) = iPr_def_18,
    inference(demodulation,[status(thm)],[c_19173,c_6932,c_16393,c_16478,c_16485]) ).

tcf(c_19207,plain,
    ! [X0: $i,X1: $i] : iPr_def_17(iPr_def_29(X0,X1)) = multiply(X0,X1),
    inference(demodulation,[status(thm)],[c_19192,c_16393,c_16471,c_16474,c_16478]) ).

tcf(c_19208,plain,
    ! [X0: $i,X1: $i] : multiply(X0,iPr_def_17(X1)) = iPr_def_29(X1,iPr_def_17(X0)),
    inference(demodulation,[status(thm)],[c_19190,c_16478,c_16485,c_17761]) ).

tcf(c_19233,plain,
    ! [X0: $i,X1: $i] : multiply(iPr_def_17(X0),X1) = iPr_def_29(iPr_def_17(X1),X0),
    inference(demodulation,[status(thm)],[c_17706,c_19196]) ).

tcf(c_19243,plain,
    ! [X0: $i,X1: $i] : multiply(X0,iPr_def_29(iPr_def_17(X1),X0)) = X1,
    inference(demodulation,[status(thm)],[c_16989,c_19233]) ).

tcf(c_19256,plain,
    iPr_def_29(iPr_def_17(iPr_def_11),iPr_def_10) = c3,
    inference(demodulation,[status(thm)],[c_16998,c_19233]) ).

tcf(c_19284,plain,
    ! [X0: $i,X1: $i,X2: $i] : iPr_def_15(iPr_def_15(iPr_def_17(X0),X1),X2) = iPr_def_29(X0,iPr_def_17(iPr_def_18)),
    inference(demodulation,[status(thm)],[c_17142,c_19208]) ).

tcf(c_19287,plain,
    ! [X0: $i] : iPr_def_29(X0,iPr_def_18) = iPr_def_17(X0),
    inference(demodulation,[status(thm)],[c_19284,c_6932,c_16393]) ).

tcf(c_19348,plain,
    ! [X0: $i,X1: $i,X2: $i] : multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),multiply(iPr_def_18,multiply(inverse(X2),X2)))))),X0) = iPr_def_14(X1,multiply(iPr_def_18,multiply(inverse(X2),X2))),
    inference(light_normalisation,[status(thm)],[c_2353,c_16485]) ).

tcf(c_19350,plain,
    ! [X0: $i,X1: $i,X2: $i] : multiply(iPr_def_17(multiply(X0,inverse(multiply(inverse(X1),multiply(iPr_def_18,multiply(inverse(X2),X2)))))),X0) = iPr_def_14(X1,multiply(iPr_def_18,multiply(inverse(X2),X2))),
    inference(superposition,[status(thm)],[c_16510,c_19348]) ).

tcf(c_19377,plain,
    ! [X0: $i,X1: $i] : iPr_def_29(iPr_def_17(X0),multiply(X0,X1)) = iPr_def_17(X1),
    inference(demodulation,[status(thm)],[c_19350,c_16471,c_16465,c_16474,c_16510,c_19196,c_19199,c_19233,c_19287]) ).

tcf(c_20082,plain,
    ! [X0: $i,X1: $i] : iPr_def_29(iPr_def_17(X0),iPr_def_17(X1)) = multiply(X1,X0),
    inference(superposition,[status(thm)],[c_16471,c_19208]) ).

tcf(c_20090,plain,
    ! [X0: $i,X1: $i,X2: $i] : iPr_def_29(multiply(X0,X1),iPr_def_17(X2)) = multiply(X2,iPr_def_29(X0,X1)),
    inference(superposition,[status(thm)],[c_19196,c_19208]) ).

tcf(c_20190,plain,
    ! [X0: $i,X1: $i,X2: $i,X3: $i] : iPr_def_29(iPr_def_17(inverse(multiply(X0,inverse(multiply(inverse(X1),iPr_def_14(X2,X3)))))),iPr_def_14(X1,iPr_def_14(X2,X3))) = iPr_def_17(multiply(X0,iPr_def_21(X2))),
    inference(superposition,[status(thm)],[c_9612,c_19377]) ).

tcf(c_20215,plain,
    ! [X0: $i,X1: $i,X2: $i] : multiply(X0,iPr_def_29(X1,multiply(X2,X0))) = iPr_def_29(X1,X2),
    inference(demodulation,[status(thm)],[c_20190,c_16465,c_16484,c_16510,c_19196,c_19207,c_20082,c_20090]) ).

tcf(c_20737,plain,
    ! [X0: $i] : multiply(b3,iPr_def_29(X0,iPr_def_10)) = iPr_def_29(X0,a3),
    inference(superposition,[status(thm)],[c_17029,c_20215]) ).

tcf(c_20805,plain,
    iPr_def_29(iPr_def_17(iPr_def_11),a3) = multiply(b3,c3),
    inference(superposition,[status(thm)],[c_19256,c_20737]) ).

tcf(c_20811,plain,
    iPr_def_29(iPr_def_17(iPr_def_11),a3) = iPr_def_12,
    inference(demodulation,[status(thm)],[c_20805,c_17030]) ).

tcf(c_20822,plain,
    multiply(a3,iPr_def_12) = iPr_def_11,
    inference(superposition,[status(thm)],[c_20811,c_19243]) ).

tcf(c_20832,plain,
    iPr_def_11 = iPr_def_13,
    inference(demodulation,[status(thm)],[c_65,c_20822]) ).

tcf(c_20833,plain,
    $false,
    inference(forward_subsumption_resolution,[status(thm)],[c_20832,c_66]) ).


%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03  % Problem  : GRP426-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.04  % Command  : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.12/0.38  % Computer : n026.cluster.edu
% 0.12/0.38  % Model    : x86_64 x86_64
% 0.12/0.38  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.38  % Memory   : 8046.5625MB
% 0.12/0.38  % OS       : Linux 6.8.0-71-generic
% 0.12/0.38  % CPULimit : 300
% 0.12/0.38  % WCLimit  : 300
% 0.12/0.38  % DateTime : Wed Sep 23 14:45:54 UTC 2026
% 0.12/0.39  % CPUTime  : 
% 0.12/0.39  Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.12/0.42  Running UEQ theorem proving
% 0.12/0.42  Running: /export/starexec/sandbox/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s ueq_schedule -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.12/0.44  
% 0.12/0.44  % ======== iProver multi-core TPTP/SMT =========
% 0.12/0.44  
% 0.12/0.44  % Detected problem language: tptp
% 0.12/0.45  % Proving...
% 21.85/4.24  WARNING - Clausifier option not provided in the heuristic config "heur/vip2_118404", setting default options.
% 21.85/4.24  % SZS status Started for theBenchmark.p
% 21.85/4.24  % SZS status Unsatisfiable for theBenchmark.p
% 21.85/4.24  
% 21.85/4.24  %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 21.85/4.24  
% 21.85/4.24  % ------  iProver source info
% 21.85/4.24  
% 21.85/4.24  % git: date: 2026-07-19 20:42:38 +0200
% 21.85/4.24  % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 21.85/4.24  % git: non_committed_changes: false
% 21.85/4.24  
% 21.85/4.24  % ------ Parsing...% successful
% 21.85/4.24  
% 21.85/4.24  
% 21.85/4.24  % ------ Clausification by vclausify_rel  & Parsing by iProver...% 
% 21.85/4.24  
% 21.85/4.24  % ------ Preprocessing... sf_s  rm: 0 0s  sf_e  pe_s  pe_e % 
% 21.85/4.24  
% 21.85/4.24  % ------ Preprocessing... gs_s  sp: 0 0s  gs_e  snvd_s sp: 0 0s snvd_e % 
% 21.85/4.24  
% 21.85/4.24  % ------ Preprocessing... sf_s  rm: 0 0s  sf_e 
% 21.85/4.24  % ------ Proving...
% 21.85/4.24  % ------ Problem Properties 
% 21.85/4.24  
% 21.85/4.24  % 
% 21.85/4.24  % clauses                               6
% 21.85/4.24  % conjectures                           1
% 21.85/4.24  % EPR                                   1
% 21.85/4.24  % Horn                                  6
% 21.85/4.24  % unary                                 6
% 21.85/4.24  % binary                                0
% 21.85/4.24  % lits                                  6
% 21.85/4.24  % lits eq                               6
% 21.85/4.24  % fd_pure                               0
% 21.85/4.24  % fd_pseudo                             0
% 21.85/4.24  % fd_cond                               0
% 21.85/4.24  % fd_pseudo_cond                        0
% 21.85/4.24  % AC symbols                            0
% 21.85/4.24  
% 21.85/4.24  % ------ Input Options Time Limit: Unbounded
% 21.85/4.24  
% 21.85/4.24  
% 21.85/4.24  % ------ 
% 21.85/4.24  % Current options:
% 21.85/4.24  % ------ 
% 21.85/4.24  
% 21.85/4.24  
% 21.85/4.24  % 
% 21.85/4.24  
% 21.85/4.24  % ------ Proving...
% 21.85/4.24  % 
% 21.85/4.24  
% 21.85/4.24  % SZS status Unsatisfiable for theBenchmark.p
% 21.85/4.24  
% 21.85/4.24  % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 21.85/4.25  
% 21.85/4.25  
%------------------------------------------------------------------------------