%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : GRP411-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 : n012.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 01:33:40 PM UTC 2026
% Result : Unsatisfiable 27.12s 4.67s
% Output : CNFRefutation 27.12s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats ran out of CPU time)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X2,X0,X1] : multiply(multiply(inverse(multiply(X0,inverse(multiply(X1,X2)))),multiply(X0,inverse(X2))),inverse(multiply(inverse(X2),X2))) = X1,
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] : multiply(multiply(inverse(multiply(X0,inverse(multiply(X1,X2)))),multiply(X0,inverse(X2))),inverse(multiply(inverse(X2),X2))) = X1,
inference(cnf_transformation,[],[f1]) ).
tcf(c_52,negated_conjecture,
multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3)),
inference(cnf_transformation,[],[f2]) ).
tcf(c_61,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : multiply(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(inverse(multiply(inverse(X2),X2))))),inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2))))) = multiply(inverse(multiply(X3,inverse(multiply(X1,X2)))),multiply(X3,inverse(X2))),
inference(superposition,[status(thm)],[c_51,c_51]) ).
tcf(c_62,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(multiply(inverse(X0),multiply(multiply(inverse(multiply(X1,inverse(multiply(X0,X2)))),multiply(X1,inverse(X2))),inverse(X2))),inverse(multiply(inverse(X2),X2))) = inverse(X2),
inference(superposition,[status(thm)],[c_51,c_51]) ).
tcf(c_63,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : multiply(multiply(inverse(multiply(multiply(inverse(multiply(X0,inverse(multiply(X1,X2)))),multiply(X0,inverse(X2))),inverse(multiply(X3,multiply(inverse(X2),X2))))),X1),inverse(multiply(inverse(multiply(inverse(X2),X2)),multiply(inverse(X2),X2)))) = X3,
inference(superposition,[status(thm)],[c_51,c_51]) ).
tcf(c_64,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(inverse(multiply(X0,inverse(multiply(X1,X2)))),multiply(X0,inverse(X2))) = iPr_def_10(X1,X2),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_10])],[c_61]) ).
tcf(c_65,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(inverse(multiply(inverse(X2),X2))))),inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2))))) = iPr_def_10(X1,X2),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_61]) ).
tcf(c_66,plain,
! [X0: $i,X1: $i] : multiply(iPr_def_10(X0,X1),inverse(multiply(inverse(X1),X1))) = X0,
inference(demodulation,[status(thm)],[c_51,c_64]) ).
tcf(c_80,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),multiply(iPr_def_10(X0,X1),inverse(X1))) = iPr_def_10(inverse(X1),X1),
inference(superposition,[status(thm)],[c_66,c_64]) ).
tcf(c_82,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(inverse(multiply(inverse(X2),X2))))) = iPr_def_10(iPr_def_10(X1,X2),inverse(multiply(inverse(X2),X2))),
inference(superposition,[status(thm)],[c_66,c_64]) ).
tcf(c_83,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(inverse(multiply(iPr_def_10(X0,X1),inverse(multiply(X2,multiply(inverse(X1),X1))))),X0) = iPr_def_10(X2,multiply(inverse(X1),X1)),
inference(superposition,[status(thm)],[c_66,c_64]) ).
tcf(c_84,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : multiply(inverse(multiply(X0,inverse(iPr_def_10(X1,X2)))),multiply(X0,inverse(multiply(X3,inverse(X2))))) = iPr_def_10(inverse(multiply(X3,inverse(multiply(X1,X2)))),multiply(X3,inverse(X2))),
inference(superposition,[status(thm)],[c_64,c_64]) ).
tcf(c_99,plain,
! [X0: $i,X1: $i] : multiply(iPr_def_10(X0,inverse(multiply(inverse(X1),X1))),inverse(multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(multiply(inverse(X1),X1))))) = iPr_def_10(multiply(X0,inverse(multiply(inverse(X1),X1))),X1),
inference(superposition,[status(thm)],[c_64,c_65]) ).
tcf(c_102,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(multiply(inverse(X0),multiply(iPr_def_10(X0,X1),inverse(inverse(multiply(inverse(X2),X2))))),inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2))))) = iPr_def_10(multiply(inverse(X1),X1),X2),
inference(superposition,[status(thm)],[c_66,c_65]) ).
tcf(c_109,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : multiply(multiply(inverse(iPr_def_10(X0,X1)),multiply(multiply(inverse(multiply(X2,inverse(X0))),multiply(X2,inverse(inverse(multiply(inverse(X1),X1))))),inverse(inverse(multiply(inverse(X3),X3))))),inverse(multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(multiply(inverse(X3),X3))))) = iPr_def_10(multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(multiply(inverse(X1),X1))),X3),
inference(superposition,[status(thm)],[c_65,c_65]) ).
tcf(c_115,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] : multiply(multiply(inverse(multiply(multiply(inverse(multiply(X0,inverse(iPr_def_10(X1,X2)))),multiply(X0,inverse(multiply(X3,inverse(X2))))),inverse(multiply(X4,multiply(inverse(multiply(X3,inverse(X2))),multiply(X3,inverse(X2))))))),inverse(multiply(X3,inverse(multiply(X1,X2))))),inverse(multiply(inverse(multiply(inverse(multiply(X3,inverse(X2))),multiply(X3,inverse(X2)))),multiply(inverse(multiply(X3,inverse(X2))),multiply(X3,inverse(X2)))))) = X4,
inference(superposition,[status(thm)],[c_64,c_63]) ).
tcf(c_133,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] : multiply(multiply(inverse(X0),multiply(multiply(inverse(multiply(multiply(inverse(multiply(multiply(inverse(multiply(X1,inverse(multiply(X2,X3)))),multiply(X1,inverse(X3))),inverse(multiply(X4,multiply(inverse(X3),X3))))),X2),inverse(multiply(X0,multiply(inverse(multiply(inverse(X3),X3)),multiply(inverse(X3),X3)))))),X4),inverse(multiply(inverse(multiply(inverse(X3),X3)),multiply(inverse(X3),X3))))),inverse(multiply(inverse(multiply(inverse(multiply(inverse(X3),X3)),multiply(inverse(X3),X3))),multiply(inverse(multiply(inverse(X3),X3)),multiply(inverse(X3),X3))))) = inverse(multiply(inverse(multiply(inverse(X3),X3)),multiply(inverse(X3),X3))),
inference(superposition,[status(thm)],[c_63,c_62]) ).
tcf(c_139,plain,
! [X0: $i,X1: $i] : iPr_def_10(multiply(X0,inverse(multiply(inverse(X1),X1))),X1) = X0,
inference(demodulation,[status(thm)],[c_99,c_66]) ).
tcf(c_163,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : multiply(multiply(inverse(X0),multiply(multiply(inverse(multiply(multiply(inverse(multiply(iPr_def_10(X1,X2),inverse(multiply(X3,multiply(inverse(X2),X2))))),X1),inverse(multiply(X0,multiply(inverse(multiply(inverse(X2),X2)),multiply(inverse(X2),X2)))))),X3),inverse(multiply(inverse(multiply(inverse(X2),X2)),multiply(inverse(X2),X2))))),inverse(multiply(inverse(multiply(inverse(multiply(inverse(X2),X2)),multiply(inverse(X2),X2))),multiply(inverse(multiply(inverse(X2),X2)),multiply(inverse(X2),X2))))) = inverse(multiply(inverse(multiply(inverse(X2),X2)),multiply(inverse(X2),X2))),
inference(demodulation,[status(thm)],[c_133,c_64]) ).
tcf(c_309,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : multiply(inverse(iPr_def_10(X0,multiply(inverse(X1),X1))),multiply(inverse(multiply(iPr_def_10(inverse(multiply(X2,X3)),X1),inverse(multiply(X0,multiply(inverse(X1),X1))))),inverse(X3))) = iPr_def_10(X2,X3),
inference(superposition,[status(thm)],[c_83,c_64]) ).
tcf(c_347,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_10(multiply(X0,inverse(iPr_def_10(iPr_def_10(inverse(multiply(inverse(X1),X1)),X1),inverse(multiply(inverse(X1),X1))))),multiply(X2,inverse(inverse(multiply(inverse(X1),X1))))) = X0,
inference(superposition,[status(thm)],[c_82,c_139]) ).
tcf(c_354,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(inverse(multiply(inverse(X2),X2))))) = multiply(inverse(multiply(X3,inverse(X1))),multiply(X3,inverse(inverse(multiply(inverse(X2),X2))))),
inference(superposition,[status(thm)],[c_82,c_82]) ).
tcf(c_399,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] : multiply(inverse(multiply(X0,inverse(iPr_def_10(X1,X2)))),multiply(X0,inverse(multiply(X3,inverse(X2))))) = multiply(inverse(multiply(X4,inverse(iPr_def_10(X1,X2)))),multiply(X4,inverse(multiply(X3,inverse(X2))))),
inference(superposition,[status(thm)],[c_84,c_84]) ).
tcf(c_455,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(inverse(X0),multiply(iPr_def_10(X0,X1),inverse(inverse(multiply(inverse(X2),X2))))) = iPr_def_10(iPr_def_10(multiply(inverse(X1),X1),X2),inverse(multiply(inverse(X2),X2))),
inference(superposition,[status(thm)],[c_102,c_139]) ).
tcf(c_457,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : iPr_def_10(multiply(multiply(inverse(X0),multiply(iPr_def_10(X0,X1),inverse(inverse(multiply(inverse(X2),X2))))),inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2))))),inverse(multiply(inverse(X2),X2))) = multiply(inverse(multiply(X3,inverse(multiply(inverse(X1),X1)))),multiply(X3,inverse(inverse(multiply(inverse(X2),X2))))),
inference(superposition,[status(thm)],[c_102,c_82]) ).
tcf(c_463,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : multiply(multiply(inverse(X0),multiply(iPr_def_10(X0,X1),inverse(inverse(multiply(inverse(X2),X2))))),inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2))))) = multiply(multiply(inverse(X3),multiply(iPr_def_10(X3,X1),inverse(inverse(multiply(inverse(X2),X2))))),inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2))))),
inference(superposition,[status(thm)],[c_102,c_102]) ).
tcf(c_600,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(inverse(multiply(inverse(X2),X2))))) = iPr_def_11(X1,X2),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_11])],[c_354]) ).
tcf(c_602,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : multiply(inverse(multiply(X0,inverse(iPr_def_10(X1,X2)))),multiply(X0,inverse(multiply(X3,inverse(X2))))) = iPr_def_12(X1,X2,X3),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_12])],[c_399]) ).
tcf(c_640,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_10(multiply(multiply(inverse(X0),multiply(iPr_def_10(X0,X1),inverse(inverse(multiply(inverse(X2),X2))))),inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2))))),inverse(multiply(inverse(X2),X2))) = iPr_def_11(multiply(inverse(X1),X1),X2),
inference(demodulation,[status(thm)],[c_457,c_600]) ).
tcf(c_641,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(inverse(X0),multiply(iPr_def_10(X0,X1),inverse(inverse(multiply(inverse(X2),X2))))) = iPr_def_11(multiply(inverse(X1),X1),X2),
inference(demodulation,[status(thm)],[c_640,c_139]) ).
tcf(c_651,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(multiply(inverse(X0),multiply(iPr_def_10(X0,X1),inverse(inverse(multiply(inverse(X2),X2))))),inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2))))) = iPr_def_13(X1,X2),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_13])],[c_463]) ).
tcf(c_835,plain,
! [X0: $i,X1: $i] : iPr_def_10(iPr_def_10(X0,X1),inverse(multiply(inverse(X1),X1))) = iPr_def_11(X0,X1),
inference(demodulation,[status(thm)],[c_82,c_600]) ).
tcf(c_836,plain,
! [X0: $i,X1: $i] : multiply(iPr_def_11(X0,X1),inverse(multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(multiply(inverse(X1),X1))))) = iPr_def_10(X0,X1),
inference(demodulation,[status(thm)],[c_65,c_600]) ).
tcf(c_839,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_10(inverse(multiply(X0,inverse(multiply(X1,X2)))),multiply(X0,inverse(X2))) = iPr_def_12(X1,X2,X0),
inference(demodulation,[status(thm)],[c_84,c_602]) ).
tcf(c_840,plain,
! [X0: $i,X1: $i] : iPr_def_10(multiply(inverse(X0),X0),X1) = iPr_def_13(X0,X1),
inference(demodulation,[status(thm)],[c_102,c_651]) ).
tcf(c_1649,plain,
! [X0: $i,X1: $i] : multiply(iPr_def_13(X0,X1),inverse(multiply(inverse(X1),X1))) = multiply(inverse(X0),X0),
inference(superposition,[status(thm)],[c_840,c_66]) ).
tcf(c_1650,plain,
! [X0: $i] : iPr_def_13(inverse(multiply(inverse(X0),X0)),X0) = inverse(inverse(multiply(inverse(X0),X0))),
inference(superposition,[status(thm)],[c_840,c_139]) ).
tcf(c_1653,plain,
! [X0: $i,X1: $i] : iPr_def_10(iPr_def_13(X0,X1),inverse(multiply(inverse(X1),X1))) = iPr_def_11(multiply(inverse(X0),X0),X1),
inference(superposition,[status(thm)],[c_840,c_835]) ).
tcf(c_1660,plain,
! [X0: $i,X1: $i] : iPr_def_10(inverse(X0),multiply(iPr_def_10(X0,X1),inverse(X1))) = iPr_def_12(inverse(X1),X1,iPr_def_10(X0,X1)),
inference(superposition,[status(thm)],[c_66,c_839]) ).
tcf(c_1700,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_13(multiply(X0,inverse(inverse(multiply(inverse(X1),X1)))),X2) = iPr_def_10(iPr_def_11(inverse(multiply(inverse(X1),X1)),X1),X2),
inference(superposition,[status(thm)],[c_600,c_840]) ).
tcf(c_1707,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(inverse(multiply(iPr_def_10(X0,inverse(X1)),inverse(iPr_def_10(X2,X1)))),X0) = iPr_def_12(X2,X1,inverse(inverse(X1))),
inference(superposition,[status(thm)],[c_66,c_602]) ).
tcf(c_1896,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : multiply(inverse(X0),multiply(iPr_def_10(X0,X1),inverse(inverse(multiply(inverse(X2),X2))))) = multiply(inverse(X3),multiply(iPr_def_10(X3,X1),inverse(inverse(multiply(inverse(X2),X2))))),
inference(superposition,[status(thm)],[c_455,c_455]) ).
tcf(c_1904,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : iPr_def_10(multiply(X0,inverse(iPr_def_10(iPr_def_10(inverse(multiply(inverse(X1),X1)),X1),inverse(multiply(inverse(X1),X1))))),iPr_def_10(X2,multiply(inverse(X3),X3))) = X0,
inference(superposition,[status(thm)],[c_83,c_347]) ).
tcf(c_1917,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : iPr_def_10(multiply(X0,inverse(iPr_def_11(inverse(multiply(inverse(X1),X1)),X1))),iPr_def_10(X2,multiply(inverse(X3),X3))) = X0,
inference(demodulation,[status(thm)],[c_1904,c_835]) ).
tcf(c_1918,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(inverse(X0),multiply(iPr_def_10(X0,X1),inverse(inverse(multiply(inverse(X2),X2))))) = iPr_def_14(X1,X2),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_14])],[c_1896]) ).
tcf(c_2011,plain,
! [X0: $i,X1: $i] : iPr_def_11(multiply(inverse(X0),X0),X1) = iPr_def_14(X0,X1),
inference(demodulation,[status(thm)],[c_641,c_1918]) ).
tcf(c_2483,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(inverse(multiply(iPr_def_13(X2,X3),inverse(multiply(inverse(X3),X3))))))) = iPr_def_11(X1,X2),
inference(superposition,[status(thm)],[c_1649,c_600]) ).
tcf(c_2497,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(iPr_def_13(X0,X1),inverse(multiply(iPr_def_13(X1,X2),inverse(multiply(inverse(X2),X2))))) = multiply(inverse(X0),X0),
inference(superposition,[status(thm)],[c_1649,c_1649]) ).
tcf(c_2510,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(iPr_def_13(X0,X1),inverse(multiply(inverse(X1),X1))) = multiply(iPr_def_13(X0,X2),inverse(multiply(inverse(X2),X2))),
inference(superposition,[status(thm)],[c_1649,c_1649]) ).
tcf(c_2514,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(iPr_def_11(X0,X1),inverse(multiply(iPr_def_13(inverse(multiply(inverse(X1),X1)),X2),inverse(multiply(inverse(X2),X2))))) = iPr_def_10(X0,X1),
inference(superposition,[status(thm)],[c_1649,c_836]) ).
tcf(c_2520,plain,
! [X0: $i,X1: $i] : iPr_def_13(inverse(multiply(iPr_def_13(X0,X1),inverse(multiply(inverse(X1),X1)))),X0) = inverse(inverse(multiply(iPr_def_13(X0,X1),inverse(multiply(inverse(X1),X1))))),
inference(superposition,[status(thm)],[c_1649,c_1650]) ).
tcf(c_2523,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_10(iPr_def_13(X0,X1),inverse(multiply(iPr_def_13(X1,X2),inverse(multiply(inverse(X2),X2))))) = iPr_def_11(multiply(inverse(X0),X0),X1),
inference(superposition,[status(thm)],[c_1649,c_1653]) ).
tcf(c_2598,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : multiply(inverse(X0),multiply(iPr_def_10(X0,X1),inverse(inverse(multiply(iPr_def_13(X2,X3),inverse(multiply(inverse(X3),X3))))))) = iPr_def_14(X1,X2),
inference(superposition,[status(thm)],[c_1649,c_1918]) ).
tcf(c_2672,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_10(multiply(X0,inverse(iPr_def_11(inverse(multiply(inverse(X1),X1)),X1))),X2) = X0,
inference(superposition,[status(thm)],[c_347,c_1917]) ).
tcf(c_2684,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : multiply(X0,inverse(multiply(inverse(iPr_def_10(X1,multiply(inverse(X2),X2))),iPr_def_10(X1,multiply(inverse(X2),X2))))) = multiply(X0,inverse(iPr_def_11(inverse(multiply(inverse(X3),X3)),X3))),
inference(superposition,[status(thm)],[c_1917,c_66]) ).
tcf(c_2708,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(iPr_def_13(multiply(X0,inverse(inverse(multiply(inverse(X1),X1)))),X2),inverse(multiply(inverse(X2),X2))) = iPr_def_11(inverse(multiply(inverse(X1),X1)),X1),
inference(superposition,[status(thm)],[c_1700,c_66]) ).
tcf(c_2713,plain,
! [X0: $i,X1: $i] : multiply(iPr_def_13(X0,X1),inverse(multiply(inverse(X1),X1))) = iPr_def_16(X0),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_16])],[c_2510]) ).
tcf(c_2715,plain,
! [X0: $i,X1: $i] : multiply(iPr_def_13(X0,X1),inverse(iPr_def_16(X1))) = multiply(inverse(X0),X0),
inference(demodulation,[status(thm)],[c_2497,c_2713]) ).
tcf(c_2717,plain,
! [X0: $i,X1: $i] : iPr_def_10(iPr_def_13(X0,X1),inverse(iPr_def_16(X1))) = iPr_def_11(multiply(inverse(X0),X0),X1),
inference(demodulation,[status(thm)],[c_2523,c_2713]) ).
tcf(c_2718,plain,
! [X0: $i,X1: $i] : iPr_def_10(iPr_def_13(X0,X1),inverse(iPr_def_16(X1))) = iPr_def_14(X0,X1),
inference(demodulation,[status(thm)],[c_2717,c_2011]) ).
tcf(c_2719,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(inverse(X0),multiply(iPr_def_10(X0,X1),inverse(inverse(iPr_def_16(X2))))) = iPr_def_14(X1,X2),
inference(demodulation,[status(thm)],[c_2598,c_2713]) ).
tcf(c_2722,plain,
! [X0: $i,X1: $i] : multiply(iPr_def_11(X0,X1),inverse(iPr_def_16(inverse(multiply(inverse(X1),X1))))) = iPr_def_10(X0,X1),
inference(demodulation,[status(thm)],[c_2514,c_2713]) ).
tcf(c_2723,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(inverse(iPr_def_16(X2))))) = iPr_def_11(X1,X2),
inference(demodulation,[status(thm)],[c_2483,c_2713]) ).
tcf(c_2725,plain,
! [X0: $i,X1: $i] : iPr_def_16(multiply(X0,inverse(inverse(multiply(inverse(X1),X1))))) = iPr_def_11(inverse(multiply(inverse(X1),X1)),X1),
inference(demodulation,[status(thm)],[c_2708,c_2713]) ).
tcf(c_2727,plain,
! [X0: $i] : iPr_def_13(inverse(iPr_def_16(X0)),X0) = inverse(inverse(iPr_def_16(X0))),
inference(demodulation,[status(thm)],[c_2520,c_2713]) ).
tcf(c_2746,plain,
! [X0: $i,X1: $i] : multiply(X0,inverse(iPr_def_11(inverse(multiply(inverse(X1),X1)),X1))) = iPr_def_17(X0),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_17])],[c_2684]) ).
tcf(c_2829,plain,
! [X0: $i] : multiply(inverse(X0),X0) = iPr_def_16(X0),
inference(demodulation,[status(thm)],[c_1649,c_2713]) ).
tcf(c_2835,plain,
! [X0: $i,X1: $i] : iPr_def_10(iPr_def_10(X0,X1),inverse(iPr_def_16(X1))) = iPr_def_11(X0,X1),
inference(demodulation,[status(thm)],[c_835,c_2829]) ).
tcf(c_2837,plain,
! [X0: $i,X1: $i] : iPr_def_10(multiply(X0,inverse(iPr_def_16(X1))),X1) = X0,
inference(demodulation,[status(thm)],[c_139,c_2829]) ).
tcf(c_2838,plain,
! [X0: $i,X1: $i] : multiply(iPr_def_10(X0,X1),inverse(iPr_def_16(X1))) = X0,
inference(demodulation,[status(thm)],[c_66,c_2829]) ).
tcf(c_5065,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(multiply(X2,inverse(X3))))) = iPr_def_12(multiply(X1,inverse(iPr_def_16(X3))),X3,X2),
inference(superposition,[status(thm)],[c_2837,c_602]) ).
tcf(c_5071,plain,
! [X0: $i,X1: $i] : multiply(iPr_def_12(inverse(X0),X0,iPr_def_10(X1,X0)),inverse(iPr_def_16(multiply(iPr_def_10(X1,X0),inverse(X0))))) = inverse(X1),
inference(superposition,[status(thm)],[c_1660,c_2838]) ).
tcf(c_5080,plain,
! [X0: $i,X1: $i] : multiply(iPr_def_14(X0,X1),inverse(iPr_def_16(inverse(iPr_def_16(X1))))) = iPr_def_13(X0,X1),
inference(superposition,[status(thm)],[c_2718,c_2838]) ).
tcf(c_5127,plain,
! [X0: $i,X1: $i] : multiply(iPr_def_13(X0,X1),inverse(iPr_def_16(X1))) = iPr_def_16(X0),
inference(superposition,[status(thm)],[c_2715,c_2829]) ).
tcf(c_5138,plain,
! [X0: $i,X1: $i] : multiply(X0,inverse(iPr_def_11(inverse(iPr_def_16(X1)),X1))) = iPr_def_17(X0),
inference(superposition,[status(thm)],[c_2829,c_2746]) ).
tcf(c_5155,plain,
! [X0: $i,X1: $i] : iPr_def_10(iPr_def_17(X0),X1) = X0,
inference(superposition,[status(thm)],[c_2746,c_2672]) ).
tcf(c_5160,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_11(multiply(X0,inverse(iPr_def_11(inverse(multiply(inverse(X1),X1)),X1))),X2) = iPr_def_10(X0,inverse(iPr_def_16(X2))),
inference(superposition,[status(thm)],[c_2672,c_2835]) ).
tcf(c_5161,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(X0,inverse(iPr_def_11(inverse(multiply(inverse(X1),X1)),X1))) = multiply(X0,inverse(iPr_def_16(X2))),
inference(superposition,[status(thm)],[c_2672,c_2838]) ).
tcf(c_5164,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(inverse(multiply(X0,inverse(iPr_def_11(inverse(multiply(inverse(X1),X1)),X1)))),multiply(X0,inverse(X2))) = iPr_def_10(inverse(X2),X2),
inference(superposition,[status(thm)],[c_2672,c_80]) ).
tcf(c_5177,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : multiply(inverse(multiply(X0,inverse(iPr_def_11(inverse(multiply(inverse(X1),X1)),X1)))),multiply(X0,inverse(inverse(iPr_def_16(X2))))) = iPr_def_14(X3,X2),
inference(superposition,[status(thm)],[c_2672,c_2719]) ).
tcf(c_5181,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(inverse(multiply(X0,inverse(iPr_def_16(X1)))),multiply(X0,inverse(inverse(iPr_def_16(X2))))) = iPr_def_14(X1,X2),
inference(superposition,[status(thm)],[c_2837,c_2719]) ).
tcf(c_5192,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(iPr_def_11(X0,X1),inverse(iPr_def_16(inverse(multiply(iPr_def_13(X1,X2),inverse(iPr_def_16(X2))))))) = iPr_def_10(X0,X1),
inference(superposition,[status(thm)],[c_2715,c_2722]) ).
tcf(c_5263,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_11(inverse(multiply(inverse(X0),X0)),X0) = iPr_def_16(iPr_def_12(X1,X2,inverse(inverse(X2)))),
inference(superposition,[status(thm)],[c_1707,c_2725]) ).
tcf(c_5315,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_16(iPr_def_12(X0,X1,inverse(inverse(X1)))) = iPr_def_11(inverse(iPr_def_16(X2)),X2),
inference(demodulation,[status(thm)],[c_5263,c_2829]) ).
tcf(c_5320,plain,
! [X0: $i,X1: $i] : multiply(X0,inverse(iPr_def_16(X1))) = iPr_def_17(X0),
inference(demodulation,[status(thm)],[c_5161,c_2746]) ).
tcf(c_5323,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(inverse(iPr_def_17(X0)),multiply(X0,inverse(inverse(iPr_def_16(X1))))) = iPr_def_14(X2,X1),
inference(demodulation,[status(thm)],[c_5181,c_5320]) ).
tcf(c_5329,plain,
! [X0: $i,X1: $i] : iPr_def_17(iPr_def_11(X0,X1)) = iPr_def_10(X0,X1),
inference(demodulation,[status(thm)],[c_5192,c_5320]) ).
tcf(c_5330,plain,
! [X0: $i,X1: $i] : iPr_def_10(X0,inverse(iPr_def_16(X1))) = iPr_def_11(iPr_def_17(X0),X1),
inference(demodulation,[status(thm)],[c_5160,c_2746]) ).
tcf(c_5334,plain,
! [X0: $i,X1: $i] : iPr_def_17(iPr_def_12(inverse(X0),X0,iPr_def_10(X1,X0))) = inverse(X1),
inference(demodulation,[status(thm)],[c_5071,c_5320]) ).
tcf(c_5351,plain,
! [X0: $i,X1: $i] : multiply(inverse(iPr_def_17(X0)),multiply(X0,inverse(X1))) = iPr_def_10(inverse(X1),X1),
inference(demodulation,[status(thm)],[c_5164,c_2746]) ).
tcf(c_5357,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_11(iPr_def_11(inverse(iPr_def_16(X0)),X0),X1) = iPr_def_14(X2,X1),
inference(demodulation,[status(thm)],[c_5177,c_2723,c_2829]) ).
tcf(c_5362,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(multiply(X2,inverse(X3))))) = iPr_def_12(iPr_def_17(X1),X3,X2),
inference(demodulation,[status(thm)],[c_5065,c_5320]) ).
tcf(c_5450,plain,
! [X0: $i,X1: $i] : iPr_def_17(iPr_def_10(X0,X1)) = X0,
inference(demodulation,[status(thm)],[c_2838,c_5320]) ).
tcf(c_5583,plain,
! [X0: $i,X1: $i,X2: $i] : inverse(multiply(X0,inverse(multiply(X1,X2)))) = iPr_def_17(iPr_def_12(X1,X2,X0)),
inference(superposition,[status(thm)],[c_839,c_5450]) ).
tcf(c_5588,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_10(X0,X1) = iPr_def_10(X0,X2),
inference(superposition,[status(thm)],[c_5450,c_5155]) ).
tcf(c_5603,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),iPr_def_17(iPr_def_10(X0,iPr_def_16(X1)))) = iPr_def_10(inverse(iPr_def_16(X1)),iPr_def_16(X1)),
inference(superposition,[status(thm)],[c_5320,c_80]) ).
tcf(c_5609,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_10(iPr_def_10(X0,X1),X2) = iPr_def_11(X0,X1),
inference(superposition,[status(thm)],[c_5329,c_5155]) ).
tcf(c_5619,plain,
! [X0: $i,X1: $i] : iPr_def_17(iPr_def_13(X0,X1)) = iPr_def_16(X0),
inference(superposition,[status(thm)],[c_5127,c_5320]) ).
tcf(c_5635,plain,
! [X0: $i,X1: $i] : iPr_def_11(iPr_def_17(iPr_def_17(X0)),X1) = X0,
inference(superposition,[status(thm)],[c_5330,c_5155]) ).
tcf(c_5664,plain,
! [X0: $i,X1: $i] : iPr_def_17(iPr_def_12(inverse(X0),X0,X1)) = inverse(iPr_def_17(X1)),
inference(superposition,[status(thm)],[c_5155,c_5334]) ).
tcf(c_5701,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(iPr_def_11(iPr_def_11(inverse(iPr_def_16(X0)),X0),X1),inverse(iPr_def_16(inverse(iPr_def_16(X1))))) = iPr_def_13(X2,X1),
inference(superposition,[status(thm)],[c_5357,c_5080]) ).
tcf(c_5709,plain,
! [X0: $i,X1: $i] : iPr_def_17(iPr_def_14(X0,X1)) = iPr_def_13(X0,X1),
inference(superposition,[status(thm)],[c_5080,c_5320]) ).
tcf(c_5830,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(inverse(iPr_def_17(X0)),multiply(X0,inverse(X1))) = multiply(inverse(iPr_def_17(X2)),multiply(X2,inverse(X1))),
inference(superposition,[status(thm)],[c_5351,c_5351]) ).
tcf(c_5867,plain,
! [X0: $i,X1: $i] : iPr_def_10(inverse(iPr_def_16(X0)),iPr_def_16(X0)) = iPr_def_16(X1),
inference(demodulation,[status(thm)],[c_5603,c_2829,c_5450]) ).
tcf(c_5876,plain,
! [X0: $i,X1: $i] : multiply(inverse(iPr_def_17(X0)),multiply(X0,inverse(X1))) = iPr_def_27(X1),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_27])],[c_5830]) ).
tcf(c_5878,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_10(iPr_def_11(inverse(iPr_def_16(X0)),X0),X1) = iPr_def_13(X2,X1),
inference(demodulation,[status(thm)],[c_5701,c_5320,c_5329]) ).
tcf(c_5975,plain,
! [X0: $i] : iPr_def_10(inverse(X0),X0) = iPr_def_27(X0),
inference(demodulation,[status(thm)],[c_5351,c_5876]) ).
tcf(c_5976,plain,
! [X0: $i,X1: $i] : iPr_def_27(inverse(iPr_def_16(X0))) = iPr_def_14(X1,X0),
inference(demodulation,[status(thm)],[c_5323,c_5876]) ).
tcf(c_6159,plain,
! [X0: $i] : iPr_def_17(iPr_def_27(X0)) = inverse(X0),
inference(superposition,[status(thm)],[c_5975,c_5450]) ).
tcf(c_6161,plain,
! [X0: $i,X1: $i] : iPr_def_10(inverse(X0),X1) = iPr_def_27(X0),
inference(superposition,[status(thm)],[c_5975,c_5588]) ).
tcf(c_6167,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_17(iPr_def_11(iPr_def_11(inverse(iPr_def_16(X0)),X0),X1)) = iPr_def_13(X2,X1),
inference(superposition,[status(thm)],[c_5357,c_5709]) ).
tcf(c_6183,plain,
! [X0: $i,X1: $i] : iPr_def_11(iPr_def_11(inverse(iPr_def_16(X0)),X0),X1) = iPr_def_27(inverse(iPr_def_16(X1))),
inference(superposition,[status(thm)],[c_5976,c_5357]) ).
tcf(c_6187,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : iPr_def_10(iPr_def_10(X0,X1),X2) = iPr_def_11(X0,X3),
inference(superposition,[status(thm)],[c_5588,c_5609]) ).
tcf(c_6189,plain,
! [X0: $i,X1: $i] : iPr_def_10(iPr_def_27(X0),X1) = iPr_def_11(inverse(X0),X0),
inference(superposition,[status(thm)],[c_5975,c_5609]) ).
tcf(c_6194,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_11(iPr_def_17(X0),X1) = iPr_def_10(X0,X2),
inference(superposition,[status(thm)],[c_5155,c_5609]) ).
tcf(c_6204,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_11(iPr_def_17(iPr_def_10(X0,X1)),X2) = iPr_def_11(X0,X1),
inference(superposition,[status(thm)],[c_5609,c_5330]) ).
tcf(c_6226,plain,
! [X0: $i,X1: $i] : inverse(iPr_def_16(X0)) = iPr_def_17(iPr_def_16(X1)),
inference(superposition,[status(thm)],[c_5867,c_5450]) ).
tcf(c_6229,plain,
! [X0: $i,X1: $i] : iPr_def_27(iPr_def_16(X0)) = iPr_def_16(X1),
inference(superposition,[status(thm)],[c_5867,c_5975]) ).
tcf(c_6230,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(inverse(multiply(iPr_def_10(X0,inverse(iPr_def_16(X1))),inverse(iPr_def_16(X2)))),X0) = iPr_def_12(inverse(iPr_def_16(X1)),iPr_def_16(X1),inverse(inverse(iPr_def_16(X1)))),
inference(superposition,[status(thm)],[c_5867,c_1707]) ).
tcf(c_6231,plain,
! [X0: $i,X1: $i] : iPr_def_16(X0) = iPr_def_16(X1),
inference(superposition,[status(thm)],[c_5867,c_5867]) ).
tcf(c_6237,plain,
! [X0: $i,X1: $i] : iPr_def_13(inverse(iPr_def_10(inverse(iPr_def_16(X0)),iPr_def_16(X0))),X1) = inverse(inverse(iPr_def_10(inverse(iPr_def_16(X0)),iPr_def_16(X0)))),
inference(superposition,[status(thm)],[c_5867,c_2727]) ).
tcf(c_6245,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_10(X0,inverse(iPr_def_10(inverse(iPr_def_16(X1)),iPr_def_16(X1)))) = iPr_def_11(iPr_def_17(X0),X2),
inference(superposition,[status(thm)],[c_5867,c_5330]) ).
tcf(c_6249,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(inverse(iPr_def_10(inverse(iPr_def_16(X2)),iPr_def_16(X2)))))) = iPr_def_11(X1,X3),
inference(superposition,[status(thm)],[c_5867,c_2723]) ).
tcf(c_6279,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_11(iPr_def_17(inverse(iPr_def_17(X0))),X1) = iPr_def_12(inverse(X2),X2,X0),
inference(superposition,[status(thm)],[c_5664,c_5635]) ).
tcf(c_6280,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_12(inverse(X0),X0,X1) = iPr_def_10(inverse(iPr_def_17(X1)),X2),
inference(superposition,[status(thm)],[c_5664,c_5155]) ).
tcf(c_6329,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(inverse(X0),multiply(iPr_def_10(X0,X1),inverse(X2))) = iPr_def_27(X2),
inference(superposition,[status(thm)],[c_5450,c_5876]) ).
tcf(c_6372,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_17(iPr_def_10(iPr_def_11(inverse(iPr_def_16(X0)),X0),X1)) = iPr_def_16(X2),
inference(superposition,[status(thm)],[c_5878,c_5619]) ).
tcf(c_6384,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_11(X0,X1) = iPr_def_11(X0,X2),
inference(demodulation,[status(thm)],[c_6204,c_5450]) ).
tcf(c_6387,plain,
! [X0: $i,X1: $i] : iPr_def_11(inverse(iPr_def_16(X0)),X0) = iPr_def_16(X1),
inference(demodulation,[status(thm)],[c_6372,c_5450]) ).
tcf(c_6388,plain,
! [X0: $i,X1: $i] : iPr_def_12(inverse(X0),X0,X1) = iPr_def_27(iPr_def_17(X1)),
inference(demodulation,[status(thm)],[c_6280,c_6161]) ).
tcf(c_6397,plain,
! [X0: $i,X1: $i] : iPr_def_11(iPr_def_17(inverse(iPr_def_17(X0))),X1) = iPr_def_27(iPr_def_17(X0)),
inference(demodulation,[status(thm)],[c_6279,c_6388]) ).
tcf(c_6407,plain,
! [X0: $i,X1: $i] : inverse(inverse(iPr_def_16(X0))) = iPr_def_13(X1,X0),
inference(demodulation,[status(thm)],[c_6167,c_6159,c_6183]) ).
tcf(c_6427,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_10(X0,inverse(iPr_def_27(iPr_def_16(X1)))) = iPr_def_11(iPr_def_17(X0),X2),
inference(demodulation,[status(thm)],[c_6245,c_6161]) ).
tcf(c_6460,plain,
! [X0: $i,X1: $i] : inverse(inverse(iPr_def_27(iPr_def_16(X0)))) = inverse(inverse(iPr_def_16(X1))),
inference(demodulation,[status(thm)],[c_6237,c_6161,c_6407]) ).
tcf(c_6461,plain,
! [X0: $i] : inverse(inverse(iPr_def_16(X0))) = iPr_def_28,
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_28])],[c_6460]) ).
tcf(c_6462,plain,
! [X0: $i] : inverse(inverse(iPr_def_27(iPr_def_16(X0)))) = iPr_def_28,
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_6460]) ).
tcf(c_6475,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,iPr_def_28)) = iPr_def_11(X1,X2),
inference(demodulation,[status(thm)],[c_6249,c_6161,c_6462]) ).
tcf(c_6486,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(inverse(multiply(iPr_def_10(X0,inverse(iPr_def_16(X1))),inverse(iPr_def_16(X2)))),X0) = iPr_def_27(iPr_def_17(iPr_def_28)),
inference(demodulation,[status(thm)],[c_6230,c_6388,c_6461]) ).
tcf(c_6487,plain,
! [X0: $i] : iPr_def_27(iPr_def_17(iPr_def_28)) = iPr_def_16(X0),
inference(demodulation,[status(thm)],[c_6486,c_2829,c_5320,c_5450]) ).
tcf(c_6495,plain,
! [X0: $i] : iPr_def_11(inverse(iPr_def_16(X0)),X0) = iPr_def_27(iPr_def_17(iPr_def_28)),
inference(demodulation,[status(thm)],[c_5315,c_6487]) ).
tcf(c_6498,plain,
! [X0: $i] : multiply(X0,inverse(iPr_def_27(iPr_def_17(iPr_def_28)))) = iPr_def_17(X0),
inference(demodulation,[status(thm)],[c_5138,c_6495]) ).
tcf(c_6942,plain,
! [X0: $i,X1: $i] : multiply(inverse(inverse(X0)),multiply(iPr_def_27(X0),inverse(X1))) = iPr_def_27(X1),
inference(superposition,[status(thm)],[c_6159,c_5876]) ).
tcf(c_6965,plain,
! [X0: $i] : multiply(iPr_def_28,inverse(iPr_def_16(X0))) = iPr_def_16(inverse(iPr_def_16(X0))),
inference(superposition,[status(thm)],[c_6461,c_2829]) ).
tcf(c_6976,plain,
inverse(inverse(iPr_def_27(iPr_def_17(iPr_def_28)))) = iPr_def_28,
inference(superposition,[status(thm)],[c_6487,c_6461]) ).
tcf(c_6977,plain,
! [X0: $i] : iPr_def_27(iPr_def_27(iPr_def_17(iPr_def_28))) = iPr_def_16(X0),
inference(superposition,[status(thm)],[c_6487,c_6229]) ).
tcf(c_7009,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_10(X0,iPr_def_17(iPr_def_16(X1))) = iPr_def_11(iPr_def_17(X0),X2),
inference(superposition,[status(thm)],[c_6226,c_5330]) ).
tcf(c_7011,plain,
! [X0: $i,X1: $i] : multiply(X0,iPr_def_17(iPr_def_16(X1))) = iPr_def_17(X0),
inference(superposition,[status(thm)],[c_6226,c_5320]) ).
tcf(c_7016,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_10(inverse(iPr_def_16(X0)),X1) = iPr_def_16(X2),
inference(superposition,[status(thm)],[c_6226,c_5155]) ).
tcf(c_7017,plain,
! [X0: $i,X1: $i] : inverse(iPr_def_16(X0)) = inverse(iPr_def_16(X1)),
inference(superposition,[status(thm)],[c_6226,c_6226]) ).
tcf(c_7082,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_17(iPr_def_11(X0,X1)) = iPr_def_10(X0,X2),
inference(superposition,[status(thm)],[c_6384,c_5329]) ).
tcf(c_7221,plain,
! [X0: $i] : inverse(iPr_def_16(X0)) = iPr_def_30,
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_30])],[c_7017]) ).
tcf(c_7236,plain,
! [X0: $i,X1: $i] : iPr_def_10(iPr_def_30,X0) = iPr_def_16(X1),
inference(demodulation,[status(thm)],[c_7016,c_7221]) ).
tcf(c_7257,plain,
multiply(iPr_def_28,iPr_def_30) = iPr_def_16(iPr_def_30),
inference(demodulation,[status(thm)],[c_6965,c_7221]) ).
tcf(c_7279,plain,
! [X0: $i] : multiply(X0,iPr_def_30) = iPr_def_17(X0),
inference(demodulation,[status(thm)],[c_5320,c_7221]) ).
tcf(c_7280,plain,
! [X0: $i] : iPr_def_17(iPr_def_16(X0)) = iPr_def_30,
inference(demodulation,[status(thm)],[c_6226,c_7221]) ).
tcf(c_7281,plain,
inverse(iPr_def_30) = iPr_def_28,
inference(demodulation,[status(thm)],[c_6461,c_7221]) ).
tcf(c_7386,plain,
multiply(iPr_def_28,inverse(iPr_def_27(iPr_def_17(iPr_def_28)))) = iPr_def_16(inverse(iPr_def_27(iPr_def_17(iPr_def_28)))),
inference(superposition,[status(thm)],[c_6976,c_2829]) ).
tcf(c_7420,plain,
! [X0: $i,X1: $i] : iPr_def_27(iPr_def_10(iPr_def_30,X0)) = iPr_def_16(X1),
inference(superposition,[status(thm)],[c_7236,c_6229]) ).
tcf(c_7431,plain,
iPr_def_16(iPr_def_30) = iPr_def_17(iPr_def_28),
inference(demodulation,[status(thm)],[c_7257,c_7279]) ).
tcf(c_7439,plain,
iPr_def_27(iPr_def_27(iPr_def_17(iPr_def_28))) = iPr_def_17(iPr_def_28),
inference(demodulation,[status(thm)],[c_7386,c_6498,c_6977]) ).
tcf(c_8263,plain,
! [X0: $i] : iPr_def_10(iPr_def_16(iPr_def_30),X0) = iPr_def_28,
inference(superposition,[status(thm)],[c_7431,c_5155]) ).
tcf(c_8703,plain,
! [X0: $i,X1: $i] : iPr_def_10(iPr_def_16(X0),X1) = iPr_def_28,
inference(superposition,[status(thm)],[c_6231,c_8263]) ).
tcf(c_8760,plain,
! [X0: $i] : iPr_def_16(X0) = iPr_def_17(iPr_def_28),
inference(superposition,[status(thm)],[c_7439,c_6977]) ).
tcf(c_8796,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_10(iPr_def_16(X0),X1) = iPr_def_11(iPr_def_30,X2),
inference(superposition,[status(thm)],[c_7280,c_6194]) ).
tcf(c_8797,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_10(iPr_def_27(X0),X1) = iPr_def_11(inverse(X0),X2),
inference(superposition,[status(thm)],[c_6159,c_6194]) ).
tcf(c_8914,plain,
! [X0: $i,X1: $i] : iPr_def_11(iPr_def_30,X0) = iPr_def_16(X1),
inference(superposition,[status(thm)],[c_7221,c_6387]) ).
tcf(c_8964,plain,
! [X0: $i,X1: $i] : iPr_def_11(inverse(iPr_def_16(X0)),X0) = iPr_def_10(iPr_def_30,X1),
inference(superposition,[status(thm)],[c_6387,c_7236]) ).
tcf(c_9001,plain,
! [X0: $i] : iPr_def_11(iPr_def_30,X0) = iPr_def_28,
inference(demodulation,[status(thm)],[c_8796,c_8703]) ).
tcf(c_9011,plain,
! [X0: $i,X1: $i] : iPr_def_10(iPr_def_30,X0) = iPr_def_11(iPr_def_30,X1),
inference(demodulation,[status(thm)],[c_8964,c_7221]) ).
tcf(c_9266,plain,
! [X0: $i,X1: $i] : iPr_def_10(iPr_def_10(iPr_def_30,X0),X1) = iPr_def_28,
inference(superposition,[status(thm)],[c_7236,c_8703]) ).
tcf(c_9291,plain,
! [X0: $i] : iPr_def_16(X0) = iPr_def_28,
inference(superposition,[status(thm)],[c_8914,c_9001]) ).
tcf(c_9293,plain,
! [X0: $i] : iPr_def_11(iPr_def_30,X0) = iPr_def_17(iPr_def_28),
inference(superposition,[status(thm)],[c_8914,c_8760]) ).
tcf(c_9346,plain,
! [X0: $i] : iPr_def_17(iPr_def_11(iPr_def_30,X0)) = iPr_def_30,
inference(superposition,[status(thm)],[c_9011,c_5450]) ).
tcf(c_9351,plain,
! [X0: $i,X1: $i] : iPr_def_27(iPr_def_11(iPr_def_30,X0)) = iPr_def_16(X1),
inference(superposition,[status(thm)],[c_9011,c_7420]) ).
tcf(c_9359,plain,
! [X0: $i] : iPr_def_10(iPr_def_30,X0) = iPr_def_28,
inference(superposition,[status(thm)],[c_9011,c_9001]) ).
tcf(c_9501,plain,
iPr_def_17(iPr_def_28) = iPr_def_30,
inference(demodulation,[status(thm)],[c_9346,c_9001]) ).
tcf(c_9502,plain,
iPr_def_17(iPr_def_28) = iPr_def_28,
inference(demodulation,[status(thm)],[c_9293,c_9001]) ).
tcf(c_9508,plain,
! [X0: $i] : iPr_def_27(iPr_def_11(iPr_def_30,X0)) = iPr_def_28,
inference(demodulation,[status(thm)],[c_9351,c_9291]) ).
tcf(c_9509,plain,
iPr_def_27(iPr_def_28) = iPr_def_28,
inference(demodulation,[status(thm)],[c_9508,c_9001]) ).
tcf(c_9525,plain,
! [X0: $i] : iPr_def_10(iPr_def_28,X0) = iPr_def_28,
inference(demodulation,[status(thm)],[c_9266,c_9359]) ).
tcf(c_9739,plain,
! [X0: $i] : multiply(inverse(X0),X0) = iPr_def_28,
inference(demodulation,[status(thm)],[c_2829,c_9291]) ).
tcf(c_9813,plain,
! [X0: $i] : multiply(inverse(iPr_def_30),multiply(iPr_def_28,inverse(X0))) = iPr_def_27(X0),
inference(superposition,[status(thm)],[c_9501,c_5876]) ).
tcf(c_9820,plain,
iPr_def_28 = iPr_def_30,
inference(demodulation,[status(thm)],[c_9501,c_9502]) ).
tcf(c_9829,plain,
! [X0: $i] : multiply(iPr_def_28,multiply(iPr_def_28,inverse(X0))) = iPr_def_27(X0),
inference(light_normalisation,[status(thm)],[c_9813,c_7281]) ).
tcf(c_9833,plain,
! [X0: $i] : multiply(X0,iPr_def_28) = iPr_def_17(X0),
inference(demodulation,[status(thm)],[c_7279,c_9820]) ).
tcf(c_9834,plain,
inverse(iPr_def_28) = iPr_def_28,
inference(demodulation,[status(thm)],[c_7281,c_9820]) ).
tcf(c_9955,plain,
! [X0: $i] : multiply(inverse(iPr_def_17(inverse(inverse(X0)))),iPr_def_28) = iPr_def_27(X0),
inference(superposition,[status(thm)],[c_9739,c_5876]) ).
tcf(c_9975,plain,
! [X0: $i] : iPr_def_17(inverse(iPr_def_17(inverse(inverse(X0))))) = iPr_def_27(X0),
inference(demodulation,[status(thm)],[c_9955,c_9833]) ).
tcf(c_10056,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : multiply(multiply(inverse(iPr_def_10(X0,X1)),multiply(multiply(inverse(multiply(X2,inverse(X0))),multiply(X2,inverse(inverse(multiply(inverse(X1),X1))))),inverse(inverse(multiply(inverse(X3),X3))))),inverse(iPr_def_28)) = iPr_def_10(multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(multiply(inverse(X1),X1))),X3),
inference(superposition,[status(thm)],[c_9739,c_109]) ).
tcf(c_10139,plain,
! [X0: $i] : multiply(X0,iPr_def_17(iPr_def_28)) = iPr_def_17(X0),
inference(superposition,[status(thm)],[c_9291,c_7011]) ).
tcf(c_10167,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_17(iPr_def_11(X0,X1)) = iPr_def_17(iPr_def_11(X0,X2)),
inference(superposition,[status(thm)],[c_7082,c_7082]) ).
tcf(c_10168,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_11(iPr_def_17(X0),X1) = iPr_def_17(iPr_def_11(X0,X2)),
inference(superposition,[status(thm)],[c_7082,c_6194]) ).
tcf(c_10431,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(multiply(inverse(iPr_def_10(X0,X1)),multiply(multiply(inverse(multiply(X2,inverse(X0))),multiply(X2,inverse(inverse(iPr_def_28)))),inverse(inverse(iPr_def_28)))),inverse(iPr_def_28)) = iPr_def_28,
inference(demodulation,[status(thm)],[c_10056,c_9525,c_9739]) ).
tcf(c_10432,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(multiply(inverse(iPr_def_10(X0,X1)),multiply(multiply(inverse(multiply(X2,inverse(X0))),multiply(X2,iPr_def_28)),iPr_def_28)),iPr_def_28) = iPr_def_28,
inference(light_normalisation,[status(thm)],[c_10431,c_9834]) ).
tcf(c_10433,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_17(multiply(inverse(iPr_def_10(X0,X1)),iPr_def_17(multiply(inverse(multiply(X2,inverse(X0))),iPr_def_17(X2))))) = iPr_def_28,
inference(demodulation,[status(thm)],[c_10432,c_9833]) ).
tcf(c_10743,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : iPr_def_10(iPr_def_11(iPr_def_17(X0),X1),X2) = iPr_def_11(X0,X3),
inference(superposition,[status(thm)],[c_6194,c_6187]) ).
tcf(c_10765,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : iPr_def_17(iPr_def_11(iPr_def_10(X0,X1),X2)) = iPr_def_11(X0,X3),
inference(superposition,[status(thm)],[c_6187,c_7082]) ).
tcf(c_10880,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] : multiply(multiply(inverse(multiply(multiply(inverse(multiply(X0,inverse(iPr_def_10(inverse(inverse(multiply(inverse(X1),X1))),inverse(multiply(inverse(X1),X1)))))),multiply(X0,inverse(multiply(multiply(inverse(iPr_def_10(X2,X3)),multiply(multiply(inverse(multiply(X4,inverse(X2))),multiply(X4,inverse(inverse(multiply(inverse(X3),X3))))),inverse(inverse(multiply(inverse(X1),X1))))),inverse(inverse(multiply(inverse(X1),X1))))))),inverse(multiply(X5,multiply(inverse(multiply(multiply(inverse(iPr_def_10(X2,X3)),multiply(multiply(inverse(multiply(X4,inverse(X2))),multiply(X4,inverse(inverse(multiply(inverse(X3),X3))))),inverse(inverse(multiply(inverse(X1),X1))))),inverse(inverse(multiply(inverse(X1),X1))))),multiply(multiply(inverse(iPr_def_10(X2,X3)),multiply(multiply(inverse(multiply(X4,inverse(X2))),multiply(X4,inverse(inverse(multiply(inverse(X3),X3))))),inverse(inverse(multiply(inverse(X1),X1))))),inverse(inverse(multiply(inverse(X1),X1))))))))),inverse(iPr_def_10(multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(multiply(inverse(X3),X3))),X1))),inverse(multiply(inverse(multiply(inverse(multiply(multiply(inverse(iPr_def_10(X2,X3)),multiply(multiply(inverse(multiply(X4,inverse(X2))),multiply(X4,inverse(inverse(multiply(inverse(X3),X3))))),inverse(inverse(multiply(inverse(X1),X1))))),inverse(inverse(multiply(inverse(X1),X1))))),multiply(multiply(inverse(iPr_def_10(X2,X3)),multiply(multiply(inverse(multiply(X4,inverse(X2))),multiply(X4,inverse(inverse(multiply(inverse(X3),X3))))),inverse(inverse(multiply(inverse(X1),X1))))),inverse(inverse(multiply(inverse(X1),X1)))))),multiply(inverse(multiply(multiply(inverse(iPr_def_10(X2,X3)),multiply(multiply(inverse(multiply(X4,inverse(X2))),multiply(X4,inverse(inverse(multiply(inverse(X3),X3))))),inverse(inverse(multiply(inverse(X1),X1))))),inverse(inverse(multiply(inverse(X1),X1))))),multiply(multiply(inverse(iPr_def_10(X2,X3)),multiply(multiply(inverse(multiply(X4,inverse(X2))),multiply(X4,inverse(inverse(multiply(inverse(X3),X3))))),inverse(inverse(multiply(inverse(X1),X1))))),inverse(inverse(multiply(inverse(X1),X1)))))))) = X5,
inference(superposition,[status(thm)],[c_109,c_115]) ).
tcf(c_11194,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : multiply(multiply(iPr_def_17(iPr_def_12(X0,iPr_def_28,iPr_def_27(iPr_def_17(multiply(inverse(iPr_def_10(X1,X2)),multiply(multiply(inverse(multiply(X3,inverse(X1))),multiply(X3,inverse(inverse(iPr_def_28)))),inverse(inverse(iPr_def_28)))))))),inverse(iPr_def_28)),inverse(iPr_def_28)) = X0,
inference(demodulation,[status(thm)],[c_10880,c_5362,c_5450,c_5583,c_6388,c_9525,c_9739]) ).
tcf(c_11195,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : multiply(multiply(iPr_def_17(iPr_def_12(X0,iPr_def_28,iPr_def_27(iPr_def_17(multiply(inverse(iPr_def_10(X1,X2)),multiply(multiply(inverse(multiply(X3,inverse(X1))),multiply(X3,iPr_def_28)),iPr_def_28)))))),iPr_def_28),iPr_def_28) = X0,
inference(light_normalisation,[status(thm)],[c_11194,c_9834]) ).
tcf(c_11196,plain,
! [X0: $i] : iPr_def_17(iPr_def_17(iPr_def_17(iPr_def_12(X0,iPr_def_28,iPr_def_27(iPr_def_28))))) = X0,
inference(demodulation,[status(thm)],[c_11195,c_9833,c_10433]) ).
tcf(c_11197,plain,
! [X0: $i] : iPr_def_17(iPr_def_17(iPr_def_17(iPr_def_12(X0,iPr_def_28,iPr_def_28)))) = X0,
inference(light_normalisation,[status(thm)],[c_11196,c_9509]) ).
tcf(c_11348,plain,
! [X0: $i,X1: $i] : inverse(iPr_def_17(inverse(inverse(X0)))) = iPr_def_10(iPr_def_27(X0),X1),
inference(superposition,[status(thm)],[c_9975,c_5155]) ).
tcf(c_11407,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_17(iPr_def_11(iPr_def_27(X0),X1)) = iPr_def_11(inverse(X0),X2),
inference(superposition,[status(thm)],[c_6159,c_10168]) ).
tcf(c_11459,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_10(iPr_def_17(iPr_def_17(iPr_def_12(X0,iPr_def_28,iPr_def_28))),X1) = iPr_def_11(X0,X2),
inference(superposition,[status(thm)],[c_11197,c_6194]) ).
tcf(c_11461,plain,
! [X0: $i,X1: $i] : iPr_def_17(iPr_def_17(iPr_def_12(X0,iPr_def_28,iPr_def_28))) = iPr_def_10(X0,X1),
inference(superposition,[status(thm)],[c_11197,c_5155]) ).
tcf(c_11499,plain,
! [X0: $i,X1: $i] : iPr_def_27(iPr_def_17(inverse(inverse(X0)))) = iPr_def_11(iPr_def_27(X0),X1),
inference(superposition,[status(thm)],[c_9975,c_6397]) ).
tcf(c_11643,plain,
! [X0: $i,X1: $i] : iPr_def_17(iPr_def_12(X0,iPr_def_28,iPr_def_28)) = iPr_def_11(X0,X1),
inference(demodulation,[status(thm)],[c_11459,c_5155]) ).
tcf(c_11778,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_10(iPr_def_11(X0,X1),X2) = iPr_def_12(X0,iPr_def_28,iPr_def_28),
inference(superposition,[status(thm)],[c_11643,c_5155]) ).
tcf(c_11786,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_10(iPr_def_10(X0,X1),X2) = iPr_def_17(iPr_def_12(X0,iPr_def_28,iPr_def_28)),
inference(superposition,[status(thm)],[c_11643,c_6187]) ).
tcf(c_11788,plain,
! [X0: $i,X1: $i] : iPr_def_17(iPr_def_17(iPr_def_12(X0,iPr_def_28,iPr_def_28))) = iPr_def_17(iPr_def_11(X0,X1)),
inference(superposition,[status(thm)],[c_11643,c_10167]) ).
tcf(c_11841,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] : iPr_def_10(iPr_def_11(X0,X1),iPr_def_17(iPr_def_16(X2))) = iPr_def_11(iPr_def_17(iPr_def_11(X0,X3)),X4),
inference(superposition,[status(thm)],[c_10167,c_7009]) ).
tcf(c_12141,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_11(iPr_def_17(iPr_def_11(X0,X1)),X2) = iPr_def_12(X0,iPr_def_28,iPr_def_28),
inference(demodulation,[status(thm)],[c_11841,c_11778]) ).
tcf(c_12476,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : iPr_def_11(iPr_def_17(iPr_def_11(iPr_def_17(X0),X1)),X2) = iPr_def_11(X0,X3),
inference(superposition,[status(thm)],[c_10743,c_7009]) ).
tcf(c_12478,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_10(iPr_def_11(iPr_def_17(X0),X1),X2) = iPr_def_17(iPr_def_12(X0,iPr_def_28,iPr_def_28)),
inference(superposition,[status(thm)],[c_10743,c_11643]) ).
tcf(c_12505,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_17(iPr_def_17(iPr_def_12(iPr_def_10(X0,X1),iPr_def_28,iPr_def_28))) = iPr_def_11(X0,X2),
inference(superposition,[status(thm)],[c_11643,c_10765]) ).
tcf(c_12548,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] : iPr_def_10(iPr_def_11(iPr_def_10(X0,X1),X2),X3) = iPr_def_11(iPr_def_11(X0,X4),X5),
inference(superposition,[status(thm)],[c_10765,c_6194]) ).
tcf(c_12698,plain,
! [X0: $i,X1: $i] : iPr_def_12(iPr_def_17(X0),iPr_def_28,iPr_def_28) = iPr_def_11(X0,X1),
inference(demodulation,[status(thm)],[c_12476,c_12141]) ).
tcf(c_12735,plain,
! [X0: $i] : iPr_def_12(iPr_def_17(X0),iPr_def_28,iPr_def_28) = iPr_def_17(iPr_def_12(X0,iPr_def_28,iPr_def_28)),
inference(demodulation,[status(thm)],[c_12478,c_11778]) ).
tcf(c_12788,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : iPr_def_12(iPr_def_10(X0,X1),iPr_def_28,iPr_def_28) = iPr_def_11(iPr_def_11(X0,X2),X3),
inference(demodulation,[status(thm)],[c_12548,c_11778]) ).
tcf(c_12998,plain,
! [X0: $i,X1: $i] : iPr_def_12(iPr_def_17(iPr_def_17(X0)),iPr_def_28,iPr_def_28) = iPr_def_10(X0,X1),
inference(superposition,[status(thm)],[c_12698,c_6194]) ).
tcf(c_13001,plain,
! [X0: $i,X1: $i] : iPr_def_12(iPr_def_17(inverse(X0)),iPr_def_28,iPr_def_28) = iPr_def_10(iPr_def_27(X0),X1),
inference(superposition,[status(thm)],[c_12698,c_8797]) ).
tcf(c_13297,plain,
! [X0: $i] : iPr_def_17(iPr_def_17(iPr_def_12(iPr_def_27(X0),iPr_def_28,iPr_def_28))) = inverse(iPr_def_17(inverse(inverse(X0)))),
inference(superposition,[status(thm)],[c_11461,c_11348]) ).
tcf(c_13535,plain,
! [X0: $i] : iPr_def_12(iPr_def_17(inverse(X0)),iPr_def_28,iPr_def_28) = inverse(iPr_def_17(inverse(inverse(X0)))),
inference(demodulation,[status(thm)],[c_13297,c_6159,c_12735]) ).
tcf(c_28421,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : iPr_def_10(iPr_def_17(iPr_def_12(X0,X1,X2)),X3) = iPr_def_27(multiply(X2,inverse(multiply(X0,X1)))),
inference(superposition,[status(thm)],[c_5583,c_6161]) ).
tcf(c_28570,plain,
! [X0: $i,X1: $i] : multiply(inverse(iPr_def_28),multiply(inverse(inverse(X0)),iPr_def_28)) = iPr_def_11(X0,X1),
inference(superposition,[status(thm)],[c_9739,c_6475]) ).
tcf(c_28591,plain,
! [X0: $i,X1: $i] : multiply(inverse(multiply(inverse(iPr_def_28),inverse(X0))),iPr_def_28) = iPr_def_11(X0,X1),
inference(superposition,[status(thm)],[c_9739,c_6475]) ).
tcf(c_28644,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,iPr_def_28)) = multiply(inverse(multiply(X2,inverse(X1))),multiply(X2,iPr_def_28)),
inference(superposition,[status(thm)],[c_6475,c_6475]) ).
tcf(c_28767,plain,
! [X0: $i,X1: $i] : iPr_def_17(inverse(multiply(inverse(iPr_def_28),inverse(X0)))) = iPr_def_11(X0,X1),
inference(demodulation,[status(thm)],[c_28591,c_9833]) ).
tcf(c_28768,plain,
! [X0: $i,X1: $i] : iPr_def_17(inverse(multiply(iPr_def_28,inverse(X0)))) = iPr_def_11(X0,X1),
inference(light_normalisation,[status(thm)],[c_28767,c_9834]) ).
tcf(c_28769,plain,
! [X0: $i,X1: $i] : multiply(inverse(iPr_def_28),iPr_def_17(inverse(inverse(X0)))) = iPr_def_11(X0,X1),
inference(demodulation,[status(thm)],[c_28570,c_9833]) ).
tcf(c_28770,plain,
! [X0: $i,X1: $i] : multiply(iPr_def_28,iPr_def_17(inverse(inverse(X0)))) = iPr_def_11(X0,X1),
inference(light_normalisation,[status(thm)],[c_28769,c_9834]) ).
tcf(c_28906,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_27(multiply(X0,inverse(multiply(X1,X2)))) = iPr_def_12(X1,X2,X0),
inference(demodulation,[status(thm)],[c_28421,c_5155]) ).
tcf(c_29149,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(inverse(multiply(X0,inverse(X1))),iPr_def_17(X0)) = multiply(inverse(multiply(X2,inverse(X1))),iPr_def_17(X2)),
inference(demodulation,[status(thm)],[c_28644,c_9833]) ).
tcf(c_29150,plain,
! [X0: $i,X1: $i] : multiply(inverse(multiply(X0,inverse(X1))),iPr_def_17(X0)) = iPr_def_35(X1),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_35])],[c_29149]) ).
tcf(c_30022,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_10(iPr_def_11(X0,X1),X2) = inverse(multiply(iPr_def_28,inverse(X0))),
inference(superposition,[status(thm)],[c_28768,c_5155]) ).
tcf(c_30044,plain,
! [X0: $i,X1: $i] : iPr_def_17(iPr_def_17(inverse(multiply(iPr_def_28,inverse(X0))))) = iPr_def_10(X0,X1),
inference(superposition,[status(thm)],[c_28768,c_7082]) ).
tcf(c_30324,plain,
! [X0: $i] : inverse(multiply(iPr_def_28,inverse(X0))) = iPr_def_12(X0,iPr_def_28,iPr_def_28),
inference(demodulation,[status(thm)],[c_30022,c_11778]) ).
tcf(c_30933,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(iPr_def_17(iPr_def_12(X0,X1,X2)),iPr_def_17(X2)) = iPr_def_35(multiply(X0,X1)),
inference(superposition,[status(thm)],[c_5583,c_29150]) ).
tcf(c_30957,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(inverse(multiply(iPr_def_10(X0,X1),inverse(X2))),X0) = iPr_def_35(X2),
inference(superposition,[status(thm)],[c_5450,c_29150]) ).
tcf(c_31012,plain,
! [X0: $i] : iPr_def_17(inverse(multiply(iPr_def_28,inverse(X0)))) = iPr_def_35(X0),
inference(superposition,[status(thm)],[c_29150,c_10139]) ).
tcf(c_31132,plain,
! [X0: $i] : iPr_def_17(iPr_def_17(inverse(multiply(iPr_def_28,inverse(iPr_def_27(X0)))))) = iPr_def_12(iPr_def_17(inverse(X0)),iPr_def_28,iPr_def_28),
inference(superposition,[status(thm)],[c_30044,c_13001]) ).
tcf(c_31156,plain,
! [X0: $i] : iPr_def_12(iPr_def_17(X0),iPr_def_28,iPr_def_28) = iPr_def_35(X0),
inference(demodulation,[status(thm)],[c_31012,c_12735,c_30324]) ).
tcf(c_31327,plain,
! [X0: $i] : iPr_def_17(iPr_def_17(inverse(multiply(iPr_def_28,inverse(iPr_def_27(X0)))))) = iPr_def_35(inverse(X0)),
inference(demodulation,[status(thm)],[c_31132,c_31156]) ).
tcf(c_31328,plain,
! [X0: $i] : inverse(iPr_def_17(inverse(inverse(X0)))) = iPr_def_35(inverse(X0)),
inference(demodulation,[status(thm)],[c_31327,c_6159,c_12735,c_13535,c_30324]) ).
tcf(c_31502,plain,
! [X0: $i,X1: $i] : iPr_def_10(X0,X1) = iPr_def_35(iPr_def_17(X0)),
inference(demodulation,[status(thm)],[c_12998,c_31156]) ).
tcf(c_31507,plain,
! [X0: $i,X1: $i] : iPr_def_11(iPr_def_17(X0),X1) = iPr_def_35(iPr_def_17(X0)),
inference(demodulation,[status(thm)],[c_6427,c_31502]) ).
tcf(c_31514,plain,
! [X0: $i,X1: $i] : iPr_def_17(iPr_def_11(X0,X1)) = iPr_def_35(iPr_def_17(X0)),
inference(demodulation,[status(thm)],[c_10168,c_31507]) ).
tcf(c_31535,plain,
! [X0: $i] : iPr_def_17(iPr_def_17(iPr_def_12(X0,iPr_def_28,iPr_def_28))) = iPr_def_35(iPr_def_17(X0)),
inference(demodulation,[status(thm)],[c_11788,c_31514]) ).
tcf(c_31545,plain,
! [X0: $i,X1: $i] : iPr_def_11(inverse(X0),X1) = iPr_def_35(iPr_def_17(iPr_def_27(X0))),
inference(demodulation,[status(thm)],[c_11407,c_31514]) ).
tcf(c_31551,plain,
! [X0: $i,X1: $i] : iPr_def_11(inverse(X0),X1) = iPr_def_35(inverse(X0)),
inference(demodulation,[status(thm)],[c_31545,c_6159]) ).
tcf(c_31558,plain,
! [X0: $i,X1: $i] : iPr_def_10(iPr_def_27(X0),X1) = iPr_def_35(inverse(X0)),
inference(demodulation,[status(thm)],[c_6189,c_31551]) ).
tcf(c_31586,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_35(iPr_def_17(iPr_def_10(X0,X1))) = iPr_def_11(X0,X2),
inference(demodulation,[status(thm)],[c_12505,c_31535]) ).
tcf(c_31587,plain,
! [X0: $i,X1: $i] : iPr_def_11(X0,X1) = iPr_def_35(X0),
inference(demodulation,[status(thm)],[c_31586,c_5450]) ).
tcf(c_31589,plain,
! [X0: $i] : multiply(iPr_def_28,iPr_def_17(inverse(inverse(X0)))) = iPr_def_35(X0),
inference(demodulation,[status(thm)],[c_28770,c_31587]) ).
tcf(c_31593,plain,
! [X0: $i,X1: $i] : iPr_def_10(X0,X1) = iPr_def_17(iPr_def_35(X0)),
inference(demodulation,[status(thm)],[c_7082,c_31587]) ).
tcf(c_31595,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_12(iPr_def_10(X0,X1),iPr_def_28,iPr_def_28) = iPr_def_11(iPr_def_35(X0),X2),
inference(demodulation,[status(thm)],[c_12788,c_31587]) ).
tcf(c_31597,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_10(iPr_def_10(X0,X1),X2) = iPr_def_35(X0),
inference(demodulation,[status(thm)],[c_6187,c_31587]) ).
tcf(c_31602,plain,
! [X0: $i] : iPr_def_27(iPr_def_17(inverse(inverse(X0)))) = iPr_def_35(iPr_def_27(X0)),
inference(demodulation,[status(thm)],[c_11499,c_31587]) ).
tcf(c_31616,plain,
! [X0: $i] : iPr_def_17(iPr_def_12(X0,iPr_def_28,iPr_def_28)) = iPr_def_35(X0),
inference(demodulation,[status(thm)],[c_11786,c_31597]) ).
tcf(c_31619,plain,
! [X0: $i,X1: $i] : iPr_def_12(iPr_def_10(X0,X1),iPr_def_28,iPr_def_28) = iPr_def_35(iPr_def_35(X0)),
inference(demodulation,[status(thm)],[c_31595,c_31587]) ).
tcf(c_31627,plain,
! [X0: $i] : iPr_def_17(iPr_def_35(inverse(X0))) = iPr_def_27(X0),
inference(demodulation,[status(thm)],[c_9975,c_31328]) ).
tcf(c_31906,plain,
! [X0: $i] : iPr_def_17(iPr_def_17(iPr_def_35(X0))) = X0,
inference(superposition,[status(thm)],[c_31593,c_5450]) ).
tcf(c_31958,plain,
! [X0: $i,X1: $i] : iPr_def_35(iPr_def_17(inverse(multiply(iPr_def_28,inverse(X0))))) = iPr_def_12(iPr_def_10(X0,X1),iPr_def_28,iPr_def_28),
inference(superposition,[status(thm)],[c_30044,c_31156]) ).
tcf(c_31964,plain,
! [X0: $i] : iPr_def_17(iPr_def_35(X0)) = iPr_def_35(iPr_def_17(X0)),
inference(superposition,[status(thm)],[c_31587,c_31514]) ).
tcf(c_31991,plain,
! [X0: $i] : iPr_def_17(iPr_def_35(iPr_def_27(X0))) = iPr_def_35(inverse(X0)),
inference(superposition,[status(thm)],[c_31558,c_31593]) ).
tcf(c_32221,plain,
! [X0: $i,X1: $i] : iPr_def_17(iPr_def_35(inverse(multiply(iPr_def_28,inverse(X0))))) = iPr_def_12(iPr_def_10(X0,X1),iPr_def_28,iPr_def_28),
inference(demodulation,[status(thm)],[c_31958,c_31964]) ).
tcf(c_32222,plain,
! [X0: $i] : iPr_def_27(multiply(iPr_def_28,inverse(X0))) = iPr_def_35(iPr_def_35(X0)),
inference(demodulation,[status(thm)],[c_32221,c_31619,c_31627]) ).
tcf(c_32878,plain,
! [X0: $i] : iPr_def_12(iPr_def_17(inverse(inverse(X0))),iPr_def_28,iPr_def_28) = inverse(multiply(iPr_def_28,iPr_def_35(inverse(X0)))),
inference(superposition,[status(thm)],[c_31328,c_30324]) ).
tcf(c_32888,plain,
! [X0: $i] : multiply(iPr_def_28,multiply(iPr_def_28,iPr_def_35(inverse(X0)))) = iPr_def_27(iPr_def_17(inverse(inverse(X0)))),
inference(superposition,[status(thm)],[c_31328,c_9829]) ).
tcf(c_32902,plain,
! [X0: $i] : multiply(iPr_def_28,iPr_def_17(inverse(iPr_def_35(inverse(X0))))) = iPr_def_35(iPr_def_17(inverse(inverse(X0)))),
inference(superposition,[status(thm)],[c_31328,c_31589]) ).
tcf(c_33309,plain,
! [X0: $i] : multiply(iPr_def_28,iPr_def_17(inverse(iPr_def_35(inverse(X0))))) = iPr_def_27(inverse(X0)),
inference(demodulation,[status(thm)],[c_32902,c_31627,c_31964]) ).
tcf(c_33310,plain,
! [X0: $i] : multiply(iPr_def_28,multiply(iPr_def_28,iPr_def_35(inverse(X0)))) = iPr_def_35(iPr_def_27(X0)),
inference(demodulation,[status(thm)],[c_32888,c_31602]) ).
tcf(c_33315,plain,
! [X0: $i] : inverse(multiply(iPr_def_28,iPr_def_35(inverse(X0)))) = iPr_def_35(inverse(inverse(X0))),
inference(demodulation,[status(thm)],[c_32878,c_31156]) ).
tcf(c_36068,plain,
! [X0: $i] : multiply(iPr_def_28,iPr_def_17(inverse(iPr_def_35(inverse(inverse(X0)))))) = iPr_def_35(multiply(iPr_def_28,iPr_def_35(inverse(X0)))),
inference(superposition,[status(thm)],[c_33315,c_31589]) ).
tcf(c_36262,plain,
! [X0: $i] : iPr_def_35(multiply(iPr_def_28,iPr_def_35(inverse(X0)))) = iPr_def_27(inverse(inverse(X0))),
inference(demodulation,[status(thm)],[c_36068,c_33309]) ).
tcf(c_39789,plain,
! [X0: $i] : iPr_def_17(iPr_def_17(iPr_def_27(inverse(inverse(X0))))) = multiply(iPr_def_28,iPr_def_35(inverse(X0))),
inference(superposition,[status(thm)],[c_36262,c_31906]) ).
tcf(c_39942,plain,
! [X0: $i] : multiply(iPr_def_28,iPr_def_35(inverse(X0))) = iPr_def_17(inverse(inverse(inverse(X0)))),
inference(demodulation,[status(thm)],[c_39789,c_6159]) ).
tcf(c_40158,plain,
! [X0: $i] : multiply(iPr_def_28,iPr_def_17(inverse(inverse(inverse(X0))))) = iPr_def_35(iPr_def_27(X0)),
inference(demodulation,[status(thm)],[c_33310,c_39942]) ).
tcf(c_40160,plain,
! [X0: $i] : iPr_def_35(inverse(X0)) = iPr_def_35(iPr_def_27(X0)),
inference(demodulation,[status(thm)],[c_40158,c_31589]) ).
tcf(c_40172,plain,
! [X0: $i] : inverse(iPr_def_17(inverse(inverse(X0)))) = iPr_def_35(iPr_def_27(X0)),
inference(demodulation,[status(thm)],[c_31328,c_40160]) ).
tcf(c_40173,plain,
! [X0: $i] : iPr_def_17(iPr_def_35(iPr_def_27(X0))) = iPr_def_35(iPr_def_27(X0)),
inference(demodulation,[status(thm)],[c_31991,c_40160]) ).
tcf(c_40175,plain,
! [X0: $i] : iPr_def_17(iPr_def_35(iPr_def_27(X0))) = iPr_def_27(X0),
inference(demodulation,[status(thm)],[c_31627,c_40160]) ).
tcf(c_40176,plain,
! [X0: $i] : iPr_def_35(iPr_def_27(X0)) = iPr_def_27(X0),
inference(demodulation,[status(thm)],[c_40173,c_40175]) ).
tcf(c_40184,plain,
! [X0: $i] : inverse(iPr_def_17(inverse(inverse(X0)))) = iPr_def_27(X0),
inference(demodulation,[status(thm)],[c_40172,c_40176]) ).
tcf(c_40319,plain,
! [X0: $i] : iPr_def_17(iPr_def_17(iPr_def_35(iPr_def_27(X0)))) = inverse(X0),
inference(superposition,[status(thm)],[c_40160,c_31906]) ).
tcf(c_40359,plain,
! [X0: $i] : iPr_def_17(iPr_def_27(X0)) = iPr_def_27(X0),
inference(superposition,[status(thm)],[c_40175,c_31906]) ).
tcf(c_40502,plain,
! [X0: $i] : iPr_def_35(iPr_def_35(iPr_def_17(inverse(inverse(X0))))) = iPr_def_27(multiply(iPr_def_28,iPr_def_27(X0))),
inference(superposition,[status(thm)],[c_40184,c_32222]) ).
tcf(c_40551,plain,
! [X0: $i] : inverse(X0) = iPr_def_27(X0),
inference(demodulation,[status(thm)],[c_40319,c_31906]) ).
tcf(c_40639,plain,
! [X0: $i] : iPr_def_27(multiply(iPr_def_28,iPr_def_27(X0))) = iPr_def_35(iPr_def_35(iPr_def_27(iPr_def_27(X0)))),
inference(demodulation,[status(thm)],[c_40502,c_40359,c_40551]) ).
tcf(c_40640,plain,
! [X0: $i] : iPr_def_27(multiply(iPr_def_28,iPr_def_27(X0))) = iPr_def_27(iPr_def_27(X0)),
inference(demodulation,[status(thm)],[c_40639,c_40176]) ).
tcf(c_40781,plain,
! [X0: $i,X1: $i] : multiply(inverse(multiply(X0,iPr_def_27(X1))),iPr_def_17(X0)) = iPr_def_35(X1),
inference(demodulation,[status(thm)],[c_29150,c_40551]) ).
tcf(c_40782,plain,
! [X0: $i,X1: $i] : multiply(inverse(inverse(X0)),multiply(iPr_def_27(X0),iPr_def_27(X1))) = iPr_def_27(X1),
inference(demodulation,[status(thm)],[c_6942,c_40551]) ).
tcf(c_40784,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(inverse(X0),multiply(iPr_def_10(X0,X1),iPr_def_27(X2))) = iPr_def_27(X2),
inference(demodulation,[status(thm)],[c_6329,c_40551]) ).
tcf(c_40809,plain,
! [X0: $i] : multiply(iPr_def_28,iPr_def_17(inverse(iPr_def_27(X0)))) = iPr_def_35(X0),
inference(demodulation,[status(thm)],[c_31589,c_40551]) ).
tcf(c_40810,plain,
! [X0: $i,X1: $i] : iPr_def_17(iPr_def_17(inverse(multiply(iPr_def_28,iPr_def_27(X0))))) = iPr_def_10(X0,X1),
inference(demodulation,[status(thm)],[c_30044,c_40551]) ).
tcf(c_40811,plain,
! [X0: $i] : inverse(multiply(iPr_def_28,iPr_def_27(X0))) = iPr_def_12(X0,iPr_def_28,iPr_def_28),
inference(demodulation,[status(thm)],[c_30324,c_40551]) ).
tcf(c_40821,plain,
! [X0: $i] : multiply(iPr_def_27(X0),X0) = iPr_def_28,
inference(demodulation,[status(thm)],[c_9739,c_40551]) ).
tcf(c_40880,plain,
! [X0: $i] : iPr_def_12(X0,iPr_def_28,iPr_def_28) = iPr_def_27(iPr_def_27(X0)),
inference(demodulation,[status(thm)],[c_40811,c_40551,c_40640]) ).
tcf(c_40889,plain,
! [X0: $i] : iPr_def_17(iPr_def_27(iPr_def_27(X0))) = iPr_def_35(X0),
inference(demodulation,[status(thm)],[c_31616,c_40880]) ).
tcf(c_40909,plain,
! [X0: $i] : iPr_def_27(iPr_def_27(X0)) = iPr_def_35(X0),
inference(demodulation,[status(thm)],[c_40889,c_40359]) ).
tcf(c_40916,plain,
! [X0: $i,X1: $i] : iPr_def_17(iPr_def_17(iPr_def_35(X0))) = iPr_def_10(X0,X1),
inference(demodulation,[status(thm)],[c_40810,c_40551,c_40640,c_40909]) ).
tcf(c_40917,plain,
! [X0: $i,X1: $i] : iPr_def_10(X0,X1) = X0,
inference(demodulation,[status(thm)],[c_40916,c_31906]) ).
tcf(c_40923,plain,
! [X0: $i] : iPr_def_17(X0) = X0,
inference(demodulation,[status(thm)],[c_5155,c_40917]) ).
tcf(c_40942,plain,
! [X0: $i] : multiply(X0,iPr_def_28) = X0,
inference(demodulation,[status(thm)],[c_9833,c_40923]) ).
tcf(c_40953,plain,
! [X0: $i] : iPr_def_17(iPr_def_35(X0)) = X0,
inference(demodulation,[status(thm)],[c_31906,c_40923]) ).
tcf(c_40955,plain,
! [X0: $i] : iPr_def_35(X0) = X0,
inference(demodulation,[status(thm)],[c_40953,c_40923]) ).
tcf(c_40968,plain,
! [X0: $i] : multiply(iPr_def_28,X0) = X0,
inference(demodulation,[status(thm)],[c_40809,c_40551,c_40909,c_40923,c_40955]) ).
tcf(c_40972,plain,
! [X0: $i,X1: $i] : multiply(iPr_def_27(X0),multiply(X0,iPr_def_27(X1))) = iPr_def_27(X1),
inference(demodulation,[status(thm)],[c_40784,c_40551,c_40917]) ).
tcf(c_40973,plain,
! [X0: $i,X1: $i] : multiply(X0,multiply(iPr_def_27(X0),iPr_def_27(X1))) = iPr_def_27(X1),
inference(demodulation,[status(thm)],[c_40782,c_40551,c_40909,c_40955]) ).
tcf(c_40974,plain,
! [X0: $i,X1: $i] : multiply(iPr_def_27(multiply(X0,iPr_def_27(X1))),X0) = X1,
inference(demodulation,[status(thm)],[c_40781,c_40551,c_40923,c_40955]) ).
tcf(c_41223,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(multiply(inverse(X0),multiply(multiply(inverse(multiply(multiply(inverse(multiply(iPr_def_10(X1,iPr_def_28),inverse(multiply(X2,inverse(iPr_def_28))))),X1),inverse(multiply(X0,multiply(inverse(inverse(iPr_def_28)),inverse(iPr_def_28)))))),X2),inverse(multiply(inverse(inverse(iPr_def_28)),inverse(iPr_def_28))))),inverse(multiply(inverse(multiply(inverse(inverse(iPr_def_28)),inverse(iPr_def_28))),multiply(inverse(inverse(iPr_def_28)),inverse(iPr_def_28))))) = inverse(multiply(inverse(inverse(iPr_def_28)),inverse(iPr_def_28))),
inference(superposition,[status(thm)],[c_40942,c_163]) ).
tcf(c_41271,plain,
! [X0: $i,X1: $i] : multiply(iPr_def_27(multiply(X0,iPr_def_35(X1))),X0) = iPr_def_27(X1),
inference(superposition,[status(thm)],[c_40909,c_40974]) ).
tcf(c_41318,plain,
! [X0: $i,X1: $i] : multiply(iPr_def_27(X0),multiply(X0,iPr_def_35(X1))) = iPr_def_35(X1),
inference(superposition,[status(thm)],[c_40909,c_40972]) ).
tcf(c_41324,plain,
! [X0: $i,X1: $i] : multiply(multiply(iPr_def_27(X0),iPr_def_27(X1)),X1) = iPr_def_27(X0),
inference(superposition,[status(thm)],[c_40974,c_40973]) ).
tcf(c_41346,plain,
! [X0: $i,X1: $i] : multiply(X0,multiply(iPr_def_27(X0),iPr_def_35(X1))) = iPr_def_35(X1),
inference(superposition,[status(thm)],[c_40909,c_40973]) ).
tcf(c_41395,plain,
! [X0: $i,X1: $i] : multiply(X0,multiply(iPr_def_27(X0),X1)) = X1,
inference(demodulation,[status(thm)],[c_41346,c_40955]) ).
tcf(c_41396,plain,
! [X0: $i,X1: $i] : multiply(iPr_def_27(X0),multiply(X0,X1)) = X1,
inference(demodulation,[status(thm)],[c_41318,c_40955]) ).
tcf(c_41398,plain,
! [X0: $i,X1: $i] : multiply(iPr_def_27(multiply(X0,X1)),X0) = iPr_def_27(X1),
inference(demodulation,[status(thm)],[c_41271,c_40955]) ).
tcf(c_41452,plain,
! [X0: $i,X1: $i] : multiply(iPr_def_27(X0),multiply(iPr_def_12(X0,iPr_def_27(iPr_def_28),multiply(X1,iPr_def_27(iPr_def_28))),X1)) = iPr_def_28,
inference(demodulation,[status(thm)],[c_41223,c_28906,c_30957,c_40551,c_40909,c_40942,c_40955,c_40968]) ).
tcf(c_41453,plain,
! [X0: $i,X1: $i] : multiply(iPr_def_27(X0),multiply(iPr_def_12(X0,iPr_def_28,multiply(X1,iPr_def_28)),X1)) = iPr_def_28,
inference(light_normalisation,[status(thm)],[c_41452,c_9509]) ).
tcf(c_41454,plain,
! [X0: $i,X1: $i] : multiply(iPr_def_27(X0),multiply(iPr_def_12(X0,iPr_def_28,X1),X1)) = iPr_def_28,
inference(demodulation,[status(thm)],[c_41453,c_40942]) ).
tcf(c_41522,plain,
! [X0: $i] : iPr_def_27(iPr_def_27(X0)) = X0,
inference(demodulation,[status(thm)],[c_40974,c_41398]) ).
tcf(c_41646,plain,
! [X0: $i,X1: $i] : multiply(iPr_def_27(X0),iPr_def_27(X1)) = iPr_def_27(multiply(X1,X0)),
inference(superposition,[status(thm)],[c_41396,c_41398]) ).
tcf(c_41653,plain,
! [X0: $i,X1: $i] : multiply(multiply(X0,X1),iPr_def_27(X1)) = X0,
inference(superposition,[status(thm)],[c_41398,c_41395]) ).
tcf(c_41657,plain,
! [X0: $i,X1: $i] : iPr_def_27(multiply(iPr_def_27(X0),X1)) = multiply(iPr_def_27(X1),X0),
inference(superposition,[status(thm)],[c_41398,c_41324]) ).
tcf(c_41668,plain,
! [X0: $i,X1: $i] : multiply(multiply(X0,iPr_def_27(X1)),X1) = X0,
inference(superposition,[status(thm)],[c_41522,c_41324]) ).
tcf(c_42125,plain,
! [X0: $i,X1: $i] : iPr_def_27(multiply(X0,iPr_def_27(X1))) = multiply(X1,iPr_def_27(X0)),
inference(superposition,[status(thm)],[c_41522,c_41646]) ).
tcf(c_42143,plain,
! [X0: $i,X1: $i] : multiply(X0,iPr_def_27(multiply(X1,X0))) = iPr_def_27(X1),
inference(superposition,[status(thm)],[c_41646,c_41395]) ).
tcf(c_42243,plain,
! [X0: $i,X1: $i] : multiply(iPr_def_12(X0,iPr_def_28,X1),X1) = multiply(X0,iPr_def_28),
inference(superposition,[status(thm)],[c_41454,c_41395]) ).
tcf(c_42317,plain,
! [X0: $i,X1: $i] : multiply(iPr_def_12(X0,iPr_def_28,X1),X1) = X0,
inference(demodulation,[status(thm)],[c_42243,c_40942]) ).
tcf(c_42455,plain,
! [X0: $i,X1: $i] : multiply(X0,iPr_def_27(X1)) = iPr_def_12(X0,iPr_def_28,X1),
inference(superposition,[status(thm)],[c_42317,c_41653]) ).
tcf(c_42460,plain,
! [X0: $i,X1: $i] : iPr_def_12(X0,iPr_def_28,iPr_def_27(X1)) = multiply(X0,X1),
inference(superposition,[status(thm)],[c_42317,c_41668]) ).
tcf(c_42502,plain,
! [X0: $i,X1: $i] : iPr_def_27(iPr_def_12(X0,iPr_def_28,X1)) = multiply(X1,iPr_def_27(X0)),
inference(superposition,[status(thm)],[c_42317,c_42143]) ).
tcf(c_42561,plain,
! [X0: $i,X1: $i] : multiply(X0,iPr_def_27(multiply(X1,iPr_def_27(iPr_def_27(X0))))) = iPr_def_27(X1),
inference(superposition,[status(thm)],[c_41668,c_42125]) ).
tcf(c_42783,plain,
! [X0: $i,X1: $i] : iPr_def_27(iPr_def_12(X0,iPr_def_28,X1)) = iPr_def_12(X1,iPr_def_28,X0),
inference(demodulation,[status(thm)],[c_42502,c_42455]) ).
tcf(c_42810,plain,
! [X0: $i,X1: $i] : iPr_def_12(X0,iPr_def_28,multiply(X1,X0)) = iPr_def_27(X1),
inference(demodulation,[status(thm)],[c_42561,c_42455,c_42460]) ).
tcf(c_43376,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_27(multiply(X0,iPr_def_27(multiply(X1,X2)))) = iPr_def_12(X1,X2,X0),
inference(superposition,[status(thm)],[c_40551,c_28906]) ).
tcf(c_43417,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(iPr_def_27(inverse(multiply(X0,X1))),X2) = iPr_def_12(X0,X1,iPr_def_27(X2)),
inference(superposition,[status(thm)],[c_28906,c_41657]) ).
tcf(c_43533,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : iPr_def_12(multiply(inverse(multiply(iPr_def_10(inverse(multiply(X0,X1)),X2),inverse(multiply(X3,multiply(inverse(X2),X2))))),inverse(X1)),iPr_def_28,iPr_def_10(X0,X1)) = iPr_def_27(inverse(iPr_def_10(X3,multiply(inverse(X2),X2)))),
inference(superposition,[status(thm)],[c_309,c_42810]) ).
tcf(c_43565,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(iPr_def_17(iPr_def_12(X0,X1,X2)),X2) = iPr_def_35(multiply(X0,X1)),
inference(superposition,[status(thm)],[c_40923,c_30933]) ).
tcf(c_43593,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(iPr_def_12(X0,X1,X2),X2) = multiply(X0,X1),
inference(demodulation,[status(thm)],[c_43565,c_40923,c_40955]) ).
tcf(c_43597,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_12(multiply(X0,X1),iPr_def_28,X2) = iPr_def_12(X0,X1,X2),
inference(demodulation,[status(thm)],[c_43376,c_42455,c_42783]) ).
tcf(c_43603,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(multiply(X0,X1),X2) = iPr_def_12(X0,X1,iPr_def_27(X2)),
inference(demodulation,[status(thm)],[c_43417,c_40551,c_41522]) ).
tcf(c_43699,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : iPr_def_12(inverse(multiply(iPr_def_10(inverse(multiply(X0,X1)),X2),inverse(multiply(X3,multiply(inverse(X2),X2))))),inverse(X1),iPr_def_10(X0,X1)) = iPr_def_27(inverse(iPr_def_10(X3,multiply(inverse(X2),X2)))),
inference(demodulation,[status(thm)],[c_43533,c_43597]) ).
tcf(c_43700,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_12(multiply(X0,multiply(X1,X2)),iPr_def_27(X2),X1) = X0,
inference(demodulation,[status(thm)],[c_43699,c_28906,c_40551,c_40821,c_40917,c_41522,c_42460]) ).
tcf(c_43929,plain,
multiply(a3,multiply(b3,c3)) != iPr_def_12(a3,b3,iPr_def_27(c3)),
inference(demodulation,[status(thm)],[c_52,c_43603]) ).
tcf(c_44306,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(multiply(X0,multiply(X1,X2)),iPr_def_27(X2)) = multiply(X0,X1),
inference(superposition,[status(thm)],[c_43700,c_43593]) ).
tcf(c_44340,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_12(X0,multiply(X1,X2),X2) = multiply(X0,X1),
inference(demodulation,[status(thm)],[c_44306,c_41522,c_43603]) ).
tcf(c_44648,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(multiply(X0,X1),X2) = multiply(X0,multiply(X1,X2)),
inference(superposition,[status(thm)],[c_44340,c_43593]) ).
tcf(c_44797,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(X0,multiply(X1,X2)) = iPr_def_12(X0,X1,iPr_def_27(X2)),
inference(demodulation,[status(thm)],[c_44648,c_43603]) ).
tcf(c_44990,plain,
$false,
inference(backward_subsumption_resolution,[status(thm)],[c_43929,c_44797]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : GRP411-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.02 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.02/0.30 % Computer : n012.cluster.edu
% 0.02/0.30 % Model : x86_64 x86_64
% 0.02/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.02/0.30 % Memory : 8046.5625MB
% 0.02/0.30 % OS : Linux 6.8.0-71-generic
% 0.02/0.30 % CPULimit : 300
% 0.02/0.30 % WCLimit : 300
% 0.02/0.30 % DateTime : Wed Sep 23 14:41:07 UTC 2026
% 0.02/0.30 % CPUTime :
% 0.02/0.30 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.02/0.33 Running UEQ theorem proving
% 0.02/0.33 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.02/0.34
% 0.02/0.34 % ======== iProver multi-core TPTP/SMT =========
% 0.02/0.34
% 0.02/0.34 % Detected problem language: tptp
% 0.06/0.35 % Proving...
% 27.12/4.67 WARNING - Clausifier option not provided in the heuristic config "heur/vip2_118404", setting default options.
% 27.12/4.67 % SZS status Started for theBenchmark.p
% 27.12/4.67 % SZS status Unsatisfiable for theBenchmark.p
% 27.12/4.67
% 27.12/4.67 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 27.12/4.67
% 27.12/4.67 % ------ iProver source info
% 27.12/4.67
% 27.12/4.67 % git: date: 2026-07-19 20:42:38 +0200
% 27.12/4.67 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 27.12/4.67 % git: non_committed_changes: false
% 27.12/4.67
% 27.12/4.67 % ------ Parsing...% successful
% 27.12/4.67
% 27.12/4.67
% 27.12/4.67 % ------ Clausification by vclausify_rel & Parsing by iProver...
% 27.12/4.67 % ------ Proving...
% 27.12/4.67 % ------ Problem Properties
% 27.12/4.67
% 27.12/4.67 %
% 27.12/4.67 % clauses 2
% 27.12/4.67 % conjectures 1
% 27.12/4.67 % EPR 0
% 27.12/4.67 % Horn 2
% 27.12/4.67 % unary 2
% 27.12/4.67 % binary 0
% 27.12/4.67 % lits 2
% 27.12/4.67 % lits eq 2
% 27.12/4.67 % fd_pure 0
% 27.12/4.67 % fd_pseudo 0
% 27.12/4.67 % fd_cond 0
% 27.12/4.67 % fd_pseudo_cond 0
% 27.12/4.67 % AC symbols 0
% 27.12/4.67
% 27.12/4.67 % ------ Input Options Time Limit: Unbounded
% 27.12/4.67
% 27.12/4.67
% 27.12/4.67 % ------
% 27.12/4.67 % Current options:
% 27.12/4.67 % ------
% 27.12/4.67
% 27.12/4.67
% 27.12/4.67 %
% 27.12/4.67
% 27.12/4.67 % ------ Proving...
% 27.12/4.67 %
% 27.12/4.67
% 27.12/4.67 % SZS status Unsatisfiable for theBenchmark.p
% 27.12/4.67
% 27.12/4.67 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 27.12/4.67
% 27.12/4.67
%------------------------------------------------------------------------------