%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : KLE108-10 : TPTP v9.3.1. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% Computer : n017.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 01:52:25 PM UTC 2026
% Result : Unsatisfiable 87.55s 12.35s
% Output : CNFRefutation 87.55s
% Verified :
% SZS Type : Refutation
% Derivation depth : 41
% Number of leaves : 47
% Syntax : Number of formulae : 253 ( 253 unt; 22 def)
% Number of atoms : 645 ( 252 equ)
% Maximal formula atoms : 1 ( 2 avg)
% Number of connectives : 7 ( 7 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 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 : 24 ( 22 usr; 23 prp; 0-2 aty)
% Number of functors : 15 ( 15 usr; 5 con; 0-2 aty)
% Number of variables : 168 ( 0 sgn 168 !; 0 ?; 112 :)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
! [X0,X1] : addition(X0,X1) = addition(X1,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',additive_commutativity) ).
fof(f4,axiom,
! [X2,X0,X1] : addition(X0,addition(X1,X2)) = addition(addition(X0,X1),X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',additive_associativity) ).
fof(f5,axiom,
! [X0] : addition(X0,zero) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',additive_identity) ).
fof(f6,axiom,
! [X0] : addition(X0,X0) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',additive_idempotence) ).
fof(f7,axiom,
! [X2,X0,X1] : multiplication(X0,multiplication(X1,X2)) = multiplication(multiplication(X0,X1),X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',multiplicative_associativity) ).
fof(f8,axiom,
! [X0] : multiplication(X0,one) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',multiplicative_right_identity) ).
fof(f9,axiom,
! [X0] : multiplication(one,X0) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',multiplicative_left_identity) ).
fof(f10,axiom,
! [X2,X0,X1] : multiplication(X0,addition(X1,X2)) = addition(multiplication(X0,X1),multiplication(X0,X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',right_distributivity) ).
fof(f11,axiom,
! [X2,X0,X1] : multiplication(addition(X0,X1),X2) = addition(multiplication(X0,X2),multiplication(X1,X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',left_distributivity) ).
fof(f12,axiom,
! [X0] : multiplication(X0,zero) = zero,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',right_annihilation) ).
fof(f13,plain,
! [X0] : zero = multiplication(X0,zero),
inference(reorient_equations,[],[f12]) ).
fof(f14,axiom,
! [X0] : multiplication(zero,X0) = zero,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',left_annihilation) ).
fof(f15,plain,
! [X0] : zero = multiplication(zero,X0),
inference(reorient_equations,[],[f14]) ).
fof(f19,axiom,
! [X0] : multiplication(antidomain(X0),X0) = zero,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',domain1) ).
fof(f20,plain,
! [X0] : zero = multiplication(antidomain(X0),X0),
inference(reorient_equations,[],[f19]) ).
fof(f21,axiom,
! [X0,X1] : addition(antidomain(multiplication(X0,X1)),antidomain(multiplication(X0,antidomain(antidomain(X1))))) = antidomain(multiplication(X0,antidomain(antidomain(X1)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',domain2) ).
fof(f22,plain,
! [X0,X1] : antidomain(multiplication(X0,antidomain(antidomain(X1)))) = addition(antidomain(multiplication(X0,X1)),antidomain(multiplication(X0,antidomain(antidomain(X1))))),
inference(reorient_equations,[],[f21]) ).
fof(f23,axiom,
! [X0] : addition(antidomain(antidomain(X0)),antidomain(X0)) = one,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',domain3) ).
fof(f24,plain,
! [X0] : one = addition(antidomain(antidomain(X0)),antidomain(X0)),
inference(reorient_equations,[],[f23]) ).
fof(f25,axiom,
! [X0] : domain(X0) = antidomain(antidomain(X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',domain4) ).
fof(f26,plain,
! [X0] : antidomain(antidomain(X0)) = domain(X0),
inference(reorient_equations,[],[f25]) ).
fof(f27,axiom,
! [X0] : multiplication(X0,coantidomain(X0)) = zero,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',codomain1) ).
fof(f28,plain,
! [X0] : zero = multiplication(X0,coantidomain(X0)),
inference(reorient_equations,[],[f27]) ).
fof(f29,axiom,
! [X0,X1] : addition(coantidomain(multiplication(X0,X1)),coantidomain(multiplication(coantidomain(coantidomain(X0)),X1))) = coantidomain(multiplication(coantidomain(coantidomain(X0)),X1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',codomain2) ).
fof(f30,plain,
! [X0,X1] : coantidomain(multiplication(coantidomain(coantidomain(X0)),X1)) = addition(coantidomain(multiplication(X0,X1)),coantidomain(multiplication(coantidomain(coantidomain(X0)),X1))),
inference(reorient_equations,[],[f29]) ).
fof(f31,axiom,
! [X0] : addition(coantidomain(coantidomain(X0)),coantidomain(X0)) = one,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',codomain3) ).
fof(f32,plain,
! [X0] : one = addition(coantidomain(coantidomain(X0)),coantidomain(X0)),
inference(reorient_equations,[],[f31]) ).
fof(f33,axiom,
! [X0] : codomain(X0) = coantidomain(coantidomain(X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',codomain4) ).
fof(f34,plain,
! [X0] : coantidomain(coantidomain(X0)) = codomain(X0),
inference(reorient_equations,[],[f33]) ).
fof(f35,axiom,
! [X0] : c(X0) = antidomain(domain(X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',complement) ).
fof(f37,axiom,
! [X0,X1] : forward_diamond(X0,X1) = domain(multiplication(X0,domain(X1))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',forward_diamond) ).
fof(f38,axiom,
! [X0,X1] : backward_diamond(X0,X1) = codomain(multiplication(codomain(X1),X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',backward_diamond) ).
fof(f39,axiom,
! [X0,X1] : forward_box(X0,X1) = c(forward_diamond(X0,c(X1))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',forward_box) ).
fof(f41,negated_conjecture,
addition(domain(sK2_goals_X1),forward_box(sK3_goals_X0,domain(sK1_goals_X2))) = forward_box(sK3_goals_X0,domain(sK1_goals_X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goals) ).
fof(f42,plain,
forward_box(sK3_goals_X0,domain(sK1_goals_X2)) = addition(domain(sK2_goals_X1),forward_box(sK3_goals_X0,domain(sK1_goals_X2))),
inference(reorient_equations,[],[f41]) ).
fof(f43,negated_conjecture,
addition(backward_diamond(sK3_goals_X0,domain(sK2_goals_X1)),domain(sK1_goals_X2)) != domain(sK1_goals_X2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goals_1) ).
fof(f44,plain,
domain(sK1_goals_X2) != addition(backward_diamond(sK3_goals_X0,domain(sK2_goals_X1)),domain(sK1_goals_X2)),
inference(reorient_equations,[],[f43]) ).
fof(f46,plain,
! [X0,X1] : forward_diamond(X0,X1) = antidomain(antidomain(multiplication(X0,antidomain(antidomain(X1))))),
inference(definition_unfolding,[],[f37,f26,f26]) ).
fof(f47,plain,
! [X0,X1] : backward_diamond(X0,X1) = coantidomain(coantidomain(multiplication(coantidomain(coantidomain(X1)),X0))),
inference(definition_unfolding,[],[f38,f34,f34]) ).
fof(f48,plain,
! [X0] : c(X0) = antidomain(antidomain(antidomain(X0))),
inference(definition_unfolding,[],[f35,f26]) ).
fof(f49,plain,
! [X0,X1] : forward_box(X0,X1) = antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(X0,antidomain(antidomain(antidomain(antidomain(antidomain(X1))))))))))),
inference(definition_unfolding,[],[f39,f48,f46,f48]) ).
fof(f51,plain,
antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK3_goals_X0,antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sK1_goals_X2))))))))))))) = addition(antidomain(antidomain(sK2_goals_X1)),antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK3_goals_X0,antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sK1_goals_X2)))))))))))))),
inference(definition_unfolding,[],[f42,f49,f26,f26,f49,f26]) ).
fof(f52,plain,
antidomain(antidomain(sK1_goals_X2)) != addition(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(sK2_goals_X1)))),sK3_goals_X0))),antidomain(antidomain(sK1_goals_X2))),
inference(definition_unfolding,[],[f44,f26,f47,f26,f26]) ).
tcf(c_82,negated_conjecture,
! [X0: $i,X1: $i] : addition(X0,X1) = addition(X1,X0),
inference(cnf_transformation,[],[f3]) ).
tcf(c_83,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] : addition(addition(X0,X1),X2) = addition(X0,addition(X1,X2)),
inference(cnf_transformation,[],[f4]) ).
tcf(c_84,negated_conjecture,
! [X0: $i] : addition(X0,zero) = X0,
inference(cnf_transformation,[],[f5]) ).
tcf(c_85,negated_conjecture,
! [X0: $i] : addition(X0,X0) = X0,
inference(cnf_transformation,[],[f6]) ).
tcf(c_86,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] : multiplication(multiplication(X0,X1),X2) = multiplication(X0,multiplication(X1,X2)),
inference(cnf_transformation,[],[f7]) ).
tcf(c_87,negated_conjecture,
! [X0: $i] : multiplication(X0,one) = X0,
inference(cnf_transformation,[],[f8]) ).
tcf(c_88,negated_conjecture,
! [X0: $i] : multiplication(one,X0) = X0,
inference(cnf_transformation,[],[f9]) ).
tcf(c_89,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] : addition(multiplication(X0,X1),multiplication(X0,X2)) = multiplication(X0,addition(X1,X2)),
inference(cnf_transformation,[],[f10]) ).
tcf(c_90,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] : addition(multiplication(X0,X1),multiplication(X2,X1)) = multiplication(addition(X0,X2),X1),
inference(cnf_transformation,[],[f11]) ).
tcf(c_91,negated_conjecture,
! [X0: $i] : multiplication(X0,zero) = zero,
inference(cnf_transformation,[],[f13]) ).
tcf(c_92,negated_conjecture,
! [X0: $i] : multiplication(zero,X0) = zero,
inference(cnf_transformation,[],[f15]) ).
tcf(c_95,negated_conjecture,
! [X0: $i] : multiplication(antidomain(X0),X0) = zero,
inference(cnf_transformation,[],[f20]) ).
tcf(c_96,negated_conjecture,
! [X0: $i,X1: $i] : addition(antidomain(multiplication(X0,X1)),antidomain(multiplication(X0,antidomain(antidomain(X1))))) = antidomain(multiplication(X0,antidomain(antidomain(X1)))),
inference(cnf_transformation,[],[f22]) ).
tcf(c_97,negated_conjecture,
! [X0: $i] : addition(antidomain(antidomain(X0)),antidomain(X0)) = one,
inference(cnf_transformation,[],[f24]) ).
tcf(c_98,negated_conjecture,
! [X0: $i] : multiplication(X0,coantidomain(X0)) = zero,
inference(cnf_transformation,[],[f28]) ).
tcf(c_99,negated_conjecture,
! [X0: $i,X1: $i] : addition(coantidomain(multiplication(X0,X1)),coantidomain(multiplication(coantidomain(coantidomain(X0)),X1))) = coantidomain(multiplication(coantidomain(coantidomain(X0)),X1)),
inference(cnf_transformation,[],[f30]) ).
tcf(c_100,negated_conjecture,
! [X0: $i] : addition(coantidomain(coantidomain(X0)),coantidomain(X0)) = one,
inference(cnf_transformation,[],[f32]) ).
tcf(c_101,negated_conjecture,
addition(antidomain(antidomain(sK2_goals_X1)),antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK3_goals_X0,antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sK1_goals_X2)))))))))))))) = antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK3_goals_X0,antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sK1_goals_X2))))))))))))),
inference(cnf_transformation,[],[f51]) ).
tcf(c_102,negated_conjecture,
addition(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(sK2_goals_X1)))),sK3_goals_X0))),antidomain(antidomain(sK1_goals_X2))) != antidomain(antidomain(sK1_goals_X2)),
inference(cnf_transformation,[],[f52]) ).
tcf(c_122,negated_conjecture,
! [X0: $i] : addition(antidomain(X0),antidomain(antidomain(X0))) = one,
inference(theory_normalisation,[status(thm)],[c_97,c_83,c_82]) ).
tcf(c_123,negated_conjecture,
! [X0: $i] : addition(coantidomain(X0),coantidomain(coantidomain(X0))) = one,
inference(theory_normalisation,[status(thm)],[c_100,c_83,c_82]) ).
tcf(c_124,negated_conjecture,
addition(antidomain(antidomain(sK1_goals_X2)),coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(sK2_goals_X1)))),sK3_goals_X0)))) != antidomain(antidomain(sK1_goals_X2)),
inference(theory_normalisation,[status(thm)],[c_102,c_83,c_82]) ).
tcf(c_181,definition,
iPr_def_10 = antidomain(sK1_goals_X2),
introduced(definition,[new_symbols(definition,[iPr_def_10])],[]) ).
tcf(c_182,definition,
iPr_def_11 = antidomain(iPr_def_10),
introduced(definition,[new_symbols(definition,[iPr_def_11])],[]) ).
tcf(c_183,definition,
iPr_def_12 = antidomain(sK2_goals_X1),
introduced(definition,[new_symbols(definition,[iPr_def_12])],[]) ).
tcf(c_184,definition,
iPr_def_13 = antidomain(iPr_def_12),
introduced(definition,[new_symbols(definition,[iPr_def_13])],[]) ).
tcf(c_185,definition,
iPr_def_14 = coantidomain(iPr_def_13),
introduced(definition,[new_symbols(definition,[iPr_def_14])],[]) ).
tcf(c_186,definition,
iPr_def_15 = coantidomain(iPr_def_14),
introduced(definition,[new_symbols(definition,[iPr_def_15])],[]) ).
tcf(c_187,definition,
iPr_def_16 = multiplication(iPr_def_15,sK3_goals_X0),
introduced(definition,[new_symbols(definition,[iPr_def_16])],[]) ).
tcf(c_188,definition,
iPr_def_17 = coantidomain(iPr_def_16),
introduced(definition,[new_symbols(definition,[iPr_def_17])],[]) ).
tcf(c_189,definition,
iPr_def_18 = coantidomain(iPr_def_17),
introduced(definition,[new_symbols(definition,[iPr_def_18])],[]) ).
tcf(c_190,definition,
iPr_def_19 = addition(iPr_def_11,iPr_def_18),
introduced(definition,[new_symbols(definition,[iPr_def_19])],[]) ).
tcf(c_191,definition,
iPr_def_20 = antidomain(iPr_def_11),
introduced(definition,[new_symbols(definition,[iPr_def_20])],[]) ).
tcf(c_192,definition,
iPr_def_21 = antidomain(iPr_def_20),
introduced(definition,[new_symbols(definition,[iPr_def_21])],[]) ).
tcf(c_193,definition,
iPr_def_22 = antidomain(iPr_def_21),
introduced(definition,[new_symbols(definition,[iPr_def_22])],[]) ).
tcf(c_194,definition,
iPr_def_23 = antidomain(iPr_def_22),
introduced(definition,[new_symbols(definition,[iPr_def_23])],[]) ).
tcf(c_195,definition,
iPr_def_24 = antidomain(iPr_def_23),
introduced(definition,[new_symbols(definition,[iPr_def_24])],[]) ).
tcf(c_196,definition,
iPr_def_25 = multiplication(sK3_goals_X0,iPr_def_24),
introduced(definition,[new_symbols(definition,[iPr_def_25])],[]) ).
tcf(c_197,definition,
iPr_def_26 = antidomain(iPr_def_25),
introduced(definition,[new_symbols(definition,[iPr_def_26])],[]) ).
tcf(c_198,definition,
iPr_def_27 = antidomain(iPr_def_26),
introduced(definition,[new_symbols(definition,[iPr_def_27])],[]) ).
tcf(c_199,definition,
iPr_def_28 = antidomain(iPr_def_27),
introduced(definition,[new_symbols(definition,[iPr_def_28])],[]) ).
tcf(c_200,definition,
iPr_def_29 = antidomain(iPr_def_28),
introduced(definition,[new_symbols(definition,[iPr_def_29])],[]) ).
tcf(c_201,definition,
iPr_def_30 = antidomain(iPr_def_29),
introduced(definition,[new_symbols(definition,[iPr_def_30])],[]) ).
tcf(c_202,definition,
iPr_def_31 = addition(iPr_def_13,iPr_def_30),
introduced(definition,[new_symbols(definition,[iPr_def_31])],[]) ).
tcf(c_203,negated_conjecture,
iPr_def_19 != iPr_def_11,
inference(demodulation,[status(thm)],[c_124,c_183,c_184,c_185,c_186,c_187,c_188,c_189,c_181,c_182,c_190]) ).
tcf(c_204,negated_conjecture,
! [X0: $i] : addition(coantidomain(X0),coantidomain(coantidomain(X0))) = one,
inference(demodulation,[status(thm)],[c_123]) ).
tcf(c_205,negated_conjecture,
! [X0: $i] : addition(antidomain(X0),antidomain(antidomain(X0))) = one,
inference(demodulation,[status(thm)],[c_122]) ).
tcf(c_206,negated_conjecture,
iPr_def_31 = iPr_def_30,
inference(demodulation,[status(thm)],[c_101,c_191,c_192,c_193,c_194,c_195,c_196,c_197,c_198,c_199,c_200,c_201,c_202]) ).
tcf(c_207,negated_conjecture,
! [X0: $i,X1: $i] : addition(coantidomain(multiplication(X0,X1)),coantidomain(multiplication(coantidomain(coantidomain(X0)),X1))) = coantidomain(multiplication(coantidomain(coantidomain(X0)),X1)),
inference(demodulation,[status(thm)],[c_99]) ).
tcf(c_208,negated_conjecture,
! [X0: $i] : multiplication(X0,coantidomain(X0)) = zero,
inference(demodulation,[status(thm)],[c_98]) ).
tcf(c_209,negated_conjecture,
! [X0: $i,X1: $i] : addition(antidomain(multiplication(X0,X1)),antidomain(multiplication(X0,antidomain(antidomain(X1))))) = antidomain(multiplication(X0,antidomain(antidomain(X1)))),
inference(demodulation,[status(thm)],[c_96]) ).
tcf(c_210,negated_conjecture,
! [X0: $i] : multiplication(antidomain(X0),X0) = zero,
inference(demodulation,[status(thm)],[c_95]) ).
tcf(c_213,negated_conjecture,
! [X0: $i] : multiplication(zero,X0) = zero,
inference(demodulation,[status(thm)],[c_92]) ).
tcf(c_214,negated_conjecture,
! [X0: $i] : multiplication(X0,zero) = zero,
inference(demodulation,[status(thm)],[c_91]) ).
tcf(c_215,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] : addition(multiplication(X0,X1),multiplication(X2,X1)) = multiplication(addition(X0,X2),X1),
inference(demodulation,[status(thm)],[c_90]) ).
tcf(c_216,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] : addition(multiplication(X0,X1),multiplication(X0,X2)) = multiplication(X0,addition(X1,X2)),
inference(demodulation,[status(thm)],[c_89]) ).
tcf(c_217,negated_conjecture,
! [X0: $i] : multiplication(one,X0) = X0,
inference(demodulation,[status(thm)],[c_88]) ).
tcf(c_218,negated_conjecture,
! [X0: $i] : multiplication(X0,one) = X0,
inference(demodulation,[status(thm)],[c_87]) ).
tcf(c_219,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] : multiplication(multiplication(X0,X1),X2) = multiplication(X0,multiplication(X1,X2)),
inference(demodulation,[status(thm)],[c_86]) ).
tcf(c_220,negated_conjecture,
! [X0: $i] : addition(X0,X0) = X0,
inference(demodulation,[status(thm)],[c_85]) ).
tcf(c_221,negated_conjecture,
! [X0: $i] : addition(X0,zero) = X0,
inference(demodulation,[status(thm)],[c_84]) ).
tcf(c_222,negated_conjecture,
! [X0: $i,X1: $i,X2: $i] : addition(addition(X0,X1),X2) = addition(X0,addition(X1,X2)),
inference(demodulation,[status(thm)],[c_83]) ).
tcf(c_223,negated_conjecture,
! [X0: $i,X1: $i] : addition(X0,X1) = addition(X1,X0),
inference(demodulation,[status(thm)],[c_82]) ).
tcf(c_378,plain,
addition(iPr_def_13,iPr_def_30) = iPr_def_30,
inference(light_normalisation,[status(thm)],[c_202,c_206]) ).
tcf(c_384,plain,
coantidomain(one) = zero,
inference(superposition,[status(thm)],[c_208,c_217]) ).
tcf(c_412,plain,
multiplication(iPr_def_11,iPr_def_10) = zero,
inference(superposition,[status(thm)],[c_182,c_210]) ).
tcf(c_414,plain,
multiplication(iPr_def_20,iPr_def_11) = zero,
inference(superposition,[status(thm)],[c_191,c_210]) ).
tcf(c_415,plain,
multiplication(iPr_def_21,iPr_def_20) = zero,
inference(superposition,[status(thm)],[c_192,c_210]) ).
tcf(c_416,plain,
multiplication(iPr_def_22,iPr_def_21) = zero,
inference(superposition,[status(thm)],[c_193,c_210]) ).
tcf(c_417,plain,
multiplication(iPr_def_23,iPr_def_22) = zero,
inference(superposition,[status(thm)],[c_194,c_210]) ).
tcf(c_418,plain,
multiplication(iPr_def_24,iPr_def_23) = zero,
inference(superposition,[status(thm)],[c_195,c_210]) ).
tcf(c_419,plain,
multiplication(iPr_def_26,iPr_def_25) = zero,
inference(superposition,[status(thm)],[c_197,c_210]) ).
tcf(c_421,plain,
multiplication(iPr_def_28,iPr_def_27) = zero,
inference(superposition,[status(thm)],[c_199,c_210]) ).
tcf(c_423,plain,
multiplication(iPr_def_30,iPr_def_29) = zero,
inference(superposition,[status(thm)],[c_201,c_210]) ).
tcf(c_425,plain,
! [X0: $i] : addition(zero,X0) = X0,
inference(superposition,[status(thm)],[c_221,c_223]) ).
tcf(c_496,plain,
addition(iPr_def_18,coantidomain(iPr_def_18)) = one,
inference(superposition,[status(thm)],[c_189,c_204]) ).
tcf(c_497,plain,
addition(zero,coantidomain(zero)) = one,
inference(superposition,[status(thm)],[c_384,c_204]) ).
tcf(c_515,plain,
addition(iPr_def_10,antidomain(iPr_def_10)) = one,
inference(superposition,[status(thm)],[c_181,c_205]) ).
tcf(c_517,plain,
addition(iPr_def_11,antidomain(iPr_def_11)) = one,
inference(superposition,[status(thm)],[c_182,c_205]) ).
tcf(c_519,plain,
addition(iPr_def_20,antidomain(iPr_def_20)) = one,
inference(superposition,[status(thm)],[c_191,c_205]) ).
tcf(c_520,plain,
addition(iPr_def_21,antidomain(iPr_def_21)) = one,
inference(superposition,[status(thm)],[c_192,c_205]) ).
tcf(c_521,plain,
addition(iPr_def_22,antidomain(iPr_def_22)) = one,
inference(superposition,[status(thm)],[c_193,c_205]) ).
tcf(c_522,plain,
addition(iPr_def_23,antidomain(iPr_def_23)) = one,
inference(superposition,[status(thm)],[c_194,c_205]) ).
tcf(c_524,plain,
addition(iPr_def_26,antidomain(iPr_def_26)) = one,
inference(superposition,[status(thm)],[c_197,c_205]) ).
tcf(c_526,plain,
addition(iPr_def_28,antidomain(iPr_def_28)) = one,
inference(superposition,[status(thm)],[c_199,c_205]) ).
tcf(c_531,plain,
addition(iPr_def_28,iPr_def_29) = one,
inference(demodulation,[status(thm)],[c_526,c_200]) ).
tcf(c_533,plain,
addition(iPr_def_26,iPr_def_27) = one,
inference(demodulation,[status(thm)],[c_524,c_198]) ).
tcf(c_534,plain,
addition(iPr_def_23,iPr_def_24) = one,
inference(demodulation,[status(thm)],[c_522,c_195]) ).
tcf(c_535,plain,
addition(iPr_def_22,iPr_def_23) = one,
inference(demodulation,[status(thm)],[c_521,c_194]) ).
tcf(c_536,plain,
addition(iPr_def_21,iPr_def_22) = one,
inference(demodulation,[status(thm)],[c_520,c_193]) ).
tcf(c_537,plain,
addition(iPr_def_20,iPr_def_21) = one,
inference(demodulation,[status(thm)],[c_519,c_192]) ).
tcf(c_538,plain,
addition(iPr_def_11,iPr_def_20) = one,
inference(demodulation,[status(thm)],[c_517,c_191]) ).
tcf(c_540,plain,
addition(iPr_def_10,iPr_def_11) = one,
inference(demodulation,[status(thm)],[c_515,c_182]) ).
tcf(c_593,plain,
! [X0: $i] : multiplication(iPr_def_15,multiplication(sK3_goals_X0,X0)) = multiplication(iPr_def_16,X0),
inference(superposition,[status(thm)],[c_187,c_219]) ).
tcf(c_594,plain,
! [X0: $i] : multiplication(sK3_goals_X0,multiplication(iPr_def_24,X0)) = multiplication(iPr_def_25,X0),
inference(superposition,[status(thm)],[c_196,c_219]) ).
tcf(c_607,plain,
! [X0: $i] : multiplication(iPr_def_24,multiplication(iPr_def_23,X0)) = multiplication(zero,X0),
inference(superposition,[status(thm)],[c_418,c_219]) ).
tcf(c_619,plain,
! [X0: $i] : multiplication(iPr_def_24,multiplication(iPr_def_23,X0)) = zero,
inference(demodulation,[status(thm)],[c_607,c_213]) ).
tcf(c_729,plain,
! [X0: $i,X1: $i] : addition(X0,addition(X0,X1)) = addition(X0,X1),
inference(superposition,[status(thm)],[c_220,c_222]) ).
tcf(c_732,plain,
! [X0: $i] : addition(iPr_def_11,addition(iPr_def_18,X0)) = addition(iPr_def_19,X0),
inference(superposition,[status(thm)],[c_190,c_222]) ).
tcf(c_756,plain,
! [X0: $i] : addition(zero,multiplication(X0,iPr_def_10)) = multiplication(addition(iPr_def_11,X0),iPr_def_10),
inference(superposition,[status(thm)],[c_412,c_215]) ).
tcf(c_758,plain,
! [X0: $i] : addition(zero,multiplication(X0,iPr_def_11)) = multiplication(addition(iPr_def_20,X0),iPr_def_11),
inference(superposition,[status(thm)],[c_414,c_215]) ).
tcf(c_759,plain,
! [X0: $i] : addition(zero,multiplication(X0,iPr_def_20)) = multiplication(addition(iPr_def_21,X0),iPr_def_20),
inference(superposition,[status(thm)],[c_415,c_215]) ).
tcf(c_760,plain,
! [X0: $i] : addition(zero,multiplication(X0,iPr_def_21)) = multiplication(addition(iPr_def_22,X0),iPr_def_21),
inference(superposition,[status(thm)],[c_416,c_215]) ).
tcf(c_761,plain,
! [X0: $i] : addition(zero,multiplication(X0,iPr_def_22)) = multiplication(addition(iPr_def_23,X0),iPr_def_22),
inference(superposition,[status(thm)],[c_417,c_215]) ).
tcf(c_763,plain,
! [X0: $i] : addition(zero,multiplication(X0,iPr_def_25)) = multiplication(addition(iPr_def_26,X0),iPr_def_25),
inference(superposition,[status(thm)],[c_419,c_215]) ).
tcf(c_765,plain,
! [X0: $i] : addition(zero,multiplication(X0,iPr_def_27)) = multiplication(addition(iPr_def_28,X0),iPr_def_27),
inference(superposition,[status(thm)],[c_421,c_215]) ).
tcf(c_771,plain,
! [X0: $i,X1: $i] : addition(multiplication(X0,X1),zero) = multiplication(addition(X0,zero),X1),
inference(superposition,[status(thm)],[c_213,c_215]) ).
tcf(c_818,plain,
! [X0: $i,X1: $i] : addition(zero,multiplication(X0,X1)) = multiplication(addition(X0,zero),X1),
inference(theory_normalisation,[status(thm)],[c_771,c_222,c_223]) ).
tcf(c_819,plain,
! [X0: $i,X1: $i] : addition(zero,multiplication(X0,X1)) = multiplication(X0,X1),
inference(demodulation,[status(thm)],[c_818,c_221]) ).
tcf(c_824,plain,
! [X0: $i] : multiplication(addition(iPr_def_28,X0),iPr_def_27) = multiplication(X0,iPr_def_27),
inference(demodulation,[status(thm)],[c_765,c_819]) ).
tcf(c_826,plain,
! [X0: $i] : multiplication(addition(iPr_def_26,X0),iPr_def_25) = multiplication(X0,iPr_def_25),
inference(demodulation,[status(thm)],[c_763,c_819]) ).
tcf(c_828,plain,
! [X0: $i] : multiplication(addition(iPr_def_23,X0),iPr_def_22) = multiplication(X0,iPr_def_22),
inference(demodulation,[status(thm)],[c_761,c_819]) ).
tcf(c_829,plain,
! [X0: $i] : multiplication(addition(iPr_def_22,X0),iPr_def_21) = multiplication(X0,iPr_def_21),
inference(demodulation,[status(thm)],[c_760,c_819]) ).
tcf(c_830,plain,
! [X0: $i] : multiplication(addition(iPr_def_21,X0),iPr_def_20) = multiplication(X0,iPr_def_20),
inference(demodulation,[status(thm)],[c_759,c_819]) ).
tcf(c_831,plain,
! [X0: $i] : multiplication(addition(iPr_def_20,X0),iPr_def_11) = multiplication(X0,iPr_def_11),
inference(demodulation,[status(thm)],[c_758,c_819]) ).
tcf(c_833,plain,
! [X0: $i] : multiplication(addition(iPr_def_11,X0),iPr_def_10) = multiplication(X0,iPr_def_10),
inference(demodulation,[status(thm)],[c_756,c_819]) ).
tcf(c_1260,plain,
! [X0: $i] : multiplication(iPr_def_30,multiplication(iPr_def_29,X0)) = multiplication(zero,X0),
inference(superposition,[status(thm)],[c_423,c_219]) ).
tcf(c_1263,plain,
! [X0: $i] : multiplication(iPr_def_30,multiplication(iPr_def_29,X0)) = zero,
inference(demodulation,[status(thm)],[c_1260,c_213]) ).
tcf(c_1688,plain,
! [X0: $i] : addition(iPr_def_10,addition(iPr_def_11,X0)) = addition(one,X0),
inference(superposition,[status(thm)],[c_540,c_222]) ).
tcf(c_1709,plain,
coantidomain(zero) = one,
inference(superposition,[status(thm)],[c_497,c_425]) ).
tcf(c_3246,plain,
multiplication(sK3_goals_X0,zero) = multiplication(iPr_def_25,iPr_def_23),
inference(superposition,[status(thm)],[c_418,c_594]) ).
tcf(c_3258,plain,
multiplication(iPr_def_25,iPr_def_23) = zero,
inference(demodulation,[status(thm)],[c_3246,c_214]) ).
tcf(c_3577,plain,
! [X0: $i] : addition(multiplication(iPr_def_25,X0),zero) = multiplication(iPr_def_25,addition(X0,iPr_def_23)),
inference(superposition,[status(thm)],[c_3258,c_216]) ).
tcf(c_3584,plain,
! [X0: $i] : addition(zero,multiplication(iPr_def_25,X0)) = multiplication(iPr_def_25,addition(X0,iPr_def_23)),
inference(theory_normalisation,[status(thm)],[c_3577,c_222,c_223]) ).
tcf(c_3585,plain,
! [X0: $i] : multiplication(iPr_def_25,addition(X0,iPr_def_23)) = multiplication(iPr_def_25,X0),
inference(demodulation,[status(thm)],[c_3584,c_425]) ).
tcf(c_3920,plain,
! [X0: $i] : addition(coantidomain(X0),one) = one,
inference(superposition,[status(thm)],[c_204,c_729]) ).
tcf(c_3921,plain,
addition(iPr_def_11,iPr_def_19) = iPr_def_19,
inference(superposition,[status(thm)],[c_190,c_729]) ).
tcf(c_3923,plain,
addition(iPr_def_18,one) = one,
inference(superposition,[status(thm)],[c_496,c_729]) ).
tcf(c_3935,plain,
addition(iPr_def_21,one) = one,
inference(superposition,[status(thm)],[c_536,c_729]) ).
tcf(c_3937,plain,
addition(iPr_def_11,one) = one,
inference(superposition,[status(thm)],[c_538,c_729]) ).
tcf(c_3945,plain,
! [X0: $i] : addition(one,coantidomain(X0)) = one,
inference(theory_normalisation,[status(thm)],[c_3920,c_222,c_223]) ).
tcf(c_4699,plain,
addition(iPr_def_11,one) = addition(iPr_def_19,one),
inference(superposition,[status(thm)],[c_3923,c_732]) ).
tcf(c_4706,plain,
addition(iPr_def_19,one) = one,
inference(demodulation,[status(thm)],[c_4699,c_3937]) ).
tcf(c_5010,plain,
multiplication(one,iPr_def_27) = multiplication(iPr_def_29,iPr_def_27),
inference(superposition,[status(thm)],[c_531,c_824]) ).
tcf(c_5020,plain,
multiplication(iPr_def_29,iPr_def_27) = iPr_def_27,
inference(demodulation,[status(thm)],[c_5010,c_217]) ).
tcf(c_5215,plain,
multiplication(iPr_def_30,iPr_def_27) = zero,
inference(superposition,[status(thm)],[c_5020,c_1263]) ).
tcf(c_5309,plain,
! [X0: $i] : addition(multiplication(X0,iPr_def_27),zero) = multiplication(addition(X0,iPr_def_30),iPr_def_27),
inference(superposition,[status(thm)],[c_5215,c_215]) ).
tcf(c_5311,plain,
! [X0: $i] : addition(zero,multiplication(X0,iPr_def_27)) = multiplication(addition(X0,iPr_def_30),iPr_def_27),
inference(theory_normalisation,[status(thm)],[c_5309,c_222,c_223]) ).
tcf(c_5312,plain,
! [X0: $i] : multiplication(addition(X0,iPr_def_30),iPr_def_27) = multiplication(X0,iPr_def_27),
inference(demodulation,[status(thm)],[c_5311,c_425]) ).
tcf(c_5574,plain,
multiplication(one,iPr_def_25) = multiplication(iPr_def_27,iPr_def_25),
inference(superposition,[status(thm)],[c_533,c_826]) ).
tcf(c_5584,plain,
multiplication(iPr_def_27,iPr_def_25) = iPr_def_25,
inference(demodulation,[status(thm)],[c_5574,c_217]) ).
tcf(c_6032,plain,
multiplication(one,iPr_def_22) = multiplication(iPr_def_24,iPr_def_22),
inference(superposition,[status(thm)],[c_534,c_828]) ).
tcf(c_6042,plain,
multiplication(iPr_def_24,iPr_def_22) = iPr_def_22,
inference(demodulation,[status(thm)],[c_6032,c_217]) ).
tcf(c_6066,plain,
multiplication(one,iPr_def_21) = multiplication(iPr_def_23,iPr_def_21),
inference(superposition,[status(thm)],[c_535,c_829]) ).
tcf(c_6076,plain,
multiplication(iPr_def_23,iPr_def_21) = iPr_def_21,
inference(demodulation,[status(thm)],[c_6066,c_217]) ).
tcf(c_6105,plain,
! [X0: $i] : multiplication(addition(X0,iPr_def_21),iPr_def_20) = multiplication(X0,iPr_def_20),
inference(superposition,[status(thm)],[c_223,c_830]) ).
tcf(c_6108,plain,
multiplication(one,iPr_def_20) = multiplication(iPr_def_22,iPr_def_20),
inference(superposition,[status(thm)],[c_536,c_830]) ).
tcf(c_6118,plain,
multiplication(iPr_def_22,iPr_def_20) = iPr_def_20,
inference(demodulation,[status(thm)],[c_6108,c_217]) ).
tcf(c_6172,plain,
! [X0: $i] : multiplication(iPr_def_24,multiplication(iPr_def_22,X0)) = multiplication(iPr_def_22,X0),
inference(superposition,[status(thm)],[c_6042,c_219]) ).
tcf(c_6175,plain,
multiplication(sK3_goals_X0,iPr_def_22) = multiplication(iPr_def_25,iPr_def_22),
inference(superposition,[status(thm)],[c_6042,c_594]) ).
tcf(c_6233,plain,
multiplication(iPr_def_24,iPr_def_21) = zero,
inference(superposition,[status(thm)],[c_6076,c_619]) ).
tcf(c_6248,plain,
! [X0: $i] : multiplication(iPr_def_22,multiplication(iPr_def_20,X0)) = multiplication(iPr_def_20,X0),
inference(superposition,[status(thm)],[c_6118,c_219]) ).
tcf(c_6309,plain,
! [X0: $i] : addition(multiplication(iPr_def_24,X0),zero) = multiplication(iPr_def_24,addition(X0,iPr_def_21)),
inference(superposition,[status(thm)],[c_6233,c_216]) ).
tcf(c_6315,plain,
! [X0: $i] : addition(zero,multiplication(iPr_def_24,X0)) = multiplication(iPr_def_24,addition(X0,iPr_def_21)),
inference(theory_normalisation,[status(thm)],[c_6309,c_222,c_223]) ).
tcf(c_6316,plain,
! [X0: $i] : multiplication(iPr_def_24,addition(X0,iPr_def_21)) = multiplication(iPr_def_24,X0),
inference(demodulation,[status(thm)],[c_6315,c_425]) ).
tcf(c_7472,plain,
multiplication(iPr_def_18,iPr_def_10) = multiplication(iPr_def_19,iPr_def_10),
inference(superposition,[status(thm)],[c_190,c_833]) ).
tcf(c_7473,plain,
multiplication(one,iPr_def_10) = multiplication(iPr_def_20,iPr_def_10),
inference(superposition,[status(thm)],[c_538,c_833]) ).
tcf(c_7484,plain,
multiplication(iPr_def_20,iPr_def_10) = iPr_def_10,
inference(demodulation,[status(thm)],[c_7473,c_217]) ).
tcf(c_13511,plain,
addition(one,iPr_def_19) = addition(iPr_def_10,iPr_def_19),
inference(superposition,[status(thm)],[c_3921,c_1688]) ).
tcf(c_13520,plain,
addition(iPr_def_10,iPr_def_19) = addition(iPr_def_19,one),
inference(theory_normalisation,[status(thm)],[c_13511,c_222,c_223]) ).
tcf(c_13521,plain,
addition(iPr_def_10,iPr_def_19) = one,
inference(demodulation,[status(thm)],[c_13520,c_4706]) ).
tcf(c_14491,plain,
multiplication(iPr_def_25,one) = multiplication(iPr_def_25,iPr_def_22),
inference(superposition,[status(thm)],[c_535,c_3585]) ).
tcf(c_14504,plain,
multiplication(iPr_def_25,iPr_def_22) = iPr_def_25,
inference(demodulation,[status(thm)],[c_14491,c_218]) ).
tcf(c_14513,plain,
multiplication(sK3_goals_X0,iPr_def_22) = iPr_def_25,
inference(demodulation,[status(thm)],[c_6175,c_14504]) ).
tcf(c_15138,plain,
multiplication(iPr_def_15,iPr_def_25) = multiplication(iPr_def_16,iPr_def_22),
inference(superposition,[status(thm)],[c_14513,c_593]) ).
tcf(c_18041,plain,
multiplication(iPr_def_13,iPr_def_27) = multiplication(iPr_def_30,iPr_def_27),
inference(superposition,[status(thm)],[c_378,c_5312]) ).
tcf(c_18055,plain,
multiplication(iPr_def_13,iPr_def_27) = zero,
inference(demodulation,[status(thm)],[c_18041,c_5215]) ).
tcf(c_18887,plain,
! [X0: $i] : multiplication(iPr_def_13,multiplication(iPr_def_27,X0)) = multiplication(zero,X0),
inference(superposition,[status(thm)],[c_18055,c_219]) ).
tcf(c_18890,plain,
! [X0: $i] : multiplication(iPr_def_13,multiplication(iPr_def_27,X0)) = zero,
inference(demodulation,[status(thm)],[c_18887,c_213]) ).
tcf(c_19118,plain,
multiplication(iPr_def_13,iPr_def_25) = zero,
inference(superposition,[status(thm)],[c_5584,c_18890]) ).
tcf(c_19668,plain,
addition(coantidomain(zero),coantidomain(multiplication(coantidomain(coantidomain(iPr_def_13)),iPr_def_25))) = coantidomain(multiplication(coantidomain(coantidomain(iPr_def_13)),iPr_def_25)),
inference(superposition,[status(thm)],[c_19118,c_207]) ).
tcf(c_19681,plain,
coantidomain(multiplication(iPr_def_15,iPr_def_25)) = one,
inference(demodulation,[status(thm)],[c_19668,c_185,c_186,c_1709,c_3945]) ).
tcf(c_19840,plain,
multiplication(multiplication(iPr_def_15,iPr_def_25),one) = zero,
inference(superposition,[status(thm)],[c_19681,c_208]) ).
tcf(c_19842,plain,
multiplication(iPr_def_15,iPr_def_25) = zero,
inference(demodulation,[status(thm)],[c_19840,c_219,c_218]) ).
tcf(c_19847,plain,
multiplication(iPr_def_16,iPr_def_22) = zero,
inference(demodulation,[status(thm)],[c_15138,c_19842]) ).
tcf(c_20081,plain,
addition(coantidomain(zero),coantidomain(multiplication(coantidomain(coantidomain(iPr_def_16)),iPr_def_22))) = coantidomain(multiplication(coantidomain(coantidomain(iPr_def_16)),iPr_def_22)),
inference(superposition,[status(thm)],[c_19847,c_207]) ).
tcf(c_20096,plain,
coantidomain(multiplication(iPr_def_18,iPr_def_22)) = one,
inference(demodulation,[status(thm)],[c_20081,c_188,c_189,c_1709,c_3945]) ).
tcf(c_20184,plain,
multiplication(multiplication(iPr_def_18,iPr_def_22),one) = zero,
inference(superposition,[status(thm)],[c_20096,c_208]) ).
tcf(c_20186,plain,
multiplication(iPr_def_18,iPr_def_22) = zero,
inference(demodulation,[status(thm)],[c_20184,c_219,c_218]) ).
tcf(c_20226,plain,
! [X0: $i] : multiplication(iPr_def_18,multiplication(iPr_def_22,X0)) = multiplication(zero,X0),
inference(superposition,[status(thm)],[c_20186,c_219]) ).
tcf(c_20231,plain,
! [X0: $i] : multiplication(iPr_def_18,multiplication(iPr_def_22,X0)) = zero,
inference(demodulation,[status(thm)],[c_20226,c_213]) ).
tcf(c_20551,plain,
multiplication(iPr_def_18,iPr_def_20) = zero,
inference(superposition,[status(thm)],[c_6118,c_20231]) ).
tcf(c_20671,plain,
! [X0: $i] : multiplication(iPr_def_18,multiplication(iPr_def_20,X0)) = multiplication(zero,X0),
inference(superposition,[status(thm)],[c_20551,c_219]) ).
tcf(c_20676,plain,
! [X0: $i] : multiplication(iPr_def_18,multiplication(iPr_def_20,X0)) = zero,
inference(demodulation,[status(thm)],[c_20671,c_213]) ).
tcf(c_20915,plain,
multiplication(iPr_def_18,iPr_def_10) = zero,
inference(superposition,[status(thm)],[c_7484,c_20676]) ).
tcf(c_20936,plain,
multiplication(iPr_def_19,iPr_def_10) = zero,
inference(demodulation,[status(thm)],[c_7472,c_20915]) ).
tcf(c_21183,plain,
! [X0: $i] : addition(zero,multiplication(iPr_def_19,X0)) = multiplication(iPr_def_19,addition(iPr_def_10,X0)),
inference(superposition,[status(thm)],[c_20936,c_216]) ).
tcf(c_21194,plain,
! [X0: $i] : multiplication(iPr_def_19,addition(iPr_def_10,X0)) = multiplication(iPr_def_19,X0),
inference(demodulation,[status(thm)],[c_21183,c_425]) ).
tcf(c_23704,plain,
multiplication(iPr_def_22,iPr_def_10) = iPr_def_10,
inference(superposition,[status(thm)],[c_7484,c_6248]) ).
tcf(c_24079,plain,
addition(antidomain(iPr_def_10),antidomain(multiplication(iPr_def_22,antidomain(antidomain(iPr_def_10))))) = antidomain(multiplication(iPr_def_22,antidomain(antidomain(iPr_def_10)))),
inference(superposition,[status(thm)],[c_23704,c_209]) ).
tcf(c_24086,plain,
multiplication(iPr_def_24,iPr_def_10) = iPr_def_10,
inference(superposition,[status(thm)],[c_23704,c_6172]) ).
tcf(c_24094,plain,
addition(iPr_def_11,iPr_def_21) = iPr_def_21,
inference(demodulation,[status(thm)],[c_24079,c_182,c_191,c_192,c_6118]) ).
tcf(c_24629,plain,
addition(one,iPr_def_21) = addition(iPr_def_10,iPr_def_21),
inference(superposition,[status(thm)],[c_24094,c_1688]) ).
tcf(c_24633,plain,
addition(iPr_def_10,iPr_def_21) = addition(iPr_def_21,one),
inference(theory_normalisation,[status(thm)],[c_24629,c_222,c_223]) ).
tcf(c_24634,plain,
addition(iPr_def_10,iPr_def_21) = one,
inference(demodulation,[status(thm)],[c_24633,c_3935]) ).
tcf(c_24676,plain,
multiplication(one,iPr_def_20) = multiplication(iPr_def_10,iPr_def_20),
inference(superposition,[status(thm)],[c_24634,c_6105]) ).
tcf(c_24677,plain,
multiplication(iPr_def_10,iPr_def_20) = iPr_def_20,
inference(demodulation,[status(thm)],[c_24676,c_217]) ).
tcf(c_24779,plain,
multiplication(iPr_def_24,one) = multiplication(iPr_def_24,iPr_def_20),
inference(superposition,[status(thm)],[c_537,c_6316]) ).
tcf(c_24781,plain,
multiplication(iPr_def_24,one) = multiplication(iPr_def_24,iPr_def_10),
inference(superposition,[status(thm)],[c_24634,c_6316]) ).
tcf(c_24794,plain,
iPr_def_10 = iPr_def_24,
inference(demodulation,[status(thm)],[c_24781,c_218,c_24086]) ).
tcf(c_24796,plain,
multiplication(iPr_def_10,one) = multiplication(iPr_def_10,iPr_def_20),
inference(demodulation,[status(thm)],[c_24779,c_24794]) ).
tcf(c_24797,plain,
multiplication(iPr_def_10,iPr_def_20) = iPr_def_10,
inference(demodulation,[status(thm)],[c_24796,c_218]) ).
tcf(c_25389,plain,
iPr_def_10 = iPr_def_20,
inference(demodulation,[status(thm)],[c_24677,c_24797]) ).
tcf(c_25431,plain,
! [X0: $i] : multiplication(addition(iPr_def_10,X0),iPr_def_11) = multiplication(X0,iPr_def_11),
inference(demodulation,[status(thm)],[c_831,c_25389]) ).
tcf(c_39495,plain,
multiplication(iPr_def_19,one) = multiplication(iPr_def_19,iPr_def_11),
inference(superposition,[status(thm)],[c_540,c_21194]) ).
tcf(c_39511,plain,
multiplication(iPr_def_19,iPr_def_11) = iPr_def_19,
inference(demodulation,[status(thm)],[c_39495,c_218]) ).
tcf(c_40515,plain,
multiplication(one,iPr_def_11) = multiplication(iPr_def_19,iPr_def_11),
inference(superposition,[status(thm)],[c_13521,c_25431]) ).
tcf(c_40527,plain,
iPr_def_11 = iPr_def_19,
inference(demodulation,[status(thm)],[c_40515,c_217,c_39511]) ).
tcf(c_40607,plain,
iPr_def_11 != iPr_def_11,
inference(demodulation,[status(thm)],[c_203,c_40527]) ).
tcf(c_40608,plain,
$false,
inference(equality_resolution_simp,[status(thm)],[c_40607]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : KLE108-10 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.09/0.36 % Computer : n017.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Wed Sep 23 18:53:01 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.36 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.13/0.39 Running UEQ theorem proving
% 0.13/0.39 Running: /export/starexec/sandbox/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s ueq_schedule -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.13/0.41
% 0.13/0.41 % ======== iProver multi-core TPTP/SMT =========
% 0.13/0.41
% 0.13/0.41 % Detected problem language: tptp
% 0.13/0.42 % Proving...
% 87.55/12.35 WARNING - Clausifier option not provided in the heuristic config "heur/vip2_118404", setting default options.
% 87.55/12.35 % SZS status Started for theBenchmark.p
% 87.55/12.35 % SZS status Unsatisfiable for theBenchmark.p
% 87.55/12.35
% 87.55/12.35 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 87.55/12.35
% 87.55/12.35 % ------ iProver source info
% 87.55/12.35
% 87.55/12.35 % git: date: 2026-07-19 20:42:38 +0200
% 87.55/12.35 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 87.55/12.35 % git: non_committed_changes: false
% 87.55/12.35
% 87.55/12.35 % ------ Parsing...% successful
% 87.55/12.35
% 87.55/12.35
% 87.55/12.35 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 87.55/12.35
% 87.55/12.35 % ------ Preprocessing... sup_sim: 0 sf_s rm: 0 0s sf_e pe_s pe_e %
% 87.55/12.35
% 87.55/12.35 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 87.55/12.35
% 87.55/12.35 % ------ Preprocessing... sf_s rm: 0 0s sf_e
% 87.55/12.35 % ------ Proving...
% 87.55/12.35 % ------ Problem Properties
% 87.55/12.35
% 87.55/12.35 %
% 87.55/12.35 % clauses 45
% 87.55/12.35 % conjectures 23
% 87.55/12.35 % EPR 2
% 87.55/12.35 % Horn 45
% 87.55/12.35 % unary 45
% 87.55/12.35 % binary 0
% 87.55/12.35 % lits 45
% 87.55/12.35 % lits eq 45
% 87.55/12.35 % fd_pure 0
% 87.55/12.35 % fd_pseudo 0
% 87.55/12.35 % fd_cond 0
% 87.55/12.35 % fd_pseudo_cond 0
% 87.55/12.35 % AC symbols 1
% 87.55/12.35
% 87.55/12.35 % ------ Input Options Time Limit: Unbounded
% 87.55/12.35
% 87.55/12.35
% 87.55/12.35 % ------
% 87.55/12.35 % Current options:
% 87.55/12.35 % ------
% 87.55/12.35
% 87.55/12.35
% 87.55/12.35 %
% 87.55/12.35
% 87.55/12.35 % ------ Proving...
% 87.55/12.35 %
% 87.55/12.35
% 87.55/12.35 % SZS status Unsatisfiable for theBenchmark.p
% 87.55/12.35
% 87.55/12.35 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 87.55/12.36
% 87.55/12.36
%------------------------------------------------------------------------------