%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : BOO031-1 : TPTP v9.3.1. Released v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% Computer : n017.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:00:17 PM UTC 2026
% Result : Unsatisfiable 210.30s 29.42s
% Output : CNFRefutation 210.30s
% Verified :
% SZS Type : Refutation
% Derivation depth : 34
% Number of leaves : 17
% Syntax : Number of formulae : 393 ( 393 unt; 5 def)
% Number of atoms : 1305 ( 392 equ)
% Maximal formula atoms : 1 ( 3 avg)
% Number of connectives : 3 ( 3 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 2 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 9 ( 7 usr; 8 prp; 0-2 aty)
% Number of functors : 8 ( 8 usr; 5 con; 0-2 aty)
% Number of variables : 469 ( 0 sgn 469 !; 0 ?; 442 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X2,X0,X1] : add(multiply(X0,X1),add(multiply(X1,X2),multiply(X2,X0))) = multiply(add(X0,X1),multiply(add(X1,X2),add(X2,X0))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',distributivity) ).
fof(f2,axiom,
! [X2,X0,X1] : add(X0,multiply(X1,multiply(X0,X2))) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',l1) ).
fof(f3,axiom,
! [X2,X0,X1] : add(add(multiply(X0,X1),multiply(X1,X2)),X1) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',l3) ).
fof(f4,axiom,
! [X0,X1] : multiply(add(X0,inverse(X0)),X1) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',property3) ).
fof(f5,axiom,
! [X2,X0,X1] : multiply(X0,add(X1,add(X0,X2))) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',l2) ).
fof(f6,axiom,
! [X2,X0,X1] : multiply(multiply(add(X0,X1),add(X1,X2)),X1) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',l4) ).
fof(f7,axiom,
! [X0,X1] : add(multiply(X0,inverse(X0)),X1) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',property3_dual) ).
fof(f8,axiom,
! [X0] : add(X0,inverse(X0)) = n1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',additive_inverse) ).
fof(f9,axiom,
! [X0] : multiply(X0,inverse(X0)) = n0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',multiplicative_inverse) ).
fof(f10,axiom,
! [X2,X0,X1] : add(add(X0,X1),X2) = add(X0,add(X1,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',associativity_of_add) ).
fof(f11,axiom,
! [X2,X0,X1] : multiply(multiply(X0,X1),X2) = multiply(X0,multiply(X1,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',associativity_of_multiply) ).
fof(f12,negated_conjecture,
multiply(a,add(b,c)) != add(multiply(b,a),multiply(c,a)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_multiply_add_property) ).
tcf(c_61,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(add(X0,X1),multiply(add(X1,X2),add(X2,X0))) = add(multiply(X0,X1),add(multiply(X1,X2),multiply(X2,X0))),
inference(cnf_transformation,[],[f1]) ).
tcf(c_62,plain,
! [X0: $i,X1: $i,X2: $i] : add(X0,multiply(X1,multiply(X0,X2))) = X0,
inference(cnf_transformation,[],[f2]) ).
tcf(c_63,plain,
! [X0: $i,X1: $i,X2: $i] : add(add(multiply(X0,X1),multiply(X1,X2)),X1) = X1,
inference(cnf_transformation,[],[f3]) ).
tcf(c_64,plain,
! [X0: $i,X1: $i] : multiply(add(X0,inverse(X0)),X1) = X1,
inference(cnf_transformation,[],[f4]) ).
tcf(c_65,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(X0,add(X1,add(X0,X2))) = X0,
inference(cnf_transformation,[],[f5]) ).
tcf(c_66,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(multiply(add(X0,X1),add(X1,X2)),X1) = X1,
inference(cnf_transformation,[],[f6]) ).
tcf(c_67,plain,
! [X0: $i,X1: $i] : add(multiply(X0,inverse(X0)),X1) = X1,
inference(cnf_transformation,[],[f7]) ).
tcf(c_68,plain,
! [X0: $i] : add(X0,inverse(X0)) = n1,
inference(cnf_transformation,[],[f8]) ).
tcf(c_69,plain,
! [X0: $i] : multiply(X0,inverse(X0)) = n0,
inference(cnf_transformation,[],[f9]) ).
tcf(c_70,plain,
! [X0: $i,X1: $i,X2: $i] : add(add(X0,X1),X2) = add(X0,add(X1,X2)),
inference(cnf_transformation,[],[f10]) ).
tcf(c_71,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(multiply(X0,X1),X2) = multiply(X0,multiply(X1,X2)),
inference(cnf_transformation,[],[f11]) ).
tcf(c_72,negated_conjecture,
add(multiply(b,a),multiply(c,a)) != multiply(a,add(b,c)),
inference(cnf_transformation,[],[f12]) ).
tcf(c_112,definition,
iPr_def_10 = multiply(b,a),
introduced(definition,[new_symbols(definition,[iPr_def_10])],[]) ).
tcf(c_113,definition,
iPr_def_11 = multiply(c,a),
introduced(definition,[new_symbols(definition,[iPr_def_11])],[]) ).
tcf(c_114,definition,
iPr_def_12 = add(iPr_def_10,iPr_def_11),
introduced(definition,[new_symbols(definition,[iPr_def_12])],[]) ).
tcf(c_115,definition,
iPr_def_13 = add(b,c),
introduced(definition,[new_symbols(definition,[iPr_def_13])],[]) ).
tcf(c_116,definition,
iPr_def_14 = multiply(a,iPr_def_13),
introduced(definition,[new_symbols(definition,[iPr_def_14])],[]) ).
tcf(c_117,negated_conjecture,
iPr_def_12 != iPr_def_14,
inference(demodulation,[status(thm)],[c_72,c_115,c_116,c_113,c_112,c_114]) ).
tcf(c_118,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(multiply(X0,X1),X2) = multiply(X0,multiply(X1,X2)),
inference(demodulation,[status(thm)],[c_71]) ).
tcf(c_119,plain,
! [X0: $i,X1: $i,X2: $i] : add(add(X0,X1),X2) = add(X0,add(X1,X2)),
inference(demodulation,[status(thm)],[c_70]) ).
tcf(c_120,plain,
! [X0: $i] : multiply(X0,inverse(X0)) = n0,
inference(demodulation,[status(thm)],[c_69]) ).
tcf(c_121,plain,
! [X0: $i] : add(X0,inverse(X0)) = n1,
inference(demodulation,[status(thm)],[c_68]) ).
tcf(c_122,plain,
! [X0: $i,X1: $i] : add(multiply(X0,inverse(X0)),X1) = X1,
inference(demodulation,[status(thm)],[c_67]) ).
tcf(c_123,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(multiply(add(X0,X1),add(X1,X2)),X1) = X1,
inference(demodulation,[status(thm)],[c_66]) ).
tcf(c_124,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(X0,add(X1,add(X0,X2))) = X0,
inference(demodulation,[status(thm)],[c_65]) ).
tcf(c_125,plain,
! [X0: $i,X1: $i] : multiply(add(X0,inverse(X0)),X1) = X1,
inference(demodulation,[status(thm)],[c_64]) ).
tcf(c_126,plain,
! [X0: $i,X1: $i,X2: $i] : add(add(multiply(X0,X1),multiply(X1,X2)),X1) = X1,
inference(demodulation,[status(thm)],[c_63]) ).
tcf(c_127,plain,
! [X0: $i,X1: $i,X2: $i] : add(X0,multiply(X1,multiply(X0,X2))) = X0,
inference(demodulation,[status(thm)],[c_62]) ).
tcf(c_128,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(add(X0,X1),multiply(add(X1,X2),add(X2,X0))) = add(multiply(X0,X1),add(multiply(X1,X2),multiply(X2,X0))),
inference(demodulation,[status(thm)],[c_61]) ).
tcf(c_190,plain,
! [X0: $i,X1: $i,X2: $i] : add(multiply(X0,X1),add(multiply(X1,X2),X1)) = X1,
inference(demodulation,[status(thm)],[c_126,c_119]) ).
tcf(c_191,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(add(X0,X1),multiply(add(X1,X2),X1)) = X1,
inference(demodulation,[status(thm)],[c_123,c_118]) ).
tcf(c_193,plain,
! [X0: $i] : multiply(b,multiply(a,X0)) = multiply(iPr_def_10,X0),
inference(superposition,[status(thm)],[c_112,c_118]) ).
tcf(c_194,plain,
! [X0: $i] : multiply(c,multiply(a,X0)) = multiply(iPr_def_11,X0),
inference(superposition,[status(thm)],[c_113,c_118]) ).
tcf(c_195,plain,
! [X0: $i] : multiply(a,multiply(iPr_def_13,X0)) = multiply(iPr_def_14,X0),
inference(superposition,[status(thm)],[c_116,c_118]) ).
tcf(c_198,plain,
! [X0: $i] : add(b,add(c,X0)) = add(iPr_def_13,X0),
inference(superposition,[status(thm)],[c_115,c_119]) ).
tcf(c_199,plain,
! [X0: $i] : add(iPr_def_10,add(iPr_def_11,X0)) = add(iPr_def_12,X0),
inference(superposition,[status(thm)],[c_114,c_119]) ).
tcf(c_203,plain,
! [X0: $i,X1: $i] : multiply(X0,multiply(inverse(X0),X1)) = multiply(n0,X1),
inference(superposition,[status(thm)],[c_120,c_118]) ).
tcf(c_204,plain,
! [X0: $i,X1: $i] : multiply(X0,multiply(X1,inverse(multiply(X0,X1)))) = n0,
inference(superposition,[status(thm)],[c_120,c_118]) ).
tcf(c_205,plain,
! [X0: $i,X1: $i] : multiply(X0,inverse(X0)) = multiply(X1,inverse(X1)),
inference(superposition,[status(thm)],[c_120,c_120]) ).
tcf(c_208,plain,
! [X0: $i,X1: $i] : add(X0,add(inverse(X0),X1)) = add(n1,X1),
inference(superposition,[status(thm)],[c_121,c_119]) ).
tcf(c_210,plain,
! [X0: $i,X1: $i] : add(X0,inverse(X0)) = add(X1,inverse(X1)),
inference(superposition,[status(thm)],[c_121,c_121]) ).
tcf(c_212,plain,
! [X0: $i] : add(n0,X0) = X0,
inference(superposition,[status(thm)],[c_120,c_122]) ).
tcf(c_213,plain,
! [X0: $i,X1: $i,X2: $i] : add(multiply(X0,multiply(X1,inverse(multiply(X0,X1)))),X2) = X2,
inference(superposition,[status(thm)],[c_118,c_122]) ).
tcf(c_215,plain,
! [X0: $i] : inverse(multiply(X0,inverse(X0))) = n1,
inference(superposition,[status(thm)],[c_122,c_121]) ).
tcf(c_217,plain,
! [X0: $i,X1: $i] : multiply(X0,add(X0,X1)) = X0,
inference(superposition,[status(thm)],[c_122,c_124]) ).
tcf(c_218,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : multiply(X0,add(X1,add(X2,add(X0,X3)))) = X0,
inference(superposition,[status(thm)],[c_119,c_124]) ).
tcf(c_219,plain,
! [X0: $i,X1: $i] : multiply(X0,add(X1,n1)) = X0,
inference(superposition,[status(thm)],[c_121,c_124]) ).
tcf(c_221,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : multiply(add(X0,X1),add(X2,add(X0,add(X1,X3)))) = add(X0,X1),
inference(superposition,[status(thm)],[c_119,c_124]) ).
tcf(c_222,plain,
! [X0: $i] : multiply(b,add(X0,iPr_def_13)) = b,
inference(superposition,[status(thm)],[c_115,c_124]) ).
tcf(c_223,plain,
! [X0: $i] : multiply(iPr_def_10,add(X0,iPr_def_12)) = iPr_def_10,
inference(superposition,[status(thm)],[c_114,c_124]) ).
tcf(c_224,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : multiply(X0,multiply(add(X1,add(X0,X2)),X3)) = multiply(X0,X3),
inference(superposition,[status(thm)],[c_124,c_118]) ).
tcf(c_225,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : multiply(X0,multiply(X1,add(X2,add(multiply(X0,X1),X3)))) = multiply(X0,X1),
inference(superposition,[status(thm)],[c_124,c_118]) ).
tcf(c_228,plain,
! [X0: $i] : multiply(n1,X0) = X0,
inference(superposition,[status(thm)],[c_121,c_125]) ).
tcf(c_237,plain,
! [X0: $i,X1: $i] : add(X0,multiply(X0,X1)) = X0,
inference(superposition,[status(thm)],[c_125,c_127]) ).
tcf(c_238,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : add(X0,multiply(X1,multiply(X2,multiply(X0,X3)))) = X0,
inference(superposition,[status(thm)],[c_118,c_127]) ).
tcf(c_240,plain,
! [X0: $i,X1: $i] : add(X0,multiply(X1,X0)) = X0,
inference(superposition,[status(thm)],[c_124,c_127]) ).
tcf(c_241,plain,
! [X0: $i,X1: $i] : add(X0,multiply(X1,n0)) = X0,
inference(superposition,[status(thm)],[c_120,c_127]) ).
tcf(c_242,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : add(multiply(X0,X1),multiply(X2,multiply(X0,multiply(X1,X3)))) = multiply(X0,X1),
inference(superposition,[status(thm)],[c_118,c_127]) ).
tcf(c_243,plain,
! [X0: $i] : add(b,multiply(X0,iPr_def_10)) = b,
inference(superposition,[status(thm)],[c_112,c_127]) ).
tcf(c_246,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : add(X0,add(multiply(X1,multiply(X0,X2)),X3)) = add(X0,X3),
inference(superposition,[status(thm)],[c_127,c_119]) ).
tcf(c_247,plain,
! [X0: $i,X1: $i] : multiply(X0,add(X1,X0)) = X0,
inference(superposition,[status(thm)],[c_127,c_124]) ).
tcf(c_249,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : add(X0,add(X1,multiply(X2,multiply(add(X0,X1),X3)))) = add(X0,X1),
inference(superposition,[status(thm)],[c_127,c_119]) ).
tcf(c_254,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : multiply(add(multiply(X0,X1),X2),multiply(add(X2,X3),add(X3,multiply(X0,X1)))) = add(multiply(X0,multiply(X1,X2)),add(multiply(X2,X3),multiply(X3,multiply(X0,X1)))),
inference(superposition,[status(thm)],[c_118,c_128]) ).
tcf(c_255,plain,
! [X0: $i] : multiply(add(b,a),multiply(add(a,X0),add(X0,b))) = add(iPr_def_10,add(multiply(a,X0),multiply(X0,b))),
inference(superposition,[status(thm)],[c_112,c_128]) ).
tcf(c_256,plain,
! [X0: $i] : multiply(add(c,a),multiply(add(a,X0),add(X0,c))) = add(iPr_def_11,add(multiply(a,X0),multiply(X0,c))),
inference(superposition,[status(thm)],[c_113,c_128]) ).
tcf(c_257,plain,
! [X0: $i] : multiply(add(a,iPr_def_13),multiply(add(iPr_def_13,X0),add(X0,a))) = add(iPr_def_14,add(multiply(iPr_def_13,X0),multiply(X0,a))),
inference(superposition,[status(thm)],[c_116,c_128]) ).
tcf(c_263,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : multiply(add(X0,multiply(X1,X2)),multiply(add(multiply(X1,X2),X3),add(X3,X0))) = add(multiply(X0,multiply(X1,X2)),add(multiply(X1,multiply(X2,X3)),multiply(X3,X0))),
inference(superposition,[status(thm)],[c_118,c_128]) ).
tcf(c_264,plain,
! [X0: $i] : multiply(add(X0,b),multiply(add(b,a),add(a,X0))) = add(multiply(X0,b),add(iPr_def_10,multiply(a,X0))),
inference(superposition,[status(thm)],[c_112,c_128]) ).
tcf(c_265,plain,
! [X0: $i] : multiply(add(X0,c),multiply(add(c,a),add(a,X0))) = add(multiply(X0,c),add(iPr_def_11,multiply(a,X0))),
inference(superposition,[status(thm)],[c_113,c_128]) ).
tcf(c_270,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : multiply(add(X0,X1),multiply(add(X1,multiply(X2,X3)),add(multiply(X2,X3),X0))) = add(multiply(X0,X1),add(multiply(X1,multiply(X2,X3)),multiply(X2,multiply(X3,X0)))),
inference(superposition,[status(thm)],[c_118,c_128]) ).
tcf(c_271,plain,
! [X0: $i] : multiply(add(a,X0),multiply(add(X0,b),add(b,a))) = add(multiply(a,X0),add(multiply(X0,b),iPr_def_10)),
inference(superposition,[status(thm)],[c_112,c_128]) ).
tcf(c_282,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : add(X0,add(multiply(add(X1,add(X0,X2)),X3),add(X1,add(X0,X2)))) = add(X1,add(X0,X2)),
inference(superposition,[status(thm)],[c_124,c_190]) ).
tcf(c_284,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : add(multiply(X0,multiply(X1,X2)),add(multiply(X2,X3),X2)) = X2,
inference(superposition,[status(thm)],[c_118,c_190]) ).
tcf(c_288,plain,
! [X0: $i,X1: $i] : add(multiply(X0,X1),X1) = X1,
inference(superposition,[status(thm)],[c_122,c_190]) ).
tcf(c_299,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(multiply(X0,X1),add(X2,X1)) = multiply(X0,X1),
inference(superposition,[status(thm)],[c_190,c_124]) ).
tcf(c_300,plain,
! [X0: $i,X1: $i] : multiply(multiply(X0,X1),X0) = multiply(X0,X1),
inference(superposition,[status(thm)],[c_190,c_124]) ).
tcf(c_313,plain,
! [X0: $i,X1: $i] : multiply(add(X0,X1),X1) = X1,
inference(superposition,[status(thm)],[c_125,c_191]) ).
tcf(c_329,plain,
! [X0: $i,X1: $i,X2: $i] : add(add(X0,X1),multiply(X2,X1)) = add(X0,X1),
inference(superposition,[status(thm)],[c_191,c_127]) ).
tcf(c_330,plain,
! [X0: $i,X1: $i] : add(add(X0,X1),X0) = add(X0,X1),
inference(superposition,[status(thm)],[c_191,c_127]) ).
tcf(c_333,plain,
! [X0: $i,X1: $i] : add(X0,add(X1,X0)) = add(X0,X1),
inference(demodulation,[status(thm)],[c_330,c_119]) ).
tcf(c_334,plain,
! [X0: $i,X1: $i] : multiply(X0,multiply(X1,X0)) = multiply(X0,X1),
inference(demodulation,[status(thm)],[c_300,c_118]) ).
tcf(c_335,plain,
! [X0: $i] : add(X0,inverse(X0)) = iPr_def_15,
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_15])],[c_210]) ).
tcf(c_337,plain,
! [X0: $i] : multiply(X0,inverse(X0)) = iPr_def_16,
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_16])],[c_205]) ).
tcf(c_339,plain,
! [X0: $i,X1: $i,X2: $i] : add(X0,add(X1,multiply(X2,X1))) = add(X0,X1),
inference(demodulation,[status(thm)],[c_329,c_119]) ).
tcf(c_340,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(X0,multiply(X1,add(X2,X1))) = multiply(X0,X1),
inference(demodulation,[status(thm)],[c_299,c_118]) ).
tcf(c_450,plain,
! [X0: $i,X1: $i,X2: $i] : add(multiply(X0,multiply(inverse(X0),X1)),add(multiply(X1,X2),X1)) = X1,
inference(superposition,[status(thm)],[c_203,c_190]) ).
tcf(c_454,plain,
! [X0: $i,X1: $i,X2: $i] : add(multiply(X0,n0),add(multiply(X1,multiply(inverse(X1),X2)),multiply(X2,X0))) = multiply(add(X0,n0),multiply(add(n0,X2),add(X2,X0))),
inference(superposition,[status(thm)],[c_203,c_128]) ).
tcf(c_492,plain,
! [X0: $i] : add(X0,n0) = X0,
inference(superposition,[status(thm)],[c_204,c_127]) ).
tcf(c_521,plain,
! [X0: $i,X1: $i] : add(inverse(multiply(X0,inverse(X0))),X1) = add(n1,X1),
inference(superposition,[status(thm)],[c_208,c_122]) ).
tcf(c_525,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(add(X0,add(inverse(X0),X1)),multiply(add(X1,X2),X1)) = X1,
inference(superposition,[status(thm)],[c_208,c_191]) ).
tcf(c_585,plain,
! [X0: $i,X1: $i] : multiply(X0,multiply(n0,X1)) = n0,
inference(superposition,[status(thm)],[c_212,c_127]) ).
tcf(c_653,plain,
! [X0: $i,X1: $i] : multiply(add(multiply(X0,inverse(X0)),n1),X1) = X1,
inference(superposition,[status(thm)],[c_215,c_125]) ).
tcf(c_661,plain,
! [X0: $i,X1: $i,X2: $i] : add(inverse(multiply(X0,inverse(X0))),X1) = add(X2,add(inverse(X2),X1)),
inference(superposition,[status(thm)],[c_215,c_208]) ).
tcf(c_670,plain,
! [X0: $i,X1: $i] : multiply(multiply(X0,inverse(X0)),X1) = multiply(X0,inverse(X0)),
inference(superposition,[status(thm)],[c_122,c_217]) ).
tcf(c_674,plain,
! [X0: $i,X1: $i] : multiply(multiply(X0,X1),X1) = multiply(X0,X1),
inference(superposition,[status(thm)],[c_190,c_217]) ).
tcf(c_676,plain,
! [X0: $i] : multiply(iPr_def_12,add(iPr_def_10,add(iPr_def_11,X0))) = iPr_def_12,
inference(superposition,[status(thm)],[c_199,c_217]) ).
tcf(c_680,plain,
! [X0: $i] : multiply(n0,X0) = n0,
inference(superposition,[status(thm)],[c_212,c_217]) ).
tcf(c_684,plain,
! [X0: $i,X1: $i,X2: $i] : add(X0,add(multiply(add(X0,X1),X2),add(X0,X1))) = add(X0,X1),
inference(superposition,[status(thm)],[c_217,c_190]) ).
tcf(c_689,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(add(add(X0,X1),X2),multiply(add(X2,X0),add(X0,add(X0,X1)))) = add(multiply(add(X0,X1),X2),add(multiply(X2,X0),X0)),
inference(superposition,[status(thm)],[c_217,c_128]) ).
tcf(c_691,plain,
! [X0: $i,X1: $i] : add(add(X0,inverse(X0)),X1) = add(X0,inverse(X0)),
inference(superposition,[status(thm)],[c_217,c_125]) ).
tcf(c_714,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(multiply(X0,X1),add(X2,X0)) = multiply(X0,X1),
inference(superposition,[status(thm)],[c_190,c_218]) ).
tcf(c_739,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] : add(X0,add(multiply(add(X1,add(X2,add(X0,X3))),X4),add(X1,add(X2,add(X0,X3))))) = add(X1,add(X2,add(X0,X3))),
inference(superposition,[status(thm)],[c_218,c_190]) ).
tcf(c_761,plain,
! [X0: $i] : multiply(X0,n1) = X0,
inference(superposition,[status(thm)],[c_212,c_219]) ).
tcf(c_775,plain,
! [X0: $i,X1: $i] : add(X0,inverse(X0)) = add(X1,n1),
inference(superposition,[status(thm)],[c_219,c_125]) ).
tcf(c_850,plain,
multiply(b,iPr_def_13) = b,
inference(superposition,[status(thm)],[c_212,c_222]) ).
tcf(c_866,plain,
multiply(iPr_def_10,iPr_def_12) = iPr_def_10,
inference(superposition,[status(thm)],[c_212,c_223]) ).
tcf(c_902,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(X0,multiply(add(X0,X1),X2)) = multiply(X0,X2),
inference(superposition,[status(thm)],[c_212,c_224]) ).
tcf(c_905,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(X0,multiply(add(X1,X0),X2)) = multiply(X0,X2),
inference(superposition,[status(thm)],[c_127,c_224]) ).
tcf(c_928,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : add(add(X0,add(X1,X2)),multiply(X1,X3)) = add(X0,add(X1,X2)),
inference(superposition,[status(thm)],[c_224,c_127]) ).
tcf(c_1033,plain,
! [X0: $i,X1: $i] : multiply(add(X0,n1),multiply(add(n1,X1),add(X1,X0))) = add(multiply(X0,n1),add(X1,multiply(X1,X0))),
inference(superposition,[status(thm)],[c_228,c_128]) ).
tcf(c_1042,plain,
! [X0: $i,X1: $i] : add(multiply(X0,inverse(multiply(n1,X0))),X1) = X1,
inference(superposition,[status(thm)],[c_228,c_213]) ).
tcf(c_1096,plain,
! [X0: $i] : multiply(X0,n0) = n0,
inference(demodulation,[status(thm)],[c_585,c_680]) ).
tcf(c_1101,plain,
! [X0: $i] : add(X0,n1) = iPr_def_15,
inference(demodulation,[status(thm)],[c_775,c_335]) ).
tcf(c_1128,plain,
! [X0: $i,X1: $i] : multiply(X0,multiply(X1,X1)) = multiply(X0,X1),
inference(demodulation,[status(thm)],[c_674,c_118]) ).
tcf(c_1136,plain,
! [X0: $i] : add(iPr_def_16,X0) = X0,
inference(demodulation,[status(thm)],[c_1042,c_228,c_337]) ).
tcf(c_1149,plain,
! [X0: $i] : multiply(iPr_def_15,X0) = X0,
inference(demodulation,[status(thm)],[c_653,c_1101]) ).
tcf(c_1162,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(X0,multiply(X1,add(X2,X0))) = multiply(X0,X1),
inference(demodulation,[status(thm)],[c_714,c_118]) ).
tcf(c_1164,plain,
! [X0: $i,X1: $i] : add(X0,add(inverse(X0),X1)) = iPr_def_15,
inference(demodulation,[status(thm)],[c_691,c_119,c_335]) ).
tcf(c_1165,plain,
! [X0: $i,X1: $i] : multiply(X0,multiply(inverse(X0),X1)) = iPr_def_16,
inference(demodulation,[status(thm)],[c_670,c_118,c_337]) ).
tcf(c_1172,plain,
! [X0: $i] : add(inverse(iPr_def_16),X0) = add(n1,X0),
inference(demodulation,[status(thm)],[c_521,c_337]) ).
tcf(c_1270,plain,
! [X0: $i,X1: $i] : add(inverse(multiply(X0,inverse(X0))),X1) = iPr_def_15,
inference(demodulation,[status(thm)],[c_661,c_1164]) ).
tcf(c_1271,plain,
! [X0: $i] : add(inverse(iPr_def_16),X0) = iPr_def_15,
inference(demodulation,[status(thm)],[c_1270,c_337]) ).
tcf(c_1284,plain,
! [X0: $i,X1: $i] : multiply(add(X0,X1),X0) = X0,
inference(demodulation,[status(thm)],[c_525,c_1149,c_1164]) ).
tcf(c_1294,plain,
! [X0: $i,X1: $i] : add(multiply(X0,X1),X0) = X0,
inference(demodulation,[status(thm)],[c_450,c_1136,c_1165]) ).
tcf(c_1304,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : add(X0,add(X1,add(X2,multiply(X1,X3)))) = add(X0,add(X1,X2)),
inference(demodulation,[status(thm)],[c_928,c_119]) ).
tcf(c_1311,plain,
! [X0: $i,X1: $i] : add(X0,add(X0,X1)) = add(X0,X1),
inference(demodulation,[status(thm)],[c_684,c_1294]) ).
tcf(c_1362,plain,
! [X0: $i,X1: $i] : add(X0,add(X1,multiply(X1,X0))) = add(X1,X0),
inference(demodulation,[status(thm)],[c_1033,c_761,c_1101,c_1149,c_1172,c_1271]) ).
tcf(c_1363,plain,
! [X0: $i,X1: $i] : add(X0,X1) = add(X1,X0),
inference(demodulation,[status(thm)],[c_1362,c_237]) ).
tcf(c_1385,plain,
! [X0: $i,X1: $i] : multiply(X0,add(n0,X1)) = add(n0,multiply(X1,X0)),
inference(demodulation,[status(thm)],[c_454,c_492,c_1096,c_1136,c_1162,c_1165]) ).
tcf(c_1386,plain,
! [X0: $i,X1: $i] : multiply(X0,X1) = multiply(X1,X0),
inference(demodulation,[status(thm)],[c_1385,c_212]) ).
tcf(c_1403,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : add(X0,add(X1,add(X2,add(X0,X3)))) = add(X1,add(X2,add(X0,X3))),
inference(demodulation,[status(thm)],[c_739,c_1294]) ).
tcf(c_1404,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(add(add(X0,X1),X2),multiply(add(X2,X0),add(X0,X1))) = add(multiply(add(X0,X1),X2),add(X0,multiply(X2,X0))),
inference(demodulation,[status(thm)],[c_689,c_1311,c_1363]) ).
tcf(c_1405,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(add(X0,add(X1,X2)),multiply(add(X2,X0),add(X0,X1))) = add(multiply(add(X0,X1),X2),X0),
inference(demodulation,[status(thm)],[c_1404,c_119,c_339]) ).
tcf(c_1499,plain,
! [X0: $i] : multiply(add(iPr_def_13,X0),multiply(add(X0,b),add(b,iPr_def_13))) = add(multiply(iPr_def_13,X0),add(multiply(X0,b),b)),
inference(superposition,[status(thm)],[c_850,c_128]) ).
tcf(c_1505,plain,
! [X0: $i] : multiply(iPr_def_10,multiply(iPr_def_12,X0)) = multiply(iPr_def_10,X0),
inference(superposition,[status(thm)],[c_866,c_118]) ).
tcf(c_1770,plain,
add(c,iPr_def_11) = c,
inference(superposition,[status(thm)],[c_113,c_237]) ).
tcf(c_1771,plain,
add(a,iPr_def_14) = a,
inference(superposition,[status(thm)],[c_116,c_237]) ).
tcf(c_1808,plain,
! [X0: $i,X1: $i,X2: $i] : add(X0,add(X1,multiply(add(X0,X1),X2))) = add(X0,X1),
inference(superposition,[status(thm)],[c_237,c_119]) ).
tcf(c_1811,plain,
! [X0: $i] : add(iPr_def_10,add(iPr_def_11,multiply(iPr_def_12,X0))) = iPr_def_12,
inference(superposition,[status(thm)],[c_237,c_199]) ).
tcf(c_1841,plain,
! [X0: $i,X1: $i,X2: $i] : add(add(X0,X1),multiply(X2,X0)) = add(X0,X1),
inference(superposition,[status(thm)],[c_191,c_238]) ).
tcf(c_1919,plain,
add(a,iPr_def_10) = a,
inference(superposition,[status(thm)],[c_112,c_240]) ).
tcf(c_1920,plain,
add(a,iPr_def_11) = a,
inference(superposition,[status(thm)],[c_113,c_240]) ).
tcf(c_1921,plain,
add(iPr_def_13,iPr_def_14) = iPr_def_13,
inference(superposition,[status(thm)],[c_116,c_240]) ).
tcf(c_1933,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : add(add(X0,add(X1,add(X2,X3))),add(X1,X2)) = add(X0,add(X1,add(X2,X3))),
inference(superposition,[status(thm)],[c_221,c_240]) ).
tcf(c_1942,plain,
add(iPr_def_13,b) = iPr_def_13,
inference(superposition,[status(thm)],[c_850,c_240]) ).
tcf(c_1943,plain,
add(iPr_def_12,iPr_def_10) = iPr_def_12,
inference(superposition,[status(thm)],[c_866,c_240]) ).
tcf(c_1954,plain,
! [X0: $i,X1: $i,X2: $i] : add(X0,add(multiply(X1,X0),X2)) = add(X0,X2),
inference(superposition,[status(thm)],[c_240,c_119]) ).
tcf(c_2003,plain,
! [X0: $i] : add(iPr_def_13,multiply(X0,n0)) = add(b,c),
inference(superposition,[status(thm)],[c_241,c_198]) ).
tcf(c_2126,plain,
add(b,iPr_def_10) = b,
inference(superposition,[status(thm)],[c_228,c_243]) ).
tcf(c_2142,plain,
add(iPr_def_10,b) = b,
inference(demodulation,[status(thm)],[c_2126,c_1363]) ).
tcf(c_2143,plain,
add(iPr_def_10,iPr_def_11) = iPr_def_12,
inference(demodulation,[status(thm)],[c_1943,c_199,c_333]) ).
tcf(c_2144,plain,
add(iPr_def_11,a) = a,
inference(demodulation,[status(thm)],[c_1920,c_1363]) ).
tcf(c_2145,plain,
add(iPr_def_10,a) = a,
inference(demodulation,[status(thm)],[c_1919,c_1363]) ).
tcf(c_2146,plain,
add(iPr_def_14,a) = a,
inference(demodulation,[status(thm)],[c_1771,c_1363]) ).
tcf(c_2147,plain,
add(iPr_def_11,c) = c,
inference(demodulation,[status(thm)],[c_1770,c_1363]) ).
tcf(c_2175,plain,
add(b,c) = iPr_def_13,
inference(demodulation,[status(thm)],[c_2003,c_241]) ).
tcf(c_2219,plain,
! [X0: $i,X1: $i,X2: $i] : add(X0,add(X1,multiply(X2,X0))) = add(X0,X1),
inference(demodulation,[status(thm)],[c_1841,c_119]) ).
tcf(c_2299,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : add(X0,add(X1,add(X2,add(X3,X1)))) = add(X0,add(X3,add(X1,X2))),
inference(demodulation,[status(thm)],[c_1933,c_119,c_1403]) ).
tcf(c_2318,plain,
! [X0: $i] : multiply(add(iPr_def_13,X0),multiply(add(X0,b),add(iPr_def_13,b))) = add(multiply(iPr_def_13,X0),b),
inference(demodulation,[status(thm)],[c_1499,c_288,c_1363]) ).
tcf(c_2378,plain,
! [X0: $i] : multiply(iPr_def_13,multiply(add(b,X0),b)) = b,
inference(superposition,[status(thm)],[c_1942,c_191]) ).
tcf(c_2391,plain,
multiply(iPr_def_10,b) = iPr_def_10,
inference(superposition,[status(thm)],[c_2142,c_217]) ).
tcf(c_2393,plain,
! [X0: $i] : add(iPr_def_10,add(b,X0)) = add(b,X0),
inference(superposition,[status(thm)],[c_2142,c_119]) ).
tcf(c_2416,plain,
! [X0: $i] : multiply(iPr_def_11,add(X0,a)) = iPr_def_11,
inference(superposition,[status(thm)],[c_2144,c_124]) ).
tcf(c_2421,plain,
multiply(iPr_def_10,a) = iPr_def_10,
inference(superposition,[status(thm)],[c_2145,c_217]) ).
tcf(c_2426,plain,
! [X0: $i] : multiply(iPr_def_10,add(X0,a)) = iPr_def_10,
inference(superposition,[status(thm)],[c_2145,c_124]) ).
tcf(c_2431,plain,
multiply(iPr_def_14,a) = iPr_def_14,
inference(superposition,[status(thm)],[c_2146,c_217]) ).
tcf(c_2441,plain,
multiply(iPr_def_11,c) = iPr_def_11,
inference(superposition,[status(thm)],[c_2147,c_217]) ).
tcf(c_2586,plain,
! [X0: $i,X1: $i,X2: $i] : add(add(X0,X1),add(X0,X2)) = add(add(X0,X1),X2),
inference(superposition,[status(thm)],[c_191,c_246]) ).
tcf(c_2641,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] : multiply(multiply(X0,multiply(X1,X2)),multiply(add(X1,X3),X4)) = multiply(multiply(X0,multiply(X1,X2)),X4),
inference(superposition,[status(thm)],[c_246,c_224]) ).
tcf(c_2656,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : multiply(X0,multiply(multiply(X1,X2),add(X1,X3))) = multiply(X0,multiply(X1,X2)),
inference(superposition,[status(thm)],[c_246,c_225]) ).
tcf(c_2675,plain,
multiply(c,iPr_def_13) = c,
inference(superposition,[status(thm)],[c_2175,c_247]) ).
tcf(c_2677,plain,
multiply(iPr_def_11,iPr_def_12) = iPr_def_11,
inference(superposition,[status(thm)],[c_2143,c_247]) ).
tcf(c_2725,plain,
! [X0: $i] : multiply(iPr_def_11,add(X0,a)) = multiply(c,a),
inference(superposition,[status(thm)],[c_247,c_194]) ).
tcf(c_2726,plain,
! [X0: $i] : multiply(iPr_def_10,add(X0,a)) = multiply(b,a),
inference(superposition,[status(thm)],[c_247,c_193]) ).
tcf(c_2919,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : add(multiply(X0,multiply(X1,n0)),add(multiply(X2,multiply(inverse(X2),X3)),multiply(X3,multiply(X0,X1)))) = multiply(add(multiply(X0,X1),n0),multiply(add(n0,X3),add(X3,multiply(X0,X1)))),
inference(superposition,[status(thm)],[c_203,c_254]) ).
tcf(c_3024,plain,
multiply(add(b,a),multiply(add(a,iPr_def_12),add(iPr_def_10,add(iPr_def_11,b)))) = add(iPr_def_10,add(multiply(a,iPr_def_12),multiply(iPr_def_12,b))),
inference(superposition,[status(thm)],[c_199,c_255]) ).
tcf(c_3029,plain,
multiply(add(b,a),multiply(add(a,iPr_def_13),iPr_def_13)) = add(iPr_def_10,add(multiply(a,iPr_def_13),multiply(iPr_def_13,b))),
inference(superposition,[status(thm)],[c_1942,c_255]) ).
tcf(c_3094,plain,
multiply(iPr_def_13,c) = c,
inference(demodulation,[status(thm)],[c_2675,c_1386]) ).
tcf(c_3099,plain,
multiply(b,a) = iPr_def_10,
inference(demodulation,[status(thm)],[c_2726,c_2426]) ).
tcf(c_3100,plain,
multiply(a,b) = iPr_def_10,
inference(demodulation,[status(thm)],[c_3099,c_1386]) ).
tcf(c_3101,plain,
multiply(c,a) = iPr_def_11,
inference(demodulation,[status(thm)],[c_2725,c_2416]) ).
tcf(c_3102,plain,
multiply(a,c) = iPr_def_11,
inference(demodulation,[status(thm)],[c_3101,c_1386]) ).
tcf(c_3117,plain,
multiply(iPr_def_13,b) = b,
inference(demodulation,[status(thm)],[c_2378,c_1284]) ).
tcf(c_3165,plain,
! [X0: $i,X1: $i,X2: $i] : add(X0,add(X1,add(X0,X2))) = add(X0,add(X1,X2)),
inference(demodulation,[status(thm)],[c_2586,c_119]) ).
tcf(c_3179,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : multiply(X0,multiply(X1,multiply(X2,add(X1,X3)))) = multiply(X0,multiply(X1,X2)),
inference(demodulation,[status(thm)],[c_2656,c_118]) ).
tcf(c_3217,plain,
multiply(add(iPr_def_13,a),multiply(iPr_def_13,add(a,b))) = add(iPr_def_10,add(multiply(iPr_def_13,a),multiply(iPr_def_13,b))),
inference(demodulation,[status(thm)],[c_3029,c_118,c_1363,c_1386]) ).
tcf(c_3225,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] : multiply(X0,multiply(X1,multiply(X2,multiply(add(X1,X3),X4)))) = multiply(X0,multiply(X1,multiply(X2,X4))),
inference(demodulation,[status(thm)],[c_2641,c_118]) ).
tcf(c_3243,plain,
multiply(add(iPr_def_10,add(iPr_def_11,a)),multiply(add(iPr_def_10,add(iPr_def_11,b)),add(a,b))) = add(iPr_def_10,add(multiply(iPr_def_12,a),multiply(iPr_def_12,b))),
inference(demodulation,[status(thm)],[c_3024,c_118,c_199,c_1363,c_1386]) ).
tcf(c_3244,plain,
multiply(a,multiply(add(iPr_def_10,add(iPr_def_11,b)),add(a,b))) = add(iPr_def_10,add(multiply(iPr_def_12,a),multiply(iPr_def_12,b))),
inference(light_normalisation,[status(thm)],[c_3243,c_2144,c_2145]) ).
tcf(c_3338,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(X0,multiply(X1,X2)) = multiply(X1,multiply(X2,X0)),
inference(demodulation,[status(thm)],[c_2919,c_118,c_212,c_217,c_492,c_1096,c_1136,c_1165]) ).
tcf(c_3450,plain,
multiply(add(c,a),multiply(add(a,b),iPr_def_13)) = add(iPr_def_11,add(multiply(a,b),multiply(b,c))),
inference(superposition,[status(thm)],[c_2175,c_256]) ).
tcf(c_3533,plain,
multiply(add(a,iPr_def_13),multiply(add(iPr_def_13,iPr_def_12),add(iPr_def_10,add(iPr_def_11,a)))) = add(iPr_def_14,add(multiply(iPr_def_13,iPr_def_12),multiply(iPr_def_12,a))),
inference(superposition,[status(thm)],[c_199,c_257]) ).
tcf(c_3650,plain,
! [X0: $i] : multiply(add(a,X0),multiply(add(X0,iPr_def_10),add(iPr_def_10,a))) = add(multiply(a,X0),add(multiply(X0,iPr_def_10),iPr_def_10)),
inference(superposition,[status(thm)],[c_2421,c_128]) ).
tcf(c_3686,plain,
! [X0: $i] : multiply(add(c,X0),multiply(add(X0,iPr_def_11),add(iPr_def_11,c))) = add(multiply(c,X0),add(multiply(X0,iPr_def_11),iPr_def_11)),
inference(superposition,[status(thm)],[c_2441,c_128]) ).
tcf(c_3698,plain,
! [X0: $i] : add(iPr_def_11,add(multiply(iPr_def_12,X0),iPr_def_12)) = iPr_def_12,
inference(superposition,[status(thm)],[c_2677,c_190]) ).
tcf(c_3748,plain,
multiply(a,c) = multiply(iPr_def_14,c),
inference(superposition,[status(thm)],[c_3094,c_195]) ).
tcf(c_3782,plain,
! [X0: $i] : multiply(add(X0,a),multiply(add(a,c),add(c,X0))) = add(multiply(X0,a),add(iPr_def_11,multiply(c,X0))),
inference(superposition,[status(thm)],[c_3102,c_128]) ).
tcf(c_3789,plain,
multiply(add(b,a),multiply(add(a,c),add(c,b))) = add(iPr_def_10,add(iPr_def_11,multiply(c,b))),
inference(superposition,[status(thm)],[c_3102,c_255]) ).
tcf(c_3909,plain,
multiply(add(a,iPr_def_13),multiply(add(iPr_def_13,b),add(b,a))) = add(iPr_def_14,add(b,multiply(b,a))),
inference(superposition,[status(thm)],[c_3117,c_257]) ).
tcf(c_3910,plain,
multiply(a,b) = multiply(iPr_def_14,b),
inference(superposition,[status(thm)],[c_3117,c_195]) ).
tcf(c_3995,plain,
multiply(add(multiply(iPr_def_13,a),multiply(iPr_def_13,b)),multiply(add(iPr_def_13,a),multiply(iPr_def_13,add(a,b)))) = add(multiply(iPr_def_13,a),multiply(iPr_def_13,b)),
inference(superposition,[status(thm)],[c_3217,c_247]) ).
tcf(c_4020,plain,
! [X0: $i] : add(multiply(a,multiply(add(iPr_def_10,add(iPr_def_11,b)),add(a,b))),X0) = add(iPr_def_10,add(add(multiply(iPr_def_12,a),multiply(iPr_def_12,b)),X0)),
inference(superposition,[status(thm)],[c_3244,c_119]) ).
tcf(c_4021,plain,
! [X0: $i] : multiply(add(X0,iPr_def_10),multiply(multiply(a,multiply(add(iPr_def_10,add(iPr_def_11,b)),add(a,b))),iPr_def_10)) = iPr_def_10,
inference(superposition,[status(thm)],[c_3244,c_191]) ).
tcf(c_4031,plain,
multiply(add(multiply(iPr_def_12,a),multiply(iPr_def_12,b)),multiply(a,multiply(add(iPr_def_10,add(iPr_def_11,b)),add(a,b)))) = add(multiply(iPr_def_12,a),multiply(iPr_def_12,b)),
inference(superposition,[status(thm)],[c_3244,c_247]) ).
tcf(c_4036,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : multiply(add(add(X0,X1),multiply(add(X1,X2),X1)),multiply(add(multiply(add(X1,X2),X1),X3),add(X3,add(X0,X1)))) = add(X1,add(multiply(add(X1,X2),multiply(X1,X3)),multiply(X3,add(X0,X1)))),
inference(superposition,[status(thm)],[c_191,c_263]) ).
tcf(c_4274,plain,
multiply(iPr_def_14,b) = iPr_def_10,
inference(light_normalisation,[status(thm)],[c_3910,c_3100]) ).
tcf(c_4278,plain,
multiply(iPr_def_14,c) = iPr_def_11,
inference(light_normalisation,[status(thm)],[c_3748,c_3102]) ).
tcf(c_4287,plain,
add(iPr_def_11,iPr_def_12) = iPr_def_12,
inference(demodulation,[status(thm)],[c_3698,c_1294]) ).
tcf(c_4390,plain,
multiply(iPr_def_10,multiply(a,add(iPr_def_10,add(iPr_def_11,b)))) = iPr_def_10,
inference(demodulation,[status(thm)],[c_4021,c_905,c_3179,c_3338]) ).
tcf(c_4392,plain,
multiply(add(iPr_def_13,a),multiply(add(iPr_def_13,b),add(a,b))) = add(iPr_def_14,b),
inference(demodulation,[status(thm)],[c_3909,c_237,c_1363]) ).
tcf(c_4393,plain,
multiply(add(iPr_def_13,a),multiply(iPr_def_13,add(a,b))) = add(iPr_def_14,b),
inference(light_normalisation,[status(thm)],[c_4392,c_1942]) ).
tcf(c_4394,plain,
multiply(add(a,b),multiply(add(a,c),add(b,c))) = add(iPr_def_10,add(iPr_def_11,multiply(b,c))),
inference(demodulation,[status(thm)],[c_3789,c_1363,c_1386]) ).
tcf(c_4395,plain,
multiply(add(a,b),multiply(add(a,c),iPr_def_13)) = add(iPr_def_10,add(iPr_def_11,multiply(b,c))),
inference(light_normalisation,[status(thm)],[c_4394,c_2175]) ).
tcf(c_4396,plain,
multiply(iPr_def_13,multiply(add(a,b),add(a,c))) = add(iPr_def_10,add(iPr_def_11,multiply(b,c))),
inference(demodulation,[status(thm)],[c_4395,c_3338]) ).
tcf(c_4431,plain,
multiply(add(a,b),multiply(iPr_def_13,add(a,c))) = add(iPr_def_11,add(multiply(a,b),multiply(b,c))),
inference(demodulation,[status(thm)],[c_3450,c_1363,c_3338]) ).
tcf(c_4432,plain,
multiply(add(a,b),multiply(iPr_def_13,add(a,c))) = add(iPr_def_11,add(iPr_def_10,multiply(b,c))),
inference(light_normalisation,[status(thm)],[c_4431,c_3100]) ).
tcf(c_4463,plain,
! [X0: $i] : multiply(add(iPr_def_11,c),multiply(add(c,X0),add(X0,iPr_def_11))) = add(iPr_def_11,multiply(c,X0)),
inference(demodulation,[status(thm)],[c_3686,c_288,c_1363,c_3338]) ).
tcf(c_4464,plain,
! [X0: $i] : multiply(c,multiply(add(c,X0),add(X0,iPr_def_11))) = add(iPr_def_11,multiply(c,X0)),
inference(light_normalisation,[status(thm)],[c_4463,c_2147]) ).
tcf(c_4465,plain,
! [X0: $i] : multiply(c,add(X0,iPr_def_11)) = add(iPr_def_11,multiply(c,X0)),
inference(demodulation,[status(thm)],[c_4464,c_902]) ).
tcf(c_4479,plain,
! [X0: $i] : multiply(add(iPr_def_10,a),multiply(add(a,X0),add(X0,iPr_def_10))) = add(iPr_def_10,multiply(a,X0)),
inference(demodulation,[status(thm)],[c_3650,c_288,c_1363,c_3338]) ).
tcf(c_4480,plain,
! [X0: $i] : multiply(a,multiply(add(a,X0),add(X0,iPr_def_10))) = add(iPr_def_10,multiply(a,X0)),
inference(light_normalisation,[status(thm)],[c_4479,c_2145]) ).
tcf(c_4481,plain,
! [X0: $i] : multiply(a,add(X0,iPr_def_10)) = add(iPr_def_10,multiply(a,X0)),
inference(demodulation,[status(thm)],[c_4480,c_902]) ).
tcf(c_4517,plain,
multiply(add(iPr_def_10,add(iPr_def_11,iPr_def_13)),multiply(add(iPr_def_10,add(iPr_def_11,a)),add(iPr_def_13,a))) = add(iPr_def_14,add(multiply(iPr_def_12,iPr_def_13),multiply(iPr_def_12,a))),
inference(demodulation,[status(thm)],[c_3533,c_199,c_1363,c_1386,c_3338]) ).
tcf(c_4518,plain,
multiply(add(iPr_def_10,add(iPr_def_11,iPr_def_13)),multiply(a,add(iPr_def_13,a))) = add(iPr_def_14,add(multiply(iPr_def_12,iPr_def_13),multiply(iPr_def_12,a))),
inference(light_normalisation,[status(thm)],[c_4517,c_2144,c_2145]) ).
tcf(c_4519,plain,
add(iPr_def_14,add(multiply(iPr_def_12,iPr_def_13),multiply(iPr_def_12,a))) = multiply(add(iPr_def_10,add(iPr_def_11,iPr_def_13)),a),
inference(demodulation,[status(thm)],[c_4518,c_340]) ).
tcf(c_4549,plain,
! [X0: $i] : add(multiply(a,multiply(add(iPr_def_10,add(iPr_def_11,b)),add(a,b))),X0) = add(iPr_def_10,add(multiply(iPr_def_12,a),add(multiply(iPr_def_12,b),X0))),
inference(demodulation,[status(thm)],[c_4020,c_119]) ).
tcf(c_4550,plain,
multiply(add(iPr_def_13,a),multiply(iPr_def_13,multiply(add(a,b),add(multiply(iPr_def_13,a),multiply(iPr_def_13,b))))) = add(multiply(iPr_def_13,a),multiply(iPr_def_13,b)),
inference(demodulation,[status(thm)],[c_3995,c_118,c_3338]) ).
tcf(c_4551,plain,
multiply(add(iPr_def_13,a),multiply(iPr_def_13,multiply(add(a,b),add(multiply(iPr_def_13,a),b)))) = add(multiply(iPr_def_13,a),b),
inference(light_normalisation,[status(thm)],[c_4550,c_3117]) ).
tcf(c_4552,plain,
multiply(add(iPr_def_13,b),multiply(add(iPr_def_13,a),add(a,b))) = multiply(add(iPr_def_13,a),multiply(iPr_def_13,add(a,b))),
inference(demodulation,[status(thm)],[c_4551,c_1128,c_2318,c_3225,c_3338]) ).
tcf(c_4553,plain,
multiply(add(iPr_def_13,a),multiply(iPr_def_13,add(a,b))) = multiply(iPr_def_13,multiply(add(iPr_def_13,a),add(a,b))),
inference(light_normalisation,[status(thm)],[c_4552,c_1942]) ).
tcf(c_4554,plain,
multiply(add(iPr_def_13,a),multiply(iPr_def_13,add(a,b))) = multiply(iPr_def_13,add(a,b)),
inference(demodulation,[status(thm)],[c_4553,c_902]) ).
tcf(c_4602,plain,
multiply(a,multiply(add(iPr_def_10,add(iPr_def_11,b)),add(multiply(iPr_def_12,a),multiply(iPr_def_12,b)))) = add(multiply(iPr_def_12,a),multiply(iPr_def_12,b)),
inference(demodulation,[status(thm)],[c_4031,c_3179,c_3338]) ).
tcf(c_4940,plain,
! [X0: $i,X1: $i,X2: $i] : multiply(add(X0,X1),add(X1,X2)) = add(X1,multiply(X2,add(X0,X1))),
inference(demodulation,[status(thm)],[c_4036,c_119,c_246,c_339,c_1162,c_1284]) ).
tcf(c_5105,plain,
add(iPr_def_14,iPr_def_10) = iPr_def_14,
inference(superposition,[status(thm)],[c_4274,c_237]) ).
tcf(c_5171,plain,
add(iPr_def_14,iPr_def_11) = iPr_def_14,
inference(superposition,[status(thm)],[c_4278,c_237]) ).
tcf(c_5195,plain,
! [X0: $i] : add(iPr_def_11,add(iPr_def_12,X0)) = add(iPr_def_12,X0),
inference(superposition,[status(thm)],[c_4287,c_119]) ).
tcf(c_5261,plain,
! [X0: $i] : add(a,add(iPr_def_10,X0)) = add(a,X0),
inference(superposition,[status(thm)],[c_4390,c_246]) ).
tcf(c_5469,plain,
add(iPr_def_13,add(iPr_def_11,add(iPr_def_10,multiply(b,c)))) = iPr_def_13,
inference(superposition,[status(thm)],[c_4432,c_127]) ).
tcf(c_5559,plain,
multiply(add(multiply(iPr_def_12,iPr_def_13),multiply(iPr_def_12,a)),multiply(add(iPr_def_10,add(iPr_def_11,iPr_def_13)),a)) = add(multiply(iPr_def_12,iPr_def_13),multiply(iPr_def_12,a)),
inference(superposition,[status(thm)],[c_4519,c_247]) ).
tcf(c_5608,plain,
multiply(iPr_def_13,add(a,b)) = add(iPr_def_14,b),
inference(superposition,[status(thm)],[c_4554,c_4393]) ).
tcf(c_5611,plain,
add(a,add(multiply(iPr_def_12,a),multiply(iPr_def_12,b))) = a,
inference(superposition,[status(thm)],[c_4602,c_237]) ).
tcf(c_5614,plain,
! [X0: $i] : add(add(multiply(iPr_def_12,a),multiply(iPr_def_12,b)),add(multiply(multiply(add(iPr_def_10,add(iPr_def_11,b)),add(multiply(iPr_def_12,a),multiply(iPr_def_12,b))),X0),multiply(add(iPr_def_10,add(iPr_def_11,b)),add(multiply(iPr_def_12,a),multiply(iPr_def_12,b))))) = multiply(add(iPr_def_10,add(iPr_def_11,b)),add(multiply(iPr_def_12,a),multiply(iPr_def_12,b))),
inference(superposition,[status(thm)],[c_4602,c_190]) ).
tcf(c_5623,plain,
! [X0: $i] : add(a,multiply(X0,add(multiply(iPr_def_12,a),multiply(iPr_def_12,b)))) = a,
inference(superposition,[status(thm)],[c_4602,c_127]) ).
tcf(c_5639,plain,
add(multiply(add(iPr_def_10,add(iPr_def_11,b)),add(multiply(iPr_def_12,a),multiply(iPr_def_12,b))),add(multiply(iPr_def_12,a),multiply(iPr_def_12,b))) = multiply(add(iPr_def_10,add(iPr_def_11,b)),add(multiply(iPr_def_12,a),multiply(iPr_def_12,b))),
inference(superposition,[status(thm)],[c_4602,c_240]) ).
tcf(c_5649,plain,
multiply(add(iPr_def_13,b),multiply(add(b,a),add(a,iPr_def_13))) = add(b,add(iPr_def_10,multiply(a,iPr_def_13))),
inference(superposition,[status(thm)],[c_3117,c_264]) ).
tcf(c_5652,plain,
multiply(add(iPr_def_14,b),multiply(add(b,a),add(a,iPr_def_14))) = add(iPr_def_10,add(iPr_def_10,multiply(a,iPr_def_14))),
inference(superposition,[status(thm)],[c_4274,c_264]) ).
tcf(c_5669,plain,
multiply(add(multiply(add(iPr_def_10,add(iPr_def_11,b)),add(multiply(iPr_def_12,a),multiply(iPr_def_12,b))),b),multiply(add(b,a),add(a,multiply(add(iPr_def_10,add(iPr_def_11,b)),add(multiply(iPr_def_12,a),multiply(iPr_def_12,b)))))) = add(multiply(multiply(add(iPr_def_10,add(iPr_def_11,b)),add(multiply(iPr_def_12,a),multiply(iPr_def_12,b))),b),add(iPr_def_10,add(multiply(iPr_def_12,a),multiply(iPr_def_12,b)))),
inference(superposition,[status(thm)],[c_4602,c_264]) ).
tcf(c_5688,plain,
add(iPr_def_11,iPr_def_14) = iPr_def_14,
inference(demodulation,[status(thm)],[c_5171,c_1363]) ).
tcf(c_5691,plain,
add(iPr_def_10,iPr_def_14) = iPr_def_14,
inference(demodulation,[status(thm)],[c_5105,c_1363]) ).
tcf(c_5700,plain,
! [X0: $i] : add(iPr_def_10,add(iPr_def_11,X0)) = add(iPr_def_11,add(iPr_def_10,X0)),
inference(demodulation,[status(thm)],[c_5195,c_199,c_3165]) ).
tcf(c_5710,plain,
add(a,multiply(iPr_def_12,b)) = a,
inference(demodulation,[status(thm)],[c_5611,c_1954]) ).
tcf(c_5711,plain,
add(iPr_def_13,add(iPr_def_10,add(iPr_def_11,multiply(b,c)))) = iPr_def_13,
inference(demodulation,[status(thm)],[c_5469,c_5700]) ).
tcf(c_5835,plain,
multiply(add(iPr_def_14,a),multiply(add(iPr_def_14,b),add(a,b))) = multiply(add(iPr_def_10,iPr_def_14),a),
inference(demodulation,[status(thm)],[c_5652,c_1311,c_1363,c_1386,c_3338,c_4481]) ).
tcf(c_5836,plain,
multiply(a,multiply(add(iPr_def_14,b),add(a,b))) = multiply(add(iPr_def_10,iPr_def_14),a),
inference(light_normalisation,[status(thm)],[c_5835,c_2146]) ).
tcf(c_5841,plain,
add(iPr_def_10,multiply(add(iPr_def_13,b),multiply(add(iPr_def_13,a),add(a,b)))) = multiply(add(iPr_def_13,a),multiply(add(iPr_def_13,b),add(a,b))),
inference(demodulation,[status(thm)],[c_5649,c_119,c_1363,c_1386,c_2318,c_3338]) ).
tcf(c_5842,plain,
add(iPr_def_10,multiply(iPr_def_13,multiply(add(iPr_def_13,a),add(a,b)))) = multiply(iPr_def_13,add(a,b)),
inference(light_normalisation,[status(thm)],[c_5841,c_1942,c_4554]) ).
tcf(c_5843,plain,
add(iPr_def_10,multiply(iPr_def_13,add(a,b))) = multiply(iPr_def_13,add(a,b)),
inference(demodulation,[status(thm)],[c_5842,c_902]) ).
tcf(c_5911,plain,
multiply(add(iPr_def_10,add(iPr_def_11,iPr_def_13)),multiply(a,add(multiply(iPr_def_12,iPr_def_13),multiply(iPr_def_12,a)))) = add(multiply(iPr_def_12,iPr_def_13),multiply(iPr_def_12,a)),
inference(demodulation,[status(thm)],[c_5559,c_3338]) ).
tcf(c_6045,plain,
multiply(add(iPr_def_10,add(iPr_def_11,b)),add(multiply(iPr_def_12,a),multiply(iPr_def_12,b))) = add(multiply(iPr_def_12,a),multiply(iPr_def_12,b)),
inference(demodulation,[status(thm)],[c_5639,c_288]) ).
tcf(c_6169,plain,
add(multiply(iPr_def_12,a),multiply(add(multiply(iPr_def_12,a),multiply(iPr_def_12,b)),add(multiply(iPr_def_12,b),add(iPr_def_10,add(iPr_def_11,b))))) = multiply(add(iPr_def_10,add(iPr_def_11,b)),add(multiply(iPr_def_12,a),multiply(iPr_def_12,b))),
inference(demodulation,[status(thm)],[c_5614,c_119,c_1294,c_4940]) ).
tcf(c_6200,plain,
add(multiply(multiply(add(iPr_def_10,add(iPr_def_11,b)),add(multiply(iPr_def_12,a),multiply(iPr_def_12,b))),b),add(iPr_def_10,add(multiply(iPr_def_12,a),multiply(iPr_def_12,b)))) = multiply(add(multiply(add(iPr_def_10,add(iPr_def_11,b)),add(multiply(iPr_def_12,a),multiply(iPr_def_12,b))),b),multiply(add(b,a),a)),
inference(demodulation,[status(thm)],[c_5669,c_5623]) ).
tcf(c_6201,plain,
add(multiply(b,multiply(add(iPr_def_10,add(iPr_def_11,b)),add(multiply(iPr_def_12,a),multiply(iPr_def_12,b)))),add(iPr_def_10,add(multiply(iPr_def_12,a),multiply(iPr_def_12,b)))) = multiply(add(a,b),multiply(a,add(b,multiply(add(iPr_def_10,add(iPr_def_11,b)),add(multiply(iPr_def_12,a),multiply(iPr_def_12,b)))))),
inference(demodulation,[status(thm)],[c_6200,c_118,c_1363,c_3338]) ).
tcf(c_6202,plain,
add(multiply(b,multiply(add(iPr_def_10,add(iPr_def_11,b)),add(multiply(iPr_def_12,a),multiply(iPr_def_12,b)))),multiply(a,multiply(add(iPr_def_10,add(iPr_def_11,b)),add(a,b)))) = multiply(add(a,b),multiply(a,add(b,multiply(add(iPr_def_10,add(iPr_def_11,b)),add(multiply(iPr_def_12,a),multiply(iPr_def_12,b)))))),
inference(light_normalisation,[status(thm)],[c_6201,c_3244]) ).
tcf(c_6203,plain,
add(iPr_def_10,add(multiply(iPr_def_12,a),add(multiply(iPr_def_12,b),multiply(b,multiply(add(iPr_def_10,add(iPr_def_11,b)),add(multiply(iPr_def_12,a),multiply(iPr_def_12,b))))))) = multiply(add(a,b),multiply(a,add(b,multiply(add(iPr_def_10,add(iPr_def_11,b)),add(multiply(iPr_def_12,a),multiply(iPr_def_12,b)))))),
inference(demodulation,[status(thm)],[c_6202,c_1363,c_4549]) ).
tcf(c_6364,plain,
! [X0: $i] : multiply(iPr_def_13,multiply(add(a,b),X0)) = multiply(add(iPr_def_14,b),X0),
inference(superposition,[status(thm)],[c_5608,c_118]) ).
tcf(c_6376,plain,
multiply(a,add(iPr_def_14,b)) = multiply(iPr_def_14,add(a,b)),
inference(superposition,[status(thm)],[c_5608,c_195]) ).
tcf(c_6379,plain,
add(add(a,b),add(iPr_def_14,b)) = add(a,b),
inference(superposition,[status(thm)],[c_5608,c_240]) ).
tcf(c_6388,plain,
! [X0: $i] : add(iPr_def_11,add(iPr_def_14,X0)) = add(iPr_def_14,X0),
inference(superposition,[status(thm)],[c_5688,c_119]) ).
tcf(c_6441,plain,
! [X0: $i] : add(iPr_def_10,add(iPr_def_14,X0)) = add(iPr_def_14,X0),
inference(superposition,[status(thm)],[c_5691,c_119]) ).
tcf(c_6497,plain,
multiply(multiply(iPr_def_12,b),a) = multiply(iPr_def_12,b),
inference(superposition,[status(thm)],[c_5710,c_247]) ).
tcf(c_6515,plain,
multiply(add(iPr_def_10,iPr_def_11),iPr_def_13) = add(iPr_def_10,iPr_def_11),
inference(superposition,[status(thm)],[c_5711,c_221]) ).
tcf(c_6516,plain,
multiply(add(iPr_def_10,add(iPr_def_11,multiply(b,c))),iPr_def_13) = add(iPr_def_10,add(iPr_def_11,multiply(b,c))),
inference(superposition,[status(thm)],[c_5711,c_247]) ).
tcf(c_6748,plain,
multiply(add(b,a),multiply(add(a,multiply(add(iPr_def_14,b),add(a,b))),add(multiply(add(iPr_def_14,b),add(a,b)),b))) = add(iPr_def_10,add(multiply(add(iPr_def_10,iPr_def_14),a),multiply(multiply(add(iPr_def_14,b),add(a,b)),b))),
inference(superposition,[status(thm)],[c_5836,c_255]) ).
tcf(c_6761,plain,
add(iPr_def_10,add(iPr_def_14,b)) = add(iPr_def_14,b),
inference(superposition,[status(thm)],[c_5608,c_5843]) ).
tcf(c_6885,plain,
add(multiply(a,add(multiply(iPr_def_12,iPr_def_13),multiply(iPr_def_12,a))),add(multiply(iPr_def_12,iPr_def_13),multiply(iPr_def_12,a))) = multiply(a,add(multiply(iPr_def_12,iPr_def_13),multiply(iPr_def_12,a))),
inference(superposition,[status(thm)],[c_5911,c_240]) ).
tcf(c_6895,plain,
multiply(iPr_def_13,add(iPr_def_10,iPr_def_11)) = add(iPr_def_10,iPr_def_11),
inference(demodulation,[status(thm)],[c_6515,c_1386]) ).
tcf(c_6896,plain,
multiply(iPr_def_13,iPr_def_12) = iPr_def_12,
inference(light_normalisation,[status(thm)],[c_6895,c_2143]) ).
tcf(c_6897,plain,
multiply(iPr_def_12,iPr_def_13) = iPr_def_12,
inference(demodulation,[status(thm)],[c_6896,c_1386]) ).
tcf(c_6898,plain,
multiply(a,multiply(iPr_def_12,b)) = multiply(iPr_def_12,b),
inference(demodulation,[status(thm)],[c_6497,c_118,c_3338]) ).
tcf(c_6938,plain,
add(a,add(iPr_def_14,b)) = add(a,b),
inference(demodulation,[status(thm)],[c_6379,c_119,c_333,c_1363]) ).
tcf(c_7050,plain,
multiply(iPr_def_13,add(iPr_def_10,add(iPr_def_11,multiply(b,c)))) = add(iPr_def_10,add(iPr_def_11,multiply(b,c))),
inference(demodulation,[status(thm)],[c_6516,c_1386]) ).
tcf(c_7175,plain,
multiply(a,add(multiply(iPr_def_12,iPr_def_13),multiply(iPr_def_12,a))) = add(multiply(iPr_def_12,iPr_def_13),multiply(iPr_def_12,a)),
inference(demodulation,[status(thm)],[c_6885,c_288]) ).
tcf(c_7257,plain,
add(iPr_def_10,add(multiply(add(iPr_def_10,iPr_def_14),a),b)) = multiply(add(iPr_def_14,b),add(a,b)),
inference(demodulation,[status(thm)],[c_6748,c_118,c_247,c_313,c_333,c_334,c_905,c_1363,c_1386,c_3338,c_4940]) ).
tcf(c_7258,plain,
multiply(add(iPr_def_14,b),add(a,b)) = add(iPr_def_10,add(iPr_def_14,b)),
inference(light_normalisation,[status(thm)],[c_7257,c_2431,c_5691]) ).
tcf(c_7499,plain,
multiply(add(b,c),multiply(add(c,a),add(a,b))) = add(multiply(b,c),add(iPr_def_11,iPr_def_10)),
inference(superposition,[status(thm)],[c_3100,c_265]) ).
tcf(c_7501,plain,
multiply(add(multiply(add(iPr_def_14,b),add(a,b)),c),multiply(add(c,a),add(a,multiply(add(iPr_def_14,b),add(a,b))))) = add(multiply(multiply(add(iPr_def_14,b),add(a,b)),c),add(iPr_def_11,multiply(add(iPr_def_10,iPr_def_14),a))),
inference(superposition,[status(thm)],[c_5836,c_265]) ).
tcf(c_7965,plain,
multiply(add(a,c),multiply(add(c,b),add(b,a))) = add(iPr_def_11,add(multiply(c,b),iPr_def_10)),
inference(superposition,[status(thm)],[c_3102,c_271]) ).
tcf(c_8161,plain,
add(multiply(a,b),multiply(add(iPr_def_11,b),c)) = add(iPr_def_10,add(iPr_def_11,multiply(b,c))),
inference(demodulation,[status(thm)],[c_7965,c_1363,c_1386,c_3338,c_3782,c_4465,c_5700]) ).
tcf(c_8162,plain,
add(iPr_def_10,multiply(add(iPr_def_11,b),c)) = add(iPr_def_10,add(iPr_def_11,multiply(b,c))),
inference(light_normalisation,[status(thm)],[c_8161,c_3100]) ).
tcf(c_8188,plain,
multiply(add(a,b),multiply(add(a,c),add(b,c))) = add(iPr_def_10,add(iPr_def_11,multiply(b,c))),
inference(demodulation,[status(thm)],[c_7499,c_119,c_1363,c_1386,c_3338,c_5700]) ).
tcf(c_8189,plain,
multiply(add(a,b),multiply(add(a,c),iPr_def_13)) = add(iPr_def_10,add(iPr_def_11,multiply(b,c))),
inference(light_normalisation,[status(thm)],[c_8188,c_2175]) ).
tcf(c_8190,plain,
multiply(add(iPr_def_14,b),add(a,c)) = add(iPr_def_10,add(iPr_def_11,multiply(b,c))),
inference(demodulation,[status(thm)],[c_8189,c_3338,c_6364]) ).
tcf(c_8555,plain,
multiply(add(a,multiply(add(iPr_def_14,b),add(a,b))),multiply(add(a,c),add(multiply(add(iPr_def_14,b),add(a,b)),c))) = add(iPr_def_11,add(multiply(add(iPr_def_10,iPr_def_14),a),multiply(add(iPr_def_14,b),multiply(add(a,b),c)))),
inference(demodulation,[status(thm)],[c_7501,c_119,c_118,c_1363,c_1386,c_3338]) ).
tcf(c_8556,plain,
multiply(add(a,b),multiply(add(a,c),add(add(iPr_def_14,b),c))) = add(iPr_def_11,add(iPr_def_14,multiply(add(iPr_def_14,b),multiply(add(a,b),c)))),
inference(light_normalisation,[status(thm)],[c_8555,c_2431,c_5691,c_6761,c_6938,c_7258]) ).
tcf(c_8557,plain,
multiply(add(a,b),multiply(add(a,c),add(iPr_def_14,add(b,c)))) = add(iPr_def_14,multiply(add(iPr_def_14,b),multiply(add(a,b),c))),
inference(demodulation,[status(thm)],[c_8556,c_119,c_6388]) ).
tcf(c_8558,plain,
multiply(add(a,b),multiply(add(a,c),add(iPr_def_14,iPr_def_13))) = add(iPr_def_14,multiply(add(iPr_def_14,b),multiply(add(a,b),c))),
inference(light_normalisation,[status(thm)],[c_8557,c_2175]) ).
tcf(c_8559,plain,
multiply(add(iPr_def_13,iPr_def_14),multiply(add(a,b),add(a,c))) = add(iPr_def_14,multiply(add(iPr_def_14,b),multiply(add(a,b),c))),
inference(demodulation,[status(thm)],[c_8558,c_1363,c_3338]) ).
tcf(c_8560,plain,
add(iPr_def_14,multiply(add(iPr_def_14,b),multiply(add(a,b),c))) = add(iPr_def_10,add(iPr_def_11,multiply(b,c))),
inference(light_normalisation,[status(thm)],[c_8559,c_1921,c_4396]) ).
tcf(c_8839,plain,
multiply(multiply(iPr_def_12,a),multiply(add(iPr_def_10,add(iPr_def_11,b)),add(multiply(iPr_def_12,a),multiply(iPr_def_12,b)))) = multiply(iPr_def_12,a),
inference(superposition,[status(thm)],[c_6169,c_217]) ).
tcf(c_8867,plain,
multiply(add(multiply(iPr_def_12,a),multiply(iPr_def_12,b)),multiply(add(a,b),multiply(a,add(b,multiply(add(iPr_def_10,add(iPr_def_11,b)),add(multiply(iPr_def_12,a),multiply(iPr_def_12,b))))))) = add(multiply(iPr_def_12,a),multiply(iPr_def_12,b)),
inference(superposition,[status(thm)],[c_6203,c_221]) ).
tcf(c_8887,plain,
! [X0: $i] : add(multiply(a,add(iPr_def_14,b)),add(multiply(add(a,b),X0),add(a,b))) = add(a,b),
inference(superposition,[status(thm)],[c_6376,c_190]) ).
tcf(c_8889,plain,
! [X0: $i] : multiply(multiply(a,add(iPr_def_14,b)),X0) = multiply(iPr_def_14,multiply(add(a,b),X0)),
inference(superposition,[status(thm)],[c_6376,c_118]) ).
tcf(c_9158,plain,
multiply(b,multiply(iPr_def_12,b)) = multiply(iPr_def_10,multiply(iPr_def_12,b)),
inference(superposition,[status(thm)],[c_6898,c_193]) ).
tcf(c_9227,plain,
! [X0: $i] : multiply(iPr_def_14,multiply(add(a,b),X0)) = multiply(iPr_def_14,X0),
inference(superposition,[status(thm)],[c_6938,c_224]) ).
tcf(c_9394,plain,
multiply(a,add(iPr_def_10,add(iPr_def_11,multiply(b,c)))) = multiply(iPr_def_14,add(iPr_def_10,add(iPr_def_11,multiply(b,c)))),
inference(superposition,[status(thm)],[c_7050,c_195]) ).
tcf(c_9492,plain,
multiply(iPr_def_10,b) = multiply(iPr_def_12,b),
inference(demodulation,[status(thm)],[c_9158,c_334,c_1386,c_1505]) ).
tcf(c_9493,plain,
multiply(iPr_def_12,b) = iPr_def_10,
inference(light_normalisation,[status(thm)],[c_9492,c_2391]) ).
tcf(c_9560,plain,
! [X0: $i] : multiply(multiply(a,add(iPr_def_14,b)),X0) = multiply(iPr_def_14,X0),
inference(demodulation,[status(thm)],[c_8889,c_9227]) ).
tcf(c_9561,plain,
! [X0: $i] : multiply(a,multiply(add(iPr_def_14,b),X0)) = multiply(iPr_def_14,X0),
inference(demodulation,[status(thm)],[c_9560,c_118]) ).
tcf(c_9596,plain,
multiply(a,add(iPr_def_10,multiply(add(iPr_def_11,b),c))) = multiply(iPr_def_14,add(iPr_def_10,multiply(add(iPr_def_11,b),c))),
inference(light_normalisation,[status(thm)],[c_9394,c_8162]) ).
tcf(c_9609,plain,
add(multiply(a,add(iPr_def_14,b)),add(a,b)) = add(a,b),
inference(demodulation,[status(thm)],[c_8887,c_1405,c_1808,c_2299,c_3338]) ).
tcf(c_9634,plain,
multiply(iPr_def_12,multiply(a,multiply(add(iPr_def_10,add(iPr_def_11,b)),add(multiply(iPr_def_12,a),multiply(iPr_def_12,b))))) = multiply(iPr_def_12,a),
inference(demodulation,[status(thm)],[c_8839,c_118]) ).
tcf(c_9635,plain,
multiply(iPr_def_12,add(multiply(iPr_def_12,a),multiply(iPr_def_12,b))) = multiply(iPr_def_12,a),
inference(light_normalisation,[status(thm)],[c_9634,c_4602]) ).
tcf(c_9899,plain,
multiply(add(multiply(iPr_def_12,a),multiply(iPr_def_12,b)),multiply(add(a,b),multiply(a,add(b,add(multiply(iPr_def_12,a),multiply(iPr_def_12,b)))))) = add(multiply(iPr_def_12,a),multiply(iPr_def_12,b)),
inference(light_normalisation,[status(thm)],[c_8867,c_6045]) ).
tcf(c_9900,plain,
multiply(add(a,b),multiply(a,multiply(add(multiply(iPr_def_12,a),b),add(multiply(iPr_def_12,a),multiply(iPr_def_12,b))))) = add(multiply(iPr_def_12,a),multiply(iPr_def_12,b)),
inference(demodulation,[status(thm)],[c_9899,c_118,c_1363,c_2219,c_3338]) ).
tcf(c_10223,plain,
multiply(a,add(iPr_def_12,multiply(iPr_def_12,a))) = add(iPr_def_12,multiply(iPr_def_12,a)),
inference(superposition,[status(thm)],[c_6897,c_7175]) ).
tcf(c_10246,plain,
multiply(add(add(multiply(iPr_def_12,iPr_def_13),multiply(iPr_def_12,a)),b),multiply(add(b,a),add(a,add(multiply(iPr_def_12,iPr_def_13),multiply(iPr_def_12,a))))) = add(multiply(add(multiply(iPr_def_12,iPr_def_13),multiply(iPr_def_12,a)),b),add(iPr_def_10,add(multiply(iPr_def_12,iPr_def_13),multiply(iPr_def_12,a)))),
inference(superposition,[status(thm)],[c_7175,c_264]) ).
tcf(c_10397,plain,
multiply(a,add(iPr_def_10,add(iPr_def_14,b))) = multiply(add(iPr_def_10,iPr_def_14),a),
inference(superposition,[status(thm)],[c_7258,c_5836]) ).
tcf(c_10517,plain,
! [X0: $i] : add(add(iPr_def_10,multiply(add(iPr_def_11,b),c)),X0) = add(iPr_def_10,add(add(iPr_def_11,multiply(b,c)),X0)),
inference(superposition,[status(thm)],[c_8162,c_119]) ).
tcf(c_10537,plain,
add(add(iPr_def_14,b),add(iPr_def_10,add(iPr_def_11,multiply(b,c)))) = add(iPr_def_14,b),
inference(superposition,[status(thm)],[c_8190,c_237]) ).
tcf(c_10548,plain,
! [X0: $i,X1: $i] : add(add(iPr_def_14,b),add(multiply(X0,add(iPr_def_10,add(iPr_def_11,multiply(b,c)))),X1)) = add(add(iPr_def_14,b),X1),
inference(superposition,[status(thm)],[c_8190,c_246]) ).
tcf(c_10684,plain,
multiply(iPr_def_14,add(iPr_def_10,add(iPr_def_11,multiply(b,c)))) = iPr_def_14,
inference(superposition,[status(thm)],[c_8560,c_217]) ).
tcf(c_10823,plain,
multiply(iPr_def_14,add(iPr_def_10,multiply(add(iPr_def_11,b),c))) = iPr_def_14,
inference(light_normalisation,[status(thm)],[c_10684,c_8162]) ).
tcf(c_10837,plain,
multiply(add(iPr_def_10,iPr_def_14),a) = multiply(a,add(iPr_def_14,b)),
inference(demodulation,[status(thm)],[c_10397,c_6441]) ).
tcf(c_10838,plain,
multiply(a,add(iPr_def_14,b)) = iPr_def_14,
inference(light_normalisation,[status(thm)],[c_10837,c_2431,c_5691]) ).
tcf(c_10839,plain,
multiply(iPr_def_12,a) = iPr_def_12,
inference(demodulation,[status(thm)],[c_10223,c_199,c_1386,c_1811]) ).
tcf(c_10846,plain,
add(iPr_def_14,add(b,add(iPr_def_10,add(iPr_def_11,multiply(b,c))))) = add(iPr_def_14,b),
inference(demodulation,[status(thm)],[c_10537,c_119]) ).
tcf(c_10847,plain,
add(iPr_def_14,add(b,add(iPr_def_10,multiply(add(iPr_def_11,b),c)))) = add(iPr_def_14,b),
inference(light_normalisation,[status(thm)],[c_10846,c_8162]) ).
tcf(c_10903,plain,
! [X0: $i] : add(iPr_def_10,add(multiply(add(iPr_def_11,b),c),X0)) = add(iPr_def_10,add(iPr_def_11,add(multiply(b,c),X0))),
inference(demodulation,[status(thm)],[c_10517,c_119]) ).
tcf(c_10950,plain,
! [X0: $i,X1: $i] : add(iPr_def_14,add(b,add(multiply(X0,add(iPr_def_10,add(iPr_def_11,multiply(b,c)))),X1))) = add(iPr_def_14,add(b,X1)),
inference(demodulation,[status(thm)],[c_10548,c_119]) ).
tcf(c_10951,plain,
! [X0: $i,X1: $i] : add(iPr_def_14,add(b,add(multiply(X0,add(iPr_def_10,multiply(add(iPr_def_11,b),c))),X1))) = add(iPr_def_14,add(b,X1)),
inference(light_normalisation,[status(thm)],[c_10950,c_8162]) ).
tcf(c_11239,plain,
multiply(add(multiply(iPr_def_12,iPr_def_13),a),multiply(add(a,b),add(multiply(iPr_def_12,iPr_def_13),add(multiply(iPr_def_12,a),b)))) = add(iPr_def_10,add(multiply(iPr_def_12,iPr_def_13),multiply(iPr_def_12,a))),
inference(demodulation,[status(thm)],[c_10246,c_119,c_1363,c_1386,c_1808,c_2219,c_3338]) ).
tcf(c_11240,plain,
multiply(add(iPr_def_12,a),multiply(add(a,b),add(iPr_def_12,add(multiply(iPr_def_12,a),b)))) = add(iPr_def_10,add(iPr_def_12,multiply(iPr_def_12,a))),
inference(light_normalisation,[status(thm)],[c_11239,c_6897]) ).
tcf(c_11241,plain,
multiply(add(iPr_def_10,add(iPr_def_11,a)),multiply(add(a,b),add(iPr_def_10,add(iPr_def_11,add(multiply(iPr_def_12,a),b))))) = add(iPr_def_10,iPr_def_12),
inference(demodulation,[status(thm)],[c_11240,c_199,c_1811]) ).
tcf(c_11242,plain,
multiply(a,multiply(add(a,b),add(iPr_def_10,add(iPr_def_11,add(multiply(iPr_def_12,a),b))))) = add(iPr_def_10,iPr_def_12),
inference(light_normalisation,[status(thm)],[c_11241,c_2144,c_2145]) ).
tcf(c_11243,plain,
multiply(a,add(iPr_def_10,add(iPr_def_11,add(multiply(iPr_def_12,a),b)))) = add(iPr_def_10,iPr_def_12),
inference(demodulation,[status(thm)],[c_11242,c_902]) ).
tcf(c_12328,plain,
! [X0: $i,X1: $i,X2: $i] : add(X0,add(add(X0,X1),add(X2,add(X0,X1)))) = add(X2,add(X0,X1)),
inference(superposition,[status(thm)],[c_191,c_282]) ).
tcf(c_12632,plain,
! [X0: $i,X1: $i] : add(iPr_def_10,add(multiply(add(X0,b),X1),add(X0,b))) = add(X0,b),
inference(superposition,[status(thm)],[c_2142,c_282]) ).
tcf(c_12656,plain,
! [X0: $i,X1: $i] : add(iPr_def_11,add(multiply(add(X0,iPr_def_14),X1),add(X0,iPr_def_14))) = add(X0,iPr_def_14),
inference(superposition,[status(thm)],[c_5688,c_282]) ).
tcf(c_12713,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] : add(X0,add(add(multiply(add(X1,add(X0,X2)),X3),add(X1,add(X0,X2))),multiply(X4,multiply(add(X1,add(X0,X2)),X5)))) = add(X1,add(X0,X2)),
inference(superposition,[status(thm)],[c_282,c_249]) ).
tcf(c_12746,plain,
! [X0: $i,X1: $i,X2: $i] : add(X0,add(X1,add(X0,X2))) = add(X1,add(X0,X2)),
inference(superposition,[status(thm)],[c_282,c_246]) ).
tcf(c_12808,plain,
! [X0: $i] : add(iPr_def_11,add(X0,iPr_def_14)) = add(X0,iPr_def_14),
inference(demodulation,[status(thm)],[c_12656,c_1405,c_1808,c_2299,c_3338]) ).
tcf(c_12816,plain,
! [X0: $i] : add(iPr_def_10,add(X0,b)) = add(X0,b),
inference(demodulation,[status(thm)],[c_12632,c_1405,c_1808,c_2299,c_3338]) ).
tcf(c_12861,plain,
! [X0: $i,X1: $i,X2: $i] : add(X0,add(X1,add(X2,X0))) = add(X1,add(X2,X0)),
inference(demodulation,[status(thm)],[c_12328,c_119,c_1403]) ).
tcf(c_13248,plain,
! [X0: $i,X1: $i,X2: $i] : add(X0,add(X1,X2)) = add(X1,add(X0,X2)),
inference(demodulation,[status(thm)],[c_12713,c_119,c_249,c_1294,c_3165]) ).
tcf(c_14443,plain,
multiply(add(b,a),multiply(add(a,add(iPr_def_10,multiply(add(iPr_def_11,b),c))),add(add(iPr_def_10,multiply(add(iPr_def_11,b),c)),b))) = add(iPr_def_10,add(multiply(iPr_def_14,add(iPr_def_10,multiply(add(iPr_def_11,b),c))),multiply(add(iPr_def_10,multiply(add(iPr_def_11,b),c)),b))),
inference(superposition,[status(thm)],[c_9596,c_255]) ).
tcf(c_14506,plain,
! [X0: $i,X1: $i] : multiply(multiply(a,add(iPr_def_14,b)),add(X0,add(X1,add(a,b)))) = multiply(a,add(iPr_def_14,b)),
inference(superposition,[status(thm)],[c_9609,c_218]) ).
tcf(c_14520,plain,
! [X0: $i,X1: $i] : add(multiply(X0,multiply(iPr_def_12,a)),add(multiply(add(multiply(iPr_def_12,a),multiply(iPr_def_12,b)),X1),add(multiply(iPr_def_12,a),multiply(iPr_def_12,b)))) = add(multiply(iPr_def_12,a),multiply(iPr_def_12,b)),
inference(superposition,[status(thm)],[c_9635,c_284]) ).
tcf(c_14849,plain,
! [X0: $i,X1: $i] : multiply(iPr_def_14,add(X0,add(X1,add(a,b)))) = multiply(a,add(iPr_def_14,b)),
inference(demodulation,[status(thm)],[c_14506,c_118,c_9561]) ).
tcf(c_14850,plain,
! [X0: $i,X1: $i] : multiply(iPr_def_14,add(X0,add(X1,add(a,b)))) = iPr_def_14,
inference(light_normalisation,[status(thm)],[c_14849,c_10838]) ).
tcf(c_15038,plain,
! [X0: $i] : add(multiply(iPr_def_12,b),multiply(add(multiply(iPr_def_12,a),multiply(iPr_def_12,b)),multiply(add(multiply(iPr_def_12,a),add(multiply(iPr_def_12,b),X0)),add(X0,multiply(iPr_def_12,a))))) = add(multiply(iPr_def_12,a),multiply(iPr_def_12,b)),
inference(demodulation,[status(thm)],[c_14520,c_1405,c_13248,c_1954,c_2299,c_3338,c_12861]) ).
tcf(c_15039,plain,
! [X0: $i] : add(iPr_def_10,multiply(add(iPr_def_12,iPr_def_10),multiply(add(iPr_def_12,add(iPr_def_10,X0)),add(X0,iPr_def_12)))) = add(iPr_def_12,iPr_def_10),
inference(light_normalisation,[status(thm)],[c_15038,c_9493,c_10839]) ).
tcf(c_15040,plain,
! [X0: $i] : add(iPr_def_10,multiply(add(iPr_def_10,iPr_def_11),multiply(add(iPr_def_10,add(iPr_def_11,X0)),add(X0,iPr_def_12)))) = add(iPr_def_10,iPr_def_11),
inference(demodulation,[status(thm)],[c_15039,c_199,c_333,c_5700,c_12746]) ).
tcf(c_15041,plain,
! [X0: $i] : add(iPr_def_10,multiply(iPr_def_12,multiply(add(iPr_def_10,add(iPr_def_11,X0)),add(X0,iPr_def_12)))) = iPr_def_12,
inference(light_normalisation,[status(thm)],[c_15040,c_2143]) ).
tcf(c_15042,plain,
add(iPr_def_10,iPr_def_12) = iPr_def_12,
inference(demodulation,[status(thm)],[c_15041,c_676,c_1162]) ).
tcf(c_15244,plain,
add(iPr_def_10,add(multiply(iPr_def_14,add(iPr_def_10,multiply(add(iPr_def_11,b),c))),multiply(b,add(iPr_def_10,multiply(add(iPr_def_11,b),c))))) = multiply(add(a,b),multiply(add(iPr_def_11,b),add(a,multiply(add(iPr_def_11,b),c)))),
inference(demodulation,[status(thm)],[c_14443,c_119,c_1294,c_1363,c_1386,c_5261,c_10903,c_12816]) ).
tcf(c_15245,plain,
multiply(add(a,b),multiply(add(iPr_def_11,b),add(a,multiply(add(iPr_def_11,b),c)))) = add(iPr_def_10,add(iPr_def_14,multiply(b,add(iPr_def_10,multiply(add(iPr_def_11,b),c))))),
inference(light_normalisation,[status(thm)],[c_15244,c_10823]) ).
tcf(c_15246,plain,
multiply(add(a,b),multiply(add(iPr_def_11,b),add(a,multiply(add(iPr_def_11,b),c)))) = add(iPr_def_14,multiply(b,add(iPr_def_10,multiply(add(iPr_def_11,b),c)))),
inference(demodulation,[status(thm)],[c_15245,c_6441]) ).
tcf(c_16003,plain,
! [X0: $i,X1: $i] : add(multiply(X0,iPr_def_12),add(multiply(a,X1),a)) = a,
inference(superposition,[status(thm)],[c_10839,c_284]) ).
tcf(c_16017,plain,
! [X0: $i,X1: $i] : multiply(add(a,X0),multiply(add(X0,multiply(X1,iPr_def_12)),add(multiply(X1,iPr_def_12),a))) = add(multiply(a,X0),add(multiply(X0,multiply(X1,iPr_def_12)),multiply(X1,iPr_def_12))),
inference(superposition,[status(thm)],[c_10839,c_270]) ).
tcf(c_16025,plain,
multiply(add(a,b),multiply(a,multiply(add(iPr_def_12,b),add(iPr_def_12,multiply(iPr_def_12,b))))) = add(iPr_def_12,multiply(iPr_def_12,b)),
inference(superposition,[status(thm)],[c_10839,c_9900]) ).
tcf(c_16074,plain,
! [X0: $i] : add(multiply(X0,iPr_def_12),a) = a,
inference(demodulation,[status(thm)],[c_16003,c_1294]) ).
tcf(c_16175,plain,
multiply(a,multiply(add(iPr_def_11,b),multiply(iPr_def_12,add(a,b)))) = iPr_def_12,
inference(demodulation,[status(thm)],[c_16025,c_118,c_199,c_1811,c_3338,c_12816]) ).
tcf(c_16307,plain,
! [X0: $i,X1: $i] : add(multiply(a,X0),add(multiply(X0,multiply(X1,iPr_def_12)),multiply(X1,iPr_def_12))) = multiply(add(a,X0),multiply(add(X0,multiply(X1,iPr_def_12)),a)),
inference(demodulation,[status(thm)],[c_16017,c_16074]) ).
tcf(c_16308,plain,
! [X0: $i,X1: $i] : multiply(a,add(X0,multiply(X1,iPr_def_12))) = add(multiply(a,X0),multiply(X1,iPr_def_12)),
inference(demodulation,[status(thm)],[c_16307,c_288,c_902,c_3338]) ).
tcf(c_17068,plain,
multiply(add(b,add(iPr_def_10,multiply(add(iPr_def_11,b),c))),add(iPr_def_14,b)) = add(b,add(iPr_def_10,multiply(add(iPr_def_11,b),c))),
inference(superposition,[status(thm)],[c_10847,c_247]) ).
tcf(c_17874,plain,
multiply(add(iPr_def_14,b),add(b,multiply(add(iPr_def_11,b),c))) = add(b,multiply(add(iPr_def_11,b),c)),
inference(demodulation,[status(thm)],[c_17068,c_1386,c_13248,c_2393]) ).
tcf(c_18854,plain,
multiply(a,add(iPr_def_10,add(iPr_def_11,add(iPr_def_12,b)))) = add(iPr_def_10,iPr_def_12),
inference(superposition,[status(thm)],[c_10839,c_11243]) ).
tcf(c_19304,plain,
multiply(a,add(iPr_def_11,b)) = add(iPr_def_10,iPr_def_12),
inference(demodulation,[status(thm)],[c_18854,c_199,c_1311,c_12816]) ).
tcf(c_19305,plain,
multiply(a,add(iPr_def_11,b)) = iPr_def_12,
inference(light_normalisation,[status(thm)],[c_19304,c_15042]) ).
tcf(c_23461,plain,
! [X0: $i] : add(add(iPr_def_11,b),add(add(iPr_def_14,multiply(b,add(iPr_def_10,multiply(add(iPr_def_11,b),c)))),X0)) = add(add(iPr_def_11,b),X0),
inference(superposition,[status(thm)],[c_15246,c_246]) ).
tcf(c_23473,plain,
add(iPr_def_11,add(b,add(iPr_def_14,multiply(b,add(iPr_def_10,multiply(add(iPr_def_11,b),c)))))) = add(iPr_def_11,b),
inference(superposition,[status(thm)],[c_15246,c_249]) ).
tcf(c_23730,plain,
! [X0: $i] : add(multiply(a,add(iPr_def_11,b)),multiply(X0,iPr_def_12)) = multiply(a,add(iPr_def_11,b)),
inference(superposition,[status(thm)],[c_16175,c_242]) ).
tcf(c_24008,plain,
! [X0: $i] : multiply(a,add(iPr_def_11,add(b,multiply(X0,iPr_def_12)))) = multiply(a,add(iPr_def_11,b)),
inference(demodulation,[status(thm)],[c_23730,c_119,c_16308]) ).
tcf(c_24009,plain,
! [X0: $i] : multiply(a,add(iPr_def_11,add(b,multiply(X0,iPr_def_12)))) = iPr_def_12,
inference(light_normalisation,[status(thm)],[c_24008,c_19305]) ).
tcf(c_24061,plain,
add(iPr_def_11,b) = add(iPr_def_14,b),
inference(demodulation,[status(thm)],[c_23473,c_1304,c_1363,c_12808]) ).
tcf(c_24110,plain,
! [X0: $i] : add(iPr_def_11,add(b,X0)) = add(iPr_def_14,add(b,X0)),
inference(demodulation,[status(thm)],[c_23461,c_119,c_13248,c_6388,c_10951]) ).
tcf(c_24931,plain,
! [X0: $i,X1: $i] : add(add(iPr_def_14,b),multiply(X0,multiply(X1,add(b,multiply(add(iPr_def_11,b),c))))) = add(iPr_def_14,b),
inference(superposition,[status(thm)],[c_17874,c_238]) ).
tcf(c_25686,plain,
! [X0: $i,X1: $i] : add(iPr_def_11,add(b,multiply(X0,multiply(X1,add(b,multiply(add(iPr_def_11,b),c)))))) = add(iPr_def_14,b),
inference(demodulation,[status(thm)],[c_24931,c_119,c_24110]) ).
tcf(c_25687,plain,
! [X0: $i,X1: $i] : add(iPr_def_11,add(b,multiply(X0,multiply(X1,add(b,multiply(add(iPr_def_11,b),c)))))) = add(iPr_def_11,b),
inference(light_normalisation,[status(thm)],[c_25686,c_24061]) ).
tcf(c_29854,plain,
$false,
inference(smt_impl_just,[status(thm)],[c_25687,c_25686,c_24009,c_24008,c_14850,c_14849,c_117]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : BOO031-1 : TPTP v9.3.1. Released v2.2.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.11/0.38 % Computer : n017.cluster.edu
% 0.11/0.38 % Model : x86_64 x86_64
% 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.38 % Memory : 8046.5625MB
% 0.11/0.38 % OS : Linux 6.8.0-71-generic
% 0.11/0.38 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.38 % DateTime : Fri Sep 25 06:31:31 UTC 2026
% 0.11/0.39 % CPUTime :
% 0.11/0.39 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.11/0.42 Running UEQ theorem proving
% 0.11/0.42 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.11/0.44
% 0.11/0.44 % ======== iProver multi-core TPTP/SMT =========
% 0.11/0.44
% 0.11/0.44 % Detected problem language: tptp
% 0.11/0.45 % Proving...
% 210.30/29.42 WARNING - Clausifier option not provided in the heuristic config "heur/vip2_118404", setting default options.
% 210.30/29.42 % SZS status Started for theBenchmark.p
% 210.30/29.42 % SZS status Unsatisfiable for theBenchmark.p
% 210.30/29.42
% 210.30/29.42 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 210.30/29.42
% 210.30/29.42 % ------ iProver source info
% 210.30/29.42
% 210.30/29.42 % git: date: 2026-07-19 20:42:38 +0200
% 210.30/29.42 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 210.30/29.42 % git: non_committed_changes: false
% 210.30/29.42
% 210.30/29.42 % ------ Parsing...% successful
% 210.30/29.42
% 210.30/29.42
% 210.30/29.42 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 210.30/29.42
% 210.30/29.42 % ------ Preprocessing... sup_sim: 0 sf_s rm: 0 0s sf_e pe_s pe_e %
% 210.30/29.42
% 210.30/29.42 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 210.30/29.42
% 210.30/29.42 % ------ Preprocessing... sf_s rm: 0 0s sf_e
% 210.30/29.42 % ------ Proving...
% 210.30/29.42 % ------ Problem Properties
% 210.30/29.42
% 210.30/29.42 %
% 210.30/29.42 % clauses 17
% 210.30/29.42 % conjectures 1
% 210.30/29.42 % EPR 1
% 210.30/29.42 % Horn 17
% 210.30/29.42 % unary 17
% 210.30/29.42 % binary 0
% 210.30/29.42 % lits 17
% 210.30/29.42 % lits eq 17
% 210.30/29.42 % fd_pure 0
% 210.30/29.42 % fd_pseudo 0
% 210.30/29.42 % fd_cond 0
% 210.30/29.42 % fd_pseudo_cond 0
% 210.30/29.42 % AC symbols 0
% 210.30/29.42
% 210.30/29.42 % ------ Input Options Time Limit: Unbounded
% 210.30/29.42
% 210.30/29.42
% 210.30/29.42 % ------
% 210.30/29.42 % Current options:
% 210.30/29.42 % ------
% 210.30/29.42
% 210.30/29.42
% 210.30/29.42 %
% 210.30/29.42
% 210.30/29.42 % ------ Proving...
% 210.30/29.42 %
% 210.30/29.42
% 210.30/29.42 % SZS status Unsatisfiable for theBenchmark.p
% 210.30/29.42
% 210.30/29.42 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 210.30/29.42
% 210.30/29.42
%------------------------------------------------------------------------------