%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : LAT210-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 : n020.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 142.14s 19.38s
% Output : CNFRefutation 142.14s
% Verified :
% SZS Type : Refutation
% Derivation depth : 70
% Number of leaves : 13
% Syntax : Number of formulae : 264 ( 252 unt; 0 def)
% Number of atoms : 284 ( 283 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 : 7 ( 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 : 596 ( 82 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_H68,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,VAR_1))))),
file('theBenchmark.p',equation_H68) ).
cnf(c_12,plain,
meet(A,join(B,C)) = meet(A,join(B,meet(A,join(C,meet(A,B))))),
inference(clausify,[status(thm)],[equation_H68]) ).
cnf(c_13,plain,
meet(A,join(B,meet(A,join(C,meet(A,B))))) = 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_29746,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_29746]) ).
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_29747,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_29747]) ).
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_29748,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_29748]) ).
cnf(c_29749,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_29749]) ).
cnf(c_29750,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_29750]) ).
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_29751,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_29751]) ).
cnf(c_29752,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_29752]) ).
cnf(c_34,plain,
meet(A,one) = A,
inference(paramod,[status(thm)],[c_9,c_3]) ).
cnf(c_29753,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_29753]) ).
cnf(c_37,plain,
join(A,zero) = A,
inference(paramod,[status(thm)],[c_10,c_4]) ).
cnf(c_29754,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_29754]) ).
cnf(c_29755,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_29755]) ).
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_29756,plain,
meet(join(A,B),join(A,meet(join(A,B),join(B,meet(join(A,B),A))))) = join(A,B),
inference(paramod,[status(thm)],[c_1,c_13]) ).
cnf(c_29757,plain,
meet(join(A,B),join(A,meet(join(A,B),join(B,meet(A,join(A,B)))))) = join(A,B),
inference(paramod,[status(thm)],[c_5,c_29756]) ).
cnf(c_44,plain,
meet(join(A,B),join(A,meet(join(A,B),join(B,A)))) = join(A,B),
inference(paramod,[status(thm)],[c_3,c_29757]) ).
cnf(c_45,plain,
meet(A,join(B,meet(A,join(C,meet(B,A))))) = meet(A,join(B,C)),
inference(paramod,[status(thm)],[c_5,c_13]) ).
cnf(c_29758,plain,
meet(A,join(complement(A),meet(A,join(B,zero)))) = meet(A,join(complement(A),B)),
inference(paramod,[status(thm)],[c_10,c_13]) ).
cnf(c_51,plain,
meet(A,join(complement(A),meet(A,B))) = meet(A,join(complement(A),B)),
inference(paramod,[status(thm)],[c_37,c_29758]) ).
cnf(c_54,plain,
join(A,meet(B,meet(C,A))) = A,
inference(paramod,[status(thm)],[c_7,c_16]) ).
cnf(c_29759,plain,
join(A,B) = join(A,join(meet(C,A),B)),
inference(paramod,[status(thm)],[c_16,c_8]) ).
cnf(c_55,plain,
join(A,join(meet(B,A),C)) = join(A,C),
inference(copy,[status(thm)],[c_29759]) ).
cnf(c_29760,plain,
join(A,B) = join(A,join(B,meet(C,join(A,B)))),
inference(paramod,[status(thm)],[c_16,c_8]) ).
cnf(c_56,plain,
join(A,join(B,meet(C,join(A,B)))) = join(A,B),
inference(copy,[status(thm)],[c_29760]) ).
cnf(c_62,plain,
join(one,A) = one,
inference(paramod,[status(thm)],[c_34,c_16]) ).
cnf(c_63,plain,
join(A,join(complement(A),B)) = one,
inference(paramod,[status(thm)],[c_62,c_35]) ).
cnf(c_29761,plain,
A = join(zero,A),
inference(paramod,[status(thm)],[c_37,c_6]) ).
cnf(c_64,plain,
join(zero,A) = A,
inference(copy,[status(thm)],[c_29761]) ).
cnf(c_69,plain,
meet(A,join(B,join(C,A))) = A,
inference(paramod,[status(thm)],[c_8,c_17]) ).
cnf(c_71,plain,
meet(zero,A) = zero,
inference(paramod,[status(thm)],[c_37,c_17]) ).
cnf(c_73,plain,
meet(A,meet(complement(A),B)) = zero,
inference(paramod,[status(thm)],[c_71,c_38]) ).
cnf(c_29762,plain,
( complement(zero) = one
| join(zero,one) != one ),
inference(resolve,[status(thm)],[c_11,c_34]) ).
cnf(c_74,plain,
complement(zero) = one,
inference(resolve,[status(thm)],[c_29762,c_64]) ).
cnf(c_76,plain,
meet(A,zero) = zero,
inference(paramod,[status(thm)],[c_64,c_16]) ).
cnf(c_29763,plain,
( complement(A) = join(complement(A),B)
| one != one
| meet(A,join(complement(A),B)) != zero ),
inference(paramod,[status(thm)],[c_63,c_11]) ).
cnf(c_29764,plain,
( join(complement(A),B) = complement(A)
| one != one
| meet(A,join(complement(A),B)) != zero ),
inference(copy,[status(thm)],[c_29763]) ).
cnf(c_88,plain,
( join(complement(A),B) = complement(A)
| meet(A,join(complement(A),B)) != zero ),
inference(copy,[status(thm)],[c_29764]) ).
cnf(c_29765,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_104,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_29765]) ).
cnf(c_29766,plain,
meet(A,join(B,meet(A,join(join(C,B),meet(A,B))))) = meet(A,join(C,B)),
inference(paramod,[status(thm)],[c_28,c_13]) ).
cnf(c_29767,plain,
meet(A,join(B,meet(A,join(C,join(B,meet(A,B)))))) = meet(A,join(C,B)),
inference(paramod,[status(thm)],[c_8,c_29766]) ).
cnf(c_111,plain,
meet(A,join(B,meet(A,join(C,B)))) = meet(A,join(C,B)),
inference(paramod,[status(thm)],[c_16,c_29767]) ).
cnf(c_112,plain,
meet(join(A,B),join(B,A)) = join(A,B),
inference(paramod,[status(thm)],[c_111,c_44]) ).
cnf(c_29768,plain,
join(join(A,B),meet(C,A)) = join(A,B),
inference(paramod,[status(thm)],[c_3,c_54]) ).
cnf(c_113,plain,
join(A,join(B,meet(C,A))) = join(A,B),
inference(paramod,[status(thm)],[c_8,c_29768]) ).
cnf(c_114,plain,
join(A,meet(B,meet(A,C))) = A,
inference(paramod,[status(thm)],[c_5,c_54]) ).
cnf(c_115,plain,
join(A,meet(B,meet(C,meet(D,A)))) = A,
inference(paramod,[status(thm)],[c_7,c_54]) ).
cnf(c_29769,plain,
meet(meet(A,B),join(C,A)) = meet(A,B),
inference(paramod,[status(thm)],[c_4,c_69]) ).
cnf(c_123,plain,
meet(A,meet(B,join(C,A))) = meet(A,B),
inference(paramod,[status(thm)],[c_7,c_29769]) ).
cnf(c_128,plain,
meet(A,meet(B,join(A,C))) = meet(A,B),
inference(paramod,[status(thm)],[c_5,c_22]) ).
cnf(c_29770,plain,
meet(A,zero) = meet(A,complement(join(A,B))),
inference(paramod,[status(thm)],[c_10,c_22]) ).
cnf(c_29771,plain,
zero = meet(A,complement(join(A,B))),
inference(paramod,[status(thm)],[c_76,c_29770]) ).
cnf(c_130,plain,
meet(A,complement(join(A,B))) = zero,
inference(copy,[status(thm)],[c_29771]) ).
cnf(c_139,plain,
meet(A,complement(join(B,A))) = zero,
inference(paramod,[status(thm)],[c_6,c_130]) ).
cnf(c_29772,plain,
zero = meet(A,meet(B,complement(join(C,meet(A,B))))),
inference(paramod,[status(thm)],[c_139,c_7]) ).
cnf(c_144,plain,
meet(A,meet(B,complement(join(C,meet(A,B))))) = zero,
inference(copy,[status(thm)],[c_29772]) ).
cnf(c_145,plain,
meet(A,complement(join(B,join(C,A)))) = zero,
inference(paramod,[status(thm)],[c_8,c_139]) ).
cnf(c_29773,plain,
join(join(A,B),meet(A,C)) = join(A,B),
inference(paramod,[status(thm)],[c_22,c_114]) ).
cnf(c_157,plain,
join(A,join(B,meet(A,C))) = join(A,B),
inference(paramod,[status(thm)],[c_8,c_29773]) ).
cnf(c_159,plain,
join(meet(A,B),meet(A,meet(C,B))) = meet(A,B),
inference(paramod,[status(thm)],[c_5,c_23]) ).
cnf(c_164,plain,
join(meet(A,B),meet(B,A)) = meet(A,B),
inference(paramod,[status(thm)],[c_20,c_23]) ).
cnf(c_29774,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_210,plain,
meet(join(A,B),meet(C,join(A,join(B,D)))) = meet(C,join(A,B)),
inference(copy,[status(thm)],[c_29774]) ).
cnf(c_29775,plain,
join(A,B) = join(B,join(A,meet(C,meet(D,B)))),
inference(paramod,[status(thm)],[c_54,c_33]) ).
cnf(c_269,plain,
join(A,join(B,meet(C,meet(D,A)))) = join(B,A),
inference(copy,[status(thm)],[c_29775]) ).
cnf(c_285,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_29776,plain,
( complement(complement(A)) = A
| one != one
| meet(complement(A),A) != zero ),
inference(paramod,[status(thm)],[c_9,c_42]) ).
cnf(c_29777,plain,
( complement(complement(A)) = A
| one != one
| meet(A,complement(A)) != zero ),
inference(paramod,[status(thm)],[c_5,c_29776]) ).
cnf(c_29778,plain,
( complement(complement(A)) = A
| one != one
| zero != zero ),
inference(paramod,[status(thm)],[c_10,c_29777]) ).
cnf(c_29779,plain,
( complement(complement(A)) = A
| one != one ),
inference(copy,[status(thm)],[c_29778]) ).
cnf(c_340,plain,
complement(complement(A)) = A,
inference(copy,[status(thm)],[c_29779]) ).
cnf(c_29780,plain,
meet(A,join(B,meet(A,join(join(B,C),meet(B,A))))) = meet(A,join(B,C)),
inference(paramod,[status(thm)],[c_27,c_45]) ).
cnf(c_29781,plain,
meet(A,join(B,meet(A,join(B,join(C,meet(B,A)))))) = meet(A,join(B,C)),
inference(paramod,[status(thm)],[c_8,c_29780]) ).
cnf(c_466,plain,
meet(A,join(B,meet(A,join(B,C)))) = meet(A,join(B,C)),
inference(paramod,[status(thm)],[c_157,c_29781]) ).
cnf(c_29782,plain,
join(A,join(B,C)) = join(B,join(A,join(meet(D,B),C))),
inference(paramod,[status(thm)],[c_55,c_33]) ).
cnf(c_587,plain,
join(A,join(B,join(meet(C,A),D))) = join(B,join(A,D)),
inference(copy,[status(thm)],[c_29782]) ).
cnf(c_29783,plain,
join(join(A,B),meet(C,join(B,A))) = join(A,B),
inference(paramod,[status(thm)],[c_112,c_54]) ).
cnf(c_629,plain,
join(A,join(B,meet(C,join(B,A)))) = join(A,B),
inference(paramod,[status(thm)],[c_8,c_29783]) ).
cnf(c_29784,plain,
meet(meet(A,B),complement(join(C,meet(B,A)))) = zero,
inference(paramod,[status(thm)],[c_164,c_145]) ).
cnf(c_1052,plain,
meet(A,meet(B,complement(join(C,meet(B,A))))) = zero,
inference(paramod,[status(thm)],[c_7,c_29784]) ).
cnf(c_29785,plain,
meet(A,join(complement(A),zero)) = meet(A,join(complement(A),complement(join(A,B)))),
inference(paramod,[status(thm)],[c_130,c_51]) ).
cnf(c_29786,plain,
meet(A,join(zero,complement(A))) = meet(A,join(complement(A),complement(join(A,B)))),
inference(paramod,[status(thm)],[c_6,c_29785]) ).
cnf(c_29787,plain,
meet(A,complement(A)) = meet(A,join(complement(A),complement(join(A,B)))),
inference(paramod,[status(thm)],[c_64,c_29786]) ).
cnf(c_29788,plain,
zero = meet(A,join(complement(A),complement(join(A,B)))),
inference(paramod,[status(thm)],[c_10,c_29787]) ).
cnf(c_1177,plain,
meet(A,join(complement(A),complement(join(A,B)))) = zero,
inference(copy,[status(thm)],[c_29788]) ).
cnf(c_29789,plain,
meet(A,join(complement(A),zero)) = meet(A,join(complement(A),meet(B,complement(meet(A,B))))),
inference(paramod,[status(thm)],[c_39,c_51]) ).
cnf(c_29790,plain,
meet(A,join(zero,complement(A))) = meet(A,join(complement(A),meet(B,complement(meet(A,B))))),
inference(paramod,[status(thm)],[c_6,c_29789]) ).
cnf(c_29791,plain,
meet(A,complement(A)) = meet(A,join(complement(A),meet(B,complement(meet(A,B))))),
inference(paramod,[status(thm)],[c_64,c_29790]) ).
cnf(c_29792,plain,
zero = meet(A,join(complement(A),meet(B,complement(meet(A,B))))),
inference(paramod,[status(thm)],[c_10,c_29791]) ).
cnf(c_1179,plain,
meet(A,join(complement(A),meet(B,complement(meet(A,B))))) = zero,
inference(copy,[status(thm)],[c_29792]) ).
cnf(c_29793,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_1177]) ).
cnf(c_29794,plain,
complement(A) = join(complement(A),complement(join(A,B))),
inference(resolve,[status(thm)],[c_29793,c_63]) ).
cnf(c_1391,plain,
join(complement(A),complement(join(A,B))) = complement(A),
inference(copy,[status(thm)],[c_29794]) ).
cnf(c_1429,plain,
join(complement(A),complement(join(B,A))) = complement(A),
inference(paramod,[status(thm)],[c_6,c_1391]) ).
cnf(c_29795,plain,
meet(complement(join(A,B)),complement(A)) = complement(join(A,B)),
inference(paramod,[status(thm)],[c_1391,c_17]) ).
cnf(c_1433,plain,
meet(complement(A),complement(join(A,B))) = complement(join(A,B)),
inference(paramod,[status(thm)],[c_5,c_29795]) ).
cnf(c_29796,plain,
join(complement(meet(A,B)),complement(A)) = complement(meet(A,B)),
inference(paramod,[status(thm)],[c_4,c_1429]) ).
cnf(c_1526,plain,
join(complement(A),complement(meet(A,B))) = complement(meet(A,B)),
inference(paramod,[status(thm)],[c_6,c_29796]) ).
cnf(c_29797,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_104]) ).
cnf(c_29798,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_29797]) ).
cnf(c_3055,plain,
join(A,meet(join(B,A),join(A,C))) = meet(join(B,A),join(A,C)),
inference(paramod,[status(thm)],[c_17,c_29798]) ).
cnf(c_6042,plain,
meet(A,complement(join(B,meet(A,complement(B))))) = zero,
inference(paramod,[status(thm)],[c_1433,c_144]) ).
cnf(c_6059,plain,
meet(A,complement(join(B,meet(complement(B),A)))) = zero,
inference(paramod,[status(thm)],[c_1433,c_1052]) ).
cnf(c_6072,plain,
meet(A,complement(join(complement(B),meet(A,B)))) = zero,
inference(paramod,[status(thm)],[c_340,c_6042]) ).
cnf(c_6281,plain,
meet(A,complement(join(complement(B),meet(B,A)))) = zero,
inference(paramod,[status(thm)],[c_340,c_6059]) ).
cnf(c_6319,plain,
meet(A,complement(join(meet(A,B),complement(B)))) = zero,
inference(paramod,[status(thm)],[c_6,c_6072]) ).
cnf(c_6374,plain,
meet(A,complement(join(meet(B,A),complement(B)))) = zero,
inference(paramod,[status(thm)],[c_6,c_6281]) ).
cnf(c_7255,plain,
meet(complement(A),meet(B,complement(meet(A,C)))) = meet(complement(A),B),
inference(paramod,[status(thm)],[c_1526,c_128]) ).
cnf(c_29799,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_159]) ).
cnf(c_9929,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_29799]) ).
cnf(c_16527,plain,
join(complement(A),meet(B,complement(meet(A,B)))) = complement(A),
inference(resolve,[status(thm)],[c_88,c_1179]) ).
cnf(c_29800,plain,
meet(meet(A,complement(meet(B,A))),complement(B)) = meet(A,complement(meet(B,A))),
inference(paramod,[status(thm)],[c_16527,c_17]) ).
cnf(c_29801,plain,
meet(complement(B),meet(A,complement(meet(B,A)))) = meet(A,complement(meet(B,A))),
inference(paramod,[status(thm)],[c_5,c_29800]) ).
cnf(c_29802,plain,
meet(complement(B),A) = meet(A,complement(meet(B,A))),
inference(paramod,[status(thm)],[c_7255,c_29801]) ).
cnf(c_16545,plain,
meet(A,complement(meet(B,A))) = meet(complement(B),A),
inference(copy,[status(thm)],[c_29802]) ).
cnf(c_16623,plain,
meet(A,complement(meet(A,B))) = meet(complement(B),A),
inference(paramod,[status(thm)],[c_5,c_16545]) ).
cnf(c_29803,plain,
meet(A,complement(zero)) = meet(complement(complement(join(B,meet(A,complement(B))))),A),
inference(paramod,[status(thm)],[c_6042,c_16623]) ).
cnf(c_29804,plain,
meet(A,one) = meet(complement(complement(join(B,meet(A,complement(B))))),A),
inference(paramod,[status(thm)],[c_74,c_29803]) ).
cnf(c_29805,plain,
A = meet(complement(complement(join(B,meet(A,complement(B))))),A),
inference(paramod,[status(thm)],[c_34,c_29804]) ).
cnf(c_29806,plain,
A = meet(join(B,meet(A,complement(B))),A),
inference(paramod,[status(thm)],[c_340,c_29805]) ).
cnf(c_29807,plain,
A = meet(A,join(B,meet(A,complement(B)))),
inference(paramod,[status(thm)],[c_5,c_29806]) ).
cnf(c_17107,plain,
meet(A,join(B,meet(A,complement(B)))) = A,
inference(copy,[status(thm)],[c_29807]) ).
cnf(c_29808,plain,
meet(A,complement(zero)) = meet(complement(complement(join(B,meet(complement(B),A)))),A),
inference(paramod,[status(thm)],[c_6059,c_16623]) ).
cnf(c_29809,plain,
meet(A,one) = meet(complement(complement(join(B,meet(complement(B),A)))),A),
inference(paramod,[status(thm)],[c_74,c_29808]) ).
cnf(c_29810,plain,
A = meet(complement(complement(join(B,meet(complement(B),A)))),A),
inference(paramod,[status(thm)],[c_34,c_29809]) ).
cnf(c_29811,plain,
A = meet(join(B,meet(complement(B),A)),A),
inference(paramod,[status(thm)],[c_340,c_29810]) ).
cnf(c_29812,plain,
A = meet(A,join(B,meet(complement(B),A))),
inference(paramod,[status(thm)],[c_5,c_29811]) ).
cnf(c_17110,plain,
meet(A,join(B,meet(complement(B),A))) = A,
inference(copy,[status(thm)],[c_29812]) ).
cnf(c_29813,plain,
meet(A,complement(zero)) = meet(complement(complement(join(complement(B),meet(A,B)))),A),
inference(paramod,[status(thm)],[c_6072,c_16623]) ).
cnf(c_29814,plain,
meet(A,one) = meet(complement(complement(join(complement(B),meet(A,B)))),A),
inference(paramod,[status(thm)],[c_74,c_29813]) ).
cnf(c_29815,plain,
A = meet(complement(complement(join(complement(B),meet(A,B)))),A),
inference(paramod,[status(thm)],[c_34,c_29814]) ).
cnf(c_29816,plain,
A = meet(join(complement(B),meet(A,B)),A),
inference(paramod,[status(thm)],[c_340,c_29815]) ).
cnf(c_29817,plain,
A = meet(A,join(complement(B),meet(A,B))),
inference(paramod,[status(thm)],[c_5,c_29816]) ).
cnf(c_17111,plain,
meet(A,join(complement(B),meet(A,B))) = A,
inference(copy,[status(thm)],[c_29817]) ).
cnf(c_29818,plain,
meet(A,complement(zero)) = meet(complement(complement(join(meet(A,B),complement(B)))),A),
inference(paramod,[status(thm)],[c_6319,c_16623]) ).
cnf(c_29819,plain,
meet(A,one) = meet(complement(complement(join(meet(A,B),complement(B)))),A),
inference(paramod,[status(thm)],[c_74,c_29818]) ).
cnf(c_29820,plain,
A = meet(complement(complement(join(meet(A,B),complement(B)))),A),
inference(paramod,[status(thm)],[c_34,c_29819]) ).
cnf(c_29821,plain,
A = meet(join(meet(A,B),complement(B)),A),
inference(paramod,[status(thm)],[c_340,c_29820]) ).
cnf(c_29822,plain,
A = meet(A,join(meet(A,B),complement(B))),
inference(paramod,[status(thm)],[c_5,c_29821]) ).
cnf(c_17114,plain,
meet(A,join(meet(A,B),complement(B))) = A,
inference(copy,[status(thm)],[c_29822]) ).
cnf(c_29823,plain,
meet(A,complement(zero)) = meet(complement(complement(join(meet(B,A),complement(B)))),A),
inference(paramod,[status(thm)],[c_6374,c_16623]) ).
cnf(c_29824,plain,
meet(A,one) = meet(complement(complement(join(meet(B,A),complement(B)))),A),
inference(paramod,[status(thm)],[c_74,c_29823]) ).
cnf(c_29825,plain,
A = meet(complement(complement(join(meet(B,A),complement(B)))),A),
inference(paramod,[status(thm)],[c_34,c_29824]) ).
cnf(c_29826,plain,
A = meet(join(meet(B,A),complement(B)),A),
inference(paramod,[status(thm)],[c_340,c_29825]) ).
cnf(c_29827,plain,
A = meet(A,join(meet(B,A),complement(B))),
inference(paramod,[status(thm)],[c_5,c_29826]) ).
cnf(c_17117,plain,
meet(A,join(meet(B,A),complement(B))) = A,
inference(copy,[status(thm)],[c_29827]) ).
cnf(c_29828,plain,
join(join(A,meet(B,complement(A))),join(B,C)) = join(join(A,meet(B,complement(A))),C),
inference(paramod,[status(thm)],[c_17107,c_55]) ).
cnf(c_29829,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_29828]) ).
cnf(c_29830,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_29829]) ).
cnf(c_29831,plain,
join(B,join(A,C)) = join(join(A,meet(B,complement(A))),C),
inference(paramod,[status(thm)],[c_285,c_29830]) ).
cnf(c_29832,plain,
join(B,join(A,C)) = join(A,join(meet(B,complement(A)),C)),
inference(paramod,[status(thm)],[c_8,c_29831]) ).
cnf(c_17239,plain,
join(A,join(meet(B,complement(A)),C)) = join(B,join(A,C)),
inference(copy,[status(thm)],[c_29832]) ).
cnf(c_29833,plain,
join(join(A,meet(B,complement(A))),meet(C,meet(D,B))) = join(A,meet(B,complement(A))),
inference(paramod,[status(thm)],[c_17107,c_115]) ).
cnf(c_29834,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_29833]) ).
cnf(c_29835,plain,
join(B,join(A,meet(C,meet(D,B)))) = join(A,meet(B,complement(A))),
inference(paramod,[status(thm)],[c_17239,c_29834]) ).
cnf(c_29836,plain,
join(A,B) = join(A,meet(B,complement(A))),
inference(paramod,[status(thm)],[c_269,c_29835]) ).
cnf(c_17241,plain,
join(A,meet(B,complement(A))) = join(A,B),
inference(copy,[status(thm)],[c_29836]) ).
cnf(c_29837,plain,
join(join(A,meet(complement(A),B)),join(B,C)) = join(join(A,meet(complement(A),B)),C),
inference(paramod,[status(thm)],[c_17110,c_55]) ).
cnf(c_29838,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_29837]) ).
cnf(c_29839,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_29838]) ).
cnf(c_29840,plain,
join(A,join(B,C)) = join(join(A,meet(complement(A),B)),C),
inference(paramod,[status(thm)],[c_587,c_29839]) ).
cnf(c_29841,plain,
join(A,join(B,C)) = join(A,join(meet(complement(A),B),C)),
inference(paramod,[status(thm)],[c_8,c_29840]) ).
cnf(c_17282,plain,
join(A,join(meet(complement(A),B),C)) = join(A,join(B,C)),
inference(copy,[status(thm)],[c_29841]) ).
cnf(c_29842,plain,
join(join(A,meet(complement(A),B)),meet(C,meet(D,B))) = join(A,meet(complement(A),B)),
inference(paramod,[status(thm)],[c_17110,c_115]) ).
cnf(c_29843,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_29842]) ).
cnf(c_29844,plain,
join(A,join(B,meet(C,meet(D,B)))) = join(A,meet(complement(A),B)),
inference(paramod,[status(thm)],[c_17282,c_29843]) ).
cnf(c_29845,plain,
join(A,B) = join(A,meet(complement(A),B)),
inference(paramod,[status(thm)],[c_54,c_29844]) ).
cnf(c_17284,plain,
join(A,meet(complement(A),B)) = join(A,B),
inference(copy,[status(thm)],[c_29845]) ).
cnf(c_29846,plain,
join(complement(A),join(meet(B,A),B)) = join(complement(A),meet(B,A)),
inference(paramod,[status(thm)],[c_17111,c_56]) ).
cnf(c_29847,plain,
join(complement(A),join(B,meet(B,A))) = join(complement(A),meet(B,A)),
inference(paramod,[status(thm)],[c_6,c_29846]) ).
cnf(c_29848,plain,
join(complement(A),B) = join(complement(A),meet(B,A)),
inference(paramod,[status(thm)],[c_4,c_29847]) ).
cnf(c_17338,plain,
join(complement(A),meet(B,A)) = join(complement(A),B),
inference(copy,[status(thm)],[c_29848]) ).
cnf(c_29849,plain,
join(join(meet(A,B),complement(B)),A) = join(meet(A,B),complement(B)),
inference(paramod,[status(thm)],[c_17114,c_16]) ).
cnf(c_29850,plain,
join(A,join(meet(A,B),complement(B))) = join(meet(A,B),complement(B)),
inference(paramod,[status(thm)],[c_6,c_29849]) ).
cnf(c_29851,plain,
join(A,complement(B)) = join(meet(A,B),complement(B)),
inference(paramod,[status(thm)],[c_31,c_29850]) ).
cnf(c_17381,plain,
join(meet(A,B),complement(B)) = join(A,complement(B)),
inference(copy,[status(thm)],[c_29851]) ).
cnf(c_29852,plain,
join(join(meet(A,B),complement(A)),B) = join(meet(A,B),complement(A)),
inference(paramod,[status(thm)],[c_17117,c_16]) ).
cnf(c_29853,plain,
join(B,join(meet(A,B),complement(A))) = join(meet(A,B),complement(A)),
inference(paramod,[status(thm)],[c_6,c_29852]) ).
cnf(c_29854,plain,
join(B,complement(A)) = join(meet(A,B),complement(A)),
inference(paramod,[status(thm)],[c_55,c_29853]) ).
cnf(c_17390,plain,
join(meet(A,B),complement(A)) = join(B,complement(A)),
inference(copy,[status(thm)],[c_29854]) ).
cnf(c_29855,plain,
join(complement(A),meet(complement(meet(A,B)),complement(complement(A)))) = complement(meet(A,B)),
inference(paramod,[status(thm)],[c_1526,c_17241]) ).
cnf(c_29856,plain,
join(complement(A),meet(complement(meet(A,B)),A)) = complement(meet(A,B)),
inference(paramod,[status(thm)],[c_340,c_29855]) ).
cnf(c_29857,plain,
join(complement(A),meet(A,complement(meet(A,B)))) = complement(meet(A,B)),
inference(paramod,[status(thm)],[c_5,c_29856]) ).
cnf(c_29858,plain,
join(complement(A),meet(complement(B),A)) = complement(meet(A,B)),
inference(paramod,[status(thm)],[c_16623,c_29857]) ).
cnf(c_29859,plain,
join(complement(A),complement(B)) = complement(meet(A,B)),
inference(paramod,[status(thm)],[c_17338,c_29858]) ).
cnf(c_17553,plain,
complement(meet(A,B)) = join(complement(A),complement(B)),
inference(copy,[status(thm)],[c_29859]) ).
cnf(c_21049,plain,
complement(join(complement(A),complement(B))) = meet(A,B),
inference(paramod,[status(thm)],[c_17553,c_340]) ).
cnf(c_21250,plain,
complement(join(A,complement(B))) = meet(complement(A),B),
inference(paramod,[status(thm)],[c_340,c_21049]) ).
cnf(c_21602,plain,
complement(join(A,B)) = meet(complement(A),complement(B)),
inference(paramod,[status(thm)],[c_340,c_21250]) ).
cnf(c_29860,plain,
meet(complement(join(A,B)),join(A,B)) = zero,
inference(paramod,[status(thm)],[c_210,c_73]) ).
cnf(c_29861,plain,
meet(meet(complement(A),complement(B)),join(A,B)) = zero,
inference(paramod,[status(thm)],[c_21602,c_29860]) ).
cnf(c_25795,plain,
meet(complement(A),meet(complement(B),join(A,B))) = zero,
inference(paramod,[status(thm)],[c_7,c_29861]) ).
cnf(c_29862,plain,
join(meet(A,B),complement(A)) = join(meet(B,join(C,A)),complement(A)),
inference(paramod,[status(thm)],[c_123,c_17390]) ).
cnf(c_29863,plain,
join(B,complement(A)) = join(meet(B,join(C,A)),complement(A)),
inference(paramod,[status(thm)],[c_17390,c_29862]) ).
cnf(c_25886,plain,
join(meet(A,join(B,C)),complement(C)) = join(A,complement(C)),
inference(copy,[status(thm)],[c_29863]) ).
cnf(c_29864,plain,
join(A,zero) = join(A,meet(complement(B),join(A,B))),
inference(paramod,[status(thm)],[c_25795,c_17284]) ).
cnf(c_29865,plain,
A = join(A,meet(complement(B),join(A,B))),
inference(paramod,[status(thm)],[c_37,c_29864]) ).
cnf(c_26592,plain,
join(A,meet(complement(B),join(A,B))) = A,
inference(copy,[status(thm)],[c_29865]) ).
cnf(c_29866,plain,
join(A,meet(complement(meet(B,complement(A))),join(A,B))) = A,
inference(paramod,[status(thm)],[c_17241,c_26592]) ).
cnf(c_29867,plain,
join(A,meet(join(complement(B),complement(complement(A))),join(A,B))) = A,
inference(paramod,[status(thm)],[c_17553,c_29866]) ).
cnf(c_29868,plain,
join(A,meet(join(complement(B),A),join(A,B))) = A,
inference(paramod,[status(thm)],[c_340,c_29867]) ).
cnf(c_26628,plain,
meet(join(complement(A),B),join(B,A)) = B,
inference(paramod,[status(thm)],[c_3055,c_29868]) ).
cnf(c_29869,plain,
meet(join(complement(join(A,B)),B),join(A,B)) = B,
inference(paramod,[status(thm)],[c_28,c_26628]) ).
cnf(c_29870,plain,
meet(join(meet(complement(A),complement(B)),B),join(A,B)) = B,
inference(paramod,[status(thm)],[c_21602,c_29869]) ).
cnf(c_29871,plain,
meet(join(B,meet(complement(A),complement(B))),join(A,B)) = B,
inference(paramod,[status(thm)],[c_6,c_29870]) ).
cnf(c_26848,plain,
meet(join(A,complement(B)),join(B,A)) = A,
inference(paramod,[status(thm)],[c_17241,c_29871]) ).
cnf(c_29872,plain,
meet(join(join(A,meet(B,C)),complement(C)),join(C,A)) = join(A,meet(B,C)),
inference(paramod,[status(thm)],[c_113,c_26848]) ).
cnf(c_29873,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_29872]) ).
cnf(c_28429,plain,
meet(join(A,join(B,complement(C))),join(C,A)) = join(A,meet(B,C)),
inference(paramod,[status(thm)],[c_17381,c_29873]) ).
cnf(c_29874,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_629,c_26848]) ).
cnf(c_29875,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_29874]) ).
cnf(c_29876,plain,
meet(join(A,join(B,complement(C))),join(C,A)) = join(A,meet(B,join(A,C))),
inference(paramod,[status(thm)],[c_25886,c_29875]) ).
cnf(c_29877,plain,
join(A,meet(B,C)) = join(A,meet(B,join(A,C))),
inference(paramod,[status(thm)],[c_28429,c_29876]) ).
cnf(c_28462,plain,
join(A,meet(B,join(A,C))) = join(A,meet(B,C)),
inference(copy,[status(thm)],[c_29877]) ).
cnf(c_28819,plain,
join(meet(A,B),meet(A,C)) = meet(A,join(meet(A,B),C)),
inference(paramod,[status(thm)],[c_28462,c_9929]) ).
cnf(c_28834,plain,
meet(A,join(B,meet(A,C))) = meet(A,join(B,C)),
inference(paramod,[status(thm)],[c_28462,c_466]) ).
cnf(c_29878,plain,
meet(a,join(meet(a,b),c)) != meet(a,join(b,c)),
inference(paramod,[status(thm)],[c_28819,c_15]) ).
cnf(c_29879,plain,
meet(a,join(c,meet(a,b))) != meet(a,join(b,c)),
inference(paramod,[status(thm)],[c_6,c_29878]) ).
cnf(c_29880,plain,
meet(a,join(c,b)) != meet(a,join(b,c)),
inference(paramod,[status(thm)],[c_28834,c_29879]) ).
cnf(c_29881,plain,
meet(a,join(b,c)) != meet(a,join(b,c)),
inference(paramod,[status(thm)],[c_6,c_29880]) ).
cnf(c_29745,plain,
$false,
inference(copy,[status(thm)],[c_29881]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LAT210-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.07/0.36 % Computer : n020.cluster.edu
% 0.07/0.36 % Model : x86_64 x86_64
% 0.07/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.36 % Memory : 8046.5625MB
% 0.07/0.36 % OS : Linux 6.8.0-71-generic
% 0.07/0.36 % CPULimit : 300
% 0.07/0.36 % WCLimit : 300
% 0.07/0.36 % DateTime : Fri Sep 25 20:17:04 UTC 2026
% 0.07/0.36 % CPUTime :
% 0.07/0.37 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.07/0.37 % Process 3672180 was started by sandbox on n020,
% 0.07/0.37 % Fri Sep 25 20:17:04 2026
% 0.07/0.37 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.07/0.37
% 0.07/0.37 % From the command line: assign(max_seconds, 300).
% 142.14/19.38
% 142.14/19.38 % given #500 (T,wt=10): 25565 meet(A,B) != zero | meet(B,A) = zero. [para(164(a,1),25523(a,1)),rewrite([164(6)])].
% 142.14/19.38
% 142.14/19.38 % SZS status Unsatisfiable for theBenchmark
% 142.14/19.38
% 142.14/19.38 % Proof 1 at 15.60 (+ 3.11) seconds.
% 142.14/19.38 % Length of proof is 115.
% 142.14/19.38 % Level of proof is 26.
% 142.14/19.38 % Maximum clause weight is 19.000.
% 142.14/19.38 % Given clauses 538.
% 142.14/19.38
% 142.14/19.38 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------