%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : REL034+2 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n017.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 02:35:56 PM UTC 2026
% Result : Theorem 256.56s 54.25s
% Output : Proof 256.56s
% Verified :
% SZS Type : Refutation
% Derivation depth : 171
% Number of leaves : 15
% Syntax : Number of formulae : 703 ( 699 unt; 0 def)
% Number of atoms : 707 ( 706 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 13 ( 9 ~; 0 |; 2 &)
% ( 0 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 1 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 11 ( 11 usr; 6 con; 0-2 aty)
% Number of variables : 989 ( 149 sgn 90 !; 3 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f6,axiom,
! [X0,X1,X2] : composition(join(X0,X1),X2) = join(composition(X0,X2),composition(X1,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',composition_distributivity) ).
fof(f6_nnf,plain,
! [X0,X1,X2] : composition(join(X0,X1),X2) = join(composition(X0,X2),composition(X1,X2)),
inference(nnf_transformation,[status(thm)],[f6]) ).
fof(f6_sk,plain,
! [X0,X1,X2] : composition(join(X0,X1),X2) = join(composition(X0,X2),composition(X1,X2)),
inference(skolemisation,[status(esa)],[f6_nnf]) ).
cnf(c6,plain,
composition(join(X0,X1),X2) = join(composition(X0,X2),composition(X1,X2)),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(t11,plain,
join(composition(X1,X2),composition(X3,X2)) = composition(join(X1,X3),X2),
inference(equality_encoding,[status(esa)],[c6]) ).
cnf(t24,plain,
join(composition(X1,X2),composition(X3,X2)) = composition(join(X1,X3),X2),
inference(orient,[status(thm)],[t11]) ).
fof(f1,axiom,
! [X0,X1,X2] : join(X0,join(X1,X2)) = join(join(X0,X1),X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',maddux2_join_associativity) ).
fof(f1_nnf,plain,
! [X0,X1,X2] : join(X0,join(X1,X2)) = join(join(X0,X1),X2),
inference(nnf_transformation,[status(thm)],[f1]) ).
fof(f1_sk,plain,
! [X0,X1,X2] : join(X0,join(X1,X2)) = join(join(X0,X1),X2),
inference(skolemisation,[status(esa)],[f1_nnf]) ).
cnf(c1,plain,
join(X0,join(X1,X2)) = join(join(X0,X1),X2),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(t10,plain,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
inference(equality_encoding,[status(esa)],[c1]) ).
cnf(t51,plain,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
inference(orient,[status(thm)],[t10]) ).
fof(f10,axiom,
! [X0,X1] : join(composition(converse(X0),complement(composition(X0,X1))),complement(X1)) = complement(X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',converse_cancellativity) ).
fof(f10_nnf,plain,
! [X0,X1] : join(composition(converse(X0),complement(composition(X0,X1))),complement(X1)) = complement(X1),
inference(nnf_transformation,[status(thm)],[f10]) ).
fof(f10_sk,plain,
! [X0,X1] : join(composition(converse(X0),complement(composition(X0,X1))),complement(X1)) = complement(X1),
inference(skolemisation,[status(esa)],[f10_nnf]) ).
cnf(c10,plain,
join(composition(converse(X0),complement(composition(X0,X1))),complement(X1)) = complement(X1),
inference(cnf_transformation,[status(esa)],[f10_sk]) ).
cnf(t12,plain,
join(composition(converse(X1),complement(composition(X1,X2))),complement(X2)) = complement(X2),
inference(equality_encoding,[status(esa)],[c10]) ).
fof(f0,axiom,
! [X0,X1] : join(X0,X1) = join(X1,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',maddux1_join_commutativity) ).
fof(f0_nnf,plain,
! [X0,X1] : join(X0,X1) = join(X1,X0),
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
! [X0,X1] : join(X0,X1) = join(X1,X0),
inference(skolemisation,[status(esa)],[f0_nnf]) ).
cnf(c0,plain,
join(X0,X1) = join(X1,X0),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(t5,plain,
join(X1,X2) = join(X2,X1),
inference(equality_encoding,[status(esa)],[c0]) ).
cnf(t48,plain,
join(X1,X2) = join(X2,X1),
inference(orient,[status(thm)],[t5]) ).
cnf(t565648,plain,
join(complement(X2),composition(converse(X1),complement(composition(X1,X2)))) = complement(X2),
inference(step,[status(thm)],[t12,t48]) ).
cnf(t59,plain,
join(complement(X1),composition(converse(X2),complement(composition(X2,X1)))) = complement(X1),
inference(orient,[status(thm)],[t565648]) ).
fof(f9,axiom,
! [X0,X1] : converse(composition(X0,X1)) = composition(converse(X1),converse(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',converse_multiplicativity) ).
fof(f9_nnf,plain,
! [X0,X1] : converse(composition(X0,X1)) = composition(converse(X1),converse(X0)),
inference(nnf_transformation,[status(thm)],[f9]) ).
fof(f9_sk,plain,
! [X0,X1] : converse(composition(X0,X1)) = composition(converse(X1),converse(X0)),
inference(skolemisation,[status(esa)],[f9_nnf]) ).
cnf(c9,plain,
converse(composition(X0,X1)) = composition(converse(X1),converse(X0)),
inference(cnf_transformation,[status(esa)],[f9_sk]) ).
cnf(t7,plain,
composition(converse(X1),converse(X2)) = converse(composition(X2,X1)),
inference(equality_encoding,[status(esa)],[c9]) ).
cnf(t27,plain,
composition(converse(X1),converse(X2)) = converse(composition(X2,X1)),
inference(orient,[status(thm)],[t7]) ).
fof(f7,axiom,
! [X0] : converse(converse(X0)) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',converse_idempotence) ).
fof(f7_nnf,plain,
! [X0] : converse(converse(X0)) = X0,
inference(nnf_transformation,[status(thm)],[f7]) ).
fof(f7_sk,plain,
! [X0] : converse(converse(X0)) = X0,
inference(skolemisation,[status(esa)],[f7_nnf]) ).
cnf(c7,plain,
converse(converse(X0)) = X0,
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
cnf(t2,plain,
converse(converse(X1)) = X1,
inference(equality_encoding,[status(esa)],[c7]) ).
cnf(t21,plain,
converse(converse(X1)) = X1,
inference(orient,[status(thm)],[t2]) ).
cnf(t29,plain,
converse(composition(converse(X1),X2)) = composition(converse(X2),X1),
inference(cp,[status(thm)],[t27,t21]) ).
cnf(t162,plain,
converse(composition(converse(X1),X2)) = composition(converse(X2),X1),
inference(orient,[status(thm)],[t29]) ).
fof(f5,axiom,
! [X0] : composition(X0,one) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',composition_identity) ).
fof(f5_nnf,plain,
! [X0] : composition(X0,one) = X0,
inference(nnf_transformation,[status(thm)],[f5]) ).
fof(f5_sk,plain,
! [X0] : composition(X0,one) = X0,
inference(skolemisation,[status(esa)],[f5_nnf]) ).
cnf(c5,plain,
composition(X0,one) = X0,
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(t0,plain,
composition(X1,one) = X1,
inference(equality_encoding,[status(esa)],[c5]) ).
cnf(t17,plain,
composition(X1,one) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t163,plain,
composition(converse(one),X1) = converse(converse(X1)),
inference(cp,[status(thm)],[t162,t17]) ).
cnf(t565653,plain,
composition(converse(one),X1) = X1,
inference(step,[status(thm)],[t163,t21]) ).
cnf(t175,plain,
composition(converse(one),X1) = X1,
inference(orient,[status(thm)],[t565653]) ).
cnf(t176,plain,
one = converse(one),
inference(cp,[status(thm)],[t175,t17]) ).
cnf(t185,plain,
converse(one) = one,
inference(orient,[status(thm)],[t176]) ).
cnf(t565654,plain,
composition(one,X1) = X1,
inference(step,[status(thm)],[t175,t185]) ).
cnf(t195,plain,
composition(one,X1) = X1,
inference(rw,[status(thm)],[t565654]) ).
cnf(t196,plain,
composition(one,X1) = X1,
inference(orient,[status(thm)],[t195]) ).
cnf(t199,plain,
complement(X1) = join(complement(X1),composition(converse(one),complement(X1))),
inference(cp,[status(thm)],[t59,t196]) ).
cnf(t565656,plain,
complement(X1) = join(complement(X1),composition(one,complement(X1))),
inference(step,[status(thm)],[t199,t185]) ).
cnf(t565657,plain,
complement(X1) = join(complement(X1),complement(X1)),
inference(step,[status(thm)],[t565656,t196]) ).
cnf(t225,plain,
join(complement(X1),complement(X1)) = complement(X1),
inference(orient,[status(thm)],[t565657]) ).
fof(f3,axiom,
! [X0,X1] : meet(X0,X1) = complement(join(complement(X0),complement(X1))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',maddux4_definiton_of_meet) ).
fof(f3_nnf,plain,
! [X0,X1] : meet(X0,X1) = complement(join(complement(X0),complement(X1))),
inference(nnf_transformation,[status(thm)],[f3]) ).
fof(f3_sk,plain,
! [X0,X1] : meet(X0,X1) = complement(join(complement(X0),complement(X1))),
inference(skolemisation,[status(esa)],[f3_nnf]) ).
cnf(c3,plain,
meet(X0,X1) = complement(join(complement(X0),complement(X1))),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(t6,plain,
complement(join(complement(X1),complement(X2))) = meet(X1,X2),
inference(equality_encoding,[status(esa)],[c3]) ).
cnf(t91,plain,
complement(join(complement(X1),complement(X2))) = meet(X1,X2),
inference(orient,[status(thm)],[t6]) ).
cnf(t226,plain,
complement(join(complement(X1),complement(X2))) = join(meet(X1,X2),complement(join(complement(X1),complement(X2)))),
inference(cp,[status(thm)],[t225,t91]) ).
cnf(t565685,plain,
meet(X1,X2) = join(meet(X1,X2),complement(join(complement(X1),complement(X2)))),
inference(step,[status(thm)],[t226,t91]) ).
cnf(t565686,plain,
meet(X1,X2) = join(meet(X1,X2),meet(X1,X2)),
inference(step,[status(thm)],[t565685,t91]) ).
cnf(t552,plain,
join(meet(X1,X2),meet(X1,X2)) = meet(X1,X2),
inference(orient,[status(thm)],[t565686]) ).
cnf(t93,plain,
meet(X1,X2) = complement(join(complement(X2),complement(X1))),
inference(cp,[status(thm)],[t91,t48]) ).
cnf(t565651,plain,
meet(X1,X2) = meet(X2,X1),
inference(step,[status(thm)],[t93,t91]) ).
cnf(t112,plain,
meet(X1,X2) = meet(X2,X1),
inference(orient,[status(thm)],[t565651]) ).
cnf(t553,plain,
meet(X1,X2) = join(meet(X2,X1),meet(X1,X2)),
inference(cp,[status(thm)],[t552,t112]) ).
cnf(t585,plain,
join(meet(X1,X2),meet(X2,X1)) = meet(X2,X1),
inference(orient,[status(thm)],[t553]) ).
fof(f2,axiom,
! [X0,X1] : X0 = join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',maddux3_a_kind_of_de_Morgan) ).
fof(f2_nnf,plain,
! [X0,X1] : X0 = join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))),
inference(nnf_transformation,[status(thm)],[f2]) ).
fof(f2_sk,plain,
! [X0,X1] : X0 = join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))),
inference(skolemisation,[status(esa)],[f2_nnf]) ).
cnf(c2,plain,
X0 = join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(t13,plain,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
inference(equality_encoding,[status(esa)],[c2]) ).
cnf(t18,plain,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
inference(orient,[status(thm)],[t13]) ).
cnf(t50,plain,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
inference(rw,[status(thm)],[t18]) ).
cnf(t566267,plain,
join(complement(join(complement(X1),X2)),complement(join(complement(X1),complement(X2)))) = X1,
inference(step,[status(thm)],[t50,t48]) ).
cnf(t566268,plain,
join(complement(join(complement(X1),X2)),meet(X1,X2)) = X1,
inference(step,[status(thm)],[t566267,t91]) ).
cnf(t566269,plain,
join(meet(X1,X2),complement(join(complement(X1),X2))) = X1,
inference(step,[status(thm)],[t566268,t48]) ).
cnf(t19946,plain,
join(meet(X1,X2),complement(join(complement(X1),X2))) = X1,
inference(orient,[status(thm)],[t566269]) ).
fof(f12,axiom,
! [X0] : zero = meet(X0,complement(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',def_zero) ).
fof(f12_nnf,plain,
! [X0] : zero = meet(X0,complement(X0)),
inference(nnf_transformation,[status(thm)],[f12]) ).
fof(f12_sk,plain,
! [X0] : zero = meet(X0,complement(X0)),
inference(skolemisation,[status(esa)],[f12_nnf]) ).
cnf(c12,plain,
zero = meet(X0,complement(X0)),
inference(cnf_transformation,[status(esa)],[f12_sk]) ).
cnf(t4,plain,
meet(X1,complement(X1)) = zero,
inference(equality_encoding,[status(esa)],[c12]) ).
cnf(t98,plain,
meet(X1,complement(X1)) = zero,
inference(orient,[status(thm)],[t4]) ).
cnf(t19947,plain,
X1 = join(zero,complement(join(complement(X1),complement(X1)))),
inference(cp,[status(thm)],[t19946,t98]) ).
cnf(t566270,plain,
X1 = join(zero,meet(X1,X1)),
inference(step,[status(thm)],[t19947,t91]) ).
cnf(t20167,plain,
join(zero,meet(X1,X1)) = X1,
inference(orient,[status(thm)],[t566270]) ).
fof(f11,axiom,
! [X0] : top = join(X0,complement(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',def_top) ).
fof(f11_nnf,plain,
! [X0] : top = join(X0,complement(X0)),
inference(nnf_transformation,[status(thm)],[f11]) ).
fof(f11_sk,plain,
! [X0] : top = join(X0,complement(X0)),
inference(skolemisation,[status(esa)],[f11_nnf]) ).
cnf(c11,plain,
top = join(X0,complement(X0)),
inference(cnf_transformation,[status(esa)],[f11_sk]) ).
cnf(t3,plain,
join(X1,complement(X1)) = top,
inference(equality_encoding,[status(esa)],[c11]) ).
cnf(t56,plain,
join(X1,complement(X1)) = top,
inference(orient,[status(thm)],[t3]) ).
cnf(t92,plain,
meet(X1,complement(X1)) = complement(top),
inference(cp,[status(thm)],[t91,t56]) ).
cnf(t565649,plain,
zero = complement(top),
inference(step,[status(thm)],[t92,t98]) ).
cnf(t103,plain,
complement(top) = zero,
inference(orient,[status(thm)],[t565649]) ).
cnf(t229,plain,
complement(top) = join(zero,complement(top)),
inference(cp,[status(thm)],[t225,t103]) ).
cnf(t565658,plain,
zero = join(zero,complement(top)),
inference(step,[status(thm)],[t229,t103]) ).
cnf(t565659,plain,
zero = join(zero,zero),
inference(step,[status(thm)],[t565658,t103]) ).
cnf(t236,plain,
join(zero,zero) = zero,
inference(orient,[status(thm)],[t565659]) ).
cnf(t237,plain,
join(zero,join(zero,X1)) = join(zero,X1),
inference(cp,[status(thm)],[t51,t236]) ).
cnf(t255,plain,
join(zero,join(zero,X1)) = join(zero,X1),
inference(orient,[status(thm)],[t237]) ).
cnf(t20177,plain,
join(zero,meet(X1,X1)) = join(zero,X1),
inference(cp,[status(thm)],[t255,t20167]) ).
cnf(t566297,plain,
X1 = join(zero,X1),
inference(step,[status(thm)],[t20177,t20167]) ).
cnf(t20280,plain,
join(zero,X1) = X1,
inference(orient,[status(thm)],[t566297]) ).
cnf(t566310,plain,
meet(X1,X1) = X1,
inference(step,[status(thm)],[t20167,t20280]) ).
cnf(t20395,plain,
meet(X1,X1) = X1,
inference(rw,[status(thm)],[t566310]) ).
cnf(t20487,plain,
meet(X1,X1) = X1,
inference(orient,[status(thm)],[t20395]) ).
cnf(t20488,plain,
meet(X1,X1) = join(X1,meet(X1,X1)),
inference(cp,[status(thm)],[t585,t20487]) ).
cnf(t566372,plain,
X1 = join(X1,meet(X1,X1)),
inference(step,[status(thm)],[t20488,t20487]) ).
cnf(t566373,plain,
X1 = join(X1,X1),
inference(step,[status(thm)],[t566372,t20487]) ).
cnf(t20552,plain,
join(X1,X1) = X1,
inference(orient,[status(thm)],[t566373]) ).
cnf(t20556,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(cp,[status(thm)],[t51,t20552]) ).
cnf(t20929,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(orient,[status(thm)],[t20556]) ).
cnf(t20951,plain,
join(meet(X1,X2),complement(join(complement(X1),X2))) = join(meet(X1,X2),X1),
inference(cp,[status(thm)],[t20929,t19946]) ).
cnf(t566423,plain,
X1 = join(meet(X1,X2),X1),
inference(step,[status(thm)],[t20951,t19946]) ).
cnf(t566424,plain,
X1 = join(X1,meet(X1,X2)),
inference(step,[status(thm)],[t566423,t48]) ).
cnf(t20965,plain,
join(X1,meet(X1,X2)) = X1,
inference(orient,[status(thm)],[t566424]) ).
fof(f4,axiom,
! [X0,X1,X2] : composition(X0,composition(X1,X2)) = composition(composition(X0,X1),X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',composition_associativity) ).
fof(f4_nnf,plain,
! [X0,X1,X2] : composition(X0,composition(X1,X2)) = composition(composition(X0,X1),X2),
inference(nnf_transformation,[status(thm)],[f4]) ).
fof(f4_sk,plain,
! [X0,X1,X2] : composition(X0,composition(X1,X2)) = composition(composition(X0,X1),X2),
inference(skolemisation,[status(esa)],[f4_nnf]) ).
cnf(c4,plain,
composition(X0,composition(X1,X2)) = composition(composition(X0,X1),X2),
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(t9,plain,
composition(composition(X1,X2),X3) = composition(X1,composition(X2,X3)),
inference(equality_encoding,[status(esa)],[c4]) ).
cnf(t22,plain,
composition(composition(X1,X2),X3) = composition(X1,composition(X2,X3)),
inference(orient,[status(thm)],[t9]) ).
cnf(t20967,plain,
X1 = join(X1,meet(X2,X1)),
inference(cp,[status(thm)],[t20965,t112]) ).
cnf(t21006,plain,
join(X1,meet(X2,X1)) = X1,
inference(orient,[status(thm)],[t20967]) ).
cnf(t21013,plain,
join(X1,join(meet(X2,X1),X3)) = join(X1,X3),
inference(cp,[status(thm)],[t51,t21006]) ).
cnf(t26619,plain,
join(X1,join(meet(X2,X1),X3)) = join(X1,X3),
inference(orient,[status(thm)],[t21013]) ).
cnf(t235,plain,
meet(X1,X1) = complement(complement(X1)),
inference(cp,[status(thm)],[t91,t225]) ).
cnf(t242,plain,
meet(X1,X1) = complement(complement(X1)),
inference(orient,[status(thm)],[t235]) ).
cnf(t252,plain,
meet(X1,complement(X2)) = complement(join(complement(X1),meet(X2,X2))),
inference(cp,[status(thm)],[t91,t242]) ).
cnf(t1333,plain,
complement(join(complement(X1),meet(X2,X2))) = meet(X1,complement(X2)),
inference(orient,[status(thm)],[t252]) ).
cnf(t566359,plain,
complement(join(complement(X1),X2)) = meet(X1,complement(X2)),
inference(step,[status(thm)],[t1333,t20487]) ).
cnf(t20527,plain,
complement(join(complement(X1),X2)) = meet(X1,complement(X2)),
inference(rw,[status(thm)],[t566359]) ).
cnf(t21385,plain,
complement(join(complement(X1),X2)) = meet(X1,complement(X2)),
inference(orient,[status(thm)],[t20527]) ).
cnf(t566446,plain,
join(meet(X1,X2),meet(X1,complement(X2))) = X1,
inference(step,[status(thm)],[t19946,t21385]) ).
cnf(t21508,plain,
join(meet(X1,X2),meet(X1,complement(X2))) = X1,
inference(rw,[status(thm)],[t566446]) ).
cnf(t31556,plain,
join(meet(X1,X2),meet(X1,complement(X2))) = X1,
inference(orient,[status(thm)],[t21508]) ).
cnf(t31622,plain,
join(X1,meet(X2,complement(X1))) = join(X1,X2),
inference(cp,[status(thm)],[t26619,t31556]) ).
cnf(t31781,plain,
join(X1,meet(X2,complement(X1))) = join(X1,X2),
inference(orient,[status(thm)],[t31622]) ).
cnf(t31799,plain,
join(X1,X2) = join(X1,meet(complement(X1),X2)),
inference(cp,[status(thm)],[t31781,t112]) ).
cnf(t32360,plain,
join(X1,meet(complement(X1),X2)) = join(X1,X2),
inference(orient,[status(thm)],[t31799]) ).
cnf(t566352,plain,
X1 = complement(complement(X1)),
inference(step,[status(thm)],[t242,t20487]) ).
cnf(t20520,plain,
X1 = complement(complement(X1)),
inference(rw,[status(thm)],[t566352]) ).
cnf(t20605,plain,
complement(complement(X1)) = X1,
inference(orient,[status(thm)],[t20520]) ).
cnf(t32386,plain,
join(complement(X1),X2) = join(complement(X1),meet(X1,X2)),
inference(cp,[status(thm)],[t32360,t20605]) ).
cnf(t33597,plain,
join(complement(X1),meet(X1,X2)) = join(complement(X1),X2),
inference(orient,[status(thm)],[t32386]) ).
fof(f13,axiom,
! [X0,X1,X2] : join(meet(composition(X0,X1),X2),composition(meet(X0,composition(X2,converse(X1))),meet(X1,composition(converse(X0),X2)))) = composition(meet(X0,composition(X2,converse(X1))),meet(X1,composition(converse(X0),X2))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dedekind_law) ).
fof(f13_nnf,plain,
! [X0,X1,X2] : join(meet(composition(X0,X1),X2),composition(meet(X0,composition(X2,converse(X1))),meet(X1,composition(converse(X0),X2)))) = composition(meet(X0,composition(X2,converse(X1))),meet(X1,composition(converse(X0),X2))),
inference(nnf_transformation,[status(thm)],[f13]) ).
fof(f13_sk,plain,
! [X0,X1,X2] : join(meet(composition(X0,X1),X2),composition(meet(X0,composition(X2,converse(X1))),meet(X1,composition(converse(X0),X2)))) = composition(meet(X0,composition(X2,converse(X1))),meet(X1,composition(converse(X0),X2))),
inference(skolemisation,[status(esa)],[f13_nnf]) ).
cnf(c13,plain,
join(meet(composition(X0,X1),X2),composition(meet(X0,composition(X2,converse(X1))),meet(X1,composition(converse(X0),X2)))) = composition(meet(X0,composition(X2,converse(X1))),meet(X1,composition(converse(X0),X2))),
inference(cnf_transformation,[status(esa)],[f13_sk]) ).
cnf(t16,plain,
join(meet(composition(X1,X2),X3),composition(meet(X1,composition(X3,converse(X2))),meet(X2,composition(converse(X1),X3)))) = composition(meet(X1,composition(X3,converse(X2))),meet(X2,composition(converse(X1),X3))),
inference(equality_encoding,[status(esa)],[c13]) ).
cnf(t33,plain,
join(meet(composition(X1,X2),X3),composition(meet(X1,composition(X3,converse(X2))),meet(X2,composition(converse(X1),X3)))) = composition(meet(X1,composition(X3,converse(X2))),meet(X2,composition(converse(X1),X3))),
inference(orient,[status(thm)],[t16]) ).
cnf(t39,plain,
composition(meet(X1,composition(X2,converse(converse(X3)))),meet(converse(X3),composition(converse(X1),X2))) = join(meet(composition(X1,converse(X3)),X2),composition(meet(X1,composition(X2,X3)),meet(converse(X3),composition(converse(X1),X2)))),
inference(cp,[status(thm)],[t33,t21]) ).
cnf(t566093,plain,
composition(meet(X1,composition(X2,X3)),meet(converse(X3),composition(converse(X1),X2))) = join(meet(composition(X1,converse(X3)),X2),composition(meet(X1,composition(X2,X3)),meet(converse(X3),composition(converse(X1),X2)))),
inference(step,[status(thm)],[t39,t21]) ).
cnf(t10630,plain,
join(meet(composition(X1,converse(X2)),X3),composition(meet(X1,composition(X3,X2)),meet(converse(X2),composition(converse(X1),X3)))) = composition(meet(X1,composition(X3,X2)),meet(converse(X2),composition(converse(X1),X3))),
inference(orient,[status(thm)],[t566093]) ).
fof(f8,axiom,
! [X0,X1] : converse(join(X0,X1)) = join(converse(X0),converse(X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',converse_additivity) ).
fof(f8_nnf,plain,
! [X0,X1] : converse(join(X0,X1)) = join(converse(X0),converse(X1)),
inference(nnf_transformation,[status(thm)],[f8]) ).
fof(f8_sk,plain,
! [X0,X1] : converse(join(X0,X1)) = join(converse(X0),converse(X1)),
inference(skolemisation,[status(esa)],[f8_nnf]) ).
cnf(c8,plain,
converse(join(X0,X1)) = join(converse(X0),converse(X1)),
inference(cnf_transformation,[status(esa)],[f8_sk]) ).
cnf(t8,plain,
join(converse(X1),converse(X2)) = converse(join(X1,X2)),
inference(equality_encoding,[status(esa)],[c8]) ).
cnf(t66,plain,
join(converse(X1),converse(X2)) = converse(join(X1,X2)),
inference(orient,[status(thm)],[t8]) ).
cnf(t70,plain,
join(converse(X1),join(converse(X2),X3)) = join(converse(join(X1,X2)),X3),
inference(cp,[status(thm)],[t51,t66]) ).
cnf(t3319,plain,
join(converse(X1),join(converse(X2),X3)) = join(converse(join(X1,X2)),X3),
inference(orient,[status(thm)],[t70]) ).
cnf(t58,plain,
join(X1,join(complement(X1),X2)) = join(top,X2),
inference(cp,[status(thm)],[t51,t56]) ).
cnf(t356,plain,
join(X1,join(complement(X1),X2)) = join(top,X2),
inference(orient,[status(thm)],[t58]) ).
cnf(t365,plain,
join(top,X1) = join(X2,join(X1,complement(X2))),
inference(cp,[status(thm)],[t356,t48]) ).
cnf(t250,plain,
top = join(complement(X1),meet(X1,X1)),
inference(cp,[status(thm)],[t56,t242]) ).
cnf(t266,plain,
join(complement(X1),meet(X1,X1)) = top,
inference(orient,[status(thm)],[t250]) ).
cnf(t360,plain,
join(top,meet(X1,X1)) = join(X1,top),
inference(cp,[status(thm)],[t356,t266]) ).
cnf(t362,plain,
join(top,complement(X1)) = join(X1,complement(X1)),
inference(cp,[status(thm)],[t356,t225]) ).
cnf(t565665,plain,
join(top,complement(X1)) = top,
inference(step,[status(thm)],[t362,t56]) ).
cnf(t374,plain,
join(top,complement(X1)) = top,
inference(orient,[status(thm)],[t565665]) ).
cnf(t375,plain,
top = join(top,meet(X1,X2)),
inference(cp,[status(thm)],[t374,t91]) ).
cnf(t382,plain,
join(top,meet(X1,X2)) = top,
inference(orient,[status(thm)],[t375]) ).
cnf(t565667,plain,
top = join(X1,top),
inference(step,[status(thm)],[t360,t382]) ).
cnf(t387,plain,
join(X1,top) = top,
inference(orient,[status(thm)],[t565667]) ).
cnf(t388,plain,
top = join(top,X1),
inference(cp,[status(thm)],[t387,t48]) ).
cnf(t394,plain,
join(top,X1) = top,
inference(orient,[status(thm)],[t388]) ).
cnf(t565676,plain,
top = join(X2,join(X1,complement(X2))),
inference(step,[status(thm)],[t365,t394]) ).
cnf(t457,plain,
join(X1,join(X2,complement(X1))) = top,
inference(orient,[status(thm)],[t565676]) ).
cnf(t3323,plain,
join(converse(join(X1,X2)),complement(converse(X1))) = top,
inference(cp,[status(thm)],[t3319,t457]) ).
cnf(t565848,plain,
join(complement(converse(X1)),converse(join(X1,X2))) = top,
inference(step,[status(thm)],[t3323,t48]) ).
cnf(t3381,plain,
join(complement(converse(X1)),converse(join(X1,X2))) = top,
inference(orient,[status(thm)],[t565848]) ).
cnf(t3422,plain,
top = join(complement(converse(converse(X1))),converse(converse(join(X1,X2)))),
inference(cp,[status(thm)],[t3381,t66]) ).
cnf(t565849,plain,
top = join(complement(X1),converse(converse(join(X1,X2)))),
inference(step,[status(thm)],[t3422,t21]) ).
cnf(t565850,plain,
top = join(complement(X1),join(X1,X2)),
inference(step,[status(thm)],[t565849,t21]) ).
cnf(t3436,plain,
join(complement(X1),join(X1,X2)) = top,
inference(orient,[status(thm)],[t565850]) ).
cnf(t3473,plain,
top = join(complement(X1),join(X2,X1)),
inference(cp,[status(thm)],[t3436,t48]) ).
cnf(t3477,plain,
join(complement(X1),join(X2,X1)) = top,
inference(orient,[status(thm)],[t3473]) ).
cnf(t61,plain,
complement(one) = join(complement(one),composition(converse(X1),complement(X1))),
inference(cp,[status(thm)],[t59,t17]) ).
cnf(t1409,plain,
join(complement(one),composition(converse(X1),complement(X1))) = complement(one),
inference(orient,[status(thm)],[t61]) ).
cnf(t1420,plain,
complement(one) = join(complement(one),composition(X1,complement(converse(X1)))),
inference(cp,[status(thm)],[t1409,t21]) ).
cnf(t1456,plain,
join(complement(one),composition(X1,complement(converse(X1)))) = complement(one),
inference(orient,[status(thm)],[t1420]) ).
cnf(t3489,plain,
top = join(complement(composition(X1,complement(converse(X1)))),complement(one)),
inference(cp,[status(thm)],[t3477,t1456]) ).
cnf(t565861,plain,
top = join(complement(one),complement(composition(X1,complement(converse(X1))))),
inference(step,[status(thm)],[t3489,t48]) ).
cnf(t3940,plain,
join(complement(one),complement(composition(X1,complement(converse(X1))))) = top,
inference(orient,[status(thm)],[t565861]) ).
cnf(t3956,plain,
meet(one,composition(X1,complement(converse(X1)))) = complement(top),
inference(cp,[status(thm)],[t91,t3940]) ).
cnf(t565862,plain,
meet(one,composition(X1,complement(converse(X1)))) = zero,
inference(step,[status(thm)],[t3956,t103]) ).
cnf(t3962,plain,
meet(one,composition(X1,complement(converse(X1)))) = zero,
inference(orient,[status(thm)],[t565862]) ).
cnf(t3973,plain,
zero = meet(one,composition(converse(X1),complement(X1))),
inference(cp,[status(thm)],[t3962,t21]) ).
cnf(t4311,plain,
meet(one,composition(converse(X1),complement(X1))) = zero,
inference(orient,[status(thm)],[t3973]) ).
cnf(t4333,plain,
zero = meet(one,composition(converse(complement(X1)),meet(X1,X1))),
inference(cp,[status(thm)],[t4311,t242]) ).
cnf(t6321,plain,
meet(one,composition(converse(complement(X1)),meet(X1,X1))) = zero,
inference(orient,[status(thm)],[t4333]) ).
cnf(t566363,plain,
meet(one,composition(converse(complement(X1)),X1)) = zero,
inference(step,[status(thm)],[t6321,t20487]) ).
cnf(t20531,plain,
meet(one,composition(converse(complement(X1)),X1)) = zero,
inference(rw,[status(thm)],[t566363]) ).
cnf(t22827,plain,
meet(one,composition(converse(complement(X1)),X1)) = zero,
inference(orient,[status(thm)],[t20531]) ).
cnf(t22842,plain,
composition(meet(one,composition(converse(complement(X1)),X1)),meet(converse(X1),composition(converse(one),converse(complement(X1))))) = join(meet(composition(one,converse(X1)),converse(complement(X1))),composition(zero,meet(converse(X1),composition(converse(one),converse(complement(X1)))))),
inference(cp,[status(thm)],[t10630,t22827]) ).
cnf(t566462,plain,
composition(zero,meet(converse(X1),composition(converse(one),converse(complement(X1))))) = join(meet(composition(one,converse(X1)),converse(complement(X1))),composition(zero,meet(converse(X1),composition(converse(one),converse(complement(X1)))))),
inference(step,[status(thm)],[t22842,t22827]) ).
cnf(t69,plain,
converse(join(X1,converse(X2))) = join(converse(X1),X2),
inference(cp,[status(thm)],[t66,t21]) ).
cnf(t288,plain,
converse(join(X1,converse(X2))) = join(converse(X1),X2),
inference(orient,[status(thm)],[t69]) ).
cnf(t68,plain,
converse(join(converse(X1),X2)) = join(X1,converse(X2)),
inference(cp,[status(thm)],[t66,t21]) ).
cnf(t271,plain,
converse(join(converse(X1),X2)) = join(X1,converse(X2)),
inference(orient,[status(thm)],[t68]) ).
cnf(t273,plain,
join(X1,converse(complement(converse(X1)))) = converse(top),
inference(cp,[status(thm)],[t271,t56]) ).
cnf(t307,plain,
join(X1,converse(complement(converse(X1)))) = converse(top),
inference(orient,[status(thm)],[t273]) ).
cnf(t397,plain,
top = converse(top),
inference(cp,[status(thm)],[t394,t307]) ).
cnf(t401,plain,
converse(top) = top,
inference(orient,[status(thm)],[t397]) ).
cnf(t406,plain,
converse(composition(X1,top)) = composition(top,converse(X1)),
inference(cp,[status(thm)],[t27,t401]) ).
cnf(t413,plain,
converse(composition(X1,top)) = composition(top,converse(X1)),
inference(orient,[status(thm)],[t406]) ).
cnf(t422,plain,
join(converse(X1),composition(X2,top)) = converse(join(X1,composition(top,converse(X2)))),
inference(cp,[status(thm)],[t288,t413]) ).
cnf(t8103,plain,
converse(join(X1,composition(top,converse(X2)))) = join(converse(X1),composition(X2,top)),
inference(orient,[status(thm)],[t422]) ).
cnf(t30,plain,
composition(join(converse(X1),X2),converse(X3)) = join(converse(composition(X3,X1)),composition(X2,converse(X3))),
inference(cp,[status(thm)],[t24,t27]) ).
cnf(t1618,plain,
join(converse(composition(X1,X2)),composition(X3,converse(X1))) = composition(join(converse(X2),X3),converse(X1)),
inference(orient,[status(thm)],[t30]) ).
cnf(t8104,plain,
join(converse(converse(composition(X1,X2))),composition(X1,top)) = converse(composition(join(converse(X2),top),converse(X1))),
inference(cp,[status(thm)],[t8103,t1618]) ).
cnf(t566025,plain,
join(composition(X1,X2),composition(X1,top)) = converse(composition(join(converse(X2),top),converse(X1))),
inference(step,[status(thm)],[t8104,t21]) ).
cnf(t28,plain,
converse(composition(X1,converse(X2))) = composition(X2,converse(X1)),
inference(cp,[status(thm)],[t27,t21]) ).
cnf(t152,plain,
converse(composition(X1,converse(X2))) = composition(X2,converse(X1)),
inference(orient,[status(thm)],[t28]) ).
cnf(t566026,plain,
join(composition(X1,X2),composition(X1,top)) = composition(X1,converse(join(converse(X2),top))),
inference(step,[status(thm)],[t566025,t152]) ).
cnf(t566027,plain,
join(composition(X1,X2),composition(X1,top)) = composition(X1,join(X2,converse(top))),
inference(step,[status(thm)],[t566026,t271]) ).
cnf(t566028,plain,
join(composition(X1,X2),composition(X1,top)) = composition(X1,join(X2,top)),
inference(step,[status(thm)],[t566027,t401]) ).
cnf(t566029,plain,
join(composition(X1,X2),composition(X1,top)) = composition(X1,top),
inference(step,[status(thm)],[t566028,t387]) ).
cnf(t8178,plain,
join(composition(X1,X2),composition(X1,top)) = composition(X1,top),
inference(orient,[status(thm)],[t566029]) ).
cnf(t407,plain,
converse(composition(top,X1)) = composition(converse(X1),top),
inference(cp,[status(thm)],[t27,t401]) ).
cnf(t439,plain,
converse(composition(top,X1)) = composition(converse(X1),top),
inference(orient,[status(thm)],[t407]) ).
cnf(t3984,plain,
composition(meet(X1,composition(complement(converse(converse(X1))),converse(one))),meet(one,composition(converse(X1),complement(converse(converse(X1)))))) = join(meet(composition(X1,one),complement(converse(converse(X1)))),composition(meet(X1,composition(complement(converse(converse(X1))),converse(one))),zero)),
inference(cp,[status(thm)],[t33,t3962]) ).
cnf(t565863,plain,
composition(meet(X1,composition(complement(X1),converse(one))),meet(one,composition(converse(X1),complement(converse(converse(X1)))))) = join(meet(composition(X1,one),complement(converse(converse(X1)))),composition(meet(X1,composition(complement(converse(converse(X1))),converse(one))),zero)),
inference(step,[status(thm)],[t3984,t21]) ).
cnf(t565864,plain,
composition(meet(X1,composition(complement(X1),one)),meet(one,composition(converse(X1),complement(converse(converse(X1)))))) = join(meet(composition(X1,one),complement(converse(converse(X1)))),composition(meet(X1,composition(complement(converse(converse(X1))),converse(one))),zero)),
inference(step,[status(thm)],[t565863,t185]) ).
cnf(t565865,plain,
composition(meet(X1,complement(X1)),meet(one,composition(converse(X1),complement(converse(converse(X1)))))) = join(meet(composition(X1,one),complement(converse(converse(X1)))),composition(meet(X1,composition(complement(converse(converse(X1))),converse(one))),zero)),
inference(step,[status(thm)],[t565864,t17]) ).
cnf(t565866,plain,
composition(zero,meet(one,composition(converse(X1),complement(converse(converse(X1)))))) = join(meet(composition(X1,one),complement(converse(converse(X1)))),composition(meet(X1,composition(complement(converse(converse(X1))),converse(one))),zero)),
inference(step,[status(thm)],[t565865,t98]) ).
cnf(t565867,plain,
composition(zero,zero) = join(meet(composition(X1,one),complement(converse(converse(X1)))),composition(meet(X1,composition(complement(converse(converse(X1))),converse(one))),zero)),
inference(step,[status(thm)],[t565866,t3962]) ).
cnf(t565868,plain,
composition(zero,zero) = join(meet(X1,complement(converse(converse(X1)))),composition(meet(X1,composition(complement(converse(converse(X1))),converse(one))),zero)),
inference(step,[status(thm)],[t565867,t17]) ).
cnf(t565869,plain,
composition(zero,zero) = join(meet(X1,complement(X1)),composition(meet(X1,composition(complement(converse(converse(X1))),converse(one))),zero)),
inference(step,[status(thm)],[t565868,t21]) ).
cnf(t565870,plain,
composition(zero,zero) = join(zero,composition(meet(X1,composition(complement(converse(converse(X1))),converse(one))),zero)),
inference(step,[status(thm)],[t565869,t98]) ).
fof(f16,conjecture,
! [X0,X1,X2] :
( composition(X0,top) = X0
=> join(composition(X1,meet(X0,X2)),composition(meet(X1,converse(X0)),meet(X0,X2))) = composition(meet(X1,converse(X0)),meet(X0,X2)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goals) ).
fof(f16_neg,negated_conjecture,
~ ! [X0,X1,X2] :
( composition(X0,top) = X0
=> join(composition(X1,meet(X0,X2)),composition(meet(X1,converse(X0)),meet(X0,X2))) = composition(meet(X1,converse(X0)),meet(X0,X2)) ),
inference(negated_conjecture,[status(cth)],[f16]) ).
fof(f16_nnf,plain,
? [X0,X1,X2] :
( join(composition(X1,meet(X0,X2)),composition(meet(X1,converse(X0)),meet(X0,X2))) != composition(meet(X1,converse(X0)),meet(X0,X2))
& composition(X0,top) = X0 ),
inference(nnf_transformation,[status(thm)],[f16_neg]) ).
fof(f16_sk,plain,
( join(composition(sk1,meet(sk0,sk2)),composition(meet(sk1,converse(sk0)),meet(sk0,sk2))) != composition(meet(sk1,converse(sk0)),meet(sk0,sk2))
& composition(sk0,top) = sk0 ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk0,sk1,sk2])],[f16_nnf]) ).
cnf(c16,plain,
composition(sk0,top) = sk0,
inference(cnf_transformation,[status(esa)],[f16_sk]) ).
cnf(t1,plain,
composition(sk0,top) = sk0,
inference(equality_encoding,[status(esa)],[c16]) ).
cnf(t43,plain,
composition(sk0,top) = sk0,
inference(orient,[status(thm)],[t1]) ).
cnf(t44,plain,
composition(join(sk0,X1),top) = join(sk0,composition(X1,top)),
inference(cp,[status(thm)],[t24,t43]) ).
cnf(t324,plain,
composition(join(sk0,X1),top) = join(sk0,composition(X1,top)),
inference(orient,[status(thm)],[t44]) ).
cnf(t414,plain,
composition(top,converse(join(sk0,X1))) = converse(join(sk0,composition(X1,top))),
inference(cp,[status(thm)],[t413,t324]) ).
cnf(t1168,plain,
converse(join(sk0,composition(X1,top))) = composition(top,converse(join(sk0,X1))),
inference(orient,[status(thm)],[t414]) ).
cnf(t1169,plain,
composition(top,converse(join(sk0,one))) = converse(join(sk0,top)),
inference(cp,[status(thm)],[t1168,t196]) ).
cnf(t187,plain,
converse(join(X1,one)) = join(converse(X1),one),
inference(cp,[status(thm)],[t66,t185]) ).
cnf(t565655,plain,
converse(join(X1,one)) = join(one,converse(X1)),
inference(step,[status(thm)],[t187,t48]) ).
cnf(t213,plain,
converse(join(X1,one)) = join(one,converse(X1)),
inference(orient,[status(thm)],[t565655]) ).
cnf(t565721,plain,
composition(top,join(one,converse(sk0))) = converse(join(sk0,top)),
inference(step,[status(thm)],[t1169,t213]) ).
cnf(t565722,plain,
composition(top,join(one,converse(sk0))) = converse(top),
inference(step,[status(thm)],[t565721,t387]) ).
cnf(t565723,plain,
composition(top,join(one,converse(sk0))) = top,
inference(step,[status(thm)],[t565722,t401]) ).
cnf(t1188,plain,
composition(top,join(one,converse(sk0))) = top,
inference(orient,[status(thm)],[t565723]) ).
cnf(t1622,plain,
composition(join(converse(join(one,converse(sk0))),X1),converse(top)) = join(converse(top),composition(X1,converse(top))),
inference(cp,[status(thm)],[t1618,t1188]) ).
cnf(t186,plain,
converse(join(one,X1)) = join(one,converse(X1)),
inference(cp,[status(thm)],[t66,t185]) ).
cnf(t202,plain,
converse(join(one,X1)) = join(one,converse(X1)),
inference(orient,[status(thm)],[t186]) ).
cnf(t565738,plain,
composition(join(join(one,converse(converse(sk0))),X1),converse(top)) = join(converse(top),composition(X1,converse(top))),
inference(step,[status(thm)],[t1622,t202]) ).
cnf(t565739,plain,
composition(join(one,join(converse(converse(sk0)),X1)),converse(top)) = join(converse(top),composition(X1,converse(top))),
inference(step,[status(thm)],[t565738,t51]) ).
cnf(t565740,plain,
composition(join(one,join(sk0,X1)),converse(top)) = join(converse(top),composition(X1,converse(top))),
inference(step,[status(thm)],[t565739,t21]) ).
cnf(t565741,plain,
composition(join(one,join(sk0,X1)),top) = join(converse(top),composition(X1,converse(top))),
inference(step,[status(thm)],[t565740,t401]) ).
cnf(t565742,plain,
composition(join(one,join(sk0,X1)),top) = join(top,composition(X1,converse(top))),
inference(step,[status(thm)],[t565741,t401]) ).
cnf(t565743,plain,
composition(join(one,join(sk0,X1)),top) = top,
inference(step,[status(thm)],[t565742,t394]) ).
cnf(t1657,plain,
composition(join(one,join(sk0,X1)),top) = top,
inference(orient,[status(thm)],[t565743]) ).
cnf(t464,plain,
join(one,converse(join(X1,complement(one)))) = converse(top),
inference(cp,[status(thm)],[t202,t457]) ).
cnf(t565677,plain,
join(one,converse(join(X1,complement(one)))) = top,
inference(step,[status(thm)],[t464,t401]) ).
cnf(t467,plain,
join(one,converse(join(X1,complement(one)))) = top,
inference(orient,[status(thm)],[t565677]) ).
cnf(t468,plain,
top = join(one,join(X1,converse(complement(one)))),
inference(cp,[status(thm)],[t467,t271]) ).
cnf(t472,plain,
join(one,join(X1,converse(complement(one)))) = top,
inference(orient,[status(thm)],[t468]) ).
cnf(t1658,plain,
top = composition(top,top),
inference(cp,[status(thm)],[t1657,t472]) ).
cnf(t1699,plain,
composition(top,top) = top,
inference(orient,[status(thm)],[t1658]) ).
cnf(t1706,plain,
complement(top) = join(complement(top),composition(converse(top),complement(top))),
inference(cp,[status(thm)],[t59,t1699]) ).
cnf(t565746,plain,
zero = join(complement(top),composition(converse(top),complement(top))),
inference(step,[status(thm)],[t1706,t103]) ).
cnf(t565747,plain,
zero = join(zero,composition(converse(top),complement(top))),
inference(step,[status(thm)],[t565746,t103]) ).
cnf(t565748,plain,
zero = join(zero,composition(top,complement(top))),
inference(step,[status(thm)],[t565747,t401]) ).
cnf(t565749,plain,
zero = join(zero,composition(top,zero)),
inference(step,[status(thm)],[t565748,t103]) ).
cnf(t1708,plain,
join(zero,composition(top,zero)) = zero,
inference(orient,[status(thm)],[t565749]) ).
cnf(t1711,plain,
join(zero,join(composition(top,zero),X1)) = join(zero,X1),
inference(cp,[status(thm)],[t51,t1708]) ).
cnf(t1751,plain,
join(zero,join(composition(top,zero),X1)) = join(zero,X1),
inference(orient,[status(thm)],[t1711]) ).
cnf(t1753,plain,
join(zero,composition(X1,zero)) = join(zero,composition(join(top,X1),zero)),
inference(cp,[status(thm)],[t1751,t24]) ).
cnf(t565752,plain,
join(zero,composition(X1,zero)) = join(zero,composition(top,zero)),
inference(step,[status(thm)],[t1753,t394]) ).
cnf(t565753,plain,
join(zero,composition(X1,zero)) = zero,
inference(step,[status(thm)],[t565752,t1708]) ).
cnf(t1774,plain,
join(zero,composition(X1,zero)) = zero,
inference(orient,[status(thm)],[t565753]) ).
cnf(t565871,plain,
composition(zero,zero) = zero,
inference(step,[status(thm)],[t565870,t1774]) ).
cnf(t3985,plain,
composition(zero,zero) = zero,
inference(orient,[status(thm)],[t565871]) ).
cnf(t3987,plain,
composition(join(zero,X1),zero) = join(zero,composition(X1,zero)),
inference(cp,[status(thm)],[t24,t3985]) ).
cnf(t565876,plain,
composition(join(zero,X1),zero) = zero,
inference(step,[status(thm)],[t3987,t1774]) ).
cnf(t4058,plain,
composition(join(zero,X1),zero) = zero,
inference(orient,[status(thm)],[t565876]) ).
cnf(t1778,plain,
join(zero,join(composition(X1,zero),X2)) = join(zero,X2),
inference(cp,[status(thm)],[t51,t1774]) ).
cnf(t1832,plain,
join(zero,join(composition(X1,zero),X2)) = join(zero,X2),
inference(orient,[status(thm)],[t1778]) ).
cnf(t565674,plain,
join(X1,converse(complement(converse(X1)))) = top,
inference(step,[status(thm)],[t307,t401]) ).
cnf(t404,plain,
join(X1,converse(complement(converse(X1)))) = top,
inference(orient,[status(thm)],[t565674]) ).
cnf(t1842,plain,
join(zero,converse(complement(converse(composition(X1,zero))))) = join(zero,top),
inference(cp,[status(thm)],[t1832,t404]) ).
cnf(t105,plain,
top = join(top,zero),
inference(cp,[status(thm)],[t56,t103]) ).
cnf(t565650,plain,
top = join(zero,top),
inference(step,[status(thm)],[t105,t48]) ).
cnf(t110,plain,
join(zero,top) = top,
inference(orient,[status(thm)],[t565650]) ).
cnf(t565765,plain,
join(zero,converse(complement(converse(composition(X1,zero))))) = top,
inference(step,[status(thm)],[t1842,t110]) ).
cnf(t1918,plain,
join(zero,converse(complement(converse(composition(X1,zero))))) = top,
inference(orient,[status(thm)],[t565765]) ).
cnf(t4059,plain,
zero = composition(top,zero),
inference(cp,[status(thm)],[t4058,t1918]) ).
cnf(t4092,plain,
composition(top,zero) = zero,
inference(orient,[status(thm)],[t4059]) ).
cnf(t4096,plain,
composition(converse(zero),top) = converse(zero),
inference(cp,[status(thm)],[t439,t4092]) ).
cnf(t4119,plain,
composition(converse(zero),top) = converse(zero),
inference(orient,[status(thm)],[t4096]) ).
cnf(t8220,plain,
composition(converse(zero),top) = join(composition(converse(zero),X1),converse(zero)),
inference(cp,[status(thm)],[t8178,t4119]) ).
cnf(t566065,plain,
converse(zero) = join(composition(converse(zero),X1),converse(zero)),
inference(step,[status(thm)],[t8220,t4119]) ).
cnf(t566066,plain,
converse(zero) = join(converse(zero),composition(converse(zero),X1)),
inference(step,[status(thm)],[t566065,t48]) ).
cnf(t9596,plain,
join(converse(zero),composition(converse(zero),X1)) = converse(zero),
inference(orient,[status(thm)],[t566066]) ).
cnf(t20315,plain,
converse(complement(converse(zero))) = top,
inference(cp,[status(thm)],[t20280,t404]) ).
cnf(t20700,plain,
converse(complement(converse(zero))) = top,
inference(orient,[status(thm)],[t20315]) ).
cnf(t20701,plain,
complement(converse(zero)) = converse(top),
inference(cp,[status(thm)],[t21,t20700]) ).
cnf(t566394,plain,
complement(converse(zero)) = top,
inference(step,[status(thm)],[t20701,t401]) ).
cnf(t20770,plain,
complement(converse(zero)) = top,
inference(orient,[status(thm)],[t566394]) ).
cnf(t20771,plain,
converse(zero) = complement(top),
inference(cp,[status(thm)],[t20605,t20770]) ).
cnf(t566395,plain,
converse(zero) = zero,
inference(step,[status(thm)],[t20771,t103]) ).
cnf(t20786,plain,
converse(zero) = zero,
inference(orient,[status(thm)],[t566395]) ).
cnf(t566404,plain,
join(zero,composition(converse(zero),X1)) = converse(zero),
inference(step,[status(thm)],[t9596,t20786]) ).
cnf(t566405,plain,
composition(converse(zero),X1) = converse(zero),
inference(step,[status(thm)],[t566404,t20280]) ).
cnf(t566406,plain,
composition(zero,X1) = converse(zero),
inference(step,[status(thm)],[t566405,t20786]) ).
cnf(t566407,plain,
composition(zero,X1) = zero,
inference(step,[status(thm)],[t566406,t20786]) ).
cnf(t20828,plain,
composition(zero,X1) = zero,
inference(rw,[status(thm)],[t566407]) ).
cnf(t20843,plain,
composition(zero,X1) = zero,
inference(orient,[status(thm)],[t20828]) ).
cnf(t566463,plain,
zero = join(meet(composition(one,converse(X1)),converse(complement(X1))),composition(zero,meet(converse(X1),composition(converse(one),converse(complement(X1)))))),
inference(step,[status(thm)],[t566462,t20843]) ).
cnf(t566464,plain,
zero = join(meet(converse(complement(X1)),composition(one,converse(X1))),composition(zero,meet(converse(X1),composition(converse(one),converse(complement(X1)))))),
inference(step,[status(thm)],[t566463,t112]) ).
cnf(t566465,plain,
zero = join(meet(converse(complement(X1)),converse(X1)),composition(zero,meet(converse(X1),composition(converse(one),converse(complement(X1)))))),
inference(step,[status(thm)],[t566464,t196]) ).
cnf(t566466,plain,
zero = join(meet(converse(X1),converse(complement(X1))),composition(zero,meet(converse(X1),composition(converse(one),converse(complement(X1)))))),
inference(step,[status(thm)],[t566465,t112]) ).
cnf(t566467,plain,
zero = join(meet(converse(X1),converse(complement(X1))),zero),
inference(step,[status(thm)],[t566466,t20843]) ).
cnf(t8182,plain,
composition(X1,top) = join(X1,composition(X1,top)),
inference(cp,[status(thm)],[t8178,t17]) ).
cnf(t8278,plain,
join(X1,composition(X1,top)) = composition(X1,top),
inference(orient,[status(thm)],[t8182]) ).
cnf(t8310,plain,
join(X1,converse(composition(converse(X1),top))) = converse(composition(converse(X1),top)),
inference(cp,[status(thm)],[t271,t8278]) ).
cnf(t566033,plain,
join(X1,composition(converse(top),X1)) = converse(composition(converse(X1),top)),
inference(step,[status(thm)],[t8310,t162]) ).
cnf(t566034,plain,
join(X1,composition(top,X1)) = converse(composition(converse(X1),top)),
inference(step,[status(thm)],[t566033,t401]) ).
cnf(t566035,plain,
join(X1,composition(top,X1)) = composition(converse(top),X1),
inference(step,[status(thm)],[t566034,t162]) ).
cnf(t566036,plain,
join(X1,composition(top,X1)) = composition(top,X1),
inference(step,[status(thm)],[t566035,t401]) ).
cnf(t8367,plain,
join(X1,composition(top,X1)) = composition(top,X1),
inference(orient,[status(thm)],[t566036]) ).
cnf(t8373,plain,
join(X1,join(composition(top,X1),X2)) = join(composition(top,X1),X2),
inference(cp,[status(thm)],[t51,t8367]) ).
cnf(t13146,plain,
join(X1,join(composition(top,X1),X2)) = join(composition(top,X1),X2),
inference(orient,[status(thm)],[t8373]) ).
cnf(t13190,plain,
join(composition(top,X1),X2) = join(X1,join(X2,composition(top,X1))),
inference(cp,[status(thm)],[t13146,t48]) ).
cnf(t15171,plain,
join(X1,join(X2,composition(top,X1))) = join(composition(top,X1),X2),
inference(orient,[status(thm)],[t13190]) ).
cnf(t20304,plain,
join(X1,composition(top,zero)) = join(composition(top,zero),X1),
inference(cp,[status(thm)],[t20280,t15171]) ).
cnf(t566348,plain,
join(X1,zero) = join(composition(top,zero),X1),
inference(step,[status(thm)],[t20304,t4092]) ).
cnf(t566349,plain,
join(X1,zero) = join(zero,X1),
inference(step,[status(thm)],[t566348,t4092]) ).
cnf(t566350,plain,
join(X1,zero) = X1,
inference(step,[status(thm)],[t566349,t20280]) ).
cnf(t20454,plain,
join(X1,zero) = X1,
inference(orient,[status(thm)],[t566350]) ).
cnf(t566468,plain,
zero = meet(converse(X1),converse(complement(X1))),
inference(step,[status(thm)],[t566467,t20454]) ).
cnf(t22878,plain,
meet(converse(X1),converse(complement(X1))) = zero,
inference(orient,[status(thm)],[t566468]) ).
cnf(t33645,plain,
join(complement(converse(X1)),converse(complement(X1))) = join(complement(converse(X1)),zero),
inference(cp,[status(thm)],[t33597,t22878]) ).
cnf(t566741,plain,
join(converse(complement(X1)),complement(converse(X1))) = join(complement(converse(X1)),zero),
inference(step,[status(thm)],[t33645,t48]) ).
cnf(t566742,plain,
join(converse(complement(X1)),complement(converse(X1))) = complement(converse(X1)),
inference(step,[status(thm)],[t566741,t20454]) ).
cnf(t34902,plain,
join(converse(complement(X1)),complement(converse(X1))) = complement(converse(X1)),
inference(orient,[status(thm)],[t566742]) ).
cnf(t34907,plain,
complement(converse(complement(X1))) = join(converse(X1),complement(converse(complement(X1)))),
inference(cp,[status(thm)],[t34902,t20605]) ).
cnf(t21441,plain,
meet(X1,complement(converse(complement(converse(complement(X1)))))) = complement(top),
inference(cp,[status(thm)],[t21385,t404]) ).
cnf(t566683,plain,
meet(X1,complement(converse(complement(converse(complement(X1)))))) = zero,
inference(step,[status(thm)],[t21441,t103]) ).
cnf(t31540,plain,
meet(X1,complement(converse(complement(converse(complement(X1)))))) = zero,
inference(orient,[status(thm)],[t566683]) ).
cnf(t32365,plain,
join(X1,complement(converse(complement(converse(complement(complement(X1))))))) = join(X1,zero),
inference(cp,[status(thm)],[t32360,t31540]) ).
cnf(t566705,plain,
join(X1,complement(converse(complement(converse(X1))))) = join(X1,zero),
inference(step,[status(thm)],[t32365,t20605]) ).
cnf(t566706,plain,
join(X1,complement(converse(complement(converse(X1))))) = X1,
inference(step,[status(thm)],[t566705,t20454]) ).
cnf(t32777,plain,
join(X1,complement(converse(complement(converse(X1))))) = X1,
inference(orient,[status(thm)],[t566706]) ).
cnf(t32801,plain,
converse(X1) = join(converse(X1),complement(converse(complement(X1)))),
inference(cp,[status(thm)],[t32777,t21]) ).
cnf(t34267,plain,
join(converse(X1),complement(converse(complement(X1)))) = converse(X1),
inference(orient,[status(thm)],[t32801]) ).
cnf(t566743,plain,
complement(converse(complement(X1))) = converse(X1),
inference(step,[status(thm)],[t34907,t34267]) ).
cnf(t34963,plain,
complement(converse(complement(X1))) = converse(X1),
inference(orient,[status(thm)],[t566743]) ).
cnf(t34968,plain,
converse(complement(X1)) = complement(converse(X1)),
inference(cp,[status(thm)],[t34963,t20605]) ).
cnf(t35037,plain,
complement(converse(X1)) = converse(complement(X1)),
inference(orient,[status(thm)],[t34968]) ).
cnf(t21445,plain,
meet(complement(X1),complement(X2)) = complement(join(X1,X2)),
inference(cp,[status(thm)],[t21385,t20605]) ).
cnf(t21762,plain,
meet(complement(X1),complement(X2)) = complement(join(X1,X2)),
inference(orient,[status(thm)],[t21445]) ).
cnf(t21769,plain,
complement(X1) = join(complement(X1),complement(join(X2,X1))),
inference(cp,[status(thm)],[t21006,t21762]) ).
cnf(t106,plain,
meet(top,X1) = complement(join(zero,complement(X1))),
inference(cp,[status(thm)],[t91,t103]) ).
cnf(t129,plain,
complement(join(zero,complement(X1))) = meet(top,X1),
inference(orient,[status(thm)],[t106]) ).
cnf(t131,plain,
meet(top,join(complement(X1),complement(X2))) = complement(join(zero,meet(X1,X2))),
inference(cp,[status(thm)],[t129,t91]) ).
cnf(t7199,plain,
meet(top,join(complement(X1),complement(X2))) = complement(join(zero,meet(X1,X2))),
inference(orient,[status(thm)],[t131]) ).
cnf(t566300,plain,
meet(top,join(complement(X1),complement(X2))) = complement(meet(X1,X2)),
inference(step,[status(thm)],[t7199,t20280]) ).
cnf(t20283,plain,
meet(top,join(complement(X1),complement(X2))) = complement(meet(X1,X2)),
inference(orient,[status(thm)],[t566300]) ).
cnf(t566330,plain,
complement(complement(X1)) = meet(top,X1),
inference(step,[status(thm)],[t129,t20280]) ).
cnf(t20411,plain,
complement(complement(X1)) = meet(top,X1),
inference(rw,[status(thm)],[t566330]) ).
cnf(t566382,plain,
X1 = meet(top,X1),
inference(step,[status(thm)],[t20411,t20605]) ).
cnf(t20661,plain,
meet(top,X1) = X1,
inference(orient,[status(thm)],[t566382]) ).
cnf(t566385,plain,
join(complement(X1),complement(X2)) = complement(meet(X1,X2)),
inference(step,[status(thm)],[t20283,t20661]) ).
cnf(t20683,plain,
join(complement(X1),complement(X2)) = complement(meet(X1,X2)),
inference(rw,[status(thm)],[t566385]) ).
cnf(t21694,plain,
join(complement(X1),complement(X2)) = complement(meet(X1,X2)),
inference(orient,[status(thm)],[t20683]) ).
cnf(t566452,plain,
complement(X1) = complement(meet(X1,join(X2,X1))),
inference(step,[status(thm)],[t21769,t21694]) ).
cnf(t21910,plain,
complement(meet(X1,join(X2,X1))) = complement(X1),
inference(orient,[status(thm)],[t566452]) ).
cnf(t21957,plain,
meet(X1,join(X2,X1)) = complement(complement(X1)),
inference(cp,[status(thm)],[t20605,t21910]) ).
cnf(t566453,plain,
meet(X1,join(X2,X1)) = X1,
inference(step,[status(thm)],[t21957,t20605]) ).
cnf(t22013,plain,
meet(X1,join(X2,X1)) = X1,
inference(orient,[status(thm)],[t566453]) ).
cnf(t21448,plain,
join(complement(X1),X2) = complement(meet(X1,complement(X2))),
inference(cp,[status(thm)],[t20605,t21385]) ).
cnf(t21779,plain,
complement(meet(X1,complement(X2))) = join(complement(X1),X2),
inference(orient,[status(thm)],[t21448]) ).
cnf(t1415,plain,
complement(one) = join(complement(one),composition(top,complement(top))),
inference(cp,[status(thm)],[t1409,t401]) ).
cnf(t565725,plain,
complement(one) = join(complement(one),composition(top,zero)),
inference(step,[status(thm)],[t1415,t103]) ).
cnf(t1435,plain,
join(complement(one),composition(top,zero)) = complement(one),
inference(orient,[status(thm)],[t565725]) ).
cnf(t565878,plain,
join(complement(one),zero) = complement(one),
inference(step,[status(thm)],[t1435,t4092]) ).
cnf(t4107,plain,
join(complement(one),zero) = complement(one),
inference(rw,[status(thm)],[t565878]) ).
cnf(t565881,plain,
join(zero,complement(one)) = complement(one),
inference(step,[status(thm)],[t4107,t48]) ).
cnf(t4137,plain,
join(zero,complement(one)) = complement(one),
inference(orient,[status(thm)],[t565881]) ).
cnf(t4152,plain,
meet(top,one) = complement(complement(one)),
inference(cp,[status(thm)],[t129,t4137]) ).
cnf(t565882,plain,
meet(top,one) = meet(one,one),
inference(step,[status(thm)],[t4152,t242]) ).
cnf(t4155,plain,
meet(one,one) = meet(top,one),
inference(orient,[status(thm)],[t565882]) ).
cnf(t6332,plain,
zero = meet(one,composition(converse(complement(one)),meet(top,one))),
inference(cp,[status(thm)],[t6321,t4155]) ).
cnf(t7111,plain,
meet(one,composition(converse(complement(one)),meet(top,one))) = zero,
inference(orient,[status(thm)],[t6332]) ).
cnf(t566353,plain,
one = meet(top,one),
inference(step,[status(thm)],[t4155,t20487]) ).
cnf(t20521,plain,
one = meet(top,one),
inference(rw,[status(thm)],[t566353]) ).
cnf(t20647,plain,
meet(top,one) = one,
inference(orient,[status(thm)],[t20521]) ).
cnf(t566380,plain,
meet(one,composition(converse(complement(one)),one)) = zero,
inference(step,[status(thm)],[t7111,t20647]) ).
cnf(t566381,plain,
meet(one,converse(complement(one))) = zero,
inference(step,[status(thm)],[t566380,t17]) ).
cnf(t20660,plain,
meet(one,converse(complement(one))) = zero,
inference(rw,[status(thm)],[t566381]) ).
cnf(t20867,plain,
meet(one,converse(complement(one))) = zero,
inference(orient,[status(thm)],[t20660]) ).
cnf(t31589,plain,
one = join(zero,meet(one,complement(converse(complement(one))))),
inference(cp,[status(thm)],[t31556,t20867]) ).
cnf(t566684,plain,
one = meet(one,complement(converse(complement(one)))),
inference(step,[status(thm)],[t31589,t20280]) ).
cnf(t31643,plain,
meet(one,complement(converse(complement(one)))) = one,
inference(orient,[status(thm)],[t566684]) ).
cnf(t31673,plain,
join(complement(one),converse(complement(one))) = complement(one),
inference(cp,[status(thm)],[t21779,t31643]) ).
cnf(t31680,plain,
join(complement(one),converse(complement(one))) = complement(one),
inference(orient,[status(thm)],[t31673]) ).
cnf(t31688,plain,
converse(complement(one)) = meet(converse(complement(one)),complement(one)),
inference(cp,[status(thm)],[t22013,t31680]) ).
cnf(t566690,plain,
converse(complement(one)) = meet(complement(one),converse(complement(one))),
inference(step,[status(thm)],[t31688,t112]) ).
cnf(t22045,plain,
converse(X1) = meet(converse(X1),converse(join(X2,X1))),
inference(cp,[status(thm)],[t22013,t66]) ).
cnf(t24448,plain,
meet(converse(X1),converse(join(X2,X1))) = converse(X1),
inference(orient,[status(thm)],[t22045]) ).
cnf(t31691,plain,
converse(converse(complement(one))) = meet(converse(converse(complement(one))),converse(complement(one))),
inference(cp,[status(thm)],[t24448,t31680]) ).
cnf(t566685,plain,
complement(one) = meet(converse(converse(complement(one))),converse(complement(one))),
inference(step,[status(thm)],[t31691,t21]) ).
cnf(t566686,plain,
complement(one) = meet(converse(complement(one)),converse(converse(complement(one)))),
inference(step,[status(thm)],[t566685,t112]) ).
cnf(t566687,plain,
complement(one) = meet(converse(complement(one)),complement(one)),
inference(step,[status(thm)],[t566686,t21]) ).
cnf(t566688,plain,
complement(one) = meet(complement(one),converse(complement(one))),
inference(step,[status(thm)],[t566687,t112]) ).
cnf(t31709,plain,
meet(complement(one),converse(complement(one))) = complement(one),
inference(orient,[status(thm)],[t566688]) ).
cnf(t566691,plain,
converse(complement(one)) = complement(one),
inference(step,[status(thm)],[t566690,t31709]) ).
cnf(t31851,plain,
converse(complement(one)) = complement(one),
inference(orient,[status(thm)],[t566691]) ).
cnf(t31853,plain,
converse(join(X1,complement(one))) = join(converse(X1),complement(one)),
inference(cp,[status(thm)],[t66,t31851]) ).
cnf(t32073,plain,
converse(join(X1,complement(one))) = join(converse(X1),complement(one)),
inference(orient,[status(thm)],[t31853]) ).
cnf(t35040,plain,
converse(complement(join(X1,complement(one)))) = complement(join(converse(X1),complement(one))),
inference(cp,[status(thm)],[t35037,t32073]) ).
cnf(t251,plain,
meet(complement(X1),X2) = complement(join(meet(X1,X1),complement(X2))),
inference(cp,[status(thm)],[t91,t242]) ).
cnf(t1283,plain,
complement(join(meet(X1,X1),complement(X2))) = meet(complement(X1),X2),
inference(orient,[status(thm)],[t251]) ).
cnf(t566360,plain,
complement(join(X1,complement(X2))) = meet(complement(X1),X2),
inference(step,[status(thm)],[t1283,t20487]) ).
cnf(t20528,plain,
complement(join(X1,complement(X2))) = meet(complement(X1),X2),
inference(rw,[status(thm)],[t566360]) ).
cnf(t21620,plain,
complement(join(X1,complement(X2))) = meet(complement(X1),X2),
inference(orient,[status(thm)],[t20528]) ).
cnf(t566756,plain,
converse(meet(complement(X1),one)) = complement(join(converse(X1),complement(one))),
inference(step,[status(thm)],[t35040,t21620]) ).
cnf(t566757,plain,
converse(meet(one,complement(X1))) = complement(join(converse(X1),complement(one))),
inference(step,[status(thm)],[t566756,t112]) ).
cnf(t566758,plain,
converse(meet(one,complement(X1))) = meet(complement(converse(X1)),one),
inference(step,[status(thm)],[t566757,t21620]) ).
cnf(t566759,plain,
converse(meet(one,complement(X1))) = meet(one,complement(converse(X1))),
inference(step,[status(thm)],[t566758,t112]) ).
cnf(t566760,plain,
converse(meet(one,complement(X1))) = meet(one,converse(complement(X1))),
inference(step,[status(thm)],[t566759,t35037]) ).
cnf(t35125,plain,
converse(meet(one,complement(X1))) = meet(one,converse(complement(X1))),
inference(orient,[status(thm)],[t566760]) ).
cnf(t35140,plain,
meet(one,converse(complement(complement(X1)))) = converse(meet(one,X1)),
inference(cp,[status(thm)],[t35125,t20605]) ).
cnf(t566761,plain,
meet(one,converse(X1)) = converse(meet(one,X1)),
inference(step,[status(thm)],[t35140,t20605]) ).
cnf(t35214,plain,
converse(meet(one,X1)) = meet(one,converse(X1)),
inference(orient,[status(thm)],[t566761]) ).
cnf(t35231,plain,
converse(composition(meet(one,X1),X2)) = composition(converse(X2),meet(one,converse(X1))),
inference(cp,[status(thm)],[t27,t35214]) ).
cnf(t31594,plain,
X1 = join(meet(X2,X1),meet(X1,complement(X2))),
inference(cp,[status(thm)],[t31556,t112]) ).
cnf(t43378,plain,
join(meet(X1,X2),meet(X2,complement(X1))) = X2,
inference(orient,[status(thm)],[t31594]) ).
cnf(t43492,plain,
X1 = join(meet(X2,X1),meet(complement(X2),X1)),
inference(cp,[status(thm)],[t43378,t112]) ).
cnf(t46507,plain,
join(meet(X1,X2),meet(complement(X1),X2)) = X2,
inference(orient,[status(thm)],[t43492]) ).
cnf(t115,plain,
composition(meet(X1,composition(X2,converse(X3))),meet(X3,composition(converse(X1),X2))) = join(meet(composition(X1,X3),X2),composition(meet(X1,composition(X2,converse(X3))),meet(composition(converse(X1),X2),X3))),
inference(cp,[status(thm)],[t33,t112]) ).
cnf(t53826,plain,
join(meet(composition(X1,X2),X3),composition(meet(X1,composition(X3,converse(X2))),meet(composition(converse(X1),X3),X2))) = composition(meet(X1,composition(X3,converse(X2))),meet(X2,composition(converse(X1),X3))),
inference(orient,[status(thm)],[t115]) ).
cnf(t21394,plain,
meet(X1,complement(join(X2,X1))) = complement(top),
inference(cp,[status(thm)],[t21385,t3477]) ).
cnf(t566448,plain,
meet(X1,complement(join(X2,X1))) = zero,
inference(step,[status(thm)],[t21394,t103]) ).
cnf(t21522,plain,
meet(X1,complement(join(X2,X1))) = zero,
inference(orient,[status(thm)],[t566448]) ).
cnf(t20973,plain,
join(X1,join(meet(X1,X2),X3)) = join(X1,X3),
inference(cp,[status(thm)],[t51,t20965]) ).
cnf(t26029,plain,
join(X1,join(meet(X1,X2),X3)) = join(X1,X3),
inference(orient,[status(thm)],[t20973]) ).
cnf(t26046,plain,
join(X1,meet(X2,meet(X1,X3))) = join(X1,meet(X1,X3)),
inference(cp,[status(thm)],[t26029,t21006]) ).
cnf(t566593,plain,
join(X1,meet(X2,meet(X1,X3))) = X1,
inference(step,[status(thm)],[t26046,t20965]) ).
cnf(t26158,plain,
join(X1,meet(X2,meet(X1,X3))) = X1,
inference(orient,[status(thm)],[t566593]) ).
cnf(t22016,plain,
meet(X1,X2) = meet(meet(X1,X2),X2),
inference(cp,[status(thm)],[t22013,t21006]) ).
cnf(t566455,plain,
meet(X1,X2) = meet(X2,meet(X1,X2)),
inference(step,[status(thm)],[t22016,t112]) ).
cnf(t22696,plain,
meet(X1,meet(X2,X1)) = meet(X2,X1),
inference(orient,[status(thm)],[t566455]) ).
cnf(t26160,plain,
X1 = join(X1,meet(X2,meet(X3,X1))),
inference(cp,[status(thm)],[t26158,t22696]) ).
cnf(t26536,plain,
join(X1,meet(X2,meet(X3,X1))) = X1,
inference(orient,[status(thm)],[t26160]) ).
cnf(t26563,plain,
zero = meet(meet(X1,meet(X2,X3)),complement(X3)),
inference(cp,[status(thm)],[t21522,t26536]) ).
cnf(t566889,plain,
zero = meet(complement(X3),meet(X1,meet(X2,X3))),
inference(step,[status(thm)],[t26563,t112]) ).
cnf(t40467,plain,
meet(complement(X1),meet(X2,meet(X3,X1))) = zero,
inference(orient,[status(thm)],[t566889]) ).
cnf(t21409,plain,
meet(one,complement(composition(converse(X1),complement(X1)))) = complement(complement(one)),
inference(cp,[status(thm)],[t21385,t1409]) ).
cnf(t566682,plain,
meet(one,complement(composition(converse(X1),complement(X1)))) = one,
inference(step,[status(thm)],[t21409,t20605]) ).
cnf(t31479,plain,
meet(one,complement(composition(converse(X1),complement(X1)))) = one,
inference(orient,[status(thm)],[t566682]) ).
cnf(t40524,plain,
zero = meet(complement(complement(composition(converse(X1),complement(X1)))),meet(X2,one)),
inference(cp,[status(thm)],[t40467,t31479]) ).
cnf(t567882,plain,
zero = meet(composition(converse(X1),complement(X1)),meet(X2,one)),
inference(step,[status(thm)],[t40524,t20605]) ).
cnf(t109931,plain,
meet(composition(converse(X1),complement(X1)),meet(X2,one)) = zero,
inference(orient,[status(thm)],[t567882]) ).
cnf(t110012,plain,
composition(meet(X1,composition(complement(X1),converse(meet(X2,one)))),meet(meet(X2,one),composition(converse(X1),complement(X1)))) = join(meet(composition(X1,meet(X2,one)),complement(X1)),composition(meet(X1,composition(complement(X1),converse(meet(X2,one)))),zero)),
inference(cp,[status(thm)],[t53826,t109931]) ).
cnf(t35226,plain,
meet(one,converse(X1)) = converse(meet(X1,one)),
inference(cp,[status(thm)],[t35214,t112]) ).
cnf(t35299,plain,
converse(meet(X1,one)) = meet(one,converse(X1)),
inference(orient,[status(thm)],[t35226]) ).
cnf(t567883,plain,
composition(meet(X1,composition(complement(X1),meet(one,converse(X2)))),meet(meet(X2,one),composition(converse(X1),complement(X1)))) = join(meet(composition(X1,meet(X2,one)),complement(X1)),composition(meet(X1,composition(complement(X1),converse(meet(X2,one)))),zero)),
inference(step,[status(thm)],[t110012,t35299]) ).
cnf(t31798,plain,
join(X1,complement(X2)) = join(X1,complement(join(X2,X1))),
inference(cp,[status(thm)],[t31781,t21762]) ).
cnf(t33042,plain,
join(X1,complement(join(X2,X1))) = join(X1,complement(X2)),
inference(orient,[status(thm)],[t31798]) ).
cnf(t33192,plain,
meet(X1,complement(complement(join(X2,complement(X1))))) = complement(join(complement(X1),complement(X2))),
inference(cp,[status(thm)],[t21385,t33042]) ).
cnf(t566713,plain,
meet(X1,join(X2,complement(X1))) = complement(join(complement(X1),complement(X2))),
inference(step,[status(thm)],[t33192,t20605]) ).
cnf(t566714,plain,
meet(X1,join(X2,complement(X1))) = meet(X1,X2),
inference(step,[status(thm)],[t566713,t91]) ).
cnf(t33216,plain,
meet(X1,join(X2,complement(X1))) = meet(X1,X2),
inference(orient,[status(thm)],[t566714]) ).
cnf(t33235,plain,
meet(X1,X2) = meet(X1,join(complement(X1),X2)),
inference(cp,[status(thm)],[t33216,t48]) ).
cnf(t33278,plain,
meet(X1,join(complement(X1),X2)) = meet(X1,X2),
inference(orient,[status(thm)],[t33235]) ).
cnf(t31817,plain,
join(X1,meet(X2,complement(meet(X3,X1)))) = join(X1,join(meet(X3,X1),X2)),
inference(cp,[status(thm)],[t26619,t31781]) ).
cnf(t567293,plain,
join(X1,meet(X2,complement(meet(X3,X1)))) = join(X1,X2),
inference(step,[status(thm)],[t31817,t26619]) ).
cnf(t64538,plain,
join(X1,meet(X2,complement(meet(X3,X1)))) = join(X1,X2),
inference(orient,[status(thm)],[t567293]) ).
cnf(t21633,plain,
join(X1,complement(X2)) = complement(meet(complement(X1),X2)),
inference(cp,[status(thm)],[t20605,t21620]) ).
cnf(t21844,plain,
complement(meet(complement(X1),X2)) = join(X1,complement(X2)),
inference(orient,[status(thm)],[t21633]) ).
cnf(t64551,plain,
join(X1,X2) = join(X1,meet(X2,join(X3,complement(X1)))),
inference(cp,[status(thm)],[t64538,t21844]) ).
cnf(t71383,plain,
join(X1,meet(X2,join(X3,complement(X1)))) = join(X1,X2),
inference(orient,[status(thm)],[t64551]) ).
cnf(t71446,plain,
meet(X1,meet(X2,join(X3,complement(complement(X1))))) = meet(X1,join(complement(X1),X2)),
inference(cp,[status(thm)],[t33278,t71383]) ).
cnf(t567431,plain,
meet(X1,meet(X2,join(X3,X1))) = meet(X1,join(complement(X1),X2)),
inference(step,[status(thm)],[t71446,t20605]) ).
cnf(t567432,plain,
meet(X1,meet(X2,join(X3,X1))) = meet(X1,X2),
inference(step,[status(thm)],[t567431,t33278]) ).
cnf(t71489,plain,
meet(X1,meet(X2,join(X3,X1))) = meet(X1,X2),
inference(orient,[status(thm)],[t567432]) ).
cnf(t71542,plain,
meet(meet(X1,X2),X3) = meet(meet(X1,X2),meet(X3,X1)),
inference(cp,[status(thm)],[t71489,t20965]) ).
cnf(t73736,plain,
meet(meet(X1,X2),meet(X3,X1)) = meet(meet(X1,X2),X3),
inference(orient,[status(thm)],[t71542]) ).
cnf(t73749,plain,
meet(meet(X1,X2),X3) = meet(meet(X3,X1),meet(X1,X2)),
inference(cp,[status(thm)],[t73736,t112]) ).
cnf(t71516,plain,
meet(X1,X2) = meet(X1,meet(join(X3,X1),X2)),
inference(cp,[status(thm)],[t71489,t112]) ).
cnf(t71849,plain,
meet(X1,meet(join(X2,X1),X3)) = meet(X1,X3),
inference(orient,[status(thm)],[t71516]) ).
cnf(t71942,plain,
meet(meet(X1,X2),X3) = meet(meet(X1,X2),meet(X2,X3)),
inference(cp,[status(thm)],[t71849,t21006]) ).
cnf(t76854,plain,
meet(meet(X1,X2),meet(X2,X3)) = meet(meet(X1,X2),X3),
inference(orient,[status(thm)],[t71942]) ).
cnf(t567455,plain,
meet(meet(X1,X2),X3) = meet(meet(X3,X1),X2),
inference(step,[status(thm)],[t73749,t76854]) ).
cnf(t77374,plain,
meet(meet(X1,X2),X3) = meet(meet(X3,X1),X2),
inference(orient,[status(thm)],[t567455]) ).
cnf(t77391,plain,
meet(meet(X1,X2),X3) = meet(X1,meet(X2,X3)),
inference(cp,[status(thm)],[t77374,t112]) ).
cnf(t78317,plain,
meet(meet(X1,X2),X3) = meet(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t77391]) ).
cnf(t567884,plain,
composition(meet(X1,composition(complement(X1),meet(one,converse(X2)))),meet(X2,meet(one,composition(converse(X1),complement(X1))))) = join(meet(composition(X1,meet(X2,one)),complement(X1)),composition(meet(X1,composition(complement(X1),converse(meet(X2,one)))),zero)),
inference(step,[status(thm)],[t567883,t78317]) ).
cnf(t567885,plain,
composition(meet(X1,composition(complement(X1),meet(one,converse(X2)))),meet(X2,zero)) = join(meet(composition(X1,meet(X2,one)),complement(X1)),composition(meet(X1,composition(complement(X1),converse(meet(X2,one)))),zero)),
inference(step,[status(thm)],[t567884,t4311]) ).
cnf(t565670,plain,
join(X1,join(complement(X1),X2)) = top,
inference(step,[status(thm)],[t356,t394]) ).
cnf(t395,plain,
join(X1,join(complement(X1),X2)) = top,
inference(orient,[status(thm)],[t565670]) ).
cnf(t8388,plain,
top = join(X1,composition(top,complement(X1))),
inference(cp,[status(thm)],[t395,t8367]) ).
cnf(t8572,plain,
join(X1,composition(top,complement(X1))) = top,
inference(orient,[status(thm)],[t8388]) ).
cnf(t20306,plain,
composition(top,complement(zero)) = top,
inference(cp,[status(thm)],[t20280,t8572]) ).
cnf(t4104,plain,
complement(zero) = join(complement(zero),composition(converse(top),complement(zero))),
inference(cp,[status(thm)],[t59,t4092]) ).
cnf(t565913,plain,
complement(zero) = join(complement(zero),composition(top,complement(zero))),
inference(step,[status(thm)],[t4104,t401]) ).
cnf(t4703,plain,
join(complement(zero),composition(top,complement(zero))) = complement(zero),
inference(orient,[status(thm)],[t565913]) ).
cnf(t566037,plain,
composition(top,complement(zero)) = complement(zero),
inference(step,[status(thm)],[t4703,t8367]) ).
cnf(t8411,plain,
composition(top,complement(zero)) = complement(zero),
inference(rw,[status(thm)],[t566037]) ).
cnf(t8412,plain,
composition(top,complement(zero)) = complement(zero),
inference(orient,[status(thm)],[t8411]) ).
cnf(t566341,plain,
complement(zero) = top,
inference(step,[status(thm)],[t20306,t8412]) ).
cnf(t20422,plain,
complement(zero) = top,
inference(orient,[status(thm)],[t566341]) ).
cnf(t20427,plain,
meet(X1,zero) = complement(join(complement(X1),top)),
inference(cp,[status(thm)],[t91,t20422]) ).
cnf(t566370,plain,
meet(X1,zero) = complement(top),
inference(step,[status(thm)],[t20427,t387]) ).
cnf(t566371,plain,
meet(X1,zero) = zero,
inference(step,[status(thm)],[t566370,t103]) ).
cnf(t20548,plain,
meet(X1,zero) = zero,
inference(orient,[status(thm)],[t566371]) ).
cnf(t567886,plain,
composition(meet(X1,composition(complement(X1),meet(one,converse(X2)))),zero) = join(meet(composition(X1,meet(X2,one)),complement(X1)),composition(meet(X1,composition(complement(X1),converse(meet(X2,one)))),zero)),
inference(step,[status(thm)],[t567885,t20548]) ).
cnf(t20174,plain,
zero = composition(X1,zero),
inference(cp,[status(thm)],[t4058,t20167]) ).
cnf(t20208,plain,
composition(X1,zero) = zero,
inference(orient,[status(thm)],[t20174]) ).
cnf(t567887,plain,
zero = join(meet(composition(X1,meet(X2,one)),complement(X1)),composition(meet(X1,composition(complement(X1),converse(meet(X2,one)))),zero)),
inference(step,[status(thm)],[t567886,t20208]) ).
cnf(t567888,plain,
zero = join(meet(complement(X1),composition(X1,meet(X2,one))),composition(meet(X1,composition(complement(X1),converse(meet(X2,one)))),zero)),
inference(step,[status(thm)],[t567887,t112]) ).
cnf(t567889,plain,
zero = join(meet(complement(X1),composition(X1,meet(X2,one))),zero),
inference(step,[status(thm)],[t567888,t20208]) ).
cnf(t567890,plain,
zero = meet(complement(X1),composition(X1,meet(X2,one))),
inference(step,[status(thm)],[t567889,t20454]) ).
cnf(t110014,plain,
meet(complement(X1),composition(X1,meet(X2,one))) = zero,
inference(orient,[status(thm)],[t567890]) ).
cnf(t110052,plain,
composition(X1,meet(X2,one)) = join(zero,meet(complement(complement(X1)),composition(X1,meet(X2,one)))),
inference(cp,[status(thm)],[t46507,t110014]) ).
cnf(t567907,plain,
composition(X1,meet(X2,one)) = meet(complement(complement(X1)),composition(X1,meet(X2,one))),
inference(step,[status(thm)],[t110052,t20280]) ).
cnf(t567908,plain,
composition(X1,meet(X2,one)) = meet(X1,composition(X1,meet(X2,one))),
inference(step,[status(thm)],[t567907,t20605]) ).
cnf(t111894,plain,
meet(X1,composition(X1,meet(X2,one))) = composition(X1,meet(X2,one)),
inference(orient,[status(thm)],[t567908]) ).
cnf(t41,plain,
composition(meet(X1,composition(one,converse(X2))),meet(X2,composition(converse(X1),one))) = join(meet(composition(X1,X2),one),composition(meet(X1,composition(one,converse(X2))),meet(X2,converse(X1)))),
inference(cp,[status(thm)],[t33,t17]) ).
cnf(t566135,plain,
composition(meet(X1,converse(X2)),meet(X2,composition(converse(X1),one))) = join(meet(composition(X1,X2),one),composition(meet(X1,composition(one,converse(X2))),meet(X2,converse(X1)))),
inference(step,[status(thm)],[t41,t196]) ).
cnf(t566136,plain,
composition(meet(X1,converse(X2)),meet(X2,converse(X1))) = join(meet(composition(X1,X2),one),composition(meet(X1,composition(one,converse(X2))),meet(X2,converse(X1)))),
inference(step,[status(thm)],[t566135,t17]) ).
cnf(t566137,plain,
composition(meet(X1,converse(X2)),meet(X2,converse(X1))) = join(meet(one,composition(X1,X2)),composition(meet(X1,composition(one,converse(X2))),meet(X2,converse(X1)))),
inference(step,[status(thm)],[t566136,t112]) ).
cnf(t566138,plain,
composition(meet(X1,converse(X2)),meet(X2,converse(X1))) = join(meet(one,composition(X1,X2)),composition(meet(X1,converse(X2)),meet(X2,converse(X1)))),
inference(step,[status(thm)],[t566137,t196]) ).
cnf(t12838,plain,
join(meet(one,composition(X1,X2)),composition(meet(X1,converse(X2)),meet(X2,converse(X1)))) = composition(meet(X1,converse(X2)),meet(X2,converse(X1))),
inference(orient,[status(thm)],[t566138]) ).
cnf(t111978,plain,
composition(meet(one,converse(meet(X1,one))),meet(meet(X1,one),converse(one))) = join(composition(one,meet(X1,one)),composition(meet(one,converse(meet(X1,one))),meet(meet(X1,one),converse(one)))),
inference(cp,[status(thm)],[t12838,t111894]) ).
cnf(t21012,plain,
join(one,converse(meet(X1,one))) = converse(one),
inference(cp,[status(thm)],[t202,t21006]) ).
cnf(t566443,plain,
join(one,converse(meet(X1,one))) = one,
inference(step,[status(thm)],[t21012,t185]) ).
cnf(t21327,plain,
join(one,converse(meet(X1,one))) = one,
inference(orient,[status(thm)],[t566443]) ).
cnf(t22040,plain,
converse(meet(X1,one)) = meet(converse(meet(X1,one)),one),
inference(cp,[status(thm)],[t22013,t21327]) ).
cnf(t566507,plain,
converse(meet(X1,one)) = meet(one,converse(meet(X1,one))),
inference(step,[status(thm)],[t22040,t112]) ).
cnf(t24361,plain,
meet(one,converse(meet(X1,one))) = converse(meet(X1,one)),
inference(orient,[status(thm)],[t566507]) ).
cnf(t567950,plain,
composition(converse(meet(X1,one)),meet(meet(X1,one),converse(one))) = join(composition(one,meet(X1,one)),composition(meet(one,converse(meet(X1,one))),meet(meet(X1,one),converse(one)))),
inference(step,[status(thm)],[t111978,t24361]) ).
cnf(t567951,plain,
composition(meet(one,converse(X1)),meet(meet(X1,one),converse(one))) = join(composition(one,meet(X1,one)),composition(meet(one,converse(meet(X1,one))),meet(meet(X1,one),converse(one)))),
inference(step,[status(thm)],[t567950,t35299]) ).
cnf(t567952,plain,
composition(meet(one,converse(X1)),meet(X1,meet(one,converse(one)))) = join(composition(one,meet(X1,one)),composition(meet(one,converse(meet(X1,one))),meet(meet(X1,one),converse(one)))),
inference(step,[status(thm)],[t567951,t78317]) ).
cnf(t567953,plain,
composition(meet(one,converse(X1)),meet(X1,meet(one,one))) = join(composition(one,meet(X1,one)),composition(meet(one,converse(meet(X1,one))),meet(meet(X1,one),converse(one)))),
inference(step,[status(thm)],[t567952,t185]) ).
cnf(t567954,plain,
composition(meet(one,converse(X1)),meet(X1,one)) = join(composition(one,meet(X1,one)),composition(meet(one,converse(meet(X1,one))),meet(meet(X1,one),converse(one)))),
inference(step,[status(thm)],[t567953,t20487]) ).
cnf(t567955,plain,
composition(meet(one,converse(X1)),meet(X1,one)) = join(meet(X1,one),composition(meet(one,converse(meet(X1,one))),meet(meet(X1,one),converse(one)))),
inference(step,[status(thm)],[t567954,t196]) ).
cnf(t567956,plain,
composition(meet(one,converse(X1)),meet(X1,one)) = join(meet(X1,one),composition(converse(meet(X1,one)),meet(meet(X1,one),converse(one)))),
inference(step,[status(thm)],[t567955,t24361]) ).
cnf(t567957,plain,
composition(meet(one,converse(X1)),meet(X1,one)) = join(meet(X1,one),composition(meet(one,converse(X1)),meet(meet(X1,one),converse(one)))),
inference(step,[status(thm)],[t567956,t35299]) ).
cnf(t567958,plain,
composition(meet(one,converse(X1)),meet(X1,one)) = join(meet(X1,one),composition(meet(one,converse(X1)),meet(X1,meet(one,converse(one))))),
inference(step,[status(thm)],[t567957,t78317]) ).
cnf(t567959,plain,
composition(meet(one,converse(X1)),meet(X1,one)) = join(meet(X1,one),composition(meet(one,converse(X1)),meet(X1,meet(one,one)))),
inference(step,[status(thm)],[t567958,t185]) ).
cnf(t567960,plain,
composition(meet(one,converse(X1)),meet(X1,one)) = join(meet(X1,one),composition(meet(one,converse(X1)),meet(X1,one))),
inference(step,[status(thm)],[t567959,t20487]) ).
cnf(t110049,plain,
join(complement(complement(X1)),composition(X1,meet(X2,one))) = join(complement(complement(X1)),zero),
inference(cp,[status(thm)],[t33597,t110014]) ).
cnf(t567891,plain,
join(X1,composition(X1,meet(X2,one))) = join(complement(complement(X1)),zero),
inference(step,[status(thm)],[t110049,t20605]) ).
cnf(t567892,plain,
join(X1,composition(X1,meet(X2,one))) = complement(complement(X1)),
inference(step,[status(thm)],[t567891,t20454]) ).
cnf(t567893,plain,
join(X1,composition(X1,meet(X2,one))) = X1,
inference(step,[status(thm)],[t567892,t20605]) ).
cnf(t110071,plain,
join(X1,composition(X1,meet(X2,one))) = X1,
inference(orient,[status(thm)],[t567893]) ).
cnf(t110123,plain,
join(X1,converse(composition(converse(X1),meet(X2,one)))) = converse(converse(X1)),
inference(cp,[status(thm)],[t271,t110071]) ).
cnf(t567896,plain,
join(X1,composition(converse(meet(X2,one)),X1)) = converse(converse(X1)),
inference(step,[status(thm)],[t110123,t162]) ).
cnf(t567897,plain,
join(X1,composition(meet(one,converse(X2)),X1)) = converse(converse(X1)),
inference(step,[status(thm)],[t567896,t35299]) ).
cnf(t567898,plain,
join(X1,composition(meet(one,converse(X2)),X1)) = X1,
inference(step,[status(thm)],[t567897,t21]) ).
cnf(t110510,plain,
join(X1,composition(meet(one,converse(X2)),X1)) = X1,
inference(orient,[status(thm)],[t567898]) ).
cnf(t567961,plain,
composition(meet(one,converse(X1)),meet(X1,one)) = meet(X1,one),
inference(step,[status(thm)],[t567960,t110510]) ).
cnf(t116396,plain,
composition(meet(one,converse(X1)),meet(X1,one)) = meet(X1,one),
inference(orient,[status(thm)],[t567961]) ).
cnf(t116461,plain,
composition(meet(one,converse(X1)),meet(X1,one)) = meet(meet(one,converse(X1)),meet(X1,one)),
inference(cp,[status(thm)],[t111894,t116396]) ).
cnf(t567962,plain,
meet(X1,one) = meet(meet(one,converse(X1)),meet(X1,one)),
inference(step,[status(thm)],[t116461,t116396]) ).
cnf(t567963,plain,
meet(X1,one) = meet(one,meet(converse(X1),meet(X1,one))),
inference(step,[status(thm)],[t567962,t78317]) ).
cnf(t26554,plain,
meet(X1,meet(X2,X3)) = meet(meet(X1,meet(X2,X3)),X3),
inference(cp,[status(thm)],[t22013,t26536]) ).
cnf(t567059,plain,
meet(X1,meet(X2,X3)) = meet(X3,meet(X1,meet(X2,X3))),
inference(step,[status(thm)],[t26554,t112]) ).
cnf(t53643,plain,
meet(X1,meet(X2,meet(X3,X1))) = meet(X2,meet(X3,X1)),
inference(orient,[status(thm)],[t567059]) ).
cnf(t567964,plain,
meet(X1,one) = meet(converse(X1),meet(X1,one)),
inference(step,[status(thm)],[t567963,t53643]) ).
cnf(t116513,plain,
meet(converse(X1),meet(X1,one)) = meet(X1,one),
inference(orient,[status(thm)],[t567964]) ).
cnf(t116575,plain,
meet(meet(X1,one),converse(X1)) = join(meet(X1,one),meet(meet(X1,one),converse(X1))),
inference(cp,[status(thm)],[t585,t116513]) ).
cnf(t567967,plain,
meet(X1,meet(one,converse(X1))) = join(meet(X1,one),meet(meet(X1,one),converse(X1))),
inference(step,[status(thm)],[t116575,t78317]) ).
cnf(t567968,plain,
meet(X1,meet(one,converse(X1))) = meet(X1,one),
inference(step,[status(thm)],[t567967,t20965]) ).
cnf(t117195,plain,
meet(X1,meet(one,converse(X1))) = meet(X1,one),
inference(orient,[status(thm)],[t567968]) ).
cnf(t117253,plain,
meet(converse(X1),one) = meet(converse(X1),meet(one,X1)),
inference(cp,[status(thm)],[t117195,t21]) ).
cnf(t567969,plain,
meet(one,converse(X1)) = meet(converse(X1),meet(one,X1)),
inference(step,[status(thm)],[t117253,t112]) ).
cnf(t116555,plain,
meet(X1,one) = meet(converse(X1),meet(one,X1)),
inference(cp,[status(thm)],[t116513,t112]) ).
cnf(t116967,plain,
meet(converse(X1),meet(one,X1)) = meet(X1,one),
inference(orient,[status(thm)],[t116555]) ).
cnf(t567970,plain,
meet(one,converse(X1)) = meet(X1,one),
inference(step,[status(thm)],[t567969,t116967]) ).
cnf(t117350,plain,
meet(one,converse(X1)) = meet(X1,one),
inference(orient,[status(thm)],[t567970]) ).
cnf(t569573,plain,
converse(composition(meet(one,X1),X2)) = composition(converse(X2),meet(X1,one)),
inference(step,[status(thm)],[t35231,t117350]) ).
cnf(t253482,plain,
converse(composition(meet(one,X1),X2)) = composition(converse(X2),meet(X1,one)),
inference(orient,[status(thm)],[t569573]) ).
cnf(t253636,plain,
composition(converse(X1),meet(composition(one,meet(X2,one)),one)) = converse(composition(composition(one,meet(X2,one)),X1)),
inference(cp,[status(thm)],[t253482,t111894]) ).
cnf(t569574,plain,
composition(converse(X1),meet(one,composition(one,meet(X2,one)))) = converse(composition(composition(one,meet(X2,one)),X1)),
inference(step,[status(thm)],[t253636,t112]) ).
cnf(t569575,plain,
composition(converse(X1),composition(one,meet(X2,one))) = converse(composition(composition(one,meet(X2,one)),X1)),
inference(step,[status(thm)],[t569574,t111894]) ).
cnf(t569576,plain,
composition(converse(X1),meet(X2,one)) = converse(composition(composition(one,meet(X2,one)),X1)),
inference(step,[status(thm)],[t569575,t196]) ).
cnf(t569577,plain,
composition(converse(X1),meet(X2,one)) = converse(composition(one,composition(meet(X2,one),X1))),
inference(step,[status(thm)],[t569576,t22]) ).
cnf(t569578,plain,
composition(converse(X1),meet(X2,one)) = converse(composition(meet(X2,one),X1)),
inference(step,[status(thm)],[t569577,t196]) ).
cnf(t254080,plain,
converse(composition(meet(X1,one),X2)) = composition(converse(X2),meet(X1,one)),
inference(orient,[status(thm)],[t569578]) ).
cnf(t33293,plain,
meet(X1,join(meet(complement(X1),X2),X3)) = meet(X1,join(complement(X1),X3)),
inference(cp,[status(thm)],[t33278,t26029]) ).
cnf(t567320,plain,
meet(X1,join(meet(complement(X1),X2),X3)) = meet(X1,X3),
inference(step,[status(thm)],[t33293,t33278]) ).
cnf(t65936,plain,
meet(X1,join(meet(complement(X1),X2),X3)) = meet(X1,X3),
inference(orient,[status(thm)],[t567320]) ).
cnf(t8181,plain,
composition(X1,top) = join(composition(X1,top),composition(X1,X2)),
inference(cp,[status(thm)],[t8178,t48]) ).
cnf(t9701,plain,
join(composition(X1,top),composition(X1,X2)) = composition(X1,top),
inference(orient,[status(thm)],[t8181]) ).
cnf(t62,plain,
complement(top) = join(complement(top),composition(converse(sk0),complement(sk0))),
inference(cp,[status(thm)],[t59,t43]) ).
cnf(t565726,plain,
zero = join(complement(top),composition(converse(sk0),complement(sk0))),
inference(step,[status(thm)],[t62,t103]) ).
cnf(t565727,plain,
zero = join(zero,composition(converse(sk0),complement(sk0))),
inference(step,[status(thm)],[t565726,t103]) ).
cnf(t1438,plain,
join(zero,composition(converse(sk0),complement(sk0))) = zero,
inference(orient,[status(thm)],[t565727]) ).
cnf(t566317,plain,
composition(converse(sk0),complement(sk0)) = zero,
inference(step,[status(thm)],[t1438,t20280]) ).
cnf(t20400,plain,
composition(converse(sk0),complement(sk0)) = zero,
inference(rw,[status(thm)],[t566317]) ).
cnf(t20844,plain,
composition(converse(sk0),complement(sk0)) = zero,
inference(orient,[status(thm)],[t20400]) ).
cnf(t20855,plain,
composition(converse(complement(sk0)),sk0) = converse(zero),
inference(cp,[status(thm)],[t162,t20844]) ).
cnf(t566419,plain,
composition(converse(complement(sk0)),sk0) = zero,
inference(step,[status(thm)],[t20855,t20786]) ).
cnf(t20873,plain,
composition(converse(complement(sk0)),sk0) = zero,
inference(orient,[status(thm)],[t566419]) ).
cnf(t20884,plain,
complement(sk0) = join(complement(sk0),composition(converse(converse(complement(sk0))),complement(zero))),
inference(cp,[status(thm)],[t59,t20873]) ).
cnf(t566420,plain,
complement(sk0) = join(complement(sk0),composition(complement(sk0),complement(zero))),
inference(step,[status(thm)],[t20884,t21]) ).
cnf(t566421,plain,
complement(sk0) = join(complement(sk0),composition(complement(sk0),top)),
inference(step,[status(thm)],[t566420,t20422]) ).
cnf(t566422,plain,
complement(sk0) = composition(complement(sk0),top),
inference(step,[status(thm)],[t566421,t8278]) ).
cnf(t20897,plain,
composition(complement(sk0),top) = complement(sk0),
inference(orient,[status(thm)],[t566422]) ).
cnf(t20898,plain,
composition(complement(sk0),top) = join(complement(sk0),composition(complement(sk0),X1)),
inference(cp,[status(thm)],[t9701,t20897]) ).
cnf(t566508,plain,
complement(sk0) = join(complement(sk0),composition(complement(sk0),X1)),
inference(step,[status(thm)],[t20898,t20897]) ).
cnf(t24418,plain,
join(complement(sk0),composition(complement(sk0),X1)) = complement(sk0),
inference(orient,[status(thm)],[t566508]) ).
cnf(t24419,plain,
composition(complement(sk0),X1) = meet(composition(complement(sk0),X1),complement(sk0)),
inference(cp,[status(thm)],[t22013,t24418]) ).
cnf(t567000,plain,
composition(complement(sk0),X1) = meet(complement(sk0),composition(complement(sk0),X1)),
inference(step,[status(thm)],[t24419,t112]) ).
cnf(t49650,plain,
meet(complement(sk0),composition(complement(sk0),X1)) = composition(complement(sk0),X1),
inference(orient,[status(thm)],[t567000]) ).
cnf(t65994,plain,
meet(sk0,X1) = meet(sk0,join(composition(complement(sk0),X2),X1)),
inference(cp,[status(thm)],[t65936,t49650]) ).
cnf(t82125,plain,
meet(sk0,join(composition(complement(sk0),X1),X2)) = meet(sk0,X2),
inference(orient,[status(thm)],[t65994]) ).
cnf(t82127,plain,
meet(sk0,composition(X1,X2)) = meet(sk0,composition(join(complement(sk0),X1),X2)),
inference(cp,[status(thm)],[t82125,t24]) ).
cnf(t562761,plain,
meet(sk0,composition(join(complement(sk0),X1),X2)) = meet(sk0,composition(X1,X2)),
inference(orient,[status(thm)],[t82127]) ).
cnf(t72053,plain,
meet(X1,X2) = meet(X1,meet(join(X1,X3),X2)),
inference(cp,[status(thm)],[t71849,t48]) ).
cnf(t72747,plain,
meet(X1,meet(join(X1,X2),X3)) = meet(X1,X3),
inference(orient,[status(thm)],[t72053]) ).
cnf(t72825,plain,
meet(X1,X2) = meet(X1,meet(composition(X1,top),X2)),
inference(cp,[status(thm)],[t72747,t8278]) ).
cnf(t73281,plain,
meet(X1,meet(composition(X1,top),X2)) = meet(X1,X2),
inference(orient,[status(thm)],[t72825]) ).
cnf(t73353,plain,
join(complement(X1),meet(composition(X1,top),X2)) = join(complement(X1),meet(X1,X2)),
inference(cp,[status(thm)],[t33597,t73281]) ).
cnf(t569923,plain,
join(complement(X1),meet(composition(X1,top),X2)) = join(complement(X1),X2),
inference(step,[status(thm)],[t73353,t33597]) ).
cnf(t317345,plain,
join(complement(X1),meet(composition(X1,top),X2)) = join(complement(X1),X2),
inference(orient,[status(thm)],[t569923]) ).
cnf(t562839,plain,
meet(sk0,composition(meet(composition(sk0,top),X1),X2)) = meet(sk0,composition(join(complement(sk0),X1),X2)),
inference(cp,[status(thm)],[t562761,t317345]) ).
cnf(t570908,plain,
meet(sk0,composition(meet(sk0,X1),X2)) = meet(sk0,composition(join(complement(sk0),X1),X2)),
inference(step,[status(thm)],[t562839,t43]) ).
cnf(t416,plain,
composition(top,converse(sk0)) = converse(sk0),
inference(cp,[status(thm)],[t413,t43]) ).
cnf(t430,plain,
composition(top,converse(sk0)) = converse(sk0),
inference(orient,[status(thm)],[t416]) ).
cnf(t431,plain,
composition(join(top,X1),converse(sk0)) = join(converse(sk0),composition(X1,converse(sk0))),
inference(cp,[status(thm)],[t24,t430]) ).
cnf(t565679,plain,
composition(top,converse(sk0)) = join(converse(sk0),composition(X1,converse(sk0))),
inference(step,[status(thm)],[t431,t394]) ).
cnf(t565680,plain,
converse(sk0) = join(converse(sk0),composition(X1,converse(sk0))),
inference(step,[status(thm)],[t565679,t430]) ).
cnf(t512,plain,
join(converse(sk0),composition(X1,converse(sk0))) = converse(sk0),
inference(orient,[status(thm)],[t565680]) ).
cnf(t518,plain,
join(sk0,converse(composition(X1,converse(sk0)))) = converse(converse(sk0)),
inference(cp,[status(thm)],[t271,t512]) ).
cnf(t565683,plain,
join(sk0,composition(sk0,converse(X1))) = converse(converse(sk0)),
inference(step,[status(thm)],[t518,t152]) ).
cnf(t565684,plain,
join(sk0,composition(sk0,converse(X1))) = sk0,
inference(step,[status(thm)],[t565683,t21]) ).
cnf(t539,plain,
join(sk0,composition(sk0,converse(X1))) = sk0,
inference(orient,[status(thm)],[t565684]) ).
cnf(t545,plain,
sk0 = join(sk0,composition(sk0,X1)),
inference(cp,[status(thm)],[t539,t21]) ).
cnf(t550,plain,
join(sk0,composition(sk0,X1)) = sk0,
inference(orient,[status(thm)],[t545]) ).
cnf(t551,plain,
join(sk0,join(composition(sk0,X1),X2)) = join(sk0,X2),
inference(cp,[status(thm)],[t51,t550]) ).
cnf(t573,plain,
join(sk0,join(composition(sk0,X1),X2)) = join(sk0,X2),
inference(orient,[status(thm)],[t551]) ).
cnf(t574,plain,
join(sk0,composition(X1,X2)) = join(sk0,composition(join(sk0,X1),X2)),
inference(cp,[status(thm)],[t573,t24]) ).
cnf(t2188,plain,
join(sk0,composition(join(sk0,X1),X2)) = join(sk0,composition(X1,X2)),
inference(orient,[status(thm)],[t574]) ).
cnf(t20991,plain,
join(sk0,composition(meet(sk0,X1),X2)) = join(sk0,composition(sk0,X2)),
inference(cp,[status(thm)],[t2188,t20965]) ).
cnf(t566474,plain,
join(sk0,composition(meet(sk0,X1),X2)) = sk0,
inference(step,[status(thm)],[t20991,t550]) ).
cnf(t23033,plain,
join(sk0,composition(meet(sk0,X1),X2)) = sk0,
inference(orient,[status(thm)],[t566474]) ).
cnf(t23036,plain,
composition(meet(sk0,X1),X2) = meet(composition(meet(sk0,X1),X2),sk0),
inference(cp,[status(thm)],[t22013,t23033]) ).
cnf(t567034,plain,
composition(meet(sk0,X1),X2) = meet(sk0,composition(meet(sk0,X1),X2)),
inference(step,[status(thm)],[t23036,t112]) ).
cnf(t51991,plain,
meet(sk0,composition(meet(sk0,X1),X2)) = composition(meet(sk0,X1),X2),
inference(orient,[status(thm)],[t567034]) ).
cnf(t570909,plain,
composition(meet(sk0,X1),X2) = meet(sk0,composition(join(complement(sk0),X1),X2)),
inference(step,[status(thm)],[t570908,t51991]) ).
cnf(t570910,plain,
composition(meet(sk0,X1),X2) = meet(sk0,composition(X1,X2)),
inference(step,[status(thm)],[t570909,t562761]) ).
cnf(t563104,plain,
composition(meet(sk0,X1),X2) = meet(sk0,composition(X1,X2)),
inference(orient,[status(thm)],[t570910]) ).
cnf(t563433,plain,
composition(converse(X1),meet(sk0,one)) = converse(meet(sk0,composition(one,X1))),
inference(cp,[status(thm)],[t254080,t563104]) ).
cnf(t570934,plain,
composition(converse(X1),meet(sk0,one)) = converse(meet(sk0,X1)),
inference(step,[status(thm)],[t563433,t196]) ).
cnf(t564521,plain,
composition(converse(X1),meet(sk0,one)) = converse(meet(sk0,X1)),
inference(orient,[status(thm)],[t570934]) ).
cnf(t564647,plain,
converse(meet(sk0,converse(X1))) = composition(X1,meet(sk0,one)),
inference(cp,[status(thm)],[t564521,t21]) ).
cnf(t35056,plain,
converse(complement(join(converse(X1),X2))) = complement(join(X1,converse(X2))),
inference(cp,[status(thm)],[t35037,t271]) ).
cnf(t36069,plain,
converse(complement(join(converse(X1),X2))) = complement(join(X1,converse(X2))),
inference(orient,[status(thm)],[t35056]) ).
cnf(t35069,plain,
complement(meet(converse(X1),X2)) = join(converse(complement(X1)),complement(X2)),
inference(cp,[status(thm)],[t21694,t35037]) ).
cnf(t36720,plain,
join(converse(complement(X1)),complement(X2)) = complement(meet(converse(X1),X2)),
inference(orient,[status(thm)],[t35069]) ).
cnf(t36770,plain,
complement(join(complement(X1),converse(complement(X2)))) = converse(complement(complement(meet(converse(X1),X2)))),
inference(cp,[status(thm)],[t36069,t36720]) ).
cnf(t566782,plain,
meet(X1,complement(converse(complement(X2)))) = converse(complement(complement(meet(converse(X1),X2)))),
inference(step,[status(thm)],[t36770,t21385]) ).
cnf(t566783,plain,
meet(X1,converse(X2)) = converse(complement(complement(meet(converse(X1),X2)))),
inference(step,[status(thm)],[t566782,t34963]) ).
cnf(t566784,plain,
meet(X1,converse(X2)) = converse(meet(converse(X1),X2)),
inference(step,[status(thm)],[t566783,t20605]) ).
cnf(t36792,plain,
converse(meet(converse(X1),X2)) = meet(X1,converse(X2)),
inference(orient,[status(thm)],[t566784]) ).
cnf(t36811,plain,
meet(X1,converse(X2)) = converse(meet(X2,converse(X1))),
inference(cp,[status(thm)],[t36792,t112]) ).
cnf(t36931,plain,
converse(meet(X1,converse(X2))) = meet(X2,converse(X1)),
inference(orient,[status(thm)],[t36811]) ).
cnf(t570935,plain,
meet(X1,converse(sk0)) = composition(X1,meet(sk0,one)),
inference(step,[status(thm)],[t564647,t36931]) ).
cnf(t564769,plain,
composition(X1,meet(sk0,one)) = meet(X1,converse(sk0)),
inference(orient,[status(thm)],[t570935]) ).
cnf(t564854,plain,
composition(X1,composition(meet(sk0,one),X2)) = composition(meet(X1,converse(sk0)),X2),
inference(cp,[status(thm)],[t22,t564769]) ).
cnf(t570951,plain,
composition(X1,meet(sk0,composition(one,X2))) = composition(meet(X1,converse(sk0)),X2),
inference(step,[status(thm)],[t564854,t563104]) ).
cnf(t570952,plain,
composition(X1,meet(sk0,X2)) = composition(meet(X1,converse(sk0)),X2),
inference(step,[status(thm)],[t570951,t196]) ).
cnf(t565113,plain,
composition(meet(X1,converse(sk0)),X2) = composition(X1,meet(sk0,X2)),
inference(orient,[status(thm)],[t570952]) ).
cnf(t22015,plain,
meet(X1,X2) = meet(meet(X1,X2),X1),
inference(cp,[status(thm)],[t22013,t20965]) ).
cnf(t566454,plain,
meet(X1,X2) = meet(X1,meet(X1,X2)),
inference(step,[status(thm)],[t22015,t112]) ).
cnf(t22680,plain,
meet(X1,meet(X1,X2)) = meet(X1,X2),
inference(orient,[status(thm)],[t566454]) ).
cnf(c17,plain,
join(composition(sk1,meet(sk0,sk2)),composition(meet(sk1,converse(sk0)),meet(sk0,sk2))) != composition(meet(sk1,converse(sk0)),meet(sk0,sk2)),
inference(cnf_transformation,[status(esa)],[f16_sk]) ).
cnf(goal_0,negated_conjecture,
join(composition(sk1,meet(sk0,sk2)),composition(meet(sk1,converse(sk0)),meet(sk0,sk2))) != composition(meet(sk1,converse(sk0)),meet(sk0,sk2)),
inference(equality_encoding,[status(esa)],[c17]) ).
cnf(g0_0,plain,
composition(join(sk1,meet(sk1,converse(sk0))),meet(sk0,sk2)) != composition(meet(sk1,converse(sk0)),meet(sk0,sk2)),
inference(rw,[status(thm)],[goal_0,t24]) ).
cnf(g0_1,plain,
composition(sk1,meet(sk0,sk2)) != composition(meet(sk1,converse(sk0)),meet(sk0,sk2)),
inference(rw,[status(thm)],[g0_0,t20965]) ).
cnf(g0_2,plain,
composition(sk1,meet(sk0,sk2)) != composition(sk1,meet(sk0,meet(sk0,sk2))),
inference(rw,[status(thm)],[g0_1,t565113]) ).
cnf(g0_3,plain,
composition(sk1,meet(sk0,sk2)) != composition(sk1,meet(sk0,sk2)),
inference(rw,[status(thm)],[g0_2,t22680]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_3]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : REL034+2 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.10/15.39 % Computer : n017.cluster.edu
% 0.10/15.39 % Model : x86_64 x86_64
% 0.10/15.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/15.39 % Memory : 8046.5625MB
% 0.10/15.39 % OS : Linux 6.8.0-71-generic
% 0.10/15.40 % CPULimit : 300
% 0.10/15.40 % WCLimit : 300
% 0.10/15.40 % DateTime : Thu Sep 24 07:25:16 UTC 2026
% 0.14/15.40 % CPUTime :
% 0.14/15.40 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 256.56/54.25 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 256.56/54.25 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------