%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : LAT209-1 : TPTP v9.3.1. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n001.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sun Sep 27 07:49:49 AM UTC 2026
% Result : Unsatisfiable 156.76s 21.42s
% Output : CNFRefutation 156.76s
% Verified :
% SZS Type : Refutation
% Derivation depth : 74
% Number of leaves : 13
% Syntax : Number of formulae : 275 ( 263 unt; 0 def)
% Number of atoms : 295 ( 294 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 47 ( 27 ~; 20 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 1 avg)
% Maximal term depth : 10 ( 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 : 628 ( 79 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_H64,axiom,
! [VAR_0,VAR_1,VAR_2] : meet(VAR_0,join(VAR_1,VAR_2)) = meet(VAR_0,join(VAR_1,meet(VAR_0,join(VAR_2,meet(VAR_0,join(VAR_1,meet(VAR_0,VAR_2))))))),
file('theBenchmark.p',equation_H64) ).
cnf(c_12,plain,
meet(A,join(B,C)) = meet(A,join(B,meet(A,join(C,meet(A,join(B,meet(A,C))))))),
inference(clausify,[status(thm)],[equation_H64]) ).
cnf(c_13,plain,
meet(A,join(B,meet(A,join(C,meet(A,join(B,meet(A,C))))))) = meet(A,join(B,C)),
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_31238,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_31238]) ).
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_31239,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_31239]) ).
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_31240,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_31240]) ).
cnf(c_31241,plain,
join(A,B) = join(A,join(A,B)),
inference(paramod,[status(thm)],[c_2,c_8]) ).
cnf(c_27,plain,
join(A,join(A,B)) = join(A,B),
inference(copy,[status(thm)],[c_31241]) ).
cnf(c_31242,plain,
join(join(A,B),B) = join(A,B),
inference(paramod,[status(thm)],[c_2,c_8]) ).
cnf(c_28,plain,
join(A,join(B,A)) = join(B,A),
inference(paramod,[status(thm)],[c_6,c_31242]) ).
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_31243,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_31243]) ).
cnf(c_31244,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_31244]) ).
cnf(c_34,plain,
meet(A,one) = A,
inference(paramod,[status(thm)],[c_9,c_3]) ).
cnf(c_31245,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_31245]) ).
cnf(c_37,plain,
join(A,zero) = A,
inference(paramod,[status(thm)],[c_10,c_4]) ).
cnf(c_31246,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_31246]) ).
cnf(c_31247,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_31247]) ).
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_31248,plain,
meet(A,join(join(B,C),meet(A,join(D,meet(A,join(B,join(C,meet(A,D)))))))) = meet(A,join(join(B,C),D)),
inference(paramod,[status(thm)],[c_8,c_13]) ).
cnf(c_31249,plain,
meet(A,join(B,join(C,meet(A,join(D,meet(A,join(B,join(C,meet(A,D))))))))) = meet(A,join(join(B,C),D)),
inference(paramod,[status(thm)],[c_8,c_31248]) ).
cnf(c_49,plain,
meet(A,join(B,join(C,meet(A,join(D,meet(A,join(B,join(C,meet(A,D))))))))) = meet(A,join(B,join(C,D))),
inference(paramod,[status(thm)],[c_8,c_31249]) ).
cnf(c_50,plain,
meet(A,join(B,meet(A,join(C,join(D,meet(A,join(B,meet(A,join(C,D))))))))) = meet(A,join(B,join(C,D))),
inference(paramod,[status(thm)],[c_8,c_13]) ).
cnf(c_31250,plain,
meet(A,join(B,meet(A,join(complement(A),meet(A,join(B,zero)))))) = meet(A,join(B,complement(A))),
inference(paramod,[status(thm)],[c_10,c_13]) ).
cnf(c_51,plain,
meet(A,join(B,meet(A,join(complement(A),meet(A,B))))) = meet(A,join(B,complement(A))),
inference(paramod,[status(thm)],[c_37,c_31250]) ).
cnf(c_55,plain,
join(A,meet(B,meet(C,A))) = A,
inference(paramod,[status(thm)],[c_7,c_16]) ).
cnf(c_31251,plain,
join(A,B) = join(A,join(meet(C,A),B)),
inference(paramod,[status(thm)],[c_16,c_8]) ).
cnf(c_56,plain,
join(A,join(meet(B,A),C)) = join(A,C),
inference(copy,[status(thm)],[c_31251]) ).
cnf(c_31252,plain,
join(A,B) = join(A,join(B,meet(C,join(A,B)))),
inference(paramod,[status(thm)],[c_16,c_8]) ).
cnf(c_57,plain,
join(A,join(B,meet(C,join(A,B)))) = join(A,B),
inference(copy,[status(thm)],[c_31252]) ).
cnf(c_64,plain,
join(one,A) = one,
inference(paramod,[status(thm)],[c_34,c_16]) ).
cnf(c_65,plain,
join(A,join(complement(A),B)) = one,
inference(paramod,[status(thm)],[c_64,c_35]) ).
cnf(c_31253,plain,
A = join(zero,A),
inference(paramod,[status(thm)],[c_37,c_6]) ).
cnf(c_66,plain,
join(zero,A) = A,
inference(copy,[status(thm)],[c_31253]) ).
cnf(c_72,plain,
meet(A,join(B,join(C,A))) = A,
inference(paramod,[status(thm)],[c_8,c_17]) ).
cnf(c_73,plain,
meet(zero,A) = zero,
inference(paramod,[status(thm)],[c_37,c_17]) ).
cnf(c_75,plain,
meet(A,meet(complement(A),B)) = zero,
inference(paramod,[status(thm)],[c_73,c_38]) ).
cnf(c_31254,plain,
( complement(zero) = one
| join(zero,one) != one ),
inference(resolve,[status(thm)],[c_11,c_34]) ).
cnf(c_76,plain,
complement(zero) = one,
inference(resolve,[status(thm)],[c_31254,c_66]) ).
cnf(c_77,plain,
meet(A,zero) = zero,
inference(paramod,[status(thm)],[c_66,c_16]) ).
cnf(c_31255,plain,
( complement(A) = join(complement(A),B)
| one != one
| meet(A,join(complement(A),B)) != zero ),
inference(paramod,[status(thm)],[c_65,c_11]) ).
cnf(c_31256,plain,
( join(complement(A),B) = complement(A)
| one != one
| meet(A,join(complement(A),B)) != zero ),
inference(copy,[status(thm)],[c_31255]) ).
cnf(c_89,plain,
( join(complement(A),B) = complement(A)
| meet(A,join(complement(A),B)) != zero ),
inference(copy,[status(thm)],[c_31256]) ).
cnf(c_31257,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_105,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_31257]) ).
cnf(c_31258,plain,
join(join(A,B),meet(C,A)) = join(A,B),
inference(paramod,[status(thm)],[c_3,c_55]) ).
cnf(c_116,plain,
join(A,join(B,meet(C,A))) = join(A,B),
inference(paramod,[status(thm)],[c_8,c_31258]) ).
cnf(c_118,plain,
join(A,meet(B,meet(C,meet(D,A)))) = A,
inference(paramod,[status(thm)],[c_7,c_55]) ).
cnf(c_125,plain,
meet(A,meet(B,join(A,C))) = meet(A,B),
inference(paramod,[status(thm)],[c_5,c_22]) ).
cnf(c_31259,plain,
meet(A,zero) = meet(A,complement(join(A,B))),
inference(paramod,[status(thm)],[c_10,c_22]) ).
cnf(c_31260,plain,
zero = meet(A,complement(join(A,B))),
inference(paramod,[status(thm)],[c_77,c_31259]) ).
cnf(c_127,plain,
meet(A,complement(join(A,B))) = zero,
inference(copy,[status(thm)],[c_31260]) ).
cnf(c_136,plain,
meet(A,complement(join(B,A))) = zero,
inference(paramod,[status(thm)],[c_6,c_127]) ).
cnf(c_31261,plain,
zero = meet(A,meet(B,complement(join(C,meet(A,B))))),
inference(paramod,[status(thm)],[c_136,c_7]) ).
cnf(c_141,plain,
meet(A,meet(B,complement(join(C,meet(A,B))))) = zero,
inference(copy,[status(thm)],[c_31261]) ).
cnf(c_142,plain,
meet(A,complement(join(B,join(C,A)))) = zero,
inference(paramod,[status(thm)],[c_8,c_136]) ).
cnf(c_31262,plain,
meet(meet(A,B),join(C,A)) = meet(A,B),
inference(paramod,[status(thm)],[c_4,c_72]) ).
cnf(c_145,plain,
meet(A,meet(B,join(C,A))) = meet(A,B),
inference(paramod,[status(thm)],[c_7,c_31262]) ).
cnf(c_158,plain,
join(meet(A,B),meet(A,meet(C,B))) = meet(A,B),
inference(paramod,[status(thm)],[c_5,c_23]) ).
cnf(c_165,plain,
join(meet(A,B),meet(B,A)) = meet(A,B),
inference(paramod,[status(thm)],[c_20,c_23]) ).
cnf(c_210,plain,
meet(join(A,B),join(B,A)) = join(A,B),
inference(paramod,[status(thm)],[c_28,c_29]) ).
cnf(c_31263,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_212,plain,
meet(join(A,B),meet(C,join(A,join(B,D)))) = meet(C,join(A,B)),
inference(copy,[status(thm)],[c_31263]) ).
cnf(c_31264,plain,
join(A,B) = join(B,join(A,meet(C,meet(D,B)))),
inference(paramod,[status(thm)],[c_55,c_33]) ).
cnf(c_271,plain,
join(A,join(B,meet(C,meet(D,A)))) = join(B,A),
inference(copy,[status(thm)],[c_31264]) ).
cnf(c_287,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_31265,plain,
( complement(complement(A)) = A
| one != one
| meet(complement(A),A) != zero ),
inference(paramod,[status(thm)],[c_9,c_42]) ).
cnf(c_31266,plain,
( complement(complement(A)) = A
| one != one
| meet(A,complement(A)) != zero ),
inference(paramod,[status(thm)],[c_5,c_31265]) ).
cnf(c_31267,plain,
( complement(complement(A)) = A
| one != one
| zero != zero ),
inference(paramod,[status(thm)],[c_10,c_31266]) ).
cnf(c_31268,plain,
( complement(complement(A)) = A
| one != one ),
inference(copy,[status(thm)],[c_31267]) ).
cnf(c_342,plain,
complement(complement(A)) = A,
inference(copy,[status(thm)],[c_31268]) ).
cnf(c_31269,plain,
join(A,join(B,C)) = join(B,join(A,join(meet(D,B),C))),
inference(paramod,[status(thm)],[c_56,c_33]) ).
cnf(c_604,plain,
join(A,join(B,join(meet(C,A),D))) = join(B,join(A,D)),
inference(copy,[status(thm)],[c_31269]) ).
cnf(c_31270,plain,
meet(meet(A,B),complement(join(C,meet(B,A)))) = zero,
inference(paramod,[status(thm)],[c_165,c_142]) ).
cnf(c_1010,plain,
meet(A,meet(B,complement(join(C,meet(B,A))))) = zero,
inference(paramod,[status(thm)],[c_7,c_31270]) ).
cnf(c_31271,plain,
meet(A,join(B,join(C,meet(A,join(B,meet(A,join(B,join(C,meet(A,B))))))))) = meet(A,join(C,B)),
inference(paramod,[status(thm)],[c_28,c_49]) ).
cnf(c_1040,plain,
meet(A,join(B,join(C,meet(A,join(B,meet(A,join(B,C))))))) = meet(A,join(C,B)),
inference(paramod,[status(thm)],[c_116,c_31271]) ).
cnf(c_31272,plain,
join(join(A,B),meet(C,join(B,A))) = join(A,B),
inference(paramod,[status(thm)],[c_210,c_55]) ).
cnf(c_1122,plain,
join(A,join(B,meet(C,join(B,A)))) = join(A,B),
inference(paramod,[status(thm)],[c_8,c_31272]) ).
cnf(c_31273,plain,
meet(A,join(B,meet(A,join(B,join(C,meet(A,join(B,meet(A,join(B,C))))))))) = meet(A,join(B,C)),
inference(paramod,[status(thm)],[c_27,c_50]) ).
cnf(c_1175,plain,
meet(A,join(B,meet(A,join(C,B)))) = meet(A,join(B,C)),
inference(paramod,[status(thm)],[c_1040,c_31273]) ).
cnf(c_31274,plain,
meet(A,join(complement(join(A,B)),meet(A,join(complement(A),zero)))) = meet(A,join(complement(join(A,B)),complement(A))),
inference(paramod,[status(thm)],[c_127,c_51]) ).
cnf(c_31275,plain,
meet(A,join(complement(join(A,B)),meet(A,join(zero,complement(A))))) = meet(A,join(complement(join(A,B)),complement(A))),
inference(paramod,[status(thm)],[c_6,c_31274]) ).
cnf(c_31276,plain,
meet(A,join(complement(join(A,B)),meet(A,complement(A)))) = meet(A,join(complement(join(A,B)),complement(A))),
inference(paramod,[status(thm)],[c_66,c_31275]) ).
cnf(c_31277,plain,
meet(A,join(complement(join(A,B)),zero)) = meet(A,join(complement(join(A,B)),complement(A))),
inference(paramod,[status(thm)],[c_10,c_31276]) ).
cnf(c_31278,plain,
meet(A,join(zero,complement(join(A,B)))) = meet(A,join(complement(join(A,B)),complement(A))),
inference(paramod,[status(thm)],[c_6,c_31277]) ).
cnf(c_31279,plain,
meet(A,complement(join(A,B))) = meet(A,join(complement(join(A,B)),complement(A))),
inference(paramod,[status(thm)],[c_66,c_31278]) ).
cnf(c_31280,plain,
zero = meet(A,join(complement(join(A,B)),complement(A))),
inference(paramod,[status(thm)],[c_127,c_31279]) ).
cnf(c_31281,plain,
zero = meet(A,join(complement(A),complement(join(A,B)))),
inference(paramod,[status(thm)],[c_6,c_31280]) ).
cnf(c_1262,plain,
meet(A,join(complement(A),complement(join(A,B)))) = zero,
inference(copy,[status(thm)],[c_31281]) ).
cnf(c_31282,plain,
meet(A,join(meet(B,complement(meet(A,B))),meet(A,join(complement(A),zero)))) = meet(A,join(meet(B,complement(meet(A,B))),complement(A))),
inference(paramod,[status(thm)],[c_39,c_51]) ).
cnf(c_31283,plain,
meet(A,join(meet(B,complement(meet(A,B))),meet(A,join(zero,complement(A))))) = meet(A,join(meet(B,complement(meet(A,B))),complement(A))),
inference(paramod,[status(thm)],[c_6,c_31282]) ).
cnf(c_31284,plain,
meet(A,join(meet(B,complement(meet(A,B))),meet(A,complement(A)))) = meet(A,join(meet(B,complement(meet(A,B))),complement(A))),
inference(paramod,[status(thm)],[c_66,c_31283]) ).
cnf(c_31285,plain,
meet(A,join(meet(B,complement(meet(A,B))),zero)) = meet(A,join(meet(B,complement(meet(A,B))),complement(A))),
inference(paramod,[status(thm)],[c_10,c_31284]) ).
cnf(c_31286,plain,
meet(A,join(zero,meet(B,complement(meet(A,B))))) = meet(A,join(meet(B,complement(meet(A,B))),complement(A))),
inference(paramod,[status(thm)],[c_6,c_31285]) ).
cnf(c_31287,plain,
meet(A,meet(B,complement(meet(A,B)))) = meet(A,join(meet(B,complement(meet(A,B))),complement(A))),
inference(paramod,[status(thm)],[c_66,c_31286]) ).
cnf(c_31288,plain,
zero = meet(A,join(meet(B,complement(meet(A,B))),complement(A))),
inference(paramod,[status(thm)],[c_39,c_31287]) ).
cnf(c_31289,plain,
zero = meet(A,join(complement(A),meet(B,complement(meet(A,B))))),
inference(paramod,[status(thm)],[c_6,c_31288]) ).
cnf(c_1264,plain,
meet(A,join(complement(A),meet(B,complement(meet(A,B))))) = zero,
inference(copy,[status(thm)],[c_31289]) ).
cnf(c_31290,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_1262]) ).
cnf(c_31291,plain,
complement(A) = join(complement(A),complement(join(A,B))),
inference(resolve,[status(thm)],[c_31290,c_65]) ).
cnf(c_1486,plain,
join(complement(A),complement(join(A,B))) = complement(A),
inference(copy,[status(thm)],[c_31291]) ).
cnf(c_1598,plain,
join(complement(A),complement(join(B,A))) = complement(A),
inference(paramod,[status(thm)],[c_6,c_1486]) ).
cnf(c_31292,plain,
meet(complement(join(A,B)),complement(A)) = complement(join(A,B)),
inference(paramod,[status(thm)],[c_1486,c_17]) ).
cnf(c_1602,plain,
meet(complement(A),complement(join(A,B))) = complement(join(A,B)),
inference(paramod,[status(thm)],[c_5,c_31292]) ).
cnf(c_31293,plain,
join(complement(meet(A,B)),complement(A)) = complement(meet(A,B)),
inference(paramod,[status(thm)],[c_4,c_1598]) ).
cnf(c_1775,plain,
join(complement(A),complement(meet(A,B))) = complement(meet(A,B)),
inference(paramod,[status(thm)],[c_6,c_31293]) ).
cnf(c_31294,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_105]) ).
cnf(c_31295,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_31294]) ).
cnf(c_4032,plain,
join(A,meet(join(B,A),join(A,C))) = meet(join(B,A),join(A,C)),
inference(paramod,[status(thm)],[c_17,c_31295]) ).
cnf(c_5927,plain,
meet(A,complement(join(B,meet(A,complement(B))))) = zero,
inference(paramod,[status(thm)],[c_1602,c_141]) ).
cnf(c_5943,plain,
meet(A,complement(join(B,meet(complement(B),A)))) = zero,
inference(paramod,[status(thm)],[c_1602,c_1010]) ).
cnf(c_5956,plain,
meet(A,complement(join(complement(B),meet(A,B)))) = zero,
inference(paramod,[status(thm)],[c_342,c_5927]) ).
cnf(c_6231,plain,
meet(A,complement(join(complement(B),meet(B,A)))) = zero,
inference(paramod,[status(thm)],[c_342,c_5943]) ).
cnf(c_6265,plain,
meet(A,complement(join(meet(A,B),complement(B)))) = zero,
inference(paramod,[status(thm)],[c_6,c_5956]) ).
cnf(c_6315,plain,
meet(A,complement(join(meet(B,A),complement(B)))) = zero,
inference(paramod,[status(thm)],[c_6,c_6231]) ).
cnf(c_7320,plain,
meet(complement(A),meet(B,complement(meet(A,C)))) = meet(complement(A),B),
inference(paramod,[status(thm)],[c_1775,c_125]) ).
cnf(c_31296,plain,
join(meet(A,join(meet(A,B),C)),meet(A,B)) = meet(A,join(meet(A,B),C)),
inference(paramod,[status(thm)],[c_21,c_158]) ).
cnf(c_11107,plain,
join(meet(A,B),meet(A,join(meet(A,B),C))) = meet(A,join(meet(A,B),C)),
inference(paramod,[status(thm)],[c_6,c_31296]) ).
cnf(c_17222,plain,
join(complement(A),meet(B,complement(meet(A,B)))) = complement(A),
inference(resolve,[status(thm)],[c_89,c_1264]) ).
cnf(c_31297,plain,
meet(meet(A,complement(meet(B,A))),complement(B)) = meet(A,complement(meet(B,A))),
inference(paramod,[status(thm)],[c_17222,c_17]) ).
cnf(c_31298,plain,
meet(complement(B),meet(A,complement(meet(B,A)))) = meet(A,complement(meet(B,A))),
inference(paramod,[status(thm)],[c_5,c_31297]) ).
cnf(c_31299,plain,
meet(complement(B),A) = meet(A,complement(meet(B,A))),
inference(paramod,[status(thm)],[c_7320,c_31298]) ).
cnf(c_17259,plain,
meet(A,complement(meet(B,A))) = meet(complement(B),A),
inference(copy,[status(thm)],[c_31299]) ).
cnf(c_17331,plain,
meet(A,complement(meet(A,B))) = meet(complement(B),A),
inference(paramod,[status(thm)],[c_5,c_17259]) ).
cnf(c_31300,plain,
meet(A,complement(zero)) = meet(complement(complement(join(B,meet(A,complement(B))))),A),
inference(paramod,[status(thm)],[c_5927,c_17331]) ).
cnf(c_31301,plain,
meet(A,one) = meet(complement(complement(join(B,meet(A,complement(B))))),A),
inference(paramod,[status(thm)],[c_76,c_31300]) ).
cnf(c_31302,plain,
A = meet(complement(complement(join(B,meet(A,complement(B))))),A),
inference(paramod,[status(thm)],[c_34,c_31301]) ).
cnf(c_31303,plain,
A = meet(join(B,meet(A,complement(B))),A),
inference(paramod,[status(thm)],[c_342,c_31302]) ).
cnf(c_31304,plain,
A = meet(A,join(B,meet(A,complement(B)))),
inference(paramod,[status(thm)],[c_5,c_31303]) ).
cnf(c_17909,plain,
meet(A,join(B,meet(A,complement(B)))) = A,
inference(copy,[status(thm)],[c_31304]) ).
cnf(c_31305,plain,
meet(A,complement(zero)) = meet(complement(complement(join(B,meet(complement(B),A)))),A),
inference(paramod,[status(thm)],[c_5943,c_17331]) ).
cnf(c_31306,plain,
meet(A,one) = meet(complement(complement(join(B,meet(complement(B),A)))),A),
inference(paramod,[status(thm)],[c_76,c_31305]) ).
cnf(c_31307,plain,
A = meet(complement(complement(join(B,meet(complement(B),A)))),A),
inference(paramod,[status(thm)],[c_34,c_31306]) ).
cnf(c_31308,plain,
A = meet(join(B,meet(complement(B),A)),A),
inference(paramod,[status(thm)],[c_342,c_31307]) ).
cnf(c_31309,plain,
A = meet(A,join(B,meet(complement(B),A))),
inference(paramod,[status(thm)],[c_5,c_31308]) ).
cnf(c_17911,plain,
meet(A,join(B,meet(complement(B),A))) = A,
inference(copy,[status(thm)],[c_31309]) ).
cnf(c_31310,plain,
meet(A,complement(zero)) = meet(complement(complement(join(complement(B),meet(A,B)))),A),
inference(paramod,[status(thm)],[c_5956,c_17331]) ).
cnf(c_31311,plain,
meet(A,one) = meet(complement(complement(join(complement(B),meet(A,B)))),A),
inference(paramod,[status(thm)],[c_76,c_31310]) ).
cnf(c_31312,plain,
A = meet(complement(complement(join(complement(B),meet(A,B)))),A),
inference(paramod,[status(thm)],[c_34,c_31311]) ).
cnf(c_31313,plain,
A = meet(join(complement(B),meet(A,B)),A),
inference(paramod,[status(thm)],[c_342,c_31312]) ).
cnf(c_31314,plain,
A = meet(A,join(complement(B),meet(A,B))),
inference(paramod,[status(thm)],[c_5,c_31313]) ).
cnf(c_17912,plain,
meet(A,join(complement(B),meet(A,B))) = A,
inference(copy,[status(thm)],[c_31314]) ).
cnf(c_31315,plain,
meet(A,complement(zero)) = meet(complement(complement(join(meet(A,B),complement(B)))),A),
inference(paramod,[status(thm)],[c_6265,c_17331]) ).
cnf(c_31316,plain,
meet(A,one) = meet(complement(complement(join(meet(A,B),complement(B)))),A),
inference(paramod,[status(thm)],[c_76,c_31315]) ).
cnf(c_31317,plain,
A = meet(complement(complement(join(meet(A,B),complement(B)))),A),
inference(paramod,[status(thm)],[c_34,c_31316]) ).
cnf(c_31318,plain,
A = meet(join(meet(A,B),complement(B)),A),
inference(paramod,[status(thm)],[c_342,c_31317]) ).
cnf(c_31319,plain,
A = meet(A,join(meet(A,B),complement(B))),
inference(paramod,[status(thm)],[c_5,c_31318]) ).
cnf(c_17916,plain,
meet(A,join(meet(A,B),complement(B))) = A,
inference(copy,[status(thm)],[c_31319]) ).
cnf(c_31320,plain,
meet(A,complement(zero)) = meet(complement(complement(join(meet(B,A),complement(B)))),A),
inference(paramod,[status(thm)],[c_6315,c_17331]) ).
cnf(c_31321,plain,
meet(A,one) = meet(complement(complement(join(meet(B,A),complement(B)))),A),
inference(paramod,[status(thm)],[c_76,c_31320]) ).
cnf(c_31322,plain,
A = meet(complement(complement(join(meet(B,A),complement(B)))),A),
inference(paramod,[status(thm)],[c_34,c_31321]) ).
cnf(c_31323,plain,
A = meet(join(meet(B,A),complement(B)),A),
inference(paramod,[status(thm)],[c_342,c_31322]) ).
cnf(c_31324,plain,
A = meet(A,join(meet(B,A),complement(B))),
inference(paramod,[status(thm)],[c_5,c_31323]) ).
cnf(c_17918,plain,
meet(A,join(meet(B,A),complement(B))) = A,
inference(copy,[status(thm)],[c_31324]) ).
cnf(c_31325,plain,
join(join(A,meet(B,complement(A))),join(B,C)) = join(join(A,meet(B,complement(A))),C),
inference(paramod,[status(thm)],[c_17909,c_56]) ).
cnf(c_31326,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_31325]) ).
cnf(c_31327,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_31326]) ).
cnf(c_31328,plain,
join(B,join(A,C)) = join(join(A,meet(B,complement(A))),C),
inference(paramod,[status(thm)],[c_287,c_31327]) ).
cnf(c_31329,plain,
join(B,join(A,C)) = join(A,join(meet(B,complement(A)),C)),
inference(paramod,[status(thm)],[c_8,c_31328]) ).
cnf(c_18025,plain,
join(A,join(meet(B,complement(A)),C)) = join(B,join(A,C)),
inference(copy,[status(thm)],[c_31329]) ).
cnf(c_31330,plain,
join(join(A,meet(B,complement(A))),meet(C,meet(D,B))) = join(A,meet(B,complement(A))),
inference(paramod,[status(thm)],[c_17909,c_118]) ).
cnf(c_31331,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_31330]) ).
cnf(c_31332,plain,
join(B,join(A,meet(C,meet(D,B)))) = join(A,meet(B,complement(A))),
inference(paramod,[status(thm)],[c_18025,c_31331]) ).
cnf(c_31333,plain,
join(A,B) = join(A,meet(B,complement(A))),
inference(paramod,[status(thm)],[c_271,c_31332]) ).
cnf(c_18027,plain,
join(A,meet(B,complement(A))) = join(A,B),
inference(copy,[status(thm)],[c_31333]) ).
cnf(c_31334,plain,
join(join(A,meet(complement(A),B)),join(B,C)) = join(join(A,meet(complement(A),B)),C),
inference(paramod,[status(thm)],[c_17911,c_56]) ).
cnf(c_31335,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_31334]) ).
cnf(c_31336,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_31335]) ).
cnf(c_31337,plain,
join(A,join(B,C)) = join(join(A,meet(complement(A),B)),C),
inference(paramod,[status(thm)],[c_604,c_31336]) ).
cnf(c_31338,plain,
join(A,join(B,C)) = join(A,join(meet(complement(A),B),C)),
inference(paramod,[status(thm)],[c_8,c_31337]) ).
cnf(c_18051,plain,
join(A,join(meet(complement(A),B),C)) = join(A,join(B,C)),
inference(copy,[status(thm)],[c_31338]) ).
cnf(c_31339,plain,
join(join(A,meet(complement(A),B)),meet(C,meet(D,B))) = join(A,meet(complement(A),B)),
inference(paramod,[status(thm)],[c_17911,c_118]) ).
cnf(c_31340,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_31339]) ).
cnf(c_31341,plain,
join(A,join(B,meet(C,meet(D,B)))) = join(A,meet(complement(A),B)),
inference(paramod,[status(thm)],[c_18051,c_31340]) ).
cnf(c_31342,plain,
join(A,B) = join(A,meet(complement(A),B)),
inference(paramod,[status(thm)],[c_55,c_31341]) ).
cnf(c_18053,plain,
join(A,meet(complement(A),B)) = join(A,B),
inference(copy,[status(thm)],[c_31342]) ).
cnf(c_31343,plain,
join(complement(A),join(meet(B,A),B)) = join(complement(A),meet(B,A)),
inference(paramod,[status(thm)],[c_17912,c_57]) ).
cnf(c_31344,plain,
join(complement(A),join(B,meet(B,A))) = join(complement(A),meet(B,A)),
inference(paramod,[status(thm)],[c_6,c_31343]) ).
cnf(c_31345,plain,
join(complement(A),B) = join(complement(A),meet(B,A)),
inference(paramod,[status(thm)],[c_4,c_31344]) ).
cnf(c_18098,plain,
join(complement(A),meet(B,A)) = join(complement(A),B),
inference(copy,[status(thm)],[c_31345]) ).
cnf(c_31346,plain,
join(join(meet(A,B),complement(B)),A) = join(meet(A,B),complement(B)),
inference(paramod,[status(thm)],[c_17916,c_16]) ).
cnf(c_31347,plain,
join(A,join(meet(A,B),complement(B))) = join(meet(A,B),complement(B)),
inference(paramod,[status(thm)],[c_6,c_31346]) ).
cnf(c_31348,plain,
join(A,complement(B)) = join(meet(A,B),complement(B)),
inference(paramod,[status(thm)],[c_31,c_31347]) ).
cnf(c_18274,plain,
join(meet(A,B),complement(B)) = join(A,complement(B)),
inference(copy,[status(thm)],[c_31348]) ).
cnf(c_31349,plain,
join(join(meet(A,B),complement(A)),B) = join(meet(A,B),complement(A)),
inference(paramod,[status(thm)],[c_17918,c_16]) ).
cnf(c_31350,plain,
join(B,join(meet(A,B),complement(A))) = join(meet(A,B),complement(A)),
inference(paramod,[status(thm)],[c_6,c_31349]) ).
cnf(c_31351,plain,
join(B,complement(A)) = join(meet(A,B),complement(A)),
inference(paramod,[status(thm)],[c_56,c_31350]) ).
cnf(c_18281,plain,
join(meet(A,B),complement(A)) = join(B,complement(A)),
inference(copy,[status(thm)],[c_31351]) ).
cnf(c_31352,plain,
join(complement(A),meet(complement(meet(A,B)),complement(complement(A)))) = complement(meet(A,B)),
inference(paramod,[status(thm)],[c_1775,c_18027]) ).
cnf(c_31353,plain,
join(complement(A),meet(complement(meet(A,B)),A)) = complement(meet(A,B)),
inference(paramod,[status(thm)],[c_342,c_31352]) ).
cnf(c_31354,plain,
join(complement(A),meet(A,complement(meet(A,B)))) = complement(meet(A,B)),
inference(paramod,[status(thm)],[c_5,c_31353]) ).
cnf(c_31355,plain,
join(complement(A),meet(complement(B),A)) = complement(meet(A,B)),
inference(paramod,[status(thm)],[c_17331,c_31354]) ).
cnf(c_31356,plain,
join(complement(A),complement(B)) = complement(meet(A,B)),
inference(paramod,[status(thm)],[c_18098,c_31355]) ).
cnf(c_18310,plain,
complement(meet(A,B)) = join(complement(A),complement(B)),
inference(copy,[status(thm)],[c_31356]) ).
cnf(c_22113,plain,
complement(join(complement(A),complement(B))) = meet(A,B),
inference(paramod,[status(thm)],[c_18310,c_342]) ).
cnf(c_22294,plain,
complement(join(A,complement(B))) = meet(complement(A),B),
inference(paramod,[status(thm)],[c_342,c_22113]) ).
cnf(c_22628,plain,
complement(join(A,B)) = meet(complement(A),complement(B)),
inference(paramod,[status(thm)],[c_342,c_22294]) ).
cnf(c_31357,plain,
meet(complement(join(A,B)),join(A,B)) = zero,
inference(paramod,[status(thm)],[c_212,c_75]) ).
cnf(c_31358,plain,
meet(meet(complement(A),complement(B)),join(A,B)) = zero,
inference(paramod,[status(thm)],[c_22628,c_31357]) ).
cnf(c_27076,plain,
meet(complement(A),meet(complement(B),join(A,B))) = zero,
inference(paramod,[status(thm)],[c_7,c_31358]) ).
cnf(c_31359,plain,
join(meet(A,B),complement(A)) = join(meet(B,join(A,C)),complement(A)),
inference(paramod,[status(thm)],[c_125,c_18281]) ).
cnf(c_31360,plain,
join(B,complement(A)) = join(meet(B,join(A,C)),complement(A)),
inference(paramod,[status(thm)],[c_18281,c_31359]) ).
cnf(c_27197,plain,
join(meet(A,join(B,C)),complement(B)) = join(A,complement(B)),
inference(copy,[status(thm)],[c_31360]) ).
cnf(c_31361,plain,
join(meet(A,B),complement(A)) = join(meet(B,join(C,A)),complement(A)),
inference(paramod,[status(thm)],[c_145,c_18281]) ).
cnf(c_31362,plain,
join(B,complement(A)) = join(meet(B,join(C,A)),complement(A)),
inference(paramod,[status(thm)],[c_18281,c_31361]) ).
cnf(c_27198,plain,
join(meet(A,join(B,C)),complement(C)) = join(A,complement(C)),
inference(copy,[status(thm)],[c_31362]) ).
cnf(c_31363,plain,
join(A,zero) = join(A,meet(complement(B),join(A,B))),
inference(paramod,[status(thm)],[c_27076,c_18053]) ).
cnf(c_31364,plain,
A = join(A,meet(complement(B),join(A,B))),
inference(paramod,[status(thm)],[c_37,c_31363]) ).
cnf(c_27734,plain,
join(A,meet(complement(B),join(A,B))) = A,
inference(copy,[status(thm)],[c_31364]) ).
cnf(c_31365,plain,
join(A,meet(complement(meet(B,complement(A))),join(A,B))) = A,
inference(paramod,[status(thm)],[c_18027,c_27734]) ).
cnf(c_31366,plain,
join(A,meet(join(complement(B),complement(complement(A))),join(A,B))) = A,
inference(paramod,[status(thm)],[c_18310,c_31365]) ).
cnf(c_31367,plain,
join(A,meet(join(complement(B),A),join(A,B))) = A,
inference(paramod,[status(thm)],[c_342,c_31366]) ).
cnf(c_27862,plain,
meet(join(complement(A),B),join(B,A)) = B,
inference(paramod,[status(thm)],[c_4032,c_31367]) ).
cnf(c_31368,plain,
meet(join(complement(join(A,B)),B),join(A,B)) = B,
inference(paramod,[status(thm)],[c_28,c_27862]) ).
cnf(c_31369,plain,
meet(join(meet(complement(A),complement(B)),B),join(A,B)) = B,
inference(paramod,[status(thm)],[c_22628,c_31368]) ).
cnf(c_31370,plain,
meet(join(B,meet(complement(A),complement(B))),join(A,B)) = B,
inference(paramod,[status(thm)],[c_6,c_31369]) ).
cnf(c_28241,plain,
meet(join(A,complement(B)),join(B,A)) = A,
inference(paramod,[status(thm)],[c_18027,c_31370]) ).
cnf(c_31371,plain,
meet(join(join(A,meet(B,C)),complement(C)),join(C,A)) = join(A,meet(B,C)),
inference(paramod,[status(thm)],[c_116,c_28241]) ).
cnf(c_31372,plain,
meet(join(A,join(meet(B,C),complement(C))),join(C,A)) = join(A,meet(B,C)),
inference(paramod,[status(thm)],[c_8,c_31371]) ).
cnf(c_29961,plain,
meet(join(A,join(B,complement(C))),join(C,A)) = join(A,meet(B,C)),
inference(paramod,[status(thm)],[c_18274,c_31372]) ).
cnf(c_31373,plain,
meet(join(join(A,meet(B,join(C,A))),complement(C)),join(C,A)) = join(A,meet(B,join(C,A))),
inference(paramod,[status(thm)],[c_57,c_28241]) ).
cnf(c_31374,plain,
meet(join(A,join(meet(B,join(C,A)),complement(C))),join(C,A)) = join(A,meet(B,join(C,A))),
inference(paramod,[status(thm)],[c_8,c_31373]) ).
cnf(c_31375,plain,
meet(join(A,join(B,complement(C))),join(C,A)) = join(A,meet(B,join(C,A))),
inference(paramod,[status(thm)],[c_27197,c_31374]) ).
cnf(c_31376,plain,
join(A,meet(B,C)) = join(A,meet(B,join(C,A))),
inference(paramod,[status(thm)],[c_29961,c_31375]) ).
cnf(c_29965,plain,
join(A,meet(B,join(C,A))) = join(A,meet(B,C)),
inference(copy,[status(thm)],[c_31376]) ).
cnf(c_31377,plain,
meet(join(join(A,meet(B,join(A,C))),complement(C)),join(C,A)) = join(A,meet(B,join(A,C))),
inference(paramod,[status(thm)],[c_1122,c_28241]) ).
cnf(c_31378,plain,
meet(join(A,join(meet(B,join(A,C)),complement(C))),join(C,A)) = join(A,meet(B,join(A,C))),
inference(paramod,[status(thm)],[c_8,c_31377]) ).
cnf(c_31379,plain,
meet(join(A,join(B,complement(C))),join(C,A)) = join(A,meet(B,join(A,C))),
inference(paramod,[status(thm)],[c_27198,c_31378]) ).
cnf(c_31380,plain,
join(A,meet(B,C)) = join(A,meet(B,join(A,C))),
inference(paramod,[status(thm)],[c_29961,c_31379]) ).
cnf(c_29987,plain,
join(A,meet(B,join(A,C))) = join(A,meet(B,C)),
inference(copy,[status(thm)],[c_31380]) ).
cnf(c_30054,plain,
meet(A,join(B,meet(A,C))) = meet(A,join(B,C)),
inference(paramod,[status(thm)],[c_29965,c_1175]) ).
cnf(c_30318,plain,
join(meet(A,B),meet(A,C)) = meet(A,join(meet(A,B),C)),
inference(paramod,[status(thm)],[c_29987,c_11107]) ).
cnf(c_31381,plain,
meet(a,join(meet(a,b),c)) != meet(a,join(b,c)),
inference(paramod,[status(thm)],[c_30318,c_15]) ).
cnf(c_31382,plain,
meet(a,join(c,meet(a,b))) != meet(a,join(b,c)),
inference(paramod,[status(thm)],[c_6,c_31381]) ).
cnf(c_31383,plain,
meet(a,join(c,b)) != meet(a,join(b,c)),
inference(paramod,[status(thm)],[c_30054,c_31382]) ).
cnf(c_31384,plain,
meet(a,join(b,c)) != meet(a,join(b,c)),
inference(paramod,[status(thm)],[c_6,c_31383]) ).
cnf(c_31237,plain,
$false,
inference(copy,[status(thm)],[c_31384]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LAT209-1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.03 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n001.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:21:11 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.36 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.08/0.36 % Process 4143381 was started by sandbox2 on n001,
% 0.08/0.36 % Fri Sep 25 20:21:11 2026
% 0.08/0.36 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.13/0.36
% 0.13/0.36 % From the command line: assign(max_seconds, 300).
% 156.76/21.42
% 156.76/21.42 % given #500 (T,wt=11): 17810 meet(A,complement(B)) != zero | meet(A,B) = A. [para(5(a,1),17325(a,1))].
% 156.76/21.42
% 156.76/21.42 % SZS status Unsatisfiable for theBenchmark
% 156.76/21.42
% 156.76/21.42 % Proof 1 at 17.44 (+ 3.23) seconds.
% 156.76/21.42 % Length of proof is 115.
% 156.76/21.42 % Level of proof is 26.
% 156.76/21.42 % Maximum clause weight is 27.000.
% 156.76/21.42 % Given clauses 547.
% 156.76/21.42
% 156.76/21.42 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------