%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : GRP508-1 : TPTP v9.3.1. Bugfixed v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% Computer : n001.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:26 PM UTC 2026
% Result : Unsatisfiable 164.56s 23.29s
% Output : CNFRefutation 101.20s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats ran out of CPU time)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X2,X3,X0,X1,X4,X5] : multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,X1)),multiply(X1,X0))),multiply(inverse(multiply(X2,X3)),multiply(X2,inverse(multiply(multiply(X4,inverse(X5)),inverse(X3))))))),X5) = X4,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',single_axiom) ).
fof(f2,negated_conjecture,
multiply(a,b) != multiply(b,a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_these_axioms_4) ).
tcf(c_51,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] : multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,X1)),multiply(X1,X0))),multiply(inverse(multiply(X2,X3)),multiply(X2,inverse(multiply(multiply(X4,inverse(X5)),inverse(X3))))))),X5) = X4,
inference(cnf_transformation,[],[f1]) ).
tcf(c_52,negated_conjecture,
multiply(a,b) != multiply(b,a),
inference(cnf_transformation,[],[f2]) ).
tcf(c_62,definition,
iPr_def_10 = multiply(a,b),
introduced(definition,[new_symbols(definition,[iPr_def_10])],[]) ).
tcf(c_63,definition,
iPr_def_11 = multiply(b,a),
introduced(definition,[new_symbols(definition,[iPr_def_11])],[]) ).
tcf(c_64,negated_conjecture,
iPr_def_10 != iPr_def_11,
inference(demodulation,[status(thm)],[c_52,c_63,c_62]) ).
tcf(c_65,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] : multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,X1)),multiply(X1,X0))),multiply(inverse(multiply(X2,X3)),multiply(X2,inverse(multiply(multiply(X4,inverse(X5)),inverse(X3))))))),X5) = X4,
inference(demodulation,[status(thm)],[c_51]) ).
tcf(c_103,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : multiply(inverse(multiply(inverse(multiply(inverse(multiply(b,a)),iPr_def_10)),multiply(inverse(multiply(X0,X1)),multiply(X0,inverse(multiply(multiply(X2,inverse(X3)),inverse(X1))))))),X3) = X2,
inference(superposition,[status(thm)],[c_62,c_65]) ).
tcf(c_104,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : multiply(inverse(multiply(inverse(multiply(inverse(multiply(a,b)),iPr_def_11)),multiply(inverse(multiply(X0,X1)),multiply(X0,inverse(multiply(multiply(X2,inverse(X3)),inverse(X1))))))),X3) = X2,
inference(superposition,[status(thm)],[c_63,c_65]) ).
tcf(c_106,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,X1)),multiply(X1,X0))),multiply(inverse(iPr_def_10),multiply(a,inverse(multiply(multiply(X2,inverse(X3)),inverse(b))))))),X3) = X2,
inference(superposition,[status(thm)],[c_62,c_65]) ).
tcf(c_113,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i] : inverse(multiply(inverse(multiply(inverse(multiply(X0,X1)),multiply(X1,X0))),multiply(inverse(multiply(X2,X3)),multiply(X2,inverse(multiply(multiply(X4,inverse(inverse(X5))),inverse(X3))))))) = multiply(inverse(multiply(inverse(multiply(inverse(multiply(X6,X7)),multiply(X7,X6))),multiply(inverse(multiply(X8,X9)),multiply(X8,inverse(multiply(X4,inverse(X9))))))),X5),
inference(superposition,[status(thm)],[c_65,c_65]) ).
tcf(c_115,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : multiply(inverse(multiply(inverse(multiply(inverse(iPr_def_10),iPr_def_11)),multiply(inverse(multiply(X0,X1)),multiply(X0,inverse(multiply(multiply(X2,inverse(X3)),inverse(X1))))))),X3) = X2,
inference(demodulation,[status(thm)],[c_104,c_62]) ).
tcf(c_116,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : multiply(inverse(multiply(inverse(multiply(inverse(iPr_def_11),iPr_def_10)),multiply(inverse(multiply(X0,X1)),multiply(X0,inverse(multiply(multiply(X2,inverse(X3)),inverse(X1))))))),X3) = X2,
inference(demodulation,[status(thm)],[c_103,c_63]) ).
tcf(c_119,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] : multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,X1)),multiply(X1,X0))),multiply(inverse(multiply(X2,X3)),multiply(X2,inverse(multiply(X4,inverse(X3))))))),X5) = iPr_def_12(X4,X5),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_12])],[c_113]) ).
tcf(c_122,plain,
! [X0: $i,X1: $i] : iPr_def_12(multiply(X0,inverse(X1)),X1) = X0,
inference(demodulation,[status(thm)],[c_65,c_119]) ).
tcf(c_134,plain,
! [X0: $i,X1: $i] : multiply(inverse(multiply(inverse(multiply(inverse(iPr_def_10),iPr_def_11)),multiply(inverse(iPr_def_10),multiply(a,inverse(multiply(multiply(X0,inverse(X1)),inverse(b))))))),X1) = X0,
inference(superposition,[status(thm)],[c_62,c_115]) ).
tcf(c_141,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] : inverse(multiply(inverse(multiply(inverse(iPr_def_10),iPr_def_11)),multiply(inverse(multiply(X0,X1)),multiply(X0,inverse(multiply(multiply(X2,inverse(inverse(X3))),inverse(X1))))))) = multiply(inverse(multiply(inverse(multiply(inverse(iPr_def_10),iPr_def_11)),multiply(inverse(multiply(X4,X5)),multiply(X4,inverse(multiply(X2,inverse(X5))))))),X3),
inference(superposition,[status(thm)],[c_115,c_115]) ).
tcf(c_143,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : multiply(inverse(multiply(inverse(multiply(inverse(iPr_def_10),iPr_def_11)),multiply(inverse(multiply(X0,X1)),multiply(X0,inverse(multiply(X2,inverse(X1))))))),X3) = iPr_def_13(X2,X3),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_13])],[c_141]) ).
tcf(c_146,plain,
! [X0: $i,X1: $i] : iPr_def_13(multiply(X0,inverse(X1)),X1) = X0,
inference(demodulation,[status(thm)],[c_115,c_143]) ).
tcf(c_155,plain,
! [X0: $i,X1: $i] : inverse(multiply(inverse(multiply(inverse(iPr_def_10),iPr_def_11)),multiply(inverse(iPr_def_10),multiply(a,inverse(multiply(multiply(X0,inverse(inverse(X1))),inverse(b))))))) = multiply(inverse(multiply(inverse(multiply(inverse(iPr_def_10),iPr_def_11)),multiply(inverse(iPr_def_10),multiply(a,inverse(multiply(X0,inverse(b))))))),X1),
inference(superposition,[status(thm)],[c_134,c_134]) ).
tcf(c_176,plain,
! [X0: $i,X1: $i] : multiply(inverse(multiply(inverse(multiply(inverse(iPr_def_10),iPr_def_11)),multiply(inverse(iPr_def_10),multiply(a,inverse(multiply(X0,inverse(b))))))),X1) = iPr_def_13(X0,X1),
inference(superposition,[status(thm)],[c_62,c_143]) ).
tcf(c_182,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : iPr_def_13(inverse(multiply(inverse(multiply(inverse(iPr_def_10),iPr_def_11)),multiply(inverse(iPr_def_10),multiply(a,inverse(multiply(multiply(X0,inverse(inverse(X1))),inverse(b))))))),X2) = multiply(inverse(multiply(inverse(multiply(inverse(iPr_def_10),iPr_def_11)),multiply(inverse(multiply(X3,X1)),multiply(X3,inverse(X0))))),X2),
inference(superposition,[status(thm)],[c_134,c_143]) ).
tcf(c_185,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : multiply(inverse(multiply(inverse(multiply(inverse(iPr_def_10),iPr_def_11)),multiply(inverse(iPr_def_10),multiply(a,inverse(multiply(iPr_def_13(X0,inverse(X1)),inverse(b))))))),X1) = inverse(multiply(inverse(multiply(inverse(iPr_def_10),iPr_def_11)),multiply(inverse(multiply(X2,X3)),multiply(X2,inverse(multiply(X0,inverse(X3))))))),
inference(superposition,[status(thm)],[c_143,c_134]) ).
tcf(c_186,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : inverse(multiply(inverse(multiply(inverse(iPr_def_10),iPr_def_11)),multiply(inverse(multiply(X0,X1)),multiply(X0,inverse(multiply(X2,inverse(X1))))))) = iPr_def_13(iPr_def_13(X2,inverse(X3)),X3),
inference(superposition,[status(thm)],[c_143,c_146]) ).
tcf(c_191,plain,
! [X0: $i,X1: $i,X2: $i] : inverse(multiply(inverse(multiply(inverse(iPr_def_10),iPr_def_11)),multiply(inverse(multiply(X0,X1)),multiply(X0,inverse(multiply(X2,inverse(X1))))))) = iPr_def_14(X2),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_14])],[c_185]) ).
tcf(c_193,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : iPr_def_13(multiply(inverse(multiply(inverse(multiply(inverse(iPr_def_10),iPr_def_11)),multiply(inverse(iPr_def_10),multiply(a,inverse(multiply(X0,inverse(b))))))),X1),X2) = multiply(inverse(multiply(inverse(multiply(inverse(iPr_def_10),iPr_def_11)),multiply(inverse(multiply(X3,X1)),multiply(X3,inverse(X0))))),X2),
inference(light_normalisation,[status(thm)],[c_182,c_155]) ).
tcf(c_197,plain,
! [X0: $i,X1: $i] : multiply(iPr_def_14(X0),X1) = iPr_def_13(X0,X1),
inference(demodulation,[status(thm)],[c_143,c_191]) ).
tcf(c_234,plain,
! [X0: $i,X1: $i] : iPr_def_13(iPr_def_13(X0,inverse(X1)),X1) = iPr_def_14(X0),
inference(superposition,[status(thm)],[c_197,c_146]) ).
tcf(c_235,plain,
! [X0: $i,X1: $i] : iPr_def_12(iPr_def_13(X0,inverse(X1)),X1) = iPr_def_14(X0),
inference(superposition,[status(thm)],[c_197,c_122]) ).
tcf(c_238,plain,
! [X0: $i,X1: $i] : iPr_def_14(multiply(X0,inverse(inverse(X1)))) = iPr_def_13(X0,X1),
inference(superposition,[status(thm)],[c_146,c_234]) ).
tcf(c_243,plain,
! [X0: $i,X1: $i] : iPr_def_14(multiply(X0,inverse(inverse(X1)))) = iPr_def_12(X0,X1),
inference(superposition,[status(thm)],[c_146,c_235]) ).
tcf(c_244,plain,
! [X0: $i,X1: $i] : iPr_def_14(iPr_def_13(X0,inverse(inverse(X1)))) = iPr_def_12(iPr_def_14(X0),X1),
inference(superposition,[status(thm)],[c_234,c_235]) ).
tcf(c_247,plain,
! [X0: $i,X1: $i] : iPr_def_12(X0,X1) = iPr_def_13(X0,X1),
inference(light_normalisation,[status(thm)],[c_238,c_243]) ).
tcf(c_248,plain,
! [X0: $i,X1: $i] : multiply(iPr_def_14(X0),X1) = iPr_def_12(X0,X1),
inference(demodulation,[status(thm)],[c_197,c_247]) ).
tcf(c_250,plain,
! [X0: $i,X1: $i] : iPr_def_13(iPr_def_12(X0,inverse(X1)),X1) = iPr_def_14(X0),
inference(demodulation,[status(thm)],[c_234,c_247]) ).
tcf(c_252,plain,
! [X0: $i,X1: $i] : iPr_def_12(iPr_def_12(X0,inverse(X1)),X1) = iPr_def_14(X0),
inference(demodulation,[status(thm)],[c_250,c_247]) ).
tcf(c_257,plain,
! [X0: $i,X1: $i] : iPr_def_14(iPr_def_12(X0,inverse(inverse(X1)))) = iPr_def_12(iPr_def_14(X0),X1),
inference(superposition,[status(thm)],[c_252,c_252]) ).
tcf(c_261,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_12(multiply(X0,inverse(inverse(X1))),X2) = multiply(iPr_def_12(X0,X1),X2),
inference(superposition,[status(thm)],[c_243,c_248]) ).
tcf(c_273,plain,
! [X0: $i,X1: $i] : multiply(iPr_def_12(X0,X1),inverse(X1)) = X0,
inference(superposition,[status(thm)],[c_261,c_122]) ).
tcf(c_278,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(multiply(iPr_def_12(X0,X1),X2),inverse(X2)) = multiply(X0,inverse(inverse(X1))),
inference(superposition,[status(thm)],[c_261,c_273]) ).
tcf(c_293,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(multiply(X0,inverse(X1)),inverse(inverse(X1))) = multiply(multiply(X0,X2),inverse(X2)),
inference(superposition,[status(thm)],[c_122,c_278]) ).
tcf(c_300,plain,
! [X0: $i,X1: $i] : multiply(multiply(X0,X1),inverse(X1)) = iPr_def_15(X0),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_15])],[c_293]) ).
tcf(c_302,plain,
! [X0: $i,X1: $i] : multiply(X0,inverse(inverse(X1))) = iPr_def_15(iPr_def_12(X0,X1)),
inference(demodulation,[status(thm)],[c_278,c_300]) ).
tcf(c_312,plain,
multiply(iPr_def_10,inverse(b)) = iPr_def_15(a),
inference(superposition,[status(thm)],[c_62,c_300]) ).
tcf(c_313,plain,
multiply(iPr_def_11,inverse(a)) = iPr_def_15(b),
inference(superposition,[status(thm)],[c_63,c_300]) ).
tcf(c_314,plain,
! [X0: $i,X1: $i] : multiply(iPr_def_12(X0,X1),inverse(X1)) = iPr_def_15(iPr_def_14(X0)),
inference(superposition,[status(thm)],[c_248,c_300]) ).
tcf(c_316,plain,
! [X0: $i,X1: $i] : multiply(iPr_def_15(X0),inverse(inverse(X1))) = iPr_def_15(multiply(X0,X1)),
inference(superposition,[status(thm)],[c_300,c_300]) ).
tcf(c_318,plain,
! [X0: $i,X1: $i] : iPr_def_12(iPr_def_15(X0),X1) = multiply(X0,X1),
inference(superposition,[status(thm)],[c_300,c_122]) ).
tcf(c_319,plain,
! [X0: $i] : iPr_def_15(iPr_def_14(X0)) = X0,
inference(demodulation,[status(thm)],[c_314,c_273]) ).
tcf(c_324,plain,
! [X0: $i,X1: $i] : iPr_def_12(X0,inverse(inverse(X1))) = iPr_def_15(iPr_def_12(iPr_def_14(X0),X1)),
inference(superposition,[status(thm)],[c_257,c_319]) ).
tcf(c_328,plain,
iPr_def_12(iPr_def_15(a),b) = iPr_def_10,
inference(superposition,[status(thm)],[c_312,c_122]) ).
tcf(c_333,plain,
multiply(a,b) = iPr_def_10,
inference(demodulation,[status(thm)],[c_328,c_318]) ).
tcf(c_337,plain,
! [X0: $i,X1: $i] : iPr_def_12(multiply(X0,inverse(X1)),X1) = iPr_def_14(iPr_def_15(X0)),
inference(superposition,[status(thm)],[c_318,c_252]) ).
tcf(c_340,plain,
! [X0: $i] : iPr_def_14(iPr_def_15(X0)) = X0,
inference(demodulation,[status(thm)],[c_337,c_122]) ).
tcf(c_447,plain,
! [X0: $i,X1: $i,X2: $i] : inverse(multiply(inverse(multiply(inverse(iPr_def_10),iPr_def_11)),multiply(inverse(multiply(iPr_def_12(X0,multiply(X1,inverse(X2))),X2)),X0))) = iPr_def_14(X1),
inference(superposition,[status(thm)],[c_273,c_191]) ).
tcf(c_454,plain,
! [X0: $i,X1: $i,X2: $i] : inverse(multiply(inverse(multiply(inverse(iPr_def_10),iPr_def_11)),multiply(inverse(multiply(X0,X1)),multiply(X0,inverse(X2))))) = iPr_def_14(iPr_def_12(X2,X1)),
inference(superposition,[status(thm)],[c_273,c_191]) ).
tcf(c_458,plain,
! [X0: $i,X1: $i,X2: $i] : inverse(multiply(inverse(multiply(inverse(iPr_def_10),iPr_def_11)),multiply(inverse(multiply(X0,X1)),multiply(X0,inverse(iPr_def_15(X2)))))) = iPr_def_14(multiply(X2,X1)),
inference(superposition,[status(thm)],[c_300,c_191]) ).
tcf(c_460,plain,
! [X0: $i] : inverse(multiply(inverse(multiply(inverse(iPr_def_10),iPr_def_11)),multiply(inverse(multiply(X0,a)),multiply(X0,inverse(iPr_def_15(b)))))) = iPr_def_14(iPr_def_11),
inference(superposition,[status(thm)],[c_313,c_191]) ).
tcf(c_1255,plain,
! [X0: $i,X1: $i,X2: $i] : inverse(multiply(inverse(multiply(inverse(iPr_def_10),iPr_def_11)),multiply(inverse(multiply(iPr_def_12(X0,X1),X2)),X0))) = iPr_def_14(iPr_def_12(X1,X2)),
inference(superposition,[status(thm)],[c_273,c_447]) ).
tcf(c_1354,plain,
! [X0: $i,X1: $i] : inverse(multiply(inverse(multiply(inverse(iPr_def_10),iPr_def_11)),multiply(inverse(X0),X0))) = iPr_def_14(iPr_def_12(X1,inverse(X1))),
inference(superposition,[status(thm)],[c_273,c_1255]) ).
tcf(c_1474,plain,
! [X0: $i,X1: $i] : inverse(multiply(inverse(multiply(inverse(iPr_def_10),iPr_def_11)),multiply(inverse(X0),X0))) = inverse(multiply(inverse(multiply(inverse(iPr_def_10),iPr_def_11)),multiply(inverse(X1),X1))),
inference(superposition,[status(thm)],[c_1354,c_1354]) ).
tcf(c_1475,plain,
! [X0: $i] : inverse(multiply(inverse(multiply(inverse(iPr_def_10),iPr_def_11)),multiply(inverse(X0),X0))) = iPr_def_16,
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_16])],[c_1474]) ).
tcf(c_1493,plain,
! [X0: $i] : iPr_def_14(iPr_def_12(X0,inverse(X0))) = iPr_def_16,
inference(demodulation,[status(thm)],[c_1354,c_1475]) ).
tcf(c_1578,plain,
! [X0: $i] : iPr_def_12(X0,inverse(X0)) = iPr_def_15(iPr_def_16),
inference(superposition,[status(thm)],[c_1493,c_319]) ).
tcf(c_1580,plain,
! [X0: $i] : iPr_def_12(iPr_def_14(inverse(X0)),X0) = iPr_def_16,
inference(superposition,[status(thm)],[c_1493,c_257]) ).
tcf(c_1743,plain,
! [X0: $i] : iPr_def_12(iPr_def_15(iPr_def_16),X0) = iPr_def_14(X0),
inference(superposition,[status(thm)],[c_1578,c_252]) ).
tcf(c_1747,plain,
! [X0: $i] : multiply(X0,inverse(iPr_def_15(X0))) = iPr_def_15(iPr_def_16),
inference(superposition,[status(thm)],[c_1578,c_318]) ).
tcf(c_1750,plain,
! [X0: $i] : multiply(iPr_def_16,X0) = iPr_def_14(X0),
inference(demodulation,[status(thm)],[c_1743,c_318]) ).
tcf(c_1776,plain,
! [X0: $i] : iPr_def_14(inverse(inverse(X0))) = iPr_def_15(iPr_def_12(iPr_def_16,X0)),
inference(superposition,[status(thm)],[c_1750,c_302]) ).
tcf(c_1802,plain,
! [X0: $i] : iPr_def_14(iPr_def_14(inverse(inverse(X0)))) = iPr_def_12(iPr_def_16,X0),
inference(superposition,[status(thm)],[c_1580,c_252]) ).
tcf(c_1804,plain,
! [X0: $i] : iPr_def_12(iPr_def_14(iPr_def_14(inverse(inverse(inverse(X0))))),X0) = iPr_def_14(iPr_def_16),
inference(superposition,[status(thm)],[c_1580,c_257]) ).
tcf(c_1842,plain,
iPr_def_14(inverse(iPr_def_15(iPr_def_16))) = iPr_def_15(iPr_def_16),
inference(superposition,[status(thm)],[c_1747,c_1750]) ).
tcf(c_1852,plain,
! [X0: $i] : iPr_def_12(inverse(iPr_def_15(iPr_def_16)),inverse(inverse(X0))) = iPr_def_15(iPr_def_12(iPr_def_15(iPr_def_16),X0)),
inference(superposition,[status(thm)],[c_1842,c_324]) ).
tcf(c_1853,plain,
inverse(iPr_def_15(iPr_def_16)) = iPr_def_15(iPr_def_15(iPr_def_16)),
inference(superposition,[status(thm)],[c_1842,c_319]) ).
tcf(c_1856,plain,
! [X0: $i] : iPr_def_12(inverse(iPr_def_15(iPr_def_16)),inverse(inverse(X0))) = X0,
inference(demodulation,[status(thm)],[c_1852,c_318,c_319,c_1750]) ).
tcf(c_1867,plain,
! [X0: $i] : multiply(iPr_def_15(X0),inverse(iPr_def_15(iPr_def_15(iPr_def_16)))) = iPr_def_15(multiply(X0,iPr_def_15(iPr_def_16))),
inference(superposition,[status(thm)],[c_1853,c_316]) ).
tcf(c_1874,plain,
! [X0: $i] : iPr_def_12(iPr_def_12(X0,iPr_def_15(iPr_def_15(iPr_def_16))),iPr_def_15(iPr_def_16)) = iPr_def_14(X0),
inference(superposition,[status(thm)],[c_1853,c_252]) ).
tcf(c_1875,plain,
! [X0: $i] : iPr_def_12(multiply(X0,iPr_def_15(iPr_def_15(iPr_def_16))),iPr_def_15(iPr_def_16)) = X0,
inference(superposition,[status(thm)],[c_1853,c_122]) ).
tcf(c_1909,plain,
iPr_def_14(inverse(inverse(inverse(iPr_def_16)))) = iPr_def_15(iPr_def_15(iPr_def_16)),
inference(superposition,[status(thm)],[c_1578,c_1776]) ).
tcf(c_1950,plain,
! [X0: $i] : iPr_def_12(iPr_def_15(iPr_def_15(iPr_def_16)),inverse(inverse(X0))) = X0,
inference(light_normalisation,[status(thm)],[c_1856,c_1853]) ).
tcf(c_1953,plain,
! [X0: $i] : multiply(inverse(multiply(inverse(iPr_def_10),iPr_def_11)),multiply(inverse(multiply(X0,a)),multiply(X0,inverse(iPr_def_15(b))))) = iPr_def_12(iPr_def_15(iPr_def_15(iPr_def_16)),inverse(iPr_def_14(iPr_def_11))),
inference(superposition,[status(thm)],[c_460,c_1950]) ).
tcf(c_1960,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(inverse(multiply(inverse(iPr_def_10),iPr_def_11)),multiply(inverse(multiply(iPr_def_12(X0,X1),X2)),X0)) = iPr_def_12(iPr_def_15(iPr_def_15(iPr_def_16)),inverse(iPr_def_14(iPr_def_12(X1,X2)))),
inference(superposition,[status(thm)],[c_1255,c_1950]) ).
tcf(c_1971,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(inverse(multiply(inverse(iPr_def_10),iPr_def_11)),multiply(inverse(multiply(iPr_def_12(X0,X1),X2)),X0)) = multiply(iPr_def_15(iPr_def_16),inverse(iPr_def_14(iPr_def_12(X1,X2)))),
inference(demodulation,[status(thm)],[c_1960,c_318]) ).
tcf(c_1976,plain,
! [X0: $i] : multiply(inverse(multiply(inverse(iPr_def_10),iPr_def_11)),multiply(inverse(multiply(X0,a)),multiply(X0,inverse(iPr_def_15(b))))) = multiply(iPr_def_15(iPr_def_16),inverse(iPr_def_14(iPr_def_11))),
inference(demodulation,[status(thm)],[c_1953,c_318]) ).
tcf(c_1984,plain,
! [X0: $i,X1: $i] : inverse(multiply(iPr_def_15(iPr_def_16),inverse(iPr_def_14(iPr_def_12(X0,X1))))) = iPr_def_14(iPr_def_12(X0,X1)),
inference(demodulation,[status(thm)],[c_1255,c_1971]) ).
tcf(c_1987,plain,
inverse(multiply(iPr_def_15(iPr_def_16),inverse(iPr_def_14(iPr_def_11)))) = iPr_def_14(iPr_def_11),
inference(demodulation,[status(thm)],[c_460,c_1976]) ).
tcf(c_2014,plain,
inverse(inverse(inverse(iPr_def_16))) = iPr_def_15(iPr_def_15(iPr_def_15(iPr_def_16))),
inference(superposition,[status(thm)],[c_1909,c_319]) ).
tcf(c_2037,plain,
! [X0: $i] : iPr_def_12(multiply(X0,iPr_def_15(iPr_def_15(iPr_def_15(iPr_def_16)))),inverse(inverse(iPr_def_16))) = X0,
inference(superposition,[status(thm)],[c_2014,c_122]) ).
tcf(c_2040,plain,
! [X0: $i] : multiply(X0,iPr_def_15(iPr_def_15(iPr_def_15(iPr_def_16)))) = iPr_def_15(iPr_def_12(X0,inverse(iPr_def_16))),
inference(superposition,[status(thm)],[c_2014,c_302]) ).
tcf(c_2368,plain,
! [X0: $i,X1: $i] : multiply(inverse(multiply(inverse(multiply(inverse(iPr_def_10),iPr_def_11)),multiply(inverse(iPr_def_10),multiply(a,inverse(multiply(X0,inverse(b))))))),X1) = iPr_def_12(X0,X1),
inference(light_normalisation,[status(thm)],[c_176,c_247]) ).
tcf(c_2488,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : multiply(inverse(multiply(inverse(multiply(inverse(iPr_def_11),iPr_def_10)),multiply(inverse(multiply(iPr_def_12(X0,multiply(multiply(X1,inverse(X2)),inverse(X3))),X3)),X0))),X2) = X1,
inference(superposition,[status(thm)],[c_273,c_116]) ).
tcf(c_2498,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(inverse(multiply(inverse(multiply(inverse(iPr_def_11),iPr_def_10)),multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(iPr_def_15(X2)))))),X1) = X2,
inference(superposition,[status(thm)],[c_300,c_116]) ).
tcf(c_2673,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(inverse(multiply(inverse(multiply(inverse(iPr_def_14(X0)),multiply(X0,iPr_def_16))),multiply(inverse(iPr_def_10),multiply(a,inverse(multiply(multiply(X1,inverse(X2)),inverse(b))))))),X2) = X1,
inference(superposition,[status(thm)],[c_1750,c_106]) ).
tcf(c_4651,plain,
! [X0: $i] : iPr_def_12(iPr_def_15(iPr_def_12(X0,inverse(iPr_def_16))),inverse(inverse(iPr_def_16))) = X0,
inference(light_normalisation,[status(thm)],[c_2037,c_2040]) ).
tcf(c_4728,plain,
inverse(multiply(inverse(multiply(inverse(iPr_def_10),iPr_def_11)),multiply(iPr_def_14(iPr_def_11),multiply(iPr_def_15(iPr_def_16),inverse(iPr_def_14(iPr_def_11)))))) = iPr_def_16,
inference(superposition,[status(thm)],[c_1987,c_1475]) ).
tcf(c_4736,plain,
! [X0: $i] : multiply(inverse(multiply(inverse(iPr_def_10),iPr_def_11)),multiply(inverse(X0),X0)) = iPr_def_12(iPr_def_15(iPr_def_15(iPr_def_16)),inverse(iPr_def_16)),
inference(superposition,[status(thm)],[c_1475,c_1950]) ).
tcf(c_4750,plain,
! [X0: $i] : multiply(inverse(multiply(inverse(iPr_def_10),iPr_def_11)),multiply(inverse(X0),X0)) = multiply(iPr_def_15(iPr_def_16),inverse(iPr_def_16)),
inference(demodulation,[status(thm)],[c_4736,c_318]) ).
tcf(c_4753,plain,
inverse(multiply(inverse(multiply(inverse(iPr_def_10),iPr_def_11)),iPr_def_12(iPr_def_11,multiply(iPr_def_15(iPr_def_16),inverse(iPr_def_14(iPr_def_11)))))) = iPr_def_16,
inference(demodulation,[status(thm)],[c_4728,c_248]) ).
tcf(c_5522,plain,
! [X0: $i] : inverse(multiply(iPr_def_15(iPr_def_16),inverse(iPr_def_14(X0)))) = iPr_def_14(X0),
inference(superposition,[status(thm)],[c_4651,c_1984]) ).
tcf(c_5553,plain,
! [X0: $i] : inverse(multiply(iPr_def_15(iPr_def_16),inverse(X0))) = X0,
inference(superposition,[status(thm)],[c_340,c_5522]) ).
tcf(c_5593,plain,
inverse(multiply(iPr_def_15(iPr_def_16),iPr_def_15(iPr_def_15(iPr_def_16)))) = iPr_def_15(iPr_def_16),
inference(superposition,[status(thm)],[c_1853,c_5553]) ).
tcf(c_5599,plain,
! [X0: $i] : multiply(iPr_def_15(iPr_def_16),inverse(X0)) = inverse(multiply(iPr_def_15(iPr_def_16),X0)),
inference(superposition,[status(thm)],[c_5553,c_5553]) ).
tcf(c_5608,plain,
! [X0: $i] : iPr_def_12(iPr_def_16,multiply(iPr_def_15(iPr_def_16),inverse(X0))) = iPr_def_14(iPr_def_14(inverse(X0))),
inference(superposition,[status(thm)],[c_5553,c_1802]) ).
tcf(c_5609,plain,
! [X0: $i] : iPr_def_12(iPr_def_14(X0),multiply(iPr_def_15(iPr_def_16),inverse(X0))) = iPr_def_16,
inference(superposition,[status(thm)],[c_5553,c_1580]) ).
tcf(c_5613,plain,
! [X0: $i,X1: $i] : iPr_def_15(multiply(X0,multiply(iPr_def_15(iPr_def_16),inverse(X1)))) = multiply(iPr_def_15(X0),inverse(X1)),
inference(superposition,[status(thm)],[c_5553,c_316]) ).
tcf(c_5623,plain,
! [X0: $i] : multiply(inverse(multiply(inverse(multiply(inverse(iPr_def_10),iPr_def_11)),multiply(inverse(iPr_def_10),multiply(a,b)))),X0) = iPr_def_12(iPr_def_15(iPr_def_16),X0),
inference(superposition,[status(thm)],[c_5553,c_2368]) ).
tcf(c_5629,plain,
! [X0: $i] : multiply(inverse(multiply(inverse(multiply(inverse(iPr_def_10),iPr_def_11)),multiply(inverse(iPr_def_10),iPr_def_10))),X0) = iPr_def_14(X0),
inference(demodulation,[status(thm)],[c_5623,c_318,c_333,c_1750]) ).
tcf(c_5672,plain,
! [X0: $i] : iPr_def_15(multiply(X0,multiply(iPr_def_15(iPr_def_16),iPr_def_15(iPr_def_15(iPr_def_16))))) = multiply(iPr_def_15(X0),inverse(iPr_def_15(iPr_def_16))),
inference(superposition,[status(thm)],[c_5593,c_316]) ).
tcf(c_5679,plain,
! [X0: $i] : iPr_def_12(iPr_def_12(X0,iPr_def_15(iPr_def_16)),multiply(iPr_def_15(iPr_def_16),iPr_def_15(iPr_def_15(iPr_def_16)))) = iPr_def_14(X0),
inference(superposition,[status(thm)],[c_5593,c_252]) ).
tcf(c_5687,plain,
! [X0: $i] : iPr_def_15(multiply(X0,multiply(iPr_def_15(iPr_def_16),iPr_def_15(iPr_def_15(iPr_def_16))))) = multiply(iPr_def_15(X0),iPr_def_15(iPr_def_15(iPr_def_16))),
inference(demodulation,[status(thm)],[c_5672,c_1853]) ).
tcf(c_5718,plain,
! [X0: $i] : iPr_def_12(X0,multiply(iPr_def_15(iPr_def_16),inverse(iPr_def_15(X0)))) = iPr_def_16,
inference(superposition,[status(thm)],[c_340,c_5609]) ).
tcf(c_5775,plain,
! [X0: $i] : multiply(iPr_def_16,inverse(multiply(iPr_def_15(iPr_def_16),inverse(iPr_def_15(X0))))) = X0,
inference(superposition,[status(thm)],[c_5718,c_273]) ).
tcf(c_5785,plain,
! [X0: $i] : iPr_def_14(inverse(multiply(iPr_def_15(iPr_def_16),inverse(iPr_def_15(X0))))) = X0,
inference(demodulation,[status(thm)],[c_5775,c_1750]) ).
tcf(c_5836,plain,
! [X0: $i] : inverse(multiply(iPr_def_15(iPr_def_16),inverse(iPr_def_15(X0)))) = iPr_def_15(X0),
inference(superposition,[status(thm)],[c_5785,c_319]) ).
tcf(c_5880,plain,
! [X0: $i,X1: $i] : iPr_def_12(multiply(X0,iPr_def_15(X1)),multiply(iPr_def_15(iPr_def_16),inverse(iPr_def_15(X1)))) = X0,
inference(superposition,[status(thm)],[c_5836,c_122]) ).
tcf(c_5958,plain,
! [X0: $i] : iPr_def_12(iPr_def_14(iPr_def_14(inverse(inverse(multiply(iPr_def_15(iPr_def_16),inverse(X0)))))),multiply(iPr_def_15(iPr_def_16),X0)) = iPr_def_14(iPr_def_16),
inference(superposition,[status(thm)],[c_5599,c_1804]) ).
tcf(c_5966,plain,
! [X0: $i,X1: $i] : multiply(X0,inverse(multiply(iPr_def_15(iPr_def_16),inverse(X1)))) = iPr_def_15(iPr_def_12(X0,multiply(iPr_def_15(iPr_def_16),X1))),
inference(superposition,[status(thm)],[c_5599,c_302]) ).
tcf(c_5969,plain,
! [X0: $i,X1: $i] : multiply(iPr_def_12(X0,multiply(iPr_def_15(iPr_def_16),X1)),multiply(iPr_def_15(iPr_def_16),inverse(X1))) = X0,
inference(superposition,[status(thm)],[c_5599,c_273]) ).
tcf(c_5971,plain,
! [X0: $i,X1: $i] : iPr_def_14(iPr_def_13(X0,inverse(multiply(iPr_def_15(iPr_def_16),inverse(X1))))) = iPr_def_12(iPr_def_14(X0),multiply(iPr_def_15(iPr_def_16),X1)),
inference(superposition,[status(thm)],[c_5599,c_244]) ).
tcf(c_5973,plain,
! [X0: $i,X1: $i] : iPr_def_12(multiply(X0,multiply(iPr_def_15(iPr_def_16),inverse(X1))),multiply(iPr_def_15(iPr_def_16),X1)) = X0,
inference(superposition,[status(thm)],[c_5599,c_122]) ).
tcf(c_5978,plain,
! [X0: $i,X1: $i] : iPr_def_15(iPr_def_12(X0,multiply(iPr_def_15(iPr_def_16),X1))) = multiply(X0,X1),
inference(demodulation,[status(thm)],[c_5966,c_316,c_319,c_1750,c_5599]) ).
tcf(c_5979,plain,
! [X0: $i,X1: $i] : iPr_def_12(iPr_def_14(X0),multiply(iPr_def_15(iPr_def_16),X1)) = iPr_def_14(iPr_def_12(X0,X1)),
inference(demodulation,[status(thm)],[c_5971,c_247,c_316,c_319,c_1750,c_5599]) ).
tcf(c_5982,plain,
! [X0: $i] : iPr_def_12(iPr_def_12(iPr_def_16,multiply(iPr_def_15(iPr_def_16),inverse(X0))),multiply(iPr_def_15(iPr_def_16),X0)) = iPr_def_14(iPr_def_16),
inference(demodulation,[status(thm)],[c_5958,c_1802]) ).
tcf(c_5983,plain,
! [X0: $i] : iPr_def_12(iPr_def_14(iPr_def_14(inverse(X0))),multiply(iPr_def_15(iPr_def_16),X0)) = iPr_def_14(iPr_def_16),
inference(light_normalisation,[status(thm)],[c_5982,c_5608]) ).
tcf(c_6192,plain,
! [X0: $i,X1: $i] : multiply(iPr_def_12(X0,multiply(iPr_def_15(iPr_def_16),X1)),inverse(multiply(X0,X1))) = iPr_def_15(iPr_def_16),
inference(superposition,[status(thm)],[c_5978,c_1747]) ).
tcf(c_6194,plain,
! [X0: $i,X1: $i] : iPr_def_12(X0,multiply(iPr_def_15(iPr_def_16),X1)) = iPr_def_14(multiply(X0,X1)),
inference(superposition,[status(thm)],[c_5978,c_340]) ).
tcf(c_6244,plain,
! [X0: $i,X1: $i] : multiply(X0,multiply(iPr_def_15(iPr_def_16),X1)) = iPr_def_14(multiply(iPr_def_15(X0),X1)),
inference(superposition,[status(thm)],[c_6194,c_318]) ).
tcf(c_6519,plain,
! [X0: $i,X1: $i] : iPr_def_12(iPr_def_14(X0),iPr_def_14(multiply(iPr_def_15(iPr_def_15(iPr_def_16)),X1))) = iPr_def_14(iPr_def_12(X0,multiply(iPr_def_15(iPr_def_16),X1))),
inference(superposition,[status(thm)],[c_6244,c_5979]) ).
tcf(c_6522,plain,
! [X0: $i] : multiply(iPr_def_15(iPr_def_16),inverse(multiply(iPr_def_15(iPr_def_16),X0))) = inverse(iPr_def_14(multiply(iPr_def_15(iPr_def_15(iPr_def_16)),X0))),
inference(superposition,[status(thm)],[c_6244,c_5599]) ).
tcf(c_6525,plain,
! [X0: $i] : inverse(iPr_def_14(multiply(iPr_def_15(iPr_def_15(iPr_def_16)),X0))) = iPr_def_14(multiply(iPr_def_15(iPr_def_15(iPr_def_16)),inverse(X0))),
inference(demodulation,[status(thm)],[c_6522,c_5599,c_6244]) ).
tcf(c_6528,plain,
! [X0: $i,X1: $i] : iPr_def_12(iPr_def_14(X0),iPr_def_14(multiply(iPr_def_15(iPr_def_15(iPr_def_16)),X1))) = iPr_def_14(iPr_def_14(multiply(X0,X1))),
inference(demodulation,[status(thm)],[c_6519,c_6194]) ).
tcf(c_7915,plain,
! [X0: $i,X1: $i] : multiply(inverse(multiply(inverse(multiply(inverse(iPr_def_11),iPr_def_10)),iPr_def_14(multiply(iPr_def_15(inverse(multiply(iPr_def_15(iPr_def_16),inverse(X0)))),inverse(iPr_def_15(X1)))))),X0) = X1,
inference(superposition,[status(thm)],[c_6244,c_2498]) ).
tcf(c_7999,plain,
! [X0: $i,X1: $i] : multiply(inverse(multiply(inverse(multiply(inverse(iPr_def_11),iPr_def_10)),iPr_def_14(multiply(iPr_def_15(X0),inverse(iPr_def_15(X1)))))),X0) = X1,
inference(demodulation,[status(thm)],[c_7915,c_316,c_319,c_1750,c_5599]) ).
tcf(c_10288,plain,
! [X0: $i,X1: $i] : multiply(iPr_def_14(multiply(X0,X1)),multiply(iPr_def_15(iPr_def_16),inverse(X1))) = X0,
inference(light_normalisation,[status(thm)],[c_5969,c_6194]) ).
tcf(c_10409,plain,
! [X0: $i,X1: $i] : multiply(iPr_def_14(multiply(X0,X1)),inverse(multiply(X0,X1))) = iPr_def_15(iPr_def_16),
inference(light_normalisation,[status(thm)],[c_6192,c_6194]) ).
tcf(c_14470,plain,
! [X0: $i] : multiply(iPr_def_14(multiply(iPr_def_15(iPr_def_16),inverse(iPr_def_16))),multiply(iPr_def_15(iPr_def_16),inverse(multiply(inverse(X0),X0)))) = inverse(multiply(inverse(iPr_def_10),iPr_def_11)),
inference(superposition,[status(thm)],[c_4750,c_10288]) ).
tcf(c_14473,plain,
! [X0: $i] : iPr_def_14(multiply(multiply(iPr_def_15(iPr_def_16),inverse(iPr_def_16)),inverse(multiply(inverse(X0),X0)))) = inverse(multiply(inverse(iPr_def_10),iPr_def_11)),
inference(demodulation,[status(thm)],[c_14470,c_248,c_6194]) ).
tcf(c_21642,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(inverse(multiply(inverse(multiply(inverse(iPr_def_11),iPr_def_10)),multiply(inverse(multiply(iPr_def_12(X0,multiply(iPr_def_15(iPr_def_16),inverse(X1))),X1)),X0))),iPr_def_15(X2)) = X2,
inference(superposition,[status(thm)],[c_1747,c_2488]) ).
tcf(c_21747,plain,
! [X0: $i,X1: $i] : multiply(inverse(multiply(inverse(multiply(inverse(iPr_def_11),iPr_def_10)),multiply(inverse(X0),X0))),iPr_def_15(X1)) = X1,
inference(demodulation,[status(thm)],[c_21642,c_122,c_248,c_6194]) ).
tcf(c_23906,plain,
! [X0: $i,X1: $i,X2: $i] : inverse(multiply(inverse(multiply(inverse(iPr_def_10),iPr_def_11)),multiply(inverse(multiply(iPr_def_14(multiply(X0,inverse(X1))),X1)),iPr_def_15(iPr_def_16)))) = iPr_def_13(iPr_def_13(X0,inverse(X2)),X2),
inference(superposition,[status(thm)],[c_10409,c_186]) ).
tcf(c_24082,plain,
! [X0: $i] : inverse(multiply(inverse(multiply(inverse(iPr_def_10),iPr_def_11)),multiply(inverse(X0),iPr_def_15(iPr_def_16)))) = iPr_def_14(X0),
inference(demodulation,[status(thm)],[c_23906,c_122,c_247,c_248,c_252]) ).
tcf(c_24546,plain,
iPr_def_14(multiply(inverse(multiply(inverse(iPr_def_10),iPr_def_11)),multiply(inverse(iPr_def_10),iPr_def_10))) = inverse(multiply(inverse(multiply(inverse(iPr_def_10),iPr_def_11)),iPr_def_14(iPr_def_15(iPr_def_16)))),
inference(superposition,[status(thm)],[c_5629,c_24082]) ).
tcf(c_24651,plain,
inverse(multiply(inverse(multiply(inverse(iPr_def_10),iPr_def_11)),iPr_def_16)) = iPr_def_14(multiply(iPr_def_15(iPr_def_16),inverse(iPr_def_16))),
inference(demodulation,[status(thm)],[c_24546,c_340,c_4750]) ).
tcf(c_25037,plain,
! [X0: $i] : inverse(multiply(inverse(multiply(inverse(iPr_def_11),iPr_def_10)),multiply(inverse(X0),X0))) = iPr_def_12(iPr_def_15(iPr_def_16),iPr_def_15(iPr_def_16)),
inference(superposition,[status(thm)],[c_21747,c_1875]) ).
tcf(c_25041,plain,
! [X0: $i] : inverse(multiply(inverse(multiply(inverse(iPr_def_11),iPr_def_10)),multiply(inverse(X0),X0))) = iPr_def_16,
inference(demodulation,[status(thm)],[c_25037,c_318,c_340,c_1750]) ).
tcf(c_25173,plain,
! [X0: $i] : multiply(inverse(multiply(inverse(iPr_def_11),iPr_def_10)),multiply(inverse(X0),X0)) = iPr_def_12(iPr_def_15(iPr_def_15(iPr_def_16)),inverse(iPr_def_16)),
inference(superposition,[status(thm)],[c_25041,c_1950]) ).
tcf(c_25216,plain,
! [X0: $i] : multiply(inverse(multiply(inverse(iPr_def_11),iPr_def_10)),multiply(inverse(X0),X0)) = multiply(iPr_def_15(iPr_def_16),inverse(iPr_def_16)),
inference(demodulation,[status(thm)],[c_25173,c_318]) ).
tcf(c_28892,plain,
! [X0: $i] : multiply(iPr_def_14(multiply(iPr_def_15(iPr_def_16),inverse(iPr_def_16))),multiply(iPr_def_15(iPr_def_16),inverse(multiply(inverse(X0),X0)))) = inverse(multiply(inverse(iPr_def_11),iPr_def_10)),
inference(superposition,[status(thm)],[c_25216,c_10288]) ).
tcf(c_28896,plain,
! [X0: $i] : iPr_def_14(multiply(multiply(iPr_def_15(iPr_def_16),inverse(iPr_def_16)),inverse(multiply(inverse(X0),X0)))) = inverse(multiply(inverse(iPr_def_11),iPr_def_10)),
inference(demodulation,[status(thm)],[c_28892,c_248,c_6194]) ).
tcf(c_28897,plain,
inverse(multiply(inverse(iPr_def_10),iPr_def_11)) = inverse(multiply(inverse(iPr_def_11),iPr_def_10)),
inference(light_normalisation,[status(thm)],[c_28896,c_14473]) ).
tcf(c_28963,plain,
iPr_def_12(iPr_def_15(iPr_def_15(iPr_def_16)),inverse(inverse(multiply(inverse(iPr_def_10),iPr_def_11)))) = multiply(inverse(iPr_def_11),iPr_def_10),
inference(superposition,[status(thm)],[c_28897,c_1950]) ).
tcf(c_29007,plain,
multiply(inverse(iPr_def_10),iPr_def_11) = multiply(inverse(iPr_def_11),iPr_def_10),
inference(demodulation,[status(thm)],[c_28963,c_1950]) ).
tcf(c_29093,plain,
multiply(multiply(inverse(iPr_def_10),iPr_def_11),inverse(iPr_def_10)) = iPr_def_15(inverse(iPr_def_11)),
inference(superposition,[status(thm)],[c_29007,c_300]) ).
tcf(c_36301,plain,
! [X0: $i,X1: $i] : multiply(inverse(multiply(inverse(multiply(inverse(iPr_def_10),iPr_def_11)),iPr_def_14(multiply(iPr_def_15(X0),inverse(iPr_def_15(X1)))))),X0) = X1,
inference(light_normalisation,[status(thm)],[c_7999,c_29007]) ).
tcf(c_36310,plain,
! [X0: $i] : multiply(inverse(multiply(inverse(multiply(inverse(iPr_def_10),iPr_def_11)),iPr_def_14(iPr_def_15(iPr_def_16)))),X0) = iPr_def_15(X0),
inference(superposition,[status(thm)],[c_1747,c_36301]) ).
tcf(c_36416,plain,
! [X0: $i] : iPr_def_12(multiply(iPr_def_15(iPr_def_16),inverse(iPr_def_16)),X0) = iPr_def_15(X0),
inference(demodulation,[status(thm)],[c_36310,c_248,c_340,c_24651]) ).
tcf(c_36575,plain,
iPr_def_12(iPr_def_15(iPr_def_15(iPr_def_16)),multiply(iPr_def_15(iPr_def_16),iPr_def_15(iPr_def_15(iPr_def_16)))) = iPr_def_14(multiply(iPr_def_15(iPr_def_16),inverse(iPr_def_16))),
inference(superposition,[status(thm)],[c_36416,c_5679]) ).
tcf(c_36591,plain,
iPr_def_12(iPr_def_15(iPr_def_15(inverse(iPr_def_16))),inverse(inverse(iPr_def_16))) = multiply(iPr_def_15(iPr_def_16),inverse(iPr_def_16)),
inference(superposition,[status(thm)],[c_36416,c_4651]) ).
tcf(c_36615,plain,
multiply(iPr_def_15(iPr_def_16),inverse(iPr_def_16)) = iPr_def_15(multiply(inverse(iPr_def_16),iPr_def_16)),
inference(demodulation,[status(thm)],[c_36591,c_316,c_318]) ).
tcf(c_36622,plain,
iPr_def_14(multiply(iPr_def_15(iPr_def_15(iPr_def_16)),iPr_def_15(iPr_def_15(iPr_def_16)))) = iPr_def_14(multiply(iPr_def_15(iPr_def_16),inverse(iPr_def_16))),
inference(demodulation,[status(thm)],[c_36575,c_318,c_6244]) ).
tcf(c_36641,plain,
! [X0: $i] : iPr_def_12(iPr_def_15(multiply(inverse(iPr_def_16),iPr_def_16)),X0) = iPr_def_15(X0),
inference(demodulation,[status(thm)],[c_36416,c_36615]) ).
tcf(c_36661,plain,
! [X0: $i] : multiply(multiply(inverse(iPr_def_16),iPr_def_16),X0) = iPr_def_15(X0),
inference(demodulation,[status(thm)],[c_36641,c_318]) ).
tcf(c_36707,plain,
! [X0: $i] : iPr_def_12(iPr_def_15(inverse(X0)),X0) = multiply(inverse(iPr_def_16),iPr_def_16),
inference(superposition,[status(thm)],[c_36661,c_122]) ).
tcf(c_36759,plain,
! [X0: $i] : multiply(inverse(X0),X0) = multiply(inverse(iPr_def_16),iPr_def_16),
inference(demodulation,[status(thm)],[c_36707,c_318]) ).
tcf(c_38061,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : multiply(inverse(multiply(inverse(multiply(inverse(iPr_def_10),iPr_def_11)),multiply(inverse(multiply(X0,X1)),multiply(X0,inverse(X2))))),X3) = iPr_def_13(iPr_def_12(X2,X1),X3),
inference(light_normalisation,[status(thm)],[c_193,c_2368]) ).
tcf(c_38062,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(iPr_def_14(iPr_def_12(X0,X1)),X2) = iPr_def_13(iPr_def_12(X0,X1),X2),
inference(light_normalisation,[status(thm)],[c_38061,c_454]) ).
tcf(c_40451,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),X0) = multiply(inverse(X1),X1),
inference(superposition,[status(thm)],[c_36759,c_36759]) ).
tcf(c_40453,plain,
! [X0: $i] : multiply(inverse(X0),X0) = iPr_def_29,
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_29])],[c_40451]) ).
tcf(c_40595,plain,
multiply(iPr_def_15(iPr_def_15(iPr_def_16)),iPr_def_15(iPr_def_16)) = iPr_def_29,
inference(superposition,[status(thm)],[c_1853,c_40453]) ).
tcf(c_40596,plain,
multiply(iPr_def_15(iPr_def_15(iPr_def_15(iPr_def_16))),inverse(inverse(iPr_def_16))) = iPr_def_29,
inference(superposition,[status(thm)],[c_2014,c_40453]) ).
tcf(c_40618,plain,
! [X0: $i] : inverse(inverse(X0)) = iPr_def_12(iPr_def_29,X0),
inference(superposition,[status(thm)],[c_40453,c_122]) ).
tcf(c_40651,plain,
inverse(iPr_def_15(iPr_def_15(iPr_def_16))) = iPr_def_12(iPr_def_29,iPr_def_15(iPr_def_16)),
inference(superposition,[status(thm)],[c_40453,c_1875]) ).
tcf(c_40665,plain,
! [X0: $i] : inverse(multiply(iPr_def_15(iPr_def_16),inverse(X0))) = iPr_def_12(iPr_def_29,multiply(iPr_def_15(iPr_def_16),X0)),
inference(superposition,[status(thm)],[c_40453,c_5973]) ).
tcf(c_40666,plain,
! [X0: $i] : multiply(iPr_def_15(inverse(multiply(iPr_def_15(iPr_def_16),inverse(X0)))),inverse(X0)) = iPr_def_15(iPr_def_29),
inference(superposition,[status(thm)],[c_40453,c_5613]) ).
tcf(c_40667,plain,
multiply(iPr_def_15(inverse(multiply(iPr_def_15(iPr_def_16),iPr_def_15(iPr_def_15(iPr_def_16))))),iPr_def_15(iPr_def_15(iPr_def_16))) = iPr_def_15(iPr_def_29),
inference(superposition,[status(thm)],[c_40453,c_5687]) ).
tcf(c_40680,plain,
iPr_def_15(multiply(iPr_def_15(iPr_def_15(iPr_def_16)),iPr_def_16)) = iPr_def_29,
inference(demodulation,[status(thm)],[c_40596,c_316]) ).
tcf(c_40688,plain,
! [X0: $i] : multiply(iPr_def_15(X0),inverse(X0)) = iPr_def_15(iPr_def_29),
inference(demodulation,[status(thm)],[c_40666,c_316,c_319,c_1750,c_5599]) ).
tcf(c_40689,plain,
! [X0: $i] : iPr_def_14(multiply(iPr_def_29,X0)) = X0,
inference(demodulation,[status(thm)],[c_40665,c_316,c_319,c_1750,c_5599,c_6194]) ).
tcf(c_40700,plain,
multiply(iPr_def_15(iPr_def_15(iPr_def_16)),iPr_def_15(iPr_def_15(iPr_def_16))) = iPr_def_15(iPr_def_29),
inference(demodulation,[status(thm)],[c_40667,c_340,c_1750,c_1867,c_5599]) ).
tcf(c_40774,plain,
! [X0: $i] : iPr_def_12(iPr_def_15(iPr_def_15(iPr_def_16)),iPr_def_12(iPr_def_29,X0)) = X0,
inference(demodulation,[status(thm)],[c_1950,c_40618]) ).
tcf(c_40775,plain,
! [X0: $i] : iPr_def_14(iPr_def_14(iPr_def_12(iPr_def_29,X0))) = iPr_def_12(iPr_def_16,X0),
inference(demodulation,[status(thm)],[c_1802,c_40618]) ).
tcf(c_40791,plain,
! [X0: $i,X1: $i] : multiply(X0,iPr_def_12(iPr_def_29,X1)) = iPr_def_15(iPr_def_12(X0,X1)),
inference(demodulation,[status(thm)],[c_302,c_40618]) ).
tcf(c_40856,plain,
! [X0: $i] : multiply(iPr_def_15(iPr_def_16),iPr_def_12(iPr_def_29,X0)) = X0,
inference(demodulation,[status(thm)],[c_40774,c_318]) ).
tcf(c_40988,plain,
inverse(iPr_def_15(iPr_def_29)) = iPr_def_14(iPr_def_15(iPr_def_16)),
inference(superposition,[status(thm)],[c_1747,c_40689]) ).
tcf(c_40989,plain,
iPr_def_14(iPr_def_15(iPr_def_12(iPr_def_29,inverse(iPr_def_16)))) = iPr_def_15(iPr_def_15(iPr_def_15(iPr_def_16))),
inference(superposition,[status(thm)],[c_2040,c_40689]) ).
tcf(c_40999,plain,
! [X0: $i] : multiply(iPr_def_29,X0) = iPr_def_15(X0),
inference(superposition,[status(thm)],[c_40689,c_319]) ).
tcf(c_41014,plain,
inverse(iPr_def_15(iPr_def_29)) = iPr_def_16,
inference(demodulation,[status(thm)],[c_40988,c_340]) ).
tcf(c_41018,plain,
iPr_def_12(iPr_def_29,inverse(iPr_def_16)) = iPr_def_15(iPr_def_15(iPr_def_15(iPr_def_16))),
inference(demodulation,[status(thm)],[c_40989,c_340]) ).
tcf(c_41087,plain,
! [X0: $i] : iPr_def_12(iPr_def_12(X0,iPr_def_16),iPr_def_15(iPr_def_29)) = iPr_def_14(X0),
inference(superposition,[status(thm)],[c_41014,c_252]) ).
tcf(c_41088,plain,
! [X0: $i] : iPr_def_12(multiply(X0,iPr_def_16),iPr_def_15(iPr_def_29)) = X0,
inference(superposition,[status(thm)],[c_41014,c_122]) ).
tcf(c_41252,plain,
! [X0: $i] : iPr_def_12(iPr_def_15(iPr_def_15(X0)),multiply(iPr_def_15(iPr_def_16),inverse(iPr_def_15(X0)))) = iPr_def_29,
inference(superposition,[status(thm)],[c_40999,c_5880]) ).
tcf(c_41261,plain,
! [X0: $i] : iPr_def_14(multiply(iPr_def_15(iPr_def_15(X0)),inverse(iPr_def_15(X0)))) = iPr_def_29,
inference(demodulation,[status(thm)],[c_41252,c_318,c_6244]) ).
tcf(c_41321,plain,
iPr_def_12(iPr_def_29,iPr_def_15(iPr_def_29)) = inverse(iPr_def_16),
inference(superposition,[status(thm)],[c_41014,c_40618]) ).
tcf(c_41324,plain,
! [X0: $i] : inverse(iPr_def_12(iPr_def_29,X0)) = iPr_def_12(iPr_def_29,inverse(X0)),
inference(superposition,[status(thm)],[c_40618,c_40618]) ).
tcf(c_41332,plain,
! [X0: $i] : iPr_def_12(iPr_def_14(iPr_def_12(iPr_def_29,X0)),inverse(X0)) = iPr_def_16,
inference(superposition,[status(thm)],[c_40618,c_1580]) ).
tcf(c_41355,plain,
! [X0: $i,X1: $i] : multiply(iPr_def_12(X0,inverse(X1)),iPr_def_12(iPr_def_29,X1)) = X0,
inference(superposition,[status(thm)],[c_40618,c_273]) ).
tcf(c_41468,plain,
iPr_def_14(multiply(iPr_def_15(iPr_def_15(iPr_def_16)),inverse(iPr_def_15(iPr_def_16)))) = inverse(iPr_def_14(iPr_def_29)),
inference(superposition,[status(thm)],[c_40595,c_6525]) ).
tcf(c_41477,plain,
iPr_def_14(multiply(iPr_def_15(iPr_def_15(iPr_def_16)),iPr_def_15(iPr_def_15(iPr_def_16)))) = inverse(iPr_def_14(iPr_def_29)),
inference(demodulation,[status(thm)],[c_41468,c_1853]) ).
tcf(c_41478,plain,
inverse(iPr_def_14(iPr_def_29)) = iPr_def_14(iPr_def_15(iPr_def_29)),
inference(light_normalisation,[status(thm)],[c_41477,c_36622,c_40700]) ).
tcf(c_41479,plain,
inverse(iPr_def_14(iPr_def_29)) = iPr_def_29,
inference(demodulation,[status(thm)],[c_41478,c_340]) ).
tcf(c_41527,plain,
! [X0: $i] : multiply(multiply(X0,iPr_def_14(iPr_def_29)),iPr_def_29) = iPr_def_15(X0),
inference(superposition,[status(thm)],[c_41479,c_300]) ).
tcf(c_41529,plain,
! [X0: $i] : iPr_def_12(iPr_def_12(X0,iPr_def_29),iPr_def_14(iPr_def_29)) = iPr_def_14(X0),
inference(superposition,[status(thm)],[c_41479,c_252]) ).
tcf(c_41530,plain,
! [X0: $i] : iPr_def_12(multiply(X0,iPr_def_29),iPr_def_14(iPr_def_29)) = X0,
inference(superposition,[status(thm)],[c_41479,c_122]) ).
tcf(c_41614,plain,
multiply(iPr_def_15(iPr_def_15(iPr_def_16)),iPr_def_16) = iPr_def_14(iPr_def_29),
inference(superposition,[status(thm)],[c_40680,c_340]) ).
tcf(c_41635,plain,
! [X0: $i] : multiply(X0,inverse(iPr_def_14(X0))) = iPr_def_15(iPr_def_29),
inference(superposition,[status(thm)],[c_319,c_40688]) ).
tcf(c_41643,plain,
! [X0: $i] : multiply(iPr_def_15(inverse(X0)),iPr_def_12(iPr_def_29,X0)) = iPr_def_15(iPr_def_29),
inference(superposition,[status(thm)],[c_40618,c_40688]) ).
tcf(c_41682,plain,
! [X0: $i] : iPr_def_14(multiply(X0,inverse(iPr_def_16))) = iPr_def_12(X0,iPr_def_15(iPr_def_29)),
inference(superposition,[status(thm)],[c_40688,c_6194]) ).
tcf(c_41947,plain,
multiply(iPr_def_15(iPr_def_16),iPr_def_15(iPr_def_16)) = inverse(iPr_def_29),
inference(superposition,[status(thm)],[c_1578,c_40856]) ).
tcf(c_41959,plain,
! [X0: $i] : multiply(X0,inverse(iPr_def_12(iPr_def_29,X0))) = iPr_def_15(iPr_def_15(iPr_def_16)),
inference(superposition,[status(thm)],[c_40856,c_300]) ).
tcf(c_41980,plain,
! [X0: $i] : multiply(X0,iPr_def_12(iPr_def_29,inverse(X0))) = iPr_def_15(iPr_def_15(iPr_def_16)),
inference(light_normalisation,[status(thm)],[c_41959,c_41324]) ).
tcf(c_42389,plain,
iPr_def_12(iPr_def_14(iPr_def_29),iPr_def_15(iPr_def_29)) = iPr_def_15(iPr_def_15(iPr_def_16)),
inference(superposition,[status(thm)],[c_41614,c_41088]) ).
tcf(c_42466,plain,
! [X0: $i] : iPr_def_12(X0,inverse(iPr_def_14(iPr_def_14(X0)))) = iPr_def_15(iPr_def_29),
inference(superposition,[status(thm)],[c_41635,c_248]) ).
tcf(c_42794,plain,
iPr_def_12(iPr_def_14(iPr_def_14(inverse(iPr_def_15(iPr_def_16)))),inverse(iPr_def_29)) = iPr_def_14(iPr_def_16),
inference(superposition,[status(thm)],[c_41947,c_5983]) ).
tcf(c_42804,plain,
iPr_def_12(iPr_def_16,inverse(iPr_def_29)) = iPr_def_14(iPr_def_16),
inference(demodulation,[status(thm)],[c_42794,c_340,c_1853]) ).
tcf(c_42854,plain,
multiply(iPr_def_14(iPr_def_16),inverse(inverse(iPr_def_29))) = iPr_def_16,
inference(superposition,[status(thm)],[c_42804,c_273]) ).
tcf(c_42856,plain,
iPr_def_12(iPr_def_16,iPr_def_12(iPr_def_29,iPr_def_29)) = iPr_def_16,
inference(demodulation,[status(thm)],[c_42854,c_248,c_40618]) ).
tcf(c_42869,plain,
multiply(iPr_def_16,inverse(iPr_def_12(iPr_def_29,iPr_def_29))) = iPr_def_16,
inference(superposition,[status(thm)],[c_42856,c_273]) ).
tcf(c_42870,plain,
iPr_def_14(inverse(iPr_def_12(iPr_def_29,iPr_def_29))) = iPr_def_16,
inference(demodulation,[status(thm)],[c_42869,c_1750]) ).
tcf(c_42874,plain,
multiply(inverse(iPr_def_12(iPr_def_29,iPr_def_29)),inverse(iPr_def_16)) = iPr_def_15(iPr_def_29),
inference(superposition,[status(thm)],[c_42870,c_41635]) ).
tcf(c_42880,plain,
inverse(iPr_def_12(iPr_def_29,iPr_def_29)) = iPr_def_15(iPr_def_16),
inference(superposition,[status(thm)],[c_42870,c_319]) ).
tcf(c_42905,plain,
iPr_def_12(iPr_def_12(iPr_def_29,iPr_def_29),iPr_def_15(iPr_def_16)) = iPr_def_15(iPr_def_16),
inference(superposition,[status(thm)],[c_42880,c_1578]) ).
tcf(c_48645,plain,
iPr_def_14(multiply(iPr_def_12(iPr_def_29,inverse(iPr_def_16)),inverse(iPr_def_15(iPr_def_15(iPr_def_16))))) = iPr_def_29,
inference(superposition,[status(thm)],[c_41018,c_41261]) ).
tcf(c_48704,plain,
iPr_def_12(iPr_def_12(iPr_def_29,inverse(iPr_def_16)),iPr_def_15(iPr_def_16)) = iPr_def_29,
inference(demodulation,[status(thm)],[c_48645,c_340,c_40651,c_40791]) ).
tcf(c_48840,plain,
multiply(iPr_def_15(iPr_def_16),iPr_def_12(iPr_def_29,multiply(inverse(multiply(inverse(iPr_def_10),iPr_def_11)),iPr_def_12(iPr_def_11,multiply(iPr_def_15(iPr_def_16),inverse(iPr_def_14(iPr_def_11))))))) = iPr_def_15(iPr_def_29),
inference(superposition,[status(thm)],[c_4753,c_41643]) ).
tcf(c_48881,plain,
multiply(inverse(multiply(inverse(iPr_def_10),iPr_def_11)),iPr_def_29) = iPr_def_15(iPr_def_29),
inference(demodulation,[status(thm)],[c_48840,c_318,c_319,c_340,c_1750,c_6194,c_40791,c_41635]) ).
tcf(c_50480,plain,
inverse(multiply(inverse(iPr_def_10),iPr_def_11)) = iPr_def_12(iPr_def_15(iPr_def_29),iPr_def_14(iPr_def_29)),
inference(superposition,[status(thm)],[c_48881,c_41530]) ).
tcf(c_50481,plain,
inverse(multiply(inverse(iPr_def_10),iPr_def_11)) = iPr_def_29,
inference(demodulation,[status(thm)],[c_50480,c_318,c_319,c_40999]) ).
tcf(c_50536,plain,
multiply(iPr_def_29,multiply(inverse(iPr_def_10),iPr_def_11)) = iPr_def_29,
inference(superposition,[status(thm)],[c_50481,c_40453]) ).
tcf(c_50564,plain,
iPr_def_15(multiply(inverse(iPr_def_10),iPr_def_11)) = iPr_def_29,
inference(demodulation,[status(thm)],[c_50536,c_40999]) ).
tcf(c_50612,plain,
multiply(inverse(iPr_def_10),iPr_def_11) = iPr_def_14(iPr_def_29),
inference(superposition,[status(thm)],[c_50564,c_340]) ).
tcf(c_50627,plain,
multiply(iPr_def_14(iPr_def_29),inverse(iPr_def_10)) = iPr_def_15(inverse(iPr_def_11)),
inference(demodulation,[status(thm)],[c_29093,c_50612]) ).
tcf(c_50629,plain,
iPr_def_12(iPr_def_29,inverse(iPr_def_10)) = iPr_def_15(inverse(iPr_def_11)),
inference(demodulation,[status(thm)],[c_50627,c_248]) ).
tcf(c_50637,plain,
multiply(iPr_def_14(iPr_def_29),inverse(iPr_def_11)) = iPr_def_15(inverse(iPr_def_10)),
inference(superposition,[status(thm)],[c_50612,c_300]) ).
tcf(c_50639,plain,
iPr_def_12(iPr_def_29,inverse(iPr_def_11)) = iPr_def_15(inverse(iPr_def_10)),
inference(demodulation,[status(thm)],[c_50637,c_248]) ).
tcf(c_50668,plain,
multiply(iPr_def_10,iPr_def_15(inverse(iPr_def_11))) = iPr_def_15(iPr_def_15(iPr_def_16)),
inference(superposition,[status(thm)],[c_50629,c_41980]) ).
tcf(c_50691,plain,
multiply(iPr_def_11,iPr_def_15(inverse(iPr_def_10))) = iPr_def_15(iPr_def_15(iPr_def_16)),
inference(superposition,[status(thm)],[c_50639,c_41980]) ).
tcf(c_51408,plain,
! [X0: $i,X1: $i,X2: $i] : inverse(multiply(iPr_def_29,multiply(inverse(multiply(X0,X1)),multiply(X0,inverse(iPr_def_15(X2)))))) = iPr_def_14(multiply(X2,X1)),
inference(light_normalisation,[status(thm)],[c_458,c_41479,c_50612]) ).
tcf(c_51491,plain,
! [X0: $i] : inverse(multiply(iPr_def_29,multiply(inverse(iPr_def_15(iPr_def_29)),multiply(inverse(iPr_def_12(iPr_def_29,iPr_def_29)),inverse(iPr_def_15(X0)))))) = iPr_def_14(multiply(X0,inverse(iPr_def_16))),
inference(superposition,[status(thm)],[c_42874,c_51408]) ).
tcf(c_51616,plain,
! [X0: $i] : iPr_def_12(X0,iPr_def_15(iPr_def_29)) = iPr_def_15(X0),
inference(demodulation,[status(thm)],[c_51491,c_318,c_319,c_340,c_1578,c_1750,c_5599,c_40618,c_40791,c_40999,c_41014,c_41324,c_41682]) ).
tcf(c_51722,plain,
! [X0: $i] : iPr_def_15(iPr_def_12(X0,iPr_def_16)) = iPr_def_14(X0),
inference(demodulation,[status(thm)],[c_41087,c_51616]) ).
tcf(c_51724,plain,
inverse(iPr_def_16) = iPr_def_15(iPr_def_29),
inference(demodulation,[status(thm)],[c_41321,c_51616]) ).
tcf(c_51725,plain,
iPr_def_15(iPr_def_14(iPr_def_29)) = iPr_def_15(iPr_def_15(iPr_def_16)),
inference(demodulation,[status(thm)],[c_42389,c_51616]) ).
tcf(c_51726,plain,
iPr_def_15(iPr_def_15(iPr_def_16)) = iPr_def_29,
inference(demodulation,[status(thm)],[c_51725,c_319]) ).
tcf(c_51743,plain,
! [X0: $i,X1: $i] : iPr_def_12(iPr_def_14(X0),iPr_def_14(multiply(iPr_def_29,X1))) = iPr_def_14(iPr_def_14(multiply(X0,X1))),
inference(demodulation,[status(thm)],[c_6528,c_51726]) ).
tcf(c_51746,plain,
! [X0: $i] : iPr_def_12(iPr_def_12(X0,iPr_def_29),iPr_def_15(iPr_def_16)) = iPr_def_14(X0),
inference(demodulation,[status(thm)],[c_1874,c_51726]) ).
tcf(c_51751,plain,
iPr_def_14(iPr_def_29) = iPr_def_15(iPr_def_16),
inference(demodulation,[status(thm)],[c_42905,c_51746]) ).
tcf(c_51762,plain,
iPr_def_12(iPr_def_12(iPr_def_29,inverse(iPr_def_16)),iPr_def_14(iPr_def_29)) = iPr_def_29,
inference(demodulation,[status(thm)],[c_48704,c_51751]) ).
tcf(c_51820,plain,
! [X0: $i,X1: $i] : multiply(X0,multiply(iPr_def_14(iPr_def_29),X1)) = iPr_def_14(multiply(iPr_def_15(X0),X1)),
inference(demodulation,[status(thm)],[c_6244,c_51751]) ).
tcf(c_51826,plain,
! [X0: $i,X1: $i] : iPr_def_12(X0,multiply(iPr_def_14(iPr_def_29),X1)) = iPr_def_14(multiply(X0,X1)),
inference(demodulation,[status(thm)],[c_6194,c_51751]) ).
tcf(c_51828,plain,
! [X0: $i] : multiply(X0,inverse(iPr_def_15(X0))) = iPr_def_14(iPr_def_29),
inference(demodulation,[status(thm)],[c_1747,c_51751]) ).
tcf(c_51829,plain,
! [X0: $i] : iPr_def_12(X0,inverse(X0)) = iPr_def_14(iPr_def_29),
inference(demodulation,[status(thm)],[c_1578,c_51751]) ).
tcf(c_51830,plain,
! [X0: $i,X1: $i] : iPr_def_12(X0,iPr_def_12(iPr_def_29,X1)) = iPr_def_14(multiply(X0,X1)),
inference(demodulation,[status(thm)],[c_51826,c_248]) ).
tcf(c_51845,plain,
! [X0: $i,X1: $i] : iPr_def_14(multiply(iPr_def_15(X0),X1)) = iPr_def_15(iPr_def_12(X0,X1)),
inference(demodulation,[status(thm)],[c_51820,c_248,c_40791]) ).
tcf(c_51907,plain,
! [X0: $i,X1: $i] : iPr_def_14(iPr_def_14(multiply(X0,X1))) = iPr_def_12(iPr_def_14(X0),X1),
inference(demodulation,[status(thm)],[c_51743,c_340,c_40999]) ).
tcf(c_52945,plain,
! [X0: $i] : iPr_def_12(iPr_def_12(X0,iPr_def_15(iPr_def_29)),iPr_def_16) = iPr_def_14(X0),
inference(superposition,[status(thm)],[c_51724,c_252]) ).
tcf(c_52954,plain,
! [X0: $i] : iPr_def_12(iPr_def_15(X0),iPr_def_16) = iPr_def_14(X0),
inference(light_normalisation,[status(thm)],[c_52945,c_51616]) ).
tcf(c_52955,plain,
! [X0: $i] : multiply(X0,iPr_def_16) = iPr_def_14(X0),
inference(demodulation,[status(thm)],[c_52954,c_318]) ).
tcf(c_53316,plain,
! [X0: $i] : iPr_def_12(X0,iPr_def_16) = iPr_def_14(iPr_def_14(X0)),
inference(superposition,[status(thm)],[c_52955,c_248]) ).
tcf(c_53335,plain,
! [X0: $i] : iPr_def_12(X0,inverse(iPr_def_12(X0,iPr_def_16))) = iPr_def_15(iPr_def_29),
inference(demodulation,[status(thm)],[c_42466,c_53316]) ).
tcf(c_53340,plain,
! [X0: $i] : iPr_def_12(iPr_def_12(iPr_def_29,X0),iPr_def_16) = iPr_def_12(iPr_def_16,X0),
inference(demodulation,[status(thm)],[c_40775,c_53316]) ).
tcf(c_53432,plain,
! [X0: $i,X1: $i] : multiply(iPr_def_12(X0,iPr_def_16),X1) = iPr_def_12(iPr_def_14(X0),X1),
inference(superposition,[status(thm)],[c_51722,c_318]) ).
tcf(c_53480,plain,
! [X0: $i] : multiply(iPr_def_14(iPr_def_29),iPr_def_12(iPr_def_29,X0)) = X0,
inference(superposition,[status(thm)],[c_51829,c_41355]) ).
tcf(c_53492,plain,
! [X0: $i] : iPr_def_12(iPr_def_29,iPr_def_12(iPr_def_29,X0)) = X0,
inference(demodulation,[status(thm)],[c_53480,c_248]) ).
tcf(c_53566,plain,
! [X0: $i,X1: $i] : multiply(iPr_def_12(X0,inverse(iPr_def_12(iPr_def_29,X1))),X1) = X0,
inference(superposition,[status(thm)],[c_53492,c_41355]) ).
tcf(c_53570,plain,
! [X0: $i] : iPr_def_12(iPr_def_14(X0),inverse(iPr_def_12(iPr_def_29,X0))) = iPr_def_16,
inference(superposition,[status(thm)],[c_53492,c_41332]) ).
tcf(c_53572,plain,
! [X0: $i] : iPr_def_12(iPr_def_14(X0),iPr_def_12(iPr_def_29,inverse(X0))) = iPr_def_16,
inference(demodulation,[status(thm)],[c_53570,c_41324]) ).
tcf(c_53575,plain,
! [X0: $i,X1: $i] : multiply(iPr_def_12(X0,iPr_def_12(iPr_def_29,inverse(X1))),X1) = X0,
inference(demodulation,[status(thm)],[c_53566,c_41324]) ).
tcf(c_53771,plain,
multiply(iPr_def_10,iPr_def_15(inverse(iPr_def_11))) = iPr_def_15(iPr_def_14(iPr_def_29)),
inference(light_normalisation,[status(thm)],[c_50668,c_51751]) ).
tcf(c_53775,plain,
multiply(iPr_def_15(iPr_def_14(iPr_def_29)),inverse(iPr_def_15(inverse(iPr_def_11)))) = iPr_def_15(iPr_def_10),
inference(superposition,[status(thm)],[c_53771,c_300]) ).
tcf(c_53781,plain,
iPr_def_15(inverse(iPr_def_15(inverse(iPr_def_11)))) = iPr_def_15(iPr_def_10),
inference(demodulation,[status(thm)],[c_53775,c_319,c_40999]) ).
tcf(c_53800,plain,
inverse(iPr_def_15(inverse(iPr_def_11))) = iPr_def_14(iPr_def_15(iPr_def_10)),
inference(superposition,[status(thm)],[c_53781,c_340]) ).
tcf(c_53804,plain,
inverse(iPr_def_15(inverse(iPr_def_11))) = iPr_def_10,
inference(demodulation,[status(thm)],[c_53800,c_340]) ).
tcf(c_53874,plain,
multiply(iPr_def_11,iPr_def_15(inverse(iPr_def_10))) = iPr_def_15(iPr_def_14(iPr_def_29)),
inference(light_normalisation,[status(thm)],[c_50691,c_51751]) ).
tcf(c_53878,plain,
multiply(iPr_def_15(iPr_def_14(iPr_def_29)),inverse(iPr_def_15(inverse(iPr_def_10)))) = iPr_def_15(iPr_def_11),
inference(superposition,[status(thm)],[c_53874,c_300]) ).
tcf(c_53884,plain,
iPr_def_15(inverse(iPr_def_15(inverse(iPr_def_10)))) = iPr_def_15(iPr_def_11),
inference(demodulation,[status(thm)],[c_53878,c_319,c_40999]) ).
tcf(c_53903,plain,
inverse(iPr_def_15(inverse(iPr_def_10))) = iPr_def_14(iPr_def_15(iPr_def_11)),
inference(superposition,[status(thm)],[c_53884,c_340]) ).
tcf(c_53907,plain,
inverse(iPr_def_15(inverse(iPr_def_10))) = iPr_def_11,
inference(demodulation,[status(thm)],[c_53903,c_340]) ).
tcf(c_53979,plain,
iPr_def_12(iPr_def_12(iPr_def_29,iPr_def_15(iPr_def_29)),iPr_def_14(iPr_def_29)) = iPr_def_29,
inference(light_normalisation,[status(thm)],[c_51762,c_51724]) ).
tcf(c_54202,plain,
! [X0: $i] : iPr_def_12(iPr_def_16,iPr_def_12(iPr_def_29,X0)) = iPr_def_12(X0,iPr_def_16),
inference(superposition,[status(thm)],[c_53492,c_53340]) ).
tcf(c_54252,plain,
! [X0: $i] : iPr_def_12(X0,iPr_def_12(iPr_def_29,inverse(iPr_def_15(X0)))) = iPr_def_16,
inference(superposition,[status(thm)],[c_340,c_53572]) ).
tcf(c_54430,plain,
! [X0: $i] : multiply(iPr_def_12(X0,iPr_def_16),inverse(iPr_def_12(iPr_def_29,X0))) = iPr_def_16,
inference(superposition,[status(thm)],[c_54202,c_273]) ).
tcf(c_54432,plain,
! [X0: $i] : iPr_def_15(iPr_def_12(iPr_def_12(X0,iPr_def_16),inverse(X0))) = iPr_def_16,
inference(demodulation,[status(thm)],[c_54430,c_40791,c_41324]) ).
tcf(c_54458,plain,
! [X0: $i] : multiply(X0,iPr_def_12(iPr_def_29,inverse(iPr_def_15(iPr_def_15(X0))))) = iPr_def_16,
inference(superposition,[status(thm)],[c_54252,c_318]) ).
tcf(c_54474,plain,
! [X0: $i] : iPr_def_15(iPr_def_12(X0,inverse(iPr_def_15(iPr_def_15(X0))))) = iPr_def_16,
inference(demodulation,[status(thm)],[c_54458,c_40791]) ).
tcf(c_54513,plain,
! [X0: $i] : iPr_def_12(iPr_def_12(X0,iPr_def_16),inverse(X0)) = iPr_def_14(iPr_def_16),
inference(superposition,[status(thm)],[c_54432,c_340]) ).
tcf(c_55583,plain,
! [X0: $i] : iPr_def_12(X0,inverse(iPr_def_15(iPr_def_15(X0)))) = iPr_def_14(iPr_def_16),
inference(superposition,[status(thm)],[c_54474,c_340]) ).
tcf(c_55639,plain,
! [X0: $i] : iPr_def_12(iPr_def_14(iPr_def_16),X0) = iPr_def_14(iPr_def_12(X0,iPr_def_16)),
inference(superposition,[status(thm)],[c_54513,c_252]) ).
tcf(c_55686,plain,
! [X0: $i] : multiply(X0,inverse(iPr_def_15(iPr_def_15(iPr_def_15(X0))))) = iPr_def_14(iPr_def_16),
inference(superposition,[status(thm)],[c_55583,c_318]) ).
tcf(c_55724,plain,
! [X0: $i] : iPr_def_12(iPr_def_14(iPr_def_16),iPr_def_15(X0)) = iPr_def_14(multiply(X0,iPr_def_16)),
inference(superposition,[status(thm)],[c_318,c_55639]) ).
tcf(c_55746,plain,
! [X0: $i] : iPr_def_12(iPr_def_14(iPr_def_16),iPr_def_15(X0)) = iPr_def_12(X0,iPr_def_16),
inference(demodulation,[status(thm)],[c_55724,c_52955,c_53316]) ).
tcf(c_56384,plain,
! [X0: $i,X1: $i] : iPr_def_15(iPr_def_12(iPr_def_14(X0),X1)) = iPr_def_14(multiply(X0,X1)),
inference(superposition,[status(thm)],[c_319,c_51845]) ).
tcf(c_56403,plain,
! [X0: $i,X1: $i] : iPr_def_15(iPr_def_15(iPr_def_12(X0,X1))) = multiply(iPr_def_15(X0),X1),
inference(superposition,[status(thm)],[c_51845,c_319]) ).
tcf(c_56575,plain,
! [X0: $i,X1: $i] : iPr_def_12(iPr_def_14(multiply(X0,X1)),inverse(X1)) = iPr_def_14(iPr_def_14(iPr_def_15(X0))),
inference(superposition,[status(thm)],[c_300,c_51907]) ).
tcf(c_56622,plain,
! [X0: $i,X1: $i] : iPr_def_12(multiply(X0,X1),iPr_def_16) = iPr_def_12(iPr_def_14(X0),X1),
inference(superposition,[status(thm)],[c_51907,c_53316]) ).
tcf(c_56640,plain,
! [X0: $i,X1: $i] : iPr_def_12(iPr_def_14(multiply(X0,X1)),inverse(X1)) = iPr_def_14(X0),
inference(demodulation,[status(thm)],[c_56575,c_318,c_52955,c_53316]) ).
tcf(c_57294,plain,
! [X0: $i,X1: $i] : multiply(multiply(X0,iPr_def_12(iPr_def_29,inverse(X1))),X1) = iPr_def_15(X0),
inference(superposition,[status(thm)],[c_318,c_53575]) ).
tcf(c_57365,plain,
! [X0: $i,X1: $i] : multiply(iPr_def_15(iPr_def_12(X0,inverse(X1))),X1) = iPr_def_15(X0),
inference(demodulation,[status(thm)],[c_57294,c_40791]) ).
tcf(c_57808,plain,
iPr_def_15(inverse(iPr_def_15(iPr_def_15(iPr_def_15(iPr_def_29))))) = iPr_def_14(iPr_def_16),
inference(superposition,[status(thm)],[c_55686,c_40999]) ).
tcf(c_57870,plain,
inverse(iPr_def_15(iPr_def_15(iPr_def_15(iPr_def_29)))) = iPr_def_14(iPr_def_14(iPr_def_16)),
inference(superposition,[status(thm)],[c_57808,c_340]) ).
tcf(c_57874,plain,
inverse(iPr_def_15(iPr_def_15(iPr_def_15(iPr_def_29)))) = iPr_def_12(iPr_def_16,iPr_def_16),
inference(demodulation,[status(thm)],[c_57870,c_53316]) ).
tcf(c_60060,plain,
multiply(iPr_def_15(iPr_def_12(iPr_def_29,iPr_def_15(iPr_def_29))),iPr_def_14(iPr_def_29)) = iPr_def_15(iPr_def_15(iPr_def_29)),
inference(superposition,[status(thm)],[c_53979,c_56403]) ).
tcf(c_60089,plain,
multiply(iPr_def_15(iPr_def_15(iPr_def_29)),iPr_def_14(iPr_def_29)) = iPr_def_15(iPr_def_15(iPr_def_29)),
inference(demodulation,[status(thm)],[c_60060,c_51616]) ).
tcf(c_60618,plain,
! [X0: $i] : multiply(iPr_def_15(iPr_def_15(iPr_def_29)),iPr_def_12(X0,iPr_def_16)) = iPr_def_15(X0),
inference(superposition,[status(thm)],[c_53335,c_57365]) ).
tcf(c_60870,plain,
multiply(iPr_def_15(iPr_def_15(iPr_def_29)),iPr_def_29) = iPr_def_15(iPr_def_15(iPr_def_15(iPr_def_29))),
inference(superposition,[status(thm)],[c_60089,c_41527]) ).
tcf(c_60898,plain,
! [X0: $i] : multiply(iPr_def_15(iPr_def_15(iPr_def_29)),multiply(X0,iPr_def_16)) = iPr_def_15(iPr_def_15(X0)),
inference(superposition,[status(thm)],[c_318,c_60618]) ).
tcf(c_60931,plain,
! [X0: $i] : multiply(iPr_def_15(iPr_def_15(iPr_def_29)),iPr_def_14(X0)) = iPr_def_15(iPr_def_15(X0)),
inference(demodulation,[status(thm)],[c_60898,c_52955]) ).
tcf(c_60970,plain,
! [X0: $i] : inverse(multiply(iPr_def_29,multiply(inverse(iPr_def_15(iPr_def_15(iPr_def_15(iPr_def_29)))),multiply(iPr_def_15(iPr_def_15(iPr_def_29)),inverse(iPr_def_15(X0)))))) = iPr_def_14(multiply(X0,iPr_def_29)),
inference(superposition,[status(thm)],[c_60870,c_51408]) ).
tcf(c_60988,plain,
! [X0: $i] : inverse(iPr_def_15(inverse(iPr_def_15(X0)))) = iPr_def_14(multiply(X0,iPr_def_29)),
inference(demodulation,[status(thm)],[c_60970,c_318,c_340,c_1750,c_40999,c_51845,c_53432,c_56384,c_57874]) ).
tcf(c_61267,plain,
! [X0: $i] : iPr_def_14(multiply(iPr_def_14(X0),iPr_def_29)) = inverse(iPr_def_15(inverse(X0))),
inference(superposition,[status(thm)],[c_319,c_60988]) ).
tcf(c_61314,plain,
! [X0: $i] : inverse(iPr_def_15(inverse(X0))) = iPr_def_14(iPr_def_12(X0,iPr_def_29)),
inference(demodulation,[status(thm)],[c_61267,c_248]) ).
tcf(c_61347,plain,
iPr_def_14(iPr_def_12(iPr_def_10,iPr_def_29)) = iPr_def_11,
inference(demodulation,[status(thm)],[c_53907,c_61314]) ).
tcf(c_61348,plain,
iPr_def_14(iPr_def_12(iPr_def_11,iPr_def_29)) = iPr_def_10,
inference(demodulation,[status(thm)],[c_53804,c_61314]) ).
tcf(c_61398,plain,
iPr_def_12(iPr_def_10,iPr_def_29) = iPr_def_15(iPr_def_11),
inference(superposition,[status(thm)],[c_61347,c_319]) ).
tcf(c_61440,plain,
iPr_def_12(iPr_def_11,iPr_def_29) = iPr_def_15(iPr_def_10),
inference(superposition,[status(thm)],[c_61348,c_319]) ).
tcf(c_61472,plain,
multiply(iPr_def_15(iPr_def_11),inverse(iPr_def_29)) = iPr_def_10,
inference(superposition,[status(thm)],[c_61398,c_273]) ).
tcf(c_61473,plain,
iPr_def_12(iPr_def_15(iPr_def_11),iPr_def_14(iPr_def_29)) = iPr_def_14(iPr_def_10),
inference(superposition,[status(thm)],[c_61398,c_41529]) ).
tcf(c_61474,plain,
multiply(iPr_def_11,iPr_def_14(iPr_def_29)) = iPr_def_14(iPr_def_10),
inference(demodulation,[status(thm)],[c_61473,c_318]) ).
tcf(c_61482,plain,
iPr_def_12(iPr_def_14(iPr_def_15(iPr_def_11)),inverse(iPr_def_29)) = iPr_def_14(iPr_def_14(iPr_def_10)),
inference(superposition,[status(thm)],[c_61472,c_51907]) ).
tcf(c_61509,plain,
iPr_def_12(iPr_def_11,inverse(iPr_def_29)) = iPr_def_12(iPr_def_10,iPr_def_16),
inference(demodulation,[status(thm)],[c_61482,c_340,c_53316]) ).
tcf(c_61547,plain,
iPr_def_12(iPr_def_14(iPr_def_14(iPr_def_10)),inverse(iPr_def_14(iPr_def_29))) = iPr_def_14(iPr_def_11),
inference(superposition,[status(thm)],[c_61474,c_56640]) ).
tcf(c_61571,plain,
iPr_def_12(iPr_def_12(iPr_def_10,iPr_def_16),iPr_def_29) = iPr_def_14(iPr_def_11),
inference(demodulation,[status(thm)],[c_61547,c_41479,c_53316]) ).
tcf(c_61971,plain,
! [X0: $i] : multiply(iPr_def_14(iPr_def_12(X0,iPr_def_29)),iPr_def_15(inverse(X0))) = iPr_def_29,
inference(superposition,[status(thm)],[c_61314,c_40453]) ).
tcf(c_61989,plain,
! [X0: $i] : multiply(inverse(X0),iPr_def_14(iPr_def_12(X0,iPr_def_29))) = iPr_def_14(iPr_def_29),
inference(superposition,[status(thm)],[c_61314,c_51828]) ).
tcf(c_61992,plain,
! [X0: $i] : iPr_def_12(iPr_def_12(X0,iPr_def_29),iPr_def_15(inverse(X0))) = iPr_def_29,
inference(demodulation,[status(thm)],[c_61971,c_247,c_38062]) ).
tcf(c_62294,plain,
iPr_def_12(iPr_def_12(iPr_def_16,iPr_def_29),iPr_def_15(iPr_def_15(iPr_def_29))) = iPr_def_29,
inference(superposition,[status(thm)],[c_51724,c_61992]) ).
tcf(c_62296,plain,
! [X0: $i] : iPr_def_12(iPr_def_12(iPr_def_15(inverse(X0)),iPr_def_29),iPr_def_15(iPr_def_14(iPr_def_12(X0,iPr_def_29)))) = iPr_def_29,
inference(superposition,[status(thm)],[c_61314,c_61992]) ).
tcf(c_62321,plain,
! [X0: $i] : iPr_def_12(multiply(inverse(X0),iPr_def_29),iPr_def_12(X0,iPr_def_29)) = iPr_def_29,
inference(demodulation,[status(thm)],[c_62296,c_318,c_319]) ).
tcf(c_63292,plain,
iPr_def_12(multiply(inverse(iPr_def_14(inverse(iPr_def_29))),iPr_def_29),iPr_def_16) = iPr_def_29,
inference(superposition,[status(thm)],[c_1580,c_62321]) ).
tcf(c_63307,plain,
iPr_def_12(iPr_def_14(inverse(iPr_def_14(inverse(iPr_def_29)))),iPr_def_29) = iPr_def_29,
inference(demodulation,[status(thm)],[c_63292,c_56622]) ).
tcf(c_63336,plain,
iPr_def_14(inverse(iPr_def_14(inverse(iPr_def_29)))) = multiply(iPr_def_29,inverse(iPr_def_29)),
inference(superposition,[status(thm)],[c_63307,c_273]) ).
tcf(c_63343,plain,
iPr_def_14(inverse(iPr_def_14(inverse(iPr_def_29)))) = iPr_def_15(inverse(iPr_def_29)),
inference(demodulation,[status(thm)],[c_63336,c_40999]) ).
tcf(c_63359,plain,
inverse(iPr_def_14(inverse(iPr_def_29))) = iPr_def_15(iPr_def_15(inverse(iPr_def_29))),
inference(superposition,[status(thm)],[c_63343,c_319]) ).
tcf(c_63367,plain,
iPr_def_12(iPr_def_15(inverse(iPr_def_29)),iPr_def_14(inverse(iPr_def_29))) = iPr_def_16,
inference(superposition,[status(thm)],[c_63343,c_1580]) ).
tcf(c_63368,plain,
multiply(inverse(iPr_def_29),iPr_def_14(inverse(iPr_def_29))) = iPr_def_16,
inference(demodulation,[status(thm)],[c_63367,c_318]) ).
tcf(c_63503,plain,
multiply(iPr_def_15(iPr_def_15(inverse(iPr_def_29))),iPr_def_14(iPr_def_12(iPr_def_14(inverse(iPr_def_29)),iPr_def_29))) = iPr_def_14(iPr_def_29),
inference(superposition,[status(thm)],[c_63359,c_61989]) ).
tcf(c_63533,plain,
multiply(inverse(iPr_def_29),iPr_def_15(iPr_def_15(inverse(iPr_def_29)))) = iPr_def_15(iPr_def_29),
inference(superposition,[status(thm)],[c_63359,c_41635]) ).
tcf(c_63544,plain,
multiply(iPr_def_15(iPr_def_15(inverse(iPr_def_29))),iPr_def_14(iPr_def_16)) = iPr_def_14(iPr_def_29),
inference(demodulation,[status(thm)],[c_63503,c_1580]) ).
tcf(c_70153,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(inverse(multiply(inverse(multiply(inverse(iPr_def_14(X0)),iPr_def_14(X0))),multiply(inverse(iPr_def_10),multiply(a,inverse(multiply(multiply(X1,inverse(X2)),inverse(b))))))),X2) = X1,
inference(light_normalisation,[status(thm)],[c_2673,c_52955]) ).
tcf(c_70212,plain,
! [X0: $i,X1: $i] : multiply(inverse(multiply(inverse(multiply(inverse(iPr_def_14(X0)),iPr_def_14(X0))),multiply(inverse(iPr_def_10),multiply(a,inverse(multiply(iPr_def_14(iPr_def_29),inverse(b))))))),iPr_def_15(X1)) = X1,
inference(superposition,[status(thm)],[c_51828,c_70153]) ).
tcf(c_70326,plain,
! [X0: $i] : multiply(inverse(iPr_def_29),iPr_def_15(X0)) = X0,
inference(demodulation,[status(thm)],[c_70212,c_248,c_333,c_340,c_40453,c_40618,c_40999,c_41324,c_51830]) ).
tcf(c_70446,plain,
iPr_def_15(inverse(iPr_def_29)) = iPr_def_15(iPr_def_29),
inference(demodulation,[status(thm)],[c_63533,c_70326]) ).
tcf(c_70447,plain,
multiply(iPr_def_15(iPr_def_15(iPr_def_29)),iPr_def_14(iPr_def_16)) = iPr_def_14(iPr_def_29),
inference(demodulation,[status(thm)],[c_63544,c_70446]) ).
tcf(c_70453,plain,
iPr_def_14(iPr_def_29) = iPr_def_29,
inference(demodulation,[status(thm)],[c_70447,c_319,c_51751,c_60931]) ).
tcf(c_70511,plain,
inverse(iPr_def_29) = iPr_def_29,
inference(demodulation,[status(thm)],[c_41479,c_70453]) ).
tcf(c_70515,plain,
multiply(iPr_def_29,iPr_def_14(iPr_def_29)) = iPr_def_16,
inference(demodulation,[status(thm)],[c_63368,c_70511]) ).
tcf(c_70519,plain,
iPr_def_12(iPr_def_10,iPr_def_16) = iPr_def_12(iPr_def_11,iPr_def_29),
inference(demodulation,[status(thm)],[c_61509,c_70511]) ).
tcf(c_70521,plain,
iPr_def_12(iPr_def_16,iPr_def_29) = iPr_def_14(iPr_def_16),
inference(demodulation,[status(thm)],[c_42804,c_70511]) ).
tcf(c_70526,plain,
iPr_def_12(iPr_def_14(iPr_def_16),iPr_def_15(iPr_def_15(iPr_def_29))) = iPr_def_29,
inference(demodulation,[status(thm)],[c_62294,c_70521]) ).
tcf(c_70531,plain,
iPr_def_15(iPr_def_16) = iPr_def_29,
inference(demodulation,[status(thm)],[c_70526,c_318,c_40999,c_55746]) ).
tcf(c_70534,plain,
iPr_def_12(iPr_def_10,iPr_def_16) = iPr_def_15(iPr_def_10),
inference(demodulation,[status(thm)],[c_70519,c_61440]) ).
tcf(c_70536,plain,
iPr_def_12(iPr_def_15(iPr_def_10),iPr_def_29) = iPr_def_14(iPr_def_11),
inference(demodulation,[status(thm)],[c_61571,c_70534]) ).
tcf(c_70538,plain,
multiply(iPr_def_10,iPr_def_29) = iPr_def_14(iPr_def_11),
inference(demodulation,[status(thm)],[c_70536,c_318]) ).
tcf(c_70544,plain,
iPr_def_16 = iPr_def_29,
inference(demodulation,[status(thm)],[c_70515,c_319,c_40999]) ).
tcf(c_70607,plain,
inverse(iPr_def_16) = iPr_def_15(iPr_def_16),
inference(demodulation,[status(thm)],[c_51724,c_70544]) ).
tcf(c_70633,plain,
! [X0: $i] : multiply(iPr_def_16,X0) = iPr_def_15(X0),
inference(demodulation,[status(thm)],[c_40999,c_70544]) ).
tcf(c_70637,plain,
! [X0: $i] : iPr_def_14(X0) = iPr_def_15(X0),
inference(demodulation,[status(thm)],[c_70633,c_1750]) ).
tcf(c_70675,plain,
! [X0: $i] : iPr_def_14(iPr_def_14(X0)) = X0,
inference(demodulation,[status(thm)],[c_319,c_70637]) ).
tcf(c_70677,plain,
! [X0: $i] : iPr_def_14(iPr_def_12(X0,iPr_def_16)) = iPr_def_14(X0),
inference(demodulation,[status(thm)],[c_51722,c_70637]) ).
tcf(c_70685,plain,
! [X0: $i] : iPr_def_12(X0,iPr_def_16) = X0,
inference(demodulation,[status(thm)],[c_53316,c_70675]) ).
tcf(c_71258,plain,
iPr_def_15(iPr_def_16) = iPr_def_16,
inference(light_normalisation,[status(thm)],[c_70531,c_70544]) ).
tcf(c_71267,plain,
inverse(iPr_def_16) = iPr_def_16,
inference(light_normalisation,[status(thm)],[c_70607,c_71258]) ).
tcf(c_71269,plain,
! [X0: $i] : multiply(iPr_def_12(X0,iPr_def_16),iPr_def_16) = X0,
inference(superposition,[status(thm)],[c_71267,c_273]) ).
tcf(c_71273,plain,
! [X0: $i] : iPr_def_14(iPr_def_12(X0,iPr_def_16)) = X0,
inference(demodulation,[status(thm)],[c_71269,c_52955]) ).
tcf(c_71274,plain,
! [X0: $i] : iPr_def_14(X0) = X0,
inference(light_normalisation,[status(thm)],[c_71273,c_70677,c_70685]) ).
tcf(c_71279,plain,
! [X0: $i] : multiply(X0,iPr_def_16) = X0,
inference(demodulation,[status(thm)],[c_52955,c_71274]) ).
tcf(c_71327,plain,
multiply(iPr_def_10,iPr_def_16) = iPr_def_14(iPr_def_11),
inference(light_normalisation,[status(thm)],[c_70538,c_70544]) ).
tcf(c_71328,plain,
iPr_def_14(iPr_def_11) = iPr_def_10,
inference(superposition,[status(thm)],[c_71279,c_71327]) ).
tcf(c_71330,plain,
iPr_def_10 = iPr_def_11,
inference(demodulation,[status(thm)],[c_71328,c_71274]) ).
tcf(c_71331,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[c_71330,c_64]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GRP508-1 : TPTP v9.3.1. Bugfixed v2.7.0.
% 0.00/0.03 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.08/0.35 % Computer : n001.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Wed Sep 23 15:02:36 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.08/0.35 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.11/0.39 Running UEQ theorem proving
% 0.11/0.39 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.11/0.40
% 0.11/0.40 % ======== iProver multi-core TPTP/SMT =========
% 0.11/0.40
% 0.11/0.40 % Detected problem language: tptp
% 0.11/0.42 % Proving...
% 164.56/23.29 WARNING - Clausifier option not provided in the heuristic config "heur/vip2_118404", setting default options.
% 164.56/23.29 % SZS status Started for theBenchmark.p
% 164.56/23.29 % SZS status Unsatisfiable for theBenchmark.p
% 164.56/23.29
% 164.56/23.29 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 164.56/23.29
% 164.56/23.29 % ------ iProver source info
% 164.56/23.29
% 164.56/23.29 % git: date: 2026-07-19 20:42:38 +0200
% 164.56/23.29 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 164.56/23.29 % git: non_committed_changes: false
% 164.56/23.29
% 164.56/23.29 % ------ Parsing...% successful
% 164.56/23.29
% 164.56/23.29
% 164.56/23.29 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 164.56/23.29
% 164.56/23.29 % ------ Preprocessing... sup_sim: 0 sf_s rm: 0 0s sf_e pe_s pe_e %
% 164.56/23.29
% 164.56/23.29 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 164.56/23.29
% 164.56/23.29 % ------ Preprocessing... sf_s rm: 0 0s sf_e
% 164.56/23.29 % ------ Proving...
% 164.56/23.29 % ------ Problem Properties
% 164.56/23.29
% 164.56/23.29 %
% 164.56/23.29 % clauses 4
% 164.56/23.29 % conjectures 1
% 164.56/23.29 % EPR 1
% 164.56/23.29 % Horn 4
% 164.56/23.29 % unary 4
% 164.56/23.29 % binary 0
% 164.56/23.29 % lits 4
% 164.56/23.29 % lits eq 4
% 164.56/23.29 % fd_pure 0
% 164.56/23.29 % fd_pseudo 0
% 164.56/23.29 % fd_cond 0
% 164.56/23.29 % fd_pseudo_cond 0
% 164.56/23.29 % AC symbols 0
% 164.56/23.29
% 164.56/23.29 % ------ Input Options Time Limit: Unbounded
% 164.56/23.29
% 164.56/23.29
% 164.56/23.29 % ------
% 164.56/23.29 % Current options:
% 164.56/23.29 % ------
% 164.56/23.29
% 164.56/23.29
% 164.56/23.29 %
% 164.56/23.29
% 164.56/23.29 % ------ Proving...
% 164.56/23.29 %
% 164.56/23.29
% 164.56/23.29 % SZS status Unsatisfiable for theBenchmark.p
% 164.56/23.29
% 164.56/23.29 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 101.20/23.32
% 101.20/23.32
%------------------------------------------------------------------------------