%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : GRP410-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 : n012.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 01:33:40 PM UTC 2026
% Result : Unsatisfiable 43.48s 7.00s
% Output : CNFRefutation 43.48s
% Verified :
% SZS Type : Refutation
% Derivation depth : 56
% Number of leaves : 5
% Syntax : Number of formulae : 179 ( 179 unt; 3 def)
% Number of atoms : 914 ( 178 equ)
% Maximal formula atoms : 1 ( 5 avg)
% Number of connectives : 5 ( 5 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 2 avg)
% Maximal term depth : 11 ( 3 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 5 ( 3 usr; 4 prp; 0-2 aty)
% Number of functors : 4 ( 4 usr; 2 con; 0-2 aty)
% Number of variables : 182 ( 0 sgn 182 !; 0 ?; 179 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X2,X0,X1] : multiply(multiply(inverse(multiply(X0,inverse(multiply(X1,X2)))),multiply(X0,inverse(X2))),inverse(multiply(inverse(X2),X2))) = X1,
file('/export/starexec/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] : multiply(multiply(inverse(multiply(X0,inverse(multiply(X1,X2)))),multiply(X0,inverse(X2))),inverse(multiply(inverse(X2),X2))) = X1,
inference(cnf_transformation,[],[f1]) ).
tcf(c_52,negated_conjecture,
multiply(multiply(inverse(b2),b2),a2) != a2,
inference(cnf_transformation,[],[f3]) ).
tcf(c_62,definition,
iPr_def_10 = inverse(b2),
introduced(definition,[new_symbols(definition,[iPr_def_10])],[]) ).
tcf(c_63,definition,
iPr_def_11 = multiply(iPr_def_10,b2),
introduced(definition,[new_symbols(definition,[iPr_def_11])],[]) ).
tcf(c_64,definition,
iPr_def_12 = multiply(iPr_def_11,a2),
introduced(definition,[new_symbols(definition,[iPr_def_12])],[]) ).
tcf(c_65,negated_conjecture,
iPr_def_12 != a2,
inference(demodulation,[status(thm)],[c_52,c_62,c_63,c_64]) ).
tcf(c_113,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : multiply(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(inverse(multiply(inverse(X2),X2))))),inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2))))) = multiply(inverse(multiply(X3,inverse(multiply(X1,X2)))),multiply(X3,inverse(X2))),
inference(superposition,[status(thm)],[c_51,c_51]) ).
tcf(c_119,plain,
! [X0: $i,X1: $i] : multiply(multiply(inverse(multiply(X0,inverse(multiply(X1,b2)))),multiply(X0,iPr_def_10)),inverse(multiply(iPr_def_10,b2))) = X1,
inference(superposition,[status(thm)],[c_62,c_51]) ).
tcf(c_120,plain,
! [X0: $i,X1: $i] : multiply(multiply(inverse(multiply(X0,inverse(multiply(X1,b2)))),multiply(X0,iPr_def_10)),inverse(iPr_def_11)) = X1,
inference(light_normalisation,[status(thm)],[c_119,c_63]) ).
tcf(c_124,plain,
! [X0: $i] : multiply(multiply(inverse(multiply(X0,inverse(iPr_def_11))),multiply(X0,inverse(b2))),inverse(multiply(inverse(b2),b2))) = iPr_def_10,
inference(superposition,[status(thm)],[c_63,c_51]) ).
tcf(c_125,plain,
! [X0: $i] : multiply(multiply(inverse(multiply(X0,inverse(iPr_def_11))),multiply(X0,iPr_def_10)),inverse(iPr_def_11)) = iPr_def_10,
inference(light_normalisation,[status(thm)],[c_124,c_62,c_63]) ).
tcf(c_128,plain,
! [X0: $i] : multiply(multiply(inverse(multiply(X0,inverse(iPr_def_12))),multiply(X0,inverse(a2))),inverse(multiply(inverse(a2),a2))) = iPr_def_11,
inference(superposition,[status(thm)],[c_64,c_51]) ).
tcf(c_151,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(inverse(iPr_def_11)))),inverse(multiply(inverse(inverse(iPr_def_11)),inverse(iPr_def_11)))) = multiply(inverse(multiply(X2,inverse(multiply(X1,b2)))),multiply(X2,iPr_def_10)),
inference(superposition,[status(thm)],[c_120,c_51]) ).
tcf(c_152,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(multiply(inverse(multiply(multiply(inverse(multiply(X0,inverse(multiply(X1,b2)))),multiply(X0,iPr_def_10)),inverse(multiply(X2,iPr_def_11)))),X1),inverse(multiply(inverse(iPr_def_11),iPr_def_11))) = X2,
inference(superposition,[status(thm)],[c_120,c_51]) ).
tcf(c_161,plain,
! [X0: $i,X1: $i] : multiply(multiply(inverse(multiply(X0,inverse(iPr_def_11))),multiply(X0,inverse(inverse(multiply(inverse(a2),a2))))),inverse(multiply(inverse(inverse(multiply(inverse(a2),a2))),inverse(multiply(inverse(a2),a2))))) = multiply(inverse(multiply(X1,inverse(iPr_def_12))),multiply(X1,inverse(a2))),
inference(superposition,[status(thm)],[c_128,c_51]) ).
tcf(c_163,plain,
! [X0: $i,X1: $i] : multiply(multiply(inverse(multiply(multiply(inverse(multiply(X0,inverse(iPr_def_12))),multiply(X0,inverse(a2))),inverse(multiply(X1,multiply(inverse(a2),a2))))),iPr_def_11),inverse(multiply(inverse(multiply(inverse(a2),a2)),multiply(inverse(a2),a2)))) = X1,
inference(superposition,[status(thm)],[c_128,c_51]) ).
tcf(c_256,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] : multiply(multiply(inverse(X0),multiply(multiply(inverse(multiply(X1,inverse(multiply(X0,X2)))),multiply(X1,inverse(X2))),inverse(inverse(multiply(inverse(X3),X3))))),inverse(multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(multiply(inverse(X3),X3))))) = multiply(inverse(multiply(X4,inverse(multiply(multiply(inverse(X2),X2),X3)))),multiply(X4,inverse(X3))),
inference(superposition,[status(thm)],[c_51,c_113]) ).
tcf(c_275,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : multiply(multiply(inverse(multiply(X0,inverse(multiply(inverse(multiply(X1,inverse(multiply(X2,b2)))),multiply(X1,iPr_def_10))))),multiply(X0,inverse(inverse(multiply(inverse(inverse(iPr_def_11)),inverse(iPr_def_11)))))),inverse(multiply(inverse(inverse(multiply(inverse(inverse(iPr_def_11)),inverse(iPr_def_11)))),inverse(multiply(inverse(inverse(iPr_def_11)),inverse(iPr_def_11)))))) = multiply(inverse(multiply(X3,inverse(X2))),multiply(X3,inverse(inverse(iPr_def_11)))),
inference(superposition,[status(thm)],[c_120,c_113]) ).
tcf(c_281,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : multiply(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(inverse(multiply(inverse(iPr_def_11),iPr_def_11))))),inverse(multiply(inverse(inverse(multiply(inverse(iPr_def_11),iPr_def_11))),inverse(multiply(inverse(iPr_def_11),iPr_def_11))))) = multiply(inverse(multiply(multiply(inverse(multiply(X2,inverse(multiply(X3,b2)))),multiply(X2,iPr_def_10)),inverse(multiply(X1,iPr_def_11)))),X3),
inference(superposition,[status(thm)],[c_120,c_113]) ).
tcf(c_282,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(inverse(multiply(inverse(iPr_def_11),iPr_def_11))))),inverse(multiply(inverse(inverse(multiply(inverse(iPr_def_11),iPr_def_11))),inverse(multiply(inverse(iPr_def_11),iPr_def_11))))) = multiply(inverse(multiply(multiply(inverse(multiply(X2,inverse(iPr_def_11))),multiply(X2,iPr_def_10)),inverse(multiply(X1,iPr_def_11)))),iPr_def_10),
inference(superposition,[status(thm)],[c_125,c_113]) ).
tcf(c_290,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(inverse(multiply(X0,inverse(multiply(multiply(X1,inverse(multiply(inverse(X2),X2))),X2)))),multiply(X0,inverse(X2))) = X1,
inference(superposition,[status(thm)],[c_113,c_51]) ).
tcf(c_292,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : multiply(inverse(multiply(X0,inverse(multiply(X1,X2)))),multiply(X0,inverse(X2))) = multiply(inverse(multiply(X3,inverse(multiply(X1,X2)))),multiply(X3,inverse(X2))),
inference(superposition,[status(thm)],[c_113,c_113]) ).
tcf(c_297,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(multiply(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(inverse(multiply(inverse(X2),X2))))),inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2))))),inverse(multiply(inverse(X2),X2))) = X1,
inference(superposition,[status(thm)],[c_113,c_51]) ).
tcf(c_363,plain,
! [X0: $i,X1: $i] : multiply(inverse(multiply(multiply(inverse(multiply(X0,inverse(iPr_def_11))),multiply(X0,iPr_def_10)),inverse(multiply(multiply(X1,inverse(multiply(inverse(iPr_def_11),iPr_def_11))),iPr_def_11)))),iPr_def_10) = X1,
inference(superposition,[status(thm)],[c_125,c_290]) ).
tcf(c_366,plain,
! [X0: $i,X1: $i] : multiply(inverse(multiply(X0,inverse(multiply(multiply(X1,inverse(multiply(iPr_def_10,b2))),b2)))),multiply(X0,iPr_def_10)) = X1,
inference(superposition,[status(thm)],[c_62,c_290]) ).
tcf(c_371,plain,
! [X0: $i,X1: $i] : multiply(inverse(multiply(X0,inverse(multiply(multiply(X1,inverse(iPr_def_11)),b2)))),multiply(X0,iPr_def_10)) = X1,
inference(light_normalisation,[status(thm)],[c_366,c_63]) ).
tcf(c_428,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(inverse(multiply(X0,inverse(multiply(X1,b2)))),multiply(X0,iPr_def_10)) = multiply(inverse(multiply(X2,inverse(multiply(X1,b2)))),multiply(X2,iPr_def_10)),
inference(superposition,[status(thm)],[c_120,c_371]) ).
tcf(c_1536,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(multiply(X2,iPr_def_10)))) = multiply(inverse(multiply(X3,inverse(X1))),multiply(X3,inverse(multiply(X2,iPr_def_10)))),
inference(superposition,[status(thm)],[c_371,c_292]) ).
tcf(c_2697,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(X2))) = multiply(inverse(multiply(X3,inverse(X1))),multiply(X3,inverse(X2))),
inference(superposition,[status(thm)],[c_363,c_1536]) ).
tcf(c_2951,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(inverse(multiply(X0,iPr_def_10)),multiply(X0,inverse(X1))) = multiply(inverse(multiply(X2,iPr_def_10)),multiply(X2,inverse(X1))),
inference(superposition,[status(thm)],[c_62,c_2697]) ).
tcf(c_3239,plain,
! [X0: $i,X1: $i] : multiply(inverse(multiply(X0,iPr_def_10)),multiply(X0,iPr_def_10)) = multiply(inverse(multiply(X1,iPr_def_10)),multiply(X1,iPr_def_10)),
inference(superposition,[status(thm)],[c_62,c_2951]) ).
tcf(c_3261,plain,
! [X0: $i,X1: $i] : multiply(inverse(multiply(X0,iPr_def_10)),multiply(X0,iPr_def_10)) = multiply(inverse(X1),X1),
inference(superposition,[status(thm)],[c_363,c_3239]) ).
tcf(c_3391,plain,
! [X0: $i,X1: $i] : multiply(inverse(X0),X0) = multiply(inverse(X1),X1),
inference(superposition,[status(thm)],[c_3261,c_3261]) ).
tcf(c_3908,plain,
! [X0: $i] : multiply(inverse(X0),X0) = multiply(iPr_def_10,b2),
inference(superposition,[status(thm)],[c_62,c_3391]) ).
tcf(c_4083,plain,
! [X0: $i] : multiply(inverse(X0),X0) = iPr_def_11,
inference(light_normalisation,[status(thm)],[c_3908,c_63]) ).
tcf(c_4172,plain,
multiply(iPr_def_10,b2) = iPr_def_11,
inference(superposition,[status(thm)],[c_62,c_4083]) ).
tcf(c_4180,plain,
! [X0: $i] : multiply(multiply(inverse(multiply(X0,inverse(iPr_def_11))),multiply(X0,iPr_def_10)),inverse(iPr_def_11)) = inverse(b2),
inference(superposition,[status(thm)],[c_4083,c_120]) ).
tcf(c_4182,plain,
! [X0: $i] : multiply(multiply(inverse(iPr_def_11),multiply(inverse(inverse(multiply(X0,b2))),iPr_def_10)),inverse(iPr_def_11)) = X0,
inference(superposition,[status(thm)],[c_4083,c_120]) ).
tcf(c_4191,plain,
! [X0: $i] : multiply(inverse(multiply(inverse(iPr_def_10),inverse(multiply(multiply(X0,inverse(iPr_def_11)),b2)))),iPr_def_11) = X0,
inference(superposition,[status(thm)],[c_4083,c_371]) ).
tcf(c_4199,plain,
multiply(multiply(inverse(iPr_def_11),multiply(inverse(inverse(iPr_def_11)),iPr_def_10)),inverse(iPr_def_11)) = iPr_def_10,
inference(superposition,[status(thm)],[c_4083,c_125]) ).
tcf(c_4207,plain,
! [X0: $i,X1: $i] : multiply(inverse(multiply(X0,inverse(multiply(X1,b2)))),multiply(X0,iPr_def_10)) = multiply(inverse(iPr_def_11),multiply(inverse(inverse(multiply(X1,b2))),iPr_def_10)),
inference(superposition,[status(thm)],[c_4083,c_428]) ).
tcf(c_4210,plain,
! [X0: $i] : multiply(inverse(iPr_def_11),multiply(inverse(inverse(multiply(multiply(X0,inverse(iPr_def_11)),b2))),iPr_def_10)) = X0,
inference(superposition,[status(thm)],[c_4083,c_371]) ).
tcf(c_4216,plain,
inverse(b2) = iPr_def_10,
inference(demodulation,[status(thm)],[c_4180,c_125]) ).
tcf(c_4258,plain,
! [X0: $i] : multiply(inverse(multiply(X0,inverse(multiply(inverse(iPr_def_11),b2)))),multiply(X0,iPr_def_10)) = multiply(iPr_def_11,inverse(multiply(inverse(inverse(iPr_def_11)),inverse(iPr_def_11)))),
inference(superposition,[status(thm)],[c_4083,c_151]) ).
tcf(c_4276,plain,
! [X0: $i] : multiply(inverse(multiply(X0,inverse(multiply(inverse(iPr_def_11),b2)))),multiply(X0,iPr_def_10)) = multiply(iPr_def_11,inverse(iPr_def_11)),
inference(demodulation,[status(thm)],[c_4258,c_4083]) ).
tcf(c_4306,plain,
multiply(inverse(multiply(inverse(iPr_def_10),inverse(multiply(iPr_def_10,b2)))),iPr_def_11) = multiply(inverse(iPr_def_11),multiply(inverse(inverse(iPr_def_11)),iPr_def_10)),
inference(superposition,[status(thm)],[c_4199,c_4191]) ).
tcf(c_4307,plain,
multiply(inverse(multiply(inverse(iPr_def_10),inverse(iPr_def_11))),iPr_def_11) = multiply(inverse(iPr_def_11),multiply(inverse(inverse(iPr_def_11)),iPr_def_10)),
inference(light_normalisation,[status(thm)],[c_4306,c_4172]) ).
tcf(c_4326,plain,
! [X0: $i,X1: $i] : multiply(multiply(inverse(multiply(multiply(inverse(iPr_def_11),multiply(inverse(inverse(multiply(X0,b2))),iPr_def_10)),inverse(multiply(X1,iPr_def_11)))),X0),inverse(multiply(inverse(iPr_def_11),iPr_def_11))) = X1,
inference(light_normalisation,[status(thm)],[c_152,c_4207]) ).
tcf(c_4327,plain,
! [X0: $i,X1: $i] : multiply(multiply(inverse(multiply(X0,inverse(multiply(X1,iPr_def_11)))),multiply(X0,inverse(iPr_def_11))),inverse(multiply(inverse(iPr_def_11),iPr_def_11))) = X1,
inference(superposition,[status(thm)],[c_4210,c_4326]) ).
tcf(c_4332,plain,
! [X0: $i] : multiply(multiply(inverse(multiply(multiply(inverse(iPr_def_11),multiply(inverse(inverse(multiply(X0,b2))),iPr_def_10)),inverse(iPr_def_11))),X0),inverse(iPr_def_11)) = inverse(iPr_def_11),
inference(superposition,[status(thm)],[c_4083,c_4326]) ).
tcf(c_4337,plain,
! [X0: $i,X1: $i] : multiply(multiply(inverse(multiply(X0,inverse(multiply(X1,iPr_def_11)))),multiply(X0,inverse(iPr_def_11))),inverse(iPr_def_11)) = X1,
inference(demodulation,[status(thm)],[c_4327,c_4083]) ).
tcf(c_4338,plain,
multiply(iPr_def_11,inverse(iPr_def_11)) = inverse(iPr_def_11),
inference(demodulation,[status(thm)],[c_4332,c_4083,c_4182]) ).
tcf(c_4351,plain,
multiply(inverse(iPr_def_11),multiply(inverse(inverse(multiply(inverse(iPr_def_11),b2))),iPr_def_10)) = iPr_def_11,
inference(superposition,[status(thm)],[c_4338,c_4210]) ).
tcf(c_4517,plain,
! [X0: $i] : multiply(inverse(multiply(X0,inverse(multiply(inverse(iPr_def_11),b2)))),multiply(X0,iPr_def_10)) = inverse(iPr_def_11),
inference(light_normalisation,[status(thm)],[c_4276,c_4338]) ).
tcf(c_4519,plain,
multiply(inverse(iPr_def_11),multiply(inverse(inverse(multiply(inverse(iPr_def_11),b2))),iPr_def_10)) = inverse(iPr_def_11),
inference(superposition,[status(thm)],[c_4083,c_4517]) ).
tcf(c_4522,plain,
inverse(iPr_def_11) = iPr_def_11,
inference(light_normalisation,[status(thm)],[c_4519,c_4351]) ).
tcf(c_4530,plain,
multiply(iPr_def_11,iPr_def_11) = iPr_def_11,
inference(demodulation,[status(thm)],[c_4338,c_4522]) ).
tcf(c_4532,plain,
! [X0: $i] : multiply(iPr_def_11,multiply(inverse(inverse(multiply(multiply(X0,iPr_def_11),b2))),iPr_def_10)) = X0,
inference(demodulation,[status(thm)],[c_4210,c_4522]) ).
tcf(c_4537,plain,
! [X0: $i] : multiply(multiply(iPr_def_11,multiply(inverse(inverse(multiply(X0,b2))),iPr_def_10)),iPr_def_11) = X0,
inference(demodulation,[status(thm)],[c_4182,c_4522]) ).
tcf(c_4538,plain,
multiply(multiply(iPr_def_11,multiply(inverse(iPr_def_11),iPr_def_10)),iPr_def_11) = iPr_def_10,
inference(demodulation,[status(thm)],[c_4199,c_4522]) ).
tcf(c_4549,plain,
! [X0: $i,X1: $i] : multiply(multiply(inverse(multiply(X0,iPr_def_11)),multiply(X0,inverse(inverse(multiply(inverse(a2),a2))))),inverse(multiply(inverse(inverse(multiply(inverse(a2),a2))),inverse(multiply(inverse(a2),a2))))) = multiply(inverse(multiply(X1,inverse(iPr_def_12))),multiply(X1,inverse(a2))),
inference(light_normalisation,[status(thm)],[c_161,c_4522]) ).
tcf(c_4552,plain,
! [X0: $i] : multiply(multiply(inverse(multiply(inverse(inverse(inverse(multiply(inverse(a2),a2)))),iPr_def_11)),iPr_def_11),inverse(multiply(inverse(inverse(multiply(inverse(a2),a2))),inverse(multiply(inverse(a2),a2))))) = multiply(inverse(multiply(X0,inverse(iPr_def_12))),multiply(X0,inverse(a2))),
inference(superposition,[status(thm)],[c_4083,c_4549]) ).
tcf(c_4566,plain,
! [X0: $i] : multiply(multiply(inverse(multiply(inverse(inverse(inverse(iPr_def_11))),iPr_def_11)),iPr_def_11),inverse(iPr_def_11)) = multiply(inverse(multiply(X0,inverse(iPr_def_12))),multiply(X0,inverse(a2))),
inference(demodulation,[status(thm)],[c_4552,c_4083]) ).
tcf(c_4567,plain,
! [X0: $i] : multiply(inverse(multiply(X0,inverse(iPr_def_12))),multiply(X0,inverse(a2))) = iPr_def_11,
inference(light_normalisation,[status(thm)],[c_4566,c_4522,c_4530]) ).
tcf(c_4580,plain,
multiply(multiply(iPr_def_11,multiply(iPr_def_11,iPr_def_10)),iPr_def_11) = iPr_def_10,
inference(light_normalisation,[status(thm)],[c_4538,c_4522]) ).
tcf(c_4587,plain,
! [X0: $i] : multiply(multiply(inverse(multiply(iPr_def_11,inverse(multiply(X0,multiply(inverse(a2),a2))))),iPr_def_11),inverse(multiply(inverse(multiply(inverse(a2),a2)),multiply(inverse(a2),a2)))) = X0,
inference(light_normalisation,[status(thm)],[c_163,c_4567]) ).
tcf(c_4591,plain,
! [X0: $i] : multiply(multiply(inverse(multiply(iPr_def_11,inverse(multiply(X0,iPr_def_11)))),iPr_def_11),inverse(multiply(inverse(iPr_def_11),iPr_def_11))) = X0,
inference(superposition,[status(thm)],[c_4083,c_4587]) ).
tcf(c_4595,plain,
! [X0: $i] : multiply(multiply(inverse(multiply(iPr_def_11,inverse(multiply(X0,iPr_def_11)))),iPr_def_11),inverse(iPr_def_11)) = X0,
inference(demodulation,[status(thm)],[c_4591,c_4083]) ).
tcf(c_4596,plain,
! [X0: $i] : multiply(multiply(inverse(multiply(iPr_def_11,inverse(multiply(X0,iPr_def_11)))),iPr_def_11),iPr_def_11) = X0,
inference(light_normalisation,[status(thm)],[c_4595,c_4522]) ).
tcf(c_4621,plain,
! [X0: $i] : multiply(multiply(inverse(multiply(iPr_def_11,inverse(X0))),iPr_def_11),iPr_def_11) = multiply(iPr_def_11,multiply(inverse(inverse(multiply(X0,b2))),iPr_def_10)),
inference(superposition,[status(thm)],[c_4537,c_4596]) ).
tcf(c_4622,plain,
multiply(multiply(inverse(multiply(iPr_def_11,inverse(iPr_def_10))),iPr_def_11),iPr_def_11) = multiply(iPr_def_11,multiply(iPr_def_11,iPr_def_10)),
inference(superposition,[status(thm)],[c_4580,c_4596]) ).
tcf(c_4624,plain,
! [X0: $i] : multiply(multiply(inverse(multiply(iPr_def_11,inverse(X0))),iPr_def_11),iPr_def_11) = multiply(inverse(multiply(iPr_def_11,inverse(multiply(X0,iPr_def_11)))),iPr_def_11),
inference(superposition,[status(thm)],[c_4596,c_4596]) ).
tcf(c_4712,plain,
multiply(inverse(multiply(inverse(iPr_def_10),iPr_def_11)),iPr_def_11) = multiply(iPr_def_11,multiply(iPr_def_11,iPr_def_10)),
inference(light_normalisation,[status(thm)],[c_4307,c_4522]) ).
tcf(c_4714,plain,
! [X0: $i,X1: $i] : multiply(multiply(inverse(multiply(X0,inverse(multiply(X1,iPr_def_11)))),multiply(X0,iPr_def_11)),iPr_def_11) = X1,
inference(light_normalisation,[status(thm)],[c_4337,c_4522]) ).
tcf(c_4715,plain,
! [X0: $i] : multiply(multiply(inverse(iPr_def_11),multiply(inverse(inverse(multiply(X0,iPr_def_11))),iPr_def_11)),iPr_def_11) = X0,
inference(superposition,[status(thm)],[c_4083,c_4714]) ).
tcf(c_4726,plain,
! [X0: $i] : multiply(multiply(inverse(multiply(multiply(iPr_def_11,multiply(iPr_def_11,iPr_def_10)),inverse(multiply(X0,iPr_def_11)))),iPr_def_10),iPr_def_11) = X0,
inference(superposition,[status(thm)],[c_4580,c_4714]) ).
tcf(c_4736,plain,
! [X0: $i] : multiply(multiply(iPr_def_11,multiply(inverse(inverse(multiply(X0,iPr_def_11))),iPr_def_11)),iPr_def_11) = X0,
inference(light_normalisation,[status(thm)],[c_4715,c_4522]) ).
tcf(c_4751,plain,
! [X0: $i] : multiply(multiply(iPr_def_11,multiply(inverse(inverse(X0)),iPr_def_11)),iPr_def_11) = multiply(iPr_def_11,multiply(inverse(inverse(multiply(X0,b2))),iPr_def_10)),
inference(superposition,[status(thm)],[c_4537,c_4736]) ).
tcf(c_4757,plain,
! [X0: $i] : multiply(iPr_def_11,multiply(inverse(inverse(multiply(X0,b2))),iPr_def_10)) = multiply(iPr_def_11,multiply(inverse(inverse(multiply(X0,iPr_def_11))),iPr_def_11)),
inference(superposition,[status(thm)],[c_4736,c_4532]) ).
tcf(c_4763,plain,
! [X0: $i] : multiply(iPr_def_11,multiply(inverse(inverse(multiply(multiply(X0,iPr_def_11),iPr_def_11))),iPr_def_11)) = X0,
inference(demodulation,[status(thm)],[c_4532,c_4757]) ).
tcf(c_4769,plain,
multiply(iPr_def_11,multiply(inverse(inverse(multiply(iPr_def_11,multiply(iPr_def_11,iPr_def_10)))),iPr_def_11)) = inverse(multiply(iPr_def_11,inverse(iPr_def_10))),
inference(superposition,[status(thm)],[c_4622,c_4763]) ).
tcf(c_4774,plain,
multiply(iPr_def_11,multiply(inverse(inverse(multiply(multiply(iPr_def_11,multiply(iPr_def_11,iPr_def_10)),iPr_def_11))),iPr_def_11)) = inverse(multiply(inverse(iPr_def_10),iPr_def_11)),
inference(superposition,[status(thm)],[c_4712,c_4763]) ).
tcf(c_4777,plain,
multiply(iPr_def_11,multiply(inverse(inverse(iPr_def_10)),iPr_def_11)) = inverse(multiply(inverse(iPr_def_10),iPr_def_11)),
inference(light_normalisation,[status(thm)],[c_4774,c_4580]) ).
tcf(c_4814,plain,
! [X0: $i] : multiply(multiply(inverse(multiply(multiply(iPr_def_11,multiply(iPr_def_11,iPr_def_10)),inverse(X0))),iPr_def_10),iPr_def_11) = multiply(inverse(multiply(multiply(iPr_def_11,multiply(iPr_def_11,iPr_def_10)),inverse(multiply(X0,iPr_def_11)))),iPr_def_10),
inference(superposition,[status(thm)],[c_4726,c_4726]) ).
tcf(c_4820,plain,
! [X0: $i] : multiply(multiply(multiply(inverse(multiply(multiply(iPr_def_11,multiply(iPr_def_11,iPr_def_10)),inverse(X0))),iPr_def_10),iPr_def_11),iPr_def_11) = X0,
inference(demodulation,[status(thm)],[c_4726,c_4814]) ).
tcf(c_4834,plain,
multiply(multiply(multiply(inverse(multiply(multiply(iPr_def_11,multiply(iPr_def_11,iPr_def_10)),iPr_def_10)),iPr_def_10),iPr_def_11),iPr_def_11) = b2,
inference(superposition,[status(thm)],[c_4216,c_4820]) ).
tcf(c_4858,plain,
multiply(multiply(inverse(multiply(multiply(iPr_def_11,multiply(iPr_def_11,iPr_def_10)),iPr_def_10)),iPr_def_10),iPr_def_11) = multiply(iPr_def_11,multiply(inverse(inverse(multiply(b2,iPr_def_11))),iPr_def_11)),
inference(superposition,[status(thm)],[c_4834,c_4763]) ).
tcf(c_4861,plain,
multiply(multiply(iPr_def_11,multiply(inverse(inverse(multiply(b2,iPr_def_11))),iPr_def_11)),iPr_def_11) = b2,
inference(demodulation,[status(thm)],[c_4834,c_4858]) ).
tcf(c_4887,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(multiply(inverse(iPr_def_11),multiply(multiply(inverse(multiply(X0,inverse(iPr_def_11))),multiply(X0,inverse(iPr_def_11))),inverse(inverse(multiply(inverse(X1),X1))))),inverse(multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(multiply(inverse(X1),X1))))) = multiply(inverse(multiply(X2,inverse(multiply(multiply(inverse(iPr_def_11),iPr_def_11),X1)))),multiply(X2,inverse(X1))),
inference(superposition,[status(thm)],[c_4530,c_256]) ).
tcf(c_4985,plain,
! [X0: $i,X1: $i] : multiply(inverse(multiply(X0,inverse(multiply(iPr_def_11,X1)))),multiply(X0,inverse(X1))) = multiply(multiply(inverse(iPr_def_11),multiply(iPr_def_11,inverse(inverse(iPr_def_11)))),inverse(iPr_def_11)),
inference(demodulation,[status(thm)],[c_4887,c_4083]) ).
tcf(c_4986,plain,
! [X0: $i,X1: $i] : multiply(inverse(multiply(X0,inverse(multiply(iPr_def_11,X1)))),multiply(X0,inverse(X1))) = iPr_def_11,
inference(light_normalisation,[status(thm)],[c_4985,c_4522,c_4530]) ).
tcf(c_5387,plain,
! [X0: $i] : multiply(inverse(multiply(inverse(inverse(X0)),inverse(multiply(iPr_def_11,X0)))),iPr_def_11) = iPr_def_11,
inference(superposition,[status(thm)],[c_4083,c_4986]) ).
tcf(c_5464,plain,
! [X0: $i] : inverse(multiply(inverse(inverse(X0)),inverse(multiply(iPr_def_11,X0)))) = multiply(iPr_def_11,multiply(inverse(inverse(multiply(iPr_def_11,iPr_def_11))),iPr_def_11)),
inference(superposition,[status(thm)],[c_5387,c_4763]) ).
tcf(c_5468,plain,
! [X0: $i] : inverse(multiply(inverse(inverse(X0)),inverse(multiply(iPr_def_11,X0)))) = iPr_def_11,
inference(light_normalisation,[status(thm)],[c_5464,c_4522,c_4530]) ).
tcf(c_15713,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : multiply(multiply(inverse(multiply(X0,inverse(multiply(inverse(multiply(X1,inverse(multiply(X2,b2)))),multiply(X1,iPr_def_10))))),multiply(X0,iPr_def_11)),iPr_def_11) = multiply(inverse(multiply(X3,inverse(X2))),multiply(X3,iPr_def_11)),
inference(light_normalisation,[status(thm)],[c_275,c_4522,c_4530]) ).
tcf(c_15747,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(multiply(inverse(multiply(X0,inverse(multiply(inverse(multiply(X1,inverse(multiply(X2,b2)))),multiply(X1,iPr_def_10))))),multiply(X0,iPr_def_11)),iPr_def_11) = multiply(inverse(iPr_def_11),multiply(inverse(inverse(X2)),iPr_def_11)),
inference(superposition,[status(thm)],[c_4083,c_15713]) ).
tcf(c_15797,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(multiply(inverse(multiply(X0,inverse(multiply(inverse(multiply(X1,inverse(multiply(X2,b2)))),multiply(X1,iPr_def_10))))),multiply(X0,iPr_def_11)),iPr_def_11) = multiply(iPr_def_11,multiply(inverse(inverse(X2)),iPr_def_11)),
inference(light_normalisation,[status(thm)],[c_15747,c_4522]) ).
tcf(c_15853,plain,
! [X0: $i,X1: $i] : multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,iPr_def_11)) = multiply(iPr_def_11,multiply(inverse(inverse(X1)),iPr_def_11)),
inference(demodulation,[status(thm)],[c_15713,c_15797]) ).
tcf(c_16456,plain,
! [X0: $i] : multiply(iPr_def_11,multiply(inverse(inverse(multiply(iPr_def_11,X0))),iPr_def_11)) = multiply(iPr_def_11,multiply(inverse(inverse(X0)),iPr_def_11)),
inference(superposition,[status(thm)],[c_5468,c_15853]) ).
tcf(c_16468,plain,
! [X0: $i] : multiply(inverse(X0),multiply(multiply(inverse(multiply(iPr_def_11,inverse(multiply(X0,multiply(inverse(a2),a2))))),iPr_def_11),iPr_def_11)) = multiply(iPr_def_11,multiply(inverse(inverse(multiply(inverse(multiply(inverse(a2),a2)),multiply(inverse(a2),a2)))),iPr_def_11)),
inference(superposition,[status(thm)],[c_4587,c_15853]) ).
tcf(c_16483,plain,
! [X0: $i] : multiply(inverse(multiply(X0,iPr_def_10)),multiply(X0,iPr_def_11)) = multiply(iPr_def_11,multiply(inverse(iPr_def_10),iPr_def_11)),
inference(superposition,[status(thm)],[c_4216,c_15853]) ).
tcf(c_16504,plain,
! [X0: $i] : multiply(inverse(multiply(iPr_def_11,inverse(X0))),iPr_def_11) = multiply(iPr_def_11,multiply(inverse(inverse(X0)),iPr_def_11)),
inference(superposition,[status(thm)],[c_4530,c_15853]) ).
tcf(c_16536,plain,
! [X0: $i] : multiply(inverse(X0),multiply(multiply(inverse(multiply(iPr_def_11,inverse(multiply(X0,iPr_def_11)))),iPr_def_11),iPr_def_11)) = multiply(iPr_def_11,multiply(inverse(inverse(iPr_def_11)),iPr_def_11)),
inference(demodulation,[status(thm)],[c_16468,c_4083]) ).
tcf(c_16537,plain,
! [X0: $i] : multiply(inverse(X0),multiply(multiply(iPr_def_11,multiply(inverse(inverse(multiply(X0,iPr_def_11))),iPr_def_11)),iPr_def_11)) = iPr_def_11,
inference(light_normalisation,[status(thm)],[c_16536,c_4522,c_4530,c_4621,c_4624,c_4757]) ).
tcf(c_16546,plain,
multiply(iPr_def_11,multiply(inverse(inverse(multiply(iPr_def_11,iPr_def_10))),iPr_def_11)) = inverse(multiply(iPr_def_11,inverse(iPr_def_10))),
inference(demodulation,[status(thm)],[c_4769,c_16456]) ).
tcf(c_16727,plain,
multiply(inverse(multiply(iPr_def_11,iPr_def_10)),iPr_def_11) = multiply(iPr_def_11,multiply(inverse(iPr_def_10),iPr_def_11)),
inference(superposition,[status(thm)],[c_4530,c_16483]) ).
tcf(c_20504,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(inverse(multiply(multiply(inverse(multiply(X0,inverse(multiply(X1,b2)))),multiply(X0,iPr_def_10)),inverse(multiply(X2,iPr_def_11)))),X1) = multiply(multiply(iPr_def_11,multiply(inverse(inverse(X2)),iPr_def_11)),iPr_def_11),
inference(light_normalisation,[status(thm)],[c_281,c_4522,c_4530,c_15853]) ).
tcf(c_20505,plain,
! [X0: $i,X1: $i] : multiply(inverse(multiply(multiply(iPr_def_11,multiply(inverse(inverse(multiply(X0,b2))),iPr_def_10)),inverse(multiply(X1,iPr_def_11)))),X0) = multiply(multiply(iPr_def_11,multiply(inverse(inverse(X1)),iPr_def_11)),iPr_def_11),
inference(light_normalisation,[status(thm)],[c_20504,c_4207,c_4522]) ).
tcf(c_20506,plain,
! [X0: $i,X1: $i] : multiply(inverse(multiply(multiply(iPr_def_11,multiply(inverse(inverse(multiply(X0,iPr_def_11))),iPr_def_11)),inverse(multiply(X1,iPr_def_11)))),X0) = multiply(multiply(iPr_def_11,multiply(inverse(inverse(X1)),iPr_def_11)),iPr_def_11),
inference(light_normalisation,[status(thm)],[c_20505,c_4757]) ).
tcf(c_20589,plain,
! [X0: $i] : multiply(iPr_def_11,multiply(inverse(inverse(multiply(multiply(multiply(iPr_def_11,multiply(inverse(inverse(X0)),iPr_def_11)),iPr_def_11),iPr_def_11))),iPr_def_11)) = inverse(multiply(multiply(iPr_def_11,multiply(inverse(inverse(multiply(iPr_def_11,iPr_def_11))),iPr_def_11)),inverse(multiply(X0,iPr_def_11)))),
inference(superposition,[status(thm)],[c_20506,c_4763]) ).
tcf(c_20614,plain,
! [X0: $i] : inverse(multiply(multiply(iPr_def_11,multiply(inverse(inverse(multiply(iPr_def_11,iPr_def_11))),iPr_def_11)),inverse(multiply(X0,iPr_def_11)))) = multiply(iPr_def_11,multiply(inverse(inverse(X0)),iPr_def_11)),
inference(demodulation,[status(thm)],[c_20589,c_4763]) ).
tcf(c_20615,plain,
! [X0: $i] : multiply(iPr_def_11,multiply(inverse(inverse(X0)),iPr_def_11)) = inverse(multiply(iPr_def_11,inverse(multiply(X0,iPr_def_11)))),
inference(light_normalisation,[status(thm)],[c_20614,c_4522,c_4530]) ).
tcf(c_21000,plain,
multiply(iPr_def_11,multiply(inverse(inverse(multiply(iPr_def_11,multiply(inverse(inverse(multiply(b2,iPr_def_11))),iPr_def_11)))),iPr_def_11)) = inverse(multiply(iPr_def_11,inverse(b2))),
inference(superposition,[status(thm)],[c_4861,c_20615]) ).
tcf(c_21027,plain,
! [X0: $i] : multiply(multiply(iPr_def_11,multiply(inverse(inverse(X0)),iPr_def_11)),multiply(iPr_def_11,inverse(multiply(X0,iPr_def_11)))) = iPr_def_11,
inference(superposition,[status(thm)],[c_20615,c_4083]) ).
tcf(c_21063,plain,
multiply(iPr_def_11,multiply(inverse(inverse(multiply(iPr_def_11,multiply(inverse(inverse(multiply(b2,iPr_def_11))),iPr_def_11)))),iPr_def_11)) = inverse(multiply(iPr_def_11,iPr_def_10)),
inference(light_normalisation,[status(thm)],[c_21000,c_4216]) ).
tcf(c_21340,plain,
! [X0: $i] : multiply(X0,multiply(iPr_def_11,inverse(multiply(multiply(multiply(X0,iPr_def_11),iPr_def_11),iPr_def_11)))) = iPr_def_11,
inference(superposition,[status(thm)],[c_4763,c_21027]) ).
tcf(c_21610,plain,
! [X0: $i,X1: $i] : multiply(inverse(multiply(multiply(inverse(multiply(X0,iPr_def_11)),multiply(X0,iPr_def_10)),inverse(multiply(X1,iPr_def_11)))),iPr_def_10) = multiply(multiply(iPr_def_11,multiply(inverse(inverse(X1)),iPr_def_11)),iPr_def_11),
inference(light_normalisation,[status(thm)],[c_282,c_4522,c_4530,c_15853]) ).
tcf(c_21641,plain,
! [X0: $i] : multiply(inverse(multiply(multiply(inverse(multiply(X0,iPr_def_11)),multiply(X0,iPr_def_10)),inverse(iPr_def_11))),iPr_def_10) = multiply(multiply(iPr_def_11,multiply(inverse(inverse(iPr_def_11)),iPr_def_11)),iPr_def_11),
inference(superposition,[status(thm)],[c_4530,c_21610]) ).
tcf(c_21645,plain,
! [X0: $i] : multiply(multiply(iPr_def_11,multiply(inverse(inverse(multiply(iPr_def_11,multiply(inverse(inverse(multiply(b2,iPr_def_11))),iPr_def_11)))),iPr_def_11)),iPr_def_11) = multiply(inverse(multiply(multiply(inverse(multiply(X0,iPr_def_11)),multiply(X0,iPr_def_10)),inverse(b2))),iPr_def_10),
inference(superposition,[status(thm)],[c_4861,c_21610]) ).
tcf(c_21658,plain,
! [X0: $i] : multiply(inverse(multiply(multiply(inverse(multiply(X0,iPr_def_11)),multiply(X0,iPr_def_10)),iPr_def_11)),iPr_def_10) = iPr_def_11,
inference(light_normalisation,[status(thm)],[c_21641,c_4522,c_4530]) ).
tcf(c_21669,plain,
! [X0: $i] : multiply(inverse(multiply(multiply(inverse(multiply(X0,iPr_def_11)),multiply(X0,iPr_def_10)),iPr_def_10)),iPr_def_10) = multiply(iPr_def_11,multiply(inverse(iPr_def_10),iPr_def_11)),
inference(light_normalisation,[status(thm)],[c_21645,c_4216,c_16727,c_21063]) ).
tcf(c_22289,plain,
multiply(iPr_def_11,multiply(inverse(inverse(iPr_def_10)),iPr_def_11)) = inverse(multiply(iPr_def_11,inverse(iPr_def_10))),
inference(superposition,[status(thm)],[c_16456,c_16546]) ).
tcf(c_22351,plain,
inverse(multiply(inverse(iPr_def_10),iPr_def_11)) = inverse(multiply(iPr_def_11,inverse(iPr_def_10))),
inference(demodulation,[status(thm)],[c_4777,c_22289]) ).
tcf(c_22355,plain,
multiply(inverse(multiply(iPr_def_11,inverse(iPr_def_10))),iPr_def_11) = multiply(iPr_def_11,multiply(iPr_def_11,iPr_def_10)),
inference(demodulation,[status(thm)],[c_4712,c_22351]) ).
tcf(c_22356,plain,
multiply(iPr_def_11,multiply(inverse(inverse(iPr_def_10)),iPr_def_11)) = multiply(iPr_def_11,multiply(iPr_def_11,iPr_def_10)),
inference(demodulation,[status(thm)],[c_22355,c_16504]) ).
tcf(c_22411,plain,
multiply(inverse(multiply(multiply(inverse(multiply(iPr_def_11,inverse(iPr_def_10))),multiply(inverse(iPr_def_10),iPr_def_10)),iPr_def_11)),iPr_def_10) = iPr_def_11,
inference(superposition,[status(thm)],[c_22351,c_21658]) ).
tcf(c_22419,plain,
multiply(inverse(multiply(multiply(iPr_def_11,multiply(inverse(inverse(iPr_def_10)),iPr_def_11)),iPr_def_11)),iPr_def_10) = iPr_def_11,
inference(demodulation,[status(thm)],[c_22411,c_4083,c_16504]) ).
tcf(c_22420,plain,
multiply(inverse(multiply(inverse(multiply(iPr_def_11,inverse(iPr_def_10))),iPr_def_11)),iPr_def_10) = iPr_def_11,
inference(light_normalisation,[status(thm)],[c_22419,c_22289]) ).
tcf(c_22968,plain,
multiply(inverse(multiply(iPr_def_11,multiply(inverse(inverse(iPr_def_10)),iPr_def_11))),iPr_def_10) = iPr_def_11,
inference(superposition,[status(thm)],[c_16504,c_22420]) ).
tcf(c_22977,plain,
multiply(inverse(inverse(multiply(iPr_def_11,inverse(iPr_def_10)))),iPr_def_10) = iPr_def_11,
inference(light_normalisation,[status(thm)],[c_22968,c_22289]) ).
tcf(c_23046,plain,
multiply(iPr_def_11,multiply(iPr_def_11,iPr_def_10)) = inverse(multiply(iPr_def_11,inverse(iPr_def_10))),
inference(superposition,[status(thm)],[c_22356,c_22289]) ).
tcf(c_23068,plain,
multiply(inverse(multiply(iPr_def_11,multiply(iPr_def_11,iPr_def_10))),iPr_def_10) = iPr_def_11,
inference(demodulation,[status(thm)],[c_22977,c_23046]) ).
tcf(c_23071,plain,
multiply(iPr_def_11,multiply(iPr_def_11,iPr_def_10)) = inverse(multiply(inverse(iPr_def_10),iPr_def_11)),
inference(demodulation,[status(thm)],[c_22351,c_23046]) ).
tcf(c_23174,plain,
multiply(inverse(iPr_def_11),multiply(inverse(multiply(iPr_def_11,multiply(iPr_def_11,iPr_def_10))),iPr_def_11)) = multiply(iPr_def_11,multiply(inverse(iPr_def_10),iPr_def_11)),
inference(superposition,[status(thm)],[c_23068,c_16483]) ).
tcf(c_23179,plain,
multiply(iPr_def_11,multiply(inverse(multiply(iPr_def_11,multiply(iPr_def_11,iPr_def_10))),iPr_def_11)) = multiply(iPr_def_11,multiply(inverse(iPr_def_10),iPr_def_11)),
inference(light_normalisation,[status(thm)],[c_23174,c_4522]) ).
tcf(c_23229,plain,
multiply(multiply(iPr_def_11,multiply(iPr_def_11,iPr_def_10)),iPr_def_11) = multiply(iPr_def_11,multiply(inverse(inverse(iPr_def_10)),iPr_def_11)),
inference(superposition,[status(thm)],[c_23046,c_16504]) ).
tcf(c_23230,plain,
multiply(iPr_def_11,multiply(inverse(multiply(iPr_def_11,multiply(iPr_def_11,iPr_def_10))),iPr_def_11)) = multiply(iPr_def_11,multiply(inverse(inverse(inverse(iPr_def_10))),iPr_def_11)),
inference(superposition,[status(thm)],[c_23046,c_16456]) ).
tcf(c_23241,plain,
multiply(iPr_def_11,multiply(inverse(inverse(iPr_def_10)),iPr_def_11)) = iPr_def_10,
inference(light_normalisation,[status(thm)],[c_23229,c_4580]) ).
tcf(c_23243,plain,
multiply(iPr_def_11,multiply(inverse(inverse(inverse(iPr_def_10))),iPr_def_11)) = multiply(iPr_def_11,multiply(inverse(iPr_def_10),iPr_def_11)),
inference(light_normalisation,[status(thm)],[c_23230,c_23179]) ).
tcf(c_23274,plain,
multiply(iPr_def_11,multiply(iPr_def_11,iPr_def_10)) = iPr_def_10,
inference(demodulation,[status(thm)],[c_22356,c_23241]) ).
tcf(c_23275,plain,
inverse(multiply(iPr_def_11,inverse(iPr_def_10))) = iPr_def_10,
inference(demodulation,[status(thm)],[c_23046,c_23274]) ).
tcf(c_23281,plain,
multiply(iPr_def_10,iPr_def_11) = iPr_def_10,
inference(demodulation,[status(thm)],[c_4580,c_23274]) ).
tcf(c_23855,plain,
inverse(multiply(inverse(iPr_def_10),inverse(multiply(iPr_def_11,multiply(iPr_def_11,inverse(iPr_def_10)))))) = iPr_def_11,
inference(superposition,[status(thm)],[c_23275,c_5468]) ).
tcf(c_26786,plain,
inverse(multiply(inverse(iPr_def_10),iPr_def_11)) = iPr_def_10,
inference(light_normalisation,[status(thm)],[c_23071,c_23274]) ).
tcf(c_26817,plain,
! [X0: $i] : multiply(inverse(multiply(multiply(inverse(multiply(X0,iPr_def_11)),multiply(X0,iPr_def_10)),iPr_def_10)),iPr_def_10) = multiply(multiply(iPr_def_11,multiply(inverse(inverse(inverse(iPr_def_10))),iPr_def_11)),iPr_def_11),
inference(superposition,[status(thm)],[c_26786,c_21610]) ).
tcf(c_26829,plain,
multiply(iPr_def_11,multiply(inverse(inverse(inverse(iPr_def_10))),iPr_def_11)) = inverse(multiply(iPr_def_11,iPr_def_10)),
inference(superposition,[status(thm)],[c_26786,c_20615]) ).
tcf(c_26831,plain,
multiply(inverse(inverse(iPr_def_10)),multiply(multiply(iPr_def_11,multiply(inverse(iPr_def_10),iPr_def_11)),iPr_def_11)) = iPr_def_11,
inference(superposition,[status(thm)],[c_26786,c_16537]) ).
tcf(c_26841,plain,
multiply(multiply(iPr_def_11,multiply(inverse(iPr_def_10),iPr_def_11)),iPr_def_11) = multiply(iPr_def_11,multiply(inverse(iPr_def_10),iPr_def_11)),
inference(light_normalisation,[status(thm)],[c_26817,c_21669,c_23243]) ).
tcf(c_34993,plain,
multiply(iPr_def_11,multiply(inverse(inverse(multiply(iPr_def_11,multiply(iPr_def_11,inverse(iPr_def_10))))),iPr_def_11)) = multiply(iPr_def_11,multiply(inverse(iPr_def_10),iPr_def_11)),
inference(superposition,[status(thm)],[c_23855,c_15853]) ).
tcf(c_35012,plain,
multiply(iPr_def_11,multiply(inverse(inverse(inverse(iPr_def_10))),iPr_def_11)) = multiply(iPr_def_11,multiply(inverse(iPr_def_10),iPr_def_11)),
inference(demodulation,[status(thm)],[c_34993,c_16456]) ).
tcf(c_35013,plain,
multiply(iPr_def_11,multiply(inverse(iPr_def_10),iPr_def_11)) = inverse(multiply(iPr_def_11,iPr_def_10)),
inference(light_normalisation,[status(thm)],[c_35012,c_26829]) ).
tcf(c_35101,plain,
multiply(inverse(multiply(iPr_def_11,iPr_def_10)),iPr_def_11) = inverse(multiply(iPr_def_11,iPr_def_10)),
inference(demodulation,[status(thm)],[c_16727,c_35013]) ).
tcf(c_35102,plain,
! [X0: $i] : multiply(inverse(multiply(X0,iPr_def_10)),multiply(X0,iPr_def_11)) = inverse(multiply(iPr_def_11,iPr_def_10)),
inference(demodulation,[status(thm)],[c_16483,c_35013]) ).
tcf(c_54526,plain,
multiply(inverse(inverse(iPr_def_10)),inverse(multiply(iPr_def_11,iPr_def_10))) = iPr_def_11,
inference(light_normalisation,[status(thm)],[c_26831,c_26841,c_35013]) ).
tcf(c_55469,plain,
! [X0: $i,X1: $i] : multiply(multiply(multiply(iPr_def_11,multiply(inverse(inverse(X0)),inverse(inverse(multiply(inverse(X1),X1))))),inverse(multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(multiply(inverse(X1),X1))))),inverse(multiply(inverse(X1),X1))) = multiply(iPr_def_11,X0),
inference(superposition,[status(thm)],[c_5468,c_297]) ).
tcf(c_55509,plain,
! [X0: $i] : multiply(multiply(multiply(inverse(iPr_def_11),multiply(inverse(inverse(iPr_def_10)),inverse(inverse(multiply(inverse(X0),X0))))),inverse(multiply(inverse(inverse(multiply(inverse(X0),X0))),inverse(multiply(inverse(X0),X0))))),inverse(multiply(inverse(X0),X0))) = multiply(iPr_def_11,iPr_def_10),
inference(superposition,[status(thm)],[c_54526,c_297]) ).
tcf(c_55513,plain,
! [X0: $i,X1: $i] : multiply(multiply(multiply(inverse(multiply(X0,iPr_def_10)),multiply(X0,inverse(inverse(multiply(inverse(X1),X1))))),inverse(multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(multiply(inverse(X1),X1))))),inverse(multiply(inverse(X1),X1))) = b2,
inference(superposition,[status(thm)],[c_4216,c_297]) ).
tcf(c_55794,plain,
! [X0: $i] : multiply(multiply(multiply(inverse(multiply(X0,iPr_def_10)),multiply(X0,inverse(inverse(iPr_def_11)))),inverse(iPr_def_11)),inverse(iPr_def_11)) = b2,
inference(demodulation,[status(thm)],[c_55513,c_4083]) ).
tcf(c_55795,plain,
inverse(multiply(iPr_def_11,iPr_def_10)) = b2,
inference(light_normalisation,[status(thm)],[c_55794,c_4522,c_35101,c_35102]) ).
tcf(c_55812,plain,
! [X0: $i] : multiply(multiply(multiply(iPr_def_11,multiply(inverse(inverse(X0)),inverse(inverse(iPr_def_11)))),inverse(iPr_def_11)),inverse(iPr_def_11)) = multiply(iPr_def_11,X0),
inference(demodulation,[status(thm)],[c_55469,c_4083]) ).
tcf(c_55813,plain,
! [X0: $i] : multiply(multiply(iPr_def_11,multiply(inverse(inverse(multiply(X0,iPr_def_11))),iPr_def_11)),iPr_def_11) = multiply(iPr_def_11,X0),
inference(light_normalisation,[status(thm)],[c_55812,c_4522,c_4751,c_4757]) ).
tcf(c_55816,plain,
multiply(multiply(multiply(inverse(iPr_def_11),multiply(inverse(inverse(iPr_def_10)),inverse(inverse(iPr_def_11)))),inverse(iPr_def_11)),inverse(iPr_def_11)) = multiply(iPr_def_11,iPr_def_10),
inference(demodulation,[status(thm)],[c_55509,c_4083]) ).
tcf(c_55817,plain,
multiply(iPr_def_11,iPr_def_10) = iPr_def_10,
inference(light_normalisation,[status(thm)],[c_55816,c_4522,c_23241,c_23281]) ).
tcf(c_56469,plain,
multiply(b2,iPr_def_11) = b2,
inference(demodulation,[status(thm)],[c_35101,c_55795]) ).
tcf(c_56471,plain,
multiply(iPr_def_11,multiply(inverse(iPr_def_10),iPr_def_11)) = b2,
inference(demodulation,[status(thm)],[c_35013,c_55795]) ).
tcf(c_56682,plain,
multiply(b2,multiply(iPr_def_11,inverse(b2))) = iPr_def_11,
inference(superposition,[status(thm)],[c_56469,c_21340]) ).
tcf(c_56684,plain,
multiply(iPr_def_11,multiply(inverse(inverse(b2)),iPr_def_11)) = inverse(multiply(iPr_def_11,inverse(b2))),
inference(superposition,[status(thm)],[c_56469,c_20615]) ).
tcf(c_56690,plain,
multiply(b2,iPr_def_10) = iPr_def_11,
inference(light_normalisation,[status(thm)],[c_56682,c_4216,c_55817]) ).
tcf(c_56693,plain,
inverse(iPr_def_10) = b2,
inference(light_normalisation,[status(thm)],[c_56684,c_4216,c_55817,c_56471]) ).
tcf(c_56742,plain,
! [X0: $i,X1: $i] : multiply(multiply(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(inverse(multiply(b2,iPr_def_10))))),inverse(multiply(inverse(inverse(multiply(b2,iPr_def_10))),inverse(multiply(b2,iPr_def_10))))),inverse(multiply(b2,iPr_def_10))) = X1,
inference(superposition,[status(thm)],[c_56693,c_297]) ).
tcf(c_56763,plain,
! [X0: $i,X1: $i] : multiply(multiply(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(inverse(multiply(b2,iPr_def_10))))),inverse(iPr_def_11)),inverse(multiply(b2,iPr_def_10))) = X1,
inference(demodulation,[status(thm)],[c_56742,c_4083]) ).
tcf(c_56764,plain,
! [X0: $i] : multiply(multiply(multiply(iPr_def_11,multiply(inverse(inverse(X0)),iPr_def_11)),iPr_def_11),iPr_def_11) = X0,
inference(light_normalisation,[status(thm)],[c_56763,c_4522,c_15853,c_56690]) ).
tcf(c_56765,plain,
! [X0: $i] : multiply(iPr_def_11,X0) = X0,
inference(light_normalisation,[status(thm)],[c_56764,c_4751,c_4757,c_55813]) ).
tcf(c_56781,plain,
a2 = iPr_def_12,
inference(demodulation,[status(thm)],[c_64,c_56765]) ).
tcf(c_56807,plain,
iPr_def_12 != iPr_def_12,
inference(demodulation,[status(thm)],[c_65,c_56781]) ).
tcf(c_56808,plain,
$false,
inference(equality_resolution_simp,[status(thm)],[c_56807]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : GRP410-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.02 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.04/0.31 % Computer : n012.cluster.edu
% 0.04/0.31 % Model : x86_64 x86_64
% 0.04/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.04/0.31 % Memory : 8046.5625MB
% 0.04/0.31 % OS : Linux 6.8.0-71-generic
% 0.04/0.31 % CPULimit : 300
% 0.04/0.31 % WCLimit : 300
% 0.04/0.31 % DateTime : Wed Sep 23 14:41:07 UTC 2026
% 0.04/0.31 % CPUTime :
% 0.04/0.31 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.04/0.32 Running UEQ theorem proving
% 0.04/0.32 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.06/0.33
% 0.06/0.33 % ======== iProver multi-core TPTP/SMT =========
% 0.06/0.33
% 0.06/0.33 % Detected problem language: tptp
% 0.06/0.34 % Proving...
% 43.48/7.00 WARNING - Clausifier option not provided in the heuristic config "heur/vip2_118404", setting default options.
% 43.48/7.00 % SZS status Started for theBenchmark.p
% 43.48/7.00 % SZS status Unsatisfiable for theBenchmark.p
% 43.48/7.00
% 43.48/7.00 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 43.48/7.00
% 43.48/7.00 % ------ iProver source info
% 43.48/7.00
% 43.48/7.00 % git: date: 2026-07-19 20:42:38 +0200
% 43.48/7.00 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 43.48/7.00 % git: non_committed_changes: false
% 43.48/7.00
% 43.48/7.00 % ------ Parsing...% successful
% 43.48/7.00
% 43.48/7.00
% 43.48/7.00 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 43.48/7.00
% 43.48/7.00 % ------ Preprocessing... sup_sim: 0 sf_s rm: 0 0s sf_e pe_s pe_e %
% 43.48/7.00
% 43.48/7.00 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 43.48/7.00
% 43.48/7.00 % ------ Preprocessing... sf_s rm: 0 0s sf_e
% 43.48/7.00 % ------ Proving...
% 43.48/7.00 % ------ Problem Properties
% 43.48/7.00
% 43.48/7.00 %
% 43.48/7.00 % clauses 5
% 43.48/7.00 % conjectures 1
% 43.48/7.00 % EPR 1
% 43.48/7.00 % Horn 5
% 43.48/7.00 % unary 5
% 43.48/7.00 % binary 0
% 43.48/7.00 % lits 5
% 43.48/7.00 % lits eq 5
% 43.48/7.00 % fd_pure 0
% 43.48/7.00 % fd_pseudo 0
% 43.48/7.00 % fd_cond 0
% 43.48/7.00 % fd_pseudo_cond 0
% 43.48/7.00 % AC symbols 0
% 43.48/7.00
% 43.48/7.00 % ------ Input Options Time Limit: Unbounded
% 43.48/7.00
% 43.48/7.00
% 43.48/7.00 % ------
% 43.48/7.00 % Current options:
% 43.48/7.00 % ------
% 43.48/7.00
% 43.48/7.00
% 43.48/7.00 %
% 43.48/7.00
% 43.48/7.00 % ------ Proving...
% 43.48/7.00 %
% 43.48/7.00
% 43.48/7.00 % SZS status Unsatisfiable for theBenchmark.p
% 43.48/7.00
% 43.48/7.00 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 43.48/7.00
% 43.48/7.00
%------------------------------------------------------------------------------