%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : KLE080+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 : n026.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:21 PM UTC 2026
% Result : Theorem 94.35s 23.22s
% Output : CNFRefutation 94.35s
% Verified :
% SZS Type : Refutation
% Derivation depth : 39
% Number of leaves : 22
% Syntax : Number of formulae : 289 ( 273 unt; 3 def)
% Number of atoms : 814 ( 320 equ)
% Maximal formula atoms : 3 ( 2 avg)
% Number of connectives : 62 ( 30 ~; 24 |; 6 &)
% ( 0 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 2 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 5 ( 3 usr; 4 prp; 0-2 aty)
% Number of functors : 7 ( 7 usr; 3 con; 0-2 aty)
% Number of variables : 275 ( 0 sgn 274 !; 1 ?; 214 :)
% 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] : addition(X0,multiplication(domain(X0),X0)) = multiplication(domain(X0),X0),
file('/export/starexec/sandbox2/benchmark/Axioms/KLE001+5.ax',domain1) ).
fof(f14,axiom,
! [X0,X1] : domain(multiplication(X0,X1)) = domain(multiplication(X0,domain(X1))),
file('/export/starexec/sandbox2/benchmark/Axioms/KLE001+5.ax',domain2) ).
fof(f15,axiom,
! [X0] : addition(domain(X0),one) = one,
file('/export/starexec/sandbox2/benchmark/Axioms/KLE001+5.ax',domain3) ).
fof(f16,axiom,
domain(zero) = zero,
file('/export/starexec/sandbox2/benchmark/Axioms/KLE001+5.ax',domain4) ).
fof(f17,axiom,
! [X0,X1] : domain(addition(X0,X1)) = addition(domain(X0),domain(X1)),
file('/export/starexec/sandbox2/benchmark/Axioms/KLE001+5.ax',domain5) ).
fof(f18,conjecture,
! [X0] :
( ! [X1] :
( multiplication(domain(X1),antidomain(X1)) = zero
& addition(domain(X1),antidomain(X1)) = one )
=> antidomain(antidomain(X0)) = domain(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goals) ).
fof(f19,negated_conjecture,
~ ! [X0] :
( ! [X1] :
( multiplication(domain(X1),antidomain(X1)) = zero
& addition(domain(X1),antidomain(X1)) = one )
=> antidomain(antidomain(X0)) = domain(X0) ),
inference(negated_conjecture,[status(cth)],[f18]) ).
fof(f20,plain,
? [X0] :
( ! [X1] :
( multiplication(domain(X1),antidomain(X1)) = zero
& addition(domain(X1),antidomain(X1)) = one )
& domain(X0) != antidomain(antidomain(X0)) ),
inference(ennf_transformation,[],[f19]) ).
fof(f21,plain,
( ! [X1] :
( multiplication(domain(X1),antidomain(X1)) = zero
& addition(domain(X1),antidomain(X1)) = one )
& domain(sK0) != antidomain(antidomain(sK0)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(X0,sK0)],[f20]) ).
fof(f22,plain,
! [X0,X1] : addition(X0,X1) = addition(X1,X0),
inference(cnf_transformation,[],[f1]) ).
fof(f23,plain,
! [X2,X0,X1] : addition(X2,addition(X1,X0)) = addition(addition(X2,X1),X0),
inference(cnf_transformation,[],[f2]) ).
fof(f24,plain,
! [X0] : addition(X0,zero) = X0,
inference(cnf_transformation,[],[f3]) ).
fof(f25,plain,
! [X0] : addition(X0,X0) = X0,
inference(cnf_transformation,[],[f4]) ).
fof(f26,plain,
! [X2,X0,X1] : multiplication(X0,multiplication(X1,X2)) = multiplication(multiplication(X0,X1),X2),
inference(cnf_transformation,[],[f5]) ).
fof(f27,plain,
! [X0] : multiplication(X0,one) = X0,
inference(cnf_transformation,[],[f6]) ).
fof(f28,plain,
! [X0] : multiplication(one,X0) = X0,
inference(cnf_transformation,[],[f7]) ).
fof(f29,plain,
! [X2,X0,X1] : multiplication(X0,addition(X1,X2)) = addition(multiplication(X0,X1),multiplication(X0,X2)),
inference(cnf_transformation,[],[f8]) ).
fof(f30,plain,
! [X2,X0,X1] : multiplication(addition(X0,X1),X2) = addition(multiplication(X0,X2),multiplication(X1,X2)),
inference(cnf_transformation,[],[f9]) ).
fof(f31,plain,
! [X0] : zero = multiplication(X0,zero),
inference(cnf_transformation,[],[f10]) ).
fof(f32,plain,
! [X0] : zero = multiplication(zero,X0),
inference(cnf_transformation,[],[f11]) ).
fof(f33,plain,
! [X0] : multiplication(domain(X0),X0) = addition(X0,multiplication(domain(X0),X0)),
inference(cnf_transformation,[],[f13]) ).
fof(f34,plain,
! [X0,X1] : domain(multiplication(X0,X1)) = domain(multiplication(X0,domain(X1))),
inference(cnf_transformation,[],[f14]) ).
fof(f35,plain,
! [X0] : one = addition(domain(X0),one),
inference(cnf_transformation,[],[f15]) ).
fof(f36,plain,
zero = domain(zero),
inference(cnf_transformation,[],[f16]) ).
fof(f37,plain,
! [X0,X1] : domain(addition(X0,X1)) = addition(domain(X0),domain(X1)),
inference(cnf_transformation,[],[f17]) ).
fof(f38,plain,
! [X1] : zero = multiplication(domain(X1),antidomain(X1)),
inference(cnf_transformation,[],[f21]) ).
fof(f39,plain,
! [X1] : one = addition(domain(X1),antidomain(X1)),
inference(cnf_transformation,[],[f21]) ).
fof(f40,plain,
domain(sK0) != antidomain(antidomain(sK0)),
inference(cnf_transformation,[],[f21]) ).
tcf(c_49,plain,
! [X0: $i,X1: $i] : addition(X0,X1) = addition(X1,X0),
inference(cnf_transformation,[],[f22]) ).
tcf(c_50,plain,
! [X0: $i,X1: $i,X2: $i] : addition(addition(X0,X1),X2) = addition(X0,addition(X1,X2)),
inference(cnf_transformation,[],[f23]) ).
tcf(c_51,plain,
! [X0: $i] : addition(X0,zero) = X0,
inference(cnf_transformation,[],[f24]) ).
tcf(c_52,plain,
! [X0: $i] : addition(X0,X0) = X0,
inference(cnf_transformation,[],[f25]) ).
tcf(c_53,plain,
! [X0: $i,X1: $i,X2: $i] : multiplication(multiplication(X0,X1),X2) = multiplication(X0,multiplication(X1,X2)),
inference(cnf_transformation,[],[f26]) ).
tcf(c_54,plain,
! [X0: $i] : multiplication(X0,one) = X0,
inference(cnf_transformation,[],[f27]) ).
tcf(c_55,plain,
! [X0: $i] : multiplication(one,X0) = X0,
inference(cnf_transformation,[],[f28]) ).
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,[],[f29]) ).
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,[],[f30]) ).
tcf(c_58,plain,
! [X0: $i] : multiplication(X0,zero) = zero,
inference(cnf_transformation,[],[f31]) ).
tcf(c_59,plain,
! [X0: $i] : multiplication(zero,X0) = zero,
inference(cnf_transformation,[],[f32]) ).
tcf(c_60,plain,
! [X0: $i] : addition(X0,multiplication(domain(X0),X0)) = multiplication(domain(X0),X0),
inference(cnf_transformation,[],[f33]) ).
tcf(c_61,plain,
! [X0: $i,X1: $i] : domain(multiplication(X0,domain(X1))) = domain(multiplication(X0,X1)),
inference(cnf_transformation,[],[f34]) ).
tcf(c_62,plain,
! [X0: $i] : addition(domain(X0),one) = one,
inference(cnf_transformation,[],[f35]) ).
tcf(c_63,plain,
domain(zero) = zero,
inference(cnf_transformation,[],[f36]) ).
tcf(c_64,plain,
! [X0: $i,X1: $i] : addition(domain(X0),domain(X1)) = domain(addition(X0,X1)),
inference(cnf_transformation,[],[f37]) ).
tcf(c_65,negated_conjecture,
antidomain(antidomain(sK0)) != domain(sK0),
inference(cnf_transformation,[],[f40]) ).
tcf(c_66,negated_conjecture,
! [X0: $i] : addition(domain(X0),antidomain(X0)) = one,
inference(cnf_transformation,[],[f39]) ).
tcf(c_67,negated_conjecture,
! [X0: $i] : multiplication(domain(X0),antidomain(X0)) = zero,
inference(cnf_transformation,[],[f38]) ).
tcf(c_83,plain,
! [X0: $i] : addition(one,domain(X0)) = one,
inference(theory_normalisation,[status(thm)],[c_62,c_50,c_49]) ).
tcf(c_129,definition,
iPr_def_10 = antidomain(sK0),
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 = domain(sK0),
introduced(definition,[new_symbols(definition,[iPr_def_12])],[]) ).
tcf(c_132,negated_conjecture,
! [X0: $i] : multiplication(domain(X0),antidomain(X0)) = zero,
inference(demodulation,[status(thm)],[c_67]) ).
tcf(c_133,negated_conjecture,
! [X0: $i] : addition(domain(X0),antidomain(X0)) = one,
inference(demodulation,[status(thm)],[c_66]) ).
tcf(c_134,negated_conjecture,
iPr_def_11 != iPr_def_12,
inference(demodulation,[status(thm)],[c_65,c_131,c_129,c_130]) ).
tcf(c_135,plain,
! [X0: $i] : X0 = X0,
theory(equality) ).
tcf(c_136,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X2 = X0 )
| ( X2 != X1 )
| ( X0 != X1 ) ),
theory(equality) ).
tcf(c_217,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_220,plain,
addition(domain(sK0),iPr_def_10) = one,
inference(superposition,[status(thm)],[c_129,c_133]) ).
tcf(c_221,plain,
multiplication(domain(sK0),iPr_def_10) = zero,
inference(superposition,[status(thm)],[c_129,c_132]) ).
tcf(c_222,plain,
multiplication(iPr_def_12,iPr_def_10) = zero,
inference(light_normalisation,[status(thm)],[c_221,c_131]) ).
tcf(c_223,plain,
addition(iPr_def_10,domain(sK0)) = one,
inference(theory_normalisation,[status(thm)],[c_220,c_50,c_49]) ).
tcf(c_224,plain,
addition(iPr_def_10,iPr_def_12) = one,
inference(light_normalisation,[status(thm)],[c_223,c_131]) ).
tcf(c_227,plain,
! [X0: $i] : multiplication(domain(X0),antidomain(X0)) = multiplication(iPr_def_12,iPr_def_10),
inference(demodulation,[status(thm)],[c_132,c_222]) ).
tcf(c_228,plain,
! [X0: $i] : addition(domain(X0),antidomain(X0)) = addition(iPr_def_10,iPr_def_12),
inference(demodulation,[status(thm)],[c_133,c_224]) ).
tcf(c_232,plain,
! [X0: $i] : addition(addition(iPr_def_10,iPr_def_12),domain(X0)) = addition(iPr_def_10,iPr_def_12),
inference(light_normalisation,[status(thm)],[c_83,c_224]) ).
tcf(c_233,plain,
! [X0: $i] : addition(iPr_def_10,addition(iPr_def_12,domain(X0))) = addition(iPr_def_10,iPr_def_12),
inference(demodulation,[status(thm)],[c_232,c_50]) ).
tcf(c_234,plain,
multiplication(domain(iPr_def_10),iPr_def_11) = multiplication(iPr_def_12,iPr_def_10),
inference(superposition,[status(thm)],[c_130,c_227]) ).
tcf(c_238,plain,
! [X0: $i] : addition(X0,multiplication(iPr_def_12,iPr_def_10)) = X0,
inference(light_normalisation,[status(thm)],[c_51,c_222]) ).
tcf(c_239,plain,
! [X0: $i] : multiplication(X0,addition(iPr_def_10,iPr_def_12)) = X0,
inference(light_normalisation,[status(thm)],[c_54,c_224]) ).
tcf(c_240,plain,
! [X0: $i] : addition(multiplication(X0,iPr_def_10),multiplication(X0,iPr_def_12)) = X0,
inference(demodulation,[status(thm)],[c_239,c_56]) ).
tcf(c_241,plain,
! [X0: $i] : multiplication(addition(iPr_def_10,iPr_def_12),X0) = X0,
inference(light_normalisation,[status(thm)],[c_55,c_224]) ).
tcf(c_242,plain,
! [X0: $i] : addition(multiplication(iPr_def_10,X0),multiplication(iPr_def_12,X0)) = X0,
inference(demodulation,[status(thm)],[c_241,c_57]) ).
tcf(c_277,plain,
! [X0: $i,X1: $i] : addition(domain(X0),addition(X1,antidomain(X0))) = addition(X1,addition(iPr_def_10,iPr_def_12)),
inference(superposition,[status(thm)],[c_228,c_217]) ).
tcf(c_289,plain,
! [X0: $i] : addition(multiplication(iPr_def_12,iPr_def_10),X0) = X0,
inference(superposition,[status(thm)],[c_238,c_49]) ).
tcf(c_295,plain,
! [X0: $i] : domain(multiplication(X0,sK0)) = domain(multiplication(X0,iPr_def_12)),
inference(superposition,[status(thm)],[c_131,c_61]) ).
tcf(c_304,plain,
! [X0: $i] : addition(domain(domain(X0)),domain(antidomain(X0))) = domain(addition(iPr_def_10,iPr_def_12)),
inference(superposition,[status(thm)],[c_228,c_64]) ).
tcf(c_320,plain,
! [X0: $i,X1: $i] : addition(X0,addition(X0,X1)) = addition(X0,X1),
inference(superposition,[status(thm)],[c_52,c_50]) ).
tcf(c_321,plain,
! [X0: $i,X1: $i] : addition(domain(X0),addition(antidomain(X0),X1)) = addition(addition(iPr_def_10,iPr_def_12),X1),
inference(superposition,[status(thm)],[c_228,c_50]) ).
tcf(c_331,plain,
! [X0: $i,X1: $i] : addition(domain(X0),addition(antidomain(X0),X1)) = addition(iPr_def_10,addition(iPr_def_12,X1)),
inference(theory_normalisation,[status(thm)],[c_321,c_50,c_49]) ).
tcf(c_351,plain,
multiplication(iPr_def_12,iPr_def_12) = iPr_def_12,
inference(superposition,[status(thm)],[c_289,c_240]) ).
tcf(c_354,plain,
addition(multiplication(iPr_def_10,iPr_def_12),iPr_def_12) = iPr_def_12,
inference(superposition,[status(thm)],[c_351,c_242]) ).
tcf(c_355,plain,
addition(iPr_def_12,multiplication(iPr_def_10,iPr_def_12)) = iPr_def_12,
inference(theory_normalisation,[status(thm)],[c_354,c_50,c_49]) ).
tcf(c_362,plain,
! [X0: $i] : addition(domain(domain(X0)),domain(antidomain(X0))) = addition(domain(iPr_def_10),domain(iPr_def_12)),
inference(demodulation,[status(thm)],[c_304,c_64]) ).
tcf(c_363,plain,
! [X0: $i,X1: $i] : addition(domain(domain(multiplication(X0,X1))),domain(antidomain(multiplication(X0,domain(X1))))) = addition(domain(iPr_def_10),domain(iPr_def_12)),
inference(superposition,[status(thm)],[c_61,c_362]) ).
tcf(c_371,plain,
! [X0: $i,X1: $i] : addition(domain(domain(X0)),addition(X1,domain(antidomain(X0)))) = addition(X1,addition(domain(iPr_def_10),domain(iPr_def_12))),
inference(superposition,[status(thm)],[c_362,c_217]) ).
tcf(c_389,plain,
! [X0: $i] : addition(antidomain(X0),addition(iPr_def_10,iPr_def_12)) = addition(domain(X0),antidomain(X0)),
inference(superposition,[status(thm)],[c_52,c_277]) ).
tcf(c_402,plain,
! [X0: $i] : addition(iPr_def_10,addition(iPr_def_12,antidomain(X0))) = addition(domain(X0),antidomain(X0)),
inference(theory_normalisation,[status(thm)],[c_389,c_50,c_49]) ).
tcf(c_403,plain,
! [X0: $i] : addition(iPr_def_10,addition(iPr_def_12,antidomain(X0))) = addition(iPr_def_10,iPr_def_12),
inference(light_normalisation,[status(thm)],[c_402,c_228]) ).
tcf(c_414,plain,
! [X0: $i] : addition(domain(iPr_def_10),domain(addition(iPr_def_12,antidomain(X0)))) = domain(addition(iPr_def_10,iPr_def_12)),
inference(superposition,[status(thm)],[c_403,c_64]) ).
tcf(c_615,plain,
! [X0: $i,X1: $i] : addition(multiplication(X0,domain(X1)),multiplication(X0,antidomain(X1))) = multiplication(X0,addition(iPr_def_10,iPr_def_12)),
inference(superposition,[status(thm)],[c_228,c_56]) ).
tcf(c_656,plain,
! [X0: $i,X1: $i] : addition(multiplication(domain(X0),X1),multiplication(antidomain(X0),X1)) = multiplication(addition(iPr_def_10,iPr_def_12),X1),
inference(superposition,[status(thm)],[c_228,c_57]) ).
tcf(c_688,plain,
! [X0: $i] :
( ( iPr_def_11 = iPr_def_12 )
| ( iPr_def_12 != X0 )
| ( iPr_def_11 != X0 ) ),
inference(instantiation,[status(thm)],[c_136]) ).
tcf(c_692,plain,
addition(domain(iPr_def_12),domain(multiplication(iPr_def_10,iPr_def_12))) = domain(iPr_def_12),
inference(superposition,[status(thm)],[c_355,c_64]) ).
tcf(c_712,plain,
! [X0: $i,X1: $i] :
( ( iPr_def_12 = X0 )
| ( iPr_def_12 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_136]) ).
tcf(c_774,plain,
! [X0: $i] :
( ( iPr_def_12 = X0 )
| ( iPr_def_12 != iPr_def_12 )
| ( X0 != iPr_def_12 ) ),
inference(instantiation,[status(thm)],[c_712]) ).
tcf(c_775,plain,
iPr_def_12 = iPr_def_12,
inference(instantiation,[status(thm)],[c_135]) ).
tcf(c_793,plain,
! [X0: $i,X1: $i] : addition(multiplication(X0,domain(X1)),multiplication(X0,antidomain(X1))) = X0,
inference(demodulation,[status(thm)],[c_615,c_56,c_240]) ).
tcf(c_803,plain,
! [X0: $i] : addition(multiplication(domain(X0),domain(X0)),multiplication(iPr_def_12,iPr_def_10)) = domain(X0),
inference(superposition,[status(thm)],[c_227,c_793]) ).
tcf(c_807,plain,
! [X0: $i] : addition(multiplication(X0,domain(iPr_def_10)),multiplication(X0,iPr_def_11)) = X0,
inference(superposition,[status(thm)],[c_130,c_793]) ).
tcf(c_816,plain,
! [X0: $i] : addition(multiplication(X0,iPr_def_11),multiplication(X0,domain(iPr_def_10))) = X0,
inference(theory_normalisation,[status(thm)],[c_807,c_50,c_49]) ).
tcf(c_821,plain,
! [X0: $i] : addition(multiplication(iPr_def_12,iPr_def_10),multiplication(domain(X0),domain(X0))) = domain(X0),
inference(theory_normalisation,[status(thm)],[c_803,c_50,c_49]) ).
tcf(c_835,plain,
iPr_def_11 = iPr_def_11,
inference(instantiation,[status(thm)],[c_135]) ).
tcf(c_836,plain,
! [X0: $i,X1: $i] :
( ( iPr_def_11 = X0 )
| ( iPr_def_11 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_136]) ).
tcf(c_839,plain,
! [X0: $i,X1: $i] : addition(multiplication(domain(X0),X1),multiplication(antidomain(X0),X1)) = X1,
inference(demodulation,[status(thm)],[c_656,c_57,c_242]) ).
tcf(c_841,plain,
! [X0: $i] : addition(multiplication(iPr_def_12,iPr_def_10),multiplication(antidomain(X0),antidomain(X0))) = antidomain(X0),
inference(superposition,[status(thm)],[c_227,c_839]) ).
tcf(c_855,plain,
! [X0: $i] : addition(multiplication(domain(iPr_def_10),X0),multiplication(iPr_def_11,X0)) = X0,
inference(superposition,[status(thm)],[c_130,c_839]) ).
tcf(c_864,plain,
! [X0: $i] : addition(multiplication(iPr_def_11,X0),multiplication(domain(iPr_def_10),X0)) = X0,
inference(theory_normalisation,[status(thm)],[c_855,c_50,c_49]) ).
tcf(c_878,plain,
! [X0: $i] : multiplication(antidomain(X0),antidomain(X0)) = antidomain(X0),
inference(demodulation,[status(thm)],[c_841,c_289]) ).
tcf(c_883,plain,
multiplication(iPr_def_11,iPr_def_11) = iPr_def_11,
inference(superposition,[status(thm)],[c_130,c_878]) ).
tcf(c_898,plain,
( ( iPr_def_12 = multiplication(iPr_def_12,one) )
| ( iPr_def_12 != iPr_def_12 )
| ( multiplication(iPr_def_12,one) != iPr_def_12 ) ),
inference(instantiation,[status(thm)],[c_774]) ).
tcf(c_899,plain,
multiplication(iPr_def_12,one) = iPr_def_12,
inference(instantiation,[status(thm)],[c_54]) ).
tcf(c_937,plain,
! [X0: $i] : addition(multiplication(X0,iPr_def_10),X0) = X0,
inference(superposition,[status(thm)],[c_240,c_320]) ).
tcf(c_948,plain,
! [X0: $i,X1: $i] : addition(multiplication(X0,domain(X1)),X0) = X0,
inference(superposition,[status(thm)],[c_793,c_320]) ).
tcf(c_949,plain,
! [X0: $i,X1: $i] : addition(multiplication(domain(X0),X1),X1) = X1,
inference(superposition,[status(thm)],[c_839,c_320]) ).
tcf(c_962,plain,
! [X0: $i] : addition(X0,multiplication(X0,iPr_def_10)) = X0,
inference(theory_normalisation,[status(thm)],[c_937,c_50,c_49]) ).
tcf(c_963,plain,
! [X0: $i,X1: $i] : addition(X0,multiplication(domain(X1),X0)) = X0,
inference(theory_normalisation,[status(thm)],[c_949,c_50,c_49]) ).
tcf(c_964,plain,
! [X0: $i,X1: $i] : addition(X0,multiplication(X0,domain(X1))) = X0,
inference(theory_normalisation,[status(thm)],[c_948,c_50,c_49]) ).
tcf(c_986,plain,
! [X0: $i] : multiplication(domain(X0),X0) = X0,
inference(demodulation,[status(thm)],[c_60,c_963]) ).
tcf(c_1003,plain,
! [X0: $i,X1: $i] : multiplication(domain(X0),multiplication(X0,X1)) = multiplication(X0,X1),
inference(superposition,[status(thm)],[c_986,c_53]) ).
tcf(c_1017,plain,
domain(multiplication(domain(sK0),iPr_def_12)) = domain(sK0),
inference(superposition,[status(thm)],[c_986,c_295]) ).
tcf(c_1020,plain,
domain(iPr_def_12) = iPr_def_12,
inference(light_normalisation,[status(thm)],[c_1017,c_131,c_351]) ).
tcf(c_1035,plain,
! [X0: $i] : addition(multiplication(iPr_def_12,X0),multiplication(antidomain(iPr_def_12),X0)) = X0,
inference(superposition,[status(thm)],[c_1020,c_839]) ).
tcf(c_1039,plain,
addition(iPr_def_12,antidomain(iPr_def_12)) = addition(iPr_def_10,iPr_def_12),
inference(superposition,[status(thm)],[c_1020,c_228]) ).
tcf(c_1081,plain,
addition(domain(iPr_def_12),domain(antidomain(iPr_def_12))) = domain(addition(iPr_def_10,iPr_def_12)),
inference(superposition,[status(thm)],[c_1039,c_64]) ).
tcf(c_1089,plain,
addition(iPr_def_12,domain(antidomain(iPr_def_12))) = domain(addition(iPr_def_10,iPr_def_12)),
inference(light_normalisation,[status(thm)],[c_1081,c_1020]) ).
tcf(c_1159,plain,
! [X0: $i] : multiplication(domain(X0),domain(X0)) = domain(X0),
inference(demodulation,[status(thm)],[c_821,c_289]) ).
tcf(c_1178,plain,
! [X0: $i] : domain(multiplication(domain(X0),X0)) = domain(domain(X0)),
inference(superposition,[status(thm)],[c_1159,c_61]) ).
tcf(c_1180,plain,
! [X0: $i] : domain(domain(X0)) = domain(X0),
inference(light_normalisation,[status(thm)],[c_1178,c_986]) ).
tcf(c_1238,plain,
! [X0: $i,X1: $i] : addition(X0,addition(multiplication(X0,iPr_def_10),X1)) = addition(X0,X1),
inference(superposition,[status(thm)],[c_962,c_50]) ).
tcf(c_1420,plain,
addition(iPr_def_12,domain(multiplication(iPr_def_10,iPr_def_12))) = iPr_def_12,
inference(light_normalisation,[status(thm)],[c_692,c_1020]) ).
tcf(c_1423,plain,
! [X0: $i] : addition(iPr_def_12,addition(domain(multiplication(iPr_def_10,iPr_def_12)),X0)) = addition(iPr_def_12,X0),
inference(superposition,[status(thm)],[c_1420,c_50]) ).
tcf(c_1515,plain,
! [X0: $i] : addition(X0,multiplication(X0,iPr_def_12)) = X0,
inference(superposition,[status(thm)],[c_1020,c_964]) ).
tcf(c_1547,plain,
! [X0: $i,X1: $i] : addition(X0,addition(multiplication(X0,iPr_def_12),X1)) = addition(X0,X1),
inference(superposition,[status(thm)],[c_1515,c_50]) ).
tcf(c_1815,plain,
! [X0: $i] : addition(multiplication(X0,iPr_def_11),X0) = X0,
inference(superposition,[status(thm)],[c_816,c_320]) ).
tcf(c_1823,plain,
! [X0: $i] : addition(X0,multiplication(X0,iPr_def_11)) = X0,
inference(theory_normalisation,[status(thm)],[c_1815,c_50,c_49]) ).
tcf(c_1841,plain,
! [X0: $i] : addition(multiplication(iPr_def_11,X0),X0) = X0,
inference(superposition,[status(thm)],[c_864,c_320]) ).
tcf(c_1849,plain,
! [X0: $i] : addition(X0,multiplication(iPr_def_11,X0)) = X0,
inference(theory_normalisation,[status(thm)],[c_1841,c_50,c_49]) ).
tcf(c_1872,plain,
! [X0: $i,X1: $i] : addition(X0,addition(multiplication(X0,iPr_def_11),X1)) = addition(X0,X1),
inference(superposition,[status(thm)],[c_1823,c_50]) ).
tcf(c_1903,plain,
! [X0: $i] : addition(iPr_def_10,addition(iPr_def_12,multiplication(iPr_def_11,antidomain(X0)))) = addition(domain(X0),antidomain(X0)),
inference(superposition,[status(thm)],[c_1849,c_331]) ).
tcf(c_1904,plain,
! [X0: $i] : addition(iPr_def_10,addition(iPr_def_12,multiplication(iPr_def_11,antidomain(X0)))) = addition(iPr_def_10,iPr_def_12),
inference(light_normalisation,[status(thm)],[c_1903,c_228]) ).
tcf(c_1962,plain,
! [X0: $i] : addition(domain(iPr_def_10),domain(addition(iPr_def_12,multiplication(iPr_def_11,antidomain(X0))))) = domain(addition(iPr_def_10,iPr_def_12)),
inference(superposition,[status(thm)],[c_1904,c_64]) ).
tcf(c_2018,plain,
! [X0: $i] :
( ( iPr_def_11 = X0 )
| ( iPr_def_11 != iPr_def_11 )
| ( X0 != iPr_def_11 ) ),
inference(instantiation,[status(thm)],[c_836]) ).
tcf(c_2319,plain,
! [X0: $i] : addition(iPr_def_12,addition(domain(iPr_def_10),domain(antidomain(X0)))) = addition(iPr_def_12,domain(iPr_def_10)),
inference(demodulation,[status(thm)],[c_414,c_49,c_64,c_217,c_1020]) ).
tcf(c_2321,plain,
addition(iPr_def_12,addition(domain(iPr_def_10),domain(iPr_def_11))) = addition(iPr_def_12,domain(iPr_def_10)),
inference(superposition,[status(thm)],[c_130,c_2319]) ).
tcf(c_3455,plain,
multiplication(antidomain(iPr_def_12),iPr_def_10) = iPr_def_10,
inference(superposition,[status(thm)],[c_1035,c_289]) ).
tcf(c_3466,plain,
multiplication(domain(antidomain(iPr_def_12)),iPr_def_10) = iPr_def_10,
inference(superposition,[status(thm)],[c_3455,c_1003]) ).
tcf(c_3489,plain,
addition(domain(antidomain(iPr_def_12)),iPr_def_10) = domain(antidomain(iPr_def_12)),
inference(superposition,[status(thm)],[c_3466,c_962]) ).
tcf(c_3494,plain,
addition(iPr_def_10,domain(antidomain(iPr_def_12))) = domain(antidomain(iPr_def_12)),
inference(theory_normalisation,[status(thm)],[c_3489,c_50,c_49]) ).
tcf(c_4330,plain,
! [X0: $i] : addition(domain(iPr_def_10),addition(iPr_def_10,X0)) = addition(domain(iPr_def_10),X0),
inference(superposition,[status(thm)],[c_986,c_1238]) ).
tcf(c_4362,plain,
! [X0: $i] : addition(iPr_def_10,addition(X0,domain(iPr_def_10))) = addition(domain(iPr_def_10),X0),
inference(theory_normalisation,[status(thm)],[c_4330,c_50,c_49]) ).
tcf(c_4544,plain,
! [X0: $i] : addition(iPr_def_12,addition(domain(iPr_def_10),domain(multiplication(iPr_def_11,antidomain(X0))))) = addition(iPr_def_10,iPr_def_12),
inference(demodulation,[status(thm)],[c_1962,c_64,c_217,c_233,c_1020,c_4362]) ).
tcf(c_4546,plain,
addition(iPr_def_12,addition(domain(iPr_def_10),domain(multiplication(iPr_def_11,iPr_def_11)))) = addition(iPr_def_10,iPr_def_12),
inference(superposition,[status(thm)],[c_130,c_4544]) ).
tcf(c_4561,plain,
addition(iPr_def_12,domain(iPr_def_10)) = addition(iPr_def_10,iPr_def_12),
inference(light_normalisation,[status(thm)],[c_4546,c_883,c_2321]) ).
tcf(c_5482,plain,
! [X0: $i] : addition(domain(iPr_def_12),addition(iPr_def_12,X0)) = addition(domain(iPr_def_12),X0),
inference(superposition,[status(thm)],[c_986,c_1547]) ).
tcf(c_5512,plain,
! [X0: $i] : addition(iPr_def_12,addition(X0,domain(iPr_def_12))) = addition(domain(iPr_def_12),X0),
inference(theory_normalisation,[status(thm)],[c_5482,c_50,c_49]) ).
tcf(c_5513,plain,
! [X0: $i] : addition(iPr_def_12,addition(X0,iPr_def_12)) = addition(iPr_def_12,X0),
inference(light_normalisation,[status(thm)],[c_5512,c_1020]) ).
tcf(c_5577,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_2018]) ).
tcf(c_5578,plain,
addition(iPr_def_11,zero) = iPr_def_11,
inference(instantiation,[status(thm)],[c_51]) ).
tcf(c_5926,plain,
! [X0: $i] : addition(domain(iPr_def_10),addition(multiplication(iPr_def_12,iPr_def_10),X0)) = addition(domain(iPr_def_10),X0),
inference(superposition,[status(thm)],[c_234,c_1872]) ).
tcf(c_5977,plain,
! [X0: $i] : addition(multiplication(iPr_def_12,iPr_def_10),addition(X0,domain(iPr_def_10))) = addition(domain(iPr_def_10),X0),
inference(theory_normalisation,[status(thm)],[c_5926,c_50,c_49]) ).
tcf(c_8021,plain,
! [X0: $i] : addition(X0,addition(iPr_def_12,iPr_def_12)) = addition(iPr_def_12,X0),
inference(superposition,[status(thm)],[c_5513,c_217]) ).
tcf(c_9447,plain,
addition(iPr_def_12,antidomain(multiplication(iPr_def_10,iPr_def_12))) = addition(iPr_def_12,addition(iPr_def_10,iPr_def_12)),
inference(superposition,[status(thm)],[c_228,c_1423]) ).
tcf(c_9528,plain,
addition(iPr_def_12,antidomain(multiplication(iPr_def_10,iPr_def_12))) = addition(iPr_def_10,addition(iPr_def_12,iPr_def_12)),
inference(theory_normalisation,[status(thm)],[c_9447,c_50,c_49]) ).
tcf(c_9822,plain,
addition(iPr_def_12,antidomain(multiplication(iPr_def_10,iPr_def_12))) = addition(iPr_def_10,iPr_def_12),
inference(demodulation,[status(thm)],[c_9528,c_49,c_8021]) ).
tcf(c_9827,plain,
addition(domain(iPr_def_12),domain(antidomain(multiplication(iPr_def_10,iPr_def_12)))) = domain(addition(iPr_def_10,iPr_def_12)),
inference(superposition,[status(thm)],[c_9822,c_64]) ).
tcf(c_9835,plain,
addition(iPr_def_12,domain(antidomain(multiplication(iPr_def_10,iPr_def_12)))) = domain(addition(iPr_def_10,iPr_def_12)),
inference(light_normalisation,[status(thm)],[c_9827,c_1020]) ).
tcf(c_11044,plain,
! [X0: $i,X1: $i] : addition(domain(domain(multiplication(X0,X1))),domain(antidomain(multiplication(X0,domain(X1))))) = addition(domain(iPr_def_10),iPr_def_12),
inference(light_normalisation,[status(thm)],[c_363,c_1020]) ).
tcf(c_11045,plain,
! [X0: $i,X1: $i] : addition(domain(multiplication(X0,X1)),domain(antidomain(multiplication(X0,domain(X1))))) = addition(iPr_def_10,iPr_def_12),
inference(demodulation,[status(thm)],[c_11044,c_289,c_1180,c_4561,c_5977]) ).
tcf(c_11135,plain,
addition(iPr_def_12,domain(antidomain(multiplication(iPr_def_10,domain(iPr_def_12))))) = addition(iPr_def_12,addition(iPr_def_10,iPr_def_12)),
inference(superposition,[status(thm)],[c_11045,c_1423]) ).
tcf(c_11145,plain,
addition(iPr_def_12,domain(antidomain(multiplication(iPr_def_10,domain(iPr_def_12))))) = addition(iPr_def_10,addition(iPr_def_12,iPr_def_12)),
inference(theory_normalisation,[status(thm)],[c_11135,c_50,c_49]) ).
tcf(c_11146,plain,
addition(iPr_def_10,addition(iPr_def_12,iPr_def_12)) = domain(addition(iPr_def_10,iPr_def_12)),
inference(light_normalisation,[status(thm)],[c_11145,c_1020,c_9835]) ).
tcf(c_12711,plain,
! [X0: $i,X1: $i] : addition(domain(X0),addition(X1,domain(antidomain(X0)))) = addition(X1,addition(domain(iPr_def_10),iPr_def_12)),
inference(light_normalisation,[status(thm)],[c_371,c_1020,c_1180]) ).
tcf(c_12712,plain,
! [X0: $i,X1: $i] : addition(domain(X0),addition(X1,domain(antidomain(X0)))) = addition(X1,addition(iPr_def_10,iPr_def_12)),
inference(demodulation,[status(thm)],[c_12711,c_289,c_4561,c_5977]) ).
tcf(c_12739,plain,
addition(domain(iPr_def_12),domain(antidomain(iPr_def_12))) = addition(iPr_def_10,addition(iPr_def_10,iPr_def_12)),
inference(superposition,[status(thm)],[c_3494,c_12712]) ).
tcf(c_12776,plain,
addition(iPr_def_10,addition(iPr_def_10,iPr_def_12)) = addition(iPr_def_10,addition(iPr_def_12,iPr_def_12)),
inference(light_normalisation,[status(thm)],[c_12739,c_1020,c_1089,c_11146]) ).
tcf(c_85428,plain,
( ( iPr_def_11 = iPr_def_12 )
| ( iPr_def_12 != addition(iPr_def_11,zero) )
| ( iPr_def_11 != addition(iPr_def_11,zero) ) ),
inference(instantiation,[status(thm)],[c_688]) ).
tcf(c_87241,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_87242,plain,
addition(iPr_def_10,addition(iPr_def_10,iPr_def_12)) = addition(iPr_def_10,iPr_def_12),
inference(demodulation,[status(thm)],[c_12776,c_52]) ).
tcf(c_87245,plain,
addition(domain(sK0),iPr_def_10) = one,
inference(superposition,[status(thm)],[c_129,c_133]) ).
tcf(c_87248,plain,
addition(iPr_def_10,domain(sK0)) = one,
inference(theory_normalisation,[status(thm)],[c_87245,c_50,c_49]) ).
tcf(c_87249,plain,
addition(iPr_def_10,iPr_def_12) = one,
inference(light_normalisation,[status(thm)],[c_87248,c_131]) ).
tcf(c_87250,plain,
addition(iPr_def_10,one) = one,
inference(demodulation,[status(thm)],[c_87242,c_87249]) ).
tcf(c_87253,plain,
addition(domain(iPr_def_10),iPr_def_11) = one,
inference(superposition,[status(thm)],[c_130,c_133]) ).
tcf(c_87255,plain,
addition(iPr_def_11,domain(iPr_def_10)) = one,
inference(theory_normalisation,[status(thm)],[c_87253,c_50,c_49]) ).
tcf(c_87263,plain,
! [X0: $i] : addition(zero,X0) = X0,
inference(superposition,[status(thm)],[c_51,c_49]) ).
tcf(c_87280,plain,
! [X0: $i,X1: $i] : addition(domain(X0),addition(X1,antidomain(X0))) = addition(X1,one),
inference(superposition,[status(thm)],[c_133,c_87241]) ).
tcf(c_87291,plain,
! [X0: $i] : domain(multiplication(one,X0)) = domain(domain(X0)),
inference(superposition,[status(thm)],[c_55,c_61]) ).
tcf(c_87300,plain,
! [X0: $i] : domain(domain(X0)) = domain(X0),
inference(light_normalisation,[status(thm)],[c_87291,c_55]) ).
tcf(c_87310,plain,
! [X0: $i,X1: $i] : addition(domain(X0),domain(X1)) = domain(addition(X1,X0)),
inference(superposition,[status(thm)],[c_64,c_49]) ).
tcf(c_87364,plain,
domain(iPr_def_12) = iPr_def_12,
inference(superposition,[status(thm)],[c_131,c_87300]) ).
tcf(c_87367,plain,
! [X0: $i] : addition(domain(X0),antidomain(domain(X0))) = one,
inference(superposition,[status(thm)],[c_87300,c_133]) ).
tcf(c_87369,plain,
! [X0: $i,X1: $i] : addition(domain(X0),domain(X1)) = domain(addition(X0,domain(X1))),
inference(superposition,[status(thm)],[c_87300,c_64]) ).
tcf(c_87370,plain,
! [X0: $i,X1: $i] : domain(addition(X0,domain(X1))) = domain(addition(X1,X0)),
inference(light_normalisation,[status(thm)],[c_87369,c_87310]) ).
tcf(c_87375,plain,
multiplication(iPr_def_12,antidomain(iPr_def_12)) = zero,
inference(superposition,[status(thm)],[c_87364,c_132]) ).
tcf(c_87376,plain,
! [X0: $i] : addition(domain(X0),iPr_def_12) = domain(addition(X0,iPr_def_12)),
inference(superposition,[status(thm)],[c_87364,c_64]) ).
tcf(c_87378,plain,
! [X0: $i] : addition(iPr_def_12,domain(X0)) = domain(addition(X0,iPr_def_12)),
inference(theory_normalisation,[status(thm)],[c_87376,c_50,c_49]) ).
tcf(c_87421,plain,
! [X0: $i] : addition(domain(X0),antidomain(X0)) = addition(antidomain(X0),one),
inference(superposition,[status(thm)],[c_52,c_87280]) ).
tcf(c_87444,plain,
! [X0: $i] : addition(domain(X0),antidomain(X0)) = addition(one,antidomain(X0)),
inference(theory_normalisation,[status(thm)],[c_87421,c_50,c_49]) ).
tcf(c_87445,plain,
! [X0: $i] : addition(one,antidomain(X0)) = one,
inference(light_normalisation,[status(thm)],[c_87444,c_133]) ).
tcf(c_87529,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_87531,plain,
! [X0: $i,X1: $i] : addition(zero,multiplication(X0,X1)) = multiplication(X0,addition(zero,X1)),
inference(superposition,[status(thm)],[c_58,c_56]) ).
tcf(c_87533,plain,
! [X0: $i,X1: $i] : multiplication(domain(X0),addition(antidomain(X0),X1)) = addition(zero,multiplication(domain(X0),X1)),
inference(superposition,[status(thm)],[c_132,c_56]) ).
tcf(c_87573,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_87576,plain,
! [X0: $i,X1: $i] : multiplication(addition(domain(X0),X1),antidomain(X0)) = addition(zero,multiplication(X1,antidomain(X0))),
inference(superposition,[status(thm)],[c_132,c_57]) ).
tcf(c_87586,plain,
! [X0: $i,X1: $i] : addition(multiplication(X0,X1),zero) = multiplication(addition(X0,zero),X1),
inference(superposition,[status(thm)],[c_59,c_57]) ).
tcf(c_87591,plain,
! [X0: $i] : addition(multiplication(X0,antidomain(iPr_def_12)),zero) = multiplication(addition(X0,iPr_def_12),antidomain(iPr_def_12)),
inference(superposition,[status(thm)],[c_87375,c_57]) ).
tcf(c_87603,plain,
! [X0: $i,X1: $i] : addition(zero,multiplication(X0,X1)) = multiplication(addition(X0,zero),X1),
inference(theory_normalisation,[status(thm)],[c_87586,c_50,c_49]) ).
tcf(c_87604,plain,
! [X0: $i,X1: $i] : multiplication(X0,addition(zero,X1)) = multiplication(X0,X1),
inference(light_normalisation,[status(thm)],[c_87603,c_51,c_87531]) ).
tcf(c_87611,plain,
! [X0: $i] : addition(zero,multiplication(X0,antidomain(iPr_def_12))) = multiplication(addition(X0,iPr_def_12),antidomain(iPr_def_12)),
inference(theory_normalisation,[status(thm)],[c_87591,c_50,c_49]) ).
tcf(c_87615,plain,
! [X0: $i] : multiplication(addition(one,domain(X0)),X0) = multiplication(domain(X0),X0),
inference(demodulation,[status(thm)],[c_60,c_87573]) ).
tcf(c_87616,plain,
! [X0: $i] : multiplication(domain(X0),X0) = X0,
inference(light_normalisation,[status(thm)],[c_87615,c_55,c_83]) ).
tcf(c_87621,plain,
! [X0: $i,X1: $i] : multiplication(domain(multiplication(X0,X1)),multiplication(X0,domain(X1))) = multiplication(X0,domain(X1)),
inference(superposition,[status(thm)],[c_61,c_87616]) ).
tcf(c_87629,plain,
domain(one) = one,
inference(superposition,[status(thm)],[c_87616,c_54]) ).
tcf(c_87797,plain,
! [X0: $i,X1: $i] : multiplication(domain(X0),addition(antidomain(X0),X1)) = multiplication(domain(X0),X1),
inference(demodulation,[status(thm)],[c_87533,c_87531,c_87604]) ).
tcf(c_87800,plain,
! [X0: $i] : multiplication(iPr_def_12,addition(antidomain(sK0),X0)) = multiplication(iPr_def_12,X0),
inference(superposition,[status(thm)],[c_131,c_87797]) ).
tcf(c_87822,plain,
! [X0: $i] : multiplication(iPr_def_12,addition(iPr_def_10,X0)) = multiplication(iPr_def_12,X0),
inference(light_normalisation,[status(thm)],[c_87800,c_129]) ).
tcf(c_87830,plain,
! [X0: $i,X1: $i] : multiplication(addition(domain(X0),X1),antidomain(X0)) = multiplication(X1,antidomain(X0)),
inference(demodulation,[status(thm)],[c_87576,c_87531,c_87604]) ).
tcf(c_87836,plain,
! [X0: $i] : multiplication(antidomain(X0),antidomain(X0)) = multiplication(one,antidomain(X0)),
inference(superposition,[status(thm)],[c_133,c_87830]) ).
tcf(c_87841,plain,
! [X0: $i] : multiplication(antidomain(domain(X0)),antidomain(X0)) = multiplication(one,antidomain(X0)),
inference(superposition,[status(thm)],[c_87367,c_87830]) ).
tcf(c_87848,plain,
! [X0: $i] : multiplication(addition(domain(sK0),X0),iPr_def_10) = multiplication(X0,iPr_def_10),
inference(superposition,[status(thm)],[c_129,c_87830]) ).
tcf(c_87850,plain,
! [X0: $i] : multiplication(addition(domain(iPr_def_10),X0),iPr_def_11) = multiplication(X0,iPr_def_11),
inference(superposition,[status(thm)],[c_130,c_87830]) ).
tcf(c_87861,plain,
! [X0: $i] : multiplication(addition(iPr_def_12,X0),iPr_def_10) = multiplication(X0,iPr_def_10),
inference(light_normalisation,[status(thm)],[c_87848,c_131]) ).
tcf(c_87870,plain,
! [X0: $i,X1: $i] :
( ( iPr_def_12 = X0 )
| ( iPr_def_12 != X1 )
| ( X0 != X1 ) ),
inference(instantiation,[status(thm)],[c_136]) ).
tcf(c_87873,plain,
! [X0: $i] : multiplication(antidomain(X0),antidomain(X0)) = antidomain(X0),
inference(demodulation,[status(thm)],[c_87836,c_55]) ).
tcf(c_87878,plain,
multiplication(iPr_def_10,iPr_def_10) = iPr_def_10,
inference(superposition,[status(thm)],[c_129,c_87873]) ).
tcf(c_87937,plain,
! [X0: $i] : addition(iPr_def_10,multiplication(iPr_def_10,X0)) = multiplication(iPr_def_10,addition(iPr_def_10,X0)),
inference(superposition,[status(thm)],[c_87878,c_56]) ).
tcf(c_88943,plain,
! [X0: $i] : multiplication(antidomain(domain(X0)),antidomain(X0)) = antidomain(X0),
inference(demodulation,[status(thm)],[c_87841,c_55]) ).
tcf(c_89498,plain,
! [X0: $i] :
( ( iPr_def_12 = X0 )
| ( iPr_def_12 != multiplication(iPr_def_12,one) )
| ( X0 != multiplication(iPr_def_12,one) ) ),
inference(instantiation,[status(thm)],[c_87870]) ).
tcf(c_91544,plain,
addition(iPr_def_12,domain(iPr_def_10)) = domain(one),
inference(superposition,[status(thm)],[c_87249,c_87378]) ).
tcf(c_91590,plain,
addition(iPr_def_12,domain(iPr_def_10)) = one,
inference(light_normalisation,[status(thm)],[c_91544,c_87629]) ).
tcf(c_98185,plain,
domain(addition(iPr_def_10,iPr_def_11)) = domain(one),
inference(superposition,[status(thm)],[c_87255,c_87370]) ).
tcf(c_98295,plain,
domain(addition(iPr_def_10,iPr_def_11)) = one,
inference(light_normalisation,[status(thm)],[c_98185,c_87629]) ).
tcf(c_98512,plain,
! [X0: $i] : domain(multiplication(X0,addition(iPr_def_10,iPr_def_11))) = domain(multiplication(X0,one)),
inference(superposition,[status(thm)],[c_98295,c_61]) ).
tcf(c_98537,plain,
! [X0: $i] : domain(multiplication(X0,addition(iPr_def_10,iPr_def_11))) = domain(X0),
inference(light_normalisation,[status(thm)],[c_98512,c_54]) ).
tcf(c_101456,plain,
domain(multiplication(iPr_def_12,iPr_def_11)) = domain(iPr_def_12),
inference(superposition,[status(thm)],[c_87822,c_98537]) ).
tcf(c_101536,plain,
domain(multiplication(iPr_def_12,iPr_def_11)) = iPr_def_12,
inference(light_normalisation,[status(thm)],[c_101456,c_87364]) ).
tcf(c_101840,plain,
addition(iPr_def_12,antidomain(multiplication(iPr_def_12,iPr_def_11))) = one,
inference(superposition,[status(thm)],[c_101536,c_133]) ).
tcf(c_101960,plain,
multiplication(antidomain(multiplication(iPr_def_12,iPr_def_11)),iPr_def_10) = multiplication(one,iPr_def_10),
inference(superposition,[status(thm)],[c_101840,c_87861]) ).
tcf(c_102279,plain,
multiplication(antidomain(multiplication(iPr_def_12,iPr_def_11)),iPr_def_10) = iPr_def_10,
inference(demodulation,[status(thm)],[c_101960,c_55]) ).
tcf(c_102688,plain,
! [X0: $i] : multiplication(addition(X0,domain(iPr_def_10)),iPr_def_11) = multiplication(X0,iPr_def_11),
inference(superposition,[status(thm)],[c_49,c_87850]) ).
tcf(c_114071,plain,
! [X0: $i] : multiplication(antidomain(domain(X0)),addition(one,antidomain(X0))) = addition(antidomain(domain(X0)),antidomain(X0)),
inference(superposition,[status(thm)],[c_88943,c_87529]) ).
tcf(c_114294,plain,
! [X0: $i] : multiplication(antidomain(domain(X0)),addition(one,antidomain(X0))) = addition(antidomain(X0),antidomain(domain(X0))),
inference(theory_normalisation,[status(thm)],[c_114071,c_50,c_49]) ).
tcf(c_114295,plain,
! [X0: $i] : addition(antidomain(X0),antidomain(domain(X0))) = multiplication(antidomain(domain(X0)),one),
inference(light_normalisation,[status(thm)],[c_114294,c_87445]) ).
tcf(c_114441,plain,
! [X0: $i] : addition(antidomain(X0),antidomain(domain(X0))) = antidomain(domain(X0)),
inference(demodulation,[status(thm)],[c_114295,c_54]) ).
tcf(c_114490,plain,
addition(antidomain(sK0),antidomain(iPr_def_12)) = antidomain(iPr_def_12),
inference(superposition,[status(thm)],[c_131,c_114441]) ).
tcf(c_114562,plain,
addition(antidomain(iPr_def_12),antidomain(sK0)) = antidomain(iPr_def_12),
inference(theory_normalisation,[status(thm)],[c_114490,c_50,c_49]) ).
tcf(c_114563,plain,
addition(antidomain(iPr_def_12),iPr_def_10) = antidomain(iPr_def_12),
inference(light_normalisation,[status(thm)],[c_114562,c_129]) ).
tcf(c_114564,plain,
addition(iPr_def_10,antidomain(iPr_def_12)) = antidomain(iPr_def_12),
inference(theory_normalisation,[status(thm)],[c_114563,c_50,c_49]) ).
tcf(c_115037,plain,
multiplication(one,iPr_def_11) = multiplication(iPr_def_12,iPr_def_11),
inference(superposition,[status(thm)],[c_91590,c_102688]) ).
tcf(c_115106,plain,
multiplication(iPr_def_12,iPr_def_11) = iPr_def_11,
inference(demodulation,[status(thm)],[c_115037,c_55]) ).
tcf(c_115114,plain,
multiplication(antidomain(iPr_def_11),iPr_def_10) = iPr_def_10,
inference(demodulation,[status(thm)],[c_102279,c_115106]) ).
tcf(c_115117,plain,
domain(iPr_def_11) = iPr_def_12,
inference(demodulation,[status(thm)],[c_101536,c_115106]) ).
tcf(c_115142,plain,
! [X0: $i] : addition(iPr_def_11,multiplication(iPr_def_12,X0)) = multiplication(iPr_def_12,addition(iPr_def_11,X0)),
inference(superposition,[status(thm)],[c_115106,c_56]) ).
tcf(c_115216,plain,
multiplication(antidomain(iPr_def_12),antidomain(iPr_def_11)) = antidomain(iPr_def_11),
inference(superposition,[status(thm)],[c_115117,c_88943]) ).
tcf(c_115306,plain,
multiplication(antidomain(iPr_def_11),addition(one,iPr_def_10)) = addition(antidomain(iPr_def_11),iPr_def_10),
inference(superposition,[status(thm)],[c_115114,c_87529]) ).
tcf(c_115323,plain,
multiplication(antidomain(iPr_def_11),addition(iPr_def_10,one)) = addition(iPr_def_10,antidomain(iPr_def_11)),
inference(theory_normalisation,[status(thm)],[c_115306,c_50,c_49]) ).
tcf(c_115324,plain,
addition(iPr_def_10,antidomain(iPr_def_11)) = multiplication(antidomain(iPr_def_11),one),
inference(light_normalisation,[status(thm)],[c_115323,c_87250]) ).
tcf(c_130552,plain,
addition(iPr_def_10,antidomain(iPr_def_11)) = antidomain(iPr_def_11),
inference(demodulation,[status(thm)],[c_115324,c_54]) ).
tcf(c_139751,plain,
! [X0: $i] : multiplication(iPr_def_10,addition(one,X0)) = multiplication(iPr_def_10,addition(iPr_def_10,X0)),
inference(demodulation,[status(thm)],[c_87937,c_87529]) ).
tcf(c_139765,plain,
! [X0: $i] : multiplication(iPr_def_10,addition(iPr_def_10,antidomain(X0))) = multiplication(iPr_def_10,one),
inference(superposition,[status(thm)],[c_87445,c_139751]) ).
tcf(c_139912,plain,
! [X0: $i] : multiplication(iPr_def_10,addition(iPr_def_10,antidomain(X0))) = iPr_def_10,
inference(demodulation,[status(thm)],[c_139765,c_54]) ).
tcf(c_139913,plain,
multiplication(iPr_def_10,antidomain(iPr_def_12)) = iPr_def_10,
inference(superposition,[status(thm)],[c_114564,c_139912]) ).
tcf(c_139914,plain,
multiplication(iPr_def_10,antidomain(iPr_def_11)) = iPr_def_10,
inference(superposition,[status(thm)],[c_130552,c_139912]) ).
tcf(c_144485,plain,
! [X0: $i] : multiplication(addition(X0,iPr_def_12),antidomain(iPr_def_12)) = multiplication(X0,antidomain(iPr_def_12)),
inference(demodulation,[status(thm)],[c_87611,c_87263]) ).
tcf(c_144492,plain,
multiplication(one,antidomain(iPr_def_12)) = multiplication(iPr_def_10,antidomain(iPr_def_12)),
inference(superposition,[status(thm)],[c_87249,c_144485]) ).
tcf(c_144533,plain,
multiplication(one,antidomain(iPr_def_12)) = iPr_def_10,
inference(light_normalisation,[status(thm)],[c_144492,c_139913]) ).
tcf(c_145071,plain,
antidomain(iPr_def_12) = iPr_def_10,
inference(demodulation,[status(thm)],[c_144533,c_55]) ).
tcf(c_145092,plain,
multiplication(iPr_def_10,antidomain(iPr_def_11)) = antidomain(iPr_def_11),
inference(demodulation,[status(thm)],[c_115216,c_145071]) ).
tcf(c_145125,plain,
antidomain(iPr_def_11) = iPr_def_10,
inference(light_normalisation,[status(thm)],[c_145092,c_139914]) ).
tcf(c_149113,plain,
! [X0: $i] : multiplication(domain(zero),multiplication(domain(X0),domain(antidomain(X0)))) = multiplication(domain(X0),domain(antidomain(X0))),
inference(superposition,[status(thm)],[c_132,c_87621]) ).
tcf(c_149414,plain,
! [X0: $i] : multiplication(zero,multiplication(domain(X0),domain(antidomain(X0)))) = multiplication(domain(X0),domain(antidomain(X0))),
inference(light_normalisation,[status(thm)],[c_149113,c_63]) ).
tcf(c_199404,plain,
! [X0: $i] : multiplication(domain(X0),domain(antidomain(X0))) = zero,
inference(demodulation,[status(thm)],[c_149414,c_59]) ).
tcf(c_199484,plain,
multiplication(domain(iPr_def_11),domain(iPr_def_10)) = zero,
inference(superposition,[status(thm)],[c_145125,c_199404]) ).
tcf(c_199632,plain,
multiplication(iPr_def_12,domain(iPr_def_10)) = zero,
inference(light_normalisation,[status(thm)],[c_199484,c_115117]) ).
tcf(c_200468,plain,
( ( iPr_def_12 = addition(iPr_def_11,zero) )
| ( iPr_def_12 != multiplication(iPr_def_12,one) )
| ( addition(iPr_def_11,zero) != multiplication(iPr_def_12,one) ) ),
inference(instantiation,[status(thm)],[c_89498]) ).
tcf(c_203986,plain,
multiplication(iPr_def_12,addition(iPr_def_11,domain(iPr_def_10))) = addition(iPr_def_11,zero),
inference(superposition,[status(thm)],[c_199632,c_115142]) ).
tcf(c_204019,plain,
addition(iPr_def_11,zero) = multiplication(iPr_def_12,one),
inference(light_normalisation,[status(thm)],[c_203986,c_87255]) ).
tcf(c_206337,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_204019,c_200468,c_85428,c_5578,c_5577,c_899,c_898,c_835,c_775,c_134]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : KLE080+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.13/0.40 % Computer : n026.cluster.edu
% 0.13/0.40 % Model : x86_64 x86_64
% 0.13/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.40 % Memory : 8046.5625MB
% 0.13/0.40 % OS : Linux 6.8.0-71-generic
% 0.13/0.40 % CPULimit : 300
% 0.13/0.40 % WCLimit : 300
% 0.13/0.40 % DateTime : Wed Sep 23 18:55:08 UTC 2026
% 0.13/0.41 % CPUTime :
% 0.13/0.41 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.13/0.46 Running first-order theorem proving
% 0.13/0.46 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.19/0.48
% 0.19/0.48 % ======== iProver multi-core TPTP/SMT =========
% 0.19/0.48
% 0.19/0.48 % Detected problem language: tptp
% 0.19/0.49 % Proving...
% 94.35/23.22 % SZS status Started for theBenchmark.p
% 94.35/23.22 % SZS status Theorem for theBenchmark.p
% 94.35/23.22
% 94.35/23.22 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 94.35/23.22
% 94.35/23.22 % ------ iProver source info
% 94.35/23.22
% 94.35/23.22 % git: date: 2026-07-19 20:42:38 +0200
% 94.35/23.22 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 94.35/23.22 % git: non_committed_changes: false
% 94.35/23.22
% 94.35/23.22 % ------ Parsing...
% 94.35/23.22 % ------ Clausification by vclausify_rel & Parsing by iProver...% ------ preprocesses with Option_UEQ
% 94.35/23.22 %
% 94.35/23.22
% 94.35/23.22 % ------ Preprocessing... sup_sim: 0 sf_s rm: 0 0s sf_e pe_s pe_e %
% 94.35/23.22
% 94.35/23.22 % ------ Preprocessing...% ------ preprocesses with Option_UEQ
% 94.35/23.22 gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 94.35/23.22
% 94.35/23.22 % ------ Preprocessing... sf_s rm: 0 0s sf_e
% 94.35/23.22 % ------ Proving...
% 94.35/23.22 % ------ Problem Properties
% 94.35/23.22
% 94.35/23.22 %
% 94.35/23.22 % clauses 22
% 94.35/23.22 % conjectures 3
% 94.35/23.22 % EPR 1
% 94.35/23.22 % Horn 22
% 94.35/23.22 % unary 22
% 94.35/23.22 % binary 0
% 94.35/23.22 % lits 22
% 94.35/23.22 % lits eq 22
% 94.35/23.22 % fd_pure 0
% 94.35/23.22 % fd_pseudo 0
% 94.35/23.22 % fd_cond 0
% 94.35/23.22 % fd_pseudo_cond 0
% 94.35/23.22 % AC symbols 1
% 94.35/23.22
% 94.35/23.22 % ------ Schedule UEQ
% 94.35/23.22
% 94.35/23.22 % ------ Option_UEQ Time Limit: 10.
% 94.35/23.22
% 94.35/23.22
% 94.35/23.22 % ------
% 94.35/23.22 % Current options:
% 94.35/23.22 % ------
% 94.35/23.22
% 94.35/23.22
% 94.35/23.22 %
% 94.35/23.22
% 94.35/23.22 % ------ Proving...
% 94.35/23.22 % Proof_search_loop: time out after: 1469 full_loop iterations
% 94.35/23.22
% 94.35/23.22 % ------ Option_UEQ Time Limit: 15.
% 94.35/23.22
% 94.35/23.22
% 94.35/23.22 % ------
% 94.35/23.22 % Current options:
% 94.35/23.22 % ------
% 94.35/23.22
% 94.35/23.22
% 94.35/23.22 %
% 94.35/23.22
% 94.35/23.22 % ------ Proving...
% 94.35/23.22 %
% 94.35/23.22
% 94.35/23.22 % SZS status Theorem for theBenchmark.p
% 94.35/23.22
% 94.35/23.22 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 94.35/23.23
% 94.35/23.23
%------------------------------------------------------------------------------