%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : REL030-4 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n007.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sun Sep 27 08:25:00 AM UTC 2026
% Result : Unsatisfiable 39.05s 5.48s
% Output : CNFRefutation 39.05s
% Verified :
% SZS Type : Refutation
% Derivation depth : 101
% Number of leaves : 17
% Syntax : Number of formulae : 387 ( 362 unt; 0 def)
% Number of atoms : 412 ( 411 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 86 ( 61 ~; 25 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 1 avg)
% Maximal term depth : 12 ( 3 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 11 ( 11 usr; 6 con; 0-2 aty)
% Number of variables : 472 ( 20 sgn 31 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(maddux1_join_commutativity_1,axiom,
! [VAR_0,VAR_1] : join(VAR_0,VAR_1) = join(VAR_1,VAR_0),
file('theBenchmark.p',maddux1_join_commutativity_1) ).
cnf(c_1,plain,
join(A,B) = join(B,A),
inference(clausify,[status(thm)],[maddux1_join_commutativity_1]) ).
fof(maddux2_join_associativity_2,axiom,
! [VAR_0,VAR_1,VAR_2] : join(VAR_0,join(VAR_1,VAR_2)) = join(join(VAR_0,VAR_1),VAR_2),
file('theBenchmark.p',maddux2_join_associativity_2) ).
cnf(c_2,plain,
join(A,join(B,C)) = join(join(A,B),C),
inference(clausify,[status(thm)],[maddux2_join_associativity_2]) ).
cnf(c_3,plain,
join(join(A,B),C) = join(A,join(B,C)),
inference(copy,[status(thm)],[c_2]) ).
fof(maddux3_a_kind_of_de_Morgan_3,axiom,
! [VAR_0,VAR_1] : VAR_0 = join(complement(join(complement(VAR_0),complement(VAR_1))),complement(join(complement(VAR_0),VAR_1))),
file('theBenchmark.p',maddux3_a_kind_of_de_Morgan_3) ).
cnf(c_4,plain,
A = join(complement(join(complement(A),complement(B))),complement(join(complement(A),B))),
inference(clausify,[status(thm)],[maddux3_a_kind_of_de_Morgan_3]) ).
cnf(c_9607,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_9607]) ).
fof(maddux4_definiton_of_meet_4,axiom,
! [VAR_0,VAR_1] : meet(VAR_0,VAR_1) = complement(join(complement(VAR_0),complement(VAR_1))),
file('theBenchmark.p',maddux4_definiton_of_meet_4) ).
cnf(c_6,plain,
meet(A,B) = complement(join(complement(A),complement(B))),
inference(clausify,[status(thm)],[maddux4_definiton_of_meet_4]) ).
fof(composition_identity_6,axiom,
! [VAR_0] : composition(VAR_0,one) = VAR_0,
file('theBenchmark.p',composition_identity_6) ).
cnf(c_9,plain,
composition(A,one) = A,
inference(clausify,[status(thm)],[composition_identity_6]) ).
fof(composition_distributivity_7,axiom,
! [VAR_0,VAR_1,VAR_2] : composition(join(VAR_0,VAR_1),VAR_2) = join(composition(VAR_0,VAR_2),composition(VAR_1,VAR_2)),
file('theBenchmark.p',composition_distributivity_7) ).
cnf(c_10,plain,
composition(join(A,B),C) = join(composition(A,C),composition(B,C)),
inference(clausify,[status(thm)],[composition_distributivity_7]) ).
fof(converse_idempotence_8,axiom,
! [VAR_0] : converse(converse(VAR_0)) = VAR_0,
file('theBenchmark.p',converse_idempotence_8) ).
cnf(c_11,plain,
converse(converse(A)) = A,
inference(clausify,[status(thm)],[converse_idempotence_8]) ).
fof(converse_additivity_9,axiom,
! [VAR_0,VAR_1] : converse(join(VAR_0,VAR_1)) = join(converse(VAR_0),converse(VAR_1)),
file('theBenchmark.p',converse_additivity_9) ).
cnf(c_12,plain,
converse(join(A,B)) = join(converse(A),converse(B)),
inference(clausify,[status(thm)],[converse_additivity_9]) ).
fof(converse_multiplicativity_10,axiom,
! [VAR_0,VAR_1] : converse(composition(VAR_0,VAR_1)) = composition(converse(VAR_1),converse(VAR_0)),
file('theBenchmark.p',converse_multiplicativity_10) ).
cnf(c_13,plain,
converse(composition(A,B)) = composition(converse(B),converse(A)),
inference(clausify,[status(thm)],[converse_multiplicativity_10]) ).
fof(converse_cancellativity_11,axiom,
! [VAR_0,VAR_1] : join(composition(converse(VAR_0),complement(composition(VAR_0,VAR_1))),complement(VAR_1)) = complement(VAR_1),
file('theBenchmark.p',converse_cancellativity_11) ).
cnf(c_14,plain,
join(composition(converse(A),complement(composition(A,B))),complement(B)) = complement(B),
inference(clausify,[status(thm)],[converse_cancellativity_11]) ).
cnf(c_15,plain,
join(complement(A),composition(converse(B),complement(composition(B,A)))) = complement(A),
inference(paramod,[status(thm)],[c_1,c_14]) ).
fof(def_top_12,axiom,
! [VAR_0] : top = join(VAR_0,complement(VAR_0)),
file('theBenchmark.p',def_top_12) ).
cnf(c_16,plain,
top = join(A,complement(A)),
inference(clausify,[status(thm)],[def_top_12]) ).
cnf(c_17,plain,
join(A,complement(A)) = top,
inference(copy,[status(thm)],[c_16]) ).
fof(def_zero_13,axiom,
! [VAR_0] : zero = meet(VAR_0,complement(VAR_0)),
file('theBenchmark.p',def_zero_13) ).
cnf(c_18,plain,
zero = meet(A,complement(A)),
inference(clausify,[status(thm)],[def_zero_13]) ).
cnf(c_9608,plain,
zero = complement(join(complement(A),complement(complement(A)))),
inference(paramod,[status(thm)],[c_6,c_18]) ).
cnf(c_9609,plain,
zero = complement(top),
inference(paramod,[status(thm)],[c_17,c_9608]) ).
cnf(c_19,plain,
complement(top) = zero,
inference(copy,[status(thm)],[c_9609]) ).
fof(dedekind_law_14,axiom,
! [VAR_0,VAR_1,VAR_2] : join(meet(composition(VAR_0,VAR_1),VAR_2),composition(meet(VAR_0,composition(VAR_2,converse(VAR_1))),meet(VAR_1,composition(converse(VAR_0),VAR_2)))) = composition(meet(VAR_0,composition(VAR_2,converse(VAR_1))),meet(VAR_1,composition(converse(VAR_0),VAR_2))),
file('theBenchmark.p',dedekind_law_14) ).
cnf(c_20,plain,
join(meet(composition(A,B),C),composition(meet(A,composition(C,converse(B))),meet(B,composition(converse(A),C)))) = composition(meet(A,composition(C,converse(B))),meet(B,composition(converse(A),C))),
inference(clausify,[status(thm)],[dedekind_law_14]) ).
cnf(c_9610,plain,
join(complement(join(complement(composition(A,B)),complement(C))),composition(meet(A,composition(C,converse(B))),meet(B,composition(converse(A),C)))) = composition(meet(A,composition(C,converse(B))),meet(B,composition(converse(A),C))),
inference(paramod,[status(thm)],[c_6,c_20]) ).
cnf(c_9611,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_9610]) ).
cnf(c_9612,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_9611]) ).
cnf(c_9613,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_9612]) ).
cnf(c_21,plain,
join(complement(join(complement(composition(A,B)),complement(C))),composition(complement(join(complement(A),complement(composition(C,converse(B))))),complement(join(complement(B),complement(composition(converse(A),C)))))) = composition(complement(join(complement(A),complement(composition(C,converse(B))))),complement(join(complement(B),complement(composition(converse(A),C))))),
inference(paramod,[status(thm)],[c_6,c_9613]) ).
fof(modular_law_1_15,axiom,
! [VAR_0,VAR_1,VAR_2] : join(meet(composition(VAR_0,VAR_1),VAR_2),meet(composition(VAR_0,meet(VAR_1,composition(converse(VAR_0),VAR_2))),VAR_2)) = meet(composition(VAR_0,meet(VAR_1,composition(converse(VAR_0),VAR_2))),VAR_2),
file('theBenchmark.p',modular_law_1_15) ).
cnf(c_22,plain,
join(meet(composition(A,B),C),meet(composition(A,meet(B,composition(converse(A),C))),C)) = meet(composition(A,meet(B,composition(converse(A),C))),C),
inference(clausify,[status(thm)],[modular_law_1_15]) ).
cnf(c_9614,plain,
join(complement(join(complement(composition(A,B)),complement(C))),meet(composition(A,meet(B,composition(converse(A),C))),C)) = meet(composition(A,meet(B,composition(converse(A),C))),C),
inference(paramod,[status(thm)],[c_6,c_22]) ).
cnf(c_9615,plain,
join(complement(join(complement(composition(A,B)),complement(C))),meet(composition(A,complement(join(complement(B),complement(composition(converse(A),C))))),C)) = meet(composition(A,meet(B,composition(converse(A),C))),C),
inference(paramod,[status(thm)],[c_6,c_9614]) ).
cnf(c_9616,plain,
join(complement(join(complement(composition(A,B)),complement(C))),complement(join(complement(composition(A,complement(join(complement(B),complement(composition(converse(A),C)))))),complement(C)))) = meet(composition(A,meet(B,composition(converse(A),C))),C),
inference(paramod,[status(thm)],[c_6,c_9615]) ).
cnf(c_9617,plain,
join(complement(join(complement(composition(A,B)),complement(C))),complement(join(complement(C),complement(composition(A,complement(join(complement(B),complement(composition(converse(A),C))))))))) = meet(composition(A,meet(B,composition(converse(A),C))),C),
inference(paramod,[status(thm)],[c_1,c_9616]) ).
cnf(c_9618,plain,
join(complement(join(complement(composition(A,B)),complement(C))),complement(join(complement(C),complement(composition(A,complement(join(complement(B),complement(composition(converse(A),C))))))))) = meet(composition(A,complement(join(complement(B),complement(composition(converse(A),C))))),C),
inference(paramod,[status(thm)],[c_6,c_9617]) ).
cnf(c_9619,plain,
join(complement(join(complement(composition(A,B)),complement(C))),complement(join(complement(C),complement(composition(A,complement(join(complement(B),complement(composition(converse(A),C))))))))) = complement(join(complement(composition(A,complement(join(complement(B),complement(composition(converse(A),C)))))),complement(C))),
inference(paramod,[status(thm)],[c_6,c_9618]) ).
cnf(c_23,plain,
join(complement(join(complement(composition(A,B)),complement(C))),complement(join(complement(C),complement(composition(A,complement(join(complement(B),complement(composition(converse(A),C))))))))) = complement(join(complement(C),complement(composition(A,complement(join(complement(B),complement(composition(converse(A),C)))))))),
inference(paramod,[status(thm)],[c_1,c_9619]) ).
fof(modular_law_2_16,axiom,
! [VAR_0,VAR_1,VAR_2] : join(meet(composition(VAR_0,VAR_1),VAR_2),meet(composition(meet(VAR_0,composition(VAR_2,converse(VAR_1))),VAR_1),VAR_2)) = meet(composition(meet(VAR_0,composition(VAR_2,converse(VAR_1))),VAR_1),VAR_2),
file('theBenchmark.p',modular_law_2_16) ).
cnf(c_24,plain,
join(meet(composition(A,B),C),meet(composition(meet(A,composition(C,converse(B))),B),C)) = meet(composition(meet(A,composition(C,converse(B))),B),C),
inference(clausify,[status(thm)],[modular_law_2_16]) ).
cnf(c_9620,plain,
join(complement(join(complement(composition(A,B)),complement(C))),meet(composition(meet(A,composition(C,converse(B))),B),C)) = meet(composition(meet(A,composition(C,converse(B))),B),C),
inference(paramod,[status(thm)],[c_6,c_24]) ).
cnf(c_9621,plain,
join(complement(join(complement(composition(A,B)),complement(C))),meet(composition(complement(join(complement(A),complement(composition(C,converse(B))))),B),C)) = meet(composition(meet(A,composition(C,converse(B))),B),C),
inference(paramod,[status(thm)],[c_6,c_9620]) ).
cnf(c_9622,plain,
join(complement(join(complement(composition(A,B)),complement(C))),complement(join(complement(composition(complement(join(complement(A),complement(composition(C,converse(B))))),B)),complement(C)))) = meet(composition(meet(A,composition(C,converse(B))),B),C),
inference(paramod,[status(thm)],[c_6,c_9621]) ).
cnf(c_9623,plain,
join(complement(join(complement(composition(A,B)),complement(C))),complement(join(complement(C),complement(composition(complement(join(complement(A),complement(composition(C,converse(B))))),B))))) = meet(composition(meet(A,composition(C,converse(B))),B),C),
inference(paramod,[status(thm)],[c_1,c_9622]) ).
cnf(c_9624,plain,
join(complement(join(complement(composition(A,B)),complement(C))),complement(join(complement(C),complement(composition(complement(join(complement(A),complement(composition(C,converse(B))))),B))))) = meet(composition(complement(join(complement(A),complement(composition(C,converse(B))))),B),C),
inference(paramod,[status(thm)],[c_6,c_9623]) ).
cnf(c_9625,plain,
join(complement(join(complement(composition(A,B)),complement(C))),complement(join(complement(C),complement(composition(complement(join(complement(A),complement(composition(C,converse(B))))),B))))) = complement(join(complement(composition(complement(join(complement(A),complement(composition(C,converse(B))))),B)),complement(C))),
inference(paramod,[status(thm)],[c_6,c_9624]) ).
cnf(c_25,plain,
join(complement(join(complement(composition(A,B)),complement(C))),complement(join(complement(C),complement(composition(complement(join(complement(A),complement(composition(C,converse(B))))),B))))) = complement(join(complement(C),complement(composition(complement(join(complement(A),complement(composition(C,converse(B))))),B)))),
inference(paramod,[status(thm)],[c_1,c_9625]) ).
fof(goals_17,axiom,
join(sk1,one) = one,
file('theBenchmark.p',goals_17) ).
cnf(c_26,plain,
join(sk1,one) = one,
inference(clausify,[status(thm)],[goals_17]) ).
cnf(c_27,plain,
join(one,sk1) = one,
inference(paramod,[status(thm)],[c_1,c_26]) ).
fof(goals_18,axiom,
( join(meet(composition(sk1,sk2),complement(composition(sk1,sk3))),meet(composition(sk1,sk2),complement(sk3))) != meet(composition(sk1,sk2),complement(sk3))
| join(meet(composition(sk1,sk2),complement(sk3)),meet(composition(sk1,sk2),complement(composition(sk1,sk3)))) != meet(composition(sk1,sk2),complement(composition(sk1,sk3))) ),
file('theBenchmark.p',goals_18) ).
cnf(c_28,plain,
( join(meet(composition(sk1,sk2),complement(composition(sk1,sk3))),meet(composition(sk1,sk2),complement(sk3))) != meet(composition(sk1,sk2),complement(sk3))
| join(meet(composition(sk1,sk2),complement(sk3)),meet(composition(sk1,sk2),complement(composition(sk1,sk3)))) != meet(composition(sk1,sk2),complement(composition(sk1,sk3))) ),
inference(clausify,[status(thm)],[goals_18]) ).
cnf(c_9626,plain,
( join(meet(composition(sk1,sk2),complement(composition(sk1,sk3))),meet(composition(sk1,sk2),complement(sk3))) != meet(composition(sk1,sk2),complement(sk3))
| join(complement(join(complement(composition(sk1,sk2)),complement(complement(sk3)))),meet(composition(sk1,sk2),complement(composition(sk1,sk3)))) != meet(composition(sk1,sk2),complement(composition(sk1,sk3))) ),
inference(paramod,[status(thm)],[c_6,c_28]) ).
cnf(c_9627,plain,
( join(meet(composition(sk1,sk2),complement(composition(sk1,sk3))),meet(composition(sk1,sk2),complement(sk3))) != meet(composition(sk1,sk2),complement(sk3))
| join(complement(join(complement(complement(sk3)),complement(composition(sk1,sk2)))),meet(composition(sk1,sk2),complement(composition(sk1,sk3)))) != meet(composition(sk1,sk2),complement(composition(sk1,sk3))) ),
inference(paramod,[status(thm)],[c_1,c_9626]) ).
cnf(c_9628,plain,
( join(meet(composition(sk1,sk2),complement(composition(sk1,sk3))),meet(composition(sk1,sk2),complement(sk3))) != meet(composition(sk1,sk2),complement(sk3))
| join(complement(join(complement(complement(sk3)),complement(composition(sk1,sk2)))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3)))))) != meet(composition(sk1,sk2),complement(composition(sk1,sk3))) ),
inference(paramod,[status(thm)],[c_6,c_9627]) ).
cnf(c_9629,plain,
( join(meet(composition(sk1,sk2),complement(composition(sk1,sk3))),meet(composition(sk1,sk2),complement(sk3))) != meet(composition(sk1,sk2),complement(sk3))
| join(complement(join(complement(complement(sk3)),complement(composition(sk1,sk2)))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3)))))) != complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))) ),
inference(paramod,[status(thm)],[c_6,c_9628]) ).
cnf(c_9630,plain,
( join(complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),meet(composition(sk1,sk2),complement(sk3))) != meet(composition(sk1,sk2),complement(sk3))
| join(complement(join(complement(complement(sk3)),complement(composition(sk1,sk2)))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3)))))) != complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))) ),
inference(paramod,[status(thm)],[c_6,c_9629]) ).
cnf(c_9631,plain,
( join(complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),complement(join(complement(composition(sk1,sk2)),complement(complement(sk3))))) != meet(composition(sk1,sk2),complement(sk3))
| join(complement(join(complement(complement(sk3)),complement(composition(sk1,sk2)))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3)))))) != complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))) ),
inference(paramod,[status(thm)],[c_6,c_9630]) ).
cnf(c_9632,plain,
( join(complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))),complement(join(complement(complement(sk3)),complement(composition(sk1,sk2))))) != meet(composition(sk1,sk2),complement(sk3))
| join(complement(join(complement(complement(sk3)),complement(composition(sk1,sk2)))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3)))))) != complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))) ),
inference(paramod,[status(thm)],[c_1,c_9631]) ).
cnf(c_9633,plain,
( join(complement(join(complement(complement(sk3)),complement(composition(sk1,sk2)))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3)))))) != meet(composition(sk1,sk2),complement(sk3))
| join(complement(join(complement(complement(sk3)),complement(composition(sk1,sk2)))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3)))))) != complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))) ),
inference(paramod,[status(thm)],[c_1,c_9632]) ).
cnf(c_9634,plain,
( join(complement(join(complement(complement(sk3)),complement(composition(sk1,sk2)))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3)))))) != complement(join(complement(composition(sk1,sk2)),complement(complement(sk3))))
| join(complement(join(complement(complement(sk3)),complement(composition(sk1,sk2)))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3)))))) != complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))) ),
inference(paramod,[status(thm)],[c_6,c_9633]) ).
cnf(c_29,plain,
( join(complement(join(complement(complement(sk3)),complement(composition(sk1,sk2)))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3)))))) != complement(join(complement(complement(sk3)),complement(composition(sk1,sk2))))
| join(complement(join(complement(complement(sk3)),complement(composition(sk1,sk2)))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3)))))) != complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))) ),
inference(paramod,[status(thm)],[c_1,c_9634]) ).
cnf(c_9635,plain,
join(join(A,B),C) = join(B,join(A,C)),
inference(paramod,[status(thm)],[c_1,c_3]) ).
cnf(c_31,plain,
join(A,join(B,C)) = join(B,join(A,C)),
inference(paramod,[status(thm)],[c_3,c_9635]) ).
cnf(c_32,plain,
join(complement(join(A,complement(B))),complement(join(complement(B),complement(A)))) = B,
inference(paramod,[status(thm)],[c_1,c_5]) ).
cnf(c_33,plain,
join(complement(join(complement(A),B)),complement(join(complement(B),complement(A)))) = A,
inference(paramod,[status(thm)],[c_1,c_5]) ).
cnf(c_9636,plain,
join(A,B) = join(complement(join(complement(A),C)),join(complement(join(complement(A),complement(C))),B)),
inference(paramod,[status(thm)],[c_5,c_3]) ).
cnf(c_34,plain,
join(complement(join(complement(A),B)),join(complement(join(complement(A),complement(B))),C)) = join(A,C),
inference(copy,[status(thm)],[c_9636]) ).
cnf(c_9637,plain,
join(complement(join(complement(join(complement(A),B)),join(complement(A),complement(B)))),complement(A)) = join(complement(A),B),
inference(paramod,[status(thm)],[c_5,c_5]) ).
cnf(c_9638,plain,
join(complement(join(join(complement(A),complement(B)),complement(join(complement(A),B)))),complement(A)) = join(complement(A),B),
inference(paramod,[status(thm)],[c_1,c_9637]) ).
cnf(c_9639,plain,
join(complement(join(complement(A),join(complement(B),complement(join(complement(A),B))))),complement(A)) = join(complement(A),B),
inference(paramod,[status(thm)],[c_3,c_9638]) ).
cnf(c_36,plain,
join(complement(A),complement(join(complement(A),join(complement(B),complement(join(complement(A),B)))))) = join(complement(A),B),
inference(paramod,[status(thm)],[c_1,c_9639]) ).
cnf(c_9640,plain,
converse(A) = composition(converse(one),converse(A)),
inference(paramod,[status(thm)],[c_9,c_13]) ).
cnf(c_40,plain,
composition(converse(one),converse(A)) = converse(A),
inference(copy,[status(thm)],[c_9640]) ).
cnf(c_9641,plain,
join(complement(A),B) = join(complement(A),join(composition(converse(C),complement(composition(C,A))),B)),
inference(paramod,[status(thm)],[c_15,c_3]) ).
cnf(c_42,plain,
join(complement(A),join(composition(converse(B),complement(composition(B,A))),C)) = join(complement(A),C),
inference(copy,[status(thm)],[c_9641]) ).
cnf(c_9642,plain,
join(top,A) = join(B,join(complement(B),A)),
inference(paramod,[status(thm)],[c_17,c_3]) ).
cnf(c_50,plain,
join(A,join(complement(A),B)) = join(top,B),
inference(copy,[status(thm)],[c_9642]) ).
cnf(c_9643,plain,
join(complement(top),complement(join(complement(A),complement(complement(complement(A)))))) = A,
inference(paramod,[status(thm)],[c_17,c_5]) ).
cnf(c_52,plain,
join(zero,complement(join(complement(A),complement(complement(complement(A)))))) = A,
inference(paramod,[status(thm)],[c_19,c_9643]) ).
cnf(c_9644,plain,
composition(top,A) = join(composition(B,A),composition(complement(B),A)),
inference(paramod,[status(thm)],[c_17,c_10]) ).
cnf(c_54,plain,
join(composition(A,B),composition(complement(A),B)) = composition(top,B),
inference(copy,[status(thm)],[c_9644]) ).
cnf(c_9645,plain,
converse(top) = join(converse(A),converse(complement(A))),
inference(paramod,[status(thm)],[c_17,c_12]) ).
cnf(c_55,plain,
join(converse(A),converse(complement(A))) = converse(top),
inference(copy,[status(thm)],[c_9645]) ).
cnf(c_63,plain,
join(complement(join(complement(A),complement(B))),composition(complement(join(complement(A),complement(composition(B,converse(one))))),complement(join(complement(one),complement(composition(converse(A),B)))))) = composition(complement(join(complement(A),complement(composition(B,converse(one))))),complement(join(complement(one),complement(composition(converse(A),B))))),
inference(paramod,[status(thm)],[c_9,c_21]) ).
cnf(c_9646,plain,
join(complement(join(complement(composition(A,B)),complement(one))),complement(join(complement(one),complement(composition(A,complement(join(complement(B),complement(converse(A))))))))) = complement(join(complement(one),complement(composition(A,complement(join(complement(B),complement(composition(converse(A),one)))))))),
inference(paramod,[status(thm)],[c_9,c_23]) ).
cnf(c_9647,plain,
join(complement(join(complement(one),complement(composition(A,B)))),complement(join(complement(one),complement(composition(A,complement(join(complement(B),complement(converse(A))))))))) = complement(join(complement(one),complement(composition(A,complement(join(complement(B),complement(composition(converse(A),one)))))))),
inference(paramod,[status(thm)],[c_1,c_9646]) ).
cnf(c_75,plain,
join(complement(join(complement(one),complement(composition(A,B)))),complement(join(complement(one),complement(composition(A,complement(join(complement(B),complement(converse(A))))))))) = complement(join(complement(one),complement(composition(A,complement(join(complement(B),complement(converse(A)))))))),
inference(paramod,[status(thm)],[c_9,c_9647]) ).
cnf(c_9648,plain,
join(one,A) = join(one,join(sk1,A)),
inference(paramod,[status(thm)],[c_27,c_3]) ).
cnf(c_85,plain,
join(one,join(sk1,A)) = join(one,A),
inference(copy,[status(thm)],[c_9648]) ).
cnf(c_9649,plain,
composition(one,A) = join(composition(one,A),composition(sk1,A)),
inference(paramod,[status(thm)],[c_27,c_10]) ).
cnf(c_87,plain,
join(composition(one,A),composition(sk1,A)) = composition(one,A),
inference(copy,[status(thm)],[c_9649]) ).
cnf(c_9650,plain,
converse(one) = join(converse(one),converse(sk1)),
inference(paramod,[status(thm)],[c_27,c_12]) ).
cnf(c_88,plain,
join(converse(one),converse(sk1)) = converse(one),
inference(copy,[status(thm)],[c_9650]) ).
cnf(c_9651,plain,
A = join(complement(join(complement(A),complement(B))),complement(join(B,complement(A)))),
inference(paramod,[status(thm)],[c_32,c_1]) ).
cnf(c_94,plain,
join(complement(join(complement(A),complement(B))),complement(join(B,complement(A)))) = A,
inference(copy,[status(thm)],[c_9651]) ).
cnf(c_9652,plain,
join(complement(join(complement(complement(A)),A)),complement(top)) = complement(A),
inference(paramod,[status(thm)],[c_17,c_33]) ).
cnf(c_9653,plain,
join(complement(join(A,complement(complement(A)))),complement(top)) = complement(A),
inference(paramod,[status(thm)],[c_1,c_9652]) ).
cnf(c_9654,plain,
join(complement(join(A,complement(complement(A)))),zero) = complement(A),
inference(paramod,[status(thm)],[c_19,c_9653]) ).
cnf(c_113,plain,
join(zero,complement(join(A,complement(complement(A))))) = complement(A),
inference(paramod,[status(thm)],[c_1,c_9654]) ).
cnf(c_9655,plain,
join(complement(join(complement(join(complement(A),complement(B))),join(complement(B),A))),complement(B)) = join(complement(A),complement(B)),
inference(paramod,[status(thm)],[c_33,c_33]) ).
cnf(c_9656,plain,
join(complement(join(join(complement(B),A),complement(join(complement(A),complement(B))))),complement(B)) = join(complement(A),complement(B)),
inference(paramod,[status(thm)],[c_1,c_9655]) ).
cnf(c_9657,plain,
join(complement(join(complement(B),join(A,complement(join(complement(A),complement(B)))))),complement(B)) = join(complement(A),complement(B)),
inference(paramod,[status(thm)],[c_3,c_9656]) ).
cnf(c_118,plain,
join(complement(A),complement(join(complement(A),join(B,complement(join(complement(B),complement(A))))))) = join(complement(B),complement(A)),
inference(paramod,[status(thm)],[c_1,c_9657]) ).
cnf(c_119,plain,
complement(complement(A)) = A,
inference(paramod,[status(thm)],[c_113,c_52]) ).
cnf(c_120,plain,
join(zero,complement(join(A,A))) = complement(A),
inference(paramod,[status(thm)],[c_119,c_113]) ).
cnf(c_9658,plain,
( join(complement(join(complement(complement(sk3)),complement(composition(sk1,sk2)))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3)))))) != complement(join(complement(complement(sk3)),complement(composition(sk1,sk2))))
| join(complement(join(sk3,complement(composition(sk1,sk2)))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3)))))) != complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))) ),
inference(paramod,[status(thm)],[c_119,c_29]) ).
cnf(c_9659,plain,
( join(complement(join(complement(complement(sk3)),complement(composition(sk1,sk2)))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3)))))) != complement(join(complement(complement(sk3)),complement(composition(sk1,sk2))))
| join(complement(join(sk3,complement(composition(sk1,sk2)))),complement(join(complement(composition(sk1,sk2)),composition(sk1,sk3)))) != complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3))))) ),
inference(paramod,[status(thm)],[c_119,c_9658]) ).
cnf(c_9660,plain,
( join(complement(join(complement(complement(sk3)),complement(composition(sk1,sk2)))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3)))))) != complement(join(complement(complement(sk3)),complement(composition(sk1,sk2))))
| join(complement(join(sk3,complement(composition(sk1,sk2)))),complement(join(complement(composition(sk1,sk2)),composition(sk1,sk3)))) != complement(join(complement(composition(sk1,sk2)),composition(sk1,sk3))) ),
inference(paramod,[status(thm)],[c_119,c_9659]) ).
cnf(c_9661,plain,
( join(complement(join(sk3,complement(composition(sk1,sk2)))),complement(join(complement(composition(sk1,sk2)),complement(complement(composition(sk1,sk3)))))) != complement(join(complement(complement(sk3)),complement(composition(sk1,sk2))))
| join(complement(join(sk3,complement(composition(sk1,sk2)))),complement(join(complement(composition(sk1,sk2)),composition(sk1,sk3)))) != complement(join(complement(composition(sk1,sk2)),composition(sk1,sk3))) ),
inference(paramod,[status(thm)],[c_119,c_9660]) ).
cnf(c_9662,plain,
( join(complement(join(sk3,complement(composition(sk1,sk2)))),complement(join(complement(composition(sk1,sk2)),composition(sk1,sk3)))) != complement(join(complement(complement(sk3)),complement(composition(sk1,sk2))))
| join(complement(join(sk3,complement(composition(sk1,sk2)))),complement(join(complement(composition(sk1,sk2)),composition(sk1,sk3)))) != complement(join(complement(composition(sk1,sk2)),composition(sk1,sk3))) ),
inference(paramod,[status(thm)],[c_119,c_9661]) ).
cnf(c_123,plain,
( join(complement(join(sk3,complement(composition(sk1,sk2)))),complement(join(complement(composition(sk1,sk2)),composition(sk1,sk3)))) != complement(join(sk3,complement(composition(sk1,sk2))))
| join(complement(join(sk3,complement(composition(sk1,sk2)))),complement(join(complement(composition(sk1,sk2)),composition(sk1,sk3)))) != complement(join(complement(composition(sk1,sk2)),composition(sk1,sk3))) ),
inference(paramod,[status(thm)],[c_119,c_9662]) ).
cnf(c_9663,plain,
composition(converse(one),A) = converse(converse(A)),
inference(paramod,[status(thm)],[c_11,c_40]) ).
cnf(c_130,plain,
composition(converse(one),A) = A,
inference(paramod,[status(thm)],[c_11,c_9663]) ).
cnf(c_9664,plain,
join(complement(join(complement(converse(A)),complement(B))),composition(complement(join(complement(converse(one)),complement(composition(B,converse(converse(A)))))),complement(join(complement(converse(A)),complement(composition(converse(converse(one)),B)))))) = composition(complement(join(complement(converse(one)),complement(composition(B,converse(converse(A)))))),complement(join(complement(converse(A)),complement(composition(converse(converse(one)),B))))),
inference(paramod,[status(thm)],[c_40,c_21]) ).
cnf(c_9665,plain,
join(complement(join(complement(converse(A)),complement(B))),composition(complement(join(complement(converse(one)),complement(composition(B,A)))),complement(join(complement(converse(A)),complement(composition(converse(converse(one)),B)))))) = composition(complement(join(complement(converse(one)),complement(composition(B,converse(converse(A)))))),complement(join(complement(converse(A)),complement(composition(converse(converse(one)),B))))),
inference(paramod,[status(thm)],[c_11,c_9664]) ).
cnf(c_9666,plain,
join(complement(join(complement(converse(A)),complement(B))),composition(complement(join(complement(converse(one)),complement(composition(B,A)))),complement(join(complement(converse(A)),complement(composition(one,B)))))) = composition(complement(join(complement(converse(one)),complement(composition(B,converse(converse(A)))))),complement(join(complement(converse(A)),complement(composition(converse(converse(one)),B))))),
inference(paramod,[status(thm)],[c_11,c_9665]) ).
cnf(c_9667,plain,
join(complement(join(complement(converse(A)),complement(B))),composition(complement(join(complement(converse(one)),complement(composition(B,A)))),complement(join(complement(converse(A)),complement(composition(one,B)))))) = composition(complement(join(complement(converse(one)),complement(composition(B,A)))),complement(join(complement(converse(A)),complement(composition(converse(converse(one)),B))))),
inference(paramod,[status(thm)],[c_11,c_9666]) ).
cnf(c_132,plain,
join(complement(join(complement(converse(A)),complement(B))),composition(complement(join(complement(converse(one)),complement(composition(B,A)))),complement(join(complement(converse(A)),complement(composition(one,B)))))) = composition(complement(join(complement(converse(one)),complement(composition(B,A)))),complement(join(complement(converse(A)),complement(composition(one,B))))),
inference(paramod,[status(thm)],[c_11,c_9667]) ).
cnf(c_9668,plain,
join(complement(join(complement(converse(A)),complement(B))),complement(join(complement(B),complement(composition(complement(join(complement(converse(one)),complement(composition(B,converse(converse(A)))))),converse(A)))))) = complement(join(complement(B),complement(composition(complement(join(complement(converse(one)),complement(composition(B,converse(converse(A)))))),converse(A))))),
inference(paramod,[status(thm)],[c_40,c_25]) ).
cnf(c_9669,plain,
join(complement(join(complement(converse(A)),complement(B))),complement(join(complement(B),complement(composition(complement(join(complement(converse(one)),complement(composition(B,A)))),converse(A)))))) = complement(join(complement(B),complement(composition(complement(join(complement(converse(one)),complement(composition(B,converse(converse(A)))))),converse(A))))),
inference(paramod,[status(thm)],[c_11,c_9668]) ).
cnf(c_137,plain,
join(complement(join(complement(converse(A)),complement(B))),complement(join(complement(B),complement(composition(complement(join(complement(converse(one)),complement(composition(B,A)))),converse(A)))))) = complement(join(complement(B),complement(composition(complement(join(complement(converse(one)),complement(composition(B,A)))),converse(A))))),
inference(paramod,[status(thm)],[c_11,c_9669]) ).
cnf(c_9670,plain,
one = converse(one),
inference(paramod,[status(thm)],[c_130,c_9]) ).
cnf(c_139,plain,
converse(one) = one,
inference(copy,[status(thm)],[c_9670]) ).
cnf(c_143,plain,
join(complement(A),complement(composition(one,A))) = complement(A),
inference(paramod,[status(thm)],[c_130,c_15]) ).
cnf(c_9671,plain,
join(complement(join(complement(converse(A)),complement(B))),complement(join(complement(B),complement(composition(complement(join(complement(one),complement(composition(B,A)))),converse(A)))))) = complement(join(complement(B),complement(composition(complement(join(complement(converse(one)),complement(composition(B,A)))),converse(A))))),
inference(paramod,[status(thm)],[c_139,c_137]) ).
cnf(c_155,plain,
join(complement(join(complement(converse(A)),complement(B))),complement(join(complement(B),complement(composition(complement(join(complement(one),complement(composition(B,A)))),converse(A)))))) = complement(join(complement(B),complement(composition(complement(join(complement(one),complement(composition(B,A)))),converse(A))))),
inference(paramod,[status(thm)],[c_139,c_9671]) ).
cnf(c_9672,plain,
join(complement(join(complement(converse(A)),complement(B))),composition(complement(join(complement(one),complement(composition(B,A)))),complement(join(complement(converse(A)),complement(composition(one,B)))))) = composition(complement(join(complement(converse(one)),complement(composition(B,A)))),complement(join(complement(converse(A)),complement(composition(one,B))))),
inference(paramod,[status(thm)],[c_139,c_132]) ).
cnf(c_157,plain,
join(complement(join(complement(converse(A)),complement(B))),composition(complement(join(complement(one),complement(composition(B,A)))),complement(join(complement(converse(A)),complement(composition(one,B)))))) = composition(complement(join(complement(one),complement(composition(B,A)))),complement(join(complement(converse(A)),complement(composition(one,B))))),
inference(paramod,[status(thm)],[c_139,c_9672]) ).
cnf(c_158,plain,
composition(one,A) = A,
inference(paramod,[status(thm)],[c_139,c_130]) ).
cnf(c_9673,plain,
join(one,converse(sk1)) = converse(one),
inference(paramod,[status(thm)],[c_139,c_88]) ).
cnf(c_160,plain,
join(one,converse(sk1)) = one,
inference(paramod,[status(thm)],[c_139,c_9673]) ).
cnf(c_9674,plain,
join(complement(join(complement(A),complement(B))),composition(complement(join(complement(A),complement(composition(B,one)))),complement(join(complement(one),complement(composition(converse(A),B)))))) = composition(complement(join(complement(A),complement(composition(B,converse(one))))),complement(join(complement(one),complement(composition(converse(A),B))))),
inference(paramod,[status(thm)],[c_139,c_63]) ).
cnf(c_9675,plain,
join(complement(join(complement(A),complement(B))),composition(complement(join(complement(A),complement(B))),complement(join(complement(one),complement(composition(converse(A),B)))))) = composition(complement(join(complement(A),complement(composition(B,converse(one))))),complement(join(complement(one),complement(composition(converse(A),B))))),
inference(paramod,[status(thm)],[c_9,c_9674]) ).
cnf(c_9676,plain,
join(complement(join(complement(A),complement(B))),composition(complement(join(complement(A),complement(B))),complement(join(complement(one),complement(composition(converse(A),B)))))) = composition(complement(join(complement(A),complement(composition(B,one)))),complement(join(complement(one),complement(composition(converse(A),B))))),
inference(paramod,[status(thm)],[c_139,c_9675]) ).
cnf(c_161,plain,
join(complement(join(complement(A),complement(B))),composition(complement(join(complement(A),complement(B))),complement(join(complement(one),complement(composition(converse(A),B)))))) = composition(complement(join(complement(A),complement(B))),complement(join(complement(one),complement(composition(converse(A),B))))),
inference(paramod,[status(thm)],[c_9,c_9676]) ).
cnf(c_9677,plain,
join(A,composition(sk1,A)) = composition(one,A),
inference(paramod,[status(thm)],[c_158,c_87]) ).
cnf(c_162,plain,
join(A,composition(sk1,A)) = A,
inference(paramod,[status(thm)],[c_158,c_9677]) ).
cnf(c_9678,plain,
join(complement(join(complement(converse(A)),complement(B))),composition(complement(join(complement(one),complement(composition(B,A)))),complement(join(complement(converse(A)),complement(B))))) = composition(complement(join(complement(one),complement(composition(B,A)))),complement(join(complement(converse(A)),complement(composition(one,B))))),
inference(paramod,[status(thm)],[c_158,c_157]) ).
cnf(c_164,plain,
join(complement(join(complement(converse(A)),complement(B))),composition(complement(join(complement(one),complement(composition(B,A)))),complement(join(complement(converse(A)),complement(B))))) = composition(complement(join(complement(one),complement(composition(B,A)))),complement(join(complement(converse(A)),complement(B)))),
inference(paramod,[status(thm)],[c_158,c_9678]) ).
cnf(c_165,plain,
join(complement(A),complement(A)) = complement(A),
inference(paramod,[status(thm)],[c_158,c_143]) ).
cnf(c_9679,plain,
composition(one,A) = join(composition(one,A),composition(converse(sk1),A)),
inference(paramod,[status(thm)],[c_160,c_10]) ).
cnf(c_9680,plain,
A = join(composition(one,A),composition(converse(sk1),A)),
inference(paramod,[status(thm)],[c_158,c_9679]) ).
cnf(c_9681,plain,
A = join(A,composition(converse(sk1),A)),
inference(paramod,[status(thm)],[c_158,c_9680]) ).
cnf(c_167,plain,
join(A,composition(converse(sk1),A)) = A,
inference(copy,[status(thm)],[c_9681]) ).
cnf(c_9682,plain,
join(complement(join(complement(A),B)),B) = join(A,complement(join(complement(B),complement(complement(A))))),
inference(paramod,[status(thm)],[c_32,c_34]) ).
cnf(c_9683,plain,
join(B,complement(join(complement(A),B))) = join(A,complement(join(complement(B),complement(complement(A))))),
inference(paramod,[status(thm)],[c_1,c_9682]) ).
cnf(c_188,plain,
join(A,complement(join(complement(B),A))) = join(B,complement(join(complement(A),B))),
inference(paramod,[status(thm)],[c_119,c_9683]) ).
cnf(c_9684,plain,
join(A,join(complement(B),C)) = join(complement(B),join(A,complement(join(complement(B),join(complement(C),complement(join(complement(B),C))))))),
inference(paramod,[status(thm)],[c_36,c_31]) ).
cnf(c_201,plain,
join(complement(A),join(B,complement(join(complement(A),join(complement(C),complement(join(complement(A),C))))))) = join(B,join(complement(A),C)),
inference(copy,[status(thm)],[c_9684]) ).
cnf(c_9685,plain,
join(complement(join(complement(A),B)),complement(join(complement(join(complement(A),join(complement(B),complement(join(complement(A),B))))),complement(complement(A))))) = join(complement(A),join(complement(B),complement(join(complement(A),B)))),
inference(paramod,[status(thm)],[c_36,c_32]) ).
cnf(c_9686,plain,
join(complement(join(complement(A),B)),complement(join(complement(join(complement(A),join(complement(B),complement(join(complement(A),B))))),A))) = join(complement(A),join(complement(B),complement(join(complement(A),B)))),
inference(paramod,[status(thm)],[c_119,c_9685]) ).
cnf(c_203,plain,
join(complement(join(complement(A),B)),complement(join(A,complement(join(complement(A),join(complement(B),complement(join(complement(A),B)))))))) = join(complement(A),join(complement(B),complement(join(complement(A),B)))),
inference(paramod,[status(thm)],[c_1,c_9686]) ).
cnf(c_9687,plain,
join(complement(join(complement(A),B)),complement(join(complement(join(complement(A),B)),join(complement(join(complement(join(complement(A),complement(B))),C)),complement(join(A,C)))))) = join(complement(join(complement(A),B)),join(complement(join(complement(A),complement(B))),C)),
inference(paramod,[status(thm)],[c_34,c_36]) ).
cnf(c_9688,plain,
join(complement(join(complement(A),B)),complement(join(complement(join(complement(A),B)),join(complement(join(A,C)),complement(join(complement(join(complement(A),complement(B))),C)))))) = join(complement(join(complement(A),B)),join(complement(join(complement(A),complement(B))),C)),
inference(paramod,[status(thm)],[c_1,c_9687]) ).
cnf(c_209,plain,
join(complement(join(complement(A),B)),complement(join(complement(join(complement(A),B)),join(complement(join(A,C)),complement(join(complement(join(complement(A),complement(B))),C)))))) = join(A,C),
inference(paramod,[status(thm)],[c_34,c_9688]) ).
cnf(c_9689,plain,
converse(A) = join(converse(A),converse(composition(sk1,A))),
inference(paramod,[status(thm)],[c_162,c_12]) ).
cnf(c_9690,plain,
converse(A) = join(converse(A),composition(converse(A),converse(sk1))),
inference(paramod,[status(thm)],[c_13,c_9689]) ).
cnf(c_227,plain,
join(converse(A),composition(converse(A),converse(sk1))) = converse(A),
inference(copy,[status(thm)],[c_9690]) ).
cnf(c_9691,plain,
join(complement(join(complement(A),A)),complement(complement(A))) = A,
inference(paramod,[status(thm)],[c_165,c_5]) ).
cnf(c_9692,plain,
join(complement(join(A,complement(A))),complement(complement(A))) = A,
inference(paramod,[status(thm)],[c_1,c_9691]) ).
cnf(c_9693,plain,
join(complement(top),complement(complement(A))) = A,
inference(paramod,[status(thm)],[c_17,c_9692]) ).
cnf(c_9694,plain,
join(zero,complement(complement(A))) = A,
inference(paramod,[status(thm)],[c_19,c_9693]) ).
cnf(c_239,plain,
join(zero,A) = A,
inference(paramod,[status(thm)],[c_119,c_9694]) ).
cnf(c_9695,plain,
join(complement(join(complement(A),B)),complement(join(complement(A),complement(B)))) = join(A,complement(join(complement(A),complement(B)))),
inference(paramod,[status(thm)],[c_165,c_34]) ).
cnf(c_9696,plain,
A = join(A,complement(join(complement(A),complement(B)))),
inference(paramod,[status(thm)],[c_5,c_9695]) ).
cnf(c_242,plain,
join(A,complement(join(complement(A),complement(B)))) = A,
inference(copy,[status(thm)],[c_9696]) ).
cnf(c_251,plain,
complement(join(A,A)) = complement(A),
inference(paramod,[status(thm)],[c_239,c_120]) ).
cnf(c_261,plain,
join(complement(A),complement(join(complement(A),B))) = join(complement(B),complement(A)),
inference(paramod,[status(thm)],[c_242,c_118]) ).
cnf(c_9697,plain,
join(complement(join(complement(join(A,C)),complement(join(complement(join(complement(A),complement(B))),C)))),complement(join(complement(A),B))) = join(A,C),
inference(paramod,[status(thm)],[c_261,c_209]) ).
cnf(c_263,plain,
join(complement(join(complement(A),B)),complement(join(complement(join(A,C)),complement(join(complement(join(complement(A),complement(B))),C))))) = join(A,C),
inference(paramod,[status(thm)],[c_1,c_9697]) ).
cnf(c_9698,plain,
join(complement(A),composition(converse(B),complement(composition(B,A)))) = join(complement(A),composition(sk1,composition(converse(B),complement(composition(B,A))))),
inference(paramod,[status(thm)],[c_162,c_42]) ).
cnf(c_9699,plain,
complement(A) = join(complement(A),composition(sk1,composition(converse(B),complement(composition(B,A))))),
inference(paramod,[status(thm)],[c_15,c_9698]) ).
cnf(c_320,plain,
join(complement(A),composition(sk1,composition(converse(B),complement(composition(B,A))))) = complement(A),
inference(copy,[status(thm)],[c_9699]) ).
cnf(c_9700,plain,
join(complement(join(complement(A),B)),complement(join(complement(join(A,A)),complement(B)))) = join(A,A),
inference(paramod,[status(thm)],[c_251,c_5]) ).
cnf(c_9701,plain,
join(complement(join(complement(A),B)),complement(join(complement(A),complement(B)))) = join(A,A),
inference(paramod,[status(thm)],[c_251,c_9700]) ).
cnf(c_9702,plain,
A = join(A,A),
inference(paramod,[status(thm)],[c_5,c_9701]) ).
cnf(c_334,plain,
join(A,A) = A,
inference(copy,[status(thm)],[c_9702]) ).
cnf(c_9703,plain,
join(join(A,B),B) = join(A,B),
inference(paramod,[status(thm)],[c_334,c_3]) ).
cnf(c_339,plain,
join(A,join(B,A)) = join(B,A),
inference(paramod,[status(thm)],[c_1,c_9703]) ).
cnf(c_9704,plain,
join(complement(join(complement(A),B)),join(complement(join(complement(A),complement(B))),A)) = A,
inference(paramod,[status(thm)],[c_334,c_34]) ).
cnf(c_9705,plain,
join(complement(join(complement(A),B)),join(A,complement(join(complement(A),complement(B))))) = A,
inference(paramod,[status(thm)],[c_1,c_9704]) ).
cnf(c_9706,plain,
join(complement(join(complement(A),B)),A) = A,
inference(paramod,[status(thm)],[c_242,c_9705]) ).
cnf(c_340,plain,
join(A,complement(join(complement(A),B))) = A,
inference(paramod,[status(thm)],[c_1,c_9706]) ).
cnf(c_9707,plain,
join(complement(join(complement(A),B)),complement(A)) = join(complement(A),join(complement(B),complement(join(complement(A),B)))),
inference(paramod,[status(thm)],[c_340,c_203]) ).
cnf(c_9708,plain,
join(complement(A),complement(join(complement(A),B))) = join(complement(A),join(complement(B),complement(join(complement(A),B)))),
inference(paramod,[status(thm)],[c_1,c_9707]) ).
cnf(c_9709,plain,
join(complement(B),complement(A)) = join(complement(A),join(complement(B),complement(join(complement(A),B)))),
inference(paramod,[status(thm)],[c_261,c_9708]) ).
cnf(c_342,plain,
join(complement(A),join(complement(B),complement(join(complement(A),B)))) = join(complement(B),complement(A)),
inference(copy,[status(thm)],[c_9709]) ).
cnf(c_345,plain,
join(complement(A),join(B,complement(join(complement(C),complement(A))))) = join(B,join(complement(A),C)),
inference(paramod,[status(thm)],[c_342,c_201]) ).
cnf(c_9710,plain,
converse(A) = join(converse(A),converse(composition(converse(sk1),A))),
inference(paramod,[status(thm)],[c_167,c_12]) ).
cnf(c_9711,plain,
converse(A) = join(converse(A),composition(converse(A),converse(converse(sk1)))),
inference(paramod,[status(thm)],[c_13,c_9710]) ).
cnf(c_9712,plain,
converse(A) = join(converse(A),composition(converse(A),sk1)),
inference(paramod,[status(thm)],[c_11,c_9711]) ).
cnf(c_489,plain,
join(converse(A),composition(converse(A),sk1)) = converse(A),
inference(copy,[status(thm)],[c_9712]) ).
cnf(c_9713,plain,
join(A,complement(A)) = join(top,complement(A)),
inference(paramod,[status(thm)],[c_334,c_50]) ).
cnf(c_9714,plain,
top = join(top,complement(A)),
inference(paramod,[status(thm)],[c_17,c_9713]) ).
cnf(c_523,plain,
join(top,complement(A)) = top,
inference(copy,[status(thm)],[c_9714]) ).
cnf(c_9715,plain,
join(A,join(complement(A),top)) = top,
inference(paramod,[status(thm)],[c_334,c_50]) ).
cnf(c_9716,plain,
join(A,join(top,complement(A))) = top,
inference(paramod,[status(thm)],[c_1,c_9715]) ).
cnf(c_524,plain,
join(A,top) = top,
inference(paramod,[status(thm)],[c_523,c_9716]) ).
cnf(c_9717,plain,
top = join(top,A),
inference(paramod,[status(thm)],[c_524,c_1]) ).
cnf(c_558,plain,
join(top,A) = top,
inference(copy,[status(thm)],[c_9717]) ).
cnf(c_9718,plain,
converse(top) = join(converse(A),converse(top)),
inference(paramod,[status(thm)],[c_524,c_12]) ).
cnf(c_560,plain,
join(converse(A),converse(top)) = converse(top),
inference(copy,[status(thm)],[c_9718]) ).
cnf(c_580,plain,
join(A,converse(top)) = converse(top),
inference(paramod,[status(thm)],[c_11,c_560]) ).
cnf(c_583,plain,
converse(top) = top,
inference(paramod,[status(thm)],[c_580,c_558]) ).
cnf(c_594,plain,
join(converse(A),converse(complement(A))) = top,
inference(paramod,[status(thm)],[c_583,c_55]) ).
cnf(c_717,plain,
join(A,converse(complement(converse(A)))) = top,
inference(paramod,[status(thm)],[c_11,c_594]) ).
cnf(c_9719,plain,
join(one,top) = join(one,complement(sk1)),
inference(paramod,[status(thm)],[c_17,c_85]) ).
cnf(c_9720,plain,
top = join(one,complement(sk1)),
inference(paramod,[status(thm)],[c_524,c_9719]) ).
cnf(c_725,plain,
join(one,complement(sk1)) = top,
inference(copy,[status(thm)],[c_9720]) ).
cnf(c_9721,plain,
join(A,composition(converse(converse(A)),sk1)) = converse(converse(A)),
inference(paramod,[status(thm)],[c_11,c_489]) ).
cnf(c_9722,plain,
join(A,composition(A,sk1)) = converse(converse(A)),
inference(paramod,[status(thm)],[c_11,c_9721]) ).
cnf(c_886,plain,
join(A,composition(A,sk1)) = A,
inference(paramod,[status(thm)],[c_11,c_9722]) ).
cnf(c_9723,plain,
join(A,B) = join(A,join(composition(A,sk1),B)),
inference(paramod,[status(thm)],[c_886,c_3]) ).
cnf(c_890,plain,
join(A,join(composition(A,sk1),B)) = join(A,B),
inference(copy,[status(thm)],[c_9723]) ).
cnf(c_9724,plain,
join(complement(join(A,complement(B))),complement(join(B,complement(complement(A))))) = complement(A),
inference(paramod,[status(thm)],[c_119,c_94]) ).
cnf(c_929,plain,
join(complement(join(A,complement(B))),complement(join(B,A))) = complement(A),
inference(paramod,[status(thm)],[c_119,c_9724]) ).
cnf(c_9725,plain,
join(complement(join(complement(sk1),complement(one))),complement(top)) = sk1,
inference(paramod,[status(thm)],[c_725,c_94]) ).
cnf(c_9726,plain,
join(complement(join(complement(one),complement(sk1))),complement(top)) = sk1,
inference(paramod,[status(thm)],[c_1,c_9725]) ).
cnf(c_9727,plain,
join(complement(join(complement(one),complement(sk1))),zero) = sk1,
inference(paramod,[status(thm)],[c_19,c_9726]) ).
cnf(c_9728,plain,
join(zero,complement(join(complement(one),complement(sk1)))) = sk1,
inference(paramod,[status(thm)],[c_1,c_9727]) ).
cnf(c_930,plain,
complement(join(complement(one),complement(sk1))) = sk1,
inference(paramod,[status(thm)],[c_239,c_9728]) ).
cnf(c_9729,plain,
join(complement(join(A,complement(B))),B) = join(complement(join(complement(B),complement(A))),complement(join(A,complement(B)))),
inference(paramod,[status(thm)],[c_94,c_339]) ).
cnf(c_9730,plain,
join(B,complement(join(A,complement(B)))) = join(complement(join(complement(B),complement(A))),complement(join(A,complement(B)))),
inference(paramod,[status(thm)],[c_1,c_9729]) ).
cnf(c_9731,plain,
join(B,complement(join(A,complement(B)))) = complement(complement(B)),
inference(paramod,[status(thm)],[c_929,c_9730]) ).
cnf(c_931,plain,
join(A,complement(join(B,complement(A)))) = A,
inference(paramod,[status(thm)],[c_119,c_9731]) ).
cnf(c_9732,plain,
complement(sk1) = join(complement(one),complement(sk1)),
inference(paramod,[status(thm)],[c_930,c_119]) ).
cnf(c_964,plain,
join(complement(one),complement(sk1)) = complement(sk1),
inference(copy,[status(thm)],[c_9732]) ).
cnf(c_9733,plain,
join(complement(sk1),A) = join(complement(one),join(complement(sk1),A)),
inference(paramod,[status(thm)],[c_964,c_3]) ).
cnf(c_970,plain,
join(complement(one),join(complement(sk1),A)) = join(complement(sk1),A),
inference(copy,[status(thm)],[c_9733]) ).
cnf(c_9734,plain,
join(A,composition(converse(converse(A)),converse(sk1))) = converse(converse(A)),
inference(paramod,[status(thm)],[c_11,c_227]) ).
cnf(c_9735,plain,
join(A,composition(A,converse(sk1))) = converse(converse(A)),
inference(paramod,[status(thm)],[c_11,c_9734]) ).
cnf(c_1148,plain,
join(A,composition(A,converse(sk1))) = A,
inference(paramod,[status(thm)],[c_11,c_9735]) ).
cnf(c_9736,plain,
join(complement(A),join(composition(converse(B),complement(composition(B,A))),complement(join(complement(complement(A)),C)))) = complement(A),
inference(paramod,[status(thm)],[c_340,c_42]) ).
cnf(c_9737,plain,
join(complement(A),join(composition(converse(B),complement(composition(B,A))),complement(join(A,C)))) = complement(A),
inference(paramod,[status(thm)],[c_119,c_9736]) ).
cnf(c_1387,plain,
join(complement(A),complement(join(A,B))) = complement(A),
inference(paramod,[status(thm)],[c_42,c_9737]) ).
cnf(c_1400,plain,
join(complement(A),complement(join(B,A))) = complement(A),
inference(paramod,[status(thm)],[c_1,c_1387]) ).
cnf(c_9738,plain,
join(complement(composition(A,sk1)),complement(A)) = complement(composition(A,sk1)),
inference(paramod,[status(thm)],[c_886,c_1400]) ).
cnf(c_1437,plain,
join(complement(A),complement(composition(A,sk1))) = complement(composition(A,sk1)),
inference(paramod,[status(thm)],[c_1,c_9738]) ).
cnf(c_9739,plain,
join(complement(composition(A,converse(sk1))),complement(A)) = complement(composition(A,converse(sk1))),
inference(paramod,[status(thm)],[c_1148,c_1400]) ).
cnf(c_1439,plain,
join(complement(A),complement(composition(A,converse(sk1)))) = complement(composition(A,converse(sk1))),
inference(paramod,[status(thm)],[c_1,c_9739]) ).
cnf(c_9740,plain,
join(complement(complement(sk1)),composition(complement(join(complement(one),complement(sk1))),complement(join(complement(one),complement(composition(converse(one),sk1)))))) = composition(complement(join(complement(one),complement(sk1))),complement(join(complement(one),complement(composition(converse(one),sk1))))),
inference(paramod,[status(thm)],[c_964,c_161]) ).
cnf(c_9741,plain,
join(sk1,composition(complement(join(complement(one),complement(sk1))),complement(join(complement(one),complement(composition(converse(one),sk1)))))) = composition(complement(join(complement(one),complement(sk1))),complement(join(complement(one),complement(composition(converse(one),sk1))))),
inference(paramod,[status(thm)],[c_119,c_9740]) ).
cnf(c_9742,plain,
join(sk1,composition(complement(complement(sk1)),complement(join(complement(one),complement(composition(converse(one),sk1)))))) = composition(complement(join(complement(one),complement(sk1))),complement(join(complement(one),complement(composition(converse(one),sk1))))),
inference(paramod,[status(thm)],[c_964,c_9741]) ).
cnf(c_9743,plain,
join(sk1,composition(sk1,complement(join(complement(one),complement(composition(converse(one),sk1)))))) = composition(complement(join(complement(one),complement(sk1))),complement(join(complement(one),complement(composition(converse(one),sk1))))),
inference(paramod,[status(thm)],[c_119,c_9742]) ).
cnf(c_9744,plain,
join(sk1,composition(sk1,complement(join(complement(one),complement(composition(one,sk1)))))) = composition(complement(join(complement(one),complement(sk1))),complement(join(complement(one),complement(composition(converse(one),sk1))))),
inference(paramod,[status(thm)],[c_139,c_9743]) ).
cnf(c_9745,plain,
join(sk1,composition(sk1,complement(join(complement(one),complement(sk1))))) = composition(complement(join(complement(one),complement(sk1))),complement(join(complement(one),complement(composition(converse(one),sk1))))),
inference(paramod,[status(thm)],[c_158,c_9744]) ).
cnf(c_9746,plain,
join(sk1,composition(sk1,complement(complement(sk1)))) = composition(complement(join(complement(one),complement(sk1))),complement(join(complement(one),complement(composition(converse(one),sk1))))),
inference(paramod,[status(thm)],[c_964,c_9745]) ).
cnf(c_9747,plain,
join(sk1,composition(sk1,sk1)) = composition(complement(join(complement(one),complement(sk1))),complement(join(complement(one),complement(composition(converse(one),sk1))))),
inference(paramod,[status(thm)],[c_119,c_9746]) ).
cnf(c_9748,plain,
sk1 = composition(complement(join(complement(one),complement(sk1))),complement(join(complement(one),complement(composition(converse(one),sk1))))),
inference(paramod,[status(thm)],[c_886,c_9747]) ).
cnf(c_9749,plain,
sk1 = composition(complement(complement(sk1)),complement(join(complement(one),complement(composition(converse(one),sk1))))),
inference(paramod,[status(thm)],[c_964,c_9748]) ).
cnf(c_9750,plain,
sk1 = composition(sk1,complement(join(complement(one),complement(composition(converse(one),sk1))))),
inference(paramod,[status(thm)],[c_119,c_9749]) ).
cnf(c_9751,plain,
sk1 = composition(sk1,complement(join(complement(one),complement(composition(one,sk1))))),
inference(paramod,[status(thm)],[c_139,c_9750]) ).
cnf(c_9752,plain,
sk1 = composition(sk1,complement(join(complement(one),complement(sk1)))),
inference(paramod,[status(thm)],[c_158,c_9751]) ).
cnf(c_9753,plain,
sk1 = composition(sk1,complement(complement(sk1))),
inference(paramod,[status(thm)],[c_964,c_9752]) ).
cnf(c_9754,plain,
sk1 = composition(sk1,sk1),
inference(paramod,[status(thm)],[c_119,c_9753]) ).
cnf(c_1464,plain,
composition(sk1,sk1) = sk1,
inference(copy,[status(thm)],[c_9754]) ).
cnf(c_9755,plain,
join(complement(join(complement(one),complement(sk1))),complement(join(complement(one),complement(composition(sk1,complement(join(complement(sk1),complement(converse(sk1))))))))) = complement(join(complement(one),complement(composition(sk1,complement(join(complement(sk1),complement(converse(sk1)))))))),
inference(paramod,[status(thm)],[c_1464,c_75]) ).
cnf(c_9756,plain,
join(complement(complement(sk1)),complement(join(complement(one),complement(composition(sk1,complement(join(complement(sk1),complement(converse(sk1))))))))) = complement(join(complement(one),complement(composition(sk1,complement(join(complement(sk1),complement(converse(sk1)))))))),
inference(paramod,[status(thm)],[c_964,c_9755]) ).
cnf(c_1514,plain,
join(sk1,complement(join(complement(one),complement(composition(sk1,complement(join(complement(sk1),complement(converse(sk1))))))))) = complement(join(complement(one),complement(composition(sk1,complement(join(complement(sk1),complement(converse(sk1)))))))),
inference(paramod,[status(thm)],[c_119,c_9756]) ).
cnf(c_9757,plain,
join(complement(join(complement(converse(sk1)),complement(sk1))),complement(join(complement(sk1),complement(composition(complement(join(complement(one),complement(sk1))),converse(sk1)))))) = complement(join(complement(sk1),complement(composition(complement(join(complement(one),complement(composition(sk1,sk1)))),converse(sk1))))),
inference(paramod,[status(thm)],[c_1464,c_155]) ).
cnf(c_9758,plain,
join(complement(join(complement(sk1),complement(converse(sk1)))),complement(join(complement(sk1),complement(composition(complement(join(complement(one),complement(sk1))),converse(sk1)))))) = complement(join(complement(sk1),complement(composition(complement(join(complement(one),complement(composition(sk1,sk1)))),converse(sk1))))),
inference(paramod,[status(thm)],[c_1,c_9757]) ).
cnf(c_9759,plain,
join(complement(join(complement(sk1),complement(converse(sk1)))),complement(join(complement(sk1),complement(composition(complement(complement(sk1)),converse(sk1)))))) = complement(join(complement(sk1),complement(composition(complement(join(complement(one),complement(composition(sk1,sk1)))),converse(sk1))))),
inference(paramod,[status(thm)],[c_964,c_9758]) ).
cnf(c_9760,plain,
join(complement(join(complement(sk1),complement(converse(sk1)))),complement(join(complement(sk1),complement(composition(sk1,converse(sk1)))))) = complement(join(complement(sk1),complement(composition(complement(join(complement(one),complement(composition(sk1,sk1)))),converse(sk1))))),
inference(paramod,[status(thm)],[c_119,c_9759]) ).
cnf(c_9761,plain,
join(complement(join(complement(sk1),complement(converse(sk1)))),complement(complement(composition(sk1,converse(sk1))))) = complement(join(complement(sk1),complement(composition(complement(join(complement(one),complement(composition(sk1,sk1)))),converse(sk1))))),
inference(paramod,[status(thm)],[c_1439,c_9760]) ).
cnf(c_9762,plain,
join(complement(join(complement(sk1),complement(converse(sk1)))),composition(sk1,converse(sk1))) = complement(join(complement(sk1),complement(composition(complement(join(complement(one),complement(composition(sk1,sk1)))),converse(sk1))))),
inference(paramod,[status(thm)],[c_119,c_9761]) ).
cnf(c_9763,plain,
join(complement(join(complement(sk1),complement(converse(sk1)))),composition(sk1,converse(sk1))) = complement(join(complement(sk1),complement(composition(complement(join(complement(one),complement(sk1))),converse(sk1))))),
inference(paramod,[status(thm)],[c_1464,c_9762]) ).
cnf(c_9764,plain,
join(complement(join(complement(sk1),complement(converse(sk1)))),composition(sk1,converse(sk1))) = complement(join(complement(sk1),complement(composition(complement(complement(sk1)),converse(sk1))))),
inference(paramod,[status(thm)],[c_964,c_9763]) ).
cnf(c_9765,plain,
join(complement(join(complement(sk1),complement(converse(sk1)))),composition(sk1,converse(sk1))) = complement(join(complement(sk1),complement(composition(sk1,converse(sk1))))),
inference(paramod,[status(thm)],[c_119,c_9764]) ).
cnf(c_9766,plain,
join(complement(join(complement(sk1),complement(converse(sk1)))),composition(sk1,converse(sk1))) = complement(complement(composition(sk1,converse(sk1)))),
inference(paramod,[status(thm)],[c_1439,c_9765]) ).
cnf(c_1518,plain,
join(complement(join(complement(sk1),complement(converse(sk1)))),composition(sk1,converse(sk1))) = composition(sk1,converse(sk1)),
inference(paramod,[status(thm)],[c_119,c_9766]) ).
cnf(c_9767,plain,
join(complement(join(complement(converse(sk1)),complement(sk1))),composition(complement(join(complement(one),complement(sk1))),complement(join(complement(converse(sk1)),complement(sk1))))) = composition(complement(join(complement(one),complement(composition(sk1,sk1)))),complement(join(complement(converse(sk1)),complement(sk1)))),
inference(paramod,[status(thm)],[c_1464,c_164]) ).
cnf(c_9768,plain,
join(complement(join(complement(sk1),complement(converse(sk1)))),composition(complement(join(complement(one),complement(sk1))),complement(join(complement(converse(sk1)),complement(sk1))))) = composition(complement(join(complement(one),complement(composition(sk1,sk1)))),complement(join(complement(converse(sk1)),complement(sk1)))),
inference(paramod,[status(thm)],[c_1,c_9767]) ).
cnf(c_9769,plain,
join(complement(join(complement(sk1),complement(converse(sk1)))),composition(complement(complement(sk1)),complement(join(complement(converse(sk1)),complement(sk1))))) = composition(complement(join(complement(one),complement(composition(sk1,sk1)))),complement(join(complement(converse(sk1)),complement(sk1)))),
inference(paramod,[status(thm)],[c_964,c_9768]) ).
cnf(c_9770,plain,
join(complement(join(complement(sk1),complement(converse(sk1)))),composition(sk1,complement(join(complement(converse(sk1)),complement(sk1))))) = composition(complement(join(complement(one),complement(composition(sk1,sk1)))),complement(join(complement(converse(sk1)),complement(sk1)))),
inference(paramod,[status(thm)],[c_119,c_9769]) ).
cnf(c_9771,plain,
join(complement(join(complement(sk1),complement(converse(sk1)))),composition(sk1,complement(join(complement(sk1),complement(converse(sk1)))))) = composition(complement(join(complement(one),complement(composition(sk1,sk1)))),complement(join(complement(converse(sk1)),complement(sk1)))),
inference(paramod,[status(thm)],[c_1,c_9770]) ).
cnf(c_9772,plain,
complement(join(complement(sk1),complement(converse(sk1)))) = composition(complement(join(complement(one),complement(composition(sk1,sk1)))),complement(join(complement(converse(sk1)),complement(sk1)))),
inference(paramod,[status(thm)],[c_162,c_9771]) ).
cnf(c_9773,plain,
complement(join(complement(sk1),complement(converse(sk1)))) = composition(complement(join(complement(one),complement(sk1))),complement(join(complement(converse(sk1)),complement(sk1)))),
inference(paramod,[status(thm)],[c_1464,c_9772]) ).
cnf(c_9774,plain,
complement(join(complement(sk1),complement(converse(sk1)))) = composition(complement(complement(sk1)),complement(join(complement(converse(sk1)),complement(sk1)))),
inference(paramod,[status(thm)],[c_964,c_9773]) ).
cnf(c_9775,plain,
complement(join(complement(sk1),complement(converse(sk1)))) = composition(sk1,complement(join(complement(converse(sk1)),complement(sk1)))),
inference(paramod,[status(thm)],[c_119,c_9774]) ).
cnf(c_9776,plain,
complement(join(complement(sk1),complement(converse(sk1)))) = composition(sk1,complement(join(complement(sk1),complement(converse(sk1))))),
inference(paramod,[status(thm)],[c_1,c_9775]) ).
cnf(c_1520,plain,
composition(sk1,complement(join(complement(sk1),complement(converse(sk1))))) = complement(join(complement(sk1),complement(converse(sk1)))),
inference(copy,[status(thm)],[c_9776]) ).
cnf(c_9777,plain,
join(sk1,complement(join(complement(one),complement(complement(join(complement(sk1),complement(converse(sk1)))))))) = complement(join(complement(one),complement(composition(sk1,complement(join(complement(sk1),complement(converse(sk1)))))))),
inference(paramod,[status(thm)],[c_1520,c_1514]) ).
cnf(c_9778,plain,
join(sk1,complement(join(complement(one),join(complement(sk1),complement(converse(sk1)))))) = complement(join(complement(one),complement(composition(sk1,complement(join(complement(sk1),complement(converse(sk1)))))))),
inference(paramod,[status(thm)],[c_119,c_9777]) ).
cnf(c_9779,plain,
join(sk1,complement(join(complement(sk1),complement(converse(sk1))))) = complement(join(complement(one),complement(composition(sk1,complement(join(complement(sk1),complement(converse(sk1)))))))),
inference(paramod,[status(thm)],[c_970,c_9778]) ).
cnf(c_9780,plain,
sk1 = complement(join(complement(one),complement(composition(sk1,complement(join(complement(sk1),complement(converse(sk1)))))))),
inference(paramod,[status(thm)],[c_340,c_9779]) ).
cnf(c_9781,plain,
sk1 = complement(join(complement(one),complement(complement(join(complement(sk1),complement(converse(sk1))))))),
inference(paramod,[status(thm)],[c_1520,c_9780]) ).
cnf(c_9782,plain,
sk1 = complement(join(complement(one),join(complement(sk1),complement(converse(sk1))))),
inference(paramod,[status(thm)],[c_119,c_9781]) ).
cnf(c_9783,plain,
sk1 = complement(join(complement(sk1),complement(converse(sk1)))),
inference(paramod,[status(thm)],[c_970,c_9782]) ).
cnf(c_1521,plain,
complement(join(complement(sk1),complement(converse(sk1)))) = sk1,
inference(copy,[status(thm)],[c_9783]) ).
cnf(c_9784,plain,
join(sk1,composition(sk1,converse(sk1))) = composition(sk1,converse(sk1)),
inference(paramod,[status(thm)],[c_1521,c_1518]) ).
cnf(c_9785,plain,
sk1 = composition(sk1,converse(sk1)),
inference(paramod,[status(thm)],[c_1148,c_9784]) ).
cnf(c_1522,plain,
composition(sk1,converse(sk1)) = sk1,
inference(copy,[status(thm)],[c_9785]) ).
cnf(c_9786,plain,
converse(sk1) = composition(converse(converse(sk1)),converse(sk1)),
inference(paramod,[status(thm)],[c_1522,c_13]) ).
cnf(c_9787,plain,
converse(sk1) = composition(sk1,converse(sk1)),
inference(paramod,[status(thm)],[c_11,c_9786]) ).
cnf(c_1524,plain,
converse(sk1) = sk1,
inference(paramod,[status(thm)],[c_1522,c_9787]) ).
cnf(c_9788,plain,
join(complement(A),join(composition(converse(B),complement(composition(B,A))),complement(join(complement(C),complement(A))))) = join(C,complement(join(complement(complement(A)),C))),
inference(paramod,[status(thm)],[c_188,c_42]) ).
cnf(c_9789,plain,
join(composition(converse(B),complement(composition(B,A))),join(complement(A),C)) = join(C,complement(join(complement(complement(A)),C))),
inference(paramod,[status(thm)],[c_345,c_9788]) ).
cnf(c_9790,plain,
join(complement(A),join(composition(converse(B),complement(composition(B,A))),C)) = join(C,complement(join(complement(complement(A)),C))),
inference(paramod,[status(thm)],[c_31,c_9789]) ).
cnf(c_9791,plain,
join(complement(A),C) = join(C,complement(join(complement(complement(A)),C))),
inference(paramod,[status(thm)],[c_42,c_9790]) ).
cnf(c_9792,plain,
join(complement(A),C) = join(C,complement(join(A,C))),
inference(paramod,[status(thm)],[c_119,c_9791]) ).
cnf(c_1985,plain,
join(A,complement(join(B,A))) = join(complement(B),A),
inference(copy,[status(thm)],[c_9792]) ).
cnf(c_2104,plain,
join(A,complement(join(A,B))) = join(complement(B),A),
inference(paramod,[status(thm)],[c_1,c_1985]) ).
cnf(c_9793,plain,
join(converse(complement(A)),complement(top)) = join(complement(converse(A)),converse(complement(A))),
inference(paramod,[status(thm)],[c_594,c_1985]) ).
cnf(c_9794,plain,
join(converse(complement(A)),zero) = join(complement(converse(A)),converse(complement(A))),
inference(paramod,[status(thm)],[c_19,c_9793]) ).
cnf(c_9795,plain,
join(zero,converse(complement(A))) = join(complement(converse(A)),converse(complement(A))),
inference(paramod,[status(thm)],[c_1,c_9794]) ).
cnf(c_9796,plain,
converse(complement(A)) = join(complement(converse(A)),converse(complement(A))),
inference(paramod,[status(thm)],[c_239,c_9795]) ).
cnf(c_2115,plain,
join(complement(converse(A)),converse(complement(A))) = converse(complement(A)),
inference(copy,[status(thm)],[c_9796]) ).
cnf(c_9797,plain,
join(converse(complement(converse(A))),complement(top)) = join(complement(A),converse(complement(converse(A)))),
inference(paramod,[status(thm)],[c_717,c_1985]) ).
cnf(c_9798,plain,
join(converse(complement(converse(A))),zero) = join(complement(A),converse(complement(converse(A)))),
inference(paramod,[status(thm)],[c_19,c_9797]) ).
cnf(c_9799,plain,
join(zero,converse(complement(converse(A)))) = join(complement(A),converse(complement(converse(A)))),
inference(paramod,[status(thm)],[c_1,c_9798]) ).
cnf(c_9800,plain,
converse(complement(converse(A))) = join(complement(A),converse(complement(converse(A)))),
inference(paramod,[status(thm)],[c_239,c_9799]) ).
cnf(c_2131,plain,
join(complement(A),converse(complement(converse(A)))) = converse(complement(converse(A))),
inference(copy,[status(thm)],[c_9800]) ).
cnf(c_9801,plain,
join(composition(A,B),complement(composition(top,B))) = join(complement(composition(complement(A),B)),composition(A,B)),
inference(paramod,[status(thm)],[c_54,c_2104]) ).
cnf(c_9802,plain,
join(composition(A,B),complement(composition(top,B))) = join(composition(A,B),complement(composition(complement(A),B))),
inference(paramod,[status(thm)],[c_1,c_9801]) ).
cnf(c_2443,plain,
join(composition(A,B),complement(composition(complement(A),B))) = join(composition(A,B),complement(composition(top,B))),
inference(copy,[status(thm)],[c_9802]) ).
cnf(c_9803,plain,
converse(converse(complement(A))) = join(converse(complement(converse(A))),converse(converse(complement(A)))),
inference(paramod,[status(thm)],[c_2115,c_12]) ).
cnf(c_9804,plain,
complement(A) = join(converse(complement(converse(A))),converse(converse(complement(A)))),
inference(paramod,[status(thm)],[c_11,c_9803]) ).
cnf(c_9805,plain,
complement(A) = join(converse(complement(converse(A))),complement(A)),
inference(paramod,[status(thm)],[c_11,c_9804]) ).
cnf(c_9806,plain,
complement(A) = join(complement(A),converse(complement(converse(A)))),
inference(paramod,[status(thm)],[c_1,c_9805]) ).
cnf(c_9807,plain,
complement(A) = converse(complement(converse(A))),
inference(paramod,[status(thm)],[c_2131,c_9806]) ).
cnf(c_2474,plain,
converse(complement(converse(A))) = complement(A),
inference(copy,[status(thm)],[c_9807]) ).
cnf(c_2482,plain,
converse(complement(A)) = complement(converse(A)),
inference(paramod,[status(thm)],[c_2474,c_11]) ).
cnf(c_9808,plain,
join(complement(join(complement(complement(A)),B)),complement(join(complement(complement(composition(A,sk1))),complement(join(complement(join(complement(complement(A)),complement(B))),complement(composition(A,sk1))))))) = join(complement(A),complement(composition(A,sk1))),
inference(paramod,[status(thm)],[c_1437,c_263]) ).
cnf(c_9809,plain,
join(complement(join(A,B)),complement(join(complement(complement(composition(A,sk1))),complement(join(complement(join(complement(complement(A)),complement(B))),complement(composition(A,sk1))))))) = join(complement(A),complement(composition(A,sk1))),
inference(paramod,[status(thm)],[c_119,c_9808]) ).
cnf(c_9810,plain,
join(complement(join(A,B)),complement(join(composition(A,sk1),complement(join(complement(join(complement(complement(A)),complement(B))),complement(composition(A,sk1))))))) = join(complement(A),complement(composition(A,sk1))),
inference(paramod,[status(thm)],[c_119,c_9809]) ).
cnf(c_9811,plain,
join(complement(join(A,B)),complement(join(composition(A,sk1),complement(join(complement(join(A,complement(B))),complement(composition(A,sk1))))))) = join(complement(A),complement(composition(A,sk1))),
inference(paramod,[status(thm)],[c_119,c_9810]) ).
cnf(c_9812,plain,
join(complement(join(A,B)),complement(composition(A,sk1))) = join(complement(A),complement(composition(A,sk1))),
inference(paramod,[status(thm)],[c_931,c_9811]) ).
cnf(c_3143,plain,
join(complement(join(A,B)),complement(composition(A,sk1))) = complement(composition(A,sk1)),
inference(paramod,[status(thm)],[c_1437,c_9812]) ).
cnf(c_9813,plain,
join(complement(complement(composition(A,sk1))),complement(composition(complement(A),sk1))) = complement(composition(complement(A),sk1)),
inference(paramod,[status(thm)],[c_1437,c_3143]) ).
cnf(c_9814,plain,
join(composition(A,sk1),complement(composition(complement(A),sk1))) = complement(composition(complement(A),sk1)),
inference(paramod,[status(thm)],[c_119,c_9813]) ).
cnf(c_9815,plain,
join(composition(A,sk1),complement(composition(top,sk1))) = complement(composition(complement(A),sk1)),
inference(paramod,[status(thm)],[c_2443,c_9814]) ).
cnf(c_4292,plain,
complement(composition(complement(A),sk1)) = join(composition(A,sk1),complement(composition(top,sk1))),
inference(copy,[status(thm)],[c_9815]) ).
cnf(c_9816,plain,
join(complement(complement(A)),complement(composition(complement(A),sk1))) = complement(composition(complement(A),sk1)),
inference(paramod,[status(thm)],[c_320,c_3143]) ).
cnf(c_9817,plain,
join(A,complement(composition(complement(A),sk1))) = complement(composition(complement(A),sk1)),
inference(paramod,[status(thm)],[c_119,c_9816]) ).
cnf(c_9818,plain,
join(A,join(composition(A,sk1),complement(composition(top,sk1)))) = complement(composition(complement(A),sk1)),
inference(paramod,[status(thm)],[c_4292,c_9817]) ).
cnf(c_9819,plain,
join(A,complement(composition(top,sk1))) = complement(composition(complement(A),sk1)),
inference(paramod,[status(thm)],[c_890,c_9818]) ).
cnf(c_9820,plain,
join(A,complement(composition(top,sk1))) = join(composition(A,sk1),complement(composition(top,sk1))),
inference(paramod,[status(thm)],[c_4292,c_9819]) ).
cnf(c_4316,plain,
join(composition(A,sk1),complement(composition(top,sk1))) = join(A,complement(composition(top,sk1))),
inference(copy,[status(thm)],[c_9820]) ).
cnf(c_4336,plain,
complement(composition(complement(A),sk1)) = join(A,complement(composition(top,sk1))),
inference(paramod,[status(thm)],[c_4316,c_4292]) ).
cnf(c_4410,plain,
complement(composition(A,sk1)) = join(complement(A),complement(composition(top,sk1))),
inference(paramod,[status(thm)],[c_119,c_4336]) ).
cnf(c_9821,plain,
converse(complement(composition(A,sk1))) = join(converse(complement(A)),converse(complement(composition(top,sk1)))),
inference(paramod,[status(thm)],[c_4410,c_12]) ).
cnf(c_9822,plain,
complement(converse(composition(A,sk1))) = join(converse(complement(A)),converse(complement(composition(top,sk1)))),
inference(paramod,[status(thm)],[c_2482,c_9821]) ).
cnf(c_9823,plain,
complement(composition(converse(sk1),converse(A))) = join(converse(complement(A)),converse(complement(composition(top,sk1)))),
inference(paramod,[status(thm)],[c_13,c_9822]) ).
cnf(c_9824,plain,
complement(composition(sk1,converse(A))) = join(converse(complement(A)),converse(complement(composition(top,sk1)))),
inference(paramod,[status(thm)],[c_1524,c_9823]) ).
cnf(c_9825,plain,
complement(composition(sk1,converse(A))) = join(complement(converse(A)),converse(complement(composition(top,sk1)))),
inference(paramod,[status(thm)],[c_2482,c_9824]) ).
cnf(c_9826,plain,
complement(composition(sk1,converse(A))) = join(complement(converse(A)),complement(converse(composition(top,sk1)))),
inference(paramod,[status(thm)],[c_2482,c_9825]) ).
cnf(c_9827,plain,
complement(composition(sk1,converse(A))) = join(complement(converse(A)),complement(composition(converse(sk1),converse(top)))),
inference(paramod,[status(thm)],[c_13,c_9826]) ).
cnf(c_9828,plain,
complement(composition(sk1,converse(A))) = join(complement(converse(A)),complement(composition(sk1,converse(top)))),
inference(paramod,[status(thm)],[c_1524,c_9827]) ).
cnf(c_9829,plain,
complement(composition(sk1,converse(A))) = join(complement(converse(A)),complement(composition(sk1,top))),
inference(paramod,[status(thm)],[c_583,c_9828]) ).
cnf(c_4462,plain,
complement(composition(sk1,converse(A))) = join(complement(composition(sk1,top)),complement(converse(A))),
inference(paramod,[status(thm)],[c_1,c_9829]) ).
cnf(c_9830,plain,
complement(composition(sk1,A)) = join(complement(composition(sk1,top)),complement(converse(converse(A)))),
inference(paramod,[status(thm)],[c_11,c_4462]) ).
cnf(c_5348,plain,
complement(composition(sk1,A)) = join(complement(composition(sk1,top)),complement(A)),
inference(paramod,[status(thm)],[c_11,c_9830]) ).
cnf(c_5387,plain,
complement(composition(sk1,A)) = join(complement(A),complement(composition(sk1,top))),
inference(paramod,[status(thm)],[c_5348,c_1]) ).
cnf(c_9831,plain,
( join(complement(join(sk3,complement(composition(sk1,sk2)))),complement(join(complement(composition(sk1,sk2)),composition(sk1,sk3)))) != complement(join(sk3,complement(composition(sk1,sk2))))
| join(complement(join(sk3,complement(composition(sk1,sk2)))),complement(join(complement(composition(sk1,sk2)),composition(sk1,sk3)))) != complement(join(join(complement(composition(sk1,top)),complement(sk2)),composition(sk1,sk3))) ),
inference(paramod,[status(thm)],[c_5348,c_123]) ).
cnf(c_9832,plain,
( join(complement(join(sk3,complement(composition(sk1,sk2)))),complement(join(complement(composition(sk1,sk2)),composition(sk1,sk3)))) != complement(join(sk3,complement(composition(sk1,sk2))))
| join(complement(join(sk3,complement(composition(sk1,sk2)))),complement(join(complement(composition(sk1,sk2)),composition(sk1,sk3)))) != complement(join(join(complement(sk2),complement(composition(sk1,top))),composition(sk1,sk3))) ),
inference(paramod,[status(thm)],[c_1,c_9831]) ).
cnf(c_5407,plain,
( join(complement(join(sk3,complement(composition(sk1,sk2)))),complement(join(complement(composition(sk1,sk2)),composition(sk1,sk3)))) != complement(join(sk3,complement(composition(sk1,sk2))))
| join(complement(join(sk3,complement(composition(sk1,sk2)))),complement(join(complement(composition(sk1,sk2)),composition(sk1,sk3)))) != complement(join(complement(sk2),join(complement(composition(sk1,top)),composition(sk1,sk3)))) ),
inference(paramod,[status(thm)],[c_3,c_9832]) ).
cnf(c_9833,plain,
join(complement(composition(sk1,top)),complement(complement(composition(sk1,A)))) = join(complement(complement(A)),complement(composition(sk1,top))),
inference(paramod,[status(thm)],[c_5348,c_2104]) ).
cnf(c_9834,plain,
join(complement(composition(sk1,top)),composition(sk1,A)) = join(complement(complement(A)),complement(composition(sk1,top))),
inference(paramod,[status(thm)],[c_119,c_9833]) ).
cnf(c_5475,plain,
join(complement(composition(sk1,top)),composition(sk1,A)) = join(A,complement(composition(sk1,top))),
inference(paramod,[status(thm)],[c_119,c_9834]) ).
cnf(c_9835,plain,
( join(complement(join(sk3,complement(composition(sk1,sk2)))),complement(join(complement(composition(sk1,sk2)),composition(sk1,sk3)))) != complement(join(sk3,join(complement(composition(sk1,top)),complement(sk2))))
| join(complement(join(sk3,complement(composition(sk1,sk2)))),complement(join(complement(composition(sk1,sk2)),composition(sk1,sk3)))) != complement(join(complement(sk2),join(complement(composition(sk1,top)),composition(sk1,sk3)))) ),
inference(paramod,[status(thm)],[c_5348,c_5407]) ).
cnf(c_5646,plain,
( join(complement(join(sk3,complement(composition(sk1,sk2)))),complement(join(complement(composition(sk1,sk2)),composition(sk1,sk3)))) != complement(join(sk3,join(complement(sk2),complement(composition(sk1,top)))))
| join(complement(join(sk3,complement(composition(sk1,sk2)))),complement(join(complement(composition(sk1,sk2)),composition(sk1,sk3)))) != complement(join(complement(sk2),join(complement(composition(sk1,top)),composition(sk1,sk3)))) ),
inference(paramod,[status(thm)],[c_1,c_9835]) ).
cnf(c_9423,plain,
join(complement(composition(sk1,top)),composition(sk1,A)) = join(complement(composition(sk1,top)),A),
inference(paramod,[status(thm)],[c_5475,c_1]) ).
cnf(c_9836,plain,
( join(complement(join(sk3,complement(composition(sk1,sk2)))),complement(join(complement(composition(sk1,sk2)),composition(sk1,sk3)))) != complement(join(sk3,join(complement(sk2),complement(composition(sk1,top)))))
| join(complement(join(sk3,complement(composition(sk1,sk2)))),complement(join(complement(composition(sk1,sk2)),composition(sk1,sk3)))) != complement(join(complement(sk2),join(sk3,complement(composition(sk1,top))))) ),
inference(paramod,[status(thm)],[c_5475,c_5646]) ).
cnf(c_9837,plain,
( join(complement(join(sk3,complement(composition(sk1,sk2)))),complement(join(complement(composition(sk1,sk2)),composition(sk1,sk3)))) != complement(join(sk3,join(complement(sk2),complement(composition(sk1,top)))))
| join(complement(join(sk3,complement(composition(sk1,sk2)))),complement(join(complement(composition(sk1,sk2)),composition(sk1,sk3)))) != complement(join(sk3,join(complement(sk2),complement(composition(sk1,top))))) ),
inference(paramod,[status(thm)],[c_31,c_9836]) ).
cnf(c_9436,plain,
join(complement(join(sk3,complement(composition(sk1,sk2)))),complement(join(complement(composition(sk1,sk2)),composition(sk1,sk3)))) != complement(join(sk3,join(complement(sk2),complement(composition(sk1,top))))),
inference(copy,[status(thm)],[c_9837]) ).
cnf(c_9602,plain,
join(complement(join(sk3,complement(composition(sk1,sk2)))),complement(join(complement(composition(sk1,sk2)),composition(sk1,sk3)))) != complement(join(sk3,complement(composition(sk1,sk2)))),
inference(paramod,[status(thm)],[c_5387,c_9436]) ).
cnf(c_9838,plain,
join(complement(join(sk3,complement(composition(sk1,sk2)))),complement(join(join(complement(composition(sk1,top)),complement(sk2)),composition(sk1,sk3)))) != complement(join(sk3,complement(composition(sk1,sk2)))),
inference(paramod,[status(thm)],[c_5348,c_9602]) ).
cnf(c_9839,plain,
join(complement(join(sk3,complement(composition(sk1,sk2)))),complement(join(join(complement(sk2),complement(composition(sk1,top))),composition(sk1,sk3)))) != complement(join(sk3,complement(composition(sk1,sk2)))),
inference(paramod,[status(thm)],[c_1,c_9838]) ).
cnf(c_9840,plain,
join(complement(join(sk3,complement(composition(sk1,sk2)))),complement(join(complement(sk2),join(complement(composition(sk1,top)),composition(sk1,sk3))))) != complement(join(sk3,complement(composition(sk1,sk2)))),
inference(paramod,[status(thm)],[c_3,c_9839]) ).
cnf(c_9841,plain,
join(complement(join(sk3,complement(composition(sk1,sk2)))),complement(join(complement(sk2),join(complement(composition(sk1,top)),sk3)))) != complement(join(sk3,complement(composition(sk1,sk2)))),
inference(paramod,[status(thm)],[c_9423,c_9840]) ).
cnf(c_9842,plain,
join(complement(join(sk3,complement(composition(sk1,sk2)))),complement(join(complement(sk2),join(sk3,complement(composition(sk1,top)))))) != complement(join(sk3,complement(composition(sk1,sk2)))),
inference(paramod,[status(thm)],[c_1,c_9841]) ).
cnf(c_9843,plain,
join(complement(join(sk3,complement(composition(sk1,sk2)))),complement(join(sk3,join(complement(sk2),complement(composition(sk1,top)))))) != complement(join(sk3,complement(composition(sk1,sk2)))),
inference(paramod,[status(thm)],[c_31,c_9842]) ).
cnf(c_9604,plain,
join(complement(join(sk3,join(complement(sk2),complement(composition(sk1,top))))),complement(join(sk3,complement(composition(sk1,sk2))))) != complement(join(sk3,complement(composition(sk1,sk2)))),
inference(paramod,[status(thm)],[c_1,c_9843]) ).
cnf(c_9844,plain,
join(complement(join(sk3,complement(composition(sk1,sk2)))),complement(join(sk3,complement(composition(sk1,sk2))))) != complement(join(sk3,complement(composition(sk1,sk2)))),
inference(paramod,[status(thm)],[c_5387,c_9604]) ).
cnf(c_9845,plain,
complement(join(sk3,complement(composition(sk1,sk2)))) != complement(join(sk3,complement(composition(sk1,sk2)))),
inference(paramod,[status(thm)],[c_334,c_9844]) ).
cnf(c_9606,plain,
$false,
inference(copy,[status(thm)],[c_9845]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : REL030-4 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.36 % Computer : n007.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Sat Sep 26 05:32:54 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.36 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.08/0.36 % Process 2898488 was started by sandbox2 on n007,
% 0.08/0.36 % Sat Sep 26 05:32:54 2026
% 0.08/0.36 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.08/0.37
% 0.08/0.37 % From the command line: assign(max_seconds, 300).
% 39.05/5.48
% 39.05/5.48 % SZS status Unsatisfiable for theBenchmark
% 39.05/5.48
% 39.05/5.48 % Proof 1 at 4.20 (+ 0.76) seconds.
% 39.05/5.48 % Length of proof is 131.
% 39.05/5.48 % Level of proof is 26.
% 39.05/5.48 % Maximum clause weight is 129.000.
% 39.05/5.48 % Given clauses 473.
% 39.05/5.48
% 39.05/5.48 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------