%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : KLE131+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 : n011.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 22.72s 3.36s
% Output : Proof 22.72s
% Verified :
% SZS Type : Refutation
% Derivation depth : 53
% Number of leaves : 19
% Syntax : Number of formulae : 337 ( 328 unt; 0 def)
% Number of atoms : 350 ( 342 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 25 ( 12 ~; 6 |; 4 &)
% ( 1 <=>; 0 =>; 2 <=; 0 <~>)
% Maximal formula depth : 6 ( 1 avg)
% Maximal term depth : 16 ( 3 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 15 ( 15 usr; 4 con; 0-4 aty)
% Number of variables : 452 ( 6 sgn 96 !; 1 ?)
% Comments :
%------------------------------------------------------------------------------
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]) ).
fof(f28,conjecture,
! [X0] :
( divergence(X0) = zero
<= ! [X1] : addition(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)))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goals) ).
fof(f28_neg,negated_conjecture,
~ ! [X0] :
( divergence(X0) = zero
<= ! [X1] : addition(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(negated_conjecture,[status(cth)],[f28]) ).
fof(f28_nnf,plain,
? [X0] :
( divergence(X0) != zero
& ! [X1] : addition(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] :
( divergence(sk0) != zero
& addition(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])],[f28_nnf]) ).
cnf(c29,plain,
addition(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(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]) ).
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(hi21,axiom,
domain(X0) = antidomain(antidomain(X0)),
inference(equality_encoding,[status(esa)],[c16]) ).
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(hi20,axiom,
forward_diamond(X0,X1) = domain(multiplication(X0,domain(X1))),
inference(equality_encoding,[status(esa)],[c23]) ).
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(hi24,axiom,
domain_difference(X0,X1) = multiplication(domain(X0),antidomain(X1)),
inference(equality_encoding,[status(esa)],[c22]) ).
cnf(h5,plain,
leq(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(t37,plain,
addition(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(t9,plain,
antidomain(antidomain(X1)) = domain(X1),
inference(equality_encoding,[status(esa)],[c16]) ).
cnf(t46,plain,
antidomain(antidomain(X1)) = domain(X1),
inference(orient,[status(thm)],[t9]) ).
cnf(t23967,plain,
addition(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)],[t37,t46]) ).
cnf(t23968,plain,
addition(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)],[t23967,t46]) ).
cnf(t23969,plain,
addition(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)],[t23968,t46]) ).
cnf(t23970,plain,
addition(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)],[t23969,t46]) ).
cnf(t23971,plain,
addition(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)],[t23970,t46]) ).
cnf(t23972,plain,
addition(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)],[t23971,t46]) ).
cnf(t23973,plain,
addition(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)],[t23972,t46]) ).
cnf(t23974,plain,
addition(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)],[t23973,t46]) ).
cnf(t23975,plain,
addition(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)],[t23974,t46]) ).
cnf(t23976,plain,
addition(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)],[t23975,t46]) ).
cnf(t23977,plain,
addition(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)],[t23976,t46]) ).
cnf(t23978,plain,
addition(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)],[t23977,t46]) ).
cnf(t23979,plain,
addition(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)],[t23978,t46]) ).
cnf(t23980,plain,
addition(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)],[t23979,t46]) ).
cnf(t23981,plain,
addition(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)],[t23980,t46]) ).
cnf(t48,plain,
addition(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)],[t23981]) ).
cnf(t22,plain,
domain(multiplication(X1,domain(X2))) = forward_diamond(X1,X2),
inference(equality_encoding,[status(esa)],[c23]) ).
cnf(t148,plain,
domain(multiplication(X1,domain(X2))) = forward_diamond(X1,X2),
inference(orient,[status(thm)],[t22]) ).
cnf(t23988,plain,
addition(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)],[t48,t148]) ).
cnf(t23989,plain,
addition(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)],[t23988,t148]) ).
cnf(t169,plain,
addition(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)],[t23989]) ).
cnf(t47,plain,
domain(antidomain(X1)) = antidomain(domain(X1)),
inference(cp,[status(thm)],[t46,t46]) ).
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(t55,plain,
antidomain(domain(X1)) = c(X1),
inference(orient,[status(thm)],[t10]) ).
cnf(t24021,plain,
domain(antidomain(X1)) = c(X1),
inference(step,[status(thm)],[t47,t55]) ).
cnf(t304,plain,
domain(antidomain(X1)) = c(X1),
inference(orient,[status(thm)],[t24021]) ).
cnf(t310,plain,
forward_diamond(X1,antidomain(X2)) = domain(multiplication(X1,c(X2))),
inference(cp,[status(thm)],[t148,t304]) ).
cnf(t1322,plain,
domain(multiplication(X1,c(X2))) = forward_diamond(X1,antidomain(X2)),
inference(orient,[status(thm)],[t310]) ).
fof(f7,axiom,
! [A,B,C] : multiplication(A,addition(B,C)) = addition(multiplication(A,B),multiplication(A,C)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',right_distributivity) ).
fof(f7_nnf,plain,
! [A,B,C] : multiplication(A,addition(B,C)) = addition(multiplication(A,B),multiplication(A,C)),
inference(nnf_transformation,[status(thm)],[f7]) ).
fof(f7_sk,plain,
! [A,B,C] : multiplication(A,addition(B,C)) = addition(multiplication(A,B),multiplication(A,C)),
inference(skolemisation,[status(esa)],[f7_nnf]) ).
cnf(c7,plain,
multiplication(X0,addition(X1,X2)) = addition(multiplication(X0,X1),multiplication(X0,X2)),
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
cnf(t28,plain,
addition(multiplication(X1,X2),multiplication(X1,X3)) = multiplication(X1,addition(X2,X3)),
inference(equality_encoding,[status(esa)],[c7]) ).
cnf(t60,plain,
addition(multiplication(X1,X2),multiplication(X1,X3)) = multiplication(X1,addition(X2,X3)),
inference(orient,[status(thm)],[t28]) ).
fof(f12,axiom,
! [X0] : multiplication(antidomain(X0),X0) = zero,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',domain1) ).
fof(f12_nnf,plain,
! [X0] : multiplication(antidomain(X0),X0) = zero,
inference(nnf_transformation,[status(thm)],[f12]) ).
fof(f12_sk,plain,
! [X0] : multiplication(antidomain(X0),X0) = zero,
inference(skolemisation,[status(esa)],[f12_nnf]) ).
cnf(c13,plain,
multiplication(antidomain(X0),X0) = zero,
inference(cnf_transformation,[status(esa)],[f12_sk]) ).
cnf(t13,plain,
multiplication(antidomain(X1),X1) = zero,
inference(equality_encoding,[status(esa)],[c13]) ).
cnf(t75,plain,
multiplication(antidomain(X1),X1) = zero,
inference(orient,[status(thm)],[t13]) ).
cnf(t79,plain,
multiplication(antidomain(X1),addition(X1,X2)) = addition(zero,multiplication(antidomain(X1),X2)),
inference(cp,[status(thm)],[t60,t75]) ).
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(t105,plain,
addition(X1,X2) = addition(X2,X1),
inference(orient,[status(thm)],[t14]) ).
fof(f2,axiom,
! [A] : addition(A,zero) = A,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',additive_identity) ).
fof(f2_nnf,plain,
! [A] : addition(A,zero) = A,
inference(nnf_transformation,[status(thm)],[f2]) ).
fof(f2_sk,plain,
! [A] : addition(A,zero) = A,
inference(skolemisation,[status(esa)],[f2_nnf]) ).
cnf(c2,plain,
addition(X0,zero) = X0,
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(t1,plain,
addition(X1,zero) = X1,
inference(equality_encoding,[status(esa)],[c2]) ).
cnf(t41,plain,
addition(X1,zero) = X1,
inference(orient,[status(thm)],[t1]) ).
cnf(t106,plain,
addition(zero,X1) = X1,
inference(cp,[status(thm)],[t105,t41]) ).
cnf(t279,plain,
addition(zero,X1) = X1,
inference(orient,[status(thm)],[t106]) ).
cnf(t24389,plain,
multiplication(antidomain(X1),addition(X1,X2)) = multiplication(antidomain(X1),X2),
inference(step,[status(thm)],[t79,t279]) ).
cnf(t5600,plain,
multiplication(antidomain(X1),addition(X1,X2)) = multiplication(antidomain(X1),X2),
inference(orient,[status(thm)],[t24389]) ).
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]) ).
cnf(t23984,plain,
addition(antidomain(X1),antidomain(antidomain(X1))) = one,
inference(step,[status(thm)],[t17,t105]) ).
cnf(t23985,plain,
addition(antidomain(X1),domain(X1)) = one,
inference(step,[status(thm)],[t23984,t46]) ).
cnf(t23986,plain,
addition(domain(X1),antidomain(X1)) = one,
inference(step,[status(thm)],[t23985,t105]) ).
cnf(t121,plain,
addition(domain(X1),antidomain(X1)) = one,
inference(orient,[status(thm)],[t23986]) ).
cnf(t5623,plain,
multiplication(antidomain(domain(X1)),antidomain(X1)) = multiplication(antidomain(domain(X1)),one),
inference(cp,[status(thm)],[t5600,t121]) ).
cnf(t24390,plain,
multiplication(c(X1),antidomain(X1)) = multiplication(antidomain(domain(X1)),one),
inference(step,[status(thm)],[t5623,t55]) ).
cnf(t23,plain,
multiplication(domain(X1),antidomain(X2)) = domain_difference(X1,X2),
inference(equality_encoding,[status(esa)],[c22]) ).
cnf(t94,plain,
multiplication(domain(X1),antidomain(X2)) = domain_difference(X1,X2),
inference(orient,[status(thm)],[t23]) ).
cnf(t308,plain,
domain_difference(antidomain(X1),X2) = multiplication(c(X1),antidomain(X2)),
inference(cp,[status(thm)],[t94,t304]) ).
cnf(t1296,plain,
multiplication(c(X1),antidomain(X2)) = domain_difference(antidomain(X1),X2),
inference(orient,[status(thm)],[t308]) ).
cnf(t24391,plain,
domain_difference(antidomain(X1),X1) = multiplication(antidomain(domain(X1)),one),
inference(step,[status(thm)],[t24390,t1296]) ).
fof(f8,axiom,
! [A,B,C] : multiplication(addition(A,B),C) = addition(multiplication(A,C),multiplication(B,C)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',left_distributivity) ).
fof(f8_nnf,plain,
! [A,B,C] : multiplication(addition(A,B),C) = addition(multiplication(A,C),multiplication(B,C)),
inference(nnf_transformation,[status(thm)],[f8]) ).
fof(f8_sk,plain,
! [A,B,C] : multiplication(addition(A,B),C) = addition(multiplication(A,C),multiplication(B,C)),
inference(skolemisation,[status(esa)],[f8_nnf]) ).
cnf(c8,plain,
multiplication(addition(X0,X1),X2) = addition(multiplication(X0,X2),multiplication(X1,X2)),
inference(cnf_transformation,[status(esa)],[f8_sk]) ).
cnf(t29,plain,
addition(multiplication(X1,X2),multiplication(X3,X2)) = multiplication(addition(X1,X3),X2),
inference(equality_encoding,[status(esa)],[c8]) ).
cnf(t84,plain,
addition(multiplication(X1,X2),multiplication(X3,X2)) = multiplication(addition(X1,X3),X2),
inference(orient,[status(thm)],[t29]) ).
cnf(t90,plain,
multiplication(addition(X1,antidomain(X2)),X2) = addition(multiplication(X1,X2),zero),
inference(cp,[status(thm)],[t84,t75]) ).
cnf(t24226,plain,
multiplication(addition(X1,antidomain(X2)),X2) = multiplication(X1,X2),
inference(step,[status(thm)],[t90,t41]) ).
cnf(t2691,plain,
multiplication(addition(X1,antidomain(X2)),X2) = multiplication(X1,X2),
inference(orient,[status(thm)],[t24226]) ).
cnf(t2695,plain,
multiplication(domain(X1),X1) = multiplication(one,X1),
inference(cp,[status(thm)],[t2691,t121]) ).
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(t39,plain,
multiplication(one,X1) = X1,
inference(orient,[status(thm)],[t7]) ).
cnf(t24227,plain,
multiplication(domain(X1),X1) = X1,
inference(step,[status(thm)],[t2695,t39]) ).
cnf(t2734,plain,
multiplication(domain(X1),X1) = X1,
inference(orient,[status(thm)],[t24227]) ).
cnf(t2736,plain,
antidomain(X1) = domain_difference(antidomain(X1),X1),
inference(cp,[status(thm)],[t2734,t94]) ).
cnf(t2824,plain,
domain_difference(antidomain(X1),X1) = antidomain(X1),
inference(orient,[status(thm)],[t2736]) ).
cnf(t24392,plain,
antidomain(X1) = multiplication(antidomain(domain(X1)),one),
inference(step,[status(thm)],[t24391,t2824]) ).
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(t38,plain,
multiplication(X1,one) = X1,
inference(orient,[status(thm)],[t5]) ).
cnf(t24393,plain,
antidomain(X1) = antidomain(domain(X1)),
inference(step,[status(thm)],[t24392,t38]) ).
cnf(t24394,plain,
antidomain(X1) = c(X1),
inference(step,[status(thm)],[t24393,t55]) ).
cnf(t5637,plain,
antidomain(X1) = c(X1),
inference(orient,[status(thm)],[t24394]) ).
cnf(t24401,plain,
domain(multiplication(X1,c(X2))) = forward_diamond(X1,c(X2)),
inference(step,[status(thm)],[t1322,t5637]) ).
cnf(t5644,plain,
domain(multiplication(X1,c(X2))) = forward_diamond(X1,c(X2)),
inference(orient,[status(thm)],[t24401]) ).
cnf(t24452,plain,
c(antidomain(X1)) = domain(X1),
inference(step,[status(thm)],[t46,t5637]) ).
cnf(t24453,plain,
c(c(X1)) = domain(X1),
inference(step,[status(thm)],[t24452,t5637]) ).
cnf(t5684,plain,
c(c(X1)) = domain(X1),
inference(rw,[status(thm)],[t24453]) ).
cnf(t5735,plain,
c(c(X1)) = domain(X1),
inference(orient,[status(thm)],[t5684]) ).
cnf(t5761,plain,
forward_diamond(X1,c(c(X2))) = domain(multiplication(X1,domain(X2))),
inference(cp,[status(thm)],[t5644,t5735]) ).
cnf(t24553,plain,
forward_diamond(X1,domain(X2)) = domain(multiplication(X1,domain(X2))),
inference(step,[status(thm)],[t5761,t5735]) ).
cnf(t24554,plain,
forward_diamond(X1,domain(X2)) = forward_diamond(X1,X2),
inference(step,[status(thm)],[t24553,t148]) ).
cnf(t5908,plain,
forward_diamond(X1,domain(X2)) = forward_diamond(X1,X2),
inference(orient,[status(thm)],[t24554]) ).
cnf(t5915,plain,
forward_diamond(X1,multiplication(X2,domain(X3))) = forward_diamond(X1,forward_diamond(X2,X3)),
inference(cp,[status(thm)],[t5908,t148]) ).
cnf(t14791,plain,
forward_diamond(X1,multiplication(X2,domain(X3))) = forward_diamond(X1,forward_diamond(X2,X3)),
inference(orient,[status(thm)],[t5915]) ).
cnf(t25209,plain,
addition(domain(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)],[t169,t14791]) ).
cnf(t152,plain,
forward_diamond(one,X1) = domain(domain(X1)),
inference(cp,[status(thm)],[t148,t39]) ).
cnf(t335,plain,
domain(domain(X1)) = forward_diamond(one,X1),
inference(orient,[status(thm)],[t152]) ).
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(t57,plain,
multiplication(multiplication(X1,X2),X3) = multiplication(X1,multiplication(X2,X3)),
inference(orient,[status(thm)],[t27]) ).
cnf(t2758,plain,
multiplication(domain(X1),multiplication(X1,X2)) = multiplication(X1,X2),
inference(cp,[status(thm)],[t57,t2734]) ).
cnf(t3954,plain,
multiplication(domain(X1),multiplication(X1,X2)) = multiplication(X1,X2),
inference(orient,[status(thm)],[t2758]) ).
cnf(t2748,plain,
domain(X1) = multiplication(forward_diamond(one,X1),domain(X1)),
inference(cp,[status(thm)],[t2734,t335]) ).
cnf(t3280,plain,
multiplication(forward_diamond(one,X1),domain(X1)) = domain(X1),
inference(orient,[status(thm)],[t2748]) ).
cnf(t3973,plain,
multiplication(forward_diamond(one,X1),domain(X1)) = multiplication(domain(forward_diamond(one,X1)),domain(X1)),
inference(cp,[status(thm)],[t3954,t3280]) ).
cnf(t24344,plain,
domain(X1) = multiplication(domain(forward_diamond(one,X1)),domain(X1)),
inference(step,[status(thm)],[t3973,t3280]) ).
cnf(t95,plain,
domain_difference(X1,antidomain(X2)) = multiplication(domain(X1),domain(X2)),
inference(cp,[status(thm)],[t94,t46]) ).
cnf(t1217,plain,
multiplication(domain(X1),domain(X2)) = domain_difference(X1,antidomain(X2)),
inference(orient,[status(thm)],[t95]) ).
cnf(t24345,plain,
domain(X1) = domain_difference(forward_diamond(one,X1),antidomain(X1)),
inference(step,[status(thm)],[t24344,t1217]) ).
cnf(t4671,plain,
domain_difference(forward_diamond(one,X1),antidomain(X1)) = domain(X1),
inference(orient,[status(thm)],[t24345]) ).
cnf(t24421,plain,
domain_difference(forward_diamond(one,X1),c(X1)) = domain(X1),
inference(step,[status(thm)],[t4671,t5637]) ).
cnf(t56,plain,
domain(domain(X1)) = antidomain(c(X1)),
inference(cp,[status(thm)],[t46,t55]) ).
cnf(t327,plain,
antidomain(c(X1)) = domain(domain(X1)),
inference(orient,[status(thm)],[t56]) ).
cnf(t24022,plain,
antidomain(c(X1)) = forward_diamond(one,X1),
inference(step,[status(thm)],[t327,t335]) ).
cnf(t336,plain,
antidomain(c(X1)) = forward_diamond(one,X1),
inference(orient,[status(thm)],[t24022]) ).
cnf(t2836,plain,
antidomain(c(X1)) = domain_difference(forward_diamond(one,X1),c(X1)),
inference(cp,[status(thm)],[t2824,t336]) ).
cnf(t24359,plain,
forward_diamond(one,X1) = domain_difference(forward_diamond(one,X1),c(X1)),
inference(step,[status(thm)],[t2836,t336]) ).
cnf(t4983,plain,
domain_difference(forward_diamond(one,X1),c(X1)) = forward_diamond(one,X1),
inference(orient,[status(thm)],[t24359]) ).
cnf(t24422,plain,
forward_diamond(one,X1) = domain(X1),
inference(step,[status(thm)],[t24421,t4983]) ).
cnf(t5663,plain,
forward_diamond(one,X1) = domain(X1),
inference(rw,[status(thm)],[t24422]) ).
cnf(t5695,plain,
forward_diamond(one,X1) = domain(X1),
inference(orient,[status(thm)],[t5663]) ).
cnf(t24476,plain,
domain(domain(X1)) = domain(X1),
inference(step,[status(thm)],[t335,t5695]) ).
cnf(t5696,plain,
domain(domain(X1)) = domain(X1),
inference(orient,[status(thm)],[t24476]) ).
cnf(t25210,plain,
addition(domain(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)],[t25209,t5696]) ).
cnf(t25211,plain,
addition(domain(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)],[t25210,t5637]) ).
cnf(t155,plain,
c(multiplication(X1,domain(X2))) = antidomain(forward_diamond(X1,X2)),
inference(cp,[status(thm)],[t55,t148]) ).
cnf(t1271,plain,
c(multiplication(X1,domain(X2))) = antidomain(forward_diamond(X1,X2)),
inference(orient,[status(thm)],[t155]) ).
cnf(t24399,plain,
c(multiplication(X1,domain(X2))) = c(forward_diamond(X1,X2)),
inference(step,[status(thm)],[t1271,t5637]) ).
cnf(t5642,plain,
c(multiplication(X1,domain(X2))) = c(forward_diamond(X1,X2)),
inference(orient,[status(thm)],[t24399]) ).
cnf(t1279,plain,
antidomain(forward_diamond(X1,antidomain(X2))) = c(multiplication(X1,c(X2))),
inference(cp,[status(thm)],[t1271,t304]) ).
cnf(t2288,plain,
antidomain(forward_diamond(X1,antidomain(X2))) = c(multiplication(X1,c(X2))),
inference(orient,[status(thm)],[t1279]) ).
cnf(t24457,plain,
c(forward_diamond(X1,antidomain(X2))) = c(multiplication(X1,c(X2))),
inference(step,[status(thm)],[t2288,t5637]) ).
cnf(t24458,plain,
c(forward_diamond(X1,c(X2))) = c(multiplication(X1,c(X2))),
inference(step,[status(thm)],[t24457,t5637]) ).
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(t212,plain,
c(forward_diamond(X1,c(X2))) = forward_box(X1,X2),
inference(orient,[status(thm)],[t20]) ).
cnf(t24459,plain,
forward_box(X1,X2) = c(multiplication(X1,c(X2))),
inference(step,[status(thm)],[t24458,t212]) ).
cnf(t5688,plain,
forward_box(X1,X2) = c(multiplication(X1,c(X2))),
inference(rw,[status(thm)],[t24459]) ).
cnf(t6034,plain,
c(multiplication(X1,c(X2))) = forward_box(X1,X2),
inference(orient,[status(thm)],[t5688]) ).
cnf(t6042,plain,
forward_box(X1,c(X2)) = c(multiplication(X1,domain(X2))),
inference(cp,[status(thm)],[t6034,t5735]) ).
cnf(t24571,plain,
forward_box(X1,c(X2)) = c(forward_diamond(X1,X2)),
inference(step,[status(thm)],[t6042,t5642]) ).
cnf(t6150,plain,
c(forward_diamond(X1,X2)) = forward_box(X1,c(X2)),
inference(orient,[status(thm)],[t24571]) ).
cnf(t24572,plain,
c(multiplication(X1,domain(X2))) = forward_box(X1,c(X2)),
inference(step,[status(thm)],[t5642,t6150]) ).
cnf(t6151,plain,
c(multiplication(X1,domain(X2))) = forward_box(X1,c(X2)),
inference(orient,[status(thm)],[t24572]) ).
cnf(t25212,plain,
addition(domain(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)],[t25211,t6151]) ).
cnf(t306,plain,
c(domain(X1)) = domain(c(X1)),
inference(cp,[status(thm)],[t304,t55]) ).
cnf(t377,plain,
c(domain(X1)) = domain(c(X1)),
inference(orient,[status(thm)],[t306]) ).
cnf(t76,plain,
zero = antidomain(one),
inference(cp,[status(thm)],[t75,t38]) ).
cnf(t226,plain,
antidomain(one) = zero,
inference(orient,[status(thm)],[t76]) ).
cnf(t229,plain,
domain(one) = antidomain(zero),
inference(cp,[status(thm)],[t46,t226]) ).
cnf(t227,plain,
one = addition(domain(one),zero),
inference(cp,[status(thm)],[t121,t226]) ).
cnf(t24006,plain,
one = domain(one),
inference(step,[status(thm)],[t227,t41]) ).
cnf(t230,plain,
domain(one) = one,
inference(orient,[status(thm)],[t24006]) ).
cnf(t24008,plain,
one = antidomain(zero),
inference(step,[status(thm)],[t229,t230]) ).
cnf(t253,plain,
antidomain(zero) = one,
inference(orient,[status(thm)],[t24008]) ).
cnf(t256,plain,
domain(zero) = antidomain(one),
inference(cp,[status(thm)],[t46,t253]) ).
cnf(t24009,plain,
domain(zero) = zero,
inference(step,[status(thm)],[t256,t226]) ).
cnf(t257,plain,
domain(zero) = zero,
inference(orient,[status(thm)],[t24009]) ).
cnf(t260,plain,
c(zero) = antidomain(zero),
inference(cp,[status(thm)],[t55,t257]) ).
cnf(t24010,plain,
c(zero) = one,
inference(step,[status(thm)],[t260,t253]) ).
cnf(t276,plain,
c(zero) = one,
inference(orient,[status(thm)],[t24010]) ).
cnf(t278,plain,
forward_box(X1,zero) = c(forward_diamond(X1,one)),
inference(cp,[status(thm)],[t212,t276]) ).
cnf(t233,plain,
forward_diamond(X1,one) = domain(multiplication(X1,one)),
inference(cp,[status(thm)],[t148,t230]) ).
cnf(t24019,plain,
forward_diamond(X1,one) = domain(X1),
inference(step,[status(thm)],[t233,t38]) ).
cnf(t299,plain,
forward_diamond(X1,one) = domain(X1),
inference(orient,[status(thm)],[t24019]) ).
cnf(t24032,plain,
forward_box(X1,zero) = c(domain(X1)),
inference(step,[status(thm)],[t278,t299]) ).
cnf(t24033,plain,
forward_box(X1,zero) = domain(c(X1)),
inference(step,[status(thm)],[t24032,t377]) ).
cnf(t413,plain,
domain(c(X1)) = forward_box(X1,zero),
inference(orient,[status(thm)],[t24033]) ).
cnf(t24034,plain,
c(domain(X1)) = forward_box(X1,zero),
inference(step,[status(thm)],[t377,t413]) ).
cnf(t414,plain,
c(domain(X1)) = forward_box(X1,zero),
inference(orient,[status(thm)],[t24034]) ).
cnf(t24446,plain,
domain(c(X1)) = c(X1),
inference(step,[status(thm)],[t304,t5637]) ).
cnf(t24447,plain,
forward_box(X1,zero) = c(X1),
inference(step,[status(thm)],[t24446,t413]) ).
cnf(t5681,plain,
forward_box(X1,zero) = c(X1),
inference(rw,[status(thm)],[t24447]) ).
cnf(t5723,plain,
forward_box(X1,zero) = c(X1),
inference(orient,[status(thm)],[t5681]) ).
cnf(t24510,plain,
c(domain(X1)) = c(X1),
inference(step,[status(thm)],[t414,t5723]) ).
cnf(t5724,plain,
c(domain(X1)) = c(X1),
inference(orient,[status(thm)],[t24510]) ).
cnf(t25213,plain,
addition(domain(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)],[t25212,t5724]) ).
cnf(t25214,plain,
addition(domain(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)],[t25213,t14791]) ).
cnf(t25215,plain,
addition(domain(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)],[t25214,t5696]) ).
cnf(t25216,plain,
addition(domain(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)],[t25215,t5637]) ).
cnf(t25217,plain,
addition(domain(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)],[t25216,t6151]) ).
cnf(t25218,plain,
addition(domain(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)],[t25217,t5724]) ).
cnf(t23877,plain,
addition(domain(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)],[t25218]) ).
fof(f26,axiom,
! [X0] : forward_diamond(X0,divergence(X0)) = divergence(X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',divergence1) ).
fof(f26_nnf,plain,
! [X0] : forward_diamond(X0,divergence(X0)) = divergence(X0),
inference(nnf_transformation,[status(thm)],[f26]) ).
fof(f26_sk,plain,
! [X0] : forward_diamond(X0,divergence(X0)) = divergence(X0),
inference(skolemisation,[status(esa)],[f26_nnf]) ).
cnf(c27,plain,
forward_diamond(X0,divergence(X0)) = divergence(X0),
inference(cnf_transformation,[status(esa)],[f26_sk]) ).
cnf(t15,plain,
forward_diamond(X1,divergence(X1)) = divergence(X1),
inference(equality_encoding,[status(esa)],[c27]) ).
cnf(t175,plain,
forward_diamond(X1,divergence(X1)) = divergence(X1),
inference(orient,[status(thm)],[t15]) ).
cnf(t6155,plain,
forward_box(X1,c(divergence(X1))) = c(divergence(X1)),
inference(cp,[status(thm)],[t6150,t175]) ).
cnf(t6237,plain,
forward_box(X1,c(divergence(X1))) = c(divergence(X1)),
inference(orient,[status(thm)],[t6155]) ).
cnf(t23926,plain,
forward_diamond(star(sk0),forward_diamond(domain(divergence(sk0)),forward_box(sk0,c(divergence(sk0))))) = addition(domain(divergence(sk0)),forward_diamond(star(sk0),forward_diamond(domain(divergence(sk0)),c(divergence(sk0))))),
inference(cp,[status(thm)],[t23877,t6237]) ).
cnf(t5738,plain,
domain(multiplication(X1,domain(X2))) = c(c(forward_diamond(X1,X2))),
inference(cp,[status(thm)],[t5735,t5642]) ).
cnf(t24550,plain,
forward_diamond(X1,X2) = c(c(forward_diamond(X1,X2))),
inference(step,[status(thm)],[t5738,t148]) ).
cnf(t24551,plain,
forward_diamond(X1,X2) = domain(forward_diamond(X1,X2)),
inference(step,[status(thm)],[t24550,t5735]) ).
cnf(t5827,plain,
domain(forward_diamond(X1,X2)) = forward_diamond(X1,X2),
inference(orient,[status(thm)],[t24551]) ).
cnf(t5828,plain,
forward_diamond(X1,divergence(X1)) = domain(divergence(X1)),
inference(cp,[status(thm)],[t5827,t175]) ).
cnf(t24552,plain,
divergence(X1) = domain(divergence(X1)),
inference(step,[status(thm)],[t5828,t175]) ).
cnf(t5857,plain,
domain(divergence(X1)) = divergence(X1),
inference(orient,[status(thm)],[t24552]) ).
cnf(t25219,plain,
forward_diamond(star(sk0),forward_diamond(divergence(sk0),forward_box(sk0,c(divergence(sk0))))) = addition(domain(divergence(sk0)),forward_diamond(star(sk0),forward_diamond(domain(divergence(sk0)),c(divergence(sk0))))),
inference(step,[status(thm)],[t23926,t5857]) ).
cnf(t25220,plain,
forward_diamond(star(sk0),forward_diamond(divergence(sk0),c(divergence(sk0)))) = addition(domain(divergence(sk0)),forward_diamond(star(sk0),forward_diamond(domain(divergence(sk0)),c(divergence(sk0))))),
inference(step,[status(thm)],[t25219,t6237]) ).
cnf(t2696,plain,
multiplication(X1,X2) = multiplication(addition(antidomain(X2),X1),X2),
inference(cp,[status(thm)],[t2691,t105]) ).
cnf(t3741,plain,
multiplication(addition(antidomain(X1),X2),X1) = multiplication(X2,X1),
inference(orient,[status(thm)],[t2696]) ).
cnf(t3762,plain,
forward_diamond(addition(antidomain(domain(X1)),X2),X1) = domain(multiplication(X2,domain(X1))),
inference(cp,[status(thm)],[t148,t3741]) ).
cnf(t24374,plain,
forward_diamond(addition(c(X1),X2),X1) = domain(multiplication(X2,domain(X1))),
inference(step,[status(thm)],[t3762,t55]) ).
cnf(t24375,plain,
forward_diamond(addition(c(X1),X2),X1) = forward_diamond(X2,X1),
inference(step,[status(thm)],[t24374,t148]) ).
cnf(t5181,plain,
forward_diamond(addition(c(X1),X2),X1) = forward_diamond(X2,X1),
inference(orient,[status(thm)],[t24375]) ).
fof(f13,axiom,
! [X0,X1] : addition(antidomain(multiplication(X0,X1)),antidomain(multiplication(X0,antidomain(antidomain(X1))))) = antidomain(multiplication(X0,antidomain(antidomain(X1)))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',domain2) ).
fof(f13_nnf,plain,
! [X0,X1] : addition(antidomain(multiplication(X0,X1)),antidomain(multiplication(X0,antidomain(antidomain(X1))))) = antidomain(multiplication(X0,antidomain(antidomain(X1)))),
inference(nnf_transformation,[status(thm)],[f13]) ).
fof(f13_sk,plain,
! [X0,X1] : addition(antidomain(multiplication(X0,X1)),antidomain(multiplication(X0,antidomain(antidomain(X1))))) = antidomain(multiplication(X0,antidomain(antidomain(X1)))),
inference(skolemisation,[status(esa)],[f13_nnf]) ).
cnf(c14,plain,
addition(antidomain(multiplication(X0,X1)),antidomain(multiplication(X0,antidomain(antidomain(X1))))) = antidomain(multiplication(X0,antidomain(antidomain(X1)))),
inference(cnf_transformation,[status(esa)],[f13_sk]) ).
cnf(t32,plain,
addition(antidomain(multiplication(X1,X2)),antidomain(multiplication(X1,antidomain(antidomain(X2))))) = antidomain(multiplication(X1,antidomain(antidomain(X2)))),
inference(equality_encoding,[status(esa)],[c14]) ).
cnf(t23982,plain,
addition(antidomain(multiplication(X1,X2)),antidomain(multiplication(X1,domain(X2)))) = antidomain(multiplication(X1,antidomain(antidomain(X2)))),
inference(step,[status(thm)],[t32,t46]) ).
cnf(t23983,plain,
addition(antidomain(multiplication(X1,X2)),antidomain(multiplication(X1,domain(X2)))) = antidomain(multiplication(X1,domain(X2))),
inference(step,[status(thm)],[t23982,t46]) ).
cnf(t50,plain,
addition(antidomain(multiplication(X1,X2)),antidomain(multiplication(X1,domain(X2)))) = antidomain(multiplication(X1,domain(X2))),
inference(orient,[status(thm)],[t23983]) ).
cnf(t52,plain,
antidomain(multiplication(one,domain(X1))) = addition(antidomain(X1),antidomain(multiplication(one,domain(X1)))),
inference(cp,[status(thm)],[t50,t39]) ).
cnf(t24071,plain,
antidomain(domain(X1)) = addition(antidomain(X1),antidomain(multiplication(one,domain(X1)))),
inference(step,[status(thm)],[t52,t39]) ).
cnf(t24072,plain,
c(X1) = addition(antidomain(X1),antidomain(multiplication(one,domain(X1)))),
inference(step,[status(thm)],[t24071,t55]) ).
cnf(t24073,plain,
c(X1) = addition(antidomain(X1),antidomain(domain(X1))),
inference(step,[status(thm)],[t24072,t39]) ).
cnf(t24074,plain,
c(X1) = addition(antidomain(X1),c(X1)),
inference(step,[status(thm)],[t24073,t55]) ).
cnf(t24075,plain,
c(X1) = addition(c(X1),antidomain(X1)),
inference(step,[status(thm)],[t24074,t105]) ).
cnf(t689,plain,
addition(c(X1),antidomain(X1)) = c(X1),
inference(orient,[status(thm)],[t24075]) ).
cnf(t5182,plain,
forward_diamond(antidomain(X1),X1) = forward_diamond(c(X1),X1),
inference(cp,[status(thm)],[t5181,t689]) ).
cnf(t150,plain,
forward_diamond(antidomain(domain(X1)),X1) = domain(zero),
inference(cp,[status(thm)],[t148,t75]) ).
cnf(t24025,plain,
forward_diamond(c(X1),X1) = domain(zero),
inference(step,[status(thm)],[t150,t55]) ).
cnf(t24026,plain,
forward_diamond(c(X1),X1) = zero,
inference(step,[status(thm)],[t24025,t257]) ).
cnf(t384,plain,
forward_diamond(c(X1),X1) = zero,
inference(orient,[status(thm)],[t24026]) ).
cnf(t24376,plain,
forward_diamond(antidomain(X1),X1) = zero,
inference(step,[status(thm)],[t5182,t384]) ).
cnf(t5202,plain,
forward_diamond(antidomain(X1),X1) = zero,
inference(orient,[status(thm)],[t24376]) ).
cnf(t5211,plain,
zero = forward_diamond(domain(X1),antidomain(X1)),
inference(cp,[status(thm)],[t5202,t46]) ).
cnf(t5217,plain,
forward_diamond(domain(X1),antidomain(X1)) = zero,
inference(orient,[status(thm)],[t5211]) ).
cnf(t24418,plain,
forward_diamond(domain(X1),c(X1)) = zero,
inference(step,[status(thm)],[t5217,t5637]) ).
cnf(t5660,plain,
forward_diamond(domain(X1),c(X1)) = zero,
inference(rw,[status(thm)],[t24418]) ).
cnf(t5920,plain,
forward_diamond(domain(X1),c(X1)) = zero,
inference(orient,[status(thm)],[t5660]) ).
cnf(t5921,plain,
zero = forward_diamond(divergence(X1),c(divergence(X1))),
inference(cp,[status(thm)],[t5920,t5857]) ).
cnf(t6289,plain,
forward_diamond(divergence(X1),c(divergence(X1))) = zero,
inference(orient,[status(thm)],[t5921]) ).
cnf(t25221,plain,
forward_diamond(star(sk0),zero) = addition(domain(divergence(sk0)),forward_diamond(star(sk0),forward_diamond(domain(divergence(sk0)),c(divergence(sk0))))),
inference(step,[status(thm)],[t25220,t6289]) ).
cnf(t261,plain,
forward_diamond(X1,zero) = domain(multiplication(X1,zero)),
inference(cp,[status(thm)],[t148,t257]) ).
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(t71,plain,
multiplication(X1,zero) = zero,
inference(orient,[status(thm)],[t6]) ).
cnf(t24013,plain,
forward_diamond(X1,zero) = domain(zero),
inference(step,[status(thm)],[t261,t71]) ).
cnf(t24014,plain,
forward_diamond(X1,zero) = zero,
inference(step,[status(thm)],[t24013,t257]) ).
cnf(t284,plain,
forward_diamond(X1,zero) = zero,
inference(orient,[status(thm)],[t24014]) ).
cnf(t25222,plain,
zero = addition(domain(divergence(sk0)),forward_diamond(star(sk0),forward_diamond(domain(divergence(sk0)),c(divergence(sk0))))),
inference(step,[status(thm)],[t25221,t284]) ).
cnf(t25223,plain,
zero = addition(divergence(sk0),forward_diamond(star(sk0),forward_diamond(domain(divergence(sk0)),c(divergence(sk0))))),
inference(step,[status(thm)],[t25222,t5857]) ).
cnf(t96,plain,
domain_difference(X1,domain(X2)) = multiplication(domain(X1),c(X2)),
inference(cp,[status(thm)],[t94,t55]) ).
cnf(t1245,plain,
multiplication(domain(X1),c(X2)) = domain_difference(X1,domain(X2)),
inference(orient,[status(thm)],[t96]) ).
cnf(t1323,plain,
forward_diamond(domain(X1),antidomain(X2)) = domain(domain_difference(X1,domain(X2))),
inference(cp,[status(thm)],[t1322,t1245]) ).
cnf(t2345,plain,
domain(domain_difference(X1,domain(X2))) = forward_diamond(domain(X1),antidomain(X2)),
inference(orient,[status(thm)],[t1323]) ).
cnf(t24409,plain,
domain(domain_difference(X1,domain(X2))) = forward_diamond(domain(X1),c(X2)),
inference(step,[status(thm)],[t2345,t5637]) ).
cnf(t5652,plain,
domain(domain_difference(X1,domain(X2))) = forward_diamond(domain(X1),c(X2)),
inference(orient,[status(thm)],[t24409]) ).
cnf(t24448,plain,
multiplication(domain(X1),c(X2)) = domain_difference(X1,X2),
inference(step,[status(thm)],[t94,t5637]) ).
cnf(t24449,plain,
domain_difference(X1,domain(X2)) = domain_difference(X1,X2),
inference(step,[status(thm)],[t24448,t1245]) ).
cnf(t5682,plain,
domain_difference(X1,domain(X2)) = domain_difference(X1,X2),
inference(rw,[status(thm)],[t24449]) ).
cnf(t5805,plain,
domain_difference(X1,domain(X2)) = domain_difference(X1,X2),
inference(orient,[status(thm)],[t5682]) ).
cnf(t24548,plain,
domain(domain_difference(X1,X2)) = forward_diamond(domain(X1),c(X2)),
inference(step,[status(thm)],[t5652,t5805]) ).
cnf(t5817,plain,
domain(domain_difference(X1,X2)) = forward_diamond(domain(X1),c(X2)),
inference(rw,[status(thm)],[t24548]) ).
cnf(t6814,plain,
forward_diamond(domain(X1),c(X2)) = domain(domain_difference(X1,X2)),
inference(orient,[status(thm)],[t5817]) ).
cnf(t25224,plain,
zero = addition(divergence(sk0),forward_diamond(star(sk0),domain(domain_difference(divergence(sk0),divergence(sk0))))),
inference(step,[status(thm)],[t25223,t6814]) ).
cnf(t6818,plain,
domain(domain_difference(divergence(X1),X2)) = forward_diamond(divergence(X1),c(X2)),
inference(cp,[status(thm)],[t6814,t5857]) ).
cnf(t7301,plain,
domain(domain_difference(divergence(X1),X2)) = forward_diamond(divergence(X1),c(X2)),
inference(orient,[status(thm)],[t6818]) ).
cnf(t25225,plain,
zero = addition(divergence(sk0),forward_diamond(star(sk0),forward_diamond(divergence(sk0),c(divergence(sk0))))),
inference(step,[status(thm)],[t25224,t7301]) ).
cnf(t25226,plain,
zero = addition(divergence(sk0),forward_diamond(star(sk0),zero)),
inference(step,[status(thm)],[t25225,t6289]) ).
cnf(t25227,plain,
zero = addition(divergence(sk0),zero),
inference(step,[status(thm)],[t25226,t284]) ).
cnf(t25228,plain,
zero = divergence(sk0),
inference(step,[status(thm)],[t25227,t41]) ).
cnf(t23966,plain,
divergence(sk0) = zero,
inference(orient,[status(thm)],[t25228]) ).
cnf(c30,plain,
divergence(sk0) != zero,
inference(cnf_transformation,[status(esa)],[f28_sk]) ).
cnf(goal_0,negated_conjecture,
divergence(sk0) != zero,
inference(equality_encoding,[status(esa)],[c30]) ).
cnf(g0_0,plain,
zero != zero,
inference(rw,[status(thm)],[goal_0,t23966]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : KLE131+1 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.08/0.34 % Computer : n011.cluster.edu
% 0.08/0.34 % Model : x86_64 x86_64
% 0.08/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.34 % Memory : 8046.5625MB
% 0.08/0.34 % OS : Linux 6.8.0-71-generic
% 0.08/0.34 % CPULimit : 300
% 0.08/0.34 % WCLimit : 300
% 0.08/0.34 % DateTime : Wed Sep 23 19:01:42 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.08/0.35 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 22.72/3.36 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 22.72/3.36 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------