%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : LAT020-1 : TPTP v9.3.1. Released v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n009.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 01:55:01 PM UTC 2026
% Result : Unsatisfiable 29.15s 9.52s
% Output : CNFRefutation 29.15s
% Verified :
% SZS Type : Refutation
% Derivation depth : 127
% Number of leaves : 10
% Syntax : Number of clauses : 582 ( 582 unt; 0 nHn; 3 RR)
% Number of literals : 582 ( 581 equ; 2 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 5 ( 5 usr; 3 con; 0-2 aty)
% Number of variables : 1849 ( 0 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t6,axiom,
join(meet(X1,join(X2,X3)),meet(X1,X2)) = meet(X1,join(X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t2,axiom,
join(X1,X2) = join(X2,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t11,plain,
join(X1,X2) = join(X2,X1),
inference(orient,[status(thm)],[t2]) ).
cnf(t89727,plain,
join(meet(X1,X2),meet(X1,join(X2,X3))) = meet(X1,join(X2,X3)),
inference(step,[status(thm)],[t6,t11]) ).
cnf(t33,plain,
join(meet(X1,X2),meet(X1,join(X2,X3))) = meet(X1,join(X2,X3)),
inference(orient,[status(thm)],[t89727]) ).
cnf(t1,axiom,
meet(X1,X1) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t10,plain,
meet(X1,X1) = X1,
inference(orient,[status(thm)],[t1]) ).
cnf(t36,plain,
meet(join(X1,X2),join(X1,X2)) = join(meet(join(X1,X2),X1),join(X1,X2)),
inference(cp,[status(thm)],[t33,t10]) ).
cnf(t89737,plain,
join(X1,X2) = join(meet(join(X1,X2),X1),join(X1,X2)),
inference(step,[status(thm)],[t36,t10]) ).
cnf(t4,axiom,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t89726,plain,
join(X3,join(X1,X2)) = join(X1,join(X2,X3)),
inference(step,[status(thm)],[t4,t11]) ).
cnf(t12,plain,
join(X1,join(X2,X3)) = join(X2,join(X3,X1)),
inference(orient,[status(thm)],[t89726]) ).
cnf(t89738,plain,
join(X1,X2) = join(X2,join(meet(join(X1,X2),X1),X1)),
inference(step,[status(thm)],[t89737,t12]) ).
cnf(t89739,plain,
join(X1,X2) = join(X1,join(X2,meet(join(X1,X2),X1))),
inference(step,[status(thm)],[t89738,t12]) ).
cnf(t3,axiom,
meet(X1,X2) = meet(X2,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t61,plain,
meet(X1,X2) = meet(X2,X1),
inference(orient,[status(thm)],[t3]) ).
cnf(t89740,plain,
join(X1,X2) = join(X1,join(X2,meet(X1,join(X1,X2)))),
inference(step,[status(thm)],[t89739,t61]) ).
cnf(t107,plain,
join(X1,join(X2,meet(X1,join(X1,X2)))) = join(X1,X2),
inference(orient,[status(thm)],[t89740]) ).
cnf(t34,plain,
meet(X1,join(X1,X2)) = join(X1,meet(X1,join(X1,X2))),
inference(cp,[status(thm)],[t33,t10]) ).
cnf(t99,plain,
join(X1,meet(X1,join(X1,X2))) = meet(X1,join(X1,X2)),
inference(orient,[status(thm)],[t34]) ).
cnf(t105,plain,
join(X1,join(meet(X1,join(X1,X2)),X3)) = join(X3,meet(X1,join(X1,X2))),
inference(cp,[status(thm)],[t12,t99]) ).
cnf(t89746,plain,
join(X1,join(X3,meet(X1,join(X1,X2)))) = join(X3,meet(X1,join(X1,X2))),
inference(step,[status(thm)],[t105,t11]) ).
cnf(t159,plain,
join(X1,join(X2,meet(X1,join(X1,X3)))) = join(X2,meet(X1,join(X1,X3))),
inference(orient,[status(thm)],[t89746]) ).
cnf(t89747,plain,
join(X2,meet(X1,join(X1,X2))) = join(X1,X2),
inference(step,[status(thm)],[t107,t159]) ).
cnf(t174,plain,
join(X2,meet(X1,join(X1,X2))) = join(X1,X2),
inference(rw,[status(thm)],[t89747]) ).
cnf(t175,plain,
join(X1,meet(X2,join(X2,X1))) = join(X2,X1),
inference(orient,[status(thm)],[t174]) ).
cnf(t7,axiom,
meet(join(X1,meet(X2,X3)),join(X1,X2)) = join(X1,meet(X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t26,plain,
meet(join(X1,meet(X2,X3)),join(X1,X2)) = join(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t7]) ).
cnf(t64,plain,
meet(join(X1,meet(X2,X3)),join(X1,X2)) = join(X1,meet(X2,X3)),
inference(rw,[status(thm)],[t26]) ).
cnf(t89741,plain,
meet(join(X1,X2),join(X1,meet(X2,X3))) = join(X1,meet(X2,X3)),
inference(step,[status(thm)],[t64,t61]) ).
cnf(t117,plain,
meet(join(X1,X2),join(X1,meet(X2,X3))) = join(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t89741]) ).
cnf(t127,plain,
join(meet(X1,X2),meet(X1,join(X2,X3))) = meet(join(meet(X1,X2),X1),meet(X1,join(X2,X3))),
inference(cp,[status(thm)],[t117,t33]) ).
cnf(t89823,plain,
meet(X1,join(X2,X3)) = meet(join(meet(X1,X2),X1),meet(X1,join(X2,X3))),
inference(step,[status(thm)],[t127,t33]) ).
cnf(t5,axiom,
meet(meet(X1,X2),X3) = meet(X1,meet(X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t89732,plain,
meet(X3,meet(X1,X2)) = meet(X1,meet(X2,X3)),
inference(step,[status(thm)],[t5,t61]) ).
cnf(t66,plain,
meet(X1,meet(X2,X3)) = meet(X2,meet(X3,X1)),
inference(orient,[status(thm)],[t89732]) ).
cnf(t89824,plain,
meet(X1,join(X2,X3)) = meet(join(X2,X3),meet(join(meet(X1,X2),X1),X1)),
inference(step,[status(thm)],[t89823,t66]) ).
cnf(t89825,plain,
meet(X1,join(X2,X3)) = meet(X1,meet(join(X2,X3),join(meet(X1,X2),X1))),
inference(step,[status(thm)],[t89824,t66]) ).
cnf(t89826,plain,
meet(X1,join(X2,X3)) = meet(X1,meet(join(X2,X3),join(X1,meet(X1,X2)))),
inference(step,[status(thm)],[t89825,t11]) ).
cnf(t0,axiom,
join(X1,X1) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t9,plain,
join(X1,X1) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t118,plain,
join(X1,meet(X1,X2)) = meet(X1,join(X1,meet(X1,X2))),
inference(cp,[status(thm)],[t117,t9]) ).
cnf(t137,plain,
meet(X1,join(X1,meet(X1,X2))) = join(X1,meet(X1,X2)),
inference(orient,[status(thm)],[t118]) ).
cnf(t145,plain,
meet(X1,meet(join(X1,meet(X1,X2)),X3)) = meet(X3,join(X1,meet(X1,X2))),
inference(cp,[status(thm)],[t66,t137]) ).
cnf(t89777,plain,
meet(X1,meet(X3,join(X1,meet(X1,X2)))) = meet(X3,join(X1,meet(X1,X2))),
inference(step,[status(thm)],[t145,t61]) ).
cnf(t423,plain,
meet(X1,meet(X2,join(X1,meet(X1,X3)))) = meet(X2,join(X1,meet(X1,X3))),
inference(orient,[status(thm)],[t89777]) ).
cnf(t89827,plain,
meet(X1,join(X2,X3)) = meet(join(X2,X3),join(X1,meet(X1,X2))),
inference(step,[status(thm)],[t89826,t423]) ).
cnf(t1188,plain,
meet(join(X1,X2),join(X3,meet(X3,X1))) = meet(X3,join(X1,X2)),
inference(orient,[status(thm)],[t89827]) ).
cnf(t1192,plain,
meet(X1,join(X2,meet(X3,join(X3,X2)))) = meet(join(X3,X2),join(X1,meet(X1,X2))),
inference(cp,[status(thm)],[t1188,t175]) ).
cnf(t89828,plain,
meet(X1,join(X3,X2)) = meet(join(X3,X2),join(X1,meet(X1,X2))),
inference(step,[status(thm)],[t1192,t175]) ).
cnf(t1259,plain,
meet(join(X1,X2),join(X3,meet(X3,X2))) = meet(X3,join(X1,X2)),
inference(orient,[status(thm)],[t89828]) ).
cnf(t126,plain,
join(meet(X1,X2),meet(X1,X2)) = meet(join(meet(X1,X2),X1),meet(X1,X2)),
inference(cp,[status(thm)],[t117,t9]) ).
cnf(t89742,plain,
meet(X1,X2) = meet(join(meet(X1,X2),X1),meet(X1,X2)),
inference(step,[status(thm)],[t126,t9]) ).
cnf(t89743,plain,
meet(X1,X2) = meet(X2,meet(join(meet(X1,X2),X1),X1)),
inference(step,[status(thm)],[t89742,t66]) ).
cnf(t89744,plain,
meet(X1,X2) = meet(X1,meet(X2,join(meet(X1,X2),X1))),
inference(step,[status(thm)],[t89743,t66]) ).
cnf(t89745,plain,
meet(X1,X2) = meet(X1,meet(X2,join(X1,meet(X1,X2)))),
inference(step,[status(thm)],[t89744,t11]) ).
cnf(t147,plain,
meet(X1,meet(X2,join(X1,meet(X1,X2)))) = meet(X1,X2),
inference(orient,[status(thm)],[t89745]) ).
cnf(t89778,plain,
meet(X2,join(X1,meet(X1,X2))) = meet(X1,X2),
inference(step,[status(thm)],[t147,t423]) ).
cnf(t442,plain,
meet(X2,join(X1,meet(X1,X2))) = meet(X1,X2),
inference(rw,[status(thm)],[t89778]) ).
cnf(t443,plain,
meet(X1,join(X2,meet(X2,X1))) = meet(X2,X1),
inference(orient,[status(thm)],[t442]) ).
cnf(t459,plain,
join(X1,meet(X2,join(X3,meet(X3,X2)))) = meet(join(X1,X2),join(X1,meet(X3,X2))),
inference(cp,[status(thm)],[t117,t443]) ).
cnf(t89786,plain,
join(X1,meet(X3,X2)) = meet(join(X1,X2),join(X1,meet(X3,X2))),
inference(step,[status(thm)],[t459,t443]) ).
cnf(t534,plain,
meet(join(X1,X2),join(X1,meet(X3,X2))) = join(X1,meet(X3,X2)),
inference(orient,[status(thm)],[t89786]) ).
cnf(t1260,plain,
meet(X1,join(X1,X2)) = join(X1,meet(X1,X2)),
inference(cp,[status(thm)],[t1259,t534]) ).
cnf(t1337,plain,
join(X1,meet(X1,X2)) = meet(X1,join(X1,X2)),
inference(orient,[status(thm)],[t1260]) ).
cnf(t89830,plain,
meet(join(X1,X2),meet(X3,join(X3,X1))) = meet(X3,join(X1,X2)),
inference(step,[status(thm)],[t1188,t1337]) ).
cnf(t1376,plain,
meet(join(X1,X2),meet(X3,join(X3,X1))) = meet(X3,join(X1,X2)),
inference(rw,[status(thm)],[t89830]) ).
cnf(t89842,plain,
meet(X3,meet(join(X3,X1),join(X1,X2))) = meet(X3,join(X1,X2)),
inference(step,[status(thm)],[t1376,t66]) ).
cnf(t89843,plain,
meet(X3,meet(join(X1,X2),join(X3,X1))) = meet(X3,join(X1,X2)),
inference(step,[status(thm)],[t89842,t61]) ).
cnf(t89844,plain,
meet(X3,meet(join(X1,X2),join(X1,X3))) = meet(X3,join(X1,X2)),
inference(step,[status(thm)],[t89843,t11]) ).
cnf(t1521,plain,
meet(X1,meet(join(X2,X3),join(X2,X1))) = meet(X1,join(X2,X3)),
inference(orient,[status(thm)],[t89844]) ).
cnf(t191,plain,
join(meet(X1,join(X1,X2)),join(X3,X2)) = join(X3,join(X1,X2)),
inference(cp,[status(thm)],[t12,t175]) ).
cnf(t89764,plain,
join(X2,join(meet(X1,join(X1,X2)),X3)) = join(X3,join(X1,X2)),
inference(step,[status(thm)],[t191,t12]) ).
cnf(t89765,plain,
join(X2,join(X3,meet(X1,join(X1,X2)))) = join(X3,join(X1,X2)),
inference(step,[status(thm)],[t89764,t11]) ).
cnf(t89766,plain,
join(X2,join(X3,meet(X1,join(X1,X2)))) = join(X2,join(X3,X1)),
inference(step,[status(thm)],[t89765,t12]) ).
cnf(t89767,plain,
join(X2,join(X3,meet(X1,join(X1,X2)))) = join(X1,join(X2,X3)),
inference(step,[status(thm)],[t89766,t12]) ).
cnf(t334,plain,
join(X1,join(X2,meet(X3,join(X3,X1)))) = join(X3,join(X1,X2)),
inference(orient,[status(thm)],[t89767]) ).
cnf(t1530,plain,
meet(X1,join(X2,join(X3,meet(Y3,join(Y3,X2))))) = meet(X1,meet(join(Y3,join(X2,X3)),join(X2,X1))),
inference(cp,[status(thm)],[t1521,t334]) ).
cnf(t10010,plain,
meet(X1,meet(join(X1,X2),join(X3,join(X2,Y3)))) = meet(X1,join(X3,join(X2,Y3))),
inference(orient,[status(thm)],[t1530]) ).
cnf(t133,plain,
meet(join(X1,X2),join(X1,meet(X2,X3))) = join(meet(join(X1,X2),X1),join(X1,meet(X2,X3))),
inference(cp,[status(thm)],[t33,t117]) ).
cnf(t89858,plain,
join(X1,meet(X2,X3)) = join(meet(join(X1,X2),X1),join(X1,meet(X2,X3))),
inference(step,[status(thm)],[t133,t117]) ).
cnf(t89859,plain,
join(X1,meet(X2,X3)) = join(meet(X2,X3),join(meet(join(X1,X2),X1),X1)),
inference(step,[status(thm)],[t89858,t12]) ).
cnf(t89860,plain,
join(X1,meet(X2,X3)) = join(X1,join(meet(X2,X3),meet(join(X1,X2),X1))),
inference(step,[status(thm)],[t89859,t12]) ).
cnf(t89861,plain,
join(X1,meet(X2,X3)) = join(X1,join(meet(X2,X3),meet(X1,join(X1,X2)))),
inference(step,[status(thm)],[t89860,t61]) ).
cnf(t89862,plain,
join(X1,meet(X2,X3)) = join(meet(X2,X3),meet(X1,join(X1,X2))),
inference(step,[status(thm)],[t89861,t159]) ).
cnf(t2374,plain,
join(meet(X1,X2),meet(X3,join(X3,X1))) = join(X3,meet(X1,X2)),
inference(orient,[status(thm)],[t89862]) ).
cnf(t3053,plain,
join(meet(X1,X2),meet(X3,join(X3,X1))) = join(X3,meet(X1,X2)),
inference(rw,[status(thm)],[t2374]) ).
cnf(t1373,plain,
join(X1,join(meet(X1,X2),X3)) = join(X3,meet(X1,join(X1,X2))),
inference(cp,[status(thm)],[t12,t1337]) ).
cnf(t89868,plain,
join(X1,join(X3,meet(X1,X2))) = join(X3,meet(X1,join(X1,X2))),
inference(step,[status(thm)],[t1373,t11]) ).
cnf(t2881,plain,
join(X1,join(X2,meet(X1,X3))) = join(X2,meet(X1,join(X1,X3))),
inference(orient,[status(thm)],[t89868]) ).
cnf(t89871,plain,
join(X3,join(meet(X1,X2),meet(X3,X1))) = join(X3,meet(X1,X2)),
inference(step,[status(thm)],[t3053,t2881]) ).
cnf(t89872,plain,
join(X3,join(meet(X1,X2),meet(X1,X3))) = join(X3,meet(X1,X2)),
inference(step,[status(thm)],[t89871,t61]) ).
cnf(t3167,plain,
join(X1,join(meet(X2,X3),meet(X2,X1))) = join(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t89872]) ).
cnf(t3169,plain,
join(join(X1,X2),meet(X3,X1)) = join(join(X1,X2),meet(X3,join(X1,X2))),
inference(cp,[status(thm)],[t3167,t33]) ).
cnf(t89876,plain,
join(meet(X3,X1),join(X1,X2)) = join(join(X1,X2),meet(X3,join(X1,X2))),
inference(step,[status(thm)],[t3169,t11]) ).
cnf(t89877,plain,
join(X2,join(meet(X3,X1),X1)) = join(join(X1,X2),meet(X3,join(X1,X2))),
inference(step,[status(thm)],[t89876,t12]) ).
cnf(t89878,plain,
join(X1,join(X2,meet(X3,X1))) = join(join(X1,X2),meet(X3,join(X1,X2))),
inference(step,[status(thm)],[t89877,t12]) ).
cnf(t89879,plain,
join(X1,join(X2,meet(X1,X3))) = join(join(X1,X2),meet(X3,join(X1,X2))),
inference(step,[status(thm)],[t89878,t61]) ).
cnf(t3512,plain,
join(join(X1,X2),meet(X3,join(X1,X2))) = join(X1,join(X2,meet(X1,X3))),
inference(orient,[status(thm)],[t89879]) ).
cnf(t3553,plain,
join(X1,join(X2,meet(X1,X3))) = join(join(X1,X2),meet(join(X1,X2),X3)),
inference(cp,[status(thm)],[t3512,t61]) ).
cnf(t184,plain,
meet(X1,join(X2,meet(X3,join(X3,X2)))) = join(meet(X1,X2),meet(X1,join(X3,X2))),
inference(cp,[status(thm)],[t33,t175]) ).
cnf(t89755,plain,
meet(X1,join(X3,X2)) = join(meet(X1,X2),meet(X1,join(X3,X2))),
inference(step,[status(thm)],[t184,t175]) ).
cnf(t243,plain,
join(meet(X1,X2),meet(X1,join(X3,X2))) = meet(X1,join(X3,X2)),
inference(orient,[status(thm)],[t89755]) ).
cnf(t3170,plain,
join(join(X1,X2),meet(X3,X2)) = join(join(X1,X2),meet(X3,join(X1,X2))),
inference(cp,[status(thm)],[t3167,t243]) ).
cnf(t89888,plain,
join(meet(X3,X2),join(X1,X2)) = join(join(X1,X2),meet(X3,join(X1,X2))),
inference(step,[status(thm)],[t3170,t11]) ).
cnf(t89889,plain,
join(X2,join(meet(X3,X2),X1)) = join(join(X1,X2),meet(X3,join(X1,X2))),
inference(step,[status(thm)],[t89888,t12]) ).
cnf(t89890,plain,
join(X1,join(X2,meet(X3,X2))) = join(join(X1,X2),meet(X3,join(X1,X2))),
inference(step,[status(thm)],[t89889,t12]) ).
cnf(t89891,plain,
join(X1,join(X2,meet(X2,X3))) = join(join(X1,X2),meet(X3,join(X1,X2))),
inference(step,[status(thm)],[t89890,t61]) ).
cnf(t89892,plain,
join(X1,meet(X2,join(X2,X3))) = join(join(X1,X2),meet(X3,join(X1,X2))),
inference(step,[status(thm)],[t89891,t1337]) ).
cnf(t89893,plain,
join(X1,meet(X2,join(X2,X3))) = join(X1,join(X2,meet(X1,X3))),
inference(step,[status(thm)],[t89892,t3512]) ).
cnf(t3895,plain,
join(X1,meet(X2,join(X2,X3))) = join(X1,join(X2,meet(X1,X3))),
inference(orient,[status(thm)],[t89893]) ).
cnf(t89896,plain,
join(X1,meet(X2,join(X2,X3))) = join(join(X1,X2),meet(join(X1,X2),X3)),
inference(step,[status(thm)],[t3553,t3895]) ).
cnf(t89897,plain,
join(X1,meet(X2,join(X2,X3))) = meet(join(X1,X2),join(join(X1,X2),X3)),
inference(step,[status(thm)],[t89896,t1337]) ).
cnf(t89898,plain,
join(X1,meet(X2,join(X2,X3))) = meet(join(X1,X2),join(X3,join(X1,X2))),
inference(step,[status(thm)],[t89897,t11]) ).
cnf(t89899,plain,
join(X1,meet(X2,join(X2,X3))) = meet(join(X1,X2),join(X2,join(X3,X1))),
inference(step,[status(thm)],[t89898,t12]) ).
cnf(t89900,plain,
join(X1,meet(X2,join(X2,X3))) = meet(join(X1,X2),join(X1,join(X2,X3))),
inference(step,[status(thm)],[t89899,t12]) ).
cnf(t4083,plain,
meet(join(X1,X2),join(X1,join(X2,X3))) = join(X1,meet(X2,join(X2,X3))),
inference(orient,[status(thm)],[t89900]) ).
cnf(t10016,plain,
meet(X1,join(X1,join(X2,X3))) = meet(X1,join(X1,meet(X2,join(X2,X3)))),
inference(cp,[status(thm)],[t10010,t4083]) ).
cnf(t10161,plain,
meet(X1,join(X1,meet(X2,join(X2,X3)))) = meet(X1,join(X1,join(X2,X3))),
inference(orient,[status(thm)],[t10016]) ).
cnf(t10188,plain,
meet(X1,join(X1,join(X2,meet(X3,join(X3,X2))))) = meet(X1,join(X1,meet(X2,join(X3,X2)))),
inference(cp,[status(thm)],[t10161,t175]) ).
cnf(t90079,plain,
meet(X1,join(X1,join(X3,X2))) = meet(X1,join(X1,meet(X2,join(X3,X2)))),
inference(step,[status(thm)],[t10188,t175]) ).
cnf(t10295,plain,
meet(X1,join(X1,meet(X2,join(X3,X2)))) = meet(X1,join(X1,join(X3,X2))),
inference(orient,[status(thm)],[t90079]) ).
cnf(t1524,plain,
meet(meet(X1,X2),join(X3,X2)) = meet(meet(X1,X2),join(X3,meet(X1,X2))),
inference(cp,[status(thm)],[t1521,t534]) ).
cnf(t89855,plain,
meet(meet(X1,X2),join(X2,X3)) = meet(meet(X1,X2),join(X3,meet(X1,X2))),
inference(step,[status(thm)],[t1524,t11]) ).
cnf(t1523,plain,
meet(meet(X1,X2),join(X3,X1)) = meet(meet(X1,X2),join(X3,meet(X1,X2))),
inference(cp,[status(thm)],[t1521,t117]) ).
cnf(t89847,plain,
meet(meet(X1,X2),join(X1,X3)) = meet(meet(X1,X2),join(X3,meet(X1,X2))),
inference(step,[status(thm)],[t1523,t11]) ).
cnf(t1699,plain,
meet(meet(X1,X2),join(X3,meet(X1,X2))) = meet(meet(X1,X2),join(X1,X3)),
inference(orient,[status(thm)],[t89847]) ).
cnf(t89856,plain,
meet(meet(X1,X2),join(X2,X3)) = meet(meet(X1,X2),join(X1,X3)),
inference(step,[status(thm)],[t89855,t1699]) ).
cnf(t2058,plain,
meet(meet(X1,X2),join(X2,X3)) = meet(meet(X1,X2),join(X1,X3)),
inference(orient,[status(thm)],[t89856]) ).
cnf(t2061,plain,
meet(meet(X1,X2),join(X1,X3)) = meet(join(X2,X3),meet(X1,X2)),
inference(cp,[status(thm)],[t2058,t61]) ).
cnf(t89935,plain,
meet(meet(X1,X2),join(X1,X3)) = meet(X2,meet(join(X2,X3),X1)),
inference(step,[status(thm)],[t2061,t66]) ).
cnf(t89936,plain,
meet(meet(X1,X2),join(X1,X3)) = meet(X1,meet(X2,join(X2,X3))),
inference(step,[status(thm)],[t89935,t66]) ).
cnf(t5963,plain,
meet(meet(X1,X2),join(X1,X3)) = meet(X1,meet(X2,join(X2,X3))),
inference(orient,[status(thm)],[t89936]) ).
cnf(t10315,plain,
meet(X1,join(X1,join(X2,meet(X2,X3)))) = meet(X1,join(X1,meet(X2,meet(X3,join(X3,meet(X2,X3)))))),
inference(cp,[status(thm)],[t10295,t5963]) ).
cnf(t90080,plain,
meet(X1,join(X1,meet(X2,join(X2,X3)))) = meet(X1,join(X1,meet(X2,meet(X3,join(X3,meet(X2,X3)))))),
inference(step,[status(thm)],[t10315,t1337]) ).
cnf(t90081,plain,
meet(X1,join(X1,join(X2,X3))) = meet(X1,join(X1,meet(X2,meet(X3,join(X3,meet(X2,X3)))))),
inference(step,[status(thm)],[t90080,t10161]) ).
cnf(t465,plain,
meet(X1,meet(join(X2,meet(X2,X1)),X3)) = meet(X3,meet(X2,X1)),
inference(cp,[status(thm)],[t66,t443]) ).
cnf(t89787,plain,
meet(X1,meet(X3,join(X2,meet(X2,X1)))) = meet(X3,meet(X2,X1)),
inference(step,[status(thm)],[t465,t61]) ).
cnf(t89788,plain,
meet(X1,meet(X3,join(X2,meet(X1,X2)))) = meet(X3,meet(X2,X1)),
inference(step,[status(thm)],[t89787,t61]) ).
cnf(t89789,plain,
meet(X1,meet(X3,join(X2,meet(X1,X2)))) = meet(X1,meet(X3,X2)),
inference(step,[status(thm)],[t89788,t66]) ).
cnf(t89790,plain,
meet(X1,meet(X3,join(X2,meet(X1,X2)))) = meet(X1,meet(X2,X3)),
inference(step,[status(thm)],[t89789,t61]) ).
cnf(t578,plain,
meet(X1,meet(X2,join(X3,meet(X1,X3)))) = meet(X1,meet(X3,X2)),
inference(orient,[status(thm)],[t89790]) ).
cnf(t90082,plain,
meet(X1,join(X1,join(X2,X3))) = meet(X1,join(X1,meet(X2,meet(X3,X3)))),
inference(step,[status(thm)],[t90081,t578]) ).
cnf(t90083,plain,
meet(X1,join(X1,join(X2,X3))) = meet(X1,join(X1,meet(X2,X3))),
inference(step,[status(thm)],[t90082,t10]) ).
cnf(t10443,plain,
meet(X1,join(X1,join(X2,X3))) = meet(X1,join(X1,meet(X2,X3))),
inference(orient,[status(thm)],[t90083]) ).
cnf(t10537,plain,
join(X1,join(X2,X3)) = join(join(X2,X3),meet(X1,join(X1,meet(X2,X3)))),
inference(cp,[status(thm)],[t175,t10443]) ).
cnf(t11040,plain,
join(join(X1,X2),meet(X3,join(X3,meet(X1,X2)))) = join(X3,join(X1,X2)),
inference(orient,[status(thm)],[t10537]) ).
cnf(t69,plain,
meet(X1,meet(X2,X1)) = meet(X2,X1),
inference(cp,[status(thm)],[t66,t10]) ).
cnf(t89735,plain,
meet(X1,meet(X1,X2)) = meet(X2,X1),
inference(step,[status(thm)],[t69,t66]) ).
cnf(t89736,plain,
meet(X1,meet(X1,X2)) = meet(X1,X2),
inference(step,[status(thm)],[t89735,t61]) ).
cnf(t90,plain,
meet(X1,meet(X1,X2)) = meet(X1,X2),
inference(orient,[status(thm)],[t89736]) ).
cnf(t4021,plain,
join(X1,meet(X2,join(X2,meet(X1,X3)))) = join(X1,join(X2,meet(X1,X3))),
inference(cp,[status(thm)],[t3895,t90]) ).
cnf(t89901,plain,
join(X1,meet(X2,join(X2,meet(X1,X3)))) = join(X1,meet(X2,join(X2,X3))),
inference(step,[status(thm)],[t4021,t3895]) ).
cnf(t4187,plain,
join(X1,meet(X2,join(X2,meet(X1,X3)))) = join(X1,meet(X2,join(X2,X3))),
inference(orient,[status(thm)],[t89901]) ).
cnf(t190,plain,
join(X1,join(meet(X2,join(X2,X1)),X3)) = join(X3,join(X2,X1)),
inference(cp,[status(thm)],[t12,t175]) ).
cnf(t89756,plain,
join(X1,join(X3,meet(X2,join(X2,X1)))) = join(X3,join(X2,X1)),
inference(step,[status(thm)],[t190,t11]) ).
cnf(t89757,plain,
join(X1,join(X3,meet(X2,join(X1,X2)))) = join(X3,join(X2,X1)),
inference(step,[status(thm)],[t89756,t11]) ).
cnf(t89758,plain,
join(X1,join(X3,meet(X2,join(X1,X2)))) = join(X1,join(X3,X2)),
inference(step,[status(thm)],[t89757,t12]) ).
cnf(t89759,plain,
join(X1,join(X3,meet(X2,join(X1,X2)))) = join(X1,join(X2,X3)),
inference(step,[status(thm)],[t89758,t11]) ).
cnf(t272,plain,
join(X1,join(X2,meet(X3,join(X1,X3)))) = join(X1,join(X3,X2)),
inference(orient,[status(thm)],[t89759]) ).
cnf(t276,plain,
join(X1,join(X2,meet(X2,join(X1,X2)))) = join(X1,meet(X2,join(X1,X2))),
inference(cp,[status(thm)],[t272,t9]) ).
cnf(t89760,plain,
join(X1,join(X2,X2)) = join(X1,meet(X2,join(X1,X2))),
inference(step,[status(thm)],[t276,t272]) ).
cnf(t89761,plain,
join(X1,X2) = join(X1,meet(X2,join(X1,X2))),
inference(step,[status(thm)],[t89760,t9]) ).
cnf(t301,plain,
join(X1,meet(X2,join(X1,X2))) = join(X1,X2),
inference(orient,[status(thm)],[t89761]) ).
cnf(t1730,plain,
join(X1,meet(X2,X3)) = join(X1,meet(meet(X2,X3),join(X2,X1))),
inference(cp,[status(thm)],[t301,t1699]) ).
cnf(t89849,plain,
join(X1,meet(X2,X3)) = join(X1,meet(meet(X2,X3),join(X1,X2))),
inference(step,[status(thm)],[t1730,t11]) ).
cnf(t1807,plain,
join(X1,meet(meet(X2,X3),join(X1,X2))) = join(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t89849]) ).
cnf(t4193,plain,
join(meet(X1,X2),meet(X3,join(X3,join(X3,X1)))) = join(meet(X1,X2),meet(X3,join(X3,meet(X1,X2)))),
inference(cp,[status(thm)],[t4187,t1807]) ).
cnf(t15,plain,
join(X1,join(X2,X1)) = join(X2,X1),
inference(cp,[status(thm)],[t12,t9]) ).
cnf(t89733,plain,
join(X1,join(X1,X2)) = join(X2,X1),
inference(step,[status(thm)],[t15,t12]) ).
cnf(t89734,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(step,[status(thm)],[t89733,t11]) ).
cnf(t82,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(orient,[status(thm)],[t89734]) ).
cnf(t89902,plain,
join(meet(X1,X2),meet(X3,join(X3,X1))) = join(meet(X1,X2),meet(X3,join(X3,meet(X1,X2)))),
inference(step,[status(thm)],[t4193,t82]) ).
cnf(t89903,plain,
join(meet(X1,X2),meet(X3,join(X1,X3))) = join(meet(X1,X2),meet(X3,join(X3,meet(X1,X2)))),
inference(step,[status(thm)],[t89902,t11]) ).
cnf(t89904,plain,
join(meet(X1,X2),meet(X3,join(X1,X3))) = join(X3,meet(X1,X2)),
inference(step,[status(thm)],[t89903,t175]) ).
cnf(t4282,plain,
join(meet(X1,X2),meet(X3,join(X1,X3))) = join(X3,meet(X1,X2)),
inference(orient,[status(thm)],[t89904]) ).
cnf(t4297,plain,
join(meet(X1,X2),meet(X3,Y3)) = join(meet(X3,Y3),meet(meet(X1,X2),join(X1,X3))),
inference(cp,[status(thm)],[t4282,t1699]) ).
cnf(t90218,plain,
join(meet(X1,X2),meet(X3,Y3)) = join(meet(X3,Y3),meet(X1,meet(X2,join(X2,X3)))),
inference(step,[status(thm)],[t4297,t5963]) ).
cnf(t2079,plain,
meet(meet(X1,X2),join(X1,X3)) = meet(meet(X2,X1),join(X2,X3)),
inference(cp,[status(thm)],[t2058,t61]) ).
cnf(t89945,plain,
meet(X1,meet(X2,join(X2,X3))) = meet(meet(X2,X1),join(X2,X3)),
inference(step,[status(thm)],[t2079,t5963]) ).
cnf(t89946,plain,
meet(X1,meet(X2,join(X2,X3))) = meet(X2,meet(X1,join(X1,X3))),
inference(step,[status(thm)],[t89945,t5963]) ).
cnf(t89947,plain,
meet(X1,meet(X2,join(X2,X3))) = meet(X1,meet(join(X1,X3),X2)),
inference(step,[status(thm)],[t89946,t66]) ).
cnf(t89948,plain,
meet(X1,meet(X2,join(X2,X3))) = meet(X1,meet(X2,join(X1,X3))),
inference(step,[status(thm)],[t89947,t61]) ).
cnf(t6477,plain,
meet(X1,meet(X2,join(X2,X3))) = meet(X1,meet(X2,join(X1,X3))),
inference(orient,[status(thm)],[t89948]) ).
cnf(t90219,plain,
join(meet(X1,X2),meet(X3,Y3)) = join(meet(X3,Y3),meet(X1,meet(X2,join(X1,X3)))),
inference(step,[status(thm)],[t90218,t6477]) ).
cnf(t17881,plain,
join(meet(X1,X2),meet(X3,meet(Y3,join(X3,X1)))) = join(meet(X3,Y3),meet(X1,X2)),
inference(orient,[status(thm)],[t90219]) ).
cnf(t17888,plain,
join(meet(X1,X2),meet(X3,X3)) = join(X3,meet(X1,meet(X2,join(X1,X3)))),
inference(cp,[status(thm)],[t17881,t10]) ).
cnf(t90220,plain,
join(meet(X1,X2),X3) = join(X3,meet(X1,meet(X2,join(X1,X3)))),
inference(step,[status(thm)],[t17888,t10]) ).
cnf(t90221,plain,
join(X3,meet(X1,X2)) = join(X3,meet(X1,meet(X2,join(X1,X3)))),
inference(step,[status(thm)],[t90220,t11]) ).
cnf(t18159,plain,
join(X1,meet(X2,meet(X3,join(X2,X1)))) = join(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t90221]) ).
cnf(t120,plain,
join(X1,meet(join(X1,X2),X3)) = meet(join(X1,X2),join(X1,meet(join(X1,X2),X3))),
inference(cp,[status(thm)],[t117,t82]) ).
cnf(t89965,plain,
join(X1,meet(X3,join(X1,X2))) = meet(join(X1,X2),join(X1,meet(join(X1,X2),X3))),
inference(step,[status(thm)],[t120,t61]) ).
cnf(t89966,plain,
join(X1,meet(X3,join(X1,X2))) = meet(join(X1,X2),join(X1,meet(X3,join(X1,X2)))),
inference(step,[status(thm)],[t89965,t61]) ).
cnf(t7317,plain,
meet(join(X1,X2),join(X1,meet(X3,join(X1,X2)))) = join(X1,meet(X3,join(X1,X2))),
inference(orient,[status(thm)],[t89966]) ).
cnf(t18192,plain,
join(meet(X1,join(X2,X3)),meet(X2,join(X2,X3))) = join(meet(X1,join(X2,X3)),meet(X2,join(X2,meet(X1,join(X2,X3))))),
inference(cp,[status(thm)],[t18159,t7317]) ).
cnf(t90296,plain,
join(meet(X1,join(X2,X3)),meet(X2,join(X2,X3))) = join(X2,meet(X1,join(X2,X3))),
inference(step,[status(thm)],[t18192,t175]) ).
cnf(t25676,plain,
join(meet(X1,join(X2,X3)),meet(X2,join(X2,X3))) = join(X2,meet(X1,join(X2,X3))),
inference(orient,[status(thm)],[t90296]) ).
cnf(t25896,plain,
join(meet(X1,join(X2,X3)),join(X2,join(X2,X3))) = join(join(X2,join(X2,X3)),meet(meet(X1,join(X2,X3)),join(X2,meet(X1,join(X2,X3))))),
inference(cp,[status(thm)],[t11040,t25676]) ).
cnf(t90297,plain,
join(meet(X1,join(X2,X3)),join(X2,X3)) = join(join(X2,join(X2,X3)),meet(meet(X1,join(X2,X3)),join(X2,meet(X1,join(X2,X3))))),
inference(step,[status(thm)],[t25896,t82]) ).
cnf(t1374,plain,
join(meet(X1,X2),join(X3,X1)) = join(X3,meet(X1,join(X1,X2))),
inference(cp,[status(thm)],[t12,t1337]) ).
cnf(t89925,plain,
join(X1,join(meet(X1,X2),X3)) = join(X3,meet(X1,join(X1,X2))),
inference(step,[status(thm)],[t1374,t12]) ).
cnf(t89926,plain,
join(X1,join(X3,meet(X1,X2))) = join(X3,meet(X1,join(X1,X2))),
inference(step,[status(thm)],[t89925,t11]) ).
cnf(t89927,plain,
join(X1,meet(X3,join(X3,X2))) = join(X3,meet(X1,join(X1,X2))),
inference(step,[status(thm)],[t89926,t3895]) ).
cnf(t89928,plain,
join(X1,meet(X3,join(X2,X3))) = join(X3,meet(X1,join(X1,X2))),
inference(step,[status(thm)],[t89927,t11]) ).
cnf(t5470,plain,
join(X1,meet(X2,join(X3,X2))) = join(X2,meet(X1,join(X1,X3))),
inference(orient,[status(thm)],[t89928]) ).
cnf(t5500,plain,
join(join(X1,X2),meet(X3,join(X3,X1))) = join(X3,meet(join(X1,X2),join(X1,X2))),
inference(cp,[status(thm)],[t5470,t82]) ).
cnf(t89929,plain,
join(join(X1,X2),meet(X3,join(X1,X3))) = join(X3,meet(join(X1,X2),join(X1,X2))),
inference(step,[status(thm)],[t5500,t11]) ).
cnf(t89930,plain,
join(join(X1,X2),meet(X3,join(X1,X3))) = join(X3,join(X1,X2)),
inference(step,[status(thm)],[t89929,t10]) ).
cnf(t89931,plain,
join(join(X1,X2),meet(X3,join(X1,X3))) = join(X2,join(X3,X1)),
inference(step,[status(thm)],[t89930,t12]) ).
cnf(t89932,plain,
join(join(X1,X2),meet(X3,join(X1,X3))) = join(X1,join(X2,X3)),
inference(step,[status(thm)],[t89931,t12]) ).
cnf(t5702,plain,
join(join(X1,X2),meet(X3,join(X1,X3))) = join(X1,join(X2,X3)),
inference(orient,[status(thm)],[t89932]) ).
cnf(t90298,plain,
join(meet(X1,join(X2,X3)),join(X2,X3)) = join(X2,join(join(X2,X3),meet(X1,join(X2,X3)))),
inference(step,[status(thm)],[t90297,t5702]) ).
cnf(t89894,plain,
join(join(X1,X2),meet(X3,join(X1,X2))) = join(X1,meet(X2,join(X2,X3))),
inference(step,[status(thm)],[t3512,t3895]) ).
cnf(t3896,plain,
join(join(X1,X2),meet(X3,join(X1,X2))) = join(X1,meet(X2,join(X2,X3))),
inference(orient,[status(thm)],[t89894]) ).
cnf(t90299,plain,
join(meet(X1,join(X2,X3)),join(X2,X3)) = join(X2,join(X2,meet(X3,join(X3,X1)))),
inference(step,[status(thm)],[t90298,t3896]) ).
cnf(t90300,plain,
join(meet(X1,join(X2,X3)),join(X2,X3)) = join(X2,meet(X3,join(X3,X1))),
inference(step,[status(thm)],[t90299,t82]) ).
cnf(t90301,plain,
join(X3,join(meet(X1,join(X2,X3)),X2)) = join(X2,meet(X3,join(X3,X1))),
inference(step,[status(thm)],[t90300,t12]) ).
cnf(t90302,plain,
join(X2,join(X3,meet(X1,join(X2,X3)))) = join(X2,meet(X3,join(X3,X1))),
inference(step,[status(thm)],[t90301,t12]) ).
cnf(t90303,plain,
join(X2,join(X3,meet(X1,join(X2,X3)))) = join(X2,meet(X3,join(X1,X3))),
inference(step,[status(thm)],[t90302,t11]) ).
cnf(t25971,plain,
join(X1,join(X2,meet(X3,join(X1,X2)))) = join(X1,meet(X2,join(X3,X2))),
inference(orient,[status(thm)],[t90303]) ).
cnf(t96,plain,
meet(X1,join(meet(X1,X2),X3)) = join(meet(X1,X2),meet(X1,join(meet(X1,X2),X3))),
inference(cp,[status(thm)],[t33,t90]) ).
cnf(t89963,plain,
meet(X1,join(X3,meet(X1,X2))) = join(meet(X1,X2),meet(X1,join(meet(X1,X2),X3))),
inference(step,[status(thm)],[t96,t11]) ).
cnf(t89964,plain,
meet(X1,join(X3,meet(X1,X2))) = join(meet(X1,X2),meet(X1,join(X3,meet(X1,X2)))),
inference(step,[status(thm)],[t89963,t11]) ).
cnf(t7199,plain,
join(meet(X1,X2),meet(X1,join(X3,meet(X1,X2)))) = meet(X1,join(X3,meet(X1,X2))),
inference(orient,[status(thm)],[t89964]) ).
cnf(t25985,plain,
join(X1,meet(meet(X2,X3),join(X2,meet(X2,X3)))) = join(X1,meet(X2,join(X1,meet(X2,X3)))),
inference(cp,[status(thm)],[t25971,t7199]) ).
cnf(t90306,plain,
join(meet(X2,X3),meet(X1,join(X1,X2))) = join(X1,meet(X2,join(X1,meet(X2,X3)))),
inference(step,[status(thm)],[t25985,t5470]) ).
cnf(t4325,plain,
join(X1,meet(X2,X3)) = join(meet(X2,X3),meet(X1,join(X1,X2))),
inference(cp,[status(thm)],[t4282,t11]) ).
cnf(t4501,plain,
join(meet(X1,X2),meet(X3,join(X3,X1))) = join(X3,meet(X1,X2)),
inference(orient,[status(thm)],[t4325]) ).
cnf(t90307,plain,
join(X1,meet(X2,X3)) = join(X1,meet(X2,join(X1,meet(X2,X3)))),
inference(step,[status(thm)],[t90306,t4501]) ).
cnf(t26241,plain,
join(X1,meet(X2,join(X1,meet(X2,X3)))) = join(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t90307]) ).
cnf(t1579,plain,
meet(meet(join(X1,X2),join(X1,X3)),meet(Y3,X3)) = meet(Y3,meet(X3,join(X1,X2))),
inference(cp,[status(thm)],[t66,t1521]) ).
cnf(t90111,plain,
meet(X3,meet(meet(join(X1,X2),join(X1,X3)),Y3)) = meet(Y3,meet(X3,join(X1,X2))),
inference(step,[status(thm)],[t1579,t66]) ).
cnf(t90112,plain,
meet(X3,meet(Y3,meet(join(X1,X2),join(X1,X3)))) = meet(Y3,meet(X3,join(X1,X2))),
inference(step,[status(thm)],[t90111,t61]) ).
cnf(t90113,plain,
meet(X3,meet(Y3,meet(join(X1,X2),join(X1,X3)))) = meet(X3,meet(join(X1,X2),Y3)),
inference(step,[status(thm)],[t90112,t66]) ).
cnf(t90114,plain,
meet(X3,meet(Y3,meet(join(X1,X2),join(X1,X3)))) = meet(X3,meet(Y3,join(X1,X2))),
inference(step,[status(thm)],[t90113,t61]) ).
cnf(t11564,plain,
meet(X1,meet(X2,meet(join(X3,Y3),join(X3,X1)))) = meet(X1,meet(X2,join(X3,Y3))),
inference(orient,[status(thm)],[t90114]) ).
cnf(t11577,plain,
meet(meet(X1,X2),meet(X3,join(Y3,X1))) = meet(meet(X1,X2),meet(X3,join(Y3,meet(X1,X2)))),
inference(cp,[status(thm)],[t11564,t117]) ).
cnf(t90444,plain,
meet(X3,meet(join(Y3,X1),meet(X1,X2))) = meet(meet(X1,X2),meet(X3,join(Y3,meet(X1,X2)))),
inference(step,[status(thm)],[t11577,t66]) ).
cnf(t90445,plain,
meet(X3,meet(X2,meet(join(Y3,X1),X1))) = meet(meet(X1,X2),meet(X3,join(Y3,meet(X1,X2)))),
inference(step,[status(thm)],[t90444,t66]) ).
cnf(t90446,plain,
meet(X3,meet(X1,meet(X2,join(Y3,X1)))) = meet(meet(X1,X2),meet(X3,join(Y3,meet(X1,X2)))),
inference(step,[status(thm)],[t90445,t66]) ).
cnf(t90447,plain,
meet(X1,meet(meet(X2,join(Y3,X1)),X3)) = meet(meet(X1,X2),meet(X3,join(Y3,meet(X1,X2)))),
inference(step,[status(thm)],[t90446,t66]) ).
cnf(t90448,plain,
meet(X1,meet(X3,meet(X2,join(Y3,X1)))) = meet(meet(X1,X2),meet(X3,join(Y3,meet(X1,X2)))),
inference(step,[status(thm)],[t90447,t61]) ).
cnf(t90449,plain,
meet(X1,meet(X2,meet(join(Y3,X1),X3))) = meet(meet(X1,X2),meet(X3,join(Y3,meet(X1,X2)))),
inference(step,[status(thm)],[t90448,t66]) ).
cnf(t90450,plain,
meet(X1,meet(X2,meet(X3,join(Y3,X1)))) = meet(meet(X1,X2),meet(X3,join(Y3,meet(X1,X2)))),
inference(step,[status(thm)],[t90449,t61]) ).
cnf(t90451,plain,
meet(X1,meet(X2,meet(X3,join(X1,Y3)))) = meet(meet(X1,X2),meet(X3,join(Y3,meet(X1,X2)))),
inference(step,[status(thm)],[t90450,t11]) ).
cnf(t90452,plain,
meet(X1,meet(X2,meet(X3,join(X1,Y3)))) = meet(X3,meet(join(Y3,meet(X1,X2)),meet(X1,X2))),
inference(step,[status(thm)],[t90451,t66]) ).
cnf(t90453,plain,
meet(X1,meet(X2,meet(X3,join(X1,Y3)))) = meet(X3,meet(X2,meet(join(Y3,meet(X1,X2)),X1))),
inference(step,[status(thm)],[t90452,t66]) ).
cnf(t90454,plain,
meet(X1,meet(X2,meet(X3,join(X1,Y3)))) = meet(X3,meet(X1,meet(X2,join(Y3,meet(X1,X2))))),
inference(step,[status(thm)],[t90453,t66]) ).
cnf(t90455,plain,
meet(X1,meet(X2,meet(X3,join(X1,Y3)))) = meet(X1,meet(meet(X2,join(Y3,meet(X1,X2))),X3)),
inference(step,[status(thm)],[t90454,t66]) ).
cnf(t90456,plain,
meet(X1,meet(X2,meet(X3,join(X1,Y3)))) = meet(X1,meet(X3,meet(X2,join(Y3,meet(X1,X2))))),
inference(step,[status(thm)],[t90455,t61]) ).
cnf(t90457,plain,
meet(X1,meet(X2,meet(X3,join(X1,Y3)))) = meet(X1,meet(X2,meet(join(Y3,meet(X1,X2)),X3))),
inference(step,[status(thm)],[t90456,t66]) ).
cnf(t90458,plain,
meet(X1,meet(X2,meet(X3,join(X1,Y3)))) = meet(X1,meet(X2,meet(X3,join(Y3,meet(X1,X2))))),
inference(step,[status(thm)],[t90457,t61]) ).
cnf(t40137,plain,
meet(X1,meet(X2,meet(X3,join(Y3,meet(X1,X2))))) = meet(X1,meet(X2,meet(X3,join(X1,Y3)))),
inference(orient,[status(thm)],[t90458]) ).
cnf(t40176,plain,
meet(X1,meet(join(X2,X3),meet(join(X2,X3),join(X1,X2)))) = meet(X1,meet(join(X2,X3),join(X2,meet(X1,join(X2,X3))))),
inference(cp,[status(thm)],[t40137,t7317]) ).
cnf(t90460,plain,
meet(X1,meet(join(X2,X3),join(X1,X2))) = meet(X1,meet(join(X2,X3),join(X2,meet(X1,join(X2,X3))))),
inference(step,[status(thm)],[t40176,t90]) ).
cnf(t90461,plain,
meet(X1,meet(join(X2,X3),join(X1,X2))) = meet(X1,join(X2,meet(X1,join(X2,X3)))),
inference(step,[status(thm)],[t90460,t7317]) ).
cnf(t90462,plain,
meet(X1,meet(join(X1,X2),join(X2,X3))) = meet(X1,join(X2,meet(X1,join(X2,X3)))),
inference(step,[status(thm)],[t90461,t61]) ).
cnf(t1526,plain,
meet(X1,join(X2,X3)) = meet(X1,meet(join(X2,X1),join(X2,X3))),
inference(cp,[status(thm)],[t1521,t61]) ).
cnf(t89846,plain,
meet(X1,join(X2,X3)) = meet(X1,meet(join(X1,X2),join(X2,X3))),
inference(step,[status(thm)],[t1526,t11]) ).
cnf(t1642,plain,
meet(X1,meet(join(X1,X2),join(X2,X3))) = meet(X1,join(X2,X3)),
inference(orient,[status(thm)],[t89846]) ).
cnf(t90463,plain,
meet(X1,join(X2,X3)) = meet(X1,join(X2,meet(X1,join(X2,X3)))),
inference(step,[status(thm)],[t90462,t1642]) ).
cnf(t40686,plain,
meet(X1,join(X2,meet(X1,join(X2,X3)))) = meet(X1,join(X2,X3)),
inference(orient,[status(thm)],[t90463]) ).
cnf(t40904,plain,
meet(X1,meet(join(X2,meet(X1,join(X2,X3))),Y3)) = meet(Y3,meet(X1,join(X2,X3))),
inference(cp,[status(thm)],[t66,t40686]) ).
cnf(t90471,plain,
meet(X1,meet(Y3,join(X2,meet(X1,join(X2,X3))))) = meet(Y3,meet(X1,join(X2,X3))),
inference(step,[status(thm)],[t40904,t61]) ).
cnf(t90472,plain,
meet(X1,meet(Y3,join(X2,meet(X1,join(X2,X3))))) = meet(X1,meet(join(X2,X3),Y3)),
inference(step,[status(thm)],[t90471,t66]) ).
cnf(t90473,plain,
meet(X1,meet(Y3,join(X2,meet(X1,join(X2,X3))))) = meet(X1,meet(Y3,join(X2,X3))),
inference(step,[status(thm)],[t90472,t61]) ).
cnf(t42455,plain,
meet(X1,meet(X2,join(X3,meet(X1,join(X3,Y3))))) = meet(X1,meet(X2,join(X3,Y3))),
inference(orient,[status(thm)],[t90473]) ).
cnf(t42528,plain,
meet(X1,meet(X2,join(X3,meet(Y3,join(Y3,X3))))) = meet(X1,meet(X2,join(X3,meet(X1,join(Y3,X3))))),
inference(cp,[status(thm)],[t42455,t175]) ).
cnf(t90475,plain,
meet(X1,meet(X2,join(Y3,X3))) = meet(X1,meet(X2,join(X3,meet(X1,join(Y3,X3))))),
inference(step,[status(thm)],[t42528,t175]) ).
cnf(t43025,plain,
meet(X1,meet(X2,join(X3,meet(X1,join(Y3,X3))))) = meet(X1,meet(X2,join(Y3,X3))),
inference(orient,[status(thm)],[t90475]) ).
cnf(t26304,plain,
join(X1,join(meet(X2,join(X1,meet(X2,X3))),Y3)) = join(join(X1,meet(X2,X3)),meet(Y3,join(X1,Y3))),
inference(cp,[status(thm)],[t5702,t26241]) ).
cnf(t90346,plain,
join(X1,join(Y3,meet(X2,join(X1,meet(X2,X3))))) = join(join(X1,meet(X2,X3)),meet(Y3,join(X1,Y3))),
inference(step,[status(thm)],[t26304,t11]) ).
cnf(t90347,plain,
join(X1,join(Y3,meet(X2,join(X1,meet(X2,X3))))) = join(X1,join(meet(X2,X3),Y3)),
inference(step,[status(thm)],[t90346,t5702]) ).
cnf(t90348,plain,
join(X1,join(Y3,meet(X2,join(X1,meet(X2,X3))))) = join(X1,join(Y3,meet(X2,X3))),
inference(step,[status(thm)],[t90347,t11]) ).
cnf(t31121,plain,
join(X1,join(X2,meet(X3,join(X1,meet(X3,Y3))))) = join(X1,join(X2,meet(X3,Y3))),
inference(orient,[status(thm)],[t90348]) ).
cnf(t3180,plain,
join(X1,meet(X2,X3)) = join(X1,join(meet(X2,X1),meet(X2,X3))),
inference(cp,[status(thm)],[t3167,t11]) ).
cnf(t89874,plain,
join(X1,meet(X2,X3)) = join(X1,join(meet(X1,X2),meet(X2,X3))),
inference(step,[status(thm)],[t3180,t61]) ).
cnf(t3356,plain,
join(X1,join(meet(X1,X2),meet(X2,X3))) = join(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t89874]) ).
cnf(t3380,plain,
join(X1,meet(meet(X1,X2),X3)) = join(X1,join(meet(X1,X2),meet(meet(X1,X2),X3))),
inference(cp,[status(thm)],[t3356,t90]) ).
cnf(t90169,plain,
join(X1,meet(X3,meet(X1,X2))) = join(X1,join(meet(X1,X2),meet(meet(X1,X2),X3))),
inference(step,[status(thm)],[t3380,t61]) ).
cnf(t90170,plain,
join(X1,meet(X2,meet(X3,X1))) = join(X1,join(meet(X1,X2),meet(meet(X1,X2),X3))),
inference(step,[status(thm)],[t90169,t66]) ).
cnf(t90171,plain,
join(X1,meet(X1,meet(X2,X3))) = join(X1,join(meet(X1,X2),meet(meet(X1,X2),X3))),
inference(step,[status(thm)],[t90170,t66]) ).
cnf(t90172,plain,
meet(X1,join(X1,meet(X2,X3))) = join(X1,join(meet(X1,X2),meet(meet(X1,X2),X3))),
inference(step,[status(thm)],[t90171,t1337]) ).
cnf(t90173,plain,
meet(X1,join(X1,meet(X2,X3))) = join(X1,meet(meet(X1,X2),join(meet(X1,X2),X3))),
inference(step,[status(thm)],[t90172,t1337]) ).
cnf(t90174,plain,
meet(X1,join(X1,meet(X2,X3))) = join(meet(X1,X2),meet(X1,join(X3,X1))),
inference(step,[status(thm)],[t90173,t5470]) ).
cnf(t90175,plain,
meet(X1,join(X1,meet(X2,X3))) = join(meet(X1,X2),meet(X1,join(X1,X3))),
inference(step,[status(thm)],[t90174,t11]) ).
cnf(t14698,plain,
join(meet(X1,X2),meet(X1,join(X1,X3))) = meet(X1,join(X1,meet(X2,X3))),
inference(orient,[status(thm)],[t90175]) ).
cnf(t31140,plain,
join(X1,join(meet(X1,X2),meet(X1,X3))) = join(X1,meet(X1,join(X1,meet(X2,meet(X1,X3))))),
inference(cp,[status(thm)],[t31121,t14698]) ).
cnf(t1814,plain,
join(X1,meet(X2,meet(X3,Y3))) = join(X1,meet(meet(X3,meet(Y3,X2)),join(X1,X2))),
inference(cp,[status(thm)],[t1807,t66]) ).
cnf(t90128,plain,
join(X1,meet(X2,meet(X3,Y3))) = join(X1,meet(join(X1,X2),meet(X3,meet(Y3,X2)))),
inference(step,[status(thm)],[t1814,t61]) ).
cnf(t90129,plain,
join(X1,meet(X2,meet(X3,Y3))) = join(X1,meet(meet(Y3,X2),meet(join(X1,X2),X3))),
inference(step,[status(thm)],[t90128,t66]) ).
cnf(t90130,plain,
join(X1,meet(X2,meet(X3,Y3))) = join(X1,meet(X3,meet(meet(Y3,X2),join(X1,X2)))),
inference(step,[status(thm)],[t90129,t66]) ).
cnf(t90131,plain,
join(X1,meet(X2,meet(X3,Y3))) = join(X1,meet(X3,meet(meet(X2,Y3),join(X1,X2)))),
inference(step,[status(thm)],[t90130,t61]) ).
cnf(t12328,plain,
join(X1,meet(X2,meet(meet(X3,Y3),join(X1,X3)))) = join(X1,meet(X3,meet(X2,Y3))),
inference(orient,[status(thm)],[t90131]) ).
cnf(t26251,plain,
join(X1,meet(X2,meet(meet(X3,Y3),join(X1,X3)))) = join(X1,meet(X2,join(X1,meet(X3,meet(X2,Y3))))),
inference(cp,[status(thm)],[t26241,t12328]) ).
cnf(t90339,plain,
join(X1,meet(X3,meet(X2,Y3))) = join(X1,meet(X2,join(X1,meet(X3,meet(X2,Y3))))),
inference(step,[status(thm)],[t26251,t12328]) ).
cnf(t30254,plain,
join(X1,meet(X2,join(X1,meet(X3,meet(X2,Y3))))) = join(X1,meet(X3,meet(X2,Y3))),
inference(orient,[status(thm)],[t90339]) ).
cnf(t90349,plain,
join(X1,join(meet(X1,X2),meet(X1,X3))) = join(X1,meet(X2,meet(X1,X3))),
inference(step,[status(thm)],[t31140,t30254]) ).
cnf(t90350,plain,
join(X1,join(meet(X1,X2),meet(X1,X3))) = join(X1,meet(X1,meet(X3,X2))),
inference(step,[status(thm)],[t90349,t66]) ).
cnf(t90351,plain,
join(X1,join(meet(X1,X2),meet(X1,X3))) = meet(X1,join(X1,meet(X3,X2))),
inference(step,[status(thm)],[t90350,t1337]) ).
cnf(t90352,plain,
join(X1,join(meet(X1,X2),meet(X1,X3))) = meet(X1,join(X1,meet(X2,X3))),
inference(step,[status(thm)],[t90351,t61]) ).
cnf(t31382,plain,
join(X1,join(meet(X1,X2),meet(X1,X3))) = meet(X1,join(X1,meet(X2,X3))),
inference(orient,[status(thm)],[t90352]) ).
cnf(t31600,plain,
join(X1,join(join(meet(X1,X2),meet(X1,X3)),Y3)) = join(meet(X1,join(X1,meet(X2,X3))),meet(Y3,join(X1,Y3))),
inference(cp,[status(thm)],[t5702,t31382]) ).
cnf(t90522,plain,
join(X1,join(Y3,join(meet(X1,X2),meet(X1,X3)))) = join(meet(X1,join(X1,meet(X2,X3))),meet(Y3,join(X1,Y3))),
inference(step,[status(thm)],[t31600,t11]) ).
cnf(t90523,plain,
join(X1,join(Y3,join(meet(X1,X2),meet(X1,X3)))) = join(Y3,meet(X1,join(X1,meet(X2,X3)))),
inference(step,[status(thm)],[t90522,t4282]) ).
cnf(t90524,plain,
join(X1,join(Y3,join(meet(X1,X2),meet(X1,X3)))) = join(X1,meet(Y3,join(meet(X2,X3),Y3))),
inference(step,[status(thm)],[t90523,t5470]) ).
cnf(t90525,plain,
join(X1,join(Y3,join(meet(X1,X2),meet(X1,X3)))) = join(X1,meet(Y3,join(Y3,meet(X2,X3)))),
inference(step,[status(thm)],[t90524,t11]) ).
cnf(t51540,plain,
join(X1,join(X2,join(meet(X1,X3),meet(X1,Y3)))) = join(X1,meet(X2,join(X2,meet(X3,Y3)))),
inference(orient,[status(thm)],[t90525]) ).
cnf(t52131,plain,
join(X1,join(meet(X2,X3),join(meet(X1,Y3),meet(X1,join(X2,Y3))))) = join(X1,meet(meet(X2,X3),join(Y3,meet(X2,X3)))),
inference(cp,[status(thm)],[t51540,t4282]) ).
cnf(t90566,plain,
join(X1,join(meet(X2,X3),meet(X1,join(X2,Y3)))) = join(X1,meet(meet(X2,X3),join(Y3,meet(X2,X3)))),
inference(step,[status(thm)],[t52131,t243]) ).
cnf(t89937,plain,
meet(meet(X1,X2),join(X3,meet(X1,X2))) = meet(X1,meet(X2,join(X2,X3))),
inference(step,[status(thm)],[t1699,t5963]) ).
cnf(t5964,plain,
meet(meet(X1,X2),join(X3,meet(X1,X2))) = meet(X1,meet(X2,join(X2,X3))),
inference(orient,[status(thm)],[t89937]) ).
cnf(t89949,plain,
meet(meet(X1,X2),join(X3,meet(X1,X2))) = meet(X1,meet(X2,join(X1,X3))),
inference(step,[status(thm)],[t5964,t6477]) ).
cnf(t6478,plain,
meet(meet(X1,X2),join(X3,meet(X1,X2))) = meet(X1,meet(X2,join(X1,X3))),
inference(orient,[status(thm)],[t89949]) ).
cnf(t90567,plain,
join(X1,join(meet(X2,X3),meet(X1,join(X2,Y3)))) = join(X1,meet(X2,meet(X3,join(X2,Y3)))),
inference(step,[status(thm)],[t90566,t6478]) ).
cnf(t57897,plain,
join(X1,join(meet(X2,X3),meet(X1,join(X2,Y3)))) = join(X1,meet(X2,meet(X3,join(X2,Y3)))),
inference(orient,[status(thm)],[t90567]) ).
cnf(t8,axiom,
meet(join(meet(join(X1,X2),X3),X2),join(X3,X1)) = join(meet(join(meet(X1,X2),X3),X2),meet(X3,X1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t89728,plain,
meet(join(X2,meet(join(X1,X2),X3)),join(X3,X1)) = join(meet(join(meet(X1,X2),X3),X2),meet(X3,X1)),
inference(step,[status(thm)],[t8,t11]) ).
cnf(t89729,plain,
meet(join(X2,meet(join(X1,X2),X3)),join(X1,X3)) = join(meet(join(meet(X1,X2),X3),X2),meet(X3,X1)),
inference(step,[status(thm)],[t89728,t11]) ).
cnf(t89730,plain,
meet(join(X2,meet(join(X1,X2),X3)),join(X1,X3)) = join(meet(X3,X1),meet(join(meet(X1,X2),X3),X2)),
inference(step,[status(thm)],[t89729,t11]) ).
cnf(t89731,plain,
meet(join(X2,meet(join(X1,X2),X3)),join(X1,X3)) = join(meet(X3,X1),meet(join(X3,meet(X1,X2)),X2)),
inference(step,[status(thm)],[t89730,t11]) ).
cnf(t46,plain,
join(meet(X1,X2),meet(join(X1,meet(X2,X3)),X3)) = meet(join(X3,meet(join(X2,X3),X1)),join(X2,X1)),
inference(orient,[status(thm)],[t89731]) ).
cnf(t65,plain,
join(meet(X1,X2),meet(join(X1,meet(X2,X3)),X3)) = meet(join(X3,meet(join(X2,X3),X1)),join(X2,X1)),
inference(rw,[status(thm)],[t46]) ).
cnf(t89953,plain,
join(meet(X1,X2),meet(X3,join(X1,meet(X2,X3)))) = meet(join(X3,meet(join(X2,X3),X1)),join(X2,X1)),
inference(step,[status(thm)],[t65,t61]) ).
cnf(t89954,plain,
join(meet(X1,X2),meet(X3,join(X1,meet(X2,X3)))) = meet(join(X2,X1),join(X3,meet(join(X2,X3),X1))),
inference(step,[status(thm)],[t89953,t61]) ).
cnf(t89955,plain,
join(meet(X1,X2),meet(X3,join(X1,meet(X2,X3)))) = meet(join(X1,X2),join(X3,meet(join(X2,X3),X1))),
inference(step,[status(thm)],[t89954,t11]) ).
cnf(t89956,plain,
join(meet(X1,X2),meet(X3,join(X1,meet(X2,X3)))) = meet(join(X1,X2),join(X3,meet(X1,join(X2,X3)))),
inference(step,[status(thm)],[t89955,t61]) ).
cnf(t6704,plain,
join(meet(X1,X2),meet(X3,join(X1,meet(X2,X3)))) = meet(join(X1,X2),join(X3,meet(X1,join(X2,X3)))),
inference(orient,[status(thm)],[t89956]) ).
cnf(t57906,plain,
join(X1,meet(X2,meet(X3,join(X2,meet(X3,X1))))) = join(X1,meet(join(X2,X3),join(X1,meet(X2,join(X3,X1))))),
inference(cp,[status(thm)],[t57897,t6704]) ).
cnf(t6505,plain,
meet(X1,meet(X2,join(X1,meet(X2,X3)))) = meet(X1,meet(X2,meet(X2,join(X2,X3)))),
inference(cp,[status(thm)],[t6477,t1337]) ).
cnf(t89960,plain,
meet(X1,meet(X2,join(X1,meet(X2,X3)))) = meet(X1,meet(X2,join(X2,X3))),
inference(step,[status(thm)],[t6505,t90]) ).
cnf(t89961,plain,
meet(X1,meet(X2,join(X1,meet(X2,X3)))) = meet(X1,meet(X2,join(X1,X3))),
inference(step,[status(thm)],[t89960,t6477]) ).
cnf(t7008,plain,
meet(X1,meet(X2,join(X1,meet(X2,X3)))) = meet(X1,meet(X2,join(X1,X3))),
inference(orient,[status(thm)],[t89961]) ).
cnf(t90625,plain,
join(X1,meet(X2,meet(X3,join(X2,X1)))) = join(X1,meet(join(X2,X3),join(X1,meet(X2,join(X3,X1))))),
inference(step,[status(thm)],[t57906,t7008]) ).
cnf(t90626,plain,
join(X1,meet(X2,X3)) = join(X1,meet(join(X2,X3),join(X1,meet(X2,join(X3,X1))))),
inference(step,[status(thm)],[t90625,t18159]) ).
cnf(t90627,plain,
join(X1,meet(X2,X3)) = join(X1,meet(join(X2,X3),join(X1,meet(X2,join(X1,X3))))),
inference(step,[status(thm)],[t90626,t11]) ).
cnf(t73403,plain,
join(X1,meet(join(X2,X3),join(X1,meet(X2,join(X1,X3))))) = join(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t90627]) ).
cnf(t73849,plain,
meet(join(X1,X2),join(X3,meet(X1,join(X3,X2)))) = meet(join(X1,X2),join(X3,meet(X1,X2))),
inference(cp,[status(thm)],[t40686,t73403]) ).
cnf(t90628,plain,
meet(join(X1,X2),join(X3,meet(X1,join(X2,X3)))) = meet(join(X1,X2),join(X3,meet(X1,X2))),
inference(step,[status(thm)],[t73849,t11]) ).
cnf(t74002,plain,
meet(join(X1,X2),join(X3,meet(X1,join(X2,X3)))) = meet(join(X1,X2),join(X3,meet(X1,X2))),
inference(orient,[status(thm)],[t90628]) ).
cnf(t74518,plain,
meet(X1,meet(join(X1,X2),join(X2,X3))) = meet(X1,meet(join(X1,X2),join(X3,meet(X1,X2)))),
inference(cp,[status(thm)],[t43025,t74002]) ).
cnf(t90631,plain,
meet(X1,join(X2,X3)) = meet(X1,meet(join(X1,X2),join(X3,meet(X1,X2)))),
inference(step,[status(thm)],[t74518,t1642]) ).
cnf(t1578,plain,
meet(X1,meet(meet(join(X2,X3),join(X2,X1)),Y3)) = meet(Y3,meet(X1,join(X2,X3))),
inference(cp,[status(thm)],[t66,t1521]) ).
cnf(t90105,plain,
meet(X1,meet(Y3,meet(join(X2,X3),join(X2,X1)))) = meet(Y3,meet(X1,join(X2,X3))),
inference(step,[status(thm)],[t1578,t61]) ).
cnf(t90106,plain,
meet(X1,meet(Y3,meet(join(X2,X1),join(X2,X3)))) = meet(Y3,meet(X1,join(X2,X3))),
inference(step,[status(thm)],[t90105,t61]) ).
cnf(t90107,plain,
meet(X1,meet(Y3,meet(join(X1,X2),join(X2,X3)))) = meet(Y3,meet(X1,join(X2,X3))),
inference(step,[status(thm)],[t90106,t11]) ).
cnf(t90108,plain,
meet(X1,meet(Y3,meet(join(X1,X2),join(X2,X3)))) = meet(X1,meet(join(X2,X3),Y3)),
inference(step,[status(thm)],[t90107,t66]) ).
cnf(t90109,plain,
meet(X1,meet(Y3,meet(join(X1,X2),join(X2,X3)))) = meet(X1,meet(Y3,join(X2,X3))),
inference(step,[status(thm)],[t90108,t61]) ).
cnf(t11419,plain,
meet(X1,meet(X2,meet(join(X1,X3),join(X3,Y3)))) = meet(X1,meet(X2,join(X3,Y3))),
inference(orient,[status(thm)],[t90109]) ).
cnf(t40142,plain,
meet(X1,meet(X2,meet(join(X1,X3),join(X1,X3)))) = meet(X1,meet(X2,join(X3,meet(X1,X2)))),
inference(cp,[status(thm)],[t40137,t11419]) ).
cnf(t89829,plain,
meet(join(X1,X2),meet(X3,join(X3,X2))) = meet(X3,join(X1,X2)),
inference(step,[status(thm)],[t1259,t1337]) ).
cnf(t1375,plain,
meet(join(X1,X2),meet(X3,join(X3,X2))) = meet(X3,join(X1,X2)),
inference(rw,[status(thm)],[t89829]) ).
cnf(t89838,plain,
meet(X3,meet(join(X3,X2),join(X1,X2))) = meet(X3,join(X1,X2)),
inference(step,[status(thm)],[t1375,t66]) ).
cnf(t89839,plain,
meet(X3,meet(join(X1,X2),join(X3,X2))) = meet(X3,join(X1,X2)),
inference(step,[status(thm)],[t89838,t61]) ).
cnf(t89840,plain,
meet(X3,meet(join(X1,X2),join(X2,X3))) = meet(X3,join(X1,X2)),
inference(step,[status(thm)],[t89839,t11]) ).
cnf(t1383,plain,
meet(X1,meet(join(X2,X3),join(X3,X1))) = meet(X1,join(X2,X3)),
inference(orient,[status(thm)],[t89840]) ).
cnf(t1444,plain,
meet(X1,meet(meet(join(X2,X3),join(X3,X1)),Y3)) = meet(Y3,meet(X1,join(X2,X3))),
inference(cp,[status(thm)],[t66,t1383]) ).
cnf(t90063,plain,
meet(X1,meet(Y3,meet(join(X2,X3),join(X3,X1)))) = meet(Y3,meet(X1,join(X2,X3))),
inference(step,[status(thm)],[t1444,t61]) ).
cnf(t90064,plain,
meet(X1,meet(Y3,meet(join(X2,X3),join(X1,X3)))) = meet(Y3,meet(X1,join(X2,X3))),
inference(step,[status(thm)],[t90063,t11]) ).
cnf(t90065,plain,
meet(X1,meet(Y3,meet(join(X1,X3),join(X2,X3)))) = meet(Y3,meet(X1,join(X2,X3))),
inference(step,[status(thm)],[t90064,t61]) ).
cnf(t90066,plain,
meet(X1,meet(Y3,meet(join(X1,X3),join(X2,X3)))) = meet(X1,meet(join(X2,X3),Y3)),
inference(step,[status(thm)],[t90065,t66]) ).
cnf(t90067,plain,
meet(X1,meet(Y3,meet(join(X1,X3),join(X2,X3)))) = meet(X1,meet(Y3,join(X2,X3))),
inference(step,[status(thm)],[t90066,t61]) ).
cnf(t9385,plain,
meet(X1,meet(X2,meet(join(X1,X3),join(Y3,X3)))) = meet(X1,meet(X2,join(Y3,X3))),
inference(orient,[status(thm)],[t90067]) ).
cnf(t90459,plain,
meet(X1,meet(X2,join(X1,X3))) = meet(X1,meet(X2,join(X3,meet(X1,X2)))),
inference(step,[status(thm)],[t40142,t9385]) ).
cnf(t40421,plain,
meet(X1,meet(X2,join(X3,meet(X1,X2)))) = meet(X1,meet(X2,join(X1,X3))),
inference(orient,[status(thm)],[t90459]) ).
cnf(t17917,plain,
join(meet(X1,join(X1,X2)),meet(join(X2,X3),Y3)) = join(meet(join(X2,X3),Y3),meet(X1,join(X1,join(X2,X3)))),
inference(cp,[status(thm)],[t17881,t10010]) ).
cnf(t90293,plain,
join(meet(X1,join(X1,X2)),meet(Y3,join(X2,X3))) = join(meet(join(X2,X3),Y3),meet(X1,join(X1,join(X2,X3)))),
inference(step,[status(thm)],[t17917,t61]) ).
cnf(t90294,plain,
join(meet(X1,join(X1,X2)),meet(Y3,join(X2,X3))) = join(X1,meet(join(X2,X3),Y3)),
inference(step,[status(thm)],[t90293,t4501]) ).
cnf(t90295,plain,
join(meet(X1,join(X1,X2)),meet(Y3,join(X2,X3))) = join(X1,meet(Y3,join(X2,X3))),
inference(step,[status(thm)],[t90294,t61]) ).
cnf(t25332,plain,
join(meet(X1,join(X1,X2)),meet(X3,join(X2,Y3))) = join(X1,meet(X3,join(X2,Y3))),
inference(orient,[status(thm)],[t90295]) ).
cnf(t40465,plain,
meet(X1,meet(join(X2,X3),join(X1,meet(Y3,join(Y3,X2))))) = meet(X1,meet(join(X2,X3),join(Y3,meet(X1,join(X2,X3))))),
inference(cp,[status(thm)],[t40421,t25332]) ).
cnf(t10552,plain,
meet(X1,meet(X2,join(X1,join(X2,join(X3,Y3))))) = meet(X1,meet(X2,join(X1,meet(X2,join(X2,meet(X3,Y3)))))),
inference(cp,[status(thm)],[t7008,t10443]) ).
cnf(t6003,plain,
meet(X1,meet(X2,join(X2,join(X1,X3)))) = meet(meet(X1,X2),join(X1,X3)),
inference(cp,[status(thm)],[t5963,t82]) ).
cnf(t89939,plain,
meet(X1,meet(X2,join(X1,join(X3,X2)))) = meet(meet(X1,X2),join(X1,X3)),
inference(step,[status(thm)],[t6003,t12]) ).
cnf(t89940,plain,
meet(X1,meet(X2,join(X1,join(X2,X3)))) = meet(meet(X1,X2),join(X1,X3)),
inference(step,[status(thm)],[t89939,t11]) ).
cnf(t89941,plain,
meet(X1,meet(X2,join(X1,join(X2,X3)))) = meet(X1,meet(X2,join(X2,X3))),
inference(step,[status(thm)],[t89940,t5963]) ).
cnf(t6207,plain,
meet(X1,meet(X2,join(X1,join(X2,X3)))) = meet(X1,meet(X2,join(X2,X3))),
inference(orient,[status(thm)],[t89941]) ).
cnf(t89951,plain,
meet(X1,meet(X2,join(X1,join(X2,X3)))) = meet(X1,meet(X2,join(X1,X3))),
inference(step,[status(thm)],[t6207,t6477]) ).
cnf(t6480,plain,
meet(X1,meet(X2,join(X1,join(X2,X3)))) = meet(X1,meet(X2,join(X1,X3))),
inference(orient,[status(thm)],[t89951]) ).
cnf(t90098,plain,
meet(X1,meet(X2,join(X1,join(X3,Y3)))) = meet(X1,meet(X2,join(X1,meet(X2,join(X2,meet(X3,Y3)))))),
inference(step,[status(thm)],[t10552,t6480]) ).
cnf(t90099,plain,
meet(X1,meet(X2,join(X1,join(X3,Y3)))) = meet(X1,meet(X2,join(X1,join(X2,meet(X3,Y3))))),
inference(step,[status(thm)],[t90098,t7008]) ).
cnf(t90100,plain,
meet(X1,meet(X2,join(X1,join(X3,Y3)))) = meet(X1,meet(X2,join(X1,meet(X3,Y3)))),
inference(step,[status(thm)],[t90099,t6480]) ).
cnf(t10768,plain,
meet(X1,meet(X2,join(X1,join(X3,Y3)))) = meet(X1,meet(X2,join(X1,meet(X3,Y3)))),
inference(orient,[status(thm)],[t90100]) ).
cnf(t10812,plain,
meet(X1,meet(X2,join(X1,meet(X3,meet(X3,Y3))))) = meet(X1,meet(X2,join(X1,meet(X3,join(X3,Y3))))),
inference(cp,[status(thm)],[t10768,t1337]) ).
cnf(t90443,plain,
meet(X1,meet(X2,join(X1,meet(X3,Y3)))) = meet(X1,meet(X2,join(X1,meet(X3,join(X3,Y3))))),
inference(step,[status(thm)],[t10812,t90]) ).
cnf(t39865,plain,
meet(X1,meet(X2,join(X1,meet(X3,join(X3,Y3))))) = meet(X1,meet(X2,join(X1,meet(X3,Y3)))),
inference(orient,[status(thm)],[t90443]) ).
cnf(t90532,plain,
meet(X1,meet(join(X2,X3),join(X1,meet(Y3,X2)))) = meet(X1,meet(join(X2,X3),join(Y3,meet(X1,join(X2,X3))))),
inference(step,[status(thm)],[t40465,t39865]) ).
cnf(t90533,plain,
meet(X1,meet(join(X2,X3),join(X1,meet(X2,Y3)))) = meet(X1,meet(join(X2,X3),join(Y3,meet(X1,join(X2,X3))))),
inference(step,[status(thm)],[t90532,t61]) ).
cnf(t90534,plain,
meet(X1,meet(join(X2,X3),join(X1,meet(X2,Y3)))) = meet(X1,meet(join(X2,X3),join(X1,Y3))),
inference(step,[status(thm)],[t90533,t40421]) ).
cnf(t90535,plain,
meet(X1,meet(join(X2,X3),join(X1,meet(X2,Y3)))) = meet(X1,meet(join(X1,Y3),join(X2,X3))),
inference(step,[status(thm)],[t90534,t61]) ).
cnf(t53559,plain,
meet(X1,meet(join(X2,X3),join(X1,meet(X2,Y3)))) = meet(X1,meet(join(X1,Y3),join(X2,X3))),
inference(orient,[status(thm)],[t90535]) ).
cnf(t53806,plain,
meet(X1,meet(join(X1,X2),join(X3,Y3))) = meet(X1,meet(join(X3,Y3),join(X1,meet(X2,X3)))),
inference(cp,[status(thm)],[t53559,t61]) ).
cnf(t58694,plain,
meet(X1,meet(join(X2,X3),join(X1,meet(Y3,X2)))) = meet(X1,meet(join(X1,Y3),join(X2,X3))),
inference(orient,[status(thm)],[t53806]) ).
cnf(t58726,plain,
meet(X1,meet(join(X1,X2),join(X3,X3))) = meet(X1,meet(X3,join(X1,meet(X2,X3)))),
inference(cp,[status(thm)],[t58694,t9]) ).
cnf(t90570,plain,
meet(X1,meet(join(X1,X2),X3)) = meet(X1,meet(X3,join(X1,meet(X2,X3)))),
inference(step,[status(thm)],[t58726,t9]) ).
cnf(t90571,plain,
meet(X1,meet(X3,join(X1,X2))) = meet(X1,meet(X3,join(X1,meet(X2,X3)))),
inference(step,[status(thm)],[t90570,t61]) ).
cnf(t59104,plain,
meet(X1,meet(X2,join(X1,meet(X3,X2)))) = meet(X1,meet(X2,join(X1,X3))),
inference(orient,[status(thm)],[t90571]) ).
cnf(t59272,plain,
meet(X1,meet(join(X2,meet(X3,Y3)),join(X1,join(X2,X3)))) = meet(X1,meet(join(X2,meet(X3,Y3)),join(X1,join(X2,meet(X3,Y3))))),
inference(cp,[status(thm)],[t59104,t117]) ).
cnf(t90577,plain,
meet(X1,meet(join(X2,meet(X3,Y3)),join(X1,meet(X2,X3)))) = meet(X1,meet(join(X2,meet(X3,Y3)),join(X1,join(X2,meet(X3,Y3))))),
inference(step,[status(thm)],[t59272,t10768]) ).
cnf(t90578,plain,
meet(X1,meet(join(X1,X3),join(X2,meet(X3,Y3)))) = meet(X1,meet(join(X2,meet(X3,Y3)),join(X1,join(X2,meet(X3,Y3))))),
inference(step,[status(thm)],[t90577,t53559]) ).
cnf(t90579,plain,
meet(X1,meet(join(X1,X3),join(X2,meet(X3,Y3)))) = meet(X1,meet(join(X2,meet(X3,Y3)),join(X1,meet(X2,meet(X3,Y3))))),
inference(step,[status(thm)],[t90578,t10768]) ).
cnf(t90580,plain,
meet(X1,meet(join(X1,X3),join(X2,meet(X3,Y3)))) = meet(X1,meet(join(X1,meet(X3,Y3)),join(X2,meet(X3,Y3)))),
inference(step,[status(thm)],[t90579,t53559]) ).
cnf(t1427,plain,
meet(X1,join(X2,X3)) = meet(X1,meet(join(X2,X3),join(X1,X3))),
inference(cp,[status(thm)],[t1383,t11]) ).
cnf(t89845,plain,
meet(X1,join(X2,X3)) = meet(X1,meet(join(X1,X3),join(X2,X3))),
inference(step,[status(thm)],[t1427,t61]) ).
cnf(t1580,plain,
meet(X1,meet(join(X1,X2),join(X3,X2))) = meet(X1,join(X3,X2)),
inference(orient,[status(thm)],[t89845]) ).
cnf(t90581,plain,
meet(X1,meet(join(X1,X3),join(X2,meet(X3,Y3)))) = meet(X1,join(X2,meet(X3,Y3))),
inference(step,[status(thm)],[t90580,t1580]) ).
cnf(t59804,plain,
meet(X1,meet(join(X1,X2),join(X3,meet(X2,Y3)))) = meet(X1,join(X3,meet(X2,Y3))),
inference(orient,[status(thm)],[t90581]) ).
cnf(t582,plain,
meet(X1,meet(X2,join(X2,meet(X1,X2)))) = meet(X1,join(X2,meet(X1,X2))),
inference(cp,[status(thm)],[t578,t10]) ).
cnf(t89791,plain,
meet(X1,meet(X2,X2)) = meet(X1,join(X2,meet(X1,X2))),
inference(step,[status(thm)],[t582,t578]) ).
cnf(t89792,plain,
meet(X1,X2) = meet(X1,join(X2,meet(X1,X2))),
inference(step,[status(thm)],[t89791,t10]) ).
cnf(t613,plain,
meet(X1,join(X2,meet(X1,X2))) = meet(X1,X2),
inference(orient,[status(thm)],[t89792]) ).
cnf(t3612,plain,
meet(X1,join(X2,X3)) = meet(X1,join(X2,join(X3,meet(X2,X1)))),
inference(cp,[status(thm)],[t613,t3512]) ).
cnf(t89880,plain,
meet(X1,join(X2,X3)) = meet(X1,join(X2,join(X3,meet(X1,X2)))),
inference(step,[status(thm)],[t3612,t61]) ).
cnf(t3645,plain,
meet(X1,join(X2,join(X3,meet(X1,X2)))) = meet(X1,join(X2,X3)),
inference(orient,[status(thm)],[t89880]) ).
cnf(t3666,plain,
meet(X1,join(join(X2,X3),meet(X1,X3))) = meet(X1,join(join(X2,X3),meet(X1,join(X2,X3)))),
inference(cp,[status(thm)],[t3645,t243]) ).
cnf(t89881,plain,
meet(X1,join(meet(X1,X3),join(X2,X3))) = meet(X1,join(join(X2,X3),meet(X1,join(X2,X3)))),
inference(step,[status(thm)],[t3666,t11]) ).
cnf(t89882,plain,
meet(X1,join(X3,join(meet(X1,X3),X2))) = meet(X1,join(join(X2,X3),meet(X1,join(X2,X3)))),
inference(step,[status(thm)],[t89881,t12]) ).
cnf(t89883,plain,
meet(X1,join(X2,join(X3,meet(X1,X3)))) = meet(X1,join(join(X2,X3),meet(X1,join(X2,X3)))),
inference(step,[status(thm)],[t89882,t12]) ).
cnf(t89884,plain,
meet(X1,join(X2,join(X3,meet(X1,X3)))) = meet(X1,join(X2,X3)),
inference(step,[status(thm)],[t89883,t613]) ).
cnf(t3735,plain,
meet(X1,join(X2,join(X3,meet(X1,X3)))) = meet(X1,join(X2,X3)),
inference(orient,[status(thm)],[t89884]) ).
cnf(t3767,plain,
meet(X1,join(X2,X3)) = meet(X1,join(X2,join(X3,meet(X3,X1)))),
inference(cp,[status(thm)],[t3735,t61]) ).
cnf(t89885,plain,
meet(X1,join(X2,X3)) = meet(X1,join(X2,meet(X3,join(X3,X1)))),
inference(step,[status(thm)],[t3767,t1337]) ).
cnf(t89886,plain,
meet(X1,join(X2,X3)) = meet(X1,join(X2,meet(X3,join(X1,X3)))),
inference(step,[status(thm)],[t89885,t11]) ).
cnf(t3811,plain,
meet(X1,join(X2,meet(X3,join(X1,X3)))) = meet(X1,join(X2,X3)),
inference(orient,[status(thm)],[t89886]) ).
cnf(t3822,plain,
meet(X1,join(X2,meet(X3,Y3))) = meet(X1,join(X2,meet(meet(X3,Y3),join(X3,X1)))),
inference(cp,[status(thm)],[t3811,t1699]) ).
cnf(t90210,plain,
meet(X1,join(X2,meet(X3,Y3))) = meet(X1,join(X2,meet(X3,meet(Y3,join(Y3,X1))))),
inference(step,[status(thm)],[t3822,t5963]) ).
cnf(t90211,plain,
meet(X1,join(X2,meet(X3,Y3))) = meet(X1,join(X2,meet(X3,meet(Y3,join(X3,X1))))),
inference(step,[status(thm)],[t90210,t6477]) ).
cnf(t90212,plain,
meet(X1,join(X2,meet(X3,Y3))) = meet(X1,join(X2,meet(X3,meet(Y3,join(X1,X3))))),
inference(step,[status(thm)],[t90211,t11]) ).
cnf(t17183,plain,
meet(X1,join(X2,meet(X3,meet(Y3,join(X1,X3))))) = meet(X1,join(X2,meet(X3,Y3))),
inference(orient,[status(thm)],[t90212]) ).
cnf(t17221,plain,
meet(X1,join(X2,meet(meet(X3,Y3),join(X1,Y3)))) = meet(X1,join(X2,meet(meet(X3,Y3),join(X1,meet(X3,Y3))))),
inference(cp,[status(thm)],[t17183,t534]) ).
cnf(t90289,plain,
meet(X1,join(X2,meet(meet(X3,Y3),join(X1,Y3)))) = meet(X1,join(X2,meet(X3,Y3))),
inference(step,[status(thm)],[t17221,t3811]) ).
cnf(t24711,plain,
meet(X1,join(X2,meet(meet(X3,Y3),join(X1,Y3)))) = meet(X1,join(X2,meet(X3,Y3))),
inference(orient,[status(thm)],[t90289]) ).
cnf(t24745,plain,
meet(X1,join(X2,meet(X3,Y3))) = meet(X1,join(X2,meet(join(X1,Y3),meet(X3,Y3)))),
inference(cp,[status(thm)],[t24711,t61]) ).
cnf(t90333,plain,
meet(X1,join(X2,meet(X3,Y3))) = meet(X1,join(X2,meet(Y3,meet(join(X1,Y3),X3)))),
inference(step,[status(thm)],[t24745,t66]) ).
cnf(t90334,plain,
meet(X1,join(X2,meet(X3,Y3))) = meet(X1,join(X2,meet(X3,meet(Y3,join(X1,Y3))))),
inference(step,[status(thm)],[t90333,t66]) ).
cnf(t29283,plain,
meet(X1,join(X2,meet(X3,meet(Y3,join(X1,Y3))))) = meet(X1,join(X2,meet(X3,Y3))),
inference(orient,[status(thm)],[t90334]) ).
cnf(t30260,plain,
join(X1,meet(X2,meet(X3,join(X3,X3)))) = join(X1,meet(X3,join(X1,meet(X2,X3)))),
inference(cp,[status(thm)],[t30254,t29283]) ).
cnf(t90340,plain,
join(X1,meet(X2,meet(X3,join(X2,X3)))) = join(X1,meet(X3,join(X1,meet(X2,X3)))),
inference(step,[status(thm)],[t30260,t6477]) ).
cnf(t585,plain,
meet(X1,meet(X2,join(X2,X1))) = meet(X1,join(X2,meet(X1,X2))),
inference(cp,[status(thm)],[t578,t117]) ).
cnf(t89793,plain,
meet(X1,meet(X2,join(X1,X2))) = meet(X1,join(X2,meet(X1,X2))),
inference(step,[status(thm)],[t585,t11]) ).
cnf(t89794,plain,
meet(X1,meet(X2,join(X1,X2))) = meet(X1,X2),
inference(step,[status(thm)],[t89793,t613]) ).
cnf(t637,plain,
meet(X1,meet(X2,join(X1,X2))) = meet(X1,X2),
inference(orient,[status(thm)],[t89794]) ).
cnf(t90341,plain,
join(X1,meet(X2,X3)) = join(X1,meet(X3,join(X1,meet(X2,X3)))),
inference(step,[status(thm)],[t90340,t637]) ).
cnf(t30482,plain,
join(X1,meet(X2,join(X1,meet(X3,X2)))) = join(X1,meet(X3,X2)),
inference(orient,[status(thm)],[t90341]) ).
cnf(t59942,plain,
meet(X1,join(X2,meet(X3,join(X2,meet(Y3,X3))))) = meet(X1,meet(join(X1,X3),join(X2,meet(Y3,X3)))),
inference(cp,[status(thm)],[t59804,t30482]) ).
cnf(t90582,plain,
meet(X1,join(X2,meet(Y3,X3))) = meet(X1,meet(join(X1,X3),join(X2,meet(Y3,X3)))),
inference(step,[status(thm)],[t59942,t30482]) ).
cnf(t60137,plain,
meet(X1,meet(join(X1,X2),join(X3,meet(Y3,X2)))) = meet(X1,join(X3,meet(Y3,X2))),
inference(orient,[status(thm)],[t90582]) ).
cnf(t90632,plain,
meet(X1,join(X2,X3)) = meet(X1,join(X3,meet(X1,X2))),
inference(step,[status(thm)],[t90631,t60137]) ).
cnf(t74574,plain,
meet(X1,join(X2,meet(X1,X3))) = meet(X1,join(X3,X2)),
inference(orient,[status(thm)],[t90632]) ).
cnf(t90638,plain,
join(X1,meet(X2,join(X3,X1))) = join(X1,meet(X2,X3)),
inference(step,[status(thm)],[t26241,t74574]) ).
cnf(t75009,plain,
join(X1,meet(X2,join(X3,X1))) = join(X1,meet(X2,X3)),
inference(rw,[status(thm)],[t90638]) ).
cnf(t90644,plain,
join(X1,meet(X2,join(X1,X3))) = join(X1,meet(X2,X3)),
inference(step,[status(thm)],[t75009,t11]) ).
cnf(t75015,plain,
join(X1,meet(X2,join(X1,X3))) = join(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t90644]) ).
cnf(t74903,plain,
meet(X1,meet(X2,join(X3,meet(join(X1,X3),Y3)))) = meet(X1,meet(X2,meet(join(X1,X3),join(Y3,X3)))),
inference(cp,[status(thm)],[t11419,t74574]) ).
cnf(t90715,plain,
meet(X1,meet(X2,join(X3,meet(Y3,join(X1,X3))))) = meet(X1,meet(X2,meet(join(X1,X3),join(Y3,X3)))),
inference(step,[status(thm)],[t74903,t61]) ).
cnf(t90716,plain,
meet(X1,meet(X2,join(X3,meet(Y3,join(X1,X3))))) = meet(X1,meet(X2,join(Y3,X3))),
inference(step,[status(thm)],[t90715,t9385]) ).
cnf(t90717,plain,
meet(X1,meet(X2,join(X3,meet(Y3,join(X1,X3))))) = meet(X1,meet(X2,join(X3,Y3))),
inference(step,[status(thm)],[t90716,t11]) ).
cnf(t79827,plain,
meet(X1,meet(X2,join(X3,meet(Y3,join(X1,X3))))) = meet(X1,meet(X2,join(X3,Y3))),
inference(orient,[status(thm)],[t90717]) ).
cnf(t1732,plain,
meet(meet(X1,X2),join(X3,meet(X1,X2))) = join(meet(meet(X1,X2),meet(X1,X2)),meet(meet(X1,X2),join(X1,X3))),
inference(cp,[status(thm)],[t243,t1699]) ).
cnf(t90120,plain,
meet(X1,meet(X2,join(X1,X3))) = join(meet(meet(X1,X2),meet(X1,X2)),meet(meet(X1,X2),join(X1,X3))),
inference(step,[status(thm)],[t1732,t6478]) ).
cnf(t90121,plain,
meet(X1,meet(X2,join(X1,X3))) = join(meet(X1,X2),meet(meet(X1,X2),join(X1,X3))),
inference(step,[status(thm)],[t90120,t10]) ).
cnf(t90122,plain,
meet(X1,meet(X2,join(X1,X3))) = meet(meet(X1,X2),join(meet(X1,X2),join(X1,X3))),
inference(step,[status(thm)],[t90121,t1337]) ).
cnf(t90123,plain,
meet(X1,meet(X2,join(X1,X3))) = meet(meet(X1,X2),join(meet(X1,X2),meet(X1,X3))),
inference(step,[status(thm)],[t90122,t10443]) ).
cnf(t11883,plain,
meet(meet(X1,X2),join(meet(X1,X2),meet(X1,X3))) = meet(X1,meet(X2,join(X1,X3))),
inference(orient,[status(thm)],[t90123]) ).
cnf(t12148,plain,
join(meet(X1,X2),meet(X3,join(meet(X1,Y3),X3))) = join(X3,meet(X1,meet(X2,join(X1,Y3)))),
inference(cp,[status(thm)],[t5470,t11883]) ).
cnf(t90495,plain,
join(meet(X1,X2),meet(X3,join(X3,meet(X1,Y3)))) = join(X3,meet(X1,meet(X2,join(X1,Y3)))),
inference(step,[status(thm)],[t12148,t11]) ).
cnf(t44344,plain,
join(meet(X1,X2),meet(X3,join(X3,meet(X1,Y3)))) = join(X3,meet(X1,meet(X2,join(X1,Y3)))),
inference(orient,[status(thm)],[t90495]) ).
cnf(t1810,plain,
join(X1,meet(X2,X3)) = join(X1,meet(join(X1,X2),meet(X2,X3))),
inference(cp,[status(thm)],[t1807,t61]) ).
cnf(t89850,plain,
join(X1,meet(X2,X3)) = join(X1,meet(X3,meet(join(X1,X2),X2))),
inference(step,[status(thm)],[t1810,t66]) ).
cnf(t89851,plain,
join(X1,meet(X2,X3)) = join(X1,meet(X2,meet(X3,join(X1,X2)))),
inference(step,[status(thm)],[t89850,t66]) ).
cnf(t1864,plain,
join(X1,meet(X2,meet(X3,join(X1,X2)))) = join(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t89851]) ).
cnf(t1871,plain,
join(X1,meet(meet(X2,X3),join(X1,X3))) = join(X1,meet(meet(X2,X3),join(X1,meet(X2,X3)))),
inference(cp,[status(thm)],[t1864,t534]) ).
cnf(t89852,plain,
join(X1,meet(meet(X2,X3),join(X1,X3))) = join(X1,meet(X2,X3)),
inference(step,[status(thm)],[t1871,t301]) ).
cnf(t1926,plain,
join(X1,meet(meet(X2,X3),join(X1,X3))) = join(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t89852]) ).
cnf(t1929,plain,
join(X1,meet(X2,X3)) = join(X1,meet(join(X1,X3),meet(X2,X3))),
inference(cp,[status(thm)],[t1926,t61]) ).
cnf(t89853,plain,
join(X1,meet(X2,X3)) = join(X1,meet(X3,meet(join(X1,X3),X2))),
inference(step,[status(thm)],[t1929,t66]) ).
cnf(t89854,plain,
join(X1,meet(X2,X3)) = join(X1,meet(X2,meet(X3,join(X1,X3)))),
inference(step,[status(thm)],[t89853,t66]) ).
cnf(t2000,plain,
join(X1,meet(X2,meet(X3,join(X1,X3)))) = join(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t89854]) ).
cnf(t2056,plain,
join(X1,join(meet(X2,meet(X3,join(X1,X3))),Y3)) = join(Y3,join(X1,meet(X2,X3))),
inference(cp,[status(thm)],[t12,t2000]) ).
cnf(t90141,plain,
join(X1,join(Y3,meet(X2,meet(X3,join(X1,X3))))) = join(Y3,join(X1,meet(X2,X3))),
inference(step,[status(thm)],[t2056,t11]) ).
cnf(t90142,plain,
join(X1,join(Y3,meet(X2,meet(X3,join(X1,X3))))) = join(X1,join(meet(X2,X3),Y3)),
inference(step,[status(thm)],[t90141,t12]) ).
cnf(t90143,plain,
join(X1,join(Y3,meet(X2,meet(X3,join(X1,X3))))) = join(X1,join(Y3,meet(X2,X3))),
inference(step,[status(thm)],[t90142,t11]) ).
cnf(t13110,plain,
join(X1,join(X2,meet(X3,meet(Y3,join(X1,Y3))))) = join(X1,join(X2,meet(X3,Y3))),
inference(orient,[status(thm)],[t90143]) ).
cnf(t122,plain,
join(meet(X1,X2),meet(meet(X1,join(X2,X3)),Y3)) = meet(meet(X1,join(X2,X3)),join(meet(X1,X2),meet(meet(X1,join(X2,X3)),Y3))),
inference(cp,[status(thm)],[t117,t33]) ).
cnf(t90176,plain,
join(meet(X1,X2),meet(Y3,meet(X1,join(X2,X3)))) = meet(meet(X1,join(X2,X3)),join(meet(X1,X2),meet(meet(X1,join(X2,X3)),Y3))),
inference(step,[status(thm)],[t122,t61]) ).
cnf(t90177,plain,
join(meet(X1,X2),meet(X1,meet(join(X2,X3),Y3))) = meet(meet(X1,join(X2,X3)),join(meet(X1,X2),meet(meet(X1,join(X2,X3)),Y3))),
inference(step,[status(thm)],[t90176,t66]) ).
cnf(t90178,plain,
join(meet(X1,X2),meet(X1,meet(Y3,join(X2,X3)))) = meet(meet(X1,join(X2,X3)),join(meet(X1,X2),meet(meet(X1,join(X2,X3)),Y3))),
inference(step,[status(thm)],[t90177,t61]) ).
cnf(t90179,plain,
join(meet(X1,X2),meet(X1,meet(Y3,join(X2,X3)))) = meet(meet(X1,join(X2,X3)),join(meet(X1,X2),meet(Y3,meet(X1,join(X2,X3))))),
inference(step,[status(thm)],[t90178,t61]) ).
cnf(t90180,plain,
join(meet(X1,X2),meet(X1,meet(Y3,join(X2,X3)))) = meet(meet(X1,join(X2,X3)),join(meet(X1,X2),meet(X1,meet(join(X2,X3),Y3)))),
inference(step,[status(thm)],[t90179,t66]) ).
cnf(t90181,plain,
join(meet(X1,X2),meet(X1,meet(Y3,join(X2,X3)))) = meet(meet(X1,join(X2,X3)),join(meet(X1,X2),meet(X1,meet(Y3,join(X2,X3))))),
inference(step,[status(thm)],[t90180,t61]) ).
cnf(t14956,plain,
meet(meet(X1,join(X2,X3)),join(meet(X1,X2),meet(X1,meet(Y3,join(X2,X3))))) = join(meet(X1,X2),meet(X1,meet(Y3,join(X2,X3)))),
inference(orient,[status(thm)],[t90181]) ).
cnf(t15063,plain,
join(meet(X1,X2),meet(X1,meet(X3,join(X2,meet(X1,X2))))) = meet(meet(X1,join(X2,meet(X1,X2))),join(meet(X1,X2),meet(X1,meet(X2,X3)))),
inference(cp,[status(thm)],[t14956,t578]) ).
cnf(t90182,plain,
join(meet(X1,X2),meet(X1,meet(X2,X3))) = meet(meet(X1,join(X2,meet(X1,X2))),join(meet(X1,X2),meet(X1,meet(X2,X3)))),
inference(step,[status(thm)],[t15063,t578]) ).
cnf(t90183,plain,
join(meet(X1,X2),meet(X1,meet(X2,X3))) = meet(meet(X1,X2),join(meet(X1,X2),meet(X1,meet(X2,X3)))),
inference(step,[status(thm)],[t90182,t613]) ).
cnf(t90184,plain,
join(meet(X1,X2),meet(X1,meet(X2,X3))) = meet(X1,meet(X2,join(X1,meet(X2,X3)))),
inference(step,[status(thm)],[t90183,t11883]) ).
cnf(t90185,plain,
join(meet(X1,X2),meet(X1,meet(X2,X3))) = meet(X1,meet(X2,join(X1,X3))),
inference(step,[status(thm)],[t90184,t7008]) ).
cnf(t15227,plain,
join(meet(X1,X2),meet(X1,meet(X2,X3))) = meet(X1,meet(X2,join(X1,X3))),
inference(orient,[status(thm)],[t90185]) ).
cnf(t15464,plain,
join(X1,join(meet(X2,X3),meet(X2,X3))) = join(X1,meet(X2,meet(X3,join(X2,join(X1,X3))))),
inference(cp,[status(thm)],[t13110,t15227]) ).
cnf(t90189,plain,
join(X1,meet(X2,X3)) = join(X1,meet(X2,meet(X3,join(X2,join(X1,X3))))),
inference(step,[status(thm)],[t15464,t9]) ).
cnf(t90190,plain,
join(X1,meet(X2,X3)) = join(X1,meet(X2,meet(X3,join(X2,meet(X1,X3))))),
inference(step,[status(thm)],[t90189,t10768]) ).
cnf(t15490,plain,
join(X1,meet(X2,meet(X3,join(X2,meet(X1,X3))))) = join(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t90190]) ).
cnf(t44482,plain,
join(X1,meet(X2,meet(X3,join(X2,meet(Y3,join(X2,meet(X1,Y3))))))) = join(meet(X2,X3),meet(X1,join(X1,meet(X2,Y3)))),
inference(cp,[status(thm)],[t44344,t15490]) ).
cnf(t90088,plain,
meet(X1,join(X1,meet(X2,join(X2,X3)))) = meet(X1,join(X1,meet(X2,X3))),
inference(step,[status(thm)],[t10161,t10443]) ).
cnf(t10446,plain,
meet(X1,join(X1,meet(X2,join(X2,X3)))) = meet(X1,join(X1,meet(X2,X3))),
inference(orient,[status(thm)],[t90088]) ).
cnf(t10540,plain,
meet(X1,join(X1,meet(X2,join(X3,Y3)))) = meet(X1,join(X1,meet(X2,join(X2,meet(X3,Y3))))),
inference(cp,[status(thm)],[t10446,t10443]) ).
cnf(t90094,plain,
meet(X1,join(X1,meet(X2,join(X3,Y3)))) = meet(X1,join(X1,meet(X2,meet(X3,Y3)))),
inference(step,[status(thm)],[t10540,t10446]) ).
cnf(t10593,plain,
meet(X1,join(X1,meet(X2,join(X3,Y3)))) = meet(X1,join(X1,meet(X2,meet(X3,Y3)))),
inference(orient,[status(thm)],[t90094]) ).
cnf(t10647,plain,
meet(X1,join(X1,meet(X2,meet(X3,meet(X3,Y3))))) = meet(X1,join(X1,meet(X2,meet(X3,join(X3,Y3))))),
inference(cp,[status(thm)],[t10593,t1337]) ).
cnf(t90441,plain,
meet(X1,join(X1,meet(X2,meet(X3,Y3)))) = meet(X1,join(X1,meet(X2,meet(X3,join(X3,Y3))))),
inference(step,[status(thm)],[t10647,t90]) ).
cnf(t90442,plain,
meet(X1,join(X1,meet(X2,meet(X3,Y3)))) = meet(X1,join(X1,meet(X2,meet(X3,join(X2,Y3))))),
inference(step,[status(thm)],[t90441,t6477]) ).
cnf(t39521,plain,
meet(X1,join(X1,meet(X2,meet(X3,join(X2,Y3))))) = meet(X1,join(X1,meet(X2,meet(X3,Y3)))),
inference(orient,[status(thm)],[t90442]) ).
cnf(t39525,plain,
meet(meet(X1,X2),join(meet(X1,X2),meet(X1,meet(X3,Y3)))) = meet(X1,meet(X2,join(X1,meet(X3,join(X1,Y3))))),
inference(cp,[status(thm)],[t39521,t11883]) ).
cnf(t90527,plain,
meet(X1,meet(X2,join(X1,meet(X3,Y3)))) = meet(X1,meet(X2,join(X1,meet(X3,join(X1,Y3))))),
inference(step,[status(thm)],[t39525,t11883]) ).
cnf(t52830,plain,
meet(X1,meet(X2,join(X1,meet(X3,join(X1,Y3))))) = meet(X1,meet(X2,join(X1,meet(X3,Y3)))),
inference(orient,[status(thm)],[t90527]) ).
cnf(t90544,plain,
join(X1,meet(X2,meet(X3,join(X2,meet(Y3,meet(X1,Y3)))))) = join(meet(X2,X3),meet(X1,join(X1,meet(X2,Y3)))),
inference(step,[status(thm)],[t44482,t52830]) ).
cnf(t90545,plain,
join(X1,meet(X2,meet(X3,join(X2,meet(X1,meet(Y3,Y3)))))) = join(meet(X2,X3),meet(X1,join(X1,meet(X2,Y3)))),
inference(step,[status(thm)],[t90544,t66]) ).
cnf(t90546,plain,
join(X1,meet(X2,meet(X3,join(X2,meet(X1,Y3))))) = join(meet(X2,X3),meet(X1,join(X1,meet(X2,Y3)))),
inference(step,[status(thm)],[t90545,t10]) ).
cnf(t90547,plain,
join(X1,meet(X2,meet(X3,join(X2,meet(X1,Y3))))) = join(X1,meet(X2,meet(X3,join(X2,Y3)))),
inference(step,[status(thm)],[t90546,t44344]) ).
cnf(t55055,plain,
join(X1,meet(X2,meet(X3,join(X2,meet(X1,Y3))))) = join(X1,meet(X2,meet(X3,join(X2,Y3)))),
inference(orient,[status(thm)],[t90547]) ).
cnf(t74600,plain,
meet(X1,join(meet(X2,join(X1,meet(X3,Y3))),X3)) = meet(X1,join(X3,meet(X1,meet(X2,join(X1,Y3))))),
inference(cp,[status(thm)],[t74574,t55055]) ).
cnf(t90760,plain,
meet(X1,join(X3,meet(X2,join(X1,meet(X3,Y3))))) = meet(X1,join(X3,meet(X1,meet(X2,join(X1,Y3))))),
inference(step,[status(thm)],[t74600,t11]) ).
cnf(t90761,plain,
meet(X1,join(X3,meet(X2,join(X1,meet(X3,Y3))))) = meet(X1,join(meet(X2,join(X1,Y3)),X3)),
inference(step,[status(thm)],[t90760,t74574]) ).
cnf(t90762,plain,
meet(X1,join(X3,meet(X2,join(X1,meet(X3,Y3))))) = meet(X1,join(X3,meet(X2,join(X1,Y3)))),
inference(step,[status(thm)],[t90761,t11]) ).
cnf(t86666,plain,
meet(X1,join(X2,meet(X3,join(X1,meet(X2,Y3))))) = meet(X1,join(X2,meet(X3,join(X1,Y3)))),
inference(orient,[status(thm)],[t90762]) ).
cnf(t256,plain,
meet(X1,join(X2,meet(X3,join(X3,X2)))) = join(meet(X1,meet(X3,join(X3,X2))),meet(X1,join(X3,X2))),
inference(cp,[status(thm)],[t243,t175]) ).
cnf(t61823,plain,
join(meet(X1,join(X2,X3)),meet(X1,meet(X2,join(X1,X3)))) = meet(X1,join(X2,X3)),
inference(orient,[status(thm)],[t256]) ).
cnf(t74630,plain,
meet(X1,join(meet(X2,join(X1,X3)),meet(X1,join(X2,X3)))) = meet(X1,meet(X1,join(X2,X3))),
inference(cp,[status(thm)],[t74574,t61823]) ).
cnf(t90695,plain,
meet(X1,join(join(X2,X3),meet(X2,join(X1,X3)))) = meet(X1,meet(X1,join(X2,X3))),
inference(step,[status(thm)],[t74630,t74574]) ).
cnf(t90696,plain,
meet(X1,join(join(X2,X3),meet(X2,join(X1,X3)))) = meet(X1,join(X2,X3)),
inference(step,[status(thm)],[t90695,t90]) ).
cnf(t77679,plain,
meet(X1,join(join(X2,X3),meet(X2,join(X1,X3)))) = meet(X1,join(X2,X3)),
inference(orient,[status(thm)],[t90696]) ).
cnf(t86712,plain,
meet(join(X1,X2),join(X1,meet(X3,join(join(X1,X2),join(X3,X2))))) = meet(join(X1,X2),join(X1,meet(X3,join(X1,X2)))),
inference(cp,[status(thm)],[t86666,t77679]) ).
cnf(t10068,plain,
meet(X1,join(X2,join(X3,meet(Y3,join(X2,Y3))))) = meet(X1,meet(join(X1,X3),join(X2,join(Y3,X3)))),
inference(cp,[status(thm)],[t10010,t272]) ).
cnf(t90254,plain,
meet(X1,join(X2,join(Y3,X3))) = meet(X1,meet(join(X1,X3),join(X2,join(Y3,X3)))),
inference(step,[status(thm)],[t10068,t272]) ).
cnf(t20955,plain,
meet(X1,meet(join(X1,X2),join(X3,join(Y3,X2)))) = meet(X1,join(X3,join(Y3,X2))),
inference(orient,[status(thm)],[t90254]) ).
cnf(t29305,plain,
meet(X1,join(X2,meet(X3,join(X3,Y3)))) = meet(X1,join(X2,meet(X3,join(X1,join(X3,Y3))))),
inference(cp,[status(thm)],[t29283,t20955]) ).
cnf(t50306,plain,
meet(X1,join(X2,meet(X3,join(X1,join(X3,Y3))))) = meet(X1,join(X2,meet(X3,join(X3,Y3)))),
inference(orient,[status(thm)],[t29305]) ).
cnf(t90763,plain,
meet(join(X1,X2),join(X1,meet(X3,join(X3,X2)))) = meet(join(X1,X2),join(X1,meet(X3,join(X1,X2)))),
inference(step,[status(thm)],[t86712,t50306]) ).
cnf(t90764,plain,
meet(join(X1,X2),join(X1,meet(X3,join(X2,X3)))) = meet(join(X1,X2),join(X1,meet(X3,join(X1,X2)))),
inference(step,[status(thm)],[t90763,t11]) ).
cnf(t4160,plain,
meet(join(X1,X2),join(X3,X1)) = meet(join(X1,X2),join(X3,meet(X1,join(X1,X2)))),
inference(cp,[status(thm)],[t1521,t4083]) ).
cnf(t90213,plain,
meet(join(X1,X2),join(X1,X3)) = meet(join(X1,X2),join(X3,meet(X1,join(X1,X2)))),
inference(step,[status(thm)],[t4160,t11]) ).
cnf(t90214,plain,
meet(join(X1,X2),join(X1,X3)) = meet(join(X1,X2),join(X1,meet(X3,join(X2,X3)))),
inference(step,[status(thm)],[t90213,t5470]) ).
cnf(t17396,plain,
meet(join(X1,X2),join(X1,meet(X3,join(X2,X3)))) = meet(join(X1,X2),join(X1,X3)),
inference(orient,[status(thm)],[t90214]) ).
cnf(t90765,plain,
meet(join(X1,X2),join(X1,X3)) = meet(join(X1,X2),join(X1,meet(X3,join(X1,X2)))),
inference(step,[status(thm)],[t90764,t17396]) ).
cnf(t90766,plain,
meet(join(X1,X2),join(X1,X3)) = join(X1,meet(X3,join(X1,X2))),
inference(step,[status(thm)],[t90765,t7317]) ).
cnf(t90767,plain,
meet(join(X1,X2),join(X1,X3)) = join(X1,meet(X3,X2)),
inference(step,[status(thm)],[t90766,t75015]) ).
cnf(t90768,plain,
meet(join(X1,X2),join(X1,X3)) = join(X1,meet(X2,X3)),
inference(step,[status(thm)],[t90767,t61]) ).
cnf(t87098,plain,
meet(join(X1,X2),join(X1,X3)) = join(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t90768]) ).
cnf(t87507,plain,
meet(X1,meet(join(X2,X3),join(X2,Y3))) = meet(X1,join(X2,meet(X3,meet(Y3,join(X1,X2))))),
inference(cp,[status(thm)],[t79827,t87098]) ).
cnf(t90787,plain,
meet(X1,join(X2,meet(X3,Y3))) = meet(X1,join(X2,meet(X3,meet(Y3,join(X1,X2))))),
inference(step,[status(thm)],[t87507,t87098]) ).
cnf(t88085,plain,
meet(X1,join(X2,meet(X3,meet(Y3,join(X1,X2))))) = meet(X1,join(X2,meet(X3,Y3))),
inference(orient,[status(thm)],[t90787]) ).
cnf(t6773,plain,
meet(join(X1,X2),join(X2,meet(X1,join(X2,X2)))) = join(meet(X1,X2),meet(X2,join(X1,X2))),
inference(cp,[status(thm)],[t6704,t10]) ).
cnf(t89957,plain,
meet(join(X1,X2),join(X2,meet(X1,X2))) = join(meet(X1,X2),meet(X2,join(X1,X2))),
inference(step,[status(thm)],[t6773,t9]) ).
cnf(t89958,plain,
meet(join(X1,X2),join(X2,meet(X1,X2))) = join(X2,meet(X1,X2)),
inference(step,[status(thm)],[t89957,t4282]) ).
cnf(t6881,plain,
meet(join(X1,X2),join(X2,meet(X1,X2))) = join(X2,meet(X1,X2)),
inference(orient,[status(thm)],[t89958]) ).
cnf(t88166,plain,
meet(X1,join(meet(X2,X1),meet(X3,join(X2,X1)))) = meet(X1,join(meet(X2,X1),meet(X3,join(X1,meet(X2,X1))))),
inference(cp,[status(thm)],[t88085,t6881]) ).
cnf(t90789,plain,
meet(X1,join(meet(X1,X2),meet(X3,join(X2,X1)))) = meet(X1,join(meet(X2,X1),meet(X3,join(X1,meet(X2,X1))))),
inference(step,[status(thm)],[t88166,t61]) ).
cnf(t90790,plain,
meet(X1,join(meet(X1,X2),meet(X3,join(X1,X2)))) = meet(X1,join(meet(X2,X1),meet(X3,join(X1,meet(X2,X1))))),
inference(step,[status(thm)],[t90789,t11]) ).
cnf(t74599,plain,
meet(X1,join(meet(X2,join(X1,X3)),X3)) = meet(X1,join(X3,meet(X1,X2))),
inference(cp,[status(thm)],[t74574,t18159]) ).
cnf(t90664,plain,
meet(X1,join(X3,meet(X2,join(X1,X3)))) = meet(X1,join(X3,meet(X1,X2))),
inference(step,[status(thm)],[t74599,t11]) ).
cnf(t90665,plain,
meet(X1,join(X3,meet(X2,join(X1,X3)))) = meet(X1,join(X2,X3)),
inference(step,[status(thm)],[t90664,t74574]) ).
cnf(t75406,plain,
meet(X1,join(X2,meet(X3,join(X1,X2)))) = meet(X1,join(X3,X2)),
inference(orient,[status(thm)],[t90665]) ).
cnf(t90791,plain,
meet(X1,join(meet(X1,X2),meet(X3,join(X1,X2)))) = meet(X1,join(X3,meet(X2,X1))),
inference(step,[status(thm)],[t90790,t75406]) ).
cnf(t90792,plain,
meet(X1,join(meet(X1,X2),meet(X3,join(X1,X2)))) = meet(X1,join(X3,meet(X1,X2))),
inference(step,[status(thm)],[t90791,t61]) ).
cnf(t90793,plain,
meet(X1,join(meet(X1,X2),meet(X3,join(X1,X2)))) = meet(X1,join(X2,X3)),
inference(step,[status(thm)],[t90792,t74574]) ).
cnf(t88833,plain,
meet(X1,join(meet(X1,X2),meet(X3,join(X1,X2)))) = meet(X1,join(X2,X3)),
inference(orient,[status(thm)],[t90793]) ).
cnf(t89094,plain,
join(meet(X1,X2),meet(X1,meet(X3,join(X1,X2)))) = join(meet(X1,X2),meet(X1,join(X2,X3))),
inference(cp,[status(thm)],[t75015,t88833]) ).
cnf(t4194,plain,
join(meet(X1,X2),meet(X3,join(X3,join(X3,X2)))) = join(meet(X1,X2),meet(X3,join(X3,meet(X1,X2)))),
inference(cp,[status(thm)],[t4187,t1926]) ).
cnf(t89905,plain,
join(meet(X1,X2),meet(X3,join(X3,X2))) = join(meet(X1,X2),meet(X3,join(X3,meet(X1,X2)))),
inference(step,[status(thm)],[t4194,t82]) ).
cnf(t89906,plain,
join(meet(X1,X2),meet(X3,join(X2,X3))) = join(meet(X1,X2),meet(X3,join(X3,meet(X1,X2)))),
inference(step,[status(thm)],[t89905,t11]) ).
cnf(t89907,plain,
join(meet(X1,X2),meet(X3,join(X2,X3))) = join(X3,meet(X1,X2)),
inference(step,[status(thm)],[t89906,t175]) ).
cnf(t4381,plain,
join(meet(X1,X2),meet(X3,join(X2,X3))) = join(X3,meet(X1,X2)),
inference(orient,[status(thm)],[t89907]) ).
cnf(t4415,plain,
join(meet(X1,X2),meet(X3,Y3)) = join(meet(X3,Y3),meet(meet(X1,X2),join(X1,Y3))),
inference(cp,[status(thm)],[t4381,t1699]) ).
cnf(t90222,plain,
join(meet(X1,X2),meet(X3,Y3)) = join(meet(X3,Y3),meet(X1,meet(X2,join(X2,Y3)))),
inference(step,[status(thm)],[t4415,t5963]) ).
cnf(t90223,plain,
join(meet(X1,X2),meet(X3,Y3)) = join(meet(X3,Y3),meet(X1,meet(X2,join(X1,Y3)))),
inference(step,[status(thm)],[t90222,t6477]) ).
cnf(t18380,plain,
join(meet(X1,X2),meet(X3,meet(Y3,join(X3,X2)))) = join(meet(X3,Y3),meet(X1,X2)),
inference(orient,[status(thm)],[t90223]) ).
cnf(t90794,plain,
join(meet(X1,X3),meet(X1,X2)) = join(meet(X1,X2),meet(X1,join(X2,X3))),
inference(step,[status(thm)],[t89094,t18380]) ).
cnf(t90795,plain,
join(meet(X1,X2),meet(X1,X3)) = join(meet(X1,X2),meet(X1,join(X2,X3))),
inference(step,[status(thm)],[t90794,t11]) ).
cnf(t90796,plain,
join(meet(X1,X2),meet(X1,X3)) = meet(X1,join(X2,X3)),
inference(step,[status(thm)],[t90795,t33]) ).
cnf(t89270,plain,
join(meet(X1,X2),meet(X1,X3)) = meet(X1,join(X2,X3)),
inference(orient,[status(thm)],[t90796]) ).
cnf(goal_0,negated_conjecture,
join(meet(a,b),meet(a,c)) != meet(a,join(b,c)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
meet(a,join(b,c)) != meet(a,join(b,c)),
inference(rw,[status(thm)],[goal_0,t89270]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LAT020-1 : TPTP v9.3.1. Released v2.2.0.
% 0.00/0.03 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.09/5.37 % Computer : n009.cluster.edu
% 0.09/5.37 % Model : x86_64 x86_64
% 0.09/5.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/5.37 % Memory : 8046.5625MB
% 0.09/5.37 % OS : Linux 6.8.0-71-generic
% 0.09/5.37 % CPULimit : 300
% 0.09/5.37 % WCLimit : 300
% 0.09/5.37 % DateTime : Wed Sep 23 20:02:18 UTC 2026
% 0.09/5.37 % CPUTime :
% 0.09/5.37 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 29.15/9.52 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 29.15/9.52 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------