%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : GRP444-1 : TPTP v9.3.1. Released v2.6.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% Computer : n014.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 01:34:16 PM UTC 2026
% Result : Unsatisfiable 5.58s 3.61s
% Output : CNFRefutation 5.58s
% Verified :
% SZS Type : Refutation
% Derivation depth : 41
% Number of leaves : 2
% Syntax : Number of formulae : 251 ( 251 unt; 0 def)
% Number of atoms : 1054 ( 250 equ)
% Maximal formula atoms : 1 ( 4 avg)
% Number of connectives : 2 ( 2 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 4 avg)
% Maximal term depth : 16 ( 2 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 5 ( 3 usr; 3 prp; 0-3 aty)
% Number of functors : 5 ( 5 usr; 3 con; 0-2 aty)
% Number of variables : 702 ( 0 sgn 702 !; 0 ?; 698 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X2,X3,X0,X1] : inverse(multiply(X0,multiply(X1,multiply(multiply(X2,inverse(X2)),inverse(multiply(X3,multiply(X0,X1))))))) = X3,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',single_axiom) ).
fof(f2,negated_conjecture,
multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_these_axioms_3) ).
tcf(c_51,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : inverse(multiply(X0,multiply(X1,multiply(multiply(X2,inverse(X2)),inverse(multiply(X3,multiply(X0,X1))))))) = X3,
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_60,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i] : inverse(multiply(X0,multiply(X1,multiply(multiply(multiply(X2,multiply(X3,multiply(multiply(X4,inverse(X4)),inverse(multiply(X5,multiply(X2,X3)))))),X5),inverse(multiply(X6,multiply(X0,X1))))))) = X6,
inference(superposition,[status(thm)],[c_51,c_51]) ).
tcf(c_61,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] : inverse(multiply(X0,multiply(multiply(multiply(X1,inverse(X1)),inverse(multiply(X2,multiply(X3,X0)))),multiply(multiply(X4,inverse(X4)),X2)))) = X3,
inference(superposition,[status(thm)],[c_51,c_51]) ).
tcf(c_71,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] : inverse(multiply(multiply(multiply(X0,inverse(X0)),inverse(multiply(X1,multiply(X2,X3)))),multiply(multiply(multiply(X4,inverse(X4)),X1),multiply(multiply(X5,inverse(X5)),X2)))) = X3,
inference(superposition,[status(thm)],[c_61,c_51]) ).
tcf(c_73,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i] : inverse(multiply(X0,multiply(multiply(multiply(X1,inverse(X1)),inverse(multiply(X2,multiply(X3,X0)))),multiply(multiply(multiply(X4,multiply(multiply(multiply(X5,inverse(X5)),inverse(multiply(X6,multiply(X7,X4)))),multiply(multiply(X8,inverse(X8)),X6))),X7),X2)))) = X3,
inference(superposition,[status(thm)],[c_61,c_61]) ).
tcf(c_74,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i] : inverse(multiply(multiply(multiply(X0,inverse(X0)),X1),multiply(multiply(multiply(X2,inverse(X2)),X3),multiply(multiply(X4,inverse(X4)),X5)))) = multiply(multiply(X6,inverse(X6)),inverse(multiply(X1,multiply(X3,X5)))),
inference(superposition,[status(thm)],[c_61,c_61]) ).
tcf(c_93,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i] : inverse(multiply(X0,multiply(X1,multiply(multiply(multiply(X2,multiply(multiply(multiply(X3,inverse(X3)),inverse(multiply(X4,multiply(X5,X2)))),multiply(multiply(X6,inverse(X6)),X4))),X5),inverse(multiply(X7,multiply(X0,X1))))))) = X7,
inference(superposition,[status(thm)],[c_51,c_60]) ).
tcf(c_96,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i] : inverse(multiply(X0,multiply(multiply(multiply(X1,inverse(X1)),inverse(multiply(X2,multiply(X3,X0)))),multiply(multiply(multiply(X4,multiply(X5,multiply(multiply(X6,inverse(X6)),inverse(multiply(X7,multiply(X4,X5)))))),X7),X2)))) = X3,
inference(superposition,[status(thm)],[c_51,c_60]) ).
tcf(c_98,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i] : inverse(multiply(multiply(multiply(X0,inverse(X0)),inverse(multiply(X1,multiply(X2,X3)))),multiply(multiply(multiply(X4,inverse(X4)),X1),multiply(multiply(multiply(X5,multiply(X6,multiply(multiply(X7,inverse(X7)),inverse(multiply(X8,multiply(X5,X6)))))),X8),X2)))) = X3,
inference(superposition,[status(thm)],[c_61,c_60]) ).
tcf(c_99,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i] : inverse(multiply(X0,multiply(X1,multiply(multiply(multiply(X2,multiply(X3,multiply(multiply(multiply(X4,multiply(X5,multiply(multiply(X6,inverse(X6)),inverse(multiply(X7,multiply(X4,X5)))))),X7),inverse(multiply(X8,multiply(X2,X3)))))),X8),inverse(multiply(X9,multiply(X0,X1))))))) = X9,
inference(superposition,[status(thm)],[c_60,c_51]) ).
tcf(c_100,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i] : inverse(multiply(X0,multiply(multiply(multiply(multiply(X1,multiply(X2,multiply(multiply(X3,inverse(X3)),inverse(multiply(X4,multiply(X1,X2)))))),X4),inverse(multiply(X5,multiply(X6,X0)))),multiply(multiply(X7,inverse(X7)),X5)))) = X6,
inference(superposition,[status(thm)],[c_60,c_51]) ).
tcf(c_106,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i] : inverse(multiply(multiply(multiply(multiply(X0,multiply(X1,multiply(multiply(X2,inverse(X2)),inverse(multiply(X3,multiply(X0,X1)))))),X3),inverse(multiply(X4,multiply(X5,X6)))),multiply(multiply(multiply(X7,inverse(X7)),X4),multiply(multiply(X8,inverse(X8)),X5)))) = X6,
inference(superposition,[status(thm)],[c_60,c_61]) ).
tcf(c_107,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : multiply(multiply(X0,inverse(X0)),inverse(multiply(X1,multiply(X2,X3)))) = iPr_def_10(X1,X2,X3),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_10])],[c_74]) ).
tcf(c_108,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] : inverse(multiply(multiply(multiply(X0,inverse(X0)),X1),multiply(multiply(multiply(X2,inverse(X2)),X3),multiply(multiply(X4,inverse(X4)),X5)))) = iPr_def_10(X1,X3,X5),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_74]) ).
tcf(c_109,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i] : inverse(multiply(X0,multiply(multiply(multiply(multiply(X1,multiply(X2,iPr_def_10(X3,X1,X2))),X3),inverse(multiply(X4,multiply(X5,X0)))),multiply(multiply(X6,inverse(X6)),X4)))) = X5,
inference(demodulation,[status(thm)],[c_100,c_107]) ).
tcf(c_110,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] : inverse(multiply(X0,multiply(iPr_def_10(X1,X2,X0),multiply(multiply(multiply(X3,multiply(X4,iPr_def_10(X5,X3,X4))),X5),X1)))) = X2,
inference(demodulation,[status(thm)],[c_96,c_107]) ).
tcf(c_111,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i] : inverse(multiply(X0,multiply(X1,multiply(multiply(multiply(X2,multiply(iPr_def_10(X3,X4,X2),multiply(multiply(X5,inverse(X5)),X3))),X4),inverse(multiply(X6,multiply(X0,X1))))))) = X6,
inference(demodulation,[status(thm)],[c_93,c_107]) ).
tcf(c_112,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i] : inverse(multiply(multiply(multiply(multiply(X0,multiply(X1,iPr_def_10(X2,X0,X1))),X2),inverse(multiply(X3,multiply(X4,X5)))),multiply(multiply(multiply(X6,inverse(X6)),X3),multiply(multiply(X7,inverse(X7)),X4)))) = X5,
inference(demodulation,[status(thm)],[c_106,c_107]) ).
tcf(c_113,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i] : inverse(multiply(iPr_def_10(X0,X1,X2),multiply(multiply(multiply(X3,inverse(X3)),X0),multiply(multiply(multiply(X4,multiply(X5,iPr_def_10(X6,X4,X5))),X6),X1)))) = X2,
inference(demodulation,[status(thm)],[c_98,c_107]) ).
tcf(c_115,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i] : inverse(multiply(X0,multiply(iPr_def_10(X1,X2,X0),multiply(multiply(multiply(X3,multiply(iPr_def_10(X4,X5,X3),multiply(multiply(X6,inverse(X6)),X4))),X5),X1)))) = X2,
inference(demodulation,[status(thm)],[c_73,c_107]) ).
tcf(c_117,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i] : inverse(multiply(X0,multiply(X1,multiply(multiply(multiply(X2,multiply(X3,multiply(multiply(multiply(X4,multiply(X5,iPr_def_10(X6,X4,X5))),X6),inverse(multiply(X7,multiply(X2,X3)))))),X7),inverse(multiply(X8,multiply(X0,X1))))))) = X8,
inference(demodulation,[status(thm)],[c_99,c_107]) ).
tcf(c_124,plain,
! [X0: $i,X1: $i,X2: $i] : inverse(multiply(X0,multiply(X1,iPr_def_10(X2,X0,X1)))) = X2,
inference(demodulation,[status(thm)],[c_51,c_107]) ).
tcf(c_125,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : inverse(multiply(X0,multiply(iPr_def_10(X1,X2,X0),multiply(multiply(X3,inverse(X3)),X1)))) = X2,
inference(demodulation,[status(thm)],[c_61,c_107]) ).
tcf(c_126,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] : inverse(multiply(X0,multiply(X1,multiply(multiply(multiply(X2,multiply(X3,iPr_def_10(X4,X2,X3))),X4),inverse(multiply(X5,multiply(X0,X1))))))) = X5,
inference(demodulation,[status(thm)],[c_60,c_107]) ).
tcf(c_184,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] : multiply(multiply(multiply(X0,multiply(X1,iPr_def_10(X2,X0,X1))),X2),inverse(multiply(X3,multiply(X4,X5)))) = iPr_def_10(X3,X4,X5),
inference(superposition,[status(thm)],[c_124,c_107]) ).
tcf(c_186,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] : multiply(multiply(X0,inverse(X0)),inverse(multiply(X1,iPr_def_10(X2,X3,X4)))) = iPr_def_10(X1,multiply(X5,inverse(X5)),inverse(multiply(X2,multiply(X3,X4)))),
inference(superposition,[status(thm)],[c_107,c_107]) ).
tcf(c_221,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i] : inverse(multiply(multiply(multiply(X0,inverse(X0)),X1),multiply(multiply(multiply(X2,inverse(X2)),X3),multiply(multiply(multiply(X4,multiply(X5,iPr_def_10(X6,X4,X5))),X6),X7)))) = iPr_def_10(X1,X3,X7),
inference(superposition,[status(thm)],[c_124,c_108]) ).
tcf(c_222,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i] : inverse(multiply(multiply(multiply(X0,inverse(X0)),X1),multiply(multiply(multiply(X2,inverse(X2)),X3),multiply(multiply(multiply(X4,multiply(iPr_def_10(X5,X6,X4),multiply(multiply(X7,inverse(X7)),X5))),X6),X8)))) = iPr_def_10(X1,X3,X8),
inference(superposition,[status(thm)],[c_125,c_108]) ).
tcf(c_248,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i] : inverse(multiply(X0,multiply(iPr_def_10(X1,X2,X0),multiply(multiply(multiply(X3,multiply(iPr_def_10(X4,X5,X3),multiply(multiply(multiply(X6,multiply(iPr_def_10(X7,X8,X6),multiply(multiply(multiply(X9,multiply(X10,iPr_def_10(X11,X9,X10))),X11),X7))),X8),X4))),X5),X1)))) = X2,
inference(superposition,[status(thm)],[c_110,c_115]) ).
tcf(c_274,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i] : inverse(multiply(multiply(multiply(X0,inverse(X0)),iPr_def_10(X1,X2,X3)),multiply(multiply(multiply(X4,inverse(X4)),multiply(multiply(X5,inverse(X5)),X1)),multiply(multiply(X6,inverse(X6)),multiply(multiply(X7,inverse(X7)),X2))))) = multiply(multiply(X8,inverse(X8)),X3),
inference(superposition,[status(thm)],[c_108,c_71]) ).
tcf(c_276,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i] : inverse(multiply(multiply(multiply(X0,inverse(X0)),X1),multiply(multiply(multiply(X2,inverse(X2)),iPr_def_10(X3,X4,X1)),multiply(multiply(X5,inverse(X5)),multiply(multiply(X6,inverse(X6)),X3))))) = multiply(multiply(multiply(X7,multiply(X8,iPr_def_10(X9,X7,X8))),X9),X4),
inference(superposition,[status(thm)],[c_113,c_71]) ).
tcf(c_277,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i] : inverse(multiply(multiply(multiply(X0,inverse(X0)),X1),multiply(multiply(multiply(X2,inverse(X2)),X3),multiply(multiply(X4,inverse(X4)),iPr_def_10(X5,X1,X3))))) = multiply(multiply(multiply(X6,multiply(iPr_def_10(X7,X8,X6),multiply(multiply(X9,inverse(X9)),X7))),X8),X5),
inference(superposition,[status(thm)],[c_115,c_71]) ).
tcf(c_280,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i] : inverse(multiply(multiply(multiply(X0,inverse(X0)),X1),multiply(multiply(multiply(X2,inverse(X2)),X3),multiply(multiply(X4,inverse(X4)),X5)))) = multiply(multiply(multiply(X6,multiply(X7,iPr_def_10(X8,X6,X7))),X8),inverse(multiply(X1,multiply(X3,X5)))),
inference(superposition,[status(thm)],[c_126,c_71]) ).
tcf(c_281,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i] : inverse(multiply(multiply(multiply(X0,inverse(X0)),inverse(multiply(X1,iPr_def_10(X2,X3,X4)))),multiply(multiply(multiply(X5,inverse(X5)),X1),multiply(multiply(X6,inverse(X6)),multiply(X7,inverse(X7)))))) = inverse(multiply(X2,multiply(X3,X4))),
inference(superposition,[status(thm)],[c_107,c_71]) ).
tcf(c_312,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_10(inverse(multiply(X0,multiply(X1,X2))),X0,X1) = X2,
inference(superposition,[status(thm)],[c_71,c_108]) ).
tcf(c_313,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i] : inverse(multiply(multiply(multiply(X0,inverse(X0)),X1),multiply(multiply(multiply(X2,inverse(X2)),X3),multiply(multiply(multiply(X4,multiply(X5,iPr_def_10(X6,X4,X5))),X6),X7)))) = multiply(multiply(X8,inverse(X8)),inverse(multiply(X1,multiply(X3,X7)))),
inference(superposition,[status(thm)],[c_71,c_126]) ).
tcf(c_315,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i] : inverse(multiply(multiply(multiply(X0,inverse(X0)),X1),multiply(multiply(multiply(multiply(X2,multiply(X3,iPr_def_10(X4,X2,X3))),X4),iPr_def_10(X5,X6,X1)),multiply(multiply(X7,inverse(X7)),multiply(multiply(X8,inverse(X8)),X5))))) = multiply(multiply(X9,inverse(X9)),X6),
inference(superposition,[status(thm)],[c_108,c_109]) ).
tcf(c_321,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i] : inverse(multiply(multiply(multiply(X0,inverse(X0)),X1),multiply(multiply(multiply(multiply(X2,multiply(X3,iPr_def_10(X4,X2,X3))),X4),X5),multiply(multiply(X6,inverse(X6)),X7)))) = iPr_def_10(X1,X5,X7),
inference(superposition,[status(thm)],[c_125,c_109]) ).
tcf(c_323,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i] : inverse(multiply(inverse(multiply(X0,multiply(X1,X2))),multiply(multiply(multiply(multiply(X3,multiply(X4,iPr_def_10(X5,X3,X4))),X5),inverse(multiply(X6,iPr_def_10(X0,X1,X2)))),multiply(multiply(X7,inverse(X7)),X6)))) = multiply(X8,inverse(X8)),
inference(superposition,[status(thm)],[c_107,c_109]) ).
tcf(c_361,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i] : inverse(multiply(multiply(multiply(X0,inverse(X0)),X1),multiply(multiply(multiply(X2,inverse(X2)),X3),multiply(multiply(multiply(X4,multiply(iPr_def_10(X5,X6,X4),multiply(multiply(X7,inverse(X7)),X5))),X6),iPr_def_10(X8,X1,X3))))) = multiply(multiply(X9,inverse(X9)),X8),
inference(superposition,[status(thm)],[c_108,c_111]) ).
tcf(c_366,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i] : inverse(multiply(iPr_def_10(X0,X1,X2),multiply(multiply(multiply(multiply(X3,multiply(iPr_def_10(X4,X5,X3),multiply(multiply(X6,inverse(X6)),X4))),X5),X0),multiply(multiply(multiply(X7,multiply(iPr_def_10(X8,X9,X7),multiply(multiply(X10,inverse(X10)),X8))),X9),X1)))) = X2,
inference(superposition,[status(thm)],[c_115,c_111]) ).
tcf(c_400,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i] : inverse(multiply(multiply(multiply(multiply(X0,multiply(X1,iPr_def_10(X2,X0,X1))),X2),inverse(multiply(inverse(multiply(X3,multiply(X4,X5))),multiply(X6,X7)))),multiply(iPr_def_10(X3,X4,X5),multiply(multiply(X8,inverse(X8)),X6)))) = X7,
inference(superposition,[status(thm)],[c_107,c_112]) ).
tcf(c_412,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i] : inverse(multiply(multiply(multiply(multiply(X0,multiply(X1,iPr_def_10(X2,X0,X1))),X2),inverse(multiply(X3,multiply(inverse(multiply(X4,multiply(X5,X6))),X7)))),multiply(multiply(multiply(X8,inverse(X8)),X3),iPr_def_10(X4,X5,X6)))) = X7,
inference(superposition,[status(thm)],[c_107,c_112]) ).
tcf(c_451,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] : inverse(multiply(iPr_def_10(X0,inverse(multiply(X1,multiply(X2,X3))),X4),multiply(multiply(multiply(X5,inverse(X5)),X0),iPr_def_10(X1,X2,X3)))) = X4,
inference(demodulation,[status(thm)],[c_412,c_184]) ).
tcf(c_452,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] : inverse(multiply(iPr_def_10(inverse(multiply(X0,multiply(X1,X2))),X3,X4),multiply(iPr_def_10(X0,X1,X2),multiply(multiply(X5,inverse(X5)),X3)))) = X4,
inference(demodulation,[status(thm)],[c_400,c_184]) ).
tcf(c_454,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] : iPr_def_10(inverse(multiply(X0,iPr_def_10(X1,X2,X3))),X0,multiply(X4,inverse(X4))) = inverse(multiply(X1,multiply(X2,X3))),
inference(demodulation,[status(thm)],[c_281,c_108]) ).
tcf(c_457,plain,
! [X0: $i] : multiply(X0,inverse(X0)) = iPr_def_11,
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_11])],[c_323]) ).
tcf(c_467,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(iPr_def_11,inverse(multiply(X0,multiply(X1,X2)))) = iPr_def_10(X0,X1,X2),
inference(demodulation,[status(thm)],[c_313,c_221,c_457]) ).
tcf(c_470,plain,
! [X0: $i,X1: $i,X2: $i] : inverse(multiply(multiply(iPr_def_11,X0),multiply(multiply(iPr_def_11,X1),multiply(iPr_def_11,X2)))) = iPr_def_10(X0,X1,X2),
inference(demodulation,[status(thm)],[c_280,c_184,c_457]) ).
tcf(c_478,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_10(iPr_def_10(X0,X1,X2),multiply(iPr_def_11,X0),multiply(iPr_def_11,X1)) = multiply(iPr_def_11,X2),
inference(demodulation,[status(thm)],[c_274,c_457,c_470]) ).
tcf(c_479,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_10(X0,X1,iPr_def_10(X2,X0,X1)) = multiply(iPr_def_11,X2),
inference(demodulation,[status(thm)],[c_361,c_222,c_457]) ).
tcf(c_480,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_10(X0,iPr_def_10(X1,X2,X0),multiply(iPr_def_11,X1)) = multiply(iPr_def_11,X2),
inference(demodulation,[status(thm)],[c_315,c_321,c_457]) ).
tcf(c_481,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : multiply(multiply(multiply(X0,multiply(iPr_def_10(X1,X2,X0),multiply(iPr_def_11,X1))),X2),X3) = multiply(iPr_def_11,X3),
inference(demodulation,[status(thm)],[c_277,c_457,c_470,c_479]) ).
tcf(c_482,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : multiply(multiply(multiply(X0,multiply(X1,iPr_def_10(X2,X0,X1))),X2),X3) = multiply(iPr_def_11,X3),
inference(demodulation,[status(thm)],[c_276,c_457,c_470,c_480]) ).
tcf(c_483,plain,
! [X0: $i,X1: $i,X2: $i] : inverse(multiply(iPr_def_10(X0,X1,X2),multiply(multiply(iPr_def_11,X0),multiply(iPr_def_11,X1)))) = X2,
inference(demodulation,[status(thm)],[c_366,c_457,c_481]) ).
tcf(c_484,plain,
! [X0: $i,X1: $i,X2: $i] : inverse(multiply(X0,multiply(iPr_def_10(X1,X2,X0),multiply(iPr_def_11,X1)))) = X2,
inference(demodulation,[status(thm)],[c_248,c_481,c_482]) ).
tcf(c_927,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(multiply(X0,multiply(X1,iPr_def_10(X2,X0,X1))),X2) = iPr_def_11,
inference(superposition,[status(thm)],[c_124,c_457]) ).
tcf(c_928,plain,
! [X0: $i,X1: $i] : iPr_def_10(inverse(multiply(X0,iPr_def_11)),X0,X1) = inverse(X1),
inference(superposition,[status(thm)],[c_457,c_312]) ).
tcf(c_934,plain,
! [X0: $i,X1: $i] : multiply(iPr_def_11,inverse(multiply(X0,iPr_def_11))) = iPr_def_10(X0,X1,inverse(X1)),
inference(superposition,[status(thm)],[c_457,c_467]) ).
tcf(c_935,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : multiply(iPr_def_11,inverse(multiply(X0,iPr_def_10(X1,X2,X3)))) = iPr_def_10(X0,iPr_def_11,inverse(multiply(X1,multiply(X2,X3)))),
inference(superposition,[status(thm)],[c_467,c_467]) ).
tcf(c_951,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(multiply(X0,multiply(iPr_def_10(X1,X2,X0),multiply(iPr_def_11,X1))),X2) = iPr_def_11,
inference(superposition,[status(thm)],[c_484,c_457]) ).
tcf(c_958,plain,
! [X0: $i,X1: $i] : iPr_def_10(iPr_def_10(inverse(iPr_def_11),X0,X1),iPr_def_11,multiply(iPr_def_11,X0)) = multiply(iPr_def_11,X1),
inference(superposition,[status(thm)],[c_457,c_478]) ).
tcf(c_960,plain,
! [X0: $i,X1: $i] : iPr_def_10(iPr_def_10(X0,inverse(iPr_def_11),X1),multiply(iPr_def_11,X0),iPr_def_11) = multiply(iPr_def_11,X1),
inference(superposition,[status(thm)],[c_457,c_478]) ).
tcf(c_971,plain,
! [X0: $i,X1: $i] : inverse(multiply(iPr_def_10(inverse(iPr_def_11),X0,X1),multiply(iPr_def_11,multiply(iPr_def_11,X0)))) = X1,
inference(superposition,[status(thm)],[c_457,c_483]) ).
tcf(c_973,plain,
! [X0: $i,X1: $i] : inverse(multiply(iPr_def_10(X0,inverse(iPr_def_11),X1),multiply(multiply(iPr_def_11,X0),iPr_def_11))) = X1,
inference(superposition,[status(thm)],[c_457,c_483]) ).
tcf(c_975,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(multiply(iPr_def_10(X0,X1,X2),multiply(multiply(iPr_def_11,X0),multiply(iPr_def_11,X1))),X2) = iPr_def_11,
inference(superposition,[status(thm)],[c_483,c_457]) ).
tcf(c_995,plain,
! [X0: $i,X1: $i] : inverse(multiply(iPr_def_11,multiply(multiply(iPr_def_11,X0),multiply(iPr_def_11,X1)))) = iPr_def_10(inverse(iPr_def_11),X0,X1),
inference(superposition,[status(thm)],[c_457,c_470]) ).
tcf(c_997,plain,
! [X0: $i,X1: $i] : inverse(multiply(multiply(iPr_def_11,X0),multiply(iPr_def_11,multiply(iPr_def_11,X1)))) = iPr_def_10(X0,inverse(iPr_def_11),X1),
inference(superposition,[status(thm)],[c_457,c_470]) ).
tcf(c_2649,plain,
! [X0: $i,X1: $i] : inverse(iPr_def_10(X0,inverse(multiply(X1,iPr_def_11)),X1)) = multiply(iPr_def_11,X0),
inference(superposition,[status(thm)],[c_928,c_479]) ).
tcf(c_2700,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_10(X0,X1,inverse(X1)) = iPr_def_10(X0,X2,inverse(X2)),
inference(superposition,[status(thm)],[c_934,c_934]) ).
tcf(c_2707,plain,
! [X0: $i,X1: $i] : iPr_def_10(X0,inverse(X0),multiply(iPr_def_11,inverse(multiply(X1,iPr_def_11)))) = multiply(iPr_def_11,X1),
inference(superposition,[status(thm)],[c_934,c_479]) ).
tcf(c_2708,plain,
! [X0: $i,X1: $i] : inverse(multiply(X0,multiply(inverse(X0),multiply(iPr_def_11,inverse(multiply(X1,iPr_def_11)))))) = X1,
inference(superposition,[status(thm)],[c_934,c_124]) ).
tcf(c_2716,plain,
! [X0: $i] : multiply(iPr_def_11,inverse(multiply(inverse(multiply(X0,iPr_def_11)),iPr_def_11))) = inverse(inverse(X0)),
inference(superposition,[status(thm)],[c_934,c_928]) ).
tcf(c_2763,plain,
! [X0: $i,X1: $i] : multiply(multiply(X0,multiply(iPr_def_10(inverse(iPr_def_11),X1,X0),iPr_def_11)),X1) = iPr_def_11,
inference(superposition,[status(thm)],[c_457,c_951]) ).
tcf(c_2871,plain,
! [X0: $i] : inverse(multiply(iPr_def_11,multiply(iPr_def_11,multiply(iPr_def_11,X0)))) = iPr_def_10(inverse(iPr_def_11),inverse(iPr_def_11),X0),
inference(superposition,[status(thm)],[c_457,c_995]) ).
tcf(c_3613,plain,
! [X0: $i,X1: $i] : inverse(inverse(multiply(X0,multiply(X1,iPr_def_10(iPr_def_11,X0,X1))))) = multiply(iPr_def_11,inverse(multiply(inverse(iPr_def_11),iPr_def_11))),
inference(superposition,[status(thm)],[c_927,c_2716]) ).
tcf(c_3638,plain,
! [X0: $i,X1: $i] : iPr_def_10(inverse(multiply(X0,iPr_def_11)),X1,inverse(X1)) = inverse(inverse(X0)),
inference(superposition,[status(thm)],[c_2716,c_934]) ).
tcf(c_3720,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(iPr_def_11,multiply(X0,multiply(X1,iPr_def_10(iPr_def_11,X0,X1)))) = iPr_def_10(X2,inverse(X2),multiply(iPr_def_11,inverse(iPr_def_11))),
inference(superposition,[status(thm)],[c_927,c_2707]) ).
tcf(c_3763,plain,
! [X0: $i,X1: $i,X2: $i] : inverse(multiply(X0,multiply(inverse(X0),multiply(iPr_def_11,inverse(iPr_def_11))))) = multiply(X1,multiply(X2,iPr_def_10(iPr_def_11,X1,X2))),
inference(superposition,[status(thm)],[c_927,c_2708]) ).
tcf(c_3765,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(X0,multiply(iPr_def_10(X1,iPr_def_11,X0),multiply(iPr_def_11,X1))) = inverse(multiply(X2,multiply(inverse(X2),multiply(iPr_def_11,inverse(iPr_def_11))))),
inference(superposition,[status(thm)],[c_951,c_2708]) ).
tcf(c_3791,plain,
multiply(iPr_def_11,inverse(multiply(inverse(iPr_def_11),iPr_def_11))) = inverse(iPr_def_11),
inference(demodulation,[status(thm)],[c_3613,c_124]) ).
tcf(c_3792,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(X0,multiply(X1,iPr_def_10(iPr_def_11,X0,X1))) = inverse(multiply(X2,multiply(inverse(X2),iPr_def_11))),
inference(demodulation,[status(thm)],[c_3763,c_457]) ).
tcf(c_3793,plain,
! [X0: $i] : inverse(multiply(X0,multiply(inverse(X0),iPr_def_11))) = iPr_def_12,
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_12])],[c_3792]) ).
tcf(c_3794,plain,
! [X0: $i,X1: $i] : multiply(X0,multiply(X1,iPr_def_10(iPr_def_11,X0,X1))) = iPr_def_12,
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_3792]) ).
tcf(c_3797,plain,
! [X0: $i] : iPr_def_10(X0,inverse(X0),multiply(iPr_def_11,inverse(iPr_def_11))) = multiply(iPr_def_11,iPr_def_12),
inference(demodulation,[status(thm)],[c_3720,c_3794]) ).
tcf(c_3798,plain,
! [X0: $i] : iPr_def_10(X0,inverse(X0),iPr_def_11) = multiply(iPr_def_11,iPr_def_12),
inference(demodulation,[status(thm)],[c_3797,c_457]) ).
tcf(c_3810,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(X0,multiply(iPr_def_10(X1,iPr_def_11,X0),multiply(iPr_def_11,X1))) = inverse(multiply(X2,multiply(inverse(X2),iPr_def_11))),
inference(demodulation,[status(thm)],[c_3765,c_457]) ).
tcf(c_3811,plain,
! [X0: $i,X1: $i] : multiply(X0,multiply(iPr_def_10(X1,iPr_def_11,X0),multiply(iPr_def_11,X1))) = iPr_def_12,
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_3810]) ).
tcf(c_4292,plain,
! [X0: $i] : multiply(multiply(X0,multiply(inverse(X0),iPr_def_11)),iPr_def_12) = iPr_def_11,
inference(superposition,[status(thm)],[c_3793,c_457]) ).
tcf(c_4323,plain,
! [X0: $i] : inverse(multiply(iPr_def_11,multiply(multiply(iPr_def_11,iPr_def_12),multiply(iPr_def_11,X0)))) = inverse(X0),
inference(superposition,[status(thm)],[c_3798,c_484]) ).
tcf(c_4338,plain,
inverse(multiply(multiply(iPr_def_11,iPr_def_12),multiply(iPr_def_11,multiply(iPr_def_11,inverse(inverse(iPr_def_11)))))) = iPr_def_11,
inference(superposition,[status(thm)],[c_3798,c_971]) ).
tcf(c_4342,plain,
multiply(iPr_def_11,multiply(iPr_def_11,iPr_def_11)) = inverse(multiply(iPr_def_11,iPr_def_12)),
inference(superposition,[status(thm)],[c_3798,c_2649]) ).
tcf(c_4359,plain,
! [X0: $i] : inverse(multiply(iPr_def_10(inverse(multiply(inverse(iPr_def_11),iPr_def_11)),inverse(iPr_def_11),X0),multiply(inverse(iPr_def_11),iPr_def_11))) = X0,
inference(superposition,[status(thm)],[c_3791,c_973]) ).
tcf(c_4361,plain,
! [X0: $i] : iPr_def_10(iPr_def_10(inverse(multiply(inverse(iPr_def_11),iPr_def_11)),inverse(iPr_def_11),X0),inverse(iPr_def_11),iPr_def_11) = multiply(iPr_def_11,X0),
inference(superposition,[status(thm)],[c_3791,c_960]) ).
tcf(c_4367,plain,
! [X0: $i] : iPr_def_10(X0,inverse(X0),inverse(iPr_def_11)) = multiply(iPr_def_11,inverse(iPr_def_11)),
inference(superposition,[status(thm)],[c_3791,c_2707]) ).
tcf(c_4368,plain,
! [X0: $i] : iPr_def_10(inverse(iPr_def_11),X0,inverse(X0)) = inverse(iPr_def_11),
inference(superposition,[status(thm)],[c_3791,c_934]) ).
tcf(c_4538,plain,
multiply(iPr_def_12,iPr_def_11) = iPr_def_11,
inference(superposition,[status(thm)],[c_3811,c_951]) ).
tcf(c_4539,plain,
inverse(iPr_def_12) = iPr_def_11,
inference(superposition,[status(thm)],[c_3811,c_484]) ).
tcf(c_4541,plain,
! [X0: $i] : iPr_def_10(X0,inverse(X0),inverse(iPr_def_11)) = iPr_def_11,
inference(demodulation,[status(thm)],[c_4367,c_457]) ).
tcf(c_4550,plain,
! [X0: $i] : iPr_def_10(inverse(iPr_def_11),iPr_def_12,X0) = inverse(X0),
inference(demodulation,[status(thm)],[c_4323,c_995]) ).
tcf(c_4553,plain,
multiply(iPr_def_11,inverse(multiply(iPr_def_12,iPr_def_11))) = iPr_def_11,
inference(demodulation,[status(thm)],[c_4338,c_934,c_997]) ).
tcf(c_4556,plain,
! [X0: $i] : iPr_def_10(inverse(X0),inverse(iPr_def_11),iPr_def_11) = multiply(iPr_def_11,X0),
inference(demodulation,[status(thm)],[c_4361,c_928]) ).
tcf(c_4558,plain,
! [X0: $i] : inverse(multiply(inverse(X0),multiply(inverse(iPr_def_11),iPr_def_11))) = X0,
inference(demodulation,[status(thm)],[c_4359,c_928]) ).
tcf(c_7021,plain,
iPr_def_10(iPr_def_12,iPr_def_11,iPr_def_11) = multiply(iPr_def_11,iPr_def_12),
inference(superposition,[status(thm)],[c_4539,c_3798]) ).
tcf(c_7022,plain,
inverse(multiply(iPr_def_12,multiply(iPr_def_11,iPr_def_11))) = iPr_def_12,
inference(superposition,[status(thm)],[c_4539,c_3793]) ).
tcf(c_7027,plain,
! [X0: $i] : iPr_def_10(inverse(multiply(X0,iPr_def_11)),iPr_def_12,iPr_def_11) = inverse(inverse(X0)),
inference(superposition,[status(thm)],[c_4539,c_3638]) ).
tcf(c_7028,plain,
! [X0: $i,X1: $i] : iPr_def_10(X0,X1,inverse(X1)) = iPr_def_10(X0,iPr_def_12,iPr_def_11),
inference(superposition,[status(thm)],[c_4539,c_2700]) ).
tcf(c_7035,plain,
! [X0: $i] : multiply(iPr_def_11,inverse(multiply(X0,iPr_def_11))) = iPr_def_10(X0,iPr_def_12,iPr_def_11),
inference(superposition,[status(thm)],[c_4538,c_467]) ).
tcf(c_7118,plain,
iPr_def_10(iPr_def_11,iPr_def_11,multiply(iPr_def_11,inverse(inverse(iPr_def_11)))) = multiply(iPr_def_11,inverse(iPr_def_11)),
inference(superposition,[status(thm)],[c_4541,c_958]) ).
tcf(c_7120,plain,
iPr_def_10(iPr_def_11,multiply(iPr_def_11,iPr_def_11),iPr_def_11) = multiply(iPr_def_11,inverse(iPr_def_11)),
inference(superposition,[status(thm)],[c_4541,c_960]) ).
tcf(c_7122,plain,
multiply(iPr_def_11,multiply(inverse(iPr_def_11),iPr_def_11)) = inverse(iPr_def_11),
inference(superposition,[status(thm)],[c_4541,c_2649]) ).
tcf(c_7150,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_10(inverse(multiply(X0,inverse(X1))),X0,multiply(X2,inverse(X2))) = inverse(multiply(inverse(iPr_def_11),multiply(iPr_def_12,X1))),
inference(superposition,[status(thm)],[c_4550,c_454]) ).
tcf(c_7175,plain,
! [X0: $i] : iPr_def_10(X0,iPr_def_11,inverse(multiply(iPr_def_12,iPr_def_11))) = multiply(iPr_def_11,inverse(multiply(X0,iPr_def_11))),
inference(superposition,[status(thm)],[c_4553,c_467]) ).
tcf(c_7233,plain,
! [X0: $i] : multiply(multiply(inverse(X0),multiply(inverse(iPr_def_11),iPr_def_11)),X0) = iPr_def_11,
inference(superposition,[status(thm)],[c_4368,c_2763]) ).
tcf(c_7272,plain,
multiply(multiply(iPr_def_12,multiply(iPr_def_11,iPr_def_11)),iPr_def_12) = iPr_def_11,
inference(superposition,[status(thm)],[c_4539,c_4292]) ).
tcf(c_7289,plain,
iPr_def_10(iPr_def_11,multiply(iPr_def_11,iPr_def_11),iPr_def_11) = iPr_def_11,
inference(demodulation,[status(thm)],[c_7120,c_457]) ).
tcf(c_7299,plain,
iPr_def_10(iPr_def_11,iPr_def_11,multiply(iPr_def_11,inverse(inverse(iPr_def_11)))) = iPr_def_11,
inference(demodulation,[status(thm)],[c_7118,c_457]) ).
tcf(c_7310,plain,
! [X0: $i] : iPr_def_10(X0,iPr_def_11,inverse(multiply(iPr_def_12,iPr_def_11))) = iPr_def_10(X0,iPr_def_12,iPr_def_11),
inference(demodulation,[status(thm)],[c_7175,c_7035]) ).
tcf(c_7311,plain,
! [X0: $i] : iPr_def_10(X0,iPr_def_11,inverse(iPr_def_11)) = iPr_def_10(X0,iPr_def_12,iPr_def_11),
inference(light_normalisation,[status(thm)],[c_7310,c_4538]) ).
tcf(c_7374,plain,
! [X0: $i,X1: $i] : iPr_def_10(inverse(multiply(X0,inverse(X1))),X0,iPr_def_11) = inverse(multiply(inverse(iPr_def_11),multiply(iPr_def_12,X1))),
inference(demodulation,[status(thm)],[c_7150,c_457]) ).
tcf(c_7512,plain,
inverse(multiply(iPr_def_11,multiply(iPr_def_11,multiply(iPr_def_11,iPr_def_12)))) = iPr_def_12,
inference(superposition,[status(thm)],[c_7021,c_124]) ).
tcf(c_7547,plain,
multiply(multiply(iPr_def_11,iPr_def_11),multiply(iPr_def_11,iPr_def_11)) = iPr_def_12,
inference(superposition,[status(thm)],[c_7289,c_3794]) ).
tcf(c_7552,plain,
! [X0: $i] : iPr_def_10(inverse(multiply(X0,inverse(iPr_def_11))),X0,iPr_def_11) = multiply(inverse(iPr_def_11),iPr_def_11),
inference(superposition,[status(thm)],[c_7122,c_312]) ).
tcf(c_7558,plain,
multiply(iPr_def_11,inverse(inverse(iPr_def_11))) = iPr_def_10(iPr_def_11,inverse(iPr_def_11),iPr_def_11),
inference(superposition,[status(thm)],[c_7122,c_467]) ).
tcf(c_7559,plain,
iPr_def_10(inverse(inverse(iPr_def_11)),iPr_def_11,inverse(iPr_def_11)) = iPr_def_11,
inference(superposition,[status(thm)],[c_7122,c_312]) ).
tcf(c_7577,plain,
multiply(inverse(iPr_def_11),iPr_def_12) = iPr_def_11,
inference(superposition,[status(thm)],[c_7122,c_4292]) ).
tcf(c_7578,plain,
inverse(inverse(iPr_def_11)) = iPr_def_12,
inference(superposition,[status(thm)],[c_7122,c_3793]) ).
tcf(c_7596,plain,
iPr_def_10(inverse(inverse(multiply(iPr_def_11,iPr_def_12))),iPr_def_11,iPr_def_11) = iPr_def_11,
inference(superposition,[status(thm)],[c_4342,c_312]) ).
tcf(c_7645,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_10(inverse(multiply(X0,multiply(iPr_def_11,X1))),X0,multiply(X2,inverse(X2))) = inverse(multiply(inverse(X1),multiply(inverse(iPr_def_11),iPr_def_11))),
inference(superposition,[status(thm)],[c_4556,c_454]) ).
tcf(c_7659,plain,
! [X0: $i] : multiply(iPr_def_11,multiply(inverse(iPr_def_11),multiply(iPr_def_11,X0))) = X0,
inference(superposition,[status(thm)],[c_4556,c_312]) ).
tcf(c_7671,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(X0,multiply(X1,iPr_def_10(X2,X0,X1))) = inverse(multiply(X2,multiply(inverse(iPr_def_11),iPr_def_11))),
inference(superposition,[status(thm)],[c_124,c_4558]) ).
tcf(c_7673,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] : multiply(iPr_def_10(X0,inverse(multiply(X1,multiply(X2,X3))),X4),multiply(multiply(multiply(X5,inverse(X5)),X0),iPr_def_10(X1,X2,X3))) = inverse(multiply(X4,multiply(inverse(iPr_def_11),iPr_def_11))),
inference(superposition,[status(thm)],[c_451,c_4558]) ).
tcf(c_7687,plain,
! [X0: $i] : inverse(multiply(X0,multiply(inverse(iPr_def_11),iPr_def_11))) = multiply(inverse(X0),multiply(inverse(iPr_def_11),iPr_def_11)),
inference(superposition,[status(thm)],[c_4558,c_4558]) ).
tcf(c_7756,plain,
iPr_def_10(inverse(inverse(iPr_def_11)),iPr_def_12,iPr_def_11) = iPr_def_11,
inference(demodulation,[status(thm)],[c_7559,c_7311]) ).
tcf(c_7757,plain,
iPr_def_10(inverse(iPr_def_11),inverse(iPr_def_11),iPr_def_12) = iPr_def_12,
inference(demodulation,[status(thm)],[c_7512,c_2871]) ).
tcf(c_7758,plain,
multiply(iPr_def_11,inverse(inverse(iPr_def_11))) = multiply(iPr_def_11,iPr_def_12),
inference(demodulation,[status(thm)],[c_7558,c_3798]) ).
tcf(c_7767,plain,
inverse(multiply(inverse(iPr_def_11),multiply(iPr_def_12,iPr_def_11))) = multiply(inverse(iPr_def_11),iPr_def_11),
inference(demodulation,[status(thm)],[c_7552,c_7374]) ).
tcf(c_7768,plain,
inverse(multiply(inverse(iPr_def_11),iPr_def_11)) = multiply(inverse(iPr_def_11),iPr_def_11),
inference(light_normalisation,[status(thm)],[c_7767,c_4538]) ).
tcf(c_7781,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(X0,multiply(X1,iPr_def_10(X2,X0,X1))) = multiply(inverse(X2),multiply(inverse(iPr_def_11),iPr_def_11)),
inference(demodulation,[status(thm)],[c_7671,c_7687]) ).
tcf(c_7809,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_10(inverse(multiply(X0,multiply(iPr_def_11,X1))),X0,multiply(X2,inverse(X2))) = multiply(inverse(inverse(X1)),multiply(inverse(iPr_def_11),iPr_def_11)),
inference(demodulation,[status(thm)],[c_7645,c_7687]) ).
tcf(c_7810,plain,
! [X0: $i] : multiply(inverse(inverse(X0)),multiply(inverse(iPr_def_11),iPr_def_11)) = X0,
inference(demodulation,[status(thm)],[c_7809,c_312,c_457]) ).
tcf(c_7866,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] : multiply(iPr_def_10(X0,inverse(multiply(X1,multiply(X2,X3))),X4),multiply(multiply(multiply(X5,inverse(X5)),X0),iPr_def_10(X1,X2,X3))) = multiply(inverse(X4),multiply(inverse(iPr_def_11),iPr_def_11)),
inference(demodulation,[status(thm)],[c_7673,c_7687]) ).
tcf(c_7867,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] : multiply(iPr_def_10(X0,inverse(multiply(X1,multiply(X2,X3))),X4),multiply(multiply(iPr_def_11,X0),iPr_def_10(X1,X2,X3))) = multiply(inverse(X4),multiply(inverse(iPr_def_11),iPr_def_11)),
inference(demodulation,[status(thm)],[c_7866,c_457]) ).
tcf(c_8606,plain,
iPr_def_10(inverse(iPr_def_11),iPr_def_12,iPr_def_11) = multiply(iPr_def_11,iPr_def_12),
inference(superposition,[status(thm)],[c_7578,c_3798]) ).
tcf(c_8607,plain,
inverse(multiply(inverse(iPr_def_11),multiply(iPr_def_12,iPr_def_11))) = iPr_def_12,
inference(superposition,[status(thm)],[c_7578,c_3793]) ).
tcf(c_8610,plain,
! [X0: $i] : iPr_def_10(X0,inverse(iPr_def_11),iPr_def_12) = iPr_def_10(X0,iPr_def_12,iPr_def_11),
inference(superposition,[status(thm)],[c_7578,c_7028]) ).
tcf(c_8630,plain,
! [X0: $i,X1: $i] : iPr_def_10(inverse(multiply(X0,iPr_def_12)),X0,multiply(X1,inverse(X1))) = inverse(multiply(inverse(iPr_def_11),multiply(inverse(iPr_def_11),iPr_def_12))),
inference(superposition,[status(thm)],[c_7757,c_454]) ).
tcf(c_8673,plain,
multiply(multiply(iPr_def_11,multiply(multiply(iPr_def_11,iPr_def_11),multiply(iPr_def_11,iPr_def_11))),multiply(iPr_def_11,inverse(inverse(iPr_def_11)))) = iPr_def_11,
inference(superposition,[status(thm)],[c_7299,c_975]) ).
tcf(c_8725,plain,
! [X0: $i] : iPr_def_10(inverse(X0),iPr_def_11,inverse(iPr_def_11)) = multiply(iPr_def_11,X0),
inference(superposition,[status(thm)],[c_7659,c_312]) ).
tcf(c_8799,plain,
! [X0: $i] : multiply(inverse(iPr_def_12),multiply(inverse(iPr_def_11),iPr_def_11)) = multiply(X0,multiply(inverse(X0),iPr_def_11)),
inference(superposition,[status(thm)],[c_3793,c_7810]) ).
tcf(c_8876,plain,
multiply(inverse(iPr_def_11),iPr_def_11) = iPr_def_12,
inference(light_normalisation,[status(thm)],[c_8607,c_4538,c_7768]) ).
tcf(c_8877,plain,
multiply(iPr_def_11,iPr_def_12) = inverse(iPr_def_11),
inference(demodulation,[status(thm)],[c_8606,c_4550]) ).
tcf(c_8882,plain,
! [X0: $i] : iPr_def_10(inverse(X0),iPr_def_12,iPr_def_11) = multiply(iPr_def_11,X0),
inference(demodulation,[status(thm)],[c_8725,c_7028]) ).
tcf(c_8905,plain,
! [X0: $i] : multiply(X0,multiply(inverse(X0),iPr_def_11)) = inverse(iPr_def_11),
inference(light_normalisation,[status(thm)],[c_8799,c_4539,c_7122]) ).
tcf(c_8956,plain,
multiply(multiply(iPr_def_11,iPr_def_12),multiply(iPr_def_11,iPr_def_12)) = iPr_def_11,
inference(light_normalisation,[status(thm)],[c_8673,c_7547,c_7758]) ).
tcf(c_8972,plain,
! [X0: $i] : inverse(multiply(inverse(iPr_def_11),multiply(inverse(iPr_def_11),iPr_def_12))) = iPr_def_10(inverse(multiply(X0,iPr_def_12)),X0,iPr_def_11),
inference(demodulation,[status(thm)],[c_8630,c_457]) ).
tcf(c_8973,plain,
! [X0: $i] : iPr_def_10(inverse(multiply(X0,iPr_def_12)),X0,iPr_def_11) = multiply(inverse(iPr_def_11),iPr_def_11),
inference(light_normalisation,[status(thm)],[c_8972,c_7577,c_7768]) ).
tcf(c_9070,plain,
iPr_def_10(inverse(iPr_def_11),iPr_def_12,iPr_def_11) = iPr_def_12,
inference(demodulation,[status(thm)],[c_7757,c_8610]) ).
tcf(c_9071,plain,
multiply(iPr_def_11,iPr_def_11) = iPr_def_12,
inference(demodulation,[status(thm)],[c_9070,c_8882]) ).
tcf(c_9075,plain,
inverse(multiply(iPr_def_11,iPr_def_12)) = multiply(iPr_def_11,iPr_def_12),
inference(demodulation,[status(thm)],[c_4342,c_9071]) ).
tcf(c_9076,plain,
multiply(multiply(iPr_def_12,iPr_def_12),iPr_def_12) = iPr_def_11,
inference(demodulation,[status(thm)],[c_7272,c_9071]) ).
tcf(c_9078,plain,
inverse(multiply(iPr_def_12,iPr_def_12)) = iPr_def_12,
inference(demodulation,[status(thm)],[c_7022,c_9071]) ).
tcf(c_9079,plain,
iPr_def_10(inverse(multiply(iPr_def_11,iPr_def_12)),iPr_def_11,iPr_def_11) = iPr_def_11,
inference(demodulation,[status(thm)],[c_7596,c_9075]) ).
tcf(c_9080,plain,
multiply(inverse(iPr_def_11),iPr_def_11) = iPr_def_11,
inference(demodulation,[status(thm)],[c_9079,c_8973]) ).
tcf(c_9081,plain,
! [X0: $i] : multiply(inverse(inverse(X0)),iPr_def_11) = X0,
inference(demodulation,[status(thm)],[c_7810,c_9080]) ).
tcf(c_9083,plain,
inverse(iPr_def_11) = iPr_def_11,
inference(demodulation,[status(thm)],[c_7768,c_9080]) ).
tcf(c_9084,plain,
multiply(iPr_def_11,iPr_def_11) = inverse(iPr_def_11),
inference(demodulation,[status(thm)],[c_7122,c_9080]) ).
tcf(c_9087,plain,
! [X0: $i] : multiply(iPr_def_11,multiply(iPr_def_11,multiply(iPr_def_11,X0))) = X0,
inference(demodulation,[status(thm)],[c_7659,c_9083]) ).
tcf(c_9090,plain,
iPr_def_10(inverse(iPr_def_11),iPr_def_12,iPr_def_11) = iPr_def_11,
inference(demodulation,[status(thm)],[c_7756,c_9083]) ).
tcf(c_9095,plain,
! [X0: $i] : iPr_def_10(X0,inverse(X0),iPr_def_11) = iPr_def_11,
inference(demodulation,[status(thm)],[c_4541,c_9083]) ).
tcf(c_9102,plain,
multiply(iPr_def_11,iPr_def_11) = iPr_def_11,
inference(demodulation,[status(thm)],[c_9090,c_8882]) ).
tcf(c_9830,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : multiply(multiply(X0,inverse(X0)),inverse(multiply(X1,iPr_def_10(X2,iPr_def_11,iPr_def_11)))) = iPr_def_10(X1,multiply(X3,inverse(X3)),inverse(multiply(X2,iPr_def_12))),
inference(superposition,[status(thm)],[c_9071,c_186]) ).
tcf(c_9836,plain,
! [X0: $i] : inverse(iPr_def_10(X0,inverse(iPr_def_12),iPr_def_11)) = multiply(iPr_def_11,X0),
inference(superposition,[status(thm)],[c_9071,c_2649]) ).
tcf(c_9837,plain,
! [X0: $i] : iPr_def_10(inverse(iPr_def_12),iPr_def_11,X0) = inverse(X0),
inference(superposition,[status(thm)],[c_9071,c_928]) ).
tcf(c_9843,plain,
iPr_def_11 = iPr_def_12,
inference(demodulation,[status(thm)],[c_9071,c_9102]) ).
tcf(c_9844,plain,
! [X0: $i] : iPr_def_10(iPr_def_11,iPr_def_11,X0) = inverse(X0),
inference(light_normalisation,[status(thm)],[c_9837,c_4539]) ).
tcf(c_9849,plain,
! [X0: $i] : inverse(iPr_def_10(X0,iPr_def_11,iPr_def_11)) = multiply(iPr_def_11,X0),
inference(light_normalisation,[status(thm)],[c_9836,c_4539]) ).
tcf(c_9863,plain,
! [X0: $i,X1: $i] : iPr_def_10(X0,iPr_def_11,inverse(multiply(X1,multiply(iPr_def_11,iPr_def_11)))) = iPr_def_10(X0,iPr_def_11,inverse(multiply(X1,iPr_def_12))),
inference(demodulation,[status(thm)],[c_9830,c_457,c_935]) ).
tcf(c_9864,plain,
! [X0: $i,X1: $i] : iPr_def_10(X0,iPr_def_11,inverse(multiply(X1,iPr_def_11))) = iPr_def_10(X0,iPr_def_11,inverse(multiply(X1,iPr_def_12))),
inference(light_normalisation,[status(thm)],[c_9863,c_9083,c_9084]) ).
tcf(c_9950,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : multiply(multiply(X0,inverse(X0)),inverse(multiply(X1,iPr_def_10(X2,inverse(iPr_def_11),iPr_def_11)))) = iPr_def_10(X1,multiply(X3,inverse(X3)),inverse(multiply(X2,iPr_def_12))),
inference(superposition,[status(thm)],[c_8876,c_186]) ).
tcf(c_9991,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] : inverse(multiply(iPr_def_10(X0,inverse(multiply(X1,multiply(X2,X3))),X4),multiply(multiply(multiply(multiply(iPr_def_12,iPr_def_12),iPr_def_12),X0),iPr_def_10(X1,X2,X3)))) = X4,
inference(superposition,[status(thm)],[c_9078,c_451]) ).
tcf(c_10074,plain,
! [X0: $i,X1: $i] : iPr_def_10(X0,iPr_def_11,multiply(inverse(X1),multiply(inverse(iPr_def_11),iPr_def_11))) = iPr_def_10(X0,iPr_def_11,inverse(multiply(X1,iPr_def_11))),
inference(demodulation,[status(thm)],[c_9950,c_457,c_935,c_7687,c_9864]) ).
tcf(c_10075,plain,
! [X0: $i,X1: $i] : iPr_def_10(X0,iPr_def_11,inverse(multiply(X1,iPr_def_11))) = iPr_def_10(X0,iPr_def_11,multiply(inverse(X1),iPr_def_11)),
inference(light_normalisation,[status(thm)],[c_10074,c_9083,c_9084]) ).
tcf(c_10076,plain,
! [X0: $i] : inverse(multiply(inverse(X0),iPr_def_11)) = X0,
inference(light_normalisation,[status(thm)],[c_9991,c_7867,c_9076,c_9083,c_9084]) ).
tcf(c_10251,plain,
! [X0: $i,X1: $i] : multiply(iPr_def_11,inverse(multiply(X0,X1))) = iPr_def_10(X0,inverse(inverse(X1)),iPr_def_11),
inference(superposition,[status(thm)],[c_9081,c_467]) ).
tcf(c_10284,plain,
! [X0: $i] : iPr_def_10(iPr_def_11,iPr_def_11,multiply(iPr_def_11,X0)) = multiply(iPr_def_11,inverse(X0)),
inference(superposition,[status(thm)],[c_9095,c_480]) ).
tcf(c_10320,plain,
! [X0: $i] : inverse(multiply(iPr_def_11,X0)) = multiply(iPr_def_11,inverse(X0)),
inference(demodulation,[status(thm)],[c_10284,c_9844]) ).
tcf(c_10437,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_10(X0,inverse(inverse(multiply(X1,X2))),iPr_def_11) = iPr_def_10(X0,X1,X2),
inference(demodulation,[status(thm)],[c_467,c_10251]) ).
tcf(c_10469,plain,
! [X0: $i] : inverse(multiply(X0,iPr_def_11)) = multiply(inverse(X0),iPr_def_11),
inference(superposition,[status(thm)],[c_10076,c_10076]) ).
tcf(c_10478,plain,
! [X0: $i,X1: $i] : iPr_def_10(X0,inverse(X0),X1) = inverse(X1),
inference(superposition,[status(thm)],[c_10076,c_928]) ).
tcf(c_10536,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i] : inverse(multiply(iPr_def_11,multiply(iPr_def_11,multiply(multiply(multiply(X0,multiply(X1,multiply(multiply(multiply(X2,multiply(X3,iPr_def_10(X4,X2,X3))),X4),inverse(multiply(X5,multiply(X0,X1)))))),X5),inverse(multiply(X6,iPr_def_11)))))) = X6,
inference(superposition,[status(thm)],[c_9102,c_117]) ).
tcf(c_10540,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i] : inverse(multiply(iPr_def_11,multiply(iPr_def_12,multiply(multiply(multiply(X0,multiply(X1,multiply(multiply(multiply(X2,multiply(X3,iPr_def_10(X4,X2,X3))),X4),inverse(multiply(X5,multiply(X0,X1)))))),X5),inverse(multiply(X6,inverse(iPr_def_11))))))) = X6,
inference(superposition,[status(thm)],[c_8877,c_117]) ).
tcf(c_10654,plain,
! [X0: $i] : multiply(inverse(X0),X0) = inverse(iPr_def_11),
inference(superposition,[status(thm)],[c_9081,c_8905]) ).
tcf(c_10669,plain,
! [X0: $i,X1: $i] : iPr_def_10(inverse(multiply(X0,inverse(iPr_def_11))),X0,X1) = multiply(inverse(X1),iPr_def_11),
inference(superposition,[status(thm)],[c_8905,c_312]) ).
tcf(c_10698,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : multiply(multiply(X0,inverse(X0)),inverse(multiply(X1,iPr_def_10(X2,multiply(iPr_def_11,iPr_def_12),multiply(iPr_def_11,iPr_def_12))))) = iPr_def_10(X1,multiply(X3,inverse(X3)),inverse(multiply(X2,iPr_def_11))),
inference(superposition,[status(thm)],[c_8956,c_186]) ).
tcf(c_10721,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i] : inverse(multiply(iPr_def_11,multiply(multiply(iPr_def_11,X0),multiply(multiply(multiply(X1,multiply(X2,multiply(multiply(multiply(X3,multiply(X4,iPr_def_10(X5,X3,X4))),X5),inverse(multiply(X6,multiply(X1,X2)))))),X6),inverse(X0))))) = iPr_def_11,
inference(superposition,[status(thm)],[c_9087,c_117]) ).
tcf(c_10742,plain,
! [X0: $i] : multiply(inverse(X0),X0) = iPr_def_11,
inference(light_normalisation,[status(thm)],[c_10654,c_9083]) ).
tcf(c_10813,plain,
! [X0: $i] : multiply(inverse(X0),iPr_def_11) = inverse(X0),
inference(light_normalisation,[status(thm)],[c_10669,c_928,c_9083]) ).
tcf(c_10960,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : multiply(multiply(X0,inverse(X0)),inverse(multiply(X1,iPr_def_10(X2,multiply(iPr_def_11,iPr_def_12),multiply(iPr_def_11,iPr_def_12))))) = iPr_def_10(X1,multiply(X3,inverse(X3)),inverse(X2)),
inference(demodulation,[status(thm)],[c_10698,c_10469,c_10813]) ).
tcf(c_10961,plain,
! [X0: $i,X1: $i] : iPr_def_10(X0,iPr_def_11,inverse(multiply(X1,multiply(multiply(iPr_def_11,iPr_def_12),multiply(iPr_def_11,iPr_def_12))))) = iPr_def_10(X0,iPr_def_11,inverse(X1)),
inference(demodulation,[status(thm)],[c_10960,c_457,c_935]) ).
tcf(c_10962,plain,
! [X0: $i,X1: $i] : iPr_def_10(X0,iPr_def_11,multiply(inverse(X1),iPr_def_11)) = iPr_def_10(X0,iPr_def_11,inverse(X1)),
inference(light_normalisation,[status(thm)],[c_10961,c_8956,c_10075]) ).
tcf(c_11008,plain,
! [X0: $i] : iPr_def_10(multiply(iPr_def_11,X0),iPr_def_11,inverse(X0)) = iPr_def_11,
inference(demodulation,[status(thm)],[c_10721,c_7233,c_7781,c_10251,c_10320,c_10437]) ).
tcf(c_11021,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i] : inverse(multiply(iPr_def_11,multiply(iPr_def_11,multiply(multiply(multiply(X0,multiply(X1,multiply(multiply(multiply(X2,multiply(X3,iPr_def_10(X4,X2,X3))),X4),inverse(multiply(X5,multiply(X0,X1)))))),X5),inverse(X6))))) = X6,
inference(demodulation,[status(thm)],[c_10536,c_10469,c_10813]) ).
tcf(c_11022,plain,
! [X0: $i] : inverse(inverse(X0)) = X0,
inference(demodulation,[status(thm)],[c_11021,c_7233,c_7781,c_9844,c_10251,c_10320,c_10437]) ).
tcf(c_11034,plain,
! [X0: $i] : iPr_def_10(iPr_def_12,iPr_def_11,inverse(multiply(X0,inverse(iPr_def_11)))) = X0,
inference(demodulation,[status(thm)],[c_10540,c_7233,c_7781,c_10251,c_10320,c_10437]) ).
tcf(c_11035,plain,
! [X0: $i] : iPr_def_10(iPr_def_11,iPr_def_11,inverse(multiply(X0,iPr_def_11))) = X0,
inference(light_normalisation,[status(thm)],[c_11034,c_9083,c_9843]) ).
tcf(c_11036,plain,
! [X0: $i] : inverse(inverse(multiply(X0,iPr_def_11))) = X0,
inference(demodulation,[status(thm)],[c_11035,c_9844]) ).
tcf(c_11188,plain,
! [X0: $i,X1: $i] : iPr_def_10(multiply(inverse(X0),iPr_def_11),X0,X1) = inverse(X1),
inference(demodulation,[status(thm)],[c_928,c_10469]) ).
tcf(c_11193,plain,
! [X0: $i,X1: $i] : iPr_def_10(inverse(X0),X0,X1) = inverse(X1),
inference(demodulation,[status(thm)],[c_11188,c_10813]) ).
tcf(c_11847,plain,
! [X0: $i,X1: $i] : iPr_def_10(inverse(iPr_def_11),inverse(multiply(X0,X1)),X0) = X1,
inference(superposition,[status(thm)],[c_10742,c_312]) ).
tcf(c_11881,plain,
! [X0: $i] : multiply(X0,iPr_def_11) = X0,
inference(superposition,[status(thm)],[c_11036,c_11022]) ).
tcf(c_11926,plain,
! [X0: $i,X1: $i] : inverse(iPr_def_10(X0,inverse(X1),X1)) = multiply(iPr_def_11,X0),
inference(superposition,[status(thm)],[c_11193,c_479]) ).
tcf(c_11983,plain,
! [X0: $i] : multiply(multiply(iPr_def_11,X0),iPr_def_10(X0,iPr_def_11,iPr_def_11)) = iPr_def_11,
inference(superposition,[status(thm)],[c_9849,c_10742]) ).
tcf(c_12022,plain,
! [X0: $i,X1: $i] : iPr_def_10(iPr_def_11,inverse(multiply(X0,X1)),X0) = X1,
inference(light_normalisation,[status(thm)],[c_11847,c_9083]) ).
tcf(c_12265,plain,
! [X0: $i,X1: $i] : iPr_def_10(multiply(iPr_def_11,inverse(multiply(X0,X1))),iPr_def_11,X0) = X1,
inference(superposition,[status(thm)],[c_10320,c_312]) ).
tcf(c_12403,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i] : multiply(X0,multiply(multiply(multiply(X1,multiply(X2,multiply(multiply(multiply(X3,multiply(X4,iPr_def_10(X5,X3,X4))),X5),inverse(multiply(X6,multiply(X1,X2)))))),X6),inverse(multiply(X7,multiply(X8,X0))))) = iPr_def_10(iPr_def_11,X7,X8),
inference(superposition,[status(thm)],[c_117,c_12022]) ).
tcf(c_12592,plain,
! [X0: $i,X1: $i] : iPr_def_10(iPr_def_10(X0,X1,iPr_def_11),iPr_def_11,X0) = X1,
inference(demodulation,[status(thm)],[c_12265,c_10251,c_11022]) ).
tcf(c_12695,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(X0,iPr_def_10(X1,X2,X0)) = iPr_def_10(iPr_def_11,X1,X2),
inference(demodulation,[status(thm)],[c_12403,c_7781,c_10251,c_10437,c_10742,c_11881]) ).
tcf(c_13638,plain,
! [X0: $i] : inverse(inverse(X0)) = multiply(iPr_def_11,X0),
inference(superposition,[status(thm)],[c_10478,c_11926]) ).
tcf(c_13654,plain,
! [X0: $i,X1: $i] : iPr_def_10(multiply(iPr_def_11,iPr_def_10(X0,inverse(X1),X1)),iPr_def_11,multiply(iPr_def_11,X0)) = iPr_def_11,
inference(superposition,[status(thm)],[c_11926,c_11008]) ).
tcf(c_13660,plain,
! [X0: $i,X1: $i] : iPr_def_10(X0,inverse(X1),X1) = inverse(multiply(iPr_def_11,X0)),
inference(superposition,[status(thm)],[c_11926,c_11022]) ).
tcf(c_13696,plain,
! [X0: $i,X1: $i] : iPr_def_10(inverse(iPr_def_11),multiply(iPr_def_11,X0),multiply(X1,inverse(X1))) = inverse(multiply(X0,multiply(iPr_def_11,iPr_def_11))),
inference(superposition,[status(thm)],[c_11983,c_454]) ).
tcf(c_13741,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : iPr_def_10(X0,multiply(X1,inverse(X1)),inverse(multiply(inverse(multiply(X2,iPr_def_11)),multiply(iPr_def_12,iPr_def_11)))) = multiply(multiply(X3,inverse(X3)),inverse(multiply(X0,inverse(inverse(X2))))),
inference(superposition,[status(thm)],[c_7027,c_186]) ).
tcf(c_13866,plain,
! [X0: $i] : multiply(iPr_def_11,X0) = X0,
inference(demodulation,[status(thm)],[c_13638,c_11022]) ).
tcf(c_13948,plain,
! [X0: $i,X1: $i] : iPr_def_10(X0,inverse(X1),X1) = inverse(X0),
inference(demodulation,[status(thm)],[c_13660,c_13866]) ).
tcf(c_14075,plain,
! [X0: $i] : iPr_def_10(inverse(X0),iPr_def_11,X0) = iPr_def_11,
inference(demodulation,[status(thm)],[c_13654,c_13866,c_13948]) ).
tcf(c_14129,plain,
! [X0: $i,X1: $i] : iPr_def_10(inverse(iPr_def_11),X0,multiply(X1,inverse(X1))) = inverse(multiply(X0,iPr_def_11)),
inference(demodulation,[status(thm)],[c_13696,c_13866]) ).
tcf(c_14130,plain,
! [X0: $i] : iPr_def_10(inverse(iPr_def_11),X0,iPr_def_11) = inverse(X0),
inference(demodulation,[status(thm)],[c_14129,c_457,c_11881]) ).
tcf(c_14131,plain,
! [X0: $i] : iPr_def_10(iPr_def_11,X0,iPr_def_11) = inverse(X0),
inference(light_normalisation,[status(thm)],[c_14130,c_9083]) ).
tcf(c_14248,plain,
! [X0: $i,X1: $i] : iPr_def_10(X0,X1,iPr_def_11) = iPr_def_10(X0,iPr_def_11,X1),
inference(demodulation,[status(thm)],[c_13741,c_457,c_9864,c_10075,c_10251,c_10962,c_11022,c_11881]) ).
tcf(c_14310,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_10(iPr_def_10(X0,X1,X2),multiply(iPr_def_11,X0),multiply(iPr_def_11,X1)) = X2,
inference(demodulation,[status(thm)],[c_478,c_13866]) ).
tcf(c_14311,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_10(X0,iPr_def_10(X1,X2,X0),multiply(iPr_def_11,X1)) = X2,
inference(demodulation,[status(thm)],[c_480,c_13866]) ).
tcf(c_14312,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_10(X0,X1,iPr_def_10(X2,X0,X1)) = X2,
inference(demodulation,[status(thm)],[c_479,c_13866]) ).
tcf(c_14345,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_10(X0,iPr_def_10(X1,X2,X0),X1) = X2,
inference(demodulation,[status(thm)],[c_14311,c_13866]) ).
tcf(c_14346,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_10(iPr_def_10(X0,X1,X2),X0,X1) = X2,
inference(demodulation,[status(thm)],[c_14310,c_13866]) ).
tcf(c_14467,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : inverse(multiply(iPr_def_11,multiply(iPr_def_10(X0,X1,X2),multiply(multiply(X3,inverse(X3)),iPr_def_11)))) = multiply(X0,multiply(X1,X2)),
inference(superposition,[status(thm)],[c_14075,c_452]) ).
tcf(c_14609,plain,
! [X0: $i,X1: $i,X2: $i] : inverse(multiply(X0,multiply(X1,X2))) = iPr_def_10(X0,X1,X2),
inference(superposition,[status(thm)],[c_312,c_14312]) ).
tcf(c_14624,plain,
! [X0: $i,X1: $i] : iPr_def_10(X0,X1,iPr_def_11) = iPr_def_10(iPr_def_11,X0,X1),
inference(superposition,[status(thm)],[c_12592,c_14312]) ).
tcf(c_14655,plain,
! [X0: $i,X1: $i] : inverse(multiply(X0,X1)) = iPr_def_10(X0,X1,iPr_def_11),
inference(superposition,[status(thm)],[c_12022,c_14345]) ).
tcf(c_14698,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_10(X0,multiply(X1,X2),iPr_def_11) = iPr_def_10(X0,X1,X2),
inference(demodulation,[status(thm)],[c_14609,c_14655]) ).
tcf(c_14699,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_10(X0,iPr_def_11,multiply(X1,X2)) = iPr_def_10(X0,X1,X2),
inference(demodulation,[status(thm)],[c_14698,c_14248]) ).
tcf(c_14753,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : iPr_def_10(iPr_def_11,iPr_def_10(X0,X1,X2),multiply(multiply(X3,inverse(X3)),iPr_def_11)) = multiply(X0,multiply(X1,X2)),
inference(demodulation,[status(thm)],[c_14467,c_14655,c_14624,c_14699]) ).
tcf(c_14754,plain,
! [X0: $i,X1: $i,X2: $i] : inverse(iPr_def_10(X0,X1,X2)) = multiply(X0,multiply(X1,X2)),
inference(demodulation,[status(thm)],[c_14753,c_457,c_11881,c_14131]) ).
tcf(c_19654,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(multiply(X0,X1),iPr_def_10(X2,X0,X1)) = iPr_def_10(iPr_def_11,X2,iPr_def_11),
inference(superposition,[status(thm)],[c_14699,c_12695]) ).
tcf(c_19853,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(multiply(X0,X1),iPr_def_10(X2,X0,X1)) = inverse(X2),
inference(demodulation,[status(thm)],[c_19654,c_14131]) ).
tcf(c_21173,plain,
! [X0: $i,X1: $i,X2: $i] : inverse(iPr_def_10(X0,X1,X2)) = multiply(multiply(X0,X1),X2),
inference(superposition,[status(thm)],[c_14346,c_19853]) ).
tcf(c_21283,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(multiply(X0,X1),X2) = multiply(X0,multiply(X1,X2)),
inference(demodulation,[status(thm)],[c_21173,c_14754]) ).
tcf(c_21433,plain,
$false,
inference(backward_subsumption_resolution,[status(thm)],[c_52,c_21283]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP444-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.10/0.36 % Computer : n014.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Wed Sep 23 14:46:33 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.36 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.10/0.40 Running UEQ theorem proving
% 0.10/0.40 Running: /export/starexec/sandbox2/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s ueq_schedule -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.41
% 0.10/0.41 % ======== iProver multi-core TPTP/SMT =========
% 0.10/0.41
% 0.10/0.41 % Detected problem language: tptp
% 0.10/0.42 % Proving...
% 5.58/3.61 WARNING - Clausifier option not provided in the heuristic config "heur/vip2_118404", setting default options.
% 5.58/3.61 % SZS status Started for theBenchmark.p
% 5.58/3.61 % SZS status Unsatisfiable for theBenchmark.p
% 5.58/3.61
% 5.58/3.61 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 5.58/3.61
% 5.58/3.61 % ------ iProver source info
% 5.58/3.61
% 5.58/3.61 % git: date: 2026-07-19 20:42:38 +0200
% 5.58/3.61 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 5.58/3.61 % git: non_committed_changes: false
% 5.58/3.61
% 5.58/3.61 % ------ Parsing...% successful
% 5.58/3.61
% 5.58/3.61
% 5.58/3.61 % ------ Clausification by vclausify_rel & Parsing by iProver...
% 5.58/3.61 % ------ Proving...
% 5.58/3.61 % ------ Problem Properties
% 5.58/3.61
% 5.58/3.61 %
% 5.58/3.61 % clauses 2
% 5.58/3.61 % conjectures 1
% 5.58/3.61 % EPR 0
% 5.58/3.61 % Horn 2
% 5.58/3.61 % unary 2
% 5.58/3.61 % binary 0
% 5.58/3.61 % lits 2
% 5.58/3.61 % lits eq 2
% 5.58/3.61 % fd_pure 0
% 5.58/3.61 % fd_pseudo 0
% 5.58/3.61 % fd_cond 0
% 5.58/3.61 % fd_pseudo_cond 0
% 5.58/3.61 % AC symbols 0
% 5.58/3.61
% 5.58/3.61 % ------ Input Options Time Limit: Unbounded
% 5.58/3.61
% 5.58/3.61
% 5.58/3.61 % ------
% 5.58/3.61 % Current options:
% 5.58/3.61 % ------
% 5.58/3.61
% 5.58/3.61
% 5.58/3.61 %
% 5.58/3.61
% 5.58/3.61 % ------ Proving...
% 5.58/3.61 %
% 5.58/3.61
% 5.58/3.61 % SZS status Unsatisfiable for theBenchmark.p
% 5.58/3.61
% 5.58/3.61 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 5.58/3.62
% 5.58/3.62
%------------------------------------------------------------------------------