%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : LAT160-1 : TPTP v9.3.1. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n020.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 01:55:47 PM UTC 2026
% Result : Unsatisfiable 35.74s 5.07s
% Output : CNFRefutation 35.74s
% Verified :
% SZS Type : Refutation
% Derivation depth : 186
% Number of leaves : 10
% Syntax : Number of clauses : 438 ( 438 unt; 0 nHn; 3 RR)
% Number of literals : 438 ( 437 equ; 2 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 9 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 6 ( 6 usr; 4 con; 0-2 aty)
% Number of variables : 1738 ( 390 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(t59649,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)],[t59649]) ).
cnf(t8,axiom,
meet(X1,join(X2,join(meet(X3,X4),meet(X3,join(X1,X2))))) = meet(X1,join(X2,meet(X3,join(X1,X4)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t33,plain,
meet(X1,join(X2,join(meet(X3,X4),meet(X3,join(X1,X2))))) = meet(X1,join(X2,meet(X3,join(X1,X4)))),
inference(orient,[status(thm)],[t8]) ).
cnf(t46,plain,
meet(X1,meet(join(X2,join(meet(X3,X4),meet(X3,join(X1,X2)))),Y4)) = meet(Y4,meet(X1,join(X2,meet(X3,join(X1,X4))))),
inference(cp,[status(thm)],[t15,t33]) ).
cnf(t60104,plain,
meet(X1,meet(Y4,join(X2,join(meet(X3,X4),meet(X3,join(X1,X2)))))) = meet(Y4,meet(X1,join(X2,meet(X3,join(X1,X4))))),
inference(step,[status(thm)],[t46,t13]) ).
cnf(t60105,plain,
meet(X1,meet(Y4,join(X2,join(meet(X3,X4),meet(X3,join(X1,X2)))))) = meet(X1,meet(join(X2,meet(X3,join(X1,X4))),Y4)),
inference(step,[status(thm)],[t60104,t15]) ).
cnf(t60106,plain,
meet(X1,meet(Y4,join(X2,join(meet(X3,X4),meet(X3,join(X1,X2)))))) = meet(X1,meet(Y4,join(X2,meet(X3,join(X1,X4))))),
inference(step,[status(thm)],[t60105,t13]) ).
cnf(t16163,plain,
meet(X1,meet(X2,join(X3,join(meet(X4,Y4),meet(X4,join(X1,X3)))))) = meet(X1,meet(X2,join(X3,meet(X4,join(X1,Y4))))),
inference(orient,[status(thm)],[t60106]) ).
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(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(t59650,plain,
join(X3,join(X1,X2)) = join(X1,join(X2,X3)),
inference(step,[status(thm)],[t6,t48]) ).
cnf(t52,plain,
join(X1,join(X2,X3)) = join(X2,join(X3,X1)),
inference(orient,[status(thm)],[t59650]) ).
cnf(t59,plain,
meet(X1,join(join(X2,X3),meet(X4,join(X1,Y4)))) = meet(X1,join(join(X2,X3),join(meet(X4,Y4),meet(X4,join(X3,join(X1,X2)))))),
inference(cp,[status(thm)],[t33,t52]) ).
cnf(t60215,plain,
meet(X1,join(join(X2,X3),meet(X4,join(X1,Y4)))) = meet(X1,join(meet(X4,Y4),join(meet(X4,join(X3,join(X1,X2))),join(X2,X3)))),
inference(step,[status(thm)],[t59,t52]) ).
cnf(t60216,plain,
meet(X1,join(join(X2,X3),meet(X4,join(X1,Y4)))) = meet(X1,join(meet(X4,Y4),join(X3,join(meet(X4,join(X3,join(X1,X2))),X2)))),
inference(step,[status(thm)],[t60215,t52]) ).
cnf(t60217,plain,
meet(X1,join(join(X2,X3),meet(X4,join(X1,Y4)))) = meet(X1,join(meet(X4,Y4),join(X2,join(X3,meet(X4,join(X3,join(X1,X2))))))),
inference(step,[status(thm)],[t60216,t52]) ).
cnf(t60218,plain,
meet(X1,join(join(X2,X3),meet(X4,join(X1,Y4)))) = meet(X1,join(X2,join(join(X3,meet(X4,join(X3,join(X1,X2)))),meet(X4,Y4)))),
inference(step,[status(thm)],[t60217,t52]) ).
cnf(t60219,plain,
meet(X1,join(join(X2,X3),meet(X4,join(X1,Y4)))) = meet(X1,join(X2,join(meet(X4,Y4),join(X3,meet(X4,join(X3,join(X1,X2))))))),
inference(step,[status(thm)],[t60218,t48]) ).
cnf(t60220,plain,
meet(X1,join(join(X2,X3),meet(X4,join(X1,Y4)))) = meet(X1,join(X2,join(X3,join(meet(X4,join(X3,join(X1,X2))),meet(X4,Y4))))),
inference(step,[status(thm)],[t60219,t52]) ).
cnf(t60221,plain,
meet(X1,join(join(X2,X3),meet(X4,join(X1,Y4)))) = meet(X1,join(X2,join(X3,join(meet(X4,Y4),meet(X4,join(X3,join(X1,X2))))))),
inference(step,[status(thm)],[t60220,t48]) ).
cnf(t60222,plain,
meet(X1,join(join(X2,X3),meet(X4,join(X1,Y4)))) = meet(X1,join(X2,join(X3,join(meet(X4,Y4),meet(X4,join(X2,join(X3,X1))))))),
inference(step,[status(thm)],[t60221,t52]) ).
cnf(t60223,plain,
meet(X1,join(join(X2,X3),meet(X4,join(X1,Y4)))) = meet(X1,join(X2,join(X3,join(meet(X4,Y4),meet(X4,join(X1,join(X2,X3))))))),
inference(step,[status(thm)],[t60222,t52]) ).
cnf(t29023,plain,
meet(X1,join(X2,join(X3,join(meet(X4,Y4),meet(X4,join(X1,join(X2,X3))))))) = meet(X1,join(join(X2,X3),meet(X4,join(X1,Y4)))),
inference(orient,[status(thm)],[t60223]) ).
cnf(t56,plain,
join(meet(X1,X2),join(X3,X1)) = join(X3,X1),
inference(cp,[status(thm)],[t52,t12]) ).
cnf(t59658,plain,
join(X1,join(meet(X1,X2),X3)) = join(X3,X1),
inference(step,[status(thm)],[t56,t52]) ).
cnf(t59659,plain,
join(X1,join(X3,meet(X1,X2))) = join(X3,X1),
inference(step,[status(thm)],[t59658,t48]) ).
cnf(t59660,plain,
join(X1,join(X3,meet(X1,X2))) = join(X1,X3),
inference(step,[status(thm)],[t59659,t48]) ).
cnf(t103,plain,
join(X1,join(X2,meet(X1,X3))) = join(X1,X2),
inference(orient,[status(thm)],[t59660]) ).
cnf(t29029,plain,
meet(X1,join(join(X2,X3),meet(X3,join(X1,X4)))) = meet(X1,join(X2,join(X3,meet(X3,X4)))),
inference(cp,[status(thm)],[t29023,t103]) ).
cnf(t60225,plain,
meet(X1,join(join(X2,X3),meet(X3,join(X1,X4)))) = meet(X1,join(X2,X3)),
inference(step,[status(thm)],[t29029,t12]) ).
cnf(t30358,plain,
meet(X1,join(join(X2,X3),meet(X3,join(X1,X4)))) = meet(X1,join(X2,X3)),
inference(orient,[status(thm)],[t60225]) ).
cnf(t30376,plain,
meet(X1,join(X2,meet(X2,X3))) = meet(X1,join(X2,meet(meet(X2,X3),join(X1,X4)))),
inference(cp,[status(thm)],[t30358,t12]) ).
cnf(t60226,plain,
meet(X1,X2) = meet(X1,join(X2,meet(meet(X2,X3),join(X1,X4)))),
inference(step,[status(thm)],[t30376,t12]) ).
cnf(t30624,plain,
meet(X1,join(X2,meet(meet(X2,X3),join(X1,X4)))) = meet(X1,X2),
inference(orient,[status(thm)],[t60226]) ).
cnf(t43,plain,
meet(X1,join(meet(X1,X2),meet(X3,join(X1,X4)))) = meet(X1,join(meet(X1,X2),join(meet(X3,X4),meet(X3,X1)))),
inference(cp,[status(thm)],[t33,t12]) ).
cnf(t59754,plain,
meet(X1,join(meet(X1,X2),meet(X3,join(X1,X4)))) = meet(X1,join(meet(X1,X2),join(meet(X3,X1),meet(X3,X4)))),
inference(step,[status(thm)],[t43,t48]) ).
cnf(t59755,plain,
meet(X1,join(meet(X1,X2),meet(X3,join(X1,X4)))) = meet(X1,join(meet(X1,X2),join(meet(X1,X3),meet(X3,X4)))),
inference(step,[status(thm)],[t59754,t13]) ).
cnf(t695,plain,
meet(X1,join(meet(X1,X2),join(meet(X1,X3),meet(X3,X4)))) = meet(X1,join(meet(X1,X2),meet(X3,join(X1,X4)))),
inference(orient,[status(thm)],[t59755]) ).
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(t730,plain,
meet(X1,join(meet(X1,X2),meet(X3,join(X1,X3)))) = meet(X1,join(meet(X1,X2),join(meet(X1,X3),X3))),
inference(cp,[status(thm)],[t695,t9]) ).
cnf(t35,plain,
meet(X1,join(X2,meet(X3,join(X1,X3)))) = meet(X1,join(X2,join(X3,meet(X3,join(X1,X2))))),
inference(cp,[status(thm)],[t33,t9]) ).
cnf(t59661,plain,
meet(X1,join(X2,meet(X3,join(X1,X3)))) = meet(X1,join(X2,X3)),
inference(step,[status(thm)],[t35,t12]) ).
cnf(t114,plain,
meet(X1,join(X2,meet(X3,join(X1,X3)))) = meet(X1,join(X2,X3)),
inference(orient,[status(thm)],[t59661]) ).
cnf(t59756,plain,
meet(X1,join(meet(X1,X2),X3)) = meet(X1,join(meet(X1,X2),join(meet(X1,X3),X3))),
inference(step,[status(thm)],[t730,t114]) ).
cnf(t59757,plain,
meet(X1,join(X3,meet(X1,X2))) = meet(X1,join(meet(X1,X2),join(meet(X1,X3),X3))),
inference(step,[status(thm)],[t59756,t48]) ).
cnf(t59758,plain,
meet(X1,join(X3,meet(X1,X2))) = meet(X1,join(X3,join(meet(X1,X2),meet(X1,X3)))),
inference(step,[status(thm)],[t59757,t52]) ).
cnf(t764,plain,
meet(X1,join(X2,join(meet(X1,X3),meet(X1,X2)))) = meet(X1,join(X2,meet(X1,X3))),
inference(orient,[status(thm)],[t59758]) ).
cnf(t805,plain,
meet(X1,meet(join(X2,join(meet(X1,X3),meet(X1,X2))),X4)) = meet(X4,meet(X1,join(X2,meet(X1,X3)))),
inference(cp,[status(thm)],[t15,t764]) ).
cnf(t59771,plain,
meet(X1,meet(X4,join(X2,join(meet(X1,X3),meet(X1,X2))))) = meet(X4,meet(X1,join(X2,meet(X1,X3)))),
inference(step,[status(thm)],[t805,t13]) ).
cnf(t59772,plain,
meet(X1,meet(X4,join(X2,join(meet(X1,X2),meet(X1,X3))))) = meet(X4,meet(X1,join(X2,meet(X1,X3)))),
inference(step,[status(thm)],[t59771,t48]) ).
cnf(t59773,plain,
meet(X1,meet(X4,join(X2,join(meet(X1,X2),meet(X1,X3))))) = meet(X1,meet(join(X2,meet(X1,X3)),X4)),
inference(step,[status(thm)],[t59772,t15]) ).
cnf(t59774,plain,
meet(X1,meet(X4,join(X2,join(meet(X1,X2),meet(X1,X3))))) = meet(X1,meet(X4,join(X2,meet(X1,X3)))),
inference(step,[status(thm)],[t59773,t13]) ).
cnf(t1146,plain,
meet(X1,meet(X2,join(X3,join(meet(X1,X3),meet(X1,X4))))) = meet(X1,meet(X2,join(X3,meet(X1,X4)))),
inference(orient,[status(thm)],[t59774]) ).
cnf(t41,plain,
meet(X1,join(X2,meet(join(X1,X2),join(X1,X3)))) = meet(X1,join(X2,join(meet(join(X1,X2),X3),join(X1,X2)))),
inference(cp,[status(thm)],[t33,t9]) ).
cnf(t59735,plain,
meet(X1,join(X2,meet(join(X1,X2),join(X1,X3)))) = meet(X1,join(X2,join(X2,join(meet(join(X1,X2),X3),X1)))),
inference(step,[status(thm)],[t41,t52]) ).
cnf(t59736,plain,
meet(X1,join(X2,meet(join(X1,X2),join(X1,X3)))) = meet(X1,join(X2,join(X1,join(X2,meet(join(X1,X2),X3))))),
inference(step,[status(thm)],[t59735,t52]) ).
cnf(t59737,plain,
meet(X1,join(X2,meet(join(X1,X2),join(X1,X3)))) = meet(X1,join(X1,join(join(X2,meet(join(X1,X2),X3)),X2))),
inference(step,[status(thm)],[t59736,t52]) ).
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(t59738,plain,
meet(X1,join(X2,meet(join(X1,X2),join(X1,X3)))) = X1,
inference(step,[status(thm)],[t59737,t10]) ).
cnf(t420,plain,
meet(X1,join(X2,meet(join(X1,X2),join(X1,X3)))) = X1,
inference(orient,[status(thm)],[t59738]) ).
cnf(t431,plain,
X1 = meet(X1,join(join(X2,X3),meet(join(X2,join(X3,X1)),join(X1,X4)))),
inference(cp,[status(thm)],[t420,t52]) ).
cnf(t59741,plain,
X1 = meet(X1,join(join(X2,X3),meet(join(X1,X4),join(X2,join(X3,X1))))),
inference(step,[status(thm)],[t431,t13]) ).
cnf(t59742,plain,
X1 = meet(X1,join(join(X2,X3),meet(join(X1,X4),join(X1,join(X2,X3))))),
inference(step,[status(thm)],[t59741,t52]) ).
cnf(t529,plain,
meet(X1,join(join(X2,X3),meet(join(X1,X4),join(X1,join(X2,X3))))) = X1,
inference(orient,[status(thm)],[t59742]) ).
cnf(t559,plain,
join(X1,X2) = meet(join(X1,X2),join(X3,join(join(X1,X2),X3))),
inference(cp,[status(thm)],[t420,t529]) ).
cnf(t59743,plain,
join(X1,X2) = meet(join(X1,X2),join(X3,join(X3,join(X1,X2)))),
inference(step,[status(thm)],[t559,t52]) ).
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(t55,plain,
join(X1,join(X2,X1)) = join(X2,X1),
inference(cp,[status(thm)],[t52,t11]) ).
cnf(t59653,plain,
join(X1,join(X1,X2)) = join(X2,X1),
inference(step,[status(thm)],[t55,t52]) ).
cnf(t59654,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(step,[status(thm)],[t59653,t48]) ).
cnf(t82,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(orient,[status(thm)],[t59654]) ).
cnf(t59744,plain,
join(X1,X2) = meet(join(X1,X2),join(X3,join(X1,X2))),
inference(step,[status(thm)],[t59743,t82]) ).
cnf(t59745,plain,
join(X1,X2) = meet(join(X1,X2),join(X2,join(X3,X1))),
inference(step,[status(thm)],[t59744,t52]) ).
cnf(t59746,plain,
join(X1,X2) = meet(join(X1,X2),join(X1,join(X2,X3))),
inference(step,[status(thm)],[t59745,t52]) ).
cnf(t573,plain,
meet(join(X1,X2),join(X1,join(X2,X3))) = join(X1,X2),
inference(orient,[status(thm)],[t59746]) ).
cnf(t1149,plain,
meet(X1,meet(join(X2,meet(X1,X2)),join(X2,meet(X1,X3)))) = meet(X1,join(X2,meet(X1,X2))),
inference(cp,[status(thm)],[t1146,t573]) ).
cnf(t1211,plain,
meet(X1,meet(join(X2,meet(X1,X2)),join(X2,meet(X1,X3)))) = meet(X1,join(X2,meet(X1,X2))),
inference(orient,[status(thm)],[t1149]) ).
cnf(t1251,plain,
meet(X1,join(X2,meet(X1,X2))) = meet(X1,meet(join(X2,meet(X2,X1)),join(X2,meet(X1,X3)))),
inference(cp,[status(thm)],[t1211,t13]) ).
cnf(t59775,plain,
meet(X1,join(X2,meet(X1,X2))) = meet(X1,meet(join(X2,meet(X1,X3)),join(X2,meet(X2,X1)))),
inference(step,[status(thm)],[t1251,t13]) ).
cnf(t59776,plain,
meet(X1,join(X2,meet(X1,X2))) = meet(X1,meet(join(X2,meet(X1,X3)),X2)),
inference(step,[status(thm)],[t59775,t12]) ).
cnf(t59777,plain,
meet(X1,join(X2,meet(X1,X2))) = meet(X1,meet(X2,join(X2,meet(X1,X3)))),
inference(step,[status(thm)],[t59776,t13]) ).
cnf(t59778,plain,
meet(X1,join(X2,meet(X1,X2))) = meet(X1,X2),
inference(step,[status(thm)],[t59777,t10]) ).
cnf(t1282,plain,
meet(X1,join(X2,meet(X1,X2))) = meet(X1,X2),
inference(orient,[status(thm)],[t59778]) ).
cnf(t19,plain,
meet(join(X1,X2),meet(X3,X1)) = meet(X3,X1),
inference(cp,[status(thm)],[t15,t10]) ).
cnf(t59655,plain,
meet(X1,meet(join(X1,X2),X3)) = meet(X3,X1),
inference(step,[status(thm)],[t19,t15]) ).
cnf(t59656,plain,
meet(X1,meet(X3,join(X1,X2))) = meet(X3,X1),
inference(step,[status(thm)],[t59655,t13]) ).
cnf(t59657,plain,
meet(X1,meet(X3,join(X1,X2))) = meet(X1,X3),
inference(step,[status(thm)],[t59656,t13]) ).
cnf(t92,plain,
meet(X1,meet(X2,join(X1,X3))) = meet(X1,X2),
inference(orient,[status(thm)],[t59657]) ).
cnf(t1306,plain,
meet(X1,meet(X2,join(X1,X3))) = meet(X1,join(meet(X2,join(X1,X3)),meet(X1,X2))),
inference(cp,[status(thm)],[t1282,t92]) ).
cnf(t59784,plain,
meet(X1,X2) = meet(X1,join(meet(X2,join(X1,X3)),meet(X1,X2))),
inference(step,[status(thm)],[t1306,t92]) ).
cnf(t59785,plain,
meet(X1,X2) = meet(X1,join(meet(X1,X2),meet(X2,join(X1,X3)))),
inference(step,[status(thm)],[t59784,t48]) ).
cnf(t696,plain,
meet(X1,join(meet(X1,X2),meet(X2,join(X1,X3)))) = meet(X1,join(meet(X1,X2),meet(X2,X3))),
inference(cp,[status(thm)],[t695,t82]) ).
cnf(t858,plain,
meet(X1,join(meet(X1,X2),meet(X2,join(X1,X3)))) = meet(X1,join(meet(X1,X2),meet(X2,X3))),
inference(orient,[status(thm)],[t696]) ).
cnf(t59786,plain,
meet(X1,X2) = meet(X1,join(meet(X1,X2),meet(X2,X3))),
inference(step,[status(thm)],[t59785,t858]) ).
cnf(t1426,plain,
meet(X1,join(meet(X1,X2),meet(X2,X3))) = meet(X1,X2),
inference(orient,[status(thm)],[t59786]) ).
cnf(t1472,plain,
meet(X1,join(meet(X1,X2),meet(X2,X3))) = meet(X1,join(meet(X1,X2),meet(join(meet(X1,X2),meet(X2,X3)),X4))),
inference(cp,[status(thm)],[t1426,t1426]) ).
cnf(t59817,plain,
meet(X1,X2) = meet(X1,join(meet(X1,X2),meet(join(meet(X1,X2),meet(X2,X3)),X4))),
inference(step,[status(thm)],[t1472,t1426]) ).
cnf(t59818,plain,
meet(X1,X2) = meet(X1,join(meet(X1,X2),meet(X4,join(meet(X1,X2),meet(X2,X3))))),
inference(step,[status(thm)],[t59817,t13]) ).
cnf(t2240,plain,
meet(X1,join(meet(X1,X2),meet(X3,join(meet(X1,X2),meet(X2,X4))))) = meet(X1,X2),
inference(orient,[status(thm)],[t59818]) ).
cnf(t123,plain,
meet(X1,meet(join(X2,meet(X3,join(X1,X3))),X4)) = meet(X4,meet(X1,join(X2,X3))),
inference(cp,[status(thm)],[t15,t114]) ).
cnf(t59673,plain,
meet(X1,meet(X4,join(X2,meet(X3,join(X1,X3))))) = meet(X4,meet(X1,join(X2,X3))),
inference(step,[status(thm)],[t123,t13]) ).
cnf(t59674,plain,
meet(X1,meet(X4,join(X2,meet(X3,join(X1,X3))))) = meet(X1,meet(join(X2,X3),X4)),
inference(step,[status(thm)],[t59673,t15]) ).
cnf(t59675,plain,
meet(X1,meet(X4,join(X2,meet(X3,join(X1,X3))))) = meet(X1,meet(X4,join(X2,X3))),
inference(step,[status(thm)],[t59674,t13]) ).
cnf(t169,plain,
meet(X1,meet(X2,join(X3,meet(X4,join(X1,X4))))) = meet(X1,meet(X2,join(X3,X4))),
inference(orient,[status(thm)],[t59675]) ).
cnf(t1351,plain,
meet(X1,meet(join(X2,meet(X1,X2)),X3)) = meet(X3,meet(X1,X2)),
inference(cp,[status(thm)],[t15,t1282]) ).
cnf(t59781,plain,
meet(X1,meet(X3,join(X2,meet(X1,X2)))) = meet(X3,meet(X1,X2)),
inference(step,[status(thm)],[t1351,t13]) ).
cnf(t59782,plain,
meet(X1,meet(X3,join(X2,meet(X1,X2)))) = meet(X2,meet(X3,X1)),
inference(step,[status(thm)],[t59781,t15]) ).
cnf(t59783,plain,
meet(X1,meet(X3,join(X2,meet(X1,X2)))) = meet(X1,meet(X2,X3)),
inference(step,[status(thm)],[t59782,t15]) ).
cnf(t1353,plain,
meet(X1,meet(X2,join(X3,meet(X1,X3)))) = meet(X1,meet(X3,X2)),
inference(orient,[status(thm)],[t59783]) ).
cnf(t1424,plain,
meet(X1,meet(meet(X2,join(X3,meet(X1,X3))),X4)) = meet(X4,meet(X1,meet(X3,X2))),
inference(cp,[status(thm)],[t15,t1353]) ).
cnf(t59793,plain,
meet(X1,meet(X4,meet(X2,join(X3,meet(X1,X3))))) = meet(X4,meet(X1,meet(X3,X2))),
inference(step,[status(thm)],[t1424,t13]) ).
cnf(t59794,plain,
meet(X1,meet(X2,meet(join(X3,meet(X1,X3)),X4))) = meet(X4,meet(X1,meet(X3,X2))),
inference(step,[status(thm)],[t59793,t15]) ).
cnf(t59795,plain,
meet(X1,meet(X2,meet(X4,join(X3,meet(X1,X3))))) = meet(X4,meet(X1,meet(X3,X2))),
inference(step,[status(thm)],[t59794,t13]) ).
cnf(t59796,plain,
meet(X1,meet(X2,meet(X4,join(X3,meet(X1,X3))))) = meet(X1,meet(meet(X3,X2),X4)),
inference(step,[status(thm)],[t59795,t15]) ).
cnf(t59797,plain,
meet(X1,meet(X2,meet(X4,join(X3,meet(X1,X3))))) = meet(X1,meet(X4,meet(X3,X2))),
inference(step,[status(thm)],[t59796,t13]) ).
cnf(t59798,plain,
meet(X1,meet(X2,meet(X4,join(X3,meet(X1,X3))))) = meet(X1,meet(X2,meet(X4,X3))),
inference(step,[status(thm)],[t59797,t15]) ).
cnf(t59799,plain,
meet(X1,meet(X2,meet(X4,join(X3,meet(X1,X3))))) = meet(X1,meet(X2,meet(X3,X4))),
inference(step,[status(thm)],[t59798,t13]) ).
cnf(t1754,plain,
meet(X1,meet(X2,meet(X3,join(X4,meet(X1,X4))))) = meet(X1,meet(X2,meet(X4,X3))),
inference(orient,[status(thm)],[t59799]) ).
cnf(t1841,plain,
meet(X1,meet(meet(X2,meet(X3,join(X4,meet(X1,X4)))),Y4)) = meet(Y4,meet(X1,meet(X2,meet(X4,X3)))),
inference(cp,[status(thm)],[t15,t1754]) ).
cnf(t59830,plain,
meet(X1,meet(Y4,meet(X2,meet(X3,join(X4,meet(X1,X4)))))) = meet(Y4,meet(X1,meet(X2,meet(X4,X3)))),
inference(step,[status(thm)],[t1841,t13]) ).
cnf(t59831,plain,
meet(X1,meet(X2,meet(meet(X3,join(X4,meet(X1,X4))),Y4))) = meet(Y4,meet(X1,meet(X2,meet(X4,X3)))),
inference(step,[status(thm)],[t59830,t15]) ).
cnf(t59832,plain,
meet(X1,meet(X2,meet(Y4,meet(X3,join(X4,meet(X1,X4)))))) = meet(Y4,meet(X1,meet(X2,meet(X4,X3)))),
inference(step,[status(thm)],[t59831,t13]) ).
cnf(t59833,plain,
meet(X1,meet(X2,meet(X3,meet(join(X4,meet(X1,X4)),Y4)))) = meet(Y4,meet(X1,meet(X2,meet(X4,X3)))),
inference(step,[status(thm)],[t59832,t15]) ).
cnf(t59834,plain,
meet(X1,meet(X2,meet(X3,meet(Y4,join(X4,meet(X1,X4)))))) = meet(Y4,meet(X1,meet(X2,meet(X4,X3)))),
inference(step,[status(thm)],[t59833,t13]) ).
cnf(t59835,plain,
meet(X1,meet(X2,meet(X3,meet(Y4,join(X4,meet(X1,X4)))))) = meet(X1,meet(meet(X2,meet(X4,X3)),Y4)),
inference(step,[status(thm)],[t59834,t15]) ).
cnf(t59836,plain,
meet(X1,meet(X2,meet(X3,meet(Y4,join(X4,meet(X1,X4)))))) = meet(X1,meet(Y4,meet(X2,meet(X4,X3)))),
inference(step,[status(thm)],[t59835,t13]) ).
cnf(t59837,plain,
meet(X1,meet(X2,meet(X3,meet(Y4,join(X4,meet(X1,X4)))))) = meet(X1,meet(X2,meet(meet(X4,X3),Y4))),
inference(step,[status(thm)],[t59836,t15]) ).
cnf(t59838,plain,
meet(X1,meet(X2,meet(X3,meet(Y4,join(X4,meet(X1,X4)))))) = meet(X1,meet(X2,meet(Y4,meet(X4,X3)))),
inference(step,[status(thm)],[t59837,t13]) ).
cnf(t59839,plain,
meet(X1,meet(X2,meet(X3,meet(Y4,join(X4,meet(X1,X4)))))) = meet(X1,meet(X2,meet(X3,meet(Y4,X4)))),
inference(step,[status(thm)],[t59838,t15]) ).
cnf(t59840,plain,
meet(X1,meet(X2,meet(X3,meet(Y4,join(X4,meet(X1,X4)))))) = meet(X1,meet(X2,meet(X3,meet(X4,Y4)))),
inference(step,[status(thm)],[t59839,t13]) ).
cnf(t2715,plain,
meet(X1,meet(X2,meet(X3,meet(X4,join(Y4,meet(X1,Y4)))))) = meet(X1,meet(X2,meet(X3,meet(Y4,X4)))),
inference(orient,[status(thm)],[t59840]) ).
cnf(t452,plain,
meet(X1,meet(join(X2,meet(join(X1,X2),join(X1,X3))),X4)) = meet(X4,X1),
inference(cp,[status(thm)],[t15,t420]) ).
cnf(t59739,plain,
meet(X1,meet(X4,join(X2,meet(join(X1,X2),join(X1,X3))))) = meet(X4,X1),
inference(step,[status(thm)],[t452,t13]) ).
cnf(t59740,plain,
meet(X1,meet(X4,join(X2,meet(join(X1,X2),join(X1,X3))))) = meet(X1,X4),
inference(step,[status(thm)],[t59739,t13]) ).
cnf(t454,plain,
meet(X1,meet(X2,join(X3,meet(join(X1,X3),join(X1,X4))))) = meet(X1,X2),
inference(orient,[status(thm)],[t59740]) ).
cnf(t2730,plain,
meet(join(X1,join(X1,X2)),meet(X3,meet(X1,meet(join(X1,X2),X4)))) = meet(join(X1,join(X1,X2)),meet(X3,meet(X1,X4))),
inference(cp,[status(thm)],[t2715,t454]) ).
cnf(t59848,plain,
meet(X3,meet(meet(X1,meet(join(X1,X2),X4)),join(X1,join(X1,X2)))) = meet(join(X1,join(X1,X2)),meet(X3,meet(X1,X4))),
inference(step,[status(thm)],[t2730,t15]) ).
cnf(t59849,plain,
meet(X3,meet(join(X1,join(X1,X2)),meet(X1,meet(join(X1,X2),X4)))) = meet(join(X1,join(X1,X2)),meet(X3,meet(X1,X4))),
inference(step,[status(thm)],[t59848,t13]) ).
cnf(t59850,plain,
meet(X3,meet(meet(join(X1,X2),X4),meet(join(X1,join(X1,X2)),X1))) = meet(join(X1,join(X1,X2)),meet(X3,meet(X1,X4))),
inference(step,[status(thm)],[t59849,t15]) ).
cnf(t59851,plain,
meet(X3,meet(X1,meet(meet(join(X1,X2),X4),join(X1,join(X1,X2))))) = meet(join(X1,join(X1,X2)),meet(X3,meet(X1,X4))),
inference(step,[status(thm)],[t59850,t15]) ).
cnf(t59852,plain,
meet(X3,meet(X1,meet(join(X1,X2),X4))) = meet(join(X1,join(X1,X2)),meet(X3,meet(X1,X4))),
inference(step,[status(thm)],[t59851,t92]) ).
cnf(t59853,plain,
meet(X1,meet(meet(join(X1,X2),X4),X3)) = meet(join(X1,join(X1,X2)),meet(X3,meet(X1,X4))),
inference(step,[status(thm)],[t59852,t15]) ).
cnf(t59854,plain,
meet(X1,meet(X3,meet(join(X1,X2),X4))) = meet(join(X1,join(X1,X2)),meet(X3,meet(X1,X4))),
inference(step,[status(thm)],[t59853,t13]) ).
cnf(t59855,plain,
meet(X1,meet(X3,meet(X4,join(X1,X2)))) = meet(join(X1,join(X1,X2)),meet(X3,meet(X1,X4))),
inference(step,[status(thm)],[t59854,t13]) ).
cnf(t101,plain,
meet(X1,meet(meet(X2,join(X1,X3)),X4)) = meet(X4,meet(X1,X2)),
inference(cp,[status(thm)],[t15,t92]) ).
cnf(t59662,plain,
meet(X1,meet(X4,meet(X2,join(X1,X3)))) = meet(X4,meet(X1,X2)),
inference(step,[status(thm)],[t101,t13]) ).
cnf(t59663,plain,
meet(X1,meet(X2,meet(join(X1,X3),X4))) = meet(X4,meet(X1,X2)),
inference(step,[status(thm)],[t59662,t15]) ).
cnf(t59664,plain,
meet(X1,meet(X2,meet(X4,join(X1,X3)))) = meet(X4,meet(X1,X2)),
inference(step,[status(thm)],[t59663,t13]) ).
cnf(t59665,plain,
meet(X1,meet(X2,meet(X4,join(X1,X3)))) = meet(X2,meet(X4,X1)),
inference(step,[status(thm)],[t59664,t15]) ).
cnf(t59666,plain,
meet(X1,meet(X2,meet(X4,join(X1,X3)))) = meet(X1,meet(X2,X4)),
inference(step,[status(thm)],[t59665,t15]) ).
cnf(t125,plain,
meet(X1,meet(X2,meet(X3,join(X1,X4)))) = meet(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t59666]) ).
cnf(t59856,plain,
meet(X1,meet(X3,X4)) = meet(join(X1,join(X1,X2)),meet(X3,meet(X1,X4))),
inference(step,[status(thm)],[t59855,t125]) ).
cnf(t59857,plain,
meet(X1,meet(X3,X4)) = meet(meet(X1,X4),meet(join(X1,join(X1,X2)),X3)),
inference(step,[status(thm)],[t59856,t15]) ).
cnf(t59858,plain,
meet(X1,meet(X3,X4)) = meet(X3,meet(meet(X1,X4),join(X1,join(X1,X2)))),
inference(step,[status(thm)],[t59857,t15]) ).
cnf(t59859,plain,
meet(X1,meet(X3,X4)) = meet(X3,meet(meet(X1,X4),join(X1,X2))),
inference(step,[status(thm)],[t59858,t82]) ).
cnf(t3000,plain,
meet(X1,meet(meet(X2,X3),join(X2,X4))) = meet(X2,meet(X1,X3)),
inference(orient,[status(thm)],[t59859]) ).
cnf(t18,plain,
meet(X1,meet(X2,X1)) = meet(X2,X1),
inference(cp,[status(thm)],[t15,t9]) ).
cnf(t59651,plain,
meet(X1,meet(X1,X2)) = meet(X2,X1),
inference(step,[status(thm)],[t18,t15]) ).
cnf(t59652,plain,
meet(X1,meet(X1,X2)) = meet(X1,X2),
inference(step,[status(thm)],[t59651,t13]) ).
cnf(t73,plain,
meet(X1,meet(X1,X2)) = meet(X1,X2),
inference(orient,[status(thm)],[t59652]) ).
cnf(t3005,plain,
meet(X1,meet(meet(X1,X2),X2)) = meet(meet(X1,X2),join(X1,X3)),
inference(cp,[status(thm)],[t3000,t73]) ).
cnf(t59860,plain,
meet(X1,meet(X2,meet(X1,X2))) = meet(meet(X1,X2),join(X1,X3)),
inference(step,[status(thm)],[t3005,t13]) ).
cnf(t59861,plain,
meet(X1,meet(X1,meet(X2,X2))) = meet(meet(X1,X2),join(X1,X3)),
inference(step,[status(thm)],[t59860,t15]) ).
cnf(t59862,plain,
meet(X1,meet(X2,X2)) = meet(meet(X1,X2),join(X1,X3)),
inference(step,[status(thm)],[t59861,t73]) ).
cnf(t59863,plain,
meet(X1,X2) = meet(meet(X1,X2),join(X1,X3)),
inference(step,[status(thm)],[t59862,t9]) ).
cnf(t3126,plain,
meet(meet(X1,X2),join(X1,X3)) = meet(X1,X2),
inference(orient,[status(thm)],[t59863]) ).
cnf(t1499,plain,
meet(X1,meet(join(meet(X1,X2),meet(X2,X3)),X4)) = meet(X4,meet(X1,X2)),
inference(cp,[status(thm)],[t15,t1426]) ).
cnf(t59789,plain,
meet(X1,meet(X4,join(meet(X1,X2),meet(X2,X3)))) = meet(X4,meet(X1,X2)),
inference(step,[status(thm)],[t1499,t13]) ).
cnf(t59790,plain,
meet(X1,meet(X4,join(meet(X1,X2),meet(X2,X3)))) = meet(X2,meet(X4,X1)),
inference(step,[status(thm)],[t59789,t15]) ).
cnf(t59791,plain,
meet(X1,meet(X4,join(meet(X1,X2),meet(X2,X3)))) = meet(X1,meet(X2,X4)),
inference(step,[status(thm)],[t59790,t15]) ).
cnf(t1552,plain,
meet(X1,meet(X2,join(meet(X1,X3),meet(X3,X4)))) = meet(X1,meet(X3,X2)),
inference(orient,[status(thm)],[t59791]) ).
cnf(t766,plain,
meet(X1,join(X2,meet(X1,X3))) = meet(X1,join(X2,join(meet(X1,X2),meet(X1,X3)))),
inference(cp,[status(thm)],[t764,t48]) ).
cnf(t807,plain,
meet(X1,join(X2,join(meet(X1,X2),meet(X1,X3)))) = meet(X1,join(X2,meet(X1,X3))),
inference(orient,[status(thm)],[t766]) ).
cnf(t3147,plain,
meet(meet(X1,X2),join(join(X1,X3),meet(meet(X1,X2),X4))) = meet(meet(X1,X2),join(join(X1,X3),join(meet(X1,X2),meet(meet(X1,X2),X4)))),
inference(cp,[status(thm)],[t807,t3126]) ).
cnf(t59919,plain,
meet(meet(X1,X2),join(join(X1,X3),meet(X4,meet(X1,X2)))) = meet(meet(X1,X2),join(join(X1,X3),join(meet(X1,X2),meet(meet(X1,X2),X4)))),
inference(step,[status(thm)],[t3147,t13]) ).
cnf(t59920,plain,
meet(meet(X1,X2),join(join(X1,X3),meet(X2,meet(X4,X1)))) = meet(meet(X1,X2),join(join(X1,X3),join(meet(X1,X2),meet(meet(X1,X2),X4)))),
inference(step,[status(thm)],[t59919,t15]) ).
cnf(t59921,plain,
meet(meet(X1,X2),join(join(X1,X3),meet(X1,meet(X2,X4)))) = meet(meet(X1,X2),join(join(X1,X3),join(meet(X1,X2),meet(meet(X1,X2),X4)))),
inference(step,[status(thm)],[t59920,t15]) ).
cnf(t59922,plain,
meet(meet(X1,X2),join(join(X1,X3),meet(X1,meet(X2,X4)))) = meet(meet(X1,X2),join(meet(X1,X2),join(meet(meet(X1,X2),X4),join(X1,X3)))),
inference(step,[status(thm)],[t59921,t52]) ).
cnf(t59923,plain,
meet(meet(X1,X2),join(join(X1,X3),meet(X1,meet(X2,X4)))) = meet(X1,X2),
inference(step,[status(thm)],[t59922,t10]) ).
cnf(t5417,plain,
meet(meet(X1,X2),join(join(X1,X3),meet(X1,meet(X2,X4)))) = meet(X1,X2),
inference(orient,[status(thm)],[t59923]) ).
cnf(t117,plain,
meet(X1,join(X2,join(X3,meet(X1,X4)))) = meet(X1,join(X2,meet(join(X3,meet(X1,X4)),join(X1,X3)))),
inference(cp,[status(thm)],[t114,t103]) ).
cnf(t59699,plain,
meet(X1,join(X2,join(X3,meet(X1,X4)))) = meet(X1,join(X2,meet(join(X1,X3),join(X3,meet(X1,X4))))),
inference(step,[status(thm)],[t117,t13]) ).
cnf(t275,plain,
meet(X1,join(X2,meet(join(X1,X3),join(X3,meet(X1,X4))))) = meet(X1,join(X2,join(X3,meet(X1,X4)))),
inference(orient,[status(thm)],[t59699]) ).
cnf(t1365,plain,
meet(join(X1,X2),meet(join(X2,meet(X1,X3)),X1)) = meet(join(X1,X2),meet(X1,join(join(X2,meet(X1,X3)),join(X2,meet(X1,X3))))),
inference(cp,[status(thm)],[t1353,t275]) ).
cnf(t59803,plain,
meet(X1,meet(join(X1,X2),join(X2,meet(X1,X3)))) = meet(join(X1,X2),meet(X1,join(join(X2,meet(X1,X3)),join(X2,meet(X1,X3))))),
inference(step,[status(thm)],[t1365,t15]) ).
cnf(t59804,plain,
meet(X1,meet(join(X1,X2),join(X2,meet(X1,X3)))) = meet(X1,meet(join(join(X2,meet(X1,X3)),join(X2,meet(X1,X3))),join(X1,X2))),
inference(step,[status(thm)],[t59803,t15]) ).
cnf(t59805,plain,
meet(X1,meet(join(X1,X2),join(X2,meet(X1,X3)))) = meet(X1,join(join(X2,meet(X1,X3)),join(X2,meet(X1,X3)))),
inference(step,[status(thm)],[t59804,t92]) ).
cnf(t59806,plain,
meet(X1,meet(join(X1,X2),join(X2,meet(X1,X3)))) = meet(X1,join(X2,meet(X1,X3))),
inference(step,[status(thm)],[t59805,t11]) ).
cnf(t2023,plain,
meet(X1,meet(join(X1,X2),join(X2,meet(X1,X3)))) = meet(X1,join(X2,meet(X1,X3))),
inference(orient,[status(thm)],[t59806]) ).
cnf(t5516,plain,
meet(X1,join(X1,X2)) = meet(meet(X1,join(X1,X2)),join(join(X1,X3),meet(X1,join(X2,meet(X1,X4))))),
inference(cp,[status(thm)],[t5417,t2023]) ).
cnf(t59924,plain,
X1 = meet(meet(X1,join(X1,X2)),join(join(X1,X3),meet(X1,join(X2,meet(X1,X4))))),
inference(step,[status(thm)],[t5516,t10]) ).
cnf(t59925,plain,
X1 = meet(X1,join(join(X1,X3),meet(X1,join(X2,meet(X1,X4))))),
inference(step,[status(thm)],[t59924,t10]) ).
cnf(t5601,plain,
meet(X1,join(join(X1,X2),meet(X1,join(X3,meet(X1,X4))))) = X1,
inference(orient,[status(thm)],[t59925]) ).
cnf(t5649,plain,
meet(X1,meet(join(join(X1,X2),meet(X1,join(X3,meet(X1,X4)))),Y4)) = meet(X1,meet(Y4,join(X1,meet(join(join(X1,X2),meet(X1,join(X3,meet(X1,X4)))),Y5)))),
inference(cp,[status(thm)],[t1552,t5601]) ).
cnf(t59995,plain,
meet(X1,meet(Y4,join(join(X1,X2),meet(X1,join(X3,meet(X1,X4)))))) = meet(X1,meet(Y4,join(X1,meet(join(join(X1,X2),meet(X1,join(X3,meet(X1,X4)))),Y5)))),
inference(step,[status(thm)],[t5649,t13]) ).
cnf(t59996,plain,
meet(X1,meet(Y4,join(join(X1,X2),meet(X1,join(X3,meet(X1,X4)))))) = meet(X1,Y4),
inference(step,[status(thm)],[t59995,t92]) ).
cnf(t8065,plain,
meet(X1,meet(X2,join(join(X1,X3),meet(X1,join(X4,meet(X1,Y4)))))) = meet(X1,X2),
inference(orient,[status(thm)],[t59996]) ).
cnf(t79,plain,
meet(X1,join(X2,meet(X3,join(X1,meet(X3,X4))))) = meet(X1,join(X2,join(meet(X3,X4),meet(X3,join(X1,X2))))),
inference(cp,[status(thm)],[t33,t73]) ).
cnf(t59694,plain,
meet(X1,join(X2,meet(X3,join(X1,meet(X3,X4))))) = meet(X1,join(X2,meet(X3,join(X1,X4)))),
inference(step,[status(thm)],[t79,t33]) ).
cnf(t223,plain,
meet(X1,join(X2,meet(X3,join(X1,meet(X3,X4))))) = meet(X1,join(X2,meet(X3,join(X1,X4)))),
inference(orient,[status(thm)],[t59694]) ).
cnf(t8069,plain,
meet(X1,X2) = meet(X1,meet(X2,join(join(X1,X3),meet(X1,join(X2,X4))))),
inference(cp,[status(thm)],[t8065,t223]) ).
cnf(t8167,plain,
meet(X1,meet(X2,join(join(X1,X3),meet(X1,join(X2,X4))))) = meet(X1,X2),
inference(orient,[status(thm)],[t8069]) ).
cnf(t8190,plain,
meet(X1,join(X2,X3)) = meet(X1,meet(join(X2,X3),join(join(X1,X4),X1))),
inference(cp,[status(thm)],[t8167,t529]) ).
cnf(t59997,plain,
meet(X1,join(X2,X3)) = meet(X1,meet(join(X2,X3),join(X1,join(X1,X4)))),
inference(step,[status(thm)],[t8190,t48]) ).
cnf(t59998,plain,
meet(X1,join(X2,X3)) = meet(X1,meet(join(X2,X3),join(X1,X4))),
inference(step,[status(thm)],[t59997,t82]) ).
cnf(t59999,plain,
meet(X1,join(X2,X3)) = meet(X1,meet(join(X1,X4),join(X2,X3))),
inference(step,[status(thm)],[t59998,t13]) ).
cnf(t8254,plain,
meet(X1,meet(join(X1,X2),join(X3,X4))) = meet(X1,join(X3,X4)),
inference(orient,[status(thm)],[t59999]) ).
cnf(t8296,plain,
meet(X1,join(meet(join(X1,X2),X3),meet(X3,X4))) = meet(X1,meet(join(X1,X2),X3)),
inference(cp,[status(thm)],[t8254,t1426]) ).
cnf(t60009,plain,
meet(X1,join(meet(X3,X4),meet(join(X1,X2),X3))) = meet(X1,meet(join(X1,X2),X3)),
inference(step,[status(thm)],[t8296,t48]) ).
cnf(t60010,plain,
meet(X1,join(meet(X3,X4),meet(X3,join(X1,X2)))) = meet(X1,meet(join(X1,X2),X3)),
inference(step,[status(thm)],[t60009,t13]) ).
cnf(t60011,plain,
meet(X1,join(meet(X3,X4),meet(X3,join(X1,X2)))) = meet(X1,meet(X3,join(X1,X2))),
inference(step,[status(thm)],[t60010,t13]) ).
cnf(t60012,plain,
meet(X1,join(meet(X3,X4),meet(X3,join(X1,X2)))) = meet(X1,X3),
inference(step,[status(thm)],[t60011,t92]) ).
cnf(t8935,plain,
meet(X1,join(meet(X2,X3),meet(X2,join(X1,X4)))) = meet(X1,X2),
inference(orient,[status(thm)],[t60012]) ).
cnf(t8981,plain,
meet(meet(X1,X2),X3) = meet(meet(X1,X2),join(meet(X3,X4),meet(X3,X1))),
inference(cp,[status(thm)],[t8935,t8935]) ).
cnf(t60013,plain,
meet(X3,meet(X1,X2)) = meet(meet(X1,X2),join(meet(X3,X4),meet(X3,X1))),
inference(step,[status(thm)],[t8981,t13]) ).
cnf(t60014,plain,
meet(X2,meet(X3,X1)) = meet(meet(X1,X2),join(meet(X3,X4),meet(X3,X1))),
inference(step,[status(thm)],[t60013,t15]) ).
cnf(t60015,plain,
meet(X1,meet(X2,X3)) = meet(meet(X1,X2),join(meet(X3,X4),meet(X3,X1))),
inference(step,[status(thm)],[t60014,t15]) ).
cnf(t60016,plain,
meet(X1,meet(X2,X3)) = meet(meet(X1,X2),join(meet(X3,X1),meet(X3,X4))),
inference(step,[status(thm)],[t60015,t48]) ).
cnf(t60017,plain,
meet(X1,meet(X2,X3)) = meet(meet(X1,X2),join(meet(X1,X3),meet(X3,X4))),
inference(step,[status(thm)],[t60016,t13]) ).
cnf(t9075,plain,
meet(meet(X1,X2),join(meet(X1,X3),meet(X3,X4))) = meet(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t60017]) ).
cnf(t9292,plain,
meet(meet(X1,X2),join(meet(X1,X3),meet(X3,X4))) = meet(meet(X1,meet(X2,X3)),join(meet(X1,X2),Y4)),
inference(cp,[status(thm)],[t3126,t9075]) ).
cnf(t60020,plain,
meet(X1,meet(X2,X3)) = meet(meet(X1,meet(X2,X3)),join(meet(X1,X2),Y4)),
inference(step,[status(thm)],[t9292,t9075]) ).
cnf(t60021,plain,
meet(X1,meet(X2,X3)) = meet(meet(X1,meet(X2,X3)),join(Y4,meet(X1,X2))),
inference(step,[status(thm)],[t60020,t48]) ).
cnf(t10106,plain,
meet(meet(X1,meet(X2,X3)),join(X4,meet(X1,X2))) = meet(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t60021]) ).
cnf(t1432,plain,
meet(X1,join(X2,meet(X1,X2))) = meet(X1,join(meet(X1,X2),meet(join(X2,meet(X1,X2)),X3))),
inference(cp,[status(thm)],[t1426,t1282]) ).
cnf(t59800,plain,
meet(X1,X2) = meet(X1,join(meet(X1,X2),meet(join(X2,meet(X1,X2)),X3))),
inference(step,[status(thm)],[t1432,t1282]) ).
cnf(t59801,plain,
meet(X1,X2) = meet(X1,join(meet(X1,X2),meet(X3,join(X2,meet(X1,X2))))),
inference(step,[status(thm)],[t59800,t13]) ).
cnf(t1843,plain,
meet(X1,join(meet(X1,X2),meet(X3,join(X2,meet(X1,X2))))) = meet(X1,X2),
inference(orient,[status(thm)],[t59801]) ).
cnf(t1965,plain,
meet(X1,meet(join(meet(X1,X2),meet(X3,join(X2,meet(X1,X2)))),X4)) = meet(X4,meet(X1,X2)),
inference(cp,[status(thm)],[t15,t1843]) ).
cnf(t59878,plain,
meet(X1,meet(X4,join(meet(X1,X2),meet(X3,join(X2,meet(X1,X2)))))) = meet(X4,meet(X1,X2)),
inference(step,[status(thm)],[t1965,t13]) ).
cnf(t59879,plain,
meet(X1,meet(X4,join(meet(X1,X2),meet(X3,join(X2,meet(X1,X2)))))) = meet(X2,meet(X4,X1)),
inference(step,[status(thm)],[t59878,t15]) ).
cnf(t59880,plain,
meet(X1,meet(X4,join(meet(X1,X2),meet(X3,join(X2,meet(X1,X2)))))) = meet(X1,meet(X2,X4)),
inference(step,[status(thm)],[t59879,t15]) ).
cnf(t3835,plain,
meet(X1,meet(X2,join(meet(X1,X3),meet(X4,join(X3,meet(X1,X3)))))) = meet(X1,meet(X3,X2)),
inference(orient,[status(thm)],[t59880]) ).
cnf(t10111,plain,
meet(X1,meet(X2,join(meet(X1,X3),meet(X4,join(X3,meet(X1,X3)))))) = meet(meet(X1,meet(X3,X2)),join(Y4,meet(X1,X2))),
inference(cp,[status(thm)],[t10106,t3835]) ).
cnf(t60022,plain,
meet(X1,meet(X3,X2)) = meet(meet(X1,meet(X3,X2)),join(Y4,meet(X1,X2))),
inference(step,[status(thm)],[t10111,t3835]) ).
cnf(t10311,plain,
meet(meet(X1,meet(X2,X3)),join(X4,meet(X1,X3))) = meet(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t60022]) ).
cnf(t10405,plain,
meet(X1,meet(X2,join(X2,X3))) = meet(meet(X1,X2),join(X4,meet(X1,join(X2,X3)))),
inference(cp,[status(thm)],[t10311,t10]) ).
cnf(t60023,plain,
meet(X1,X2) = meet(meet(X1,X2),join(X4,meet(X1,join(X2,X3)))),
inference(step,[status(thm)],[t10405,t10]) ).
cnf(t10593,plain,
meet(meet(X1,X2),join(X3,meet(X1,join(X2,X4)))) = meet(X1,X2),
inference(orient,[status(thm)],[t60023]) ).
cnf(t10778,plain,
meet(X1,meet(meet(X2,X1),join(X3,X2))) = meet(X1,meet(X2,X1)),
inference(cp,[status(thm)],[t169,t10593]) ).
cnf(t60024,plain,
meet(X1,meet(meet(X1,X2),join(X3,X2))) = meet(X1,meet(X2,X1)),
inference(step,[status(thm)],[t10778,t13]) ).
cnf(t60025,plain,
meet(X1,meet(meet(X1,X2),join(X2,X3))) = meet(X1,meet(X2,X1)),
inference(step,[status(thm)],[t60024,t48]) ).
cnf(t60026,plain,
meet(X1,meet(meet(X1,X2),join(X2,X3))) = meet(X1,meet(X1,X2)),
inference(step,[status(thm)],[t60025,t15]) ).
cnf(t60027,plain,
meet(X1,meet(meet(X1,X2),join(X2,X3))) = meet(X1,X2),
inference(step,[status(thm)],[t60026,t73]) ).
cnf(t10807,plain,
meet(X1,meet(meet(X1,X2),join(X2,X3))) = meet(X1,X2),
inference(orient,[status(thm)],[t60027]) ).
cnf(t8366,plain,
meet(X1,meet(meet(join(X1,X2),join(X3,X4)),Y4)) = meet(Y4,meet(X1,join(X3,X4))),
inference(cp,[status(thm)],[t15,t8254]) ).
cnf(t60044,plain,
meet(X1,meet(Y4,meet(join(X1,X2),join(X3,X4)))) = meet(Y4,meet(X1,join(X3,X4))),
inference(step,[status(thm)],[t8366,t13]) ).
cnf(t60045,plain,
meet(X1,meet(Y4,meet(join(X1,X2),join(X3,X4)))) = meet(X1,meet(join(X3,X4),Y4)),
inference(step,[status(thm)],[t60044,t15]) ).
cnf(t60046,plain,
meet(X1,meet(Y4,meet(join(X1,X2),join(X3,X4)))) = meet(X1,meet(Y4,join(X3,X4))),
inference(step,[status(thm)],[t60045,t13]) ).
cnf(t12055,plain,
meet(X1,meet(X2,meet(join(X1,X3),join(X4,Y4)))) = meet(X1,meet(X2,join(X4,Y4))),
inference(orient,[status(thm)],[t60046]) ).
cnf(t1638,plain,
meet(X1,meet(meet(X2,join(meet(X1,X3),meet(X3,X4))),Y4)) = meet(Y4,meet(X1,meet(X3,X2))),
inference(cp,[status(thm)],[t15,t1552]) ).
cnf(t59810,plain,
meet(X1,meet(Y4,meet(X2,join(meet(X1,X3),meet(X3,X4))))) = meet(Y4,meet(X1,meet(X3,X2))),
inference(step,[status(thm)],[t1638,t13]) ).
cnf(t59811,plain,
meet(X1,meet(X2,meet(join(meet(X1,X3),meet(X3,X4)),Y4))) = meet(Y4,meet(X1,meet(X3,X2))),
inference(step,[status(thm)],[t59810,t15]) ).
cnf(t59812,plain,
meet(X1,meet(X2,meet(Y4,join(meet(X1,X3),meet(X3,X4))))) = meet(Y4,meet(X1,meet(X3,X2))),
inference(step,[status(thm)],[t59811,t13]) ).
cnf(t59813,plain,
meet(X1,meet(X2,meet(Y4,join(meet(X1,X3),meet(X3,X4))))) = meet(X1,meet(meet(X3,X2),Y4)),
inference(step,[status(thm)],[t59812,t15]) ).
cnf(t59814,plain,
meet(X1,meet(X2,meet(Y4,join(meet(X1,X3),meet(X3,X4))))) = meet(X1,meet(Y4,meet(X3,X2))),
inference(step,[status(thm)],[t59813,t13]) ).
cnf(t59815,plain,
meet(X1,meet(X2,meet(Y4,join(meet(X1,X3),meet(X3,X4))))) = meet(X1,meet(X2,meet(Y4,X3))),
inference(step,[status(thm)],[t59814,t15]) ).
cnf(t59816,plain,
meet(X1,meet(X2,meet(Y4,join(meet(X1,X3),meet(X3,X4))))) = meet(X1,meet(X2,meet(X3,Y4))),
inference(step,[status(thm)],[t59815,t13]) ).
cnf(t2134,plain,
meet(X1,meet(X2,meet(X3,join(meet(X1,X4),meet(X4,Y4))))) = meet(X1,meet(X2,meet(X4,X3))),
inference(orient,[status(thm)],[t59816]) ).
cnf(t5626,plain,
meet(X1,X2) = meet(meet(X1,X2),join(join(meet(X1,X2),X3),meet(X1,X2))),
inference(cp,[status(thm)],[t5601,t3126]) ).
cnf(t59926,plain,
meet(X1,X2) = meet(meet(X1,X2),join(meet(X1,X2),join(meet(X1,X2),X3))),
inference(step,[status(thm)],[t5626,t48]) ).
cnf(t59927,plain,
meet(X1,X2) = meet(meet(X1,X2),join(meet(X1,X2),X3)),
inference(step,[status(thm)],[t59926,t82]) ).
cnf(t59928,plain,
meet(X1,X2) = meet(meet(X1,X2),join(X3,meet(X1,X2))),
inference(step,[status(thm)],[t59927,t48]) ).
cnf(t5711,plain,
meet(meet(X1,X2),join(X3,meet(X1,X2))) = meet(X1,X2),
inference(orient,[status(thm)],[t59928]) ).
cnf(t5771,plain,
meet(meet(X1,X2),meet(X3,meet(join(X4,meet(X1,X2)),Y4))) = meet(meet(X1,X2),meet(X3,meet(Y4,join(meet(X1,X2),meet(join(X4,meet(X1,X2)),Y5))))),
inference(cp,[status(thm)],[t2134,t5711]) ).
cnf(t59929,plain,
meet(X3,meet(meet(join(X4,meet(X1,X2)),Y4),meet(X1,X2))) = meet(meet(X1,X2),meet(X3,meet(Y4,join(meet(X1,X2),meet(join(X4,meet(X1,X2)),Y5))))),
inference(step,[status(thm)],[t5771,t15]) ).
cnf(t59930,plain,
meet(X3,meet(X2,meet(meet(join(X4,meet(X1,X2)),Y4),X1))) = meet(meet(X1,X2),meet(X3,meet(Y4,join(meet(X1,X2),meet(join(X4,meet(X1,X2)),Y5))))),
inference(step,[status(thm)],[t59929,t15]) ).
cnf(t59931,plain,
meet(X3,meet(X1,meet(X2,meet(join(X4,meet(X1,X2)),Y4)))) = meet(meet(X1,X2),meet(X3,meet(Y4,join(meet(X1,X2),meet(join(X4,meet(X1,X2)),Y5))))),
inference(step,[status(thm)],[t59930,t15]) ).
cnf(t59932,plain,
meet(X1,meet(meet(X2,meet(join(X4,meet(X1,X2)),Y4)),X3)) = meet(meet(X1,X2),meet(X3,meet(Y4,join(meet(X1,X2),meet(join(X4,meet(X1,X2)),Y5))))),
inference(step,[status(thm)],[t59931,t15]) ).
cnf(t59933,plain,
meet(X1,meet(X3,meet(X2,meet(join(X4,meet(X1,X2)),Y4)))) = meet(meet(X1,X2),meet(X3,meet(Y4,join(meet(X1,X2),meet(join(X4,meet(X1,X2)),Y5))))),
inference(step,[status(thm)],[t59932,t13]) ).
cnf(t59934,plain,
meet(X1,meet(X2,meet(meet(join(X4,meet(X1,X2)),Y4),X3))) = meet(meet(X1,X2),meet(X3,meet(Y4,join(meet(X1,X2),meet(join(X4,meet(X1,X2)),Y5))))),
inference(step,[status(thm)],[t59933,t15]) ).
cnf(t59935,plain,
meet(X1,meet(X2,meet(X3,meet(join(X4,meet(X1,X2)),Y4)))) = meet(meet(X1,X2),meet(X3,meet(Y4,join(meet(X1,X2),meet(join(X4,meet(X1,X2)),Y5))))),
inference(step,[status(thm)],[t59934,t13]) ).
cnf(t59936,plain,
meet(X1,meet(X2,meet(X3,meet(Y4,join(X4,meet(X1,X2)))))) = meet(meet(X1,X2),meet(X3,meet(Y4,join(meet(X1,X2),meet(join(X4,meet(X1,X2)),Y5))))),
inference(step,[status(thm)],[t59935,t13]) ).
cnf(t59937,plain,
meet(X1,meet(X2,meet(X3,meet(Y4,join(X4,meet(X1,X2)))))) = meet(meet(X1,X2),meet(X3,Y4)),
inference(step,[status(thm)],[t59936,t125]) ).
cnf(t59938,plain,
meet(X1,meet(X2,meet(X3,meet(Y4,join(X4,meet(X1,X2)))))) = meet(Y4,meet(meet(X1,X2),X3)),
inference(step,[status(thm)],[t59937,t15]) ).
cnf(t59939,plain,
meet(X1,meet(X2,meet(X3,meet(Y4,join(X4,meet(X1,X2)))))) = meet(X3,meet(Y4,meet(X1,X2))),
inference(step,[status(thm)],[t59938,t15]) ).
cnf(t59940,plain,
meet(X1,meet(X2,meet(X3,meet(Y4,join(X4,meet(X1,X2)))))) = meet(X3,meet(X2,meet(Y4,X1))),
inference(step,[status(thm)],[t59939,t15]) ).
cnf(t59941,plain,
meet(X1,meet(X2,meet(X3,meet(Y4,join(X4,meet(X1,X2)))))) = meet(X3,meet(X1,meet(X2,Y4))),
inference(step,[status(thm)],[t59940,t15]) ).
cnf(t59942,plain,
meet(X1,meet(X2,meet(X3,meet(Y4,join(X4,meet(X1,X2)))))) = meet(X1,meet(meet(X2,Y4),X3)),
inference(step,[status(thm)],[t59941,t15]) ).
cnf(t59943,plain,
meet(X1,meet(X2,meet(X3,meet(Y4,join(X4,meet(X1,X2)))))) = meet(X1,meet(X3,meet(X2,Y4))),
inference(step,[status(thm)],[t59942,t13]) ).
cnf(t59944,plain,
meet(X1,meet(X2,meet(X3,meet(Y4,join(X4,meet(X1,X2)))))) = meet(X1,meet(X2,meet(Y4,X3))),
inference(step,[status(thm)],[t59943,t15]) ).
cnf(t59945,plain,
meet(X1,meet(X2,meet(X3,meet(Y4,join(X4,meet(X1,X2)))))) = meet(X1,meet(X2,meet(X3,Y4))),
inference(step,[status(thm)],[t59944,t13]) ).
cnf(t5887,plain,
meet(X1,meet(X2,meet(X3,meet(X4,join(Y4,meet(X1,X2)))))) = meet(X1,meet(X2,meet(X3,X4))),
inference(orient,[status(thm)],[t59945]) ).
cnf(t5895,plain,
meet(X1,meet(X2,meet(X2,X3))) = meet(X1,meet(X2,meet(X3,join(X4,meet(X1,X2))))),
inference(cp,[status(thm)],[t5887,t73]) ).
cnf(t59946,plain,
meet(X1,meet(X2,X3)) = meet(X1,meet(X2,meet(X3,join(X4,meet(X1,X2))))),
inference(step,[status(thm)],[t5895,t73]) ).
cnf(t6061,plain,
meet(X1,meet(X2,meet(X3,join(X4,meet(X1,X2))))) = meet(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t59946]) ).
cnf(t2069,plain,
meet(X1,meet(meet(join(X1,X2),join(X2,meet(X1,X3))),X4)) = meet(X4,meet(X1,join(X2,meet(X1,X3)))),
inference(cp,[status(thm)],[t15,t2023]) ).
cnf(t59841,plain,
meet(X1,meet(X4,meet(join(X1,X2),join(X2,meet(X1,X3))))) = meet(X4,meet(X1,join(X2,meet(X1,X3)))),
inference(step,[status(thm)],[t2069,t13]) ).
cnf(t59842,plain,
meet(X1,meet(X4,meet(join(X1,X2),join(X2,meet(X1,X3))))) = meet(X1,meet(join(X2,meet(X1,X3)),X4)),
inference(step,[status(thm)],[t59841,t15]) ).
cnf(t59843,plain,
meet(X1,meet(X4,meet(join(X1,X2),join(X2,meet(X1,X3))))) = meet(X1,meet(X4,join(X2,meet(X1,X3)))),
inference(step,[status(thm)],[t59842,t13]) ).
cnf(t2834,plain,
meet(X1,meet(X2,meet(join(X1,X3),join(X3,meet(X1,X4))))) = meet(X1,meet(X2,join(X3,meet(X1,X4)))),
inference(orient,[status(thm)],[t59843]) ).
cnf(t6065,plain,
meet(X1,meet(X2,join(X1,X3))) = meet(X1,meet(X2,join(X3,meet(X1,X2)))),
inference(cp,[status(thm)],[t6061,t2834]) ).
cnf(t59947,plain,
meet(X1,X2) = meet(X1,meet(X2,join(X3,meet(X1,X2)))),
inference(step,[status(thm)],[t6065,t92]) ).
cnf(t6224,plain,
meet(X1,meet(X2,join(X3,meet(X1,X2)))) = meet(X1,X2),
inference(orient,[status(thm)],[t59947]) ).
cnf(t12064,plain,
meet(X1,meet(X2,join(X3,meet(X2,join(X1,X4))))) = meet(X1,meet(X2,join(X1,X4))),
inference(cp,[status(thm)],[t12055,t6224]) ).
cnf(t60047,plain,
meet(X1,meet(X2,join(X3,meet(X2,join(X1,X4))))) = meet(X1,X2),
inference(step,[status(thm)],[t12064,t92]) ).
cnf(t12187,plain,
meet(X1,meet(X2,join(X3,meet(X2,join(X1,X4))))) = meet(X1,X2),
inference(orient,[status(thm)],[t60047]) ).
cnf(t12246,plain,
meet(X1,meet(X2,join(X3,meet(join(X1,X4),join(X2,Y4))))) = meet(X1,meet(X2,join(X1,X4))),
inference(cp,[status(thm)],[t12055,t12187]) ).
cnf(t60079,plain,
meet(X1,meet(X2,join(X3,meet(join(X1,X4),join(X2,Y4))))) = meet(X1,X2),
inference(step,[status(thm)],[t12246,t92]) ).
cnf(t14216,plain,
meet(X1,meet(X2,join(X3,meet(join(X1,X4),join(X2,Y4))))) = meet(X1,X2),
inference(orient,[status(thm)],[t60079]) ).
cnf(t14240,plain,
meet(X1,meet(X2,X3)) = meet(X1,meet(meet(X2,X3),join(X4,meet(join(X1,Y4),X2)))),
inference(cp,[status(thm)],[t14216,t8935]) ).
cnf(t60145,plain,
meet(X1,meet(X2,X3)) = meet(X1,meet(meet(X2,X3),join(X4,meet(X2,join(X1,Y4))))),
inference(step,[status(thm)],[t14240,t13]) ).
cnf(t19157,plain,
meet(X1,meet(meet(X2,X3),join(X4,meet(X2,join(X1,Y4))))) = meet(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t60145]) ).
cnf(t8316,plain,
meet(X1,join(X1,X2)) = meet(meet(X1,join(X1,X2)),join(join(X1,X3),meet(X1,join(X4,Y4)))),
inference(cp,[status(thm)],[t5417,t8254]) ).
cnf(t60000,plain,
X1 = meet(meet(X1,join(X1,X2)),join(join(X1,X3),meet(X1,join(X4,Y4)))),
inference(step,[status(thm)],[t8316,t10]) ).
cnf(t60001,plain,
X1 = meet(X1,join(join(X1,X3),meet(X1,join(X4,Y4)))),
inference(step,[status(thm)],[t60000,t10]) ).
cnf(t8368,plain,
meet(X1,join(join(X1,X2),meet(X1,join(X3,X4)))) = X1,
inference(orient,[status(thm)],[t60001]) ).
cnf(t19196,plain,
meet(join(X1,X2),meet(X1,X3)) = meet(join(X1,X2),meet(meet(X1,X3),join(X4,X1))),
inference(cp,[status(thm)],[t19157,t8368]) ).
cnf(t60146,plain,
meet(X3,meet(join(X1,X2),X1)) = meet(join(X1,X2),meet(meet(X1,X3),join(X4,X1))),
inference(step,[status(thm)],[t19196,t15]) ).
cnf(t60147,plain,
meet(X1,meet(X3,join(X1,X2))) = meet(join(X1,X2),meet(meet(X1,X3),join(X4,X1))),
inference(step,[status(thm)],[t60146,t15]) ).
cnf(t60148,plain,
meet(X1,X3) = meet(join(X1,X2),meet(meet(X1,X3),join(X4,X1))),
inference(step,[status(thm)],[t60147,t92]) ).
cnf(t60149,plain,
meet(X1,X3) = meet(meet(X1,X3),meet(join(X4,X1),join(X1,X2))),
inference(step,[status(thm)],[t60148,t15]) ).
cnf(t60150,plain,
meet(X1,X3) = meet(meet(X1,X3),meet(join(X1,X2),join(X4,X1))),
inference(step,[status(thm)],[t60149,t13]) ).
cnf(t60151,plain,
meet(X1,X3) = meet(meet(X1,X3),meet(join(X1,X2),join(X1,X4))),
inference(step,[status(thm)],[t60150,t48]) ).
cnf(t19318,plain,
meet(meet(X1,X2),meet(join(X1,X3),join(X1,X4))) = meet(X1,X2),
inference(orient,[status(thm)],[t60151]) ).
cnf(t19354,plain,
meet(meet(X1,X2),meet(join(X1,X3),join(X1,X4))) = meet(meet(X1,X2),meet(meet(X1,X2),join(meet(join(X1,X3),join(X1,X4)),Y4))),
inference(cp,[status(thm)],[t10807,t19318]) ).
cnf(t60152,plain,
meet(X1,X2) = meet(meet(X1,X2),meet(meet(X1,X2),join(meet(join(X1,X3),join(X1,X4)),Y4))),
inference(step,[status(thm)],[t19354,t19318]) ).
cnf(t60153,plain,
meet(X1,X2) = meet(meet(X1,X2),join(meet(join(X1,X3),join(X1,X4)),Y4)),
inference(step,[status(thm)],[t60152,t73]) ).
cnf(t60154,plain,
meet(X1,X2) = meet(meet(X1,X2),join(Y4,meet(join(X1,X3),join(X1,X4)))),
inference(step,[status(thm)],[t60153,t48]) ).
cnf(t19437,plain,
meet(meet(X1,X2),join(X3,meet(join(X1,X4),join(X1,Y4)))) = meet(X1,X2),
inference(orient,[status(thm)],[t60154]) ).
cnf(t19541,plain,
meet(X1,join(X2,X3)) = meet(X1,join(meet(X1,join(X2,X3)),meet(X2,X4))),
inference(cp,[status(thm)],[t2240,t19437]) ).
cnf(t60155,plain,
meet(X1,join(X2,X3)) = meet(X1,join(meet(X2,X4),meet(X1,join(X2,X3)))),
inference(step,[status(thm)],[t19541,t48]) ).
cnf(t19583,plain,
meet(X1,join(meet(X2,X3),meet(X1,join(X2,X4)))) = meet(X1,join(X2,X4)),
inference(orient,[status(thm)],[t60155]) ).
cnf(t19596,plain,
meet(X1,join(X2,X3)) = meet(X1,join(meet(X4,meet(Y4,X2)),meet(X1,join(X2,X3)))),
inference(cp,[status(thm)],[t19583,t15]) ).
cnf(t60191,plain,
meet(X1,join(X2,X3)) = meet(X1,join(meet(X1,join(X2,X3)),meet(X4,meet(Y4,X2)))),
inference(step,[status(thm)],[t19596,t48]) ).
cnf(t60192,plain,
meet(X1,join(X2,X3)) = meet(X1,join(meet(X1,join(X2,X3)),meet(X2,meet(X4,Y4)))),
inference(step,[status(thm)],[t60191,t15]) ).
cnf(t25653,plain,
meet(X1,join(meet(X1,join(X2,X3)),meet(X2,meet(X4,Y4)))) = meet(X1,join(X2,X3)),
inference(orient,[status(thm)],[t60192]) ).
cnf(t30637,plain,
meet(meet(meet(X1,X2),join(X3,X4)),X1) = meet(meet(meet(X1,X2),join(X3,X4)),join(X1,meet(meet(X1,X2),join(X3,X4)))),
inference(cp,[status(thm)],[t30624,t25653]) ).
cnf(t60227,plain,
meet(X1,meet(meet(X1,X2),join(X3,X4))) = meet(meet(meet(X1,X2),join(X3,X4)),join(X1,meet(meet(X1,X2),join(X3,X4)))),
inference(step,[status(thm)],[t30637,t13]) ).
cnf(t60228,plain,
meet(X1,meet(meet(X1,X2),join(X3,X4))) = meet(meet(X1,X2),join(X3,X4)),
inference(step,[status(thm)],[t60227,t5711]) ).
cnf(t30840,plain,
meet(X1,meet(meet(X1,X2),join(X3,X4))) = meet(meet(X1,X2),join(X3,X4)),
inference(orient,[status(thm)],[t60228]) ).
cnf(t30893,plain,
X1 = join(X1,meet(meet(X1,X2),join(X3,X4))),
inference(cp,[status(thm)],[t12,t30840]) ).
cnf(t31039,plain,
join(X1,meet(meet(X1,X2),join(X3,X4))) = X1,
inference(orient,[status(thm)],[t30893]) ).
cnf(t31060,plain,
X1 = join(X1,meet(meet(X2,meet(X3,X1)),join(X4,Y4))),
inference(cp,[status(thm)],[t31039,t15]) ).
cnf(t60229,plain,
X1 = join(X1,meet(join(X4,Y4),meet(X2,meet(X3,X1)))),
inference(step,[status(thm)],[t31060,t13]) ).
cnf(t60230,plain,
X1 = join(X1,meet(meet(X3,X1),meet(join(X4,Y4),X2))),
inference(step,[status(thm)],[t60229,t15]) ).
cnf(t60231,plain,
X1 = join(X1,meet(X2,meet(meet(X3,X1),join(X4,Y4)))),
inference(step,[status(thm)],[t60230,t15]) ).
cnf(t60232,plain,
X1 = join(X1,meet(X2,meet(meet(X1,X3),join(X4,Y4)))),
inference(step,[status(thm)],[t60231,t13]) ).
cnf(t31218,plain,
join(X1,meet(X2,meet(meet(X1,X3),join(X4,Y4)))) = X1,
inference(orient,[status(thm)],[t60232]) ).
cnf(t31349,plain,
join(X1,X2) = join(join(X1,X2),meet(X3,meet(join(X1,X2),join(X4,Y4)))),
inference(cp,[status(thm)],[t31218,t573]) ).
cnf(t35025,plain,
join(join(X1,X2),meet(X3,meet(join(X1,X2),join(X4,Y4)))) = join(X1,X2),
inference(orient,[status(thm)],[t31349]) ).
cnf(t10902,plain,
meet(meet(X1,X2),join(X3,meet(X1,X2))) = meet(meet(X1,X2),meet(meet(X1,X2),join(join(X3,meet(X1,X2)),X4))),
inference(cp,[status(thm)],[t10807,t5711]) ).
cnf(t60028,plain,
meet(X1,X2) = meet(meet(X1,X2),meet(meet(X1,X2),join(join(X3,meet(X1,X2)),X4))),
inference(step,[status(thm)],[t10902,t5711]) ).
cnf(t60029,plain,
meet(X1,X2) = meet(meet(X1,X2),join(join(X3,meet(X1,X2)),X4)),
inference(step,[status(thm)],[t60028,t73]) ).
cnf(t60030,plain,
meet(X1,X2) = meet(meet(X1,X2),join(X4,join(X3,meet(X1,X2)))),
inference(step,[status(thm)],[t60029,t48]) ).
cnf(t60031,plain,
meet(X1,X2) = meet(meet(X1,X2),join(X3,join(meet(X1,X2),X4))),
inference(step,[status(thm)],[t60030,t52]) ).
cnf(t60032,plain,
meet(X1,X2) = meet(meet(X1,X2),join(X3,join(X4,meet(X1,X2)))),
inference(step,[status(thm)],[t60031,t48]) ).
cnf(t10982,plain,
meet(meet(X1,X2),join(X3,join(X4,meet(X1,X2)))) = meet(X1,X2),
inference(orient,[status(thm)],[t60032]) ).
cnf(t11027,plain,
meet(meet(X1,X2),meet(X3,join(X4,join(Y4,meet(X1,X2))))) = meet(meet(meet(X1,X2),X3),join(meet(X1,X2),meet(join(X4,join(Y4,meet(X1,X2))),Y5))),
inference(cp,[status(thm)],[t9075,t10982]) ).
cnf(t60128,plain,
meet(X3,meet(join(X4,join(Y4,meet(X1,X2))),meet(X1,X2))) = meet(meet(meet(X1,X2),X3),join(meet(X1,X2),meet(join(X4,join(Y4,meet(X1,X2))),Y5))),
inference(step,[status(thm)],[t11027,t15]) ).
cnf(t60129,plain,
meet(X3,meet(X2,meet(join(X4,join(Y4,meet(X1,X2))),X1))) = meet(meet(meet(X1,X2),X3),join(meet(X1,X2),meet(join(X4,join(Y4,meet(X1,X2))),Y5))),
inference(step,[status(thm)],[t60128,t15]) ).
cnf(t60130,plain,
meet(X3,meet(X1,meet(X2,join(X4,join(Y4,meet(X1,X2)))))) = meet(meet(meet(X1,X2),X3),join(meet(X1,X2),meet(join(X4,join(Y4,meet(X1,X2))),Y5))),
inference(step,[status(thm)],[t60129,t15]) ).
cnf(t60131,plain,
meet(X1,meet(meet(X2,join(X4,join(Y4,meet(X1,X2)))),X3)) = meet(meet(meet(X1,X2),X3),join(meet(X1,X2),meet(join(X4,join(Y4,meet(X1,X2))),Y5))),
inference(step,[status(thm)],[t60130,t15]) ).
cnf(t60132,plain,
meet(X1,meet(X3,meet(X2,join(X4,join(Y4,meet(X1,X2)))))) = meet(meet(meet(X1,X2),X3),join(meet(X1,X2),meet(join(X4,join(Y4,meet(X1,X2))),Y5))),
inference(step,[status(thm)],[t60131,t13]) ).
cnf(t60133,plain,
meet(X1,meet(X2,meet(join(X4,join(Y4,meet(X1,X2))),X3))) = meet(meet(meet(X1,X2),X3),join(meet(X1,X2),meet(join(X4,join(Y4,meet(X1,X2))),Y5))),
inference(step,[status(thm)],[t60132,t15]) ).
cnf(t60134,plain,
meet(X1,meet(X2,meet(X3,join(X4,join(Y4,meet(X1,X2)))))) = meet(meet(meet(X1,X2),X3),join(meet(X1,X2),meet(join(X4,join(Y4,meet(X1,X2))),Y5))),
inference(step,[status(thm)],[t60133,t13]) ).
cnf(t60135,plain,
meet(X1,meet(X2,meet(X3,join(X4,join(Y4,meet(X1,X2)))))) = meet(meet(X1,X2),X3),
inference(step,[status(thm)],[t60134,t3126]) ).
cnf(t60136,plain,
meet(X1,meet(X2,meet(X3,join(X4,join(Y4,meet(X1,X2)))))) = meet(X3,meet(X1,X2)),
inference(step,[status(thm)],[t60135,t13]) ).
cnf(t60137,plain,
meet(X1,meet(X2,meet(X3,join(X4,join(Y4,meet(X1,X2)))))) = meet(X2,meet(X3,X1)),
inference(step,[status(thm)],[t60136,t15]) ).
cnf(t60138,plain,
meet(X1,meet(X2,meet(X3,join(X4,join(Y4,meet(X1,X2)))))) = meet(X1,meet(X2,X3)),
inference(step,[status(thm)],[t60137,t15]) ).
cnf(t17388,plain,
meet(X1,meet(X2,meet(X3,join(X4,join(Y4,meet(X1,X2)))))) = meet(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t60138]) ).
cnf(t17389,plain,
meet(X1,meet(X2,join(X1,X3))) = meet(X1,meet(X2,join(X4,join(Y4,meet(X1,X2))))),
inference(cp,[status(thm)],[t17388,t12055]) ).
cnf(t60139,plain,
meet(X1,X2) = meet(X1,meet(X2,join(X4,join(Y4,meet(X1,X2))))),
inference(step,[status(thm)],[t17389,t92]) ).
cnf(t17607,plain,
meet(X1,meet(X2,join(X3,join(X4,meet(X1,X2))))) = meet(X1,X2),
inference(orient,[status(thm)],[t60139]) ).
cnf(t17757,plain,
meet(X1,meet(X2,join(X3,join(X4,meet(X2,join(X1,Y4)))))) = meet(X1,meet(X2,join(X1,Y4))),
inference(cp,[status(thm)],[t12055,t17607]) ).
cnf(t60140,plain,
meet(X1,meet(X2,join(X3,join(X4,meet(X2,join(X1,Y4)))))) = meet(X1,X2),
inference(step,[status(thm)],[t17757,t92]) ).
cnf(t17814,plain,
meet(X1,meet(X2,join(X3,join(X4,meet(X2,join(X1,Y4)))))) = meet(X1,X2),
inference(orient,[status(thm)],[t60140]) ).
cnf(t35039,plain,
join(X1,X2) = join(join(X1,X2),meet(X3,join(X1,X2))),
inference(cp,[status(thm)],[t35025,t17814]) ).
cnf(t35417,plain,
join(join(X1,X2),meet(X3,join(X1,X2))) = join(X1,X2),
inference(orient,[status(thm)],[t35039]) ).
cnf(t10419,plain,
meet(X1,meet(meet(X2,X3),join(X2,X4))) = meet(meet(X1,meet(X2,X3)),join(Y4,meet(X1,join(X2,X4)))),
inference(cp,[status(thm)],[t10311,t3126]) ).
cnf(t60117,plain,
meet(X1,meet(X2,X3)) = meet(meet(X1,meet(X2,X3)),join(Y4,meet(X1,join(X2,X4)))),
inference(step,[status(thm)],[t10419,t3126]) ).
cnf(t16650,plain,
meet(meet(X1,meet(X2,X3)),join(X4,meet(X1,join(X2,Y4)))) = meet(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t60117]) ).
cnf(t9073,plain,
meet(X1,meet(join(meet(X2,X3),meet(X2,join(X1,X4))),Y4)) = meet(Y4,meet(X1,X2)),
inference(cp,[status(thm)],[t15,t8935]) ).
cnf(t60096,plain,
meet(X1,meet(Y4,join(meet(X2,X3),meet(X2,join(X1,X4))))) = meet(Y4,meet(X1,X2)),
inference(step,[status(thm)],[t9073,t13]) ).
cnf(t60097,plain,
meet(X1,meet(Y4,join(meet(X2,X3),meet(X2,join(X1,X4))))) = meet(X2,meet(Y4,X1)),
inference(step,[status(thm)],[t60096,t15]) ).
cnf(t60098,plain,
meet(X1,meet(Y4,join(meet(X2,X3),meet(X2,join(X1,X4))))) = meet(X1,meet(X2,Y4)),
inference(step,[status(thm)],[t60097,t15]) ).
cnf(t14835,plain,
meet(X1,meet(X2,join(meet(X3,X4),meet(X3,join(X1,Y4))))) = meet(X1,meet(X3,X2)),
inference(orient,[status(thm)],[t60098]) ).
cnf(t16657,plain,
meet(X1,meet(X2,join(meet(X3,X4),meet(X3,join(X1,Y4))))) = meet(meet(X1,meet(X3,X2)),join(Y5,meet(X1,join(X2,Y6)))),
inference(cp,[status(thm)],[t16650,t14835]) ).
cnf(t60156,plain,
meet(X1,meet(X3,X2)) = meet(meet(X1,meet(X3,X2)),join(Y5,meet(X1,join(X2,Y6)))),
inference(step,[status(thm)],[t16657,t14835]) ).
cnf(t19758,plain,
meet(meet(X1,meet(X2,X3)),join(X4,meet(X1,join(X3,Y4)))) = meet(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t60156]) ).
cnf(t9079,plain,
meet(X1,meet(X2,X3)) = meet(meet(X1,X2),join(meet(X1,X3),X3)),
inference(cp,[status(thm)],[t9075,t114]) ).
cnf(t60019,plain,
meet(X1,meet(X2,X3)) = meet(meet(X1,X2),join(X3,meet(X1,X3))),
inference(step,[status(thm)],[t9079,t48]) ).
cnf(t9599,plain,
meet(meet(X1,X2),join(X3,meet(X1,X3))) = meet(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t60019]) ).
cnf(t19759,plain,
meet(X1,meet(X2,X3)) = meet(X1,meet(meet(X2,X3),join(X3,X4))),
inference(cp,[status(thm)],[t19758,t9599]) ).
cnf(t20110,plain,
meet(X1,meet(meet(X2,X3),join(X3,X4))) = meet(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t19759]) ).
cnf(t20116,plain,
meet(meet(X1,X2),meet(X1,X2)) = meet(meet(X1,X2),join(X2,X3)),
inference(cp,[status(thm)],[t20110,t73]) ).
cnf(t60158,plain,
meet(X1,X2) = meet(meet(X1,X2),join(X2,X3)),
inference(step,[status(thm)],[t20116,t9]) ).
cnf(t20337,plain,
meet(meet(X1,X2),join(X2,X3)) = meet(X1,X2),
inference(orient,[status(thm)],[t60158]) ).
cnf(t20428,plain,
meet(X1,meet(X2,join(X1,X3))) = meet(meet(X1,X2),join(meet(X2,join(X1,X3)),X4)),
inference(cp,[status(thm)],[t20337,t92]) ).
cnf(t60159,plain,
meet(X1,X2) = meet(meet(X1,X2),join(meet(X2,join(X1,X3)),X4)),
inference(step,[status(thm)],[t20428,t92]) ).
cnf(t60160,plain,
meet(X1,X2) = meet(meet(X1,X2),join(X4,meet(X2,join(X1,X3)))),
inference(step,[status(thm)],[t60159,t48]) ).
cnf(t20587,plain,
meet(meet(X1,X2),join(X3,meet(X2,join(X1,X4)))) = meet(X1,X2),
inference(orient,[status(thm)],[t60160]) ).
cnf(t35501,plain,
join(X1,meet(X2,join(X3,X4))) = join(join(X1,meet(X2,join(X3,X4))),meet(X3,X2)),
inference(cp,[status(thm)],[t35417,t20587]) ).
cnf(t60274,plain,
join(X1,meet(X2,join(X3,X4))) = join(meet(X3,X2),join(X1,meet(X2,join(X3,X4)))),
inference(step,[status(thm)],[t35501,t48]) ).
cnf(t60275,plain,
join(X1,meet(X2,join(X3,X4))) = join(X1,join(meet(X2,join(X3,X4)),meet(X3,X2))),
inference(step,[status(thm)],[t60274,t52]) ).
cnf(t60276,plain,
join(X1,meet(X2,join(X3,X4))) = join(X1,join(meet(X3,X2),meet(X2,join(X3,X4)))),
inference(step,[status(thm)],[t60275,t48]) ).
cnf(t60277,plain,
join(X1,meet(X2,join(X3,X4))) = join(X1,join(meet(X2,X3),meet(X2,join(X3,X4)))),
inference(step,[status(thm)],[t60276,t13]) ).
cnf(t38201,plain,
join(X1,join(meet(X2,X3),meet(X2,join(X3,X4)))) = join(X1,meet(X2,join(X3,X4))),
inference(orient,[status(thm)],[t60277]) ).
cnf(t38428,plain,
meet(X1,join(X2,meet(X3,join(X1,X1)))) = meet(X1,join(X2,meet(X3,join(X1,X2)))),
inference(cp,[status(thm)],[t33,t38201]) ).
cnf(t60282,plain,
meet(X1,join(X2,meet(X3,X1))) = meet(X1,join(X2,meet(X3,join(X1,X2)))),
inference(step,[status(thm)],[t38428,t11]) ).
cnf(t60283,plain,
meet(X1,join(X2,meet(X1,X3))) = meet(X1,join(X2,meet(X3,join(X1,X2)))),
inference(step,[status(thm)],[t60282,t13]) ).
cnf(t38748,plain,
meet(X1,join(X2,meet(X3,join(X1,X2)))) = meet(X1,join(X2,meet(X1,X3))),
inference(orient,[status(thm)],[t60283]) ).
cnf(t20745,plain,
meet(X1,meet(X2,X3)) = meet(meet(X1,meet(X2,X3)),join(X4,meet(X2,X3))),
inference(cp,[status(thm)],[t20587,t19437]) ).
cnf(t20876,plain,
meet(meet(X1,meet(X2,X3)),join(X4,meet(X2,X3))) = meet(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t20745]) ).
cnf(t20945,plain,
meet(X1,meet(join(X2,X3),join(X2,join(X3,X4)))) = meet(meet(X1,join(X2,X3)),join(Y4,meet(join(X2,X3),join(X2,join(X3,X4))))),
inference(cp,[status(thm)],[t20876,t573]) ).
cnf(t60161,plain,
meet(X1,join(X2,X3)) = meet(meet(X1,join(X2,X3)),join(Y4,meet(join(X2,X3),join(X2,join(X3,X4))))),
inference(step,[status(thm)],[t20945,t573]) ).
cnf(t60162,plain,
meet(X1,join(X2,X3)) = meet(meet(X1,join(X2,X3)),join(Y4,join(X2,X3))),
inference(step,[status(thm)],[t60161,t573]) ).
cnf(t60163,plain,
meet(X1,join(X2,X3)) = meet(meet(X1,join(X2,X3)),join(X3,join(Y4,X2))),
inference(step,[status(thm)],[t60162,t52]) ).
cnf(t60164,plain,
meet(X1,join(X2,X3)) = meet(meet(X1,join(X2,X3)),join(X2,join(X3,Y4))),
inference(step,[status(thm)],[t60163,t52]) ).
cnf(t21084,plain,
meet(meet(X1,join(X2,X3)),join(X2,join(X3,X4))) = meet(X1,join(X2,X3)),
inference(orient,[status(thm)],[t60164]) ).
cnf(t38818,plain,
meet(X1,join(join(X2,X3),meet(X1,meet(X4,join(X1,X2))))) = meet(X1,join(join(X2,X3),meet(X4,join(X1,X2)))),
inference(cp,[status(thm)],[t38748,t21084]) ).
cnf(t60407,plain,
meet(X1,join(join(X2,X3),meet(X1,X4))) = meet(X1,join(join(X2,X3),meet(X4,join(X1,X2)))),
inference(step,[status(thm)],[t38818,t92]) ).
cnf(t60408,plain,
meet(X1,join(meet(X1,X4),join(X2,X3))) = meet(X1,join(join(X2,X3),meet(X4,join(X1,X2)))),
inference(step,[status(thm)],[t60407,t48]) ).
cnf(t60409,plain,
meet(X1,join(X3,join(meet(X1,X4),X2))) = meet(X1,join(join(X2,X3),meet(X4,join(X1,X2)))),
inference(step,[status(thm)],[t60408,t52]) ).
cnf(t60410,plain,
meet(X1,join(X2,join(X3,meet(X1,X4)))) = meet(X1,join(join(X2,X3),meet(X4,join(X1,X2)))),
inference(step,[status(thm)],[t60409,t52]) ).
cnf(t54870,plain,
meet(X1,join(join(X2,X3),meet(X4,join(X1,X2)))) = meet(X1,join(X2,join(X3,meet(X1,X4)))),
inference(orient,[status(thm)],[t60410]) ).
cnf(t54887,plain,
meet(X1,join(X2,join(X3,meet(X1,X4)))) = meet(X1,join(meet(X4,join(X1,X2)),join(X2,X3))),
inference(cp,[status(thm)],[t54870,t48]) ).
cnf(t60436,plain,
meet(X1,join(X2,join(X3,meet(X1,X4)))) = meet(X1,join(X3,join(meet(X4,join(X1,X2)),X2))),
inference(step,[status(thm)],[t54887,t52]) ).
cnf(t60437,plain,
meet(X1,join(X2,join(X3,meet(X1,X4)))) = meet(X1,join(X2,join(X3,meet(X4,join(X1,X2))))),
inference(step,[status(thm)],[t60436,t52]) ).
cnf(t58061,plain,
meet(X1,join(X2,join(X3,meet(X4,join(X1,X2))))) = meet(X1,join(X2,join(X3,meet(X1,X4)))),
inference(orient,[status(thm)],[t60437]) ).
cnf(t58390,plain,
meet(X1,meet(X1,join(X2,meet(X3,join(X1,X4))))) = meet(X1,meet(X1,join(X2,join(meet(X3,X4),meet(X1,X3))))),
inference(cp,[status(thm)],[t16163,t58061]) ).
cnf(t60445,plain,
meet(X1,join(X2,meet(X3,join(X1,X4)))) = meet(X1,meet(X1,join(X2,join(meet(X3,X4),meet(X1,X3))))),
inference(step,[status(thm)],[t58390,t73]) ).
cnf(t60446,plain,
meet(X1,join(X2,meet(X3,join(X1,X4)))) = meet(X1,join(X2,join(meet(X3,X4),meet(X1,X3)))),
inference(step,[status(thm)],[t60445,t73]) ).
cnf(t60447,plain,
meet(X1,join(X2,meet(X3,join(X1,X4)))) = meet(X1,join(X2,join(meet(X1,X3),meet(X3,X4)))),
inference(step,[status(thm)],[t60446,t48]) ).
cnf(t59108,plain,
meet(X1,join(X2,join(meet(X1,X3),meet(X3,X4)))) = meet(X1,join(X2,meet(X3,join(X1,X4)))),
inference(orient,[status(thm)],[t60447]) ).
cnf(goal_0,negated_conjecture,
meet(a,join(b,join(meet(a,c),meet(c,d)))) != meet(a,join(b,meet(c,join(a,d)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
meet(a,join(b,meet(c,join(a,d)))) != meet(a,join(b,meet(c,join(a,d)))),
inference(rw,[status(thm)],[goal_0,t59108]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT160-1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.10/0.36 % Computer : n020.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Wed Sep 23 20:25:33 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 35.74/5.07 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 35.74/5.07 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------