%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : REL030-3 : 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 : n011.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sun Sep 27 08:25:00 AM UTC 2026
% Result : Unsatisfiable 34.44s 5.00s
% Output : CNFRefutation 34.44s
% Verified :
% SZS Type : Refutation
% Derivation depth : 90
% Number of leaves : 17
% Syntax : Number of formulae : 364 ( 364 unt; 0 def)
% Number of atoms : 364 ( 363 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 15 ( 15 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 1 avg)
% Maximal term depth : 12 ( 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 : 470 ( 20 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_9431,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_9431]) ).
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_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_9432,plain,
zero = complement(join(complement(A),complement(complement(A)))),
inference(paramod,[status(thm)],[c_6,c_18]) ).
cnf(c_9433,plain,
zero = complement(top),
inference(paramod,[status(thm)],[c_17,c_9432]) ).
cnf(c_19,plain,
complement(top) = zero,
inference(copy,[status(thm)],[c_9433]) ).
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_9434,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_9435,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_9434]) ).
cnf(c_9436,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_9435]) ).
cnf(c_9437,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_9436]) ).
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_9437]) ).
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_9438,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_9439,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_9438]) ).
cnf(c_9440,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_9439]) ).
cnf(c_9441,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_9440]) ).
cnf(c_9442,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_9441]) ).
cnf(c_9443,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_9442]) ).
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_9443]) ).
fof(modular_law_2_16,axiom,
! [VAR_0,VAR_1,VAR_2] : join(meet(composition(VAR_0,VAR_1),VAR_2),meet(composition(meet(VAR_0,composition(VAR_2,converse(VAR_1))),VAR_1),VAR_2)) = meet(composition(meet(VAR_0,composition(VAR_2,converse(VAR_1))),VAR_1),VAR_2),
file('theBenchmark.p',modular_law_2_16) ).
cnf(c_24,plain,
join(meet(composition(A,B),C),meet(composition(meet(A,composition(C,converse(B))),B),C)) = meet(composition(meet(A,composition(C,converse(B))),B),C),
inference(clausify,[status(thm)],[modular_law_2_16]) ).
cnf(c_9444,plain,
join(complement(join(complement(composition(A,B)),complement(C))),meet(composition(meet(A,composition(C,converse(B))),B),C)) = meet(composition(meet(A,composition(C,converse(B))),B),C),
inference(paramod,[status(thm)],[c_6,c_24]) ).
cnf(c_9445,plain,
join(complement(join(complement(composition(A,B)),complement(C))),meet(composition(complement(join(complement(A),complement(composition(C,converse(B))))),B),C)) = meet(composition(meet(A,composition(C,converse(B))),B),C),
inference(paramod,[status(thm)],[c_6,c_9444]) ).
cnf(c_9446,plain,
join(complement(join(complement(composition(A,B)),complement(C))),complement(join(complement(composition(complement(join(complement(A),complement(composition(C,converse(B))))),B)),complement(C)))) = meet(composition(meet(A,composition(C,converse(B))),B),C),
inference(paramod,[status(thm)],[c_6,c_9445]) ).
cnf(c_9447,plain,
join(complement(join(complement(composition(A,B)),complement(C))),complement(join(complement(C),complement(composition(complement(join(complement(A),complement(composition(C,converse(B))))),B))))) = meet(composition(meet(A,composition(C,converse(B))),B),C),
inference(paramod,[status(thm)],[c_1,c_9446]) ).
cnf(c_9448,plain,
join(complement(join(complement(composition(A,B)),complement(C))),complement(join(complement(C),complement(composition(complement(join(complement(A),complement(composition(C,converse(B))))),B))))) = meet(composition(complement(join(complement(A),complement(composition(C,converse(B))))),B),C),
inference(paramod,[status(thm)],[c_6,c_9447]) ).
cnf(c_9449,plain,
join(complement(join(complement(composition(A,B)),complement(C))),complement(join(complement(C),complement(composition(complement(join(complement(A),complement(composition(C,converse(B))))),B))))) = complement(join(complement(composition(complement(join(complement(A),complement(composition(C,converse(B))))),B)),complement(C))),
inference(paramod,[status(thm)],[c_6,c_9448]) ).
cnf(c_25,plain,
join(complement(join(complement(composition(A,B)),complement(C))),complement(join(complement(C),complement(composition(complement(join(complement(A),complement(composition(C,converse(B))))),B))))) = complement(join(complement(C),complement(composition(complement(join(complement(A),complement(composition(C,converse(B))))),B)))),
inference(paramod,[status(thm)],[c_1,c_9449]) ).
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,
meet(composition(sk1,sk2),complement(sk3)) != meet(composition(sk1,sk2),complement(composition(sk1,sk3))),
file('theBenchmark.p',goals_18) ).
cnf(c_28,plain,
meet(composition(sk1,sk2),complement(sk3)) != meet(composition(sk1,sk2),complement(composition(sk1,sk3))),
inference(clausify,[status(thm)],[goals_18]) ).
cnf(c_9450,plain,
complement(join(complement(composition(sk1,sk2)),complement(complement(sk3)))) != meet(composition(sk1,sk2),complement(composition(sk1,sk3))),
inference(paramod,[status(thm)],[c_6,c_28]) ).
cnf(c_9451,plain,
complement(join(complement(complement(sk3)),complement(composition(sk1,sk2)))) != meet(composition(sk1,sk2),complement(composition(sk1,sk3))),
inference(paramod,[status(thm)],[c_1,c_9450]) ).
cnf(c_9452,plain,
complement(join(complement(complement(sk3)),complement(composition(sk1,sk2)))) != complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),
inference(paramod,[status(thm)],[c_6,c_9451]) ).
cnf(c_29,plain,
complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))) != complement(join(complement(complement(sk3)),complement(composition(sk1,sk2)))),
inference(copy,[status(thm)],[c_9452]) ).
cnf(c_9453,plain,
join(join(A,B),C) = join(B,join(A,C)),
inference(paramod,[status(thm)],[c_1,c_3]) ).
cnf(c_31,plain,
join(A,join(B,C)) = join(B,join(A,C)),
inference(paramod,[status(thm)],[c_3,c_9453]) ).
cnf(c_32,plain,
join(complement(join(A,complement(B))),complement(join(complement(B),complement(A)))) = B,
inference(paramod,[status(thm)],[c_1,c_5]) ).
cnf(c_33,plain,
join(complement(join(complement(A),B)),complement(join(complement(B),complement(A)))) = A,
inference(paramod,[status(thm)],[c_1,c_5]) ).
cnf(c_9454,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_34,plain,
join(complement(join(complement(A),B)),join(complement(join(complement(A),complement(B))),C)) = join(A,C),
inference(copy,[status(thm)],[c_9454]) ).
cnf(c_9455,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_9456,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_9455]) ).
cnf(c_9457,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_9456]) ).
cnf(c_36,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_9457]) ).
cnf(c_9458,plain,
converse(A) = composition(converse(one),converse(A)),
inference(paramod,[status(thm)],[c_9,c_13]) ).
cnf(c_40,plain,
composition(converse(one),converse(A)) = converse(A),
inference(copy,[status(thm)],[c_9458]) ).
cnf(c_9459,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_42,plain,
join(complement(A),join(composition(converse(B),complement(composition(B,A))),C)) = join(complement(A),C),
inference(copy,[status(thm)],[c_9459]) ).
cnf(c_9460,plain,
join(top,A) = join(B,join(complement(B),A)),
inference(paramod,[status(thm)],[c_17,c_3]) ).
cnf(c_50,plain,
join(A,join(complement(A),B)) = join(top,B),
inference(copy,[status(thm)],[c_9460]) ).
cnf(c_9461,plain,
join(complement(top),complement(join(complement(A),complement(complement(complement(A)))))) = A,
inference(paramod,[status(thm)],[c_17,c_5]) ).
cnf(c_52,plain,
join(zero,complement(join(complement(A),complement(complement(complement(A)))))) = A,
inference(paramod,[status(thm)],[c_19,c_9461]) ).
cnf(c_9462,plain,
composition(top,A) = join(composition(B,A),composition(complement(B),A)),
inference(paramod,[status(thm)],[c_17,c_10]) ).
cnf(c_54,plain,
join(composition(A,B),composition(complement(A),B)) = composition(top,B),
inference(copy,[status(thm)],[c_9462]) ).
cnf(c_9463,plain,
converse(top) = join(converse(A),converse(complement(A))),
inference(paramod,[status(thm)],[c_17,c_12]) ).
cnf(c_55,plain,
join(converse(A),converse(complement(A))) = converse(top),
inference(copy,[status(thm)],[c_9463]) ).
cnf(c_63,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_9464,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_9465,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_9464]) ).
cnf(c_75,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_9465]) ).
cnf(c_9466,plain,
join(one,A) = join(one,join(sk1,A)),
inference(paramod,[status(thm)],[c_27,c_3]) ).
cnf(c_85,plain,
join(one,join(sk1,A)) = join(one,A),
inference(copy,[status(thm)],[c_9466]) ).
cnf(c_9467,plain,
composition(one,A) = join(composition(one,A),composition(sk1,A)),
inference(paramod,[status(thm)],[c_27,c_10]) ).
cnf(c_87,plain,
join(composition(one,A),composition(sk1,A)) = composition(one,A),
inference(copy,[status(thm)],[c_9467]) ).
cnf(c_9468,plain,
converse(one) = join(converse(one),converse(sk1)),
inference(paramod,[status(thm)],[c_27,c_12]) ).
cnf(c_88,plain,
join(converse(one),converse(sk1)) = converse(one),
inference(copy,[status(thm)],[c_9468]) ).
cnf(c_9469,plain,
A = join(complement(join(complement(A),complement(B))),complement(join(B,complement(A)))),
inference(paramod,[status(thm)],[c_32,c_1]) ).
cnf(c_94,plain,
join(complement(join(complement(A),complement(B))),complement(join(B,complement(A)))) = A,
inference(copy,[status(thm)],[c_9469]) ).
cnf(c_9470,plain,
join(complement(join(complement(complement(A)),A)),complement(top)) = complement(A),
inference(paramod,[status(thm)],[c_17,c_33]) ).
cnf(c_9471,plain,
join(complement(join(A,complement(complement(A)))),complement(top)) = complement(A),
inference(paramod,[status(thm)],[c_1,c_9470]) ).
cnf(c_9472,plain,
join(complement(join(A,complement(complement(A)))),zero) = complement(A),
inference(paramod,[status(thm)],[c_19,c_9471]) ).
cnf(c_113,plain,
join(zero,complement(join(A,complement(complement(A))))) = complement(A),
inference(paramod,[status(thm)],[c_1,c_9472]) ).
cnf(c_9473,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_33,c_33]) ).
cnf(c_9474,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_9473]) ).
cnf(c_9475,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_9474]) ).
cnf(c_118,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_9475]) ).
cnf(c_119,plain,
complement(complement(A)) = A,
inference(paramod,[status(thm)],[c_113,c_52]) ).
cnf(c_120,plain,
join(zero,complement(join(A,A))) = complement(A),
inference(paramod,[status(thm)],[c_119,c_113]) ).
cnf(c_9476,plain,
complement(join(complement(composition(sk1,sk2)),composition(sk1,sk3))) != complement(join(complement(complement(sk3)),complement(composition(sk1,sk2)))),
inference(paramod,[status(thm)],[c_119,c_29]) ).
cnf(c_123,plain,
complement(join(complement(composition(sk1,sk2)),composition(sk1,sk3))) != complement(join(sk3,complement(composition(sk1,sk2)))),
inference(paramod,[status(thm)],[c_119,c_9476]) ).
cnf(c_9477,plain,
composition(converse(one),A) = converse(converse(A)),
inference(paramod,[status(thm)],[c_11,c_40]) ).
cnf(c_130,plain,
composition(converse(one),A) = A,
inference(paramod,[status(thm)],[c_11,c_9477]) ).
cnf(c_9478,plain,
join(complement(join(complement(converse(A)),complement(B))),composition(complement(join(complement(converse(one)),complement(composition(B,converse(converse(A)))))),complement(join(complement(converse(A)),complement(composition(converse(converse(one)),B)))))) = composition(complement(join(complement(converse(one)),complement(composition(B,converse(converse(A)))))),complement(join(complement(converse(A)),complement(composition(converse(converse(one)),B))))),
inference(paramod,[status(thm)],[c_40,c_21]) ).
cnf(c_9479,plain,
join(complement(join(complement(converse(A)),complement(B))),composition(complement(join(complement(converse(one)),complement(composition(B,A)))),complement(join(complement(converse(A)),complement(composition(converse(converse(one)),B)))))) = composition(complement(join(complement(converse(one)),complement(composition(B,converse(converse(A)))))),complement(join(complement(converse(A)),complement(composition(converse(converse(one)),B))))),
inference(paramod,[status(thm)],[c_11,c_9478]) ).
cnf(c_9480,plain,
join(complement(join(complement(converse(A)),complement(B))),composition(complement(join(complement(converse(one)),complement(composition(B,A)))),complement(join(complement(converse(A)),complement(composition(one,B)))))) = composition(complement(join(complement(converse(one)),complement(composition(B,converse(converse(A)))))),complement(join(complement(converse(A)),complement(composition(converse(converse(one)),B))))),
inference(paramod,[status(thm)],[c_11,c_9479]) ).
cnf(c_9481,plain,
join(complement(join(complement(converse(A)),complement(B))),composition(complement(join(complement(converse(one)),complement(composition(B,A)))),complement(join(complement(converse(A)),complement(composition(one,B)))))) = composition(complement(join(complement(converse(one)),complement(composition(B,A)))),complement(join(complement(converse(A)),complement(composition(converse(converse(one)),B))))),
inference(paramod,[status(thm)],[c_11,c_9480]) ).
cnf(c_132,plain,
join(complement(join(complement(converse(A)),complement(B))),composition(complement(join(complement(converse(one)),complement(composition(B,A)))),complement(join(complement(converse(A)),complement(composition(one,B)))))) = composition(complement(join(complement(converse(one)),complement(composition(B,A)))),complement(join(complement(converse(A)),complement(composition(one,B))))),
inference(paramod,[status(thm)],[c_11,c_9481]) ).
cnf(c_9482,plain,
join(complement(join(complement(converse(A)),complement(B))),complement(join(complement(B),complement(composition(complement(join(complement(converse(one)),complement(composition(B,converse(converse(A)))))),converse(A)))))) = complement(join(complement(B),complement(composition(complement(join(complement(converse(one)),complement(composition(B,converse(converse(A)))))),converse(A))))),
inference(paramod,[status(thm)],[c_40,c_25]) ).
cnf(c_9483,plain,
join(complement(join(complement(converse(A)),complement(B))),complement(join(complement(B),complement(composition(complement(join(complement(converse(one)),complement(composition(B,A)))),converse(A)))))) = complement(join(complement(B),complement(composition(complement(join(complement(converse(one)),complement(composition(B,converse(converse(A)))))),converse(A))))),
inference(paramod,[status(thm)],[c_11,c_9482]) ).
cnf(c_137,plain,
join(complement(join(complement(converse(A)),complement(B))),complement(join(complement(B),complement(composition(complement(join(complement(converse(one)),complement(composition(B,A)))),converse(A)))))) = complement(join(complement(B),complement(composition(complement(join(complement(converse(one)),complement(composition(B,A)))),converse(A))))),
inference(paramod,[status(thm)],[c_11,c_9483]) ).
cnf(c_9484,plain,
one = converse(one),
inference(paramod,[status(thm)],[c_130,c_9]) ).
cnf(c_139,plain,
converse(one) = one,
inference(copy,[status(thm)],[c_9484]) ).
cnf(c_143,plain,
join(complement(A),complement(composition(one,A))) = complement(A),
inference(paramod,[status(thm)],[c_130,c_15]) ).
cnf(c_9485,plain,
join(complement(join(complement(converse(A)),complement(B))),complement(join(complement(B),complement(composition(complement(join(complement(one),complement(composition(B,A)))),converse(A)))))) = complement(join(complement(B),complement(composition(complement(join(complement(converse(one)),complement(composition(B,A)))),converse(A))))),
inference(paramod,[status(thm)],[c_139,c_137]) ).
cnf(c_155,plain,
join(complement(join(complement(converse(A)),complement(B))),complement(join(complement(B),complement(composition(complement(join(complement(one),complement(composition(B,A)))),converse(A)))))) = complement(join(complement(B),complement(composition(complement(join(complement(one),complement(composition(B,A)))),converse(A))))),
inference(paramod,[status(thm)],[c_139,c_9485]) ).
cnf(c_9486,plain,
join(complement(join(complement(converse(A)),complement(B))),composition(complement(join(complement(one),complement(composition(B,A)))),complement(join(complement(converse(A)),complement(composition(one,B)))))) = composition(complement(join(complement(converse(one)),complement(composition(B,A)))),complement(join(complement(converse(A)),complement(composition(one,B))))),
inference(paramod,[status(thm)],[c_139,c_132]) ).
cnf(c_157,plain,
join(complement(join(complement(converse(A)),complement(B))),composition(complement(join(complement(one),complement(composition(B,A)))),complement(join(complement(converse(A)),complement(composition(one,B)))))) = composition(complement(join(complement(one),complement(composition(B,A)))),complement(join(complement(converse(A)),complement(composition(one,B))))),
inference(paramod,[status(thm)],[c_139,c_9486]) ).
cnf(c_158,plain,
composition(one,A) = A,
inference(paramod,[status(thm)],[c_139,c_130]) ).
cnf(c_9487,plain,
join(one,converse(sk1)) = converse(one),
inference(paramod,[status(thm)],[c_139,c_88]) ).
cnf(c_160,plain,
join(one,converse(sk1)) = one,
inference(paramod,[status(thm)],[c_139,c_9487]) ).
cnf(c_9488,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_139,c_63]) ).
cnf(c_9489,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_9488]) ).
cnf(c_9490,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_139,c_9489]) ).
cnf(c_161,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_9490]) ).
cnf(c_9491,plain,
join(A,composition(sk1,A)) = composition(one,A),
inference(paramod,[status(thm)],[c_158,c_87]) ).
cnf(c_162,plain,
join(A,composition(sk1,A)) = A,
inference(paramod,[status(thm)],[c_158,c_9491]) ).
cnf(c_9492,plain,
join(complement(join(complement(converse(A)),complement(B))),composition(complement(join(complement(one),complement(composition(B,A)))),complement(join(complement(converse(A)),complement(B))))) = composition(complement(join(complement(one),complement(composition(B,A)))),complement(join(complement(converse(A)),complement(composition(one,B))))),
inference(paramod,[status(thm)],[c_158,c_157]) ).
cnf(c_164,plain,
join(complement(join(complement(converse(A)),complement(B))),composition(complement(join(complement(one),complement(composition(B,A)))),complement(join(complement(converse(A)),complement(B))))) = composition(complement(join(complement(one),complement(composition(B,A)))),complement(join(complement(converse(A)),complement(B)))),
inference(paramod,[status(thm)],[c_158,c_9492]) ).
cnf(c_165,plain,
join(complement(A),complement(A)) = complement(A),
inference(paramod,[status(thm)],[c_158,c_143]) ).
cnf(c_9493,plain,
composition(one,A) = join(composition(one,A),composition(converse(sk1),A)),
inference(paramod,[status(thm)],[c_160,c_10]) ).
cnf(c_9494,plain,
A = join(composition(one,A),composition(converse(sk1),A)),
inference(paramod,[status(thm)],[c_158,c_9493]) ).
cnf(c_9495,plain,
A = join(A,composition(converse(sk1),A)),
inference(paramod,[status(thm)],[c_158,c_9494]) ).
cnf(c_167,plain,
join(A,composition(converse(sk1),A)) = A,
inference(copy,[status(thm)],[c_9495]) ).
cnf(c_9496,plain,
join(complement(join(complement(A),B)),B) = join(A,complement(join(complement(B),complement(complement(A))))),
inference(paramod,[status(thm)],[c_32,c_34]) ).
cnf(c_9497,plain,
join(B,complement(join(complement(A),B))) = join(A,complement(join(complement(B),complement(complement(A))))),
inference(paramod,[status(thm)],[c_1,c_9496]) ).
cnf(c_188,plain,
join(A,complement(join(complement(B),A))) = join(B,complement(join(complement(A),B))),
inference(paramod,[status(thm)],[c_119,c_9497]) ).
cnf(c_9498,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_36,c_31]) ).
cnf(c_201,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_9498]) ).
cnf(c_9499,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_36,c_32]) ).
cnf(c_9500,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_119,c_9499]) ).
cnf(c_203,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_9500]) ).
cnf(c_9501,plain,
join(complement(join(complement(A),B)),complement(join(complement(join(complement(A),B)),join(complement(join(complement(join(complement(A),complement(B))),C)),complement(join(A,C)))))) = join(complement(join(complement(A),B)),join(complement(join(complement(A),complement(B))),C)),
inference(paramod,[status(thm)],[c_34,c_36]) ).
cnf(c_9502,plain,
join(complement(join(complement(A),B)),complement(join(complement(join(complement(A),B)),join(complement(join(A,C)),complement(join(complement(join(complement(A),complement(B))),C)))))) = join(complement(join(complement(A),B)),join(complement(join(complement(A),complement(B))),C)),
inference(paramod,[status(thm)],[c_1,c_9501]) ).
cnf(c_209,plain,
join(complement(join(complement(A),B)),complement(join(complement(join(complement(A),B)),join(complement(join(A,C)),complement(join(complement(join(complement(A),complement(B))),C)))))) = join(A,C),
inference(paramod,[status(thm)],[c_34,c_9502]) ).
cnf(c_9503,plain,
converse(A) = join(converse(A),converse(composition(sk1,A))),
inference(paramod,[status(thm)],[c_162,c_12]) ).
cnf(c_9504,plain,
converse(A) = join(converse(A),composition(converse(A),converse(sk1))),
inference(paramod,[status(thm)],[c_13,c_9503]) ).
cnf(c_227,plain,
join(converse(A),composition(converse(A),converse(sk1))) = converse(A),
inference(copy,[status(thm)],[c_9504]) ).
cnf(c_9505,plain,
join(complement(join(complement(A),A)),complement(complement(A))) = A,
inference(paramod,[status(thm)],[c_165,c_5]) ).
cnf(c_9506,plain,
join(complement(join(A,complement(A))),complement(complement(A))) = A,
inference(paramod,[status(thm)],[c_1,c_9505]) ).
cnf(c_9507,plain,
join(complement(top),complement(complement(A))) = A,
inference(paramod,[status(thm)],[c_17,c_9506]) ).
cnf(c_9508,plain,
join(zero,complement(complement(A))) = A,
inference(paramod,[status(thm)],[c_19,c_9507]) ).
cnf(c_239,plain,
join(zero,A) = A,
inference(paramod,[status(thm)],[c_119,c_9508]) ).
cnf(c_9509,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_165,c_34]) ).
cnf(c_9510,plain,
A = join(A,complement(join(complement(A),complement(B)))),
inference(paramod,[status(thm)],[c_5,c_9509]) ).
cnf(c_242,plain,
join(A,complement(join(complement(A),complement(B)))) = A,
inference(copy,[status(thm)],[c_9510]) ).
cnf(c_251,plain,
complement(join(A,A)) = complement(A),
inference(paramod,[status(thm)],[c_239,c_120]) ).
cnf(c_261,plain,
join(complement(A),complement(join(complement(A),B))) = join(complement(B),complement(A)),
inference(paramod,[status(thm)],[c_242,c_118]) ).
cnf(c_9511,plain,
join(complement(join(complement(join(A,C)),complement(join(complement(join(complement(A),complement(B))),C)))),complement(join(complement(A),B))) = join(A,C),
inference(paramod,[status(thm)],[c_261,c_209]) ).
cnf(c_263,plain,
join(complement(join(complement(A),B)),complement(join(complement(join(A,C)),complement(join(complement(join(complement(A),complement(B))),C))))) = join(A,C),
inference(paramod,[status(thm)],[c_1,c_9511]) ).
cnf(c_9512,plain,
join(complement(A),composition(converse(B),complement(composition(B,A)))) = join(complement(A),composition(sk1,composition(converse(B),complement(composition(B,A))))),
inference(paramod,[status(thm)],[c_162,c_42]) ).
cnf(c_9513,plain,
complement(A) = join(complement(A),composition(sk1,composition(converse(B),complement(composition(B,A))))),
inference(paramod,[status(thm)],[c_15,c_9512]) ).
cnf(c_320,plain,
join(complement(A),composition(sk1,composition(converse(B),complement(composition(B,A))))) = complement(A),
inference(copy,[status(thm)],[c_9513]) ).
cnf(c_9514,plain,
join(complement(join(complement(A),B)),complement(join(complement(join(A,A)),complement(B)))) = join(A,A),
inference(paramod,[status(thm)],[c_251,c_5]) ).
cnf(c_9515,plain,
join(complement(join(complement(A),B)),complement(join(complement(A),complement(B)))) = join(A,A),
inference(paramod,[status(thm)],[c_251,c_9514]) ).
cnf(c_9516,plain,
A = join(A,A),
inference(paramod,[status(thm)],[c_5,c_9515]) ).
cnf(c_334,plain,
join(A,A) = A,
inference(copy,[status(thm)],[c_9516]) ).
cnf(c_9517,plain,
join(join(A,B),B) = join(A,B),
inference(paramod,[status(thm)],[c_334,c_3]) ).
cnf(c_339,plain,
join(A,join(B,A)) = join(B,A),
inference(paramod,[status(thm)],[c_1,c_9517]) ).
cnf(c_9518,plain,
join(complement(join(complement(A),B)),join(complement(join(complement(A),complement(B))),A)) = A,
inference(paramod,[status(thm)],[c_334,c_34]) ).
cnf(c_9519,plain,
join(complement(join(complement(A),B)),join(A,complement(join(complement(A),complement(B))))) = A,
inference(paramod,[status(thm)],[c_1,c_9518]) ).
cnf(c_9520,plain,
join(complement(join(complement(A),B)),A) = A,
inference(paramod,[status(thm)],[c_242,c_9519]) ).
cnf(c_340,plain,
join(A,complement(join(complement(A),B))) = A,
inference(paramod,[status(thm)],[c_1,c_9520]) ).
cnf(c_9521,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_340,c_203]) ).
cnf(c_9522,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_9521]) ).
cnf(c_9523,plain,
join(complement(B),complement(A)) = join(complement(A),join(complement(B),complement(join(complement(A),B)))),
inference(paramod,[status(thm)],[c_261,c_9522]) ).
cnf(c_342,plain,
join(complement(A),join(complement(B),complement(join(complement(A),B)))) = join(complement(B),complement(A)),
inference(copy,[status(thm)],[c_9523]) ).
cnf(c_345,plain,
join(complement(A),join(B,complement(join(complement(C),complement(A))))) = join(B,join(complement(A),C)),
inference(paramod,[status(thm)],[c_342,c_201]) ).
cnf(c_9524,plain,
converse(A) = join(converse(A),converse(composition(converse(sk1),A))),
inference(paramod,[status(thm)],[c_167,c_12]) ).
cnf(c_9525,plain,
converse(A) = join(converse(A),composition(converse(A),converse(converse(sk1)))),
inference(paramod,[status(thm)],[c_13,c_9524]) ).
cnf(c_9526,plain,
converse(A) = join(converse(A),composition(converse(A),sk1)),
inference(paramod,[status(thm)],[c_11,c_9525]) ).
cnf(c_489,plain,
join(converse(A),composition(converse(A),sk1)) = converse(A),
inference(copy,[status(thm)],[c_9526]) ).
cnf(c_9527,plain,
join(A,complement(A)) = join(top,complement(A)),
inference(paramod,[status(thm)],[c_334,c_50]) ).
cnf(c_9528,plain,
top = join(top,complement(A)),
inference(paramod,[status(thm)],[c_17,c_9527]) ).
cnf(c_523,plain,
join(top,complement(A)) = top,
inference(copy,[status(thm)],[c_9528]) ).
cnf(c_9529,plain,
join(A,join(complement(A),top)) = top,
inference(paramod,[status(thm)],[c_334,c_50]) ).
cnf(c_9530,plain,
join(A,join(top,complement(A))) = top,
inference(paramod,[status(thm)],[c_1,c_9529]) ).
cnf(c_524,plain,
join(A,top) = top,
inference(paramod,[status(thm)],[c_523,c_9530]) ).
cnf(c_9531,plain,
top = join(top,A),
inference(paramod,[status(thm)],[c_524,c_1]) ).
cnf(c_558,plain,
join(top,A) = top,
inference(copy,[status(thm)],[c_9531]) ).
cnf(c_9532,plain,
converse(top) = join(converse(A),converse(top)),
inference(paramod,[status(thm)],[c_524,c_12]) ).
cnf(c_560,plain,
join(converse(A),converse(top)) = converse(top),
inference(copy,[status(thm)],[c_9532]) ).
cnf(c_580,plain,
join(A,converse(top)) = converse(top),
inference(paramod,[status(thm)],[c_11,c_560]) ).
cnf(c_583,plain,
converse(top) = top,
inference(paramod,[status(thm)],[c_580,c_558]) ).
cnf(c_594,plain,
join(converse(A),converse(complement(A))) = top,
inference(paramod,[status(thm)],[c_583,c_55]) ).
cnf(c_717,plain,
join(A,converse(complement(converse(A)))) = top,
inference(paramod,[status(thm)],[c_11,c_594]) ).
cnf(c_9533,plain,
join(one,top) = join(one,complement(sk1)),
inference(paramod,[status(thm)],[c_17,c_85]) ).
cnf(c_9534,plain,
top = join(one,complement(sk1)),
inference(paramod,[status(thm)],[c_524,c_9533]) ).
cnf(c_725,plain,
join(one,complement(sk1)) = top,
inference(copy,[status(thm)],[c_9534]) ).
cnf(c_9535,plain,
join(A,composition(converse(converse(A)),sk1)) = converse(converse(A)),
inference(paramod,[status(thm)],[c_11,c_489]) ).
cnf(c_9536,plain,
join(A,composition(A,sk1)) = converse(converse(A)),
inference(paramod,[status(thm)],[c_11,c_9535]) ).
cnf(c_886,plain,
join(A,composition(A,sk1)) = A,
inference(paramod,[status(thm)],[c_11,c_9536]) ).
cnf(c_9537,plain,
join(A,B) = join(A,join(composition(A,sk1),B)),
inference(paramod,[status(thm)],[c_886,c_3]) ).
cnf(c_890,plain,
join(A,join(composition(A,sk1),B)) = join(A,B),
inference(copy,[status(thm)],[c_9537]) ).
cnf(c_9538,plain,
join(complement(join(A,complement(B))),complement(join(B,complement(complement(A))))) = complement(A),
inference(paramod,[status(thm)],[c_119,c_94]) ).
cnf(c_929,plain,
join(complement(join(A,complement(B))),complement(join(B,A))) = complement(A),
inference(paramod,[status(thm)],[c_119,c_9538]) ).
cnf(c_9539,plain,
join(complement(join(complement(sk1),complement(one))),complement(top)) = sk1,
inference(paramod,[status(thm)],[c_725,c_94]) ).
cnf(c_9540,plain,
join(complement(join(complement(one),complement(sk1))),complement(top)) = sk1,
inference(paramod,[status(thm)],[c_1,c_9539]) ).
cnf(c_9541,plain,
join(complement(join(complement(one),complement(sk1))),zero) = sk1,
inference(paramod,[status(thm)],[c_19,c_9540]) ).
cnf(c_9542,plain,
join(zero,complement(join(complement(one),complement(sk1)))) = sk1,
inference(paramod,[status(thm)],[c_1,c_9541]) ).
cnf(c_930,plain,
complement(join(complement(one),complement(sk1))) = sk1,
inference(paramod,[status(thm)],[c_239,c_9542]) ).
cnf(c_9543,plain,
join(complement(join(A,complement(B))),B) = join(complement(join(complement(B),complement(A))),complement(join(A,complement(B)))),
inference(paramod,[status(thm)],[c_94,c_339]) ).
cnf(c_9544,plain,
join(B,complement(join(A,complement(B)))) = join(complement(join(complement(B),complement(A))),complement(join(A,complement(B)))),
inference(paramod,[status(thm)],[c_1,c_9543]) ).
cnf(c_9545,plain,
join(B,complement(join(A,complement(B)))) = complement(complement(B)),
inference(paramod,[status(thm)],[c_929,c_9544]) ).
cnf(c_931,plain,
join(A,complement(join(B,complement(A)))) = A,
inference(paramod,[status(thm)],[c_119,c_9545]) ).
cnf(c_9546,plain,
complement(sk1) = join(complement(one),complement(sk1)),
inference(paramod,[status(thm)],[c_930,c_119]) ).
cnf(c_964,plain,
join(complement(one),complement(sk1)) = complement(sk1),
inference(copy,[status(thm)],[c_9546]) ).
cnf(c_9547,plain,
join(complement(sk1),A) = join(complement(one),join(complement(sk1),A)),
inference(paramod,[status(thm)],[c_964,c_3]) ).
cnf(c_970,plain,
join(complement(one),join(complement(sk1),A)) = join(complement(sk1),A),
inference(copy,[status(thm)],[c_9547]) ).
cnf(c_9548,plain,
join(A,composition(converse(converse(A)),converse(sk1))) = converse(converse(A)),
inference(paramod,[status(thm)],[c_11,c_227]) ).
cnf(c_9549,plain,
join(A,composition(A,converse(sk1))) = converse(converse(A)),
inference(paramod,[status(thm)],[c_11,c_9548]) ).
cnf(c_1148,plain,
join(A,composition(A,converse(sk1))) = A,
inference(paramod,[status(thm)],[c_11,c_9549]) ).
cnf(c_9550,plain,
join(complement(A),join(composition(converse(B),complement(composition(B,A))),complement(join(complement(complement(A)),C)))) = complement(A),
inference(paramod,[status(thm)],[c_340,c_42]) ).
cnf(c_9551,plain,
join(complement(A),join(composition(converse(B),complement(composition(B,A))),complement(join(A,C)))) = complement(A),
inference(paramod,[status(thm)],[c_119,c_9550]) ).
cnf(c_1387,plain,
join(complement(A),complement(join(A,B))) = complement(A),
inference(paramod,[status(thm)],[c_42,c_9551]) ).
cnf(c_1400,plain,
join(complement(A),complement(join(B,A))) = complement(A),
inference(paramod,[status(thm)],[c_1,c_1387]) ).
cnf(c_9552,plain,
join(complement(composition(A,sk1)),complement(A)) = complement(composition(A,sk1)),
inference(paramod,[status(thm)],[c_886,c_1400]) ).
cnf(c_1437,plain,
join(complement(A),complement(composition(A,sk1))) = complement(composition(A,sk1)),
inference(paramod,[status(thm)],[c_1,c_9552]) ).
cnf(c_9553,plain,
join(complement(composition(A,converse(sk1))),complement(A)) = complement(composition(A,converse(sk1))),
inference(paramod,[status(thm)],[c_1148,c_1400]) ).
cnf(c_1439,plain,
join(complement(A),complement(composition(A,converse(sk1)))) = complement(composition(A,converse(sk1))),
inference(paramod,[status(thm)],[c_1,c_9553]) ).
cnf(c_9554,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_964,c_161]) ).
cnf(c_9555,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_119,c_9554]) ).
cnf(c_9556,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_964,c_9555]) ).
cnf(c_9557,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_119,c_9556]) ).
cnf(c_9558,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_139,c_9557]) ).
cnf(c_9559,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_158,c_9558]) ).
cnf(c_9560,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_964,c_9559]) ).
cnf(c_9561,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_119,c_9560]) ).
cnf(c_9562,plain,
sk1 = composition(complement(join(complement(one),complement(sk1))),complement(join(complement(one),complement(composition(converse(one),sk1))))),
inference(paramod,[status(thm)],[c_886,c_9561]) ).
cnf(c_9563,plain,
sk1 = composition(complement(complement(sk1)),complement(join(complement(one),complement(composition(converse(one),sk1))))),
inference(paramod,[status(thm)],[c_964,c_9562]) ).
cnf(c_9564,plain,
sk1 = composition(sk1,complement(join(complement(one),complement(composition(converse(one),sk1))))),
inference(paramod,[status(thm)],[c_119,c_9563]) ).
cnf(c_9565,plain,
sk1 = composition(sk1,complement(join(complement(one),complement(composition(one,sk1))))),
inference(paramod,[status(thm)],[c_139,c_9564]) ).
cnf(c_9566,plain,
sk1 = composition(sk1,complement(join(complement(one),complement(sk1)))),
inference(paramod,[status(thm)],[c_158,c_9565]) ).
cnf(c_9567,plain,
sk1 = composition(sk1,complement(complement(sk1))),
inference(paramod,[status(thm)],[c_964,c_9566]) ).
cnf(c_9568,plain,
sk1 = composition(sk1,sk1),
inference(paramod,[status(thm)],[c_119,c_9567]) ).
cnf(c_1464,plain,
composition(sk1,sk1) = sk1,
inference(copy,[status(thm)],[c_9568]) ).
cnf(c_9569,plain,
join(complement(join(complement(one),complement(sk1))),complement(join(complement(one),complement(composition(sk1,complement(join(complement(sk1),complement(converse(sk1))))))))) = complement(join(complement(one),complement(composition(sk1,complement(join(complement(sk1),complement(converse(sk1)))))))),
inference(paramod,[status(thm)],[c_1464,c_75]) ).
cnf(c_9570,plain,
join(complement(complement(sk1)),complement(join(complement(one),complement(composition(sk1,complement(join(complement(sk1),complement(converse(sk1))))))))) = complement(join(complement(one),complement(composition(sk1,complement(join(complement(sk1),complement(converse(sk1)))))))),
inference(paramod,[status(thm)],[c_964,c_9569]) ).
cnf(c_1514,plain,
join(sk1,complement(join(complement(one),complement(composition(sk1,complement(join(complement(sk1),complement(converse(sk1))))))))) = complement(join(complement(one),complement(composition(sk1,complement(join(complement(sk1),complement(converse(sk1)))))))),
inference(paramod,[status(thm)],[c_119,c_9570]) ).
cnf(c_9571,plain,
join(complement(join(complement(converse(sk1)),complement(sk1))),complement(join(complement(sk1),complement(composition(complement(join(complement(one),complement(sk1))),converse(sk1)))))) = complement(join(complement(sk1),complement(composition(complement(join(complement(one),complement(composition(sk1,sk1)))),converse(sk1))))),
inference(paramod,[status(thm)],[c_1464,c_155]) ).
cnf(c_9572,plain,
join(complement(join(complement(sk1),complement(converse(sk1)))),complement(join(complement(sk1),complement(composition(complement(join(complement(one),complement(sk1))),converse(sk1)))))) = complement(join(complement(sk1),complement(composition(complement(join(complement(one),complement(composition(sk1,sk1)))),converse(sk1))))),
inference(paramod,[status(thm)],[c_1,c_9571]) ).
cnf(c_9573,plain,
join(complement(join(complement(sk1),complement(converse(sk1)))),complement(join(complement(sk1),complement(composition(complement(complement(sk1)),converse(sk1)))))) = complement(join(complement(sk1),complement(composition(complement(join(complement(one),complement(composition(sk1,sk1)))),converse(sk1))))),
inference(paramod,[status(thm)],[c_964,c_9572]) ).
cnf(c_9574,plain,
join(complement(join(complement(sk1),complement(converse(sk1)))),complement(join(complement(sk1),complement(composition(sk1,converse(sk1)))))) = complement(join(complement(sk1),complement(composition(complement(join(complement(one),complement(composition(sk1,sk1)))),converse(sk1))))),
inference(paramod,[status(thm)],[c_119,c_9573]) ).
cnf(c_9575,plain,
join(complement(join(complement(sk1),complement(converse(sk1)))),complement(complement(composition(sk1,converse(sk1))))) = complement(join(complement(sk1),complement(composition(complement(join(complement(one),complement(composition(sk1,sk1)))),converse(sk1))))),
inference(paramod,[status(thm)],[c_1439,c_9574]) ).
cnf(c_9576,plain,
join(complement(join(complement(sk1),complement(converse(sk1)))),composition(sk1,converse(sk1))) = complement(join(complement(sk1),complement(composition(complement(join(complement(one),complement(composition(sk1,sk1)))),converse(sk1))))),
inference(paramod,[status(thm)],[c_119,c_9575]) ).
cnf(c_9577,plain,
join(complement(join(complement(sk1),complement(converse(sk1)))),composition(sk1,converse(sk1))) = complement(join(complement(sk1),complement(composition(complement(join(complement(one),complement(sk1))),converse(sk1))))),
inference(paramod,[status(thm)],[c_1464,c_9576]) ).
cnf(c_9578,plain,
join(complement(join(complement(sk1),complement(converse(sk1)))),composition(sk1,converse(sk1))) = complement(join(complement(sk1),complement(composition(complement(complement(sk1)),converse(sk1))))),
inference(paramod,[status(thm)],[c_964,c_9577]) ).
cnf(c_9579,plain,
join(complement(join(complement(sk1),complement(converse(sk1)))),composition(sk1,converse(sk1))) = complement(join(complement(sk1),complement(composition(sk1,converse(sk1))))),
inference(paramod,[status(thm)],[c_119,c_9578]) ).
cnf(c_9580,plain,
join(complement(join(complement(sk1),complement(converse(sk1)))),composition(sk1,converse(sk1))) = complement(complement(composition(sk1,converse(sk1)))),
inference(paramod,[status(thm)],[c_1439,c_9579]) ).
cnf(c_1518,plain,
join(complement(join(complement(sk1),complement(converse(sk1)))),composition(sk1,converse(sk1))) = composition(sk1,converse(sk1)),
inference(paramod,[status(thm)],[c_119,c_9580]) ).
cnf(c_9581,plain,
join(complement(join(complement(converse(sk1)),complement(sk1))),composition(complement(join(complement(one),complement(sk1))),complement(join(complement(converse(sk1)),complement(sk1))))) = composition(complement(join(complement(one),complement(composition(sk1,sk1)))),complement(join(complement(converse(sk1)),complement(sk1)))),
inference(paramod,[status(thm)],[c_1464,c_164]) ).
cnf(c_9582,plain,
join(complement(join(complement(sk1),complement(converse(sk1)))),composition(complement(join(complement(one),complement(sk1))),complement(join(complement(converse(sk1)),complement(sk1))))) = composition(complement(join(complement(one),complement(composition(sk1,sk1)))),complement(join(complement(converse(sk1)),complement(sk1)))),
inference(paramod,[status(thm)],[c_1,c_9581]) ).
cnf(c_9583,plain,
join(complement(join(complement(sk1),complement(converse(sk1)))),composition(complement(complement(sk1)),complement(join(complement(converse(sk1)),complement(sk1))))) = composition(complement(join(complement(one),complement(composition(sk1,sk1)))),complement(join(complement(converse(sk1)),complement(sk1)))),
inference(paramod,[status(thm)],[c_964,c_9582]) ).
cnf(c_9584,plain,
join(complement(join(complement(sk1),complement(converse(sk1)))),composition(sk1,complement(join(complement(converse(sk1)),complement(sk1))))) = composition(complement(join(complement(one),complement(composition(sk1,sk1)))),complement(join(complement(converse(sk1)),complement(sk1)))),
inference(paramod,[status(thm)],[c_119,c_9583]) ).
cnf(c_9585,plain,
join(complement(join(complement(sk1),complement(converse(sk1)))),composition(sk1,complement(join(complement(sk1),complement(converse(sk1)))))) = composition(complement(join(complement(one),complement(composition(sk1,sk1)))),complement(join(complement(converse(sk1)),complement(sk1)))),
inference(paramod,[status(thm)],[c_1,c_9584]) ).
cnf(c_9586,plain,
complement(join(complement(sk1),complement(converse(sk1)))) = composition(complement(join(complement(one),complement(composition(sk1,sk1)))),complement(join(complement(converse(sk1)),complement(sk1)))),
inference(paramod,[status(thm)],[c_162,c_9585]) ).
cnf(c_9587,plain,
complement(join(complement(sk1),complement(converse(sk1)))) = composition(complement(join(complement(one),complement(sk1))),complement(join(complement(converse(sk1)),complement(sk1)))),
inference(paramod,[status(thm)],[c_1464,c_9586]) ).
cnf(c_9588,plain,
complement(join(complement(sk1),complement(converse(sk1)))) = composition(complement(complement(sk1)),complement(join(complement(converse(sk1)),complement(sk1)))),
inference(paramod,[status(thm)],[c_964,c_9587]) ).
cnf(c_9589,plain,
complement(join(complement(sk1),complement(converse(sk1)))) = composition(sk1,complement(join(complement(converse(sk1)),complement(sk1)))),
inference(paramod,[status(thm)],[c_119,c_9588]) ).
cnf(c_9590,plain,
complement(join(complement(sk1),complement(converse(sk1)))) = composition(sk1,complement(join(complement(sk1),complement(converse(sk1))))),
inference(paramod,[status(thm)],[c_1,c_9589]) ).
cnf(c_1520,plain,
composition(sk1,complement(join(complement(sk1),complement(converse(sk1))))) = complement(join(complement(sk1),complement(converse(sk1)))),
inference(copy,[status(thm)],[c_9590]) ).
cnf(c_9591,plain,
join(sk1,complement(join(complement(one),complement(complement(join(complement(sk1),complement(converse(sk1)))))))) = complement(join(complement(one),complement(composition(sk1,complement(join(complement(sk1),complement(converse(sk1)))))))),
inference(paramod,[status(thm)],[c_1520,c_1514]) ).
cnf(c_9592,plain,
join(sk1,complement(join(complement(one),join(complement(sk1),complement(converse(sk1)))))) = complement(join(complement(one),complement(composition(sk1,complement(join(complement(sk1),complement(converse(sk1)))))))),
inference(paramod,[status(thm)],[c_119,c_9591]) ).
cnf(c_9593,plain,
join(sk1,complement(join(complement(sk1),complement(converse(sk1))))) = complement(join(complement(one),complement(composition(sk1,complement(join(complement(sk1),complement(converse(sk1)))))))),
inference(paramod,[status(thm)],[c_970,c_9592]) ).
cnf(c_9594,plain,
sk1 = complement(join(complement(one),complement(composition(sk1,complement(join(complement(sk1),complement(converse(sk1)))))))),
inference(paramod,[status(thm)],[c_340,c_9593]) ).
cnf(c_9595,plain,
sk1 = complement(join(complement(one),complement(complement(join(complement(sk1),complement(converse(sk1))))))),
inference(paramod,[status(thm)],[c_1520,c_9594]) ).
cnf(c_9596,plain,
sk1 = complement(join(complement(one),join(complement(sk1),complement(converse(sk1))))),
inference(paramod,[status(thm)],[c_119,c_9595]) ).
cnf(c_9597,plain,
sk1 = complement(join(complement(sk1),complement(converse(sk1)))),
inference(paramod,[status(thm)],[c_970,c_9596]) ).
cnf(c_1521,plain,
complement(join(complement(sk1),complement(converse(sk1)))) = sk1,
inference(copy,[status(thm)],[c_9597]) ).
cnf(c_9598,plain,
join(sk1,composition(sk1,converse(sk1))) = composition(sk1,converse(sk1)),
inference(paramod,[status(thm)],[c_1521,c_1518]) ).
cnf(c_9599,plain,
sk1 = composition(sk1,converse(sk1)),
inference(paramod,[status(thm)],[c_1148,c_9598]) ).
cnf(c_1522,plain,
composition(sk1,converse(sk1)) = sk1,
inference(copy,[status(thm)],[c_9599]) ).
cnf(c_9600,plain,
converse(sk1) = composition(converse(converse(sk1)),converse(sk1)),
inference(paramod,[status(thm)],[c_1522,c_13]) ).
cnf(c_9601,plain,
converse(sk1) = composition(sk1,converse(sk1)),
inference(paramod,[status(thm)],[c_11,c_9600]) ).
cnf(c_1524,plain,
converse(sk1) = sk1,
inference(paramod,[status(thm)],[c_1522,c_9601]) ).
cnf(c_9602,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_188,c_42]) ).
cnf(c_9603,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_345,c_9602]) ).
cnf(c_9604,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_31,c_9603]) ).
cnf(c_9605,plain,
join(complement(A),C) = join(C,complement(join(complement(complement(A)),C))),
inference(paramod,[status(thm)],[c_42,c_9604]) ).
cnf(c_9606,plain,
join(complement(A),C) = join(C,complement(join(A,C))),
inference(paramod,[status(thm)],[c_119,c_9605]) ).
cnf(c_1985,plain,
join(A,complement(join(B,A))) = join(complement(B),A),
inference(copy,[status(thm)],[c_9606]) ).
cnf(c_2104,plain,
join(A,complement(join(A,B))) = join(complement(B),A),
inference(paramod,[status(thm)],[c_1,c_1985]) ).
cnf(c_9607,plain,
join(converse(complement(A)),complement(top)) = join(complement(converse(A)),converse(complement(A))),
inference(paramod,[status(thm)],[c_594,c_1985]) ).
cnf(c_9608,plain,
join(converse(complement(A)),zero) = join(complement(converse(A)),converse(complement(A))),
inference(paramod,[status(thm)],[c_19,c_9607]) ).
cnf(c_9609,plain,
join(zero,converse(complement(A))) = join(complement(converse(A)),converse(complement(A))),
inference(paramod,[status(thm)],[c_1,c_9608]) ).
cnf(c_9610,plain,
converse(complement(A)) = join(complement(converse(A)),converse(complement(A))),
inference(paramod,[status(thm)],[c_239,c_9609]) ).
cnf(c_2115,plain,
join(complement(converse(A)),converse(complement(A))) = converse(complement(A)),
inference(copy,[status(thm)],[c_9610]) ).
cnf(c_9611,plain,
join(converse(complement(converse(A))),complement(top)) = join(complement(A),converse(complement(converse(A)))),
inference(paramod,[status(thm)],[c_717,c_1985]) ).
cnf(c_9612,plain,
join(converse(complement(converse(A))),zero) = join(complement(A),converse(complement(converse(A)))),
inference(paramod,[status(thm)],[c_19,c_9611]) ).
cnf(c_9613,plain,
join(zero,converse(complement(converse(A)))) = join(complement(A),converse(complement(converse(A)))),
inference(paramod,[status(thm)],[c_1,c_9612]) ).
cnf(c_9614,plain,
converse(complement(converse(A))) = join(complement(A),converse(complement(converse(A)))),
inference(paramod,[status(thm)],[c_239,c_9613]) ).
cnf(c_2131,plain,
join(complement(A),converse(complement(converse(A)))) = converse(complement(converse(A))),
inference(copy,[status(thm)],[c_9614]) ).
cnf(c_9615,plain,
join(composition(A,B),complement(composition(top,B))) = join(complement(composition(complement(A),B)),composition(A,B)),
inference(paramod,[status(thm)],[c_54,c_2104]) ).
cnf(c_9616,plain,
join(composition(A,B),complement(composition(top,B))) = join(composition(A,B),complement(composition(complement(A),B))),
inference(paramod,[status(thm)],[c_1,c_9615]) ).
cnf(c_2443,plain,
join(composition(A,B),complement(composition(complement(A),B))) = join(composition(A,B),complement(composition(top,B))),
inference(copy,[status(thm)],[c_9616]) ).
cnf(c_9617,plain,
converse(converse(complement(A))) = join(converse(complement(converse(A))),converse(converse(complement(A)))),
inference(paramod,[status(thm)],[c_2115,c_12]) ).
cnf(c_9618,plain,
complement(A) = join(converse(complement(converse(A))),converse(converse(complement(A)))),
inference(paramod,[status(thm)],[c_11,c_9617]) ).
cnf(c_9619,plain,
complement(A) = join(converse(complement(converse(A))),complement(A)),
inference(paramod,[status(thm)],[c_11,c_9618]) ).
cnf(c_9620,plain,
complement(A) = join(complement(A),converse(complement(converse(A)))),
inference(paramod,[status(thm)],[c_1,c_9619]) ).
cnf(c_9621,plain,
complement(A) = converse(complement(converse(A))),
inference(paramod,[status(thm)],[c_2131,c_9620]) ).
cnf(c_2474,plain,
converse(complement(converse(A))) = complement(A),
inference(copy,[status(thm)],[c_9621]) ).
cnf(c_2482,plain,
converse(complement(A)) = complement(converse(A)),
inference(paramod,[status(thm)],[c_2474,c_11]) ).
cnf(c_9622,plain,
join(complement(join(complement(complement(A)),B)),complement(join(complement(complement(composition(A,sk1))),complement(join(complement(join(complement(complement(A)),complement(B))),complement(composition(A,sk1))))))) = join(complement(A),complement(composition(A,sk1))),
inference(paramod,[status(thm)],[c_1437,c_263]) ).
cnf(c_9623,plain,
join(complement(join(A,B)),complement(join(complement(complement(composition(A,sk1))),complement(join(complement(join(complement(complement(A)),complement(B))),complement(composition(A,sk1))))))) = join(complement(A),complement(composition(A,sk1))),
inference(paramod,[status(thm)],[c_119,c_9622]) ).
cnf(c_9624,plain,
join(complement(join(A,B)),complement(join(composition(A,sk1),complement(join(complement(join(complement(complement(A)),complement(B))),complement(composition(A,sk1))))))) = join(complement(A),complement(composition(A,sk1))),
inference(paramod,[status(thm)],[c_119,c_9623]) ).
cnf(c_9625,plain,
join(complement(join(A,B)),complement(join(composition(A,sk1),complement(join(complement(join(A,complement(B))),complement(composition(A,sk1))))))) = join(complement(A),complement(composition(A,sk1))),
inference(paramod,[status(thm)],[c_119,c_9624]) ).
cnf(c_9626,plain,
join(complement(join(A,B)),complement(composition(A,sk1))) = join(complement(A),complement(composition(A,sk1))),
inference(paramod,[status(thm)],[c_931,c_9625]) ).
cnf(c_3143,plain,
join(complement(join(A,B)),complement(composition(A,sk1))) = complement(composition(A,sk1)),
inference(paramod,[status(thm)],[c_1437,c_9626]) ).
cnf(c_9627,plain,
join(complement(complement(composition(A,sk1))),complement(composition(complement(A),sk1))) = complement(composition(complement(A),sk1)),
inference(paramod,[status(thm)],[c_1437,c_3143]) ).
cnf(c_9628,plain,
join(composition(A,sk1),complement(composition(complement(A),sk1))) = complement(composition(complement(A),sk1)),
inference(paramod,[status(thm)],[c_119,c_9627]) ).
cnf(c_9629,plain,
join(composition(A,sk1),complement(composition(top,sk1))) = complement(composition(complement(A),sk1)),
inference(paramod,[status(thm)],[c_2443,c_9628]) ).
cnf(c_4292,plain,
complement(composition(complement(A),sk1)) = join(composition(A,sk1),complement(composition(top,sk1))),
inference(copy,[status(thm)],[c_9629]) ).
cnf(c_9630,plain,
join(complement(complement(A)),complement(composition(complement(A),sk1))) = complement(composition(complement(A),sk1)),
inference(paramod,[status(thm)],[c_320,c_3143]) ).
cnf(c_9631,plain,
join(A,complement(composition(complement(A),sk1))) = complement(composition(complement(A),sk1)),
inference(paramod,[status(thm)],[c_119,c_9630]) ).
cnf(c_9632,plain,
join(A,join(composition(A,sk1),complement(composition(top,sk1)))) = complement(composition(complement(A),sk1)),
inference(paramod,[status(thm)],[c_4292,c_9631]) ).
cnf(c_9633,plain,
join(A,complement(composition(top,sk1))) = complement(composition(complement(A),sk1)),
inference(paramod,[status(thm)],[c_890,c_9632]) ).
cnf(c_9634,plain,
join(A,complement(composition(top,sk1))) = join(composition(A,sk1),complement(composition(top,sk1))),
inference(paramod,[status(thm)],[c_4292,c_9633]) ).
cnf(c_4316,plain,
join(composition(A,sk1),complement(composition(top,sk1))) = join(A,complement(composition(top,sk1))),
inference(copy,[status(thm)],[c_9634]) ).
cnf(c_4336,plain,
complement(composition(complement(A),sk1)) = join(A,complement(composition(top,sk1))),
inference(paramod,[status(thm)],[c_4316,c_4292]) ).
cnf(c_4410,plain,
complement(composition(A,sk1)) = join(complement(A),complement(composition(top,sk1))),
inference(paramod,[status(thm)],[c_119,c_4336]) ).
cnf(c_9635,plain,
converse(complement(composition(A,sk1))) = join(converse(complement(A)),converse(complement(composition(top,sk1)))),
inference(paramod,[status(thm)],[c_4410,c_12]) ).
cnf(c_9636,plain,
complement(converse(composition(A,sk1))) = join(converse(complement(A)),converse(complement(composition(top,sk1)))),
inference(paramod,[status(thm)],[c_2482,c_9635]) ).
cnf(c_9637,plain,
complement(composition(converse(sk1),converse(A))) = join(converse(complement(A)),converse(complement(composition(top,sk1)))),
inference(paramod,[status(thm)],[c_13,c_9636]) ).
cnf(c_9638,plain,
complement(composition(sk1,converse(A))) = join(converse(complement(A)),converse(complement(composition(top,sk1)))),
inference(paramod,[status(thm)],[c_1524,c_9637]) ).
cnf(c_9639,plain,
complement(composition(sk1,converse(A))) = join(complement(converse(A)),converse(complement(composition(top,sk1)))),
inference(paramod,[status(thm)],[c_2482,c_9638]) ).
cnf(c_9640,plain,
complement(composition(sk1,converse(A))) = join(complement(converse(A)),complement(converse(composition(top,sk1)))),
inference(paramod,[status(thm)],[c_2482,c_9639]) ).
cnf(c_9641,plain,
complement(composition(sk1,converse(A))) = join(complement(converse(A)),complement(composition(converse(sk1),converse(top)))),
inference(paramod,[status(thm)],[c_13,c_9640]) ).
cnf(c_9642,plain,
complement(composition(sk1,converse(A))) = join(complement(converse(A)),complement(composition(sk1,converse(top)))),
inference(paramod,[status(thm)],[c_1524,c_9641]) ).
cnf(c_9643,plain,
complement(composition(sk1,converse(A))) = join(complement(converse(A)),complement(composition(sk1,top))),
inference(paramod,[status(thm)],[c_583,c_9642]) ).
cnf(c_4462,plain,
complement(composition(sk1,converse(A))) = join(complement(composition(sk1,top)),complement(converse(A))),
inference(paramod,[status(thm)],[c_1,c_9643]) ).
cnf(c_9644,plain,
complement(composition(sk1,A)) = join(complement(composition(sk1,top)),complement(converse(converse(A)))),
inference(paramod,[status(thm)],[c_11,c_4462]) ).
cnf(c_5348,plain,
complement(composition(sk1,A)) = join(complement(composition(sk1,top)),complement(A)),
inference(paramod,[status(thm)],[c_11,c_9644]) ).
cnf(c_9645,plain,
complement(join(join(complement(composition(sk1,top)),complement(sk2)),composition(sk1,sk3))) != complement(join(sk3,complement(composition(sk1,sk2)))),
inference(paramod,[status(thm)],[c_5348,c_123]) ).
cnf(c_9646,plain,
complement(join(join(complement(sk2),complement(composition(sk1,top))),composition(sk1,sk3))) != complement(join(sk3,complement(composition(sk1,sk2)))),
inference(paramod,[status(thm)],[c_1,c_9645]) ).
cnf(c_5405,plain,
complement(join(complement(sk2),join(complement(composition(sk1,top)),composition(sk1,sk3)))) != complement(join(sk3,complement(composition(sk1,sk2)))),
inference(paramod,[status(thm)],[c_3,c_9646]) ).
cnf(c_9647,plain,
join(complement(composition(sk1,top)),complement(complement(composition(sk1,A)))) = join(complement(complement(A)),complement(composition(sk1,top))),
inference(paramod,[status(thm)],[c_5348,c_2104]) ).
cnf(c_9648,plain,
join(complement(composition(sk1,top)),composition(sk1,A)) = join(complement(complement(A)),complement(composition(sk1,top))),
inference(paramod,[status(thm)],[c_119,c_9647]) ).
cnf(c_5471,plain,
join(complement(composition(sk1,top)),composition(sk1,A)) = join(A,complement(composition(sk1,top))),
inference(paramod,[status(thm)],[c_119,c_9648]) ).
cnf(c_9649,plain,
complement(join(complement(sk2),join(complement(composition(sk1,top)),composition(sk1,sk3)))) != complement(join(sk3,join(complement(composition(sk1,top)),complement(sk2)))),
inference(paramod,[status(thm)],[c_5348,c_5405]) ).
cnf(c_5642,plain,
complement(join(complement(sk2),join(complement(composition(sk1,top)),composition(sk1,sk3)))) != complement(join(sk3,join(complement(sk2),complement(composition(sk1,top))))),
inference(paramod,[status(thm)],[c_1,c_9649]) ).
cnf(c_9650,plain,
complement(join(complement(sk2),join(sk3,complement(composition(sk1,top))))) != complement(join(sk3,join(complement(sk2),complement(composition(sk1,top))))),
inference(paramod,[status(thm)],[c_5471,c_5642]) ).
cnf(c_9651,plain,
complement(join(sk3,join(complement(sk2),complement(composition(sk1,top))))) != complement(join(sk3,join(complement(sk2),complement(composition(sk1,top))))),
inference(paramod,[status(thm)],[c_31,c_9650]) ).
cnf(c_9430,plain,
$false,
inference(copy,[status(thm)],[c_9651]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : REL030-3 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.37 % Computer : n011.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Sat Sep 26 05:34:44 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.10/0.37 % Process 3888968 was started by sandbox on n011,
% 0.10/0.37 % Sat Sep 26 05:34:44 2026
% 0.10/0.37 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.10/0.38
% 0.10/0.38 % From the command line: assign(max_seconds, 300).
% 34.44/5.00
% 34.44/5.00 % SZS status Unsatisfiable for theBenchmark
% 34.44/5.00
% 34.44/5.00 % Proof 1 at 3.90 (+ 0.69) seconds.
% 34.44/5.00 % Length of proof is 126.
% 34.44/5.00 % Level of proof is 23.
% 34.44/5.00 % Maximum clause weight is 97.000.
% 34.44/5.00 % Given clauses 458.
% 34.44/5.00
% 34.44/5.00 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------