%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : KLE104-10 : TPTP v9.3.1. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n001.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:19 AM UTC 2026
% Result : Unsatisfiable 175.81s 34.01s
% Output : CNFRefutation 175.81s
% Verified :
% SZS Type : Refutation
% Derivation depth : 69
% Number of leaves : 29
% Syntax : Number of formulae : 344 ( 344 unt; 0 def)
% Number of atoms : 344 ( 343 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 15 ( 15 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 1 avg)
% Maximal term depth : 17 ( 3 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 20 ( 20 usr; 6 con; 0-4 aty)
% Number of variables : 508 ( 60 sgn 48 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(ifeq_axiom,axiom,
! [VAR_0,VAR_1,VAR_2] : ifeq2(VAR_0,VAR_0,VAR_1,VAR_2) = VAR_1,
file('theBenchmark.p',ifeq_axiom) ).
cnf(c_1,plain,
ifeq2(A,A,B,C) = B,
inference(clausify,[status(thm)],[ifeq_axiom]) ).
fof(ifeq_axiom_001,axiom,
! [VAR_0,VAR_1,VAR_2] : ifeq(VAR_0,VAR_0,VAR_1,VAR_2) = VAR_1,
file('theBenchmark.p',ifeq_axiom_001) ).
cnf(c_2,plain,
ifeq(A,A,B,C) = B,
inference(clausify,[status(thm)],[ifeq_axiom_001]) ).
fof(additive_commutativity,axiom,
! [VAR_0,VAR_1] : addition(VAR_0,VAR_1) = addition(VAR_1,VAR_0),
file('theBenchmark.p',additive_commutativity) ).
cnf(c_3,plain,
addition(A,B) = addition(B,A),
inference(clausify,[status(thm)],[additive_commutativity]) ).
fof(additive_associativity,axiom,
! [VAR_0,VAR_1,VAR_2] : addition(VAR_0,addition(VAR_1,VAR_2)) = addition(addition(VAR_0,VAR_1),VAR_2),
file('theBenchmark.p',additive_associativity) ).
cnf(c_4,plain,
addition(A,addition(B,C)) = addition(addition(A,B),C),
inference(clausify,[status(thm)],[additive_associativity]) ).
cnf(c_5,plain,
addition(addition(A,B),C) = addition(A,addition(B,C)),
inference(copy,[status(thm)],[c_4]) ).
fof(additive_identity,axiom,
! [VAR_0] : addition(VAR_0,zero) = VAR_0,
file('theBenchmark.p',additive_identity) ).
cnf(c_6,plain,
addition(A,zero) = A,
inference(clausify,[status(thm)],[additive_identity]) ).
fof(additive_idempotence,axiom,
! [VAR_0] : addition(VAR_0,VAR_0) = VAR_0,
file('theBenchmark.p',additive_idempotence) ).
cnf(c_7,plain,
addition(A,A) = A,
inference(clausify,[status(thm)],[additive_idempotence]) ).
fof(multiplicative_associativity,axiom,
! [VAR_0,VAR_1,VAR_2] : multiplication(VAR_0,multiplication(VAR_1,VAR_2)) = multiplication(multiplication(VAR_0,VAR_1),VAR_2),
file('theBenchmark.p',multiplicative_associativity) ).
cnf(c_8,plain,
multiplication(A,multiplication(B,C)) = multiplication(multiplication(A,B),C),
inference(clausify,[status(thm)],[multiplicative_associativity]) ).
cnf(c_9,plain,
multiplication(multiplication(A,B),C) = multiplication(A,multiplication(B,C)),
inference(copy,[status(thm)],[c_8]) ).
fof(multiplicative_right_identity,axiom,
! [VAR_0] : multiplication(VAR_0,one) = VAR_0,
file('theBenchmark.p',multiplicative_right_identity) ).
cnf(c_10,plain,
multiplication(A,one) = A,
inference(clausify,[status(thm)],[multiplicative_right_identity]) ).
fof(multiplicative_left_identity,axiom,
! [VAR_0] : multiplication(one,VAR_0) = VAR_0,
file('theBenchmark.p',multiplicative_left_identity) ).
cnf(c_11,plain,
multiplication(one,A) = A,
inference(clausify,[status(thm)],[multiplicative_left_identity]) ).
fof(right_distributivity,axiom,
! [VAR_0,VAR_1,VAR_2] : multiplication(VAR_0,addition(VAR_1,VAR_2)) = addition(multiplication(VAR_0,VAR_1),multiplication(VAR_0,VAR_2)),
file('theBenchmark.p',right_distributivity) ).
cnf(c_12,plain,
multiplication(A,addition(B,C)) = addition(multiplication(A,B),multiplication(A,C)),
inference(clausify,[status(thm)],[right_distributivity]) ).
cnf(c_13,plain,
addition(multiplication(A,B),multiplication(A,C)) = multiplication(A,addition(B,C)),
inference(copy,[status(thm)],[c_12]) ).
fof(left_distributivity,axiom,
! [VAR_0,VAR_1,VAR_2] : multiplication(addition(VAR_0,VAR_1),VAR_2) = addition(multiplication(VAR_0,VAR_2),multiplication(VAR_1,VAR_2)),
file('theBenchmark.p',left_distributivity) ).
cnf(c_14,plain,
multiplication(addition(A,B),C) = addition(multiplication(A,C),multiplication(B,C)),
inference(clausify,[status(thm)],[left_distributivity]) ).
cnf(c_15,plain,
addition(multiplication(A,B),multiplication(C,B)) = multiplication(addition(A,C),B),
inference(copy,[status(thm)],[c_14]) ).
fof(left_annihilation,axiom,
! [VAR_0] : multiplication(zero,VAR_0) = zero,
file('theBenchmark.p',left_annihilation) ).
cnf(c_17,plain,
multiplication(zero,A) = zero,
inference(clausify,[status(thm)],[left_annihilation]) ).
fof(order_1,axiom,
! [VAR_0,VAR_1] : ifeq(leq(VAR_0,VAR_1),true,addition(VAR_0,VAR_1),VAR_1) = VAR_1,
file('theBenchmark.p',order_1) ).
cnf(c_18,plain,
ifeq(leq(A,B),true,addition(A,B),B) = B,
inference(clausify,[status(thm)],[order_1]) ).
fof(order,axiom,
! [VAR_0,VAR_1] : ifeq2(addition(VAR_0,VAR_1),VAR_1,leq(VAR_0,VAR_1),true) = true,
file('theBenchmark.p',order) ).
cnf(c_19,plain,
ifeq2(addition(A,B),B,leq(A,B),true) = true,
inference(clausify,[status(thm)],[order]) ).
fof(domain1,axiom,
! [VAR_0] : multiplication(antidomain(VAR_0),VAR_0) = zero,
file('theBenchmark.p',domain1) ).
cnf(c_20,plain,
multiplication(antidomain(A),A) = zero,
inference(clausify,[status(thm)],[domain1]) ).
fof(domain2,axiom,
! [VAR_0,VAR_1] : addition(antidomain(multiplication(VAR_0,VAR_1)),antidomain(multiplication(VAR_0,antidomain(antidomain(VAR_1))))) = antidomain(multiplication(VAR_0,antidomain(antidomain(VAR_1)))),
file('theBenchmark.p',domain2) ).
cnf(c_21,plain,
addition(antidomain(multiplication(A,B)),antidomain(multiplication(A,antidomain(antidomain(B))))) = antidomain(multiplication(A,antidomain(antidomain(B)))),
inference(clausify,[status(thm)],[domain2]) ).
fof(domain3,axiom,
! [VAR_0] : addition(antidomain(antidomain(VAR_0)),antidomain(VAR_0)) = one,
file('theBenchmark.p',domain3) ).
cnf(c_22,plain,
addition(antidomain(antidomain(A)),antidomain(A)) = one,
inference(clausify,[status(thm)],[domain3]) ).
cnf(c_23,plain,
addition(antidomain(A),antidomain(antidomain(A))) = one,
inference(paramod,[status(thm)],[c_3,c_22]) ).
fof(domain4,axiom,
! [VAR_0] : domain(VAR_0) = antidomain(antidomain(VAR_0)),
file('theBenchmark.p',domain4) ).
cnf(c_24,plain,
domain(A) = antidomain(antidomain(A)),
inference(clausify,[status(thm)],[domain4]) ).
fof(codomain1,axiom,
! [VAR_0] : multiplication(VAR_0,coantidomain(VAR_0)) = zero,
file('theBenchmark.p',codomain1) ).
cnf(c_25,plain,
multiplication(A,coantidomain(A)) = zero,
inference(clausify,[status(thm)],[codomain1]) ).
fof(codomain2,axiom,
! [VAR_0,VAR_1] : addition(coantidomain(multiplication(VAR_0,VAR_1)),coantidomain(multiplication(coantidomain(coantidomain(VAR_0)),VAR_1))) = coantidomain(multiplication(coantidomain(coantidomain(VAR_0)),VAR_1)),
file('theBenchmark.p',codomain2) ).
cnf(c_26,plain,
addition(coantidomain(multiplication(A,B)),coantidomain(multiplication(coantidomain(coantidomain(A)),B))) = coantidomain(multiplication(coantidomain(coantidomain(A)),B)),
inference(clausify,[status(thm)],[codomain2]) ).
fof(codomain3,axiom,
! [VAR_0] : addition(coantidomain(coantidomain(VAR_0)),coantidomain(VAR_0)) = one,
file('theBenchmark.p',codomain3) ).
cnf(c_27,plain,
addition(coantidomain(coantidomain(A)),coantidomain(A)) = one,
inference(clausify,[status(thm)],[codomain3]) ).
cnf(c_28,plain,
addition(coantidomain(A),coantidomain(coantidomain(A))) = one,
inference(paramod,[status(thm)],[c_3,c_27]) ).
fof(codomain4,axiom,
! [VAR_0] : codomain(VAR_0) = coantidomain(coantidomain(VAR_0)),
file('theBenchmark.p',codomain4) ).
cnf(c_29,plain,
codomain(A) = coantidomain(coantidomain(A)),
inference(clausify,[status(thm)],[codomain4]) ).
fof(complement,axiom,
! [VAR_0] : c(VAR_0) = antidomain(domain(VAR_0)),
file('theBenchmark.p',complement) ).
cnf(c_30,plain,
c(A) = antidomain(domain(A)),
inference(clausify,[status(thm)],[complement]) ).
cnf(c_31,plain,
c(A) = antidomain(antidomain(antidomain(A))),
inference(paramod,[status(thm)],[c_24,c_30]) ).
fof(forward_diamond,axiom,
! [VAR_0,VAR_1] : forward_diamond(VAR_0,VAR_1) = domain(multiplication(VAR_0,domain(VAR_1))),
file('theBenchmark.p',forward_diamond) ).
cnf(c_34,plain,
forward_diamond(A,B) = domain(multiplication(A,domain(B))),
inference(clausify,[status(thm)],[forward_diamond]) ).
cnf(c_34929,plain,
forward_diamond(A,B) = domain(multiplication(A,antidomain(antidomain(B)))),
inference(paramod,[status(thm)],[c_24,c_34]) ).
cnf(c_35,plain,
forward_diamond(A,B) = antidomain(antidomain(multiplication(A,antidomain(antidomain(B))))),
inference(paramod,[status(thm)],[c_24,c_34929]) ).
fof(backward_diamond,axiom,
! [VAR_0,VAR_1] : backward_diamond(VAR_0,VAR_1) = codomain(multiplication(codomain(VAR_1),VAR_0)),
file('theBenchmark.p',backward_diamond) ).
cnf(c_36,plain,
backward_diamond(A,B) = codomain(multiplication(codomain(B),A)),
inference(clausify,[status(thm)],[backward_diamond]) ).
cnf(c_34930,plain,
backward_diamond(A,B) = codomain(multiplication(coantidomain(coantidomain(B)),A)),
inference(paramod,[status(thm)],[c_29,c_36]) ).
cnf(c_37,plain,
backward_diamond(A,B) = coantidomain(coantidomain(multiplication(coantidomain(coantidomain(B)),A))),
inference(paramod,[status(thm)],[c_29,c_34930]) ).
fof(forward_box,axiom,
! [VAR_0,VAR_1] : forward_box(VAR_0,VAR_1) = c(forward_diamond(VAR_0,c(VAR_1))),
file('theBenchmark.p',forward_box) ).
cnf(c_38,plain,
forward_box(A,B) = c(forward_diamond(A,c(B))),
inference(clausify,[status(thm)],[forward_box]) ).
cnf(c_34931,plain,
forward_box(A,B) = c(forward_diamond(A,antidomain(antidomain(antidomain(B))))),
inference(paramod,[status(thm)],[c_31,c_38]) ).
cnf(c_34932,plain,
forward_box(A,B) = c(antidomain(antidomain(multiplication(A,antidomain(antidomain(antidomain(antidomain(antidomain(B))))))))),
inference(paramod,[status(thm)],[c_35,c_34931]) ).
cnf(c_39,plain,
forward_box(A,B) = antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(A,antidomain(antidomain(antidomain(antidomain(antidomain(B))))))))))),
inference(paramod,[status(thm)],[c_31,c_34932]) ).
fof(backward_box,axiom,
! [VAR_0,VAR_1] : backward_box(VAR_0,VAR_1) = c(backward_diamond(VAR_0,c(VAR_1))),
file('theBenchmark.p',backward_box) ).
cnf(c_40,plain,
backward_box(A,B) = c(backward_diamond(A,c(B))),
inference(clausify,[status(thm)],[backward_box]) ).
cnf(c_34933,plain,
backward_box(A,B) = c(backward_diamond(A,antidomain(antidomain(antidomain(B))))),
inference(paramod,[status(thm)],[c_31,c_40]) ).
cnf(c_34934,plain,
backward_box(A,B) = c(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(B))))),A)))),
inference(paramod,[status(thm)],[c_37,c_34933]) ).
cnf(c_41,plain,
backward_box(A,B) = antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(B))))),A)))))),
inference(paramod,[status(thm)],[c_31,c_34934]) ).
fof(goals,axiom,
addition(domain(sK2_goals_X1),backward_box(sK3_goals_X0,domain(sK1_goals_X2))) = one,
file('theBenchmark.p',goals) ).
cnf(c_42,plain,
addition(domain(sK2_goals_X1),backward_box(sK3_goals_X0,domain(sK1_goals_X2))) = one,
inference(clausify,[status(thm)],[goals]) ).
cnf(c_34935,plain,
addition(antidomain(antidomain(sK2_goals_X1)),backward_box(sK3_goals_X0,domain(sK1_goals_X2))) = one,
inference(paramod,[status(thm)],[c_24,c_42]) ).
cnf(c_34936,plain,
addition(antidomain(antidomain(sK2_goals_X1)),backward_box(sK3_goals_X0,antidomain(antidomain(sK1_goals_X2)))) = one,
inference(paramod,[status(thm)],[c_24,c_34935]) ).
cnf(c_34937,plain,
addition(antidomain(antidomain(sK2_goals_X1)),antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sK1_goals_X2))))))),sK3_goals_X0))))))) = one,
inference(paramod,[status(thm)],[c_41,c_34936]) ).
cnf(c_43,plain,
one = addition(antidomain(antidomain(sK2_goals_X1)),antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sK1_goals_X2))))))),sK3_goals_X0))))))),
inference(copy,[status(thm)],[c_34937]) ).
fof(goals_1,axiom,
addition(forward_box(sK3_goals_X0,domain(sK2_goals_X1)),domain(sK1_goals_X2)) != one,
file('theBenchmark.p',goals_1) ).
cnf(c_44,plain,
addition(forward_box(sK3_goals_X0,domain(sK2_goals_X1)),domain(sK1_goals_X2)) != one,
inference(clausify,[status(thm)],[goals_1]) ).
cnf(c_34938,plain,
addition(forward_box(sK3_goals_X0,antidomain(antidomain(sK2_goals_X1))),domain(sK1_goals_X2)) != one,
inference(paramod,[status(thm)],[c_24,c_44]) ).
cnf(c_34939,plain,
addition(antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK3_goals_X0,antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sK2_goals_X1))))))))))))),domain(sK1_goals_X2)) != one,
inference(paramod,[status(thm)],[c_39,c_34938]) ).
cnf(c_34940,plain,
addition(antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK3_goals_X0,antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sK2_goals_X1))))))))))))),antidomain(antidomain(sK1_goals_X2))) != one,
inference(paramod,[status(thm)],[c_24,c_34939]) ).
cnf(c_34941,plain,
addition(antidomain(antidomain(sK1_goals_X2)),antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK3_goals_X0,antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sK2_goals_X1)))))))))))))) != one,
inference(paramod,[status(thm)],[c_3,c_34940]) ).
cnf(c_34942,plain,
addition(antidomain(antidomain(sK1_goals_X2)),antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK3_goals_X0,antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sK2_goals_X1)))))))))))))) != addition(antidomain(antidomain(sK2_goals_X1)),antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sK1_goals_X2))))))),sK3_goals_X0))))))),
inference(paramod,[status(thm)],[c_43,c_34941]) ).
cnf(c_45,plain,
addition(antidomain(antidomain(sK2_goals_X1)),antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sK1_goals_X2))))))),sK3_goals_X0))))))) != addition(antidomain(antidomain(sK1_goals_X2)),antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK3_goals_X0,antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sK2_goals_X1)))))))))))))),
inference(copy,[status(thm)],[c_34942]) ).
cnf(c_46,plain,
addition(coantidomain(A),coantidomain(coantidomain(A))) = addition(antidomain(antidomain(sK2_goals_X1)),antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sK1_goals_X2))))))),sK3_goals_X0))))))),
inference(paramod,[status(thm)],[c_43,c_28]) ).
cnf(c_34943,plain,
addition(antidomain(A),antidomain(antidomain(A))) = addition(antidomain(antidomain(sK2_goals_X1)),antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sK1_goals_X2))))))),sK3_goals_X0))))))),
inference(paramod,[status(thm)],[c_43,c_23]) ).
cnf(c_47,plain,
addition(antidomain(antidomain(sK2_goals_X1)),antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sK1_goals_X2))))))),sK3_goals_X0))))))) = addition(antidomain(A),antidomain(antidomain(A))),
inference(copy,[status(thm)],[c_34943]) ).
cnf(c_48,plain,
multiplication(addition(antidomain(antidomain(sK2_goals_X1)),antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sK1_goals_X2))))))),sK3_goals_X0))))))),A) = A,
inference(paramod,[status(thm)],[c_43,c_11]) ).
cnf(c_49,plain,
multiplication(A,addition(antidomain(antidomain(sK2_goals_X1)),antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sK1_goals_X2))))))),sK3_goals_X0)))))))) = A,
inference(paramod,[status(thm)],[c_43,c_10]) ).
cnf(c_34944,plain,
addition(addition(A,B),C) = addition(B,addition(A,C)),
inference(paramod,[status(thm)],[c_3,c_5]) ).
cnf(c_51,plain,
addition(A,addition(B,C)) = addition(B,addition(A,C)),
inference(paramod,[status(thm)],[c_5,c_34944]) ).
cnf(c_34945,plain,
A = addition(zero,A),
inference(paramod,[status(thm)],[c_6,c_3]) ).
cnf(c_52,plain,
addition(zero,A) = A,
inference(copy,[status(thm)],[c_34945]) ).
cnf(c_34946,plain,
addition(A,B) = addition(A,addition(A,B)),
inference(paramod,[status(thm)],[c_7,c_5]) ).
cnf(c_53,plain,
addition(A,addition(A,B)) = addition(A,B),
inference(copy,[status(thm)],[c_34946]) ).
cnf(c_56,plain,
addition(multiplication(A,addition(B,C)),D) = addition(multiplication(A,B),addition(multiplication(A,C),D)),
inference(paramod,[status(thm)],[c_13,c_5]) ).
cnf(c_57,plain,
addition(multiplication(addition(A,B),C),D) = addition(multiplication(A,C),addition(multiplication(B,C),D)),
inference(paramod,[status(thm)],[c_15,c_5]) ).
cnf(c_64,plain,
ifeq(leq(multiplication(A,B),multiplication(A,C)),true,multiplication(A,addition(B,C)),multiplication(A,C)) = multiplication(A,C),
inference(paramod,[status(thm)],[c_13,c_18]) ).
cnf(c_34947,plain,
multiplication(zero,A) = multiplication(antidomain(B),multiplication(B,A)),
inference(paramod,[status(thm)],[c_20,c_9]) ).
cnf(c_34948,plain,
zero = multiplication(antidomain(B),multiplication(B,A)),
inference(paramod,[status(thm)],[c_17,c_34947]) ).
cnf(c_72,plain,
multiplication(antidomain(A),multiplication(A,B)) = zero,
inference(copy,[status(thm)],[c_34948]) ).
cnf(c_34949,plain,
addition(zero,multiplication(antidomain(A),B)) = multiplication(antidomain(A),addition(A,B)),
inference(paramod,[status(thm)],[c_20,c_13]) ).
cnf(c_34950,plain,
multiplication(antidomain(A),B) = multiplication(antidomain(A),addition(A,B)),
inference(paramod,[status(thm)],[c_52,c_34949]) ).
cnf(c_73,plain,
multiplication(antidomain(A),addition(A,B)) = multiplication(antidomain(A),B),
inference(copy,[status(thm)],[c_34950]) ).
cnf(c_34951,plain,
addition(multiplication(antidomain(A),B),zero) = multiplication(antidomain(A),addition(B,A)),
inference(paramod,[status(thm)],[c_20,c_13]) ).
cnf(c_34952,plain,
addition(zero,multiplication(antidomain(A),B)) = multiplication(antidomain(A),addition(B,A)),
inference(paramod,[status(thm)],[c_3,c_34951]) ).
cnf(c_34953,plain,
multiplication(antidomain(A),B) = multiplication(antidomain(A),addition(B,A)),
inference(paramod,[status(thm)],[c_52,c_34952]) ).
cnf(c_74,plain,
multiplication(antidomain(A),addition(B,A)) = multiplication(antidomain(A),B),
inference(copy,[status(thm)],[c_34953]) ).
cnf(c_34954,plain,
addition(zero,multiplication(A,B)) = multiplication(addition(antidomain(B),A),B),
inference(paramod,[status(thm)],[c_20,c_15]) ).
cnf(c_34955,plain,
multiplication(A,B) = multiplication(addition(antidomain(B),A),B),
inference(paramod,[status(thm)],[c_52,c_34954]) ).
cnf(c_75,plain,
multiplication(addition(antidomain(A),B),A) = multiplication(B,A),
inference(copy,[status(thm)],[c_34955]) ).
cnf(c_34956,plain,
addition(multiplication(A,B),zero) = multiplication(addition(A,antidomain(B)),B),
inference(paramod,[status(thm)],[c_20,c_15]) ).
cnf(c_34957,plain,
addition(zero,multiplication(A,B)) = multiplication(addition(A,antidomain(B)),B),
inference(paramod,[status(thm)],[c_3,c_34956]) ).
cnf(c_34958,plain,
multiplication(A,B) = multiplication(addition(A,antidomain(B)),B),
inference(paramod,[status(thm)],[c_52,c_34957]) ).
cnf(c_76,plain,
multiplication(addition(A,antidomain(B)),B) = multiplication(A,B),
inference(copy,[status(thm)],[c_34958]) ).
cnf(c_34959,plain,
multiplication(zero,A) = multiplication(B,multiplication(coantidomain(B),A)),
inference(paramod,[status(thm)],[c_25,c_9]) ).
cnf(c_34960,plain,
zero = multiplication(B,multiplication(coantidomain(B),A)),
inference(paramod,[status(thm)],[c_17,c_34959]) ).
cnf(c_85,plain,
multiplication(A,multiplication(coantidomain(A),B)) = zero,
inference(copy,[status(thm)],[c_34960]) ).
cnf(c_34961,plain,
addition(zero,multiplication(A,B)) = multiplication(A,addition(coantidomain(A),B)),
inference(paramod,[status(thm)],[c_25,c_13]) ).
cnf(c_34962,plain,
multiplication(A,B) = multiplication(A,addition(coantidomain(A),B)),
inference(paramod,[status(thm)],[c_52,c_34961]) ).
cnf(c_87,plain,
multiplication(A,addition(coantidomain(A),B)) = multiplication(A,B),
inference(copy,[status(thm)],[c_34962]) ).
cnf(c_34963,plain,
addition(zero,multiplication(A,coantidomain(B))) = multiplication(addition(B,A),coantidomain(B)),
inference(paramod,[status(thm)],[c_25,c_15]) ).
cnf(c_34964,plain,
multiplication(A,coantidomain(B)) = multiplication(addition(B,A),coantidomain(B)),
inference(paramod,[status(thm)],[c_52,c_34963]) ).
cnf(c_89,plain,
multiplication(addition(A,B),coantidomain(A)) = multiplication(B,coantidomain(A)),
inference(copy,[status(thm)],[c_34964]) ).
cnf(c_34965,plain,
addition(multiplication(A,coantidomain(B)),zero) = multiplication(addition(A,B),coantidomain(B)),
inference(paramod,[status(thm)],[c_25,c_15]) ).
cnf(c_34966,plain,
addition(zero,multiplication(A,coantidomain(B))) = multiplication(addition(A,B),coantidomain(B)),
inference(paramod,[status(thm)],[c_3,c_34965]) ).
cnf(c_34967,plain,
multiplication(A,coantidomain(B)) = multiplication(addition(A,B),coantidomain(B)),
inference(paramod,[status(thm)],[c_52,c_34966]) ).
cnf(c_90,plain,
multiplication(addition(A,B),coantidomain(B)) = multiplication(A,coantidomain(B)),
inference(copy,[status(thm)],[c_34967]) ).
cnf(c_91,plain,
addition(antidomain(zero),antidomain(multiplication(A,antidomain(antidomain(coantidomain(A)))))) = antidomain(multiplication(A,antidomain(antidomain(coantidomain(A))))),
inference(paramod,[status(thm)],[c_25,c_21]) ).
cnf(c_98,plain,
addition(coantidomain(zero),coantidomain(multiplication(coantidomain(coantidomain(antidomain(A))),A))) = coantidomain(multiplication(coantidomain(coantidomain(antidomain(A))),A)),
inference(paramod,[status(thm)],[c_20,c_26]) ).
cnf(c_34968,plain,
addition(addition(antidomain(antidomain(sK2_goals_X1)),antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sK1_goals_X2))))))),sK3_goals_X0))))))),A) = addition(coantidomain(B),addition(coantidomain(coantidomain(B)),A)),
inference(paramod,[status(thm)],[c_46,c_5]) ).
cnf(c_34969,plain,
addition(antidomain(antidomain(sK2_goals_X1)),addition(antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sK1_goals_X2))))))),sK3_goals_X0)))))),A)) = addition(coantidomain(B),addition(coantidomain(coantidomain(B)),A)),
inference(paramod,[status(thm)],[c_5,c_34968]) ).
cnf(c_101,plain,
addition(coantidomain(A),addition(coantidomain(coantidomain(A)),B)) = addition(antidomain(antidomain(sK2_goals_X1)),addition(antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sK1_goals_X2))))))),sK3_goals_X0)))))),B)),
inference(copy,[status(thm)],[c_34969]) ).
cnf(c_34970,plain,
addition(addition(antidomain(A),antidomain(antidomain(A))),B) = addition(antidomain(antidomain(sK2_goals_X1)),addition(antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sK1_goals_X2))))))),sK3_goals_X0)))))),B)),
inference(paramod,[status(thm)],[c_47,c_5]) ).
cnf(c_34971,plain,
addition(antidomain(A),addition(antidomain(antidomain(A)),B)) = addition(antidomain(antidomain(sK2_goals_X1)),addition(antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sK1_goals_X2))))))),sK3_goals_X0)))))),B)),
inference(paramod,[status(thm)],[c_5,c_34970]) ).
cnf(c_105,plain,
addition(antidomain(antidomain(sK2_goals_X1)),addition(antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sK1_goals_X2))))))),sK3_goals_X0)))))),A)) = addition(antidomain(B),addition(antidomain(antidomain(B)),A)),
inference(copy,[status(thm)],[c_34971]) ).
cnf(c_34972,plain,
addition(multiplication(antidomain(antidomain(sK2_goals_X1)),A),multiplication(antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sK1_goals_X2))))))),sK3_goals_X0)))))),A)) = multiplication(addition(antidomain(B),antidomain(antidomain(B))),A),
inference(paramod,[status(thm)],[c_47,c_15]) ).
cnf(c_34973,plain,
multiplication(addition(antidomain(antidomain(sK2_goals_X1)),antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sK1_goals_X2))))))),sK3_goals_X0))))))),A) = multiplication(addition(antidomain(B),antidomain(antidomain(B))),A),
inference(paramod,[status(thm)],[c_15,c_34972]) ).
cnf(c_34974,plain,
A = multiplication(addition(antidomain(B),antidomain(antidomain(B))),A),
inference(paramod,[status(thm)],[c_48,c_34973]) ).
cnf(c_109,plain,
multiplication(addition(antidomain(A),antidomain(antidomain(A))),B) = B,
inference(copy,[status(thm)],[c_34974]) ).
cnf(c_119,plain,
coantidomain(addition(antidomain(antidomain(sK2_goals_X1)),antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sK1_goals_X2))))))),sK3_goals_X0)))))))) = zero,
inference(paramod,[status(thm)],[c_48,c_25]) ).
cnf(c_123,plain,
antidomain(addition(antidomain(antidomain(sK2_goals_X1)),antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sK1_goals_X2))))))),sK3_goals_X0)))))))) = zero,
inference(paramod,[status(thm)],[c_49,c_20]) ).
cnf(c_34975,plain,
addition(A,addition(antidomain(B),antidomain(antidomain(B)))) = addition(antidomain(antidomain(sK2_goals_X1)),addition(A,antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sK1_goals_X2))))))),sK3_goals_X0)))))))),
inference(paramod,[status(thm)],[c_47,c_51]) ).
cnf(c_133,plain,
addition(antidomain(antidomain(sK2_goals_X1)),addition(A,antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sK1_goals_X2))))))),sK3_goals_X0)))))))) = addition(A,addition(antidomain(B),antidomain(antidomain(B)))),
inference(copy,[status(thm)],[c_34975]) ).
cnf(c_34976,plain,
ifeq2(A,A,leq(zero,A),true) = true,
inference(paramod,[status(thm)],[c_52,c_19]) ).
cnf(c_136,plain,
leq(zero,A) = true,
inference(paramod,[status(thm)],[c_1,c_34976]) ).
cnf(c_142,plain,
addition(antidomain(zero),antidomain(multiplication(antidomain(A),antidomain(antidomain(multiplication(A,B)))))) = antidomain(multiplication(antidomain(A),antidomain(antidomain(multiplication(A,B))))),
inference(paramod,[status(thm)],[c_72,c_21]) ).
cnf(c_34977,plain,
ifeq2(addition(A,B),addition(A,B),leq(A,addition(A,B)),true) = true,
inference(paramod,[status(thm)],[c_53,c_19]) ).
cnf(c_147,plain,
leq(A,addition(A,B)) = true,
inference(paramod,[status(thm)],[c_1,c_34977]) ).
cnf(c_34978,plain,
addition(coantidomain(A),addition(antidomain(antidomain(sK2_goals_X1)),antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sK1_goals_X2))))))),sK3_goals_X0)))))))) = addition(coantidomain(A),coantidomain(coantidomain(A))),
inference(paramod,[status(thm)],[c_46,c_53]) ).
cnf(c_34979,plain,
addition(antidomain(antidomain(sK2_goals_X1)),addition(coantidomain(A),antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sK1_goals_X2))))))),sK3_goals_X0)))))))) = addition(coantidomain(A),coantidomain(coantidomain(A))),
inference(paramod,[status(thm)],[c_51,c_34978]) ).
cnf(c_148,plain,
addition(antidomain(antidomain(sK2_goals_X1)),addition(coantidomain(A),antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sK1_goals_X2))))))),sK3_goals_X0)))))))) = addition(antidomain(antidomain(sK2_goals_X1)),antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sK1_goals_X2))))))),sK3_goals_X0))))))),
inference(paramod,[status(thm)],[c_46,c_34979]) ).
cnf(c_34980,plain,
addition(antidomain(A),addition(antidomain(antidomain(sK2_goals_X1)),antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sK1_goals_X2))))))),sK3_goals_X0)))))))) = addition(antidomain(A),antidomain(antidomain(A))),
inference(paramod,[status(thm)],[c_47,c_53]) ).
cnf(c_150,plain,
addition(antidomain(A),antidomain(antidomain(A))) = addition(antidomain(A),addition(antidomain(antidomain(sK2_goals_X1)),antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sK1_goals_X2))))))),sK3_goals_X0)))))))),
inference(copy,[status(thm)],[c_34980]) ).
cnf(c_151,plain,
leq(A,addition(B,A)) = true,
inference(paramod,[status(thm)],[c_3,c_147]) ).
cnf(c_159,plain,
leq(A,addition(B,addition(C,A))) = true,
inference(paramod,[status(thm)],[c_5,c_151]) ).
cnf(c_34981,plain,
addition(multiplication(A,addition(antidomain(antidomain(sK2_goals_X1)),antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sK1_goals_X2))))))),sK3_goals_X0)))))))),B) = addition(multiplication(A,coantidomain(C)),addition(multiplication(A,coantidomain(coantidomain(C))),B)),
inference(paramod,[status(thm)],[c_46,c_56]) ).
cnf(c_34982,plain,
addition(A,B) = addition(multiplication(A,coantidomain(C)),addition(multiplication(A,coantidomain(coantidomain(C))),B)),
inference(paramod,[status(thm)],[c_49,c_34981]) ).
cnf(c_185,plain,
addition(multiplication(A,coantidomain(B)),addition(multiplication(A,coantidomain(coantidomain(B))),C)) = addition(A,C),
inference(copy,[status(thm)],[c_34982]) ).
cnf(c_34983,plain,
addition(multiplication(A,addition(antidomain(antidomain(sK2_goals_X1)),antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sK1_goals_X2))))))),sK3_goals_X0)))))))),B) = addition(multiplication(A,antidomain(C)),addition(multiplication(A,antidomain(antidomain(C))),B)),
inference(paramod,[status(thm)],[c_47,c_56]) ).
cnf(c_34984,plain,
addition(A,B) = addition(multiplication(A,antidomain(C)),addition(multiplication(A,antidomain(antidomain(C))),B)),
inference(paramod,[status(thm)],[c_49,c_34983]) ).
cnf(c_187,plain,
addition(multiplication(A,antidomain(B)),addition(multiplication(A,antidomain(antidomain(B))),C)) = addition(A,C),
inference(copy,[status(thm)],[c_34984]) ).
cnf(c_34985,plain,
addition(multiplication(addition(antidomain(antidomain(sK2_goals_X1)),antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sK1_goals_X2))))))),sK3_goals_X0))))))),A),B) = addition(multiplication(antidomain(C),A),addition(multiplication(antidomain(antidomain(C)),A),B)),
inference(paramod,[status(thm)],[c_47,c_57]) ).
cnf(c_34986,plain,
addition(A,B) = addition(multiplication(antidomain(C),A),addition(multiplication(antidomain(antidomain(C)),A),B)),
inference(paramod,[status(thm)],[c_48,c_34985]) ).
cnf(c_214,plain,
addition(multiplication(antidomain(A),B),addition(multiplication(antidomain(antidomain(A)),B),C)) = addition(B,C),
inference(copy,[status(thm)],[c_34986]) ).
cnf(c_34987,plain,
multiplication(addition(antidomain(A),antidomain(antidomain(A))),antidomain(sK2_goals_X1)) = multiplication(antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sK1_goals_X2))))))),sK3_goals_X0)))))),antidomain(sK2_goals_X1)),
inference(paramod,[status(thm)],[c_47,c_75]) ).
cnf(c_34988,plain,
antidomain(sK2_goals_X1) = multiplication(antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sK1_goals_X2))))))),sK3_goals_X0)))))),antidomain(sK2_goals_X1)),
inference(paramod,[status(thm)],[c_109,c_34987]) ).
cnf(c_224,plain,
multiplication(antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sK1_goals_X2))))))),sK3_goals_X0)))))),antidomain(sK2_goals_X1)) = antidomain(sK2_goals_X1),
inference(copy,[status(thm)],[c_34988]) ).
cnf(c_34989,plain,
multiplication(addition(antidomain(antidomain(sK2_goals_X1)),antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sK1_goals_X2))))))),sK3_goals_X0))))))),A) = multiplication(antidomain(antidomain(A)),A),
inference(paramod,[status(thm)],[c_47,c_75]) ).
cnf(c_34990,plain,
A = multiplication(antidomain(antidomain(A)),A),
inference(paramod,[status(thm)],[c_48,c_34989]) ).
cnf(c_225,plain,
multiplication(antidomain(antidomain(A)),A) = A,
inference(copy,[status(thm)],[c_34990]) ).
cnf(c_34991,plain,
addition(antidomain(antidomain(sK2_goals_X1)),antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sK1_goals_X2))))))),sK3_goals_X0))))))) = antidomain(antidomain(addition(antidomain(antidomain(sK2_goals_X1)),antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sK1_goals_X2))))))),sK3_goals_X0))))))))),
inference(paramod,[status(thm)],[c_225,c_49]) ).
cnf(c_235,plain,
addition(antidomain(antidomain(sK2_goals_X1)),antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sK1_goals_X2))))))),sK3_goals_X0))))))) = antidomain(zero),
inference(paramod,[status(thm)],[c_123,c_34991]) ).
cnf(c_244,plain,
addition(antidomain(A),antidomain(antidomain(A))) = addition(antidomain(A),antidomain(zero)),
inference(paramod,[status(thm)],[c_235,c_150]) ).
cnf(c_246,plain,
addition(antidomain(antidomain(sK2_goals_X1)),addition(coantidomain(A),antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sK1_goals_X2))))))),sK3_goals_X0)))))))) = antidomain(zero),
inference(paramod,[status(thm)],[c_235,c_148]) ).
cnf(c_251,plain,
coantidomain(antidomain(zero)) = zero,
inference(paramod,[status(thm)],[c_235,c_119]) ).
cnf(c_259,plain,
multiplication(A,antidomain(zero)) = A,
inference(paramod,[status(thm)],[c_235,c_49]) ).
cnf(c_260,plain,
multiplication(antidomain(zero),A) = A,
inference(paramod,[status(thm)],[c_235,c_48]) ).
cnf(c_34992,plain,
antidomain(zero) = addition(antidomain(A),antidomain(antidomain(A))),
inference(paramod,[status(thm)],[c_235,c_47]) ).
cnf(c_34993,plain,
antidomain(zero) = addition(antidomain(A),antidomain(zero)),
inference(paramod,[status(thm)],[c_244,c_34992]) ).
cnf(c_261,plain,
addition(antidomain(A),antidomain(zero)) = antidomain(zero),
inference(copy,[status(thm)],[c_34993]) ).
cnf(c_262,plain,
addition(coantidomain(A),coantidomain(coantidomain(A))) = antidomain(zero),
inference(paramod,[status(thm)],[c_235,c_46]) ).
cnf(c_34994,plain,
antidomain(zero) != addition(antidomain(antidomain(sK1_goals_X2)),antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK3_goals_X0,antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sK2_goals_X1)))))))))))))),
inference(paramod,[status(thm)],[c_235,c_45]) ).
cnf(c_263,plain,
addition(antidomain(antidomain(sK1_goals_X2)),antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK3_goals_X0,antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sK2_goals_X1)))))))))))))) != antidomain(zero),
inference(copy,[status(thm)],[c_34994]) ).
cnf(c_34995,plain,
addition(antidomain(antidomain(sK2_goals_X1)),addition(A,antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sK1_goals_X2))))))),sK3_goals_X0)))))))) = addition(A,addition(antidomain(B),antidomain(zero))),
inference(paramod,[status(thm)],[c_244,c_133]) ).
cnf(c_267,plain,
addition(antidomain(antidomain(sK2_goals_X1)),addition(A,antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sK1_goals_X2))))))),sK3_goals_X0)))))))) = addition(A,antidomain(zero)),
inference(paramod,[status(thm)],[c_261,c_34995]) ).
cnf(c_271,plain,
addition(antidomain(A),antidomain(antidomain(A))) = antidomain(zero),
inference(paramod,[status(thm)],[c_261,c_244]) ).
cnf(c_34996,plain,
addition(coantidomain(A),antidomain(zero)) = antidomain(zero),
inference(paramod,[status(thm)],[c_267,c_246]) ).
cnf(c_272,plain,
addition(antidomain(zero),coantidomain(A)) = antidomain(zero),
inference(paramod,[status(thm)],[c_3,c_34996]) ).
cnf(c_34997,plain,
antidomain(zero) = addition(antidomain(zero),antidomain(A)),
inference(paramod,[status(thm)],[c_261,c_3]) ).
cnf(c_321,plain,
addition(antidomain(zero),antidomain(A)) = antidomain(zero),
inference(copy,[status(thm)],[c_34997]) ).
cnf(c_34998,plain,
addition(multiplication(A,antidomain(B)),multiplication(A,antidomain(zero))) = multiplication(A,antidomain(zero)),
inference(paramod,[status(thm)],[c_261,c_13]) ).
cnf(c_34999,plain,
addition(multiplication(A,antidomain(B)),A) = multiplication(A,antidomain(zero)),
inference(paramod,[status(thm)],[c_259,c_34998]) ).
cnf(c_35000,plain,
addition(A,multiplication(A,antidomain(B))) = multiplication(A,antidomain(zero)),
inference(paramod,[status(thm)],[c_3,c_34999]) ).
cnf(c_324,plain,
addition(A,multiplication(A,antidomain(B))) = A,
inference(paramod,[status(thm)],[c_259,c_35000]) ).
cnf(c_35001,plain,
addition(multiplication(antidomain(A),B),multiplication(antidomain(zero),B)) = multiplication(antidomain(zero),B),
inference(paramod,[status(thm)],[c_261,c_15]) ).
cnf(c_35002,plain,
addition(multiplication(antidomain(A),B),B) = multiplication(antidomain(zero),B),
inference(paramod,[status(thm)],[c_260,c_35001]) ).
cnf(c_35003,plain,
addition(B,multiplication(antidomain(A),B)) = multiplication(antidomain(zero),B),
inference(paramod,[status(thm)],[c_3,c_35002]) ).
cnf(c_325,plain,
addition(A,multiplication(antidomain(B),A)) = A,
inference(paramod,[status(thm)],[c_260,c_35003]) ).
cnf(c_35004,plain,
antidomain(zero) = antidomain(multiplication(antidomain(A),antidomain(antidomain(multiplication(A,B))))),
inference(paramod,[status(thm)],[c_321,c_142]) ).
cnf(c_330,plain,
antidomain(multiplication(antidomain(A),antidomain(antidomain(multiplication(A,B))))) = antidomain(zero),
inference(copy,[status(thm)],[c_35004]) ).
cnf(c_35005,plain,
antidomain(zero) = antidomain(multiplication(A,antidomain(antidomain(coantidomain(A))))),
inference(paramod,[status(thm)],[c_321,c_91]) ).
cnf(c_331,plain,
antidomain(multiplication(A,antidomain(antidomain(coantidomain(A))))) = antidomain(zero),
inference(copy,[status(thm)],[c_35005]) ).
cnf(c_35006,plain,
addition(multiplication(A,antidomain(zero)),multiplication(A,coantidomain(B))) = multiplication(A,antidomain(zero)),
inference(paramod,[status(thm)],[c_272,c_13]) ).
cnf(c_35007,plain,
addition(A,multiplication(A,coantidomain(B))) = multiplication(A,antidomain(zero)),
inference(paramod,[status(thm)],[c_259,c_35006]) ).
cnf(c_334,plain,
addition(A,multiplication(A,coantidomain(B))) = A,
inference(paramod,[status(thm)],[c_259,c_35007]) ).
cnf(c_35008,plain,
addition(multiplication(antidomain(zero),A),multiplication(coantidomain(B),A)) = multiplication(antidomain(zero),A),
inference(paramod,[status(thm)],[c_272,c_15]) ).
cnf(c_35009,plain,
addition(A,multiplication(coantidomain(B),A)) = multiplication(antidomain(zero),A),
inference(paramod,[status(thm)],[c_260,c_35008]) ).
cnf(c_335,plain,
addition(A,multiplication(coantidomain(B),A)) = A,
inference(paramod,[status(thm)],[c_260,c_35009]) ).
cnf(c_35010,plain,
multiplication(antidomain(A),A) = multiplication(multiplication(antidomain(A),antidomain(B)),A),
inference(paramod,[status(thm)],[c_324,c_75]) ).
cnf(c_35011,plain,
zero = multiplication(multiplication(antidomain(A),antidomain(B)),A),
inference(paramod,[status(thm)],[c_20,c_35010]) ).
cnf(c_35012,plain,
zero = multiplication(antidomain(A),multiplication(antidomain(B),A)),
inference(paramod,[status(thm)],[c_9,c_35011]) ).
cnf(c_364,plain,
multiplication(antidomain(A),multiplication(antidomain(B),A)) = zero,
inference(copy,[status(thm)],[c_35012]) ).
cnf(c_370,plain,
leq(multiplication(antidomain(A),B),B) = true,
inference(paramod,[status(thm)],[c_325,c_151]) ).
cnf(c_414,plain,
leq(multiplication(coantidomain(A),B),addition(C,B)) = true,
inference(paramod,[status(thm)],[c_335,c_159]) ).
cnf(c_35013,plain,
addition(antidomain(zero),A) = addition(coantidomain(B),addition(coantidomain(coantidomain(B)),A)),
inference(paramod,[status(thm)],[c_262,c_5]) ).
cnf(c_449,plain,
addition(coantidomain(A),addition(coantidomain(coantidomain(A)),B)) = addition(antidomain(zero),B),
inference(copy,[status(thm)],[c_35013]) ).
cnf(c_35014,plain,
addition(zero,coantidomain(coantidomain(antidomain(zero)))) = antidomain(zero),
inference(paramod,[status(thm)],[c_251,c_262]) ).
cnf(c_35015,plain,
addition(zero,coantidomain(zero)) = antidomain(zero),
inference(paramod,[status(thm)],[c_251,c_35014]) ).
cnf(c_450,plain,
coantidomain(zero) = antidomain(zero),
inference(paramod,[status(thm)],[c_52,c_35015]) ).
cnf(c_35016,plain,
addition(antidomain(zero),B) = addition(antidomain(antidomain(sK2_goals_X1)),addition(antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sK1_goals_X2))))))),sK3_goals_X0)))))),B)),
inference(paramod,[status(thm)],[c_449,c_101]) ).
cnf(c_454,plain,
addition(antidomain(antidomain(sK2_goals_X1)),addition(antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(antidomain(antidomain(sK1_goals_X2))))))),sK3_goals_X0)))))),A)) = addition(antidomain(zero),A),
inference(copy,[status(thm)],[c_35016]) ).
cnf(c_35017,plain,
addition(antidomain(zero),coantidomain(multiplication(coantidomain(coantidomain(antidomain(A))),A))) = coantidomain(multiplication(coantidomain(coantidomain(antidomain(A))),A)),
inference(paramod,[status(thm)],[c_450,c_98]) ).
cnf(c_35018,plain,
antidomain(zero) = coantidomain(multiplication(coantidomain(coantidomain(antidomain(A))),A)),
inference(paramod,[status(thm)],[c_272,c_35017]) ).
cnf(c_459,plain,
coantidomain(multiplication(coantidomain(coantidomain(antidomain(A))),A)) = antidomain(zero),
inference(copy,[status(thm)],[c_35018]) ).
cnf(c_35019,plain,
addition(antidomain(zero),A) = addition(antidomain(B),addition(antidomain(antidomain(B)),A)),
inference(paramod,[status(thm)],[c_454,c_105]) ).
cnf(c_460,plain,
addition(antidomain(A),addition(antidomain(antidomain(A)),B)) = addition(antidomain(zero),B),
inference(copy,[status(thm)],[c_35019]) ).
cnf(c_35020,plain,
ifeq(leq(multiplication(A,antidomain(B)),multiplication(A,antidomain(antidomain(B)))),true,multiplication(A,antidomain(zero)),multiplication(A,antidomain(antidomain(B)))) = multiplication(A,antidomain(antidomain(B))),
inference(paramod,[status(thm)],[c_271,c_64]) ).
cnf(c_475,plain,
ifeq(leq(multiplication(A,antidomain(B)),multiplication(A,antidomain(antidomain(B)))),true,A,multiplication(A,antidomain(antidomain(B)))) = multiplication(A,antidomain(antidomain(B))),
inference(paramod,[status(thm)],[c_259,c_35020]) ).
cnf(c_35021,plain,
addition(multiplication(A,multiplication(antidomain(B),C)),zero) = multiplication(addition(A,antidomain(C)),multiplication(antidomain(B),C)),
inference(paramod,[status(thm)],[c_364,c_15]) ).
cnf(c_35022,plain,
addition(zero,multiplication(A,multiplication(antidomain(B),C))) = multiplication(addition(A,antidomain(C)),multiplication(antidomain(B),C)),
inference(paramod,[status(thm)],[c_3,c_35021]) ).
cnf(c_35023,plain,
multiplication(A,multiplication(antidomain(B),C)) = multiplication(addition(A,antidomain(C)),multiplication(antidomain(B),C)),
inference(paramod,[status(thm)],[c_52,c_35022]) ).
cnf(c_481,plain,
multiplication(addition(A,antidomain(B)),multiplication(antidomain(C),B)) = multiplication(A,multiplication(antidomain(C),B)),
inference(copy,[status(thm)],[c_35023]) ).
cnf(c_35024,plain,
multiplication(antidomain(multiplication(A,antidomain(antidomain(B)))),multiplication(A,antidomain(antidomain(B)))) = multiplication(antidomain(multiplication(A,B)),multiplication(A,antidomain(antidomain(B)))),
inference(paramod,[status(thm)],[c_21,c_76]) ).
cnf(c_35025,plain,
zero = multiplication(antidomain(multiplication(A,B)),multiplication(A,antidomain(antidomain(B)))),
inference(paramod,[status(thm)],[c_20,c_35024]) ).
cnf(c_547,plain,
multiplication(antidomain(multiplication(A,B)),multiplication(A,antidomain(antidomain(B)))) = zero,
inference(copy,[status(thm)],[c_35025]) ).
cnf(c_35026,plain,
multiplication(A,antidomain(zero)) = multiplication(A,coantidomain(coantidomain(A))),
inference(paramod,[status(thm)],[c_262,c_87]) ).
cnf(c_35027,plain,
A = multiplication(A,coantidomain(coantidomain(A))),
inference(paramod,[status(thm)],[c_259,c_35026]) ).
cnf(c_601,plain,
multiplication(A,coantidomain(coantidomain(A))) = A,
inference(copy,[status(thm)],[c_35027]) ).
cnf(c_35028,plain,
multiplication(antidomain(coantidomain(A)),antidomain(zero)) = multiplication(antidomain(coantidomain(A)),coantidomain(coantidomain(A))),
inference(paramod,[status(thm)],[c_262,c_73]) ).
cnf(c_35029,plain,
antidomain(coantidomain(A)) = multiplication(antidomain(coantidomain(A)),coantidomain(coantidomain(A))),
inference(paramod,[status(thm)],[c_259,c_35028]) ).
cnf(c_771,plain,
multiplication(antidomain(coantidomain(A)),coantidomain(coantidomain(A))) = antidomain(coantidomain(A)),
inference(copy,[status(thm)],[c_35029]) ).
cnf(c_35030,plain,
multiplication(antidomain(zero),multiplication(A,antidomain(antidomain(coantidomain(A))))) = zero,
inference(paramod,[status(thm)],[c_331,c_20]) ).
cnf(c_807,plain,
multiplication(A,antidomain(antidomain(coantidomain(A)))) = zero,
inference(paramod,[status(thm)],[c_260,c_35030]) ).
cnf(c_35031,plain,
multiplication(antidomain(antidomain(antidomain(A))),antidomain(zero)) = multiplication(antidomain(antidomain(antidomain(A))),antidomain(A)),
inference(paramod,[status(thm)],[c_271,c_74]) ).
cnf(c_35032,plain,
antidomain(antidomain(antidomain(A))) = multiplication(antidomain(antidomain(antidomain(A))),antidomain(A)),
inference(paramod,[status(thm)],[c_259,c_35031]) ).
cnf(c_842,plain,
antidomain(antidomain(antidomain(A))) = antidomain(A),
inference(paramod,[status(thm)],[c_225,c_35032]) ).
cnf(c_35033,plain,
addition(antidomain(antidomain(sK1_goals_X2)),antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK3_goals_X0,antidomain(antidomain(antidomain(antidomain(antidomain(sK2_goals_X1)))))))))))) != antidomain(zero),
inference(paramod,[status(thm)],[c_842,c_263]) ).
cnf(c_35034,plain,
addition(antidomain(antidomain(sK1_goals_X2)),antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK3_goals_X0,antidomain(antidomain(antidomain(sK2_goals_X1)))))))))) != antidomain(zero),
inference(paramod,[status(thm)],[c_842,c_35033]) ).
cnf(c_35035,plain,
addition(antidomain(antidomain(sK1_goals_X2)),antidomain(antidomain(antidomain(antidomain(antidomain(multiplication(sK3_goals_X0,antidomain(sK2_goals_X1)))))))) != antidomain(zero),
inference(paramod,[status(thm)],[c_842,c_35034]) ).
cnf(c_35036,plain,
addition(antidomain(antidomain(sK1_goals_X2)),antidomain(antidomain(antidomain(multiplication(sK3_goals_X0,antidomain(sK2_goals_X1)))))) != antidomain(zero),
inference(paramod,[status(thm)],[c_842,c_35035]) ).
cnf(c_852,plain,
addition(antidomain(antidomain(sK1_goals_X2)),antidomain(multiplication(sK3_goals_X0,antidomain(sK2_goals_X1)))) != antidomain(zero),
inference(paramod,[status(thm)],[c_842,c_35036]) ).
cnf(c_35037,plain,
multiplication(antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(antidomain(antidomain(sK1_goals_X2))))),sK3_goals_X0)))))),antidomain(sK2_goals_X1)) = antidomain(sK2_goals_X1),
inference(paramod,[status(thm)],[c_842,c_224]) ).
cnf(c_35038,plain,
multiplication(antidomain(antidomain(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(sK1_goals_X2))),sK3_goals_X0)))))),antidomain(sK2_goals_X1)) = antidomain(sK2_goals_X1),
inference(paramod,[status(thm)],[c_842,c_35037]) ).
cnf(c_854,plain,
multiplication(antidomain(coantidomain(coantidomain(multiplication(coantidomain(coantidomain(antidomain(sK1_goals_X2))),sK3_goals_X0)))),antidomain(sK2_goals_X1)) = antidomain(sK2_goals_X1),
inference(paramod,[status(thm)],[c_842,c_35038]) ).
cnf(c_1068,plain,
leq(multiplication(coantidomain(A),multiplication(antidomain(B),C)),C) = true,
inference(paramod,[status(thm)],[c_325,c_414]) ).
cnf(c_35039,plain,
multiplication(multiplication(coantidomain(coantidomain(antidomain(A))),A),antidomain(zero)) = zero,
inference(paramod,[status(thm)],[c_459,c_25]) ).
cnf(c_1072,plain,
multiplication(coantidomain(coantidomain(antidomain(A))),A) = zero,
inference(paramod,[status(thm)],[c_259,c_35039]) ).
cnf(c_35040,plain,
multiplication(antidomain(zero),coantidomain(antidomain(A))) = multiplication(antidomain(antidomain(A)),coantidomain(antidomain(A))),
inference(paramod,[status(thm)],[c_271,c_89]) ).
cnf(c_35041,plain,
coantidomain(antidomain(A)) = multiplication(antidomain(antidomain(A)),coantidomain(antidomain(A))),
inference(paramod,[status(thm)],[c_260,c_35040]) ).
cnf(c_1152,plain,
multiplication(antidomain(antidomain(A)),coantidomain(antidomain(A))) = coantidomain(antidomain(A)),
inference(copy,[status(thm)],[c_35041]) ).
cnf(c_35042,plain,
multiplication(antidomain(zero),coantidomain(coantidomain(coantidomain(A)))) = multiplication(coantidomain(A),coantidomain(coantidomain(coantidomain(A)))),
inference(paramod,[status(thm)],[c_262,c_90]) ).
cnf(c_35043,plain,
coantidomain(coantidomain(coantidomain(A))) = multiplication(coantidomain(A),coantidomain(coantidomain(coantidomain(A)))),
inference(paramod,[status(thm)],[c_260,c_35042]) ).
cnf(c_1222,plain,
coantidomain(coantidomain(coantidomain(A))) = coantidomain(A),
inference(paramod,[status(thm)],[c_601,c_35043]) ).
cnf(c_2656,plain,
leq(antidomain(coantidomain(A)),coantidomain(coantidomain(A))) = true,
inference(paramod,[status(thm)],[c_771,c_370]) ).
cnf(c_2714,plain,
leq(antidomain(coantidomain(coantidomain(A))),coantidomain(A)) = true,
inference(paramod,[status(thm)],[c_1222,c_2656]) ).
cnf(c_35044,plain,
ifeq(true,true,addition(antidomain(coantidomain(coantidomain(A))),coantidomain(A)),coantidomain(A)) = coantidomain(A),
inference(paramod,[status(thm)],[c_2714,c_18]) ).
cnf(c_35045,plain,
ifeq(true,true,addition(coantidomain(A),antidomain(coantidomain(coantidomain(A)))),coantidomain(A)) = coantidomain(A),
inference(paramod,[status(thm)],[c_3,c_35044]) ).
cnf(c_2715,plain,
addition(coantidomain(A),antidomain(coantidomain(coantidomain(A)))) = coantidomain(A),
inference(paramod,[status(thm)],[c_2,c_35045]) ).
cnf(c_35046,plain,
ifeq(true,true,addition(multiplication(coantidomain(A),multiplication(antidomain(B),C)),C),C) = C,
inference(paramod,[status(thm)],[c_1068,c_18]) ).
cnf(c_35047,plain,
ifeq(true,true,addition(C,multiplication(coantidomain(A),multiplication(antidomain(B),C))),C) = C,
inference(paramod,[status(thm)],[c_3,c_35046]) ).
cnf(c_3036,plain,
addition(A,multiplication(coantidomain(B),multiplication(antidomain(C),A))) = A,
inference(paramod,[status(thm)],[c_2,c_35047]) ).
cnf(c_3101,plain,
addition(antidomain(antidomain(A)),coantidomain(antidomain(A))) = antidomain(antidomain(A)),
inference(paramod,[status(thm)],[c_1152,c_334]) ).
cnf(c_35048,plain,
addition(multiplication(antidomain(antidomain(coantidomain(coantidomain(A)))),coantidomain(A)),addition(coantidomain(coantidomain(A)),B)) = addition(antidomain(antidomain(coantidomain(coantidomain(A)))),B),
inference(paramod,[status(thm)],[c_225,c_185]) ).
cnf(c_4636,plain,
addition(coantidomain(coantidomain(A)),addition(multiplication(antidomain(antidomain(coantidomain(coantidomain(A)))),coantidomain(A)),B)) = addition(antidomain(antidomain(coantidomain(coantidomain(A)))),B),
inference(paramod,[status(thm)],[c_51,c_35048]) ).
cnf(c_35049,plain,
addition(zero,addition(multiplication(A,antidomain(antidomain(antidomain(coantidomain(A))))),B)) = addition(A,B),
inference(paramod,[status(thm)],[c_807,c_187]) ).
cnf(c_35050,plain,
addition(zero,addition(multiplication(A,antidomain(coantidomain(A))),B)) = addition(A,B),
inference(paramod,[status(thm)],[c_842,c_35049]) ).
cnf(c_4793,plain,
addition(multiplication(A,antidomain(coantidomain(A))),B) = addition(A,B),
inference(paramod,[status(thm)],[c_52,c_35050]) ).
cnf(c_5339,plain,
addition(coantidomain(coantidomain(A)),multiplication(coantidomain(B),antidomain(coantidomain(A)))) = coantidomain(coantidomain(A)),
inference(paramod,[status(thm)],[c_771,c_3036]) ).
cnf(c_35051,plain,
addition(A,zero) = multiplication(A,antidomain(coantidomain(A))),
inference(paramod,[status(thm)],[c_4793,c_6]) ).
cnf(c_35052,plain,
A = multiplication(A,antidomain(coantidomain(A))),
inference(paramod,[status(thm)],[c_6,c_35051]) ).
cnf(c_6362,plain,
multiplication(A,antidomain(coantidomain(A))) = A,
inference(copy,[status(thm)],[c_35052]) ).
cnf(c_35053,plain,
multiplication(A,B) = multiplication(A,multiplication(B,antidomain(coantidomain(multiplication(A,B))))),
inference(paramod,[status(thm)],[c_6362,c_9]) ).
cnf(c_6374,plain,
multiplication(A,multiplication(B,antidomain(coantidomain(multiplication(A,B))))) = multiplication(A,B),
inference(copy,[status(thm)],[c_35053]) ).
cnf(c_35054,plain,
addition(antidomain(coantidomain(coantidomain(A))),coantidomain(A)) = antidomain(coantidomain(coantidomain(A))),
inference(paramod,[status(thm)],[c_6362,c_335]) ).
cnf(c_35055,plain,
addition(coantidomain(A),antidomain(coantidomain(coantidomain(A)))) = antidomain(coantidomain(coantidomain(A))),
inference(paramod,[status(thm)],[c_3,c_35054]) ).
cnf(c_35056,plain,
coantidomain(A) = antidomain(coantidomain(coantidomain(A))),
inference(paramod,[status(thm)],[c_2715,c_35055]) ).
cnf(c_6381,plain,
antidomain(coantidomain(coantidomain(A))) = coantidomain(A),
inference(copy,[status(thm)],[c_35056]) ).
cnf(c_35057,plain,
addition(coantidomain(coantidomain(A)),addition(multiplication(antidomain(coantidomain(A)),coantidomain(A)),B)) = addition(antidomain(antidomain(coantidomain(coantidomain(A)))),B),
inference(paramod,[status(thm)],[c_6381,c_4636]) ).
cnf(c_35058,plain,
addition(coantidomain(coantidomain(A)),addition(zero,B)) = addition(antidomain(antidomain(coantidomain(coantidomain(A)))),B),
inference(paramod,[status(thm)],[c_20,c_35057]) ).
cnf(c_35059,plain,
addition(coantidomain(coantidomain(A)),B) = addition(antidomain(antidomain(coantidomain(coantidomain(A)))),B),
inference(paramod,[status(thm)],[c_52,c_35058]) ).
cnf(c_6418,plain,
addition(coantidomain(coantidomain(A)),B) = addition(antidomain(coantidomain(A)),B),
inference(paramod,[status(thm)],[c_6381,c_35059]) ).
cnf(c_6422,plain,
multiplication(coantidomain(multiplication(coantidomain(coantidomain(antidomain(sK1_goals_X2))),sK3_goals_X0)),antidomain(sK2_goals_X1)) = antidomain(sK2_goals_X1),
inference(paramod,[status(thm)],[c_6381,c_854]) ).
cnf(c_35060,plain,
addition(antidomain(coantidomain(A)),multiplication(coantidomain(B),antidomain(coantidomain(A)))) = coantidomain(coantidomain(A)),
inference(paramod,[status(thm)],[c_6418,c_5339]) ).
cnf(c_35061,plain,
antidomain(coantidomain(A)) = coantidomain(coantidomain(A)),
inference(paramod,[status(thm)],[c_335,c_35060]) ).
cnf(c_6453,plain,
coantidomain(coantidomain(A)) = antidomain(coantidomain(A)),
inference(copy,[status(thm)],[c_35061]) ).
cnf(c_6508,plain,
multiplication(coantidomain(multiplication(antidomain(coantidomain(antidomain(sK1_goals_X2))),sK3_goals_X0)),antidomain(sK2_goals_X1)) = antidomain(sK2_goals_X1),
inference(paramod,[status(thm)],[c_6453,c_6422]) ).
cnf(c_6513,plain,
antidomain(antidomain(coantidomain(A))) = coantidomain(A),
inference(paramod,[status(thm)],[c_6453,c_6381]) ).
cnf(c_7283,plain,
multiplication(antidomain(coantidomain(antidomain(A))),A) = zero,
inference(paramod,[status(thm)],[c_6453,c_1072]) ).
cnf(c_35062,plain,
addition(zero,addition(multiplication(antidomain(antidomain(coantidomain(antidomain(A)))),A),B)) = addition(A,B),
inference(paramod,[status(thm)],[c_7283,c_214]) ).
cnf(c_35063,plain,
addition(zero,addition(multiplication(coantidomain(antidomain(A)),A),B)) = addition(A,B),
inference(paramod,[status(thm)],[c_6513,c_35062]) ).
cnf(c_8345,plain,
addition(multiplication(coantidomain(antidomain(A)),A),B) = addition(A,B),
inference(paramod,[status(thm)],[c_52,c_35063]) ).
cnf(c_35064,plain,
addition(multiplication(coantidomain(antidomain(antidomain(antidomain(A)))),antidomain(antidomain(A))),coantidomain(antidomain(A))) = antidomain(antidomain(A)),
inference(paramod,[status(thm)],[c_3101,c_8345]) ).
cnf(c_35065,plain,
addition(multiplication(coantidomain(antidomain(A)),antidomain(antidomain(A))),coantidomain(antidomain(A))) = antidomain(antidomain(A)),
inference(paramod,[status(thm)],[c_842,c_35064]) ).
cnf(c_35066,plain,
addition(coantidomain(antidomain(A)),multiplication(coantidomain(antidomain(A)),antidomain(antidomain(A)))) = antidomain(antidomain(A)),
inference(paramod,[status(thm)],[c_3,c_35065]) ).
cnf(c_8566,plain,
coantidomain(antidomain(A)) = antidomain(antidomain(A)),
inference(paramod,[status(thm)],[c_324,c_35066]) ).
cnf(c_35067,plain,
multiplication(coantidomain(multiplication(antidomain(antidomain(antidomain(sK1_goals_X2))),sK3_goals_X0)),antidomain(sK2_goals_X1)) = antidomain(sK2_goals_X1),
inference(paramod,[status(thm)],[c_8566,c_6508]) ).
cnf(c_8577,plain,
multiplication(coantidomain(multiplication(antidomain(sK1_goals_X2),sK3_goals_X0)),antidomain(sK2_goals_X1)) = antidomain(sK2_goals_X1),
inference(paramod,[status(thm)],[c_842,c_35067]) ).
cnf(c_35068,plain,
multiplication(multiplication(antidomain(sK1_goals_X2),sK3_goals_X0),antidomain(sK2_goals_X1)) = zero,
inference(paramod,[status(thm)],[c_8577,c_85]) ).
cnf(c_8660,plain,
multiplication(antidomain(sK1_goals_X2),multiplication(sK3_goals_X0,antidomain(sK2_goals_X1))) = zero,
inference(paramod,[status(thm)],[c_9,c_35068]) ).
cnf(c_35069,plain,
multiplication(antidomain(zero),multiplication(antidomain(A),antidomain(antidomain(multiplication(A,B))))) = zero,
inference(paramod,[status(thm)],[c_330,c_20]) ).
cnf(c_10684,plain,
multiplication(antidomain(A),antidomain(antidomain(multiplication(A,B)))) = zero,
inference(paramod,[status(thm)],[c_260,c_35069]) ).
cnf(c_35070,plain,
multiplication(antidomain(zero),multiplication(antidomain(sK1_goals_X2),antidomain(antidomain(multiplication(sK3_goals_X0,antidomain(sK2_goals_X1)))))) = zero,
inference(paramod,[status(thm)],[c_8660,c_547]) ).
cnf(c_11741,plain,
multiplication(antidomain(sK1_goals_X2),antidomain(antidomain(multiplication(sK3_goals_X0,antidomain(sK2_goals_X1))))) = zero,
inference(paramod,[status(thm)],[c_260,c_35070]) ).
cnf(c_35071,plain,
ifeq(leq(zero,multiplication(antidomain(A),antidomain(antidomain(antidomain(multiplication(A,B)))))),true,antidomain(A),multiplication(antidomain(A),antidomain(antidomain(antidomain(multiplication(A,B)))))) = multiplication(antidomain(A),antidomain(antidomain(antidomain(multiplication(A,B))))),
inference(paramod,[status(thm)],[c_10684,c_475]) ).
cnf(c_35072,plain,
ifeq(leq(zero,multiplication(antidomain(A),antidomain(multiplication(A,B)))),true,antidomain(A),multiplication(antidomain(A),antidomain(antidomain(antidomain(multiplication(A,B)))))) = multiplication(antidomain(A),antidomain(antidomain(antidomain(multiplication(A,B))))),
inference(paramod,[status(thm)],[c_842,c_35071]) ).
cnf(c_35073,plain,
ifeq(true,true,antidomain(A),multiplication(antidomain(A),antidomain(antidomain(antidomain(multiplication(A,B)))))) = multiplication(antidomain(A),antidomain(antidomain(antidomain(multiplication(A,B))))),
inference(paramod,[status(thm)],[c_136,c_35072]) ).
cnf(c_35074,plain,
ifeq(true,true,antidomain(A),multiplication(antidomain(A),antidomain(multiplication(A,B)))) = multiplication(antidomain(A),antidomain(antidomain(antidomain(multiplication(A,B))))),
inference(paramod,[status(thm)],[c_842,c_35073]) ).
cnf(c_35075,plain,
antidomain(A) = multiplication(antidomain(A),antidomain(antidomain(antidomain(multiplication(A,B))))),
inference(paramod,[status(thm)],[c_2,c_35074]) ).
cnf(c_35076,plain,
antidomain(A) = multiplication(antidomain(A),antidomain(multiplication(A,B))),
inference(paramod,[status(thm)],[c_842,c_35075]) ).
cnf(c_29394,plain,
multiplication(antidomain(A),antidomain(multiplication(A,B))) = antidomain(A),
inference(copy,[status(thm)],[c_35076]) ).
cnf(c_35077,plain,
ifeq(leq(zero,multiplication(antidomain(sK1_goals_X2),antidomain(antidomain(antidomain(multiplication(sK3_goals_X0,antidomain(sK2_goals_X1))))))),true,antidomain(sK1_goals_X2),multiplication(antidomain(sK1_goals_X2),antidomain(antidomain(antidomain(multiplication(sK3_goals_X0,antidomain(sK2_goals_X1))))))) = multiplication(antidomain(sK1_goals_X2),antidomain(antidomain(antidomain(multiplication(sK3_goals_X0,antidomain(sK2_goals_X1)))))),
inference(paramod,[status(thm)],[c_11741,c_475]) ).
cnf(c_35078,plain,
ifeq(leq(zero,multiplication(antidomain(sK1_goals_X2),antidomain(multiplication(sK3_goals_X0,antidomain(sK2_goals_X1))))),true,antidomain(sK1_goals_X2),multiplication(antidomain(sK1_goals_X2),antidomain(antidomain(antidomain(multiplication(sK3_goals_X0,antidomain(sK2_goals_X1))))))) = multiplication(antidomain(sK1_goals_X2),antidomain(antidomain(antidomain(multiplication(sK3_goals_X0,antidomain(sK2_goals_X1)))))),
inference(paramod,[status(thm)],[c_842,c_35077]) ).
cnf(c_35079,plain,
ifeq(true,true,antidomain(sK1_goals_X2),multiplication(antidomain(sK1_goals_X2),antidomain(antidomain(antidomain(multiplication(sK3_goals_X0,antidomain(sK2_goals_X1))))))) = multiplication(antidomain(sK1_goals_X2),antidomain(antidomain(antidomain(multiplication(sK3_goals_X0,antidomain(sK2_goals_X1)))))),
inference(paramod,[status(thm)],[c_136,c_35078]) ).
cnf(c_35080,plain,
ifeq(true,true,antidomain(sK1_goals_X2),multiplication(antidomain(sK1_goals_X2),antidomain(multiplication(sK3_goals_X0,antidomain(sK2_goals_X1))))) = multiplication(antidomain(sK1_goals_X2),antidomain(antidomain(antidomain(multiplication(sK3_goals_X0,antidomain(sK2_goals_X1)))))),
inference(paramod,[status(thm)],[c_842,c_35079]) ).
cnf(c_35081,plain,
antidomain(sK1_goals_X2) = multiplication(antidomain(sK1_goals_X2),antidomain(antidomain(antidomain(multiplication(sK3_goals_X0,antidomain(sK2_goals_X1)))))),
inference(paramod,[status(thm)],[c_2,c_35080]) ).
cnf(c_35082,plain,
antidomain(sK1_goals_X2) = multiplication(antidomain(sK1_goals_X2),antidomain(multiplication(sK3_goals_X0,antidomain(sK2_goals_X1)))),
inference(paramod,[status(thm)],[c_842,c_35081]) ).
cnf(c_29401,plain,
multiplication(antidomain(sK1_goals_X2),antidomain(multiplication(sK3_goals_X0,antidomain(sK2_goals_X1)))) = antidomain(sK1_goals_X2),
inference(copy,[status(thm)],[c_35082]) ).
cnf(c_35083,plain,
addition(antidomain(multiplication(A,B)),antidomain(A)) = antidomain(multiplication(A,B)),
inference(paramod,[status(thm)],[c_29394,c_325]) ).
cnf(c_29530,plain,
addition(antidomain(A),antidomain(multiplication(A,B))) = antidomain(multiplication(A,B)),
inference(paramod,[status(thm)],[c_3,c_35083]) ).
cnf(c_35084,plain,
multiplication(antidomain(zero),multiplication(antidomain(A),antidomain(B))) = multiplication(antidomain(B),multiplication(antidomain(A),antidomain(B))),
inference(paramod,[status(thm)],[c_271,c_481]) ).
cnf(c_35085,plain,
multiplication(antidomain(A),antidomain(B)) = multiplication(antidomain(B),multiplication(antidomain(A),antidomain(B))),
inference(paramod,[status(thm)],[c_260,c_35084]) ).
cnf(c_30628,plain,
multiplication(antidomain(A),multiplication(antidomain(B),antidomain(A))) = multiplication(antidomain(B),antidomain(A)),
inference(copy,[status(thm)],[c_35085]) ).
cnf(c_35086,plain,
multiplication(antidomain(sK1_goals_X2),multiplication(antidomain(multiplication(sK3_goals_X0,antidomain(sK2_goals_X1))),antidomain(coantidomain(antidomain(sK1_goals_X2))))) = multiplication(antidomain(sK1_goals_X2),antidomain(multiplication(sK3_goals_X0,antidomain(sK2_goals_X1)))),
inference(paramod,[status(thm)],[c_29401,c_6374]) ).
cnf(c_35087,plain,
multiplication(antidomain(sK1_goals_X2),multiplication(antidomain(multiplication(sK3_goals_X0,antidomain(sK2_goals_X1))),antidomain(antidomain(antidomain(sK1_goals_X2))))) = multiplication(antidomain(sK1_goals_X2),antidomain(multiplication(sK3_goals_X0,antidomain(sK2_goals_X1)))),
inference(paramod,[status(thm)],[c_8566,c_35086]) ).
cnf(c_35088,plain,
multiplication(antidomain(sK1_goals_X2),multiplication(antidomain(multiplication(sK3_goals_X0,antidomain(sK2_goals_X1))),antidomain(sK1_goals_X2))) = multiplication(antidomain(sK1_goals_X2),antidomain(multiplication(sK3_goals_X0,antidomain(sK2_goals_X1)))),
inference(paramod,[status(thm)],[c_842,c_35087]) ).
cnf(c_35089,plain,
multiplication(antidomain(multiplication(sK3_goals_X0,antidomain(sK2_goals_X1))),antidomain(sK1_goals_X2)) = multiplication(antidomain(sK1_goals_X2),antidomain(multiplication(sK3_goals_X0,antidomain(sK2_goals_X1)))),
inference(paramod,[status(thm)],[c_30628,c_35088]) ).
cnf(c_31414,plain,
multiplication(antidomain(multiplication(sK3_goals_X0,antidomain(sK2_goals_X1))),antidomain(sK1_goals_X2)) = antidomain(sK1_goals_X2),
inference(paramod,[status(thm)],[c_29401,c_35089]) ).
cnf(c_35090,plain,
addition(antidomain(A),antidomain(multiplication(antidomain(A),B))) = addition(antidomain(zero),antidomain(multiplication(antidomain(A),B))),
inference(paramod,[status(thm)],[c_29530,c_460]) ).
cnf(c_34862,plain,
addition(antidomain(A),antidomain(multiplication(antidomain(A),B))) = antidomain(zero),
inference(paramod,[status(thm)],[c_321,c_35090]) ).
cnf(c_35091,plain,
addition(antidomain(multiplication(sK3_goals_X0,antidomain(sK2_goals_X1))),antidomain(antidomain(sK1_goals_X2))) = antidomain(zero),
inference(paramod,[status(thm)],[c_31414,c_34862]) ).
cnf(c_34927,plain,
addition(antidomain(antidomain(sK1_goals_X2)),antidomain(multiplication(sK3_goals_X0,antidomain(sK2_goals_X1)))) = antidomain(zero),
inference(paramod,[status(thm)],[c_3,c_35091]) ).
cnf(c_34928,plain,
$false,
inference(resolve,[status(thm)],[c_34927,c_852]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : KLE104-10 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/10.36 % Computer : n001.cluster.edu
% 0.10/10.36 % Model : x86_64 x86_64
% 0.10/10.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/10.36 % Memory : 8046.5625MB
% 0.10/10.36 % OS : Linux 6.8.0-71-generic
% 0.10/10.36 % CPULimit : 300
% 0.10/10.36 % WCLimit : 300
% 0.10/10.36 % DateTime : Fri Sep 25 19:27:52 UTC 2026
% 0.10/10.37 % CPUTime :
% 0.10/10.37 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.10/10.37 % Process 4029598 was started by sandbox on n001,
% 0.10/10.37 % Fri Sep 25 19:27:52 2026
% 0.10/10.37 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.10/10.37
% 0.10/10.37 % From the command line: assign(max_seconds, 300).
% 175.81/34.01
% 175.81/34.01 % given #500 (A,wt=17): 287 multiplication(addition(multiplication(antidomain(antidomain(multiplication(A,B))),A),C),B) = multiplication(addition(A,C),B). [para(225(a,1),58(a,1,1)),rewrite([15(3)]),flip(a)].
% 175.81/34.01
% 175.81/34.01 % given #1000 (A,wt=16): 481 multiplication(addition(A,antidomain(B)),multiplication(antidomain(C),B)) = multiplication(A,multiplication(antidomain(C),B)). [para(364(a,1),15(a,1,2)),rewrite([3(5),52(5)]),flip(a)].
% 175.81/34.01
% 175.81/34.01 % SZS status Unsatisfiable for theBenchmark
% 175.81/34.01
% 175.81/34.01 % Proof 1 at 17.95 (+ 4.96) seconds.
% 175.81/34.01 % Length of proof is 152.
% 175.81/34.01 % Level of proof is 26.
% 175.81/34.01 % Maximum clause weight is 42.000.
% 175.81/34.01 % Given clauses 1179.
% 175.81/34.01
% 175.81/34.01 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------