%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : GRP423-1 : TPTP v9.3.1. Released v2.6.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% Computer : n005.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:52 PM UTC 2026
% Result : Unsatisfiable 11.92s 2.33s
% Output : CNFRefutation 11.92s
% Verified :
% SZS Type : Refutation
% Derivation depth : 48
% Number of leaves : 2
% Syntax : Number of formulae : 233 ( 233 unt; 0 def)
% Number of atoms : 1091 ( 232 equ)
% Maximal formula atoms : 1 ( 4 avg)
% Number of connectives : 3 ( 3 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 3 avg)
% Maximal term depth : 19 ( 3 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 7 ( 5 usr; 2 prp; 0-3 aty)
% Number of functors : 5 ( 5 usr; 3 con; 0-2 aty)
% Number of variables : 532 ( 0 sgn 532 !; 0 ?; 529 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X2,X0,X1] : inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),multiply(inverse(X2),inverse(multiply(inverse(X2),X2))))))),multiply(X0,X2))) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',single_axiom) ).
fof(f2,negated_conjecture,
multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_these_axioms_3) ).
tcf(c_51,plain,
! [X0: $i,X1: $i,X2: $i] : inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),multiply(inverse(X2),inverse(multiply(inverse(X2),X2))))))),multiply(X0,X2))) = X1,
inference(cnf_transformation,[],[f1]) ).
tcf(c_52,negated_conjecture,
multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3)),
inference(cnf_transformation,[],[f2]) ).
tcf(c_62,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] : inverse(multiply(inverse(multiply(X0,inverse(multiply(X1,multiply(inverse(X2),inverse(multiply(inverse(X2),X2))))))),multiply(X0,X2))) = multiply(inverse(multiply(X3,inverse(multiply(inverse(X1),multiply(inverse(X4),inverse(multiply(inverse(X4),X4))))))),multiply(X3,X4)),
inference(superposition,[status(thm)],[c_51,c_51]) ).
tcf(c_63,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] : inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),multiply(X2,inverse(multiply(X2,multiply(inverse(multiply(X3,inverse(multiply(inverse(X2),multiply(inverse(X4),inverse(multiply(inverse(X4),X4))))))),multiply(X3,X4))))))))),multiply(X0,multiply(inverse(multiply(X3,inverse(multiply(inverse(X2),multiply(inverse(X4),inverse(multiply(inverse(X4),X4))))))),multiply(X3,X4))))) = X1,
inference(superposition,[status(thm)],[c_51,c_51]) ).
tcf(c_64,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(inverse(X0),inverse(multiply(inverse(X1),multiply(inverse(inverse(multiply(inverse(X0),X0))),inverse(multiply(inverse(inverse(multiply(inverse(X0),X0))),inverse(multiply(inverse(X0),X0)))))))) = inverse(multiply(inverse(multiply(X2,X1)),multiply(X2,X0))),
inference(superposition,[status(thm)],[c_51,c_51]) ).
tcf(c_65,plain,
! [X0: $i,X1: $i,X2: $i] : inverse(multiply(inverse(multiply(X0,inverse(multiply(X1,multiply(inverse(X2),inverse(multiply(inverse(X2),X2))))))),multiply(X0,X2))) = iPr_def_10(X1),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_10])],[c_62]) ).
tcf(c_66,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),multiply(inverse(X2),inverse(multiply(inverse(X2),X2))))))),multiply(X0,X2)) = iPr_def_10(X1),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_62]) ).
tcf(c_67,plain,
! [X0: $i,X1: $i,X2: $i] : inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),multiply(X2,inverse(multiply(X2,iPr_def_10(X2)))))))),multiply(X0,iPr_def_10(X2)))) = X1,
inference(demodulation,[status(thm)],[c_63,c_66]) ).
tcf(c_68,plain,
! [X0: $i] : iPr_def_10(inverse(X0)) = X0,
inference(demodulation,[status(thm)],[c_51,c_65]) ).
tcf(c_89,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_10(inverse(multiply(inverse(X0),inverse(multiply(X1,multiply(inverse(inverse(multiply(inverse(X0),X0))),inverse(multiply(inverse(inverse(multiply(inverse(X0),X0))),inverse(multiply(inverse(X0),X0)))))))))) = inverse(multiply(inverse(multiply(X2,iPr_def_10(X1))),multiply(X2,X0))),
inference(superposition,[status(thm)],[c_65,c_65]) ).
tcf(c_100,plain,
! [X0: $i] : inverse(iPr_def_10(X0)) = iPr_def_10(inverse(X0)),
inference(superposition,[status(thm)],[c_66,c_65]) ).
tcf(c_101,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(X0,inverse(multiply(X1,multiply(inverse(inverse(multiply(X0,iPr_def_10(X0)))),inverse(multiply(inverse(inverse(multiply(X0,iPr_def_10(X0)))),inverse(multiply(X0,iPr_def_10(X0))))))))) = inverse(multiply(inverse(multiply(X2,iPr_def_10(X1))),multiply(X2,iPr_def_10(X0)))),
inference(superposition,[status(thm)],[c_65,c_67]) ).
tcf(c_107,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] : inverse(multiply(inverse(multiply(X0,inverse(multiply(X1,multiply(X2,inverse(multiply(X2,iPr_def_10(X2)))))))),multiply(X0,iPr_def_10(X2)))) = multiply(inverse(multiply(X3,inverse(multiply(inverse(X1),multiply(X4,inverse(multiply(X4,iPr_def_10(X4)))))))),multiply(X3,iPr_def_10(X4))),
inference(superposition,[status(thm)],[c_67,c_67]) ).
tcf(c_110,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] : inverse(multiply(inverse(multiply(X0,inverse(multiply(X1,multiply(X2,inverse(multiply(X2,multiply(inverse(multiply(X3,inverse(multiply(inverse(X2),multiply(X4,inverse(multiply(X4,iPr_def_10(X4)))))))),multiply(X3,iPr_def_10(X4)))))))))),multiply(X0,multiply(inverse(multiply(X3,inverse(multiply(inverse(X2),multiply(X4,inverse(multiply(X4,iPr_def_10(X4)))))))),multiply(X3,iPr_def_10(X4)))))) = iPr_def_10(X1),
inference(superposition,[status(thm)],[c_67,c_65]) ).
tcf(c_111,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),multiply(X2,inverse(multiply(X2,iPr_def_10(X2)))))))),multiply(X0,iPr_def_10(X2))) = iPr_def_10(X1),
inference(superposition,[status(thm)],[c_67,c_68]) ).
tcf(c_116,plain,
! [X0: $i,X1: $i,X2: $i] : inverse(multiply(inverse(multiply(X0,multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(multiply(X2,multiply(inverse(inverse(multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(multiply(inverse(X1),X1))))),inverse(multiply(inverse(inverse(multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(multiply(inverse(X1),X1))))),inverse(multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(multiply(inverse(X1),X1)))))))))))),multiply(X0,X1))) = multiply(inverse(X1),iPr_def_10(X2)),
inference(superposition,[status(thm)],[c_65,c_64]) ).
tcf(c_138,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : multiply(inverse(X0),inverse(multiply(inverse(multiply(X1,iPr_def_10(X2))),multiply(inverse(inverse(multiply(inverse(X0),X0))),inverse(multiply(inverse(inverse(multiply(inverse(X0),X0))),inverse(multiply(inverse(X0),X0)))))))) = inverse(multiply(X3,multiply(inverse(multiply(X1,inverse(multiply(inverse(X3),multiply(X2,inverse(multiply(X2,iPr_def_10(X2)))))))),X0))),
inference(superposition,[status(thm)],[c_67,c_64]) ).
tcf(c_139,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : multiply(inverse(X0),inverse(multiply(inverse(multiply(X1,X2)),multiply(inverse(inverse(multiply(inverse(X0),X0))),inverse(multiply(inverse(inverse(multiply(inverse(X0),X0))),inverse(multiply(inverse(X0),X0)))))))) = inverse(multiply(inverse(iPr_def_10(X3)),multiply(inverse(multiply(X1,inverse(multiply(inverse(X3),multiply(inverse(X2),inverse(multiply(inverse(X2),X2))))))),X0))),
inference(superposition,[status(thm)],[c_66,c_64]) ).
tcf(c_141,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : multiply(inverse(multiply(X0,X1)),inverse(multiply(inverse(X2),multiply(inverse(inverse(multiply(inverse(multiply(X0,X1)),multiply(X0,X1)))),inverse(multiply(inverse(inverse(multiply(inverse(multiply(X0,X1)),multiply(X0,X1)))),inverse(multiply(inverse(multiply(X0,X1)),multiply(X0,X1))))))))) = inverse(multiply(inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X3),multiply(inverse(X1),inverse(multiply(inverse(X1),X1))))))),X2)),iPr_def_10(X3))),
inference(superposition,[status(thm)],[c_66,c_64]) ).
tcf(c_142,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(inverse(inverse(multiply(inverse(multiply(X0,X1)),multiply(X0,X2)))),multiply(inverse(X2),inverse(multiply(inverse(X2),X2)))) = iPr_def_10(X1),
inference(superposition,[status(thm)],[c_64,c_66]) ).
tcf(c_145,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : inverse(multiply(inverse(multiply(X0,X1)),multiply(X0,X2))) = inverse(multiply(inverse(multiply(X3,X1)),multiply(X3,X2))),
inference(superposition,[status(thm)],[c_64,c_64]) ).
tcf(c_146,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : multiply(inverse(X0),inverse(multiply(inverse(inverse(multiply(inverse(X1),multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2)))))))),multiply(inverse(inverse(multiply(inverse(X0),X0))),inverse(multiply(inverse(inverse(multiply(inverse(X0),X0))),inverse(multiply(inverse(X0),X0)))))))) = inverse(multiply(inverse(inverse(multiply(inverse(multiply(X3,X1)),multiply(X3,X2)))),multiply(inverse(X2),X0))),
inference(superposition,[status(thm)],[c_64,c_64]) ).
tcf(c_149,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] : inverse(multiply(inverse(multiply(X0,inverse(multiply(multiply(inverse(X1),inverse(multiply(inverse(X2),multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(multiply(inverse(X1),X1)))))))),multiply(X3,inverse(multiply(X3,iPr_def_10(X3)))))))),multiply(X0,iPr_def_10(X3)))) = multiply(inverse(multiply(X4,X2)),multiply(X4,X1)),
inference(superposition,[status(thm)],[c_64,c_67]) ).
tcf(c_154,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : inverse(multiply(inverse(multiply(X0,inverse(multiply(X1,multiply(inverse(multiply(X2,X3)),multiply(inverse(X3),inverse(multiply(inverse(X3),multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(multiply(inverse(X3),X3))))))))))))),multiply(X0,multiply(X2,X3)))) = iPr_def_10(X1),
inference(superposition,[status(thm)],[c_64,c_65]) ).
tcf(c_157,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : multiply(inverse(multiply(X0,X1)),inverse(multiply(inverse(X2),multiply(inverse(multiply(inverse(X1),inverse(multiply(inverse(X1),multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(multiply(inverse(X1),X1))))))))),inverse(multiply(inverse(multiply(inverse(X1),inverse(multiply(inverse(X1),multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(multiply(inverse(X1),X1))))))))),multiply(inverse(X1),inverse(multiply(inverse(X1),multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(multiply(inverse(X1),X1)))))))))))))) = inverse(multiply(inverse(multiply(X3,X2)),multiply(X3,multiply(X0,X1)))),
inference(superposition,[status(thm)],[c_64,c_64]) ).
tcf(c_158,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : inverse(multiply(multiply(inverse(X0),inverse(multiply(inverse(X1),multiply(inverse(inverse(multiply(inverse(X0),X0))),inverse(multiply(inverse(inverse(multiply(inverse(X0),X0))),inverse(multiply(inverse(X0),X0)))))))),multiply(inverse(multiply(X2,X1)),X3))) = multiply(inverse(X3),inverse(multiply(inverse(multiply(X2,X0)),multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(multiply(inverse(X3),X3)))))))),
inference(superposition,[status(thm)],[c_64,c_64]) ).
tcf(c_159,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),inverse(multiply(inverse(inverse(multiply(X1,multiply(inverse(X0),inverse(multiply(inverse(X0),X0)))))),multiply(inverse(inverse(multiply(inverse(X0),X0))),inverse(multiply(inverse(inverse(multiply(inverse(X0),X0))),inverse(multiply(inverse(X0),X0)))))))) = iPr_def_10(X1),
inference(superposition,[status(thm)],[c_64,c_65]) ).
tcf(c_161,plain,
! [X0: $i] : inverse(iPr_def_10(X0)) = X0,
inference(demodulation,[status(thm)],[c_100,c_68]) ).
tcf(c_162,plain,
! [X0: $i,X1: $i,X2: $i] : inverse(multiply(inverse(multiply(X0,X1)),multiply(X0,X2))) = iPr_def_11(X1,X2),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_11])],[c_145]) ).
tcf(c_164,plain,
! [X0: $i,X1: $i] : multiply(inverse(iPr_def_11(X0,X1)),multiply(inverse(X1),inverse(multiply(inverse(X1),X1)))) = iPr_def_10(X0),
inference(demodulation,[status(thm)],[c_142,c_162]) ).
tcf(c_166,plain,
! [X0: $i,X1: $i] : multiply(X0,inverse(multiply(X1,multiply(inverse(inverse(multiply(X0,iPr_def_10(X0)))),inverse(multiply(inverse(inverse(multiply(X0,iPr_def_10(X0)))),inverse(multiply(X0,iPr_def_10(X0))))))))) = iPr_def_11(iPr_def_10(X1),iPr_def_10(X0)),
inference(demodulation,[status(thm)],[c_101,c_162]) ).
tcf(c_167,plain,
! [X0: $i,X1: $i] : iPr_def_11(inverse(multiply(X0,multiply(X1,inverse(multiply(X1,iPr_def_10(X1)))))),iPr_def_10(X1)) = iPr_def_10(X0),
inference(demodulation,[status(thm)],[c_107,c_111,c_162]) ).
tcf(c_171,plain,
! [X0: $i,X1: $i] : iPr_def_10(inverse(multiply(inverse(X0),inverse(multiply(X1,multiply(inverse(inverse(multiply(inverse(X0),X0))),inverse(multiply(inverse(inverse(multiply(inverse(X0),X0))),inverse(multiply(inverse(X0),X0)))))))))) = iPr_def_11(iPr_def_10(X1),X0),
inference(demodulation,[status(thm)],[c_89,c_162]) ).
tcf(c_172,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),inverse(multiply(X1,multiply(inverse(inverse(multiply(inverse(X0),X0))),inverse(multiply(inverse(inverse(multiply(inverse(X0),X0))),inverse(multiply(inverse(X0),X0)))))))) = iPr_def_11(iPr_def_10(X1),X0),
inference(demodulation,[status(thm)],[c_171,c_68]) ).
tcf(c_174,plain,
! [X0: $i,X1: $i] : iPr_def_11(iPr_def_10(inverse(inverse(multiply(X0,multiply(inverse(X1),inverse(multiply(inverse(X1),X1))))))),X1) = iPr_def_10(X0),
inference(demodulation,[status(thm)],[c_159,c_172]) ).
tcf(c_175,plain,
! [X0: $i,X1: $i] : iPr_def_11(inverse(multiply(X0,multiply(inverse(X1),inverse(multiply(inverse(X1),X1))))),X1) = iPr_def_10(X0),
inference(demodulation,[status(thm)],[c_174,c_68]) ).
tcf(c_187,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_11(inverse(multiply(X0,multiply(inverse(multiply(X1,X2)),iPr_def_11(iPr_def_10(inverse(X2)),X2)))),multiply(X1,X2)) = iPr_def_10(X0),
inference(demodulation,[status(thm)],[c_154,c_162,c_172]) ).
tcf(c_188,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_11(inverse(multiply(X0,multiply(inverse(multiply(X1,X2)),iPr_def_11(X2,X2)))),multiply(X1,X2)) = iPr_def_10(X0),
inference(demodulation,[status(thm)],[c_187,c_68]) ).
tcf(c_191,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : inverse(multiply(X0,multiply(inverse(multiply(X1,inverse(multiply(inverse(X0),multiply(X2,inverse(multiply(X2,iPr_def_10(X2)))))))),X3))) = iPr_def_11(iPr_def_10(inverse(multiply(X1,iPr_def_10(X2)))),X3),
inference(demodulation,[status(thm)],[c_138,c_172]) ).
tcf(c_192,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : inverse(multiply(X0,multiply(inverse(multiply(X1,inverse(multiply(inverse(X0),multiply(X2,inverse(multiply(X2,iPr_def_10(X2)))))))),X3))) = iPr_def_11(multiply(X1,iPr_def_10(X2)),X3),
inference(demodulation,[status(thm)],[c_191,c_68]) ).
tcf(c_195,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : inverse(multiply(X0,multiply(inverse(multiply(X1,inverse(multiply(inverse(X0),multiply(inverse(X2),inverse(multiply(inverse(X2),X2))))))),X3))) = iPr_def_11(iPr_def_10(inverse(multiply(X1,X2))),X3),
inference(demodulation,[status(thm)],[c_139,c_161,c_172]) ).
tcf(c_196,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : inverse(multiply(X0,multiply(inverse(multiply(X1,inverse(multiply(inverse(X0),multiply(inverse(X2),inverse(multiply(inverse(X2),X2))))))),X3))) = iPr_def_11(multiply(X1,X2),X3),
inference(demodulation,[status(thm)],[c_195,c_68]) ).
tcf(c_199,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(inverse(multiply(X0,X1)),multiply(X0,X2)) = iPr_def_10(iPr_def_11(iPr_def_10(inverse(X1)),X2)),
inference(demodulation,[status(thm)],[c_149,c_162,c_167,c_172]) ).
tcf(c_200,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(inverse(multiply(X0,X1)),multiply(X0,X2)) = iPr_def_10(iPr_def_11(X1,X2)),
inference(demodulation,[status(thm)],[c_199,c_68]) ).
tcf(c_201,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : iPr_def_11(inverse(multiply(X0,multiply(X1,iPr_def_11(multiply(X2,iPr_def_10(X3)),multiply(X2,iPr_def_10(X3)))))),iPr_def_10(X1)) = iPr_def_10(X0),
inference(demodulation,[status(thm)],[c_110,c_111,c_162,c_192]) ).
tcf(c_205,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : inverse(multiply(inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),multiply(inverse(X2),inverse(multiply(inverse(X2),X2))))))),X3)),iPr_def_10(X1))) = iPr_def_11(iPr_def_10(inverse(X3)),multiply(X0,X2)),
inference(demodulation,[status(thm)],[c_141,c_172]) ).
tcf(c_206,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : inverse(multiply(inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),multiply(inverse(X2),inverse(multiply(inverse(X2),X2))))))),X3)),iPr_def_10(X1))) = iPr_def_11(X3,multiply(X0,X2)),
inference(demodulation,[status(thm)],[c_205,c_68]) ).
tcf(c_207,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : inverse(multiply(iPr_def_11(iPr_def_10(inverse(X0)),X1),multiply(inverse(multiply(X2,X0)),X3))) = iPr_def_11(iPr_def_10(inverse(multiply(X2,X1))),X3),
inference(demodulation,[status(thm)],[c_158,c_172]) ).
tcf(c_208,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : inverse(multiply(iPr_def_11(X0,X1),multiply(inverse(multiply(X2,X0)),X3))) = iPr_def_11(multiply(X2,X1),X3),
inference(demodulation,[status(thm)],[c_207,c_68]) ).
tcf(c_211,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_11(iPr_def_10(inverse(inverse(multiply(inverse(X0),multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(multiply(inverse(X1),X1))))))))),X2) = inverse(multiply(inverse(iPr_def_11(X0,X1)),multiply(inverse(X1),X2))),
inference(demodulation,[status(thm)],[c_146,c_162,c_172]) ).
tcf(c_212,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_11(inverse(multiply(inverse(X0),multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(multiply(inverse(X1),X1))))))),X2) = inverse(multiply(inverse(iPr_def_11(X0,X1)),multiply(inverse(X1),X2))),
inference(demodulation,[status(thm)],[c_211,c_68]) ).
tcf(c_215,plain,
! [X0: $i,X1: $i] : iPr_def_11(iPr_def_11(iPr_def_10(X0),inverse(multiply(inverse(X1),X1))),X1) = multiply(inverse(X1),iPr_def_10(X0)),
inference(demodulation,[status(thm)],[c_116,c_162,c_172]) ).
tcf(c_227,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(inverse(multiply(X0,X1)),inverse(multiply(inverse(X2),multiply(inverse(iPr_def_11(iPr_def_10(inverse(X1)),X1)),inverse(multiply(inverse(iPr_def_11(X1,X1)),iPr_def_11(iPr_def_10(inverse(X1)),X1))))))) = iPr_def_11(X2,multiply(X0,X1)),
inference(demodulation,[status(thm)],[c_157,c_162,c_172,c_212]) ).
tcf(c_228,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(inverse(multiply(X0,X1)),inverse(multiply(inverse(X2),multiply(inverse(iPr_def_11(X1,X1)),inverse(multiply(inverse(iPr_def_11(X1,X1)),iPr_def_11(X1,X1))))))) = iPr_def_11(X2,multiply(X0,X1)),
inference(demodulation,[status(thm)],[c_227,c_68]) ).
tcf(c_457,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(inverse(iPr_def_11(X0,multiply(X1,X2))),multiply(inverse(multiply(X1,X2)),inverse(iPr_def_10(iPr_def_11(X2,X2))))) = iPr_def_10(X0),
inference(superposition,[status(thm)],[c_200,c_164]) ).
tcf(c_471,plain,
! [X0: $i,X1: $i] : iPr_def_11(iPr_def_11(X0,inverse(multiply(inverse(X1),X1))),X1) = multiply(inverse(X1),X0),
inference(superposition,[status(thm)],[c_68,c_215]) ).
tcf(c_478,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : inverse(multiply(iPr_def_11(X0,X1),iPr_def_10(iPr_def_11(X0,X2)))) = iPr_def_11(multiply(X3,X1),multiply(X3,X2)),
inference(superposition,[status(thm)],[c_200,c_208]) ).
tcf(c_480,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] : inverse(multiply(iPr_def_11(multiply(X0,X1),X2),multiply(inverse(iPr_def_10(iPr_def_11(X3,X1))),X4))) = iPr_def_11(multiply(inverse(multiply(X0,X3)),X2),X4),
inference(superposition,[status(thm)],[c_200,c_208]) ).
tcf(c_485,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : multiply(iPr_def_11(X0,X1),multiply(inverse(multiply(X2,X0)),X3)) = iPr_def_10(iPr_def_11(multiply(X2,X1),X3)),
inference(superposition,[status(thm)],[c_208,c_68]) ).
tcf(c_500,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : iPr_def_11(inverse(iPr_def_10(iPr_def_11(X0,iPr_def_11(multiply(X1,iPr_def_10(X2)),multiply(X1,iPr_def_10(X2)))))),iPr_def_10(X3)) = iPr_def_10(inverse(multiply(X3,X0))),
inference(superposition,[status(thm)],[c_200,c_201]) ).
tcf(c_594,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] : iPr_def_10(iPr_def_11(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),multiply(inverse(X2),inverse(multiply(inverse(X2),X2))))))),X3),X4)) = multiply(iPr_def_11(multiply(X0,X2),X3),multiply(X1,X4)),
inference(superposition,[status(thm)],[c_196,c_200]) ).
tcf(c_642,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] : multiply(iPr_def_11(X0,multiply(X1,X2)),multiply(inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(X3),multiply(inverse(X2),inverse(multiply(inverse(X2),X2))))))),X0)),X4)) = iPr_def_10(iPr_def_11(iPr_def_10(X3),X4)),
inference(superposition,[status(thm)],[c_206,c_200]) ).
tcf(c_655,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_11(iPr_def_11(X0,iPr_def_11(X1,X1)),multiply(X2,X1)) = multiply(inverse(multiply(X2,X1)),inverse(iPr_def_10(X0))),
inference(superposition,[status(thm)],[c_164,c_228]) ).
tcf(c_677,plain,
! [X0: $i,X1: $i] : iPr_def_11(iPr_def_10(inverse(iPr_def_11(X0,inverse(multiply(X1,iPr_def_10(X1)))))),iPr_def_10(X1)) = multiply(X1,inverse(iPr_def_10(X0))),
inference(superposition,[status(thm)],[c_164,c_166]) ).
tcf(c_739,plain,
! [X0: $i,X1: $i] : iPr_def_11(iPr_def_11(X0,inverse(multiply(X1,iPr_def_10(X1)))),iPr_def_10(X1)) = multiply(X1,X0),
inference(demodulation,[status(thm)],[c_677,c_68,c_161]) ).
tcf(c_740,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_11(iPr_def_11(X0,iPr_def_11(X1,X1)),multiply(X2,X1)) = multiply(inverse(multiply(X2,X1)),X0),
inference(demodulation,[status(thm)],[c_655,c_161]) ).
tcf(c_746,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(inverse(iPr_def_11(X0,multiply(X1,X2))),multiply(inverse(multiply(X1,X2)),iPr_def_11(X2,X2))) = iPr_def_10(X0),
inference(demodulation,[status(thm)],[c_457,c_161]) ).
tcf(c_751,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : iPr_def_11(iPr_def_11(X0,iPr_def_11(multiply(X1,iPr_def_10(X2)),multiply(X1,iPr_def_10(X2)))),iPr_def_10(X3)) = multiply(X3,X0),
inference(demodulation,[status(thm)],[c_500,c_68,c_161]) ).
tcf(c_754,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] : inverse(multiply(iPr_def_11(multiply(X0,X1),X2),multiply(iPr_def_11(X3,X1),X4))) = iPr_def_11(multiply(inverse(multiply(X0,X3)),X2),X4),
inference(demodulation,[status(thm)],[c_480,c_161]) ).
tcf(c_774,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : multiply(iPr_def_11(multiply(X0,X1),multiply(X0,X1)),multiply(X2,X3)) = iPr_def_10(iPr_def_11(iPr_def_10(X2),X3)),
inference(demodulation,[status(thm)],[c_642,c_485,c_594]) ).
tcf(c_1708,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] : iPr_def_11(iPr_def_11(X0,inverse(multiply(iPr_def_11(multiply(X1,X2),multiply(X1,X3)),multiply(iPr_def_11(X4,X2),iPr_def_10(iPr_def_11(X4,X3)))))),multiply(iPr_def_11(X4,X2),iPr_def_10(iPr_def_11(X4,X3)))) = multiply(iPr_def_11(multiply(X1,X2),multiply(X1,X3)),X0),
inference(superposition,[status(thm)],[c_478,c_471]) ).
tcf(c_1725,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : inverse(multiply(iPr_def_11(X0,X1),iPr_def_10(iPr_def_11(X0,X2)))) = inverse(multiply(iPr_def_11(X3,X1),iPr_def_10(iPr_def_11(X3,X2)))),
inference(superposition,[status(thm)],[c_478,c_478]) ).
tcf(c_1787,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_11(inverse(iPr_def_10(iPr_def_11(iPr_def_10(X0),inverse(multiply(X0,iPr_def_10(X0)))))),iPr_def_10(X0)) = iPr_def_10(iPr_def_11(multiply(X1,X2),multiply(X1,X2))),
inference(superposition,[status(thm)],[c_774,c_167]) ).
tcf(c_1788,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_11(inverse(iPr_def_10(iPr_def_11(iPr_def_10(inverse(X0)),inverse(multiply(inverse(X0),X0))))),X0) = iPr_def_10(iPr_def_11(multiply(X1,X2),multiply(X1,X2))),
inference(superposition,[status(thm)],[c_774,c_175]) ).
tcf(c_1789,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : iPr_def_11(inverse(iPr_def_10(iPr_def_11(iPr_def_10(inverse(multiply(X0,X1))),iPr_def_11(X1,X1)))),multiply(X0,X1)) = iPr_def_10(iPr_def_11(multiply(X2,X3),multiply(X2,X3))),
inference(superposition,[status(thm)],[c_774,c_188]) ).
tcf(c_1889,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : iPr_def_11(iPr_def_11(X0,inverse(multiply(iPr_def_11(X1,iPr_def_10(X2)),iPr_def_10(iPr_def_11(X1,iPr_def_10(X2)))))),iPr_def_10(X3)) = multiply(X3,X0),
inference(superposition,[status(thm)],[c_478,c_751]) ).
tcf(c_1940,plain,
! [X0: $i,X1: $i,X2: $i] : inverse(multiply(iPr_def_11(X0,X1),iPr_def_10(iPr_def_11(X0,X2)))) = iPr_def_13(X1,X2),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_13])],[c_1725]) ).
tcf(c_1942,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_11(iPr_def_11(X0,iPr_def_13(iPr_def_10(X1),iPr_def_10(X1))),iPr_def_10(X2)) = multiply(X2,X0),
inference(demodulation,[status(thm)],[c_1889,c_1940]) ).
tcf(c_1947,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_10(iPr_def_11(multiply(X0,X1),multiply(X0,X1))) = multiply(inverse(X2),X2),
inference(demodulation,[status(thm)],[c_1788,c_68,c_161,c_471]) ).
tcf(c_1948,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_10(iPr_def_11(multiply(X0,X1),multiply(X0,X1))) = multiply(X2,iPr_def_10(X2)),
inference(demodulation,[status(thm)],[c_1787,c_161,c_739]) ).
tcf(c_1961,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_10(iPr_def_11(multiply(X0,X1),multiply(X0,X1))) = iPr_def_10(iPr_def_11(X2,X2)),
inference(demodulation,[status(thm)],[c_1789,c_68,c_161,c_200,c_740]) ).
tcf(c_2030,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] : multiply(inverse(multiply(iPr_def_11(X0,X1),iPr_def_10(iPr_def_11(X0,X2)))),X3) = multiply(iPr_def_11(multiply(X4,X1),multiply(X4,X2)),X3),
inference(demodulation,[status(thm)],[c_1708,c_200,c_740,c_754]) ).
tcf(c_2031,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : multiply(iPr_def_11(multiply(X0,X1),multiply(X0,X2)),X3) = iPr_def_14(X1,X2,X3),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_14])],[c_2030]) ).
tcf(c_2032,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : multiply(inverse(multiply(iPr_def_11(X0,X1),iPr_def_10(iPr_def_11(X0,X2)))),X3) = iPr_def_14(X1,X2,X3),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_2030]) ).
tcf(c_2033,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(iPr_def_13(X0,X1),X2) = iPr_def_14(X0,X1,X2),
inference(demodulation,[status(thm)],[c_2032,c_1940]) ).
tcf(c_2045,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_11(multiply(X0,X1),multiply(X0,X2)) = iPr_def_13(X1,X2),
inference(demodulation,[status(thm)],[c_478,c_1940]) ).
tcf(c_2047,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(iPr_def_13(X0,X0),multiply(X1,X2)) = iPr_def_10(iPr_def_11(iPr_def_10(X1),X2)),
inference(demodulation,[status(thm)],[c_774,c_2045]) ).
tcf(c_2048,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_14(X0,X0,multiply(X1,X2)) = iPr_def_10(iPr_def_11(iPr_def_10(X1),X2)),
inference(demodulation,[status(thm)],[c_2047,c_2033]) ).
tcf(c_3426,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_11(iPr_def_10(inverse(multiply(inverse(inverse(multiply(X0,iPr_def_10(X0)))),inverse(multiply(inverse(inverse(multiply(X0,iPr_def_10(X0)))),inverse(multiply(X0,iPr_def_10(X0)))))))),iPr_def_10(X0)) = multiply(X0,inverse(iPr_def_10(iPr_def_11(multiply(X1,X2),multiply(X1,X2))))),
inference(superposition,[status(thm)],[c_1947,c_166]) ).
tcf(c_3432,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : iPr_def_11(iPr_def_11(X0,inverse(iPr_def_10(iPr_def_11(multiply(X1,X2),multiply(X1,X2))))),X3) = multiply(inverse(X3),X0),
inference(superposition,[status(thm)],[c_1947,c_471]) ).
tcf(c_3439,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_11(inverse(iPr_def_10(iPr_def_11(multiply(X0,X1),multiply(X0,X1)))),X2) = iPr_def_10(inverse(multiply(inverse(X2),inverse(multiply(inverse(X2),X2))))),
inference(superposition,[status(thm)],[c_1947,c_175]) ).
tcf(c_3478,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_11(multiply(X0,X1),multiply(X0,X1)) = inverse(multiply(X2,iPr_def_10(X2))),
inference(superposition,[status(thm)],[c_1948,c_161]) ).
tcf(c_3482,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),X0) = multiply(X1,iPr_def_10(X1)),
inference(superposition,[status(thm)],[c_1948,c_1947]) ).
tcf(c_3553,plain,
! [X0: $i,X1: $i,X2: $i] : inverse(iPr_def_10(iPr_def_11(multiply(X0,X1),multiply(X0,X1)))) = iPr_def_11(X2,X2),
inference(superposition,[status(thm)],[c_1961,c_161]) ).
tcf(c_3572,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_11(iPr_def_11(X0,iPr_def_13(iPr_def_10(X1),iPr_def_10(X1))),X2) = multiply(inverse(X2),X0),
inference(superposition,[status(thm)],[c_68,c_1942]) ).
tcf(c_3576,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] : iPr_def_11(iPr_def_11(X0,iPr_def_13(iPr_def_10(X1),iPr_def_10(X1))),multiply(inverse(X2),X2)) = multiply(iPr_def_11(multiply(X3,X4),multiply(X3,X4)),X0),
inference(superposition,[status(thm)],[c_1947,c_1942]) ).
tcf(c_3583,plain,
! [X0: $i] : multiply(inverse(X0),X0) = iPr_def_16,
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_16])],[c_3482]) ).
tcf(c_3584,plain,
! [X0: $i] : multiply(X0,iPr_def_10(X0)) = iPr_def_16,
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_3482]) ).
tcf(c_3587,plain,
! [X0: $i,X1: $i] : iPr_def_11(X0,X0) = iPr_def_13(X1,X1),
inference(demodulation,[status(thm)],[c_3553,c_161,c_2045]) ).
tcf(c_3590,plain,
! [X0: $i,X1: $i] : iPr_def_11(multiply(X0,X1),multiply(X0,X1)) = inverse(iPr_def_16),
inference(demodulation,[status(thm)],[c_3478,c_3584]) ).
tcf(c_3591,plain,
! [X0: $i] : iPr_def_13(X0,X0) = inverse(iPr_def_16),
inference(demodulation,[status(thm)],[c_3590,c_2045]) ).
tcf(c_3594,plain,
! [X0: $i,X1: $i] : iPr_def_11(iPr_def_11(X0,inverse(iPr_def_16)),X1) = multiply(inverse(X1),X0),
inference(demodulation,[status(thm)],[c_3572,c_3591]) ).
tcf(c_3617,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_11(iPr_def_11(X0,iPr_def_13(X1,X1)),X2) = multiply(inverse(X2),X0),
inference(demodulation,[status(thm)],[c_3432,c_161,c_2045]) ).
tcf(c_3651,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(iPr_def_11(multiply(X0,X1),multiply(X0,X1)),X2) = multiply(inverse(iPr_def_16),X2),
inference(demodulation,[status(thm)],[c_3576,c_3583,c_3617]) ).
tcf(c_3652,plain,
! [X0: $i,X1: $i] : iPr_def_14(X0,X0,X1) = multiply(inverse(iPr_def_16),X1),
inference(demodulation,[status(thm)],[c_3651,c_2031]) ).
tcf(c_3659,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_11(inverse(iPr_def_10(iPr_def_11(multiply(X0,X1),multiply(X0,X1)))),X2) = iPr_def_10(inverse(multiply(inverse(X2),inverse(iPr_def_16)))),
inference(demodulation,[status(thm)],[c_3439,c_3583]) ).
tcf(c_3660,plain,
! [X0: $i,X1: $i] : iPr_def_11(iPr_def_13(X0,X0),X1) = multiply(inverse(X1),inverse(iPr_def_16)),
inference(demodulation,[status(thm)],[c_3659,c_68,c_161,c_2045]) ).
tcf(c_3733,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(X0,inverse(iPr_def_10(iPr_def_11(multiply(X1,X2),multiply(X1,X2))))) = iPr_def_11(iPr_def_10(inverse(iPr_def_16)),iPr_def_10(X0)),
inference(demodulation,[status(thm)],[c_3426,c_3583,c_3584]) ).
tcf(c_3734,plain,
! [X0: $i,X1: $i] : multiply(X0,iPr_def_13(X1,X1)) = iPr_def_11(iPr_def_16,iPr_def_10(X0)),
inference(demodulation,[status(thm)],[c_3733,c_68,c_161,c_2045]) ).
tcf(c_3892,plain,
! [X0: $i,X1: $i] : multiply(inverse(iPr_def_11(X0,iPr_def_16)),multiply(inverse(iPr_def_16),iPr_def_11(X1,X1))) = iPr_def_10(X0),
inference(superposition,[status(thm)],[c_3583,c_746]) ).
tcf(c_3893,plain,
! [X0: $i,X1: $i] : iPr_def_11(inverse(multiply(X0,multiply(inverse(iPr_def_16),iPr_def_11(X1,X1)))),iPr_def_16) = iPr_def_10(X0),
inference(superposition,[status(thm)],[c_3583,c_188]) ).
tcf(c_3894,plain,
! [X0: $i,X1: $i] : iPr_def_10(inverse(multiply(inverse(multiply(X0,X1)),iPr_def_11(X1,X1)))) = iPr_def_11(inverse(iPr_def_16),multiply(X0,X1)),
inference(superposition,[status(thm)],[c_3583,c_188]) ).
tcf(c_3895,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_10(iPr_def_11(multiply(X0,X1),multiply(X0,X2))) = multiply(iPr_def_11(X2,X1),iPr_def_16),
inference(superposition,[status(thm)],[c_3583,c_485]) ).
tcf(c_3899,plain,
! [X0: $i,X1: $i] : iPr_def_11(multiply(X0,X1),iPr_def_16) = iPr_def_13(X1,iPr_def_10(X0)),
inference(superposition,[status(thm)],[c_3584,c_2045]) ).
tcf(c_3900,plain,
! [X0: $i,X1: $i] : multiply(inverse(multiply(X0,X1)),iPr_def_16) = iPr_def_10(iPr_def_11(X1,iPr_def_10(X0))),
inference(superposition,[status(thm)],[c_3584,c_200]) ).
tcf(c_3903,plain,
! [X0: $i,X1: $i] : iPr_def_11(iPr_def_16,multiply(X0,X1)) = iPr_def_13(iPr_def_10(X0),X1),
inference(superposition,[status(thm)],[c_3584,c_2045]) ).
tcf(c_3928,plain,
! [X0: $i] : iPr_def_11(X0,X0) = inverse(iPr_def_16),
inference(superposition,[status(thm)],[c_3587,c_3591]) ).
tcf(c_4088,plain,
! [X0: $i,X1: $i] : multiply(inverse(iPr_def_16),multiply(X0,X1)) = iPr_def_10(iPr_def_11(iPr_def_10(X0),X1)),
inference(superposition,[status(thm)],[c_3652,c_2048]) ).
tcf(c_4144,plain,
! [X0: $i] : multiply(X0,inverse(iPr_def_16)) = iPr_def_11(iPr_def_16,iPr_def_10(X0)),
inference(superposition,[status(thm)],[c_3591,c_3734]) ).
tcf(c_4148,plain,
! [X0: $i] : iPr_def_11(iPr_def_16,iPr_def_10(inverse(iPr_def_13(X0,X0)))) = iPr_def_16,
inference(superposition,[status(thm)],[c_3734,c_3583]) ).
tcf(c_4165,plain,
iPr_def_11(iPr_def_16,inverse(iPr_def_16)) = iPr_def_16,
inference(demodulation,[status(thm)],[c_4148,c_68,c_3591]) ).
tcf(c_4223,plain,
! [X0: $i,X1: $i] : multiply(iPr_def_11(X0,X1),iPr_def_16) = iPr_def_10(iPr_def_13(X1,X0)),
inference(demodulation,[status(thm)],[c_3895,c_2045]) ).
tcf(c_4224,plain,
! [X0: $i] : iPr_def_11(inverse(multiply(X0,iPr_def_11(iPr_def_16,iPr_def_10(inverse(iPr_def_16))))),iPr_def_16) = iPr_def_10(X0),
inference(demodulation,[status(thm)],[c_3893,c_3928,c_4144]) ).
tcf(c_4225,plain,
! [X0: $i] : iPr_def_11(inverse(multiply(X0,iPr_def_11(iPr_def_16,iPr_def_16))),iPr_def_16) = iPr_def_10(X0),
inference(demodulation,[status(thm)],[c_4224,c_68]) ).
tcf(c_4226,plain,
! [X0: $i] : multiply(inverse(iPr_def_11(X0,iPr_def_16)),iPr_def_11(iPr_def_16,iPr_def_10(inverse(iPr_def_16)))) = iPr_def_10(X0),
inference(demodulation,[status(thm)],[c_3892,c_3928,c_4144]) ).
tcf(c_4227,plain,
! [X0: $i] : multiply(inverse(iPr_def_11(X0,iPr_def_16)),iPr_def_11(iPr_def_16,iPr_def_16)) = iPr_def_10(X0),
inference(demodulation,[status(thm)],[c_4226,c_68]) ).
tcf(c_4241,plain,
! [X0: $i,X1: $i] : iPr_def_10(inverse(iPr_def_11(iPr_def_16,iPr_def_10(inverse(multiply(X0,X1)))))) = iPr_def_11(inverse(iPr_def_16),multiply(X0,X1)),
inference(demodulation,[status(thm)],[c_3894,c_3928,c_4144]) ).
tcf(c_4242,plain,
! [X0: $i,X1: $i] : iPr_def_11(inverse(iPr_def_16),multiply(X0,X1)) = iPr_def_11(iPr_def_16,multiply(X0,X1)),
inference(demodulation,[status(thm)],[c_4241,c_68]) ).
tcf(c_4429,plain,
! [X0: $i,X1: $i] : iPr_def_11(iPr_def_16,iPr_def_14(X0,X0,X1)) = iPr_def_13(iPr_def_10(inverse(iPr_def_16)),X1),
inference(superposition,[status(thm)],[c_3652,c_3903]) ).
tcf(c_4450,plain,
! [X0: $i] : multiply(inverse(X0),iPr_def_16) = iPr_def_11(iPr_def_16,X0),
inference(superposition,[status(thm)],[c_4165,c_3594]) ).
tcf(c_4454,plain,
! [X0: $i] : multiply(inverse(iPr_def_11(X0,inverse(iPr_def_16))),X0) = inverse(iPr_def_16),
inference(superposition,[status(thm)],[c_3594,c_3928]) ).
tcf(c_4470,plain,
! [X0: $i] : iPr_def_11(iPr_def_13(X0,X0),inverse(iPr_def_16)) = iPr_def_16,
inference(superposition,[status(thm)],[c_3660,c_3583]) ).
tcf(c_4499,plain,
! [X0: $i] : multiply(inverse(multiply(inverse(iPr_def_16),X0)),iPr_def_11(iPr_def_16,iPr_def_16)) = iPr_def_10(iPr_def_11(X0,inverse(iPr_def_16))),
inference(superposition,[status(thm)],[c_3594,c_4227]) ).
tcf(c_4503,plain,
! [X0: $i] : multiply(inverse(iPr_def_11(X0,iPr_def_16)),inverse(iPr_def_16)) = iPr_def_10(X0),
inference(superposition,[status(thm)],[c_3928,c_4227]) ).
tcf(c_4508,plain,
! [X0: $i] : iPr_def_13(iPr_def_10(inverse(iPr_def_11(X0,iPr_def_16))),iPr_def_11(iPr_def_16,iPr_def_16)) = iPr_def_11(iPr_def_16,iPr_def_10(X0)),
inference(superposition,[status(thm)],[c_4227,c_3903]) ).
tcf(c_4509,plain,
! [X0: $i] : iPr_def_13(iPr_def_11(iPr_def_16,iPr_def_16),iPr_def_10(inverse(iPr_def_11(X0,iPr_def_16)))) = iPr_def_11(iPr_def_10(X0),iPr_def_16),
inference(superposition,[status(thm)],[c_4227,c_3899]) ).
tcf(c_4544,plain,
! [X0: $i,X1: $i] : multiply(inverse(iPr_def_14(X0,X0,X1)),iPr_def_16) = iPr_def_10(iPr_def_11(X1,iPr_def_10(inverse(iPr_def_16)))),
inference(superposition,[status(thm)],[c_3652,c_3900]) ).
tcf(c_4571,plain,
! [X0: $i,X1: $i] : multiply(inverse(iPr_def_16),iPr_def_11(iPr_def_13(X0,X0),X1)) = iPr_def_10(iPr_def_11(iPr_def_10(inverse(X1)),inverse(iPr_def_16))),
inference(superposition,[status(thm)],[c_3660,c_4088]) ).
tcf(c_4634,plain,
inverse(iPr_def_16) = iPr_def_16,
inference(demodulation,[status(thm)],[c_4470,c_3591,c_3928]) ).
tcf(c_4637,plain,
! [X0: $i] : iPr_def_11(iPr_def_16,iPr_def_11(X0,iPr_def_16)) = iPr_def_10(X0),
inference(demodulation,[status(thm)],[c_4503,c_68,c_4144]) ).
tcf(c_4655,plain,
! [X0: $i,X1: $i] : iPr_def_11(iPr_def_16,iPr_def_14(X0,X0,X1)) = iPr_def_13(iPr_def_16,X1),
inference(demodulation,[status(thm)],[c_4429,c_68]) ).
tcf(c_4664,plain,
! [X0: $i] : iPr_def_10(iPr_def_11(X0,iPr_def_10(inverse(iPr_def_16)))) = iPr_def_13(iPr_def_16,X0),
inference(demodulation,[status(thm)],[c_4544,c_4450,c_4655]) ).
tcf(c_4665,plain,
! [X0: $i] : iPr_def_10(iPr_def_11(X0,iPr_def_16)) = iPr_def_13(iPr_def_16,X0),
inference(demodulation,[status(thm)],[c_4664,c_68]) ).
tcf(c_4667,plain,
! [X0: $i] : iPr_def_13(inverse(iPr_def_16),iPr_def_11(X0,iPr_def_16)) = iPr_def_11(iPr_def_10(X0),iPr_def_16),
inference(demodulation,[status(thm)],[c_4509,c_68,c_3928]) ).
tcf(c_4668,plain,
! [X0: $i] : iPr_def_13(iPr_def_11(X0,iPr_def_16),inverse(iPr_def_16)) = iPr_def_11(iPr_def_16,iPr_def_10(X0)),
inference(demodulation,[status(thm)],[c_4508,c_68,c_3928]) ).
tcf(c_4698,plain,
! [X0: $i] : iPr_def_10(iPr_def_11(X0,inverse(iPr_def_16))) = iPr_def_13(iPr_def_16,X0),
inference(demodulation,[status(thm)],[c_4499,c_68,c_3903,c_3928,c_4144]) ).
tcf(c_4710,plain,
! [X0: $i,X1: $i] : multiply(inverse(iPr_def_16),iPr_def_11(iPr_def_13(X0,X0),X1)) = iPr_def_13(iPr_def_16,iPr_def_10(inverse(X1))),
inference(demodulation,[status(thm)],[c_4571,c_4698]) ).
tcf(c_4711,plain,
! [X0: $i] : multiply(inverse(iPr_def_16),iPr_def_11(inverse(iPr_def_16),X0)) = iPr_def_13(iPr_def_16,X0),
inference(demodulation,[status(thm)],[c_4710,c_68,c_3591]) ).
tcf(c_4792,plain,
! [X0: $i,X1: $i] : iPr_def_10(iPr_def_11(X0,iPr_def_10(X1))) = iPr_def_11(iPr_def_16,multiply(X1,X0)),
inference(demodulation,[status(thm)],[c_3900,c_4450]) ).
tcf(c_4793,plain,
! [X0: $i,X1: $i] : iPr_def_10(iPr_def_11(X0,iPr_def_10(X1))) = iPr_def_13(iPr_def_10(X1),X0),
inference(demodulation,[status(thm)],[c_4792,c_3903]) ).
tcf(c_4799,plain,
! [X0: $i,X1: $i] : iPr_def_11(iPr_def_11(X0,iPr_def_16),X1) = multiply(inverse(X1),X0),
inference(demodulation,[status(thm)],[c_3594,c_4634]) ).
tcf(c_4803,plain,
! [X0: $i] : iPr_def_11(X0,X0) = iPr_def_16,
inference(demodulation,[status(thm)],[c_3928,c_4634]) ).
tcf(c_4805,plain,
! [X0: $i] : iPr_def_13(X0,X0) = iPr_def_16,
inference(demodulation,[status(thm)],[c_3591,c_4634]) ).
tcf(c_4806,plain,
! [X0: $i] : iPr_def_11(iPr_def_16,iPr_def_10(X0)) = multiply(X0,iPr_def_16),
inference(demodulation,[status(thm)],[c_3734,c_4805]) ).
tcf(c_4813,plain,
! [X0: $i] : iPr_def_11(inverse(multiply(X0,iPr_def_16)),iPr_def_16) = iPr_def_10(X0),
inference(demodulation,[status(thm)],[c_4225,c_4803]) ).
tcf(c_7223,plain,
! [X0: $i,X1: $i] : iPr_def_11(inverse(iPr_def_10(iPr_def_13(X0,X1))),iPr_def_16) = iPr_def_10(iPr_def_11(X1,X0)),
inference(superposition,[status(thm)],[c_4223,c_4813]) ).
tcf(c_7225,plain,
! [X0: $i] : iPr_def_11(inverse(iPr_def_11(iPr_def_16,X0)),iPr_def_16) = iPr_def_10(inverse(X0)),
inference(superposition,[status(thm)],[c_4450,c_4813]) ).
tcf(c_7235,plain,
! [X0: $i,X1: $i] : iPr_def_11(multiply(inverse(iPr_def_11(X0,inverse(iPr_def_16))),X1),inverse(iPr_def_16)) = iPr_def_13(X1,X0),
inference(superposition,[status(thm)],[c_4454,c_2045]) ).
tcf(c_7240,plain,
! [X0: $i,X1: $i] : iPr_def_11(inverse(iPr_def_16),multiply(inverse(iPr_def_11(X0,inverse(iPr_def_16))),X1)) = iPr_def_13(X0,X1),
inference(superposition,[status(thm)],[c_4454,c_2045]) ).
tcf(c_7250,plain,
! [X0: $i,X1: $i] : iPr_def_10(iPr_def_11(X0,X1)) = iPr_def_13(X1,X0),
inference(superposition,[status(thm)],[c_68,c_4793]) ).
tcf(c_7259,plain,
! [X0: $i,X1: $i] : inverse(iPr_def_13(iPr_def_10(X0),X1)) = iPr_def_11(X1,iPr_def_10(X0)),
inference(superposition,[status(thm)],[c_4793,c_161]) ).
tcf(c_7275,plain,
! [X0: $i] : iPr_def_10(multiply(inverse(iPr_def_16),X0)) = iPr_def_13(iPr_def_16,iPr_def_11(X0,iPr_def_16)),
inference(superposition,[status(thm)],[c_4799,c_4665]) ).
tcf(c_7287,plain,
! [X0: $i] : iPr_def_13(iPr_def_16,iPr_def_11(X0,iPr_def_16)) = iPr_def_11(iPr_def_10(X0),iPr_def_16),
inference(superposition,[status(thm)],[c_4634,c_4667]) ).
tcf(c_7343,plain,
! [X0: $i] : iPr_def_13(iPr_def_11(inverse(iPr_def_16),X0),iPr_def_10(inverse(iPr_def_16))) = iPr_def_11(iPr_def_13(iPr_def_16,X0),iPr_def_16),
inference(superposition,[status(thm)],[c_4711,c_3899]) ).
tcf(c_7511,plain,
! [X0: $i] : iPr_def_11(inverse(iPr_def_11(iPr_def_16,X0)),iPr_def_16) = X0,
inference(demodulation,[status(thm)],[c_7225,c_68]) ).
tcf(c_7524,plain,
! [X0: $i] : iPr_def_10(multiply(inverse(iPr_def_16),X0)) = iPr_def_11(iPr_def_10(X0),iPr_def_16),
inference(demodulation,[status(thm)],[c_7275,c_7287]) ).
tcf(c_7525,plain,
! [X0: $i] : iPr_def_10(multiply(iPr_def_16,X0)) = iPr_def_11(iPr_def_10(X0),iPr_def_16),
inference(light_normalisation,[status(thm)],[c_7524,c_4634]) ).
tcf(c_7553,plain,
! [X0: $i,X1: $i] : iPr_def_11(inverse(iPr_def_10(iPr_def_13(X0,X1))),iPr_def_16) = iPr_def_13(X0,X1),
inference(demodulation,[status(thm)],[c_7223,c_7250]) ).
tcf(c_7554,plain,
! [X0: $i,X1: $i] : iPr_def_11(iPr_def_13(X0,X1),iPr_def_16) = iPr_def_13(X0,X1),
inference(demodulation,[status(thm)],[c_7553,c_161]) ).
tcf(c_7596,plain,
! [X0: $i] : iPr_def_13(iPr_def_11(inverse(iPr_def_16),X0),iPr_def_10(inverse(iPr_def_16))) = iPr_def_13(iPr_def_16,X0),
inference(demodulation,[status(thm)],[c_7343,c_7554]) ).
tcf(c_7597,plain,
! [X0: $i] : iPr_def_13(iPr_def_11(inverse(iPr_def_16),X0),iPr_def_16) = iPr_def_13(iPr_def_16,X0),
inference(demodulation,[status(thm)],[c_7596,c_68]) ).
tcf(c_7598,plain,
! [X0: $i] : iPr_def_13(iPr_def_11(iPr_def_16,X0),iPr_def_16) = iPr_def_13(iPr_def_16,X0),
inference(light_normalisation,[status(thm)],[c_7597,c_4634]) ).
tcf(c_7636,plain,
! [X0: $i,X1: $i] : iPr_def_13(iPr_def_11(X0,inverse(iPr_def_16)),X1) = iPr_def_13(X0,X1),
inference(demodulation,[status(thm)],[c_7240,c_68,c_3903,c_4242]) ).
tcf(c_7637,plain,
! [X0: $i,X1: $i] : iPr_def_13(iPr_def_11(X0,iPr_def_16),X1) = iPr_def_13(X0,X1),
inference(light_normalisation,[status(thm)],[c_7636,c_4634]) ).
tcf(c_7638,plain,
! [X0: $i,X1: $i] : iPr_def_11(multiply(inverse(iPr_def_11(X0,iPr_def_16)),X1),iPr_def_16) = iPr_def_13(X1,X0),
inference(light_normalisation,[status(thm)],[c_7235,c_4634]) ).
tcf(c_7639,plain,
! [X0: $i,X1: $i] : iPr_def_13(X0,iPr_def_11(X1,iPr_def_16)) = iPr_def_13(X0,X1),
inference(demodulation,[status(thm)],[c_7638,c_68,c_3899]) ).
tcf(c_7958,plain,
! [X0: $i] : iPr_def_13(inverse(iPr_def_16),iPr_def_11(X0,iPr_def_16)) = iPr_def_10(multiply(iPr_def_16,X0)),
inference(demodulation,[status(thm)],[c_4667,c_7525]) ).
tcf(c_7959,plain,
! [X0: $i] : iPr_def_10(multiply(iPr_def_16,X0)) = iPr_def_13(inverse(iPr_def_16),X0),
inference(demodulation,[status(thm)],[c_7958,c_7639]) ).
tcf(c_7960,plain,
! [X0: $i] : iPr_def_10(multiply(iPr_def_16,X0)) = iPr_def_13(iPr_def_16,X0),
inference(light_normalisation,[status(thm)],[c_7959,c_4634]) ).
tcf(c_7964,plain,
! [X0: $i] : iPr_def_11(iPr_def_16,iPr_def_10(X0)) = iPr_def_13(X0,inverse(iPr_def_16)),
inference(demodulation,[status(thm)],[c_4668,c_7637]) ).
tcf(c_7965,plain,
! [X0: $i] : iPr_def_13(X0,inverse(iPr_def_16)) = multiply(X0,iPr_def_16),
inference(demodulation,[status(thm)],[c_7964,c_4806]) ).
tcf(c_7966,plain,
! [X0: $i] : multiply(X0,iPr_def_16) = iPr_def_13(X0,iPr_def_16),
inference(light_normalisation,[status(thm)],[c_7965,c_4634]) ).
tcf(c_7968,plain,
! [X0: $i] : iPr_def_11(inverse(iPr_def_13(X0,iPr_def_16)),iPr_def_16) = iPr_def_10(X0),
inference(demodulation,[status(thm)],[c_4813,c_7966]) ).
tcf(c_7971,plain,
! [X0: $i] : iPr_def_13(inverse(X0),iPr_def_16) = iPr_def_11(iPr_def_16,X0),
inference(demodulation,[status(thm)],[c_4450,c_7966]) ).
tcf(c_8141,plain,
! [X0: $i,X1: $i] : iPr_def_11(multiply(X0,X1),iPr_def_13(X0,iPr_def_16)) = iPr_def_13(X1,iPr_def_16),
inference(superposition,[status(thm)],[c_7966,c_2045]) ).
tcf(c_8159,plain,
! [X0: $i] : iPr_def_13(iPr_def_11(X0,iPr_def_16),iPr_def_16) = iPr_def_10(iPr_def_10(X0)),
inference(superposition,[status(thm)],[c_4637,c_7250]) ).
tcf(c_8194,plain,
! [X0: $i] : iPr_def_13(iPr_def_16,inverse(iPr_def_11(iPr_def_16,X0))) = iPr_def_10(X0),
inference(superposition,[status(thm)],[c_7511,c_7250]) ).
tcf(c_8196,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),inverse(iPr_def_11(iPr_def_16,X1))) = iPr_def_11(X1,X0),
inference(superposition,[status(thm)],[c_7511,c_4799]) ).
tcf(c_8201,plain,
! [X0: $i] : inverse(iPr_def_13(iPr_def_16,X0)) = multiply(iPr_def_16,X0),
inference(superposition,[status(thm)],[c_7960,c_161]) ).
tcf(c_8273,plain,
! [X0: $i] : iPr_def_10(multiply(iPr_def_16,inverse(X0))) = iPr_def_11(X0,iPr_def_16),
inference(superposition,[status(thm)],[c_68,c_7525]) ).
tcf(c_8294,plain,
! [X0: $i] : iPr_def_11(iPr_def_11(iPr_def_16,X0),iPr_def_16) = iPr_def_11(iPr_def_16,X0),
inference(superposition,[status(thm)],[c_7971,c_7554]) ).
tcf(c_8341,plain,
! [X0: $i] : iPr_def_11(inverse(iPr_def_13(iPr_def_16,X0)),iPr_def_16) = iPr_def_10(iPr_def_11(iPr_def_16,X0)),
inference(superposition,[status(thm)],[c_7598,c_7968]) ).
tcf(c_8377,plain,
! [X0: $i,X1: $i] : iPr_def_11(iPr_def_11(X0,iPr_def_16),iPr_def_10(X1)) = inverse(iPr_def_13(iPr_def_10(X1),X0)),
inference(superposition,[status(thm)],[c_7639,c_7259]) ).
tcf(c_8378,plain,
! [X0: $i,X1: $i] : inverse(iPr_def_13(X0,X1)) = iPr_def_11(X1,X0),
inference(superposition,[status(thm)],[c_68,c_7259]) ).
tcf(c_8410,plain,
! [X0: $i] : multiply(iPr_def_16,X0) = iPr_def_11(X0,iPr_def_16),
inference(demodulation,[status(thm)],[c_8201,c_8378]) ).
tcf(c_8420,plain,
! [X0: $i] : iPr_def_10(iPr_def_11(inverse(X0),iPr_def_16)) = iPr_def_11(X0,iPr_def_16),
inference(demodulation,[status(thm)],[c_8273,c_8410]) ).
tcf(c_8421,plain,
! [X0: $i] : iPr_def_13(iPr_def_16,inverse(X0)) = iPr_def_11(X0,iPr_def_16),
inference(demodulation,[status(thm)],[c_8420,c_7250]) ).
tcf(c_8425,plain,
! [X0: $i] : iPr_def_11(iPr_def_16,X0) = iPr_def_10(X0),
inference(demodulation,[status(thm)],[c_8194,c_8294,c_8421]) ).
tcf(c_8437,plain,
! [X0: $i] : iPr_def_10(iPr_def_10(X0)) = iPr_def_13(X0,iPr_def_16),
inference(demodulation,[status(thm)],[c_8159,c_7637]) ).
tcf(c_8489,plain,
! [X0: $i] : iPr_def_11(iPr_def_11(X0,iPr_def_16),iPr_def_16) = iPr_def_10(iPr_def_10(X0)),
inference(demodulation,[status(thm)],[c_8341,c_8378,c_8425]) ).
tcf(c_8490,plain,
! [X0: $i] : multiply(inverse(iPr_def_16),X0) = iPr_def_10(iPr_def_10(X0)),
inference(demodulation,[status(thm)],[c_8489,c_4799]) ).
tcf(c_8491,plain,
! [X0: $i] : multiply(iPr_def_16,X0) = iPr_def_10(iPr_def_10(X0)),
inference(light_normalisation,[status(thm)],[c_8490,c_4634]) ).
tcf(c_8507,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),inverse(iPr_def_10(X1))) = iPr_def_11(X1,X0),
inference(demodulation,[status(thm)],[c_8196,c_8425]) ).
tcf(c_8508,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),X1) = iPr_def_11(X1,X0),
inference(demodulation,[status(thm)],[c_8507,c_161]) ).
tcf(c_8523,plain,
! [X0: $i,X1: $i] : iPr_def_11(multiply(X0,X1),iPr_def_10(iPr_def_10(X0))) = iPr_def_10(iPr_def_10(X1)),
inference(demodulation,[status(thm)],[c_8141,c_8437]) ).
tcf(c_8525,plain,
! [X0: $i,X1: $i] : iPr_def_11(iPr_def_11(X0,iPr_def_16),iPr_def_10(X1)) = iPr_def_11(X0,iPr_def_10(X1)),
inference(demodulation,[status(thm)],[c_8377,c_8378]) ).
tcf(c_8526,plain,
! [X0: $i,X1: $i] : iPr_def_11(X0,iPr_def_10(X1)) = multiply(X1,X0),
inference(demodulation,[status(thm)],[c_8525,c_161,c_4799]) ).
tcf(c_8619,plain,
! [X0: $i] : iPr_def_11(inverse(iPr_def_10(X0)),iPr_def_16) = X0,
inference(demodulation,[status(thm)],[c_7511,c_8425]) ).
tcf(c_8624,plain,
! [X0: $i] : iPr_def_11(X0,iPr_def_16) = X0,
inference(demodulation,[status(thm)],[c_8619,c_161]) ).
tcf(c_8731,plain,
! [X0: $i] : iPr_def_10(iPr_def_10(X0)) = iPr_def_11(X0,iPr_def_16),
inference(demodulation,[status(thm)],[c_8410,c_8491]) ).
tcf(c_8734,plain,
! [X0: $i] : iPr_def_10(iPr_def_10(X0)) = X0,
inference(demodulation,[status(thm)],[c_8731,c_8624]) ).
tcf(c_8740,plain,
! [X0: $i] : multiply(iPr_def_16,X0) = X0,
inference(demodulation,[status(thm)],[c_8491,c_8734]) ).
tcf(c_8758,plain,
! [X0: $i] : inverse(X0) = iPr_def_10(X0),
inference(superposition,[status(thm)],[c_8734,c_161]) ).
tcf(c_8763,plain,
! [X0: $i,X1: $i] : iPr_def_11(X0,multiply(iPr_def_16,X1)) = iPr_def_13(X0,X1),
inference(superposition,[status(thm)],[c_8740,c_2045]) ).
tcf(c_8826,plain,
! [X0: $i,X1: $i] : iPr_def_11(X0,X1) = iPr_def_13(X0,X1),
inference(demodulation,[status(thm)],[c_8763,c_8740]) ).
tcf(c_8962,plain,
! [X0: $i,X1: $i] : multiply(iPr_def_10(X0),X1) = iPr_def_11(X1,X0),
inference(demodulation,[status(thm)],[c_8508,c_8758]) ).
tcf(c_8970,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_11(multiply(X0,X1),multiply(X0,X2)) = iPr_def_11(X1,X2),
inference(demodulation,[status(thm)],[c_2045,c_8826]) ).
tcf(c_8971,plain,
! [X0: $i,X1: $i] : iPr_def_10(iPr_def_11(X0,X1)) = iPr_def_11(X1,X0),
inference(demodulation,[status(thm)],[c_7250,c_8826]) ).
tcf(c_8972,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(iPr_def_11(X0,X1),X2) = iPr_def_14(X0,X1,X2),
inference(demodulation,[status(thm)],[c_2033,c_8826]) ).
tcf(c_9043,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(iPr_def_11(X0,X1),X2) = iPr_def_11(X2,iPr_def_11(X1,X0)),
inference(superposition,[status(thm)],[c_8971,c_8526]) ).
tcf(c_9127,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(multiply(X0,X1),X2) = iPr_def_14(X1,iPr_def_10(X0),X2),
inference(superposition,[status(thm)],[c_8526,c_8972]) ).
tcf(c_9162,plain,
! [X0: $i,X1: $i] : iPr_def_11(multiply(X0,X1),X0) = iPr_def_10(iPr_def_10(X1)),
inference(superposition,[status(thm)],[c_8734,c_8523]) ).
tcf(c_9192,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_11(multiply(iPr_def_10(X0),X1),iPr_def_11(X2,X0)) = iPr_def_11(X1,X2),
inference(superposition,[status(thm)],[c_8962,c_8970]) ).
tcf(c_9324,plain,
! [X0: $i,X1: $i] : iPr_def_11(multiply(X0,X1),X0) = X1,
inference(demodulation,[status(thm)],[c_9162,c_8734]) ).
tcf(c_9362,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_11(X0,iPr_def_11(X1,X2)) = iPr_def_14(X2,X1,X0),
inference(demodulation,[status(thm)],[c_9043,c_8972]) ).
tcf(c_9371,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_14(X0,X1,multiply(iPr_def_10(X0),X2)) = iPr_def_11(X2,X1),
inference(demodulation,[status(thm)],[c_9192,c_9362]) ).
tcf(c_9372,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_14(X0,X1,iPr_def_11(X2,X0)) = iPr_def_11(X2,X1),
inference(demodulation,[status(thm)],[c_9371,c_8962]) ).
tcf(c_9561,plain,
multiply(a3,multiply(b3,c3)) != iPr_def_14(b3,iPr_def_10(a3),c3),
inference(demodulation,[status(thm)],[c_52,c_9127]) ).
tcf(c_9780,plain,
! [X0: $i,X1: $i,X2: $i] : iPr_def_11(multiply(X0,X1),X2) = iPr_def_14(X0,X2,X1),
inference(superposition,[status(thm)],[c_9324,c_9372]) ).
tcf(c_10783,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(X0,multiply(X1,X2)) = iPr_def_14(X1,iPr_def_10(X0),X2),
inference(superposition,[status(thm)],[c_9780,c_8526]) ).
tcf(c_10927,plain,
$false,
inference(backward_subsumption_resolution,[status(thm)],[c_9561,c_10783]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP423-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.11/0.38 % Computer : n005.cluster.edu
% 0.11/0.38 % Model : x86_64 x86_64
% 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.38 % Memory : 8046.5625MB
% 0.11/0.38 % OS : Linux 6.8.0-71-generic
% 0.11/0.38 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.38 % DateTime : Wed Sep 23 14:43:02 UTC 2026
% 0.11/0.39 % CPUTime :
% 0.11/0.39 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.11/0.42 Running UEQ theorem proving
% 0.11/0.43 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.44
% 0.11/0.44 % ======== iProver multi-core TPTP/SMT =========
% 0.11/0.44
% 0.11/0.44 % Detected problem language: tptp
% 0.11/0.45 % Proving...
% 11.92/2.33 WARNING - Clausifier option not provided in the heuristic config "heur/vip2_118404", setting default options.
% 11.92/2.33 % SZS status Started for theBenchmark.p
% 11.92/2.33 % SZS status Unsatisfiable for theBenchmark.p
% 11.92/2.33
% 11.92/2.33 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 11.92/2.33
% 11.92/2.33 % ------ iProver source info
% 11.92/2.33
% 11.92/2.33 % git: date: 2026-07-19 20:42:38 +0200
% 11.92/2.33 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 11.92/2.33 % git: non_committed_changes: false
% 11.92/2.33
% 11.92/2.33 % ------ Parsing...% successful
% 11.92/2.33
% 11.92/2.33
% 11.92/2.33 % ------ Clausification by vclausify_rel & Parsing by iProver...
% 11.92/2.33 % ------ Proving...
% 11.92/2.33 % ------ Problem Properties
% 11.92/2.33
% 11.92/2.33 %
% 11.92/2.33 % clauses 2
% 11.92/2.33 % conjectures 1
% 11.92/2.33 % EPR 0
% 11.92/2.33 % Horn 2
% 11.92/2.33 % unary 2
% 11.92/2.33 % binary 0
% 11.92/2.33 % lits 2
% 11.92/2.33 % lits eq 2
% 11.92/2.33 % fd_pure 0
% 11.92/2.33 % fd_pseudo 0
% 11.92/2.33 % fd_cond 0
% 11.92/2.33 % fd_pseudo_cond 0
% 11.92/2.33 % AC symbols 0
% 11.92/2.33
% 11.92/2.33 % ------ Input Options Time Limit: Unbounded
% 11.92/2.33
% 11.92/2.33
% 11.92/2.33 % ------
% 11.92/2.33 % Current options:
% 11.92/2.33 % ------
% 11.92/2.33
% 11.92/2.33
% 11.92/2.33 %
% 11.92/2.33
% 11.92/2.33 % ------ Proving...
% 11.92/2.33 %
% 11.92/2.33
% 11.92/2.33 % SZS status Unsatisfiable for theBenchmark.p
% 11.92/2.33
% 11.92/2.33 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 11.92/2.33
% 11.92/2.33
%------------------------------------------------------------------------------