%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : LAT010-1 : TPTP v9.3.1. Released v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n007.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sun Sep 27 07:49:32 AM UTC 2026
% Result : Unsatisfiable 0.14s 0.84s
% Output : CNFRefutation 0.14s
% Verified :
% SZS Type : Refutation
% Derivation depth : 41
% Number of leaves : 12
% Syntax : Number of formulae : 136 ( 136 unt; 0 def)
% Number of atoms : 136 ( 135 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 18 ( 18 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 1 avg)
% Maximal term depth : 9 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 6 ( 6 usr; 4 con; 0-2 aty)
% Number of variables : 319 ( 21 sgn 27 !; 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(n5_1,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] : meet(VAR_0,join(VAR_1,meet(VAR_2,join(VAR_0,VAR_3)))) = join(meet(VAR_0,join(VAR_1,meet(VAR_0,VAR_2))),meet(VAR_0,join(meet(VAR_0,VAR_1),meet(VAR_2,VAR_3)))),
file('theBenchmark.p',n5_1) ).
cnf(c_9,plain,
meet(A,join(B,meet(C,join(A,D)))) = join(meet(A,join(B,meet(A,C))),meet(A,join(meet(A,B),meet(C,D)))),
inference(clausify,[status(thm)],[n5_1]) ).
cnf(c_10,plain,
join(meet(A,join(B,meet(A,C))),meet(A,join(meet(A,B),meet(C,D)))) = meet(A,join(B,meet(C,join(A,D)))),
inference(copy,[status(thm)],[c_9]) ).
fof(n5_2,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3] : join(VAR_0,meet(VAR_1,join(VAR_2,meet(VAR_0,VAR_3)))) = meet(join(VAR_0,meet(VAR_1,join(VAR_0,VAR_2))),join(VAR_0,meet(join(VAR_0,VAR_1),join(VAR_2,VAR_3)))),
file('theBenchmark.p',n5_2) ).
cnf(c_11,plain,
join(A,meet(B,join(C,meet(A,D)))) = meet(join(A,meet(B,join(A,C))),join(A,meet(join(A,B),join(C,D)))),
inference(clausify,[status(thm)],[n5_2]) ).
cnf(c_12,plain,
meet(join(A,meet(B,join(A,C))),join(A,meet(join(A,B),join(C,D)))) = join(A,meet(B,join(C,meet(A,D)))),
inference(copy,[status(thm)],[c_11]) ).
fof(nr_3,axiom,
! [VAR_0,VAR_1,VAR_2] : meet(join(VAR_0,meet(VAR_1,VAR_2)),join(VAR_2,meet(VAR_0,VAR_1))) = join(meet(VAR_2,join(VAR_0,meet(VAR_1,VAR_2))),meet(VAR_0,join(VAR_1,VAR_2))),
file('theBenchmark.p',nr_3) ).
cnf(c_13,plain,
meet(join(A,meet(B,C)),join(C,meet(A,B))) = join(meet(C,join(A,meet(B,C))),meet(A,join(B,C))),
inference(clausify,[status(thm)],[nr_3]) ).
cnf(c_769,plain,
meet(join(A,meet(B,C)),join(C,meet(A,B))) = join(meet(A,join(B,C)),meet(C,join(A,meet(B,C)))),
inference(paramod,[status(thm)],[c_6,c_13]) ).
cnf(c_14,plain,
join(meet(A,join(B,C)),meet(C,join(A,meet(B,C)))) = meet(join(A,meet(B,C)),join(C,meet(A,B))),
inference(copy,[status(thm)],[c_769]) ).
fof(prove_this,axiom,
meet(a,meet(join(b,c),join(b,d))) != meet(meet(a,meet(join(b,c),join(b,d))),join(meet(a,join(b,meet(c,d))),join(meet(a,c),meet(a,d)))),
file('theBenchmark.p',prove_this) ).
cnf(c_15,plain,
meet(a,meet(join(b,c),join(b,d))) != meet(meet(a,meet(join(b,c),join(b,d))),join(meet(a,join(b,meet(c,d))),join(meet(a,c),meet(a,d)))),
inference(clausify,[status(thm)],[prove_this]) ).
cnf(c_770,plain,
meet(a,meet(join(b,c),join(b,d))) != meet(a,meet(meet(join(b,c),join(b,d)),join(meet(a,join(b,meet(c,d))),join(meet(a,c),meet(a,d))))),
inference(paramod,[status(thm)],[c_7,c_15]) ).
cnf(c_771,plain,
meet(a,meet(join(b,c),join(b,d))) != meet(a,meet(join(b,c),meet(join(b,d),join(meet(a,join(b,meet(c,d))),join(meet(a,c),meet(a,d)))))),
inference(paramod,[status(thm)],[c_7,c_770]) ).
cnf(c_16,plain,
meet(a,meet(join(b,c),meet(join(b,d),join(meet(a,join(b,meet(c,d))),join(meet(a,c),meet(a,d)))))) != meet(a,meet(join(b,c),join(b,d))),
inference(copy,[status(thm)],[c_771]) ).
cnf(c_17,plain,
join(A,meet(B,A)) = A,
inference(paramod,[status(thm)],[c_5,c_4]) ).
cnf(c_18,plain,
meet(A,join(B,A)) = A,
inference(paramod,[status(thm)],[c_6,c_3]) ).
cnf(c_772,plain,
meet(A,B) = meet(A,meet(A,B)),
inference(paramod,[status(thm)],[c_1,c_7]) ).
cnf(c_20,plain,
meet(A,meet(A,B)) = meet(A,B),
inference(copy,[status(thm)],[c_772]) ).
cnf(c_773,plain,
meet(meet(A,B),B) = meet(A,B),
inference(paramod,[status(thm)],[c_1,c_7]) ).
cnf(c_21,plain,
meet(A,meet(B,A)) = meet(B,A),
inference(paramod,[status(thm)],[c_5,c_773]) ).
cnf(c_774,plain,
meet(A,B) = meet(A,meet(join(A,C),B)),
inference(paramod,[status(thm)],[c_3,c_7]) ).
cnf(c_23,plain,
meet(A,meet(join(A,B),C)) = meet(A,C),
inference(copy,[status(thm)],[c_774]) ).
cnf(c_24,plain,
join(meet(A,B),meet(A,meet(B,C))) = meet(A,B),
inference(paramod,[status(thm)],[c_7,c_4]) ).
cnf(c_775,plain,
meet(meet(A,B),C) = meet(B,meet(A,C)),
inference(paramod,[status(thm)],[c_5,c_7]) ).
cnf(c_26,plain,
meet(A,meet(B,C)) = meet(B,meet(A,C)),
inference(paramod,[status(thm)],[c_7,c_775]) ).
cnf(c_776,plain,
join(join(A,B),B) = join(A,B),
inference(paramod,[status(thm)],[c_2,c_8]) ).
cnf(c_29,plain,
join(A,join(B,A)) = join(B,A),
inference(paramod,[status(thm)],[c_6,c_776]) ).
cnf(c_33,plain,
join(A,join(B,C)) = join(C,join(A,B)),
inference(paramod,[status(thm)],[c_8,c_6]) ).
cnf(c_777,plain,
join(join(A,B),C) = join(B,join(A,C)),
inference(paramod,[status(thm)],[c_6,c_8]) ).
cnf(c_34,plain,
join(A,join(B,C)) = join(B,join(A,C)),
inference(paramod,[status(thm)],[c_8,c_777]) ).
cnf(c_778,plain,
meet(a,meet(join(b,c),meet(join(b,d),join(meet(a,d),join(meet(a,join(b,meet(c,d))),meet(a,c)))))) != meet(a,meet(join(b,c),join(b,d))),
inference(paramod,[status(thm)],[c_33,c_16]) ).
cnf(c_779,plain,
meet(a,meet(join(b,c),meet(join(b,d),join(meet(a,d),join(meet(a,c),meet(a,join(b,meet(c,d)))))))) != meet(a,meet(join(b,c),join(b,d))),
inference(paramod,[status(thm)],[c_6,c_778]) ).
cnf(c_35,plain,
meet(a,meet(join(b,c),meet(join(b,d),join(meet(a,c),join(meet(a,d),meet(a,join(b,meet(c,d)))))))) != meet(a,meet(join(b,c),join(b,d))),
inference(paramod,[status(thm)],[c_34,c_779]) ).
cnf(c_780,plain,
join(meet(A,meet(A,B)),meet(A,join(meet(A,meet(A,B)),meet(B,C)))) = meet(A,join(meet(A,B),meet(B,join(A,C)))),
inference(paramod,[status(thm)],[c_2,c_10]) ).
cnf(c_781,plain,
join(meet(A,B),meet(A,join(meet(A,meet(A,B)),meet(B,C)))) = meet(A,join(meet(A,B),meet(B,join(A,C)))),
inference(paramod,[status(thm)],[c_20,c_780]) ).
cnf(c_38,plain,
join(meet(A,B),meet(A,join(meet(A,B),meet(B,C)))) = meet(A,join(meet(A,B),meet(B,join(A,C)))),
inference(paramod,[status(thm)],[c_20,c_781]) ).
cnf(c_782,plain,
join(meet(A,join(B,meet(A,B))),meet(A,join(meet(A,B),meet(B,C)))) = meet(A,B),
inference(paramod,[status(thm)],[c_4,c_10]) ).
cnf(c_783,plain,
join(meet(A,B),meet(A,join(meet(A,B),meet(B,C)))) = meet(A,B),
inference(paramod,[status(thm)],[c_17,c_782]) ).
cnf(c_43,plain,
meet(A,join(meet(A,B),meet(B,join(A,C)))) = meet(A,B),
inference(paramod,[status(thm)],[c_38,c_783]) ).
cnf(c_55,plain,
join(meet(A,B),meet(A,join(meet(A,B),meet(B,C)))) = meet(A,B),
inference(paramod,[status(thm)],[c_43,c_38]) ).
cnf(c_784,plain,
join(join(A,B),meet(B,join(join(A,B),meet(A,B)))) = meet(join(join(A,B),meet(A,B)),join(B,meet(join(A,B),A))),
inference(paramod,[status(thm)],[c_1,c_14]) ).
cnf(c_785,plain,
join(join(A,B),meet(B,join(meet(A,B),join(A,B)))) = meet(join(join(A,B),meet(A,B)),join(B,meet(join(A,B),A))),
inference(paramod,[status(thm)],[c_6,c_784]) ).
cnf(c_786,plain,
join(join(A,B),meet(B,join(A,join(meet(A,B),B)))) = meet(join(join(A,B),meet(A,B)),join(B,meet(join(A,B),A))),
inference(paramod,[status(thm)],[c_34,c_785]) ).
cnf(c_787,plain,
join(join(A,B),meet(B,join(A,join(B,meet(A,B))))) = meet(join(join(A,B),meet(A,B)),join(B,meet(join(A,B),A))),
inference(paramod,[status(thm)],[c_6,c_786]) ).
cnf(c_788,plain,
join(join(A,B),meet(B,join(A,B))) = meet(join(join(A,B),meet(A,B)),join(B,meet(join(A,B),A))),
inference(paramod,[status(thm)],[c_17,c_787]) ).
cnf(c_789,plain,
join(join(A,B),B) = meet(join(join(A,B),meet(A,B)),join(B,meet(join(A,B),A))),
inference(paramod,[status(thm)],[c_18,c_788]) ).
cnf(c_790,plain,
join(B,join(A,B)) = meet(join(join(A,B),meet(A,B)),join(B,meet(join(A,B),A))),
inference(paramod,[status(thm)],[c_6,c_789]) ).
cnf(c_791,plain,
join(A,B) = meet(join(join(A,B),meet(A,B)),join(B,meet(join(A,B),A))),
inference(paramod,[status(thm)],[c_29,c_790]) ).
cnf(c_792,plain,
join(A,B) = meet(join(meet(A,B),join(A,B)),join(B,meet(join(A,B),A))),
inference(paramod,[status(thm)],[c_6,c_791]) ).
cnf(c_793,plain,
join(A,B) = meet(join(A,join(meet(A,B),B)),join(B,meet(join(A,B),A))),
inference(paramod,[status(thm)],[c_34,c_792]) ).
cnf(c_794,plain,
join(A,B) = meet(join(A,join(B,meet(A,B))),join(B,meet(join(A,B),A))),
inference(paramod,[status(thm)],[c_6,c_793]) ).
cnf(c_795,plain,
join(A,B) = meet(join(A,B),join(B,meet(join(A,B),A))),
inference(paramod,[status(thm)],[c_17,c_794]) ).
cnf(c_796,plain,
join(A,B) = meet(join(A,B),join(B,meet(A,join(A,B)))),
inference(paramod,[status(thm)],[c_5,c_795]) ).
cnf(c_797,plain,
join(A,B) = meet(join(A,B),join(B,A)),
inference(paramod,[status(thm)],[c_3,c_796]) ).
cnf(c_75,plain,
meet(join(A,B),join(B,A)) = join(A,B),
inference(copy,[status(thm)],[c_797]) ).
cnf(c_798,plain,
join(meet(A,join(meet(A,join(B,C)),meet(A,C))),meet(A,join(meet(A,meet(A,join(B,C))),meet(C,meet(B,C))))) = meet(A,meet(join(A,meet(B,C)),join(C,meet(A,B)))),
inference(paramod,[status(thm)],[c_14,c_10]) ).
cnf(c_799,plain,
join(meet(A,join(meet(A,C),meet(A,join(B,C)))),meet(A,join(meet(A,meet(A,join(B,C))),meet(C,meet(B,C))))) = meet(A,meet(join(A,meet(B,C)),join(C,meet(A,B)))),
inference(paramod,[status(thm)],[c_6,c_798]) ).
cnf(c_800,plain,
join(meet(A,join(meet(A,C),meet(A,join(B,C)))),meet(A,join(meet(A,join(B,C)),meet(C,meet(B,C))))) = meet(A,meet(join(A,meet(B,C)),join(C,meet(A,B)))),
inference(paramod,[status(thm)],[c_20,c_799]) ).
cnf(c_801,plain,
join(meet(A,join(meet(A,C),meet(A,join(B,C)))),meet(A,join(meet(A,join(B,C)),meet(B,C)))) = meet(A,meet(join(A,meet(B,C)),join(C,meet(A,B)))),
inference(paramod,[status(thm)],[c_21,c_800]) ).
cnf(c_802,plain,
join(meet(A,join(meet(A,C),meet(A,join(B,C)))),meet(A,join(meet(B,C),meet(A,join(B,C))))) = meet(A,meet(join(A,meet(B,C)),join(C,meet(A,B)))),
inference(paramod,[status(thm)],[c_6,c_801]) ).
cnf(c_92,plain,
join(meet(A,join(meet(A,B),meet(A,join(C,B)))),meet(A,join(meet(C,B),meet(A,join(C,B))))) = meet(A,join(B,meet(A,C))),
inference(paramod,[status(thm)],[c_23,c_802]) ).
cnf(c_105,plain,
meet(A,join(B,join(C,A))) = A,
inference(paramod,[status(thm)],[c_8,c_18]) ).
cnf(c_803,plain,
meet(join(A,join(B,A)),join(A,meet(join(A,join(B,A)),join(B,C)))) = join(A,meet(join(B,A),join(B,meet(A,C)))),
inference(paramod,[status(thm)],[c_75,c_12]) ).
cnf(c_804,plain,
meet(join(B,A),join(A,meet(join(A,join(B,A)),join(B,C)))) = join(A,meet(join(B,A),join(B,meet(A,C)))),
inference(paramod,[status(thm)],[c_29,c_803]) ).
cnf(c_118,plain,
meet(join(A,B),join(B,meet(join(A,B),join(A,C)))) = join(B,meet(join(A,B),join(A,meet(B,C)))),
inference(paramod,[status(thm)],[c_29,c_804]) ).
cnf(c_805,plain,
meet(A,meet(B,meet(C,A))) = meet(meet(B,C),A),
inference(paramod,[status(thm)],[c_7,c_21]) ).
cnf(c_130,plain,
meet(A,meet(B,meet(C,A))) = meet(B,meet(C,A)),
inference(paramod,[status(thm)],[c_7,c_805]) ).
cnf(c_806,plain,
join(A,meet(join(B,A),join(A,meet(C,join(B,A))))) = meet(join(A,meet(C,join(B,A))),join(join(B,A),meet(A,C))),
inference(paramod,[status(thm)],[c_105,c_14]) ).
cnf(c_807,plain,
join(A,meet(join(B,A),join(A,meet(C,join(B,A))))) = meet(join(A,meet(C,join(B,A))),join(B,join(A,meet(A,C)))),
inference(paramod,[status(thm)],[c_8,c_806]) ).
cnf(c_808,plain,
join(A,meet(join(B,A),join(A,meet(C,join(B,A))))) = meet(join(A,meet(C,join(B,A))),join(B,A)),
inference(paramod,[status(thm)],[c_4,c_807]) ).
cnf(c_197,plain,
join(A,meet(join(B,A),join(A,meet(C,join(B,A))))) = meet(join(B,A),join(A,meet(C,join(B,A)))),
inference(paramod,[status(thm)],[c_5,c_808]) ).
cnf(c_809,plain,
meet(A,meet(join(A,B),meet(C,A))) = meet(C,A),
inference(paramod,[status(thm)],[c_21,c_23]) ).
cnf(c_211,plain,
meet(join(A,B),meet(C,A)) = meet(C,A),
inference(paramod,[status(thm)],[c_130,c_809]) ).
cnf(c_221,plain,
meet(join(A,B),meet(C,B)) = meet(C,B),
inference(paramod,[status(thm)],[c_6,c_211]) ).
cnf(c_810,plain,
join(meet(join(A,B),C),meet(C,A)) = meet(join(A,B),C),
inference(paramod,[status(thm)],[c_211,c_24]) ).
cnf(c_250,plain,
join(meet(A,B),meet(join(B,C),A)) = meet(join(B,C),A),
inference(paramod,[status(thm)],[c_6,c_810]) ).
cnf(c_299,plain,
join(meet(A,B),meet(A,join(B,C))) = meet(join(B,C),A),
inference(paramod,[status(thm)],[c_5,c_250]) ).
cnf(c_811,plain,
join(meet(A,B),meet(join(meet(A,B),C),A)) = meet(join(meet(A,B),C),A),
inference(paramod,[status(thm)],[c_20,c_250]) ).
cnf(c_812,plain,
join(meet(A,B),meet(A,join(meet(A,B),C))) = meet(join(meet(A,B),C),A),
inference(paramod,[status(thm)],[c_5,c_811]) ).
cnf(c_311,plain,
join(meet(A,B),meet(A,join(meet(A,B),C))) = meet(A,join(meet(A,B),C)),
inference(paramod,[status(thm)],[c_5,c_812]) ).
cnf(c_322,plain,
meet(A,join(meet(A,B),meet(B,C))) = meet(A,B),
inference(paramod,[status(thm)],[c_311,c_55]) ).
cnf(c_348,plain,
meet(A,join(meet(B,C),meet(A,B))) = meet(A,B),
inference(paramod,[status(thm)],[c_6,c_322]) ).
cnf(c_520,plain,
meet(A,join(meet(B,C),meet(A,join(D,C)))) = meet(A,join(D,C)),
inference(paramod,[status(thm)],[c_221,c_348]) ).
cnf(c_813,plain,
join(meet(A,join(C,B)),meet(A,join(meet(C,B),meet(A,join(C,B))))) = meet(A,join(B,meet(A,C))),
inference(paramod,[status(thm)],[c_520,c_92]) ).
cnf(c_814,plain,
join(meet(A,join(C,B)),meet(A,join(C,B))) = meet(A,join(B,meet(A,C))),
inference(paramod,[status(thm)],[c_520,c_813]) ).
cnf(c_815,plain,
meet(A,join(C,B)) = meet(A,join(B,meet(A,C))),
inference(paramod,[status(thm)],[c_2,c_814]) ).
cnf(c_532,plain,
meet(A,join(B,meet(A,C))) = meet(A,join(C,B)),
inference(copy,[status(thm)],[c_815]) ).
cnf(c_816,plain,
meet(join(A,B),join(join(A,C),B)) = join(B,meet(join(A,B),join(A,meet(B,C)))),
inference(paramod,[status(thm)],[c_532,c_118]) ).
cnf(c_817,plain,
meet(join(A,B),join(A,join(C,B))) = join(B,meet(join(A,B),join(A,meet(B,C)))),
inference(paramod,[status(thm)],[c_8,c_816]) ).
cnf(c_561,plain,
join(A,meet(join(B,A),join(B,meet(A,C)))) = meet(join(B,A),join(B,join(C,A))),
inference(copy,[status(thm)],[c_817]) ).
cnf(c_607,plain,
meet(A,join(B,meet(C,A))) = meet(A,join(C,B)),
inference(paramod,[status(thm)],[c_5,c_532]) ).
cnf(c_818,plain,
join(join(A,meet(B,C)),meet(B,join(C,A))) = join(A,meet(B,C)),
inference(paramod,[status(thm)],[c_532,c_17]) ).
cnf(c_819,plain,
join(meet(B,join(C,A)),join(A,meet(B,C))) = join(A,meet(B,C)),
inference(paramod,[status(thm)],[c_6,c_818]) ).
cnf(c_820,plain,
join(A,join(meet(B,join(C,A)),meet(B,C))) = join(A,meet(B,C)),
inference(paramod,[status(thm)],[c_34,c_819]) ).
cnf(c_821,plain,
join(A,join(meet(B,C),meet(B,join(C,A)))) = join(A,meet(B,C)),
inference(paramod,[status(thm)],[c_6,c_820]) ).
cnf(c_616,plain,
join(A,meet(join(B,A),C)) = join(A,meet(C,B)),
inference(paramod,[status(thm)],[c_299,c_821]) ).
cnf(c_822,plain,
join(A,meet(join(B,A),join(C,A))) = meet(join(B,A),join(A,meet(C,join(B,A)))),
inference(paramod,[status(thm)],[c_607,c_197]) ).
cnf(c_823,plain,
join(A,meet(join(C,A),B)) = meet(join(B,A),join(A,meet(C,join(B,A)))),
inference(paramod,[status(thm)],[c_616,c_822]) ).
cnf(c_824,plain,
join(A,meet(B,C)) = meet(join(B,A),join(A,meet(C,join(B,A)))),
inference(paramod,[status(thm)],[c_616,c_823]) ).
cnf(c_825,plain,
join(A,meet(B,C)) = meet(join(B,A),join(C,A)),
inference(paramod,[status(thm)],[c_607,c_824]) ).
cnf(c_640,plain,
meet(join(A,B),join(C,B)) = join(B,meet(A,C)),
inference(copy,[status(thm)],[c_825]) ).
cnf(c_826,plain,
join(A,meet(join(B,meet(A,C)),B)) = meet(join(B,A),join(B,join(C,A))),
inference(paramod,[status(thm)],[c_616,c_561]) ).
cnf(c_827,plain,
join(A,meet(B,join(B,meet(A,C)))) = meet(join(B,A),join(B,join(C,A))),
inference(paramod,[status(thm)],[c_5,c_826]) ).
cnf(c_828,plain,
join(A,B) = meet(join(B,A),join(B,join(C,A))),
inference(paramod,[status(thm)],[c_3,c_827]) ).
cnf(c_689,plain,
meet(join(A,B),join(A,join(C,B))) = join(B,A),
inference(copy,[status(thm)],[c_828]) ).
cnf(c_829,plain,
meet(A,join(B,meet(A,C))) = join(meet(A,C),meet(A,B)),
inference(paramod,[status(thm)],[c_4,c_640]) ).
cnf(c_830,plain,
meet(A,join(C,B)) = join(meet(A,C),meet(A,B)),
inference(paramod,[status(thm)],[c_532,c_829]) ).
cnf(c_723,plain,
join(meet(A,B),meet(A,C)) = meet(A,join(B,C)),
inference(copy,[status(thm)],[c_830]) ).
cnf(c_831,plain,
meet(a,meet(join(b,c),meet(join(b,d),join(meet(a,c),meet(a,join(d,join(b,meet(c,d)))))))) != meet(a,meet(join(b,c),join(b,d))),
inference(paramod,[status(thm)],[c_723,c_35]) ).
cnf(c_832,plain,
meet(a,meet(join(b,c),meet(join(b,d),join(meet(a,c),meet(a,join(b,join(d,meet(c,d)))))))) != meet(a,meet(join(b,c),join(b,d))),
inference(paramod,[status(thm)],[c_34,c_831]) ).
cnf(c_833,plain,
meet(a,meet(join(b,c),meet(join(b,d),join(meet(a,c),meet(a,join(b,d)))))) != meet(a,meet(join(b,c),join(b,d))),
inference(paramod,[status(thm)],[c_17,c_832]) ).
cnf(c_834,plain,
meet(a,meet(join(b,c),meet(join(b,d),meet(a,join(c,join(b,d)))))) != meet(a,meet(join(b,c),join(b,d))),
inference(paramod,[status(thm)],[c_723,c_833]) ).
cnf(c_835,plain,
meet(a,meet(join(b,c),meet(join(b,d),meet(a,join(b,join(c,d)))))) != meet(a,meet(join(b,c),join(b,d))),
inference(paramod,[status(thm)],[c_34,c_834]) ).
cnf(c_836,plain,
meet(a,meet(join(b,c),meet(a,meet(join(b,d),join(b,join(c,d)))))) != meet(a,meet(join(b,c),join(b,d))),
inference(paramod,[status(thm)],[c_26,c_835]) ).
cnf(c_837,plain,
meet(a,meet(join(b,c),meet(a,join(d,b)))) != meet(a,meet(join(b,c),join(b,d))),
inference(paramod,[status(thm)],[c_689,c_836]) ).
cnf(c_838,plain,
meet(a,meet(join(b,c),meet(a,join(b,d)))) != meet(a,meet(join(b,c),join(b,d))),
inference(paramod,[status(thm)],[c_6,c_837]) ).
cnf(c_839,plain,
meet(a,meet(a,meet(join(b,c),join(b,d)))) != meet(a,meet(join(b,c),join(b,d))),
inference(paramod,[status(thm)],[c_26,c_838]) ).
cnf(c_840,plain,
meet(a,meet(join(b,c),join(b,d))) != meet(a,meet(join(b,c),join(b,d))),
inference(paramod,[status(thm)],[c_20,c_839]) ).
cnf(c_768,plain,
$false,
inference(copy,[status(thm)],[c_840]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT010-1 : TPTP v9.3.1. Released v2.2.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.58 % Computer : n007.cluster.edu
% 0.09/0.58 % Model : x86_64 x86_64
% 0.09/0.58 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.58 % Memory : 8046.5625MB
% 0.09/0.58 % OS : Linux 6.8.0-71-generic
% 0.09/0.58 % CPULimit : 300
% 0.09/0.58 % WCLimit : 300
% 0.09/0.58 % DateTime : Fri Sep 25 19:54:24 UTC 2026
% 0.09/0.58 % CPUTime :
% 0.09/0.59 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.09/0.59 % Process 1736221 was started by sandbox2 on n007,
% 0.09/0.59 % Fri Sep 25 19:54:24 2026
% 0.09/0.59 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.09/0.59
% 0.09/0.59 % From the command line: assign(max_seconds, 300).
% 0.14/0.84
% 0.14/0.84 % SZS status Unsatisfiable for theBenchmark
% 0.14/0.84
% 0.14/0.84 % Proof 1 at 0.19 (+ 0.05) seconds.
% 0.14/0.84 % Length of proof is 52.
% 0.14/0.84 % Level of proof is 13.
% 0.14/0.84 % Maximum clause weight is 100.000.
% 0.14/0.84 % Given clauses 42.
% 0.14/0.84
% 0.14/0.84 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------