%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : KLE112+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 : n007.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 : Theorem 111.44s 18.48s
% Output : CNFRefutation 111.44s
% Verified :
% SZS Type : Refutation
% Derivation depth : 56
% Number of leaves : 42
% Syntax : Number of formulae : 334 ( 334 unt; 19 def)
% Number of atoms : 946 ( 333 equ)
% Maximal formula atoms : 1 ( 2 avg)
% Number of connectives : 9 ( 9 ~; 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 : 235 ( 0 sgn 233 !; 2 ?; 152 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] : addition(X0,X1) = addition(X1,X0),
file('/export/starexec/sandbox2/benchmark/Axioms/KLE001+0.ax',additive_commutativity) ).
fof(f2,axiom,
! [X0,X1,X2] : addition(X2,addition(X1,X0)) = addition(addition(X2,X1),X0),
file('/export/starexec/sandbox2/benchmark/Axioms/KLE001+0.ax',additive_associativity) ).
fof(f3,axiom,
! [X0] : addition(X0,zero) = X0,
file('/export/starexec/sandbox2/benchmark/Axioms/KLE001+0.ax',additive_identity) ).
fof(f4,axiom,
! [X0] : addition(X0,X0) = X0,
file('/export/starexec/sandbox2/benchmark/Axioms/KLE001+0.ax',additive_idempotence) ).
fof(f5,axiom,
! [X0,X1,X2] : multiplication(X0,multiplication(X1,X2)) = multiplication(multiplication(X0,X1),X2),
file('/export/starexec/sandbox2/benchmark/Axioms/KLE001+0.ax',multiplicative_associativity) ).
fof(f6,axiom,
! [X0] : multiplication(X0,one) = X0,
file('/export/starexec/sandbox2/benchmark/Axioms/KLE001+0.ax',multiplicative_right_identity) ).
fof(f7,axiom,
! [X0] : multiplication(one,X0) = X0,
file('/export/starexec/sandbox2/benchmark/Axioms/KLE001+0.ax',multiplicative_left_identity) ).
fof(f8,axiom,
! [X0,X1,X2] : multiplication(X0,addition(X1,X2)) = addition(multiplication(X0,X1),multiplication(X0,X2)),
file('/export/starexec/sandbox2/benchmark/Axioms/KLE001+0.ax',right_distributivity) ).
fof(f9,axiom,
! [X0,X1,X2] : multiplication(addition(X0,X1),X2) = addition(multiplication(X0,X2),multiplication(X1,X2)),
file('/export/starexec/sandbox2/benchmark/Axioms/KLE001+0.ax',left_distributivity) ).
fof(f10,axiom,
! [X0] : multiplication(X0,zero) = zero,
file('/export/starexec/sandbox2/benchmark/Axioms/KLE001+0.ax',right_annihilation) ).
fof(f11,axiom,
! [X0] : multiplication(zero,X0) = zero,
file('/export/starexec/sandbox2/benchmark/Axioms/KLE001+0.ax',left_annihilation) ).
fof(f13,axiom,
! [X0] : multiplication(antidomain(X0),X0) = zero,
file('/export/starexec/sandbox2/benchmark/Axioms/KLE001+4.ax',domain1) ).
fof(f14,axiom,
! [X0,X1] : addition(antidomain(multiplication(X0,X1)),antidomain(multiplication(X0,antidomain(antidomain(X1))))) = antidomain(multiplication(X0,antidomain(antidomain(X1)))),
file('/export/starexec/sandbox2/benchmark/Axioms/KLE001+4.ax',domain2) ).
fof(f15,axiom,
! [X0] : addition(antidomain(antidomain(X0)),antidomain(X0)) = one,
file('/export/starexec/sandbox2/benchmark/Axioms/KLE001+4.ax',domain3) ).
fof(f16,axiom,
! [X0] : domain(X0) = antidomain(antidomain(X0)),
file('/export/starexec/sandbox2/benchmark/Axioms/KLE001+4.ax',domain4) ).
fof(f17,axiom,
! [X0] : multiplication(X0,coantidomain(X0)) = zero,
file('/export/starexec/sandbox2/benchmark/Axioms/KLE001+4.ax',codomain1) ).
fof(f19,axiom,
! [X0] : addition(coantidomain(coantidomain(X0)),coantidomain(X0)) = one,
file('/export/starexec/sandbox2/benchmark/Axioms/KLE001+4.ax',codomain3) ).
fof(f20,axiom,
! [X0] : codomain(X0) = coantidomain(coantidomain(X0)),
file('/export/starexec/sandbox2/benchmark/Axioms/KLE001+4.ax',codomain4) ).
fof(f21,axiom,
! [X0] : c(X0) = antidomain(domain(X0)),
file('/export/starexec/sandbox2/benchmark/Axioms/KLE001+6.ax',complement) ).
fof(f23,axiom,
! [X0,X1] : forward_diamond(X0,X1) = domain(multiplication(X0,domain(X1))),
file('/export/starexec/sandbox2/benchmark/Axioms/KLE001+6.ax',forward_diamond) ).
fof(f24,axiom,
! [X0,X1] : backward_diamond(X0,X1) = codomain(multiplication(codomain(X1),X0)),
file('/export/starexec/sandbox2/benchmark/Axioms/KLE001+6.ax',backward_diamond) ).
fof(f25,axiom,
! [X0,X1] : forward_box(X0,X1) = c(forward_diamond(X0,c(X1))),
file('/export/starexec/sandbox2/benchmark/Axioms/KLE001+6.ax',forward_box) ).
fof(f27,conjecture,
! [X0,X1] : addition(domain(X0),forward_box(X1,backward_diamond(X1,domain(X0)))) = forward_box(X1,backward_diamond(X1,domain(X0))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goals) ).
fof(f28,negated_conjecture,
~ ! [X0,X1] : addition(domain(X0),forward_box(X1,backward_diamond(X1,domain(X0)))) = forward_box(X1,backward_diamond(X1,domain(X0))),
inference(negated_conjecture,[status(cth)],[f27]) ).
fof(f29,plain,
? [X0,X1] : forward_box(X1,backward_diamond(X1,domain(X0))) != addition(domain(X0),forward_box(X1,backward_diamond(X1,domain(X0)))),
inference(ennf_transformation,[],[f28]) ).
fof(f30,plain,
forward_box(sK1,backward_diamond(sK1,domain(sK0))) != addition(domain(sK0),forward_box(sK1,backward_diamond(sK1,domain(sK0)))),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1]),skolemize(X0,sK0),skolemize(X1,sK1)],[f29]) ).
fof(f31,plain,
! [X0,X1] : addition(X0,X1) = addition(X1,X0),
inference(cnf_transformation,[],[f1]) ).
fof(f32,plain,
! [X2,X0,X1] : addition(X2,addition(X1,X0)) = addition(addition(X2,X1),X0),
inference(cnf_transformation,[],[f2]) ).
fof(f33,plain,
! [X0] : addition(X0,zero) = X0,
inference(cnf_transformation,[],[f3]) ).
fof(f34,plain,
! [X0] : addition(X0,X0) = X0,
inference(cnf_transformation,[],[f4]) ).
fof(f35,plain,
! [X2,X0,X1] : multiplication(X0,multiplication(X1,X2)) = multiplication(multiplication(X0,X1),X2),
inference(cnf_transformation,[],[f5]) ).
fof(f36,plain,
! [X0] : multiplication(X0,one) = X0,
inference(cnf_transformation,[],[f6]) ).
fof(f37,plain,
! [X0] : multiplication(one,X0) = X0,
inference(cnf_transformation,[],[f7]) ).
fof(f38,plain,
! [X2,X0,X1] : multiplication(X0,addition(X1,X2)) = addition(multiplication(X0,X1),multiplication(X0,X2)),
inference(cnf_transformation,[],[f8]) ).
fof(f39,plain,
! [X2,X0,X1] : multiplication(addition(X0,X1),X2) = addition(multiplication(X0,X2),multiplication(X1,X2)),
inference(cnf_transformation,[],[f9]) ).
fof(f40,plain,
! [X0] : zero = multiplication(X0,zero),
inference(cnf_transformation,[],[f10]) ).
fof(f41,plain,
! [X0] : zero = multiplication(zero,X0),
inference(cnf_transformation,[],[f11]) ).
fof(f42,plain,
! [X0] : zero = multiplication(antidomain(X0),X0),
inference(cnf_transformation,[],[f13]) ).
fof(f43,plain,
! [X0,X1] : antidomain(multiplication(X0,antidomain(antidomain(X1)))) = addition(antidomain(multiplication(X0,X1)),antidomain(multiplication(X0,antidomain(antidomain(X1))))),
inference(cnf_transformation,[],[f14]) ).
fof(f44,plain,
! [X0] : one = addition(antidomain(antidomain(X0)),antidomain(X0)),
inference(cnf_transformation,[],[f15]) ).
fof(f45,plain,
! [X0] : antidomain(antidomain(X0)) = domain(X0),
inference(cnf_transformation,[],[f16]) ).
fof(f46,plain,
! [X0] : zero = multiplication(X0,coantidomain(X0)),
inference(cnf_transformation,[],[f17]) ).
fof(f48,plain,
! [X0] : one = addition(coantidomain(coantidomain(X0)),coantidomain(X0)),
inference(cnf_transformation,[],[f19]) ).
fof(f49,plain,
! [X0] : coantidomain(coantidomain(X0)) = codomain(X0),
inference(cnf_transformation,[],[f20]) ).
fof(f50,plain,
! [X0] : c(X0) = antidomain(domain(X0)),
inference(cnf_transformation,[],[f21]) ).
fof(f52,plain,
! [X0,X1] : forward_diamond(X0,X1) = domain(multiplication(X0,domain(X1))),
inference(cnf_transformation,[],[f23]) ).
fof(f53,plain,
! [X0,X1] : backward_diamond(X0,X1) = codomain(multiplication(codomain(X1),X0)),
inference(cnf_transformation,[],[f24]) ).
fof(f54,plain,
! [X0,X1] : forward_box(X0,X1) = c(forward_diamond(X0,c(X1))),
inference(cnf_transformation,[],[f25]) ).
fof(f56,plain,
forward_box(sK1,backward_diamond(sK1,domain(sK0))) != addition(domain(sK0),forward_box(sK1,backward_diamond(sK1,domain(sK0)))),
inference(cnf_transformation,[],[f30]) ).
fof(f57,plain,
! [X0] : c(X0) = antidomain(antidomain(antidomain(X0))),
inference(definition_unfolding,[],[f50,f45]) ).
fof(f58,plain,
! [X0,X1] : backward_diamond(X0,X1) = coantidomain(coantidomain(multiplication(coantidomain(coantidomain(X1)),X0))),
inference(definition_unfolding,[],[f53,f49,f49]) ).
fof(f61,plain,
! [X0,X1] : forward_diamond(X0,X1) = antidomain(antidomain(multiplication(X0,antidomain(antidomain(X1))))),
inference(definition_unfolding,[],[f52,f45,f45]) ).
fof(f62,plain,
! [X0,X1] : forward_box(X0,X1) = antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(X0,antidomain(antidomain(antidomain(antidomain(antidomain(X1))))))))))),
inference(definition_unfolding,[],[f54,f57,f61,f57]) ).
fof(f63,plain,
antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK1,antidomain(antidomain(antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(sK0)))),sK1)))))))))))))) != addition(antidomain(antidomain(sK0)),antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK1,antidomain(antidomain(antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(sK0)))),sK1))))))))))))))),
inference(definition_unfolding,[],[f56,f62,f58,f45,f45,f62,f58,f45]) ).
tcf(c_49,plain,
! [X0: $i,X1: $i] : addition(X0,X1) = addition(X1,X0),
inference(cnf_transformation,[],[f31]) ).
tcf(c_50,plain,
! [X0: $i,X1: $i,X2: $i] : addition(addition(X0,X1),X2) = addition(X0,addition(X1,X2)),
inference(cnf_transformation,[],[f32]) ).
tcf(c_51,plain,
! [X0: $i] : addition(X0,zero) = X0,
inference(cnf_transformation,[],[f33]) ).
tcf(c_52,plain,
! [X0: $i] : addition(X0,X0) = X0,
inference(cnf_transformation,[],[f34]) ).
tcf(c_53,plain,
! [X0: $i,X1: $i,X2: $i] : multiplication(multiplication(X0,X1),X2) = multiplication(X0,multiplication(X1,X2)),
inference(cnf_transformation,[],[f35]) ).
tcf(c_54,plain,
! [X0: $i] : multiplication(X0,one) = X0,
inference(cnf_transformation,[],[f36]) ).
tcf(c_55,plain,
! [X0: $i] : multiplication(one,X0) = X0,
inference(cnf_transformation,[],[f37]) ).
tcf(c_56,plain,
! [X0: $i,X1: $i,X2: $i] : addition(multiplication(X0,X1),multiplication(X0,X2)) = multiplication(X0,addition(X1,X2)),
inference(cnf_transformation,[],[f38]) ).
tcf(c_57,plain,
! [X0: $i,X1: $i,X2: $i] : addition(multiplication(X0,X1),multiplication(X2,X1)) = multiplication(addition(X0,X2),X1),
inference(cnf_transformation,[],[f39]) ).
tcf(c_58,plain,
! [X0: $i] : multiplication(X0,zero) = zero,
inference(cnf_transformation,[],[f40]) ).
tcf(c_59,plain,
! [X0: $i] : multiplication(zero,X0) = zero,
inference(cnf_transformation,[],[f41]) ).
tcf(c_60,plain,
! [X0: $i] : multiplication(antidomain(X0),X0) = zero,
inference(cnf_transformation,[],[f42]) ).
tcf(c_61,plain,
! [X0: $i,X1: $i] : addition(antidomain(multiplication(X0,X1)),antidomain(multiplication(X0,antidomain(antidomain(X1))))) = antidomain(multiplication(X0,antidomain(antidomain(X1)))),
inference(cnf_transformation,[],[f43]) ).
tcf(c_62,plain,
! [X0: $i] : addition(antidomain(antidomain(X0)),antidomain(X0)) = one,
inference(cnf_transformation,[],[f44]) ).
tcf(c_63,plain,
! [X0: $i] : multiplication(X0,coantidomain(X0)) = zero,
inference(cnf_transformation,[],[f46]) ).
tcf(c_65,plain,
! [X0: $i] : addition(coantidomain(coantidomain(X0)),coantidomain(X0)) = one,
inference(cnf_transformation,[],[f48]) ).
tcf(c_66,negated_conjecture,
addition(antidomain(antidomain(sK0)),antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK1,antidomain(antidomain(antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(sK0)))),sK1))))))))))))))) != antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK1,antidomain(antidomain(antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(sK0)))),sK1)))))))))))))),
inference(cnf_transformation,[],[f63]) ).
tcf(c_82,plain,
! [X0: $i] : addition(antidomain(X0),antidomain(antidomain(X0))) = one,
inference(theory_normalisation,[status(thm)],[c_62,c_50,c_49]) ).
tcf(c_83,plain,
! [X0: $i] : addition(coantidomain(X0),coantidomain(coantidomain(X0))) = one,
inference(theory_normalisation,[status(thm)],[c_65,c_50,c_49]) ).
tcf(c_128,definition,
iPr_def_10 = antidomain(sK0),
introduced(definition,[new_symbols(definition,[iPr_def_10])],[]) ).
tcf(c_129,definition,
iPr_def_11 = antidomain(iPr_def_10),
introduced(definition,[new_symbols(definition,[iPr_def_11])],[]) ).
tcf(c_130,definition,
iPr_def_12 = coantidomain(iPr_def_11),
introduced(definition,[new_symbols(definition,[iPr_def_12])],[]) ).
tcf(c_131,definition,
iPr_def_13 = coantidomain(iPr_def_12),
introduced(definition,[new_symbols(definition,[iPr_def_13])],[]) ).
tcf(c_132,definition,
iPr_def_14 = multiplication(iPr_def_13,sK1),
introduced(definition,[new_symbols(definition,[iPr_def_14])],[]) ).
tcf(c_133,definition,
iPr_def_15 = coantidomain(iPr_def_14),
introduced(definition,[new_symbols(definition,[iPr_def_15])],[]) ).
tcf(c_134,definition,
iPr_def_16 = coantidomain(iPr_def_15),
introduced(definition,[new_symbols(definition,[iPr_def_16])],[]) ).
tcf(c_135,definition,
iPr_def_17 = antidomain(iPr_def_16),
introduced(definition,[new_symbols(definition,[iPr_def_17])],[]) ).
tcf(c_136,definition,
iPr_def_18 = antidomain(iPr_def_17),
introduced(definition,[new_symbols(definition,[iPr_def_18])],[]) ).
tcf(c_137,definition,
iPr_def_19 = antidomain(iPr_def_18),
introduced(definition,[new_symbols(definition,[iPr_def_19])],[]) ).
tcf(c_138,definition,
iPr_def_20 = antidomain(iPr_def_19),
introduced(definition,[new_symbols(definition,[iPr_def_20])],[]) ).
tcf(c_139,definition,
iPr_def_21 = antidomain(iPr_def_20),
introduced(definition,[new_symbols(definition,[iPr_def_21])],[]) ).
tcf(c_140,definition,
iPr_def_22 = multiplication(sK1,iPr_def_21),
introduced(definition,[new_symbols(definition,[iPr_def_22])],[]) ).
tcf(c_141,definition,
iPr_def_23 = antidomain(iPr_def_22),
introduced(definition,[new_symbols(definition,[iPr_def_23])],[]) ).
tcf(c_142,definition,
iPr_def_24 = antidomain(iPr_def_23),
introduced(definition,[new_symbols(definition,[iPr_def_24])],[]) ).
tcf(c_143,definition,
iPr_def_25 = antidomain(iPr_def_24),
introduced(definition,[new_symbols(definition,[iPr_def_25])],[]) ).
tcf(c_144,definition,
iPr_def_26 = antidomain(iPr_def_25),
introduced(definition,[new_symbols(definition,[iPr_def_26])],[]) ).
tcf(c_145,definition,
iPr_def_27 = antidomain(iPr_def_26),
introduced(definition,[new_symbols(definition,[iPr_def_27])],[]) ).
tcf(c_146,definition,
iPr_def_28 = addition(iPr_def_11,iPr_def_27),
introduced(definition,[new_symbols(definition,[iPr_def_28])],[]) ).
tcf(c_147,negated_conjecture,
iPr_def_28 != iPr_def_27,
inference(demodulation,[status(thm)],[c_66,c_130,c_131,c_132,c_133,c_134,c_135,c_136,c_137,c_138,c_139,c_140,c_141,c_142,c_143,c_144,c_145,c_128,c_129,c_146]) ).
tcf(c_260,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_264,plain,
addition(iPr_def_10,antidomain(iPr_def_10)) = one,
inference(superposition,[status(thm)],[c_128,c_82]) ).
tcf(c_266,plain,
addition(iPr_def_17,antidomain(iPr_def_17)) = one,
inference(superposition,[status(thm)],[c_135,c_82]) ).
tcf(c_267,plain,
addition(iPr_def_17,iPr_def_18) = one,
inference(light_normalisation,[status(thm)],[c_266,c_136]) ).
tcf(c_268,plain,
addition(iPr_def_10,iPr_def_11) = one,
inference(light_normalisation,[status(thm)],[c_264,c_129]) ).
tcf(c_270,plain,
! [X0: $i] : multiplication(X0,addition(iPr_def_17,iPr_def_18)) = X0,
inference(light_normalisation,[status(thm)],[c_54,c_267]) ).
tcf(c_271,plain,
! [X0: $i] : addition(multiplication(X0,iPr_def_17),multiplication(X0,iPr_def_18)) = X0,
inference(demodulation,[status(thm)],[c_270,c_56]) ).
tcf(c_272,plain,
! [X0: $i] : multiplication(addition(iPr_def_17,iPr_def_18),X0) = X0,
inference(light_normalisation,[status(thm)],[c_55,c_267]) ).
tcf(c_273,plain,
! [X0: $i] : addition(multiplication(iPr_def_17,X0),multiplication(iPr_def_18,X0)) = X0,
inference(demodulation,[status(thm)],[c_272,c_57]) ).
tcf(c_280,plain,
! [X0: $i] : addition(coantidomain(X0),coantidomain(coantidomain(X0))) = addition(iPr_def_17,iPr_def_18),
inference(light_normalisation,[status(thm)],[c_83,c_267]) ).
tcf(c_285,plain,
addition(iPr_def_12,coantidomain(iPr_def_12)) = addition(iPr_def_17,iPr_def_18),
inference(superposition,[status(thm)],[c_130,c_280]) ).
tcf(c_287,plain,
addition(iPr_def_15,coantidomain(iPr_def_15)) = addition(iPr_def_17,iPr_def_18),
inference(superposition,[status(thm)],[c_133,c_280]) ).
tcf(c_289,plain,
addition(iPr_def_15,iPr_def_16) = addition(iPr_def_17,iPr_def_18),
inference(light_normalisation,[status(thm)],[c_287,c_134]) ).
tcf(c_290,plain,
addition(iPr_def_12,iPr_def_13) = addition(iPr_def_17,iPr_def_18),
inference(light_normalisation,[status(thm)],[c_285,c_131]) ).
tcf(c_293,plain,
multiplication(iPr_def_11,iPr_def_10) = zero,
inference(superposition,[status(thm)],[c_129,c_60]) ).
tcf(c_314,plain,
! [X0: $i] : addition(X0,multiplication(iPr_def_11,iPr_def_10)) = X0,
inference(demodulation,[status(thm)],[c_51,c_293]) ).
tcf(c_315,plain,
! [X0: $i] : multiplication(X0,coantidomain(X0)) = multiplication(iPr_def_11,iPr_def_10),
inference(light_normalisation,[status(thm)],[c_63,c_293]) ).
tcf(c_316,plain,
multiplication(iPr_def_11,iPr_def_10) = multiplication(iPr_def_11,iPr_def_12),
inference(superposition,[status(thm)],[c_130,c_315]) ).
tcf(c_323,plain,
addition(iPr_def_15,iPr_def_16) = one,
inference(light_normalisation,[status(thm)],[c_267,c_289]) ).
tcf(c_324,plain,
addition(iPr_def_10,iPr_def_11) = addition(iPr_def_15,iPr_def_16),
inference(demodulation,[status(thm)],[c_323,c_268]) ).
tcf(c_359,plain,
! [X0: $i,X1: $i] : addition(X0,addition(X0,X1)) = addition(X0,X1),
inference(superposition,[status(thm)],[c_52,c_50]) ).
tcf(c_402,plain,
! [X0: $i] : addition(multiplication(X0,iPr_def_15),multiplication(X0,iPr_def_16)) = multiplication(X0,addition(iPr_def_10,iPr_def_11)),
inference(superposition,[status(thm)],[c_324,c_56]) ).
tcf(c_427,plain,
addition(iPr_def_10,iPr_def_11) = addition(iPr_def_17,iPr_def_18),
inference(light_normalisation,[status(thm)],[c_289,c_324]) ).
tcf(c_429,plain,
! [X0: $i] : addition(multiplication(X0,iPr_def_17),multiplication(X0,iPr_def_18)) = multiplication(X0,addition(iPr_def_10,iPr_def_11)),
inference(superposition,[status(thm)],[c_427,c_56]) ).
tcf(c_433,plain,
! [X0: $i] : addition(multiplication(X0,iPr_def_15),multiplication(X0,iPr_def_16)) = X0,
inference(light_normalisation,[status(thm)],[c_429,c_271,c_402]) ).
tcf(c_434,plain,
addition(iPr_def_10,iPr_def_11) = addition(iPr_def_12,iPr_def_13),
inference(light_normalisation,[status(thm)],[c_290,c_427]) ).
tcf(c_436,plain,
! [X0: $i] : addition(multiplication(X0,iPr_def_12),multiplication(X0,iPr_def_13)) = multiplication(X0,addition(iPr_def_10,iPr_def_11)),
inference(superposition,[status(thm)],[c_434,c_56]) ).
tcf(c_517,plain,
! [X0: $i] : addition(multiplication(iPr_def_17,X0),multiplication(iPr_def_18,X0)) = multiplication(addition(iPr_def_10,iPr_def_11),X0),
inference(superposition,[status(thm)],[c_427,c_57]) ).
tcf(c_528,plain,
! [X0: $i] : multiplication(addition(iPr_def_10,iPr_def_11),X0) = X0,
inference(light_normalisation,[status(thm)],[c_517,c_273]) ).
tcf(c_737,plain,
! [X0: $i] : addition(multiplication(iPr_def_10,X0),multiplication(iPr_def_11,X0)) = X0,
inference(demodulation,[status(thm)],[c_528,c_57]) ).
tcf(c_744,plain,
addition(multiplication(iPr_def_10,iPr_def_12),multiplication(iPr_def_11,iPr_def_10)) = iPr_def_12,
inference(superposition,[status(thm)],[c_316,c_737]) ).
tcf(c_957,plain,
! [X0: $i] : addition(multiplication(iPr_def_10,X0),X0) = X0,
inference(superposition,[status(thm)],[c_737,c_359]) ).
tcf(c_967,plain,
! [X0: $i] : addition(X0,multiplication(iPr_def_10,X0)) = X0,
inference(theory_normalisation,[status(thm)],[c_957,c_50,c_49]) ).
tcf(c_1016,plain,
! [X0: $i,X1: $i] : addition(X0,addition(multiplication(iPr_def_10,X0),X1)) = addition(X0,X1),
inference(superposition,[status(thm)],[c_967,c_50]) ).
tcf(c_1441,plain,
multiplication(iPr_def_10,iPr_def_12) = iPr_def_12,
inference(demodulation,[status(thm)],[c_744,c_314]) ).
tcf(c_5086,plain,
! [X0: $i] : addition(X0,multiplication(iPr_def_11,X0)) = addition(X0,X0),
inference(superposition,[status(thm)],[c_737,c_1016]) ).
tcf(c_5163,plain,
! [X0: $i] : addition(X0,multiplication(iPr_def_11,X0)) = X0,
inference(light_normalisation,[status(thm)],[c_5086,c_52]) ).
tcf(c_5478,plain,
! [X0: $i,X1: $i] : addition(X0,addition(multiplication(iPr_def_11,X0),X1)) = addition(X0,X1),
inference(superposition,[status(thm)],[c_5163,c_50]) ).
tcf(c_8109,plain,
! [X0: $i] : addition(multiplication(X0,iPr_def_12),multiplication(X0,iPr_def_13)) = X0,
inference(light_normalisation,[status(thm)],[c_402,c_433,c_436]) ).
tcf(c_8115,plain,
addition(iPr_def_12,multiplication(iPr_def_10,iPr_def_13)) = iPr_def_10,
inference(superposition,[status(thm)],[c_1441,c_8109]) ).
tcf(c_8357,plain,
addition(iPr_def_12,iPr_def_10) = iPr_def_10,
inference(superposition,[status(thm)],[c_8115,c_359]) ).
tcf(c_8358,plain,
! [X0: $i] : addition(iPr_def_12,addition(multiplication(iPr_def_10,iPr_def_13),X0)) = addition(iPr_def_10,X0),
inference(superposition,[status(thm)],[c_8115,c_50]) ).
tcf(c_8363,plain,
addition(iPr_def_10,iPr_def_12) = iPr_def_10,
inference(theory_normalisation,[status(thm)],[c_8357,c_50,c_49]) ).
tcf(c_8369,plain,
! [X0: $i] : addition(iPr_def_10,addition(X0,iPr_def_12)) = addition(X0,iPr_def_10),
inference(superposition,[status(thm)],[c_8363,c_260]) ).
tcf(c_11553,plain,
! [X0: $i] : addition(iPr_def_10,addition(X0,iPr_def_10)) = addition(X0,iPr_def_10),
inference(superposition,[status(thm)],[c_8369,c_359]) ).
tcf(c_13366,plain,
! [X0: $i,X1: $i] : addition(X0,addition(X1,multiplication(iPr_def_11,X0))) = addition(X0,X1),
inference(superposition,[status(thm)],[c_49,c_5478]) ).
tcf(c_22686,plain,
addition(multiplication(iPr_def_11,iPr_def_10),iPr_def_10) = addition(iPr_def_10,iPr_def_10),
inference(superposition,[status(thm)],[c_11553,c_5478]) ).
tcf(c_22709,plain,
addition(iPr_def_10,multiplication(iPr_def_11,iPr_def_10)) = addition(iPr_def_10,iPr_def_10),
inference(theory_normalisation,[status(thm)],[c_22686,c_50,c_49]) ).
tcf(c_24101,plain,
addition(iPr_def_10,multiplication(iPr_def_11,iPr_def_12)) = addition(iPr_def_12,multiplication(iPr_def_10,iPr_def_13)),
inference(superposition,[status(thm)],[c_13366,c_8358]) ).
tcf(c_24156,plain,
addition(iPr_def_12,multiplication(iPr_def_10,iPr_def_13)) = addition(iPr_def_10,iPr_def_10),
inference(light_normalisation,[status(thm)],[c_24101,c_316,c_22709]) ).
tcf(c_158217,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_158221,plain,
addition(iPr_def_10,antidomain(iPr_def_10)) = one,
inference(superposition,[status(thm)],[c_128,c_82]) ).
tcf(c_158222,plain,
addition(iPr_def_11,antidomain(iPr_def_11)) = one,
inference(superposition,[status(thm)],[c_129,c_82]) ).
tcf(c_158223,plain,
addition(iPr_def_17,antidomain(iPr_def_17)) = one,
inference(superposition,[status(thm)],[c_135,c_82]) ).
tcf(c_158224,plain,
addition(iPr_def_17,iPr_def_18) = one,
inference(light_normalisation,[status(thm)],[c_158223,c_136]) ).
tcf(c_158225,plain,
addition(iPr_def_10,iPr_def_11) = one,
inference(light_normalisation,[status(thm)],[c_158221,c_129]) ).
tcf(c_158228,plain,
addition(iPr_def_19,antidomain(iPr_def_19)) = one,
inference(superposition,[status(thm)],[c_137,c_82]) ).
tcf(c_158229,plain,
addition(iPr_def_19,iPr_def_20) = one,
inference(light_normalisation,[status(thm)],[c_158228,c_138]) ).
tcf(c_158232,plain,
addition(iPr_def_21,antidomain(iPr_def_21)) = one,
inference(superposition,[status(thm)],[c_139,c_82]) ).
tcf(c_158233,plain,
addition(iPr_def_23,antidomain(iPr_def_23)) = one,
inference(superposition,[status(thm)],[c_141,c_82]) ).
tcf(c_158234,plain,
addition(iPr_def_23,iPr_def_24) = one,
inference(light_normalisation,[status(thm)],[c_158233,c_142]) ).
tcf(c_158235,plain,
addition(iPr_def_24,antidomain(iPr_def_24)) = one,
inference(superposition,[status(thm)],[c_142,c_82]) ).
tcf(c_158236,plain,
addition(iPr_def_24,iPr_def_25) = one,
inference(light_normalisation,[status(thm)],[c_158235,c_143]) ).
tcf(c_158237,plain,
addition(iPr_def_25,antidomain(iPr_def_25)) = one,
inference(superposition,[status(thm)],[c_143,c_82]) ).
tcf(c_158238,plain,
addition(iPr_def_25,iPr_def_26) = one,
inference(light_normalisation,[status(thm)],[c_158237,c_144]) ).
tcf(c_158239,plain,
addition(iPr_def_26,antidomain(iPr_def_26)) = one,
inference(superposition,[status(thm)],[c_144,c_82]) ).
tcf(c_158240,plain,
addition(iPr_def_26,iPr_def_27) = one,
inference(light_normalisation,[status(thm)],[c_158239,c_145]) ).
tcf(c_158241,plain,
addition(iPr_def_27,antidomain(iPr_def_27)) = one,
inference(superposition,[status(thm)],[c_145,c_82]) ).
tcf(c_158246,plain,
addition(iPr_def_12,coantidomain(iPr_def_12)) = one,
inference(superposition,[status(thm)],[c_130,c_83]) ).
tcf(c_158248,plain,
addition(iPr_def_15,coantidomain(iPr_def_15)) = one,
inference(superposition,[status(thm)],[c_133,c_83]) ).
tcf(c_158250,plain,
addition(iPr_def_15,iPr_def_16) = one,
inference(light_normalisation,[status(thm)],[c_158248,c_134]) ).
tcf(c_158251,plain,
addition(iPr_def_12,iPr_def_13) = one,
inference(light_normalisation,[status(thm)],[c_158246,c_131]) ).
tcf(c_158254,plain,
multiplication(iPr_def_11,iPr_def_10) = zero,
inference(superposition,[status(thm)],[c_129,c_60]) ).
tcf(c_158260,plain,
multiplication(iPr_def_23,iPr_def_22) = zero,
inference(superposition,[status(thm)],[c_141,c_60]) ).
tcf(c_158262,plain,
multiplication(iPr_def_25,iPr_def_24) = zero,
inference(superposition,[status(thm)],[c_143,c_60]) ).
tcf(c_158263,plain,
multiplication(iPr_def_26,iPr_def_25) = zero,
inference(superposition,[status(thm)],[c_144,c_60]) ).
tcf(c_158265,plain,
antidomain(one) = zero,
inference(superposition,[status(thm)],[c_60,c_54]) ).
tcf(c_158267,plain,
multiplication(iPr_def_11,iPr_def_12) = zero,
inference(superposition,[status(thm)],[c_130,c_63]) ).
tcf(c_158269,plain,
multiplication(iPr_def_14,iPr_def_15) = zero,
inference(superposition,[status(thm)],[c_133,c_63]) ).
tcf(c_158273,plain,
addition(zero,antidomain(zero)) = one,
inference(superposition,[status(thm)],[c_158265,c_82]) ).
tcf(c_158276,plain,
addition(iPr_def_12,multiplication(iPr_def_10,iPr_def_13)) = iPr_def_10,
inference(demodulation,[status(thm)],[c_24156,c_52]) ).
tcf(c_158277,plain,
! [X0: $i] : addition(zero,X0) = X0,
inference(superposition,[status(thm)],[c_51,c_49]) ).
tcf(c_158284,plain,
! [X0: $i,X1: $i] : addition(X0,addition(X0,X1)) = addition(X0,X1),
inference(superposition,[status(thm)],[c_52,c_50]) ).
tcf(c_158298,plain,
! [X0: $i] : addition(iPr_def_12,addition(multiplication(iPr_def_10,iPr_def_13),X0)) = addition(iPr_def_10,X0),
inference(superposition,[status(thm)],[c_158276,c_50]) ).
tcf(c_158308,plain,
! [X0: $i,X1: $i] : multiplication(antidomain(X0),multiplication(X0,X1)) = multiplication(zero,X1),
inference(superposition,[status(thm)],[c_60,c_53]) ).
tcf(c_158310,plain,
! [X0: $i] : multiplication(iPr_def_13,multiplication(sK1,X0)) = multiplication(iPr_def_14,X0),
inference(superposition,[status(thm)],[c_132,c_53]) ).
tcf(c_158319,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_158323,plain,
! [X0: $i,X1: $i] : multiplication(antidomain(X0),addition(X0,X1)) = addition(zero,multiplication(antidomain(X0),X1)),
inference(superposition,[status(thm)],[c_60,c_56]) ).
tcf(c_158324,plain,
! [X0: $i,X1: $i] : multiplication(X0,addition(coantidomain(X0),X1)) = addition(zero,multiplication(X0,X1)),
inference(superposition,[status(thm)],[c_63,c_56]) ).
tcf(c_158330,plain,
! [X0: $i,X1: $i] : addition(multiplication(X0,X1),zero) = multiplication(X0,addition(X1,zero)),
inference(superposition,[status(thm)],[c_58,c_56]) ).
tcf(c_158344,plain,
! [X0: $i,X1: $i] : addition(zero,multiplication(X0,X1)) = multiplication(X0,addition(X1,zero)),
inference(theory_normalisation,[status(thm)],[c_158330,c_50,c_49]) ).
tcf(c_158356,plain,
! [X0: $i] : multiplication(iPr_def_11,multiplication(iPr_def_10,X0)) = multiplication(zero,X0),
inference(superposition,[status(thm)],[c_158254,c_53]) ).
tcf(c_158358,plain,
! [X0: $i] : multiplication(iPr_def_11,multiplication(iPr_def_10,X0)) = zero,
inference(light_normalisation,[status(thm)],[c_158356,c_59]) ).
tcf(c_158434,plain,
! [X0: $i] : addition(iPr_def_12,addition(X0,iPr_def_13)) = addition(X0,one),
inference(superposition,[status(thm)],[c_158251,c_158217]) ).
tcf(c_158454,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_158457,plain,
! [X0: $i,X1: $i] : multiplication(addition(antidomain(X0),X1),X0) = addition(zero,multiplication(X1,X0)),
inference(superposition,[status(thm)],[c_60,c_57]) ).
tcf(c_158468,plain,
! [X0: $i] : addition(zero,multiplication(X0,iPr_def_22)) = multiplication(addition(iPr_def_23,X0),iPr_def_22),
inference(superposition,[status(thm)],[c_158260,c_57]) ).
tcf(c_158651,plain,
! [X0: $i] : addition(multiplication(iPr_def_11,X0),zero) = multiplication(iPr_def_11,addition(X0,iPr_def_12)),
inference(superposition,[status(thm)],[c_158267,c_56]) ).
tcf(c_158655,plain,
! [X0: $i] : addition(zero,multiplication(iPr_def_11,X0)) = multiplication(iPr_def_11,addition(X0,iPr_def_12)),
inference(theory_normalisation,[status(thm)],[c_158651,c_50,c_49]) ).
tcf(c_158718,plain,
antidomain(zero) = one,
inference(demodulation,[status(thm)],[c_158273,c_158277]) ).
tcf(c_158754,plain,
! [X0: $i] : addition(antidomain(zero),antidomain(multiplication(iPr_def_11,antidomain(antidomain(multiplication(iPr_def_10,X0)))))) = antidomain(multiplication(iPr_def_11,antidomain(antidomain(multiplication(iPr_def_10,X0))))),
inference(superposition,[status(thm)],[c_158358,c_61]) ).
tcf(c_158763,plain,
! [X0: $i] : addition(one,antidomain(multiplication(iPr_def_11,antidomain(antidomain(multiplication(iPr_def_10,X0)))))) = antidomain(multiplication(iPr_def_11,antidomain(antidomain(multiplication(iPr_def_10,X0))))),
inference(light_normalisation,[status(thm)],[c_158754,c_158718]) ).
tcf(c_159013,plain,
! [X0: $i] : addition(antidomain(X0),one) = one,
inference(superposition,[status(thm)],[c_82,c_158284]) ).
tcf(c_159017,plain,
addition(iPr_def_11,one) = one,
inference(superposition,[status(thm)],[c_158222,c_158284]) ).
tcf(c_159019,plain,
addition(iPr_def_10,one) = one,
inference(superposition,[status(thm)],[c_158225,c_158284]) ).
tcf(c_159023,plain,
addition(iPr_def_12,one) = one,
inference(superposition,[status(thm)],[c_158251,c_158284]) ).
tcf(c_159024,plain,
addition(iPr_def_21,one) = one,
inference(superposition,[status(thm)],[c_158232,c_158284]) ).
tcf(c_159025,plain,
addition(iPr_def_27,one) = one,
inference(superposition,[status(thm)],[c_158241,c_158284]) ).
tcf(c_159026,plain,
addition(iPr_def_26,one) = one,
inference(superposition,[status(thm)],[c_158240,c_158284]) ).
tcf(c_159027,plain,
addition(iPr_def_25,one) = one,
inference(superposition,[status(thm)],[c_158238,c_158284]) ).
tcf(c_159028,plain,
addition(iPr_def_24,one) = one,
inference(superposition,[status(thm)],[c_158236,c_158284]) ).
tcf(c_159040,plain,
! [X0: $i] : addition(one,antidomain(X0)) = one,
inference(theory_normalisation,[status(thm)],[c_159013,c_50,c_49]) ).
tcf(c_159091,plain,
! [X0: $i,X1: $i] : addition(one,addition(X0,antidomain(X1))) = addition(X0,one),
inference(superposition,[status(thm)],[c_159040,c_158217]) ).
tcf(c_159141,plain,
! [X0: $i] : addition(iPr_def_12,addition(X0,one)) = addition(X0,one),
inference(superposition,[status(thm)],[c_159023,c_158217]) ).
tcf(c_159643,plain,
multiplication(iPr_def_13,iPr_def_22) = multiplication(iPr_def_14,iPr_def_21),
inference(superposition,[status(thm)],[c_140,c_158310]) ).
tcf(c_159997,plain,
addition(multiplication(iPr_def_10,iPr_def_13),one) = addition(iPr_def_10,iPr_def_13),
inference(superposition,[status(thm)],[c_158434,c_158298]) ).
tcf(c_159999,plain,
addition(one,multiplication(iPr_def_10,iPr_def_13)) = addition(iPr_def_10,iPr_def_13),
inference(theory_normalisation,[status(thm)],[c_159997,c_50,c_49]) ).
tcf(c_160258,plain,
! [X0: $i,X1: $i] : multiplication(antidomain(X0),multiplication(X0,X1)) = zero,
inference(demodulation,[status(thm)],[c_158308,c_59]) ).
tcf(c_160743,plain,
addition(multiplication(iPr_def_10,iPr_def_13),one) = addition(iPr_def_10,one),
inference(superposition,[status(thm)],[c_159141,c_158298]) ).
tcf(c_160744,plain,
addition(one,multiplication(iPr_def_10,iPr_def_13)) = addition(iPr_def_10,one),
inference(theory_normalisation,[status(thm)],[c_160743,c_50,c_49]) ).
tcf(c_160745,plain,
addition(iPr_def_10,iPr_def_13) = one,
inference(light_normalisation,[status(thm)],[c_160744,c_159019,c_159999]) ).
tcf(c_163761,plain,
! [X0: $i,X1: $i] : multiplication(antidomain(X0),addition(X0,X1)) = multiplication(antidomain(X0),X1),
inference(demodulation,[status(thm)],[c_158323,c_51,c_158344]) ).
tcf(c_163766,plain,
! [X0: $i] : multiplication(iPr_def_17,addition(iPr_def_16,X0)) = multiplication(iPr_def_17,X0),
inference(superposition,[status(thm)],[c_135,c_163761]) ).
tcf(c_163768,plain,
! [X0: $i] : multiplication(iPr_def_19,addition(iPr_def_18,X0)) = multiplication(iPr_def_19,X0),
inference(superposition,[status(thm)],[c_137,c_163761]) ).
tcf(c_163770,plain,
! [X0: $i] : multiplication(iPr_def_21,addition(iPr_def_20,X0)) = multiplication(iPr_def_21,X0),
inference(superposition,[status(thm)],[c_139,c_163761]) ).
tcf(c_163773,plain,
! [X0: $i] : multiplication(iPr_def_25,addition(iPr_def_24,X0)) = multiplication(iPr_def_25,X0),
inference(superposition,[status(thm)],[c_143,c_163761]) ).
tcf(c_163774,plain,
! [X0: $i] : multiplication(iPr_def_26,addition(iPr_def_25,X0)) = multiplication(iPr_def_26,X0),
inference(superposition,[status(thm)],[c_144,c_163761]) ).
tcf(c_163775,plain,
! [X0: $i] : multiplication(iPr_def_27,addition(iPr_def_26,X0)) = multiplication(iPr_def_27,X0),
inference(superposition,[status(thm)],[c_145,c_163761]) ).
tcf(c_163790,plain,
multiplication(antidomain(iPr_def_10),one) = multiplication(antidomain(iPr_def_10),iPr_def_11),
inference(superposition,[status(thm)],[c_158225,c_163761]) ).
tcf(c_163859,plain,
multiplication(antidomain(iPr_def_10),one) = multiplication(antidomain(iPr_def_10),iPr_def_13),
inference(superposition,[status(thm)],[c_160745,c_163761]) ).
tcf(c_163891,plain,
multiplication(iPr_def_11,one) = multiplication(iPr_def_11,iPr_def_13),
inference(light_normalisation,[status(thm)],[c_163859,c_129]) ).
tcf(c_163902,plain,
multiplication(iPr_def_11,one) = multiplication(iPr_def_11,iPr_def_11),
inference(light_normalisation,[status(thm)],[c_163790,c_129]) ).
tcf(c_164160,plain,
multiplication(iPr_def_11,iPr_def_11) = multiplication(iPr_def_11,iPr_def_13),
inference(demodulation,[status(thm)],[c_163891,c_163902]) ).
tcf(c_164388,plain,
! [X0: $i,X1: $i] : multiplication(X0,addition(coantidomain(X0),X1)) = multiplication(X0,X1),
inference(demodulation,[status(thm)],[c_158324,c_51,c_158344]) ).
tcf(c_164396,plain,
! [X0: $i] : multiplication(X0,coantidomain(coantidomain(X0))) = multiplication(X0,one),
inference(superposition,[status(thm)],[c_83,c_164388]) ).
tcf(c_164401,plain,
! [X0: $i] : multiplication(iPr_def_11,addition(iPr_def_12,X0)) = multiplication(iPr_def_11,X0),
inference(superposition,[status(thm)],[c_130,c_164388]) ).
tcf(c_164403,plain,
! [X0: $i] : multiplication(iPr_def_14,addition(iPr_def_15,X0)) = multiplication(iPr_def_14,X0),
inference(superposition,[status(thm)],[c_133,c_164388]) ).
tcf(c_164448,plain,
! [X0: $i] : multiplication(X0,coantidomain(coantidomain(X0))) = X0,
inference(light_normalisation,[status(thm)],[c_164396,c_54]) ).
tcf(c_164463,plain,
multiplication(iPr_def_11,coantidomain(iPr_def_12)) = iPr_def_11,
inference(superposition,[status(thm)],[c_130,c_164448]) ).
tcf(c_164510,plain,
multiplication(iPr_def_11,iPr_def_11) = iPr_def_11,
inference(light_normalisation,[status(thm)],[c_164463,c_131,c_164160]) ).
tcf(c_164521,plain,
multiplication(iPr_def_11,iPr_def_13) = iPr_def_11,
inference(demodulation,[status(thm)],[c_164160,c_164510]) ).
tcf(c_164627,plain,
! [X0: $i] : multiplication(iPr_def_11,multiplication(iPr_def_13,X0)) = multiplication(iPr_def_11,X0),
inference(superposition,[status(thm)],[c_164521,c_53]) ).
tcf(c_164727,plain,
! [X0: $i] : multiplication(iPr_def_17,addition(X0,iPr_def_16)) = multiplication(iPr_def_17,X0),
inference(superposition,[status(thm)],[c_49,c_163766]) ).
tcf(c_164783,plain,
! [X0: $i] : multiplication(iPr_def_19,addition(X0,iPr_def_18)) = multiplication(iPr_def_19,X0),
inference(superposition,[status(thm)],[c_49,c_163768]) ).
tcf(c_164933,plain,
! [X0: $i] : multiplication(iPr_def_21,addition(X0,iPr_def_20)) = multiplication(iPr_def_21,X0),
inference(superposition,[status(thm)],[c_49,c_163770]) ).
tcf(c_165019,plain,
! [X0: $i] : multiplication(iPr_def_25,addition(X0,iPr_def_24)) = multiplication(iPr_def_25,X0),
inference(superposition,[status(thm)],[c_49,c_163773]) ).
tcf(c_165049,plain,
! [X0: $i] : multiplication(iPr_def_26,addition(X0,iPr_def_25)) = multiplication(iPr_def_26,X0),
inference(superposition,[status(thm)],[c_49,c_163774]) ).
tcf(c_165079,plain,
! [X0: $i] : multiplication(iPr_def_27,addition(X0,iPr_def_26)) = multiplication(iPr_def_27,X0),
inference(superposition,[status(thm)],[c_49,c_163775]) ).
tcf(c_166097,plain,
! [X0: $i] : multiplication(iPr_def_11,addition(X0,iPr_def_12)) = multiplication(iPr_def_11,X0),
inference(superposition,[status(thm)],[c_49,c_164401]) ).
tcf(c_166721,plain,
multiplication(iPr_def_17,one) = multiplication(iPr_def_17,iPr_def_15),
inference(superposition,[status(thm)],[c_158250,c_164727]) ).
tcf(c_166744,plain,
multiplication(iPr_def_17,iPr_def_15) = iPr_def_17,
inference(demodulation,[status(thm)],[c_166721,c_54]) ).
tcf(c_166800,plain,
multiplication(iPr_def_19,one) = multiplication(iPr_def_19,iPr_def_17),
inference(superposition,[status(thm)],[c_158224,c_164783]) ).
tcf(c_166825,plain,
multiplication(iPr_def_19,iPr_def_17) = iPr_def_19,
inference(demodulation,[status(thm)],[c_166800,c_54]) ).
tcf(c_166834,plain,
! [X0: $i] : multiplication(iPr_def_19,multiplication(iPr_def_17,X0)) = multiplication(iPr_def_19,X0),
inference(superposition,[status(thm)],[c_166825,c_53]) ).
tcf(c_166921,plain,
multiplication(iPr_def_21,one) = multiplication(iPr_def_21,iPr_def_19),
inference(superposition,[status(thm)],[c_158229,c_164933]) ).
tcf(c_167042,plain,
multiplication(iPr_def_21,iPr_def_19) = iPr_def_21,
inference(demodulation,[status(thm)],[c_166921,c_54]) ).
tcf(c_167051,plain,
! [X0: $i] : multiplication(iPr_def_21,multiplication(iPr_def_19,X0)) = multiplication(iPr_def_21,X0),
inference(superposition,[status(thm)],[c_167042,c_53]) ).
tcf(c_167178,plain,
multiplication(iPr_def_25,one) = multiplication(iPr_def_25,iPr_def_23),
inference(superposition,[status(thm)],[c_158234,c_165019]) ).
tcf(c_167223,plain,
multiplication(iPr_def_26,one) = multiplication(iPr_def_26,iPr_def_24),
inference(superposition,[status(thm)],[c_158236,c_165049]) ).
tcf(c_167254,plain,
multiplication(iPr_def_27,one) = multiplication(iPr_def_27,iPr_def_25),
inference(superposition,[status(thm)],[c_158238,c_165079]) ).
tcf(c_167323,plain,
multiplication(iPr_def_25,iPr_def_23) = iPr_def_25,
inference(demodulation,[status(thm)],[c_167178,c_54]) ).
tcf(c_167344,plain,
multiplication(iPr_def_26,iPr_def_24) = iPr_def_26,
inference(demodulation,[status(thm)],[c_167223,c_54]) ).
tcf(c_167367,plain,
multiplication(iPr_def_27,iPr_def_25) = iPr_def_27,
inference(demodulation,[status(thm)],[c_167254,c_54]) ).
tcf(c_168120,plain,
multiplication(iPr_def_19,iPr_def_15) = multiplication(iPr_def_19,iPr_def_17),
inference(superposition,[status(thm)],[c_166744,c_166834]) ).
tcf(c_168143,plain,
multiplication(iPr_def_19,iPr_def_15) = iPr_def_19,
inference(light_normalisation,[status(thm)],[c_168120,c_166825]) ).
tcf(c_168377,plain,
multiplication(iPr_def_21,iPr_def_15) = multiplication(iPr_def_21,iPr_def_19),
inference(superposition,[status(thm)],[c_168143,c_167051]) ).
tcf(c_168401,plain,
multiplication(iPr_def_21,iPr_def_15) = iPr_def_21,
inference(light_normalisation,[status(thm)],[c_168377,c_167042]) ).
tcf(c_175128,plain,
! [X0: $i,X1: $i] : addition(one,antidomain(multiplication(X0,antidomain(antidomain(X1))))) = addition(antidomain(multiplication(X0,X1)),one),
inference(superposition,[status(thm)],[c_61,c_159091]) ).
tcf(c_175203,plain,
! [X0: $i,X1: $i] : addition(one,antidomain(multiplication(X0,antidomain(antidomain(X1))))) = addition(one,antidomain(multiplication(X0,X1))),
inference(theory_normalisation,[status(thm)],[c_175128,c_50,c_49]) ).
tcf(c_179343,plain,
multiplication(addition(one,iPr_def_26),iPr_def_25) = addition(iPr_def_25,zero),
inference(superposition,[status(thm)],[c_158263,c_158454]) ).
tcf(c_179373,plain,
! [X0: $i,X1: $i] : multiplication(addition(one,antidomain(X0)),multiplication(X0,X1)) = addition(multiplication(X0,X1),zero),
inference(superposition,[status(thm)],[c_160258,c_158454]) ).
tcf(c_179417,plain,
multiplication(addition(one,iPr_def_21),iPr_def_15) = addition(iPr_def_15,iPr_def_21),
inference(superposition,[status(thm)],[c_168401,c_158454]) ).
tcf(c_179445,plain,
multiplication(addition(one,iPr_def_26),iPr_def_24) = addition(iPr_def_24,iPr_def_26),
inference(superposition,[status(thm)],[c_167344,c_158454]) ).
tcf(c_179448,plain,
multiplication(addition(one,iPr_def_27),iPr_def_25) = addition(iPr_def_25,iPr_def_27),
inference(superposition,[status(thm)],[c_167367,c_158454]) ).
tcf(c_179792,plain,
multiplication(addition(iPr_def_27,one),iPr_def_25) = addition(iPr_def_25,iPr_def_27),
inference(theory_normalisation,[status(thm)],[c_179448,c_50,c_49]) ).
tcf(c_179793,plain,
addition(iPr_def_25,iPr_def_27) = multiplication(one,iPr_def_25),
inference(light_normalisation,[status(thm)],[c_179792,c_159025]) ).
tcf(c_179796,plain,
multiplication(addition(iPr_def_26,one),iPr_def_24) = addition(iPr_def_24,iPr_def_26),
inference(theory_normalisation,[status(thm)],[c_179445,c_50,c_49]) ).
tcf(c_179797,plain,
addition(iPr_def_24,iPr_def_26) = multiplication(one,iPr_def_24),
inference(light_normalisation,[status(thm)],[c_179796,c_159026]) ).
tcf(c_179827,plain,
multiplication(addition(iPr_def_21,one),iPr_def_15) = addition(iPr_def_15,iPr_def_21),
inference(theory_normalisation,[status(thm)],[c_179417,c_50,c_49]) ).
tcf(c_179828,plain,
addition(iPr_def_15,iPr_def_21) = multiplication(one,iPr_def_15),
inference(light_normalisation,[status(thm)],[c_179827,c_159024]) ).
tcf(c_179872,plain,
multiplication(addition(iPr_def_26,one),iPr_def_25) = addition(iPr_def_25,zero),
inference(theory_normalisation,[status(thm)],[c_179343,c_50,c_49]) ).
tcf(c_179873,plain,
addition(iPr_def_25,zero) = multiplication(one,iPr_def_25),
inference(light_normalisation,[status(thm)],[c_179872,c_159026]) ).
tcf(c_180068,plain,
! [X0: $i,X1: $i] : multiplication(addition(one,antidomain(X0)),multiplication(X0,X1)) = addition(zero,multiplication(X0,X1)),
inference(theory_normalisation,[status(thm)],[c_179373,c_50,c_49]) ).
tcf(c_180069,plain,
! [X0: $i,X1: $i] : addition(zero,multiplication(X0,X1)) = multiplication(one,multiplication(X0,X1)),
inference(light_normalisation,[status(thm)],[c_180068,c_159040]) ).
tcf(c_180426,plain,
addition(iPr_def_25,iPr_def_27) = iPr_def_25,
inference(demodulation,[status(thm)],[c_179793,c_55]) ).
tcf(c_180480,plain,
addition(iPr_def_24,iPr_def_26) = iPr_def_24,
inference(demodulation,[status(thm)],[c_179797,c_55]) ).
tcf(c_180483,plain,
! [X0: $i] : addition(iPr_def_24,addition(iPr_def_26,X0)) = addition(iPr_def_24,X0),
inference(superposition,[status(thm)],[c_180480,c_50]) ).
tcf(c_180489,plain,
multiplication(iPr_def_25,iPr_def_24) = multiplication(iPr_def_25,iPr_def_26),
inference(superposition,[status(thm)],[c_180480,c_163773]) ).
tcf(c_180494,plain,
multiplication(iPr_def_25,iPr_def_26) = zero,
inference(light_normalisation,[status(thm)],[c_180489,c_158262]) ).
tcf(c_180503,plain,
multiplication(iPr_def_25,addition(one,iPr_def_26)) = addition(iPr_def_25,zero),
inference(superposition,[status(thm)],[c_180494,c_158319]) ).
tcf(c_180523,plain,
multiplication(iPr_def_25,addition(iPr_def_26,one)) = addition(iPr_def_25,zero),
inference(theory_normalisation,[status(thm)],[c_180503,c_50,c_49]) ).
tcf(c_180524,plain,
multiplication(one,iPr_def_25) = multiplication(iPr_def_25,one),
inference(light_normalisation,[status(thm)],[c_180523,c_159026,c_179873]) ).
tcf(c_181387,plain,
addition(iPr_def_24,one) = addition(iPr_def_24,iPr_def_27),
inference(superposition,[status(thm)],[c_158240,c_180483]) ).
tcf(c_181420,plain,
addition(iPr_def_24,iPr_def_27) = one,
inference(light_normalisation,[status(thm)],[c_181387,c_159028]) ).
tcf(c_181482,plain,
multiplication(iPr_def_25,one) = multiplication(iPr_def_25,iPr_def_27),
inference(superposition,[status(thm)],[c_181420,c_163773]) ).
tcf(c_181545,plain,
addition(iPr_def_15,iPr_def_21) = iPr_def_15,
inference(demodulation,[status(thm)],[c_179828,c_55]) ).
tcf(c_181553,plain,
multiplication(iPr_def_14,iPr_def_15) = multiplication(iPr_def_14,iPr_def_21),
inference(superposition,[status(thm)],[c_181545,c_164403]) ).
tcf(c_181554,plain,
multiplication(iPr_def_13,iPr_def_22) = zero,
inference(light_normalisation,[status(thm)],[c_181553,c_159643,c_158269]) ).
tcf(c_181578,plain,
multiplication(iPr_def_11,zero) = multiplication(iPr_def_11,iPr_def_22),
inference(superposition,[status(thm)],[c_181554,c_164627]) ).
tcf(c_184084,plain,
addition(iPr_def_25,zero) = multiplication(iPr_def_25,iPr_def_27),
inference(light_normalisation,[status(thm)],[c_179873,c_180524,c_181482]) ).
tcf(c_184085,plain,
multiplication(iPr_def_25,iPr_def_27) = iPr_def_25,
inference(demodulation,[status(thm)],[c_184084,c_51]) ).
tcf(c_184103,plain,
multiplication(addition(one,iPr_def_25),iPr_def_27) = addition(iPr_def_27,iPr_def_25),
inference(superposition,[status(thm)],[c_184085,c_158454]) ).
tcf(c_184110,plain,
multiplication(addition(iPr_def_25,one),iPr_def_27) = addition(iPr_def_25,iPr_def_27),
inference(theory_normalisation,[status(thm)],[c_184103,c_50,c_49]) ).
tcf(c_184111,plain,
multiplication(one,iPr_def_27) = iPr_def_25,
inference(light_normalisation,[status(thm)],[c_184110,c_159027,c_180426]) ).
tcf(c_184121,plain,
iPr_def_25 = iPr_def_27,
inference(demodulation,[status(thm)],[c_184111,c_55]) ).
tcf(c_184197,plain,
addition(iPr_def_11,iPr_def_25) = iPr_def_28,
inference(demodulation,[status(thm)],[c_146,c_184121]) ).
tcf(c_184199,plain,
iPr_def_25 != iPr_def_28,
inference(demodulation,[status(thm)],[c_147,c_184121]) ).
tcf(c_184646,plain,
! [X0: $i,X1: $i] : multiplication(addition(antidomain(X0),X1),X0) = multiplication(X1,X0),
inference(demodulation,[status(thm)],[c_158457,c_55,c_180069]) ).
tcf(c_184653,plain,
! [X0: $i] : multiplication(antidomain(antidomain(X0)),X0) = multiplication(one,X0),
inference(superposition,[status(thm)],[c_82,c_184646]) ).
tcf(c_184668,plain,
! [X0: $i] : multiplication(addition(iPr_def_23,X0),iPr_def_22) = multiplication(X0,iPr_def_22),
inference(superposition,[status(thm)],[c_141,c_184646]) ).
tcf(c_184699,plain,
! [X0: $i] : multiplication(antidomain(antidomain(X0)),X0) = X0,
inference(light_normalisation,[status(thm)],[c_184653,c_55]) ).
tcf(c_184721,plain,
multiplication(antidomain(iPr_def_24),iPr_def_23) = iPr_def_23,
inference(superposition,[status(thm)],[c_142,c_184699]) ).
tcf(c_184752,plain,
iPr_def_23 = iPr_def_25,
inference(light_normalisation,[status(thm)],[c_184721,c_143,c_167323]) ).
tcf(c_184820,plain,
addition(iPr_def_11,iPr_def_23) = iPr_def_28,
inference(demodulation,[status(thm)],[c_184197,c_184752]) ).
tcf(c_184823,plain,
iPr_def_23 != iPr_def_28,
inference(demodulation,[status(thm)],[c_184199,c_184752]) ).
tcf(c_186088,plain,
multiplication(iPr_def_11,iPr_def_22) = zero,
inference(demodulation,[status(thm)],[c_181578,c_58]) ).
tcf(c_186098,plain,
! [X0: $i] : addition(zero,multiplication(X0,iPr_def_22)) = multiplication(addition(iPr_def_11,X0),iPr_def_22),
inference(superposition,[status(thm)],[c_186088,c_57]) ).
tcf(c_186099,plain,
! [X0: $i] : addition(zero,multiplication(iPr_def_11,X0)) = multiplication(iPr_def_11,addition(iPr_def_22,X0)),
inference(superposition,[status(thm)],[c_186088,c_56]) ).
tcf(c_186102,plain,
! [X0: $i] : addition(multiplication(iPr_def_11,X0),zero) = multiplication(iPr_def_11,addition(X0,iPr_def_22)),
inference(superposition,[status(thm)],[c_186088,c_56]) ).
tcf(c_186115,plain,
! [X0: $i] : addition(zero,multiplication(iPr_def_11,X0)) = multiplication(iPr_def_11,addition(X0,iPr_def_22)),
inference(theory_normalisation,[status(thm)],[c_186102,c_50,c_49]) ).
tcf(c_186116,plain,
! [X0: $i] : multiplication(iPr_def_11,addition(X0,iPr_def_22)) = multiplication(iPr_def_11,X0),
inference(light_normalisation,[status(thm)],[c_186115,c_158655,c_166097]) ).
tcf(c_188333,plain,
! [X0: $i] : multiplication(addition(iPr_def_11,X0),iPr_def_22) = multiplication(X0,iPr_def_22),
inference(light_normalisation,[status(thm)],[c_158468,c_184668,c_186098]) ).
tcf(c_188334,plain,
! [X0: $i] : multiplication(addition(X0,iPr_def_11),iPr_def_22) = multiplication(X0,iPr_def_22),
inference(superposition,[status(thm)],[c_49,c_188333]) ).
tcf(c_189525,plain,
! [X0: $i] : multiplication(iPr_def_11,addition(iPr_def_22,X0)) = multiplication(iPr_def_11,X0),
inference(superposition,[status(thm)],[c_49,c_186116]) ).
tcf(c_194427,plain,
multiplication(one,iPr_def_22) = multiplication(iPr_def_10,iPr_def_22),
inference(superposition,[status(thm)],[c_158225,c_188334]) ).
tcf(c_194575,plain,
multiplication(iPr_def_10,iPr_def_22) = iPr_def_22,
inference(demodulation,[status(thm)],[c_194427,c_55]) ).
tcf(c_259818,plain,
! [X0: $i] : antidomain(multiplication(iPr_def_11,antidomain(antidomain(multiplication(iPr_def_10,X0))))) = one,
inference(demodulation,[status(thm)],[c_158763,c_159040,c_175203]) ).
tcf(c_259836,plain,
antidomain(multiplication(iPr_def_11,antidomain(antidomain(iPr_def_22)))) = one,
inference(superposition,[status(thm)],[c_194575,c_259818]) ).
tcf(c_259900,plain,
antidomain(multiplication(iPr_def_11,iPr_def_24)) = one,
inference(light_normalisation,[status(thm)],[c_259836,c_141,c_142]) ).
tcf(c_259946,plain,
multiplication(one,multiplication(iPr_def_11,iPr_def_24)) = zero,
inference(superposition,[status(thm)],[c_259900,c_60]) ).
tcf(c_259993,plain,
multiplication(iPr_def_11,iPr_def_24) = zero,
inference(demodulation,[status(thm)],[c_259946,c_55]) ).
tcf(c_260021,plain,
! [X0: $i] : addition(zero,multiplication(iPr_def_11,X0)) = multiplication(iPr_def_11,addition(iPr_def_24,X0)),
inference(superposition,[status(thm)],[c_259993,c_56]) ).
tcf(c_260052,plain,
! [X0: $i] : multiplication(iPr_def_11,addition(iPr_def_24,X0)) = multiplication(iPr_def_11,X0),
inference(light_normalisation,[status(thm)],[c_260021,c_186099,c_189525]) ).
tcf(c_260899,plain,
! [X0: $i] : multiplication(iPr_def_11,addition(X0,iPr_def_24)) = multiplication(iPr_def_11,X0),
inference(superposition,[status(thm)],[c_49,c_260052]) ).
tcf(c_261158,plain,
multiplication(iPr_def_11,one) = multiplication(iPr_def_11,iPr_def_23),
inference(superposition,[status(thm)],[c_158234,c_260899]) ).
tcf(c_261231,plain,
multiplication(iPr_def_11,iPr_def_23) = iPr_def_11,
inference(demodulation,[status(thm)],[c_261158,c_54]) ).
tcf(c_261261,plain,
multiplication(addition(one,iPr_def_11),iPr_def_23) = addition(iPr_def_23,iPr_def_11),
inference(superposition,[status(thm)],[c_261231,c_158454]) ).
tcf(c_261272,plain,
multiplication(addition(iPr_def_11,one),iPr_def_23) = addition(iPr_def_11,iPr_def_23),
inference(theory_normalisation,[status(thm)],[c_261261,c_50,c_49]) ).
tcf(c_261273,plain,
multiplication(one,iPr_def_23) = iPr_def_28,
inference(light_normalisation,[status(thm)],[c_261272,c_159017,c_184820]) ).
tcf(c_261318,plain,
iPr_def_23 = iPr_def_28,
inference(demodulation,[status(thm)],[c_261273,c_55]) ).
tcf(c_261319,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[c_261318,c_184823]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : KLE112+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.11/0.38 % Computer : n007.cluster.edu
% 0.11/0.38 % Model : x86_64 x86_64
% 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.38 % Memory : 8046.5625MB
% 0.11/0.38 % OS : Linux 6.8.0-71-generic
% 0.11/0.38 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.38 % DateTime : Wed Sep 23 18:56:37 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.38 Running run_iprover 300 /export/starexec/sandbox2/benchmark/theBenchmark.p THM
% 0.11/0.42 Running first-order theorem proving
% 0.11/0.42 Running: /export/starexec/sandbox2/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.11/0.43
% 0.11/0.43 % ======== iProver multi-core TPTP/SMT =========
% 0.11/0.43
% 0.11/0.43 % Detected problem language: tptp
% 0.11/0.44 % Proving...
% 111.44/18.48 % SZS status Started for theBenchmark.p
% 111.44/18.48 % SZS status Theorem for theBenchmark.p
% 111.44/18.48
% 111.44/18.48 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 111.44/18.48
% 111.44/18.48 % ------ iProver source info
% 111.44/18.48
% 111.44/18.48 % git: date: 2026-07-19 20:42:38 +0200
% 111.44/18.48 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 111.44/18.48 % git: non_committed_changes: false
% 111.44/18.48
% 111.44/18.48 % ------ Parsing...
% 111.44/18.48 % ------ Clausification by vclausify_rel & Parsing by iProver...% ------ preprocesses with Option_UEQ
% 111.44/18.48 %
% 111.44/18.48
% 111.44/18.48 % ------ Preprocessing... sup_sim: 0 sf_s rm: 0 0s sf_e pe_s pe_e %
% 111.44/18.48
% 111.44/18.48 % ------ Preprocessing...% ------ preprocesses with Option_UEQ
% 111.44/18.48 gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 111.44/18.48
% 111.44/18.48 % ------ Preprocessing... sf_s rm: 0 0s sf_e
% 111.44/18.48 % ------ Proving...
% 111.44/18.48 % ------ Problem Properties
% 111.44/18.48
% 111.44/18.48 %
% 111.44/18.48 % clauses 37
% 111.44/18.48 % conjectures 1
% 111.44/18.48 % EPR 1
% 111.44/18.48 % Horn 37
% 111.44/18.48 % unary 37
% 111.44/18.48 % binary 0
% 111.44/18.48 % lits 37
% 111.44/18.48 % lits eq 37
% 111.44/18.48 % fd_pure 0
% 111.44/18.48 % fd_pseudo 0
% 111.44/18.48 % fd_cond 0
% 111.44/18.48 % fd_pseudo_cond 0
% 111.44/18.48 % AC symbols 1
% 111.44/18.48
% 111.44/18.48 % ------ Schedule UEQ
% 111.44/18.48
% 111.44/18.48 % ------ Option_UEQ Time Limit: 10.
% 111.44/18.48
% 111.44/18.48
% 111.44/18.48 % ------
% 111.44/18.48 % Current options:
% 111.44/18.48 % ------
% 111.44/18.48
% 111.44/18.48
% 111.44/18.48 %
% 111.44/18.48
% 111.44/18.48 % ------ Proving...
% 111.44/18.48 % Proof_search_loop: time out after: 2715 full_loop iterations
% 111.44/18.48
% 111.44/18.48 % ------ Option_UEQ Time Limit: 15.
% 111.44/18.48
% 111.44/18.48
% 111.44/18.48 % ------
% 111.44/18.48 % Current options:
% 111.44/18.48 % ------
% 111.44/18.48
% 111.44/18.48
% 111.44/18.48 %
% 111.44/18.48
% 111.44/18.48 % ------ Proving...
% 111.44/18.48 %
% 111.44/18.48
% 111.44/18.48 % SZS status Theorem for theBenchmark.p
% 111.44/18.48
% 111.44/18.48 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 111.44/18.48
% 111.44/18.48
%------------------------------------------------------------------------------