%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : GRP122-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 : n013.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 55.27s 9.28s
% Output : CNFRefutation 55.27s
% Verified :
% SZS Type : Refutation
% Derivation depth : 88
% Number of leaves : 3
% Syntax : Number of formulae : 300 ( 300 unt; 0 def)
% Number of atoms : 300 ( 299 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 2 ( 2 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 avg)
% Maximal term depth : 15 ( 2 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 5 ( 5 usr; 4 con; 0-2 aty)
% Number of variables : 521 ( 0 sgn 521 !; 0 ?; 518 :)
% 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(multiply(a,b),c) != multiply(a,multiply(b,c)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_order3) ).
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(multiply(a,b),c) != multiply(a,multiply(b,c)),
inference(cnf_transformation,[],[f4]) ).
tcf(c_91,plain,
! [X0: $i,X1: $i] : multiply(identity,multiply(multiply(identity,multiply(identity,multiply(X0,X1))),multiply(X1,multiply(X1,X1)))) = X0,
inference(superposition,[status(thm)],[c_53,c_52]) ).
tcf(c_93,plain,
! [X0: $i] : multiply(X0,multiply(multiply(X0,multiply(multiply(X0,X0),identity)),identity)) = identity,
inference(superposition,[status(thm)],[c_53,c_52]) ).
tcf(c_94,plain,
! [X0: $i,X1: $i] : multiply(X0,multiply(multiply(X0,multiply(multiply(X0,X0),multiply(X1,identity))),identity)) = X1,
inference(superposition,[status(thm)],[c_53,c_52]) ).
tcf(c_95,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_52,c_52]) ).
tcf(c_96,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_52,c_52]) ).
tcf(c_102,plain,
! [X0: $i,X1: $i] : multiply(X0,multiply(multiply(X0,multiply(multiply(X0,X0),identity)),multiply(multiply(multiply(X1,multiply(multiply(X1,X1),identity)),identity),multiply(multiply(multiply(X1,multiply(multiply(X1,X1),identity)),identity),multiply(multiply(X1,multiply(multiply(X1,X1),identity)),identity))))) = X1,
inference(superposition,[status(thm)],[c_93,c_52]) ).
tcf(c_103,plain,
! [X0: $i] : multiply(multiply(X0,X0),multiply(multiply(multiply(X0,X0),multiply(X0,X0)),identity)) = multiply(X0,multiply(multiply(X0,identity),multiply(identity,multiply(identity,identity)))),
inference(superposition,[status(thm)],[c_93,c_52]) ).
tcf(c_104,plain,
! [X0: $i] : multiply(multiply(X0,X0),multiply(multiply(multiply(X0,X0),multiply(X0,X0)),identity)) = multiply(X0,multiply(multiply(X0,identity),identity)),
inference(light_normalisation,[status(thm)],[c_103,c_53]) ).
tcf(c_109,plain,
! [X0: $i] : multiply(identity,multiply(multiply(identity,multiply(identity,multiply(X0,identity))),identity)) = X0,
inference(superposition,[status(thm)],[c_53,c_94]) ).
tcf(c_113,plain,
! [X0: $i,X1: $i] : multiply(multiply(X0,X0),multiply(multiply(multiply(X0,X0),multiply(X0,X0)),multiply(X1,identity))) = multiply(X0,multiply(multiply(X0,X1),identity)),
inference(superposition,[status(thm)],[c_94,c_94]) ).
tcf(c_128,plain,
! [X0: $i] : multiply(identity,multiply(multiply(identity,X0),identity)) = multiply(identity,multiply(identity,multiply(X0,identity))),
inference(superposition,[status(thm)],[c_109,c_109]) ).
tcf(c_130,plain,
! [X0: $i] : multiply(identity,multiply(identity,multiply(multiply(identity,multiply(X0,identity)),identity))) = X0,
inference(demodulation,[status(thm)],[c_109,c_128]) ).
tcf(c_134,plain,
! [X0: $i] : multiply(identity,multiply(identity,multiply(identity,multiply(multiply(X0,identity),identity)))) = X0,
inference(demodulation,[status(thm)],[c_130,c_128]) ).
tcf(c_141,plain,
! [X0: $i] : multiply(identity,multiply(identity,multiply(multiply(multiply(identity,multiply(multiply(identity,identity),multiply(X0,identity))),identity),identity))) = multiply(identity,multiply(X0,identity)),
inference(superposition,[status(thm)],[c_94,c_128]) ).
tcf(c_155,plain,
! [X0: $i] : multiply(identity,multiply(identity,multiply(multiply(multiply(identity,multiply(identity,multiply(X0,identity))),identity),identity))) = multiply(identity,multiply(X0,identity)),
inference(light_normalisation,[status(thm)],[c_141,c_53]) ).
tcf(c_162,plain,
! [X0: $i] : multiply(identity,multiply(X0,multiply(multiply(multiply(X0,identity),identity),multiply(multiply(multiply(X0,identity),identity),multiply(multiply(X0,identity),identity))))) = identity,
inference(superposition,[status(thm)],[c_134,c_91]) ).
tcf(c_228,plain,
! [X0: $i] : multiply(identity,multiply(identity,multiply(multiply(multiply(identity,X0),identity),identity))) = X0,
inference(superposition,[status(thm)],[c_94,c_155]) ).
tcf(c_238,plain,
! [X0: $i,X1: $i] : multiply(multiply(identity,multiply(identity,multiply(X0,X1))),multiply(X1,multiply(X1,X1))) = multiply(identity,multiply(identity,multiply(multiply(X0,identity),identity))),
inference(superposition,[status(thm)],[c_91,c_228]) ).
tcf(c_246,plain,
! [X0: $i] : multiply(identity,multiply(X0,multiply(identity,multiply(identity,identity)))) = multiply(multiply(identity,X0),identity),
inference(superposition,[status(thm)],[c_228,c_91]) ).
tcf(c_249,plain,
! [X0: $i] : multiply(multiply(identity,X0),identity) = multiply(identity,multiply(X0,identity)),
inference(light_normalisation,[status(thm)],[c_246,c_53]) ).
tcf(c_271,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(multiply(X0,X0),multiply(multiply(X0,multiply(multiply(X0,identity),identity)),multiply(multiply(multiply(X1,multiply(multiply(X1,X1),multiply(identity,X2))),multiply(X2,multiply(X2,X2))),multiply(multiply(multiply(X1,multiply(multiply(X1,X1),multiply(identity,X2))),multiply(X2,multiply(X2,X2))),multiply(multiply(X1,multiply(multiply(X1,X1),multiply(identity,X2))),multiply(X2,multiply(X2,X2))))))) = X1,
inference(superposition,[status(thm)],[c_104,c_95]) ).
tcf(c_313,plain,
! [X0: $i,X1: $i] : multiply(X0,multiply(multiply(X0,multiply(multiply(X0,X0),multiply(multiply(X1,X1),multiply(multiply(multiply(X1,X1),multiply(X1,X1)),identity)))),multiply(multiply(multiply(X1,identity),multiply(identity,multiply(identity,identity))),multiply(multiply(multiply(X1,identity),multiply(identity,multiply(identity,identity))),multiply(multiply(X1,identity),multiply(identity,multiply(identity,identity))))))) = X1,
inference(superposition,[status(thm)],[c_93,c_95]) ).
tcf(c_321,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(X0,multiply(multiply(X0,multiply(multiply(X0,X0),X1)),multiply(multiply(multiply(X2,multiply(multiply(X2,X2),identity)),multiply(multiply(multiply(X1,multiply(multiply(X1,X1),identity)),identity),multiply(multiply(multiply(X1,multiply(multiply(X1,X1),identity)),identity),multiply(multiply(X1,multiply(multiply(X1,X1),identity)),identity)))),multiply(multiply(multiply(X2,multiply(multiply(X2,X2),identity)),multiply(multiply(multiply(X1,multiply(multiply(X1,X1),identity)),identity),multiply(multiply(multiply(X1,multiply(multiply(X1,X1),identity)),identity),multiply(multiply(X1,multiply(multiply(X1,X1),identity)),identity)))),multiply(multiply(X2,multiply(multiply(X2,X2),identity)),multiply(multiply(multiply(X1,multiply(multiply(X1,X1),identity)),identity),multiply(multiply(multiply(X1,multiply(multiply(X1,X1),identity)),identity),multiply(multiply(X1,multiply(multiply(X1,X1),identity)),identity)))))))) = X2,
inference(superposition,[status(thm)],[c_93,c_95]) ).
tcf(c_323,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(X0,multiply(multiply(X0,multiply(multiply(X0,X0),multiply(X1,X1))),multiply(multiply(multiply(X2,multiply(multiply(X2,X2),multiply(X1,multiply(multiply(X1,identity),identity)))),multiply(multiply(multiply(multiply(X1,X1),multiply(X1,X1)),identity),multiply(multiply(multiply(multiply(X1,X1),multiply(X1,X1)),identity),multiply(multiply(multiply(X1,X1),multiply(X1,X1)),identity)))),multiply(multiply(multiply(X2,multiply(multiply(X2,X2),multiply(X1,multiply(multiply(X1,identity),identity)))),multiply(multiply(multiply(multiply(X1,X1),multiply(X1,X1)),identity),multiply(multiply(multiply(multiply(X1,X1),multiply(X1,X1)),identity),multiply(multiply(multiply(X1,X1),multiply(X1,X1)),identity)))),multiply(multiply(X2,multiply(multiply(X2,X2),multiply(X1,multiply(multiply(X1,identity),identity)))),multiply(multiply(multiply(multiply(X1,X1),multiply(X1,X1)),identity),multiply(multiply(multiply(multiply(X1,X1),multiply(X1,X1)),identity),multiply(multiply(multiply(X1,X1),multiply(X1,X1)),identity)))))))) = X2,
inference(superposition,[status(thm)],[c_104,c_95]) ).
tcf(c_324,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(X0,multiply(multiply(X0,multiply(multiply(X0,X0),identity)),multiply(multiply(multiply(X1,multiply(multiply(X1,X1),X2)),multiply(multiply(identity,multiply(identity,multiply(multiply(X2,identity),identity))),multiply(multiply(identity,multiply(identity,multiply(multiply(X2,identity),identity))),multiply(identity,multiply(identity,multiply(multiply(X2,identity),identity)))))),multiply(multiply(multiply(X1,multiply(multiply(X1,X1),X2)),multiply(multiply(identity,multiply(identity,multiply(multiply(X2,identity),identity))),multiply(multiply(identity,multiply(identity,multiply(multiply(X2,identity),identity))),multiply(identity,multiply(identity,multiply(multiply(X2,identity),identity)))))),multiply(multiply(X1,multiply(multiply(X1,X1),X2)),multiply(multiply(identity,multiply(identity,multiply(multiply(X2,identity),identity))),multiply(multiply(identity,multiply(identity,multiply(multiply(X2,identity),identity))),multiply(identity,multiply(identity,multiply(multiply(X2,identity),identity)))))))))) = X1,
inference(superposition,[status(thm)],[c_134,c_95]) ).
tcf(c_329,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] : multiply(X0,multiply(multiply(X0,multiply(multiply(X0,X0),X1)),multiply(multiply(multiply(X2,multiply(multiply(X2,X2),X3)),multiply(multiply(multiply(X1,multiply(multiply(X1,X1),X4)),multiply(multiply(multiply(X3,multiply(multiply(X3,X3),multiply(X4,X5))),multiply(X5,multiply(X5,X5))),multiply(multiply(multiply(X3,multiply(multiply(X3,X3),multiply(X4,X5))),multiply(X5,multiply(X5,X5))),multiply(multiply(X3,multiply(multiply(X3,X3),multiply(X4,X5))),multiply(X5,multiply(X5,X5)))))),multiply(multiply(multiply(X1,multiply(multiply(X1,X1),X4)),multiply(multiply(multiply(X3,multiply(multiply(X3,X3),multiply(X4,X5))),multiply(X5,multiply(X5,X5))),multiply(multiply(multiply(X3,multiply(multiply(X3,X3),multiply(X4,X5))),multiply(X5,multiply(X5,X5))),multiply(multiply(X3,multiply(multiply(X3,X3),multiply(X4,X5))),multiply(X5,multiply(X5,X5)))))),multiply(multiply(X1,multiply(multiply(X1,X1),X4)),multiply(multiply(multiply(X3,multiply(multiply(X3,X3),multiply(X4,X5))),multiply(X5,multiply(X5,X5))),multiply(multiply(multiply(X3,multiply(multiply(X3,X3),multiply(X4,X5))),multiply(X5,multiply(X5,X5))),multiply(multiply(X3,multiply(multiply(X3,X3),multiply(X4,X5))),multiply(X5,multiply(X5,X5))))))))),multiply(multiply(multiply(X2,multiply(multiply(X2,X2),X3)),multiply(multiply(multiply(X1,multiply(multiply(X1,X1),X4)),multiply(multiply(multiply(X3,multiply(multiply(X3,X3),multiply(X4,X5))),multiply(X5,multiply(X5,X5))),multiply(multiply(multiply(X3,multiply(multiply(X3,X3),multiply(X4,X5))),multiply(X5,multiply(X5,X5))),multiply(multiply(X3,multiply(multiply(X3,X3),multiply(X4,X5))),multiply(X5,multiply(X5,X5)))))),multiply(multiply(multiply(X1,multiply(multiply(X1,X1),X4)),multiply(multiply(multiply(X3,multiply(multiply(X3,X3),multiply(X4,X5))),multiply(X5,multiply(X5,X5))),multiply(multiply(multiply(X3,multiply(multiply(X3,X3),multiply(X4,X5))),multiply(X5,multiply(X5,X5))),multiply(multiply(X3,multiply(multiply(X3,X3),multiply(X4,X5))),multiply(X5,multiply(X5,X5)))))),multiply(multiply(X1,multiply(multiply(X1,X1),X4)),multiply(multiply(multiply(X3,multiply(multiply(X3,X3),multiply(X4,X5))),multiply(X5,multiply(X5,X5))),multiply(multiply(multiply(X3,multiply(multiply(X3,X3),multiply(X4,X5))),multiply(X5,multiply(X5,X5))),multiply(multiply(X3,multiply(multiply(X3,X3),multiply(X4,X5))),multiply(X5,multiply(X5,X5))))))))),multiply(multiply(X2,multiply(multiply(X2,X2),X3)),multiply(multiply(multiply(X1,multiply(multiply(X1,X1),X4)),multiply(multiply(multiply(X3,multiply(multiply(X3,X3),multiply(X4,X5))),multiply(X5,multiply(X5,X5))),multiply(multiply(multiply(X3,multiply(multiply(X3,X3),multiply(X4,X5))),multiply(X5,multiply(X5,X5))),multiply(multiply(X3,multiply(multiply(X3,X3),multiply(X4,X5))),multiply(X5,multiply(X5,X5)))))),multiply(multiply(multiply(X1,multiply(multiply(X1,X1),X4)),multiply(multiply(multiply(X3,multiply(multiply(X3,X3),multiply(X4,X5))),multiply(X5,multiply(X5,X5))),multiply(multiply(multiply(X3,multiply(multiply(X3,X3),multiply(X4,X5))),multiply(X5,multiply(X5,X5))),multiply(multiply(X3,multiply(multiply(X3,X3),multiply(X4,X5))),multiply(X5,multiply(X5,X5)))))),multiply(multiply(X1,multiply(multiply(X1,X1),X4)),multiply(multiply(multiply(X3,multiply(multiply(X3,X3),multiply(X4,X5))),multiply(X5,multiply(X5,X5))),multiply(multiply(multiply(X3,multiply(multiply(X3,X3),multiply(X4,X5))),multiply(X5,multiply(X5,X5))),multiply(multiply(X3,multiply(multiply(X3,X3),multiply(X4,X5))),multiply(X5,multiply(X5,X5))))))))))))) = X2,
inference(superposition,[status(thm)],[c_95,c_95]) ).
tcf(c_333,plain,
! [X0: $i,X1: $i] : multiply(X0,multiply(multiply(X0,multiply(multiply(X0,X0),multiply(multiply(X1,X1),multiply(multiply(multiply(X1,X1),multiply(X1,X1)),identity)))),multiply(multiply(multiply(X1,identity),identity),multiply(multiply(multiply(X1,identity),identity),multiply(multiply(X1,identity),identity))))) = X1,
inference(light_normalisation,[status(thm)],[c_313,c_53]) ).
tcf(c_388,plain,
! [X0: $i,X1: $i] : multiply(X0,multiply(multiply(X0,multiply(multiply(X0,X0),multiply(identity,multiply(X1,identity)))),identity)) = multiply(identity,X1),
inference(superposition,[status(thm)],[c_249,c_94]) ).
tcf(c_437,plain,
! [X0: $i,X1: $i] : multiply(X0,multiply(multiply(X0,multiply(multiply(X0,X0),X1)),identity)) = multiply(identity,multiply(identity,multiply(multiply(identity,identity),multiply(X1,identity)))),
inference(superposition,[status(thm)],[c_94,c_388]) ).
tcf(c_452,plain,
! [X0: $i,X1: $i] : multiply(X0,multiply(multiply(X0,multiply(multiply(X0,X0),X1)),identity)) = multiply(identity,multiply(identity,multiply(identity,multiply(X1,identity)))),
inference(light_normalisation,[status(thm)],[c_437,c_53]) ).
tcf(c_500,plain,
! [X0: $i,X1: $i] : multiply(X0,multiply(multiply(X0,multiply(identity,multiply(identity,multiply(identity,multiply(X1,identity))))),multiply(identity,multiply(identity,identity)))) = multiply(multiply(X0,X0),multiply(multiply(multiply(X0,X0),multiply(X0,X0)),X1)),
inference(superposition,[status(thm)],[c_452,c_52]) ).
tcf(c_511,plain,
! [X0: $i,X1: $i] : multiply(X0,multiply(multiply(X0,multiply(identity,multiply(identity,multiply(identity,multiply(X1,identity))))),identity)) = multiply(multiply(X0,X0),multiply(multiply(multiply(X0,X0),multiply(X0,X0)),X1)),
inference(light_normalisation,[status(thm)],[c_500,c_53]) ).
tcf(c_535,plain,
! [X0: $i,X1: $i] : multiply(multiply(X0,X0),multiply(multiply(X0,multiply(multiply(X0,X1),identity)),multiply(identity,multiply(identity,identity)))) = X1,
inference(superposition,[status(thm)],[c_113,c_52]) ).
tcf(c_543,plain,
! [X0: $i,X1: $i] : multiply(multiply(X0,X0),multiply(multiply(X0,multiply(multiply(X0,X1),identity)),identity)) = X1,
inference(light_normalisation,[status(thm)],[c_535,c_53]) ).
tcf(c_564,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,identity)),identity)),
inference(superposition,[status(thm)],[c_52,c_543]) ).
tcf(c_565,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,identity)),identity)),
inference(superposition,[status(thm)],[c_95,c_543]) ).
tcf(c_576,plain,
! [X0: $i,X1: $i] : multiply(multiply(multiply(X0,X0),multiply(X0,X0)),multiply(multiply(multiply(X0,X0),multiply(X1,identity)),identity)) = multiply(multiply(X0,multiply(multiply(X0,X1),identity)),identity),
inference(superposition,[status(thm)],[c_543,c_543]) ).
tcf(c_588,plain,
! [X0: $i,X1: $i] : multiply(X0,multiply(multiply(X0,X0),multiply(multiply(X0,multiply(X1,identity)),identity))) = X1,
inference(demodulation,[status(thm)],[c_52,c_564]) ).
tcf(c_650,plain,
! [X0: $i] : multiply(X0,multiply(multiply(X0,X0),multiply(multiply(X0,identity),identity))) = identity,
inference(superposition,[status(thm)],[c_53,c_588]) ).
tcf(c_651,plain,
! [X0: $i,X1: $i] : multiply(X0,multiply(multiply(X0,X0),multiply(multiply(X0,multiply(identity,multiply(X1,identity))),identity))) = multiply(identity,X1),
inference(superposition,[status(thm)],[c_249,c_588]) ).
tcf(c_820,plain,
! [X0: $i] : multiply(multiply(identity,X0),multiply(multiply(multiply(identity,X0),multiply(identity,X0)),multiply(multiply(identity,multiply(X0,identity)),identity))) = identity,
inference(superposition,[status(thm)],[c_249,c_650]) ).
tcf(c_844,plain,
! [X0: $i,X1: $i] : multiply(X0,multiply(multiply(X0,X0),multiply(multiply(X0,multiply(identity,multiply(identity,multiply(identity,multiply(X1,identity))))),identity))) = multiply(identity,multiply(identity,multiply(multiply(identity,identity),X1))),
inference(superposition,[status(thm)],[c_452,c_651]) ).
tcf(c_858,plain,
! [X0: $i,X1: $i] : multiply(X0,multiply(multiply(X0,X0),multiply(multiply(X0,multiply(identity,multiply(identity,multiply(identity,multiply(X1,identity))))),identity))) = multiply(identity,multiply(identity,multiply(identity,X1))),
inference(light_normalisation,[status(thm)],[c_844,c_53]) ).
tcf(c_908,plain,
! [X0: $i] : multiply(multiply(identity,X0),multiply(multiply(multiply(identity,X0),multiply(identity,X0)),multiply(identity,multiply(multiply(X0,identity),identity)))) = identity,
inference(demodulation,[status(thm)],[c_820,c_249]) ).
tcf(c_934,plain,
! [X0: $i] : multiply(multiply(multiply(identity,X0),multiply(identity,X0)),multiply(multiply(multiply(identity,X0),multiply(identity,identity)),identity)) = multiply(multiply(multiply(identity,X0),multiply(identity,X0)),multiply(identity,multiply(multiply(X0,identity),identity))),
inference(superposition,[status(thm)],[c_908,c_543]) ).
tcf(c_942,plain,
! [X0: $i] : multiply(multiply(multiply(identity,X0),multiply(identity,X0)),multiply(multiply(identity,multiply(X0,identity)),identity)) = multiply(multiply(multiply(identity,X0),multiply(identity,X0)),multiply(identity,multiply(multiply(X0,identity),identity))),
inference(light_normalisation,[status(thm)],[c_934,c_53,c_249]) ).
tcf(c_967,plain,
! [X0: $i] : multiply(X0,multiply(multiply(multiply(X0,identity),identity),multiply(multiply(multiply(X0,identity),identity),multiply(multiply(X0,identity),identity)))) = multiply(multiply(identity,identity),multiply(multiply(identity,multiply(identity,identity)),identity)),
inference(superposition,[status(thm)],[c_162,c_543]) ).
tcf(c_973,plain,
! [X0: $i] : multiply(X0,multiply(multiply(multiply(X0,identity),identity),multiply(multiply(multiply(X0,identity),identity),multiply(multiply(X0,identity),identity)))) = identity,
inference(light_normalisation,[status(thm)],[c_967,c_53]) ).
tcf(c_993,plain,
! [X0: $i] : multiply(multiply(multiply(X0,identity),identity),multiply(multiply(multiply(X0,identity),identity),multiply(multiply(X0,identity),identity))) = multiply(multiply(X0,X0),multiply(multiply(X0,multiply(identity,identity)),identity)),
inference(superposition,[status(thm)],[c_973,c_543]) ).
tcf(c_999,plain,
! [X0: $i] : multiply(multiply(multiply(X0,identity),identity),multiply(multiply(multiply(X0,identity),identity),multiply(multiply(X0,identity),identity))) = multiply(multiply(X0,X0),multiply(multiply(X0,identity),identity)),
inference(light_normalisation,[status(thm)],[c_993,c_53]) ).
tcf(c_1140,plain,
! [X0: $i,X1: $i] : multiply(multiply(identity,identity),multiply(multiply(multiply(identity,identity),multiply(identity,identity)),multiply(multiply(identity,multiply(X0,multiply(X1,multiply(X1,X1)))),X1))) = multiply(identity,multiply(identity,multiply(identity,multiply(multiply(X0,identity),identity)))),
inference(superposition,[status(thm)],[c_238,c_96]) ).
tcf(c_1147,plain,
! [X0: $i,X1: $i] : multiply(identity,multiply(identity,multiply(multiply(identity,multiply(X0,multiply(X1,multiply(X1,X1)))),X1))) = X0,
inference(light_normalisation,[status(thm)],[c_1140,c_53,c_134]) ).
tcf(c_1203,plain,
! [X0: $i,X1: $i] : multiply(identity,multiply(multiply(identity,multiply(X0,multiply(X1,multiply(X1,X1)))),X1)) = multiply(multiply(identity,identity),multiply(multiply(identity,multiply(X0,identity)),identity)),
inference(superposition,[status(thm)],[c_1147,c_543]) ).
tcf(c_1212,plain,
! [X0: $i,X1: $i] : multiply(identity,multiply(multiply(identity,multiply(X0,multiply(X1,multiply(X1,X1)))),X1)) = multiply(identity,multiply(multiply(identity,multiply(X0,identity)),identity)),
inference(light_normalisation,[status(thm)],[c_1203,c_53]) ).
tcf(c_1337,plain,
! [X0: $i,X1: $i] : multiply(multiply(X0,multiply(multiply(X0,X0),identity)),multiply(multiply(multiply(X1,multiply(multiply(X1,X1),identity)),identity),multiply(multiply(multiply(X1,multiply(multiply(X1,X1),identity)),identity),multiply(multiply(X1,multiply(multiply(X1,X1),identity)),identity)))) = multiply(multiply(X0,X0),multiply(multiply(X0,multiply(X1,identity)),identity)),
inference(superposition,[status(thm)],[c_102,c_543]) ).
tcf(c_1424,plain,
! [X0: $i,X1: $i] : multiply(identity,multiply(multiply(identity,multiply(X0,multiply(X1,multiply(X1,X1)))),X1)) = multiply(identity,multiply(identity,multiply(multiply(X0,identity),identity))),
inference(demodulation,[status(thm)],[c_1212,c_249]) ).
tcf(c_1435,plain,
! [X0: $i,X1: $i] : multiply(multiply(identity,identity),multiply(multiply(identity,multiply(multiply(identity,multiply(identity,multiply(multiply(X0,identity),identity))),identity)),identity)) = multiply(multiply(identity,multiply(X0,multiply(X1,multiply(X1,X1)))),X1),
inference(superposition,[status(thm)],[c_1424,c_543]) ).
tcf(c_1452,plain,
! [X0: $i,X1: $i] : multiply(identity,multiply(multiply(identity,multiply(multiply(identity,multiply(identity,multiply(multiply(X0,identity),identity))),identity)),identity)) = multiply(multiply(identity,multiply(X0,multiply(X1,multiply(X1,X1)))),X1),
inference(light_normalisation,[status(thm)],[c_1435,c_53]) ).
tcf(c_1717,plain,
! [X0: $i] : multiply(identity,multiply(multiply(multiply(X0,identity),identity),multiply(multiply(multiply(X0,identity),identity),multiply(multiply(X0,identity),identity)))) = multiply(multiply(multiply(identity,X0),multiply(identity,X0)),multiply(multiply(multiply(identity,X0),multiply(identity,identity)),identity)),
inference(superposition,[status(thm)],[c_908,c_564]) ).
tcf(c_1735,plain,
! [X0: $i] : multiply(multiply(X0,multiply(multiply(X0,X0),identity)),identity) = multiply(multiply(X0,X0),multiply(multiply(X0,identity),identity)),
inference(superposition,[status(thm)],[c_53,c_564]) ).
tcf(c_1739,plain,
! [X0: $i,X1: $i] : multiply(multiply(X0,multiply(multiply(X0,X0),multiply(X1,multiply(multiply(X1,identity),identity)))),multiply(multiply(multiply(multiply(X1,X1),multiply(X1,X1)),identity),multiply(multiply(multiply(multiply(X1,X1),multiply(X1,X1)),identity),multiply(multiply(multiply(X1,X1),multiply(X1,X1)),identity)))) = multiply(multiply(X0,X0),multiply(multiply(X0,multiply(multiply(X1,X1),identity)),identity)),
inference(superposition,[status(thm)],[c_104,c_564]) ).
tcf(c_1741,plain,
! [X0: $i,X1: $i] : multiply(multiply(X0,multiply(multiply(X0,X0),multiply(identity,multiply(X1,identity)))),multiply(identity,multiply(identity,identity))) = multiply(multiply(X0,X0),multiply(multiply(X0,multiply(identity,multiply(X1,identity))),identity)),
inference(superposition,[status(thm)],[c_249,c_564]) ).
tcf(c_1742,plain,
! [X0: $i,X1: $i] : multiply(multiply(X0,multiply(multiply(X0,X0),X1)),multiply(multiply(identity,multiply(identity,multiply(multiply(X1,identity),identity))),multiply(multiply(identity,multiply(identity,multiply(multiply(X1,identity),identity))),multiply(identity,multiply(identity,multiply(multiply(X1,identity),identity)))))) = multiply(multiply(X0,X0),multiply(multiply(X0,multiply(identity,identity)),identity)),
inference(superposition,[status(thm)],[c_134,c_564]) ).
tcf(c_1761,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(multiply(X0,X0),multiply(multiply(multiply(X0,X0),multiply(X0,X0)),multiply(multiply(multiply(X0,X0),multiply(X1,multiply(X2,multiply(X2,X2)))),X2))) = multiply(X0,multiply(multiply(X0,X0),multiply(multiply(X0,multiply(X1,identity)),identity))),
inference(superposition,[status(thm)],[c_564,c_96]) ).
tcf(c_1769,plain,
! [X0: $i,X1: $i] : multiply(multiply(X0,multiply(multiply(X0,X0),multiply(identity,multiply(X1,identity)))),identity) = multiply(multiply(X0,X0),multiply(multiply(X0,multiply(identity,multiply(X1,identity))),identity)),
inference(light_normalisation,[status(thm)],[c_1741,c_53]) ).
tcf(c_1774,plain,
! [X0: $i] : multiply(multiply(multiply(identity,X0),multiply(identity,X0)),multiply(identity,multiply(multiply(X0,identity),identity))) = multiply(identity,multiply(multiply(X0,X0),multiply(multiply(X0,identity),identity))),
inference(light_normalisation,[status(thm)],[c_1717,c_53,c_249,c_942,c_999]) ).
tcf(c_1775,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(multiply(X0,X0),multiply(multiply(multiply(X0,X0),multiply(X0,X0)),multiply(multiply(multiply(X0,X0),multiply(X1,multiply(X2,multiply(X2,X2)))),X2))) = X1,
inference(light_normalisation,[status(thm)],[c_1761,c_588]) ).
tcf(c_1785,plain,
! [X0: $i,X1: $i] : multiply(multiply(X0,multiply(multiply(X0,X0),X1)),multiply(multiply(identity,multiply(identity,multiply(multiply(X1,identity),identity))),multiply(multiply(identity,multiply(identity,multiply(multiply(X1,identity),identity))),multiply(identity,multiply(identity,multiply(multiply(X1,identity),identity)))))) = multiply(multiply(X0,X0),multiply(multiply(X0,identity),identity)),
inference(light_normalisation,[status(thm)],[c_1742,c_53]) ).
tcf(c_1997,plain,
! [X0: $i,X1: $i] : multiply(X0,multiply(multiply(X0,X0),multiply(multiply(X0,multiply(identity,multiply(multiply(X1,X1),multiply(multiply(X1,identity),identity)))),identity))) = multiply(identity,multiply(X1,multiply(multiply(X1,X1),identity))),
inference(superposition,[status(thm)],[c_1735,c_651]) ).
tcf(c_2009,plain,
! [X0: $i] : multiply(multiply(X0,X0),multiply(multiply(X0,X0),multiply(multiply(X0,identity),identity))) = X0,
inference(superposition,[status(thm)],[c_1735,c_543]) ).
tcf(c_2040,plain,
! [X0: $i] : multiply(multiply(multiply(identity,X0),multiply(identity,X0)),multiply(multiply(multiply(identity,X0),multiply(identity,X0)),multiply(multiply(identity,multiply(X0,identity)),identity))) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_249,c_2009]) ).
tcf(c_2049,plain,
! [X0: $i] : multiply(multiply(multiply(identity,X0),multiply(identity,X0)),multiply(identity,multiply(multiply(X0,X0),multiply(multiply(X0,identity),identity)))) = multiply(identity,X0),
inference(light_normalisation,[status(thm)],[c_2040,c_942,c_1774]) ).
tcf(c_2228,plain,
! [X0: $i] : multiply(identity,multiply(identity,multiply(identity,multiply(multiply(identity,multiply(multiply(X0,X0),multiply(multiply(X0,identity),identity))),identity)))) = multiply(multiply(identity,X0),multiply(multiply(multiply(identity,X0),multiply(identity,X0)),identity)),
inference(superposition,[status(thm)],[c_2049,c_452]) ).
tcf(c_2609,plain,
! [X0: $i,X1: $i] : multiply(multiply(multiply(multiply(X0,X0),multiply(X0,X0)),multiply(multiply(X0,X0),multiply(X0,X0))),multiply(multiply(multiply(multiply(X0,X0),multiply(X0,X0)),multiply(multiply(multiply(X0,multiply(multiply(X0,X1),identity)),identity),identity)),identity)) = multiply(multiply(multiply(X0,X0),multiply(X1,identity)),identity),
inference(superposition,[status(thm)],[c_576,c_543]) ).
tcf(c_2648,plain,
! [X0: $i,X1: $i] : multiply(X0,multiply(multiply(X0,X0),multiply(multiply(X0,X1),identity))) = multiply(identity,multiply(identity,multiply(identity,multiply(X1,identity)))),
inference(superposition,[status(thm)],[c_134,c_858]) ).
tcf(c_2868,plain,
! [X0: $i,X1: $i] : multiply(multiply(identity,multiply(identity,multiply(X0,multiply(multiply(X1,identity),identity)))),multiply(multiply(X1,X1),multiply(multiply(X1,identity),identity))) = multiply(identity,multiply(identity,multiply(multiply(X0,identity),identity))),
inference(superposition,[status(thm)],[c_999,c_238]) ).
tcf(c_3195,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(multiply(multiply(X0,X0),multiply(X0,X0)),multiply(multiply(multiply(X0,X0),multiply(X1,multiply(X2,multiply(X2,X2)))),X2)) = multiply(multiply(multiply(X0,X0),multiply(X0,X0)),multiply(multiply(multiply(X0,X0),multiply(X1,identity)),identity)),
inference(superposition,[status(thm)],[c_1775,c_543]) ).
tcf(c_3205,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(multiply(multiply(X0,X0),multiply(X0,X0)),multiply(multiply(multiply(X0,X0),multiply(X1,multiply(X2,multiply(X2,X2)))),X2)) = multiply(multiply(X0,multiply(multiply(X0,X1),identity)),identity),
inference(light_normalisation,[status(thm)],[c_3195,c_576]) ).
tcf(c_3639,plain,
! [X0: $i,X1: $i] : multiply(multiply(X0,multiply(multiply(X0,X0),multiply(multiply(identity,identity),multiply(multiply(multiply(identity,identity),multiply(identity,identity)),X1)))),identity) = multiply(multiply(X0,X0),multiply(multiply(X0,multiply(multiply(identity,identity),multiply(multiply(multiply(identity,identity),multiply(identity,identity)),X1))),identity)),
inference(superposition,[status(thm)],[c_511,c_1769]) ).
tcf(c_3687,plain,
! [X0: $i,X1: $i] : multiply(multiply(X0,multiply(multiply(X0,X0),multiply(identity,multiply(identity,X1)))),identity) = multiply(multiply(X0,X0),multiply(multiply(X0,multiply(identity,multiply(identity,X1))),identity)),
inference(light_normalisation,[status(thm)],[c_3639,c_53]) ).
tcf(c_3823,plain,
! [X0: $i,X1: $i] : multiply(multiply(X0,multiply(multiply(X0,X0),X1)),identity) = multiply(multiply(X0,X0),multiply(multiply(X0,X1),identity)),
inference(superposition,[status(thm)],[c_134,c_3687]) ).
tcf(c_3925,plain,
! [X0: $i,X1: $i] : multiply(identity,multiply(identity,multiply(identity,multiply(multiply(multiply(X0,X0),multiply(multiply(X0,X1),identity)),identity)))) = multiply(X0,multiply(multiply(X0,X0),X1)),
inference(superposition,[status(thm)],[c_3823,c_134]) ).
tcf(c_4233,plain,
! [X0: $i,X1: $i] : multiply(multiply(identity,multiply(X0,multiply(X1,multiply(X1,X1)))),X1) = multiply(identity,multiply(multiply(X0,identity),identity)),
inference(demodulation,[status(thm)],[c_1452,c_134,c_249]) ).
tcf(c_4239,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(multiply(identity,multiply(multiply(X0,X0),multiply(multiply(X0,multiply(X1,identity)),identity))),X2) = multiply(identity,multiply(multiply(multiply(X0,multiply(multiply(X0,X0),multiply(X1,X2))),identity),identity)),
inference(superposition,[status(thm)],[c_564,c_4233]) ).
tcf(c_4243,plain,
! [X0: $i,X1: $i] : multiply(multiply(identity,multiply(X0,multiply(multiply(X1,X1),multiply(multiply(X1,identity),identity)))),multiply(multiply(X1,identity),identity)) = multiply(identity,multiply(multiply(X0,identity),identity)),
inference(superposition,[status(thm)],[c_999,c_4233]) ).
tcf(c_4355,plain,
! [X0: $i,X1: $i] : multiply(multiply(identity,multiply(identity,multiply(identity,multiply(multiply(X0,identity),identity)))),multiply(multiply(multiply(X1,identity),identity),multiply(multiply(multiply(X1,identity),identity),multiply(multiply(X1,identity),identity)))) = multiply(identity,multiply(identity,multiply(multiply(multiply(identity,multiply(X0,multiply(multiply(X1,X1),multiply(multiply(X1,identity),identity)))),identity),identity))),
inference(superposition,[status(thm)],[c_4243,c_238]) ).
tcf(c_4362,plain,
! [X0: $i,X1: $i] : multiply(identity,multiply(identity,multiply(multiply(multiply(identity,multiply(X0,multiply(multiply(X1,X1),multiply(multiply(X1,identity),identity)))),identity),identity))) = multiply(X0,multiply(multiply(multiply(X1,identity),identity),multiply(multiply(multiply(X1,identity),identity),multiply(multiply(X1,identity),identity)))),
inference(light_normalisation,[status(thm)],[c_4355,c_134]) ).
tcf(c_5601,plain,
! [X0: $i] : multiply(multiply(identity,X0),multiply(multiply(multiply(identity,X0),multiply(identity,X0)),identity)) = multiply(identity,multiply(X0,multiply(multiply(X0,X0),identity))),
inference(demodulation,[status(thm)],[c_1997,c_2228,c_2648]) ).
tcf(c_6305,plain,
! [X0: $i,X1: $i] : multiply(multiply(identity,multiply(identity,multiply(identity,multiply(multiply(X0,identity),identity)))),multiply(multiply(X1,X1),multiply(multiply(X1,identity),identity))) = multiply(identity,multiply(identity,multiply(multiply(multiply(identity,multiply(X0,multiply(multiply(X1,X1),multiply(multiply(X1,identity),identity)))),identity),identity))),
inference(superposition,[status(thm)],[c_4243,c_2868]) ).
tcf(c_6339,plain,
! [X0: $i,X1: $i] : multiply(X0,multiply(multiply(multiply(X1,identity),identity),multiply(multiply(multiply(X1,identity),identity),multiply(multiply(X1,identity),identity)))) = multiply(X0,multiply(multiply(X1,X1),multiply(multiply(X1,identity),identity))),
inference(light_normalisation,[status(thm)],[c_6305,c_134,c_4362]) ).
tcf(c_6390,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(multiply(multiply(multiply(X0,X0),multiply(X0,X0)),multiply(multiply(X0,X0),multiply(X0,X0))),multiply(multiply(multiply(multiply(X0,X0),multiply(X0,X0)),multiply(multiply(multiply(X0,multiply(multiply(X0,X1),identity)),identity),identity)),identity)) = multiply(multiply(multiply(X0,X0),multiply(X1,multiply(X2,multiply(X2,X2)))),X2),
inference(superposition,[status(thm)],[c_3205,c_543]) ).
tcf(c_6409,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(multiply(multiply(X0,X0),multiply(X1,multiply(X2,multiply(X2,X2)))),X2) = multiply(multiply(multiply(X0,X0),multiply(X1,identity)),identity),
inference(light_normalisation,[status(thm)],[c_6390,c_2609]) ).
tcf(c_6441,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(multiply(multiply(X0,X0),multiply(multiply(identity,multiply(identity,multiply(X1,X2))),identity)),identity) = multiply(multiply(multiply(X0,X0),multiply(identity,multiply(identity,multiply(multiply(X1,identity),identity)))),X2),
inference(superposition,[status(thm)],[c_238,c_6409]) ).
tcf(c_6712,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(multiply(identity,multiply(multiply(X0,X0),multiply(multiply(X0,multiply(X1,identity)),identity))),X2) = multiply(identity,multiply(multiply(multiply(X0,X0),multiply(multiply(X0,multiply(X1,X2)),identity)),identity)),
inference(demodulation,[status(thm)],[c_4239,c_3823]) ).
tcf(c_6724,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(identity,multiply(multiply(multiply(X0,X0),multiply(multiply(X0,multiply(multiply(X0,X1),X2)),identity)),identity)) = multiply(multiply(identity,X1),X2),
inference(superposition,[status(thm)],[c_543,c_6712]) ).
tcf(c_6752,plain,
! [X0: $i,X1: $i] : multiply(identity,multiply(multiply(multiply(X0,X0),multiply(multiply(X0,multiply(identity,X1)),identity)),identity)) = multiply(multiply(identity,multiply(multiply(X0,X0),multiply(multiply(X0,identity),identity))),X1),
inference(superposition,[status(thm)],[c_53,c_6712]) ).
tcf(c_7264,plain,
! [X0: $i,X1: $i] : multiply(identity,multiply(multiply(multiply(X0,X0),multiply(multiply(identity,multiply(identity,multiply(identity,multiply(X1,identity)))),identity)),identity)) = multiply(multiply(identity,X0),multiply(multiply(X0,X1),identity)),
inference(superposition,[status(thm)],[c_2648,c_6724]) ).
tcf(c_7279,plain,
! [X0: $i,X1: $i] : multiply(identity,multiply(multiply(multiply(X0,X0),multiply(multiply(X0,multiply(multiply(X0,X0),multiply(multiply(X0,X1),identity))),identity)),identity)) = multiply(multiply(identity,multiply(multiply(X0,X0),X1)),identity),
inference(superposition,[status(thm)],[c_3823,c_6724]) ).
tcf(c_7401,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(X0,multiply(multiply(X0,X0),multiply(multiply(X0,X1),X2))) = multiply(identity,multiply(identity,multiply(multiply(identity,X1),X2))),
inference(superposition,[status(thm)],[c_6724,c_3925]) ).
tcf(c_7419,plain,
! [X0: $i,X1: $i] : multiply(identity,multiply(multiply(multiply(X0,X0),multiply(multiply(identity,multiply(identity,multiply(identity,multiply(X1,identity)))),identity)),identity)) = multiply(multiply(identity,multiply(multiply(X0,X0),X1)),identity),
inference(light_normalisation,[status(thm)],[c_7279,c_2648]) ).
tcf(c_7776,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(multiply(X0,X0),multiply(multiply(X0,multiply(multiply(X0,X1),X2)),identity)) = multiply(multiply(identity,multiply(identity,multiply(multiply(identity,X1),X2))),identity),
inference(superposition,[status(thm)],[c_7401,c_3823]) ).
tcf(c_8314,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(multiply(X0,X0),multiply(multiply(X0,multiply(multiply(X0,X1),X2)),identity)) = multiply(identity,multiply(identity,multiply(multiply(multiply(identity,X1),X2),identity))),
inference(demodulation,[status(thm)],[c_7776,c_249]) ).
tcf(c_8459,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(X0,multiply(identity,multiply(identity,multiply(multiply(multiply(identity,X1),X2),identity)))) = multiply(identity,multiply(identity,multiply(multiply(identity,multiply(multiply(X0,X1),X2)),identity))),
inference(superposition,[status(thm)],[c_8314,c_7401]) ).
tcf(c_11055,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(X0,multiply(identity,multiply(identity,multiply(multiply(multiply(identity,X1),X2),identity)))) = multiply(identity,multiply(identity,multiply(identity,multiply(multiply(multiply(X0,X1),X2),identity)))),
inference(demodulation,[status(thm)],[c_8459,c_249]) ).
tcf(c_11100,plain,
! [X0: $i,X1: $i] : multiply(identity,multiply(identity,multiply(identity,multiply(multiply(multiply(X0,identity),X1),identity)))) = multiply(X0,multiply(identity,multiply(identity,multiply(multiply(identity,X1),identity)))),
inference(superposition,[status(thm)],[c_53,c_11055]) ).
tcf(c_11582,plain,
! [X0: $i,X1: $i] : multiply(identity,multiply(identity,multiply(identity,multiply(multiply(multiply(X0,identity),X1),identity)))) = multiply(X0,multiply(identity,multiply(identity,multiply(identity,multiply(X1,identity))))),
inference(demodulation,[status(thm)],[c_11100,c_249]) ).
tcf(c_11646,plain,
! [X0: $i,X1: $i] : multiply(identity,multiply(multiply(identity,multiply(identity,multiply(multiply(multiply(X0,identity),X1),identity))),identity)) = multiply(multiply(X0,multiply(identity,multiply(identity,multiply(identity,multiply(X1,identity))))),identity),
inference(superposition,[status(thm)],[c_11582,c_249]) ).
tcf(c_13100,plain,
! [X0: $i,X1: $i] : multiply(identity,multiply(identity,multiply(multiply(identity,multiply(multiply(X0,X0),multiply(multiply(X0,identity),identity))),X1))) = multiply(X0,multiply(multiply(X0,X0),multiply(identity,X1))),
inference(superposition,[status(thm)],[c_6752,c_3925]) ).
tcf(c_13409,plain,
! [X0: $i,X1: $i] : multiply(identity,multiply(multiply(multiply(X0,X0),identity),multiply(X1,identity))) = multiply(multiply(identity,X0),multiply(multiply(X0,X1),identity)),
inference(demodulation,[status(thm)],[c_7264,c_53,c_249,c_6441]) ).
tcf(c_13844,plain,
! [X0: $i,X1: $i] : multiply(multiply(identity,X0),multiply(multiply(X0,X1),identity)) = multiply(identity,multiply(multiply(multiply(X0,X0),X1),identity)),
inference(demodulation,[status(thm)],[c_7419,c_53,c_249,c_6441,c_13409]) ).
tcf(c_15298,plain,
! [X0: $i,X1: $i] : multiply(multiply(X0,multiply(identity,multiply(identity,multiply(identity,multiply(X1,identity))))),identity) = multiply(multiply(X0,identity),X1),
inference(demodulation,[status(thm)],[c_11646,c_134,c_249]) ).
tcf(c_15299,plain,
! [X0: $i,X1: $i] : multiply(multiply(X0,X0),multiply(multiply(multiply(X0,X0),multiply(X0,X0)),X1)) = multiply(X0,multiply(multiply(X0,identity),X1)),
inference(demodulation,[status(thm)],[c_511,c_15298]) ).
tcf(c_15313,plain,
! [X0: $i,X1: $i] : multiply(multiply(X0,identity),multiply(X1,identity)) = multiply(multiply(X0,X1),identity),
inference(superposition,[status(thm)],[c_134,c_15298]) ).
tcf(c_15314,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(multiply(X0,identity),multiply(multiply(X1,X1),multiply(multiply(X1,X2),identity))) = multiply(multiply(X0,multiply(X1,multiply(multiply(X1,X1),X2))),identity),
inference(superposition,[status(thm)],[c_3925,c_15298]) ).
tcf(c_15409,plain,
! [X0: $i] : multiply(multiply(multiply(X0,identity),identity),multiply(multiply(multiply(X0,identity),multiply(X0,identity)),identity)) = multiply(multiply(X0,X0),multiply(multiply(X0,identity),identity)),
inference(demodulation,[status(thm)],[c_999,c_15313]) ).
tcf(c_15494,plain,
! [X0: $i,X1: $i] : multiply(multiply(identity,multiply(X0,identity)),multiply(X1,identity)) = multiply(multiply(multiply(identity,X0),X1),identity),
inference(superposition,[status(thm)],[c_249,c_15313]) ).
tcf(c_15495,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(multiply(multiply(X0,X0),multiply(multiply(X0,X1),identity)),multiply(X2,identity)) = multiply(multiply(multiply(X0,multiply(multiply(X0,X0),X1)),X2),identity),
inference(superposition,[status(thm)],[c_3823,c_15313]) ).
tcf(c_15501,plain,
! [X0: $i,X1: $i] : multiply(multiply(X0,identity),multiply(identity,multiply(X1,identity))) = multiply(multiply(X0,multiply(identity,X1)),identity),
inference(superposition,[status(thm)],[c_249,c_15313]) ).
tcf(c_15560,plain,
! [X0: $i,X1: $i] : multiply(multiply(identity,multiply(X0,multiply(multiply(X1,identity),multiply(multiply(X1,X1),identity)))),multiply(X1,identity)) = multiply(identity,multiply(multiply(X0,identity),identity)),
inference(superposition,[status(thm)],[c_15313,c_4233]) ).
tcf(c_15778,plain,
! [X0: $i,X1: $i] : multiply(multiply(identity,multiply(identity,multiply(X0,identity))),multiply(X1,identity)) = multiply(multiply(multiply(identity,multiply(identity,X0)),X1),identity),
inference(superposition,[status(thm)],[c_249,c_15494]) ).
tcf(c_15786,plain,
! [X0: $i,X1: $i] : multiply(multiply(identity,multiply(X0,identity)),multiply(identity,multiply(X1,identity))) = multiply(multiply(multiply(identity,X0),multiply(identity,X1)),identity),
inference(superposition,[status(thm)],[c_249,c_15494]) ).
tcf(c_15816,plain,
! [X0: $i] : multiply(multiply(multiply(identity,X0),multiply(multiply(identity,multiply(X0,identity)),multiply(identity,multiply(X0,identity)))),identity) = multiply(identity,multiply(multiply(X0,identity),multiply(multiply(multiply(X0,identity),multiply(X0,identity)),identity))),
inference(superposition,[status(thm)],[c_15494,c_5601]) ).
tcf(c_15941,plain,
! [X0: $i,X1: $i] : multiply(multiply(X0,identity),multiply(identity,multiply(identity,multiply(X1,identity)))) = multiply(multiply(X0,multiply(identity,multiply(identity,X1))),identity),
inference(superposition,[status(thm)],[c_249,c_15501]) ).
tcf(c_16046,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(multiply(multiply(X0,X0),multiply(X0,X0)),multiply(multiply(multiply(X0,X0),multiply(X1,identity)),identity)) = multiply(multiply(X0,multiply(multiply(X0,identity),multiply(X1,X2))),multiply(X2,multiply(X2,X2))),
inference(superposition,[status(thm)],[c_15299,c_564]) ).
tcf(c_16082,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(multiply(X0,multiply(multiply(X0,identity),multiply(X1,X2))),multiply(X2,multiply(X2,X2))) = multiply(multiply(X0,multiply(multiply(X0,X1),identity)),identity),
inference(light_normalisation,[status(thm)],[c_16046,c_576]) ).
tcf(c_16242,plain,
! [X0: $i,X1: $i] : multiply(multiply(multiply(identity,multiply(identity,multiply(identity,multiply(multiply(X0,X0),multiply(multiply(X0,identity),identity))))),X1),identity) = multiply(multiply(X0,multiply(multiply(X0,X0),multiply(identity,identity))),multiply(X1,identity)),
inference(superposition,[status(thm)],[c_13100,c_15778]) ).
tcf(c_16247,plain,
! [X0: $i,X1: $i] : multiply(multiply(identity,multiply(identity,multiply(identity,multiply(X0,identity)))),multiply(X1,identity)) = multiply(multiply(multiply(identity,multiply(identity,multiply(identity,X0))),X1),identity),
inference(superposition,[status(thm)],[c_249,c_15778]) ).
tcf(c_16251,plain,
! [X0: $i,X1: $i] : multiply(multiply(multiply(identity,multiply(identity,multiply(identity,multiply(X0,multiply(identity,multiply(identity,identity)))))),X1),identity) = multiply(multiply(identity,multiply(identity,multiply(identity,multiply(multiply(X0,identity),identity)))),multiply(X1,identity)),
inference(superposition,[status(thm)],[c_4233,c_15778]) ).
tcf(c_16299,plain,
! [X0: $i,X1: $i] : multiply(multiply(multiply(identity,multiply(identity,multiply(identity,multiply(X0,identity)))),X1),identity) = multiply(X0,multiply(X1,identity)),
inference(light_normalisation,[status(thm)],[c_16251,c_53,c_134]) ).
tcf(c_16300,plain,
! [X0: $i,X1: $i] : multiply(multiply(multiply(identity,multiply(identity,multiply(identity,multiply(multiply(X0,X0),multiply(multiply(X0,identity),identity))))),X1),identity) = multiply(multiply(X0,multiply(multiply(X0,X0),identity)),multiply(X1,identity)),
inference(light_normalisation,[status(thm)],[c_16242,c_53]) ).
tcf(c_16383,plain,
! [X0: $i] : multiply(X0,multiply(multiply(multiply(X0,identity),multiply(multiply(X0,identity),multiply(X0,identity))),identity)) = multiply(multiply(identity,multiply(identity,multiply(multiply(identity,identity),identity))),identity),
inference(superposition,[status(thm)],[c_238,c_16299]) ).
tcf(c_16466,plain,
! [X0: $i,X1: $i] : multiply(identity,multiply(identity,multiply(identity,multiply(multiply(X0,multiply(X1,identity)),identity)))) = multiply(multiply(identity,multiply(identity,multiply(identity,multiply(X0,identity)))),X1),
inference(superposition,[status(thm)],[c_16299,c_134]) ).
tcf(c_16521,plain,
! [X0: $i] : multiply(X0,multiply(multiply(multiply(X0,identity),multiply(multiply(X0,identity),multiply(X0,identity))),identity)) = identity,
inference(light_normalisation,[status(thm)],[c_16383,c_53]) ).
tcf(c_16563,plain,
! [X0: $i,X1: $i] : multiply(multiply(identity,multiply(identity,multiply(identity,multiply(multiply(X0,X0),identity)))),multiply(X0,X1)) = multiply(X0,multiply(multiply(X0,X0),X1)),
inference(demodulation,[status(thm)],[c_3925,c_16466]) ).
tcf(c_16810,plain,
! [X0: $i] : multiply(X0,multiply(multiply(multiply(X0,multiply(X0,X0)),identity),identity)) = identity,
inference(demodulation,[status(thm)],[c_16521,c_15313]) ).
tcf(c_16824,plain,
! [X0: $i] : multiply(identity,multiply(multiply(multiply(X0,X0),multiply(multiply(multiply(X0,multiply(X0,X0)),identity),identity)),identity)) = multiply(multiply(identity,X0),multiply(identity,identity)),
inference(superposition,[status(thm)],[c_16810,c_13844]) ).
tcf(c_16828,plain,
! [X0: $i,X1: $i] : multiply(identity,multiply(identity,multiply(multiply(identity,multiply(multiply(multiply(X0,multiply(X0,X0)),identity),identity)),X1))) = multiply(X0,multiply(multiply(X0,X0),multiply(identity,X1))),
inference(superposition,[status(thm)],[c_16810,c_7401]) ).
tcf(c_16892,plain,
! [X0: $i] : multiply(identity,multiply(multiply(multiply(X0,X0),multiply(multiply(multiply(X0,multiply(X0,X0)),identity),identity)),identity)) = multiply(identity,multiply(X0,identity)),
inference(light_normalisation,[status(thm)],[c_16824,c_53,c_249]) ).
tcf(c_17030,plain,
! [X0: $i] : multiply(multiply(identity,multiply(X0,identity)),multiply(multiply(multiply(multiply(identity,X0),multiply(identity,X0)),identity),identity)) = multiply(identity,multiply(multiply(X0,identity),multiply(multiply(multiply(X0,identity),multiply(X0,identity)),identity))),
inference(superposition,[status(thm)],[c_15786,c_5601]) ).
tcf(c_17184,plain,
! [X0: $i,X1: $i] : multiply(multiply(X0,multiply(identity,multiply(identity,multiply(identity,multiply(multiply(X1,X1),multiply(multiply(X1,identity),identity)))))),identity) = multiply(multiply(X0,identity),multiply(X1,multiply(multiply(X1,X1),multiply(identity,identity)))),
inference(superposition,[status(thm)],[c_13100,c_15941]) ).
tcf(c_17189,plain,
! [X0: $i,X1: $i] : multiply(multiply(X0,identity),multiply(identity,multiply(identity,multiply(identity,multiply(X1,identity))))) = multiply(multiply(X0,multiply(identity,multiply(identity,multiply(identity,X1)))),identity),
inference(superposition,[status(thm)],[c_249,c_15941]) ).
tcf(c_17221,plain,
! [X0: $i,X1: $i] : multiply(multiply(X0,multiply(identity,multiply(identity,multiply(identity,multiply(multiply(X1,X1),multiply(multiply(X1,identity),identity)))))),identity) = multiply(multiply(X0,identity),multiply(X1,multiply(multiply(X1,X1),identity))),
inference(light_normalisation,[status(thm)],[c_17184,c_53]) ).
tcf(c_18226,plain,
! [X0: $i,X1: $i] : multiply(multiply(X0,multiply(identity,multiply(identity,multiply(identity,multiply(multiply(X0,identity),identity))))),multiply(multiply(X0,identity),X1)) = multiply(multiply(X0,identity),multiply(multiply(multiply(X0,identity),multiply(X0,identity)),X1)),
inference(superposition,[status(thm)],[c_11582,c_16563]) ).
tcf(c_18239,plain,
! [X0: $i] : multiply(multiply(identity,multiply(identity,multiply(identity,multiply(multiply(multiply(identity,X0),multiply(identity,X0)),identity)))),multiply(identity,multiply(X0,identity))) = multiply(multiply(identity,X0),multiply(multiply(multiply(identity,X0),multiply(identity,X0)),identity)),
inference(superposition,[status(thm)],[c_249,c_16563]) ).
tcf(c_18371,plain,
! [X0: $i,X1: $i] : multiply(multiply(X0,identity),multiply(multiply(multiply(X0,identity),multiply(X0,identity)),X1)) = multiply(multiply(X0,X0),multiply(multiply(X0,identity),X1)),
inference(light_normalisation,[status(thm)],[c_18226,c_134]) ).
tcf(c_18372,plain,
! [X0: $i] : multiply(multiply(identity,multiply(identity,multiply(identity,multiply(multiply(multiply(identity,X0),multiply(identity,X0)),identity)))),multiply(identity,multiply(X0,identity))) = multiply(identity,multiply(X0,multiply(multiply(X0,X0),identity))),
inference(light_normalisation,[status(thm)],[c_18239,c_5601]) ).
tcf(c_18637,plain,
! [X0: $i,X1: $i] : multiply(multiply(multiply(X0,X0),multiply(multiply(multiply(X0,multiply(X0,X0)),identity),identity)),multiply(X1,identity)) = multiply(multiply(multiply(identity,multiply(identity,multiply(identity,multiply(X0,identity)))),X1),identity),
inference(superposition,[status(thm)],[c_16892,c_16299]) ).
tcf(c_18680,plain,
! [X0: $i,X1: $i] : multiply(multiply(multiply(X0,X0),multiply(multiply(multiply(X0,multiply(X0,X0)),identity),identity)),multiply(X1,identity)) = multiply(X0,multiply(X1,identity)),
inference(light_normalisation,[status(thm)],[c_18637,c_16299]) ).
tcf(c_18784,plain,
! [X0: $i,X1: $i] : multiply(multiply(X0,identity),multiply(multiply(multiply(X0,X0),identity),X1)) = multiply(multiply(X0,X0),multiply(multiply(X0,identity),X1)),
inference(demodulation,[status(thm)],[c_18371,c_15313]) ).
tcf(c_19412,plain,
! [X0: $i] : multiply(multiply(multiply(X0,X0),multiply(multiply(multiply(X0,multiply(X0,X0)),identity),identity)),identity) = multiply(X0,identity),
inference(superposition,[status(thm)],[c_53,c_18680]) ).
tcf(c_19794,plain,
! [X0: $i] : multiply(multiply(X0,X0),multiply(multiply(multiply(X0,multiply(X0,X0)),identity),identity)) = multiply(identity,multiply(identity,multiply(identity,multiply(multiply(X0,identity),identity)))),
inference(superposition,[status(thm)],[c_19412,c_134]) ).
tcf(c_19809,plain,
! [X0: $i] : multiply(multiply(X0,X0),multiply(multiply(multiply(X0,multiply(X0,X0)),identity),identity)) = X0,
inference(light_normalisation,[status(thm)],[c_19794,c_134]) ).
tcf(c_19909,plain,
! [X0: $i,X1: $i] : multiply(identity,multiply(identity,multiply(multiply(identity,multiply(multiply(multiply(X0,multiply(X0,X0)),identity),identity)),X1))) = multiply(multiply(X0,X0),multiply(multiply(multiply(X0,X0),multiply(X0,X0)),multiply(X0,X1))),
inference(superposition,[status(thm)],[c_19809,c_7401]) ).
tcf(c_19929,plain,
! [X0: $i,X1: $i] : multiply(multiply(X0,X0),multiply(multiply(multiply(X0,X0),multiply(X0,X0)),multiply(X0,X1))) = multiply(X0,multiply(multiply(X0,X0),multiply(identity,X1))),
inference(light_normalisation,[status(thm)],[c_19909,c_16828]) ).
tcf(c_19953,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : multiply(multiply(multiply(X0,X0),multiply(multiply(X0,X1),identity)),multiply(multiply(X2,X2),multiply(multiply(X2,X3),identity))) = multiply(multiply(multiply(X0,multiply(multiply(X0,X0),X1)),multiply(X2,multiply(multiply(X2,X2),X3))),identity),
inference(superposition,[status(thm)],[c_3823,c_15314]) ).
tcf(c_20455,plain,
! [X0: $i] : multiply(multiply(multiply(X0,multiply(X0,X0)),identity),identity) = multiply(multiply(X0,X0),multiply(multiply(X0,identity),identity)),
inference(demodulation,[status(thm)],[c_15409,c_15313]) ).
tcf(c_20483,plain,
! [X0: $i,X1: $i] : multiply(multiply(X0,multiply(identity,multiply(identity,multiply(identity,multiply(multiply(X1,X1),multiply(multiply(X1,identity),identity)))))),identity) = multiply(multiply(X0,identity),multiply(multiply(X1,multiply(X1,X1)),identity)),
inference(superposition,[status(thm)],[c_20455,c_15298]) ).
tcf(c_20488,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(multiply(multiply(X0,X0),multiply(multiply(X0,identity),identity)),multiply(multiply(X1,X1),multiply(multiply(X1,X2),identity))) = multiply(multiply(multiply(multiply(X0,multiply(X0,X0)),identity),multiply(X1,multiply(multiply(X1,X1),X2))),identity),
inference(superposition,[status(thm)],[c_20455,c_15314]) ).
tcf(c_20496,plain,
! [X0: $i,X1: $i] : multiply(multiply(multiply(identity,multiply(identity,multiply(identity,multiply(multiply(X0,X0),multiply(multiply(X0,identity),identity))))),X1),identity) = multiply(multiply(multiply(X0,multiply(X0,X0)),identity),multiply(X1,identity)),
inference(superposition,[status(thm)],[c_20455,c_16299]) ).
tcf(c_20536,plain,
! [X0: $i] : multiply(identity,multiply(identity,multiply(identity,multiply(multiply(X0,X0),multiply(multiply(X0,identity),identity))))) = multiply(X0,multiply(X0,X0)),
inference(superposition,[status(thm)],[c_20455,c_134]) ).
tcf(c_20557,plain,
! [X0: $i,X1: $i] : multiply(multiply(multiply(X0,multiply(X0,X0)),identity),multiply(X1,identity)) = multiply(multiply(X0,multiply(multiply(X0,X0),identity)),multiply(X1,identity)),
inference(light_normalisation,[status(thm)],[c_20496,c_16300]) ).
tcf(c_20558,plain,
! [X0: $i,X1: $i] : multiply(multiply(X0,identity),multiply(multiply(X1,multiply(X1,X1)),identity)) = multiply(multiply(X0,identity),multiply(X1,multiply(multiply(X1,X1),identity))),
inference(light_normalisation,[status(thm)],[c_20483,c_17221]) ).
tcf(c_21137,plain,
! [X0: $i,X1: $i] : multiply(multiply(X0,multiply(multiply(X0,X0),identity)),multiply(X1,identity)) = multiply(multiply(multiply(X0,multiply(X0,X0)),X1),identity),
inference(demodulation,[status(thm)],[c_20557,c_15313]) ).
tcf(c_21161,plain,
! [X0: $i,X1: $i] : multiply(multiply(X0,multiply(multiply(X0,X0),identity)),multiply(identity,multiply(X1,identity))) = multiply(multiply(multiply(X0,multiply(X0,X0)),multiply(identity,X1)),identity),
inference(superposition,[status(thm)],[c_249,c_21137]) ).
tcf(c_21278,plain,
! [X0: $i,X1: $i] : multiply(multiply(X0,identity),multiply(X1,multiply(multiply(X1,X1),identity))) = multiply(multiply(X0,multiply(X1,multiply(X1,X1))),identity),
inference(demodulation,[status(thm)],[c_20558,c_15313]) ).
tcf(c_21281,plain,
! [X0: $i] : multiply(multiply(identity,multiply(X0,multiply(X0,X0))),identity) = multiply(identity,multiply(X0,multiply(multiply(X0,X0),identity))),
inference(superposition,[status(thm)],[c_53,c_21278]) ).
tcf(c_21298,plain,
! [X0: $i,X1: $i] : multiply(multiply(X0,multiply(multiply(X1,multiply(multiply(X1,X1),identity)),multiply(multiply(X1,multiply(multiply(X1,X1),identity)),multiply(X1,multiply(multiply(X1,X1),identity))))),identity) = multiply(multiply(X0,identity),multiply(multiply(multiply(X1,multiply(X1,X1)),multiply(multiply(X1,multiply(multiply(X1,X1),identity)),multiply(X1,multiply(multiply(X1,X1),identity)))),identity)),
inference(superposition,[status(thm)],[c_21137,c_21278]) ).
tcf(c_21611,plain,
! [X0: $i] : multiply(identity,multiply(multiply(X0,multiply(X0,X0)),identity)) = multiply(identity,multiply(X0,multiply(multiply(X0,X0),identity))),
inference(demodulation,[status(thm)],[c_21281,c_249]) ).
tcf(c_21630,plain,
! [X0: $i] : multiply(multiply(identity,multiply(identity,multiply(X0,multiply(multiply(X0,X0),identity)))),multiply(identity,multiply(identity,identity))) = multiply(identity,multiply(identity,multiply(multiply(multiply(X0,multiply(X0,X0)),identity),identity))),
inference(superposition,[status(thm)],[c_21611,c_238]) ).
tcf(c_21673,plain,
! [X0: $i] : multiply(multiply(identity,multiply(identity,multiply(X0,multiply(multiply(X0,X0),identity)))),identity) = multiply(identity,multiply(identity,multiply(multiply(X0,X0),multiply(multiply(X0,identity),identity)))),
inference(light_normalisation,[status(thm)],[c_21630,c_53,c_20455]) ).
tcf(c_22416,plain,
! [X0: $i,X1: $i] : multiply(multiply(identity,multiply(X0,multiply(multiply(X1,multiply(X1,X1)),identity))),multiply(X1,identity)) = multiply(identity,multiply(multiply(X0,identity),identity)),
inference(demodulation,[status(thm)],[c_15560,c_15313]) ).
tcf(c_23612,plain,
! [X0: $i,X1: $i] : multiply(multiply(multiply(multiply(identity,multiply(identity,multiply(identity,X0))),X1),identity),identity) = multiply(X0,multiply(multiply(X1,identity),identity)),
inference(superposition,[status(thm)],[c_16247,c_16299]) ).
tcf(c_23613,plain,
! [X0: $i] : multiply(multiply(multiply(identity,multiply(identity,multiply(identity,multiply(X0,X0)))),X0),identity) = multiply(X0,multiply(multiply(X0,X0),identity)),
inference(superposition,[status(thm)],[c_16247,c_16563]) ).
tcf(c_23741,plain,
! [X0: $i,X1: $i] : multiply(multiply(multiply(X0,X0),multiply(multiply(X0,identity),identity)),multiply(multiply(X1,identity),identity)) = multiply(multiply(multiply(multiply(X0,multiply(X0,X0)),X1),identity),identity),
inference(superposition,[status(thm)],[c_20536,c_23612]) ).
tcf(c_23845,plain,
! [X0: $i,X1: $i] : multiply(identity,multiply(identity,multiply(identity,multiply(X0,multiply(multiply(X1,identity),identity))))) = multiply(multiply(identity,multiply(identity,multiply(identity,X0))),X1),
inference(superposition,[status(thm)],[c_23612,c_134]) ).
tcf(c_23913,plain,
! [X0: $i] : multiply(multiply(identity,multiply(identity,multiply(identity,multiply(X0,X0)))),X0) = multiply(X0,multiply(X0,X0)),
inference(demodulation,[status(thm)],[c_20536,c_23845]) ).
tcf(c_24057,plain,
! [X0: $i] : multiply(multiply(identity,multiply(identity,multiply(identity,multiply(multiply(multiply(identity,X0),multiply(identity,X0)),identity)))),multiply(identity,multiply(X0,identity))) = multiply(multiply(identity,multiply(X0,identity)),multiply(multiply(multiply(identity,X0),multiply(identity,X0)),identity)),
inference(superposition,[status(thm)],[c_15786,c_23913]) ).
tcf(c_24187,plain,
! [X0: $i] : multiply(multiply(identity,multiply(X0,identity)),multiply(multiply(multiply(identity,X0),multiply(identity,X0)),identity)) = multiply(identity,multiply(X0,multiply(multiply(X0,X0),identity))),
inference(light_normalisation,[status(thm)],[c_24057,c_18372]) ).
tcf(c_24253,plain,
! [X0: $i] : multiply(multiply(X0,multiply(X0,X0)),identity) = multiply(X0,multiply(multiply(X0,X0),identity)),
inference(light_normalisation,[status(thm)],[c_23613,c_23913]) ).
tcf(c_24256,plain,
! [X0: $i,X1: $i] : multiply(multiply(identity,multiply(X0,multiply(X1,multiply(multiply(X1,X1),identity)))),multiply(X1,identity)) = multiply(identity,multiply(multiply(X0,identity),identity)),
inference(demodulation,[status(thm)],[c_22416,c_24253]) ).
tcf(c_24269,plain,
! [X0: $i] : multiply(multiply(multiply(identity,multiply(X0,identity)),multiply(multiply(multiply(identity,X0),multiply(identity,X0)),identity)),identity) = multiply(multiply(identity,multiply(X0,identity)),multiply(multiply(multiply(multiply(identity,X0),multiply(identity,X0)),identity),identity)),
inference(superposition,[status(thm)],[c_15786,c_24253]) ).
tcf(c_24282,plain,
! [X0: $i] : multiply(multiply(identity,multiply(identity,multiply(X0,multiply(multiply(X0,X0),identity)))),multiply(identity,multiply(identity,identity))) = multiply(identity,multiply(identity,multiply(multiply(X0,multiply(multiply(X0,X0),identity)),identity))),
inference(superposition,[status(thm)],[c_24253,c_238]) ).
tcf(c_24300,plain,
! [X0: $i,X1: $i] : multiply(multiply(X0,multiply(multiply(X0,X0),identity)),multiply(X1,multiply(multiply(X1,X1),identity))) = multiply(multiply(multiply(X0,multiply(X0,X0)),multiply(X1,multiply(X1,X1))),identity),
inference(superposition,[status(thm)],[c_24253,c_21278]) ).
tcf(c_24363,plain,
! [X0: $i] : multiply(identity,multiply(identity,multiply(multiply(X0,multiply(multiply(X0,X0),identity)),identity))) = multiply(identity,multiply(identity,multiply(multiply(X0,X0),multiply(multiply(X0,identity),identity)))),
inference(light_normalisation,[status(thm)],[c_24282,c_53,c_21673]) ).
tcf(c_24366,plain,
! [X0: $i] : multiply(identity,multiply(multiply(X0,identity),multiply(multiply(multiply(X0,identity),multiply(X0,identity)),identity))) = multiply(multiply(identity,multiply(X0,multiply(multiply(X0,X0),identity))),identity),
inference(light_normalisation,[status(thm)],[c_24269,c_17030,c_24187]) ).
tcf(c_24413,plain,
! [X0: $i,X1: $i] : multiply(multiply(identity,multiply(identity,multiply(identity,multiply(identity,multiply(X0,multiply(multiply(X1,X1),multiply(multiply(X1,identity),identity))))))),X1) = multiply(identity,multiply(identity,multiply(identity,multiply(identity,multiply(multiply(X0,identity),identity))))),
inference(superposition,[status(thm)],[c_4243,c_23845]) ).
tcf(c_24419,plain,
! [X0: $i] : multiply(identity,multiply(identity,multiply(identity,multiply(multiply(X0,X0),multiply(multiply(X0,identity),identity))))) = multiply(multiply(identity,multiply(identity,multiply(identity,multiply(X0,identity)))),multiply(X0,X0)),
inference(superposition,[status(thm)],[c_18784,c_23845]) ).
tcf(c_24510,plain,
! [X0: $i,X1: $i] : multiply(multiply(identity,multiply(identity,multiply(identity,multiply(identity,multiply(X0,multiply(multiply(X1,X1),multiply(multiply(X1,identity),identity))))))),X1) = multiply(identity,X0),
inference(light_normalisation,[status(thm)],[c_24413,c_134]) ).
tcf(c_24744,plain,
! [X0: $i] : multiply(multiply(identity,multiply(identity,multiply(multiply(identity,X0),multiply(multiply(multiply(identity,X0),multiply(identity,X0)),identity)))),multiply(multiply(identity,X0),identity)) = multiply(identity,multiply(multiply(multiply(identity,identity),identity),identity)),
inference(superposition,[status(thm)],[c_7401,c_24256]) ).
tcf(c_24827,plain,
! [X0: $i] : multiply(multiply(identity,multiply(identity,multiply(identity,multiply(X0,multiply(multiply(X0,X0),identity))))),multiply(identity,multiply(X0,identity))) = identity,
inference(light_normalisation,[status(thm)],[c_24744,c_53,c_249,c_5601]) ).
tcf(c_24948,plain,
! [X0: $i] : multiply(multiply(X0,multiply(multiply(X0,X0),identity)),multiply(multiply(multiply(identity,multiply(X0,identity)),identity),identity)) = multiply(multiply(identity,identity),identity),
inference(superposition,[status(thm)],[c_24827,c_23612]) ).
tcf(c_24953,plain,
! [X0: $i] : multiply(multiply(X0,multiply(multiply(X0,X0),identity)),multiply(multiply(multiply(identity,multiply(X0,identity)),identity),identity)) = identity,
inference(light_normalisation,[status(thm)],[c_24948,c_53]) ).
tcf(c_25028,plain,
! [X0: $i] : multiply(multiply(multiply(X0,multiply(X0,X0)),multiply(identity,multiply(multiply(X0,identity),identity))),identity) = identity,
inference(demodulation,[status(thm)],[c_24953,c_249,c_21137]) ).
tcf(c_25117,plain,
! [X0: $i] : multiply(multiply(X0,multiply(X0,X0)),multiply(identity,multiply(multiply(X0,identity),identity))) = multiply(identity,multiply(identity,multiply(identity,multiply(identity,identity)))),
inference(superposition,[status(thm)],[c_25028,c_134]) ).
tcf(c_25128,plain,
! [X0: $i] : multiply(multiply(X0,multiply(X0,X0)),multiply(multiply(multiply(X0,multiply(X0,X0)),multiply(X0,multiply(X0,X0))),identity)) = multiply(identity,multiply(identity,multiply(multiply(identity,multiply(identity,multiply(multiply(X0,identity),identity))),identity))),
inference(superposition,[status(thm)],[c_25028,c_7401]) ).
tcf(c_25135,plain,
! [X0: $i] : multiply(multiply(X0,multiply(X0,X0)),multiply(identity,multiply(multiply(X0,identity),identity))) = identity,
inference(light_normalisation,[status(thm)],[c_25117,c_53]) ).
tcf(c_25327,plain,
! [X0: $i] : multiply(identity,multiply(identity,multiply(multiply(identity,multiply(X0,X0)),multiply(identity,multiply(multiply(X0,identity),identity))))) = multiply(X0,multiply(multiply(X0,X0),identity)),
inference(superposition,[status(thm)],[c_25135,c_7401]) ).
tcf(c_27893,plain,
! [X0: $i,X1: $i] : multiply(multiply(multiply(X0,multiply(identity,multiply(identity,multiply(identity,X1)))),identity),identity) = multiply(multiply(multiply(X0,identity),identity),X1),
inference(superposition,[status(thm)],[c_17189,c_15298]) ).
tcf(c_28273,plain,
! [X0: $i,X1: $i] : multiply(identity,multiply(identity,multiply(identity,multiply(multiply(multiply(X0,identity),identity),X1)))) = multiply(X0,multiply(identity,multiply(identity,multiply(identity,X1)))),
inference(superposition,[status(thm)],[c_27893,c_134]) ).
tcf(c_28761,plain,
! [X0: $i,X1: $i] : multiply(X0,multiply(multiply(X0,X0),multiply(identity,X1))) = multiply(X0,multiply(multiply(X0,identity),multiply(X0,X1))),
inference(demodulation,[status(thm)],[c_19929,c_15299]) ).
tcf(c_28859,plain,
! [X0: $i,X1: $i] : multiply(multiply(X0,multiply(multiply(X0,X0),multiply(identity,X1))),multiply(X1,multiply(X1,X1))) = multiply(multiply(X0,multiply(multiply(X0,X0),identity)),identity),
inference(superposition,[status(thm)],[c_28761,c_16082]) ).
tcf(c_32433,plain,
! [X0: $i,X1: $i] : multiply(multiply(X0,X0),multiply(multiply(X0,multiply(multiply(X0,identity),identity)),multiply(identity,multiply(multiply(X1,identity),identity)))) = X1,
inference(demodulation,[status(thm)],[c_271,c_53,c_249,c_3823,c_20488,c_21278,c_23741,c_24253,c_25128,c_28273,c_28859]) ).
tcf(c_32531,plain,
! [X0: $i,X1: $i] : multiply(identity,multiply(identity,multiply(multiply(identity,multiply(multiply(X0,identity),identity)),multiply(identity,multiply(multiply(X1,identity),identity))))) = multiply(X0,X1),
inference(superposition,[status(thm)],[c_32433,c_7401]) ).
tcf(c_32636,plain,
! [X0: $i,X1: $i] : multiply(identity,multiply(identity,multiply(multiply(multiply(multiply(identity,X0),multiply(identity,X1)),identity),identity))) = multiply(X0,X1),
inference(demodulation,[status(thm)],[c_32531,c_15786]) ).
tcf(c_32771,plain,
! [X0: $i,X1: $i] : multiply(multiply(identity,X0),multiply(identity,X1)) = multiply(identity,multiply(X0,X1)),
inference(superposition,[status(thm)],[c_32636,c_134]) ).
tcf(c_33037,plain,
! [X0: $i,X1: $i] : multiply(identity,multiply(multiply(identity,multiply(identity,multiply(multiply(X0,identity),identity))),X1)) = multiply(X0,multiply(identity,X1)),
inference(superposition,[status(thm)],[c_134,c_32771]) ).
tcf(c_33477,plain,
! [X0: $i,X1: $i] : multiply(identity,multiply(identity,multiply(multiply(identity,multiply(multiply(X0,identity),identity)),X1))) = multiply(X0,multiply(identity,multiply(identity,X1))),
inference(superposition,[status(thm)],[c_32771,c_33037]) ).
tcf(c_33480,plain,
! [X0: $i,X1: $i] : multiply(identity,multiply(multiply(multiply(identity,multiply(identity,multiply(X0,identity))),X1),identity)) = multiply(X0,multiply(identity,multiply(X1,identity))),
inference(superposition,[status(thm)],[c_15778,c_33037]) ).
tcf(c_33565,plain,
! [X0: $i,X1: $i] : multiply(multiply(identity,multiply(identity,multiply(identity,multiply(X0,multiply(identity,multiply(multiply(X1,X1),multiply(multiply(X1,identity),identity))))))),X1) = multiply(identity,multiply(identity,multiply(identity,multiply(multiply(X0,identity),identity)))),
inference(superposition,[status(thm)],[c_33037,c_24510]) ).
tcf(c_33567,plain,
! [X0: $i,X1: $i] : multiply(multiply(identity,multiply(identity,multiply(identity,multiply(identity,multiply(identity,multiply(multiply(X0,identity),identity)))))),X1) = multiply(identity,multiply(identity,multiply(X0,multiply(identity,multiply(multiply(X1,identity),identity))))),
inference(superposition,[status(thm)],[c_33037,c_23845]) ).
tcf(c_33597,plain,
! [X0: $i,X1: $i] : multiply(identity,multiply(identity,multiply(X0,multiply(identity,multiply(multiply(X1,identity),identity))))) = multiply(multiply(identity,multiply(identity,X0)),X1),
inference(light_normalisation,[status(thm)],[c_33567,c_134]) ).
tcf(c_33603,plain,
! [X0: $i,X1: $i] : multiply(multiply(identity,multiply(identity,multiply(identity,multiply(X0,multiply(identity,multiply(multiply(X1,X1),multiply(multiply(X1,identity),identity))))))),X1) = X0,
inference(light_normalisation,[status(thm)],[c_33565,c_134]) ).
tcf(c_34984,plain,
! [X0: $i,X1: $i] : multiply(identity,multiply(multiply(multiply(multiply(identity,multiply(identity,X0)),X1),identity),identity)) = multiply(X0,multiply(identity,multiply(multiply(X1,identity),identity))),
inference(superposition,[status(thm)],[c_15778,c_33480]) ).
tcf(c_35217,plain,
! [X0: $i,X1: $i] : multiply(identity,multiply(identity,multiply(multiply(X0,multiply(identity,multiply(X1,identity))),identity))) = multiply(multiply(identity,multiply(identity,multiply(X0,identity))),X1),
inference(superposition,[status(thm)],[c_15501,c_33597]) ).
tcf(c_36329,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(X0,multiply(multiply(X0,multiply(multiply(X0,X0),X1)),multiply(multiply(X2,multiply(multiply(X2,X2),multiply(X1,identity))),multiply(multiply(multiply(X2,multiply(multiply(X2,X2),multiply(X1,identity))),multiply(X2,multiply(multiply(X2,X2),multiply(X1,identity)))),identity)))) = X2,
inference(demodulation,[status(thm)],[c_321,c_1337,c_15495,c_19953,c_24253]) ).
tcf(c_36516,plain,
! [X0: $i,X1: $i] : multiply(X0,multiply(multiply(X0,multiply(multiply(X0,X0),identity)),multiply(multiply(X1,multiply(multiply(X1,X1),identity)),multiply(multiply(multiply(X1,multiply(multiply(X1,X1),identity)),multiply(X1,multiply(multiply(X1,X1),identity))),identity)))) = X1,
inference(superposition,[status(thm)],[c_53,c_36329]) ).
tcf(c_36834,plain,
! [X0: $i] : multiply(multiply(identity,multiply(identity,multiply(identity,multiply(identity,multiply(multiply(identity,identity),multiply(multiply(X0,X0),multiply(multiply(X0,identity),identity))))))),X0) = multiply(identity,multiply(identity,multiply(identity,multiply(multiply(identity,identity),identity)))),
inference(superposition,[status(thm)],[c_16563,c_33603]) ).
tcf(c_37007,plain,
! [X0: $i] : multiply(multiply(identity,multiply(identity,multiply(multiply(identity,multiply(identity,multiply(identity,multiply(X0,identity)))),multiply(X0,X0)))),X0) = identity,
inference(light_normalisation,[status(thm)],[c_36834,c_53,c_24419]) ).
tcf(c_37722,plain,
! [X0: $i] : multiply(multiply(identity,multiply(X0,X0)),multiply(identity,multiply(multiply(X0,identity),identity))) = multiply(identity,multiply(multiply(multiply(X0,multiply(X0,X0)),identity),identity)),
inference(superposition,[status(thm)],[c_23913,c_34984]) ).
tcf(c_37833,plain,
! [X0: $i] : multiply(multiply(identity,multiply(X0,X0)),multiply(identity,multiply(multiply(X0,identity),identity))) = multiply(identity,multiply(multiply(X0,multiply(multiply(X0,X0),identity)),identity)),
inference(light_normalisation,[status(thm)],[c_37722,c_24253]) ).
tcf(c_38018,plain,
! [X0: $i,X1: $i] : multiply(identity,multiply(identity,multiply(multiply(identity,multiply(X0,multiply(X1,identity))),identity))) = multiply(multiply(identity,multiply(identity,multiply(multiply(identity,X0),identity))),X1),
inference(superposition,[status(thm)],[c_32771,c_35217]) ).
tcf(c_38129,plain,
! [X0: $i,X1: $i] : multiply(identity,multiply(identity,multiply(multiply(identity,multiply(X0,multiply(X1,identity))),identity))) = multiply(multiply(identity,multiply(identity,multiply(identity,multiply(X0,identity)))),X1),
inference(light_normalisation,[status(thm)],[c_38018,c_249]) ).
tcf(c_38775,plain,
! [X0: $i,X1: $i] : multiply(X0,multiply(multiply(multiply(X0,multiply(X0,X0)),multiply(identity,multiply(X1,identity))),identity)) = X1,
inference(demodulation,[status(thm)],[c_36516,c_53,c_249,c_15313,c_16247,c_21298,c_24300,c_25128,c_38129]) ).
tcf(c_38870,plain,
! [X0: $i,X1: $i] : multiply(X0,multiply(multiply(multiply(X0,multiply(X0,X0)),X1),identity)) = multiply(multiply(identity,multiply(identity,identity)),multiply(identity,multiply(X1,identity))),
inference(superposition,[status(thm)],[c_38775,c_38775]) ).
tcf(c_38934,plain,
! [X0: $i,X1: $i] : multiply(X0,multiply(multiply(multiply(X0,multiply(X0,X0)),X1),identity)) = multiply(identity,multiply(identity,multiply(X1,identity))),
inference(light_normalisation,[status(thm)],[c_38870,c_53]) ).
tcf(c_39939,plain,
! [X0: $i] : multiply(multiply(identity,multiply(identity,multiply(identity,multiply(X0,identity)))),multiply(X0,X0)) = multiply(X0,multiply(multiply(X0,X0),identity)),
inference(light_normalisation,[status(thm)],[c_25327,c_24363,c_24419,c_37833]) ).
tcf(c_39940,plain,
! [X0: $i] : multiply(multiply(identity,multiply(identity,multiply(X0,multiply(multiply(X0,X0),identity)))),X0) = identity,
inference(demodulation,[status(thm)],[c_37007,c_39939]) ).
tcf(c_40007,plain,
! [X0: $i] : multiply(multiply(identity,identity),multiply(multiply(identity,multiply(X0,multiply(multiply(X0,X0),identity))),identity)) = multiply(identity,multiply(identity,multiply(multiply(X0,multiply(multiply(X0,X0),identity)),identity))),
inference(superposition,[status(thm)],[c_39939,c_8314]) ).
tcf(c_40027,plain,
! [X0: $i] : multiply(identity,multiply(multiply(identity,multiply(X0,multiply(multiply(X0,X0),identity))),identity)) = multiply(identity,multiply(identity,multiply(multiply(X0,X0),multiply(multiply(X0,identity),identity)))),
inference(light_normalisation,[status(thm)],[c_40007,c_53,c_24363]) ).
tcf(c_40278,plain,
! [X0: $i] : multiply(multiply(identity,multiply(identity,multiply(multiply(multiply(identity,X0),multiply(multiply(identity,multiply(X0,identity)),multiply(identity,multiply(X0,identity)))),identity))),multiply(identity,multiply(X0,identity))) = identity,
inference(superposition,[status(thm)],[c_15494,c_39940]) ).
tcf(c_40455,plain,
! [X0: $i] : multiply(multiply(X0,multiply(multiply(X0,X0),identity)),multiply(identity,multiply(X0,identity))) = identity,
inference(light_normalisation,[status(thm)],[c_40278,c_15816,c_24366,c_24419,c_39939,c_40027]) ).
tcf(c_40602,plain,
! [X0: $i] : multiply(multiply(multiply(X0,multiply(X0,X0)),multiply(identity,X0)),identity) = identity,
inference(demodulation,[status(thm)],[c_40455,c_21161]) ).
tcf(c_40714,plain,
! [X0: $i] : multiply(multiply(X0,multiply(X0,X0)),multiply(identity,X0)) = multiply(identity,multiply(identity,multiply(identity,multiply(identity,identity)))),
inference(superposition,[status(thm)],[c_40602,c_134]) ).
tcf(c_40740,plain,
! [X0: $i] : multiply(identity,multiply(identity,multiply(multiply(identity,X0),identity))) = multiply(X0,identity),
inference(superposition,[status(thm)],[c_40602,c_38934]) ).
tcf(c_40742,plain,
! [X0: $i] : multiply(identity,multiply(identity,multiply(identity,multiply(X0,identity)))) = multiply(X0,identity),
inference(light_normalisation,[status(thm)],[c_40740,c_249]) ).
tcf(c_40745,plain,
! [X0: $i] : multiply(multiply(X0,multiply(X0,X0)),multiply(identity,X0)) = identity,
inference(light_normalisation,[status(thm)],[c_40714,c_53]) ).
tcf(c_40817,plain,
! [X0: $i] : multiply(multiply(X0,identity),multiply(X0,X0)) = multiply(X0,multiply(multiply(X0,X0),identity)),
inference(demodulation,[status(thm)],[c_39939,c_40742]) ).
tcf(c_40827,plain,
! [X0: $i,X1: $i] : multiply(multiply(X0,multiply(X1,identity)),identity) = multiply(multiply(X0,identity),X1),
inference(demodulation,[status(thm)],[c_15298,c_40742]) ).
tcf(c_40830,plain,
! [X0: $i] : multiply(multiply(X0,identity),identity) = X0,
inference(demodulation,[status(thm)],[c_134,c_40742]) ).
tcf(c_40834,plain,
! [X0: $i,X1: $i] : multiply(identity,multiply(identity,multiply(multiply(identity,X0),X1))) = multiply(X0,multiply(identity,multiply(identity,X1))),
inference(demodulation,[status(thm)],[c_33477,c_40830]) ).
tcf(c_40836,plain,
! [X0: $i,X1: $i] : multiply(identity,multiply(multiply(identity,multiply(identity,X0)),X1)) = multiply(X0,multiply(identity,X1)),
inference(demodulation,[status(thm)],[c_33037,c_40830]) ).
tcf(c_40849,plain,
! [X0: $i,X1: $i] : multiply(multiply(identity,multiply(X0,multiply(X1,multiply(X1,X1)))),X1) = multiply(identity,X0),
inference(demodulation,[status(thm)],[c_4233,c_40830]) ).
tcf(c_40866,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(X0,multiply(multiply(X0,X0),multiply(multiply(X0,X1),X2))) = multiply(X1,multiply(identity,multiply(identity,X2))),
inference(demodulation,[status(thm)],[c_7401,c_40834]) ).
tcf(c_40872,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,identity),X1)),
inference(demodulation,[status(thm)],[c_564,c_40827]) ).
tcf(c_41217,plain,
! [X0: $i] : multiply(multiply(X0,multiply(multiply(X0,X0),identity)),identity) = multiply(X0,multiply(X0,X0)),
inference(superposition,[status(thm)],[c_24253,c_40830]) ).
tcf(c_41263,plain,
! [X0: $i] : multiply(identity,multiply(identity,multiply(multiply(multiply(identity,identity),identity),identity))) = multiply(multiply(X0,X0),multiply(multiply(X0,X0),identity)),
inference(superposition,[status(thm)],[c_40830,c_8314]) ).
tcf(c_41264,plain,
! [X0: $i] : multiply(multiply(X0,X0),multiply(multiply(X0,identity),identity)) = multiply(multiply(X0,identity),multiply(X0,X0)),
inference(superposition,[status(thm)],[c_40830,c_18784]) ).
tcf(c_41266,plain,
! [X0: $i] : multiply(X0,multiply(X0,multiply(X0,X0))) = multiply(identity,multiply(identity,multiply(identity,identity))),
inference(superposition,[status(thm)],[c_40830,c_38934]) ).
tcf(c_41270,plain,
! [X0: $i] : multiply(X0,multiply(X0,multiply(X0,X0))) = identity,
inference(light_normalisation,[status(thm)],[c_41266,c_53]) ).
tcf(c_41273,plain,
! [X0: $i] : multiply(X0,multiply(multiply(X0,X0),identity)) = multiply(multiply(X0,X0),X0),
inference(light_normalisation,[status(thm)],[c_41264,c_40817,c_40830]) ).
tcf(c_41278,plain,
! [X0: $i] : multiply(multiply(X0,X0),multiply(multiply(X0,X0),identity)) = identity,
inference(light_normalisation,[status(thm)],[c_41263,c_53]) ).
tcf(c_41293,plain,
! [X0: $i] : multiply(multiply(X0,multiply(X0,X0)),identity) = multiply(multiply(X0,X0),X0),
inference(demodulation,[status(thm)],[c_24253,c_41273]) ).
tcf(c_41435,plain,
! [X0: $i] : multiply(multiply(X0,X0),multiply(multiply(X0,multiply(multiply(X0,X0),identity)),identity)) = multiply(multiply(X0,identity),identity),
inference(superposition,[status(thm)],[c_41278,c_3823]) ).
tcf(c_41448,plain,
! [X0: $i] : multiply(multiply(X0,X0),multiply(X0,multiply(X0,X0))) = X0,
inference(light_normalisation,[status(thm)],[c_41435,c_40830,c_41217]) ).
tcf(c_41498,plain,
! [X0: $i] : multiply(identity,multiply(identity,multiply(identity,X0))) = X0,
inference(superposition,[status(thm)],[c_40830,c_40742]) ).
tcf(c_41656,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(X0,multiply(multiply(X0,multiply(multiply(X0,X0),multiply(X1,X1))),multiply(multiply(multiply(X2,X2),multiply(multiply(X2,identity),multiply(X1,X1))),multiply(multiply(multiply(X2,X2),multiply(multiply(X2,identity),multiply(X1,X1))),multiply(multiply(X2,X2),multiply(multiply(X2,identity),multiply(X1,X1))))))) = X2,
inference(demodulation,[status(thm)],[c_323,c_1739,c_40827]) ).
tcf(c_41701,plain,
! [X0: $i] : multiply(X0,multiply(multiply(X0,multiply(multiply(X0,X0),multiply(multiply(identity,identity),multiply(identity,identity)))),multiply(identity,multiply(identity,identity)))) = identity,
inference(superposition,[status(thm)],[c_41270,c_41656]) ).
tcf(c_41738,plain,
! [X0: $i] : multiply(X0,multiply(multiply(multiply(X0,X0),X0),identity)) = identity,
inference(light_normalisation,[status(thm)],[c_41701,c_53,c_41273]) ).
tcf(c_41880,plain,
! [X0: $i] : multiply(multiply(multiply(X0,X0),multiply(multiply(X0,identity),identity)),identity) = multiply(multiply(multiply(X0,identity),identity),multiply(multiply(X0,X0),identity)),
inference(superposition,[status(thm)],[c_18784,c_40827]) ).
tcf(c_41883,plain,
! [X0: $i] : multiply(multiply(X0,identity),multiply(multiply(X0,X0),X0)) = multiply(identity,identity),
inference(superposition,[status(thm)],[c_41738,c_40827]) ).
tcf(c_41928,plain,
! [X0: $i] : multiply(multiply(X0,identity),multiply(multiply(X0,X0),X0)) = identity,
inference(light_normalisation,[status(thm)],[c_41883,c_53]) ).
tcf(c_41936,plain,
! [X0: $i] : multiply(multiply(multiply(X0,X0),X0),identity) = multiply(multiply(X0,X0),X0),
inference(light_normalisation,[status(thm)],[c_41880,c_40830,c_41273]) ).
tcf(c_42289,plain,
! [X0: $i] : multiply(multiply(multiply(X0,X0),X0),identity) = multiply(X0,multiply(X0,X0)),
inference(superposition,[status(thm)],[c_41293,c_40830]) ).
tcf(c_42330,plain,
! [X0: $i] : multiply(multiply(X0,X0),X0) = multiply(X0,multiply(X0,X0)),
inference(light_normalisation,[status(thm)],[c_41936,c_42289]) ).
tcf(c_42334,plain,
! [X0: $i] : multiply(multiply(X0,identity),multiply(X0,multiply(X0,X0))) = identity,
inference(demodulation,[status(thm)],[c_41928,c_42330]) ).
tcf(c_43168,plain,
! [X0: $i,X1: $i] : multiply(multiply(X0,multiply(identity,multiply(X1,multiply(X1,X1)))),X1) = multiply(identity,multiply(identity,multiply(identity,X0))),
inference(superposition,[status(thm)],[c_40836,c_40849]) ).
tcf(c_43182,plain,
! [X0: $i] : multiply(multiply(identity,identity),X0) = multiply(identity,multiply(X0,identity)),
inference(superposition,[status(thm)],[c_42334,c_40849]) ).
tcf(c_43227,plain,
! [X0: $i] : multiply(identity,multiply(X0,identity)) = multiply(identity,X0),
inference(light_normalisation,[status(thm)],[c_43182,c_53]) ).
tcf(c_43234,plain,
! [X0: $i,X1: $i] : multiply(multiply(X0,multiply(identity,multiply(X1,multiply(X1,X1)))),X1) = X0,
inference(light_normalisation,[status(thm)],[c_43168,c_41498]) ).
tcf(c_43325,plain,
! [X0: $i] : multiply(identity,multiply(identity,multiply(identity,X0))) = multiply(X0,identity),
inference(superposition,[status(thm)],[c_43227,c_41498]) ).
tcf(c_43343,plain,
! [X0: $i] : multiply(X0,identity) = X0,
inference(light_normalisation,[status(thm)],[c_43325,c_41498]) ).
tcf(c_43364,plain,
! [X0: $i,X1: $i] : multiply(multiply(X0,X0),multiply(multiply(multiply(X0,X0),multiply(X0,X0)),X1)) = multiply(X0,multiply(X0,X1)),
inference(demodulation,[status(thm)],[c_15299,c_43343]) ).
tcf(c_43367,plain,
! [X0: $i] : multiply(multiply(X0,X0),multiply(X0,X0)) = identity,
inference(demodulation,[status(thm)],[c_41278,c_43343]) ).
tcf(c_43429,plain,
! [X0: $i] : multiply(multiply(X0,X0),identity) = multiply(identity,multiply(X0,X0)),
inference(superposition,[status(thm)],[c_43367,c_42330]) ).
tcf(c_43486,plain,
! [X0: $i] : multiply(identity,multiply(X0,X0)) = multiply(X0,X0),
inference(demodulation,[status(thm)],[c_43429,c_43343]) ).
tcf(c_43496,plain,
! [X0: $i,X1: $i] : multiply(multiply(X0,X0),multiply(identity,X1)) = multiply(identity,multiply(multiply(X0,X0),X1)),
inference(superposition,[status(thm)],[c_43486,c_32771]) ).
tcf(c_43570,plain,
! [X0: $i] : multiply(multiply(X0,multiply(X0,X0)),multiply(multiply(X0,multiply(X0,X0)),multiply(X0,multiply(X0,X0)))) = multiply(identity,X0),
inference(superposition,[status(thm)],[c_40745,c_43234]) ).
tcf(c_43597,plain,
! [X0: $i,X1: $i] : multiply(X0,multiply(multiply(X0,multiply(X0,X0)),multiply(identity,X1))) = X1,
inference(demodulation,[status(thm)],[c_324,c_1785,c_42330,c_43343,c_43570]) ).
tcf(c_43605,plain,
! [X0: $i,X1: $i] : multiply(multiply(X0,X0),multiply(multiply(multiply(X0,X0),identity),multiply(identity,X1))) = X1,
inference(superposition,[status(thm)],[c_43367,c_43597]) ).
tcf(c_43773,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),X3)),multiply(multiply(multiply(X1,X1),multiply(X1,X3)),multiply(multiply(multiply(X1,X1),multiply(X1,X3)),multiply(multiply(X1,X1),multiply(X1,X3))))),multiply(multiply(multiply(X2,multiply(multiply(X2,X2),X3)),multiply(multiply(multiply(X1,X1),multiply(X1,X3)),multiply(multiply(multiply(X1,X1),multiply(X1,X3)),multiply(multiply(X1,X1),multiply(X1,X3))))),multiply(multiply(X2,multiply(multiply(X2,X2),X3)),multiply(multiply(multiply(X1,X1),multiply(X1,X3)),multiply(multiply(multiply(X1,X1),multiply(X1,X3)),multiply(multiply(X1,X1),multiply(X1,X3))))))))) = X2,
inference(demodulation,[status(thm)],[c_329,c_565,c_43343]) ).
tcf(c_45584,plain,
! [X0: $i,X1: $i] : multiply(identity,multiply(multiply(X0,X0),multiply(multiply(X0,X0),X1))) = X1,
inference(demodulation,[status(thm)],[c_43605,c_43343,c_43496]) ).
tcf(c_45596,plain,
! [X0: $i] : multiply(identity,multiply(multiply(X0,X0),multiply(X0,multiply(X0,X0)))) = X0,
inference(superposition,[status(thm)],[c_42330,c_45584]) ).
tcf(c_45623,plain,
! [X0: $i,X1: $i] : multiply(multiply(X0,X0),multiply(multiply(X0,X0),X1)) = multiply(identity,multiply(identity,X1)),
inference(superposition,[status(thm)],[c_45584,c_41498]) ).
tcf(c_45638,plain,
! [X0: $i] : multiply(identity,X0) = X0,
inference(light_normalisation,[status(thm)],[c_45596,c_41448]) ).
tcf(c_45740,plain,
! [X0: $i,X1: $i] : multiply(X0,multiply(multiply(X0,X0),multiply(X0,X1))) = X1,
inference(demodulation,[status(thm)],[c_333,c_6339,c_40872,c_42330,c_43343,c_43364]) ).
tcf(c_45754,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),X3)),multiply(multiply(multiply(X1,X1),multiply(X1,X3)),multiply(multiply(multiply(X1,X1),multiply(X1,X3)),multiply(multiply(X1,X1),multiply(X1,X3))))),multiply(multiply(multiply(X2,multiply(multiply(X2,X2),X3)),multiply(multiply(multiply(X1,X1),multiply(X1,X3)),multiply(multiply(multiply(X1,X1),multiply(X1,X3)),multiply(multiply(X1,X1),multiply(X1,X3))))),multiply(multiply(X2,multiply(multiply(X2,X2),X3)),multiply(multiply(multiply(X1,X1),multiply(X1,X3)),multiply(multiply(multiply(X1,X1),multiply(X1,X3)),multiply(multiply(X1,X1),multiply(X1,X3)))))))) = multiply(X0,multiply(multiply(X0,X0),X2)),
inference(superposition,[status(thm)],[c_43773,c_45740]) ).
tcf(c_45769,plain,
! [X0: $i,X1: $i] : multiply(X0,multiply(X0,multiply(multiply(X0,X0),X1))) = X1,
inference(demodulation,[status(thm)],[c_43773,c_45754]) ).
tcf(c_45824,plain,
! [X0: $i,X1: $i] : multiply(multiply(X0,X0),multiply(multiply(X0,X0),X1)) = X1,
inference(demodulation,[status(thm)],[c_45623,c_45638]) ).
tcf(c_45838,plain,
! [X0: $i,X1: $i] : multiply(multiply(X0,X0),X1) = multiply(X0,multiply(X0,X1)),
inference(superposition,[status(thm)],[c_45824,c_45769]) ).
tcf(c_45848,plain,
! [X0: $i,X1: $i] : multiply(X0,multiply(X0,multiply(X0,multiply(X0,X1)))) = X1,
inference(demodulation,[status(thm)],[c_45769,c_45838]) ).
tcf(c_47903,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(X0,multiply(X0,multiply(X0,multiply(multiply(X0,X1),X2)))) = multiply(X1,X2),
inference(demodulation,[status(thm)],[c_40866,c_45638,c_45838]) ).
tcf(c_47955,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(multiply(X0,X1),X2) = multiply(X0,multiply(X1,X2)),
inference(superposition,[status(thm)],[c_47903,c_45848]) ).
tcf(c_47978,plain,
$false,
inference(backward_subsumption_resolution,[status(thm)],[c_54,c_47955]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP122-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.10/0.35 % Computer : n013.cluster.edu
% 0.10/0.35 % Model : x86_64 x86_64
% 0.10/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.35 % Memory : 8046.5625MB
% 0.10/0.35 % OS : Linux 6.8.0-71-generic
% 0.10/0.35 % CPULimit : 300
% 0.10/0.35 % WCLimit : 300
% 0.10/0.35 % DateTime : Wed Sep 23 13:34:36 UTC 2026
% 0.10/0.35 % CPUTime :
% 0.10/0.35 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.14/0.39 Running UEQ theorem proving
% 0.14/0.39 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.14/0.40
% 0.14/0.40 % ======== iProver multi-core TPTP/SMT =========
% 0.14/0.40
% 0.14/0.40 % Detected problem language: tptp
% 0.14/0.41 % Proving...
% 55.27/9.28 WARNING - Clausifier option not provided in the heuristic config "heur/vip2_118404", setting default options.
% 55.27/9.28 % SZS status Started for theBenchmark.p
% 55.27/9.28 % SZS status Unsatisfiable for theBenchmark.p
% 55.27/9.28
% 55.27/9.28 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 55.27/9.28
% 55.27/9.28 % ------ iProver source info
% 55.27/9.28
% 55.27/9.28 % git: date: 2026-07-19 20:42:38 +0200
% 55.27/9.28 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 55.27/9.28 % git: non_committed_changes: false
% 55.27/9.28
% 55.27/9.28 % ------ Parsing...% successful
% 55.27/9.28
% 55.27/9.28
% 55.27/9.28 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 55.27/9.28
% 55.27/9.28 % ------ Preprocessing... sup_sim: 0 sf_s rm: 0 0s sf_e pe_s pe_e %
% 55.27/9.28
% 55.27/9.28 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 55.27/9.28
% 55.27/9.28 % ------ Preprocessing... sf_s rm: 0 0s sf_e
% 55.27/9.28 % ------ Proving...
% 55.27/9.28 % ------ Problem Properties
% 55.27/9.28
% 55.27/9.28 %
% 55.27/9.28 % clauses 3
% 55.27/9.28 % conjectures 1
% 55.27/9.28 % EPR 0
% 55.27/9.28 % Horn 3
% 55.27/9.28 % unary 3
% 55.27/9.28 % binary 0
% 55.27/9.28 % lits 3
% 55.27/9.28 % lits eq 3
% 55.27/9.28 % fd_pure 0
% 55.27/9.28 % fd_pseudo 0
% 55.27/9.28 % fd_cond 0
% 55.27/9.28 % fd_pseudo_cond 0
% 55.27/9.28 % AC symbols 0
% 55.27/9.28
% 55.27/9.28 % ------ Input Options Time Limit: Unbounded
% 55.27/9.28
% 55.27/9.28
% 55.27/9.28 % ------
% 55.27/9.28 % Current options:
% 55.27/9.28 % ------
% 55.27/9.28
% 55.27/9.28
% 55.27/9.28 %
% 55.27/9.28
% 55.27/9.28 % ------ Proving...
% 55.27/9.28 %
% 55.27/9.28
% 55.27/9.28 % SZS status Unsatisfiable for theBenchmark.p
% 55.27/9.28
% 55.27/9.28 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 55.27/9.29
% 55.27/9.29
%------------------------------------------------------------------------------