%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : GRP422-1 : TPTP v9.3.1. Released v2.6.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% Computer : n026.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 01:33:52 PM UTC 2026
% Result : Unsatisfiable 2.57s 2.26s
% Output : CNFRefutation 2.57s
% Verified :
% SZS Type : Refutation
% Derivation depth : 36
% Number of leaves : 2
% Syntax : Number of formulae : 185 ( 185 unt; 0 def)
% Number of atoms : 849 ( 184 equ)
% Maximal formula atoms : 1 ( 4 avg)
% Number of connectives : 5 ( 5 ~; 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 : 4 ( 4 usr; 2 con; 0-2 aty)
% Number of variables : 435 ( 0 sgn 435 !; 0 ?; 432 :)
% 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(inverse(b2),b2),a2) != a2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_these_axioms_2) ).
fof(f3,plain,
a2 != multiply(multiply(inverse(b2),b2),a2),
inference(reorient_equations,[],[f2]) ).
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(inverse(b2),b2),a2) != a2,
inference(cnf_transformation,[],[f3]) ).
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_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_3427,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_3433,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_3440,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_3479,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_3483,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_3554,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_3573,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_3577,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_3584,plain,
! [X0: $i] : multiply(inverse(X0),X0) = iPr_def_16,
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_16])],[c_3483]) ).
tcf(c_3585,plain,
! [X0: $i] : multiply(X0,iPr_def_10(X0)) = iPr_def_16,
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_3483]) ).
tcf(c_3588,plain,
! [X0: $i,X1: $i] : iPr_def_11(X0,X0) = iPr_def_13(X1,X1),
inference(demodulation,[status(thm)],[c_3554,c_161,c_2045]) ).
tcf(c_3591,plain,
! [X0: $i,X1: $i] : iPr_def_11(multiply(X0,X1),multiply(X0,X1)) = inverse(iPr_def_16),
inference(demodulation,[status(thm)],[c_3479,c_3585]) ).
tcf(c_3592,plain,
! [X0: $i] : iPr_def_13(X0,X0) = inverse(iPr_def_16),
inference(demodulation,[status(thm)],[c_3591,c_2045]) ).
tcf(c_3595,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_3573,c_3592]) ).
tcf(c_3618,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_3433,c_161,c_2045]) ).
tcf(c_3652,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_3577,c_3584,c_3618]) ).
tcf(c_3653,plain,
! [X0: $i,X1: $i] : iPr_def_14(X0,X0,X1) = multiply(inverse(iPr_def_16),X1),
inference(demodulation,[status(thm)],[c_3652,c_2031]) ).
tcf(c_3660,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_3440,c_3584]) ).
tcf(c_3661,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_3660,c_68,c_161,c_2045]) ).
tcf(c_3734,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_3427,c_3584,c_3585]) ).
tcf(c_3735,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_3734,c_68,c_161,c_2045]) ).
tcf(c_3759,plain,
multiply(iPr_def_16,a2) != a2,
inference(demodulation,[status(thm)],[c_52,c_3584]) ).
tcf(c_3894,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_3584,c_746]) ).
tcf(c_3895,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_3584,c_188]) ).
tcf(c_3896,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_3584,c_188]) ).
tcf(c_3897,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_3584,c_485]) ).
tcf(c_3901,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_3585,c_2045]) ).
tcf(c_3902,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_3585,c_200]) ).
tcf(c_3905,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_3585,c_2045]) ).
tcf(c_3930,plain,
! [X0: $i] : iPr_def_11(X0,X0) = inverse(iPr_def_16),
inference(superposition,[status(thm)],[c_3588,c_3592]) ).
tcf(c_4146,plain,
! [X0: $i] : multiply(X0,inverse(iPr_def_16)) = iPr_def_11(iPr_def_16,iPr_def_10(X0)),
inference(superposition,[status(thm)],[c_3592,c_3735]) ).
tcf(c_4150,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_3735,c_3584]) ).
tcf(c_4167,plain,
iPr_def_11(iPr_def_16,inverse(iPr_def_16)) = iPr_def_16,
inference(demodulation,[status(thm)],[c_4150,c_68,c_3592]) ).
tcf(c_4225,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_3897,c_2045]) ).
tcf(c_4226,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_3895,c_3930,c_4146]) ).
tcf(c_4227,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_4226,c_68]) ).
tcf(c_4228,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_3894,c_3930,c_4146]) ).
tcf(c_4229,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_4228,c_68]) ).
tcf(c_4243,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_3896,c_3930,c_4146]) ).
tcf(c_4244,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_4243,c_68]) ).
tcf(c_4431,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_3653,c_3905]) ).
tcf(c_4452,plain,
! [X0: $i] : multiply(inverse(X0),iPr_def_16) = iPr_def_11(iPr_def_16,X0),
inference(superposition,[status(thm)],[c_4167,c_3595]) ).
tcf(c_4456,plain,
! [X0: $i] : multiply(inverse(iPr_def_11(X0,inverse(iPr_def_16))),X0) = inverse(iPr_def_16),
inference(superposition,[status(thm)],[c_3595,c_3930]) ).
tcf(c_4472,plain,
! [X0: $i] : iPr_def_11(iPr_def_13(X0,X0),inverse(iPr_def_16)) = iPr_def_16,
inference(superposition,[status(thm)],[c_3661,c_3584]) ).
tcf(c_4510,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_4229,c_3905]) ).
tcf(c_4511,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_4229,c_3901]) ).
tcf(c_4546,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_3653,c_3902]) ).
tcf(c_4636,plain,
inverse(iPr_def_16) = iPr_def_16,
inference(demodulation,[status(thm)],[c_4472,c_3592,c_3930]) ).
tcf(c_4657,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_4431,c_68]) ).
tcf(c_4666,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_4546,c_4452,c_4657]) ).
tcf(c_4667,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_4666,c_68]) ).
tcf(c_4669,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_4511,c_68,c_3930]) ).
tcf(c_4670,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_4510,c_68,c_3930]) ).
tcf(c_4794,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_3902,c_4452]) ).
tcf(c_4795,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_4794,c_3905]) ).
tcf(c_4801,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_3595,c_4636]) ).
tcf(c_4805,plain,
! [X0: $i] : iPr_def_11(X0,X0) = iPr_def_16,
inference(demodulation,[status(thm)],[c_3930,c_4636]) ).
tcf(c_4807,plain,
! [X0: $i] : iPr_def_13(X0,X0) = iPr_def_16,
inference(demodulation,[status(thm)],[c_3592,c_4636]) ).
tcf(c_4808,plain,
! [X0: $i] : iPr_def_11(iPr_def_16,iPr_def_10(X0)) = multiply(X0,iPr_def_16),
inference(demodulation,[status(thm)],[c_3735,c_4807]) ).
tcf(c_4815,plain,
! [X0: $i] : iPr_def_11(inverse(multiply(X0,iPr_def_16)),iPr_def_16) = iPr_def_10(X0),
inference(demodulation,[status(thm)],[c_4227,c_4805]) ).
tcf(c_7225,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_4225,c_4815]) ).
tcf(c_7227,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_4452,c_4815]) ).
tcf(c_7237,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_4456,c_2045]) ).
tcf(c_7242,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_4456,c_2045]) ).
tcf(c_7252,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_4795]) ).
tcf(c_7261,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_4795,c_161]) ).
tcf(c_7277,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_4801,c_4667]) ).
tcf(c_7289,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_4636,c_4669]) ).
tcf(c_7494,plain,
! [X0: $i] : iPr_def_11(inverse(iPr_def_11(iPr_def_16,X0)),iPr_def_16) = X0,
inference(demodulation,[status(thm)],[c_7227,c_68]) ).
tcf(c_7507,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_7277,c_7289]) ).
tcf(c_7508,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_7507,c_4636]) ).
tcf(c_7534,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_7225,c_7252]) ).
tcf(c_7535,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_7534,c_161]) ).
tcf(c_7611,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_7242,c_68,c_3905,c_4244]) ).
tcf(c_7612,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_7611,c_4636]) ).
tcf(c_7613,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_7237,c_4636]) ).
tcf(c_7614,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_7613,c_68,c_3901]) ).
tcf(c_7920,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_4669,c_7508]) ).
tcf(c_7921,plain,
! [X0: $i] : iPr_def_10(multiply(iPr_def_16,X0)) = iPr_def_13(inverse(iPr_def_16),X0),
inference(demodulation,[status(thm)],[c_7920,c_7614]) ).
tcf(c_7922,plain,
! [X0: $i] : iPr_def_10(multiply(iPr_def_16,X0)) = iPr_def_13(iPr_def_16,X0),
inference(light_normalisation,[status(thm)],[c_7921,c_4636]) ).
tcf(c_7926,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_4670,c_7612]) ).
tcf(c_7927,plain,
! [X0: $i] : iPr_def_13(X0,inverse(iPr_def_16)) = multiply(X0,iPr_def_16),
inference(demodulation,[status(thm)],[c_7926,c_4808]) ).
tcf(c_7928,plain,
! [X0: $i] : multiply(X0,iPr_def_16) = iPr_def_13(X0,iPr_def_16),
inference(light_normalisation,[status(thm)],[c_7927,c_4636]) ).
tcf(c_7933,plain,
! [X0: $i] : iPr_def_13(inverse(X0),iPr_def_16) = iPr_def_11(iPr_def_16,X0),
inference(demodulation,[status(thm)],[c_4452,c_7928]) ).
tcf(c_8146,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_7494,c_7252]) ).
tcf(c_8153,plain,
! [X0: $i] : inverse(iPr_def_13(iPr_def_16,X0)) = multiply(iPr_def_16,X0),
inference(superposition,[status(thm)],[c_7922,c_161]) ).
tcf(c_8223,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_7508]) ).
tcf(c_8243,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_7933,c_7535]) ).
tcf(c_8325,plain,
! [X0: $i,X1: $i] : inverse(iPr_def_13(X0,X1)) = iPr_def_11(X1,X0),
inference(superposition,[status(thm)],[c_68,c_7261]) ).
tcf(c_8356,plain,
! [X0: $i] : multiply(iPr_def_16,X0) = iPr_def_11(X0,iPr_def_16),
inference(demodulation,[status(thm)],[c_8153,c_8325]) ).
tcf(c_8366,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_8223,c_8356]) ).
tcf(c_8367,plain,
! [X0: $i] : iPr_def_13(iPr_def_16,inverse(X0)) = iPr_def_11(X0,iPr_def_16),
inference(demodulation,[status(thm)],[c_8366,c_7252]) ).
tcf(c_8371,plain,
! [X0: $i] : iPr_def_11(iPr_def_16,X0) = iPr_def_10(X0),
inference(demodulation,[status(thm)],[c_8146,c_8243,c_8367]) ).
tcf(c_8546,plain,
iPr_def_11(a2,iPr_def_16) != a2,
inference(demodulation,[status(thm)],[c_3759,c_8356]) ).
tcf(c_8566,plain,
! [X0: $i] : iPr_def_11(inverse(iPr_def_10(X0)),iPr_def_16) = X0,
inference(demodulation,[status(thm)],[c_7494,c_8371]) ).
tcf(c_8571,plain,
! [X0: $i] : iPr_def_11(X0,iPr_def_16) = X0,
inference(demodulation,[status(thm)],[c_8566,c_161]) ).
tcf(c_8586,plain,
iPr_def_11(a2,iPr_def_16) = a2,
inference(instantiation,[status(thm)],[c_8571]) ).
tcf(c_8587,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_8546,c_8586]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GRP422-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.10/0.38 % Computer : n026.cluster.edu
% 0.10/0.38 % Model : x86_64 x86_64
% 0.10/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.38 % Memory : 8046.5625MB
% 0.10/0.38 % OS : Linux 6.8.0-71-generic
% 0.10/0.38 % CPULimit : 300
% 0.10/0.38 % WCLimit : 300
% 0.10/0.38 % DateTime : Wed Sep 23 14:45:39 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.38 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.10/0.42 Running UEQ theorem proving
% 0.10/0.42 Running: /export/starexec/sandbox/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s ueq_schedule -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.43
% 0.10/0.43 % ======== iProver multi-core TPTP/SMT =========
% 0.10/0.43
% 0.10/0.43 % Detected problem language: tptp
% 0.10/0.44 % Proving...
% 2.57/2.26 WARNING - Clausifier option not provided in the heuristic config "heur/vip2_118404", setting default options.
% 2.57/2.26 % SZS status Started for theBenchmark.p
% 2.57/2.26 % SZS status Unsatisfiable for theBenchmark.p
% 2.57/2.26
% 2.57/2.26 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 2.57/2.26
% 2.57/2.26 % ------ iProver source info
% 2.57/2.26
% 2.57/2.26 % git: date: 2026-07-19 20:42:38 +0200
% 2.57/2.26 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 2.57/2.26 % git: non_committed_changes: false
% 2.57/2.26
% 2.57/2.26 % ------ Parsing...% successful
% 2.57/2.26
% 2.57/2.26
% 2.57/2.26 % ------ Clausification by vclausify_rel & Parsing by iProver...
% 2.57/2.26 % ------ Proving...
% 2.57/2.26 % ------ Problem Properties
% 2.57/2.26
% 2.57/2.26 %
% 2.57/2.26 % clauses 2
% 2.57/2.26 % conjectures 1
% 2.57/2.26 % EPR 0
% 2.57/2.26 % Horn 2
% 2.57/2.26 % unary 2
% 2.57/2.26 % binary 0
% 2.57/2.26 % lits 2
% 2.57/2.26 % lits eq 2
% 2.57/2.26 % fd_pure 0
% 2.57/2.26 % fd_pseudo 0
% 2.57/2.26 % fd_cond 0
% 2.57/2.26 % fd_pseudo_cond 0
% 2.57/2.26 % AC symbols 0
% 2.57/2.26
% 2.57/2.26 % ------ Input Options Time Limit: Unbounded
% 2.57/2.26
% 2.57/2.26
% 2.57/2.26 % ------
% 2.57/2.26 % Current options:
% 2.57/2.26 % ------
% 2.57/2.26
% 2.57/2.26
% 2.57/2.26 %
% 2.57/2.26
% 2.57/2.26 % ------ Proving...
% 2.57/2.26 %
% 2.57/2.26
% 2.57/2.26 % SZS status Unsatisfiable for theBenchmark.p
% 2.57/2.26
% 2.57/2.26 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 2.57/2.27
% 2.57/2.27
%------------------------------------------------------------------------------