%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : KLE101+1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% Computer : n002.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:52:24 PM UTC 2026
% Result : Theorem 77.64s 19.48s
% Output : CNFRefutation 77.64s
% Verified :
% SZS Type : Refutation
% Derivation depth : 63
% Number of leaves : 38
% Syntax : Number of formulae : 490 ( 486 unt; 16 def)
% Number of atoms : 1545 ( 493 equ)
% Maximal formula atoms : 2 ( 3 avg)
% Number of connectives : 12 ( 8 ~; 0 |; 2 &)
% ( 0 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 2 avg)
% Maximal term depth : 9 ( 2 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 18 ( 16 usr; 17 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 5 con; 0-2 aty)
% Number of variables : 373 ( 0 sgn 370 !; 3 ?; 292 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] : addition(X0,X1) = addition(X1,X0),
file('/export/starexec/sandbox/benchmark/Axioms/KLE001+0.ax',additive_commutativity) ).
fof(f2,axiom,
! [X0,X1,X2] : addition(X2,addition(X1,X0)) = addition(addition(X2,X1),X0),
file('/export/starexec/sandbox/benchmark/Axioms/KLE001+0.ax',additive_associativity) ).
fof(f3,axiom,
! [X0] : addition(X0,zero) = X0,
file('/export/starexec/sandbox/benchmark/Axioms/KLE001+0.ax',additive_identity) ).
fof(f4,axiom,
! [X0] : addition(X0,X0) = X0,
file('/export/starexec/sandbox/benchmark/Axioms/KLE001+0.ax',additive_idempotence) ).
fof(f5,axiom,
! [X0,X1,X2] : multiplication(X0,multiplication(X1,X2)) = multiplication(multiplication(X0,X1),X2),
file('/export/starexec/sandbox/benchmark/Axioms/KLE001+0.ax',multiplicative_associativity) ).
fof(f6,axiom,
! [X0] : multiplication(X0,one) = X0,
file('/export/starexec/sandbox/benchmark/Axioms/KLE001+0.ax',multiplicative_right_identity) ).
fof(f7,axiom,
! [X0] : multiplication(one,X0) = X0,
file('/export/starexec/sandbox/benchmark/Axioms/KLE001+0.ax',multiplicative_left_identity) ).
fof(f8,axiom,
! [X0,X1,X2] : multiplication(X0,addition(X1,X2)) = addition(multiplication(X0,X1),multiplication(X0,X2)),
file('/export/starexec/sandbox/benchmark/Axioms/KLE001+0.ax',right_distributivity) ).
fof(f9,axiom,
! [X0,X1,X2] : multiplication(addition(X0,X1),X2) = addition(multiplication(X0,X2),multiplication(X1,X2)),
file('/export/starexec/sandbox/benchmark/Axioms/KLE001+0.ax',left_distributivity) ).
fof(f10,axiom,
! [X0] : multiplication(X0,zero) = zero,
file('/export/starexec/sandbox/benchmark/Axioms/KLE001+0.ax',right_annihilation) ).
fof(f11,axiom,
! [X0] : multiplication(zero,X0) = zero,
file('/export/starexec/sandbox/benchmark/Axioms/KLE001+0.ax',left_annihilation) ).
fof(f13,axiom,
! [X0] : multiplication(antidomain(X0),X0) = zero,
file('/export/starexec/sandbox/benchmark/Axioms/KLE001+4.ax',domain1) ).
fof(f14,axiom,
! [X0,X1] : addition(antidomain(multiplication(X0,X1)),antidomain(multiplication(X0,antidomain(antidomain(X1))))) = antidomain(multiplication(X0,antidomain(antidomain(X1)))),
file('/export/starexec/sandbox/benchmark/Axioms/KLE001+4.ax',domain2) ).
fof(f15,axiom,
! [X0] : addition(antidomain(antidomain(X0)),antidomain(X0)) = one,
file('/export/starexec/sandbox/benchmark/Axioms/KLE001+4.ax',domain3) ).
fof(f16,axiom,
! [X0] : domain(X0) = antidomain(antidomain(X0)),
file('/export/starexec/sandbox/benchmark/Axioms/KLE001+4.ax',domain4) ).
fof(f17,axiom,
! [X0] : multiplication(X0,coantidomain(X0)) = zero,
file('/export/starexec/sandbox/benchmark/Axioms/KLE001+4.ax',codomain1) ).
fof(f18,axiom,
! [X0,X1] : addition(coantidomain(multiplication(X0,X1)),coantidomain(multiplication(coantidomain(coantidomain(X0)),X1))) = coantidomain(multiplication(coantidomain(coantidomain(X0)),X1)),
file('/export/starexec/sandbox/benchmark/Axioms/KLE001+4.ax',codomain2) ).
fof(f19,axiom,
! [X0] : addition(coantidomain(coantidomain(X0)),coantidomain(X0)) = one,
file('/export/starexec/sandbox/benchmark/Axioms/KLE001+4.ax',codomain3) ).
fof(f20,axiom,
! [X0] : codomain(X0) = coantidomain(coantidomain(X0)),
file('/export/starexec/sandbox/benchmark/Axioms/KLE001+4.ax',codomain4) ).
fof(f23,axiom,
! [X0,X1] : forward_diamond(X0,X1) = domain(multiplication(X0,domain(X1))),
file('/export/starexec/sandbox/benchmark/Axioms/KLE001+6.ax',forward_diamond) ).
fof(f24,axiom,
! [X0,X1] : backward_diamond(X0,X1) = codomain(multiplication(codomain(X1),X0)),
file('/export/starexec/sandbox/benchmark/Axioms/KLE001+6.ax',backward_diamond) ).
fof(f27,conjecture,
! [X0,X1,X2] :
( multiplication(forward_diamond(X0,domain(X1)),domain(X2)) = zero
=> multiplication(domain(X1),backward_diamond(X0,domain(X2))) = zero ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goals) ).
fof(f28,negated_conjecture,
~ ! [X0,X1,X2] :
( multiplication(forward_diamond(X0,domain(X1)),domain(X2)) = zero
=> multiplication(domain(X1),backward_diamond(X0,domain(X2))) = zero ),
inference(negated_conjecture,[status(cth)],[f27]) ).
fof(f29,plain,
? [X0,X1,X2] :
( multiplication(forward_diamond(X0,domain(X1)),domain(X2)) = zero
& zero != multiplication(domain(X1),backward_diamond(X0,domain(X2))) ),
inference(ennf_transformation,[],[f28]) ).
fof(f30,plain,
( zero = multiplication(forward_diamond(sK0,domain(sK1)),domain(sK2))
& zero != multiplication(domain(sK1),backward_diamond(sK0,domain(sK2))) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2]),skolemize(X0,sK0),skolemize(X1,sK1),skolemize(X2,sK2)],[f29]) ).
fof(f31,plain,
! [X0,X1] : addition(X0,X1) = addition(X1,X0),
inference(cnf_transformation,[],[f1]) ).
fof(f32,plain,
! [X2,X0,X1] : addition(X2,addition(X1,X0)) = addition(addition(X2,X1),X0),
inference(cnf_transformation,[],[f2]) ).
fof(f33,plain,
! [X0] : addition(X0,zero) = X0,
inference(cnf_transformation,[],[f3]) ).
fof(f34,plain,
! [X0] : addition(X0,X0) = X0,
inference(cnf_transformation,[],[f4]) ).
fof(f35,plain,
! [X2,X0,X1] : multiplication(X0,multiplication(X1,X2)) = multiplication(multiplication(X0,X1),X2),
inference(cnf_transformation,[],[f5]) ).
fof(f36,plain,
! [X0] : multiplication(X0,one) = X0,
inference(cnf_transformation,[],[f6]) ).
fof(f37,plain,
! [X0] : multiplication(one,X0) = X0,
inference(cnf_transformation,[],[f7]) ).
fof(f38,plain,
! [X2,X0,X1] : multiplication(X0,addition(X1,X2)) = addition(multiplication(X0,X1),multiplication(X0,X2)),
inference(cnf_transformation,[],[f8]) ).
fof(f39,plain,
! [X2,X0,X1] : multiplication(addition(X0,X1),X2) = addition(multiplication(X0,X2),multiplication(X1,X2)),
inference(cnf_transformation,[],[f9]) ).
fof(f40,plain,
! [X0] : zero = multiplication(X0,zero),
inference(cnf_transformation,[],[f10]) ).
fof(f41,plain,
! [X0] : zero = multiplication(zero,X0),
inference(cnf_transformation,[],[f11]) ).
fof(f42,plain,
! [X0] : zero = multiplication(antidomain(X0),X0),
inference(cnf_transformation,[],[f13]) ).
fof(f43,plain,
! [X0,X1] : antidomain(multiplication(X0,antidomain(antidomain(X1)))) = addition(antidomain(multiplication(X0,X1)),antidomain(multiplication(X0,antidomain(antidomain(X1))))),
inference(cnf_transformation,[],[f14]) ).
fof(f44,plain,
! [X0] : one = addition(antidomain(antidomain(X0)),antidomain(X0)),
inference(cnf_transformation,[],[f15]) ).
fof(f45,plain,
! [X0] : antidomain(antidomain(X0)) = domain(X0),
inference(cnf_transformation,[],[f16]) ).
fof(f46,plain,
! [X0] : zero = multiplication(X0,coantidomain(X0)),
inference(cnf_transformation,[],[f17]) ).
fof(f47,plain,
! [X0,X1] : coantidomain(multiplication(coantidomain(coantidomain(X0)),X1)) = addition(coantidomain(multiplication(X0,X1)),coantidomain(multiplication(coantidomain(coantidomain(X0)),X1))),
inference(cnf_transformation,[],[f18]) ).
fof(f48,plain,
! [X0] : one = addition(coantidomain(coantidomain(X0)),coantidomain(X0)),
inference(cnf_transformation,[],[f19]) ).
fof(f49,plain,
! [X0] : coantidomain(coantidomain(X0)) = codomain(X0),
inference(cnf_transformation,[],[f20]) ).
fof(f52,plain,
! [X0,X1] : forward_diamond(X0,X1) = domain(multiplication(X0,domain(X1))),
inference(cnf_transformation,[],[f23]) ).
fof(f53,plain,
! [X0,X1] : backward_diamond(X0,X1) = codomain(multiplication(codomain(X1),X0)),
inference(cnf_transformation,[],[f24]) ).
fof(f56,plain,
zero = multiplication(forward_diamond(sK0,domain(sK1)),domain(sK2)),
inference(cnf_transformation,[],[f30]) ).
fof(f57,plain,
zero != multiplication(domain(sK1),backward_diamond(sK0,domain(sK2))),
inference(cnf_transformation,[],[f30]) ).
fof(f59,plain,
! [X0,X1] : backward_diamond(X0,X1) = coantidomain(coantidomain(multiplication(coantidomain(coantidomain(X1)),X0))),
inference(definition_unfolding,[],[f53,f49,f49]) ).
fof(f62,plain,
! [X0,X1] : forward_diamond(X0,X1) = antidomain(antidomain(multiplication(X0,antidomain(antidomain(X1))))),
inference(definition_unfolding,[],[f52,f45,f45]) ).
fof(f64,plain,
zero != multiplication(antidomain(antidomain(sK1)),coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(sK2)))),sK0)))),
inference(definition_unfolding,[],[f57,f45,f59,f45]) ).
fof(f65,plain,
zero = multiplication(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(sK1))))))),antidomain(antidomain(sK2))),
inference(definition_unfolding,[],[f56,f62,f45,f45]) ).
tcf(c_49,plain,
! [X0: $i,X1: $i] : addition(X0,X1) = addition(X1,X0),
inference(cnf_transformation,[],[f31]) ).
tcf(c_50,plain,
! [X0: $i,X1: $i,X2: $i] : addition(addition(X0,X1),X2) = addition(X0,addition(X1,X2)),
inference(cnf_transformation,[],[f32]) ).
tcf(c_51,plain,
! [X0: $i] : addition(X0,zero) = X0,
inference(cnf_transformation,[],[f33]) ).
tcf(c_52,plain,
! [X0: $i] : addition(X0,X0) = X0,
inference(cnf_transformation,[],[f34]) ).
tcf(c_53,plain,
! [X0: $i,X1: $i,X2: $i] : multiplication(multiplication(X0,X1),X2) = multiplication(X0,multiplication(X1,X2)),
inference(cnf_transformation,[],[f35]) ).
tcf(c_54,plain,
! [X0: $i] : multiplication(X0,one) = X0,
inference(cnf_transformation,[],[f36]) ).
tcf(c_55,plain,
! [X0: $i] : multiplication(one,X0) = X0,
inference(cnf_transformation,[],[f37]) ).
tcf(c_56,plain,
! [X0: $i,X1: $i,X2: $i] : addition(multiplication(X0,X1),multiplication(X0,X2)) = multiplication(X0,addition(X1,X2)),
inference(cnf_transformation,[],[f38]) ).
tcf(c_57,plain,
! [X0: $i,X1: $i,X2: $i] : addition(multiplication(X0,X1),multiplication(X2,X1)) = multiplication(addition(X0,X2),X1),
inference(cnf_transformation,[],[f39]) ).
tcf(c_58,plain,
! [X0: $i] : multiplication(X0,zero) = zero,
inference(cnf_transformation,[],[f40]) ).
tcf(c_59,plain,
! [X0: $i] : multiplication(zero,X0) = zero,
inference(cnf_transformation,[],[f41]) ).
tcf(c_60,plain,
! [X0: $i] : multiplication(antidomain(X0),X0) = zero,
inference(cnf_transformation,[],[f42]) ).
tcf(c_61,plain,
! [X0: $i,X1: $i] : addition(antidomain(multiplication(X0,X1)),antidomain(multiplication(X0,antidomain(antidomain(X1))))) = antidomain(multiplication(X0,antidomain(antidomain(X1)))),
inference(cnf_transformation,[],[f43]) ).
tcf(c_62,plain,
! [X0: $i] : addition(antidomain(antidomain(X0)),antidomain(X0)) = one,
inference(cnf_transformation,[],[f44]) ).
tcf(c_63,plain,
! [X0: $i] : multiplication(X0,coantidomain(X0)) = zero,
inference(cnf_transformation,[],[f46]) ).
tcf(c_64,plain,
! [X0: $i,X1: $i] : addition(coantidomain(multiplication(X0,X1)),coantidomain(multiplication(coantidomain(coantidomain(X0)),X1))) = coantidomain(multiplication(coantidomain(coantidomain(X0)),X1)),
inference(cnf_transformation,[],[f47]) ).
tcf(c_65,plain,
! [X0: $i] : addition(coantidomain(coantidomain(X0)),coantidomain(X0)) = one,
inference(cnf_transformation,[],[f48]) ).
tcf(c_66,negated_conjecture,
multiplication(antidomain(antidomain(sK1)),coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(sK2)))),sK0)))) != zero,
inference(cnf_transformation,[],[f64]) ).
tcf(c_67,negated_conjecture,
multiplication(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(sK1))))))),antidomain(antidomain(sK2))) = zero,
inference(cnf_transformation,[],[f65]) ).
tcf(c_83,plain,
! [X0: $i] : addition(antidomain(X0),antidomain(antidomain(X0))) = one,
inference(theory_normalisation,[status(thm)],[c_62,c_50,c_49]) ).
tcf(c_84,plain,
! [X0: $i] : addition(coantidomain(X0),coantidomain(coantidomain(X0))) = one,
inference(theory_normalisation,[status(thm)],[c_65,c_50,c_49]) ).
tcf(c_131,definition,
iPr_def_10 = antidomain(sK1),
introduced(definition,[new_symbols(definition,[iPr_def_10])],[]) ).
tcf(c_132,definition,
iPr_def_11 = antidomain(iPr_def_10),
introduced(definition,[new_symbols(definition,[iPr_def_11])],[]) ).
tcf(c_133,definition,
iPr_def_12 = antidomain(iPr_def_11),
introduced(definition,[new_symbols(definition,[iPr_def_12])],[]) ).
tcf(c_134,definition,
iPr_def_13 = antidomain(iPr_def_12),
introduced(definition,[new_symbols(definition,[iPr_def_13])],[]) ).
tcf(c_135,definition,
iPr_def_14 = multiplication(sK0,iPr_def_13),
introduced(definition,[new_symbols(definition,[iPr_def_14])],[]) ).
tcf(c_136,definition,
iPr_def_15 = antidomain(iPr_def_14),
introduced(definition,[new_symbols(definition,[iPr_def_15])],[]) ).
tcf(c_137,definition,
iPr_def_16 = antidomain(iPr_def_15),
introduced(definition,[new_symbols(definition,[iPr_def_16])],[]) ).
tcf(c_138,definition,
iPr_def_17 = antidomain(sK2),
introduced(definition,[new_symbols(definition,[iPr_def_17])],[]) ).
tcf(c_139,definition,
iPr_def_18 = antidomain(iPr_def_17),
introduced(definition,[new_symbols(definition,[iPr_def_18])],[]) ).
tcf(c_140,definition,
iPr_def_19 = multiplication(iPr_def_16,iPr_def_18),
introduced(definition,[new_symbols(definition,[iPr_def_19])],[]) ).
tcf(c_141,definition,
iPr_def_20 = coantidomain(iPr_def_18),
introduced(definition,[new_symbols(definition,[iPr_def_20])],[]) ).
tcf(c_142,definition,
iPr_def_21 = coantidomain(iPr_def_20),
introduced(definition,[new_symbols(definition,[iPr_def_21])],[]) ).
tcf(c_143,definition,
iPr_def_22 = multiplication(iPr_def_21,sK0),
introduced(definition,[new_symbols(definition,[iPr_def_22])],[]) ).
tcf(c_144,definition,
iPr_def_23 = coantidomain(iPr_def_22),
introduced(definition,[new_symbols(definition,[iPr_def_23])],[]) ).
tcf(c_145,definition,
iPr_def_24 = coantidomain(iPr_def_23),
introduced(definition,[new_symbols(definition,[iPr_def_24])],[]) ).
tcf(c_146,definition,
iPr_def_25 = multiplication(iPr_def_11,iPr_def_24),
introduced(definition,[new_symbols(definition,[iPr_def_25])],[]) ).
tcf(c_147,negated_conjecture,
iPr_def_19 = zero,
inference(demodulation,[status(thm)],[c_67,c_138,c_139,c_131,c_132,c_133,c_134,c_135,c_136,c_137,c_140]) ).
tcf(c_148,negated_conjecture,
iPr_def_25 != zero,
inference(demodulation,[status(thm)],[c_66,c_141,c_142,c_143,c_144,c_145,c_146]) ).
tcf(c_265,plain,
addition(iPr_def_10,antidomain(iPr_def_10)) = one,
inference(superposition,[status(thm)],[c_131,c_83]) ).
tcf(c_266,plain,
addition(iPr_def_11,antidomain(iPr_def_11)) = one,
inference(superposition,[status(thm)],[c_132,c_83]) ).
tcf(c_267,plain,
addition(iPr_def_12,antidomain(iPr_def_12)) = one,
inference(superposition,[status(thm)],[c_133,c_83]) ).
tcf(c_269,plain,
addition(iPr_def_15,antidomain(iPr_def_15)) = one,
inference(superposition,[status(thm)],[c_136,c_83]) ).
tcf(c_270,plain,
addition(iPr_def_16,antidomain(iPr_def_16)) = one,
inference(superposition,[status(thm)],[c_137,c_83]) ).
tcf(c_271,plain,
addition(iPr_def_15,iPr_def_16) = one,
inference(light_normalisation,[status(thm)],[c_269,c_137]) ).
tcf(c_272,plain,
addition(iPr_def_12,iPr_def_13) = one,
inference(light_normalisation,[status(thm)],[c_267,c_134]) ).
tcf(c_273,plain,
addition(iPr_def_11,iPr_def_12) = one,
inference(light_normalisation,[status(thm)],[c_266,c_133]) ).
tcf(c_274,plain,
addition(iPr_def_10,iPr_def_11) = one,
inference(light_normalisation,[status(thm)],[c_265,c_132]) ).
tcf(c_275,plain,
! [X0: $i] : addition(antidomain(X0),antidomain(antidomain(X0))) = addition(iPr_def_15,iPr_def_16),
inference(demodulation,[status(thm)],[c_83,c_271]) ).
tcf(c_276,plain,
! [X0: $i] : addition(X0,iPr_def_19) = X0,
inference(light_normalisation,[status(thm)],[c_51,c_147]) ).
tcf(c_277,plain,
! [X0: $i] : multiplication(X0,addition(iPr_def_15,iPr_def_16)) = X0,
inference(light_normalisation,[status(thm)],[c_54,c_271]) ).
tcf(c_278,plain,
! [X0: $i] : addition(multiplication(X0,iPr_def_15),multiplication(X0,iPr_def_16)) = X0,
inference(demodulation,[status(thm)],[c_277,c_56]) ).
tcf(c_279,plain,
! [X0: $i] : multiplication(addition(iPr_def_15,iPr_def_16),X0) = X0,
inference(light_normalisation,[status(thm)],[c_55,c_271]) ).
tcf(c_280,plain,
! [X0: $i] : addition(multiplication(iPr_def_15,X0),multiplication(iPr_def_16,X0)) = X0,
inference(demodulation,[status(thm)],[c_279,c_57]) ).
tcf(c_285,plain,
! [X0: $i] : multiplication(iPr_def_19,X0) = iPr_def_19,
inference(light_normalisation,[status(thm)],[c_59,c_147]) ).
tcf(c_300,plain,
addition(multiplication(iPr_def_15,iPr_def_18),iPr_def_19) = iPr_def_18,
inference(superposition,[status(thm)],[c_140,c_280]) ).
tcf(c_301,plain,
addition(iPr_def_19,multiplication(iPr_def_15,iPr_def_18)) = iPr_def_18,
inference(theory_normalisation,[status(thm)],[c_300,c_50,c_49]) ).
tcf(c_302,plain,
addition(iPr_def_12,iPr_def_13) = addition(iPr_def_15,iPr_def_16),
inference(demodulation,[status(thm)],[c_271,c_272]) ).
tcf(c_304,plain,
addition(iPr_def_11,iPr_def_12) = addition(iPr_def_12,iPr_def_13),
inference(demodulation,[status(thm)],[c_272,c_273]) ).
tcf(c_305,plain,
addition(iPr_def_11,iPr_def_12) = addition(iPr_def_15,iPr_def_16),
inference(demodulation,[status(thm)],[c_302,c_304]) ).
tcf(c_306,plain,
addition(iPr_def_10,iPr_def_11) = addition(iPr_def_11,iPr_def_12),
inference(demodulation,[status(thm)],[c_273,c_274]) ).
tcf(c_308,plain,
! [X0: $i] : multiplication(antidomain(X0),X0) = iPr_def_19,
inference(light_normalisation,[status(thm)],[c_60,c_147]) ).
tcf(c_311,plain,
multiplication(iPr_def_11,iPr_def_10) = iPr_def_19,
inference(superposition,[status(thm)],[c_132,c_308]) ).
tcf(c_312,plain,
multiplication(iPr_def_12,iPr_def_11) = iPr_def_19,
inference(superposition,[status(thm)],[c_133,c_308]) ).
tcf(c_315,plain,
multiplication(iPr_def_16,iPr_def_15) = iPr_def_19,
inference(superposition,[status(thm)],[c_137,c_308]) ).
tcf(c_334,plain,
! [X0: $i] : addition(iPr_def_19,X0) = X0,
inference(superposition,[status(thm)],[c_276,c_49]) ).
tcf(c_340,plain,
! [X0: $i,X1: $i] : addition(X0,addition(X0,X1)) = addition(X0,X1),
inference(superposition,[status(thm)],[c_52,c_50]) ).
tcf(c_344,plain,
! [X0: $i,X1: $i] : addition(multiplication(X0,iPr_def_15),addition(multiplication(X0,iPr_def_16),X1)) = addition(X0,X1),
inference(superposition,[status(thm)],[c_278,c_50]) ).
tcf(c_345,plain,
! [X0: $i,X1: $i] : addition(multiplication(iPr_def_15,X0),addition(multiplication(iPr_def_16,X0),X1)) = addition(X0,X1),
inference(superposition,[status(thm)],[c_280,c_50]) ).
tcf(c_366,plain,
! [X0: $i] : multiplication(iPr_def_16,multiplication(iPr_def_15,X0)) = multiplication(iPr_def_19,X0),
inference(superposition,[status(thm)],[c_315,c_53]) ).
tcf(c_371,plain,
! [X0: $i] : multiplication(iPr_def_16,multiplication(iPr_def_15,X0)) = iPr_def_19,
inference(light_normalisation,[status(thm)],[c_366,c_285]) ).
tcf(c_428,plain,
addition(iPr_def_16,antidomain(iPr_def_16)) = addition(iPr_def_10,iPr_def_11),
inference(demodulation,[status(thm)],[c_270,c_274]) ).
tcf(c_440,plain,
! [X0: $i] : addition(multiplication(X0,iPr_def_11),multiplication(X0,iPr_def_12)) = multiplication(X0,addition(iPr_def_10,iPr_def_11)),
inference(superposition,[status(thm)],[c_306,c_56]) ).
tcf(c_443,plain,
! [X0: $i,X1: $i] : addition(multiplication(X0,multiplication(X1,iPr_def_15)),multiplication(X0,multiplication(X1,iPr_def_16))) = multiplication(X0,X1),
inference(superposition,[status(thm)],[c_278,c_56]) ).
tcf(c_444,plain,
! [X0: $i,X1: $i] : addition(multiplication(X0,multiplication(iPr_def_15,X1)),multiplication(X0,multiplication(iPr_def_16,X1))) = multiplication(X0,X1),
inference(superposition,[status(thm)],[c_280,c_56]) ).
tcf(c_447,plain,
! [X0: $i,X1: $i] : addition(multiplication(antidomain(addition(X0,X1)),X0),multiplication(antidomain(addition(X0,X1)),X1)) = iPr_def_19,
inference(superposition,[status(thm)],[c_56,c_308]) ).
tcf(c_471,plain,
! [X0: $i] : addition(multiplication(iPr_def_16,X0),multiplication(antidomain(iPr_def_16),X0)) = multiplication(addition(iPr_def_10,iPr_def_11),X0),
inference(superposition,[status(thm)],[c_428,c_57]) ).
tcf(c_472,plain,
! [X0: $i] : addition(multiplication(iPr_def_11,X0),multiplication(iPr_def_12,X0)) = multiplication(addition(iPr_def_10,iPr_def_11),X0),
inference(superposition,[status(thm)],[c_306,c_57]) ).
tcf(c_619,plain,
multiplication(iPr_def_15,iPr_def_18) = iPr_def_18,
inference(demodulation,[status(thm)],[c_301,c_334]) ).
tcf(c_623,plain,
multiplication(iPr_def_16,iPr_def_18) = iPr_def_19,
inference(superposition,[status(thm)],[c_619,c_371]) ).
tcf(c_704,plain,
! [X0: $i] : addition(antidomain(X0),antidomain(antidomain(X0))) = addition(iPr_def_10,iPr_def_11),
inference(light_normalisation,[status(thm)],[c_275,c_305,c_306]) ).
tcf(c_714,plain,
addition(iPr_def_17,antidomain(iPr_def_17)) = addition(iPr_def_10,iPr_def_11),
inference(superposition,[status(thm)],[c_138,c_704]) ).
tcf(c_727,plain,
addition(iPr_def_10,iPr_def_11) = addition(iPr_def_17,iPr_def_18),
inference(light_normalisation,[status(thm)],[c_714,c_139]) ).
tcf(c_737,plain,
addition(iPr_def_10,iPr_def_11) = addition(iPr_def_15,iPr_def_16),
inference(light_normalisation,[status(thm)],[c_305,c_306]) ).
tcf(c_739,plain,
! [X0: $i] : addition(multiplication(X0,iPr_def_15),multiplication(X0,iPr_def_16)) = multiplication(X0,addition(iPr_def_10,iPr_def_11)),
inference(superposition,[status(thm)],[c_737,c_56]) ).
tcf(c_740,plain,
! [X0: $i] : addition(multiplication(iPr_def_15,X0),multiplication(iPr_def_16,X0)) = multiplication(addition(iPr_def_10,iPr_def_11),X0),
inference(superposition,[status(thm)],[c_737,c_57]) ).
tcf(c_742,plain,
! [X0: $i] : addition(multiplication(iPr_def_11,X0),multiplication(iPr_def_12,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_740,c_280,c_472]) ).
tcf(c_743,plain,
! [X0: $i] : addition(multiplication(X0,iPr_def_11),multiplication(X0,iPr_def_12)) = X0,
inference(light_normalisation,[status(thm)],[c_739,c_278,c_440]) ).
tcf(c_781,plain,
! [X0: $i] : addition(multiplication(X0,iPr_def_17),multiplication(X0,iPr_def_18)) = multiplication(X0,addition(iPr_def_10,iPr_def_11)),
inference(superposition,[status(thm)],[c_727,c_56]) ).
tcf(c_782,plain,
! [X0: $i] : addition(multiplication(iPr_def_17,X0),multiplication(iPr_def_18,X0)) = multiplication(addition(iPr_def_10,iPr_def_11),X0),
inference(superposition,[status(thm)],[c_727,c_57]) ).
tcf(c_784,plain,
! [X0: $i] : addition(multiplication(iPr_def_17,X0),multiplication(iPr_def_18,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_782,c_472,c_742]) ).
tcf(c_785,plain,
! [X0: $i] : addition(multiplication(X0,iPr_def_17),multiplication(X0,iPr_def_18)) = X0,
inference(light_normalisation,[status(thm)],[c_781,c_440,c_743]) ).
tcf(c_1434,plain,
addition(iPr_def_15,addition(iPr_def_10,iPr_def_11)) = addition(iPr_def_10,iPr_def_11),
inference(superposition,[status(thm)],[c_737,c_340]) ).
tcf(c_1467,plain,
addition(iPr_def_10,addition(iPr_def_11,iPr_def_15)) = addition(iPr_def_10,iPr_def_11),
inference(theory_normalisation,[status(thm)],[c_1434,c_50,c_49]) ).
tcf(c_1925,plain,
! [X0: $i] : addition(multiplication(iPr_def_15,X0),multiplication(iPr_def_16,X0)) = addition(X0,multiplication(iPr_def_16,X0)),
inference(superposition,[status(thm)],[c_52,c_345]) ).
tcf(c_1976,plain,
! [X0: $i] : addition(X0,multiplication(iPr_def_16,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_1925,c_280]) ).
tcf(c_2896,plain,
addition(iPr_def_19,multiplication(iPr_def_12,iPr_def_10)) = iPr_def_10,
inference(superposition,[status(thm)],[c_311,c_742]) ).
tcf(c_3142,plain,
multiplication(iPr_def_12,iPr_def_10) = iPr_def_10,
inference(demodulation,[status(thm)],[c_2896,c_334]) ).
tcf(c_5889,plain,
! [X0: $i] : addition(multiplication(iPr_def_17,X0),X0) = X0,
inference(superposition,[status(thm)],[c_784,c_340]) ).
tcf(c_5899,plain,
! [X0: $i] : addition(X0,multiplication(iPr_def_17,X0)) = X0,
inference(theory_normalisation,[status(thm)],[c_5889,c_50,c_49]) ).
tcf(c_5963,plain,
addition(multiplication(iPr_def_16,iPr_def_17),iPr_def_19) = iPr_def_16,
inference(superposition,[status(thm)],[c_623,c_785]) ).
tcf(c_5966,plain,
addition(multiplication(iPr_def_15,iPr_def_17),iPr_def_18) = iPr_def_15,
inference(superposition,[status(thm)],[c_619,c_785]) ).
tcf(c_5969,plain,
! [X0: $i] : addition(multiplication(X0,iPr_def_17),X0) = X0,
inference(superposition,[status(thm)],[c_785,c_340]) ).
tcf(c_5979,plain,
! [X0: $i] : addition(X0,multiplication(X0,iPr_def_17)) = X0,
inference(theory_normalisation,[status(thm)],[c_5969,c_50,c_49]) ).
tcf(c_5980,plain,
addition(iPr_def_18,multiplication(iPr_def_15,iPr_def_17)) = iPr_def_15,
inference(theory_normalisation,[status(thm)],[c_5966,c_50,c_49]) ).
tcf(c_5982,plain,
addition(iPr_def_19,multiplication(iPr_def_16,iPr_def_17)) = iPr_def_16,
inference(theory_normalisation,[status(thm)],[c_5963,c_50,c_49]) ).
tcf(c_6860,plain,
! [X0: $i] : multiplication(X0,addition(iPr_def_10,iPr_def_11)) = X0,
inference(light_normalisation,[status(thm)],[c_440,c_743]) ).
tcf(c_6861,plain,
! [X0: $i] : addition(multiplication(X0,iPr_def_10),multiplication(X0,iPr_def_11)) = X0,
inference(demodulation,[status(thm)],[c_6860,c_56]) ).
tcf(c_6875,plain,
addition(multiplication(iPr_def_12,iPr_def_10),iPr_def_19) = iPr_def_12,
inference(superposition,[status(thm)],[c_312,c_6861]) ).
tcf(c_6897,plain,
addition(iPr_def_19,multiplication(iPr_def_12,iPr_def_10)) = iPr_def_12,
inference(theory_normalisation,[status(thm)],[c_6875,c_50,c_49]) ).
tcf(c_6898,plain,
addition(iPr_def_19,iPr_def_10) = iPr_def_12,
inference(light_normalisation,[status(thm)],[c_6897,c_3142]) ).
tcf(c_6899,plain,
addition(iPr_def_10,iPr_def_19) = iPr_def_12,
inference(theory_normalisation,[status(thm)],[c_6898,c_50,c_49]) ).
tcf(c_7081,plain,
iPr_def_10 = iPr_def_12,
inference(demodulation,[status(thm)],[c_6899,c_276]) ).
tcf(c_7123,plain,
! [X0: $i] : addition(multiplication(iPr_def_11,X0),multiplication(iPr_def_10,X0)) = X0,
inference(demodulation,[status(thm)],[c_742,c_7081]) ).
tcf(c_7136,plain,
! [X0: $i] : addition(multiplication(iPr_def_10,X0),multiplication(iPr_def_11,X0)) = X0,
inference(theory_normalisation,[status(thm)],[c_7123,c_50,c_49]) ).
tcf(c_8465,plain,
! [X0: $i] : addition(multiplication(antidomain(X0),X0),multiplication(antidomain(X0),multiplication(iPr_def_17,X0))) = iPr_def_19,
inference(superposition,[status(thm)],[c_5899,c_447]) ).
tcf(c_8466,plain,
! [X0: $i,X1: $i] : addition(X0,addition(multiplication(iPr_def_17,X0),X1)) = addition(X0,X1),
inference(superposition,[status(thm)],[c_5899,c_50]) ).
tcf(c_8489,plain,
! [X0: $i] : addition(iPr_def_19,multiplication(antidomain(X0),multiplication(iPr_def_17,X0))) = iPr_def_19,
inference(light_normalisation,[status(thm)],[c_8465,c_308]) ).
tcf(c_8532,plain,
! [X0: $i] : multiplication(antidomain(X0),multiplication(iPr_def_17,X0)) = iPr_def_19,
inference(demodulation,[status(thm)],[c_8489,c_334]) ).
tcf(c_8561,plain,
addition(iPr_def_19,multiplication(antidomain(iPr_def_15),multiplication(iPr_def_17,iPr_def_16))) = multiplication(antidomain(iPr_def_15),iPr_def_17),
inference(superposition,[status(thm)],[c_8532,c_443]) ).
tcf(c_8572,plain,
addition(iPr_def_19,multiplication(iPr_def_16,multiplication(iPr_def_17,iPr_def_16))) = multiplication(iPr_def_16,iPr_def_17),
inference(light_normalisation,[status(thm)],[c_8561,c_137]) ).
tcf(c_9310,plain,
addition(iPr_def_18,iPr_def_15) = iPr_def_15,
inference(superposition,[status(thm)],[c_5980,c_340]) ).
tcf(c_9319,plain,
addition(iPr_def_15,iPr_def_18) = iPr_def_15,
inference(theory_normalisation,[status(thm)],[c_9310,c_50,c_49]) ).
tcf(c_9335,plain,
! [X0: $i] : addition(iPr_def_15,addition(iPr_def_18,X0)) = addition(iPr_def_15,X0),
inference(superposition,[status(thm)],[c_9319,c_50]) ).
tcf(c_9345,plain,
multiplication(iPr_def_16,iPr_def_17) = iPr_def_16,
inference(demodulation,[status(thm)],[c_5982,c_334]) ).
tcf(c_9354,plain,
addition(iPr_def_17,iPr_def_16) = iPr_def_17,
inference(superposition,[status(thm)],[c_9345,c_1976]) ).
tcf(c_9360,plain,
addition(iPr_def_16,iPr_def_17) = iPr_def_17,
inference(theory_normalisation,[status(thm)],[c_9354,c_50,c_49]) ).
tcf(c_9793,plain,
! [X0: $i] : addition(multiplication(X0,iPr_def_16),multiplication(X0,iPr_def_17)) = multiplication(X0,iPr_def_17),
inference(superposition,[status(thm)],[c_9360,c_56]) ).
tcf(c_10192,plain,
! [X0: $i] : addition(iPr_def_15,addition(X0,iPr_def_18)) = addition(iPr_def_15,X0),
inference(superposition,[status(thm)],[c_49,c_9335]) ).
tcf(c_10481,plain,
addition(iPr_def_15,addition(iPr_def_10,iPr_def_11)) = addition(iPr_def_15,iPr_def_17),
inference(superposition,[status(thm)],[c_727,c_10192]) ).
tcf(c_10495,plain,
addition(iPr_def_10,addition(iPr_def_11,iPr_def_15)) = addition(iPr_def_15,iPr_def_17),
inference(theory_normalisation,[status(thm)],[c_10481,c_50,c_49]) ).
tcf(c_10496,plain,
addition(iPr_def_10,iPr_def_11) = addition(iPr_def_15,iPr_def_17),
inference(light_normalisation,[status(thm)],[c_10495,c_1467]) ).
tcf(c_14866,plain,
! [X0: $i] : addition(multiplication(iPr_def_16,X0),multiplication(antidomain(iPr_def_16),X0)) = addition(multiplication(iPr_def_11,X0),multiplication(iPr_def_10,X0)),
inference(light_normalisation,[status(thm)],[c_471,c_472,c_7081]) ).
tcf(c_14867,plain,
! [X0: $i] : addition(multiplication(iPr_def_16,X0),multiplication(antidomain(iPr_def_16),X0)) = X0,
inference(demodulation,[status(thm)],[c_14866,c_49,c_7136]) ).
tcf(c_14928,plain,
addition(multiplication(iPr_def_16,multiplication(iPr_def_17,iPr_def_16)),iPr_def_19) = multiplication(iPr_def_17,iPr_def_16),
inference(superposition,[status(thm)],[c_8532,c_14867]) ).
tcf(c_14969,plain,
addition(iPr_def_19,multiplication(iPr_def_16,multiplication(iPr_def_17,iPr_def_16))) = multiplication(iPr_def_17,iPr_def_16),
inference(theory_normalisation,[status(thm)],[c_14928,c_50,c_49]) ).
tcf(c_14970,plain,
multiplication(iPr_def_17,iPr_def_16) = iPr_def_16,
inference(light_normalisation,[status(thm)],[c_14969,c_8572,c_9345]) ).
tcf(c_15221,plain,
! [X0: $i] : multiplication(iPr_def_17,multiplication(iPr_def_16,X0)) = multiplication(iPr_def_16,X0),
inference(superposition,[status(thm)],[c_14970,c_53]) ).
tcf(c_23499,plain,
! [X0: $i] : addition(multiplication(X0,iPr_def_15),multiplication(X0,iPr_def_17)) = multiplication(X0,addition(iPr_def_10,iPr_def_11)),
inference(superposition,[status(thm)],[c_10496,c_56]) ).
tcf(c_36012,plain,
! [X0: $i] : addition(multiplication(iPr_def_15,X0),multiplication(iPr_def_17,multiplication(iPr_def_16,X0))) = addition(multiplication(iPr_def_15,X0),multiplication(iPr_def_17,X0)),
inference(superposition,[status(thm)],[c_444,c_8466]) ).
tcf(c_36220,plain,
! [X0: $i] : addition(multiplication(iPr_def_15,X0),multiplication(iPr_def_17,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_36012,c_280,c_15221]) ).
tcf(c_39445,plain,
! [X0: $i] : addition(multiplication(X0,iPr_def_15),multiplication(X0,iPr_def_17)) = addition(X0,multiplication(X0,iPr_def_17)),
inference(superposition,[status(thm)],[c_9793,c_344]) ).
tcf(c_39470,plain,
! [X0: $i] : addition(multiplication(X0,iPr_def_15),multiplication(X0,iPr_def_17)) = X0,
inference(light_normalisation,[status(thm)],[c_39445,c_5979]) ).
tcf(c_194124,plain,
iPr_def_19 != iPr_def_25,
inference(light_normalisation,[status(thm)],[c_148,c_147]) ).
tcf(c_194125,plain,
! [X0: $i] : multiplication(addition(iPr_def_15,iPr_def_17),X0) = X0,
inference(demodulation,[status(thm)],[c_36220,c_57]) ).
tcf(c_194126,plain,
! [X0: $i] : multiplication(X0,addition(iPr_def_15,iPr_def_17)) = X0,
inference(demodulation,[status(thm)],[c_39470,c_56]) ).
tcf(c_194127,plain,
! [X0: $i] : multiplication(X0,addition(iPr_def_10,iPr_def_11)) = X0,
inference(demodulation,[status(thm)],[c_23499,c_56,c_194126]) ).
tcf(c_194128,plain,
addition(iPr_def_10,iPr_def_11) = addition(iPr_def_15,iPr_def_17),
inference(superposition,[status(thm)],[c_194125,c_194127]) ).
tcf(c_194134,plain,
addition(iPr_def_10,antidomain(iPr_def_10)) = one,
inference(superposition,[status(thm)],[c_131,c_83]) ).
tcf(c_194135,plain,
addition(iPr_def_10,iPr_def_11) = one,
inference(light_normalisation,[status(thm)],[c_194134,c_132]) ).
tcf(c_194137,plain,
addition(iPr_def_15,iPr_def_17) = one,
inference(demodulation,[status(thm)],[c_194128,c_194135]) ).
tcf(c_194147,plain,
addition(iPr_def_17,antidomain(iPr_def_17)) = one,
inference(superposition,[status(thm)],[c_138,c_83]) ).
tcf(c_194148,plain,
addition(iPr_def_17,iPr_def_18) = one,
inference(light_normalisation,[status(thm)],[c_194147,c_139]) ).
tcf(c_194150,plain,
! [X0: $i] : addition(X0,iPr_def_19) = X0,
inference(light_normalisation,[status(thm)],[c_51,c_147]) ).
tcf(c_194155,plain,
addition(iPr_def_20,coantidomain(iPr_def_20)) = one,
inference(superposition,[status(thm)],[c_141,c_84]) ).
tcf(c_194157,plain,
addition(iPr_def_23,coantidomain(iPr_def_23)) = one,
inference(superposition,[status(thm)],[c_144,c_84]) ).
tcf(c_194159,plain,
addition(iPr_def_23,iPr_def_24) = one,
inference(light_normalisation,[status(thm)],[c_194157,c_145]) ).
tcf(c_194160,plain,
addition(iPr_def_20,iPr_def_21) = one,
inference(light_normalisation,[status(thm)],[c_194155,c_142]) ).
tcf(c_194161,plain,
! [X0: $i] : multiplication(X0,iPr_def_19) = iPr_def_19,
inference(light_normalisation,[status(thm)],[c_58,c_147]) ).
tcf(c_194162,plain,
! [X0: $i] : multiplication(iPr_def_19,X0) = iPr_def_19,
inference(light_normalisation,[status(thm)],[c_59,c_147]) ).
tcf(c_194163,plain,
! [X0: $i] : multiplication(antidomain(X0),X0) = iPr_def_19,
inference(light_normalisation,[status(thm)],[c_60,c_147]) ).
tcf(c_194169,plain,
multiplication(iPr_def_13,iPr_def_12) = iPr_def_19,
inference(superposition,[status(thm)],[c_134,c_194163]) ).
tcf(c_194172,plain,
multiplication(iPr_def_18,iPr_def_17) = iPr_def_19,
inference(superposition,[status(thm)],[c_139,c_194163]) ).
tcf(c_194173,plain,
antidomain(one) = iPr_def_19,
inference(superposition,[status(thm)],[c_194163,c_54]) ).
tcf(c_194175,plain,
addition(iPr_def_19,antidomain(iPr_def_19)) = one,
inference(superposition,[status(thm)],[c_194173,c_83]) ).
tcf(c_194176,plain,
! [X0: $i] : multiplication(X0,coantidomain(X0)) = iPr_def_19,
inference(light_normalisation,[status(thm)],[c_63,c_147]) ).
tcf(c_194179,plain,
multiplication(iPr_def_20,iPr_def_21) = iPr_def_19,
inference(superposition,[status(thm)],[c_142,c_194176]) ).
tcf(c_194181,plain,
multiplication(iPr_def_23,iPr_def_24) = iPr_def_19,
inference(superposition,[status(thm)],[c_145,c_194176]) ).
tcf(c_194182,plain,
coantidomain(one) = iPr_def_19,
inference(superposition,[status(thm)],[c_194176,c_55]) ).
tcf(c_194183,plain,
! [X0: $i] : addition(iPr_def_19,X0) = X0,
inference(superposition,[status(thm)],[c_194150,c_49]) ).
tcf(c_194189,plain,
! [X0: $i,X1: $i] : addition(X0,addition(X0,X1)) = addition(X0,X1),
inference(superposition,[status(thm)],[c_52,c_50]) ).
tcf(c_194190,plain,
! [X0: $i,X1: $i] : addition(antidomain(X0),addition(antidomain(antidomain(X0)),X1)) = addition(one,X1),
inference(superposition,[status(thm)],[c_83,c_50]) ).
tcf(c_194191,plain,
! [X0: $i,X1: $i] : addition(coantidomain(X0),addition(coantidomain(coantidomain(X0)),X1)) = addition(one,X1),
inference(superposition,[status(thm)],[c_84,c_50]) ).
tcf(c_194196,plain,
! [X0: $i] : addition(iPr_def_10,addition(iPr_def_11,X0)) = addition(one,X0),
inference(superposition,[status(thm)],[c_194135,c_50]) ).
tcf(c_194209,plain,
! [X0: $i,X1: $i] : multiplication(antidomain(X0),multiplication(X0,X1)) = multiplication(iPr_def_19,X1),
inference(superposition,[status(thm)],[c_194163,c_53]) ).
tcf(c_194210,plain,
! [X0: $i,X1: $i] : multiplication(X0,multiplication(coantidomain(X0),X1)) = multiplication(iPr_def_19,X1),
inference(superposition,[status(thm)],[c_194176,c_53]) ).
tcf(c_194213,plain,
! [X0: $i] : multiplication(iPr_def_21,multiplication(sK0,X0)) = multiplication(iPr_def_22,X0),
inference(superposition,[status(thm)],[c_143,c_53]) ).
tcf(c_194214,plain,
! [X0: $i] : multiplication(iPr_def_11,multiplication(iPr_def_24,X0)) = multiplication(iPr_def_25,X0),
inference(superposition,[status(thm)],[c_146,c_53]) ).
tcf(c_194218,plain,
! [X0: $i,X1: $i] : multiplication(X0,multiplication(X1,coantidomain(multiplication(X0,X1)))) = iPr_def_19,
inference(superposition,[status(thm)],[c_53,c_194176]) ).
tcf(c_194222,plain,
addition(iPr_def_19,coantidomain(iPr_def_19)) = one,
inference(superposition,[status(thm)],[c_194182,c_84]) ).
tcf(c_194231,plain,
! [X0: $i] : multiplication(iPr_def_13,multiplication(iPr_def_12,X0)) = multiplication(iPr_def_19,X0),
inference(superposition,[status(thm)],[c_194169,c_53]) ).
tcf(c_194232,plain,
! [X0: $i] : multiplication(iPr_def_13,multiplication(iPr_def_12,X0)) = iPr_def_19,
inference(light_normalisation,[status(thm)],[c_194231,c_194162]) ).
tcf(c_194250,plain,
! [X0: $i,X1: $i] : addition(X0,multiplication(X0,X1)) = multiplication(X0,addition(one,X1)),
inference(superposition,[status(thm)],[c_54,c_56]) ).
tcf(c_194252,plain,
! [X0: $i,X1: $i] : multiplication(antidomain(X0),addition(X0,X1)) = addition(iPr_def_19,multiplication(antidomain(X0),X1)),
inference(superposition,[status(thm)],[c_194163,c_56]) ).
tcf(c_194253,plain,
! [X0: $i,X1: $i] : multiplication(X0,addition(coantidomain(X0),X1)) = addition(iPr_def_19,multiplication(X0,X1)),
inference(superposition,[status(thm)],[c_194176,c_56]) ).
tcf(c_194264,plain,
! [X0: $i] : addition(iPr_def_19,multiplication(iPr_def_13,X0)) = multiplication(iPr_def_13,addition(iPr_def_12,X0)),
inference(superposition,[status(thm)],[c_194169,c_56]) ).
tcf(c_194280,plain,
! [X0: $i,X1: $i] : addition(multiplication(X0,X1),iPr_def_19) = multiplication(X0,addition(X1,iPr_def_19)),
inference(superposition,[status(thm)],[c_194161,c_56]) ).
tcf(c_194310,plain,
! [X0: $i,X1: $i] : addition(iPr_def_19,multiplication(X0,X1)) = multiplication(X0,addition(X1,iPr_def_19)),
inference(theory_normalisation,[status(thm)],[c_194280,c_50,c_49]) ).
tcf(c_194323,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : addition(multiplication(X0,multiplication(X1,X2)),multiplication(X3,X2)) = multiplication(addition(multiplication(X0,X1),X3),X2),
inference(superposition,[status(thm)],[c_53,c_57]) ).
tcf(c_194325,plain,
! [X0: $i,X1: $i] : addition(X0,multiplication(X1,X0)) = multiplication(addition(one,X1),X0),
inference(superposition,[status(thm)],[c_55,c_57]) ).
tcf(c_194326,plain,
! [X0: $i,X1: $i] : multiplication(addition(antidomain(X0),X1),X0) = addition(iPr_def_19,multiplication(X1,X0)),
inference(superposition,[status(thm)],[c_194163,c_57]) ).
tcf(c_194327,plain,
! [X0: $i,X1: $i] : multiplication(addition(X0,X1),coantidomain(X0)) = addition(iPr_def_19,multiplication(X1,coantidomain(X0))),
inference(superposition,[status(thm)],[c_194176,c_57]) ).
tcf(c_194341,plain,
! [X0: $i] : addition(iPr_def_19,multiplication(X0,iPr_def_17)) = multiplication(addition(iPr_def_18,X0),iPr_def_17),
inference(superposition,[status(thm)],[c_194172,c_57]) ).
tcf(c_194399,plain,
! [X0: $i,X1: $i,X2: $i] : addition(antidomain(multiplication(X0,multiplication(X1,X2))),antidomain(multiplication(multiplication(X0,X1),antidomain(antidomain(X2))))) = antidomain(multiplication(multiplication(X0,X1),antidomain(antidomain(X2)))),
inference(superposition,[status(thm)],[c_53,c_61]) ).
tcf(c_194402,plain,
! [X0: $i] : addition(antidomain(iPr_def_19),antidomain(multiplication(antidomain(X0),antidomain(antidomain(X0))))) = antidomain(multiplication(antidomain(X0),antidomain(antidomain(X0)))),
inference(superposition,[status(thm)],[c_194163,c_61]) ).
tcf(c_194457,plain,
! [X0: $i,X1: $i,X2: $i] : addition(coantidomain(multiplication(X0,multiplication(X1,X2))),coantidomain(multiplication(coantidomain(coantidomain(multiplication(X0,X1))),X2))) = coantidomain(multiplication(coantidomain(coantidomain(multiplication(X0,X1))),X2)),
inference(superposition,[status(thm)],[c_53,c_64]) ).
tcf(c_194460,plain,
! [X0: $i] : addition(coantidomain(iPr_def_19),coantidomain(multiplication(coantidomain(coantidomain(antidomain(X0))),X0))) = coantidomain(multiplication(coantidomain(coantidomain(antidomain(X0))),X0)),
inference(superposition,[status(thm)],[c_194163,c_64]) ).
tcf(c_194461,plain,
! [X0: $i] : addition(coantidomain(iPr_def_19),coantidomain(multiplication(coantidomain(coantidomain(X0)),coantidomain(X0)))) = coantidomain(multiplication(coantidomain(coantidomain(X0)),coantidomain(X0))),
inference(superposition,[status(thm)],[c_194176,c_64]) ).
tcf(c_194641,plain,
antidomain(iPr_def_19) = one,
inference(demodulation,[status(thm)],[c_194175,c_194183]) ).
tcf(c_194647,plain,
coantidomain(iPr_def_19) = one,
inference(demodulation,[status(thm)],[c_194222,c_194183]) ).
tcf(c_194790,plain,
! [X0: $i] : addition(antidomain(X0),antidomain(antidomain(X0))) = addition(one,antidomain(antidomain(X0))),
inference(superposition,[status(thm)],[c_52,c_194190]) ).
tcf(c_194816,plain,
! [X0: $i] : addition(one,antidomain(antidomain(X0))) = one,
inference(light_normalisation,[status(thm)],[c_194790,c_83]) ).
tcf(c_194836,plain,
addition(one,antidomain(iPr_def_17)) = one,
inference(superposition,[status(thm)],[c_138,c_194816]) ).
tcf(c_194853,plain,
addition(one,iPr_def_18) = one,
inference(light_normalisation,[status(thm)],[c_194836,c_139]) ).
tcf(c_194854,plain,
addition(iPr_def_18,one) = one,
inference(theory_normalisation,[status(thm)],[c_194853,c_50,c_49]) ).
tcf(c_194884,plain,
! [X0: $i,X1: $i] : multiplication(antidomain(X0),multiplication(X0,X1)) = iPr_def_19,
inference(demodulation,[status(thm)],[c_194209,c_194162]) ).
tcf(c_194961,plain,
! [X0: $i,X1: $i] : multiplication(X0,multiplication(coantidomain(X0),X1)) = iPr_def_19,
inference(demodulation,[status(thm)],[c_194210,c_194162]) ).
tcf(c_195158,plain,
! [X0: $i] : addition(coantidomain(X0),coantidomain(coantidomain(X0))) = addition(one,coantidomain(coantidomain(X0))),
inference(superposition,[status(thm)],[c_52,c_194191]) ).
tcf(c_195177,plain,
! [X0: $i] : addition(one,coantidomain(coantidomain(X0))) = one,
inference(light_normalisation,[status(thm)],[c_195158,c_84]) ).
tcf(c_195234,plain,
addition(one,coantidomain(iPr_def_20)) = one,
inference(superposition,[status(thm)],[c_141,c_195177]) ).
tcf(c_195236,plain,
addition(one,coantidomain(iPr_def_23)) = one,
inference(superposition,[status(thm)],[c_144,c_195177]) ).
tcf(c_195242,plain,
addition(one,iPr_def_24) = one,
inference(light_normalisation,[status(thm)],[c_195236,c_145]) ).
tcf(c_195243,plain,
addition(iPr_def_24,one) = one,
inference(theory_normalisation,[status(thm)],[c_195242,c_50,c_49]) ).
tcf(c_195244,plain,
addition(one,iPr_def_21) = one,
inference(light_normalisation,[status(thm)],[c_195234,c_142]) ).
tcf(c_195245,plain,
addition(iPr_def_21,one) = one,
inference(theory_normalisation,[status(thm)],[c_195244,c_50,c_49]) ).
tcf(c_195295,plain,
! [X0: $i,X1: $i] : multiplication(X0,addition(coantidomain(X0),X1)) = multiplication(X0,X1),
inference(demodulation,[status(thm)],[c_194253,c_194150,c_194310]) ).
tcf(c_195301,plain,
! [X0: $i] : multiplication(X0,coantidomain(coantidomain(X0))) = multiplication(X0,one),
inference(superposition,[status(thm)],[c_84,c_195295]) ).
tcf(c_195305,plain,
! [X0: $i] : multiplication(iPr_def_20,addition(iPr_def_21,X0)) = multiplication(iPr_def_20,X0),
inference(superposition,[status(thm)],[c_142,c_195295]) ).
tcf(c_195307,plain,
! [X0: $i] : multiplication(iPr_def_23,addition(iPr_def_24,X0)) = multiplication(iPr_def_23,X0),
inference(superposition,[status(thm)],[c_145,c_195295]) ).
tcf(c_195345,plain,
! [X0: $i] : multiplication(X0,coantidomain(coantidomain(X0))) = X0,
inference(light_normalisation,[status(thm)],[c_195301,c_54]) ).
tcf(c_195352,plain,
! [X0: $i,X1: $i] : multiplication(addition(antidomain(X0),X1),X0) = multiplication(X1,X0),
inference(demodulation,[status(thm)],[c_194326,c_194150,c_194310]) ).
tcf(c_195357,plain,
! [X0: $i] : multiplication(antidomain(antidomain(X0)),X0) = multiplication(one,X0),
inference(superposition,[status(thm)],[c_83,c_195352]) ).
tcf(c_195365,plain,
! [X0: $i] : multiplication(addition(iPr_def_15,X0),iPr_def_14) = multiplication(X0,iPr_def_14),
inference(superposition,[status(thm)],[c_136,c_195352]) ).
tcf(c_195367,plain,
! [X0: $i] : multiplication(addition(iPr_def_18,X0),iPr_def_17) = multiplication(X0,iPr_def_17),
inference(superposition,[status(thm)],[c_139,c_195352]) ).
tcf(c_195386,plain,
! [X0: $i] : multiplication(antidomain(antidomain(X0)),X0) = X0,
inference(light_normalisation,[status(thm)],[c_195357,c_55]) ).
tcf(c_195392,plain,
! [X0: $i,X1: $i] : multiplication(antidomain(X0),addition(X0,X1)) = multiplication(antidomain(X0),X1),
inference(demodulation,[status(thm)],[c_194252,c_194150,c_194310]) ).
tcf(c_195396,plain,
! [X0: $i] : multiplication(iPr_def_12,addition(iPr_def_11,X0)) = multiplication(iPr_def_12,X0),
inference(superposition,[status(thm)],[c_133,c_195392]) ).
tcf(c_195397,plain,
! [X0: $i] : multiplication(iPr_def_13,addition(iPr_def_12,X0)) = multiplication(iPr_def_13,X0),
inference(superposition,[status(thm)],[c_134,c_195392]) ).
tcf(c_195415,plain,
multiplication(antidomain(iPr_def_10),one) = multiplication(antidomain(iPr_def_10),iPr_def_11),
inference(superposition,[status(thm)],[c_194135,c_195392]) ).
tcf(c_195443,plain,
multiplication(iPr_def_11,one) = multiplication(iPr_def_11,iPr_def_11),
inference(light_normalisation,[status(thm)],[c_195415,c_132]) ).
tcf(c_195472,plain,
! [X0: $i,X1: $i] : multiplication(addition(X0,X1),coantidomain(X0)) = multiplication(X1,coantidomain(X0)),
inference(demodulation,[status(thm)],[c_194327,c_194150,c_194310]) ).
tcf(c_195489,plain,
multiplication(one,coantidomain(iPr_def_23)) = multiplication(iPr_def_24,coantidomain(iPr_def_23)),
inference(superposition,[status(thm)],[c_194159,c_195472]) ).
tcf(c_195493,plain,
multiplication(one,coantidomain(iPr_def_17)) = multiplication(iPr_def_18,coantidomain(iPr_def_17)),
inference(superposition,[status(thm)],[c_194148,c_195472]) ).
tcf(c_195501,plain,
! [X0: $i] : multiplication(addition(iPr_def_18,X0),iPr_def_20) = multiplication(X0,iPr_def_20),
inference(superposition,[status(thm)],[c_141,c_195472]) ).
tcf(c_195504,plain,
! [X0: $i] : multiplication(addition(iPr_def_23,X0),iPr_def_24) = multiplication(X0,iPr_def_24),
inference(superposition,[status(thm)],[c_145,c_195472]) ).
tcf(c_195517,plain,
multiplication(one,iPr_def_24) = multiplication(iPr_def_24,iPr_def_24),
inference(light_normalisation,[status(thm)],[c_195489,c_145]) ).
tcf(c_195558,plain,
multiplication(iPr_def_18,coantidomain(iPr_def_20)) = iPr_def_18,
inference(superposition,[status(thm)],[c_141,c_195345]) ).
tcf(c_195560,plain,
multiplication(iPr_def_22,coantidomain(iPr_def_23)) = iPr_def_22,
inference(superposition,[status(thm)],[c_144,c_195345]) ).
tcf(c_195570,plain,
! [X0: $i,X1: $i] : multiplication(X0,multiplication(coantidomain(coantidomain(X0)),X1)) = multiplication(X0,X1),
inference(superposition,[status(thm)],[c_195345,c_53]) ).
tcf(c_195597,plain,
multiplication(iPr_def_22,iPr_def_24) = iPr_def_22,
inference(light_normalisation,[status(thm)],[c_195560,c_145]) ).
tcf(c_195598,plain,
multiplication(iPr_def_18,iPr_def_21) = iPr_def_18,
inference(light_normalisation,[status(thm)],[c_195558,c_142]) ).
tcf(c_195626,plain,
! [X0: $i] : multiplication(iPr_def_18,multiplication(iPr_def_21,X0)) = multiplication(iPr_def_18,X0),
inference(superposition,[status(thm)],[c_195598,c_53]) ).
tcf(c_195665,plain,
! [X0: $i] : addition(one,antidomain(multiplication(antidomain(X0),antidomain(antidomain(X0))))) = antidomain(multiplication(antidomain(X0),antidomain(antidomain(X0)))),
inference(light_normalisation,[status(thm)],[c_194402,c_194641]) ).
tcf(c_195709,plain,
! [X0: $i] : addition(one,coantidomain(multiplication(coantidomain(coantidomain(antidomain(X0))),X0))) = coantidomain(multiplication(coantidomain(coantidomain(antidomain(X0))),X0)),
inference(light_normalisation,[status(thm)],[c_194460,c_194647]) ).
tcf(c_195728,plain,
! [X0: $i] : addition(one,coantidomain(multiplication(coantidomain(coantidomain(X0)),coantidomain(X0)))) = coantidomain(multiplication(coantidomain(coantidomain(X0)),coantidomain(X0))),
inference(light_normalisation,[status(thm)],[c_194461,c_194647]) ).
tcf(c_195754,plain,
multiplication(antidomain(iPr_def_10),sK1) = sK1,
inference(superposition,[status(thm)],[c_131,c_195386]) ).
tcf(c_195756,plain,
multiplication(antidomain(iPr_def_11),iPr_def_10) = iPr_def_10,
inference(superposition,[status(thm)],[c_132,c_195386]) ).
tcf(c_195757,plain,
multiplication(antidomain(iPr_def_12),iPr_def_11) = iPr_def_11,
inference(superposition,[status(thm)],[c_133,c_195386]) ).
tcf(c_195779,plain,
multiplication(iPr_def_13,iPr_def_11) = iPr_def_11,
inference(light_normalisation,[status(thm)],[c_195757,c_134]) ).
tcf(c_195780,plain,
multiplication(iPr_def_12,iPr_def_10) = iPr_def_10,
inference(light_normalisation,[status(thm)],[c_195756,c_133]) ).
tcf(c_195782,plain,
multiplication(iPr_def_11,sK1) = sK1,
inference(light_normalisation,[status(thm)],[c_195754,c_132]) ).
tcf(c_195826,plain,
multiplication(iPr_def_13,iPr_def_10) = iPr_def_19,
inference(superposition,[status(thm)],[c_195780,c_194232]) ).
tcf(c_195868,plain,
! [X0: $i] : addition(iPr_def_19,multiplication(iPr_def_13,X0)) = multiplication(iPr_def_13,addition(iPr_def_10,X0)),
inference(superposition,[status(thm)],[c_195826,c_56]) ).
tcf(c_196447,plain,
multiplication(iPr_def_21,iPr_def_14) = multiplication(iPr_def_22,iPr_def_13),
inference(superposition,[status(thm)],[c_135,c_194213]) ).
tcf(c_196501,plain,
multiplication(iPr_def_11,iPr_def_11) = iPr_def_11,
inference(demodulation,[status(thm)],[c_195443,c_54]) ).
tcf(c_196508,plain,
! [X0: $i] : multiplication(iPr_def_11,multiplication(iPr_def_11,X0)) = multiplication(iPr_def_11,X0),
inference(superposition,[status(thm)],[c_196501,c_53]) ).
tcf(c_196786,plain,
! [X0: $i] : addition(antidomain(X0),one) = one,
inference(superposition,[status(thm)],[c_83,c_194189]) ).
tcf(c_196787,plain,
! [X0: $i] : addition(coantidomain(X0),one) = one,
inference(superposition,[status(thm)],[c_84,c_194189]) ).
tcf(c_196793,plain,
addition(iPr_def_10,one) = one,
inference(superposition,[status(thm)],[c_194135,c_194189]) ).
tcf(c_196797,plain,
addition(iPr_def_23,one) = one,
inference(superposition,[status(thm)],[c_194159,c_194189]) ).
tcf(c_196798,plain,
addition(iPr_def_20,one) = one,
inference(superposition,[status(thm)],[c_194160,c_194189]) ).
tcf(c_196802,plain,
addition(iPr_def_17,one) = one,
inference(superposition,[status(thm)],[c_194148,c_194189]) ).
tcf(c_196817,plain,
! [X0: $i] : addition(one,coantidomain(X0)) = one,
inference(theory_normalisation,[status(thm)],[c_196787,c_50,c_49]) ).
tcf(c_196818,plain,
! [X0: $i] : addition(one,antidomain(X0)) = one,
inference(theory_normalisation,[status(thm)],[c_196786,c_50,c_49]) ).
tcf(c_196828,plain,
! [X0: $i] : coantidomain(multiplication(coantidomain(coantidomain(antidomain(X0))),X0)) = one,
inference(demodulation,[status(thm)],[c_195709,c_196817]) ).
tcf(c_196829,plain,
! [X0: $i] : coantidomain(multiplication(coantidomain(coantidomain(X0)),coantidomain(X0))) = one,
inference(demodulation,[status(thm)],[c_195728,c_196817]) ).
tcf(c_196830,plain,
! [X0: $i] : antidomain(multiplication(antidomain(X0),antidomain(antidomain(X0)))) = one,
inference(demodulation,[status(thm)],[c_195665,c_196818]) ).
tcf(c_197258,plain,
multiplication(iPr_def_24,iPr_def_24) = iPr_def_24,
inference(demodulation,[status(thm)],[c_195517,c_55]) ).
tcf(c_197268,plain,
multiplication(iPr_def_11,iPr_def_24) = multiplication(iPr_def_25,iPr_def_24),
inference(superposition,[status(thm)],[c_197258,c_194214]) ).
tcf(c_197270,plain,
multiplication(iPr_def_25,iPr_def_24) = iPr_def_25,
inference(light_normalisation,[status(thm)],[c_197268,c_146]) ).
tcf(c_197279,plain,
! [X0: $i] : multiplication(iPr_def_25,multiplication(iPr_def_24,X0)) = multiplication(iPr_def_25,X0),
inference(superposition,[status(thm)],[c_197270,c_53]) ).
tcf(c_197452,plain,
multiplication(iPr_def_11,addition(one,iPr_def_24)) = addition(iPr_def_11,iPr_def_25),
inference(superposition,[status(thm)],[c_146,c_194250]) ).
tcf(c_197643,plain,
multiplication(iPr_def_11,addition(iPr_def_24,one)) = addition(iPr_def_11,iPr_def_25),
inference(theory_normalisation,[status(thm)],[c_197452,c_50,c_49]) ).
tcf(c_197644,plain,
addition(iPr_def_11,iPr_def_25) = multiplication(iPr_def_11,one),
inference(light_normalisation,[status(thm)],[c_197643,c_195243]) ).
tcf(c_197748,plain,
addition(iPr_def_11,iPr_def_25) = iPr_def_11,
inference(demodulation,[status(thm)],[c_197644,c_54]) ).
tcf(c_197753,plain,
addition(one,iPr_def_25) = addition(iPr_def_10,iPr_def_11),
inference(superposition,[status(thm)],[c_197748,c_194196]) ).
tcf(c_197754,plain,
addition(iPr_def_10,iPr_def_11) = addition(iPr_def_25,one),
inference(theory_normalisation,[status(thm)],[c_197753,c_50,c_49]) ).
tcf(c_197755,plain,
addition(iPr_def_25,one) = one,
inference(light_normalisation,[status(thm)],[c_197754,c_194135]) ).
tcf(c_197901,plain,
! [X0: $i] : multiplication(iPr_def_20,addition(X0,iPr_def_21)) = multiplication(iPr_def_20,X0),
inference(superposition,[status(thm)],[c_49,c_195305]) ).
tcf(c_198161,plain,
multiplication(one,iPr_def_14) = multiplication(iPr_def_17,iPr_def_14),
inference(superposition,[status(thm)],[c_194137,c_195365]) ).
tcf(c_198333,plain,
! [X0: $i] : multiplication(addition(X0,iPr_def_18),iPr_def_17) = multiplication(X0,iPr_def_17),
inference(superposition,[status(thm)],[c_49,c_195367]) ).
tcf(c_198453,plain,
! [X0: $i] : multiplication(iPr_def_12,addition(X0,iPr_def_11)) = multiplication(iPr_def_12,X0),
inference(superposition,[status(thm)],[c_49,c_195396]) ).
tcf(c_198727,plain,
! [X0: $i] : multiplication(addition(X0,iPr_def_18),iPr_def_20) = multiplication(X0,iPr_def_20),
inference(superposition,[status(thm)],[c_49,c_195501]) ).
tcf(c_198820,plain,
! [X0: $i] : multiplication(antidomain(addition(iPr_def_23,X0)),multiplication(X0,iPr_def_24)) = iPr_def_19,
inference(superposition,[status(thm)],[c_195504,c_194884]) ).
tcf(c_199355,plain,
multiplication(iPr_def_18,sK0) = multiplication(iPr_def_18,iPr_def_22),
inference(superposition,[status(thm)],[c_143,c_195626]) ).
tcf(c_199441,plain,
multiplication(iPr_def_17,iPr_def_14) = iPr_def_14,
inference(demodulation,[status(thm)],[c_198161,c_55]) ).
tcf(c_199815,plain,
multiplication(iPr_def_18,coantidomain(iPr_def_17)) = coantidomain(iPr_def_17),
inference(demodulation,[status(thm)],[c_195493,c_55]) ).
tcf(c_200303,plain,
multiplication(iPr_def_11,iPr_def_25) = iPr_def_25,
inference(superposition,[status(thm)],[c_146,c_196508]) ).
tcf(c_200510,plain,
! [X0: $i] : multiplication(iPr_def_13,addition(iPr_def_10,X0)) = multiplication(iPr_def_13,X0),
inference(light_normalisation,[status(thm)],[c_194264,c_195397,c_195868]) ).
tcf(c_200513,plain,
multiplication(iPr_def_13,one) = multiplication(iPr_def_13,iPr_def_11),
inference(superposition,[status(thm)],[c_194135,c_200510]) ).
tcf(c_200530,plain,
multiplication(iPr_def_13,one) = iPr_def_11,
inference(light_normalisation,[status(thm)],[c_200513,c_195779]) ).
tcf(c_200657,plain,
iPr_def_11 = iPr_def_13,
inference(demodulation,[status(thm)],[c_200530,c_54]) ).
tcf(c_200691,plain,
multiplication(iPr_def_21,iPr_def_14) = multiplication(iPr_def_22,iPr_def_11),
inference(demodulation,[status(thm)],[c_196447,c_200657]) ).
tcf(c_200712,plain,
antidomain(iPr_def_12) = iPr_def_11,
inference(demodulation,[status(thm)],[c_134,c_200657]) ).
tcf(c_201077,plain,
coantidomain(multiplication(coantidomain(coantidomain(iPr_def_18)),iPr_def_17)) = one,
inference(superposition,[status(thm)],[c_139,c_196828]) ).
tcf(c_201096,plain,
coantidomain(multiplication(iPr_def_21,iPr_def_17)) = one,
inference(light_normalisation,[status(thm)],[c_201077,c_141,c_142]) ).
tcf(c_201114,plain,
multiplication(iPr_def_21,multiplication(iPr_def_17,one)) = iPr_def_19,
inference(superposition,[status(thm)],[c_201096,c_194218]) ).
tcf(c_201213,plain,
multiplication(iPr_def_21,iPr_def_17) = iPr_def_19,
inference(demodulation,[status(thm)],[c_201114,c_54]) ).
tcf(c_201220,plain,
! [X0: $i] : addition(iPr_def_19,multiplication(X0,iPr_def_17)) = multiplication(addition(iPr_def_21,X0),iPr_def_17),
inference(superposition,[status(thm)],[c_201213,c_57]) ).
tcf(c_201222,plain,
! [X0: $i] : multiplication(iPr_def_21,multiplication(iPr_def_17,X0)) = multiplication(iPr_def_19,X0),
inference(superposition,[status(thm)],[c_201213,c_53]) ).
tcf(c_201230,plain,
! [X0: $i] : multiplication(iPr_def_21,multiplication(iPr_def_17,X0)) = iPr_def_19,
inference(light_normalisation,[status(thm)],[c_201222,c_194162]) ).
tcf(c_201235,plain,
! [X0: $i] : multiplication(addition(iPr_def_21,X0),iPr_def_17) = multiplication(X0,iPr_def_17),
inference(light_normalisation,[status(thm)],[c_201220,c_194341,c_195367]) ).
tcf(c_201246,plain,
multiplication(iPr_def_21,iPr_def_14) = iPr_def_19,
inference(superposition,[status(thm)],[c_199441,c_201230]) ).
tcf(c_201537,plain,
multiplication(iPr_def_22,iPr_def_11) = iPr_def_19,
inference(light_normalisation,[status(thm)],[c_200691,c_201246]) ).
tcf(c_201545,plain,
! [X0: $i] : multiplication(iPr_def_22,multiplication(iPr_def_11,X0)) = multiplication(iPr_def_19,X0),
inference(superposition,[status(thm)],[c_201537,c_53]) ).
tcf(c_201551,plain,
! [X0: $i] : multiplication(iPr_def_22,multiplication(iPr_def_11,X0)) = iPr_def_19,
inference(light_normalisation,[status(thm)],[c_201545,c_194162]) ).
tcf(c_201566,plain,
! [X0: $i] : multiplication(iPr_def_22,multiplication(iPr_def_25,X0)) = iPr_def_19,
inference(superposition,[status(thm)],[c_194214,c_201551]) ).
tcf(c_201572,plain,
multiplication(iPr_def_22,iPr_def_25) = iPr_def_19,
inference(superposition,[status(thm)],[c_200303,c_201551]) ).
tcf(c_201573,plain,
multiplication(iPr_def_22,sK1) = iPr_def_19,
inference(superposition,[status(thm)],[c_195782,c_201551]) ).
tcf(c_201872,plain,
coantidomain(multiplication(coantidomain(iPr_def_20),iPr_def_20)) = one,
inference(superposition,[status(thm)],[c_141,c_196829]) ).
tcf(c_201874,plain,
coantidomain(multiplication(coantidomain(iPr_def_23),iPr_def_23)) = one,
inference(superposition,[status(thm)],[c_144,c_196829]) ).
tcf(c_201901,plain,
coantidomain(multiplication(iPr_def_24,iPr_def_23)) = one,
inference(light_normalisation,[status(thm)],[c_201874,c_145]) ).
tcf(c_201902,plain,
coantidomain(multiplication(iPr_def_21,iPr_def_20)) = one,
inference(light_normalisation,[status(thm)],[c_201872,c_142]) ).
tcf(c_201919,plain,
multiplication(iPr_def_24,multiplication(iPr_def_23,one)) = iPr_def_19,
inference(superposition,[status(thm)],[c_201901,c_194218]) ).
tcf(c_201937,plain,
multiplication(iPr_def_21,multiplication(iPr_def_20,one)) = iPr_def_19,
inference(superposition,[status(thm)],[c_201902,c_194218]) ).
tcf(c_201992,plain,
multiplication(iPr_def_24,iPr_def_23) = iPr_def_19,
inference(demodulation,[status(thm)],[c_201919,c_54]) ).
tcf(c_202006,plain,
multiplication(iPr_def_11,iPr_def_19) = multiplication(iPr_def_25,iPr_def_23),
inference(superposition,[status(thm)],[c_201992,c_194214]) ).
tcf(c_202074,plain,
multiplication(iPr_def_21,iPr_def_20) = iPr_def_19,
inference(demodulation,[status(thm)],[c_201937,c_54]) ).
tcf(c_202275,plain,
antidomain(multiplication(iPr_def_10,antidomain(iPr_def_10))) = one,
inference(superposition,[status(thm)],[c_131,c_196830]) ).
tcf(c_202306,plain,
antidomain(multiplication(iPr_def_10,iPr_def_11)) = one,
inference(light_normalisation,[status(thm)],[c_202275,c_132]) ).
tcf(c_202357,plain,
multiplication(one,multiplication(iPr_def_10,iPr_def_11)) = iPr_def_19,
inference(superposition,[status(thm)],[c_202306,c_194163]) ).
tcf(c_202414,plain,
multiplication(iPr_def_10,iPr_def_11) = iPr_def_19,
inference(demodulation,[status(thm)],[c_202357,c_55]) ).
tcf(c_202423,plain,
! [X0: $i] : multiplication(iPr_def_10,multiplication(iPr_def_11,X0)) = multiplication(iPr_def_19,X0),
inference(superposition,[status(thm)],[c_202414,c_53]) ).
tcf(c_202431,plain,
! [X0: $i] : multiplication(iPr_def_10,multiplication(iPr_def_11,X0)) = iPr_def_19,
inference(light_normalisation,[status(thm)],[c_202423,c_194162]) ).
tcf(c_202547,plain,
! [X0: $i] : multiplication(iPr_def_10,multiplication(iPr_def_25,X0)) = iPr_def_19,
inference(superposition,[status(thm)],[c_194214,c_202431]) ).
tcf(c_202553,plain,
multiplication(iPr_def_10,iPr_def_25) = iPr_def_19,
inference(superposition,[status(thm)],[c_200303,c_202431]) ).
tcf(c_202676,plain,
! [X0: $i] : addition(iPr_def_19,multiplication(X0,iPr_def_25)) = multiplication(addition(iPr_def_10,X0),iPr_def_25),
inference(superposition,[status(thm)],[c_202553,c_57]) ).
tcf(c_202782,plain,
multiplication(iPr_def_25,iPr_def_23) = iPr_def_19,
inference(demodulation,[status(thm)],[c_202006,c_194161]) ).
tcf(c_202789,plain,
! [X0: $i] : addition(iPr_def_19,multiplication(iPr_def_25,X0)) = multiplication(iPr_def_25,addition(iPr_def_23,X0)),
inference(superposition,[status(thm)],[c_202782,c_56]) ).
tcf(c_207986,plain,
multiplication(one,iPr_def_17) = multiplication(iPr_def_17,iPr_def_17),
inference(superposition,[status(thm)],[c_194148,c_198333]) ).
tcf(c_208101,plain,
multiplication(iPr_def_17,iPr_def_17) = iPr_def_17,
inference(demodulation,[status(thm)],[c_207986,c_55]) ).
tcf(c_208440,plain,
multiplication(iPr_def_12,one) = multiplication(iPr_def_12,iPr_def_10),
inference(superposition,[status(thm)],[c_194135,c_198453]) ).
tcf(c_208460,plain,
multiplication(iPr_def_12,one) = iPr_def_10,
inference(light_normalisation,[status(thm)],[c_208440,c_195780]) ).
tcf(c_208499,plain,
iPr_def_10 = iPr_def_12,
inference(demodulation,[status(thm)],[c_208460,c_54]) ).
tcf(c_208528,plain,
antidomain(iPr_def_10) = iPr_def_11,
inference(demodulation,[status(thm)],[c_200712,c_208499]) ).
tcf(c_209089,plain,
multiplication(antidomain(addition(iPr_def_23,iPr_def_22)),iPr_def_22) = iPr_def_19,
inference(superposition,[status(thm)],[c_195597,c_198820]) ).
tcf(c_209108,plain,
multiplication(antidomain(addition(iPr_def_22,iPr_def_23)),iPr_def_22) = iPr_def_19,
inference(theory_normalisation,[status(thm)],[c_209089,c_50,c_49]) ).
tcf(c_209581,plain,
multiplication(one,iPr_def_20) = multiplication(iPr_def_17,iPr_def_20),
inference(superposition,[status(thm)],[c_194148,c_198727]) ).
tcf(c_209685,plain,
multiplication(iPr_def_17,iPr_def_20) = iPr_def_20,
inference(demodulation,[status(thm)],[c_209581,c_55]) ).
tcf(c_209687,plain,
multiplication(iPr_def_17,addition(one,iPr_def_20)) = addition(iPr_def_17,iPr_def_20),
inference(superposition,[status(thm)],[c_209685,c_194250]) ).
tcf(c_209706,plain,
multiplication(iPr_def_17,addition(iPr_def_20,one)) = addition(iPr_def_17,iPr_def_20),
inference(theory_normalisation,[status(thm)],[c_209687,c_50,c_49]) ).
tcf(c_209707,plain,
addition(iPr_def_17,iPr_def_20) = multiplication(iPr_def_17,one),
inference(light_normalisation,[status(thm)],[c_209706,c_196798]) ).
tcf(c_209716,plain,
addition(iPr_def_17,iPr_def_20) = iPr_def_17,
inference(demodulation,[status(thm)],[c_209707,c_54]) ).
tcf(c_209720,plain,
! [X0: $i] : addition(iPr_def_17,addition(iPr_def_20,X0)) = addition(iPr_def_17,X0),
inference(superposition,[status(thm)],[c_209716,c_50]) ).
tcf(c_211153,plain,
! [X0: $i] : multiplication(addition(X0,iPr_def_21),iPr_def_17) = multiplication(X0,iPr_def_17),
inference(superposition,[status(thm)],[c_49,c_201235]) ).
tcf(c_213933,plain,
! [X0: $i,X1: $i] : addition(multiplication(X0,iPr_def_19),multiplication(X1,iPr_def_25)) = multiplication(addition(multiplication(X0,iPr_def_22),X1),iPr_def_25),
inference(superposition,[status(thm)],[c_201572,c_194323]) ).
tcf(c_213935,plain,
! [X0: $i,X1: $i,X2: $i] : addition(multiplication(X0,iPr_def_19),multiplication(X1,multiplication(iPr_def_25,X2))) = multiplication(addition(multiplication(X0,iPr_def_22),X1),multiplication(iPr_def_25,X2)),
inference(superposition,[status(thm)],[c_201566,c_194323]) ).
tcf(c_214643,plain,
! [X0: $i,X1: $i] : multiplication(addition(multiplication(X0,iPr_def_22),X1),iPr_def_25) = addition(iPr_def_19,multiplication(X1,iPr_def_25)),
inference(light_normalisation,[status(thm)],[c_213933,c_194161]) ).
tcf(c_214984,plain,
! [X0: $i,X1: $i,X2: $i] : multiplication(addition(multiplication(X0,iPr_def_22),X1),multiplication(iPr_def_25,X2)) = addition(iPr_def_19,multiplication(X1,multiplication(iPr_def_25,X2))),
inference(light_normalisation,[status(thm)],[c_213935,c_194161]) ).
tcf(c_215792,plain,
! [X0: $i,X1: $i] : multiplication(addition(multiplication(X0,iPr_def_22),X1),iPr_def_25) = multiplication(addition(iPr_def_10,X1),iPr_def_25),
inference(demodulation,[status(thm)],[c_214643,c_202676]) ).
tcf(c_215817,plain,
! [X0: $i] : multiplication(addition(iPr_def_10,X0),iPr_def_25) = multiplication(addition(iPr_def_19,X0),iPr_def_25),
inference(superposition,[status(thm)],[c_209108,c_215792]) ).
tcf(c_215828,plain,
! [X0: $i,X1: $i,X2: $i] : multiplication(addition(multiplication(X0,iPr_def_22),X1),multiplication(iPr_def_25,X2)) = multiplication(multiplication(addition(iPr_def_10,X1),iPr_def_25),X2),
inference(superposition,[status(thm)],[c_215792,c_53]) ).
tcf(c_215834,plain,
! [X0: $i] : multiplication(addition(iPr_def_10,X0),iPr_def_25) = multiplication(X0,iPr_def_25),
inference(light_normalisation,[status(thm)],[c_215817,c_194183]) ).
tcf(c_216526,plain,
multiplication(addition(one,iPr_def_21),iPr_def_20) = addition(iPr_def_20,iPr_def_19),
inference(superposition,[status(thm)],[c_202074,c_194325]) ).
tcf(c_216579,plain,
multiplication(addition(one,iPr_def_17),iPr_def_17) = addition(iPr_def_17,iPr_def_17),
inference(superposition,[status(thm)],[c_208101,c_194325]) ).
tcf(c_216597,plain,
! [X0: $i] : multiplication(addition(one,iPr_def_10),multiplication(iPr_def_25,X0)) = addition(multiplication(iPr_def_25,X0),iPr_def_19),
inference(superposition,[status(thm)],[c_202547,c_194325]) ).
tcf(c_216629,plain,
multiplication(addition(one,iPr_def_25),iPr_def_24) = addition(iPr_def_24,iPr_def_25),
inference(superposition,[status(thm)],[c_197270,c_194325]) ).
tcf(c_216638,plain,
multiplication(addition(one,iPr_def_18),iPr_def_21) = addition(iPr_def_21,iPr_def_18),
inference(superposition,[status(thm)],[c_195598,c_194325]) ).
tcf(c_216930,plain,
multiplication(addition(iPr_def_18,one),iPr_def_21) = addition(iPr_def_18,iPr_def_21),
inference(theory_normalisation,[status(thm)],[c_216638,c_50,c_49]) ).
tcf(c_216931,plain,
addition(iPr_def_18,iPr_def_21) = multiplication(one,iPr_def_21),
inference(light_normalisation,[status(thm)],[c_216930,c_194854]) ).
tcf(c_216934,plain,
multiplication(addition(iPr_def_25,one),iPr_def_24) = addition(iPr_def_24,iPr_def_25),
inference(theory_normalisation,[status(thm)],[c_216629,c_50,c_49]) ).
tcf(c_216935,plain,
addition(iPr_def_24,iPr_def_25) = multiplication(one,iPr_def_24),
inference(light_normalisation,[status(thm)],[c_216934,c_197755]) ).
tcf(c_216959,plain,
multiplication(addition(iPr_def_17,one),iPr_def_17) = addition(iPr_def_17,iPr_def_17),
inference(theory_normalisation,[status(thm)],[c_216579,c_50,c_49]) ).
tcf(c_216960,plain,
addition(iPr_def_17,iPr_def_17) = multiplication(one,iPr_def_17),
inference(light_normalisation,[status(thm)],[c_216959,c_196802]) ).
tcf(c_216984,plain,
multiplication(addition(iPr_def_21,one),iPr_def_20) = addition(iPr_def_19,iPr_def_20),
inference(theory_normalisation,[status(thm)],[c_216526,c_50,c_49]) ).
tcf(c_216985,plain,
addition(iPr_def_19,iPr_def_20) = multiplication(one,iPr_def_20),
inference(light_normalisation,[status(thm)],[c_216984,c_195245]) ).
tcf(c_217207,plain,
! [X0: $i] : multiplication(addition(iPr_def_10,one),multiplication(iPr_def_25,X0)) = addition(iPr_def_19,multiplication(iPr_def_25,X0)),
inference(theory_normalisation,[status(thm)],[c_216597,c_50,c_49]) ).
tcf(c_217208,plain,
! [X0: $i] : multiplication(one,multiplication(iPr_def_25,X0)) = multiplication(iPr_def_25,addition(iPr_def_23,X0)),
inference(light_normalisation,[status(thm)],[c_217207,c_196793,c_202789]) ).
tcf(c_217719,plain,
! [X0: $i] : addition(iPr_def_17,addition(X0,iPr_def_20)) = addition(iPr_def_17,X0),
inference(superposition,[status(thm)],[c_49,c_209720]) ).
tcf(c_217722,plain,
addition(iPr_def_17,one) = addition(iPr_def_17,iPr_def_21),
inference(superposition,[status(thm)],[c_194160,c_209720]) ).
tcf(c_217741,plain,
addition(iPr_def_17,iPr_def_21) = one,
inference(light_normalisation,[status(thm)],[c_217722,c_196802]) ).
tcf(c_217763,plain,
multiplication(iPr_def_20,one) = multiplication(iPr_def_20,iPr_def_17),
inference(superposition,[status(thm)],[c_217741,c_197901]) ).
tcf(c_218147,plain,
multiplication(one,iPr_def_17) = multiplication(iPr_def_20,iPr_def_17),
inference(superposition,[status(thm)],[c_194160,c_211153]) ).
tcf(c_218887,plain,
addition(iPr_def_18,iPr_def_21) = iPr_def_21,
inference(demodulation,[status(thm)],[c_216931,c_55]) ).
tcf(c_218894,plain,
multiplication(iPr_def_20,iPr_def_18) = multiplication(iPr_def_20,iPr_def_21),
inference(superposition,[status(thm)],[c_218887,c_197901]) ).
tcf(c_218898,plain,
multiplication(iPr_def_20,iPr_def_18) = iPr_def_19,
inference(light_normalisation,[status(thm)],[c_218894,c_194179]) ).
tcf(c_219421,plain,
addition(iPr_def_17,iPr_def_17) = addition(iPr_def_17,iPr_def_20),
inference(superposition,[status(thm)],[c_217719,c_194189]) ).
tcf(c_219432,plain,
multiplication(iPr_def_20,iPr_def_17) = iPr_def_17,
inference(light_normalisation,[status(thm)],[c_219421,c_209716,c_216960,c_218147]) ).
tcf(c_219557,plain,
multiplication(iPr_def_20,addition(one,iPr_def_18)) = addition(iPr_def_20,iPr_def_19),
inference(superposition,[status(thm)],[c_218898,c_194250]) ).
tcf(c_219581,plain,
multiplication(iPr_def_20,addition(iPr_def_18,one)) = addition(iPr_def_19,iPr_def_20),
inference(theory_normalisation,[status(thm)],[c_219557,c_50,c_49]) ).
tcf(c_219582,plain,
multiplication(one,iPr_def_20) = iPr_def_17,
inference(light_normalisation,[status(thm)],[c_219581,c_194854,c_216985,c_217763,c_219432]) ).
tcf(c_219667,plain,
iPr_def_17 = iPr_def_20,
inference(demodulation,[status(thm)],[c_219582,c_55]) ).
tcf(c_219728,plain,
coantidomain(iPr_def_17) = iPr_def_21,
inference(demodulation,[status(thm)],[c_142,c_219667]) ).
tcf(c_219756,plain,
multiplication(iPr_def_18,iPr_def_21) = iPr_def_21,
inference(demodulation,[status(thm)],[c_199815,c_219728]) ).
tcf(c_219757,plain,
iPr_def_18 = iPr_def_21,
inference(light_normalisation,[status(thm)],[c_219756,c_195598]) ).
tcf(c_219807,plain,
multiplication(iPr_def_18,sK0) = iPr_def_22,
inference(demodulation,[status(thm)],[c_143,c_219757]) ).
tcf(c_219808,plain,
multiplication(iPr_def_18,iPr_def_22) = iPr_def_22,
inference(demodulation,[status(thm)],[c_199355,c_219807]) ).
tcf(c_221789,plain,
addition(iPr_def_24,iPr_def_25) = iPr_def_24,
inference(demodulation,[status(thm)],[c_216935,c_55]) ).
tcf(c_221795,plain,
multiplication(iPr_def_23,iPr_def_24) = multiplication(iPr_def_23,iPr_def_25),
inference(superposition,[status(thm)],[c_221789,c_195307]) ).
tcf(c_221799,plain,
multiplication(iPr_def_23,iPr_def_25) = iPr_def_19,
inference(light_normalisation,[status(thm)],[c_221795,c_194181]) ).
tcf(c_222109,plain,
! [X0: $i] : multiplication(iPr_def_23,multiplication(iPr_def_25,X0)) = multiplication(iPr_def_19,X0),
inference(superposition,[status(thm)],[c_221799,c_53]) ).
tcf(c_222126,plain,
! [X0: $i] : multiplication(iPr_def_23,multiplication(iPr_def_25,X0)) = iPr_def_19,
inference(light_normalisation,[status(thm)],[c_222109,c_194162]) ).
tcf(c_222180,plain,
! [X0: $i,X1: $i] : addition(multiplication(X0,multiplication(iPr_def_25,X1)),iPr_def_19) = multiplication(addition(X0,iPr_def_23),multiplication(iPr_def_25,X1)),
inference(superposition,[status(thm)],[c_222126,c_57]) ).
tcf(c_222198,plain,
! [X0: $i,X1: $i] : addition(iPr_def_19,multiplication(X0,multiplication(iPr_def_25,X1))) = multiplication(addition(X0,iPr_def_23),multiplication(iPr_def_25,X1)),
inference(theory_normalisation,[status(thm)],[c_222180,c_50,c_49]) ).
tcf(c_232431,plain,
! [X0: $i,X1: $i] : addition(iPr_def_19,multiplication(X0,multiplication(iPr_def_25,X1))) = multiplication(multiplication(addition(iPr_def_10,X0),iPr_def_25),X1),
inference(light_normalisation,[status(thm)],[c_214984,c_215828]) ).
tcf(c_232432,plain,
! [X0: $i,X1: $i] : multiplication(addition(X0,iPr_def_23),multiplication(iPr_def_25,X1)) = multiplication(multiplication(X0,iPr_def_25),X1),
inference(light_normalisation,[status(thm)],[c_232431,c_215834,c_222198]) ).
tcf(c_232433,plain,
! [X0: $i,X1: $i] : multiplication(addition(X0,iPr_def_23),multiplication(iPr_def_25,X1)) = multiplication(X0,multiplication(iPr_def_25,X1)),
inference(demodulation,[status(thm)],[c_232432,c_53]) ).
tcf(c_236588,plain,
! [X0: $i,X1: $i,X2: $i] : addition(antidomain(multiplication(X0,multiplication(X1,X2))),antidomain(multiplication(X0,multiplication(X1,antidomain(antidomain(X2)))))) = antidomain(multiplication(X0,multiplication(X1,antidomain(antidomain(X2))))),
inference(demodulation,[status(thm)],[c_194399,c_53]) ).
tcf(c_258638,plain,
! [X0: $i] : addition(coantidomain(multiplication(X0,iPr_def_19)),coantidomain(multiplication(coantidomain(coantidomain(multiplication(X0,iPr_def_22))),sK1))) = coantidomain(multiplication(coantidomain(coantidomain(multiplication(X0,iPr_def_22))),sK1)),
inference(superposition,[status(thm)],[c_201573,c_194457]) ).
tcf(c_259652,plain,
! [X0: $i] : addition(one,coantidomain(multiplication(coantidomain(coantidomain(multiplication(X0,iPr_def_22))),sK1))) = coantidomain(multiplication(coantidomain(coantidomain(multiplication(X0,iPr_def_22))),sK1)),
inference(light_normalisation,[status(thm)],[c_258638,c_194161,c_194647]) ).
tcf(c_261087,plain,
! [X0: $i] : coantidomain(multiplication(coantidomain(coantidomain(multiplication(X0,iPr_def_22))),sK1)) = one,
inference(demodulation,[status(thm)],[c_259652,c_196817]) ).
tcf(c_261098,plain,
coantidomain(multiplication(coantidomain(coantidomain(iPr_def_22)),sK1)) = one,
inference(superposition,[status(thm)],[c_219808,c_261087]) ).
tcf(c_261163,plain,
coantidomain(multiplication(iPr_def_24,sK1)) = one,
inference(light_normalisation,[status(thm)],[c_261098,c_144,c_145]) ).
tcf(c_261604,plain,
! [X0: $i] : multiplication(multiplication(iPr_def_24,sK1),multiplication(coantidomain(one),X0)) = multiplication(multiplication(iPr_def_24,sK1),X0),
inference(superposition,[status(thm)],[c_261163,c_195570]) ).
tcf(c_261611,plain,
multiplication(multiplication(iPr_def_24,sK1),coantidomain(one)) = multiplication(iPr_def_24,sK1),
inference(superposition,[status(thm)],[c_261163,c_195345]) ).
tcf(c_261615,plain,
! [X0: $i] : multiplication(multiplication(iPr_def_24,sK1),multiplication(one,X0)) = iPr_def_19,
inference(superposition,[status(thm)],[c_261163,c_194961]) ).
tcf(c_261627,plain,
! [X0: $i] : multiplication(multiplication(iPr_def_24,sK1),X0) = iPr_def_19,
inference(light_normalisation,[status(thm)],[c_261615,c_55]) ).
tcf(c_261628,plain,
multiplication(multiplication(iPr_def_24,sK1),iPr_def_19) = multiplication(iPr_def_24,sK1),
inference(light_normalisation,[status(thm)],[c_261611,c_194182]) ).
tcf(c_261631,plain,
! [X0: $i] : multiplication(multiplication(iPr_def_24,sK1),X0) = multiplication(multiplication(iPr_def_24,sK1),iPr_def_19),
inference(light_normalisation,[status(thm)],[c_261604,c_194162,c_194182]) ).
tcf(c_261766,plain,
multiplication(iPr_def_24,sK1) = iPr_def_19,
inference(light_normalisation,[status(thm)],[c_261631,c_261627,c_261628]) ).
tcf(c_261769,plain,
! [X0: $i] : addition(antidomain(multiplication(X0,iPr_def_19)),antidomain(multiplication(X0,multiplication(iPr_def_24,antidomain(antidomain(sK1)))))) = antidomain(multiplication(X0,multiplication(iPr_def_24,antidomain(antidomain(sK1))))),
inference(superposition,[status(thm)],[c_261766,c_236588]) ).
tcf(c_261834,plain,
! [X0: $i] : addition(one,antidomain(multiplication(X0,multiplication(iPr_def_24,iPr_def_11)))) = antidomain(multiplication(X0,multiplication(iPr_def_24,iPr_def_11))),
inference(light_normalisation,[status(thm)],[c_261769,c_131,c_194161,c_208528,c_194641]) ).
tcf(c_262091,plain,
! [X0: $i] : antidomain(multiplication(X0,multiplication(iPr_def_24,iPr_def_11))) = one,
inference(demodulation,[status(thm)],[c_261834,c_196818]) ).
tcf(c_262128,plain,
! [X0: $i] : multiplication(one,multiplication(X0,multiplication(iPr_def_24,iPr_def_11))) = iPr_def_19,
inference(superposition,[status(thm)],[c_262091,c_194163]) ).
tcf(c_262158,plain,
! [X0: $i] : multiplication(X0,multiplication(iPr_def_24,iPr_def_11)) = iPr_def_19,
inference(demodulation,[status(thm)],[c_262128,c_55]) ).
tcf(c_262326,plain,
multiplication(iPr_def_24,iPr_def_11) = iPr_def_19,
inference(superposition,[status(thm)],[c_262158,c_195386]) ).
tcf(c_262340,plain,
multiplication(iPr_def_25,iPr_def_11) = iPr_def_19,
inference(superposition,[status(thm)],[c_262158,c_197279]) ).
tcf(c_262536,plain,
! [X0: $i] : multiplication(iPr_def_24,multiplication(iPr_def_11,X0)) = multiplication(iPr_def_19,X0),
inference(superposition,[status(thm)],[c_262326,c_53]) ).
tcf(c_262561,plain,
! [X0: $i] : multiplication(iPr_def_24,multiplication(iPr_def_11,X0)) = iPr_def_19,
inference(light_normalisation,[status(thm)],[c_262536,c_194162]) ).
tcf(c_262606,plain,
! [X0: $i] : multiplication(iPr_def_25,multiplication(iPr_def_11,X0)) = multiplication(iPr_def_19,X0),
inference(superposition,[status(thm)],[c_262340,c_53]) ).
tcf(c_262629,plain,
! [X0: $i] : multiplication(iPr_def_25,multiplication(iPr_def_11,X0)) = iPr_def_19,
inference(light_normalisation,[status(thm)],[c_262606,c_194162]) ).
tcf(c_262803,plain,
! [X0: $i] : multiplication(iPr_def_24,multiplication(iPr_def_25,X0)) = iPr_def_19,
inference(superposition,[status(thm)],[c_194214,c_262561]) ).
tcf(c_262845,plain,
! [X0: $i,X1: $i,X2: $i] : addition(multiplication(X0,iPr_def_19),multiplication(X1,multiplication(iPr_def_11,X2))) = multiplication(addition(multiplication(X0,iPr_def_24),X1),multiplication(iPr_def_11,X2)),
inference(superposition,[status(thm)],[c_262561,c_194323]) ).
tcf(c_262908,plain,
! [X0: $i,X1: $i,X2: $i] : multiplication(addition(multiplication(X0,iPr_def_24),X1),multiplication(iPr_def_11,X2)) = addition(iPr_def_19,multiplication(X1,multiplication(iPr_def_11,X2))),
inference(light_normalisation,[status(thm)],[c_262845,c_194161]) ).
tcf(c_262934,plain,
! [X0: $i] : multiplication(iPr_def_25,multiplication(iPr_def_25,X0)) = iPr_def_19,
inference(superposition,[status(thm)],[c_194214,c_262629]) ).
tcf(c_262996,plain,
! [X0: $i,X1: $i] : addition(iPr_def_19,multiplication(X0,multiplication(iPr_def_11,X1))) = multiplication(addition(iPr_def_25,X0),multiplication(iPr_def_11,X1)),
inference(superposition,[status(thm)],[c_262629,c_57]) ).
tcf(c_263926,plain,
! [X0: $i,X1: $i,X2: $i] : multiplication(addition(multiplication(X0,iPr_def_24),X1),multiplication(iPr_def_11,X2)) = multiplication(addition(iPr_def_25,X1),multiplication(iPr_def_11,X2)),
inference(demodulation,[status(thm)],[c_262908,c_262996]) ).
tcf(c_263978,plain,
! [X0: $i,X1: $i,X2: $i] : multiplication(addition(multiplication(X0,iPr_def_24),X1),multiplication(iPr_def_25,X2)) = multiplication(addition(iPr_def_25,X1),multiplication(iPr_def_25,X2)),
inference(superposition,[status(thm)],[c_194214,c_263926]) ).
tcf(c_266264,plain,
! [X0: $i,X1: $i,X2: $i] : addition(multiplication(X0,iPr_def_19),multiplication(X1,multiplication(iPr_def_25,X2))) = multiplication(addition(multiplication(X0,iPr_def_24),X1),multiplication(iPr_def_25,X2)),
inference(superposition,[status(thm)],[c_262803,c_194323]) ).
tcf(c_266284,plain,
! [X0: $i,X1: $i] : addition(iPr_def_19,multiplication(X0,multiplication(iPr_def_25,X1))) = multiplication(addition(iPr_def_24,X0),multiplication(iPr_def_25,X1)),
inference(superposition,[status(thm)],[c_262803,c_57]) ).
tcf(c_266327,plain,
! [X0: $i,X1: $i] : addition(iPr_def_19,multiplication(X0,multiplication(iPr_def_25,X1))) = multiplication(addition(iPr_def_25,X0),multiplication(iPr_def_25,X1)),
inference(light_normalisation,[status(thm)],[c_266264,c_194161,c_263978]) ).
tcf(c_266349,plain,
! [X0: $i,X1: $i] : multiplication(addition(iPr_def_24,X0),multiplication(iPr_def_25,X1)) = multiplication(addition(iPr_def_25,X0),multiplication(iPr_def_25,X1)),
inference(light_normalisation,[status(thm)],[c_266327,c_266284]) ).
tcf(c_266467,plain,
! [X0: $i] : multiplication(addition(iPr_def_24,iPr_def_23),multiplication(iPr_def_25,X0)) = multiplication(iPr_def_25,multiplication(iPr_def_25,X0)),
inference(superposition,[status(thm)],[c_266349,c_232433]) ).
tcf(c_266470,plain,
! [X0: $i] : multiplication(addition(iPr_def_23,iPr_def_24),multiplication(iPr_def_25,X0)) = multiplication(iPr_def_25,multiplication(iPr_def_25,X0)),
inference(theory_normalisation,[status(thm)],[c_266467,c_50,c_49]) ).
tcf(c_266471,plain,
! [X0: $i] : multiplication(iPr_def_25,addition(iPr_def_23,X0)) = iPr_def_19,
inference(light_normalisation,[status(thm)],[c_266470,c_194159,c_217208,c_262934]) ).
tcf(c_268517,plain,
multiplication(iPr_def_25,one) = iPr_def_19,
inference(superposition,[status(thm)],[c_196797,c_266471]) ).
tcf(c_268607,plain,
iPr_def_19 = iPr_def_25,
inference(demodulation,[status(thm)],[c_268517,c_54]) ).
tcf(c_268608,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[c_268607,c_194124]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : KLE101+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.11/5.38 % Computer : n002.cluster.edu
% 0.11/5.38 % Model : x86_64 x86_64
% 0.11/5.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/5.38 % Memory : 8046.5625MB
% 0.11/5.38 % OS : Linux 6.8.0-71-generic
% 0.11/5.38 % CPULimit : 300
% 0.11/5.38 % WCLimit : 300
% 0.11/5.38 % DateTime : Wed Sep 23 18:58:30 UTC 2026
% 0.11/5.39 % CPUTime :
% 0.11/5.39 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.14/5.42 Running first-order theorem proving
% 0.14/5.42 Running: /export/starexec/sandbox/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.14/5.44
% 0.14/5.44 % ======== iProver multi-core TPTP/SMT =========
% 0.14/5.44
% 0.14/5.44 % Detected problem language: tptp
% 0.14/5.45 % Proving...
% 77.64/19.48 % SZS status Started for theBenchmark.p
% 77.64/19.48 % SZS status Theorem for theBenchmark.p
% 77.64/19.48
% 77.64/19.48 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 77.64/19.48
% 77.64/19.48 % ------ iProver source info
% 77.64/19.48
% 77.64/19.48 % git: date: 2026-07-19 20:42:38 +0200
% 77.64/19.48 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 77.64/19.48 % git: non_committed_changes: false
% 77.64/19.48
% 77.64/19.48 % ------ Parsing...
% 77.64/19.48 % ------ Clausification by vclausify_rel & Parsing by iProver...% ------ preprocesses with Option_UEQ
% 77.64/19.48 %
% 77.64/19.48
% 77.64/19.48 % ------ Preprocessing... sup_sim: 0 sf_s rm: 0 0s sf_e pe_s pe_e %
% 77.64/19.48
% 77.64/19.48 % ------ Preprocessing...% ------ preprocesses with Option_UEQ
% 77.64/19.48 gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 77.64/19.48
% 77.64/19.48 % ------ Preprocessing... sf_s rm: 0 0s sf_e
% 77.64/19.48 % ------ Proving...
% 77.64/19.48 % ------ Problem Properties
% 77.64/19.48
% 77.64/19.48 %
% 77.64/19.48 % clauses 35
% 77.64/19.48 % conjectures 2
% 77.64/19.48 % EPR 2
% 77.64/19.48 % Horn 35
% 77.64/19.48 % unary 35
% 77.64/19.48 % binary 0
% 77.64/19.48 % lits 35
% 77.64/19.48 % lits eq 35
% 77.64/19.48 % fd_pure 0
% 77.64/19.48 % fd_pseudo 0
% 77.64/19.48 % fd_cond 0
% 77.64/19.48 % fd_pseudo_cond 0
% 77.64/19.48 % AC symbols 1
% 77.64/19.48
% 77.64/19.48 % ------ Schedule UEQ
% 77.64/19.48
% 77.64/19.48 % ------ Option_UEQ Time Limit: 10.
% 77.64/19.48
% 77.64/19.48
% 77.64/19.48 % ------
% 77.64/19.48 % Current options:
% 77.64/19.48 % ------
% 77.64/19.48
% 77.64/19.48
% 77.64/19.48 %
% 77.64/19.48
% 77.64/19.48 % ------ Proving...
% 77.64/19.48 % Proof_search_loop: time out after: 2611 full_loop iterations
% 77.64/19.48
% 77.64/19.48 % ------ Option_UEQ Time Limit: 15.
% 77.64/19.48
% 77.64/19.48
% 77.64/19.48 % ------
% 77.64/19.48 % Current options:
% 77.64/19.48 % ------
% 77.64/19.48
% 77.64/19.48
% 77.64/19.48 %
% 77.64/19.48
% 77.64/19.48 % ------ Proving...
% 77.64/19.48 %
% 77.64/19.48
% 77.64/19.48 % SZS status Theorem for theBenchmark.p
% 77.64/19.48
% 77.64/19.48 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 77.64/19.49
% 77.64/19.49
%------------------------------------------------------------------------------