%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : KLE099+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 : n010.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:36 PM UTC 2026
% Result : Theorem 249.89s 32.44s
% Output : Proof 249.89s
% Verified :
% SZS Type : Refutation
% Derivation depth : 134
% Number of leaves : 28
% Syntax : Number of formulae : 950 ( 941 unt; 0 def)
% Number of atoms : 963 ( 955 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 26 ( 13 ~; 6 |; 4 &)
% ( 1 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 1 avg)
% Maximal term depth : 6 ( 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 : 1352 ( 103 sgn 135 !; 3 ?)
% Comments :
%------------------------------------------------------------------------------
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(t58,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(t73,plain,
multiplication(antidomain(X1),X1) = zero,
inference(orient,[status(thm)],[t13]) ).
cnf(t77,plain,
multiplication(antidomain(X1),addition(X1,X2)) = addition(zero,multiplication(antidomain(X1),X2)),
inference(cp,[status(thm)],[t58,t73]) ).
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(t103,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(t39,plain,
addition(X1,zero) = X1,
inference(orient,[status(thm)],[t1]) ).
cnf(t104,plain,
addition(zero,X1) = X1,
inference(cp,[status(thm)],[t103,t39]) ).
cnf(t233,plain,
addition(zero,X1) = X1,
inference(orient,[status(thm)],[t104]) ).
cnf(t377306,plain,
multiplication(antidomain(X1),addition(X1,X2)) = multiplication(antidomain(X1),X2),
inference(step,[status(thm)],[t77,t233]) ).
cnf(t4592,plain,
multiplication(antidomain(X1),addition(X1,X2)) = multiplication(antidomain(X1),X2),
inference(orient,[status(thm)],[t377306]) ).
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(t376964,plain,
addition(antidomain(X1),antidomain(antidomain(X1))) = one,
inference(step,[status(thm)],[t16,t103]) ).
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(t44,plain,
antidomain(antidomain(X1)) = domain(X1),
inference(orient,[status(thm)],[t9]) ).
cnf(t376965,plain,
addition(antidomain(X1),domain(X1)) = one,
inference(step,[status(thm)],[t376964,t44]) ).
cnf(t376966,plain,
addition(domain(X1),antidomain(X1)) = one,
inference(step,[status(thm)],[t376965,t103]) ).
cnf(t119,plain,
addition(domain(X1),antidomain(X1)) = one,
inference(orient,[status(thm)],[t376966]) ).
cnf(t4608,plain,
multiplication(antidomain(domain(X1)),antidomain(X1)) = multiplication(antidomain(domain(X1)),one),
inference(cp,[status(thm)],[t4592,t119]) ).
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(t53,plain,
antidomain(domain(X1)) = c(X1),
inference(orient,[status(thm)],[t10]) ).
cnf(t377307,plain,
multiplication(c(X1),antidomain(X1)) = multiplication(antidomain(domain(X1)),one),
inference(step,[status(thm)],[t4608,t53]) ).
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(t94,plain,
multiplication(domain(X1),antidomain(X2)) = domain_difference(X1,X2),
inference(orient,[status(thm)],[t22]) ).
cnf(t45,plain,
domain(antidomain(X1)) = antidomain(domain(X1)),
inference(cp,[status(thm)],[t44,t44]) ).
cnf(t376994,plain,
domain(antidomain(X1)) = c(X1),
inference(step,[status(thm)],[t45,t53]) ).
cnf(t252,plain,
domain(antidomain(X1)) = c(X1),
inference(orient,[status(thm)],[t376994]) ).
cnf(t256,plain,
domain_difference(antidomain(X1),X2) = multiplication(c(X1),antidomain(X2)),
inference(cp,[status(thm)],[t94,t252]) ).
cnf(t1041,plain,
multiplication(c(X1),antidomain(X2)) = domain_difference(antidomain(X1),X2),
inference(orient,[status(thm)],[t256]) ).
cnf(t377308,plain,
domain_difference(antidomain(X1),X1) = multiplication(antidomain(domain(X1)),one),
inference(step,[status(thm)],[t377307,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(t82,plain,
addition(multiplication(X1,X2),multiplication(X3,X2)) = multiplication(addition(X1,X3),X2),
inference(orient,[status(thm)],[t29]) ).
cnf(t88,plain,
multiplication(addition(X1,antidomain(X2)),X2) = addition(multiplication(X1,X2),zero),
inference(cp,[status(thm)],[t82,t73]) ).
cnf(t377156,plain,
multiplication(addition(X1,antidomain(X2)),X2) = multiplication(X1,X2),
inference(step,[status(thm)],[t88,t39]) ).
cnf(t2114,plain,
multiplication(addition(X1,antidomain(X2)),X2) = multiplication(X1,X2),
inference(orient,[status(thm)],[t377156]) ).
cnf(t2115,plain,
multiplication(domain(X1),X1) = multiplication(one,X1),
inference(cp,[status(thm)],[t2114,t119]) ).
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(t37,plain,
multiplication(one,X1) = X1,
inference(orient,[status(thm)],[t7]) ).
cnf(t377157,plain,
multiplication(domain(X1),X1) = X1,
inference(step,[status(thm)],[t2115,t37]) ).
cnf(t2153,plain,
multiplication(domain(X1),X1) = X1,
inference(orient,[status(thm)],[t377157]) ).
cnf(t2155,plain,
antidomain(X1) = domain_difference(antidomain(X1),X1),
inference(cp,[status(thm)],[t2153,t94]) ).
cnf(t2239,plain,
domain_difference(antidomain(X1),X1) = antidomain(X1),
inference(orient,[status(thm)],[t2155]) ).
cnf(t377309,plain,
antidomain(X1) = multiplication(antidomain(domain(X1)),one),
inference(step,[status(thm)],[t377308,t2239]) ).
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(t36,plain,
multiplication(X1,one) = X1,
inference(orient,[status(thm)],[t5]) ).
cnf(t377310,plain,
antidomain(X1) = antidomain(domain(X1)),
inference(step,[status(thm)],[t377309,t36]) ).
cnf(t377311,plain,
antidomain(X1) = c(X1),
inference(step,[status(thm)],[t377310,t53]) ).
cnf(t4627,plain,
antidomain(X1) = c(X1),
inference(orient,[status(thm)],[t377311]) ).
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(t62,plain,
multiplication(X1,coantidomain(X1)) = zero,
inference(orient,[status(thm)],[t12]) ).
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(t142,plain,
coantidomain(coantidomain(X1)) = codomain(X1),
inference(orient,[status(thm)],[t11]) ).
cnf(t143,plain,
codomain(coantidomain(X1)) = coantidomain(codomain(X1)),
inference(cp,[status(thm)],[t142,t142]) ).
cnf(t269,plain,
coantidomain(codomain(X1)) = codomain(coantidomain(X1)),
inference(orient,[status(thm)],[t143]) ).
cnf(t83,plain,
multiplication(addition(X1,X2),coantidomain(X1)) = addition(zero,multiplication(X2,coantidomain(X1))),
inference(cp,[status(thm)],[t82,t62]) ).
cnf(t377494,plain,
multiplication(addition(X1,X2),coantidomain(X1)) = multiplication(X2,coantidomain(X1)),
inference(step,[status(thm)],[t83,t233]) ).
cnf(t5466,plain,
multiplication(addition(X1,X2),coantidomain(X1)) = multiplication(X2,coantidomain(X1)),
inference(orient,[status(thm)],[t377494]) ).
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(t376967,plain,
addition(coantidomain(X1),coantidomain(coantidomain(X1))) = one,
inference(step,[status(thm)],[t17,t103]) ).
cnf(t136,plain,
addition(coantidomain(X1),coantidomain(coantidomain(X1))) = one,
inference(orient,[status(thm)],[t376967]) ).
cnf(t376969,plain,
addition(coantidomain(X1),codomain(X1)) = one,
inference(step,[status(thm)],[t136,t142]) ).
cnf(t145,plain,
addition(coantidomain(X1),codomain(X1)) = one,
inference(rw,[status(thm)],[t376969]) ).
cnf(t377016,plain,
addition(codomain(X1),coantidomain(X1)) = one,
inference(step,[status(thm)],[t145,t103]) ).
cnf(t435,plain,
addition(codomain(X1),coantidomain(X1)) = one,
inference(orient,[status(thm)],[t377016]) ).
cnf(t5471,plain,
multiplication(coantidomain(X1),coantidomain(codomain(X1))) = multiplication(one,coantidomain(codomain(X1))),
inference(cp,[status(thm)],[t5466,t435]) ).
cnf(t377495,plain,
multiplication(coantidomain(X1),codomain(coantidomain(X1))) = multiplication(one,coantidomain(codomain(X1))),
inference(step,[status(thm)],[t5471,t269]) ).
cnf(t66,plain,
multiplication(X1,addition(X2,coantidomain(X1))) = addition(multiplication(X1,X2),zero),
inference(cp,[status(thm)],[t58,t62]) ).
cnf(t377149,plain,
multiplication(X1,addition(X2,coantidomain(X1))) = multiplication(X1,X2),
inference(step,[status(thm)],[t66,t39]) ).
cnf(t1975,plain,
multiplication(X1,addition(X2,coantidomain(X1))) = multiplication(X1,X2),
inference(orient,[status(thm)],[t377149]) ).
cnf(t1977,plain,
multiplication(X1,codomain(X1)) = multiplication(X1,one),
inference(cp,[status(thm)],[t1975,t435]) ).
cnf(t377150,plain,
multiplication(X1,codomain(X1)) = X1,
inference(step,[status(thm)],[t1977,t36]) ).
cnf(t1999,plain,
multiplication(X1,codomain(X1)) = X1,
inference(orient,[status(thm)],[t377150]) ).
cnf(t377496,plain,
coantidomain(X1) = multiplication(one,coantidomain(codomain(X1))),
inference(step,[status(thm)],[t377495,t1999]) ).
cnf(t377497,plain,
coantidomain(X1) = coantidomain(codomain(X1)),
inference(step,[status(thm)],[t377496,t37]) ).
cnf(t377498,plain,
coantidomain(X1) = codomain(coantidomain(X1)),
inference(step,[status(thm)],[t377497,t269]) ).
cnf(t5494,plain,
codomain(coantidomain(X1)) = coantidomain(X1),
inference(orient,[status(thm)],[t377498]) ).
cnf(t377499,plain,
coantidomain(codomain(X1)) = coantidomain(X1),
inference(step,[status(thm)],[t269,t5494]) ).
cnf(t5495,plain,
coantidomain(codomain(X1)) = coantidomain(X1),
inference(orient,[status(thm)],[t377499]) ).
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(t200,plain,
codomain(multiplication(codomain(X1),X2)) = backward_diamond(X2,X1),
inference(orient,[status(thm)],[t20]) ).
cnf(t5510,plain,
backward_diamond(X1,coantidomain(X2)) = codomain(multiplication(coantidomain(X2),X1)),
inference(cp,[status(thm)],[t200,t5494]) ).
cnf(t5732,plain,
codomain(multiplication(coantidomain(X1),X2)) = backward_diamond(X2,coantidomain(X1)),
inference(orient,[status(thm)],[t5510]) ).
cnf(t5757,plain,
coantidomain(multiplication(coantidomain(X1),X2)) = coantidomain(backward_diamond(X2,coantidomain(X1))),
inference(cp,[status(thm)],[t5495,t5732]) ).
cnf(t5892,plain,
coantidomain(backward_diamond(X1,coantidomain(X2))) = coantidomain(multiplication(coantidomain(X2),X1)),
inference(orient,[status(thm)],[t5757]) ).
cnf(t5893,plain,
coantidomain(multiplication(coantidomain(coantidomain(X1)),X2)) = coantidomain(backward_diamond(X2,codomain(X1))),
inference(cp,[status(thm)],[t5892,t142]) ).
cnf(t377539,plain,
coantidomain(multiplication(codomain(X1),X2)) = coantidomain(backward_diamond(X2,codomain(X1))),
inference(step,[status(thm)],[t5893,t142]) ).
cnf(t5738,plain,
backward_diamond(X1,coantidomain(coantidomain(X2))) = codomain(multiplication(codomain(X2),X1)),
inference(cp,[status(thm)],[t5732,t142]) ).
cnf(t377533,plain,
backward_diamond(X1,codomain(X2)) = codomain(multiplication(codomain(X2),X1)),
inference(step,[status(thm)],[t5738,t142]) ).
cnf(t377534,plain,
backward_diamond(X1,codomain(X2)) = backward_diamond(X1,X2),
inference(step,[status(thm)],[t377533,t200]) ).
cnf(t5768,plain,
backward_diamond(X1,codomain(X2)) = backward_diamond(X1,X2),
inference(orient,[status(thm)],[t377534]) ).
cnf(t377540,plain,
coantidomain(multiplication(codomain(X1),X2)) = coantidomain(backward_diamond(X2,X1)),
inference(step,[status(thm)],[t377539,t5768]) ).
cnf(t5915,plain,
coantidomain(multiplication(codomain(X1),X2)) = coantidomain(backward_diamond(X2,X1)),
inference(orient,[status(thm)],[t377540]) ).
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(t196,plain,
c(backward_diamond(X1,c(X2))) = backward_box(X1,X2),
inference(orient,[status(thm)],[t18]) ).
cnf(t74,plain,
zero = antidomain(one),
inference(cp,[status(thm)],[t73,t36]) ).
cnf(t208,plain,
antidomain(one) = zero,
inference(orient,[status(thm)],[t74]) ).
cnf(t211,plain,
domain(one) = antidomain(zero),
inference(cp,[status(thm)],[t44,t208]) ).
cnf(t209,plain,
one = addition(domain(one),zero),
inference(cp,[status(thm)],[t119,t208]) ).
cnf(t376979,plain,
one = domain(one),
inference(step,[status(thm)],[t209,t39]) ).
cnf(t212,plain,
domain(one) = one,
inference(orient,[status(thm)],[t376979]) ).
cnf(t376981,plain,
one = antidomain(zero),
inference(step,[status(thm)],[t211,t212]) ).
cnf(t221,plain,
antidomain(zero) = one,
inference(orient,[status(thm)],[t376981]) ).
cnf(t224,plain,
domain(zero) = antidomain(one),
inference(cp,[status(thm)],[t44,t221]) ).
cnf(t376982,plain,
domain(zero) = zero,
inference(step,[status(thm)],[t224,t208]) ).
cnf(t225,plain,
domain(zero) = zero,
inference(orient,[status(thm)],[t376982]) ).
cnf(t228,plain,
c(zero) = antidomain(zero),
inference(cp,[status(thm)],[t53,t225]) ).
cnf(t376983,plain,
c(zero) = one,
inference(step,[status(thm)],[t228,t221]) ).
cnf(t230,plain,
c(zero) = one,
inference(orient,[status(thm)],[t376983]) ).
cnf(t231,plain,
backward_box(X1,zero) = c(backward_diamond(X1,one)),
inference(cp,[status(thm)],[t196,t230]) ).
cnf(t322,plain,
c(backward_diamond(X1,one)) = backward_box(X1,zero),
inference(orient,[status(thm)],[t231]) ).
cnf(t64,plain,
zero = coantidomain(one),
inference(cp,[status(thm)],[t62,t37]) ).
cnf(t206,plain,
coantidomain(one) = zero,
inference(orient,[status(thm)],[t64]) ).
cnf(t441,plain,
one = addition(codomain(one),zero),
inference(cp,[status(thm)],[t435,t206]) ).
cnf(t377017,plain,
one = codomain(one),
inference(step,[status(thm)],[t441,t39]) ).
cnf(t445,plain,
codomain(one) = one,
inference(orient,[status(thm)],[t377017]) ).
cnf(t450,plain,
backward_diamond(X1,one) = codomain(multiplication(one,X1)),
inference(cp,[status(thm)],[t200,t445]) ).
cnf(t377035,plain,
backward_diamond(X1,one) = codomain(X1),
inference(step,[status(thm)],[t450,t37]) ).
cnf(t468,plain,
backward_diamond(X1,one) = codomain(X1),
inference(orient,[status(thm)],[t377035]) ).
cnf(t377036,plain,
c(codomain(X1)) = backward_box(X1,zero),
inference(step,[status(thm)],[t322,t468]) ).
cnf(t469,plain,
c(codomain(X1)) = backward_box(X1,zero),
inference(rw,[status(thm)],[t377036]) ).
cnf(t470,plain,
c(codomain(X1)) = backward_box(X1,zero),
inference(orient,[status(thm)],[t469]) ).
cnf(t202,plain,
backward_diamond(one,X1) = codomain(codomain(X1)),
inference(cp,[status(thm)],[t200,t36]) ).
cnf(t284,plain,
codomain(codomain(X1)) = backward_diamond(one,X1),
inference(orient,[status(thm)],[t202]) ).
cnf(t5497,plain,
coantidomain(coantidomain(X1)) = codomain(codomain(X1)),
inference(cp,[status(thm)],[t5494,t142]) ).
cnf(t377506,plain,
codomain(X1) = codomain(codomain(X1)),
inference(step,[status(thm)],[t5497,t142]) ).
cnf(t377507,plain,
codomain(X1) = backward_diamond(one,X1),
inference(step,[status(thm)],[t377506,t284]) ).
cnf(t5516,plain,
backward_diamond(one,X1) = codomain(X1),
inference(orient,[status(thm)],[t377507]) ).
cnf(t377508,plain,
codomain(codomain(X1)) = codomain(X1),
inference(step,[status(thm)],[t284,t5516]) ).
cnf(t5517,plain,
codomain(codomain(X1)) = codomain(X1),
inference(orient,[status(thm)],[t377508]) ).
cnf(t5756,plain,
codomain(multiplication(coantidomain(X1),X2)) = codomain(backward_diamond(X2,coantidomain(X1))),
inference(cp,[status(thm)],[t5517,t5732]) ).
cnf(t377535,plain,
backward_diamond(X2,coantidomain(X1)) = codomain(backward_diamond(X2,coantidomain(X1))),
inference(step,[status(thm)],[t5756,t5732]) ).
cnf(t5780,plain,
codomain(backward_diamond(X1,coantidomain(X2))) = backward_diamond(X1,coantidomain(X2)),
inference(orient,[status(thm)],[t377535]) ).
cnf(t5781,plain,
backward_diamond(X1,coantidomain(coantidomain(X2))) = codomain(backward_diamond(X1,codomain(X2))),
inference(cp,[status(thm)],[t5780,t142]) ).
cnf(t377536,plain,
backward_diamond(X1,codomain(X2)) = codomain(backward_diamond(X1,codomain(X2))),
inference(step,[status(thm)],[t5781,t142]) ).
cnf(t377537,plain,
backward_diamond(X1,X2) = codomain(backward_diamond(X1,codomain(X2))),
inference(step,[status(thm)],[t377536,t5768]) ).
cnf(t377538,plain,
backward_diamond(X1,X2) = codomain(backward_diamond(X1,X2)),
inference(step,[status(thm)],[t377537,t5768]) ).
cnf(t5798,plain,
codomain(backward_diamond(X1,X2)) = backward_diamond(X1,X2),
inference(orient,[status(thm)],[t377538]) ).
cnf(t5806,plain,
backward_box(backward_diamond(X1,X2),zero) = c(backward_diamond(X1,X2)),
inference(cp,[status(thm)],[t470,t5798]) ).
cnf(t5815,plain,
backward_box(backward_diamond(X1,X2),zero) = c(backward_diamond(X1,X2)),
inference(orient,[status(thm)],[t5806]) ).
cnf(t59,plain,
multiplication(X1,addition(one,X2)) = addition(X1,multiplication(X1,X2)),
inference(cp,[status(thm)],[t58,t36]) ).
cnf(t1266,plain,
addition(X1,multiplication(X1,X2)) = multiplication(X1,addition(one,X2)),
inference(orient,[status(thm)],[t59]) ).
cnf(t2170,plain,
multiplication(domain(X1),addition(one,X1)) = addition(domain(X1),X1),
inference(cp,[status(thm)],[t1266,t2153]) ).
cnf(t377636,plain,
multiplication(domain(X1),addition(one,X1)) = addition(X1,domain(X1)),
inference(step,[status(thm)],[t2170,t103]) ).
cnf(t8351,plain,
multiplication(domain(X1),addition(one,X1)) = addition(X1,domain(X1)),
inference(orient,[status(thm)],[t377636]) ).
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(t182,plain,
domain(multiplication(X1,domain(X2))) = forward_diamond(X1,X2),
inference(orient,[status(thm)],[t21]) ).
cnf(t189,plain,
c(multiplication(X1,domain(X2))) = antidomain(forward_diamond(X1,X2)),
inference(cp,[status(thm)],[t53,t182]) ).
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(t1835,plain,
antidomain(forward_diamond(X1,antidomain(X2))) = c(multiplication(X1,c(X2))),
inference(orient,[status(thm)],[t1024]) ).
cnf(t377371,plain,
c(forward_diamond(X1,antidomain(X2))) = c(multiplication(X1,c(X2))),
inference(step,[status(thm)],[t1835,t4627]) ).
cnf(t377372,plain,
c(forward_diamond(X1,c(X2))) = c(multiplication(X1,c(X2))),
inference(step,[status(thm)],[t377371,t4627]) ).
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(t194,plain,
c(forward_diamond(X1,c(X2))) = forward_box(X1,X2),
inference(orient,[status(thm)],[t19]) ).
cnf(t377373,plain,
forward_box(X1,X2) = c(multiplication(X1,c(X2))),
inference(step,[status(thm)],[t377372,t194]) ).
cnf(t4675,plain,
forward_box(X1,X2) = c(multiplication(X1,c(X2))),
inference(rw,[status(thm)],[t377373]) ).
cnf(t4946,plain,
c(multiplication(X1,c(X2))) = forward_box(X1,X2),
inference(orient,[status(thm)],[t4675]) ).
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(t34,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(t376962,plain,
addition(antidomain(multiplication(X1,X2)),antidomain(multiplication(X1,domain(X2)))) = antidomain(multiplication(X1,antidomain(antidomain(X2)))),
inference(step,[status(thm)],[t34,t44]) ).
cnf(t376963,plain,
addition(antidomain(multiplication(X1,X2)),antidomain(multiplication(X1,domain(X2)))) = antidomain(multiplication(X1,domain(X2))),
inference(step,[status(thm)],[t376962,t44]) ).
cnf(t48,plain,
addition(antidomain(multiplication(X1,X2)),antidomain(multiplication(X1,domain(X2)))) = antidomain(multiplication(X1,domain(X2))),
inference(orient,[status(thm)],[t376963]) ).
cnf(t68,plain,
antidomain(multiplication(X1,domain(coantidomain(X1)))) = addition(antidomain(zero),antidomain(multiplication(X1,domain(coantidomain(X1))))),
inference(cp,[status(thm)],[t48,t62]) ).
cnf(t377230,plain,
antidomain(multiplication(X1,domain(coantidomain(X1)))) = addition(one,antidomain(multiplication(X1,domain(coantidomain(X1))))),
inference(step,[status(thm)],[t68,t221]) ).
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(t41,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(t172,plain,
ifeq(addition(X1,X2),X2,leq(X1,X2),true) = true,
inference(orient,[status(thm)],[t25]) ).
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(t109,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(t38,plain,
addition(X1,X1) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t112,plain,
addition(X1,addition(X1,X2)) = addition(X1,X2),
inference(cp,[status(thm)],[t109,t38]) ).
cnf(t620,plain,
addition(X1,addition(X1,X2)) = addition(X1,X2),
inference(orient,[status(thm)],[t112]) ).
cnf(t628,plain,
true = ifeq(addition(X1,X2),addition(X1,X2),leq(X1,addition(X1,X2)),true),
inference(cp,[status(thm)],[t172,t620]) ).
cnf(t15,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t40,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t15]) ).
cnf(t377060,plain,
true = leq(X1,addition(X1,X2)),
inference(step,[status(thm)],[t628,t40]) ).
cnf(t659,plain,
leq(X1,addition(X1,X2)) = true,
inference(orient,[status(thm)],[t377060]) ).
cnf(t666,plain,
true = leq(X1,addition(X2,X1)),
inference(cp,[status(thm)],[t659,t103]) ).
cnf(t723,plain,
leq(X1,addition(X2,X1)) = true,
inference(orient,[status(thm)],[t666]) ).
cnf(t729,plain,
true = leq(antidomain(X1),one),
inference(cp,[status(thm)],[t723,t119]) ).
cnf(t740,plain,
leq(antidomain(X1),one) = true,
inference(orient,[status(thm)],[t729]) ).
cnf(t744,plain,
one = ifeq(true,true,addition(antidomain(X1),one),one),
inference(cp,[status(thm)],[t41,t740]) ).
cnf(t377063,plain,
one = addition(antidomain(X1),one),
inference(step,[status(thm)],[t744,t40]) ).
cnf(t377064,plain,
one = addition(one,antidomain(X1)),
inference(step,[status(thm)],[t377063,t103]) ).
cnf(t750,plain,
addition(one,antidomain(X1)) = one,
inference(orient,[status(thm)],[t377064]) ).
cnf(t377231,plain,
antidomain(multiplication(X1,domain(coantidomain(X1)))) = one,
inference(step,[status(thm)],[t377230,t750]) ).
cnf(t3559,plain,
antidomain(multiplication(X1,domain(coantidomain(X1)))) = one,
inference(orient,[status(thm)],[t377231]) ).
cnf(t3583,plain,
zero = multiplication(one,multiplication(X1,domain(coantidomain(X1)))),
inference(cp,[status(thm)],[t73,t3559]) ).
cnf(t377234,plain,
zero = multiplication(X1,domain(coantidomain(X1))),
inference(step,[status(thm)],[t3583,t37]) ).
cnf(t3598,plain,
multiplication(X1,domain(coantidomain(X1))) = zero,
inference(orient,[status(thm)],[t377234]) ).
cnf(t3607,plain,
multiplication(X1,addition(domain(coantidomain(X1)),X2)) = addition(zero,multiplication(X1,X2)),
inference(cp,[status(thm)],[t58,t3598]) ).
cnf(t377868,plain,
multiplication(X1,addition(domain(coantidomain(X1)),X2)) = multiplication(X1,X2),
inference(step,[status(thm)],[t3607,t233]) ).
cnf(t14972,plain,
multiplication(X1,addition(domain(coantidomain(X1)),X2)) = multiplication(X1,X2),
inference(orient,[status(thm)],[t377868]) ).
cnf(t255,plain,
one = addition(c(X1),antidomain(antidomain(X1))),
inference(cp,[status(thm)],[t119,t252]) ).
cnf(t377039,plain,
one = addition(c(X1),domain(X1)),
inference(step,[status(thm)],[t255,t44]) ).
cnf(t377040,plain,
one = addition(domain(X1),c(X1)),
inference(step,[status(thm)],[t377039,t103]) ).
cnf(t492,plain,
addition(domain(X1),c(X1)) = one,
inference(orient,[status(thm)],[t377040]) ).
cnf(t14978,plain,
multiplication(X1,c(coantidomain(X1))) = multiplication(X1,one),
inference(cp,[status(thm)],[t14972,t492]) ).
cnf(t377869,plain,
multiplication(X1,c(coantidomain(X1))) = X1,
inference(step,[status(thm)],[t14978,t36]) ).
cnf(t15284,plain,
multiplication(X1,c(coantidomain(X1))) = X1,
inference(orient,[status(thm)],[t377869]) ).
cnf(t15323,plain,
forward_box(X1,coantidomain(X1)) = c(X1),
inference(cp,[status(thm)],[t4946,t15284]) ).
cnf(t15329,plain,
forward_box(X1,coantidomain(X1)) = c(X1),
inference(orient,[status(thm)],[t15323]) ).
cnf(t15332,plain,
c(codomain(X1)) = forward_box(codomain(X1),coantidomain(X1)),
inference(cp,[status(thm)],[t15329,t5495]) ).
cnf(t377870,plain,
backward_box(X1,zero) = forward_box(codomain(X1),coantidomain(X1)),
inference(step,[status(thm)],[t15332,t470]) ).
cnf(t2172,plain,
multiplication(addition(X1,domain(X2)),X2) = addition(multiplication(X1,X2),X2),
inference(cp,[status(thm)],[t82,t2153]) ).
cnf(t377793,plain,
multiplication(addition(X1,domain(X2)),X2) = addition(X2,multiplication(X1,X2)),
inference(step,[status(thm)],[t2172,t103]) ).
cnf(t86,plain,
multiplication(addition(one,X1),X2) = addition(X2,multiplication(X1,X2)),
inference(cp,[status(thm)],[t82,t37]) ).
cnf(t1543,plain,
addition(X1,multiplication(X2,X1)) = multiplication(addition(one,X2),X1),
inference(orient,[status(thm)],[t86]) ).
cnf(t377794,plain,
multiplication(addition(X1,domain(X2)),X2) = multiplication(addition(one,X1),X2),
inference(step,[status(thm)],[t377793,t1543]) ).
cnf(t11842,plain,
multiplication(addition(X1,domain(X2)),X2) = multiplication(addition(one,X1),X2),
inference(orient,[status(thm)],[t377794]) ).
cnf(t11886,plain,
forward_box(addition(X1,domain(c(X2))),X2) = c(multiplication(addition(one,X1),c(X2))),
inference(cp,[status(thm)],[t4946,t11842]) ).
cnf(t232,plain,
forward_box(X1,zero) = c(forward_diamond(X1,one)),
inference(cp,[status(thm)],[t194,t230]) ).
cnf(t215,plain,
forward_diamond(X1,one) = domain(multiplication(X1,one)),
inference(cp,[status(thm)],[t182,t212]) ).
cnf(t376992,plain,
forward_diamond(X1,one) = domain(X1),
inference(step,[status(thm)],[t215,t36]) ).
cnf(t247,plain,
forward_diamond(X1,one) = domain(X1),
inference(orient,[status(thm)],[t376992]) ).
cnf(t377005,plain,
forward_box(X1,zero) = c(domain(X1)),
inference(step,[status(thm)],[t232,t247]) ).
cnf(t254,plain,
c(domain(X1)) = domain(c(X1)),
inference(cp,[status(thm)],[t252,t53]) ).
cnf(t297,plain,
c(domain(X1)) = domain(c(X1)),
inference(orient,[status(thm)],[t254]) ).
cnf(t377006,plain,
forward_box(X1,zero) = domain(c(X1)),
inference(step,[status(thm)],[t377005,t297]) ).
cnf(t331,plain,
domain(c(X1)) = forward_box(X1,zero),
inference(orient,[status(thm)],[t377006]) ).
cnf(t377361,plain,
domain(c(X1)) = c(X1),
inference(step,[status(thm)],[t252,t4627]) ).
cnf(t377362,plain,
forward_box(X1,zero) = c(X1),
inference(step,[status(thm)],[t377361,t331]) ).
cnf(t4669,plain,
forward_box(X1,zero) = c(X1),
inference(rw,[status(thm)],[t377362]) ).
cnf(t4706,plain,
forward_box(X1,zero) = c(X1),
inference(orient,[status(thm)],[t4669]) ).
cnf(t377425,plain,
domain(c(X1)) = c(X1),
inference(step,[status(thm)],[t331,t4706]) ).
cnf(t4709,plain,
domain(c(X1)) = c(X1),
inference(orient,[status(thm)],[t377425]) ).
cnf(t377818,plain,
forward_box(addition(X1,c(X2)),X2) = c(multiplication(addition(one,X1),c(X2))),
inference(step,[status(thm)],[t11886,t4709]) ).
cnf(t377819,plain,
forward_box(addition(X1,c(X2)),X2) = forward_box(addition(one,X1),X2),
inference(step,[status(thm)],[t377818,t4946]) ).
cnf(t13963,plain,
forward_box(addition(X1,c(X2)),X2) = forward_box(addition(one,X1),X2),
inference(orient,[status(thm)],[t377819]) ).
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(t55,plain,
multiplication(multiplication(X1,X2),X3) = multiplication(X1,multiplication(X2,X3)),
inference(orient,[status(thm)],[t27]) ).
cnf(t79,plain,
multiplication(antidomain(X1),multiplication(X1,X2)) = multiplication(zero,X2),
inference(cp,[status(thm)],[t55,t73]) ).
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(t92,plain,
multiplication(zero,X1) = zero,
inference(orient,[status(thm)],[t8]) ).
cnf(t377154,plain,
multiplication(antidomain(X1),multiplication(X1,X2)) = zero,
inference(step,[status(thm)],[t79,t92]) ).
cnf(t2060,plain,
multiplication(antidomain(X1),multiplication(X1,X2)) = zero,
inference(orient,[status(thm)],[t377154]) ).
cnf(t2169,plain,
zero = multiplication(antidomain(domain(X1)),X1),
inference(cp,[status(thm)],[t2060,t2153]) ).
cnf(t377158,plain,
zero = multiplication(c(X1),X1),
inference(step,[status(thm)],[t2169,t53]) ).
cnf(t2192,plain,
multiplication(c(X1),X1) = zero,
inference(orient,[status(thm)],[t377158]) ).
cnf(t2208,plain,
multiplication(c(X1),addition(X1,X2)) = addition(zero,multiplication(c(X1),X2)),
inference(cp,[status(thm)],[t58,t2192]) ).
cnf(t377650,plain,
multiplication(c(X1),addition(X1,X2)) = multiplication(c(X1),X2),
inference(step,[status(thm)],[t2208,t233]) ).
cnf(t8590,plain,
multiplication(c(X1),addition(X1,X2)) = multiplication(c(X1),X2),
inference(orient,[status(thm)],[t377650]) ).
cnf(t8608,plain,
multiplication(c(codomain(X1)),coantidomain(X1)) = multiplication(c(codomain(X1)),one),
inference(cp,[status(thm)],[t8590,t435]) ).
cnf(t377656,plain,
multiplication(backward_box(X1,zero),coantidomain(X1)) = multiplication(c(codomain(X1)),one),
inference(step,[status(thm)],[t8608,t470]) ).
cnf(t377657,plain,
multiplication(backward_box(X1,zero),coantidomain(X1)) = c(codomain(X1)),
inference(step,[status(thm)],[t377656,t36]) ).
cnf(t377658,plain,
multiplication(backward_box(X1,zero),coantidomain(X1)) = backward_box(X1,zero),
inference(step,[status(thm)],[t377657,t470]) ).
cnf(t8664,plain,
multiplication(backward_box(X1,zero),coantidomain(X1)) = backward_box(X1,zero),
inference(orient,[status(thm)],[t377658]) ).
cnf(t8675,plain,
multiplication(addition(one,backward_box(X1,zero)),coantidomain(X1)) = addition(coantidomain(X1),backward_box(X1,zero)),
inference(cp,[status(thm)],[t1543,t8664]) ).
cnf(t623,plain,
addition(domain(X1),antidomain(X1)) = addition(domain(X1),one),
inference(cp,[status(thm)],[t620,t119]) ).
cnf(t377058,plain,
one = addition(domain(X1),one),
inference(step,[status(thm)],[t623,t119]) ).
cnf(t377059,plain,
one = addition(one,domain(X1)),
inference(step,[status(thm)],[t377058,t103]) ).
cnf(t636,plain,
addition(one,domain(X1)) = one,
inference(orient,[status(thm)],[t377059]) ).
cnf(t642,plain,
one = addition(one,c(X1)),
inference(cp,[status(thm)],[t636,t252]) ).
cnf(t647,plain,
addition(one,c(X1)) = one,
inference(orient,[status(thm)],[t642]) ).
cnf(t649,plain,
one = addition(one,backward_box(X1,zero)),
inference(cp,[status(thm)],[t647,t470]) ).
cnf(t711,plain,
addition(one,backward_box(X1,zero)) = one,
inference(orient,[status(thm)],[t649]) ).
cnf(t377659,plain,
multiplication(one,coantidomain(X1)) = addition(coantidomain(X1),backward_box(X1,zero)),
inference(step,[status(thm)],[t8675,t711]) ).
cnf(t377660,plain,
coantidomain(X1) = addition(coantidomain(X1),backward_box(X1,zero)),
inference(step,[status(thm)],[t377659,t37]) ).
cnf(t8688,plain,
addition(coantidomain(X1),backward_box(X1,zero)) = coantidomain(X1),
inference(orient,[status(thm)],[t377660]) ).
cnf(t8691,plain,
coantidomain(coantidomain(X1)) = addition(codomain(X1),backward_box(coantidomain(X1),zero)),
inference(cp,[status(thm)],[t8688,t142]) ).
cnf(t377669,plain,
codomain(X1) = addition(codomain(X1),backward_box(coantidomain(X1),zero)),
inference(step,[status(thm)],[t8691,t142]) ).
cnf(t5504,plain,
backward_box(coantidomain(X1),zero) = c(coantidomain(X1)),
inference(cp,[status(thm)],[t470,t5494]) ).
cnf(t5542,plain,
backward_box(coantidomain(X1),zero) = c(coantidomain(X1)),
inference(orient,[status(thm)],[t5504]) ).
cnf(t377670,plain,
codomain(X1) = addition(codomain(X1),c(coantidomain(X1))),
inference(step,[status(thm)],[t377669,t5542]) ).
cnf(t9151,plain,
addition(codomain(X1),c(coantidomain(X1))) = codomain(X1),
inference(orient,[status(thm)],[t377670]) ).
cnf(t13965,plain,
forward_box(addition(one,codomain(X1)),coantidomain(X1)) = forward_box(codomain(X1),coantidomain(X1)),
inference(cp,[status(thm)],[t13963,t9151]) ).
cnf(t622,plain,
addition(codomain(X1),coantidomain(X1)) = addition(codomain(X1),one),
inference(cp,[status(thm)],[t620,t435]) ).
cnf(t377056,plain,
one = addition(codomain(X1),one),
inference(step,[status(thm)],[t622,t435]) ).
cnf(t377057,plain,
one = addition(one,codomain(X1)),
inference(step,[status(thm)],[t377056,t103]) ).
cnf(t629,plain,
addition(one,codomain(X1)) = one,
inference(orient,[status(thm)],[t377057]) ).
cnf(t377820,plain,
forward_box(one,coantidomain(X1)) = forward_box(codomain(X1),coantidomain(X1)),
inference(step,[status(thm)],[t13965,t629]) ).
cnf(t186,plain,
forward_diamond(one,X1) = domain(domain(X1)),
inference(cp,[status(thm)],[t182,t37]) ).
cnf(t272,plain,
domain(domain(X1)) = forward_diamond(one,X1),
inference(orient,[status(thm)],[t186]) ).
cnf(t280,plain,
c(domain(X1)) = antidomain(forward_diamond(one,X1)),
inference(cp,[status(thm)],[t53,t272]) ).
cnf(t377007,plain,
c(domain(X1)) = forward_box(X1,zero),
inference(step,[status(thm)],[t297,t331]) ).
cnf(t332,plain,
c(domain(X1)) = forward_box(X1,zero),
inference(orient,[status(thm)],[t377007]) ).
cnf(t377012,plain,
forward_box(X1,zero) = antidomain(forward_diamond(one,X1)),
inference(step,[status(thm)],[t280,t332]) ).
cnf(t360,plain,
antidomain(forward_diamond(one,X1)) = forward_box(X1,zero),
inference(orient,[status(thm)],[t377012]) ).
cnf(t54,plain,
domain(domain(X1)) = antidomain(c(X1)),
inference(cp,[status(thm)],[t44,t53]) ).
cnf(t261,plain,
antidomain(c(X1)) = domain(domain(X1)),
inference(orient,[status(thm)],[t54]) ).
cnf(t264,plain,
c(c(X1)) = domain(domain(domain(X1))),
inference(cp,[status(thm)],[t252,t261]) ).
cnf(t377010,plain,
c(c(X1)) = forward_diamond(one,domain(X1)),
inference(step,[status(thm)],[t264,t272]) ).
cnf(t351,plain,
forward_diamond(one,domain(X1)) = c(c(X1)),
inference(orient,[status(thm)],[t377010]) ).
cnf(t352,plain,
c(c(c(X1))) = forward_diamond(one,forward_box(X1,zero)),
inference(cp,[status(thm)],[t351,t331]) ).
cnf(t1130,plain,
forward_diamond(one,forward_box(X1,zero)) = c(c(c(X1))),
inference(orient,[status(thm)],[t352]) ).
cnf(t1135,plain,
forward_box(forward_box(X1,zero),zero) = antidomain(c(c(c(X1)))),
inference(cp,[status(thm)],[t360,t1130]) ).
cnf(t376995,plain,
antidomain(c(X1)) = forward_diamond(one,X1),
inference(step,[status(thm)],[t261,t272]) ).
cnf(t273,plain,
antidomain(c(X1)) = forward_diamond(one,X1),
inference(orient,[status(thm)],[t376995]) ).
cnf(t377081,plain,
forward_box(forward_box(X1,zero),zero) = forward_diamond(one,c(c(X1))),
inference(step,[status(thm)],[t1135,t273]) ).
cnf(t253,plain,
c(antidomain(X1)) = domain(domain(X1)),
inference(cp,[status(thm)],[t252,t44]) ).
cnf(t376997,plain,
c(antidomain(X1)) = forward_diamond(one,X1),
inference(step,[status(thm)],[t253,t272]) ).
cnf(t290,plain,
c(antidomain(X1)) = forward_diamond(one,X1),
inference(orient,[status(thm)],[t376997]) ).
cnf(t291,plain,
forward_diamond(one,c(X1)) = c(forward_diamond(one,X1)),
inference(cp,[status(thm)],[t290,t273]) ).
cnf(t523,plain,
c(forward_diamond(one,X1)) = forward_diamond(one,c(X1)),
inference(orient,[status(thm)],[t291]) ).
cnf(t524,plain,
forward_diamond(one,c(c(X1))) = forward_box(one,X1),
inference(cp,[status(thm)],[t523,t194]) ).
cnf(t776,plain,
forward_diamond(one,c(c(X1))) = forward_box(one,X1),
inference(orient,[status(thm)],[t524]) ).
cnf(t377082,plain,
forward_box(forward_box(X1,zero),zero) = forward_box(one,X1),
inference(step,[status(thm)],[t377081,t776]) ).
cnf(t1136,plain,
forward_box(forward_box(X1,zero),zero) = forward_box(one,X1),
inference(orient,[status(thm)],[t377082]) ).
cnf(t377434,plain,
c(forward_box(X1,zero)) = forward_box(one,X1),
inference(step,[status(thm)],[t1136,t4706]) ).
cnf(t342,plain,
forward_box(c(X1),zero) = c(forward_box(X1,zero)),
inference(cp,[status(thm)],[t332,t331]) ).
cnf(t547,plain,
c(forward_box(X1,zero)) = forward_box(c(X1),zero),
inference(orient,[status(thm)],[t342]) ).
cnf(t377435,plain,
forward_box(c(X1),zero) = forward_box(one,X1),
inference(step,[status(thm)],[t377434,t547]) ).
cnf(t377436,plain,
c(c(X1)) = forward_box(one,X1),
inference(step,[status(thm)],[t377435,t4706]) ).
cnf(t4716,plain,
c(c(X1)) = forward_box(one,X1),
inference(rw,[status(thm)],[t377436]) ).
cnf(t377367,plain,
c(antidomain(X1)) = domain(X1),
inference(step,[status(thm)],[t44,t4627]) ).
cnf(t377368,plain,
c(c(X1)) = domain(X1),
inference(step,[status(thm)],[t377367,t4627]) ).
cnf(t4672,plain,
c(c(X1)) = domain(X1),
inference(rw,[status(thm)],[t377368]) ).
cnf(t4718,plain,
c(c(X1)) = domain(X1),
inference(orient,[status(thm)],[t4672]) ).
cnf(t377446,plain,
domain(X1) = forward_box(one,X1),
inference(step,[status(thm)],[t4716,t4718]) ).
cnf(t4752,plain,
forward_box(one,X1) = domain(X1),
inference(orient,[status(thm)],[t377446]) ).
cnf(t377821,plain,
domain(coantidomain(X1)) = forward_box(codomain(X1),coantidomain(X1)),
inference(step,[status(thm)],[t377820,t4752]) ).
cnf(t13986,plain,
forward_box(codomain(X1),coantidomain(X1)) = domain(coantidomain(X1)),
inference(orient,[status(thm)],[t377821]) ).
cnf(t377871,plain,
backward_box(X1,zero) = domain(coantidomain(X1)),
inference(step,[status(thm)],[t377870,t13986]) ).
cnf(t15336,plain,
domain(coantidomain(X1)) = backward_box(X1,zero),
inference(orient,[status(thm)],[t377871]) ).
cnf(t15358,plain,
addition(coantidomain(X1),domain(coantidomain(X1))) = multiplication(backward_box(X1,zero),addition(one,coantidomain(X1))),
inference(cp,[status(thm)],[t8351,t15336]) ).
cnf(t377890,plain,
addition(coantidomain(X1),backward_box(X1,zero)) = multiplication(backward_box(X1,zero),addition(one,coantidomain(X1))),
inference(step,[status(thm)],[t15358,t15336]) ).
cnf(t377891,plain,
coantidomain(X1) = multiplication(backward_box(X1,zero),addition(one,coantidomain(X1))),
inference(step,[status(thm)],[t377890,t8688]) ).
cnf(t728,plain,
true = leq(coantidomain(X1),one),
inference(cp,[status(thm)],[t723,t435]) ).
cnf(t736,plain,
leq(coantidomain(X1),one) = true,
inference(orient,[status(thm)],[t728]) ).
cnf(t738,plain,
one = ifeq(true,true,addition(coantidomain(X1),one),one),
inference(cp,[status(thm)],[t41,t736]) ).
cnf(t377061,plain,
one = addition(coantidomain(X1),one),
inference(step,[status(thm)],[t738,t40]) ).
cnf(t377062,plain,
one = addition(one,coantidomain(X1)),
inference(step,[status(thm)],[t377061,t103]) ).
cnf(t746,plain,
addition(one,coantidomain(X1)) = one,
inference(orient,[status(thm)],[t377062]) ).
cnf(t377892,plain,
coantidomain(X1) = multiplication(backward_box(X1,zero),one),
inference(step,[status(thm)],[t377891,t746]) ).
cnf(t377893,plain,
coantidomain(X1) = backward_box(X1,zero),
inference(step,[status(thm)],[t377892,t36]) ).
cnf(t15466,plain,
backward_box(X1,zero) = coantidomain(X1),
inference(orient,[status(thm)],[t377893]) ).
cnf(t377928,plain,
coantidomain(backward_diamond(X1,X2)) = c(backward_diamond(X1,X2)),
inference(step,[status(thm)],[t5815,t15466]) ).
cnf(t15502,plain,
coantidomain(backward_diamond(X1,X2)) = c(backward_diamond(X1,X2)),
inference(rw,[status(thm)],[t377928]) ).
cnf(t15943,plain,
c(backward_diamond(X1,X2)) = coantidomain(backward_diamond(X1,X2)),
inference(orient,[status(thm)],[t15502]) ).
cnf(t377997,plain,
coantidomain(backward_diamond(X1,c(X2))) = backward_box(X1,X2),
inference(step,[status(thm)],[t196,t15943]) ).
cnf(t16035,plain,
coantidomain(backward_diamond(X1,c(X2))) = backward_box(X1,X2),
inference(rw,[status(thm)],[t377997]) ).
cnf(t16337,plain,
coantidomain(backward_diamond(X1,c(X2))) = backward_box(X1,X2),
inference(orient,[status(thm)],[t16035]) ).
cnf(t377934,plain,
coantidomain(coantidomain(X1)) = c(coantidomain(X1)),
inference(step,[status(thm)],[t5542,t15466]) ).
cnf(t377935,plain,
codomain(X1) = c(coantidomain(X1)),
inference(step,[status(thm)],[t377934,t142]) ).
cnf(t15506,plain,
codomain(X1) = c(coantidomain(X1)),
inference(rw,[status(thm)],[t377935]) ).
cnf(t15518,plain,
c(coantidomain(X1)) = codomain(X1),
inference(orient,[status(thm)],[t15506]) ).
cnf(t16347,plain,
backward_box(X1,coantidomain(X2)) = coantidomain(backward_diamond(X1,codomain(X2))),
inference(cp,[status(thm)],[t16337,t15518]) ).
cnf(t378013,plain,
backward_box(X1,coantidomain(X2)) = coantidomain(backward_diamond(X1,X2)),
inference(step,[status(thm)],[t16347,t5768]) ).
cnf(t16438,plain,
coantidomain(backward_diamond(X1,X2)) = backward_box(X1,coantidomain(X2)),
inference(orient,[status(thm)],[t378013]) ).
cnf(t378014,plain,
coantidomain(multiplication(codomain(X1),X2)) = backward_box(X2,coantidomain(X1)),
inference(step,[status(thm)],[t5915,t16438]) ).
cnf(t16439,plain,
coantidomain(multiplication(codomain(X1),X2)) = backward_box(X2,coantidomain(X1)),
inference(orient,[status(thm)],[t378014]) ).
cnf(t2013,plain,
backward_diamond(codomain(codomain(X1)),X1) = codomain(codomain(X1)),
inference(cp,[status(thm)],[t200,t1999]) ).
cnf(t377151,plain,
backward_diamond(backward_diamond(one,X1),X1) = codomain(codomain(X1)),
inference(step,[status(thm)],[t2013,t284]) ).
cnf(t377152,plain,
backward_diamond(backward_diamond(one,X1),X1) = backward_diamond(one,X1),
inference(step,[status(thm)],[t377151,t284]) ).
cnf(t2019,plain,
backward_diamond(backward_diamond(one,X1),X1) = backward_diamond(one,X1),
inference(orient,[status(thm)],[t377152]) ).
cnf(t377511,plain,
backward_diamond(codomain(X1),X1) = backward_diamond(one,X1),
inference(step,[status(thm)],[t2019,t5516]) ).
cnf(t377512,plain,
backward_diamond(codomain(X1),X1) = codomain(X1),
inference(step,[status(thm)],[t377511,t5516]) ).
cnf(t5523,plain,
backward_diamond(codomain(X1),X1) = codomain(X1),
inference(rw,[status(thm)],[t377512]) ).
cnf(t5535,plain,
backward_diamond(codomain(X1),X1) = codomain(X1),
inference(orient,[status(thm)],[t5523]) ).
cnf(t5536,plain,
codomain(coantidomain(X1)) = backward_diamond(coantidomain(X1),coantidomain(X1)),
inference(cp,[status(thm)],[t5535,t5494]) ).
cnf(t377527,plain,
coantidomain(X1) = backward_diamond(coantidomain(X1),coantidomain(X1)),
inference(step,[status(thm)],[t5536,t5494]) ).
cnf(t5664,plain,
backward_diamond(coantidomain(X1),coantidomain(X1)) = coantidomain(X1),
inference(orient,[status(thm)],[t377527]) ).
cnf(t4958,plain,
forward_box(X1,codomain(X2)) = c(multiplication(X1,backward_box(X2,zero))),
inference(cp,[status(thm)],[t4946,t470]) ).
cnf(t9832,plain,
c(multiplication(X1,backward_box(X2,zero))) = forward_box(X1,codomain(X2)),
inference(orient,[status(thm)],[t4958]) ).
cnf(t61,plain,
multiplication(X1,X2) = ifeq(leq(multiplication(X1,X3),multiplication(X1,X2)),true,multiplication(X1,addition(X3,X2)),multiplication(X1,X2)),
inference(cp,[status(thm)],[t41,t58]) ).
cnf(t1591,plain,
ifeq(leq(multiplication(X1,X2),multiplication(X1,X3)),true,multiplication(X1,addition(X2,X3)),multiplication(X1,X3)) = multiplication(X1,X3),
inference(orient,[status(thm)],[t61]) ).
cnf(t1593,plain,
multiplication(X1,X2) = ifeq(leq(zero,multiplication(X1,X2)),true,multiplication(X1,addition(coantidomain(X1),X2)),multiplication(X1,X2)),
inference(cp,[status(thm)],[t1591,t62]) ).
cnf(t235,plain,
true = ifeq(X1,X1,leq(zero,X1),true),
inference(cp,[status(thm)],[t172,t233]) ).
cnf(t376988,plain,
true = leq(zero,X1),
inference(step,[status(thm)],[t235,t40]) ).
cnf(t239,plain,
leq(zero,X1) = true,
inference(orient,[status(thm)],[t376988]) ).
cnf(t377191,plain,
multiplication(X1,X2) = ifeq(true,true,multiplication(X1,addition(coantidomain(X1),X2)),multiplication(X1,X2)),
inference(step,[status(thm)],[t1593,t239]) ).
cnf(t377192,plain,
multiplication(X1,X2) = multiplication(X1,addition(coantidomain(X1),X2)),
inference(step,[status(thm)],[t377191,t40]) ).
cnf(t2955,plain,
multiplication(X1,addition(coantidomain(X1),X2)) = multiplication(X1,X2),
inference(orient,[status(thm)],[t377192]) ).
cnf(t8706,plain,
multiplication(X1,backward_box(X1,zero)) = multiplication(X1,coantidomain(X1)),
inference(cp,[status(thm)],[t2955,t8688]) ).
cnf(t377661,plain,
multiplication(X1,backward_box(X1,zero)) = zero,
inference(step,[status(thm)],[t8706,t62]) ).
cnf(t8708,plain,
multiplication(X1,backward_box(X1,zero)) = zero,
inference(orient,[status(thm)],[t377661]) ).
cnf(t9833,plain,
forward_box(X1,codomain(X1)) = c(zero),
inference(cp,[status(thm)],[t9832,t8708]) ).
cnf(t377714,plain,
forward_box(X1,codomain(X1)) = one,
inference(step,[status(thm)],[t9833,t230]) ).
cnf(t9948,plain,
forward_box(X1,codomain(X1)) = one,
inference(orient,[status(thm)],[t377714]) ).
cnf(t9949,plain,
one = forward_box(multiplication(codomain(X1),X2),backward_diamond(X2,X1)),
inference(cp,[status(thm)],[t9948,t200]) ).
cnf(t33178,plain,
forward_box(multiplication(codomain(X1),X2),backward_diamond(X2,X1)) = one,
inference(orient,[status(thm)],[t9949]) ).
cnf(t5521,plain,
backward_box(one,X1) = c(codomain(c(X1))),
inference(cp,[status(thm)],[t196,t5516]) ).
cnf(t377522,plain,
backward_box(one,X1) = backward_box(c(X1),zero),
inference(step,[status(thm)],[t5521,t470]) ).
cnf(t5545,plain,
backward_box(c(X1),zero) = backward_box(one,X1),
inference(orient,[status(thm)],[t377522]) ).
cnf(t5556,plain,
backward_box(one,backward_diamond(X1,c(X2))) = backward_box(backward_box(X1,X2),zero),
inference(cp,[status(thm)],[t5545,t196]) ).
cnf(t13038,plain,
backward_box(one,backward_diamond(X1,c(X2))) = backward_box(backward_box(X1,X2),zero),
inference(orient,[status(thm)],[t5556]) ).
cnf(t377902,plain,
backward_box(one,backward_diamond(X1,c(X2))) = coantidomain(backward_box(X1,X2)),
inference(step,[status(thm)],[t13038,t15466]) ).
cnf(t15475,plain,
backward_box(one,backward_diamond(X1,c(X2))) = coantidomain(backward_box(X1,X2)),
inference(orient,[status(thm)],[t377902]) ).
cnf(t5555,plain,
backward_box(one,codomain(X1)) = backward_box(backward_box(X1,zero),zero),
inference(cp,[status(thm)],[t5545,t470]) ).
cnf(t5773,plain,
backward_box(backward_box(X1,zero),zero) = backward_box(one,codomain(X1)),
inference(orient,[status(thm)],[t5555]) ).
cnf(t377929,plain,
coantidomain(backward_box(X1,zero)) = backward_box(one,codomain(X1)),
inference(step,[status(thm)],[t5773,t15466]) ).
cnf(t377930,plain,
coantidomain(coantidomain(X1)) = backward_box(one,codomain(X1)),
inference(step,[status(thm)],[t377929,t15466]) ).
cnf(t377931,plain,
codomain(X1) = backward_box(one,codomain(X1)),
inference(step,[status(thm)],[t377930,t142]) ).
cnf(t15503,plain,
codomain(X1) = backward_box(one,codomain(X1)),
inference(rw,[status(thm)],[t377931]) ).
cnf(t15746,plain,
backward_box(one,codomain(X1)) = codomain(X1),
inference(orient,[status(thm)],[t15503]) ).
cnf(t15748,plain,
codomain(backward_diamond(X1,X2)) = backward_box(one,backward_diamond(X1,X2)),
inference(cp,[status(thm)],[t15746,t5798]) ).
cnf(t378003,plain,
backward_diamond(X1,X2) = backward_box(one,backward_diamond(X1,X2)),
inference(step,[status(thm)],[t15748,t5798]) ).
cnf(t16235,plain,
backward_box(one,backward_diamond(X1,X2)) = backward_diamond(X1,X2),
inference(orient,[status(thm)],[t378003]) ).
cnf(t378004,plain,
backward_diamond(X1,c(X2)) = coantidomain(backward_box(X1,X2)),
inference(step,[status(thm)],[t15475,t16235]) ).
cnf(t16248,plain,
backward_diamond(X1,c(X2)) = coantidomain(backward_box(X1,X2)),
inference(rw,[status(thm)],[t378004]) ).
cnf(t16249,plain,
coantidomain(backward_box(X1,X2)) = backward_diamond(X1,c(X2)),
inference(orient,[status(thm)],[t16248]) ).
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(t35,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(t124,plain,
addition(coantidomain(multiplication(X1,X2)),coantidomain(multiplication(coantidomain(coantidomain(X1)),X2))) = coantidomain(multiplication(coantidomain(coantidomain(X1)),X2)),
inference(orient,[status(thm)],[t35]) ).
cnf(t376970,plain,
addition(coantidomain(multiplication(X1,X2)),coantidomain(multiplication(codomain(X1),X2))) = coantidomain(multiplication(coantidomain(coantidomain(X1)),X2)),
inference(step,[status(thm)],[t124,t142]) ).
cnf(t376971,plain,
addition(coantidomain(multiplication(X1,X2)),coantidomain(multiplication(codomain(X1),X2))) = coantidomain(multiplication(codomain(X1),X2)),
inference(step,[status(thm)],[t376970,t142]) ).
cnf(t146,plain,
addition(coantidomain(multiplication(X1,X2)),coantidomain(multiplication(codomain(X1),X2))) = coantidomain(multiplication(codomain(X1),X2)),
inference(rw,[status(thm)],[t376971]) ).
cnf(t378095,plain,
addition(coantidomain(multiplication(X1,X2)),backward_box(X2,coantidomain(X1))) = coantidomain(multiplication(codomain(X1),X2)),
inference(step,[status(thm)],[t146,t16439]) ).
cnf(t378096,plain,
addition(backward_box(X2,coantidomain(X1)),coantidomain(multiplication(X1,X2))) = coantidomain(multiplication(codomain(X1),X2)),
inference(step,[status(thm)],[t378095,t103]) ).
cnf(t378097,plain,
addition(backward_box(X2,coantidomain(X1)),coantidomain(multiplication(X1,X2))) = backward_box(X2,coantidomain(X1)),
inference(step,[status(thm)],[t378096,t16439]) ).
cnf(t20961,plain,
addition(backward_box(X1,coantidomain(X2)),coantidomain(multiplication(X2,X1))) = backward_box(X1,coantidomain(X2)),
inference(orient,[status(thm)],[t378097]) ).
cnf(t21022,plain,
backward_box(X1,coantidomain(c(X1))) = addition(backward_box(X1,coantidomain(c(X1))),coantidomain(zero)),
inference(cp,[status(thm)],[t20961,t2192]) ).
cnf(t377933,plain,
coantidomain(c(X1)) = backward_box(one,X1),
inference(step,[status(thm)],[t5545,t15466]) ).
cnf(t15505,plain,
coantidomain(c(X1)) = backward_box(one,X1),
inference(rw,[status(thm)],[t377933]) ).
cnf(t15694,plain,
coantidomain(c(X1)) = backward_box(one,X1),
inference(orient,[status(thm)],[t15505]) ).
cnf(t378098,plain,
backward_box(X1,backward_box(one,X1)) = addition(backward_box(X1,coantidomain(c(X1))),coantidomain(zero)),
inference(step,[status(thm)],[t21022,t15694]) ).
cnf(t4723,plain,
domain(backward_diamond(X1,c(X2))) = c(backward_box(X1,X2)),
inference(cp,[status(thm)],[t4718,t196]) ).
cnf(t5261,plain,
domain(backward_diamond(X1,c(X2))) = c(backward_box(X1,X2)),
inference(orient,[status(thm)],[t4723]) ).
cnf(t258,plain,
forward_diamond(X1,antidomain(X2)) = domain(multiplication(X1,c(X2))),
inference(cp,[status(thm)],[t182,t252]) ).
cnf(t1098,plain,
domain(multiplication(X1,c(X2))) = forward_diamond(X1,antidomain(X2)),
inference(orient,[status(thm)],[t258]) ).
cnf(t377318,plain,
domain(multiplication(X1,c(X2))) = forward_diamond(X1,c(X2)),
inference(step,[status(thm)],[t1098,t4627]) ).
cnf(t4634,plain,
domain(multiplication(X1,c(X2))) = forward_diamond(X1,c(X2)),
inference(orient,[status(thm)],[t377318]) ).
cnf(t2164,plain,
c(X1) = multiplication(forward_box(X1,zero),c(X1)),
inference(cp,[status(thm)],[t2153,t331]) ).
cnf(t2653,plain,
multiplication(forward_box(X1,zero),c(X1)) = c(X1),
inference(orient,[status(thm)],[t2164]) ).
cnf(t377433,plain,
multiplication(c(X1),c(X1)) = c(X1),
inference(step,[status(thm)],[t2653,t4706]) ).
cnf(t4715,plain,
multiplication(c(X1),c(X1)) = c(X1),
inference(rw,[status(thm)],[t377433]) ).
cnf(t4895,plain,
multiplication(c(X1),c(X1)) = c(X1),
inference(orient,[status(thm)],[t4715]) ).
cnf(t4913,plain,
forward_diamond(c(X1),c(X1)) = domain(c(X1)),
inference(cp,[status(thm)],[t4634,t4895]) ).
cnf(t377471,plain,
forward_diamond(c(X1),c(X1)) = c(X1),
inference(step,[status(thm)],[t4913,t4709]) ).
cnf(t4937,plain,
forward_diamond(c(X1),c(X1)) = c(X1),
inference(orient,[status(thm)],[t377471]) ).
cnf(t15545,plain,
c(coantidomain(X1)) = forward_diamond(codomain(X1),c(coantidomain(X1))),
inference(cp,[status(thm)],[t4937,t15518]) ).
cnf(t377955,plain,
codomain(X1) = forward_diamond(codomain(X1),c(coantidomain(X1))),
inference(step,[status(thm)],[t15545,t15518]) ).
cnf(t377956,plain,
codomain(X1) = forward_diamond(codomain(X1),codomain(X1)),
inference(step,[status(thm)],[t377955,t15518]) ).
cnf(t2007,plain,
multiplication(X1,addition(codomain(X1),X2)) = addition(X1,multiplication(X1,X2)),
inference(cp,[status(thm)],[t58,t1999]) ).
cnf(t377734,plain,
multiplication(X1,addition(codomain(X1),X2)) = multiplication(X1,addition(one,X2)),
inference(step,[status(thm)],[t2007,t1266]) ).
cnf(t10568,plain,
multiplication(X1,addition(codomain(X1),X2)) = multiplication(X1,addition(one,X2)),
inference(orient,[status(thm)],[t377734]) ).
cnf(t8372,plain,
addition(codomain(X1),domain(codomain(X1))) = multiplication(domain(codomain(X1)),one),
inference(cp,[status(thm)],[t8351,t629]) ).
cnf(t377644,plain,
addition(codomain(X1),domain(codomain(X1))) = domain(codomain(X1)),
inference(step,[status(thm)],[t8372,t36]) ).
cnf(t8448,plain,
addition(codomain(X1),domain(codomain(X1))) = domain(codomain(X1)),
inference(orient,[status(thm)],[t377644]) ).
cnf(t10570,plain,
multiplication(X1,addition(one,domain(codomain(X1)))) = multiplication(X1,domain(codomain(X1))),
inference(cp,[status(thm)],[t10568,t8448]) ).
cnf(t377735,plain,
multiplication(X1,one) = multiplication(X1,domain(codomain(X1))),
inference(step,[status(thm)],[t10570,t636]) ).
cnf(t377736,plain,
X1 = multiplication(X1,domain(codomain(X1))),
inference(step,[status(thm)],[t377735,t36]) ).
cnf(t10604,plain,
multiplication(X1,domain(codomain(X1))) = X1,
inference(orient,[status(thm)],[t377736]) ).
cnf(t10634,plain,
forward_diamond(X1,codomain(X1)) = domain(X1),
inference(cp,[status(thm)],[t182,t10604]) ).
cnf(t10636,plain,
forward_diamond(X1,codomain(X1)) = domain(X1),
inference(orient,[status(thm)],[t10634]) ).
cnf(t10641,plain,
domain(codomain(X1)) = forward_diamond(codomain(X1),codomain(X1)),
inference(cp,[status(thm)],[t10636,t5517]) ).
cnf(t10665,plain,
forward_diamond(codomain(X1),codomain(X1)) = domain(codomain(X1)),
inference(orient,[status(thm)],[t10641]) ).
cnf(t377957,plain,
codomain(X1) = domain(codomain(X1)),
inference(step,[status(thm)],[t377956,t10665]) ).
cnf(t15633,plain,
domain(codomain(X1)) = codomain(X1),
inference(orient,[status(thm)],[t377957]) ).
cnf(t15645,plain,
codomain(backward_diamond(X1,X2)) = domain(backward_diamond(X1,X2)),
inference(cp,[status(thm)],[t15633,t5798]) ).
cnf(t377988,plain,
backward_diamond(X1,X2) = domain(backward_diamond(X1,X2)),
inference(step,[status(thm)],[t15645,t5798]) ).
cnf(t15800,plain,
domain(backward_diamond(X1,X2)) = backward_diamond(X1,X2),
inference(orient,[status(thm)],[t377988]) ).
cnf(t377991,plain,
backward_diamond(X1,c(X2)) = c(backward_box(X1,X2)),
inference(step,[status(thm)],[t5261,t15800]) ).
cnf(t15871,plain,
backward_diamond(X1,c(X2)) = c(backward_box(X1,X2)),
inference(rw,[status(thm)],[t377991]) ).
cnf(t16036,plain,
c(backward_box(X1,X2)) = backward_diamond(X1,c(X2)),
inference(orient,[status(thm)],[t15871]) ).
cnf(t16075,plain,
domain(backward_box(X1,X2)) = c(backward_diamond(X1,c(X2))),
inference(cp,[status(thm)],[t4718,t16036]) ).
cnf(t2143,plain,
forward_diamond(addition(X1,antidomain(domain(X2))),X2) = domain(multiplication(X1,domain(X2))),
inference(cp,[status(thm)],[t182,t2114]) ).
cnf(t377207,plain,
forward_diamond(addition(X1,c(X2)),X2) = domain(multiplication(X1,domain(X2))),
inference(step,[status(thm)],[t2143,t53]) ).
cnf(t377208,plain,
forward_diamond(addition(X1,c(X2)),X2) = forward_diamond(X1,X2),
inference(step,[status(thm)],[t377207,t182]) ).
cnf(t3190,plain,
forward_diamond(addition(X1,c(X2)),X2) = forward_diamond(X1,X2),
inference(orient,[status(thm)],[t377208]) ).
cnf(t3191,plain,
forward_diamond(domain(X1),X1) = forward_diamond(one,X1),
inference(cp,[status(thm)],[t3190,t492]) ).
cnf(t3207,plain,
forward_diamond(domain(X1),X1) = forward_diamond(one,X1),
inference(orient,[status(thm)],[t3191]) ).
cnf(t3222,plain,
forward_box(domain(c(X1)),X1) = c(forward_diamond(one,c(X1))),
inference(cp,[status(thm)],[t194,t3207]) ).
cnf(t377211,plain,
forward_box(forward_box(X1,zero),X1) = c(forward_diamond(one,c(X1))),
inference(step,[status(thm)],[t3222,t331]) ).
cnf(t377212,plain,
forward_box(forward_box(X1,zero),X1) = forward_diamond(one,c(c(X1))),
inference(step,[status(thm)],[t377211,t523]) ).
cnf(t377213,plain,
forward_box(forward_box(X1,zero),X1) = forward_box(one,X1),
inference(step,[status(thm)],[t377212,t776]) ).
cnf(t3301,plain,
forward_box(forward_box(X1,zero),X1) = forward_box(one,X1),
inference(orient,[status(thm)],[t377213]) ).
cnf(t377432,plain,
forward_box(c(X1),X1) = forward_box(one,X1),
inference(step,[status(thm)],[t3301,t4706]) ).
cnf(t4714,plain,
forward_box(c(X1),X1) = forward_box(one,X1),
inference(rw,[status(thm)],[t377432]) ).
cnf(t377461,plain,
forward_box(c(X1),X1) = domain(X1),
inference(step,[status(thm)],[t4714,t4752]) ).
cnf(t4801,plain,
forward_box(c(X1),X1) = domain(X1),
inference(orient,[status(thm)],[t377461]) ).
cnf(t4802,plain,
domain(c(X1)) = forward_box(domain(X1),c(X1)),
inference(cp,[status(thm)],[t4801,t4718]) ).
cnf(t377469,plain,
c(X1) = forward_box(domain(X1),c(X1)),
inference(step,[status(thm)],[t4802,t4709]) ).
cnf(t4915,plain,
forward_box(domain(X1),c(X1)) = c(X1),
inference(orient,[status(thm)],[t377469]) ).
cnf(t5281,plain,
c(backward_diamond(X1,c(X2))) = forward_box(c(backward_box(X1,X2)),c(backward_diamond(X1,c(X2)))),
inference(cp,[status(thm)],[t4915,t5261]) ).
cnf(t377487,plain,
backward_box(X1,X2) = forward_box(c(backward_box(X1,X2)),c(backward_diamond(X1,c(X2)))),
inference(step,[status(thm)],[t5281,t196]) ).
cnf(t377488,plain,
backward_box(X1,X2) = forward_box(c(backward_box(X1,X2)),backward_box(X1,X2)),
inference(step,[status(thm)],[t377487,t196]) ).
cnf(t377489,plain,
backward_box(X1,X2) = domain(backward_box(X1,X2)),
inference(step,[status(thm)],[t377488,t4801]) ).
cnf(t5296,plain,
domain(backward_box(X1,X2)) = backward_box(X1,X2),
inference(orient,[status(thm)],[t377489]) ).
cnf(t378025,plain,
backward_box(X1,X2) = c(backward_diamond(X1,c(X2))),
inference(step,[status(thm)],[t16075,t5296]) ).
cnf(t378016,plain,
c(backward_diamond(X1,X2)) = backward_box(X1,coantidomain(X2)),
inference(step,[status(thm)],[t15943,t16438]) ).
cnf(t16441,plain,
c(backward_diamond(X1,X2)) = backward_box(X1,coantidomain(X2)),
inference(orient,[status(thm)],[t378016]) ).
cnf(t378026,plain,
backward_box(X1,X2) = backward_box(X1,coantidomain(c(X2))),
inference(step,[status(thm)],[t378025,t16441]) ).
cnf(t378027,plain,
backward_box(X1,X2) = backward_box(X1,backward_box(one,X2)),
inference(step,[status(thm)],[t378026,t15694]) ).
cnf(t16539,plain,
backward_box(X1,backward_box(one,X2)) = backward_box(X1,X2),
inference(orient,[status(thm)],[t378027]) ).
cnf(t378099,plain,
backward_box(X1,X1) = addition(backward_box(X1,coantidomain(c(X1))),coantidomain(zero)),
inference(step,[status(thm)],[t378098,t16539]) ).
cnf(t378100,plain,
backward_box(X1,X1) = addition(coantidomain(zero),backward_box(X1,coantidomain(c(X1)))),
inference(step,[status(thm)],[t378099,t103]) ).
cnf(t207,plain,
codomain(one) = coantidomain(zero),
inference(cp,[status(thm)],[t142,t206]) ).
cnf(t219,plain,
coantidomain(zero) = codomain(one),
inference(orient,[status(thm)],[t207]) ).
cnf(t377018,plain,
coantidomain(zero) = one,
inference(step,[status(thm)],[t219,t445]) ).
cnf(t446,plain,
coantidomain(zero) = one,
inference(orient,[status(thm)],[t377018]) ).
cnf(t378101,plain,
backward_box(X1,X1) = addition(one,backward_box(X1,coantidomain(c(X1)))),
inference(step,[status(thm)],[t378100,t446]) ).
cnf(t654,plain,
one = addition(one,backward_box(X1,X2)),
inference(cp,[status(thm)],[t647,t196]) ).
cnf(t719,plain,
addition(one,backward_box(X1,X2)) = one,
inference(orient,[status(thm)],[t654]) ).
cnf(t378102,plain,
backward_box(X1,X1) = one,
inference(step,[status(thm)],[t378101,t719]) ).
cnf(t21068,plain,
backward_box(X1,X1) = one,
inference(orient,[status(thm)],[t378102]) ).
cnf(t21071,plain,
backward_diamond(X1,c(X1)) = coantidomain(one),
inference(cp,[status(thm)],[t16249,t21068]) ).
cnf(t378103,plain,
backward_diamond(X1,c(X1)) = zero,
inference(step,[status(thm)],[t21071,t206]) ).
cnf(t21088,plain,
backward_diamond(X1,c(X1)) = zero,
inference(orient,[status(thm)],[t378103]) ).
cnf(t33193,plain,
one = forward_box(multiplication(codomain(c(X1)),X1),zero),
inference(cp,[status(thm)],[t33178,t21088]) ).
cnf(t378376,plain,
one = c(multiplication(codomain(c(X1)),X1)),
inference(step,[status(thm)],[t33193,t4706]) ).
cnf(t33284,plain,
c(multiplication(codomain(c(X1)),X1)) = one,
inference(orient,[status(thm)],[t378376]) ).
cnf(t33327,plain,
zero = multiplication(one,multiplication(codomain(c(X1)),X1)),
inference(cp,[status(thm)],[t2192,t33284]) ).
cnf(t378382,plain,
zero = multiplication(codomain(c(X1)),X1),
inference(step,[status(thm)],[t33327,t37]) ).
cnf(t33445,plain,
multiplication(codomain(c(X1)),X1) = zero,
inference(orient,[status(thm)],[t378382]) ).
cnf(t33456,plain,
multiplication(addition(codomain(c(X1)),X2),X1) = addition(zero,multiplication(X2,X1)),
inference(cp,[status(thm)],[t82,t33445]) ).
cnf(t378416,plain,
multiplication(addition(codomain(c(X1)),X2),X1) = multiplication(X2,X1),
inference(step,[status(thm)],[t33456,t233]) ).
cnf(t34244,plain,
multiplication(addition(codomain(c(X1)),X2),X1) = multiplication(X2,X1),
inference(orient,[status(thm)],[t378416]) ).
cnf(t34249,plain,
multiplication(coantidomain(c(X1)),X1) = multiplication(one,X1),
inference(cp,[status(thm)],[t34244,t435]) ).
cnf(t378417,plain,
multiplication(backward_box(one,X1),X1) = multiplication(one,X1),
inference(step,[status(thm)],[t34249,t15694]) ).
cnf(t378418,plain,
multiplication(backward_box(one,X1),X1) = X1,
inference(step,[status(thm)],[t378417,t37]) ).
cnf(t34336,plain,
multiplication(backward_box(one,X1),X1) = X1,
inference(orient,[status(thm)],[t378418]) ).
cnf(t377349,plain,
multiplication(c(X1),c(X2)) = domain_difference(antidomain(X1),X2),
inference(step,[status(thm)],[t1041,t4627]) ).
cnf(t377350,plain,
multiplication(c(X1),c(X2)) = domain_difference(c(X1),X2),
inference(step,[status(thm)],[t377349,t4627]) ).
cnf(t4660,plain,
multiplication(c(X1),c(X2)) = domain_difference(c(X1),X2),
inference(rw,[status(thm)],[t377350]) ).
cnf(t5218,plain,
multiplication(c(X1),c(X2)) = domain_difference(c(X1),X2),
inference(orient,[status(thm)],[t4660]) ).
cnf(t5227,plain,
domain_difference(c(backward_diamond(X1,c(X2))),X3) = multiplication(backward_box(X1,X2),c(X3)),
inference(cp,[status(thm)],[t5218,t196]) ).
cnf(t377806,plain,
domain_difference(backward_box(X1,X2),X3) = multiplication(backward_box(X1,X2),c(X3)),
inference(step,[status(thm)],[t5227,t196]) ).
cnf(t12390,plain,
multiplication(backward_box(X1,X2),c(X3)) = domain_difference(backward_box(X1,X2),X3),
inference(orient,[status(thm)],[t377806]) ).
cnf(t34337,plain,
c(X1) = domain_difference(backward_box(one,c(X1)),X1),
inference(cp,[status(thm)],[t34336,t12390]) ).
cnf(t4745,plain,
backward_box(X1,c(X2)) = c(backward_diamond(X1,domain(X2))),
inference(cp,[status(thm)],[t196,t4718]) ).
cnf(t5333,plain,
c(backward_diamond(X1,domain(X2))) = backward_box(X1,c(X2)),
inference(orient,[status(thm)],[t4745]) ).
cnf(t5519,plain,
backward_box(one,c(X1)) = c(codomain(domain(X1))),
inference(cp,[status(thm)],[t5333,t5516]) ).
cnf(t377526,plain,
backward_box(one,c(X1)) = backward_box(domain(X1),zero),
inference(step,[status(thm)],[t5519,t470]) ).
cnf(t5605,plain,
backward_box(domain(X1),zero) = backward_box(one,c(X1)),
inference(orient,[status(thm)],[t377526]) ).
cnf(t377932,plain,
coantidomain(domain(X1)) = backward_box(one,c(X1)),
inference(step,[status(thm)],[t5605,t15466]) ).
cnf(t15504,plain,
coantidomain(domain(X1)) = backward_box(one,c(X1)),
inference(rw,[status(thm)],[t377932]) ).
cnf(t15771,plain,
backward_box(one,c(X1)) = coantidomain(domain(X1)),
inference(orient,[status(thm)],[t15504]) ).
cnf(t378419,plain,
c(X1) = domain_difference(coantidomain(domain(X1)),X1),
inference(step,[status(thm)],[t34337,t15771]) ).
cnf(t2209,plain,
multiplication(c(X1),addition(X2,X1)) = addition(multiplication(c(X1),X2),zero),
inference(cp,[status(thm)],[t58,t2192]) ).
cnf(t377692,plain,
multiplication(c(X1),addition(X2,X1)) = multiplication(c(X1),X2),
inference(step,[status(thm)],[t2209,t39]) ).
cnf(t9502,plain,
multiplication(c(X1),addition(X2,X1)) = multiplication(c(X1),X2),
inference(orient,[status(thm)],[t377692]) ).
cnf(t505,plain,
addition(domain(X1),addition(c(X1),X2)) = addition(one,X2),
inference(cp,[status(thm)],[t109,t492]) ).
cnf(t14123,plain,
addition(domain(X1),addition(c(X1),X2)) = addition(one,X2),
inference(orient,[status(thm)],[t505]) ).
cnf(t2004,plain,
multiplication(addition(one,X1),codomain(X1)) = addition(codomain(X1),X1),
inference(cp,[status(thm)],[t1543,t1999]) ).
cnf(t377632,plain,
multiplication(addition(one,X1),codomain(X1)) = addition(X1,codomain(X1)),
inference(step,[status(thm)],[t2004,t103]) ).
cnf(t8216,plain,
multiplication(addition(one,X1),codomain(X1)) = addition(X1,codomain(X1)),
inference(orient,[status(thm)],[t377632]) ).
cnf(t8230,plain,
addition(c(X1),codomain(c(X1))) = multiplication(one,codomain(c(X1))),
inference(cp,[status(thm)],[t8216,t647]) ).
cnf(t377633,plain,
addition(c(X1),codomain(c(X1))) = codomain(c(X1)),
inference(step,[status(thm)],[t8230,t37]) ).
cnf(t8252,plain,
addition(c(X1),codomain(c(X1))) = codomain(c(X1)),
inference(orient,[status(thm)],[t377633]) ).
cnf(t14139,plain,
addition(one,codomain(c(X1))) = addition(domain(X1),codomain(c(X1))),
inference(cp,[status(thm)],[t14123,t8252]) ).
cnf(t377832,plain,
one = addition(domain(X1),codomain(c(X1))),
inference(step,[status(thm)],[t14139,t629]) ).
cnf(t14179,plain,
addition(domain(X1),codomain(c(X1))) = one,
inference(orient,[status(thm)],[t377832]) ).
cnf(t14191,plain,
one = addition(c(X1),codomain(c(c(X1)))),
inference(cp,[status(thm)],[t14179,t4709]) ).
cnf(t377833,plain,
one = addition(c(X1),codomain(domain(X1))),
inference(step,[status(thm)],[t14191,t4718]) ).
cnf(t14224,plain,
addition(c(X1),codomain(domain(X1))) = one,
inference(orient,[status(thm)],[t377833]) ).
cnf(t14255,plain,
multiplication(c(codomain(domain(X1))),c(X1)) = multiplication(c(codomain(domain(X1))),one),
inference(cp,[status(thm)],[t9502,t14224]) ).
cnf(t377843,plain,
domain_difference(c(codomain(domain(X1))),X1) = multiplication(c(codomain(domain(X1))),one),
inference(step,[status(thm)],[t14255,t5218]) ).
cnf(t377844,plain,
domain_difference(backward_box(domain(X1),zero),X1) = multiplication(c(codomain(domain(X1))),one),
inference(step,[status(thm)],[t377843,t470]) ).
cnf(t377845,plain,
domain_difference(backward_box(one,c(X1)),X1) = multiplication(c(codomain(domain(X1))),one),
inference(step,[status(thm)],[t377844,t5605]) ).
cnf(t377846,plain,
domain_difference(backward_box(one,c(X1)),X1) = c(codomain(domain(X1))),
inference(step,[status(thm)],[t377845,t36]) ).
cnf(t377847,plain,
domain_difference(backward_box(one,c(X1)),X1) = backward_box(domain(X1),zero),
inference(step,[status(thm)],[t377846,t470]) ).
cnf(t377848,plain,
domain_difference(backward_box(one,c(X1)),X1) = backward_box(one,c(X1)),
inference(step,[status(thm)],[t377847,t5605]) ).
cnf(t14450,plain,
domain_difference(backward_box(one,c(X1)),X1) = backward_box(one,c(X1)),
inference(orient,[status(thm)],[t377848]) ).
cnf(t14463,plain,
backward_box(one,c(c(X1))) = domain_difference(backward_box(one,domain(X1)),c(X1)),
inference(cp,[status(thm)],[t14450,t4718]) ).
cnf(t377849,plain,
backward_box(one,domain(X1)) = domain_difference(backward_box(one,domain(X1)),c(X1)),
inference(step,[status(thm)],[t14463,t4718]) ).
cnf(t472,plain,
backward_box(codomain(X1),zero) = c(backward_diamond(one,X1)),
inference(cp,[status(thm)],[t470,t284]) ).
cnf(t568,plain,
c(backward_diamond(one,X1)) = backward_box(codomain(X1),zero),
inference(orient,[status(thm)],[t472]) ).
cnf(t569,plain,
backward_box(codomain(c(X1)),zero) = backward_box(one,X1),
inference(cp,[status(thm)],[t568,t196]) ).
cnf(t801,plain,
backward_box(codomain(c(X1)),zero) = backward_box(one,X1),
inference(orient,[status(thm)],[t569]) ).
cnf(t4744,plain,
backward_box(one,c(X1)) = backward_box(codomain(domain(X1)),zero),
inference(cp,[status(thm)],[t801,t4718]) ).
cnf(t5314,plain,
backward_box(codomain(domain(X1)),zero) = backward_box(one,c(X1)),
inference(orient,[status(thm)],[t4744]) ).
cnf(t5319,plain,
backward_box(one,c(c(X1))) = backward_box(codomain(c(X1)),zero),
inference(cp,[status(thm)],[t5314,t4709]) ).
cnf(t377490,plain,
backward_box(one,domain(X1)) = backward_box(codomain(c(X1)),zero),
inference(step,[status(thm)],[t5319,t4718]) ).
cnf(t377491,plain,
backward_box(one,domain(X1)) = backward_box(one,X1),
inference(step,[status(thm)],[t377490,t801]) ).
cnf(t5326,plain,
backward_box(one,domain(X1)) = backward_box(one,X1),
inference(orient,[status(thm)],[t377491]) ).
cnf(t377850,plain,
backward_box(one,X1) = domain_difference(backward_box(one,domain(X1)),c(X1)),
inference(step,[status(thm)],[t377849,t5326]) ).
cnf(t377851,plain,
backward_box(one,X1) = domain_difference(backward_box(one,X1),c(X1)),
inference(step,[status(thm)],[t377850,t5326]) ).
cnf(t14477,plain,
domain_difference(backward_box(one,X1),c(X1)) = backward_box(one,X1),
inference(orient,[status(thm)],[t377851]) ).
cnf(t15784,plain,
backward_box(one,c(X1)) = domain_difference(coantidomain(domain(X1)),c(c(X1))),
inference(cp,[status(thm)],[t14477,t15771]) ).
cnf(t378009,plain,
coantidomain(domain(X1)) = domain_difference(coantidomain(domain(X1)),c(c(X1))),
inference(step,[status(thm)],[t15784,t15771]) ).
cnf(t378010,plain,
coantidomain(domain(X1)) = domain_difference(coantidomain(domain(X1)),domain(X1)),
inference(step,[status(thm)],[t378009,t4718]) ).
cnf(t377363,plain,
multiplication(domain(X1),c(X2)) = domain_difference(X1,X2),
inference(step,[status(thm)],[t94,t4627]) ).
cnf(t96,plain,
domain_difference(X1,domain(X2)) = multiplication(domain(X1),c(X2)),
inference(cp,[status(thm)],[t94,t53]) ).
cnf(t991,plain,
multiplication(domain(X1),c(X2)) = domain_difference(X1,domain(X2)),
inference(orient,[status(thm)],[t96]) ).
cnf(t377364,plain,
domain_difference(X1,domain(X2)) = domain_difference(X1,X2),
inference(step,[status(thm)],[t377363,t991]) ).
cnf(t4670,plain,
domain_difference(X1,domain(X2)) = domain_difference(X1,X2),
inference(rw,[status(thm)],[t377364]) ).
cnf(t4790,plain,
domain_difference(X1,domain(X2)) = domain_difference(X1,X2),
inference(orient,[status(thm)],[t4670]) ).
cnf(t378011,plain,
coantidomain(domain(X1)) = domain_difference(coantidomain(domain(X1)),X1),
inference(step,[status(thm)],[t378010,t4790]) ).
cnf(t16321,plain,
domain_difference(coantidomain(domain(X1)),X1) = coantidomain(domain(X1)),
inference(orient,[status(thm)],[t378011]) ).
cnf(t378420,plain,
c(X1) = coantidomain(domain(X1)),
inference(step,[status(thm)],[t378419,t16321]) ).
cnf(t34403,plain,
coantidomain(domain(X1)) = c(X1),
inference(orient,[status(thm)],[t378420]) ).
cnf(t34439,plain,
coantidomain(domain(X1)) = backward_diamond(c(X1),coantidomain(domain(X1))),
inference(cp,[status(thm)],[t5664,t34403]) ).
cnf(t378529,plain,
c(X1) = backward_diamond(c(X1),coantidomain(domain(X1))),
inference(step,[status(thm)],[t34439,t34403]) ).
cnf(t378530,plain,
c(X1) = backward_diamond(c(X1),c(X1)),
inference(step,[status(thm)],[t378529,t34403]) ).
cnf(t2171,plain,
multiplication(addition(domain(X1),X2),X1) = addition(X1,multiplication(X2,X1)),
inference(cp,[status(thm)],[t82,t2153]) ).
cnf(t377756,plain,
multiplication(addition(domain(X1),X2),X1) = multiplication(addition(one,X2),X1),
inference(step,[status(thm)],[t2171,t1543]) ).
cnf(t10908,plain,
multiplication(addition(domain(X1),X2),X1) = multiplication(addition(one,X2),X1),
inference(orient,[status(thm)],[t377756]) ).
cnf(t8231,plain,
addition(domain(X1),codomain(domain(X1))) = multiplication(one,codomain(domain(X1))),
inference(cp,[status(thm)],[t8216,t636]) ).
cnf(t377635,plain,
addition(domain(X1),codomain(domain(X1))) = codomain(domain(X1)),
inference(step,[status(thm)],[t8231,t37]) ).
cnf(t8331,plain,
addition(domain(X1),codomain(domain(X1))) = codomain(domain(X1)),
inference(orient,[status(thm)],[t377635]) ).
cnf(t10909,plain,
multiplication(addition(one,codomain(domain(X1))),X1) = multiplication(codomain(domain(X1)),X1),
inference(cp,[status(thm)],[t10908,t8331]) ).
cnf(t377757,plain,
multiplication(one,X1) = multiplication(codomain(domain(X1)),X1),
inference(step,[status(thm)],[t10909,t629]) ).
cnf(t377758,plain,
X1 = multiplication(codomain(domain(X1)),X1),
inference(step,[status(thm)],[t377757,t37]) ).
cnf(t10955,plain,
multiplication(codomain(domain(X1)),X1) = X1,
inference(orient,[status(thm)],[t377758]) ).
cnf(t10998,plain,
backward_diamond(X1,domain(X1)) = codomain(X1),
inference(cp,[status(thm)],[t200,t10955]) ).
cnf(t11000,plain,
backward_diamond(X1,domain(X1)) = codomain(X1),
inference(orient,[status(thm)],[t10998]) ).
cnf(t11008,plain,
codomain(c(X1)) = backward_diamond(c(X1),c(X1)),
inference(cp,[status(thm)],[t11000,t4709]) ).
cnf(t11074,plain,
backward_diamond(c(X1),c(X1)) = codomain(c(X1)),
inference(orient,[status(thm)],[t11008]) ).
cnf(t378531,plain,
c(X1) = codomain(c(X1)),
inference(step,[status(thm)],[t378530,t11074]) ).
cnf(t34608,plain,
codomain(c(X1)) = c(X1),
inference(orient,[status(thm)],[t378531]) ).
cnf(t34642,plain,
backward_box(X1,coantidomain(c(X2))) = coantidomain(multiplication(c(X2),X1)),
inference(cp,[status(thm)],[t16439,t34608]) ).
cnf(t5343,plain,
backward_box(X1,c(c(X2))) = c(backward_diamond(X1,c(X2))),
inference(cp,[status(thm)],[t5333,t4709]) ).
cnf(t377492,plain,
backward_box(X1,domain(X2)) = c(backward_diamond(X1,c(X2))),
inference(step,[status(thm)],[t5343,t4718]) ).
cnf(t377493,plain,
backward_box(X1,domain(X2)) = backward_box(X1,X2),
inference(step,[status(thm)],[t377492,t196]) ).
cnf(t5383,plain,
backward_box(X1,domain(X2)) = backward_box(X1,X2),
inference(orient,[status(thm)],[t377493]) ).
cnf(t34353,plain,
domain(X1) = multiplication(backward_box(one,X1),domain(X1)),
inference(cp,[status(thm)],[t34336,t5383]) ).
cnf(t14212,plain,
multiplication(c(codomain(c(X1))),domain(X1)) = multiplication(c(codomain(c(X1))),one),
inference(cp,[status(thm)],[t9502,t14179]) ).
cnf(t377834,plain,
multiplication(backward_box(c(X1),zero),domain(X1)) = multiplication(c(codomain(c(X1))),one),
inference(step,[status(thm)],[t14212,t470]) ).
cnf(t377835,plain,
multiplication(backward_box(one,X1),domain(X1)) = multiplication(c(codomain(c(X1))),one),
inference(step,[status(thm)],[t377834,t5545]) ).
cnf(t377836,plain,
multiplication(backward_box(one,X1),domain(X1)) = c(codomain(c(X1))),
inference(step,[status(thm)],[t377835,t36]) ).
cnf(t377837,plain,
multiplication(backward_box(one,X1),domain(X1)) = backward_box(c(X1),zero),
inference(step,[status(thm)],[t377836,t470]) ).
cnf(t377838,plain,
multiplication(backward_box(one,X1),domain(X1)) = backward_box(one,X1),
inference(step,[status(thm)],[t377837,t5545]) ).
cnf(t14268,plain,
multiplication(backward_box(one,X1),domain(X1)) = backward_box(one,X1),
inference(orient,[status(thm)],[t377838]) ).
cnf(t378453,plain,
domain(X1) = backward_box(one,X1),
inference(step,[status(thm)],[t34353,t14268]) ).
cnf(t34513,plain,
backward_box(one,X1) = domain(X1),
inference(orient,[status(thm)],[t378453]) ).
cnf(t378458,plain,
coantidomain(c(X1)) = domain(X1),
inference(step,[status(thm)],[t15694,t34513]) ).
cnf(t34518,plain,
coantidomain(c(X1)) = domain(X1),
inference(orient,[status(thm)],[t378458]) ).
cnf(t378547,plain,
backward_box(X1,domain(X2)) = coantidomain(multiplication(c(X2),X1)),
inference(step,[status(thm)],[t34642,t34518]) ).
cnf(t378548,plain,
backward_box(X1,X2) = coantidomain(multiplication(c(X2),X1)),
inference(step,[status(thm)],[t378547,t5383]) ).
cnf(t35090,plain,
coantidomain(multiplication(c(X1),X2)) = backward_box(X2,X1),
inference(orient,[status(thm)],[t378548]) ).
cnf(t35176,plain,
zero = multiplication(multiplication(c(X1),X2),backward_box(X2,X1)),
inference(cp,[status(thm)],[t62,t35090]) ).
cnf(t378863,plain,
zero = multiplication(c(X1),multiplication(X2,backward_box(X2,X1))),
inference(step,[status(thm)],[t35176,t55]) ).
cnf(t53277,plain,
multiplication(c(X1),multiplication(X2,backward_box(X2,X1))) = zero,
inference(orient,[status(thm)],[t378863]) ).
cnf(t9519,plain,
multiplication(c(addition(X1,X2)),X1) = multiplication(c(addition(X1,X2)),addition(X1,X2)),
inference(cp,[status(thm)],[t9502,t620]) ).
cnf(t377699,plain,
multiplication(c(addition(X1,X2)),X1) = zero,
inference(step,[status(thm)],[t9519,t2192]) ).
cnf(t9560,plain,
multiplication(c(addition(X1,X2)),X1) = zero,
inference(orient,[status(thm)],[t377699]) ).
cnf(t9573,plain,
multiplication(addition(X1,c(addition(X2,X3))),X2) = addition(multiplication(X1,X2),zero),
inference(cp,[status(thm)],[t82,t9560]) ).
cnf(t380338,plain,
multiplication(addition(X1,c(addition(X2,X3))),X2) = multiplication(X1,X2),
inference(step,[status(thm)],[t9573,t39]) ).
cnf(t130871,plain,
multiplication(addition(X1,c(addition(X2,X3))),X2) = multiplication(X1,X2),
inference(orient,[status(thm)],[t380338]) ).
cnf(t130872,plain,
multiplication(domain(addition(X1,X2)),X1) = multiplication(one,X1),
inference(cp,[status(thm)],[t130871,t492]) ).
cnf(t380339,plain,
multiplication(domain(addition(X1,X2)),X1) = X1,
inference(step,[status(thm)],[t130872,t37]) ).
cnf(t131039,plain,
multiplication(domain(addition(X1,X2)),X1) = X1,
inference(orient,[status(thm)],[t380339]) ).
cnf(t131061,plain,
X1 = multiplication(domain(addition(X2,X1)),X1),
inference(cp,[status(thm)],[t131039,t103]) ).
cnf(t131194,plain,
multiplication(domain(addition(X1,X2)),X2) = X2,
inference(orient,[status(thm)],[t131061]) ).
cnf(t1550,plain,
multiplication(addition(one,domain(X1)),antidomain(X2)) = addition(antidomain(X2),domain_difference(X1,X2)),
inference(cp,[status(thm)],[t1543,t94]) ).
cnf(t377143,plain,
multiplication(one,antidomain(X2)) = addition(antidomain(X2),domain_difference(X1,X2)),
inference(step,[status(thm)],[t1550,t636]) ).
cnf(t377144,plain,
antidomain(X2) = addition(antidomain(X2),domain_difference(X1,X2)),
inference(step,[status(thm)],[t377143,t37]) ).
cnf(t1715,plain,
addition(antidomain(X1),domain_difference(X2,X1)) = antidomain(X1),
inference(orient,[status(thm)],[t377144]) ).
cnf(t377347,plain,
addition(c(X1),domain_difference(X2,X1)) = antidomain(X1),
inference(step,[status(thm)],[t1715,t4627]) ).
cnf(t377348,plain,
addition(c(X1),domain_difference(X2,X1)) = c(X1),
inference(step,[status(thm)],[t377347,t4627]) ).
cnf(t4659,plain,
addition(c(X1),domain_difference(X2,X1)) = c(X1),
inference(rw,[status(thm)],[t377348]) ).
cnf(t5413,plain,
addition(c(X1),domain_difference(X2,X1)) = c(X1),
inference(orient,[status(thm)],[t4659]) ).
cnf(t131219,plain,
domain_difference(X1,X2) = multiplication(domain(c(X2)),domain_difference(X1,X2)),
inference(cp,[status(thm)],[t131194,t5413]) ).
cnf(t380340,plain,
domain_difference(X1,X2) = multiplication(c(X2),domain_difference(X1,X2)),
inference(step,[status(thm)],[t131219,t4709]) ).
cnf(t87,plain,
multiplication(addition(X1,X2),coantidomain(X2)) = addition(multiplication(X1,coantidomain(X2)),zero),
inference(cp,[status(thm)],[t82,t62]) ).
cnf(t377586,plain,
multiplication(addition(X1,X2),coantidomain(X2)) = multiplication(X1,coantidomain(X2)),
inference(step,[status(thm)],[t87,t39]) ).
cnf(t7023,plain,
multiplication(addition(X1,X2),coantidomain(X2)) = multiplication(X1,coantidomain(X2)),
inference(orient,[status(thm)],[t377586]) ).
cnf(t7026,plain,
multiplication(X1,coantidomain(addition(X1,X2))) = multiplication(addition(X1,X2),coantidomain(addition(X1,X2))),
inference(cp,[status(thm)],[t7023,t620]) ).
cnf(t377589,plain,
multiplication(X1,coantidomain(addition(X1,X2))) = zero,
inference(step,[status(thm)],[t7026,t62]) ).
cnf(t7068,plain,
multiplication(X1,coantidomain(addition(X1,X2))) = zero,
inference(orient,[status(thm)],[t377589]) ).
cnf(t7081,plain,
multiplication(X1,addition(X2,coantidomain(addition(X1,X3)))) = addition(multiplication(X1,X2),zero),
inference(cp,[status(thm)],[t58,t7068]) ).
cnf(t379638,plain,
multiplication(X1,addition(X2,coantidomain(addition(X1,X3)))) = multiplication(X1,X2),
inference(step,[status(thm)],[t7081,t39]) ).
cnf(t99531,plain,
multiplication(X1,addition(X2,coantidomain(addition(X1,X3)))) = multiplication(X1,X2),
inference(orient,[status(thm)],[t379638]) ).
cnf(t99533,plain,
multiplication(X1,codomain(addition(X1,X2))) = multiplication(X1,one),
inference(cp,[status(thm)],[t99531,t435]) ).
cnf(t379639,plain,
multiplication(X1,codomain(addition(X1,X2))) = X1,
inference(step,[status(thm)],[t99533,t36]) ).
cnf(t99660,plain,
multiplication(X1,codomain(addition(X1,X2))) = X1,
inference(orient,[status(thm)],[t379639]) ).
cnf(t99674,plain,
X1 = multiplication(X1,codomain(addition(X2,X1))),
inference(cp,[status(thm)],[t99660,t103]) ).
cnf(t99792,plain,
multiplication(X1,codomain(addition(X2,X1))) = X1,
inference(orient,[status(thm)],[t99674]) ).
cnf(t1271,plain,
multiplication(domain(X1),addition(one,antidomain(X2))) = addition(domain(X1),domain_difference(X1,X2)),
inference(cp,[status(thm)],[t1266,t94]) ).
cnf(t377092,plain,
multiplication(domain(X1),one) = addition(domain(X1),domain_difference(X1,X2)),
inference(step,[status(thm)],[t1271,t750]) ).
cnf(t377093,plain,
domain(X1) = addition(domain(X1),domain_difference(X1,X2)),
inference(step,[status(thm)],[t377092,t36]) ).
cnf(t1280,plain,
addition(domain(X1),domain_difference(X1,X2)) = domain(X1),
inference(orient,[status(thm)],[t377093]) ).
cnf(t99810,plain,
domain_difference(X1,X2) = multiplication(domain_difference(X1,X2),codomain(domain(X1))),
inference(cp,[status(thm)],[t99792,t1280]) ).
cnf(t34437,plain,
codomain(domain(X1)) = c(c(X1)),
inference(cp,[status(thm)],[t15518,t34403]) ).
cnf(t378522,plain,
codomain(domain(X1)) = domain(X1),
inference(step,[status(thm)],[t34437,t4718]) ).
cnf(t34563,plain,
codomain(domain(X1)) = domain(X1),
inference(orient,[status(thm)],[t378522]) ).
cnf(t379646,plain,
domain_difference(X1,X2) = multiplication(domain_difference(X1,X2),domain(X1)),
inference(step,[status(thm)],[t99810,t34563]) ).
cnf(t100185,plain,
multiplication(domain_difference(X1,X2),domain(X1)) = domain_difference(X1,X2),
inference(orient,[status(thm)],[t379646]) ).
cnf(t95,plain,
domain_difference(X1,antidomain(X2)) = multiplication(domain(X1),domain(X2)),
inference(cp,[status(thm)],[t94,t44]) ).
cnf(t965,plain,
multiplication(domain(X1),domain(X2)) = domain_difference(X1,antidomain(X2)),
inference(orient,[status(thm)],[t95]) ).
cnf(t971,plain,
domain_difference(antidomain(X1),antidomain(X2)) = multiplication(c(X1),domain(X2)),
inference(cp,[status(thm)],[t965,t252]) ).
cnf(t1769,plain,
domain_difference(antidomain(X1),antidomain(X2)) = multiplication(c(X1),domain(X2)),
inference(orient,[status(thm)],[t971]) ).
cnf(t377344,plain,
domain_difference(c(X1),antidomain(X2)) = multiplication(c(X1),domain(X2)),
inference(step,[status(thm)],[t1769,t4627]) ).
cnf(t377345,plain,
domain_difference(c(X1),c(X2)) = multiplication(c(X1),domain(X2)),
inference(step,[status(thm)],[t377344,t4627]) ).
cnf(t4657,plain,
domain_difference(c(X1),c(X2)) = multiplication(c(X1),domain(X2)),
inference(rw,[status(thm)],[t377345]) ).
cnf(t5440,plain,
domain_difference(c(X1),c(X2)) = multiplication(c(X1),domain(X2)),
inference(orient,[status(thm)],[t4657]) ).
cnf(t100218,plain,
domain_difference(c(X1),c(X2)) = multiplication(multiplication(c(X1),domain(X2)),domain(c(X1))),
inference(cp,[status(thm)],[t100185,t5440]) ).
cnf(t379896,plain,
multiplication(c(X1),domain(X2)) = multiplication(multiplication(c(X1),domain(X2)),domain(c(X1))),
inference(step,[status(thm)],[t100218,t5440]) ).
cnf(t379897,plain,
multiplication(c(X1),domain(X2)) = multiplication(c(X1),multiplication(domain(X2),domain(c(X1)))),
inference(step,[status(thm)],[t379896,t55]) ).
cnf(t377314,plain,
multiplication(domain(X1),domain(X2)) = domain_difference(X1,c(X2)),
inference(step,[status(thm)],[t965,t4627]) ).
cnf(t4630,plain,
multiplication(domain(X1),domain(X2)) = domain_difference(X1,c(X2)),
inference(orient,[status(thm)],[t377314]) ).
cnf(t379898,plain,
multiplication(c(X1),domain(X2)) = multiplication(c(X1),domain_difference(X2,c(c(X1)))),
inference(step,[status(thm)],[t379897,t4630]) ).
cnf(t379899,plain,
multiplication(c(X1),domain(X2)) = multiplication(c(X1),domain_difference(X2,domain(X1))),
inference(step,[status(thm)],[t379898,t4718]) ).
cnf(t379900,plain,
multiplication(c(X1),domain(X2)) = multiplication(c(X1),domain_difference(X2,X1)),
inference(step,[status(thm)],[t379899,t4790]) ).
cnf(t109250,plain,
multiplication(c(X1),domain_difference(X2,X1)) = multiplication(c(X1),domain(X2)),
inference(orient,[status(thm)],[t379900]) ).
cnf(t380341,plain,
domain_difference(X1,X2) = multiplication(c(X2),domain(X1)),
inference(step,[status(thm)],[t380340,t109250]) ).
cnf(t131362,plain,
multiplication(c(X1),domain(X2)) = domain_difference(X2,X1),
inference(orient,[status(thm)],[t380341]) ).
cnf(t131428,plain,
multiplication(c(X1),multiplication(domain(X2),X3)) = multiplication(domain_difference(X2,X1),X3),
inference(cp,[status(thm)],[t55,t131362]) ).
cnf(t157580,plain,
multiplication(c(X1),multiplication(domain(X2),X3)) = multiplication(domain_difference(X2,X1),X3),
inference(orient,[status(thm)],[t131428]) ).
cnf(t157831,plain,
backward_box(multiplication(domain(X1),X2),X3) = coantidomain(multiplication(domain_difference(X1,X3),X2)),
inference(cp,[status(thm)],[t35090,t157580]) ).
cnf(t164688,plain,
coantidomain(multiplication(domain_difference(X1,X2),X3)) = backward_box(multiplication(domain(X1),X3),X2),
inference(orient,[status(thm)],[t157831]) ).
cnf(t21050,plain,
multiplication(c(backward_box(X1,coantidomain(X2))),coantidomain(multiplication(X2,X1))) = multiplication(c(backward_box(X1,coantidomain(X2))),backward_box(X1,coantidomain(X2))),
inference(cp,[status(thm)],[t8590,t20961]) ).
cnf(t378664,plain,
multiplication(backward_diamond(X1,c(coantidomain(X2))),coantidomain(multiplication(X2,X1))) = multiplication(c(backward_box(X1,coantidomain(X2))),backward_box(X1,coantidomain(X2))),
inference(step,[status(thm)],[t21050,t16036]) ).
cnf(t378665,plain,
multiplication(backward_diamond(X1,codomain(X2)),coantidomain(multiplication(X2,X1))) = multiplication(c(backward_box(X1,coantidomain(X2))),backward_box(X1,coantidomain(X2))),
inference(step,[status(thm)],[t378664,t15518]) ).
cnf(t378666,plain,
multiplication(backward_diamond(X1,X2),coantidomain(multiplication(X2,X1))) = multiplication(c(backward_box(X1,coantidomain(X2))),backward_box(X1,coantidomain(X2))),
inference(step,[status(thm)],[t378665,t5768]) ).
cnf(t378667,plain,
multiplication(backward_diamond(X1,X2),coantidomain(multiplication(X2,X1))) = zero,
inference(step,[status(thm)],[t378666,t2192]) ).
cnf(t43890,plain,
multiplication(backward_diamond(X1,X2),coantidomain(multiplication(X2,X1))) = zero,
inference(orient,[status(thm)],[t378667]) ).
cnf(t2119,plain,
multiplication(X1,X2) = multiplication(addition(antidomain(X2),X1),X2),
inference(cp,[status(thm)],[t2114,t103]) ).
cnf(t3117,plain,
multiplication(addition(antidomain(X1),X2),X1) = multiplication(X2,X1),
inference(orient,[status(thm)],[t2119]) ).
cnf(t3118,plain,
multiplication(domain_difference(X1,X2),X2) = multiplication(antidomain(X2),X2),
inference(cp,[status(thm)],[t3117,t1715]) ).
cnf(t377205,plain,
multiplication(domain_difference(X1,X2),X2) = zero,
inference(step,[status(thm)],[t3118,t73]) ).
cnf(t3153,plain,
multiplication(domain_difference(X1,X2),X2) = zero,
inference(orient,[status(thm)],[t377205]) ).
cnf(t43945,plain,
zero = multiplication(backward_diamond(X1,domain_difference(X2,X1)),coantidomain(zero)),
inference(cp,[status(thm)],[t43890,t3153]) ).
cnf(t378668,plain,
zero = multiplication(backward_diamond(X1,domain_difference(X2,X1)),one),
inference(step,[status(thm)],[t43945,t446]) ).
cnf(t378669,plain,
zero = backward_diamond(X1,domain_difference(X2,X1)),
inference(step,[status(thm)],[t378668,t36]) ).
cnf(t44005,plain,
backward_diamond(X1,domain_difference(X2,X1)) = zero,
inference(orient,[status(thm)],[t378669]) ).
cnf(t44020,plain,
one = forward_box(multiplication(codomain(domain_difference(X1,X2)),X2),zero),
inference(cp,[status(thm)],[t33178,t44005]) ).
cnf(t378709,plain,
one = c(multiplication(codomain(domain_difference(X1,X2)),X2)),
inference(step,[status(thm)],[t44020,t4706]) ).
cnf(t44758,plain,
c(multiplication(codomain(domain_difference(X1,X2)),X2)) = one,
inference(orient,[status(thm)],[t378709]) ).
cnf(t44806,plain,
zero = multiplication(one,multiplication(codomain(domain_difference(X1,X2)),X2)),
inference(cp,[status(thm)],[t2192,t44758]) ).
cnf(t378710,plain,
zero = multiplication(codomain(domain_difference(X1,X2)),X2),
inference(step,[status(thm)],[t44806,t37]) ).
cnf(t44899,plain,
multiplication(codomain(domain_difference(X1,X2)),X2) = zero,
inference(orient,[status(thm)],[t378710]) ).
cnf(t44914,plain,
multiplication(addition(codomain(domain_difference(X1,X2)),X3),X2) = addition(zero,multiplication(X3,X2)),
inference(cp,[status(thm)],[t82,t44899]) ).
cnf(t381036,plain,
multiplication(addition(codomain(domain_difference(X1,X2)),X3),X2) = multiplication(X3,X2),
inference(step,[status(thm)],[t44914,t233]) ).
cnf(t175583,plain,
multiplication(addition(codomain(domain_difference(X1,X2)),X3),X2) = multiplication(X3,X2),
inference(orient,[status(thm)],[t381036]) ).
cnf(t175588,plain,
multiplication(coantidomain(domain_difference(X1,X2)),X2) = multiplication(one,X2),
inference(cp,[status(thm)],[t175583,t435]) ).
cnf(t131456,plain,
backward_box(domain(X1),X2) = coantidomain(domain_difference(X1,X2)),
inference(cp,[status(thm)],[t35090,t131362]) ).
cnf(t132016,plain,
coantidomain(domain_difference(X1,X2)) = backward_box(domain(X1),X2),
inference(orient,[status(thm)],[t131456]) ).
cnf(t381037,plain,
multiplication(backward_box(domain(X1),X2),X2) = multiplication(one,X2),
inference(step,[status(thm)],[t175588,t132016]) ).
cnf(t381038,plain,
multiplication(backward_box(domain(X1),X2),X2) = X2,
inference(step,[status(thm)],[t381037,t37]) ).
cnf(t175813,plain,
multiplication(backward_box(domain(X1),X2),X2) = X2,
inference(orient,[status(thm)],[t381038]) ).
cnf(t175860,plain,
X1 = multiplication(backward_box(c(X2),X1),X1),
inference(cp,[status(thm)],[t175813,t4709]) ).
cnf(t176422,plain,
multiplication(backward_box(c(X1),X2),X2) = X2,
inference(orient,[status(thm)],[t175860]) ).
cnf(t176423,plain,
c(X1) = domain_difference(backward_box(c(X2),c(X1)),X1),
inference(cp,[status(thm)],[t176422,t12390]) ).
cnf(t15541,plain,
domain_difference(c(coantidomain(X1)),X2) = multiplication(codomain(X1),c(X2)),
inference(cp,[status(thm)],[t5218,t15518]) ).
cnf(t378041,plain,
domain_difference(codomain(X1),X2) = multiplication(codomain(X1),c(X2)),
inference(step,[status(thm)],[t15541,t15518]) ).
cnf(t17054,plain,
multiplication(codomain(X1),c(X2)) = domain_difference(codomain(X1),X2),
inference(orient,[status(thm)],[t378041]) ).
cnf(t17092,plain,
backward_box(c(X1),coantidomain(X2)) = coantidomain(domain_difference(codomain(X2),X1)),
inference(cp,[status(thm)],[t16439,t17054]) ).
cnf(t18678,plain,
coantidomain(domain_difference(codomain(X1),X2)) = backward_box(c(X2),coantidomain(X1)),
inference(orient,[status(thm)],[t17092]) ).
cnf(t34590,plain,
backward_box(c(X1),coantidomain(domain(X2))) = coantidomain(domain_difference(domain(X2),X1)),
inference(cp,[status(thm)],[t18678,t34563]) ).
cnf(t377996,plain,
coantidomain(backward_diamond(X1,domain(X2))) = backward_box(X1,c(X2)),
inference(step,[status(thm)],[t5333,t15943]) ).
cnf(t16034,plain,
coantidomain(backward_diamond(X1,domain(X2))) = backward_box(X1,c(X2)),
inference(rw,[status(thm)],[t377996]) ).
cnf(t378044,plain,
backward_box(X1,coantidomain(domain(X2))) = backward_box(X1,c(X2)),
inference(step,[status(thm)],[t16034,t16438]) ).
cnf(t17547,plain,
backward_box(X1,coantidomain(domain(X2))) = backward_box(X1,c(X2)),
inference(orient,[status(thm)],[t378044]) ).
cnf(t378574,plain,
backward_box(c(X1),c(X2)) = coantidomain(domain_difference(domain(X2),X1)),
inference(step,[status(thm)],[t34590,t17547]) ).
cnf(t5223,plain,
domain_difference(c(c(X1)),X2) = multiplication(domain(X1),c(X2)),
inference(cp,[status(thm)],[t5218,t4718]) ).
cnf(t377485,plain,
domain_difference(domain(X1),X2) = multiplication(domain(X1),c(X2)),
inference(step,[status(thm)],[t5223,t4718]) ).
cnf(t377457,plain,
multiplication(domain(X1),c(X2)) = domain_difference(X1,X2),
inference(step,[status(thm)],[t991,t4790]) ).
cnf(t4791,plain,
multiplication(domain(X1),c(X2)) = domain_difference(X1,X2),
inference(orient,[status(thm)],[t377457]) ).
cnf(t377486,plain,
domain_difference(domain(X1),X2) = domain_difference(X1,X2),
inference(step,[status(thm)],[t377485,t4791]) ).
cnf(t5255,plain,
domain_difference(domain(X1),X2) = domain_difference(X1,X2),
inference(orient,[status(thm)],[t377486]) ).
cnf(t378575,plain,
backward_box(c(X1),c(X2)) = coantidomain(domain_difference(X2,X1)),
inference(step,[status(thm)],[t378574,t5255]) ).
cnf(t36026,plain,
backward_box(c(X1),c(X2)) = coantidomain(domain_difference(X2,X1)),
inference(orient,[status(thm)],[t378575]) ).
cnf(t380374,plain,
backward_box(c(X1),c(X2)) = backward_box(domain(X2),X1),
inference(step,[status(thm)],[t36026,t132016]) ).
cnf(t132019,plain,
backward_box(c(X1),c(X2)) = backward_box(domain(X2),X1),
inference(orient,[status(thm)],[t380374]) ).
cnf(t381047,plain,
c(X1) = domain_difference(backward_box(domain(X1),X2),X1),
inference(step,[status(thm)],[t176423,t132019]) ).
cnf(t177438,plain,
domain_difference(backward_box(domain(X1),X2),X1) = c(X1),
inference(orient,[status(thm)],[t381047]) ).
cnf(t10975,plain,
multiplication(codomain(domain(X1)),multiplication(X1,X2)) = multiplication(X1,X2),
inference(cp,[status(thm)],[t55,t10955]) ).
cnf(t23599,plain,
multiplication(codomain(domain(X1)),multiplication(X1,X2)) = multiplication(X1,X2),
inference(orient,[status(thm)],[t10975]) ).
cnf(t23667,plain,
backward_box(multiplication(X1,X2),coantidomain(domain(X1))) = coantidomain(multiplication(X1,X2)),
inference(cp,[status(thm)],[t16439,t23599]) ).
cnf(t378143,plain,
backward_box(multiplication(X1,X2),c(X1)) = coantidomain(multiplication(X1,X2)),
inference(step,[status(thm)],[t23667,t17547]) ).
cnf(t23672,plain,
backward_box(multiplication(X1,X2),c(X1)) = coantidomain(multiplication(X1,X2)),
inference(orient,[status(thm)],[t378143]) ).
fof(f26,conjecture,
! [X0,X1,X2] :
( addition(forward_diamond(X0,domain(X1)),domain(X2)) = domain(X2)
=> multiplication(antidomain(X2),multiplication(X0,domain(X1))) = zero ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goals) ).
fof(f26_neg,negated_conjecture,
~ ! [X0,X1,X2] :
( addition(forward_diamond(X0,domain(X1)),domain(X2)) = domain(X2)
=> multiplication(antidomain(X2),multiplication(X0,domain(X1))) = zero ),
inference(negated_conjecture,[status(cth)],[f26]) ).
fof(f26_nnf,plain,
? [X0,X1,X2] :
( multiplication(antidomain(X2),multiplication(X0,domain(X1))) != zero
& addition(forward_diamond(X0,domain(X1)),domain(X2)) = domain(X2) ),
inference(nnf_transformation,[status(thm)],[f26_neg]) ).
fof(f26_sk,plain,
( multiplication(antidomain(sk2),multiplication(sk0,domain(sk1))) != zero
& addition(forward_diamond(sk0,domain(sk1)),domain(sk2)) = domain(sk2) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk0,sk1,sk2])],[f26_nnf]) ).
cnf(c27,plain,
addition(forward_diamond(sk0,domain(sk1)),domain(sk2)) = domain(sk2),
inference(cnf_transformation,[status(esa)],[f26_sk]) ).
cnf(t23,plain,
addition(forward_diamond(sk0,domain(sk1)),domain(sk2)) = domain(sk2),
inference(equality_encoding,[status(esa)],[c27]) ).
cnf(t376968,plain,
addition(domain(sk2),forward_diamond(sk0,domain(sk1))) = domain(sk2),
inference(step,[status(thm)],[t23,t103]) ).
cnf(t139,plain,
addition(domain(sk2),forward_diamond(sk0,domain(sk1))) = domain(sk2),
inference(orient,[status(thm)],[t376968]) ).
cnf(t4743,plain,
forward_diamond(X1,c(c(X2))) = domain(multiplication(X1,domain(X2))),
inference(cp,[status(thm)],[t4634,t4718]) ).
cnf(t377464,plain,
forward_diamond(X1,domain(X2)) = domain(multiplication(X1,domain(X2))),
inference(step,[status(thm)],[t4743,t4718]) ).
cnf(t377465,plain,
forward_diamond(X1,domain(X2)) = forward_diamond(X1,X2),
inference(step,[status(thm)],[t377464,t182]) ).
cnf(t4847,plain,
forward_diamond(X1,domain(X2)) = forward_diamond(X1,X2),
inference(orient,[status(thm)],[t377465]) ).
cnf(t377468,plain,
addition(domain(sk2),forward_diamond(sk0,sk1)) = domain(sk2),
inference(step,[status(thm)],[t139,t4847]) ).
cnf(t4855,plain,
addition(domain(sk2),forward_diamond(sk0,sk1)) = domain(sk2),
inference(rw,[status(thm)],[t377468]) ).
cnf(t5431,plain,
addition(domain(sk2),forward_diamond(sk0,sk1)) = domain(sk2),
inference(orient,[status(thm)],[t4855]) ).
cnf(t99808,plain,
forward_diamond(sk0,sk1) = multiplication(forward_diamond(sk0,sk1),codomain(domain(sk2))),
inference(cp,[status(thm)],[t99792,t5431]) ).
cnf(t379645,plain,
forward_diamond(sk0,sk1) = multiplication(forward_diamond(sk0,sk1),domain(sk2)),
inference(step,[status(thm)],[t99808,t34563]) ).
cnf(t100145,plain,
multiplication(forward_diamond(sk0,sk1),domain(sk2)) = forward_diamond(sk0,sk1),
inference(orient,[status(thm)],[t379645]) ).
cnf(t100147,plain,
coantidomain(multiplication(forward_diamond(sk0,sk1),domain(sk2))) = backward_box(forward_diamond(sk0,sk1),c(forward_diamond(sk0,sk1))),
inference(cp,[status(thm)],[t23672,t100145]) ).
cnf(t377316,plain,
c(multiplication(X1,domain(X2))) = c(forward_diamond(X1,X2)),
inference(step,[status(thm)],[t1016,t4627]) ).
cnf(t4632,plain,
c(multiplication(X1,domain(X2))) = c(forward_diamond(X1,X2)),
inference(orient,[status(thm)],[t377316]) ).
cnf(t4720,plain,
domain(multiplication(X1,domain(X2))) = c(c(forward_diamond(X1,X2))),
inference(cp,[status(thm)],[t4718,t4632]) ).
cnf(t377462,plain,
forward_diamond(X1,X2) = c(c(forward_diamond(X1,X2))),
inference(step,[status(thm)],[t4720,t182]) ).
cnf(t377463,plain,
forward_diamond(X1,X2) = domain(forward_diamond(X1,X2)),
inference(step,[status(thm)],[t377462,t4718]) ).
cnf(t4809,plain,
domain(forward_diamond(X1,X2)) = forward_diamond(X1,X2),
inference(orient,[status(thm)],[t377463]) ).
cnf(t34577,plain,
domain(forward_diamond(X1,X2)) = codomain(forward_diamond(X1,X2)),
inference(cp,[status(thm)],[t34563,t4809]) ).
cnf(t378542,plain,
forward_diamond(X1,X2) = codomain(forward_diamond(X1,X2)),
inference(step,[status(thm)],[t34577,t4809]) ).
cnf(t34741,plain,
codomain(forward_diamond(X1,X2)) = forward_diamond(X1,X2),
inference(orient,[status(thm)],[t378542]) ).
cnf(t34826,plain,
backward_box(X1,coantidomain(forward_diamond(X2,X3))) = coantidomain(multiplication(forward_diamond(X2,X3),X1)),
inference(cp,[status(thm)],[t16439,t34741]) ).
cnf(t34423,plain,
c(forward_diamond(X1,X2)) = coantidomain(forward_diamond(X1,X2)),
inference(cp,[status(thm)],[t34403,t4809]) ).
cnf(t4954,plain,
forward_box(X1,c(X2)) = c(multiplication(X1,domain(X2))),
inference(cp,[status(thm)],[t4946,t4718]) ).
cnf(t377474,plain,
forward_box(X1,c(X2)) = c(forward_diamond(X1,X2)),
inference(step,[status(thm)],[t4954,t4632]) ).
cnf(t5060,plain,
c(forward_diamond(X1,X2)) = forward_box(X1,c(X2)),
inference(orient,[status(thm)],[t377474]) ).
cnf(t378545,plain,
forward_box(X1,c(X2)) = coantidomain(forward_diamond(X1,X2)),
inference(step,[status(thm)],[t34423,t5060]) ).
cnf(t34956,plain,
coantidomain(forward_diamond(X1,X2)) = forward_box(X1,c(X2)),
inference(orient,[status(thm)],[t378545]) ).
cnf(t379157,plain,
backward_box(X1,forward_box(X2,c(X3))) = coantidomain(multiplication(forward_diamond(X2,X3),X1)),
inference(step,[status(thm)],[t34826,t34956]) ).
cnf(t75451,plain,
coantidomain(multiplication(forward_diamond(X1,X2),X3)) = backward_box(X3,forward_box(X1,c(X2))),
inference(orient,[status(thm)],[t379157]) ).
cnf(t380211,plain,
backward_box(domain(sk2),forward_box(sk0,c(sk1))) = backward_box(forward_diamond(sk0,sk1),c(forward_diamond(sk0,sk1))),
inference(step,[status(thm)],[t100147,t75451]) ).
cnf(t471,plain,
backward_box(multiplication(codomain(X1),X2),zero) = c(backward_diamond(X2,X1)),
inference(cp,[status(thm)],[t470,t200]) ).
cnf(t8108,plain,
backward_box(multiplication(codomain(X1),X2),zero) = c(backward_diamond(X2,X1)),
inference(orient,[status(thm)],[t471]) ).
cnf(t10981,plain,
c(backward_diamond(X1,domain(X1))) = backward_box(X1,zero),
inference(cp,[status(thm)],[t8108,t10955]) ).
cnf(t377759,plain,
backward_box(X1,c(X1)) = backward_box(X1,zero),
inference(step,[status(thm)],[t10981,t5333]) ).
cnf(t11014,plain,
backward_box(X1,c(X1)) = backward_box(X1,zero),
inference(orient,[status(thm)],[t377759]) ).
cnf(t377898,plain,
backward_box(X1,c(X1)) = coantidomain(X1),
inference(step,[status(thm)],[t11014,t15466]) ).
cnf(t15471,plain,
backward_box(X1,c(X1)) = coantidomain(X1),
inference(orient,[status(thm)],[t377898]) ).
cnf(t380212,plain,
backward_box(domain(sk2),forward_box(sk0,c(sk1))) = coantidomain(forward_diamond(sk0,sk1)),
inference(step,[status(thm)],[t380211,t15471]) ).
cnf(t380213,plain,
backward_box(domain(sk2),forward_box(sk0,c(sk1))) = forward_box(sk0,c(sk1)),
inference(step,[status(thm)],[t380212,t34956]) ).
cnf(t123979,plain,
backward_box(domain(sk2),forward_box(sk0,c(sk1))) = forward_box(sk0,c(sk1)),
inference(orient,[status(thm)],[t380213]) ).
cnf(t177461,plain,
c(sk2) = domain_difference(forward_box(sk0,c(sk1)),sk2),
inference(cp,[status(thm)],[t177438,t123979]) ).
cnf(t178269,plain,
domain_difference(forward_box(sk0,c(sk1)),sk2) = c(sk2),
inference(orient,[status(thm)],[t177461]) ).
cnf(t178287,plain,
backward_box(multiplication(domain(forward_box(sk0,c(sk1))),X1),sk2) = coantidomain(multiplication(c(sk2),X1)),
inference(cp,[status(thm)],[t164688,t178269]) ).
cnf(t4985,plain,
c(multiplication(X1,c(X2))) = domain(forward_box(X1,X2)),
inference(cp,[status(thm)],[t4709,t4946]) ).
cnf(t377473,plain,
forward_box(X1,X2) = domain(forward_box(X1,X2)),
inference(step,[status(thm)],[t4985,t4946]) ).
cnf(t5007,plain,
domain(forward_box(X1,X2)) = forward_box(X1,X2),
inference(orient,[status(thm)],[t377473]) ).
cnf(t383335,plain,
backward_box(multiplication(forward_box(sk0,c(sk1)),X1),sk2) = coantidomain(multiplication(c(sk2),X1)),
inference(step,[status(thm)],[t178287,t5007]) ).
cnf(t383336,plain,
backward_box(multiplication(forward_box(sk0,c(sk1)),X1),sk2) = backward_box(X1,sk2),
inference(step,[status(thm)],[t383335,t35090]) ).
cnf(t376345,plain,
backward_box(multiplication(forward_box(sk0,c(sk1)),X1),sk2) = backward_box(X1,sk2),
inference(orient,[status(thm)],[t383336]) ).
cnf(t4980,plain,
zero = multiplication(forward_box(X1,X2),multiplication(X1,c(X2))),
inference(cp,[status(thm)],[t2192,t4946]) ).
cnf(t28040,plain,
multiplication(forward_box(X1,X2),multiplication(X1,c(X2))) = zero,
inference(orient,[status(thm)],[t4980]) ).
cnf(t376348,plain,
backward_box(multiplication(sk0,c(c(sk1))),sk2) = backward_box(zero,sk2),
inference(cp,[status(thm)],[t376345,t28040]) ).
cnf(t383337,plain,
backward_box(multiplication(sk0,domain(sk1)),sk2) = backward_box(zero,sk2),
inference(step,[status(thm)],[t376348,t4718]) ).
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(t69,plain,
multiplication(X1,zero) = zero,
inference(orient,[status(thm)],[t6]) ).
cnf(t201,plain,
backward_diamond(zero,X1) = codomain(zero),
inference(cp,[status(thm)],[t200,t69]) ).
cnf(t243,plain,
backward_diamond(zero,X1) = codomain(zero),
inference(orient,[status(thm)],[t201]) ).
cnf(t244,plain,
backward_box(zero,X1) = c(codomain(zero)),
inference(cp,[status(thm)],[t196,t243]) ).
cnf(t377054,plain,
backward_box(zero,X1) = backward_box(zero,zero),
inference(step,[status(thm)],[t244,t470]) ).
cnf(t214,plain,
c(one) = antidomain(one),
inference(cp,[status(thm)],[t53,t212]) ).
cnf(t376980,plain,
c(one) = zero,
inference(step,[status(thm)],[t214,t208]) ).
cnf(t216,plain,
c(one) = zero,
inference(orient,[status(thm)],[t376980]) ).
cnf(t217,plain,
backward_box(X1,one) = c(backward_diamond(X1,zero)),
inference(cp,[status(thm)],[t196,t216]) ).
cnf(t310,plain,
c(backward_diamond(X1,zero)) = backward_box(X1,one),
inference(orient,[status(thm)],[t217]) ).
cnf(t311,plain,
backward_box(zero,one) = c(codomain(zero)),
inference(cp,[status(thm)],[t310,t243]) ).
cnf(t316,plain,
c(codomain(zero)) = backward_box(zero,one),
inference(orient,[status(thm)],[t311]) ).
cnf(t323,plain,
backward_box(zero,zero) = c(codomain(zero)),
inference(cp,[status(thm)],[t322,t243]) ).
cnf(t377002,plain,
backward_box(zero,zero) = backward_box(zero,one),
inference(step,[status(thm)],[t323,t316]) ).
cnf(t328,plain,
backward_box(zero,one) = backward_box(zero,zero),
inference(orient,[status(thm)],[t377002]) ).
cnf(t377003,plain,
c(codomain(zero)) = backward_box(zero,zero),
inference(step,[status(thm)],[t316,t328]) ).
cnf(t329,plain,
c(codomain(zero)) = backward_box(zero,zero),
inference(orient,[status(thm)],[t377003]) ).
cnf(t449,plain,
codomain(coantidomain(one)) = coantidomain(one),
inference(cp,[status(thm)],[t269,t445]) ).
cnf(t377020,plain,
codomain(zero) = coantidomain(one),
inference(step,[status(thm)],[t449,t206]) ).
cnf(t377021,plain,
codomain(zero) = zero,
inference(step,[status(thm)],[t377020,t206]) ).
cnf(t451,plain,
codomain(zero) = zero,
inference(orient,[status(thm)],[t377021]) ).
cnf(t377024,plain,
c(zero) = backward_box(zero,zero),
inference(step,[status(thm)],[t329,t451]) ).
cnf(t377025,plain,
one = backward_box(zero,zero),
inference(step,[status(thm)],[t377024,t230]) ).
cnf(t456,plain,
one = backward_box(zero,zero),
inference(rw,[status(thm)],[t377025]) ).
cnf(t463,plain,
backward_box(zero,zero) = one,
inference(orient,[status(thm)],[t456]) ).
cnf(t377055,plain,
backward_box(zero,X1) = one,
inference(step,[status(thm)],[t377054,t463]) ).
cnf(t619,plain,
backward_box(zero,X1) = one,
inference(orient,[status(thm)],[t377055]) ).
cnf(t383338,plain,
backward_box(multiplication(sk0,domain(sk1)),sk2) = one,
inference(step,[status(thm)],[t383337,t619]) ).
cnf(t376470,plain,
backward_box(multiplication(sk0,domain(sk1)),sk2) = one,
inference(orient,[status(thm)],[t383338]) ).
cnf(t376476,plain,
zero = multiplication(c(sk2),multiplication(multiplication(sk0,domain(sk1)),one)),
inference(cp,[status(thm)],[t53277,t376470]) ).
cnf(t383344,plain,
zero = multiplication(c(sk2),multiplication(sk0,multiplication(domain(sk1),one))),
inference(step,[status(thm)],[t376476,t55]) ).
cnf(t383345,plain,
zero = multiplication(c(sk2),multiplication(sk0,domain(sk1))),
inference(step,[status(thm)],[t383344,t36]) ).
cnf(t376904,plain,
multiplication(c(sk2),multiplication(sk0,domain(sk1))) = zero,
inference(orient,[status(thm)],[t383345]) ).
cnf(c28,plain,
multiplication(antidomain(sk2),multiplication(sk0,domain(sk1))) != zero,
inference(cnf_transformation,[status(esa)],[f26_sk]) ).
cnf(goal_0,negated_conjecture,
multiplication(antidomain(sk2),multiplication(sk0,domain(sk1))) != zero,
inference(equality_encoding,[status(esa)],[c28]) ).
cnf(g0_0,plain,
multiplication(c(sk2),multiplication(sk0,domain(sk1))) != zero,
inference(rw,[status(thm)],[goal_0,t4627]) ).
cnf(g0_1,plain,
zero != zero,
inference(rw,[status(thm)],[g0_0,t376904]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : KLE099+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.10/0.36 % Computer : n010.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Wed Sep 23 18:56:42 UTC 2026
% 0.14/0.36 % CPUTime :
% 0.14/0.36 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 249.89/32.44 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 249.89/32.44 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------