%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : REL019+2 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n002.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:34:47 PM UTC 2026
% Result : Theorem 253.69s 37.04s
% Output : Proof 253.69s
% Verified :
% SZS Type : Refutation
% Derivation depth : 113
% Number of leaves : 15
% Syntax : Number of formulae : 568 ( 564 unt; 0 def)
% Number of atoms : 576 ( 575 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 16 ( 8 ~; 0 |; 6 &)
% ( 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 : 10 ( 10 usr; 5 con; 0-2 aty)
% Number of variables : 705 ( 90 sgn 88 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
! [X0,X1] : meet(X0,X1) = complement(join(complement(X0),complement(X1))),
file('/export/starexec/sandbox/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(t7,plain,
complement(join(complement(X1),complement(X2))) = meet(X1,X2),
inference(equality_encoding,[status(esa)],[c3]) ).
cnf(t100,plain,
complement(join(complement(X1),complement(X2))) = meet(X1,X2),
inference(orient,[status(thm)],[t7]) ).
fof(f0,axiom,
! [X0,X1] : join(X0,X1) = join(X1,X0),
file('/export/starexec/sandbox/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(t6,plain,
join(X1,X2) = join(X2,X1),
inference(equality_encoding,[status(esa)],[c0]) ).
cnf(t54,plain,
join(X1,X2) = join(X2,X1),
inference(orient,[status(thm)],[t6]) ).
cnf(t102,plain,
meet(X1,X2) = complement(join(complement(X2),complement(X1))),
inference(cp,[status(thm)],[t100,t54]) ).
cnf(t459130,plain,
meet(X1,X2) = meet(X2,X1),
inference(step,[status(thm)],[t102,t100]) ).
cnf(t121,plain,
meet(X1,X2) = meet(X2,X1),
inference(orient,[status(thm)],[t459130]) ).
fof(f9,axiom,
! [X0,X1] : converse(composition(X0,X1)) = composition(converse(X1),converse(X0)),
file('/export/starexec/sandbox/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(t8,plain,
composition(converse(X1),converse(X2)) = converse(composition(X2,X1)),
inference(equality_encoding,[status(esa)],[c9]) ).
cnf(t28,plain,
composition(converse(X1),converse(X2)) = converse(composition(X2,X1)),
inference(orient,[status(thm)],[t8]) ).
fof(f1,axiom,
! [X0,X1,X2] : join(X0,join(X1,X2)) = join(join(X0,X1),X2),
file('/export/starexec/sandbox/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(t11,plain,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
inference(equality_encoding,[status(esa)],[c1]) ).
cnf(t57,plain,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
inference(orient,[status(thm)],[t11]) ).
fof(f11,axiom,
! [X0] : top = join(X0,complement(X0)),
file('/export/starexec/sandbox/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(t4,plain,
join(X1,complement(X1)) = top,
inference(equality_encoding,[status(esa)],[c11]) ).
cnf(t62,plain,
join(X1,complement(X1)) = top,
inference(orient,[status(thm)],[t4]) ).
cnf(t64,plain,
join(X1,join(complement(X1),X2)) = join(top,X2),
inference(cp,[status(thm)],[t57,t62]) ).
cnf(t395,plain,
join(X1,join(complement(X1),X2)) = join(top,X2),
inference(orient,[status(thm)],[t64]) ).
fof(f10,axiom,
! [X0,X1] : join(composition(converse(X0),complement(composition(X0,X1))),complement(X1)) = complement(X1),
file('/export/starexec/sandbox/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(t13,plain,
join(composition(converse(X1),complement(composition(X1,X2))),complement(X2)) = complement(X2),
inference(equality_encoding,[status(esa)],[c10]) ).
cnf(t459127,plain,
join(complement(X2),composition(converse(X1),complement(composition(X1,X2)))) = complement(X2),
inference(step,[status(thm)],[t13,t54]) ).
cnf(t65,plain,
join(complement(X1),composition(converse(X2),complement(composition(X2,X1)))) = complement(X1),
inference(orient,[status(thm)],[t459127]) ).
fof(f7,axiom,
! [X0] : converse(converse(X0)) = X0,
file('/export/starexec/sandbox/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(t3,plain,
converse(converse(X1)) = X1,
inference(equality_encoding,[status(esa)],[c7]) ).
cnf(t22,plain,
converse(converse(X1)) = X1,
inference(orient,[status(thm)],[t3]) ).
cnf(t30,plain,
converse(composition(converse(X1),X2)) = composition(converse(X2),X1),
inference(cp,[status(thm)],[t28,t22]) ).
cnf(t176,plain,
converse(composition(converse(X1),X2)) = composition(converse(X2),X1),
inference(orient,[status(thm)],[t30]) ).
fof(f5,axiom,
! [X0] : composition(X0,one) = X0,
file('/export/starexec/sandbox/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(t18,plain,
composition(X1,one) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t177,plain,
composition(converse(one),X1) = converse(converse(X1)),
inference(cp,[status(thm)],[t176,t18]) ).
cnf(t459132,plain,
composition(converse(one),X1) = X1,
inference(step,[status(thm)],[t177,t22]) ).
cnf(t189,plain,
composition(converse(one),X1) = X1,
inference(orient,[status(thm)],[t459132]) ).
cnf(t190,plain,
one = converse(one),
inference(cp,[status(thm)],[t189,t18]) ).
cnf(t199,plain,
converse(one) = one,
inference(orient,[status(thm)],[t190]) ).
cnf(t459133,plain,
composition(one,X1) = X1,
inference(step,[status(thm)],[t189,t199]) ).
cnf(t209,plain,
composition(one,X1) = X1,
inference(rw,[status(thm)],[t459133]) ).
cnf(t210,plain,
composition(one,X1) = X1,
inference(orient,[status(thm)],[t209]) ).
cnf(t213,plain,
complement(X1) = join(complement(X1),composition(converse(one),complement(X1))),
inference(cp,[status(thm)],[t65,t210]) ).
cnf(t459135,plain,
complement(X1) = join(complement(X1),composition(one,complement(X1))),
inference(step,[status(thm)],[t213,t199]) ).
cnf(t459136,plain,
complement(X1) = join(complement(X1),complement(X1)),
inference(step,[status(thm)],[t459135,t210]) ).
cnf(t239,plain,
join(complement(X1),complement(X1)) = complement(X1),
inference(orient,[status(thm)],[t459136]) ).
cnf(t249,plain,
meet(X1,X1) = complement(complement(X1)),
inference(cp,[status(thm)],[t100,t239]) ).
cnf(t256,plain,
meet(X1,X1) = complement(complement(X1)),
inference(orient,[status(thm)],[t249]) ).
cnf(t264,plain,
top = join(complement(X1),meet(X1,X1)),
inference(cp,[status(thm)],[t62,t256]) ).
cnf(t280,plain,
join(complement(X1),meet(X1,X1)) = top,
inference(orient,[status(thm)],[t264]) ).
cnf(t399,plain,
join(top,meet(X1,X1)) = join(X1,top),
inference(cp,[status(thm)],[t395,t280]) ).
cnf(t401,plain,
join(top,complement(X1)) = join(X1,complement(X1)),
inference(cp,[status(thm)],[t395,t239]) ).
cnf(t459145,plain,
join(top,complement(X1)) = top,
inference(step,[status(thm)],[t401,t62]) ).
cnf(t414,plain,
join(top,complement(X1)) = top,
inference(orient,[status(thm)],[t459145]) ).
cnf(t415,plain,
top = join(top,meet(X1,X2)),
inference(cp,[status(thm)],[t414,t100]) ).
cnf(t422,plain,
join(top,meet(X1,X2)) = top,
inference(orient,[status(thm)],[t415]) ).
cnf(t459147,plain,
top = join(X1,top),
inference(step,[status(thm)],[t399,t422]) ).
cnf(t427,plain,
join(X1,top) = top,
inference(orient,[status(thm)],[t459147]) ).
cnf(t428,plain,
top = join(top,X1),
inference(cp,[status(thm)],[t427,t54]) ).
cnf(t435,plain,
join(top,X1) = top,
inference(orient,[status(thm)],[t428]) ).
fof(f8,axiom,
! [X0,X1] : converse(join(X0,X1)) = join(converse(X0),converse(X1)),
file('/export/starexec/sandbox/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(t9,plain,
join(converse(X1),converse(X2)) = converse(join(X1,X2)),
inference(equality_encoding,[status(esa)],[c8]) ).
cnf(t73,plain,
join(converse(X1),converse(X2)) = converse(join(X1,X2)),
inference(orient,[status(thm)],[t9]) ).
cnf(t75,plain,
converse(join(converse(X1),X2)) = join(X1,converse(X2)),
inference(cp,[status(thm)],[t73,t22]) ).
cnf(t285,plain,
converse(join(converse(X1),X2)) = join(X1,converse(X2)),
inference(orient,[status(thm)],[t75]) ).
cnf(t287,plain,
join(X1,converse(complement(converse(X1)))) = converse(top),
inference(cp,[status(thm)],[t285,t62]) ).
cnf(t321,plain,
join(X1,converse(complement(converse(X1)))) = converse(top),
inference(orient,[status(thm)],[t287]) ).
cnf(t438,plain,
top = converse(top),
inference(cp,[status(thm)],[t435,t321]) ).
cnf(t443,plain,
converse(top) = top,
inference(orient,[status(thm)],[t438]) ).
cnf(t449,plain,
converse(composition(top,X1)) = composition(converse(X1),top),
inference(cp,[status(thm)],[t28,t443]) ).
cnf(t493,plain,
converse(composition(top,X1)) = composition(converse(X1),top),
inference(orient,[status(thm)],[t449]) ).
fof(f4,axiom,
! [X0,X1,X2] : composition(X0,composition(X1,X2)) = composition(composition(X0,X1),X2),
file('/export/starexec/sandbox/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(t10,plain,
composition(composition(X1,X2),X3) = composition(X1,composition(X2,X3)),
inference(equality_encoding,[status(esa)],[c4]) ).
cnf(t23,plain,
composition(composition(X1,X2),X3) = composition(X1,composition(X2,X3)),
inference(orient,[status(thm)],[t10]) ).
fof(f6,axiom,
! [X0,X1,X2] : composition(join(X0,X1),X2) = join(composition(X0,X2),composition(X1,X2)),
file('/export/starexec/sandbox/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(t12,plain,
join(composition(X1,X2),composition(X3,X2)) = composition(join(X1,X3),X2),
inference(equality_encoding,[status(esa)],[c6]) ).
cnf(t25,plain,
join(composition(X1,X2),composition(X3,X2)) = composition(join(X1,X3),X2),
inference(orient,[status(thm)],[t12]) ).
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/sandbox/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(t17,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(t34,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)],[t17]) ).
cnf(t35,plain,
composition(meet(X1,composition(X2,converse(one))),meet(one,composition(converse(X1),X2))) = join(meet(X1,X2),composition(meet(X1,composition(X2,converse(one))),meet(one,composition(converse(X1),X2)))),
inference(cp,[status(thm)],[t34,t18]) ).
cnf(t459373,plain,
composition(meet(X1,composition(X2,one)),meet(one,composition(converse(X1),X2))) = join(meet(X1,X2),composition(meet(X1,composition(X2,converse(one))),meet(one,composition(converse(X1),X2)))),
inference(step,[status(thm)],[t35,t199]) ).
cnf(t459374,plain,
composition(meet(X1,X2),meet(one,composition(converse(X1),X2))) = join(meet(X1,X2),composition(meet(X1,composition(X2,converse(one))),meet(one,composition(converse(X1),X2)))),
inference(step,[status(thm)],[t459373,t18]) ).
cnf(t459375,plain,
composition(meet(X1,X2),meet(one,composition(converse(X1),X2))) = join(meet(X1,X2),composition(meet(X1,composition(X2,one)),meet(one,composition(converse(X1),X2)))),
inference(step,[status(thm)],[t459374,t199]) ).
cnf(t459376,plain,
composition(meet(X1,X2),meet(one,composition(converse(X1),X2))) = join(meet(X1,X2),composition(meet(X1,X2),meet(one,composition(converse(X1),X2)))),
inference(step,[status(thm)],[t459375,t18]) ).
cnf(t3618,plain,
join(meet(X1,X2),composition(meet(X1,X2),meet(one,composition(converse(X1),X2)))) = composition(meet(X1,X2),meet(one,composition(converse(X1),X2))),
inference(orient,[status(thm)],[t459376]) ).
cnf(t77,plain,
join(converse(X1),join(converse(X2),X3)) = join(converse(join(X1,X2)),X3),
inference(cp,[status(thm)],[t57,t73]) ).
cnf(t4911,plain,
join(converse(X1),join(converse(X2),X3)) = join(converse(join(X1,X2)),X3),
inference(orient,[status(thm)],[t77]) ).
cnf(t404,plain,
join(top,X1) = join(X2,join(X1,complement(X2))),
inference(cp,[status(thm)],[t395,t54]) ).
cnf(t459156,plain,
top = join(X2,join(X1,complement(X2))),
inference(step,[status(thm)],[t404,t435]) ).
cnf(t517,plain,
join(X1,join(X2,complement(X1))) = top,
inference(orient,[status(thm)],[t459156]) ).
cnf(t4915,plain,
join(converse(join(X1,X2)),complement(converse(X1))) = top,
inference(cp,[status(thm)],[t4911,t517]) ).
cnf(t459433,plain,
join(complement(converse(X1)),converse(join(X1,X2))) = top,
inference(step,[status(thm)],[t4915,t54]) ).
cnf(t4978,plain,
join(complement(converse(X1)),converse(join(X1,X2))) = top,
inference(orient,[status(thm)],[t459433]) ).
cnf(t5027,plain,
top = join(complement(converse(converse(X1))),converse(converse(join(X1,X2)))),
inference(cp,[status(thm)],[t4978,t73]) ).
cnf(t459434,plain,
top = join(complement(X1),converse(converse(join(X1,X2)))),
inference(step,[status(thm)],[t5027,t22]) ).
cnf(t459435,plain,
top = join(complement(X1),join(X1,X2)),
inference(step,[status(thm)],[t459434,t22]) ).
cnf(t5041,plain,
join(complement(X1),join(X1,X2)) = top,
inference(orient,[status(thm)],[t459435]) ).
cnf(t5084,plain,
top = join(complement(X1),join(X2,X1)),
inference(cp,[status(thm)],[t5041,t54]) ).
cnf(t5089,plain,
join(complement(X1),join(X2,X1)) = top,
inference(orient,[status(thm)],[t5084]) ).
cnf(t67,plain,
complement(one) = join(complement(one),composition(converse(X1),complement(X1))),
inference(cp,[status(thm)],[t65,t18]) ).
cnf(t2515,plain,
join(complement(one),composition(converse(X1),complement(X1))) = complement(one),
inference(orient,[status(thm)],[t67]) ).
cnf(t2522,plain,
complement(one) = join(complement(one),composition(top,complement(top))),
inference(cp,[status(thm)],[t2515,t443]) ).
cnf(t101,plain,
meet(X1,complement(X1)) = complement(top),
inference(cp,[status(thm)],[t100,t62]) ).
fof(f12,axiom,
! [X0] : zero = meet(X0,complement(X0)),
file('/export/starexec/sandbox/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(t5,plain,
meet(X1,complement(X1)) = zero,
inference(equality_encoding,[status(esa)],[c12]) ).
cnf(t107,plain,
meet(X1,complement(X1)) = zero,
inference(orient,[status(thm)],[t5]) ).
cnf(t459128,plain,
zero = complement(top),
inference(step,[status(thm)],[t101,t107]) ).
cnf(t112,plain,
complement(top) = zero,
inference(orient,[status(thm)],[t459128]) ).
cnf(t459298,plain,
complement(one) = join(complement(one),composition(top,zero)),
inference(step,[status(thm)],[t2522,t112]) ).
cnf(t2542,plain,
join(complement(one),composition(top,zero)) = complement(one),
inference(orient,[status(thm)],[t459298]) ).
cnf(t5102,plain,
top = join(complement(composition(top,zero)),complement(one)),
inference(cp,[status(thm)],[t5089,t2542]) ).
cnf(t459436,plain,
top = join(complement(one),complement(composition(top,zero))),
inference(step,[status(thm)],[t5102,t54]) ).
cnf(t5164,plain,
join(complement(one),complement(composition(top,zero))) = top,
inference(orient,[status(thm)],[t459436]) ).
cnf(t5166,plain,
meet(one,composition(top,zero)) = complement(top),
inference(cp,[status(thm)],[t100,t5164]) ).
cnf(t459437,plain,
meet(one,composition(top,zero)) = zero,
inference(step,[status(thm)],[t5166,t112]) ).
cnf(t5171,plain,
meet(one,composition(top,zero)) = zero,
inference(orient,[status(thm)],[t459437]) ).
cnf(t5176,plain,
composition(meet(one,composition(top,zero)),meet(one,composition(converse(one),composition(top,zero)))) = join(zero,composition(meet(one,composition(top,zero)),meet(one,composition(converse(one),composition(top,zero))))),
inference(cp,[status(thm)],[t3618,t5171]) ).
cnf(t459438,plain,
composition(zero,meet(one,composition(converse(one),composition(top,zero)))) = join(zero,composition(meet(one,composition(top,zero)),meet(one,composition(converse(one),composition(top,zero))))),
inference(step,[status(thm)],[t5176,t5171]) ).
cnf(t459439,plain,
composition(zero,meet(one,composition(one,composition(top,zero)))) = join(zero,composition(meet(one,composition(top,zero)),meet(one,composition(converse(one),composition(top,zero))))),
inference(step,[status(thm)],[t459438,t199]) ).
cnf(t459440,plain,
composition(zero,meet(one,composition(top,zero))) = join(zero,composition(meet(one,composition(top,zero)),meet(one,composition(converse(one),composition(top,zero))))),
inference(step,[status(thm)],[t459439,t210]) ).
cnf(t459441,plain,
composition(zero,zero) = join(zero,composition(meet(one,composition(top,zero)),meet(one,composition(converse(one),composition(top,zero))))),
inference(step,[status(thm)],[t459440,t5171]) ).
cnf(t459442,plain,
composition(zero,zero) = join(zero,composition(zero,meet(one,composition(converse(one),composition(top,zero))))),
inference(step,[status(thm)],[t459441,t5171]) ).
cnf(t459443,plain,
composition(zero,zero) = join(zero,composition(zero,meet(one,composition(one,composition(top,zero))))),
inference(step,[status(thm)],[t459442,t199]) ).
cnf(t459444,plain,
composition(zero,zero) = join(zero,composition(zero,meet(one,composition(top,zero)))),
inference(step,[status(thm)],[t459443,t210]) ).
cnf(t459445,plain,
composition(zero,zero) = join(zero,composition(zero,zero)),
inference(step,[status(thm)],[t459444,t5171]) ).
cnf(t31,plain,
composition(join(converse(X1),X2),converse(X3)) = join(converse(composition(X3,X1)),composition(X2,converse(X3))),
inference(cp,[status(thm)],[t25,t28]) ).
cnf(t1276,plain,
join(converse(composition(X1,X2)),composition(X3,converse(X1))) = composition(join(converse(X2),X3),converse(X1)),
inference(orient,[status(thm)],[t31]) ).
cnf(t448,plain,
converse(composition(X1,top)) = composition(top,converse(X1)),
inference(cp,[status(thm)],[t28,t443]) ).
cnf(t455,plain,
converse(composition(X1,top)) = composition(top,converse(X1)),
inference(orient,[status(thm)],[t448]) ).
fof(f16,conjecture,
! [X0,X1] :
( ( composition(X1,top) = X1
& composition(X0,top) = X0 )
=> composition(meet(X0,X1),top) = meet(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',goals) ).
fof(f16_neg,negated_conjecture,
~ ! [X0,X1] :
( ( composition(X1,top) = X1
& composition(X0,top) = X0 )
=> composition(meet(X0,X1),top) = meet(X0,X1) ),
inference(negated_conjecture,[status(cth)],[f16]) ).
fof(f16_nnf,plain,
? [X0,X1] :
( composition(meet(X0,X1),top) != meet(X0,X1)
& composition(X1,top) = X1
& composition(X0,top) = X0 ),
inference(nnf_transformation,[status(thm)],[f16_neg]) ).
fof(f16_sk,plain,
( composition(meet(sk0,sk1),top) != meet(sk0,sk1)
& composition(sk1,top) = sk1
& composition(sk0,top) = sk0 ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk0,sk1])],[f16_nnf]) ).
cnf(c17,plain,
composition(sk1,top) = sk1,
inference(cnf_transformation,[status(esa)],[f16_sk]) ).
cnf(t2,plain,
composition(sk1,top) = sk1,
inference(equality_encoding,[status(esa)],[c17]) ).
cnf(t49,plain,
composition(sk1,top) = sk1,
inference(orient,[status(thm)],[t2]) ).
cnf(t50,plain,
composition(join(sk1,X1),top) = join(sk1,composition(X1,top)),
inference(cp,[status(thm)],[t25,t49]) ).
cnf(t374,plain,
composition(join(sk1,X1),top) = join(sk1,composition(X1,top)),
inference(orient,[status(thm)],[t50]) ).
cnf(t456,plain,
composition(top,converse(join(sk1,X1))) = converse(join(sk1,composition(X1,top))),
inference(cp,[status(thm)],[t455,t374]) ).
cnf(t1429,plain,
converse(join(sk1,composition(X1,top))) = composition(top,converse(join(sk1,X1))),
inference(orient,[status(thm)],[t456]) ).
cnf(t1432,plain,
composition(top,converse(join(sk1,one))) = converse(join(sk1,top)),
inference(cp,[status(thm)],[t1429,t210]) ).
cnf(t201,plain,
converse(join(X1,one)) = join(converse(X1),one),
inference(cp,[status(thm)],[t73,t199]) ).
cnf(t459134,plain,
converse(join(X1,one)) = join(one,converse(X1)),
inference(step,[status(thm)],[t201,t54]) ).
cnf(t227,plain,
converse(join(X1,one)) = join(one,converse(X1)),
inference(orient,[status(thm)],[t459134]) ).
cnf(t459214,plain,
composition(top,join(one,converse(sk1))) = converse(join(sk1,top)),
inference(step,[status(thm)],[t1432,t227]) ).
cnf(t459215,plain,
composition(top,join(one,converse(sk1))) = converse(top),
inference(step,[status(thm)],[t459214,t427]) ).
cnf(t459216,plain,
composition(top,join(one,converse(sk1))) = top,
inference(step,[status(thm)],[t459215,t443]) ).
cnf(t1453,plain,
composition(top,join(one,converse(sk1))) = top,
inference(orient,[status(thm)],[t459216]) ).
cnf(t1457,plain,
composition(join(converse(join(one,converse(sk1))),X1),converse(top)) = join(converse(top),composition(X1,converse(top))),
inference(cp,[status(thm)],[t1276,t1453]) ).
cnf(t200,plain,
converse(join(one,X1)) = join(one,converse(X1)),
inference(cp,[status(thm)],[t73,t199]) ).
cnf(t216,plain,
converse(join(one,X1)) = join(one,converse(X1)),
inference(orient,[status(thm)],[t200]) ).
cnf(t459219,plain,
composition(join(join(one,converse(converse(sk1))),X1),converse(top)) = join(converse(top),composition(X1,converse(top))),
inference(step,[status(thm)],[t1457,t216]) ).
cnf(t459220,plain,
composition(join(one,join(converse(converse(sk1)),X1)),converse(top)) = join(converse(top),composition(X1,converse(top))),
inference(step,[status(thm)],[t459219,t57]) ).
cnf(t459221,plain,
composition(join(one,join(sk1,X1)),converse(top)) = join(converse(top),composition(X1,converse(top))),
inference(step,[status(thm)],[t459220,t22]) ).
cnf(t459222,plain,
composition(join(one,join(sk1,X1)),top) = join(converse(top),composition(X1,converse(top))),
inference(step,[status(thm)],[t459221,t443]) ).
cnf(t459223,plain,
composition(join(one,join(sk1,X1)),top) = join(top,composition(X1,converse(top))),
inference(step,[status(thm)],[t459222,t443]) ).
cnf(t459224,plain,
composition(join(one,join(sk1,X1)),top) = top,
inference(step,[status(thm)],[t459223,t435]) ).
cnf(t1484,plain,
composition(join(one,join(sk1,X1)),top) = top,
inference(orient,[status(thm)],[t459224]) ).
cnf(t525,plain,
join(one,converse(join(X1,complement(one)))) = converse(top),
inference(cp,[status(thm)],[t216,t517]) ).
cnf(t459157,plain,
join(one,converse(join(X1,complement(one)))) = top,
inference(step,[status(thm)],[t525,t443]) ).
cnf(t528,plain,
join(one,converse(join(X1,complement(one)))) = top,
inference(orient,[status(thm)],[t459157]) ).
cnf(t529,plain,
top = join(one,join(X1,converse(complement(one)))),
inference(cp,[status(thm)],[t528,t285]) ).
cnf(t533,plain,
join(one,join(X1,converse(complement(one)))) = top,
inference(orient,[status(thm)],[t529]) ).
cnf(t1485,plain,
top = composition(top,top),
inference(cp,[status(thm)],[t1484,t533]) ).
cnf(t1523,plain,
composition(top,top) = top,
inference(orient,[status(thm)],[t1485]) ).
cnf(t1531,plain,
complement(top) = join(complement(top),composition(converse(top),complement(top))),
inference(cp,[status(thm)],[t65,t1523]) ).
cnf(t459229,plain,
zero = join(complement(top),composition(converse(top),complement(top))),
inference(step,[status(thm)],[t1531,t112]) ).
cnf(t459230,plain,
zero = join(zero,composition(converse(top),complement(top))),
inference(step,[status(thm)],[t459229,t112]) ).
cnf(t459231,plain,
zero = join(zero,composition(top,complement(top))),
inference(step,[status(thm)],[t459230,t443]) ).
cnf(t459232,plain,
zero = join(zero,composition(top,zero)),
inference(step,[status(thm)],[t459231,t112]) ).
cnf(t1533,plain,
join(zero,composition(top,zero)) = zero,
inference(orient,[status(thm)],[t459232]) ).
cnf(t1536,plain,
join(zero,join(composition(top,zero),X1)) = join(zero,X1),
inference(cp,[status(thm)],[t57,t1533]) ).
cnf(t1583,plain,
join(zero,join(composition(top,zero),X1)) = join(zero,X1),
inference(orient,[status(thm)],[t1536]) ).
cnf(t1585,plain,
join(zero,composition(X1,zero)) = join(zero,composition(join(top,X1),zero)),
inference(cp,[status(thm)],[t1583,t25]) ).
cnf(t459235,plain,
join(zero,composition(X1,zero)) = join(zero,composition(top,zero)),
inference(step,[status(thm)],[t1585,t435]) ).
cnf(t459236,plain,
join(zero,composition(X1,zero)) = zero,
inference(step,[status(thm)],[t459235,t1533]) ).
cnf(t1604,plain,
join(zero,composition(X1,zero)) = zero,
inference(orient,[status(thm)],[t459236]) ).
cnf(t459446,plain,
composition(zero,zero) = zero,
inference(step,[status(thm)],[t459445,t1604]) ).
cnf(t5178,plain,
composition(zero,zero) = zero,
inference(orient,[status(thm)],[t459446]) ).
cnf(t5180,plain,
composition(join(zero,X1),zero) = join(zero,composition(X1,zero)),
inference(cp,[status(thm)],[t25,t5178]) ).
cnf(t459447,plain,
composition(join(zero,X1),zero) = zero,
inference(step,[status(thm)],[t5180,t1604]) ).
cnf(t5194,plain,
composition(join(zero,X1),zero) = zero,
inference(orient,[status(thm)],[t459447]) ).
cnf(t243,plain,
complement(top) = join(zero,complement(top)),
inference(cp,[status(thm)],[t239,t112]) ).
cnf(t459137,plain,
zero = join(zero,complement(top)),
inference(step,[status(thm)],[t243,t112]) ).
cnf(t459138,plain,
zero = join(zero,zero),
inference(step,[status(thm)],[t459137,t112]) ).
cnf(t250,plain,
join(zero,zero) = zero,
inference(orient,[status(thm)],[t459138]) ).
cnf(t251,plain,
join(zero,join(zero,X1)) = join(zero,X1),
inference(cp,[status(thm)],[t57,t250]) ).
cnf(t269,plain,
join(zero,join(zero,X1)) = join(zero,X1),
inference(orient,[status(thm)],[t251]) ).
cnf(t271,plain,
join(zero,X1) = join(zero,join(X1,zero)),
inference(cp,[status(thm)],[t269,t54]) ).
cnf(t272,plain,
join(zero,join(X1,zero)) = join(zero,X1),
inference(orient,[status(thm)],[t271]) ).
cnf(t275,plain,
join(zero,join(join(X1,zero),X2)) = join(join(zero,X1),X2),
inference(cp,[status(thm)],[t57,t272]) ).
cnf(t459349,plain,
join(zero,join(X1,join(zero,X2))) = join(join(zero,X1),X2),
inference(step,[status(thm)],[t275,t57]) ).
cnf(t459350,plain,
join(zero,join(X1,join(zero,X2))) = join(zero,join(X1,X2)),
inference(step,[status(thm)],[t459349,t57]) ).
cnf(t2986,plain,
join(zero,join(X1,join(zero,X2))) = join(zero,join(X1,X2)),
inference(orient,[status(thm)],[t459350]) ).
cnf(t63,plain,
top = join(X1,join(X2,complement(join(X1,X2)))),
inference(cp,[status(thm)],[t62,t57]) ).
cnf(t777,plain,
join(X1,join(X2,complement(join(X1,X2)))) = top,
inference(orient,[status(thm)],[t63]) ).
cnf(t803,plain,
top = join(X1,join(X2,complement(join(X2,X1)))),
inference(cp,[status(thm)],[t777,t54]) ).
cnf(t935,plain,
join(X1,join(X2,complement(join(X2,X1)))) = top,
inference(orient,[status(thm)],[t803]) ).
cnf(t535,plain,
top = join(one,join(converse(complement(one)),X1)),
inference(cp,[status(thm)],[t533,t54]) ).
cnf(t540,plain,
join(one,join(converse(complement(one)),X1)) = top,
inference(orient,[status(thm)],[t535]) ).
cnf(t965,plain,
top = join(join(converse(complement(one)),X1),join(one,complement(top))),
inference(cp,[status(thm)],[t935,t540]) ).
cnf(t459400,plain,
top = join(converse(complement(one)),join(X1,join(one,complement(top)))),
inference(step,[status(thm)],[t965,t57]) ).
cnf(t459401,plain,
top = join(converse(complement(one)),join(X1,join(one,zero))),
inference(step,[status(thm)],[t459400,t112]) ).
cnf(t459402,plain,
top = join(converse(complement(one)),join(X1,join(zero,one))),
inference(step,[status(thm)],[t459401,t54]) ).
cnf(t4239,plain,
join(converse(complement(one)),join(X1,join(zero,one))) = top,
inference(orient,[status(thm)],[t459402]) ).
cnf(t4242,plain,
top = join(converse(complement(one)),join(join(zero,one),X1)),
inference(cp,[status(thm)],[t4239,t54]) ).
cnf(t459418,plain,
top = join(converse(complement(one)),join(zero,join(one,X1))),
inference(step,[status(thm)],[t4242,t57]) ).
cnf(t4787,plain,
join(converse(complement(one)),join(zero,join(one,X1))) = top,
inference(orient,[status(thm)],[t459418]) ).
cnf(t4791,plain,
join(zero,join(converse(complement(one)),join(one,X1))) = join(zero,top),
inference(cp,[status(thm)],[t2986,t4787]) ).
cnf(t114,plain,
top = join(top,zero),
inference(cp,[status(thm)],[t62,t112]) ).
cnf(t459129,plain,
top = join(zero,top),
inference(step,[status(thm)],[t114,t54]) ).
cnf(t119,plain,
join(zero,top) = top,
inference(orient,[status(thm)],[t459129]) ).
cnf(t459423,plain,
join(zero,join(converse(complement(one)),join(one,X1))) = top,
inference(step,[status(thm)],[t4791,t119]) ).
cnf(t4873,plain,
join(zero,join(converse(complement(one)),join(one,X1))) = top,
inference(orient,[status(thm)],[t459423]) ).
cnf(t5195,plain,
zero = composition(top,zero),
inference(cp,[status(thm)],[t5194,t4873]) ).
cnf(t5234,plain,
composition(top,zero) = zero,
inference(orient,[status(thm)],[t5195]) ).
cnf(t5246,plain,
complement(zero) = join(complement(zero),composition(converse(top),complement(zero))),
inference(cp,[status(thm)],[t65,t5234]) ).
cnf(t459488,plain,
complement(zero) = join(complement(zero),composition(top,complement(zero))),
inference(step,[status(thm)],[t5246,t443]) ).
cnf(t6205,plain,
join(complement(zero),composition(top,complement(zero))) = complement(zero),
inference(orient,[status(thm)],[t459488]) ).
cnf(t76,plain,
converse(join(X1,converse(X2))) = join(converse(X1),X2),
inference(cp,[status(thm)],[t73,t22]) ).
cnf(t302,plain,
converse(join(X1,converse(X2))) = join(converse(X1),X2),
inference(orient,[status(thm)],[t76]) ).
cnf(t467,plain,
join(converse(X1),composition(X2,top)) = converse(join(X1,composition(top,converse(X2)))),
inference(cp,[status(thm)],[t302,t455]) ).
cnf(t10588,plain,
converse(join(X1,composition(top,converse(X2)))) = join(converse(X1),composition(X2,top)),
inference(orient,[status(thm)],[t467]) ).
cnf(t10590,plain,
join(converse(converse(composition(X1,X2))),composition(X1,top)) = converse(composition(join(converse(X2),top),converse(X1))),
inference(cp,[status(thm)],[t10588,t1276]) ).
cnf(t459616,plain,
join(composition(X1,X2),composition(X1,top)) = converse(composition(join(converse(X2),top),converse(X1))),
inference(step,[status(thm)],[t10590,t22]) ).
cnf(t29,plain,
converse(composition(X1,converse(X2))) = composition(X2,converse(X1)),
inference(cp,[status(thm)],[t28,t22]) ).
cnf(t166,plain,
converse(composition(X1,converse(X2))) = composition(X2,converse(X1)),
inference(orient,[status(thm)],[t29]) ).
cnf(t459617,plain,
join(composition(X1,X2),composition(X1,top)) = composition(X1,converse(join(converse(X2),top))),
inference(step,[status(thm)],[t459616,t166]) ).
cnf(t459618,plain,
join(composition(X1,X2),composition(X1,top)) = composition(X1,join(X2,converse(top))),
inference(step,[status(thm)],[t459617,t285]) ).
cnf(t459619,plain,
join(composition(X1,X2),composition(X1,top)) = composition(X1,join(X2,top)),
inference(step,[status(thm)],[t459618,t443]) ).
cnf(t459620,plain,
join(composition(X1,X2),composition(X1,top)) = composition(X1,top),
inference(step,[status(thm)],[t459619,t427]) ).
cnf(t10668,plain,
join(composition(X1,X2),composition(X1,top)) = composition(X1,top),
inference(orient,[status(thm)],[t459620]) ).
cnf(t10672,plain,
composition(X1,top) = join(X1,composition(X1,top)),
inference(cp,[status(thm)],[t10668,t18]) ).
cnf(t10781,plain,
join(X1,composition(X1,top)) = composition(X1,top),
inference(orient,[status(thm)],[t10672]) ).
cnf(t10815,plain,
join(X1,converse(composition(converse(X1),top))) = converse(composition(converse(X1),top)),
inference(cp,[status(thm)],[t285,t10781]) ).
cnf(t459624,plain,
join(X1,composition(converse(top),X1)) = converse(composition(converse(X1),top)),
inference(step,[status(thm)],[t10815,t176]) ).
cnf(t459625,plain,
join(X1,composition(top,X1)) = converse(composition(converse(X1),top)),
inference(step,[status(thm)],[t459624,t443]) ).
cnf(t459626,plain,
join(X1,composition(top,X1)) = composition(converse(top),X1),
inference(step,[status(thm)],[t459625,t176]) ).
cnf(t459627,plain,
join(X1,composition(top,X1)) = composition(top,X1),
inference(step,[status(thm)],[t459626,t443]) ).
cnf(t10876,plain,
join(X1,composition(top,X1)) = composition(top,X1),
inference(orient,[status(thm)],[t459627]) ).
cnf(t459628,plain,
composition(top,complement(zero)) = complement(zero),
inference(step,[status(thm)],[t6205,t10876]) ).
cnf(t10925,plain,
composition(top,complement(zero)) = complement(zero),
inference(rw,[status(thm)],[t459628]) ).
cnf(t10926,plain,
composition(top,complement(zero)) = complement(zero),
inference(orient,[status(thm)],[t10925]) ).
cnf(t10932,plain,
composition(top,composition(complement(zero),X1)) = composition(complement(zero),X1),
inference(cp,[status(thm)],[t23,t10926]) ).
cnf(t11923,plain,
composition(top,composition(complement(zero),X1)) = composition(complement(zero),X1),
inference(orient,[status(thm)],[t10932]) ).
cnf(t11937,plain,
complement(composition(complement(zero),X1)) = join(complement(composition(complement(zero),X1)),composition(converse(top),complement(composition(complement(zero),X1)))),
inference(cp,[status(thm)],[t65,t11923]) ).
cnf(t459781,plain,
complement(composition(complement(zero),X1)) = join(complement(composition(complement(zero),X1)),composition(top,complement(composition(complement(zero),X1)))),
inference(step,[status(thm)],[t11937,t443]) ).
cnf(t459782,plain,
complement(composition(complement(zero),X1)) = composition(top,complement(composition(complement(zero),X1))),
inference(step,[status(thm)],[t459781,t10876]) ).
cnf(t17479,plain,
composition(top,complement(composition(complement(zero),X1))) = complement(composition(complement(zero),X1)),
inference(orient,[status(thm)],[t459782]) ).
fof(f2,axiom,
! [X0,X1] : X0 = join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))),
file('/export/starexec/sandbox/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(t14,plain,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
inference(equality_encoding,[status(esa)],[c2]) ).
cnf(t19,plain,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
inference(orient,[status(thm)],[t14]) ).
cnf(t56,plain,
join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) = X1,
inference(rw,[status(thm)],[t19]) ).
cnf(t459830,plain,
join(complement(join(complement(X1),X2)),complement(join(complement(X1),complement(X2)))) = X1,
inference(step,[status(thm)],[t56,t54]) ).
cnf(t459831,plain,
join(complement(join(complement(X1),X2)),meet(X1,X2)) = X1,
inference(step,[status(thm)],[t459830,t100]) ).
cnf(t459832,plain,
join(meet(X1,X2),complement(join(complement(X1),X2))) = X1,
inference(step,[status(thm)],[t459831,t54]) ).
cnf(t20475,plain,
join(meet(X1,X2),complement(join(complement(X1),X2))) = X1,
inference(orient,[status(thm)],[t459832]) ).
cnf(t20476,plain,
X1 = join(zero,complement(join(complement(X1),complement(X1)))),
inference(cp,[status(thm)],[t20475,t107]) ).
cnf(t459833,plain,
X1 = join(zero,meet(X1,X1)),
inference(step,[status(thm)],[t20476,t100]) ).
cnf(t20680,plain,
join(zero,meet(X1,X1)) = X1,
inference(orient,[status(thm)],[t459833]) ).
cnf(t20690,plain,
join(zero,meet(X1,X1)) = join(zero,X1),
inference(cp,[status(thm)],[t269,t20680]) ).
cnf(t459861,plain,
X1 = join(zero,X1),
inference(step,[status(thm)],[t20690,t20680]) ).
cnf(t20807,plain,
join(zero,X1) = X1,
inference(orient,[status(thm)],[t459861]) ).
cnf(t459150,plain,
join(X1,join(complement(X1),X2)) = top,
inference(step,[status(thm)],[t395,t435]) ).
cnf(t436,plain,
join(X1,join(complement(X1),X2)) = top,
inference(orient,[status(thm)],[t459150]) ).
cnf(t10899,plain,
top = join(X1,composition(top,complement(X1))),
inference(cp,[status(thm)],[t436,t10876]) ).
cnf(t11107,plain,
join(X1,composition(top,complement(X1))) = top,
inference(orient,[status(thm)],[t10899]) ).
cnf(t20829,plain,
composition(top,complement(zero)) = top,
inference(cp,[status(thm)],[t20807,t11107]) ).
cnf(t459903,plain,
complement(zero) = top,
inference(step,[status(thm)],[t20829,t10926]) ).
cnf(t20947,plain,
complement(zero) = top,
inference(orient,[status(thm)],[t459903]) ).
cnf(t459907,plain,
composition(top,complement(composition(top,X1))) = complement(composition(complement(zero),X1)),
inference(step,[status(thm)],[t17479,t20947]) ).
cnf(t459908,plain,
composition(top,complement(composition(top,X1))) = complement(composition(top,X1)),
inference(step,[status(thm)],[t459907,t20947]) ).
cnf(t20975,plain,
composition(top,complement(composition(top,X1))) = complement(composition(top,X1)),
inference(rw,[status(thm)],[t459908]) ).
cnf(t25011,plain,
composition(top,complement(composition(top,X1))) = complement(composition(top,X1)),
inference(orient,[status(thm)],[t20975]) ).
cnf(t25023,plain,
composition(converse(complement(composition(top,X1))),top) = converse(complement(composition(top,X1))),
inference(cp,[status(thm)],[t493,t25011]) ).
cnf(t66544,plain,
composition(converse(complement(composition(top,X1))),top) = converse(complement(composition(top,X1))),
inference(orient,[status(thm)],[t25023]) ).
cnf(t240,plain,
complement(join(complement(X1),complement(X2))) = join(meet(X1,X2),complement(join(complement(X1),complement(X2)))),
inference(cp,[status(thm)],[t239,t100]) ).
cnf(t459172,plain,
meet(X1,X2) = join(meet(X1,X2),complement(join(complement(X1),complement(X2)))),
inference(step,[status(thm)],[t240,t100]) ).
cnf(t459173,plain,
meet(X1,X2) = join(meet(X1,X2),meet(X1,X2)),
inference(step,[status(thm)],[t459172,t100]) ).
cnf(t671,plain,
join(meet(X1,X2),meet(X1,X2)) = meet(X1,X2),
inference(orient,[status(thm)],[t459173]) ).
cnf(t672,plain,
meet(X1,X2) = join(meet(X2,X1),meet(X1,X2)),
inference(cp,[status(thm)],[t671,t121]) ).
cnf(t751,plain,
join(meet(X1,X2),meet(X2,X1)) = meet(X2,X1),
inference(orient,[status(thm)],[t672]) ).
cnf(t459870,plain,
meet(X1,X1) = X1,
inference(step,[status(thm)],[t20680,t20807]) ).
cnf(t20918,plain,
meet(X1,X1) = X1,
inference(rw,[status(thm)],[t459870]) ).
cnf(t21009,plain,
meet(X1,X1) = X1,
inference(orient,[status(thm)],[t20918]) ).
cnf(t21010,plain,
meet(X1,X1) = join(X1,meet(X1,X1)),
inference(cp,[status(thm)],[t751,t21009]) ).
cnf(t459934,plain,
X1 = join(X1,meet(X1,X1)),
inference(step,[status(thm)],[t21010,t21009]) ).
cnf(t459935,plain,
X1 = join(X1,X1),
inference(step,[status(thm)],[t459934,t21009]) ).
cnf(t21071,plain,
join(X1,X1) = X1,
inference(orient,[status(thm)],[t459935]) ).
cnf(t21075,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(cp,[status(thm)],[t57,t21071]) ).
cnf(t21504,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(orient,[status(thm)],[t21075]) ).
cnf(t21528,plain,
join(meet(X1,X2),complement(join(complement(X1),X2))) = join(meet(X1,X2),X1),
inference(cp,[status(thm)],[t21504,t20475]) ).
cnf(t459990,plain,
X1 = join(meet(X1,X2),X1),
inference(step,[status(thm)],[t21528,t20475]) ).
cnf(t459991,plain,
X1 = join(X1,meet(X1,X2)),
inference(step,[status(thm)],[t459990,t54]) ).
cnf(t21540,plain,
join(X1,meet(X1,X2)) = X1,
inference(orient,[status(thm)],[t459991]) ).
cnf(t21542,plain,
X1 = join(X1,meet(X2,X1)),
inference(cp,[status(thm)],[t21540,t121]) ).
cnf(t21581,plain,
join(X1,meet(X2,X1)) = X1,
inference(orient,[status(thm)],[t21542]) ).
cnf(t21590,plain,
join(X1,join(meet(X2,X1),X3)) = join(X1,X3),
inference(cp,[status(thm)],[t57,t21581]) ).
cnf(t29994,plain,
join(X1,join(meet(X2,X1),X3)) = join(X1,X3),
inference(orient,[status(thm)],[t21590]) ).
cnf(t266,plain,
meet(X1,complement(X2)) = complement(join(complement(X1),meet(X2,X2))),
inference(cp,[status(thm)],[t100,t256]) ).
cnf(t2431,plain,
complement(join(complement(X1),meet(X2,X2))) = meet(X1,complement(X2)),
inference(orient,[status(thm)],[t266]) ).
cnf(t459921,plain,
complement(join(complement(X1),X2)) = meet(X1,complement(X2)),
inference(step,[status(thm)],[t2431,t21009]) ).
cnf(t21048,plain,
complement(join(complement(X1),X2)) = meet(X1,complement(X2)),
inference(rw,[status(thm)],[t459921]) ).
cnf(t22025,plain,
complement(join(complement(X1),X2)) = meet(X1,complement(X2)),
inference(orient,[status(thm)],[t21048]) ).
cnf(t460026,plain,
join(meet(X1,X2),meet(X1,complement(X2))) = X1,
inference(step,[status(thm)],[t20475,t22025]) ).
cnf(t22150,plain,
join(meet(X1,X2),meet(X1,complement(X2))) = X1,
inference(rw,[status(thm)],[t460026]) ).
cnf(t36043,plain,
join(meet(X1,X2),meet(X1,complement(X2))) = X1,
inference(orient,[status(thm)],[t22150]) ).
cnf(t36116,plain,
join(X1,meet(X2,complement(X1))) = join(X1,X2),
inference(cp,[status(thm)],[t29994,t36043]) ).
cnf(t36275,plain,
join(X1,meet(X2,complement(X1))) = join(X1,X2),
inference(orient,[status(thm)],[t36116]) ).
cnf(t36292,plain,
join(X1,X2) = join(X1,meet(complement(X1),X2)),
inference(cp,[status(thm)],[t36275,t121]) ).
cnf(t36815,plain,
join(X1,meet(complement(X1),X2)) = join(X1,X2),
inference(orient,[status(thm)],[t36292]) ).
cnf(t459914,plain,
X1 = complement(complement(X1)),
inference(step,[status(thm)],[t256,t21009]) ).
cnf(t21041,plain,
X1 = complement(complement(X1)),
inference(rw,[status(thm)],[t459914]) ).
cnf(t21120,plain,
complement(complement(X1)) = X1,
inference(orient,[status(thm)],[t21041]) ).
cnf(t36839,plain,
join(complement(X1),X2) = join(complement(X1),meet(X1,X2)),
inference(cp,[status(thm)],[t36815,t21120]) ).
cnf(t38324,plain,
join(complement(X1),meet(X1,X2)) = join(complement(X1),X2),
inference(orient,[status(thm)],[t36839]) ).
cnf(t40,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)],[t34,t22]) ).
cnf(t459601,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)],[t40,t22]) ).
cnf(t9273,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)],[t459601]) ).
cnf(t2527,plain,
complement(one) = join(complement(one),composition(X1,complement(converse(X1)))),
inference(cp,[status(thm)],[t2515,t22]) ).
cnf(t2732,plain,
join(complement(one),composition(X1,complement(converse(X1)))) = complement(one),
inference(orient,[status(thm)],[t2527]) ).
cnf(t5100,plain,
top = join(complement(composition(X1,complement(converse(X1)))),complement(one)),
inference(cp,[status(thm)],[t5089,t2732]) ).
cnf(t459544,plain,
top = join(complement(one),complement(composition(X1,complement(converse(X1))))),
inference(step,[status(thm)],[t5100,t54]) ).
cnf(t8225,plain,
join(complement(one),complement(composition(X1,complement(converse(X1))))) = top,
inference(orient,[status(thm)],[t459544]) ).
cnf(t8244,plain,
meet(one,composition(X1,complement(converse(X1)))) = complement(top),
inference(cp,[status(thm)],[t100,t8225]) ).
cnf(t459545,plain,
meet(one,composition(X1,complement(converse(X1)))) = zero,
inference(step,[status(thm)],[t8244,t112]) ).
cnf(t8249,plain,
meet(one,composition(X1,complement(converse(X1)))) = zero,
inference(orient,[status(thm)],[t459545]) ).
cnf(t8263,plain,
zero = meet(one,composition(converse(X1),complement(X1))),
inference(cp,[status(thm)],[t8249,t22]) ).
cnf(t8274,plain,
meet(one,composition(converse(X1),complement(X1))) = zero,
inference(orient,[status(thm)],[t8263]) ).
cnf(t8299,plain,
zero = meet(one,composition(converse(complement(X1)),meet(X1,X1))),
inference(cp,[status(thm)],[t8274,t256]) ).
cnf(t9246,plain,
meet(one,composition(converse(complement(X1)),meet(X1,X1))) = zero,
inference(orient,[status(thm)],[t8299]) ).
cnf(t459925,plain,
meet(one,composition(converse(complement(X1)),X1)) = zero,
inference(step,[status(thm)],[t9246,t21009]) ).
cnf(t21052,plain,
meet(one,composition(converse(complement(X1)),X1)) = zero,
inference(rw,[status(thm)],[t459925]) ).
cnf(t23476,plain,
meet(one,composition(converse(complement(X1)),X1)) = zero,
inference(orient,[status(thm)],[t21052]) ).
cnf(t23491,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)],[t9273,t23476]) ).
cnf(t460043,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)],[t23491,t23476]) ).
cnf(t5238,plain,
composition(converse(zero),top) = converse(zero),
inference(cp,[status(thm)],[t493,t5234]) ).
cnf(t5262,plain,
composition(converse(zero),top) = converse(zero),
inference(orient,[status(thm)],[t5238]) ).
cnf(t10714,plain,
composition(converse(zero),top) = join(composition(converse(zero),X1),converse(zero)),
inference(cp,[status(thm)],[t10668,t5262]) ).
cnf(t459669,plain,
converse(zero) = join(composition(converse(zero),X1),converse(zero)),
inference(step,[status(thm)],[t10714,t5262]) ).
cnf(t459670,plain,
converse(zero) = join(converse(zero),composition(converse(zero),X1)),
inference(step,[status(thm)],[t459669,t54]) ).
cnf(t12337,plain,
join(converse(zero),composition(converse(zero),X1)) = converse(zero),
inference(orient,[status(thm)],[t459670]) ).
cnf(t459154,plain,
join(X1,converse(complement(converse(X1)))) = top,
inference(step,[status(thm)],[t321,t443]) ).
cnf(t446,plain,
join(X1,converse(complement(converse(X1)))) = top,
inference(orient,[status(thm)],[t459154]) ).
cnf(t20838,plain,
converse(complement(converse(zero))) = top,
inference(cp,[status(thm)],[t20807,t446]) ).
cnf(t21207,plain,
converse(complement(converse(zero))) = top,
inference(orient,[status(thm)],[t20838]) ).
cnf(t21208,plain,
complement(converse(zero)) = converse(top),
inference(cp,[status(thm)],[t22,t21207]) ).
cnf(t459955,plain,
complement(converse(zero)) = top,
inference(step,[status(thm)],[t21208,t443]) ).
cnf(t21269,plain,
complement(converse(zero)) = top,
inference(orient,[status(thm)],[t459955]) ).
cnf(t21270,plain,
converse(zero) = complement(top),
inference(cp,[status(thm)],[t21120,t21269]) ).
cnf(t459956,plain,
converse(zero) = zero,
inference(step,[status(thm)],[t21270,t112]) ).
cnf(t21285,plain,
converse(zero) = zero,
inference(orient,[status(thm)],[t459956]) ).
cnf(t459965,plain,
join(zero,composition(converse(zero),X1)) = converse(zero),
inference(step,[status(thm)],[t12337,t21285]) ).
cnf(t459966,plain,
composition(converse(zero),X1) = converse(zero),
inference(step,[status(thm)],[t459965,t20807]) ).
cnf(t459967,plain,
composition(zero,X1) = converse(zero),
inference(step,[status(thm)],[t459966,t21285]) ).
cnf(t459968,plain,
composition(zero,X1) = zero,
inference(step,[status(thm)],[t459967,t21285]) ).
cnf(t21321,plain,
composition(zero,X1) = zero,
inference(rw,[status(thm)],[t459968]) ).
cnf(t21337,plain,
composition(zero,X1) = zero,
inference(orient,[status(thm)],[t21321]) ).
cnf(t460044,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)],[t460043,t21337]) ).
cnf(t460045,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)],[t460044,t121]) ).
cnf(t460046,plain,
zero = join(meet(converse(complement(X1)),converse(X1)),composition(zero,meet(converse(X1),composition(converse(one),converse(complement(X1)))))),
inference(step,[status(thm)],[t460045,t210]) ).
cnf(t460047,plain,
zero = join(meet(converse(X1),converse(complement(X1))),composition(zero,meet(converse(X1),composition(converse(one),converse(complement(X1)))))),
inference(step,[status(thm)],[t460046,t121]) ).
cnf(t460048,plain,
zero = join(meet(converse(X1),converse(complement(X1))),zero),
inference(step,[status(thm)],[t460047,t21337]) ).
cnf(t10883,plain,
join(X1,join(composition(top,X1),X2)) = join(composition(top,X1),X2),
inference(cp,[status(thm)],[t57,t10876]) ).
cnf(t16151,plain,
join(X1,join(composition(top,X1),X2)) = join(composition(top,X1),X2),
inference(orient,[status(thm)],[t10883]) ).
cnf(t16201,plain,
join(composition(top,X1),X2) = join(X1,join(X2,composition(top,X1))),
inference(cp,[status(thm)],[t16151,t54]) ).
cnf(t18821,plain,
join(X1,join(X2,composition(top,X1))) = join(composition(top,X1),X2),
inference(orient,[status(thm)],[t16201]) ).
cnf(t20827,plain,
join(X1,composition(top,zero)) = join(composition(top,zero),X1),
inference(cp,[status(thm)],[t20807,t18821]) ).
cnf(t459910,plain,
join(X1,zero) = join(composition(top,zero),X1),
inference(step,[status(thm)],[t20827,t5234]) ).
cnf(t459911,plain,
join(X1,zero) = join(zero,X1),
inference(step,[status(thm)],[t459910,t5234]) ).
cnf(t459912,plain,
join(X1,zero) = X1,
inference(step,[status(thm)],[t459911,t20807]) ).
cnf(t20977,plain,
join(X1,zero) = X1,
inference(orient,[status(thm)],[t459912]) ).
cnf(t460049,plain,
zero = meet(converse(X1),converse(complement(X1))),
inference(step,[status(thm)],[t460048,t20977]) ).
cnf(t23524,plain,
meet(converse(X1),converse(complement(X1))) = zero,
inference(orient,[status(thm)],[t460049]) ).
cnf(t38379,plain,
join(complement(converse(X1)),converse(complement(X1))) = join(complement(converse(X1)),zero),
inference(cp,[status(thm)],[t38324,t23524]) ).
cnf(t460500,plain,
join(converse(complement(X1)),complement(converse(X1))) = join(complement(converse(X1)),zero),
inference(step,[status(thm)],[t38379,t54]) ).
cnf(t460501,plain,
join(converse(complement(X1)),complement(converse(X1))) = complement(converse(X1)),
inference(step,[status(thm)],[t460500,t20977]) ).
cnf(t40156,plain,
join(converse(complement(X1)),complement(converse(X1))) = complement(converse(X1)),
inference(orient,[status(thm)],[t460501]) ).
cnf(t40161,plain,
complement(converse(complement(X1))) = join(converse(X1),complement(converse(complement(X1)))),
inference(cp,[status(thm)],[t40156,t21120]) ).
cnf(t22081,plain,
meet(X1,complement(converse(complement(converse(complement(X1)))))) = complement(top),
inference(cp,[status(thm)],[t22025,t446]) ).
cnf(t460433,plain,
meet(X1,complement(converse(complement(converse(complement(X1)))))) = zero,
inference(step,[status(thm)],[t22081,t112]) ).
cnf(t36025,plain,
meet(X1,complement(converse(complement(converse(complement(X1)))))) = zero,
inference(orient,[status(thm)],[t460433]) ).
cnf(t36820,plain,
join(X1,complement(converse(complement(converse(complement(complement(X1))))))) = join(X1,zero),
inference(cp,[status(thm)],[t36815,t36025]) ).
cnf(t460445,plain,
join(X1,complement(converse(complement(converse(X1))))) = join(X1,zero),
inference(step,[status(thm)],[t36820,t21120]) ).
cnf(t460446,plain,
join(X1,complement(converse(complement(converse(X1))))) = X1,
inference(step,[status(thm)],[t460445,t20977]) ).
cnf(t37025,plain,
join(X1,complement(converse(complement(converse(X1))))) = X1,
inference(orient,[status(thm)],[t460446]) ).
cnf(t37046,plain,
converse(X1) = join(converse(X1),complement(converse(complement(X1)))),
inference(cp,[status(thm)],[t37025,t22]) ).
cnf(t39048,plain,
join(converse(X1),complement(converse(complement(X1)))) = converse(X1),
inference(orient,[status(thm)],[t37046]) ).
cnf(t460502,plain,
complement(converse(complement(X1))) = converse(X1),
inference(step,[status(thm)],[t40161,t39048]) ).
cnf(t40213,plain,
complement(converse(complement(X1))) = converse(X1),
inference(orient,[status(thm)],[t460502]) ).
cnf(t40218,plain,
converse(complement(X1)) = complement(converse(X1)),
inference(cp,[status(thm)],[t40213,t21120]) ).
cnf(t40287,plain,
complement(converse(X1)) = converse(complement(X1)),
inference(orient,[status(thm)],[t40218]) ).
cnf(t40307,plain,
converse(complement(composition(X1,converse(X2)))) = complement(composition(X2,converse(X1))),
inference(cp,[status(thm)],[t40287,t166]) ).
cnf(t41704,plain,
converse(complement(composition(X1,converse(X2)))) = complement(composition(X2,converse(X1))),
inference(orient,[status(thm)],[t40307]) ).
cnf(t66548,plain,
converse(complement(composition(top,converse(X1)))) = composition(complement(composition(X1,converse(top))),top),
inference(cp,[status(thm)],[t66544,t41704]) ).
cnf(t461039,plain,
complement(composition(X1,converse(top))) = composition(complement(composition(X1,converse(top))),top),
inference(step,[status(thm)],[t66548,t41704]) ).
cnf(t461040,plain,
complement(composition(X1,top)) = composition(complement(composition(X1,converse(top))),top),
inference(step,[status(thm)],[t461039,t443]) ).
cnf(t461041,plain,
complement(composition(X1,top)) = composition(complement(composition(X1,top)),top),
inference(step,[status(thm)],[t461040,t443]) ).
cnf(t66628,plain,
composition(complement(composition(X1,top)),top) = complement(composition(X1,top)),
inference(orient,[status(thm)],[t461041]) ).
cnf(t68,plain,
complement(top) = join(complement(top),composition(converse(sk1),complement(sk1))),
inference(cp,[status(thm)],[t65,t49]) ).
cnf(t459299,plain,
zero = join(complement(top),composition(converse(sk1),complement(sk1))),
inference(step,[status(thm)],[t68,t112]) ).
cnf(t459300,plain,
zero = join(zero,composition(converse(sk1),complement(sk1))),
inference(step,[status(thm)],[t459299,t112]) ).
cnf(t2544,plain,
join(zero,composition(converse(sk1),complement(sk1))) = zero,
inference(orient,[status(thm)],[t459300]) ).
cnf(t459878,plain,
composition(converse(sk1),complement(sk1)) = zero,
inference(step,[status(thm)],[t2544,t20807]) ).
cnf(t20924,plain,
composition(converse(sk1),complement(sk1)) = zero,
inference(rw,[status(thm)],[t459878]) ).
cnf(t21361,plain,
composition(converse(sk1),complement(sk1)) = zero,
inference(orient,[status(thm)],[t20924]) ).
cnf(t21372,plain,
composition(converse(complement(sk1)),sk1) = converse(zero),
inference(cp,[status(thm)],[t176,t21361]) ).
cnf(t459986,plain,
composition(converse(complement(sk1)),sk1) = zero,
inference(step,[status(thm)],[t21372,t21285]) ).
cnf(t21447,plain,
composition(converse(complement(sk1)),sk1) = zero,
inference(orient,[status(thm)],[t459986]) ).
cnf(t21458,plain,
complement(sk1) = join(complement(sk1),composition(converse(converse(complement(sk1))),complement(zero))),
inference(cp,[status(thm)],[t65,t21447]) ).
cnf(t459987,plain,
complement(sk1) = join(complement(sk1),composition(complement(sk1),complement(zero))),
inference(step,[status(thm)],[t21458,t22]) ).
cnf(t459988,plain,
complement(sk1) = join(complement(sk1),composition(complement(sk1),top)),
inference(step,[status(thm)],[t459987,t20947]) ).
cnf(t459989,plain,
complement(sk1) = composition(complement(sk1),top),
inference(step,[status(thm)],[t459988,t10781]) ).
cnf(t21471,plain,
composition(complement(sk1),top) = complement(sk1),
inference(orient,[status(thm)],[t459989]) ).
cnf(t21475,plain,
composition(join(complement(sk1),X1),top) = join(complement(sk1),composition(X1,top)),
inference(cp,[status(thm)],[t25,t21471]) ).
cnf(t56174,plain,
composition(join(complement(sk1),X1),top) = join(complement(sk1),composition(X1,top)),
inference(orient,[status(thm)],[t21475]) ).
cnf(t22085,plain,
meet(complement(X1),complement(X2)) = complement(join(X1,X2)),
inference(cp,[status(thm)],[t22025,t21120]) ).
cnf(t22915,plain,
meet(complement(X1),complement(X2)) = complement(join(X1,X2)),
inference(orient,[status(thm)],[t22085]) ).
cnf(t36291,plain,
join(X1,complement(X2)) = join(X1,complement(join(X2,X1))),
inference(cp,[status(thm)],[t36275,t22915]) ).
cnf(t37715,plain,
join(X1,complement(join(X2,X1))) = join(X1,complement(X2)),
inference(orient,[status(thm)],[t36291]) ).
cnf(t37881,plain,
meet(X1,complement(complement(join(X2,complement(X1))))) = complement(join(complement(X1),complement(X2))),
inference(cp,[status(thm)],[t22025,t37715]) ).
cnf(t460458,plain,
meet(X1,join(X2,complement(X1))) = complement(join(complement(X1),complement(X2))),
inference(step,[status(thm)],[t37881,t21120]) ).
cnf(t460459,plain,
meet(X1,join(X2,complement(X1))) = meet(X1,X2),
inference(step,[status(thm)],[t460458,t100]) ).
cnf(t37905,plain,
meet(X1,join(X2,complement(X1))) = meet(X1,X2),
inference(orient,[status(thm)],[t460459]) ).
cnf(t37931,plain,
meet(X1,X2) = meet(X1,join(complement(X1),X2)),
inference(cp,[status(thm)],[t37905,t54]) ).
cnf(t37975,plain,
meet(X1,join(complement(X1),X2)) = meet(X1,X2),
inference(orient,[status(thm)],[t37931]) ).
cnf(t36312,plain,
join(X1,meet(X2,complement(meet(X3,X1)))) = join(X1,join(meet(X3,X1),X2)),
inference(cp,[status(thm)],[t29994,t36275]) ).
cnf(t461295,plain,
join(X1,meet(X2,complement(meet(X3,X1)))) = join(X1,X2),
inference(step,[status(thm)],[t36312,t29994]) ).
cnf(t80116,plain,
join(X1,meet(X2,complement(meet(X3,X1)))) = join(X1,X2),
inference(orient,[status(thm)],[t461295]) ).
cnf(t265,plain,
meet(complement(X1),X2) = complement(join(meet(X1,X1),complement(X2))),
inference(cp,[status(thm)],[t100,t256]) ).
cnf(t2381,plain,
complement(join(meet(X1,X1),complement(X2))) = meet(complement(X1),X2),
inference(orient,[status(thm)],[t265]) ).
cnf(t459922,plain,
complement(join(X1,complement(X2))) = meet(complement(X1),X2),
inference(step,[status(thm)],[t2381,t21009]) ).
cnf(t21049,plain,
complement(join(X1,complement(X2))) = meet(complement(X1),X2),
inference(rw,[status(thm)],[t459922]) ).
cnf(t22267,plain,
complement(join(X1,complement(X2))) = meet(complement(X1),X2),
inference(orient,[status(thm)],[t21049]) ).
cnf(t22283,plain,
join(X1,complement(X2)) = complement(meet(complement(X1),X2)),
inference(cp,[status(thm)],[t21120,t22267]) ).
cnf(t22991,plain,
complement(meet(complement(X1),X2)) = join(X1,complement(X2)),
inference(orient,[status(thm)],[t22283]) ).
cnf(t80130,plain,
join(X1,X2) = join(X1,meet(X2,join(X3,complement(X1)))),
inference(cp,[status(thm)],[t80116,t22991]) ).
cnf(t98883,plain,
join(X1,meet(X2,join(X3,complement(X1)))) = join(X1,X2),
inference(orient,[status(thm)],[t80130]) ).
cnf(t98958,plain,
meet(X1,meet(X2,join(X3,complement(complement(X1))))) = meet(X1,join(complement(X1),X2)),
inference(cp,[status(thm)],[t37975,t98883]) ).
cnf(t461635,plain,
meet(X1,meet(X2,join(X3,X1))) = meet(X1,join(complement(X1),X2)),
inference(step,[status(thm)],[t98958,t21120]) ).
cnf(t461636,plain,
meet(X1,meet(X2,join(X3,X1))) = meet(X1,X2),
inference(step,[status(thm)],[t461635,t37975]) ).
cnf(t99005,plain,
meet(X1,meet(X2,join(X3,X1))) = meet(X1,X2),
inference(orient,[status(thm)],[t461636]) ).
cnf(t99247,plain,
meet(X1,X2) = meet(X1,meet(X2,join(X1,X3))),
inference(cp,[status(thm)],[t99005,t54]) ).
cnf(t99719,plain,
meet(X1,meet(X2,join(X1,X3))) = meet(X1,X2),
inference(orient,[status(thm)],[t99247]) ).
cnf(t99767,plain,
meet(X1,X2) = meet(X1,meet(X2,composition(top,X1))),
inference(cp,[status(thm)],[t99719,t10876]) ).
cnf(t100468,plain,
meet(X1,meet(X2,composition(top,X1))) = meet(X1,X2),
inference(orient,[status(thm)],[t99767]) ).
cnf(t36819,plain,
join(X1,complement(X2)) = join(X1,complement(join(X1,X2))),
inference(cp,[status(thm)],[t36815,t22915]) ).
cnf(t38168,plain,
join(X1,complement(join(X1,X2))) = join(X1,complement(X2)),
inference(orient,[status(thm)],[t36819]) ).
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(t44,plain,
composition(sk0,top) = sk0,
inference(orient,[status(thm)],[t1]) ).
cnf(t461,plain,
composition(top,converse(sk0)) = converse(sk0),
inference(cp,[status(thm)],[t455,t44]) ).
cnf(t484,plain,
composition(top,converse(sk0)) = converse(sk0),
inference(orient,[status(thm)],[t461]) ).
cnf(t485,plain,
composition(join(top,X1),converse(sk0)) = join(converse(sk0),composition(X1,converse(sk0))),
inference(cp,[status(thm)],[t25,t484]) ).
cnf(t459166,plain,
composition(top,converse(sk0)) = join(converse(sk0),composition(X1,converse(sk0))),
inference(step,[status(thm)],[t485,t435]) ).
cnf(t459167,plain,
converse(sk0) = join(converse(sk0),composition(X1,converse(sk0))),
inference(step,[status(thm)],[t459166,t484]) ).
cnf(t631,plain,
join(converse(sk0),composition(X1,converse(sk0))) = converse(sk0),
inference(orient,[status(thm)],[t459167]) ).
cnf(t637,plain,
join(sk0,converse(composition(X1,converse(sk0)))) = converse(converse(sk0)),
inference(cp,[status(thm)],[t285,t631]) ).
cnf(t459170,plain,
join(sk0,composition(sk0,converse(X1))) = converse(converse(sk0)),
inference(step,[status(thm)],[t637,t166]) ).
cnf(t459171,plain,
join(sk0,composition(sk0,converse(X1))) = sk0,
inference(step,[status(thm)],[t459170,t22]) ).
cnf(t658,plain,
join(sk0,composition(sk0,converse(X1))) = sk0,
inference(orient,[status(thm)],[t459171]) ).
cnf(t664,plain,
sk0 = join(sk0,composition(sk0,X1)),
inference(cp,[status(thm)],[t658,t22]) ).
cnf(t669,plain,
join(sk0,composition(sk0,X1)) = sk0,
inference(orient,[status(thm)],[t664]) ).
cnf(t670,plain,
join(sk0,join(composition(sk0,X1),X2)) = join(sk0,X2),
inference(cp,[status(thm)],[t57,t669]) ).
cnf(t704,plain,
join(sk0,join(composition(sk0,X1),X2)) = join(sk0,X2),
inference(orient,[status(thm)],[t670]) ).
cnf(t705,plain,
join(sk0,composition(X1,X2)) = join(sk0,composition(join(sk0,X1),X2)),
inference(cp,[status(thm)],[t704,t25]) ).
cnf(t3306,plain,
join(sk0,composition(join(sk0,X1),X2)) = join(sk0,composition(X1,X2)),
inference(orient,[status(thm)],[t705]) ).
cnf(t3336,plain,
join(sk0,composition(complement(sk0),X1)) = join(sk0,composition(top,X1)),
inference(cp,[status(thm)],[t3306,t62]) ).
cnf(t3347,plain,
join(sk0,composition(complement(sk0),X1)) = join(sk0,composition(top,X1)),
inference(orient,[status(thm)],[t3336]) ).
cnf(t38229,plain,
join(sk0,complement(composition(complement(sk0),X1))) = join(sk0,complement(join(sk0,composition(top,X1)))),
inference(cp,[status(thm)],[t38168,t3347]) ).
cnf(t69,plain,
complement(top) = join(complement(top),composition(converse(sk0),complement(sk0))),
inference(cp,[status(thm)],[t65,t44]) ).
cnf(t459310,plain,
zero = join(complement(top),composition(converse(sk0),complement(sk0))),
inference(step,[status(thm)],[t69,t112]) ).
cnf(t459311,plain,
zero = join(zero,composition(converse(sk0),complement(sk0))),
inference(step,[status(thm)],[t459310,t112]) ).
cnf(t2576,plain,
join(zero,composition(converse(sk0),complement(sk0))) = zero,
inference(orient,[status(thm)],[t459311]) ).
cnf(t459877,plain,
composition(converse(sk0),complement(sk0)) = zero,
inference(step,[status(thm)],[t2576,t20807]) ).
cnf(t20923,plain,
composition(converse(sk0),complement(sk0)) = zero,
inference(rw,[status(thm)],[t459877]) ).
cnf(t21338,plain,
composition(converse(sk0),complement(sk0)) = zero,
inference(orient,[status(thm)],[t20923]) ).
cnf(t21341,plain,
composition(converse(sk0),composition(complement(sk0),X1)) = composition(zero,X1),
inference(cp,[status(thm)],[t23,t21338]) ).
cnf(t460050,plain,
composition(converse(sk0),composition(complement(sk0),X1)) = zero,
inference(step,[status(thm)],[t21341,t21337]) ).
cnf(t23552,plain,
composition(converse(sk0),composition(complement(sk0),X1)) = zero,
inference(orient,[status(thm)],[t460050]) ).
cnf(t23563,plain,
complement(composition(complement(sk0),X1)) = join(complement(composition(complement(sk0),X1)),composition(converse(converse(sk0)),complement(zero))),
inference(cp,[status(thm)],[t65,t23552]) ).
cnf(t461001,plain,
complement(composition(complement(sk0),X1)) = join(complement(composition(complement(sk0),X1)),composition(sk0,complement(zero))),
inference(step,[status(thm)],[t23563,t22]) ).
cnf(t461002,plain,
complement(composition(complement(sk0),X1)) = join(composition(sk0,complement(zero)),complement(composition(complement(sk0),X1))),
inference(step,[status(thm)],[t461001,t54]) ).
cnf(t461003,plain,
complement(composition(complement(sk0),X1)) = join(composition(sk0,top),complement(composition(complement(sk0),X1))),
inference(step,[status(thm)],[t461002,t20947]) ).
cnf(t461004,plain,
complement(composition(complement(sk0),X1)) = join(sk0,complement(composition(complement(sk0),X1))),
inference(step,[status(thm)],[t461003,t44]) ).
cnf(t64962,plain,
join(sk0,complement(composition(complement(sk0),X1))) = complement(composition(complement(sk0),X1)),
inference(orient,[status(thm)],[t461004]) ).
cnf(t465696,plain,
complement(composition(complement(sk0),X1)) = join(sk0,complement(join(sk0,composition(top,X1)))),
inference(step,[status(thm)],[t38229,t64962]) ).
cnf(t465697,plain,
complement(composition(complement(sk0),X1)) = join(sk0,complement(composition(top,X1))),
inference(step,[status(thm)],[t465696,t38168]) ).
cnf(t456274,plain,
join(sk0,complement(composition(top,X1))) = complement(composition(complement(sk0),X1)),
inference(orient,[status(thm)],[t465697]) ).
cnf(t456510,plain,
meet(complement(sk0),composition(top,X1)) = complement(complement(composition(complement(sk0),X1))),
inference(cp,[status(thm)],[t22267,t456274]) ).
cnf(t465698,plain,
meet(complement(sk0),composition(top,X1)) = composition(complement(sk0),X1),
inference(step,[status(thm)],[t456510,t21120]) ).
cnf(t456594,plain,
meet(complement(sk0),composition(top,X1)) = composition(complement(sk0),X1),
inference(orient,[status(thm)],[t465698]) ).
cnf(t456797,plain,
meet(X1,complement(sk0)) = meet(X1,composition(complement(sk0),X1)),
inference(cp,[status(thm)],[t100468,t456594]) ).
cnf(t456869,plain,
meet(X1,composition(complement(sk0),X1)) = meet(X1,complement(sk0)),
inference(orient,[status(thm)],[t456797]) ).
cnf(t456919,plain,
join(complement(X1),composition(complement(sk0),X1)) = join(complement(X1),meet(X1,complement(sk0))),
inference(cp,[status(thm)],[t38324,t456869]) ).
cnf(t465712,plain,
join(complement(X1),composition(complement(sk0),X1)) = join(complement(X1),complement(sk0)),
inference(step,[status(thm)],[t456919,t38324]) ).
cnf(t115,plain,
meet(top,X1) = complement(join(zero,complement(X1))),
inference(cp,[status(thm)],[t100,t112]) ).
cnf(t143,plain,
complement(join(zero,complement(X1))) = meet(top,X1),
inference(orient,[status(thm)],[t115]) ).
cnf(t145,plain,
meet(top,join(complement(X1),complement(X2))) = complement(join(zero,meet(X1,X2))),
inference(cp,[status(thm)],[t143,t100]) ).
cnf(t9606,plain,
meet(top,join(complement(X1),complement(X2))) = complement(join(zero,meet(X1,X2))),
inference(orient,[status(thm)],[t145]) ).
cnf(t459864,plain,
meet(top,join(complement(X1),complement(X2))) = complement(meet(X1,X2)),
inference(step,[status(thm)],[t9606,t20807]) ).
cnf(t20810,plain,
meet(top,join(complement(X1),complement(X2))) = complement(meet(X1,X2)),
inference(orient,[status(thm)],[t459864]) ).
cnf(t459891,plain,
complement(complement(X1)) = meet(top,X1),
inference(step,[status(thm)],[t143,t20807]) ).
cnf(t20935,plain,
complement(complement(X1)) = meet(top,X1),
inference(rw,[status(thm)],[t459891]) ).
cnf(t459942,plain,
X1 = meet(top,X1),
inference(step,[status(thm)],[t20935,t21120]) ).
cnf(t21168,plain,
meet(top,X1) = X1,
inference(orient,[status(thm)],[t459942]) ).
cnf(t459945,plain,
join(complement(X1),complement(X2)) = complement(meet(X1,X2)),
inference(step,[status(thm)],[t20810,t21168]) ).
cnf(t21190,plain,
join(complement(X1),complement(X2)) = complement(meet(X1,X2)),
inference(rw,[status(thm)],[t459945]) ).
cnf(t22346,plain,
join(complement(X1),complement(X2)) = complement(meet(X1,X2)),
inference(orient,[status(thm)],[t21190]) ).
cnf(t465713,plain,
join(complement(X1),composition(complement(sk0),X1)) = complement(meet(X1,sk0)),
inference(step,[status(thm)],[t465712,t22346]) ).
cnf(t458636,plain,
join(complement(X1),composition(complement(sk0),X1)) = complement(meet(X1,sk0)),
inference(orient,[status(thm)],[t465713]) ).
cnf(t458739,plain,
join(complement(sk1),composition(composition(complement(sk0),sk1),top)) = composition(complement(meet(sk1,sk0)),top),
inference(cp,[status(thm)],[t56174,t458636]) ).
cnf(t465714,plain,
join(complement(sk1),composition(complement(sk0),composition(sk1,top))) = composition(complement(meet(sk1,sk0)),top),
inference(step,[status(thm)],[t458739,t23]) ).
cnf(t465715,plain,
join(complement(sk1),composition(complement(sk0),sk1)) = composition(complement(meet(sk1,sk0)),top),
inference(step,[status(thm)],[t465714,t49]) ).
cnf(t465716,plain,
complement(meet(sk1,sk0)) = composition(complement(meet(sk1,sk0)),top),
inference(step,[status(thm)],[t465715,t458636]) ).
cnf(t458821,plain,
composition(complement(meet(sk1,sk0)),top) = complement(meet(sk1,sk0)),
inference(orient,[status(thm)],[t465716]) ).
cnf(t458864,plain,
complement(composition(complement(meet(sk1,sk0)),top)) = composition(complement(complement(meet(sk1,sk0))),top),
inference(cp,[status(thm)],[t66628,t458821]) ).
cnf(t465717,plain,
complement(complement(meet(sk1,sk0))) = composition(complement(complement(meet(sk1,sk0))),top),
inference(step,[status(thm)],[t458864,t458821]) ).
cnf(t465718,plain,
meet(sk1,sk0) = composition(complement(complement(meet(sk1,sk0))),top),
inference(step,[status(thm)],[t465717,t21120]) ).
cnf(t465719,plain,
meet(sk1,sk0) = composition(meet(sk1,sk0),top),
inference(step,[status(thm)],[t465718,t21120]) ).
cnf(t458974,plain,
composition(meet(sk1,sk0),top) = meet(sk1,sk0),
inference(orient,[status(thm)],[t465719]) ).
cnf(c18,plain,
composition(meet(sk0,sk1),top) != meet(sk0,sk1),
inference(cnf_transformation,[status(esa)],[f16_sk]) ).
cnf(goal_0,negated_conjecture,
composition(meet(sk0,sk1),top) != meet(sk0,sk1),
inference(equality_encoding,[status(esa)],[c18]) ).
cnf(g0_0,plain,
composition(meet(sk1,sk0),top) != meet(sk0,sk1),
inference(rw,[status(thm)],[goal_0,t121]) ).
cnf(g0_1,plain,
meet(sk1,sk0) != meet(sk0,sk1),
inference(rw,[status(thm)],[g0_0,t458974]) ).
cnf(g0_2,plain,
meet(sk1,sk0) != meet(sk1,sk0),
inference(rw,[status(thm)],[g0_1,t121]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_2]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : REL019+2 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.10/0.38 % Computer : n002.cluster.edu
% 0.10/0.38 % Model : x86_64 x86_64
% 0.10/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.38 % Memory : 8046.5625MB
% 0.10/0.38 % OS : Linux 6.8.0-71-generic
% 0.10/0.38 % CPULimit : 300
% 0.10/0.38 % WCLimit : 300
% 0.10/0.38 % DateTime : Thu Sep 24 07:19:04 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.38 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 253.69/37.04 % SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p
% 253.69/37.04 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------