%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : GRP120-1 : TPTP v9.3.1. Released v1.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% Computer : n005.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 01:30:57 PM UTC 2026
% Result : Unsatisfiable 15.11s 4.68s
% Output : CNFRefutation 15.11s
% Verified :
% SZS Type : Refutation
% Derivation depth : 56
% Number of leaves : 5
% Syntax : Number of formulae : 169 ( 169 unt; 2 def)
% Number of atoms : 1037 ( 168 equ)
% Maximal formula atoms : 1 ( 6 avg)
% Number of connectives : 5 ( 5 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 2 avg)
% Maximal term depth : 12 ( 2 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 4 ( 2 usr; 3 prp; 0-2 aty)
% Number of functors : 3 ( 3 usr; 2 con; 0-2 aty)
% Number of variables : 146 ( 0 sgn 146 !; 0 ?; 143 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X2,X0,X1] : multiply(X0,multiply(multiply(X0,multiply(multiply(X0,X0),multiply(X1,X2))),multiply(X2,multiply(X2,X2)))) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',single_axiom) ).
fof(f2,axiom,
multiply(identity,identity) = identity,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',single_axiom2) ).
fof(f3,plain,
identity = multiply(identity,identity),
inference(reorient_equations,[],[f2]) ).
fof(f4,negated_conjecture,
multiply(identity,a) != a,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_order3) ).
fof(f5,plain,
a != multiply(identity,a),
inference(reorient_equations,[],[f4]) ).
tcf(c_52,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(X0,multiply(multiply(X0,multiply(multiply(X0,X0),multiply(X1,X2))),multiply(X2,multiply(X2,X2)))) = X1,
inference(cnf_transformation,[],[f1]) ).
tcf(c_53,plain,
multiply(identity,identity) = identity,
inference(cnf_transformation,[],[f3]) ).
tcf(c_54,negated_conjecture,
multiply(identity,a) != a,
inference(cnf_transformation,[],[f5]) ).
tcf(c_65,definition,
iPr_def_10 = multiply(identity,a),
introduced(definition,[new_symbols(definition,[iPr_def_10])],[]) ).
tcf(c_66,definition,
iPr_def_11 = multiply(identity,identity),
introduced(definition,[new_symbols(definition,[iPr_def_11])],[]) ).
tcf(c_67,negated_conjecture,
iPr_def_10 != a,
inference(demodulation,[status(thm)],[c_54,c_65]) ).
tcf(c_68,plain,
iPr_def_11 = identity,
inference(demodulation,[status(thm)],[c_53,c_66]) ).
tcf(c_69,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(X0,multiply(multiply(X0,multiply(multiply(X0,X0),multiply(X1,X2))),multiply(X2,multiply(X2,X2)))) = X1,
inference(demodulation,[status(thm)],[c_52]) ).
tcf(c_101,plain,
multiply(iPr_def_11,iPr_def_11) = iPr_def_11,
inference(light_normalisation,[status(thm)],[c_66,c_68]) ).
tcf(c_697,plain,
! [X0: $i,X1: $i] : multiply(X0,multiply(multiply(X0,multiply(multiply(X0,X0),multiply(X1,iPr_def_11))),iPr_def_11)) = X1,
inference(superposition,[status(thm)],[c_101,c_69]) ).
tcf(c_699,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(X0,multiply(multiply(X0,X1),multiply(multiply(X2,multiply(X2,X2)),multiply(multiply(X2,multiply(X2,X2)),multiply(X2,multiply(X2,X2)))))) = multiply(multiply(X0,X0),multiply(multiply(multiply(X0,X0),multiply(X0,X0)),multiply(X1,X2))),
inference(superposition,[status(thm)],[c_69,c_69]) ).
tcf(c_705,plain,
! [X0: $i] : multiply(iPr_def_11,multiply(multiply(iPr_def_11,multiply(iPr_def_11,multiply(X0,iPr_def_11))),iPr_def_11)) = X0,
inference(superposition,[status(thm)],[c_101,c_697]) ).
tcf(c_709,plain,
! [X0: $i,X1: $i] : multiply(multiply(X0,X0),multiply(multiply(multiply(X0,X0),multiply(X0,X0)),multiply(X1,iPr_def_11))) = multiply(X0,multiply(multiply(X0,X1),iPr_def_11)),
inference(superposition,[status(thm)],[c_697,c_697]) ).
tcf(c_714,plain,
! [X0: $i] : multiply(iPr_def_11,multiply(multiply(iPr_def_11,X0),iPr_def_11)) = multiply(iPr_def_11,multiply(iPr_def_11,multiply(X0,iPr_def_11))),
inference(superposition,[status(thm)],[c_705,c_705]) ).
tcf(c_716,plain,
! [X0: $i] : multiply(iPr_def_11,multiply(iPr_def_11,multiply(multiply(iPr_def_11,multiply(X0,iPr_def_11)),iPr_def_11))) = X0,
inference(demodulation,[status(thm)],[c_705,c_714]) ).
tcf(c_717,plain,
! [X0: $i] : multiply(iPr_def_11,multiply(iPr_def_11,multiply(iPr_def_11,multiply(multiply(X0,iPr_def_11),iPr_def_11)))) = X0,
inference(demodulation,[status(thm)],[c_716,c_714]) ).
tcf(c_731,plain,
! [X0: $i] : multiply(iPr_def_11,multiply(multiply(iPr_def_11,multiply(iPr_def_11,multiply(X0,iPr_def_11))),iPr_def_11)) = multiply(iPr_def_11,multiply(iPr_def_11,multiply(multiply(multiply(iPr_def_11,X0),iPr_def_11),iPr_def_11))),
inference(superposition,[status(thm)],[c_714,c_714]) ).
tcf(c_736,plain,
! [X0: $i] : multiply(iPr_def_11,multiply(iPr_def_11,multiply(multiply(multiply(iPr_def_11,X0),iPr_def_11),iPr_def_11))) = multiply(iPr_def_11,multiply(iPr_def_11,multiply(iPr_def_11,multiply(multiply(X0,iPr_def_11),iPr_def_11)))),
inference(demodulation,[status(thm)],[c_731,c_714]) ).
tcf(c_737,plain,
! [X0: $i] : multiply(iPr_def_11,multiply(iPr_def_11,multiply(multiply(multiply(iPr_def_11,X0),iPr_def_11),iPr_def_11))) = X0,
inference(demodulation,[status(thm)],[c_736,c_717]) ).
tcf(c_755,plain,
! [X0: $i] : multiply(iPr_def_11,multiply(iPr_def_11,multiply(multiply(multiply(iPr_def_11,multiply(iPr_def_11,multiply(X0,iPr_def_11))),iPr_def_11),iPr_def_11))) = multiply(multiply(iPr_def_11,X0),iPr_def_11),
inference(superposition,[status(thm)],[c_714,c_737]) ).
tcf(c_760,plain,
! [X0: $i] : multiply(iPr_def_11,multiply(multiply(multiply(iPr_def_11,X0),iPr_def_11),iPr_def_11)) = multiply(iPr_def_11,multiply(iPr_def_11,multiply(multiply(X0,iPr_def_11),iPr_def_11))),
inference(superposition,[status(thm)],[c_737,c_737]) ).
tcf(c_763,plain,
! [X0: $i] : multiply(multiply(iPr_def_11,X0),iPr_def_11) = multiply(iPr_def_11,multiply(X0,iPr_def_11)),
inference(demodulation,[status(thm)],[c_755,c_737]) ).
tcf(c_779,plain,
! [X0: $i,X1: $i] : multiply(X0,multiply(multiply(X0,multiply(multiply(X0,X0),multiply(iPr_def_11,multiply(X1,iPr_def_11)))),iPr_def_11)) = multiply(iPr_def_11,X1),
inference(superposition,[status(thm)],[c_763,c_697]) ).
tcf(c_812,plain,
! [X0: $i] : multiply(iPr_def_11,multiply(multiply(iPr_def_11,multiply(X0,iPr_def_11)),iPr_def_11)) = multiply(iPr_def_11,multiply(iPr_def_11,multiply(multiply(X0,iPr_def_11),iPr_def_11))),
inference(light_normalisation,[status(thm)],[c_760,c_763]) ).
tcf(c_830,plain,
! [X0: $i,X1: $i] : multiply(X0,multiply(multiply(X0,multiply(multiply(X0,X0),X1)),iPr_def_11)) = multiply(iPr_def_11,multiply(iPr_def_11,multiply(multiply(iPr_def_11,iPr_def_11),multiply(X1,iPr_def_11)))),
inference(superposition,[status(thm)],[c_697,c_779]) ).
tcf(c_845,plain,
! [X0: $i,X1: $i] : multiply(X0,multiply(multiply(X0,multiply(multiply(X0,X0),X1)),iPr_def_11)) = multiply(iPr_def_11,multiply(iPr_def_11,multiply(iPr_def_11,multiply(X1,iPr_def_11)))),
inference(demodulation,[status(thm)],[c_830,c_101]) ).
tcf(c_924,plain,
! [X0: $i,X1: $i] : multiply(multiply(X0,X0),multiply(multiply(X0,multiply(multiply(X0,X1),iPr_def_11)),multiply(iPr_def_11,multiply(iPr_def_11,iPr_def_11)))) = X1,
inference(superposition,[status(thm)],[c_709,c_69]) ).
tcf(c_927,plain,
! [X0: $i,X1: $i] : multiply(multiply(X0,X0),multiply(multiply(X0,multiply(multiply(X0,X1),iPr_def_11)),iPr_def_11)) = X1,
inference(demodulation,[status(thm)],[c_924,c_101]) ).
tcf(c_953,plain,
! [X0: $i,X1: $i] : multiply(multiply(X0,X0),multiply(multiply(X0,multiply(multiply(iPr_def_11,multiply(iPr_def_11,multiply(iPr_def_11,multiply(X1,iPr_def_11)))),iPr_def_11)),iPr_def_11)) = multiply(multiply(X0,multiply(multiply(X0,X0),X1)),iPr_def_11),
inference(superposition,[status(thm)],[c_845,c_927]) ).
tcf(c_963,plain,
! [X0: $i,X1: $i] : multiply(multiply(X0,multiply(multiply(X0,X0),X1)),iPr_def_11) = multiply(multiply(X0,X0),multiply(multiply(X0,X1),iPr_def_11)),
inference(demodulation,[status(thm)],[c_953,c_717,c_763,c_812]) ).
tcf(c_970,plain,
! [X0: $i,X1: $i] : multiply(X0,multiply(multiply(X0,X0),multiply(multiply(X0,X1),iPr_def_11))) = multiply(iPr_def_11,multiply(iPr_def_11,multiply(iPr_def_11,multiply(X1,iPr_def_11)))),
inference(demodulation,[status(thm)],[c_845,c_963]) ).
tcf(c_1062,plain,
! [X0: $i,X1: $i] : multiply(multiply(X0,X0),multiply(multiply(X0,multiply(multiply(multiply(X0,X0),multiply(X0,X0)),multiply(X1,iPr_def_11))),iPr_def_11)) = multiply(multiply(X0,multiply(X0,multiply(multiply(X0,X1),iPr_def_11))),iPr_def_11),
inference(superposition,[status(thm)],[c_709,c_963]) ).
tcf(c_4062,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(multiply(X0,X0),multiply(multiply(X0,multiply(multiply(multiply(X0,X0),multiply(multiply(multiply(X0,X0),multiply(X0,X0)),multiply(X1,X2))),iPr_def_11)),iPr_def_11)) = multiply(multiply(X0,X1),multiply(multiply(X2,multiply(X2,X2)),multiply(multiply(X2,multiply(X2,X2)),multiply(X2,multiply(X2,X2))))),
inference(superposition,[status(thm)],[c_699,c_927]) ).
tcf(c_4106,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(multiply(X0,X1),multiply(multiply(X2,multiply(X2,X2)),multiply(multiply(X2,multiply(X2,X2)),multiply(X2,multiply(X2,X2))))) = multiply(multiply(X0,multiply(iPr_def_11,multiply(iPr_def_11,multiply(iPr_def_11,multiply(multiply(X1,X2),iPr_def_11))))),iPr_def_11),
inference(demodulation,[status(thm)],[c_4062,c_963,c_970,c_1062]) ).
tcf(c_6288,plain,
multiply(iPr_def_11,a) = iPr_def_10,
inference(light_normalisation,[status(thm)],[c_65,c_68]) ).
tcf(c_6293,plain,
! [X0: $i] : multiply(X0,multiply(multiply(X0,multiply(multiply(X0,X0),iPr_def_10)),multiply(a,multiply(a,a)))) = iPr_def_11,
inference(superposition,[status(thm)],[c_6288,c_69]) ).
tcf(c_6294,plain,
! [X0: $i] : multiply(X0,multiply(multiply(X0,multiply(multiply(X0,X0),iPr_def_11)),iPr_def_11)) = iPr_def_11,
inference(superposition,[status(thm)],[c_101,c_69]) ).
tcf(c_6295,plain,
! [X0: $i,X1: $i] : multiply(X0,multiply(multiply(X0,multiply(multiply(X0,X0),multiply(X1,iPr_def_11))),iPr_def_11)) = X1,
inference(superposition,[status(thm)],[c_101,c_69]) ).
tcf(c_6296,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : multiply(X0,multiply(multiply(X0,multiply(multiply(X0,X0),X1)),multiply(multiply(multiply(X2,multiply(multiply(X2,X2),multiply(X1,X3))),multiply(X3,multiply(X3,X3))),multiply(multiply(multiply(X2,multiply(multiply(X2,X2),multiply(X1,X3))),multiply(X3,multiply(X3,X3))),multiply(multiply(X2,multiply(multiply(X2,X2),multiply(X1,X3))),multiply(X3,multiply(X3,X3))))))) = X2,
inference(superposition,[status(thm)],[c_69,c_69]) ).
tcf(c_6300,plain,
! [X0: $i] : multiply(multiply(X0,X0),multiply(multiply(multiply(X0,X0),multiply(X0,X0)),iPr_def_11)) = multiply(X0,multiply(multiply(X0,iPr_def_11),multiply(iPr_def_11,multiply(iPr_def_11,iPr_def_11)))),
inference(superposition,[status(thm)],[c_6294,c_69]) ).
tcf(c_6301,plain,
! [X0: $i] : multiply(multiply(X0,X0),multiply(multiply(multiply(X0,X0),multiply(X0,X0)),iPr_def_11)) = multiply(X0,multiply(multiply(X0,iPr_def_11),iPr_def_11)),
inference(demodulation,[status(thm)],[c_6300,c_101]) ).
tcf(c_6304,plain,
! [X0: $i] : multiply(iPr_def_11,multiply(multiply(iPr_def_11,multiply(iPr_def_11,multiply(X0,iPr_def_11))),iPr_def_11)) = X0,
inference(superposition,[status(thm)],[c_101,c_6295]) ).
tcf(c_6308,plain,
! [X0: $i,X1: $i] : multiply(multiply(X0,X0),multiply(multiply(multiply(X0,X0),multiply(X0,X0)),multiply(X1,iPr_def_11))) = multiply(X0,multiply(multiply(X0,X1),iPr_def_11)),
inference(superposition,[status(thm)],[c_6295,c_6295]) ).
tcf(c_6313,plain,
! [X0: $i] : multiply(iPr_def_11,multiply(multiply(iPr_def_11,X0),iPr_def_11)) = multiply(iPr_def_11,multiply(iPr_def_11,multiply(X0,iPr_def_11))),
inference(superposition,[status(thm)],[c_6304,c_6304]) ).
tcf(c_6315,plain,
! [X0: $i] : multiply(iPr_def_11,multiply(iPr_def_11,multiply(multiply(iPr_def_11,multiply(X0,iPr_def_11)),iPr_def_11))) = X0,
inference(demodulation,[status(thm)],[c_6304,c_6313]) ).
tcf(c_6316,plain,
! [X0: $i] : multiply(iPr_def_11,multiply(iPr_def_11,multiply(iPr_def_11,multiply(multiply(X0,iPr_def_11),iPr_def_11)))) = X0,
inference(demodulation,[status(thm)],[c_6315,c_6313]) ).
tcf(c_6321,plain,
multiply(iPr_def_11,multiply(iPr_def_11,multiply(a,iPr_def_11))) = multiply(iPr_def_11,multiply(iPr_def_10,iPr_def_11)),
inference(superposition,[status(thm)],[c_6288,c_6313]) ).
tcf(c_6330,plain,
! [X0: $i] : multiply(iPr_def_11,multiply(multiply(iPr_def_11,multiply(iPr_def_11,multiply(X0,iPr_def_11))),iPr_def_11)) = multiply(iPr_def_11,multiply(iPr_def_11,multiply(multiply(multiply(iPr_def_11,X0),iPr_def_11),iPr_def_11))),
inference(superposition,[status(thm)],[c_6313,c_6313]) ).
tcf(c_6335,plain,
! [X0: $i] : multiply(iPr_def_11,multiply(iPr_def_11,multiply(multiply(multiply(iPr_def_11,X0),iPr_def_11),iPr_def_11))) = multiply(iPr_def_11,multiply(iPr_def_11,multiply(iPr_def_11,multiply(multiply(X0,iPr_def_11),iPr_def_11)))),
inference(demodulation,[status(thm)],[c_6330,c_6313]) ).
tcf(c_6336,plain,
! [X0: $i] : multiply(iPr_def_11,multiply(iPr_def_11,multiply(multiply(multiply(iPr_def_11,X0),iPr_def_11),iPr_def_11))) = X0,
inference(demodulation,[status(thm)],[c_6335,c_6316]) ).
tcf(c_6341,plain,
multiply(iPr_def_11,multiply(iPr_def_11,multiply(multiply(iPr_def_11,multiply(a,iPr_def_11)),iPr_def_11))) = multiply(iPr_def_11,multiply(multiply(iPr_def_11,multiply(iPr_def_10,iPr_def_11)),iPr_def_11)),
inference(superposition,[status(thm)],[c_6321,c_6313]) ).
tcf(c_6342,plain,
multiply(iPr_def_11,multiply(iPr_def_11,multiply(multiply(iPr_def_10,iPr_def_11),iPr_def_11))) = a,
inference(demodulation,[status(thm)],[c_6341,c_6313,c_6316]) ).
tcf(c_6344,plain,
multiply(iPr_def_11,multiply(iPr_def_11,multiply(multiply(iPr_def_11,multiply(multiply(iPr_def_10,iPr_def_11),iPr_def_11)),iPr_def_11))) = multiply(iPr_def_11,multiply(a,iPr_def_11)),
inference(superposition,[status(thm)],[c_6342,c_6313]) ).
tcf(c_6346,plain,
multiply(iPr_def_11,multiply(a,iPr_def_11)) = multiply(iPr_def_10,iPr_def_11),
inference(demodulation,[status(thm)],[c_6344,c_6313,c_6316]) ).
tcf(c_6350,plain,
! [X0: $i,X1: $i] : multiply(multiply(iPr_def_11,multiply(multiply(iPr_def_11,iPr_def_11),multiply(X0,X1))),multiply(X1,multiply(X1,X1))) = multiply(iPr_def_11,multiply(iPr_def_11,multiply(multiply(X0,iPr_def_11),iPr_def_11))),
inference(superposition,[status(thm)],[c_69,c_6336]) ).
tcf(c_6354,plain,
! [X0: $i] : multiply(iPr_def_11,multiply(iPr_def_11,multiply(multiply(multiply(iPr_def_11,multiply(iPr_def_11,multiply(X0,iPr_def_11))),iPr_def_11),iPr_def_11))) = multiply(multiply(iPr_def_11,X0),iPr_def_11),
inference(superposition,[status(thm)],[c_6313,c_6336]) ).
tcf(c_6359,plain,
! [X0: $i] : multiply(iPr_def_11,multiply(multiply(multiply(iPr_def_11,X0),iPr_def_11),iPr_def_11)) = multiply(iPr_def_11,multiply(iPr_def_11,multiply(multiply(X0,iPr_def_11),iPr_def_11))),
inference(superposition,[status(thm)],[c_6336,c_6336]) ).
tcf(c_6362,plain,
! [X0: $i] : multiply(multiply(iPr_def_11,X0),iPr_def_11) = multiply(iPr_def_11,multiply(X0,iPr_def_11)),
inference(demodulation,[status(thm)],[c_6354,c_6336]) ).
tcf(c_6364,plain,
! [X0: $i,X1: $i] : multiply(multiply(iPr_def_11,multiply(iPr_def_11,multiply(X0,X1))),multiply(X1,multiply(X1,X1))) = multiply(iPr_def_11,multiply(iPr_def_11,multiply(multiply(X0,iPr_def_11),iPr_def_11))),
inference(demodulation,[status(thm)],[c_6350,c_101]) ).
tcf(c_6378,plain,
! [X0: $i,X1: $i] : multiply(X0,multiply(multiply(X0,multiply(multiply(X0,X0),multiply(iPr_def_11,multiply(X1,iPr_def_11)))),iPr_def_11)) = multiply(iPr_def_11,X1),
inference(superposition,[status(thm)],[c_6362,c_6295]) ).
tcf(c_6399,plain,
! [X0: $i] : multiply(X0,multiply(multiply(X0,iPr_def_11),multiply(multiply(a,multiply(a,a)),multiply(multiply(a,multiply(a,a)),multiply(a,multiply(a,a)))))) = multiply(multiply(X0,X0),multiply(multiply(multiply(X0,X0),multiply(X0,X0)),iPr_def_10)),
inference(superposition,[status(thm)],[c_6293,c_69]) ).
tcf(c_6400,plain,
multiply(iPr_def_11,multiply(multiply(multiply(iPr_def_11,multiply(multiply(iPr_def_11,iPr_def_11),iPr_def_10)),multiply(a,multiply(a,a))),iPr_def_11)) = multiply(iPr_def_11,iPr_def_11),
inference(superposition,[status(thm)],[c_6293,c_6362]) ).
tcf(c_6401,plain,
multiply(iPr_def_11,multiply(multiply(multiply(iPr_def_11,multiply(iPr_def_11,iPr_def_10)),multiply(a,multiply(a,a))),iPr_def_11)) = iPr_def_11,
inference(demodulation,[status(thm)],[c_6400,c_101]) ).
tcf(c_6402,plain,
! [X0: $i] : multiply(X0,multiply(multiply(X0,multiply(iPr_def_11,multiply(iPr_def_11,multiply(iPr_def_11,multiply(iPr_def_10,iPr_def_11))))),iPr_def_11)) = multiply(multiply(X0,X0),multiply(multiply(multiply(X0,X0),multiply(X0,X0)),iPr_def_10)),
inference(demodulation,[status(thm)],[c_6399,c_6346,c_6362,c_4106]) ).
tcf(c_6410,plain,
multiply(iPr_def_11,multiply(multiply(multiply(multiply(iPr_def_11,multiply(iPr_def_11,iPr_def_10)),multiply(a,multiply(a,a))),iPr_def_11),iPr_def_11)) = multiply(iPr_def_11,iPr_def_11),
inference(superposition,[status(thm)],[c_6401,c_6362]) ).
tcf(c_6411,plain,
multiply(iPr_def_11,multiply(multiply(multiply(multiply(iPr_def_11,multiply(iPr_def_11,iPr_def_10)),multiply(a,multiply(a,a))),iPr_def_11),iPr_def_11)) = iPr_def_11,
inference(demodulation,[status(thm)],[c_6410,c_101]) ).
tcf(c_6412,plain,
! [X0: $i] : multiply(iPr_def_11,multiply(multiply(iPr_def_11,multiply(X0,iPr_def_11)),iPr_def_11)) = multiply(iPr_def_11,multiply(iPr_def_11,multiply(multiply(X0,iPr_def_11),iPr_def_11))),
inference(light_normalisation,[status(thm)],[c_6359,c_6362]) ).
tcf(c_6430,plain,
! [X0: $i,X1: $i] : multiply(X0,multiply(multiply(X0,multiply(multiply(X0,X0),X1)),iPr_def_11)) = multiply(iPr_def_11,multiply(iPr_def_11,multiply(multiply(iPr_def_11,iPr_def_11),multiply(X1,iPr_def_11)))),
inference(superposition,[status(thm)],[c_6295,c_6378]) ).
tcf(c_6445,plain,
! [X0: $i,X1: $i] : multiply(X0,multiply(multiply(X0,multiply(multiply(X0,X0),X1)),iPr_def_11)) = multiply(iPr_def_11,multiply(iPr_def_11,multiply(iPr_def_11,multiply(X1,iPr_def_11)))),
inference(demodulation,[status(thm)],[c_6430,c_101]) ).
tcf(c_6461,plain,
multiply(multiply(iPr_def_11,multiply(iPr_def_11,iPr_def_10)),multiply(a,multiply(a,a))) = multiply(iPr_def_11,multiply(iPr_def_11,iPr_def_11)),
inference(superposition,[status(thm)],[c_6411,c_6316]) ).
tcf(c_6462,plain,
multiply(multiply(iPr_def_11,multiply(iPr_def_11,iPr_def_10)),multiply(a,multiply(a,a))) = iPr_def_11,
inference(demodulation,[status(thm)],[c_6461,c_101]) ).
tcf(c_6525,plain,
! [X0: $i,X1: $i] : multiply(multiply(X0,X0),multiply(multiply(X0,multiply(multiply(X0,X1),iPr_def_11)),multiply(iPr_def_11,multiply(iPr_def_11,iPr_def_11)))) = X1,
inference(superposition,[status(thm)],[c_6308,c_69]) ).
tcf(c_6528,plain,
! [X0: $i,X1: $i] : multiply(multiply(X0,X0),multiply(multiply(X0,multiply(multiply(X0,X1),iPr_def_11)),iPr_def_11)) = X1,
inference(demodulation,[status(thm)],[c_6525,c_101]) ).
tcf(c_6538,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(multiply(X0,multiply(multiply(X0,X0),multiply(X1,X2))),multiply(X2,multiply(X2,X2))) = multiply(multiply(X0,X0),multiply(multiply(X0,multiply(X1,iPr_def_11)),iPr_def_11)),
inference(superposition,[status(thm)],[c_69,c_6528]) ).
tcf(c_6540,plain,
! [X0: $i] : multiply(multiply(X0,multiply(multiply(X0,X0),iPr_def_10)),multiply(a,multiply(a,a))) = multiply(multiply(X0,X0),multiply(multiply(X0,multiply(iPr_def_11,iPr_def_11)),iPr_def_11)),
inference(superposition,[status(thm)],[c_6293,c_6528]) ).
tcf(c_6552,plain,
multiply(multiply(multiply(iPr_def_11,multiply(iPr_def_11,iPr_def_10)),multiply(iPr_def_11,multiply(iPr_def_11,iPr_def_10))),multiply(multiply(multiply(iPr_def_11,multiply(iPr_def_11,iPr_def_10)),multiply(iPr_def_11,iPr_def_11)),iPr_def_11)) = multiply(a,multiply(a,a)),
inference(superposition,[status(thm)],[c_6462,c_6528]) ).
tcf(c_6554,plain,
! [X0: $i,X1: $i] : multiply(multiply(X0,X0),multiply(multiply(X0,multiply(multiply(iPr_def_11,multiply(iPr_def_11,multiply(iPr_def_11,multiply(X1,iPr_def_11)))),iPr_def_11)),iPr_def_11)) = multiply(multiply(X0,multiply(multiply(X0,X0),X1)),iPr_def_11),
inference(superposition,[status(thm)],[c_6445,c_6528]) ).
tcf(c_6559,plain,
! [X0: $i,X1: $i] : multiply(multiply(multiply(X0,X0),multiply(X0,X0)),multiply(multiply(multiply(X0,X0),multiply(X1,iPr_def_11)),iPr_def_11)) = multiply(multiply(X0,multiply(multiply(X0,X1),iPr_def_11)),iPr_def_11),
inference(superposition,[status(thm)],[c_6528,c_6528]) ).
tcf(c_6562,plain,
! [X0: $i] : multiply(multiply(X0,multiply(multiply(X0,X0),iPr_def_10)),multiply(a,multiply(a,a))) = multiply(multiply(X0,X0),multiply(multiply(X0,iPr_def_11),iPr_def_11)),
inference(demodulation,[status(thm)],[c_6540,c_101]) ).
tcf(c_6564,plain,
! [X0: $i,X1: $i] : multiply(multiply(X0,multiply(multiply(X0,X0),X1)),iPr_def_11) = multiply(multiply(X0,X0),multiply(multiply(X0,X1),iPr_def_11)),
inference(demodulation,[status(thm)],[c_6554,c_6316,c_6362,c_6412]) ).
tcf(c_6566,plain,
multiply(multiply(multiply(iPr_def_11,multiply(iPr_def_11,iPr_def_10)),multiply(iPr_def_11,multiply(iPr_def_11,iPr_def_10))),a) = multiply(a,multiply(a,a)),
inference(demodulation,[status(thm)],[c_6552,c_101,c_6342,c_6362,c_6412]) ).
tcf(c_6570,plain,
! [X0: $i] : multiply(X0,multiply(multiply(X0,X0),multiply(multiply(X0,iPr_def_11),iPr_def_11))) = iPr_def_11,
inference(demodulation,[status(thm)],[c_6293,c_6562]) ).
tcf(c_6571,plain,
! [X0: $i,X1: $i] : multiply(X0,multiply(multiply(X0,X0),multiply(multiply(X0,X1),iPr_def_11))) = multiply(iPr_def_11,multiply(iPr_def_11,multiply(iPr_def_11,multiply(X1,iPr_def_11)))),
inference(demodulation,[status(thm)],[c_6445,c_6564]) ).
tcf(c_6574,plain,
! [X0: $i] : multiply(multiply(iPr_def_11,X0),multiply(multiply(multiply(iPr_def_11,X0),multiply(iPr_def_11,X0)),multiply(multiply(iPr_def_11,multiply(X0,iPr_def_11)),iPr_def_11))) = iPr_def_11,
inference(superposition,[status(thm)],[c_6362,c_6570]) ).
tcf(c_6578,plain,
! [X0: $i] : multiply(multiply(iPr_def_11,X0),multiply(multiply(multiply(iPr_def_11,X0),multiply(iPr_def_11,X0)),multiply(iPr_def_11,multiply(multiply(X0,iPr_def_11),iPr_def_11)))) = iPr_def_11,
inference(demodulation,[status(thm)],[c_6574,c_6362]) ).
tcf(c_6595,plain,
! [X0: $i] : multiply(multiply(multiply(X0,X0),multiply(X0,X0)),multiply(multiply(multiply(X0,X0),iPr_def_11),iPr_def_11)) = multiply(multiply(X0,multiply(multiply(X0,iPr_def_11),iPr_def_11)),iPr_def_11),
inference(superposition,[status(thm)],[c_6301,c_6564]) ).
tcf(c_6613,plain,
! [X0: $i,X1: $i] : multiply(iPr_def_11,multiply(iPr_def_11,multiply(iPr_def_11,multiply(multiply(multiply(X0,X0),multiply(multiply(X0,X1),iPr_def_11)),iPr_def_11)))) = multiply(X0,multiply(multiply(X0,X0),X1)),
inference(superposition,[status(thm)],[c_6564,c_6316]) ).
tcf(c_6617,plain,
! [X0: $i] : multiply(multiply(X0,X0),multiply(multiply(X0,X0),multiply(multiply(X0,iPr_def_11),iPr_def_11))) = X0,
inference(superposition,[status(thm)],[c_6564,c_6528]) ).
tcf(c_6629,plain,
multiply(multiply(multiply(iPr_def_11,multiply(iPr_def_11,iPr_def_10)),multiply(iPr_def_11,multiply(iPr_def_11,iPr_def_10))),multiply(multiply(multiply(iPr_def_11,multiply(iPr_def_11,iPr_def_10)),a),iPr_def_11)) = multiply(multiply(multiply(iPr_def_11,multiply(iPr_def_11,iPr_def_10)),multiply(a,multiply(a,a))),iPr_def_11),
inference(superposition,[status(thm)],[c_6566,c_6564]) ).
tcf(c_6630,plain,
multiply(multiply(multiply(iPr_def_11,multiply(iPr_def_11,iPr_def_10)),multiply(iPr_def_11,multiply(iPr_def_11,iPr_def_10))),multiply(multiply(multiply(iPr_def_11,multiply(iPr_def_11,iPr_def_10)),a),iPr_def_11)) = iPr_def_11,
inference(demodulation,[status(thm)],[c_6629,c_101,c_6462]) ).
tcf(c_6727,plain,
! [X0: $i] : multiply(X0,multiply(multiply(multiply(X0,iPr_def_11),iPr_def_11),multiply(multiply(multiply(X0,iPr_def_11),iPr_def_11),multiply(multiply(X0,iPr_def_11),iPr_def_11)))) = multiply(iPr_def_11,multiply(iPr_def_11,multiply(multiply(iPr_def_11,iPr_def_11),iPr_def_11))),
inference(superposition,[status(thm)],[c_6316,c_6364]) ).
tcf(c_6770,plain,
! [X0: $i] : multiply(X0,multiply(multiply(multiply(X0,iPr_def_11),iPr_def_11),multiply(multiply(multiply(X0,iPr_def_11),iPr_def_11),multiply(multiply(X0,iPr_def_11),iPr_def_11)))) = iPr_def_11,
inference(demodulation,[status(thm)],[c_6727,c_101,c_6362]) ).
tcf(c_6802,plain,
! [X0: $i] : multiply(multiply(multiply(X0,iPr_def_11),iPr_def_11),multiply(multiply(multiply(X0,iPr_def_11),iPr_def_11),multiply(multiply(X0,iPr_def_11),iPr_def_11))) = multiply(multiply(X0,X0),multiply(multiply(X0,multiply(iPr_def_11,iPr_def_11)),iPr_def_11)),
inference(superposition,[status(thm)],[c_6770,c_6528]) ).
tcf(c_6807,plain,
! [X0: $i] : multiply(multiply(multiply(X0,iPr_def_11),iPr_def_11),multiply(multiply(multiply(X0,iPr_def_11),iPr_def_11),multiply(multiply(X0,iPr_def_11),iPr_def_11))) = multiply(multiply(X0,X0),multiply(multiply(X0,iPr_def_11),iPr_def_11)),
inference(demodulation,[status(thm)],[c_6802,c_101]) ).
tcf(c_7108,plain,
! [X0: $i] : multiply(iPr_def_11,multiply(multiply(multiply(X0,iPr_def_11),iPr_def_11),multiply(multiply(multiply(X0,iPr_def_11),iPr_def_11),multiply(multiply(X0,iPr_def_11),iPr_def_11)))) = multiply(multiply(multiply(iPr_def_11,X0),multiply(iPr_def_11,X0)),multiply(multiply(multiply(iPr_def_11,X0),multiply(iPr_def_11,iPr_def_11)),iPr_def_11)),
inference(superposition,[status(thm)],[c_6578,c_6538]) ).
tcf(c_7166,plain,
! [X0: $i] : multiply(multiply(multiply(iPr_def_11,X0),multiply(iPr_def_11,X0)),multiply(iPr_def_11,multiply(multiply(X0,iPr_def_11),iPr_def_11))) = multiply(iPr_def_11,multiply(multiply(X0,X0),multiply(multiply(X0,iPr_def_11),iPr_def_11))),
inference(demodulation,[status(thm)],[c_7108,c_101,c_6362,c_6807]) ).
tcf(c_7193,plain,
! [X0: $i] : multiply(multiply(iPr_def_11,X0),multiply(iPr_def_11,multiply(multiply(X0,X0),multiply(multiply(X0,iPr_def_11),iPr_def_11)))) = iPr_def_11,
inference(demodulation,[status(thm)],[c_6578,c_7166]) ).
tcf(c_7211,plain,
! [X0: $i] : multiply(multiply(iPr_def_11,multiply(X0,X0)),multiply(iPr_def_11,multiply(multiply(X0,multiply(multiply(X0,iPr_def_11),iPr_def_11)),iPr_def_11))) = iPr_def_11,
inference(superposition,[status(thm)],[c_6595,c_7193]) ).
tcf(c_7219,plain,
! [X0: $i] : multiply(iPr_def_11,multiply(iPr_def_11,multiply(iPr_def_11,multiply(multiply(iPr_def_11,multiply(multiply(X0,X0),multiply(multiply(X0,iPr_def_11),iPr_def_11))),iPr_def_11)))) = multiply(multiply(iPr_def_11,X0),multiply(multiply(multiply(iPr_def_11,X0),multiply(iPr_def_11,X0)),multiply(iPr_def_11,iPr_def_11))),
inference(superposition,[status(thm)],[c_7193,c_6571]) ).
tcf(c_7224,plain,
! [X0: $i] : multiply(multiply(iPr_def_11,X0),multiply(multiply(multiply(iPr_def_11,X0),multiply(iPr_def_11,X0)),iPr_def_11)) = multiply(iPr_def_11,multiply(X0,multiply(multiply(X0,X0),iPr_def_11))),
inference(demodulation,[status(thm)],[c_7219,c_101,c_6362,c_6613]) ).
tcf(c_7375,plain,
multiply(iPr_def_11,multiply(a,multiply(multiply(a,a),iPr_def_11))) = multiply(iPr_def_10,multiply(multiply(iPr_def_10,iPr_def_10),iPr_def_11)),
inference(superposition,[status(thm)],[c_6288,c_7224]) ).
tcf(c_7425,plain,
multiply(multiply(iPr_def_11,iPr_def_11),multiply(multiply(iPr_def_11,multiply(multiply(iPr_def_10,multiply(multiply(iPr_def_10,iPr_def_10),iPr_def_11)),iPr_def_11)),iPr_def_11)) = multiply(a,multiply(multiply(a,a),iPr_def_11)),
inference(superposition,[status(thm)],[c_7375,c_6528]) ).
tcf(c_7432,plain,
multiply(iPr_def_11,multiply(iPr_def_11,multiply(multiply(multiply(iPr_def_10,iPr_def_10),multiply(multiply(iPr_def_10,iPr_def_11),iPr_def_11)),iPr_def_11))) = multiply(a,multiply(multiply(a,a),iPr_def_11)),
inference(demodulation,[status(thm)],[c_7425,c_101,c_6362,c_6564]) ).
tcf(c_8151,plain,
multiply(multiply(multiply(multiply(iPr_def_11,iPr_def_11),multiply(multiply(multiply(iPr_def_11,iPr_def_11),multiply(iPr_def_11,iPr_def_11)),iPr_def_10)),multiply(multiply(iPr_def_11,iPr_def_11),multiply(multiply(multiply(iPr_def_11,iPr_def_11),multiply(iPr_def_11,iPr_def_11)),iPr_def_10))),multiply(iPr_def_11,multiply(multiply(multiply(multiply(iPr_def_11,multiply(iPr_def_11,multiply(iPr_def_11,multiply(iPr_def_11,multiply(iPr_def_10,iPr_def_11))))),iPr_def_11),iPr_def_11),iPr_def_11))) = multiply(iPr_def_11,multiply(multiply(multiply(multiply(iPr_def_11,multiply(iPr_def_11,multiply(iPr_def_11,multiply(iPr_def_11,multiply(iPr_def_10,iPr_def_11))))),iPr_def_11),multiply(multiply(iPr_def_11,multiply(iPr_def_11,multiply(iPr_def_11,multiply(iPr_def_11,multiply(iPr_def_10,iPr_def_11))))),iPr_def_11)),multiply(multiply(multiply(multiply(iPr_def_11,multiply(iPr_def_11,multiply(iPr_def_11,multiply(iPr_def_11,multiply(iPr_def_10,iPr_def_11))))),iPr_def_11),iPr_def_11),iPr_def_11))),
inference(superposition,[status(thm)],[c_6402,c_7166]) ).
tcf(c_8179,plain,
multiply(iPr_def_11,multiply(iPr_def_11,multiply(multiply(iPr_def_10,iPr_def_10),multiply(multiply(iPr_def_10,iPr_def_11),iPr_def_11)))) = multiply(a,multiply(a,a)),
inference(demodulation,[status(thm)],[c_8151,c_6288,c_101,c_6342,c_6362,c_6412,c_6566,c_7166]) ).
tcf(c_8196,plain,
multiply(iPr_def_11,multiply(multiply(iPr_def_11,multiply(multiply(iPr_def_10,iPr_def_10),multiply(multiply(iPr_def_10,iPr_def_11),iPr_def_11))),iPr_def_11)) = multiply(multiply(a,multiply(a,a)),iPr_def_11),
inference(superposition,[status(thm)],[c_8179,c_6362]) ).
tcf(c_8201,plain,
multiply(multiply(a,multiply(a,a)),iPr_def_11) = multiply(a,multiply(multiply(a,a),iPr_def_11)),
inference(demodulation,[status(thm)],[c_8196,c_6362,c_7432]) ).
tcf(c_8246,plain,
multiply(a,multiply(multiply(a,a),multiply(a,multiply(multiply(a,a),iPr_def_11)))) = multiply(iPr_def_11,multiply(iPr_def_11,multiply(iPr_def_11,multiply(multiply(a,a),iPr_def_11)))),
inference(superposition,[status(thm)],[c_8201,c_6571]) ).
tcf(c_8287,plain,
multiply(multiply(iPr_def_11,multiply(iPr_def_11,multiply(iPr_def_11,multiply(multiply(a,a),iPr_def_11)))),multiply(multiply(multiply(a,a),iPr_def_11),multiply(multiply(multiply(a,a),iPr_def_11),multiply(multiply(a,a),iPr_def_11)))) = multiply(multiply(a,a),multiply(multiply(a,multiply(a,iPr_def_11)),iPr_def_11)),
inference(superposition,[status(thm)],[c_8246,c_6538]) ).
tcf(c_8294,plain,
multiply(multiply(a,a),multiply(multiply(a,multiply(a,iPr_def_11)),iPr_def_11)) = iPr_def_11,
inference(demodulation,[status(thm)],[c_8287,c_101,c_6362,c_6364]) ).
tcf(c_8307,plain,
multiply(iPr_def_11,multiply(iPr_def_11,multiply(iPr_def_11,multiply(multiply(a,iPr_def_11),iPr_def_11)))) = multiply(a,iPr_def_11),
inference(superposition,[status(thm)],[c_8294,c_6571]) ).
tcf(c_8308,plain,
multiply(a,iPr_def_11) = a,
inference(demodulation,[status(thm)],[c_8307,c_6316]) ).
tcf(c_8340,plain,
multiply(iPr_def_10,iPr_def_11) = multiply(iPr_def_11,a),
inference(demodulation,[status(thm)],[c_6346,c_8308]) ).
tcf(c_8341,plain,
multiply(iPr_def_10,iPr_def_11) = iPr_def_10,
inference(demodulation,[status(thm)],[c_8340,c_6288]) ).
tcf(c_8347,plain,
multiply(iPr_def_11,multiply(iPr_def_11,multiply(iPr_def_10,iPr_def_11))) = a,
inference(demodulation,[status(thm)],[c_6342,c_8341]) ).
tcf(c_8348,plain,
multiply(iPr_def_11,multiply(iPr_def_11,iPr_def_10)) = a,
inference(demodulation,[status(thm)],[c_8347,c_8341]) ).
tcf(c_8350,plain,
multiply(multiply(a,a),multiply(multiply(a,a),iPr_def_11)) = iPr_def_11,
inference(demodulation,[status(thm)],[c_6630,c_8348]) ).
tcf(c_8351,plain,
multiply(multiply(a,a),a) = multiply(a,multiply(a,a)),
inference(demodulation,[status(thm)],[c_6566,c_8348]) ).
tcf(c_8352,plain,
multiply(a,multiply(a,multiply(a,a))) = iPr_def_11,
inference(demodulation,[status(thm)],[c_6462,c_8348]) ).
tcf(c_8389,plain,
multiply(multiply(iPr_def_11,multiply(a,a)),multiply(iPr_def_11,multiply(multiply(a,a),iPr_def_11))) = iPr_def_11,
inference(superposition,[status(thm)],[c_8308,c_7211]) ).
tcf(c_8393,plain,
multiply(multiply(a,a),multiply(multiply(a,a),a)) = a,
inference(superposition,[status(thm)],[c_8308,c_6617]) ).
tcf(c_8397,plain,
multiply(multiply(a,a),multiply(a,multiply(a,a))) = a,
inference(demodulation,[status(thm)],[c_8393,c_8351]) ).
tcf(c_8750,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : multiply(multiply(X0,multiply(multiply(X0,X0),X1)),multiply(multiply(multiply(X2,multiply(multiply(X2,X2),multiply(X1,X3))),multiply(X3,multiply(X3,X3))),multiply(multiply(multiply(X2,multiply(multiply(X2,X2),multiply(X1,X3))),multiply(X3,multiply(X3,X3))),multiply(multiply(X2,multiply(multiply(X2,X2),multiply(X1,X3))),multiply(X3,multiply(X3,X3)))))) = multiply(multiply(X0,X0),multiply(multiply(X0,multiply(X2,iPr_def_11)),iPr_def_11)),
inference(superposition,[status(thm)],[c_6296,c_6528]) ).
tcf(c_8772,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(multiply(X0,multiply(multiply(X0,X0),X1)),multiply(multiply(multiply(X2,X2),multiply(multiply(X2,multiply(X1,iPr_def_11)),iPr_def_11)),multiply(multiply(multiply(X2,X2),multiply(multiply(X2,multiply(X1,iPr_def_11)),iPr_def_11)),multiply(multiply(X2,X2),multiply(multiply(X2,multiply(X1,iPr_def_11)),iPr_def_11))))) = multiply(multiply(X0,X0),multiply(multiply(X0,multiply(X2,iPr_def_11)),iPr_def_11)),
inference(demodulation,[status(thm)],[c_8750,c_6538]) ).
tcf(c_9149,plain,
! [X0: $i,X1: $i] : multiply(multiply(iPr_def_11,multiply(iPr_def_11,multiply(iPr_def_11,multiply(iPr_def_11,multiply(multiply(multiply(iPr_def_11,multiply(iPr_def_11,multiply(multiply(X0,iPr_def_11),iPr_def_11))),X1),iPr_def_11))))),iPr_def_11) = multiply(X0,multiply(multiply(X1,multiply(X1,X1)),multiply(multiply(X1,multiply(X1,X1)),multiply(X1,multiply(X1,X1))))),
inference(superposition,[status(thm)],[c_6316,c_4106]) ).
tcf(c_9258,plain,
! [X0: $i,X1: $i] : multiply(X0,multiply(multiply(X1,multiply(X1,X1)),multiply(multiply(X1,multiply(X1,X1)),multiply(X1,multiply(X1,X1))))) = multiply(iPr_def_11,multiply(multiply(iPr_def_11,multiply(iPr_def_11,multiply(multiply(X0,iPr_def_11),iPr_def_11))),X1)),
inference(demodulation,[status(thm)],[c_9149,c_6316,c_6362,c_6412]) ).
tcf(c_10224,plain,
multiply(multiply(a,a),multiply(multiply(a,a),multiply(multiply(a,a),multiply(a,a)))) = multiply(multiply(a,a),multiply(multiply(a,multiply(a,iPr_def_11)),iPr_def_11)),
inference(superposition,[status(thm)],[c_8397,c_6538]) ).
tcf(c_10228,plain,
multiply(multiply(iPr_def_11,multiply(iPr_def_11,a)),multiply(multiply(a,multiply(a,a)),multiply(multiply(a,multiply(a,a)),multiply(a,multiply(a,a))))) = multiply(iPr_def_11,multiply(iPr_def_11,multiply(multiply(multiply(a,a),iPr_def_11),iPr_def_11))),
inference(superposition,[status(thm)],[c_8397,c_6364]) ).
tcf(c_10237,plain,
multiply(multiply(a,a),multiply(multiply(a,a),multiply(multiply(a,a),multiply(a,a)))) = iPr_def_11,
inference(demodulation,[status(thm)],[c_10224,c_8308,c_8350]) ).
tcf(c_10238,plain,
multiply(iPr_def_11,multiply(iPr_def_11,multiply(multiply(multiply(a,a),iPr_def_11),iPr_def_11))) = multiply(iPr_def_11,multiply(iPr_def_10,a)),
inference(demodulation,[status(thm)],[c_10228,c_6288,c_6362,c_8308,c_8341,c_8348,c_9258]) ).
tcf(c_10848,plain,
multiply(multiply(iPr_def_11,multiply(a,a)),multiply(multiply(multiply(iPr_def_11,multiply(a,a)),multiply(iPr_def_11,multiply(a,a))),multiply(iPr_def_11,iPr_def_11))) = multiply(iPr_def_11,multiply(iPr_def_11,multiply(iPr_def_11,multiply(multiply(iPr_def_11,multiply(multiply(a,a),iPr_def_11)),iPr_def_11)))),
inference(superposition,[status(thm)],[c_8389,c_6571]) ).
tcf(c_10850,plain,
multiply(iPr_def_11,multiply(iPr_def_11,multiply(iPr_def_11,multiply(iPr_def_10,a)))) = multiply(iPr_def_11,multiply(a,a)),
inference(demodulation,[status(thm)],[c_10848,c_101,c_6301,c_6412,c_7224,c_8308,c_10238]) ).
tcf(c_11219,plain,
multiply(multiply(iPr_def_11,iPr_def_11),multiply(multiply(iPr_def_11,multiply(multiply(iPr_def_11,multiply(a,a)),iPr_def_11)),iPr_def_11)) = multiply(iPr_def_11,multiply(iPr_def_11,multiply(iPr_def_10,a))),
inference(superposition,[status(thm)],[c_10850,c_6528]) ).
tcf(c_11235,plain,
multiply(iPr_def_11,multiply(iPr_def_11,multiply(iPr_def_10,a))) = multiply(a,a),
inference(demodulation,[status(thm)],[c_11219,c_6528]) ).
tcf(c_11276,plain,
multiply(iPr_def_11,multiply(multiply(iPr_def_11,multiply(iPr_def_10,a)),iPr_def_11)) = multiply(multiply(a,a),iPr_def_11),
inference(superposition,[status(thm)],[c_11235,c_6362]) ).
tcf(c_11279,plain,
multiply(iPr_def_11,multiply(iPr_def_11,multiply(multiply(iPr_def_10,a),iPr_def_11))) = multiply(multiply(a,a),iPr_def_11),
inference(demodulation,[status(thm)],[c_11276,c_6362]) ).
tcf(c_11339,plain,
multiply(multiply(iPr_def_11,iPr_def_11),multiply(multiply(iPr_def_11,multiply(multiply(multiply(a,a),iPr_def_11),iPr_def_11)),iPr_def_11)) = multiply(iPr_def_11,multiply(multiply(iPr_def_10,a),iPr_def_11)),
inference(superposition,[status(thm)],[c_11279,c_6528]) ).
tcf(c_11357,plain,
multiply(iPr_def_11,multiply(iPr_def_11,multiply(multiply(multiply(multiply(a,a),iPr_def_11),iPr_def_11),iPr_def_11))) = multiply(iPr_def_11,multiply(multiply(iPr_def_10,a),iPr_def_11)),
inference(demodulation,[status(thm)],[c_11339,c_101,c_6362]) ).
tcf(c_11560,plain,
multiply(multiply(multiply(a,a),multiply(a,a)),multiply(multiply(multiply(a,a),multiply(iPr_def_11,iPr_def_11)),iPr_def_11)) = multiply(multiply(a,a),multiply(multiply(a,a),multiply(a,a))),
inference(superposition,[status(thm)],[c_10237,c_6528]) ).
tcf(c_11568,plain,
multiply(multiply(a,a),multiply(multiply(a,a),multiply(a,a))) = multiply(multiply(a,a),iPr_def_11),
inference(demodulation,[status(thm)],[c_11560,c_6559,c_8308]) ).
tcf(c_11607,plain,
multiply(multiply(iPr_def_11,iPr_def_11),multiply(multiply(iPr_def_11,multiply(multiply(iPr_def_11,multiply(iPr_def_10,a)),iPr_def_11)),iPr_def_11)) = multiply(iPr_def_11,multiply(multiply(multiply(a,a),iPr_def_11),iPr_def_11)),
inference(superposition,[status(thm)],[c_10238,c_6528]) ).
tcf(c_11625,plain,
multiply(iPr_def_11,multiply(multiply(multiply(a,a),iPr_def_11),iPr_def_11)) = multiply(iPr_def_10,a),
inference(demodulation,[status(thm)],[c_11607,c_6528]) ).
tcf(c_11846,plain,
multiply(iPr_def_11,multiply(iPr_def_11,multiply(iPr_def_11,multiply(multiply(multiply(multiply(a,a),multiply(a,a)),multiply(multiply(multiply(a,a),iPr_def_11),iPr_def_11)),iPr_def_11)))) = multiply(multiply(a,a),multiply(multiply(multiply(a,a),multiply(a,a)),multiply(multiply(a,a),multiply(a,a)))),
inference(superposition,[status(thm)],[c_11568,c_6613]) ).
tcf(c_11847,plain,
multiply(multiply(iPr_def_11,multiply(iPr_def_11,multiply(multiply(a,a),iPr_def_11))),multiply(multiply(multiply(a,a),multiply(a,a)),multiply(multiply(multiply(a,a),multiply(a,a)),multiply(multiply(a,a),multiply(a,a))))) = multiply(iPr_def_11,multiply(iPr_def_11,multiply(multiply(multiply(a,a),iPr_def_11),iPr_def_11))),
inference(superposition,[status(thm)],[c_11568,c_6364]) ).
tcf(c_11849,plain,
multiply(multiply(multiply(a,a),multiply(a,a)),multiply(multiply(multiply(a,a),multiply(multiply(multiply(a,a),iPr_def_11),iPr_def_11)),iPr_def_11)) = multiply(multiply(a,a),multiply(a,a)),
inference(superposition,[status(thm)],[c_11568,c_6528]) ).
tcf(c_11860,plain,
multiply(multiply(a,a),multiply(a,a)) = iPr_def_11,
inference(demodulation,[status(thm)],[c_11849,c_101,c_6559,c_6564,c_8308,c_8351,c_8352]) ).
tcf(c_11863,plain,
multiply(iPr_def_11,multiply(iPr_def_11,multiply(iPr_def_11,multiply(multiply(iPr_def_11,multiply(multiply(multiply(a,a),iPr_def_11),iPr_def_11)),iPr_def_11)))) = multiply(multiply(a,a),multiply(iPr_def_11,iPr_def_11)),
inference(demodulation,[status(thm)],[c_11846,c_11860]) ).
tcf(c_11864,plain,
multiply(iPr_def_11,multiply(multiply(a,a),iPr_def_11)) = multiply(multiply(a,a),iPr_def_11),
inference(demodulation,[status(thm)],[c_11863,c_101,c_6412,c_11279,c_11357]) ).
tcf(c_11866,plain,
multiply(multiply(multiply(a,a),iPr_def_11),multiply(iPr_def_11,multiply(iPr_def_11,iPr_def_11))) = multiply(iPr_def_11,multiply(iPr_def_11,multiply(multiply(multiply(a,a),iPr_def_11),iPr_def_11))),
inference(demodulation,[status(thm)],[c_11847,c_11860,c_11864]) ).
tcf(c_11867,plain,
multiply(multiply(multiply(a,a),iPr_def_11),iPr_def_11) = multiply(iPr_def_11,multiply(iPr_def_10,a)),
inference(demodulation,[status(thm)],[c_11866,c_101,c_11625]) ).
tcf(c_11883,plain,
multiply(iPr_def_11,multiply(iPr_def_11,multiply(iPr_def_10,a))) = multiply(iPr_def_10,a),
inference(demodulation,[status(thm)],[c_11625,c_11867]) ).
tcf(c_11884,plain,
multiply(a,a) = multiply(iPr_def_10,a),
inference(demodulation,[status(thm)],[c_11235,c_11883]) ).
tcf(c_11928,plain,
! [X0: $i,X1: $i] : multiply(multiply(a,multiply(multiply(iPr_def_10,a),multiply(X0,X1))),multiply(X1,multiply(X1,X1))) = multiply(multiply(iPr_def_10,a),multiply(multiply(a,multiply(X0,iPr_def_11)),iPr_def_11)),
inference(superposition,[status(thm)],[c_11884,c_6538]) ).
tcf(c_11941,plain,
! [X0: $i] : multiply(multiply(X0,multiply(multiply(X0,X0),multiply(iPr_def_10,a))),multiply(a,multiply(iPr_def_10,a))) = multiply(multiply(X0,X0),multiply(multiply(X0,multiply(a,iPr_def_11)),iPr_def_11)),
inference(superposition,[status(thm)],[c_11884,c_6538]) ).
tcf(c_11942,plain,
! [X0: $i,X1: $i] : multiply(multiply(X0,multiply(multiply(X0,X0),X1)),multiply(multiply(multiply(iPr_def_10,a),multiply(multiply(a,multiply(X1,iPr_def_11)),iPr_def_11)),multiply(multiply(multiply(iPr_def_10,a),multiply(multiply(a,multiply(X1,iPr_def_11)),iPr_def_11)),multiply(multiply(iPr_def_10,a),multiply(multiply(a,multiply(X1,iPr_def_11)),iPr_def_11))))) = multiply(multiply(X0,X0),multiply(multiply(X0,multiply(a,iPr_def_11)),iPr_def_11)),
inference(superposition,[status(thm)],[c_11884,c_8772]) ).
tcf(c_11944,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(X0,multiply(multiply(X0,multiply(multiply(X0,X0),X1)),multiply(multiply(multiply(a,multiply(multiply(iPr_def_10,a),multiply(X1,X2))),multiply(X2,multiply(X2,X2))),multiply(multiply(multiply(a,multiply(multiply(iPr_def_10,a),multiply(X1,X2))),multiply(X2,multiply(X2,X2))),multiply(multiply(a,multiply(multiply(iPr_def_10,a),multiply(X1,X2))),multiply(X2,multiply(X2,X2))))))) = a,
inference(superposition,[status(thm)],[c_11884,c_6296]) ).
tcf(c_11945,plain,
! [X0: $i,X1: $i] : multiply(multiply(X0,multiply(multiply(X0,X0),multiply(X1,a))),multiply(a,multiply(iPr_def_10,a))) = multiply(multiply(X0,X0),multiply(multiply(X0,multiply(X1,iPr_def_11)),iPr_def_11)),
inference(superposition,[status(thm)],[c_11884,c_6538]) ).
tcf(c_11964,plain,
! [X0: $i] : multiply(multiply(X0,X0),multiply(multiply(X0,multiply(a,iPr_def_11)),iPr_def_11)) = multiply(multiply(X0,X0),multiply(multiply(X0,multiply(iPr_def_10,iPr_def_11)),iPr_def_11)),
inference(demodulation,[status(thm)],[c_11941,c_11945]) ).
tcf(c_11965,plain,
! [X0: $i] : multiply(multiply(X0,X0),multiply(multiply(X0,a),iPr_def_11)) = multiply(multiply(X0,X0),multiply(multiply(X0,iPr_def_10),iPr_def_11)),
inference(demodulation,[status(thm)],[c_11964,c_8308,c_8341]) ).
tcf(c_11975,plain,
! [X0: $i,X1: $i] : multiply(multiply(X0,multiply(multiply(X0,X0),X1)),multiply(multiply(multiply(iPr_def_10,a),multiply(multiply(a,multiply(X1,iPr_def_11)),iPr_def_11)),multiply(multiply(multiply(iPr_def_10,a),multiply(multiply(a,multiply(X1,iPr_def_11)),iPr_def_11)),multiply(multiply(iPr_def_10,a),multiply(multiply(a,multiply(X1,iPr_def_11)),iPr_def_11))))) = multiply(multiply(X0,X0),multiply(multiply(X0,a),iPr_def_11)),
inference(demodulation,[status(thm)],[c_11942,c_8308]) ).
tcf(c_11979,plain,
! [X0: $i] : multiply(X0,multiply(multiply(X0,X0),multiply(multiply(X0,iPr_def_10),iPr_def_11))) = a,
inference(demodulation,[status(thm)],[c_11944,c_11928,c_11965,c_11975]) ).
tcf(c_11980,plain,
a = iPr_def_10,
inference(demodulation,[status(thm)],[c_11979,c_6288,c_6571,c_8341,c_8348]) ).
tcf(c_11994,plain,
iPr_def_10 != iPr_def_10,
inference(demodulation,[status(thm)],[c_67,c_11980]) ).
tcf(c_11995,plain,
$false,
inference(equality_resolution_simp,[status(thm)],[c_11994]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP120-1 : TPTP v9.3.1. Released v1.2.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.07/0.35 % Computer : n005.cluster.edu
% 0.07/0.35 % Model : x86_64 x86_64
% 0.07/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.35 % Memory : 8046.5625MB
% 0.07/0.35 % OS : Linux 6.8.0-71-generic
% 0.07/0.35 % CPULimit : 300
% 0.07/0.35 % WCLimit : 300
% 0.07/0.35 % DateTime : Wed Sep 23 13:35:02 UTC 2026
% 0.07/0.35 % CPUTime :
% 0.07/0.35 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.13/0.38 Running UEQ theorem proving
% 0.13/0.38 Running: /export/starexec/sandbox2/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s ueq_schedule -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.13/0.40
% 0.13/0.40 % ======== iProver multi-core TPTP/SMT =========
% 0.13/0.40
% 0.13/0.40 % Detected problem language: tptp
% 0.13/0.41 % Proving...
% 15.11/4.68 WARNING - Clausifier option not provided in the heuristic config "heur/vip2_118404", setting default options.
% 15.11/4.68 % SZS status Started for theBenchmark.p
% 15.11/4.68 % SZS status Unsatisfiable for theBenchmark.p
% 15.11/4.68
% 15.11/4.68 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 15.11/4.68
% 15.11/4.68 % ------ iProver source info
% 15.11/4.68
% 15.11/4.68 % git: date: 2026-07-19 20:42:38 +0200
% 15.11/4.68 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 15.11/4.68 % git: non_committed_changes: false
% 15.11/4.68
% 15.11/4.68 % ------ Parsing...% successful
% 15.11/4.68
% 15.11/4.68
% 15.11/4.68 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 15.11/4.68
% 15.11/4.68 % ------ Preprocessing... sf_s rm: 0 0s sf_e pe_s pe_e %
% 15.11/4.68
% 15.11/4.68 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 15.11/4.68
% 15.11/4.68 % ------ Preprocessing... sf_s rm: 0 0s sf_e
% 15.11/4.68 % ------ Proving...
% 15.11/4.68 % ------ Problem Properties
% 15.11/4.68
% 15.11/4.68 %
% 15.11/4.68 % clauses 5
% 15.11/4.68 % conjectures 1
% 15.11/4.68 % EPR 2
% 15.11/4.68 % Horn 5
% 15.11/4.68 % unary 5
% 15.11/4.68 % binary 0
% 15.11/4.68 % lits 5
% 15.11/4.68 % lits eq 5
% 15.11/4.68 % fd_pure 0
% 15.11/4.68 % fd_pseudo 0
% 15.11/4.68 % fd_cond 0
% 15.11/4.68 % fd_pseudo_cond 0
% 15.11/4.68 % AC symbols 0
% 15.11/4.68
% 15.11/4.68 % ------ Input Options Time Limit: Unbounded
% 15.11/4.68
% 15.11/4.68
% 15.11/4.68 % ------
% 15.11/4.68 % Current options:
% 15.11/4.68 % ------
% 15.11/4.68
% 15.11/4.68
% 15.11/4.68 %
% 15.11/4.68
% 15.11/4.68 % ------ Proving...
% 15.11/4.68 %
% 15.11/4.68
% 15.11/4.68 % SZS status Unsatisfiable for theBenchmark.p
% 15.11/4.68
% 15.11/4.68 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 15.11/4.68
% 15.11/4.68
%------------------------------------------------------------------------------