%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : REL027-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 : n008.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:56 AM UTC 2026
% Result : Unsatisfiable 13.51s 2.42s
% Output : CNFRefutation 13.51s
% Verified :
% SZS Type : Refutation
% Derivation depth : 128
% Number of leaves : 16
% Syntax : Number of formulae : 382 ( 353 unt; 0 def)
% Number of atoms : 411 ( 410 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 88 ( 59 ~; 29 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 1 avg)
% Maximal term depth : 9 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 4 con; 0-2 aty)
% Number of variables : 425 ( 34 sgn 28 !; 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_3327,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_3327]) ).
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]) ).
cnf(c_11,plain,
join(composition(A,B),composition(C,B)) = composition(join(A,C),B),
inference(copy,[status(thm)],[c_10]) ).
fof(converse_idempotence_8,axiom,
! [VAR_0] : converse(converse(VAR_0)) = VAR_0,
file('theBenchmark.p',converse_idempotence_8) ).
cnf(c_12,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_13,plain,
converse(join(A,B)) = join(converse(A),converse(B)),
inference(clausify,[status(thm)],[converse_additivity_9]) ).
cnf(c_14,plain,
join(converse(A),converse(B)) = converse(join(A,B)),
inference(copy,[status(thm)],[c_13]) ).
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_15,plain,
converse(composition(A,B)) = composition(converse(B),converse(A)),
inference(clausify,[status(thm)],[converse_multiplicativity_10]) ).
cnf(c_16,plain,
composition(converse(A),converse(B)) = converse(composition(B,A)),
inference(copy,[status(thm)],[c_15]) ).
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_17,plain,
join(composition(converse(A),complement(composition(A,B))),complement(B)) = complement(B),
inference(clausify,[status(thm)],[converse_cancellativity_11]) ).
cnf(c_18,plain,
join(complement(A),composition(converse(B),complement(composition(B,A)))) = complement(A),
inference(paramod,[status(thm)],[c_1,c_17]) ).
fof(def_top_12,axiom,
! [VAR_0] : top = join(VAR_0,complement(VAR_0)),
file('theBenchmark.p',def_top_12) ).
cnf(c_19,plain,
top = join(A,complement(A)),
inference(clausify,[status(thm)],[def_top_12]) ).
cnf(c_20,plain,
join(A,complement(A)) = top,
inference(copy,[status(thm)],[c_19]) ).
fof(def_zero_13,axiom,
! [VAR_0] : zero = meet(VAR_0,complement(VAR_0)),
file('theBenchmark.p',def_zero_13) ).
cnf(c_21,plain,
zero = meet(A,complement(A)),
inference(clausify,[status(thm)],[def_zero_13]) ).
cnf(c_3328,plain,
zero = complement(join(complement(A),complement(complement(A)))),
inference(paramod,[status(thm)],[c_6,c_21]) ).
cnf(c_3329,plain,
zero = complement(top),
inference(paramod,[status(thm)],[c_20,c_3328]) ).
cnf(c_22,plain,
complement(top) = zero,
inference(copy,[status(thm)],[c_3329]) ).
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_23,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_3330,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_23]) ).
cnf(c_3331,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_3330]) ).
cnf(c_3332,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_3331]) ).
cnf(c_3333,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_3332]) ).
cnf(c_24,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_3333]) ).
fof(goals_17,axiom,
join(sk1,one) = one,
file('theBenchmark.p',goals_17) ).
cnf(c_29,plain,
join(sk1,one) = one,
inference(clausify,[status(thm)],[goals_17]) ).
cnf(c_30,plain,
join(one,sk1) = one,
inference(paramod,[status(thm)],[c_1,c_29]) ).
fof(goals_18,axiom,
( join(meet(complement(composition(sk1,top)),one),meet(complement(sk1),one)) != meet(complement(sk1),one)
| join(meet(complement(sk1),one),meet(complement(composition(sk1,top)),one)) != meet(complement(composition(sk1,top)),one) ),
file('theBenchmark.p',goals_18) ).
cnf(c_31,plain,
( join(meet(complement(composition(sk1,top)),one),meet(complement(sk1),one)) != meet(complement(sk1),one)
| join(meet(complement(sk1),one),meet(complement(composition(sk1,top)),one)) != meet(complement(composition(sk1,top)),one) ),
inference(clausify,[status(thm)],[goals_18]) ).
cnf(c_3334,plain,
( join(meet(complement(composition(sk1,top)),one),meet(complement(sk1),one)) != meet(complement(sk1),one)
| join(complement(join(complement(complement(sk1)),complement(one))),meet(complement(composition(sk1,top)),one)) != meet(complement(composition(sk1,top)),one) ),
inference(paramod,[status(thm)],[c_6,c_31]) ).
cnf(c_3335,plain,
( join(meet(complement(composition(sk1,top)),one),meet(complement(sk1),one)) != meet(complement(sk1),one)
| join(complement(join(complement(one),complement(complement(sk1)))),meet(complement(composition(sk1,top)),one)) != meet(complement(composition(sk1,top)),one) ),
inference(paramod,[status(thm)],[c_1,c_3334]) ).
cnf(c_3336,plain,
( join(meet(complement(composition(sk1,top)),one),meet(complement(sk1),one)) != meet(complement(sk1),one)
| join(complement(join(complement(one),complement(complement(sk1)))),complement(join(complement(complement(composition(sk1,top))),complement(one)))) != meet(complement(composition(sk1,top)),one) ),
inference(paramod,[status(thm)],[c_6,c_3335]) ).
cnf(c_3337,plain,
( join(meet(complement(composition(sk1,top)),one),meet(complement(sk1),one)) != meet(complement(sk1),one)
| join(complement(join(complement(one),complement(complement(sk1)))),complement(join(complement(one),complement(complement(composition(sk1,top)))))) != meet(complement(composition(sk1,top)),one) ),
inference(paramod,[status(thm)],[c_1,c_3336]) ).
cnf(c_3338,plain,
( join(meet(complement(composition(sk1,top)),one),meet(complement(sk1),one)) != meet(complement(sk1),one)
| join(complement(join(complement(one),complement(complement(sk1)))),complement(join(complement(one),complement(complement(composition(sk1,top)))))) != complement(join(complement(complement(composition(sk1,top))),complement(one))) ),
inference(paramod,[status(thm)],[c_6,c_3337]) ).
cnf(c_3339,plain,
( join(meet(complement(composition(sk1,top)),one),meet(complement(sk1),one)) != meet(complement(sk1),one)
| join(complement(join(complement(one),complement(complement(sk1)))),complement(join(complement(one),complement(complement(composition(sk1,top)))))) != complement(join(complement(one),complement(complement(composition(sk1,top))))) ),
inference(paramod,[status(thm)],[c_1,c_3338]) ).
cnf(c_3340,plain,
( join(complement(join(complement(complement(composition(sk1,top))),complement(one))),meet(complement(sk1),one)) != meet(complement(sk1),one)
| join(complement(join(complement(one),complement(complement(sk1)))),complement(join(complement(one),complement(complement(composition(sk1,top)))))) != complement(join(complement(one),complement(complement(composition(sk1,top))))) ),
inference(paramod,[status(thm)],[c_6,c_3339]) ).
cnf(c_3341,plain,
( join(complement(join(complement(one),complement(complement(composition(sk1,top))))),meet(complement(sk1),one)) != meet(complement(sk1),one)
| join(complement(join(complement(one),complement(complement(sk1)))),complement(join(complement(one),complement(complement(composition(sk1,top)))))) != complement(join(complement(one),complement(complement(composition(sk1,top))))) ),
inference(paramod,[status(thm)],[c_1,c_3340]) ).
cnf(c_3342,plain,
( join(complement(join(complement(one),complement(complement(composition(sk1,top))))),complement(join(complement(complement(sk1)),complement(one)))) != meet(complement(sk1),one)
| join(complement(join(complement(one),complement(complement(sk1)))),complement(join(complement(one),complement(complement(composition(sk1,top)))))) != complement(join(complement(one),complement(complement(composition(sk1,top))))) ),
inference(paramod,[status(thm)],[c_6,c_3341]) ).
cnf(c_3343,plain,
( join(complement(join(complement(one),complement(complement(composition(sk1,top))))),complement(join(complement(one),complement(complement(sk1))))) != meet(complement(sk1),one)
| join(complement(join(complement(one),complement(complement(sk1)))),complement(join(complement(one),complement(complement(composition(sk1,top)))))) != complement(join(complement(one),complement(complement(composition(sk1,top))))) ),
inference(paramod,[status(thm)],[c_1,c_3342]) ).
cnf(c_3344,plain,
( join(complement(join(complement(one),complement(complement(sk1)))),complement(join(complement(one),complement(complement(composition(sk1,top)))))) != meet(complement(sk1),one)
| join(complement(join(complement(one),complement(complement(sk1)))),complement(join(complement(one),complement(complement(composition(sk1,top)))))) != complement(join(complement(one),complement(complement(composition(sk1,top))))) ),
inference(paramod,[status(thm)],[c_1,c_3343]) ).
cnf(c_3345,plain,
( join(complement(join(complement(one),complement(complement(sk1)))),complement(join(complement(one),complement(complement(composition(sk1,top)))))) != complement(join(complement(complement(sk1)),complement(one)))
| join(complement(join(complement(one),complement(complement(sk1)))),complement(join(complement(one),complement(complement(composition(sk1,top)))))) != complement(join(complement(one),complement(complement(composition(sk1,top))))) ),
inference(paramod,[status(thm)],[c_6,c_3344]) ).
cnf(c_32,plain,
( join(complement(join(complement(one),complement(complement(sk1)))),complement(join(complement(one),complement(complement(composition(sk1,top)))))) != complement(join(complement(one),complement(complement(sk1))))
| join(complement(join(complement(one),complement(complement(sk1)))),complement(join(complement(one),complement(complement(composition(sk1,top)))))) != complement(join(complement(one),complement(complement(composition(sk1,top))))) ),
inference(paramod,[status(thm)],[c_1,c_3345]) ).
cnf(c_3346,plain,
join(join(A,B),C) = join(B,join(A,C)),
inference(paramod,[status(thm)],[c_1,c_3]) ).
cnf(c_34,plain,
join(A,join(B,C)) = join(B,join(A,C)),
inference(paramod,[status(thm)],[c_3,c_3346]) ).
cnf(c_36,plain,
join(complement(join(complement(A),B)),complement(join(complement(B),complement(A)))) = A,
inference(paramod,[status(thm)],[c_1,c_5]) ).
cnf(c_3347,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_37,plain,
join(complement(join(complement(A),B)),join(complement(join(complement(A),complement(B))),C)) = join(A,C),
inference(copy,[status(thm)],[c_3347]) ).
cnf(c_3348,plain,
composition(A,B) = composition(A,composition(one,B)),
inference(paramod,[status(thm)],[c_9,c_8]) ).
cnf(c_41,plain,
composition(A,composition(one,B)) = composition(A,B),
inference(copy,[status(thm)],[c_3348]) ).
cnf(c_43,plain,
join(composition(A,composition(B,C)),composition(D,C)) = composition(join(composition(A,B),D),C),
inference(paramod,[status(thm)],[c_8,c_11]) ).
cnf(c_44,plain,
join(composition(A,B),composition(C,composition(D,B))) = composition(join(A,composition(C,D)),B),
inference(paramod,[status(thm)],[c_8,c_11]) ).
cnf(c_3349,plain,
join(A,converse(B)) = converse(join(converse(A),B)),
inference(paramod,[status(thm)],[c_12,c_14]) ).
cnf(c_46,plain,
converse(join(converse(A),B)) = join(A,converse(B)),
inference(copy,[status(thm)],[c_3349]) ).
cnf(c_3350,plain,
join(converse(A),B) = converse(join(A,converse(B))),
inference(paramod,[status(thm)],[c_12,c_14]) ).
cnf(c_47,plain,
converse(join(A,converse(B))) = join(converse(A),B),
inference(copy,[status(thm)],[c_3350]) ).
cnf(c_3351,plain,
composition(converse(composition(A,B)),C) = composition(converse(B),composition(converse(A),C)),
inference(paramod,[status(thm)],[c_16,c_8]) ).
cnf(c_48,plain,
composition(converse(A),composition(converse(B),C)) = composition(converse(composition(B,A)),C),
inference(copy,[status(thm)],[c_3351]) ).
cnf(c_50,plain,
join(composition(A,converse(B)),converse(composition(B,C))) = composition(join(A,converse(C)),converse(B)),
inference(paramod,[status(thm)],[c_16,c_11]) ).
cnf(c_3352,plain,
composition(converse(A),B) = converse(composition(converse(B),A)),
inference(paramod,[status(thm)],[c_12,c_16]) ).
cnf(c_52,plain,
converse(composition(converse(A),B)) = composition(converse(B),A),
inference(copy,[status(thm)],[c_3352]) ).
cnf(c_54,plain,
join(complement(complement(A)),complement(join(complement(A),complement(composition(converse(B),complement(composition(B,A))))))) = A,
inference(paramod,[status(thm)],[c_18,c_5]) ).
cnf(c_3353,plain,
join(top,A) = join(B,join(complement(B),A)),
inference(paramod,[status(thm)],[c_20,c_3]) ).
cnf(c_60,plain,
join(A,join(complement(A),B)) = join(top,B),
inference(copy,[status(thm)],[c_3353]) ).
cnf(c_3354,plain,
join(join(A,B),complement(B)) = join(A,top),
inference(paramod,[status(thm)],[c_20,c_3]) ).
cnf(c_62,plain,
join(complement(A),join(B,A)) = join(B,top),
inference(paramod,[status(thm)],[c_1,c_3354]) ).
cnf(c_3355,plain,
join(complement(top),complement(join(complement(A),complement(complement(complement(A)))))) = A,
inference(paramod,[status(thm)],[c_20,c_5]) ).
cnf(c_63,plain,
join(zero,complement(join(complement(A),complement(complement(complement(A)))))) = A,
inference(paramod,[status(thm)],[c_22,c_3355]) ).
cnf(c_3356,plain,
join(zero,composition(converse(A),complement(composition(A,top)))) = complement(top),
inference(paramod,[status(thm)],[c_22,c_18]) ).
cnf(c_67,plain,
join(zero,composition(converse(A),complement(composition(A,top)))) = zero,
inference(paramod,[status(thm)],[c_22,c_3356]) ).
cnf(c_69,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_24]) ).
cnf(c_3357,plain,
join(complement(join(complement(composition(A,converse(B))),complement(C))),composition(complement(join(complement(A),complement(composition(C,B)))),complement(join(complement(converse(B)),complement(composition(converse(A),C)))))) = composition(complement(join(complement(A),complement(composition(C,converse(converse(B)))))),complement(join(complement(converse(B)),complement(composition(converse(A),C))))),
inference(paramod,[status(thm)],[c_12,c_24]) ).
cnf(c_75,plain,
join(complement(join(complement(composition(A,converse(B))),complement(C))),composition(complement(join(complement(A),complement(composition(C,B)))),complement(join(complement(converse(B)),complement(composition(converse(A),C)))))) = composition(complement(join(complement(A),complement(composition(C,B)))),complement(join(complement(converse(B)),complement(composition(converse(A),C))))),
inference(paramod,[status(thm)],[c_12,c_3357]) ).
cnf(c_3358,plain,
join(complement(join(complement(converse(composition(A,B))),complement(C))),composition(complement(join(complement(converse(B)),complement(composition(C,converse(converse(A)))))),complement(join(complement(converse(A)),complement(composition(converse(converse(B)),C)))))) = composition(complement(join(complement(converse(B)),complement(composition(C,converse(converse(A)))))),complement(join(complement(converse(A)),complement(composition(converse(converse(B)),C))))),
inference(paramod,[status(thm)],[c_16,c_24]) ).
cnf(c_3359,plain,
join(complement(join(complement(converse(composition(A,B))),complement(C))),composition(complement(join(complement(converse(B)),complement(composition(C,A)))),complement(join(complement(converse(A)),complement(composition(converse(converse(B)),C)))))) = composition(complement(join(complement(converse(B)),complement(composition(C,converse(converse(A)))))),complement(join(complement(converse(A)),complement(composition(converse(converse(B)),C))))),
inference(paramod,[status(thm)],[c_12,c_3358]) ).
cnf(c_3360,plain,
join(complement(join(complement(converse(composition(A,B))),complement(C))),composition(complement(join(complement(converse(B)),complement(composition(C,A)))),complement(join(complement(converse(A)),complement(composition(B,C)))))) = composition(complement(join(complement(converse(B)),complement(composition(C,converse(converse(A)))))),complement(join(complement(converse(A)),complement(composition(converse(converse(B)),C))))),
inference(paramod,[status(thm)],[c_12,c_3359]) ).
cnf(c_3361,plain,
join(complement(join(complement(converse(composition(A,B))),complement(C))),composition(complement(join(complement(converse(B)),complement(composition(C,A)))),complement(join(complement(converse(A)),complement(composition(B,C)))))) = composition(complement(join(complement(converse(B)),complement(composition(C,A)))),complement(join(complement(converse(A)),complement(composition(converse(converse(B)),C))))),
inference(paramod,[status(thm)],[c_12,c_3360]) ).
cnf(c_77,plain,
join(complement(join(complement(converse(composition(A,B))),complement(C))),composition(complement(join(complement(converse(B)),complement(composition(C,A)))),complement(join(complement(converse(A)),complement(composition(B,C)))))) = composition(complement(join(complement(converse(B)),complement(composition(C,A)))),complement(join(complement(converse(A)),complement(composition(B,C))))),
inference(paramod,[status(thm)],[c_12,c_3361]) ).
cnf(c_3362,plain,
join(one,A) = join(one,join(sk1,A)),
inference(paramod,[status(thm)],[c_30,c_3]) ).
cnf(c_100,plain,
join(one,join(sk1,A)) = join(one,A),
inference(copy,[status(thm)],[c_3362]) ).
cnf(c_3363,plain,
join(A,top) = join(B,join(A,complement(B))),
inference(paramod,[status(thm)],[c_20,c_34]) ).
cnf(c_107,plain,
join(A,join(B,complement(A))) = join(B,top),
inference(copy,[status(thm)],[c_3363]) ).
cnf(c_3364,plain,
join(one,join(sk1,complement(one))) = top,
inference(paramod,[status(thm)],[c_20,c_100]) ).
cnf(c_116,plain,
join(sk1,top) = top,
inference(paramod,[status(thm)],[c_107,c_3364]) ).
cnf(c_3365,plain,
join(join(A,sk1),top) = join(A,top),
inference(paramod,[status(thm)],[c_116,c_3]) ).
cnf(c_119,plain,
join(top,join(A,sk1)) = join(A,top),
inference(paramod,[status(thm)],[c_1,c_3365]) ).
cnf(c_3366,plain,
join(complement(join(complement(complement(A)),A)),complement(top)) = complement(A),
inference(paramod,[status(thm)],[c_20,c_36]) ).
cnf(c_3367,plain,
join(complement(join(A,complement(complement(A)))),complement(top)) = complement(A),
inference(paramod,[status(thm)],[c_1,c_3366]) ).
cnf(c_3368,plain,
join(complement(join(A,complement(complement(A)))),zero) = complement(A),
inference(paramod,[status(thm)],[c_22,c_3367]) ).
cnf(c_153,plain,
join(zero,complement(join(A,complement(complement(A))))) = complement(A),
inference(paramod,[status(thm)],[c_1,c_3368]) ).
cnf(c_159,plain,
complement(complement(A)) = A,
inference(paramod,[status(thm)],[c_153,c_63]) ).
cnf(c_160,plain,
join(zero,complement(join(A,A))) = complement(A),
inference(paramod,[status(thm)],[c_159,c_153]) ).
cnf(c_162,plain,
join(A,complement(join(complement(A),complement(composition(converse(B),complement(composition(B,A))))))) = A,
inference(paramod,[status(thm)],[c_159,c_54]) ).
cnf(c_3369,plain,
( join(complement(join(complement(one),complement(complement(sk1)))),complement(join(complement(one),complement(complement(composition(sk1,top)))))) != complement(join(complement(one),complement(complement(sk1))))
| join(complement(join(complement(one),sk1)),complement(join(complement(one),complement(complement(composition(sk1,top)))))) != complement(join(complement(one),complement(complement(composition(sk1,top))))) ),
inference(paramod,[status(thm)],[c_159,c_32]) ).
cnf(c_3370,plain,
( join(complement(join(complement(one),complement(complement(sk1)))),complement(join(complement(one),complement(complement(composition(sk1,top)))))) != complement(join(complement(one),complement(complement(sk1))))
| join(complement(join(sk1,complement(one))),complement(join(complement(one),complement(complement(composition(sk1,top)))))) != complement(join(complement(one),complement(complement(composition(sk1,top))))) ),
inference(paramod,[status(thm)],[c_1,c_3369]) ).
cnf(c_3371,plain,
( join(complement(join(complement(one),complement(complement(sk1)))),complement(join(complement(one),complement(complement(composition(sk1,top)))))) != complement(join(complement(one),complement(complement(sk1))))
| join(complement(join(sk1,complement(one))),complement(join(complement(one),composition(sk1,top)))) != complement(join(complement(one),complement(complement(composition(sk1,top))))) ),
inference(paramod,[status(thm)],[c_159,c_3370]) ).
cnf(c_3372,plain,
( join(complement(join(complement(one),complement(complement(sk1)))),complement(join(complement(one),complement(complement(composition(sk1,top)))))) != complement(join(complement(one),complement(complement(sk1))))
| join(complement(join(sk1,complement(one))),complement(join(complement(one),composition(sk1,top)))) != complement(join(complement(one),composition(sk1,top))) ),
inference(paramod,[status(thm)],[c_159,c_3371]) ).
cnf(c_3373,plain,
( join(complement(join(complement(one),sk1)),complement(join(complement(one),complement(complement(composition(sk1,top)))))) != complement(join(complement(one),complement(complement(sk1))))
| join(complement(join(sk1,complement(one))),complement(join(complement(one),composition(sk1,top)))) != complement(join(complement(one),composition(sk1,top))) ),
inference(paramod,[status(thm)],[c_159,c_3372]) ).
cnf(c_3374,plain,
( join(complement(join(sk1,complement(one))),complement(join(complement(one),complement(complement(composition(sk1,top)))))) != complement(join(complement(one),complement(complement(sk1))))
| join(complement(join(sk1,complement(one))),complement(join(complement(one),composition(sk1,top)))) != complement(join(complement(one),composition(sk1,top))) ),
inference(paramod,[status(thm)],[c_1,c_3373]) ).
cnf(c_3375,plain,
( join(complement(join(sk1,complement(one))),complement(join(complement(one),composition(sk1,top)))) != complement(join(complement(one),complement(complement(sk1))))
| join(complement(join(sk1,complement(one))),complement(join(complement(one),composition(sk1,top)))) != complement(join(complement(one),composition(sk1,top))) ),
inference(paramod,[status(thm)],[c_159,c_3374]) ).
cnf(c_3376,plain,
( join(complement(join(sk1,complement(one))),complement(join(complement(one),composition(sk1,top)))) != complement(join(complement(one),sk1))
| join(complement(join(sk1,complement(one))),complement(join(complement(one),composition(sk1,top)))) != complement(join(complement(one),composition(sk1,top))) ),
inference(paramod,[status(thm)],[c_159,c_3375]) ).
cnf(c_163,plain,
( join(complement(join(sk1,complement(one))),complement(join(complement(one),composition(sk1,top)))) != complement(join(sk1,complement(one)))
| join(complement(join(sk1,complement(one))),complement(join(complement(one),composition(sk1,top)))) != complement(join(complement(one),composition(sk1,top))) ),
inference(paramod,[status(thm)],[c_1,c_3376]) ).
cnf(c_166,plain,
complement(zero) = top,
inference(paramod,[status(thm)],[c_22,c_159]) ).
cnf(c_3377,plain,
join(complement(composition(converse(A),complement(composition(A,B)))),complement(B)) = join(complement(B),top),
inference(paramod,[status(thm)],[c_18,c_62]) ).
cnf(c_3378,plain,
join(complement(B),complement(composition(converse(A),complement(composition(A,B))))) = join(complement(B),top),
inference(paramod,[status(thm)],[c_1,c_3377]) ).
cnf(c_190,plain,
join(complement(A),complement(composition(converse(B),complement(composition(B,A))))) = join(top,complement(A)),
inference(paramod,[status(thm)],[c_1,c_3378]) ).
cnf(c_3379,plain,
join(complement(composition(complement(join(complement(A),complement(composition(B,converse(C))))),complement(join(complement(C),complement(composition(converse(A),B)))))),composition(complement(join(complement(A),complement(composition(B,converse(C))))),complement(join(complement(C),complement(composition(converse(A),B)))))) = join(complement(join(complement(composition(A,C)),complement(B))),top),
inference(paramod,[status(thm)],[c_24,c_62]) ).
cnf(c_3380,plain,
join(composition(complement(join(complement(A),complement(composition(B,converse(C))))),complement(join(complement(C),complement(composition(converse(A),B))))),complement(composition(complement(join(complement(A),complement(composition(B,converse(C))))),complement(join(complement(C),complement(composition(converse(A),B))))))) = join(complement(join(complement(composition(A,C)),complement(B))),top),
inference(paramod,[status(thm)],[c_1,c_3379]) ).
cnf(c_3381,plain,
top = join(complement(join(complement(composition(A,C)),complement(B))),top),
inference(paramod,[status(thm)],[c_20,c_3380]) ).
cnf(c_3382,plain,
top = join(top,complement(join(complement(composition(A,C)),complement(B)))),
inference(paramod,[status(thm)],[c_1,c_3381]) ).
cnf(c_191,plain,
join(top,complement(join(complement(composition(A,B)),complement(C)))) = top,
inference(copy,[status(thm)],[c_3382]) ).
cnf(c_3383,plain,
join(complement(join(A,sk1)),join(A,top)) = join(top,top),
inference(paramod,[status(thm)],[c_119,c_62]) ).
cnf(c_3384,plain,
join(join(A,top),complement(join(A,sk1))) = join(top,top),
inference(paramod,[status(thm)],[c_1,c_3383]) ).
cnf(c_197,plain,
join(A,join(top,complement(join(A,sk1)))) = join(top,top),
inference(paramod,[status(thm)],[c_3,c_3384]) ).
cnf(c_3385,plain,
join(complement(join(A,B)),join(A,top)) = join(complement(B),top),
inference(paramod,[status(thm)],[c_62,c_62]) ).
cnf(c_3386,plain,
join(join(A,top),complement(join(A,B))) = join(complement(B),top),
inference(paramod,[status(thm)],[c_1,c_3385]) ).
cnf(c_3387,plain,
join(A,join(top,complement(join(A,B)))) = join(complement(B),top),
inference(paramod,[status(thm)],[c_3,c_3386]) ).
cnf(c_198,plain,
join(A,join(top,complement(join(A,B)))) = join(top,complement(B)),
inference(paramod,[status(thm)],[c_1,c_3387]) ).
cnf(c_199,plain,
join(A,complement(join(top,complement(A)))) = A,
inference(paramod,[status(thm)],[c_190,c_162]) ).
cnf(c_201,plain,
join(top,complement(sk1)) = join(top,top),
inference(paramod,[status(thm)],[c_198,c_197]) ).
cnf(c_3388,plain,
join(A,join(top,top)) = join(top,join(A,complement(sk1))),
inference(paramod,[status(thm)],[c_201,c_34]) ).
cnf(c_204,plain,
join(top,join(A,complement(sk1))) = join(A,join(top,top)),
inference(copy,[status(thm)],[c_3388]) ).
cnf(c_3389,plain,
join(complement(join(complement(A),B)),top) = join(A,complement(complement(join(complement(A),complement(B))))),
inference(paramod,[status(thm)],[c_20,c_37]) ).
cnf(c_3390,plain,
join(top,complement(join(complement(A),B))) = join(A,complement(complement(join(complement(A),complement(B))))),
inference(paramod,[status(thm)],[c_1,c_3389]) ).
cnf(c_3391,plain,
join(top,complement(join(complement(A),B))) = join(A,join(complement(A),complement(B))),
inference(paramod,[status(thm)],[c_159,c_3390]) ).
cnf(c_210,plain,
join(top,complement(join(complement(A),B))) = join(top,complement(B)),
inference(paramod,[status(thm)],[c_60,c_3391]) ).
cnf(c_3392,plain,
join(top,complement(complement(C))) = top,
inference(paramod,[status(thm)],[c_210,c_191]) ).
cnf(c_226,plain,
join(top,A) = top,
inference(paramod,[status(thm)],[c_159,c_3392]) ).
cnf(c_3393,plain,
top = join(A,join(top,top)),
inference(paramod,[status(thm)],[c_226,c_204]) ).
cnf(c_3394,plain,
top = join(A,top),
inference(paramod,[status(thm)],[c_226,c_3393]) ).
cnf(c_230,plain,
join(A,top) = top,
inference(copy,[status(thm)],[c_3394]) ).
cnf(c_3395,plain,
join(A,complement(top)) = A,
inference(paramod,[status(thm)],[c_226,c_199]) ).
cnf(c_232,plain,
join(A,zero) = A,
inference(paramod,[status(thm)],[c_22,c_3395]) ).
cnf(c_3396,plain,
A = join(zero,A),
inference(paramod,[status(thm)],[c_232,c_1]) ).
cnf(c_257,plain,
join(zero,A) = A,
inference(copy,[status(thm)],[c_3396]) ).
cnf(c_261,plain,
complement(join(A,A)) = complement(A),
inference(paramod,[status(thm)],[c_257,c_160]) ).
cnf(c_269,plain,
composition(converse(A),complement(composition(A,top))) = zero,
inference(paramod,[status(thm)],[c_257,c_67]) ).
cnf(c_3397,plain,
complement(complement(A)) = join(A,A),
inference(paramod,[status(thm)],[c_261,c_159]) ).
cnf(c_3398,plain,
A = join(A,A),
inference(paramod,[status(thm)],[c_159,c_3397]) ).
cnf(c_281,plain,
join(A,A) = A,
inference(copy,[status(thm)],[c_3398]) ).
cnf(c_3399,plain,
join(A,B) = join(A,join(A,B)),
inference(paramod,[status(thm)],[c_281,c_3]) ).
cnf(c_287,plain,
join(A,join(A,B)) = join(A,B),
inference(copy,[status(thm)],[c_3399]) ).
cnf(c_3400,plain,
converse(top) = join(A,converse(top)),
inference(paramod,[status(thm)],[c_230,c_46]) ).
cnf(c_324,plain,
join(A,converse(top)) = converse(top),
inference(copy,[status(thm)],[c_3400]) ).
cnf(c_339,plain,
converse(top) = top,
inference(paramod,[status(thm)],[c_324,c_226]) ).
cnf(c_3401,plain,
composition(top,converse(A)) = converse(composition(A,top)),
inference(paramod,[status(thm)],[c_339,c_16]) ).
cnf(c_349,plain,
converse(composition(A,top)) = composition(top,converse(A)),
inference(copy,[status(thm)],[c_3401]) ).
cnf(c_3402,plain,
composition(converse(A),top) = converse(composition(top,A)),
inference(paramod,[status(thm)],[c_339,c_16]) ).
cnf(c_350,plain,
converse(composition(top,A)) = composition(converse(A),top),
inference(copy,[status(thm)],[c_3402]) ).
cnf(c_351,plain,
join(complement(A),composition(top,complement(composition(top,A)))) = complement(A),
inference(paramod,[status(thm)],[c_339,c_18]) ).
cnf(c_354,plain,
composition(top,complement(composition(top,top))) = zero,
inference(paramod,[status(thm)],[c_339,c_269]) ).
cnf(c_3403,plain,
converse(top) = composition(converse(one),top),
inference(paramod,[status(thm)],[c_9,c_350]) ).
cnf(c_3404,plain,
top = composition(converse(one),top),
inference(paramod,[status(thm)],[c_339,c_3403]) ).
cnf(c_379,plain,
composition(converse(one),top) = top,
inference(copy,[status(thm)],[c_3404]) ).
cnf(c_3405,plain,
join(top,composition(A,top)) = composition(join(converse(one),A),top),
inference(paramod,[status(thm)],[c_379,c_11]) ).
cnf(c_3406,plain,
top = composition(join(converse(one),A),top),
inference(paramod,[status(thm)],[c_226,c_3405]) ).
cnf(c_394,plain,
composition(join(converse(one),A),top) = top,
inference(copy,[status(thm)],[c_3406]) ).
cnf(c_3407,plain,
join(zero,composition(A,complement(composition(top,top)))) = composition(join(top,A),complement(composition(top,top))),
inference(paramod,[status(thm)],[c_354,c_11]) ).
cnf(c_3408,plain,
composition(A,complement(composition(top,top))) = composition(join(top,A),complement(composition(top,top))),
inference(paramod,[status(thm)],[c_257,c_3407]) ).
cnf(c_3409,plain,
composition(A,complement(composition(top,top))) = composition(top,complement(composition(top,top))),
inference(paramod,[status(thm)],[c_226,c_3408]) ).
cnf(c_525,plain,
composition(A,complement(composition(top,top))) = zero,
inference(paramod,[status(thm)],[c_354,c_3409]) ).
cnf(c_3410,plain,
join(composition(A,zero),composition(B,complement(composition(top,top)))) = composition(join(composition(A,top),B),complement(composition(top,top))),
inference(paramod,[status(thm)],[c_354,c_43]) ).
cnf(c_3411,plain,
join(composition(A,zero),zero) = composition(join(composition(A,top),B),complement(composition(top,top))),
inference(paramod,[status(thm)],[c_525,c_3410]) ).
cnf(c_3412,plain,
join(zero,composition(A,zero)) = composition(join(composition(A,top),B),complement(composition(top,top))),
inference(paramod,[status(thm)],[c_1,c_3411]) ).
cnf(c_3413,plain,
composition(A,zero) = composition(join(composition(A,top),B),complement(composition(top,top))),
inference(paramod,[status(thm)],[c_257,c_3412]) ).
cnf(c_527,plain,
composition(A,zero) = zero,
inference(paramod,[status(thm)],[c_525,c_3413]) ).
cnf(c_558,plain,
composition(top,top) = top,
inference(paramod,[status(thm)],[c_20,c_394]) ).
cnf(c_3414,plain,
composition(converse(A),zero) = composition(converse(composition(B,A)),complement(composition(B,top))),
inference(paramod,[status(thm)],[c_269,c_48]) ).
cnf(c_3415,plain,
zero = composition(converse(composition(B,A)),complement(composition(B,top))),
inference(paramod,[status(thm)],[c_527,c_3414]) ).
cnf(c_566,plain,
composition(converse(composition(A,B)),complement(composition(A,top))) = zero,
inference(copy,[status(thm)],[c_3415]) ).
cnf(c_3416,plain,
composition(top,A) = composition(top,composition(top,A)),
inference(paramod,[status(thm)],[c_558,c_8]) ).
cnf(c_571,plain,
composition(top,composition(top,A)) = composition(top,A),
inference(copy,[status(thm)],[c_3416]) ).
cnf(c_3417,plain,
join(complement(composition(top,A)),composition(converse(top),complement(composition(top,A)))) = complement(composition(top,A)),
inference(paramod,[status(thm)],[c_571,c_18]) ).
cnf(c_577,plain,
join(complement(composition(top,A)),composition(top,complement(composition(top,A)))) = complement(composition(top,A)),
inference(paramod,[status(thm)],[c_339,c_3417]) ).
cnf(c_3418,plain,
converse(converse(A)) = composition(converse(one),A),
inference(paramod,[status(thm)],[c_9,c_52]) ).
cnf(c_3419,plain,
A = composition(converse(one),A),
inference(paramod,[status(thm)],[c_12,c_3418]) ).
cnf(c_642,plain,
composition(converse(one),A) = A,
inference(copy,[status(thm)],[c_3419]) ).
cnf(c_3420,plain,
one = converse(one),
inference(paramod,[status(thm)],[c_642,c_9]) ).
cnf(c_649,plain,
converse(one) = one,
inference(copy,[status(thm)],[c_3420]) ).
cnf(c_3421,plain,
join(A,composition(B,A)) = composition(join(converse(one),B),A),
inference(paramod,[status(thm)],[c_642,c_11]) ).
cnf(c_3422,plain,
join(A,composition(B,A)) = composition(join(one,B),A),
inference(paramod,[status(thm)],[c_649,c_3421]) ).
cnf(c_650,plain,
composition(join(one,A),B) = join(B,composition(A,B)),
inference(copy,[status(thm)],[c_3422]) ).
cnf(c_3423,plain,
composition(converse(one),composition(one,A)) = A,
inference(paramod,[status(thm)],[c_642,c_41]) ).
cnf(c_3424,plain,
composition(one,composition(one,A)) = A,
inference(paramod,[status(thm)],[c_649,c_3423]) ).
cnf(c_666,plain,
composition(one,A) = A,
inference(paramod,[status(thm)],[c_41,c_3424]) ).
cnf(c_3425,plain,
composition(join(one,top),complement(composition(top,A))) = complement(composition(top,A)),
inference(paramod,[status(thm)],[c_650,c_577]) ).
cnf(c_690,plain,
composition(top,complement(composition(top,A))) = complement(composition(top,A)),
inference(paramod,[status(thm)],[c_230,c_3425]) ).
cnf(c_696,plain,
join(complement(A),complement(composition(top,A))) = complement(A),
inference(paramod,[status(thm)],[c_690,c_351]) ).
cnf(c_3426,plain,
join(one,converse(A)) = converse(join(one,A)),
inference(paramod,[status(thm)],[c_649,c_14]) ).
cnf(c_697,plain,
converse(join(one,A)) = join(one,converse(A)),
inference(copy,[status(thm)],[c_3426]) ).
cnf(c_3427,plain,
converse(one) = join(one,converse(sk1)),
inference(paramod,[status(thm)],[c_30,c_697]) ).
cnf(c_3428,plain,
one = join(one,converse(sk1)),
inference(paramod,[status(thm)],[c_649,c_3427]) ).
cnf(c_718,plain,
join(one,converse(sk1)) = one,
inference(copy,[status(thm)],[c_3428]) ).
cnf(c_3429,plain,
join(composition(one,A),composition(converse(sk1),A)) = composition(one,A),
inference(paramod,[status(thm)],[c_718,c_11]) ).
cnf(c_3430,plain,
join(A,composition(converse(sk1),A)) = composition(one,A),
inference(paramod,[status(thm)],[c_666,c_3429]) ).
cnf(c_729,plain,
join(A,composition(converse(sk1),A)) = A,
inference(paramod,[status(thm)],[c_666,c_3430]) ).
cnf(c_3431,plain,
composition(one,A) = join(A,composition(sk1,A)),
inference(paramod,[status(thm)],[c_30,c_650]) ).
cnf(c_3432,plain,
A = join(A,composition(sk1,A)),
inference(paramod,[status(thm)],[c_666,c_3431]) ).
cnf(c_746,plain,
join(A,composition(sk1,A)) = A,
inference(copy,[status(thm)],[c_3432]) ).
cnf(c_753,plain,
join(A,composition(join(one,B),A)) = join(A,composition(B,A)),
inference(paramod,[status(thm)],[c_650,c_287]) ).
cnf(c_3433,plain,
join(one,sk1) = join(one,composition(converse(sk1),sk1)),
inference(paramod,[status(thm)],[c_729,c_100]) ).
cnf(c_3434,plain,
one = join(one,composition(converse(sk1),sk1)),
inference(paramod,[status(thm)],[c_30,c_3433]) ).
cnf(c_882,plain,
join(one,composition(converse(sk1),sk1)) = one,
inference(copy,[status(thm)],[c_3434]) ).
cnf(c_3435,plain,
converse(converse(A)) = join(A,converse(composition(converse(sk1),converse(A)))),
inference(paramod,[status(thm)],[c_729,c_46]) ).
cnf(c_3436,plain,
A = join(A,converse(composition(converse(sk1),converse(A)))),
inference(paramod,[status(thm)],[c_12,c_3435]) ).
cnf(c_3437,plain,
A = join(A,converse(converse(composition(A,sk1)))),
inference(paramod,[status(thm)],[c_16,c_3436]) ).
cnf(c_3438,plain,
A = join(A,composition(A,sk1)),
inference(paramod,[status(thm)],[c_12,c_3437]) ).
cnf(c_884,plain,
join(A,composition(A,sk1)) = A,
inference(copy,[status(thm)],[c_3438]) ).
cnf(c_3439,plain,
join(composition(one,A),composition(composition(converse(sk1),sk1),A)) = composition(one,A),
inference(paramod,[status(thm)],[c_882,c_11]) ).
cnf(c_3440,plain,
join(A,composition(composition(converse(sk1),sk1),A)) = composition(one,A),
inference(paramod,[status(thm)],[c_666,c_3439]) ).
cnf(c_3441,plain,
join(A,composition(converse(sk1),composition(sk1,A))) = composition(one,A),
inference(paramod,[status(thm)],[c_8,c_3440]) ).
cnf(c_939,plain,
join(A,composition(converse(sk1),composition(sk1,A))) = A,
inference(paramod,[status(thm)],[c_666,c_3441]) ).
cnf(c_3442,plain,
join(complement(complement(composition(A,top))),composition(converse(converse(composition(A,B))),complement(zero))) = complement(complement(composition(A,top))),
inference(paramod,[status(thm)],[c_566,c_18]) ).
cnf(c_3443,plain,
join(composition(A,top),composition(converse(converse(composition(A,B))),complement(zero))) = complement(complement(composition(A,top))),
inference(paramod,[status(thm)],[c_159,c_3442]) ).
cnf(c_3444,plain,
join(composition(A,top),composition(composition(A,B),complement(zero))) = complement(complement(composition(A,top))),
inference(paramod,[status(thm)],[c_12,c_3443]) ).
cnf(c_3445,plain,
join(composition(A,top),composition(composition(A,B),top)) = complement(complement(composition(A,top))),
inference(paramod,[status(thm)],[c_166,c_3444]) ).
cnf(c_3446,plain,
join(composition(A,top),composition(A,composition(B,top))) = complement(complement(composition(A,top))),
inference(paramod,[status(thm)],[c_8,c_3445]) ).
cnf(c_3447,plain,
composition(join(A,composition(A,B)),top) = complement(complement(composition(A,top))),
inference(paramod,[status(thm)],[c_44,c_3446]) ).
cnf(c_1185,plain,
composition(join(A,composition(A,B)),top) = composition(A,top),
inference(paramod,[status(thm)],[c_159,c_3447]) ).
cnf(c_3448,plain,
join(converse(A),converse(composition(converse(sk1),composition(sk1,A)))) = converse(A),
inference(paramod,[status(thm)],[c_939,c_14]) ).
cnf(c_1545,plain,
join(converse(A),composition(converse(composition(sk1,A)),sk1)) = converse(A),
inference(paramod,[status(thm)],[c_52,c_3448]) ).
cnf(c_3449,plain,
join(complement(join(complement(composition(A,converse(top))),complement(top))),composition(complement(join(complement(A),complement(top))),complement(join(complement(converse(top)),complement(composition(converse(A),top)))))) = composition(complement(join(complement(A),complement(composition(top,top)))),complement(join(complement(converse(top)),complement(composition(converse(A),top))))),
inference(paramod,[status(thm)],[c_558,c_75]) ).
cnf(c_3450,plain,
join(complement(join(complement(composition(A,top)),complement(top))),composition(complement(join(complement(A),complement(top))),complement(join(complement(converse(top)),complement(composition(converse(A),top)))))) = composition(complement(join(complement(A),complement(composition(top,top)))),complement(join(complement(converse(top)),complement(composition(converse(A),top))))),
inference(paramod,[status(thm)],[c_339,c_3449]) ).
cnf(c_3451,plain,
join(complement(join(complement(composition(A,top)),zero)),composition(complement(join(complement(A),complement(top))),complement(join(complement(converse(top)),complement(composition(converse(A),top)))))) = composition(complement(join(complement(A),complement(composition(top,top)))),complement(join(complement(converse(top)),complement(composition(converse(A),top))))),
inference(paramod,[status(thm)],[c_22,c_3450]) ).
cnf(c_3452,plain,
join(complement(join(zero,complement(composition(A,top)))),composition(complement(join(complement(A),complement(top))),complement(join(complement(converse(top)),complement(composition(converse(A),top)))))) = composition(complement(join(complement(A),complement(composition(top,top)))),complement(join(complement(converse(top)),complement(composition(converse(A),top))))),
inference(paramod,[status(thm)],[c_1,c_3451]) ).
cnf(c_3453,plain,
join(complement(complement(composition(A,top))),composition(complement(join(complement(A),complement(top))),complement(join(complement(converse(top)),complement(composition(converse(A),top)))))) = composition(complement(join(complement(A),complement(composition(top,top)))),complement(join(complement(converse(top)),complement(composition(converse(A),top))))),
inference(paramod,[status(thm)],[c_257,c_3452]) ).
cnf(c_3454,plain,
join(composition(A,top),composition(complement(join(complement(A),complement(top))),complement(join(complement(converse(top)),complement(composition(converse(A),top)))))) = composition(complement(join(complement(A),complement(composition(top,top)))),complement(join(complement(converse(top)),complement(composition(converse(A),top))))),
inference(paramod,[status(thm)],[c_159,c_3453]) ).
cnf(c_3455,plain,
join(composition(A,top),composition(complement(join(complement(A),zero)),complement(join(complement(converse(top)),complement(composition(converse(A),top)))))) = composition(complement(join(complement(A),complement(composition(top,top)))),complement(join(complement(converse(top)),complement(composition(converse(A),top))))),
inference(paramod,[status(thm)],[c_22,c_3454]) ).
cnf(c_3456,plain,
join(composition(A,top),composition(complement(join(zero,complement(A))),complement(join(complement(converse(top)),complement(composition(converse(A),top)))))) = composition(complement(join(complement(A),complement(composition(top,top)))),complement(join(complement(converse(top)),complement(composition(converse(A),top))))),
inference(paramod,[status(thm)],[c_1,c_3455]) ).
cnf(c_3457,plain,
join(composition(A,top),composition(complement(complement(A)),complement(join(complement(converse(top)),complement(composition(converse(A),top)))))) = composition(complement(join(complement(A),complement(composition(top,top)))),complement(join(complement(converse(top)),complement(composition(converse(A),top))))),
inference(paramod,[status(thm)],[c_257,c_3456]) ).
cnf(c_3458,plain,
join(composition(A,top),composition(A,complement(join(complement(converse(top)),complement(composition(converse(A),top)))))) = composition(complement(join(complement(A),complement(composition(top,top)))),complement(join(complement(converse(top)),complement(composition(converse(A),top))))),
inference(paramod,[status(thm)],[c_159,c_3457]) ).
cnf(c_3459,plain,
join(composition(A,top),composition(A,complement(join(complement(top),complement(composition(converse(A),top)))))) = composition(complement(join(complement(A),complement(composition(top,top)))),complement(join(complement(converse(top)),complement(composition(converse(A),top))))),
inference(paramod,[status(thm)],[c_339,c_3458]) ).
cnf(c_3460,plain,
join(composition(A,top),composition(A,complement(join(zero,complement(composition(converse(A),top)))))) = composition(complement(join(complement(A),complement(composition(top,top)))),complement(join(complement(converse(top)),complement(composition(converse(A),top))))),
inference(paramod,[status(thm)],[c_22,c_3459]) ).
cnf(c_3461,plain,
join(composition(A,top),composition(A,complement(complement(composition(converse(A),top))))) = composition(complement(join(complement(A),complement(composition(top,top)))),complement(join(complement(converse(top)),complement(composition(converse(A),top))))),
inference(paramod,[status(thm)],[c_257,c_3460]) ).
cnf(c_3462,plain,
join(composition(A,top),composition(A,composition(converse(A),top))) = composition(complement(join(complement(A),complement(composition(top,top)))),complement(join(complement(converse(top)),complement(composition(converse(A),top))))),
inference(paramod,[status(thm)],[c_159,c_3461]) ).
cnf(c_3463,plain,
composition(join(A,composition(A,converse(A))),top) = composition(complement(join(complement(A),complement(composition(top,top)))),complement(join(complement(converse(top)),complement(composition(converse(A),top))))),
inference(paramod,[status(thm)],[c_44,c_3462]) ).
cnf(c_3464,plain,
composition(A,top) = composition(complement(join(complement(A),complement(composition(top,top)))),complement(join(complement(converse(top)),complement(composition(converse(A),top))))),
inference(paramod,[status(thm)],[c_1185,c_3463]) ).
cnf(c_3465,plain,
composition(A,top) = composition(complement(join(complement(A),complement(top))),complement(join(complement(converse(top)),complement(composition(converse(A),top))))),
inference(paramod,[status(thm)],[c_558,c_3464]) ).
cnf(c_3466,plain,
composition(A,top) = composition(complement(join(complement(A),zero)),complement(join(complement(converse(top)),complement(composition(converse(A),top))))),
inference(paramod,[status(thm)],[c_22,c_3465]) ).
cnf(c_3467,plain,
composition(A,top) = composition(complement(join(zero,complement(A))),complement(join(complement(converse(top)),complement(composition(converse(A),top))))),
inference(paramod,[status(thm)],[c_1,c_3466]) ).
cnf(c_3468,plain,
composition(A,top) = composition(complement(complement(A)),complement(join(complement(converse(top)),complement(composition(converse(A),top))))),
inference(paramod,[status(thm)],[c_257,c_3467]) ).
cnf(c_3469,plain,
composition(A,top) = composition(A,complement(join(complement(converse(top)),complement(composition(converse(A),top))))),
inference(paramod,[status(thm)],[c_159,c_3468]) ).
cnf(c_3470,plain,
composition(A,top) = composition(A,complement(join(complement(top),complement(composition(converse(A),top))))),
inference(paramod,[status(thm)],[c_339,c_3469]) ).
cnf(c_3471,plain,
composition(A,top) = composition(A,complement(join(zero,complement(composition(converse(A),top))))),
inference(paramod,[status(thm)],[c_22,c_3470]) ).
cnf(c_3472,plain,
composition(A,top) = composition(A,complement(complement(composition(converse(A),top)))),
inference(paramod,[status(thm)],[c_257,c_3471]) ).
cnf(c_3473,plain,
composition(A,top) = composition(A,composition(converse(A),top)),
inference(paramod,[status(thm)],[c_159,c_3472]) ).
cnf(c_1572,plain,
composition(A,composition(converse(A),top)) = composition(A,top),
inference(copy,[status(thm)],[c_3473]) ).
cnf(c_3474,plain,
join(complement(join(complement(converse(composition(top,A))),complement(top))),composition(complement(join(complement(converse(A)),complement(top))),complement(join(complement(converse(top)),complement(composition(A,top)))))) = composition(complement(join(complement(converse(A)),complement(composition(top,top)))),complement(join(complement(converse(top)),complement(composition(A,top))))),
inference(paramod,[status(thm)],[c_558,c_77]) ).
cnf(c_3475,plain,
join(complement(join(complement(composition(converse(A),top)),complement(top))),composition(complement(join(complement(converse(A)),complement(top))),complement(join(complement(converse(top)),complement(composition(A,top)))))) = composition(complement(join(complement(converse(A)),complement(composition(top,top)))),complement(join(complement(converse(top)),complement(composition(A,top))))),
inference(paramod,[status(thm)],[c_350,c_3474]) ).
cnf(c_3476,plain,
join(complement(join(complement(composition(converse(A),top)),zero)),composition(complement(join(complement(converse(A)),complement(top))),complement(join(complement(converse(top)),complement(composition(A,top)))))) = composition(complement(join(complement(converse(A)),complement(composition(top,top)))),complement(join(complement(converse(top)),complement(composition(A,top))))),
inference(paramod,[status(thm)],[c_22,c_3475]) ).
cnf(c_3477,plain,
join(complement(join(zero,complement(composition(converse(A),top)))),composition(complement(join(complement(converse(A)),complement(top))),complement(join(complement(converse(top)),complement(composition(A,top)))))) = composition(complement(join(complement(converse(A)),complement(composition(top,top)))),complement(join(complement(converse(top)),complement(composition(A,top))))),
inference(paramod,[status(thm)],[c_1,c_3476]) ).
cnf(c_3478,plain,
join(complement(complement(composition(converse(A),top))),composition(complement(join(complement(converse(A)),complement(top))),complement(join(complement(converse(top)),complement(composition(A,top)))))) = composition(complement(join(complement(converse(A)),complement(composition(top,top)))),complement(join(complement(converse(top)),complement(composition(A,top))))),
inference(paramod,[status(thm)],[c_257,c_3477]) ).
cnf(c_3479,plain,
join(composition(converse(A),top),composition(complement(join(complement(converse(A)),complement(top))),complement(join(complement(converse(top)),complement(composition(A,top)))))) = composition(complement(join(complement(converse(A)),complement(composition(top,top)))),complement(join(complement(converse(top)),complement(composition(A,top))))),
inference(paramod,[status(thm)],[c_159,c_3478]) ).
cnf(c_3480,plain,
join(composition(converse(A),top),composition(complement(join(complement(converse(A)),zero)),complement(join(complement(converse(top)),complement(composition(A,top)))))) = composition(complement(join(complement(converse(A)),complement(composition(top,top)))),complement(join(complement(converse(top)),complement(composition(A,top))))),
inference(paramod,[status(thm)],[c_22,c_3479]) ).
cnf(c_3481,plain,
join(composition(converse(A),top),composition(complement(join(zero,complement(converse(A)))),complement(join(complement(converse(top)),complement(composition(A,top)))))) = composition(complement(join(complement(converse(A)),complement(composition(top,top)))),complement(join(complement(converse(top)),complement(composition(A,top))))),
inference(paramod,[status(thm)],[c_1,c_3480]) ).
cnf(c_3482,plain,
join(composition(converse(A),top),composition(complement(complement(converse(A))),complement(join(complement(converse(top)),complement(composition(A,top)))))) = composition(complement(join(complement(converse(A)),complement(composition(top,top)))),complement(join(complement(converse(top)),complement(composition(A,top))))),
inference(paramod,[status(thm)],[c_257,c_3481]) ).
cnf(c_3483,plain,
join(composition(converse(A),top),composition(converse(A),complement(join(complement(converse(top)),complement(composition(A,top)))))) = composition(complement(join(complement(converse(A)),complement(composition(top,top)))),complement(join(complement(converse(top)),complement(composition(A,top))))),
inference(paramod,[status(thm)],[c_159,c_3482]) ).
cnf(c_3484,plain,
join(composition(converse(A),top),composition(converse(A),complement(join(complement(top),complement(composition(A,top)))))) = composition(complement(join(complement(converse(A)),complement(composition(top,top)))),complement(join(complement(converse(top)),complement(composition(A,top))))),
inference(paramod,[status(thm)],[c_339,c_3483]) ).
cnf(c_3485,plain,
join(composition(converse(A),top),composition(converse(A),complement(join(zero,complement(composition(A,top)))))) = composition(complement(join(complement(converse(A)),complement(composition(top,top)))),complement(join(complement(converse(top)),complement(composition(A,top))))),
inference(paramod,[status(thm)],[c_22,c_3484]) ).
cnf(c_3486,plain,
join(composition(converse(A),top),composition(converse(A),complement(complement(composition(A,top))))) = composition(complement(join(complement(converse(A)),complement(composition(top,top)))),complement(join(complement(converse(top)),complement(composition(A,top))))),
inference(paramod,[status(thm)],[c_257,c_3485]) ).
cnf(c_3487,plain,
join(composition(converse(A),top),composition(converse(A),composition(A,top))) = composition(complement(join(complement(converse(A)),complement(composition(top,top)))),complement(join(complement(converse(top)),complement(composition(A,top))))),
inference(paramod,[status(thm)],[c_159,c_3486]) ).
cnf(c_3488,plain,
composition(join(converse(A),composition(converse(A),A)),top) = composition(complement(join(complement(converse(A)),complement(composition(top,top)))),complement(join(complement(converse(top)),complement(composition(A,top))))),
inference(paramod,[status(thm)],[c_44,c_3487]) ).
cnf(c_3489,plain,
composition(converse(A),top) = composition(complement(join(complement(converse(A)),complement(composition(top,top)))),complement(join(complement(converse(top)),complement(composition(A,top))))),
inference(paramod,[status(thm)],[c_1185,c_3488]) ).
cnf(c_3490,plain,
composition(converse(A),top) = composition(complement(join(complement(converse(A)),complement(top))),complement(join(complement(converse(top)),complement(composition(A,top))))),
inference(paramod,[status(thm)],[c_558,c_3489]) ).
cnf(c_3491,plain,
composition(converse(A),top) = composition(complement(join(complement(converse(A)),zero)),complement(join(complement(converse(top)),complement(composition(A,top))))),
inference(paramod,[status(thm)],[c_22,c_3490]) ).
cnf(c_3492,plain,
composition(converse(A),top) = composition(complement(join(zero,complement(converse(A)))),complement(join(complement(converse(top)),complement(composition(A,top))))),
inference(paramod,[status(thm)],[c_1,c_3491]) ).
cnf(c_3493,plain,
composition(converse(A),top) = composition(complement(complement(converse(A))),complement(join(complement(converse(top)),complement(composition(A,top))))),
inference(paramod,[status(thm)],[c_257,c_3492]) ).
cnf(c_3494,plain,
composition(converse(A),top) = composition(converse(A),complement(join(complement(converse(top)),complement(composition(A,top))))),
inference(paramod,[status(thm)],[c_159,c_3493]) ).
cnf(c_3495,plain,
composition(converse(A),top) = composition(converse(A),complement(join(complement(top),complement(composition(A,top))))),
inference(paramod,[status(thm)],[c_339,c_3494]) ).
cnf(c_3496,plain,
composition(converse(A),top) = composition(converse(A),complement(join(zero,complement(composition(A,top))))),
inference(paramod,[status(thm)],[c_22,c_3495]) ).
cnf(c_3497,plain,
composition(converse(A),top) = composition(converse(A),complement(complement(composition(A,top)))),
inference(paramod,[status(thm)],[c_257,c_3496]) ).
cnf(c_3498,plain,
composition(converse(A),top) = composition(converse(A),composition(A,top)),
inference(paramod,[status(thm)],[c_159,c_3497]) ).
cnf(c_1777,plain,
composition(converse(A),composition(A,top)) = composition(converse(A),top),
inference(copy,[status(thm)],[c_3498]) ).
cnf(c_3499,plain,
join(composition(sk1,top),composition(converse(sk1),top)) = composition(sk1,top),
inference(paramod,[status(thm)],[c_1777,c_729]) ).
cnf(c_1844,plain,
composition(join(sk1,converse(sk1)),top) = composition(sk1,top),
inference(paramod,[status(thm)],[c_11,c_3499]) ).
cnf(c_3500,plain,
join(composition(converse(sk1),top),composition(sk1,top)) = composition(converse(sk1),top),
inference(paramod,[status(thm)],[c_1572,c_746]) ).
cnf(c_3501,plain,
join(composition(sk1,top),composition(converse(sk1),top)) = composition(converse(sk1),top),
inference(paramod,[status(thm)],[c_1,c_3500]) ).
cnf(c_3502,plain,
composition(join(sk1,converse(sk1)),top) = composition(converse(sk1),top),
inference(paramod,[status(thm)],[c_11,c_3501]) ).
cnf(c_3503,plain,
composition(sk1,top) = composition(converse(sk1),top),
inference(paramod,[status(thm)],[c_1844,c_3502]) ).
cnf(c_2105,plain,
composition(converse(sk1),top) = composition(sk1,top),
inference(copy,[status(thm)],[c_3503]) ).
cnf(c_3504,plain,
composition(converse(top),converse(converse(sk1))) = converse(composition(sk1,top)),
inference(paramod,[status(thm)],[c_2105,c_16]) ).
cnf(c_3505,plain,
composition(top,converse(converse(sk1))) = converse(composition(sk1,top)),
inference(paramod,[status(thm)],[c_339,c_3504]) ).
cnf(c_3506,plain,
composition(top,sk1) = converse(composition(sk1,top)),
inference(paramod,[status(thm)],[c_12,c_3505]) ).
cnf(c_3507,plain,
composition(top,sk1) = composition(top,converse(sk1)),
inference(paramod,[status(thm)],[c_349,c_3506]) ).
cnf(c_2127,plain,
composition(top,converse(sk1)) = composition(top,sk1),
inference(copy,[status(thm)],[c_3507]) ).
cnf(c_3508,plain,
join(complement(converse(sk1)),composition(converse(top),complement(composition(top,sk1)))) = complement(converse(sk1)),
inference(paramod,[status(thm)],[c_2127,c_18]) ).
cnf(c_3509,plain,
join(complement(converse(sk1)),composition(top,complement(composition(top,sk1)))) = complement(converse(sk1)),
inference(paramod,[status(thm)],[c_339,c_3508]) ).
cnf(c_2196,plain,
join(complement(converse(sk1)),complement(composition(top,sk1))) = complement(converse(sk1)),
inference(paramod,[status(thm)],[c_690,c_3509]) ).
cnf(c_3510,plain,
join(complement(complement(converse(sk1))),composition(complement(join(complement(top),complement(composition(converse(sk1),converse(sk1))))),complement(join(complement(sk1),complement(composition(converse(top),converse(sk1))))))) = composition(complement(join(complement(top),complement(composition(converse(sk1),converse(sk1))))),complement(join(complement(sk1),complement(composition(converse(top),converse(sk1)))))),
inference(paramod,[status(thm)],[c_2196,c_69]) ).
cnf(c_3511,plain,
join(converse(sk1),composition(complement(join(complement(top),complement(composition(converse(sk1),converse(sk1))))),complement(join(complement(sk1),complement(composition(converse(top),converse(sk1))))))) = composition(complement(join(complement(top),complement(composition(converse(sk1),converse(sk1))))),complement(join(complement(sk1),complement(composition(converse(top),converse(sk1)))))),
inference(paramod,[status(thm)],[c_159,c_3510]) ).
cnf(c_3512,plain,
join(converse(sk1),composition(complement(join(zero,complement(composition(converse(sk1),converse(sk1))))),complement(join(complement(sk1),complement(composition(converse(top),converse(sk1))))))) = composition(complement(join(complement(top),complement(composition(converse(sk1),converse(sk1))))),complement(join(complement(sk1),complement(composition(converse(top),converse(sk1)))))),
inference(paramod,[status(thm)],[c_22,c_3511]) ).
cnf(c_3513,plain,
join(converse(sk1),composition(complement(join(zero,complement(converse(composition(sk1,sk1))))),complement(join(complement(sk1),complement(composition(converse(top),converse(sk1))))))) = composition(complement(join(complement(top),complement(composition(converse(sk1),converse(sk1))))),complement(join(complement(sk1),complement(composition(converse(top),converse(sk1)))))),
inference(paramod,[status(thm)],[c_16,c_3512]) ).
cnf(c_3514,plain,
join(converse(sk1),composition(complement(complement(converse(composition(sk1,sk1)))),complement(join(complement(sk1),complement(composition(converse(top),converse(sk1))))))) = composition(complement(join(complement(top),complement(composition(converse(sk1),converse(sk1))))),complement(join(complement(sk1),complement(composition(converse(top),converse(sk1)))))),
inference(paramod,[status(thm)],[c_257,c_3513]) ).
cnf(c_3515,plain,
join(converse(sk1),composition(converse(composition(sk1,sk1)),complement(join(complement(sk1),complement(composition(converse(top),converse(sk1))))))) = composition(complement(join(complement(top),complement(composition(converse(sk1),converse(sk1))))),complement(join(complement(sk1),complement(composition(converse(top),converse(sk1)))))),
inference(paramod,[status(thm)],[c_159,c_3514]) ).
cnf(c_3516,plain,
join(converse(sk1),composition(converse(composition(sk1,sk1)),complement(join(complement(sk1),complement(composition(top,converse(sk1))))))) = composition(complement(join(complement(top),complement(composition(converse(sk1),converse(sk1))))),complement(join(complement(sk1),complement(composition(converse(top),converse(sk1)))))),
inference(paramod,[status(thm)],[c_339,c_3515]) ).
cnf(c_3517,plain,
join(converse(sk1),composition(converse(composition(sk1,sk1)),complement(join(complement(sk1),complement(composition(top,sk1)))))) = composition(complement(join(complement(top),complement(composition(converse(sk1),converse(sk1))))),complement(join(complement(sk1),complement(composition(converse(top),converse(sk1)))))),
inference(paramod,[status(thm)],[c_2127,c_3516]) ).
cnf(c_3518,plain,
join(converse(sk1),composition(converse(composition(sk1,sk1)),complement(complement(sk1)))) = composition(complement(join(complement(top),complement(composition(converse(sk1),converse(sk1))))),complement(join(complement(sk1),complement(composition(converse(top),converse(sk1)))))),
inference(paramod,[status(thm)],[c_696,c_3517]) ).
cnf(c_3519,plain,
join(converse(sk1),composition(converse(composition(sk1,sk1)),sk1)) = composition(complement(join(complement(top),complement(composition(converse(sk1),converse(sk1))))),complement(join(complement(sk1),complement(composition(converse(top),converse(sk1)))))),
inference(paramod,[status(thm)],[c_159,c_3518]) ).
cnf(c_3520,plain,
converse(sk1) = composition(complement(join(complement(top),complement(composition(converse(sk1),converse(sk1))))),complement(join(complement(sk1),complement(composition(converse(top),converse(sk1)))))),
inference(paramod,[status(thm)],[c_1545,c_3519]) ).
cnf(c_3521,plain,
converse(sk1) = composition(complement(join(zero,complement(composition(converse(sk1),converse(sk1))))),complement(join(complement(sk1),complement(composition(converse(top),converse(sk1)))))),
inference(paramod,[status(thm)],[c_22,c_3520]) ).
cnf(c_3522,plain,
converse(sk1) = composition(complement(join(zero,complement(converse(composition(sk1,sk1))))),complement(join(complement(sk1),complement(composition(converse(top),converse(sk1)))))),
inference(paramod,[status(thm)],[c_16,c_3521]) ).
cnf(c_3523,plain,
converse(sk1) = composition(complement(complement(converse(composition(sk1,sk1)))),complement(join(complement(sk1),complement(composition(converse(top),converse(sk1)))))),
inference(paramod,[status(thm)],[c_257,c_3522]) ).
cnf(c_3524,plain,
converse(sk1) = composition(converse(composition(sk1,sk1)),complement(join(complement(sk1),complement(composition(converse(top),converse(sk1)))))),
inference(paramod,[status(thm)],[c_159,c_3523]) ).
cnf(c_3525,plain,
converse(sk1) = composition(converse(composition(sk1,sk1)),complement(join(complement(sk1),complement(composition(top,converse(sk1)))))),
inference(paramod,[status(thm)],[c_339,c_3524]) ).
cnf(c_3526,plain,
converse(sk1) = composition(converse(composition(sk1,sk1)),complement(join(complement(sk1),complement(composition(top,sk1))))),
inference(paramod,[status(thm)],[c_2127,c_3525]) ).
cnf(c_3527,plain,
converse(sk1) = composition(converse(composition(sk1,sk1)),complement(complement(sk1))),
inference(paramod,[status(thm)],[c_696,c_3526]) ).
cnf(c_3528,plain,
converse(sk1) = composition(converse(composition(sk1,sk1)),sk1),
inference(paramod,[status(thm)],[c_159,c_3527]) ).
cnf(c_2742,plain,
composition(converse(composition(sk1,sk1)),sk1) = converse(sk1),
inference(copy,[status(thm)],[c_3528]) ).
cnf(c_3529,plain,
composition(converse(sk1),A) = composition(converse(composition(sk1,sk1)),composition(sk1,A)),
inference(paramod,[status(thm)],[c_2742,c_8]) ).
cnf(c_2748,plain,
composition(converse(composition(sk1,sk1)),composition(sk1,A)) = composition(converse(sk1),A),
inference(copy,[status(thm)],[c_3529]) ).
cnf(c_3530,plain,
composition(converse(sk1),composition(converse(converse(composition(sk1,sk1))),A)) = composition(converse(converse(sk1)),A),
inference(paramod,[status(thm)],[c_2742,c_48]) ).
cnf(c_3531,plain,
composition(converse(sk1),composition(composition(sk1,sk1),A)) = composition(converse(converse(sk1)),A),
inference(paramod,[status(thm)],[c_12,c_3530]) ).
cnf(c_3532,plain,
composition(converse(sk1),composition(sk1,composition(sk1,A))) = composition(converse(converse(sk1)),A),
inference(paramod,[status(thm)],[c_8,c_3531]) ).
cnf(c_2758,plain,
composition(converse(sk1),composition(sk1,composition(sk1,A))) = composition(sk1,A),
inference(paramod,[status(thm)],[c_12,c_3532]) ).
cnf(c_3533,plain,
join(composition(A,converse(converse(composition(sk1,sk1)))),converse(converse(sk1))) = composition(join(A,converse(sk1)),converse(converse(composition(sk1,sk1)))),
inference(paramod,[status(thm)],[c_2742,c_50]) ).
cnf(c_3534,plain,
join(composition(A,composition(sk1,sk1)),converse(converse(sk1))) = composition(join(A,converse(sk1)),converse(converse(composition(sk1,sk1)))),
inference(paramod,[status(thm)],[c_12,c_3533]) ).
cnf(c_3535,plain,
join(composition(A,composition(sk1,sk1)),sk1) = composition(join(A,converse(sk1)),converse(converse(composition(sk1,sk1)))),
inference(paramod,[status(thm)],[c_12,c_3534]) ).
cnf(c_3536,plain,
join(sk1,composition(A,composition(sk1,sk1))) = composition(join(A,converse(sk1)),converse(converse(composition(sk1,sk1)))),
inference(paramod,[status(thm)],[c_1,c_3535]) ).
cnf(c_3537,plain,
join(sk1,composition(A,composition(sk1,sk1))) = composition(join(A,converse(sk1)),composition(sk1,sk1)),
inference(paramod,[status(thm)],[c_12,c_3536]) ).
cnf(c_2760,plain,
composition(join(A,converse(sk1)),composition(sk1,sk1)) = join(sk1,composition(A,composition(sk1,sk1))),
inference(copy,[status(thm)],[c_3537]) ).
cnf(c_3538,plain,
join(converse(composition(sk1,sk1)),converse(sk1)) = converse(composition(sk1,sk1)),
inference(paramod,[status(thm)],[c_2742,c_884]) ).
cnf(c_3539,plain,
join(converse(sk1),converse(composition(sk1,sk1))) = converse(composition(sk1,sk1)),
inference(paramod,[status(thm)],[c_1,c_3538]) ).
cnf(c_3540,plain,
converse(join(sk1,composition(sk1,sk1))) = converse(composition(sk1,sk1)),
inference(paramod,[status(thm)],[c_14,c_3539]) ).
cnf(c_3541,plain,
converse(sk1) = converse(composition(sk1,sk1)),
inference(paramod,[status(thm)],[c_884,c_3540]) ).
cnf(c_2764,plain,
converse(composition(sk1,sk1)) = converse(sk1),
inference(copy,[status(thm)],[c_3541]) ).
cnf(c_2808,plain,
composition(converse(sk1),composition(sk1,A)) = composition(converse(sk1),A),
inference(paramod,[status(thm)],[c_2764,c_2748]) ).
cnf(c_2810,plain,
composition(converse(sk1),sk1) = converse(sk1),
inference(paramod,[status(thm)],[c_2764,c_2742]) ).
cnf(c_3542,plain,
composition(converse(sk1),composition(sk1,A)) = composition(sk1,A),
inference(paramod,[status(thm)],[c_2808,c_2758]) ).
cnf(c_2815,plain,
composition(converse(sk1),A) = composition(sk1,A),
inference(paramod,[status(thm)],[c_2808,c_3542]) ).
cnf(c_2828,plain,
composition(sk1,sk1) = converse(sk1),
inference(paramod,[status(thm)],[c_2815,c_2810]) ).
cnf(c_3543,plain,
converse(converse(sk1)) = converse(sk1),
inference(paramod,[status(thm)],[c_2828,c_2764]) ).
cnf(c_3544,plain,
sk1 = converse(sk1),
inference(paramod,[status(thm)],[c_12,c_3543]) ).
cnf(c_2848,plain,
converse(sk1) = sk1,
inference(copy,[status(thm)],[c_3544]) ).
cnf(c_3545,plain,
composition(join(A,sk1),composition(sk1,sk1)) = join(sk1,composition(A,composition(sk1,sk1))),
inference(paramod,[status(thm)],[c_2848,c_2760]) ).
cnf(c_3546,plain,
composition(join(A,sk1),converse(sk1)) = join(sk1,composition(A,composition(sk1,sk1))),
inference(paramod,[status(thm)],[c_2828,c_3545]) ).
cnf(c_3547,plain,
composition(join(A,sk1),sk1) = join(sk1,composition(A,composition(sk1,sk1))),
inference(paramod,[status(thm)],[c_2848,c_3546]) ).
cnf(c_3548,plain,
composition(join(A,sk1),sk1) = join(sk1,composition(A,converse(sk1))),
inference(paramod,[status(thm)],[c_2828,c_3547]) ).
cnf(c_3549,plain,
composition(join(A,sk1),sk1) = join(sk1,composition(A,sk1)),
inference(paramod,[status(thm)],[c_2848,c_3548]) ).
cnf(c_3550,plain,
composition(join(A,sk1),sk1) = composition(join(one,A),sk1),
inference(paramod,[status(thm)],[c_650,c_3549]) ).
cnf(c_2849,plain,
composition(join(one,A),sk1) = composition(join(A,sk1),sk1),
inference(copy,[status(thm)],[c_3550]) ).
cnf(c_3551,plain,
composition(sk1,converse(A)) = converse(composition(A,sk1)),
inference(paramod,[status(thm)],[c_2848,c_16]) ).
cnf(c_2906,plain,
converse(composition(A,sk1)) = composition(sk1,converse(A)),
inference(copy,[status(thm)],[c_3551]) ).
cnf(c_3552,plain,
join(join(A,sk1),composition(join(one,A),sk1)) = join(A,sk1),
inference(paramod,[status(thm)],[c_2849,c_884]) ).
cnf(c_3553,plain,
join(A,join(sk1,composition(join(one,A),sk1))) = join(A,sk1),
inference(paramod,[status(thm)],[c_3,c_3552]) ).
cnf(c_3554,plain,
join(A,join(sk1,composition(A,sk1))) = join(A,sk1),
inference(paramod,[status(thm)],[c_753,c_3553]) ).
cnf(c_3087,plain,
join(A,composition(join(one,A),sk1)) = join(A,sk1),
inference(paramod,[status(thm)],[c_650,c_3554]) ).
cnf(c_3555,plain,
converse(join(converse(A),sk1)) = join(A,converse(composition(join(one,converse(A)),sk1))),
inference(paramod,[status(thm)],[c_3087,c_46]) ).
cnf(c_3556,plain,
converse(join(sk1,converse(A))) = join(A,converse(composition(join(one,converse(A)),sk1))),
inference(paramod,[status(thm)],[c_1,c_3555]) ).
cnf(c_3557,plain,
join(converse(sk1),A) = join(A,converse(composition(join(one,converse(A)),sk1))),
inference(paramod,[status(thm)],[c_47,c_3556]) ).
cnf(c_3558,plain,
join(sk1,A) = join(A,converse(composition(join(one,converse(A)),sk1))),
inference(paramod,[status(thm)],[c_2848,c_3557]) ).
cnf(c_3559,plain,
join(sk1,A) = join(A,composition(sk1,converse(join(one,converse(A))))),
inference(paramod,[status(thm)],[c_2906,c_3558]) ).
cnf(c_3560,plain,
join(sk1,A) = join(A,composition(sk1,join(converse(one),A))),
inference(paramod,[status(thm)],[c_47,c_3559]) ).
cnf(c_3561,plain,
join(sk1,A) = join(A,composition(sk1,join(one,A))),
inference(paramod,[status(thm)],[c_649,c_3560]) ).
cnf(c_3219,plain,
join(A,composition(sk1,join(one,A))) = join(sk1,A),
inference(copy,[status(thm)],[c_3561]) ).
cnf(c_3302,plain,
join(complement(one),composition(sk1,top)) = join(sk1,complement(one)),
inference(paramod,[status(thm)],[c_20,c_3219]) ).
cnf(c_3562,plain,
( join(complement(join(sk1,complement(one))),complement(join(complement(one),composition(sk1,top)))) != complement(join(sk1,complement(one)))
| join(complement(join(sk1,complement(one))),complement(join(sk1,complement(one)))) != complement(join(complement(one),composition(sk1,top))) ),
inference(paramod,[status(thm)],[c_3302,c_163]) ).
cnf(c_3563,plain,
( join(complement(join(sk1,complement(one))),complement(join(complement(one),composition(sk1,top)))) != complement(join(sk1,complement(one)))
| complement(join(sk1,complement(one))) != complement(join(complement(one),composition(sk1,top))) ),
inference(paramod,[status(thm)],[c_281,c_3562]) ).
cnf(c_3564,plain,
( join(complement(join(sk1,complement(one))),complement(join(complement(one),composition(sk1,top)))) != complement(join(sk1,complement(one)))
| complement(join(sk1,complement(one))) != complement(join(sk1,complement(one))) ),
inference(paramod,[status(thm)],[c_3302,c_3563]) ).
cnf(c_3565,plain,
( join(complement(join(sk1,complement(one))),complement(join(sk1,complement(one)))) != complement(join(sk1,complement(one)))
| complement(join(sk1,complement(one))) != complement(join(sk1,complement(one))) ),
inference(paramod,[status(thm)],[c_3302,c_3564]) ).
cnf(c_3566,plain,
( complement(join(sk1,complement(one))) != complement(join(sk1,complement(one)))
| complement(join(sk1,complement(one))) != complement(join(sk1,complement(one))) ),
inference(paramod,[status(thm)],[c_281,c_3565]) ).
cnf(c_3567,plain,
complement(join(sk1,complement(one))) != complement(join(sk1,complement(one))),
inference(copy,[status(thm)],[c_3566]) ).
cnf(c_3326,plain,
$false,
inference(copy,[status(thm)],[c_3567]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : REL027-4 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.20/0.44 % Computer : n008.cluster.edu
% 0.20/0.44 % Model : x86_64 x86_64
% 0.20/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.20/0.44 % Memory : 8046.5625MB
% 0.20/0.44 % OS : Linux 6.8.0-71-generic
% 0.20/0.44 % CPULimit : 300
% 0.20/0.44 % WCLimit : 300
% 0.20/0.44 % DateTime : Sat Sep 26 05:33:54 UTC 2026
% 0.20/0.44 % CPUTime :
% 0.20/0.44 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.20/0.44 % Process 2880450 was started by sandbox on n008,
% 0.20/0.44 % Sat Sep 26 05:33:54 2026
% 0.20/0.44 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.20/0.45
% 0.20/0.45 % From the command line: assign(max_seconds, 300).
% 13.51/2.42
% 13.51/2.42 % SZS status Unsatisfiable for theBenchmark
% 13.51/2.42
% 13.51/2.42 % Proof 1 at 1.51 (+ 0.41) seconds.
% 13.51/2.42 % Length of proof is 125.
% 13.51/2.42 % Level of proof is 32.
% 13.51/2.42 % Maximum clause weight is 99.000.
% 13.51/2.42 % Given clauses 280.
% 13.51/2.42
% 13.51/2.42 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------