%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : LAT009-1 : TPTP v9.3.1. Released v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n003.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:54:59 PM UTC 2026
% Result : Unsatisfiable 14.37s 7.23s
% Output : CNFRefutation 14.37s
% Verified :
% SZS Type : Refutation
% Derivation depth : 101
% Number of leaves : 10
% Syntax : Number of clauses : 242 ( 242 unt; 0 nHn; 3 RR)
% Number of literals : 242 ( 241 equ; 2 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 7 ( 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 : 747 ( 86 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t7,axiom,
meet(meet(X1,X2),X3) = meet(X1,meet(X2,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t4,axiom,
meet(X1,X2) = meet(X2,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t13,plain,
meet(X1,X2) = meet(X2,X1),
inference(orient,[status(thm)],[t4]) ).
cnf(t8945,plain,
meet(X3,meet(X1,X2)) = meet(X1,meet(X2,X3)),
inference(step,[status(thm)],[t7,t13]) ).
cnf(t15,plain,
meet(X1,meet(X2,X3)) = meet(X2,meet(X3,X1)),
inference(orient,[status(thm)],[t8945]) ).
cnf(t5,axiom,
meet(X1,join(X1,X2)) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t10,plain,
meet(X1,join(X1,X2)) = X1,
inference(orient,[status(thm)],[t5]) ).
cnf(t19,plain,
meet(join(X1,X2),meet(X3,X1)) = meet(X3,X1),
inference(cp,[status(thm)],[t15,t10]) ).
cnf(t8955,plain,
meet(X1,meet(join(X1,X2),X3)) = meet(X3,X1),
inference(step,[status(thm)],[t19,t15]) ).
cnf(t8956,plain,
meet(X1,meet(X3,join(X1,X2))) = meet(X3,X1),
inference(step,[status(thm)],[t8955,t13]) ).
cnf(t8957,plain,
meet(X1,meet(X3,join(X1,X2))) = meet(X1,X3),
inference(step,[status(thm)],[t8956,t13]) ).
cnf(t85,plain,
meet(X1,meet(X2,join(X1,X3))) = meet(X1,X2),
inference(orient,[status(thm)],[t8957]) ).
cnf(t6,axiom,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t2,axiom,
join(X1,X2) = join(X2,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t48,plain,
join(X1,X2) = join(X2,X1),
inference(orient,[status(thm)],[t2]) ).
cnf(t8950,plain,
join(X3,join(X1,X2)) = join(X1,join(X2,X3)),
inference(step,[status(thm)],[t6,t48]) ).
cnf(t51,plain,
join(X1,join(X2,X3)) = join(X2,join(X3,X1)),
inference(orient,[status(thm)],[t8950]) ).
cnf(t3,axiom,
join(X1,meet(X1,X2)) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t12,plain,
join(X1,meet(X1,X2)) = X1,
inference(orient,[status(thm)],[t3]) ).
cnf(t55,plain,
join(meet(X1,X2),join(X3,X1)) = join(X3,X1),
inference(cp,[status(thm)],[t51,t12]) ).
cnf(t8958,plain,
join(X1,join(meet(X1,X2),X3)) = join(X3,X1),
inference(step,[status(thm)],[t55,t51]) ).
cnf(t8959,plain,
join(X1,join(X3,meet(X1,X2))) = join(X3,X1),
inference(step,[status(thm)],[t8958,t48]) ).
cnf(t8960,plain,
join(X1,join(X3,meet(X1,X2))) = join(X1,X3),
inference(step,[status(thm)],[t8959,t48]) ).
cnf(t95,plain,
join(X1,join(X2,meet(X1,X3))) = join(X1,X2),
inference(orient,[status(thm)],[t8960]) ).
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/sandbox/benchmark/theBenchmark.p') ).
cnf(t8946,plain,
meet(join(X3,X1),join(meet(join(X1,X2),X3),X2)) = join(meet(join(meet(X1,X2),X3),X2),meet(X3,X1)),
inference(step,[status(thm)],[t8,t13]) ).
cnf(t8947,plain,
meet(join(X3,X1),join(meet(X3,join(X1,X2)),X2)) = join(meet(join(meet(X1,X2),X3),X2),meet(X3,X1)),
inference(step,[status(thm)],[t8946,t13]) ).
cnf(t8948,plain,
meet(join(X3,X1),join(meet(X3,join(X1,X2)),X2)) = join(meet(X2,join(meet(X1,X2),X3)),meet(X3,X1)),
inference(step,[status(thm)],[t8947,t13]) ).
cnf(t8949,plain,
meet(join(X3,X1),join(meet(X3,join(X1,X2)),X2)) = join(meet(X2,join(meet(X1,X2),X3)),meet(X1,X3)),
inference(step,[status(thm)],[t8948,t13]) ).
cnf(t33,plain,
join(meet(X1,join(meet(X2,X1),X3)),meet(X2,X3)) = meet(join(X3,X2),join(meet(X3,join(X2,X1)),X1)),
inference(orient,[status(thm)],[t8949]) ).
cnf(t50,plain,
join(meet(X1,join(meet(X2,X1),X3)),meet(X2,X3)) = meet(join(X3,X2),join(meet(X3,join(X2,X1)),X1)),
inference(rw,[status(thm)],[t33]) ).
cnf(t8989,plain,
join(meet(X2,X3),meet(X1,join(meet(X2,X1),X3))) = meet(join(X3,X2),join(meet(X3,join(X2,X1)),X1)),
inference(step,[status(thm)],[t50,t48]) ).
cnf(t8990,plain,
join(meet(X2,X3),meet(X1,join(X3,meet(X2,X1)))) = meet(join(X3,X2),join(meet(X3,join(X2,X1)),X1)),
inference(step,[status(thm)],[t8989,t48]) ).
cnf(t8991,plain,
join(meet(X2,X3),meet(X1,join(X3,meet(X1,X2)))) = meet(join(X3,X2),join(meet(X3,join(X2,X1)),X1)),
inference(step,[status(thm)],[t8990,t13]) ).
cnf(t8992,plain,
join(meet(X2,X3),meet(X1,join(X3,meet(X1,X2)))) = meet(join(X2,X3),join(meet(X3,join(X2,X1)),X1)),
inference(step,[status(thm)],[t8991,t48]) ).
cnf(t8993,plain,
join(meet(X2,X3),meet(X1,join(X3,meet(X1,X2)))) = meet(join(X2,X3),join(X1,meet(X3,join(X2,X1)))),
inference(step,[status(thm)],[t8992,t48]) ).
cnf(t8994,plain,
join(meet(X2,X3),meet(X1,join(X3,meet(X1,X2)))) = meet(join(X2,X3),join(X1,meet(X3,join(X1,X2)))),
inference(step,[status(thm)],[t8993,t48]) ).
cnf(t169,plain,
join(meet(X1,X2),meet(X3,join(X2,meet(X3,X1)))) = meet(join(X1,X2),join(X3,meet(X2,join(X3,X1)))),
inference(orient,[status(thm)],[t8994]) ).
cnf(t196,plain,
join(X1,meet(X2,X3)) = join(X1,meet(join(X2,X3),join(X1,meet(X3,join(X1,X2))))),
inference(cp,[status(thm)],[t95,t169]) ).
cnf(t505,plain,
join(X1,meet(join(X2,X3),join(X1,meet(X3,join(X1,X2))))) = join(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t196]) ).
cnf(t516,plain,
join(X1,meet(X2,meet(X2,X3))) = join(X1,meet(X2,join(X1,meet(meet(X2,X3),join(X1,X2))))),
inference(cp,[status(thm)],[t505,t12]) ).
cnf(t1,axiom,
meet(X1,X1) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t9,plain,
meet(X1,X1) = X1,
inference(orient,[status(thm)],[t1]) ).
cnf(t18,plain,
meet(X1,meet(X2,X1)) = meet(X2,X1),
inference(cp,[status(thm)],[t15,t9]) ).
cnf(t8951,plain,
meet(X1,meet(X1,X2)) = meet(X2,X1),
inference(step,[status(thm)],[t18,t15]) ).
cnf(t8952,plain,
meet(X1,meet(X1,X2)) = meet(X1,X2),
inference(step,[status(thm)],[t8951,t13]) ).
cnf(t69,plain,
meet(X1,meet(X1,X2)) = meet(X1,X2),
inference(orient,[status(thm)],[t8952]) ).
cnf(t9018,plain,
join(X1,meet(X2,X3)) = join(X1,meet(X2,join(X1,meet(meet(X2,X3),join(X1,X2))))),
inference(step,[status(thm)],[t516,t69]) ).
cnf(t739,plain,
join(X1,meet(X2,join(X1,meet(meet(X2,X3),join(X1,X2))))) = join(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t9018]) ).
cnf(t761,plain,
join(X1,meet(X2,X3)) = join(X1,meet(X2,join(X1,meet(meet(X2,X3),join(X2,X1))))),
inference(cp,[status(thm)],[t739,t48]) ).
cnf(t180,plain,
meet(join(X1,X2),join(X2,meet(X2,join(X2,X1)))) = join(meet(X1,X2),X2),
inference(cp,[status(thm)],[t169,t10]) ).
cnf(t8995,plain,
meet(join(X1,X2),X2) = join(meet(X1,X2),X2),
inference(step,[status(thm)],[t180,t12]) ).
cnf(t8996,plain,
meet(X2,join(X1,X2)) = join(meet(X1,X2),X2),
inference(step,[status(thm)],[t8995,t13]) ).
cnf(t8997,plain,
meet(X2,join(X1,X2)) = join(X2,meet(X1,X2)),
inference(step,[status(thm)],[t8996,t48]) ).
cnf(t204,plain,
join(X1,meet(X2,X1)) = meet(X1,join(X2,X1)),
inference(orient,[status(thm)],[t8997]) ).
cnf(t223,plain,
join(meet(X1,X2),join(X3,X2)) = join(X3,meet(X2,join(X1,X2))),
inference(cp,[status(thm)],[t51,t204]) ).
cnf(t9003,plain,
join(X2,join(meet(X1,X2),X3)) = join(X3,meet(X2,join(X1,X2))),
inference(step,[status(thm)],[t223,t51]) ).
cnf(t9004,plain,
join(X2,join(X3,meet(X1,X2))) = join(X3,meet(X2,join(X1,X2))),
inference(step,[status(thm)],[t9003,t48]) ).
cnf(t360,plain,
join(X1,join(X2,meet(X3,X1))) = join(X2,meet(X1,join(X3,X1))),
inference(orient,[status(thm)],[t9004]) ).
cnf(t372,plain,
join(X1,meet(meet(X2,join(X3,Y3)),join(X3,meet(X2,join(X3,Y3))))) = join(meet(X2,join(X3,Y3)),join(X1,meet(X3,X2))),
inference(cp,[status(thm)],[t360,t85]) ).
cnf(t211,plain,
meet(meet(X1,X2),join(X3,meet(X1,X2))) = join(meet(X1,X2),meet(X1,meet(X2,X3))),
inference(cp,[status(thm)],[t204,t15]) ).
cnf(t292,plain,
join(meet(X1,X2),meet(X1,meet(X2,X3))) = meet(meet(X1,X2),join(X3,meet(X1,X2))),
inference(orient,[status(thm)],[t211]) ).
cnf(t318,plain,
meet(X1,X2) = meet(meet(X1,X2),meet(meet(X1,X2),join(X3,meet(X1,X2)))),
inference(cp,[status(thm)],[t10,t292]) ).
cnf(t9000,plain,
meet(X1,X2) = meet(meet(X1,X2),join(X3,meet(X1,X2))),
inference(step,[status(thm)],[t318,t69]) ).
cnf(t332,plain,
meet(meet(X1,X2),join(X3,meet(X1,X2))) = meet(X1,X2),
inference(orient,[status(thm)],[t9000]) ).
cnf(t9005,plain,
join(X1,meet(X2,join(X3,Y3))) = join(meet(X2,join(X3,Y3)),join(X1,meet(X3,X2))),
inference(step,[status(thm)],[t372,t332]) ).
cnf(t9006,plain,
join(X1,meet(X2,join(X3,Y3))) = join(meet(X3,X2),join(meet(X2,join(X3,Y3)),X1)),
inference(step,[status(thm)],[t9005,t51]) ).
cnf(t9007,plain,
join(X1,meet(X2,join(X3,Y3))) = join(X1,join(meet(X3,X2),meet(X2,join(X3,Y3)))),
inference(step,[status(thm)],[t9006,t51]) ).
cnf(t9008,plain,
join(X1,meet(X2,join(X3,Y3))) = join(X1,join(meet(X2,X3),meet(X2,join(X3,Y3)))),
inference(step,[status(thm)],[t9007,t13]) ).
cnf(t469,plain,
join(X1,join(meet(X2,X3),meet(X2,join(X3,Y3)))) = join(X1,meet(X2,join(X3,Y3))),
inference(orient,[status(thm)],[t9008]) ).
cnf(t483,plain,
join(X1,meet(meet(X2,X3),join(join(Y3,meet(X2,X3)),Y4))) = join(X1,join(meet(X2,X3),meet(meet(X2,X3),join(join(Y3,meet(X2,X3)),Y4)))),
inference(cp,[status(thm)],[t469,t332]) ).
cnf(t9011,plain,
join(X1,meet(meet(X2,X3),join(Y4,join(Y3,meet(X2,X3))))) = join(X1,join(meet(X2,X3),meet(meet(X2,X3),join(join(Y3,meet(X2,X3)),Y4)))),
inference(step,[status(thm)],[t483,t48]) ).
cnf(t9012,plain,
join(X1,meet(meet(X2,X3),join(Y3,join(meet(X2,X3),Y4)))) = join(X1,join(meet(X2,X3),meet(meet(X2,X3),join(join(Y3,meet(X2,X3)),Y4)))),
inference(step,[status(thm)],[t9011,t51]) ).
cnf(t9013,plain,
join(X1,meet(meet(X2,X3),join(Y3,join(Y4,meet(X2,X3))))) = join(X1,join(meet(X2,X3),meet(meet(X2,X3),join(join(Y3,meet(X2,X3)),Y4)))),
inference(step,[status(thm)],[t9012,t48]) ).
cnf(t9014,plain,
join(X1,meet(meet(X2,X3),join(Y3,join(Y4,meet(X2,X3))))) = join(X1,meet(X2,X3)),
inference(step,[status(thm)],[t9013,t12]) ).
cnf(t617,plain,
join(X1,meet(meet(X2,X3),join(Y3,join(Y4,meet(X2,X3))))) = join(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t9014]) ).
cnf(t627,plain,
join(X1,meet(X2,X3)) = join(X1,meet(meet(X2,X3),join(X2,Y3))),
inference(cp,[status(thm)],[t617,t95]) ).
cnf(t667,plain,
join(X1,meet(meet(X2,X3),join(X2,Y3))) = join(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t627]) ).
cnf(t9019,plain,
join(X1,meet(X2,X3)) = join(X1,meet(X2,join(X1,meet(X2,X3)))),
inference(step,[status(thm)],[t761,t667]) ).
cnf(t782,plain,
join(X1,meet(X2,join(X1,meet(X2,X3)))) = join(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t9019]) ).
cnf(t785,plain,
join(meet(X1,X2),meet(X3,join(X2,meet(X3,X1)))) = join(meet(X1,X2),meet(X3,meet(join(X1,X2),join(X3,meet(X2,join(X3,X1)))))),
inference(cp,[status(thm)],[t782,t169]) ).
cnf(t9059,plain,
meet(join(X1,X2),join(X3,meet(X2,join(X3,X1)))) = join(meet(X1,X2),meet(X3,meet(join(X1,X2),join(X3,meet(X2,join(X3,X1)))))),
inference(step,[status(thm)],[t785,t169]) ).
cnf(t9060,plain,
meet(join(X1,X2),join(X3,meet(X2,join(X1,X3)))) = join(meet(X1,X2),meet(X3,meet(join(X1,X2),join(X3,meet(X2,join(X3,X1)))))),
inference(step,[status(thm)],[t9059,t48]) ).
cnf(t9061,plain,
meet(join(X1,X2),join(X3,meet(X2,join(X1,X3)))) = join(meet(X1,X2),meet(X3,join(X1,X2))),
inference(step,[status(thm)],[t9060,t85]) ).
cnf(t1713,plain,
meet(join(X1,X2),join(X3,meet(X2,join(X1,X3)))) = join(meet(X1,X2),meet(X3,join(X1,X2))),
inference(orient,[status(thm)],[t9061]) ).
cnf(t1806,plain,
meet(X1,join(X2,X3)) = meet(X1,join(meet(X2,X3),meet(X1,join(X2,X3)))),
inference(cp,[status(thm)],[t85,t1713]) ).
cnf(t2915,plain,
meet(X1,join(meet(X2,X3),meet(X1,join(X2,X3)))) = meet(X1,join(X2,X3)),
inference(orient,[status(thm)],[t1806]) ).
cnf(t2927,plain,
meet(X1,join(X2,join(X2,X3))) = meet(X1,join(X2,meet(X1,join(X2,join(X2,X3))))),
inference(cp,[status(thm)],[t2915,t10]) ).
cnf(t0,axiom,
join(X1,X1) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t11,plain,
join(X1,X1) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t54,plain,
join(X1,join(X2,X1)) = join(X2,X1),
inference(cp,[status(thm)],[t51,t11]) ).
cnf(t8953,plain,
join(X1,join(X1,X2)) = join(X2,X1),
inference(step,[status(thm)],[t54,t51]) ).
cnf(t8954,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(step,[status(thm)],[t8953,t48]) ).
cnf(t77,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(orient,[status(thm)],[t8954]) ).
cnf(t9129,plain,
meet(X1,join(X2,X3)) = meet(X1,join(X2,meet(X1,join(X2,join(X2,X3))))),
inference(step,[status(thm)],[t2927,t77]) ).
cnf(t9130,plain,
meet(X1,join(X2,X3)) = meet(X1,join(X2,meet(X1,join(X2,X3)))),
inference(step,[status(thm)],[t9129,t77]) ).
cnf(t3001,plain,
meet(X1,join(X2,meet(X1,join(X2,X3)))) = meet(X1,join(X2,X3)),
inference(orient,[status(thm)],[t9130]) ).
cnf(t3008,plain,
meet(join(X1,X2),join(X3,meet(X2,join(X1,X3)))) = meet(join(X1,X2),join(X3,join(meet(X1,X2),meet(X3,join(X1,X2))))),
inference(cp,[status(thm)],[t3001,t1713]) ).
cnf(t9132,plain,
join(meet(X1,X2),meet(X3,join(X1,X2))) = meet(join(X1,X2),join(X3,join(meet(X1,X2),meet(X3,join(X1,X2))))),
inference(step,[status(thm)],[t3008,t1713]) ).
cnf(t9133,plain,
join(meet(X1,X2),meet(X3,join(X1,X2))) = meet(join(X1,X2),join(X3,meet(X1,X2))),
inference(step,[status(thm)],[t9132,t95]) ).
cnf(t3102,plain,
join(meet(X1,X2),meet(X3,join(X1,X2))) = meet(join(X1,X2),join(X3,meet(X1,X2))),
inference(orient,[status(thm)],[t9133]) ).
cnf(t3115,plain,
meet(join(X1,join(X1,X2)),join(X3,meet(X1,join(X1,X2)))) = join(X1,meet(X3,join(X1,join(X1,X2)))),
inference(cp,[status(thm)],[t3102,t10]) ).
cnf(t9136,plain,
meet(join(X1,X2),join(X3,meet(X1,join(X1,X2)))) = join(X1,meet(X3,join(X1,join(X1,X2)))),
inference(step,[status(thm)],[t3115,t77]) ).
cnf(t9137,plain,
meet(join(X1,X2),join(X3,X1)) = join(X1,meet(X3,join(X1,join(X1,X2)))),
inference(step,[status(thm)],[t9136,t10]) ).
cnf(t9138,plain,
meet(join(X1,X2),join(X1,X3)) = join(X1,meet(X3,join(X1,join(X1,X2)))),
inference(step,[status(thm)],[t9137,t48]) ).
cnf(t9139,plain,
meet(join(X1,X2),join(X1,X3)) = join(X1,meet(X3,join(X1,X2))),
inference(step,[status(thm)],[t9138,t77]) ).
cnf(t1740,plain,
join(meet(X1,meet(X1,X2)),meet(X3,join(X1,meet(X1,X2)))) = meet(X1,join(X3,meet(meet(X1,X2),join(X1,X3)))),
inference(cp,[status(thm)],[t1713,t12]) ).
cnf(t9075,plain,
join(meet(X1,X2),meet(X3,join(X1,meet(X1,X2)))) = meet(X1,join(X3,meet(meet(X1,X2),join(X1,X3)))),
inference(step,[status(thm)],[t1740,t69]) ).
cnf(t9076,plain,
join(meet(X1,X2),meet(X3,X1)) = meet(X1,join(X3,meet(meet(X1,X2),join(X1,X3)))),
inference(step,[status(thm)],[t9075,t12]) ).
cnf(t9077,plain,
join(meet(X1,X2),meet(X1,X3)) = meet(X1,join(X3,meet(meet(X1,X2),join(X1,X3)))),
inference(step,[status(thm)],[t9076,t13]) ).
cnf(t9078,plain,
join(meet(X1,X2),meet(X1,X3)) = meet(X1,join(X3,meet(X1,X2))),
inference(step,[status(thm)],[t9077,t667]) ).
cnf(t1890,plain,
join(meet(X1,X2),meet(X1,X3)) = meet(X1,join(X3,meet(X1,X2))),
inference(orient,[status(thm)],[t9078]) ).
cnf(t1973,plain,
join(meet(X1,X2),meet(X3,join(X1,X3))) = join(X3,meet(X1,join(X3,meet(X1,X2)))),
inference(cp,[status(thm)],[t360,t1890]) ).
cnf(t9087,plain,
join(X3,join(meet(X1,X2),meet(X1,X3))) = join(X3,meet(X1,join(X3,meet(X1,X2)))),
inference(step,[status(thm)],[t1973,t360]) ).
cnf(t1905,plain,
meet(X1,join(X2,meet(X1,X3))) = join(meet(X3,X1),meet(X1,X2)),
inference(cp,[status(thm)],[t1890,t13]) ).
cnf(t9081,plain,
meet(X1,join(X2,meet(X1,X3))) = join(meet(X1,X2),meet(X3,X1)),
inference(step,[status(thm)],[t1905,t48]) ).
cnf(t9082,plain,
meet(X1,join(X2,meet(X1,X3))) = join(meet(X1,X2),meet(X1,X3)),
inference(step,[status(thm)],[t9081,t13]) ).
cnf(t9083,plain,
meet(X1,join(X2,meet(X1,X3))) = meet(X1,join(X3,meet(X1,X2))),
inference(step,[status(thm)],[t9082,t1890]) ).
cnf(t1977,plain,
meet(X1,join(X2,meet(X1,X3))) = meet(X1,join(X3,meet(X1,X2))),
inference(orient,[status(thm)],[t9083]) ).
cnf(t9084,plain,
join(meet(X1,X2),meet(X1,X3)) = meet(X1,join(X2,meet(X1,X3))),
inference(step,[status(thm)],[t1890,t1977]) ).
cnf(t1978,plain,
join(meet(X1,X2),meet(X1,X3)) = meet(X1,join(X2,meet(X1,X3))),
inference(orient,[status(thm)],[t9084]) ).
cnf(t9088,plain,
join(X3,meet(X1,join(X2,meet(X1,X3)))) = join(X3,meet(X1,join(X3,meet(X1,X2)))),
inference(step,[status(thm)],[t9087,t1978]) ).
cnf(t9089,plain,
join(X3,meet(X1,join(X2,meet(X1,X3)))) = join(X3,meet(X1,X2)),
inference(step,[status(thm)],[t9088,t782]) ).
cnf(t2080,plain,
join(X1,meet(X2,join(X3,meet(X2,X1)))) = join(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t9089]) ).
cnf(t2104,plain,
join(X1,meet(X2,X3)) = join(X1,meet(X2,join(X3,meet(X1,X2)))),
inference(cp,[status(thm)],[t2080,t13]) ).
cnf(t2143,plain,
join(X1,meet(X2,join(X3,meet(X1,X2)))) = join(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t2104]) ).
cnf(t2167,plain,
join(X1,meet(join(X1,X2),X3)) = join(X1,meet(join(X1,X2),join(X3,X1))),
inference(cp,[status(thm)],[t2143,t10]) ).
cnf(t9099,plain,
join(X1,meet(X3,join(X1,X2))) = join(X1,meet(join(X1,X2),join(X3,X1))),
inference(step,[status(thm)],[t2167,t13]) ).
cnf(t9100,plain,
join(X1,meet(X3,join(X1,X2))) = join(X1,meet(join(X1,X2),join(X1,X3))),
inference(step,[status(thm)],[t9099,t48]) ).
cnf(t2261,plain,
join(X1,meet(join(X1,X2),join(X1,X3))) = join(X1,meet(X3,join(X1,X2))),
inference(orient,[status(thm)],[t9100]) ).
cnf(t2277,plain,
join(X1,meet(X2,join(X1,X3))) = join(X1,meet(join(X3,X1),join(X1,X2))),
inference(cp,[status(thm)],[t2261,t48]) ).
cnf(t9110,plain,
join(X1,meet(X2,join(X1,X3))) = join(X1,meet(join(X1,X2),join(X3,X1))),
inference(step,[status(thm)],[t2277,t13]) ).
cnf(t9111,plain,
join(X1,meet(X2,join(X1,X3))) = join(X1,meet(join(X1,X2),join(X1,X3))),
inference(step,[status(thm)],[t9110,t48]) ).
cnf(t9112,plain,
join(X1,meet(X2,join(X1,X3))) = join(X1,meet(X3,join(X1,X2))),
inference(step,[status(thm)],[t9111,t2261]) ).
cnf(t2650,plain,
join(X1,meet(X2,join(X1,X3))) = join(X1,meet(X3,join(X1,X2))),
inference(orient,[status(thm)],[t9112]) ).
cnf(t9140,plain,
meet(join(X1,X2),join(X1,X3)) = join(X1,meet(X2,join(X1,X3))),
inference(step,[status(thm)],[t9139,t2650]) ).
cnf(t3220,plain,
join(X1,meet(X2,join(X1,X3))) = meet(join(X1,X2),join(X1,X3)),
inference(orient,[status(thm)],[t9140]) ).
cnf(t2918,plain,
meet(meet(X1,X2),join(X3,join(Y3,meet(X1,X2)))) = meet(meet(X1,X2),join(meet(X3,join(Y3,meet(X1,X2))),meet(X1,X2))),
inference(cp,[status(thm)],[t2915,t617]) ).
cnf(t9131,plain,
meet(meet(X1,X2),join(X3,join(Y3,meet(X1,X2)))) = meet(X1,X2),
inference(step,[status(thm)],[t2918,t332]) ).
cnf(t3036,plain,
meet(meet(X1,X2),join(X3,join(Y3,meet(X1,X2)))) = meet(X1,X2),
inference(orient,[status(thm)],[t9131]) ).
cnf(t3067,plain,
meet(X1,X2) = meet(meet(X1,X2),join(X3,meet(X1,join(Y3,meet(X1,X2))))),
inference(cp,[status(thm)],[t3036,t1978]) ).
cnf(t9291,plain,
meet(X1,X2) = meet(meet(X1,X2),join(X3,meet(X1,join(X2,meet(X1,Y3))))),
inference(step,[status(thm)],[t3067,t1977]) ).
cnf(t8213,plain,
meet(meet(X1,X2),join(X3,meet(X1,join(X2,meet(X1,Y3))))) = meet(X1,X2),
inference(orient,[status(thm)],[t9291]) ).
cnf(t1921,plain,
meet(X1,X2) = meet(meet(X1,X2),meet(X1,join(X3,meet(X1,X2)))),
inference(cp,[status(thm)],[t10,t1890]) ).
cnf(t9116,plain,
meet(X1,X2) = meet(X1,meet(join(X3,meet(X1,X2)),meet(X1,X2))),
inference(step,[status(thm)],[t1921,t15]) ).
cnf(t9117,plain,
meet(X1,X2) = meet(X1,meet(X2,meet(join(X3,meet(X1,X2)),X1))),
inference(step,[status(thm)],[t9116,t15]) ).
cnf(t9118,plain,
meet(X1,X2) = meet(X1,meet(X1,meet(X2,join(X3,meet(X1,X2))))),
inference(step,[status(thm)],[t9117,t15]) ).
cnf(t9119,plain,
meet(X1,X2) = meet(X1,meet(X2,join(X3,meet(X1,X2)))),
inference(step,[status(thm)],[t9118,t69]) ).
cnf(t2785,plain,
meet(X1,meet(X2,join(X3,meet(X1,X2)))) = meet(X1,X2),
inference(orient,[status(thm)],[t9119]) ).
cnf(t669,plain,
join(meet(meet(X1,X2),join(X1,X3)),meet(X1,X2)) = meet(meet(X1,X2),join(X1,X3)),
inference(cp,[status(thm)],[t667,t11]) ).
cnf(t9015,plain,
join(meet(X1,X2),meet(meet(X1,X2),join(X1,X3))) = meet(meet(X1,X2),join(X1,X3)),
inference(step,[status(thm)],[t669,t48]) ).
cnf(t9016,plain,
join(meet(X1,X2),meet(X1,X2)) = meet(meet(X1,X2),join(X1,X3)),
inference(step,[status(thm)],[t9015,t667]) ).
cnf(t9017,plain,
meet(X1,X2) = meet(meet(X1,X2),join(X1,X3)),
inference(step,[status(thm)],[t9016,t11]) ).
cnf(t708,plain,
meet(meet(X1,X2),join(X1,X3)) = meet(X1,X2),
inference(orient,[status(thm)],[t9017]) ).
cnf(t2811,plain,
meet(meet(X1,X2),join(X1,X3)) = meet(meet(X1,X2),meet(join(X1,X3),join(Y3,meet(X1,X2)))),
inference(cp,[status(thm)],[t2785,t708]) ).
cnf(t9290,plain,
meet(X1,X2) = meet(meet(X1,X2),meet(join(X1,X3),join(Y3,meet(X1,X2)))),
inference(step,[status(thm)],[t2811,t708]) ).
cnf(t8081,plain,
meet(meet(X1,X2),meet(join(X1,X3),join(Y3,meet(X1,X2)))) = meet(X1,X2),
inference(orient,[status(thm)],[t9290]) ).
cnf(t8294,plain,
meet(meet(X1,X2),X3) = meet(meet(meet(X1,X2),X3),join(Y3,meet(meet(X1,X2),join(X3,meet(X1,X2))))),
inference(cp,[status(thm)],[t8213,t8081]) ).
cnf(t9292,plain,
meet(X3,meet(X1,X2)) = meet(meet(meet(X1,X2),X3),join(Y3,meet(meet(X1,X2),join(X3,meet(X1,X2))))),
inference(step,[status(thm)],[t8294,t13]) ).
cnf(t9293,plain,
meet(X2,meet(X3,X1)) = meet(meet(meet(X1,X2),X3),join(Y3,meet(meet(X1,X2),join(X3,meet(X1,X2))))),
inference(step,[status(thm)],[t9292,t15]) ).
cnf(t9294,plain,
meet(X1,meet(X2,X3)) = meet(meet(meet(X1,X2),X3),join(Y3,meet(meet(X1,X2),join(X3,meet(X1,X2))))),
inference(step,[status(thm)],[t9293,t15]) ).
cnf(t9295,plain,
meet(X1,meet(X2,X3)) = meet(meet(X3,meet(X1,X2)),join(Y3,meet(meet(X1,X2),join(X3,meet(X1,X2))))),
inference(step,[status(thm)],[t9294,t13]) ).
cnf(t9296,plain,
meet(X1,meet(X2,X3)) = meet(meet(X2,meet(X3,X1)),join(Y3,meet(meet(X1,X2),join(X3,meet(X1,X2))))),
inference(step,[status(thm)],[t9295,t15]) ).
cnf(t9297,plain,
meet(X1,meet(X2,X3)) = meet(meet(X1,meet(X2,X3)),join(Y3,meet(meet(X1,X2),join(X3,meet(X1,X2))))),
inference(step,[status(thm)],[t9296,t15]) ).
cnf(t784,plain,
join(X1,meet(join(X2,X3),join(X1,meet(X3,join(X1,X2))))) = join(X1,meet(join(X2,X3),join(X1,meet(X2,X3)))),
inference(cp,[status(thm)],[t782,t505]) ).
cnf(t9020,plain,
join(X1,meet(X2,X3)) = join(X1,meet(join(X2,X3),join(X1,meet(X2,X3)))),
inference(step,[status(thm)],[t784,t505]) ).
cnf(t807,plain,
join(X1,meet(join(X2,X3),join(X1,meet(X2,X3)))) = join(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t9020]) ).
cnf(t815,plain,
join(X1,meet(X2,join(X2,X3))) = join(X1,meet(join(X2,X3),join(X1,meet(X2,join(X2,X3))))),
inference(cp,[status(thm)],[t807,t77]) ).
cnf(t9021,plain,
join(X1,X2) = join(X1,meet(join(X2,X3),join(X1,meet(X2,join(X2,X3))))),
inference(step,[status(thm)],[t815,t10]) ).
cnf(t9022,plain,
join(X1,X2) = join(X1,meet(join(X2,X3),join(X1,X2))),
inference(step,[status(thm)],[t9021,t10]) ).
cnf(t9023,plain,
join(X1,X2) = join(X1,meet(join(X1,X2),join(X2,X3))),
inference(step,[status(thm)],[t9022,t13]) ).
cnf(t873,plain,
join(X1,meet(join(X1,X2),join(X2,X3))) = join(X1,X2),
inference(orient,[status(thm)],[t9023]) ).
cnf(t925,plain,
join(X1,join(meet(join(X1,X2),join(X2,X3)),Y3)) = join(Y3,join(X1,X2)),
inference(cp,[status(thm)],[t51,t873]) ).
cnf(t9030,plain,
join(X1,join(Y3,meet(join(X1,X2),join(X2,X3)))) = join(Y3,join(X1,X2)),
inference(step,[status(thm)],[t925,t48]) ).
cnf(t9031,plain,
join(X1,join(Y3,meet(join(X1,X2),join(X2,X3)))) = join(X2,join(Y3,X1)),
inference(step,[status(thm)],[t9030,t51]) ).
cnf(t9032,plain,
join(X1,join(Y3,meet(join(X1,X2),join(X2,X3)))) = join(X1,join(X2,Y3)),
inference(step,[status(thm)],[t9031,t51]) ).
cnf(t1022,plain,
join(X1,join(X2,meet(join(X1,X3),join(X3,Y3)))) = join(X1,join(X3,X2)),
inference(orient,[status(thm)],[t9032]) ).
cnf(t1030,plain,
join(X1,join(X2,X2)) = join(X1,join(X2,meet(join(X1,X2),X3))),
inference(cp,[status(thm)],[t1022,t739]) ).
cnf(t9034,plain,
join(X1,X2) = join(X1,join(X2,meet(join(X1,X2),X3))),
inference(step,[status(thm)],[t1030,t11]) ).
cnf(t9035,plain,
join(X1,X2) = join(X1,join(X2,meet(X3,join(X1,X2)))),
inference(step,[status(thm)],[t9034,t13]) ).
cnf(t1092,plain,
join(X1,join(X2,meet(X3,join(X1,X2)))) = join(X1,X2),
inference(orient,[status(thm)],[t9035]) ).
cnf(t1139,plain,
join(X1,join(join(X2,meet(X3,join(X1,X2))),Y3)) = join(Y3,join(X1,X2)),
inference(cp,[status(thm)],[t51,t1092]) ).
cnf(t9040,plain,
join(X1,join(Y3,join(X2,meet(X3,join(X1,X2))))) = join(Y3,join(X1,X2)),
inference(step,[status(thm)],[t1139,t48]) ).
cnf(t9041,plain,
join(X1,join(X2,join(meet(X3,join(X1,X2)),Y3))) = join(Y3,join(X1,X2)),
inference(step,[status(thm)],[t9040,t51]) ).
cnf(t9042,plain,
join(X1,join(X2,join(Y3,meet(X3,join(X1,X2))))) = join(Y3,join(X1,X2)),
inference(step,[status(thm)],[t9041,t48]) ).
cnf(t9043,plain,
join(X1,join(X2,join(Y3,meet(X3,join(X1,X2))))) = join(X2,join(Y3,X1)),
inference(step,[status(thm)],[t9042,t51]) ).
cnf(t9044,plain,
join(X1,join(X2,join(Y3,meet(X3,join(X1,X2))))) = join(X1,join(X2,Y3)),
inference(step,[status(thm)],[t9043,t51]) ).
cnf(t1205,plain,
join(X1,join(X2,join(X3,meet(Y3,join(X1,X2))))) = join(X1,join(X2,X3)),
inference(orient,[status(thm)],[t9044]) ).
cnf(t2130,plain,
join(X1,join(meet(X2,X3),X3)) = join(X1,join(meet(X2,X3),join(X3,meet(X2,X1)))),
inference(cp,[status(thm)],[t1205,t2080]) ).
cnf(t9160,plain,
join(X1,join(X3,meet(X2,X3))) = join(X1,join(meet(X2,X3),join(X3,meet(X2,X1)))),
inference(step,[status(thm)],[t2130,t48]) ).
cnf(t9161,plain,
join(X1,meet(X3,join(X2,X3))) = join(X1,join(meet(X2,X3),join(X3,meet(X2,X1)))),
inference(step,[status(thm)],[t9160,t204]) ).
cnf(t9162,plain,
join(X1,meet(X3,join(X2,X3))) = join(X1,join(meet(X2,X1),join(meet(X2,X3),X3))),
inference(step,[status(thm)],[t9161,t51]) ).
cnf(t9163,plain,
join(X1,meet(X3,join(X2,X3))) = join(X1,join(X3,join(meet(X2,X1),meet(X2,X3)))),
inference(step,[status(thm)],[t9162,t51]) ).
cnf(t9164,plain,
join(X1,meet(X3,join(X2,X3))) = join(X1,join(X3,meet(X2,join(X1,meet(X2,X3))))),
inference(step,[status(thm)],[t9163,t1978]) ).
cnf(t9165,plain,
join(X1,meet(X3,join(X2,X3))) = join(X1,join(X3,meet(X2,X1))),
inference(step,[status(thm)],[t9164,t2080]) ).
cnf(t9166,plain,
join(X1,meet(X3,join(X2,X3))) = join(X1,join(X3,meet(X1,X2))),
inference(step,[status(thm)],[t9165,t13]) ).
cnf(t9167,plain,
join(X1,meet(X3,join(X2,X3))) = join(X1,X3),
inference(step,[status(thm)],[t9166,t95]) ).
cnf(t3780,plain,
join(X1,meet(X2,join(X3,X2))) = join(X1,X2),
inference(orient,[status(thm)],[t9167]) ).
cnf(t9298,plain,
meet(X1,meet(X2,X3)) = meet(meet(X1,meet(X2,X3)),join(Y3,meet(X1,X2))),
inference(step,[status(thm)],[t9297,t3780]) ).
cnf(t8355,plain,
meet(meet(X1,meet(X2,X3)),join(Y3,meet(X1,X2))) = meet(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t9298]) ).
cnf(t9143,plain,
meet(X1,meet(join(X2,X1),join(X2,X3))) = meet(X1,join(X2,X3)),
inference(step,[status(thm)],[t3001,t3220]) ).
cnf(t3284,plain,
meet(X1,meet(join(X2,X1),join(X2,X3))) = meet(X1,join(X2,X3)),
inference(rw,[status(thm)],[t9143]) ).
cnf(t9145,plain,
meet(X1,meet(join(X1,X2),join(X2,X3))) = meet(X1,join(X2,X3)),
inference(step,[status(thm)],[t3284,t48]) ).
cnf(t3286,plain,
meet(X1,meet(join(X1,X2),join(X2,X3))) = meet(X1,join(X2,X3)),
inference(orient,[status(thm)],[t9145]) ).
cnf(t8358,plain,
meet(X1,meet(join(X1,X2),join(X2,X3))) = meet(meet(X1,join(X2,X3)),join(Y3,meet(X1,join(X1,X2)))),
inference(cp,[status(thm)],[t8355,t3286]) ).
cnf(t9299,plain,
meet(X1,join(X2,X3)) = meet(meet(X1,join(X2,X3)),join(Y3,meet(X1,join(X1,X2)))),
inference(step,[status(thm)],[t8358,t3286]) ).
cnf(t9300,plain,
meet(X1,join(X2,X3)) = meet(meet(X1,join(X2,X3)),join(Y3,X1)),
inference(step,[status(thm)],[t9299,t10]) ).
cnf(t9301,plain,
meet(X1,join(X2,X3)) = meet(join(Y3,X1),meet(X1,join(X2,X3))),
inference(step,[status(thm)],[t9300,t13]) ).
cnf(t9302,plain,
meet(X1,join(X2,X3)) = meet(join(X2,X3),meet(join(Y3,X1),X1)),
inference(step,[status(thm)],[t9301,t15]) ).
cnf(t9303,plain,
meet(X1,join(X2,X3)) = meet(X1,meet(join(X2,X3),join(Y3,X1))),
inference(step,[status(thm)],[t9302,t15]) ).
cnf(t9304,plain,
meet(X1,join(X2,X3)) = meet(X1,meet(join(X2,X3),join(X1,Y3))),
inference(step,[status(thm)],[t9303,t48]) ).
cnf(t9305,plain,
meet(X1,join(X2,X3)) = meet(X1,meet(join(X1,Y3),join(X2,X3))),
inference(step,[status(thm)],[t9304,t13]) ).
cnf(t8482,plain,
meet(X1,meet(join(X1,X2),join(X3,Y3))) = meet(X1,join(X3,Y3)),
inference(orient,[status(thm)],[t9305]) ).
cnf(t9134,plain,
meet(join(X1,X2),join(X3,meet(X2,join(X1,X3)))) = meet(join(X1,X2),join(X3,meet(X1,X2))),
inference(step,[status(thm)],[t1713,t3102]) ).
cnf(t3103,plain,
meet(join(X1,X2),join(X3,meet(X2,join(X1,X3)))) = meet(join(X1,X2),join(X3,meet(X1,X2))),
inference(orient,[status(thm)],[t9134]) ).
cnf(t8485,plain,
meet(X1,join(X2,meet(X3,join(X1,X2)))) = meet(X1,meet(join(X1,X3),join(X2,meet(X1,X3)))),
inference(cp,[status(thm)],[t8482,t3103]) ).
cnf(t9306,plain,
meet(X1,join(X2,meet(X3,join(X1,X2)))) = meet(X1,join(X2,meet(X1,X3))),
inference(step,[status(thm)],[t8485,t8482]) ).
cnf(t8550,plain,
meet(X1,join(X2,meet(X3,join(X1,X2)))) = meet(X1,join(X2,meet(X1,X3))),
inference(orient,[status(thm)],[t9306]) ).
cnf(t8623,plain,
meet(X1,join(X2,meet(X1,X3))) = meet(X1,join(X2,meet(X3,join(X2,X1)))),
inference(cp,[status(thm)],[t8550,t48]) ).
cnf(t9307,plain,
meet(X1,join(X2,meet(X1,X3))) = meet(X1,meet(join(X2,X3),join(X2,X1))),
inference(step,[status(thm)],[t8623,t3220]) ).
cnf(t9308,plain,
meet(X1,join(X2,meet(X1,X3))) = meet(X1,meet(join(X2,X1),join(X2,X3))),
inference(step,[status(thm)],[t9307,t13]) ).
cnf(t9309,plain,
meet(X1,join(X2,meet(X1,X3))) = meet(X1,meet(join(X1,X2),join(X2,X3))),
inference(step,[status(thm)],[t9308,t48]) ).
cnf(t9310,plain,
meet(X1,join(X2,meet(X1,X3))) = meet(X1,join(X2,X3)),
inference(step,[status(thm)],[t9309,t8482]) ).
cnf(t8675,plain,
meet(X1,join(X2,meet(X1,X3))) = meet(X1,join(X2,X3)),
inference(orient,[status(thm)],[t9310]) ).
cnf(t8745,plain,
meet(join(X1,X2),join(X1,meet(X2,X3))) = join(X1,meet(X2,join(X1,X3))),
inference(cp,[status(thm)],[t3220,t8675]) ).
cnf(t2086,plain,
join(join(X1,meet(X2,X3)),meet(X2,X1)) = join(join(X1,meet(X2,X3)),meet(X2,join(X1,meet(X2,X3)))),
inference(cp,[status(thm)],[t2080,t782]) ).
cnf(t9120,plain,
join(meet(X2,X1),join(X1,meet(X2,X3))) = join(join(X1,meet(X2,X3)),meet(X2,join(X1,meet(X2,X3)))),
inference(step,[status(thm)],[t2086,t48]) ).
cnf(t9121,plain,
join(X1,join(meet(X2,X3),meet(X2,X1))) = join(join(X1,meet(X2,X3)),meet(X2,join(X1,meet(X2,X3)))),
inference(step,[status(thm)],[t9120,t51]) ).
cnf(t9122,plain,
join(X1,meet(X2,join(X3,meet(X2,X1)))) = join(join(X1,meet(X2,X3)),meet(X2,join(X1,meet(X2,X3)))),
inference(step,[status(thm)],[t9121,t1978]) ).
cnf(t9123,plain,
join(X1,meet(X2,join(X1,meet(X2,X3)))) = join(join(X1,meet(X2,X3)),meet(X2,join(X1,meet(X2,X3)))),
inference(step,[status(thm)],[t9122,t1977]) ).
cnf(t9124,plain,
join(X1,meet(X2,X3)) = join(join(X1,meet(X2,X3)),meet(X2,join(X1,meet(X2,X3)))),
inference(step,[status(thm)],[t9123,t782]) ).
cnf(t9125,plain,
join(X1,meet(X2,X3)) = meet(join(X1,meet(X2,X3)),join(X2,join(X1,meet(X2,X3)))),
inference(step,[status(thm)],[t9124,t204]) ).
cnf(t9126,plain,
join(X1,meet(X2,X3)) = meet(join(X1,meet(X2,X3)),join(X2,X1)),
inference(step,[status(thm)],[t9125,t95]) ).
cnf(t9127,plain,
join(X1,meet(X2,X3)) = meet(join(X1,meet(X2,X3)),join(X1,X2)),
inference(step,[status(thm)],[t9126,t48]) ).
cnf(t9128,plain,
join(X1,meet(X2,X3)) = meet(join(X1,X2),join(X1,meet(X2,X3))),
inference(step,[status(thm)],[t9127,t13]) ).
cnf(t2829,plain,
meet(join(X1,X2),join(X1,meet(X2,X3))) = join(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t9128]) ).
cnf(t9323,plain,
join(X1,meet(X2,X3)) = join(X1,meet(X2,join(X1,X3))),
inference(step,[status(thm)],[t8745,t2829]) ).
cnf(t9324,plain,
join(X1,meet(X2,X3)) = meet(join(X1,X2),join(X1,X3)),
inference(step,[status(thm)],[t9323,t3220]) ).
cnf(t8780,plain,
meet(join(X1,X2),join(X1,X3)) = join(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t9324]) ).
cnf(goal_0,negated_conjecture,
meet(join(a,b),join(a,c)) != join(a,meet(b,c)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
join(a,meet(b,c)) != join(a,meet(b,c)),
inference(rw,[status(thm)],[goal_0,t8780]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT009-1 : TPTP v9.3.1. Released v2.2.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.09/5.38 % Computer : n003.cluster.edu
% 0.09/5.38 % Model : x86_64 x86_64
% 0.09/5.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/5.38 % Memory : 8046.5625MB
% 0.09/5.38 % OS : Linux 6.8.0-71-generic
% 0.09/5.38 % CPULimit : 300
% 0.09/5.38 % WCLimit : 300
% 0.09/5.38 % DateTime : Wed Sep 23 20:02:09 UTC 2026
% 0.09/5.39 % CPUTime :
% 0.09/5.39 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 14.37/7.23 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 14.37/7.23 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------