%------------------------------------------------------------------------------
% 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 : n001.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 : Theorem 10.20s 3.24s
% Output : CNFRefutation 10.20s
% Verified :
% SZS Type : Refutation
% Derivation depth : 126
% Number of leaves : 15
% Syntax : Number of formulae : 368 ( 334 unt; 0 def)
% Number of atoms : 406 ( 405 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 104 ( 66 ~; 32 |; 4 &)
% ( 0 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 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 : 407 ( 34 sgn 30 !; 1 ?)
% Comments :
%------------------------------------------------------------------------------
fof(maddux1_join_commutativity,axiom,
! [X0,X1] : join(X0,X1) = join(X1,X0),
file('theBenchmark.p',maddux1_join_commutativity) ).
fof(maddux2_join_associativity,axiom,
! [X0,X1,X2] : join(X0,join(X1,X2)) = join(join(X0,X1),X2),
file('theBenchmark.p',maddux2_join_associativity) ).
fof(maddux3_a_kind_of_de_Morgan,axiom,
! [X0,X1] : X0 = join(complement(join(complement(X0),complement(X1))),complement(join(complement(X0),X1))),
file('theBenchmark.p',maddux3_a_kind_of_de_Morgan) ).
fof(maddux4_definiton_of_meet,axiom,
! [X0,X1] : meet(X0,X1) = complement(join(complement(X0),complement(X1))),
file('theBenchmark.p',maddux4_definiton_of_meet) ).
fof(composition_associativity,axiom,
! [X0,X1,X2] : composition(X0,composition(X1,X2)) = composition(composition(X0,X1),X2),
file('theBenchmark.p',composition_associativity) ).
fof(composition_identity,axiom,
! [X0] : composition(X0,one) = X0,
file('theBenchmark.p',composition_identity) ).
fof(composition_distributivity,axiom,
! [X0,X1,X2] : composition(join(X0,X1),X2) = join(composition(X0,X2),composition(X1,X2)),
file('theBenchmark.p',composition_distributivity) ).
fof(converse_idempotence,axiom,
! [X0] : converse(converse(X0)) = X0,
file('theBenchmark.p',converse_idempotence) ).
fof(converse_additivity,axiom,
! [X0,X1] : converse(join(X0,X1)) = join(converse(X0),converse(X1)),
file('theBenchmark.p',converse_additivity) ).
fof(converse_multiplicativity,axiom,
! [X0,X1] : converse(composition(X0,X1)) = composition(converse(X1),converse(X0)),
file('theBenchmark.p',converse_multiplicativity) ).
fof(converse_cancellativity,axiom,
! [X0,X1] : join(composition(converse(X0),complement(composition(X0,X1))),complement(X1)) = complement(X1),
file('theBenchmark.p',converse_cancellativity) ).
fof(def_top,axiom,
! [X0] : top = join(X0,complement(X0)),
file('theBenchmark.p',def_top) ).
fof(def_zero,axiom,
! [X0] : zero = meet(X0,complement(X0)),
file('theBenchmark.p',def_zero) ).
fof(dedekind_law,axiom,
! [X0,X1,X2] : join(meet(composition(X0,X1),X2),composition(meet(X0,composition(X2,converse(X1))),meet(X1,composition(converse(X0),X2)))) = composition(meet(X0,composition(X2,converse(X1))),meet(X1,composition(converse(X0),X2))),
file('theBenchmark.p',dedekind_law) ).
fof(goals,conjecture,
! [X0] :
( join(X0,one) = one
=> ( join(meet(complement(X0),one),meet(complement(composition(X0,top)),one)) = meet(complement(composition(X0,top)),one)
& join(meet(complement(composition(X0,top)),one),meet(complement(X0),one)) = meet(complement(X0),one) ) ),
file('theBenchmark.p',goals) ).
fof(goals_neg,negated_conjecture,
~ ! [X0] :
( join(X0,one) = one
=> ( join(meet(complement(X0),one),meet(complement(composition(X0,top)),one)) = meet(complement(composition(X0,top)),one)
& join(meet(complement(composition(X0,top)),one),meet(complement(X0),one)) = meet(complement(X0),one) ) ),
inference(assume_negation,[status(cth)],[goals]) ).
cnf(c_18,plain,
join(A,B) = join(B,A),
inference(clausify,[status(thm)],[maddux1_join_commutativity]) ).
cnf(c_19,plain,
join(join(A,B),C) = join(A,join(B,C)),
inference(clausify,[status(thm)],[maddux2_join_associativity]) ).
cnf(c_20,plain,
join(complement(join(complement(A),complement(B))),complement(join(complement(A),B))) = A,
inference(clausify,[status(thm)],[maddux3_a_kind_of_de_Morgan]) ).
cnf(c_21,plain,
join(complement(join(complement(A),B)),complement(join(complement(A),complement(B)))) = A,
inference(paramod,[status(thm)],[c_18,c_20]) ).
cnf(c_22,plain,
meet(A,B) = complement(join(complement(A),complement(B))),
inference(clausify,[status(thm)],[maddux4_definiton_of_meet]) ).
cnf(c_23,plain,
composition(composition(A,B),C) = composition(A,composition(B,C)),
inference(clausify,[status(thm)],[composition_associativity]) ).
cnf(c_24,plain,
composition(A,one) = A,
inference(clausify,[status(thm)],[composition_identity]) ).
cnf(c_25,plain,
composition(join(A,B),C) = join(composition(A,C),composition(B,C)),
inference(clausify,[status(thm)],[composition_distributivity]) ).
cnf(c_26,plain,
join(composition(A,B),composition(C,B)) = composition(join(A,C),B),
inference(copy,[status(thm)],[c_25]) ).
cnf(c_27,plain,
converse(converse(A)) = A,
inference(clausify,[status(thm)],[converse_idempotence]) ).
cnf(c_28,plain,
converse(join(A,B)) = join(converse(A),converse(B)),
inference(clausify,[status(thm)],[converse_additivity]) ).
cnf(c_29,plain,
join(converse(A),converse(B)) = converse(join(A,B)),
inference(copy,[status(thm)],[c_28]) ).
cnf(c_30,plain,
converse(composition(A,B)) = composition(converse(B),converse(A)),
inference(clausify,[status(thm)],[converse_multiplicativity]) ).
cnf(c_31,plain,
composition(converse(A),converse(B)) = converse(composition(B,A)),
inference(copy,[status(thm)],[c_30]) ).
cnf(c_32,plain,
complement(A) = join(composition(converse(B),complement(composition(B,A))),complement(A)),
inference(clausify,[status(thm)],[converse_cancellativity]) ).
cnf(c_3341,plain,
complement(A) = join(complement(A),composition(converse(B),complement(composition(B,A)))),
inference(paramod,[status(thm)],[c_18,c_32]) ).
cnf(c_33,plain,
join(complement(A),composition(converse(B),complement(composition(B,A)))) = complement(A),
inference(copy,[status(thm)],[c_3341]) ).
cnf(c_34,plain,
join(A,complement(A)) = top,
inference(clausify,[status(thm)],[def_top]) ).
cnf(c_35,plain,
meet(A,complement(A)) = zero,
inference(clausify,[status(thm)],[def_zero]) ).
cnf(c_3342,plain,
complement(join(complement(A),complement(complement(A)))) = zero,
inference(paramod,[status(thm)],[c_22,c_35]) ).
cnf(c_36,plain,
complement(top) = zero,
inference(paramod,[status(thm)],[c_34,c_3342]) ).
cnf(c_37,plain,
composition(meet(A,composition(B,converse(C))),meet(C,composition(converse(A),B))) = join(meet(composition(A,C),B),composition(meet(A,composition(B,converse(C))),meet(C,composition(converse(A),B)))),
inference(clausify,[status(thm)],[dedekind_law]) ).
cnf(c_3343,plain,
composition(complement(join(complement(A),complement(composition(B,converse(C))))),meet(C,composition(converse(A),B))) = join(meet(composition(A,C),B),composition(meet(A,composition(B,converse(C))),meet(C,composition(converse(A),B)))),
inference(paramod,[status(thm)],[c_22,c_37]) ).
cnf(c_3344,plain,
composition(complement(join(complement(A),complement(composition(B,converse(C))))),complement(join(complement(C),complement(composition(converse(A),B))))) = join(meet(composition(A,C),B),composition(meet(A,composition(B,converse(C))),meet(C,composition(converse(A),B)))),
inference(paramod,[status(thm)],[c_22,c_3343]) ).
cnf(c_3345,plain,
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))),composition(meet(A,composition(B,converse(C))),meet(C,composition(converse(A),B)))),
inference(paramod,[status(thm)],[c_22,c_3344]) ).
cnf(c_3346,plain,
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))),composition(complement(join(complement(A),complement(composition(B,converse(C))))),meet(C,composition(converse(A),B)))),
inference(paramod,[status(thm)],[c_22,c_3345]) ).
cnf(c_3347,plain,
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))),composition(complement(join(complement(A),complement(composition(B,converse(C))))),complement(join(complement(C),complement(composition(converse(A),B)))))),
inference(paramod,[status(thm)],[c_22,c_3346]) ).
cnf(c_38,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(copy,[status(thm)],[c_3347]) ).
fof(nnf_17,plain,
? [X0] :
( ( meet(complement(composition(X0,top)),one) != join(meet(complement(X0),one),meet(complement(composition(X0,top)),one))
| meet(complement(X0),one) != join(meet(complement(composition(X0,top)),one),meet(complement(X0),one)) )
& join(X0,one) = one ),
inference(fof_nnf,[status(thm)],[goals_neg]) ).
fof(sk_goals_neg,plain,
( ( meet(complement(composition(sK0,top)),one) != join(meet(complement(sK0),one),meet(complement(composition(sK0,top)),one))
| meet(complement(sK0),one) != join(meet(complement(composition(sK0,top)),one),meet(complement(sK0),one)) )
& join(sK0,one) = one ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(X0,sK0)],[nnf_17]) ).
cnf(c_43,negated_conjecture,
join(sK0,one) = one,
inference(split_conjunct,[status(thm)],[sk_goals_neg]) ).
cnf(c_44,negated_conjecture,
join(one,sK0) = one,
inference(paramod,[status(thm)],[c_18,c_43]) ).
cnf(c_45,negated_conjecture,
( meet(complement(composition(sK0,top)),one) != join(meet(complement(sK0),one),meet(complement(composition(sK0,top)),one))
| meet(complement(sK0),one) != join(meet(complement(composition(sK0,top)),one),meet(complement(sK0),one)) ),
inference(split_conjunct,[status(thm)],[sk_goals_neg]) ).
cnf(c_3348,negated_conjecture,
( meet(complement(composition(sK0,top)),one) != join(meet(complement(sK0),one),meet(complement(composition(sK0,top)),one))
| complement(join(complement(complement(sK0)),complement(one))) != join(meet(complement(composition(sK0,top)),one),meet(complement(sK0),one)) ),
inference(paramod,[status(thm)],[c_22,c_45]) ).
cnf(c_3349,negated_conjecture,
( meet(complement(composition(sK0,top)),one) != join(meet(complement(sK0),one),meet(complement(composition(sK0,top)),one))
| complement(join(complement(one),complement(complement(sK0)))) != join(meet(complement(composition(sK0,top)),one),meet(complement(sK0),one)) ),
inference(paramod,[status(thm)],[c_18,c_3348]) ).
cnf(c_3350,negated_conjecture,
( meet(complement(composition(sK0,top)),one) != join(meet(complement(sK0),one),meet(complement(composition(sK0,top)),one))
| complement(join(complement(one),complement(complement(sK0)))) != join(complement(join(complement(complement(composition(sK0,top))),complement(one))),meet(complement(sK0),one)) ),
inference(paramod,[status(thm)],[c_22,c_3349]) ).
cnf(c_3351,negated_conjecture,
( meet(complement(composition(sK0,top)),one) != join(meet(complement(sK0),one),meet(complement(composition(sK0,top)),one))
| complement(join(complement(one),complement(complement(sK0)))) != join(complement(join(complement(one),complement(complement(composition(sK0,top))))),meet(complement(sK0),one)) ),
inference(paramod,[status(thm)],[c_18,c_3350]) ).
cnf(c_3352,negated_conjecture,
( meet(complement(composition(sK0,top)),one) != join(meet(complement(sK0),one),meet(complement(composition(sK0,top)),one))
| complement(join(complement(one),complement(complement(sK0)))) != join(complement(join(complement(one),complement(complement(composition(sK0,top))))),complement(join(complement(complement(sK0)),complement(one)))) ),
inference(paramod,[status(thm)],[c_22,c_3351]) ).
cnf(c_3353,negated_conjecture,
( meet(complement(composition(sK0,top)),one) != join(meet(complement(sK0),one),meet(complement(composition(sK0,top)),one))
| complement(join(complement(one),complement(complement(sK0)))) != join(complement(join(complement(one),complement(complement(composition(sK0,top))))),complement(join(complement(one),complement(complement(sK0))))) ),
inference(paramod,[status(thm)],[c_18,c_3352]) ).
cnf(c_3354,negated_conjecture,
( meet(complement(composition(sK0,top)),one) != join(meet(complement(sK0),one),meet(complement(composition(sK0,top)),one))
| complement(join(complement(one),complement(complement(sK0)))) != join(complement(join(complement(one),complement(complement(sK0)))),complement(join(complement(one),complement(complement(composition(sK0,top)))))) ),
inference(paramod,[status(thm)],[c_18,c_3353]) ).
cnf(c_3355,negated_conjecture,
( complement(join(complement(complement(composition(sK0,top))),complement(one))) != join(meet(complement(sK0),one),meet(complement(composition(sK0,top)),one))
| complement(join(complement(one),complement(complement(sK0)))) != join(complement(join(complement(one),complement(complement(sK0)))),complement(join(complement(one),complement(complement(composition(sK0,top)))))) ),
inference(paramod,[status(thm)],[c_22,c_3354]) ).
cnf(c_3356,negated_conjecture,
( complement(join(complement(one),complement(complement(composition(sK0,top))))) != join(meet(complement(sK0),one),meet(complement(composition(sK0,top)),one))
| complement(join(complement(one),complement(complement(sK0)))) != join(complement(join(complement(one),complement(complement(sK0)))),complement(join(complement(one),complement(complement(composition(sK0,top)))))) ),
inference(paramod,[status(thm)],[c_18,c_3355]) ).
cnf(c_3357,negated_conjecture,
( complement(join(complement(one),complement(complement(composition(sK0,top))))) != join(complement(join(complement(complement(sK0)),complement(one))),meet(complement(composition(sK0,top)),one))
| complement(join(complement(one),complement(complement(sK0)))) != join(complement(join(complement(one),complement(complement(sK0)))),complement(join(complement(one),complement(complement(composition(sK0,top)))))) ),
inference(paramod,[status(thm)],[c_22,c_3356]) ).
cnf(c_3358,negated_conjecture,
( complement(join(complement(one),complement(complement(composition(sK0,top))))) != join(complement(join(complement(one),complement(complement(sK0)))),meet(complement(composition(sK0,top)),one))
| complement(join(complement(one),complement(complement(sK0)))) != join(complement(join(complement(one),complement(complement(sK0)))),complement(join(complement(one),complement(complement(composition(sK0,top)))))) ),
inference(paramod,[status(thm)],[c_18,c_3357]) ).
cnf(c_3359,negated_conjecture,
( complement(join(complement(one),complement(complement(composition(sK0,top))))) != join(complement(join(complement(one),complement(complement(sK0)))),complement(join(complement(complement(composition(sK0,top))),complement(one))))
| complement(join(complement(one),complement(complement(sK0)))) != join(complement(join(complement(one),complement(complement(sK0)))),complement(join(complement(one),complement(complement(composition(sK0,top)))))) ),
inference(paramod,[status(thm)],[c_22,c_3358]) ).
cnf(c_3360,negated_conjecture,
( complement(join(complement(one),complement(complement(composition(sK0,top))))) != join(complement(join(complement(one),complement(complement(sK0)))),complement(join(complement(one),complement(complement(composition(sK0,top))))))
| complement(join(complement(one),complement(complement(sK0)))) != join(complement(join(complement(one),complement(complement(sK0)))),complement(join(complement(one),complement(complement(composition(sK0,top)))))) ),
inference(paramod,[status(thm)],[c_18,c_3359]) ).
cnf(c_3361,negated_conjecture,
( complement(join(complement(one),complement(complement(composition(sK0,top))))) != join(complement(join(complement(one),complement(complement(sK0)))),complement(join(complement(one),complement(complement(composition(sK0,top))))))
| join(complement(join(complement(one),complement(complement(sK0)))),complement(join(complement(one),complement(complement(composition(sK0,top)))))) != complement(join(complement(one),complement(complement(sK0)))) ),
inference(copy,[status(thm)],[c_3360]) ).
cnf(c_46,negated_conjecture,
( join(complement(join(complement(one),complement(complement(sK0)))),complement(join(complement(one),complement(complement(composition(sK0,top)))))) != complement(join(complement(one),complement(complement(composition(sK0,top)))))
| join(complement(join(complement(one),complement(complement(sK0)))),complement(join(complement(one),complement(complement(composition(sK0,top)))))) != complement(join(complement(one),complement(complement(sK0)))) ),
inference(copy,[status(thm)],[c_3361]) ).
cnf(c_50,plain,
join(complement(join(complement(A),B)),complement(join(complement(B),complement(A)))) = A,
inference(paramod,[status(thm)],[c_18,c_21]) ).
cnf(c_3362,plain,
join(A,B) = join(complement(join(complement(A),C)),join(complement(join(complement(A),complement(C))),B)),
inference(paramod,[status(thm)],[c_21,c_19]) ).
cnf(c_51,plain,
join(complement(join(complement(A),B)),join(complement(join(complement(A),complement(B))),C)) = join(A,C),
inference(copy,[status(thm)],[c_3362]) ).
cnf(c_3363,plain,
composition(A,B) = composition(A,composition(one,B)),
inference(paramod,[status(thm)],[c_24,c_23]) ).
cnf(c_55,plain,
composition(A,composition(one,B)) = composition(A,B),
inference(copy,[status(thm)],[c_3363]) ).
cnf(c_57,plain,
join(composition(A,composition(B,C)),composition(D,C)) = composition(join(composition(A,B),D),C),
inference(paramod,[status(thm)],[c_23,c_26]) ).
cnf(c_58,plain,
join(composition(A,B),composition(C,composition(D,B))) = composition(join(A,composition(C,D)),B),
inference(paramod,[status(thm)],[c_23,c_26]) ).
cnf(c_3364,plain,
join(A,converse(B)) = converse(join(converse(A),B)),
inference(paramod,[status(thm)],[c_27,c_29]) ).
cnf(c_60,plain,
converse(join(converse(A),B)) = join(A,converse(B)),
inference(copy,[status(thm)],[c_3364]) ).
cnf(c_3365,plain,
join(converse(A),B) = converse(join(A,converse(B))),
inference(paramod,[status(thm)],[c_27,c_29]) ).
cnf(c_61,plain,
converse(join(A,converse(B))) = join(converse(A),B),
inference(copy,[status(thm)],[c_3365]) ).
cnf(c_3366,plain,
composition(converse(composition(A,B)),C) = composition(converse(B),composition(converse(A),C)),
inference(paramod,[status(thm)],[c_31,c_23]) ).
cnf(c_62,plain,
composition(converse(A),composition(converse(B),C)) = composition(converse(composition(B,A)),C),
inference(copy,[status(thm)],[c_3366]) ).
cnf(c_64,plain,
join(composition(A,converse(B)),converse(composition(B,C))) = composition(join(A,converse(C)),converse(B)),
inference(paramod,[status(thm)],[c_31,c_26]) ).
cnf(c_3367,plain,
composition(converse(A),B) = converse(composition(converse(B),A)),
inference(paramod,[status(thm)],[c_27,c_31]) ).
cnf(c_66,plain,
converse(composition(converse(A),B)) = composition(converse(B),A),
inference(copy,[status(thm)],[c_3367]) ).
cnf(c_68,plain,
join(complement(complement(A)),complement(join(complement(A),complement(composition(converse(B),complement(composition(B,A))))))) = A,
inference(paramod,[status(thm)],[c_33,c_21]) ).
cnf(c_3368,plain,
join(top,A) = join(B,join(complement(B),A)),
inference(paramod,[status(thm)],[c_34,c_19]) ).
cnf(c_74,plain,
join(A,join(complement(A),B)) = join(top,B),
inference(copy,[status(thm)],[c_3368]) ).
cnf(c_3369,plain,
join(join(A,B),complement(B)) = join(A,top),
inference(paramod,[status(thm)],[c_34,c_19]) ).
cnf(c_76,plain,
join(complement(A),join(B,A)) = join(B,top),
inference(paramod,[status(thm)],[c_18,c_3369]) ).
cnf(c_3370,plain,
join(complement(top),complement(join(complement(A),complement(complement(complement(A)))))) = A,
inference(paramod,[status(thm)],[c_34,c_21]) ).
cnf(c_77,plain,
join(zero,complement(join(complement(A),complement(complement(complement(A)))))) = A,
inference(paramod,[status(thm)],[c_36,c_3370]) ).
cnf(c_3371,plain,
join(zero,composition(converse(A),complement(composition(A,top)))) = complement(top),
inference(paramod,[status(thm)],[c_36,c_33]) ).
cnf(c_81,plain,
join(zero,composition(converse(A),complement(composition(A,top)))) = zero,
inference(paramod,[status(thm)],[c_36,c_3371]) ).
cnf(c_83,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_18,c_38]) ).
cnf(c_3372,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_27,c_38]) ).
cnf(c_89,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_27,c_3372]) ).
cnf(c_3373,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_31,c_38]) ).
cnf(c_3374,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_27,c_3373]) ).
cnf(c_3375,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_27,c_3374]) ).
cnf(c_3376,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_27,c_3375]) ).
cnf(c_91,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_27,c_3376]) ).
cnf(c_3377,plain,
join(one,A) = join(one,join(sK0,A)),
inference(paramod,[status(thm)],[c_44,c_19]) ).
cnf(c_114,plain,
join(one,join(sK0,A)) = join(one,A),
inference(copy,[status(thm)],[c_3377]) ).
cnf(c_3378,plain,
join(complement(join(complement(complement(A)),A)),complement(top)) = complement(A),
inference(paramod,[status(thm)],[c_34,c_50]) ).
cnf(c_3379,plain,
join(complement(join(A,complement(complement(A)))),complement(top)) = complement(A),
inference(paramod,[status(thm)],[c_18,c_3378]) ).
cnf(c_3380,plain,
join(complement(join(A,complement(complement(A)))),zero) = complement(A),
inference(paramod,[status(thm)],[c_36,c_3379]) ).
cnf(c_168,plain,
join(zero,complement(join(A,complement(complement(A))))) = complement(A),
inference(paramod,[status(thm)],[c_18,c_3380]) ).
cnf(c_174,plain,
complement(complement(A)) = A,
inference(paramod,[status(thm)],[c_168,c_77]) ).
cnf(c_175,plain,
join(zero,complement(join(A,A))) = complement(A),
inference(paramod,[status(thm)],[c_174,c_168]) ).
cnf(c_177,plain,
join(A,complement(join(complement(A),complement(composition(converse(B),complement(composition(B,A))))))) = A,
inference(paramod,[status(thm)],[c_174,c_68]) ).
cnf(c_3381,negated_conjecture,
( join(complement(join(complement(one),complement(complement(sK0)))),complement(join(complement(one),complement(complement(composition(sK0,top)))))) != complement(join(complement(one),complement(complement(composition(sK0,top)))))
| join(complement(join(complement(one),sK0)),complement(join(complement(one),complement(complement(composition(sK0,top)))))) != complement(join(complement(one),complement(complement(sK0)))) ),
inference(paramod,[status(thm)],[c_174,c_46]) ).
cnf(c_3382,negated_conjecture,
( join(complement(join(complement(one),complement(complement(sK0)))),complement(join(complement(one),complement(complement(composition(sK0,top)))))) != complement(join(complement(one),complement(complement(composition(sK0,top)))))
| join(complement(join(sK0,complement(one))),complement(join(complement(one),complement(complement(composition(sK0,top)))))) != complement(join(complement(one),complement(complement(sK0)))) ),
inference(paramod,[status(thm)],[c_18,c_3381]) ).
cnf(c_3383,negated_conjecture,
( join(complement(join(complement(one),complement(complement(sK0)))),complement(join(complement(one),complement(complement(composition(sK0,top)))))) != complement(join(complement(one),complement(complement(composition(sK0,top)))))
| join(complement(join(sK0,complement(one))),complement(join(complement(one),composition(sK0,top)))) != complement(join(complement(one),complement(complement(sK0)))) ),
inference(paramod,[status(thm)],[c_174,c_3382]) ).
cnf(c_3384,negated_conjecture,
( join(complement(join(complement(one),complement(complement(sK0)))),complement(join(complement(one),complement(complement(composition(sK0,top)))))) != complement(join(complement(one),complement(complement(composition(sK0,top)))))
| join(complement(join(sK0,complement(one))),complement(join(complement(one),composition(sK0,top)))) != complement(join(complement(one),sK0)) ),
inference(paramod,[status(thm)],[c_174,c_3383]) ).
cnf(c_3385,negated_conjecture,
( join(complement(join(complement(one),complement(complement(sK0)))),complement(join(complement(one),complement(complement(composition(sK0,top)))))) != complement(join(complement(one),complement(complement(composition(sK0,top)))))
| join(complement(join(sK0,complement(one))),complement(join(complement(one),composition(sK0,top)))) != complement(join(sK0,complement(one))) ),
inference(paramod,[status(thm)],[c_18,c_3384]) ).
cnf(c_3386,negated_conjecture,
( join(complement(join(complement(one),sK0)),complement(join(complement(one),complement(complement(composition(sK0,top)))))) != complement(join(complement(one),complement(complement(composition(sK0,top)))))
| join(complement(join(sK0,complement(one))),complement(join(complement(one),composition(sK0,top)))) != complement(join(sK0,complement(one))) ),
inference(paramod,[status(thm)],[c_174,c_3385]) ).
cnf(c_3387,negated_conjecture,
( join(complement(join(sK0,complement(one))),complement(join(complement(one),complement(complement(composition(sK0,top)))))) != complement(join(complement(one),complement(complement(composition(sK0,top)))))
| join(complement(join(sK0,complement(one))),complement(join(complement(one),composition(sK0,top)))) != complement(join(sK0,complement(one))) ),
inference(paramod,[status(thm)],[c_18,c_3386]) ).
cnf(c_3388,negated_conjecture,
( join(complement(join(sK0,complement(one))),complement(join(complement(one),composition(sK0,top)))) != complement(join(complement(one),complement(complement(composition(sK0,top)))))
| join(complement(join(sK0,complement(one))),complement(join(complement(one),composition(sK0,top)))) != complement(join(sK0,complement(one))) ),
inference(paramod,[status(thm)],[c_174,c_3387]) ).
cnf(c_178,negated_conjecture,
( join(complement(join(sK0,complement(one))),complement(join(complement(one),composition(sK0,top)))) != complement(join(complement(one),composition(sK0,top)))
| join(complement(join(sK0,complement(one))),complement(join(complement(one),composition(sK0,top)))) != complement(join(sK0,complement(one))) ),
inference(paramod,[status(thm)],[c_174,c_3388]) ).
cnf(c_181,plain,
complement(zero) = top,
inference(paramod,[status(thm)],[c_36,c_174]) ).
cnf(c_3389,plain,
join(complement(composition(converse(A),complement(composition(A,B)))),complement(B)) = join(complement(B),top),
inference(paramod,[status(thm)],[c_33,c_76]) ).
cnf(c_3390,plain,
join(complement(B),complement(composition(converse(A),complement(composition(A,B))))) = join(complement(B),top),
inference(paramod,[status(thm)],[c_18,c_3389]) ).
cnf(c_208,plain,
join(complement(A),complement(composition(converse(B),complement(composition(B,A))))) = join(top,complement(A)),
inference(paramod,[status(thm)],[c_18,c_3390]) ).
cnf(c_3391,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_38,c_76]) ).
cnf(c_3392,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_18,c_3391]) ).
cnf(c_3393,plain,
top = join(complement(join(complement(composition(A,C)),complement(B))),top),
inference(paramod,[status(thm)],[c_34,c_3392]) ).
cnf(c_3394,plain,
top = join(top,complement(join(complement(composition(A,C)),complement(B)))),
inference(paramod,[status(thm)],[c_18,c_3393]) ).
cnf(c_209,plain,
join(top,complement(join(complement(composition(A,B)),complement(C)))) = top,
inference(copy,[status(thm)],[c_3394]) ).
cnf(c_3395,plain,
join(complement(join(A,B)),join(A,top)) = join(complement(B),top),
inference(paramod,[status(thm)],[c_76,c_76]) ).
cnf(c_3396,plain,
join(join(A,top),complement(join(A,B))) = join(complement(B),top),
inference(paramod,[status(thm)],[c_18,c_3395]) ).
cnf(c_3397,plain,
join(A,join(top,complement(join(A,B)))) = join(complement(B),top),
inference(paramod,[status(thm)],[c_19,c_3396]) ).
cnf(c_217,plain,
join(A,join(top,complement(join(A,B)))) = join(top,complement(B)),
inference(paramod,[status(thm)],[c_18,c_3397]) ).
cnf(c_218,plain,
join(A,complement(join(top,complement(A)))) = A,
inference(paramod,[status(thm)],[c_208,c_177]) ).
cnf(c_3398,plain,
join(complement(join(complement(A),B)),top) = join(A,complement(complement(join(complement(A),complement(B))))),
inference(paramod,[status(thm)],[c_34,c_51]) ).
cnf(c_3399,plain,
join(top,complement(join(complement(A),B))) = join(A,complement(complement(join(complement(A),complement(B))))),
inference(paramod,[status(thm)],[c_18,c_3398]) ).
cnf(c_3400,plain,
join(top,complement(join(complement(A),B))) = join(A,join(complement(A),complement(B))),
inference(paramod,[status(thm)],[c_174,c_3399]) ).
cnf(c_225,plain,
join(top,complement(join(complement(A),B))) = join(top,complement(B)),
inference(paramod,[status(thm)],[c_74,c_3400]) ).
cnf(c_3401,plain,
join(top,complement(complement(C))) = top,
inference(paramod,[status(thm)],[c_225,c_209]) ).
cnf(c_240,plain,
join(top,A) = top,
inference(paramod,[status(thm)],[c_174,c_3401]) ).
cnf(c_3402,plain,
join(A,complement(top)) = A,
inference(paramod,[status(thm)],[c_240,c_218]) ).
cnf(c_245,plain,
join(A,zero) = A,
inference(paramod,[status(thm)],[c_36,c_3402]) ).
cnf(c_3403,plain,
join(A,top) = join(top,complement(B)),
inference(paramod,[status(thm)],[c_240,c_217]) ).
cnf(c_246,plain,
join(A,top) = top,
inference(paramod,[status(thm)],[c_240,c_3403]) ).
cnf(c_3404,plain,
A = join(zero,A),
inference(paramod,[status(thm)],[c_245,c_18]) ).
cnf(c_271,plain,
join(zero,A) = A,
inference(copy,[status(thm)],[c_3404]) ).
cnf(c_275,plain,
complement(join(A,A)) = complement(A),
inference(paramod,[status(thm)],[c_271,c_175]) ).
cnf(c_283,plain,
composition(converse(A),complement(composition(A,top))) = zero,
inference(paramod,[status(thm)],[c_271,c_81]) ).
cnf(c_3405,plain,
complement(complement(A)) = join(A,A),
inference(paramod,[status(thm)],[c_275,c_174]) ).
cnf(c_3406,plain,
A = join(A,A),
inference(paramod,[status(thm)],[c_174,c_3405]) ).
cnf(c_295,plain,
join(A,A) = A,
inference(copy,[status(thm)],[c_3406]) ).
cnf(c_3407,plain,
join(A,B) = join(A,join(A,B)),
inference(paramod,[status(thm)],[c_295,c_19]) ).
cnf(c_301,plain,
join(A,join(A,B)) = join(A,B),
inference(copy,[status(thm)],[c_3407]) ).
cnf(c_3408,plain,
converse(top) = join(A,converse(top)),
inference(paramod,[status(thm)],[c_246,c_60]) ).
cnf(c_339,plain,
join(A,converse(top)) = converse(top),
inference(copy,[status(thm)],[c_3408]) ).
cnf(c_353,plain,
converse(top) = top,
inference(paramod,[status(thm)],[c_339,c_240]) ).
cnf(c_3409,plain,
composition(top,converse(A)) = converse(composition(A,top)),
inference(paramod,[status(thm)],[c_353,c_31]) ).
cnf(c_363,plain,
converse(composition(A,top)) = composition(top,converse(A)),
inference(copy,[status(thm)],[c_3409]) ).
cnf(c_3410,plain,
composition(converse(A),top) = converse(composition(top,A)),
inference(paramod,[status(thm)],[c_353,c_31]) ).
cnf(c_364,plain,
converse(composition(top,A)) = composition(converse(A),top),
inference(copy,[status(thm)],[c_3410]) ).
cnf(c_365,plain,
join(complement(A),composition(top,complement(composition(top,A)))) = complement(A),
inference(paramod,[status(thm)],[c_353,c_33]) ).
cnf(c_368,plain,
composition(top,complement(composition(top,top))) = zero,
inference(paramod,[status(thm)],[c_353,c_283]) ).
cnf(c_3411,plain,
converse(top) = composition(converse(one),top),
inference(paramod,[status(thm)],[c_24,c_364]) ).
cnf(c_3412,plain,
top = composition(converse(one),top),
inference(paramod,[status(thm)],[c_353,c_3411]) ).
cnf(c_393,plain,
composition(converse(one),top) = top,
inference(copy,[status(thm)],[c_3412]) ).
cnf(c_3413,plain,
join(top,composition(A,top)) = composition(join(converse(one),A),top),
inference(paramod,[status(thm)],[c_393,c_26]) ).
cnf(c_3414,plain,
top = composition(join(converse(one),A),top),
inference(paramod,[status(thm)],[c_240,c_3413]) ).
cnf(c_408,plain,
composition(join(converse(one),A),top) = top,
inference(copy,[status(thm)],[c_3414]) ).
cnf(c_3415,plain,
join(zero,composition(A,complement(composition(top,top)))) = composition(join(top,A),complement(composition(top,top))),
inference(paramod,[status(thm)],[c_368,c_26]) ).
cnf(c_3416,plain,
composition(A,complement(composition(top,top))) = composition(join(top,A),complement(composition(top,top))),
inference(paramod,[status(thm)],[c_271,c_3415]) ).
cnf(c_3417,plain,
composition(A,complement(composition(top,top))) = composition(top,complement(composition(top,top))),
inference(paramod,[status(thm)],[c_240,c_3416]) ).
cnf(c_539,plain,
composition(A,complement(composition(top,top))) = zero,
inference(paramod,[status(thm)],[c_368,c_3417]) ).
cnf(c_3418,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_368,c_57]) ).
cnf(c_3419,plain,
join(composition(A,zero),zero) = composition(join(composition(A,top),B),complement(composition(top,top))),
inference(paramod,[status(thm)],[c_539,c_3418]) ).
cnf(c_3420,plain,
join(zero,composition(A,zero)) = composition(join(composition(A,top),B),complement(composition(top,top))),
inference(paramod,[status(thm)],[c_18,c_3419]) ).
cnf(c_3421,plain,
composition(A,zero) = composition(join(composition(A,top),B),complement(composition(top,top))),
inference(paramod,[status(thm)],[c_271,c_3420]) ).
cnf(c_541,plain,
composition(A,zero) = zero,
inference(paramod,[status(thm)],[c_539,c_3421]) ).
cnf(c_572,plain,
composition(top,top) = top,
inference(paramod,[status(thm)],[c_34,c_408]) ).
cnf(c_3422,plain,
composition(converse(A),zero) = composition(converse(composition(B,A)),complement(composition(B,top))),
inference(paramod,[status(thm)],[c_283,c_62]) ).
cnf(c_3423,plain,
zero = composition(converse(composition(B,A)),complement(composition(B,top))),
inference(paramod,[status(thm)],[c_541,c_3422]) ).
cnf(c_580,plain,
composition(converse(composition(A,B)),complement(composition(A,top))) = zero,
inference(copy,[status(thm)],[c_3423]) ).
cnf(c_3424,plain,
composition(top,A) = composition(top,composition(top,A)),
inference(paramod,[status(thm)],[c_572,c_23]) ).
cnf(c_585,plain,
composition(top,composition(top,A)) = composition(top,A),
inference(copy,[status(thm)],[c_3424]) ).
cnf(c_3425,plain,
join(complement(composition(top,A)),composition(converse(top),complement(composition(top,A)))) = complement(composition(top,A)),
inference(paramod,[status(thm)],[c_585,c_33]) ).
cnf(c_591,plain,
join(complement(composition(top,A)),composition(top,complement(composition(top,A)))) = complement(composition(top,A)),
inference(paramod,[status(thm)],[c_353,c_3425]) ).
cnf(c_3426,plain,
converse(converse(A)) = composition(converse(one),A),
inference(paramod,[status(thm)],[c_24,c_66]) ).
cnf(c_3427,plain,
A = composition(converse(one),A),
inference(paramod,[status(thm)],[c_27,c_3426]) ).
cnf(c_656,plain,
composition(converse(one),A) = A,
inference(copy,[status(thm)],[c_3427]) ).
cnf(c_3428,plain,
one = converse(one),
inference(paramod,[status(thm)],[c_656,c_24]) ).
cnf(c_663,plain,
converse(one) = one,
inference(copy,[status(thm)],[c_3428]) ).
cnf(c_3429,plain,
join(A,composition(B,A)) = composition(join(converse(one),B),A),
inference(paramod,[status(thm)],[c_656,c_26]) ).
cnf(c_3430,plain,
join(A,composition(B,A)) = composition(join(one,B),A),
inference(paramod,[status(thm)],[c_663,c_3429]) ).
cnf(c_664,plain,
composition(join(one,A),B) = join(B,composition(A,B)),
inference(copy,[status(thm)],[c_3430]) ).
cnf(c_3431,plain,
composition(converse(one),composition(one,A)) = A,
inference(paramod,[status(thm)],[c_656,c_55]) ).
cnf(c_3432,plain,
composition(one,composition(one,A)) = A,
inference(paramod,[status(thm)],[c_663,c_3431]) ).
cnf(c_680,plain,
composition(one,A) = A,
inference(paramod,[status(thm)],[c_55,c_3432]) ).
cnf(c_3433,plain,
composition(join(one,top),complement(composition(top,A))) = complement(composition(top,A)),
inference(paramod,[status(thm)],[c_664,c_591]) ).
cnf(c_704,plain,
composition(top,complement(composition(top,A))) = complement(composition(top,A)),
inference(paramod,[status(thm)],[c_246,c_3433]) ).
cnf(c_710,plain,
join(complement(A),complement(composition(top,A))) = complement(A),
inference(paramod,[status(thm)],[c_704,c_365]) ).
cnf(c_3434,plain,
join(one,converse(A)) = converse(join(one,A)),
inference(paramod,[status(thm)],[c_663,c_29]) ).
cnf(c_711,plain,
converse(join(one,A)) = join(one,converse(A)),
inference(copy,[status(thm)],[c_3434]) ).
cnf(c_3435,plain,
converse(one) = join(one,converse(sK0)),
inference(paramod,[status(thm)],[c_44,c_711]) ).
cnf(c_3436,plain,
one = join(one,converse(sK0)),
inference(paramod,[status(thm)],[c_663,c_3435]) ).
cnf(c_732,plain,
join(one,converse(sK0)) = one,
inference(copy,[status(thm)],[c_3436]) ).
cnf(c_3437,plain,
join(composition(one,A),composition(converse(sK0),A)) = composition(one,A),
inference(paramod,[status(thm)],[c_732,c_26]) ).
cnf(c_3438,plain,
join(A,composition(converse(sK0),A)) = composition(one,A),
inference(paramod,[status(thm)],[c_680,c_3437]) ).
cnf(c_743,plain,
join(A,composition(converse(sK0),A)) = A,
inference(paramod,[status(thm)],[c_680,c_3438]) ).
cnf(c_3439,plain,
composition(one,A) = join(A,composition(sK0,A)),
inference(paramod,[status(thm)],[c_44,c_664]) ).
cnf(c_3440,plain,
A = join(A,composition(sK0,A)),
inference(paramod,[status(thm)],[c_680,c_3439]) ).
cnf(c_760,plain,
join(A,composition(sK0,A)) = A,
inference(copy,[status(thm)],[c_3440]) ).
cnf(c_767,plain,
join(A,composition(join(one,B),A)) = join(A,composition(B,A)),
inference(paramod,[status(thm)],[c_664,c_301]) ).
cnf(c_3441,plain,
join(one,sK0) = join(one,composition(converse(sK0),sK0)),
inference(paramod,[status(thm)],[c_743,c_114]) ).
cnf(c_3442,plain,
one = join(one,composition(converse(sK0),sK0)),
inference(paramod,[status(thm)],[c_44,c_3441]) ).
cnf(c_896,plain,
join(one,composition(converse(sK0),sK0)) = one,
inference(copy,[status(thm)],[c_3442]) ).
cnf(c_3443,plain,
converse(converse(A)) = join(A,converse(composition(converse(sK0),converse(A)))),
inference(paramod,[status(thm)],[c_743,c_60]) ).
cnf(c_3444,plain,
A = join(A,converse(composition(converse(sK0),converse(A)))),
inference(paramod,[status(thm)],[c_27,c_3443]) ).
cnf(c_3445,plain,
A = join(A,converse(converse(composition(A,sK0)))),
inference(paramod,[status(thm)],[c_31,c_3444]) ).
cnf(c_3446,plain,
A = join(A,composition(A,sK0)),
inference(paramod,[status(thm)],[c_27,c_3445]) ).
cnf(c_898,plain,
join(A,composition(A,sK0)) = A,
inference(copy,[status(thm)],[c_3446]) ).
cnf(c_3447,plain,
join(composition(one,A),composition(composition(converse(sK0),sK0),A)) = composition(one,A),
inference(paramod,[status(thm)],[c_896,c_26]) ).
cnf(c_3448,plain,
join(A,composition(composition(converse(sK0),sK0),A)) = composition(one,A),
inference(paramod,[status(thm)],[c_680,c_3447]) ).
cnf(c_3449,plain,
join(A,composition(converse(sK0),composition(sK0,A))) = composition(one,A),
inference(paramod,[status(thm)],[c_23,c_3448]) ).
cnf(c_953,plain,
join(A,composition(converse(sK0),composition(sK0,A))) = A,
inference(paramod,[status(thm)],[c_680,c_3449]) ).
cnf(c_3450,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_580,c_33]) ).
cnf(c_3451,plain,
join(composition(A,top),composition(converse(converse(composition(A,B))),complement(zero))) = complement(complement(composition(A,top))),
inference(paramod,[status(thm)],[c_174,c_3450]) ).
cnf(c_3452,plain,
join(composition(A,top),composition(composition(A,B),complement(zero))) = complement(complement(composition(A,top))),
inference(paramod,[status(thm)],[c_27,c_3451]) ).
cnf(c_3453,plain,
join(composition(A,top),composition(composition(A,B),top)) = complement(complement(composition(A,top))),
inference(paramod,[status(thm)],[c_181,c_3452]) ).
cnf(c_3454,plain,
join(composition(A,top),composition(A,composition(B,top))) = complement(complement(composition(A,top))),
inference(paramod,[status(thm)],[c_23,c_3453]) ).
cnf(c_3455,plain,
composition(join(A,composition(A,B)),top) = complement(complement(composition(A,top))),
inference(paramod,[status(thm)],[c_58,c_3454]) ).
cnf(c_1199,plain,
composition(join(A,composition(A,B)),top) = composition(A,top),
inference(paramod,[status(thm)],[c_174,c_3455]) ).
cnf(c_3456,plain,
join(converse(A),converse(composition(converse(sK0),composition(sK0,A)))) = converse(A),
inference(paramod,[status(thm)],[c_953,c_29]) ).
cnf(c_1559,plain,
join(converse(A),composition(converse(composition(sK0,A)),sK0)) = converse(A),
inference(paramod,[status(thm)],[c_66,c_3456]) ).
cnf(c_3457,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_572,c_89]) ).
cnf(c_3458,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_353,c_3457]) ).
cnf(c_3459,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_36,c_3458]) ).
cnf(c_3460,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_18,c_3459]) ).
cnf(c_3461,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_271,c_3460]) ).
cnf(c_3462,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_174,c_3461]) ).
cnf(c_3463,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_36,c_3462]) ).
cnf(c_3464,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_18,c_3463]) ).
cnf(c_3465,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_271,c_3464]) ).
cnf(c_3466,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_174,c_3465]) ).
cnf(c_3467,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_353,c_3466]) ).
cnf(c_3468,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_36,c_3467]) ).
cnf(c_3469,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_271,c_3468]) ).
cnf(c_3470,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_174,c_3469]) ).
cnf(c_3471,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_58,c_3470]) ).
cnf(c_3472,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_1199,c_3471]) ).
cnf(c_3473,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_572,c_3472]) ).
cnf(c_3474,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_36,c_3473]) ).
cnf(c_3475,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_18,c_3474]) ).
cnf(c_3476,plain,
composition(A,top) = composition(complement(complement(A)),complement(join(complement(converse(top)),complement(composition(converse(A),top))))),
inference(paramod,[status(thm)],[c_271,c_3475]) ).
cnf(c_3477,plain,
composition(A,top) = composition(A,complement(join(complement(converse(top)),complement(composition(converse(A),top))))),
inference(paramod,[status(thm)],[c_174,c_3476]) ).
cnf(c_3478,plain,
composition(A,top) = composition(A,complement(join(complement(top),complement(composition(converse(A),top))))),
inference(paramod,[status(thm)],[c_353,c_3477]) ).
cnf(c_3479,plain,
composition(A,top) = composition(A,complement(join(zero,complement(composition(converse(A),top))))),
inference(paramod,[status(thm)],[c_36,c_3478]) ).
cnf(c_3480,plain,
composition(A,top) = composition(A,complement(complement(composition(converse(A),top)))),
inference(paramod,[status(thm)],[c_271,c_3479]) ).
cnf(c_3481,plain,
composition(A,top) = composition(A,composition(converse(A),top)),
inference(paramod,[status(thm)],[c_174,c_3480]) ).
cnf(c_1586,plain,
composition(A,composition(converse(A),top)) = composition(A,top),
inference(copy,[status(thm)],[c_3481]) ).
cnf(c_3482,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_572,c_91]) ).
cnf(c_3483,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_364,c_3482]) ).
cnf(c_3484,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_36,c_3483]) ).
cnf(c_3485,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_18,c_3484]) ).
cnf(c_3486,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_271,c_3485]) ).
cnf(c_3487,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_174,c_3486]) ).
cnf(c_3488,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_36,c_3487]) ).
cnf(c_3489,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_18,c_3488]) ).
cnf(c_3490,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_271,c_3489]) ).
cnf(c_3491,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_174,c_3490]) ).
cnf(c_3492,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_353,c_3491]) ).
cnf(c_3493,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_36,c_3492]) ).
cnf(c_3494,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_271,c_3493]) ).
cnf(c_3495,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_174,c_3494]) ).
cnf(c_3496,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_58,c_3495]) ).
cnf(c_3497,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_1199,c_3496]) ).
cnf(c_3498,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_572,c_3497]) ).
cnf(c_3499,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_36,c_3498]) ).
cnf(c_3500,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_18,c_3499]) ).
cnf(c_3501,plain,
composition(converse(A),top) = composition(complement(complement(converse(A))),complement(join(complement(converse(top)),complement(composition(A,top))))),
inference(paramod,[status(thm)],[c_271,c_3500]) ).
cnf(c_3502,plain,
composition(converse(A),top) = composition(converse(A),complement(join(complement(converse(top)),complement(composition(A,top))))),
inference(paramod,[status(thm)],[c_174,c_3501]) ).
cnf(c_3503,plain,
composition(converse(A),top) = composition(converse(A),complement(join(complement(top),complement(composition(A,top))))),
inference(paramod,[status(thm)],[c_353,c_3502]) ).
cnf(c_3504,plain,
composition(converse(A),top) = composition(converse(A),complement(join(zero,complement(composition(A,top))))),
inference(paramod,[status(thm)],[c_36,c_3503]) ).
cnf(c_3505,plain,
composition(converse(A),top) = composition(converse(A),complement(complement(composition(A,top)))),
inference(paramod,[status(thm)],[c_271,c_3504]) ).
cnf(c_3506,plain,
composition(converse(A),top) = composition(converse(A),composition(A,top)),
inference(paramod,[status(thm)],[c_174,c_3505]) ).
cnf(c_1791,plain,
composition(converse(A),composition(A,top)) = composition(converse(A),top),
inference(copy,[status(thm)],[c_3506]) ).
cnf(c_3507,plain,
join(composition(sK0,top),composition(converse(sK0),top)) = composition(sK0,top),
inference(paramod,[status(thm)],[c_1791,c_743]) ).
cnf(c_1858,plain,
composition(join(sK0,converse(sK0)),top) = composition(sK0,top),
inference(paramod,[status(thm)],[c_26,c_3507]) ).
cnf(c_3508,plain,
join(composition(converse(sK0),top),composition(sK0,top)) = composition(converse(sK0),top),
inference(paramod,[status(thm)],[c_1586,c_760]) ).
cnf(c_3509,plain,
join(composition(sK0,top),composition(converse(sK0),top)) = composition(converse(sK0),top),
inference(paramod,[status(thm)],[c_18,c_3508]) ).
cnf(c_3510,plain,
composition(join(sK0,converse(sK0)),top) = composition(converse(sK0),top),
inference(paramod,[status(thm)],[c_26,c_3509]) ).
cnf(c_3511,plain,
composition(sK0,top) = composition(converse(sK0),top),
inference(paramod,[status(thm)],[c_1858,c_3510]) ).
cnf(c_2119,plain,
composition(converse(sK0),top) = composition(sK0,top),
inference(copy,[status(thm)],[c_3511]) ).
cnf(c_3512,plain,
composition(converse(top),converse(converse(sK0))) = converse(composition(sK0,top)),
inference(paramod,[status(thm)],[c_2119,c_31]) ).
cnf(c_3513,plain,
composition(top,converse(converse(sK0))) = converse(composition(sK0,top)),
inference(paramod,[status(thm)],[c_353,c_3512]) ).
cnf(c_3514,plain,
composition(top,sK0) = converse(composition(sK0,top)),
inference(paramod,[status(thm)],[c_27,c_3513]) ).
cnf(c_3515,plain,
composition(top,sK0) = composition(top,converse(sK0)),
inference(paramod,[status(thm)],[c_363,c_3514]) ).
cnf(c_2141,plain,
composition(top,converse(sK0)) = composition(top,sK0),
inference(copy,[status(thm)],[c_3515]) ).
cnf(c_3516,plain,
join(complement(converse(sK0)),composition(converse(top),complement(composition(top,sK0)))) = complement(converse(sK0)),
inference(paramod,[status(thm)],[c_2141,c_33]) ).
cnf(c_3517,plain,
join(complement(converse(sK0)),composition(top,complement(composition(top,sK0)))) = complement(converse(sK0)),
inference(paramod,[status(thm)],[c_353,c_3516]) ).
cnf(c_2210,plain,
join(complement(converse(sK0)),complement(composition(top,sK0))) = complement(converse(sK0)),
inference(paramod,[status(thm)],[c_704,c_3517]) ).
cnf(c_3518,plain,
join(complement(complement(converse(sK0))),composition(complement(join(complement(top),complement(composition(converse(sK0),converse(sK0))))),complement(join(complement(sK0),complement(composition(converse(top),converse(sK0))))))) = composition(complement(join(complement(top),complement(composition(converse(sK0),converse(sK0))))),complement(join(complement(sK0),complement(composition(converse(top),converse(sK0)))))),
inference(paramod,[status(thm)],[c_2210,c_83]) ).
cnf(c_3519,plain,
join(converse(sK0),composition(complement(join(complement(top),complement(composition(converse(sK0),converse(sK0))))),complement(join(complement(sK0),complement(composition(converse(top),converse(sK0))))))) = composition(complement(join(complement(top),complement(composition(converse(sK0),converse(sK0))))),complement(join(complement(sK0),complement(composition(converse(top),converse(sK0)))))),
inference(paramod,[status(thm)],[c_174,c_3518]) ).
cnf(c_3520,plain,
join(converse(sK0),composition(complement(join(zero,complement(composition(converse(sK0),converse(sK0))))),complement(join(complement(sK0),complement(composition(converse(top),converse(sK0))))))) = composition(complement(join(complement(top),complement(composition(converse(sK0),converse(sK0))))),complement(join(complement(sK0),complement(composition(converse(top),converse(sK0)))))),
inference(paramod,[status(thm)],[c_36,c_3519]) ).
cnf(c_3521,plain,
join(converse(sK0),composition(complement(join(zero,complement(converse(composition(sK0,sK0))))),complement(join(complement(sK0),complement(composition(converse(top),converse(sK0))))))) = composition(complement(join(complement(top),complement(composition(converse(sK0),converse(sK0))))),complement(join(complement(sK0),complement(composition(converse(top),converse(sK0)))))),
inference(paramod,[status(thm)],[c_31,c_3520]) ).
cnf(c_3522,plain,
join(converse(sK0),composition(complement(complement(converse(composition(sK0,sK0)))),complement(join(complement(sK0),complement(composition(converse(top),converse(sK0))))))) = composition(complement(join(complement(top),complement(composition(converse(sK0),converse(sK0))))),complement(join(complement(sK0),complement(composition(converse(top),converse(sK0)))))),
inference(paramod,[status(thm)],[c_271,c_3521]) ).
cnf(c_3523,plain,
join(converse(sK0),composition(converse(composition(sK0,sK0)),complement(join(complement(sK0),complement(composition(converse(top),converse(sK0))))))) = composition(complement(join(complement(top),complement(composition(converse(sK0),converse(sK0))))),complement(join(complement(sK0),complement(composition(converse(top),converse(sK0)))))),
inference(paramod,[status(thm)],[c_174,c_3522]) ).
cnf(c_3524,plain,
join(converse(sK0),composition(converse(composition(sK0,sK0)),complement(join(complement(sK0),complement(composition(top,converse(sK0))))))) = composition(complement(join(complement(top),complement(composition(converse(sK0),converse(sK0))))),complement(join(complement(sK0),complement(composition(converse(top),converse(sK0)))))),
inference(paramod,[status(thm)],[c_353,c_3523]) ).
cnf(c_3525,plain,
join(converse(sK0),composition(converse(composition(sK0,sK0)),complement(join(complement(sK0),complement(composition(top,sK0)))))) = composition(complement(join(complement(top),complement(composition(converse(sK0),converse(sK0))))),complement(join(complement(sK0),complement(composition(converse(top),converse(sK0)))))),
inference(paramod,[status(thm)],[c_2141,c_3524]) ).
cnf(c_3526,plain,
join(converse(sK0),composition(converse(composition(sK0,sK0)),complement(complement(sK0)))) = composition(complement(join(complement(top),complement(composition(converse(sK0),converse(sK0))))),complement(join(complement(sK0),complement(composition(converse(top),converse(sK0)))))),
inference(paramod,[status(thm)],[c_710,c_3525]) ).
cnf(c_3527,plain,
join(converse(sK0),composition(converse(composition(sK0,sK0)),sK0)) = composition(complement(join(complement(top),complement(composition(converse(sK0),converse(sK0))))),complement(join(complement(sK0),complement(composition(converse(top),converse(sK0)))))),
inference(paramod,[status(thm)],[c_174,c_3526]) ).
cnf(c_3528,plain,
converse(sK0) = composition(complement(join(complement(top),complement(composition(converse(sK0),converse(sK0))))),complement(join(complement(sK0),complement(composition(converse(top),converse(sK0)))))),
inference(paramod,[status(thm)],[c_1559,c_3527]) ).
cnf(c_3529,plain,
converse(sK0) = composition(complement(join(zero,complement(composition(converse(sK0),converse(sK0))))),complement(join(complement(sK0),complement(composition(converse(top),converse(sK0)))))),
inference(paramod,[status(thm)],[c_36,c_3528]) ).
cnf(c_3530,plain,
converse(sK0) = composition(complement(join(zero,complement(converse(composition(sK0,sK0))))),complement(join(complement(sK0),complement(composition(converse(top),converse(sK0)))))),
inference(paramod,[status(thm)],[c_31,c_3529]) ).
cnf(c_3531,plain,
converse(sK0) = composition(complement(complement(converse(composition(sK0,sK0)))),complement(join(complement(sK0),complement(composition(converse(top),converse(sK0)))))),
inference(paramod,[status(thm)],[c_271,c_3530]) ).
cnf(c_3532,plain,
converse(sK0) = composition(converse(composition(sK0,sK0)),complement(join(complement(sK0),complement(composition(converse(top),converse(sK0)))))),
inference(paramod,[status(thm)],[c_174,c_3531]) ).
cnf(c_3533,plain,
converse(sK0) = composition(converse(composition(sK0,sK0)),complement(join(complement(sK0),complement(composition(top,converse(sK0)))))),
inference(paramod,[status(thm)],[c_353,c_3532]) ).
cnf(c_3534,plain,
converse(sK0) = composition(converse(composition(sK0,sK0)),complement(join(complement(sK0),complement(composition(top,sK0))))),
inference(paramod,[status(thm)],[c_2141,c_3533]) ).
cnf(c_3535,plain,
converse(sK0) = composition(converse(composition(sK0,sK0)),complement(complement(sK0))),
inference(paramod,[status(thm)],[c_710,c_3534]) ).
cnf(c_3536,plain,
converse(sK0) = composition(converse(composition(sK0,sK0)),sK0),
inference(paramod,[status(thm)],[c_174,c_3535]) ).
cnf(c_2756,plain,
composition(converse(composition(sK0,sK0)),sK0) = converse(sK0),
inference(copy,[status(thm)],[c_3536]) ).
cnf(c_3537,plain,
composition(converse(sK0),A) = composition(converse(composition(sK0,sK0)),composition(sK0,A)),
inference(paramod,[status(thm)],[c_2756,c_23]) ).
cnf(c_2762,plain,
composition(converse(composition(sK0,sK0)),composition(sK0,A)) = composition(converse(sK0),A),
inference(copy,[status(thm)],[c_3537]) ).
cnf(c_3538,plain,
composition(converse(sK0),composition(converse(converse(composition(sK0,sK0))),A)) = composition(converse(converse(sK0)),A),
inference(paramod,[status(thm)],[c_2756,c_62]) ).
cnf(c_3539,plain,
composition(converse(sK0),composition(composition(sK0,sK0),A)) = composition(converse(converse(sK0)),A),
inference(paramod,[status(thm)],[c_27,c_3538]) ).
cnf(c_3540,plain,
composition(converse(sK0),composition(sK0,composition(sK0,A))) = composition(converse(converse(sK0)),A),
inference(paramod,[status(thm)],[c_23,c_3539]) ).
cnf(c_2772,plain,
composition(converse(sK0),composition(sK0,composition(sK0,A))) = composition(sK0,A),
inference(paramod,[status(thm)],[c_27,c_3540]) ).
cnf(c_3541,plain,
join(composition(A,converse(converse(composition(sK0,sK0)))),converse(converse(sK0))) = composition(join(A,converse(sK0)),converse(converse(composition(sK0,sK0)))),
inference(paramod,[status(thm)],[c_2756,c_64]) ).
cnf(c_3542,plain,
join(composition(A,composition(sK0,sK0)),converse(converse(sK0))) = composition(join(A,converse(sK0)),converse(converse(composition(sK0,sK0)))),
inference(paramod,[status(thm)],[c_27,c_3541]) ).
cnf(c_3543,plain,
join(composition(A,composition(sK0,sK0)),sK0) = composition(join(A,converse(sK0)),converse(converse(composition(sK0,sK0)))),
inference(paramod,[status(thm)],[c_27,c_3542]) ).
cnf(c_3544,plain,
join(sK0,composition(A,composition(sK0,sK0))) = composition(join(A,converse(sK0)),converse(converse(composition(sK0,sK0)))),
inference(paramod,[status(thm)],[c_18,c_3543]) ).
cnf(c_3545,plain,
join(sK0,composition(A,composition(sK0,sK0))) = composition(join(A,converse(sK0)),composition(sK0,sK0)),
inference(paramod,[status(thm)],[c_27,c_3544]) ).
cnf(c_2774,plain,
composition(join(A,converse(sK0)),composition(sK0,sK0)) = join(sK0,composition(A,composition(sK0,sK0))),
inference(copy,[status(thm)],[c_3545]) ).
cnf(c_3546,plain,
join(converse(composition(sK0,sK0)),converse(sK0)) = converse(composition(sK0,sK0)),
inference(paramod,[status(thm)],[c_2756,c_898]) ).
cnf(c_3547,plain,
join(converse(sK0),converse(composition(sK0,sK0))) = converse(composition(sK0,sK0)),
inference(paramod,[status(thm)],[c_18,c_3546]) ).
cnf(c_3548,plain,
converse(join(sK0,composition(sK0,sK0))) = converse(composition(sK0,sK0)),
inference(paramod,[status(thm)],[c_29,c_3547]) ).
cnf(c_3549,plain,
converse(sK0) = converse(composition(sK0,sK0)),
inference(paramod,[status(thm)],[c_898,c_3548]) ).
cnf(c_2778,plain,
converse(composition(sK0,sK0)) = converse(sK0),
inference(copy,[status(thm)],[c_3549]) ).
cnf(c_2822,plain,
composition(converse(sK0),composition(sK0,A)) = composition(converse(sK0),A),
inference(paramod,[status(thm)],[c_2778,c_2762]) ).
cnf(c_2824,plain,
composition(converse(sK0),sK0) = converse(sK0),
inference(paramod,[status(thm)],[c_2778,c_2756]) ).
cnf(c_3550,plain,
composition(converse(sK0),composition(sK0,A)) = composition(sK0,A),
inference(paramod,[status(thm)],[c_2822,c_2772]) ).
cnf(c_2829,plain,
composition(converse(sK0),A) = composition(sK0,A),
inference(paramod,[status(thm)],[c_2822,c_3550]) ).
cnf(c_2842,plain,
composition(sK0,sK0) = converse(sK0),
inference(paramod,[status(thm)],[c_2829,c_2824]) ).
cnf(c_3551,plain,
converse(converse(sK0)) = converse(sK0),
inference(paramod,[status(thm)],[c_2842,c_2778]) ).
cnf(c_3552,plain,
sK0 = converse(sK0),
inference(paramod,[status(thm)],[c_27,c_3551]) ).
cnf(c_2862,plain,
converse(sK0) = sK0,
inference(copy,[status(thm)],[c_3552]) ).
cnf(c_3553,plain,
composition(join(A,sK0),composition(sK0,sK0)) = join(sK0,composition(A,composition(sK0,sK0))),
inference(paramod,[status(thm)],[c_2862,c_2774]) ).
cnf(c_3554,plain,
composition(join(A,sK0),converse(sK0)) = join(sK0,composition(A,composition(sK0,sK0))),
inference(paramod,[status(thm)],[c_2842,c_3553]) ).
cnf(c_3555,plain,
composition(join(A,sK0),sK0) = join(sK0,composition(A,composition(sK0,sK0))),
inference(paramod,[status(thm)],[c_2862,c_3554]) ).
cnf(c_3556,plain,
composition(join(A,sK0),sK0) = join(sK0,composition(A,converse(sK0))),
inference(paramod,[status(thm)],[c_2842,c_3555]) ).
cnf(c_3557,plain,
composition(join(A,sK0),sK0) = join(sK0,composition(A,sK0)),
inference(paramod,[status(thm)],[c_2862,c_3556]) ).
cnf(c_3558,plain,
composition(join(A,sK0),sK0) = composition(join(one,A),sK0),
inference(paramod,[status(thm)],[c_664,c_3557]) ).
cnf(c_2863,plain,
composition(join(one,A),sK0) = composition(join(A,sK0),sK0),
inference(copy,[status(thm)],[c_3558]) ).
cnf(c_3559,plain,
composition(sK0,converse(A)) = converse(composition(A,sK0)),
inference(paramod,[status(thm)],[c_2862,c_31]) ).
cnf(c_2920,plain,
converse(composition(A,sK0)) = composition(sK0,converse(A)),
inference(copy,[status(thm)],[c_3559]) ).
cnf(c_3560,plain,
join(join(A,sK0),composition(join(one,A),sK0)) = join(A,sK0),
inference(paramod,[status(thm)],[c_2863,c_898]) ).
cnf(c_3561,plain,
join(A,join(sK0,composition(join(one,A),sK0))) = join(A,sK0),
inference(paramod,[status(thm)],[c_19,c_3560]) ).
cnf(c_3562,plain,
join(A,join(sK0,composition(A,sK0))) = join(A,sK0),
inference(paramod,[status(thm)],[c_767,c_3561]) ).
cnf(c_3101,plain,
join(A,composition(join(one,A),sK0)) = join(A,sK0),
inference(paramod,[status(thm)],[c_664,c_3562]) ).
cnf(c_3563,plain,
converse(join(converse(A),sK0)) = join(A,converse(composition(join(one,converse(A)),sK0))),
inference(paramod,[status(thm)],[c_3101,c_60]) ).
cnf(c_3564,plain,
converse(join(sK0,converse(A))) = join(A,converse(composition(join(one,converse(A)),sK0))),
inference(paramod,[status(thm)],[c_18,c_3563]) ).
cnf(c_3565,plain,
join(converse(sK0),A) = join(A,converse(composition(join(one,converse(A)),sK0))),
inference(paramod,[status(thm)],[c_61,c_3564]) ).
cnf(c_3566,plain,
join(sK0,A) = join(A,converse(composition(join(one,converse(A)),sK0))),
inference(paramod,[status(thm)],[c_2862,c_3565]) ).
cnf(c_3567,plain,
join(sK0,A) = join(A,composition(sK0,converse(join(one,converse(A))))),
inference(paramod,[status(thm)],[c_2920,c_3566]) ).
cnf(c_3568,plain,
join(sK0,A) = join(A,composition(sK0,join(converse(one),A))),
inference(paramod,[status(thm)],[c_61,c_3567]) ).
cnf(c_3569,plain,
join(sK0,A) = join(A,composition(sK0,join(one,A))),
inference(paramod,[status(thm)],[c_663,c_3568]) ).
cnf(c_3233,plain,
join(A,composition(sK0,join(one,A))) = join(sK0,A),
inference(copy,[status(thm)],[c_3569]) ).
cnf(c_3316,plain,
join(complement(one),composition(sK0,top)) = join(sK0,complement(one)),
inference(paramod,[status(thm)],[c_34,c_3233]) ).
cnf(c_3570,negated_conjecture,
( join(complement(join(sK0,complement(one))),complement(join(complement(one),composition(sK0,top)))) != complement(join(complement(one),composition(sK0,top)))
| join(complement(join(sK0,complement(one))),complement(join(sK0,complement(one)))) != complement(join(sK0,complement(one))) ),
inference(paramod,[status(thm)],[c_3316,c_178]) ).
cnf(c_3571,negated_conjecture,
( join(complement(join(sK0,complement(one))),complement(join(complement(one),composition(sK0,top)))) != complement(join(complement(one),composition(sK0,top)))
| complement(join(sK0,complement(one))) != complement(join(sK0,complement(one))) ),
inference(paramod,[status(thm)],[c_295,c_3570]) ).
cnf(c_3572,negated_conjecture,
( join(complement(join(sK0,complement(one))),complement(join(sK0,complement(one)))) != complement(join(complement(one),composition(sK0,top)))
| complement(join(sK0,complement(one))) != complement(join(sK0,complement(one))) ),
inference(paramod,[status(thm)],[c_3316,c_3571]) ).
cnf(c_3573,negated_conjecture,
( complement(join(sK0,complement(one))) != complement(join(complement(one),composition(sK0,top)))
| complement(join(sK0,complement(one))) != complement(join(sK0,complement(one))) ),
inference(paramod,[status(thm)],[c_295,c_3572]) ).
cnf(c_3574,negated_conjecture,
( complement(join(sK0,complement(one))) != complement(join(sK0,complement(one)))
| complement(join(sK0,complement(one))) != complement(join(sK0,complement(one))) ),
inference(paramod,[status(thm)],[c_3316,c_3573]) ).
cnf(c_3575,negated_conjecture,
complement(join(sK0,complement(one))) != complement(join(sK0,complement(one))),
inference(copy,[status(thm)],[c_3574]) ).
cnf(c_3340,negated_conjecture,
$false,
inference(copy,[status(thm)],[c_3575]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : REL027+4 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.03 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.05/0.35 % Computer : n001.cluster.edu
% 0.05/0.35 % Model : x86_64 x86_64
% 0.05/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.05/0.35 % Memory : 8046.5625MB
% 0.05/0.35 % OS : Linux 6.8.0-71-generic
% 0.05/0.35 % CPULimit : 300
% 0.05/0.35 % WCLimit : 300
% 0.05/0.35 % DateTime : Sat Sep 26 05:39:12 UTC 2026
% 0.05/0.35 % CPUTime :
% 0.05/0.35 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.05/0.35 % Process 1011450 was started by sandbox on n001,
% 0.05/0.35 % Sat Sep 26 05:39:12 2026
% 0.05/0.35 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.05/0.37
% 0.05/0.37 % From the command line: assign(max_seconds, 300).
% 10.20/3.24
% 10.20/3.24 % SZS status Theorem for theBenchmark
% 10.20/3.24
% 10.20/3.24 % Proof 1 at 0.99 (+ 0.24) seconds.
% 10.20/3.24 % Length of proof is 130.
% 10.20/3.24 % Level of proof is 31.
% 10.20/3.24 % Maximum clause weight is 99.000.
% 10.20/3.24 % Given clauses 280.
% 10.20/3.24
% 10.20/3.24 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------