%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : REL029-4 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n012.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sun Sep 27 08:24:58 AM UTC 2026
% Result : Unsatisfiable 26.81s 18.74s
% Output : CNFRefutation 26.81s
% Verified :
% SZS Type : Refutation
% Derivation depth : 136
% Number of leaves : 18
% Syntax : Number of formulae : 719 ( 700 unt; 0 def)
% Number of atoms : 738 ( 737 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 66 ( 47 ~; 19 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 1 avg)
% Maximal term depth : 11 ( 3 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 11 ( 11 usr; 6 con; 0-2 aty)
% Number of variables : 609 ( 37 sgn 31 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(maddux1_join_commutativity_1,axiom,
! [VAR_0,VAR_1] : join(VAR_0,VAR_1) = join(VAR_1,VAR_0),
file('theBenchmark.p',maddux1_join_commutativity_1) ).
cnf(c_1,plain,
join(A,B) = join(B,A),
inference(clausify,[status(thm)],[maddux1_join_commutativity_1]) ).
fof(maddux2_join_associativity_2,axiom,
! [VAR_0,VAR_1,VAR_2] : join(VAR_0,join(VAR_1,VAR_2)) = join(join(VAR_0,VAR_1),VAR_2),
file('theBenchmark.p',maddux2_join_associativity_2) ).
cnf(c_2,plain,
join(A,join(B,C)) = join(join(A,B),C),
inference(clausify,[status(thm)],[maddux2_join_associativity_2]) ).
cnf(c_3,plain,
join(join(A,B),C) = join(A,join(B,C)),
inference(copy,[status(thm)],[c_2]) ).
fof(maddux3_a_kind_of_de_Morgan_3,axiom,
! [VAR_0,VAR_1] : VAR_0 = join(complement(join(complement(VAR_0),complement(VAR_1))),complement(join(complement(VAR_0),VAR_1))),
file('theBenchmark.p',maddux3_a_kind_of_de_Morgan_3) ).
cnf(c_4,plain,
A = join(complement(join(complement(A),complement(B))),complement(join(complement(A),B))),
inference(clausify,[status(thm)],[maddux3_a_kind_of_de_Morgan_3]) ).
cnf(c_12274,plain,
A = join(complement(join(complement(A),B)),complement(join(complement(A),complement(B)))),
inference(paramod,[status(thm)],[c_1,c_4]) ).
cnf(c_5,plain,
join(complement(join(complement(A),B)),complement(join(complement(A),complement(B)))) = A,
inference(copy,[status(thm)],[c_12274]) ).
fof(maddux4_definiton_of_meet_4,axiom,
! [VAR_0,VAR_1] : meet(VAR_0,VAR_1) = complement(join(complement(VAR_0),complement(VAR_1))),
file('theBenchmark.p',maddux4_definiton_of_meet_4) ).
cnf(c_6,plain,
meet(A,B) = complement(join(complement(A),complement(B))),
inference(clausify,[status(thm)],[maddux4_definiton_of_meet_4]) ).
fof(composition_associativity_5,axiom,
! [VAR_0,VAR_1,VAR_2] : composition(VAR_0,composition(VAR_1,VAR_2)) = composition(composition(VAR_0,VAR_1),VAR_2),
file('theBenchmark.p',composition_associativity_5) ).
cnf(c_7,plain,
composition(A,composition(B,C)) = composition(composition(A,B),C),
inference(clausify,[status(thm)],[composition_associativity_5]) ).
cnf(c_8,plain,
composition(composition(A,B),C) = composition(A,composition(B,C)),
inference(copy,[status(thm)],[c_7]) ).
fof(composition_identity_6,axiom,
! [VAR_0] : composition(VAR_0,one) = VAR_0,
file('theBenchmark.p',composition_identity_6) ).
cnf(c_9,plain,
composition(A,one) = A,
inference(clausify,[status(thm)],[composition_identity_6]) ).
fof(composition_distributivity_7,axiom,
! [VAR_0,VAR_1,VAR_2] : composition(join(VAR_0,VAR_1),VAR_2) = join(composition(VAR_0,VAR_2),composition(VAR_1,VAR_2)),
file('theBenchmark.p',composition_distributivity_7) ).
cnf(c_10,plain,
composition(join(A,B),C) = join(composition(A,C),composition(B,C)),
inference(clausify,[status(thm)],[composition_distributivity_7]) ).
fof(converse_idempotence_8,axiom,
! [VAR_0] : converse(converse(VAR_0)) = VAR_0,
file('theBenchmark.p',converse_idempotence_8) ).
cnf(c_11,plain,
converse(converse(A)) = A,
inference(clausify,[status(thm)],[converse_idempotence_8]) ).
fof(converse_additivity_9,axiom,
! [VAR_0,VAR_1] : converse(join(VAR_0,VAR_1)) = join(converse(VAR_0),converse(VAR_1)),
file('theBenchmark.p',converse_additivity_9) ).
cnf(c_12,plain,
converse(join(A,B)) = join(converse(A),converse(B)),
inference(clausify,[status(thm)],[converse_additivity_9]) ).
fof(converse_multiplicativity_10,axiom,
! [VAR_0,VAR_1] : converse(composition(VAR_0,VAR_1)) = composition(converse(VAR_1),converse(VAR_0)),
file('theBenchmark.p',converse_multiplicativity_10) ).
cnf(c_13,plain,
converse(composition(A,B)) = composition(converse(B),converse(A)),
inference(clausify,[status(thm)],[converse_multiplicativity_10]) ).
fof(converse_cancellativity_11,axiom,
! [VAR_0,VAR_1] : join(composition(converse(VAR_0),complement(composition(VAR_0,VAR_1))),complement(VAR_1)) = complement(VAR_1),
file('theBenchmark.p',converse_cancellativity_11) ).
cnf(c_14,plain,
join(composition(converse(A),complement(composition(A,B))),complement(B)) = complement(B),
inference(clausify,[status(thm)],[converse_cancellativity_11]) ).
cnf(c_15,plain,
join(complement(A),composition(converse(B),complement(composition(B,A)))) = complement(A),
inference(paramod,[status(thm)],[c_1,c_14]) ).
fof(def_top_12,axiom,
! [VAR_0] : top = join(VAR_0,complement(VAR_0)),
file('theBenchmark.p',def_top_12) ).
cnf(c_16,plain,
top = join(A,complement(A)),
inference(clausify,[status(thm)],[def_top_12]) ).
cnf(c_17,plain,
join(A,complement(A)) = top,
inference(copy,[status(thm)],[c_16]) ).
fof(def_zero_13,axiom,
! [VAR_0] : zero = meet(VAR_0,complement(VAR_0)),
file('theBenchmark.p',def_zero_13) ).
cnf(c_18,plain,
zero = meet(A,complement(A)),
inference(clausify,[status(thm)],[def_zero_13]) ).
cnf(c_12275,plain,
zero = complement(join(complement(A),complement(complement(A)))),
inference(paramod,[status(thm)],[c_6,c_18]) ).
cnf(c_12276,plain,
zero = complement(top),
inference(paramod,[status(thm)],[c_17,c_12275]) ).
cnf(c_19,plain,
complement(top) = zero,
inference(copy,[status(thm)],[c_12276]) ).
fof(dedekind_law_14,axiom,
! [VAR_0,VAR_1,VAR_2] : join(meet(composition(VAR_0,VAR_1),VAR_2),composition(meet(VAR_0,composition(VAR_2,converse(VAR_1))),meet(VAR_1,composition(converse(VAR_0),VAR_2)))) = composition(meet(VAR_0,composition(VAR_2,converse(VAR_1))),meet(VAR_1,composition(converse(VAR_0),VAR_2))),
file('theBenchmark.p',dedekind_law_14) ).
cnf(c_20,plain,
join(meet(composition(A,B),C),composition(meet(A,composition(C,converse(B))),meet(B,composition(converse(A),C)))) = composition(meet(A,composition(C,converse(B))),meet(B,composition(converse(A),C))),
inference(clausify,[status(thm)],[dedekind_law_14]) ).
cnf(c_12277,plain,
join(complement(join(complement(composition(A,B)),complement(C))),composition(meet(A,composition(C,converse(B))),meet(B,composition(converse(A),C)))) = composition(meet(A,composition(C,converse(B))),meet(B,composition(converse(A),C))),
inference(paramod,[status(thm)],[c_6,c_20]) ).
cnf(c_12278,plain,
join(complement(join(complement(composition(A,B)),complement(C))),composition(complement(join(complement(A),complement(composition(C,converse(B))))),meet(B,composition(converse(A),C)))) = composition(meet(A,composition(C,converse(B))),meet(B,composition(converse(A),C))),
inference(paramod,[status(thm)],[c_6,c_12277]) ).
cnf(c_12279,plain,
join(complement(join(complement(composition(A,B)),complement(C))),composition(complement(join(complement(A),complement(composition(C,converse(B))))),complement(join(complement(B),complement(composition(converse(A),C)))))) = composition(meet(A,composition(C,converse(B))),meet(B,composition(converse(A),C))),
inference(paramod,[status(thm)],[c_6,c_12278]) ).
cnf(c_12280,plain,
join(complement(join(complement(composition(A,B)),complement(C))),composition(complement(join(complement(A),complement(composition(C,converse(B))))),complement(join(complement(B),complement(composition(converse(A),C)))))) = composition(complement(join(complement(A),complement(composition(C,converse(B))))),meet(B,composition(converse(A),C))),
inference(paramod,[status(thm)],[c_6,c_12279]) ).
cnf(c_21,plain,
join(complement(join(complement(composition(A,B)),complement(C))),composition(complement(join(complement(A),complement(composition(C,converse(B))))),complement(join(complement(B),complement(composition(converse(A),C)))))) = composition(complement(join(complement(A),complement(composition(C,converse(B))))),complement(join(complement(B),complement(composition(converse(A),C))))),
inference(paramod,[status(thm)],[c_6,c_12280]) ).
fof(modular_law_1_15,axiom,
! [VAR_0,VAR_1,VAR_2] : join(meet(composition(VAR_0,VAR_1),VAR_2),meet(composition(VAR_0,meet(VAR_1,composition(converse(VAR_0),VAR_2))),VAR_2)) = meet(composition(VAR_0,meet(VAR_1,composition(converse(VAR_0),VAR_2))),VAR_2),
file('theBenchmark.p',modular_law_1_15) ).
cnf(c_22,plain,
join(meet(composition(A,B),C),meet(composition(A,meet(B,composition(converse(A),C))),C)) = meet(composition(A,meet(B,composition(converse(A),C))),C),
inference(clausify,[status(thm)],[modular_law_1_15]) ).
cnf(c_12281,plain,
join(complement(join(complement(composition(A,B)),complement(C))),meet(composition(A,meet(B,composition(converse(A),C))),C)) = meet(composition(A,meet(B,composition(converse(A),C))),C),
inference(paramod,[status(thm)],[c_6,c_22]) ).
cnf(c_12282,plain,
join(complement(join(complement(composition(A,B)),complement(C))),meet(composition(A,complement(join(complement(B),complement(composition(converse(A),C))))),C)) = meet(composition(A,meet(B,composition(converse(A),C))),C),
inference(paramod,[status(thm)],[c_6,c_12281]) ).
cnf(c_12283,plain,
join(complement(join(complement(composition(A,B)),complement(C))),complement(join(complement(composition(A,complement(join(complement(B),complement(composition(converse(A),C)))))),complement(C)))) = meet(composition(A,meet(B,composition(converse(A),C))),C),
inference(paramod,[status(thm)],[c_6,c_12282]) ).
cnf(c_12284,plain,
join(complement(join(complement(composition(A,B)),complement(C))),complement(join(complement(C),complement(composition(A,complement(join(complement(B),complement(composition(converse(A),C))))))))) = meet(composition(A,meet(B,composition(converse(A),C))),C),
inference(paramod,[status(thm)],[c_1,c_12283]) ).
cnf(c_12285,plain,
join(complement(join(complement(composition(A,B)),complement(C))),complement(join(complement(C),complement(composition(A,complement(join(complement(B),complement(composition(converse(A),C))))))))) = meet(composition(A,complement(join(complement(B),complement(composition(converse(A),C))))),C),
inference(paramod,[status(thm)],[c_6,c_12284]) ).
cnf(c_12286,plain,
join(complement(join(complement(composition(A,B)),complement(C))),complement(join(complement(C),complement(composition(A,complement(join(complement(B),complement(composition(converse(A),C))))))))) = complement(join(complement(composition(A,complement(join(complement(B),complement(composition(converse(A),C)))))),complement(C))),
inference(paramod,[status(thm)],[c_6,c_12285]) ).
cnf(c_23,plain,
join(complement(join(complement(composition(A,B)),complement(C))),complement(join(complement(C),complement(composition(A,complement(join(complement(B),complement(composition(converse(A),C))))))))) = complement(join(complement(C),complement(composition(A,complement(join(complement(B),complement(composition(converse(A),C)))))))),
inference(paramod,[status(thm)],[c_1,c_12286]) ).
fof(goals_17,axiom,
join(sk1,one) = one,
file('theBenchmark.p',goals_17) ).
cnf(c_26,plain,
join(sk1,one) = one,
inference(clausify,[status(thm)],[goals_17]) ).
cnf(c_27,plain,
join(one,sk1) = one,
inference(paramod,[status(thm)],[c_1,c_26]) ).
fof(goals_18,axiom,
join(sk2,one) = one,
file('theBenchmark.p',goals_18) ).
cnf(c_28,plain,
join(sk2,one) = one,
inference(clausify,[status(thm)],[goals_18]) ).
cnf(c_29,plain,
join(one,sk2) = one,
inference(paramod,[status(thm)],[c_1,c_28]) ).
fof(goals_19,axiom,
( join(meet(composition(sk1,sk3),composition(sk2,sk3)),composition(meet(sk1,sk2),sk3)) != composition(meet(sk1,sk2),sk3)
| join(composition(meet(sk1,sk2),sk3),meet(composition(sk1,sk3),composition(sk2,sk3))) != meet(composition(sk1,sk3),composition(sk2,sk3)) ),
file('theBenchmark.p',goals_19) ).
cnf(c_30,plain,
( join(meet(composition(sk1,sk3),composition(sk2,sk3)),composition(meet(sk1,sk2),sk3)) != composition(meet(sk1,sk2),sk3)
| join(composition(meet(sk1,sk2),sk3),meet(composition(sk1,sk3),composition(sk2,sk3))) != meet(composition(sk1,sk3),composition(sk2,sk3)) ),
inference(clausify,[status(thm)],[goals_19]) ).
cnf(c_12287,plain,
( join(meet(composition(sk1,sk3),composition(sk2,sk3)),composition(meet(sk1,sk2),sk3)) != composition(meet(sk1,sk2),sk3)
| join(composition(complement(join(complement(sk1),complement(sk2))),sk3),meet(composition(sk1,sk3),composition(sk2,sk3))) != meet(composition(sk1,sk3),composition(sk2,sk3)) ),
inference(paramod,[status(thm)],[c_6,c_30]) ).
cnf(c_12288,plain,
( join(meet(composition(sk1,sk3),composition(sk2,sk3)),composition(meet(sk1,sk2),sk3)) != composition(meet(sk1,sk2),sk3)
| join(composition(complement(join(complement(sk1),complement(sk2))),sk3),complement(join(complement(composition(sk1,sk3)),complement(composition(sk2,sk3))))) != meet(composition(sk1,sk3),composition(sk2,sk3)) ),
inference(paramod,[status(thm)],[c_6,c_12287]) ).
cnf(c_12289,plain,
( join(meet(composition(sk1,sk3),composition(sk2,sk3)),composition(meet(sk1,sk2),sk3)) != composition(meet(sk1,sk2),sk3)
| join(complement(join(complement(composition(sk1,sk3)),complement(composition(sk2,sk3)))),composition(complement(join(complement(sk1),complement(sk2))),sk3)) != meet(composition(sk1,sk3),composition(sk2,sk3)) ),
inference(paramod,[status(thm)],[c_1,c_12288]) ).
cnf(c_12290,plain,
( join(meet(composition(sk1,sk3),composition(sk2,sk3)),composition(meet(sk1,sk2),sk3)) != composition(meet(sk1,sk2),sk3)
| join(complement(join(complement(composition(sk1,sk3)),complement(composition(sk2,sk3)))),composition(complement(join(complement(sk1),complement(sk2))),sk3)) != complement(join(complement(composition(sk1,sk3)),complement(composition(sk2,sk3)))) ),
inference(paramod,[status(thm)],[c_6,c_12289]) ).
cnf(c_12291,plain,
( join(complement(join(complement(composition(sk1,sk3)),complement(composition(sk2,sk3)))),composition(meet(sk1,sk2),sk3)) != composition(meet(sk1,sk2),sk3)
| join(complement(join(complement(composition(sk1,sk3)),complement(composition(sk2,sk3)))),composition(complement(join(complement(sk1),complement(sk2))),sk3)) != complement(join(complement(composition(sk1,sk3)),complement(composition(sk2,sk3)))) ),
inference(paramod,[status(thm)],[c_6,c_12290]) ).
cnf(c_12292,plain,
( join(complement(join(complement(composition(sk1,sk3)),complement(composition(sk2,sk3)))),composition(complement(join(complement(sk1),complement(sk2))),sk3)) != composition(meet(sk1,sk2),sk3)
| join(complement(join(complement(composition(sk1,sk3)),complement(composition(sk2,sk3)))),composition(complement(join(complement(sk1),complement(sk2))),sk3)) != complement(join(complement(composition(sk1,sk3)),complement(composition(sk2,sk3)))) ),
inference(paramod,[status(thm)],[c_6,c_12291]) ).
cnf(c_31,plain,
( join(complement(join(complement(composition(sk1,sk3)),complement(composition(sk2,sk3)))),composition(complement(join(complement(sk1),complement(sk2))),sk3)) != composition(complement(join(complement(sk1),complement(sk2))),sk3)
| join(complement(join(complement(composition(sk1,sk3)),complement(composition(sk2,sk3)))),composition(complement(join(complement(sk1),complement(sk2))),sk3)) != complement(join(complement(composition(sk1,sk3)),complement(composition(sk2,sk3)))) ),
inference(paramod,[status(thm)],[c_6,c_12292]) ).
cnf(c_12293,plain,
join(join(A,B),C) = join(B,join(A,C)),
inference(paramod,[status(thm)],[c_1,c_3]) ).
cnf(c_33,plain,
join(A,join(B,C)) = join(B,join(A,C)),
inference(paramod,[status(thm)],[c_3,c_12293]) ).
cnf(c_34,plain,
join(complement(join(A,complement(B))),complement(join(complement(B),complement(A)))) = B,
inference(paramod,[status(thm)],[c_1,c_5]) ).
cnf(c_35,plain,
join(complement(join(complement(A),B)),complement(join(complement(B),complement(A)))) = A,
inference(paramod,[status(thm)],[c_1,c_5]) ).
cnf(c_12294,plain,
join(A,B) = join(complement(join(complement(A),C)),join(complement(join(complement(A),complement(C))),B)),
inference(paramod,[status(thm)],[c_5,c_3]) ).
cnf(c_36,plain,
join(complement(join(complement(A),B)),join(complement(join(complement(A),complement(B))),C)) = join(A,C),
inference(copy,[status(thm)],[c_12294]) ).
cnf(c_12295,plain,
join(complement(join(complement(join(complement(A),B)),join(complement(A),complement(B)))),complement(A)) = join(complement(A),B),
inference(paramod,[status(thm)],[c_5,c_5]) ).
cnf(c_12296,plain,
join(complement(join(join(complement(A),complement(B)),complement(join(complement(A),B)))),complement(A)) = join(complement(A),B),
inference(paramod,[status(thm)],[c_1,c_12295]) ).
cnf(c_12297,plain,
join(complement(join(complement(A),join(complement(B),complement(join(complement(A),B))))),complement(A)) = join(complement(A),B),
inference(paramod,[status(thm)],[c_3,c_12296]) ).
cnf(c_38,plain,
join(complement(A),complement(join(complement(A),join(complement(B),complement(join(complement(A),B)))))) = join(complement(A),B),
inference(paramod,[status(thm)],[c_1,c_12297]) ).
cnf(c_12298,plain,
composition(A,B) = join(composition(complement(join(complement(A),C)),B),composition(complement(join(complement(A),complement(C))),B)),
inference(paramod,[status(thm)],[c_5,c_10]) ).
cnf(c_40,plain,
join(composition(complement(join(complement(A),B)),C),composition(complement(join(complement(A),complement(B))),C)) = composition(A,C),
inference(copy,[status(thm)],[c_12298]) ).
cnf(c_12299,plain,
converse(A) = composition(converse(one),converse(A)),
inference(paramod,[status(thm)],[c_9,c_13]) ).
cnf(c_42,plain,
composition(converse(one),converse(A)) = converse(A),
inference(copy,[status(thm)],[c_12299]) ).
cnf(c_12300,plain,
join(complement(A),B) = join(complement(A),join(composition(converse(C),complement(composition(C,A))),B)),
inference(paramod,[status(thm)],[c_15,c_3]) ).
cnf(c_44,plain,
join(complement(A),join(composition(converse(B),complement(composition(B,A))),C)) = join(complement(A),C),
inference(copy,[status(thm)],[c_12300]) ).
cnf(c_12301,plain,
converse(complement(A)) = join(converse(complement(A)),converse(composition(converse(B),complement(composition(B,A))))),
inference(paramod,[status(thm)],[c_15,c_12]) ).
cnf(c_12302,plain,
converse(complement(A)) = join(converse(complement(A)),composition(converse(complement(composition(B,A))),converse(converse(B)))),
inference(paramod,[status(thm)],[c_13,c_12301]) ).
cnf(c_12303,plain,
converse(complement(A)) = join(converse(complement(A)),composition(converse(complement(composition(B,A))),B)),
inference(paramod,[status(thm)],[c_11,c_12302]) ).
cnf(c_51,plain,
join(converse(complement(A)),composition(converse(complement(composition(B,A))),B)) = converse(complement(A)),
inference(copy,[status(thm)],[c_12303]) ).
cnf(c_12304,plain,
join(top,A) = join(B,join(complement(B),A)),
inference(paramod,[status(thm)],[c_17,c_3]) ).
cnf(c_52,plain,
join(A,join(complement(A),B)) = join(top,B),
inference(copy,[status(thm)],[c_12304]) ).
cnf(c_12305,plain,
join(complement(top),complement(join(complement(A),complement(complement(complement(A)))))) = A,
inference(paramod,[status(thm)],[c_17,c_5]) ).
cnf(c_54,plain,
join(zero,complement(join(complement(A),complement(complement(complement(A)))))) = A,
inference(paramod,[status(thm)],[c_19,c_12305]) ).
cnf(c_12306,plain,
composition(top,A) = join(composition(B,A),composition(complement(B),A)),
inference(paramod,[status(thm)],[c_17,c_10]) ).
cnf(c_56,plain,
join(composition(A,B),composition(complement(A),B)) = composition(top,B),
inference(copy,[status(thm)],[c_12306]) ).
cnf(c_12307,plain,
converse(top) = join(converse(A),converse(complement(A))),
inference(paramod,[status(thm)],[c_17,c_12]) ).
cnf(c_57,plain,
join(converse(A),converse(complement(A))) = converse(top),
inference(copy,[status(thm)],[c_12307]) ).
cnf(c_62,plain,
join(complement(join(complement(A),complement(composition(B,C)))),composition(complement(join(complement(B),complement(composition(A,converse(C))))),complement(join(complement(C),complement(composition(converse(B),A)))))) = composition(complement(join(complement(B),complement(composition(A,converse(C))))),complement(join(complement(C),complement(composition(converse(B),A))))),
inference(paramod,[status(thm)],[c_1,c_21]) ).
cnf(c_65,plain,
join(complement(join(complement(A),complement(B))),composition(complement(join(complement(A),complement(composition(B,converse(one))))),complement(join(complement(one),complement(composition(converse(A),B)))))) = composition(complement(join(complement(A),complement(composition(B,converse(one))))),complement(join(complement(one),complement(composition(converse(A),B))))),
inference(paramod,[status(thm)],[c_9,c_21]) ).
cnf(c_12308,plain,
join(complement(join(complement(composition(converse(A),B)),complement(C))),composition(complement(join(complement(converse(A)),complement(composition(C,converse(B))))),complement(join(complement(B),complement(composition(A,C)))))) = composition(complement(join(complement(converse(A)),complement(composition(C,converse(B))))),complement(join(complement(B),complement(composition(converse(converse(A)),C))))),
inference(paramod,[status(thm)],[c_11,c_21]) ).
cnf(c_68,plain,
join(complement(join(complement(composition(converse(A),B)),complement(C))),composition(complement(join(complement(converse(A)),complement(composition(C,converse(B))))),complement(join(complement(B),complement(composition(A,C)))))) = composition(complement(join(complement(converse(A)),complement(composition(C,converse(B))))),complement(join(complement(B),complement(composition(A,C))))),
inference(paramod,[status(thm)],[c_11,c_12308]) ).
cnf(c_76,plain,
join(complement(join(complement(A),complement(B))),complement(join(complement(B),complement(composition(A,complement(join(complement(one),complement(composition(converse(A),B))))))))) = complement(join(complement(B),complement(composition(A,complement(join(complement(one),complement(composition(converse(A),B)))))))),
inference(paramod,[status(thm)],[c_9,c_23]) ).
cnf(c_12309,plain,
join(complement(join(complement(composition(A,B)),complement(one))),complement(join(complement(one),complement(composition(A,complement(join(complement(B),complement(converse(A))))))))) = complement(join(complement(one),complement(composition(A,complement(join(complement(B),complement(composition(converse(A),one)))))))),
inference(paramod,[status(thm)],[c_9,c_23]) ).
cnf(c_12310,plain,
join(complement(join(complement(one),complement(composition(A,B)))),complement(join(complement(one),complement(composition(A,complement(join(complement(B),complement(converse(A))))))))) = complement(join(complement(one),complement(composition(A,complement(join(complement(B),complement(composition(converse(A),one)))))))),
inference(paramod,[status(thm)],[c_1,c_12309]) ).
cnf(c_77,plain,
join(complement(join(complement(one),complement(composition(A,B)))),complement(join(complement(one),complement(composition(A,complement(join(complement(B),complement(converse(A))))))))) = complement(join(complement(one),complement(composition(A,complement(join(complement(B),complement(converse(A)))))))),
inference(paramod,[status(thm)],[c_9,c_12310]) ).
cnf(c_12311,plain,
join(complement(join(complement(composition(converse(A),B)),complement(C))),complement(join(complement(C),complement(composition(converse(A),complement(join(complement(B),complement(composition(A,C))))))))) = complement(join(complement(C),complement(composition(converse(A),complement(join(complement(B),complement(composition(converse(converse(A)),C)))))))),
inference(paramod,[status(thm)],[c_11,c_23]) ).
cnf(c_78,plain,
join(complement(join(complement(composition(converse(A),B)),complement(C))),complement(join(complement(C),complement(composition(converse(A),complement(join(complement(B),complement(composition(A,C))))))))) = complement(join(complement(C),complement(composition(converse(A),complement(join(complement(B),complement(composition(A,C)))))))),
inference(paramod,[status(thm)],[c_11,c_12311]) ).
cnf(c_12312,plain,
join(one,A) = join(one,join(sk1,A)),
inference(paramod,[status(thm)],[c_27,c_3]) ).
cnf(c_87,plain,
join(one,join(sk1,A)) = join(one,A),
inference(copy,[status(thm)],[c_12312]) ).
cnf(c_12313,plain,
composition(one,A) = join(composition(one,A),composition(sk1,A)),
inference(paramod,[status(thm)],[c_27,c_10]) ).
cnf(c_89,plain,
join(composition(one,A),composition(sk1,A)) = composition(one,A),
inference(copy,[status(thm)],[c_12313]) ).
cnf(c_12314,plain,
converse(one) = join(converse(one),converse(sk1)),
inference(paramod,[status(thm)],[c_27,c_12]) ).
cnf(c_90,plain,
join(converse(one),converse(sk1)) = converse(one),
inference(copy,[status(thm)],[c_12314]) ).
cnf(c_12315,plain,
join(one,A) = join(one,join(sk2,A)),
inference(paramod,[status(thm)],[c_29,c_3]) ).
cnf(c_91,plain,
join(one,join(sk2,A)) = join(one,A),
inference(copy,[status(thm)],[c_12315]) ).
cnf(c_12316,plain,
join(join(A,one),sk2) = join(A,one),
inference(paramod,[status(thm)],[c_29,c_3]) ).
cnf(c_92,plain,
join(sk2,join(A,one)) = join(A,one),
inference(paramod,[status(thm)],[c_1,c_12316]) ).
cnf(c_12317,plain,
composition(one,A) = join(composition(one,A),composition(sk2,A)),
inference(paramod,[status(thm)],[c_29,c_10]) ).
cnf(c_93,plain,
join(composition(one,A),composition(sk2,A)) = composition(one,A),
inference(copy,[status(thm)],[c_12317]) ).
cnf(c_12318,plain,
converse(one) = join(converse(one),converse(sk2)),
inference(paramod,[status(thm)],[c_29,c_12]) ).
cnf(c_94,plain,
join(converse(one),converse(sk2)) = converse(one),
inference(copy,[status(thm)],[c_12318]) ).
cnf(c_12319,plain,
join(A,B) = join(complement(join(complement(B),C)),join(A,complement(join(complement(B),complement(C))))),
inference(paramod,[status(thm)],[c_5,c_33]) ).
cnf(c_96,plain,
join(complement(join(complement(A),B)),join(C,complement(join(complement(A),complement(B))))) = join(C,A),
inference(copy,[status(thm)],[c_12319]) ).
cnf(c_12320,plain,
A = join(complement(join(complement(A),complement(B))),complement(join(B,complement(A)))),
inference(paramod,[status(thm)],[c_34,c_1]) ).
cnf(c_101,plain,
join(complement(join(complement(A),complement(B))),complement(join(B,complement(A)))) = A,
inference(copy,[status(thm)],[c_12320]) ).
cnf(c_102,plain,
join(complement(join(A,complement(B))),complement(join(complement(A),complement(B)))) = B,
inference(paramod,[status(thm)],[c_1,c_34]) ).
cnf(c_12321,plain,
join(A,B) = join(complement(join(C,complement(A))),join(complement(join(complement(A),complement(C))),B)),
inference(paramod,[status(thm)],[c_34,c_3]) ).
cnf(c_103,plain,
join(complement(join(A,complement(B))),join(complement(join(complement(B),complement(A))),C)) = join(B,C),
inference(copy,[status(thm)],[c_12321]) ).
cnf(c_104,plain,
join(complement(join(A,join(B,complement(C)))),complement(join(complement(C),complement(join(A,B))))) = C,
inference(paramod,[status(thm)],[c_3,c_34]) ).
cnf(c_12322,plain,
composition(A,B) = join(composition(complement(join(C,complement(A))),B),composition(complement(join(complement(A),complement(C))),B)),
inference(paramod,[status(thm)],[c_34,c_10]) ).
cnf(c_108,plain,
join(composition(complement(join(A,complement(B))),C),composition(complement(join(complement(B),complement(A))),C)) = composition(B,C),
inference(copy,[status(thm)],[c_12322]) ).
cnf(c_12323,plain,
converse(A) = join(converse(complement(join(B,complement(A)))),converse(complement(join(complement(A),complement(B))))),
inference(paramod,[status(thm)],[c_34,c_12]) ).
cnf(c_109,plain,
join(converse(complement(join(A,complement(B)))),converse(complement(join(complement(B),complement(A))))) = converse(B),
inference(copy,[status(thm)],[c_12323]) ).
cnf(c_12324,plain,
join(complement(join(complement(complement(A)),A)),complement(top)) = complement(A),
inference(paramod,[status(thm)],[c_17,c_35]) ).
cnf(c_12325,plain,
join(complement(join(A,complement(complement(A)))),complement(top)) = complement(A),
inference(paramod,[status(thm)],[c_1,c_12324]) ).
cnf(c_12326,plain,
join(complement(join(A,complement(complement(A)))),zero) = complement(A),
inference(paramod,[status(thm)],[c_19,c_12325]) ).
cnf(c_120,plain,
join(zero,complement(join(A,complement(complement(A))))) = complement(A),
inference(paramod,[status(thm)],[c_1,c_12326]) ).
cnf(c_12327,plain,
join(complement(join(complement(join(complement(A),complement(B))),join(complement(B),A))),complement(B)) = join(complement(A),complement(B)),
inference(paramod,[status(thm)],[c_35,c_35]) ).
cnf(c_12328,plain,
join(complement(join(join(complement(B),A),complement(join(complement(A),complement(B))))),complement(B)) = join(complement(A),complement(B)),
inference(paramod,[status(thm)],[c_1,c_12327]) ).
cnf(c_12329,plain,
join(complement(join(complement(B),join(A,complement(join(complement(A),complement(B)))))),complement(B)) = join(complement(A),complement(B)),
inference(paramod,[status(thm)],[c_3,c_12328]) ).
cnf(c_125,plain,
join(complement(A),complement(join(complement(A),join(B,complement(join(complement(B),complement(A))))))) = join(complement(B),complement(A)),
inference(paramod,[status(thm)],[c_1,c_12329]) ).
cnf(c_126,plain,
complement(complement(A)) = A,
inference(paramod,[status(thm)],[c_120,c_54]) ).
cnf(c_127,plain,
join(zero,complement(join(A,A))) = complement(A),
inference(paramod,[status(thm)],[c_126,c_120]) ).
cnf(c_12330,plain,
composition(converse(one),A) = converse(converse(A)),
inference(paramod,[status(thm)],[c_11,c_42]) ).
cnf(c_136,plain,
composition(converse(one),A) = A,
inference(paramod,[status(thm)],[c_11,c_12330]) ).
cnf(c_12331,plain,
one = converse(one),
inference(paramod,[status(thm)],[c_136,c_9]) ).
cnf(c_145,plain,
converse(one) = one,
inference(copy,[status(thm)],[c_12331]) ).
cnf(c_149,plain,
join(complement(A),complement(composition(one,A))) = complement(A),
inference(paramod,[status(thm)],[c_136,c_15]) ).
cnf(c_12332,plain,
join(complement(join(complement(A),complement(B))),composition(complement(join(complement(converse(one)),complement(composition(B,converse(A))))),complement(join(complement(A),complement(composition(converse(converse(one)),B)))))) = composition(complement(join(complement(converse(one)),complement(composition(B,converse(A))))),complement(join(complement(A),complement(composition(converse(converse(one)),B))))),
inference(paramod,[status(thm)],[c_136,c_21]) ).
cnf(c_12333,plain,
join(complement(join(complement(A),complement(B))),composition(complement(join(complement(one),complement(composition(B,converse(A))))),complement(join(complement(A),complement(composition(converse(converse(one)),B)))))) = composition(complement(join(complement(converse(one)),complement(composition(B,converse(A))))),complement(join(complement(A),complement(composition(converse(converse(one)),B))))),
inference(paramod,[status(thm)],[c_145,c_12332]) ).
cnf(c_12334,plain,
join(complement(join(complement(A),complement(B))),composition(complement(join(complement(one),complement(composition(B,converse(A))))),complement(join(complement(A),complement(composition(converse(one),B)))))) = composition(complement(join(complement(converse(one)),complement(composition(B,converse(A))))),complement(join(complement(A),complement(composition(converse(converse(one)),B))))),
inference(paramod,[status(thm)],[c_145,c_12333]) ).
cnf(c_12335,plain,
join(complement(join(complement(A),complement(B))),composition(complement(join(complement(one),complement(composition(B,converse(A))))),complement(join(complement(A),complement(composition(one,B)))))) = composition(complement(join(complement(converse(one)),complement(composition(B,converse(A))))),complement(join(complement(A),complement(composition(converse(converse(one)),B))))),
inference(paramod,[status(thm)],[c_145,c_12334]) ).
cnf(c_12336,plain,
join(complement(join(complement(A),complement(B))),composition(complement(join(complement(one),complement(composition(B,converse(A))))),complement(join(complement(A),complement(composition(one,B)))))) = composition(complement(join(complement(one),complement(composition(B,converse(A))))),complement(join(complement(A),complement(composition(converse(converse(one)),B))))),
inference(paramod,[status(thm)],[c_145,c_12335]) ).
cnf(c_12337,plain,
join(complement(join(complement(A),complement(B))),composition(complement(join(complement(one),complement(composition(B,converse(A))))),complement(join(complement(A),complement(composition(one,B)))))) = composition(complement(join(complement(one),complement(composition(B,converse(A))))),complement(join(complement(A),complement(composition(converse(one),B))))),
inference(paramod,[status(thm)],[c_145,c_12336]) ).
cnf(c_150,plain,
join(complement(join(complement(A),complement(B))),composition(complement(join(complement(one),complement(composition(B,converse(A))))),complement(join(complement(A),complement(composition(one,B)))))) = composition(complement(join(complement(one),complement(composition(B,converse(A))))),complement(join(complement(A),complement(composition(one,B))))),
inference(paramod,[status(thm)],[c_145,c_12337]) ).
cnf(c_164,plain,
composition(one,A) = A,
inference(paramod,[status(thm)],[c_145,c_136]) ).
cnf(c_12338,plain,
join(one,converse(sk2)) = converse(one),
inference(paramod,[status(thm)],[c_145,c_94]) ).
cnf(c_166,plain,
join(one,converse(sk2)) = one,
inference(paramod,[status(thm)],[c_145,c_12338]) ).
cnf(c_12339,plain,
join(one,converse(sk1)) = converse(one),
inference(paramod,[status(thm)],[c_145,c_90]) ).
cnf(c_167,plain,
join(one,converse(sk1)) = one,
inference(paramod,[status(thm)],[c_145,c_12339]) ).
cnf(c_12340,plain,
join(complement(join(complement(A),complement(B))),composition(complement(join(complement(A),complement(composition(B,one)))),complement(join(complement(one),complement(composition(converse(A),B)))))) = composition(complement(join(complement(A),complement(composition(B,converse(one))))),complement(join(complement(one),complement(composition(converse(A),B))))),
inference(paramod,[status(thm)],[c_145,c_65]) ).
cnf(c_12341,plain,
join(complement(join(complement(A),complement(B))),composition(complement(join(complement(A),complement(B))),complement(join(complement(one),complement(composition(converse(A),B)))))) = composition(complement(join(complement(A),complement(composition(B,converse(one))))),complement(join(complement(one),complement(composition(converse(A),B))))),
inference(paramod,[status(thm)],[c_9,c_12340]) ).
cnf(c_12342,plain,
join(complement(join(complement(A),complement(B))),composition(complement(join(complement(A),complement(B))),complement(join(complement(one),complement(composition(converse(A),B)))))) = composition(complement(join(complement(A),complement(composition(B,one)))),complement(join(complement(one),complement(composition(converse(A),B))))),
inference(paramod,[status(thm)],[c_145,c_12341]) ).
cnf(c_168,plain,
join(complement(join(complement(A),complement(B))),composition(complement(join(complement(A),complement(B))),complement(join(complement(one),complement(composition(converse(A),B)))))) = composition(complement(join(complement(A),complement(B))),complement(join(complement(one),complement(composition(converse(A),B))))),
inference(paramod,[status(thm)],[c_9,c_12342]) ).
cnf(c_12343,plain,
join(A,composition(sk2,A)) = composition(one,A),
inference(paramod,[status(thm)],[c_164,c_93]) ).
cnf(c_169,plain,
join(A,composition(sk2,A)) = A,
inference(paramod,[status(thm)],[c_164,c_12343]) ).
cnf(c_12344,plain,
join(A,composition(sk1,A)) = composition(one,A),
inference(paramod,[status(thm)],[c_164,c_89]) ).
cnf(c_170,plain,
join(A,composition(sk1,A)) = A,
inference(paramod,[status(thm)],[c_164,c_12344]) ).
cnf(c_12345,plain,
join(complement(join(complement(A),complement(B))),composition(complement(join(complement(one),complement(composition(B,converse(A))))),complement(join(complement(A),complement(B))))) = composition(complement(join(complement(one),complement(composition(B,converse(A))))),complement(join(complement(A),complement(composition(one,B))))),
inference(paramod,[status(thm)],[c_164,c_150]) ).
cnf(c_171,plain,
join(complement(join(complement(A),complement(B))),composition(complement(join(complement(one),complement(composition(B,converse(A))))),complement(join(complement(A),complement(B))))) = composition(complement(join(complement(one),complement(composition(B,converse(A))))),complement(join(complement(A),complement(B)))),
inference(paramod,[status(thm)],[c_164,c_12345]) ).
cnf(c_173,plain,
join(complement(A),complement(A)) = complement(A),
inference(paramod,[status(thm)],[c_164,c_149]) ).
cnf(c_12346,plain,
composition(one,A) = join(composition(one,A),composition(converse(sk2),A)),
inference(paramod,[status(thm)],[c_166,c_10]) ).
cnf(c_12347,plain,
A = join(composition(one,A),composition(converse(sk2),A)),
inference(paramod,[status(thm)],[c_164,c_12346]) ).
cnf(c_12348,plain,
A = join(A,composition(converse(sk2),A)),
inference(paramod,[status(thm)],[c_164,c_12347]) ).
cnf(c_175,plain,
join(A,composition(converse(sk2),A)) = A,
inference(copy,[status(thm)],[c_12348]) ).
cnf(c_12349,plain,
join(complement(join(complement(A),B)),B) = join(A,complement(join(complement(B),complement(complement(A))))),
inference(paramod,[status(thm)],[c_34,c_36]) ).
cnf(c_12350,plain,
join(B,complement(join(complement(A),B))) = join(A,complement(join(complement(B),complement(complement(A))))),
inference(paramod,[status(thm)],[c_1,c_12349]) ).
cnf(c_196,plain,
join(A,complement(join(complement(B),A))) = join(B,complement(join(complement(A),B))),
inference(paramod,[status(thm)],[c_126,c_12350]) ).
cnf(c_12351,plain,
join(A,join(complement(B),C)) = join(complement(B),join(A,complement(join(complement(B),join(complement(C),complement(join(complement(B),C))))))),
inference(paramod,[status(thm)],[c_38,c_33]) ).
cnf(c_209,plain,
join(complement(A),join(B,complement(join(complement(A),join(complement(C),complement(join(complement(A),C))))))) = join(B,join(complement(A),C)),
inference(copy,[status(thm)],[c_12351]) ).
cnf(c_12352,plain,
join(complement(join(complement(A),B)),complement(join(complement(join(complement(A),join(complement(B),complement(join(complement(A),B))))),complement(complement(A))))) = join(complement(A),join(complement(B),complement(join(complement(A),B)))),
inference(paramod,[status(thm)],[c_38,c_34]) ).
cnf(c_12353,plain,
join(complement(join(complement(A),B)),complement(join(complement(join(complement(A),join(complement(B),complement(join(complement(A),B))))),A))) = join(complement(A),join(complement(B),complement(join(complement(A),B)))),
inference(paramod,[status(thm)],[c_126,c_12352]) ).
cnf(c_211,plain,
join(complement(join(complement(A),B)),complement(join(A,complement(join(complement(A),join(complement(B),complement(join(complement(A),B)))))))) = join(complement(A),join(complement(B),complement(join(complement(A),B)))),
inference(paramod,[status(thm)],[c_1,c_12353]) ).
cnf(c_227,plain,
join(composition(complement(join(A,join(complement(B),C))),D),composition(complement(join(complement(B),complement(join(A,C)))),D)) = composition(B,D),
inference(paramod,[status(thm)],[c_33,c_40]) ).
cnf(c_12354,plain,
composition(one,A) = join(composition(one,A),composition(converse(sk1),A)),
inference(paramod,[status(thm)],[c_167,c_10]) ).
cnf(c_12355,plain,
A = join(composition(one,A),composition(converse(sk1),A)),
inference(paramod,[status(thm)],[c_164,c_12354]) ).
cnf(c_12356,plain,
A = join(A,composition(converse(sk1),A)),
inference(paramod,[status(thm)],[c_164,c_12355]) ).
cnf(c_233,plain,
join(A,composition(converse(sk1),A)) = A,
inference(copy,[status(thm)],[c_12356]) ).
cnf(c_12357,plain,
join(A,B) = join(B,join(A,composition(sk2,B))),
inference(paramod,[status(thm)],[c_169,c_33]) ).
cnf(c_239,plain,
join(A,join(B,composition(sk2,A))) = join(B,A),
inference(copy,[status(thm)],[c_12357]) ).
cnf(c_12358,plain,
join(complement(complement(A)),complement(join(complement(A),complement(complement(A))))) = A,
inference(paramod,[status(thm)],[c_173,c_5]) ).
cnf(c_12359,plain,
join(A,complement(join(complement(A),complement(complement(A))))) = A,
inference(paramod,[status(thm)],[c_126,c_12358]) ).
cnf(c_12360,plain,
join(A,complement(join(complement(A),A))) = A,
inference(paramod,[status(thm)],[c_126,c_12359]) ).
cnf(c_12361,plain,
join(A,complement(join(A,complement(A)))) = A,
inference(paramod,[status(thm)],[c_1,c_12360]) ).
cnf(c_12362,plain,
join(A,complement(top)) = A,
inference(paramod,[status(thm)],[c_17,c_12361]) ).
cnf(c_258,plain,
join(A,zero) = A,
inference(paramod,[status(thm)],[c_19,c_12362]) ).
cnf(c_12363,plain,
join(complement(join(complement(A),A)),complement(complement(A))) = A,
inference(paramod,[status(thm)],[c_173,c_5]) ).
cnf(c_12364,plain,
join(complement(join(A,complement(A))),complement(complement(A))) = A,
inference(paramod,[status(thm)],[c_1,c_12363]) ).
cnf(c_12365,plain,
join(complement(top),complement(complement(A))) = A,
inference(paramod,[status(thm)],[c_17,c_12364]) ).
cnf(c_12366,plain,
join(zero,complement(complement(A))) = A,
inference(paramod,[status(thm)],[c_19,c_12365]) ).
cnf(c_259,plain,
join(zero,A) = A,
inference(paramod,[status(thm)],[c_126,c_12366]) ).
cnf(c_12367,plain,
join(complement(join(complement(A),B)),complement(join(complement(A),complement(B)))) = join(A,complement(join(complement(A),complement(B)))),
inference(paramod,[status(thm)],[c_173,c_36]) ).
cnf(c_12368,plain,
A = join(A,complement(join(complement(A),complement(B)))),
inference(paramod,[status(thm)],[c_5,c_12367]) ).
cnf(c_262,plain,
join(A,complement(join(complement(A),complement(B)))) = A,
inference(copy,[status(thm)],[c_12368]) ).
cnf(c_271,plain,
complement(join(A,A)) = complement(A),
inference(paramod,[status(thm)],[c_259,c_127]) ).
cnf(c_281,plain,
join(complement(A),complement(join(complement(A),B))) = join(complement(B),complement(A)),
inference(paramod,[status(thm)],[c_262,c_125]) ).
cnf(c_12369,plain,
converse(A) = join(converse(A),converse(zero)),
inference(paramod,[status(thm)],[c_258,c_12]) ).
cnf(c_291,plain,
join(converse(A),converse(zero)) = converse(A),
inference(copy,[status(thm)],[c_12369]) ).
cnf(c_329,plain,
complement(zero) = top,
inference(paramod,[status(thm)],[c_259,c_17]) ).
cnf(c_12370,plain,
join(complement(join(complement(A),B)),complement(join(complement(join(A,A)),complement(B)))) = join(A,A),
inference(paramod,[status(thm)],[c_271,c_5]) ).
cnf(c_12371,plain,
join(complement(join(complement(A),B)),complement(join(complement(A),complement(B)))) = join(A,A),
inference(paramod,[status(thm)],[c_271,c_12370]) ).
cnf(c_12372,plain,
A = join(A,A),
inference(paramod,[status(thm)],[c_5,c_12371]) ).
cnf(c_364,plain,
join(A,A) = A,
inference(copy,[status(thm)],[c_12372]) ).
cnf(c_12373,plain,
join(complement(join(complement(A),B)),join(complement(join(complement(A),complement(B))),A)) = A,
inference(paramod,[status(thm)],[c_364,c_36]) ).
cnf(c_12374,plain,
join(complement(join(complement(A),B)),join(A,complement(join(complement(A),complement(B))))) = A,
inference(paramod,[status(thm)],[c_1,c_12373]) ).
cnf(c_12375,plain,
join(complement(join(complement(A),B)),A) = A,
inference(paramod,[status(thm)],[c_262,c_12374]) ).
cnf(c_405,plain,
join(A,complement(join(complement(A),B))) = A,
inference(paramod,[status(thm)],[c_1,c_12375]) ).
cnf(c_12376,plain,
join(complement(join(complement(A),B)),complement(A)) = join(complement(A),join(complement(B),complement(join(complement(A),B)))),
inference(paramod,[status(thm)],[c_405,c_211]) ).
cnf(c_12377,plain,
join(complement(A),complement(join(complement(A),B))) = join(complement(A),join(complement(B),complement(join(complement(A),B)))),
inference(paramod,[status(thm)],[c_1,c_12376]) ).
cnf(c_12378,plain,
join(complement(B),complement(A)) = join(complement(A),join(complement(B),complement(join(complement(A),B)))),
inference(paramod,[status(thm)],[c_281,c_12377]) ).
cnf(c_407,plain,
join(complement(A),join(complement(B),complement(join(complement(A),B)))) = join(complement(B),complement(A)),
inference(copy,[status(thm)],[c_12378]) ).
cnf(c_410,plain,
join(complement(A),join(B,complement(join(complement(C),complement(A))))) = join(B,join(complement(A),C)),
inference(paramod,[status(thm)],[c_407,c_209]) ).
cnf(c_12379,plain,
join(A,converse(zero)) = converse(converse(A)),
inference(paramod,[status(thm)],[c_11,c_291]) ).
cnf(c_413,plain,
join(A,converse(zero)) = A,
inference(paramod,[status(thm)],[c_11,c_12379]) ).
cnf(c_12380,plain,
zero = converse(zero),
inference(paramod,[status(thm)],[c_413,c_259]) ).
cnf(c_420,plain,
converse(zero) = zero,
inference(copy,[status(thm)],[c_12380]) ).
cnf(c_12381,plain,
join(A,complement(A)) = join(top,complement(A)),
inference(paramod,[status(thm)],[c_364,c_52]) ).
cnf(c_12382,plain,
top = join(top,complement(A)),
inference(paramod,[status(thm)],[c_17,c_12381]) ).
cnf(c_561,plain,
join(top,complement(A)) = top,
inference(copy,[status(thm)],[c_12382]) ).
cnf(c_12383,plain,
join(A,join(complement(A),top)) = top,
inference(paramod,[status(thm)],[c_364,c_52]) ).
cnf(c_12384,plain,
join(A,join(top,complement(A))) = top,
inference(paramod,[status(thm)],[c_1,c_12383]) ).
cnf(c_562,plain,
join(A,top) = top,
inference(paramod,[status(thm)],[c_561,c_12384]) ).
cnf(c_12385,plain,
join(A,composition(top,B)) = join(composition(C,B),join(A,composition(complement(C),B))),
inference(paramod,[status(thm)],[c_56,c_33]) ).
cnf(c_588,plain,
join(composition(A,B),join(C,composition(complement(A),B))) = join(C,composition(top,B)),
inference(copy,[status(thm)],[c_12385]) ).
cnf(c_12386,plain,
top = join(top,A),
inference(paramod,[status(thm)],[c_562,c_1]) ).
cnf(c_594,plain,
join(top,A) = top,
inference(copy,[status(thm)],[c_12386]) ).
cnf(c_12387,plain,
composition(top,A) = join(composition(B,A),composition(top,A)),
inference(paramod,[status(thm)],[c_562,c_10]) ).
cnf(c_595,plain,
join(composition(A,B),composition(top,B)) = composition(top,B),
inference(copy,[status(thm)],[c_12387]) ).
cnf(c_12388,plain,
converse(top) = join(converse(A),converse(top)),
inference(paramod,[status(thm)],[c_562,c_12]) ).
cnf(c_596,plain,
join(converse(A),converse(top)) = converse(top),
inference(copy,[status(thm)],[c_12388]) ).
cnf(c_623,plain,
join(A,converse(top)) = converse(top),
inference(paramod,[status(thm)],[c_11,c_596]) ).
cnf(c_626,plain,
converse(top) = top,
inference(paramod,[status(thm)],[c_623,c_594]) ).
cnf(c_638,plain,
join(converse(A),converse(complement(A))) = top,
inference(paramod,[status(thm)],[c_626,c_57]) ).
cnf(c_699,plain,
join(A,composition(top,A)) = composition(top,A),
inference(paramod,[status(thm)],[c_164,c_595]) ).
cnf(c_705,plain,
composition(top,top) = top,
inference(paramod,[status(thm)],[c_699,c_594]) ).
cnf(c_12389,plain,
join(complement(top),composition(converse(top),complement(top))) = complement(top),
inference(paramod,[status(thm)],[c_705,c_15]) ).
cnf(c_12390,plain,
join(zero,composition(converse(top),complement(top))) = complement(top),
inference(paramod,[status(thm)],[c_19,c_12389]) ).
cnf(c_12391,plain,
join(zero,composition(top,complement(top))) = complement(top),
inference(paramod,[status(thm)],[c_626,c_12390]) ).
cnf(c_12392,plain,
join(zero,composition(top,zero)) = complement(top),
inference(paramod,[status(thm)],[c_19,c_12391]) ).
cnf(c_12393,plain,
composition(top,zero) = complement(top),
inference(paramod,[status(thm)],[c_699,c_12392]) ).
cnf(c_707,plain,
composition(top,zero) = zero,
inference(paramod,[status(thm)],[c_19,c_12393]) ).
cnf(c_12394,plain,
join(converse(complement(top)),composition(converse(complement(top)),top)) = converse(complement(top)),
inference(paramod,[status(thm)],[c_705,c_51]) ).
cnf(c_12395,plain,
join(converse(zero),composition(converse(complement(top)),top)) = converse(complement(top)),
inference(paramod,[status(thm)],[c_19,c_12394]) ).
cnf(c_12396,plain,
join(zero,composition(converse(complement(top)),top)) = converse(complement(top)),
inference(paramod,[status(thm)],[c_420,c_12395]) ).
cnf(c_12397,plain,
join(zero,composition(converse(zero),top)) = converse(complement(top)),
inference(paramod,[status(thm)],[c_19,c_12396]) ).
cnf(c_12398,plain,
join(zero,composition(zero,top)) = converse(complement(top)),
inference(paramod,[status(thm)],[c_420,c_12397]) ).
cnf(c_12399,plain,
composition(zero,top) = converse(complement(top)),
inference(paramod,[status(thm)],[c_259,c_12398]) ).
cnf(c_12400,plain,
composition(zero,top) = converse(zero),
inference(paramod,[status(thm)],[c_19,c_12399]) ).
cnf(c_713,plain,
composition(zero,top) = zero,
inference(paramod,[status(thm)],[c_420,c_12400]) ).
cnf(c_12401,plain,
composition(join(top,A),zero) = join(zero,composition(A,zero)),
inference(paramod,[status(thm)],[c_707,c_10]) ).
cnf(c_12402,plain,
composition(top,zero) = join(zero,composition(A,zero)),
inference(paramod,[status(thm)],[c_594,c_12401]) ).
cnf(c_12403,plain,
zero = join(zero,composition(A,zero)),
inference(paramod,[status(thm)],[c_707,c_12402]) ).
cnf(c_12404,plain,
zero = composition(A,zero),
inference(paramod,[status(thm)],[c_259,c_12403]) ).
cnf(c_724,plain,
composition(A,zero) = zero,
inference(copy,[status(thm)],[c_12404]) ).
cnf(c_12405,plain,
join(complement(join(complement(composition(converse(zero),A)),complement(top))),composition(complement(join(complement(converse(zero)),complement(composition(top,converse(A))))),complement(join(complement(A),complement(zero))))) = composition(complement(join(complement(converse(zero)),complement(composition(top,converse(A))))),complement(join(complement(A),complement(composition(zero,top))))),
inference(paramod,[status(thm)],[c_713,c_68]) ).
cnf(c_12406,plain,
join(complement(join(complement(composition(zero,A)),complement(top))),composition(complement(join(complement(converse(zero)),complement(composition(top,converse(A))))),complement(join(complement(A),complement(zero))))) = composition(complement(join(complement(converse(zero)),complement(composition(top,converse(A))))),complement(join(complement(A),complement(composition(zero,top))))),
inference(paramod,[status(thm)],[c_420,c_12405]) ).
cnf(c_12407,plain,
join(complement(join(complement(composition(zero,A)),zero)),composition(complement(join(complement(converse(zero)),complement(composition(top,converse(A))))),complement(join(complement(A),complement(zero))))) = composition(complement(join(complement(converse(zero)),complement(composition(top,converse(A))))),complement(join(complement(A),complement(composition(zero,top))))),
inference(paramod,[status(thm)],[c_19,c_12406]) ).
cnf(c_12408,plain,
join(complement(join(zero,complement(composition(zero,A)))),composition(complement(join(complement(converse(zero)),complement(composition(top,converse(A))))),complement(join(complement(A),complement(zero))))) = composition(complement(join(complement(converse(zero)),complement(composition(top,converse(A))))),complement(join(complement(A),complement(composition(zero,top))))),
inference(paramod,[status(thm)],[c_1,c_12407]) ).
cnf(c_12409,plain,
join(complement(complement(composition(zero,A))),composition(complement(join(complement(converse(zero)),complement(composition(top,converse(A))))),complement(join(complement(A),complement(zero))))) = composition(complement(join(complement(converse(zero)),complement(composition(top,converse(A))))),complement(join(complement(A),complement(composition(zero,top))))),
inference(paramod,[status(thm)],[c_259,c_12408]) ).
cnf(c_12410,plain,
join(composition(zero,A),composition(complement(join(complement(converse(zero)),complement(composition(top,converse(A))))),complement(join(complement(A),complement(zero))))) = composition(complement(join(complement(converse(zero)),complement(composition(top,converse(A))))),complement(join(complement(A),complement(composition(zero,top))))),
inference(paramod,[status(thm)],[c_126,c_12409]) ).
cnf(c_12411,plain,
join(composition(zero,A),composition(complement(join(complement(zero),complement(composition(top,converse(A))))),complement(join(complement(A),complement(zero))))) = composition(complement(join(complement(converse(zero)),complement(composition(top,converse(A))))),complement(join(complement(A),complement(composition(zero,top))))),
inference(paramod,[status(thm)],[c_420,c_12410]) ).
cnf(c_12412,plain,
join(composition(zero,A),composition(complement(join(top,complement(composition(top,converse(A))))),complement(join(complement(A),complement(zero))))) = composition(complement(join(complement(converse(zero)),complement(composition(top,converse(A))))),complement(join(complement(A),complement(composition(zero,top))))),
inference(paramod,[status(thm)],[c_329,c_12411]) ).
cnf(c_12413,plain,
join(composition(zero,A),composition(complement(top),complement(join(complement(A),complement(zero))))) = composition(complement(join(complement(converse(zero)),complement(composition(top,converse(A))))),complement(join(complement(A),complement(composition(zero,top))))),
inference(paramod,[status(thm)],[c_594,c_12412]) ).
cnf(c_12414,plain,
join(composition(zero,A),composition(zero,complement(join(complement(A),complement(zero))))) = composition(complement(join(complement(converse(zero)),complement(composition(top,converse(A))))),complement(join(complement(A),complement(composition(zero,top))))),
inference(paramod,[status(thm)],[c_19,c_12413]) ).
cnf(c_12415,plain,
join(composition(zero,A),composition(zero,complement(join(complement(A),top)))) = composition(complement(join(complement(converse(zero)),complement(composition(top,converse(A))))),complement(join(complement(A),complement(composition(zero,top))))),
inference(paramod,[status(thm)],[c_329,c_12414]) ).
cnf(c_12416,plain,
join(composition(zero,A),composition(zero,complement(join(top,complement(A))))) = composition(complement(join(complement(converse(zero)),complement(composition(top,converse(A))))),complement(join(complement(A),complement(composition(zero,top))))),
inference(paramod,[status(thm)],[c_1,c_12415]) ).
cnf(c_12417,plain,
join(composition(zero,A),composition(zero,complement(top))) = composition(complement(join(complement(converse(zero)),complement(composition(top,converse(A))))),complement(join(complement(A),complement(composition(zero,top))))),
inference(paramod,[status(thm)],[c_594,c_12416]) ).
cnf(c_12418,plain,
join(composition(zero,A),composition(zero,zero)) = composition(complement(join(complement(converse(zero)),complement(composition(top,converse(A))))),complement(join(complement(A),complement(composition(zero,top))))),
inference(paramod,[status(thm)],[c_19,c_12417]) ).
cnf(c_12419,plain,
join(composition(zero,A),zero) = composition(complement(join(complement(converse(zero)),complement(composition(top,converse(A))))),complement(join(complement(A),complement(composition(zero,top))))),
inference(paramod,[status(thm)],[c_724,c_12418]) ).
cnf(c_12420,plain,
join(zero,composition(zero,A)) = composition(complement(join(complement(converse(zero)),complement(composition(top,converse(A))))),complement(join(complement(A),complement(composition(zero,top))))),
inference(paramod,[status(thm)],[c_1,c_12419]) ).
cnf(c_12421,plain,
composition(zero,A) = composition(complement(join(complement(converse(zero)),complement(composition(top,converse(A))))),complement(join(complement(A),complement(composition(zero,top))))),
inference(paramod,[status(thm)],[c_259,c_12420]) ).
cnf(c_12422,plain,
composition(zero,A) = composition(complement(join(complement(zero),complement(composition(top,converse(A))))),complement(join(complement(A),complement(composition(zero,top))))),
inference(paramod,[status(thm)],[c_420,c_12421]) ).
cnf(c_12423,plain,
composition(zero,A) = composition(complement(join(top,complement(composition(top,converse(A))))),complement(join(complement(A),complement(composition(zero,top))))),
inference(paramod,[status(thm)],[c_329,c_12422]) ).
cnf(c_12424,plain,
composition(zero,A) = composition(complement(top),complement(join(complement(A),complement(composition(zero,top))))),
inference(paramod,[status(thm)],[c_594,c_12423]) ).
cnf(c_12425,plain,
composition(zero,A) = composition(zero,complement(join(complement(A),complement(composition(zero,top))))),
inference(paramod,[status(thm)],[c_19,c_12424]) ).
cnf(c_12426,plain,
composition(zero,A) = composition(zero,complement(join(complement(A),complement(zero)))),
inference(paramod,[status(thm)],[c_713,c_12425]) ).
cnf(c_12427,plain,
composition(zero,A) = composition(zero,complement(join(complement(A),top))),
inference(paramod,[status(thm)],[c_329,c_12426]) ).
cnf(c_12428,plain,
composition(zero,A) = composition(zero,complement(join(top,complement(A)))),
inference(paramod,[status(thm)],[c_1,c_12427]) ).
cnf(c_12429,plain,
composition(zero,A) = composition(zero,complement(top)),
inference(paramod,[status(thm)],[c_594,c_12428]) ).
cnf(c_12430,plain,
composition(zero,A) = composition(zero,zero),
inference(paramod,[status(thm)],[c_19,c_12429]) ).
cnf(c_758,plain,
composition(zero,A) = zero,
inference(paramod,[status(thm)],[c_724,c_12430]) ).
cnf(c_12431,plain,
converse(A) = join(converse(A),converse(composition(converse(sk2),A))),
inference(paramod,[status(thm)],[c_175,c_12]) ).
cnf(c_12432,plain,
converse(A) = join(converse(A),composition(converse(A),converse(converse(sk2)))),
inference(paramod,[status(thm)],[c_13,c_12431]) ).
cnf(c_12433,plain,
converse(A) = join(converse(A),composition(converse(A),sk2)),
inference(paramod,[status(thm)],[c_11,c_12432]) ).
cnf(c_767,plain,
join(converse(A),composition(converse(A),sk2)) = converse(A),
inference(copy,[status(thm)],[c_12433]) ).
cnf(c_12434,plain,
converse(A) = join(converse(A),converse(composition(converse(sk1),A))),
inference(paramod,[status(thm)],[c_233,c_12]) ).
cnf(c_12435,plain,
converse(A) = join(converse(A),composition(converse(A),converse(converse(sk1)))),
inference(paramod,[status(thm)],[c_13,c_12434]) ).
cnf(c_12436,plain,
converse(A) = join(converse(A),composition(converse(A),sk1)),
inference(paramod,[status(thm)],[c_11,c_12435]) ).
cnf(c_772,plain,
join(converse(A),composition(converse(A),sk1)) = converse(A),
inference(copy,[status(thm)],[c_12436]) ).
cnf(c_12437,plain,
join(one,top) = join(one,complement(sk1)),
inference(paramod,[status(thm)],[c_17,c_87]) ).
cnf(c_12438,plain,
top = join(one,complement(sk1)),
inference(paramod,[status(thm)],[c_562,c_12437]) ).
cnf(c_807,plain,
join(one,complement(sk1)) = top,
inference(copy,[status(thm)],[c_12438]) ).
cnf(c_12439,plain,
join(one,sk1) = join(one,composition(sk2,sk1)),
inference(paramod,[status(thm)],[c_169,c_87]) ).
cnf(c_12440,plain,
one = join(one,composition(sk2,sk1)),
inference(paramod,[status(thm)],[c_27,c_12439]) ).
cnf(c_809,plain,
join(one,composition(sk2,sk1)) = one,
inference(copy,[status(thm)],[c_12440]) ).
cnf(c_12441,plain,
join(one,sk1) = join(one,composition(sk1,sk1)),
inference(paramod,[status(thm)],[c_170,c_87]) ).
cnf(c_12442,plain,
one = join(one,composition(sk1,sk1)),
inference(paramod,[status(thm)],[c_27,c_12441]) ).
cnf(c_810,plain,
join(one,composition(sk1,sk1)) = one,
inference(copy,[status(thm)],[c_12442]) ).
cnf(c_12443,plain,
composition(top,A) = join(composition(one,A),composition(complement(sk1),A)),
inference(paramod,[status(thm)],[c_807,c_10]) ).
cnf(c_12444,plain,
composition(top,A) = join(A,composition(complement(sk1),A)),
inference(paramod,[status(thm)],[c_164,c_12443]) ).
cnf(c_815,plain,
join(A,composition(complement(sk1),A)) = composition(top,A),
inference(copy,[status(thm)],[c_12444]) ).
cnf(c_12445,plain,
join(one,top) = join(one,complement(sk2)),
inference(paramod,[status(thm)],[c_17,c_91]) ).
cnf(c_12446,plain,
top = join(one,complement(sk2)),
inference(paramod,[status(thm)],[c_562,c_12445]) ).
cnf(c_859,plain,
join(one,complement(sk2)) = top,
inference(copy,[status(thm)],[c_12446]) ).
cnf(c_12447,plain,
join(one,sk2) = join(one,composition(sk2,sk2)),
inference(paramod,[status(thm)],[c_169,c_91]) ).
cnf(c_12448,plain,
one = join(one,composition(sk2,sk2)),
inference(paramod,[status(thm)],[c_29,c_12447]) ).
cnf(c_861,plain,
join(one,composition(sk2,sk2)) = one,
inference(copy,[status(thm)],[c_12448]) ).
cnf(c_12449,plain,
join(one,sk2) = join(one,composition(sk1,sk2)),
inference(paramod,[status(thm)],[c_170,c_91]) ).
cnf(c_12450,plain,
one = join(one,composition(sk1,sk2)),
inference(paramod,[status(thm)],[c_29,c_12449]) ).
cnf(c_862,plain,
join(one,composition(sk1,sk2)) = one,
inference(copy,[status(thm)],[c_12450]) ).
cnf(c_12451,plain,
join(complement(join(zero,A)),join(B,complement(join(complement(top),complement(A))))) = join(B,top),
inference(paramod,[status(thm)],[c_19,c_96]) ).
cnf(c_12452,plain,
join(complement(A),join(B,complement(join(complement(top),complement(A))))) = join(B,top),
inference(paramod,[status(thm)],[c_259,c_12451]) ).
cnf(c_12453,plain,
join(complement(A),join(B,complement(join(zero,complement(A))))) = join(B,top),
inference(paramod,[status(thm)],[c_19,c_12452]) ).
cnf(c_12454,plain,
join(complement(A),join(B,complement(complement(A)))) = join(B,top),
inference(paramod,[status(thm)],[c_259,c_12453]) ).
cnf(c_12455,plain,
join(complement(A),join(B,A)) = join(B,top),
inference(paramod,[status(thm)],[c_126,c_12454]) ).
cnf(c_928,plain,
join(complement(A),join(B,A)) = top,
inference(paramod,[status(thm)],[c_562,c_12455]) ).
cnf(c_12456,plain,
join(complement(converse(sk2)),one) = top,
inference(paramod,[status(thm)],[c_166,c_928]) ).
cnf(c_954,plain,
join(one,complement(converse(sk2))) = top,
inference(paramod,[status(thm)],[c_1,c_12456]) ).
cnf(c_12457,plain,
join(complement(converse(sk1)),one) = top,
inference(paramod,[status(thm)],[c_167,c_928]) ).
cnf(c_955,plain,
join(one,complement(converse(sk1))) = top,
inference(paramod,[status(thm)],[c_1,c_12457]) ).
cnf(c_12458,plain,
join(complement(composition(sk2,A)),A) = top,
inference(paramod,[status(thm)],[c_169,c_928]) ).
cnf(c_956,plain,
join(A,complement(composition(sk2,A))) = top,
inference(paramod,[status(thm)],[c_1,c_12458]) ).
cnf(c_12459,plain,
join(complement(composition(sk1,A)),A) = top,
inference(paramod,[status(thm)],[c_170,c_928]) ).
cnf(c_957,plain,
join(A,complement(composition(sk1,A))) = top,
inference(paramod,[status(thm)],[c_1,c_12459]) ).
cnf(c_12460,plain,
join(complement(composition(sk2,sk1)),one) = top,
inference(paramod,[status(thm)],[c_809,c_928]) ).
cnf(c_968,plain,
join(one,complement(composition(sk2,sk1))) = top,
inference(paramod,[status(thm)],[c_1,c_12460]) ).
cnf(c_12461,plain,
join(complement(composition(sk1,sk1)),one) = top,
inference(paramod,[status(thm)],[c_810,c_928]) ).
cnf(c_969,plain,
join(one,complement(composition(sk1,sk1))) = top,
inference(paramod,[status(thm)],[c_1,c_12461]) ).
cnf(c_12462,plain,
join(complement(composition(sk2,sk2)),one) = top,
inference(paramod,[status(thm)],[c_861,c_928]) ).
cnf(c_973,plain,
join(one,complement(composition(sk2,sk2))) = top,
inference(paramod,[status(thm)],[c_1,c_12462]) ).
cnf(c_12463,plain,
join(complement(composition(sk1,sk2)),one) = top,
inference(paramod,[status(thm)],[c_862,c_928]) ).
cnf(c_974,plain,
join(one,complement(composition(sk1,sk2))) = top,
inference(paramod,[status(thm)],[c_1,c_12463]) ).
cnf(c_12464,plain,
join(complement(join(complement(sk1),complement(one))),complement(top)) = sk1,
inference(paramod,[status(thm)],[c_807,c_101]) ).
cnf(c_12465,plain,
join(complement(join(complement(one),complement(sk1))),complement(top)) = sk1,
inference(paramod,[status(thm)],[c_1,c_12464]) ).
cnf(c_12466,plain,
join(complement(join(complement(one),complement(sk1))),zero) = sk1,
inference(paramod,[status(thm)],[c_19,c_12465]) ).
cnf(c_12467,plain,
join(zero,complement(join(complement(one),complement(sk1)))) = sk1,
inference(paramod,[status(thm)],[c_1,c_12466]) ).
cnf(c_1012,plain,
complement(join(complement(one),complement(sk1))) = sk1,
inference(paramod,[status(thm)],[c_259,c_12467]) ).
cnf(c_12468,plain,
join(complement(join(complement(sk2),complement(one))),complement(top)) = sk2,
inference(paramod,[status(thm)],[c_859,c_101]) ).
cnf(c_12469,plain,
join(complement(join(complement(one),complement(sk2))),complement(top)) = sk2,
inference(paramod,[status(thm)],[c_1,c_12468]) ).
cnf(c_12470,plain,
join(complement(join(complement(one),complement(sk2))),zero) = sk2,
inference(paramod,[status(thm)],[c_19,c_12469]) ).
cnf(c_12471,plain,
join(zero,complement(join(complement(one),complement(sk2)))) = sk2,
inference(paramod,[status(thm)],[c_1,c_12470]) ).
cnf(c_1013,plain,
complement(join(complement(one),complement(sk2))) = sk2,
inference(paramod,[status(thm)],[c_259,c_12471]) ).
cnf(c_12472,plain,
join(complement(join(complement(converse(sk2)),complement(one))),complement(top)) = converse(sk2),
inference(paramod,[status(thm)],[c_954,c_101]) ).
cnf(c_12473,plain,
join(complement(join(complement(one),complement(converse(sk2)))),complement(top)) = converse(sk2),
inference(paramod,[status(thm)],[c_1,c_12472]) ).
cnf(c_12474,plain,
join(complement(join(complement(one),complement(converse(sk2)))),zero) = converse(sk2),
inference(paramod,[status(thm)],[c_19,c_12473]) ).
cnf(c_12475,plain,
join(zero,complement(join(complement(one),complement(converse(sk2))))) = converse(sk2),
inference(paramod,[status(thm)],[c_1,c_12474]) ).
cnf(c_1014,plain,
complement(join(complement(one),complement(converse(sk2)))) = converse(sk2),
inference(paramod,[status(thm)],[c_259,c_12475]) ).
cnf(c_12476,plain,
join(complement(join(complement(converse(sk1)),complement(one))),complement(top)) = converse(sk1),
inference(paramod,[status(thm)],[c_955,c_101]) ).
cnf(c_12477,plain,
join(complement(join(complement(one),complement(converse(sk1)))),complement(top)) = converse(sk1),
inference(paramod,[status(thm)],[c_1,c_12476]) ).
cnf(c_12478,plain,
join(complement(join(complement(one),complement(converse(sk1)))),zero) = converse(sk1),
inference(paramod,[status(thm)],[c_19,c_12477]) ).
cnf(c_12479,plain,
join(zero,complement(join(complement(one),complement(converse(sk1))))) = converse(sk1),
inference(paramod,[status(thm)],[c_1,c_12478]) ).
cnf(c_1015,plain,
complement(join(complement(one),complement(converse(sk1)))) = converse(sk1),
inference(paramod,[status(thm)],[c_259,c_12479]) ).
cnf(c_12480,plain,
join(complement(join(complement(composition(sk2,A)),complement(A))),complement(top)) = composition(sk2,A),
inference(paramod,[status(thm)],[c_956,c_101]) ).
cnf(c_12481,plain,
join(complement(join(complement(A),complement(composition(sk2,A)))),complement(top)) = composition(sk2,A),
inference(paramod,[status(thm)],[c_1,c_12480]) ).
cnf(c_12482,plain,
join(complement(join(complement(A),complement(composition(sk2,A)))),zero) = composition(sk2,A),
inference(paramod,[status(thm)],[c_19,c_12481]) ).
cnf(c_12483,plain,
join(zero,complement(join(complement(A),complement(composition(sk2,A))))) = composition(sk2,A),
inference(paramod,[status(thm)],[c_1,c_12482]) ).
cnf(c_1016,plain,
complement(join(complement(A),complement(composition(sk2,A)))) = composition(sk2,A),
inference(paramod,[status(thm)],[c_259,c_12483]) ).
cnf(c_12484,plain,
join(complement(join(complement(composition(sk1,A)),complement(A))),complement(top)) = composition(sk1,A),
inference(paramod,[status(thm)],[c_957,c_101]) ).
cnf(c_12485,plain,
join(complement(join(complement(A),complement(composition(sk1,A)))),complement(top)) = composition(sk1,A),
inference(paramod,[status(thm)],[c_1,c_12484]) ).
cnf(c_12486,plain,
join(complement(join(complement(A),complement(composition(sk1,A)))),zero) = composition(sk1,A),
inference(paramod,[status(thm)],[c_19,c_12485]) ).
cnf(c_12487,plain,
join(zero,complement(join(complement(A),complement(composition(sk1,A))))) = composition(sk1,A),
inference(paramod,[status(thm)],[c_1,c_12486]) ).
cnf(c_1017,plain,
complement(join(complement(A),complement(composition(sk1,A)))) = composition(sk1,A),
inference(paramod,[status(thm)],[c_259,c_12487]) ).
cnf(c_12488,plain,
join(complement(join(A,B)),complement(join(complement(A),complement(complement(B))))) = complement(B),
inference(paramod,[status(thm)],[c_126,c_102]) ).
cnf(c_1024,plain,
join(complement(join(A,B)),complement(join(complement(A),B))) = complement(B),
inference(paramod,[status(thm)],[c_126,c_12488]) ).
cnf(c_12489,plain,
complement(sk1) = join(complement(one),complement(sk1)),
inference(paramod,[status(thm)],[c_1012,c_126]) ).
cnf(c_1048,plain,
join(complement(one),complement(sk1)) = complement(sk1),
inference(copy,[status(thm)],[c_12489]) ).
cnf(c_12490,plain,
join(complement(sk1),A) = join(complement(one),join(complement(sk1),A)),
inference(paramod,[status(thm)],[c_1048,c_3]) ).
cnf(c_1054,plain,
join(complement(one),join(complement(sk1),A)) = join(complement(sk1),A),
inference(copy,[status(thm)],[c_12490]) ).
cnf(c_12491,plain,
complement(sk2) = join(complement(one),complement(sk2)),
inference(paramod,[status(thm)],[c_1013,c_126]) ).
cnf(c_1067,plain,
join(complement(one),complement(sk2)) = complement(sk2),
inference(copy,[status(thm)],[c_12491]) ).
cnf(c_12492,plain,
join(complement(join(A,complement(B))),join(complement(join(complement(B),complement(A))),B)) = B,
inference(paramod,[status(thm)],[c_364,c_103]) ).
cnf(c_12493,plain,
join(complement(join(A,complement(B))),join(B,complement(join(complement(B),complement(A))))) = B,
inference(paramod,[status(thm)],[c_1,c_12492]) ).
cnf(c_12494,plain,
join(complement(join(A,complement(B))),B) = B,
inference(paramod,[status(thm)],[c_405,c_12493]) ).
cnf(c_1084,plain,
join(A,complement(join(B,complement(A)))) = A,
inference(paramod,[status(thm)],[c_1,c_12494]) ).
cnf(c_12495,plain,
join(complement(join(A,top)),complement(join(complement(composition(sk1,sk2)),complement(join(A,one))))) = composition(sk1,sk2),
inference(paramod,[status(thm)],[c_974,c_104]) ).
cnf(c_12496,plain,
join(complement(top),complement(join(complement(composition(sk1,sk2)),complement(join(A,one))))) = composition(sk1,sk2),
inference(paramod,[status(thm)],[c_562,c_12495]) ).
cnf(c_12497,plain,
join(zero,complement(join(complement(composition(sk1,sk2)),complement(join(A,one))))) = composition(sk1,sk2),
inference(paramod,[status(thm)],[c_19,c_12496]) ).
cnf(c_1129,plain,
complement(join(complement(composition(sk1,sk2)),complement(join(A,one)))) = composition(sk1,sk2),
inference(paramod,[status(thm)],[c_259,c_12497]) ).
cnf(c_12498,plain,
join(composition(complement(top),A),composition(complement(join(complement(composition(sk2,sk2)),complement(one))),A)) = composition(composition(sk2,sk2),A),
inference(paramod,[status(thm)],[c_973,c_108]) ).
cnf(c_12499,plain,
join(composition(zero,A),composition(complement(join(complement(composition(sk2,sk2)),complement(one))),A)) = composition(composition(sk2,sk2),A),
inference(paramod,[status(thm)],[c_19,c_12498]) ).
cnf(c_12500,plain,
join(zero,composition(complement(join(complement(composition(sk2,sk2)),complement(one))),A)) = composition(composition(sk2,sk2),A),
inference(paramod,[status(thm)],[c_758,c_12499]) ).
cnf(c_12501,plain,
join(zero,composition(complement(join(complement(one),complement(composition(sk2,sk2)))),A)) = composition(composition(sk2,sk2),A),
inference(paramod,[status(thm)],[c_1,c_12500]) ).
cnf(c_12502,plain,
composition(complement(join(complement(one),complement(composition(sk2,sk2)))),A) = composition(composition(sk2,sk2),A),
inference(paramod,[status(thm)],[c_259,c_12501]) ).
cnf(c_1141,plain,
composition(complement(join(complement(one),complement(composition(sk2,sk2)))),A) = composition(sk2,composition(sk2,A)),
inference(paramod,[status(thm)],[c_8,c_12502]) ).
cnf(c_12503,plain,
join(complement(sk2),A) = join(complement(one),join(complement(sk2),A)),
inference(paramod,[status(thm)],[c_1067,c_3]) ).
cnf(c_1144,plain,
join(complement(one),join(complement(sk2),A)) = join(complement(sk2),A),
inference(copy,[status(thm)],[c_12503]) ).
cnf(c_12504,plain,
join(converse(complement(top)),converse(complement(join(complement(composition(sk1,sk1)),complement(one))))) = converse(composition(sk1,sk1)),
inference(paramod,[status(thm)],[c_969,c_109]) ).
cnf(c_12505,plain,
join(converse(zero),converse(complement(join(complement(composition(sk1,sk1)),complement(one))))) = converse(composition(sk1,sk1)),
inference(paramod,[status(thm)],[c_19,c_12504]) ).
cnf(c_12506,plain,
join(zero,converse(complement(join(complement(composition(sk1,sk1)),complement(one))))) = converse(composition(sk1,sk1)),
inference(paramod,[status(thm)],[c_420,c_12505]) ).
cnf(c_12507,plain,
join(zero,converse(complement(join(complement(one),complement(composition(sk1,sk1)))))) = converse(composition(sk1,sk1)),
inference(paramod,[status(thm)],[c_1,c_12506]) ).
cnf(c_12508,plain,
converse(complement(join(complement(one),complement(composition(sk1,sk1))))) = converse(composition(sk1,sk1)),
inference(paramod,[status(thm)],[c_259,c_12507]) ).
cnf(c_1189,plain,
converse(complement(join(complement(one),complement(composition(sk1,sk1))))) = composition(converse(sk1),converse(sk1)),
inference(paramod,[status(thm)],[c_13,c_12508]) ).
cnf(c_12509,plain,
join(converse(complement(top)),converse(complement(join(complement(composition(sk2,sk2)),complement(one))))) = converse(composition(sk2,sk2)),
inference(paramod,[status(thm)],[c_973,c_109]) ).
cnf(c_12510,plain,
join(converse(zero),converse(complement(join(complement(composition(sk2,sk2)),complement(one))))) = converse(composition(sk2,sk2)),
inference(paramod,[status(thm)],[c_19,c_12509]) ).
cnf(c_12511,plain,
join(zero,converse(complement(join(complement(composition(sk2,sk2)),complement(one))))) = converse(composition(sk2,sk2)),
inference(paramod,[status(thm)],[c_420,c_12510]) ).
cnf(c_12512,plain,
join(zero,converse(complement(join(complement(one),complement(composition(sk2,sk2)))))) = converse(composition(sk2,sk2)),
inference(paramod,[status(thm)],[c_1,c_12511]) ).
cnf(c_12513,plain,
converse(complement(join(complement(one),complement(composition(sk2,sk2))))) = converse(composition(sk2,sk2)),
inference(paramod,[status(thm)],[c_259,c_12512]) ).
cnf(c_1190,plain,
converse(complement(join(complement(one),complement(composition(sk2,sk2))))) = composition(converse(sk2),converse(sk2)),
inference(paramod,[status(thm)],[c_13,c_12513]) ).
cnf(c_12514,plain,
join(A,composition(converse(converse(A)),sk2)) = converse(converse(A)),
inference(paramod,[status(thm)],[c_11,c_767]) ).
cnf(c_12515,plain,
join(A,composition(A,sk2)) = converse(converse(A)),
inference(paramod,[status(thm)],[c_11,c_12514]) ).
cnf(c_1338,plain,
join(A,composition(A,sk2)) = A,
inference(paramod,[status(thm)],[c_11,c_12515]) ).
cnf(c_12516,plain,
join(complement(composition(A,sk2)),A) = top,
inference(paramod,[status(thm)],[c_1338,c_928]) ).
cnf(c_1349,plain,
join(A,complement(composition(A,sk2))) = top,
inference(paramod,[status(thm)],[c_1,c_12516]) ).
cnf(c_12517,plain,
join(A,composition(converse(converse(A)),sk1)) = converse(converse(A)),
inference(paramod,[status(thm)],[c_11,c_772]) ).
cnf(c_12518,plain,
join(A,composition(A,sk1)) = converse(converse(A)),
inference(paramod,[status(thm)],[c_11,c_12517]) ).
cnf(c_1407,plain,
join(A,composition(A,sk1)) = A,
inference(paramod,[status(thm)],[c_11,c_12518]) ).
cnf(c_12519,plain,
converse(composition(top,A)) = join(converse(A),converse(composition(complement(sk1),A))),
inference(paramod,[status(thm)],[c_815,c_12]) ).
cnf(c_12520,plain,
composition(converse(A),converse(top)) = join(converse(A),converse(composition(complement(sk1),A))),
inference(paramod,[status(thm)],[c_13,c_12519]) ).
cnf(c_12521,plain,
composition(converse(A),top) = join(converse(A),converse(composition(complement(sk1),A))),
inference(paramod,[status(thm)],[c_626,c_12520]) ).
cnf(c_12522,plain,
composition(converse(A),top) = join(converse(A),composition(converse(A),converse(complement(sk1)))),
inference(paramod,[status(thm)],[c_13,c_12521]) ).
cnf(c_1430,plain,
join(converse(A),composition(converse(A),converse(complement(sk1)))) = composition(converse(A),top),
inference(copy,[status(thm)],[c_12522]) ).
cnf(c_12523,plain,
join(complement(complement(sk1)),composition(complement(join(complement(one),complement(sk1))),complement(join(complement(one),complement(composition(converse(one),sk1)))))) = composition(complement(join(complement(one),complement(sk1))),complement(join(complement(one),complement(composition(converse(one),sk1))))),
inference(paramod,[status(thm)],[c_1048,c_168]) ).
cnf(c_12524,plain,
join(sk1,composition(complement(join(complement(one),complement(sk1))),complement(join(complement(one),complement(composition(converse(one),sk1)))))) = composition(complement(join(complement(one),complement(sk1))),complement(join(complement(one),complement(composition(converse(one),sk1))))),
inference(paramod,[status(thm)],[c_126,c_12523]) ).
cnf(c_12525,plain,
join(sk1,composition(complement(complement(sk1)),complement(join(complement(one),complement(composition(converse(one),sk1)))))) = composition(complement(join(complement(one),complement(sk1))),complement(join(complement(one),complement(composition(converse(one),sk1))))),
inference(paramod,[status(thm)],[c_1048,c_12524]) ).
cnf(c_12526,plain,
join(sk1,composition(sk1,complement(join(complement(one),complement(composition(converse(one),sk1)))))) = composition(complement(join(complement(one),complement(sk1))),complement(join(complement(one),complement(composition(converse(one),sk1))))),
inference(paramod,[status(thm)],[c_126,c_12525]) ).
cnf(c_12527,plain,
join(sk1,composition(sk1,complement(join(complement(one),complement(composition(one,sk1)))))) = composition(complement(join(complement(one),complement(sk1))),complement(join(complement(one),complement(composition(converse(one),sk1))))),
inference(paramod,[status(thm)],[c_145,c_12526]) ).
cnf(c_12528,plain,
join(sk1,composition(sk1,complement(join(complement(one),complement(sk1))))) = composition(complement(join(complement(one),complement(sk1))),complement(join(complement(one),complement(composition(converse(one),sk1))))),
inference(paramod,[status(thm)],[c_164,c_12527]) ).
cnf(c_12529,plain,
join(sk1,composition(sk1,complement(complement(sk1)))) = composition(complement(join(complement(one),complement(sk1))),complement(join(complement(one),complement(composition(converse(one),sk1))))),
inference(paramod,[status(thm)],[c_1048,c_12528]) ).
cnf(c_12530,plain,
join(sk1,composition(sk1,sk1)) = composition(complement(join(complement(one),complement(sk1))),complement(join(complement(one),complement(composition(converse(one),sk1))))),
inference(paramod,[status(thm)],[c_126,c_12529]) ).
cnf(c_12531,plain,
sk1 = composition(complement(join(complement(one),complement(sk1))),complement(join(complement(one),complement(composition(converse(one),sk1))))),
inference(paramod,[status(thm)],[c_1407,c_12530]) ).
cnf(c_12532,plain,
sk1 = composition(complement(complement(sk1)),complement(join(complement(one),complement(composition(converse(one),sk1))))),
inference(paramod,[status(thm)],[c_1048,c_12531]) ).
cnf(c_12533,plain,
sk1 = composition(sk1,complement(join(complement(one),complement(composition(converse(one),sk1))))),
inference(paramod,[status(thm)],[c_126,c_12532]) ).
cnf(c_12534,plain,
sk1 = composition(sk1,complement(join(complement(one),complement(composition(one,sk1))))),
inference(paramod,[status(thm)],[c_145,c_12533]) ).
cnf(c_12535,plain,
sk1 = composition(sk1,complement(join(complement(one),complement(sk1)))),
inference(paramod,[status(thm)],[c_164,c_12534]) ).
cnf(c_12536,plain,
sk1 = composition(sk1,complement(complement(sk1))),
inference(paramod,[status(thm)],[c_1048,c_12535]) ).
cnf(c_12537,plain,
sk1 = composition(sk1,sk1),
inference(paramod,[status(thm)],[c_126,c_12536]) ).
cnf(c_1482,plain,
composition(sk1,sk1) = sk1,
inference(copy,[status(thm)],[c_12537]) ).
cnf(c_12538,plain,
join(complement(complement(sk2)),composition(complement(join(complement(one),complement(sk2))),complement(join(complement(one),complement(composition(converse(one),sk2)))))) = composition(complement(join(complement(one),complement(sk2))),complement(join(complement(one),complement(composition(converse(one),sk2))))),
inference(paramod,[status(thm)],[c_1067,c_168]) ).
cnf(c_12539,plain,
join(sk2,composition(complement(join(complement(one),complement(sk2))),complement(join(complement(one),complement(composition(converse(one),sk2)))))) = composition(complement(join(complement(one),complement(sk2))),complement(join(complement(one),complement(composition(converse(one),sk2))))),
inference(paramod,[status(thm)],[c_126,c_12538]) ).
cnf(c_12540,plain,
join(sk2,composition(complement(complement(sk2)),complement(join(complement(one),complement(composition(converse(one),sk2)))))) = composition(complement(join(complement(one),complement(sk2))),complement(join(complement(one),complement(composition(converse(one),sk2))))),
inference(paramod,[status(thm)],[c_1067,c_12539]) ).
cnf(c_12541,plain,
join(sk2,composition(sk2,complement(join(complement(one),complement(composition(converse(one),sk2)))))) = composition(complement(join(complement(one),complement(sk2))),complement(join(complement(one),complement(composition(converse(one),sk2))))),
inference(paramod,[status(thm)],[c_126,c_12540]) ).
cnf(c_12542,plain,
join(sk2,composition(sk2,complement(join(complement(one),complement(composition(one,sk2)))))) = composition(complement(join(complement(one),complement(sk2))),complement(join(complement(one),complement(composition(converse(one),sk2))))),
inference(paramod,[status(thm)],[c_145,c_12541]) ).
cnf(c_12543,plain,
join(sk2,composition(sk2,complement(join(complement(one),complement(sk2))))) = composition(complement(join(complement(one),complement(sk2))),complement(join(complement(one),complement(composition(converse(one),sk2))))),
inference(paramod,[status(thm)],[c_164,c_12542]) ).
cnf(c_12544,plain,
join(sk2,composition(sk2,complement(complement(sk2)))) = composition(complement(join(complement(one),complement(sk2))),complement(join(complement(one),complement(composition(converse(one),sk2))))),
inference(paramod,[status(thm)],[c_1067,c_12543]) ).
cnf(c_12545,plain,
join(sk2,composition(sk2,sk2)) = composition(complement(join(complement(one),complement(sk2))),complement(join(complement(one),complement(composition(converse(one),sk2))))),
inference(paramod,[status(thm)],[c_126,c_12544]) ).
cnf(c_12546,plain,
sk2 = composition(complement(join(complement(one),complement(sk2))),complement(join(complement(one),complement(composition(converse(one),sk2))))),
inference(paramod,[status(thm)],[c_1338,c_12545]) ).
cnf(c_12547,plain,
sk2 = composition(complement(complement(sk2)),complement(join(complement(one),complement(composition(converse(one),sk2))))),
inference(paramod,[status(thm)],[c_1067,c_12546]) ).
cnf(c_12548,plain,
sk2 = composition(sk2,complement(join(complement(one),complement(composition(converse(one),sk2))))),
inference(paramod,[status(thm)],[c_126,c_12547]) ).
cnf(c_12549,plain,
sk2 = composition(sk2,complement(join(complement(one),complement(composition(one,sk2))))),
inference(paramod,[status(thm)],[c_145,c_12548]) ).
cnf(c_12550,plain,
sk2 = composition(sk2,complement(join(complement(one),complement(sk2)))),
inference(paramod,[status(thm)],[c_164,c_12549]) ).
cnf(c_12551,plain,
sk2 = composition(sk2,complement(complement(sk2))),
inference(paramod,[status(thm)],[c_1067,c_12550]) ).
cnf(c_12552,plain,
sk2 = composition(sk2,sk2),
inference(paramod,[status(thm)],[c_126,c_12551]) ).
cnf(c_1483,plain,
composition(sk2,sk2) = sk2,
inference(copy,[status(thm)],[c_12552]) ).
cnf(c_12553,plain,
converse(complement(join(complement(one),complement(sk1)))) = composition(converse(sk1),converse(sk1)),
inference(paramod,[status(thm)],[c_1482,c_1189]) ).
cnf(c_12554,plain,
converse(complement(complement(sk1))) = composition(converse(sk1),converse(sk1)),
inference(paramod,[status(thm)],[c_1048,c_12553]) ).
cnf(c_12555,plain,
converse(sk1) = composition(converse(sk1),converse(sk1)),
inference(paramod,[status(thm)],[c_126,c_12554]) ).
cnf(c_1484,plain,
composition(converse(sk1),converse(sk1)) = converse(sk1),
inference(copy,[status(thm)],[c_12555]) ).
cnf(c_12556,plain,
converse(complement(join(complement(one),complement(sk2)))) = composition(converse(sk2),converse(sk2)),
inference(paramod,[status(thm)],[c_1483,c_1190]) ).
cnf(c_12557,plain,
converse(complement(complement(sk2))) = composition(converse(sk2),converse(sk2)),
inference(paramod,[status(thm)],[c_1067,c_12556]) ).
cnf(c_12558,plain,
converse(sk2) = composition(converse(sk2),converse(sk2)),
inference(paramod,[status(thm)],[c_126,c_12557]) ).
cnf(c_1486,plain,
composition(converse(sk2),converse(sk2)) = converse(sk2),
inference(copy,[status(thm)],[c_12558]) ).
cnf(c_12559,plain,
composition(complement(join(complement(one),complement(sk2))),A) = composition(sk2,composition(sk2,A)),
inference(paramod,[status(thm)],[c_1483,c_1141]) ).
cnf(c_12560,plain,
composition(complement(complement(sk2)),A) = composition(sk2,composition(sk2,A)),
inference(paramod,[status(thm)],[c_1067,c_12559]) ).
cnf(c_12561,plain,
composition(sk2,A) = composition(sk2,composition(sk2,A)),
inference(paramod,[status(thm)],[c_126,c_12560]) ).
cnf(c_1487,plain,
composition(sk2,composition(sk2,A)) = composition(sk2,A),
inference(copy,[status(thm)],[c_12561]) ).
cnf(c_12562,plain,
join(complement(join(complement(sk1),complement(converse(sk1)))),complement(join(complement(converse(sk1)),complement(composition(sk1,complement(join(complement(one),complement(converse(sk1))))))))) = complement(join(complement(converse(sk1)),complement(composition(sk1,complement(join(complement(one),complement(composition(converse(sk1),converse(sk1))))))))),
inference(paramod,[status(thm)],[c_1484,c_76]) ).
cnf(c_12563,plain,
join(complement(join(complement(sk1),complement(converse(sk1)))),complement(join(complement(converse(sk1)),complement(composition(sk1,converse(sk1)))))) = complement(join(complement(converse(sk1)),complement(composition(sk1,complement(join(complement(one),complement(composition(converse(sk1),converse(sk1))))))))),
inference(paramod,[status(thm)],[c_1015,c_12562]) ).
cnf(c_12564,plain,
join(complement(join(complement(sk1),complement(converse(sk1)))),composition(sk1,converse(sk1))) = complement(join(complement(converse(sk1)),complement(composition(sk1,complement(join(complement(one),complement(composition(converse(sk1),converse(sk1))))))))),
inference(paramod,[status(thm)],[c_1017,c_12563]) ).
cnf(c_12565,plain,
join(complement(join(complement(sk1),complement(converse(sk1)))),composition(sk1,converse(sk1))) = complement(join(complement(converse(sk1)),complement(composition(sk1,complement(join(complement(one),complement(converse(sk1)))))))),
inference(paramod,[status(thm)],[c_1484,c_12564]) ).
cnf(c_12566,plain,
join(complement(join(complement(sk1),complement(converse(sk1)))),composition(sk1,converse(sk1))) = complement(join(complement(converse(sk1)),complement(composition(sk1,converse(sk1))))),
inference(paramod,[status(thm)],[c_1015,c_12565]) ).
cnf(c_1540,plain,
join(complement(join(complement(sk1),complement(converse(sk1)))),composition(sk1,converse(sk1))) = composition(sk1,converse(sk1)),
inference(paramod,[status(thm)],[c_1017,c_12566]) ).
cnf(c_12567,plain,
join(complement(join(complement(one),complement(converse(sk1)))),complement(join(complement(one),complement(composition(converse(sk1),complement(join(complement(converse(sk1)),complement(converse(converse(sk1)))))))))) = complement(join(complement(one),complement(composition(converse(sk1),complement(join(complement(converse(sk1)),complement(converse(converse(sk1))))))))),
inference(paramod,[status(thm)],[c_1484,c_77]) ).
cnf(c_12568,plain,
join(converse(sk1),complement(join(complement(one),complement(composition(converse(sk1),complement(join(complement(converse(sk1)),complement(converse(converse(sk1)))))))))) = complement(join(complement(one),complement(composition(converse(sk1),complement(join(complement(converse(sk1)),complement(converse(converse(sk1))))))))),
inference(paramod,[status(thm)],[c_1015,c_12567]) ).
cnf(c_12569,plain,
join(converse(sk1),complement(join(complement(one),complement(composition(converse(sk1),complement(join(complement(converse(sk1)),complement(sk1)))))))) = complement(join(complement(one),complement(composition(converse(sk1),complement(join(complement(converse(sk1)),complement(converse(converse(sk1))))))))),
inference(paramod,[status(thm)],[c_11,c_12568]) ).
cnf(c_12570,plain,
join(converse(sk1),complement(join(complement(one),complement(composition(converse(sk1),complement(join(complement(sk1),complement(converse(sk1))))))))) = complement(join(complement(one),complement(composition(converse(sk1),complement(join(complement(converse(sk1)),complement(converse(converse(sk1))))))))),
inference(paramod,[status(thm)],[c_1,c_12569]) ).
cnf(c_12571,plain,
join(converse(sk1),complement(join(complement(one),complement(composition(converse(sk1),complement(join(complement(sk1),complement(converse(sk1))))))))) = complement(join(complement(one),complement(composition(converse(sk1),complement(join(complement(converse(sk1)),complement(sk1))))))),
inference(paramod,[status(thm)],[c_11,c_12570]) ).
cnf(c_1541,plain,
join(converse(sk1),complement(join(complement(one),complement(composition(converse(sk1),complement(join(complement(sk1),complement(converse(sk1))))))))) = complement(join(complement(one),complement(composition(converse(sk1),complement(join(complement(sk1),complement(converse(sk1)))))))),
inference(paramod,[status(thm)],[c_1,c_12571]) ).
cnf(c_12572,plain,
join(complement(join(complement(sk2),complement(converse(sk2)))),complement(join(complement(converse(sk2)),complement(composition(sk2,complement(join(complement(one),complement(converse(sk2))))))))) = complement(join(complement(converse(sk2)),complement(composition(sk2,complement(join(complement(one),complement(composition(converse(sk2),converse(sk2))))))))),
inference(paramod,[status(thm)],[c_1486,c_76]) ).
cnf(c_12573,plain,
join(complement(join(complement(sk2),complement(converse(sk2)))),complement(join(complement(converse(sk2)),complement(composition(sk2,converse(sk2)))))) = complement(join(complement(converse(sk2)),complement(composition(sk2,complement(join(complement(one),complement(composition(converse(sk2),converse(sk2))))))))),
inference(paramod,[status(thm)],[c_1014,c_12572]) ).
cnf(c_12574,plain,
join(complement(join(complement(sk2),complement(converse(sk2)))),composition(sk2,converse(sk2))) = complement(join(complement(converse(sk2)),complement(composition(sk2,complement(join(complement(one),complement(composition(converse(sk2),converse(sk2))))))))),
inference(paramod,[status(thm)],[c_1016,c_12573]) ).
cnf(c_12575,plain,
join(complement(join(complement(sk2),complement(converse(sk2)))),composition(sk2,converse(sk2))) = complement(join(complement(converse(sk2)),complement(composition(sk2,complement(join(complement(one),complement(converse(sk2)))))))),
inference(paramod,[status(thm)],[c_1486,c_12574]) ).
cnf(c_12576,plain,
join(complement(join(complement(sk2),complement(converse(sk2)))),composition(sk2,converse(sk2))) = complement(join(complement(converse(sk2)),complement(composition(sk2,converse(sk2))))),
inference(paramod,[status(thm)],[c_1014,c_12575]) ).
cnf(c_1565,plain,
join(complement(join(complement(sk2),complement(converse(sk2)))),composition(sk2,converse(sk2))) = composition(sk2,converse(sk2)),
inference(paramod,[status(thm)],[c_1016,c_12576]) ).
cnf(c_12577,plain,
join(complement(join(complement(one),complement(converse(sk2)))),complement(join(complement(one),complement(composition(converse(sk2),complement(join(complement(converse(sk2)),complement(converse(converse(sk2)))))))))) = complement(join(complement(one),complement(composition(converse(sk2),complement(join(complement(converse(sk2)),complement(converse(converse(sk2))))))))),
inference(paramod,[status(thm)],[c_1486,c_77]) ).
cnf(c_12578,plain,
join(converse(sk2),complement(join(complement(one),complement(composition(converse(sk2),complement(join(complement(converse(sk2)),complement(converse(converse(sk2)))))))))) = complement(join(complement(one),complement(composition(converse(sk2),complement(join(complement(converse(sk2)),complement(converse(converse(sk2))))))))),
inference(paramod,[status(thm)],[c_1014,c_12577]) ).
cnf(c_12579,plain,
join(converse(sk2),complement(join(complement(one),complement(composition(converse(sk2),complement(join(complement(converse(sk2)),complement(sk2)))))))) = complement(join(complement(one),complement(composition(converse(sk2),complement(join(complement(converse(sk2)),complement(converse(converse(sk2))))))))),
inference(paramod,[status(thm)],[c_11,c_12578]) ).
cnf(c_12580,plain,
join(converse(sk2),complement(join(complement(one),complement(composition(converse(sk2),complement(join(complement(sk2),complement(converse(sk2))))))))) = complement(join(complement(one),complement(composition(converse(sk2),complement(join(complement(converse(sk2)),complement(converse(converse(sk2))))))))),
inference(paramod,[status(thm)],[c_1,c_12579]) ).
cnf(c_12581,plain,
join(converse(sk2),complement(join(complement(one),complement(composition(converse(sk2),complement(join(complement(sk2),complement(converse(sk2))))))))) = complement(join(complement(one),complement(composition(converse(sk2),complement(join(complement(converse(sk2)),complement(sk2))))))),
inference(paramod,[status(thm)],[c_11,c_12580]) ).
cnf(c_1566,plain,
join(converse(sk2),complement(join(complement(one),complement(composition(converse(sk2),complement(join(complement(sk2),complement(converse(sk2))))))))) = complement(join(complement(one),complement(composition(converse(sk2),complement(join(complement(sk2),complement(converse(sk2)))))))),
inference(paramod,[status(thm)],[c_1,c_12581]) ).
cnf(c_12582,plain,
join(complement(join(complement(sk1),complement(converse(sk1)))),composition(complement(join(complement(one),complement(converse(sk1)))),complement(join(complement(sk1),complement(converse(sk1)))))) = composition(complement(join(complement(one),complement(composition(converse(sk1),converse(sk1))))),complement(join(complement(sk1),complement(converse(sk1))))),
inference(paramod,[status(thm)],[c_1484,c_171]) ).
cnf(c_12583,plain,
join(complement(join(complement(sk1),complement(converse(sk1)))),composition(converse(sk1),complement(join(complement(sk1),complement(converse(sk1)))))) = composition(complement(join(complement(one),complement(composition(converse(sk1),converse(sk1))))),complement(join(complement(sk1),complement(converse(sk1))))),
inference(paramod,[status(thm)],[c_1015,c_12582]) ).
cnf(c_12584,plain,
complement(join(complement(sk1),complement(converse(sk1)))) = composition(complement(join(complement(one),complement(composition(converse(sk1),converse(sk1))))),complement(join(complement(sk1),complement(converse(sk1))))),
inference(paramod,[status(thm)],[c_233,c_12583]) ).
cnf(c_12585,plain,
complement(join(complement(sk1),complement(converse(sk1)))) = composition(complement(join(complement(one),complement(converse(sk1)))),complement(join(complement(sk1),complement(converse(sk1))))),
inference(paramod,[status(thm)],[c_1484,c_12584]) ).
cnf(c_12586,plain,
complement(join(complement(sk1),complement(converse(sk1)))) = composition(converse(sk1),complement(join(complement(sk1),complement(converse(sk1))))),
inference(paramod,[status(thm)],[c_1015,c_12585]) ).
cnf(c_1589,plain,
composition(converse(sk1),complement(join(complement(sk1),complement(converse(sk1))))) = complement(join(complement(sk1),complement(converse(sk1)))),
inference(copy,[status(thm)],[c_12586]) ).
cnf(c_12587,plain,
join(complement(join(complement(sk2),complement(converse(sk2)))),composition(complement(join(complement(one),complement(converse(sk2)))),complement(join(complement(sk2),complement(converse(sk2)))))) = composition(complement(join(complement(one),complement(composition(converse(sk2),converse(sk2))))),complement(join(complement(sk2),complement(converse(sk2))))),
inference(paramod,[status(thm)],[c_1486,c_171]) ).
cnf(c_12588,plain,
join(complement(join(complement(sk2),complement(converse(sk2)))),composition(converse(sk2),complement(join(complement(sk2),complement(converse(sk2)))))) = composition(complement(join(complement(one),complement(composition(converse(sk2),converse(sk2))))),complement(join(complement(sk2),complement(converse(sk2))))),
inference(paramod,[status(thm)],[c_1014,c_12587]) ).
cnf(c_12589,plain,
complement(join(complement(sk2),complement(converse(sk2)))) = composition(complement(join(complement(one),complement(composition(converse(sk2),converse(sk2))))),complement(join(complement(sk2),complement(converse(sk2))))),
inference(paramod,[status(thm)],[c_175,c_12588]) ).
cnf(c_12590,plain,
complement(join(complement(sk2),complement(converse(sk2)))) = composition(complement(join(complement(one),complement(converse(sk2)))),complement(join(complement(sk2),complement(converse(sk2))))),
inference(paramod,[status(thm)],[c_1486,c_12589]) ).
cnf(c_12591,plain,
complement(join(complement(sk2),complement(converse(sk2)))) = composition(converse(sk2),complement(join(complement(sk2),complement(converse(sk2))))),
inference(paramod,[status(thm)],[c_1014,c_12590]) ).
cnf(c_1590,plain,
composition(converse(sk2),complement(join(complement(sk2),complement(converse(sk2))))) = complement(join(complement(sk2),complement(converse(sk2)))),
inference(copy,[status(thm)],[c_12591]) ).
cnf(c_12592,plain,
join(converse(sk1),complement(join(complement(one),complement(complement(join(complement(sk1),complement(converse(sk1)))))))) = complement(join(complement(one),complement(composition(converse(sk1),complement(join(complement(sk1),complement(converse(sk1)))))))),
inference(paramod,[status(thm)],[c_1589,c_1541]) ).
cnf(c_12593,plain,
join(converse(sk1),complement(join(complement(one),join(complement(sk1),complement(converse(sk1)))))) = complement(join(complement(one),complement(composition(converse(sk1),complement(join(complement(sk1),complement(converse(sk1)))))))),
inference(paramod,[status(thm)],[c_126,c_12592]) ).
cnf(c_12594,plain,
join(converse(sk1),complement(join(complement(sk1),complement(converse(sk1))))) = complement(join(complement(one),complement(composition(converse(sk1),complement(join(complement(sk1),complement(converse(sk1)))))))),
inference(paramod,[status(thm)],[c_1054,c_12593]) ).
cnf(c_12595,plain,
converse(sk1) = complement(join(complement(one),complement(composition(converse(sk1),complement(join(complement(sk1),complement(converse(sk1)))))))),
inference(paramod,[status(thm)],[c_1084,c_12594]) ).
cnf(c_12596,plain,
converse(sk1) = complement(join(complement(one),complement(complement(join(complement(sk1),complement(converse(sk1))))))),
inference(paramod,[status(thm)],[c_1589,c_12595]) ).
cnf(c_12597,plain,
converse(sk1) = complement(join(complement(one),join(complement(sk1),complement(converse(sk1))))),
inference(paramod,[status(thm)],[c_126,c_12596]) ).
cnf(c_12598,plain,
converse(sk1) = complement(join(complement(sk1),complement(converse(sk1)))),
inference(paramod,[status(thm)],[c_1054,c_12597]) ).
cnf(c_1591,plain,
complement(join(complement(sk1),complement(converse(sk1)))) = converse(sk1),
inference(copy,[status(thm)],[c_12598]) ).
cnf(c_12599,plain,
join(converse(sk2),complement(join(complement(one),complement(complement(join(complement(sk2),complement(converse(sk2)))))))) = complement(join(complement(one),complement(composition(converse(sk2),complement(join(complement(sk2),complement(converse(sk2)))))))),
inference(paramod,[status(thm)],[c_1590,c_1566]) ).
cnf(c_12600,plain,
join(converse(sk2),complement(join(complement(one),join(complement(sk2),complement(converse(sk2)))))) = complement(join(complement(one),complement(composition(converse(sk2),complement(join(complement(sk2),complement(converse(sk2)))))))),
inference(paramod,[status(thm)],[c_126,c_12599]) ).
cnf(c_12601,plain,
join(converse(sk2),complement(join(complement(sk2),complement(converse(sk2))))) = complement(join(complement(one),complement(composition(converse(sk2),complement(join(complement(sk2),complement(converse(sk2)))))))),
inference(paramod,[status(thm)],[c_1144,c_12600]) ).
cnf(c_12602,plain,
converse(sk2) = complement(join(complement(one),complement(composition(converse(sk2),complement(join(complement(sk2),complement(converse(sk2)))))))),
inference(paramod,[status(thm)],[c_1084,c_12601]) ).
cnf(c_12603,plain,
converse(sk2) = complement(join(complement(one),complement(complement(join(complement(sk2),complement(converse(sk2))))))),
inference(paramod,[status(thm)],[c_1590,c_12602]) ).
cnf(c_12604,plain,
converse(sk2) = complement(join(complement(one),join(complement(sk2),complement(converse(sk2))))),
inference(paramod,[status(thm)],[c_126,c_12603]) ).
cnf(c_12605,plain,
converse(sk2) = complement(join(complement(sk2),complement(converse(sk2)))),
inference(paramod,[status(thm)],[c_1144,c_12604]) ).
cnf(c_1592,plain,
complement(join(complement(sk2),complement(converse(sk2)))) = converse(sk2),
inference(copy,[status(thm)],[c_12605]) ).
cnf(c_12606,plain,
join(converse(sk1),composition(sk1,converse(sk1))) = composition(sk1,converse(sk1)),
inference(paramod,[status(thm)],[c_1591,c_1540]) ).
cnf(c_12607,plain,
converse(sk1) = composition(sk1,converse(sk1)),
inference(paramod,[status(thm)],[c_170,c_12606]) ).
cnf(c_1594,plain,
composition(sk1,converse(sk1)) = converse(sk1),
inference(copy,[status(thm)],[c_12607]) ).
cnf(c_12608,plain,
join(converse(sk2),composition(sk2,converse(sk2))) = composition(sk2,converse(sk2)),
inference(paramod,[status(thm)],[c_1592,c_1565]) ).
cnf(c_12609,plain,
converse(sk2) = composition(sk2,converse(sk2)),
inference(paramod,[status(thm)],[c_169,c_12608]) ).
cnf(c_1598,plain,
composition(sk2,converse(sk2)) = converse(sk2),
inference(copy,[status(thm)],[c_12609]) ).
cnf(c_12610,plain,
converse(converse(sk1)) = composition(converse(converse(sk1)),converse(sk1)),
inference(paramod,[status(thm)],[c_1594,c_13]) ).
cnf(c_12611,plain,
sk1 = composition(converse(converse(sk1)),converse(sk1)),
inference(paramod,[status(thm)],[c_11,c_12610]) ).
cnf(c_12612,plain,
sk1 = composition(sk1,converse(sk1)),
inference(paramod,[status(thm)],[c_11,c_12611]) ).
cnf(c_12613,plain,
sk1 = converse(sk1),
inference(paramod,[status(thm)],[c_1594,c_12612]) ).
cnf(c_1623,plain,
converse(sk1) = sk1,
inference(copy,[status(thm)],[c_12613]) ).
cnf(c_1663,plain,
join(sk1,converse(complement(sk1))) = top,
inference(paramod,[status(thm)],[c_1623,c_638]) ).
cnf(c_12614,plain,
converse(converse(sk2)) = composition(converse(converse(sk2)),converse(sk2)),
inference(paramod,[status(thm)],[c_1598,c_13]) ).
cnf(c_12615,plain,
sk2 = composition(converse(converse(sk2)),converse(sk2)),
inference(paramod,[status(thm)],[c_11,c_12614]) ).
cnf(c_12616,plain,
sk2 = composition(sk2,converse(sk2)),
inference(paramod,[status(thm)],[c_11,c_12615]) ).
cnf(c_12617,plain,
sk2 = converse(sk2),
inference(paramod,[status(thm)],[c_1598,c_12616]) ).
cnf(c_1675,plain,
converse(sk2) = sk2,
inference(copy,[status(thm)],[c_12617]) ).
cnf(c_12618,plain,
join(complement(A),join(composition(converse(B),complement(composition(B,A))),complement(join(complement(C),complement(A))))) = join(C,complement(join(complement(complement(A)),C))),
inference(paramod,[status(thm)],[c_196,c_44]) ).
cnf(c_12619,plain,
join(composition(converse(B),complement(composition(B,A))),join(complement(A),C)) = join(C,complement(join(complement(complement(A)),C))),
inference(paramod,[status(thm)],[c_410,c_12618]) ).
cnf(c_12620,plain,
join(complement(A),join(composition(converse(B),complement(composition(B,A))),C)) = join(C,complement(join(complement(complement(A)),C))),
inference(paramod,[status(thm)],[c_33,c_12619]) ).
cnf(c_12621,plain,
join(complement(A),C) = join(C,complement(join(complement(complement(A)),C))),
inference(paramod,[status(thm)],[c_44,c_12620]) ).
cnf(c_12622,plain,
join(complement(A),C) = join(C,complement(join(A,C))),
inference(paramod,[status(thm)],[c_126,c_12621]) ).
cnf(c_2108,plain,
join(A,complement(join(B,A))) = join(complement(B),A),
inference(copy,[status(thm)],[c_12622]) ).
cnf(c_2451,plain,
join(A,complement(join(A,B))) = join(complement(B),A),
inference(paramod,[status(thm)],[c_1,c_2108]) ).
cnf(c_12623,plain,
composition(join(complement(A),B),C) = join(composition(B,C),composition(complement(join(A,B)),C)),
inference(paramod,[status(thm)],[c_2108,c_10]) ).
cnf(c_12624,plain,
join(composition(complement(A),C),composition(B,C)) = join(composition(B,C),composition(complement(join(A,B)),C)),
inference(paramod,[status(thm)],[c_10,c_12623]) ).
cnf(c_2455,plain,
join(composition(A,B),composition(complement(join(C,A)),B)) = join(composition(complement(C),B),composition(A,B)),
inference(copy,[status(thm)],[c_12624]) ).
cnf(c_12625,plain,
join(converse(complement(A)),complement(top)) = join(complement(converse(A)),converse(complement(A))),
inference(paramod,[status(thm)],[c_638,c_2108]) ).
cnf(c_12626,plain,
join(converse(complement(A)),zero) = join(complement(converse(A)),converse(complement(A))),
inference(paramod,[status(thm)],[c_19,c_12625]) ).
cnf(c_12627,plain,
join(zero,converse(complement(A))) = join(complement(converse(A)),converse(complement(A))),
inference(paramod,[status(thm)],[c_1,c_12626]) ).
cnf(c_12628,plain,
converse(complement(A)) = join(complement(converse(A)),converse(complement(A))),
inference(paramod,[status(thm)],[c_259,c_12627]) ).
cnf(c_2466,plain,
join(complement(converse(A)),converse(complement(A))) = converse(complement(A)),
inference(copy,[status(thm)],[c_12628]) ).
cnf(c_12629,plain,
join(complement(composition(sk2,A)),complement(top)) = join(complement(A),complement(composition(sk2,A))),
inference(paramod,[status(thm)],[c_956,c_2108]) ).
cnf(c_12630,plain,
join(complement(composition(sk2,A)),zero) = join(complement(A),complement(composition(sk2,A))),
inference(paramod,[status(thm)],[c_19,c_12629]) ).
cnf(c_12631,plain,
join(zero,complement(composition(sk2,A))) = join(complement(A),complement(composition(sk2,A))),
inference(paramod,[status(thm)],[c_1,c_12630]) ).
cnf(c_12632,plain,
complement(composition(sk2,A)) = join(complement(A),complement(composition(sk2,A))),
inference(paramod,[status(thm)],[c_259,c_12631]) ).
cnf(c_2478,plain,
join(complement(A),complement(composition(sk2,A))) = complement(composition(sk2,A)),
inference(copy,[status(thm)],[c_12632]) ).
cnf(c_12633,plain,
join(complement(composition(sk1,A)),complement(top)) = join(complement(A),complement(composition(sk1,A))),
inference(paramod,[status(thm)],[c_957,c_2108]) ).
cnf(c_12634,plain,
join(complement(composition(sk1,A)),zero) = join(complement(A),complement(composition(sk1,A))),
inference(paramod,[status(thm)],[c_19,c_12633]) ).
cnf(c_12635,plain,
join(zero,complement(composition(sk1,A))) = join(complement(A),complement(composition(sk1,A))),
inference(paramod,[status(thm)],[c_1,c_12634]) ).
cnf(c_12636,plain,
complement(composition(sk1,A)) = join(complement(A),complement(composition(sk1,A))),
inference(paramod,[status(thm)],[c_259,c_12635]) ).
cnf(c_2479,plain,
join(complement(A),complement(composition(sk1,A))) = complement(composition(sk1,A)),
inference(copy,[status(thm)],[c_12636]) ).
cnf(c_12637,plain,
join(complement(composition(sk2,sk1)),complement(top)) = join(complement(one),complement(composition(sk2,sk1))),
inference(paramod,[status(thm)],[c_968,c_2108]) ).
cnf(c_12638,plain,
join(complement(composition(sk2,sk1)),zero) = join(complement(one),complement(composition(sk2,sk1))),
inference(paramod,[status(thm)],[c_19,c_12637]) ).
cnf(c_12639,plain,
join(zero,complement(composition(sk2,sk1))) = join(complement(one),complement(composition(sk2,sk1))),
inference(paramod,[status(thm)],[c_1,c_12638]) ).
cnf(c_12640,plain,
complement(composition(sk2,sk1)) = join(complement(one),complement(composition(sk2,sk1))),
inference(paramod,[status(thm)],[c_259,c_12639]) ).
cnf(c_2480,plain,
join(complement(one),complement(composition(sk2,sk1))) = complement(composition(sk2,sk1)),
inference(copy,[status(thm)],[c_12640]) ).
cnf(c_12641,plain,
join(complement(composition(sk1,sk2)),complement(top)) = join(complement(one),complement(composition(sk1,sk2))),
inference(paramod,[status(thm)],[c_974,c_2108]) ).
cnf(c_12642,plain,
join(complement(composition(sk1,sk2)),zero) = join(complement(one),complement(composition(sk1,sk2))),
inference(paramod,[status(thm)],[c_19,c_12641]) ).
cnf(c_12643,plain,
join(zero,complement(composition(sk1,sk2))) = join(complement(one),complement(composition(sk1,sk2))),
inference(paramod,[status(thm)],[c_1,c_12642]) ).
cnf(c_12644,plain,
complement(composition(sk1,sk2)) = join(complement(one),complement(composition(sk1,sk2))),
inference(paramod,[status(thm)],[c_259,c_12643]) ).
cnf(c_2482,plain,
join(complement(one),complement(composition(sk1,sk2))) = complement(composition(sk1,sk2)),
inference(copy,[status(thm)],[c_12644]) ).
cnf(c_12645,plain,
join(complement(composition(A,sk2)),complement(top)) = join(complement(A),complement(composition(A,sk2))),
inference(paramod,[status(thm)],[c_1349,c_2108]) ).
cnf(c_12646,plain,
join(complement(composition(A,sk2)),zero) = join(complement(A),complement(composition(A,sk2))),
inference(paramod,[status(thm)],[c_19,c_12645]) ).
cnf(c_12647,plain,
join(zero,complement(composition(A,sk2))) = join(complement(A),complement(composition(A,sk2))),
inference(paramod,[status(thm)],[c_1,c_12646]) ).
cnf(c_12648,plain,
complement(composition(A,sk2)) = join(complement(A),complement(composition(A,sk2))),
inference(paramod,[status(thm)],[c_259,c_12647]) ).
cnf(c_2486,plain,
join(complement(A),complement(composition(A,sk2))) = complement(composition(A,sk2)),
inference(copy,[status(thm)],[c_12648]) ).
cnf(c_12649,plain,
join(converse(complement(sk1)),complement(top)) = join(complement(sk1),converse(complement(sk1))),
inference(paramod,[status(thm)],[c_1663,c_2108]) ).
cnf(c_12650,plain,
join(converse(complement(sk1)),zero) = join(complement(sk1),converse(complement(sk1))),
inference(paramod,[status(thm)],[c_19,c_12649]) ).
cnf(c_12651,plain,
join(zero,converse(complement(sk1))) = join(complement(sk1),converse(complement(sk1))),
inference(paramod,[status(thm)],[c_1,c_12650]) ).
cnf(c_12652,plain,
converse(complement(sk1)) = join(complement(sk1),converse(complement(sk1))),
inference(paramod,[status(thm)],[c_259,c_12651]) ).
cnf(c_2498,plain,
join(complement(sk1),converse(complement(sk1))) = converse(complement(sk1)),
inference(copy,[status(thm)],[c_12652]) ).
cnf(c_12653,plain,
join(complement(join(A,B)),complement(join(complement(A),B))) = join(complement(B),complement(join(A,B))),
inference(paramod,[status(thm)],[c_2108,c_2108]) ).
cnf(c_12654,plain,
complement(B) = join(complement(B),complement(join(A,B))),
inference(paramod,[status(thm)],[c_1024,c_12653]) ).
cnf(c_2519,plain,
join(complement(A),complement(join(B,A))) = complement(A),
inference(copy,[status(thm)],[c_12654]) ).
cnf(c_12655,plain,
converse(converse(complement(sk1))) = join(converse(complement(sk1)),converse(converse(complement(sk1)))),
inference(paramod,[status(thm)],[c_2498,c_12]) ).
cnf(c_12656,plain,
complement(sk1) = join(converse(complement(sk1)),converse(converse(complement(sk1)))),
inference(paramod,[status(thm)],[c_11,c_12655]) ).
cnf(c_12657,plain,
complement(sk1) = join(converse(complement(sk1)),complement(sk1)),
inference(paramod,[status(thm)],[c_11,c_12656]) ).
cnf(c_12658,plain,
complement(sk1) = join(complement(sk1),converse(complement(sk1))),
inference(paramod,[status(thm)],[c_1,c_12657]) ).
cnf(c_12659,plain,
complement(sk1) = converse(complement(sk1)),
inference(paramod,[status(thm)],[c_2498,c_12658]) ).
cnf(c_2703,plain,
converse(complement(sk1)) = complement(sk1),
inference(copy,[status(thm)],[c_12659]) ).
cnf(c_2711,plain,
join(converse(A),composition(converse(A),complement(sk1))) = composition(converse(A),top),
inference(paramod,[status(thm)],[c_2703,c_1430]) ).
cnf(c_12660,plain,
join(composition(complement(join(A,complement(sk2))),B),composition(complement(join(complement(one),complement(join(A,complement(sk2))))),B)) = composition(one,B),
inference(paramod,[status(thm)],[c_1067,c_227]) ).
cnf(c_12661,plain,
join(composition(complement(complement(one)),B),composition(complement(join(A,complement(sk2))),B)) = composition(one,B),
inference(paramod,[status(thm)],[c_2455,c_12660]) ).
cnf(c_12662,plain,
join(composition(one,B),composition(complement(join(A,complement(sk2))),B)) = composition(one,B),
inference(paramod,[status(thm)],[c_126,c_12661]) ).
cnf(c_12663,plain,
join(B,composition(complement(join(A,complement(sk2))),B)) = composition(one,B),
inference(paramod,[status(thm)],[c_164,c_12662]) ).
cnf(c_2771,plain,
join(A,composition(complement(join(B,complement(sk2))),A)) = A,
inference(paramod,[status(thm)],[c_164,c_12663]) ).
cnf(c_2929,plain,
join(complement(A),complement(join(A,B))) = complement(A),
inference(paramod,[status(thm)],[c_1,c_2519]) ).
cnf(c_3064,plain,
join(complement(sk2),complement(join(A,one))) = complement(sk2),
inference(paramod,[status(thm)],[c_92,c_2929]) ).
cnf(c_3333,plain,
join(complement(A),converse(complement(converse(A)))) = converse(complement(converse(A))),
inference(paramod,[status(thm)],[c_11,c_2466]) ).
cnf(c_12664,plain,
converse(converse(complement(A))) = join(converse(complement(converse(A))),converse(converse(complement(A)))),
inference(paramod,[status(thm)],[c_2466,c_12]) ).
cnf(c_12665,plain,
complement(A) = join(converse(complement(converse(A))),converse(converse(complement(A)))),
inference(paramod,[status(thm)],[c_11,c_12664]) ).
cnf(c_12666,plain,
complement(A) = join(converse(complement(converse(A))),complement(A)),
inference(paramod,[status(thm)],[c_11,c_12665]) ).
cnf(c_12667,plain,
complement(A) = join(complement(A),converse(complement(converse(A)))),
inference(paramod,[status(thm)],[c_1,c_12666]) ).
cnf(c_12668,plain,
complement(A) = converse(complement(converse(A))),
inference(paramod,[status(thm)],[c_3333,c_12667]) ).
cnf(c_3334,plain,
converse(complement(converse(A))) = complement(A),
inference(copy,[status(thm)],[c_12668]) ).
cnf(c_3344,plain,
converse(complement(A)) = complement(converse(A)),
inference(paramod,[status(thm)],[c_3334,c_11]) ).
cnf(c_12669,plain,
join(complement(composition(sk1,A)),B) = join(complement(A),join(complement(composition(sk1,A)),B)),
inference(paramod,[status(thm)],[c_2479,c_3]) ).
cnf(c_4199,plain,
join(complement(A),join(complement(composition(sk1,A)),B)) = join(complement(composition(sk1,A)),B),
inference(copy,[status(thm)],[c_12669]) ).
cnf(c_12670,plain,
join(complement(complement(composition(sk2,sk1))),composition(complement(join(complement(sk2),complement(composition(one,converse(sk1))))),complement(join(complement(sk1),complement(composition(converse(sk2),one)))))) = composition(complement(join(complement(sk2),complement(composition(one,converse(sk1))))),complement(join(complement(sk1),complement(composition(converse(sk2),one))))),
inference(paramod,[status(thm)],[c_2480,c_62]) ).
cnf(c_12671,plain,
join(composition(sk2,sk1),composition(complement(join(complement(sk2),complement(composition(one,converse(sk1))))),complement(join(complement(sk1),complement(composition(converse(sk2),one)))))) = composition(complement(join(complement(sk2),complement(composition(one,converse(sk1))))),complement(join(complement(sk1),complement(composition(converse(sk2),one))))),
inference(paramod,[status(thm)],[c_126,c_12670]) ).
cnf(c_12672,plain,
join(composition(sk2,sk1),composition(complement(join(complement(sk2),complement(composition(one,sk1)))),complement(join(complement(sk1),complement(composition(converse(sk2),one)))))) = composition(complement(join(complement(sk2),complement(composition(one,converse(sk1))))),complement(join(complement(sk1),complement(composition(converse(sk2),one))))),
inference(paramod,[status(thm)],[c_1623,c_12671]) ).
cnf(c_12673,plain,
join(composition(sk2,sk1),composition(complement(join(complement(sk2),complement(sk1))),complement(join(complement(sk1),complement(composition(converse(sk2),one)))))) = composition(complement(join(complement(sk2),complement(composition(one,converse(sk1))))),complement(join(complement(sk1),complement(composition(converse(sk2),one))))),
inference(paramod,[status(thm)],[c_164,c_12672]) ).
cnf(c_12674,plain,
join(composition(sk2,sk1),composition(complement(join(complement(sk1),complement(sk2))),complement(join(complement(sk1),complement(composition(converse(sk2),one)))))) = composition(complement(join(complement(sk2),complement(composition(one,converse(sk1))))),complement(join(complement(sk1),complement(composition(converse(sk2),one))))),
inference(paramod,[status(thm)],[c_1,c_12673]) ).
cnf(c_12675,plain,
join(composition(sk2,sk1),composition(complement(join(complement(sk1),complement(sk2))),complement(join(complement(sk1),complement(composition(sk2,one)))))) = composition(complement(join(complement(sk2),complement(composition(one,converse(sk1))))),complement(join(complement(sk1),complement(composition(converse(sk2),one))))),
inference(paramod,[status(thm)],[c_1675,c_12674]) ).
cnf(c_12676,plain,
join(composition(sk2,sk1),composition(complement(join(complement(sk1),complement(sk2))),complement(join(complement(sk1),complement(sk2))))) = composition(complement(join(complement(sk2),complement(composition(one,converse(sk1))))),complement(join(complement(sk1),complement(composition(converse(sk2),one))))),
inference(paramod,[status(thm)],[c_9,c_12675]) ).
cnf(c_12677,plain,
join(composition(sk2,sk1),composition(complement(join(complement(sk1),complement(sk2))),complement(join(complement(sk1),complement(sk2))))) = composition(complement(join(complement(sk2),complement(composition(one,sk1)))),complement(join(complement(sk1),complement(composition(converse(sk2),one))))),
inference(paramod,[status(thm)],[c_1623,c_12676]) ).
cnf(c_12678,plain,
join(composition(sk2,sk1),composition(complement(join(complement(sk1),complement(sk2))),complement(join(complement(sk1),complement(sk2))))) = composition(complement(join(complement(sk2),complement(sk1))),complement(join(complement(sk1),complement(composition(converse(sk2),one))))),
inference(paramod,[status(thm)],[c_164,c_12677]) ).
cnf(c_12679,plain,
join(composition(sk2,sk1),composition(complement(join(complement(sk1),complement(sk2))),complement(join(complement(sk1),complement(sk2))))) = composition(complement(join(complement(sk1),complement(sk2))),complement(join(complement(sk1),complement(composition(converse(sk2),one))))),
inference(paramod,[status(thm)],[c_1,c_12678]) ).
cnf(c_12680,plain,
join(composition(sk2,sk1),composition(complement(join(complement(sk1),complement(sk2))),complement(join(complement(sk1),complement(sk2))))) = composition(complement(join(complement(sk1),complement(sk2))),complement(join(complement(sk1),complement(composition(sk2,one))))),
inference(paramod,[status(thm)],[c_1675,c_12679]) ).
cnf(c_4232,plain,
join(composition(sk2,sk1),composition(complement(join(complement(sk1),complement(sk2))),complement(join(complement(sk1),complement(sk2))))) = composition(complement(join(complement(sk1),complement(sk2))),complement(join(complement(sk1),complement(sk2)))),
inference(paramod,[status(thm)],[c_9,c_12680]) ).
cnf(c_12681,plain,
join(complement(join(complement(composition(converse(sk2),one)),complement(sk1))),complement(join(complement(sk1),complement(composition(converse(sk2),complement(complement(composition(sk2,sk1)))))))) = complement(join(complement(sk1),complement(composition(converse(sk2),complement(join(complement(one),complement(composition(sk2,sk1)))))))),
inference(paramod,[status(thm)],[c_2480,c_78]) ).
cnf(c_12682,plain,
join(complement(join(complement(composition(sk2,one)),complement(sk1))),complement(join(complement(sk1),complement(composition(converse(sk2),complement(complement(composition(sk2,sk1)))))))) = complement(join(complement(sk1),complement(composition(converse(sk2),complement(join(complement(one),complement(composition(sk2,sk1)))))))),
inference(paramod,[status(thm)],[c_1675,c_12681]) ).
cnf(c_12683,plain,
join(complement(join(complement(sk2),complement(sk1))),complement(join(complement(sk1),complement(composition(converse(sk2),complement(complement(composition(sk2,sk1)))))))) = complement(join(complement(sk1),complement(composition(converse(sk2),complement(join(complement(one),complement(composition(sk2,sk1)))))))),
inference(paramod,[status(thm)],[c_9,c_12682]) ).
cnf(c_12684,plain,
join(complement(join(complement(sk1),complement(sk2))),complement(join(complement(sk1),complement(composition(converse(sk2),complement(complement(composition(sk2,sk1)))))))) = complement(join(complement(sk1),complement(composition(converse(sk2),complement(join(complement(one),complement(composition(sk2,sk1)))))))),
inference(paramod,[status(thm)],[c_1,c_12683]) ).
cnf(c_12685,plain,
join(complement(join(complement(sk1),complement(sk2))),complement(join(complement(sk1),complement(composition(sk2,complement(complement(composition(sk2,sk1)))))))) = complement(join(complement(sk1),complement(composition(converse(sk2),complement(join(complement(one),complement(composition(sk2,sk1)))))))),
inference(paramod,[status(thm)],[c_1675,c_12684]) ).
cnf(c_12686,plain,
join(complement(join(complement(sk1),complement(sk2))),complement(join(complement(sk1),complement(composition(sk2,composition(sk2,sk1)))))) = complement(join(complement(sk1),complement(composition(converse(sk2),complement(join(complement(one),complement(composition(sk2,sk1)))))))),
inference(paramod,[status(thm)],[c_126,c_12685]) ).
cnf(c_12687,plain,
join(complement(join(complement(sk1),complement(sk2))),complement(join(complement(sk1),complement(composition(sk2,sk1))))) = complement(join(complement(sk1),complement(composition(converse(sk2),complement(join(complement(one),complement(composition(sk2,sk1)))))))),
inference(paramod,[status(thm)],[c_1487,c_12686]) ).
cnf(c_12688,plain,
join(complement(join(complement(sk1),complement(sk2))),complement(complement(composition(sk2,sk1)))) = complement(join(complement(sk1),complement(composition(converse(sk2),complement(join(complement(one),complement(composition(sk2,sk1)))))))),
inference(paramod,[status(thm)],[c_2478,c_12687]) ).
cnf(c_12689,plain,
join(complement(join(complement(sk1),complement(sk2))),composition(sk2,sk1)) = complement(join(complement(sk1),complement(composition(converse(sk2),complement(join(complement(one),complement(composition(sk2,sk1)))))))),
inference(paramod,[status(thm)],[c_126,c_12688]) ).
cnf(c_12690,plain,
join(complement(join(complement(sk1),complement(sk2))),composition(sk2,sk1)) = complement(join(complement(sk1),complement(composition(sk2,complement(join(complement(one),complement(composition(sk2,sk1)))))))),
inference(paramod,[status(thm)],[c_1675,c_12689]) ).
cnf(c_12691,plain,
join(complement(join(complement(sk1),complement(sk2))),composition(sk2,sk1)) = complement(join(complement(sk1),complement(composition(sk2,complement(complement(composition(sk2,sk1))))))),
inference(paramod,[status(thm)],[c_2480,c_12690]) ).
cnf(c_12692,plain,
join(complement(join(complement(sk1),complement(sk2))),composition(sk2,sk1)) = complement(join(complement(sk1),complement(composition(sk2,composition(sk2,sk1))))),
inference(paramod,[status(thm)],[c_126,c_12691]) ).
cnf(c_12693,plain,
join(complement(join(complement(sk1),complement(sk2))),composition(sk2,sk1)) = complement(join(complement(sk1),complement(composition(sk2,sk1)))),
inference(paramod,[status(thm)],[c_1487,c_12692]) ).
cnf(c_12694,plain,
join(complement(join(complement(sk1),complement(sk2))),composition(sk2,sk1)) = complement(complement(composition(sk2,sk1))),
inference(paramod,[status(thm)],[c_2478,c_12693]) ).
cnf(c_4236,plain,
join(complement(join(complement(sk1),complement(sk2))),composition(sk2,sk1)) = composition(sk2,sk1),
inference(paramod,[status(thm)],[c_126,c_12694]) ).
cnf(c_12695,plain,
join(complement(join(complement(composition(converse(sk1),one)),complement(sk2))),composition(complement(join(complement(converse(sk1)),complement(composition(sk2,converse(one))))),complement(complement(composition(sk1,sk2))))) = composition(complement(join(complement(converse(sk1)),complement(composition(sk2,converse(one))))),complement(join(complement(one),complement(composition(sk1,sk2))))),
inference(paramod,[status(thm)],[c_2482,c_68]) ).
cnf(c_12696,plain,
join(complement(join(complement(composition(sk1,one)),complement(sk2))),composition(complement(join(complement(converse(sk1)),complement(composition(sk2,converse(one))))),complement(complement(composition(sk1,sk2))))) = composition(complement(join(complement(converse(sk1)),complement(composition(sk2,converse(one))))),complement(join(complement(one),complement(composition(sk1,sk2))))),
inference(paramod,[status(thm)],[c_1623,c_12695]) ).
cnf(c_12697,plain,
join(complement(join(complement(sk1),complement(sk2))),composition(complement(join(complement(converse(sk1)),complement(composition(sk2,converse(one))))),complement(complement(composition(sk1,sk2))))) = composition(complement(join(complement(converse(sk1)),complement(composition(sk2,converse(one))))),complement(join(complement(one),complement(composition(sk1,sk2))))),
inference(paramod,[status(thm)],[c_9,c_12696]) ).
cnf(c_12698,plain,
join(complement(join(complement(sk1),complement(sk2))),composition(complement(join(complement(sk1),complement(composition(sk2,converse(one))))),complement(complement(composition(sk1,sk2))))) = composition(complement(join(complement(converse(sk1)),complement(composition(sk2,converse(one))))),complement(join(complement(one),complement(composition(sk1,sk2))))),
inference(paramod,[status(thm)],[c_1623,c_12697]) ).
cnf(c_12699,plain,
join(complement(join(complement(sk1),complement(sk2))),composition(complement(join(complement(sk1),complement(composition(sk2,one)))),complement(complement(composition(sk1,sk2))))) = composition(complement(join(complement(converse(sk1)),complement(composition(sk2,converse(one))))),complement(join(complement(one),complement(composition(sk1,sk2))))),
inference(paramod,[status(thm)],[c_145,c_12698]) ).
cnf(c_12700,plain,
join(complement(join(complement(sk1),complement(sk2))),composition(complement(join(complement(sk1),complement(sk2))),complement(complement(composition(sk1,sk2))))) = composition(complement(join(complement(converse(sk1)),complement(composition(sk2,converse(one))))),complement(join(complement(one),complement(composition(sk1,sk2))))),
inference(paramod,[status(thm)],[c_9,c_12699]) ).
cnf(c_12701,plain,
join(complement(join(complement(sk1),complement(sk2))),composition(complement(join(complement(sk1),complement(sk2))),composition(sk1,sk2))) = composition(complement(join(complement(converse(sk1)),complement(composition(sk2,converse(one))))),complement(join(complement(one),complement(composition(sk1,sk2))))),
inference(paramod,[status(thm)],[c_126,c_12700]) ).
cnf(c_12702,plain,
join(complement(join(complement(sk1),complement(sk2))),composition(complement(join(complement(sk1),complement(sk2))),composition(sk1,sk2))) = composition(complement(join(complement(sk1),complement(composition(sk2,converse(one))))),complement(join(complement(one),complement(composition(sk1,sk2))))),
inference(paramod,[status(thm)],[c_1623,c_12701]) ).
cnf(c_12703,plain,
join(complement(join(complement(sk1),complement(sk2))),composition(complement(join(complement(sk1),complement(sk2))),composition(sk1,sk2))) = composition(complement(join(complement(sk1),complement(composition(sk2,one)))),complement(join(complement(one),complement(composition(sk1,sk2))))),
inference(paramod,[status(thm)],[c_145,c_12702]) ).
cnf(c_12704,plain,
join(complement(join(complement(sk1),complement(sk2))),composition(complement(join(complement(sk1),complement(sk2))),composition(sk1,sk2))) = composition(complement(join(complement(sk1),complement(sk2))),complement(join(complement(one),complement(composition(sk1,sk2))))),
inference(paramod,[status(thm)],[c_9,c_12703]) ).
cnf(c_12705,plain,
join(complement(join(complement(sk1),complement(sk2))),composition(complement(join(complement(sk1),complement(sk2))),composition(sk1,sk2))) = composition(complement(join(complement(sk1),complement(sk2))),complement(complement(composition(sk1,sk2)))),
inference(paramod,[status(thm)],[c_2482,c_12704]) ).
cnf(c_4262,plain,
join(complement(join(complement(sk1),complement(sk2))),composition(complement(join(complement(sk1),complement(sk2))),composition(sk1,sk2))) = composition(complement(join(complement(sk1),complement(sk2))),composition(sk1,sk2)),
inference(paramod,[status(thm)],[c_126,c_12705]) ).
cnf(c_12706,plain,
join(A,composition(converse(converse(A)),complement(sk1))) = composition(converse(converse(A)),top),
inference(paramod,[status(thm)],[c_11,c_2711]) ).
cnf(c_12707,plain,
join(A,composition(A,complement(sk1))) = composition(converse(converse(A)),top),
inference(paramod,[status(thm)],[c_11,c_12706]) ).
cnf(c_5416,plain,
join(A,composition(A,complement(sk1))) = composition(A,top),
inference(paramod,[status(thm)],[c_11,c_12707]) ).
cnf(c_5548,plain,
join(complement(sk1),composition(sk2,top)) = join(sk2,complement(sk1)),
inference(paramod,[status(thm)],[c_5416,c_239]) ).
cnf(c_12708,plain,
converse(join(sk2,complement(sk1))) = join(converse(complement(sk1)),converse(composition(sk2,top))),
inference(paramod,[status(thm)],[c_5548,c_12]) ).
cnf(c_12709,plain,
join(converse(sk2),converse(complement(sk1))) = join(converse(complement(sk1)),converse(composition(sk2,top))),
inference(paramod,[status(thm)],[c_12,c_12708]) ).
cnf(c_12710,plain,
join(sk2,converse(complement(sk1))) = join(converse(complement(sk1)),converse(composition(sk2,top))),
inference(paramod,[status(thm)],[c_1675,c_12709]) ).
cnf(c_12711,plain,
join(sk2,complement(converse(sk1))) = join(converse(complement(sk1)),converse(composition(sk2,top))),
inference(paramod,[status(thm)],[c_3344,c_12710]) ).
cnf(c_12712,plain,
join(sk2,complement(sk1)) = join(converse(complement(sk1)),converse(composition(sk2,top))),
inference(paramod,[status(thm)],[c_1623,c_12711]) ).
cnf(c_12713,plain,
join(sk2,complement(sk1)) = join(complement(converse(sk1)),converse(composition(sk2,top))),
inference(paramod,[status(thm)],[c_3344,c_12712]) ).
cnf(c_12714,plain,
join(sk2,complement(sk1)) = join(complement(sk1),converse(composition(sk2,top))),
inference(paramod,[status(thm)],[c_1623,c_12713]) ).
cnf(c_12715,plain,
join(sk2,complement(sk1)) = join(complement(sk1),composition(converse(top),converse(sk2))),
inference(paramod,[status(thm)],[c_13,c_12714]) ).
cnf(c_12716,plain,
join(sk2,complement(sk1)) = join(complement(sk1),composition(top,converse(sk2))),
inference(paramod,[status(thm)],[c_626,c_12715]) ).
cnf(c_12717,plain,
join(sk2,complement(sk1)) = join(complement(sk1),composition(top,sk2)),
inference(paramod,[status(thm)],[c_1675,c_12716]) ).
cnf(c_5601,plain,
join(complement(sk1),composition(top,sk2)) = join(sk2,complement(sk1)),
inference(copy,[status(thm)],[c_12717]) ).
cnf(c_12718,plain,
join(composition(A,sk2),complement(A)) = join(complement(A),composition(top,sk2)),
inference(paramod,[status(thm)],[c_1338,c_588]) ).
cnf(c_12719,plain,
join(complement(A),composition(A,sk2)) = join(complement(A),composition(top,sk2)),
inference(paramod,[status(thm)],[c_1,c_12718]) ).
cnf(c_7219,plain,
join(complement(A),composition(top,sk2)) = join(complement(A),composition(A,sk2)),
inference(copy,[status(thm)],[c_12719]) ).
cnf(c_12720,plain,
join(complement(A),complement(join(complement(A),composition(A,sk2)))) = join(complement(composition(top,sk2)),complement(A)),
inference(paramod,[status(thm)],[c_7219,c_2451]) ).
cnf(c_12721,plain,
join(complement(composition(A,sk2)),complement(A)) = join(complement(composition(top,sk2)),complement(A)),
inference(paramod,[status(thm)],[c_2451,c_12720]) ).
cnf(c_12722,plain,
join(complement(A),complement(composition(A,sk2))) = join(complement(composition(top,sk2)),complement(A)),
inference(paramod,[status(thm)],[c_1,c_12721]) ).
cnf(c_7294,plain,
complement(composition(A,sk2)) = join(complement(composition(top,sk2)),complement(A)),
inference(paramod,[status(thm)],[c_2486,c_12722]) ).
cnf(c_7302,plain,
join(complement(sk1),composition(sk1,sk2)) = join(sk2,complement(sk1)),
inference(paramod,[status(thm)],[c_7219,c_5601]) ).
cnf(c_12723,plain,
join(complement(sk1),complement(join(sk2,complement(sk1)))) = join(complement(composition(sk1,sk2)),complement(sk1)),
inference(paramod,[status(thm)],[c_7302,c_2451]) ).
cnf(c_12724,plain,
join(complement(sk2),complement(sk1)) = join(complement(composition(sk1,sk2)),complement(sk1)),
inference(paramod,[status(thm)],[c_2108,c_12723]) ).
cnf(c_12725,plain,
join(complement(sk1),complement(sk2)) = join(complement(composition(sk1,sk2)),complement(sk1)),
inference(paramod,[status(thm)],[c_1,c_12724]) ).
cnf(c_12726,plain,
join(complement(sk1),complement(sk2)) = join(complement(sk1),complement(composition(sk1,sk2))),
inference(paramod,[status(thm)],[c_1,c_12725]) ).
cnf(c_12727,plain,
join(complement(sk1),complement(sk2)) = complement(composition(sk1,sk2)),
inference(paramod,[status(thm)],[c_2486,c_12726]) ).
cnf(c_7318,plain,
complement(composition(sk1,sk2)) = join(complement(sk1),complement(sk2)),
inference(copy,[status(thm)],[c_12727]) ).
cnf(c_12728,plain,
complement(join(join(complement(sk1),complement(sk2)),complement(join(A,one)))) = composition(sk1,sk2),
inference(paramod,[status(thm)],[c_7318,c_1129]) ).
cnf(c_12729,plain,
complement(join(complement(sk1),join(complement(sk2),complement(join(A,one))))) = composition(sk1,sk2),
inference(paramod,[status(thm)],[c_3,c_12728]) ).
cnf(c_12730,plain,
complement(join(complement(sk1),complement(sk2))) = composition(sk1,sk2),
inference(paramod,[status(thm)],[c_3064,c_12729]) ).
cnf(c_7325,plain,
composition(sk1,sk2) = complement(join(complement(sk1),complement(sk2))),
inference(copy,[status(thm)],[c_12730]) ).
cnf(c_12731,plain,
join(complement(join(complement(sk1),complement(sk2))),composition(complement(join(complement(sk1),complement(sk2))),complement(join(complement(sk1),complement(sk2))))) = composition(complement(join(complement(sk1),complement(sk2))),composition(sk1,sk2)),
inference(paramod,[status(thm)],[c_7325,c_4262]) ).
cnf(c_12732,plain,
complement(join(complement(sk1),complement(sk2))) = composition(complement(join(complement(sk1),complement(sk2))),composition(sk1,sk2)),
inference(paramod,[status(thm)],[c_2771,c_12731]) ).
cnf(c_12733,plain,
complement(join(complement(sk1),complement(sk2))) = composition(complement(join(complement(sk1),complement(sk2))),complement(join(complement(sk1),complement(sk2)))),
inference(paramod,[status(thm)],[c_7325,c_12732]) ).
cnf(c_7341,plain,
composition(complement(join(complement(sk1),complement(sk2))),complement(join(complement(sk1),complement(sk2)))) = complement(join(complement(sk1),complement(sk2))),
inference(copy,[status(thm)],[c_12733]) ).
cnf(c_12734,plain,
join(composition(sk2,sk1),complement(join(complement(sk1),complement(sk2)))) = composition(complement(join(complement(sk1),complement(sk2))),complement(join(complement(sk1),complement(sk2)))),
inference(paramod,[status(thm)],[c_7341,c_4232]) ).
cnf(c_12735,plain,
join(complement(join(complement(sk1),complement(sk2))),composition(sk2,sk1)) = composition(complement(join(complement(sk1),complement(sk2))),complement(join(complement(sk1),complement(sk2)))),
inference(paramod,[status(thm)],[c_1,c_12734]) ).
cnf(c_12736,plain,
composition(sk2,sk1) = composition(complement(join(complement(sk1),complement(sk2))),complement(join(complement(sk1),complement(sk2)))),
inference(paramod,[status(thm)],[c_4236,c_12735]) ).
cnf(c_7344,plain,
composition(sk2,sk1) = complement(join(complement(sk1),complement(sk2))),
inference(paramod,[status(thm)],[c_7341,c_12736]) ).
cnf(c_7528,plain,
composition(complement(join(complement(sk1),complement(sk2))),A) = composition(sk1,composition(sk2,A)),
inference(paramod,[status(thm)],[c_7325,c_8]) ).
cnf(c_12737,plain,
( join(complement(join(complement(composition(sk1,sk3)),complement(composition(sk2,sk3)))),composition(complement(join(complement(sk1),complement(sk2))),sk3)) != composition(complement(join(complement(sk1),complement(sk2))),sk3)
| join(complement(join(complement(composition(sk1,sk3)),complement(composition(sk2,sk3)))),composition(sk1,composition(sk2,sk3))) != complement(join(complement(composition(sk1,sk3)),complement(composition(sk2,sk3)))) ),
inference(paramod,[status(thm)],[c_7528,c_31]) ).
cnf(c_12738,plain,
( join(complement(join(complement(composition(sk1,sk3)),complement(composition(sk2,sk3)))),composition(sk1,composition(sk2,sk3))) != composition(complement(join(complement(sk1),complement(sk2))),sk3)
| join(complement(join(complement(composition(sk1,sk3)),complement(composition(sk2,sk3)))),composition(sk1,composition(sk2,sk3))) != complement(join(complement(composition(sk1,sk3)),complement(composition(sk2,sk3)))) ),
inference(paramod,[status(thm)],[c_7528,c_12737]) ).
cnf(c_7563,plain,
( join(complement(join(complement(composition(sk1,sk3)),complement(composition(sk2,sk3)))),composition(sk1,composition(sk2,sk3))) != composition(sk1,composition(sk2,sk3))
| join(complement(join(complement(composition(sk1,sk3)),complement(composition(sk2,sk3)))),composition(sk1,composition(sk2,sk3))) != complement(join(complement(composition(sk1,sk3)),complement(composition(sk2,sk3)))) ),
inference(paramod,[status(thm)],[c_7528,c_12738]) ).
cnf(c_12739,plain,
composition(complement(join(complement(sk1),complement(sk2))),A) = composition(sk2,composition(sk1,A)),
inference(paramod,[status(thm)],[c_7344,c_8]) ).
cnf(c_12740,plain,
composition(sk1,composition(sk2,A)) = composition(sk2,composition(sk1,A)),
inference(paramod,[status(thm)],[c_7528,c_12739]) ).
cnf(c_7564,plain,
composition(sk2,composition(sk1,A)) = composition(sk1,composition(sk2,A)),
inference(copy,[status(thm)],[c_12740]) ).
cnf(c_12741,plain,
converse(complement(composition(A,sk2))) = join(converse(complement(composition(top,sk2))),converse(complement(A))),
inference(paramod,[status(thm)],[c_7294,c_12]) ).
cnf(c_12742,plain,
complement(converse(composition(A,sk2))) = join(converse(complement(composition(top,sk2))),converse(complement(A))),
inference(paramod,[status(thm)],[c_3344,c_12741]) ).
cnf(c_12743,plain,
complement(composition(converse(sk2),converse(A))) = join(converse(complement(composition(top,sk2))),converse(complement(A))),
inference(paramod,[status(thm)],[c_13,c_12742]) ).
cnf(c_12744,plain,
complement(composition(sk2,converse(A))) = join(converse(complement(composition(top,sk2))),converse(complement(A))),
inference(paramod,[status(thm)],[c_1675,c_12743]) ).
cnf(c_12745,plain,
complement(composition(sk2,converse(A))) = join(complement(converse(composition(top,sk2))),converse(complement(A))),
inference(paramod,[status(thm)],[c_3344,c_12744]) ).
cnf(c_12746,plain,
complement(composition(sk2,converse(A))) = join(complement(composition(converse(sk2),converse(top))),converse(complement(A))),
inference(paramod,[status(thm)],[c_13,c_12745]) ).
cnf(c_12747,plain,
complement(composition(sk2,converse(A))) = join(complement(composition(sk2,converse(top))),converse(complement(A))),
inference(paramod,[status(thm)],[c_1675,c_12746]) ).
cnf(c_12748,plain,
complement(composition(sk2,converse(A))) = join(complement(composition(sk2,top)),converse(complement(A))),
inference(paramod,[status(thm)],[c_626,c_12747]) ).
cnf(c_7655,plain,
complement(composition(sk2,converse(A))) = join(complement(composition(sk2,top)),complement(converse(A))),
inference(paramod,[status(thm)],[c_3344,c_12748]) ).
cnf(c_12749,plain,
complement(composition(sk2,A)) = join(complement(composition(sk2,top)),complement(converse(converse(A)))),
inference(paramod,[status(thm)],[c_11,c_7655]) ).
cnf(c_11344,plain,
complement(composition(sk2,A)) = join(complement(composition(sk2,top)),complement(A)),
inference(paramod,[status(thm)],[c_11,c_12749]) ).
cnf(c_11411,plain,
complement(composition(sk2,A)) = join(complement(A),complement(composition(sk2,top))),
inference(paramod,[status(thm)],[c_11344,c_1]) ).
cnf(c_12750,plain,
( join(complement(join(complement(composition(sk1,sk3)),complement(composition(sk2,sk3)))),composition(sk1,composition(sk2,sk3))) != composition(sk1,composition(sk2,sk3))
| join(complement(join(complement(composition(sk1,sk3)),complement(composition(sk2,sk3)))),composition(sk1,composition(sk2,sk3))) != complement(join(complement(composition(sk1,sk3)),join(complement(composition(sk2,top)),complement(sk3)))) ),
inference(paramod,[status(thm)],[c_11344,c_7563]) ).
cnf(c_12751,plain,
( join(complement(join(complement(composition(sk1,sk3)),complement(composition(sk2,sk3)))),composition(sk1,composition(sk2,sk3))) != composition(sk1,composition(sk2,sk3))
| join(complement(join(complement(composition(sk1,sk3)),complement(composition(sk2,sk3)))),composition(sk1,composition(sk2,sk3))) != complement(join(complement(composition(sk1,sk3)),join(complement(sk3),complement(composition(sk2,top))))) ),
inference(paramod,[status(thm)],[c_1,c_12750]) ).
cnf(c_12752,plain,
( join(complement(join(complement(composition(sk1,sk3)),complement(composition(sk2,sk3)))),composition(sk1,composition(sk2,sk3))) != composition(sk1,composition(sk2,sk3))
| join(complement(join(complement(composition(sk1,sk3)),complement(composition(sk2,sk3)))),composition(sk1,composition(sk2,sk3))) != complement(join(complement(sk3),join(complement(composition(sk1,sk3)),complement(composition(sk2,top))))) ),
inference(paramod,[status(thm)],[c_33,c_12751]) ).
cnf(c_11585,plain,
( join(complement(join(complement(composition(sk1,sk3)),complement(composition(sk2,sk3)))),composition(sk1,composition(sk2,sk3))) != composition(sk1,composition(sk2,sk3))
| join(complement(join(complement(composition(sk1,sk3)),complement(composition(sk2,sk3)))),composition(sk1,composition(sk2,sk3))) != complement(join(complement(composition(sk1,sk3)),complement(composition(sk2,top)))) ),
inference(paramod,[status(thm)],[c_4199,c_12752]) ).
cnf(c_12753,plain,
( join(complement(join(complement(composition(sk1,sk3)),complement(composition(sk2,sk3)))),composition(sk1,composition(sk2,sk3))) != composition(sk1,composition(sk2,sk3))
| join(complement(join(complement(composition(sk1,sk3)),complement(composition(sk2,sk3)))),composition(sk1,composition(sk2,sk3))) != complement(complement(composition(sk2,composition(sk1,sk3)))) ),
inference(paramod,[status(thm)],[c_11411,c_11585]) ).
cnf(c_12754,plain,
( join(complement(join(complement(composition(sk1,sk3)),complement(composition(sk2,sk3)))),composition(sk1,composition(sk2,sk3))) != composition(sk1,composition(sk2,sk3))
| join(complement(join(complement(composition(sk1,sk3)),complement(composition(sk2,sk3)))),composition(sk1,composition(sk2,sk3))) != complement(complement(composition(sk1,composition(sk2,sk3)))) ),
inference(paramod,[status(thm)],[c_7564,c_12753]) ).
cnf(c_12755,plain,
( join(complement(join(complement(composition(sk1,sk3)),complement(composition(sk2,sk3)))),composition(sk1,composition(sk2,sk3))) != composition(sk1,composition(sk2,sk3))
| join(complement(join(complement(composition(sk1,sk3)),complement(composition(sk2,sk3)))),composition(sk1,composition(sk2,sk3))) != composition(sk1,composition(sk2,sk3)) ),
inference(paramod,[status(thm)],[c_126,c_12754]) ).
cnf(c_12004,plain,
join(complement(join(complement(composition(sk1,sk3)),complement(composition(sk2,sk3)))),composition(sk1,composition(sk2,sk3))) != composition(sk1,composition(sk2,sk3)),
inference(copy,[status(thm)],[c_12755]) ).
cnf(c_12756,plain,
join(complement(join(complement(composition(sk1,sk3)),join(complement(composition(sk2,top)),complement(sk3)))),composition(sk1,composition(sk2,sk3))) != composition(sk1,composition(sk2,sk3)),
inference(paramod,[status(thm)],[c_11344,c_12004]) ).
cnf(c_12757,plain,
join(complement(join(complement(composition(sk1,sk3)),join(complement(sk3),complement(composition(sk2,top))))),composition(sk1,composition(sk2,sk3))) != composition(sk1,composition(sk2,sk3)),
inference(paramod,[status(thm)],[c_1,c_12756]) ).
cnf(c_12758,plain,
join(complement(join(complement(sk3),join(complement(composition(sk1,sk3)),complement(composition(sk2,top))))),composition(sk1,composition(sk2,sk3))) != composition(sk1,composition(sk2,sk3)),
inference(paramod,[status(thm)],[c_33,c_12757]) ).
cnf(c_12270,plain,
join(complement(join(complement(composition(sk1,sk3)),complement(composition(sk2,top)))),composition(sk1,composition(sk2,sk3))) != composition(sk1,composition(sk2,sk3)),
inference(paramod,[status(thm)],[c_4199,c_12758]) ).
cnf(c_12759,plain,
join(complement(complement(composition(sk2,composition(sk1,sk3)))),composition(sk1,composition(sk2,sk3))) != composition(sk1,composition(sk2,sk3)),
inference(paramod,[status(thm)],[c_11411,c_12270]) ).
cnf(c_12760,plain,
join(complement(complement(composition(sk1,composition(sk2,sk3)))),composition(sk1,composition(sk2,sk3))) != composition(sk1,composition(sk2,sk3)),
inference(paramod,[status(thm)],[c_7564,c_12759]) ).
cnf(c_12761,plain,
join(composition(sk1,composition(sk2,sk3)),composition(sk1,composition(sk2,sk3))) != composition(sk1,composition(sk2,sk3)),
inference(paramod,[status(thm)],[c_126,c_12760]) ).
cnf(c_12762,plain,
composition(sk1,composition(sk2,sk3)) != composition(sk1,composition(sk2,sk3)),
inference(paramod,[status(thm)],[c_364,c_12761]) ).
cnf(c_12273,plain,
$false,
inference(copy,[status(thm)],[c_12762]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : REL029-4 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.02 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.04/15.33 % Computer : n012.cluster.edu
% 0.04/15.33 % Model : x86_64 x86_64
% 0.04/15.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.04/15.33 % Memory : 8046.5625MB
% 0.04/15.33 % OS : Linux 6.8.0-71-generic
% 0.04/15.33 % CPULimit : 300
% 0.04/15.33 % WCLimit : 300
% 0.04/15.33 % DateTime : Sat Sep 26 05:34:09 UTC 2026
% 0.04/15.33 % CPUTime :
% 0.04/15.33 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.04/15.33 % Process 4001342 was started by sandbox on n012,
% 0.04/15.33 % Sat Sep 26 05:34:09 2026
% 0.04/15.33 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.04/15.33
% 0.04/15.33 % From the command line: assign(max_seconds, 300).
% 26.81/18.74
% 26.81/18.74 % given #500 (A,wt=80): 647 join(complement(join(complement(A),complement(B))),composition(complement(join(complement(one),complement(composition(A,converse(B))))),complement(join(complement(B),complement(A))))) = composition(complement(join(complement(one),complement(composition(A,converse(B))))),complement(join(complement(B),complement(A)))). [para(145(a,1),62(a,1,2,2,1,2,1,1)),rewrite([164(3),164(14),145(27),164(27)])].
% 26.81/18.74
% 26.81/18.74 % SZS status Unsatisfiable for theBenchmark
% 26.81/18.74
% 26.81/18.74 % Proof 1 at 2.78 (+ 0.59) seconds.
% 26.81/18.74 % Length of proof is 212.
% 26.81/18.74 % Level of proof is 35.
% 26.81/18.74 % Maximum clause weight is 97.000.
% 26.81/18.74 % Given clauses 606.
% 26.81/18.74
% 26.81/18.74 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------