%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : KLE133+1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n016.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 : Sun Sep 27 07:44:22 AM UTC 2026
% Result : Theorem 0.15s 0.50s
% Output : CNFRefutation 0.15s
% Verified :
% SZS Type : Refutation
% Derivation depth : 56
% Number of leaves : 12
% Syntax : Number of formulae : 131 ( 127 unt; 0 def)
% Number of atoms : 139 ( 138 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 45 ( 37 ~; 0 |; 6 &)
% ( 0 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 1 avg)
% Maximal term depth : 26 ( 5 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 12 ( 12 usr; 4 con; 0-2 aty)
% Number of variables : 104 ( 13 sgn 26 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(additive_commutativity,axiom,
! [A,B] : addition(A,B) = addition(B,A),
file('theBenchmark.p',additive_commutativity) ).
fof(additive_identity,axiom,
! [A] : addition(A,zero) = A,
file('theBenchmark.p',additive_identity) ).
fof(multiplicative_right_identity,axiom,
! [A] : multiplication(A,one) = A,
file('theBenchmark.p',multiplicative_right_identity) ).
fof(right_annihilation,axiom,
! [A] : multiplication(A,zero) = zero,
file('theBenchmark.p',right_annihilation) ).
fof(left_annihilation,axiom,
! [A] : multiplication(zero,A) = zero,
file('theBenchmark.p',left_annihilation) ).
fof(domain1,axiom,
! [X0] : multiplication(antidomain(X0),X0) = zero,
file('theBenchmark.p',domain1) ).
fof(domain3,axiom,
! [X0] : addition(antidomain(antidomain(X0)),antidomain(X0)) = one,
file('theBenchmark.p',domain3) ).
fof(domain4,axiom,
! [X0] : domain(X0) = antidomain(antidomain(X0)),
file('theBenchmark.p',domain4) ).
fof(domain_difference,axiom,
! [X0,X1] : domain_difference(X0,X1) = multiplication(domain(X0),antidomain(X1)),
file('theBenchmark.p',domain_difference) ).
fof(forward_diamond,axiom,
! [X0,X1] : forward_diamond(X0,X1) = domain(multiplication(X0,domain(X1))),
file('theBenchmark.p',forward_diamond) ).
fof(divergence1,axiom,
! [X0] : forward_diamond(X0,divergence(X0)) = divergence(X0),
file('theBenchmark.p',divergence1) ).
fof(goals,conjecture,
! [X0] :
( ( ! [X2] : forward_diamond(X0,forward_diamond(X0,domain(X2))) = forward_diamond(X0,domain(X2))
& ! [X1] : addition(domain(X1),forward_diamond(star(X0),domain_difference(domain(X1),forward_diamond(X0,domain(X1))))) = forward_diamond(star(X0),domain_difference(domain(X1),forward_diamond(X0,domain(X1)))) )
=> ! [X3] : addition(forward_diamond(X0,domain(X3)),forward_diamond(star(X0),domain_difference(domain(X3),forward_diamond(X0,domain(X3))))) = forward_diamond(star(X0),domain_difference(domain(X3),forward_diamond(X0,domain(X3)))) ),
file('theBenchmark.p',goals) ).
fof(goals_neg,negated_conjecture,
~ ! [X0] :
( ( ! [X2] : forward_diamond(X0,forward_diamond(X0,domain(X2))) = forward_diamond(X0,domain(X2))
& ! [X1] : addition(domain(X1),forward_diamond(star(X0),domain_difference(domain(X1),forward_diamond(X0,domain(X1))))) = forward_diamond(star(X0),domain_difference(domain(X1),forward_diamond(X0,domain(X1)))) )
=> ! [X3] : addition(forward_diamond(X0,domain(X3)),forward_diamond(star(X0),domain_difference(domain(X3),forward_diamond(X0,domain(X3))))) = forward_diamond(star(X0),domain_difference(domain(X3),forward_diamond(X0,domain(X3)))) ),
inference(assume_negation,[status(cth)],[goals]) ).
fof(nnf_29,plain,
? [X0] :
( ? [X3] : forward_diamond(star(X0),domain_difference(domain(X3),forward_diamond(X0,domain(X3)))) != addition(forward_diamond(X0,domain(X3)),forward_diamond(star(X0),domain_difference(domain(X3),forward_diamond(X0,domain(X3)))))
& ! [X2] : forward_diamond(X0,forward_diamond(X0,domain(X2))) = forward_diamond(X0,domain(X2))
& ! [X1] : forward_diamond(star(X0),domain_difference(domain(X1),forward_diamond(X0,domain(X1)))) = addition(domain(X1),forward_diamond(star(X0),domain_difference(domain(X1),forward_diamond(X0,domain(X1))))) ),
inference(fof_nnf,[status(thm)],[goals_neg]) ).
fof(sk_goals_neg,plain,
( forward_diamond(star(sK0),domain_difference(domain(sK1),forward_diamond(sK0,domain(sK1)))) != addition(forward_diamond(sK0,domain(sK1)),forward_diamond(star(sK0),domain_difference(domain(sK1),forward_diamond(sK0,domain(sK1)))))
& ! [X2] : forward_diamond(sK0,forward_diamond(sK0,domain(X2))) = forward_diamond(sK0,domain(X2))
& ! [X1] : forward_diamond(star(sK0),domain_difference(domain(X1),forward_diamond(sK0,domain(X1)))) = addition(domain(X1),forward_diamond(star(sK0),domain_difference(domain(X1),forward_diamond(sK0,domain(X1))))) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1]),skolemize(X0,sK0),skolemize(X3,sK1)],[nnf_29]) ).
cnf(c_32,negated_conjecture,
forward_diamond(star(sK0),domain_difference(domain(sK1),forward_diamond(sK0,domain(sK1)))) != addition(forward_diamond(sK0,domain(sK1)),forward_diamond(star(sK0),domain_difference(domain(sK1),forward_diamond(sK0,domain(sK1))))),
inference(split_conjunct,[status(thm)],[sk_goals_neg]) ).
cnf(c_33,negated_conjecture,
addition(forward_diamond(sK0,domain(sK1)),forward_diamond(star(sK0),domain_difference(domain(sK1),forward_diamond(sK0,domain(sK1))))) != forward_diamond(star(sK0),domain_difference(domain(sK1),forward_diamond(sK0,domain(sK1)))),
inference(copy,[status(thm)],[c_32]) ).
cnf(c_34,negated_conjecture,
forward_diamond(sK0,forward_diamond(sK0,domain(A))) = forward_diamond(sK0,domain(A)),
inference(split_conjunct,[status(thm)],[sk_goals_neg]) ).
cnf(c_35,negated_conjecture,
forward_diamond(star(sK0),domain_difference(domain(A),forward_diamond(sK0,domain(A)))) = addition(domain(A),forward_diamond(star(sK0),domain_difference(domain(A),forward_diamond(sK0,domain(A))))),
inference(split_conjunct,[status(thm)],[sk_goals_neg]) ).
cnf(c_36,negated_conjecture,
addition(domain(A),forward_diamond(star(sK0),domain_difference(domain(A),forward_diamond(sK0,domain(A))))) = forward_diamond(star(sK0),domain_difference(domain(A),forward_diamond(sK0,domain(A)))),
inference(copy,[status(thm)],[c_35]) ).
cnf(c_39,plain,
divergence(A) = forward_diamond(A,divergence(A)),
inference(clausify,[status(thm)],[divergence1]) ).
cnf(c_40,plain,
forward_diamond(A,divergence(A)) = divergence(A),
inference(copy,[status(thm)],[c_39]) ).
cnf(c_44,plain,
forward_diamond(A,B) = domain(multiplication(A,domain(B))),
inference(clausify,[status(thm)],[forward_diamond]) ).
cnf(c_45,plain,
domain_difference(A,B) = multiplication(domain(A),antidomain(B)),
inference(clausify,[status(thm)],[domain_difference]) ).
cnf(c_52,plain,
domain(A) = antidomain(antidomain(A)),
inference(clausify,[status(thm)],[domain4]) ).
cnf(c_53,plain,
addition(antidomain(antidomain(A)),antidomain(A)) = one,
inference(clausify,[status(thm)],[domain3]) ).
cnf(c_56,plain,
multiplication(antidomain(A),A) = zero,
inference(clausify,[status(thm)],[domain1]) ).
cnf(c_57,plain,
multiplication(zero,A) = zero,
inference(clausify,[status(thm)],[left_annihilation]) ).
cnf(c_58,plain,
multiplication(A,zero) = zero,
inference(clausify,[status(thm)],[right_annihilation]) ).
cnf(c_64,plain,
multiplication(A,one) = A,
inference(clausify,[status(thm)],[multiplicative_right_identity]) ).
cnf(c_67,plain,
addition(A,zero) = A,
inference(clausify,[status(thm)],[additive_identity]) ).
cnf(c_69,plain,
addition(A,B) = addition(B,A),
inference(clausify,[status(thm)],[additive_commutativity]) ).
cnf(c_165,plain,
domain(multiplication(A,domain(divergence(A)))) = divergence(A),
inference(paramod,[status(thm)],[c_44,c_40]) ).
cnf(c_166,plain,
domain(multiplication(A,antidomain(antidomain(divergence(A))))) = divergence(A),
inference(paramod,[status(thm)],[c_52,c_165]) ).
cnf(c_72,plain,
antidomain(antidomain(multiplication(A,antidomain(antidomain(divergence(A)))))) = divergence(A),
inference(paramod,[status(thm)],[c_52,c_166]) ).
cnf(c_167,negated_conjecture,
addition(antidomain(antidomain(A)),forward_diamond(star(sK0),domain_difference(domain(A),forward_diamond(sK0,domain(A))))) = forward_diamond(star(sK0),domain_difference(domain(A),forward_diamond(sK0,domain(A)))),
inference(paramod,[status(thm)],[c_52,c_36]) ).
cnf(c_168,negated_conjecture,
addition(antidomain(antidomain(A)),forward_diamond(star(sK0),domain_difference(antidomain(antidomain(A)),forward_diamond(sK0,domain(A))))) = forward_diamond(star(sK0),domain_difference(domain(A),forward_diamond(sK0,domain(A)))),
inference(paramod,[status(thm)],[c_52,c_167]) ).
cnf(c_169,negated_conjecture,
addition(antidomain(antidomain(A)),forward_diamond(star(sK0),domain_difference(antidomain(antidomain(A)),forward_diamond(sK0,antidomain(antidomain(A)))))) = forward_diamond(star(sK0),domain_difference(domain(A),forward_diamond(sK0,domain(A)))),
inference(paramod,[status(thm)],[c_52,c_168]) ).
cnf(c_170,negated_conjecture,
addition(antidomain(antidomain(A)),forward_diamond(star(sK0),domain_difference(antidomain(antidomain(A)),domain(multiplication(sK0,domain(antidomain(antidomain(A)))))))) = forward_diamond(star(sK0),domain_difference(domain(A),forward_diamond(sK0,domain(A)))),
inference(paramod,[status(thm)],[c_44,c_169]) ).
cnf(c_171,negated_conjecture,
addition(antidomain(antidomain(A)),forward_diamond(star(sK0),domain_difference(antidomain(antidomain(A)),domain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(A))))))))) = forward_diamond(star(sK0),domain_difference(domain(A),forward_diamond(sK0,domain(A)))),
inference(paramod,[status(thm)],[c_52,c_170]) ).
cnf(c_172,negated_conjecture,
addition(antidomain(antidomain(A)),forward_diamond(star(sK0),domain_difference(antidomain(antidomain(A)),antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(A)))))))))) = forward_diamond(star(sK0),domain_difference(domain(A),forward_diamond(sK0,domain(A)))),
inference(paramod,[status(thm)],[c_52,c_171]) ).
cnf(c_173,negated_conjecture,
addition(antidomain(antidomain(A)),forward_diamond(star(sK0),multiplication(domain(antidomain(antidomain(A))),antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(A))))))))))) = forward_diamond(star(sK0),domain_difference(domain(A),forward_diamond(sK0,domain(A)))),
inference(paramod,[status(thm)],[c_45,c_172]) ).
cnf(c_174,negated_conjecture,
addition(antidomain(antidomain(A)),forward_diamond(star(sK0),multiplication(antidomain(antidomain(antidomain(antidomain(A)))),antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(A))))))))))) = forward_diamond(star(sK0),domain_difference(domain(A),forward_diamond(sK0,domain(A)))),
inference(paramod,[status(thm)],[c_52,c_173]) ).
cnf(c_175,negated_conjecture,
addition(antidomain(antidomain(A)),domain(multiplication(star(sK0),domain(multiplication(antidomain(antidomain(antidomain(antidomain(A)))),antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(A))))))))))))) = forward_diamond(star(sK0),domain_difference(domain(A),forward_diamond(sK0,domain(A)))),
inference(paramod,[status(thm)],[c_44,c_174]) ).
cnf(c_176,negated_conjecture,
addition(antidomain(antidomain(A)),domain(multiplication(star(sK0),antidomain(antidomain(multiplication(antidomain(antidomain(antidomain(antidomain(A)))),antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(A)))))))))))))) = forward_diamond(star(sK0),domain_difference(domain(A),forward_diamond(sK0,domain(A)))),
inference(paramod,[status(thm)],[c_52,c_175]) ).
cnf(c_177,negated_conjecture,
addition(antidomain(antidomain(A)),antidomain(antidomain(multiplication(star(sK0),antidomain(antidomain(multiplication(antidomain(antidomain(antidomain(antidomain(A)))),antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(A))))))))))))))) = forward_diamond(star(sK0),domain_difference(domain(A),forward_diamond(sK0,domain(A)))),
inference(paramod,[status(thm)],[c_52,c_176]) ).
cnf(c_178,negated_conjecture,
addition(antidomain(antidomain(A)),antidomain(antidomain(multiplication(star(sK0),antidomain(antidomain(multiplication(antidomain(antidomain(antidomain(antidomain(A)))),antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(A))))))))))))))) = forward_diamond(star(sK0),domain_difference(antidomain(antidomain(A)),forward_diamond(sK0,domain(A)))),
inference(paramod,[status(thm)],[c_52,c_177]) ).
cnf(c_179,negated_conjecture,
addition(antidomain(antidomain(A)),antidomain(antidomain(multiplication(star(sK0),antidomain(antidomain(multiplication(antidomain(antidomain(antidomain(antidomain(A)))),antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(A))))))))))))))) = forward_diamond(star(sK0),domain_difference(antidomain(antidomain(A)),forward_diamond(sK0,antidomain(antidomain(A))))),
inference(paramod,[status(thm)],[c_52,c_178]) ).
cnf(c_180,negated_conjecture,
addition(antidomain(antidomain(A)),antidomain(antidomain(multiplication(star(sK0),antidomain(antidomain(multiplication(antidomain(antidomain(antidomain(antidomain(A)))),antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(A))))))))))))))) = forward_diamond(star(sK0),domain_difference(antidomain(antidomain(A)),domain(multiplication(sK0,domain(antidomain(antidomain(A))))))),
inference(paramod,[status(thm)],[c_44,c_179]) ).
cnf(c_181,negated_conjecture,
addition(antidomain(antidomain(A)),antidomain(antidomain(multiplication(star(sK0),antidomain(antidomain(multiplication(antidomain(antidomain(antidomain(antidomain(A)))),antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(A))))))))))))))) = forward_diamond(star(sK0),domain_difference(antidomain(antidomain(A)),domain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(A)))))))),
inference(paramod,[status(thm)],[c_52,c_180]) ).
cnf(c_182,negated_conjecture,
addition(antidomain(antidomain(A)),antidomain(antidomain(multiplication(star(sK0),antidomain(antidomain(multiplication(antidomain(antidomain(antidomain(antidomain(A)))),antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(A))))))))))))))) = forward_diamond(star(sK0),domain_difference(antidomain(antidomain(A)),antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(A))))))))),
inference(paramod,[status(thm)],[c_52,c_181]) ).
cnf(c_183,negated_conjecture,
addition(antidomain(antidomain(A)),antidomain(antidomain(multiplication(star(sK0),antidomain(antidomain(multiplication(antidomain(antidomain(antidomain(antidomain(A)))),antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(A))))))))))))))) = forward_diamond(star(sK0),multiplication(domain(antidomain(antidomain(A))),antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(A)))))))))),
inference(paramod,[status(thm)],[c_45,c_182]) ).
cnf(c_184,negated_conjecture,
addition(antidomain(antidomain(A)),antidomain(antidomain(multiplication(star(sK0),antidomain(antidomain(multiplication(antidomain(antidomain(antidomain(antidomain(A)))),antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(A))))))))))))))) = forward_diamond(star(sK0),multiplication(antidomain(antidomain(antidomain(antidomain(A)))),antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(A)))))))))),
inference(paramod,[status(thm)],[c_52,c_183]) ).
cnf(c_185,negated_conjecture,
addition(antidomain(antidomain(A)),antidomain(antidomain(multiplication(star(sK0),antidomain(antidomain(multiplication(antidomain(antidomain(antidomain(antidomain(A)))),antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(A))))))))))))))) = domain(multiplication(star(sK0),domain(multiplication(antidomain(antidomain(antidomain(antidomain(A)))),antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(A)))))))))))),
inference(paramod,[status(thm)],[c_44,c_184]) ).
cnf(c_186,negated_conjecture,
addition(antidomain(antidomain(A)),antidomain(antidomain(multiplication(star(sK0),antidomain(antidomain(multiplication(antidomain(antidomain(antidomain(antidomain(A)))),antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(A))))))))))))))) = domain(multiplication(star(sK0),antidomain(antidomain(multiplication(antidomain(antidomain(antidomain(antidomain(A)))),antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(A))))))))))))),
inference(paramod,[status(thm)],[c_52,c_185]) ).
cnf(c_74,negated_conjecture,
addition(antidomain(antidomain(A)),antidomain(antidomain(multiplication(star(sK0),antidomain(antidomain(multiplication(antidomain(antidomain(antidomain(antidomain(A)))),antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(A))))))))))))))) = antidomain(antidomain(multiplication(star(sK0),antidomain(antidomain(multiplication(antidomain(antidomain(antidomain(antidomain(A)))),antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(A)))))))))))))),
inference(paramod,[status(thm)],[c_52,c_186]) ).
cnf(c_187,negated_conjecture,
forward_diamond(sK0,forward_diamond(sK0,antidomain(antidomain(A)))) = forward_diamond(sK0,domain(A)),
inference(paramod,[status(thm)],[c_52,c_34]) ).
cnf(c_188,negated_conjecture,
forward_diamond(sK0,domain(multiplication(sK0,domain(antidomain(antidomain(A)))))) = forward_diamond(sK0,domain(A)),
inference(paramod,[status(thm)],[c_44,c_187]) ).
cnf(c_189,negated_conjecture,
forward_diamond(sK0,domain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(A))))))) = forward_diamond(sK0,domain(A)),
inference(paramod,[status(thm)],[c_52,c_188]) ).
cnf(c_190,negated_conjecture,
forward_diamond(sK0,antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(A)))))))) = forward_diamond(sK0,domain(A)),
inference(paramod,[status(thm)],[c_52,c_189]) ).
cnf(c_191,negated_conjecture,
domain(multiplication(sK0,domain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(A)))))))))) = forward_diamond(sK0,domain(A)),
inference(paramod,[status(thm)],[c_44,c_190]) ).
cnf(c_192,negated_conjecture,
domain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(A))))))))))) = forward_diamond(sK0,domain(A)),
inference(paramod,[status(thm)],[c_52,c_191]) ).
cnf(c_193,negated_conjecture,
antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(A)))))))))))) = forward_diamond(sK0,domain(A)),
inference(paramod,[status(thm)],[c_52,c_192]) ).
cnf(c_194,negated_conjecture,
antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(A)))))))))))) = forward_diamond(sK0,antidomain(antidomain(A))),
inference(paramod,[status(thm)],[c_52,c_193]) ).
cnf(c_195,negated_conjecture,
antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(A)))))))))))) = domain(multiplication(sK0,domain(antidomain(antidomain(A))))),
inference(paramod,[status(thm)],[c_44,c_194]) ).
cnf(c_196,negated_conjecture,
antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(A)))))))))))) = domain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(A)))))),
inference(paramod,[status(thm)],[c_52,c_195]) ).
cnf(c_75,negated_conjecture,
antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(A)))))))))))) = antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(A))))))),
inference(paramod,[status(thm)],[c_52,c_196]) ).
cnf(c_197,negated_conjecture,
addition(forward_diamond(sK0,antidomain(antidomain(sK1))),forward_diamond(star(sK0),domain_difference(domain(sK1),forward_diamond(sK0,domain(sK1))))) != forward_diamond(star(sK0),domain_difference(domain(sK1),forward_diamond(sK0,domain(sK1)))),
inference(paramod,[status(thm)],[c_52,c_33]) ).
cnf(c_198,negated_conjecture,
addition(domain(multiplication(sK0,domain(antidomain(antidomain(sK1))))),forward_diamond(star(sK0),domain_difference(domain(sK1),forward_diamond(sK0,domain(sK1))))) != forward_diamond(star(sK0),domain_difference(domain(sK1),forward_diamond(sK0,domain(sK1)))),
inference(paramod,[status(thm)],[c_44,c_197]) ).
cnf(c_199,negated_conjecture,
addition(domain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(sK1)))))),forward_diamond(star(sK0),domain_difference(domain(sK1),forward_diamond(sK0,domain(sK1))))) != forward_diamond(star(sK0),domain_difference(domain(sK1),forward_diamond(sK0,domain(sK1)))),
inference(paramod,[status(thm)],[c_52,c_198]) ).
cnf(c_200,negated_conjecture,
addition(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(sK1))))))),forward_diamond(star(sK0),domain_difference(domain(sK1),forward_diamond(sK0,domain(sK1))))) != forward_diamond(star(sK0),domain_difference(domain(sK1),forward_diamond(sK0,domain(sK1)))),
inference(paramod,[status(thm)],[c_52,c_199]) ).
cnf(c_201,negated_conjecture,
addition(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(sK1))))))),forward_diamond(star(sK0),domain_difference(antidomain(antidomain(sK1)),forward_diamond(sK0,domain(sK1))))) != forward_diamond(star(sK0),domain_difference(domain(sK1),forward_diamond(sK0,domain(sK1)))),
inference(paramod,[status(thm)],[c_52,c_200]) ).
cnf(c_202,negated_conjecture,
addition(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(sK1))))))),forward_diamond(star(sK0),domain_difference(antidomain(antidomain(sK1)),forward_diamond(sK0,antidomain(antidomain(sK1)))))) != forward_diamond(star(sK0),domain_difference(domain(sK1),forward_diamond(sK0,domain(sK1)))),
inference(paramod,[status(thm)],[c_52,c_201]) ).
cnf(c_203,negated_conjecture,
addition(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(sK1))))))),forward_diamond(star(sK0),domain_difference(antidomain(antidomain(sK1)),domain(multiplication(sK0,domain(antidomain(antidomain(sK1)))))))) != forward_diamond(star(sK0),domain_difference(domain(sK1),forward_diamond(sK0,domain(sK1)))),
inference(paramod,[status(thm)],[c_44,c_202]) ).
cnf(c_204,negated_conjecture,
addition(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(sK1))))))),forward_diamond(star(sK0),domain_difference(antidomain(antidomain(sK1)),domain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(sK1))))))))) != forward_diamond(star(sK0),domain_difference(domain(sK1),forward_diamond(sK0,domain(sK1)))),
inference(paramod,[status(thm)],[c_52,c_203]) ).
cnf(c_205,negated_conjecture,
addition(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(sK1))))))),forward_diamond(star(sK0),domain_difference(antidomain(antidomain(sK1)),antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(sK1)))))))))) != forward_diamond(star(sK0),domain_difference(domain(sK1),forward_diamond(sK0,domain(sK1)))),
inference(paramod,[status(thm)],[c_52,c_204]) ).
cnf(c_206,negated_conjecture,
addition(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(sK1))))))),forward_diamond(star(sK0),multiplication(domain(antidomain(antidomain(sK1))),antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(sK1))))))))))) != forward_diamond(star(sK0),domain_difference(domain(sK1),forward_diamond(sK0,domain(sK1)))),
inference(paramod,[status(thm)],[c_45,c_205]) ).
cnf(c_207,negated_conjecture,
addition(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(sK1))))))),forward_diamond(star(sK0),multiplication(antidomain(antidomain(antidomain(antidomain(sK1)))),antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(sK1))))))))))) != forward_diamond(star(sK0),domain_difference(domain(sK1),forward_diamond(sK0,domain(sK1)))),
inference(paramod,[status(thm)],[c_52,c_206]) ).
cnf(c_208,negated_conjecture,
addition(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(sK1))))))),domain(multiplication(star(sK0),domain(multiplication(antidomain(antidomain(antidomain(antidomain(sK1)))),antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(sK1))))))))))))) != forward_diamond(star(sK0),domain_difference(domain(sK1),forward_diamond(sK0,domain(sK1)))),
inference(paramod,[status(thm)],[c_44,c_207]) ).
cnf(c_209,negated_conjecture,
addition(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(sK1))))))),domain(multiplication(star(sK0),antidomain(antidomain(multiplication(antidomain(antidomain(antidomain(antidomain(sK1)))),antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(sK1)))))))))))))) != forward_diamond(star(sK0),domain_difference(domain(sK1),forward_diamond(sK0,domain(sK1)))),
inference(paramod,[status(thm)],[c_52,c_208]) ).
cnf(c_210,negated_conjecture,
addition(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(sK1))))))),antidomain(antidomain(multiplication(star(sK0),antidomain(antidomain(multiplication(antidomain(antidomain(antidomain(antidomain(sK1)))),antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(sK1))))))))))))))) != forward_diamond(star(sK0),domain_difference(domain(sK1),forward_diamond(sK0,domain(sK1)))),
inference(paramod,[status(thm)],[c_52,c_209]) ).
cnf(c_211,negated_conjecture,
addition(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(sK1))))))),antidomain(antidomain(multiplication(star(sK0),antidomain(antidomain(multiplication(antidomain(antidomain(antidomain(antidomain(sK1)))),antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(sK1))))))))))))))) != forward_diamond(star(sK0),domain_difference(antidomain(antidomain(sK1)),forward_diamond(sK0,domain(sK1)))),
inference(paramod,[status(thm)],[c_52,c_210]) ).
cnf(c_212,negated_conjecture,
addition(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(sK1))))))),antidomain(antidomain(multiplication(star(sK0),antidomain(antidomain(multiplication(antidomain(antidomain(antidomain(antidomain(sK1)))),antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(sK1))))))))))))))) != forward_diamond(star(sK0),domain_difference(antidomain(antidomain(sK1)),forward_diamond(sK0,antidomain(antidomain(sK1))))),
inference(paramod,[status(thm)],[c_52,c_211]) ).
cnf(c_213,negated_conjecture,
addition(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(sK1))))))),antidomain(antidomain(multiplication(star(sK0),antidomain(antidomain(multiplication(antidomain(antidomain(antidomain(antidomain(sK1)))),antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(sK1))))))))))))))) != forward_diamond(star(sK0),domain_difference(antidomain(antidomain(sK1)),domain(multiplication(sK0,domain(antidomain(antidomain(sK1))))))),
inference(paramod,[status(thm)],[c_44,c_212]) ).
cnf(c_214,negated_conjecture,
addition(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(sK1))))))),antidomain(antidomain(multiplication(star(sK0),antidomain(antidomain(multiplication(antidomain(antidomain(antidomain(antidomain(sK1)))),antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(sK1))))))))))))))) != forward_diamond(star(sK0),domain_difference(antidomain(antidomain(sK1)),domain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(sK1)))))))),
inference(paramod,[status(thm)],[c_52,c_213]) ).
cnf(c_215,negated_conjecture,
addition(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(sK1))))))),antidomain(antidomain(multiplication(star(sK0),antidomain(antidomain(multiplication(antidomain(antidomain(antidomain(antidomain(sK1)))),antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(sK1))))))))))))))) != forward_diamond(star(sK0),domain_difference(antidomain(antidomain(sK1)),antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(sK1))))))))),
inference(paramod,[status(thm)],[c_52,c_214]) ).
cnf(c_216,negated_conjecture,
addition(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(sK1))))))),antidomain(antidomain(multiplication(star(sK0),antidomain(antidomain(multiplication(antidomain(antidomain(antidomain(antidomain(sK1)))),antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(sK1))))))))))))))) != forward_diamond(star(sK0),multiplication(domain(antidomain(antidomain(sK1))),antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(sK1)))))))))),
inference(paramod,[status(thm)],[c_45,c_215]) ).
cnf(c_217,negated_conjecture,
addition(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(sK1))))))),antidomain(antidomain(multiplication(star(sK0),antidomain(antidomain(multiplication(antidomain(antidomain(antidomain(antidomain(sK1)))),antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(sK1))))))))))))))) != forward_diamond(star(sK0),multiplication(antidomain(antidomain(antidomain(antidomain(sK1)))),antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(sK1)))))))))),
inference(paramod,[status(thm)],[c_52,c_216]) ).
cnf(c_218,negated_conjecture,
addition(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(sK1))))))),antidomain(antidomain(multiplication(star(sK0),antidomain(antidomain(multiplication(antidomain(antidomain(antidomain(antidomain(sK1)))),antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(sK1))))))))))))))) != domain(multiplication(star(sK0),domain(multiplication(antidomain(antidomain(antidomain(antidomain(sK1)))),antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(sK1)))))))))))),
inference(paramod,[status(thm)],[c_44,c_217]) ).
cnf(c_219,negated_conjecture,
addition(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(sK1))))))),antidomain(antidomain(multiplication(star(sK0),antidomain(antidomain(multiplication(antidomain(antidomain(antidomain(antidomain(sK1)))),antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(sK1))))))))))))))) != domain(multiplication(star(sK0),antidomain(antidomain(multiplication(antidomain(antidomain(antidomain(antidomain(sK1)))),antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(sK1))))))))))))),
inference(paramod,[status(thm)],[c_52,c_218]) ).
cnf(c_76,negated_conjecture,
addition(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(sK1))))))),antidomain(antidomain(multiplication(star(sK0),antidomain(antidomain(multiplication(antidomain(antidomain(antidomain(antidomain(sK1)))),antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(sK1))))))))))))))) != antidomain(antidomain(multiplication(star(sK0),antidomain(antidomain(multiplication(antidomain(antidomain(antidomain(antidomain(sK1)))),antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(sK1)))))))))))))),
inference(paramod,[status(thm)],[c_52,c_219]) ).
cnf(c_81,plain,
addition(antidomain(A),antidomain(antidomain(A))) = one,
inference(paramod,[status(thm)],[c_69,c_53]) ).
cnf(c_115,plain,
antidomain(one) = zero,
inference(paramod,[status(thm)],[c_64,c_56]) ).
cnf(c_135,plain,
addition(zero,A) = A,
inference(paramod,[status(thm)],[c_69,c_67]) ).
cnf(c_140,plain,
antidomain(antidomain(zero)) = divergence(zero),
inference(paramod,[status(thm)],[c_57,c_72]) ).
cnf(c_220,plain,
addition(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(A))))))),antidomain(antidomain(multiplication(star(sK0),antidomain(antidomain(multiplication(antidomain(antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(A)))))))))))))),antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(A))))))))))))))))))))))))) = antidomain(antidomain(multiplication(star(sK0),antidomain(antidomain(multiplication(antidomain(antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(A)))))))))))))),antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(A)))))))))))))))))))))))),
inference(paramod,[status(thm)],[c_75,c_74]) ).
cnf(c_221,plain,
addition(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(A))))))),antidomain(antidomain(multiplication(star(sK0),antidomain(antidomain(multiplication(antidomain(antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(A))))))))),antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(A))))))))))))))))))))))))) = antidomain(antidomain(multiplication(star(sK0),antidomain(antidomain(multiplication(antidomain(antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(A)))))))))))))),antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(A)))))))))))))))))))))))),
inference(paramod,[status(thm)],[c_75,c_220]) ).
cnf(c_222,plain,
addition(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(A))))))),antidomain(antidomain(multiplication(star(sK0),antidomain(antidomain(multiplication(antidomain(antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(A))))))))),antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(A)))))))))))))))))))) = antidomain(antidomain(multiplication(star(sK0),antidomain(antidomain(multiplication(antidomain(antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(A)))))))))))))),antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(A)))))))))))))))))))))))),
inference(paramod,[status(thm)],[c_75,c_221]) ).
cnf(c_223,plain,
addition(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(A))))))),antidomain(antidomain(multiplication(star(sK0),antidomain(antidomain(multiplication(antidomain(antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(A))))))))),antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(A))))))))))))))) = antidomain(antidomain(multiplication(star(sK0),antidomain(antidomain(multiplication(antidomain(antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(A)))))))))))))),antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(A)))))))))))))))))))))))),
inference(paramod,[status(thm)],[c_75,c_222]) ).
cnf(c_224,plain,
addition(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(A))))))),antidomain(antidomain(multiplication(star(sK0),antidomain(antidomain(zero)))))) = antidomain(antidomain(multiplication(star(sK0),antidomain(antidomain(multiplication(antidomain(antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(A)))))))))))))),antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(A)))))))))))))))))))))))),
inference(paramod,[status(thm)],[c_56,c_223]) ).
cnf(c_225,plain,
addition(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(A))))))),antidomain(antidomain(multiplication(star(sK0),divergence(zero))))) = antidomain(antidomain(multiplication(star(sK0),antidomain(antidomain(multiplication(antidomain(antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(A)))))))))))))),antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(A)))))))))))))))))))))))),
inference(paramod,[status(thm)],[c_140,c_224]) ).
cnf(c_226,plain,
addition(antidomain(antidomain(multiplication(star(sK0),divergence(zero)))),antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(A)))))))) = antidomain(antidomain(multiplication(star(sK0),antidomain(antidomain(multiplication(antidomain(antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(A)))))))))))))),antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(A)))))))))))))))))))))))),
inference(paramod,[status(thm)],[c_69,c_225]) ).
cnf(c_227,plain,
addition(antidomain(antidomain(multiplication(star(sK0),divergence(zero)))),antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(A)))))))) = antidomain(antidomain(multiplication(star(sK0),antidomain(antidomain(multiplication(antidomain(antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(A))))))))),antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(A)))))))))))))))))))))))),
inference(paramod,[status(thm)],[c_75,c_226]) ).
cnf(c_228,plain,
addition(antidomain(antidomain(multiplication(star(sK0),divergence(zero)))),antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(A)))))))) = antidomain(antidomain(multiplication(star(sK0),antidomain(antidomain(multiplication(antidomain(antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(A))))))))),antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(A))))))))))))))))))),
inference(paramod,[status(thm)],[c_75,c_227]) ).
cnf(c_229,plain,
addition(antidomain(antidomain(multiplication(star(sK0),divergence(zero)))),antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(A)))))))) = antidomain(antidomain(multiplication(star(sK0),antidomain(antidomain(multiplication(antidomain(antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(A))))))))),antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(A)))))))))))))),
inference(paramod,[status(thm)],[c_75,c_228]) ).
cnf(c_230,plain,
addition(antidomain(antidomain(multiplication(star(sK0),divergence(zero)))),antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(A)))))))) = antidomain(antidomain(multiplication(star(sK0),antidomain(antidomain(zero))))),
inference(paramod,[status(thm)],[c_56,c_229]) ).
cnf(c_144,plain,
addition(antidomain(antidomain(multiplication(star(sK0),divergence(zero)))),antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(A)))))))) = antidomain(antidomain(multiplication(star(sK0),divergence(zero)))),
inference(paramod,[status(thm)],[c_140,c_230]) ).
cnf(c_231,plain,
addition(zero,antidomain(antidomain(one))) = one,
inference(paramod,[status(thm)],[c_115,c_81]) ).
cnf(c_232,plain,
addition(zero,antidomain(zero)) = one,
inference(paramod,[status(thm)],[c_115,c_231]) ).
cnf(c_157,plain,
antidomain(zero) = one,
inference(paramod,[status(thm)],[c_135,c_232]) ).
cnf(c_233,plain,
antidomain(one) = divergence(zero),
inference(paramod,[status(thm)],[c_157,c_140]) ).
cnf(c_234,plain,
zero = divergence(zero),
inference(paramod,[status(thm)],[c_115,c_233]) ).
cnf(c_159,plain,
divergence(zero) = zero,
inference(copy,[status(thm)],[c_234]) ).
cnf(c_235,plain,
addition(antidomain(antidomain(multiplication(star(sK0),zero))),antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(A)))))))) = antidomain(antidomain(multiplication(star(sK0),divergence(zero)))),
inference(paramod,[status(thm)],[c_159,c_144]) ).
cnf(c_236,plain,
addition(antidomain(antidomain(zero)),antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(A)))))))) = antidomain(antidomain(multiplication(star(sK0),divergence(zero)))),
inference(paramod,[status(thm)],[c_58,c_235]) ).
cnf(c_237,plain,
addition(antidomain(one),antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(A)))))))) = antidomain(antidomain(multiplication(star(sK0),divergence(zero)))),
inference(paramod,[status(thm)],[c_157,c_236]) ).
cnf(c_238,plain,
addition(zero,antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(A)))))))) = antidomain(antidomain(multiplication(star(sK0),divergence(zero)))),
inference(paramod,[status(thm)],[c_115,c_237]) ).
cnf(c_239,plain,
antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(A))))))) = antidomain(antidomain(multiplication(star(sK0),divergence(zero)))),
inference(paramod,[status(thm)],[c_135,c_238]) ).
cnf(c_240,plain,
antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(A))))))) = antidomain(antidomain(multiplication(star(sK0),zero))),
inference(paramod,[status(thm)],[c_159,c_239]) ).
cnf(c_241,plain,
antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(A))))))) = antidomain(antidomain(zero)),
inference(paramod,[status(thm)],[c_58,c_240]) ).
cnf(c_242,plain,
antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(A))))))) = antidomain(one),
inference(paramod,[status(thm)],[c_157,c_241]) ).
cnf(c_163,plain,
antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(A))))))) = zero,
inference(paramod,[status(thm)],[c_115,c_242]) ).
cnf(c_243,negated_conjecture,
addition(zero,antidomain(antidomain(multiplication(star(sK0),antidomain(antidomain(multiplication(antidomain(antidomain(antidomain(antidomain(sK1)))),antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(sK1))))))))))))))) != antidomain(antidomain(multiplication(star(sK0),antidomain(antidomain(multiplication(antidomain(antidomain(antidomain(antidomain(sK1)))),antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(sK1)))))))))))))),
inference(paramod,[status(thm)],[c_163,c_76]) ).
cnf(c_244,negated_conjecture,
addition(zero,antidomain(antidomain(multiplication(star(sK0),antidomain(antidomain(multiplication(antidomain(antidomain(antidomain(antidomain(sK1)))),antidomain(zero)))))))) != antidomain(antidomain(multiplication(star(sK0),antidomain(antidomain(multiplication(antidomain(antidomain(antidomain(antidomain(sK1)))),antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(sK1)))))))))))))),
inference(paramod,[status(thm)],[c_163,c_243]) ).
cnf(c_245,negated_conjecture,
addition(zero,antidomain(antidomain(multiplication(star(sK0),antidomain(antidomain(multiplication(antidomain(antidomain(antidomain(antidomain(sK1)))),one))))))) != antidomain(antidomain(multiplication(star(sK0),antidomain(antidomain(multiplication(antidomain(antidomain(antidomain(antidomain(sK1)))),antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(sK1)))))))))))))),
inference(paramod,[status(thm)],[c_157,c_244]) ).
cnf(c_246,negated_conjecture,
addition(zero,antidomain(antidomain(multiplication(star(sK0),antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sK1)))))))))) != antidomain(antidomain(multiplication(star(sK0),antidomain(antidomain(multiplication(antidomain(antidomain(antidomain(antidomain(sK1)))),antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(sK1)))))))))))))),
inference(paramod,[status(thm)],[c_64,c_245]) ).
cnf(c_247,negated_conjecture,
antidomain(antidomain(multiplication(star(sK0),antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sK1))))))))) != antidomain(antidomain(multiplication(star(sK0),antidomain(antidomain(multiplication(antidomain(antidomain(antidomain(antidomain(sK1)))),antidomain(antidomain(antidomain(multiplication(sK0,antidomain(antidomain(antidomain(antidomain(sK1)))))))))))))),
inference(paramod,[status(thm)],[c_135,c_246]) ).
cnf(c_248,negated_conjecture,
antidomain(antidomain(multiplication(star(sK0),antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sK1))))))))) != antidomain(antidomain(multiplication(star(sK0),antidomain(antidomain(multiplication(antidomain(antidomain(antidomain(antidomain(sK1)))),antidomain(zero))))))),
inference(paramod,[status(thm)],[c_163,c_247]) ).
cnf(c_249,negated_conjecture,
antidomain(antidomain(multiplication(star(sK0),antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sK1))))))))) != antidomain(antidomain(multiplication(star(sK0),antidomain(antidomain(multiplication(antidomain(antidomain(antidomain(antidomain(sK1)))),one)))))),
inference(paramod,[status(thm)],[c_157,c_248]) ).
cnf(c_250,negated_conjecture,
antidomain(antidomain(multiplication(star(sK0),antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sK1))))))))) != antidomain(antidomain(multiplication(star(sK0),antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sK1))))))))),
inference(paramod,[status(thm)],[c_64,c_249]) ).
cnf(c_164,negated_conjecture,
$false,
inference(copy,[status(thm)],[c_250]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : KLE133+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.15/0.42 % Computer : n016.cluster.edu
% 0.15/0.42 % Model : x86_64 x86_64
% 0.15/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.42 % Memory : 8046.5625MB
% 0.15/0.42 % OS : Linux 6.8.0-71-generic
% 0.15/0.42 % CPULimit : 300
% 0.15/0.42 % WCLimit : 300
% 0.15/0.42 % DateTime : Fri Sep 25 19:30:29 UTC 2026
% 0.15/0.42 % CPUTime :
% 0.15/0.43 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.15/0.43 % Process 3101100 was started by sandbox2 on n016,
% 0.15/0.43 % Fri Sep 25 19:30:29 2026
% 0.15/0.43 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.15/0.43
% 0.15/0.43 % From the command line: assign(max_seconds, 300).
% 0.15/0.50
% 0.15/0.50 % SZS status Theorem for theBenchmark
% 0.15/0.50
% 0.15/0.50 % Proof 1 at 0.03 (+ 0.02) seconds.
% 0.15/0.50 % Length of proof is 42.
% 0.15/0.50 % Level of proof is 7.
% 0.15/0.50 % Maximum clause weight is 257.000.
% 0.15/0.50 % Given clauses 33.
% 0.15/0.50
% 0.15/0.50 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------