%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : KLE118+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 : n012.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:27 PM UTC 2026
% Result : Theorem 69.02s 16.63s
% Output : CNFRefutation 69.02s
% Verified :
% SZS Type : Refutation
% Derivation depth : 33
% Number of leaves : 41
% Syntax : Number of formulae : 258 ( 254 unt; 21 def)
% Number of atoms : 677 ( 261 equ)
% Maximal formula atoms : 2 ( 2 avg)
% Number of connectives : 13 ( 9 ~; 0 |; 2 &)
% ( 0 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 2 avg)
% Maximal term depth : 15 ( 2 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 23 ( 21 usr; 22 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 5 con; 0-2 aty)
% Number of variables : 166 ( 0 sgn 163 !; 3 ?; 90 :)
% 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(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(f25,axiom,
! [X0,X1] : forward_box(X0,X1) = c(forward_diamond(X0,c(X1))),
file('/export/starexec/sandbox2/benchmark/Axioms/KLE001+6.ax',forward_box) ).
fof(f27,conjecture,
! [X0,X1] :
( addition(X0,X1) = X1
=> ! [X2] : addition(forward_box(X0,domain(X2)),forward_box(X1,domain(X2))) = forward_box(X0,domain(X2)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goals) ).
fof(f28,negated_conjecture,
~ ! [X0,X1] :
( addition(X0,X1) = X1
=> ! [X2] : addition(forward_box(X0,domain(X2)),forward_box(X1,domain(X2))) = forward_box(X0,domain(X2)) ),
inference(negated_conjecture,[status(cth)],[f27]) ).
fof(f29,plain,
? [X0,X1] :
( addition(X0,X1) = X1
& ? [X2] : forward_box(X0,domain(X2)) != addition(forward_box(X0,domain(X2)),forward_box(X1,domain(X2))) ),
inference(ennf_transformation,[],[f28]) ).
fof(f30,plain,
( sK1 = addition(sK0,sK1)
& forward_box(sK0,domain(sK2)) != addition(forward_box(sK0,domain(sK2)),forward_box(sK1,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(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(f54,plain,
! [X0,X1] : forward_box(X0,X1) = c(forward_diamond(X0,c(X1))),
inference(cnf_transformation,[],[f25]) ).
fof(f56,plain,
sK1 = addition(sK0,sK1),
inference(cnf_transformation,[],[f30]) ).
fof(f57,plain,
forward_box(sK0,domain(sK2)) != addition(forward_box(sK0,domain(sK2)),forward_box(sK1,domain(sK2))),
inference(cnf_transformation,[],[f30]) ).
fof(f58,plain,
! [X0] : c(X0) = antidomain(antidomain(antidomain(X0))),
inference(definition_unfolding,[],[f50,f45]) ).
fof(f62,plain,
! [X0,X1] : forward_diamond(X0,X1) = antidomain(antidomain(multiplication(X0,antidomain(antidomain(X1))))),
inference(definition_unfolding,[],[f52,f45,f45]) ).
fof(f63,plain,
! [X0,X1] : forward_box(X0,X1) = antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(X0,antidomain(antidomain(antidomain(antidomain(antidomain(X1))))))))))),
inference(definition_unfolding,[],[f54,f58,f62,f58]) ).
fof(f64,plain,
antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sK2))))))))))))) != addition(antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sK2))))))))))))),antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK1,antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sK2)))))))))))))),
inference(definition_unfolding,[],[f57,f63,f45,f63,f45,f63,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_66,negated_conjecture,
addition(antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sK2))))))))))))),antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK1,antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sK2)))))))))))))) != antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sK2))))))))))))),
inference(cnf_transformation,[],[f64]) ).
tcf(c_67,negated_conjecture,
addition(sK0,sK1) = sK1,
inference(cnf_transformation,[],[f56]) ).
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_131,definition,
iPr_def_10 = addition(sK0,sK1),
introduced(definition,[new_symbols(definition,[iPr_def_10])],[]) ).
tcf(c_132,definition,
iPr_def_11 = antidomain(sK2),
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 = antidomain(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(iPr_def_16),
introduced(definition,[new_symbols(definition,[iPr_def_17])],[]) ).
tcf(c_139,definition,
iPr_def_18 = multiplication(sK0,iPr_def_17),
introduced(definition,[new_symbols(definition,[iPr_def_18])],[]) ).
tcf(c_140,definition,
iPr_def_19 = antidomain(iPr_def_18),
introduced(definition,[new_symbols(definition,[iPr_def_19])],[]) ).
tcf(c_141,definition,
iPr_def_20 = antidomain(iPr_def_19),
introduced(definition,[new_symbols(definition,[iPr_def_20])],[]) ).
tcf(c_142,definition,
iPr_def_21 = antidomain(iPr_def_20),
introduced(definition,[new_symbols(definition,[iPr_def_21])],[]) ).
tcf(c_143,definition,
iPr_def_22 = antidomain(iPr_def_21),
introduced(definition,[new_symbols(definition,[iPr_def_22])],[]) ).
tcf(c_144,definition,
iPr_def_23 = antidomain(iPr_def_22),
introduced(definition,[new_symbols(definition,[iPr_def_23])],[]) ).
tcf(c_145,definition,
iPr_def_24 = multiplication(sK1,iPr_def_17),
introduced(definition,[new_symbols(definition,[iPr_def_24])],[]) ).
tcf(c_146,definition,
iPr_def_25 = antidomain(iPr_def_24),
introduced(definition,[new_symbols(definition,[iPr_def_25])],[]) ).
tcf(c_147,definition,
iPr_def_26 = antidomain(iPr_def_25),
introduced(definition,[new_symbols(definition,[iPr_def_26])],[]) ).
tcf(c_148,definition,
iPr_def_27 = antidomain(iPr_def_26),
introduced(definition,[new_symbols(definition,[iPr_def_27])],[]) ).
tcf(c_149,definition,
iPr_def_28 = antidomain(iPr_def_27),
introduced(definition,[new_symbols(definition,[iPr_def_28])],[]) ).
tcf(c_150,definition,
iPr_def_29 = antidomain(iPr_def_28),
introduced(definition,[new_symbols(definition,[iPr_def_29])],[]) ).
tcf(c_151,definition,
iPr_def_30 = addition(iPr_def_23,iPr_def_29),
introduced(definition,[new_symbols(definition,[iPr_def_30])],[]) ).
tcf(c_152,negated_conjecture,
iPr_def_10 = sK1,
inference(demodulation,[status(thm)],[c_67,c_131]) ).
tcf(c_153,negated_conjecture,
iPr_def_30 != iPr_def_23,
inference(demodulation,[status(thm)],[c_66,c_145,c_146,c_147,c_148,c_149,c_150,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_151]) ).
tcf(c_232908,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_232928,plain,
addition(iPr_def_19,antidomain(iPr_def_19)) = one,
inference(superposition,[status(thm)],[c_140,c_83]) ).
tcf(c_232929,plain,
addition(iPr_def_19,iPr_def_20) = one,
inference(light_normalisation,[status(thm)],[c_232928,c_141]) ).
tcf(c_232930,plain,
addition(iPr_def_20,antidomain(iPr_def_20)) = one,
inference(superposition,[status(thm)],[c_141,c_83]) ).
tcf(c_232931,plain,
addition(iPr_def_20,iPr_def_21) = one,
inference(light_normalisation,[status(thm)],[c_232930,c_142]) ).
tcf(c_232932,plain,
addition(iPr_def_21,antidomain(iPr_def_21)) = one,
inference(superposition,[status(thm)],[c_142,c_83]) ).
tcf(c_232933,plain,
addition(iPr_def_21,iPr_def_22) = one,
inference(light_normalisation,[status(thm)],[c_232932,c_143]) ).
tcf(c_232934,plain,
addition(iPr_def_22,antidomain(iPr_def_22)) = one,
inference(superposition,[status(thm)],[c_143,c_83]) ).
tcf(c_232935,plain,
addition(iPr_def_22,iPr_def_23) = one,
inference(light_normalisation,[status(thm)],[c_232934,c_144]) ).
tcf(c_232937,plain,
addition(iPr_def_25,antidomain(iPr_def_25)) = one,
inference(superposition,[status(thm)],[c_146,c_83]) ).
tcf(c_232938,plain,
addition(iPr_def_25,iPr_def_26) = one,
inference(light_normalisation,[status(thm)],[c_232937,c_147]) ).
tcf(c_232947,plain,
addition(sK0,iPr_def_10) = iPr_def_10,
inference(light_normalisation,[status(thm)],[c_131,c_152]) ).
tcf(c_232948,plain,
addition(iPr_def_10,sK0) = iPr_def_10,
inference(demodulation,[status(thm)],[c_232947,c_49]) ).
tcf(c_232949,plain,
multiplication(iPr_def_10,iPr_def_17) = iPr_def_24,
inference(light_normalisation,[status(thm)],[c_145,c_152]) ).
tcf(c_232973,plain,
! [X0: $i,X1: $i] : addition(antidomain(X0),addition(X1,antidomain(antidomain(X0)))) = addition(X1,one),
inference(superposition,[status(thm)],[c_83,c_232908]) ).
tcf(c_233010,plain,
multiplication(iPr_def_25,iPr_def_24) = zero,
inference(superposition,[status(thm)],[c_146,c_60]) ).
tcf(c_233015,plain,
antidomain(one) = zero,
inference(superposition,[status(thm)],[c_60,c_54]) ).
tcf(c_233022,plain,
! [X0: $i] : addition(zero,X0) = X0,
inference(superposition,[status(thm)],[c_49,c_51]) ).
tcf(c_233027,plain,
! [X0: $i,X1: $i] : addition(X0,addition(X0,X1)) = addition(X0,X1),
inference(superposition,[status(thm)],[c_52,c_50]) ).
tcf(c_233030,plain,
! [X0: $i] : addition(iPr_def_23,addition(iPr_def_29,X0)) = addition(iPr_def_30,X0),
inference(superposition,[status(thm)],[c_151,c_50]) ).
tcf(c_233039,plain,
! [X0: $i] : addition(iPr_def_22,addition(iPr_def_23,X0)) = addition(one,X0),
inference(superposition,[status(thm)],[c_232935,c_50]) ).
tcf(c_233049,plain,
addition(zero,antidomain(zero)) = one,
inference(superposition,[status(thm)],[c_233015,c_83]) ).
tcf(c_233177,plain,
! [X0: $i,X1: $i] : multiplication(antidomain(X0),multiplication(X0,X1)) = multiplication(zero,X1),
inference(superposition,[status(thm)],[c_60,c_53]) ).
tcf(c_233188,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_233192,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_233193,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_233199,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_233215,plain,
! [X0: $i,X1: $i] : addition(zero,multiplication(X0,X1)) = multiplication(X0,addition(X1,zero)),
inference(theory_normalisation,[status(thm)],[c_233199,c_50,c_49]) ).
tcf(c_233226,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_233229,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_233232,plain,
! [X0: $i] : addition(iPr_def_24,multiplication(X0,iPr_def_17)) = multiplication(addition(iPr_def_10,X0),iPr_def_17),
inference(superposition,[status(thm)],[c_232949,c_57]) ).
tcf(c_233375,plain,
multiplication(addition(iPr_def_10,sK0),iPr_def_17) = addition(iPr_def_24,iPr_def_18),
inference(superposition,[status(thm)],[c_139,c_233232]) ).
tcf(c_233381,plain,
multiplication(addition(iPr_def_10,sK0),iPr_def_17) = addition(iPr_def_18,iPr_def_24),
inference(theory_normalisation,[status(thm)],[c_233375,c_50,c_49]) ).
tcf(c_233382,plain,
addition(iPr_def_18,iPr_def_24) = iPr_def_24,
inference(light_normalisation,[status(thm)],[c_233381,c_232948,c_232949]) ).
tcf(c_233740,plain,
antidomain(zero) = one,
inference(demodulation,[status(thm)],[c_233049,c_233022]) ).
tcf(c_234331,plain,
! [X0: $i] : addition(antidomain(X0),antidomain(antidomain(X0))) = addition(antidomain(antidomain(X0)),one),
inference(superposition,[status(thm)],[c_52,c_232973]) ).
tcf(c_234376,plain,
! [X0: $i] : addition(antidomain(X0),antidomain(antidomain(X0))) = addition(one,antidomain(antidomain(X0))),
inference(theory_normalisation,[status(thm)],[c_234331,c_50,c_49]) ).
tcf(c_234377,plain,
! [X0: $i] : addition(one,antidomain(antidomain(X0))) = one,
inference(light_normalisation,[status(thm)],[c_234376,c_83]) ).
tcf(c_234513,plain,
addition(one,antidomain(iPr_def_19)) = one,
inference(superposition,[status(thm)],[c_140,c_234377]) ).
tcf(c_234514,plain,
addition(one,antidomain(iPr_def_20)) = one,
inference(superposition,[status(thm)],[c_141,c_234377]) ).
tcf(c_234516,plain,
addition(one,antidomain(iPr_def_22)) = one,
inference(superposition,[status(thm)],[c_143,c_234377]) ).
tcf(c_234521,plain,
addition(one,antidomain(iPr_def_28)) = one,
inference(superposition,[status(thm)],[c_149,c_234377]) ).
tcf(c_234527,plain,
! [X0: $i] : addition(antidomain(X0),one) = addition(one,one),
inference(superposition,[status(thm)],[c_234377,c_232973]) ).
tcf(c_234529,plain,
addition(one,iPr_def_29) = one,
inference(light_normalisation,[status(thm)],[c_234521,c_150]) ).
tcf(c_234530,plain,
addition(iPr_def_29,one) = one,
inference(theory_normalisation,[status(thm)],[c_234529,c_50,c_49]) ).
tcf(c_234537,plain,
addition(one,iPr_def_23) = one,
inference(light_normalisation,[status(thm)],[c_234516,c_144]) ).
tcf(c_234538,plain,
addition(iPr_def_23,one) = one,
inference(theory_normalisation,[status(thm)],[c_234537,c_50,c_49]) ).
tcf(c_234541,plain,
addition(one,iPr_def_21) = one,
inference(light_normalisation,[status(thm)],[c_234514,c_142]) ).
tcf(c_234542,plain,
addition(iPr_def_21,one) = one,
inference(theory_normalisation,[status(thm)],[c_234541,c_50,c_49]) ).
tcf(c_234543,plain,
addition(one,iPr_def_20) = one,
inference(light_normalisation,[status(thm)],[c_234513,c_141]) ).
tcf(c_234544,plain,
addition(iPr_def_20,one) = one,
inference(theory_normalisation,[status(thm)],[c_234543,c_50,c_49]) ).
tcf(c_234557,plain,
! [X0: $i] : addition(one,antidomain(X0)) = addition(one,one),
inference(theory_normalisation,[status(thm)],[c_234527,c_50,c_49]) ).
tcf(c_235358,plain,
! [X0: $i] : addition(one,antidomain(X0)) = one,
inference(demodulation,[status(thm)],[c_234557,c_52]) ).
tcf(c_235367,plain,
addition(one,iPr_def_19) = one,
inference(superposition,[status(thm)],[c_140,c_235358]) ).
tcf(c_235384,plain,
addition(iPr_def_19,one) = one,
inference(theory_normalisation,[status(thm)],[c_235367,c_50,c_49]) ).
tcf(c_236314,plain,
addition(iPr_def_23,iPr_def_30) = iPr_def_30,
inference(superposition,[status(thm)],[c_151,c_233027]) ).
tcf(c_236487,plain,
addition(iPr_def_23,one) = addition(iPr_def_30,one),
inference(superposition,[status(thm)],[c_234530,c_233030]) ).
tcf(c_236499,plain,
addition(iPr_def_30,one) = one,
inference(light_normalisation,[status(thm)],[c_236487,c_234538]) ).
tcf(c_237067,plain,
addition(one,iPr_def_30) = addition(iPr_def_22,iPr_def_30),
inference(superposition,[status(thm)],[c_236314,c_233039]) ).
tcf(c_237081,plain,
addition(iPr_def_22,iPr_def_30) = addition(iPr_def_30,one),
inference(theory_normalisation,[status(thm)],[c_237067,c_50,c_49]) ).
tcf(c_237082,plain,
addition(iPr_def_22,iPr_def_30) = one,
inference(light_normalisation,[status(thm)],[c_237081,c_236499]) ).
tcf(c_250775,plain,
! [X0: $i,X1: $i] : multiplication(antidomain(X0),multiplication(X0,X1)) = zero,
inference(demodulation,[status(thm)],[c_233177,c_59]) ).
tcf(c_255536,plain,
! [X0: $i,X1: $i] : multiplication(antidomain(X0),addition(X0,X1)) = multiplication(antidomain(X0),X1),
inference(demodulation,[status(thm)],[c_233192,c_51,c_233215]) ).
tcf(c_255547,plain,
! [X0: $i] : multiplication(iPr_def_21,addition(iPr_def_20,X0)) = multiplication(iPr_def_21,X0),
inference(superposition,[status(thm)],[c_142,c_255536]) ).
tcf(c_255548,plain,
! [X0: $i] : multiplication(iPr_def_22,addition(iPr_def_21,X0)) = multiplication(iPr_def_22,X0),
inference(superposition,[status(thm)],[c_143,c_255536]) ).
tcf(c_255549,plain,
! [X0: $i] : multiplication(iPr_def_23,addition(iPr_def_22,X0)) = multiplication(iPr_def_23,X0),
inference(superposition,[status(thm)],[c_144,c_255536]) ).
tcf(c_255550,plain,
! [X0: $i] : multiplication(iPr_def_25,addition(iPr_def_24,X0)) = multiplication(iPr_def_25,X0),
inference(superposition,[status(thm)],[c_146,c_255536]) ).
tcf(c_255552,plain,
! [X0: $i] : multiplication(iPr_def_27,addition(iPr_def_26,X0)) = multiplication(iPr_def_27,X0),
inference(superposition,[status(thm)],[c_148,c_255536]) ).
tcf(c_255606,plain,
multiplication(antidomain(iPr_def_22),one) = multiplication(antidomain(iPr_def_22),iPr_def_23),
inference(superposition,[status(thm)],[c_232935,c_255536]) ).
tcf(c_255607,plain,
multiplication(antidomain(iPr_def_21),one) = multiplication(antidomain(iPr_def_21),iPr_def_22),
inference(superposition,[status(thm)],[c_232933,c_255536]) ).
tcf(c_255608,plain,
multiplication(antidomain(iPr_def_20),one) = multiplication(antidomain(iPr_def_20),iPr_def_21),
inference(superposition,[status(thm)],[c_232931,c_255536]) ).
tcf(c_255609,plain,
multiplication(antidomain(iPr_def_19),one) = multiplication(antidomain(iPr_def_19),iPr_def_20),
inference(superposition,[status(thm)],[c_232929,c_255536]) ).
tcf(c_255739,plain,
multiplication(antidomain(iPr_def_22),one) = multiplication(antidomain(iPr_def_22),iPr_def_30),
inference(superposition,[status(thm)],[c_237082,c_255536]) ).
tcf(c_255839,plain,
multiplication(iPr_def_23,one) = multiplication(iPr_def_23,iPr_def_30),
inference(light_normalisation,[status(thm)],[c_255739,c_144]) ).
tcf(c_255842,plain,
multiplication(iPr_def_20,one) = multiplication(iPr_def_20,iPr_def_20),
inference(light_normalisation,[status(thm)],[c_255609,c_141]) ).
tcf(c_255843,plain,
multiplication(iPr_def_21,one) = multiplication(iPr_def_21,iPr_def_21),
inference(light_normalisation,[status(thm)],[c_255608,c_142]) ).
tcf(c_255844,plain,
multiplication(iPr_def_22,one) = multiplication(iPr_def_22,iPr_def_22),
inference(light_normalisation,[status(thm)],[c_255607,c_143]) ).
tcf(c_255845,plain,
multiplication(iPr_def_23,one) = multiplication(iPr_def_23,iPr_def_23),
inference(light_normalisation,[status(thm)],[c_255606,c_144]) ).
tcf(c_256515,plain,
multiplication(iPr_def_23,iPr_def_23) = multiplication(iPr_def_23,iPr_def_30),
inference(demodulation,[status(thm)],[c_255839,c_255845]) ).
tcf(c_256541,plain,
multiplication(iPr_def_20,iPr_def_20) = iPr_def_20,
inference(demodulation,[status(thm)],[c_255842,c_54]) ).
tcf(c_256559,plain,
multiplication(iPr_def_21,iPr_def_21) = iPr_def_21,
inference(demodulation,[status(thm)],[c_255843,c_54]) ).
tcf(c_256930,plain,
! [X0: $i,X1: $i] : multiplication(X0,addition(coantidomain(X0),X1)) = multiplication(X0,X1),
inference(demodulation,[status(thm)],[c_233193,c_51,c_233215]) ).
tcf(c_256934,plain,
! [X0: $i,X1: $i] : multiplication(X0,addition(X1,coantidomain(X0))) = multiplication(X0,X1),
inference(superposition,[status(thm)],[c_49,c_256930]) ).
tcf(c_257318,plain,
multiplication(iPr_def_22,iPr_def_22) = iPr_def_22,
inference(demodulation,[status(thm)],[c_255844,c_54]) ).
tcf(c_257336,plain,
multiplication(iPr_def_23,iPr_def_23) = iPr_def_23,
inference(demodulation,[status(thm)],[c_255845,c_54]) ).
tcf(c_257337,plain,
multiplication(iPr_def_23,iPr_def_30) = iPr_def_23,
inference(demodulation,[status(thm)],[c_256515,c_257336]) ).
tcf(c_259339,plain,
! [X0: $i] : multiplication(iPr_def_21,addition(X0,iPr_def_20)) = multiplication(iPr_def_21,X0),
inference(superposition,[status(thm)],[c_49,c_255547]) ).
tcf(c_259373,plain,
! [X0: $i] : multiplication(iPr_def_22,addition(X0,iPr_def_21)) = multiplication(iPr_def_22,X0),
inference(superposition,[status(thm)],[c_49,c_255548]) ).
tcf(c_259407,plain,
! [X0: $i] : multiplication(iPr_def_23,addition(X0,iPr_def_22)) = multiplication(iPr_def_23,X0),
inference(superposition,[status(thm)],[c_49,c_255549]) ).
tcf(c_259711,plain,
! [X0: $i] : multiplication(iPr_def_25,addition(X0,iPr_def_24)) = multiplication(iPr_def_25,X0),
inference(superposition,[status(thm)],[c_49,c_255550]) ).
tcf(c_259790,plain,
! [X0: $i] : multiplication(iPr_def_27,addition(X0,iPr_def_26)) = multiplication(iPr_def_27,X0),
inference(superposition,[status(thm)],[c_49,c_255552]) ).
tcf(c_264918,plain,
! [X0: $i,X1: $i] : multiplication(addition(one,antidomain(X0)),multiplication(X0,X1)) = addition(multiplication(X0,X1),zero),
inference(superposition,[status(thm)],[c_250775,c_233226]) ).
tcf(c_265345,plain,
! [X0: $i,X1: $i] : multiplication(addition(one,antidomain(X0)),multiplication(X0,X1)) = addition(zero,multiplication(X0,X1)),
inference(theory_normalisation,[status(thm)],[c_264918,c_50,c_49]) ).
tcf(c_265346,plain,
! [X0: $i,X1: $i] : addition(zero,multiplication(X0,X1)) = multiplication(one,multiplication(X0,X1)),
inference(light_normalisation,[status(thm)],[c_265345,c_235358]) ).
tcf(c_266252,plain,
multiplication(iPr_def_21,one) = multiplication(iPr_def_21,iPr_def_19),
inference(superposition,[status(thm)],[c_232929,c_259339]) ).
tcf(c_266304,plain,
multiplication(iPr_def_22,one) = multiplication(iPr_def_22,iPr_def_20),
inference(superposition,[status(thm)],[c_232931,c_259373]) ).
tcf(c_266356,plain,
multiplication(iPr_def_23,one) = multiplication(iPr_def_23,iPr_def_21),
inference(superposition,[status(thm)],[c_232933,c_259407]) ).
tcf(c_266656,plain,
! [X0: $i,X1: $i] : multiplication(addition(antidomain(X0),X1),X0) = multiplication(X1,X0),
inference(demodulation,[status(thm)],[c_233229,c_55,c_265346]) ).
tcf(c_266663,plain,
! [X0: $i] : multiplication(antidomain(antidomain(X0)),X0) = multiplication(one,X0),
inference(superposition,[status(thm)],[c_83,c_266656]) ).
tcf(c_266681,plain,
! [X0: $i] : multiplication(addition(iPr_def_20,X0),iPr_def_19) = multiplication(X0,iPr_def_19),
inference(superposition,[status(thm)],[c_141,c_266656]) ).
tcf(c_266733,plain,
! [X0: $i] : multiplication(antidomain(antidomain(X0)),X0) = X0,
inference(light_normalisation,[status(thm)],[c_266663,c_55]) ).
tcf(c_266774,plain,
multiplication(antidomain(iPr_def_19),iPr_def_18) = iPr_def_18,
inference(superposition,[status(thm)],[c_140,c_266733]) ).
tcf(c_266775,plain,
multiplication(antidomain(iPr_def_20),iPr_def_19) = iPr_def_19,
inference(superposition,[status(thm)],[c_141,c_266733]) ).
tcf(c_266776,plain,
multiplication(antidomain(iPr_def_21),iPr_def_20) = iPr_def_20,
inference(superposition,[status(thm)],[c_142,c_266733]) ).
tcf(c_266777,plain,
multiplication(antidomain(iPr_def_22),iPr_def_21) = iPr_def_21,
inference(superposition,[status(thm)],[c_143,c_266733]) ).
tcf(c_266780,plain,
multiplication(antidomain(iPr_def_26),iPr_def_25) = iPr_def_25,
inference(superposition,[status(thm)],[c_147,c_266733]) ).
tcf(c_266827,plain,
multiplication(iPr_def_27,iPr_def_25) = iPr_def_25,
inference(light_normalisation,[status(thm)],[c_266780,c_148]) ).
tcf(c_266829,plain,
multiplication(iPr_def_23,iPr_def_21) = iPr_def_21,
inference(light_normalisation,[status(thm)],[c_266777,c_144]) ).
tcf(c_266830,plain,
multiplication(iPr_def_22,iPr_def_20) = iPr_def_20,
inference(light_normalisation,[status(thm)],[c_266776,c_143]) ).
tcf(c_266831,plain,
multiplication(iPr_def_21,iPr_def_19) = iPr_def_19,
inference(light_normalisation,[status(thm)],[c_266775,c_142]) ).
tcf(c_266832,plain,
multiplication(iPr_def_20,iPr_def_18) = iPr_def_18,
inference(light_normalisation,[status(thm)],[c_266774,c_141]) ).
tcf(c_267614,plain,
multiplication(iPr_def_23,addition(one,iPr_def_21)) = addition(iPr_def_23,iPr_def_21),
inference(superposition,[status(thm)],[c_266829,c_233188]) ).
tcf(c_267630,plain,
multiplication(iPr_def_23,addition(iPr_def_21,one)) = addition(iPr_def_21,iPr_def_23),
inference(theory_normalisation,[status(thm)],[c_267614,c_50,c_49]) ).
tcf(c_267631,plain,
addition(iPr_def_21,iPr_def_23) = iPr_def_21,
inference(light_normalisation,[status(thm)],[c_267630,c_234542,c_266356,c_266829]) ).
tcf(c_267663,plain,
multiplication(iPr_def_22,addition(one,iPr_def_20)) = addition(iPr_def_22,iPr_def_20),
inference(superposition,[status(thm)],[c_266830,c_233188]) ).
tcf(c_267667,plain,
addition(antidomain(iPr_def_20),antidomain(multiplication(iPr_def_22,antidomain(antidomain(iPr_def_20))))) = antidomain(multiplication(iPr_def_22,antidomain(antidomain(iPr_def_20)))),
inference(superposition,[status(thm)],[c_266830,c_61]) ).
tcf(c_267681,plain,
multiplication(iPr_def_22,addition(iPr_def_20,one)) = addition(iPr_def_20,iPr_def_22),
inference(theory_normalisation,[status(thm)],[c_267663,c_50,c_49]) ).
tcf(c_267682,plain,
addition(iPr_def_20,iPr_def_22) = iPr_def_20,
inference(light_normalisation,[status(thm)],[c_267681,c_234544,c_266304,c_266830]) ).
tcf(c_267693,plain,
iPr_def_21 = iPr_def_23,
inference(light_normalisation,[status(thm)],[c_267667,c_142,c_143,c_144,c_257318,c_267631]) ).
tcf(c_267702,plain,
multiplication(iPr_def_21,iPr_def_30) = iPr_def_21,
inference(demodulation,[status(thm)],[c_257337,c_267693]) ).
tcf(c_267725,plain,
addition(iPr_def_21,iPr_def_29) = iPr_def_30,
inference(demodulation,[status(thm)],[c_151,c_267693]) ).
tcf(c_267727,plain,
iPr_def_21 != iPr_def_30,
inference(demodulation,[status(thm)],[c_153,c_267693]) ).
tcf(c_267740,plain,
multiplication(iPr_def_21,addition(one,iPr_def_19)) = addition(iPr_def_21,iPr_def_19),
inference(superposition,[status(thm)],[c_266831,c_233188]) ).
tcf(c_267744,plain,
addition(antidomain(iPr_def_19),antidomain(multiplication(iPr_def_21,antidomain(antidomain(iPr_def_19))))) = antidomain(multiplication(iPr_def_21,antidomain(antidomain(iPr_def_19)))),
inference(superposition,[status(thm)],[c_266831,c_61]) ).
tcf(c_267753,plain,
multiplication(addition(one,iPr_def_21),iPr_def_19) = addition(iPr_def_19,iPr_def_19),
inference(superposition,[status(thm)],[c_266831,c_233226]) ).
tcf(c_267756,plain,
multiplication(addition(iPr_def_21,one),iPr_def_19) = addition(iPr_def_19,iPr_def_19),
inference(theory_normalisation,[status(thm)],[c_267753,c_50,c_49]) ).
tcf(c_267757,plain,
addition(iPr_def_19,iPr_def_19) = multiplication(one,iPr_def_19),
inference(light_normalisation,[status(thm)],[c_267756,c_234542]) ).
tcf(c_267758,plain,
multiplication(iPr_def_21,addition(iPr_def_19,one)) = addition(iPr_def_19,iPr_def_21),
inference(theory_normalisation,[status(thm)],[c_267740,c_50,c_49]) ).
tcf(c_267759,plain,
addition(iPr_def_19,iPr_def_21) = iPr_def_19,
inference(light_normalisation,[status(thm)],[c_267758,c_235384,c_266252,c_266831]) ).
tcf(c_267767,plain,
iPr_def_20 = iPr_def_22,
inference(light_normalisation,[status(thm)],[c_267744,c_141,c_142,c_143,c_256559,c_267682]) ).
tcf(c_267782,plain,
addition(iPr_def_20,iPr_def_30) = one,
inference(demodulation,[status(thm)],[c_237082,c_267767]) ).
tcf(c_268252,plain,
addition(antidomain(iPr_def_18),antidomain(multiplication(iPr_def_20,antidomain(antidomain(iPr_def_18))))) = antidomain(multiplication(iPr_def_20,antidomain(antidomain(iPr_def_18)))),
inference(superposition,[status(thm)],[c_266832,c_61]) ).
tcf(c_268273,plain,
iPr_def_19 = iPr_def_21,
inference(light_normalisation,[status(thm)],[c_268252,c_140,c_141,c_142,c_256541,c_267759]) ).
tcf(c_268274,plain,
iPr_def_19 != iPr_def_30,
inference(demodulation,[status(thm)],[c_267727,c_268273]) ).
tcf(c_268292,plain,
antidomain(iPr_def_20) = iPr_def_19,
inference(demodulation,[status(thm)],[c_142,c_268273]) ).
tcf(c_269283,plain,
! [X0: $i] : multiplication(addition(iPr_def_19,X0),iPr_def_20) = multiplication(X0,iPr_def_20),
inference(superposition,[status(thm)],[c_268292,c_266656]) ).
tcf(c_270226,plain,
multiplication(iPr_def_25,iPr_def_18) = multiplication(iPr_def_25,iPr_def_24),
inference(superposition,[status(thm)],[c_233382,c_259711]) ).
tcf(c_270253,plain,
multiplication(iPr_def_25,iPr_def_18) = zero,
inference(light_normalisation,[status(thm)],[c_270226,c_233010]) ).
tcf(c_270327,plain,
multiplication(iPr_def_27,one) = multiplication(iPr_def_27,iPr_def_25),
inference(superposition,[status(thm)],[c_232938,c_259790]) ).
tcf(c_270355,plain,
multiplication(iPr_def_27,one) = iPr_def_25,
inference(light_normalisation,[status(thm)],[c_270327,c_266827]) ).
tcf(c_272974,plain,
multiplication(iPr_def_19,iPr_def_30) = iPr_def_19,
inference(light_normalisation,[status(thm)],[c_267702,c_268273]) ).
tcf(c_272982,plain,
multiplication(iPr_def_19,addition(one,iPr_def_30)) = addition(iPr_def_19,iPr_def_19),
inference(superposition,[status(thm)],[c_272974,c_233188]) ).
tcf(c_273006,plain,
multiplication(iPr_def_19,addition(iPr_def_30,one)) = addition(iPr_def_19,iPr_def_19),
inference(theory_normalisation,[status(thm)],[c_272982,c_50,c_49]) ).
tcf(c_273007,plain,
multiplication(one,iPr_def_19) = multiplication(iPr_def_19,one),
inference(light_normalisation,[status(thm)],[c_273006,c_236499,c_267757]) ).
tcf(c_273281,plain,
addition(iPr_def_19,iPr_def_29) = iPr_def_30,
inference(light_normalisation,[status(thm)],[c_267725,c_268273]) ).
tcf(c_274362,plain,
addition(antidomain(zero),antidomain(multiplication(iPr_def_25,antidomain(antidomain(iPr_def_18))))) = antidomain(multiplication(iPr_def_25,antidomain(antidomain(iPr_def_18)))),
inference(superposition,[status(thm)],[c_270253,c_61]) ).
tcf(c_274399,plain,
addition(one,antidomain(multiplication(iPr_def_25,iPr_def_20))) = antidomain(multiplication(iPr_def_25,iPr_def_20)),
inference(light_normalisation,[status(thm)],[c_274362,c_140,c_141,c_233740]) ).
tcf(c_274402,plain,
iPr_def_25 = iPr_def_27,
inference(demodulation,[status(thm)],[c_270355,c_54]) ).
tcf(c_274431,plain,
antidomain(iPr_def_25) = iPr_def_28,
inference(demodulation,[status(thm)],[c_149,c_274402]) ).
tcf(c_274432,plain,
antidomain(iPr_def_26) = iPr_def_25,
inference(demodulation,[status(thm)],[c_148,c_274402]) ).
tcf(c_274433,plain,
iPr_def_26 = iPr_def_28,
inference(light_normalisation,[status(thm)],[c_274431,c_147]) ).
tcf(c_274463,plain,
antidomain(iPr_def_26) = iPr_def_29,
inference(demodulation,[status(thm)],[c_150,c_274433]) ).
tcf(c_274580,plain,
iPr_def_25 = iPr_def_29,
inference(light_normalisation,[status(thm)],[c_274463,c_274432]) ).
tcf(c_274581,plain,
addition(iPr_def_19,iPr_def_25) = iPr_def_30,
inference(demodulation,[status(thm)],[c_273281,c_274580]) ).
tcf(c_274686,plain,
multiplication(one,iPr_def_19) = multiplication(iPr_def_30,iPr_def_19),
inference(superposition,[status(thm)],[c_267782,c_266681]) ).
tcf(c_274716,plain,
multiplication(iPr_def_19,one) = multiplication(iPr_def_30,iPr_def_19),
inference(light_normalisation,[status(thm)],[c_274686,c_273007]) ).
tcf(c_283800,plain,
multiplication(iPr_def_30,iPr_def_19) = iPr_def_19,
inference(demodulation,[status(thm)],[c_274716,c_54]) ).
tcf(c_283817,plain,
! [X0: $i] : addition(iPr_def_19,multiplication(iPr_def_30,X0)) = multiplication(iPr_def_30,addition(iPr_def_19,X0)),
inference(superposition,[status(thm)],[c_283800,c_56]) ).
tcf(c_324931,plain,
multiplication(iPr_def_25,iPr_def_20) = multiplication(iPr_def_30,iPr_def_20),
inference(superposition,[status(thm)],[c_274581,c_269283]) ).
tcf(c_332012,plain,
antidomain(multiplication(iPr_def_25,iPr_def_20)) = one,
inference(demodulation,[status(thm)],[c_274399,c_235358]) ).
tcf(c_332028,plain,
multiplication(one,multiplication(iPr_def_25,iPr_def_20)) = zero,
inference(superposition,[status(thm)],[c_332012,c_60]) ).
tcf(c_332060,plain,
multiplication(iPr_def_25,iPr_def_20) = zero,
inference(demodulation,[status(thm)],[c_332028,c_55]) ).
tcf(c_332063,plain,
multiplication(iPr_def_30,iPr_def_20) = zero,
inference(demodulation,[status(thm)],[c_324931,c_332060]) ).
tcf(c_343201,plain,
multiplication(iPr_def_30,addition(iPr_def_19,coantidomain(iPr_def_30))) = addition(iPr_def_19,zero),
inference(superposition,[status(thm)],[c_63,c_283817]) ).
tcf(c_343207,plain,
multiplication(iPr_def_30,addition(iPr_def_19,iPr_def_20)) = addition(iPr_def_19,zero),
inference(superposition,[status(thm)],[c_332063,c_283817]) ).
tcf(c_343255,plain,
addition(iPr_def_19,zero) = multiplication(iPr_def_30,one),
inference(light_normalisation,[status(thm)],[c_343207,c_232929]) ).
tcf(c_343301,plain,
multiplication(iPr_def_30,addition(iPr_def_19,coantidomain(iPr_def_30))) = multiplication(iPr_def_30,one),
inference(light_normalisation,[status(thm)],[c_343201,c_343255]) ).
tcf(c_343302,plain,
iPr_def_19 = iPr_def_30,
inference(demodulation,[status(thm)],[c_343301,c_54,c_256934,c_283800]) ).
tcf(c_343303,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[c_343302,c_268274]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : KLE118+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.02 % Command : run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.03/0.30 % Computer : n012.cluster.edu
% 0.03/0.30 % Model : x86_64 x86_64
% 0.03/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.03/0.30 % Memory : 8046.5625MB
% 0.03/0.30 % OS : Linux 6.8.0-71-generic
% 0.03/0.30 % CPULimit : 300
% 0.03/0.30 % WCLimit : 300
% 0.03/0.30 % DateTime : Wed Sep 23 18:59:06 UTC 2026
% 0.03/0.30 % CPUTime :
% 0.03/0.30 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.03/0.32 Running first-order theorem proving
% 0.03/0.32 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.03/0.33
% 0.03/0.33 % ======== iProver multi-core TPTP/SMT =========
% 0.03/0.33
% 0.03/0.33 % Detected problem language: tptp
% 0.07/0.33 % Proving...
% 69.02/16.63 % SZS status Started for theBenchmark.p
% 69.02/16.63 % SZS status Theorem for theBenchmark.p
% 69.02/16.63
% 69.02/16.63 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 69.02/16.63
% 69.02/16.63 % ------ iProver source info
% 69.02/16.63
% 69.02/16.63 % git: date: 2026-07-19 20:42:38 +0200
% 69.02/16.63 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 69.02/16.63 % git: non_committed_changes: false
% 69.02/16.63
% 69.02/16.63 % ------ Parsing...
% 69.02/16.63 % ------ Clausification by vclausify_rel & Parsing by iProver...% ------ preprocesses with Option_UEQ
% 69.02/16.63 %
% 69.02/16.63
% 69.02/16.63 % ------ Preprocessing... sup_sim: 0 sf_s rm: 0 0s sf_e pe_s pe_e %
% 69.02/16.63
% 69.02/16.63 % ------ Preprocessing...% ------ preprocesses with Option_UEQ
% 69.02/16.63 gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 69.02/16.63
% 69.02/16.63 % ------ Preprocessing... sf_s rm: 0 0s sf_e
% 69.02/16.63 % ------ Proving...
% 69.02/16.63 % ------ Problem Properties
% 69.02/16.63
% 69.02/16.63 %
% 69.02/16.63 % clauses 40
% 69.02/16.63 % conjectures 2
% 69.02/16.63 % EPR 2
% 69.02/16.63 % Horn 40
% 69.02/16.63 % unary 40
% 69.02/16.63 % binary 0
% 69.02/16.63 % lits 40
% 69.02/16.63 % lits eq 40
% 69.02/16.63 % fd_pure 0
% 69.02/16.63 % fd_pseudo 0
% 69.02/16.63 % fd_cond 0
% 69.02/16.63 % fd_pseudo_cond 0
% 69.02/16.63 % AC symbols 1
% 69.02/16.63
% 69.02/16.63 % ------ Schedule UEQ
% 69.02/16.63
% 69.02/16.63 % ------ Option_UEQ Time Limit: 10.
% 69.02/16.63
% 69.02/16.63
% 69.02/16.63 % ------
% 69.02/16.63 % Current options:
% 69.02/16.63 % ------
% 69.02/16.63
% 69.02/16.63
% 69.02/16.63 %
% 69.02/16.63
% 69.02/16.63 % ------ Proving...
% 69.02/16.63 % Proof_search_loop: time out after: 4000 full_loop iterations
% 69.02/16.63
% 69.02/16.63 % ------ Option_UEQ Time Limit: 15.
% 69.02/16.63
% 69.02/16.63
% 69.02/16.63 % ------
% 69.02/16.63 % Current options:
% 69.02/16.63 % ------
% 69.02/16.63
% 69.02/16.63
% 69.02/16.63 %
% 69.02/16.63
% 69.02/16.63 % ------ Proving...
% 69.02/16.63 %
% 69.02/16.63
% 69.02/16.63 % SZS status Theorem for theBenchmark.p
% 69.02/16.63
% 69.02/16.63 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 69.02/16.64
% 69.02/16.64
%------------------------------------------------------------------------------