%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : KLE109+1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% Computer : n016.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:25 PM UTC 2026
% Result : Theorem 121.31s 19.65s
% Output : CNFRefutation 121.31s
% Verified :
% SZS Type : Refutation
% Derivation depth : 49
% Number of leaves : 44
% Syntax : Number of formulae : 355 ( 346 unt; 19 def)
% Number of atoms : 1124 ( 372 equ)
% Maximal formula atoms : 3 ( 3 avg)
% Number of connectives : 44 ( 26 ~; 18 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 2 avg)
% Maximal term depth : 20 ( 2 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 21 ( 19 usr; 20 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 4 con; 0-2 aty)
% Number of variables : 233 ( 0 sgn 231 !; 2 ?; 150 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] : addition(X0,X1) = addition(X1,X0),
file('/export/starexec/sandbox2/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/sandbox2/benchmark/Axioms/KLE001+0.ax',additive_associativity) ).
fof(f3,axiom,
! [X0] : addition(X0,zero) = X0,
file('/export/starexec/sandbox2/benchmark/Axioms/KLE001+0.ax',additive_identity) ).
fof(f4,axiom,
! [X0] : addition(X0,X0) = X0,
file('/export/starexec/sandbox2/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/sandbox2/benchmark/Axioms/KLE001+0.ax',multiplicative_associativity) ).
fof(f6,axiom,
! [X0] : multiplication(X0,one) = X0,
file('/export/starexec/sandbox2/benchmark/Axioms/KLE001+0.ax',multiplicative_right_identity) ).
fof(f7,axiom,
! [X0] : multiplication(one,X0) = X0,
file('/export/starexec/sandbox2/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/sandbox2/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/sandbox2/benchmark/Axioms/KLE001+0.ax',left_distributivity) ).
fof(f10,axiom,
! [X0] : multiplication(X0,zero) = zero,
file('/export/starexec/sandbox2/benchmark/Axioms/KLE001+0.ax',right_annihilation) ).
fof(f11,axiom,
! [X0] : multiplication(zero,X0) = zero,
file('/export/starexec/sandbox2/benchmark/Axioms/KLE001+0.ax',left_annihilation) ).
fof(f13,axiom,
! [X0] : multiplication(antidomain(X0),X0) = zero,
file('/export/starexec/sandbox2/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/sandbox2/benchmark/Axioms/KLE001+4.ax',domain2) ).
fof(f15,axiom,
! [X0] : addition(antidomain(antidomain(X0)),antidomain(X0)) = one,
file('/export/starexec/sandbox2/benchmark/Axioms/KLE001+4.ax',domain3) ).
fof(f16,axiom,
! [X0] : domain(X0) = antidomain(antidomain(X0)),
file('/export/starexec/sandbox2/benchmark/Axioms/KLE001+4.ax',domain4) ).
fof(f17,axiom,
! [X0] : multiplication(X0,coantidomain(X0)) = zero,
file('/export/starexec/sandbox2/benchmark/Axioms/KLE001+4.ax',codomain1) ).
fof(f19,axiom,
! [X0] : addition(coantidomain(coantidomain(X0)),coantidomain(X0)) = one,
file('/export/starexec/sandbox2/benchmark/Axioms/KLE001+4.ax',codomain3) ).
fof(f20,axiom,
! [X0] : codomain(X0) = coantidomain(coantidomain(X0)),
file('/export/starexec/sandbox2/benchmark/Axioms/KLE001+4.ax',codomain4) ).
fof(f21,axiom,
! [X0] : c(X0) = antidomain(domain(X0)),
file('/export/starexec/sandbox2/benchmark/Axioms/KLE001+6.ax',complement) ).
fof(f23,axiom,
! [X0,X1] : forward_diamond(X0,X1) = domain(multiplication(X0,domain(X1))),
file('/export/starexec/sandbox2/benchmark/Axioms/KLE001+6.ax',forward_diamond) ).
fof(f24,axiom,
! [X0,X1] : backward_diamond(X0,X1) = codomain(multiplication(codomain(X1),X0)),
file('/export/starexec/sandbox2/benchmark/Axioms/KLE001+6.ax',backward_diamond) ).
fof(f26,axiom,
! [X0,X1] : backward_box(X0,X1) = c(backward_diamond(X0,c(X1))),
file('/export/starexec/sandbox2/benchmark/Axioms/KLE001+6.ax',backward_box) ).
fof(f27,conjecture,
! [X0,X1] : addition(forward_diamond(X0,backward_box(X0,domain(X1))),domain(X1)) = domain(X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goals) ).
fof(f28,negated_conjecture,
~ ! [X0,X1] : addition(forward_diamond(X0,backward_box(X0,domain(X1))),domain(X1)) = domain(X1),
inference(negated_conjecture,[status(cth)],[f27]) ).
fof(f29,plain,
? [X0,X1] : domain(X1) != addition(forward_diamond(X0,backward_box(X0,domain(X1))),domain(X1)),
inference(ennf_transformation,[],[f28]) ).
fof(f30,plain,
domain(sK1) != addition(forward_diamond(sK0,backward_box(sK0,domain(sK1))),domain(sK1)),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1]),skolemize(X0,sK0),skolemize(X1,sK1)],[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(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(f50,plain,
! [X0] : c(X0) = antidomain(domain(X0)),
inference(cnf_transformation,[],[f21]) ).
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(f55,plain,
! [X0,X1] : backward_box(X0,X1) = c(backward_diamond(X0,c(X1))),
inference(cnf_transformation,[],[f26]) ).
fof(f56,plain,
domain(sK1) != addition(forward_diamond(sK0,backward_box(sK0,domain(sK1))),domain(sK1)),
inference(cnf_transformation,[],[f30]) ).
fof(f57,plain,
! [X0] : c(X0) = antidomain(antidomain(antidomain(X0))),
inference(definition_unfolding,[],[f50,f45]) ).
fof(f58,plain,
! [X0,X1] : backward_diamond(X0,X1) = coantidomain(coantidomain(multiplication(coantidomain(coantidomain(X1)),X0))),
inference(definition_unfolding,[],[f53,f49,f49]) ).
fof(f59,plain,
! [X0,X1] : backward_box(X0,X1) = antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(X1))))),X0)))))),
inference(definition_unfolding,[],[f55,f57,f58,f57]) ).
fof(f61,plain,
! [X0,X1] : forward_diamond(X0,X1) = antidomain(antidomain(multiplication(X0,antidomain(antidomain(X1))))),
inference(definition_unfolding,[],[f52,f45,f45]) ).
fof(f63,plain,
antidomain(antidomain(sK1)) != addition(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sK1))))))),sK0))))))))))),antidomain(antidomain(sK1))),
inference(definition_unfolding,[],[f56,f45,f61,f59,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_65,plain,
! [X0: $i] : addition(coantidomain(coantidomain(X0)),coantidomain(X0)) = one,
inference(cnf_transformation,[],[f48]) ).
tcf(c_66,negated_conjecture,
addition(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sK1))))))),sK0))))))))))),antidomain(antidomain(sK1))) != antidomain(antidomain(sK1)),
inference(cnf_transformation,[],[f63]) ).
tcf(c_82,plain,
! [X0: $i] : addition(antidomain(X0),antidomain(antidomain(X0))) = one,
inference(theory_normalisation,[status(thm)],[c_62,c_50,c_49]) ).
tcf(c_83,plain,
! [X0: $i] : addition(coantidomain(X0),coantidomain(coantidomain(X0))) = one,
inference(theory_normalisation,[status(thm)],[c_65,c_50,c_49]) ).
tcf(c_84,negated_conjecture,
addition(antidomain(antidomain(sK1)),antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sK1))))))),sK0)))))))))))) != antidomain(antidomain(sK1)),
inference(theory_normalisation,[status(thm)],[c_66,c_50,c_49]) ).
tcf(c_129,definition,
iPr_def_10 = antidomain(sK1),
introduced(definition,[new_symbols(definition,[iPr_def_10])],[]) ).
tcf(c_130,definition,
iPr_def_11 = antidomain(iPr_def_10),
introduced(definition,[new_symbols(definition,[iPr_def_11])],[]) ).
tcf(c_131,definition,
iPr_def_12 = antidomain(iPr_def_11),
introduced(definition,[new_symbols(definition,[iPr_def_12])],[]) ).
tcf(c_132,definition,
iPr_def_13 = antidomain(iPr_def_12),
introduced(definition,[new_symbols(definition,[iPr_def_13])],[]) ).
tcf(c_133,definition,
iPr_def_14 = antidomain(iPr_def_13),
introduced(definition,[new_symbols(definition,[iPr_def_14])],[]) ).
tcf(c_134,definition,
iPr_def_15 = coantidomain(iPr_def_14),
introduced(definition,[new_symbols(definition,[iPr_def_15])],[]) ).
tcf(c_135,definition,
iPr_def_16 = coantidomain(iPr_def_15),
introduced(definition,[new_symbols(definition,[iPr_def_16])],[]) ).
tcf(c_136,definition,
iPr_def_17 = multiplication(iPr_def_16,sK0),
introduced(definition,[new_symbols(definition,[iPr_def_17])],[]) ).
tcf(c_137,definition,
iPr_def_18 = coantidomain(iPr_def_17),
introduced(definition,[new_symbols(definition,[iPr_def_18])],[]) ).
tcf(c_138,definition,
iPr_def_19 = coantidomain(iPr_def_18),
introduced(definition,[new_symbols(definition,[iPr_def_19])],[]) ).
tcf(c_139,definition,
iPr_def_20 = antidomain(iPr_def_19),
introduced(definition,[new_symbols(definition,[iPr_def_20])],[]) ).
tcf(c_140,definition,
iPr_def_21 = antidomain(iPr_def_20),
introduced(definition,[new_symbols(definition,[iPr_def_21])],[]) ).
tcf(c_141,definition,
iPr_def_22 = antidomain(iPr_def_21),
introduced(definition,[new_symbols(definition,[iPr_def_22])],[]) ).
tcf(c_142,definition,
iPr_def_23 = antidomain(iPr_def_22),
introduced(definition,[new_symbols(definition,[iPr_def_23])],[]) ).
tcf(c_143,definition,
iPr_def_24 = antidomain(iPr_def_23),
introduced(definition,[new_symbols(definition,[iPr_def_24])],[]) ).
tcf(c_144,definition,
iPr_def_25 = multiplication(sK0,iPr_def_24),
introduced(definition,[new_symbols(definition,[iPr_def_25])],[]) ).
tcf(c_145,definition,
iPr_def_26 = antidomain(iPr_def_25),
introduced(definition,[new_symbols(definition,[iPr_def_26])],[]) ).
tcf(c_146,definition,
iPr_def_27 = antidomain(iPr_def_26),
introduced(definition,[new_symbols(definition,[iPr_def_27])],[]) ).
tcf(c_147,definition,
iPr_def_28 = addition(iPr_def_11,iPr_def_27),
introduced(definition,[new_symbols(definition,[iPr_def_28])],[]) ).
tcf(c_148,negated_conjecture,
iPr_def_28 != iPr_def_11,
inference(demodulation,[status(thm)],[c_84,c_131,c_132,c_133,c_134,c_135,c_136,c_137,c_138,c_139,c_140,c_141,c_142,c_143,c_144,c_145,c_146,c_129,c_130,c_147]) ).
tcf(c_149,plain,
! [X0: $i] : X0 = X0,
theory(equality) ).
tcf(c_150,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = X0 )
| ( X2 != X1 )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_267,plain,
addition(iPr_def_10,antidomain(iPr_def_10)) = one,
inference(superposition,[status(thm)],[c_129,c_82]) ).
tcf(c_268,plain,
addition(iPr_def_11,antidomain(iPr_def_11)) = one,
inference(superposition,[status(thm)],[c_130,c_82]) ).
tcf(c_269,plain,
addition(iPr_def_12,antidomain(iPr_def_12)) = one,
inference(superposition,[status(thm)],[c_131,c_82]) ).
tcf(c_270,plain,
addition(iPr_def_13,antidomain(iPr_def_13)) = one,
inference(superposition,[status(thm)],[c_132,c_82]) ).
tcf(c_272,plain,
addition(iPr_def_13,iPr_def_14) = one,
inference(light_normalisation,[status(thm)],[c_270,c_133]) ).
tcf(c_273,plain,
addition(iPr_def_12,iPr_def_13) = one,
inference(light_normalisation,[status(thm)],[c_269,c_132]) ).
tcf(c_274,plain,
addition(iPr_def_11,iPr_def_12) = one,
inference(light_normalisation,[status(thm)],[c_268,c_131]) ).
tcf(c_275,plain,
addition(iPr_def_10,iPr_def_11) = one,
inference(light_normalisation,[status(thm)],[c_267,c_130]) ).
tcf(c_276,plain,
! [X0: $i] : addition(antidomain(X0),antidomain(antidomain(X0))) = addition(iPr_def_13,iPr_def_14),
inference(demodulation,[status(thm)],[c_82,c_272]) ).
tcf(c_277,plain,
! [X0: $i] : multiplication(X0,addition(iPr_def_13,iPr_def_14)) = X0,
inference(light_normalisation,[status(thm)],[c_54,c_272]) ).
tcf(c_278,plain,
! [X0: $i] : addition(multiplication(X0,iPr_def_13),multiplication(X0,iPr_def_14)) = X0,
inference(demodulation,[status(thm)],[c_277,c_56]) ).
tcf(c_279,plain,
! [X0: $i] : multiplication(addition(iPr_def_13,iPr_def_14),X0) = X0,
inference(light_normalisation,[status(thm)],[c_55,c_272]) ).
tcf(c_280,plain,
! [X0: $i] : addition(multiplication(iPr_def_13,X0),multiplication(iPr_def_14,X0)) = X0,
inference(demodulation,[status(thm)],[c_279,c_57]) ).
tcf(c_287,plain,
! [X0: $i] : addition(coantidomain(X0),coantidomain(coantidomain(X0))) = addition(iPr_def_13,iPr_def_14),
inference(light_normalisation,[status(thm)],[c_83,c_272]) ).
tcf(c_292,plain,
addition(iPr_def_15,coantidomain(iPr_def_15)) = addition(iPr_def_13,iPr_def_14),
inference(superposition,[status(thm)],[c_134,c_287]) ).
tcf(c_294,plain,
addition(iPr_def_18,coantidomain(iPr_def_18)) = addition(iPr_def_13,iPr_def_14),
inference(superposition,[status(thm)],[c_137,c_287]) ).
tcf(c_295,plain,
addition(iPr_def_19,coantidomain(iPr_def_19)) = addition(iPr_def_13,iPr_def_14),
inference(superposition,[status(thm)],[c_138,c_287]) ).
tcf(c_296,plain,
addition(iPr_def_13,iPr_def_14) = addition(iPr_def_18,iPr_def_19),
inference(light_normalisation,[status(thm)],[c_294,c_138]) ).
tcf(c_297,plain,
addition(iPr_def_13,iPr_def_14) = addition(iPr_def_15,iPr_def_16),
inference(light_normalisation,[status(thm)],[c_292,c_135]) ).
tcf(c_299,plain,
multiplication(iPr_def_11,iPr_def_10) = zero,
inference(superposition,[status(thm)],[c_130,c_60]) ).
tcf(c_300,plain,
multiplication(iPr_def_12,iPr_def_11) = zero,
inference(superposition,[status(thm)],[c_131,c_60]) ).
tcf(c_301,plain,
multiplication(iPr_def_13,iPr_def_12) = zero,
inference(superposition,[status(thm)],[c_132,c_60]) ).
tcf(c_302,plain,
multiplication(iPr_def_14,iPr_def_13) = zero,
inference(superposition,[status(thm)],[c_133,c_60]) ).
tcf(c_303,plain,
multiplication(iPr_def_20,iPr_def_19) = zero,
inference(superposition,[status(thm)],[c_139,c_60]) ).
tcf(c_304,plain,
multiplication(iPr_def_21,iPr_def_20) = zero,
inference(superposition,[status(thm)],[c_140,c_60]) ).
tcf(c_305,plain,
multiplication(iPr_def_22,iPr_def_21) = zero,
inference(superposition,[status(thm)],[c_141,c_60]) ).
tcf(c_318,plain,
! [X0: $i] : addition(X0,multiplication(iPr_def_11,iPr_def_10)) = X0,
inference(demodulation,[status(thm)],[c_51,c_299]) ).
tcf(c_319,plain,
! [X0: $i] : multiplication(X0,coantidomain(X0)) = multiplication(iPr_def_11,iPr_def_10),
inference(light_normalisation,[status(thm)],[c_63,c_299]) ).
tcf(c_320,plain,
multiplication(iPr_def_11,iPr_def_10) = multiplication(iPr_def_14,iPr_def_15),
inference(superposition,[status(thm)],[c_134,c_319]) ).
tcf(c_325,plain,
addition(multiplication(iPr_def_13,coantidomain(iPr_def_14)),multiplication(iPr_def_11,iPr_def_10)) = coantidomain(iPr_def_14),
inference(superposition,[status(thm)],[c_319,c_280]) ).
tcf(c_326,plain,
addition(multiplication(iPr_def_11,iPr_def_10),multiplication(iPr_def_13,coantidomain(iPr_def_14))) = coantidomain(iPr_def_14),
inference(theory_normalisation,[status(thm)],[c_325,c_50,c_49]) ).
tcf(c_327,plain,
addition(multiplication(iPr_def_11,iPr_def_10),multiplication(iPr_def_13,iPr_def_15)) = iPr_def_15,
inference(light_normalisation,[status(thm)],[c_326,c_134]) ).
tcf(c_328,plain,
addition(iPr_def_12,iPr_def_13) = addition(iPr_def_13,iPr_def_14),
inference(demodulation,[status(thm)],[c_272,c_273]) ).
tcf(c_330,plain,
addition(iPr_def_11,iPr_def_12) = addition(iPr_def_12,iPr_def_13),
inference(demodulation,[status(thm)],[c_273,c_274]) ).
tcf(c_331,plain,
addition(iPr_def_11,iPr_def_12) = addition(iPr_def_13,iPr_def_14),
inference(demodulation,[status(thm)],[c_328,c_330]) ).
tcf(c_332,plain,
addition(iPr_def_10,iPr_def_11) = addition(iPr_def_11,iPr_def_12),
inference(demodulation,[status(thm)],[c_274,c_275]) ).
tcf(c_333,plain,
addition(iPr_def_10,iPr_def_11) = addition(iPr_def_12,iPr_def_13),
inference(demodulation,[status(thm)],[c_330,c_332]) ).
tcf(c_335,plain,
multiplication(iPr_def_11,iPr_def_10) = multiplication(iPr_def_12,iPr_def_11),
inference(light_normalisation,[status(thm)],[c_300,c_299]) ).
tcf(c_336,plain,
multiplication(iPr_def_11,iPr_def_10) = multiplication(iPr_def_13,iPr_def_12),
inference(light_normalisation,[status(thm)],[c_301,c_299]) ).
tcf(c_337,plain,
addition(multiplication(iPr_def_11,iPr_def_10),multiplication(iPr_def_14,iPr_def_12)) = iPr_def_12,
inference(superposition,[status(thm)],[c_336,c_280]) ).
tcf(c_338,plain,
multiplication(iPr_def_11,iPr_def_10) = multiplication(iPr_def_14,iPr_def_13),
inference(light_normalisation,[status(thm)],[c_302,c_299]) ).
tcf(c_342,plain,
multiplication(iPr_def_11,iPr_def_10) = multiplication(iPr_def_20,iPr_def_19),
inference(light_normalisation,[status(thm)],[c_303,c_299]) ).
tcf(c_343,plain,
multiplication(iPr_def_11,iPr_def_10) = multiplication(iPr_def_21,iPr_def_20),
inference(light_normalisation,[status(thm)],[c_304,c_299]) ).
tcf(c_344,plain,
multiplication(iPr_def_11,iPr_def_10) = multiplication(iPr_def_22,iPr_def_21),
inference(light_normalisation,[status(thm)],[c_305,c_299]) ).
tcf(c_364,plain,
! [X0: $i,X1: $i] : addition(X0,addition(X0,X1)) = addition(X0,X1),
inference(superposition,[status(thm)],[c_52,c_50]) ).
tcf(c_401,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_332,c_56]) ).
tcf(c_434,plain,
addition(iPr_def_10,iPr_def_11) = addition(iPr_def_18,iPr_def_19),
inference(light_normalisation,[status(thm)],[c_296,c_331,c_332]) ).
tcf(c_435,plain,
! [X0: $i] : addition(addition(iPr_def_10,iPr_def_11),X0) = addition(iPr_def_18,addition(iPr_def_19,X0)),
inference(superposition,[status(thm)],[c_434,c_50]) ).
tcf(c_439,plain,
! [X0: $i] : addition(iPr_def_10,addition(iPr_def_11,X0)) = addition(iPr_def_18,addition(iPr_def_19,X0)),
inference(theory_normalisation,[status(thm)],[c_435,c_50,c_49]) ).
tcf(c_441,plain,
addition(iPr_def_10,iPr_def_11) = addition(iPr_def_15,iPr_def_16),
inference(light_normalisation,[status(thm)],[c_297,c_331,c_332]) ).
tcf(c_457,plain,
! [X0: $i] : addition(antidomain(X0),antidomain(antidomain(X0))) = addition(iPr_def_10,iPr_def_11),
inference(light_normalisation,[status(thm)],[c_276,c_331,c_332]) ).
tcf(c_475,plain,
addition(iPr_def_20,antidomain(iPr_def_20)) = addition(iPr_def_10,iPr_def_11),
inference(superposition,[status(thm)],[c_139,c_457]) ).
tcf(c_476,plain,
addition(iPr_def_21,antidomain(iPr_def_21)) = addition(iPr_def_10,iPr_def_11),
inference(superposition,[status(thm)],[c_140,c_457]) ).
tcf(c_489,plain,
addition(iPr_def_10,iPr_def_11) = addition(iPr_def_21,iPr_def_22),
inference(light_normalisation,[status(thm)],[c_476,c_141]) ).
tcf(c_490,plain,
addition(iPr_def_10,iPr_def_11) = addition(iPr_def_20,iPr_def_21),
inference(light_normalisation,[status(thm)],[c_475,c_140]) ).
tcf(c_508,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_332,c_57]) ).
tcf(c_621,plain,
! [X0: $i] : addition(multiplication(iPr_def_11,iPr_def_10),X0) = X0,
inference(superposition,[status(thm)],[c_318,c_49]) ).
tcf(c_652,plain,
addition(iPr_def_10,iPr_def_11) = addition(iPr_def_13,iPr_def_14),
inference(light_normalisation,[status(thm)],[c_331,c_332]) ).
tcf(c_654,plain,
! [X0: $i] : addition(multiplication(X0,iPr_def_13),multiplication(X0,iPr_def_14)) = multiplication(X0,addition(iPr_def_10,iPr_def_11)),
inference(superposition,[status(thm)],[c_652,c_56]) ).
tcf(c_656,plain,
! [X0: $i] : addition(multiplication(iPr_def_13,X0),multiplication(iPr_def_14,X0)) = multiplication(addition(iPr_def_10,iPr_def_11),X0),
inference(superposition,[status(thm)],[c_652,c_57]) ).
tcf(c_659,plain,
! [X0: $i] : addition(multiplication(iPr_def_11,X0),multiplication(iPr_def_12,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_656,c_280,c_508]) ).
tcf(c_660,plain,
! [X0: $i] : addition(multiplication(X0,iPr_def_11),multiplication(X0,iPr_def_12)) = X0,
inference(light_normalisation,[status(thm)],[c_654,c_278,c_401]) ).
tcf(c_662,plain,
! [X0: $i] : addition(multiplication(X0,iPr_def_12),multiplication(X0,iPr_def_13)) = multiplication(X0,addition(iPr_def_10,iPr_def_11)),
inference(superposition,[status(thm)],[c_333,c_56]) ).
tcf(c_664,plain,
! [X0: $i] : addition(multiplication(iPr_def_12,X0),multiplication(iPr_def_13,X0)) = multiplication(addition(iPr_def_10,iPr_def_11),X0),
inference(superposition,[status(thm)],[c_333,c_57]) ).
tcf(c_667,plain,
! [X0: $i] : addition(multiplication(iPr_def_12,X0),multiplication(iPr_def_13,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_664,c_508,c_659]) ).
tcf(c_668,plain,
! [X0: $i] : addition(multiplication(X0,iPr_def_12),multiplication(X0,iPr_def_13)) = X0,
inference(light_normalisation,[status(thm)],[c_662,c_401,c_660]) ).
tcf(c_701,plain,
! [X0: $i] : addition(multiplication(iPr_def_21,X0),multiplication(iPr_def_22,X0)) = multiplication(addition(iPr_def_10,iPr_def_11),X0),
inference(superposition,[status(thm)],[c_489,c_57]) ).
tcf(c_704,plain,
! [X0: $i] : addition(multiplication(iPr_def_21,X0),multiplication(iPr_def_22,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_701,c_508,c_659]) ).
tcf(c_716,plain,
! [X0: $i] : addition(multiplication(X0,iPr_def_20),multiplication(X0,iPr_def_21)) = multiplication(X0,addition(iPr_def_10,iPr_def_11)),
inference(superposition,[status(thm)],[c_490,c_56]) ).
tcf(c_718,plain,
! [X0: $i] : addition(multiplication(iPr_def_20,X0),multiplication(iPr_def_21,X0)) = multiplication(addition(iPr_def_10,iPr_def_11),X0),
inference(superposition,[status(thm)],[c_490,c_57]) ).
tcf(c_721,plain,
! [X0: $i] : addition(multiplication(iPr_def_20,X0),multiplication(iPr_def_21,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_718,c_508,c_659]) ).
tcf(c_722,plain,
! [X0: $i] : addition(multiplication(X0,iPr_def_20),multiplication(X0,iPr_def_21)) = X0,
inference(light_normalisation,[status(thm)],[c_716,c_401,c_660]) ).
tcf(c_739,plain,
addition(iPr_def_19,coantidomain(iPr_def_19)) = addition(iPr_def_10,iPr_def_11),
inference(light_normalisation,[status(thm)],[c_295,c_652]) ).
tcf(c_741,plain,
! [X0: $i] : addition(multiplication(X0,iPr_def_19),multiplication(X0,coantidomain(iPr_def_19))) = multiplication(X0,addition(iPr_def_10,iPr_def_11)),
inference(superposition,[status(thm)],[c_739,c_56]) ).
tcf(c_747,plain,
! [X0: $i] : addition(multiplication(X0,iPr_def_19),multiplication(X0,coantidomain(iPr_def_19))) = X0,
inference(light_normalisation,[status(thm)],[c_741,c_401,c_660]) ).
tcf(c_813,plain,
multiplication(iPr_def_13,iPr_def_15) = iPr_def_15,
inference(demodulation,[status(thm)],[c_327,c_621]) ).
tcf(c_820,plain,
multiplication(iPr_def_14,iPr_def_12) = iPr_def_12,
inference(demodulation,[status(thm)],[c_337,c_621]) ).
tcf(c_911,plain,
addition(iPr_def_15,addition(iPr_def_10,iPr_def_11)) = addition(iPr_def_10,iPr_def_11),
inference(superposition,[status(thm)],[c_441,c_364]) ).
tcf(c_921,plain,
addition(iPr_def_21,addition(iPr_def_10,iPr_def_11)) = addition(iPr_def_10,iPr_def_11),
inference(superposition,[status(thm)],[c_489,c_364]) ).
tcf(c_935,plain,
addition(iPr_def_10,addition(iPr_def_11,iPr_def_21)) = addition(iPr_def_10,iPr_def_11),
inference(theory_normalisation,[status(thm)],[c_921,c_50,c_49]) ).
tcf(c_942,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_911,c_50,c_49]) ).
tcf(c_984,plain,
! [X0: $i] :
( ( iPr_def_28 = iPr_def_11 )
| ( iPr_def_28 != X0 )
| ( iPr_def_11 != X0 ) ),
inference(instantiation,[status(thm)],[c_150]) ).
tcf(c_1005,plain,
! [X0: $i,X1: $i] :
( ( iPr_def_11 = X0 )
| ( iPr_def_11 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_150]) ).
tcf(c_1075,plain,
! [X0: $i] :
( ( iPr_def_11 = X0 )
| ( iPr_def_11 != iPr_def_11 )
| ( X0 != iPr_def_11 ) ),
inference(instantiation,[status(thm)],[c_1005]) ).
tcf(c_1076,plain,
iPr_def_11 = iPr_def_11,
inference(instantiation,[status(thm)],[c_149]) ).
tcf(c_1136,plain,
iPr_def_28 = iPr_def_28,
inference(instantiation,[status(thm)],[c_149]) ).
tcf(c_1213,plain,
( ( iPr_def_11 = addition(iPr_def_11,zero) )
| ( iPr_def_11 != iPr_def_11 )
| ( addition(iPr_def_11,zero) != iPr_def_11 ) ),
inference(instantiation,[status(thm)],[c_1075]) ).
tcf(c_1214,plain,
addition(iPr_def_11,zero) = iPr_def_11,
inference(instantiation,[status(thm)],[c_51]) ).
tcf(c_1302,plain,
multiplication(iPr_def_12,iPr_def_10) = iPr_def_10,
inference(superposition,[status(thm)],[c_659,c_621]) ).
tcf(c_1415,plain,
addition(multiplication(iPr_def_13,iPr_def_11),multiplication(iPr_def_11,iPr_def_10)) = iPr_def_13,
inference(superposition,[status(thm)],[c_336,c_660]) ).
tcf(c_1425,plain,
addition(multiplication(iPr_def_11,iPr_def_10),multiplication(iPr_def_13,iPr_def_11)) = iPr_def_13,
inference(theory_normalisation,[status(thm)],[c_1415,c_50,c_49]) ).
tcf(c_1451,plain,
addition(multiplication(iPr_def_11,iPr_def_10),multiplication(iPr_def_13,iPr_def_11)) = iPr_def_11,
inference(superposition,[status(thm)],[c_335,c_667]) ).
tcf(c_1485,plain,
addition(iPr_def_12,multiplication(iPr_def_14,iPr_def_13)) = iPr_def_14,
inference(superposition,[status(thm)],[c_820,c_668]) ).
tcf(c_1499,plain,
addition(iPr_def_12,multiplication(iPr_def_11,iPr_def_10)) = iPr_def_14,
inference(light_normalisation,[status(thm)],[c_1485,c_338]) ).
tcf(c_1607,plain,
iPr_def_12 = iPr_def_14,
inference(demodulation,[status(thm)],[c_1499,c_318]) ).
tcf(c_1618,plain,
multiplication(iPr_def_11,iPr_def_10) = multiplication(iPr_def_12,iPr_def_15),
inference(demodulation,[status(thm)],[c_320,c_1607]) ).
tcf(c_1772,plain,
( ( iPr_def_28 = iPr_def_11 )
| ( iPr_def_28 != addition(iPr_def_11,zero) )
| ( iPr_def_11 != addition(iPr_def_11,zero) ) ),
inference(instantiation,[status(thm)],[c_984]) ).
tcf(c_1994,plain,
addition(multiplication(iPr_def_11,iPr_def_10),multiplication(iPr_def_22,iPr_def_20)) = iPr_def_20,
inference(superposition,[status(thm)],[c_343,c_704]) ).
tcf(c_2064,plain,
addition(multiplication(iPr_def_11,iPr_def_10),multiplication(iPr_def_21,iPr_def_19)) = iPr_def_19,
inference(superposition,[status(thm)],[c_342,c_721]) ).
tcf(c_2072,plain,
! [X0: $i] : addition(multiplication(iPr_def_20,X0),X0) = X0,
inference(superposition,[status(thm)],[c_721,c_364]) ).
tcf(c_2078,plain,
! [X0: $i] : addition(X0,multiplication(iPr_def_20,X0)) = X0,
inference(theory_normalisation,[status(thm)],[c_2072,c_50,c_49]) ).
tcf(c_2092,plain,
addition(multiplication(iPr_def_22,iPr_def_20),multiplication(iPr_def_11,iPr_def_10)) = iPr_def_22,
inference(superposition,[status(thm)],[c_344,c_722]) ).
tcf(c_2100,plain,
addition(multiplication(iPr_def_11,iPr_def_10),multiplication(iPr_def_22,iPr_def_20)) = iPr_def_22,
inference(theory_normalisation,[status(thm)],[c_2092,c_50,c_49]) ).
tcf(c_2101,plain,
iPr_def_20 = iPr_def_22,
inference(light_normalisation,[status(thm)],[c_2100,c_1994]) ).
tcf(c_2116,plain,
multiplication(iPr_def_11,iPr_def_10) = multiplication(iPr_def_20,iPr_def_21),
inference(demodulation,[status(thm)],[c_344,c_2101]) ).
tcf(c_2499,plain,
! [X0: $i] : addition(multiplication(X0,iPr_def_10),multiplication(X0,addition(iPr_def_11,iPr_def_15))) = multiplication(X0,addition(iPr_def_10,iPr_def_11)),
inference(superposition,[status(thm)],[c_942,c_56]) ).
tcf(c_2505,plain,
! [X0: $i] : addition(multiplication(X0,iPr_def_10),multiplication(X0,addition(iPr_def_11,iPr_def_15))) = X0,
inference(light_normalisation,[status(thm)],[c_2499,c_401,c_660]) ).
tcf(c_2799,plain,
! [X0: $i] : addition(multiplication(X0,iPr_def_19),X0) = X0,
inference(superposition,[status(thm)],[c_747,c_364]) ).
tcf(c_2805,plain,
! [X0: $i] : addition(X0,multiplication(X0,iPr_def_19)) = X0,
inference(theory_normalisation,[status(thm)],[c_2799,c_50,c_49]) ).
tcf(c_2841,plain,
iPr_def_11 = iPr_def_13,
inference(light_normalisation,[status(thm)],[c_1425,c_1451]) ).
tcf(c_2855,plain,
multiplication(iPr_def_11,iPr_def_15) = iPr_def_15,
inference(demodulation,[status(thm)],[c_813,c_2841]) ).
tcf(c_2991,plain,
! [X0: $i,X1: $i] :
( ( X1 = addition(iPr_def_11,zero) )
| ( X1 != X0 )
| ( addition(iPr_def_11,zero) != X0 ) ),
inference(instantiation,[status(thm)],[c_150]) ).
tcf(c_3818,plain,
multiplication(iPr_def_21,iPr_def_19) = iPr_def_19,
inference(demodulation,[status(thm)],[c_2064,c_621]) ).
tcf(c_3825,plain,
addition(iPr_def_21,iPr_def_19) = iPr_def_21,
inference(superposition,[status(thm)],[c_3818,c_2805]) ).
tcf(c_3827,plain,
addition(iPr_def_19,iPr_def_21) = iPr_def_21,
inference(theory_normalisation,[status(thm)],[c_3825,c_50,c_49]) ).
tcf(c_3836,plain,
addition(iPr_def_10,addition(iPr_def_11,iPr_def_21)) = addition(iPr_def_18,iPr_def_21),
inference(superposition,[status(thm)],[c_3827,c_439]) ).
tcf(c_3837,plain,
addition(iPr_def_10,iPr_def_11) = addition(iPr_def_18,iPr_def_21),
inference(light_normalisation,[status(thm)],[c_3836,c_935]) ).
tcf(c_3840,plain,
! [X0: $i] : addition(multiplication(X0,iPr_def_18),multiplication(X0,iPr_def_21)) = multiplication(X0,addition(iPr_def_10,iPr_def_11)),
inference(superposition,[status(thm)],[c_3837,c_56]) ).
tcf(c_3847,plain,
! [X0: $i] : addition(multiplication(X0,iPr_def_18),multiplication(X0,iPr_def_21)) = X0,
inference(light_normalisation,[status(thm)],[c_3840,c_401,c_660]) ).
tcf(c_4447,plain,
! [X0: $i] : multiplication(X0,addition(iPr_def_10,iPr_def_11)) = X0,
inference(light_normalisation,[status(thm)],[c_401,c_660]) ).
tcf(c_4448,plain,
! [X0: $i] : addition(multiplication(X0,iPr_def_10),multiplication(X0,iPr_def_11)) = X0,
inference(demodulation,[status(thm)],[c_4447,c_56]) ).
tcf(c_4454,plain,
addition(iPr_def_10,multiplication(iPr_def_12,iPr_def_11)) = iPr_def_12,
inference(superposition,[status(thm)],[c_1302,c_4448]) ).
tcf(c_4462,plain,
! [X0: $i,X1: $i] : addition(multiplication(X0,iPr_def_10),addition(multiplication(X0,iPr_def_11),X1)) = addition(X0,X1),
inference(superposition,[status(thm)],[c_4448,c_50]) ).
tcf(c_4469,plain,
addition(iPr_def_10,multiplication(iPr_def_11,iPr_def_10)) = iPr_def_12,
inference(light_normalisation,[status(thm)],[c_4454,c_335]) ).
tcf(c_4594,plain,
iPr_def_10 = iPr_def_12,
inference(demodulation,[status(thm)],[c_4469,c_318]) ).
tcf(c_4606,plain,
multiplication(iPr_def_10,iPr_def_15) = multiplication(iPr_def_11,iPr_def_10),
inference(demodulation,[status(thm)],[c_1618,c_4594]) ).
tcf(c_4617,plain,
multiplication(iPr_def_10,iPr_def_11) = multiplication(iPr_def_11,iPr_def_10),
inference(demodulation,[status(thm)],[c_335,c_4594]) ).
tcf(c_4628,plain,
multiplication(iPr_def_10,iPr_def_15) = multiplication(iPr_def_20,iPr_def_21),
inference(demodulation,[status(thm)],[c_2116,c_4606]) ).
tcf(c_4641,plain,
! [X0: $i] : addition(multiplication(iPr_def_10,iPr_def_15),X0) = X0,
inference(demodulation,[status(thm)],[c_621,c_4606]) ).
tcf(c_4689,plain,
multiplication(iPr_def_10,iPr_def_11) = multiplication(iPr_def_10,iPr_def_15),
inference(demodulation,[status(thm)],[c_4606,c_4617]) ).
tcf(c_4768,plain,
multiplication(iPr_def_10,iPr_def_11) = multiplication(iPr_def_20,iPr_def_21),
inference(light_normalisation,[status(thm)],[c_4628,c_4689]) ).
tcf(c_4777,plain,
addition(multiplication(iPr_def_20,iPr_def_18),multiplication(iPr_def_10,iPr_def_11)) = iPr_def_20,
inference(superposition,[status(thm)],[c_4768,c_3847]) ).
tcf(c_4783,plain,
addition(multiplication(iPr_def_10,iPr_def_11),multiplication(iPr_def_20,iPr_def_18)) = iPr_def_20,
inference(theory_normalisation,[status(thm)],[c_4777,c_50,c_49]) ).
tcf(c_4798,plain,
! [X0: $i] : addition(multiplication(iPr_def_10,iPr_def_11),X0) = X0,
inference(light_normalisation,[status(thm)],[c_4641,c_4689]) ).
tcf(c_7109,plain,
multiplication(iPr_def_20,iPr_def_18) = iPr_def_20,
inference(demodulation,[status(thm)],[c_4783,c_4798]) ).
tcf(c_7117,plain,
addition(iPr_def_18,iPr_def_20) = iPr_def_18,
inference(superposition,[status(thm)],[c_7109,c_2078]) ).
tcf(c_8716,plain,
! [X0: $i] : addition(X0,multiplication(X0,iPr_def_15)) = X0,
inference(demodulation,[status(thm)],[c_2505,c_56,c_4462]) ).
tcf(c_8724,plain,
addition(iPr_def_11,iPr_def_15) = iPr_def_11,
inference(superposition,[status(thm)],[c_2855,c_8716]) ).
tcf(c_74251,plain,
! [X0: $i] :
( ( iPr_def_28 = addition(iPr_def_11,zero) )
| ( iPr_def_28 != X0 )
| ( addition(iPr_def_11,zero) != X0 ) ),
inference(instantiation,[status(thm)],[c_2991]) ).
tcf(c_82712,plain,
( ( iPr_def_28 = addition(iPr_def_11,zero) )
| ( iPr_def_28 != iPr_def_28 )
| ( addition(iPr_def_11,zero) != iPr_def_28 ) ),
inference(instantiation,[status(thm)],[c_74251]) ).
tcf(c_105028,plain,
! [X0: $i,X1: $i,X2: $i] : addition(X0,addition(X1,X2)) = addition(X1,addition(X0,X2)),
inference(superposition,[status(thm)],[c_50,c_49]) ).
tcf(c_105029,plain,
antidomain(iPr_def_11) = iPr_def_10,
inference(light_normalisation,[status(thm)],[c_131,c_4594]) ).
tcf(c_105031,plain,
iPr_def_10 = iPr_def_14,
inference(light_normalisation,[status(thm)],[c_133,c_2841,c_105029]) ).
tcf(c_105037,plain,
addition(iPr_def_10,antidomain(iPr_def_10)) = one,
inference(superposition,[status(thm)],[c_105029,c_82]) ).
tcf(c_105038,plain,
addition(iPr_def_10,iPr_def_11) = one,
inference(light_normalisation,[status(thm)],[c_105037,c_130]) ).
tcf(c_105041,plain,
coantidomain(iPr_def_10) = iPr_def_15,
inference(light_normalisation,[status(thm)],[c_134,c_105031]) ).
tcf(c_105042,plain,
addition(iPr_def_20,antidomain(iPr_def_20)) = one,
inference(superposition,[status(thm)],[c_139,c_82]) ).
tcf(c_105043,plain,
addition(iPr_def_20,iPr_def_21) = one,
inference(light_normalisation,[status(thm)],[c_105042,c_140]) ).
tcf(c_105046,plain,
addition(iPr_def_22,antidomain(iPr_def_22)) = one,
inference(superposition,[status(thm)],[c_141,c_82]) ).
tcf(c_105047,plain,
addition(iPr_def_22,iPr_def_23) = one,
inference(light_normalisation,[status(thm)],[c_105046,c_142]) ).
tcf(c_105050,plain,
addition(iPr_def_24,antidomain(iPr_def_24)) = one,
inference(superposition,[status(thm)],[c_143,c_82]) ).
tcf(c_105053,plain,
addition(iPr_def_27,antidomain(iPr_def_27)) = one,
inference(superposition,[status(thm)],[c_146,c_82]) ).
tcf(c_105059,plain,
addition(iPr_def_18,coantidomain(iPr_def_18)) = one,
inference(superposition,[status(thm)],[c_137,c_83]) ).
tcf(c_105061,plain,
addition(iPr_def_15,coantidomain(iPr_def_15)) = one,
inference(superposition,[status(thm)],[c_105041,c_83]) ).
tcf(c_105062,plain,
addition(iPr_def_15,iPr_def_16) = one,
inference(light_normalisation,[status(thm)],[c_105061,c_135]) ).
tcf(c_105063,plain,
addition(iPr_def_18,iPr_def_19) = one,
inference(light_normalisation,[status(thm)],[c_105059,c_138]) ).
tcf(c_105067,plain,
multiplication(iPr_def_10,iPr_def_11) = zero,
inference(superposition,[status(thm)],[c_105029,c_60]) ).
tcf(c_105073,plain,
multiplication(iPr_def_26,iPr_def_25) = zero,
inference(superposition,[status(thm)],[c_145,c_60]) ).
tcf(c_105075,plain,
antidomain(one) = zero,
inference(superposition,[status(thm)],[c_60,c_54]) ).
tcf(c_105077,plain,
addition(zero,antidomain(zero)) = one,
inference(superposition,[status(thm)],[c_105075,c_82]) ).
tcf(c_105082,plain,
multiplication(iPr_def_17,iPr_def_18) = zero,
inference(superposition,[status(thm)],[c_137,c_63]) ).
tcf(c_105090,plain,
! [X0: $i] : addition(zero,X0) = X0,
inference(superposition,[status(thm)],[c_49,c_51]) ).
tcf(c_105095,plain,
! [X0: $i,X1: $i] : addition(X0,addition(X0,X1)) = addition(X0,X1),
inference(superposition,[status(thm)],[c_52,c_50]) ).
tcf(c_105098,plain,
! [X0: $i] : addition(iPr_def_11,addition(iPr_def_27,X0)) = addition(iPr_def_28,X0),
inference(superposition,[status(thm)],[c_147,c_50]) ).
tcf(c_105099,plain,
! [X0: $i] : addition(iPr_def_10,addition(iPr_def_11,X0)) = addition(one,X0),
inference(superposition,[status(thm)],[c_105038,c_50]) ).
tcf(c_105107,plain,
! [X0: $i] : addition(iPr_def_11,addition(iPr_def_15,X0)) = addition(iPr_def_11,X0),
inference(superposition,[status(thm)],[c_8724,c_50]) ).
tcf(c_105109,plain,
! [X0: $i] : addition(iPr_def_18,addition(iPr_def_20,X0)) = addition(iPr_def_18,X0),
inference(superposition,[status(thm)],[c_7117,c_50]) ).
tcf(c_105122,plain,
! [X0: $i,X1: $i] : multiplication(antidomain(X0),multiplication(X0,X1)) = multiplication(zero,X1),
inference(superposition,[status(thm)],[c_60,c_53]) ).
tcf(c_105124,plain,
! [X0: $i] : multiplication(iPr_def_16,multiplication(sK0,X0)) = multiplication(iPr_def_17,X0),
inference(superposition,[status(thm)],[c_136,c_53]) ).
tcf(c_105135,plain,
! [X0: $i] : multiplication(iPr_def_10,multiplication(iPr_def_11,X0)) = multiplication(zero,X0),
inference(superposition,[status(thm)],[c_105067,c_53]) ).
tcf(c_105136,plain,
! [X0: $i] : multiplication(iPr_def_10,multiplication(iPr_def_11,X0)) = zero,
inference(light_normalisation,[status(thm)],[c_105135,c_59]) ).
tcf(c_105164,plain,
! [X0: $i,X1: $i] : multiplication(antidomain(X0),addition(X0,X1)) = addition(zero,multiplication(antidomain(X0),X1)),
inference(superposition,[status(thm)],[c_60,c_56]) ).
tcf(c_105165,plain,
! [X0: $i,X1: $i] : multiplication(X0,addition(coantidomain(X0),X1)) = addition(zero,multiplication(X0,X1)),
inference(superposition,[status(thm)],[c_63,c_56]) ).
tcf(c_105182,plain,
! [X0: $i,X1: $i] : addition(multiplication(X0,X1),zero) = multiplication(X0,addition(X1,zero)),
inference(superposition,[status(thm)],[c_58,c_56]) ).
tcf(c_105219,plain,
! [X0: $i,X1: $i] : addition(zero,multiplication(X0,X1)) = multiplication(X0,addition(X1,zero)),
inference(theory_normalisation,[status(thm)],[c_105182,c_50,c_49]) ).
tcf(c_105231,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_105234,plain,
! [X0: $i,X1: $i] : multiplication(addition(antidomain(X0),X1),X0) = addition(zero,multiplication(X1,X0)),
inference(superposition,[status(thm)],[c_60,c_57]) ).
tcf(c_105245,plain,
! [X0: $i] : addition(zero,multiplication(X0,iPr_def_25)) = multiplication(addition(iPr_def_26,X0),iPr_def_25),
inference(superposition,[status(thm)],[c_105073,c_57]) ).
tcf(c_105450,plain,
antidomain(zero) = one,
inference(demodulation,[status(thm)],[c_105077,c_105090]) ).
tcf(c_105519,plain,
! [X0: $i] : addition(antidomain(zero),antidomain(multiplication(iPr_def_10,antidomain(antidomain(multiplication(iPr_def_11,X0)))))) = antidomain(multiplication(iPr_def_10,antidomain(antidomain(multiplication(iPr_def_11,X0))))),
inference(superposition,[status(thm)],[c_105136,c_61]) ).
tcf(c_105529,plain,
! [X0: $i] : addition(one,antidomain(multiplication(iPr_def_10,antidomain(antidomain(multiplication(iPr_def_11,X0)))))) = antidomain(multiplication(iPr_def_10,antidomain(antidomain(multiplication(iPr_def_11,X0))))),
inference(light_normalisation,[status(thm)],[c_105519,c_105450]) ).
tcf(c_105847,plain,
! [X0: $i] : addition(antidomain(X0),one) = one,
inference(superposition,[status(thm)],[c_82,c_105095]) ).
tcf(c_105849,plain,
addition(iPr_def_11,iPr_def_28) = iPr_def_28,
inference(superposition,[status(thm)],[c_147,c_105095]) ).
tcf(c_105854,plain,
addition(iPr_def_18,one) = one,
inference(superposition,[status(thm)],[c_105063,c_105095]) ).
tcf(c_105856,plain,
addition(iPr_def_24,one) = one,
inference(superposition,[status(thm)],[c_105050,c_105095]) ).
tcf(c_105857,plain,
addition(iPr_def_27,one) = one,
inference(superposition,[status(thm)],[c_105053,c_105095]) ).
tcf(c_105874,plain,
! [X0: $i] : addition(one,antidomain(X0)) = one,
inference(theory_normalisation,[status(thm)],[c_105847,c_50,c_49]) ).
tcf(c_105907,plain,
addition(one,iPr_def_11) = one,
inference(superposition,[status(thm)],[c_130,c_105874]) ).
tcf(c_105919,plain,
! [X0: $i,X1: $i] : addition(one,addition(X0,antidomain(X1))) = addition(X0,one),
inference(superposition,[status(thm)],[c_105874,c_105028]) ).
tcf(c_105929,plain,
addition(iPr_def_11,one) = one,
inference(theory_normalisation,[status(thm)],[c_105907,c_50,c_49]) ).
tcf(c_105985,plain,
addition(iPr_def_11,one) = addition(iPr_def_28,one),
inference(superposition,[status(thm)],[c_105857,c_105098]) ).
tcf(c_105990,plain,
addition(iPr_def_28,one) = one,
inference(light_normalisation,[status(thm)],[c_105985,c_105929]) ).
tcf(c_106013,plain,
addition(one,iPr_def_28) = addition(iPr_def_10,iPr_def_28),
inference(superposition,[status(thm)],[c_105849,c_105099]) ).
tcf(c_106023,plain,
addition(iPr_def_10,iPr_def_28) = addition(iPr_def_28,one),
inference(theory_normalisation,[status(thm)],[c_106013,c_50,c_49]) ).
tcf(c_106024,plain,
addition(iPr_def_10,iPr_def_28) = one,
inference(light_normalisation,[status(thm)],[c_106023,c_105990]) ).
tcf(c_106247,plain,
addition(iPr_def_11,one) = addition(iPr_def_11,iPr_def_16),
inference(superposition,[status(thm)],[c_105062,c_105107]) ).
tcf(c_106254,plain,
addition(iPr_def_11,iPr_def_16) = one,
inference(light_normalisation,[status(thm)],[c_106247,c_105929]) ).
tcf(c_106293,plain,
addition(iPr_def_18,one) = addition(iPr_def_18,iPr_def_21),
inference(superposition,[status(thm)],[c_105043,c_105109]) ).
tcf(c_106299,plain,
addition(iPr_def_18,iPr_def_21) = one,
inference(light_normalisation,[status(thm)],[c_106293,c_105854]) ).
tcf(c_106312,plain,
multiplication(iPr_def_16,iPr_def_25) = multiplication(iPr_def_17,iPr_def_24),
inference(superposition,[status(thm)],[c_144,c_105124]) ).
tcf(c_108810,plain,
! [X0: $i,X1: $i] : multiplication(antidomain(X0),multiplication(X0,X1)) = zero,
inference(demodulation,[status(thm)],[c_105122,c_59]) ).
tcf(c_112846,plain,
! [X0: $i,X1: $i] : multiplication(antidomain(X0),addition(X0,X1)) = multiplication(antidomain(X0),X1),
inference(demodulation,[status(thm)],[c_105164,c_51,c_105219]) ).
tcf(c_112854,plain,
! [X0: $i] : multiplication(iPr_def_22,addition(iPr_def_21,X0)) = multiplication(iPr_def_22,X0),
inference(superposition,[status(thm)],[c_141,c_112846]) ).
tcf(c_112856,plain,
! [X0: $i] : multiplication(iPr_def_24,addition(iPr_def_23,X0)) = multiplication(iPr_def_24,X0),
inference(superposition,[status(thm)],[c_143,c_112846]) ).
tcf(c_112869,plain,
multiplication(antidomain(iPr_def_11),iPr_def_27) = multiplication(antidomain(iPr_def_11),iPr_def_28),
inference(superposition,[status(thm)],[c_147,c_112846]) ).
tcf(c_112871,plain,
multiplication(antidomain(iPr_def_10),one) = multiplication(antidomain(iPr_def_10),iPr_def_11),
inference(superposition,[status(thm)],[c_105038,c_112846]) ).
tcf(c_112927,plain,
multiplication(antidomain(iPr_def_10),one) = multiplication(antidomain(iPr_def_10),iPr_def_28),
inference(superposition,[status(thm)],[c_106024,c_112846]) ).
tcf(c_112929,plain,
multiplication(antidomain(iPr_def_11),one) = multiplication(antidomain(iPr_def_11),iPr_def_16),
inference(superposition,[status(thm)],[c_106254,c_112846]) ).
tcf(c_113000,plain,
multiplication(iPr_def_10,one) = multiplication(iPr_def_10,iPr_def_16),
inference(light_normalisation,[status(thm)],[c_112929,c_105029]) ).
tcf(c_113002,plain,
multiplication(iPr_def_11,one) = multiplication(iPr_def_11,iPr_def_28),
inference(light_normalisation,[status(thm)],[c_112927,c_130]) ).
tcf(c_113009,plain,
multiplication(iPr_def_11,one) = multiplication(iPr_def_11,iPr_def_11),
inference(light_normalisation,[status(thm)],[c_112871,c_130]) ).
tcf(c_113010,plain,
multiplication(iPr_def_10,iPr_def_27) = multiplication(iPr_def_10,iPr_def_28),
inference(light_normalisation,[status(thm)],[c_112869,c_105029]) ).
tcf(c_113230,plain,
multiplication(iPr_def_10,iPr_def_16) = iPr_def_10,
inference(demodulation,[status(thm)],[c_113000,c_54]) ).
tcf(c_113238,plain,
! [X0: $i] : multiplication(iPr_def_10,multiplication(iPr_def_16,X0)) = multiplication(iPr_def_10,X0),
inference(superposition,[status(thm)],[c_113230,c_53]) ).
tcf(c_113249,plain,
multiplication(iPr_def_11,iPr_def_11) = multiplication(iPr_def_11,iPr_def_28),
inference(demodulation,[status(thm)],[c_113002,c_113009]) ).
tcf(c_113416,plain,
multiplication(iPr_def_11,iPr_def_11) = iPr_def_11,
inference(demodulation,[status(thm)],[c_113009,c_54]) ).
tcf(c_113417,plain,
multiplication(iPr_def_11,iPr_def_28) = iPr_def_11,
inference(demodulation,[status(thm)],[c_113249,c_113416]) ).
tcf(c_113440,plain,
! [X0: $i] : addition(iPr_def_11,multiplication(X0,iPr_def_28)) = multiplication(addition(iPr_def_11,X0),iPr_def_28),
inference(superposition,[status(thm)],[c_113417,c_57]) ).
tcf(c_113452,plain,
! [X0: $i,X1: $i] : multiplication(X0,addition(coantidomain(X0),X1)) = multiplication(X0,X1),
inference(demodulation,[status(thm)],[c_105165,c_51,c_105219]) ).
tcf(c_113466,plain,
! [X0: $i] : multiplication(iPr_def_17,addition(iPr_def_18,X0)) = multiplication(iPr_def_17,X0),
inference(superposition,[status(thm)],[c_137,c_113452]) ).
tcf(c_113704,plain,
! [X0: $i] : multiplication(iPr_def_22,addition(X0,iPr_def_21)) = multiplication(iPr_def_22,X0),
inference(superposition,[status(thm)],[c_49,c_112854]) ).
tcf(c_113767,plain,
! [X0: $i] : multiplication(iPr_def_24,addition(X0,iPr_def_23)) = multiplication(iPr_def_24,X0),
inference(superposition,[status(thm)],[c_49,c_112856]) ).
tcf(c_115132,plain,
multiplication(iPr_def_22,one) = multiplication(iPr_def_22,iPr_def_18),
inference(superposition,[status(thm)],[c_106299,c_113704]) ).
tcf(c_115187,plain,
multiplication(iPr_def_24,one) = multiplication(iPr_def_24,iPr_def_22),
inference(superposition,[status(thm)],[c_105047,c_113767]) ).
tcf(c_115229,plain,
multiplication(iPr_def_22,iPr_def_18) = iPr_def_22,
inference(demodulation,[status(thm)],[c_115132,c_54]) ).
tcf(c_115285,plain,
multiplication(iPr_def_24,iPr_def_22) = iPr_def_24,
inference(demodulation,[status(thm)],[c_115187,c_54]) ).
tcf(c_115293,plain,
! [X0: $i] : multiplication(iPr_def_24,multiplication(iPr_def_22,X0)) = multiplication(iPr_def_24,X0),
inference(superposition,[status(thm)],[c_115285,c_53]) ).
tcf(c_116201,plain,
multiplication(iPr_def_24,iPr_def_18) = multiplication(iPr_def_24,iPr_def_22),
inference(superposition,[status(thm)],[c_115229,c_115293]) ).
tcf(c_116221,plain,
multiplication(iPr_def_24,iPr_def_18) = iPr_def_24,
inference(light_normalisation,[status(thm)],[c_116201,c_115285]) ).
tcf(c_120420,plain,
! [X0: $i,X1: $i] : addition(one,antidomain(multiplication(X0,antidomain(antidomain(X1))))) = addition(antidomain(multiplication(X0,X1)),one),
inference(superposition,[status(thm)],[c_61,c_105919]) ).
tcf(c_120489,plain,
! [X0: $i,X1: $i] : addition(one,antidomain(multiplication(X0,antidomain(antidomain(X1))))) = addition(one,antidomain(multiplication(X0,X1))),
inference(theory_normalisation,[status(thm)],[c_120420,c_50,c_49]) ).
tcf(c_123361,plain,
! [X0: $i,X1: $i] : multiplication(addition(one,antidomain(X0)),multiplication(X0,X1)) = addition(multiplication(X0,X1),zero),
inference(superposition,[status(thm)],[c_108810,c_105231]) ).
tcf(c_123559,plain,
multiplication(addition(one,iPr_def_24),iPr_def_18) = addition(iPr_def_18,iPr_def_24),
inference(superposition,[status(thm)],[c_116221,c_105231]) ).
tcf(c_123718,plain,
multiplication(addition(iPr_def_24,one),iPr_def_18) = addition(iPr_def_18,iPr_def_24),
inference(theory_normalisation,[status(thm)],[c_123559,c_50,c_49]) ).
tcf(c_123719,plain,
addition(iPr_def_18,iPr_def_24) = multiplication(one,iPr_def_18),
inference(light_normalisation,[status(thm)],[c_123718,c_105856]) ).
tcf(c_123974,plain,
! [X0: $i,X1: $i] : multiplication(addition(one,antidomain(X0)),multiplication(X0,X1)) = addition(zero,multiplication(X0,X1)),
inference(theory_normalisation,[status(thm)],[c_123361,c_50,c_49]) ).
tcf(c_123975,plain,
! [X0: $i,X1: $i] : addition(zero,multiplication(X0,X1)) = multiplication(one,multiplication(X0,X1)),
inference(light_normalisation,[status(thm)],[c_123974,c_105874]) ).
tcf(c_124331,plain,
addition(iPr_def_18,iPr_def_24) = iPr_def_18,
inference(demodulation,[status(thm)],[c_123719,c_55]) ).
tcf(c_124339,plain,
multiplication(iPr_def_17,iPr_def_18) = multiplication(iPr_def_17,iPr_def_24),
inference(superposition,[status(thm)],[c_124331,c_113466]) ).
tcf(c_124340,plain,
multiplication(iPr_def_16,iPr_def_25) = zero,
inference(light_normalisation,[status(thm)],[c_124339,c_106312,c_105082]) ).
tcf(c_124362,plain,
multiplication(iPr_def_10,zero) = multiplication(iPr_def_10,iPr_def_25),
inference(superposition,[status(thm)],[c_124340,c_113238]) ).
tcf(c_126431,plain,
multiplication(iPr_def_10,iPr_def_25) = zero,
inference(demodulation,[status(thm)],[c_124362,c_58]) ).
tcf(c_126440,plain,
! [X0: $i] : addition(zero,multiplication(X0,iPr_def_25)) = multiplication(addition(iPr_def_10,X0),iPr_def_25),
inference(superposition,[status(thm)],[c_126431,c_57]) ).
tcf(c_126541,plain,
! [X0: $i,X1: $i] : multiplication(addition(antidomain(X0),X1),X0) = multiplication(X1,X0),
inference(demodulation,[status(thm)],[c_105234,c_55,c_123975]) ).
tcf(c_126562,plain,
! [X0: $i] : multiplication(addition(iPr_def_26,X0),iPr_def_25) = multiplication(X0,iPr_def_25),
inference(superposition,[status(thm)],[c_145,c_126541]) ).
tcf(c_131441,plain,
! [X0: $i] : multiplication(addition(iPr_def_10,X0),iPr_def_25) = multiplication(X0,iPr_def_25),
inference(light_normalisation,[status(thm)],[c_105245,c_126440,c_126562]) ).
tcf(c_131448,plain,
multiplication(one,iPr_def_25) = multiplication(iPr_def_11,iPr_def_25),
inference(superposition,[status(thm)],[c_105038,c_131441]) ).
tcf(c_131674,plain,
multiplication(iPr_def_11,iPr_def_25) = iPr_def_25,
inference(demodulation,[status(thm)],[c_131448,c_55]) ).
tcf(c_164668,plain,
addition(iPr_def_11,multiplication(iPr_def_10,iPr_def_27)) = multiplication(addition(iPr_def_11,iPr_def_10),iPr_def_28),
inference(superposition,[status(thm)],[c_113010,c_113440]) ).
tcf(c_164694,plain,
addition(iPr_def_11,multiplication(iPr_def_10,iPr_def_27)) = multiplication(addition(iPr_def_10,iPr_def_11),iPr_def_28),
inference(theory_normalisation,[status(thm)],[c_164668,c_50,c_49]) ).
tcf(c_164695,plain,
addition(iPr_def_11,multiplication(iPr_def_10,iPr_def_27)) = multiplication(one,iPr_def_28),
inference(light_normalisation,[status(thm)],[c_164694,c_105038]) ).
tcf(c_164764,plain,
addition(iPr_def_11,multiplication(iPr_def_10,iPr_def_27)) = iPr_def_28,
inference(demodulation,[status(thm)],[c_164695,c_55]) ).
tcf(c_192632,plain,
! [X0: $i] : antidomain(multiplication(iPr_def_10,antidomain(antidomain(multiplication(iPr_def_11,X0))))) = one,
inference(demodulation,[status(thm)],[c_105529,c_105874,c_120489]) ).
tcf(c_192654,plain,
antidomain(multiplication(iPr_def_10,antidomain(antidomain(iPr_def_25)))) = one,
inference(superposition,[status(thm)],[c_131674,c_192632]) ).
tcf(c_192736,plain,
antidomain(multiplication(iPr_def_10,iPr_def_27)) = one,
inference(light_normalisation,[status(thm)],[c_192654,c_145,c_146]) ).
tcf(c_192776,plain,
multiplication(one,multiplication(iPr_def_10,iPr_def_27)) = zero,
inference(superposition,[status(thm)],[c_192736,c_60]) ).
tcf(c_192803,plain,
multiplication(iPr_def_10,iPr_def_27) = zero,
inference(demodulation,[status(thm)],[c_192776,c_55]) ).
tcf(c_192805,plain,
addition(iPr_def_11,zero) = iPr_def_28,
inference(demodulation,[status(thm)],[c_164764,c_192803]) ).
tcf(c_192889,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_192805,c_82712,c_1772,c_1214,c_1213,c_1136,c_1076,c_148]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : KLE109+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.08/0.35 % Computer : n016.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Wed Sep 23 19:02:50 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.36 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.13/0.42 Running first-order theorem proving
% 0.13/0.42 Running: /export/starexec/sandbox2/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.13/0.43
% 0.13/0.43 % ======== iProver multi-core TPTP/SMT =========
% 0.13/0.43
% 0.13/0.44 % Detected problem language: tptp
% 0.13/0.45 % Proving...
% 121.31/19.65 % SZS status Started for theBenchmark.p
% 121.31/19.65 % SZS status Theorem for theBenchmark.p
% 121.31/19.65
% 121.31/19.65 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 121.31/19.65
% 121.31/19.65 % ------ iProver source info
% 121.31/19.65
% 121.31/19.65 % git: date: 2026-07-19 20:42:38 +0200
% 121.31/19.65 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 121.31/19.65 % git: non_committed_changes: false
% 121.31/19.65
% 121.31/19.65 % ------ Parsing...
% 121.31/19.65 % ------ Clausification by vclausify_rel & Parsing by iProver...% ------ preprocesses with Option_UEQ
% 121.31/19.65 %
% 121.31/19.65
% 121.31/19.65 % ------ Preprocessing... sup_sim: 0 sf_s rm: 0 0s sf_e pe_s pe_e %
% 121.31/19.65
% 121.31/19.65 % ------ Preprocessing...% ------ preprocesses with Option_UEQ
% 121.31/19.65 gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 121.31/19.65
% 121.31/19.65 % ------ Preprocessing... sf_s rm: 0 0s sf_e
% 121.31/19.65 % ------ Proving...
% 121.31/19.65 % ------ Problem Properties
% 121.31/19.65
% 121.31/19.65 %
% 121.31/19.65 % clauses 37
% 121.31/19.65 % conjectures 1
% 121.31/19.65 % EPR 1
% 121.31/19.65 % Horn 37
% 121.31/19.65 % unary 37
% 121.31/19.65 % binary 0
% 121.31/19.65 % lits 37
% 121.31/19.66 % lits eq 37
% 121.31/19.66 % fd_pure 0
% 121.31/19.66 % fd_pseudo 0
% 121.31/19.66 % fd_cond 0
% 121.31/19.66 % fd_pseudo_cond 0
% 121.31/19.66 % AC symbols 1
% 121.31/19.66
% 121.31/19.66 % ------ Schedule UEQ
% 121.31/19.66
% 121.31/19.66 % ------ Option_UEQ Time Limit: 10.
% 121.31/19.66
% 121.31/19.66
% 121.31/19.66 % ------
% 121.31/19.66 % Current options:
% 121.31/19.66 % ------
% 121.31/19.66
% 121.31/19.66
% 121.31/19.66 %
% 121.31/19.66
% 121.31/19.66 % ------ Proving...
% 121.31/19.66 % Proof_search_loop: time out after: 2148 full_loop iterations
% 121.31/19.66
% 121.31/19.66 % ------ Option_UEQ Time Limit: 15.
% 121.31/19.66
% 121.31/19.66
% 121.31/19.66 % ------
% 121.31/19.66 % Current options:
% 121.31/19.66 % ------
% 121.31/19.66
% 121.31/19.66
% 121.31/19.66 %
% 121.31/19.66
% 121.31/19.66 % ------ Proving...
% 121.31/19.66 %
% 121.31/19.66
% 121.31/19.66 % SZS status Theorem for theBenchmark.p
% 121.31/19.66
% 121.31/19.66 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 121.31/19.67
% 121.31/19.67
%------------------------------------------------------------------------------