%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : KLE120+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 : n005.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:39 PM UTC 2026
% Result : Theorem 44.69s 6.29s
% Output : Proof 44.69s
% Verified :
% SZS Type : Refutation
% Derivation depth : 86
% Number of leaves : 27
% Syntax : Number of formulae : 623 ( 618 unt; 0 def)
% Number of atoms : 632 ( 624 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 24 ( 15 ~; 6 |; 2 &)
% ( 1 <=>; 0 =>; 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 : 17 ( 17 usr; 4 con; 0-4 aty)
% Number of variables : 850 ( 27 sgn 128 !; 1 ?)
% Comments :
%------------------------------------------------------------------------------
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(t100,plain,
addition(X1,X2) = addition(X2,X1),
inference(orient,[status(thm)],[t14]) ).
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(t28,plain,
addition(multiplication(X1,X2),multiplication(X3,X2)) = multiplication(addition(X1,X3),X2),
inference(equality_encoding,[status(esa)],[c8]) ).
cnf(t60,plain,
addition(multiplication(X1,X2),multiplication(X3,X2)) = multiplication(addition(X1,X3),X2),
inference(orient,[status(thm)],[t28]) ).
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(t46,plain,
multiplication(X1,coantidomain(X1)) = zero,
inference(orient,[status(thm)],[t12]) ).
cnf(t61,plain,
multiplication(addition(X1,X2),coantidomain(X1)) = addition(zero,multiplication(X2,coantidomain(X1))),
inference(cp,[status(thm)],[t60,t46]) ).
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(t36,plain,
addition(X1,zero) = X1,
inference(orient,[status(thm)],[t1]) ).
cnf(t101,plain,
addition(zero,X1) = X1,
inference(cp,[status(thm)],[t100,t36]) ).
cnf(t222,plain,
addition(zero,X1) = X1,
inference(orient,[status(thm)],[t101]) ).
cnf(t47488,plain,
multiplication(addition(X1,X2),coantidomain(X1)) = multiplication(X2,coantidomain(X1)),
inference(step,[status(thm)],[t61,t222]) ).
cnf(t4366,plain,
multiplication(addition(X1,X2),coantidomain(X1)) = multiplication(X2,coantidomain(X1)),
inference(orient,[status(thm)],[t47488]) ).
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(t47062,plain,
addition(coantidomain(X1),coantidomain(coantidomain(X1))) = one,
inference(step,[status(thm)],[t17,t100]) ).
cnf(t131,plain,
addition(coantidomain(X1),coantidomain(coantidomain(X1))) = one,
inference(orient,[status(thm)],[t47062]) ).
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(t134,plain,
coantidomain(coantidomain(X1)) = codomain(X1),
inference(orient,[status(thm)],[t11]) ).
cnf(t47063,plain,
addition(coantidomain(X1),codomain(X1)) = one,
inference(step,[status(thm)],[t131,t134]) ).
cnf(t137,plain,
addition(coantidomain(X1),codomain(X1)) = one,
inference(rw,[status(thm)],[t47063]) ).
cnf(t47105,plain,
addition(codomain(X1),coantidomain(X1)) = one,
inference(step,[status(thm)],[t137,t100]) ).
cnf(t416,plain,
addition(codomain(X1),coantidomain(X1)) = one,
inference(orient,[status(thm)],[t47105]) ).
cnf(t4371,plain,
multiplication(coantidomain(X1),coantidomain(codomain(X1))) = multiplication(one,coantidomain(codomain(X1))),
inference(cp,[status(thm)],[t4366,t416]) ).
cnf(t135,plain,
codomain(coantidomain(X1)) = coantidomain(codomain(X1)),
inference(cp,[status(thm)],[t134,t134]) ).
cnf(t257,plain,
coantidomain(codomain(X1)) = codomain(coantidomain(X1)),
inference(orient,[status(thm)],[t135]) ).
cnf(t47489,plain,
multiplication(coantidomain(X1),codomain(coantidomain(X1))) = multiplication(one,coantidomain(codomain(X1))),
inference(step,[status(thm)],[t4371,t257]) ).
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(t27,plain,
addition(multiplication(X1,X2),multiplication(X1,X3)) = multiplication(X1,addition(X2,X3)),
inference(equality_encoding,[status(esa)],[c7]) ).
cnf(t42,plain,
addition(multiplication(X1,X2),multiplication(X1,X3)) = multiplication(X1,addition(X2,X3)),
inference(orient,[status(thm)],[t27]) ).
cnf(t50,plain,
multiplication(X1,addition(X2,coantidomain(X1))) = addition(multiplication(X1,X2),zero),
inference(cp,[status(thm)],[t42,t46]) ).
cnf(t47231,plain,
multiplication(X1,addition(X2,coantidomain(X1))) = multiplication(X1,X2),
inference(step,[status(thm)],[t50,t36]) ).
cnf(t1861,plain,
multiplication(X1,addition(X2,coantidomain(X1))) = multiplication(X1,X2),
inference(orient,[status(thm)],[t47231]) ).
cnf(t1863,plain,
multiplication(X1,codomain(X1)) = multiplication(X1,one),
inference(cp,[status(thm)],[t1861,t416]) ).
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(t33,plain,
multiplication(X1,one) = X1,
inference(orient,[status(thm)],[t5]) ).
cnf(t47232,plain,
multiplication(X1,codomain(X1)) = X1,
inference(step,[status(thm)],[t1863,t33]) ).
cnf(t1884,plain,
multiplication(X1,codomain(X1)) = X1,
inference(orient,[status(thm)],[t47232]) ).
cnf(t47490,plain,
coantidomain(X1) = multiplication(one,coantidomain(codomain(X1))),
inference(step,[status(thm)],[t47489,t1884]) ).
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(t34,plain,
multiplication(one,X1) = X1,
inference(orient,[status(thm)],[t7]) ).
cnf(t47491,plain,
coantidomain(X1) = coantidomain(codomain(X1)),
inference(step,[status(thm)],[t47490,t34]) ).
cnf(t47492,plain,
coantidomain(X1) = codomain(coantidomain(X1)),
inference(step,[status(thm)],[t47491,t257]) ).
cnf(t4392,plain,
codomain(coantidomain(X1)) = coantidomain(X1),
inference(orient,[status(thm)],[t47492]) ).
cnf(t4395,plain,
coantidomain(coantidomain(X1)) = codomain(codomain(X1)),
inference(cp,[status(thm)],[t4392,t134]) ).
cnf(t47498,plain,
codomain(X1) = codomain(codomain(X1)),
inference(step,[status(thm)],[t4395,t134]) ).
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(t188,plain,
codomain(multiplication(codomain(X1),X2)) = backward_diamond(X2,X1),
inference(orient,[status(thm)],[t20]) ).
cnf(t190,plain,
backward_diamond(one,X1) = codomain(codomain(X1)),
inference(cp,[status(thm)],[t188,t33]) ).
cnf(t271,plain,
codomain(codomain(X1)) = backward_diamond(one,X1),
inference(orient,[status(thm)],[t190]) ).
cnf(t47499,plain,
codomain(X1) = backward_diamond(one,X1),
inference(step,[status(thm)],[t47498,t271]) ).
cnf(t4411,plain,
backward_diamond(one,X1) = codomain(X1),
inference(orient,[status(thm)],[t47499]) ).
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(t184,plain,
c(backward_diamond(X1,c(X2))) = backward_box(X1,X2),
inference(orient,[status(thm)],[t18]) ).
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(t96,plain,
antidomain(domain(X1)) = c(X1),
inference(orient,[status(thm)],[t10]) ).
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(t91,plain,
antidomain(antidomain(X1)) = domain(X1),
inference(orient,[status(thm)],[t9]) ).
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(t55,plain,
multiplication(antidomain(X1),X1) = zero,
inference(orient,[status(thm)],[t13]) ).
cnf(t56,plain,
zero = antidomain(one),
inference(cp,[status(thm)],[t55,t33]) ).
cnf(t196,plain,
antidomain(one) = zero,
inference(orient,[status(thm)],[t56]) ).
cnf(t198,plain,
domain(one) = antidomain(zero),
inference(cp,[status(thm)],[t91,t196]) ).
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(t47059,plain,
addition(antidomain(X1),antidomain(antidomain(X1))) = one,
inference(step,[status(thm)],[t16,t100]) ).
cnf(t47060,plain,
addition(antidomain(X1),domain(X1)) = one,
inference(step,[status(thm)],[t47059,t91]) ).
cnf(t47061,plain,
addition(domain(X1),antidomain(X1)) = one,
inference(step,[status(thm)],[t47060,t100]) ).
cnf(t114,plain,
addition(domain(X1),antidomain(X1)) = one,
inference(orient,[status(thm)],[t47061]) ).
cnf(t197,plain,
one = addition(domain(one),zero),
inference(cp,[status(thm)],[t114,t196]) ).
cnf(t47068,plain,
one = domain(one),
inference(step,[status(thm)],[t197,t36]) ).
cnf(t200,plain,
domain(one) = one,
inference(orient,[status(thm)],[t47068]) ).
cnf(t47070,plain,
one = antidomain(zero),
inference(step,[status(thm)],[t198,t200]) ).
cnf(t209,plain,
antidomain(zero) = one,
inference(orient,[status(thm)],[t47070]) ).
cnf(t211,plain,
domain(zero) = antidomain(one),
inference(cp,[status(thm)],[t91,t209]) ).
cnf(t47071,plain,
domain(zero) = zero,
inference(step,[status(thm)],[t211,t196]) ).
cnf(t213,plain,
domain(zero) = zero,
inference(orient,[status(thm)],[t47071]) ).
cnf(t215,plain,
c(zero) = antidomain(zero),
inference(cp,[status(thm)],[t96,t213]) ).
cnf(t47072,plain,
c(zero) = one,
inference(step,[status(thm)],[t215,t209]) ).
cnf(t218,plain,
c(zero) = one,
inference(orient,[status(thm)],[t47072]) ).
cnf(t219,plain,
backward_box(X1,zero) = c(backward_diamond(X1,one)),
inference(cp,[status(thm)],[t184,t218]) ).
cnf(t309,plain,
c(backward_diamond(X1,one)) = backward_box(X1,zero),
inference(orient,[status(thm)],[t219]) ).
cnf(t48,plain,
zero = coantidomain(one),
inference(cp,[status(thm)],[t46,t34]) ).
cnf(t194,plain,
coantidomain(one) = zero,
inference(orient,[status(thm)],[t48]) ).
cnf(t422,plain,
one = addition(codomain(one),zero),
inference(cp,[status(thm)],[t416,t194]) ).
cnf(t47106,plain,
one = codomain(one),
inference(step,[status(thm)],[t422,t36]) ).
cnf(t426,plain,
codomain(one) = one,
inference(orient,[status(thm)],[t47106]) ).
cnf(t431,plain,
backward_diamond(X1,one) = codomain(multiplication(one,X1)),
inference(cp,[status(thm)],[t188,t426]) ).
cnf(t47124,plain,
backward_diamond(X1,one) = codomain(X1),
inference(step,[status(thm)],[t431,t34]) ).
cnf(t449,plain,
backward_diamond(X1,one) = codomain(X1),
inference(orient,[status(thm)],[t47124]) ).
cnf(t47125,plain,
c(codomain(X1)) = backward_box(X1,zero),
inference(step,[status(thm)],[t309,t449]) ).
cnf(t450,plain,
c(codomain(X1)) = backward_box(X1,zero),
inference(rw,[status(thm)],[t47125]) ).
cnf(t451,plain,
c(codomain(X1)) = backward_box(X1,zero),
inference(orient,[status(thm)],[t450]) ).
cnf(t4401,plain,
backward_box(coantidomain(X1),zero) = c(coantidomain(X1)),
inference(cp,[status(thm)],[t451,t4392]) ).
cnf(t4436,plain,
backward_box(coantidomain(X1),zero) = c(coantidomain(X1)),
inference(orient,[status(thm)],[t4401]) ).
cnf(t43,plain,
multiplication(X1,addition(one,X2)) = addition(X1,multiplication(X1,X2)),
inference(cp,[status(thm)],[t42,t33]) ).
cnf(t599,plain,
addition(X1,multiplication(X1,X2)) = multiplication(X1,addition(one,X2)),
inference(orient,[status(thm)],[t43]) ).
cnf(t66,plain,
multiplication(addition(X1,antidomain(X2)),X2) = addition(multiplication(X1,X2),zero),
inference(cp,[status(thm)],[t60,t55]) ).
cnf(t47238,plain,
multiplication(addition(X1,antidomain(X2)),X2) = multiplication(X1,X2),
inference(step,[status(thm)],[t66,t36]) ).
cnf(t1991,plain,
multiplication(addition(X1,antidomain(X2)),X2) = multiplication(X1,X2),
inference(orient,[status(thm)],[t47238]) ).
cnf(t1992,plain,
multiplication(domain(X1),X1) = multiplication(one,X1),
inference(cp,[status(thm)],[t1991,t114]) ).
cnf(t47239,plain,
multiplication(domain(X1),X1) = X1,
inference(step,[status(thm)],[t1992,t34]) ).
cnf(t2023,plain,
multiplication(domain(X1),X1) = X1,
inference(orient,[status(thm)],[t47239]) ).
cnf(t2040,plain,
multiplication(domain(X1),addition(one,X1)) = addition(domain(X1),X1),
inference(cp,[status(thm)],[t599,t2023]) ).
cnf(t47599,plain,
multiplication(domain(X1),addition(one,X1)) = addition(X1,domain(X1)),
inference(step,[status(thm)],[t2040,t100]) ).
cnf(t6670,plain,
multiplication(domain(X1),addition(one,X1)) = addition(X1,domain(X1)),
inference(orient,[status(thm)],[t47599]) ).
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(t172,plain,
domain(multiplication(X1,domain(X2))) = forward_diamond(X1,X2),
inference(orient,[status(thm)],[t21]) ).
cnf(t178,plain,
c(multiplication(X1,domain(X2))) = antidomain(forward_diamond(X1,X2)),
inference(cp,[status(thm)],[t96,t172]) ).
cnf(t1004,plain,
c(multiplication(X1,domain(X2))) = antidomain(forward_diamond(X1,X2)),
inference(orient,[status(thm)],[t178]) ).
cnf(t92,plain,
domain(antidomain(X1)) = antidomain(domain(X1)),
inference(cp,[status(thm)],[t91,t91]) ).
cnf(t47084,plain,
domain(antidomain(X1)) = c(X1),
inference(step,[status(thm)],[t92,t96]) ).
cnf(t241,plain,
domain(antidomain(X1)) = c(X1),
inference(orient,[status(thm)],[t47084]) ).
cnf(t1012,plain,
antidomain(forward_diamond(X1,antidomain(X2))) = c(multiplication(X1,c(X2))),
inference(cp,[status(thm)],[t1004,t241]) ).
cnf(t1738,plain,
antidomain(forward_diamond(X1,antidomain(X2))) = c(multiplication(X1,c(X2))),
inference(orient,[status(thm)],[t1012]) ).
cnf(t57,plain,
multiplication(antidomain(X1),addition(X1,X2)) = addition(zero,multiplication(antidomain(X1),X2)),
inference(cp,[status(thm)],[t42,t55]) ).
cnf(t47324,plain,
multiplication(antidomain(X1),addition(X1,X2)) = multiplication(antidomain(X1),X2),
inference(step,[status(thm)],[t57,t222]) ).
cnf(t3421,plain,
multiplication(antidomain(X1),addition(X1,X2)) = multiplication(antidomain(X1),X2),
inference(orient,[status(thm)],[t47324]) ).
cnf(t3437,plain,
multiplication(antidomain(domain(X1)),antidomain(X1)) = multiplication(antidomain(domain(X1)),one),
inference(cp,[status(thm)],[t3421,t114]) ).
cnf(t47325,plain,
multiplication(c(X1),antidomain(X1)) = multiplication(antidomain(domain(X1)),one),
inference(step,[status(thm)],[t3437,t96]) ).
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(t72,plain,
multiplication(domain(X1),antidomain(X2)) = domain_difference(X1,X2),
inference(orient,[status(thm)],[t22]) ).
cnf(t246,plain,
domain_difference(antidomain(X1),X2) = multiplication(c(X1),antidomain(X2)),
inference(cp,[status(thm)],[t72,t241]) ).
cnf(t1029,plain,
multiplication(c(X1),antidomain(X2)) = domain_difference(antidomain(X1),X2),
inference(orient,[status(thm)],[t246]) ).
cnf(t47326,plain,
domain_difference(antidomain(X1),X1) = multiplication(antidomain(domain(X1)),one),
inference(step,[status(thm)],[t47325,t1029]) ).
cnf(t2025,plain,
antidomain(X1) = domain_difference(antidomain(X1),X1),
inference(cp,[status(thm)],[t2023,t72]) ).
cnf(t2099,plain,
domain_difference(antidomain(X1),X1) = antidomain(X1),
inference(orient,[status(thm)],[t2025]) ).
cnf(t47327,plain,
antidomain(X1) = multiplication(antidomain(domain(X1)),one),
inference(step,[status(thm)],[t47326,t2099]) ).
cnf(t47328,plain,
antidomain(X1) = antidomain(domain(X1)),
inference(step,[status(thm)],[t47327,t33]) ).
cnf(t47329,plain,
antidomain(X1) = c(X1),
inference(step,[status(thm)],[t47328,t96]) ).
cnf(t3453,plain,
antidomain(X1) = c(X1),
inference(orient,[status(thm)],[t47329]) ).
cnf(t47385,plain,
c(forward_diamond(X1,antidomain(X2))) = c(multiplication(X1,c(X2))),
inference(step,[status(thm)],[t1738,t3453]) ).
cnf(t47386,plain,
c(forward_diamond(X1,c(X2))) = c(multiplication(X1,c(X2))),
inference(step,[status(thm)],[t47385,t3453]) ).
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(t182,plain,
c(forward_diamond(X1,c(X2))) = forward_box(X1,X2),
inference(orient,[status(thm)],[t19]) ).
cnf(t47387,plain,
forward_box(X1,X2) = c(multiplication(X1,c(X2))),
inference(step,[status(thm)],[t47386,t182]) ).
cnf(t3498,plain,
forward_box(X1,X2) = c(multiplication(X1,c(X2))),
inference(rw,[status(thm)],[t47387]) ).
cnf(t3754,plain,
c(multiplication(X1,c(X2))) = forward_box(X1,X2),
inference(orient,[status(thm)],[t3498]) ).
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(t26,plain,
multiplication(multiplication(X1,X2),X3) = multiplication(X1,multiplication(X2,X3)),
inference(equality_encoding,[status(esa)],[c4]) ).
cnf(t41,plain,
multiplication(multiplication(X1,X2),X3) = multiplication(X1,multiplication(X2,X3)),
inference(orient,[status(thm)],[t26]) ).
cnf(t59,plain,
multiplication(antidomain(X1),multiplication(X1,X2)) = multiplication(zero,X2),
inference(cp,[status(thm)],[t41,t55]) ).
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(t70,plain,
multiplication(zero,X1) = zero,
inference(orient,[status(thm)],[t8]) ).
cnf(t47236,plain,
multiplication(antidomain(X1),multiplication(X1,X2)) = zero,
inference(step,[status(thm)],[t59,t70]) ).
cnf(t1941,plain,
multiplication(antidomain(X1),multiplication(X1,X2)) = zero,
inference(orient,[status(thm)],[t47236]) ).
cnf(t2039,plain,
zero = multiplication(antidomain(domain(X1)),X1),
inference(cp,[status(thm)],[t1941,t2023]) ).
cnf(t47240,plain,
zero = multiplication(c(X1),X1),
inference(step,[status(thm)],[t2039,t96]) ).
cnf(t2056,plain,
multiplication(c(X1),X1) = zero,
inference(orient,[status(thm)],[t47240]) ).
cnf(t3786,plain,
zero = multiplication(forward_box(X1,X2),multiplication(X1,c(X2))),
inference(cp,[status(thm)],[t2056,t3754]) ).
cnf(t23829,plain,
multiplication(forward_box(X1,X2),multiplication(X1,c(X2))) = zero,
inference(orient,[status(thm)],[t3786]) ).
cnf(t174,plain,
forward_diamond(antidomain(domain(X1)),X1) = domain(zero),
inference(cp,[status(thm)],[t172,t55]) ).
cnf(t47088,plain,
forward_diamond(c(X1),X1) = domain(zero),
inference(step,[status(thm)],[t174,t96]) ).
cnf(t47089,plain,
forward_diamond(c(X1),X1) = zero,
inference(step,[status(thm)],[t47088,t213]) ).
cnf(t291,plain,
forward_diamond(c(X1),X1) = zero,
inference(orient,[status(thm)],[t47089]) ).
cnf(t296,plain,
forward_box(c(c(X1)),X1) = c(zero),
inference(cp,[status(thm)],[t182,t291]) ).
cnf(t47130,plain,
forward_box(c(c(X1)),X1) = one,
inference(step,[status(thm)],[t296,t218]) ).
cnf(t487,plain,
forward_box(c(c(X1)),X1) = one,
inference(orient,[status(thm)],[t47130]) ).
cnf(t47376,plain,
c(antidomain(X1)) = domain(X1),
inference(step,[status(thm)],[t91,t3453]) ).
cnf(t47377,plain,
c(c(X1)) = domain(X1),
inference(step,[status(thm)],[t47376,t3453]) ).
cnf(t3491,plain,
c(c(X1)) = domain(X1),
inference(rw,[status(thm)],[t47377]) ).
cnf(t3521,plain,
c(c(X1)) = domain(X1),
inference(orient,[status(thm)],[t3491]) ).
cnf(t47428,plain,
forward_box(domain(X1),X1) = one,
inference(step,[status(thm)],[t487,t3521]) ).
cnf(t3557,plain,
forward_box(domain(X1),X1) = one,
inference(rw,[status(thm)],[t47428]) ).
cnf(t3581,plain,
forward_box(domain(X1),X1) = one,
inference(orient,[status(thm)],[t3557]) ).
cnf(t47334,plain,
c(multiplication(X1,domain(X2))) = c(forward_diamond(X1,X2)),
inference(step,[status(thm)],[t1004,t3453]) ).
cnf(t3458,plain,
c(multiplication(X1,domain(X2))) = c(forward_diamond(X1,X2)),
inference(orient,[status(thm)],[t47334]) ).
cnf(t3528,plain,
domain(multiplication(X1,domain(X2))) = c(c(forward_diamond(X1,X2))),
inference(cp,[status(thm)],[t3521,t3458]) ).
cnf(t47456,plain,
forward_diamond(X1,X2) = c(c(forward_diamond(X1,X2))),
inference(step,[status(thm)],[t3528,t172]) ).
cnf(t47457,plain,
forward_diamond(X1,X2) = domain(forward_diamond(X1,X2)),
inference(step,[status(thm)],[t47456,t3521]) ).
cnf(t3625,plain,
domain(forward_diamond(X1,X2)) = forward_diamond(X1,X2),
inference(orient,[status(thm)],[t47457]) ).
cnf(t3626,plain,
one = forward_box(forward_diamond(X1,X2),forward_diamond(X1,X2)),
inference(cp,[status(thm)],[t3581,t3625]) ).
cnf(t5782,plain,
forward_box(forward_diamond(X1,X2),forward_diamond(X1,X2)) = one,
inference(orient,[status(thm)],[t3626]) ).
cnf(t2072,plain,
multiplication(c(X1),addition(X1,X2)) = addition(zero,multiplication(c(X1),X2)),
inference(cp,[status(thm)],[t42,t2056]) ).
cnf(t47613,plain,
multiplication(c(X1),addition(X1,X2)) = multiplication(c(X1),X2),
inference(step,[status(thm)],[t2072,t222]) ).
cnf(t7045,plain,
multiplication(c(X1),addition(X1,X2)) = multiplication(c(X1),X2),
inference(orient,[status(thm)],[t47613]) ).
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(t31,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(t78,plain,
addition(antidomain(multiplication(X1,X2)),antidomain(multiplication(X1,antidomain(antidomain(X2))))) = antidomain(multiplication(X1,antidomain(antidomain(X2)))),
inference(orient,[status(thm)],[t31]) ).
cnf(t47057,plain,
addition(antidomain(multiplication(X1,X2)),antidomain(multiplication(X1,domain(X2)))) = antidomain(multiplication(X1,antidomain(antidomain(X2)))),
inference(step,[status(thm)],[t78,t91]) ).
cnf(t47058,plain,
addition(antidomain(multiplication(X1,X2)),antidomain(multiplication(X1,domain(X2)))) = antidomain(multiplication(X1,domain(X2))),
inference(step,[status(thm)],[t47057,t91]) ).
cnf(t95,plain,
addition(antidomain(multiplication(X1,X2)),antidomain(multiplication(X1,domain(X2)))) = antidomain(multiplication(X1,domain(X2))),
inference(rw,[status(thm)],[t47058]) ).
cnf(t47706,plain,
addition(c(multiplication(X1,X2)),antidomain(multiplication(X1,domain(X2)))) = antidomain(multiplication(X1,domain(X2))),
inference(step,[status(thm)],[t95,t3453]) ).
cnf(t47707,plain,
addition(c(multiplication(X1,X2)),c(multiplication(X1,domain(X2)))) = antidomain(multiplication(X1,domain(X2))),
inference(step,[status(thm)],[t47706,t3453]) ).
cnf(t3760,plain,
forward_box(X1,c(X2)) = c(multiplication(X1,domain(X2))),
inference(cp,[status(thm)],[t3754,t3521]) ).
cnf(t47467,plain,
forward_box(X1,c(X2)) = c(forward_diamond(X1,X2)),
inference(step,[status(thm)],[t3760,t3458]) ).
cnf(t3855,plain,
c(forward_diamond(X1,X2)) = forward_box(X1,c(X2)),
inference(orient,[status(thm)],[t47467]) ).
cnf(t47468,plain,
c(multiplication(X1,domain(X2))) = forward_box(X1,c(X2)),
inference(step,[status(thm)],[t3458,t3855]) ).
cnf(t3856,plain,
c(multiplication(X1,domain(X2))) = forward_box(X1,c(X2)),
inference(orient,[status(thm)],[t47468]) ).
cnf(t47708,plain,
addition(c(multiplication(X1,X2)),forward_box(X1,c(X2))) = antidomain(multiplication(X1,domain(X2))),
inference(step,[status(thm)],[t47707,t3856]) ).
cnf(t47709,plain,
addition(forward_box(X1,c(X2)),c(multiplication(X1,X2))) = antidomain(multiplication(X1,domain(X2))),
inference(step,[status(thm)],[t47708,t100]) ).
cnf(t47710,plain,
addition(forward_box(X1,c(X2)),c(multiplication(X1,X2))) = c(multiplication(X1,domain(X2))),
inference(step,[status(thm)],[t47709,t3453]) ).
cnf(t47711,plain,
addition(forward_box(X1,c(X2)),c(multiplication(X1,X2))) = forward_box(X1,c(X2)),
inference(step,[status(thm)],[t47710,t3856]) ).
cnf(t9070,plain,
addition(forward_box(X1,c(X2)),c(multiplication(X1,X2))) = forward_box(X1,c(X2)),
inference(orient,[status(thm)],[t47711]) ).
cnf(t9146,plain,
multiplication(c(forward_box(X1,c(X2))),c(multiplication(X1,X2))) = multiplication(c(forward_box(X1,c(X2))),forward_box(X1,c(X2))),
inference(cp,[status(thm)],[t7045,t9070]) ).
cnf(t47360,plain,
multiplication(c(X1),c(X2)) = domain_difference(antidomain(X1),X2),
inference(step,[status(thm)],[t1029,t3453]) ).
cnf(t47361,plain,
multiplication(c(X1),c(X2)) = domain_difference(c(X1),X2),
inference(step,[status(thm)],[t47360,t3453]) ).
cnf(t3480,plain,
multiplication(c(X1),c(X2)) = domain_difference(c(X1),X2),
inference(rw,[status(thm)],[t47361]) ).
cnf(t3977,plain,
multiplication(c(X1),c(X2)) = domain_difference(c(X1),X2),
inference(orient,[status(thm)],[t3480]) ).
cnf(t47712,plain,
domain_difference(c(forward_box(X1,c(X2))),multiplication(X1,X2)) = multiplication(c(forward_box(X1,c(X2))),forward_box(X1,c(X2))),
inference(step,[status(thm)],[t9146,t3977]) ).
cnf(t3782,plain,
domain(multiplication(X1,c(X2))) = c(forward_box(X1,X2)),
inference(cp,[status(thm)],[t3521,t3754]) ).
cnf(t247,plain,
forward_diamond(X1,antidomain(X2)) = domain(multiplication(X1,c(X2))),
inference(cp,[status(thm)],[t172,t241]) ).
cnf(t1054,plain,
domain(multiplication(X1,c(X2))) = forward_diamond(X1,antidomain(X2)),
inference(orient,[status(thm)],[t247]) ).
cnf(t47336,plain,
domain(multiplication(X1,c(X2))) = forward_diamond(X1,c(X2)),
inference(step,[status(thm)],[t1054,t3453]) ).
cnf(t3460,plain,
domain(multiplication(X1,c(X2))) = forward_diamond(X1,c(X2)),
inference(orient,[status(thm)],[t47336]) ).
cnf(t47470,plain,
forward_diamond(X1,c(X2)) = c(forward_box(X1,X2)),
inference(step,[status(thm)],[t3782,t3460]) ).
cnf(t3891,plain,
c(forward_box(X1,X2)) = forward_diamond(X1,c(X2)),
inference(orient,[status(thm)],[t47470]) ).
cnf(t47713,plain,
domain_difference(forward_diamond(X1,c(c(X2))),multiplication(X1,X2)) = multiplication(c(forward_box(X1,c(X2))),forward_box(X1,c(X2))),
inference(step,[status(thm)],[t47712,t3891]) ).
cnf(t47714,plain,
domain_difference(forward_diamond(X1,domain(X2)),multiplication(X1,X2)) = multiplication(c(forward_box(X1,c(X2))),forward_box(X1,c(X2))),
inference(step,[status(thm)],[t47713,t3521]) ).
cnf(t3551,plain,
forward_diamond(X1,c(c(X2))) = domain(multiplication(X1,domain(X2))),
inference(cp,[status(thm)],[t3460,t3521]) ).
cnf(t47458,plain,
forward_diamond(X1,domain(X2)) = domain(multiplication(X1,domain(X2))),
inference(step,[status(thm)],[t3551,t3521]) ).
cnf(t47459,plain,
forward_diamond(X1,domain(X2)) = forward_diamond(X1,X2),
inference(step,[status(thm)],[t47458,t172]) ).
cnf(t3656,plain,
forward_diamond(X1,domain(X2)) = forward_diamond(X1,X2),
inference(orient,[status(thm)],[t47459]) ).
cnf(t47715,plain,
domain_difference(forward_diamond(X1,X2),multiplication(X1,X2)) = multiplication(c(forward_box(X1,c(X2))),forward_box(X1,c(X2))),
inference(step,[status(thm)],[t47714,t3656]) ).
cnf(t47716,plain,
domain_difference(forward_diamond(X1,X2),multiplication(X1,X2)) = zero,
inference(step,[status(thm)],[t47715,t2056]) ).
cnf(t9159,plain,
domain_difference(forward_diamond(X1,X2),multiplication(X1,X2)) = zero,
inference(orient,[status(thm)],[t47716]) ).
cnf(t9174,plain,
zero = domain_difference(forward_diamond(X1,coantidomain(X1)),zero),
inference(cp,[status(thm)],[t9159,t46]) ).
cnf(t212,plain,
domain_difference(X1,zero) = multiplication(domain(X1),one),
inference(cp,[status(thm)],[t72,t209]) ).
cnf(t47083,plain,
domain_difference(X1,zero) = domain(X1),
inference(step,[status(thm)],[t212,t33]) ).
cnf(t240,plain,
domain_difference(X1,zero) = domain(X1),
inference(orient,[status(thm)],[t47083]) ).
cnf(t47717,plain,
zero = domain(forward_diamond(X1,coantidomain(X1))),
inference(step,[status(thm)],[t9174,t240]) ).
cnf(t47718,plain,
zero = forward_diamond(X1,coantidomain(X1)),
inference(step,[status(thm)],[t47717,t3625]) ).
cnf(t9225,plain,
forward_diamond(X1,coantidomain(X1)) = zero,
inference(orient,[status(thm)],[t47718]) ).
cnf(t9230,plain,
one = forward_box(forward_diamond(X1,coantidomain(X1)),zero),
inference(cp,[status(thm)],[t5782,t9225]) ).
cnf(t47372,plain,
domain(c(X1)) = c(X1),
inference(step,[status(thm)],[t241,t3453]) ).
cnf(t220,plain,
forward_box(X1,zero) = c(forward_diamond(X1,one)),
inference(cp,[status(thm)],[t182,t218]) ).
cnf(t203,plain,
forward_diamond(X1,one) = domain(multiplication(X1,one)),
inference(cp,[status(thm)],[t172,t200]) ).
cnf(t47082,plain,
forward_diamond(X1,one) = domain(X1),
inference(step,[status(thm)],[t203,t33]) ).
cnf(t235,plain,
forward_diamond(X1,one) = domain(X1),
inference(orient,[status(thm)],[t47082]) ).
cnf(t47095,plain,
forward_box(X1,zero) = c(domain(X1)),
inference(step,[status(thm)],[t220,t235]) ).
cnf(t243,plain,
c(domain(X1)) = domain(c(X1)),
inference(cp,[status(thm)],[t241,t96]) ).
cnf(t284,plain,
c(domain(X1)) = domain(c(X1)),
inference(orient,[status(thm)],[t243]) ).
cnf(t47096,plain,
forward_box(X1,zero) = domain(c(X1)),
inference(step,[status(thm)],[t47095,t284]) ).
cnf(t318,plain,
domain(c(X1)) = forward_box(X1,zero),
inference(orient,[status(thm)],[t47096]) ).
cnf(t47373,plain,
forward_box(X1,zero) = c(X1),
inference(step,[status(thm)],[t47372,t318]) ).
cnf(t3489,plain,
forward_box(X1,zero) = c(X1),
inference(rw,[status(thm)],[t47373]) ).
cnf(t3502,plain,
forward_box(X1,zero) = c(X1),
inference(orient,[status(thm)],[t3489]) ).
cnf(t47723,plain,
one = c(forward_diamond(X1,coantidomain(X1))),
inference(step,[status(thm)],[t9230,t3502]) ).
cnf(t47724,plain,
one = forward_box(X1,c(coantidomain(X1))),
inference(step,[status(thm)],[t47723,t3855]) ).
cnf(t9246,plain,
forward_box(X1,c(coantidomain(X1))) = one,
inference(orient,[status(thm)],[t47724]) ).
cnf(t23837,plain,
zero = multiplication(one,multiplication(X1,c(c(coantidomain(X1))))),
inference(cp,[status(thm)],[t23829,t9246]) ).
cnf(t48240,plain,
zero = multiplication(X1,c(c(coantidomain(X1)))),
inference(step,[status(thm)],[t23837,t34]) ).
cnf(t48241,plain,
zero = multiplication(X1,domain(coantidomain(X1))),
inference(step,[status(thm)],[t48240,t3521]) ).
cnf(t23916,plain,
multiplication(X1,domain(coantidomain(X1))) = zero,
inference(orient,[status(thm)],[t48241]) ).
cnf(t23926,plain,
multiplication(X1,addition(domain(coantidomain(X1)),X2)) = addition(zero,multiplication(X1,X2)),
inference(cp,[status(thm)],[t42,t23916]) ).
cnf(t48349,plain,
multiplication(X1,addition(domain(coantidomain(X1)),X2)) = multiplication(X1,X2),
inference(step,[status(thm)],[t23926,t222]) ).
cnf(t26741,plain,
multiplication(X1,addition(domain(coantidomain(X1)),X2)) = multiplication(X1,X2),
inference(orient,[status(thm)],[t48349]) ).
cnf(t244,plain,
one = addition(c(X1),antidomain(antidomain(X1))),
inference(cp,[status(thm)],[t114,t241]) ).
cnf(t47128,plain,
one = addition(c(X1),domain(X1)),
inference(step,[status(thm)],[t244,t91]) ).
cnf(t47129,plain,
one = addition(domain(X1),c(X1)),
inference(step,[status(thm)],[t47128,t100]) ).
cnf(t473,plain,
addition(domain(X1),c(X1)) = one,
inference(orient,[status(thm)],[t47129]) ).
cnf(t26748,plain,
multiplication(X1,c(coantidomain(X1))) = multiplication(X1,one),
inference(cp,[status(thm)],[t26741,t473]) ).
cnf(t48350,plain,
multiplication(X1,c(coantidomain(X1))) = X1,
inference(step,[status(thm)],[t26748,t33]) ).
cnf(t26803,plain,
multiplication(X1,c(coantidomain(X1))) = X1,
inference(orient,[status(thm)],[t48350]) ).
cnf(t26856,plain,
forward_box(X1,coantidomain(X1)) = c(X1),
inference(cp,[status(thm)],[t3754,t26803]) ).
cnf(t26865,plain,
forward_box(X1,coantidomain(X1)) = c(X1),
inference(orient,[status(thm)],[t26856]) ).
cnf(t47493,plain,
coantidomain(codomain(X1)) = coantidomain(X1),
inference(step,[status(thm)],[t257,t4392]) ).
cnf(t4393,plain,
coantidomain(codomain(X1)) = coantidomain(X1),
inference(orient,[status(thm)],[t47493]) ).
cnf(t26868,plain,
c(codomain(X1)) = forward_box(codomain(X1),coantidomain(X1)),
inference(cp,[status(thm)],[t26865,t4393]) ).
cnf(t48351,plain,
backward_box(X1,zero) = forward_box(codomain(X1),coantidomain(X1)),
inference(step,[status(thm)],[t26868,t451]) ).
cnf(t2042,plain,
multiplication(addition(X1,domain(X2)),X2) = addition(multiplication(X1,X2),X2),
inference(cp,[status(thm)],[t60,t2023]) ).
cnf(t47906,plain,
multiplication(addition(X1,domain(X2)),X2) = addition(X2,multiplication(X1,X2)),
inference(step,[status(thm)],[t2042,t100]) ).
cnf(t64,plain,
multiplication(addition(one,X1),X2) = addition(X2,multiplication(X1,X2)),
inference(cp,[status(thm)],[t60,t34]) ).
cnf(t1500,plain,
addition(X1,multiplication(X2,X1)) = multiplication(addition(one,X2),X1),
inference(orient,[status(thm)],[t64]) ).
cnf(t47907,plain,
multiplication(addition(X1,domain(X2)),X2) = multiplication(addition(one,X1),X2),
inference(step,[status(thm)],[t47906,t1500]) ).
cnf(t11907,plain,
multiplication(addition(X1,domain(X2)),X2) = multiplication(addition(one,X1),X2),
inference(orient,[status(thm)],[t47907]) ).
cnf(t11961,plain,
forward_box(addition(X1,domain(c(X2))),X2) = c(multiplication(addition(one,X1),c(X2))),
inference(cp,[status(thm)],[t3754,t11907]) ).
cnf(t47397,plain,
domain(c(X1)) = c(X1),
inference(step,[status(thm)],[t318,t3502]) ).
cnf(t3505,plain,
domain(c(X1)) = c(X1),
inference(orient,[status(thm)],[t47397]) ).
cnf(t47933,plain,
forward_box(addition(X1,c(X2)),X2) = c(multiplication(addition(one,X1),c(X2))),
inference(step,[status(thm)],[t11961,t3505]) ).
cnf(t47934,plain,
forward_box(addition(X1,c(X2)),X2) = forward_box(addition(one,X1),X2),
inference(step,[status(thm)],[t47933,t3754]) ).
cnf(t14302,plain,
forward_box(addition(X1,c(X2)),X2) = forward_box(addition(one,X1),X2),
inference(orient,[status(thm)],[t47934]) ).
cnf(t7063,plain,
multiplication(c(codomain(X1)),coantidomain(X1)) = multiplication(c(codomain(X1)),one),
inference(cp,[status(thm)],[t7045,t416]) ).
cnf(t47617,plain,
multiplication(backward_box(X1,zero),coantidomain(X1)) = multiplication(c(codomain(X1)),one),
inference(step,[status(thm)],[t7063,t451]) ).
cnf(t47618,plain,
multiplication(backward_box(X1,zero),coantidomain(X1)) = c(codomain(X1)),
inference(step,[status(thm)],[t47617,t33]) ).
cnf(t47619,plain,
multiplication(backward_box(X1,zero),coantidomain(X1)) = backward_box(X1,zero),
inference(step,[status(thm)],[t47618,t451]) ).
cnf(t7105,plain,
multiplication(backward_box(X1,zero),coantidomain(X1)) = backward_box(X1,zero),
inference(orient,[status(thm)],[t47619]) ).
cnf(t7116,plain,
multiplication(addition(one,backward_box(X1,zero)),coantidomain(X1)) = addition(coantidomain(X1),backward_box(X1,zero)),
inference(cp,[status(thm)],[t1500,t7105]) ).
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(t23,plain,
addition(addition(X1,X2),X3) = addition(X1,addition(X2,X3)),
inference(equality_encoding,[status(esa)],[c1]) ).
cnf(t105,plain,
addition(addition(X1,X2),X3) = addition(X1,addition(X2,X3)),
inference(orient,[status(thm)],[t23]) ).
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(t35,plain,
addition(X1,X1) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t108,plain,
addition(X1,addition(X1,X2)) = addition(X1,X2),
inference(cp,[status(thm)],[t105,t35]) ).
cnf(t610,plain,
addition(X1,addition(X1,X2)) = addition(X1,X2),
inference(orient,[status(thm)],[t108]) ).
cnf(t613,plain,
addition(domain(X1),antidomain(X1)) = addition(domain(X1),one),
inference(cp,[status(thm)],[t610,t114]) ).
cnf(t47144,plain,
one = addition(domain(X1),one),
inference(step,[status(thm)],[t613,t114]) ).
cnf(t47145,plain,
one = addition(one,domain(X1)),
inference(step,[status(thm)],[t47144,t100]) ).
cnf(t626,plain,
addition(one,domain(X1)) = one,
inference(orient,[status(thm)],[t47145]) ).
cnf(t632,plain,
one = addition(one,c(X1)),
inference(cp,[status(thm)],[t626,t241]) ).
cnf(t637,plain,
addition(one,c(X1)) = one,
inference(orient,[status(thm)],[t632]) ).
cnf(t639,plain,
one = addition(one,backward_box(X1,zero)),
inference(cp,[status(thm)],[t637,t451]) ).
cnf(t702,plain,
addition(one,backward_box(X1,zero)) = one,
inference(orient,[status(thm)],[t639]) ).
cnf(t47620,plain,
multiplication(one,coantidomain(X1)) = addition(coantidomain(X1),backward_box(X1,zero)),
inference(step,[status(thm)],[t7116,t702]) ).
cnf(t47621,plain,
coantidomain(X1) = addition(coantidomain(X1),backward_box(X1,zero)),
inference(step,[status(thm)],[t47620,t34]) ).
cnf(t7130,plain,
addition(coantidomain(X1),backward_box(X1,zero)) = coantidomain(X1),
inference(orient,[status(thm)],[t47621]) ).
cnf(t7133,plain,
coantidomain(coantidomain(X1)) = addition(codomain(X1),backward_box(coantidomain(X1),zero)),
inference(cp,[status(thm)],[t7130,t134]) ).
cnf(t47630,plain,
codomain(X1) = addition(codomain(X1),backward_box(coantidomain(X1),zero)),
inference(step,[status(thm)],[t7133,t134]) ).
cnf(t47631,plain,
codomain(X1) = addition(codomain(X1),c(coantidomain(X1))),
inference(step,[status(thm)],[t47630,t4436]) ).
cnf(t7289,plain,
addition(codomain(X1),c(coantidomain(X1))) = codomain(X1),
inference(orient,[status(thm)],[t47631]) ).
cnf(t14305,plain,
forward_box(addition(one,codomain(X1)),coantidomain(X1)) = forward_box(codomain(X1),coantidomain(X1)),
inference(cp,[status(thm)],[t14302,t7289]) ).
cnf(t612,plain,
addition(codomain(X1),coantidomain(X1)) = addition(codomain(X1),one),
inference(cp,[status(thm)],[t610,t416]) ).
cnf(t47142,plain,
one = addition(codomain(X1),one),
inference(step,[status(thm)],[t612,t416]) ).
cnf(t47143,plain,
one = addition(one,codomain(X1)),
inference(step,[status(thm)],[t47142,t100]) ).
cnf(t619,plain,
addition(one,codomain(X1)) = one,
inference(orient,[status(thm)],[t47143]) ).
cnf(t47935,plain,
forward_box(one,coantidomain(X1)) = forward_box(codomain(X1),coantidomain(X1)),
inference(step,[status(thm)],[t14305,t619]) ).
cnf(t242,plain,
c(antidomain(X1)) = domain(domain(X1)),
inference(cp,[status(thm)],[t241,t91]) ).
cnf(t176,plain,
forward_diamond(one,X1) = domain(domain(X1)),
inference(cp,[status(thm)],[t172,t34]) ).
cnf(t260,plain,
domain(domain(X1)) = forward_diamond(one,X1),
inference(orient,[status(thm)],[t176]) ).
cnf(t47087,plain,
c(antidomain(X1)) = forward_diamond(one,X1),
inference(step,[status(thm)],[t242,t260]) ).
cnf(t277,plain,
c(antidomain(X1)) = forward_diamond(one,X1),
inference(orient,[status(thm)],[t47087]) ).
cnf(t97,plain,
domain(domain(X1)) = antidomain(c(X1)),
inference(cp,[status(thm)],[t91,t96]) ).
cnf(t249,plain,
antidomain(c(X1)) = domain(domain(X1)),
inference(orient,[status(thm)],[t97]) ).
cnf(t47085,plain,
antidomain(c(X1)) = forward_diamond(one,X1),
inference(step,[status(thm)],[t249,t260]) ).
cnf(t261,plain,
antidomain(c(X1)) = forward_diamond(one,X1),
inference(orient,[status(thm)],[t47085]) ).
cnf(t278,plain,
forward_diamond(one,c(X1)) = c(forward_diamond(one,X1)),
inference(cp,[status(thm)],[t277,t261]) ).
cnf(t504,plain,
c(forward_diamond(one,X1)) = forward_diamond(one,c(X1)),
inference(orient,[status(thm)],[t278]) ).
cnf(t505,plain,
forward_diamond(one,c(c(X1))) = forward_box(one,X1),
inference(cp,[status(thm)],[t504,t182]) ).
cnf(t767,plain,
forward_diamond(one,c(c(X1))) = forward_box(one,X1),
inference(orient,[status(thm)],[t505]) ).
cnf(t47426,plain,
forward_diamond(one,domain(X1)) = forward_box(one,X1),
inference(step,[status(thm)],[t767,t3521]) ).
cnf(t252,plain,
c(c(X1)) = domain(domain(domain(X1))),
inference(cp,[status(thm)],[t241,t249]) ).
cnf(t47100,plain,
c(c(X1)) = forward_diamond(one,domain(X1)),
inference(step,[status(thm)],[t252,t260]) ).
cnf(t337,plain,
forward_diamond(one,domain(X1)) = c(c(X1)),
inference(orient,[status(thm)],[t47100]) ).
cnf(t47420,plain,
forward_diamond(one,domain(X1)) = domain(X1),
inference(step,[status(thm)],[t337,t3521]) ).
cnf(t3522,plain,
forward_diamond(one,domain(X1)) = domain(X1),
inference(orient,[status(thm)],[t47420]) ).
cnf(t47427,plain,
domain(X1) = forward_box(one,X1),
inference(step,[status(thm)],[t47426,t3522]) ).
cnf(t3556,plain,
domain(X1) = forward_box(one,X1),
inference(rw,[status(thm)],[t47427]) ).
cnf(t3570,plain,
forward_box(one,X1) = domain(X1),
inference(orient,[status(thm)],[t3556]) ).
cnf(t47936,plain,
domain(coantidomain(X1)) = forward_box(codomain(X1),coantidomain(X1)),
inference(step,[status(thm)],[t47935,t3570]) ).
cnf(t14325,plain,
forward_box(codomain(X1),coantidomain(X1)) = domain(coantidomain(X1)),
inference(orient,[status(thm)],[t47936]) ).
cnf(t48352,plain,
backward_box(X1,zero) = domain(coantidomain(X1)),
inference(step,[status(thm)],[t48351,t14325]) ).
cnf(t26879,plain,
domain(coantidomain(X1)) = backward_box(X1,zero),
inference(orient,[status(thm)],[t48352]) ).
cnf(t26914,plain,
addition(coantidomain(X1),domain(coantidomain(X1))) = multiplication(backward_box(X1,zero),addition(one,coantidomain(X1))),
inference(cp,[status(thm)],[t6670,t26879]) ).
cnf(t48384,plain,
addition(coantidomain(X1),backward_box(X1,zero)) = multiplication(backward_box(X1,zero),addition(one,coantidomain(X1))),
inference(step,[status(thm)],[t26914,t26879]) ).
cnf(t48385,plain,
coantidomain(X1) = multiplication(backward_box(X1,zero),addition(one,coantidomain(X1))),
inference(step,[status(thm)],[t48384,t7130]) ).
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(t25,plain,
ifeq(leq(X1,X2),true,addition(X1,X2),X2) = X2,
inference(equality_encoding,[status(esa)],[c11]) ).
cnf(t38,plain,
ifeq(leq(X1,X2),true,addition(X1,X2),X2) = X2,
inference(orient,[status(thm)],[t25]) ).
cnf(c12,plain,
( addition(X0,X1) != X1
| leq(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f11_sk]) ).
cnf(t24,plain,
ifeq(addition(X1,X2),X2,leq(X1,X2),true) = true,
inference(equality_encoding,[status(esa)],[c12]) ).
cnf(t163,plain,
ifeq(addition(X1,X2),X2,leq(X1,X2),true) = true,
inference(orient,[status(thm)],[t24]) ).
cnf(t618,plain,
true = ifeq(addition(X1,X2),addition(X1,X2),leq(X1,addition(X1,X2)),true),
inference(cp,[status(thm)],[t163,t610]) ).
cnf(t15,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t37,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t15]) ).
cnf(t47146,plain,
true = leq(X1,addition(X1,X2)),
inference(step,[status(thm)],[t618,t37]) ).
cnf(t649,plain,
leq(X1,addition(X1,X2)) = true,
inference(orient,[status(thm)],[t47146]) ).
cnf(t657,plain,
true = leq(X1,addition(X2,X1)),
inference(cp,[status(thm)],[t649,t100]) ).
cnf(t714,plain,
leq(X1,addition(X2,X1)) = true,
inference(orient,[status(thm)],[t657]) ).
cnf(t720,plain,
true = leq(coantidomain(X1),one),
inference(cp,[status(thm)],[t714,t416]) ).
cnf(t727,plain,
leq(coantidomain(X1),one) = true,
inference(orient,[status(thm)],[t720]) ).
cnf(t729,plain,
one = ifeq(true,true,addition(coantidomain(X1),one),one),
inference(cp,[status(thm)],[t38,t727]) ).
cnf(t47147,plain,
one = addition(coantidomain(X1),one),
inference(step,[status(thm)],[t729,t37]) ).
cnf(t47148,plain,
one = addition(one,coantidomain(X1)),
inference(step,[status(thm)],[t47147,t100]) ).
cnf(t737,plain,
addition(one,coantidomain(X1)) = one,
inference(orient,[status(thm)],[t47148]) ).
cnf(t48386,plain,
coantidomain(X1) = multiplication(backward_box(X1,zero),one),
inference(step,[status(thm)],[t48385,t737]) ).
cnf(t48387,plain,
coantidomain(X1) = backward_box(X1,zero),
inference(step,[status(thm)],[t48386,t33]) ).
cnf(t27112,plain,
backward_box(X1,zero) = coantidomain(X1),
inference(orient,[status(thm)],[t48387]) ).
cnf(t48438,plain,
coantidomain(coantidomain(X1)) = c(coantidomain(X1)),
inference(step,[status(thm)],[t4436,t27112]) ).
cnf(t48439,plain,
codomain(X1) = c(coantidomain(X1)),
inference(step,[status(thm)],[t48438,t134]) ).
cnf(t27163,plain,
codomain(X1) = c(coantidomain(X1)),
inference(rw,[status(thm)],[t48439]) ).
cnf(t27181,plain,
c(coantidomain(X1)) = codomain(X1),
inference(orient,[status(thm)],[t27163]) ).
cnf(t3764,plain,
forward_box(X1,codomain(X2)) = c(multiplication(X1,backward_box(X2,zero))),
inference(cp,[status(thm)],[t3754,t451]) ).
cnf(t8227,plain,
c(multiplication(X1,backward_box(X2,zero))) = forward_box(X1,codomain(X2)),
inference(orient,[status(thm)],[t3764]) ).
cnf(t49,plain,
multiplication(X1,addition(coantidomain(X1),X2)) = addition(zero,multiplication(X1,X2)),
inference(cp,[status(thm)],[t42,t46]) ).
cnf(t47256,plain,
multiplication(X1,addition(coantidomain(X1),X2)) = multiplication(X1,X2),
inference(step,[status(thm)],[t49,t222]) ).
cnf(t2440,plain,
multiplication(X1,addition(coantidomain(X1),X2)) = multiplication(X1,X2),
inference(orient,[status(thm)],[t47256]) ).
cnf(t7148,plain,
multiplication(X1,backward_box(X1,zero)) = multiplication(X1,coantidomain(X1)),
inference(cp,[status(thm)],[t2440,t7130]) ).
cnf(t47622,plain,
multiplication(X1,backward_box(X1,zero)) = zero,
inference(step,[status(thm)],[t7148,t46]) ).
cnf(t7150,plain,
multiplication(X1,backward_box(X1,zero)) = zero,
inference(orient,[status(thm)],[t47622]) ).
cnf(t8228,plain,
forward_box(X1,codomain(X1)) = c(zero),
inference(cp,[status(thm)],[t8227,t7150]) ).
cnf(t47675,plain,
forward_box(X1,codomain(X1)) = one,
inference(step,[status(thm)],[t8228,t218]) ).
cnf(t8335,plain,
forward_box(X1,codomain(X1)) = one,
inference(orient,[status(thm)],[t47675]) ).
cnf(t8336,plain,
one = forward_box(multiplication(codomain(X1),X2),backward_diamond(X2,X1)),
inference(cp,[status(thm)],[t8335,t188]) ).
cnf(t43531,plain,
forward_box(multiplication(codomain(X1),X2),backward_diamond(X2,X1)) = one,
inference(orient,[status(thm)],[t8336]) ).
cnf(t191,plain,
backward_diamond(coantidomain(codomain(X1)),X1) = codomain(zero),
inference(cp,[status(thm)],[t188,t46]) ).
cnf(t47136,plain,
backward_diamond(codomain(coantidomain(X1)),X1) = codomain(zero),
inference(step,[status(thm)],[t191,t257]) ).
cnf(t430,plain,
codomain(coantidomain(one)) = coantidomain(one),
inference(cp,[status(thm)],[t257,t426]) ).
cnf(t47109,plain,
codomain(zero) = coantidomain(one),
inference(step,[status(thm)],[t430,t194]) ).
cnf(t47110,plain,
codomain(zero) = zero,
inference(step,[status(thm)],[t47109,t194]) ).
cnf(t432,plain,
codomain(zero) = zero,
inference(orient,[status(thm)],[t47110]) ).
cnf(t47137,plain,
backward_diamond(codomain(coantidomain(X1)),X1) = zero,
inference(step,[status(thm)],[t47136,t432]) ).
cnf(t575,plain,
backward_diamond(codomain(coantidomain(X1)),X1) = zero,
inference(orient,[status(thm)],[t47137]) ).
cnf(t578,plain,
zero = backward_diamond(codomain(codomain(X1)),coantidomain(X1)),
inference(cp,[status(thm)],[t575,t134]) ).
cnf(t47161,plain,
zero = backward_diamond(backward_diamond(one,X1),coantidomain(X1)),
inference(step,[status(thm)],[t578,t271]) ).
cnf(t934,plain,
backward_diamond(backward_diamond(one,X1),coantidomain(X1)) = zero,
inference(orient,[status(thm)],[t47161]) ).
cnf(t47505,plain,
backward_diamond(codomain(X1),coantidomain(X1)) = zero,
inference(step,[status(thm)],[t934,t4411]) ).
cnf(t4419,plain,
backward_diamond(codomain(X1),coantidomain(X1)) = zero,
inference(rw,[status(thm)],[t47505]) ).
cnf(t4484,plain,
backward_diamond(codomain(X1),coantidomain(X1)) = zero,
inference(orient,[status(thm)],[t4419]) ).
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(t32,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(t119,plain,
addition(coantidomain(multiplication(X1,X2)),coantidomain(multiplication(coantidomain(coantidomain(X1)),X2))) = coantidomain(multiplication(coantidomain(coantidomain(X1)),X2)),
inference(orient,[status(thm)],[t32]) ).
cnf(t47064,plain,
addition(coantidomain(multiplication(X1,X2)),coantidomain(multiplication(codomain(X1),X2))) = coantidomain(multiplication(coantidomain(coantidomain(X1)),X2)),
inference(step,[status(thm)],[t119,t134]) ).
cnf(t47065,plain,
addition(coantidomain(multiplication(X1,X2)),coantidomain(multiplication(codomain(X1),X2))) = coantidomain(multiplication(codomain(X1),X2)),
inference(step,[status(thm)],[t47064,t134]) ).
cnf(t138,plain,
addition(coantidomain(multiplication(X1,X2)),coantidomain(multiplication(codomain(X1),X2))) = coantidomain(multiplication(codomain(X1),X2)),
inference(rw,[status(thm)],[t47065]) ).
cnf(t4407,plain,
backward_diamond(X1,coantidomain(X2)) = codomain(multiplication(coantidomain(X2),X1)),
inference(cp,[status(thm)],[t188,t4392]) ).
cnf(t4588,plain,
codomain(multiplication(coantidomain(X1),X2)) = backward_diamond(X2,coantidomain(X1)),
inference(orient,[status(thm)],[t4407]) ).
cnf(t4611,plain,
coantidomain(multiplication(coantidomain(X1),X2)) = coantidomain(backward_diamond(X2,coantidomain(X1))),
inference(cp,[status(thm)],[t4393,t4588]) ).
cnf(t4658,plain,
coantidomain(backward_diamond(X1,coantidomain(X2))) = coantidomain(multiplication(coantidomain(X2),X1)),
inference(orient,[status(thm)],[t4611]) ).
cnf(t4659,plain,
coantidomain(multiplication(coantidomain(coantidomain(X1)),X2)) = coantidomain(backward_diamond(X2,codomain(X1))),
inference(cp,[status(thm)],[t4658,t134]) ).
cnf(t47524,plain,
coantidomain(multiplication(codomain(X1),X2)) = coantidomain(backward_diamond(X2,codomain(X1))),
inference(step,[status(thm)],[t4659,t134]) ).
cnf(t4594,plain,
backward_diamond(X1,coantidomain(coantidomain(X2))) = codomain(multiplication(codomain(X2),X1)),
inference(cp,[status(thm)],[t4588,t134]) ).
cnf(t47518,plain,
backward_diamond(X1,codomain(X2)) = codomain(multiplication(codomain(X2),X1)),
inference(step,[status(thm)],[t4594,t134]) ).
cnf(t47519,plain,
backward_diamond(X1,codomain(X2)) = backward_diamond(X1,X2),
inference(step,[status(thm)],[t47518,t188]) ).
cnf(t4617,plain,
backward_diamond(X1,codomain(X2)) = backward_diamond(X1,X2),
inference(orient,[status(thm)],[t47519]) ).
cnf(t47525,plain,
coantidomain(multiplication(codomain(X1),X2)) = coantidomain(backward_diamond(X2,X1)),
inference(step,[status(thm)],[t47524,t4617]) ).
cnf(t4671,plain,
coantidomain(multiplication(codomain(X1),X2)) = coantidomain(backward_diamond(X2,X1)),
inference(orient,[status(thm)],[t47525]) ).
cnf(t48170,plain,
addition(coantidomain(multiplication(X1,X2)),coantidomain(backward_diamond(X2,X1))) = coantidomain(multiplication(codomain(X1),X2)),
inference(step,[status(thm)],[t138,t4671]) ).
cnf(t48171,plain,
addition(coantidomain(multiplication(X1,X2)),coantidomain(backward_diamond(X2,X1))) = coantidomain(backward_diamond(X2,X1)),
inference(step,[status(thm)],[t48170,t4671]) ).
cnf(t19949,plain,
addition(coantidomain(multiplication(X1,X2)),coantidomain(backward_diamond(X2,X1))) = coantidomain(backward_diamond(X2,X1)),
inference(orient,[status(thm)],[t48171]) ).
cnf(t20000,plain,
coantidomain(backward_diamond(X1,c(X1))) = addition(coantidomain(zero),coantidomain(backward_diamond(X1,c(X1)))),
inference(cp,[status(thm)],[t19949,t2056]) ).
cnf(t195,plain,
codomain(one) = coantidomain(zero),
inference(cp,[status(thm)],[t134,t194]) ).
cnf(t207,plain,
coantidomain(zero) = codomain(one),
inference(orient,[status(thm)],[t195]) ).
cnf(t47107,plain,
coantidomain(zero) = one,
inference(step,[status(thm)],[t207,t426]) ).
cnf(t427,plain,
coantidomain(zero) = one,
inference(orient,[status(thm)],[t47107]) ).
cnf(t48172,plain,
coantidomain(backward_diamond(X1,c(X1))) = addition(one,coantidomain(backward_diamond(X1,c(X1)))),
inference(step,[status(thm)],[t20000,t427]) ).
cnf(t48173,plain,
coantidomain(backward_diamond(X1,c(X1))) = one,
inference(step,[status(thm)],[t48172,t737]) ).
cnf(t20054,plain,
coantidomain(backward_diamond(X1,c(X1))) = one,
inference(orient,[status(thm)],[t48173]) ).
cnf(t20077,plain,
zero = backward_diamond(codomain(backward_diamond(X1,c(X1))),one),
inference(cp,[status(thm)],[t4484,t20054]) ).
cnf(t48178,plain,
zero = codomain(codomain(backward_diamond(X1,c(X1)))),
inference(step,[status(thm)],[t20077,t449]) ).
cnf(t47500,plain,
codomain(codomain(X1)) = codomain(X1),
inference(step,[status(thm)],[t271,t4411]) ).
cnf(t4412,plain,
codomain(codomain(X1)) = codomain(X1),
inference(orient,[status(thm)],[t47500]) ).
cnf(t48179,plain,
zero = codomain(backward_diamond(X1,c(X1))),
inference(step,[status(thm)],[t48178,t4412]) ).
cnf(t4610,plain,
codomain(multiplication(coantidomain(X1),X2)) = codomain(backward_diamond(X2,coantidomain(X1))),
inference(cp,[status(thm)],[t4412,t4588]) ).
cnf(t47520,plain,
backward_diamond(X2,coantidomain(X1)) = codomain(backward_diamond(X2,coantidomain(X1))),
inference(step,[status(thm)],[t4610,t4588]) ).
cnf(t4628,plain,
codomain(backward_diamond(X1,coantidomain(X2))) = backward_diamond(X1,coantidomain(X2)),
inference(orient,[status(thm)],[t47520]) ).
cnf(t4629,plain,
backward_diamond(X1,coantidomain(coantidomain(X2))) = codomain(backward_diamond(X1,codomain(X2))),
inference(cp,[status(thm)],[t4628,t134]) ).
cnf(t47521,plain,
backward_diamond(X1,codomain(X2)) = codomain(backward_diamond(X1,codomain(X2))),
inference(step,[status(thm)],[t4629,t134]) ).
cnf(t47522,plain,
backward_diamond(X1,X2) = codomain(backward_diamond(X1,codomain(X2))),
inference(step,[status(thm)],[t47521,t4617]) ).
cnf(t47523,plain,
backward_diamond(X1,X2) = codomain(backward_diamond(X1,X2)),
inference(step,[status(thm)],[t47522,t4617]) ).
cnf(t4643,plain,
codomain(backward_diamond(X1,X2)) = backward_diamond(X1,X2),
inference(orient,[status(thm)],[t47523]) ).
cnf(t48180,plain,
zero = backward_diamond(X1,c(X1)),
inference(step,[status(thm)],[t48179,t4643]) ).
cnf(t20115,plain,
backward_diamond(X1,c(X1)) = zero,
inference(orient,[status(thm)],[t48180]) ).
cnf(t43550,plain,
one = forward_box(multiplication(codomain(c(X1)),X1),zero),
inference(cp,[status(thm)],[t43531,t20115]) ).
cnf(t48837,plain,
one = c(multiplication(codomain(c(X1)),X1)),
inference(step,[status(thm)],[t43550,t3502]) ).
cnf(t43680,plain,
c(multiplication(codomain(c(X1)),X1)) = one,
inference(orient,[status(thm)],[t48837]) ).
cnf(t43731,plain,
zero = multiplication(one,multiplication(codomain(c(X1)),X1)),
inference(cp,[status(thm)],[t2056,t43680]) ).
cnf(t48838,plain,
zero = multiplication(codomain(c(X1)),X1),
inference(step,[status(thm)],[t43731,t34]) ).
cnf(t43865,plain,
multiplication(codomain(c(X1)),X1) = zero,
inference(orient,[status(thm)],[t48838]) ).
cnf(t43877,plain,
multiplication(addition(codomain(c(X1)),X2),X1) = addition(zero,multiplication(X2,X1)),
inference(cp,[status(thm)],[t60,t43865]) ).
cnf(t48960,plain,
multiplication(addition(codomain(c(X1)),X2),X1) = multiplication(X2,X1),
inference(step,[status(thm)],[t43877,t222]) ).
cnf(t46646,plain,
multiplication(addition(codomain(c(X1)),X2),X1) = multiplication(X2,X1),
inference(orient,[status(thm)],[t48960]) ).
cnf(t46651,plain,
multiplication(coantidomain(c(X1)),X1) = multiplication(one,X1),
inference(cp,[status(thm)],[t46646,t416]) ).
cnf(t4416,plain,
backward_box(one,X1) = c(codomain(c(X1))),
inference(cp,[status(thm)],[t184,t4411]) ).
cnf(t47511,plain,
backward_box(one,X1) = backward_box(c(X1),zero),
inference(step,[status(thm)],[t4416,t451]) ).
cnf(t4438,plain,
backward_box(c(X1),zero) = backward_box(one,X1),
inference(orient,[status(thm)],[t47511]) ).
cnf(t48437,plain,
coantidomain(c(X1)) = backward_box(one,X1),
inference(step,[status(thm)],[t4438,t27112]) ).
cnf(t27162,plain,
coantidomain(c(X1)) = backward_box(one,X1),
inference(rw,[status(thm)],[t48437]) ).
cnf(t27450,plain,
coantidomain(c(X1)) = backward_box(one,X1),
inference(orient,[status(thm)],[t27162]) ).
cnf(t48961,plain,
multiplication(backward_box(one,X1),X1) = multiplication(one,X1),
inference(step,[status(thm)],[t46651,t27450]) ).
cnf(t48962,plain,
multiplication(backward_box(one,X1),X1) = X1,
inference(step,[status(thm)],[t48961,t34]) ).
cnf(t46745,plain,
multiplication(backward_box(one,X1),X1) = X1,
inference(orient,[status(thm)],[t48962]) ).
cnf(t3986,plain,
domain_difference(c(backward_diamond(X1,c(X2))),X3) = multiplication(backward_box(X1,X2),c(X3)),
inference(cp,[status(thm)],[t3977,t184]) ).
cnf(t47919,plain,
domain_difference(backward_box(X1,X2),X3) = multiplication(backward_box(X1,X2),c(X3)),
inference(step,[status(thm)],[t3986,t184]) ).
cnf(t12588,plain,
multiplication(backward_box(X1,X2),c(X3)) = domain_difference(backward_box(X1,X2),X3),
inference(orient,[status(thm)],[t47919]) ).
cnf(t46746,plain,
c(X1) = domain_difference(backward_box(one,c(X1)),X1),
inference(cp,[status(thm)],[t46745,t12588]) ).
cnf(t3553,plain,
backward_box(X1,c(X2)) = c(backward_diamond(X1,domain(X2))),
inference(cp,[status(thm)],[t184,t3521]) ).
cnf(t4082,plain,
c(backward_diamond(X1,domain(X2))) = backward_box(X1,c(X2)),
inference(orient,[status(thm)],[t3553]) ).
cnf(t4414,plain,
backward_box(one,c(X1)) = c(codomain(domain(X1))),
inference(cp,[status(thm)],[t4082,t4411]) ).
cnf(t47514,plain,
backward_box(one,c(X1)) = backward_box(domain(X1),zero),
inference(step,[status(thm)],[t4414,t451]) ).
cnf(t4490,plain,
backward_box(domain(X1),zero) = backward_box(one,c(X1)),
inference(orient,[status(thm)],[t47514]) ).
cnf(t48436,plain,
coantidomain(domain(X1)) = backward_box(one,c(X1)),
inference(step,[status(thm)],[t4490,t27112]) ).
cnf(t27161,plain,
coantidomain(domain(X1)) = backward_box(one,c(X1)),
inference(rw,[status(thm)],[t48436]) ).
cnf(t27571,plain,
backward_box(one,c(X1)) = coantidomain(domain(X1)),
inference(orient,[status(thm)],[t27161]) ).
cnf(t48963,plain,
c(X1) = domain_difference(coantidomain(domain(X1)),X1),
inference(step,[status(thm)],[t46746,t27571]) ).
cnf(t2073,plain,
multiplication(c(X1),addition(X2,X1)) = addition(multiplication(c(X1),X2),zero),
inference(cp,[status(thm)],[t42,t2056]) ).
cnf(t47653,plain,
multiplication(c(X1),addition(X2,X1)) = multiplication(c(X1),X2),
inference(step,[status(thm)],[t2073,t36]) ).
cnf(t7618,plain,
multiplication(c(X1),addition(X2,X1)) = multiplication(c(X1),X2),
inference(orient,[status(thm)],[t47653]) ).
cnf(t486,plain,
addition(domain(X1),addition(c(X1),X2)) = addition(one,X2),
inference(cp,[status(thm)],[t105,t473]) ).
cnf(t14452,plain,
addition(domain(X1),addition(c(X1),X2)) = addition(one,X2),
inference(orient,[status(thm)],[t486]) ).
cnf(t1889,plain,
multiplication(addition(one,X1),codomain(X1)) = addition(codomain(X1),X1),
inference(cp,[status(thm)],[t1500,t1884]) ).
cnf(t47595,plain,
multiplication(addition(one,X1),codomain(X1)) = addition(X1,codomain(X1)),
inference(step,[status(thm)],[t1889,t100]) ).
cnf(t6537,plain,
multiplication(addition(one,X1),codomain(X1)) = addition(X1,codomain(X1)),
inference(orient,[status(thm)],[t47595]) ).
cnf(t6551,plain,
addition(c(X1),codomain(c(X1))) = multiplication(one,codomain(c(X1))),
inference(cp,[status(thm)],[t6537,t637]) ).
cnf(t47596,plain,
addition(c(X1),codomain(c(X1))) = codomain(c(X1)),
inference(step,[status(thm)],[t6551,t34]) ).
cnf(t6571,plain,
addition(c(X1),codomain(c(X1))) = codomain(c(X1)),
inference(orient,[status(thm)],[t47596]) ).
cnf(t14468,plain,
addition(one,codomain(c(X1))) = addition(domain(X1),codomain(c(X1))),
inference(cp,[status(thm)],[t14452,t6571]) ).
cnf(t47945,plain,
one = addition(domain(X1),codomain(c(X1))),
inference(step,[status(thm)],[t14468,t619]) ).
cnf(t14508,plain,
addition(domain(X1),codomain(c(X1))) = one,
inference(orient,[status(thm)],[t47945]) ).
cnf(t14520,plain,
one = addition(c(X1),codomain(c(c(X1)))),
inference(cp,[status(thm)],[t14508,t3505]) ).
cnf(t47946,plain,
one = addition(c(X1),codomain(domain(X1))),
inference(step,[status(thm)],[t14520,t3521]) ).
cnf(t14553,plain,
addition(c(X1),codomain(domain(X1))) = one,
inference(orient,[status(thm)],[t47946]) ).
cnf(t14584,plain,
multiplication(c(codomain(domain(X1))),c(X1)) = multiplication(c(codomain(domain(X1))),one),
inference(cp,[status(thm)],[t7618,t14553]) ).
cnf(t47956,plain,
domain_difference(c(codomain(domain(X1))),X1) = multiplication(c(codomain(domain(X1))),one),
inference(step,[status(thm)],[t14584,t3977]) ).
cnf(t47957,plain,
domain_difference(backward_box(domain(X1),zero),X1) = multiplication(c(codomain(domain(X1))),one),
inference(step,[status(thm)],[t47956,t451]) ).
cnf(t47958,plain,
domain_difference(backward_box(one,c(X1)),X1) = multiplication(c(codomain(domain(X1))),one),
inference(step,[status(thm)],[t47957,t4490]) ).
cnf(t47959,plain,
domain_difference(backward_box(one,c(X1)),X1) = c(codomain(domain(X1))),
inference(step,[status(thm)],[t47958,t33]) ).
cnf(t47960,plain,
domain_difference(backward_box(one,c(X1)),X1) = backward_box(domain(X1),zero),
inference(step,[status(thm)],[t47959,t451]) ).
cnf(t47961,plain,
domain_difference(backward_box(one,c(X1)),X1) = backward_box(one,c(X1)),
inference(step,[status(thm)],[t47960,t4490]) ).
cnf(t14812,plain,
domain_difference(backward_box(one,c(X1)),X1) = backward_box(one,c(X1)),
inference(orient,[status(thm)],[t47961]) ).
cnf(t14825,plain,
backward_box(one,c(c(X1))) = domain_difference(backward_box(one,domain(X1)),c(X1)),
inference(cp,[status(thm)],[t14812,t3521]) ).
cnf(t47962,plain,
backward_box(one,domain(X1)) = domain_difference(backward_box(one,domain(X1)),c(X1)),
inference(step,[status(thm)],[t14825,t3521]) ).
cnf(t453,plain,
backward_box(codomain(X1),zero) = c(backward_diamond(one,X1)),
inference(cp,[status(thm)],[t451,t271]) ).
cnf(t548,plain,
c(backward_diamond(one,X1)) = backward_box(codomain(X1),zero),
inference(orient,[status(thm)],[t453]) ).
cnf(t549,plain,
backward_box(codomain(c(X1)),zero) = backward_box(one,X1),
inference(cp,[status(thm)],[t548,t184]) ).
cnf(t792,plain,
backward_box(codomain(c(X1)),zero) = backward_box(one,X1),
inference(orient,[status(thm)],[t549]) ).
cnf(t3552,plain,
backward_box(one,c(X1)) = backward_box(codomain(domain(X1)),zero),
inference(cp,[status(thm)],[t792,t3521]) ).
cnf(t4064,plain,
backward_box(codomain(domain(X1)),zero) = backward_box(one,c(X1)),
inference(orient,[status(thm)],[t3552]) ).
cnf(t4069,plain,
backward_box(one,c(c(X1))) = backward_box(codomain(c(X1)),zero),
inference(cp,[status(thm)],[t4064,t3505]) ).
cnf(t47478,plain,
backward_box(one,domain(X1)) = backward_box(codomain(c(X1)),zero),
inference(step,[status(thm)],[t4069,t3521]) ).
cnf(t47479,plain,
backward_box(one,domain(X1)) = backward_box(one,X1),
inference(step,[status(thm)],[t47478,t792]) ).
cnf(t4075,plain,
backward_box(one,domain(X1)) = backward_box(one,X1),
inference(orient,[status(thm)],[t47479]) ).
cnf(t47963,plain,
backward_box(one,X1) = domain_difference(backward_box(one,domain(X1)),c(X1)),
inference(step,[status(thm)],[t47962,t4075]) ).
cnf(t47964,plain,
backward_box(one,X1) = domain_difference(backward_box(one,X1),c(X1)),
inference(step,[status(thm)],[t47963,t4075]) ).
cnf(t14843,plain,
domain_difference(backward_box(one,X1),c(X1)) = backward_box(one,X1),
inference(orient,[status(thm)],[t47964]) ).
cnf(t27585,plain,
backward_box(one,c(X1)) = domain_difference(coantidomain(domain(X1)),c(c(X1))),
inference(cp,[status(thm)],[t14843,t27571]) ).
cnf(t48545,plain,
coantidomain(domain(X1)) = domain_difference(coantidomain(domain(X1)),c(c(X1))),
inference(step,[status(thm)],[t27585,t27571]) ).
cnf(t48546,plain,
coantidomain(domain(X1)) = domain_difference(coantidomain(domain(X1)),domain(X1)),
inference(step,[status(thm)],[t48545,t3521]) ).
cnf(t47378,plain,
multiplication(domain(X1),c(X2)) = domain_difference(X1,X2),
inference(step,[status(thm)],[t72,t3453]) ).
cnf(t98,plain,
domain_difference(X1,domain(X2)) = multiplication(domain(X1),c(X2)),
inference(cp,[status(thm)],[t72,t96]) ).
cnf(t979,plain,
multiplication(domain(X1),c(X2)) = domain_difference(X1,domain(X2)),
inference(orient,[status(thm)],[t98]) ).
cnf(t47379,plain,
domain_difference(X1,domain(X2)) = domain_difference(X1,X2),
inference(step,[status(thm)],[t47378,t979]) ).
cnf(t3492,plain,
domain_difference(X1,domain(X2)) = domain_difference(X1,X2),
inference(rw,[status(thm)],[t47379]) ).
cnf(t3606,plain,
domain_difference(X1,domain(X2)) = domain_difference(X1,X2),
inference(orient,[status(thm)],[t3492]) ).
cnf(t48547,plain,
coantidomain(domain(X1)) = domain_difference(coantidomain(domain(X1)),X1),
inference(step,[status(thm)],[t48546,t3606]) ).
cnf(t28516,plain,
domain_difference(coantidomain(domain(X1)),X1) = coantidomain(domain(X1)),
inference(orient,[status(thm)],[t48547]) ).
cnf(t48964,plain,
c(X1) = coantidomain(domain(X1)),
inference(step,[status(thm)],[t48963,t28516]) ).
cnf(t46812,plain,
coantidomain(domain(X1)) = c(X1),
inference(orient,[status(thm)],[t48964]) ).
cnf(t46846,plain,
codomain(domain(X1)) = c(c(X1)),
inference(cp,[status(thm)],[t27181,t46812]) ).
cnf(t49066,plain,
codomain(domain(X1)) = domain(X1),
inference(step,[status(thm)],[t46846,t3521]) ).
cnf(t47011,plain,
codomain(domain(X1)) = domain(X1),
inference(orient,[status(thm)],[t49066]) ).
fof(f26,conjecture,
! [X0] : addition(backward_diamond(one,domain(X0)),domain(X0)) = domain(X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goals) ).
fof(f26_neg,negated_conjecture,
~ ! [X0] : addition(backward_diamond(one,domain(X0)),domain(X0)) = domain(X0),
inference(negated_conjecture,[status(cth)],[f26]) ).
fof(f26_nnf,plain,
? [X0] : addition(backward_diamond(one,domain(X0)),domain(X0)) != domain(X0),
inference(nnf_transformation,[status(thm)],[f26_neg]) ).
fof(f26_sk,plain,
addition(backward_diamond(one,domain(sk0)),domain(sk0)) != domain(sk0),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk0])],[f26_nnf]) ).
cnf(c27,plain,
addition(backward_diamond(one,domain(sk0)),domain(sk0)) != domain(sk0),
inference(cnf_transformation,[status(esa)],[f26_sk]) ).
cnf(goal_0,negated_conjecture,
addition(backward_diamond(one,domain(sk0)),domain(sk0)) != domain(sk0),
inference(equality_encoding,[status(esa)],[c27]) ).
cnf(g0_0,plain,
addition(domain(sk0),backward_diamond(one,domain(sk0))) != domain(sk0),
inference(rw,[status(thm)],[goal_0,t100]) ).
cnf(g0_1,plain,
addition(domain(sk0),codomain(domain(sk0))) != domain(sk0),
inference(rw,[status(thm)],[g0_0,t4411]) ).
cnf(g0_2,plain,
addition(domain(sk0),domain(sk0)) != domain(sk0),
inference(rw,[status(thm)],[g0_1,t47011]) ).
cnf(g0_3,plain,
domain(sk0) != domain(sk0),
inference(rw,[status(thm)],[g0_2,t35]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_3]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : KLE120+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.09/0.35 % Computer : n005.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Wed Sep 23 18:59:47 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.36 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 44.69/6.29 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 44.69/6.29 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------