%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : KLE110-10 : TPTP v9.3.1. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% Computer : n005.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:26 PM UTC 2026
% Result : Unsatisfiable 8.61s 4.71s
% Output : CNFRefutation 8.61s
% Verified :
% SZS Type : Refutation
% Derivation depth : 26
% Number of leaves : 41
% Syntax : Number of formulae : 210 ( 210 unt; 19 def)
% Number of atoms : 477 ( 209 equ)
% Maximal formula atoms : 1 ( 2 avg)
% Number of connectives : 6 ( 6 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 2 avg)
% Maximal term depth : 20 ( 2 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 21 ( 19 usr; 20 prp; 0-2 aty)
% Number of functors : 14 ( 14 usr; 4 con; 0-2 aty)
% Number of variables : 157 ( 0 sgn 157 !; 0 ?; 105 :)
% 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(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(f40,axiom,
! [X0,X1] : backward_box(X0,X1) = c(backward_diamond(X0,c(X1))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',backward_box) ).
fof(f41,negated_conjecture,
addition(domain(sK2_goals_X0),backward_box(sK1_goals_X1,forward_diamond(sK1_goals_X1,domain(sK2_goals_X0)))) != backward_box(sK1_goals_X1,forward_diamond(sK1_goals_X1,domain(sK2_goals_X0))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goals) ).
fof(f42,plain,
backward_box(sK1_goals_X1,forward_diamond(sK1_goals_X1,domain(sK2_goals_X0))) != addition(domain(sK2_goals_X0),backward_box(sK1_goals_X1,forward_diamond(sK1_goals_X1,domain(sK2_goals_X0)))),
inference(reorient_equations,[],[f41]) ).
fof(f44,plain,
! [X0,X1] : forward_diamond(X0,X1) = antidomain(antidomain(multiplication(X0,antidomain(antidomain(X1))))),
inference(definition_unfolding,[],[f37,f26,f26]) ).
fof(f45,plain,
! [X0,X1] : backward_diamond(X0,X1) = coantidomain(coantidomain(multiplication(coantidomain(coantidomain(X1)),X0))),
inference(definition_unfolding,[],[f38,f34,f34]) ).
fof(f46,plain,
! [X0] : c(X0) = antidomain(antidomain(antidomain(X0))),
inference(definition_unfolding,[],[f35,f26]) ).
fof(f48,plain,
! [X0,X1] : backward_box(X0,X1) = antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(X1))))),X0)))))),
inference(definition_unfolding,[],[f40,f46,f45,f46]) ).
fof(f49,plain,
antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK1_goals_X1,antidomain(antidomain(antidomain(antidomain(sK2_goals_X0)))))))))))),sK1_goals_X1)))))) != addition(antidomain(antidomain(sK2_goals_X0)),antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK1_goals_X1,antidomain(antidomain(antidomain(antidomain(sK2_goals_X0)))))))))))),sK1_goals_X1))))))),
inference(definition_unfolding,[],[f42,f48,f44,f26,f26,f48,f44,f26]) ).
tcf(c_81,plain,
! [X0: $i,X1: $i] : addition(X0,X1) = addition(X1,X0),
inference(cnf_transformation,[],[f3]) ).
tcf(c_82,plain,
! [X0: $i,X1: $i,X2: $i] : addition(addition(X0,X1),X2) = addition(X0,addition(X1,X2)),
inference(cnf_transformation,[],[f4]) ).
tcf(c_83,plain,
! [X0: $i] : addition(X0,zero) = X0,
inference(cnf_transformation,[],[f5]) ).
tcf(c_84,plain,
! [X0: $i] : addition(X0,X0) = X0,
inference(cnf_transformation,[],[f6]) ).
tcf(c_85,plain,
! [X0: $i,X1: $i,X2: $i] : multiplication(multiplication(X0,X1),X2) = multiplication(X0,multiplication(X1,X2)),
inference(cnf_transformation,[],[f7]) ).
tcf(c_86,plain,
! [X0: $i] : multiplication(X0,one) = X0,
inference(cnf_transformation,[],[f8]) ).
tcf(c_87,plain,
! [X0: $i] : multiplication(one,X0) = X0,
inference(cnf_transformation,[],[f9]) ).
tcf(c_88,plain,
! [X0: $i,X1: $i,X2: $i] : addition(multiplication(X0,X1),multiplication(X0,X2)) = multiplication(X0,addition(X1,X2)),
inference(cnf_transformation,[],[f10]) ).
tcf(c_89,plain,
! [X0: $i,X1: $i,X2: $i] : addition(multiplication(X0,X1),multiplication(X2,X1)) = multiplication(addition(X0,X2),X1),
inference(cnf_transformation,[],[f11]) ).
tcf(c_94,plain,
! [X0: $i] : multiplication(antidomain(X0),X0) = zero,
inference(cnf_transformation,[],[f20]) ).
tcf(c_95,plain,
! [X0: $i,X1: $i] : addition(antidomain(multiplication(X0,X1)),antidomain(multiplication(X0,antidomain(antidomain(X1))))) = antidomain(multiplication(X0,antidomain(antidomain(X1)))),
inference(cnf_transformation,[],[f22]) ).
tcf(c_96,plain,
! [X0: $i] : addition(antidomain(antidomain(X0)),antidomain(X0)) = one,
inference(cnf_transformation,[],[f24]) ).
tcf(c_97,plain,
! [X0: $i] : multiplication(X0,coantidomain(X0)) = zero,
inference(cnf_transformation,[],[f28]) ).
tcf(c_98,plain,
! [X0: $i,X1: $i] : addition(coantidomain(multiplication(X0,X1)),coantidomain(multiplication(coantidomain(coantidomain(X0)),X1))) = coantidomain(multiplication(coantidomain(coantidomain(X0)),X1)),
inference(cnf_transformation,[],[f30]) ).
tcf(c_99,plain,
! [X0: $i] : addition(coantidomain(coantidomain(X0)),coantidomain(X0)) = one,
inference(cnf_transformation,[],[f32]) ).
tcf(c_100,negated_conjecture,
addition(antidomain(antidomain(sK2_goals_X0)),antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK1_goals_X1,antidomain(antidomain(antidomain(antidomain(sK2_goals_X0)))))))))))),sK1_goals_X1))))))) != antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK1_goals_X1,antidomain(antidomain(antidomain(antidomain(sK2_goals_X0)))))))))))),sK1_goals_X1)))))),
inference(cnf_transformation,[],[f49]) ).
tcf(c_120,plain,
! [X0: $i] : addition(antidomain(X0),antidomain(antidomain(X0))) = one,
inference(theory_normalisation,[status(thm)],[c_96,c_82,c_81]) ).
tcf(c_121,plain,
! [X0: $i] : addition(coantidomain(X0),coantidomain(coantidomain(X0))) = one,
inference(theory_normalisation,[status(thm)],[c_99,c_82,c_81]) ).
tcf(c_176,definition,
iPr_def_10 = antidomain(sK2_goals_X0),
introduced(definition,[new_symbols(definition,[iPr_def_10])],[]) ).
tcf(c_177,definition,
iPr_def_11 = antidomain(iPr_def_10),
introduced(definition,[new_symbols(definition,[iPr_def_11])],[]) ).
tcf(c_178,definition,
iPr_def_12 = antidomain(iPr_def_11),
introduced(definition,[new_symbols(definition,[iPr_def_12])],[]) ).
tcf(c_179,definition,
iPr_def_13 = antidomain(iPr_def_12),
introduced(definition,[new_symbols(definition,[iPr_def_13])],[]) ).
tcf(c_180,definition,
iPr_def_14 = multiplication(sK1_goals_X1,iPr_def_13),
introduced(definition,[new_symbols(definition,[iPr_def_14])],[]) ).
tcf(c_181,definition,
iPr_def_15 = antidomain(iPr_def_14),
introduced(definition,[new_symbols(definition,[iPr_def_15])],[]) ).
tcf(c_182,definition,
iPr_def_16 = antidomain(iPr_def_15),
introduced(definition,[new_symbols(definition,[iPr_def_16])],[]) ).
tcf(c_183,definition,
iPr_def_17 = antidomain(iPr_def_16),
introduced(definition,[new_symbols(definition,[iPr_def_17])],[]) ).
tcf(c_184,definition,
iPr_def_18 = antidomain(iPr_def_17),
introduced(definition,[new_symbols(definition,[iPr_def_18])],[]) ).
tcf(c_185,definition,
iPr_def_19 = antidomain(iPr_def_18),
introduced(definition,[new_symbols(definition,[iPr_def_19])],[]) ).
tcf(c_186,definition,
iPr_def_20 = coantidomain(iPr_def_19),
introduced(definition,[new_symbols(definition,[iPr_def_20])],[]) ).
tcf(c_187,definition,
iPr_def_21 = coantidomain(iPr_def_20),
introduced(definition,[new_symbols(definition,[iPr_def_21])],[]) ).
tcf(c_188,definition,
iPr_def_22 = multiplication(iPr_def_21,sK1_goals_X1),
introduced(definition,[new_symbols(definition,[iPr_def_22])],[]) ).
tcf(c_189,definition,
iPr_def_23 = coantidomain(iPr_def_22),
introduced(definition,[new_symbols(definition,[iPr_def_23])],[]) ).
tcf(c_190,definition,
iPr_def_24 = coantidomain(iPr_def_23),
introduced(definition,[new_symbols(definition,[iPr_def_24])],[]) ).
tcf(c_191,definition,
iPr_def_25 = antidomain(iPr_def_24),
introduced(definition,[new_symbols(definition,[iPr_def_25])],[]) ).
tcf(c_192,definition,
iPr_def_26 = antidomain(iPr_def_25),
introduced(definition,[new_symbols(definition,[iPr_def_26])],[]) ).
tcf(c_193,definition,
iPr_def_27 = antidomain(iPr_def_26),
introduced(definition,[new_symbols(definition,[iPr_def_27])],[]) ).
tcf(c_194,definition,
iPr_def_28 = addition(iPr_def_11,iPr_def_27),
introduced(definition,[new_symbols(definition,[iPr_def_28])],[]) ).
tcf(c_195,negated_conjecture,
iPr_def_28 != iPr_def_27,
inference(demodulation,[status(thm)],[c_100,c_178,c_179,c_180,c_181,c_182,c_183,c_184,c_185,c_186,c_187,c_188,c_189,c_190,c_191,c_192,c_193,c_176,c_177,c_194]) ).
tcf(c_196,plain,
! [X0: $i] : addition(coantidomain(X0),coantidomain(coantidomain(X0))) = one,
inference(demodulation,[status(thm)],[c_121]) ).
tcf(c_197,plain,
! [X0: $i] : addition(antidomain(X0),antidomain(antidomain(X0))) = one,
inference(demodulation,[status(thm)],[c_120]) ).
tcf(c_198,plain,
! [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_98]) ).
tcf(c_199,plain,
! [X0: $i] : multiplication(X0,coantidomain(X0)) = zero,
inference(demodulation,[status(thm)],[c_97]) ).
tcf(c_200,plain,
! [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_95]) ).
tcf(c_201,plain,
! [X0: $i] : multiplication(antidomain(X0),X0) = zero,
inference(demodulation,[status(thm)],[c_94]) ).
tcf(c_206,plain,
! [X0: $i,X1: $i,X2: $i] : addition(multiplication(X0,X1),multiplication(X2,X1)) = multiplication(addition(X0,X2),X1),
inference(demodulation,[status(thm)],[c_89]) ).
tcf(c_207,plain,
! [X0: $i,X1: $i,X2: $i] : addition(multiplication(X0,X1),multiplication(X0,X2)) = multiplication(X0,addition(X1,X2)),
inference(demodulation,[status(thm)],[c_88]) ).
tcf(c_208,plain,
! [X0: $i] : multiplication(one,X0) = X0,
inference(demodulation,[status(thm)],[c_87]) ).
tcf(c_209,plain,
! [X0: $i] : multiplication(X0,one) = X0,
inference(demodulation,[status(thm)],[c_86]) ).
tcf(c_210,plain,
! [X0: $i,X1: $i,X2: $i] : multiplication(multiplication(X0,X1),X2) = multiplication(X0,multiplication(X1,X2)),
inference(demodulation,[status(thm)],[c_85]) ).
tcf(c_211,plain,
! [X0: $i] : addition(X0,X0) = X0,
inference(demodulation,[status(thm)],[c_84]) ).
tcf(c_212,plain,
! [X0: $i] : addition(X0,zero) = X0,
inference(demodulation,[status(thm)],[c_83]) ).
tcf(c_213,plain,
! [X0: $i,X1: $i,X2: $i] : addition(addition(X0,X1),X2) = addition(X0,addition(X1,X2)),
inference(demodulation,[status(thm)],[c_82]) ).
tcf(c_214,plain,
! [X0: $i,X1: $i] : addition(X0,X1) = addition(X1,X0),
inference(demodulation,[status(thm)],[c_81]) ).
tcf(c_366,plain,
addition(iPr_def_23,coantidomain(iPr_def_23)) = one,
inference(superposition,[status(thm)],[c_189,c_196]) ).
tcf(c_368,plain,
addition(iPr_def_24,iPr_def_23) = one,
inference(demodulation,[status(thm)],[c_366,c_214,c_190]) ).
tcf(c_382,plain,
addition(iPr_def_10,antidomain(iPr_def_10)) = one,
inference(superposition,[status(thm)],[c_176,c_197]) ).
tcf(c_383,plain,
addition(iPr_def_11,antidomain(iPr_def_11)) = one,
inference(superposition,[status(thm)],[c_177,c_197]) ).
tcf(c_384,plain,
addition(iPr_def_12,antidomain(iPr_def_12)) = one,
inference(superposition,[status(thm)],[c_178,c_197]) ).
tcf(c_386,plain,
addition(iPr_def_15,antidomain(iPr_def_15)) = one,
inference(superposition,[status(thm)],[c_181,c_197]) ).
tcf(c_388,plain,
addition(iPr_def_17,antidomain(iPr_def_17)) = one,
inference(superposition,[status(thm)],[c_183,c_197]) ).
tcf(c_391,plain,
addition(iPr_def_25,antidomain(iPr_def_25)) = one,
inference(superposition,[status(thm)],[c_191,c_197]) ).
tcf(c_392,plain,
addition(iPr_def_26,antidomain(iPr_def_26)) = one,
inference(superposition,[status(thm)],[c_192,c_197]) ).
tcf(c_393,plain,
addition(iPr_def_27,antidomain(iPr_def_27)) = one,
inference(superposition,[status(thm)],[c_193,c_197]) ).
tcf(c_394,plain,
addition(iPr_def_27,iPr_def_26) = one,
inference(demodulation,[status(thm)],[c_392,c_214,c_193]) ).
tcf(c_395,plain,
addition(iPr_def_25,iPr_def_26) = one,
inference(demodulation,[status(thm)],[c_391,c_192]) ).
tcf(c_397,plain,
addition(iPr_def_17,iPr_def_18) = one,
inference(demodulation,[status(thm)],[c_388,c_184]) ).
tcf(c_399,plain,
addition(iPr_def_15,iPr_def_16) = one,
inference(demodulation,[status(thm)],[c_386,c_182]) ).
tcf(c_400,plain,
addition(iPr_def_12,iPr_def_13) = one,
inference(demodulation,[status(thm)],[c_384,c_179]) ).
tcf(c_401,plain,
addition(iPr_def_12,iPr_def_11) = one,
inference(demodulation,[status(thm)],[c_383,c_214,c_178]) ).
tcf(c_402,plain,
addition(iPr_def_11,iPr_def_10) = one,
inference(demodulation,[status(thm)],[c_382,c_214,c_177]) ).
tcf(c_408,plain,
coantidomain(one) = zero,
inference(superposition,[status(thm)],[c_199,c_208]) ).
tcf(c_419,plain,
! [X0: $i] : addition(coantidomain(multiplication(iPr_def_19,X0)),coantidomain(multiplication(coantidomain(iPr_def_20),X0))) = coantidomain(multiplication(coantidomain(iPr_def_20),X0)),
inference(superposition,[status(thm)],[c_186,c_198]) ).
tcf(c_421,plain,
! [X0: $i] : addition(coantidomain(multiplication(iPr_def_22,X0)),coantidomain(multiplication(coantidomain(iPr_def_23),X0))) = coantidomain(multiplication(coantidomain(iPr_def_23),X0)),
inference(superposition,[status(thm)],[c_189,c_198]) ).
tcf(c_425,plain,
! [X0: $i] : addition(coantidomain(multiplication(iPr_def_22,X0)),coantidomain(multiplication(iPr_def_24,X0))) = coantidomain(multiplication(iPr_def_24,X0)),
inference(demodulation,[status(thm)],[c_421,c_190]) ).
tcf(c_426,plain,
! [X0: $i] : addition(coantidomain(multiplication(iPr_def_19,X0)),coantidomain(multiplication(iPr_def_21,X0))) = coantidomain(multiplication(iPr_def_21,X0)),
inference(demodulation,[status(thm)],[c_419,c_187]) ).
tcf(c_443,plain,
! [X0: $i] : addition(antidomain(zero),antidomain(multiplication(X0,antidomain(antidomain(coantidomain(X0)))))) = antidomain(multiplication(X0,antidomain(antidomain(coantidomain(X0))))),
inference(superposition,[status(thm)],[c_199,c_200]) ).
tcf(c_493,plain,
multiplication(iPr_def_15,iPr_def_14) = zero,
inference(superposition,[status(thm)],[c_181,c_201]) ).
tcf(c_503,plain,
antidomain(one) = zero,
inference(superposition,[status(thm)],[c_201,c_209]) ).
tcf(c_527,plain,
addition(zero,coantidomain(zero)) = one,
inference(superposition,[status(thm)],[c_408,c_196]) ).
tcf(c_529,plain,
addition(zero,antidomain(zero)) = one,
inference(superposition,[status(thm)],[c_503,c_197]) ).
tcf(c_539,plain,
! [X0: $i] : addition(zero,X0) = X0,
inference(superposition,[status(thm)],[c_214,c_212]) ).
tcf(c_570,plain,
! [X0: $i,X1: $i] : multiplication(addition(antidomain(X0),X1),X0) = addition(zero,multiplication(X1,X0)),
inference(superposition,[status(thm)],[c_201,c_206]) ).
tcf(c_575,plain,
! [X0: $i,X1: $i] : addition(multiplication(X0,X1),X1) = multiplication(addition(X0,one),X1),
inference(superposition,[status(thm)],[c_208,c_206]) ).
tcf(c_589,plain,
! [X0: $i,X1: $i] : addition(X0,multiplication(X1,X0)) = multiplication(addition(X1,one),X0),
inference(demodulation,[status(thm)],[c_575,c_214]) ).
tcf(c_591,plain,
! [X0: $i,X1: $i] : multiplication(addition(antidomain(X0),X1),X0) = multiplication(X1,X0),
inference(demodulation,[status(thm)],[c_570,c_539]) ).
tcf(c_646,plain,
! [X0: $i,X1: $i] : multiplication(antidomain(X0),addition(X0,X1)) = addition(zero,multiplication(antidomain(X0),X1)),
inference(superposition,[status(thm)],[c_201,c_207]) ).
tcf(c_650,plain,
! [X0: $i,X1: $i] : addition(multiplication(X0,X1),X0) = multiplication(X0,addition(X1,one)),
inference(superposition,[status(thm)],[c_209,c_207]) ).
tcf(c_654,plain,
! [X0: $i,X1: $i] : multiplication(antidomain(X0),addition(X1,X0)) = addition(multiplication(antidomain(X0),X1),zero),
inference(superposition,[status(thm)],[c_201,c_207]) ).
tcf(c_666,plain,
! [X0: $i,X1: $i] : addition(X0,multiplication(X0,X1)) = multiplication(X0,addition(X1,one)),
inference(demodulation,[status(thm)],[c_650,c_214]) ).
tcf(c_669,plain,
! [X0: $i,X1: $i] : multiplication(antidomain(X0),addition(X1,X0)) = multiplication(antidomain(X0),X1),
inference(demodulation,[status(thm)],[c_654,c_212]) ).
tcf(c_670,plain,
! [X0: $i,X1: $i] : multiplication(antidomain(X0),addition(X0,X1)) = multiplication(antidomain(X0),X1),
inference(demodulation,[status(thm)],[c_646,c_539]) ).
tcf(c_692,plain,
! [X0: $i] : multiplication(iPr_def_21,multiplication(sK1_goals_X1,X0)) = multiplication(iPr_def_22,X0),
inference(superposition,[status(thm)],[c_188,c_210]) ).
tcf(c_702,plain,
! [X0: $i,X1: $i] : multiplication(X0,multiplication(X1,coantidomain(multiplication(X0,X1)))) = zero,
inference(superposition,[status(thm)],[c_210,c_199]) ).
tcf(c_720,plain,
! [X0: $i,X1: $i] : addition(X0,addition(X0,X1)) = addition(X0,X1),
inference(superposition,[status(thm)],[c_211,c_213]) ).
tcf(c_727,plain,
! [X0: $i] : addition(iPr_def_11,addition(iPr_def_27,X0)) = addition(iPr_def_28,X0),
inference(superposition,[status(thm)],[c_194,c_213]) ).
tcf(c_1522,plain,
coantidomain(zero) = one,
inference(superposition,[status(thm)],[c_527,c_539]) ).
tcf(c_1544,plain,
antidomain(zero) = one,
inference(superposition,[status(thm)],[c_529,c_539]) ).
tcf(c_1659,plain,
! [X0: $i] : addition(one,antidomain(multiplication(X0,antidomain(antidomain(coantidomain(X0)))))) = antidomain(multiplication(X0,antidomain(antidomain(coantidomain(X0))))),
inference(light_normalisation,[status(thm)],[c_443,c_1544]) ).
tcf(c_1667,plain,
addition(one,antidomain(multiplication(iPr_def_23,antidomain(antidomain(iPr_def_24))))) = antidomain(multiplication(iPr_def_23,antidomain(antidomain(iPr_def_24)))),
inference(superposition,[status(thm)],[c_190,c_1659]) ).
tcf(c_1674,plain,
addition(one,antidomain(multiplication(iPr_def_23,iPr_def_26))) = antidomain(multiplication(iPr_def_23,iPr_def_26)),
inference(demodulation,[status(thm)],[c_1667,c_191,c_192]) ).
tcf(c_3863,plain,
multiplication(iPr_def_21,iPr_def_14) = multiplication(iPr_def_22,iPr_def_13),
inference(superposition,[status(thm)],[c_180,c_692]) ).
tcf(c_4301,plain,
! [X0: $i] : addition(antidomain(X0),one) = one,
inference(superposition,[status(thm)],[c_197,c_720]) ).
tcf(c_4302,plain,
! [X0: $i] : addition(coantidomain(X0),one) = one,
inference(superposition,[status(thm)],[c_196,c_720]) ).
tcf(c_4311,plain,
addition(iPr_def_27,one) = one,
inference(superposition,[status(thm)],[c_393,c_720]) ).
tcf(c_4318,plain,
addition(iPr_def_12,one) = one,
inference(superposition,[status(thm)],[c_400,c_720]) ).
tcf(c_4320,plain,
addition(iPr_def_11,one) = one,
inference(superposition,[status(thm)],[c_402,c_720]) ).
tcf(c_4351,plain,
! [X0: $i] : addition(one,coantidomain(X0)) = one,
inference(demodulation,[status(thm)],[c_4302,c_214]) ).
tcf(c_4352,plain,
! [X0: $i] : addition(one,antidomain(X0)) = one,
inference(demodulation,[status(thm)],[c_4301,c_214]) ).
tcf(c_6114,plain,
! [X0: $i] : multiplication(antidomain(antidomain(X0)),X0) = multiplication(one,X0),
inference(superposition,[status(thm)],[c_197,c_591]) ).
tcf(c_6190,plain,
! [X0: $i] : multiplication(antidomain(antidomain(X0)),X0) = X0,
inference(demodulation,[status(thm)],[c_6114,c_208]) ).
tcf(c_6342,plain,
! [X0: $i] : addition(X0,multiplication(iPr_def_27,X0)) = multiplication(one,X0),
inference(superposition,[status(thm)],[c_4311,c_589]) ).
tcf(c_6343,plain,
! [X0: $i] : addition(X0,multiplication(iPr_def_27,X0)) = X0,
inference(demodulation,[status(thm)],[c_6342,c_208]) ).
tcf(c_6410,plain,
addition(one,iPr_def_23) = one,
inference(superposition,[status(thm)],[c_189,c_4351]) ).
tcf(c_6424,plain,
addition(iPr_def_23,one) = one,
inference(demodulation,[status(thm)],[c_6410,c_214]) ).
tcf(c_8548,plain,
! [X0: $i] : addition(X0,multiplication(iPr_def_23,X0)) = multiplication(one,X0),
inference(superposition,[status(thm)],[c_6424,c_589]) ).
tcf(c_8549,plain,
! [X0: $i] : addition(X0,multiplication(iPr_def_23,X0)) = X0,
inference(demodulation,[status(thm)],[c_8548,c_208]) ).
tcf(c_10063,plain,
! [X0: $i] : addition(X0,multiplication(iPr_def_12,X0)) = multiplication(one,X0),
inference(superposition,[status(thm)],[c_4318,c_589]) ).
tcf(c_10064,plain,
! [X0: $i] : addition(X0,multiplication(iPr_def_12,X0)) = X0,
inference(demodulation,[status(thm)],[c_10063,c_208]) ).
tcf(c_10317,plain,
! [X0: $i] : addition(X0,multiplication(X0,iPr_def_11)) = multiplication(X0,one),
inference(superposition,[status(thm)],[c_4320,c_666]) ).
tcf(c_10401,plain,
! [X0: $i] : addition(X0,multiplication(X0,iPr_def_11)) = X0,
inference(demodulation,[status(thm)],[c_10317,c_209]) ).
tcf(c_11422,plain,
multiplication(antidomain(iPr_def_26),one) = multiplication(antidomain(iPr_def_26),iPr_def_25),
inference(superposition,[status(thm)],[c_395,c_669]) ).
tcf(c_11424,plain,
multiplication(antidomain(iPr_def_18),one) = multiplication(antidomain(iPr_def_18),iPr_def_17),
inference(superposition,[status(thm)],[c_397,c_669]) ).
tcf(c_11426,plain,
multiplication(antidomain(iPr_def_16),one) = multiplication(antidomain(iPr_def_16),iPr_def_15),
inference(superposition,[status(thm)],[c_399,c_669]) ).
tcf(c_11509,plain,
multiplication(iPr_def_17,iPr_def_15) = iPr_def_17,
inference(demodulation,[status(thm)],[c_11426,c_209,c_183]) ).
tcf(c_11511,plain,
multiplication(iPr_def_19,iPr_def_17) = iPr_def_19,
inference(demodulation,[status(thm)],[c_11424,c_209,c_185]) ).
tcf(c_11512,plain,
multiplication(iPr_def_27,iPr_def_25) = iPr_def_27,
inference(demodulation,[status(thm)],[c_11422,c_209,c_193]) ).
tcf(c_11627,plain,
multiplication(antidomain(iPr_def_11),iPr_def_27) = multiplication(antidomain(iPr_def_11),iPr_def_28),
inference(superposition,[status(thm)],[c_194,c_670]) ).
tcf(c_11631,plain,
multiplication(antidomain(iPr_def_24),one) = multiplication(antidomain(iPr_def_24),iPr_def_23),
inference(superposition,[status(thm)],[c_368,c_670]) ).
tcf(c_11643,plain,
multiplication(antidomain(iPr_def_12),one) = multiplication(antidomain(iPr_def_12),iPr_def_11),
inference(superposition,[status(thm)],[c_401,c_670]) ).
tcf(c_11700,plain,
multiplication(iPr_def_13,iPr_def_11) = iPr_def_13,
inference(demodulation,[status(thm)],[c_11643,c_209,c_179]) ).
tcf(c_11708,plain,
multiplication(iPr_def_25,iPr_def_23) = iPr_def_25,
inference(demodulation,[status(thm)],[c_11631,c_209,c_191]) ).
tcf(c_11709,plain,
multiplication(iPr_def_12,iPr_def_27) = multiplication(iPr_def_12,iPr_def_28),
inference(demodulation,[status(thm)],[c_11627,c_178]) ).
tcf(c_14548,plain,
multiplication(antidomain(iPr_def_12),iPr_def_11) = iPr_def_11,
inference(superposition,[status(thm)],[c_178,c_6190]) ).
tcf(c_14551,plain,
multiplication(antidomain(iPr_def_16),iPr_def_15) = iPr_def_15,
inference(superposition,[status(thm)],[c_182,c_6190]) ).
tcf(c_14553,plain,
multiplication(antidomain(iPr_def_18),iPr_def_17) = iPr_def_17,
inference(superposition,[status(thm)],[c_184,c_6190]) ).
tcf(c_14556,plain,
multiplication(antidomain(iPr_def_26),iPr_def_25) = iPr_def_25,
inference(superposition,[status(thm)],[c_192,c_6190]) ).
tcf(c_14628,plain,
iPr_def_25 = iPr_def_27,
inference(demodulation,[status(thm)],[c_14556,c_193,c_11512]) ).
tcf(c_14630,plain,
iPr_def_17 = iPr_def_19,
inference(demodulation,[status(thm)],[c_14553,c_185,c_11511]) ).
tcf(c_14632,plain,
iPr_def_15 = iPr_def_17,
inference(demodulation,[status(thm)],[c_14551,c_183,c_11509]) ).
tcf(c_14634,plain,
iPr_def_11 = iPr_def_13,
inference(demodulation,[status(thm)],[c_14548,c_179,c_11700]) ).
tcf(c_14722,plain,
multiplication(iPr_def_17,iPr_def_14) = zero,
inference(demodulation,[status(thm)],[c_493,c_14632]) ).
tcf(c_14735,plain,
multiplication(iPr_def_19,iPr_def_14) = zero,
inference(demodulation,[status(thm)],[c_14722,c_14630]) ).
tcf(c_14747,plain,
multiplication(iPr_def_21,iPr_def_14) = multiplication(iPr_def_22,iPr_def_11),
inference(demodulation,[status(thm)],[c_3863,c_14634]) ).
tcf(c_24898,plain,
multiplication(iPr_def_27,iPr_def_23) = iPr_def_27,
inference(light_normalisation,[status(thm)],[c_11708,c_14628]) ).
tcf(c_25586,plain,
addition(coantidomain(zero),coantidomain(multiplication(iPr_def_21,iPr_def_14))) = coantidomain(multiplication(iPr_def_21,iPr_def_14)),
inference(superposition,[status(thm)],[c_14735,c_426]) ).
tcf(c_25592,plain,
coantidomain(multiplication(iPr_def_22,iPr_def_11)) = one,
inference(demodulation,[status(thm)],[c_25586,c_1522,c_4351,c_14747]) ).
tcf(c_29886,plain,
addition(one,coantidomain(multiplication(iPr_def_24,iPr_def_11))) = coantidomain(multiplication(iPr_def_24,iPr_def_11)),
inference(superposition,[status(thm)],[c_25592,c_425]) ).
tcf(c_29892,plain,
coantidomain(multiplication(iPr_def_24,iPr_def_11)) = one,
inference(demodulation,[status(thm)],[c_29886,c_4351]) ).
tcf(c_32047,plain,
multiplication(iPr_def_24,multiplication(iPr_def_11,one)) = zero,
inference(superposition,[status(thm)],[c_29892,c_702]) ).
tcf(c_32054,plain,
multiplication(iPr_def_24,iPr_def_11) = zero,
inference(demodulation,[status(thm)],[c_32047,c_209]) ).
tcf(c_32104,plain,
! [X0: $i] : addition(multiplication(X0,iPr_def_11),zero) = multiplication(addition(X0,iPr_def_24),iPr_def_11),
inference(superposition,[status(thm)],[c_32054,c_206]) ).
tcf(c_32113,plain,
! [X0: $i] : multiplication(addition(X0,iPr_def_24),iPr_def_11) = multiplication(X0,iPr_def_11),
inference(demodulation,[status(thm)],[c_32104,c_212]) ).
tcf(c_35689,plain,
addition(iPr_def_23,iPr_def_27) = iPr_def_23,
inference(superposition,[status(thm)],[c_24898,c_6343]) ).
tcf(c_35770,plain,
addition(iPr_def_27,iPr_def_23) = iPr_def_23,
inference(demodulation,[status(thm)],[c_35689,c_214]) ).
tcf(c_38674,plain,
antidomain(multiplication(iPr_def_23,iPr_def_26)) = one,
inference(superposition,[status(thm)],[c_1674,c_4352]) ).
tcf(c_38857,plain,
multiplication(one,multiplication(iPr_def_23,iPr_def_26)) = zero,
inference(superposition,[status(thm)],[c_38674,c_201]) ).
tcf(c_38870,plain,
multiplication(iPr_def_23,iPr_def_26) = zero,
inference(demodulation,[status(thm)],[c_38857,c_208]) ).
tcf(c_38916,plain,
! [X0: $i] : addition(multiplication(iPr_def_23,X0),zero) = multiplication(iPr_def_23,addition(X0,iPr_def_26)),
inference(superposition,[status(thm)],[c_38870,c_207]) ).
tcf(c_38931,plain,
! [X0: $i] : multiplication(iPr_def_23,addition(X0,iPr_def_26)) = multiplication(iPr_def_23,X0),
inference(demodulation,[status(thm)],[c_38916,c_212]) ).
tcf(c_53974,plain,
addition(iPr_def_28,multiplication(iPr_def_12,iPr_def_27)) = iPr_def_28,
inference(superposition,[status(thm)],[c_11709,c_10064]) ).
tcf(c_54042,plain,
addition(iPr_def_28,multiplication(iPr_def_12,iPr_def_27)) = addition(iPr_def_11,iPr_def_27),
inference(superposition,[status(thm)],[c_10064,c_727]) ).
tcf(c_54096,plain,
addition(iPr_def_11,iPr_def_27) = iPr_def_28,
inference(demodulation,[status(thm)],[c_54042,c_53974]) ).
tcf(c_61756,plain,
multiplication(iPr_def_23,one) = multiplication(iPr_def_23,iPr_def_27),
inference(superposition,[status(thm)],[c_394,c_38931]) ).
tcf(c_61817,plain,
multiplication(iPr_def_23,iPr_def_27) = iPr_def_23,
inference(demodulation,[status(thm)],[c_61756,c_209]) ).
tcf(c_62457,plain,
addition(iPr_def_27,iPr_def_23) = iPr_def_27,
inference(superposition,[status(thm)],[c_61817,c_8549]) ).
tcf(c_62493,plain,
iPr_def_23 = iPr_def_27,
inference(demodulation,[status(thm)],[c_35770,c_62457]) ).
tcf(c_62546,plain,
addition(iPr_def_24,iPr_def_27) = one,
inference(demodulation,[status(thm)],[c_368,c_62493]) ).
tcf(c_62552,plain,
addition(iPr_def_27,iPr_def_24) = one,
inference(demodulation,[status(thm)],[c_62546,c_214]) ).
tcf(c_65221,plain,
multiplication(one,iPr_def_11) = multiplication(iPr_def_27,iPr_def_11),
inference(superposition,[status(thm)],[c_62552,c_32113]) ).
tcf(c_65222,plain,
multiplication(iPr_def_27,iPr_def_11) = iPr_def_11,
inference(demodulation,[status(thm)],[c_65221,c_208]) ).
tcf(c_65702,plain,
addition(iPr_def_27,iPr_def_11) = iPr_def_27,
inference(superposition,[status(thm)],[c_65222,c_10401]) ).
tcf(c_65714,plain,
iPr_def_27 = iPr_def_28,
inference(demodulation,[status(thm)],[c_65702,c_214,c_54096]) ).
tcf(c_65792,plain,
iPr_def_27 != iPr_def_27,
inference(demodulation,[status(thm)],[c_195,c_65714]) ).
tcf(c_65793,plain,
$false,
inference(equality_resolution_simp,[status(thm)],[c_65792]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : KLE110-10 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.08/0.35 % Computer : n005.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Wed Sep 23 18:58:17 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.36 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.12/0.39 Running UEQ theorem proving
% 0.12/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.12/0.40
% 0.12/0.40 % ======== iProver multi-core TPTP/SMT =========
% 0.12/0.40
% 0.12/0.41 % Detected problem language: tptp
% 0.12/0.42 % Proving...
% 8.61/4.71 WARNING - Clausifier option not provided in the heuristic config "heur/vip2_118404", setting default options.
% 8.61/4.71 % SZS status Started for theBenchmark.p
% 8.61/4.71 % SZS status Unsatisfiable for theBenchmark.p
% 8.61/4.71
% 8.61/4.71 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 8.61/4.71
% 8.61/4.71 % ------ iProver source info
% 8.61/4.71
% 8.61/4.71 % git: date: 2026-07-19 20:42:38 +0200
% 8.61/4.71 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 8.61/4.71 % git: non_committed_changes: false
% 8.61/4.71
% 8.61/4.71 % ------ Parsing...% successful
% 8.61/4.71
% 8.61/4.71
% 8.61/4.71 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 8.61/4.71
% 8.61/4.71 % ------ Preprocessing... sup_sim: 0 sf_s rm: 0 0s sf_e pe_s pe_e %
% 8.61/4.71
% 8.61/4.71 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 8.61/4.71
% 8.61/4.71 % ------ Preprocessing... sf_s rm: 0 0s sf_e
% 8.61/4.71 % ------ Proving...
% 8.61/4.71 % ------ Problem Properties
% 8.61/4.71
% 8.61/4.71 %
% 8.61/4.71 % clauses 41
% 8.61/4.71 % conjectures 1
% 8.61/4.71 % EPR 1
% 8.61/4.71 % Horn 41
% 8.61/4.71 % unary 41
% 8.61/4.71 % binary 0
% 8.61/4.71 % lits 41
% 8.61/4.71 % lits eq 41
% 8.61/4.71 % fd_pure 0
% 8.61/4.71 % fd_pseudo 0
% 8.61/4.71 % fd_cond 0
% 8.61/4.71 % fd_pseudo_cond 0
% 8.61/4.71 % AC symbols 1
% 8.61/4.71
% 8.61/4.71 % ------ Input Options Time Limit: Unbounded
% 8.61/4.71
% 8.61/4.71
% 8.61/4.71 % ------
% 8.61/4.71 % Current options:
% 8.61/4.71 % ------
% 8.61/4.71
% 8.61/4.71
% 8.61/4.71 %
% 8.61/4.71
% 8.61/4.71 % ------ Proving...
% 8.61/4.71 %
% 8.61/4.71
% 8.61/4.71 % SZS status Unsatisfiable for theBenchmark.p
% 8.61/4.71
% 8.61/4.71 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 8.61/4.72
% 8.61/4.72
%------------------------------------------------------------------------------