%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : LAT020-1 : TPTP v9.3.1. Released v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n002.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 07:49:33 AM UTC 2026
% Result : Unsatisfiable 15.23s 4.45s
% Output : CNFRefutation 15.23s
% Verified :
% SZS Type : Refutation
% Derivation depth : 71
% Number of leaves : 10
% Syntax : Number of formulae : 505 ( 505 unt; 0 def)
% Number of atoms : 505 ( 504 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 3 ( 3 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 1 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 5 ( 5 usr; 3 con; 0-2 aty)
% Number of variables : 1493 ( 0 sgn 21 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(idempotence_of_meet,axiom,
! [VAR_0] : meet(VAR_0,VAR_0) = VAR_0,
file('theBenchmark.p',idempotence_of_meet) ).
cnf(c_1,plain,
meet(A,A) = A,
inference(clausify,[status(thm)],[idempotence_of_meet]) ).
fof(idempotence_of_join,axiom,
! [VAR_0] : join(VAR_0,VAR_0) = VAR_0,
file('theBenchmark.p',idempotence_of_join) ).
cnf(c_2,plain,
join(A,A) = A,
inference(clausify,[status(thm)],[idempotence_of_join]) ).
fof(commutativity_of_meet,axiom,
! [VAR_0,VAR_1] : meet(VAR_0,VAR_1) = meet(VAR_1,VAR_0),
file('theBenchmark.p',commutativity_of_meet) ).
cnf(c_3,plain,
meet(A,B) = meet(B,A),
inference(clausify,[status(thm)],[commutativity_of_meet]) ).
fof(commutativity_of_join,axiom,
! [VAR_0,VAR_1] : join(VAR_0,VAR_1) = join(VAR_1,VAR_0),
file('theBenchmark.p',commutativity_of_join) ).
cnf(c_4,plain,
join(A,B) = join(B,A),
inference(clausify,[status(thm)],[commutativity_of_join]) ).
fof(associativity_of_meet,axiom,
! [VAR_0,VAR_1,VAR_2] : meet(meet(VAR_0,VAR_1),VAR_2) = meet(VAR_0,meet(VAR_1,VAR_2)),
file('theBenchmark.p',associativity_of_meet) ).
cnf(c_5,plain,
meet(meet(A,B),C) = meet(A,meet(B,C)),
inference(clausify,[status(thm)],[associativity_of_meet]) ).
fof(associativity_of_join,axiom,
! [VAR_0,VAR_1,VAR_2] : join(join(VAR_0,VAR_1),VAR_2) = join(VAR_0,join(VAR_1,VAR_2)),
file('theBenchmark.p',associativity_of_join) ).
cnf(c_6,plain,
join(join(A,B),C) = join(A,join(B,C)),
inference(clausify,[status(thm)],[associativity_of_join]) ).
fof(quasi_lattice1,axiom,
! [VAR_0,VAR_1,VAR_2] : join(meet(VAR_0,join(VAR_1,VAR_2)),meet(VAR_0,VAR_1)) = meet(VAR_0,join(VAR_1,VAR_2)),
file('theBenchmark.p',quasi_lattice1) ).
cnf(c_7,plain,
join(meet(A,join(B,C)),meet(A,B)) = meet(A,join(B,C)),
inference(clausify,[status(thm)],[quasi_lattice1]) ).
cnf(c_8,plain,
join(meet(A,B),meet(A,join(B,C))) = meet(A,join(B,C)),
inference(paramod,[status(thm)],[c_4,c_7]) ).
fof(quasi_lattice2,axiom,
! [VAR_0,VAR_1,VAR_2] : meet(join(VAR_0,meet(VAR_1,VAR_2)),join(VAR_0,VAR_1)) = join(VAR_0,meet(VAR_1,VAR_2)),
file('theBenchmark.p',quasi_lattice2) ).
cnf(c_9,plain,
meet(join(A,meet(B,C)),join(A,B)) = join(A,meet(B,C)),
inference(clausify,[status(thm)],[quasi_lattice2]) ).
cnf(c_10,plain,
meet(join(A,B),join(A,meet(B,C))) = join(A,meet(B,C)),
inference(paramod,[status(thm)],[c_3,c_9]) ).
fof(self_dual_distributivity,axiom,
! [VAR_0,VAR_1,VAR_2] : join(meet(join(meet(VAR_0,VAR_1),VAR_2),VAR_1),meet(VAR_2,VAR_0)) = meet(join(meet(join(VAR_0,VAR_1),VAR_2),VAR_1),join(VAR_2,VAR_0)),
file('theBenchmark.p',self_dual_distributivity) ).
cnf(c_11,plain,
join(meet(join(meet(A,B),C),B),meet(C,A)) = meet(join(meet(join(A,B),C),B),join(C,A)),
inference(clausify,[status(thm)],[self_dual_distributivity]) ).
cnf(c_5618,plain,
join(meet(B,join(meet(A,B),C)),meet(C,A)) = meet(join(meet(join(A,B),C),B),join(C,A)),
inference(paramod,[status(thm)],[c_3,c_11]) ).
cnf(c_5619,plain,
join(meet(C,A),meet(B,join(meet(A,B),C))) = meet(join(meet(join(A,B),C),B),join(C,A)),
inference(paramod,[status(thm)],[c_4,c_5618]) ).
cnf(c_5620,plain,
join(meet(C,A),meet(B,join(meet(A,B),C))) = meet(join(B,meet(join(A,B),C)),join(C,A)),
inference(paramod,[status(thm)],[c_4,c_5619]) ).
cnf(c_5621,plain,
join(meet(C,A),meet(B,join(meet(A,B),C))) = meet(join(C,A),join(B,meet(join(A,B),C))),
inference(paramod,[status(thm)],[c_3,c_5620]) ).
cnf(c_12,plain,
meet(join(A,B),join(C,meet(join(B,C),A))) = join(meet(A,B),meet(C,join(meet(B,C),A))),
inference(copy,[status(thm)],[c_5621]) ).
fof(prove_distributivity,axiom,
meet(a,join(b,c)) != join(meet(a,b),meet(a,c)),
file('theBenchmark.p',prove_distributivity) ).
cnf(c_13,plain,
meet(a,join(b,c)) != join(meet(a,b),meet(a,c)),
inference(clausify,[status(thm)],[prove_distributivity]) ).
cnf(c_14,plain,
join(meet(a,b),meet(a,c)) != meet(a,join(b,c)),
inference(copy,[status(thm)],[c_13]) ).
cnf(c_5622,plain,
meet(A,B) = meet(A,meet(A,B)),
inference(paramod,[status(thm)],[c_1,c_5]) ).
cnf(c_16,plain,
meet(A,meet(A,B)) = meet(A,B),
inference(copy,[status(thm)],[c_5622]) ).
cnf(c_5623,plain,
meet(meet(A,B),B) = meet(A,B),
inference(paramod,[status(thm)],[c_1,c_5]) ).
cnf(c_17,plain,
meet(A,meet(B,A)) = meet(B,A),
inference(paramod,[status(thm)],[c_3,c_5623]) ).
cnf(c_5624,plain,
meet(meet(A,B),C) = meet(B,meet(A,C)),
inference(paramod,[status(thm)],[c_3,c_5]) ).
cnf(c_19,plain,
meet(A,meet(B,C)) = meet(B,meet(A,C)),
inference(paramod,[status(thm)],[c_5,c_5624]) ).
cnf(c_5625,plain,
join(A,B) = join(A,join(A,B)),
inference(paramod,[status(thm)],[c_2,c_6]) ).
cnf(c_21,plain,
join(A,join(A,B)) = join(A,B),
inference(copy,[status(thm)],[c_5625]) ).
cnf(c_5626,plain,
join(join(A,B),B) = join(A,B),
inference(paramod,[status(thm)],[c_2,c_6]) ).
cnf(c_22,plain,
join(A,join(B,A)) = join(B,A),
inference(paramod,[status(thm)],[c_4,c_5626]) ).
cnf(c_5627,plain,
join(join(A,B),C) = join(B,join(A,C)),
inference(paramod,[status(thm)],[c_4,c_6]) ).
cnf(c_24,plain,
join(A,join(B,C)) = join(B,join(A,C)),
inference(paramod,[status(thm)],[c_6,c_5627]) ).
cnf(c_25,plain,
join(A,meet(A,join(A,B))) = meet(A,join(A,B)),
inference(paramod,[status(thm)],[c_1,c_8]) ).
cnf(c_5628,plain,
join(meet(join(A,B),A),join(A,B)) = meet(join(A,B),join(A,B)),
inference(paramod,[status(thm)],[c_1,c_8]) ).
cnf(c_5629,plain,
join(meet(A,join(A,B)),join(A,B)) = meet(join(A,B),join(A,B)),
inference(paramod,[status(thm)],[c_3,c_5628]) ).
cnf(c_5630,plain,
join(join(A,B),meet(A,join(A,B))) = meet(join(A,B),join(A,B)),
inference(paramod,[status(thm)],[c_4,c_5629]) ).
cnf(c_5631,plain,
join(A,join(B,meet(A,join(A,B)))) = meet(join(A,B),join(A,B)),
inference(paramod,[status(thm)],[c_6,c_5630]) ).
cnf(c_26,plain,
join(A,join(B,meet(A,join(A,B)))) = join(A,B),
inference(paramod,[status(thm)],[c_1,c_5631]) ).
cnf(c_27,plain,
join(meet(A,B),meet(B,join(A,C))) = meet(B,join(A,C)),
inference(paramod,[status(thm)],[c_3,c_8]) ).
cnf(c_28,plain,
join(meet(A,B),meet(join(B,C),A)) = meet(A,join(B,C)),
inference(paramod,[status(thm)],[c_3,c_8]) ).
cnf(c_29,plain,
join(meet(A,B),meet(A,join(C,B))) = meet(A,join(B,C)),
inference(paramod,[status(thm)],[c_4,c_8]) ).
cnf(c_5632,plain,
join(meet(A,join(B,C)),D) = join(meet(A,B),join(meet(A,join(B,C)),D)),
inference(paramod,[status(thm)],[c_8,c_6]) ).
cnf(c_31,plain,
join(meet(A,B),join(meet(A,join(B,C)),D)) = join(meet(A,join(B,C)),D),
inference(copy,[status(thm)],[c_5632]) ).
cnf(c_33,plain,
meet(A,join(A,meet(A,B))) = join(A,meet(A,B)),
inference(paramod,[status(thm)],[c_2,c_10]) ).
cnf(c_5633,plain,
meet(join(meet(A,B),A),meet(A,B)) = join(meet(A,B),meet(A,B)),
inference(paramod,[status(thm)],[c_2,c_10]) ).
cnf(c_5634,plain,
meet(join(A,meet(A,B)),meet(A,B)) = join(meet(A,B),meet(A,B)),
inference(paramod,[status(thm)],[c_4,c_5633]) ).
cnf(c_5635,plain,
meet(meet(A,B),join(A,meet(A,B))) = join(meet(A,B),meet(A,B)),
inference(paramod,[status(thm)],[c_3,c_5634]) ).
cnf(c_5636,plain,
meet(A,meet(B,join(A,meet(A,B)))) = join(meet(A,B),meet(A,B)),
inference(paramod,[status(thm)],[c_5,c_5635]) ).
cnf(c_34,plain,
meet(A,meet(B,join(A,meet(A,B)))) = meet(A,B),
inference(paramod,[status(thm)],[c_2,c_5636]) ).
cnf(c_35,plain,
meet(join(A,B),join(A,meet(C,B))) = join(A,meet(B,C)),
inference(paramod,[status(thm)],[c_3,c_10]) ).
cnf(c_36,plain,
meet(join(A,B),join(B,meet(A,C))) = join(B,meet(A,C)),
inference(paramod,[status(thm)],[c_4,c_10]) ).
cnf(c_5637,plain,
meet(join(A,meet(B,C)),D) = meet(join(A,B),meet(join(A,meet(B,C)),D)),
inference(paramod,[status(thm)],[c_10,c_5]) ).
cnf(c_38,plain,
meet(join(A,B),meet(join(A,meet(B,C)),D)) = meet(join(A,meet(B,C)),D),
inference(copy,[status(thm)],[c_5637]) ).
cnf(c_5638,plain,
join(join(A,meet(B,C)),meet(join(A,B),join(join(A,meet(B,C)),D))) = meet(join(A,B),join(join(A,meet(B,C)),D)),
inference(paramod,[status(thm)],[c_10,c_8]) ).
cnf(c_5639,plain,
join(join(A,meet(B,C)),meet(join(A,B),join(A,join(meet(B,C),D)))) = meet(join(A,B),join(join(A,meet(B,C)),D)),
inference(paramod,[status(thm)],[c_6,c_5638]) ).
cnf(c_5640,plain,
join(A,join(meet(B,C),meet(join(A,B),join(A,join(meet(B,C),D))))) = meet(join(A,B),join(join(A,meet(B,C)),D)),
inference(paramod,[status(thm)],[c_6,c_5639]) ).
cnf(c_41,plain,
join(A,join(meet(B,C),meet(join(A,B),join(A,join(meet(B,C),D))))) = meet(join(A,B),join(A,join(meet(B,C),D))),
inference(paramod,[status(thm)],[c_6,c_5640]) ).
cnf(c_5641,plain,
join(meet(join(A,B),A),join(A,meet(B,C))) = meet(join(A,B),join(A,meet(B,C))),
inference(paramod,[status(thm)],[c_10,c_8]) ).
cnf(c_5642,plain,
join(meet(A,join(A,B)),join(A,meet(B,C))) = meet(join(A,B),join(A,meet(B,C))),
inference(paramod,[status(thm)],[c_3,c_5641]) ).
cnf(c_5643,plain,
join(A,join(meet(A,join(A,B)),meet(B,C))) = meet(join(A,B),join(A,meet(B,C))),
inference(paramod,[status(thm)],[c_24,c_5642]) ).
cnf(c_42,plain,
join(A,join(meet(A,join(A,B)),meet(B,C))) = join(A,meet(B,C)),
inference(paramod,[status(thm)],[c_10,c_5643]) ).
cnf(c_5644,plain,
meet(join(meet(A,B),A),meet(A,join(B,C))) = join(meet(A,B),meet(A,join(B,C))),
inference(paramod,[status(thm)],[c_8,c_10]) ).
cnf(c_5645,plain,
meet(join(A,meet(A,B)),meet(A,join(B,C))) = join(meet(A,B),meet(A,join(B,C))),
inference(paramod,[status(thm)],[c_4,c_5644]) ).
cnf(c_5646,plain,
meet(A,meet(join(A,meet(A,B)),join(B,C))) = join(meet(A,B),meet(A,join(B,C))),
inference(paramod,[status(thm)],[c_19,c_5645]) ).
cnf(c_44,plain,
meet(A,meet(join(A,meet(A,B)),join(B,C))) = meet(A,join(B,C)),
inference(paramod,[status(thm)],[c_8,c_5646]) ).
cnf(c_5647,plain,
meet(join(A,A),join(B,meet(join(A,B),A))) = join(A,meet(B,join(meet(A,B),A))),
inference(paramod,[status(thm)],[c_1,c_12]) ).
cnf(c_5648,plain,
meet(A,join(B,meet(join(A,B),A))) = join(A,meet(B,join(meet(A,B),A))),
inference(paramod,[status(thm)],[c_2,c_5647]) ).
cnf(c_5649,plain,
meet(A,join(B,meet(A,join(A,B)))) = join(A,meet(B,join(meet(A,B),A))),
inference(paramod,[status(thm)],[c_3,c_5648]) ).
cnf(c_46,plain,
meet(A,join(B,meet(A,join(A,B)))) = join(A,meet(B,join(A,meet(A,B)))),
inference(paramod,[status(thm)],[c_4,c_5649]) ).
cnf(c_5650,plain,
meet(meet(A,B),meet(B,C)) = meet(A,meet(B,C)),
inference(paramod,[status(thm)],[c_16,c_5]) ).
cnf(c_5651,plain,
meet(B,meet(meet(A,B),C)) = meet(A,meet(B,C)),
inference(paramod,[status(thm)],[c_19,c_5650]) ).
cnf(c_67,plain,
meet(A,meet(B,meet(A,C))) = meet(B,meet(A,C)),
inference(paramod,[status(thm)],[c_5,c_5651]) ).
cnf(c_5652,plain,
meet(A,meet(B,meet(C,A))) = meet(meet(B,C),A),
inference(paramod,[status(thm)],[c_5,c_17]) ).
cnf(c_72,plain,
meet(A,meet(B,meet(C,A))) = meet(B,meet(C,A)),
inference(paramod,[status(thm)],[c_5,c_5652]) ).
cnf(c_96,plain,
join(A,meet(A,join(B,A))) = meet(A,join(A,B)),
inference(paramod,[status(thm)],[c_4,c_25]) ).
cnf(c_5653,plain,
join(meet(A,join(A,B)),C) = join(A,join(meet(A,join(A,B)),C)),
inference(paramod,[status(thm)],[c_25,c_6]) ).
cnf(c_98,plain,
join(A,join(meet(A,join(A,B)),C)) = join(meet(A,join(A,B)),C),
inference(copy,[status(thm)],[c_5653]) ).
cnf(c_5654,plain,
join(join(A,B),join(meet(A,B),meet(join(A,B),join(meet(B,join(A,B)),A)))) = meet(join(A,B),join(join(A,B),meet(join(B,join(A,B)),A))),
inference(paramod,[status(thm)],[c_12,c_25]) ).
cnf(c_5655,plain,
join(join(A,B),join(meet(A,B),meet(join(A,B),join(A,meet(B,join(A,B)))))) = meet(join(A,B),join(join(A,B),meet(join(B,join(A,B)),A))),
inference(paramod,[status(thm)],[c_4,c_5654]) ).
cnf(c_5656,plain,
join(join(A,B),join(meet(A,B),join(A,meet(B,join(A,B))))) = meet(join(A,B),join(join(A,B),meet(join(B,join(A,B)),A))),
inference(paramod,[status(thm)],[c_10,c_5655]) ).
cnf(c_5657,plain,
join(join(A,B),join(A,join(meet(A,B),meet(B,join(A,B))))) = meet(join(A,B),join(join(A,B),meet(join(B,join(A,B)),A))),
inference(paramod,[status(thm)],[c_24,c_5656]) ).
cnf(c_5658,plain,
join(join(A,B),join(A,meet(B,join(A,B)))) = meet(join(A,B),join(join(A,B),meet(join(B,join(A,B)),A))),
inference(paramod,[status(thm)],[c_27,c_5657]) ).
cnf(c_5659,plain,
join(A,join(join(A,B),meet(B,join(A,B)))) = meet(join(A,B),join(join(A,B),meet(join(B,join(A,B)),A))),
inference(paramod,[status(thm)],[c_24,c_5658]) ).
cnf(c_5660,plain,
join(A,join(A,join(B,meet(B,join(A,B))))) = meet(join(A,B),join(join(A,B),meet(join(B,join(A,B)),A))),
inference(paramod,[status(thm)],[c_6,c_5659]) ).
cnf(c_5661,plain,
join(A,join(A,meet(B,join(B,A)))) = meet(join(A,B),join(join(A,B),meet(join(B,join(A,B)),A))),
inference(paramod,[status(thm)],[c_96,c_5660]) ).
cnf(c_5662,plain,
join(A,meet(B,join(B,A))) = meet(join(A,B),join(join(A,B),meet(join(B,join(A,B)),A))),
inference(paramod,[status(thm)],[c_21,c_5661]) ).
cnf(c_5663,plain,
join(A,meet(B,join(B,A))) = meet(join(A,B),join(join(A,B),meet(join(A,B),A))),
inference(paramod,[status(thm)],[c_22,c_5662]) ).
cnf(c_5664,plain,
join(A,meet(B,join(B,A))) = meet(join(A,B),join(join(A,B),meet(A,join(A,B)))),
inference(paramod,[status(thm)],[c_3,c_5663]) ).
cnf(c_5665,plain,
join(A,meet(B,join(B,A))) = meet(join(A,B),join(A,join(B,meet(A,join(A,B))))),
inference(paramod,[status(thm)],[c_6,c_5664]) ).
cnf(c_5666,plain,
join(A,meet(B,join(B,A))) = meet(join(A,B),join(A,B)),
inference(paramod,[status(thm)],[c_26,c_5665]) ).
cnf(c_105,plain,
join(A,meet(B,join(B,A))) = join(A,B),
inference(paramod,[status(thm)],[c_1,c_5666]) ).
cnf(c_108,plain,
join(A,meet(A,join(B,join(A,C)))) = meet(A,join(A,join(B,C))),
inference(paramod,[status(thm)],[c_24,c_25]) ).
cnf(c_109,plain,
join(meet(A,join(A,B)),meet(B,C)) = join(A,meet(B,C)),
inference(paramod,[status(thm)],[c_98,c_42]) ).
cnf(c_5667,plain,
meet(A,join(B,A)) = join(A,meet(B,join(A,meet(A,B)))),
inference(paramod,[status(thm)],[c_105,c_46]) ).
cnf(c_110,plain,
join(A,meet(B,join(A,meet(A,B)))) = meet(A,join(B,A)),
inference(copy,[status(thm)],[c_5667]) ).
cnf(c_5668,plain,
join(meet(A,B),meet(B,A)) = meet(B,join(A,A)),
inference(paramod,[status(thm)],[c_2,c_27]) ).
cnf(c_112,plain,
join(meet(A,B),meet(B,A)) = meet(B,A),
inference(paramod,[status(thm)],[c_2,c_5668]) ).
cnf(c_113,plain,
join(meet(A,B),meet(join(A,C),B)) = meet(B,join(A,C)),
inference(paramod,[status(thm)],[c_3,c_27]) ).
cnf(c_114,plain,
join(meet(A,B),meet(B,join(C,A))) = meet(B,join(A,C)),
inference(paramod,[status(thm)],[c_4,c_27]) ).
cnf(c_131,plain,
join(meet(A,B),meet(B,join(C,join(A,D)))) = meet(B,join(A,join(C,D))),
inference(paramod,[status(thm)],[c_24,c_27]) ).
cnf(c_5669,plain,
join(meet(A,B),C) = join(meet(B,A),join(meet(A,B),C)),
inference(paramod,[status(thm)],[c_112,c_6]) ).
cnf(c_137,plain,
join(meet(A,B),join(meet(B,A),C)) = join(meet(B,A),C),
inference(copy,[status(thm)],[c_5669]) ).
cnf(c_146,plain,
join(A,meet(B,join(A,B))) = join(A,B),
inference(paramod,[status(thm)],[c_4,c_105]) ).
cnf(c_5670,plain,
join(A,join(B,C)) = join(B,join(A,meet(C,join(B,C)))),
inference(paramod,[status(thm)],[c_146,c_24]) ).
cnf(c_166,plain,
join(A,join(B,meet(C,join(A,C)))) = join(B,join(A,C)),
inference(copy,[status(thm)],[c_5670]) ).
cnf(c_5671,plain,
join(meet(A,join(B,A)),meet(B,join(B,A))) = join(meet(A,join(B,A)),B),
inference(paramod,[status(thm)],[c_146,c_105]) ).
cnf(c_5672,plain,
join(meet(A,join(B,A)),meet(B,join(B,A))) = join(B,meet(A,join(B,A))),
inference(paramod,[status(thm)],[c_4,c_5671]) ).
cnf(c_168,plain,
join(meet(A,join(B,A)),meet(B,join(B,A))) = join(B,A),
inference(paramod,[status(thm)],[c_146,c_5672]) ).
cnf(c_5673,plain,
meet(join(A,meet(A,B)),C) = meet(A,meet(join(A,meet(A,B)),C)),
inference(paramod,[status(thm)],[c_33,c_5]) ).
cnf(c_170,plain,
meet(A,meet(join(A,meet(A,B)),C)) = meet(join(A,meet(A,B)),C),
inference(copy,[status(thm)],[c_5673]) ).
cnf(c_5674,plain,
meet(A,join(B,meet(B,C))) = meet(B,meet(A,join(B,meet(B,C)))),
inference(paramod,[status(thm)],[c_33,c_19]) ).
cnf(c_179,plain,
meet(A,meet(B,join(A,meet(A,C)))) = meet(B,join(A,meet(A,C))),
inference(copy,[status(thm)],[c_5674]) ).
cnf(c_182,plain,
meet(join(A,meet(A,B)),join(B,C)) = meet(A,join(B,C)),
inference(paramod,[status(thm)],[c_170,c_44]) ).
cnf(c_184,plain,
meet(A,join(B,meet(B,A))) = meet(B,A),
inference(paramod,[status(thm)],[c_179,c_34]) ).
cnf(c_5675,plain,
join(A,meet(A,B)) = meet(A,join(B,A)),
inference(paramod,[status(thm)],[c_184,c_110]) ).
cnf(c_186,plain,
meet(A,join(B,A)) = join(A,meet(A,B)),
inference(copy,[status(thm)],[c_5675]) ).
cnf(c_5676,plain,
join(join(A,meet(A,B)),meet(B,join(B,A))) = join(B,A),
inference(paramod,[status(thm)],[c_186,c_168]) ).
cnf(c_5677,plain,
join(A,join(meet(A,B),meet(B,join(B,A)))) = join(B,A),
inference(paramod,[status(thm)],[c_6,c_5676]) ).
cnf(c_5678,plain,
join(A,meet(B,join(A,B))) = join(B,A),
inference(paramod,[status(thm)],[c_114,c_5677]) ).
cnf(c_187,plain,
join(A,join(B,meet(B,A))) = join(B,A),
inference(paramod,[status(thm)],[c_186,c_5678]) ).
cnf(c_188,plain,
join(A,join(B,join(C,meet(C,A)))) = join(B,join(A,C)),
inference(paramod,[status(thm)],[c_186,c_166]) ).
cnf(c_5679,plain,
join(A,join(A,meet(A,B))) = meet(A,join(A,B)),
inference(paramod,[status(thm)],[c_186,c_96]) ).
cnf(c_5680,plain,
join(A,meet(A,B)) = meet(A,join(A,B)),
inference(paramod,[status(thm)],[c_21,c_5679]) ).
cnf(c_193,plain,
meet(A,join(A,B)) = join(A,meet(A,B)),
inference(copy,[status(thm)],[c_5680]) ).
cnf(c_5681,plain,
join(join(A,meet(A,B)),meet(B,C)) = join(A,meet(B,C)),
inference(paramod,[status(thm)],[c_193,c_109]) ).
cnf(c_202,plain,
join(A,join(meet(A,B),meet(B,C))) = join(A,meet(B,C)),
inference(paramod,[status(thm)],[c_6,c_5681]) ).
cnf(c_203,plain,
join(A,meet(A,join(B,join(A,C)))) = join(A,meet(A,join(B,C))),
inference(paramod,[status(thm)],[c_193,c_108]) ).
cnf(c_211,plain,
meet(join(A,meet(A,B)),C) = meet(A,meet(join(B,A),C)),
inference(paramod,[status(thm)],[c_186,c_5]) ).
cnf(c_213,plain,
meet(A,join(B,join(C,A))) = join(A,meet(A,join(B,C))),
inference(paramod,[status(thm)],[c_6,c_186]) ).
cnf(c_5682,plain,
join(join(A,meet(A,B)),meet(A,join(join(B,A),C))) = meet(A,join(join(B,A),C)),
inference(paramod,[status(thm)],[c_186,c_8]) ).
cnf(c_5683,plain,
join(join(A,meet(A,B)),meet(A,join(B,join(A,C)))) = meet(A,join(join(B,A),C)),
inference(paramod,[status(thm)],[c_6,c_5682]) ).
cnf(c_5684,plain,
join(A,join(meet(A,B),meet(A,join(B,join(A,C))))) = meet(A,join(join(B,A),C)),
inference(paramod,[status(thm)],[c_6,c_5683]) ).
cnf(c_5685,plain,
join(A,meet(A,join(B,join(A,C)))) = meet(A,join(join(B,A),C)),
inference(paramod,[status(thm)],[c_8,c_5684]) ).
cnf(c_5686,plain,
join(A,meet(A,join(B,C))) = meet(A,join(join(B,A),C)),
inference(paramod,[status(thm)],[c_203,c_5685]) ).
cnf(c_5687,plain,
join(A,meet(A,join(B,C))) = meet(A,join(B,join(A,C))),
inference(paramod,[status(thm)],[c_6,c_5686]) ).
cnf(c_214,plain,
meet(A,join(B,join(A,C))) = join(A,meet(A,join(B,C))),
inference(copy,[status(thm)],[c_5687]) ).
cnf(c_5688,plain,
meet(join(A,B),join(A,B)) = join(join(A,B),meet(join(A,B),A)),
inference(paramod,[status(thm)],[c_21,c_186]) ).
cnf(c_5689,plain,
join(A,B) = join(join(A,B),meet(join(A,B),A)),
inference(paramod,[status(thm)],[c_1,c_5688]) ).
cnf(c_5690,plain,
join(A,B) = join(join(A,B),meet(A,join(A,B))),
inference(paramod,[status(thm)],[c_3,c_5689]) ).
cnf(c_5691,plain,
join(A,B) = join(join(A,B),join(A,meet(A,B))),
inference(paramod,[status(thm)],[c_193,c_5690]) ).
cnf(c_5692,plain,
join(A,B) = join(A,join(join(A,B),meet(A,B))),
inference(paramod,[status(thm)],[c_24,c_5691]) ).
cnf(c_5693,plain,
join(A,B) = join(A,join(A,join(B,meet(A,B)))),
inference(paramod,[status(thm)],[c_6,c_5692]) ).
cnf(c_5694,plain,
join(A,B) = join(A,join(B,meet(A,B))),
inference(paramod,[status(thm)],[c_21,c_5693]) ).
cnf(c_217,plain,
join(A,join(B,meet(A,B))) = join(A,B),
inference(copy,[status(thm)],[c_5694]) ).
cnf(c_218,plain,
meet(A,join(B,meet(B,C))) = meet(B,meet(A,join(C,B))),
inference(paramod,[status(thm)],[c_186,c_19]) ).
cnf(c_5695,plain,
meet(join(A,B),join(A,join(C,B))) = join(join(A,B),meet(join(A,B),C)),
inference(paramod,[status(thm)],[c_24,c_186]) ).
cnf(c_219,plain,
meet(join(A,B),join(A,join(C,B))) = join(A,join(B,meet(join(A,B),C))),
inference(paramod,[status(thm)],[c_6,c_5695]) ).
cnf(c_5696,plain,
join(join(A,meet(A,B)),meet(join(B,A),join(A,C))) = meet(join(B,A),join(A,C)),
inference(paramod,[status(thm)],[c_186,c_27]) ).
cnf(c_220,plain,
join(A,join(meet(A,B),meet(join(B,A),join(A,C)))) = meet(join(B,A),join(A,C)),
inference(paramod,[status(thm)],[c_6,c_5696]) ).
cnf(c_222,plain,
meet(A,meet(join(B,A),join(B,C))) = meet(A,join(B,C)),
inference(paramod,[status(thm)],[c_211,c_182]) ).
cnf(c_5697,plain,
meet(join(A,B),join(A,join(B,C))) = join(join(A,B),meet(join(A,B),C)),
inference(paramod,[status(thm)],[c_6,c_193]) ).
cnf(c_234,plain,
meet(join(A,B),join(A,join(B,C))) = join(A,join(B,meet(join(A,B),C))),
inference(paramod,[status(thm)],[c_6,c_5697]) ).
cnf(c_238,plain,
meet(A,join(B,meet(B,C))) = meet(B,meet(A,join(B,C))),
inference(paramod,[status(thm)],[c_193,c_19]) ).
cnf(c_243,plain,
join(meet(A,B),meet(join(C,B),A)) = meet(A,join(B,C)),
inference(paramod,[status(thm)],[c_4,c_28]) ).
cnf(c_5698,plain,
meet(join(A,B),meet(A,join(B,meet(A,B)))) = join(meet(A,B),meet(meet(A,B),join(meet(B,meet(A,B)),A))),
inference(paramod,[status(thm)],[c_28,c_12]) ).
cnf(c_5699,plain,
meet(A,meet(join(A,B),join(B,meet(A,B)))) = join(meet(A,B),meet(meet(A,B),join(meet(B,meet(A,B)),A))),
inference(paramod,[status(thm)],[c_19,c_5698]) ).
cnf(c_5700,plain,
meet(A,join(B,meet(A,B))) = join(meet(A,B),meet(meet(A,B),join(meet(B,meet(A,B)),A))),
inference(paramod,[status(thm)],[c_36,c_5699]) ).
cnf(c_5701,plain,
meet(A,join(B,meet(A,B))) = join(meet(A,B),meet(meet(A,B),join(meet(A,B),A))),
inference(paramod,[status(thm)],[c_17,c_5700]) ).
cnf(c_5702,plain,
meet(A,join(B,meet(A,B))) = join(meet(A,B),meet(meet(A,B),join(A,meet(A,B)))),
inference(paramod,[status(thm)],[c_4,c_5701]) ).
cnf(c_5703,plain,
meet(A,join(B,meet(A,B))) = join(meet(A,B),join(meet(A,B),meet(meet(A,B),A))),
inference(paramod,[status(thm)],[c_186,c_5702]) ).
cnf(c_5704,plain,
meet(A,join(B,meet(A,B))) = join(meet(A,B),join(meet(A,B),meet(A,meet(A,B)))),
inference(paramod,[status(thm)],[c_3,c_5703]) ).
cnf(c_5705,plain,
meet(A,join(B,meet(A,B))) = join(meet(A,B),join(meet(A,B),meet(A,B))),
inference(paramod,[status(thm)],[c_16,c_5704]) ).
cnf(c_5706,plain,
meet(A,join(B,meet(A,B))) = join(meet(A,B),meet(A,B)),
inference(paramod,[status(thm)],[c_2,c_5705]) ).
cnf(c_252,plain,
meet(A,join(B,meet(A,B))) = meet(A,B),
inference(paramod,[status(thm)],[c_2,c_5706]) ).
cnf(c_5707,plain,
meet(join(A,join(B,meet(B,A))),join(C,meet(join(join(B,meet(B,A)),C),A))) = join(meet(B,A),meet(C,join(meet(join(B,meet(B,A)),C),A))),
inference(paramod,[status(thm)],[c_184,c_12]) ).
cnf(c_5708,plain,
meet(join(B,A),join(C,meet(join(join(B,meet(B,A)),C),A))) = join(meet(B,A),meet(C,join(meet(join(B,meet(B,A)),C),A))),
inference(paramod,[status(thm)],[c_187,c_5707]) ).
cnf(c_5709,plain,
meet(join(B,A),join(C,meet(join(B,join(meet(B,A),C)),A))) = join(meet(B,A),meet(C,join(meet(join(B,meet(B,A)),C),A))),
inference(paramod,[status(thm)],[c_6,c_5708]) ).
cnf(c_5710,plain,
meet(join(B,A),join(C,meet(A,join(B,join(meet(B,A),C))))) = join(meet(B,A),meet(C,join(meet(join(B,meet(B,A)),C),A))),
inference(paramod,[status(thm)],[c_3,c_5709]) ).
cnf(c_5711,plain,
meet(join(B,A),join(C,meet(A,join(B,join(meet(B,A),C))))) = join(meet(B,A),meet(C,join(meet(B,meet(join(A,B),C)),A))),
inference(paramod,[status(thm)],[c_211,c_5710]) ).
cnf(c_270,plain,
meet(join(A,B),join(C,meet(B,join(A,join(meet(A,B),C))))) = join(meet(A,B),meet(C,join(B,meet(A,meet(join(B,A),C))))),
inference(paramod,[status(thm)],[c_4,c_5711]) ).
cnf(c_5712,plain,
meet(A,meet(B,C)) = meet(C,meet(A,join(B,meet(B,C)))),
inference(paramod,[status(thm)],[c_184,c_19]) ).
cnf(c_273,plain,
meet(A,meet(B,join(C,meet(C,A)))) = meet(B,meet(C,A)),
inference(copy,[status(thm)],[c_5712]) ).
cnf(c_315,plain,
join(meet(A,B),meet(B,join(C,meet(A,B)))) = meet(B,join(meet(A,B),C)),
inference(paramod,[status(thm)],[c_17,c_29]) ).
cnf(c_5713,plain,
join(meet(A,join(B,C)),meet(A,join(C,B))) = join(meet(A,C),meet(A,join(B,C))),
inference(paramod,[status(thm)],[c_29,c_22]) ).
cnf(c_316,plain,
join(meet(A,join(B,C)),meet(A,join(C,B))) = meet(A,join(C,B)),
inference(paramod,[status(thm)],[c_29,c_5713]) ).
cnf(c_5714,plain,
meet(meet(A,join(B,C)),meet(A,join(C,B))) = join(meet(A,join(B,C)),meet(meet(A,join(B,C)),meet(A,C))),
inference(paramod,[status(thm)],[c_29,c_186]) ).
cnf(c_5715,plain,
meet(A,meet(meet(A,join(B,C)),join(C,B))) = join(meet(A,join(B,C)),meet(meet(A,join(B,C)),meet(A,C))),
inference(paramod,[status(thm)],[c_19,c_5714]) ).
cnf(c_5716,plain,
meet(A,meet(join(C,B),meet(A,join(B,C)))) = join(meet(A,join(B,C)),meet(meet(A,join(B,C)),meet(A,C))),
inference(paramod,[status(thm)],[c_3,c_5715]) ).
cnf(c_5717,plain,
meet(join(C,B),meet(A,join(B,C))) = join(meet(A,join(B,C)),meet(meet(A,join(B,C)),meet(A,C))),
inference(paramod,[status(thm)],[c_67,c_5716]) ).
cnf(c_5718,plain,
meet(join(C,B),meet(A,join(B,C))) = join(meet(A,join(B,C)),meet(meet(A,C),meet(A,join(B,C)))),
inference(paramod,[status(thm)],[c_3,c_5717]) ).
cnf(c_5719,plain,
meet(join(C,B),meet(A,join(B,C))) = join(meet(A,join(B,C)),meet(A,meet(meet(A,C),join(B,C)))),
inference(paramod,[status(thm)],[c_19,c_5718]) ).
cnf(c_5720,plain,
meet(join(C,B),meet(A,join(B,C))) = join(meet(A,join(B,C)),meet(A,meet(A,meet(C,join(B,C))))),
inference(paramod,[status(thm)],[c_5,c_5719]) ).
cnf(c_5721,plain,
meet(join(C,B),meet(A,join(B,C))) = join(meet(A,join(B,C)),meet(A,meet(A,join(C,meet(C,B))))),
inference(paramod,[status(thm)],[c_186,c_5720]) ).
cnf(c_5722,plain,
meet(join(C,B),meet(A,join(B,C))) = join(meet(A,join(B,C)),meet(A,join(C,meet(C,B)))),
inference(paramod,[status(thm)],[c_16,c_5721]) ).
cnf(c_320,plain,
join(meet(A,join(B,C)),meet(A,join(C,meet(C,B)))) = meet(join(C,B),meet(A,join(B,C))),
inference(copy,[status(thm)],[c_5722]) ).
cnf(c_5723,plain,
join(meet(A,join(B,C)),join(meet(A,C),meet(meet(A,C),meet(A,join(B,C))))) = meet(A,join(C,B)),
inference(paramod,[status(thm)],[c_29,c_187]) ).
cnf(c_5724,plain,
join(meet(A,join(B,C)),join(meet(A,C),meet(A,meet(meet(A,C),join(B,C))))) = meet(A,join(C,B)),
inference(paramod,[status(thm)],[c_19,c_5723]) ).
cnf(c_5725,plain,
join(meet(A,join(B,C)),join(meet(A,C),meet(A,meet(A,meet(C,join(B,C)))))) = meet(A,join(C,B)),
inference(paramod,[status(thm)],[c_5,c_5724]) ).
cnf(c_5726,plain,
join(meet(A,join(B,C)),join(meet(A,C),meet(A,meet(A,join(C,meet(C,B)))))) = meet(A,join(C,B)),
inference(paramod,[status(thm)],[c_186,c_5725]) ).
cnf(c_5727,plain,
join(meet(A,join(B,C)),join(meet(A,C),meet(A,join(C,meet(C,B))))) = meet(A,join(C,B)),
inference(paramod,[status(thm)],[c_16,c_5726]) ).
cnf(c_5728,plain,
join(meet(A,join(B,C)),meet(A,join(C,meet(C,B)))) = meet(A,join(C,B)),
inference(paramod,[status(thm)],[c_8,c_5727]) ).
cnf(c_321,plain,
meet(join(A,B),meet(C,join(B,A))) = meet(C,join(A,B)),
inference(paramod,[status(thm)],[c_320,c_5728]) ).
cnf(c_361,plain,
meet(join(A,B),join(meet(C,B),A)) = join(A,meet(B,C)),
inference(paramod,[status(thm)],[c_4,c_35]) ).
cnf(c_5729,plain,
meet(join(meet(A,B),join(A,C)),meet(B,join(A,C))) = join(meet(A,B),meet(join(A,C),B)),
inference(paramod,[status(thm)],[c_27,c_35]) ).
cnf(c_5730,plain,
meet(join(A,join(meet(A,B),C)),meet(B,join(A,C))) = join(meet(A,B),meet(join(A,C),B)),
inference(paramod,[status(thm)],[c_24,c_5729]) ).
cnf(c_5731,plain,
meet(meet(B,join(A,C)),join(A,join(meet(A,B),C))) = join(meet(A,B),meet(join(A,C),B)),
inference(paramod,[status(thm)],[c_3,c_5730]) ).
cnf(c_5732,plain,
meet(B,meet(join(A,C),join(A,join(meet(A,B),C)))) = join(meet(A,B),meet(join(A,C),B)),
inference(paramod,[status(thm)],[c_5,c_5731]) ).
cnf(c_5733,plain,
meet(B,join(A,join(C,meet(join(A,C),meet(A,B))))) = join(meet(A,B),meet(join(A,C),B)),
inference(paramod,[status(thm)],[c_219,c_5732]) ).
cnf(c_5734,plain,
meet(B,join(A,join(C,meet(A,meet(join(A,C),B))))) = join(meet(A,B),meet(join(A,C),B)),
inference(paramod,[status(thm)],[c_19,c_5733]) ).
cnf(c_379,plain,
meet(A,join(B,join(C,meet(B,meet(join(B,C),A))))) = meet(A,join(B,C)),
inference(paramod,[status(thm)],[c_113,c_5734]) ).
cnf(c_5735,plain,
meet(join(A,join(B,meet(C,B))),join(A,meet(C,B))) = join(A,meet(join(B,meet(C,B)),C)),
inference(paramod,[status(thm)],[c_252,c_35]) ).
cnf(c_5736,plain,
meet(join(A,meet(C,B)),join(A,join(B,meet(C,B)))) = join(A,meet(join(B,meet(C,B)),C)),
inference(paramod,[status(thm)],[c_3,c_5735]) ).
cnf(c_5737,plain,
join(A,join(meet(C,B),meet(join(A,meet(C,B)),B))) = join(A,meet(join(B,meet(C,B)),C)),
inference(paramod,[status(thm)],[c_219,c_5736]) ).
cnf(c_5738,plain,
join(A,join(meet(C,B),meet(B,join(A,meet(C,B))))) = join(A,meet(join(B,meet(C,B)),C)),
inference(paramod,[status(thm)],[c_3,c_5737]) ).
cnf(c_5739,plain,
join(A,meet(B,join(meet(C,B),A))) = join(A,meet(join(B,meet(C,B)),C)),
inference(paramod,[status(thm)],[c_315,c_5738]) ).
cnf(c_5740,plain,
join(A,meet(B,join(meet(C,B),A))) = join(A,meet(C,join(B,meet(C,B)))),
inference(paramod,[status(thm)],[c_3,c_5739]) ).
cnf(c_386,plain,
join(A,meet(B,join(meet(C,B),A))) = join(A,meet(C,B)),
inference(paramod,[status(thm)],[c_252,c_5740]) ).
cnf(c_5741,plain,
meet(join(A,B),join(B,meet(C,join(A,meet(A,B))))) = join(B,meet(join(A,meet(A,B)),C)),
inference(paramod,[status(thm)],[c_187,c_35]) ).
cnf(c_387,plain,
meet(join(A,B),join(B,meet(C,join(A,meet(A,B))))) = join(B,meet(A,meet(join(B,A),C))),
inference(paramod,[status(thm)],[c_211,c_5741]) ).
cnf(c_398,plain,
meet(join(A,B),join(meet(A,C),B)) = join(B,meet(A,C)),
inference(paramod,[status(thm)],[c_4,c_36]) ).
cnf(c_5742,plain,
meet(join(A,B),join(join(A,B),meet(A,C))) = join(join(A,B),meet(A,C)),
inference(paramod,[status(thm)],[c_21,c_36]) ).
cnf(c_5743,plain,
meet(join(A,B),join(A,join(B,meet(A,C)))) = join(join(A,B),meet(A,C)),
inference(paramod,[status(thm)],[c_6,c_5742]) ).
cnf(c_5744,plain,
join(A,join(B,meet(join(A,B),meet(A,C)))) = join(join(A,B),meet(A,C)),
inference(paramod,[status(thm)],[c_234,c_5743]) ).
cnf(c_5745,plain,
join(A,join(B,meet(A,meet(join(A,B),C)))) = join(join(A,B),meet(A,C)),
inference(paramod,[status(thm)],[c_19,c_5744]) ).
cnf(c_411,plain,
join(A,join(B,meet(A,meet(join(A,B),C)))) = join(A,join(B,meet(A,C))),
inference(paramod,[status(thm)],[c_6,c_5745]) ).
cnf(c_424,plain,
meet(A,join(B,join(C,meet(B,A)))) = meet(A,join(B,C)),
inference(paramod,[status(thm)],[c_411,c_379]) ).
cnf(c_5746,plain,
join(meet(A,B),meet(join(B,C),join(A,meet(A,B)))) = meet(join(A,meet(A,B)),join(B,C)),
inference(paramod,[status(thm)],[c_184,c_113]) ).
cnf(c_5747,plain,
join(meet(A,B),meet(join(B,C),join(A,meet(A,B)))) = meet(A,meet(join(B,A),join(B,C))),
inference(paramod,[status(thm)],[c_211,c_5746]) ).
cnf(c_468,plain,
join(meet(A,B),meet(join(B,C),join(A,meet(A,B)))) = meet(A,join(B,C)),
inference(paramod,[status(thm)],[c_222,c_5747]) ).
cnf(c_469,plain,
join(meet(A,B),meet(join(A,C),join(B,meet(A,B)))) = meet(join(B,meet(A,B)),join(A,C)),
inference(paramod,[status(thm)],[c_252,c_113]) ).
cnf(c_5748,plain,
meet(join(meet(A,join(B,C)),C),join(A,meet(join(C,A),meet(A,join(B,C))))) = join(meet(meet(A,join(B,C)),C),meet(A,meet(A,join(C,B)))),
inference(paramod,[status(thm)],[c_114,c_12]) ).
cnf(c_5749,plain,
meet(join(C,meet(A,join(B,C))),join(A,meet(join(C,A),meet(A,join(B,C))))) = join(meet(meet(A,join(B,C)),C),meet(A,meet(A,join(C,B)))),
inference(paramod,[status(thm)],[c_4,c_5748]) ).
cnf(c_5750,plain,
meet(join(C,meet(A,join(B,C))),join(A,meet(A,meet(join(C,A),join(B,C))))) = join(meet(meet(A,join(B,C)),C),meet(A,meet(A,join(C,B)))),
inference(paramod,[status(thm)],[c_19,c_5749]) ).
cnf(c_5751,plain,
meet(join(C,meet(A,join(B,C))),join(A,meet(A,meet(join(C,A),join(B,C))))) = join(meet(C,meet(A,join(B,C))),meet(A,meet(A,join(C,B)))),
inference(paramod,[status(thm)],[c_3,c_5750]) ).
cnf(c_5752,plain,
meet(join(C,meet(A,join(B,C))),join(A,meet(A,meet(join(C,A),join(B,C))))) = join(meet(C,meet(A,join(B,C))),meet(A,join(C,B))),
inference(paramod,[status(thm)],[c_16,c_5751]) ).
cnf(c_488,plain,
meet(join(A,meet(B,join(C,A))),join(B,meet(B,meet(join(A,B),join(C,A))))) = join(meet(B,join(A,C)),meet(A,meet(B,join(C,A)))),
inference(paramod,[status(thm)],[c_4,c_5752]) ).
cnf(c_5753,plain,
join(join(A,meet(A,B)),meet(join(B,A),join(C,A))) = meet(join(B,A),join(A,C)),
inference(paramod,[status(thm)],[c_186,c_114]) ).
cnf(c_495,plain,
join(A,join(meet(A,B),meet(join(B,A),join(C,A)))) = meet(join(B,A),join(A,C)),
inference(paramod,[status(thm)],[c_6,c_5753]) ).
cnf(c_5754,plain,
join(meet(meet(A,B),join(C,B)),join(C,meet(B,A))) = meet(join(C,B),join(meet(A,B),C)),
inference(paramod,[status(thm)],[c_35,c_114]) ).
cnf(c_5755,plain,
join(meet(A,meet(B,join(C,B))),join(C,meet(B,A))) = meet(join(C,B),join(meet(A,B),C)),
inference(paramod,[status(thm)],[c_5,c_5754]) ).
cnf(c_5756,plain,
join(meet(A,join(B,meet(B,C))),join(C,meet(B,A))) = meet(join(C,B),join(meet(A,B),C)),
inference(paramod,[status(thm)],[c_186,c_5755]) ).
cnf(c_5757,plain,
join(join(C,meet(B,A)),meet(A,join(B,meet(B,C)))) = meet(join(C,B),join(meet(A,B),C)),
inference(paramod,[status(thm)],[c_4,c_5756]) ).
cnf(c_5758,plain,
join(C,join(meet(B,A),meet(A,join(B,meet(B,C))))) = meet(join(C,B),join(meet(A,B),C)),
inference(paramod,[status(thm)],[c_6,c_5757]) ).
cnf(c_5759,plain,
join(C,meet(A,join(B,meet(B,C)))) = meet(join(C,B),join(meet(A,B),C)),
inference(paramod,[status(thm)],[c_27,c_5758]) ).
cnf(c_508,plain,
join(A,meet(B,join(C,meet(C,A)))) = join(A,meet(C,B)),
inference(paramod,[status(thm)],[c_361,c_5759]) ).
cnf(c_5760,plain,
meet(join(A,B),join(B,meet(A,C))) = join(B,meet(A,meet(join(B,A),C))),
inference(paramod,[status(thm)],[c_508,c_387]) ).
cnf(c_5761,plain,
join(B,meet(A,C)) = join(B,meet(A,meet(join(B,A),C))),
inference(paramod,[status(thm)],[c_36,c_5760]) ).
cnf(c_514,plain,
join(A,meet(B,meet(join(A,B),C))) = join(A,meet(B,C)),
inference(copy,[status(thm)],[c_5761]) ).
cnf(c_515,plain,
meet(join(A,B),join(C,meet(B,join(A,join(meet(A,B),C))))) = join(meet(A,B),meet(C,join(B,meet(A,C)))),
inference(paramod,[status(thm)],[c_514,c_270]) ).
cnf(c_5762,plain,
join(meet(A,B),meet(join(B,C),join(A,D))) = join(meet(A,join(B,C)),meet(join(B,C),join(A,D))),
inference(paramod,[status(thm)],[c_27,c_31]) ).
cnf(c_551,plain,
join(meet(A,B),meet(join(B,C),join(A,D))) = meet(join(B,C),join(A,D)),
inference(paramod,[status(thm)],[c_27,c_5762]) ).
cnf(c_568,plain,
meet(join(A,B),join(C,meet(C,A))) = meet(C,join(A,B)),
inference(paramod,[status(thm)],[c_551,c_468]) ).
cnf(c_569,plain,
join(A,meet(join(B,A),join(A,C))) = meet(join(B,A),join(A,C)),
inference(paramod,[status(thm)],[c_551,c_220]) ).
cnf(c_5763,plain,
meet(meet(A,B),meet(A,join(B,C))) = join(meet(A,B),meet(meet(A,B),meet(join(C,B),A))),
inference(paramod,[status(thm)],[c_243,c_193]) ).
cnf(c_5764,plain,
meet(A,meet(meet(A,B),join(B,C))) = join(meet(A,B),meet(meet(A,B),meet(join(C,B),A))),
inference(paramod,[status(thm)],[c_19,c_5763]) ).
cnf(c_5765,plain,
meet(A,meet(A,meet(B,join(B,C)))) = join(meet(A,B),meet(meet(A,B),meet(join(C,B),A))),
inference(paramod,[status(thm)],[c_5,c_5764]) ).
cnf(c_5766,plain,
meet(A,meet(A,join(B,meet(B,C)))) = join(meet(A,B),meet(meet(A,B),meet(join(C,B),A))),
inference(paramod,[status(thm)],[c_193,c_5765]) ).
cnf(c_5767,plain,
meet(A,join(B,meet(B,C))) = join(meet(A,B),meet(meet(A,B),meet(join(C,B),A))),
inference(paramod,[status(thm)],[c_16,c_5766]) ).
cnf(c_5768,plain,
meet(A,join(B,meet(B,C))) = join(meet(A,B),meet(A,meet(B,meet(join(C,B),A)))),
inference(paramod,[status(thm)],[c_5,c_5767]) ).
cnf(c_5769,plain,
meet(A,join(B,meet(B,C))) = join(meet(A,B),meet(B,meet(join(C,B),A))),
inference(paramod,[status(thm)],[c_72,c_5768]) ).
cnf(c_585,plain,
join(meet(A,B),meet(B,meet(join(C,B),A))) = meet(A,join(B,meet(B,C))),
inference(copy,[status(thm)],[c_5769]) ).
cnf(c_5770,plain,
join(meet(A,B),meet(join(C,join(A,meet(A,B))),B)) = meet(B,join(join(A,meet(A,B)),C)),
inference(paramod,[status(thm)],[c_184,c_243]) ).
cnf(c_5771,plain,
join(meet(A,B),meet(B,join(C,join(A,meet(A,B))))) = meet(B,join(join(A,meet(A,B)),C)),
inference(paramod,[status(thm)],[c_3,c_5770]) ).
cnf(c_5772,plain,
meet(B,join(A,join(C,meet(A,B)))) = meet(B,join(join(A,meet(A,B)),C)),
inference(paramod,[status(thm)],[c_131,c_5771]) ).
cnf(c_5773,plain,
meet(B,join(A,C)) = meet(B,join(join(A,meet(A,B)),C)),
inference(paramod,[status(thm)],[c_424,c_5772]) ).
cnf(c_5774,plain,
meet(B,join(A,C)) = meet(B,join(A,join(meet(A,B),C))),
inference(paramod,[status(thm)],[c_6,c_5773]) ).
cnf(c_587,plain,
meet(A,join(B,join(meet(B,A),C))) = meet(A,join(B,C)),
inference(copy,[status(thm)],[c_5774]) ).
cnf(c_603,plain,
meet(join(A,B),join(C,meet(B,join(A,C)))) = join(meet(A,B),meet(C,join(B,meet(A,C)))),
inference(paramod,[status(thm)],[c_587,c_515]) ).
cnf(c_750,plain,
meet(join(A,B),join(C,meet(A,C))) = meet(C,join(A,B)),
inference(paramod,[status(thm)],[c_3,c_568]) ).
cnf(c_751,plain,
meet(join(A,B),join(C,meet(C,B))) = meet(C,join(B,A)),
inference(paramod,[status(thm)],[c_4,c_568]) ).
cnf(c_5775,plain,
meet(join(A,B),join(meet(C,D),meet(C,meet(D,A)))) = meet(meet(C,D),join(A,B)),
inference(paramod,[status(thm)],[c_5,c_568]) ).
cnf(c_753,plain,
meet(join(A,B),join(meet(C,D),meet(C,meet(D,A)))) = meet(C,meet(D,join(A,B))),
inference(paramod,[status(thm)],[c_5,c_5775]) ).
cnf(c_5776,plain,
meet(join(A,B),join(join(A,B),join(C,meet(C,A)))) = join(join(A,B),meet(C,join(A,B))),
inference(paramod,[status(thm)],[c_568,c_193]) ).
cnf(c_5777,plain,
meet(join(A,B),join(A,join(B,join(C,meet(C,A))))) = join(join(A,B),meet(C,join(A,B))),
inference(paramod,[status(thm)],[c_6,c_5776]) ).
cnf(c_5778,plain,
meet(join(A,B),join(B,join(A,C))) = join(join(A,B),meet(C,join(A,B))),
inference(paramod,[status(thm)],[c_188,c_5777]) ).
cnf(c_769,plain,
meet(join(A,B),join(B,join(A,C))) = join(A,join(B,meet(C,join(A,B)))),
inference(paramod,[status(thm)],[c_6,c_5778]) ).
cnf(c_5779,plain,
join(meet(A,B),meet(B,join(A,C))) = meet(join(B,meet(A,B)),join(A,C)),
inference(paramod,[status(thm)],[c_750,c_469]) ).
cnf(c_5780,plain,
meet(B,join(A,C)) = meet(join(B,meet(A,B)),join(A,C)),
inference(paramod,[status(thm)],[c_27,c_5779]) ).
cnf(c_789,plain,
meet(join(A,meet(B,A)),join(B,C)) = meet(A,join(B,C)),
inference(copy,[status(thm)],[c_5780]) ).
cnf(c_876,plain,
meet(join(A,B),join(C,meet(B,C))) = meet(C,join(B,A)),
inference(paramod,[status(thm)],[c_4,c_750]) ).
cnf(c_5781,plain,
meet(join(A,B),join(meet(C,A),meet(C,A))) = meet(meet(C,A),join(A,B)),
inference(paramod,[status(thm)],[c_17,c_750]) ).
cnf(c_5782,plain,
meet(join(A,B),meet(C,A)) = meet(meet(C,A),join(A,B)),
inference(paramod,[status(thm)],[c_2,c_5781]) ).
cnf(c_5783,plain,
meet(join(A,B),meet(C,A)) = meet(C,meet(A,join(A,B))),
inference(paramod,[status(thm)],[c_5,c_5782]) ).
cnf(c_886,plain,
meet(join(A,B),meet(C,A)) = meet(C,join(A,meet(A,B))),
inference(paramod,[status(thm)],[c_193,c_5783]) ).
cnf(c_5784,plain,
meet(A,join(B,C)) = meet(join(A,meet(A,B)),join(C,B)),
inference(paramod,[status(thm)],[c_751,c_3]) ).
cnf(c_5785,plain,
meet(A,join(B,C)) = meet(A,meet(join(B,A),join(C,B))),
inference(paramod,[status(thm)],[c_211,c_5784]) ).
cnf(c_905,plain,
meet(A,meet(join(B,A),join(C,B))) = meet(A,join(B,C)),
inference(copy,[status(thm)],[c_5785]) ).
cnf(c_958,plain,
meet(join(A,meet(B,join(C,A))),join(B,meet(B,join(A,C)))) = join(meet(B,join(A,C)),meet(A,meet(B,join(C,A)))),
inference(paramod,[status(thm)],[c_905,c_488]) ).
cnf(c_5786,plain,
meet(join(A,B),join(meet(C,B),meet(C,B))) = meet(meet(C,B),join(B,A)),
inference(paramod,[status(thm)],[c_17,c_876]) ).
cnf(c_5787,plain,
meet(join(A,B),meet(C,B)) = meet(meet(C,B),join(B,A)),
inference(paramod,[status(thm)],[c_2,c_5786]) ).
cnf(c_5788,plain,
meet(join(A,B),meet(C,B)) = meet(C,meet(B,join(B,A))),
inference(paramod,[status(thm)],[c_5,c_5787]) ).
cnf(c_990,plain,
meet(join(A,B),meet(C,B)) = meet(C,join(B,meet(B,A))),
inference(paramod,[status(thm)],[c_193,c_5788]) ).
cnf(c_5789,plain,
join(meet(meet(A,B),join(C,A)),meet(B,join(A,C))) = meet(join(C,A),join(meet(A,B),B)),
inference(paramod,[status(thm)],[c_876,c_114]) ).
cnf(c_5790,plain,
join(meet(A,meet(B,join(C,A))),meet(B,join(A,C))) = meet(join(C,A),join(meet(A,B),B)),
inference(paramod,[status(thm)],[c_5,c_5789]) ).
cnf(c_5791,plain,
join(meet(B,join(A,C)),meet(A,meet(B,join(C,A)))) = meet(join(C,A),join(meet(A,B),B)),
inference(paramod,[status(thm)],[c_4,c_5790]) ).
cnf(c_5792,plain,
join(meet(B,join(A,C)),meet(A,meet(B,join(C,A)))) = meet(join(C,A),join(B,meet(A,B))),
inference(paramod,[status(thm)],[c_4,c_5791]) ).
cnf(c_1004,plain,
join(meet(A,join(B,C)),meet(B,meet(A,join(C,B)))) = meet(A,join(B,C)),
inference(paramod,[status(thm)],[c_876,c_5792]) ).
cnf(c_1012,plain,
meet(join(A,meet(B,join(C,A))),join(B,meet(B,join(A,C)))) = meet(B,join(A,C)),
inference(paramod,[status(thm)],[c_1004,c_958]) ).
cnf(c_5793,plain,
meet(join(A,B),meet(A,join(B,C))) = meet(join(A,meet(B,A)),join(B,C)),
inference(paramod,[status(thm)],[c_789,c_38]) ).
cnf(c_5794,plain,
meet(A,meet(join(A,B),join(B,C))) = meet(join(A,meet(B,A)),join(B,C)),
inference(paramod,[status(thm)],[c_19,c_5793]) ).
cnf(c_1087,plain,
meet(A,meet(join(A,B),join(B,C))) = meet(A,join(B,C)),
inference(paramod,[status(thm)],[c_789,c_5794]) ).
cnf(c_1135,plain,
join(A,join(meet(A,B),meet(C,B))) = join(A,meet(B,C)),
inference(paramod,[status(thm)],[c_3,c_202]) ).
cnf(c_1136,plain,
join(A,join(meet(B,C),meet(A,B))) = join(A,meet(B,C)),
inference(paramod,[status(thm)],[c_4,c_202]) ).
cnf(c_5795,plain,
join(A,join(join(A,meet(A,B)),meet(join(B,A),C))) = join(A,meet(join(B,A),C)),
inference(paramod,[status(thm)],[c_186,c_202]) ).
cnf(c_5796,plain,
join(A,join(A,join(meet(A,B),meet(join(B,A),C)))) = join(A,meet(join(B,A),C)),
inference(paramod,[status(thm)],[c_6,c_5795]) ).
cnf(c_1151,plain,
join(A,join(meet(A,B),meet(join(B,A),C))) = join(A,meet(join(B,A),C)),
inference(paramod,[status(thm)],[c_21,c_5796]) ).
cnf(c_1190,plain,
join(A,meet(join(B,A),join(C,A))) = meet(join(B,A),join(A,C)),
inference(paramod,[status(thm)],[c_1151,c_495]) ).
cnf(c_1197,plain,
meet(join(A,meet(B,A)),C) = meet(A,meet(join(B,A),C)),
inference(paramod,[status(thm)],[c_3,c_211]) ).
cnf(c_5797,plain,
meet(A,meet(join(B,A),join(join(A,meet(A,B)),C))) = join(join(A,meet(A,B)),meet(join(A,meet(A,B)),C)),
inference(paramod,[status(thm)],[c_211,c_193]) ).
cnf(c_5798,plain,
meet(A,meet(join(B,A),join(A,join(meet(A,B),C)))) = join(join(A,meet(A,B)),meet(join(A,meet(A,B)),C)),
inference(paramod,[status(thm)],[c_6,c_5797]) ).
cnf(c_5799,plain,
meet(A,meet(join(B,A),join(A,join(meet(A,B),C)))) = join(join(A,meet(A,B)),meet(A,meet(join(B,A),C))),
inference(paramod,[status(thm)],[c_211,c_5798]) ).
cnf(c_1210,plain,
meet(A,meet(join(B,A),join(A,join(meet(A,B),C)))) = join(A,join(meet(A,B),meet(A,meet(join(B,A),C)))),
inference(paramod,[status(thm)],[c_6,c_5799]) ).
cnf(c_5800,plain,
meet(meet(A,join(B,C)),join(D,meet(A,join(B,C)))) = join(meet(A,join(B,C)),meet(meet(A,join(B,C)),join(D,meet(A,B)))),
inference(paramod,[status(thm)],[c_8,c_213]) ).
cnf(c_5801,plain,
join(meet(A,join(B,C)),meet(meet(A,join(B,C)),D)) = join(meet(A,join(B,C)),meet(meet(A,join(B,C)),join(D,meet(A,B)))),
inference(paramod,[status(thm)],[c_186,c_5800]) ).
cnf(c_5802,plain,
join(meet(A,join(B,C)),meet(A,meet(join(B,C),D))) = join(meet(A,join(B,C)),meet(meet(A,join(B,C)),join(D,meet(A,B)))),
inference(paramod,[status(thm)],[c_5,c_5801]) ).
cnf(c_5803,plain,
join(meet(A,join(B,C)),meet(A,meet(join(B,C),D))) = join(meet(A,join(B,C)),meet(A,meet(join(B,C),join(D,meet(A,B))))),
inference(paramod,[status(thm)],[c_5,c_5802]) ).
cnf(c_1292,plain,
join(meet(A,join(B,C)),meet(A,meet(join(B,C),join(D,meet(A,B))))) = join(meet(A,join(B,C)),meet(A,meet(join(B,C),D))),
inference(copy,[status(thm)],[c_5803]) ).
cnf(c_5804,plain,
meet(join(A,meet(B,A)),join(C,join(B,A))) = join(join(A,meet(B,A)),meet(join(A,meet(B,A)),join(C,B))),
inference(paramod,[status(thm)],[c_217,c_213]) ).
cnf(c_5805,plain,
meet(A,meet(join(B,A),join(C,join(B,A)))) = join(join(A,meet(B,A)),meet(join(A,meet(B,A)),join(C,B))),
inference(paramod,[status(thm)],[c_1197,c_5804]) ).
cnf(c_5806,plain,
meet(A,join(join(B,A),meet(join(B,A),C))) = join(join(A,meet(B,A)),meet(join(A,meet(B,A)),join(C,B))),
inference(paramod,[status(thm)],[c_186,c_5805]) ).
cnf(c_5807,plain,
meet(A,join(B,join(A,meet(join(B,A),C)))) = join(join(A,meet(B,A)),meet(join(A,meet(B,A)),join(C,B))),
inference(paramod,[status(thm)],[c_6,c_5806]) ).
cnf(c_5808,plain,
join(A,meet(A,join(B,meet(join(B,A),C)))) = join(join(A,meet(B,A)),meet(join(A,meet(B,A)),join(C,B))),
inference(paramod,[status(thm)],[c_214,c_5807]) ).
cnf(c_5809,plain,
join(A,meet(A,join(B,meet(join(B,A),C)))) = join(join(A,meet(B,A)),meet(A,meet(join(B,A),join(C,B)))),
inference(paramod,[status(thm)],[c_1197,c_5808]) ).
cnf(c_5810,plain,
join(A,meet(A,join(B,meet(join(B,A),C)))) = join(join(A,meet(B,A)),meet(A,join(B,C))),
inference(paramod,[status(thm)],[c_905,c_5809]) ).
cnf(c_5811,plain,
join(A,meet(A,join(B,meet(join(B,A),C)))) = join(A,join(meet(B,A),meet(A,join(B,C)))),
inference(paramod,[status(thm)],[c_6,c_5810]) ).
cnf(c_1306,plain,
join(A,meet(A,join(B,meet(join(B,A),C)))) = join(A,meet(A,join(B,C))),
inference(paramod,[status(thm)],[c_27,c_5811]) ).
cnf(c_5812,plain,
meet(meet(A,join(B,C)),join(meet(A,join(B,C)),D)) = join(meet(A,join(B,C)),meet(meet(A,join(B,C)),join(meet(A,B),D))),
inference(paramod,[status(thm)],[c_31,c_214]) ).
cnf(c_5813,plain,
join(meet(A,join(B,C)),meet(meet(A,join(B,C)),D)) = join(meet(A,join(B,C)),meet(meet(A,join(B,C)),join(meet(A,B),D))),
inference(paramod,[status(thm)],[c_193,c_5812]) ).
cnf(c_5814,plain,
join(meet(A,join(B,C)),meet(A,meet(join(B,C),D))) = join(meet(A,join(B,C)),meet(meet(A,join(B,C)),join(meet(A,B),D))),
inference(paramod,[status(thm)],[c_5,c_5813]) ).
cnf(c_5815,plain,
join(meet(A,join(B,C)),meet(A,meet(join(B,C),D))) = join(meet(A,join(B,C)),meet(A,meet(join(B,C),join(meet(A,B),D)))),
inference(paramod,[status(thm)],[c_5,c_5814]) ).
cnf(c_1359,plain,
join(meet(A,join(B,C)),meet(A,meet(join(B,C),join(meet(A,B),D)))) = join(meet(A,join(B,C)),meet(A,meet(join(B,C),D))),
inference(copy,[status(thm)],[c_5815]) ).
cnf(c_5816,plain,
meet(join(A,B),join(meet(B,C),meet(meet(B,C),A))) = meet(meet(B,C),join(A,meet(B,C))),
inference(paramod,[status(thm)],[c_10,c_218]) ).
cnf(c_5817,plain,
meet(join(A,B),join(meet(B,C),meet(B,meet(C,A)))) = meet(meet(B,C),join(A,meet(B,C))),
inference(paramod,[status(thm)],[c_5,c_5816]) ).
cnf(c_5818,plain,
meet(B,meet(C,join(A,B))) = meet(meet(B,C),join(A,meet(B,C))),
inference(paramod,[status(thm)],[c_753,c_5817]) ).
cnf(c_5819,plain,
meet(B,meet(C,join(A,B))) = join(meet(B,C),meet(meet(B,C),A)),
inference(paramod,[status(thm)],[c_186,c_5818]) ).
cnf(c_5820,plain,
meet(B,meet(C,join(A,B))) = join(meet(B,C),meet(B,meet(C,A))),
inference(paramod,[status(thm)],[c_5,c_5819]) ).
cnf(c_1449,plain,
join(meet(A,B),meet(A,meet(B,C))) = meet(A,meet(B,join(C,A))),
inference(copy,[status(thm)],[c_5820]) ).
cnf(c_5821,plain,
meet(A,join(join(B,meet(B,C)),A)) = join(A,meet(B,meet(A,join(C,B)))),
inference(paramod,[status(thm)],[c_218,c_186]) ).
cnf(c_5822,plain,
meet(A,join(B,join(meet(B,C),A))) = join(A,meet(B,meet(A,join(C,B)))),
inference(paramod,[status(thm)],[c_6,c_5821]) ).
cnf(c_5823,plain,
join(A,meet(A,join(B,meet(B,C)))) = join(A,meet(B,meet(A,join(C,B)))),
inference(paramod,[status(thm)],[c_213,c_5822]) ).
cnf(c_1465,plain,
join(A,meet(B,meet(A,join(C,B)))) = join(A,meet(A,join(B,meet(B,C)))),
inference(copy,[status(thm)],[c_5823]) ).
cnf(c_5824,plain,
meet(A,meet(join(B,C),join(join(meet(A,B),D),A))) = join(meet(A,join(B,C)),meet(A,meet(join(B,C),D))),
inference(paramod,[status(thm)],[c_1449,c_1359]) ).
cnf(c_5825,plain,
meet(A,meet(join(B,C),join(A,join(meet(A,B),D)))) = join(meet(A,join(B,C)),meet(A,meet(join(B,C),D))),
inference(paramod,[status(thm)],[c_4,c_5824]) ).
cnf(c_1567,plain,
meet(A,meet(join(B,C),join(A,join(meet(A,B),D)))) = meet(A,meet(join(B,C),join(D,A))),
inference(paramod,[status(thm)],[c_1449,c_5825]) ).
cnf(c_5826,plain,
meet(A,meet(join(B,C),join(join(D,meet(A,B)),A))) = join(meet(A,join(B,C)),meet(A,meet(join(B,C),D))),
inference(paramod,[status(thm)],[c_1449,c_1292]) ).
cnf(c_5827,plain,
meet(A,meet(join(B,C),join(A,join(D,meet(A,B))))) = join(meet(A,join(B,C)),meet(A,meet(join(B,C),D))),
inference(paramod,[status(thm)],[c_4,c_5826]) ).
cnf(c_1583,plain,
meet(A,meet(join(B,C),join(A,join(D,meet(A,B))))) = meet(A,meet(join(B,C),join(D,A))),
inference(paramod,[status(thm)],[c_1449,c_5827]) ).
cnf(c_5828,plain,
meet(A,meet(join(B,A),join(C,A))) = join(A,join(meet(A,B),meet(A,meet(join(B,A),C)))),
inference(paramod,[status(thm)],[c_1567,c_1210]) ).
cnf(c_1601,plain,
join(A,join(meet(A,B),meet(A,meet(join(B,A),C)))) = meet(A,meet(join(B,A),join(C,A))),
inference(copy,[status(thm)],[c_5828]) ).
cnf(c_1726,plain,
meet(A,join(B,meet(B,join(C,A)))) = meet(B,join(A,meet(A,join(B,C)))),
inference(paramod,[status(thm)],[c_213,c_238]) ).
cnf(c_1727,plain,
meet(A,join(B,meet(B,join(A,C)))) = meet(B,join(A,meet(A,join(B,C)))),
inference(paramod,[status(thm)],[c_214,c_238]) ).
cnf(c_5829,plain,
meet(join(A,join(B,C)),join(meet(D,join(C,B)),meet(D,join(B,C)))) = meet(meet(D,join(C,B)),join(join(B,C),A)),
inference(paramod,[status(thm)],[c_321,c_876]) ).
cnf(c_5830,plain,
meet(join(A,join(B,C)),meet(D,join(B,C))) = meet(meet(D,join(C,B)),join(join(B,C),A)),
inference(paramod,[status(thm)],[c_316,c_5829]) ).
cnf(c_5831,plain,
meet(join(A,join(B,C)),meet(D,join(B,C))) = meet(meet(D,join(C,B)),join(B,join(C,A))),
inference(paramod,[status(thm)],[c_6,c_5830]) ).
cnf(c_5832,plain,
meet(join(A,join(B,C)),meet(D,join(B,C))) = meet(D,meet(join(C,B),join(B,join(C,A)))),
inference(paramod,[status(thm)],[c_5,c_5831]) ).
cnf(c_1783,plain,
meet(join(A,join(B,C)),meet(D,join(B,C))) = meet(D,join(C,join(B,meet(A,join(C,B))))),
inference(paramod,[status(thm)],[c_769,c_5832]) ).
cnf(c_1972,plain,
join(A,meet(A,meet(join(B,A),join(C,A)))) = meet(join(B,A),join(A,meet(A,C))),
inference(paramod,[status(thm)],[c_218,c_569]) ).
cnf(c_5833,plain,
meet(join(meet(A,B),B),join(C,meet(A,join(B,meet(B,C))))) = join(meet(meet(A,B),B),meet(C,join(meet(B,C),meet(A,B)))),
inference(paramod,[status(thm)],[c_886,c_12]) ).
cnf(c_5834,plain,
meet(join(B,meet(A,B)),join(C,meet(A,join(B,meet(B,C))))) = join(meet(meet(A,B),B),meet(C,join(meet(B,C),meet(A,B)))),
inference(paramod,[status(thm)],[c_4,c_5833]) ).
cnf(c_5835,plain,
meet(join(B,meet(A,B)),join(C,meet(B,A))) = join(meet(meet(A,B),B),meet(C,join(meet(B,C),meet(A,B)))),
inference(paramod,[status(thm)],[c_508,c_5834]) ).
cnf(c_5836,plain,
meet(B,meet(join(A,B),join(C,meet(B,A)))) = join(meet(meet(A,B),B),meet(C,join(meet(B,C),meet(A,B)))),
inference(paramod,[status(thm)],[c_1197,c_5835]) ).
cnf(c_5837,plain,
meet(B,meet(join(A,B),join(C,meet(B,A)))) = join(meet(B,meet(A,B)),meet(C,join(meet(B,C),meet(A,B)))),
inference(paramod,[status(thm)],[c_3,c_5836]) ).
cnf(c_5838,plain,
meet(B,meet(join(A,B),join(C,meet(B,A)))) = join(meet(A,B),meet(C,join(meet(B,C),meet(A,B)))),
inference(paramod,[status(thm)],[c_17,c_5837]) ).
cnf(c_2066,plain,
meet(A,meet(join(B,A),join(C,meet(A,B)))) = join(meet(B,A),meet(A,C)),
inference(paramod,[status(thm)],[c_386,c_5838]) ).
cnf(c_5839,plain,
join(A,join(meet(A,B),meet(join(A,A),join(A,meet(B,C))))) = meet(join(A,A),join(A,join(meet(A,B),meet(B,C)))),
inference(paramod,[status(thm)],[c_202,c_41]) ).
cnf(c_5840,plain,
join(A,join(meet(A,B),meet(A,join(A,meet(B,C))))) = meet(join(A,A),join(A,join(meet(A,B),meet(B,C)))),
inference(paramod,[status(thm)],[c_2,c_5839]) ).
cnf(c_5841,plain,
join(A,join(meet(A,B),join(A,meet(A,meet(B,C))))) = meet(join(A,A),join(A,join(meet(A,B),meet(B,C)))),
inference(paramod,[status(thm)],[c_193,c_5840]) ).
cnf(c_5842,plain,
join(A,join(A,join(meet(A,B),meet(A,meet(B,C))))) = meet(join(A,A),join(A,join(meet(A,B),meet(B,C)))),
inference(paramod,[status(thm)],[c_24,c_5841]) ).
cnf(c_5843,plain,
join(A,join(A,meet(A,meet(B,join(C,A))))) = meet(join(A,A),join(A,join(meet(A,B),meet(B,C)))),
inference(paramod,[status(thm)],[c_1449,c_5842]) ).
cnf(c_5844,plain,
join(A,meet(A,meet(B,join(C,A)))) = meet(join(A,A),join(A,join(meet(A,B),meet(B,C)))),
inference(paramod,[status(thm)],[c_21,c_5843]) ).
cnf(c_5845,plain,
join(A,meet(A,meet(B,join(C,A)))) = meet(A,join(A,join(meet(A,B),meet(B,C)))),
inference(paramod,[status(thm)],[c_2,c_5844]) ).
cnf(c_5846,plain,
join(A,meet(A,meet(B,join(C,A)))) = meet(A,join(A,meet(B,C))),
inference(paramod,[status(thm)],[c_202,c_5845]) ).
cnf(c_2308,plain,
join(A,meet(A,meet(B,join(C,A)))) = join(A,meet(A,meet(B,C))),
inference(paramod,[status(thm)],[c_193,c_5846]) ).
cnf(c_5847,plain,
join(A,meet(A,meet(join(B,A),C))) = meet(join(B,A),join(A,meet(A,C))),
inference(paramod,[status(thm)],[c_2308,c_1972]) ).
cnf(c_2336,plain,
meet(join(A,B),join(B,meet(B,C))) = join(B,meet(B,meet(join(A,B),C))),
inference(copy,[status(thm)],[c_5847]) ).
cnf(c_5848,plain,
meet(join(meet(A,B),C),join(B,meet(A,join(B,meet(B,C))))) = join(meet(meet(A,B),C),meet(B,join(meet(C,B),meet(A,B)))),
inference(paramod,[status(thm)],[c_990,c_12]) ).
cnf(c_2350,plain,
meet(join(meet(A,B),C),join(B,meet(A,join(B,meet(B,C))))) = join(meet(A,meet(B,C)),meet(B,join(meet(C,B),meet(A,B)))),
inference(paramod,[status(thm)],[c_5,c_5848]) ).
cnf(c_5849,plain,
meet(join(A,join(B,meet(B,C))),meet(D,join(B,meet(B,C)))) = meet(D,join(join(B,meet(B,C)),meet(B,meet(join(C,B),A)))),
inference(paramod,[status(thm)],[c_211,c_990]) ).
cnf(c_5850,plain,
meet(join(A,join(B,meet(B,C))),meet(D,join(B,meet(B,C)))) = meet(D,join(B,join(meet(B,C),meet(B,meet(join(C,B),A))))),
inference(paramod,[status(thm)],[c_6,c_5849]) ).
cnf(c_2421,plain,
meet(join(A,join(B,meet(B,C))),meet(D,join(B,meet(B,C)))) = meet(D,meet(B,meet(join(C,B),join(A,B)))),
inference(paramod,[status(thm)],[c_1601,c_5850]) ).
cnf(c_5851,plain,
meet(A,meet(A,meet(join(B,A),join(meet(A,B),C)))) = meet(A,join(meet(A,B),C)),
inference(paramod,[status(thm)],[c_211,c_1087]) ).
cnf(c_2508,plain,
meet(A,meet(join(B,A),join(meet(A,B),C))) = meet(A,join(meet(A,B),C)),
inference(paramod,[status(thm)],[c_16,c_5851]) ).
cnf(c_2605,plain,
join(A,join(meet(A,B),meet(C,meet(D,B)))) = join(A,meet(B,meet(C,D))),
inference(paramod,[status(thm)],[c_5,c_1135]) ).
cnf(c_5852,plain,
join(A,join(meet(meet(B,A),C),meet(B,A))) = join(A,meet(meet(B,A),C)),
inference(paramod,[status(thm)],[c_17,c_1136]) ).
cnf(c_5853,plain,
join(A,join(meet(B,meet(A,C)),meet(B,A))) = join(A,meet(meet(B,A),C)),
inference(paramod,[status(thm)],[c_5,c_5852]) ).
cnf(c_5854,plain,
join(A,join(meet(B,A),meet(B,meet(A,C)))) = join(A,meet(meet(B,A),C)),
inference(paramod,[status(thm)],[c_4,c_5853]) ).
cnf(c_5855,plain,
join(A,meet(B,meet(A,join(C,B)))) = join(A,meet(meet(B,A),C)),
inference(paramod,[status(thm)],[c_1449,c_5854]) ).
cnf(c_2706,plain,
join(A,meet(B,meet(A,join(C,B)))) = join(A,meet(B,meet(A,C))),
inference(paramod,[status(thm)],[c_5,c_5855]) ).
cnf(c_5856,plain,
join(join(A,B),meet(C,join(A,B))) = join(join(A,B),meet(C,A)),
inference(paramod,[status(thm)],[c_28,c_1136]) ).
cnf(c_5857,plain,
join(A,join(B,meet(C,join(A,B)))) = join(join(A,B),meet(C,A)),
inference(paramod,[status(thm)],[c_6,c_5856]) ).
cnf(c_2712,plain,
join(A,join(B,meet(C,join(A,B)))) = join(A,join(B,meet(C,A))),
inference(paramod,[status(thm)],[c_6,c_5857]) ).
cnf(c_5858,plain,
join(join(A,B),meet(C,join(B,A))) = join(join(A,B),meet(C,B)),
inference(paramod,[status(thm)],[c_243,c_1136]) ).
cnf(c_5859,plain,
join(A,join(B,meet(C,join(B,A)))) = join(join(A,B),meet(C,B)),
inference(paramod,[status(thm)],[c_6,c_5858]) ).
cnf(c_2722,plain,
join(A,join(B,meet(C,join(B,A)))) = join(A,join(B,meet(C,B))),
inference(paramod,[status(thm)],[c_6,c_5859]) ).
cnf(c_5860,plain,
meet(meet(A,B),join(C,meet(A,B))) = join(meet(A,B),meet(meet(A,B),join(C,meet(C,A)))),
inference(paramod,[status(thm)],[c_1136,c_214]) ).
cnf(c_5861,plain,
join(meet(A,B),meet(meet(A,B),C)) = join(meet(A,B),meet(meet(A,B),join(C,meet(C,A)))),
inference(paramod,[status(thm)],[c_186,c_5860]) ).
cnf(c_5862,plain,
join(meet(A,B),meet(A,meet(B,C))) = join(meet(A,B),meet(meet(A,B),join(C,meet(C,A)))),
inference(paramod,[status(thm)],[c_5,c_5861]) ).
cnf(c_5863,plain,
meet(A,meet(B,join(C,A))) = join(meet(A,B),meet(meet(A,B),join(C,meet(C,A)))),
inference(paramod,[status(thm)],[c_1449,c_5862]) ).
cnf(c_5864,plain,
meet(A,meet(B,join(C,A))) = join(meet(A,B),meet(A,meet(B,join(C,meet(C,A))))),
inference(paramod,[status(thm)],[c_5,c_5863]) ).
cnf(c_5865,plain,
meet(A,meet(B,join(C,A))) = join(meet(A,B),meet(B,meet(C,A))),
inference(paramod,[status(thm)],[c_273,c_5864]) ).
cnf(c_2737,plain,
join(meet(A,B),meet(B,meet(C,A))) = meet(A,meet(B,join(C,A))),
inference(copy,[status(thm)],[c_5865]) ).
cnf(c_5866,plain,
join(A,meet(B,meet(A,C))) = join(A,meet(A,join(B,meet(B,C)))),
inference(paramod,[status(thm)],[c_2706,c_1465]) ).
cnf(c_2763,plain,
join(A,meet(A,join(B,meet(B,C)))) = join(A,meet(B,meet(A,C))),
inference(copy,[status(thm)],[c_5866]) ).
cnf(c_2772,plain,
meet(join(A,join(B,C)),meet(D,join(B,C))) = meet(D,join(C,join(B,meet(A,C)))),
inference(paramod,[status(thm)],[c_2712,c_1783]) ).
cnf(c_5867,plain,
meet(A,meet(B,join(join(C,B),A))) = meet(A,join(B,meet(B,C))),
inference(paramod,[status(thm)],[c_2737,c_585]) ).
cnf(c_5868,plain,
meet(A,meet(B,join(C,join(B,A)))) = meet(A,join(B,meet(B,C))),
inference(paramod,[status(thm)],[c_6,c_5867]) ).
cnf(c_2810,plain,
meet(A,join(B,meet(B,join(C,A)))) = meet(A,join(B,meet(B,C))),
inference(paramod,[status(thm)],[c_214,c_5868]) ).
cnf(c_5869,plain,
meet(D,join(meet(B,C),join(B,meet(A,meet(B,C))))) = meet(D,meet(B,meet(join(C,B),join(A,B)))),
inference(paramod,[status(thm)],[c_2772,c_2421]) ).
cnf(c_5870,plain,
meet(D,join(B,join(meet(B,C),meet(A,meet(B,C))))) = meet(D,meet(B,meet(join(C,B),join(A,B)))),
inference(paramod,[status(thm)],[c_24,c_5869]) ).
cnf(c_5871,plain,
meet(D,join(B,meet(C,meet(A,B)))) = meet(D,meet(B,meet(join(C,B),join(A,B)))),
inference(paramod,[status(thm)],[c_2605,c_5870]) ).
cnf(c_2822,plain,
meet(A,meet(B,meet(join(C,B),join(D,B)))) = meet(A,join(B,meet(C,meet(D,B)))),
inference(copy,[status(thm)],[c_5871]) ).
cnf(c_5872,plain,
meet(A,join(B,meet(B,C))) = meet(B,join(A,meet(A,join(B,C)))),
inference(paramod,[status(thm)],[c_2810,c_1726]) ).
cnf(c_2862,plain,
meet(A,join(B,meet(B,join(A,C)))) = meet(B,join(A,meet(A,C))),
inference(copy,[status(thm)],[c_5872]) ).
cnf(c_5873,plain,
meet(B,join(A,meet(A,C))) = meet(B,join(A,meet(A,join(B,C)))),
inference(paramod,[status(thm)],[c_2862,c_1727]) ).
cnf(c_2904,plain,
meet(A,join(B,meet(B,C))) = meet(B,join(A,meet(A,C))),
inference(paramod,[status(thm)],[c_2862,c_5873]) ).
cnf(c_2914,plain,
meet(A,join(B,meet(C,B))) = meet(B,join(A,meet(A,C))),
inference(paramod,[status(thm)],[c_3,c_2904]) ).
cnf(c_5874,plain,
meet(A,join(join(B,meet(B,C)),A)) = join(A,meet(B,join(A,meet(A,C)))),
inference(paramod,[status(thm)],[c_2904,c_186]) ).
cnf(c_5875,plain,
meet(A,join(B,join(meet(B,C),A))) = join(A,meet(B,join(A,meet(A,C)))),
inference(paramod,[status(thm)],[c_6,c_5874]) ).
cnf(c_5876,plain,
join(A,meet(A,join(B,meet(B,C)))) = join(A,meet(B,join(A,meet(A,C)))),
inference(paramod,[status(thm)],[c_213,c_5875]) ).
cnf(c_5877,plain,
join(A,meet(B,meet(A,C))) = join(A,meet(B,join(A,meet(A,C)))),
inference(paramod,[status(thm)],[c_2763,c_5876]) ).
cnf(c_2934,plain,
join(A,meet(B,join(A,meet(A,C)))) = join(A,meet(B,meet(A,C))),
inference(copy,[status(thm)],[c_5877]) ).
cnf(c_5878,plain,
meet(A,join(join(B,C),meet(D,join(C,B)))) = meet(join(B,C),join(A,meet(A,join(D,meet(D,C))))),
inference(paramod,[status(thm)],[c_751,c_2904]) ).
cnf(c_5879,plain,
meet(A,join(B,join(C,meet(D,join(C,B))))) = meet(join(B,C),join(A,meet(A,join(D,meet(D,C))))),
inference(paramod,[status(thm)],[c_6,c_5878]) ).
cnf(c_5880,plain,
meet(A,join(B,join(C,meet(D,C)))) = meet(join(B,C),join(A,meet(A,join(D,meet(D,C))))),
inference(paramod,[status(thm)],[c_2722,c_5879]) ).
cnf(c_5881,plain,
meet(A,join(B,join(C,meet(D,C)))) = meet(join(B,C),join(A,meet(D,meet(A,C)))),
inference(paramod,[status(thm)],[c_2763,c_5880]) ).
cnf(c_2967,plain,
meet(join(A,B),join(C,meet(D,meet(C,B)))) = meet(C,join(A,join(B,meet(D,B)))),
inference(copy,[status(thm)],[c_5881]) ).
cnf(c_5882,plain,
meet(A,join(join(B,meet(B,C)),meet(join(B,meet(B,C)),D))) = meet(B,meet(join(C,B),join(A,meet(A,D)))),
inference(paramod,[status(thm)],[c_2904,c_211]) ).
cnf(c_5883,plain,
meet(A,join(join(B,meet(B,C)),meet(B,meet(join(C,B),D)))) = meet(B,meet(join(C,B),join(A,meet(A,D)))),
inference(paramod,[status(thm)],[c_211,c_5882]) ).
cnf(c_5884,plain,
meet(A,join(B,join(meet(B,C),meet(B,meet(join(C,B),D))))) = meet(B,meet(join(C,B),join(A,meet(A,D)))),
inference(paramod,[status(thm)],[c_6,c_5883]) ).
cnf(c_5885,plain,
meet(A,meet(B,meet(join(C,B),join(D,B)))) = meet(B,meet(join(C,B),join(A,meet(A,D)))),
inference(paramod,[status(thm)],[c_1601,c_5884]) ).
cnf(c_5886,plain,
meet(A,join(B,meet(C,meet(D,B)))) = meet(B,meet(join(C,B),join(A,meet(A,D)))),
inference(paramod,[status(thm)],[c_2822,c_5885]) ).
cnf(c_2981,plain,
meet(A,meet(join(B,A),join(C,meet(C,D)))) = meet(C,join(A,meet(B,meet(D,A)))),
inference(copy,[status(thm)],[c_5886]) ).
cnf(c_5887,plain,
join(A,meet(A,join(join(B,A),meet(join(B,A),C)))) = meet(join(B,A),join(A,meet(A,C))),
inference(paramod,[status(thm)],[c_2904,c_569]) ).
cnf(c_5888,plain,
join(A,meet(A,join(B,join(A,meet(join(B,A),C))))) = meet(join(B,A),join(A,meet(A,C))),
inference(paramod,[status(thm)],[c_6,c_5887]) ).
cnf(c_5889,plain,
join(A,join(A,meet(A,join(B,meet(join(B,A),C))))) = meet(join(B,A),join(A,meet(A,C))),
inference(paramod,[status(thm)],[c_214,c_5888]) ).
cnf(c_5890,plain,
join(A,join(A,meet(A,join(B,C)))) = meet(join(B,A),join(A,meet(A,C))),
inference(paramod,[status(thm)],[c_1306,c_5889]) ).
cnf(c_5891,plain,
join(A,meet(A,join(B,C))) = meet(join(B,A),join(A,meet(A,C))),
inference(paramod,[status(thm)],[c_21,c_5890]) ).
cnf(c_5892,plain,
join(A,meet(A,join(B,C))) = join(A,meet(A,meet(join(B,A),C))),
inference(paramod,[status(thm)],[c_2336,c_5891]) ).
cnf(c_3004,plain,
join(A,meet(A,meet(join(B,A),C))) = join(A,meet(A,join(B,C))),
inference(copy,[status(thm)],[c_5892]) ).
cnf(c_5893,plain,
meet(join(meet(A,B),C),join(B,meet(A,meet(B,C)))) = join(meet(A,meet(B,C)),meet(B,join(meet(C,B),meet(A,B)))),
inference(paramod,[status(thm)],[c_2934,c_2350]) ).
cnf(c_5894,plain,
meet(B,join(meet(A,B),join(C,meet(A,C)))) = join(meet(A,meet(B,C)),meet(B,join(meet(C,B),meet(A,B)))),
inference(paramod,[status(thm)],[c_2967,c_5893]) ).
cnf(c_3026,plain,
join(meet(A,meet(B,C)),meet(B,join(meet(C,B),meet(A,B)))) = meet(B,join(meet(A,B),join(C,meet(A,C)))),
inference(copy,[status(thm)],[c_5894]) ).
cnf(c_3047,plain,
meet(join(A,B),join(B,meet(B,C))) = join(B,meet(B,join(A,C))),
inference(paramod,[status(thm)],[c_3004,c_2336]) ).
cnf(c_5895,plain,
meet(A,join(join(meet(B,C),D),join(D,meet(B,C)))) = meet(join(meet(B,C),D),join(A,meet(A,join(B,D)))),
inference(paramod,[status(thm)],[c_398,c_2914]) ).
cnf(c_5896,plain,
meet(A,join(D,join(join(meet(B,C),D),meet(B,C)))) = meet(join(meet(B,C),D),join(A,meet(A,join(B,D)))),
inference(paramod,[status(thm)],[c_24,c_5895]) ).
cnf(c_5897,plain,
meet(A,join(D,join(meet(B,C),join(meet(B,C),D)))) = meet(join(meet(B,C),D),join(A,meet(A,join(B,D)))),
inference(paramod,[status(thm)],[c_4,c_5896]) ).
cnf(c_5898,plain,
meet(A,join(D,join(meet(B,C),D))) = meet(join(meet(B,C),D),join(A,meet(A,join(B,D)))),
inference(paramod,[status(thm)],[c_21,c_5897]) ).
cnf(c_5899,plain,
meet(A,join(meet(B,C),D)) = meet(join(meet(B,C),D),join(A,meet(A,join(B,D)))),
inference(paramod,[status(thm)],[c_22,c_5898]) ).
cnf(c_3224,plain,
meet(join(meet(A,B),C),join(D,meet(D,join(A,C)))) = meet(D,join(meet(A,B),C)),
inference(copy,[status(thm)],[c_5899]) ).
cnf(c_5900,plain,
meet(A,join(join(B,meet(B,C)),meet(B,join(C,D)))) = meet(join(B,meet(B,C)),join(A,meet(A,join(D,C)))),
inference(paramod,[status(thm)],[c_751,c_2914]) ).
cnf(c_5901,plain,
meet(A,join(B,join(meet(B,C),meet(B,join(C,D))))) = meet(join(B,meet(B,C)),join(A,meet(A,join(D,C)))),
inference(paramod,[status(thm)],[c_6,c_5900]) ).
cnf(c_5902,plain,
meet(A,join(B,meet(B,join(C,D)))) = meet(join(B,meet(B,C)),join(A,meet(A,join(D,C)))),
inference(paramod,[status(thm)],[c_8,c_5901]) ).
cnf(c_5903,plain,
meet(A,join(B,meet(B,join(C,D)))) = meet(B,meet(join(C,B),join(A,meet(A,join(D,C))))),
inference(paramod,[status(thm)],[c_211,c_5902]) ).
cnf(c_5904,plain,
meet(A,join(B,meet(B,join(C,D)))) = meet(A,join(B,meet(C,meet(join(D,C),B)))),
inference(paramod,[status(thm)],[c_2981,c_5903]) ).
cnf(c_3239,plain,
meet(A,join(B,meet(C,meet(join(D,C),B)))) = meet(A,join(B,meet(B,join(C,D)))),
inference(copy,[status(thm)],[c_5904]) ).
cnf(c_5905,plain,
meet(join(A,B),join(C,meet(join(D,meet(D,B)),C))) = meet(C,join(join(A,B),meet(D,join(B,A)))),
inference(paramod,[status(thm)],[c_751,c_2914]) ).
cnf(c_5906,plain,
meet(join(A,B),join(C,meet(D,meet(join(B,D),C)))) = meet(C,join(join(A,B),meet(D,join(B,A)))),
inference(paramod,[status(thm)],[c_211,c_5905]) ).
cnf(c_5907,plain,
meet(join(A,B),join(C,meet(C,join(D,B)))) = meet(C,join(join(A,B),meet(D,join(B,A)))),
inference(paramod,[status(thm)],[c_3239,c_5906]) ).
cnf(c_5908,plain,
meet(join(A,B),join(C,meet(C,join(D,B)))) = meet(C,join(A,join(B,meet(D,join(B,A))))),
inference(paramod,[status(thm)],[c_6,c_5907]) ).
cnf(c_3240,plain,
meet(join(A,B),join(C,meet(C,join(D,B)))) = meet(C,join(A,join(B,meet(D,B)))),
inference(paramod,[status(thm)],[c_2722,c_5908]) ).
cnf(c_3341,plain,
meet(A,join(meet(B,C),join(D,meet(B,D)))) = meet(A,join(meet(B,C),D)),
inference(paramod,[status(thm)],[c_3240,c_3224]) ).
cnf(c_3356,plain,
join(meet(A,meet(B,C)),meet(B,join(meet(C,B),meet(A,B)))) = meet(B,join(meet(A,B),C)),
inference(paramod,[status(thm)],[c_3341,c_3026]) ).
cnf(c_5909,plain,
join(meet(A,B),meet(A,meet(join(B,A),join(C,meet(A,B))))) = meet(join(A,meet(A,B)),join(meet(A,B),C)),
inference(paramod,[status(thm)],[c_211,c_1190]) ).
cnf(c_5910,plain,
join(meet(A,B),join(meet(B,A),meet(A,C))) = meet(join(A,meet(A,B)),join(meet(A,B),C)),
inference(paramod,[status(thm)],[c_2066,c_5909]) ).
cnf(c_5911,plain,
join(meet(B,A),meet(A,C)) = meet(join(A,meet(A,B)),join(meet(A,B),C)),
inference(paramod,[status(thm)],[c_137,c_5910]) ).
cnf(c_5912,plain,
join(meet(B,A),meet(A,C)) = meet(A,meet(join(B,A),join(meet(A,B),C))),
inference(paramod,[status(thm)],[c_211,c_5911]) ).
cnf(c_5913,plain,
join(meet(B,A),meet(A,C)) = meet(A,join(meet(A,B),C)),
inference(paramod,[status(thm)],[c_2508,c_5912]) ).
cnf(c_3435,plain,
meet(A,join(meet(A,B),C)) = join(meet(B,A),meet(A,C)),
inference(copy,[status(thm)],[c_5913]) ).
cnf(c_5914,plain,
join(A,meet(join(B,A),join(meet(A,C),A))) = meet(A,meet(join(B,A),join(C,A))),
inference(paramod,[status(thm)],[c_218,c_1190]) ).
cnf(c_5915,plain,
join(A,meet(join(B,A),join(A,meet(A,C)))) = meet(A,meet(join(B,A),join(C,A))),
inference(paramod,[status(thm)],[c_4,c_5914]) ).
cnf(c_5916,plain,
join(A,join(A,meet(A,join(B,C)))) = meet(A,meet(join(B,A),join(C,A))),
inference(paramod,[status(thm)],[c_3047,c_5915]) ).
cnf(c_5917,plain,
join(A,meet(A,join(B,C))) = meet(A,meet(join(B,A),join(C,A))),
inference(paramod,[status(thm)],[c_21,c_5916]) ).
cnf(c_3437,plain,
meet(A,meet(join(B,A),join(C,A))) = join(A,meet(A,join(B,C))),
inference(copy,[status(thm)],[c_5917]) ).
cnf(c_3462,plain,
meet(A,meet(join(B,A),join(meet(A,B),C))) = join(meet(B,A),meet(A,C)),
inference(paramod,[status(thm)],[c_3435,c_2508]) ).
cnf(c_3478,plain,
join(A,join(meet(A,B),meet(A,meet(join(B,A),C)))) = join(A,meet(A,join(B,C))),
inference(paramod,[status(thm)],[c_3437,c_1601]) ).
cnf(c_3499,plain,
meet(A,join(meet(B,A),C)) = join(meet(B,A),meet(A,C)),
inference(paramod,[status(thm)],[c_3,c_3435]) ).
cnf(c_3500,plain,
meet(A,join(B,meet(A,C))) = join(meet(C,A),meet(A,B)),
inference(paramod,[status(thm)],[c_4,c_3435]) ).
cnf(c_5918,plain,
meet(join(A,meet(A,B)),join(meet(join(A,meet(A,B)),B),C)) = join(meet(A,B),meet(join(A,meet(A,B)),C)),
inference(paramod,[status(thm)],[c_184,c_3435]) ).
cnf(c_5919,plain,
meet(join(A,meet(A,B)),join(meet(B,join(A,meet(A,B))),C)) = join(meet(A,B),meet(join(A,meet(A,B)),C)),
inference(paramod,[status(thm)],[c_3,c_5918]) ).
cnf(c_5920,plain,
meet(join(A,meet(A,B)),join(meet(A,B),C)) = join(meet(A,B),meet(join(A,meet(A,B)),C)),
inference(paramod,[status(thm)],[c_184,c_5919]) ).
cnf(c_5921,plain,
meet(A,meet(join(B,A),join(meet(A,B),C))) = join(meet(A,B),meet(join(A,meet(A,B)),C)),
inference(paramod,[status(thm)],[c_211,c_5920]) ).
cnf(c_5922,plain,
join(meet(B,A),meet(A,C)) = join(meet(A,B),meet(join(A,meet(A,B)),C)),
inference(paramod,[status(thm)],[c_3462,c_5921]) ).
cnf(c_5923,plain,
join(meet(B,A),meet(A,C)) = join(meet(A,B),meet(A,meet(join(B,A),C))),
inference(paramod,[status(thm)],[c_211,c_5922]) ).
cnf(c_3520,plain,
join(meet(A,B),meet(A,meet(join(B,A),C))) = join(meet(B,A),meet(A,C)),
inference(copy,[status(thm)],[c_5923]) ).
cnf(c_5924,plain,
join(meet(A,meet(B,C)),join(meet(C,B),meet(B,meet(A,B)))) = meet(B,join(meet(A,B),C)),
inference(paramod,[status(thm)],[c_3499,c_3356]) ).
cnf(c_5925,plain,
join(meet(A,meet(B,C)),join(meet(C,B),meet(A,B))) = meet(B,join(meet(A,B),C)),
inference(paramod,[status(thm)],[c_17,c_5924]) ).
cnf(c_5926,plain,
join(meet(C,B),join(meet(A,meet(B,C)),meet(A,B))) = meet(B,join(meet(A,B),C)),
inference(paramod,[status(thm)],[c_24,c_5925]) ).
cnf(c_5927,plain,
join(meet(C,B),join(meet(A,B),meet(A,meet(B,C)))) = meet(B,join(meet(A,B),C)),
inference(paramod,[status(thm)],[c_4,c_5926]) ).
cnf(c_5928,plain,
join(meet(C,B),meet(A,meet(B,join(C,A)))) = meet(B,join(meet(A,B),C)),
inference(paramod,[status(thm)],[c_1449,c_5927]) ).
cnf(c_3619,plain,
join(meet(A,B),meet(C,meet(B,join(A,C)))) = join(meet(C,B),meet(B,A)),
inference(paramod,[status(thm)],[c_3499,c_5928]) ).
cnf(c_3999,plain,
join(A,join(meet(B,A),meet(A,C))) = join(A,meet(A,join(B,C))),
inference(paramod,[status(thm)],[c_3520,c_3478]) ).
cnf(c_4471,plain,
meet(A,join(B,meet(C,A))) = join(meet(C,A),meet(A,B)),
inference(paramod,[status(thm)],[c_4,c_3499]) ).
cnf(c_4531,plain,
meet(join(A,B),join(C,meet(B,join(A,C)))) = join(meet(A,B),join(meet(A,C),meet(C,B))),
inference(paramod,[status(thm)],[c_4471,c_603]) ).
cnf(c_5929,plain,
meet(A,join(B,join(meet(C,B),meet(B,D)))) = meet(B,meet(A,join(join(D,meet(B,C)),B))),
inference(paramod,[status(thm)],[c_3500,c_218]) ).
cnf(c_5930,plain,
meet(A,join(B,meet(B,join(C,D)))) = meet(B,meet(A,join(join(D,meet(B,C)),B))),
inference(paramod,[status(thm)],[c_3999,c_5929]) ).
cnf(c_5931,plain,
meet(A,join(B,meet(B,join(C,D)))) = meet(B,meet(A,join(B,join(D,meet(B,C))))),
inference(paramod,[status(thm)],[c_4,c_5930]) ).
cnf(c_4583,plain,
meet(A,meet(B,join(A,join(C,meet(A,D))))) = meet(B,join(A,meet(A,join(D,C)))),
inference(copy,[status(thm)],[c_5931]) ).
cnf(c_4670,plain,
meet(join(A,B),join(C,meet(C,join(A,D)))) = meet(C,meet(join(A,B),join(D,C))),
inference(paramod,[status(thm)],[c_4583,c_1583]) ).
cnf(c_5932,plain,
meet(B,meet(join(A,meet(B,join(C,A))),join(C,B))) = meet(B,join(A,C)),
inference(paramod,[status(thm)],[c_4670,c_1012]) ).
cnf(c_5933,plain,
meet(B,meet(join(C,B),join(A,meet(B,join(C,A))))) = meet(B,join(A,C)),
inference(paramod,[status(thm)],[c_3,c_5932]) ).
cnf(c_5934,plain,
meet(B,join(meet(C,B),join(meet(C,A),meet(A,B)))) = meet(B,join(A,C)),
inference(paramod,[status(thm)],[c_4531,c_5933]) ).
cnf(c_5935,plain,
join(meet(C,B),meet(B,join(meet(C,A),meet(A,B)))) = meet(B,join(A,C)),
inference(paramod,[status(thm)],[c_3499,c_5934]) ).
cnf(c_5936,plain,
join(meet(C,B),join(meet(A,B),meet(B,meet(C,A)))) = meet(B,join(A,C)),
inference(paramod,[status(thm)],[c_4471,c_5935]) ).
cnf(c_5937,plain,
join(meet(C,B),meet(A,meet(B,join(C,A)))) = meet(B,join(A,C)),
inference(paramod,[status(thm)],[c_2737,c_5936]) ).
cnf(c_4779,plain,
join(meet(A,B),meet(B,C)) = meet(B,join(A,C)),
inference(paramod,[status(thm)],[c_3619,c_5937]) ).
cnf(c_5616,plain,
join(meet(A,B),meet(A,C)) = meet(A,join(B,C)),
inference(paramod,[status(thm)],[c_3,c_4779]) ).
cnf(c_5617,plain,
$false,
inference(resolve,[status(thm)],[c_5616,c_14]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LAT020-1 : TPTP v9.3.1. Released v2.2.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n002.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.02/0.36 % CPULimit : 300
% 0.02/0.36 % WCLimit : 300
% 0.02/0.36 % DateTime : Fri Sep 25 19:59:50 UTC 2026
% 0.02/0.36 % CPUTime :
% 0.02/0.36 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.02/0.36 % Process 4013827 was started by sandbox on n002,
% 0.02/0.36 % Fri Sep 25 19:59:50 2026
% 0.02/0.36 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.02/0.37
% 0.02/0.37 % From the command line: assign(max_seconds, 300).
% 15.23/4.45
% 15.23/4.45 % SZS status Unsatisfiable for theBenchmark
% 15.23/4.45
% 15.23/4.45 % Proof 1 at 1.62 (+ 0.23) seconds.
% 15.23/4.45 % Length of proof is 175.
% 15.23/4.45 % Level of proof is 26.
% 15.23/4.45 % Maximum clause weight is 70.000.
% 15.23/4.45 % Given clauses 89.
% 15.23/4.45
% 15.23/4.45 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------