%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : LAT211-1 : TPTP v9.3.1. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n009.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:49 AM UTC 2026
% Result : Unsatisfiable 153.24s 20.78s
% Output : CNFRefutation 153.24s
% Verified :
% SZS Type : Refutation
% Derivation depth : 79
% Number of leaves : 13
% Syntax : Number of formulae : 313 ( 300 unt; 0 def)
% Number of atoms : 334 ( 333 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 49 ( 28 ~; 21 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 1 avg)
% Maximal term depth : 9 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 8 ( 8 usr; 5 con; 0-2 aty)
% Number of variables : 755 ( 121 sgn 23 !; 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(absorption1,axiom,
! [VAR_0,VAR_1] : meet(VAR_0,join(VAR_0,VAR_1)) = VAR_0,
file('theBenchmark.p',absorption1) ).
cnf(c_3,plain,
meet(A,join(A,B)) = A,
inference(clausify,[status(thm)],[absorption1]) ).
fof(absorption2,axiom,
! [VAR_0,VAR_1] : join(VAR_0,meet(VAR_0,VAR_1)) = VAR_0,
file('theBenchmark.p',absorption2) ).
cnf(c_4,plain,
join(A,meet(A,B)) = A,
inference(clausify,[status(thm)],[absorption2]) ).
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_5,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_6,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_7,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_8,plain,
join(join(A,B),C) = join(A,join(B,C)),
inference(clausify,[status(thm)],[associativity_of_join]) ).
fof(complement_join,axiom,
! [VAR_0] : join(VAR_0,complement(VAR_0)) = one,
file('theBenchmark.p',complement_join) ).
cnf(c_9,plain,
join(A,complement(A)) = one,
inference(clausify,[status(thm)],[complement_join]) ).
fof(complement_meet,axiom,
! [VAR_0] : meet(VAR_0,complement(VAR_0)) = zero,
file('theBenchmark.p',complement_meet) ).
cnf(c_10,plain,
meet(A,complement(A)) = zero,
inference(clausify,[status(thm)],[complement_meet]) ).
fof(meet_join_complement,axiom,
! [VAR_0,VAR_1] :
( complement(VAR_0) = VAR_1
| join(VAR_0,VAR_1) != one
| meet(VAR_0,VAR_1) != zero ),
file('theBenchmark.p',meet_join_complement) ).
cnf(c_11,plain,
( complement(A) = B
| join(A,B) != one
| meet(A,B) != zero ),
inference(clausify,[status(thm)],[meet_join_complement]) ).
fof(equation_H69,axiom,
! [VAR_0,VAR_1,VAR_2] : meet(VAR_0,join(VAR_1,VAR_2)) = join(meet(VAR_0,join(VAR_2,meet(VAR_0,VAR_1))),meet(VAR_0,join(VAR_1,meet(VAR_0,VAR_2)))),
file('theBenchmark.p',equation_H69) ).
cnf(c_12,plain,
meet(A,join(B,C)) = join(meet(A,join(C,meet(A,B))),meet(A,join(B,meet(A,C)))),
inference(clausify,[status(thm)],[equation_H69]) ).
cnf(c_13,plain,
join(meet(A,join(B,meet(A,C))),meet(A,join(C,meet(A,B)))) = meet(A,join(C,B)),
inference(copy,[status(thm)],[c_12]) ).
fof(prove_distributivity,axiom,
meet(a,join(b,c)) != join(meet(a,b),meet(a,c)),
file('theBenchmark.p',prove_distributivity) ).
cnf(c_14,plain,
meet(a,join(b,c)) != join(meet(a,b),meet(a,c)),
inference(clausify,[status(thm)],[prove_distributivity]) ).
cnf(c_15,plain,
join(meet(a,b),meet(a,c)) != meet(a,join(b,c)),
inference(copy,[status(thm)],[c_14]) ).
cnf(c_16,plain,
join(A,meet(B,A)) = A,
inference(paramod,[status(thm)],[c_5,c_4]) ).
cnf(c_17,plain,
meet(A,join(B,A)) = A,
inference(paramod,[status(thm)],[c_6,c_3]) ).
cnf(c_32448,plain,
meet(meet(A,B),B) = meet(A,B),
inference(paramod,[status(thm)],[c_1,c_7]) ).
cnf(c_20,plain,
meet(A,meet(B,A)) = meet(B,A),
inference(paramod,[status(thm)],[c_5,c_32448]) ).
cnf(c_21,plain,
meet(A,meet(B,join(meet(A,B),C))) = meet(A,B),
inference(paramod,[status(thm)],[c_7,c_3]) ).
cnf(c_32449,plain,
meet(A,B) = meet(A,meet(join(A,C),B)),
inference(paramod,[status(thm)],[c_3,c_7]) ).
cnf(c_22,plain,
meet(A,meet(join(A,B),C)) = meet(A,C),
inference(copy,[status(thm)],[c_32449]) ).
cnf(c_23,plain,
join(meet(A,B),meet(A,meet(B,C))) = meet(A,B),
inference(paramod,[status(thm)],[c_7,c_4]) ).
cnf(c_32450,plain,
meet(meet(A,B),C) = meet(B,meet(A,C)),
inference(paramod,[status(thm)],[c_5,c_7]) ).
cnf(c_25,plain,
meet(A,meet(B,C)) = meet(B,meet(A,C)),
inference(paramod,[status(thm)],[c_7,c_32450]) ).
cnf(c_29,plain,
meet(join(A,B),join(A,join(B,C))) = join(A,B),
inference(paramod,[status(thm)],[c_8,c_3]) ).
cnf(c_32451,plain,
join(A,B) = join(A,join(meet(A,C),B)),
inference(paramod,[status(thm)],[c_4,c_8]) ).
cnf(c_31,plain,
join(A,join(meet(A,B),C)) = join(A,C),
inference(copy,[status(thm)],[c_32451]) ).
cnf(c_32452,plain,
join(join(A,B),C) = join(B,join(A,C)),
inference(paramod,[status(thm)],[c_6,c_8]) ).
cnf(c_33,plain,
join(A,join(B,C)) = join(B,join(A,C)),
inference(paramod,[status(thm)],[c_8,c_32452]) ).
cnf(c_34,plain,
meet(A,one) = A,
inference(paramod,[status(thm)],[c_9,c_3]) ).
cnf(c_32453,plain,
join(one,A) = join(B,join(complement(B),A)),
inference(paramod,[status(thm)],[c_9,c_8]) ).
cnf(c_35,plain,
join(A,join(complement(A),B)) = join(one,B),
inference(copy,[status(thm)],[c_32453]) ).
cnf(c_32454,plain,
one = join(A,join(B,complement(join(A,B)))),
inference(paramod,[status(thm)],[c_9,c_8]) ).
cnf(c_36,plain,
join(A,join(B,complement(join(A,B)))) = one,
inference(copy,[status(thm)],[c_32454]) ).
cnf(c_37,plain,
join(A,zero) = A,
inference(paramod,[status(thm)],[c_10,c_4]) ).
cnf(c_32455,plain,
meet(zero,A) = meet(B,meet(complement(B),A)),
inference(paramod,[status(thm)],[c_10,c_7]) ).
cnf(c_38,plain,
meet(A,meet(complement(A),B)) = meet(zero,B),
inference(copy,[status(thm)],[c_32455]) ).
cnf(c_32456,plain,
zero = meet(A,meet(B,complement(meet(A,B)))),
inference(paramod,[status(thm)],[c_10,c_7]) ).
cnf(c_39,plain,
meet(A,meet(B,complement(meet(A,B)))) = zero,
inference(copy,[status(thm)],[c_32456]) ).
cnf(c_42,plain,
( complement(A) = B
| join(B,A) != one
| meet(A,B) != zero ),
inference(paramod,[status(thm)],[c_6,c_11]) ).
cnf(c_46,plain,
join(meet(A,join(B,meet(C,A))),meet(A,join(C,meet(A,B)))) = meet(A,join(C,B)),
inference(paramod,[status(thm)],[c_5,c_13]) ).
cnf(c_32457,plain,
join(meet(A,join(meet(A,B),C)),meet(A,join(B,meet(A,C)))) = meet(A,join(B,C)),
inference(paramod,[status(thm)],[c_6,c_13]) ).
cnf(c_48,plain,
join(meet(A,join(B,meet(A,C))),meet(A,join(meet(A,B),C))) = meet(A,join(B,C)),
inference(paramod,[status(thm)],[c_6,c_32457]) ).
cnf(c_32458,plain,
join(meet(A,join(B,meet(A,join(C,D)))),meet(A,join(C,join(D,meet(A,B))))) = meet(A,join(join(C,D),B)),
inference(paramod,[status(thm)],[c_8,c_13]) ).
cnf(c_52,plain,
join(meet(A,join(B,meet(A,join(C,D)))),meet(A,join(C,join(D,meet(A,B))))) = meet(A,join(C,join(D,B))),
inference(paramod,[status(thm)],[c_8,c_32458]) ).
cnf(c_32459,plain,
join(meet(A,join(B,zero)),meet(A,join(complement(A),meet(A,B)))) = meet(A,join(complement(A),B)),
inference(paramod,[status(thm)],[c_10,c_13]) ).
cnf(c_53,plain,
join(meet(A,B),meet(A,join(complement(A),meet(A,B)))) = meet(A,join(complement(A),B)),
inference(paramod,[status(thm)],[c_37,c_32459]) ).
cnf(c_56,plain,
join(A,meet(B,meet(C,A))) = A,
inference(paramod,[status(thm)],[c_7,c_16]) ).
cnf(c_32460,plain,
join(A,B) = join(A,join(meet(C,A),B)),
inference(paramod,[status(thm)],[c_16,c_8]) ).
cnf(c_57,plain,
join(A,join(meet(B,A),C)) = join(A,C),
inference(copy,[status(thm)],[c_32460]) ).
cnf(c_32461,plain,
join(A,B) = join(A,join(B,meet(C,join(A,B)))),
inference(paramod,[status(thm)],[c_16,c_8]) ).
cnf(c_58,plain,
join(A,join(B,meet(C,join(A,B)))) = join(A,B),
inference(copy,[status(thm)],[c_32461]) ).
cnf(c_32462,plain,
A = meet(one,A),
inference(paramod,[status(thm)],[c_34,c_5]) ).
cnf(c_62,plain,
meet(one,A) = A,
inference(copy,[status(thm)],[c_32462]) ).
cnf(c_65,plain,
join(one,A) = one,
inference(paramod,[status(thm)],[c_34,c_16]) ).
cnf(c_66,plain,
join(A,join(complement(A),B)) = one,
inference(paramod,[status(thm)],[c_65,c_35]) ).
cnf(c_32463,plain,
A = join(zero,A),
inference(paramod,[status(thm)],[c_37,c_6]) ).
cnf(c_67,plain,
join(zero,A) = A,
inference(copy,[status(thm)],[c_32463]) ).
cnf(c_32464,plain,
( complement(one) = zero
| join(one,zero) != one ),
inference(resolve,[status(thm)],[c_11,c_62]) ).
cnf(c_70,plain,
complement(one) = zero,
inference(resolve,[status(thm)],[c_32464,c_37]) ).
cnf(c_73,plain,
meet(A,join(B,join(C,A))) = A,
inference(paramod,[status(thm)],[c_8,c_17]) ).
cnf(c_75,plain,
meet(zero,A) = zero,
inference(paramod,[status(thm)],[c_37,c_17]) ).
cnf(c_32465,plain,
one = join(A,one),
inference(paramod,[status(thm)],[c_17,c_62]) ).
cnf(c_76,plain,
join(A,one) = one,
inference(copy,[status(thm)],[c_32465]) ).
cnf(c_77,plain,
meet(A,meet(complement(A),B)) = zero,
inference(paramod,[status(thm)],[c_75,c_38]) ).
cnf(c_32466,plain,
( complement(zero) = one
| join(zero,one) != one ),
inference(resolve,[status(thm)],[c_11,c_34]) ).
cnf(c_78,plain,
complement(zero) = one,
inference(resolve,[status(thm)],[c_32466,c_67]) ).
cnf(c_79,plain,
meet(A,zero) = zero,
inference(paramod,[status(thm)],[c_67,c_16]) ).
cnf(c_32467,plain,
meet(A,meet(B,meet(C,A))) = meet(meet(B,C),A),
inference(paramod,[status(thm)],[c_7,c_20]) ).
cnf(c_87,plain,
meet(A,meet(B,meet(C,A))) = meet(B,meet(C,A)),
inference(paramod,[status(thm)],[c_7,c_32467]) ).
cnf(c_32468,plain,
( complement(A) = join(complement(A),B)
| one != one
| meet(A,join(complement(A),B)) != zero ),
inference(paramod,[status(thm)],[c_66,c_11]) ).
cnf(c_32469,plain,
( join(complement(A),B) = complement(A)
| one != one
| meet(A,join(complement(A),B)) != zero ),
inference(copy,[status(thm)],[c_32468]) ).
cnf(c_92,plain,
( join(complement(A),B) = complement(A)
| meet(A,join(complement(A),B)) != zero ),
inference(copy,[status(thm)],[c_32469]) ).
cnf(c_32470,plain,
join(meet(A,join(join(complement(B),C),meet(A,B))),meet(A,join(B,meet(A,join(complement(B),C))))) = meet(A,one),
inference(paramod,[status(thm)],[c_66,c_13]) ).
cnf(c_32471,plain,
join(meet(A,join(complement(B),join(C,meet(A,B)))),meet(A,join(B,meet(A,join(complement(B),C))))) = meet(A,one),
inference(paramod,[status(thm)],[c_8,c_32470]) ).
cnf(c_32472,plain,
join(meet(A,join(B,meet(A,join(complement(B),C)))),meet(A,join(complement(B),join(C,meet(A,B))))) = meet(A,one),
inference(paramod,[status(thm)],[c_6,c_32471]) ).
cnf(c_32473,plain,
meet(A,join(complement(B),join(C,B))) = meet(A,one),
inference(paramod,[status(thm)],[c_52,c_32472]) ).
cnf(c_93,plain,
meet(A,join(complement(B),join(C,B))) = A,
inference(paramod,[status(thm)],[c_34,c_32473]) ).
cnf(c_94,plain,
meet(A,meet(B,complement(A))) = zero,
inference(paramod,[status(thm)],[c_5,c_77]) ).
cnf(c_32474,plain,
join(meet(A,join(B,zero)),meet(A,join(meet(complement(A),C),meet(A,B)))) = meet(A,join(meet(complement(A),C),B)),
inference(paramod,[status(thm)],[c_77,c_13]) ).
cnf(c_96,plain,
join(meet(A,B),meet(A,join(meet(complement(A),C),meet(A,B)))) = meet(A,join(meet(complement(A),C),B)),
inference(paramod,[status(thm)],[c_37,c_32474]) ).
cnf(c_32475,plain,
join(meet(A,join(meet(B,A),C)),meet(B,A)) = meet(A,join(meet(B,A),C)),
inference(paramod,[status(thm)],[c_21,c_16]) ).
cnf(c_110,plain,
join(meet(A,B),meet(B,join(meet(A,B),C))) = meet(B,join(meet(A,B),C)),
inference(paramod,[status(thm)],[c_6,c_32475]) ).
cnf(c_127,plain,
join(A,meet(B,meet(C,meet(D,A)))) = A,
inference(paramod,[status(thm)],[c_7,c_56]) ).
cnf(c_133,plain,
meet(A,meet(B,join(A,C))) = meet(A,B),
inference(paramod,[status(thm)],[c_5,c_22]) ).
cnf(c_32476,plain,
meet(A,zero) = meet(A,complement(join(A,B))),
inference(paramod,[status(thm)],[c_10,c_22]) ).
cnf(c_32477,plain,
zero = meet(A,complement(join(A,B))),
inference(paramod,[status(thm)],[c_79,c_32476]) ).
cnf(c_135,plain,
meet(A,complement(join(A,B))) = zero,
inference(copy,[status(thm)],[c_32477]) ).
cnf(c_32478,plain,
join(meet(join(A,B),C),meet(A,C)) = meet(join(A,B),C),
inference(paramod,[status(thm)],[c_22,c_16]) ).
cnf(c_139,plain,
join(meet(A,B),meet(join(A,C),B)) = meet(join(A,C),B),
inference(paramod,[status(thm)],[c_6,c_32478]) ).
cnf(c_32479,plain,
meet(A,meet(join(A,B),meet(C,A))) = meet(C,A),
inference(paramod,[status(thm)],[c_20,c_22]) ).
cnf(c_140,plain,
meet(join(A,B),meet(C,A)) = meet(C,A),
inference(paramod,[status(thm)],[c_87,c_32479]) ).
cnf(c_145,plain,
meet(A,complement(join(B,A))) = zero,
inference(paramod,[status(thm)],[c_6,c_135]) ).
cnf(c_32480,plain,
zero = meet(A,meet(B,complement(join(C,meet(A,B))))),
inference(paramod,[status(thm)],[c_145,c_7]) ).
cnf(c_151,plain,
meet(A,meet(B,complement(join(C,meet(A,B))))) = zero,
inference(copy,[status(thm)],[c_32480]) ).
cnf(c_152,plain,
meet(A,complement(join(B,join(C,A)))) = zero,
inference(paramod,[status(thm)],[c_8,c_145]) ).
cnf(c_178,plain,
join(meet(A,B),meet(B,A)) = meet(A,B),
inference(paramod,[status(thm)],[c_20,c_23]) ).
cnf(c_180,plain,
join(A,join(B,complement(join(B,A)))) = one,
inference(paramod,[status(thm)],[c_6,c_36]) ).
cnf(c_32481,plain,
one = join(complement(A),join(B,A)),
inference(paramod,[status(thm)],[c_93,c_62]) ).
cnf(c_195,plain,
join(complement(A),join(B,A)) = one,
inference(copy,[status(thm)],[c_32481]) ).
cnf(c_32482,plain,
join(complement(meet(A,meet(B,C))),meet(A,B)) = one,
inference(paramod,[status(thm)],[c_23,c_195]) ).
cnf(c_220,plain,
join(meet(A,B),complement(meet(A,meet(B,C)))) = one,
inference(paramod,[status(thm)],[c_6,c_32482]) ).
cnf(c_32483,plain,
meet(A,join(B,C)) = meet(join(B,C),meet(A,join(B,join(C,D)))),
inference(paramod,[status(thm)],[c_29,c_25]) ).
cnf(c_241,plain,
meet(join(A,B),meet(C,join(A,join(B,D)))) = meet(C,join(A,B)),
inference(copy,[status(thm)],[c_32483]) ).
cnf(c_32484,plain,
join(A,B) = join(B,join(A,meet(C,meet(D,B)))),
inference(paramod,[status(thm)],[c_56,c_33]) ).
cnf(c_328,plain,
join(A,join(B,meet(C,meet(D,A)))) = join(B,A),
inference(copy,[status(thm)],[c_32484]) ).
cnf(c_343,plain,
join(A,join(B,join(meet(A,C),D))) = join(A,join(B,D)),
inference(paramod,[status(thm)],[c_33,c_31]) ).
cnf(c_32485,plain,
join(A,one) = join(B,join(A,join(C,complement(join(C,B))))),
inference(paramod,[status(thm)],[c_180,c_33]) ).
cnf(c_32486,plain,
one = join(B,join(A,join(C,complement(join(C,B))))),
inference(paramod,[status(thm)],[c_76,c_32485]) ).
cnf(c_345,plain,
join(A,join(B,join(C,complement(join(C,A))))) = one,
inference(copy,[status(thm)],[c_32486]) ).
cnf(c_32487,plain,
( complement(complement(A)) = A
| one != one
| meet(complement(A),A) != zero ),
inference(paramod,[status(thm)],[c_9,c_42]) ).
cnf(c_32488,plain,
( complement(complement(A)) = A
| one != one
| meet(A,complement(A)) != zero ),
inference(paramod,[status(thm)],[c_5,c_32487]) ).
cnf(c_32489,plain,
( complement(complement(A)) = A
| one != one
| zero != zero ),
inference(paramod,[status(thm)],[c_10,c_32488]) ).
cnf(c_32490,plain,
( complement(complement(A)) = A
| one != one ),
inference(copy,[status(thm)],[c_32489]) ).
cnf(c_403,plain,
complement(complement(A)) = A,
inference(copy,[status(thm)],[c_32490]) ).
cnf(c_436,plain,
meet(complement(A),meet(B,A)) = zero,
inference(paramod,[status(thm)],[c_403,c_94]) ).
cnf(c_32491,plain,
join(A,join(B,C)) = join(B,join(A,join(meet(D,B),C))),
inference(paramod,[status(thm)],[c_57,c_33]) ).
cnf(c_582,plain,
join(A,join(B,join(meet(C,A),D))) = join(B,join(A,D)),
inference(copy,[status(thm)],[c_32491]) ).
cnf(c_32492,plain,
join(join(A,meet(B,C)),meet(C,join(B,A))) = join(join(A,meet(B,C)),meet(C,join(B,meet(C,A)))),
inference(paramod,[status(thm)],[c_46,c_57]) ).
cnf(c_32493,plain,
join(A,join(meet(B,C),meet(C,join(B,A)))) = join(join(A,meet(B,C)),meet(C,join(B,meet(C,A)))),
inference(paramod,[status(thm)],[c_8,c_32492]) ).
cnf(c_32494,plain,
join(A,join(meet(B,C),meet(C,join(B,A)))) = join(A,join(meet(B,C),meet(C,join(B,meet(C,A))))),
inference(paramod,[status(thm)],[c_8,c_32493]) ).
cnf(c_749,plain,
join(A,join(meet(B,C),meet(C,join(B,meet(C,A))))) = join(A,join(meet(B,C),meet(C,join(B,A)))),
inference(copy,[status(thm)],[c_32494]) ).
cnf(c_32495,plain,
meet(meet(A,B),join(C,meet(B,A))) = meet(A,B),
inference(paramod,[status(thm)],[c_178,c_73]) ).
cnf(c_936,plain,
meet(A,meet(B,join(C,meet(B,A)))) = meet(A,B),
inference(paramod,[status(thm)],[c_7,c_32495]) ).
cnf(c_32496,plain,
meet(meet(A,B),complement(join(C,meet(B,A)))) = zero,
inference(paramod,[status(thm)],[c_178,c_152]) ).
cnf(c_939,plain,
meet(A,meet(B,complement(join(C,meet(B,A))))) = zero,
inference(paramod,[status(thm)],[c_7,c_32496]) ).
cnf(c_32497,plain,
join(zero,meet(A,join(complement(A),meet(A,complement(join(A,B)))))) = meet(A,join(complement(A),complement(join(A,B)))),
inference(paramod,[status(thm)],[c_135,c_53]) ).
cnf(c_32498,plain,
join(zero,meet(A,join(complement(A),zero))) = meet(A,join(complement(A),complement(join(A,B)))),
inference(paramod,[status(thm)],[c_135,c_32497]) ).
cnf(c_32499,plain,
join(zero,meet(A,join(zero,complement(A)))) = meet(A,join(complement(A),complement(join(A,B)))),
inference(paramod,[status(thm)],[c_6,c_32498]) ).
cnf(c_32500,plain,
join(zero,meet(A,complement(A))) = meet(A,join(complement(A),complement(join(A,B)))),
inference(paramod,[status(thm)],[c_67,c_32499]) ).
cnf(c_32501,plain,
join(zero,zero) = meet(A,join(complement(A),complement(join(A,B)))),
inference(paramod,[status(thm)],[c_10,c_32500]) ).
cnf(c_32502,plain,
zero = meet(A,join(complement(A),complement(join(A,B)))),
inference(paramod,[status(thm)],[c_2,c_32501]) ).
cnf(c_1612,plain,
meet(A,join(complement(A),complement(join(A,B)))) = zero,
inference(copy,[status(thm)],[c_32502]) ).
cnf(c_32503,plain,
join(zero,meet(A,join(complement(A),meet(A,meet(B,complement(meet(A,B))))))) = meet(A,join(complement(A),meet(B,complement(meet(A,B))))),
inference(paramod,[status(thm)],[c_39,c_53]) ).
cnf(c_32504,plain,
join(zero,meet(A,join(complement(A),zero))) = meet(A,join(complement(A),meet(B,complement(meet(A,B))))),
inference(paramod,[status(thm)],[c_39,c_32503]) ).
cnf(c_32505,plain,
join(zero,meet(A,join(zero,complement(A)))) = meet(A,join(complement(A),meet(B,complement(meet(A,B))))),
inference(paramod,[status(thm)],[c_6,c_32504]) ).
cnf(c_32506,plain,
join(zero,meet(A,complement(A))) = meet(A,join(complement(A),meet(B,complement(meet(A,B))))),
inference(paramod,[status(thm)],[c_67,c_32505]) ).
cnf(c_32507,plain,
join(zero,zero) = meet(A,join(complement(A),meet(B,complement(meet(A,B))))),
inference(paramod,[status(thm)],[c_10,c_32506]) ).
cnf(c_32508,plain,
zero = meet(A,join(complement(A),meet(B,complement(meet(A,B))))),
inference(paramod,[status(thm)],[c_2,c_32507]) ).
cnf(c_1614,plain,
meet(A,join(complement(A),meet(B,complement(meet(A,B))))) = zero,
inference(copy,[status(thm)],[c_32508]) ).
cnf(c_32509,plain,
( complement(A) = join(complement(A),complement(join(A,B)))
| join(A,join(complement(A),complement(join(A,B)))) != one ),
inference(resolve,[status(thm)],[c_11,c_1612]) ).
cnf(c_32510,plain,
complement(A) = join(complement(A),complement(join(A,B))),
inference(resolve,[status(thm)],[c_32509,c_66]) ).
cnf(c_1657,plain,
join(complement(A),complement(join(A,B))) = complement(A),
inference(copy,[status(thm)],[c_32510]) ).
cnf(c_1670,plain,
join(complement(A),complement(join(B,A))) = complement(A),
inference(paramod,[status(thm)],[c_6,c_1657]) ).
cnf(c_32511,plain,
meet(complement(join(A,B)),complement(A)) = complement(join(A,B)),
inference(paramod,[status(thm)],[c_1657,c_17]) ).
cnf(c_1674,plain,
meet(complement(A),complement(join(A,B))) = complement(join(A,B)),
inference(paramod,[status(thm)],[c_5,c_32511]) ).
cnf(c_32512,plain,
join(complement(meet(A,B)),complement(A)) = complement(meet(A,B)),
inference(paramod,[status(thm)],[c_4,c_1670]) ).
cnf(c_1837,plain,
join(complement(A),complement(meet(A,B))) = complement(meet(A,B)),
inference(paramod,[status(thm)],[c_6,c_32512]) ).
cnf(c_2449,plain,
join(meet(join(A,B),C),complement(meet(C,A))) = one,
inference(paramod,[status(thm)],[c_140,c_220]) ).
cnf(c_32513,plain,
join(zero,meet(complement(A),join(meet(complement(complement(A)),B),meet(complement(A),meet(C,A))))) = meet(complement(A),join(meet(complement(complement(A)),B),meet(C,A))),
inference(paramod,[status(thm)],[c_436,c_96]) ).
cnf(c_32514,plain,
join(zero,meet(complement(A),join(meet(A,B),meet(complement(A),meet(C,A))))) = meet(complement(A),join(meet(complement(complement(A)),B),meet(C,A))),
inference(paramod,[status(thm)],[c_403,c_32513]) ).
cnf(c_32515,plain,
join(zero,meet(complement(A),join(meet(A,B),zero))) = meet(complement(A),join(meet(complement(complement(A)),B),meet(C,A))),
inference(paramod,[status(thm)],[c_436,c_32514]) ).
cnf(c_32516,plain,
join(zero,meet(complement(A),join(zero,meet(A,B)))) = meet(complement(A),join(meet(complement(complement(A)),B),meet(C,A))),
inference(paramod,[status(thm)],[c_6,c_32515]) ).
cnf(c_32517,plain,
join(zero,meet(complement(A),meet(A,B))) = meet(complement(A),join(meet(complement(complement(A)),B),meet(C,A))),
inference(paramod,[status(thm)],[c_67,c_32516]) ).
cnf(c_32518,plain,
join(zero,meet(A,meet(complement(A),B))) = meet(complement(A),join(meet(complement(complement(A)),B),meet(C,A))),
inference(paramod,[status(thm)],[c_25,c_32517]) ).
cnf(c_32519,plain,
join(zero,zero) = meet(complement(A),join(meet(complement(complement(A)),B),meet(C,A))),
inference(paramod,[status(thm)],[c_77,c_32518]) ).
cnf(c_32520,plain,
zero = meet(complement(A),join(meet(complement(complement(A)),B),meet(C,A))),
inference(paramod,[status(thm)],[c_2,c_32519]) ).
cnf(c_32521,plain,
zero = meet(complement(A),join(meet(A,B),meet(C,A))),
inference(paramod,[status(thm)],[c_403,c_32520]) ).
cnf(c_2734,plain,
meet(complement(A),join(meet(A,B),meet(C,A))) = zero,
inference(copy,[status(thm)],[c_32521]) ).
cnf(c_32522,plain,
join(A,meet(join(B,A),join(meet(A,join(B,A)),C))) = meet(join(B,A),join(meet(A,join(B,A)),C)),
inference(paramod,[status(thm)],[c_17,c_110]) ).
cnf(c_32523,plain,
join(A,meet(join(B,A),join(A,C))) = meet(join(B,A),join(meet(A,join(B,A)),C)),
inference(paramod,[status(thm)],[c_17,c_32522]) ).
cnf(c_4233,plain,
join(A,meet(join(B,A),join(A,C))) = meet(join(B,A),join(A,C)),
inference(paramod,[status(thm)],[c_17,c_32523]) ).
cnf(c_6390,plain,
meet(A,complement(join(B,meet(A,complement(B))))) = zero,
inference(paramod,[status(thm)],[c_1674,c_151]) ).
cnf(c_6406,plain,
meet(A,complement(join(B,meet(complement(B),A)))) = zero,
inference(paramod,[status(thm)],[c_1674,c_939]) ).
cnf(c_6418,plain,
meet(A,complement(join(complement(B),meet(A,B)))) = zero,
inference(paramod,[status(thm)],[c_403,c_6390]) ).
cnf(c_6565,plain,
meet(A,complement(join(complement(B),meet(B,A)))) = zero,
inference(paramod,[status(thm)],[c_403,c_6406]) ).
cnf(c_7389,plain,
meet(complement(A),meet(B,complement(meet(A,C)))) = meet(complement(A),B),
inference(paramod,[status(thm)],[c_1837,c_133]) ).
cnf(c_8330,plain,
join(meet(A,B),meet(B,join(A,C))) = meet(join(A,C),B),
inference(paramod,[status(thm)],[c_5,c_139]) ).
cnf(c_32524,plain,
join(A,meet(join(B,meet(C,A)),C)) = join(A,join(meet(B,C),meet(C,join(B,A)))),
inference(paramod,[status(thm)],[c_8330,c_749]) ).
cnf(c_32525,plain,
join(A,meet(C,join(B,meet(C,A)))) = join(A,join(meet(B,C),meet(C,join(B,A)))),
inference(paramod,[status(thm)],[c_5,c_32524]) ).
cnf(c_8419,plain,
join(A,meet(B,join(C,meet(B,A)))) = join(A,meet(join(C,A),B)),
inference(paramod,[status(thm)],[c_8330,c_32525]) ).
cnf(c_32526,plain,
join(complement(meet(A,B)),join(C,join(meet(join(B,D),A),complement(one)))) = one,
inference(paramod,[status(thm)],[c_2449,c_345]) ).
cnf(c_32527,plain,
join(complement(meet(A,B)),join(C,join(meet(join(B,D),A),zero))) = one,
inference(paramod,[status(thm)],[c_70,c_32526]) ).
cnf(c_32528,plain,
join(complement(meet(A,B)),join(C,join(zero,meet(join(B,D),A)))) = one,
inference(paramod,[status(thm)],[c_6,c_32527]) ).
cnf(c_10788,plain,
join(complement(meet(A,B)),join(C,meet(join(B,D),A))) = one,
inference(paramod,[status(thm)],[c_67,c_32528]) ).
cnf(c_11434,plain,
meet(complement(A),join(meet(A,B),meet(A,C))) = zero,
inference(paramod,[status(thm)],[c_5,c_2734]) ).
cnf(c_18370,plain,
join(complement(A),meet(B,complement(meet(A,B)))) = complement(A),
inference(resolve,[status(thm)],[c_92,c_1614]) ).
cnf(c_32529,plain,
meet(meet(A,complement(meet(B,A))),complement(B)) = meet(A,complement(meet(B,A))),
inference(paramod,[status(thm)],[c_18370,c_17]) ).
cnf(c_32530,plain,
meet(complement(B),meet(A,complement(meet(B,A)))) = meet(A,complement(meet(B,A))),
inference(paramod,[status(thm)],[c_5,c_32529]) ).
cnf(c_32531,plain,
meet(complement(B),A) = meet(A,complement(meet(B,A))),
inference(paramod,[status(thm)],[c_7389,c_32530]) ).
cnf(c_18438,plain,
meet(A,complement(meet(B,A))) = meet(complement(B),A),
inference(copy,[status(thm)],[c_32531]) ).
cnf(c_18526,plain,
meet(A,complement(meet(A,B))) = meet(complement(B),A),
inference(paramod,[status(thm)],[c_5,c_18438]) ).
cnf(c_32532,plain,
meet(join(meet(A,B),meet(A,C)),complement(zero)) = meet(complement(complement(A)),join(meet(A,B),meet(A,C))),
inference(paramod,[status(thm)],[c_11434,c_18438]) ).
cnf(c_32533,plain,
meet(join(meet(A,B),meet(A,C)),one) = meet(complement(complement(A)),join(meet(A,B),meet(A,C))),
inference(paramod,[status(thm)],[c_78,c_32532]) ).
cnf(c_32534,plain,
meet(one,join(meet(A,B),meet(A,C))) = meet(complement(complement(A)),join(meet(A,B),meet(A,C))),
inference(paramod,[status(thm)],[c_5,c_32533]) ).
cnf(c_32535,plain,
join(meet(A,B),meet(A,C)) = meet(complement(complement(A)),join(meet(A,B),meet(A,C))),
inference(paramod,[status(thm)],[c_62,c_32534]) ).
cnf(c_32536,plain,
join(meet(A,B),meet(A,C)) = meet(A,join(meet(A,B),meet(A,C))),
inference(paramod,[status(thm)],[c_403,c_32535]) ).
cnf(c_18645,plain,
meet(A,join(meet(A,B),meet(A,C))) = join(meet(A,B),meet(A,C)),
inference(copy,[status(thm)],[c_32536]) ).
cnf(c_32537,plain,
meet(A,complement(zero)) = meet(complement(complement(join(B,meet(A,complement(B))))),A),
inference(paramod,[status(thm)],[c_6390,c_18526]) ).
cnf(c_32538,plain,
meet(A,one) = meet(complement(complement(join(B,meet(A,complement(B))))),A),
inference(paramod,[status(thm)],[c_78,c_32537]) ).
cnf(c_32539,plain,
A = meet(complement(complement(join(B,meet(A,complement(B))))),A),
inference(paramod,[status(thm)],[c_34,c_32538]) ).
cnf(c_32540,plain,
A = meet(join(B,meet(A,complement(B))),A),
inference(paramod,[status(thm)],[c_403,c_32539]) ).
cnf(c_32541,plain,
A = meet(A,join(B,meet(A,complement(B)))),
inference(paramod,[status(thm)],[c_5,c_32540]) ).
cnf(c_18824,plain,
meet(A,join(B,meet(A,complement(B)))) = A,
inference(copy,[status(thm)],[c_32541]) ).
cnf(c_32542,plain,
meet(A,complement(zero)) = meet(complement(complement(join(B,meet(complement(B),A)))),A),
inference(paramod,[status(thm)],[c_6406,c_18526]) ).
cnf(c_32543,plain,
meet(A,one) = meet(complement(complement(join(B,meet(complement(B),A)))),A),
inference(paramod,[status(thm)],[c_78,c_32542]) ).
cnf(c_32544,plain,
A = meet(complement(complement(join(B,meet(complement(B),A)))),A),
inference(paramod,[status(thm)],[c_34,c_32543]) ).
cnf(c_32545,plain,
A = meet(join(B,meet(complement(B),A)),A),
inference(paramod,[status(thm)],[c_403,c_32544]) ).
cnf(c_32546,plain,
A = meet(A,join(B,meet(complement(B),A))),
inference(paramod,[status(thm)],[c_5,c_32545]) ).
cnf(c_18827,plain,
meet(A,join(B,meet(complement(B),A))) = A,
inference(copy,[status(thm)],[c_32546]) ).
cnf(c_32547,plain,
meet(A,complement(zero)) = meet(complement(complement(join(complement(B),meet(A,B)))),A),
inference(paramod,[status(thm)],[c_6418,c_18526]) ).
cnf(c_32548,plain,
meet(A,one) = meet(complement(complement(join(complement(B),meet(A,B)))),A),
inference(paramod,[status(thm)],[c_78,c_32547]) ).
cnf(c_32549,plain,
A = meet(complement(complement(join(complement(B),meet(A,B)))),A),
inference(paramod,[status(thm)],[c_34,c_32548]) ).
cnf(c_32550,plain,
A = meet(join(complement(B),meet(A,B)),A),
inference(paramod,[status(thm)],[c_403,c_32549]) ).
cnf(c_32551,plain,
A = meet(A,join(complement(B),meet(A,B))),
inference(paramod,[status(thm)],[c_5,c_32550]) ).
cnf(c_18828,plain,
meet(A,join(complement(B),meet(A,B))) = A,
inference(copy,[status(thm)],[c_32551]) ).
cnf(c_32552,plain,
meet(A,complement(zero)) = meet(complement(complement(join(complement(B),meet(B,A)))),A),
inference(paramod,[status(thm)],[c_6565,c_18526]) ).
cnf(c_32553,plain,
meet(A,one) = meet(complement(complement(join(complement(B),meet(B,A)))),A),
inference(paramod,[status(thm)],[c_78,c_32552]) ).
cnf(c_32554,plain,
A = meet(complement(complement(join(complement(B),meet(B,A)))),A),
inference(paramod,[status(thm)],[c_34,c_32553]) ).
cnf(c_32555,plain,
A = meet(join(complement(B),meet(B,A)),A),
inference(paramod,[status(thm)],[c_403,c_32554]) ).
cnf(c_32556,plain,
A = meet(A,join(complement(B),meet(B,A))),
inference(paramod,[status(thm)],[c_5,c_32555]) ).
cnf(c_18830,plain,
meet(A,join(complement(B),meet(B,A))) = A,
inference(copy,[status(thm)],[c_32556]) ).
cnf(c_32557,plain,
join(join(A,meet(B,complement(A))),join(B,C)) = join(join(A,meet(B,complement(A))),C),
inference(paramod,[status(thm)],[c_18824,c_57]) ).
cnf(c_32558,plain,
join(B,join(join(A,meet(B,complement(A))),C)) = join(join(A,meet(B,complement(A))),C),
inference(paramod,[status(thm)],[c_33,c_32557]) ).
cnf(c_32559,plain,
join(B,join(A,join(meet(B,complement(A)),C))) = join(join(A,meet(B,complement(A))),C),
inference(paramod,[status(thm)],[c_8,c_32558]) ).
cnf(c_32560,plain,
join(B,join(A,C)) = join(join(A,meet(B,complement(A))),C),
inference(paramod,[status(thm)],[c_343,c_32559]) ).
cnf(c_32561,plain,
join(B,join(A,C)) = join(A,join(meet(B,complement(A)),C)),
inference(paramod,[status(thm)],[c_8,c_32560]) ).
cnf(c_19035,plain,
join(A,join(meet(B,complement(A)),C)) = join(B,join(A,C)),
inference(copy,[status(thm)],[c_32561]) ).
cnf(c_32562,plain,
join(join(A,meet(B,complement(A))),meet(C,meet(D,B))) = join(A,meet(B,complement(A))),
inference(paramod,[status(thm)],[c_18824,c_127]) ).
cnf(c_32563,plain,
join(A,join(meet(B,complement(A)),meet(C,meet(D,B)))) = join(A,meet(B,complement(A))),
inference(paramod,[status(thm)],[c_8,c_32562]) ).
cnf(c_32564,plain,
join(B,join(A,meet(C,meet(D,B)))) = join(A,meet(B,complement(A))),
inference(paramod,[status(thm)],[c_19035,c_32563]) ).
cnf(c_32565,plain,
join(A,B) = join(A,meet(B,complement(A))),
inference(paramod,[status(thm)],[c_328,c_32564]) ).
cnf(c_19037,plain,
join(A,meet(B,complement(A))) = join(A,B),
inference(copy,[status(thm)],[c_32565]) ).
cnf(c_32566,plain,
join(join(A,meet(complement(A),B)),join(B,C)) = join(join(A,meet(complement(A),B)),C),
inference(paramod,[status(thm)],[c_18827,c_57]) ).
cnf(c_32567,plain,
join(B,join(join(A,meet(complement(A),B)),C)) = join(join(A,meet(complement(A),B)),C),
inference(paramod,[status(thm)],[c_33,c_32566]) ).
cnf(c_32568,plain,
join(B,join(A,join(meet(complement(A),B),C))) = join(join(A,meet(complement(A),B)),C),
inference(paramod,[status(thm)],[c_8,c_32567]) ).
cnf(c_32569,plain,
join(A,join(B,C)) = join(join(A,meet(complement(A),B)),C),
inference(paramod,[status(thm)],[c_582,c_32568]) ).
cnf(c_32570,plain,
join(A,join(B,C)) = join(A,join(meet(complement(A),B),C)),
inference(paramod,[status(thm)],[c_8,c_32569]) ).
cnf(c_19064,plain,
join(A,join(meet(complement(A),B),C)) = join(A,join(B,C)),
inference(copy,[status(thm)],[c_32570]) ).
cnf(c_32571,plain,
join(join(A,meet(complement(A),B)),meet(C,meet(D,B))) = join(A,meet(complement(A),B)),
inference(paramod,[status(thm)],[c_18827,c_127]) ).
cnf(c_32572,plain,
join(A,join(meet(complement(A),B),meet(C,meet(D,B)))) = join(A,meet(complement(A),B)),
inference(paramod,[status(thm)],[c_8,c_32571]) ).
cnf(c_32573,plain,
join(A,join(B,meet(C,meet(D,B)))) = join(A,meet(complement(A),B)),
inference(paramod,[status(thm)],[c_19064,c_32572]) ).
cnf(c_32574,plain,
join(A,B) = join(A,meet(complement(A),B)),
inference(paramod,[status(thm)],[c_56,c_32573]) ).
cnf(c_19066,plain,
join(A,meet(complement(A),B)) = join(A,B),
inference(copy,[status(thm)],[c_32574]) ).
cnf(c_32575,plain,
join(complement(A),join(meet(B,A),B)) = join(complement(A),meet(B,A)),
inference(paramod,[status(thm)],[c_18828,c_58]) ).
cnf(c_32576,plain,
join(complement(A),join(B,meet(B,A))) = join(complement(A),meet(B,A)),
inference(paramod,[status(thm)],[c_6,c_32575]) ).
cnf(c_32577,plain,
join(complement(A),B) = join(complement(A),meet(B,A)),
inference(paramod,[status(thm)],[c_4,c_32576]) ).
cnf(c_19102,plain,
join(complement(A),meet(B,A)) = join(complement(A),B),
inference(copy,[status(thm)],[c_32577]) ).
cnf(c_32578,plain,
join(join(complement(A),meet(A,B)),join(B,C)) = join(join(complement(A),meet(A,B)),C),
inference(paramod,[status(thm)],[c_18830,c_57]) ).
cnf(c_32579,plain,
join(B,join(join(complement(A),meet(A,B)),C)) = join(join(complement(A),meet(A,B)),C),
inference(paramod,[status(thm)],[c_33,c_32578]) ).
cnf(c_32580,plain,
join(B,join(complement(A),join(meet(A,B),C))) = join(join(complement(A),meet(A,B)),C),
inference(paramod,[status(thm)],[c_8,c_32579]) ).
cnf(c_32581,plain,
join(complement(A),join(B,C)) = join(join(complement(A),meet(A,B)),C),
inference(paramod,[status(thm)],[c_582,c_32580]) ).
cnf(c_32582,plain,
join(complement(A),join(B,C)) = join(complement(A),join(meet(A,B),C)),
inference(paramod,[status(thm)],[c_8,c_32581]) ).
cnf(c_19157,plain,
join(complement(A),join(meet(A,B),C)) = join(complement(A),join(B,C)),
inference(copy,[status(thm)],[c_32582]) ).
cnf(c_32583,plain,
join(join(complement(A),meet(A,B)),meet(C,meet(D,B))) = join(complement(A),meet(A,B)),
inference(paramod,[status(thm)],[c_18830,c_127]) ).
cnf(c_32584,plain,
join(complement(A),join(meet(A,B),meet(C,meet(D,B)))) = join(complement(A),meet(A,B)),
inference(paramod,[status(thm)],[c_8,c_32583]) ).
cnf(c_32585,plain,
join(complement(A),join(B,meet(C,meet(D,B)))) = join(complement(A),meet(A,B)),
inference(paramod,[status(thm)],[c_19157,c_32584]) ).
cnf(c_32586,plain,
join(complement(A),B) = join(complement(A),meet(A,B)),
inference(paramod,[status(thm)],[c_56,c_32585]) ).
cnf(c_19159,plain,
join(complement(A),meet(A,B)) = join(complement(A),B),
inference(copy,[status(thm)],[c_32586]) ).
cnf(c_32587,plain,
join(complement(A),meet(complement(meet(A,B)),complement(complement(A)))) = complement(meet(A,B)),
inference(paramod,[status(thm)],[c_1837,c_19037]) ).
cnf(c_32588,plain,
join(complement(A),meet(complement(meet(A,B)),A)) = complement(meet(A,B)),
inference(paramod,[status(thm)],[c_403,c_32587]) ).
cnf(c_32589,plain,
join(complement(A),meet(A,complement(meet(A,B)))) = complement(meet(A,B)),
inference(paramod,[status(thm)],[c_5,c_32588]) ).
cnf(c_32590,plain,
join(complement(A),meet(complement(B),A)) = complement(meet(A,B)),
inference(paramod,[status(thm)],[c_18526,c_32589]) ).
cnf(c_32591,plain,
join(complement(A),complement(B)) = complement(meet(A,B)),
inference(paramod,[status(thm)],[c_19102,c_32590]) ).
cnf(c_19237,plain,
complement(meet(A,B)) = join(complement(A),complement(B)),
inference(copy,[status(thm)],[c_32591]) ).
cnf(c_32592,plain,
join(join(complement(A),complement(B)),join(C,meet(join(B,D),A))) = one,
inference(paramod,[status(thm)],[c_19237,c_10788]) ).
cnf(c_21119,plain,
join(complement(A),join(complement(B),join(C,meet(join(B,D),A)))) = one,
inference(paramod,[status(thm)],[c_8,c_32592]) ).
cnf(c_23142,plain,
complement(join(complement(A),complement(B))) = meet(A,B),
inference(paramod,[status(thm)],[c_19237,c_403]) ).
cnf(c_23308,plain,
complement(join(A,complement(B))) = meet(complement(A),B),
inference(paramod,[status(thm)],[c_403,c_23142]) ).
cnf(c_23653,plain,
complement(join(A,B)) = meet(complement(A),complement(B)),
inference(paramod,[status(thm)],[c_403,c_23308]) ).
cnf(c_32593,plain,
join(complement(A),meet(A,B)) = join(complement(A),meet(B,join(C,meet(B,A)))),
inference(paramod,[status(thm)],[c_936,c_19159]) ).
cnf(c_32594,plain,
join(complement(A),B) = join(complement(A),meet(B,join(C,meet(B,A)))),
inference(paramod,[status(thm)],[c_19159,c_32593]) ).
cnf(c_28148,plain,
join(complement(A),meet(B,join(C,meet(B,A)))) = join(complement(A),B),
inference(copy,[status(thm)],[c_32594]) ).
cnf(c_32595,plain,
meet(complement(join(A,B)),join(A,B)) = zero,
inference(paramod,[status(thm)],[c_241,c_77]) ).
cnf(c_32596,plain,
meet(meet(complement(A),complement(B)),join(A,B)) = zero,
inference(paramod,[status(thm)],[c_23653,c_32595]) ).
cnf(c_28427,plain,
meet(complement(A),meet(complement(B),join(A,B))) = zero,
inference(paramod,[status(thm)],[c_7,c_32596]) ).
cnf(c_32597,plain,
join(A,zero) = join(A,meet(complement(B),join(A,B))),
inference(paramod,[status(thm)],[c_28427,c_19066]) ).
cnf(c_32598,plain,
A = join(A,meet(complement(B),join(A,B))),
inference(paramod,[status(thm)],[c_37,c_32597]) ).
cnf(c_29068,plain,
join(A,meet(complement(B),join(A,B))) = A,
inference(copy,[status(thm)],[c_32598]) ).
cnf(c_32599,plain,
join(A,meet(complement(meet(B,complement(A))),join(A,B))) = A,
inference(paramod,[status(thm)],[c_19037,c_29068]) ).
cnf(c_32600,plain,
join(A,meet(join(complement(B),complement(complement(A))),join(A,B))) = A,
inference(paramod,[status(thm)],[c_19237,c_32599]) ).
cnf(c_32601,plain,
join(A,meet(join(complement(B),A),join(A,B))) = A,
inference(paramod,[status(thm)],[c_403,c_32600]) ).
cnf(c_29124,plain,
meet(join(complement(A),B),join(B,A)) = B,
inference(paramod,[status(thm)],[c_4233,c_32601]) ).
cnf(c_32602,plain,
meet(join(complement(A),B),join(join(meet(C,complement(A)),B),A)) = join(meet(C,complement(A)),B),
inference(paramod,[status(thm)],[c_57,c_29124]) ).
cnf(c_32603,plain,
meet(join(complement(A),B),join(A,join(meet(C,complement(A)),B))) = join(meet(C,complement(A)),B),
inference(paramod,[status(thm)],[c_6,c_32602]) ).
cnf(c_32604,plain,
meet(join(complement(A),B),join(C,join(A,B))) = join(meet(C,complement(A)),B),
inference(paramod,[status(thm)],[c_19035,c_32603]) ).
cnf(c_29437,plain,
join(meet(A,complement(B)),C) = meet(join(complement(B),C),join(A,join(B,C))),
inference(copy,[status(thm)],[c_32604]) ).
cnf(c_32605,plain,
meet(join(complement(meet(A,join(meet(A,B),C))),meet(A,join(B,meet(A,C)))),meet(A,join(B,C))) = meet(A,join(B,meet(A,C))),
inference(paramod,[status(thm)],[c_48,c_29124]) ).
cnf(c_32606,plain,
meet(join(join(complement(A),complement(join(meet(A,B),C))),meet(A,join(B,meet(A,C)))),meet(A,join(B,C))) = meet(A,join(B,meet(A,C))),
inference(paramod,[status(thm)],[c_19237,c_32605]) ).
cnf(c_32607,plain,
meet(join(join(complement(A),meet(complement(meet(A,B)),complement(C))),meet(A,join(B,meet(A,C)))),meet(A,join(B,C))) = meet(A,join(B,meet(A,C))),
inference(paramod,[status(thm)],[c_23653,c_32606]) ).
cnf(c_32608,plain,
meet(join(join(complement(A),meet(join(complement(A),complement(B)),complement(C))),meet(A,join(B,meet(A,C)))),meet(A,join(B,C))) = meet(A,join(B,meet(A,C))),
inference(paramod,[status(thm)],[c_19237,c_32607]) ).
cnf(c_32609,plain,
meet(join(complement(A),join(meet(join(complement(A),complement(B)),complement(C)),meet(A,join(B,meet(A,C))))),meet(A,join(B,C))) = meet(A,join(B,meet(A,C))),
inference(paramod,[status(thm)],[c_8,c_32608]) ).
cnf(c_32610,plain,
meet(join(complement(A),meet(join(complement(C),meet(A,join(B,meet(A,C)))),join(join(complement(A),complement(B)),join(C,meet(A,join(B,meet(A,C))))))),meet(A,join(B,C))) = meet(A,join(B,meet(A,C))),
inference(paramod,[status(thm)],[c_29437,c_32609]) ).
cnf(c_32611,plain,
meet(join(complement(A),meet(join(complement(C),A),join(join(complement(A),complement(B)),join(C,meet(A,join(B,meet(A,C))))))),meet(A,join(B,C))) = meet(A,join(B,meet(A,C))),
inference(paramod,[status(thm)],[c_28148,c_32610]) ).
cnf(c_32612,plain,
meet(join(complement(A),meet(join(complement(C),A),join(join(complement(A),complement(B)),join(C,meet(join(B,C),A))))),meet(A,join(B,C))) = meet(A,join(B,meet(A,C))),
inference(paramod,[status(thm)],[c_8419,c_32611]) ).
cnf(c_32613,plain,
meet(join(complement(A),meet(join(complement(C),A),join(complement(A),join(complement(B),join(C,meet(join(B,C),A)))))),meet(A,join(B,C))) = meet(A,join(B,meet(A,C))),
inference(paramod,[status(thm)],[c_8,c_32612]) ).
cnf(c_32614,plain,
meet(join(complement(A),meet(join(complement(C),A),one)),meet(A,join(B,C))) = meet(A,join(B,meet(A,C))),
inference(paramod,[status(thm)],[c_21119,c_32613]) ).
cnf(c_32615,plain,
meet(join(complement(A),meet(one,join(complement(C),A))),meet(A,join(B,C))) = meet(A,join(B,meet(A,C))),
inference(paramod,[status(thm)],[c_5,c_32614]) ).
cnf(c_32616,plain,
meet(join(complement(A),join(complement(C),A)),meet(A,join(B,C))) = meet(A,join(B,meet(A,C))),
inference(paramod,[status(thm)],[c_62,c_32615]) ).
cnf(c_32617,plain,
meet(one,meet(A,join(B,C))) = meet(A,join(B,meet(A,C))),
inference(paramod,[status(thm)],[c_195,c_32616]) ).
cnf(c_32618,plain,
meet(A,join(B,C)) = meet(A,join(B,meet(A,C))),
inference(paramod,[status(thm)],[c_62,c_32617]) ).
cnf(c_29443,plain,
meet(A,join(B,meet(A,C))) = meet(A,join(B,C)),
inference(copy,[status(thm)],[c_32618]) ).
cnf(c_32619,plain,
meet(A,join(meet(A,B),C)) = join(meet(A,B),meet(A,C)),
inference(paramod,[status(thm)],[c_29443,c_18645]) ).
cnf(c_31069,plain,
join(meet(A,B),meet(A,C)) = meet(A,join(meet(A,B),C)),
inference(copy,[status(thm)],[c_32619]) ).
cnf(c_32620,plain,
meet(a,join(meet(a,b),c)) != meet(a,join(b,c)),
inference(paramod,[status(thm)],[c_31069,c_15]) ).
cnf(c_32621,plain,
meet(a,join(c,meet(a,b))) != meet(a,join(b,c)),
inference(paramod,[status(thm)],[c_6,c_32620]) ).
cnf(c_32622,plain,
meet(a,join(c,b)) != meet(a,join(b,c)),
inference(paramod,[status(thm)],[c_29443,c_32621]) ).
cnf(c_32623,plain,
meet(a,join(b,c)) != meet(a,join(b,c)),
inference(paramod,[status(thm)],[c_6,c_32622]) ).
cnf(c_32447,plain,
$false,
inference(copy,[status(thm)],[c_32623]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LAT211-1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n009.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Fri Sep 25 20:15:59 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.08/0.35 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.08/0.35 % Process 2439052 was started by sandbox on n009,
% 0.08/0.35 % Fri Sep 25 20:15:59 2026
% 0.08/0.35 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.13/0.36
% 0.13/0.36 % From the command line: assign(max_seconds, 300).
% 153.24/20.78
% 153.24/20.78 % given #500 (T,wt=10): 23308 complement(join(A,complement(B))) = meet(complement(A),B). [para(403(a,1),23142(a,1,1,1))].
% 153.24/20.78
% 153.24/20.78 % SZS status Unsatisfiable for theBenchmark
% 153.24/20.78
% 153.24/20.78 % Proof 1 at 16.93 (+ 3.31) seconds.
% 153.24/20.78 % Length of proof is 124.
% 153.24/20.78 % Level of proof is 25.
% 153.24/20.78 % Maximum clause weight is 27.000.
% 153.24/20.78 % Given clauses 541.
% 153.24/20.78
% 153.24/20.78 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------