%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : KLE132+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:40 PM UTC 2026
% Result : Theorem 57.60s 12.80s
% Output : Proof 2.32s
% Verified :
% SZS Type : Refutation
% Derivation depth : 113
% Number of leaves : 28
% Syntax : Number of formulae : 803 ( 794 unt; 0 def)
% Number of atoms : 820 ( 812 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 30 ( 13 ~; 6 |; 6 &)
% ( 1 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 1 avg)
% Maximal term depth : 16 ( 2 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 19 ( 19 usr; 5 con; 0-4 aty)
% Number of variables : 1082 ( 52 sgn 137 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
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(t30,plain,
addition(multiplication(X1,X2),multiplication(X3,X2)) = multiplication(addition(X1,X3),X2),
inference(equality_encoding,[status(esa)],[c8]) ).
cnf(t89,plain,
addition(multiplication(X1,X2),multiplication(X3,X2)) = multiplication(addition(X1,X3),X2),
inference(orient,[status(thm)],[t30]) ).
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(t80,plain,
multiplication(antidomain(X1),X1) = zero,
inference(orient,[status(thm)],[t13]) ).
cnf(t95,plain,
multiplication(addition(X1,antidomain(X2)),X2) = addition(multiplication(X1,X2),zero),
inference(cp,[status(thm)],[t89,t80]) ).
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(t44,plain,
addition(X1,zero) = X1,
inference(orient,[status(thm)],[t1]) ).
cnf(t44570,plain,
multiplication(addition(X1,antidomain(X2)),X2) = multiplication(X1,X2),
inference(step,[status(thm)],[t95,t44]) ).
cnf(t2712,plain,
multiplication(addition(X1,antidomain(X2)),X2) = multiplication(X1,X2),
inference(orient,[status(thm)],[t44570]) ).
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(t17,plain,
addition(antidomain(antidomain(X1)),antidomain(X1)) = one,
inference(equality_encoding,[status(esa)],[c15]) ).
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(t110,plain,
addition(X1,X2) = addition(X2,X1),
inference(orient,[status(thm)],[t14]) ).
cnf(t44326,plain,
addition(antidomain(X1),antidomain(antidomain(X1))) = one,
inference(step,[status(thm)],[t17,t110]) ).
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(t49,plain,
antidomain(antidomain(X1)) = domain(X1),
inference(orient,[status(thm)],[t9]) ).
cnf(t44327,plain,
addition(antidomain(X1),domain(X1)) = one,
inference(step,[status(thm)],[t44326,t49]) ).
cnf(t44328,plain,
addition(domain(X1),antidomain(X1)) = one,
inference(step,[status(thm)],[t44327,t110]) ).
cnf(t127,plain,
addition(domain(X1),antidomain(X1)) = one,
inference(orient,[status(thm)],[t44328]) ).
cnf(t2713,plain,
multiplication(domain(X1),X1) = multiplication(one,X1),
inference(cp,[status(thm)],[t2712,t127]) ).
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(t42,plain,
multiplication(one,X1) = X1,
inference(orient,[status(thm)],[t7]) ).
cnf(t44571,plain,
multiplication(domain(X1),X1) = X1,
inference(step,[status(thm)],[t2713,t42]) ).
cnf(t2755,plain,
multiplication(domain(X1),X1) = X1,
inference(orient,[status(thm)],[t44571]) ).
cnf(t2775,plain,
multiplication(addition(domain(X1),X2),X1) = addition(X1,multiplication(X2,X1)),
inference(cp,[status(thm)],[t89,t2755]) ).
cnf(t93,plain,
multiplication(addition(one,X1),X2) = addition(X2,multiplication(X1,X2)),
inference(cp,[status(thm)],[t89,t42]) ).
cnf(t2076,plain,
addition(X1,multiplication(X2,X1)) = multiplication(addition(one,X2),X1),
inference(orient,[status(thm)],[t93]) ).
cnf(t45209,plain,
multiplication(addition(domain(X1),X2),X1) = multiplication(addition(one,X2),X1),
inference(step,[status(thm)],[t2775,t2076]) ).
cnf(t13409,plain,
multiplication(addition(domain(X1),X2),X1) = multiplication(addition(one,X2),X1),
inference(orient,[status(thm)],[t45209]) ).
fof(f28,conjecture,
! [X0] :
( ! [X1] : addition(forward_diamond(X0,domain(X1)),forward_diamond(star(X0),domain_difference(domain(X1),forward_diamond(X0,domain(X1))))) = forward_diamond(star(X0),domain_difference(domain(X1),forward_diamond(X0,domain(X1))))
=> ! [X2] :
( addition(domain(X2),forward_diamond(X0,domain(X2))) = forward_diamond(X0,domain(X2))
=> domain(X2) = zero ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goals) ).
fof(f28_neg,negated_conjecture,
~ ! [X0] :
( ! [X1] : addition(forward_diamond(X0,domain(X1)),forward_diamond(star(X0),domain_difference(domain(X1),forward_diamond(X0,domain(X1))))) = forward_diamond(star(X0),domain_difference(domain(X1),forward_diamond(X0,domain(X1))))
=> ! [X2] :
( addition(domain(X2),forward_diamond(X0,domain(X2))) = forward_diamond(X0,domain(X2))
=> domain(X2) = zero ) ),
inference(negated_conjecture,[status(cth)],[f28]) ).
fof(f28_nnf,plain,
? [X0] :
( ? [X2] :
( domain(X2) != zero
& addition(domain(X2),forward_diamond(X0,domain(X2))) = forward_diamond(X0,domain(X2)) )
& ! [X1] : addition(forward_diamond(X0,domain(X1)),forward_diamond(star(X0),domain_difference(domain(X1),forward_diamond(X0,domain(X1))))) = forward_diamond(star(X0),domain_difference(domain(X1),forward_diamond(X0,domain(X1)))) ),
inference(nnf_transformation,[status(thm)],[f28_neg]) ).
fof(f28_sk,plain,
! [X1] :
( domain(sk1) != zero
& addition(domain(sk1),forward_diamond(sk0,domain(sk1))) = forward_diamond(sk0,domain(sk1))
& addition(forward_diamond(sk0,domain(X1)),forward_diamond(star(sk0),domain_difference(domain(X1),forward_diamond(sk0,domain(X1))))) = forward_diamond(star(sk0),domain_difference(domain(X1),forward_diamond(sk0,domain(X1)))) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk0,sk1])],[f28_nnf]) ).
cnf(c30,plain,
addition(domain(sk1),forward_diamond(sk0,domain(sk1))) = forward_diamond(sk0,domain(sk1)),
inference(cnf_transformation,[status(esa)],[f28_sk]) ).
cnf(t28,plain,
addition(domain(sk1),forward_diamond(sk0,domain(sk1))) = forward_diamond(sk0,domain(sk1)),
inference(equality_encoding,[status(esa)],[c30]) ).
cnf(t132,plain,
addition(domain(sk1),forward_diamond(sk0,domain(sk1))) = forward_diamond(sk0,domain(sk1)),
inference(orient,[status(thm)],[t28]) ).
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(t22,plain,
domain(multiplication(X1,domain(X2))) = forward_diamond(X1,X2),
inference(equality_encoding,[status(esa)],[c23]) ).
cnf(t157,plain,
domain(multiplication(X1,domain(X2))) = forward_diamond(X1,X2),
inference(orient,[status(thm)],[t22]) ).
cnf(t50,plain,
domain(antidomain(X1)) = antidomain(domain(X1)),
inference(cp,[status(thm)],[t49,t49]) ).
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(t60,plain,
antidomain(domain(X1)) = c(X1),
inference(orient,[status(thm)],[t10]) ).
cnf(t44372,plain,
domain(antidomain(X1)) = c(X1),
inference(step,[status(thm)],[t50,t60]) ).
cnf(t314,plain,
domain(antidomain(X1)) = c(X1),
inference(orient,[status(thm)],[t44372]) ).
cnf(t320,plain,
forward_diamond(X1,antidomain(X2)) = domain(multiplication(X1,c(X2))),
inference(cp,[status(thm)],[t157,t314]) ).
cnf(t1333,plain,
domain(multiplication(X1,c(X2))) = forward_diamond(X1,antidomain(X2)),
inference(orient,[status(thm)],[t320]) ).
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(t29,plain,
addition(multiplication(X1,X2),multiplication(X1,X3)) = multiplication(X1,addition(X2,X3)),
inference(equality_encoding,[status(esa)],[c7]) ).
cnf(t65,plain,
addition(multiplication(X1,X2),multiplication(X1,X3)) = multiplication(X1,addition(X2,X3)),
inference(orient,[status(thm)],[t29]) ).
cnf(t84,plain,
multiplication(antidomain(X1),addition(X1,X2)) = addition(zero,multiplication(antidomain(X1),X2)),
inference(cp,[status(thm)],[t65,t80]) ).
cnf(t111,plain,
addition(zero,X1) = X1,
inference(cp,[status(thm)],[t110,t44]) ).
cnf(t289,plain,
addition(zero,X1) = X1,
inference(orient,[status(thm)],[t111]) ).
cnf(t44729,plain,
multiplication(antidomain(X1),addition(X1,X2)) = multiplication(antidomain(X1),X2),
inference(step,[status(thm)],[t84,t289]) ).
cnf(t5534,plain,
multiplication(antidomain(X1),addition(X1,X2)) = multiplication(antidomain(X1),X2),
inference(orient,[status(thm)],[t44729]) ).
cnf(t5553,plain,
multiplication(antidomain(domain(X1)),antidomain(X1)) = multiplication(antidomain(domain(X1)),one),
inference(cp,[status(thm)],[t5534,t127]) ).
cnf(t44730,plain,
multiplication(c(X1),antidomain(X1)) = multiplication(antidomain(domain(X1)),one),
inference(step,[status(thm)],[t5553,t60]) ).
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(t23,plain,
multiplication(domain(X1),antidomain(X2)) = domain_difference(X1,X2),
inference(equality_encoding,[status(esa)],[c22]) ).
cnf(t99,plain,
multiplication(domain(X1),antidomain(X2)) = domain_difference(X1,X2),
inference(orient,[status(thm)],[t23]) ).
cnf(t318,plain,
domain_difference(antidomain(X1),X2) = multiplication(c(X1),antidomain(X2)),
inference(cp,[status(thm)],[t99,t314]) ).
cnf(t1307,plain,
multiplication(c(X1),antidomain(X2)) = domain_difference(antidomain(X1),X2),
inference(orient,[status(thm)],[t318]) ).
cnf(t44731,plain,
domain_difference(antidomain(X1),X1) = multiplication(antidomain(domain(X1)),one),
inference(step,[status(thm)],[t44730,t1307]) ).
cnf(t2757,plain,
antidomain(X1) = domain_difference(antidomain(X1),X1),
inference(cp,[status(thm)],[t2755,t99]) ).
cnf(t2845,plain,
domain_difference(antidomain(X1),X1) = antidomain(X1),
inference(orient,[status(thm)],[t2757]) ).
cnf(t44732,plain,
antidomain(X1) = multiplication(antidomain(domain(X1)),one),
inference(step,[status(thm)],[t44731,t2845]) ).
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(t41,plain,
multiplication(X1,one) = X1,
inference(orient,[status(thm)],[t5]) ).
cnf(t44733,plain,
antidomain(X1) = antidomain(domain(X1)),
inference(step,[status(thm)],[t44732,t41]) ).
cnf(t44734,plain,
antidomain(X1) = c(X1),
inference(step,[status(thm)],[t44733,t60]) ).
cnf(t5571,plain,
antidomain(X1) = c(X1),
inference(orient,[status(thm)],[t44734]) ).
cnf(t44741,plain,
domain(multiplication(X1,c(X2))) = forward_diamond(X1,c(X2)),
inference(step,[status(thm)],[t1333,t5571]) ).
cnf(t5578,plain,
domain(multiplication(X1,c(X2))) = forward_diamond(X1,c(X2)),
inference(orient,[status(thm)],[t44741]) ).
cnf(t44792,plain,
c(antidomain(X1)) = domain(X1),
inference(step,[status(thm)],[t49,t5571]) ).
cnf(t44793,plain,
c(c(X1)) = domain(X1),
inference(step,[status(thm)],[t44792,t5571]) ).
cnf(t5618,plain,
c(c(X1)) = domain(X1),
inference(rw,[status(thm)],[t44793]) ).
cnf(t5669,plain,
c(c(X1)) = domain(X1),
inference(orient,[status(thm)],[t5618]) ).
cnf(t5691,plain,
forward_diamond(X1,c(c(X2))) = domain(multiplication(X1,domain(X2))),
inference(cp,[status(thm)],[t5578,t5669]) ).
cnf(t44891,plain,
forward_diamond(X1,domain(X2)) = domain(multiplication(X1,domain(X2))),
inference(step,[status(thm)],[t5691,t5669]) ).
cnf(t44892,plain,
forward_diamond(X1,domain(X2)) = forward_diamond(X1,X2),
inference(step,[status(thm)],[t44891,t157]) ).
cnf(t5834,plain,
forward_diamond(X1,domain(X2)) = forward_diamond(X1,X2),
inference(orient,[status(thm)],[t44892]) ).
cnf(t44895,plain,
addition(domain(sk1),forward_diamond(sk0,sk1)) = forward_diamond(sk0,domain(sk1)),
inference(step,[status(thm)],[t132,t5834]) ).
cnf(t44896,plain,
addition(domain(sk1),forward_diamond(sk0,sk1)) = forward_diamond(sk0,sk1),
inference(step,[status(thm)],[t44895,t5834]) ).
cnf(t5843,plain,
addition(domain(sk1),forward_diamond(sk0,sk1)) = forward_diamond(sk0,sk1),
inference(rw,[status(thm)],[t44896]) ).
cnf(t7439,plain,
addition(domain(sk1),forward_diamond(sk0,sk1)) = forward_diamond(sk0,sk1),
inference(orient,[status(thm)],[t5843]) ).
cnf(t13411,plain,
multiplication(addition(one,forward_diamond(sk0,sk1)),sk1) = multiplication(forward_diamond(sk0,sk1),sk1),
inference(cp,[status(thm)],[t13409,t7439]) ).
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(t115,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(t43,plain,
addition(X1,X1) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t118,plain,
addition(X1,addition(X1,X2)) = addition(X1,X2),
inference(cp,[status(thm)],[t115,t43]) ).
cnf(t790,plain,
addition(X1,addition(X1,X2)) = addition(X1,X2),
inference(orient,[status(thm)],[t118]) ).
cnf(t793,plain,
addition(domain(X1),antidomain(X1)) = addition(domain(X1),one),
inference(cp,[status(thm)],[t790,t127]) ).
cnf(t44438,plain,
one = addition(domain(X1),one),
inference(step,[status(thm)],[t793,t127]) ).
cnf(t44439,plain,
one = addition(one,domain(X1)),
inference(step,[status(thm)],[t44438,t110]) ).
cnf(t806,plain,
addition(one,domain(X1)) = one,
inference(orient,[status(thm)],[t44439]) ).
cnf(t813,plain,
one = addition(one,forward_diamond(X1,X2)),
inference(cp,[status(thm)],[t806,t157]) ).
cnf(t883,plain,
addition(one,forward_diamond(X1,X2)) = one,
inference(orient,[status(thm)],[t813]) ).
cnf(t45215,plain,
multiplication(one,sk1) = multiplication(forward_diamond(sk0,sk1),sk1),
inference(step,[status(thm)],[t13411,t883]) ).
cnf(t45216,plain,
sk1 = multiplication(forward_diamond(sk0,sk1),sk1),
inference(step,[status(thm)],[t45215,t42]) ).
cnf(t13566,plain,
multiplication(forward_diamond(sk0,sk1),sk1) = sk1,
inference(orient,[status(thm)],[t45216]) ).
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(c12,plain,
( addition(X0,X1) != X1
| leq(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f11_sk]) ).
cnf(hi12,axiom,
ifeq(addition(X0,X1),X1,leq(X0,X1),true) = true,
inference(equality_encoding,[status(esa)],[c12]) ).
cnf(c29,plain,
addition(forward_diamond(sk0,domain(X1)),forward_diamond(star(sk0),domain_difference(domain(X1),forward_diamond(sk0,domain(X1))))) = forward_diamond(star(sk0),domain_difference(domain(X1),forward_diamond(sk0,domain(X1)))),
inference(cnf_transformation,[status(esa)],[f28_sk]) ).
cnf(hi23,negated_conjecture,
addition(forward_diamond(sk0,domain(X0)),forward_diamond(star(sk0),domain_difference(domain(X0),forward_diamond(sk0,domain(X0))))) = forward_diamond(star(sk0),domain_difference(domain(X0),forward_diamond(sk0,domain(X0)))),
inference(equality_encoding,[status(esa)],[c29]) ).
cnf(hi21,axiom,
domain(X0) = antidomain(antidomain(X0)),
inference(equality_encoding,[status(esa)],[c16]) ).
cnf(hi20,axiom,
forward_diamond(X0,X1) = domain(multiplication(X0,domain(X1))),
inference(equality_encoding,[status(esa)],[c23]) ).
cnf(hi24,axiom,
domain_difference(X0,X1) = multiplication(domain(X0),antidomain(X1)),
inference(equality_encoding,[status(esa)],[c22]) ).
cnf(h5,plain,
leq(antidomain(antidomain(multiplication(sk0,antidomain(antidomain(antidomain(antidomain(V0))))))),antidomain(antidomain(multiplication(star(sk0),antidomain(antidomain(multiplication(antidomain(antidomain(antidomain(antidomain(V0)))),antidomain(antidomain(antidomain(multiplication(sk0,antidomain(antidomain(antidomain(antidomain(V0))))))))))))))) = true,
inference(hyper_resolution,[status(thm)],[hi12,hi23,hi21,hi20,hi24]) ).
cnf(c11,plain,
( addition(X0,X1) = X1
| ~ leq(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f11_sk]) ).
cnf(hi11,axiom,
ifeq(leq(X0,X1),true,addition(X0,X1),X1) = X1,
inference(equality_encoding,[status(esa)],[c11]) ).
cnf(t40,plain,
addition(antidomain(antidomain(multiplication(sk0,antidomain(antidomain(antidomain(antidomain(X1))))))),antidomain(antidomain(multiplication(star(sk0),antidomain(antidomain(multiplication(antidomain(antidomain(antidomain(antidomain(X1)))),antidomain(antidomain(antidomain(multiplication(sk0,antidomain(antidomain(antidomain(antidomain(X1))))))))))))))) = antidomain(antidomain(multiplication(star(sk0),antidomain(antidomain(multiplication(antidomain(antidomain(antidomain(antidomain(X1)))),antidomain(antidomain(antidomain(multiplication(sk0,antidomain(antidomain(antidomain(antidomain(X1)))))))))))))),
inference(hyper_resolution,[status(thm)],[hi11,h5]) ).
cnf(t44307,plain,
addition(domain(multiplication(sk0,antidomain(antidomain(antidomain(antidomain(X1)))))),antidomain(antidomain(multiplication(star(sk0),antidomain(antidomain(multiplication(antidomain(antidomain(antidomain(antidomain(X1)))),antidomain(antidomain(antidomain(multiplication(sk0,antidomain(antidomain(antidomain(antidomain(X1))))))))))))))) = antidomain(antidomain(multiplication(star(sk0),antidomain(antidomain(multiplication(antidomain(antidomain(antidomain(antidomain(X1)))),antidomain(antidomain(antidomain(multiplication(sk0,antidomain(antidomain(antidomain(antidomain(X1)))))))))))))),
inference(step,[status(thm)],[t40,t49]) ).
cnf(t44308,plain,
addition(domain(multiplication(sk0,domain(antidomain(antidomain(X1))))),antidomain(antidomain(multiplication(star(sk0),antidomain(antidomain(multiplication(antidomain(antidomain(antidomain(antidomain(X1)))),antidomain(antidomain(antidomain(multiplication(sk0,antidomain(antidomain(antidomain(antidomain(X1))))))))))))))) = antidomain(antidomain(multiplication(star(sk0),antidomain(antidomain(multiplication(antidomain(antidomain(antidomain(antidomain(X1)))),antidomain(antidomain(antidomain(multiplication(sk0,antidomain(antidomain(antidomain(antidomain(X1)))))))))))))),
inference(step,[status(thm)],[t44307,t49]) ).
cnf(t44309,plain,
addition(domain(multiplication(sk0,domain(domain(X1)))),antidomain(antidomain(multiplication(star(sk0),antidomain(antidomain(multiplication(antidomain(antidomain(antidomain(antidomain(X1)))),antidomain(antidomain(antidomain(multiplication(sk0,antidomain(antidomain(antidomain(antidomain(X1))))))))))))))) = antidomain(antidomain(multiplication(star(sk0),antidomain(antidomain(multiplication(antidomain(antidomain(antidomain(antidomain(X1)))),antidomain(antidomain(antidomain(multiplication(sk0,antidomain(antidomain(antidomain(antidomain(X1)))))))))))))),
inference(step,[status(thm)],[t44308,t49]) ).
cnf(t44310,plain,
addition(domain(multiplication(sk0,domain(domain(X1)))),domain(multiplication(star(sk0),antidomain(antidomain(multiplication(antidomain(antidomain(antidomain(antidomain(X1)))),antidomain(antidomain(antidomain(multiplication(sk0,antidomain(antidomain(antidomain(antidomain(X1)))))))))))))) = antidomain(antidomain(multiplication(star(sk0),antidomain(antidomain(multiplication(antidomain(antidomain(antidomain(antidomain(X1)))),antidomain(antidomain(antidomain(multiplication(sk0,antidomain(antidomain(antidomain(antidomain(X1)))))))))))))),
inference(step,[status(thm)],[t44309,t49]) ).
cnf(t44311,plain,
addition(domain(multiplication(sk0,domain(domain(X1)))),domain(multiplication(star(sk0),domain(multiplication(antidomain(antidomain(antidomain(antidomain(X1)))),antidomain(antidomain(antidomain(multiplication(sk0,antidomain(antidomain(antidomain(antidomain(X1))))))))))))) = antidomain(antidomain(multiplication(star(sk0),antidomain(antidomain(multiplication(antidomain(antidomain(antidomain(antidomain(X1)))),antidomain(antidomain(antidomain(multiplication(sk0,antidomain(antidomain(antidomain(antidomain(X1)))))))))))))),
inference(step,[status(thm)],[t44310,t49]) ).
cnf(t44312,plain,
addition(domain(multiplication(sk0,domain(domain(X1)))),domain(multiplication(star(sk0),domain(multiplication(domain(antidomain(antidomain(X1))),antidomain(antidomain(antidomain(multiplication(sk0,antidomain(antidomain(antidomain(antidomain(X1))))))))))))) = antidomain(antidomain(multiplication(star(sk0),antidomain(antidomain(multiplication(antidomain(antidomain(antidomain(antidomain(X1)))),antidomain(antidomain(antidomain(multiplication(sk0,antidomain(antidomain(antidomain(antidomain(X1)))))))))))))),
inference(step,[status(thm)],[t44311,t49]) ).
cnf(t44313,plain,
addition(domain(multiplication(sk0,domain(domain(X1)))),domain(multiplication(star(sk0),domain(multiplication(domain(domain(X1)),antidomain(antidomain(antidomain(multiplication(sk0,antidomain(antidomain(antidomain(antidomain(X1))))))))))))) = antidomain(antidomain(multiplication(star(sk0),antidomain(antidomain(multiplication(antidomain(antidomain(antidomain(antidomain(X1)))),antidomain(antidomain(antidomain(multiplication(sk0,antidomain(antidomain(antidomain(antidomain(X1)))))))))))))),
inference(step,[status(thm)],[t44312,t49]) ).
cnf(t44314,plain,
addition(domain(multiplication(sk0,domain(domain(X1)))),domain(multiplication(star(sk0),domain(multiplication(domain(domain(X1)),domain(antidomain(multiplication(sk0,antidomain(antidomain(antidomain(antidomain(X1)))))))))))) = antidomain(antidomain(multiplication(star(sk0),antidomain(antidomain(multiplication(antidomain(antidomain(antidomain(antidomain(X1)))),antidomain(antidomain(antidomain(multiplication(sk0,antidomain(antidomain(antidomain(antidomain(X1)))))))))))))),
inference(step,[status(thm)],[t44313,t49]) ).
cnf(t44315,plain,
addition(domain(multiplication(sk0,domain(domain(X1)))),domain(multiplication(star(sk0),domain(multiplication(domain(domain(X1)),domain(antidomain(multiplication(sk0,domain(antidomain(antidomain(X1))))))))))) = antidomain(antidomain(multiplication(star(sk0),antidomain(antidomain(multiplication(antidomain(antidomain(antidomain(antidomain(X1)))),antidomain(antidomain(antidomain(multiplication(sk0,antidomain(antidomain(antidomain(antidomain(X1)))))))))))))),
inference(step,[status(thm)],[t44314,t49]) ).
cnf(t44316,plain,
addition(domain(multiplication(sk0,domain(domain(X1)))),domain(multiplication(star(sk0),domain(multiplication(domain(domain(X1)),domain(antidomain(multiplication(sk0,domain(domain(X1)))))))))) = antidomain(antidomain(multiplication(star(sk0),antidomain(antidomain(multiplication(antidomain(antidomain(antidomain(antidomain(X1)))),antidomain(antidomain(antidomain(multiplication(sk0,antidomain(antidomain(antidomain(antidomain(X1)))))))))))))),
inference(step,[status(thm)],[t44315,t49]) ).
cnf(t44317,plain,
addition(domain(multiplication(sk0,domain(domain(X1)))),domain(multiplication(star(sk0),domain(multiplication(domain(domain(X1)),domain(antidomain(multiplication(sk0,domain(domain(X1)))))))))) = domain(multiplication(star(sk0),antidomain(antidomain(multiplication(antidomain(antidomain(antidomain(antidomain(X1)))),antidomain(antidomain(antidomain(multiplication(sk0,antidomain(antidomain(antidomain(antidomain(X1))))))))))))),
inference(step,[status(thm)],[t44316,t49]) ).
cnf(t44318,plain,
addition(domain(multiplication(sk0,domain(domain(X1)))),domain(multiplication(star(sk0),domain(multiplication(domain(domain(X1)),domain(antidomain(multiplication(sk0,domain(domain(X1)))))))))) = domain(multiplication(star(sk0),domain(multiplication(antidomain(antidomain(antidomain(antidomain(X1)))),antidomain(antidomain(antidomain(multiplication(sk0,antidomain(antidomain(antidomain(antidomain(X1)))))))))))),
inference(step,[status(thm)],[t44317,t49]) ).
cnf(t44319,plain,
addition(domain(multiplication(sk0,domain(domain(X1)))),domain(multiplication(star(sk0),domain(multiplication(domain(domain(X1)),domain(antidomain(multiplication(sk0,domain(domain(X1)))))))))) = domain(multiplication(star(sk0),domain(multiplication(domain(antidomain(antidomain(X1))),antidomain(antidomain(antidomain(multiplication(sk0,antidomain(antidomain(antidomain(antidomain(X1)))))))))))),
inference(step,[status(thm)],[t44318,t49]) ).
cnf(t44320,plain,
addition(domain(multiplication(sk0,domain(domain(X1)))),domain(multiplication(star(sk0),domain(multiplication(domain(domain(X1)),domain(antidomain(multiplication(sk0,domain(domain(X1)))))))))) = domain(multiplication(star(sk0),domain(multiplication(domain(domain(X1)),antidomain(antidomain(antidomain(multiplication(sk0,antidomain(antidomain(antidomain(antidomain(X1)))))))))))),
inference(step,[status(thm)],[t44319,t49]) ).
cnf(t44321,plain,
addition(domain(multiplication(sk0,domain(domain(X1)))),domain(multiplication(star(sk0),domain(multiplication(domain(domain(X1)),domain(antidomain(multiplication(sk0,domain(domain(X1)))))))))) = domain(multiplication(star(sk0),domain(multiplication(domain(domain(X1)),domain(antidomain(multiplication(sk0,antidomain(antidomain(antidomain(antidomain(X1))))))))))),
inference(step,[status(thm)],[t44320,t49]) ).
cnf(t44322,plain,
addition(domain(multiplication(sk0,domain(domain(X1)))),domain(multiplication(star(sk0),domain(multiplication(domain(domain(X1)),domain(antidomain(multiplication(sk0,domain(domain(X1)))))))))) = domain(multiplication(star(sk0),domain(multiplication(domain(domain(X1)),domain(antidomain(multiplication(sk0,domain(antidomain(antidomain(X1)))))))))),
inference(step,[status(thm)],[t44321,t49]) ).
cnf(t44323,plain,
addition(domain(multiplication(sk0,domain(domain(X1)))),domain(multiplication(star(sk0),domain(multiplication(domain(domain(X1)),domain(antidomain(multiplication(sk0,domain(domain(X1)))))))))) = domain(multiplication(star(sk0),domain(multiplication(domain(domain(X1)),domain(antidomain(multiplication(sk0,domain(domain(X1))))))))),
inference(step,[status(thm)],[t44322,t49]) ).
cnf(t53,plain,
addition(domain(multiplication(sk0,domain(domain(X1)))),domain(multiplication(star(sk0),domain(multiplication(domain(domain(X1)),domain(antidomain(multiplication(sk0,domain(domain(X1)))))))))) = domain(multiplication(star(sk0),domain(multiplication(domain(domain(X1)),domain(antidomain(multiplication(sk0,domain(domain(X1))))))))),
inference(orient,[status(thm)],[t44323]) ).
cnf(t44330,plain,
addition(forward_diamond(sk0,domain(X1)),domain(multiplication(star(sk0),domain(multiplication(domain(domain(X1)),domain(antidomain(multiplication(sk0,domain(domain(X1)))))))))) = domain(multiplication(star(sk0),domain(multiplication(domain(domain(X1)),domain(antidomain(multiplication(sk0,domain(domain(X1))))))))),
inference(step,[status(thm)],[t53,t157]) ).
cnf(t44331,plain,
addition(forward_diamond(sk0,domain(X1)),forward_diamond(star(sk0),multiplication(domain(domain(X1)),domain(antidomain(multiplication(sk0,domain(domain(X1)))))))) = domain(multiplication(star(sk0),domain(multiplication(domain(domain(X1)),domain(antidomain(multiplication(sk0,domain(domain(X1))))))))),
inference(step,[status(thm)],[t44330,t157]) ).
cnf(t44332,plain,
addition(forward_diamond(sk0,domain(X1)),forward_diamond(star(sk0),multiplication(domain(domain(X1)),domain(antidomain(multiplication(sk0,domain(domain(X1)))))))) = forward_diamond(star(sk0),multiplication(domain(domain(X1)),domain(antidomain(multiplication(sk0,domain(domain(X1))))))),
inference(step,[status(thm)],[t44331,t157]) ).
cnf(t178,plain,
addition(forward_diamond(sk0,domain(X1)),forward_diamond(star(sk0),multiplication(domain(domain(X1)),domain(antidomain(multiplication(sk0,domain(domain(X1)))))))) = forward_diamond(star(sk0),multiplication(domain(domain(X1)),domain(antidomain(multiplication(sk0,domain(domain(X1))))))),
inference(rw,[status(thm)],[t44332]) ).
cnf(t45562,plain,
addition(forward_diamond(sk0,X1),forward_diamond(star(sk0),multiplication(domain(domain(X1)),domain(antidomain(multiplication(sk0,domain(domain(X1)))))))) = forward_diamond(star(sk0),multiplication(domain(domain(X1)),domain(antidomain(multiplication(sk0,domain(domain(X1))))))),
inference(step,[status(thm)],[t178,t5834]) ).
cnf(t5841,plain,
forward_diamond(X1,multiplication(X2,domain(X3))) = forward_diamond(X1,forward_diamond(X2,X3)),
inference(cp,[status(thm)],[t5834,t157]) ).
cnf(t14867,plain,
forward_diamond(X1,multiplication(X2,domain(X3))) = forward_diamond(X1,forward_diamond(X2,X3)),
inference(orient,[status(thm)],[t5841]) ).
cnf(t45563,plain,
addition(forward_diamond(sk0,X1),forward_diamond(star(sk0),forward_diamond(domain(domain(X1)),antidomain(multiplication(sk0,domain(domain(X1))))))) = forward_diamond(star(sk0),multiplication(domain(domain(X1)),domain(antidomain(multiplication(sk0,domain(domain(X1))))))),
inference(step,[status(thm)],[t45562,t14867]) ).
cnf(t161,plain,
forward_diamond(one,X1) = domain(domain(X1)),
inference(cp,[status(thm)],[t157,t42]) ).
cnf(t345,plain,
domain(domain(X1)) = forward_diamond(one,X1),
inference(orient,[status(thm)],[t161]) ).
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(t62,plain,
multiplication(multiplication(X1,X2),X3) = multiplication(X1,multiplication(X2,X3)),
inference(orient,[status(thm)],[t27]) ).
cnf(t2779,plain,
multiplication(domain(X1),multiplication(X1,X2)) = multiplication(X1,X2),
inference(cp,[status(thm)],[t62,t2755]) ).
cnf(t3975,plain,
multiplication(domain(X1),multiplication(X1,X2)) = multiplication(X1,X2),
inference(orient,[status(thm)],[t2779]) ).
cnf(t2769,plain,
domain(X1) = multiplication(forward_diamond(one,X1),domain(X1)),
inference(cp,[status(thm)],[t2755,t345]) ).
cnf(t3301,plain,
multiplication(forward_diamond(one,X1),domain(X1)) = domain(X1),
inference(orient,[status(thm)],[t2769]) ).
cnf(t3994,plain,
multiplication(forward_diamond(one,X1),domain(X1)) = multiplication(domain(forward_diamond(one,X1)),domain(X1)),
inference(cp,[status(thm)],[t3975,t3301]) ).
cnf(t44688,plain,
domain(X1) = multiplication(domain(forward_diamond(one,X1)),domain(X1)),
inference(step,[status(thm)],[t3994,t3301]) ).
cnf(t100,plain,
domain_difference(X1,antidomain(X2)) = multiplication(domain(X1),domain(X2)),
inference(cp,[status(thm)],[t99,t49]) ).
cnf(t1228,plain,
multiplication(domain(X1),domain(X2)) = domain_difference(X1,antidomain(X2)),
inference(orient,[status(thm)],[t100]) ).
cnf(t44689,plain,
domain(X1) = domain_difference(forward_diamond(one,X1),antidomain(X1)),
inference(step,[status(thm)],[t44688,t1228]) ).
cnf(t4692,plain,
domain_difference(forward_diamond(one,X1),antidomain(X1)) = domain(X1),
inference(orient,[status(thm)],[t44689]) ).
cnf(t44761,plain,
domain_difference(forward_diamond(one,X1),c(X1)) = domain(X1),
inference(step,[status(thm)],[t4692,t5571]) ).
cnf(t61,plain,
domain(domain(X1)) = antidomain(c(X1)),
inference(cp,[status(thm)],[t49,t60]) ).
cnf(t337,plain,
antidomain(c(X1)) = domain(domain(X1)),
inference(orient,[status(thm)],[t61]) ).
cnf(t44373,plain,
antidomain(c(X1)) = forward_diamond(one,X1),
inference(step,[status(thm)],[t337,t345]) ).
cnf(t346,plain,
antidomain(c(X1)) = forward_diamond(one,X1),
inference(orient,[status(thm)],[t44373]) ).
cnf(t2857,plain,
antidomain(c(X1)) = domain_difference(forward_diamond(one,X1),c(X1)),
inference(cp,[status(thm)],[t2845,t346]) ).
cnf(t44703,plain,
forward_diamond(one,X1) = domain_difference(forward_diamond(one,X1),c(X1)),
inference(step,[status(thm)],[t2857,t346]) ).
cnf(t5004,plain,
domain_difference(forward_diamond(one,X1),c(X1)) = forward_diamond(one,X1),
inference(orient,[status(thm)],[t44703]) ).
cnf(t44762,plain,
forward_diamond(one,X1) = domain(X1),
inference(step,[status(thm)],[t44761,t5004]) ).
cnf(t5597,plain,
forward_diamond(one,X1) = domain(X1),
inference(rw,[status(thm)],[t44762]) ).
cnf(t5629,plain,
forward_diamond(one,X1) = domain(X1),
inference(orient,[status(thm)],[t5597]) ).
cnf(t44816,plain,
domain(domain(X1)) = domain(X1),
inference(step,[status(thm)],[t345,t5629]) ).
cnf(t5630,plain,
domain(domain(X1)) = domain(X1),
inference(orient,[status(thm)],[t44816]) ).
cnf(t45564,plain,
addition(forward_diamond(sk0,X1),forward_diamond(star(sk0),forward_diamond(domain(X1),antidomain(multiplication(sk0,domain(domain(X1))))))) = forward_diamond(star(sk0),multiplication(domain(domain(X1)),domain(antidomain(multiplication(sk0,domain(domain(X1))))))),
inference(step,[status(thm)],[t45563,t5630]) ).
cnf(t45565,plain,
addition(forward_diamond(sk0,X1),forward_diamond(star(sk0),forward_diamond(domain(X1),c(multiplication(sk0,domain(domain(X1))))))) = forward_diamond(star(sk0),multiplication(domain(domain(X1)),domain(antidomain(multiplication(sk0,domain(domain(X1))))))),
inference(step,[status(thm)],[t45564,t5571]) ).
cnf(t164,plain,
c(multiplication(X1,domain(X2))) = antidomain(forward_diamond(X1,X2)),
inference(cp,[status(thm)],[t60,t157]) ).
cnf(t1282,plain,
c(multiplication(X1,domain(X2))) = antidomain(forward_diamond(X1,X2)),
inference(orient,[status(thm)],[t164]) ).
cnf(t44739,plain,
c(multiplication(X1,domain(X2))) = c(forward_diamond(X1,X2)),
inference(step,[status(thm)],[t1282,t5571]) ).
cnf(t5576,plain,
c(multiplication(X1,domain(X2))) = c(forward_diamond(X1,X2)),
inference(orient,[status(thm)],[t44739]) ).
cnf(t1290,plain,
antidomain(forward_diamond(X1,antidomain(X2))) = c(multiplication(X1,c(X2))),
inference(cp,[status(thm)],[t1282,t314]) ).
cnf(t2336,plain,
antidomain(forward_diamond(X1,antidomain(X2))) = c(multiplication(X1,c(X2))),
inference(orient,[status(thm)],[t1290]) ).
cnf(t44797,plain,
c(forward_diamond(X1,antidomain(X2))) = c(multiplication(X1,c(X2))),
inference(step,[status(thm)],[t2336,t5571]) ).
cnf(t44798,plain,
c(forward_diamond(X1,c(X2))) = c(multiplication(X1,c(X2))),
inference(step,[status(thm)],[t44797,t5571]) ).
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(t20,plain,
c(forward_diamond(X1,c(X2))) = forward_box(X1,X2),
inference(equality_encoding,[status(esa)],[c25]) ).
cnf(t222,plain,
c(forward_diamond(X1,c(X2))) = forward_box(X1,X2),
inference(orient,[status(thm)],[t20]) ).
cnf(t44799,plain,
forward_box(X1,X2) = c(multiplication(X1,c(X2))),
inference(step,[status(thm)],[t44798,t222]) ).
cnf(t5622,plain,
forward_box(X1,X2) = c(multiplication(X1,c(X2))),
inference(rw,[status(thm)],[t44799]) ).
cnf(t5960,plain,
c(multiplication(X1,c(X2))) = forward_box(X1,X2),
inference(orient,[status(thm)],[t5622]) ).
cnf(t5968,plain,
forward_box(X1,c(X2)) = c(multiplication(X1,domain(X2))),
inference(cp,[status(thm)],[t5960,t5669]) ).
cnf(t44914,plain,
forward_box(X1,c(X2)) = c(forward_diamond(X1,X2)),
inference(step,[status(thm)],[t5968,t5576]) ).
cnf(t6076,plain,
c(forward_diamond(X1,X2)) = forward_box(X1,c(X2)),
inference(orient,[status(thm)],[t44914]) ).
cnf(t44915,plain,
c(multiplication(X1,domain(X2))) = forward_box(X1,c(X2)),
inference(step,[status(thm)],[t5576,t6076]) ).
cnf(t6077,plain,
c(multiplication(X1,domain(X2))) = forward_box(X1,c(X2)),
inference(orient,[status(thm)],[t44915]) ).
cnf(t45566,plain,
addition(forward_diamond(sk0,X1),forward_diamond(star(sk0),forward_diamond(domain(X1),forward_box(sk0,c(domain(X1)))))) = forward_diamond(star(sk0),multiplication(domain(domain(X1)),domain(antidomain(multiplication(sk0,domain(domain(X1))))))),
inference(step,[status(thm)],[t45565,t6077]) ).
cnf(t316,plain,
c(domain(X1)) = domain(c(X1)),
inference(cp,[status(thm)],[t314,t60]) ).
cnf(t387,plain,
c(domain(X1)) = domain(c(X1)),
inference(orient,[status(thm)],[t316]) ).
cnf(t81,plain,
zero = antidomain(one),
inference(cp,[status(thm)],[t80,t41]) ).
cnf(t236,plain,
antidomain(one) = zero,
inference(orient,[status(thm)],[t81]) ).
cnf(t239,plain,
domain(one) = antidomain(zero),
inference(cp,[status(thm)],[t49,t236]) ).
cnf(t237,plain,
one = addition(domain(one),zero),
inference(cp,[status(thm)],[t127,t236]) ).
cnf(t44357,plain,
one = domain(one),
inference(step,[status(thm)],[t237,t44]) ).
cnf(t240,plain,
domain(one) = one,
inference(orient,[status(thm)],[t44357]) ).
cnf(t44359,plain,
one = antidomain(zero),
inference(step,[status(thm)],[t239,t240]) ).
cnf(t263,plain,
antidomain(zero) = one,
inference(orient,[status(thm)],[t44359]) ).
cnf(t266,plain,
domain(zero) = antidomain(one),
inference(cp,[status(thm)],[t49,t263]) ).
cnf(t44360,plain,
domain(zero) = zero,
inference(step,[status(thm)],[t266,t236]) ).
cnf(t267,plain,
domain(zero) = zero,
inference(orient,[status(thm)],[t44360]) ).
cnf(t270,plain,
c(zero) = antidomain(zero),
inference(cp,[status(thm)],[t60,t267]) ).
cnf(t44361,plain,
c(zero) = one,
inference(step,[status(thm)],[t270,t263]) ).
cnf(t286,plain,
c(zero) = one,
inference(orient,[status(thm)],[t44361]) ).
cnf(t288,plain,
forward_box(X1,zero) = c(forward_diamond(X1,one)),
inference(cp,[status(thm)],[t222,t286]) ).
cnf(t243,plain,
forward_diamond(X1,one) = domain(multiplication(X1,one)),
inference(cp,[status(thm)],[t157,t240]) ).
cnf(t44370,plain,
forward_diamond(X1,one) = domain(X1),
inference(step,[status(thm)],[t243,t41]) ).
cnf(t309,plain,
forward_diamond(X1,one) = domain(X1),
inference(orient,[status(thm)],[t44370]) ).
cnf(t44383,plain,
forward_box(X1,zero) = c(domain(X1)),
inference(step,[status(thm)],[t288,t309]) ).
cnf(t44384,plain,
forward_box(X1,zero) = domain(c(X1)),
inference(step,[status(thm)],[t44383,t387]) ).
cnf(t423,plain,
domain(c(X1)) = forward_box(X1,zero),
inference(orient,[status(thm)],[t44384]) ).
cnf(t44385,plain,
c(domain(X1)) = forward_box(X1,zero),
inference(step,[status(thm)],[t387,t423]) ).
cnf(t424,plain,
c(domain(X1)) = forward_box(X1,zero),
inference(orient,[status(thm)],[t44385]) ).
cnf(t44786,plain,
domain(c(X1)) = c(X1),
inference(step,[status(thm)],[t314,t5571]) ).
cnf(t44787,plain,
forward_box(X1,zero) = c(X1),
inference(step,[status(thm)],[t44786,t423]) ).
cnf(t5615,plain,
forward_box(X1,zero) = c(X1),
inference(rw,[status(thm)],[t44787]) ).
cnf(t5657,plain,
forward_box(X1,zero) = c(X1),
inference(orient,[status(thm)],[t5615]) ).
cnf(t44850,plain,
c(domain(X1)) = c(X1),
inference(step,[status(thm)],[t424,t5657]) ).
cnf(t5658,plain,
c(domain(X1)) = c(X1),
inference(orient,[status(thm)],[t44850]) ).
cnf(t45567,plain,
addition(forward_diamond(sk0,X1),forward_diamond(star(sk0),forward_diamond(domain(X1),forward_box(sk0,c(X1))))) = forward_diamond(star(sk0),multiplication(domain(domain(X1)),domain(antidomain(multiplication(sk0,domain(domain(X1))))))),
inference(step,[status(thm)],[t45566,t5658]) ).
cnf(t45568,plain,
addition(forward_diamond(sk0,X1),forward_diamond(star(sk0),forward_diamond(domain(X1),forward_box(sk0,c(X1))))) = forward_diamond(star(sk0),forward_diamond(domain(domain(X1)),antidomain(multiplication(sk0,domain(domain(X1)))))),
inference(step,[status(thm)],[t45567,t14867]) ).
cnf(t45569,plain,
addition(forward_diamond(sk0,X1),forward_diamond(star(sk0),forward_diamond(domain(X1),forward_box(sk0,c(X1))))) = forward_diamond(star(sk0),forward_diamond(domain(X1),antidomain(multiplication(sk0,domain(domain(X1)))))),
inference(step,[status(thm)],[t45568,t5630]) ).
cnf(t45570,plain,
addition(forward_diamond(sk0,X1),forward_diamond(star(sk0),forward_diamond(domain(X1),forward_box(sk0,c(X1))))) = forward_diamond(star(sk0),forward_diamond(domain(X1),c(multiplication(sk0,domain(domain(X1)))))),
inference(step,[status(thm)],[t45569,t5571]) ).
cnf(t45571,plain,
addition(forward_diamond(sk0,X1),forward_diamond(star(sk0),forward_diamond(domain(X1),forward_box(sk0,c(X1))))) = forward_diamond(star(sk0),forward_diamond(domain(X1),forward_box(sk0,c(domain(X1))))),
inference(step,[status(thm)],[t45570,t6077]) ).
cnf(t45572,plain,
addition(forward_diamond(sk0,X1),forward_diamond(star(sk0),forward_diamond(domain(X1),forward_box(sk0,c(X1))))) = forward_diamond(star(sk0),forward_diamond(domain(X1),forward_box(sk0,c(X1)))),
inference(step,[status(thm)],[t45571,t5658]) ).
cnf(t23589,plain,
addition(forward_diamond(sk0,X1),forward_diamond(star(sk0),forward_diamond(domain(X1),forward_box(sk0,c(X1))))) = forward_diamond(star(sk0),forward_diamond(domain(X1),forward_box(sk0,c(X1)))),
inference(orient,[status(thm)],[t45572]) ).
cnf(t2744,plain,
forward_diamond(addition(X1,antidomain(domain(X2))),X2) = domain(multiplication(X1,domain(X2))),
inference(cp,[status(thm)],[t157,t2712]) ).
cnf(t44622,plain,
forward_diamond(addition(X1,c(X2)),X2) = domain(multiplication(X1,domain(X2))),
inference(step,[status(thm)],[t2744,t60]) ).
cnf(t44623,plain,
forward_diamond(addition(X1,c(X2)),X2) = forward_diamond(X1,X2),
inference(step,[status(thm)],[t44622,t157]) ).
cnf(t3844,plain,
forward_diamond(addition(X1,c(X2)),X2) = forward_diamond(X1,X2),
inference(orient,[status(thm)],[t44623]) ).
cnf(t317,plain,
one = addition(c(X1),antidomain(antidomain(X1))),
inference(cp,[status(thm)],[t127,t314]) ).
cnf(t44417,plain,
one = addition(c(X1),domain(X1)),
inference(step,[status(thm)],[t317,t49]) ).
cnf(t44418,plain,
one = addition(domain(X1),c(X1)),
inference(step,[status(thm)],[t44417,t110]) ).
cnf(t625,plain,
addition(domain(X1),c(X1)) = one,
inference(orient,[status(thm)],[t44418]) ).
cnf(t3845,plain,
forward_diamond(domain(X1),X1) = forward_diamond(one,X1),
inference(cp,[status(thm)],[t3844,t625]) ).
cnf(t3865,plain,
forward_diamond(domain(X1),X1) = forward_diamond(one,X1),
inference(orient,[status(thm)],[t3845]) ).
cnf(t3881,plain,
forward_box(domain(c(X1)),X1) = c(forward_diamond(one,c(X1))),
inference(cp,[status(thm)],[t222,t3865]) ).
cnf(t44626,plain,
forward_box(forward_box(X1,zero),X1) = c(forward_diamond(one,c(X1))),
inference(step,[status(thm)],[t3881,t423]) ).
cnf(t315,plain,
c(antidomain(X1)) = domain(domain(X1)),
inference(cp,[status(thm)],[t314,t49]) ).
cnf(t44375,plain,
c(antidomain(X1)) = forward_diamond(one,X1),
inference(step,[status(thm)],[t315,t345]) ).
cnf(t380,plain,
c(antidomain(X1)) = forward_diamond(one,X1),
inference(orient,[status(thm)],[t44375]) ).
cnf(t381,plain,
forward_diamond(one,c(X1)) = c(forward_diamond(one,X1)),
inference(cp,[status(thm)],[t380,t346]) ).
cnf(t674,plain,
c(forward_diamond(one,X1)) = forward_diamond(one,c(X1)),
inference(orient,[status(thm)],[t381]) ).
cnf(t44627,plain,
forward_box(forward_box(X1,zero),X1) = forward_diamond(one,c(c(X1))),
inference(step,[status(thm)],[t44626,t674]) ).
cnf(t675,plain,
forward_diamond(one,c(c(X1))) = forward_box(one,X1),
inference(cp,[status(thm)],[t674,t222]) ).
cnf(t964,plain,
forward_diamond(one,c(c(X1))) = forward_box(one,X1),
inference(orient,[status(thm)],[t675]) ).
cnf(t44628,plain,
forward_box(forward_box(X1,zero),X1) = forward_box(one,X1),
inference(step,[status(thm)],[t44627,t964]) ).
cnf(t3965,plain,
forward_box(forward_box(X1,zero),X1) = forward_box(one,X1),
inference(orient,[status(thm)],[t44628]) ).
cnf(t44859,plain,
forward_box(c(X1),X1) = forward_box(one,X1),
inference(step,[status(thm)],[t3965,t5657]) ).
cnf(t5665,plain,
forward_box(c(X1),X1) = forward_box(one,X1),
inference(rw,[status(thm)],[t44859]) ).
cnf(t353,plain,
c(domain(X1)) = antidomain(forward_diamond(one,X1)),
inference(cp,[status(thm)],[t60,t345]) ).
cnf(t44390,plain,
forward_box(X1,zero) = antidomain(forward_diamond(one,X1)),
inference(step,[status(thm)],[t353,t424]) ).
cnf(t468,plain,
antidomain(forward_diamond(one,X1)) = forward_box(X1,zero),
inference(orient,[status(thm)],[t44390]) ).
cnf(t340,plain,
c(c(X1)) = domain(domain(domain(X1))),
inference(cp,[status(thm)],[t314,t337]) ).
cnf(t44388,plain,
c(c(X1)) = forward_diamond(one,domain(X1)),
inference(step,[status(thm)],[t340,t345]) ).
cnf(t457,plain,
forward_diamond(one,domain(X1)) = c(c(X1)),
inference(orient,[status(thm)],[t44388]) ).
cnf(t458,plain,
c(c(c(X1))) = forward_diamond(one,forward_box(X1,zero)),
inference(cp,[status(thm)],[t457,t423]) ).
cnf(t1379,plain,
forward_diamond(one,forward_box(X1,zero)) = c(c(c(X1))),
inference(orient,[status(thm)],[t458]) ).
cnf(t1384,plain,
forward_box(forward_box(X1,zero),zero) = antidomain(c(c(c(X1)))),
inference(cp,[status(thm)],[t468,t1379]) ).
cnf(t44477,plain,
forward_box(forward_box(X1,zero),zero) = forward_diamond(one,c(c(X1))),
inference(step,[status(thm)],[t1384,t346]) ).
cnf(t44478,plain,
forward_box(forward_box(X1,zero),zero) = forward_box(one,X1),
inference(step,[status(thm)],[t44477,t964]) ).
cnf(t1385,plain,
forward_box(forward_box(X1,zero),zero) = forward_box(one,X1),
inference(orient,[status(thm)],[t44478]) ).
cnf(t44861,plain,
c(forward_box(X1,zero)) = forward_box(one,X1),
inference(step,[status(thm)],[t1385,t5657]) ).
cnf(t434,plain,
forward_box(c(X1),zero) = c(forward_box(X1,zero)),
inference(cp,[status(thm)],[t424,t423]) ).
cnf(t715,plain,
c(forward_box(X1,zero)) = forward_box(c(X1),zero),
inference(orient,[status(thm)],[t434]) ).
cnf(t44862,plain,
forward_box(c(X1),zero) = forward_box(one,X1),
inference(step,[status(thm)],[t44861,t715]) ).
cnf(t44863,plain,
c(c(X1)) = forward_box(one,X1),
inference(step,[status(thm)],[t44862,t5657]) ).
cnf(t5667,plain,
c(c(X1)) = forward_box(one,X1),
inference(rw,[status(thm)],[t44863]) ).
cnf(t44874,plain,
domain(X1) = forward_box(one,X1),
inference(step,[status(thm)],[t5667,t5669]) ).
cnf(t5701,plain,
forward_box(one,X1) = domain(X1),
inference(orient,[status(thm)],[t44874]) ).
cnf(t44887,plain,
forward_box(c(X1),X1) = domain(X1),
inference(step,[status(thm)],[t5665,t5701]) ).
cnf(t5746,plain,
forward_box(c(X1),X1) = domain(X1),
inference(orient,[status(thm)],[t44887]) ).
cnf(t5747,plain,
domain(c(X1)) = forward_box(domain(X1),c(X1)),
inference(cp,[status(thm)],[t5746,t5669]) ).
cnf(t44852,plain,
domain(c(X1)) = c(X1),
inference(step,[status(thm)],[t423,t5657]) ).
cnf(t5660,plain,
domain(c(X1)) = c(X1),
inference(orient,[status(thm)],[t44852]) ).
cnf(t44908,plain,
c(X1) = forward_box(domain(X1),c(X1)),
inference(step,[status(thm)],[t5747,t5660]) ).
cnf(t5915,plain,
forward_box(domain(X1),c(X1)) = c(X1),
inference(orient,[status(thm)],[t44908]) ).
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(t19,plain,
c(backward_diamond(X1,c(X2))) = backward_box(X1,X2),
inference(equality_encoding,[status(esa)],[c26]) ).
cnf(t224,plain,
c(backward_diamond(X1,c(X2))) = backward_box(X1,X2),
inference(orient,[status(thm)],[t19]) ).
cnf(t5673,plain,
domain(backward_diamond(X1,c(X2))) = c(backward_box(X1,X2)),
inference(cp,[status(thm)],[t5669,t224]) ).
cnf(t6326,plain,
domain(backward_diamond(X1,c(X2))) = c(backward_box(X1,X2)),
inference(orient,[status(thm)],[t5673]) ).
cnf(t6346,plain,
c(backward_diamond(X1,c(X2))) = forward_box(c(backward_box(X1,X2)),c(backward_diamond(X1,c(X2)))),
inference(cp,[status(thm)],[t5915,t6326]) ).
cnf(t44927,plain,
backward_box(X1,X2) = forward_box(c(backward_box(X1,X2)),c(backward_diamond(X1,c(X2)))),
inference(step,[status(thm)],[t6346,t224]) ).
cnf(t44928,plain,
backward_box(X1,X2) = forward_box(c(backward_box(X1,X2)),backward_box(X1,X2)),
inference(step,[status(thm)],[t44927,t224]) ).
cnf(t44929,plain,
backward_box(X1,X2) = domain(backward_box(X1,X2)),
inference(step,[status(thm)],[t44928,t5746]) ).
cnf(t6361,plain,
domain(backward_box(X1,X2)) = backward_box(X1,X2),
inference(orient,[status(thm)],[t44929]) ).
cnf(t6377,plain,
forward_diamond(X1,backward_box(X2,X3)) = domain(multiplication(X1,backward_box(X2,X3))),
inference(cp,[status(thm)],[t157,t6361]) ).
cnf(t15661,plain,
domain(multiplication(X1,backward_box(X2,X3))) = forward_diamond(X1,backward_box(X2,X3)),
inference(orient,[status(thm)],[t6377]) ).
cnf(t66,plain,
multiplication(X1,addition(one,X2)) = addition(X1,multiplication(X1,X2)),
inference(cp,[status(thm)],[t65,t41]) ).
cnf(t1650,plain,
addition(X1,multiplication(X1,X2)) = multiplication(X1,addition(one,X2)),
inference(orient,[status(thm)],[t66]) ).
cnf(t2774,plain,
multiplication(domain(X1),addition(one,X1)) = addition(domain(X1),X1),
inference(cp,[status(thm)],[t1650,t2755]) ).
cnf(t45081,plain,
multiplication(domain(X1),addition(one,X1)) = addition(X1,domain(X1)),
inference(step,[status(thm)],[t2774,t110]) ).
cnf(t10521,plain,
multiplication(domain(X1),addition(one,X1)) = addition(X1,domain(X1)),
inference(orient,[status(thm)],[t45081]) ).
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(t44324,plain,
addition(antidomain(multiplication(X1,X2)),antidomain(multiplication(X1,domain(X2)))) = antidomain(multiplication(X1,antidomain(antidomain(X2)))),
inference(step,[status(thm)],[t34,t49]) ).
cnf(t44325,plain,
addition(antidomain(multiplication(X1,X2)),antidomain(multiplication(X1,domain(X2)))) = antidomain(multiplication(X1,domain(X2))),
inference(step,[status(thm)],[t44324,t49]) ).
cnf(t55,plain,
addition(antidomain(multiplication(X1,X2)),antidomain(multiplication(X1,domain(X2)))) = antidomain(multiplication(X1,domain(X2))),
inference(orient,[status(thm)],[t44325]) ).
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(t69,plain,
multiplication(X1,coantidomain(X1)) = zero,
inference(orient,[status(thm)],[t12]) ).
cnf(t75,plain,
antidomain(multiplication(X1,domain(coantidomain(X1)))) = addition(antidomain(zero),antidomain(multiplication(X1,domain(coantidomain(X1))))),
inference(cp,[status(thm)],[t55,t69]) ).
cnf(t44674,plain,
antidomain(multiplication(X1,domain(coantidomain(X1)))) = addition(one,antidomain(multiplication(X1,domain(coantidomain(X1))))),
inference(step,[status(thm)],[t75,t263]) ).
cnf(t26,plain,
ifeq(leq(X1,X2),true,addition(X1,X2),X2) = X2,
inference(equality_encoding,[status(esa)],[c11]) ).
cnf(t46,plain,
ifeq(leq(X1,X2),true,addition(X1,X2),X2) = X2,
inference(orient,[status(thm)],[t26]) ).
cnf(t25,plain,
ifeq(addition(X1,X2),X2,leq(X1,X2),true) = true,
inference(equality_encoding,[status(esa)],[c12]) ).
cnf(t214,plain,
ifeq(addition(X1,X2),X2,leq(X1,X2),true) = true,
inference(orient,[status(thm)],[t25]) ).
cnf(t798,plain,
true = ifeq(addition(X1,X2),addition(X1,X2),leq(X1,addition(X1,X2)),true),
inference(cp,[status(thm)],[t214,t790]) ).
cnf(t16,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t45,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t16]) ).
cnf(t44440,plain,
true = leq(X1,addition(X1,X2)),
inference(step,[status(thm)],[t798,t45]) ).
cnf(t829,plain,
leq(X1,addition(X1,X2)) = true,
inference(orient,[status(thm)],[t44440]) ).
cnf(t836,plain,
true = leq(X1,addition(X2,X1)),
inference(cp,[status(thm)],[t829,t110]) ).
cnf(t905,plain,
leq(X1,addition(X2,X1)) = true,
inference(orient,[status(thm)],[t836]) ).
cnf(t912,plain,
true = leq(antidomain(X1),one),
inference(cp,[status(thm)],[t905,t127]) ).
cnf(t925,plain,
leq(antidomain(X1),one) = true,
inference(orient,[status(thm)],[t912]) ).
cnf(t929,plain,
one = ifeq(true,true,addition(antidomain(X1),one),one),
inference(cp,[status(thm)],[t46,t925]) ).
cnf(t44443,plain,
one = addition(antidomain(X1),one),
inference(step,[status(thm)],[t929,t45]) ).
cnf(t44444,plain,
one = addition(one,antidomain(X1)),
inference(step,[status(thm)],[t44443,t110]) ).
cnf(t935,plain,
addition(one,antidomain(X1)) = one,
inference(orient,[status(thm)],[t44444]) ).
cnf(t44675,plain,
antidomain(multiplication(X1,domain(coantidomain(X1)))) = one,
inference(step,[status(thm)],[t44674,t935]) ).
cnf(t4505,plain,
antidomain(multiplication(X1,domain(coantidomain(X1)))) = one,
inference(orient,[status(thm)],[t44675]) ).
cnf(t4532,plain,
zero = multiplication(one,multiplication(X1,domain(coantidomain(X1)))),
inference(cp,[status(thm)],[t80,t4505]) ).
cnf(t44678,plain,
zero = multiplication(X1,domain(coantidomain(X1))),
inference(step,[status(thm)],[t4532,t42]) ).
cnf(t4549,plain,
multiplication(X1,domain(coantidomain(X1))) = zero,
inference(orient,[status(thm)],[t44678]) ).
cnf(t4558,plain,
multiplication(X1,addition(domain(coantidomain(X1)),X2)) = addition(zero,multiplication(X1,X2)),
inference(cp,[status(thm)],[t65,t4549]) ).
cnf(t45334,plain,
multiplication(X1,addition(domain(coantidomain(X1)),X2)) = multiplication(X1,X2),
inference(step,[status(thm)],[t4558,t289]) ).
cnf(t18239,plain,
multiplication(X1,addition(domain(coantidomain(X1)),X2)) = multiplication(X1,X2),
inference(orient,[status(thm)],[t45334]) ).
cnf(t18245,plain,
multiplication(X1,c(coantidomain(X1))) = multiplication(X1,one),
inference(cp,[status(thm)],[t18239,t625]) ).
cnf(t45335,plain,
multiplication(X1,c(coantidomain(X1))) = X1,
inference(step,[status(thm)],[t18245,t41]) ).
cnf(t18286,plain,
multiplication(X1,c(coantidomain(X1))) = X1,
inference(orient,[status(thm)],[t45335]) ).
cnf(t18327,plain,
forward_box(X1,coantidomain(X1)) = c(X1),
inference(cp,[status(thm)],[t5960,t18286]) ).
cnf(t18333,plain,
forward_box(X1,coantidomain(X1)) = c(X1),
inference(orient,[status(thm)],[t18327]) ).
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(t179,plain,
coantidomain(coantidomain(X1)) = codomain(X1),
inference(orient,[status(thm)],[t11]) ).
cnf(t180,plain,
codomain(coantidomain(X1)) = coantidomain(codomain(X1)),
inference(cp,[status(thm)],[t179,t179]) ).
cnf(t371,plain,
coantidomain(codomain(X1)) = codomain(coantidomain(X1)),
inference(orient,[status(thm)],[t180]) ).
cnf(t90,plain,
multiplication(addition(X1,X2),coantidomain(X1)) = addition(zero,multiplication(X2,coantidomain(X1))),
inference(cp,[status(thm)],[t89,t69]) ).
cnf(t44930,plain,
multiplication(addition(X1,X2),coantidomain(X1)) = multiplication(X2,coantidomain(X1)),
inference(step,[status(thm)],[t90,t289]) ).
cnf(t6393,plain,
multiplication(addition(X1,X2),coantidomain(X1)) = multiplication(X2,coantidomain(X1)),
inference(orient,[status(thm)],[t44930]) ).
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(t18,plain,
addition(coantidomain(coantidomain(X1)),coantidomain(X1)) = one,
inference(equality_encoding,[status(esa)],[c19]) ).
cnf(t44329,plain,
addition(coantidomain(X1),coantidomain(coantidomain(X1))) = one,
inference(step,[status(thm)],[t18,t110]) ).
cnf(t147,plain,
addition(coantidomain(X1),coantidomain(coantidomain(X1))) = one,
inference(orient,[status(thm)],[t44329]) ).
cnf(t44333,plain,
addition(coantidomain(X1),codomain(X1)) = one,
inference(step,[status(thm)],[t147,t179]) ).
cnf(t182,plain,
addition(coantidomain(X1),codomain(X1)) = one,
inference(rw,[status(thm)],[t44333]) ).
cnf(t44394,plain,
addition(codomain(X1),coantidomain(X1)) = one,
inference(step,[status(thm)],[t182,t110]) ).
cnf(t567,plain,
addition(codomain(X1),coantidomain(X1)) = one,
inference(orient,[status(thm)],[t44394]) ).
cnf(t6397,plain,
multiplication(coantidomain(X1),coantidomain(codomain(X1))) = multiplication(one,coantidomain(codomain(X1))),
inference(cp,[status(thm)],[t6393,t567]) ).
cnf(t44931,plain,
multiplication(coantidomain(X1),codomain(coantidomain(X1))) = multiplication(one,coantidomain(codomain(X1))),
inference(step,[status(thm)],[t6397,t371]) ).
cnf(t73,plain,
multiplication(X1,addition(X2,coantidomain(X1))) = addition(multiplication(X1,X2),zero),
inference(cp,[status(thm)],[t65,t69]) ).
cnf(t44563,plain,
multiplication(X1,addition(X2,coantidomain(X1))) = multiplication(X1,X2),
inference(step,[status(thm)],[t73,t44]) ).
cnf(t2563,plain,
multiplication(X1,addition(X2,coantidomain(X1))) = multiplication(X1,X2),
inference(orient,[status(thm)],[t44563]) ).
cnf(t2565,plain,
multiplication(X1,codomain(X1)) = multiplication(X1,one),
inference(cp,[status(thm)],[t2563,t567]) ).
cnf(t44564,plain,
multiplication(X1,codomain(X1)) = X1,
inference(step,[status(thm)],[t2565,t41]) ).
cnf(t2588,plain,
multiplication(X1,codomain(X1)) = X1,
inference(orient,[status(thm)],[t44564]) ).
cnf(t44932,plain,
coantidomain(X1) = multiplication(one,coantidomain(codomain(X1))),
inference(step,[status(thm)],[t44931,t2588]) ).
cnf(t44933,plain,
coantidomain(X1) = coantidomain(codomain(X1)),
inference(step,[status(thm)],[t44932,t42]) ).
cnf(t44934,plain,
coantidomain(X1) = codomain(coantidomain(X1)),
inference(step,[status(thm)],[t44933,t371]) ).
cnf(t6420,plain,
codomain(coantidomain(X1)) = coantidomain(X1),
inference(orient,[status(thm)],[t44934]) ).
cnf(t44935,plain,
coantidomain(codomain(X1)) = coantidomain(X1),
inference(step,[status(thm)],[t371,t6420]) ).
cnf(t6421,plain,
coantidomain(codomain(X1)) = coantidomain(X1),
inference(orient,[status(thm)],[t44935]) ).
cnf(t18336,plain,
c(codomain(X1)) = forward_box(codomain(X1),coantidomain(X1)),
inference(cp,[status(thm)],[t18333,t6421]) ).
cnf(t287,plain,
backward_box(X1,zero) = c(backward_diamond(X1,one)),
inference(cp,[status(thm)],[t224,t286]) ).
cnf(t414,plain,
c(backward_diamond(X1,one)) = backward_box(X1,zero),
inference(orient,[status(thm)],[t287]) ).
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(t21,plain,
codomain(multiplication(codomain(X1),X2)) = backward_diamond(X2,X1),
inference(equality_encoding,[status(esa)],[c24]) ).
cnf(t228,plain,
codomain(multiplication(codomain(X1),X2)) = backward_diamond(X2,X1),
inference(orient,[status(thm)],[t21]) ).
cnf(t71,plain,
zero = coantidomain(one),
inference(cp,[status(thm)],[t69,t42]) ).
cnf(t234,plain,
coantidomain(one) = zero,
inference(orient,[status(thm)],[t71]) ).
cnf(t573,plain,
one = addition(codomain(one),zero),
inference(cp,[status(thm)],[t567,t234]) ).
cnf(t44395,plain,
one = codomain(one),
inference(step,[status(thm)],[t573,t44]) ).
cnf(t577,plain,
codomain(one) = one,
inference(orient,[status(thm)],[t44395]) ).
cnf(t582,plain,
backward_diamond(X1,one) = codomain(multiplication(one,X1)),
inference(cp,[status(thm)],[t228,t577]) ).
cnf(t44413,plain,
backward_diamond(X1,one) = codomain(X1),
inference(step,[status(thm)],[t582,t42]) ).
cnf(t600,plain,
backward_diamond(X1,one) = codomain(X1),
inference(orient,[status(thm)],[t44413]) ).
cnf(t44414,plain,
c(codomain(X1)) = backward_box(X1,zero),
inference(step,[status(thm)],[t414,t600]) ).
cnf(t601,plain,
c(codomain(X1)) = backward_box(X1,zero),
inference(rw,[status(thm)],[t44414]) ).
cnf(t602,plain,
c(codomain(X1)) = backward_box(X1,zero),
inference(orient,[status(thm)],[t601]) ).
cnf(t45336,plain,
backward_box(X1,zero) = forward_box(codomain(X1),coantidomain(X1)),
inference(step,[status(thm)],[t18336,t602]) ).
cnf(t2776,plain,
multiplication(addition(X1,domain(X2)),X2) = addition(multiplication(X1,X2),X2),
inference(cp,[status(thm)],[t89,t2755]) ).
cnf(t45255,plain,
multiplication(addition(X1,domain(X2)),X2) = addition(X2,multiplication(X1,X2)),
inference(step,[status(thm)],[t2776,t110]) ).
cnf(t45256,plain,
multiplication(addition(X1,domain(X2)),X2) = multiplication(addition(one,X1),X2),
inference(step,[status(thm)],[t45255,t2076]) ).
cnf(t14596,plain,
multiplication(addition(X1,domain(X2)),X2) = multiplication(addition(one,X1),X2),
inference(orient,[status(thm)],[t45256]) ).
cnf(t14647,plain,
forward_box(addition(X1,domain(c(X2))),X2) = c(multiplication(addition(one,X1),c(X2))),
inference(cp,[status(thm)],[t5960,t14596]) ).
cnf(t45279,plain,
forward_box(addition(X1,c(X2)),X2) = c(multiplication(addition(one,X1),c(X2))),
inference(step,[status(thm)],[t14647,t5660]) ).
cnf(t45280,plain,
forward_box(addition(X1,c(X2)),X2) = forward_box(addition(one,X1),X2),
inference(step,[status(thm)],[t45279,t5960]) ).
cnf(t16891,plain,
forward_box(addition(X1,c(X2)),X2) = forward_box(addition(one,X1),X2),
inference(orient,[status(thm)],[t45280]) ).
cnf(t86,plain,
multiplication(antidomain(X1),multiplication(X1,X2)) = multiplication(zero,X2),
inference(cp,[status(thm)],[t62,t80]) ).
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(t108,plain,
multiplication(zero,X1) = zero,
inference(orient,[status(thm)],[t8]) ).
cnf(t44568,plain,
multiplication(antidomain(X1),multiplication(X1,X2)) = zero,
inference(step,[status(thm)],[t86,t108]) ).
cnf(t2651,plain,
multiplication(antidomain(X1),multiplication(X1,X2)) = zero,
inference(orient,[status(thm)],[t44568]) ).
cnf(t2773,plain,
zero = multiplication(antidomain(domain(X1)),X1),
inference(cp,[status(thm)],[t2651,t2755]) ).
cnf(t44572,plain,
zero = multiplication(c(X1),X1),
inference(step,[status(thm)],[t2773,t60]) ).
cnf(t2797,plain,
multiplication(c(X1),X1) = zero,
inference(orient,[status(thm)],[t44572]) ).
cnf(t2813,plain,
multiplication(c(X1),addition(X1,X2)) = addition(zero,multiplication(c(X1),X2)),
inference(cp,[status(thm)],[t65,t2797]) ).
cnf(t45095,plain,
multiplication(c(X1),addition(X1,X2)) = multiplication(c(X1),X2),
inference(step,[status(thm)],[t2813,t289]) ).
cnf(t10795,plain,
multiplication(c(X1),addition(X1,X2)) = multiplication(c(X1),X2),
inference(orient,[status(thm)],[t45095]) ).
cnf(t10816,plain,
multiplication(c(codomain(X1)),coantidomain(X1)) = multiplication(c(codomain(X1)),one),
inference(cp,[status(thm)],[t10795,t567]) ).
cnf(t45099,plain,
multiplication(backward_box(X1,zero),coantidomain(X1)) = multiplication(c(codomain(X1)),one),
inference(step,[status(thm)],[t10816,t602]) ).
cnf(t45100,plain,
multiplication(backward_box(X1,zero),coantidomain(X1)) = c(codomain(X1)),
inference(step,[status(thm)],[t45099,t41]) ).
cnf(t45101,plain,
multiplication(backward_box(X1,zero),coantidomain(X1)) = backward_box(X1,zero),
inference(step,[status(thm)],[t45100,t602]) ).
cnf(t10868,plain,
multiplication(backward_box(X1,zero),coantidomain(X1)) = backward_box(X1,zero),
inference(orient,[status(thm)],[t45101]) ).
cnf(t10879,plain,
multiplication(addition(one,backward_box(X1,zero)),coantidomain(X1)) = addition(coantidomain(X1),backward_box(X1,zero)),
inference(cp,[status(thm)],[t2076,t10868]) ).
cnf(t812,plain,
one = addition(one,c(X1)),
inference(cp,[status(thm)],[t806,t314]) ).
cnf(t817,plain,
addition(one,c(X1)) = one,
inference(orient,[status(thm)],[t812]) ).
cnf(t819,plain,
one = addition(one,backward_box(X1,zero)),
inference(cp,[status(thm)],[t817,t602]) ).
cnf(t892,plain,
addition(one,backward_box(X1,zero)) = one,
inference(orient,[status(thm)],[t819]) ).
cnf(t45102,plain,
multiplication(one,coantidomain(X1)) = addition(coantidomain(X1),backward_box(X1,zero)),
inference(step,[status(thm)],[t10879,t892]) ).
cnf(t45103,plain,
coantidomain(X1) = addition(coantidomain(X1),backward_box(X1,zero)),
inference(step,[status(thm)],[t45102,t42]) ).
cnf(t10895,plain,
addition(coantidomain(X1),backward_box(X1,zero)) = coantidomain(X1),
inference(orient,[status(thm)],[t45103]) ).
cnf(t10898,plain,
coantidomain(coantidomain(X1)) = addition(codomain(X1),backward_box(coantidomain(X1),zero)),
inference(cp,[status(thm)],[t10895,t179]) ).
cnf(t45112,plain,
codomain(X1) = addition(codomain(X1),backward_box(coantidomain(X1),zero)),
inference(step,[status(thm)],[t10898,t179]) ).
cnf(t6430,plain,
backward_box(coantidomain(X1),zero) = c(coantidomain(X1)),
inference(cp,[status(thm)],[t602,t6420]) ).
cnf(t6473,plain,
backward_box(coantidomain(X1),zero) = c(coantidomain(X1)),
inference(orient,[status(thm)],[t6430]) ).
cnf(t45113,plain,
codomain(X1) = addition(codomain(X1),c(coantidomain(X1))),
inference(step,[status(thm)],[t45112,t6473]) ).
cnf(t11074,plain,
addition(codomain(X1),c(coantidomain(X1))) = codomain(X1),
inference(orient,[status(thm)],[t45113]) ).
cnf(t16893,plain,
forward_box(addition(one,codomain(X1)),coantidomain(X1)) = forward_box(codomain(X1),coantidomain(X1)),
inference(cp,[status(thm)],[t16891,t11074]) ).
cnf(t792,plain,
addition(codomain(X1),coantidomain(X1)) = addition(codomain(X1),one),
inference(cp,[status(thm)],[t790,t567]) ).
cnf(t44436,plain,
one = addition(codomain(X1),one),
inference(step,[status(thm)],[t792,t567]) ).
cnf(t44437,plain,
one = addition(one,codomain(X1)),
inference(step,[status(thm)],[t44436,t110]) ).
cnf(t799,plain,
addition(one,codomain(X1)) = one,
inference(orient,[status(thm)],[t44437]) ).
cnf(t45281,plain,
forward_box(one,coantidomain(X1)) = forward_box(codomain(X1),coantidomain(X1)),
inference(step,[status(thm)],[t16893,t799]) ).
cnf(t45282,plain,
domain(coantidomain(X1)) = forward_box(codomain(X1),coantidomain(X1)),
inference(step,[status(thm)],[t45281,t5701]) ).
cnf(t16916,plain,
forward_box(codomain(X1),coantidomain(X1)) = domain(coantidomain(X1)),
inference(orient,[status(thm)],[t45282]) ).
cnf(t45337,plain,
backward_box(X1,zero) = domain(coantidomain(X1)),
inference(step,[status(thm)],[t45336,t16916]) ).
cnf(t18340,plain,
domain(coantidomain(X1)) = backward_box(X1,zero),
inference(orient,[status(thm)],[t45337]) ).
cnf(t18362,plain,
addition(coantidomain(X1),domain(coantidomain(X1))) = multiplication(backward_box(X1,zero),addition(one,coantidomain(X1))),
inference(cp,[status(thm)],[t10521,t18340]) ).
cnf(t45356,plain,
addition(coantidomain(X1),backward_box(X1,zero)) = multiplication(backward_box(X1,zero),addition(one,coantidomain(X1))),
inference(step,[status(thm)],[t18362,t18340]) ).
cnf(t45357,plain,
coantidomain(X1) = multiplication(backward_box(X1,zero),addition(one,coantidomain(X1))),
inference(step,[status(thm)],[t45356,t10895]) ).
cnf(t911,plain,
true = leq(coantidomain(X1),one),
inference(cp,[status(thm)],[t905,t567]) ).
cnf(t921,plain,
leq(coantidomain(X1),one) = true,
inference(orient,[status(thm)],[t911]) ).
cnf(t923,plain,
one = ifeq(true,true,addition(coantidomain(X1),one),one),
inference(cp,[status(thm)],[t46,t921]) ).
cnf(t44441,plain,
one = addition(coantidomain(X1),one),
inference(step,[status(thm)],[t923,t45]) ).
cnf(t44442,plain,
one = addition(one,coantidomain(X1)),
inference(step,[status(thm)],[t44441,t110]) ).
cnf(t931,plain,
addition(one,coantidomain(X1)) = one,
inference(orient,[status(thm)],[t44442]) ).
cnf(t45358,plain,
coantidomain(X1) = multiplication(backward_box(X1,zero),one),
inference(step,[status(thm)],[t45357,t931]) ).
cnf(t45359,plain,
coantidomain(X1) = backward_box(X1,zero),
inference(step,[status(thm)],[t45358,t41]) ).
cnf(t18474,plain,
backward_box(X1,zero) = coantidomain(X1),
inference(orient,[status(thm)],[t45359]) ).
cnf(t18503,plain,
forward_diamond(X1,backward_box(X2,zero)) = domain(multiplication(X1,coantidomain(X2))),
inference(cp,[status(thm)],[t15661,t18474]) ).
cnf(t45507,plain,
forward_diamond(X1,coantidomain(X2)) = domain(multiplication(X1,coantidomain(X2))),
inference(step,[status(thm)],[t18503,t18474]) ).
cnf(t19881,plain,
domain(multiplication(X1,coantidomain(X2))) = forward_diamond(X1,coantidomain(X2)),
inference(orient,[status(thm)],[t45507]) ).
cnf(t94,plain,
multiplication(addition(X1,X2),coantidomain(X2)) = addition(multiplication(X1,coantidomain(X2)),zero),
inference(cp,[status(thm)],[t89,t69]) ).
cnf(t45008,plain,
multiplication(addition(X1,X2),coantidomain(X2)) = multiplication(X1,coantidomain(X2)),
inference(step,[status(thm)],[t94,t44]) ).
cnf(t8211,plain,
multiplication(addition(X1,X2),coantidomain(X2)) = multiplication(X1,coantidomain(X2)),
inference(orient,[status(thm)],[t45008]) ).
cnf(t8214,plain,
multiplication(X1,coantidomain(addition(X1,X2))) = multiplication(addition(X1,X2),coantidomain(addition(X1,X2))),
inference(cp,[status(thm)],[t8211,t790]) ).
cnf(t45009,plain,
multiplication(X1,coantidomain(addition(X1,X2))) = zero,
inference(step,[status(thm)],[t8214,t69]) ).
cnf(t8252,plain,
multiplication(X1,coantidomain(addition(X1,X2))) = zero,
inference(orient,[status(thm)],[t45009]) ).
cnf(t19883,plain,
forward_diamond(X1,coantidomain(addition(X1,X2))) = domain(zero),
inference(cp,[status(thm)],[t19881,t8252]) ).
cnf(t45508,plain,
forward_diamond(X1,coantidomain(addition(X1,X2))) = zero,
inference(step,[status(thm)],[t19883,t267]) ).
cnf(t20007,plain,
forward_diamond(X1,coantidomain(addition(X1,X2))) = zero,
inference(orient,[status(thm)],[t45508]) ).
cnf(t20010,plain,
zero = forward_diamond(domain(sk1),coantidomain(forward_diamond(sk0,sk1))),
inference(cp,[status(thm)],[t20007,t7439]) ).
cnf(t23748,plain,
forward_diamond(domain(sk1),coantidomain(forward_diamond(sk0,sk1))) = zero,
inference(orient,[status(thm)],[t20010]) ).
cnf(t5972,plain,
forward_box(X1,codomain(X2)) = c(multiplication(X1,backward_box(X2,zero))),
inference(cp,[status(thm)],[t5960,t602]) ).
cnf(t11941,plain,
c(multiplication(X1,backward_box(X2,zero))) = forward_box(X1,codomain(X2)),
inference(orient,[status(thm)],[t5972]) ).
cnf(t72,plain,
multiplication(X1,addition(coantidomain(X1),X2)) = addition(zero,multiplication(X1,X2)),
inference(cp,[status(thm)],[t65,t69]) ).
cnf(t44598,plain,
multiplication(X1,addition(coantidomain(X1),X2)) = multiplication(X1,X2),
inference(step,[status(thm)],[t72,t289]) ).
cnf(t3415,plain,
multiplication(X1,addition(coantidomain(X1),X2)) = multiplication(X1,X2),
inference(orient,[status(thm)],[t44598]) ).
cnf(t10914,plain,
multiplication(X1,backward_box(X1,zero)) = multiplication(X1,coantidomain(X1)),
inference(cp,[status(thm)],[t3415,t10895]) ).
cnf(t45104,plain,
multiplication(X1,backward_box(X1,zero)) = zero,
inference(step,[status(thm)],[t10914,t69]) ).
cnf(t10916,plain,
multiplication(X1,backward_box(X1,zero)) = zero,
inference(orient,[status(thm)],[t45104]) ).
cnf(t11942,plain,
forward_box(X1,codomain(X1)) = c(zero),
inference(cp,[status(thm)],[t11941,t10916]) ).
cnf(t45163,plain,
forward_box(X1,codomain(X1)) = one,
inference(step,[status(thm)],[t11942,t286]) ).
cnf(t12062,plain,
forward_box(X1,codomain(X1)) = one,
inference(orient,[status(thm)],[t45163]) ).
cnf(t12063,plain,
one = forward_box(multiplication(codomain(X1),X2),backward_diamond(X2,X1)),
inference(cp,[status(thm)],[t12062,t228]) ).
cnf(t38926,plain,
forward_box(multiplication(codomain(X1),X2),backward_diamond(X2,X1)) = one,
inference(orient,[status(thm)],[t12063]) ).
cnf(t6423,plain,
coantidomain(coantidomain(X1)) = codomain(codomain(X1)),
inference(cp,[status(thm)],[t6420,t179]) ).
cnf(t44942,plain,
codomain(X1) = codomain(codomain(X1)),
inference(step,[status(thm)],[t6423,t179]) ).
cnf(t230,plain,
backward_diamond(one,X1) = codomain(codomain(X1)),
inference(cp,[status(thm)],[t228,t41]) ).
cnf(t374,plain,
codomain(codomain(X1)) = backward_diamond(one,X1),
inference(orient,[status(thm)],[t230]) ).
cnf(t44943,plain,
codomain(X1) = backward_diamond(one,X1),
inference(step,[status(thm)],[t44942,t374]) ).
cnf(t6442,plain,
backward_diamond(one,X1) = codomain(X1),
inference(orient,[status(thm)],[t44943]) ).
cnf(t6446,plain,
backward_box(one,X1) = c(codomain(c(X1))),
inference(cp,[status(thm)],[t224,t6442]) ).
cnf(t44960,plain,
backward_box(one,X1) = backward_box(c(X1),zero),
inference(step,[status(thm)],[t6446,t602]) ).
cnf(t6476,plain,
backward_box(c(X1),zero) = backward_box(one,X1),
inference(orient,[status(thm)],[t44960]) ).
cnf(t6487,plain,
backward_box(one,backward_diamond(X1,c(X2))) = backward_box(backward_box(X1,X2),zero),
inference(cp,[status(thm)],[t6476,t224]) ).
cnf(t15986,plain,
backward_box(one,backward_diamond(X1,c(X2))) = backward_box(backward_box(X1,X2),zero),
inference(orient,[status(thm)],[t6487]) ).
cnf(t45370,plain,
backward_box(one,backward_diamond(X1,c(X2))) = coantidomain(backward_box(X1,X2)),
inference(step,[status(thm)],[t15986,t18474]) ).
cnf(t18485,plain,
backward_box(one,backward_diamond(X1,c(X2))) = coantidomain(backward_box(X1,X2)),
inference(orient,[status(thm)],[t45370]) ).
cnf(t6486,plain,
backward_box(one,codomain(X1)) = backward_box(backward_box(X1,zero),zero),
inference(cp,[status(thm)],[t6476,t602]) ).
cnf(t6868,plain,
backward_box(backward_box(X1,zero),zero) = backward_box(one,codomain(X1)),
inference(orient,[status(thm)],[t6486]) ).
cnf(t45398,plain,
coantidomain(backward_box(X1,zero)) = backward_box(one,codomain(X1)),
inference(step,[status(thm)],[t6868,t18474]) ).
cnf(t45399,plain,
coantidomain(coantidomain(X1)) = backward_box(one,codomain(X1)),
inference(step,[status(thm)],[t45398,t18474]) ).
cnf(t45400,plain,
codomain(X1) = backward_box(one,codomain(X1)),
inference(step,[status(thm)],[t45399,t179]) ).
cnf(t18514,plain,
codomain(X1) = backward_box(one,codomain(X1)),
inference(rw,[status(thm)],[t45400]) ).
cnf(t18772,plain,
backward_box(one,codomain(X1)) = codomain(X1),
inference(orient,[status(thm)],[t18514]) ).
cnf(t44944,plain,
codomain(codomain(X1)) = codomain(X1),
inference(step,[status(thm)],[t374,t6442]) ).
cnf(t6443,plain,
codomain(codomain(X1)) = codomain(X1),
inference(orient,[status(thm)],[t44944]) ).
cnf(t6436,plain,
backward_diamond(X1,coantidomain(X2)) = codomain(multiplication(coantidomain(X2),X1)),
inference(cp,[status(thm)],[t228,t6420]) ).
cnf(t6827,plain,
codomain(multiplication(coantidomain(X1),X2)) = backward_diamond(X2,coantidomain(X1)),
inference(orient,[status(thm)],[t6436]) ).
cnf(t6851,plain,
codomain(multiplication(coantidomain(X1),X2)) = codomain(backward_diamond(X2,coantidomain(X1))),
inference(cp,[status(thm)],[t6443,t6827]) ).
cnf(t44973,plain,
backward_diamond(X2,coantidomain(X1)) = codomain(backward_diamond(X2,coantidomain(X1))),
inference(step,[status(thm)],[t6851,t6827]) ).
cnf(t6876,plain,
codomain(backward_diamond(X1,coantidomain(X2))) = backward_diamond(X1,coantidomain(X2)),
inference(orient,[status(thm)],[t44973]) ).
cnf(t6877,plain,
backward_diamond(X1,coantidomain(coantidomain(X2))) = codomain(backward_diamond(X1,codomain(X2))),
inference(cp,[status(thm)],[t6876,t179]) ).
cnf(t44974,plain,
backward_diamond(X1,codomain(X2)) = codomain(backward_diamond(X1,codomain(X2))),
inference(step,[status(thm)],[t6877,t179]) ).
cnf(t6833,plain,
backward_diamond(X1,coantidomain(coantidomain(X2))) = codomain(multiplication(codomain(X2),X1)),
inference(cp,[status(thm)],[t6827,t179]) ).
cnf(t44971,plain,
backward_diamond(X1,codomain(X2)) = codomain(multiplication(codomain(X2),X1)),
inference(step,[status(thm)],[t6833,t179]) ).
cnf(t44972,plain,
backward_diamond(X1,codomain(X2)) = backward_diamond(X1,X2),
inference(step,[status(thm)],[t44971,t228]) ).
cnf(t6863,plain,
backward_diamond(X1,codomain(X2)) = backward_diamond(X1,X2),
inference(orient,[status(thm)],[t44972]) ).
cnf(t44975,plain,
backward_diamond(X1,X2) = codomain(backward_diamond(X1,codomain(X2))),
inference(step,[status(thm)],[t44974,t6863]) ).
cnf(t44976,plain,
backward_diamond(X1,X2) = codomain(backward_diamond(X1,X2)),
inference(step,[status(thm)],[t44975,t6863]) ).
cnf(t6894,plain,
codomain(backward_diamond(X1,X2)) = backward_diamond(X1,X2),
inference(orient,[status(thm)],[t44976]) ).
cnf(t18774,plain,
codomain(backward_diamond(X1,X2)) = backward_box(one,backward_diamond(X1,X2)),
inference(cp,[status(thm)],[t18772,t6894]) ).
cnf(t45474,plain,
backward_diamond(X1,X2) = backward_box(one,backward_diamond(X1,X2)),
inference(step,[status(thm)],[t18774,t6894]) ).
cnf(t19286,plain,
backward_box(one,backward_diamond(X1,X2)) = backward_diamond(X1,X2),
inference(orient,[status(thm)],[t45474]) ).
cnf(t45475,plain,
backward_diamond(X1,c(X2)) = coantidomain(backward_box(X1,X2)),
inference(step,[status(thm)],[t18485,t19286]) ).
cnf(t19299,plain,
backward_diamond(X1,c(X2)) = coantidomain(backward_box(X1,X2)),
inference(rw,[status(thm)],[t45475]) ).
cnf(t19300,plain,
coantidomain(backward_box(X1,X2)) = backward_diamond(X1,c(X2)),
inference(orient,[status(thm)],[t19299]) ).
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(t135,plain,
addition(coantidomain(multiplication(X1,X2)),coantidomain(multiplication(coantidomain(coantidomain(X1)),X2))) = coantidomain(multiplication(coantidomain(coantidomain(X1)),X2)),
inference(orient,[status(thm)],[t35]) ).
cnf(t44334,plain,
addition(coantidomain(multiplication(X1,X2)),coantidomain(multiplication(codomain(X1),X2))) = coantidomain(multiplication(coantidomain(coantidomain(X1)),X2)),
inference(step,[status(thm)],[t135,t179]) ).
cnf(t44335,plain,
addition(coantidomain(multiplication(X1,X2)),coantidomain(multiplication(codomain(X1),X2))) = coantidomain(multiplication(codomain(X1),X2)),
inference(step,[status(thm)],[t44334,t179]) ).
cnf(t183,plain,
addition(coantidomain(multiplication(X1,X2)),coantidomain(multiplication(codomain(X1),X2))) = coantidomain(multiplication(codomain(X1),X2)),
inference(rw,[status(thm)],[t44335]) ).
cnf(t6852,plain,
coantidomain(multiplication(coantidomain(X1),X2)) = coantidomain(backward_diamond(X2,coantidomain(X1))),
inference(cp,[status(thm)],[t6421,t6827]) ).
cnf(t7351,plain,
coantidomain(backward_diamond(X1,coantidomain(X2))) = coantidomain(multiplication(coantidomain(X2),X1)),
inference(orient,[status(thm)],[t6852]) ).
cnf(t7352,plain,
coantidomain(multiplication(coantidomain(coantidomain(X1)),X2)) = coantidomain(backward_diamond(X2,codomain(X1))),
inference(cp,[status(thm)],[t7351,t179]) ).
cnf(t44979,plain,
coantidomain(multiplication(codomain(X1),X2)) = coantidomain(backward_diamond(X2,codomain(X1))),
inference(step,[status(thm)],[t7352,t179]) ).
cnf(t44980,plain,
coantidomain(multiplication(codomain(X1),X2)) = coantidomain(backward_diamond(X2,X1)),
inference(step,[status(thm)],[t44979,t6863]) ).
cnf(t7374,plain,
coantidomain(multiplication(codomain(X1),X2)) = coantidomain(backward_diamond(X2,X1)),
inference(orient,[status(thm)],[t44980]) ).
cnf(t6902,plain,
backward_box(backward_diamond(X1,X2),zero) = c(backward_diamond(X1,X2)),
inference(cp,[status(thm)],[t602,t6894]) ).
cnf(t6911,plain,
backward_box(backward_diamond(X1,X2),zero) = c(backward_diamond(X1,X2)),
inference(orient,[status(thm)],[t6902]) ).
cnf(t45397,plain,
coantidomain(backward_diamond(X1,X2)) = c(backward_diamond(X1,X2)),
inference(step,[status(thm)],[t6911,t18474]) ).
cnf(t18513,plain,
coantidomain(backward_diamond(X1,X2)) = c(backward_diamond(X1,X2)),
inference(rw,[status(thm)],[t45397]) ).
cnf(t18976,plain,
c(backward_diamond(X1,X2)) = coantidomain(backward_diamond(X1,X2)),
inference(orient,[status(thm)],[t18513]) ).
cnf(t45468,plain,
coantidomain(backward_diamond(X1,c(X2))) = backward_box(X1,X2),
inference(step,[status(thm)],[t224,t18976]) ).
cnf(t19075,plain,
coantidomain(backward_diamond(X1,c(X2))) = backward_box(X1,X2),
inference(rw,[status(thm)],[t45468]) ).
cnf(t19395,plain,
coantidomain(backward_diamond(X1,c(X2))) = backward_box(X1,X2),
inference(orient,[status(thm)],[t19075]) ).
cnf(t45403,plain,
coantidomain(coantidomain(X1)) = c(coantidomain(X1)),
inference(step,[status(thm)],[t6473,t18474]) ).
cnf(t45404,plain,
codomain(X1) = c(coantidomain(X1)),
inference(step,[status(thm)],[t45403,t179]) ).
cnf(t18517,plain,
codomain(X1) = c(coantidomain(X1)),
inference(rw,[status(thm)],[t45404]) ).
cnf(t18530,plain,
c(coantidomain(X1)) = codomain(X1),
inference(orient,[status(thm)],[t18517]) ).
cnf(t19405,plain,
backward_box(X1,coantidomain(X2)) = coantidomain(backward_diamond(X1,codomain(X2))),
inference(cp,[status(thm)],[t19395,t18530]) ).
cnf(t45484,plain,
backward_box(X1,coantidomain(X2)) = coantidomain(backward_diamond(X1,X2)),
inference(step,[status(thm)],[t19405,t6863]) ).
cnf(t19497,plain,
coantidomain(backward_diamond(X1,X2)) = backward_box(X1,coantidomain(X2)),
inference(orient,[status(thm)],[t45484]) ).
cnf(t45485,plain,
coantidomain(multiplication(codomain(X1),X2)) = backward_box(X2,coantidomain(X1)),
inference(step,[status(thm)],[t7374,t19497]) ).
cnf(t19498,plain,
coantidomain(multiplication(codomain(X1),X2)) = backward_box(X2,coantidomain(X1)),
inference(orient,[status(thm)],[t45485]) ).
cnf(t45605,plain,
addition(coantidomain(multiplication(X1,X2)),backward_box(X2,coantidomain(X1))) = coantidomain(multiplication(codomain(X1),X2)),
inference(step,[status(thm)],[t183,t19498]) ).
cnf(t45606,plain,
addition(backward_box(X2,coantidomain(X1)),coantidomain(multiplication(X1,X2))) = coantidomain(multiplication(codomain(X1),X2)),
inference(step,[status(thm)],[t45605,t110]) ).
cnf(t45607,plain,
addition(backward_box(X2,coantidomain(X1)),coantidomain(multiplication(X1,X2))) = backward_box(X2,coantidomain(X1)),
inference(step,[status(thm)],[t45606,t19498]) ).
cnf(t25042,plain,
addition(backward_box(X1,coantidomain(X2)),coantidomain(multiplication(X2,X1))) = backward_box(X1,coantidomain(X2)),
inference(orient,[status(thm)],[t45607]) ).
cnf(t25109,plain,
backward_box(X1,coantidomain(c(X1))) = addition(backward_box(X1,coantidomain(c(X1))),coantidomain(zero)),
inference(cp,[status(thm)],[t25042,t2797]) ).
cnf(t45402,plain,
coantidomain(c(X1)) = backward_box(one,X1),
inference(step,[status(thm)],[t6476,t18474]) ).
cnf(t18516,plain,
coantidomain(c(X1)) = backward_box(one,X1),
inference(rw,[status(thm)],[t45402]) ).
cnf(t18718,plain,
coantidomain(c(X1)) = backward_box(one,X1),
inference(orient,[status(thm)],[t18516]) ).
cnf(t45608,plain,
backward_box(X1,backward_box(one,X1)) = addition(backward_box(X1,coantidomain(c(X1))),coantidomain(zero)),
inference(step,[status(thm)],[t25109,t18718]) ).
cnf(t2768,plain,
c(X1) = multiplication(forward_box(X1,zero),c(X1)),
inference(cp,[status(thm)],[t2755,t423]) ).
cnf(t3268,plain,
multiplication(forward_box(X1,zero),c(X1)) = c(X1),
inference(orient,[status(thm)],[t2768]) ).
cnf(t44860,plain,
multiplication(c(X1),c(X1)) = c(X1),
inference(step,[status(thm)],[t3268,t5657]) ).
cnf(t5666,plain,
multiplication(c(X1),c(X1)) = c(X1),
inference(rw,[status(thm)],[t44860]) ).
cnf(t5895,plain,
multiplication(c(X1),c(X1)) = c(X1),
inference(orient,[status(thm)],[t5666]) ).
cnf(t5913,plain,
forward_diamond(c(X1),c(X1)) = domain(c(X1)),
inference(cp,[status(thm)],[t5578,t5895]) ).
cnf(t44911,plain,
forward_diamond(c(X1),c(X1)) = c(X1),
inference(step,[status(thm)],[t5913,t5660]) ).
cnf(t5951,plain,
forward_diamond(c(X1),c(X1)) = c(X1),
inference(orient,[status(thm)],[t44911]) ).
cnf(t18559,plain,
c(coantidomain(X1)) = forward_diamond(codomain(X1),c(coantidomain(X1))),
inference(cp,[status(thm)],[t5951,t18530]) ).
cnf(t45425,plain,
codomain(X1) = forward_diamond(codomain(X1),c(coantidomain(X1))),
inference(step,[status(thm)],[t18559,t18530]) ).
cnf(t45426,plain,
codomain(X1) = forward_diamond(codomain(X1),codomain(X1)),
inference(step,[status(thm)],[t45425,t18530]) ).
cnf(t2596,plain,
multiplication(X1,addition(codomain(X1),X2)) = addition(X1,multiplication(X1,X2)),
inference(cp,[status(thm)],[t65,t2588]) ).
cnf(t45185,plain,
multiplication(X1,addition(codomain(X1),X2)) = multiplication(X1,addition(one,X2)),
inference(step,[status(thm)],[t2596,t1650]) ).
cnf(t13034,plain,
multiplication(X1,addition(codomain(X1),X2)) = multiplication(X1,addition(one,X2)),
inference(orient,[status(thm)],[t45185]) ).
cnf(t10550,plain,
addition(codomain(X1),domain(codomain(X1))) = multiplication(domain(codomain(X1)),one),
inference(cp,[status(thm)],[t10521,t799]) ).
cnf(t45089,plain,
addition(codomain(X1),domain(codomain(X1))) = domain(codomain(X1)),
inference(step,[status(thm)],[t10550,t41]) ).
cnf(t10630,plain,
addition(codomain(X1),domain(codomain(X1))) = domain(codomain(X1)),
inference(orient,[status(thm)],[t45089]) ).
cnf(t13036,plain,
multiplication(X1,addition(one,domain(codomain(X1)))) = multiplication(X1,domain(codomain(X1))),
inference(cp,[status(thm)],[t13034,t10630]) ).
cnf(t45186,plain,
multiplication(X1,one) = multiplication(X1,domain(codomain(X1))),
inference(step,[status(thm)],[t13036,t806]) ).
cnf(t45187,plain,
X1 = multiplication(X1,domain(codomain(X1))),
inference(step,[status(thm)],[t45186,t41]) ).
cnf(t13072,plain,
multiplication(X1,domain(codomain(X1))) = X1,
inference(orient,[status(thm)],[t45187]) ).
cnf(t13102,plain,
forward_diamond(X1,codomain(X1)) = domain(X1),
inference(cp,[status(thm)],[t157,t13072]) ).
cnf(t13104,plain,
forward_diamond(X1,codomain(X1)) = domain(X1),
inference(orient,[status(thm)],[t13102]) ).
cnf(t13109,plain,
domain(codomain(X1)) = forward_diamond(codomain(X1),codomain(X1)),
inference(cp,[status(thm)],[t13104,t6443]) ).
cnf(t13134,plain,
forward_diamond(codomain(X1),codomain(X1)) = domain(codomain(X1)),
inference(orient,[status(thm)],[t13109]) ).
cnf(t45427,plain,
codomain(X1) = domain(codomain(X1)),
inference(step,[status(thm)],[t45426,t13134]) ).
cnf(t18651,plain,
domain(codomain(X1)) = codomain(X1),
inference(orient,[status(thm)],[t45427]) ).
cnf(t18663,plain,
codomain(backward_diamond(X1,X2)) = domain(backward_diamond(X1,X2)),
inference(cp,[status(thm)],[t18651,t6894]) ).
cnf(t45458,plain,
backward_diamond(X1,X2) = domain(backward_diamond(X1,X2)),
inference(step,[status(thm)],[t18663,t6894]) ).
cnf(t18827,plain,
domain(backward_diamond(X1,X2)) = backward_diamond(X1,X2),
inference(orient,[status(thm)],[t45458]) ).
cnf(t45461,plain,
backward_diamond(X1,c(X2)) = c(backward_box(X1,X2)),
inference(step,[status(thm)],[t6326,t18827]) ).
cnf(t18904,plain,
backward_diamond(X1,c(X2)) = c(backward_box(X1,X2)),
inference(rw,[status(thm)],[t45461]) ).
cnf(t19076,plain,
c(backward_box(X1,X2)) = backward_diamond(X1,c(X2)),
inference(orient,[status(thm)],[t18904]) ).
cnf(t19117,plain,
domain(backward_box(X1,X2)) = c(backward_diamond(X1,c(X2))),
inference(cp,[status(thm)],[t5669,t19076]) ).
cnf(t45496,plain,
backward_box(X1,X2) = c(backward_diamond(X1,c(X2))),
inference(step,[status(thm)],[t19117,t6361]) ).
cnf(t45487,plain,
c(backward_diamond(X1,X2)) = backward_box(X1,coantidomain(X2)),
inference(step,[status(thm)],[t18976,t19497]) ).
cnf(t19500,plain,
c(backward_diamond(X1,X2)) = backward_box(X1,coantidomain(X2)),
inference(orient,[status(thm)],[t45487]) ).
cnf(t45497,plain,
backward_box(X1,X2) = backward_box(X1,coantidomain(c(X2))),
inference(step,[status(thm)],[t45496,t19500]) ).
cnf(t45498,plain,
backward_box(X1,X2) = backward_box(X1,backward_box(one,X2)),
inference(step,[status(thm)],[t45497,t18718]) ).
cnf(t19732,plain,
backward_box(X1,backward_box(one,X2)) = backward_box(X1,X2),
inference(orient,[status(thm)],[t45498]) ).
cnf(t45609,plain,
backward_box(X1,X1) = addition(backward_box(X1,coantidomain(c(X1))),coantidomain(zero)),
inference(step,[status(thm)],[t45608,t19732]) ).
cnf(t45610,plain,
backward_box(X1,X1) = addition(coantidomain(zero),backward_box(X1,coantidomain(c(X1)))),
inference(step,[status(thm)],[t45609,t110]) ).
cnf(t235,plain,
codomain(one) = coantidomain(zero),
inference(cp,[status(thm)],[t179,t234]) ).
cnf(t261,plain,
coantidomain(zero) = codomain(one),
inference(orient,[status(thm)],[t235]) ).
cnf(t44396,plain,
coantidomain(zero) = one,
inference(step,[status(thm)],[t261,t577]) ).
cnf(t578,plain,
coantidomain(zero) = one,
inference(orient,[status(thm)],[t44396]) ).
cnf(t45611,plain,
backward_box(X1,X1) = addition(one,backward_box(X1,coantidomain(c(X1)))),
inference(step,[status(thm)],[t45610,t578]) ).
cnf(t824,plain,
one = addition(one,backward_box(X1,X2)),
inference(cp,[status(thm)],[t817,t224]) ).
cnf(t901,plain,
addition(one,backward_box(X1,X2)) = one,
inference(orient,[status(thm)],[t824]) ).
cnf(t45612,plain,
backward_box(X1,X1) = one,
inference(step,[status(thm)],[t45611,t901]) ).
cnf(t25156,plain,
backward_box(X1,X1) = one,
inference(orient,[status(thm)],[t45612]) ).
cnf(t25160,plain,
backward_diamond(X1,c(X1)) = coantidomain(one),
inference(cp,[status(thm)],[t19300,t25156]) ).
cnf(t45613,plain,
backward_diamond(X1,c(X1)) = zero,
inference(step,[status(thm)],[t25160,t234]) ).
cnf(t25181,plain,
backward_diamond(X1,c(X1)) = zero,
inference(orient,[status(thm)],[t45613]) ).
cnf(t38941,plain,
one = forward_box(multiplication(codomain(c(X1)),X1),zero),
inference(cp,[status(thm)],[t38926,t25181]) ).
cnf(t45907,plain,
one = c(multiplication(codomain(c(X1)),X1)),
inference(step,[status(thm)],[t38941,t5657]) ).
cnf(t39042,plain,
c(multiplication(codomain(c(X1)),X1)) = one,
inference(orient,[status(thm)],[t45907]) ).
cnf(t39089,plain,
zero = multiplication(one,multiplication(codomain(c(X1)),X1)),
inference(cp,[status(thm)],[t2797,t39042]) ).
cnf(t45913,plain,
zero = multiplication(codomain(c(X1)),X1),
inference(step,[status(thm)],[t39089,t42]) ).
cnf(t39221,plain,
multiplication(codomain(c(X1)),X1) = zero,
inference(orient,[status(thm)],[t45913]) ).
cnf(t39233,plain,
multiplication(addition(codomain(c(X1)),X2),X1) = addition(zero,multiplication(X2,X1)),
inference(cp,[status(thm)],[t89,t39221]) ).
cnf(t45953,plain,
multiplication(addition(codomain(c(X1)),X2),X1) = multiplication(X2,X1),
inference(step,[status(thm)],[t39233,t289]) ).
cnf(t40135,plain,
multiplication(addition(codomain(c(X1)),X2),X1) = multiplication(X2,X1),
inference(orient,[status(thm)],[t45953]) ).
cnf(t40140,plain,
multiplication(coantidomain(c(X1)),X1) = multiplication(one,X1),
inference(cp,[status(thm)],[t40135,t567]) ).
cnf(t45954,plain,
multiplication(backward_box(one,X1),X1) = multiplication(one,X1),
inference(step,[status(thm)],[t40140,t18718]) ).
cnf(t45955,plain,
multiplication(backward_box(one,X1),X1) = X1,
inference(step,[status(thm)],[t45954,t42]) ).
cnf(t40230,plain,
multiplication(backward_box(one,X1),X1) = X1,
inference(orient,[status(thm)],[t45955]) ).
cnf(t44775,plain,
multiplication(c(X1),c(X2)) = domain_difference(antidomain(X1),X2),
inference(step,[status(thm)],[t1307,t5571]) ).
cnf(t44776,plain,
multiplication(c(X1),c(X2)) = domain_difference(c(X1),X2),
inference(step,[status(thm)],[t44775,t5571]) ).
cnf(t5607,plain,
multiplication(c(X1),c(X2)) = domain_difference(c(X1),X2),
inference(rw,[status(thm)],[t44776]) ).
cnf(t6282,plain,
multiplication(c(X1),c(X2)) = domain_difference(c(X1),X2),
inference(orient,[status(thm)],[t5607]) ).
cnf(t6291,plain,
domain_difference(c(backward_diamond(X1,c(X2))),X3) = multiplication(backward_box(X1,X2),c(X3)),
inference(cp,[status(thm)],[t6282,t224]) ).
cnf(t45264,plain,
domain_difference(backward_box(X1,X2),X3) = multiplication(backward_box(X1,X2),c(X3)),
inference(step,[status(thm)],[t6291,t224]) ).
cnf(t15188,plain,
multiplication(backward_box(X1,X2),c(X3)) = domain_difference(backward_box(X1,X2),X3),
inference(orient,[status(thm)],[t45264]) ).
cnf(t40231,plain,
c(X1) = domain_difference(backward_box(one,c(X1)),X1),
inference(cp,[status(thm)],[t40230,t15188]) ).
cnf(t6481,plain,
backward_box(one,c(X1)) = backward_box(domain(X1),zero),
inference(cp,[status(thm)],[t6476,t5669]) ).
cnf(t6560,plain,
backward_box(domain(X1),zero) = backward_box(one,c(X1)),
inference(orient,[status(thm)],[t6481]) ).
cnf(t45401,plain,
coantidomain(domain(X1)) = backward_box(one,c(X1)),
inference(step,[status(thm)],[t6560,t18474]) ).
cnf(t18515,plain,
coantidomain(domain(X1)) = backward_box(one,c(X1)),
inference(rw,[status(thm)],[t45401]) ).
cnf(t18797,plain,
backward_box(one,c(X1)) = coantidomain(domain(X1)),
inference(orient,[status(thm)],[t18515]) ).
cnf(t45956,plain,
c(X1) = domain_difference(coantidomain(domain(X1)),X1),
inference(step,[status(thm)],[t40231,t18797]) ).
cnf(t2814,plain,
multiplication(c(X1),addition(X2,X1)) = addition(multiplication(c(X1),X2),zero),
inference(cp,[status(thm)],[t65,t2797]) ).
cnf(t45135,plain,
multiplication(c(X1),addition(X2,X1)) = multiplication(c(X1),X2),
inference(step,[status(thm)],[t2814,t44]) ).
cnf(t11525,plain,
multiplication(c(X1),addition(X2,X1)) = multiplication(c(X1),X2),
inference(orient,[status(thm)],[t45135]) ).
cnf(t639,plain,
addition(domain(X1),addition(c(X1),X2)) = addition(one,X2),
inference(cp,[status(thm)],[t115,t625]) ).
cnf(t17056,plain,
addition(domain(X1),addition(c(X1),X2)) = addition(one,X2),
inference(orient,[status(thm)],[t639]) ).
cnf(t2593,plain,
multiplication(addition(one,X1),codomain(X1)) = addition(codomain(X1),X1),
inference(cp,[status(thm)],[t2076,t2588]) ).
cnf(t45076,plain,
multiplication(addition(one,X1),codomain(X1)) = addition(X1,codomain(X1)),
inference(step,[status(thm)],[t2593,t110]) ).
cnf(t10346,plain,
multiplication(addition(one,X1),codomain(X1)) = addition(X1,codomain(X1)),
inference(orient,[status(thm)],[t45076]) ).
cnf(t10367,plain,
addition(c(X1),codomain(c(X1))) = multiplication(one,codomain(c(X1))),
inference(cp,[status(thm)],[t10346,t817]) ).
cnf(t45078,plain,
addition(c(X1),codomain(c(X1))) = codomain(c(X1)),
inference(step,[status(thm)],[t10367,t42]) ).
cnf(t10404,plain,
addition(c(X1),codomain(c(X1))) = codomain(c(X1)),
inference(orient,[status(thm)],[t45078]) ).
cnf(t17075,plain,
addition(one,codomain(c(X1))) = addition(domain(X1),codomain(c(X1))),
inference(cp,[status(thm)],[t17056,t10404]) ).
cnf(t45293,plain,
one = addition(domain(X1),codomain(c(X1))),
inference(step,[status(thm)],[t17075,t799]) ).
cnf(t17117,plain,
addition(domain(X1),codomain(c(X1))) = one,
inference(orient,[status(thm)],[t45293]) ).
cnf(t17132,plain,
one = addition(c(X1),codomain(c(c(X1)))),
inference(cp,[status(thm)],[t17117,t5660]) ).
cnf(t45294,plain,
one = addition(c(X1),codomain(domain(X1))),
inference(step,[status(thm)],[t17132,t5669]) ).
cnf(t17167,plain,
addition(c(X1),codomain(domain(X1))) = one,
inference(orient,[status(thm)],[t45294]) ).
cnf(t17202,plain,
multiplication(c(codomain(domain(X1))),c(X1)) = multiplication(c(codomain(domain(X1))),one),
inference(cp,[status(thm)],[t11525,t17167]) ).
cnf(t45305,plain,
domain_difference(c(codomain(domain(X1))),X1) = multiplication(c(codomain(domain(X1))),one),
inference(step,[status(thm)],[t17202,t6282]) ).
cnf(t45306,plain,
domain_difference(backward_box(domain(X1),zero),X1) = multiplication(c(codomain(domain(X1))),one),
inference(step,[status(thm)],[t45305,t602]) ).
cnf(t45307,plain,
domain_difference(backward_box(one,c(X1)),X1) = multiplication(c(codomain(domain(X1))),one),
inference(step,[status(thm)],[t45306,t6560]) ).
cnf(t45308,plain,
domain_difference(backward_box(one,c(X1)),X1) = c(codomain(domain(X1))),
inference(step,[status(thm)],[t45307,t41]) ).
cnf(t45309,plain,
domain_difference(backward_box(one,c(X1)),X1) = backward_box(domain(X1),zero),
inference(step,[status(thm)],[t45308,t602]) ).
cnf(t45310,plain,
domain_difference(backward_box(one,c(X1)),X1) = backward_box(one,c(X1)),
inference(step,[status(thm)],[t45309,t6560]) ).
cnf(t17460,plain,
domain_difference(backward_box(one,c(X1)),X1) = backward_box(one,c(X1)),
inference(orient,[status(thm)],[t45310]) ).
cnf(t17477,plain,
backward_box(one,c(c(X1))) = domain_difference(backward_box(one,domain(X1)),c(X1)),
inference(cp,[status(thm)],[t17460,t5669]) ).
cnf(t45311,plain,
backward_box(one,domain(X1)) = domain_difference(backward_box(one,domain(X1)),c(X1)),
inference(step,[status(thm)],[t17477,t5669]) ).
cnf(t604,plain,
backward_box(codomain(X1),zero) = c(backward_diamond(one,X1)),
inference(cp,[status(thm)],[t602,t374]) ).
cnf(t738,plain,
c(backward_diamond(one,X1)) = backward_box(codomain(X1),zero),
inference(orient,[status(thm)],[t604]) ).
cnf(t739,plain,
backward_box(codomain(c(X1)),zero) = backward_box(one,X1),
inference(cp,[status(thm)],[t738,t224]) ).
cnf(t991,plain,
backward_box(codomain(c(X1)),zero) = backward_box(one,X1),
inference(orient,[status(thm)],[t739]) ).
cnf(t5692,plain,
backward_box(one,c(X1)) = backward_box(codomain(domain(X1)),zero),
inference(cp,[status(thm)],[t991,t5669]) ).
cnf(t6379,plain,
backward_box(codomain(domain(X1)),zero) = backward_box(one,c(X1)),
inference(orient,[status(thm)],[t5692]) ).
cnf(t6386,plain,
backward_box(one,c(c(X1))) = backward_box(codomain(c(X1)),zero),
inference(cp,[status(thm)],[t6379,t5660]) ).
cnf(t44958,plain,
backward_box(one,domain(X1)) = backward_box(codomain(c(X1)),zero),
inference(step,[status(thm)],[t6386,t5669]) ).
cnf(t44959,plain,
backward_box(one,domain(X1)) = backward_box(one,X1),
inference(step,[status(thm)],[t44958,t991]) ).
cnf(t6465,plain,
backward_box(one,domain(X1)) = backward_box(one,X1),
inference(orient,[status(thm)],[t44959]) ).
cnf(t45312,plain,
backward_box(one,X1) = domain_difference(backward_box(one,domain(X1)),c(X1)),
inference(step,[status(thm)],[t45311,t6465]) ).
cnf(t45313,plain,
backward_box(one,X1) = domain_difference(backward_box(one,X1),c(X1)),
inference(step,[status(thm)],[t45312,t6465]) ).
cnf(t17492,plain,
domain_difference(backward_box(one,X1),c(X1)) = backward_box(one,X1),
inference(orient,[status(thm)],[t45313]) ).
cnf(t18811,plain,
backward_box(one,c(X1)) = domain_difference(coantidomain(domain(X1)),c(c(X1))),
inference(cp,[status(thm)],[t17492,t18797]) ).
cnf(t45480,plain,
coantidomain(domain(X1)) = domain_difference(coantidomain(domain(X1)),c(c(X1))),
inference(step,[status(thm)],[t18811,t18797]) ).
cnf(t45481,plain,
coantidomain(domain(X1)) = domain_difference(coantidomain(domain(X1)),domain(X1)),
inference(step,[status(thm)],[t45480,t5669]) ).
cnf(t44788,plain,
multiplication(domain(X1),c(X2)) = domain_difference(X1,X2),
inference(step,[status(thm)],[t99,t5571]) ).
cnf(t101,plain,
domain_difference(X1,domain(X2)) = multiplication(domain(X1),c(X2)),
inference(cp,[status(thm)],[t99,t60]) ).
cnf(t1256,plain,
multiplication(domain(X1),c(X2)) = domain_difference(X1,domain(X2)),
inference(orient,[status(thm)],[t101]) ).
cnf(t44789,plain,
domain_difference(X1,domain(X2)) = domain_difference(X1,X2),
inference(step,[status(thm)],[t44788,t1256]) ).
cnf(t5616,plain,
domain_difference(X1,domain(X2)) = domain_difference(X1,X2),
inference(rw,[status(thm)],[t44789]) ).
cnf(t5733,plain,
domain_difference(X1,domain(X2)) = domain_difference(X1,X2),
inference(orient,[status(thm)],[t5616]) ).
cnf(t45482,plain,
coantidomain(domain(X1)) = domain_difference(coantidomain(domain(X1)),X1),
inference(step,[status(thm)],[t45481,t5733]) ).
cnf(t19375,plain,
domain_difference(coantidomain(domain(X1)),X1) = coantidomain(domain(X1)),
inference(orient,[status(thm)],[t45482]) ).
cnf(t45957,plain,
c(X1) = coantidomain(domain(X1)),
inference(step,[status(thm)],[t45956,t19375]) ).
cnf(t40301,plain,
coantidomain(domain(X1)) = c(X1),
inference(orient,[status(thm)],[t45957]) ).
cnf(t5670,plain,
domain(multiplication(X1,domain(X2))) = c(c(forward_diamond(X1,X2))),
inference(cp,[status(thm)],[t5669,t5576]) ).
cnf(t44888,plain,
forward_diamond(X1,X2) = c(c(forward_diamond(X1,X2))),
inference(step,[status(thm)],[t5670,t157]) ).
cnf(t44889,plain,
forward_diamond(X1,X2) = domain(forward_diamond(X1,X2)),
inference(step,[status(thm)],[t44888,t5669]) ).
cnf(t5754,plain,
domain(forward_diamond(X1,X2)) = forward_diamond(X1,X2),
inference(orient,[status(thm)],[t44889]) ).
cnf(t40324,plain,
c(forward_diamond(X1,X2)) = coantidomain(forward_diamond(X1,X2)),
inference(cp,[status(thm)],[t40301,t5754]) ).
cnf(t46099,plain,
forward_box(X1,c(X2)) = coantidomain(forward_diamond(X1,X2)),
inference(step,[status(thm)],[t40324,t6076]) ).
cnf(t41050,plain,
coantidomain(forward_diamond(X1,X2)) = forward_box(X1,c(X2)),
inference(orient,[status(thm)],[t46099]) ).
cnf(t46101,plain,
forward_diamond(domain(sk1),forward_box(sk0,c(sk1))) = zero,
inference(step,[status(thm)],[t23748,t41050]) ).
cnf(t41193,plain,
forward_diamond(domain(sk1),forward_box(sk0,c(sk1))) = zero,
inference(rw,[status(thm)],[t46101]) ).
cnf(t44278,plain,
forward_diamond(domain(sk1),forward_box(sk0,c(sk1))) = zero,
inference(orient,[status(thm)],[t41193]) ).
cnf(t44279,plain,
forward_diamond(star(sk0),forward_diamond(domain(sk1),forward_box(sk0,c(sk1)))) = addition(forward_diamond(sk0,sk1),forward_diamond(star(sk0),zero)),
inference(cp,[status(thm)],[t23589,t44278]) ).
cnf(t46144,plain,
forward_diamond(star(sk0),zero) = addition(forward_diamond(sk0,sk1),forward_diamond(star(sk0),zero)),
inference(step,[status(thm)],[t44279,t44278]) ).
cnf(t271,plain,
forward_diamond(X1,zero) = domain(multiplication(X1,zero)),
inference(cp,[status(thm)],[t157,t267]) ).
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(t76,plain,
multiplication(X1,zero) = zero,
inference(orient,[status(thm)],[t6]) ).
cnf(t44364,plain,
forward_diamond(X1,zero) = domain(zero),
inference(step,[status(thm)],[t271,t76]) ).
cnf(t44365,plain,
forward_diamond(X1,zero) = zero,
inference(step,[status(thm)],[t44364,t267]) ).
cnf(t294,plain,
forward_diamond(X1,zero) = zero,
inference(orient,[status(thm)],[t44365]) ).
cnf(t46145,plain,
zero = addition(forward_diamond(sk0,sk1),forward_diamond(star(sk0),zero)),
inference(step,[status(thm)],[t46144,t294]) ).
cnf(t46146,plain,
zero = addition(forward_diamond(sk0,sk1),zero),
inference(step,[status(thm)],[t46145,t294]) ).
cnf(t46147,plain,
zero = forward_diamond(sk0,sk1),
inference(step,[status(thm)],[t46146,t44]) ).
cnf(t44280,plain,
forward_diamond(sk0,sk1) = zero,
inference(orient,[status(thm)],[t46147]) ).
cnf(t46168,plain,
multiplication(zero,sk1) = sk1,
inference(step,[status(thm)],[t13566,t44280]) ).
cnf(t46169,plain,
zero = sk1,
inference(step,[status(thm)],[t46168,t108]) ).
cnf(t44294,plain,
zero = sk1,
inference(rw,[status(thm)],[t46169]) ).
cnf(t44299,plain,
sk1 = zero,
inference(orient,[status(thm)],[t44294]) ).
cnf(c31,plain,
domain(sk1) != zero,
inference(cnf_transformation,[status(esa)],[f28_sk]) ).
cnf(goal_0,negated_conjecture,
domain(sk1) != zero,
inference(equality_encoding,[status(esa)],[c31]) ).
cnf(g0_0,plain,
domain(zero) != zero,
inference(rw,[status(thm)],[goal_0,t44299]) ).
cnf(g0_1,plain,
zero != zero,
inference(rw,[status(thm)],[g0_0,t267]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_1]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : KLE132+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.13/5.40 % Computer : n005.cluster.edu
% 0.13/5.40 % Model : x86_64 x86_64
% 0.13/5.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/5.40 % Memory : 8046.5625MB
% 0.13/5.40 % OS : Linux 6.8.0-71-generic
% 0.13/5.40 % CPULimit : 300
% 0.16/5.40 % WCLimit : 300
% 0.16/5.40 % DateTime : Wed Sep 23 19:02:07 UTC 2026
% 0.16/5.40 % CPUTime :
% 0.16/5.40 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 57.60/12.80 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 57.60/12.80 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------