%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : GRP443-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 : n018.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 01:34:07 PM UTC 2026
% Result : Unsatisfiable 3.90s 2.29s
% Output : CNFRefutation 3.90s
% Verified :
% SZS Type : Refutation
% Derivation depth : 59
% Number of leaves : 5
% Syntax : Number of formulae : 221 ( 221 unt; 3 def)
% Number of atoms : 838 ( 220 equ)
% Maximal formula atoms : 1 ( 3 avg)
% Number of connectives : 4 ( 4 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 2 avg)
% Maximal term depth : 12 ( 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 : 227 ( 0 sgn 227 !; 0 ?; 223 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X2,X3,X0,X1] : inverse(multiply(X0,multiply(X1,multiply(multiply(X2,inverse(X2)),inverse(multiply(X3,multiply(X0,X1))))))) = X3,
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,X3: $i] : inverse(multiply(X0,multiply(X1,multiply(multiply(X2,inverse(X2)),inverse(multiply(X3,multiply(X0,X1))))))) = X3,
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_66,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : inverse(multiply(X0,multiply(X1,multiply(multiply(X2,inverse(X2)),inverse(multiply(X3,multiply(X0,X1))))))) = X3,
inference(demodulation,[status(thm)],[c_51]) ).
tcf(c_103,plain,
! [X0: $i,X1: $i,X2: $i] : inverse(multiply(X0,multiply(X1,multiply(multiply(b2,iPr_def_10),inverse(multiply(X2,multiply(X0,X1))))))) = X2,
inference(superposition,[status(thm)],[c_62,c_66]) ).
tcf(c_105,plain,
! [X0: $i,X1: $i] : inverse(multiply(iPr_def_10,multiply(b2,multiply(multiply(X0,inverse(X0)),inverse(multiply(X1,iPr_def_11)))))) = X1,
inference(superposition,[status(thm)],[c_63,c_66]) ).
tcf(c_108,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] : inverse(multiply(X0,multiply(multiply(multiply(X1,inverse(X1)),inverse(multiply(X2,multiply(X3,X0)))),multiply(multiply(X4,inverse(X4)),X2)))) = X3,
inference(superposition,[status(thm)],[c_66,c_66]) ).
tcf(c_145,plain,
! [X0: $i] : inverse(multiply(iPr_def_10,multiply(b2,multiply(multiply(b2,iPr_def_10),inverse(multiply(X0,iPr_def_11)))))) = X0,
inference(superposition,[status(thm)],[c_63,c_103]) ).
tcf(c_146,plain,
! [X0: $i] : inverse(multiply(iPr_def_11,multiply(a2,multiply(multiply(b2,iPr_def_10),inverse(multiply(X0,iPr_def_12)))))) = X0,
inference(superposition,[status(thm)],[c_64,c_103]) ).
tcf(c_151,plain,
! [X0: $i,X1: $i,X2: $i] : inverse(multiply(X0,multiply(multiply(multiply(b2,iPr_def_10),inverse(multiply(X1,multiply(X2,X0)))),multiply(multiply(b2,iPr_def_10),X1)))) = X2,
inference(superposition,[status(thm)],[c_103,c_103]) ).
tcf(c_153,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : inverse(multiply(X0,multiply(multiply(multiply(b2,iPr_def_10),inverse(multiply(X1,multiply(X2,X0)))),multiply(multiply(X3,inverse(X3)),X1)))) = X2,
inference(superposition,[status(thm)],[c_62,c_108]) ).
tcf(c_529,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] : inverse(multiply(multiply(multiply(X0,inverse(X0)),X1),multiply(multiply(multiply(b2,iPr_def_10),X2),multiply(multiply(b2,iPr_def_10),X3)))) = multiply(multiply(X4,inverse(X4)),inverse(multiply(X1,multiply(X2,X3)))),
inference(superposition,[status(thm)],[c_108,c_151]) ).
tcf(c_534,plain,
! [X0: $i] : inverse(multiply(multiply(multiply(b2,iPr_def_10),inverse(multiply(X0,iPr_def_12))),multiply(multiply(multiply(b2,iPr_def_10),X0),multiply(multiply(b2,iPr_def_10),iPr_def_11)))) = a2,
inference(superposition,[status(thm)],[c_146,c_151]) ).
tcf(c_539,plain,
! [X0: $i] : inverse(multiply(b2,multiply(multiply(multiply(b2,iPr_def_10),inverse(multiply(X0,iPr_def_11))),multiply(multiply(b2,iPr_def_10),X0)))) = iPr_def_10,
inference(superposition,[status(thm)],[c_63,c_151]) ).
tcf(c_540,plain,
! [X0: $i] : inverse(multiply(a2,multiply(multiply(multiply(b2,iPr_def_10),inverse(multiply(X0,iPr_def_12))),multiply(multiply(b2,iPr_def_10),X0)))) = iPr_def_11,
inference(superposition,[status(thm)],[c_64,c_151]) ).
tcf(c_558,plain,
! [X0: $i,X1: $i,X2: $i] : inverse(multiply(multiply(multiply(b2,iPr_def_10),X0),multiply(multiply(multiply(b2,iPr_def_10),X1),multiply(multiply(b2,iPr_def_10),X2)))) = multiply(multiply(b2,iPr_def_10),inverse(multiply(X0,multiply(X1,X2)))),
inference(superposition,[status(thm)],[c_151,c_151]) ).
tcf(c_643,plain,
! [X0: $i,X1: $i] : inverse(multiply(b2,multiply(multiply(multiply(b2,iPr_def_10),inverse(multiply(X0,iPr_def_11))),multiply(multiply(X1,inverse(X1)),X0)))) = iPr_def_10,
inference(superposition,[status(thm)],[c_63,c_153]) ).
tcf(c_678,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : inverse(multiply(multiply(multiply(X0,inverse(X0)),X1),multiply(multiply(multiply(b2,iPr_def_10),X2),multiply(multiply(b2,iPr_def_10),X3)))) = multiply(multiply(b2,iPr_def_10),inverse(multiply(X1,multiply(X2,X3)))),
inference(superposition,[status(thm)],[c_153,c_151]) ).
tcf(c_680,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : multiply(multiply(X0,inverse(X0)),inverse(multiply(X1,multiply(X2,X3)))) = multiply(multiply(b2,iPr_def_10),inverse(multiply(X1,multiply(X2,X3)))),
inference(demodulation,[status(thm)],[c_529,c_678]) ).
tcf(c_1188,plain,
! [X0: $i,X1: $i] : multiply(multiply(X0,inverse(X0)),X1) = multiply(multiply(b2,iPr_def_10),X1),
inference(superposition,[status(thm)],[c_153,c_680]) ).
tcf(c_1209,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] : inverse(multiply(inverse(multiply(X0,multiply(X1,X2))),multiply(multiply(multiply(b2,iPr_def_10),inverse(multiply(X3,multiply(multiply(b2,iPr_def_10),inverse(multiply(X0,multiply(X1,X2))))))),multiply(multiply(b2,iPr_def_10),X3)))) = multiply(X4,inverse(X4)),
inference(superposition,[status(thm)],[c_680,c_151]) ).
tcf(c_1336,plain,
! [X0: $i] : multiply(X0,inverse(X0)) = multiply(b2,iPr_def_10),
inference(demodulation,[status(thm)],[c_1209,c_151]) ).
tcf(c_1430,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(multiply(X0,multiply(X1,multiply(multiply(b2,iPr_def_10),inverse(multiply(X2,multiply(X0,X1)))))),X2) = multiply(b2,iPr_def_10),
inference(superposition,[status(thm)],[c_103,c_1336]) ).
tcf(c_1436,plain,
! [X0: $i] : multiply(multiply(iPr_def_11,multiply(a2,multiply(multiply(b2,iPr_def_10),inverse(multiply(X0,iPr_def_12))))),X0) = multiply(b2,iPr_def_10),
inference(superposition,[status(thm)],[c_146,c_1336]) ).
tcf(c_1453,plain,
! [X0: $i,X1: $i] : inverse(multiply(X0,multiply(inverse(X0),multiply(multiply(b2,iPr_def_10),inverse(multiply(X1,multiply(b2,iPr_def_10))))))) = X1,
inference(superposition,[status(thm)],[c_1336,c_103]) ).
tcf(c_1901,plain,
inverse(multiply(iPr_def_11,multiply(a2,multiply(multiply(b2,iPr_def_10),inverse(multiply(b2,iPr_def_10)))))) = multiply(iPr_def_11,multiply(a2,multiply(multiply(b2,iPr_def_10),inverse(multiply(iPr_def_12,iPr_def_12))))),
inference(superposition,[status(thm)],[c_1436,c_146]) ).
tcf(c_1961,plain,
! [X0: $i,X1: $i] : inverse(multiply(multiply(multiply(b2,iPr_def_10),inverse(multiply(X0,multiply(b2,iPr_def_10)))),multiply(multiply(multiply(b2,iPr_def_10),X0),multiply(multiply(b2,iPr_def_10),X1)))) = inverse(X1),
inference(superposition,[status(thm)],[c_1453,c_151]) ).
tcf(c_1993,plain,
! [X0: $i,X1: $i] : multiply(multiply(X0,multiply(inverse(X0),multiply(multiply(b2,iPr_def_10),inverse(multiply(X1,multiply(b2,iPr_def_10)))))),X1) = multiply(b2,iPr_def_10),
inference(superposition,[status(thm)],[c_1336,c_1430]) ).
tcf(c_2022,plain,
! [X0: $i,X1: $i] : multiply(X0,multiply(X1,multiply(multiply(b2,iPr_def_10),inverse(multiply(iPr_def_11,multiply(X0,X1)))))) = inverse(multiply(iPr_def_10,multiply(b2,multiply(multiply(b2,iPr_def_10),inverse(multiply(b2,iPr_def_10)))))),
inference(superposition,[status(thm)],[c_1430,c_145]) ).
tcf(c_2092,plain,
! [X0: $i,X1: $i] : multiply(multiply(b2,iPr_def_10),inverse(multiply(inverse(multiply(X0,multiply(b2,iPr_def_10))),multiply(X0,X1)))) = inverse(X1),
inference(demodulation,[status(thm)],[c_1961,c_558]) ).
tcf(c_2093,plain,
multiply(iPr_def_11,multiply(a2,multiply(multiply(b2,iPr_def_10),inverse(multiply(iPr_def_12,iPr_def_12))))) = inverse(multiply(iPr_def_11,multiply(a2,multiply(b2,iPr_def_10)))),
inference(demodulation,[status(thm)],[c_1901,c_1336]) ).
tcf(c_2103,plain,
! [X0: $i,X1: $i] : multiply(X0,multiply(X1,multiply(multiply(b2,iPr_def_10),inverse(multiply(iPr_def_11,multiply(X0,X1)))))) = inverse(multiply(iPr_def_10,multiply(b2,multiply(b2,iPr_def_10)))),
inference(demodulation,[status(thm)],[c_2022,c_1336]) ).
tcf(c_2634,plain,
multiply(multiply(b2,iPr_def_10),inverse(multiply(inverse(multiply(iPr_def_10,multiply(b2,iPr_def_10))),iPr_def_11))) = inverse(b2),
inference(superposition,[status(thm)],[c_63,c_2092]) ).
tcf(c_2635,plain,
multiply(multiply(b2,iPr_def_10),inverse(multiply(inverse(multiply(iPr_def_11,multiply(b2,iPr_def_10))),iPr_def_12))) = inverse(a2),
inference(superposition,[status(thm)],[c_64,c_2092]) ).
tcf(c_2636,plain,
! [X0: $i] : multiply(multiply(b2,iPr_def_10),inverse(multiply(inverse(multiply(X0,multiply(b2,iPr_def_10))),multiply(b2,iPr_def_10)))) = inverse(inverse(X0)),
inference(superposition,[status(thm)],[c_1336,c_2092]) ).
tcf(c_2664,plain,
! [X0: $i] : inverse(multiply(X0,multiply(inverse(X0),inverse(iPr_def_10)))) = inverse(multiply(b2,multiply(b2,iPr_def_10))),
inference(superposition,[status(thm)],[c_2092,c_1453]) ).
tcf(c_3016,plain,
! [X0: $i] : inverse(multiply(a2,multiply(multiply(multiply(b2,iPr_def_10),inverse(multiply(b2,iPr_def_10))),multiply(multiply(b2,iPr_def_10),multiply(X0,multiply(inverse(X0),multiply(multiply(b2,iPr_def_10),inverse(multiply(iPr_def_12,multiply(b2,iPr_def_10)))))))))) = iPr_def_11,
inference(superposition,[status(thm)],[c_1993,c_540]) ).
tcf(c_3017,plain,
! [X0: $i] : multiply(X0,multiply(inverse(X0),multiply(multiply(b2,iPr_def_10),inverse(multiply(iPr_def_12,multiply(b2,iPr_def_10)))))) = inverse(multiply(iPr_def_11,multiply(a2,multiply(multiply(b2,iPr_def_10),inverse(multiply(b2,iPr_def_10)))))),
inference(superposition,[status(thm)],[c_1993,c_146]) ).
tcf(c_3045,plain,
inverse(inverse(multiply(iPr_def_11,multiply(a2,multiply(b2,iPr_def_10))))) = iPr_def_12,
inference(superposition,[status(thm)],[c_2093,c_146]) ).
tcf(c_3050,plain,
multiply(multiply(b2,iPr_def_10),inverse(multiply(inverse(multiply(iPr_def_10,multiply(b2,iPr_def_10))),iPr_def_11))) = iPr_def_10,
inference(demodulation,[status(thm)],[c_2634,c_62]) ).
tcf(c_3060,plain,
! [X0: $i] : multiply(X0,multiply(inverse(X0),multiply(multiply(b2,iPr_def_10),inverse(multiply(iPr_def_12,multiply(b2,iPr_def_10)))))) = inverse(multiply(iPr_def_11,multiply(a2,multiply(b2,iPr_def_10)))),
inference(demodulation,[status(thm)],[c_3017,c_1336]) ).
tcf(c_3098,plain,
inverse(multiply(a2,multiply(multiply(multiply(b2,iPr_def_10),inverse(multiply(b2,iPr_def_10))),multiply(multiply(b2,iPr_def_10),inverse(multiply(iPr_def_11,multiply(a2,multiply(b2,iPr_def_10)))))))) = iPr_def_11,
inference(demodulation,[status(thm)],[c_3016,c_3060]) ).
tcf(c_3099,plain,
inverse(inverse(multiply(iPr_def_10,multiply(b2,multiply(b2,iPr_def_10))))) = iPr_def_11,
inference(demodulation,[status(thm)],[c_3098,c_1188,c_2103]) ).
tcf(c_3659,plain,
! [X0: $i] : inverse(multiply(b2,multiply(iPr_def_10,inverse(inverse(X0))))) = inverse(multiply(X0,multiply(b2,iPr_def_10))),
inference(superposition,[status(thm)],[c_2636,c_103]) ).
tcf(c_3676,plain,
! [X0: $i,X1: $i] : inverse(multiply(X0,multiply(inverse(X0),inverse(inverse(X1))))) = inverse(multiply(X1,multiply(b2,iPr_def_10))),
inference(superposition,[status(thm)],[c_2636,c_1453]) ).
tcf(c_4074,plain,
inverse(multiply(multiply(iPr_def_11,multiply(a2,multiply(b2,iPr_def_10))),multiply(b2,iPr_def_10))) = inverse(multiply(b2,multiply(iPr_def_10,iPr_def_12))),
inference(superposition,[status(thm)],[c_3045,c_3659]) ).
tcf(c_4075,plain,
inverse(multiply(multiply(iPr_def_10,multiply(b2,multiply(b2,iPr_def_10))),multiply(b2,iPr_def_10))) = inverse(multiply(b2,multiply(iPr_def_10,iPr_def_11))),
inference(superposition,[status(thm)],[c_3099,c_3659]) ).
tcf(c_4085,plain,
! [X0: $i] : inverse(multiply(multiply(iPr_def_11,multiply(a2,multiply(multiply(b2,iPr_def_10),inverse(multiply(X0,iPr_def_12))))),multiply(b2,iPr_def_10))) = inverse(multiply(b2,multiply(iPr_def_10,inverse(X0)))),
inference(superposition,[status(thm)],[c_146,c_3659]) ).
tcf(c_4266,plain,
! [X0: $i] : inverse(multiply(multiply(iPr_def_11,multiply(a2,multiply(b2,iPr_def_10))),multiply(b2,iPr_def_10))) = inverse(multiply(X0,multiply(inverse(X0),iPr_def_12))),
inference(superposition,[status(thm)],[c_3045,c_3676]) ).
tcf(c_4267,plain,
! [X0: $i] : inverse(multiply(multiply(iPr_def_10,multiply(b2,multiply(b2,iPr_def_10))),multiply(b2,iPr_def_10))) = inverse(multiply(X0,multiply(inverse(X0),iPr_def_11))),
inference(superposition,[status(thm)],[c_3099,c_3676]) ).
tcf(c_4277,plain,
! [X0: $i,X1: $i] : inverse(multiply(multiply(iPr_def_11,multiply(a2,multiply(multiply(b2,iPr_def_10),inverse(multiply(X0,iPr_def_12))))),multiply(b2,iPr_def_10))) = inverse(multiply(X1,multiply(inverse(X1),inverse(X0)))),
inference(superposition,[status(thm)],[c_146,c_3676]) ).
tcf(c_4335,plain,
! [X0: $i,X1: $i] : inverse(multiply(inverse(X0),multiply(inverse(inverse(X1)),multiply(multiply(b2,iPr_def_10),inverse(multiply(X1,multiply(b2,iPr_def_10))))))) = X0,
inference(superposition,[status(thm)],[c_3676,c_103]) ).
tcf(c_4340,plain,
! [X0: $i] : inverse(multiply(X0,multiply(inverse(X0),iPr_def_11))) = inverse(multiply(b2,multiply(iPr_def_10,iPr_def_11))),
inference(demodulation,[status(thm)],[c_4267,c_4075]) ).
tcf(c_4341,plain,
! [X0: $i] : inverse(multiply(X0,multiply(inverse(X0),iPr_def_12))) = inverse(multiply(b2,multiply(iPr_def_10,iPr_def_12))),
inference(demodulation,[status(thm)],[c_4266,c_4074]) ).
tcf(c_4359,plain,
! [X0: $i,X1: $i] : inverse(multiply(X0,multiply(inverse(X0),inverse(X1)))) = inverse(multiply(b2,multiply(iPr_def_10,inverse(X1)))),
inference(demodulation,[status(thm)],[c_4277,c_4085]) ).
tcf(c_4986,plain,
! [X0: $i] : inverse(multiply(inverse(X0),multiply(iPr_def_11,multiply(multiply(b2,iPr_def_10),inverse(multiply(b2,multiply(iPr_def_10,iPr_def_11))))))) = X0,
inference(superposition,[status(thm)],[c_4340,c_103]) ).
tcf(c_5062,plain,
! [X0: $i] : inverse(multiply(inverse(X0),multiply(iPr_def_12,multiply(multiply(b2,iPr_def_10),inverse(multiply(b2,multiply(iPr_def_10,iPr_def_12))))))) = X0,
inference(superposition,[status(thm)],[c_4341,c_103]) ).
tcf(c_5132,plain,
! [X0: $i,X1: $i] : inverse(multiply(X0,multiply(inverse(X0),X1))) = inverse(multiply(b2,multiply(iPr_def_10,X1))),
inference(superposition,[status(thm)],[c_1453,c_4359]) ).
tcf(c_5661,plain,
! [X0: $i] : inverse(multiply(inverse(multiply(X0,multiply(b2,iPr_def_10))),multiply(iPr_def_12,multiply(multiply(b2,iPr_def_10),inverse(multiply(b2,multiply(iPr_def_10,iPr_def_12))))))) = multiply(b2,multiply(iPr_def_10,inverse(inverse(X0)))),
inference(superposition,[status(thm)],[c_3659,c_5062]) ).
tcf(c_5787,plain,
! [X0: $i] : multiply(b2,multiply(iPr_def_10,inverse(inverse(X0)))) = multiply(X0,multiply(b2,iPr_def_10)),
inference(demodulation,[status(thm)],[c_5661,c_5062]) ).
tcf(c_6345,plain,
! [X0: $i,X1: $i] : inverse(multiply(inverse(multiply(b2,multiply(iPr_def_10,X0))),multiply(iPr_def_11,multiply(multiply(b2,iPr_def_10),inverse(multiply(b2,multiply(iPr_def_10,iPr_def_11))))))) = multiply(X1,multiply(inverse(X1),X0)),
inference(superposition,[status(thm)],[c_5132,c_4986]) ).
tcf(c_6374,plain,
! [X0: $i,X1: $i] : inverse(multiply(inverse(X0),multiply(X1,multiply(multiply(b2,iPr_def_10),inverse(multiply(b2,multiply(iPr_def_10,X1))))))) = X0,
inference(superposition,[status(thm)],[c_5132,c_103]) ).
tcf(c_6466,plain,
! [X0: $i] : inverse(multiply(inverse(X0),multiply(inverse(inverse(multiply(iPr_def_11,multiply(a2,multiply(multiply(b2,iPr_def_10),inverse(multiply(multiply(b2,iPr_def_10),iPr_def_12))))))),multiply(multiply(b2,iPr_def_10),inverse(multiply(b2,iPr_def_10)))))) = X0,
inference(superposition,[status(thm)],[c_1436,c_4335]) ).
tcf(c_6542,plain,
! [X0: $i,X1: $i] : multiply(X0,multiply(inverse(X0),X1)) = multiply(b2,multiply(iPr_def_10,X1)),
inference(demodulation,[status(thm)],[c_6345,c_6374]) ).
tcf(c_6591,plain,
! [X0: $i] : inverse(multiply(inverse(X0),multiply(inverse(multiply(b2,iPr_def_10)),multiply(b2,iPr_def_10)))) = X0,
inference(demodulation,[status(thm)],[c_6466,c_146,c_1336]) ).
tcf(c_6831,plain,
! [X0: $i] : inverse(multiply(inverse(X0),multiply(b2,multiply(multiply(b2,iPr_def_10),inverse(multiply(b2,iPr_def_11)))))) = X0,
inference(superposition,[status(thm)],[c_63,c_6374]) ).
tcf(c_7106,plain,
inverse(multiply(iPr_def_10,multiply(inverse(multiply(b2,iPr_def_10)),multiply(b2,iPr_def_10)))) = b2,
inference(superposition,[status(thm)],[c_62,c_6591]) ).
tcf(c_7112,plain,
! [X0: $i] : multiply(iPr_def_10,multiply(b2,multiply(multiply(b2,iPr_def_10),inverse(multiply(X0,iPr_def_11))))) = inverse(multiply(X0,multiply(inverse(multiply(b2,iPr_def_10)),multiply(b2,iPr_def_10)))),
inference(superposition,[status(thm)],[c_145,c_6591]) ).
tcf(c_7114,plain,
! [X0: $i] : multiply(iPr_def_11,multiply(a2,multiply(multiply(b2,iPr_def_10),inverse(multiply(X0,iPr_def_12))))) = inverse(multiply(X0,multiply(inverse(multiply(b2,iPr_def_10)),multiply(b2,iPr_def_10)))),
inference(superposition,[status(thm)],[c_146,c_6591]) ).
tcf(c_7121,plain,
! [X0: $i] : multiply(b2,multiply(multiply(multiply(b2,iPr_def_10),inverse(multiply(X0,iPr_def_11))),multiply(multiply(b2,iPr_def_10),X0))) = inverse(multiply(iPr_def_10,multiply(inverse(multiply(b2,iPr_def_10)),multiply(b2,iPr_def_10)))),
inference(superposition,[status(thm)],[c_539,c_6591]) ).
tcf(c_7162,plain,
! [X0: $i] : multiply(multiply(inverse(X0),multiply(inverse(multiply(b2,iPr_def_10)),multiply(b2,iPr_def_10))),X0) = multiply(b2,iPr_def_10),
inference(superposition,[status(thm)],[c_6591,c_1336]) ).
tcf(c_7169,plain,
! [X0: $i,X1: $i] : inverse(multiply(iPr_def_10,multiply(b2,multiply(multiply(multiply(inverse(X0),multiply(inverse(multiply(b2,iPr_def_10)),multiply(b2,iPr_def_10))),X0),inverse(multiply(X1,iPr_def_11)))))) = X1,
inference(superposition,[status(thm)],[c_6591,c_105]) ).
tcf(c_7176,plain,
! [X0: $i,X1: $i] : inverse(multiply(b2,multiply(multiply(multiply(b2,iPr_def_10),inverse(multiply(X0,iPr_def_11))),multiply(multiply(multiply(inverse(X1),multiply(inverse(multiply(b2,iPr_def_10)),multiply(b2,iPr_def_10))),X1),X0)))) = iPr_def_10,
inference(superposition,[status(thm)],[c_6591,c_643]) ).
tcf(c_7183,plain,
! [X0: $i] : inverse(multiply(inverse(multiply(b2,iPr_def_10)),multiply(multiply(b2,iPr_def_10),multiply(multiply(b2,iPr_def_10),X0)))) = inverse(X0),
inference(superposition,[status(thm)],[c_6591,c_103]) ).
tcf(c_7188,plain,
multiply(multiply(b2,iPr_def_10),multiply(inverse(multiply(b2,iPr_def_10)),multiply(b2,iPr_def_10))) = inverse(multiply(b2,iPr_def_10)),
inference(superposition,[status(thm)],[c_6591,c_2092]) ).
tcf(c_7189,plain,
multiply(b2,multiply(iPr_def_10,multiply(b2,iPr_def_10))) = inverse(multiply(b2,iPr_def_10)),
inference(demodulation,[status(thm)],[c_7188,c_6542]) ).
tcf(c_7207,plain,
! [X0: $i] : inverse(inverse(multiply(X0,multiply(inverse(multiply(b2,iPr_def_10)),multiply(b2,iPr_def_10))))) = X0,
inference(demodulation,[status(thm)],[c_7169,c_7112,c_7162]) ).
tcf(c_7242,plain,
! [X0: $i] : multiply(b2,multiply(multiply(multiply(b2,iPr_def_10),inverse(multiply(X0,iPr_def_11))),multiply(multiply(b2,iPr_def_10),X0))) = b2,
inference(demodulation,[status(thm)],[c_7121,c_7106]) ).
tcf(c_7252,plain,
inverse(b2) = iPr_def_10,
inference(demodulation,[status(thm)],[c_7176,c_7162,c_7242]) ).
tcf(c_7666,plain,
multiply(multiply(iPr_def_10,multiply(inverse(multiply(b2,iPr_def_10)),multiply(b2,iPr_def_10))),b2) = multiply(b2,iPr_def_10),
inference(superposition,[status(thm)],[c_7106,c_1336]) ).
tcf(c_7753,plain,
! [X0: $i] : multiply(multiply(inverse(X0),multiply(b2,multiply(multiply(b2,iPr_def_10),inverse(multiply(b2,iPr_def_11))))),X0) = multiply(b2,iPr_def_10),
inference(superposition,[status(thm)],[c_6831,c_1336]) ).
tcf(c_7854,plain,
inverse(inverse(multiply(b2,multiply(iPr_def_10,multiply(b2,iPr_def_10))))) = multiply(b2,iPr_def_10),
inference(superposition,[status(thm)],[c_7183,c_6374]) ).
tcf(c_7855,plain,
inverse(inverse(inverse(multiply(b2,iPr_def_10)))) = multiply(b2,iPr_def_10),
inference(demodulation,[status(thm)],[c_7854,c_7189]) ).
tcf(c_8425,plain,
multiply(multiply(b2,iPr_def_10),inverse(multiply(inverse(multiply(multiply(iPr_def_10,multiply(inverse(multiply(b2,iPr_def_10)),multiply(b2,iPr_def_10))),multiply(b2,iPr_def_10))),multiply(b2,iPr_def_10)))) = inverse(b2),
inference(superposition,[status(thm)],[c_7666,c_2092]) ).
tcf(c_8439,plain,
inverse(multiply(multiply(b2,iPr_def_10),multiply(inverse(multiply(b2,iPr_def_10)),multiply(b2,iPr_def_10)))) = inverse(inverse(multiply(b2,iPr_def_10))),
inference(superposition,[status(thm)],[c_7855,c_6591]) ).
tcf(c_8472,plain,
multiply(inverse(multiply(b2,iPr_def_10)),multiply(b2,iPr_def_10)) = multiply(b2,multiply(iPr_def_10,multiply(b2,iPr_def_10))),
inference(superposition,[status(thm)],[c_7855,c_5787]) ).
tcf(c_8480,plain,
multiply(iPr_def_11,multiply(a2,multiply(multiply(b2,iPr_def_10),inverse(multiply(multiply(inverse(multiply(b2,iPr_def_10)),multiply(b2,iPr_def_10)),iPr_def_12))))) = inverse(inverse(multiply(b2,iPr_def_10))),
inference(superposition,[status(thm)],[c_1436,c_7207]) ).
tcf(c_8509,plain,
! [X0: $i,X1: $i] : inverse(multiply(inverse(X0),multiply(inverse(X1),multiply(multiply(b2,iPr_def_10),inverse(multiply(inverse(multiply(X1,multiply(inverse(multiply(b2,iPr_def_10)),multiply(b2,iPr_def_10)))),multiply(b2,iPr_def_10))))))) = X0,
inference(superposition,[status(thm)],[c_7207,c_4335]) ).
tcf(c_8685,plain,
multiply(inverse(multiply(b2,iPr_def_10)),multiply(b2,iPr_def_10)) = inverse(multiply(b2,iPr_def_10)),
inference(demodulation,[status(thm)],[c_8472,c_7189]) ).
tcf(c_8690,plain,
inverse(multiply(multiply(b2,iPr_def_10),inverse(multiply(b2,iPr_def_10)))) = inverse(inverse(multiply(b2,iPr_def_10))),
inference(demodulation,[status(thm)],[c_8439,c_8685]) ).
tcf(c_8691,plain,
inverse(inverse(multiply(b2,iPr_def_10))) = inverse(multiply(b2,iPr_def_10)),
inference(demodulation,[status(thm)],[c_8690,c_1336]) ).
tcf(c_8730,plain,
multiply(iPr_def_11,multiply(a2,multiply(multiply(b2,iPr_def_10),inverse(multiply(inverse(multiply(b2,iPr_def_10)),iPr_def_12))))) = inverse(multiply(b2,iPr_def_10)),
inference(demodulation,[status(thm)],[c_8480,c_8685,c_8691]) ).
tcf(c_8731,plain,
inverse(multiply(b2,iPr_def_10)) = multiply(b2,iPr_def_10),
inference(demodulation,[status(thm)],[c_8730,c_6591,c_7114]) ).
tcf(c_8770,plain,
multiply(multiply(b2,iPr_def_10),inverse(multiply(inverse(multiply(multiply(iPr_def_10,multiply(b2,iPr_def_10)),multiply(b2,iPr_def_10))),multiply(b2,iPr_def_10)))) = inverse(b2),
inference(demodulation,[status(thm)],[c_8425,c_8685,c_8731]) ).
tcf(c_8771,plain,
inverse(inverse(multiply(iPr_def_10,multiply(b2,iPr_def_10)))) = iPr_def_10,
inference(demodulation,[status(thm)],[c_8770,c_2636,c_7252]) ).
tcf(c_8801,plain,
! [X0: $i,X1: $i] : inverse(multiply(inverse(X0),multiply(inverse(X1),multiply(multiply(b2,iPr_def_10),inverse(multiply(inverse(multiply(X1,multiply(b2,iPr_def_10))),multiply(b2,iPr_def_10))))))) = X0,
inference(demodulation,[status(thm)],[c_8509,c_8685,c_8731]) ).
tcf(c_8802,plain,
! [X0: $i] : inverse(multiply(inverse(X0),multiply(b2,iPr_def_10))) = X0,
inference(demodulation,[status(thm)],[c_8801,c_1336,c_2636]) ).
tcf(c_9433,plain,
! [X0: $i,X1: $i] : multiply(inverse(multiply(X0,X1)),multiply(b2,multiply(multiply(b2,iPr_def_10),inverse(multiply(b2,iPr_def_11))))) = inverse(multiply(X0,multiply(X1,multiply(multiply(b2,iPr_def_10),inverse(multiply(b2,iPr_def_10)))))),
inference(superposition,[status(thm)],[c_7753,c_103]) ).
tcf(c_9458,plain,
! [X0: $i,X1: $i] : inverse(multiply(X0,multiply(multiply(multiply(b2,iPr_def_10),inverse(multiply(X1,multiply(b2,iPr_def_10)))),multiply(multiply(b2,iPr_def_10),X1)))) = multiply(inverse(X0),multiply(b2,multiply(multiply(b2,iPr_def_10),inverse(multiply(b2,iPr_def_11))))),
inference(superposition,[status(thm)],[c_7753,c_151]) ).
tcf(c_9504,plain,
! [X0: $i] : multiply(multiply(b2,iPr_def_10),multiply(multiply(b2,iPr_def_10),X0)) = multiply(b2,multiply(iPr_def_10,X0)),
inference(superposition,[status(thm)],[c_8731,c_6542]) ).
tcf(c_9505,plain,
! [X0: $i] : inverse(multiply(multiply(b2,iPr_def_10),multiply(X0,multiply(multiply(b2,iPr_def_10),inverse(multiply(b2,multiply(iPr_def_10,X0))))))) = multiply(b2,iPr_def_10),
inference(superposition,[status(thm)],[c_8731,c_6374]) ).
tcf(c_9508,plain,
multiply(multiply(b2,iPr_def_10),multiply(b2,iPr_def_10)) = multiply(b2,multiply(iPr_def_10,multiply(b2,iPr_def_10))),
inference(superposition,[status(thm)],[c_8731,c_5787]) ).
tcf(c_9517,plain,
multiply(multiply(b2,iPr_def_10),multiply(b2,iPr_def_10)) = multiply(b2,iPr_def_10),
inference(superposition,[status(thm)],[c_8731,c_1336]) ).
tcf(c_9538,plain,
! [X0: $i] : inverse(inverse(multiply(X0,multiply(multiply(b2,iPr_def_10),multiply(b2,iPr_def_10))))) = X0,
inference(superposition,[status(thm)],[c_8731,c_7207]) ).
tcf(c_9539,plain,
multiply(multiply(iPr_def_10,multiply(multiply(b2,iPr_def_10),multiply(b2,iPr_def_10))),b2) = multiply(b2,iPr_def_10),
inference(superposition,[status(thm)],[c_8731,c_7666]) ).
tcf(c_9563,plain,
inverse(multiply(inverse(multiply(iPr_def_10,multiply(b2,iPr_def_10))),multiply(iPr_def_10,inverse(iPr_def_10)))) = inverse(multiply(b2,multiply(b2,iPr_def_10))),
inference(superposition,[status(thm)],[c_8771,c_2664]) ).
tcf(c_9586,plain,
inverse(multiply(multiply(iPr_def_10,multiply(b2,iPr_def_10)),multiply(b2,iPr_def_10))) = inverse(multiply(b2,multiply(iPr_def_10,iPr_def_10))),
inference(superposition,[status(thm)],[c_8771,c_3659]) ).
tcf(c_9590,plain,
inverse(multiply(iPr_def_10,multiply(b2,iPr_def_10))) = b2,
inference(superposition,[status(thm)],[c_7252,c_8802]) ).
tcf(c_9628,plain,
! [X0: $i] : multiply(inverse(X0),multiply(b2,multiply(multiply(b2,iPr_def_10),inverse(multiply(b2,iPr_def_11))))) = inverse(multiply(X0,multiply(b2,iPr_def_10))),
inference(superposition,[status(thm)],[c_6831,c_8802]) ).
tcf(c_9631,plain,
! [X0: $i] : multiply(inverse(multiply(b2,iPr_def_10)),multiply(multiply(b2,iPr_def_10),multiply(multiply(b2,iPr_def_10),X0))) = inverse(multiply(inverse(X0),multiply(b2,iPr_def_10))),
inference(superposition,[status(thm)],[c_7183,c_8802]) ).
tcf(c_9641,plain,
! [X0: $i] : inverse(multiply(X0,multiply(b2,iPr_def_10))) = multiply(inverse(X0),multiply(b2,iPr_def_10)),
inference(superposition,[status(thm)],[c_8802,c_8802]) ).
tcf(c_9645,plain,
! [X0: $i,X1: $i] : multiply(multiply(inverse(X0),multiply(b2,iPr_def_10)),multiply(X0,X1)) = multiply(b2,multiply(iPr_def_10,X1)),
inference(superposition,[status(thm)],[c_8802,c_6542]) ).
tcf(c_9649,plain,
! [X0: $i] : multiply(multiply(inverse(X0),multiply(b2,iPr_def_10)),multiply(b2,iPr_def_10)) = multiply(b2,multiply(iPr_def_10,inverse(X0))),
inference(superposition,[status(thm)],[c_8802,c_5787]) ).
tcf(c_9653,plain,
! [X0: $i] : inverse(multiply(multiply(inverse(X0),multiply(b2,iPr_def_10)),multiply(b2,iPr_def_10))) = inverse(multiply(b2,multiply(iPr_def_10,inverse(X0)))),
inference(superposition,[status(thm)],[c_8802,c_3659]) ).
tcf(c_9679,plain,
! [X0: $i] : inverse(multiply(b2,multiply(iPr_def_10,multiply(multiply(b2,iPr_def_10),X0)))) = inverse(X0),
inference(superposition,[status(thm)],[c_8802,c_103]) ).
tcf(c_9687,plain,
! [X0: $i] : multiply(multiply(b2,iPr_def_10),inverse(multiply(X0,multiply(b2,iPr_def_10)))) = inverse(inverse(inverse(X0))),
inference(superposition,[status(thm)],[c_8802,c_2636]) ).
tcf(c_9688,plain,
! [X0: $i,X1: $i] : multiply(multiply(b2,iPr_def_10),inverse(multiply(X0,multiply(inverse(X0),X1)))) = inverse(X1),
inference(superposition,[status(thm)],[c_8802,c_2092]) ).
tcf(c_9692,plain,
! [X0: $i] : inverse(inverse(multiply(X0,multiply(b2,iPr_def_10)))) = X0,
inference(demodulation,[status(thm)],[c_9538,c_9517]) ).
tcf(c_9693,plain,
! [X0: $i] : multiply(multiply(b2,iPr_def_10),inverse(multiply(b2,multiply(iPr_def_10,X0)))) = inverse(X0),
inference(demodulation,[status(thm)],[c_9688,c_5132]) ).
tcf(c_9697,plain,
multiply(multiply(iPr_def_10,multiply(b2,iPr_def_10)),b2) = multiply(b2,iPr_def_10),
inference(demodulation,[status(thm)],[c_9539,c_9517]) ).
tcf(c_9698,plain,
multiply(b2,multiply(iPr_def_10,multiply(b2,iPr_def_10))) = multiply(b2,iPr_def_10),
inference(demodulation,[status(thm)],[c_9508,c_9517]) ).
tcf(c_9699,plain,
! [X0: $i,X1: $i] : multiply(inverse(multiply(X0,multiply(b2,iPr_def_10))),multiply(X0,X1)) = multiply(b2,multiply(iPr_def_10,X1)),
inference(demodulation,[status(thm)],[c_9645,c_9641]) ).
tcf(c_9704,plain,
! [X0: $i] : inverse(multiply(multiply(X0,multiply(b2,iPr_def_10)),multiply(b2,iPr_def_10))) = multiply(b2,multiply(iPr_def_10,inverse(X0))),
inference(demodulation,[status(thm)],[c_9649,c_9641]) ).
tcf(c_9705,plain,
inverse(multiply(b2,multiply(iPr_def_10,iPr_def_10))) = multiply(b2,multiply(iPr_def_10,inverse(iPr_def_10))),
inference(demodulation,[status(thm)],[c_9586,c_9704]) ).
tcf(c_9706,plain,
inverse(multiply(b2,multiply(iPr_def_10,iPr_def_10))) = multiply(b2,multiply(b2,iPr_def_10)),
inference(demodulation,[status(thm)],[c_9705,c_1336]) ).
tcf(c_9723,plain,
! [X0: $i] : inverse(multiply(b2,multiply(iPr_def_10,inverse(X0)))) = multiply(b2,multiply(iPr_def_10,inverse(inverse(X0)))),
inference(demodulation,[status(thm)],[c_9653,c_9704]) ).
tcf(c_9724,plain,
! [X0: $i] : inverse(multiply(b2,multiply(iPr_def_10,inverse(X0)))) = multiply(X0,multiply(b2,iPr_def_10)),
inference(demodulation,[status(thm)],[c_9723,c_5787]) ).
tcf(c_9727,plain,
inverse(multiply(b2,multiply(b2,iPr_def_10))) = multiply(iPr_def_10,multiply(b2,iPr_def_10)),
inference(demodulation,[status(thm)],[c_9563,c_9699,c_9724]) ).
tcf(c_9738,plain,
! [X0: $i] : inverse(multiply(multiply(b2,iPr_def_10),multiply(X0,inverse(X0)))) = multiply(b2,iPr_def_10),
inference(demodulation,[status(thm)],[c_9505,c_9693]) ).
tcf(c_9739,plain,
inverse(multiply(multiply(b2,iPr_def_10),multiply(b2,iPr_def_10))) = multiply(b2,iPr_def_10),
inference(demodulation,[status(thm)],[c_9738,c_1336]) ).
tcf(c_9745,plain,
! [X0: $i] : multiply(inverse(multiply(b2,iPr_def_10)),multiply(b2,multiply(iPr_def_10,X0))) = X0,
inference(demodulation,[status(thm)],[c_9631,c_9692,c_9504,c_9641]) ).
tcf(c_9746,plain,
! [X0: $i] : multiply(multiply(b2,iPr_def_10),multiply(b2,multiply(iPr_def_10,X0))) = X0,
inference(demodulation,[status(thm)],[c_9745,c_8731]) ).
tcf(c_9851,plain,
! [X0: $i,X1: $i] : inverse(multiply(X0,multiply(X1,multiply(multiply(b2,iPr_def_10),inverse(multiply(b2,iPr_def_10)))))) = inverse(multiply(multiply(X0,X1),multiply(b2,iPr_def_10))),
inference(demodulation,[status(thm)],[c_9433,c_9628]) ).
tcf(c_9852,plain,
! [X0: $i,X1: $i] : inverse(multiply(multiply(X0,X1),multiply(b2,iPr_def_10))) = inverse(multiply(X0,multiply(X1,multiply(b2,iPr_def_10)))),
inference(demodulation,[status(thm)],[c_9851,c_1336]) ).
tcf(c_9910,plain,
! [X0: $i,X1: $i] : inverse(multiply(X0,multiply(inverse(inverse(inverse(X1))),multiply(multiply(b2,iPr_def_10),X1)))) = inverse(multiply(X0,multiply(b2,iPr_def_10))),
inference(demodulation,[status(thm)],[c_9458,c_9687,c_9628]) ).
tcf(c_10063,plain,
multiply(multiply(b2,iPr_def_10),inverse(multiply(b2,iPr_def_11))) = iPr_def_10,
inference(superposition,[status(thm)],[c_9590,c_3050]) ).
tcf(c_10067,plain,
inverse(inverse(multiply(inverse(multiply(iPr_def_10,multiply(b2,iPr_def_10))),iPr_def_11))) = inverse(multiply(b2,multiply(iPr_def_10,iPr_def_10))),
inference(superposition,[status(thm)],[c_3050,c_9679]) ).
tcf(c_10079,plain,
! [X0: $i] : multiply(b2,multiply(iPr_def_10,multiply(multiply(b2,iPr_def_10),X0))) = inverse(multiply(inverse(X0),multiply(b2,iPr_def_10))),
inference(superposition,[status(thm)],[c_9679,c_8802]) ).
tcf(c_10413,plain,
! [X0: $i] : multiply(b2,multiply(iPr_def_10,multiply(multiply(b2,iPr_def_10),X0))) = X0,
inference(demodulation,[status(thm)],[c_10079,c_8802]) ).
tcf(c_10414,plain,
inverse(inverse(multiply(b2,iPr_def_11))) = multiply(b2,multiply(b2,iPr_def_10)),
inference(demodulation,[status(thm)],[c_10067,c_9590,c_9706]) ).
tcf(c_11069,plain,
multiply(multiply(b2,iPr_def_10),inverse(multiply(inverse(multiply(b2,multiply(b2,iPr_def_10))),multiply(b2,iPr_def_10)))) = inverse(multiply(iPr_def_10,multiply(b2,iPr_def_10))),
inference(superposition,[status(thm)],[c_9698,c_2092]) ).
tcf(c_11082,plain,
! [X0: $i,X1: $i] : inverse(multiply(multiply(iPr_def_10,multiply(b2,iPr_def_10)),multiply(multiply(multiply(b2,iPr_def_10),inverse(multiply(X0,multiply(b2,iPr_def_10)))),multiply(multiply(X1,inverse(X1)),X0)))) = b2,
inference(superposition,[status(thm)],[c_9698,c_153]) ).
tcf(c_11091,plain,
multiply(multiply(b2,iPr_def_10),multiply(b2,iPr_def_11)) = b2,
inference(superposition,[status(thm)],[c_63,c_9746]) ).
tcf(c_11106,plain,
! [X0: $i] : inverse(multiply(b2,multiply(multiply(iPr_def_10,X0),multiply(multiply(b2,iPr_def_10),inverse(X0))))) = multiply(b2,iPr_def_10),
inference(superposition,[status(thm)],[c_9746,c_103]) ).
tcf(c_11127,plain,
! [X0: $i,X1: $i] : inverse(multiply(inverse(multiply(X0,multiply(b2,iPr_def_10))),multiply(X0,X1))) = multiply(b2,multiply(iPr_def_10,inverse(X1))),
inference(superposition,[status(thm)],[c_2092,c_10413]) ).
tcf(c_11130,plain,
inverse(multiply(inverse(multiply(iPr_def_11,multiply(b2,iPr_def_10))),iPr_def_12)) = multiply(b2,multiply(iPr_def_10,inverse(a2))),
inference(superposition,[status(thm)],[c_2635,c_10413]) ).
tcf(c_11190,plain,
! [X0: $i] : inverse(multiply(b2,multiply(iPr_def_10,X0))) = multiply(b2,multiply(iPr_def_10,inverse(X0))),
inference(demodulation,[status(thm)],[c_11127,c_9699]) ).
tcf(c_11220,plain,
inverse(iPr_def_10) = b2,
inference(demodulation,[status(thm)],[c_11069,c_2636,c_7252,c_9590]) ).
tcf(c_11243,plain,
inverse(inverse(multiply(b2,iPr_def_11))) = b2,
inference(demodulation,[status(thm)],[c_11082,c_1188,c_1336,c_9687,c_9704,c_9910,c_10414]) ).
tcf(c_11397,plain,
! [X0: $i,X1: $i] : inverse(multiply(X0,multiply(multiply(multiply(b2,iPr_def_10),inverse(multiply(multiply(b2,iPr_def_11),multiply(X1,X0)))),b2))) = X1,
inference(superposition,[status(thm)],[c_11091,c_151]) ).
tcf(c_11533,plain,
! [X0: $i] : multiply(b2,multiply(multiply(iPr_def_10,X0),multiply(multiply(b2,iPr_def_10),inverse(X0)))) = inverse(multiply(multiply(b2,iPr_def_10),multiply(b2,iPr_def_10))),
inference(superposition,[status(thm)],[c_11106,c_8802]) ).
tcf(c_11547,plain,
! [X0: $i] : inverse(multiply(multiply(b2,multiply(multiply(iPr_def_10,X0),multiply(multiply(b2,iPr_def_10),inverse(X0)))),multiply(multiply(b2,iPr_def_10),inverse(iPr_def_10)))) = inverse(multiply(b2,multiply(b2,iPr_def_10))),
inference(superposition,[status(thm)],[c_11106,c_2664]) ).
tcf(c_11639,plain,
! [X0: $i] : multiply(b2,multiply(multiply(iPr_def_10,X0),multiply(multiply(b2,iPr_def_10),inverse(X0)))) = multiply(b2,iPr_def_10),
inference(demodulation,[status(thm)],[c_11533,c_9739]) ).
tcf(c_11679,plain,
inverse(multiply(multiply(b2,iPr_def_10),multiply(multiply(b2,iPr_def_10),inverse(iPr_def_10)))) = inverse(multiply(b2,multiply(b2,iPr_def_10))),
inference(demodulation,[status(thm)],[c_11547,c_11639]) ).
tcf(c_11680,plain,
multiply(iPr_def_10,multiply(b2,iPr_def_10)) = iPr_def_10,
inference(demodulation,[status(thm)],[c_11679,c_7252,c_9504,c_9706,c_9727,c_10414,c_11190,c_11243]) ).
tcf(c_11864,plain,
inverse(multiply(b2,multiply(b2,iPr_def_10))) = iPr_def_10,
inference(superposition,[status(thm)],[c_11220,c_8802]) ).
tcf(c_11868,plain,
! [X0: $i] : multiply(b2,multiply(iPr_def_10,X0)) = multiply(iPr_def_10,multiply(b2,X0)),
inference(superposition,[status(thm)],[c_11220,c_6542]) ).
tcf(c_11949,plain,
multiply(multiply(b2,iPr_def_10),inverse(multiply(inverse(iPr_def_10),iPr_def_10))) = inverse(multiply(b2,iPr_def_10)),
inference(superposition,[status(thm)],[c_11680,c_2092]) ).
tcf(c_11972,plain,
multiply(b2,iPr_def_10) = multiply(iPr_def_10,b2),
inference(superposition,[status(thm)],[c_11680,c_9697]) ).
tcf(c_12127,plain,
multiply(b2,iPr_def_10) = iPr_def_11,
inference(demodulation,[status(thm)],[c_11972,c_63]) ).
tcf(c_12128,plain,
inverse(multiply(b2,iPr_def_11)) = iPr_def_10,
inference(demodulation,[status(thm)],[c_11864,c_12127]) ).
tcf(c_12146,plain,
multiply(iPr_def_11,inverse(multiply(inverse(iPr_def_10),iPr_def_10))) = inverse(iPr_def_11),
inference(demodulation,[status(thm)],[c_11949,c_12127]) ).
tcf(c_12147,plain,
multiply(iPr_def_11,multiply(b2,iPr_def_10)) = inverse(iPr_def_11),
inference(demodulation,[status(thm)],[c_12146,c_8731,c_11220]) ).
tcf(c_12764,plain,
inverse(inverse(multiply(b2,iPr_def_11))) = multiply(b2,iPr_def_11),
inference(superposition,[status(thm)],[c_12127,c_10414]) ).
tcf(c_12770,plain,
multiply(iPr_def_11,iPr_def_11) = iPr_def_11,
inference(superposition,[status(thm)],[c_12127,c_9517]) ).
tcf(c_12772,plain,
! [X0: $i] : inverse(inverse(multiply(X0,iPr_def_11))) = X0,
inference(superposition,[status(thm)],[c_12127,c_9692]) ).
tcf(c_12778,plain,
! [X0: $i] : inverse(multiply(inverse(X0),iPr_def_11)) = X0,
inference(superposition,[status(thm)],[c_12127,c_8802]) ).
tcf(c_12779,plain,
inverse(iPr_def_11) = iPr_def_11,
inference(superposition,[status(thm)],[c_12127,c_8731]) ).
tcf(c_12929,plain,
multiply(multiply(b2,iPr_def_10),iPr_def_10) = iPr_def_10,
inference(superposition,[status(thm)],[c_12128,c_10063]) ).
tcf(c_12941,plain,
! [X0: $i,X1: $i] : inverse(multiply(X0,multiply(multiply(iPr_def_11,inverse(multiply(multiply(b2,iPr_def_11),multiply(X1,X0)))),b2))) = X1,
inference(light_normalisation,[status(thm)],[c_11397,c_12127]) ).
tcf(c_13003,plain,
! [X0: $i,X1: $i] : multiply(X0,multiply(multiply(iPr_def_11,inverse(multiply(multiply(b2,iPr_def_11),multiply(X1,X0)))),b2)) = inverse(multiply(X1,multiply(b2,iPr_def_10))),
inference(superposition,[status(thm)],[c_12941,c_8802]) ).
tcf(c_13007,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(multiply(X0,multiply(multiply(iPr_def_11,inverse(multiply(multiply(b2,iPr_def_11),multiply(X1,X0)))),b2)),multiply(X1,X2)) = multiply(b2,multiply(iPr_def_10,X2)),
inference(superposition,[status(thm)],[c_12941,c_6542]) ).
tcf(c_13010,plain,
! [X0: $i,X1: $i,X2: $i] : inverse(multiply(multiply(X0,multiply(multiply(iPr_def_11,inverse(multiply(multiply(b2,iPr_def_11),multiply(X1,X0)))),b2)),multiply(X1,X2))) = inverse(multiply(b2,multiply(iPr_def_10,X2))),
inference(superposition,[status(thm)],[c_12941,c_5132]) ).
tcf(c_13011,plain,
! [X0: $i,X1: $i] : multiply(multiply(X0,multiply(multiply(iPr_def_11,inverse(multiply(multiply(b2,iPr_def_11),multiply(X1,X0)))),b2)),multiply(b2,iPr_def_10)) = multiply(b2,multiply(iPr_def_10,inverse(X1))),
inference(superposition,[status(thm)],[c_12941,c_5787]) ).
tcf(c_13013,plain,
! [X0: $i,X1: $i,X2: $i] : inverse(multiply(multiply(X0,multiply(multiply(iPr_def_11,inverse(multiply(multiply(b2,iPr_def_11),multiply(X1,X0)))),b2)),multiply(X1,inverse(inverse(X2))))) = inverse(multiply(X2,multiply(b2,iPr_def_10))),
inference(superposition,[status(thm)],[c_12941,c_3676]) ).
tcf(c_13047,plain,
multiply(iPr_def_11,iPr_def_10) = iPr_def_10,
inference(demodulation,[status(thm)],[c_12929,c_12127]) ).
tcf(c_13055,plain,
multiply(b2,iPr_def_11) = b2,
inference(demodulation,[status(thm)],[c_12764,c_12772]) ).
tcf(c_13168,plain,
! [X0: $i,X1: $i] : multiply(X0,multiply(multiply(iPr_def_11,inverse(multiply(b2,multiply(X1,X0)))),b2)) = inverse(multiply(X1,multiply(b2,iPr_def_10))),
inference(demodulation,[status(thm)],[c_13003,c_13055]) ).
tcf(c_13169,plain,
! [X0: $i,X1: $i] : multiply(X0,multiply(multiply(iPr_def_11,inverse(multiply(b2,multiply(X1,X0)))),b2)) = inverse(multiply(X1,iPr_def_11)),
inference(demodulation,[status(thm)],[c_13168,c_12127]) ).
tcf(c_13223,plain,
! [X0: $i,X1: $i] : multiply(inverse(multiply(X0,iPr_def_11)),multiply(X0,X1)) = multiply(b2,multiply(iPr_def_10,X1)),
inference(demodulation,[status(thm)],[c_13007,c_13055,c_13169]) ).
tcf(c_13224,plain,
! [X0: $i,X1: $i] : multiply(inverse(multiply(X0,iPr_def_11)),multiply(X0,X1)) = multiply(iPr_def_10,multiply(b2,X1)),
inference(demodulation,[status(thm)],[c_13223,c_11868]) ).
tcf(c_13237,plain,
! [X0: $i] : multiply(inverse(multiply(X0,iPr_def_11)),multiply(b2,iPr_def_10)) = multiply(b2,multiply(iPr_def_10,inverse(X0))),
inference(demodulation,[status(thm)],[c_13011,c_13055,c_13169]) ).
tcf(c_13238,plain,
! [X0: $i] : inverse(multiply(iPr_def_10,multiply(b2,X0))) = inverse(multiply(X0,inverse(iPr_def_11))),
inference(demodulation,[status(thm)],[c_13237,c_9641,c_9852,c_11190,c_11868,c_12147]) ).
tcf(c_13247,plain,
! [X0: $i] : inverse(multiply(b2,multiply(iPr_def_10,X0))) = inverse(multiply(X0,iPr_def_11)),
inference(demodulation,[status(thm)],[c_13010,c_12779,c_13055,c_13169,c_13224,c_13238]) ).
tcf(c_13248,plain,
! [X0: $i] : inverse(multiply(iPr_def_10,multiply(b2,X0))) = inverse(multiply(X0,iPr_def_11)),
inference(demodulation,[status(thm)],[c_13247,c_11868]) ).
tcf(c_13270,plain,
! [X0: $i] : inverse(multiply(X0,multiply(b2,iPr_def_10))) = inverse(X0),
inference(demodulation,[status(thm)],[c_13013,c_12778,c_13055,c_13169,c_13224,c_13248]) ).
tcf(c_13271,plain,
! [X0: $i] : inverse(multiply(X0,iPr_def_11)) = inverse(X0),
inference(demodulation,[status(thm)],[c_13270,c_12127]) ).
tcf(c_13919,plain,
! [X0: $i] : inverse(multiply(X0,iPr_def_11)) = multiply(inverse(X0),iPr_def_11),
inference(light_normalisation,[status(thm)],[c_9628,c_10063,c_12127]) ).
tcf(c_13973,plain,
! [X0: $i] : inverse(multiply(multiply(inverse(X0),multiply(b2,iPr_def_10)),iPr_def_11)) = multiply(X0,iPr_def_11),
inference(superposition,[status(thm)],[c_8802,c_13919]) ).
tcf(c_14000,plain,
! [X0: $i] : inverse(multiply(iPr_def_10,multiply(b2,multiply(multiply(b2,iPr_def_10),inverse(inverse(multiply(X0,iPr_def_11))))))) = inverse(X0),
inference(superposition,[status(thm)],[c_13919,c_145]) ).
tcf(c_14055,plain,
! [X0: $i] : inverse(multiply(iPr_def_11,multiply(iPr_def_11,inverse(inverse(X0))))) = inverse(multiply(X0,multiply(b2,iPr_def_10))),
inference(superposition,[status(thm)],[c_12779,c_3676]) ).
tcf(c_14117,plain,
! [X0: $i,X1: $i] : inverse(multiply(iPr_def_11,multiply(iPr_def_11,multiply(multiply(X0,inverse(X0)),inverse(multiply(X1,iPr_def_11)))))) = X1,
inference(superposition,[status(thm)],[c_12770,c_66]) ).
tcf(c_14192,plain,
! [X0: $i] : inverse(multiply(inverse(X0),multiply(b2,multiply(multiply(b2,iPr_def_10),inverse(b2))))) = X0,
inference(superposition,[status(thm)],[c_13055,c_6831]) ).
tcf(c_14195,plain,
! [X0: $i] : multiply(X0,iPr_def_11) = X0,
inference(demodulation,[status(thm)],[c_13973,c_8802,c_13271]) ).
tcf(c_14197,plain,
! [X0: $i] : inverse(inverse(X0)) = X0,
inference(demodulation,[status(thm)],[c_14192,c_7252,c_12127,c_13047,c_13271,c_13919]) ).
tcf(c_14214,plain,
! [X0: $i] : inverse(multiply(X0,multiply(b2,iPr_def_10))) = inverse(multiply(iPr_def_11,multiply(iPr_def_11,X0))),
inference(demodulation,[status(thm)],[c_14055,c_14197]) ).
tcf(c_14215,plain,
! [X0: $i] : inverse(multiply(iPr_def_11,multiply(iPr_def_11,X0))) = inverse(X0),
inference(demodulation,[status(thm)],[c_14214,c_12127,c_13271]) ).
tcf(c_14225,plain,
! [X0: $i,X1: $i] : inverse(multiply(multiply(X0,inverse(X0)),inverse(X1))) = X1,
inference(demodulation,[status(thm)],[c_14117,c_14195,c_14215]) ).
tcf(c_14226,plain,
! [X0: $i] : inverse(multiply(iPr_def_11,inverse(X0))) = X0,
inference(demodulation,[status(thm)],[c_14225,c_1188,c_12127]) ).
tcf(c_14238,plain,
! [X0: $i] : inverse(multiply(iPr_def_10,multiply(b2,multiply(multiply(b2,iPr_def_10),X0)))) = inverse(X0),
inference(demodulation,[status(thm)],[c_14000,c_14195,c_14197]) ).
tcf(c_14239,plain,
! [X0: $i] : inverse(multiply(iPr_def_11,X0)) = inverse(X0),
inference(demodulation,[status(thm)],[c_14238,c_12127,c_12779,c_13238,c_13271]) ).
tcf(c_14985,plain,
inverse(multiply(multiply(multiply(b2,iPr_def_10),inverse(multiply(iPr_def_11,iPr_def_12))),multiply(multiply(b2,iPr_def_10),multiply(b2,iPr_def_10)))) = a2,
inference(superposition,[status(thm)],[c_14195,c_534]) ).
tcf(c_15056,plain,
multiply(inverse(multiply(iPr_def_11,multiply(b2,iPr_def_10))),iPr_def_12) = inverse(multiply(b2,multiply(iPr_def_10,inverse(a2)))),
inference(superposition,[status(thm)],[c_11130,c_14197]) ).
tcf(c_15059,plain,
inverse(multiply(iPr_def_11,multiply(a2,multiply(b2,iPr_def_10)))) = inverse(iPr_def_12),
inference(superposition,[status(thm)],[c_3045,c_14197]) ).
tcf(c_15070,plain,
! [X0: $i] : multiply(b2,multiply(iPr_def_10,multiply(multiply(b2,iPr_def_10),X0))) = inverse(inverse(X0)),
inference(superposition,[status(thm)],[c_9679,c_14197]) ).
tcf(c_15128,plain,
! [X0: $i] : multiply(X0,multiply(b2,iPr_def_10)) = multiply(b2,multiply(iPr_def_10,X0)),
inference(superposition,[status(thm)],[c_14197,c_5787]) ).
tcf(c_15139,plain,
! [X0: $i] : multiply(b2,multiply(iPr_def_10,X0)) = X0,
inference(demodulation,[status(thm)],[c_15128,c_12127,c_14195]) ).
tcf(c_15140,plain,
inverse(a2) = inverse(iPr_def_12),
inference(demodulation,[status(thm)],[c_15059,c_12127,c_14195,c_14239]) ).
tcf(c_15147,plain,
! [X0: $i] : multiply(multiply(b2,iPr_def_10),X0) = inverse(inverse(X0)),
inference(demodulation,[status(thm)],[c_15070,c_15139]) ).
tcf(c_15148,plain,
! [X0: $i] : multiply(iPr_def_11,X0) = X0,
inference(demodulation,[status(thm)],[c_15147,c_12127,c_14197]) ).
tcf(c_15180,plain,
multiply(inverse(multiply(b2,iPr_def_10)),iPr_def_12) = inverse(inverse(iPr_def_12)),
inference(demodulation,[status(thm)],[c_15056,c_15139,c_15140,c_15148]) ).
tcf(c_15181,plain,
multiply(iPr_def_11,iPr_def_12) = iPr_def_12,
inference(demodulation,[status(thm)],[c_15180,c_8731,c_12127,c_14197]) ).
tcf(c_15241,plain,
inverse(multiply(multiply(multiply(b2,iPr_def_10),inverse(iPr_def_12)),multiply(multiply(b2,iPr_def_10),multiply(b2,iPr_def_10)))) = a2,
inference(demodulation,[status(thm)],[c_14985,c_15181]) ).
tcf(c_15242,plain,
a2 = iPr_def_12,
inference(demodulation,[status(thm)],[c_15241,c_9517,c_12127,c_14195,c_14226]) ).
tcf(c_16019,plain,
$false,
inference(superposition,[status(thm)],[c_15242,c_65]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP443-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 : n018.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:49:02 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...
% 3.90/2.29 WARNING - Clausifier option not provided in the heuristic config "heur/vip2_118404", setting default options.
% 3.90/2.29 % SZS status Started for theBenchmark.p
% 3.90/2.29 % SZS status Unsatisfiable for theBenchmark.p
% 3.90/2.29
% 3.90/2.29 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 3.90/2.29
% 3.90/2.29 % ------ iProver source info
% 3.90/2.29
% 3.90/2.29 % git: date: 2026-07-19 20:42:38 +0200
% 3.90/2.29 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 3.90/2.29 % git: non_committed_changes: false
% 3.90/2.29
% 3.90/2.29 % ------ Parsing...% successful
% 3.90/2.29
% 3.90/2.29
% 3.90/2.29 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 3.90/2.29
% 3.90/2.29 % ------ Preprocessing... sf_s rm: 0 0s sf_e pe_s pe_e %
% 3.90/2.29
% 3.90/2.29 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 3.90/2.29
% 3.90/2.29 % ------ Preprocessing... sf_s rm: 0 0s sf_e
% 3.90/2.29 % ------ Proving...
% 3.90/2.29 % ------ Problem Properties
% 3.90/2.29
% 3.90/2.29 %
% 3.90/2.29 % clauses 5
% 3.90/2.29 % conjectures 1
% 3.90/2.29 % EPR 1
% 3.90/2.29 % Horn 5
% 3.90/2.29 % unary 5
% 3.90/2.29 % binary 0
% 3.90/2.29 % lits 5
% 3.90/2.29 % lits eq 5
% 3.90/2.29 % fd_pure 0
% 3.90/2.29 % fd_pseudo 0
% 3.90/2.29 % fd_cond 0
% 3.90/2.29 % fd_pseudo_cond 0
% 3.90/2.29 % AC symbols 0
% 3.90/2.29
% 3.90/2.29 % ------ Input Options Time Limit: Unbounded
% 3.90/2.29
% 3.90/2.29
% 3.90/2.29 % ------
% 3.90/2.29 % Current options:
% 3.90/2.29 % ------
% 3.90/2.29
% 3.90/2.29
% 3.90/2.29 %
% 3.90/2.29
% 3.90/2.29 % ------ Proving...
% 3.90/2.29 %
% 3.90/2.29
% 3.90/2.29 % SZS status Unsatisfiable for theBenchmark.p
% 3.90/2.29
% 3.90/2.29 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 3.90/2.30
% 3.90/2.30
%------------------------------------------------------------------------------