%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : KLE102+1 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n020.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 01:51:37 PM UTC 2026
% Result : Theorem 158.43s 20.76s
% Output : Proof 158.43s
% Verified :
% SZS Type : Refutation
% Derivation depth : 163
% Number of leaves : 28
% Syntax : Number of formulae : 1002 ( 993 unt; 0 def)
% Number of atoms : 1015 (1007 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 26 ( 13 ~; 6 |; 4 &)
% ( 1 <=>; 0 =>; 2 <=; 0 <~>)
% Maximal formula depth : 6 ( 1 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 19 ( 19 usr; 6 con; 0-4 aty)
% Number of variables : 1461 ( 110 sgn 135 !; 3 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f22,axiom,
! [X0,X1] : forward_diamond(X0,X1) = domain(multiplication(X0,domain(X1))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',forward_diamond) ).
fof(f22_nnf,plain,
! [X0,X1] : forward_diamond(X0,X1) = domain(multiplication(X0,domain(X1))),
inference(nnf_transformation,[status(thm)],[f22]) ).
fof(f22_sk,plain,
! [X0,X1] : forward_diamond(X0,X1) = domain(multiplication(X0,domain(X1))),
inference(skolemisation,[status(esa)],[f22_nnf]) ).
cnf(c23,plain,
forward_diamond(X0,X1) = domain(multiplication(X0,domain(X1))),
inference(cnf_transformation,[status(esa)],[f22_sk]) ).
cnf(t21,plain,
domain(multiplication(X1,domain(X2))) = forward_diamond(X1,X2),
inference(equality_encoding,[status(esa)],[c23]) ).
cnf(t183,plain,
domain(multiplication(X1,domain(X2))) = forward_diamond(X1,X2),
inference(orient,[status(thm)],[t21]) ).
fof(f15,axiom,
! [X0] : domain(X0) = antidomain(antidomain(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',domain4) ).
fof(f15_nnf,plain,
! [X0] : domain(X0) = antidomain(antidomain(X0)),
inference(nnf_transformation,[status(thm)],[f15]) ).
fof(f15_sk,plain,
! [X0] : domain(X0) = antidomain(antidomain(X0)),
inference(skolemisation,[status(esa)],[f15_nnf]) ).
cnf(c16,plain,
domain(X0) = antidomain(antidomain(X0)),
inference(cnf_transformation,[status(esa)],[f15_sk]) ).
cnf(t9,plain,
antidomain(antidomain(X1)) = domain(X1),
inference(equality_encoding,[status(esa)],[c16]) ).
cnf(t99,plain,
antidomain(antidomain(X1)) = domain(X1),
inference(orient,[status(thm)],[t9]) ).
cnf(t100,plain,
domain(antidomain(X1)) = antidomain(domain(X1)),
inference(cp,[status(thm)],[t99,t99]) ).
fof(f20,axiom,
! [X0] : c(X0) = antidomain(domain(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',complement) ).
fof(f20_nnf,plain,
! [X0] : c(X0) = antidomain(domain(X0)),
inference(nnf_transformation,[status(thm)],[f20]) ).
fof(f20_sk,plain,
! [X0] : c(X0) = antidomain(domain(X0)),
inference(skolemisation,[status(esa)],[f20_nnf]) ).
cnf(c21,plain,
c(X0) = antidomain(domain(X0)),
inference(cnf_transformation,[status(esa)],[f20_sk]) ).
cnf(t10,plain,
antidomain(domain(X1)) = c(X1),
inference(equality_encoding,[status(esa)],[c21]) ).
cnf(t104,plain,
antidomain(domain(X1)) = c(X1),
inference(orient,[status(thm)],[t10]) ).
cnf(t190391,plain,
domain(antidomain(X1)) = c(X1),
inference(step,[status(thm)],[t100,t104]) ).
cnf(t252,plain,
domain(antidomain(X1)) = c(X1),
inference(orient,[status(thm)],[t190391]) ).
cnf(t258,plain,
forward_diamond(X1,antidomain(X2)) = domain(multiplication(X1,c(X2))),
inference(cp,[status(thm)],[t183,t252]) ).
cnf(t1066,plain,
domain(multiplication(X1,c(X2))) = forward_diamond(X1,antidomain(X2)),
inference(orient,[status(thm)],[t258]) ).
fof(f7,axiom,
! [A,B,C] : multiplication(A,addition(B,C)) = addition(multiplication(A,B),multiplication(A,C)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',right_distributivity) ).
fof(f7_nnf,plain,
! [A,B,C] : multiplication(A,addition(B,C)) = addition(multiplication(A,B),multiplication(A,C)),
inference(nnf_transformation,[status(thm)],[f7]) ).
fof(f7_sk,plain,
! [A,B,C] : multiplication(A,addition(B,C)) = addition(multiplication(A,B),multiplication(A,C)),
inference(skolemisation,[status(esa)],[f7_nnf]) ).
cnf(c7,plain,
multiplication(X0,addition(X1,X2)) = addition(multiplication(X0,X1),multiplication(X0,X2)),
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
cnf(t28,plain,
addition(multiplication(X1,X2),multiplication(X1,X3)) = multiplication(X1,addition(X2,X3)),
inference(equality_encoding,[status(esa)],[c7]) ).
cnf(t43,plain,
addition(multiplication(X1,X2),multiplication(X1,X3)) = multiplication(X1,addition(X2,X3)),
inference(orient,[status(thm)],[t28]) ).
fof(f12,axiom,
! [X0] : multiplication(antidomain(X0),X0) = zero,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',domain1) ).
fof(f12_nnf,plain,
! [X0] : multiplication(antidomain(X0),X0) = zero,
inference(nnf_transformation,[status(thm)],[f12]) ).
fof(f12_sk,plain,
! [X0] : multiplication(antidomain(X0),X0) = zero,
inference(skolemisation,[status(esa)],[f12_nnf]) ).
cnf(c13,plain,
multiplication(antidomain(X0),X0) = zero,
inference(cnf_transformation,[status(esa)],[f12_sk]) ).
cnf(t13,plain,
multiplication(antidomain(X1),X1) = zero,
inference(equality_encoding,[status(esa)],[c13]) ).
cnf(t56,plain,
multiplication(antidomain(X1),X1) = zero,
inference(orient,[status(thm)],[t13]) ).
cnf(t58,plain,
multiplication(antidomain(X1),addition(X1,X2)) = addition(zero,multiplication(antidomain(X1),X2)),
inference(cp,[status(thm)],[t43,t56]) ).
fof(f0,axiom,
! [A,B] : addition(A,B) = addition(B,A),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',additive_commutativity) ).
fof(f0_nnf,plain,
! [A,B] : addition(A,B) = addition(B,A),
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
! [A,B] : addition(A,B) = addition(B,A),
inference(skolemisation,[status(esa)],[f0_nnf]) ).
cnf(c0,plain,
addition(X0,X1) = addition(X1,X0),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(t14,plain,
addition(X1,X2) = addition(X2,X1),
inference(equality_encoding,[status(esa)],[c0]) ).
cnf(t108,plain,
addition(X1,X2) = addition(X2,X1),
inference(orient,[status(thm)],[t14]) ).
fof(f2,axiom,
! [A] : addition(A,zero) = A,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',additive_identity) ).
fof(f2_nnf,plain,
! [A] : addition(A,zero) = A,
inference(nnf_transformation,[status(thm)],[f2]) ).
fof(f2_sk,plain,
! [A] : addition(A,zero) = A,
inference(skolemisation,[status(esa)],[f2_nnf]) ).
cnf(c2,plain,
addition(X0,zero) = X0,
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(t1,plain,
addition(X1,zero) = X1,
inference(equality_encoding,[status(esa)],[c2]) ).
cnf(t37,plain,
addition(X1,zero) = X1,
inference(orient,[status(thm)],[t1]) ).
cnf(t109,plain,
addition(zero,X1) = X1,
inference(cp,[status(thm)],[t108,t37]) ).
cnf(t233,plain,
addition(zero,X1) = X1,
inference(orient,[status(thm)],[t109]) ).
cnf(t190629,plain,
multiplication(antidomain(X1),addition(X1,X2)) = multiplication(antidomain(X1),X2),
inference(step,[status(thm)],[t58,t233]) ).
cnf(t3411,plain,
multiplication(antidomain(X1),addition(X1,X2)) = multiplication(antidomain(X1),X2),
inference(orient,[status(thm)],[t190629]) ).
fof(f14,axiom,
! [X0] : addition(antidomain(antidomain(X0)),antidomain(X0)) = one,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',domain3) ).
fof(f14_nnf,plain,
! [X0] : addition(antidomain(antidomain(X0)),antidomain(X0)) = one,
inference(nnf_transformation,[status(thm)],[f14]) ).
fof(f14_sk,plain,
! [X0] : addition(antidomain(antidomain(X0)),antidomain(X0)) = one,
inference(skolemisation,[status(esa)],[f14_nnf]) ).
cnf(c15,plain,
addition(antidomain(antidomain(X0)),antidomain(X0)) = one,
inference(cnf_transformation,[status(esa)],[f14_sk]) ).
cnf(t16,plain,
addition(antidomain(antidomain(X1)),antidomain(X1)) = one,
inference(equality_encoding,[status(esa)],[c15]) ).
cnf(t190366,plain,
addition(antidomain(X1),antidomain(antidomain(X1))) = one,
inference(step,[status(thm)],[t16,t108]) ).
cnf(t190367,plain,
addition(antidomain(X1),domain(X1)) = one,
inference(step,[status(thm)],[t190366,t99]) ).
cnf(t190368,plain,
addition(domain(X1),antidomain(X1)) = one,
inference(step,[status(thm)],[t190367,t108]) ).
cnf(t122,plain,
addition(domain(X1),antidomain(X1)) = one,
inference(orient,[status(thm)],[t190368]) ).
cnf(t3427,plain,
multiplication(antidomain(domain(X1)),antidomain(X1)) = multiplication(antidomain(domain(X1)),one),
inference(cp,[status(thm)],[t3411,t122]) ).
cnf(t190630,plain,
multiplication(c(X1),antidomain(X1)) = multiplication(antidomain(domain(X1)),one),
inference(step,[status(thm)],[t3427,t104]) ).
fof(f21,axiom,
! [X0,X1] : domain_difference(X0,X1) = multiplication(domain(X0),antidomain(X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',domain_difference) ).
fof(f21_nnf,plain,
! [X0,X1] : domain_difference(X0,X1) = multiplication(domain(X0),antidomain(X1)),
inference(nnf_transformation,[status(thm)],[f21]) ).
fof(f21_sk,plain,
! [X0,X1] : domain_difference(X0,X1) = multiplication(domain(X0),antidomain(X1)),
inference(skolemisation,[status(esa)],[f21_nnf]) ).
cnf(c22,plain,
domain_difference(X0,X1) = multiplication(domain(X0),antidomain(X1)),
inference(cnf_transformation,[status(esa)],[f21_sk]) ).
cnf(t22,plain,
multiplication(domain(X1),antidomain(X2)) = domain_difference(X1,X2),
inference(equality_encoding,[status(esa)],[c22]) ).
cnf(t73,plain,
multiplication(domain(X1),antidomain(X2)) = domain_difference(X1,X2),
inference(orient,[status(thm)],[t22]) ).
cnf(t257,plain,
domain_difference(antidomain(X1),X2) = multiplication(c(X1),antidomain(X2)),
inference(cp,[status(thm)],[t73,t252]) ).
cnf(t1041,plain,
multiplication(c(X1),antidomain(X2)) = domain_difference(antidomain(X1),X2),
inference(orient,[status(thm)],[t257]) ).
cnf(t190631,plain,
domain_difference(antidomain(X1),X1) = multiplication(antidomain(domain(X1)),one),
inference(step,[status(thm)],[t190630,t1041]) ).
fof(f8,axiom,
! [A,B,C] : multiplication(addition(A,B),C) = addition(multiplication(A,C),multiplication(B,C)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',left_distributivity) ).
fof(f8_nnf,plain,
! [A,B,C] : multiplication(addition(A,B),C) = addition(multiplication(A,C),multiplication(B,C)),
inference(nnf_transformation,[status(thm)],[f8]) ).
fof(f8_sk,plain,
! [A,B,C] : multiplication(addition(A,B),C) = addition(multiplication(A,C),multiplication(B,C)),
inference(skolemisation,[status(esa)],[f8_nnf]) ).
cnf(c8,plain,
multiplication(addition(X0,X1),X2) = addition(multiplication(X0,X2),multiplication(X1,X2)),
inference(cnf_transformation,[status(esa)],[f8_sk]) ).
cnf(t29,plain,
addition(multiplication(X1,X2),multiplication(X3,X2)) = multiplication(addition(X1,X3),X2),
inference(equality_encoding,[status(esa)],[c8]) ).
cnf(t61,plain,
addition(multiplication(X1,X2),multiplication(X3,X2)) = multiplication(addition(X1,X3),X2),
inference(orient,[status(thm)],[t29]) ).
cnf(t67,plain,
multiplication(addition(X1,antidomain(X2)),X2) = addition(multiplication(X1,X2),zero),
inference(cp,[status(thm)],[t61,t56]) ).
cnf(t190545,plain,
multiplication(addition(X1,antidomain(X2)),X2) = multiplication(X1,X2),
inference(step,[status(thm)],[t67,t37]) ).
cnf(t2006,plain,
multiplication(addition(X1,antidomain(X2)),X2) = multiplication(X1,X2),
inference(orient,[status(thm)],[t190545]) ).
cnf(t2007,plain,
multiplication(domain(X1),X1) = multiplication(one,X1),
inference(cp,[status(thm)],[t2006,t122]) ).
fof(f6,axiom,
! [A] : multiplication(one,A) = A,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',multiplicative_left_identity) ).
fof(f6_nnf,plain,
! [A] : multiplication(one,A) = A,
inference(nnf_transformation,[status(thm)],[f6]) ).
fof(f6_sk,plain,
! [A] : multiplication(one,A) = A,
inference(skolemisation,[status(esa)],[f6_nnf]) ).
cnf(c6,plain,
multiplication(one,X0) = X0,
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(t7,plain,
multiplication(one,X1) = X1,
inference(equality_encoding,[status(esa)],[c6]) ).
cnf(t35,plain,
multiplication(one,X1) = X1,
inference(orient,[status(thm)],[t7]) ).
cnf(t190546,plain,
multiplication(domain(X1),X1) = X1,
inference(step,[status(thm)],[t2007,t35]) ).
cnf(t2038,plain,
multiplication(domain(X1),X1) = X1,
inference(orient,[status(thm)],[t190546]) ).
cnf(t2040,plain,
antidomain(X1) = domain_difference(antidomain(X1),X1),
inference(cp,[status(thm)],[t2038,t73]) ).
cnf(t2114,plain,
domain_difference(antidomain(X1),X1) = antidomain(X1),
inference(orient,[status(thm)],[t2040]) ).
cnf(t190632,plain,
antidomain(X1) = multiplication(antidomain(domain(X1)),one),
inference(step,[status(thm)],[t190631,t2114]) ).
fof(f5,axiom,
! [A] : multiplication(A,one) = A,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',multiplicative_right_identity) ).
fof(f5_nnf,plain,
! [A] : multiplication(A,one) = A,
inference(nnf_transformation,[status(thm)],[f5]) ).
fof(f5_sk,plain,
! [A] : multiplication(A,one) = A,
inference(skolemisation,[status(esa)],[f5_nnf]) ).
cnf(c5,plain,
multiplication(X0,one) = X0,
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(t5,plain,
multiplication(X1,one) = X1,
inference(equality_encoding,[status(esa)],[c5]) ).
cnf(t34,plain,
multiplication(X1,one) = X1,
inference(orient,[status(thm)],[t5]) ).
cnf(t190633,plain,
antidomain(X1) = antidomain(domain(X1)),
inference(step,[status(thm)],[t190632,t34]) ).
cnf(t190634,plain,
antidomain(X1) = c(X1),
inference(step,[status(thm)],[t190633,t104]) ).
cnf(t3443,plain,
antidomain(X1) = c(X1),
inference(orient,[status(thm)],[t190634]) ).
cnf(t190641,plain,
domain(multiplication(X1,c(X2))) = forward_diamond(X1,c(X2)),
inference(step,[status(thm)],[t1066,t3443]) ).
cnf(t3450,plain,
domain(multiplication(X1,c(X2))) = forward_diamond(X1,c(X2)),
inference(orient,[status(thm)],[t190641]) ).
cnf(t190681,plain,
c(antidomain(X1)) = domain(X1),
inference(step,[status(thm)],[t99,t3443]) ).
cnf(t190682,plain,
c(c(X1)) = domain(X1),
inference(step,[status(thm)],[t190681,t3443]) ).
cnf(t3481,plain,
c(c(X1)) = domain(X1),
inference(rw,[status(thm)],[t190682]) ).
cnf(t3510,plain,
c(c(X1)) = domain(X1),
inference(orient,[status(thm)],[t3481]) ).
cnf(t3540,plain,
forward_diamond(X1,c(c(X2))) = domain(multiplication(X1,domain(X2))),
inference(cp,[status(thm)],[t3450,t3510]) ).
cnf(t190762,plain,
forward_diamond(X1,domain(X2)) = domain(multiplication(X1,domain(X2))),
inference(step,[status(thm)],[t3540,t3510]) ).
cnf(t190763,plain,
forward_diamond(X1,domain(X2)) = forward_diamond(X1,X2),
inference(step,[status(thm)],[t190762,t183]) ).
cnf(t3645,plain,
forward_diamond(X1,domain(X2)) = forward_diamond(X1,X2),
inference(orient,[status(thm)],[t190763]) ).
fof(f16,axiom,
! [X0] : multiplication(X0,coantidomain(X0)) = zero,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',codomain1) ).
fof(f16_nnf,plain,
! [X0] : multiplication(X0,coantidomain(X0)) = zero,
inference(nnf_transformation,[status(thm)],[f16]) ).
fof(f16_sk,plain,
! [X0] : multiplication(X0,coantidomain(X0)) = zero,
inference(skolemisation,[status(esa)],[f16_nnf]) ).
cnf(c17,plain,
multiplication(X0,coantidomain(X0)) = zero,
inference(cnf_transformation,[status(esa)],[f16_sk]) ).
cnf(t12,plain,
multiplication(X1,coantidomain(X1)) = zero,
inference(equality_encoding,[status(esa)],[c17]) ).
cnf(t47,plain,
multiplication(X1,coantidomain(X1)) = zero,
inference(orient,[status(thm)],[t12]) ).
cnf(t66,plain,
multiplication(addition(X1,X2),coantidomain(X2)) = addition(multiplication(X1,coantidomain(X2)),zero),
inference(cp,[status(thm)],[t61,t47]) ).
cnf(t190878,plain,
multiplication(addition(X1,X2),coantidomain(X2)) = multiplication(X1,coantidomain(X2)),
inference(step,[status(thm)],[t66,t37]) ).
cnf(t5898,plain,
multiplication(addition(X1,X2),coantidomain(X2)) = multiplication(X1,coantidomain(X2)),
inference(orient,[status(thm)],[t190878]) ).
fof(f1,axiom,
! [C,B,A] : addition(A,addition(B,C)) = addition(addition(A,B),C),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',additive_associativity) ).
fof(f1_nnf,plain,
! [C,B,A] : addition(A,addition(B,C)) = addition(addition(A,B),C),
inference(nnf_transformation,[status(thm)],[f1]) ).
fof(f1_sk,plain,
! [A,B,C] : addition(A,addition(B,C)) = addition(addition(A,B),C),
inference(skolemisation,[status(esa)],[f1_nnf]) ).
cnf(c1,plain,
addition(X2,addition(X1,X0)) = addition(addition(X2,X1),X0),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(t24,plain,
addition(addition(X1,X2),X3) = addition(X1,addition(X2,X3)),
inference(equality_encoding,[status(esa)],[c1]) ).
cnf(t113,plain,
addition(addition(X1,X2),X3) = addition(X1,addition(X2,X3)),
inference(orient,[status(thm)],[t24]) ).
fof(f3,axiom,
! [A] : addition(A,A) = A,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',additive_idempotence) ).
fof(f3_nnf,plain,
! [A] : addition(A,A) = A,
inference(nnf_transformation,[status(thm)],[f3]) ).
fof(f3_sk,plain,
! [A] : addition(A,A) = A,
inference(skolemisation,[status(esa)],[f3_nnf]) ).
cnf(c3,plain,
addition(X0,X0) = X0,
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(t0,plain,
addition(X1,X1) = X1,
inference(equality_encoding,[status(esa)],[c3]) ).
cnf(t36,plain,
addition(X1,X1) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t116,plain,
addition(X1,addition(X1,X2)) = addition(X1,X2),
inference(cp,[status(thm)],[t113,t36]) ).
cnf(t622,plain,
addition(X1,addition(X1,X2)) = addition(X1,X2),
inference(orient,[status(thm)],[t116]) ).
cnf(t5899,plain,
multiplication(X1,coantidomain(addition(X1,X2))) = multiplication(addition(X1,X2),coantidomain(addition(X1,X2))),
inference(cp,[status(thm)],[t5898,t622]) ).
cnf(t190879,plain,
multiplication(X1,coantidomain(addition(X1,X2))) = zero,
inference(step,[status(thm)],[t5899,t47]) ).
cnf(t5936,plain,
multiplication(X1,coantidomain(addition(X1,X2))) = zero,
inference(orient,[status(thm)],[t190879]) ).
cnf(t5949,plain,
multiplication(X1,addition(X2,coantidomain(addition(X1,X3)))) = addition(multiplication(X1,X2),zero),
inference(cp,[status(thm)],[t43,t5936]) ).
cnf(t194166,plain,
multiplication(X1,addition(X2,coantidomain(addition(X1,X3)))) = multiplication(X1,X2),
inference(step,[status(thm)],[t5949,t37]) ).
cnf(t147904,plain,
multiplication(X1,addition(X2,coantidomain(addition(X1,X3)))) = multiplication(X1,X2),
inference(orient,[status(thm)],[t194166]) ).
fof(f18,axiom,
! [X0] : addition(coantidomain(coantidomain(X0)),coantidomain(X0)) = one,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',codomain3) ).
fof(f18_nnf,plain,
! [X0] : addition(coantidomain(coantidomain(X0)),coantidomain(X0)) = one,
inference(nnf_transformation,[status(thm)],[f18]) ).
fof(f18_sk,plain,
! [X0] : addition(coantidomain(coantidomain(X0)),coantidomain(X0)) = one,
inference(skolemisation,[status(esa)],[f18_nnf]) ).
cnf(c19,plain,
addition(coantidomain(coantidomain(X0)),coantidomain(X0)) = one,
inference(cnf_transformation,[status(esa)],[f18_sk]) ).
cnf(t17,plain,
addition(coantidomain(coantidomain(X1)),coantidomain(X1)) = one,
inference(equality_encoding,[status(esa)],[c19]) ).
cnf(t190369,plain,
addition(coantidomain(X1),coantidomain(coantidomain(X1))) = one,
inference(step,[status(thm)],[t17,t108]) ).
cnf(t140,plain,
addition(coantidomain(X1),coantidomain(coantidomain(X1))) = one,
inference(orient,[status(thm)],[t190369]) ).
fof(f19,axiom,
! [X0] : codomain(X0) = coantidomain(coantidomain(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',codomain4) ).
fof(f19_nnf,plain,
! [X0] : codomain(X0) = coantidomain(coantidomain(X0)),
inference(nnf_transformation,[status(thm)],[f19]) ).
fof(f19_sk,plain,
! [X0] : codomain(X0) = coantidomain(coantidomain(X0)),
inference(skolemisation,[status(esa)],[f19_nnf]) ).
cnf(c20,plain,
codomain(X0) = coantidomain(coantidomain(X0)),
inference(cnf_transformation,[status(esa)],[f19_sk]) ).
cnf(t11,plain,
coantidomain(coantidomain(X1)) = codomain(X1),
inference(equality_encoding,[status(esa)],[c20]) ).
cnf(t143,plain,
coantidomain(coantidomain(X1)) = codomain(X1),
inference(orient,[status(thm)],[t11]) ).
cnf(t190370,plain,
addition(coantidomain(X1),codomain(X1)) = one,
inference(step,[status(thm)],[t140,t143]) ).
cnf(t146,plain,
addition(coantidomain(X1),codomain(X1)) = one,
inference(rw,[status(thm)],[t190370]) ).
cnf(t190412,plain,
addition(codomain(X1),coantidomain(X1)) = one,
inference(step,[status(thm)],[t146,t108]) ).
cnf(t427,plain,
addition(codomain(X1),coantidomain(X1)) = one,
inference(orient,[status(thm)],[t190412]) ).
cnf(t147906,plain,
multiplication(X1,codomain(addition(X1,X2))) = multiplication(X1,one),
inference(cp,[status(thm)],[t147904,t427]) ).
cnf(t194167,plain,
multiplication(X1,codomain(addition(X1,X2))) = X1,
inference(step,[status(thm)],[t147906,t34]) ).
cnf(t148091,plain,
multiplication(X1,codomain(addition(X1,X2))) = X1,
inference(orient,[status(thm)],[t194167]) ).
cnf(t148106,plain,
X1 = multiplication(X1,codomain(addition(X2,X1))),
inference(cp,[status(thm)],[t148091,t108]) ).
cnf(t148267,plain,
multiplication(X1,codomain(addition(X2,X1))) = X1,
inference(orient,[status(thm)],[t148106]) ).
cnf(t44,plain,
multiplication(X1,addition(one,X2)) = addition(X1,multiplication(X1,X2)),
inference(cp,[status(thm)],[t43,t34]) ).
cnf(t609,plain,
addition(X1,multiplication(X1,X2)) = multiplication(X1,addition(one,X2)),
inference(orient,[status(thm)],[t44]) ).
cnf(t101,plain,
domain_difference(X1,antidomain(X2)) = multiplication(domain(X1),domain(X2)),
inference(cp,[status(thm)],[t73,t99]) ).
cnf(t966,plain,
multiplication(domain(X1),domain(X2)) = domain_difference(X1,antidomain(X2)),
inference(orient,[status(thm)],[t101]) ).
cnf(t981,plain,
multiplication(domain(X1),addition(one,domain(X2))) = addition(domain(X1),domain_difference(X1,antidomain(X2))),
inference(cp,[status(thm)],[t609,t966]) ).
cnf(t625,plain,
addition(domain(X1),antidomain(X1)) = addition(domain(X1),one),
inference(cp,[status(thm)],[t622,t122]) ).
cnf(t190451,plain,
one = addition(domain(X1),one),
inference(step,[status(thm)],[t625,t122]) ).
cnf(t190452,plain,
one = addition(one,domain(X1)),
inference(step,[status(thm)],[t190451,t108]) ).
cnf(t638,plain,
addition(one,domain(X1)) = one,
inference(orient,[status(thm)],[t190452]) ).
cnf(t190984,plain,
multiplication(domain(X1),one) = addition(domain(X1),domain_difference(X1,antidomain(X2))),
inference(step,[status(thm)],[t981,t638]) ).
cnf(t190985,plain,
domain(X1) = addition(domain(X1),domain_difference(X1,antidomain(X2))),
inference(step,[status(thm)],[t190984,t34]) ).
cnf(t190986,plain,
domain(X1) = addition(domain(X1),domain_difference(X1,c(X2))),
inference(step,[status(thm)],[t190985,t3443]) ).
cnf(t8450,plain,
addition(domain(X1),domain_difference(X1,c(X2))) = domain(X1),
inference(orient,[status(thm)],[t190986]) ).
cnf(t8467,plain,
domain(X1) = addition(domain(X1),domain_difference(X1,domain(X2))),
inference(cp,[status(thm)],[t8450,t3510]) ).
cnf(t190683,plain,
multiplication(domain(X1),c(X2)) = domain_difference(X1,X2),
inference(step,[status(thm)],[t73,t3443]) ).
cnf(t106,plain,
domain_difference(X1,domain(X2)) = multiplication(domain(X1),c(X2)),
inference(cp,[status(thm)],[t73,t104]) ).
cnf(t991,plain,
multiplication(domain(X1),c(X2)) = domain_difference(X1,domain(X2)),
inference(orient,[status(thm)],[t106]) ).
cnf(t190684,plain,
domain_difference(X1,domain(X2)) = domain_difference(X1,X2),
inference(step,[status(thm)],[t190683,t991]) ).
cnf(t3482,plain,
domain_difference(X1,domain(X2)) = domain_difference(X1,X2),
inference(rw,[status(thm)],[t190684]) ).
cnf(t3595,plain,
domain_difference(X1,domain(X2)) = domain_difference(X1,X2),
inference(orient,[status(thm)],[t3482]) ).
cnf(t190991,plain,
domain(X1) = addition(domain(X1),domain_difference(X1,X2)),
inference(step,[status(thm)],[t8467,t3595]) ).
cnf(t8535,plain,
addition(domain(X1),domain_difference(X1,X2)) = domain(X1),
inference(orient,[status(thm)],[t190991]) ).
cnf(t148287,plain,
domain_difference(X1,X2) = multiplication(domain_difference(X1,X2),codomain(domain(X1))),
inference(cp,[status(thm)],[t148267,t8535]) ).
fof(f25,axiom,
! [X0,X1] : backward_box(X0,X1) = c(backward_diamond(X0,c(X1))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',backward_box) ).
fof(f25_nnf,plain,
! [X0,X1] : backward_box(X0,X1) = c(backward_diamond(X0,c(X1))),
inference(nnf_transformation,[status(thm)],[f25]) ).
fof(f25_sk,plain,
! [X0,X1] : backward_box(X0,X1) = c(backward_diamond(X0,c(X1))),
inference(skolemisation,[status(esa)],[f25_nnf]) ).
cnf(c26,plain,
backward_box(X0,X1) = c(backward_diamond(X0,c(X1))),
inference(cnf_transformation,[status(esa)],[f25_sk]) ).
cnf(t18,plain,
c(backward_diamond(X1,c(X2))) = backward_box(X1,X2),
inference(equality_encoding,[status(esa)],[c26]) ).
cnf(t193,plain,
c(backward_diamond(X1,c(X2))) = backward_box(X1,X2),
inference(orient,[status(thm)],[t18]) ).
cnf(t57,plain,
zero = antidomain(one),
inference(cp,[status(thm)],[t56,t34]) ).
cnf(t207,plain,
antidomain(one) = zero,
inference(orient,[status(thm)],[t57]) ).
cnf(t209,plain,
domain(one) = antidomain(zero),
inference(cp,[status(thm)],[t99,t207]) ).
cnf(t208,plain,
one = addition(domain(one),zero),
inference(cp,[status(thm)],[t122,t207]) ).
cnf(t190375,plain,
one = domain(one),
inference(step,[status(thm)],[t208,t37]) ).
cnf(t211,plain,
domain(one) = one,
inference(orient,[status(thm)],[t190375]) ).
cnf(t190377,plain,
one = antidomain(zero),
inference(step,[status(thm)],[t209,t211]) ).
cnf(t220,plain,
antidomain(zero) = one,
inference(orient,[status(thm)],[t190377]) ).
cnf(t222,plain,
domain(zero) = antidomain(one),
inference(cp,[status(thm)],[t99,t220]) ).
cnf(t190378,plain,
domain(zero) = zero,
inference(step,[status(thm)],[t222,t207]) ).
cnf(t224,plain,
domain(zero) = zero,
inference(orient,[status(thm)],[t190378]) ).
cnf(t226,plain,
c(zero) = antidomain(zero),
inference(cp,[status(thm)],[t104,t224]) ).
cnf(t190379,plain,
c(zero) = one,
inference(step,[status(thm)],[t226,t220]) ).
cnf(t229,plain,
c(zero) = one,
inference(orient,[status(thm)],[t190379]) ).
cnf(t231,plain,
backward_box(X1,zero) = c(backward_diamond(X1,one)),
inference(cp,[status(thm)],[t193,t229]) ).
cnf(t338,plain,
c(backward_diamond(X1,one)) = backward_box(X1,zero),
inference(orient,[status(thm)],[t231]) ).
fof(f23,axiom,
! [X0,X1] : backward_diamond(X0,X1) = codomain(multiplication(codomain(X1),X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',backward_diamond) ).
fof(f23_nnf,plain,
! [X0,X1] : backward_diamond(X0,X1) = codomain(multiplication(codomain(X1),X0)),
inference(nnf_transformation,[status(thm)],[f23]) ).
fof(f23_sk,plain,
! [X0,X1] : backward_diamond(X0,X1) = codomain(multiplication(codomain(X1),X0)),
inference(skolemisation,[status(esa)],[f23_nnf]) ).
cnf(c24,plain,
backward_diamond(X0,X1) = codomain(multiplication(codomain(X1),X0)),
inference(cnf_transformation,[status(esa)],[f23_sk]) ).
cnf(t20,plain,
codomain(multiplication(codomain(X1),X2)) = backward_diamond(X2,X1),
inference(equality_encoding,[status(esa)],[c24]) ).
cnf(t199,plain,
codomain(multiplication(codomain(X1),X2)) = backward_diamond(X2,X1),
inference(orient,[status(thm)],[t20]) ).
cnf(t49,plain,
zero = coantidomain(one),
inference(cp,[status(thm)],[t47,t35]) ).
cnf(t205,plain,
coantidomain(one) = zero,
inference(orient,[status(thm)],[t49]) ).
cnf(t433,plain,
one = addition(codomain(one),zero),
inference(cp,[status(thm)],[t427,t205]) ).
cnf(t190413,plain,
one = codomain(one),
inference(step,[status(thm)],[t433,t37]) ).
cnf(t437,plain,
codomain(one) = one,
inference(orient,[status(thm)],[t190413]) ).
cnf(t442,plain,
backward_diamond(X1,one) = codomain(multiplication(one,X1)),
inference(cp,[status(thm)],[t199,t437]) ).
cnf(t190431,plain,
backward_diamond(X1,one) = codomain(X1),
inference(step,[status(thm)],[t442,t35]) ).
cnf(t460,plain,
backward_diamond(X1,one) = codomain(X1),
inference(orient,[status(thm)],[t190431]) ).
cnf(t190432,plain,
c(codomain(X1)) = backward_box(X1,zero),
inference(step,[status(thm)],[t338,t460]) ).
cnf(t461,plain,
c(codomain(X1)) = backward_box(X1,zero),
inference(rw,[status(thm)],[t190432]) ).
cnf(t462,plain,
c(codomain(X1)) = backward_box(X1,zero),
inference(orient,[status(thm)],[t461]) ).
cnf(t62,plain,
multiplication(addition(X1,X2),coantidomain(X1)) = addition(zero,multiplication(X2,coantidomain(X1))),
inference(cp,[status(thm)],[t61,t47]) ).
cnf(t190792,plain,
multiplication(addition(X1,X2),coantidomain(X1)) = multiplication(X2,coantidomain(X1)),
inference(step,[status(thm)],[t62,t233]) ).
cnf(t4355,plain,
multiplication(addition(X1,X2),coantidomain(X1)) = multiplication(X2,coantidomain(X1)),
inference(orient,[status(thm)],[t190792]) ).
cnf(t4360,plain,
multiplication(coantidomain(X1),coantidomain(codomain(X1))) = multiplication(one,coantidomain(codomain(X1))),
inference(cp,[status(thm)],[t4355,t427]) ).
cnf(t144,plain,
codomain(coantidomain(X1)) = coantidomain(codomain(X1)),
inference(cp,[status(thm)],[t143,t143]) ).
cnf(t268,plain,
coantidomain(codomain(X1)) = codomain(coantidomain(X1)),
inference(orient,[status(thm)],[t144]) ).
cnf(t190793,plain,
multiplication(coantidomain(X1),codomain(coantidomain(X1))) = multiplication(one,coantidomain(codomain(X1))),
inference(step,[status(thm)],[t4360,t268]) ).
cnf(t51,plain,
multiplication(X1,addition(X2,coantidomain(X1))) = addition(multiplication(X1,X2),zero),
inference(cp,[status(thm)],[t43,t47]) ).
cnf(t190538,plain,
multiplication(X1,addition(X2,coantidomain(X1))) = multiplication(X1,X2),
inference(step,[status(thm)],[t51,t37]) ).
cnf(t1876,plain,
multiplication(X1,addition(X2,coantidomain(X1))) = multiplication(X1,X2),
inference(orient,[status(thm)],[t190538]) ).
cnf(t1878,plain,
multiplication(X1,codomain(X1)) = multiplication(X1,one),
inference(cp,[status(thm)],[t1876,t427]) ).
cnf(t190539,plain,
multiplication(X1,codomain(X1)) = X1,
inference(step,[status(thm)],[t1878,t34]) ).
cnf(t1899,plain,
multiplication(X1,codomain(X1)) = X1,
inference(orient,[status(thm)],[t190539]) ).
cnf(t190794,plain,
coantidomain(X1) = multiplication(one,coantidomain(codomain(X1))),
inference(step,[status(thm)],[t190793,t1899]) ).
cnf(t190795,plain,
coantidomain(X1) = coantidomain(codomain(X1)),
inference(step,[status(thm)],[t190794,t35]) ).
cnf(t190796,plain,
coantidomain(X1) = codomain(coantidomain(X1)),
inference(step,[status(thm)],[t190795,t268]) ).
cnf(t4381,plain,
codomain(coantidomain(X1)) = coantidomain(X1),
inference(orient,[status(thm)],[t190796]) ).
cnf(t4390,plain,
backward_box(coantidomain(X1),zero) = c(coantidomain(X1)),
inference(cp,[status(thm)],[t462,t4381]) ).
cnf(t4425,plain,
backward_box(coantidomain(X1),zero) = c(coantidomain(X1)),
inference(orient,[status(thm)],[t4390]) ).
cnf(t2055,plain,
multiplication(domain(X1),addition(one,X1)) = addition(domain(X1),X1),
inference(cp,[status(thm)],[t609,t2038]) ).
cnf(t190903,plain,
multiplication(domain(X1),addition(one,X1)) = addition(X1,domain(X1)),
inference(step,[status(thm)],[t2055,t108]) ).
cnf(t6661,plain,
multiplication(domain(X1),addition(one,X1)) = addition(X1,domain(X1)),
inference(orient,[status(thm)],[t190903]) ).
cnf(t189,plain,
c(multiplication(X1,domain(X2))) = antidomain(forward_diamond(X1,X2)),
inference(cp,[status(thm)],[t104,t183]) ).
cnf(t1016,plain,
c(multiplication(X1,domain(X2))) = antidomain(forward_diamond(X1,X2)),
inference(orient,[status(thm)],[t189]) ).
cnf(t1024,plain,
antidomain(forward_diamond(X1,antidomain(X2))) = c(multiplication(X1,c(X2))),
inference(cp,[status(thm)],[t1016,t252]) ).
cnf(t1753,plain,
antidomain(forward_diamond(X1,antidomain(X2))) = c(multiplication(X1,c(X2))),
inference(orient,[status(thm)],[t1024]) ).
cnf(t190689,plain,
c(forward_diamond(X1,antidomain(X2))) = c(multiplication(X1,c(X2))),
inference(step,[status(thm)],[t1753,t3443]) ).
cnf(t190690,plain,
c(forward_diamond(X1,c(X2))) = c(multiplication(X1,c(X2))),
inference(step,[status(thm)],[t190689,t3443]) ).
fof(f24,axiom,
! [X0,X1] : forward_box(X0,X1) = c(forward_diamond(X0,c(X1))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',forward_box) ).
fof(f24_nnf,plain,
! [X0,X1] : forward_box(X0,X1) = c(forward_diamond(X0,c(X1))),
inference(nnf_transformation,[status(thm)],[f24]) ).
fof(f24_sk,plain,
! [X0,X1] : forward_box(X0,X1) = c(forward_diamond(X0,c(X1))),
inference(skolemisation,[status(esa)],[f24_nnf]) ).
cnf(c25,plain,
forward_box(X0,X1) = c(forward_diamond(X0,c(X1))),
inference(cnf_transformation,[status(esa)],[f24_sk]) ).
cnf(t19,plain,
c(forward_diamond(X1,c(X2))) = forward_box(X1,X2),
inference(equality_encoding,[status(esa)],[c25]) ).
cnf(t195,plain,
c(forward_diamond(X1,c(X2))) = forward_box(X1,X2),
inference(orient,[status(thm)],[t19]) ).
cnf(t190691,plain,
forward_box(X1,X2) = c(multiplication(X1,c(X2))),
inference(step,[status(thm)],[t190690,t195]) ).
cnf(t3487,plain,
forward_box(X1,X2) = c(multiplication(X1,c(X2))),
inference(rw,[status(thm)],[t190691]) ).
cnf(t3743,plain,
c(multiplication(X1,c(X2))) = forward_box(X1,X2),
inference(orient,[status(thm)],[t3487]) ).
fof(f4,axiom,
! [A,B,C] : multiplication(A,multiplication(B,C)) = multiplication(multiplication(A,B),C),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',multiplicative_associativity) ).
fof(f4_nnf,plain,
! [A,B,C] : multiplication(A,multiplication(B,C)) = multiplication(multiplication(A,B),C),
inference(nnf_transformation,[status(thm)],[f4]) ).
fof(f4_sk,plain,
! [A,B,C] : multiplication(A,multiplication(B,C)) = multiplication(multiplication(A,B),C),
inference(skolemisation,[status(esa)],[f4_nnf]) ).
cnf(c4,plain,
multiplication(X0,multiplication(X1,X2)) = multiplication(multiplication(X0,X1),X2),
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(t27,plain,
multiplication(multiplication(X1,X2),X3) = multiplication(X1,multiplication(X2,X3)),
inference(equality_encoding,[status(esa)],[c4]) ).
cnf(t42,plain,
multiplication(multiplication(X1,X2),X3) = multiplication(X1,multiplication(X2,X3)),
inference(orient,[status(thm)],[t27]) ).
cnf(t60,plain,
multiplication(antidomain(X1),multiplication(X1,X2)) = multiplication(zero,X2),
inference(cp,[status(thm)],[t42,t56]) ).
fof(f10,axiom,
! [A] : multiplication(zero,A) = zero,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',left_annihilation) ).
fof(f10_nnf,plain,
! [A] : multiplication(zero,A) = zero,
inference(nnf_transformation,[status(thm)],[f10]) ).
fof(f10_sk,plain,
! [A] : multiplication(zero,A) = zero,
inference(skolemisation,[status(esa)],[f10_nnf]) ).
cnf(c10,plain,
multiplication(zero,X0) = zero,
inference(cnf_transformation,[status(esa)],[f10_sk]) ).
cnf(t8,plain,
multiplication(zero,X1) = zero,
inference(equality_encoding,[status(esa)],[c10]) ).
cnf(t71,plain,
multiplication(zero,X1) = zero,
inference(orient,[status(thm)],[t8]) ).
cnf(t190543,plain,
multiplication(antidomain(X1),multiplication(X1,X2)) = zero,
inference(step,[status(thm)],[t60,t71]) ).
cnf(t1956,plain,
multiplication(antidomain(X1),multiplication(X1,X2)) = zero,
inference(orient,[status(thm)],[t190543]) ).
cnf(t2054,plain,
zero = multiplication(antidomain(domain(X1)),X1),
inference(cp,[status(thm)],[t1956,t2038]) ).
cnf(t190547,plain,
zero = multiplication(c(X1),X1),
inference(step,[status(thm)],[t2054,t104]) ).
cnf(t2071,plain,
multiplication(c(X1),X1) = zero,
inference(orient,[status(thm)],[t190547]) ).
cnf(t3775,plain,
zero = multiplication(forward_box(X1,X2),multiplication(X1,c(X2))),
inference(cp,[status(thm)],[t2071,t3743]) ).
cnf(t20771,plain,
multiplication(forward_box(X1,X2),multiplication(X1,c(X2))) = zero,
inference(orient,[status(thm)],[t3775]) ).
cnf(t185,plain,
forward_diamond(antidomain(domain(X1)),X1) = domain(zero),
inference(cp,[status(thm)],[t183,t56]) ).
cnf(t190395,plain,
forward_diamond(c(X1),X1) = domain(zero),
inference(step,[status(thm)],[t185,t104]) ).
cnf(t190396,plain,
forward_diamond(c(X1),X1) = zero,
inference(step,[status(thm)],[t190395,t224]) ).
cnf(t302,plain,
forward_diamond(c(X1),X1) = zero,
inference(orient,[status(thm)],[t190396]) ).
cnf(t307,plain,
forward_box(c(c(X1)),X1) = c(zero),
inference(cp,[status(thm)],[t195,t302]) ).
cnf(t190437,plain,
forward_box(c(c(X1)),X1) = one,
inference(step,[status(thm)],[t307,t229]) ).
cnf(t498,plain,
forward_box(c(c(X1)),X1) = one,
inference(orient,[status(thm)],[t190437]) ).
cnf(t190732,plain,
forward_box(domain(X1),X1) = one,
inference(step,[status(thm)],[t498,t3510]) ).
cnf(t3546,plain,
forward_box(domain(X1),X1) = one,
inference(rw,[status(thm)],[t190732]) ).
cnf(t3570,plain,
forward_box(domain(X1),X1) = one,
inference(orient,[status(thm)],[t3546]) ).
cnf(t190639,plain,
c(multiplication(X1,domain(X2))) = c(forward_diamond(X1,X2)),
inference(step,[status(thm)],[t1016,t3443]) ).
cnf(t3448,plain,
c(multiplication(X1,domain(X2))) = c(forward_diamond(X1,X2)),
inference(orient,[status(thm)],[t190639]) ).
cnf(t3517,plain,
domain(multiplication(X1,domain(X2))) = c(c(forward_diamond(X1,X2))),
inference(cp,[status(thm)],[t3510,t3448]) ).
cnf(t190760,plain,
forward_diamond(X1,X2) = c(c(forward_diamond(X1,X2))),
inference(step,[status(thm)],[t3517,t183]) ).
cnf(t190761,plain,
forward_diamond(X1,X2) = domain(forward_diamond(X1,X2)),
inference(step,[status(thm)],[t190760,t3510]) ).
cnf(t3614,plain,
domain(forward_diamond(X1,X2)) = forward_diamond(X1,X2),
inference(orient,[status(thm)],[t190761]) ).
cnf(t3615,plain,
one = forward_box(forward_diamond(X1,X2),forward_diamond(X1,X2)),
inference(cp,[status(thm)],[t3570,t3614]) ).
cnf(t5773,plain,
forward_box(forward_diamond(X1,X2),forward_diamond(X1,X2)) = one,
inference(orient,[status(thm)],[t3615]) ).
cnf(t2087,plain,
multiplication(c(X1),addition(X1,X2)) = addition(zero,multiplication(c(X1),X2)),
inference(cp,[status(thm)],[t43,t2071]) ).
cnf(t190917,plain,
multiplication(c(X1),addition(X1,X2)) = multiplication(c(X1),X2),
inference(step,[status(thm)],[t2087,t233]) ).
cnf(t7038,plain,
multiplication(c(X1),addition(X1,X2)) = multiplication(c(X1),X2),
inference(orient,[status(thm)],[t190917]) ).
fof(f13,axiom,
! [X0,X1] : addition(antidomain(multiplication(X0,X1)),antidomain(multiplication(X0,antidomain(antidomain(X1))))) = antidomain(multiplication(X0,antidomain(antidomain(X1)))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',domain2) ).
fof(f13_nnf,plain,
! [X0,X1] : addition(antidomain(multiplication(X0,X1)),antidomain(multiplication(X0,antidomain(antidomain(X1))))) = antidomain(multiplication(X0,antidomain(antidomain(X1)))),
inference(nnf_transformation,[status(thm)],[f13]) ).
fof(f13_sk,plain,
! [X0,X1] : addition(antidomain(multiplication(X0,X1)),antidomain(multiplication(X0,antidomain(antidomain(X1))))) = antidomain(multiplication(X0,antidomain(antidomain(X1)))),
inference(skolemisation,[status(esa)],[f13_nnf]) ).
cnf(c14,plain,
addition(antidomain(multiplication(X0,X1)),antidomain(multiplication(X0,antidomain(antidomain(X1))))) = antidomain(multiplication(X0,antidomain(antidomain(X1)))),
inference(cnf_transformation,[status(esa)],[f13_sk]) ).
cnf(t32,plain,
addition(antidomain(multiplication(X1,X2)),antidomain(multiplication(X1,antidomain(antidomain(X2))))) = antidomain(multiplication(X1,antidomain(antidomain(X2)))),
inference(equality_encoding,[status(esa)],[c14]) ).
cnf(t85,plain,
addition(antidomain(multiplication(X1,X2)),antidomain(multiplication(X1,antidomain(antidomain(X2))))) = antidomain(multiplication(X1,antidomain(antidomain(X2)))),
inference(orient,[status(thm)],[t32]) ).
cnf(t190364,plain,
addition(antidomain(multiplication(X1,X2)),antidomain(multiplication(X1,domain(X2)))) = antidomain(multiplication(X1,antidomain(antidomain(X2)))),
inference(step,[status(thm)],[t85,t99]) ).
cnf(t190365,plain,
addition(antidomain(multiplication(X1,X2)),antidomain(multiplication(X1,domain(X2)))) = antidomain(multiplication(X1,domain(X2))),
inference(step,[status(thm)],[t190364,t99]) ).
cnf(t103,plain,
addition(antidomain(multiplication(X1,X2)),antidomain(multiplication(X1,domain(X2)))) = antidomain(multiplication(X1,domain(X2))),
inference(rw,[status(thm)],[t190365]) ).
cnf(t191290,plain,
addition(c(multiplication(X1,X2)),antidomain(multiplication(X1,domain(X2)))) = antidomain(multiplication(X1,domain(X2))),
inference(step,[status(thm)],[t103,t3443]) ).
cnf(t191291,plain,
addition(c(multiplication(X1,X2)),c(multiplication(X1,domain(X2)))) = antidomain(multiplication(X1,domain(X2))),
inference(step,[status(thm)],[t191290,t3443]) ).
cnf(t3749,plain,
forward_box(X1,c(X2)) = c(multiplication(X1,domain(X2))),
inference(cp,[status(thm)],[t3743,t3510]) ).
cnf(t190771,plain,
forward_box(X1,c(X2)) = c(forward_diamond(X1,X2)),
inference(step,[status(thm)],[t3749,t3448]) ).
cnf(t3844,plain,
c(forward_diamond(X1,X2)) = forward_box(X1,c(X2)),
inference(orient,[status(thm)],[t190771]) ).
cnf(t190772,plain,
c(multiplication(X1,domain(X2))) = forward_box(X1,c(X2)),
inference(step,[status(thm)],[t3448,t3844]) ).
cnf(t3845,plain,
c(multiplication(X1,domain(X2))) = forward_box(X1,c(X2)),
inference(orient,[status(thm)],[t190772]) ).
cnf(t191292,plain,
addition(c(multiplication(X1,X2)),forward_box(X1,c(X2))) = antidomain(multiplication(X1,domain(X2))),
inference(step,[status(thm)],[t191291,t3845]) ).
cnf(t191293,plain,
addition(forward_box(X1,c(X2)),c(multiplication(X1,X2))) = antidomain(multiplication(X1,domain(X2))),
inference(step,[status(thm)],[t191292,t108]) ).
cnf(t191294,plain,
addition(forward_box(X1,c(X2)),c(multiplication(X1,X2))) = c(multiplication(X1,domain(X2))),
inference(step,[status(thm)],[t191293,t3443]) ).
cnf(t191295,plain,
addition(forward_box(X1,c(X2)),c(multiplication(X1,X2))) = forward_box(X1,c(X2)),
inference(step,[status(thm)],[t191294,t3845]) ).
cnf(t15954,plain,
addition(forward_box(X1,c(X2)),c(multiplication(X1,X2))) = forward_box(X1,c(X2)),
inference(orient,[status(thm)],[t191295]) ).
cnf(t16065,plain,
multiplication(c(forward_box(X1,c(X2))),c(multiplication(X1,X2))) = multiplication(c(forward_box(X1,c(X2))),forward_box(X1,c(X2))),
inference(cp,[status(thm)],[t7038,t15954]) ).
cnf(t190665,plain,
multiplication(c(X1),c(X2)) = domain_difference(antidomain(X1),X2),
inference(step,[status(thm)],[t1041,t3443]) ).
cnf(t190666,plain,
multiplication(c(X1),c(X2)) = domain_difference(c(X1),X2),
inference(step,[status(thm)],[t190665,t3443]) ).
cnf(t3470,plain,
multiplication(c(X1),c(X2)) = domain_difference(c(X1),X2),
inference(rw,[status(thm)],[t190666]) ).
cnf(t3966,plain,
multiplication(c(X1),c(X2)) = domain_difference(c(X1),X2),
inference(orient,[status(thm)],[t3470]) ).
cnf(t191296,plain,
domain_difference(c(forward_box(X1,c(X2))),multiplication(X1,X2)) = multiplication(c(forward_box(X1,c(X2))),forward_box(X1,c(X2))),
inference(step,[status(thm)],[t16065,t3966]) ).
cnf(t3771,plain,
domain(multiplication(X1,c(X2))) = c(forward_box(X1,X2)),
inference(cp,[status(thm)],[t3510,t3743]) ).
cnf(t190774,plain,
forward_diamond(X1,c(X2)) = c(forward_box(X1,X2)),
inference(step,[status(thm)],[t3771,t3450]) ).
cnf(t3880,plain,
c(forward_box(X1,X2)) = forward_diamond(X1,c(X2)),
inference(orient,[status(thm)],[t190774]) ).
cnf(t191297,plain,
domain_difference(forward_diamond(X1,c(c(X2))),multiplication(X1,X2)) = multiplication(c(forward_box(X1,c(X2))),forward_box(X1,c(X2))),
inference(step,[status(thm)],[t191296,t3880]) ).
cnf(t191298,plain,
domain_difference(forward_diamond(X1,domain(X2)),multiplication(X1,X2)) = multiplication(c(forward_box(X1,c(X2))),forward_box(X1,c(X2))),
inference(step,[status(thm)],[t191297,t3510]) ).
cnf(t191299,plain,
domain_difference(forward_diamond(X1,X2),multiplication(X1,X2)) = multiplication(c(forward_box(X1,c(X2))),forward_box(X1,c(X2))),
inference(step,[status(thm)],[t191298,t3645]) ).
cnf(t191300,plain,
domain_difference(forward_diamond(X1,X2),multiplication(X1,X2)) = zero,
inference(step,[status(thm)],[t191299,t2071]) ).
cnf(t16080,plain,
domain_difference(forward_diamond(X1,X2),multiplication(X1,X2)) = zero,
inference(orient,[status(thm)],[t191300]) ).
cnf(t16106,plain,
zero = domain_difference(forward_diamond(X1,coantidomain(X1)),zero),
inference(cp,[status(thm)],[t16080,t47]) ).
cnf(t223,plain,
domain_difference(X1,zero) = multiplication(domain(X1),one),
inference(cp,[status(thm)],[t73,t220]) ).
cnf(t190390,plain,
domain_difference(X1,zero) = domain(X1),
inference(step,[status(thm)],[t223,t34]) ).
cnf(t251,plain,
domain_difference(X1,zero) = domain(X1),
inference(orient,[status(thm)],[t190390]) ).
cnf(t191301,plain,
zero = domain(forward_diamond(X1,coantidomain(X1))),
inference(step,[status(thm)],[t16106,t251]) ).
cnf(t191302,plain,
zero = forward_diamond(X1,coantidomain(X1)),
inference(step,[status(thm)],[t191301,t3614]) ).
cnf(t16171,plain,
forward_diamond(X1,coantidomain(X1)) = zero,
inference(orient,[status(thm)],[t191302]) ).
cnf(t16176,plain,
one = forward_box(forward_diamond(X1,coantidomain(X1)),zero),
inference(cp,[status(thm)],[t5773,t16171]) ).
cnf(t190677,plain,
domain(c(X1)) = c(X1),
inference(step,[status(thm)],[t252,t3443]) ).
cnf(t230,plain,
forward_box(X1,zero) = c(forward_diamond(X1,one)),
inference(cp,[status(thm)],[t195,t229]) ).
cnf(t214,plain,
forward_diamond(X1,one) = domain(multiplication(X1,one)),
inference(cp,[status(thm)],[t183,t211]) ).
cnf(t190389,plain,
forward_diamond(X1,one) = domain(X1),
inference(step,[status(thm)],[t214,t34]) ).
cnf(t246,plain,
forward_diamond(X1,one) = domain(X1),
inference(orient,[status(thm)],[t190389]) ).
cnf(t190399,plain,
forward_box(X1,zero) = c(domain(X1)),
inference(step,[status(thm)],[t230,t246]) ).
cnf(t254,plain,
c(domain(X1)) = domain(c(X1)),
inference(cp,[status(thm)],[t252,t104]) ).
cnf(t295,plain,
c(domain(X1)) = domain(c(X1)),
inference(orient,[status(thm)],[t254]) ).
cnf(t190400,plain,
forward_box(X1,zero) = domain(c(X1)),
inference(step,[status(thm)],[t190399,t295]) ).
cnf(t320,plain,
domain(c(X1)) = forward_box(X1,zero),
inference(orient,[status(thm)],[t190400]) ).
cnf(t190678,plain,
forward_box(X1,zero) = c(X1),
inference(step,[status(thm)],[t190677,t320]) ).
cnf(t3479,plain,
forward_box(X1,zero) = c(X1),
inference(rw,[status(thm)],[t190678]) ).
cnf(t3491,plain,
forward_box(X1,zero) = c(X1),
inference(orient,[status(thm)],[t3479]) ).
cnf(t191307,plain,
one = c(forward_diamond(X1,coantidomain(X1))),
inference(step,[status(thm)],[t16176,t3491]) ).
cnf(t191308,plain,
one = forward_box(X1,c(coantidomain(X1))),
inference(step,[status(thm)],[t191307,t3844]) ).
cnf(t16194,plain,
forward_box(X1,c(coantidomain(X1))) = one,
inference(orient,[status(thm)],[t191308]) ).
cnf(t20778,plain,
zero = multiplication(one,multiplication(X1,c(c(coantidomain(X1))))),
inference(cp,[status(thm)],[t20771,t16194]) ).
cnf(t191498,plain,
zero = multiplication(X1,c(c(coantidomain(X1)))),
inference(step,[status(thm)],[t20778,t35]) ).
cnf(t191499,plain,
zero = multiplication(X1,domain(coantidomain(X1))),
inference(step,[status(thm)],[t191498,t3510]) ).
cnf(t20850,plain,
multiplication(X1,domain(coantidomain(X1))) = zero,
inference(orient,[status(thm)],[t191499]) ).
cnf(t20860,plain,
multiplication(X1,addition(domain(coantidomain(X1)),X2)) = addition(zero,multiplication(X1,X2)),
inference(cp,[status(thm)],[t43,t20850]) ).
cnf(t191593,plain,
multiplication(X1,addition(domain(coantidomain(X1)),X2)) = multiplication(X1,X2),
inference(step,[status(thm)],[t20860,t233]) ).
cnf(t23286,plain,
multiplication(X1,addition(domain(coantidomain(X1)),X2)) = multiplication(X1,X2),
inference(orient,[status(thm)],[t191593]) ).
cnf(t255,plain,
one = addition(c(X1),antidomain(antidomain(X1))),
inference(cp,[status(thm)],[t122,t252]) ).
cnf(t190435,plain,
one = addition(c(X1),domain(X1)),
inference(step,[status(thm)],[t255,t99]) ).
cnf(t190436,plain,
one = addition(domain(X1),c(X1)),
inference(step,[status(thm)],[t190435,t108]) ).
cnf(t484,plain,
addition(domain(X1),c(X1)) = one,
inference(orient,[status(thm)],[t190436]) ).
cnf(t23293,plain,
multiplication(X1,c(coantidomain(X1))) = multiplication(X1,one),
inference(cp,[status(thm)],[t23286,t484]) ).
cnf(t191594,plain,
multiplication(X1,c(coantidomain(X1))) = X1,
inference(step,[status(thm)],[t23293,t34]) ).
cnf(t23340,plain,
multiplication(X1,c(coantidomain(X1))) = X1,
inference(orient,[status(thm)],[t191594]) ).
cnf(t23385,plain,
forward_box(X1,coantidomain(X1)) = c(X1),
inference(cp,[status(thm)],[t3743,t23340]) ).
cnf(t23394,plain,
forward_box(X1,coantidomain(X1)) = c(X1),
inference(orient,[status(thm)],[t23385]) ).
cnf(t190797,plain,
coantidomain(codomain(X1)) = coantidomain(X1),
inference(step,[status(thm)],[t268,t4381]) ).
cnf(t4382,plain,
coantidomain(codomain(X1)) = coantidomain(X1),
inference(orient,[status(thm)],[t190797]) ).
cnf(t23397,plain,
c(codomain(X1)) = forward_box(codomain(X1),coantidomain(X1)),
inference(cp,[status(thm)],[t23394,t4382]) ).
cnf(t191595,plain,
backward_box(X1,zero) = forward_box(codomain(X1),coantidomain(X1)),
inference(step,[status(thm)],[t23397,t462]) ).
cnf(t2057,plain,
multiplication(addition(X1,domain(X2)),X2) = addition(multiplication(X1,X2),X2),
inference(cp,[status(thm)],[t61,t2038]) ).
cnf(t191071,plain,
multiplication(addition(X1,domain(X2)),X2) = addition(X2,multiplication(X1,X2)),
inference(step,[status(thm)],[t2057,t108]) ).
cnf(t65,plain,
multiplication(addition(one,X1),X2) = addition(X2,multiplication(X1,X2)),
inference(cp,[status(thm)],[t61,t35]) ).
cnf(t1515,plain,
addition(X1,multiplication(X2,X1)) = multiplication(addition(one,X2),X1),
inference(orient,[status(thm)],[t65]) ).
cnf(t191072,plain,
multiplication(addition(X1,domain(X2)),X2) = multiplication(addition(one,X1),X2),
inference(step,[status(thm)],[t191071,t1515]) ).
cnf(t10142,plain,
multiplication(addition(X1,domain(X2)),X2) = multiplication(addition(one,X1),X2),
inference(orient,[status(thm)],[t191072]) ).
cnf(t10186,plain,
forward_box(addition(X1,domain(c(X2))),X2) = c(multiplication(addition(one,X1),c(X2))),
inference(cp,[status(thm)],[t3743,t10142]) ).
cnf(t190701,plain,
domain(c(X1)) = c(X1),
inference(step,[status(thm)],[t320,t3491]) ).
cnf(t3494,plain,
domain(c(X1)) = c(X1),
inference(orient,[status(thm)],[t190701]) ).
cnf(t191092,plain,
forward_box(addition(X1,c(X2)),X2) = c(multiplication(addition(one,X1),c(X2))),
inference(step,[status(thm)],[t10186,t3494]) ).
cnf(t191093,plain,
forward_box(addition(X1,c(X2)),X2) = forward_box(addition(one,X1),X2),
inference(step,[status(thm)],[t191092,t3743]) ).
cnf(t11956,plain,
forward_box(addition(X1,c(X2)),X2) = forward_box(addition(one,X1),X2),
inference(orient,[status(thm)],[t191093]) ).
cnf(t7056,plain,
multiplication(c(codomain(X1)),coantidomain(X1)) = multiplication(c(codomain(X1)),one),
inference(cp,[status(thm)],[t7038,t427]) ).
cnf(t190921,plain,
multiplication(backward_box(X1,zero),coantidomain(X1)) = multiplication(c(codomain(X1)),one),
inference(step,[status(thm)],[t7056,t462]) ).
cnf(t190922,plain,
multiplication(backward_box(X1,zero),coantidomain(X1)) = c(codomain(X1)),
inference(step,[status(thm)],[t190921,t34]) ).
cnf(t190923,plain,
multiplication(backward_box(X1,zero),coantidomain(X1)) = backward_box(X1,zero),
inference(step,[status(thm)],[t190922,t462]) ).
cnf(t7098,plain,
multiplication(backward_box(X1,zero),coantidomain(X1)) = backward_box(X1,zero),
inference(orient,[status(thm)],[t190923]) ).
cnf(t7109,plain,
multiplication(addition(one,backward_box(X1,zero)),coantidomain(X1)) = addition(coantidomain(X1),backward_box(X1,zero)),
inference(cp,[status(thm)],[t1515,t7098]) ).
cnf(t644,plain,
one = addition(one,c(X1)),
inference(cp,[status(thm)],[t638,t252]) ).
cnf(t649,plain,
addition(one,c(X1)) = one,
inference(orient,[status(thm)],[t644]) ).
cnf(t651,plain,
one = addition(one,backward_box(X1,zero)),
inference(cp,[status(thm)],[t649,t462]) ).
cnf(t714,plain,
addition(one,backward_box(X1,zero)) = one,
inference(orient,[status(thm)],[t651]) ).
cnf(t190924,plain,
multiplication(one,coantidomain(X1)) = addition(coantidomain(X1),backward_box(X1,zero)),
inference(step,[status(thm)],[t7109,t714]) ).
cnf(t190925,plain,
coantidomain(X1) = addition(coantidomain(X1),backward_box(X1,zero)),
inference(step,[status(thm)],[t190924,t35]) ).
cnf(t7123,plain,
addition(coantidomain(X1),backward_box(X1,zero)) = coantidomain(X1),
inference(orient,[status(thm)],[t190925]) ).
cnf(t7126,plain,
coantidomain(coantidomain(X1)) = addition(codomain(X1),backward_box(coantidomain(X1),zero)),
inference(cp,[status(thm)],[t7123,t143]) ).
cnf(t190934,plain,
codomain(X1) = addition(codomain(X1),backward_box(coantidomain(X1),zero)),
inference(step,[status(thm)],[t7126,t143]) ).
cnf(t190935,plain,
codomain(X1) = addition(codomain(X1),c(coantidomain(X1))),
inference(step,[status(thm)],[t190934,t4425]) ).
cnf(t7282,plain,
addition(codomain(X1),c(coantidomain(X1))) = codomain(X1),
inference(orient,[status(thm)],[t190935]) ).
cnf(t11958,plain,
forward_box(addition(one,codomain(X1)),coantidomain(X1)) = forward_box(codomain(X1),coantidomain(X1)),
inference(cp,[status(thm)],[t11956,t7282]) ).
cnf(t624,plain,
addition(codomain(X1),coantidomain(X1)) = addition(codomain(X1),one),
inference(cp,[status(thm)],[t622,t427]) ).
cnf(t190449,plain,
one = addition(codomain(X1),one),
inference(step,[status(thm)],[t624,t427]) ).
cnf(t190450,plain,
one = addition(one,codomain(X1)),
inference(step,[status(thm)],[t190449,t108]) ).
cnf(t631,plain,
addition(one,codomain(X1)) = one,
inference(orient,[status(thm)],[t190450]) ).
cnf(t191094,plain,
forward_box(one,coantidomain(X1)) = forward_box(codomain(X1),coantidomain(X1)),
inference(step,[status(thm)],[t11958,t631]) ).
cnf(t253,plain,
c(antidomain(X1)) = domain(domain(X1)),
inference(cp,[status(thm)],[t252,t99]) ).
cnf(t187,plain,
forward_diamond(one,X1) = domain(domain(X1)),
inference(cp,[status(thm)],[t183,t35]) ).
cnf(t271,plain,
domain(domain(X1)) = forward_diamond(one,X1),
inference(orient,[status(thm)],[t187]) ).
cnf(t190394,plain,
c(antidomain(X1)) = forward_diamond(one,X1),
inference(step,[status(thm)],[t253,t271]) ).
cnf(t288,plain,
c(antidomain(X1)) = forward_diamond(one,X1),
inference(orient,[status(thm)],[t190394]) ).
cnf(t105,plain,
domain(domain(X1)) = antidomain(c(X1)),
inference(cp,[status(thm)],[t99,t104]) ).
cnf(t260,plain,
antidomain(c(X1)) = domain(domain(X1)),
inference(orient,[status(thm)],[t105]) ).
cnf(t190392,plain,
antidomain(c(X1)) = forward_diamond(one,X1),
inference(step,[status(thm)],[t260,t271]) ).
cnf(t272,plain,
antidomain(c(X1)) = forward_diamond(one,X1),
inference(orient,[status(thm)],[t190392]) ).
cnf(t289,plain,
forward_diamond(one,c(X1)) = c(forward_diamond(one,X1)),
inference(cp,[status(thm)],[t288,t272]) ).
cnf(t515,plain,
c(forward_diamond(one,X1)) = forward_diamond(one,c(X1)),
inference(orient,[status(thm)],[t289]) ).
cnf(t516,plain,
forward_diamond(one,c(c(X1))) = forward_box(one,X1),
inference(cp,[status(thm)],[t515,t195]) ).
cnf(t779,plain,
forward_diamond(one,c(c(X1))) = forward_box(one,X1),
inference(orient,[status(thm)],[t516]) ).
cnf(t190730,plain,
forward_diamond(one,domain(X1)) = forward_box(one,X1),
inference(step,[status(thm)],[t779,t3510]) ).
cnf(t263,plain,
c(c(X1)) = domain(domain(domain(X1))),
inference(cp,[status(thm)],[t252,t260]) ).
cnf(t190407,plain,
c(c(X1)) = forward_diamond(one,domain(X1)),
inference(step,[status(thm)],[t263,t271]) ).
cnf(t348,plain,
forward_diamond(one,domain(X1)) = c(c(X1)),
inference(orient,[status(thm)],[t190407]) ).
cnf(t190724,plain,
forward_diamond(one,domain(X1)) = domain(X1),
inference(step,[status(thm)],[t348,t3510]) ).
cnf(t3511,plain,
forward_diamond(one,domain(X1)) = domain(X1),
inference(orient,[status(thm)],[t190724]) ).
cnf(t190731,plain,
domain(X1) = forward_box(one,X1),
inference(step,[status(thm)],[t190730,t3511]) ).
cnf(t3545,plain,
domain(X1) = forward_box(one,X1),
inference(rw,[status(thm)],[t190731]) ).
cnf(t3559,plain,
forward_box(one,X1) = domain(X1),
inference(orient,[status(thm)],[t3545]) ).
cnf(t191095,plain,
domain(coantidomain(X1)) = forward_box(codomain(X1),coantidomain(X1)),
inference(step,[status(thm)],[t191094,t3559]) ).
cnf(t11979,plain,
forward_box(codomain(X1),coantidomain(X1)) = domain(coantidomain(X1)),
inference(orient,[status(thm)],[t191095]) ).
cnf(t191596,plain,
backward_box(X1,zero) = domain(coantidomain(X1)),
inference(step,[status(thm)],[t191595,t11979]) ).
cnf(t23408,plain,
domain(coantidomain(X1)) = backward_box(X1,zero),
inference(orient,[status(thm)],[t191596]) ).
cnf(t23441,plain,
addition(coantidomain(X1),domain(coantidomain(X1))) = multiplication(backward_box(X1,zero),addition(one,coantidomain(X1))),
inference(cp,[status(thm)],[t6661,t23408]) ).
cnf(t191628,plain,
addition(coantidomain(X1),backward_box(X1,zero)) = multiplication(backward_box(X1,zero),addition(one,coantidomain(X1))),
inference(step,[status(thm)],[t23441,t23408]) ).
cnf(t191629,plain,
coantidomain(X1) = multiplication(backward_box(X1,zero),addition(one,coantidomain(X1))),
inference(step,[status(thm)],[t191628,t7123]) ).
fof(f11,axiom,
! [A,B] :
( leq(A,B)
<=> addition(A,B) = B ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',order) ).
fof(f11_nnf,plain,
! [A,B] :
( ( addition(A,B) != B
| leq(A,B) )
& ( addition(A,B) = B
| ~ leq(A,B) ) ),
inference(nnf_transformation,[status(thm)],[f11]) ).
fof(f11_sk,plain,
! [A,B] :
( ( addition(A,B) != B
| leq(A,B) )
& ( addition(A,B) = B
| ~ leq(A,B) ) ),
inference(skolemisation,[status(esa)],[f11_nnf]) ).
cnf(c11,plain,
( addition(X0,X1) = X1
| ~ leq(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f11_sk]) ).
cnf(t26,plain,
ifeq(leq(X1,X2),true,addition(X1,X2),X2) = X2,
inference(equality_encoding,[status(esa)],[c11]) ).
cnf(t39,plain,
ifeq(leq(X1,X2),true,addition(X1,X2),X2) = X2,
inference(orient,[status(thm)],[t26]) ).
cnf(c12,plain,
( addition(X0,X1) != X1
| leq(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f11_sk]) ).
cnf(t25,plain,
ifeq(addition(X1,X2),X2,leq(X1,X2),true) = true,
inference(equality_encoding,[status(esa)],[c12]) ).
cnf(t174,plain,
ifeq(addition(X1,X2),X2,leq(X1,X2),true) = true,
inference(orient,[status(thm)],[t25]) ).
cnf(t630,plain,
true = ifeq(addition(X1,X2),addition(X1,X2),leq(X1,addition(X1,X2)),true),
inference(cp,[status(thm)],[t174,t622]) ).
cnf(t15,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t38,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t15]) ).
cnf(t190453,plain,
true = leq(X1,addition(X1,X2)),
inference(step,[status(thm)],[t630,t38]) ).
cnf(t661,plain,
leq(X1,addition(X1,X2)) = true,
inference(orient,[status(thm)],[t190453]) ).
cnf(t669,plain,
true = leq(X1,addition(X2,X1)),
inference(cp,[status(thm)],[t661,t108]) ).
cnf(t726,plain,
leq(X1,addition(X2,X1)) = true,
inference(orient,[status(thm)],[t669]) ).
cnf(t732,plain,
true = leq(coantidomain(X1),one),
inference(cp,[status(thm)],[t726,t427]) ).
cnf(t739,plain,
leq(coantidomain(X1),one) = true,
inference(orient,[status(thm)],[t732]) ).
cnf(t741,plain,
one = ifeq(true,true,addition(coantidomain(X1),one),one),
inference(cp,[status(thm)],[t39,t739]) ).
cnf(t190454,plain,
one = addition(coantidomain(X1),one),
inference(step,[status(thm)],[t741,t38]) ).
cnf(t190455,plain,
one = addition(one,coantidomain(X1)),
inference(step,[status(thm)],[t190454,t108]) ).
cnf(t749,plain,
addition(one,coantidomain(X1)) = one,
inference(orient,[status(thm)],[t190455]) ).
cnf(t191630,plain,
coantidomain(X1) = multiplication(backward_box(X1,zero),one),
inference(step,[status(thm)],[t191629,t749]) ).
cnf(t191631,plain,
coantidomain(X1) = backward_box(X1,zero),
inference(step,[status(thm)],[t191630,t34]) ).
cnf(t23618,plain,
backward_box(X1,zero) = coantidomain(X1),
inference(orient,[status(thm)],[t191631]) ).
cnf(t191682,plain,
coantidomain(coantidomain(X1)) = c(coantidomain(X1)),
inference(step,[status(thm)],[t4425,t23618]) ).
cnf(t191683,plain,
codomain(X1) = c(coantidomain(X1)),
inference(step,[status(thm)],[t191682,t143]) ).
cnf(t23669,plain,
codomain(X1) = c(coantidomain(X1)),
inference(rw,[status(thm)],[t191683]) ).
cnf(t23687,plain,
c(coantidomain(X1)) = codomain(X1),
inference(orient,[status(thm)],[t23669]) ).
cnf(t3753,plain,
forward_box(X1,codomain(X2)) = c(multiplication(X1,backward_box(X2,zero))),
inference(cp,[status(thm)],[t3743,t462]) ).
cnf(t8223,plain,
c(multiplication(X1,backward_box(X2,zero))) = forward_box(X1,codomain(X2)),
inference(orient,[status(thm)],[t3753]) ).
cnf(t50,plain,
multiplication(X1,addition(coantidomain(X1),X2)) = addition(zero,multiplication(X1,X2)),
inference(cp,[status(thm)],[t43,t47]) ).
cnf(t190563,plain,
multiplication(X1,addition(coantidomain(X1),X2)) = multiplication(X1,X2),
inference(step,[status(thm)],[t50,t233]) ).
cnf(t2443,plain,
multiplication(X1,addition(coantidomain(X1),X2)) = multiplication(X1,X2),
inference(orient,[status(thm)],[t190563]) ).
cnf(t7141,plain,
multiplication(X1,backward_box(X1,zero)) = multiplication(X1,coantidomain(X1)),
inference(cp,[status(thm)],[t2443,t7123]) ).
cnf(t190926,plain,
multiplication(X1,backward_box(X1,zero)) = zero,
inference(step,[status(thm)],[t7141,t47]) ).
cnf(t7143,plain,
multiplication(X1,backward_box(X1,zero)) = zero,
inference(orient,[status(thm)],[t190926]) ).
cnf(t8224,plain,
forward_box(X1,codomain(X1)) = c(zero),
inference(cp,[status(thm)],[t8223,t7143]) ).
cnf(t190979,plain,
forward_box(X1,codomain(X1)) = one,
inference(step,[status(thm)],[t8224,t229]) ).
cnf(t8331,plain,
forward_box(X1,codomain(X1)) = one,
inference(orient,[status(thm)],[t190979]) ).
cnf(t8332,plain,
one = forward_box(multiplication(codomain(X1),X2),backward_diamond(X2,X1)),
inference(cp,[status(thm)],[t8331,t199]) ).
cnf(t40047,plain,
forward_box(multiplication(codomain(X1),X2),backward_diamond(X2,X1)) = one,
inference(orient,[status(thm)],[t8332]) ).
cnf(t4384,plain,
coantidomain(coantidomain(X1)) = codomain(codomain(X1)),
inference(cp,[status(thm)],[t4381,t143]) ).
cnf(t190802,plain,
codomain(X1) = codomain(codomain(X1)),
inference(step,[status(thm)],[t4384,t143]) ).
cnf(t201,plain,
backward_diamond(one,X1) = codomain(codomain(X1)),
inference(cp,[status(thm)],[t199,t34]) ).
cnf(t282,plain,
codomain(codomain(X1)) = backward_diamond(one,X1),
inference(orient,[status(thm)],[t201]) ).
cnf(t190803,plain,
codomain(X1) = backward_diamond(one,X1),
inference(step,[status(thm)],[t190802,t282]) ).
cnf(t4400,plain,
backward_diamond(one,X1) = codomain(X1),
inference(orient,[status(thm)],[t190803]) ).
cnf(t4405,plain,
backward_box(one,X1) = c(codomain(c(X1))),
inference(cp,[status(thm)],[t193,t4400]) ).
cnf(t190815,plain,
backward_box(one,X1) = backward_box(c(X1),zero),
inference(step,[status(thm)],[t4405,t462]) ).
cnf(t4427,plain,
backward_box(c(X1),zero) = backward_box(one,X1),
inference(orient,[status(thm)],[t190815]) ).
cnf(t4439,plain,
backward_box(one,backward_diamond(X1,c(X2))) = backward_box(backward_box(X1,X2),zero),
inference(cp,[status(thm)],[t4427,t193]) ).
cnf(t11314,plain,
backward_box(one,backward_diamond(X1,c(X2))) = backward_box(backward_box(X1,X2),zero),
inference(orient,[status(thm)],[t4439]) ).
cnf(t191640,plain,
backward_box(one,backward_diamond(X1,c(X2))) = coantidomain(backward_box(X1,X2)),
inference(step,[status(thm)],[t11314,t23618]) ).
cnf(t23627,plain,
backward_box(one,backward_diamond(X1,c(X2))) = coantidomain(backward_box(X1,X2)),
inference(orient,[status(thm)],[t191640]) ).
cnf(t4438,plain,
backward_box(one,codomain(X1)) = backward_box(backward_box(X1,zero),zero),
inference(cp,[status(thm)],[t4427,t462]) ).
cnf(t4611,plain,
backward_box(backward_box(X1,zero),zero) = backward_box(one,codomain(X1)),
inference(orient,[status(thm)],[t4438]) ).
cnf(t191677,plain,
coantidomain(backward_box(X1,zero)) = backward_box(one,codomain(X1)),
inference(step,[status(thm)],[t4611,t23618]) ).
cnf(t191678,plain,
coantidomain(coantidomain(X1)) = backward_box(one,codomain(X1)),
inference(step,[status(thm)],[t191677,t23618]) ).
cnf(t191679,plain,
codomain(X1) = backward_box(one,codomain(X1)),
inference(step,[status(thm)],[t191678,t143]) ).
cnf(t23666,plain,
codomain(X1) = backward_box(one,codomain(X1)),
inference(rw,[status(thm)],[t191679]) ).
cnf(t24042,plain,
backward_box(one,codomain(X1)) = codomain(X1),
inference(orient,[status(thm)],[t23666]) ).
cnf(t190804,plain,
codomain(codomain(X1)) = codomain(X1),
inference(step,[status(thm)],[t282,t4400]) ).
cnf(t4401,plain,
codomain(codomain(X1)) = codomain(X1),
inference(orient,[status(thm)],[t190804]) ).
cnf(t4396,plain,
backward_diamond(X1,coantidomain(X2)) = codomain(multiplication(coantidomain(X2),X1)),
inference(cp,[status(thm)],[t199,t4381]) ).
cnf(t4577,plain,
codomain(multiplication(coantidomain(X1),X2)) = backward_diamond(X2,coantidomain(X1)),
inference(orient,[status(thm)],[t4396]) ).
cnf(t4599,plain,
codomain(multiplication(coantidomain(X1),X2)) = codomain(backward_diamond(X2,coantidomain(X1))),
inference(cp,[status(thm)],[t4401,t4577]) ).
cnf(t190824,plain,
backward_diamond(X2,coantidomain(X1)) = codomain(backward_diamond(X2,coantidomain(X1))),
inference(step,[status(thm)],[t4599,t4577]) ).
cnf(t4617,plain,
codomain(backward_diamond(X1,coantidomain(X2))) = backward_diamond(X1,coantidomain(X2)),
inference(orient,[status(thm)],[t190824]) ).
cnf(t4618,plain,
backward_diamond(X1,coantidomain(coantidomain(X2))) = codomain(backward_diamond(X1,codomain(X2))),
inference(cp,[status(thm)],[t4617,t143]) ).
cnf(t190825,plain,
backward_diamond(X1,codomain(X2)) = codomain(backward_diamond(X1,codomain(X2))),
inference(step,[status(thm)],[t4618,t143]) ).
cnf(t4583,plain,
backward_diamond(X1,coantidomain(coantidomain(X2))) = codomain(multiplication(codomain(X2),X1)),
inference(cp,[status(thm)],[t4577,t143]) ).
cnf(t190822,plain,
backward_diamond(X1,codomain(X2)) = codomain(multiplication(codomain(X2),X1)),
inference(step,[status(thm)],[t4583,t143]) ).
cnf(t190823,plain,
backward_diamond(X1,codomain(X2)) = backward_diamond(X1,X2),
inference(step,[status(thm)],[t190822,t199]) ).
cnf(t4606,plain,
backward_diamond(X1,codomain(X2)) = backward_diamond(X1,X2),
inference(orient,[status(thm)],[t190823]) ).
cnf(t190826,plain,
backward_diamond(X1,X2) = codomain(backward_diamond(X1,codomain(X2))),
inference(step,[status(thm)],[t190825,t4606]) ).
cnf(t190827,plain,
backward_diamond(X1,X2) = codomain(backward_diamond(X1,X2)),
inference(step,[status(thm)],[t190826,t4606]) ).
cnf(t4632,plain,
codomain(backward_diamond(X1,X2)) = backward_diamond(X1,X2),
inference(orient,[status(thm)],[t190827]) ).
cnf(t24044,plain,
codomain(backward_diamond(X1,X2)) = backward_box(one,backward_diamond(X1,X2)),
inference(cp,[status(thm)],[t24042,t4632]) ).
cnf(t191787,plain,
backward_diamond(X1,X2) = backward_box(one,backward_diamond(X1,X2)),
inference(step,[status(thm)],[t24044,t4632]) ).
cnf(t24791,plain,
backward_box(one,backward_diamond(X1,X2)) = backward_diamond(X1,X2),
inference(orient,[status(thm)],[t191787]) ).
cnf(t191788,plain,
backward_diamond(X1,c(X2)) = coantidomain(backward_box(X1,X2)),
inference(step,[status(thm)],[t23627,t24791]) ).
cnf(t24808,plain,
backward_diamond(X1,c(X2)) = coantidomain(backward_box(X1,X2)),
inference(rw,[status(thm)],[t191788]) ).
cnf(t24809,plain,
coantidomain(backward_box(X1,X2)) = backward_diamond(X1,c(X2)),
inference(orient,[status(thm)],[t24808]) ).
fof(f17,axiom,
! [X0,X1] : addition(coantidomain(multiplication(X0,X1)),coantidomain(multiplication(coantidomain(coantidomain(X0)),X1))) = coantidomain(multiplication(coantidomain(coantidomain(X0)),X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',codomain2) ).
fof(f17_nnf,plain,
! [X0,X1] : addition(coantidomain(multiplication(X0,X1)),coantidomain(multiplication(coantidomain(coantidomain(X0)),X1))) = coantidomain(multiplication(coantidomain(coantidomain(X0)),X1)),
inference(nnf_transformation,[status(thm)],[f17]) ).
fof(f17_sk,plain,
! [X0,X1] : addition(coantidomain(multiplication(X0,X1)),coantidomain(multiplication(coantidomain(coantidomain(X0)),X1))) = coantidomain(multiplication(coantidomain(coantidomain(X0)),X1)),
inference(skolemisation,[status(esa)],[f17_nnf]) ).
cnf(c18,plain,
addition(coantidomain(multiplication(X0,X1)),coantidomain(multiplication(coantidomain(coantidomain(X0)),X1))) = coantidomain(multiplication(coantidomain(coantidomain(X0)),X1)),
inference(cnf_transformation,[status(esa)],[f17_sk]) ).
cnf(t33,plain,
addition(coantidomain(multiplication(X1,X2)),coantidomain(multiplication(coantidomain(coantidomain(X1)),X2))) = coantidomain(multiplication(coantidomain(coantidomain(X1)),X2)),
inference(equality_encoding,[status(esa)],[c18]) ).
cnf(t127,plain,
addition(coantidomain(multiplication(X1,X2)),coantidomain(multiplication(coantidomain(coantidomain(X1)),X2))) = coantidomain(multiplication(coantidomain(coantidomain(X1)),X2)),
inference(orient,[status(thm)],[t33]) ).
cnf(t190371,plain,
addition(coantidomain(multiplication(X1,X2)),coantidomain(multiplication(codomain(X1),X2))) = coantidomain(multiplication(coantidomain(coantidomain(X1)),X2)),
inference(step,[status(thm)],[t127,t143]) ).
cnf(t190372,plain,
addition(coantidomain(multiplication(X1,X2)),coantidomain(multiplication(codomain(X1),X2))) = coantidomain(multiplication(codomain(X1),X2)),
inference(step,[status(thm)],[t190371,t143]) ).
cnf(t147,plain,
addition(coantidomain(multiplication(X1,X2)),coantidomain(multiplication(codomain(X1),X2))) = coantidomain(multiplication(codomain(X1),X2)),
inference(rw,[status(thm)],[t190372]) ).
cnf(t4600,plain,
coantidomain(multiplication(coantidomain(X1),X2)) = coantidomain(backward_diamond(X2,coantidomain(X1))),
inference(cp,[status(thm)],[t4382,t4577]) ).
cnf(t4647,plain,
coantidomain(backward_diamond(X1,coantidomain(X2))) = coantidomain(multiplication(coantidomain(X2),X1)),
inference(orient,[status(thm)],[t4600]) ).
cnf(t4648,plain,
coantidomain(multiplication(coantidomain(coantidomain(X1)),X2)) = coantidomain(backward_diamond(X2,codomain(X1))),
inference(cp,[status(thm)],[t4647,t143]) ).
cnf(t190828,plain,
coantidomain(multiplication(codomain(X1),X2)) = coantidomain(backward_diamond(X2,codomain(X1))),
inference(step,[status(thm)],[t4648,t143]) ).
cnf(t190829,plain,
coantidomain(multiplication(codomain(X1),X2)) = coantidomain(backward_diamond(X2,X1)),
inference(step,[status(thm)],[t190828,t4606]) ).
cnf(t4660,plain,
coantidomain(multiplication(codomain(X1),X2)) = coantidomain(backward_diamond(X2,X1)),
inference(orient,[status(thm)],[t190829]) ).
cnf(t4639,plain,
backward_box(backward_diamond(X1,X2),zero) = c(backward_diamond(X1,X2)),
inference(cp,[status(thm)],[t462,t4632]) ).
cnf(t4646,plain,
backward_box(backward_diamond(X1,X2),zero) = c(backward_diamond(X1,X2)),
inference(orient,[status(thm)],[t4639]) ).
cnf(t191676,plain,
coantidomain(backward_diamond(X1,X2)) = c(backward_diamond(X1,X2)),
inference(step,[status(thm)],[t4646,t23618]) ).
cnf(t23665,plain,
coantidomain(backward_diamond(X1,X2)) = c(backward_diamond(X1,X2)),
inference(rw,[status(thm)],[t191676]) ).
cnf(t24353,plain,
c(backward_diamond(X1,X2)) = coantidomain(backward_diamond(X1,X2)),
inference(orient,[status(thm)],[t23665]) ).
cnf(t191781,plain,
coantidomain(backward_diamond(X1,c(X2))) = backward_box(X1,X2),
inference(step,[status(thm)],[t193,t24353]) ).
cnf(t24490,plain,
coantidomain(backward_diamond(X1,c(X2))) = backward_box(X1,X2),
inference(rw,[status(thm)],[t191781]) ).
cnf(t24934,plain,
coantidomain(backward_diamond(X1,c(X2))) = backward_box(X1,X2),
inference(orient,[status(thm)],[t24490]) ).
cnf(t24945,plain,
backward_box(X1,coantidomain(X2)) = coantidomain(backward_diamond(X1,codomain(X2))),
inference(cp,[status(thm)],[t24934,t23687]) ).
cnf(t191797,plain,
backward_box(X1,coantidomain(X2)) = coantidomain(backward_diamond(X1,X2)),
inference(step,[status(thm)],[t24945,t4606]) ).
cnf(t25093,plain,
coantidomain(backward_diamond(X1,X2)) = backward_box(X1,coantidomain(X2)),
inference(orient,[status(thm)],[t191797]) ).
cnf(t191798,plain,
coantidomain(multiplication(codomain(X1),X2)) = backward_box(X2,coantidomain(X1)),
inference(step,[status(thm)],[t4660,t25093]) ).
cnf(t25094,plain,
coantidomain(multiplication(codomain(X1),X2)) = backward_box(X2,coantidomain(X1)),
inference(orient,[status(thm)],[t191798]) ).
cnf(t191879,plain,
addition(coantidomain(multiplication(X1,X2)),backward_box(X2,coantidomain(X1))) = coantidomain(multiplication(codomain(X1),X2)),
inference(step,[status(thm)],[t147,t25094]) ).
cnf(t191880,plain,
addition(backward_box(X2,coantidomain(X1)),coantidomain(multiplication(X1,X2))) = coantidomain(multiplication(codomain(X1),X2)),
inference(step,[status(thm)],[t191879,t108]) ).
cnf(t191881,plain,
addition(backward_box(X2,coantidomain(X1)),coantidomain(multiplication(X1,X2))) = backward_box(X2,coantidomain(X1)),
inference(step,[status(thm)],[t191880,t25094]) ).
cnf(t30299,plain,
addition(backward_box(X1,coantidomain(X2)),coantidomain(multiplication(X2,X1))) = backward_box(X1,coantidomain(X2)),
inference(orient,[status(thm)],[t191881]) ).
cnf(t30379,plain,
backward_box(X1,coantidomain(c(X1))) = addition(backward_box(X1,coantidomain(c(X1))),coantidomain(zero)),
inference(cp,[status(thm)],[t30299,t2071]) ).
cnf(t191681,plain,
coantidomain(c(X1)) = backward_box(one,X1),
inference(step,[status(thm)],[t4427,t23618]) ).
cnf(t23668,plain,
coantidomain(c(X1)) = backward_box(one,X1),
inference(rw,[status(thm)],[t191681]) ).
cnf(t23946,plain,
coantidomain(c(X1)) = backward_box(one,X1),
inference(orient,[status(thm)],[t23668]) ).
cnf(t191882,plain,
backward_box(X1,backward_box(one,X1)) = addition(backward_box(X1,coantidomain(c(X1))),coantidomain(zero)),
inference(step,[status(thm)],[t30379,t23946]) ).
cnf(t3520,plain,
domain(backward_diamond(X1,c(X2))) = c(backward_box(X1,X2)),
inference(cp,[status(thm)],[t3510,t193]) ).
cnf(t4009,plain,
domain(backward_diamond(X1,c(X2))) = c(backward_box(X1,X2)),
inference(orient,[status(thm)],[t3520]) ).
cnf(t2049,plain,
c(X1) = multiplication(forward_box(X1,zero),c(X1)),
inference(cp,[status(thm)],[t2038,t320]) ).
cnf(t2501,plain,
multiplication(forward_box(X1,zero),c(X1)) = c(X1),
inference(orient,[status(thm)],[t2049]) ).
cnf(t190711,plain,
multiplication(c(X1),c(X1)) = c(X1),
inference(step,[status(thm)],[t2501,t3491]) ).
cnf(t3502,plain,
multiplication(c(X1),c(X1)) = c(X1),
inference(rw,[status(thm)],[t190711]) ).
cnf(t3692,plain,
multiplication(c(X1),c(X1)) = c(X1),
inference(orient,[status(thm)],[t3502]) ).
cnf(t3710,plain,
forward_diamond(c(X1),c(X1)) = domain(c(X1)),
inference(cp,[status(thm)],[t3450,t3692]) ).
cnf(t190768,plain,
forward_diamond(c(X1),c(X1)) = c(X1),
inference(step,[status(thm)],[t3710,t3494]) ).
cnf(t3734,plain,
forward_diamond(c(X1),c(X1)) = c(X1),
inference(orient,[status(thm)],[t190768]) ).
cnf(t23724,plain,
c(coantidomain(X1)) = forward_diamond(codomain(X1),c(coantidomain(X1))),
inference(cp,[status(thm)],[t3734,t23687]) ).
cnf(t191724,plain,
codomain(X1) = forward_diamond(codomain(X1),c(coantidomain(X1))),
inference(step,[status(thm)],[t23724,t23687]) ).
cnf(t191725,plain,
codomain(X1) = forward_diamond(codomain(X1),codomain(X1)),
inference(step,[status(thm)],[t191724,t23687]) ).
cnf(t1907,plain,
multiplication(X1,addition(codomain(X1),X2)) = addition(X1,multiplication(X1,X2)),
inference(cp,[status(thm)],[t43,t1899]) ).
cnf(t191011,plain,
multiplication(X1,addition(codomain(X1),X2)) = multiplication(X1,addition(one,X2)),
inference(step,[status(thm)],[t1907,t609]) ).
cnf(t9092,plain,
multiplication(X1,addition(codomain(X1),X2)) = multiplication(X1,addition(one,X2)),
inference(orient,[status(thm)],[t191011]) ).
cnf(t6682,plain,
addition(codomain(X1),domain(codomain(X1))) = multiplication(domain(codomain(X1)),one),
inference(cp,[status(thm)],[t6661,t631]) ).
cnf(t190911,plain,
addition(codomain(X1),domain(codomain(X1))) = domain(codomain(X1)),
inference(step,[status(thm)],[t6682,t34]) ).
cnf(t6896,plain,
addition(codomain(X1),domain(codomain(X1))) = domain(codomain(X1)),
inference(orient,[status(thm)],[t190911]) ).
cnf(t9094,plain,
multiplication(X1,addition(one,domain(codomain(X1)))) = multiplication(X1,domain(codomain(X1))),
inference(cp,[status(thm)],[t9092,t6896]) ).
cnf(t191012,plain,
multiplication(X1,one) = multiplication(X1,domain(codomain(X1))),
inference(step,[status(thm)],[t9094,t638]) ).
cnf(t191013,plain,
X1 = multiplication(X1,domain(codomain(X1))),
inference(step,[status(thm)],[t191012,t34]) ).
cnf(t9128,plain,
multiplication(X1,domain(codomain(X1))) = X1,
inference(orient,[status(thm)],[t191013]) ).
cnf(t9158,plain,
forward_diamond(X1,codomain(X1)) = domain(X1),
inference(cp,[status(thm)],[t183,t9128]) ).
cnf(t9160,plain,
forward_diamond(X1,codomain(X1)) = domain(X1),
inference(orient,[status(thm)],[t9158]) ).
cnf(t9165,plain,
domain(codomain(X1)) = forward_diamond(codomain(X1),codomain(X1)),
inference(cp,[status(thm)],[t9160,t4401]) ).
cnf(t9189,plain,
forward_diamond(codomain(X1),codomain(X1)) = domain(codomain(X1)),
inference(orient,[status(thm)],[t9165]) ).
cnf(t191726,plain,
codomain(X1) = domain(codomain(X1)),
inference(step,[status(thm)],[t191725,t9189]) ).
cnf(t23858,plain,
domain(codomain(X1)) = codomain(X1),
inference(orient,[status(thm)],[t191726]) ).
cnf(t23874,plain,
codomain(backward_diamond(X1,X2)) = domain(backward_diamond(X1,X2)),
inference(cp,[status(thm)],[t23858,t4632]) ).
cnf(t191772,plain,
backward_diamond(X1,X2) = domain(backward_diamond(X1,X2)),
inference(step,[status(thm)],[t23874,t4632]) ).
cnf(t24118,plain,
domain(backward_diamond(X1,X2)) = backward_diamond(X1,X2),
inference(orient,[status(thm)],[t191772]) ).
cnf(t191775,plain,
backward_diamond(X1,c(X2)) = c(backward_box(X1,X2)),
inference(step,[status(thm)],[t4009,t24118]) ).
cnf(t24232,plain,
backward_diamond(X1,c(X2)) = c(backward_box(X1,X2)),
inference(rw,[status(thm)],[t191775]) ).
cnf(t24491,plain,
c(backward_box(X1,X2)) = backward_diamond(X1,c(X2)),
inference(orient,[status(thm)],[t24232]) ).
cnf(t24541,plain,
domain(backward_box(X1,X2)) = c(backward_diamond(X1,c(X2))),
inference(cp,[status(thm)],[t3510,t24491]) ).
cnf(t2033,plain,
forward_diamond(addition(X1,antidomain(domain(X2))),X2) = domain(multiplication(X1,domain(X2))),
inference(cp,[status(thm)],[t183,t2006]) ).
cnf(t190595,plain,
forward_diamond(addition(X1,c(X2)),X2) = domain(multiplication(X1,domain(X2))),
inference(step,[status(thm)],[t2033,t104]) ).
cnf(t190596,plain,
forward_diamond(addition(X1,c(X2)),X2) = forward_diamond(X1,X2),
inference(step,[status(thm)],[t190595,t183]) ).
cnf(t2988,plain,
forward_diamond(addition(X1,c(X2)),X2) = forward_diamond(X1,X2),
inference(orient,[status(thm)],[t190596]) ).
cnf(t2989,plain,
forward_diamond(domain(X1),X1) = forward_diamond(one,X1),
inference(cp,[status(thm)],[t2988,t484]) ).
cnf(t3005,plain,
forward_diamond(domain(X1),X1) = forward_diamond(one,X1),
inference(orient,[status(thm)],[t2989]) ).
cnf(t3020,plain,
forward_box(domain(c(X1)),X1) = c(forward_diamond(one,c(X1))),
inference(cp,[status(thm)],[t195,t3005]) ).
cnf(t190599,plain,
forward_box(forward_box(X1,zero),X1) = c(forward_diamond(one,c(X1))),
inference(step,[status(thm)],[t3020,t320]) ).
cnf(t190600,plain,
forward_box(forward_box(X1,zero),X1) = forward_diamond(one,c(c(X1))),
inference(step,[status(thm)],[t190599,t515]) ).
cnf(t190601,plain,
forward_box(forward_box(X1,zero),X1) = forward_box(one,X1),
inference(step,[status(thm)],[t190600,t779]) ).
cnf(t3099,plain,
forward_box(forward_box(X1,zero),X1) = forward_box(one,X1),
inference(orient,[status(thm)],[t190601]) ).
cnf(t190710,plain,
forward_box(c(X1),X1) = forward_box(one,X1),
inference(step,[status(thm)],[t3099,t3491]) ).
cnf(t3501,plain,
forward_box(c(X1),X1) = forward_box(one,X1),
inference(rw,[status(thm)],[t190710]) ).
cnf(t190759,plain,
forward_box(c(X1),X1) = domain(X1),
inference(step,[status(thm)],[t3501,t3559]) ).
cnf(t3606,plain,
forward_box(c(X1),X1) = domain(X1),
inference(orient,[status(thm)],[t190759]) ).
cnf(t3607,plain,
domain(c(X1)) = forward_box(domain(X1),c(X1)),
inference(cp,[status(thm)],[t3606,t3510]) ).
cnf(t190766,plain,
c(X1) = forward_box(domain(X1),c(X1)),
inference(step,[status(thm)],[t3607,t3494]) ).
cnf(t3712,plain,
forward_box(domain(X1),c(X1)) = c(X1),
inference(orient,[status(thm)],[t190766]) ).
cnf(t4027,plain,
c(backward_diamond(X1,c(X2))) = forward_box(c(backward_box(X1,X2)),c(backward_diamond(X1,c(X2)))),
inference(cp,[status(thm)],[t3712,t4009]) ).
cnf(t190779,plain,
backward_box(X1,X2) = forward_box(c(backward_box(X1,X2)),c(backward_diamond(X1,c(X2)))),
inference(step,[status(thm)],[t4027,t193]) ).
cnf(t190780,plain,
backward_box(X1,X2) = forward_box(c(backward_box(X1,X2)),backward_box(X1,X2)),
inference(step,[status(thm)],[t190779,t193]) ).
cnf(t190781,plain,
backward_box(X1,X2) = domain(backward_box(X1,X2)),
inference(step,[status(thm)],[t190780,t3606]) ).
cnf(t4039,plain,
domain(backward_box(X1,X2)) = backward_box(X1,X2),
inference(orient,[status(thm)],[t190781]) ).
cnf(t191809,plain,
backward_box(X1,X2) = c(backward_diamond(X1,c(X2))),
inference(step,[status(thm)],[t24541,t4039]) ).
cnf(t191800,plain,
c(backward_diamond(X1,X2)) = backward_box(X1,coantidomain(X2)),
inference(step,[status(thm)],[t24353,t25093]) ).
cnf(t25096,plain,
c(backward_diamond(X1,X2)) = backward_box(X1,coantidomain(X2)),
inference(orient,[status(thm)],[t191800]) ).
cnf(t191810,plain,
backward_box(X1,X2) = backward_box(X1,coantidomain(c(X2))),
inference(step,[status(thm)],[t191809,t25096]) ).
cnf(t191811,plain,
backward_box(X1,X2) = backward_box(X1,backward_box(one,X2)),
inference(step,[status(thm)],[t191810,t23946]) ).
cnf(t25418,plain,
backward_box(X1,backward_box(one,X2)) = backward_box(X1,X2),
inference(orient,[status(thm)],[t191811]) ).
cnf(t191883,plain,
backward_box(X1,X1) = addition(backward_box(X1,coantidomain(c(X1))),coantidomain(zero)),
inference(step,[status(thm)],[t191882,t25418]) ).
cnf(t191884,plain,
backward_box(X1,X1) = addition(coantidomain(zero),backward_box(X1,coantidomain(c(X1)))),
inference(step,[status(thm)],[t191883,t108]) ).
cnf(t206,plain,
codomain(one) = coantidomain(zero),
inference(cp,[status(thm)],[t143,t205]) ).
cnf(t218,plain,
coantidomain(zero) = codomain(one),
inference(orient,[status(thm)],[t206]) ).
cnf(t190414,plain,
coantidomain(zero) = one,
inference(step,[status(thm)],[t218,t437]) ).
cnf(t438,plain,
coantidomain(zero) = one,
inference(orient,[status(thm)],[t190414]) ).
cnf(t191885,plain,
backward_box(X1,X1) = addition(one,backward_box(X1,coantidomain(c(X1)))),
inference(step,[status(thm)],[t191884,t438]) ).
cnf(t654,plain,
one = addition(one,backward_box(X1,X2)),
inference(cp,[status(thm)],[t649,t193]) ).
cnf(t718,plain,
addition(one,backward_box(X1,X2)) = one,
inference(orient,[status(thm)],[t654]) ).
cnf(t191886,plain,
backward_box(X1,X1) = one,
inference(step,[status(thm)],[t191885,t718]) ).
cnf(t30439,plain,
backward_box(X1,X1) = one,
inference(orient,[status(thm)],[t191886]) ).
cnf(t30442,plain,
backward_diamond(X1,c(X1)) = coantidomain(one),
inference(cp,[status(thm)],[t24809,t30439]) ).
cnf(t191887,plain,
backward_diamond(X1,c(X1)) = zero,
inference(step,[status(thm)],[t30442,t205]) ).
cnf(t30465,plain,
backward_diamond(X1,c(X1)) = zero,
inference(orient,[status(thm)],[t191887]) ).
cnf(t40062,plain,
one = forward_box(multiplication(codomain(c(X1)),X1),zero),
inference(cp,[status(thm)],[t40047,t30465]) ).
cnf(t192063,plain,
one = c(multiplication(codomain(c(X1)),X1)),
inference(step,[status(thm)],[t40062,t3491]) ).
cnf(t40158,plain,
c(multiplication(codomain(c(X1)),X1)) = one,
inference(orient,[status(thm)],[t192063]) ).
cnf(t40207,plain,
zero = multiplication(one,multiplication(codomain(c(X1)),X1)),
inference(cp,[status(thm)],[t2071,t40158]) ).
cnf(t192069,plain,
zero = multiplication(codomain(c(X1)),X1),
inference(step,[status(thm)],[t40207,t35]) ).
cnf(t40351,plain,
multiplication(codomain(c(X1)),X1) = zero,
inference(orient,[status(thm)],[t192069]) ).
cnf(t40363,plain,
multiplication(addition(codomain(c(X1)),X2),X1) = addition(zero,multiplication(X2,X1)),
inference(cp,[status(thm)],[t61,t40351]) ).
cnf(t192098,plain,
multiplication(addition(codomain(c(X1)),X2),X1) = multiplication(X2,X1),
inference(step,[status(thm)],[t40363,t233]) ).
cnf(t41064,plain,
multiplication(addition(codomain(c(X1)),X2),X1) = multiplication(X2,X1),
inference(orient,[status(thm)],[t192098]) ).
cnf(t41068,plain,
multiplication(coantidomain(c(X1)),X1) = multiplication(one,X1),
inference(cp,[status(thm)],[t41064,t427]) ).
cnf(t192099,plain,
multiplication(backward_box(one,X1),X1) = multiplication(one,X1),
inference(step,[status(thm)],[t41068,t23946]) ).
cnf(t192100,plain,
multiplication(backward_box(one,X1),X1) = X1,
inference(step,[status(thm)],[t192099,t35]) ).
cnf(t41162,plain,
multiplication(backward_box(one,X1),X1) = X1,
inference(orient,[status(thm)],[t192100]) ).
cnf(t3975,plain,
domain_difference(c(backward_diamond(X1,c(X2))),X3) = multiplication(backward_box(X1,X2),c(X3)),
inference(cp,[status(thm)],[t3966,t193]) ).
cnf(t191080,plain,
domain_difference(backward_box(X1,X2),X3) = multiplication(backward_box(X1,X2),c(X3)),
inference(step,[status(thm)],[t3975,t193]) ).
cnf(t10685,plain,
multiplication(backward_box(X1,X2),c(X3)) = domain_difference(backward_box(X1,X2),X3),
inference(orient,[status(thm)],[t191080]) ).
cnf(t41163,plain,
c(X1) = domain_difference(backward_box(one,c(X1)),X1),
inference(cp,[status(thm)],[t41162,t10685]) ).
cnf(t3543,plain,
backward_box(X1,c(X2)) = c(backward_diamond(X1,domain(X2))),
inference(cp,[status(thm)],[t193,t3510]) ).
cnf(t4071,plain,
c(backward_diamond(X1,domain(X2))) = backward_box(X1,c(X2)),
inference(orient,[status(thm)],[t3543]) ).
cnf(t4403,plain,
backward_box(one,c(X1)) = c(codomain(domain(X1))),
inference(cp,[status(thm)],[t4071,t4400]) ).
cnf(t190818,plain,
backward_box(one,c(X1)) = backward_box(domain(X1),zero),
inference(step,[status(thm)],[t4403,t462]) ).
cnf(t4479,plain,
backward_box(domain(X1),zero) = backward_box(one,c(X1)),
inference(orient,[status(thm)],[t190818]) ).
cnf(t191680,plain,
coantidomain(domain(X1)) = backward_box(one,c(X1)),
inference(step,[status(thm)],[t4479,t23618]) ).
cnf(t23667,plain,
coantidomain(domain(X1)) = backward_box(one,c(X1)),
inference(rw,[status(thm)],[t191680]) ).
cnf(t24077,plain,
backward_box(one,c(X1)) = coantidomain(domain(X1)),
inference(orient,[status(thm)],[t23667]) ).
cnf(t192101,plain,
c(X1) = domain_difference(coantidomain(domain(X1)),X1),
inference(step,[status(thm)],[t41163,t24077]) ).
cnf(t2088,plain,
multiplication(c(X1),addition(X2,X1)) = addition(multiplication(c(X1),X2),zero),
inference(cp,[status(thm)],[t43,t2071]) ).
cnf(t190957,plain,
multiplication(c(X1),addition(X2,X1)) = multiplication(c(X1),X2),
inference(step,[status(thm)],[t2088,t37]) ).
cnf(t7611,plain,
multiplication(c(X1),addition(X2,X1)) = multiplication(c(X1),X2),
inference(orient,[status(thm)],[t190957]) ).
cnf(t497,plain,
addition(domain(X1),addition(c(X1),X2)) = addition(one,X2),
inference(cp,[status(thm)],[t113,t484]) ).
cnf(t12105,plain,
addition(domain(X1),addition(c(X1),X2)) = addition(one,X2),
inference(orient,[status(thm)],[t497]) ).
cnf(t1904,plain,
multiplication(addition(one,X1),codomain(X1)) = addition(codomain(X1),X1),
inference(cp,[status(thm)],[t1515,t1899]) ).
cnf(t190899,plain,
multiplication(addition(one,X1),codomain(X1)) = addition(X1,codomain(X1)),
inference(step,[status(thm)],[t1904,t108]) ).
cnf(t6528,plain,
multiplication(addition(one,X1),codomain(X1)) = addition(X1,codomain(X1)),
inference(orient,[status(thm)],[t190899]) ).
cnf(t6542,plain,
addition(c(X1),codomain(c(X1))) = multiplication(one,codomain(c(X1))),
inference(cp,[status(thm)],[t6528,t649]) ).
cnf(t190900,plain,
addition(c(X1),codomain(c(X1))) = codomain(c(X1)),
inference(step,[status(thm)],[t6542,t35]) ).
cnf(t6562,plain,
addition(c(X1),codomain(c(X1))) = codomain(c(X1)),
inference(orient,[status(thm)],[t190900]) ).
cnf(t12121,plain,
addition(one,codomain(c(X1))) = addition(domain(X1),codomain(c(X1))),
inference(cp,[status(thm)],[t12105,t6562]) ).
cnf(t191106,plain,
one = addition(domain(X1),codomain(c(X1))),
inference(step,[status(thm)],[t12121,t631]) ).
cnf(t12157,plain,
addition(domain(X1),codomain(c(X1))) = one,
inference(orient,[status(thm)],[t191106]) ).
cnf(t12169,plain,
one = addition(c(X1),codomain(c(c(X1)))),
inference(cp,[status(thm)],[t12157,t3494]) ).
cnf(t191107,plain,
one = addition(c(X1),codomain(domain(X1))),
inference(step,[status(thm)],[t12169,t3510]) ).
cnf(t12200,plain,
addition(c(X1),codomain(domain(X1))) = one,
inference(orient,[status(thm)],[t191107]) ).
cnf(t12230,plain,
multiplication(c(codomain(domain(X1))),c(X1)) = multiplication(c(codomain(domain(X1))),one),
inference(cp,[status(thm)],[t7611,t12200]) ).
cnf(t191118,plain,
domain_difference(c(codomain(domain(X1))),X1) = multiplication(c(codomain(domain(X1))),one),
inference(step,[status(thm)],[t12230,t3966]) ).
cnf(t191119,plain,
domain_difference(backward_box(domain(X1),zero),X1) = multiplication(c(codomain(domain(X1))),one),
inference(step,[status(thm)],[t191118,t462]) ).
cnf(t191120,plain,
domain_difference(backward_box(one,c(X1)),X1) = multiplication(c(codomain(domain(X1))),one),
inference(step,[status(thm)],[t191119,t4479]) ).
cnf(t191121,plain,
domain_difference(backward_box(one,c(X1)),X1) = c(codomain(domain(X1))),
inference(step,[status(thm)],[t191120,t34]) ).
cnf(t191122,plain,
domain_difference(backward_box(one,c(X1)),X1) = backward_box(domain(X1),zero),
inference(step,[status(thm)],[t191121,t462]) ).
cnf(t191123,plain,
domain_difference(backward_box(one,c(X1)),X1) = backward_box(one,c(X1)),
inference(step,[status(thm)],[t191122,t4479]) ).
cnf(t12437,plain,
domain_difference(backward_box(one,c(X1)),X1) = backward_box(one,c(X1)),
inference(orient,[status(thm)],[t191123]) ).
cnf(t12450,plain,
backward_box(one,c(c(X1))) = domain_difference(backward_box(one,domain(X1)),c(X1)),
inference(cp,[status(thm)],[t12437,t3510]) ).
cnf(t191124,plain,
backward_box(one,domain(X1)) = domain_difference(backward_box(one,domain(X1)),c(X1)),
inference(step,[status(thm)],[t12450,t3510]) ).
cnf(t464,plain,
backward_box(codomain(X1),zero) = c(backward_diamond(one,X1)),
inference(cp,[status(thm)],[t462,t282]) ).
cnf(t559,plain,
c(backward_diamond(one,X1)) = backward_box(codomain(X1),zero),
inference(orient,[status(thm)],[t464]) ).
cnf(t560,plain,
backward_box(codomain(c(X1)),zero) = backward_box(one,X1),
inference(cp,[status(thm)],[t559,t193]) ).
cnf(t804,plain,
backward_box(codomain(c(X1)),zero) = backward_box(one,X1),
inference(orient,[status(thm)],[t560]) ).
cnf(t3541,plain,
backward_box(one,c(X1)) = backward_box(codomain(domain(X1)),zero),
inference(cp,[status(thm)],[t804,t3510]) ).
cnf(t4053,plain,
backward_box(codomain(domain(X1)),zero) = backward_box(one,c(X1)),
inference(orient,[status(thm)],[t3541]) ).
cnf(t4058,plain,
backward_box(one,c(c(X1))) = backward_box(codomain(c(X1)),zero),
inference(cp,[status(thm)],[t4053,t3494]) ).
cnf(t190782,plain,
backward_box(one,domain(X1)) = backward_box(codomain(c(X1)),zero),
inference(step,[status(thm)],[t4058,t3510]) ).
cnf(t190783,plain,
backward_box(one,domain(X1)) = backward_box(one,X1),
inference(step,[status(thm)],[t190782,t804]) ).
cnf(t4064,plain,
backward_box(one,domain(X1)) = backward_box(one,X1),
inference(orient,[status(thm)],[t190783]) ).
cnf(t191125,plain,
backward_box(one,X1) = domain_difference(backward_box(one,domain(X1)),c(X1)),
inference(step,[status(thm)],[t191124,t4064]) ).
cnf(t191126,plain,
backward_box(one,X1) = domain_difference(backward_box(one,X1),c(X1)),
inference(step,[status(thm)],[t191125,t4064]) ).
cnf(t12464,plain,
domain_difference(backward_box(one,X1),c(X1)) = backward_box(one,X1),
inference(orient,[status(thm)],[t191126]) ).
cnf(t24091,plain,
backward_box(one,c(X1)) = domain_difference(coantidomain(domain(X1)),c(c(X1))),
inference(cp,[status(thm)],[t12464,t24077]) ).
cnf(t191793,plain,
coantidomain(domain(X1)) = domain_difference(coantidomain(domain(X1)),c(c(X1))),
inference(step,[status(thm)],[t24091,t24077]) ).
cnf(t191794,plain,
coantidomain(domain(X1)) = domain_difference(coantidomain(domain(X1)),domain(X1)),
inference(step,[status(thm)],[t191793,t3510]) ).
cnf(t191795,plain,
coantidomain(domain(X1)) = domain_difference(coantidomain(domain(X1)),X1),
inference(step,[status(thm)],[t191794,t3595]) ).
cnf(t24921,plain,
domain_difference(coantidomain(domain(X1)),X1) = coantidomain(domain(X1)),
inference(orient,[status(thm)],[t191795]) ).
cnf(t192102,plain,
c(X1) = coantidomain(domain(X1)),
inference(step,[status(thm)],[t192101,t24921]) ).
cnf(t41228,plain,
coantidomain(domain(X1)) = c(X1),
inference(orient,[status(thm)],[t192102]) ).
cnf(t41261,plain,
codomain(domain(X1)) = c(c(X1)),
inference(cp,[status(thm)],[t23687,t41228]) ).
cnf(t192205,plain,
codomain(domain(X1)) = domain(X1),
inference(step,[status(thm)],[t41261,t3510]) ).
cnf(t41412,plain,
codomain(domain(X1)) = domain(X1),
inference(orient,[status(thm)],[t192205]) ).
cnf(t194212,plain,
domain_difference(X1,X2) = multiplication(domain_difference(X1,X2),domain(X1)),
inference(step,[status(thm)],[t148287,t41412]) ).
cnf(t150894,plain,
multiplication(domain_difference(X1,X2),domain(X1)) = domain_difference(X1,X2),
inference(orient,[status(thm)],[t194212]) ).
cnf(t972,plain,
domain_difference(antidomain(X1),antidomain(X2)) = multiplication(c(X1),domain(X2)),
inference(cp,[status(thm)],[t966,t252]) ).
cnf(t1689,plain,
domain_difference(antidomain(X1),antidomain(X2)) = multiplication(c(X1),domain(X2)),
inference(orient,[status(thm)],[t972]) ).
cnf(t190660,plain,
domain_difference(c(X1),antidomain(X2)) = multiplication(c(X1),domain(X2)),
inference(step,[status(thm)],[t1689,t3443]) ).
cnf(t190661,plain,
domain_difference(c(X1),c(X2)) = multiplication(c(X1),domain(X2)),
inference(step,[status(thm)],[t190660,t3443]) ).
cnf(t3467,plain,
domain_difference(c(X1),c(X2)) = multiplication(c(X1),domain(X2)),
inference(rw,[status(thm)],[t190661]) ).
cnf(t4163,plain,
domain_difference(c(X1),c(X2)) = multiplication(c(X1),domain(X2)),
inference(orient,[status(thm)],[t3467]) ).
cnf(t150925,plain,
domain_difference(c(X1),c(X2)) = multiplication(multiplication(c(X1),domain(X2)),domain(c(X1))),
inference(cp,[status(thm)],[t150894,t4163]) ).
cnf(t194543,plain,
multiplication(c(X1),domain(X2)) = multiplication(multiplication(c(X1),domain(X2)),domain(c(X1))),
inference(step,[status(thm)],[t150925,t4163]) ).
cnf(t194544,plain,
multiplication(c(X1),domain(X2)) = multiplication(c(X1),multiplication(domain(X2),domain(c(X1)))),
inference(step,[status(thm)],[t194543,t42]) ).
cnf(t190637,plain,
multiplication(domain(X1),domain(X2)) = domain_difference(X1,c(X2)),
inference(step,[status(thm)],[t966,t3443]) ).
cnf(t3446,plain,
multiplication(domain(X1),domain(X2)) = domain_difference(X1,c(X2)),
inference(orient,[status(thm)],[t190637]) ).
cnf(t194545,plain,
multiplication(c(X1),domain(X2)) = multiplication(c(X1),domain_difference(X2,c(c(X1)))),
inference(step,[status(thm)],[t194544,t3446]) ).
cnf(t194546,plain,
multiplication(c(X1),domain(X2)) = multiplication(c(X1),domain_difference(X2,domain(X1))),
inference(step,[status(thm)],[t194545,t3510]) ).
cnf(t194547,plain,
multiplication(c(X1),domain(X2)) = multiplication(c(X1),domain_difference(X2,X1)),
inference(step,[status(thm)],[t194546,t3595]) ).
cnf(t164517,plain,
multiplication(c(X1),domain_difference(X2,X1)) = multiplication(c(X1),domain(X2)),
inference(orient,[status(thm)],[t194547]) ).
cnf(t5944,plain,
zero = multiplication(X1,coantidomain(addition(X2,X1))),
inference(cp,[status(thm)],[t5936,t108]) ).
cnf(t5960,plain,
multiplication(X1,coantidomain(addition(X2,X1))) = zero,
inference(orient,[status(thm)],[t5944]) ).
cnf(t5980,plain,
coantidomain(backward_diamond(coantidomain(addition(X1,codomain(X2))),X2)) = coantidomain(zero),
inference(cp,[status(thm)],[t4660,t5960]) ).
cnf(t192016,plain,
backward_box(coantidomain(addition(X1,codomain(X2))),coantidomain(X2)) = coantidomain(zero),
inference(step,[status(thm)],[t5980,t25093]) ).
cnf(t192017,plain,
backward_box(coantidomain(addition(X1,codomain(X2))),coantidomain(X2)) = one,
inference(step,[status(thm)],[t192016,t438]) ).
cnf(t38371,plain,
backward_box(coantidomain(addition(X1,codomain(X2))),coantidomain(X2)) = one,
inference(orient,[status(thm)],[t192017]) ).
cnf(t1913,plain,
backward_diamond(codomain(codomain(X1)),X1) = codomain(codomain(X1)),
inference(cp,[status(thm)],[t199,t1899]) ).
cnf(t190540,plain,
backward_diamond(backward_diamond(one,X1),X1) = codomain(codomain(X1)),
inference(step,[status(thm)],[t1913,t282]) ).
cnf(t190541,plain,
backward_diamond(backward_diamond(one,X1),X1) = backward_diamond(one,X1),
inference(step,[status(thm)],[t190540,t282]) ).
cnf(t1918,plain,
backward_diamond(backward_diamond(one,X1),X1) = backward_diamond(one,X1),
inference(orient,[status(thm)],[t190541]) ).
cnf(t190807,plain,
backward_diamond(codomain(X1),X1) = backward_diamond(one,X1),
inference(step,[status(thm)],[t1918,t4400]) ).
cnf(t190808,plain,
backward_diamond(codomain(X1),X1) = codomain(X1),
inference(step,[status(thm)],[t190807,t4400]) ).
cnf(t4407,plain,
backward_diamond(codomain(X1),X1) = codomain(X1),
inference(rw,[status(thm)],[t190808]) ).
cnf(t4418,plain,
backward_diamond(codomain(X1),X1) = codomain(X1),
inference(orient,[status(thm)],[t4407]) ).
cnf(t4419,plain,
codomain(coantidomain(X1)) = backward_diamond(coantidomain(X1),coantidomain(X1)),
inference(cp,[status(thm)],[t4418,t4381]) ).
cnf(t190819,plain,
coantidomain(X1) = backward_diamond(coantidomain(X1),coantidomain(X1)),
inference(step,[status(thm)],[t4419,t4381]) ).
cnf(t4538,plain,
backward_diamond(coantidomain(X1),coantidomain(X1)) = coantidomain(X1),
inference(orient,[status(thm)],[t190819]) ).
cnf(t41264,plain,
coantidomain(domain(X1)) = backward_diamond(c(X1),coantidomain(domain(X1))),
inference(cp,[status(thm)],[t4538,t41228]) ).
cnf(t192212,plain,
c(X1) = backward_diamond(c(X1),coantidomain(domain(X1))),
inference(step,[status(thm)],[t41264,t41228]) ).
cnf(t192213,plain,
c(X1) = backward_diamond(c(X1),c(X1)),
inference(step,[status(thm)],[t192212,t41228]) ).
cnf(t2056,plain,
multiplication(addition(domain(X1),X2),X1) = addition(X1,multiplication(X2,X1)),
inference(cp,[status(thm)],[t61,t2038]) ).
cnf(t191033,plain,
multiplication(addition(domain(X1),X2),X1) = multiplication(addition(one,X2),X1),
inference(step,[status(thm)],[t2056,t1515]) ).
cnf(t9430,plain,
multiplication(addition(domain(X1),X2),X1) = multiplication(addition(one,X2),X1),
inference(orient,[status(thm)],[t191033]) ).
cnf(t6543,plain,
addition(domain(X1),codomain(domain(X1))) = multiplication(one,codomain(domain(X1))),
inference(cp,[status(thm)],[t6528,t638]) ).
cnf(t190902,plain,
addition(domain(X1),codomain(domain(X1))) = codomain(domain(X1)),
inference(step,[status(thm)],[t6543,t35]) ).
cnf(t6641,plain,
addition(domain(X1),codomain(domain(X1))) = codomain(domain(X1)),
inference(orient,[status(thm)],[t190902]) ).
cnf(t9431,plain,
multiplication(addition(one,codomain(domain(X1))),X1) = multiplication(codomain(domain(X1)),X1),
inference(cp,[status(thm)],[t9430,t6641]) ).
cnf(t191034,plain,
multiplication(one,X1) = multiplication(codomain(domain(X1)),X1),
inference(step,[status(thm)],[t9431,t631]) ).
cnf(t191035,plain,
X1 = multiplication(codomain(domain(X1)),X1),
inference(step,[status(thm)],[t191034,t35]) ).
cnf(t9477,plain,
multiplication(codomain(domain(X1)),X1) = X1,
inference(orient,[status(thm)],[t191035]) ).
cnf(t9520,plain,
backward_diamond(X1,domain(X1)) = codomain(X1),
inference(cp,[status(thm)],[t199,t9477]) ).
cnf(t9522,plain,
backward_diamond(X1,domain(X1)) = codomain(X1),
inference(orient,[status(thm)],[t9520]) ).
cnf(t9530,plain,
codomain(c(X1)) = backward_diamond(c(X1),c(X1)),
inference(cp,[status(thm)],[t9522,t3494]) ).
cnf(t9596,plain,
backward_diamond(c(X1),c(X1)) = codomain(c(X1)),
inference(orient,[status(thm)],[t9530]) ).
cnf(t192214,plain,
c(X1) = codomain(c(X1)),
inference(step,[status(thm)],[t192213,t9596]) ).
cnf(t41459,plain,
codomain(c(X1)) = c(X1),
inference(orient,[status(thm)],[t192214]) ).
cnf(t41503,plain,
one = backward_box(coantidomain(addition(X1,c(X2))),coantidomain(c(X2))),
inference(cp,[status(thm)],[t38371,t41459]) ).
cnf(t4079,plain,
backward_box(X1,c(c(X2))) = c(backward_diamond(X1,c(X2))),
inference(cp,[status(thm)],[t4071,t3494]) ).
cnf(t190784,plain,
backward_box(X1,domain(X2)) = c(backward_diamond(X1,c(X2))),
inference(step,[status(thm)],[t4079,t3510]) ).
cnf(t190785,plain,
backward_box(X1,domain(X2)) = backward_box(X1,X2),
inference(step,[status(thm)],[t190784,t193]) ).
cnf(t4115,plain,
backward_box(X1,domain(X2)) = backward_box(X1,X2),
inference(orient,[status(thm)],[t190785]) ).
cnf(t41179,plain,
domain(X1) = multiplication(backward_box(one,X1),domain(X1)),
inference(cp,[status(thm)],[t41162,t4115]) ).
cnf(t12189,plain,
multiplication(c(codomain(c(X1))),domain(X1)) = multiplication(c(codomain(c(X1))),one),
inference(cp,[status(thm)],[t7611,t12157]) ).
cnf(t191109,plain,
multiplication(backward_box(c(X1),zero),domain(X1)) = multiplication(c(codomain(c(X1))),one),
inference(step,[status(thm)],[t12189,t462]) ).
cnf(t191110,plain,
multiplication(backward_box(one,X1),domain(X1)) = multiplication(c(codomain(c(X1))),one),
inference(step,[status(thm)],[t191109,t4427]) ).
cnf(t191111,plain,
multiplication(backward_box(one,X1),domain(X1)) = c(codomain(c(X1))),
inference(step,[status(thm)],[t191110,t34]) ).
cnf(t191112,plain,
multiplication(backward_box(one,X1),domain(X1)) = backward_box(c(X1),zero),
inference(step,[status(thm)],[t191111,t462]) ).
cnf(t191113,plain,
multiplication(backward_box(one,X1),domain(X1)) = backward_box(one,X1),
inference(step,[status(thm)],[t191112,t4427]) ).
cnf(t12262,plain,
multiplication(backward_box(one,X1),domain(X1)) = backward_box(one,X1),
inference(orient,[status(thm)],[t191113]) ).
cnf(t192135,plain,
domain(X1) = backward_box(one,X1),
inference(step,[status(thm)],[t41179,t12262]) ).
cnf(t41361,plain,
backward_box(one,X1) = domain(X1),
inference(orient,[status(thm)],[t192135]) ).
cnf(t192140,plain,
coantidomain(c(X1)) = domain(X1),
inference(step,[status(thm)],[t23946,t41361]) ).
cnf(t41366,plain,
coantidomain(c(X1)) = domain(X1),
inference(orient,[status(thm)],[t192140]) ).
cnf(t192279,plain,
one = backward_box(coantidomain(addition(X1,c(X2))),domain(X2)),
inference(step,[status(thm)],[t41503,t41366]) ).
cnf(t192280,plain,
one = backward_box(coantidomain(addition(X1,c(X2))),X2),
inference(step,[status(thm)],[t192279,t4115]) ).
cnf(t45718,plain,
backward_box(coantidomain(addition(X1,c(X2))),X2) = one,
inference(orient,[status(thm)],[t192280]) ).
cnf(t45720,plain,
one = backward_box(coantidomain(forward_box(X1,c(X2))),multiplication(X1,X2)),
inference(cp,[status(thm)],[t45718,t15954]) ).
cnf(t4429,plain,
backward_box(one,forward_diamond(X1,X2)) = backward_box(forward_box(X1,c(X2)),zero),
inference(cp,[status(thm)],[t4427,t3844]) ).
cnf(t11179,plain,
backward_box(forward_box(X1,c(X2)),zero) = backward_box(one,forward_diamond(X1,X2)),
inference(orient,[status(thm)],[t4429]) ).
cnf(t191696,plain,
coantidomain(forward_box(X1,c(X2))) = backward_box(one,forward_diamond(X1,X2)),
inference(step,[status(thm)],[t11179,t23618]) ).
cnf(t23679,plain,
coantidomain(forward_box(X1,c(X2))) = backward_box(one,forward_diamond(X1,X2)),
inference(rw,[status(thm)],[t191696]) ).
cnf(t27090,plain,
coantidomain(forward_box(X1,c(X2))) = backward_box(one,forward_diamond(X1,X2)),
inference(orient,[status(thm)],[t23679]) ).
cnf(t192146,plain,
coantidomain(forward_box(X1,c(X2))) = domain(forward_diamond(X1,X2)),
inference(step,[status(thm)],[t27090,t41361]) ).
cnf(t192147,plain,
coantidomain(forward_box(X1,c(X2))) = forward_diamond(X1,X2),
inference(step,[status(thm)],[t192146,t3614]) ).
cnf(t41372,plain,
coantidomain(forward_box(X1,c(X2))) = forward_diamond(X1,X2),
inference(orient,[status(thm)],[t192147]) ).
cnf(t192322,plain,
one = backward_box(forward_diamond(X1,X2),multiplication(X1,X2)),
inference(step,[status(thm)],[t45720,t41372]) ).
cnf(t47078,plain,
backward_box(forward_diamond(X1,X2),multiplication(X1,X2)) = one,
inference(orient,[status(thm)],[t192322]) ).
cnf(t48,plain,
zero = multiplication(X1,multiplication(X2,coantidomain(multiplication(X1,X2)))),
inference(cp,[status(thm)],[t47,t42]) ).
cnf(t1578,plain,
multiplication(X1,multiplication(X2,coantidomain(multiplication(X1,X2)))) = zero,
inference(orient,[status(thm)],[t48]) ).
cnf(t47096,plain,
one = backward_box(forward_diamond(X1,multiplication(X2,coantidomain(multiplication(X1,X2)))),zero),
inference(cp,[status(thm)],[t47078,t1578]) ).
cnf(t192793,plain,
one = coantidomain(forward_diamond(X1,multiplication(X2,coantidomain(multiplication(X1,X2))))),
inference(step,[status(thm)],[t47096,t23618]) ).
cnf(t41247,plain,
c(forward_diamond(X1,X2)) = coantidomain(forward_diamond(X1,X2)),
inference(cp,[status(thm)],[t41228,t3614]) ).
cnf(t192227,plain,
forward_box(X1,c(X2)) = coantidomain(forward_diamond(X1,X2)),
inference(step,[status(thm)],[t41247,t3844]) ).
cnf(t42120,plain,
coantidomain(forward_diamond(X1,X2)) = forward_box(X1,c(X2)),
inference(orient,[status(thm)],[t192227]) ).
cnf(t192794,plain,
one = forward_box(X1,c(multiplication(X2,coantidomain(multiplication(X1,X2))))),
inference(step,[status(thm)],[t192793,t42120]) ).
cnf(t191700,plain,
c(multiplication(X1,coantidomain(X2))) = forward_box(X1,codomain(X2)),
inference(step,[status(thm)],[t8223,t23618]) ).
cnf(t23683,plain,
c(multiplication(X1,coantidomain(X2))) = forward_box(X1,codomain(X2)),
inference(rw,[status(thm)],[t191700]) ).
cnf(t25832,plain,
c(multiplication(X1,coantidomain(X2))) = forward_box(X1,codomain(X2)),
inference(orient,[status(thm)],[t23683]) ).
cnf(t192795,plain,
one = forward_box(X1,forward_box(X2,codomain(multiplication(X1,X2)))),
inference(step,[status(thm)],[t192794,t25832]) ).
cnf(t72787,plain,
forward_box(X1,forward_box(X2,codomain(multiplication(X1,X2)))) = one,
inference(orient,[status(thm)],[t192795]) ).
cnf(t72900,plain,
zero = multiplication(one,multiplication(X1,c(forward_box(X2,codomain(multiplication(X1,X2)))))),
inference(cp,[status(thm)],[t20771,t72787]) ).
cnf(t193090,plain,
zero = multiplication(X1,c(forward_box(X2,codomain(multiplication(X1,X2))))),
inference(step,[status(thm)],[t72900,t35]) ).
cnf(t193091,plain,
zero = multiplication(X1,forward_diamond(X2,c(codomain(multiplication(X1,X2))))),
inference(step,[status(thm)],[t193090,t3880]) ).
cnf(t191632,plain,
c(codomain(X1)) = coantidomain(X1),
inference(step,[status(thm)],[t462,t23618]) ).
cnf(t23619,plain,
c(codomain(X1)) = coantidomain(X1),
inference(orient,[status(thm)],[t191632]) ).
cnf(t193092,plain,
zero = multiplication(X1,forward_diamond(X2,coantidomain(multiplication(X1,X2)))),
inference(step,[status(thm)],[t193091,t23619]) ).
cnf(t85534,plain,
multiplication(X1,forward_diamond(X2,coantidomain(multiplication(X1,X2)))) = zero,
inference(orient,[status(thm)],[t193092]) ).
cnf(t72794,plain,
one = forward_box(codomain(X1),forward_box(X2,backward_diamond(X2,X1))),
inference(cp,[status(thm)],[t72787,t199]) ).
cnf(t85287,plain,
forward_box(codomain(X1),forward_box(X2,backward_diamond(X2,X1))) = one,
inference(orient,[status(thm)],[t72794]) ).
cnf(t85414,plain,
zero = multiplication(one,multiplication(codomain(X1),c(forward_box(X2,backward_diamond(X2,X1))))),
inference(cp,[status(thm)],[t20771,t85287]) ).
cnf(t193197,plain,
zero = multiplication(codomain(X1),c(forward_box(X2,backward_diamond(X2,X1)))),
inference(step,[status(thm)],[t85414,t35]) ).
cnf(t23720,plain,
domain_difference(c(coantidomain(X1)),X2) = multiplication(codomain(X1),c(X2)),
inference(cp,[status(thm)],[t3966,t23687]) ).
cnf(t191818,plain,
domain_difference(codomain(X1),X2) = multiplication(codomain(X1),c(X2)),
inference(step,[status(thm)],[t23720,t23687]) ).
cnf(t26036,plain,
multiplication(codomain(X1),c(X2)) = domain_difference(codomain(X1),X2),
inference(orient,[status(thm)],[t191818]) ).
cnf(t193198,plain,
zero = domain_difference(codomain(X1),forward_box(X2,backward_diamond(X2,X1))),
inference(step,[status(thm)],[t193197,t26036]) ).
cnf(t88530,plain,
domain_difference(codomain(X1),forward_box(X2,backward_diamond(X2,X1))) = zero,
inference(orient,[status(thm)],[t193198]) ).
cnf(t30476,plain,
zero = backward_diamond(multiplication(X1,c(X2)),forward_box(X1,X2)),
inference(cp,[status(thm)],[t30465,t3743]) ).
cnf(t64413,plain,
backward_diamond(multiplication(X1,c(X2)),forward_box(X1,X2)) = zero,
inference(orient,[status(thm)],[t30476]) ).
cnf(t186,plain,
forward_diamond(multiplication(X1,X2),X3) = domain(multiplication(X1,multiplication(X2,domain(X3)))),
inference(cp,[status(thm)],[t183,t42]) ).
cnf(t41909,plain,
domain(multiplication(X1,multiplication(X2,domain(X3)))) = forward_diamond(multiplication(X1,X2),X3),
inference(orient,[status(thm)],[t186]) ).
cnf(t52,plain,
multiplication(X1,multiplication(coantidomain(X1),X2)) = multiplication(zero,X2),
inference(cp,[status(thm)],[t42,t47]) ).
cnf(t190542,plain,
multiplication(X1,multiplication(coantidomain(X1),X2)) = zero,
inference(step,[status(thm)],[t52,t71]) ).
cnf(t1939,plain,
multiplication(X1,multiplication(coantidomain(X1),X2)) = zero,
inference(orient,[status(thm)],[t190542]) ).
cnf(t16105,plain,
zero = domain_difference(forward_diamond(X1,multiplication(coantidomain(X1),X2)),zero),
inference(cp,[status(thm)],[t16080,t1939]) ).
cnf(t191313,plain,
zero = domain(forward_diamond(X1,multiplication(coantidomain(X1),X2))),
inference(step,[status(thm)],[t16105,t251]) ).
cnf(t191314,plain,
zero = forward_diamond(X1,multiplication(coantidomain(X1),X2)),
inference(step,[status(thm)],[t191313,t3614]) ).
cnf(t16219,plain,
forward_diamond(X1,multiplication(coantidomain(X1),X2)) = zero,
inference(orient,[status(thm)],[t191314]) ).
cnf(t16225,plain,
one = forward_box(forward_diamond(X1,multiplication(coantidomain(X1),X2)),zero),
inference(cp,[status(thm)],[t5773,t16219]) ).
cnf(t191399,plain,
one = c(forward_diamond(X1,multiplication(coantidomain(X1),X2))),
inference(step,[status(thm)],[t16225,t3491]) ).
cnf(t191400,plain,
one = forward_box(X1,c(multiplication(coantidomain(X1),X2))),
inference(step,[status(thm)],[t191399,t3844]) ).
cnf(t17245,plain,
forward_box(X1,c(multiplication(coantidomain(X1),X2))) = one,
inference(orient,[status(thm)],[t191400]) ).
cnf(t20776,plain,
zero = multiplication(one,multiplication(X1,c(c(multiplication(coantidomain(X1),X2))))),
inference(cp,[status(thm)],[t20771,t17245]) ).
cnf(t191516,plain,
zero = multiplication(X1,c(c(multiplication(coantidomain(X1),X2)))),
inference(step,[status(thm)],[t20776,t35]) ).
cnf(t191517,plain,
zero = multiplication(X1,domain(multiplication(coantidomain(X1),X2))),
inference(step,[status(thm)],[t191516,t3510]) ).
cnf(t21459,plain,
multiplication(X1,domain(multiplication(coantidomain(X1),X2))) = zero,
inference(orient,[status(thm)],[t191517]) ).
cnf(t41931,plain,
forward_diamond(multiplication(X1,X2),multiplication(coantidomain(X2),X3)) = domain(multiplication(X1,zero)),
inference(cp,[status(thm)],[t41909,t21459]) ).
fof(f9,axiom,
! [A] : multiplication(A,zero) = zero,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',right_annihilation) ).
fof(f9_nnf,plain,
! [A] : multiplication(A,zero) = zero,
inference(nnf_transformation,[status(thm)],[f9]) ).
fof(f9_sk,plain,
! [A] : multiplication(A,zero) = zero,
inference(skolemisation,[status(esa)],[f9_nnf]) ).
cnf(c9,plain,
multiplication(X0,zero) = zero,
inference(cnf_transformation,[status(esa)],[f9_sk]) ).
cnf(t6,plain,
multiplication(X1,zero) = zero,
inference(equality_encoding,[status(esa)],[c9]) ).
cnf(t53,plain,
multiplication(X1,zero) = zero,
inference(orient,[status(thm)],[t6]) ).
cnf(t192693,plain,
forward_diamond(multiplication(X1,X2),multiplication(coantidomain(X2),X3)) = domain(zero),
inference(step,[status(thm)],[t41931,t53]) ).
cnf(t192694,plain,
forward_diamond(multiplication(X1,X2),multiplication(coantidomain(X2),X3)) = zero,
inference(step,[status(thm)],[t192693,t224]) ).
cnf(t68152,plain,
forward_diamond(multiplication(X1,X2),multiplication(coantidomain(X2),X3)) = zero,
inference(orient,[status(thm)],[t192694]) ).
cnf(t4387,plain,
coantidomain(X1) = multiplication(coantidomain(X1),coantidomain(X1)),
inference(cp,[status(thm)],[t1899,t4381]) ).
cnf(t4516,plain,
multiplication(coantidomain(X1),coantidomain(X1)) = coantidomain(X1),
inference(orient,[status(thm)],[t4387]) ).
cnf(t68175,plain,
zero = forward_diamond(multiplication(X1,X2),coantidomain(X2)),
inference(cp,[status(thm)],[t68152,t4516]) ).
cnf(t68201,plain,
forward_diamond(multiplication(X1,X2),coantidomain(X2)) = zero,
inference(orient,[status(thm)],[t68175]) ).
cnf(t68233,plain,
forward_box(multiplication(X1,X2),c(coantidomain(X2))) = coantidomain(zero),
inference(cp,[status(thm)],[t42120,t68201]) ).
cnf(t192695,plain,
forward_box(multiplication(X1,X2),codomain(X2)) = coantidomain(zero),
inference(step,[status(thm)],[t68233,t23687]) ).
cnf(t192696,plain,
forward_box(multiplication(X1,X2),codomain(X2)) = one,
inference(step,[status(thm)],[t192695,t438]) ).
cnf(t68237,plain,
forward_box(multiplication(X1,X2),codomain(X2)) = one,
inference(orient,[status(thm)],[t192696]) ).
cnf(t1909,plain,
multiplication(X1,multiplication(codomain(X1),X2)) = multiplication(X1,X2),
inference(cp,[status(thm)],[t42,t1899]) ).
cnf(t2797,plain,
multiplication(X1,multiplication(codomain(X1),X2)) = multiplication(X1,X2),
inference(orient,[status(thm)],[t1909]) ).
cnf(t68240,plain,
one = forward_box(multiplication(X1,X2),codomain(multiplication(codomain(X1),X2))),
inference(cp,[status(thm)],[t68237,t2797]) ).
cnf(t192697,plain,
one = forward_box(multiplication(X1,X2),backward_diamond(X2,X1)),
inference(step,[status(thm)],[t68240,t199]) ).
cnf(t68277,plain,
forward_box(multiplication(X1,X2),backward_diamond(X2,X1)) = one,
inference(orient,[status(thm)],[t192697]) ).
cnf(t9497,plain,
multiplication(codomain(domain(X1)),multiplication(X1,X2)) = multiplication(X1,X2),
inference(cp,[status(thm)],[t42,t9477]) ).
cnf(t14251,plain,
multiplication(codomain(domain(X1)),multiplication(X1,X2)) = multiplication(X1,X2),
inference(orient,[status(thm)],[t9497]) ).
cnf(t14321,plain,
backward_diamond(multiplication(X1,X2),domain(X1)) = codomain(multiplication(X1,X2)),
inference(cp,[status(thm)],[t199,t14251]) ).
cnf(t14442,plain,
backward_diamond(multiplication(X1,X2),domain(X1)) = codomain(multiplication(X1,X2)),
inference(orient,[status(thm)],[t14321]) ).
cnf(t2085,plain,
multiplication(addition(c(X1),X2),X1) = addition(zero,multiplication(X2,X1)),
inference(cp,[status(thm)],[t61,t2071]) ).
cnf(t190786,plain,
multiplication(addition(c(X1),X2),X1) = multiplication(X2,X1),
inference(step,[status(thm)],[t2085,t233]) ).
cnf(t4254,plain,
multiplication(addition(c(X1),X2),X1) = multiplication(X2,X1),
inference(orient,[status(thm)],[t190786]) ).
cnf(t3991,plain,
multiplication(c(X1),addition(one,c(X2))) = addition(c(X1),domain_difference(c(X1),X2)),
inference(cp,[status(thm)],[t609,t3966]) ).
cnf(t191001,plain,
multiplication(c(X1),one) = addition(c(X1),domain_difference(c(X1),X2)),
inference(step,[status(thm)],[t3991,t649]) ).
cnf(t191002,plain,
c(X1) = addition(c(X1),domain_difference(c(X1),X2)),
inference(step,[status(thm)],[t191001,t34]) ).
cnf(t8689,plain,
addition(c(X1),domain_difference(c(X1),X2)) = c(X1),
inference(orient,[status(thm)],[t191002]) ).
cnf(t8718,plain,
multiplication(domain_difference(c(X1),X2),X1) = multiplication(c(X1),X1),
inference(cp,[status(thm)],[t4254,t8689]) ).
cnf(t191003,plain,
multiplication(domain_difference(c(X1),X2),X1) = zero,
inference(step,[status(thm)],[t8718,t2071]) ).
cnf(t8720,plain,
multiplication(domain_difference(c(X1),X2),X1) = zero,
inference(orient,[status(thm)],[t191003]) ).
cnf(t8721,plain,
zero = multiplication(multiplication(c(X1),domain(X2)),X1),
inference(cp,[status(thm)],[t8720,t4163]) ).
cnf(t191005,plain,
zero = multiplication(c(X1),multiplication(domain(X2),X1)),
inference(step,[status(thm)],[t8721,t42]) ).
cnf(t8786,plain,
multiplication(c(X1),multiplication(domain(X2),X1)) = zero,
inference(orient,[status(thm)],[t191005]) ).
fof(f26,conjecture,
! [X0,X1,X2] :
( multiplication(forward_diamond(X0,domain(X1)),domain(X2)) = zero
<= multiplication(domain(X1),backward_diamond(X0,domain(X2))) = zero ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goals) ).
fof(f26_neg,negated_conjecture,
~ ! [X0,X1,X2] :
( multiplication(forward_diamond(X0,domain(X1)),domain(X2)) = zero
<= multiplication(domain(X1),backward_diamond(X0,domain(X2))) = zero ),
inference(negated_conjecture,[status(cth)],[f26]) ).
fof(f26_nnf,plain,
? [X0,X1,X2] :
( multiplication(forward_diamond(X0,domain(X1)),domain(X2)) != zero
& multiplication(domain(X1),backward_diamond(X0,domain(X2))) = zero ),
inference(nnf_transformation,[status(thm)],[f26_neg]) ).
fof(f26_sk,plain,
( multiplication(forward_diamond(sk0,domain(sk1)),domain(sk2)) != zero
& multiplication(domain(sk1),backward_diamond(sk0,domain(sk2))) = zero ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk0,sk1,sk2])],[f26_nnf]) ).
cnf(c27,plain,
multiplication(domain(sk1),backward_diamond(sk0,domain(sk2))) = zero,
inference(cnf_transformation,[status(esa)],[f26_sk]) ).
cnf(t23,plain,
multiplication(domain(sk1),backward_diamond(sk0,domain(sk2))) = zero,
inference(equality_encoding,[status(esa)],[c27]) ).
cnf(t79,plain,
multiplication(domain(sk1),backward_diamond(sk0,domain(sk2))) = zero,
inference(orient,[status(thm)],[t23]) ).
cnf(t82,plain,
multiplication(domain(sk1),addition(backward_diamond(sk0,domain(sk2)),X1)) = addition(zero,multiplication(domain(sk1),X1)),
inference(cp,[status(thm)],[t43,t79]) ).
cnf(t191108,plain,
multiplication(domain(sk1),addition(backward_diamond(sk0,domain(sk2)),X1)) = multiplication(domain(sk1),X1),
inference(step,[status(thm)],[t82,t233]) ).
cnf(t12241,plain,
multiplication(domain(sk1),addition(backward_diamond(sk0,domain(sk2)),X1)) = multiplication(domain(sk1),X1),
inference(orient,[status(thm)],[t191108]) ).
cnf(t4640,plain,
one = addition(backward_diamond(X1,X2),coantidomain(backward_diamond(X1,X2))),
inference(cp,[status(thm)],[t427,t4632]) ).
cnf(t191978,plain,
one = addition(backward_diamond(X1,X2),backward_box(X1,coantidomain(X2))),
inference(step,[status(thm)],[t4640,t25093]) ).
cnf(t36011,plain,
addition(backward_diamond(X1,X2),backward_box(X1,coantidomain(X2))) = one,
inference(orient,[status(thm)],[t191978]) ).
cnf(t36070,plain,
multiplication(domain(sk1),backward_box(sk0,coantidomain(domain(sk2)))) = multiplication(domain(sk1),one),
inference(cp,[status(thm)],[t12241,t36011]) ).
cnf(t191780,plain,
coantidomain(backward_diamond(X1,domain(X2))) = backward_box(X1,c(X2)),
inference(step,[status(thm)],[t4071,t24353]) ).
cnf(t24489,plain,
coantidomain(backward_diamond(X1,domain(X2))) = backward_box(X1,c(X2)),
inference(rw,[status(thm)],[t191780]) ).
cnf(t191822,plain,
backward_box(X1,coantidomain(domain(X2))) = backward_box(X1,c(X2)),
inference(step,[status(thm)],[t24489,t25093]) ).
cnf(t26614,plain,
backward_box(X1,coantidomain(domain(X2))) = backward_box(X1,c(X2)),
inference(orient,[status(thm)],[t191822]) ).
cnf(t191979,plain,
multiplication(domain(sk1),backward_box(sk0,c(sk2))) = multiplication(domain(sk1),one),
inference(step,[status(thm)],[t36070,t26614]) ).
cnf(t191980,plain,
multiplication(domain(sk1),backward_box(sk0,c(sk2))) = domain(sk1),
inference(step,[status(thm)],[t191979,t34]) ).
cnf(t36074,plain,
multiplication(domain(sk1),backward_box(sk0,c(sk2))) = domain(sk1),
inference(orient,[status(thm)],[t191980]) ).
cnf(t36094,plain,
zero = multiplication(c(backward_box(sk0,c(sk2))),domain(sk1)),
inference(cp,[status(thm)],[t8786,t36074]) ).
cnf(t4015,plain,
c(backward_box(X1,c(X2))) = domain(backward_diamond(X1,domain(X2))),
inference(cp,[status(thm)],[t4009,t3510]) ).
cnf(t4220,plain,
c(backward_box(X1,c(X2))) = domain(backward_diamond(X1,domain(X2))),
inference(orient,[status(thm)],[t4015]) ).
cnf(t191773,plain,
c(backward_box(X1,c(X2))) = backward_diamond(X1,domain(X2)),
inference(step,[status(thm)],[t4220,t24118]) ).
cnf(t24119,plain,
c(backward_box(X1,c(X2))) = backward_diamond(X1,domain(X2)),
inference(orient,[status(thm)],[t191773]) ).
cnf(t191983,plain,
zero = multiplication(backward_diamond(sk0,domain(sk2)),domain(sk1)),
inference(step,[status(thm)],[t36094,t24119]) ).
cnf(t36110,plain,
multiplication(backward_diamond(sk0,domain(sk2)),domain(sk1)) = zero,
inference(orient,[status(thm)],[t191983]) ).
cnf(t36112,plain,
codomain(multiplication(backward_diamond(sk0,domain(sk2)),domain(sk1))) = backward_diamond(zero,domain(backward_diamond(sk0,domain(sk2)))),
inference(cp,[status(thm)],[t14442,t36110]) ).
cnf(t4645,plain,
backward_diamond(X1,backward_diamond(X2,X3)) = codomain(multiplication(backward_diamond(X2,X3),X1)),
inference(cp,[status(thm)],[t199,t4632]) ).
cnf(t11448,plain,
codomain(multiplication(backward_diamond(X1,X2),X3)) = backward_diamond(X3,backward_diamond(X1,X2)),
inference(orient,[status(thm)],[t4645]) ).
cnf(t191986,plain,
backward_diamond(domain(sk1),backward_diamond(sk0,domain(sk2))) = backward_diamond(zero,domain(backward_diamond(sk0,domain(sk2)))),
inference(step,[status(thm)],[t36112,t11448]) ).
cnf(t200,plain,
backward_diamond(zero,X1) = codomain(zero),
inference(cp,[status(thm)],[t199,t53]) ).
cnf(t243,plain,
backward_diamond(zero,X1) = codomain(zero),
inference(orient,[status(thm)],[t200]) ).
cnf(t441,plain,
codomain(coantidomain(one)) = coantidomain(one),
inference(cp,[status(thm)],[t268,t437]) ).
cnf(t190416,plain,
codomain(zero) = coantidomain(one),
inference(step,[status(thm)],[t441,t205]) ).
cnf(t190417,plain,
codomain(zero) = zero,
inference(step,[status(thm)],[t190416,t205]) ).
cnf(t443,plain,
codomain(zero) = zero,
inference(orient,[status(thm)],[t190417]) ).
cnf(t190418,plain,
backward_diamond(zero,X1) = zero,
inference(step,[status(thm)],[t243,t443]) ).
cnf(t444,plain,
backward_diamond(zero,X1) = zero,
inference(orient,[status(thm)],[t190418]) ).
cnf(t191987,plain,
backward_diamond(domain(sk1),backward_diamond(sk0,domain(sk2))) = zero,
inference(step,[status(thm)],[t191986,t444]) ).
cnf(t36141,plain,
backward_diamond(domain(sk1),backward_diamond(sk0,domain(sk2))) = zero,
inference(orient,[status(thm)],[t191987]) ).
cnf(t4609,plain,
backward_diamond(X1,multiplication(codomain(X2),X3)) = backward_diamond(X1,backward_diamond(X3,X2)),
inference(cp,[status(thm)],[t4606,t199]) ).
cnf(t11429,plain,
backward_diamond(X1,multiplication(codomain(X2),X3)) = backward_diamond(X1,backward_diamond(X3,X2)),
inference(orient,[status(thm)],[t4609]) ).
cnf(t41446,plain,
backward_diamond(X1,backward_diamond(X2,domain(X3))) = backward_diamond(X1,multiplication(domain(X3),X2)),
inference(cp,[status(thm)],[t11429,t41412]) ).
cnf(t105509,plain,
backward_diamond(X1,backward_diamond(X2,domain(X3))) = backward_diamond(X1,multiplication(domain(X3),X2)),
inference(orient,[status(thm)],[t41446]) ).
cnf(t193318,plain,
backward_diamond(domain(sk1),multiplication(domain(sk2),sk0)) = zero,
inference(step,[status(thm)],[t36141,t105509]) ).
cnf(t105658,plain,
backward_diamond(domain(sk1),multiplication(domain(sk2),sk0)) = zero,
inference(rw,[status(thm)],[t193318]) ).
cnf(t105659,plain,
backward_diamond(domain(sk1),multiplication(domain(sk2),sk0)) = zero,
inference(orient,[status(thm)],[t105658]) ).
cnf(t105660,plain,
one = forward_box(multiplication(multiplication(domain(sk2),sk0),domain(sk1)),zero),
inference(cp,[status(thm)],[t68277,t105659]) ).
cnf(t193319,plain,
one = c(multiplication(multiplication(domain(sk2),sk0),domain(sk1))),
inference(step,[status(thm)],[t105660,t3491]) ).
cnf(t193320,plain,
one = forward_box(multiplication(domain(sk2),sk0),c(sk1)),
inference(step,[status(thm)],[t193319,t3845]) ).
cnf(t105662,plain,
forward_box(multiplication(domain(sk2),sk0),c(sk1)) = one,
inference(orient,[status(thm)],[t193320]) ).
cnf(t105671,plain,
zero = backward_diamond(multiplication(multiplication(domain(sk2),sk0),c(c(sk1))),one),
inference(cp,[status(thm)],[t64413,t105662]) ).
cnf(t193324,plain,
zero = codomain(multiplication(multiplication(domain(sk2),sk0),c(c(sk1)))),
inference(step,[status(thm)],[t105671,t460]) ).
cnf(t193325,plain,
zero = codomain(multiplication(domain(sk2),multiplication(sk0,c(c(sk1))))),
inference(step,[status(thm)],[t193324,t42]) ).
cnf(t24975,plain,
coantidomain(backward_diamond(X1,c(X2))) = codomain(backward_box(X1,X2)),
inference(cp,[status(thm)],[t4381,t24934]) ).
cnf(t191796,plain,
backward_box(X1,X2) = codomain(backward_box(X1,X2)),
inference(step,[status(thm)],[t24975,t24934]) ).
cnf(t25035,plain,
codomain(backward_box(X1,X2)) = backward_box(X1,X2),
inference(orient,[status(thm)],[t191796]) ).
cnf(t25088,plain,
backward_diamond(X1,backward_box(X2,X3)) = codomain(multiplication(backward_box(X2,X3),X1)),
inference(cp,[status(thm)],[t199,t25035]) ).
cnf(t33222,plain,
codomain(multiplication(backward_box(X1,X2),X3)) = backward_diamond(X3,backward_box(X1,X2)),
inference(orient,[status(thm)],[t25088]) ).
cnf(t41385,plain,
backward_diamond(X1,backward_box(one,X2)) = codomain(multiplication(domain(X2),X1)),
inference(cp,[status(thm)],[t33222,t41361]) ).
cnf(t192263,plain,
backward_diamond(X1,domain(X2)) = codomain(multiplication(domain(X2),X1)),
inference(step,[status(thm)],[t41385,t41361]) ).
cnf(t43470,plain,
codomain(multiplication(domain(X1),X2)) = backward_diamond(X2,domain(X1)),
inference(orient,[status(thm)],[t192263]) ).
cnf(t193326,plain,
zero = backward_diamond(multiplication(sk0,c(c(sk1))),domain(sk2)),
inference(step,[status(thm)],[t193325,t43470]) ).
cnf(t193327,plain,
zero = backward_diamond(multiplication(sk0,domain(sk1)),domain(sk2)),
inference(step,[status(thm)],[t193326,t3510]) ).
cnf(t105690,plain,
backward_diamond(multiplication(sk0,domain(sk1)),domain(sk2)) = zero,
inference(orient,[status(thm)],[t193327]) ).
cnf(t105699,plain,
zero = domain_difference(codomain(domain(sk2)),forward_box(multiplication(sk0,domain(sk1)),zero)),
inference(cp,[status(thm)],[t88530,t105690]) ).
cnf(t193328,plain,
zero = domain_difference(domain(sk2),forward_box(multiplication(sk0,domain(sk1)),zero)),
inference(step,[status(thm)],[t105699,t41412]) ).
cnf(t3971,plain,
domain_difference(c(c(X1)),X2) = multiplication(domain(X1),c(X2)),
inference(cp,[status(thm)],[t3966,t3510]) ).
cnf(t190777,plain,
domain_difference(domain(X1),X2) = multiplication(domain(X1),c(X2)),
inference(step,[status(thm)],[t3971,t3510]) ).
cnf(t190755,plain,
multiplication(domain(X1),c(X2)) = domain_difference(X1,X2),
inference(step,[status(thm)],[t991,t3595]) ).
cnf(t3596,plain,
multiplication(domain(X1),c(X2)) = domain_difference(X1,X2),
inference(orient,[status(thm)],[t190755]) ).
cnf(t190778,plain,
domain_difference(domain(X1),X2) = domain_difference(X1,X2),
inference(step,[status(thm)],[t190777,t3596]) ).
cnf(t4003,plain,
domain_difference(domain(X1),X2) = domain_difference(X1,X2),
inference(orient,[status(thm)],[t190778]) ).
cnf(t193329,plain,
zero = domain_difference(sk2,forward_box(multiplication(sk0,domain(sk1)),zero)),
inference(step,[status(thm)],[t193328,t4003]) ).
cnf(t193330,plain,
zero = domain_difference(sk2,c(multiplication(sk0,domain(sk1)))),
inference(step,[status(thm)],[t193329,t3491]) ).
cnf(t193331,plain,
zero = domain_difference(sk2,forward_box(sk0,c(sk1))),
inference(step,[status(thm)],[t193330,t3845]) ).
cnf(t3621,plain,
domain_difference(X1,c(forward_diamond(X2,X3))) = multiplication(domain(X1),forward_diamond(X2,X3)),
inference(cp,[status(thm)],[t3446,t3614]) ).
cnf(t193305,plain,
domain_difference(X1,forward_box(X2,c(X3))) = multiplication(domain(X1),forward_diamond(X2,X3)),
inference(step,[status(thm)],[t3621,t3844]) ).
cnf(t94158,plain,
domain_difference(X1,forward_box(X2,c(X3))) = multiplication(domain(X1),forward_diamond(X2,X3)),
inference(orient,[status(thm)],[t193305]) ).
cnf(t193332,plain,
zero = multiplication(domain(sk2),forward_diamond(sk0,sk1)),
inference(step,[status(thm)],[t193331,t94158]) ).
cnf(t105706,plain,
multiplication(domain(sk2),forward_diamond(sk0,sk1)) = zero,
inference(orient,[status(thm)],[t193332]) ).
cnf(t105716,plain,
multiplication(domain(sk2),multiplication(forward_diamond(sk0,sk1),X1)) = multiplication(zero,X1),
inference(cp,[status(thm)],[t42,t105706]) ).
cnf(t193347,plain,
multiplication(domain(sk2),multiplication(forward_diamond(sk0,sk1),X1)) = zero,
inference(step,[status(thm)],[t105716,t71]) ).
cnf(t105843,plain,
multiplication(domain(sk2),multiplication(forward_diamond(sk0,sk1),X1)) = zero,
inference(orient,[status(thm)],[t193347]) ).
cnf(t105898,plain,
zero = multiplication(domain(sk2),forward_diamond(multiplication(forward_diamond(sk0,sk1),X1),coantidomain(zero))),
inference(cp,[status(thm)],[t85534,t105843]) ).
cnf(t193355,plain,
zero = multiplication(domain(sk2),forward_diamond(multiplication(forward_diamond(sk0,sk1),X1),one)),
inference(step,[status(thm)],[t105898,t438]) ).
cnf(t193356,plain,
zero = multiplication(domain(sk2),domain(multiplication(forward_diamond(sk0,sk1),X1))),
inference(step,[status(thm)],[t193355,t246]) ).
cnf(t193357,plain,
zero = domain_difference(sk2,c(multiplication(forward_diamond(sk0,sk1),X1))),
inference(step,[status(thm)],[t193356,t3446]) ).
cnf(t106045,plain,
domain_difference(sk2,c(multiplication(forward_diamond(sk0,sk1),X1))) = zero,
inference(orient,[status(thm)],[t193357]) ).
cnf(t164580,plain,
multiplication(c(c(multiplication(forward_diamond(sk0,sk1),X1))),domain(sk2)) = multiplication(c(c(multiplication(forward_diamond(sk0,sk1),X1))),zero),
inference(cp,[status(thm)],[t164517,t106045]) ).
cnf(t195024,plain,
multiplication(domain(multiplication(forward_diamond(sk0,sk1),X1)),domain(sk2)) = multiplication(c(c(multiplication(forward_diamond(sk0,sk1),X1))),zero),
inference(step,[status(thm)],[t164580,t3510]) ).
cnf(t195025,plain,
domain_difference(multiplication(forward_diamond(sk0,sk1),X1),c(sk2)) = multiplication(c(c(multiplication(forward_diamond(sk0,sk1),X1))),zero),
inference(step,[status(thm)],[t195024,t3446]) ).
cnf(t195026,plain,
domain_difference(multiplication(forward_diamond(sk0,sk1),X1),c(sk2)) = zero,
inference(step,[status(thm)],[t195025,t53]) ).
cnf(t190254,plain,
domain_difference(multiplication(forward_diamond(sk0,sk1),X1),c(sk2)) = zero,
inference(orient,[status(thm)],[t195026]) ).
cnf(t3618,plain,
forward_diamond(X1,X2) = multiplication(forward_diamond(X1,X2),forward_diamond(X1,X2)),
inference(cp,[status(thm)],[t2038,t3614]) ).
cnf(t12852,plain,
multiplication(forward_diamond(X1,X2),forward_diamond(X1,X2)) = forward_diamond(X1,X2),
inference(orient,[status(thm)],[t3618]) ).
cnf(t190257,plain,
zero = domain_difference(forward_diamond(sk0,sk1),c(sk2)),
inference(cp,[status(thm)],[t190254,t12852]) ).
cnf(t3620,plain,
domain_difference(forward_diamond(X1,X2),c(X3)) = multiplication(forward_diamond(X1,X2),domain(X3)),
inference(cp,[status(thm)],[t3446,t3614]) ).
cnf(t94007,plain,
domain_difference(forward_diamond(X1,X2),c(X3)) = multiplication(forward_diamond(X1,X2),domain(X3)),
inference(orient,[status(thm)],[t3620]) ).
cnf(t195027,plain,
zero = multiplication(forward_diamond(sk0,sk1),domain(sk2)),
inference(step,[status(thm)],[t190257,t94007]) ).
cnf(t190300,plain,
multiplication(forward_diamond(sk0,sk1),domain(sk2)) = zero,
inference(orient,[status(thm)],[t195027]) ).
cnf(c28,plain,
multiplication(forward_diamond(sk0,domain(sk1)),domain(sk2)) != zero,
inference(cnf_transformation,[status(esa)],[f26_sk]) ).
cnf(goal_0,negated_conjecture,
multiplication(forward_diamond(sk0,domain(sk1)),domain(sk2)) != zero,
inference(equality_encoding,[status(esa)],[c28]) ).
cnf(g0_0,plain,
multiplication(forward_diamond(sk0,sk1),domain(sk2)) != zero,
inference(rw,[status(thm)],[goal_0,t3645]) ).
cnf(g0_1,plain,
zero != zero,
inference(rw,[status(thm)],[g0_0,t190300]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : KLE102+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.06/0.34 % Computer : n020.cluster.edu
% 0.06/0.34 % Model : x86_64 x86_64
% 0.06/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.06/0.34 % Memory : 8046.5625MB
% 0.06/0.34 % OS : Linux 6.8.0-71-generic
% 0.06/0.34 % CPULimit : 300
% 0.06/0.34 % WCLimit : 300
% 0.06/0.34 % DateTime : Wed Sep 23 18:56:48 UTC 2026
% 0.06/0.35 % CPUTime :
% 0.06/0.35 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 158.43/20.76 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 158.43/20.76 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------