%------------------------------------------------------------------------------
% File : Waldmeister---710
% Problem : REL042-2 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : woody %s
% Computer : n015.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 600s
% DateTime : Mon Jul 18 20:10:34 EDT 2022
% Result : Unsatisfiable 1.72s 2.12s
% Output : CNFRefutation 1.74s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.14 % Problem : REL042-2 : TPTP v8.1.0. Released v4.0.0.
% 0.08/0.15 % Command : woody %s
% 0.15/0.37 % Computer : n015.cluster.edu
% 0.15/0.37 % Model : x86_64 x86_64
% 0.15/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.37 % Memory : 8042.1875MB
% 0.15/0.37 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.37 % CPULimit : 300
% 0.15/0.37 % WCLimit : 600
% 0.15/0.37 % DateTime : Fri Jul 8 14:02:06 EDT 2022
% 0.15/0.37 % CPUTime :
% 0.65/1.06 ********************************************************************************
% 0.65/1.06 * W A L D M E I S T E R \| \ / \|/ *
% 0.65/1.06 * |/ | \/ | *
% 0.65/1.06 * (C) 1994-2010 A. Buch and Th. Hillenbrand, \ / \ / *
% 0.65/1.06 * A. Jaeger and B. Loechner | | *
% 0.65/1.06 * <waldmeister@informatik.uni-kl.de> | *
% 0.65/1.06 ********************************************************************************
% 0.65/1.06
% 0.65/1.06
% 0.65/1.06 Goals:
% 0.65/1.06 ------
% 0.65/1.06
% 0.65/1.06 ( 1) join(composition(converse(sk1),sk1),one) ?=? one
% 0.65/1.06
% 0.65/1.06 Detected structure: Orkus
% 0.65/1.06 ********************************************************************************
% 0.65/1.06 ****************************** COMPLETION - PROOF ******************************
% 0.65/1.06 ********************************************************************************
% 0.65/1.06
% 1.72/2.12 joined goal: 1 join(composition(converse(sk1),sk1),one) ?= one to one
% 1.72/2.12 goal joined
% 1.72/2.12 % SZS status Unsatisfiable
% 1.72/2.12 #START OF PROOF
% 1.72/2.12 % SZS output start CNFRefutation
% 1.72/2.12 cnf('0.1.0.0',axiom,
% 1.72/2.12 ( X1 = composition(X1,one) ),
% 1.72/2.12 file('/tmp/WALDMEISTER_7164_n015')).
% 1.72/2.12 cnf('0.1.1.0',plain,
% 1.72/2.12 ( X1 = composition(X1,one) ),
% 1.72/2.12 inference(weigh,[status(thm)],['0.1.0.0']),
% 1.72/2.12 [weight('<0,0,0,[0,0,0,1]>')]).
% 1.72/2.12 cnf('0.1.2.0',plain,
% 1.72/2.12 ( composition(X1,one) = X1 ),
% 1.72/2.12 inference(orient,[status(thm)],['0.1.1.0',theory(equality)]),
% 1.72/2.12 [x,rule_1]).
% 1.72/2.12 cnf('0.3.0.0',axiom,
% 1.72/2.12 ( X1 = converse(converse(X1)) ),
% 1.72/2.12 file('/tmp/WALDMEISTER_7164_n015')).
% 1.72/2.12 cnf('0.3.1.0',plain,
% 1.72/2.12 ( X1 = converse(converse(X1)) ),
% 1.72/2.12 inference(weigh,[status(thm)],['0.3.0.0']),
% 1.72/2.12 [weight('<2,0,0,[0,0,0,3]>')]).
% 1.72/2.12 cnf('0.3.2.0',plain,
% 1.72/2.12 ( converse(converse(X1)) = X1 ),
% 1.72/2.12 inference(orient,[status(thm)],['0.3.1.0',theory(equality)]),
% 1.72/2.12 [x,rule_3]).
% 1.72/2.12 cnf('0.4.0.0',axiom,
% 1.72/2.12 ( composition(X1,composition(X2,X3)) = composition(composition(X1,X2),X3) ),
% 1.72/2.12 file('/tmp/WALDMEISTER_7164_n015')).
% 1.72/2.12 cnf('0.4.1.0',plain,
% 1.72/2.12 ( composition(X1,composition(X2,X3)) = composition(composition(X1,X2),X3) ),
% 1.72/2.12 inference(weigh,[status(thm)],['0.4.0.0']),
% 1.72/2.12 [weight('<3,0,0,[0,0,0,4]>')]).
% 1.72/2.12 cnf('0.4.2.0',plain,
% 1.72/2.12 ( composition(composition(X1,X2),X3) = composition(X1,composition(X2,X3)) ),
% 1.72/2.12 inference(orient,[status(thm)],['0.4.1.0',theory(equality)]),
% 1.72/2.12 [x,rule_4]).
% 1.72/2.12 cnf('0.5.0.0',axiom,
% 1.72/2.12 ( composition(join(X1,X2),X3) = join(composition(X1,X3),composition(X2,X3)) ),
% 1.72/2.12 file('/tmp/WALDMEISTER_7164_n015')).
% 1.72/2.12 cnf('0.5.1.0',plain,
% 1.72/2.12 ( composition(join(X1,X2),X3) = join(composition(X1,X3),composition(X2,X3)) ),
% 1.72/2.12 inference(weigh,[status(thm)],['0.5.0.0']),
% 1.72/2.12 [weight('<4,0,0,[0,0,0,5]>')]).
% 1.72/2.12 cnf('0.5.2.0',plain,
% 1.72/2.12 ( join(composition(X1,X2),composition(X3,X2)) = composition(join(X1,X3),X2) ),
% 1.72/2.12 inference(orient,[status(thm)],['0.5.1.0',theory(equality)]),
% 1.72/2.12 [x,rule_5]).
% 1.72/2.12 cnf('0.6.0.0',axiom,
% 1.72/2.12 ( 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(X3,composition(converse(X1),X2)))) ),
% 1.72/2.12 file('/tmp/WALDMEISTER_7164_n015')).
% 1.72/2.12 cnf('0.6.1.0',plain,
% 1.72/2.12 ( 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(X3,composition(converse(X1),X2)))) ),
% 1.72/2.12 inference(weigh,[status(thm)],['0.6.0.0']),
% 1.72/2.12 [weight('<5,0,0,[0,0,0,6]>')]).
% 1.72/2.12 cnf('0.6.2.0',plain,
% 1.72/2.12 ( 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))) ),
% 1.72/2.12 inference(orient,[status(thm)],['0.6.1.0',theory(equality)]),
% 1.72/2.12 [x,rule_6]).
% 1.72/2.12 cnf('0.7.0.0',axiom,
% 1.72/2.12 ( composition(converse(X1),converse(X2)) = converse(composition(X2,X1)) ),
% 1.72/2.12 file('/tmp/WALDMEISTER_7164_n015')).
% 1.72/2.12 cnf('0.7.1.0',plain,
% 1.72/2.12 ( composition(converse(X1),converse(X2)) = converse(composition(X2,X1)) ),
% 1.72/2.12 inference(weigh,[status(thm)],['0.7.0.0']),
% 1.72/2.12 [weight('<6,0,0,[0,0,0,7]>')]).
% 1.72/2.12 cnf('0.7.2.0',plain,
% 1.72/2.12 ( composition(converse(X1),converse(X2)) = converse(composition(X2,X1)) ),
% 1.72/2.12 inference(orient,[status(thm)],['0.7.1.0',theory(equality)]),
% 1.72/2.12 [u,rule_7]).
% 1.72/2.12 cnf('0.8.0.0',axiom,
% 1.72/2.12 ( join(X1,X2) = join(X2,X1) ),
% 1.72/2.12 file('/tmp/WALDMEISTER_7164_n015')).
% 1.72/2.12 cnf('0.8.1.0',plain,
% 1.72/2.12 ( join(X1,X2) = join(X2,X1) ),
% 1.72/2.12 inference(weigh,[status(thm)],['0.8.0.0']),
% 1.72/2.12 [weight('<7,0,0,[0,0,0,8]>')]).
% 1.72/2.12 cnf('0.8.2.0',plain,
% 1.72/2.12 ( join(X1,X2) = join(X2,X1) ),
% 1.72/2.12 inference(activate,[status(thm)],['0.8.1.0']),
% 1.72/2.12 [equation_1]).
% 1.72/2.12 cnf('0.9.0.0',axiom,
% 1.72/2.12 ( join(X1,join(X2,X3)) = join(join(X1,X2),X3) ),
% 1.72/2.12 file('/tmp/WALDMEISTER_7164_n015')).
% 1.72/2.12 cnf('0.9.1.0',plain,
% 1.72/2.12 ( join(X1,join(X2,X3)) = join(join(X1,X2),X3) ),
% 1.72/2.12 inference(weigh,[status(thm)],['0.9.0.0']),
% 1.72/2.12 [weight('<8,0,0,[0,0,0,9]>')]).
% 1.72/2.12 cnf('0.9.2.0',plain,
% 1.72/2.12 ( join(join(X1,X2),X3) = join(X1,join(X2,X3)) ),
% 1.72/2.12 inference(orient,[status(thm)],['0.9.1.0',theory(equality)]),
% 1.72/2.12 [x,rule_8]).
% 1.72/2.12 cnf('0.10.0.0',axiom,
% 1.72/2.12 ( join(X1,complement(X1)) = top ),
% 1.72/2.12 file('/tmp/WALDMEISTER_7164_n015')).
% 1.72/2.12 cnf('0.10.1.0',plain,
% 1.72/2.12 ( join(X1,complement(X1)) = top ),
% 1.72/2.12 inference(weigh,[status(thm)],['0.10.0.0']),
% 1.72/2.12 [weight('<9,0,0,[0,0,0,10]>')]).
% 1.72/2.12 cnf('0.10.2.0',plain,
% 1.72/2.12 ( join(X1,complement(X1)) = top ),
% 1.72/2.12 inference(orient,[status(thm)],['0.10.1.0',theory(equality)]),
% 1.72/2.12 [u,rule_9]).
% 1.72/2.12 cnf('0.11.0.0',axiom,
% 1.72/2.12 ( join(composition(converse(X1),complement(composition(X1,X2))),complement(X2)) = complement(X2) ),
% 1.72/2.12 file('/tmp/WALDMEISTER_7164_n015')).
% 1.72/2.12 cnf('0.11.1.0',plain,
% 1.72/2.12 ( join(composition(converse(X1),complement(composition(X1,X2))),complement(X2)) = complement(X2) ),
% 1.72/2.12 inference(weigh,[status(thm)],['0.11.0.0']),
% 1.72/2.12 [weight('<10,0,0,[0,0,0,11]>')]).
% 1.72/2.12 cnf('0.11.1.1',plain,
% 1.72/2.12 ( join(complement(X2),composition(converse(X1),complement(composition(X1,X2)))) = complement(X2) ),
% 1.72/2.12 inference(reduction,[status(thm)],['0.11.1.0','0.8.2.0',theory(equality)]),
% 1.72/2.12 [pos('L','L')]).
% 1.72/2.12 cnf('0.11.2.0',plain,
% 1.72/2.12 ( join(complement(X1),composition(converse(X2),complement(composition(X2,X1)))) = complement(X1) ),
% 1.72/2.12 inference(orient,[status(thm)],['0.11.1.1',theory(equality)]),
% 1.72/2.12 [u,rule_10]).
% 1.72/2.12 cnf('0.14.0.0',axiom,
% 1.72/2.12 ( join(converse(X1),converse(X2)) = converse(join(X1,X2)) ),
% 1.72/2.12 file('/tmp/WALDMEISTER_7164_n015')).
% 1.72/2.12 cnf('0.14.1.0',plain,
% 1.72/2.12 ( join(converse(X1),converse(X2)) = converse(join(X1,X2)) ),
% 1.72/2.12 inference(weigh,[status(thm)],['0.14.0.0']),
% 1.72/2.12 [weight('<13,0,0,[0,0,0,14]>')]).
% 1.72/2.12 cnf('0.14.2.0',plain,
% 1.72/2.12 ( join(converse(X1),converse(X2)) = converse(join(X1,X2)) ),
% 1.72/2.12 inference(orient,[status(thm)],['0.14.1.0',theory(equality)]),
% 1.72/2.12 [u,rule_13]).
% 1.72/2.12 cnf('0.15.0.0',axiom,
% 1.72/2.12 ( meet(X1,X2) = complement(join(complement(X1),complement(X2))) ),
% 1.72/2.12 file('/tmp/WALDMEISTER_7164_n015')).
% 1.72/2.12 cnf('0.15.1.0',plain,
% 1.72/2.12 ( meet(X1,X2) = complement(join(complement(X1),complement(X2))) ),
% 1.72/2.12 inference(weigh,[status(thm)],['0.15.0.0']),
% 1.72/2.12 [weight('<14,0,0,[0,0,0,15]>')]).
% 1.72/2.12 cnf('0.15.2.0',plain,
% 1.72/2.12 ( complement(join(complement(X1),complement(X2))) = meet(X1,X2) ),
% 1.72/2.12 inference(orient,[status(thm)],['0.15.1.0',theory(equality)]),
% 1.72/2.12 [x,rule_14]).
% 1.72/2.12 cnf('0.16.0.0',axiom,
% 1.72/2.12 ( meet(X1,complement(X1)) = zero ),
% 1.72/2.12 file('/tmp/WALDMEISTER_7164_n015')).
% 1.72/2.12 cnf('0.16.1.0',plain,
% 1.72/2.12 ( meet(X1,complement(X1)) = zero ),
% 1.72/2.12 inference(weigh,[status(thm)],['0.16.0.0']),
% 1.72/2.12 [weight('<15,0,0,[0,0,0,16]>')]).
% 1.72/2.12 cnf('0.16.2.0',plain,
% 1.72/2.12 ( meet(X1,complement(X1)) = zero ),
% 1.72/2.12 inference(orient,[status(thm)],['0.16.1.0',theory(equality)]),
% 1.72/2.12 [u,rule_15]).
% 1.72/2.12 cnf('0.17.0.0',axiom,
% 1.72/2.12 ( meet(composition(sk1,X1),composition(sk1,complement(X1))) = zero ),
% 1.72/2.12 file('/tmp/WALDMEISTER_7164_n015')).
% 1.72/2.12 cnf('0.17.1.0',plain,
% 1.72/2.12 ( meet(composition(sk1,X1),composition(sk1,complement(X1))) = zero ),
% 1.72/2.12 inference(weigh,[status(thm)],['0.17.0.0']),
% 1.72/2.12 [weight('<16,0,0,[0,0,0,17]>')]).
% 1.72/2.12 cnf('0.17.2.0',plain,
% 1.72/2.12 ( meet(composition(sk1,X1),composition(sk1,complement(X1))) = zero ),
% 1.72/2.12 inference(orient,[status(thm)],['0.17.1.0',theory(equality)]),
% 1.72/2.12 [u,rule_16]).
% 1.72/2.12 cnf('0.18.0.0',plain,
% 1.72/2.12 ( meet(X1,complement(X1)) = complement(top) ),
% 1.72/2.12 inference(cp,[status(thm)],['0.15.2.0','0.10.2.0',theory(equality)]),
% 1.72/2.12 [pos('L.1','L')]).
% 1.72/2.12 cnf('0.18.1.0',plain,
% 1.72/2.12 ( meet(X1,complement(X1)) = complement(top) ),
% 1.72/2.12 inference(weigh,[status(thm)],['0.18.0.0']),
% 1.72/2.12 [weight('<34,15,10,[1,0,0,1]>')]).
% 1.72/2.12 cnf('0.18.1.1',plain,
% 1.72/2.12 ( zero = complement(top) ),
% 1.72/2.12 inference(reduction,[status(thm)],['0.18.1.0','0.16.2.0',theory(equality)]),
% 1.72/2.12 [pos('L','L')]).
% 1.72/2.12 cnf('0.18.2.0',plain,
% 1.72/2.12 ( complement(top) = zero ),
% 1.72/2.12 inference(orient,[status(thm)],['0.18.1.1',theory(equality)]),
% 1.72/2.12 [x,rule_17]).
% 1.72/2.12 cnf('0.21.0.0',plain,
% 1.72/2.12 ( meet(X1,X2) = complement(join(complement(X2),complement(X1))) ),
% 1.72/2.12 inference(cp,[status(thm)],['0.15.2.0','0.8.2.0',theory(equality)]),
% 1.72/2.12 [pos('L.1','L')]).
% 1.72/2.12 cnf('0.21.0.1',plain,
% 1.72/2.12 ( meet(X1,X2) = meet(X2,X1) ),
% 1.72/2.12 inference(reduction,[status(thm)],['0.21.0.0','0.15.2.0',theory(equality)]),
% 1.72/2.12 [pos('R','L')]).
% 1.72/2.12 cnf('0.21.1.0',plain,
% 1.72/2.12 ( meet(X1,X2) = meet(X2,X1) ),
% 1.72/2.12 inference(weigh,[status(thm)],['0.21.0.1']),
% 1.72/2.12 [weight('<48,15,8,[1,0,0,1]>')]).
% 1.72/2.12 cnf('0.21.2.0',plain,
% 1.72/2.12 ( meet(X1,X2) = meet(X2,X1) ),
% 1.72/2.12 inference(activate,[status(thm)],['0.21.1.0']),
% 1.72/2.12 [equation_2]).
% 1.72/2.12 cnf('0.23.0.0',plain,
% 1.72/2.12 ( meet(top,X1) = complement(join(zero,complement(X1))) ),
% 1.72/2.12 inference(cp,[status(thm)],['0.15.2.0','0.18.2.0',theory(equality)]),
% 1.72/2.12 [pos('L.1.1','L')]).
% 1.72/2.12 cnf('0.23.1.0',plain,
% 1.72/2.12 ( meet(top,X1) = complement(join(zero,complement(X1))) ),
% 1.72/2.12 inference(weigh,[status(thm)],['0.23.0.0']),
% 1.72/2.12 [weight('<53,18,15,[0,0,0,2]>')]).
% 1.72/2.12 cnf('0.23.2.0',plain,
% 1.72/2.12 ( complement(join(zero,complement(X1))) = meet(top,X1) ),
% 1.72/2.12 inference(orient,[status(thm)],['0.23.1.0',theory(equality)]),
% 1.72/2.12 [x,rule_21]).
% 1.72/2.12 cnf('0.28.0.0',plain,
% 1.72/2.12 ( zero = meet(sk1,composition(sk1,complement(one))) ),
% 1.72/2.12 inference(cp,[status(thm)],['0.17.2.0','0.1.2.0',theory(equality)]),
% 1.72/2.12 [pos('L.1','L')]).
% 1.72/2.12 cnf('0.28.1.0',plain,
% 1.72/2.12 ( zero = meet(sk1,composition(sk1,complement(one))) ),
% 1.72/2.12 inference(weigh,[status(thm)],['0.28.0.0']),
% 1.72/2.12 [weight('<55,17,1,[1,0,0,1]>')]).
% 1.72/2.12 cnf('0.28.2.0',plain,
% 1.72/2.12 ( meet(sk1,composition(sk1,complement(one))) = zero ),
% 1.72/2.12 inference(orient,[status(thm)],['0.28.1.0',theory(equality)]),
% 1.72/2.12 [x,rule_26]).
% 1.72/2.12 cnf('0.29.0.0',plain,
% 1.72/2.12 ( converse(composition(X1,converse(X2))) = composition(X2,converse(X1)) ),
% 1.72/2.12 inference(cp,[status(thm)],['0.7.2.0','0.3.2.0',theory(equality)]),
% 1.72/2.12 [pos('L.1','L')]).
% 1.72/2.12 cnf('0.29.1.0',plain,
% 1.72/2.12 ( converse(composition(X1,converse(X2))) = composition(X2,converse(X1)) ),
% 1.72/2.12 inference(weigh,[status(thm)],['0.29.0.0']),
% 1.72/2.12 [weight('<59,7,3,[1,0,0,1]>')]).
% 1.72/2.12 cnf('0.29.2.0',plain,
% 1.72/2.12 ( converse(composition(X1,converse(X2))) = composition(X2,converse(X1)) ),
% 1.72/2.12 inference(orient,[status(thm)],['0.29.1.0',theory(equality)]),
% 1.72/2.12 [u,rule_27]).
% 1.72/2.12 cnf('0.30.0.0',plain,
% 1.72/2.12 ( converse(composition(converse(X1),X2)) = composition(converse(X2),X1) ),
% 1.72/2.12 inference(cp,[status(thm)],['0.7.2.0','0.3.2.0',theory(equality)]),
% 1.72/2.12 [pos('L.2','L')]).
% 1.72/2.12 cnf('0.30.1.0',plain,
% 1.72/2.12 ( converse(composition(converse(X1),X2)) = composition(converse(X2),X1) ),
% 1.72/2.12 inference(weigh,[status(thm)],['0.30.0.0']),
% 1.72/2.12 [weight('<59,7,3,[1,0,0,3]>')]).
% 1.72/2.12 cnf('0.30.2.0',plain,
% 1.72/2.12 ( converse(composition(converse(X1),X2)) = composition(converse(X2),X1) ),
% 1.72/2.12 inference(orient,[status(thm)],['0.30.1.0',theory(equality)]),
% 1.72/2.12 [u,rule_28]).
% 1.72/2.12 cnf('0.31.0.0',plain,
% 1.72/2.12 ( composition(converse(one),X1) = converse(converse(X1)) ),
% 1.72/2.12 inference(cp,[status(thm)],['0.30.2.0','0.1.2.0',theory(equality)]),
% 1.72/2.12 [pos('L.1','L')]).
% 1.72/2.12 cnf('0.31.0.1',plain,
% 1.72/2.12 ( composition(converse(one),X1) = X1 ),
% 1.72/2.12 inference(reduction,[status(thm)],['0.31.0.0','0.3.2.0',theory(equality)]),
% 1.72/2.12 [pos('R','L')]).
% 1.72/2.12 cnf('0.31.1.0',plain,
% 1.72/2.12 ( composition(converse(one),X1) = X1 ),
% 1.72/2.12 inference(weigh,[status(thm)],['0.31.0.1']),
% 1.72/2.12 [weight('<29,30,1,[1,0,0,1]>')]).
% 1.72/2.12 cnf('0.31.2.0',plain,
% 1.72/2.12 ( composition(converse(one),X1) = X1 ),
% 1.72/2.12 inference(orient,[status(thm)],['0.31.1.0',theory(equality)]),
% 1.72/2.12 [u,rule_29]).
% 1.72/2.12 cnf('0.32.0.0',plain,
% 1.72/2.12 ( one = converse(one) ),
% 1.72/2.12 inference(cp,[status(thm)],['0.31.2.0','0.1.2.0',theory(equality)]),
% 1.72/2.12 [pos('L','L')]).
% 1.72/2.12 cnf('0.32.1.0',plain,
% 1.72/2.12 ( one = converse(one) ),
% 1.72/2.12 inference(weigh,[status(thm)],['0.32.0.0']),
% 1.72/2.12 [weight('<11,31,1,[1,0,0,0]>')]).
% 1.72/2.12 cnf('0.32.2.0',plain,
% 1.72/2.12 ( converse(one) = one ),
% 1.72/2.12 inference(orient,[status(thm)],['0.32.1.0',theory(equality)]),
% 1.72/2.12 [x,rule_30]).
% 1.72/2.12 cnf('0.33.0.0',plain,
% 1.72/2.12 ( composition(converse(one),X1) = X1 ),
% 1.72/2.12 inference(interreduction_right,[status(thm)],['0.31.2.0'])).
% 1.72/2.12 cnf('0.33.0.1',plain,
% 1.72/2.12 ( composition(one,X1) = X1 ),
% 1.72/2.12 inference(reduction,[status(thm)],['0.33.0.0','0.32.2.0',theory(equality)]),
% 1.72/2.12 [pos('L.1','L')]).
% 1.72/2.12 cnf('0.33.1.0',plain,
% 1.72/2.12 ( composition(one,X1) = X1 ),
% 1.72/2.12 inference(weigh,[status(thm)],['0.33.0.1']),
% 1.72/2.12 [weight('<19,31,32,[0,0,0,0]>')]).
% 1.72/2.12 cnf('0.33.2.0',plain,
% 1.72/2.12 ( composition(one,X1) = X1 ),
% 1.72/2.12 inference(orient,[status(thm)],['0.33.1.0',theory(equality)]),
% 1.72/2.12 [u,rule_31]).
% 1.72/2.12 cnf('0.34.0.0',plain,
% 1.72/2.12 ( converse(join(one,X1)) = join(one,converse(X1)) ),
% 1.72/2.12 inference(cp,[status(thm)],['0.14.2.0','0.32.2.0',theory(equality)]),
% 1.72/2.12 [pos('L.1','L')]).
% 1.72/2.12 cnf('0.34.1.0',plain,
% 1.72/2.12 ( converse(join(one,X1)) = join(one,converse(X1)) ),
% 1.72/2.12 inference(weigh,[status(thm)],['0.34.0.0']),
% 1.72/2.12 [weight('<44,32,14,[0,0,0,1]>')]).
% 1.72/2.12 cnf('0.34.2.0',plain,
% 1.72/2.12 ( converse(join(one,X1)) = join(one,converse(X1)) ),
% 1.72/2.12 inference(orient,[status(thm)],['0.34.1.0',theory(equality)]),
% 1.72/2.12 [u,rule_32]).
% 1.72/2.12 cnf('0.36.0.0',plain,
% 1.72/2.12 ( complement(X1) = join(complement(X1),composition(converse(one),complement(X1))) ),
% 1.72/2.12 inference(cp,[status(thm)],['0.11.2.0','0.33.2.0',theory(equality)]),
% 1.72/2.12 [pos('L.2.2.1','L')]).
% 1.72/2.12 cnf('0.36.0.1',plain,
% 1.72/2.12 ( complement(X1) = join(complement(X1),composition(one,complement(X1))) ),
% 1.72/2.12 inference(reduction,[status(thm)],['0.36.0.0','0.32.2.0',theory(equality)]),
% 1.72/2.12 [pos('R.2.1','L')]).
% 1.72/2.12 cnf('0.36.0.2',plain,
% 1.72/2.12 ( complement(X1) = join(complement(X1),complement(X1)) ),
% 1.72/2.12 inference(reduction,[status(thm)],['0.36.0.1','0.33.2.0',theory(equality)]),
% 1.72/2.12 [pos('R.2','L')]).
% 1.72/2.12 cnf('0.36.1.0',plain,
% 1.72/2.12 ( complement(X1) = join(complement(X1),complement(X1)) ),
% 1.72/2.12 inference(weigh,[status(thm)],['0.36.0.2']),
% 1.72/2.12 [weight('<47,33,11,[0,0,0,7]>')]).
% 1.72/2.12 cnf('0.36.2.0',plain,
% 1.72/2.12 ( join(complement(X1),complement(X1)) = complement(X1) ),
% 1.72/2.12 inference(orient,[status(thm)],['0.36.1.0',theory(equality)]),
% 1.72/2.12 [x,rule_34]).
% 1.72/2.12 cnf('0.37.0.0',plain,
% 1.72/2.12 ( complement(top) = join(zero,complement(top)) ),
% 1.72/2.12 inference(cp,[status(thm)],['0.36.2.0','0.18.2.0',theory(equality)]),
% 1.72/2.12 [pos('L.1','L')]).
% 1.72/2.12 cnf('0.37.0.1',plain,
% 1.72/2.12 ( zero = join(zero,complement(top)) ),
% 1.72/2.12 inference(reduction,[status(thm)],['0.37.0.0','0.18.2.0',theory(equality)]),
% 1.72/2.12 [pos('L','L')]).
% 1.72/2.12 cnf('0.37.0.2',plain,
% 1.72/2.12 ( zero = join(zero,zero) ),
% 1.72/2.12 inference(reduction,[status(thm)],['0.37.0.1','0.18.2.0',theory(equality)]),
% 1.72/2.12 [pos('R.2','L')]).
% 1.72/2.12 cnf('0.37.1.0',plain,
% 1.72/2.12 ( zero = join(zero,zero) ),
% 1.72/2.12 inference(weigh,[status(thm)],['0.37.0.2']),
% 1.72/2.12 [weight('<19,36,18,[1,0,0,1]>')]).
% 1.72/2.12 cnf('0.37.2.0',plain,
% 1.72/2.12 ( join(zero,zero) = zero ),
% 1.72/2.12 inference(orient,[status(thm)],['0.37.1.0',theory(equality)]),
% 1.72/2.12 [x,rule_35]).
% 1.72/2.12 cnf('0.40.0.0',plain,
% 1.72/2.12 ( meet(X1,X1) = complement(complement(X1)) ),
% 1.72/2.12 inference(cp,[status(thm)],['0.15.2.0','0.36.2.0',theory(equality)]),
% 1.72/2.12 [pos('L.1','L')]).
% 1.72/2.12 cnf('0.40.1.0',plain,
% 1.72/2.12 ( meet(X1,X1) = complement(complement(X1)) ),
% 1.72/2.12 inference(weigh,[status(thm)],['0.40.0.0']),
% 1.72/2.12 [weight('<48,36,15,[0,0,0,1]>')]).
% 1.72/2.12 cnf('0.40.2.0',plain,
% 1.72/2.12 ( meet(X1,X1) = complement(complement(X1)) ),
% 1.72/2.12 inference(activate,[status(thm)],['0.40.1.0']),
% 1.72/2.12 [equation_3]).
% 1.72/2.12 cnf('0.41.0.0',plain,
% 1.72/2.12 ( join(zero,join(zero,X1)) = join(zero,X1) ),
% 1.72/2.12 inference(cp,[status(thm)],['0.9.2.0','0.37.2.0',theory(equality)]),
% 1.72/2.12 [pos('L.1','L')]).
% 1.72/2.12 cnf('0.41.1.0',plain,
% 1.72/2.12 ( join(zero,join(zero,X1)) = join(zero,X1) ),
% 1.72/2.12 inference(weigh,[status(thm)],['0.41.0.0']),
% 1.72/2.12 [weight('<53,37,9,[0,0,0,1]>')]).
% 1.72/2.12 cnf('0.41.2.0',plain,
% 1.72/2.12 ( join(zero,join(zero,X1)) = join(zero,X1) ),
% 1.72/2.12 inference(orient,[status(thm)],['0.41.1.0',theory(equality)]),
% 1.72/2.12 [u,rule_38]).
% 1.72/2.12 cnf('0.42.0.0',plain,
% 1.72/2.12 ( join(zero,X1) = join(zero,join(X1,zero)) ),
% 1.72/2.12 inference(cp,[status(thm)],['0.41.2.0','0.8.2.0',theory(equality)]),
% 1.72/2.12 [pos('L.2','L')]).
% 1.72/2.12 cnf('0.42.1.0',plain,
% 1.72/2.12 ( join(zero,X1) = join(zero,join(X1,zero)) ),
% 1.72/2.12 inference(weigh,[status(thm)],['0.42.0.0']),
% 1.72/2.12 [weight('<53,41,8,[1,0,0,2]>')]).
% 1.72/2.12 cnf('0.42.2.0',plain,
% 1.72/2.12 ( join(zero,join(X1,zero)) = join(zero,X1) ),
% 1.72/2.12 inference(orient,[status(thm)],['0.42.1.0',theory(equality)]),
% 1.72/2.12 [x,rule_39]).
% 1.72/2.12 cnf('0.45.0.0',plain,
% 1.72/2.12 ( converse(join(converse(X1),X2)) = join(X1,converse(X2)) ),
% 1.72/2.12 inference(cp,[status(thm)],['0.14.2.0','0.3.2.0',theory(equality)]),
% 1.72/2.12 [pos('L.1','L')]).
% 1.72/2.12 cnf('0.45.1.0',plain,
% 1.72/2.12 ( converse(join(converse(X1),X2)) = join(X1,converse(X2)) ),
% 1.72/2.12 inference(weigh,[status(thm)],['0.45.0.0']),
% 1.72/2.12 [weight('<59,14,3,[1,0,0,1]>')]).
% 1.72/2.12 cnf('0.45.2.0',plain,
% 1.72/2.12 ( converse(join(converse(X1),X2)) = join(X1,converse(X2)) ),
% 1.72/2.12 inference(orient,[status(thm)],['0.45.1.0',theory(equality)]),
% 1.72/2.12 [u,rule_42]).
% 1.72/2.12 cnf('0.46.0.0',plain,
% 1.72/2.12 ( converse(join(X1,converse(X2))) = join(converse(X1),X2) ),
% 1.72/2.12 inference(cp,[status(thm)],['0.14.2.0','0.3.2.0',theory(equality)]),
% 1.72/2.12 [pos('L.2','L')]).
% 1.72/2.12 cnf('0.46.1.0',plain,
% 1.72/2.12 ( converse(join(X1,converse(X2))) = join(converse(X1),X2) ),
% 1.72/2.12 inference(weigh,[status(thm)],['0.46.0.0']),
% 1.72/2.12 [weight('<59,14,3,[1,0,0,3]>')]).
% 1.72/2.12 cnf('0.46.2.0',plain,
% 1.72/2.12 ( converse(join(X1,converse(X2))) = join(converse(X1),X2) ),
% 1.72/2.12 inference(orient,[status(thm)],['0.46.1.0',theory(equality)]),
% 1.72/2.12 [u,rule_43]).
% 1.72/2.12 cnf('0.47.0.0',plain,
% 1.72/2.12 ( join(X1,converse(complement(converse(X1)))) = converse(top) ),
% 1.72/2.12 inference(cp,[status(thm)],['0.45.2.0','0.10.2.0',theory(equality)]),
% 1.72/2.12 [pos('L.1','L')]).
% 1.72/2.12 cnf('0.47.1.0',plain,
% 1.72/2.12 ( join(X1,converse(complement(converse(X1)))) = converse(top) ),
% 1.72/2.12 inference(weigh,[status(thm)],['0.47.0.0']),
% 1.72/2.12 [weight('<62,45,10,[1,0,0,1]>')]).
% 1.72/2.12 cnf('0.47.2.0',plain,
% 1.72/2.12 ( join(X1,converse(complement(converse(X1)))) = converse(top) ),
% 1.72/2.12 inference(orient,[status(thm)],['0.47.1.0',theory(equality)]),
% 1.72/2.12 [u,rule_44]).
% 1.72/2.12 cnf('0.50.0.0',plain,
% 1.72/2.12 ( join(X1,join(complement(X1),X2)) = join(top,X2) ),
% 1.72/2.12 inference(cp,[status(thm)],['0.9.2.0','0.10.2.0',theory(equality)]),
% 1.72/2.12 [pos('L.1','L')]).
% 1.72/2.12 cnf('0.50.1.0',plain,
% 1.72/2.12 ( join(X1,join(complement(X1),X2)) = join(top,X2) ),
% 1.72/2.12 inference(weigh,[status(thm)],['0.50.0.0']),
% 1.72/2.12 [weight('<69,10,9,[0,0,0,1]>')]).
% 1.72/2.12 cnf('0.50.2.0',plain,
% 1.72/2.12 ( join(X1,join(complement(X1),X2)) = join(top,X2) ),
% 1.72/2.12 inference(orient,[status(thm)],['0.50.1.0',theory(equality)]),
% 1.72/2.12 [u,rule_47]).
% 1.72/2.12 cnf('0.51.0.0',plain,
% 1.72/2.12 ( join(top,complement(X1)) = join(X1,complement(X1)) ),
% 1.72/2.12 inference(cp,[status(thm)],['0.50.2.0','0.36.2.0',theory(equality)]),
% 1.72/2.12 [pos('L.2','L')]).
% 1.72/2.12 cnf('0.51.0.1',plain,
% 1.72/2.12 ( join(top,complement(X1)) = top ),
% 1.72/2.12 inference(reduction,[status(thm)],['0.51.0.0','0.10.2.0',theory(equality)]),
% 1.72/2.12 [pos('R','L')]).
% 1.72/2.12 cnf('0.51.1.0',plain,
% 1.72/2.12 ( join(top,complement(X1)) = top ),
% 1.72/2.12 inference(weigh,[status(thm)],['0.51.0.1']),
% 1.72/2.12 [weight('<29,50,36,[1,0,0,2]>')]).
% 1.72/2.12 cnf('0.51.2.0',plain,
% 1.72/2.12 ( join(top,complement(X1)) = top ),
% 1.72/2.12 inference(orient,[status(thm)],['0.51.1.0',theory(equality)]),
% 1.72/2.12 [u,rule_48]).
% 1.72/2.12 cnf('0.54.0.0',plain,
% 1.72/2.12 ( join(top,complement(complement(X1))) = join(X1,top) ),
% 1.72/2.12 inference(cp,[status(thm)],['0.50.2.0','0.10.2.0',theory(equality)]),
% 1.72/2.12 [pos('L.2','L')]).
% 1.72/2.12 cnf('0.54.1.0',plain,
% 1.72/2.12 ( join(top,complement(complement(X1))) = join(X1,top) ),
% 1.72/2.12 inference(weigh,[status(thm)],['0.54.0.0']),
% 1.72/2.12 [weight('<53,50,10,[1,0,0,2]>')]).
% 1.72/2.12 cnf('0.54.1.1',plain,
% 1.72/2.12 ( top = join(X1,top) ),
% 1.72/2.12 inference(reduction,[status(thm)],['0.54.1.0','0.51.2.0',theory(equality)]),
% 1.72/2.12 [pos('L','L')]).
% 1.72/2.12 cnf('0.54.2.0',plain,
% 1.72/2.12 ( join(X1,top) = top ),
% 1.72/2.12 inference(orient,[status(thm)],['0.54.1.1',theory(equality)]),
% 1.72/2.12 [x,rule_51]).
% 1.72/2.12 cnf('0.55.0.0',plain,
% 1.72/2.12 ( top = join(top,X1) ),
% 1.72/2.12 inference(cp,[status(thm)],['0.54.2.0','0.8.2.0',theory(equality)]),
% 1.72/2.12 [pos('L','L')]).
% 1.72/2.12 cnf('0.55.1.0',plain,
% 1.72/2.12 ( top = join(top,X1) ),
% 1.72/2.12 inference(weigh,[status(thm)],['0.55.0.0']),
% 1.72/2.12 [weight('<19,54,8,[1,0,0,0]>')]).
% 1.72/2.12 cnf('0.55.2.0',plain,
% 1.72/2.12 ( join(top,X1) = top ),
% 1.72/2.12 inference(orient,[status(thm)],['0.55.1.0',theory(equality)]),
% 1.72/2.12 [x,rule_52]).
% 1.72/2.12 cnf('0.56.0.0',plain,
% 1.72/2.12 ( top = converse(top) ),
% 1.72/2.12 inference(cp,[status(thm)],['0.55.2.0','0.47.2.0',theory(equality)]),
% 1.72/2.12 [pos('L','L')]).
% 1.72/2.12 cnf('0.56.1.0',plain,
% 1.72/2.12 ( top = converse(top) ),
% 1.72/2.12 inference(weigh,[status(thm)],['0.56.0.0']),
% 1.72/2.12 [weight('<11,55,47,[1,0,0,0]>')]).
% 1.72/2.12 cnf('0.56.2.0',plain,
% 1.72/2.12 ( converse(top) = top ),
% 1.72/2.12 inference(orient,[status(thm)],['0.56.1.0',theory(equality)]),
% 1.72/2.12 [x,rule_53]).
% 1.72/2.12 cnf('0.58.0.0',plain,
% 1.72/2.12 ( converse(composition(X1,top)) = composition(top,converse(X1)) ),
% 1.72/2.12 inference(cp,[status(thm)],['0.7.2.0','0.56.2.0',theory(equality)]),
% 1.72/2.12 [pos('L.1','L')]).
% 1.72/2.12 cnf('0.58.1.0',plain,
% 1.72/2.12 ( converse(composition(X1,top)) = composition(top,converse(X1)) ),
% 1.72/2.12 inference(weigh,[status(thm)],['0.58.0.0']),
% 1.72/2.12 [weight('<44,56,7,[0,0,0,1]>')]).
% 1.72/2.12 cnf('0.58.2.0',plain,
% 1.72/2.12 ( converse(composition(X1,top)) = composition(top,converse(X1)) ),
% 1.72/2.12 inference(orient,[status(thm)],['0.58.1.0',theory(equality)]),
% 1.72/2.12 [u,rule_55]).
% 1.72/2.12 cnf('0.59.0.0',plain,
% 1.72/2.12 ( converse(composition(top,X1)) = composition(converse(X1),top) ),
% 1.72/2.12 inference(cp,[status(thm)],['0.7.2.0','0.56.2.0',theory(equality)]),
% 1.72/2.12 [pos('L.2','L')]).
% 1.72/2.12 cnf('0.59.1.0',plain,
% 1.72/2.12 ( converse(composition(top,X1)) = composition(converse(X1),top) ),
% 1.72/2.12 inference(weigh,[status(thm)],['0.59.0.0']),
% 1.72/2.12 [weight('<44,56,7,[0,0,0,3]>')]).
% 1.72/2.12 cnf('0.59.2.0',plain,
% 1.72/2.12 ( converse(composition(top,X1)) = composition(converse(X1),top) ),
% 1.72/2.12 inference(orient,[status(thm)],['0.59.1.0',theory(equality)]),
% 1.72/2.12 [u,rule_56]).
% 1.72/2.12 cnf('0.60.0.0',plain,
% 1.72/2.12 ( join(X1,converse(complement(converse(X1)))) = converse(top) ),
% 1.72/2.12 inference(interreduction_right,[status(thm)],['0.47.2.0'])).
% 1.72/2.12 cnf('0.60.0.1',plain,
% 1.72/2.12 ( join(X1,converse(complement(converse(X1)))) = top ),
% 1.72/2.12 inference(reduction,[status(thm)],['0.60.0.0','0.56.2.0',theory(equality)]),
% 1.72/2.12 [pos('R','L')]).
% 1.72/2.12 cnf('0.60.1.0',plain,
% 1.72/2.12 ( join(X1,converse(complement(converse(X1)))) = top ),
% 1.72/2.12 inference(weigh,[status(thm)],['0.60.0.1']),
% 1.72/2.12 [weight('<55,47,56,[0,0,0,0]>')]).
% 1.72/2.12 cnf('0.60.2.0',plain,
% 1.72/2.12 ( join(X1,converse(complement(converse(X1)))) = top ),
% 1.72/2.12 inference(orient,[status(thm)],['0.60.1.0',theory(equality)]),
% 1.72/2.12 [u,rule_57]).
% 1.72/2.12 cnf('0.61.0.0',axiom,
% 1.72/2.12 ( X1 = join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) ),
% 1.72/2.12 file('/tmp/WALDMEISTER_7164_n015')).
% 1.72/2.12 cnf('0.61.1.0',plain,
% 1.72/2.12 ( X1 = join(complement(join(complement(X1),complement(X2))),complement(join(complement(X1),X2))) ),
% 1.72/2.12 inference(weigh,[status(thm)],['0.61.0.0']),
% 1.72/2.12 [weight('<0,0,0,[0,0,0,2]>')]).
% 1.72/2.12 cnf('0.61.1.1',plain,
% 1.72/2.12 ( X1 = join(complement(join(complement(X1),X2)),complement(join(complement(X1),complement(X2)))) ),
% 1.72/2.12 inference(reduction,[status(thm)],['0.61.1.0','0.8.2.0',theory(equality)]),
% 1.72/2.12 [pos('R','L')]).
% 1.72/2.12 cnf('0.61.1.2',plain,
% 1.72/2.12 ( X1 = join(complement(join(complement(X1),X2)),meet(X1,X2)) ),
% 1.72/2.12 inference(reduction,[status(thm)],['0.61.1.1','0.15.2.0',theory(equality)]),
% 1.72/2.12 [pos('R.2','L')]).
% 1.72/2.12 cnf('0.61.1.3',plain,
% 1.72/2.12 ( X1 = join(meet(X1,X2),complement(join(complement(X1),X2))) ),
% 1.72/2.12 inference(reduction,[status(thm)],['0.61.1.2','0.8.2.0',theory(equality)]),
% 1.72/2.12 [pos('R','L')]).
% 1.72/2.12 cnf('0.61.2.0',plain,
% 1.72/2.12 ( join(meet(X1,X2),complement(join(complement(X1),X2))) = X1 ),
% 1.72/2.12 inference(orient,[status(thm)],['0.61.1.3',theory(equality)]),
% 1.72/2.12 [x,rule_58]).
% 1.72/2.12 cnf('0.62.0.0',plain,
% 1.72/2.12 ( X1 = join(zero,complement(join(complement(X1),complement(X1)))) ),
% 1.72/2.12 inference(cp,[status(thm)],['0.61.2.0','0.16.2.0',theory(equality)]),
% 1.72/2.12 [pos('L.1','L')]).
% 1.72/2.12 cnf('0.62.0.1',plain,
% 1.72/2.12 ( X1 = join(zero,meet(X1,X1)) ),
% 1.72/2.12 inference(reduction,[status(thm)],['0.62.0.0','0.15.2.0',theory(equality)]),
% 1.72/2.12 [pos('R.2','L')]).
% 1.72/2.12 cnf('0.62.1.0',plain,
% 1.72/2.12 ( X1 = join(zero,meet(X1,X1)) ),
% 1.72/2.12 inference(weigh,[status(thm)],['0.62.0.1']),
% 1.72/2.12 [weight('<41,61,16,[1,0,0,1]>')]).
% 1.72/2.12 cnf('0.62.2.0',plain,
% 1.72/2.12 ( join(zero,meet(X1,X1)) = X1 ),
% 1.72/2.12 inference(orient,[status(thm)],['0.62.1.0',theory(equality)]),
% 1.72/2.12 [x,rule_59]).
% 1.72/2.12 cnf('0.63.0.0',plain,
% 1.72/2.12 ( join(zero,meet(X1,X1)) = join(zero,X1) ),
% 1.72/2.12 inference(cp,[status(thm)],['0.41.2.0','0.62.2.0',theory(equality)]),
% 1.72/2.12 [pos('L.2','L')]).
% 1.72/2.12 cnf('0.63.0.1',plain,
% 1.72/2.12 ( X1 = join(zero,X1) ),
% 1.72/2.12 inference(reduction,[status(thm)],['0.63.0.0','0.62.2.0',theory(equality)]),
% 1.72/2.12 [pos('L','L')]).
% 1.72/2.12 cnf('0.63.1.0',plain,
% 1.72/2.12 ( X1 = join(zero,X1) ),
% 1.72/2.12 inference(weigh,[status(thm)],['0.63.0.1']),
% 1.72/2.12 [weight('<19,62,41,[0,0,0,2]>')]).
% 1.72/2.12 cnf('0.63.2.0',plain,
% 1.72/2.12 ( join(zero,X1) = X1 ),
% 1.72/2.12 inference(orient,[status(thm)],['0.63.1.0',theory(equality)]),
% 1.72/2.12 [x,rule_60]).
% 1.72/2.12 cnf('0.64.0.0',plain,
% 1.72/2.12 ( complement(zero) = top ),
% 1.72/2.12 inference(cp,[status(thm)],['0.63.2.0','0.10.2.0',theory(equality)]),
% 1.72/2.12 [pos('L','L')]).
% 1.72/2.12 cnf('0.64.1.0',plain,
% 1.72/2.12 ( complement(zero) = top ),
% 1.72/2.12 inference(weigh,[status(thm)],['0.64.0.0']),
% 1.72/2.12 [weight('<11,63,10,[1,0,0,0]>')]).
% 1.72/2.12 cnf('0.64.2.0',plain,
% 1.72/2.12 ( complement(zero) = top ),
% 1.72/2.12 inference(orient,[status(thm)],['0.64.1.0',theory(equality)]),
% 1.72/2.12 [u,rule_61]).
% 1.72/2.12 cnf('0.66.0.0',plain,
% 1.72/2.12 ( join(zero,join(X1,zero)) = join(zero,X1) ),
% 1.72/2.12 inference(interreduction_right,[status(thm)],['0.42.2.0'])).
% 1.72/2.12 cnf('0.66.0.1',plain,
% 1.72/2.12 ( join(X1,zero) = join(zero,X1) ),
% 1.72/2.12 inference(reduction,[status(thm)],['0.66.0.0','0.63.2.0',theory(equality)]),
% 1.72/2.12 [pos('L','L')]).
% 1.72/2.12 cnf('0.66.0.2',plain,
% 1.72/2.12 ( join(X1,zero) = X1 ),
% 1.72/2.12 inference(reduction,[status(thm)],['0.66.0.1','0.63.2.0',theory(equality)]),
% 1.72/2.12 [pos('R','L')]).
% 1.72/2.12 cnf('0.66.1.0',plain,
% 1.72/2.12 ( join(X1,zero) = X1 ),
% 1.72/2.12 inference(weigh,[status(thm)],['0.66.0.2']),
% 1.72/2.12 [weight('<19,42,63,[0,0,0,0]>')]).
% 1.72/2.12 cnf('0.66.2.0',plain,
% 1.72/2.12 ( join(X1,zero) = X1 ),
% 1.72/2.12 inference(orient,[status(thm)],['0.66.1.0',theory(equality)]),
% 1.72/2.12 [u,rule_63]).
% 1.72/2.12 cnf('0.67.0.0',plain,
% 1.72/2.12 ( join(zero,meet(X1,X1)) = X1 ),
% 1.72/2.12 inference(interreduction_right,[status(thm)],['0.62.2.0'])).
% 1.72/2.12 cnf('0.67.0.1',plain,
% 1.72/2.12 ( meet(X1,X1) = X1 ),
% 1.72/2.12 inference(reduction,[status(thm)],['0.67.0.0','0.63.2.0',theory(equality)]),
% 1.72/2.12 [pos('L','L')]).
% 1.72/2.12 cnf('0.67.1.0',plain,
% 1.72/2.12 ( meet(X1,X1) = X1 ),
% 1.72/2.12 inference(weigh,[status(thm)],['0.67.0.1']),
% 1.72/2.12 [weight('<19,62,63,[0,0,0,0]>')]).
% 1.72/2.12 cnf('0.67.2.0',plain,
% 1.72/2.12 ( meet(X1,X1) = X1 ),
% 1.72/2.12 inference(orient,[status(thm)],['0.67.1.0',theory(equality)]),
% 1.72/2.12 [u,rule_64]).
% 1.72/2.12 cnf('0.68.0.0',plain,
% 1.72/2.12 ( meet(X1,X1) = complement(complement(X1)) ),
% 1.72/2.12 inference(interreduction_right,[status(thm)],['0.40.2.0'])).
% 1.72/2.12 cnf('0.68.0.1',plain,
% 1.72/2.12 ( X1 = complement(complement(X1)) ),
% 1.72/2.12 inference(reduction,[status(thm)],['0.68.0.0','0.67.2.0',theory(equality)]),
% 1.72/2.12 [pos('L','L')]).
% 1.72/2.12 cnf('0.68.1.0',plain,
% 1.72/2.12 ( X1 = complement(complement(X1)) ),
% 1.72/2.12 inference(weigh,[status(thm)],['0.68.0.1']),
% 1.72/2.12 [weight('<19,40,67,[0,0,0,0]>')]).
% 1.72/2.12 cnf('0.68.2.0',plain,
% 1.72/2.12 ( complement(complement(X1)) = X1 ),
% 1.72/2.12 inference(orient,[status(thm)],['0.68.1.0',theory(equality)]),
% 1.72/2.12 [x,rule_65]).
% 1.72/2.12 cnf('0.69.0.0',plain,
% 1.72/2.12 ( meet(zero,X1) = complement(join(top,complement(X1))) ),
% 1.72/2.12 inference(cp,[status(thm)],['0.15.2.0','0.64.2.0',theory(equality)]),
% 1.72/2.12 [pos('L.1.1','L')]).
% 1.72/2.12 cnf('0.69.0.1',plain,
% 1.72/2.12 ( meet(zero,X1) = complement(top) ),
% 1.72/2.12 inference(reduction,[status(thm)],['0.69.0.0','0.55.2.0',theory(equality)]),
% 1.72/2.12 [pos('R.1','L')]).
% 1.72/2.12 cnf('0.69.0.2',plain,
% 1.72/2.12 ( meet(zero,X1) = zero ),
% 1.72/2.12 inference(reduction,[status(thm)],['0.69.0.1','0.18.2.0',theory(equality)]),
% 1.72/2.12 [pos('R','L')]).
% 1.72/2.12 cnf('0.69.1.0',plain,
% 1.72/2.12 ( meet(zero,X1) = zero ),
% 1.72/2.12 inference(weigh,[status(thm)],['0.69.0.2']),
% 1.72/2.12 [weight('<19,64,15,[0,0,0,2]>')]).
% 1.72/2.12 cnf('0.69.2.0',plain,
% 1.72/2.12 ( meet(zero,X1) = zero ),
% 1.72/2.12 inference(orient,[status(thm)],['0.69.1.0',theory(equality)]),
% 1.72/2.12 [u,rule_66]).
% 1.72/2.12 cnf('0.70.0.0',plain,
% 1.72/2.12 ( meet(X1,zero) = complement(join(complement(X1),top)) ),
% 1.72/2.12 inference(cp,[status(thm)],['0.15.2.0','0.64.2.0',theory(equality)]),
% 1.72/2.12 [pos('L.1.2','L')]).
% 1.72/2.12 cnf('0.70.0.1',plain,
% 1.72/2.12 ( meet(X1,zero) = complement(top) ),
% 1.72/2.12 inference(reduction,[status(thm)],['0.70.0.0','0.54.2.0',theory(equality)]),
% 1.72/2.12 [pos('R.1','L')]).
% 1.72/2.12 cnf('0.70.0.2',plain,
% 1.72/2.12 ( meet(X1,zero) = zero ),
% 1.72/2.12 inference(reduction,[status(thm)],['0.70.0.1','0.18.2.0',theory(equality)]),
% 1.72/2.12 [pos('R','L')]).
% 1.72/2.12 cnf('0.70.1.0',plain,
% 1.72/2.12 ( meet(X1,zero) = zero ),
% 1.72/2.12 inference(weigh,[status(thm)],['0.70.0.2']),
% 1.72/2.12 [weight('<19,64,15,[0,0,0,4]>')]).
% 1.72/2.12 cnf('0.70.2.0',plain,
% 1.72/2.12 ( meet(X1,zero) = zero ),
% 1.72/2.12 inference(orient,[status(thm)],['0.70.1.0',theory(equality)]),
% 1.72/2.12 [u,rule_67]).
% 1.72/2.12 cnf('0.71.0.0',plain,
% 1.72/2.12 ( complement(complement(X1)) = join(X1,complement(complement(X1))) ),
% 1.72/2.12 inference(cp,[status(thm)],['0.36.2.0','0.68.2.0',theory(equality)]),
% 1.72/2.12 [pos('L.1','L')]).
% 1.72/2.12 cnf('0.71.0.1',plain,
% 1.72/2.12 ( X1 = join(X1,complement(complement(X1))) ),
% 1.72/2.12 inference(reduction,[status(thm)],['0.71.0.0','0.68.2.0',theory(equality)]),
% 1.72/2.12 [pos('L','L')]).
% 1.72/2.12 cnf('0.71.0.2',plain,
% 1.72/2.12 ( X1 = join(X1,X1) ),
% 1.72/2.12 inference(reduction,[status(thm)],['0.71.0.1','0.68.2.0',theory(equality)]),
% 1.72/2.12 [pos('R.2','L')]).
% 1.72/2.12 cnf('0.71.1.0',plain,
% 1.72/2.12 ( X1 = join(X1,X1) ),
% 1.72/2.12 inference(weigh,[status(thm)],['0.71.0.2']),
% 1.72/2.12 [weight('<19,68,36,[0,0,0,1]>')]).
% 1.72/2.12 cnf('0.71.2.0',plain,
% 1.72/2.12 ( join(X1,X1) = X1 ),
% 1.72/2.12 inference(orient,[status(thm)],['0.71.1.0',theory(equality)]),
% 1.72/2.12 [x,rule_68]).
% 1.72/2.12 cnf('0.72.0.0',plain,
% 1.72/2.12 ( complement(join(zero,complement(X1))) = meet(top,X1) ),
% 1.72/2.12 inference(interreduction_right,[status(thm)],['0.23.2.0'])).
% 1.72/2.12 cnf('0.72.0.1',plain,
% 1.72/2.12 ( complement(complement(X1)) = meet(top,X1) ),
% 1.72/2.12 inference(reduction,[status(thm)],['0.72.0.0','0.63.2.0',theory(equality)]),
% 1.72/2.12 [pos('L.1','L')]).
% 1.72/2.12 cnf('0.72.1.0',plain,
% 1.72/2.12 ( complement(complement(X1)) = meet(top,X1) ),
% 1.72/2.12 inference(weigh,[status(thm)],['0.72.0.1']),
% 1.72/2.12 [weight('<27,23,63,[0,0,0,0]>')]).
% 1.72/2.12 cnf('0.72.1.1',plain,
% 1.72/2.12 ( X1 = meet(top,X1) ),
% 1.72/2.12 inference(reduction,[status(thm)],['0.72.1.0','0.68.2.0',theory(equality)]),
% 1.72/2.12 [pos('L','L')]).
% 1.72/2.12 cnf('0.72.2.0',plain,
% 1.72/2.12 ( meet(top,X1) = X1 ),
% 1.72/2.12 inference(orient,[status(thm)],['0.72.1.1',theory(equality)]),
% 1.72/2.12 [x,rule_69]).
% 1.72/2.12 cnf('0.73.0.0',plain,
% 1.72/2.12 ( X1 = meet(X1,top) ),
% 1.72/2.12 inference(cp,[status(thm)],['0.72.2.0','0.21.2.0',theory(equality)]),
% 1.72/2.12 [pos('L','L')]).
% 1.72/2.12 cnf('0.73.1.0',plain,
% 1.72/2.12 ( X1 = meet(X1,top) ),
% 1.72/2.12 inference(weigh,[status(thm)],['0.73.0.0']),
% 1.72/2.12 [weight('<19,72,21,[1,0,0,0]>')]).
% 1.72/2.12 cnf('0.73.2.0',plain,
% 1.72/2.12 ( meet(X1,top) = X1 ),
% 1.72/2.12 inference(orient,[status(thm)],['0.73.1.0',theory(equality)]),
% 1.72/2.12 [x,rule_70]).
% 1.72/2.12 cnf('0.75.0.0',plain,
% 1.72/2.12 ( join(converse(zero),X1) = converse(converse(X1)) ),
% 1.72/2.12 inference(cp,[status(thm)],['0.46.2.0','0.63.2.0',theory(equality)]),
% 1.72/2.12 [pos('L.1','L')]).
% 1.72/2.12 cnf('0.75.0.1',plain,
% 1.72/2.12 ( join(converse(zero),X1) = X1 ),
% 1.72/2.12 inference(reduction,[status(thm)],['0.75.0.0','0.3.2.0',theory(equality)]),
% 1.72/2.12 [pos('R','L')]).
% 1.72/2.12 cnf('0.75.1.0',plain,
% 1.72/2.12 ( join(converse(zero),X1) = X1 ),
% 1.72/2.12 inference(weigh,[status(thm)],['0.75.0.1']),
% 1.72/2.12 [weight('<29,63,46,[0,0,0,1]>')]).
% 1.72/2.12 cnf('0.75.2.0',plain,
% 1.72/2.12 ( join(converse(zero),X1) = X1 ),
% 1.72/2.12 inference(orient,[status(thm)],['0.75.1.0',theory(equality)]),
% 1.72/2.12 [u,rule_72]).
% 1.72/2.12 cnf('0.76.0.0',plain,
% 1.72/2.12 ( zero = converse(zero) ),
% 1.72/2.12 inference(cp,[status(thm)],['0.75.2.0','0.66.2.0',theory(equality)]),
% 1.72/2.12 [pos('L','L')]).
% 1.72/2.12 cnf('0.76.1.0',plain,
% 1.72/2.12 ( zero = converse(zero) ),
% 1.72/2.12 inference(weigh,[status(thm)],['0.76.0.0']),
% 1.72/2.12 [weight('<11,75,66,[1,0,0,0]>')]).
% 1.72/2.12 cnf('0.76.2.0',plain,
% 1.72/2.12 ( converse(zero) = zero ),
% 1.72/2.12 inference(orient,[status(thm)],['0.76.1.0',theory(equality)]),
% 1.72/2.12 [x,rule_73]).
% 1.72/2.12 cnf('0.77.0.0',plain,
% 1.72/2.12 ( converse(composition(X1,zero)) = composition(zero,converse(X1)) ),
% 1.72/2.12 inference(cp,[status(thm)],['0.7.2.0','0.76.2.0',theory(equality)]),
% 1.72/2.12 [pos('L.1','L')]).
% 1.72/2.12 cnf('0.77.1.0',plain,
% 1.72/2.12 ( converse(composition(X1,zero)) = composition(zero,converse(X1)) ),
% 1.72/2.12 inference(weigh,[status(thm)],['0.77.0.0']),
% 1.72/2.12 [weight('<44,76,7,[0,0,0,1]>')]).
% 1.72/2.12 cnf('0.77.2.0',plain,
% 1.72/2.12 ( converse(composition(X1,zero)) = composition(zero,converse(X1)) ),
% 1.72/2.12 inference(orient,[status(thm)],['0.77.1.0',theory(equality)]),
% 1.72/2.12 [u,rule_74]).
% 1.72/2.12 cnf('0.78.0.0',plain,
% 1.72/2.12 ( converse(composition(zero,X1)) = composition(converse(X1),zero) ),
% 1.72/2.12 inference(cp,[status(thm)],['0.7.2.0','0.76.2.0',theory(equality)]),
% 1.72/2.12 [pos('L.2','L')]).
% 1.72/2.12 cnf('0.78.1.0',plain,
% 1.72/2.12 ( converse(composition(zero,X1)) = composition(converse(X1),zero) ),
% 1.72/2.12 inference(weigh,[status(thm)],['0.78.0.0']),
% 1.72/2.12 [weight('<44,76,7,[0,0,0,3]>')]).
% 1.72/2.12 cnf('0.78.2.0',plain,
% 1.72/2.12 ( converse(composition(zero,X1)) = composition(converse(X1),zero) ),
% 1.72/2.12 inference(orient,[status(thm)],['0.78.1.0',theory(equality)]),
% 1.72/2.12 [u,rule_75]).
% 1.72/2.12 cnf('0.79.0.0',plain,
% 1.72/2.12 ( join(X1,join(X1,X2)) = join(X1,X2) ),
% 1.72/2.12 inference(cp,[status(thm)],['0.9.2.0','0.71.2.0',theory(equality)]),
% 1.72/2.12 [pos('L.1','L')]).
% 1.72/2.12 cnf('0.79.1.0',plain,
% 1.72/2.12 ( join(X1,join(X1,X2)) = join(X1,X2) ),
% 1.72/2.12 inference(weigh,[status(thm)],['0.79.0.0']),
% 1.72/2.12 [weight('<53,71,9,[0,0,0,1]>')]).
% 1.72/2.12 cnf('0.79.2.0',plain,
% 1.72/2.12 ( join(X1,join(X1,X2)) = join(X1,X2) ),
% 1.72/2.12 inference(orient,[status(thm)],['0.79.1.0',theory(equality)]),
% 1.72/2.12 [u,rule_76]).
% 1.72/2.12 cnf('0.80.0.0',plain,
% 1.72/2.12 ( join(meet(X1,X2),complement(join(complement(X1),X2))) = join(meet(X1,X2),X1) ),
% 1.72/2.12 inference(cp,[status(thm)],['0.79.2.0','0.61.2.0',theory(equality)]),
% 1.72/2.12 [pos('L.2','L')]).
% 1.72/2.12 cnf('0.80.0.1',plain,
% 1.72/2.12 ( X1 = join(meet(X1,X2),X1) ),
% 1.72/2.12 inference(reduction,[status(thm)],['0.80.0.0','0.61.2.0',theory(equality)]),
% 1.72/2.12 [pos('L','L')]).
% 1.72/2.12 cnf('0.80.1.0',plain,
% 1.72/2.12 ( X1 = join(meet(X1,X2),X1) ),
% 1.72/2.12 inference(weigh,[status(thm)],['0.80.0.1']),
% 1.72/2.12 [weight('<41,79,61,[1,0,0,2]>')]).
% 1.72/2.12 cnf('0.80.1.1',plain,
% 1.72/2.12 ( X1 = join(X1,meet(X1,X2)) ),
% 1.72/2.12 inference(reduction,[status(thm)],['0.80.1.0','0.8.2.0',theory(equality)]),
% 1.72/2.12 [pos('R','L')]).
% 1.72/2.12 cnf('0.80.2.0',plain,
% 1.72/2.12 ( join(X1,meet(X1,X2)) = X1 ),
% 1.72/2.12 inference(orient,[status(thm)],['0.80.1.1',theory(equality)]),
% 1.72/2.12 [x,rule_77]).
% 1.72/2.12 cnf('0.81.0.0',plain,
% 1.72/2.12 ( X1 = join(X1,meet(X2,X1)) ),
% 1.72/2.12 inference(cp,[status(thm)],['0.80.2.0','0.21.2.0',theory(equality)]),
% 1.72/2.12 [pos('L.2','L')]).
% 1.72/2.12 cnf('0.81.1.0',plain,
% 1.72/2.12 ( X1 = join(X1,meet(X2,X1)) ),
% 1.72/2.12 inference(weigh,[status(thm)],['0.81.0.0']),
% 1.72/2.12 [weight('<41,80,21,[1,0,0,2]>')]).
% 1.72/2.12 cnf('0.81.2.0',plain,
% 1.72/2.12 ( join(X1,meet(X2,X1)) = X1 ),
% 1.72/2.12 inference(orient,[status(thm)],['0.81.1.0',theory(equality)]),
% 1.72/2.12 [x,rule_78]).
% 1.72/2.12 cnf('0.82.0.0',plain,
% 1.72/2.12 ( join(X1,X2) = join(X1,join(X2,X1)) ),
% 1.72/2.12 inference(cp,[status(thm)],['0.79.2.0','0.8.2.0',theory(equality)]),
% 1.72/2.12 [pos('L.2','L')]).
% 1.72/2.12 cnf('0.82.1.0',plain,
% 1.72/2.12 ( join(X1,X2) = join(X1,join(X2,X1)) ),
% 1.72/2.12 inference(weigh,[status(thm)],['0.82.0.0']),
% 1.72/2.12 [weight('<53,79,8,[1,0,0,2]>')]).
% 1.72/2.12 cnf('0.82.2.0',plain,
% 1.72/2.12 ( join(X1,join(X2,X1)) = join(X1,X2) ),
% 1.72/2.12 inference(orient,[status(thm)],['0.82.1.0',theory(equality)]),
% 1.72/2.12 [x,rule_79]).
% 1.72/2.12 cnf('0.83.0.0',plain,
% 1.72/2.12 ( join(X1,join(complement(X1),X2)) = join(top,X2) ),
% 1.72/2.12 inference(interreduction_right,[status(thm)],['0.50.2.0'])).
% 1.72/2.12 cnf('0.83.0.1',plain,
% 1.72/2.12 ( join(X1,join(complement(X1),X2)) = top ),
% 1.72/2.12 inference(reduction,[status(thm)],['0.83.0.0','0.55.2.0',theory(equality)]),
% 1.72/2.12 [pos('R','L')]).
% 1.72/2.12 cnf('0.83.1.0',plain,
% 1.72/2.12 ( join(X1,join(complement(X1),X2)) = top ),
% 1.72/2.12 inference(weigh,[status(thm)],['0.83.0.1']),
% 1.72/2.12 [weight('<55,50,55,[0,0,0,0]>')]).
% 1.72/2.12 cnf('0.83.2.0',plain,
% 1.72/2.12 ( join(X1,join(complement(X1),X2)) = top ),
% 1.72/2.12 inference(orient,[status(thm)],['0.83.1.0',theory(equality)]),
% 1.72/2.12 [u,rule_80]).
% 1.72/2.12 cnf('0.84.0.0',plain,
% 1.72/2.12 ( X1 = join(meet(X1,join(complement(complement(X1)),X2)),complement(top)) ),
% 1.72/2.12 inference(cp,[status(thm)],['0.61.2.0','0.83.2.0',theory(equality)]),
% 1.72/2.12 [pos('L.2.1','L')]).
% 1.72/2.12 cnf('0.84.0.1',plain,
% 1.72/2.12 ( X1 = join(meet(X1,join(X1,X2)),complement(top)) ),
% 1.72/2.12 inference(reduction,[status(thm)],['0.84.0.0','0.68.2.0',theory(equality)]),
% 1.72/2.12 [pos('R.1.2.1','L')]).
% 1.72/2.12 cnf('0.84.0.2',plain,
% 1.72/2.12 ( X1 = join(meet(X1,join(X1,X2)),zero) ),
% 1.72/2.12 inference(reduction,[status(thm)],['0.84.0.1','0.18.2.0',theory(equality)]),
% 1.72/2.12 [pos('R.2','L')]).
% 1.72/2.12 cnf('0.84.0.3',plain,
% 1.72/2.12 ( X1 = meet(X1,join(X1,X2)) ),
% 1.72/2.12 inference(reduction,[status(thm)],['0.84.0.2','0.66.2.0',theory(equality)]),
% 1.72/2.12 [pos('R','L')]).
% 1.72/2.12 cnf('0.84.1.0',plain,
% 1.72/2.12 ( X1 = meet(X1,join(X1,X2)) ),
% 1.72/2.12 inference(weigh,[status(thm)],['0.84.0.3']),
% 1.72/2.12 [weight('<41,83,61,[0,0,0,5]>')]).
% 1.72/2.12 cnf('0.84.2.0',plain,
% 1.72/2.12 ( meet(X1,join(X1,X2)) = X1 ),
% 1.72/2.12 inference(orient,[status(thm)],['0.84.1.0',theory(equality)]),
% 1.72/2.12 [x,rule_81]).
% 1.72/2.12 cnf('0.85.0.0',plain,
% 1.72/2.12 ( X1 = meet(X1,join(X2,X1)) ),
% 1.72/2.12 inference(cp,[status(thm)],['0.84.2.0','0.8.2.0',theory(equality)]),
% 1.72/2.12 [pos('L.2','L')]).
% 1.72/2.12 cnf('0.85.1.0',plain,
% 1.72/2.12 ( X1 = meet(X1,join(X2,X1)) ),
% 1.72/2.12 inference(weigh,[status(thm)],['0.85.0.0']),
% 1.72/2.12 [weight('<41,84,8,[1,0,0,2]>')]).
% 1.72/2.12 cnf('0.85.2.0',plain,
% 1.72/2.12 ( meet(X1,join(X2,X1)) = X1 ),
% 1.72/2.12 inference(orient,[status(thm)],['0.85.1.0',theory(equality)]),
% 1.72/2.12 [x,rule_82]).
% 1.72/2.12 cnf('0.92.0.0',plain,
% 1.72/2.12 ( join(join(complement(X1),X2),X1) = join(join(complement(X1),X2),top) ),
% 1.72/2.12 inference(cp,[status(thm)],['0.82.2.0','0.83.2.0',theory(equality)]),
% 1.72/2.12 [pos('L.2','L')]).
% 1.72/2.12 cnf('0.92.0.1',plain,
% 1.72/2.12 ( join(complement(X1),join(X2,X1)) = join(join(complement(X1),X2),top) ),
% 1.72/2.12 inference(reduction,[status(thm)],['0.92.0.0','0.9.2.0',theory(equality)]),
% 1.72/2.12 [pos('L','L')]).
% 1.72/2.12 cnf('0.92.0.2',plain,
% 1.72/2.12 ( join(complement(X1),join(X2,X1)) = join(complement(X1),join(X2,top)) ),
% 1.72/2.12 inference(reduction,[status(thm)],['0.92.0.1','0.9.2.0',theory(equality)]),
% 1.72/2.12 [pos('R','L')]).
% 1.72/2.12 cnf('0.92.0.3',plain,
% 1.72/2.12 ( join(complement(X1),join(X2,X1)) = join(complement(X1),top) ),
% 1.72/2.12 inference(reduction,[status(thm)],['0.92.0.2','0.54.2.0',theory(equality)]),
% 1.72/2.12 [pos('R.2','L')]).
% 1.72/2.12 cnf('0.92.0.4',plain,
% 1.72/2.12 ( join(complement(X1),join(X2,X1)) = top ),
% 1.72/2.12 inference(reduction,[status(thm)],['0.92.0.3','0.54.2.0',theory(equality)]),
% 1.72/2.12 [pos('R','L')]).
% 1.72/2.12 cnf('0.92.1.0',plain,
% 1.72/2.12 ( join(complement(X1),join(X2,X1)) = top ),
% 1.72/2.12 inference(weigh,[status(thm)],['0.92.0.4']),
% 1.72/2.12 [weight('<55,83,82,[0,0,0,2]>')]).
% 1.72/2.12 cnf('0.92.2.0',plain,
% 1.72/2.12 ( join(complement(X1),join(X2,X1)) = top ),
% 1.72/2.12 inference(orient,[status(thm)],['0.92.1.0',theory(equality)]),
% 1.72/2.12 [u,rule_89]).
% 1.72/2.12 cnf('0.94.0.0',plain,
% 1.72/2.12 ( top = join(complement(meet(X1,X2)),X2) ),
% 1.72/2.12 inference(cp,[status(thm)],['0.92.2.0','0.81.2.0',theory(equality)]),
% 1.72/2.12 [pos('L.2','L')]).
% 1.72/2.12 cnf('0.94.1.0',plain,
% 1.72/2.12 ( top = join(complement(meet(X1,X2)),X2) ),
% 1.72/2.12 inference(weigh,[status(thm)],['0.94.0.0']),
% 1.72/2.12 [weight('<55,92,81,[1,0,0,3]>')]).
% 1.72/2.12 cnf('0.94.1.1',plain,
% 1.72/2.12 ( top = join(X2,complement(meet(X1,X2))) ),
% 1.72/2.12 inference(reduction,[status(thm)],['0.94.1.0','0.8.2.0',theory(equality)]),
% 1.72/2.12 [pos('R','L')]).
% 1.72/2.12 cnf('0.94.2.0',plain,
% 1.72/2.12 ( join(X1,complement(meet(X2,X1))) = top ),
% 1.72/2.12 inference(orient,[status(thm)],['0.94.1.1',theory(equality)]),
% 1.72/2.12 [x,rule_91]).
% 1.72/2.12 cnf('0.96.0.0',plain,
% 1.72/2.12 ( meet(X1,meet(X2,complement(X1))) = complement(top) ),
% 1.72/2.12 inference(cp,[status(thm)],['0.15.2.0','0.94.2.0',theory(equality)]),
% 1.72/2.12 [pos('L.1','L')]).
% 1.72/2.12 cnf('0.96.0.1',plain,
% 1.72/2.12 ( meet(X1,meet(X2,complement(X1))) = zero ),
% 1.72/2.12 inference(reduction,[status(thm)],['0.96.0.0','0.18.2.0',theory(equality)]),
% 1.72/2.12 [pos('R','L')]).
% 1.72/2.12 cnf('0.96.1.0',plain,
% 1.72/2.12 ( meet(X1,meet(X2,complement(X1))) = zero ),
% 1.72/2.12 inference(weigh,[status(thm)],['0.96.0.1']),
% 1.72/2.12 [weight('<55,94,15,[0,0,0,1]>')]).
% 1.72/2.12 cnf('0.96.2.0',plain,
% 1.72/2.12 ( meet(X1,meet(X2,complement(X1))) = zero ),
% 1.72/2.12 inference(orient,[status(thm)],['0.96.1.0',theory(equality)]),
% 1.72/2.12 [u,rule_93]).
% 1.72/2.12 cnf('0.98.0.0',plain,
% 1.72/2.12 ( zero = meet(complement(X1),meet(X2,X1)) ),
% 1.72/2.12 inference(cp,[status(thm)],['0.96.2.0','0.68.2.0',theory(equality)]),
% 1.72/2.12 [pos('L.2.2','L')]).
% 1.72/2.12 cnf('0.98.1.0',plain,
% 1.72/2.12 ( zero = meet(complement(X1),meet(X2,X1)) ),
% 1.72/2.12 inference(weigh,[status(thm)],['0.98.0.0']),
% 1.72/2.12 [weight('<55,96,68,[1,0,0,4]>')]).
% 1.72/2.12 cnf('0.98.2.0',plain,
% 1.72/2.12 ( meet(complement(X1),meet(X2,X1)) = zero ),
% 1.72/2.12 inference(orient,[status(thm)],['0.98.1.0',theory(equality)]),
% 1.72/2.12 [x,rule_95]).
% 1.72/2.12 cnf('0.100.0.0',plain,
% 1.72/2.12 ( zero = meet(complement(join(X1,X2)),X2) ),
% 1.72/2.12 inference(cp,[status(thm)],['0.98.2.0','0.85.2.0',theory(equality)]),
% 1.72/2.12 [pos('L.2','L')]).
% 1.72/2.12 cnf('0.100.1.0',plain,
% 1.72/2.12 ( zero = meet(complement(join(X1,X2)),X2) ),
% 1.72/2.12 inference(weigh,[status(thm)],['0.100.0.0']),
% 1.72/2.12 [weight('<55,98,85,[1,0,0,3]>')]).
% 1.72/2.12 cnf('0.100.1.1',plain,
% 1.72/2.12 ( zero = meet(X2,complement(join(X1,X2))) ),
% 1.72/2.12 inference(reduction,[status(thm)],['0.100.1.0','0.21.2.0',theory(equality)]),
% 1.72/2.12 [pos('R','L')]).
% 1.72/2.12 cnf('0.100.2.0',plain,
% 1.72/2.12 ( meet(X1,complement(join(X2,X1))) = zero ),
% 1.72/2.12 inference(orient,[status(thm)],['0.100.1.1',theory(equality)]),
% 1.72/2.12 [x,rule_97]).
% 1.72/2.12 cnf('0.101.0.0',plain,
% 1.72/2.12 ( meet(complement(X1),X2) = complement(join(X1,complement(X2))) ),
% 1.72/2.12 inference(cp,[status(thm)],['0.15.2.0','0.68.2.0',theory(equality)]),
% 1.72/2.12 [pos('L.1.1','L')]).
% 1.72/2.12 cnf('0.101.1.0',plain,
% 1.72/2.12 ( meet(complement(X1),X2) = complement(join(X1,complement(X2))) ),
% 1.72/2.12 inference(weigh,[status(thm)],['0.101.0.0']),
% 1.72/2.12 [weight('<59,68,15,[0,0,0,2]>')]).
% 1.72/2.12 cnf('0.101.2.0',plain,
% 1.72/2.12 ( complement(join(X1,complement(X2))) = meet(complement(X1),X2) ),
% 1.72/2.12 inference(orient,[status(thm)],['0.101.1.0',theory(equality)]),
% 1.72/2.12 [x,rule_98]).
% 1.72/2.12 cnf('0.102.0.0',plain,
% 1.72/2.12 ( meet(complement(X1),X2) = complement(join(complement(X2),X1)) ),
% 1.72/2.12 inference(cp,[status(thm)],['0.101.2.0','0.8.2.0',theory(equality)]),
% 1.72/2.12 [pos('L.1','L')]).
% 1.72/2.12 cnf('0.102.1.0',plain,
% 1.72/2.12 ( meet(complement(X1),X2) = complement(join(complement(X2),X1)) ),
% 1.72/2.12 inference(weigh,[status(thm)],['0.102.0.0']),
% 1.72/2.12 [weight('<59,101,8,[1,0,0,1]>')]).
% 1.72/2.12 cnf('0.102.2.0',plain,
% 1.72/2.12 ( complement(join(complement(X1),X2)) = meet(complement(X2),X1) ),
% 1.72/2.12 inference(orient,[status(thm)],['0.102.1.0',theory(equality)]),
% 1.72/2.12 [x,rule_99]).
% 1.72/2.12 cnf('0.103.0.0',plain,
% 1.72/2.12 ( join(X1,complement(X2)) = complement(meet(complement(X1),X2)) ),
% 1.72/2.12 inference(cp,[status(thm)],['0.68.2.0','0.101.2.0',theory(equality)]),
% 1.72/2.12 [pos('L.1','L')]).
% 1.72/2.12 cnf('0.103.1.0',plain,
% 1.72/2.12 ( join(X1,complement(X2)) = complement(meet(complement(X1),X2)) ),
% 1.72/2.12 inference(weigh,[status(thm)],['0.103.0.0']),
% 1.72/2.12 [weight('<59,101,68,[0,0,0,1]>')]).
% 1.72/2.12 cnf('0.103.2.0',plain,
% 1.72/2.12 ( complement(meet(complement(X1),X2)) = join(X1,complement(X2)) ),
% 1.72/2.12 inference(orient,[status(thm)],['0.103.1.0',theory(equality)]),
% 1.72/2.12 [x,rule_100]).
% 1.72/2.12 cnf('0.104.0.0',plain,
% 1.72/2.12 ( meet(complement(X1),complement(X2)) = complement(join(X1,X2)) ),
% 1.72/2.12 inference(cp,[status(thm)],['0.101.2.0','0.68.2.0',theory(equality)]),
% 1.72/2.12 [pos('L.1.2','L')]).
% 1.72/2.12 cnf('0.104.1.0',plain,
% 1.72/2.12 ( meet(complement(X1),complement(X2)) = complement(join(X1,X2)) ),
% 1.72/2.12 inference(weigh,[status(thm)],['0.104.0.0']),
% 1.72/2.12 [weight('<59,101,68,[1,0,0,3]>')]).
% 1.72/2.12 cnf('0.104.2.0',plain,
% 1.72/2.12 ( meet(complement(X1),complement(X2)) = complement(join(X1,X2)) ),
% 1.72/2.12 inference(orient,[status(thm)],['0.104.1.0',theory(equality)]),
% 1.72/2.12 [u,rule_101]).
% 1.72/2.12 cnf('0.105.0.0',plain,
% 1.72/2.12 ( join(X1,complement(X2)) = complement(meet(X2,complement(X1))) ),
% 1.72/2.12 inference(cp,[status(thm)],['0.103.2.0','0.21.2.0',theory(equality)]),
% 1.72/2.12 [pos('L.1','L')]).
% 1.72/2.12 cnf('0.105.1.0',plain,
% 1.72/2.12 ( join(X1,complement(X2)) = complement(meet(X2,complement(X1))) ),
% 1.72/2.12 inference(weigh,[status(thm)],['0.105.0.0']),
% 1.72/2.12 [weight('<59,103,21,[1,0,0,1]>')]).
% 1.72/2.12 cnf('0.105.2.0',plain,
% 1.72/2.12 ( complement(meet(X1,complement(X2))) = join(X2,complement(X1)) ),
% 1.72/2.12 inference(orient,[status(thm)],['0.105.1.0',theory(equality)]),
% 1.72/2.12 [x,rule_102]).
% 1.72/2.12 cnf('0.106.0.0',plain,
% 1.72/2.12 ( join(complement(X1),complement(X2)) = complement(meet(X1,X2)) ),
% 1.72/2.12 inference(cp,[status(thm)],['0.103.2.0','0.68.2.0',theory(equality)]),
% 1.72/2.12 [pos('L.1.1','L')]).
% 1.72/2.12 cnf('0.106.1.0',plain,
% 1.72/2.12 ( join(complement(X1),complement(X2)) = complement(meet(X1,X2)) ),
% 1.72/2.12 inference(weigh,[status(thm)],['0.106.0.0']),
% 1.72/2.12 [weight('<59,103,68,[1,0,0,2]>')]).
% 1.72/2.12 cnf('0.106.2.0',plain,
% 1.72/2.12 ( join(complement(X1),complement(X2)) = complement(meet(X1,X2)) ),
% 1.72/2.12 inference(orient,[status(thm)],['0.106.1.0',theory(equality)]),
% 1.72/2.12 [u,rule_103]).
% 1.72/2.12 cnf('0.110.0.0',plain,
% 1.72/2.12 ( join(X1,converse(meet(X2,converse(X1)))) = converse(converse(X1)) ),
% 1.72/2.12 inference(cp,[status(thm)],['0.45.2.0','0.81.2.0',theory(equality)]),
% 1.72/2.12 [pos('L.1','L')]).
% 1.72/2.12 cnf('0.110.0.1',plain,
% 1.72/2.12 ( join(X1,converse(meet(X2,converse(X1)))) = X1 ),
% 1.72/2.12 inference(reduction,[status(thm)],['0.110.0.0','0.3.2.0',theory(equality)]),
% 1.72/2.12 [pos('R','L')]).
% 1.72/2.12 cnf('0.110.1.0',plain,
% 1.72/2.12 ( join(X1,converse(meet(X2,converse(X1)))) = X1 ),
% 1.72/2.12 inference(weigh,[status(thm)],['0.110.0.1']),
% 1.72/2.12 [weight('<71,81,45,[0,0,0,1]>')]).
% 1.72/2.12 cnf('0.110.2.0',plain,
% 1.72/2.12 ( join(X1,converse(meet(X2,converse(X1)))) = X1 ),
% 1.72/2.12 inference(orient,[status(thm)],['0.110.1.0',theory(equality)]),
% 1.72/2.12 [u,rule_107]).
% 1.72/2.12 cnf('0.129.0.0',plain,
% 1.72/2.12 ( join(X1,join(meet(X1,X2),X3)) = join(X1,X3) ),
% 1.72/2.12 inference(cp,[status(thm)],['0.9.2.0','0.80.2.0',theory(equality)]),
% 1.72/2.12 [pos('L.1','L')]).
% 1.72/2.12 cnf('0.129.1.0',plain,
% 1.72/2.12 ( join(X1,join(meet(X1,X2),X3)) = join(X1,X3) ),
% 1.72/2.12 inference(weigh,[status(thm)],['0.129.0.0']),
% 1.72/2.12 [weight('<87,80,9,[0,0,0,1]>')]).
% 1.72/2.12 cnf('0.129.2.0',plain,
% 1.72/2.12 ( join(X1,join(meet(X1,X2),X3)) = join(X1,X3) ),
% 1.72/2.12 inference(orient,[status(thm)],['0.129.1.0',theory(equality)]),
% 1.72/2.12 [u,rule_126]).
% 1.72/2.12 cnf('0.130.0.0',plain,
% 1.72/2.12 ( join(X1,meet(meet(X1,X2),X3)) = join(X1,meet(X1,X2)) ),
% 1.72/2.12 inference(cp,[status(thm)],['0.129.2.0','0.80.2.0',theory(equality)]),
% 1.72/2.12 [pos('L.2','L')]).
% 1.72/2.12 cnf('0.130.0.1',plain,
% 1.72/2.12 ( join(X1,meet(meet(X1,X2),X3)) = X1 ),
% 1.72/2.12 inference(reduction,[status(thm)],['0.130.0.0','0.80.2.0',theory(equality)]),
% 1.72/2.12 [pos('R','L')]).
% 1.72/2.12 cnf('0.130.1.0',plain,
% 1.72/2.12 ( join(X1,meet(meet(X1,X2),X3)) = X1 ),
% 1.72/2.12 inference(weigh,[status(thm)],['0.130.0.1']),
% 1.72/2.12 [weight('<71,129,80,[1,0,0,2]>')]).
% 1.72/2.12 cnf('0.130.2.0',plain,
% 1.72/2.12 ( join(X1,meet(meet(X1,X2),X3)) = X1 ),
% 1.72/2.12 inference(orient,[status(thm)],['0.130.1.0',theory(equality)]),
% 1.72/2.12 [u,rule_127]).
% 1.72/2.12 cnf('0.134.0.0',plain,
% 1.72/2.12 ( join(X1,join(meet(X2,X1),X3)) = join(X1,X3) ),
% 1.72/2.12 inference(cp,[status(thm)],['0.9.2.0','0.81.2.0',theory(equality)]),
% 1.72/2.12 [pos('L.1','L')]).
% 1.72/2.12 cnf('0.134.1.0',plain,
% 1.72/2.12 ( join(X1,join(meet(X2,X1),X3)) = join(X1,X3) ),
% 1.72/2.12 inference(weigh,[status(thm)],['0.134.0.0']),
% 1.72/2.12 [weight('<87,81,9,[0,0,0,1]>')]).
% 1.72/2.12 cnf('0.134.2.0',plain,
% 1.72/2.12 ( join(X1,join(meet(X2,X1),X3)) = join(X1,X3) ),
% 1.72/2.12 inference(orient,[status(thm)],['0.134.1.0',theory(equality)]),
% 1.72/2.12 [u,rule_131]).
% 1.72/2.12 cnf('0.148.0.0',plain,
% 1.72/2.12 ( join(meet(X1,X2),complement(join(complement(X1),X2))) = X1 ),
% 1.72/2.12 inference(interreduction_right,[status(thm)],['0.61.2.0'])).
% 1.72/2.12 cnf('0.148.0.1',plain,
% 1.72/2.12 ( join(meet(X1,X2),meet(complement(X2),X1)) = X1 ),
% 1.72/2.12 inference(reduction,[status(thm)],['0.148.0.0','0.102.2.0',theory(equality)]),
% 1.72/2.12 [pos('L.2','L')]).
% 1.72/2.12 cnf('0.148.1.0',plain,
% 1.72/2.12 ( join(meet(X1,X2),meet(complement(X2),X1)) = X1 ),
% 1.72/2.12 inference(weigh,[status(thm)],['0.148.0.1']),
% 1.72/2.12 [weight('<89,61,102,[0,0,0,0]>')]).
% 1.72/2.12 cnf('0.148.2.0',plain,
% 1.72/2.12 ( join(meet(X1,X2),meet(complement(X2),X1)) = X1 ),
% 1.72/2.12 inference(orient,[status(thm)],['0.148.1.0',theory(equality)]),
% 1.72/2.12 [u,rule_145]).
% 1.72/2.12 cnf('0.149.0.0',plain,
% 1.72/2.12 ( join(X1,meet(complement(X1),X2)) = join(X1,X2) ),
% 1.72/2.12 inference(cp,[status(thm)],['0.134.2.0','0.148.2.0',theory(equality)]),
% 1.72/2.12 [pos('L.2','L')]).
% 1.72/2.12 cnf('0.149.1.0',plain,
% 1.72/2.12 ( join(X1,meet(complement(X1),X2)) = join(X1,X2) ),
% 1.72/2.12 inference(weigh,[status(thm)],['0.149.0.0']),
% 1.72/2.12 [weight('<69,148,134,[0,0,0,2]>')]).
% 1.72/2.12 cnf('0.149.2.0',plain,
% 1.72/2.12 ( join(X1,meet(complement(X1),X2)) = join(X1,X2) ),
% 1.72/2.12 inference(orient,[status(thm)],['0.149.1.0',theory(equality)]),
% 1.72/2.12 [u,rule_146]).
% 1.72/2.12 cnf('0.150.0.0',plain,
% 1.72/2.12 ( join(X1,X2) = join(X1,meet(X2,complement(X1))) ),
% 1.72/2.12 inference(cp,[status(thm)],['0.149.2.0','0.21.2.0',theory(equality)]),
% 1.72/2.12 [pos('L.2','L')]).
% 1.72/2.12 cnf('0.150.1.0',plain,
% 1.72/2.12 ( join(X1,X2) = join(X1,meet(X2,complement(X1))) ),
% 1.72/2.12 inference(weigh,[status(thm)],['0.150.0.0']),
% 1.72/2.12 [weight('<69,149,21,[1,0,0,2]>')]).
% 1.72/2.12 cnf('0.150.2.0',plain,
% 1.72/2.12 ( join(X1,meet(X2,complement(X1))) = join(X1,X2) ),
% 1.72/2.12 inference(orient,[status(thm)],['0.150.1.0',theory(equality)]),
% 1.72/2.12 [x,rule_147]).
% 1.72/2.12 cnf('0.151.0.0',plain,
% 1.72/2.12 ( sk1 = join(zero,meet(complement(composition(sk1,complement(one))),sk1)) ),
% 1.72/2.12 inference(cp,[status(thm)],['0.148.2.0','0.28.2.0',theory(equality)]),
% 1.72/2.12 [pos('L.1','L')]).
% 1.72/2.12 cnf('0.151.0.1',plain,
% 1.72/2.12 ( sk1 = meet(complement(composition(sk1,complement(one))),sk1) ),
% 1.72/2.12 inference(reduction,[status(thm)],['0.151.0.0','0.63.2.0',theory(equality)]),
% 1.72/2.12 [pos('R','L')]).
% 1.72/2.12 cnf('0.151.1.0',plain,
% 1.72/2.12 ( sk1 = meet(complement(composition(sk1,complement(one))),sk1) ),
% 1.72/2.12 inference(weigh,[status(thm)],['0.151.0.1']),
% 1.72/2.12 [weight('<71,148,28,[1,0,0,1]>')]).
% 1.72/2.12 cnf('0.151.1.1',plain,
% 1.72/2.12 ( sk1 = meet(sk1,complement(composition(sk1,complement(one)))) ),
% 1.72/2.12 inference(reduction,[status(thm)],['0.151.1.0','0.21.2.0',theory(equality)]),
% 1.72/2.12 [pos('R','L')]).
% 1.72/2.12 cnf('0.151.2.0',plain,
% 1.72/2.12 ( meet(sk1,complement(composition(sk1,complement(one)))) = sk1 ),
% 1.72/2.12 inference(orient,[status(thm)],['0.151.1.1',theory(equality)]),
% 1.72/2.12 [x,rule_148]).
% 1.72/2.12 cnf('0.154.0.0',plain,
% 1.72/2.12 ( meet(complement(meet(complement(complement(X1)),X2)),X1) = complement(join(complement(X1),X2)) ),
% 1.72/2.12 inference(cp,[status(thm)],['0.102.2.0','0.149.2.0',theory(equality)]),
% 1.72/2.12 [pos('L.1','L')]).
% 1.72/2.12 cnf('0.154.0.1',plain,
% 1.72/2.12 ( meet(join(complement(X1),complement(X2)),X1) = complement(join(complement(X1),X2)) ),
% 1.72/2.12 inference(reduction,[status(thm)],['0.154.0.0','0.103.2.0',theory(equality)]),
% 1.72/2.12 [pos('L.1','L')]).
% 1.72/2.12 cnf('0.154.0.2',plain,
% 1.72/2.12 ( meet(complement(meet(X1,X2)),X1) = complement(join(complement(X1),X2)) ),
% 1.72/2.12 inference(reduction,[status(thm)],['0.154.0.1','0.106.2.0',theory(equality)]),
% 1.72/2.12 [pos('L.1','L')]).
% 1.72/2.12 cnf('0.154.0.3',plain,
% 1.72/2.12 ( meet(complement(meet(X1,X2)),X1) = meet(complement(X2),X1) ),
% 1.72/2.12 inference(reduction,[status(thm)],['0.154.0.2','0.102.2.0',theory(equality)]),
% 1.72/2.12 [pos('R','L')]).
% 1.72/2.12 cnf('0.154.1.0',plain,
% 1.72/2.12 ( meet(complement(meet(X1,X2)),X1) = meet(complement(X2),X1) ),
% 1.72/2.12 inference(weigh,[status(thm)],['0.154.0.3']),
% 1.72/2.12 [weight('<76,149,102,[0,0,0,1]>')]).
% 1.72/2.12 cnf('0.154.1.1',plain,
% 1.72/2.12 ( meet(X1,complement(meet(X1,X2))) = meet(complement(X2),X1) ),
% 1.72/2.12 inference(reduction,[status(thm)],['0.154.1.0','0.21.2.0',theory(equality)]),
% 1.72/2.12 [pos('L','L')]).
% 1.72/2.12 cnf('0.154.2.0',plain,
% 1.72/2.12 ( meet(X1,complement(meet(X1,X2))) = meet(complement(X2),X1) ),
% 1.72/2.12 inference(orient,[status(thm)],['0.154.1.1',theory(equality)]),
% 1.72/2.12 [u,rule_151]).
% 1.72/2.12 cnf('0.155.0.0',plain,
% 1.72/2.12 ( meet(complement(complement(X1)),X2) = meet(X2,join(X1,complement(X2))) ),
% 1.72/2.12 inference(cp,[status(thm)],['0.154.2.0','0.105.2.0',theory(equality)]),
% 1.72/2.12 [pos('L.2','L')]).
% 1.72/2.12 cnf('0.155.0.1',plain,
% 1.72/2.12 ( meet(X1,X2) = meet(X2,join(X1,complement(X2))) ),
% 1.72/2.12 inference(reduction,[status(thm)],['0.155.0.0','0.68.2.0',theory(equality)]),
% 1.72/2.12 [pos('L.1','L')]).
% 1.72/2.12 cnf('0.155.1.0',plain,
% 1.72/2.12 ( meet(X1,X2) = meet(X2,join(X1,complement(X2))) ),
% 1.72/2.12 inference(weigh,[status(thm)],['0.155.0.1']),
% 1.72/2.12 [weight('<69,154,105,[1,0,0,2]>')]).
% 1.72/2.12 cnf('0.155.2.0',plain,
% 1.72/2.12 ( meet(X1,join(X2,complement(X1))) = meet(X2,X1) ),
% 1.72/2.12 inference(orient,[status(thm)],['0.155.1.0',theory(equality)]),
% 1.72/2.12 [x,rule_152]).
% 1.72/2.12 cnf('0.156.0.0',plain,
% 1.72/2.12 ( meet(X1,X2) = meet(X2,join(complement(X2),X1)) ),
% 1.72/2.12 inference(cp,[status(thm)],['0.155.2.0','0.8.2.0',theory(equality)]),
% 1.72/2.12 [pos('L.2','L')]).
% 1.72/2.12 cnf('0.156.1.0',plain,
% 1.72/2.12 ( meet(X1,X2) = meet(X2,join(complement(X2),X1)) ),
% 1.72/2.12 inference(weigh,[status(thm)],['0.156.0.0']),
% 1.72/2.12 [weight('<69,155,8,[1,0,0,2]>')]).
% 1.72/2.12 cnf('0.156.2.0',plain,
% 1.72/2.12 ( meet(X1,join(complement(X1),X2)) = meet(X2,X1) ),
% 1.72/2.12 inference(orient,[status(thm)],['0.156.1.0',theory(equality)]),
% 1.72/2.12 [x,rule_153]).
% 1.72/2.12 cnf('0.157.0.0',plain,
% 1.72/2.12 ( meet(converse(complement(converse(complement(X1)))),X1) = meet(X1,top) ),
% 1.72/2.12 inference(cp,[status(thm)],['0.156.2.0','0.60.2.0',theory(equality)]),
% 1.72/2.12 [pos('L.2','L')]).
% 1.72/2.12 cnf('0.157.0.1',plain,
% 1.72/2.12 ( meet(converse(complement(converse(complement(X1)))),X1) = X1 ),
% 1.72/2.12 inference(reduction,[status(thm)],['0.157.0.0','0.73.2.0',theory(equality)]),
% 1.72/2.12 [pos('R','L')]).
% 1.72/2.12 cnf('0.157.1.0',plain,
% 1.72/2.12 ( meet(converse(complement(converse(complement(X1)))),X1) = X1 ),
% 1.72/2.12 inference(weigh,[status(thm)],['0.157.0.1']),
% 1.72/2.12 [weight('<71,156,60,[1,0,0,2]>')]).
% 1.72/2.12 cnf('0.157.1.1',plain,
% 1.72/2.12 ( meet(X1,converse(complement(converse(complement(X1))))) = X1 ),
% 1.72/2.12 inference(reduction,[status(thm)],['0.157.1.0','0.21.2.0',theory(equality)]),
% 1.72/2.12 [pos('L','L')]).
% 1.72/2.12 cnf('0.157.2.0',plain,
% 1.72/2.12 ( meet(X1,converse(complement(converse(complement(X1))))) = X1 ),
% 1.72/2.12 inference(orient,[status(thm)],['0.157.1.1',theory(equality)]),
% 1.72/2.12 [u,rule_154]).
% 1.72/2.12 cnf('0.158.0.0',plain,
% 1.72/2.12 ( join(X1,complement(converse(complement(converse(complement(complement(X1))))))) = complement(complement(X1)) ),
% 1.72/2.12 inference(cp,[status(thm)],['0.103.2.0','0.157.2.0',theory(equality)]),
% 1.72/2.12 [pos('L.1','L')]).
% 1.72/2.12 cnf('0.158.0.1',plain,
% 1.72/2.12 ( join(X1,complement(converse(complement(converse(X1))))) = complement(complement(X1)) ),
% 1.72/2.12 inference(reduction,[status(thm)],['0.158.0.0','0.68.2.0',theory(equality)]),
% 1.72/2.12 [pos('L.2.1.1.1.1','L')]).
% 1.72/2.12 cnf('0.158.0.2',plain,
% 1.72/2.12 ( join(X1,complement(converse(complement(converse(X1))))) = X1 ),
% 1.72/2.12 inference(reduction,[status(thm)],['0.158.0.1','0.68.2.0',theory(equality)]),
% 1.72/2.12 [pos('R','L')]).
% 1.72/2.12 cnf('0.158.1.0',plain,
% 1.72/2.12 ( join(X1,complement(converse(complement(converse(X1))))) = X1 ),
% 1.72/2.12 inference(weigh,[status(thm)],['0.158.0.2']),
% 1.72/2.12 [weight('<71,157,103,[0,0,0,1]>')]).
% 1.72/2.12 cnf('0.158.2.0',plain,
% 1.72/2.12 ( join(X1,complement(converse(complement(converse(X1))))) = X1 ),
% 1.72/2.12 inference(orient,[status(thm)],['0.158.1.0',theory(equality)]),
% 1.72/2.12 [u,rule_155]).
% 1.72/2.12 cnf('0.159.0.0',plain,
% 1.72/2.12 ( one = join(one,complement(converse(complement(one)))) ),
% 1.72/2.12 inference(cp,[status(thm)],['0.158.2.0','0.32.2.0',theory(equality)]),
% 1.72/2.12 [pos('L.2.1.1.1','L')]).
% 1.72/2.12 cnf('0.159.1.0',plain,
% 1.72/2.12 ( one = join(one,complement(converse(complement(one)))) ),
% 1.72/2.12 inference(weigh,[status(thm)],['0.159.0.0']),
% 1.72/2.12 [weight('<55,158,32,[1,0,0,5]>')]).
% 1.72/2.12 cnf('0.159.2.0',plain,
% 1.72/2.12 ( join(one,complement(converse(complement(one)))) = one ),
% 1.72/2.12 inference(orient,[status(thm)],['0.159.1.0',theory(equality)]),
% 1.72/2.12 [x,rule_156]).
% 1.72/2.12 cnf('0.160.0.0',plain,
% 1.72/2.12 ( meet(complement(one),converse(complement(one))) = complement(one) ),
% 1.72/2.12 inference(cp,[status(thm)],['0.101.2.0','0.159.2.0',theory(equality)]),
% 1.72/2.12 [pos('L.1','L')]).
% 1.72/2.12 cnf('0.160.1.0',plain,
% 1.72/2.12 ( meet(complement(one),converse(complement(one))) = complement(one) ),
% 1.72/2.12 inference(weigh,[status(thm)],['0.160.0.0']),
% 1.72/2.12 [weight('<62,159,101,[0,0,0,1]>')]).
% 1.72/2.12 cnf('0.160.2.0',plain,
% 1.72/2.12 ( meet(complement(one),converse(complement(one))) = complement(one) ),
% 1.72/2.12 inference(orient,[status(thm)],['0.160.1.0',theory(equality)]),
% 1.72/2.12 [u,rule_157]).
% 1.72/2.12 cnf('0.161.0.0',plain,
% 1.72/2.12 ( complement(one) = join(complement(one),converse(complement(one))) ),
% 1.72/2.12 inference(cp,[status(thm)],['0.110.2.0','0.160.2.0',theory(equality)]),
% 1.72/2.12 [pos('L.2.1','L')]).
% 1.72/2.12 cnf('0.161.1.0',plain,
% 1.72/2.12 ( complement(one) = join(complement(one),converse(complement(one))) ),
% 1.72/2.12 inference(weigh,[status(thm)],['0.161.0.0']),
% 1.72/2.12 [weight('<62,160,110,[0,0,0,3]>')]).
% 1.72/2.12 cnf('0.161.2.0',plain,
% 1.72/2.12 ( join(complement(one),converse(complement(one))) = complement(one) ),
% 1.72/2.12 inference(orient,[status(thm)],['0.161.1.0',theory(equality)]),
% 1.72/2.12 [x,rule_158]).
% 1.72/2.12 cnf('0.163.0.0',axiom,
% 1.72/2.12 ( join(meet(composition(X1,X2),X3),meet(composition(meet(X1,composition(X3,converse(X2))),X2),X3)) = meet(composition(meet(X1,composition(X3,converse(X2))),X2),X3) ),
% 1.72/2.12 file('/tmp/WALDMEISTER_7164_n015')).
% 1.72/2.12 cnf('0.163.1.0',plain,
% 1.72/2.12 ( join(meet(composition(X1,X2),X3),meet(composition(meet(X1,composition(X3,converse(X2))),X2),X3)) = meet(composition(meet(X1,composition(X3,converse(X2))),X2),X3) ),
% 1.72/2.12 inference(weigh,[status(thm)],['0.163.0.0']),
% 1.72/2.12 [weight('<0,0,0,[0,0,0,13]>')]).
% 1.72/2.12 cnf('0.163.1.1',plain,
% 1.72/2.12 ( join(meet(composition(X1,X2),X3),meet(X3,composition(meet(X1,composition(X3,converse(X2))),X2))) = meet(composition(meet(X1,composition(X3,converse(X2))),X2),X3) ),
% 1.72/2.12 inference(reduction,[status(thm)],['0.163.1.0','0.21.2.0',theory(equality)]),
% 1.72/2.12 [pos('L.2','L')]).
% 1.72/2.12 cnf('0.163.1.2',plain,
% 1.72/2.12 ( join(meet(composition(X1,X2),X3),meet(X3,composition(meet(X1,composition(X3,converse(X2))),X2))) = meet(X3,composition(meet(X1,composition(X3,converse(X2))),X2)) ),
% 1.72/2.12 inference(reduction,[status(thm)],['0.163.1.1','0.21.2.0',theory(equality)]),
% 1.72/2.12 [pos('R','L')]).
% 1.72/2.12 cnf('0.163.2.0',plain,
% 1.72/2.12 ( join(meet(composition(X1,X2),X3),meet(X3,composition(meet(X1,composition(X3,converse(X2))),X2))) = meet(X3,composition(meet(X1,composition(X3,converse(X2))),X2)) ),
% 1.72/2.12 inference(orient,[status(thm)],['0.163.1.2',theory(equality)]),
% 1.72/2.12 [u,rule_160]).
% 1.72/2.12 cnf('0.165.0.0',plain,
% 1.72/2.12 ( converse(complement(one)) = join(converse(complement(one)),complement(one)) ),
% 1.72/2.12 inference(cp,[status(thm)],['0.81.2.0','0.160.2.0',theory(equality)]),
% 1.72/2.12 [pos('L.2','L')]).
% 1.72/2.12 cnf('0.165.1.0',plain,
% 1.72/2.12 ( converse(complement(one)) = join(converse(complement(one)),complement(one)) ),
% 1.72/2.12 inference(weigh,[status(thm)],['0.165.0.0']),
% 1.72/2.12 [weight('<69,160,81,[0,0,0,2]>')]).
% 1.72/2.12 cnf('0.165.1.1',plain,
% 1.72/2.12 ( converse(complement(one)) = join(complement(one),converse(complement(one))) ),
% 1.72/2.12 inference(reduction,[status(thm)],['0.165.1.0','0.8.2.0',theory(equality)]),
% 1.72/2.12 [pos('R','L')]).
% 1.72/2.12 cnf('0.165.1.2',plain,
% 1.72/2.12 ( converse(complement(one)) = complement(one) ),
% 1.72/2.12 inference(reduction,[status(thm)],['0.165.1.1','0.161.2.0',theory(equality)]),
% 1.72/2.12 [pos('R','L')]).
% 1.72/2.12 cnf('0.165.2.0',plain,
% 1.72/2.12 ( converse(complement(one)) = complement(one) ),
% 1.72/2.12 inference(orient,[status(thm)],['0.165.1.2',theory(equality)]),
% 1.72/2.12 [u,rule_162]).
% 1.72/2.12 cnf('0.166.0.0',plain,
% 1.72/2.12 ( converse(composition(X1,complement(one))) = composition(complement(one),converse(X1)) ),
% 1.72/2.12 inference(cp,[status(thm)],['0.7.2.0','0.165.2.0',theory(equality)]),
% 1.72/2.12 [pos('L.1','L')]).
% 1.72/2.12 cnf('0.166.1.0',plain,
% 1.72/2.12 ( converse(composition(X1,complement(one))) = composition(complement(one),converse(X1)) ),
% 1.72/2.12 inference(weigh,[status(thm)],['0.166.0.0']),
% 1.72/2.12 [weight('<65,165,7,[0,0,0,1]>')]).
% 1.72/2.12 cnf('0.166.2.0',plain,
% 1.72/2.12 ( converse(composition(X1,complement(one))) = composition(complement(one),converse(X1)) ),
% 1.72/2.12 inference(orient,[status(thm)],['0.166.1.0',theory(equality)]),
% 1.72/2.12 [u,rule_163]).
% 1.72/2.12 cnf('0.167.0.0',plain,
% 1.72/2.12 ( converse(composition(complement(one),X1)) = composition(converse(X1),complement(one)) ),
% 1.72/2.12 inference(cp,[status(thm)],['0.7.2.0','0.165.2.0',theory(equality)]),
% 1.72/2.12 [pos('L.2','L')]).
% 1.72/2.12 cnf('0.167.1.0',plain,
% 1.72/2.12 ( converse(composition(complement(one),X1)) = composition(converse(X1),complement(one)) ),
% 1.72/2.12 inference(weigh,[status(thm)],['0.167.0.0']),
% 1.72/2.12 [weight('<65,165,7,[0,0,0,3]>')]).
% 1.72/2.12 cnf('0.167.2.0',plain,
% 1.72/2.12 ( converse(composition(complement(one),X1)) = composition(converse(X1),complement(one)) ),
% 1.72/2.12 inference(orient,[status(thm)],['0.167.1.0',theory(equality)]),
% 1.72/2.12 [u,rule_164]).
% 1.72/2.12 cnf('0.170.0.0',plain,
% 1.72/2.12 ( join(X1,converse(complement(converse(complement(converse(converse(X1))))))) = converse(converse(X1)) ),
% 1.72/2.12 inference(cp,[status(thm)],['0.45.2.0','0.158.2.0',theory(equality)]),
% 1.72/2.12 [pos('L.1','L')]).
% 1.72/2.12 cnf('0.170.0.1',plain,
% 1.72/2.12 ( join(X1,converse(complement(converse(complement(X1))))) = converse(converse(X1)) ),
% 1.72/2.12 inference(reduction,[status(thm)],['0.170.0.0','0.3.2.0',theory(equality)]),
% 1.72/2.12 [pos('L.2.1.1.1.1','L')]).
% 1.72/2.12 cnf('0.170.0.2',plain,
% 1.72/2.12 ( join(X1,converse(complement(converse(complement(X1))))) = X1 ),
% 1.72/2.12 inference(reduction,[status(thm)],['0.170.0.1','0.3.2.0',theory(equality)]),
% 1.72/2.12 [pos('R','L')]).
% 1.72/2.12 cnf('0.170.1.0',plain,
% 1.72/2.12 ( join(X1,converse(complement(converse(complement(X1))))) = X1 ),
% 1.72/2.12 inference(weigh,[status(thm)],['0.170.0.2']),
% 1.72/2.12 [weight('<71,158,45,[0,0,0,1]>')]).
% 1.72/2.12 cnf('0.170.2.0',plain,
% 1.72/2.12 ( join(X1,converse(complement(converse(complement(X1))))) = X1 ),
% 1.72/2.12 inference(orient,[status(thm)],['0.170.1.0',theory(equality)]),
% 1.72/2.12 [u,rule_167]).
% 1.72/2.12 cnf('0.173.0.0',plain,
% 1.72/2.12 ( meet(complement(converse(complement(converse(complement(complement(X1)))))),X1) = complement(complement(X1)) ),
% 1.72/2.12 inference(cp,[status(thm)],['0.102.2.0','0.170.2.0',theory(equality)]),
% 1.72/2.12 [pos('L.1','L')]).
% 1.72/2.12 cnf('0.173.0.1',plain,
% 1.72/2.12 ( meet(complement(converse(complement(converse(X1)))),X1) = complement(complement(X1)) ),
% 1.72/2.12 inference(reduction,[status(thm)],['0.173.0.0','0.68.2.0',theory(equality)]),
% 1.72/2.12 [pos('L.1.1.1.1.1','L')]).
% 1.72/2.12 cnf('0.173.0.2',plain,
% 1.72/2.12 ( meet(complement(converse(complement(converse(X1)))),X1) = X1 ),
% 1.72/2.12 inference(reduction,[status(thm)],['0.173.0.1','0.68.2.0',theory(equality)]),
% 1.72/2.12 [pos('R','L')]).
% 1.72/2.12 cnf('0.173.1.0',plain,
% 1.72/2.12 ( meet(complement(converse(complement(converse(X1)))),X1) = X1 ),
% 1.72/2.12 inference(weigh,[status(thm)],['0.173.0.2']),
% 1.72/2.12 [weight('<71,170,102,[0,0,0,1]>')]).
% 1.72/2.12 cnf('0.173.1.1',plain,
% 1.72/2.12 ( meet(X1,complement(converse(complement(converse(X1))))) = X1 ),
% 1.72/2.12 inference(reduction,[status(thm)],['0.173.1.0','0.21.2.0',theory(equality)]),
% 1.72/2.12 [pos('L','L')]).
% 1.72/2.12 cnf('0.173.2.0',plain,
% 1.72/2.12 ( meet(X1,complement(converse(complement(converse(X1))))) = X1 ),
% 1.72/2.12 inference(orient,[status(thm)],['0.173.1.1',theory(equality)]),
% 1.72/2.12 [u,rule_170]).
% 1.72/2.12 cnf('0.174.0.0',plain,
% 1.72/2.12 ( join(X1,complement(X2)) = join(X1,complement(join(X1,X2))) ),
% 1.72/2.12 inference(cp,[status(thm)],['0.149.2.0','0.104.2.0',theory(equality)]),
% 1.72/2.12 [pos('L.2','L')]).
% 1.72/2.12 cnf('0.174.1.0',plain,
% 1.72/2.12 ( join(X1,complement(X2)) = join(X1,complement(join(X1,X2))) ),
% 1.72/2.12 inference(weigh,[status(thm)],['0.174.0.0']),
% 1.72/2.12 [weight('<76,149,104,[1,0,0,2]>')]).
% 1.72/2.12 cnf('0.174.2.0',plain,
% 1.72/2.12 ( join(X1,complement(join(X1,X2))) = join(X1,complement(X2)) ),
% 1.72/2.12 inference(orient,[status(thm)],['0.174.1.0',theory(equality)]),
% 1.72/2.12 [x,rule_171]).
% 1.72/2.12 cnf('0.178.0.0',plain,
% 1.72/2.12 ( meet(X1,complement(X2)) = meet(complement(X2),join(X1,X2)) ),
% 1.72/2.12 inference(cp,[status(thm)],['0.155.2.0','0.68.2.0',theory(equality)]),
% 1.72/2.12 [pos('L.2.2','L')]).
% 1.72/2.12 cnf('0.178.1.0',plain,
% 1.72/2.12 ( meet(X1,complement(X2)) = meet(complement(X2),join(X1,X2)) ),
% 1.72/2.12 inference(weigh,[status(thm)],['0.178.0.0']),
% 1.72/2.12 [weight('<76,155,68,[1,0,0,4]>')]).
% 1.72/2.12 cnf('0.178.2.0',plain,
% 1.72/2.12 ( meet(complement(X1),join(X2,X1)) = meet(X2,complement(X1)) ),
% 1.72/2.12 inference(orient,[status(thm)],['0.178.1.0',theory(equality)]),
% 1.72/2.12 [x,rule_175]).
% 1.72/2.12 cnf('0.179.0.0',plain,
% 1.72/2.12 ( meet(X1,complement(converse(complement(converse(X1))))) = meet(complement(converse(complement(converse(X1)))),top) ),
% 1.72/2.12 inference(cp,[status(thm)],['0.178.2.0','0.60.2.0',theory(equality)]),
% 1.72/2.12 [pos('L.2','L')]).
% 1.72/2.12 cnf('0.179.0.1',plain,
% 1.72/2.12 ( X1 = meet(complement(converse(complement(converse(X1)))),top) ),
% 1.72/2.12 inference(reduction,[status(thm)],['0.179.0.0','0.173.2.0',theory(equality)]),
% 1.72/2.12 [pos('L','L')]).
% 1.72/2.12 cnf('0.179.0.2',plain,
% 1.72/2.12 ( X1 = complement(converse(complement(converse(X1)))) ),
% 1.72/2.12 inference(reduction,[status(thm)],['0.179.0.1','0.73.2.0',theory(equality)]),
% 1.72/2.12 [pos('R','L')]).
% 1.72/2.12 cnf('0.179.1.0',plain,
% 1.72/2.12 ( X1 = complement(converse(complement(converse(X1)))) ),
% 1.72/2.12 inference(weigh,[status(thm)],['0.179.0.2']),
% 1.72/2.12 [weight('<41,178,60,[1,0,0,3]>')]).
% 1.72/2.12 cnf('0.179.2.0',plain,
% 1.72/2.12 ( complement(converse(complement(converse(X1)))) = X1 ),
% 1.72/2.12 inference(orient,[status(thm)],['0.179.1.0',theory(equality)]),
% 1.72/2.12 [x,rule_176]).
% 1.72/2.12 cnf('0.180.0.0',plain,
% 1.72/2.12 ( converse(X1) = complement(converse(complement(X1))) ),
% 1.72/2.12 inference(cp,[status(thm)],['0.179.2.0','0.3.2.0',theory(equality)]),
% 1.72/2.12 [pos('L.1.1.1','L')]).
% 1.72/2.12 cnf('0.180.1.0',plain,
% 1.72/2.12 ( converse(X1) = complement(converse(complement(X1))) ),
% 1.72/2.12 inference(weigh,[status(thm)],['0.180.0.0']),
% 1.72/2.12 [weight('<34,179,3,[1,0,0,3]>')]).
% 1.72/2.12 cnf('0.180.2.0',plain,
% 1.72/2.12 ( complement(converse(complement(X1))) = converse(X1) ),
% 1.72/2.12 inference(orient,[status(thm)],['0.180.1.0',theory(equality)]),
% 1.72/2.12 [x,rule_177]).
% 1.72/2.12 cnf('0.181.0.0',plain,
% 1.72/2.12 ( converse(complement(X1)) = complement(converse(X1)) ),
% 1.72/2.12 inference(cp,[status(thm)],['0.68.2.0','0.180.2.0',theory(equality)]),
% 1.72/2.12 [pos('L.1','L')]).
% 1.72/2.12 cnf('0.181.1.0',plain,
% 1.72/2.12 ( converse(complement(X1)) = complement(converse(X1)) ),
% 1.72/2.12 inference(weigh,[status(thm)],['0.181.0.0']),
% 1.72/2.12 [weight('<27,180,68,[0,0,0,1]>')]).
% 1.72/2.12 cnf('0.181.2.0',plain,
% 1.72/2.12 ( converse(complement(X1)) = complement(converse(X1)) ),
% 1.72/2.12 inference(orient,[status(thm)],['0.181.1.0',theory(equality)]),
% 1.72/2.12 [u,rule_178]).
% 1.72/2.12 cnf('0.194.0.0',plain,
% 1.72/2.12 ( join(complement(X1),converse(X2)) = converse(join(complement(converse(X1)),X2)) ),
% 1.72/2.12 inference(cp,[status(thm)],['0.45.2.0','0.181.2.0',theory(equality)]),
% 1.72/2.12 [pos('L.1.1','L')]).
% 1.72/2.12 cnf('0.194.1.0',plain,
% 1.72/2.12 ( join(complement(X1),converse(X2)) = converse(join(complement(converse(X1)),X2)) ),
% 1.72/2.12 inference(weigh,[status(thm)],['0.194.0.0']),
% 1.72/2.12 [weight('<83,181,45,[0,0,0,2]>')]).
% 1.72/2.12 cnf('0.194.2.0',plain,
% 1.72/2.12 ( converse(join(complement(converse(X1)),X2)) = join(complement(X1),converse(X2)) ),
% 1.72/2.12 inference(orient,[status(thm)],['0.194.1.0',theory(equality)]),
% 1.72/2.12 [x,rule_191]).
% 1.72/2.12 cnf('0.196.0.0',plain,
% 1.72/2.12 ( complement(converse(join(X1,complement(X2)))) = converse(meet(complement(X1),X2)) ),
% 1.72/2.12 inference(cp,[status(thm)],['0.181.2.0','0.101.2.0',theory(equality)]),
% 1.72/2.12 [pos('L.1','L')]).
% 1.72/2.12 cnf('0.196.1.0',plain,
% 1.72/2.12 ( complement(converse(join(X1,complement(X2)))) = converse(meet(complement(X1),X2)) ),
% 1.72/2.12 inference(weigh,[status(thm)],['0.196.0.0']),
% 1.72/2.12 [weight('<83,181,101,[1,0,0,1]>')]).
% 1.72/2.12 cnf('0.196.2.0',plain,
% 1.72/2.12 ( complement(converse(join(X1,complement(X2)))) = converse(meet(complement(X1),X2)) ),
% 1.72/2.12 inference(orient,[status(thm)],['0.196.1.0',theory(equality)]),
% 1.72/2.12 [u,rule_193]).
% 1.72/2.12 cnf('0.197.0.0',plain,
% 1.72/2.12 ( converse(meet(complement(complement(converse(X1))),X2)) = complement(join(complement(X1),converse(complement(X2)))) ),
% 1.72/2.12 inference(cp,[status(thm)],['0.196.2.0','0.194.2.0',theory(equality)]),
% 1.72/2.12 [pos('L.1','L')]).
% 1.72/2.12 cnf('0.197.0.1',plain,
% 1.72/2.12 ( converse(meet(converse(X1),X2)) = complement(join(complement(X1),converse(complement(X2)))) ),
% 1.72/2.12 inference(reduction,[status(thm)],['0.197.0.0','0.68.2.0',theory(equality)]),
% 1.72/2.12 [pos('L.1.1','L')]).
% 1.72/2.12 cnf('0.197.0.2',plain,
% 1.72/2.12 ( converse(meet(converse(X1),X2)) = meet(complement(converse(complement(X2))),X1) ),
% 1.72/2.12 inference(reduction,[status(thm)],['0.197.0.1','0.102.2.0',theory(equality)]),
% 1.72/2.12 [pos('R','L')]).
% 1.72/2.12 cnf('0.197.0.3',plain,
% 1.72/2.12 ( converse(meet(converse(X1),X2)) = meet(complement(complement(converse(X2))),X1) ),
% 1.72/2.12 inference(reduction,[status(thm)],['0.197.0.2','0.181.2.0',theory(equality)]),
% 1.72/2.12 [pos('R.1.1','L')]).
% 1.72/2.12 cnf('0.197.0.4',plain,
% 1.72/2.12 ( converse(meet(converse(X1),X2)) = meet(converse(X2),X1) ),
% 1.72/2.12 inference(reduction,[status(thm)],['0.197.0.3','0.68.2.0',theory(equality)]),
% 1.72/2.12 [pos('R.1','L')]).
% 1.72/2.12 cnf('0.197.1.0',plain,
% 1.72/2.12 ( converse(meet(converse(X1),X2)) = meet(converse(X2),X1) ),
% 1.72/2.12 inference(weigh,[status(thm)],['0.197.0.4']),
% 1.72/2.12 [weight('<59,196,194,[1,0,0,1]>')]).
% 1.72/2.12 cnf('0.197.2.0',plain,
% 1.72/2.12 ( converse(meet(converse(X1),X2)) = meet(converse(X2),X1) ),
% 1.72/2.12 inference(orient,[status(thm)],['0.197.1.0',theory(equality)]),
% 1.72/2.12 [u,rule_194]).
% 1.72/2.12 cnf('0.198.0.0',plain,
% 1.72/2.12 ( meet(converse(X1),converse(X2)) = converse(meet(X2,X1)) ),
% 1.72/2.12 inference(cp,[status(thm)],['0.197.2.0','0.3.2.0',theory(equality)]),
% 1.72/2.12 [pos('L.1.1','L')]).
% 1.72/2.12 cnf('0.198.1.0',plain,
% 1.72/2.12 ( meet(converse(X1),converse(X2)) = converse(meet(X2,X1)) ),
% 1.72/2.12 inference(weigh,[status(thm)],['0.198.0.0']),
% 1.72/2.12 [weight('<59,197,3,[1,0,0,2]>')]).
% 1.72/2.12 cnf('0.198.2.0',plain,
% 1.72/2.12 ( meet(converse(X1),converse(X2)) = converse(meet(X2,X1)) ),
% 1.72/2.12 inference(orient,[status(thm)],['0.198.1.0',theory(equality)]),
% 1.72/2.12 [u,rule_195]).
% 1.72/2.12 cnf('0.214.0.0',plain,
% 1.72/2.12 ( composition(join(composition(X1,X2),X3),X4) = join(composition(X1,composition(X2,X4)),composition(X3,X4)) ),
% 1.72/2.12 inference(cp,[status(thm)],['0.5.2.0','0.4.2.0',theory(equality)]),
% 1.72/2.12 [pos('L.1','L')]).
% 1.72/2.12 cnf('0.214.1.0',plain,
% 1.72/2.12 ( composition(join(composition(X1,X2),X3),X4) = join(composition(X1,composition(X2,X4)),composition(X3,X4)) ),
% 1.72/2.12 inference(weigh,[status(thm)],['0.214.0.0']),
% 1.72/2.12 [weight('<?,5,4,[1,0,0,1]>')]).
% 1.72/2.12 cnf('0.214.2.0',plain,
% 1.72/2.12 ( join(composition(X1,composition(X2,X3)),composition(X4,X3)) = composition(join(composition(X1,X2),X4),X3) ),
% 1.72/2.12 inference(orient,[status(thm)],['0.214.1.0',theory(equality)]),
% 1.72/2.12 [x,rule_211]).
% 1.72/2.12 cnf('0.222.0.0',plain,
% 1.72/2.12 ( join(one,converse(meet(meet(one,X1),X2))) = converse(one) ),
% 1.72/2.12 inference(cp,[status(thm)],['0.34.2.0','0.130.2.0',theory(equality)]),
% 1.72/2.12 [pos('L.1','L')]).
% 1.72/2.12 cnf('0.222.0.1',plain,
% 1.72/2.12 ( join(one,converse(meet(meet(one,X1),X2))) = one ),
% 1.72/2.12 inference(reduction,[status(thm)],['0.222.0.0','0.32.2.0',theory(equality)]),
% 1.72/2.12 [pos('R','L')]).
% 1.72/2.12 cnf('0.222.1.0',plain,
% 1.72/2.12 ( join(one,converse(meet(meet(one,X1),X2))) = one ),
% 1.72/2.12 inference(weigh,[status(thm)],['0.222.0.1']),
% 1.72/2.12 [weight('<89,130,34,[0,0,0,1]>')]).
% 1.72/2.12 cnf('0.222.2.0',plain,
% 1.72/2.12 ( join(one,converse(meet(meet(one,X1),X2))) = one ),
% 1.72/2.12 inference(orient,[status(thm)],['0.222.1.0',theory(equality)]),
% 1.72/2.12 [u,rule_219]).
% 1.72/2.12 cnf('0.265.0.0',plain,
% 1.72/2.12 ( composition(join(X1,composition(X2,X3)),X4) = join(composition(X1,X4),composition(X2,composition(X3,X4))) ),
% 1.72/2.12 inference(cp,[status(thm)],['0.5.2.0','0.4.2.0',theory(equality)]),
% 1.72/2.12 [pos('L.2','L')]).
% 1.72/2.12 cnf('0.265.1.0',plain,
% 1.72/2.12 ( composition(join(X1,composition(X2,X3)),X4) = join(composition(X1,X4),composition(X2,composition(X3,X4))) ),
% 1.72/2.12 inference(weigh,[status(thm)],['0.265.0.0']),
% 1.72/2.12 [weight('<?,5,4,[1,0,0,4]>')]).
% 1.72/2.12 cnf('0.265.2.0',plain,
% 1.72/2.12 ( join(composition(X1,X2),composition(X3,composition(X4,X2))) = composition(join(X1,composition(X3,X4)),X2) ),
% 1.72/2.12 inference(orient,[status(thm)],['0.265.1.0',theory(equality)]),
% 1.72/2.12 [x,rule_262]).
% 1.72/2.12 cnf('0.292.0.0',plain,
% 1.72/2.12 ( complement(one) = join(complement(one),composition(converse(X1),complement(X1))) ),
% 1.72/2.12 inference(cp,[status(thm)],['0.11.2.0','0.1.2.0',theory(equality)]),
% 1.72/2.12 [pos('L.2.2.1','L')]).
% 1.72/2.12 cnf('0.292.1.0',plain,
% 1.72/2.12 ( complement(one) = join(complement(one),composition(converse(X1),complement(X1))) ),
% 1.72/2.12 inference(weigh,[status(thm)],['0.292.0.0']),
% 1.72/2.12 [weight('<98,11,1,[1,0,0,7]>')]).
% 1.72/2.12 cnf('0.292.2.0',plain,
% 1.72/2.12 ( join(complement(one),composition(converse(X1),complement(X1))) = complement(one) ),
% 1.72/2.12 inference(orient,[status(thm)],['0.292.1.0',theory(equality)]),
% 1.72/2.12 [x,rule_289]).
% 1.72/2.12 cnf('0.293.0.0',plain,
% 1.72/2.12 ( complement(one) = join(complement(one),composition(converse(top),zero)) ),
% 1.72/2.12 inference(cp,[status(thm)],['0.292.2.0','0.18.2.0',theory(equality)]),
% 1.72/2.12 [pos('L.2.2','L')]).
% 1.72/2.12 cnf('0.293.0.1',plain,
% 1.72/2.12 ( complement(one) = join(complement(one),composition(top,zero)) ),
% 1.72/2.12 inference(reduction,[status(thm)],['0.293.0.0','0.56.2.0',theory(equality)]),
% 1.72/2.12 [pos('R.2.1','L')]).
% 1.72/2.12 cnf('0.293.1.0',plain,
% 1.72/2.12 ( complement(one) = join(complement(one),composition(top,zero)) ),
% 1.72/2.12 inference(weigh,[status(thm)],['0.293.0.1']),
% 1.72/2.12 [weight('<62,292,18,[1,0,0,6]>')]).
% 1.72/2.12 cnf('0.293.2.0',plain,
% 1.72/2.12 ( join(complement(one),composition(top,zero)) = complement(one) ),
% 1.72/2.12 inference(orient,[status(thm)],['0.293.1.0',theory(equality)]),
% 1.72/2.12 [x,rule_290]).
% 1.72/2.12 cnf('0.294.0.0',plain,
% 1.72/2.12 ( zero = meet(composition(top,zero),complement(complement(one))) ),
% 1.72/2.12 inference(cp,[status(thm)],['0.100.2.0','0.293.2.0',theory(equality)]),
% 1.72/2.12 [pos('L.2.1','L')]).
% 1.72/2.12 cnf('0.294.0.1',plain,
% 1.72/2.12 ( zero = meet(composition(top,zero),one) ),
% 1.72/2.12 inference(reduction,[status(thm)],['0.294.0.0','0.68.2.0',theory(equality)]),
% 1.72/2.12 [pos('R.2','L')]).
% 1.72/2.12 cnf('0.294.1.0',plain,
% 1.72/2.12 ( zero = meet(composition(top,zero),one) ),
% 1.72/2.12 inference(weigh,[status(thm)],['0.294.0.1']),
% 1.72/2.12 [weight('<41,293,100,[0,0,0,3]>')]).
% 1.72/2.12 cnf('0.294.1.1',plain,
% 1.72/2.12 ( zero = meet(one,composition(top,zero)) ),
% 1.72/2.12 inference(reduction,[status(thm)],['0.294.1.0','0.21.2.0',theory(equality)]),
% 1.72/2.12 [pos('R','L')]).
% 1.72/2.12 cnf('0.294.2.0',plain,
% 1.72/2.12 ( meet(one,composition(top,zero)) = zero ),
% 1.72/2.12 inference(orient,[status(thm)],['0.294.1.1',theory(equality)]),
% 1.72/2.12 [x,rule_291]).
% 1.72/2.12 cnf('0.299.0.0',plain,
% 1.72/2.12 ( composition(top,zero) = meet(composition(top,zero),complement(one)) ),
% 1.72/2.12 inference(cp,[status(thm)],['0.85.2.0','0.293.2.0',theory(equality)]),
% 1.74/2.12 [pos('L.2','L')]).
% 1.74/2.12 cnf('0.299.1.0',plain,
% 1.74/2.12 ( composition(top,zero) = meet(composition(top,zero),complement(one)) ),
% 1.74/2.12 inference(weigh,[status(thm)],['0.299.0.0']),
% 1.74/2.12 [weight('<69,293,85,[0,0,0,2]>')]).
% 1.74/2.12 cnf('0.299.1.1',plain,
% 1.74/2.12 ( composition(top,zero) = meet(complement(one),composition(top,zero)) ),
% 1.74/2.12 inference(reduction,[status(thm)],['0.299.1.0','0.21.2.0',theory(equality)]),
% 1.74/2.12 [pos('R','L')]).
% 1.74/2.12 cnf('0.299.2.0',plain,
% 1.74/2.12 ( meet(complement(one),composition(top,zero)) = composition(top,zero) ),
% 1.74/2.12 inference(orient,[status(thm)],['0.299.1.1',theory(equality)]),
% 1.74/2.12 [x,rule_296]).
% 1.74/2.12 cnf('0.301.0.0',plain,
% 1.74/2.12 ( zero = meet(composition(converse(X1),complement(X1)),complement(complement(one))) ),
% 1.74/2.12 inference(cp,[status(thm)],['0.100.2.0','0.292.2.0',theory(equality)]),
% 1.74/2.12 [pos('L.2.1','L')]).
% 1.74/2.12 cnf('0.301.0.1',plain,
% 1.74/2.12 ( zero = meet(composition(converse(X1),complement(X1)),one) ),
% 1.74/2.12 inference(reduction,[status(thm)],['0.301.0.0','0.68.2.0',theory(equality)]),
% 1.74/2.12 [pos('R.2','L')]).
% 1.74/2.12 cnf('0.301.1.0',plain,
% 1.74/2.12 ( zero = meet(composition(converse(X1),complement(X1)),one) ),
% 1.74/2.12 inference(weigh,[status(thm)],['0.301.0.1']),
% 1.74/2.12 [weight('<71,292,100,[0,0,0,3]>')]).
% 1.74/2.12 cnf('0.301.1.1',plain,
% 1.74/2.12 ( zero = meet(one,composition(converse(X1),complement(X1))) ),
% 1.74/2.12 inference(reduction,[status(thm)],['0.301.1.0','0.21.2.0',theory(equality)]),
% 1.74/2.12 [pos('R','L')]).
% 1.74/2.12 cnf('0.301.2.0',plain,
% 1.74/2.12 ( meet(one,composition(converse(X1),complement(X1))) = zero ),
% 1.74/2.12 inference(orient,[status(thm)],['0.301.1.1',theory(equality)]),
% 1.74/2.12 [x,rule_298]).
% 1.74/2.12 cnf('0.315.0.0',plain,
% 1.74/2.12 ( zero = meet(one,composition(converse(complement(X1)),X1)) ),
% 1.74/2.12 inference(cp,[status(thm)],['0.301.2.0','0.68.2.0',theory(equality)]),
% 1.74/2.12 [pos('L.2.2','L')]).
% 1.74/2.12 cnf('0.315.0.1',plain,
% 1.74/2.12 ( zero = meet(one,composition(complement(converse(X1)),X1)) ),
% 1.74/2.12 inference(reduction,[status(thm)],['0.315.0.0','0.181.2.0',theory(equality)]),
% 1.74/2.12 [pos('R.2.1','L')]).
% 1.74/2.12 cnf('0.315.1.0',plain,
% 1.74/2.12 ( zero = meet(one,composition(complement(converse(X1)),X1)) ),
% 1.74/2.12 inference(weigh,[status(thm)],['0.315.0.1']),
% 1.74/2.12 [weight('<71,301,68,[1,0,0,5]>')]).
% 1.74/2.12 cnf('0.315.2.0',plain,
% 1.74/2.12 ( meet(one,composition(complement(converse(X1)),X1)) = zero ),
% 1.74/2.12 inference(orient,[status(thm)],['0.315.1.0',theory(equality)]),
% 1.74/2.12 [x,rule_312]).
% 1.74/2.12 cnf('0.349.0.0',plain,
% 1.74/2.12 ( complement(composition(sk1,complement(one))) = join(complement(composition(sk1,complement(one))),sk1) ),
% 1.74/2.12 inference(cp,[status(thm)],['0.81.2.0','0.151.2.0',theory(equality)]),
% 1.74/2.12 [pos('L.2','L')]).
% 1.74/2.12 cnf('0.349.1.0',plain,
% 1.74/2.12 ( complement(composition(sk1,complement(one))) = join(complement(composition(sk1,complement(one))),sk1) ),
% 1.74/2.12 inference(weigh,[status(thm)],['0.349.0.0']),
% 1.74/2.12 [weight('<103,151,81,[0,0,0,2]>')]).
% 1.74/2.12 cnf('0.349.1.1',plain,
% 1.74/2.12 ( complement(composition(sk1,complement(one))) = join(sk1,complement(composition(sk1,complement(one)))) ),
% 1.74/2.12 inference(reduction,[status(thm)],['0.349.1.0','0.8.2.0',theory(equality)]),
% 1.74/2.12 [pos('R','L')]).
% 1.74/2.12 cnf('0.349.2.0',plain,
% 1.74/2.12 ( join(sk1,complement(composition(sk1,complement(one)))) = complement(composition(sk1,complement(one))) ),
% 1.74/2.12 inference(orient,[status(thm)],['0.349.1.1',theory(equality)]),
% 1.74/2.12 [x,rule_346]).
% 1.74/2.12 cnf('0.357.0.0',plain,
% 1.74/2.12 ( meet(join(meet(complement(X1),X2),X3),X1) = meet(X1,join(complement(X1),X3)) ),
% 1.74/2.12 inference(cp,[status(thm)],['0.156.2.0','0.129.2.0',theory(equality)]),
% 1.74/2.12 [pos('L.2','L')]).
% 1.74/2.12 cnf('0.357.0.1',plain,
% 1.74/2.12 ( meet(join(meet(complement(X1),X2),X3),X1) = meet(X3,X1) ),
% 1.74/2.12 inference(reduction,[status(thm)],['0.357.0.0','0.156.2.0',theory(equality)]),
% 1.74/2.12 [pos('R','L')]).
% 1.74/2.12 cnf('0.357.1.0',plain,
% 1.74/2.12 ( meet(join(meet(complement(X1),X2),X3),X1) = meet(X3,X1) ),
% 1.74/2.12 inference(weigh,[status(thm)],['0.357.0.1']),
% 1.74/2.12 [weight('<107,156,129,[1,0,0,2]>')]).
% 1.74/2.12 cnf('0.357.1.1',plain,
% 1.74/2.12 ( meet(X1,join(meet(complement(X1),X2),X3)) = meet(X3,X1) ),
% 1.74/2.12 inference(reduction,[status(thm)],['0.357.1.0','0.21.2.0',theory(equality)]),
% 1.74/2.12 [pos('L','L')]).
% 1.74/2.12 cnf('0.357.2.0',plain,
% 1.74/2.12 ( meet(X1,join(meet(complement(X1),X2),X3)) = meet(X3,X1) ),
% 1.74/2.12 inference(orient,[status(thm)],['0.357.1.1',theory(equality)]),
% 1.74/2.12 [u,rule_352]).
% 1.74/2.12 cnf('0.358.0.0',plain,
% 1.74/2.12 ( meet(X1,one) = meet(one,join(composition(top,zero),X1)) ),
% 1.74/2.12 inference(cp,[status(thm)],['0.357.2.0','0.299.2.0',theory(equality)]),
% 1.74/2.12 [pos('L.2.1','L')]).
% 1.74/2.12 cnf('0.358.1.0',plain,
% 1.74/2.12 ( meet(X1,one) = meet(one,join(composition(top,zero),X1)) ),
% 1.74/2.12 inference(weigh,[status(thm)],['0.358.0.0']),
% 1.74/2.12 [weight('<87,357,299,[1,0,0,3]>')]).
% 1.74/2.12 cnf('0.358.2.0',plain,
% 1.74/2.12 ( meet(one,join(composition(top,zero),X1)) = meet(X1,one) ),
% 1.74/2.12 inference(orient,[status(thm)],['0.358.1.0',theory(equality)]),
% 1.74/2.12 [x,rule_353]).
% 1.74/2.12 cnf('0.359.0.0',plain,
% 1.74/2.12 ( meet(composition(X1,zero),one) = meet(one,composition(join(top,X1),zero)) ),
% 1.74/2.12 inference(cp,[status(thm)],['0.358.2.0','0.5.2.0',theory(equality)]),
% 1.74/2.12 [pos('L.2','L')]).
% 1.74/2.12 cnf('0.359.0.1',plain,
% 1.74/2.12 ( meet(composition(X1,zero),one) = meet(one,composition(top,zero)) ),
% 1.74/2.12 inference(reduction,[status(thm)],['0.359.0.0','0.55.2.0',theory(equality)]),
% 1.74/2.12 [pos('R.2.1','L')]).
% 1.74/2.12 cnf('0.359.0.2',plain,
% 1.74/2.12 ( meet(composition(X1,zero),one) = zero ),
% 1.74/2.12 inference(reduction,[status(thm)],['0.359.0.1','0.294.2.0',theory(equality)]),
% 1.74/2.12 [pos('R','L')]).
% 1.74/2.12 cnf('0.359.1.0',plain,
% 1.74/2.12 ( meet(composition(X1,zero),one) = zero ),
% 1.74/2.12 inference(weigh,[status(thm)],['0.359.0.2']),
% 1.74/2.12 [weight('<41,358,5,[1,0,0,2]>')]).
% 1.74/2.12 cnf('0.359.1.1',plain,
% 1.74/2.12 ( meet(one,composition(X1,zero)) = zero ),
% 1.74/2.12 inference(reduction,[status(thm)],['0.359.1.0','0.21.2.0',theory(equality)]),
% 1.74/2.12 [pos('L','L')]).
% 1.74/2.12 cnf('0.359.2.0',plain,
% 1.74/2.12 ( meet(one,composition(X1,zero)) = zero ),
% 1.74/2.12 inference(orient,[status(thm)],['0.359.1.1',theory(equality)]),
% 1.74/2.12 [u,rule_354]).
% 1.74/2.12 cnf('0.360.0.0',plain,
% 1.74/2.12 ( one = join(zero,meet(complement(composition(X1,zero)),one)) ),
% 1.74/2.12 inference(cp,[status(thm)],['0.148.2.0','0.359.2.0',theory(equality)]),
% 1.74/2.12 [pos('L.1','L')]).
% 1.74/2.12 cnf('0.360.0.1',plain,
% 1.74/2.12 ( one = meet(complement(composition(X1,zero)),one) ),
% 1.74/2.12 inference(reduction,[status(thm)],['0.360.0.0','0.63.2.0',theory(equality)]),
% 1.74/2.12 [pos('R','L')]).
% 1.74/2.12 cnf('0.360.1.0',plain,
% 1.74/2.12 ( one = meet(complement(composition(X1,zero)),one) ),
% 1.74/2.12 inference(weigh,[status(thm)],['0.360.0.1']),
% 1.74/2.12 [weight('<55,359,148,[0,0,0,1]>')]).
% 1.74/2.12 cnf('0.360.1.1',plain,
% 1.74/2.12 ( one = meet(one,complement(composition(X1,zero))) ),
% 1.74/2.12 inference(reduction,[status(thm)],['0.360.1.0','0.21.2.0',theory(equality)]),
% 1.74/2.12 [pos('R','L')]).
% 1.74/2.12 cnf('0.360.2.0',plain,
% 1.74/2.12 ( meet(one,complement(composition(X1,zero))) = one ),
% 1.74/2.12 inference(orient,[status(thm)],['0.360.1.1',theory(equality)]),
% 1.74/2.12 [x,rule_355]).
% 1.74/2.12 cnf('0.407.0.0',plain,
% 1.74/2.12 ( meet(join(meet(X1,complement(X2)),X3),X2) = meet(X2,join(complement(X2),X3)) ),
% 1.74/2.12 inference(cp,[status(thm)],['0.156.2.0','0.134.2.0',theory(equality)]),
% 1.74/2.12 [pos('L.2','L')]).
% 1.74/2.12 cnf('0.407.0.1',plain,
% 1.74/2.12 ( meet(join(meet(X1,complement(X2)),X3),X2) = meet(X3,X2) ),
% 1.74/2.12 inference(reduction,[status(thm)],['0.407.0.0','0.156.2.0',theory(equality)]),
% 1.74/2.12 [pos('R','L')]).
% 1.74/2.12 cnf('0.407.1.0',plain,
% 1.74/2.12 ( meet(join(meet(X1,complement(X2)),X3),X2) = meet(X3,X2) ),
% 1.74/2.12 inference(weigh,[status(thm)],['0.407.0.1']),
% 1.74/2.12 [weight('<107,156,134,[1,0,0,2]>')]).
% 1.74/2.12 cnf('0.407.1.1',plain,
% 1.74/2.12 ( meet(X2,join(meet(X1,complement(X2)),X3)) = meet(X3,X2) ),
% 1.74/2.12 inference(reduction,[status(thm)],['0.407.1.0','0.21.2.0',theory(equality)]),
% 1.74/2.12 [pos('L','L')]).
% 1.74/2.12 cnf('0.407.2.0',plain,
% 1.74/2.12 ( meet(X1,join(meet(X2,complement(X1)),X3)) = meet(X3,X1) ),
% 1.74/2.12 inference(orient,[status(thm)],['0.407.1.1',theory(equality)]),
% 1.74/2.12 [u,rule_402]).
% 1.74/2.12 cnf('0.408.0.0',plain,
% 1.74/2.12 ( meet(X1,composition(X2,zero)) = meet(composition(X2,zero),join(one,X1)) ),
% 1.74/2.12 inference(cp,[status(thm)],['0.407.2.0','0.360.2.0',theory(equality)]),
% 1.74/2.12 [pos('L.2.1','L')]).
% 1.74/2.12 cnf('0.408.1.0',plain,
% 1.74/2.12 ( meet(X1,composition(X2,zero)) = meet(composition(X2,zero),join(one,X1)) ),
% 1.74/2.12 inference(weigh,[status(thm)],['0.408.0.0']),
% 1.74/2.12 [weight('<103,407,360,[1,0,0,3]>')]).
% 1.74/2.12 cnf('0.408.2.0',plain,
% 1.74/2.12 ( meet(composition(X1,zero),join(one,X2)) = meet(X2,composition(X1,zero)) ),
% 1.74/2.12 inference(orient,[status(thm)],['0.408.1.0',theory(equality)]),
% 1.74/2.12 [x,rule_403]).
% 1.74/2.12 cnf('0.411.0.0',plain,
% 1.74/2.12 ( meet(X1,composition(X2,zero)) = meet(join(one,X1),composition(X2,zero)) ),
% 1.74/2.12 inference(cp,[status(thm)],['0.408.2.0','0.21.2.0',theory(equality)]),
% 1.74/2.12 [pos('L','L')]).
% 1.74/2.12 cnf('0.411.1.0',plain,
% 1.74/2.12 ( meet(X1,composition(X2,zero)) = meet(join(one,X1),composition(X2,zero)) ),
% 1.74/2.12 inference(weigh,[status(thm)],['0.411.0.0']),
% 1.74/2.12 [weight('<103,408,21,[1,0,0,0]>')]).
% 1.74/2.12 cnf('0.411.2.0',plain,
% 1.74/2.12 ( meet(join(one,X1),composition(X2,zero)) = meet(X1,composition(X2,zero)) ),
% 1.74/2.12 inference(orient,[status(thm)],['0.411.1.0',theory(equality)]),
% 1.74/2.12 [x,rule_406]).
% 1.74/2.12 cnf('0.419.0.0',plain,
% 1.74/2.12 ( meet(top,composition(meet(X1,composition(top,converse(X2))),X2)) = join(meet(composition(X1,X2),top),composition(meet(X1,composition(top,converse(X2))),X2)) ),
% 1.74/2.12 inference(cp,[status(thm)],['0.163.2.0','0.72.2.0',theory(equality)]),
% 1.74/2.12 [pos('L.2','L')]).
% 1.74/2.12 cnf('0.419.0.1',plain,
% 1.74/2.12 ( composition(meet(X1,composition(top,converse(X2))),X2) = join(meet(composition(X1,X2),top),composition(meet(X1,composition(top,converse(X2))),X2)) ),
% 1.74/2.12 inference(reduction,[status(thm)],['0.419.0.0','0.72.2.0',theory(equality)]),
% 1.74/2.12 [pos('L','L')]).
% 1.74/2.12 cnf('0.419.0.2',plain,
% 1.74/2.12 ( composition(meet(X1,composition(top,converse(X2))),X2) = join(composition(X1,X2),composition(meet(X1,composition(top,converse(X2))),X2)) ),
% 1.74/2.12 inference(reduction,[status(thm)],['0.419.0.1','0.73.2.0',theory(equality)]),
% 1.74/2.12 [pos('R.1','L')]).
% 1.74/2.12 cnf('0.419.0.3',plain,
% 1.74/2.12 ( composition(meet(X1,composition(top,converse(X2))),X2) = composition(join(X1,meet(X1,composition(top,converse(X2)))),X2) ),
% 1.74/2.12 inference(reduction,[status(thm)],['0.419.0.2','0.5.2.0',theory(equality)]),
% 1.74/2.12 [pos('R','L')]).
% 1.74/2.12 cnf('0.419.0.4',plain,
% 1.74/2.12 ( composition(meet(X1,composition(top,converse(X2))),X2) = composition(X1,X2) ),
% 1.74/2.12 inference(reduction,[status(thm)],['0.419.0.3','0.80.2.0',theory(equality)]),
% 1.74/2.12 [pos('R.1','L')]).
% 1.74/2.12 cnf('0.419.1.0',plain,
% 1.74/2.12 ( composition(meet(X1,composition(top,converse(X2))),X2) = composition(X1,X2) ),
% 1.74/2.12 inference(weigh,[status(thm)],['0.419.0.4']),
% 1.74/2.12 [weight('<107,163,72,[1,0,0,6]>')]).
% 1.74/2.12 cnf('0.419.2.0',plain,
% 1.74/2.12 ( composition(meet(X1,composition(top,converse(X2))),X2) = composition(X1,X2) ),
% 1.74/2.12 inference(orient,[status(thm)],['0.419.1.0',theory(equality)]),
% 1.74/2.12 [u,rule_414]).
% 1.74/2.12 cnf('0.427.0.0',plain,
% 1.74/2.12 ( composition(X1,top) = composition(meet(X1,composition(top,top)),top) ),
% 1.74/2.12 inference(cp,[status(thm)],['0.419.2.0','0.56.2.0',theory(equality)]),
% 1.74/2.12 [pos('L.1.2.2','L')]).
% 1.74/2.12 cnf('0.427.1.0',plain,
% 1.74/2.12 ( composition(X1,top) = composition(meet(X1,composition(top,top)),top) ),
% 1.74/2.12 inference(weigh,[status(thm)],['0.427.0.0']),
% 1.74/2.12 [weight('<87,419,56,[1,0,0,5]>')]).
% 1.74/2.12 cnf('0.427.2.0',plain,
% 1.74/2.12 ( composition(meet(X1,composition(top,top)),top) = composition(X1,top) ),
% 1.74/2.12 inference(orient,[status(thm)],['0.427.1.0',theory(equality)]),
% 1.74/2.12 [x,rule_422]).
% 1.74/2.12 cnf('0.428.0.0',plain,
% 1.74/2.12 ( composition(X1,zero) = composition(meet(X1,composition(top,zero)),zero) ),
% 1.74/2.12 inference(cp,[status(thm)],['0.419.2.0','0.76.2.0',theory(equality)]),
% 1.74/2.12 [pos('L.1.2.2','L')]).
% 1.74/2.12 cnf('0.428.1.0',plain,
% 1.74/2.12 ( composition(X1,zero) = composition(meet(X1,composition(top,zero)),zero) ),
% 1.74/2.12 inference(weigh,[status(thm)],['0.428.0.0']),
% 1.74/2.12 [weight('<87,419,76,[1,0,0,5]>')]).
% 1.74/2.12 cnf('0.428.2.0',plain,
% 1.74/2.12 ( composition(meet(X1,composition(top,zero)),zero) = composition(X1,zero) ),
% 1.74/2.12 inference(orient,[status(thm)],['0.428.1.0',theory(equality)]),
% 1.74/2.12 [x,rule_423]).
% 1.74/2.12 cnf('0.429.0.0',plain,
% 1.74/2.12 ( composition(one,zero) = composition(zero,zero) ),
% 1.74/2.12 inference(cp,[status(thm)],['0.428.2.0','0.359.2.0',theory(equality)]),
% 1.74/2.12 [pos('L.1','L')]).
% 1.74/2.12 cnf('0.429.0.1',plain,
% 1.74/2.12 ( zero = composition(zero,zero) ),
% 1.74/2.12 inference(reduction,[status(thm)],['0.429.0.0','0.33.2.0',theory(equality)]),
% 1.74/2.12 [pos('L','L')]).
% 1.74/2.12 cnf('0.429.1.0',plain,
% 1.74/2.12 ( zero = composition(zero,zero) ),
% 1.74/2.12 inference(weigh,[status(thm)],['0.429.0.1']),
% 1.74/2.12 [weight('<19,428,359,[1,0,0,1]>')]).
% 1.74/2.12 cnf('0.429.2.0',plain,
% 1.74/2.12 ( composition(zero,zero) = zero ),
% 1.74/2.12 inference(orient,[status(thm)],['0.429.1.0',theory(equality)]),
% 1.74/2.12 [x,rule_424]).
% 1.74/2.12 cnf('0.434.0.0',plain,
% 1.74/2.12 ( composition(join(one,X1),zero) = composition(meet(X1,composition(top,zero)),zero) ),
% 1.74/2.12 inference(cp,[status(thm)],['0.428.2.0','0.411.2.0',theory(equality)]),
% 1.74/2.12 [pos('L.1','L')]).
% 1.74/2.12 cnf('0.434.0.1',plain,
% 1.74/2.12 ( composition(join(one,X1),zero) = composition(X1,zero) ),
% 1.74/2.12 inference(reduction,[status(thm)],['0.434.0.0','0.428.2.0',theory(equality)]),
% 1.74/2.12 [pos('R','L')]).
% 1.74/2.12 cnf('0.434.1.0',plain,
% 1.74/2.12 ( composition(join(one,X1),zero) = composition(X1,zero) ),
% 1.74/2.12 inference(weigh,[status(thm)],['0.434.0.1']),
% 1.74/2.12 [weight('<53,428,411,[1,0,0,1]>')]).
% 1.74/2.12 cnf('0.434.2.0',plain,
% 1.74/2.12 ( composition(join(one,X1),zero) = composition(X1,zero) ),
% 1.74/2.12 inference(orient,[status(thm)],['0.434.1.0',theory(equality)]),
% 1.74/2.12 [u,rule_429]).
% 1.74/2.12 cnf('0.469.0.0',plain,
% 1.74/2.12 ( composition(meet(converse(X1),composition(X2,converse(X3))),meet(X3,composition(converse(converse(X1)),X2))) = join(meet(composition(converse(X1),X3),X2),composition(meet(converse(X1),composition(X2,converse(X3))),meet(X3,composition(X1,X2)))) ),
% 1.74/2.12 inference(cp,[status(thm)],['0.6.2.0','0.3.2.0',theory(equality)]),
% 1.74/2.12 [pos('L.2.2.2.1','L')]).
% 1.74/2.12 cnf('0.469.0.1',plain,
% 1.74/2.12 ( composition(meet(converse(X1),composition(X2,converse(X3))),meet(X3,composition(X1,X2))) = join(meet(composition(converse(X1),X3),X2),composition(meet(converse(X1),composition(X2,converse(X3))),meet(X3,composition(X1,X2)))) ),
% 1.74/2.12 inference(reduction,[status(thm)],['0.469.0.0','0.3.2.0',theory(equality)]),
% 1.74/2.12 [pos('L.2.2.1','L')]).
% 1.74/2.12 cnf('0.469.1.0',plain,
% 1.74/2.12 ( composition(meet(converse(X1),composition(X2,converse(X3))),meet(X3,composition(X1,X2))) = join(meet(composition(converse(X1),X3),X2),composition(meet(converse(X1),composition(X2,converse(X3))),meet(X3,composition(X1,X2)))) ),
% 1.74/2.12 inference(weigh,[status(thm)],['0.469.0.1']),
% 1.74/2.12 [weight('<?,6,3,[1,0,0,16]>')]).
% 1.74/2.12 cnf('0.469.2.0',plain,
% 1.74/2.12 ( join(meet(composition(converse(X1),X2),X3),composition(meet(converse(X1),composition(X3,converse(X2))),meet(X2,composition(X1,X3)))) = composition(meet(converse(X1),composition(X3,converse(X2))),meet(X2,composition(X1,X3))) ),
% 1.74/2.12 inference(orient,[status(thm)],['0.469.1.0',theory(equality)]),
% 1.74/2.12 [x,rule_464]).
% 1.74/2.12 cnf('0.472.0.0',plain,
% 1.74/2.12 ( composition(X1,top) = composition(meet(composition(top,top),X1),top) ),
% 1.74/2.12 inference(cp,[status(thm)],['0.427.2.0','0.21.2.0',theory(equality)]),
% 1.74/2.12 [pos('L.1','L')]).
% 1.74/2.12 cnf('0.472.1.0',plain,
% 1.74/2.12 ( composition(X1,top) = composition(meet(composition(top,top),X1),top) ),
% 1.74/2.12 inference(weigh,[status(thm)],['0.472.0.0']),
% 1.74/2.12 [weight('<87,427,21,[1,0,0,1]>')]).
% 1.74/2.12 cnf('0.472.2.0',plain,
% 1.74/2.12 ( composition(meet(composition(top,top),X1),top) = composition(X1,top) ),
% 1.74/2.12 inference(orient,[status(thm)],['0.472.1.0',theory(equality)]),
% 1.74/2.12 [x,rule_467]).
% 1.74/2.12 cnf('0.473.0.0',plain,
% 1.74/2.12 ( composition(complement(composition(top,top)),top) = composition(zero,top) ),
% 1.74/2.12 inference(cp,[status(thm)],['0.472.2.0','0.16.2.0',theory(equality)]),
% 1.74/2.12 [pos('L.1','L')]).
% 1.74/2.12 cnf('0.473.1.0',plain,
% 1.74/2.12 ( composition(complement(composition(top,top)),top) = composition(zero,top) ),
% 1.74/2.12 inference(weigh,[status(thm)],['0.473.0.0']),
% 1.74/2.12 [weight('<69,472,16,[1,0,0,1]>')]).
% 1.74/2.12 cnf('0.473.2.0',plain,
% 1.74/2.12 ( composition(complement(composition(top,top)),top) = composition(zero,top) ),
% 1.74/2.12 inference(orient,[status(thm)],['0.473.1.0',theory(equality)]),
% 1.74/2.12 [u,rule_468]).
% 1.74/2.12 cnf('0.474.0.0',plain,
% 1.74/2.12 ( composition(top,converse(complement(composition(top,top)))) = converse(composition(zero,top)) ),
% 1.74/2.12 inference(cp,[status(thm)],['0.58.2.0','0.473.2.0',theory(equality)]),
% 1.74/2.12 [pos('L.1','L')]).
% 1.74/2.12 cnf('0.474.0.1',plain,
% 1.74/2.12 ( composition(top,complement(converse(composition(top,top)))) = converse(composition(zero,top)) ),
% 1.74/2.12 inference(reduction,[status(thm)],['0.474.0.0','0.181.2.0',theory(equality)]),
% 1.74/2.12 [pos('L.2','L')]).
% 1.74/2.12 cnf('0.474.0.2',plain,
% 1.74/2.12 ( composition(top,complement(composition(converse(top),top))) = converse(composition(zero,top)) ),
% 1.74/2.12 inference(reduction,[status(thm)],['0.474.0.1','0.59.2.0',theory(equality)]),
% 1.74/2.12 [pos('L.2.1','L')]).
% 1.74/2.12 cnf('0.474.0.3',plain,
% 1.74/2.12 ( composition(top,complement(composition(top,top))) = converse(composition(zero,top)) ),
% 1.74/2.12 inference(reduction,[status(thm)],['0.474.0.2','0.56.2.0',theory(equality)]),
% 1.74/2.12 [pos('L.2.1.1','L')]).
% 1.74/2.12 cnf('0.474.0.4',plain,
% 1.74/2.12 ( composition(top,complement(composition(top,top))) = composition(converse(top),zero) ),
% 1.74/2.12 inference(reduction,[status(thm)],['0.474.0.3','0.78.2.0',theory(equality)]),
% 1.74/2.12 [pos('R','L')]).
% 1.74/2.12 cnf('0.474.0.5',plain,
% 1.74/2.12 ( composition(top,complement(composition(top,top))) = composition(top,zero) ),
% 1.74/2.12 inference(reduction,[status(thm)],['0.474.0.4','0.56.2.0',theory(equality)]),
% 1.74/2.12 [pos('R.1','L')]).
% 1.74/2.12 cnf('0.474.1.0',plain,
% 1.74/2.12 ( composition(top,complement(composition(top,top))) = composition(top,zero) ),
% 1.74/2.12 inference(weigh,[status(thm)],['0.474.0.5']),
% 1.74/2.12 [weight('<69,473,58,[0,0,0,1]>')]).
% 1.74/2.12 cnf('0.474.2.0',plain,
% 1.74/2.12 ( composition(top,complement(composition(top,top))) = composition(top,zero) ),
% 1.74/2.12 inference(orient,[status(thm)],['0.474.1.0',theory(equality)]),
% 1.74/2.12 [u,rule_469]).
% 1.74/2.12 cnf('0.475.0.0',plain,
% 1.74/2.12 ( composition(X1,zero) = composition(meet(composition(top,zero),X1),zero) ),
% 1.74/2.12 inference(cp,[status(thm)],['0.428.2.0','0.21.2.0',theory(equality)]),
% 1.74/2.12 [pos('L.1','L')]).
% 1.74/2.12 cnf('0.475.1.0',plain,
% 1.74/2.12 ( composition(X1,zero) = composition(meet(composition(top,zero),X1),zero) ),
% 1.74/2.12 inference(weigh,[status(thm)],['0.475.0.0']),
% 1.74/2.12 [weight('<87,428,21,[1,0,0,1]>')]).
% 1.74/2.12 cnf('0.475.2.0',plain,
% 1.74/2.12 ( composition(meet(composition(top,zero),X1),zero) = composition(X1,zero) ),
% 1.74/2.12 inference(orient,[status(thm)],['0.475.1.0',theory(equality)]),
% 1.74/2.12 [x,rule_470]).
% 1.74/2.12 cnf('0.476.0.0',plain,
% 1.74/2.12 ( composition(complement(composition(top,zero)),zero) = composition(zero,zero) ),
% 1.74/2.12 inference(cp,[status(thm)],['0.475.2.0','0.16.2.0',theory(equality)]),
% 1.74/2.12 [pos('L.1','L')]).
% 1.74/2.12 cnf('0.476.0.1',plain,
% 1.74/2.12 ( composition(complement(composition(top,zero)),zero) = zero ),
% 1.74/2.12 inference(reduction,[status(thm)],['0.476.0.0','0.429.2.0',theory(equality)]),
% 1.74/2.12 [pos('R','L')]).
% 1.74/2.12 cnf('0.476.1.0',plain,
% 1.74/2.12 ( composition(complement(composition(top,zero)),zero) = zero ),
% 1.74/2.12 inference(weigh,[status(thm)],['0.476.0.1']),
% 1.74/2.12 [weight('<55,475,16,[1,0,0,1]>')]).
% 1.74/2.12 cnf('0.476.2.0',plain,
% 1.74/2.12 ( composition(complement(composition(top,zero)),zero) = zero ),
% 1.74/2.12 inference(orient,[status(thm)],['0.476.1.0',theory(equality)]),
% 1.74/2.12 [u,rule_471]).
% 1.74/2.12 cnf('0.477.0.0',plain,
% 1.74/2.12 ( composition(zero,converse(complement(composition(top,zero)))) = converse(zero) ),
% 1.74/2.12 inference(cp,[status(thm)],['0.77.2.0','0.476.2.0',theory(equality)]),
% 1.74/2.12 [pos('L.1','L')]).
% 1.74/2.12 cnf('0.477.0.1',plain,
% 1.74/2.12 ( composition(zero,complement(converse(composition(top,zero)))) = converse(zero) ),
% 1.74/2.12 inference(reduction,[status(thm)],['0.477.0.0','0.181.2.0',theory(equality)]),
% 1.74/2.12 [pos('L.2','L')]).
% 1.74/2.12 cnf('0.477.0.2',plain,
% 1.74/2.12 ( composition(zero,complement(composition(converse(zero),top))) = converse(zero) ),
% 1.74/2.12 inference(reduction,[status(thm)],['0.477.0.1','0.59.2.0',theory(equality)]),
% 1.74/2.12 [pos('L.2.1','L')]).
% 1.74/2.12 cnf('0.477.0.3',plain,
% 1.74/2.12 ( composition(zero,complement(composition(zero,top))) = converse(zero) ),
% 1.74/2.12 inference(reduction,[status(thm)],['0.477.0.2','0.76.2.0',theory(equality)]),
% 1.74/2.12 [pos('L.2.1.1','L')]).
% 1.74/2.12 cnf('0.477.0.4',plain,
% 1.74/2.12 ( composition(zero,complement(composition(zero,top))) = zero ),
% 1.74/2.12 inference(reduction,[status(thm)],['0.477.0.3','0.76.2.0',theory(equality)]),
% 1.74/2.12 [pos('R','L')]).
% 1.74/2.12 cnf('0.477.1.0',plain,
% 1.74/2.12 ( composition(zero,complement(composition(zero,top))) = zero ),
% 1.74/2.12 inference(weigh,[status(thm)],['0.477.0.4']),
% 1.74/2.12 [weight('<55,476,77,[0,0,0,1]>')]).
% 1.74/2.12 cnf('0.477.2.0',plain,
% 1.74/2.12 ( composition(zero,complement(composition(zero,top))) = zero ),
% 1.74/2.12 inference(orient,[status(thm)],['0.477.1.0',theory(equality)]),
% 1.74/2.12 [u,rule_472]).
% 1.74/2.12 cnf('0.492.0.0',plain,
% 1.74/2.12 ( composition(converse(meet(meet(one,X1),X2)),zero) = composition(one,zero) ),
% 1.74/2.12 inference(cp,[status(thm)],['0.434.2.0','0.222.2.0',theory(equality)]),
% 1.74/2.12 [pos('L.1','L')]).
% 1.74/2.12 cnf('0.492.0.1',plain,
% 1.74/2.12 ( composition(converse(meet(meet(one,X1),X2)),zero) = zero ),
% 1.74/2.12 inference(reduction,[status(thm)],['0.492.0.0','0.33.2.0',theory(equality)]),
% 1.74/2.12 [pos('R','L')]).
% 1.74/2.12 cnf('0.492.1.0',plain,
% 1.74/2.12 ( composition(converse(meet(meet(one,X1),X2)),zero) = zero ),
% 1.74/2.12 inference(weigh,[status(thm)],['0.492.0.1']),
% 1.74/2.12 [weight('<89,434,222,[1,0,0,1]>')]).
% 1.74/2.12 cnf('0.492.2.0',plain,
% 1.74/2.12 ( composition(converse(meet(meet(one,X1),X2)),zero) = zero ),
% 1.74/2.12 inference(orient,[status(thm)],['0.492.1.0',theory(equality)]),
% 1.74/2.12 [u,rule_487]).
% 1.74/2.12 cnf('0.507.0.0',plain,
% 1.74/2.12 ( composition(meet(converse(zero),composition(complement(composition(zero,top)),converse(X1))),meet(X1,composition(zero,complement(composition(zero,top))))) = join(meet(composition(converse(zero),X1),complement(composition(zero,top))),composition(meet(converse(zero),composition(complement(composition(zero,top)),converse(X1))),meet(X1,zero))) ),
% 1.74/2.12 inference(cp,[status(thm)],['0.469.2.0','0.477.2.0',theory(equality)]),
% 1.74/2.12 [pos('L.2.2.2','L')]).
% 1.74/2.12 cnf('0.507.0.1',plain,
% 1.74/2.12 ( composition(meet(zero,composition(complement(composition(zero,top)),converse(X1))),meet(X1,composition(zero,complement(composition(zero,top))))) = join(meet(composition(converse(zero),X1),complement(composition(zero,top))),composition(meet(converse(zero),composition(complement(composition(zero,top)),converse(X1))),meet(X1,zero))) ),
% 1.74/2.12 inference(reduction,[status(thm)],['0.507.0.0','0.76.2.0',theory(equality)]),
% 1.74/2.12 [pos('L.1.1','L')]).
% 1.74/2.12 cnf('0.507.0.2',plain,
% 1.74/2.12 ( composition(zero,meet(X1,composition(zero,complement(composition(zero,top))))) = join(meet(composition(converse(zero),X1),complement(composition(zero,top))),composition(meet(converse(zero),composition(complement(composition(zero,top)),converse(X1))),meet(X1,zero))) ),
% 1.74/2.12 inference(reduction,[status(thm)],['0.507.0.1','0.69.2.0',theory(equality)]),
% 1.74/2.12 [pos('L.1','L')]).
% 1.74/2.12 cnf('0.507.0.3',plain,
% 1.74/2.12 ( composition(zero,meet(X1,zero)) = join(meet(composition(converse(zero),X1),complement(composition(zero,top))),composition(meet(converse(zero),composition(complement(composition(zero,top)),converse(X1))),meet(X1,zero))) ),
% 1.74/2.12 inference(reduction,[status(thm)],['0.507.0.2','0.477.2.0',theory(equality)]),
% 1.74/2.12 [pos('L.2.2','L')]).
% 1.74/2.12 cnf('0.507.0.4',plain,
% 1.74/2.12 ( composition(zero,zero) = join(meet(composition(converse(zero),X1),complement(composition(zero,top))),composition(meet(converse(zero),composition(complement(composition(zero,top)),converse(X1))),meet(X1,zero))) ),
% 1.74/2.12 inference(reduction,[status(thm)],['0.507.0.3','0.70.2.0',theory(equality)]),
% 1.74/2.12 [pos('L.2','L')]).
% 1.74/2.12 cnf('0.507.0.5',plain,
% 1.74/2.12 ( zero = join(meet(composition(converse(zero),X1),complement(composition(zero,top))),composition(meet(converse(zero),composition(complement(composition(zero,top)),converse(X1))),meet(X1,zero))) ),
% 1.74/2.12 inference(reduction,[status(thm)],['0.507.0.4','0.429.2.0',theory(equality)]),
% 1.74/2.12 [pos('L','L')]).
% 1.74/2.12 cnf('0.507.0.6',plain,
% 1.74/2.12 ( zero = join(meet(composition(zero,X1),complement(composition(zero,top))),composition(meet(converse(zero),composition(complement(composition(zero,top)),converse(X1))),meet(X1,zero))) ),
% 1.74/2.12 inference(reduction,[status(thm)],['0.507.0.5','0.76.2.0',theory(equality)]),
% 1.74/2.12 [pos('R.1.1.1','L')]).
% 1.74/2.12 cnf('0.507.0.7',plain,
% 1.74/2.12 ( zero = join(meet(composition(zero,X1),complement(composition(zero,top))),composition(meet(zero,composition(complement(composition(zero,top)),converse(X1))),meet(X1,zero))) ),
% 1.74/2.12 inference(reduction,[status(thm)],['0.507.0.6','0.76.2.0',theory(equality)]),
% 1.74/2.12 [pos('R.2.1.1','L')]).
% 1.74/2.12 cnf('0.507.0.8',plain,
% 1.74/2.12 ( zero = join(meet(composition(zero,X1),complement(composition(zero,top))),composition(zero,meet(X1,zero))) ),
% 1.74/2.12 inference(reduction,[status(thm)],['0.507.0.7','0.69.2.0',theory(equality)]),
% 1.74/2.12 [pos('R.2.1','L')]).
% 1.74/2.12 cnf('0.507.0.9',plain,
% 1.74/2.12 ( zero = join(meet(composition(zero,X1),complement(composition(zero,top))),composition(zero,zero)) ),
% 1.74/2.12 inference(reduction,[status(thm)],['0.507.0.8','0.70.2.0',theory(equality)]),
% 1.74/2.12 [pos('R.2.2','L')]).
% 1.74/2.12 cnf('0.507.0.10',plain,
% 1.74/2.12 ( zero = join(meet(composition(zero,X1),complement(composition(zero,top))),zero) ),
% 1.74/2.12 inference(reduction,[status(thm)],['0.507.0.9','0.429.2.0',theory(equality)]),
% 1.74/2.12 [pos('R.2','L')]).
% 1.74/2.12 cnf('0.507.0.11',plain,
% 1.74/2.12 ( zero = meet(composition(zero,X1),complement(composition(zero,top))) ),
% 1.74/2.12 inference(reduction,[status(thm)],['0.507.0.10','0.66.2.0',theory(equality)]),
% 1.74/2.12 [pos('R','L')]).
% 1.74/2.12 cnf('0.507.1.0',plain,
% 1.74/2.12 ( zero = meet(composition(zero,X1),complement(composition(zero,top))) ),
% 1.74/2.12 inference(weigh,[status(thm)],['0.507.0.11']),
% 1.74/2.12 [weight('<89,477,469,[0,0,0,17]>')]).
% 1.74/2.12 cnf('0.507.2.0',plain,
% 1.74/2.12 ( meet(composition(zero,X1),complement(composition(zero,top))) = zero ),
% 1.74/2.12 inference(orient,[status(thm)],['0.507.1.0',theory(equality)]),
% 1.74/2.12 [x,rule_502]).
% 1.74/2.12 cnf('0.509.0.0',plain,
% 1.74/2.12 ( join(composition(zero,top),composition(zero,X1)) = join(composition(zero,top),zero) ),
% 1.74/2.12 inference(cp,[status(thm)],['0.150.2.0','0.507.2.0',theory(equality)]),
% 1.74/2.12 [pos('L.2','L')]).
% 1.74/2.12 cnf('0.509.0.1',plain,
% 1.74/2.12 ( join(composition(zero,top),composition(zero,X1)) = composition(zero,top) ),
% 1.74/2.12 inference(reduction,[status(thm)],['0.509.0.0','0.66.2.0',theory(equality)]),
% 1.74/2.12 [pos('R','L')]).
% 1.74/2.12 cnf('0.509.1.0',plain,
% 1.74/2.12 ( join(composition(zero,top),composition(zero,X1)) = composition(zero,top) ),
% 1.74/2.12 inference(weigh,[status(thm)],['0.509.0.1']),
% 1.74/2.12 [weight('<87,507,150,[0,0,0,2]>')]).
% 1.74/2.12 cnf('0.509.2.0',plain,
% 1.74/2.12 ( join(composition(zero,top),composition(zero,X1)) = composition(zero,top) ),
% 1.74/2.12 inference(orient,[status(thm)],['0.509.1.0',theory(equality)]),
% 1.74/2.12 [u,rule_504]).
% 1.74/2.12 cnf('0.510.0.0',plain,
% 1.74/2.12 ( composition(zero,top) = composition(join(zero,composition(zero,X1)),top) ),
% 1.74/2.12 inference(cp,[status(thm)],['0.509.2.0','0.265.2.0',theory(equality)]),
% 1.74/2.12 [pos('L','L')]).
% 1.74/2.12 cnf('0.510.0.1',plain,
% 1.74/2.12 ( composition(zero,top) = composition(composition(zero,X1),top) ),
% 1.74/2.12 inference(reduction,[status(thm)],['0.510.0.0','0.63.2.0',theory(equality)]),
% 1.74/2.12 [pos('R.1','L')]).
% 1.74/2.12 cnf('0.510.0.2',plain,
% 1.74/2.12 ( composition(zero,top) = composition(zero,composition(X1,top)) ),
% 1.74/2.12 inference(reduction,[status(thm)],['0.510.0.1','0.4.2.0',theory(equality)]),
% 1.74/2.12 [pos('R','L')]).
% 1.74/2.12 cnf('0.510.1.0',plain,
% 1.74/2.12 ( composition(zero,top) = composition(zero,composition(X1,top)) ),
% 1.74/2.12 inference(weigh,[status(thm)],['0.510.0.2']),
% 1.74/2.12 [weight('<53,509,265,[1,0,0,0]>')]).
% 1.74/2.12 cnf('0.510.2.0',plain,
% 1.74/2.12 ( composition(zero,composition(X1,top)) = composition(zero,top) ),
% 1.74/2.12 inference(orient,[status(thm)],['0.510.1.0',theory(equality)]),
% 1.74/2.12 [x,rule_505]).
% 1.74/2.12 cnf('0.516.0.0',plain,
% 1.74/2.12 ( composition(join(composition(zero,X1),X2),top) = join(composition(zero,top),composition(X2,top)) ),
% 1.74/2.12 inference(cp,[status(thm)],['0.214.2.0','0.510.2.0',theory(equality)]),
% 1.74/2.12 [pos('L.1','L')]).
% 1.74/2.12 cnf('0.516.0.1',plain,
% 1.74/2.12 ( composition(join(composition(zero,X1),X2),top) = composition(join(zero,X2),top) ),
% 1.74/2.12 inference(reduction,[status(thm)],['0.516.0.0','0.5.2.0',theory(equality)]),
% 1.74/2.12 [pos('R','L')]).
% 1.74/2.12 cnf('0.516.0.2',plain,
% 1.74/2.12 ( composition(join(composition(zero,X1),X2),top) = composition(X2,top) ),
% 1.74/2.12 inference(reduction,[status(thm)],['0.516.0.1','0.63.2.0',theory(equality)]),
% 1.74/2.12 [pos('R.1','L')]).
% 1.74/2.12 cnf('0.516.1.0',plain,
% 1.74/2.12 ( composition(join(composition(zero,X1),X2),top) = composition(X2,top) ),
% 1.74/2.12 inference(weigh,[status(thm)],['0.516.0.2']),
% 1.74/2.12 [weight('<87,510,214,[0,0,0,1]>')]).
% 1.74/2.12 cnf('0.516.2.0',plain,
% 1.74/2.12 ( composition(join(composition(zero,X1),X2),top) = composition(X2,top) ),
% 1.74/2.12 inference(orient,[status(thm)],['0.516.1.0',theory(equality)]),
% 1.74/2.12 [u,rule_511]).
% 1.74/2.12 cnf('0.517.0.0',plain,
% 1.74/2.12 ( composition(complement(composition(zero,X1)),top) = composition(top,top) ),
% 1.74/2.12 inference(cp,[status(thm)],['0.516.2.0','0.10.2.0',theory(equality)]),
% 1.74/2.12 [pos('L.1','L')]).
% 1.74/2.12 cnf('0.517.1.0',plain,
% 1.74/2.12 ( composition(complement(composition(zero,X1)),top) = composition(top,top) ),
% 1.74/2.12 inference(weigh,[status(thm)],['0.517.0.0']),
% 1.74/2.12 [weight('<69,516,10,[1,0,0,1]>')]).
% 1.74/2.12 cnf('0.517.2.0',plain,
% 1.74/2.12 ( composition(complement(composition(zero,X1)),top) = composition(top,top) ),
% 1.74/2.12 inference(orient,[status(thm)],['0.517.1.0',theory(equality)]),
% 1.74/2.12 [u,rule_512]).
% 1.74/2.12 cnf('0.525.0.0',plain,
% 1.74/2.12 ( composition(top,converse(complement(composition(zero,X1)))) = converse(composition(top,top)) ),
% 1.74/2.12 inference(cp,[status(thm)],['0.58.2.0','0.517.2.0',theory(equality)]),
% 1.74/2.12 [pos('L.1','L')]).
% 1.74/2.12 cnf('0.525.0.1',plain,
% 1.74/2.12 ( composition(top,complement(converse(composition(zero,X1)))) = converse(composition(top,top)) ),
% 1.74/2.12 inference(reduction,[status(thm)],['0.525.0.0','0.181.2.0',theory(equality)]),
% 1.74/2.12 [pos('L.2','L')]).
% 1.74/2.12 cnf('0.525.0.2',plain,
% 1.74/2.12 ( composition(top,complement(composition(converse(X1),zero))) = converse(composition(top,top)) ),
% 1.74/2.12 inference(reduction,[status(thm)],['0.525.0.1','0.78.2.0',theory(equality)]),
% 1.74/2.12 [pos('L.2.1','L')]).
% 1.74/2.12 cnf('0.525.0.3',plain,
% 1.74/2.12 ( composition(top,complement(composition(converse(X1),zero))) = composition(converse(top),top) ),
% 1.74/2.12 inference(reduction,[status(thm)],['0.525.0.2','0.59.2.0',theory(equality)]),
% 1.74/2.12 [pos('R','L')]).
% 1.74/2.12 cnf('0.525.0.4',plain,
% 1.74/2.12 ( composition(top,complement(composition(converse(X1),zero))) = composition(top,top) ),
% 1.74/2.12 inference(reduction,[status(thm)],['0.525.0.3','0.56.2.0',theory(equality)]),
% 1.74/2.12 [pos('R.1','L')]).
% 1.74/2.12 cnf('0.525.1.0',plain,
% 1.74/2.12 ( composition(top,complement(composition(converse(X1),zero))) = composition(top,top) ),
% 1.74/2.12 inference(weigh,[status(thm)],['0.525.0.4']),
% 1.74/2.12 [weight('<87,517,58,[0,0,0,1]>')]).
% 1.74/2.12 cnf('0.525.2.0',plain,
% 1.74/2.12 ( composition(top,complement(composition(converse(X1),zero))) = composition(top,top) ),
% 1.74/2.12 inference(orient,[status(thm)],['0.525.1.0',theory(equality)]),
% 1.74/2.12 [u,rule_520]).
% 1.74/2.12 cnf('0.526.0.0',plain,
% 1.74/2.12 ( complement(complement(composition(converse(X1),zero))) = join(complement(complement(composition(converse(X1),zero))),composition(converse(top),complement(composition(top,top)))) ),
% 1.74/2.12 inference(cp,[status(thm)],['0.11.2.0','0.525.2.0',theory(equality)]),
% 1.74/2.12 [pos('L.2.2.1','L')]).
% 1.74/2.12 cnf('0.526.0.1',plain,
% 1.74/2.12 ( composition(converse(X1),zero) = join(complement(complement(composition(converse(X1),zero))),composition(converse(top),complement(composition(top,top)))) ),
% 1.74/2.12 inference(reduction,[status(thm)],['0.526.0.0','0.68.2.0',theory(equality)]),
% 1.74/2.12 [pos('L','L')]).
% 1.74/2.12 cnf('0.526.0.2',plain,
% 1.74/2.12 ( composition(converse(X1),zero) = join(composition(converse(X1),zero),composition(converse(top),complement(composition(top,top)))) ),
% 1.74/2.12 inference(reduction,[status(thm)],['0.526.0.1','0.68.2.0',theory(equality)]),
% 1.74/2.12 [pos('R.1','L')]).
% 1.74/2.12 cnf('0.526.0.3',plain,
% 1.74/2.12 ( composition(converse(X1),zero) = join(composition(converse(X1),zero),composition(top,complement(composition(top,top)))) ),
% 1.74/2.12 inference(reduction,[status(thm)],['0.526.0.2','0.56.2.0',theory(equality)]),
% 1.74/2.12 [pos('R.2.1','L')]).
% 1.74/2.12 cnf('0.526.0.4',plain,
% 1.74/2.12 ( composition(converse(X1),zero) = join(composition(converse(X1),zero),composition(top,zero)) ),
% 1.74/2.12 inference(reduction,[status(thm)],['0.526.0.3','0.474.2.0',theory(equality)]),
% 1.74/2.12 [pos('R.2','L')]).
% 1.74/2.12 cnf('0.526.0.5',plain,
% 1.74/2.12 ( composition(converse(X1),zero) = composition(join(converse(X1),top),zero) ),
% 1.74/2.12 inference(reduction,[status(thm)],['0.526.0.4','0.5.2.0',theory(equality)]),
% 1.74/2.12 [pos('R','L')]).
% 1.74/2.12 cnf('0.526.0.6',plain,
% 1.74/2.12 ( composition(converse(X1),zero) = composition(top,zero) ),
% 1.74/2.12 inference(reduction,[status(thm)],['0.526.0.5','0.54.2.0',theory(equality)]),
% 1.74/2.12 [pos('R.1','L')]).
% 1.74/2.12 cnf('0.526.1.0',plain,
% 1.74/2.12 ( composition(converse(X1),zero) = composition(top,zero) ),
% 1.74/2.12 inference(weigh,[status(thm)],['0.526.0.6']),
% 1.74/2.12 [weight('<39,525,11,[0,0,0,7]>')]).
% 1.74/2.12 cnf('0.526.2.0',plain,
% 1.74/2.12 ( composition(converse(X1),zero) = composition(top,zero) ),
% 1.74/2.12 inference(orient,[status(thm)],['0.526.1.0',theory(equality)]),
% 1.74/2.12 [u,rule_521]).
% 1.74/2.12 cnf('0.527.0.0',plain,
% 1.74/2.12 ( composition(converse(meet(meet(one,X1),X2)),zero) = zero ),
% 1.74/2.12 inference(interreduction_right,[status(thm)],['0.492.2.0'])).
% 1.74/2.12 cnf('0.527.0.1',plain,
% 1.74/2.12 ( composition(top,zero) = zero ),
% 1.74/2.12 inference(reduction,[status(thm)],['0.527.0.0','0.526.2.0',theory(equality)]),
% 1.74/2.12 [pos('L','L')]).
% 1.74/2.12 cnf('0.527.1.0',plain,
% 1.74/2.12 ( composition(top,zero) = zero ),
% 1.74/2.12 inference(weigh,[status(thm)],['0.527.0.1']),
% 1.74/2.12 [weight('<19,492,526,[0,0,0,0]>')]).
% 1.74/2.12 cnf('0.527.2.0',plain,
% 1.74/2.12 ( composition(top,zero) = zero ),
% 1.74/2.12 inference(orient,[status(thm)],['0.527.1.0',theory(equality)]),
% 1.74/2.12 [u,rule_522]).
% 1.74/2.12 cnf('0.528.0.0',plain,
% 1.74/2.12 ( composition(meet(X1,composition(top,zero)),zero) = composition(X1,zero) ),
% 1.74/2.12 inference(interreduction_right,[status(thm)],['0.428.2.0'])).
% 1.74/2.12 cnf('0.528.0.1',plain,
% 1.74/2.12 ( composition(meet(X1,zero),zero) = composition(X1,zero) ),
% 1.74/2.12 inference(reduction,[status(thm)],['0.528.0.0','0.527.2.0',theory(equality)]),
% 1.74/2.12 [pos('L.1.2','L')]).
% 1.74/2.12 cnf('0.528.0.2',plain,
% 1.74/2.12 ( composition(zero,zero) = composition(X1,zero) ),
% 1.74/2.12 inference(reduction,[status(thm)],['0.528.0.1','0.70.2.0',theory(equality)]),
% 1.74/2.12 [pos('L.1','L')]).
% 1.74/2.12 cnf('0.528.0.3',plain,
% 1.74/2.12 ( zero = composition(X1,zero) ),
% 1.74/2.12 inference(reduction,[status(thm)],['0.528.0.2','0.429.2.0',theory(equality)]),
% 1.74/2.12 [pos('L','L')]).
% 1.74/2.12 cnf('0.528.1.0',plain,
% 1.74/2.12 ( zero = composition(X1,zero) ),
% 1.74/2.12 inference(weigh,[status(thm)],['0.528.0.3']),
% 1.74/2.12 [weight('<19,428,527,[0,0,0,0]>')]).
% 1.74/2.12 cnf('0.528.2.0',plain,
% 1.74/2.12 ( composition(X1,zero) = zero ),
% 1.74/2.12 inference(orient,[status(thm)],['0.528.1.0',theory(equality)]),
% 1.74/2.12 [x,rule_523]).
% 1.74/2.12 cnf('0.529.0.0',plain,
% 1.74/2.12 ( composition(converse(zero),X1) = converse(zero) ),
% 1.74/2.12 inference(cp,[status(thm)],['0.30.2.0','0.528.2.0',theory(equality)]),
% 1.74/2.12 [pos('L.1','L')]).
% 1.74/2.12 cnf('0.529.0.1',plain,
% 1.74/2.12 ( composition(zero,X1) = converse(zero) ),
% 1.74/2.12 inference(reduction,[status(thm)],['0.529.0.0','0.76.2.0',theory(equality)]),
% 1.74/2.12 [pos('L.1','L')]).
% 1.74/2.12 cnf('0.529.0.2',plain,
% 1.74/2.12 ( composition(zero,X1) = zero ),
% 1.74/2.12 inference(reduction,[status(thm)],['0.529.0.1','0.76.2.0',theory(equality)]),
% 1.74/2.12 [pos('R','L')]).
% 1.74/2.12 cnf('0.529.1.0',plain,
% 1.74/2.12 ( composition(zero,X1) = zero ),
% 1.74/2.12 inference(weigh,[status(thm)],['0.529.0.2']),
% 1.74/2.12 [weight('<19,528,30,[0,0,0,1]>')]).
% 1.74/2.12 cnf('0.529.2.0',plain,
% 1.74/2.12 ( composition(zero,X1) = zero ),
% 1.74/2.12 inference(orient,[status(thm)],['0.529.1.0',theory(equality)]),
% 1.74/2.12 [u,rule_524]).
% 1.74/2.12 cnf('0.530.0.0',plain,
% 1.74/2.12 ( composition(complement(composition(top,top)),top) = composition(zero,top) ),
% 1.74/2.12 inference(interreduction_right,[status(thm)],['0.473.2.0'])).
% 1.74/2.12 cnf('0.530.0.1',plain,
% 1.74/2.12 ( composition(complement(composition(top,top)),top) = zero ),
% 1.74/2.12 inference(reduction,[status(thm)],['0.530.0.0','0.529.2.0',theory(equality)]),
% 1.74/2.12 [pos('R','L')]).
% 1.74/2.12 cnf('0.530.1.0',plain,
% 1.74/2.12 ( composition(complement(composition(top,top)),top) = zero ),
% 1.74/2.12 inference(weigh,[status(thm)],['0.530.0.1']),
% 1.74/2.12 [weight('<55,473,529,[0,0,0,0]>')]).
% 1.74/2.12 cnf('0.530.2.0',plain,
% 1.74/2.12 ( composition(complement(composition(top,top)),top) = zero ),
% 1.74/2.12 inference(orient,[status(thm)],['0.530.1.0',theory(equality)]),
% 1.74/2.12 [u,rule_525]).
% 1.74/2.12 cnf('0.532.0.0',plain,
% 1.74/2.12 ( composition(meet(converse(complement(composition(top,top))),composition(top,converse(X1))),meet(X1,composition(complement(composition(top,top)),top))) = join(meet(composition(converse(complement(composition(top,top))),X1),top),composition(meet(converse(complement(composition(top,top))),composition(top,converse(X1))),meet(X1,zero))) ),
% 1.74/2.12 inference(cp,[status(thm)],['0.469.2.0','0.530.2.0',theory(equality)]),
% 1.74/2.12 [pos('L.2.2.2','L')]).
% 1.74/2.12 cnf('0.532.0.1',plain,
% 1.74/2.12 ( composition(meet(complement(converse(composition(top,top))),composition(top,converse(X1))),meet(X1,composition(complement(composition(top,top)),top))) = join(meet(composition(converse(complement(composition(top,top))),X1),top),composition(meet(converse(complement(composition(top,top))),composition(top,converse(X1))),meet(X1,zero))) ),
% 1.74/2.12 inference(reduction,[status(thm)],['0.532.0.0','0.181.2.0',theory(equality)]),
% 1.74/2.12 [pos('L.1.1','L')]).
% 1.74/2.12 cnf('0.532.0.2',plain,
% 1.74/2.12 ( composition(meet(complement(composition(converse(top),top)),composition(top,converse(X1))),meet(X1,composition(complement(composition(top,top)),top))) = join(meet(composition(converse(complement(composition(top,top))),X1),top),composition(meet(converse(complement(composition(top,top))),composition(top,converse(X1))),meet(X1,zero))) ),
% 1.74/2.12 inference(reduction,[status(thm)],['0.532.0.1','0.59.2.0',theory(equality)]),
% 1.74/2.12 [pos('L.1.1.1','L')]).
% 1.74/2.12 cnf('0.532.0.3',plain,
% 1.74/2.12 ( composition(meet(complement(composition(top,top)),composition(top,converse(X1))),meet(X1,composition(complement(composition(top,top)),top))) = join(meet(composition(converse(complement(composition(top,top))),X1),top),composition(meet(converse(complement(composition(top,top))),composition(top,converse(X1))),meet(X1,zero))) ),
% 1.74/2.12 inference(reduction,[status(thm)],['0.532.0.2','0.56.2.0',theory(equality)]),
% 1.74/2.12 [pos('L.1.1.1.1','L')]).
% 1.74/2.12 cnf('0.532.0.4',plain,
% 1.74/2.12 ( composition(meet(complement(composition(top,top)),composition(top,converse(X1))),meet(X1,zero)) = join(meet(composition(converse(complement(composition(top,top))),X1),top),composition(meet(converse(complement(composition(top,top))),composition(top,converse(X1))),meet(X1,zero))) ),
% 1.74/2.12 inference(reduction,[status(thm)],['0.532.0.3','0.530.2.0',theory(equality)]),
% 1.74/2.12 [pos('L.2.2','L')]).
% 1.74/2.12 cnf('0.532.0.5',plain,
% 1.74/2.12 ( composition(meet(complement(composition(top,top)),composition(top,converse(X1))),zero) = join(meet(composition(converse(complement(composition(top,top))),X1),top),composition(meet(converse(complement(composition(top,top))),composition(top,converse(X1))),meet(X1,zero))) ),
% 1.74/2.12 inference(reduction,[status(thm)],['0.532.0.4','0.70.2.0',theory(equality)]),
% 1.74/2.12 [pos('L.2','L')]).
% 1.74/2.12 cnf('0.532.0.6',plain,
% 1.74/2.12 ( zero = join(meet(composition(converse(complement(composition(top,top))),X1),top),composition(meet(converse(complement(composition(top,top))),composition(top,converse(X1))),meet(X1,zero))) ),
% 1.74/2.12 inference(reduction,[status(thm)],['0.532.0.5','0.528.2.0',theory(equality)]),
% 1.74/2.12 [pos('L','L')]).
% 1.74/2.12 cnf('0.532.0.7',plain,
% 1.74/2.12 ( zero = join(composition(converse(complement(composition(top,top))),X1),composition(meet(converse(complement(composition(top,top))),composition(top,converse(X1))),meet(X1,zero))) ),
% 1.74/2.12 inference(reduction,[status(thm)],['0.532.0.6','0.73.2.0',theory(equality)]),
% 1.74/2.12 [pos('R.1','L')]).
% 1.74/2.12 cnf('0.532.0.8',plain,
% 1.74/2.12 ( zero = join(composition(complement(converse(composition(top,top))),X1),composition(meet(converse(complement(composition(top,top))),composition(top,converse(X1))),meet(X1,zero))) ),
% 1.74/2.12 inference(reduction,[status(thm)],['0.532.0.7','0.181.2.0',theory(equality)]),
% 1.74/2.12 [pos('R.1.1','L')]).
% 1.74/2.12 cnf('0.532.0.9',plain,
% 1.74/2.12 ( zero = join(composition(complement(composition(converse(top),top)),X1),composition(meet(converse(complement(composition(top,top))),composition(top,converse(X1))),meet(X1,zero))) ),
% 1.74/2.12 inference(reduction,[status(thm)],['0.532.0.8','0.59.2.0',theory(equality)]),
% 1.74/2.12 [pos('R.1.1.1','L')]).
% 1.74/2.12 cnf('0.532.0.10',plain,
% 1.74/2.12 ( zero = join(composition(complement(composition(top,top)),X1),composition(meet(converse(complement(composition(top,top))),composition(top,converse(X1))),meet(X1,zero))) ),
% 1.74/2.12 inference(reduction,[status(thm)],['0.532.0.9','0.56.2.0',theory(equality)]),
% 1.74/2.12 [pos('R.1.1.1.1','L')]).
% 1.74/2.12 cnf('0.532.0.11',plain,
% 1.74/2.12 ( zero = join(composition(complement(composition(top,top)),X1),composition(meet(complement(converse(composition(top,top))),composition(top,converse(X1))),meet(X1,zero))) ),
% 1.74/2.12 inference(reduction,[status(thm)],['0.532.0.10','0.181.2.0',theory(equality)]),
% 1.74/2.12 [pos('R.2.1.1','L')]).
% 1.74/2.12 cnf('0.532.0.12',plain,
% 1.74/2.12 ( zero = join(composition(complement(composition(top,top)),X1),composition(meet(complement(composition(converse(top),top)),composition(top,converse(X1))),meet(X1,zero))) ),
% 1.74/2.12 inference(reduction,[status(thm)],['0.532.0.11','0.59.2.0',theory(equality)]),
% 1.74/2.12 [pos('R.2.1.1.1','L')]).
% 1.74/2.12 cnf('0.532.0.13',plain,
% 1.74/2.12 ( zero = join(composition(complement(composition(top,top)),X1),composition(meet(complement(composition(top,top)),composition(top,converse(X1))),meet(X1,zero))) ),
% 1.74/2.12 inference(reduction,[status(thm)],['0.532.0.12','0.56.2.0',theory(equality)]),
% 1.74/2.12 [pos('R.2.1.1.1.1','L')]).
% 1.74/2.12 cnf('0.532.0.14',plain,
% 1.74/2.12 ( zero = join(composition(complement(composition(top,top)),X1),composition(meet(complement(composition(top,top)),composition(top,converse(X1))),zero)) ),
% 1.74/2.12 inference(reduction,[status(thm)],['0.532.0.13','0.70.2.0',theory(equality)]),
% 1.74/2.12 [pos('R.2.2','L')]).
% 1.74/2.12 cnf('0.532.0.15',plain,
% 1.74/2.12 ( zero = join(composition(complement(composition(top,top)),X1),zero) ),
% 1.74/2.12 inference(reduction,[status(thm)],['0.532.0.14','0.528.2.0',theory(equality)]),
% 1.74/2.12 [pos('R.2','L')]).
% 1.74/2.12 cnf('0.532.0.16',plain,
% 1.74/2.12 ( zero = composition(complement(composition(top,top)),X1) ),
% 1.74/2.12 inference(reduction,[status(thm)],['0.532.0.15','0.66.2.0',theory(equality)]),
% 1.74/2.12 [pos('R','L')]).
% 1.74/2.12 cnf('0.532.1.0',plain,
% 1.74/2.12 ( zero = composition(complement(composition(top,top)),X1) ),
% 1.74/2.12 inference(weigh,[status(thm)],['0.532.0.16']),
% 1.74/2.12 [weight('<55,530,469,[0,0,0,17]>')]).
% 1.74/2.12 cnf('0.532.2.0',plain,
% 1.74/2.12 ( composition(complement(composition(top,top)),X1) = zero ),
% 1.74/2.12 inference(orient,[status(thm)],['0.532.1.0',theory(equality)]),
% 1.74/2.12 [x,rule_527]).
% 1.74/2.12 cnf('0.533.0.0',plain,
% 1.74/2.12 ( zero = complement(composition(top,top)) ),
% 1.74/2.12 inference(cp,[status(thm)],['0.532.2.0','0.1.2.0',theory(equality)]),
% 1.74/2.12 [pos('L','L')]).
% 1.74/2.12 cnf('0.533.1.0',plain,
% 1.74/2.12 ( zero = complement(composition(top,top)) ),
% 1.74/2.12 inference(weigh,[status(thm)],['0.533.0.0']),
% 1.74/2.12 [weight('<29,532,1,[1,0,0,0]>')]).
% 1.74/2.12 cnf('0.533.2.0',plain,
% 1.74/2.12 ( complement(composition(top,top)) = zero ),
% 1.74/2.12 inference(orient,[status(thm)],['0.533.1.0',theory(equality)]),
% 1.74/2.12 [x,rule_528]).
% 1.74/2.12 cnf('0.534.0.0',plain,
% 1.74/2.12 ( top = join(composition(top,top),zero) ),
% 1.74/2.12 inference(cp,[status(thm)],['0.10.2.0','0.533.2.0',theory(equality)]),
% 1.74/2.12 [pos('L.2','L')]).
% 1.74/2.12 cnf('0.534.0.1',plain,
% 1.74/2.12 ( top = composition(top,top) ),
% 1.74/2.12 inference(reduction,[status(thm)],['0.534.0.0','0.66.2.0',theory(equality)]),
% 1.74/2.12 [pos('R','L')]).
% 1.74/2.12 cnf('0.534.1.0',plain,
% 1.74/2.12 ( top = composition(top,top) ),
% 1.74/2.12 inference(weigh,[status(thm)],['0.534.0.1']),
% 1.74/2.12 [weight('<19,533,10,[0,0,0,2]>')]).
% 1.74/2.12 cnf('0.534.2.0',plain,
% 1.74/2.12 ( composition(top,top) = top ),
% 1.74/2.12 inference(orient,[status(thm)],['0.534.1.0',theory(equality)]),
% 1.74/2.12 [x,rule_529]).
% 1.74/2.12 cnf('0.535.0.0',plain,
% 1.74/2.12 ( meet(X1,composition(meet(top,composition(X1,converse(top))),top)) = join(meet(top,X1),meet(X1,composition(meet(top,composition(X1,converse(top))),top))) ),
% 1.74/2.12 inference(cp,[status(thm)],['0.163.2.0','0.534.2.0',theory(equality)]),
% 1.74/2.12 [pos('L.1.1','L')]).
% 1.74/2.12 cnf('0.535.0.1',plain,
% 1.74/2.12 ( meet(X1,composition(composition(X1,converse(top)),top)) = join(meet(top,X1),meet(X1,composition(meet(top,composition(X1,converse(top))),top))) ),
% 1.74/2.12 inference(reduction,[status(thm)],['0.535.0.0','0.72.2.0',theory(equality)]),
% 1.74/2.12 [pos('L.2.1','L')]).
% 1.74/2.12 cnf('0.535.0.2',plain,
% 1.74/2.12 ( meet(X1,composition(X1,composition(converse(top),top))) = join(meet(top,X1),meet(X1,composition(meet(top,composition(X1,converse(top))),top))) ),
% 1.74/2.12 inference(reduction,[status(thm)],['0.535.0.1','0.4.2.0',theory(equality)]),
% 1.74/2.12 [pos('L.2','L')]).
% 1.74/2.12 cnf('0.535.0.3',plain,
% 1.74/2.12 ( meet(X1,composition(X1,composition(top,top))) = join(meet(top,X1),meet(X1,composition(meet(top,composition(X1,converse(top))),top))) ),
% 1.74/2.12 inference(reduction,[status(thm)],['0.535.0.2','0.56.2.0',theory(equality)]),
% 1.74/2.12 [pos('L.2.2.1','L')]).
% 1.74/2.12 cnf('0.535.0.4',plain,
% 1.74/2.12 ( meet(X1,composition(X1,top)) = join(meet(top,X1),meet(X1,composition(meet(top,composition(X1,converse(top))),top))) ),
% 1.74/2.12 inference(reduction,[status(thm)],['0.535.0.3','0.534.2.0',theory(equality)]),
% 1.74/2.12 [pos('L.2.2','L')]).
% 1.74/2.12 cnf('0.535.0.5',plain,
% 1.74/2.12 ( meet(X1,composition(X1,top)) = join(X1,meet(X1,composition(meet(top,composition(X1,converse(top))),top))) ),
% 1.74/2.12 inference(reduction,[status(thm)],['0.535.0.4','0.72.2.0',theory(equality)]),
% 1.74/2.12 [pos('R.1','L')]).
% 1.74/2.12 cnf('0.535.0.6',plain,
% 1.74/2.12 ( meet(X1,composition(X1,top)) = X1 ),
% 1.74/2.12 inference(reduction,[status(thm)],['0.535.0.5','0.80.2.0',theory(equality)]),
% 1.74/2.12 [pos('R','L')]).
% 1.74/2.12 cnf('0.535.1.0',plain,
% 1.74/2.12 ( meet(X1,composition(X1,top)) = X1 ),
% 1.74/2.12 inference(weigh,[status(thm)],['0.535.0.6']),
% 1.74/2.12 [weight('<41,534,163,[0,0,0,2]>')]).
% 1.74/2.12 cnf('0.535.2.0',plain,
% 1.74/2.12 ( meet(X1,composition(X1,top)) = X1 ),
% 1.74/2.12 inference(orient,[status(thm)],['0.535.1.0',theory(equality)]),
% 1.74/2.12 [u,rule_530]).
% 1.74/2.12 cnf('0.571.0.0',plain,
% 1.74/2.12 ( composition(meet(X1,composition(composition(X2,X3),converse(X4))),meet(X4,composition(converse(X1),composition(X2,X3)))) = join(meet(composition(X1,X4),composition(X2,X3)),composition(meet(X1,composition(X2,composition(X3,converse(X4)))),meet(X4,composition(converse(X1),composition(X2,X3))))) ),
% 1.74/2.12 inference(cp,[status(thm)],['0.6.2.0','0.4.2.0',theory(equality)]),
% 1.74/2.12 [pos('L.2.1.2','L')]).
% 1.74/2.12 cnf('0.571.0.1',plain,
% 1.74/2.12 ( composition(meet(X1,composition(X2,composition(X3,converse(X4)))),meet(X4,composition(converse(X1),composition(X2,X3)))) = join(meet(composition(X1,X4),composition(X2,X3)),composition(meet(X1,composition(X2,composition(X3,converse(X4)))),meet(X4,composition(converse(X1),composition(X2,X3))))) ),
% 1.74/2.12 inference(reduction,[status(thm)],['0.571.0.0','0.4.2.0',theory(equality)]),
% 1.74/2.12 [pos('L.1.2','L')]).
% 1.74/2.12 cnf('0.571.1.0',plain,
% 1.74/2.12 ( composition(meet(X1,composition(X2,composition(X3,converse(X4)))),meet(X4,composition(converse(X1),composition(X2,X3)))) = join(meet(composition(X1,X4),composition(X2,X3)),composition(meet(X1,composition(X2,composition(X3,converse(X4)))),meet(X4,composition(converse(X1),composition(X2,X3))))) ),
% 1.74/2.12 inference(weigh,[status(thm)],['0.571.0.1']),
% 1.74/2.12 [weight('<?,6,4,[1,0,0,9]>')]).
% 1.74/2.12 cnf('0.571.2.0',plain,
% 1.74/2.12 ( join(meet(composition(X1,X2),composition(X3,X4)),composition(meet(X1,composition(X3,composition(X4,converse(X2)))),meet(X2,composition(converse(X1),composition(X3,X4))))) = composition(meet(X1,composition(X3,composition(X4,converse(X2)))),meet(X2,composition(converse(X1),composition(X3,X4)))) ),
% 1.74/2.12 inference(orient,[status(thm)],['0.571.1.0',theory(equality)]),
% 1.74/2.12 [x,rule_566]).
% 1.74/2.12 cnf('0.808.0.0',plain,
% 1.74/2.12 ( composition(meet(one,composition(complement(converse(composition(X1,converse(X2)))),composition(X1,converse(X2)))),meet(X2,composition(converse(one),composition(complement(converse(composition(X1,converse(X2)))),X1)))) = join(meet(composition(one,X2),composition(complement(converse(composition(X1,converse(X2)))),X1)),composition(zero,meet(X2,composition(converse(one),composition(complement(converse(composition(X1,converse(X2)))),X1))))) ),
% 1.74/2.12 inference(cp,[status(thm)],['0.571.2.0','0.315.2.0',theory(equality)]),
% 1.74/2.12 [pos('L.2.1','L')]).
% 1.74/2.12 cnf('0.808.0.1',plain,
% 1.74/2.12 ( composition(zero,meet(X2,composition(converse(one),composition(complement(converse(composition(X1,converse(X2)))),X1)))) = join(meet(composition(one,X2),composition(complement(converse(composition(X1,converse(X2)))),X1)),composition(zero,meet(X2,composition(converse(one),composition(complement(converse(composition(X1,converse(X2)))),X1))))) ),
% 1.74/2.12 inference(reduction,[status(thm)],['0.808.0.0','0.315.2.0',theory(equality)]),
% 1.74/2.12 [pos('L.1','L')]).
% 1.74/2.12 cnf('0.808.0.2',plain,
% 1.74/2.12 ( zero = join(meet(composition(one,X2),composition(complement(converse(composition(X1,converse(X2)))),X1)),composition(zero,meet(X2,composition(converse(one),composition(complement(converse(composition(X1,converse(X2)))),X1))))) ),
% 1.74/2.12 inference(reduction,[status(thm)],['0.808.0.1','0.529.2.0',theory(equality)]),
% 1.74/2.12 [pos('L','L')]).
% 1.74/2.12 cnf('0.808.0.3',plain,
% 1.74/2.12 ( zero = join(meet(X2,composition(complement(converse(composition(X1,converse(X2)))),X1)),composition(zero,meet(X2,composition(converse(one),composition(complement(converse(composition(X1,converse(X2)))),X1))))) ),
% 1.74/2.12 inference(reduction,[status(thm)],['0.808.0.2','0.33.2.0',theory(equality)]),
% 1.74/2.12 [pos('R.1.1','L')]).
% 1.74/2.12 cnf('0.808.0.4',plain,
% 1.74/2.12 ( zero = join(meet(X2,composition(complement(composition(X2,converse(X1))),X1)),composition(zero,meet(X2,composition(converse(one),composition(complement(converse(composition(X1,converse(X2)))),X1))))) ),
% 1.74/2.12 inference(reduction,[status(thm)],['0.808.0.3','0.29.2.0',theory(equality)]),
% 1.74/2.12 [pos('R.1.2.1.1','L')]).
% 1.74/2.12 cnf('0.808.0.5',plain,
% 1.74/2.12 ( zero = join(meet(X2,composition(complement(composition(X2,converse(X1))),X1)),zero) ),
% 1.74/2.12 inference(reduction,[status(thm)],['0.808.0.4','0.529.2.0',theory(equality)]),
% 1.74/2.12 [pos('R.2','L')]).
% 1.74/2.12 cnf('0.808.0.6',plain,
% 1.74/2.12 ( zero = meet(X2,composition(complement(composition(X2,converse(X1))),X1)) ),
% 1.74/2.12 inference(reduction,[status(thm)],['0.808.0.5','0.66.2.0',theory(equality)]),
% 1.74/2.12 [pos('R','L')]).
% 1.74/2.12 cnf('0.808.1.0',plain,
% 1.74/2.12 ( zero = meet(X2,composition(complement(composition(X2,converse(X1))),X1)) ),
% 1.74/2.12 inference(weigh,[status(thm)],['0.808.0.6']),
% 1.74/2.12 [weight('<109,571,315,[1,0,0,9]>')]).
% 1.74/2.12 cnf('0.808.2.0',plain,
% 1.74/2.12 ( meet(X1,composition(complement(composition(X1,converse(X2))),X2)) = zero ),
% 1.74/2.12 inference(orient,[status(thm)],['0.808.1.0',theory(equality)]),
% 1.74/2.12 [x,rule_800]).
% 1.74/2.12 cnf('0.1007.0.0',plain,
% 1.74/2.12 ( converse(meet(composition(X1,top),X2)) = meet(converse(X2),composition(top,converse(X1))) ),
% 1.74/2.12 inference(cp,[status(thm)],['0.198.2.0','0.58.2.0',theory(equality)]),
% 1.74/2.12 [pos('L.2','L')]).
% 1.74/2.12 cnf('0.1007.1.0',plain,
% 1.74/2.12 ( converse(meet(composition(X1,top),X2)) = meet(converse(X2),composition(top,converse(X1))) ),
% 1.74/2.12 inference(weigh,[status(thm)],['0.1007.0.0']),
% 1.74/2.12 [weight('<111,198,58,[1,0,0,3]>')]).
% 1.74/2.12 cnf('0.1007.2.0',plain,
% 1.74/2.12 ( meet(converse(X1),composition(top,converse(X2))) = converse(meet(composition(X2,top),X1)) ),
% 1.74/2.12 inference(orient,[status(thm)],['0.1007.1.0',theory(equality)]),
% 1.74/2.12 [x,rule_999]).
% 1.74/2.12 cnf('0.1461.0.0',plain,
% 1.74/2.12 ( composition(converse(X1),X2) = composition(converse(meet(composition(X2,top),X1)),X2) ),
% 1.74/2.12 inference(cp,[status(thm)],['0.419.2.0','0.1007.2.0',theory(equality)]),
% 1.74/2.12 [pos('L.1','L')]).
% 1.74/2.12 cnf('0.1461.1.0',plain,
% 1.74/2.12 ( composition(converse(X1),X2) = composition(converse(meet(composition(X2,top),X1)),X2) ),
% 1.74/2.12 inference(weigh,[status(thm)],['0.1461.0.0']),
% 1.74/2.12 [weight('<116,1007,419,[0,0,0,1]>')]).
% 1.74/2.12 cnf('0.1461.2.0',plain,
% 1.74/2.12 ( composition(converse(meet(composition(X1,top),X2)),X1) = composition(converse(X2),X1) ),
% 1.74/2.12 inference(orient,[status(thm)],['0.1461.1.0',theory(equality)]),
% 1.74/2.12 [x,rule_1449]).
% 1.74/2.12 cnf('0.1683.0.0',plain,
% 1.74/2.12 ( composition(join(one,X1),X2) = join(X2,composition(X1,X2)) ),
% 1.74/2.12 inference(cp,[status(thm)],['0.5.2.0','0.33.2.0',theory(equality)]),
% 1.74/2.12 [pos('L.1','L')]).
% 1.74/2.12 cnf('0.1683.1.0',plain,
% 1.74/2.12 ( composition(join(one,X1),X2) = join(X2,composition(X1,X2)) ),
% 1.74/2.12 inference(weigh,[status(thm)],['0.1683.0.0']),
% 1.74/2.12 [weight('<120,33,5,[0,0,0,1]>')]).
% 1.74/2.12 cnf('0.1683.2.0',plain,
% 1.74/2.12 ( composition(join(one,X1),X2) = join(X2,composition(X1,X2)) ),
% 1.74/2.12 inference(activate,[status(thm)],['0.1683.1.0']),
% 1.74/2.12 [equation_18]).
% 1.74/2.12 cnf('0.1684.0.0',plain,
% 1.74/2.12 ( join(X1,composition(complement(one),X1)) = composition(top,X1) ),
% 1.74/2.12 inference(cp,[status(thm)],['0.1683.2.0','0.10.2.0',theory(equality)]),
% 1.74/2.12 [pos('L.1','L')]).
% 1.74/2.12 cnf('0.1684.1.0',plain,
% 1.74/2.12 ( join(X1,composition(complement(one),X1)) = composition(top,X1) ),
% 1.74/2.12 inference(weigh,[status(thm)],['0.1684.0.0']),
% 1.74/2.12 [weight('<69,1683,10,[1,0,0,1]>')]).
% 1.74/2.12 cnf('0.1684.2.0',plain,
% 1.74/2.12 ( join(X1,composition(complement(one),X1)) = composition(top,X1) ),
% 1.74/2.12 inference(orient,[status(thm)],['0.1684.1.0',theory(equality)]),
% 1.74/2.12 [u,rule_1666]).
% 1.74/2.12 cnf('0.1685.0.0',plain,
% 1.74/2.12 ( join(X1,converse(composition(complement(one),converse(X1)))) = converse(composition(top,converse(X1))) ),
% 1.74/2.12 inference(cp,[status(thm)],['0.45.2.0','0.1684.2.0',theory(equality)]),
% 1.74/2.12 [pos('L.1','L')]).
% 1.74/2.12 cnf('0.1685.0.1',plain,
% 1.74/2.12 ( join(X1,composition(converse(converse(X1)),complement(one))) = converse(composition(top,converse(X1))) ),
% 1.74/2.12 inference(reduction,[status(thm)],['0.1685.0.0','0.167.2.0',theory(equality)]),
% 1.74/2.12 [pos('L.2','L')]).
% 1.74/2.12 cnf('0.1685.0.2',plain,
% 1.74/2.12 ( join(X1,composition(X1,complement(one))) = converse(composition(top,converse(X1))) ),
% 1.74/2.12 inference(reduction,[status(thm)],['0.1685.0.1','0.3.2.0',theory(equality)]),
% 1.74/2.12 [pos('L.2.1','L')]).
% 1.74/2.12 cnf('0.1685.0.3',plain,
% 1.74/2.12 ( join(X1,composition(X1,complement(one))) = composition(converse(converse(X1)),top) ),
% 1.74/2.12 inference(reduction,[status(thm)],['0.1685.0.2','0.59.2.0',theory(equality)]),
% 1.74/2.12 [pos('R','L')]).
% 1.74/2.12 cnf('0.1685.0.4',plain,
% 1.74/2.12 ( join(X1,composition(X1,complement(one))) = composition(X1,top) ),
% 1.74/2.12 inference(reduction,[status(thm)],['0.1685.0.3','0.3.2.0',theory(equality)]),
% 1.74/2.12 [pos('R.1','L')]).
% 1.74/2.12 cnf('0.1685.1.0',plain,
% 1.74/2.12 ( join(X1,composition(X1,complement(one))) = composition(X1,top) ),
% 1.74/2.12 inference(weigh,[status(thm)],['0.1685.0.4']),
% 1.74/2.12 [weight('<69,1684,45,[0,0,0,1]>')]).
% 1.74/2.12 cnf('0.1685.2.0',plain,
% 1.74/2.12 ( join(X1,composition(X1,complement(one))) = composition(X1,top) ),
% 1.74/2.12 inference(orient,[status(thm)],['0.1685.1.0',theory(equality)]),
% 1.74/2.12 [u,rule_1667]).
% 1.74/2.12 cnf('0.1722.0.0',plain,
% 1.74/2.12 ( join(X1,complement(composition(X1,complement(one)))) = join(X1,complement(composition(X1,top))) ),
% 1.74/2.12 inference(cp,[status(thm)],['0.174.2.0','0.1685.2.0',theory(equality)]),
% 1.74/2.12 [pos('L.2.1','L')]).
% 1.74/2.12 cnf('0.1722.1.0',plain,
% 1.74/2.12 ( join(X1,complement(composition(X1,complement(one)))) = join(X1,complement(composition(X1,top))) ),
% 1.74/2.12 inference(weigh,[status(thm)],['0.1722.0.0']),
% 1.74/2.12 [weight('<111,1685,174,[0,0,0,3]>')]).
% 1.74/2.12 cnf('0.1722.2.0',plain,
% 1.74/2.12 ( join(X1,complement(composition(X1,complement(one)))) = join(X1,complement(composition(X1,top))) ),
% 1.74/2.12 inference(orient,[status(thm)],['0.1722.1.0',theory(equality)]),
% 1.74/2.12 [u,rule_1704]).
% 1.74/2.12 cnf('0.1723.0.0',plain,
% 1.74/2.12 ( join(sk1,complement(composition(sk1,complement(one)))) = complement(composition(sk1,complement(one))) ),
% 1.74/2.12 inference(interreduction_right,[status(thm)],['0.349.2.0'])).
% 1.74/2.12 cnf('0.1723.0.1',plain,
% 1.74/2.12 ( join(sk1,complement(composition(sk1,top))) = complement(composition(sk1,complement(one))) ),
% 1.74/2.12 inference(reduction,[status(thm)],['0.1723.0.0','0.1722.2.0',theory(equality)]),
% 1.74/2.12 [pos('L','L')]).
% 1.74/2.12 cnf('0.1723.1.0',plain,
% 1.74/2.12 ( join(sk1,complement(composition(sk1,top))) = complement(composition(sk1,complement(one))) ),
% 1.74/2.12 inference(weigh,[status(thm)],['0.1723.0.1']),
% 1.74/2.12 [weight('<83,349,1722,[0,0,0,0]>')]).
% 1.74/2.12 cnf('0.1723.2.0',plain,
% 1.74/2.12 ( join(sk1,complement(composition(sk1,top))) = complement(composition(sk1,complement(one))) ),
% 1.74/2.12 inference(orient,[status(thm)],['0.1723.1.0',theory(equality)]),
% 1.74/2.12 [u,rule_1705]).
% 1.74/2.12 cnf('0.1727.0.0',plain,
% 1.74/2.12 ( meet(sk1,composition(sk1,top)) = meet(composition(sk1,top),complement(composition(sk1,complement(one)))) ),
% 1.74/2.12 inference(cp,[status(thm)],['0.155.2.0','0.1723.2.0',theory(equality)]),
% 1.74/2.12 [pos('L.2','L')]).
% 1.74/2.12 cnf('0.1727.0.1',plain,
% 1.74/2.12 ( sk1 = meet(composition(sk1,top),complement(composition(sk1,complement(one)))) ),
% 1.74/2.12 inference(reduction,[status(thm)],['0.1727.0.0','0.535.2.0',theory(equality)]),
% 1.74/2.12 [pos('L','L')]).
% 1.74/2.12 cnf('0.1727.1.0',plain,
% 1.74/2.12 ( sk1 = meet(composition(sk1,top),complement(composition(sk1,complement(one)))) ),
% 1.74/2.12 inference(weigh,[status(thm)],['0.1727.0.1']),
% 1.74/2.12 [weight('<109,1723,155,[0,0,0,2]>')]).
% 1.74/2.12 cnf('0.1727.2.0',plain,
% 1.74/2.12 ( meet(composition(sk1,top),complement(composition(sk1,complement(one)))) = sk1 ),
% 1.74/2.12 inference(orient,[status(thm)],['0.1727.1.0',theory(equality)]),
% 1.74/2.12 [x,rule_1709]).
% 1.74/2.12 cnf('0.1732.0.0',plain,
% 1.74/2.12 ( composition(converse(complement(composition(sk1,complement(one)))),sk1) = composition(converse(sk1),sk1) ),
% 1.74/2.12 inference(cp,[status(thm)],['0.1461.2.0','0.1727.2.0',theory(equality)]),
% 1.74/2.12 [pos('L.1.1','L')]).
% 1.74/2.12 cnf('0.1732.0.1',plain,
% 1.74/2.12 ( composition(complement(converse(composition(sk1,complement(one)))),sk1) = composition(converse(sk1),sk1) ),
% 1.74/2.12 inference(reduction,[status(thm)],['0.1732.0.0','0.181.2.0',theory(equality)]),
% 1.74/2.12 [pos('L.1','L')]).
% 1.74/2.12 cnf('0.1732.0.2',plain,
% 1.74/2.12 ( composition(complement(composition(complement(one),converse(sk1))),sk1) = composition(converse(sk1),sk1) ),
% 1.74/2.12 inference(reduction,[status(thm)],['0.1732.0.1','0.166.2.0',theory(equality)]),
% 1.74/2.12 [pos('L.1.1','L')]).
% 1.74/2.12 cnf('0.1732.1.0',plain,
% 1.74/2.12 ( composition(complement(composition(complement(one),converse(sk1))),sk1) = composition(converse(sk1),sk1) ),
% 1.74/2.12 inference(weigh,[status(thm)],['0.1732.0.2']),
% 1.74/2.12 [weight('<116,1727,1461,[0,0,0,2]>')]).
% 1.74/2.12 cnf('0.1732.2.0',plain,
% 1.74/2.12 ( composition(complement(composition(complement(one),converse(sk1))),sk1) = composition(converse(sk1),sk1) ),
% 1.74/2.12 inference(orient,[status(thm)],['0.1732.1.0',theory(equality)]),
% 1.74/2.12 [u,rule_1714]).
% 1.74/2.12 cnf('0.1733.0.0',plain,
% 1.74/2.12 ( zero = meet(complement(one),composition(converse(sk1),sk1)) ),
% 1.74/2.12 inference(cp,[status(thm)],['0.808.2.0','0.1732.2.0',theory(equality)]),
% 1.74/2.12 [pos('L.2','L')]).
% 1.74/2.12 cnf('0.1733.1.0',plain,
% 1.74/2.12 ( zero = meet(complement(one),composition(converse(sk1),sk1)) ),
% 1.74/2.12 inference(weigh,[status(thm)],['0.1733.0.0']),
% 1.74/2.12 [weight('<71,1732,808,[0,0,0,2]>')]).
% 1.74/2.12 cnf('0.1733.2.0',plain,
% 1.74/2.12 ( meet(complement(one),composition(converse(sk1),sk1)) = zero ),
% 1.74/2.12 inference(orient,[status(thm)],['0.1733.1.0',theory(equality)]),
% 1.74/2.12 [x,rule_1715]).
% 1.74/2.12 cnf('0.1734.0.0',plain,
% 1.74/2.12 ( join(one,composition(converse(sk1),sk1)) = join(one,zero) ),
% 1.74/2.12 inference(cp,[status(thm)],['0.149.2.0','0.1733.2.0',theory(equality)]),
% 1.74/2.12 [pos('L.2','L')]).
% 1.74/2.12 cnf('0.1734.0.1',plain,
% 1.74/2.12 ( join(one,composition(converse(sk1),sk1)) = one ),
% 1.74/2.12 inference(reduction,[status(thm)],['0.1734.0.0','0.66.2.0',theory(equality)]),
% 1.74/2.12 [pos('R','L')]).
% 1.74/2.12 cnf('0.1734.1.0',plain,
% 1.74/2.12 ( join(one,composition(converse(sk1),sk1)) = one ),
% 1.74/2.12 inference(weigh,[status(thm)],['0.1734.0.1']),
% 1.74/2.12 [weight('<55,1733,149,[0,0,0,2]>')]).
% 1.74/2.12 cnf('0.1734.2.0',plain,
% 1.74/2.12 ( join(one,composition(converse(sk1),sk1)) = one ),
% 1.74/2.12 inference(orient,[status(thm)],['0.1734.1.0',theory(equality)]),
% 1.74/2.12 [u,rule_1716]).
% 1.74/2.12 cnf('1.0.0.0',conjecture,
% 1.74/2.12 ( join(composition(converse(sk1),sk1),one) = one ),
% 1.74/2.12 file('/tmp/WALDMEISTER_7164_n015',conjecture_1)).
% 1.74/2.12 cnf('1.0.0.1',plain,
% 1.74/2.12 ( join(one,composition(converse(sk1),sk1)) = one ),
% 1.74/2.12 inference(reduction,[status(thm)],['1.0.0.0','0.8.2.0',theory(equality)]),
% 1.74/2.12 [pos('L','L')]).
% 1.74/2.12 cnf('1.0.0.2',plain,
% 1.74/2.12 ( one = one ),
% 1.74/2.12 inference(reduction,[status(thm)],['1.0.0.1','0.1734.2.0',theory(equality)]),
% 1.74/2.12 [pos('L','L')]).
% 1.74/2.12 cnf('1.0.0.3',plain,
% 1.74/2.12 ( $true ),
% 1.74/2.12 inference(trivial,[status(thm)],['1.0.0.2',theory(equality)]),
% 1.74/2.12 [conjecture_1]).
% 1.74/2.12
% 1.74/2.12 Proved Goals:
% 1.74/2.12 No. 1: join(composition(converse(sk1),sk1),one) ?= one joined, current: one = one
% 1.74/2.12 1 goal was specified, which was proved.
% 1.74/2.12 % SZS output end CNFRefutation
% 1.74/2.12 #END OF PROOF
% 1.74/2.12
% 1.74/2.12 Problem WALDMEISTER_7164_n015
% 1.74/2.12 CPs.gen 380012
% 1.74/2.12 CPs.reexp 0
% 1.74/2.12 Select 22571
% 1.74/2.12 R 1716
% 1.74/2.12 E 18
% 1.74/2.12 vsize 9.7M
% 1.74/2.12 rss 5.2M
% 1.74/2.12 process.time 1.058s
% 1.74/2.12 wallclock.time 1.058s
% 1.74/2.12 status S
% 1.74/2.12
% 1.74/2.12
% 1.74/2.12 Waldmeister states: Goal proved.
% 1.74/2.12 % SZS status Unsatisfiable
%------------------------------------------------------------------------------