%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : LAT159-1 : TPTP v9.3.1. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n013.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 198.54s 27.78s
% Output : CNFRefutation 198.54s
% Verified :
% SZS Type : Refutation
% Derivation depth : 64
% Number of leaves : 20
% Syntax : Number of clauses : 535 ( 535 unt; 0 nHn; 336 RR)
% Number of literals : 535 ( 534 equ; 16 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 : 15 ( 15 usr; 13 con; 0-2 aty)
% Number of variables : 300 ( 76 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t4,axiom,
meet(X1,X2) = meet(X2,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t23,plain,
meet(X1,X2) = meet(X2,X1),
inference(orient,[status(thm)],[t4]) ).
cnf(t9,axiom,
sFlat0 = meet(a,b),
introduced(definition) ).
cnf(t68105,plain,
sFlat0 = meet(b,a),
inference(step,[status(thm)],[t9,t23]) ).
cnf(t54,plain,
meet(b,a) = sFlat0,
inference(orient,[status(thm)],[t68105]) ).
cnf(t2,axiom,
join(X1,X2) = join(X2,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t66,plain,
join(X1,X2) = join(X2,X1),
inference(orient,[status(thm)],[t2]) ).
cnf(t10,axiom,
sFlat1 = join(a,b),
introduced(definition) ).
cnf(t68112,plain,
sFlat1 = join(b,a),
inference(step,[status(thm)],[t10,t66]) ).
cnf(t85,plain,
join(b,a) = sFlat1,
inference(orient,[status(thm)],[t68112]) ).
cnf(t11,axiom,
sFlat2 = meet(c,join(a,b)),
introduced(definition) ).
cnf(t62,plain,
meet(c,join(a,b)) = sFlat2,
inference(orient,[status(thm)],[t11]) ).
cnf(t67,plain,
meet(c,join(a,b)) = sFlat2,
inference(rw,[status(thm)],[t62]) ).
cnf(t68134,plain,
meet(c,join(b,a)) = sFlat2,
inference(step,[status(thm)],[t67,t66]) ).
cnf(t68135,plain,
meet(c,sFlat1) = sFlat2,
inference(step,[status(thm)],[t68134,t85]) ).
cnf(t68136,plain,
meet(sFlat1,c) = sFlat2,
inference(step,[status(thm)],[t68135,t23]) ).
cnf(t164,plain,
meet(sFlat1,c) = sFlat2,
inference(orient,[status(thm)],[t68136]) ).
cnf(t12,axiom,
sFlat3 = join(meet(a,b),meet(c,join(a,b))),
introduced(definition) ).
cnf(t68109,plain,
sFlat3 = join(meet(b,a),meet(c,join(a,b))),
inference(step,[status(thm)],[t12,t23]) ).
cnf(t68110,plain,
sFlat3 = join(sFlat0,meet(c,join(a,b))),
inference(step,[status(thm)],[t68109,t54]) ).
cnf(t68111,plain,
sFlat3 = join(sFlat0,meet(c,join(b,a))),
inference(step,[status(thm)],[t68110,t66]) ).
cnf(t80,plain,
join(sFlat0,meet(c,join(b,a))) = sFlat3,
inference(orient,[status(thm)],[t68111]) ).
cnf(t68113,plain,
join(sFlat0,meet(c,sFlat1)) = sFlat3,
inference(step,[status(thm)],[t80,t85]) ).
cnf(t89,plain,
join(sFlat0,meet(c,sFlat1)) = sFlat3,
inference(rw,[status(thm)],[t68113]) ).
cnf(t68141,plain,
join(sFlat0,meet(sFlat1,c)) = sFlat3,
inference(step,[status(thm)],[t89,t23]) ).
cnf(t68142,plain,
join(sFlat0,sFlat2) = sFlat3,
inference(step,[status(thm)],[t68141,t164]) ).
cnf(t186,plain,
join(sFlat0,sFlat2) = sFlat3,
inference(orient,[status(thm)],[t68142]) ).
cnf(t7,axiom,
meet(meet(X1,X2),X3) = meet(X1,meet(X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t24,plain,
meet(meet(X1,X2),X3) = meet(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t7]) ).
cnf(t13,axiom,
sFlat4 = meet(a,join(meet(a,b),meet(c,join(a,b)))),
introduced(definition) ).
cnf(t68101,plain,
sFlat4 = meet(a,join(meet(b,a),meet(c,join(a,b)))),
inference(step,[status(thm)],[t13,t23]) ).
cnf(t42,plain,
meet(a,join(meet(b,a),meet(c,join(a,b)))) = sFlat4,
inference(orient,[status(thm)],[t68101]) ).
cnf(t43,plain,
meet(a,meet(join(meet(b,a),meet(c,join(a,b))),X1)) = meet(sFlat4,X1),
inference(cp,[status(thm)],[t24,t42]) ).
cnf(t68549,plain,
meet(a,meet(join(sFlat0,meet(c,join(a,b))),X1)) = meet(sFlat4,X1),
inference(step,[status(thm)],[t43,t54]) ).
cnf(t68550,plain,
meet(a,meet(join(sFlat0,meet(c,join(b,a))),X1)) = meet(sFlat4,X1),
inference(step,[status(thm)],[t68549,t66]) ).
cnf(t68551,plain,
meet(a,meet(join(sFlat0,meet(c,sFlat1)),X1)) = meet(sFlat4,X1),
inference(step,[status(thm)],[t68550,t85]) ).
cnf(t68552,plain,
meet(a,meet(join(sFlat0,meet(sFlat1,c)),X1)) = meet(sFlat4,X1),
inference(step,[status(thm)],[t68551,t23]) ).
cnf(t68553,plain,
meet(a,meet(join(sFlat0,sFlat2),X1)) = meet(sFlat4,X1),
inference(step,[status(thm)],[t68552,t164]) ).
cnf(t68554,plain,
meet(a,meet(sFlat3,X1)) = meet(sFlat4,X1),
inference(step,[status(thm)],[t68553,t186]) ).
cnf(t30,plain,
meet(X1,meet(X2,X3)) = meet(meet(X2,X1),X3),
inference(cp,[status(thm)],[t24,t23]) ).
cnf(t68154,plain,
meet(X1,meet(X2,X3)) = meet(X2,meet(X1,X3)),
inference(step,[status(thm)],[t30,t24]) ).
cnf(t315,plain,
meet(X1,meet(X2,X3)) = meet(X2,meet(X1,X3)),
inference(orient,[status(thm)],[t68154]) ).
cnf(t68555,plain,
meet(sFlat3,meet(a,X1)) = meet(sFlat4,X1),
inference(step,[status(thm)],[t68554,t315]) ).
cnf(t8483,plain,
meet(sFlat3,meet(a,X1)) = meet(sFlat4,X1),
inference(orient,[status(thm)],[t68555]) ).
cnf(t1,axiom,
meet(X1,X1) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t19,plain,
meet(X1,X1) = X1,
inference(orient,[status(thm)],[t1]) ).
cnf(t8502,plain,
meet(sFlat4,a) = meet(sFlat3,a),
inference(cp,[status(thm)],[t8483,t19]) ).
cnf(t5,axiom,
meet(X1,join(X1,X2)) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t20,plain,
meet(X1,join(X1,X2)) = X1,
inference(orient,[status(thm)],[t5]) ).
cnf(t3,axiom,
join(X1,meet(X1,X2)) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t22,plain,
join(X1,meet(X1,X2)) = X1,
inference(orient,[status(thm)],[t3]) ).
cnf(t44,plain,
a = join(a,sFlat4),
inference(cp,[status(thm)],[t22,t42]) ).
cnf(t68122,plain,
a = join(sFlat4,a),
inference(step,[status(thm)],[t44,t66]) ).
cnf(t99,plain,
join(sFlat4,a) = a,
inference(orient,[status(thm)],[t68122]) ).
cnf(t100,plain,
sFlat4 = meet(sFlat4,a),
inference(cp,[status(thm)],[t20,t99]) ).
cnf(t133,plain,
meet(sFlat4,a) = sFlat4,
inference(orient,[status(thm)],[t100]) ).
cnf(t68559,plain,
sFlat4 = meet(sFlat3,a),
inference(step,[status(thm)],[t8502,t133]) ).
cnf(t8552,plain,
meet(sFlat3,a) = sFlat4,
inference(orient,[status(thm)],[t68559]) ).
cnf(t14,axiom,
sFlat5 = join(b,meet(a,join(meet(a,b),meet(c,join(a,b))))),
introduced(definition) ).
cnf(t68114,plain,
sFlat5 = join(b,meet(a,join(meet(b,a),meet(c,join(a,b))))),
inference(step,[status(thm)],[t14,t23]) ).
cnf(t68115,plain,
sFlat5 = join(b,meet(a,join(sFlat0,meet(c,join(a,b))))),
inference(step,[status(thm)],[t68114,t54]) ).
cnf(t68116,plain,
sFlat5 = join(b,meet(a,join(sFlat0,meet(c,join(b,a))))),
inference(step,[status(thm)],[t68115,t66]) ).
cnf(t68117,plain,
sFlat5 = join(b,meet(a,join(sFlat0,meet(c,sFlat1)))),
inference(step,[status(thm)],[t68116,t85]) ).
cnf(t68118,plain,
sFlat5 = join(b,meet(a,join(sFlat0,meet(sFlat1,c)))),
inference(step,[status(thm)],[t68117,t23]) ).
cnf(t90,plain,
join(b,meet(a,join(sFlat0,meet(sFlat1,c)))) = sFlat5,
inference(orient,[status(thm)],[t68118]) ).
cnf(t68137,plain,
join(b,meet(a,join(sFlat0,sFlat2))) = sFlat5,
inference(step,[status(thm)],[t90,t164]) ).
cnf(t168,plain,
join(b,meet(a,join(sFlat0,sFlat2))) = sFlat5,
inference(rw,[status(thm)],[t68137]) ).
cnf(t68352,plain,
join(b,meet(a,sFlat3)) = sFlat5,
inference(step,[status(thm)],[t168,t186]) ).
cnf(t68353,plain,
join(b,meet(sFlat3,a)) = sFlat5,
inference(step,[status(thm)],[t68352,t23]) ).
cnf(t3069,plain,
join(b,meet(sFlat3,a)) = sFlat5,
inference(orient,[status(thm)],[t68353]) ).
cnf(t68566,plain,
join(b,sFlat4) = sFlat5,
inference(step,[status(thm)],[t3069,t8552]) ).
cnf(t8573,plain,
join(b,sFlat4) = sFlat5,
inference(rw,[status(thm)],[t68566]) ).
cnf(t68583,plain,
join(sFlat4,b) = sFlat5,
inference(step,[status(thm)],[t8573,t66]) ).
cnf(t8667,plain,
join(sFlat4,b) = sFlat5,
inference(orient,[status(thm)],[t68583]) ).
cnf(t16,axiom,
sFlat7 = meet(a,c),
introduced(definition) ).
cnf(t68107,plain,
sFlat7 = meet(c,a),
inference(step,[status(thm)],[t16,t23]) ).
cnf(t58,plain,
meet(c,a) = sFlat7,
inference(orient,[status(thm)],[t68107]) ).
cnf(t17,axiom,
sFlat8 = join(b,meet(a,c)),
introduced(definition) ).
cnf(t68119,plain,
sFlat8 = join(b,meet(c,a)),
inference(step,[status(thm)],[t17,t23]) ).
cnf(t68120,plain,
sFlat8 = join(b,sFlat7),
inference(step,[status(thm)],[t68119,t58]) ).
cnf(t68121,plain,
sFlat8 = join(sFlat7,b),
inference(step,[status(thm)],[t68120,t66]) ).
cnf(t95,plain,
join(sFlat7,b) = sFlat8,
inference(orient,[status(thm)],[t68121]) ).
cnf(t18,axiom,
sFlat9 = meet(a,join(b,meet(a,c))),
introduced(definition) ).
cnf(t68104,plain,
sFlat9 = meet(a,join(b,meet(c,a))),
inference(step,[status(thm)],[t18,t23]) ).
cnf(t50,plain,
meet(a,join(b,meet(c,a))) = sFlat9,
inference(orient,[status(thm)],[t68104]) ).
cnf(t68108,plain,
meet(a,join(b,sFlat7)) = sFlat9,
inference(step,[status(thm)],[t50,t58]) ).
cnf(t61,plain,
meet(a,join(b,sFlat7)) = sFlat9,
inference(rw,[status(thm)],[t68108]) ).
cnf(t68130,plain,
meet(a,join(sFlat7,b)) = sFlat9,
inference(step,[status(thm)],[t61,t66]) ).
cnf(t68131,plain,
meet(a,sFlat8) = sFlat9,
inference(step,[status(thm)],[t68130,t95]) ).
cnf(t68132,plain,
meet(sFlat8,a) = sFlat9,
inference(step,[status(thm)],[t68131,t23]) ).
cnf(t154,plain,
meet(sFlat8,a) = sFlat9,
inference(orient,[status(thm)],[t68132]) ).
cnf(t156,plain,
meet(sFlat8,meet(a,X1)) = meet(sFlat9,X1),
inference(cp,[status(thm)],[t24,t154]) ).
cnf(t374,plain,
meet(sFlat8,meet(a,X1)) = meet(sFlat9,X1),
inference(orient,[status(thm)],[t156]) ).
cnf(t378,plain,
sFlat8 = join(sFlat8,meet(sFlat9,X1)),
inference(cp,[status(thm)],[t22,t374]) ).
cnf(t635,plain,
join(sFlat8,meet(sFlat9,X1)) = sFlat8,
inference(orient,[status(thm)],[t378]) ).
cnf(t636,plain,
sFlat8 = join(sFlat8,meet(X1,sFlat9)),
inference(cp,[status(thm)],[t635,t23]) ).
cnf(t848,plain,
join(sFlat8,meet(X1,sFlat9)) = sFlat8,
inference(orient,[status(thm)],[t636]) ).
cnf(t15,axiom,
sFlat6 = meet(a,join(b,meet(a,join(meet(a,b),meet(c,join(a,b)))))),
introduced(definition) ).
cnf(t68102,plain,
sFlat6 = meet(a,join(b,meet(a,join(meet(b,a),meet(c,join(a,b)))))),
inference(step,[status(thm)],[t15,t23]) ).
cnf(t68103,plain,
sFlat6 = meet(a,join(b,sFlat4)),
inference(step,[status(thm)],[t68102,t42]) ).
cnf(t46,plain,
meet(a,join(b,sFlat4)) = sFlat6,
inference(orient,[status(thm)],[t68103]) ).
cnf(t47,plain,
meet(a,meet(join(b,sFlat4),X1)) = meet(sFlat6,X1),
inference(cp,[status(thm)],[t24,t46]) ).
cnf(t68277,plain,
meet(a,meet(join(sFlat4,b),X1)) = meet(sFlat6,X1),
inference(step,[status(thm)],[t47,t66]) ).
cnf(t1817,plain,
meet(a,meet(join(sFlat4,b),X1)) = meet(sFlat6,X1),
inference(orient,[status(thm)],[t68277]) ).
cnf(t8495,plain,
meet(sFlat4,meet(join(sFlat4,b),X1)) = meet(sFlat3,meet(sFlat6,X1)),
inference(cp,[status(thm)],[t8483,t1817]) ).
cnf(t29,plain,
meet(X1,meet(join(X1,X2),X3)) = meet(X1,X3),
inference(cp,[status(thm)],[t24,t20]) ).
cnf(t695,plain,
meet(X1,meet(join(X1,X2),X3)) = meet(X1,X3),
inference(orient,[status(thm)],[t29]) ).
cnf(t68597,plain,
meet(sFlat4,X1) = meet(sFlat3,meet(sFlat6,X1)),
inference(step,[status(thm)],[t8495,t695]) ).
cnf(t8704,plain,
meet(sFlat3,meet(sFlat6,X1)) = meet(sFlat4,X1),
inference(orient,[status(thm)],[t68597]) ).
cnf(t8,axiom,
meet(X1,join(X2,meet(X3,join(X1,meet(X3,join(X2,X4)))))) = meet(X1,join(X2,meet(X3,join(X1,X4)))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t32,plain,
meet(X1,join(X2,meet(X3,join(X1,meet(X3,join(X2,X4)))))) = meet(X1,join(X2,meet(X3,join(X1,X4)))),
inference(orient,[status(thm)],[t8]) ).
cnf(t6,axiom,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t69,plain,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
inference(orient,[status(thm)],[t6]) ).
cnf(t97,plain,
join(sFlat7,join(b,X1)) = join(sFlat8,X1),
inference(cp,[status(thm)],[t69,t95]) ).
cnf(t237,plain,
join(sFlat7,join(b,X1)) = join(sFlat8,X1),
inference(orient,[status(thm)],[t97]) ).
cnf(t238,plain,
join(sFlat8,a) = join(sFlat7,sFlat1),
inference(cp,[status(thm)],[t237,t85]) ).
cnf(t68148,plain,
join(sFlat8,a) = join(sFlat1,sFlat7),
inference(step,[status(thm)],[t238,t66]) ).
cnf(t250,plain,
join(sFlat8,a) = join(sFlat1,sFlat7),
inference(orient,[status(thm)],[t68148]) ).
cnf(t254,plain,
meet(X1,join(sFlat8,meet(X2,join(X1,a)))) = meet(X1,join(sFlat8,meet(X2,join(X1,meet(X2,join(sFlat1,sFlat7)))))),
inference(cp,[status(thm)],[t32,t250]) ).
cnf(t59,plain,
meet(c,meet(a,X1)) = meet(sFlat7,X1),
inference(cp,[status(thm)],[t24,t58]) ).
cnf(t213,plain,
meet(c,meet(a,X1)) = meet(sFlat7,X1),
inference(orient,[status(thm)],[t59]) ).
cnf(t218,plain,
meet(sFlat7,join(a,X1)) = meet(c,a),
inference(cp,[status(thm)],[t213,t20]) ).
cnf(t68150,plain,
meet(sFlat7,join(a,X1)) = sFlat7,
inference(step,[status(thm)],[t218,t58]) ).
cnf(t265,plain,
meet(sFlat7,join(a,X1)) = sFlat7,
inference(orient,[status(thm)],[t68150]) ).
cnf(t266,plain,
sFlat7 = meet(sFlat7,join(X1,a)),
inference(cp,[status(thm)],[t265,t66]) ).
cnf(t532,plain,
meet(sFlat7,join(X1,a)) = sFlat7,
inference(orient,[status(thm)],[t266]) ).
cnf(t87,plain,
join(b,join(a,X1)) = join(sFlat1,X1),
inference(cp,[status(thm)],[t69,t85]) ).
cnf(t226,plain,
join(b,join(a,X1)) = join(sFlat1,X1),
inference(orient,[status(thm)],[t87]) ).
cnf(t0,axiom,
join(X1,X1) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t21,plain,
join(X1,X1) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t227,plain,
join(sFlat1,a) = join(b,a),
inference(cp,[status(thm)],[t226,t21]) ).
cnf(t68146,plain,
join(sFlat1,a) = sFlat1,
inference(step,[status(thm)],[t227,t85]) ).
cnf(t234,plain,
join(sFlat1,a) = sFlat1,
inference(orient,[status(thm)],[t68146]) ).
cnf(t534,plain,
sFlat7 = meet(sFlat7,sFlat1),
inference(cp,[status(thm)],[t532,t234]) ).
cnf(t68191,plain,
sFlat7 = meet(sFlat1,sFlat7),
inference(step,[status(thm)],[t534,t23]) ).
cnf(t539,plain,
meet(sFlat1,sFlat7) = sFlat7,
inference(orient,[status(thm)],[t68191]) ).
cnf(t540,plain,
sFlat1 = join(sFlat1,sFlat7),
inference(cp,[status(thm)],[t22,t539]) ).
cnf(t541,plain,
join(sFlat1,sFlat7) = sFlat1,
inference(orient,[status(thm)],[t540]) ).
cnf(t70162,plain,
meet(X1,join(sFlat8,meet(X2,join(X1,a)))) = meet(X1,join(sFlat8,meet(X2,join(X1,meet(X2,sFlat1))))),
inference(step,[status(thm)],[t254,t541]) ).
cnf(t67700,plain,
meet(X1,join(sFlat8,meet(X2,join(X1,meet(X2,sFlat1))))) = meet(X1,join(sFlat8,meet(X2,join(X1,a)))),
inference(orient,[status(thm)],[t70162]) ).
cnf(t67744,plain,
meet(sFlat4,join(sFlat8,meet(X1,join(sFlat6,meet(X1,sFlat1))))) = meet(sFlat3,meet(sFlat6,join(sFlat8,meet(X1,join(sFlat6,a))))),
inference(cp,[status(thm)],[t8704,t67700]) ).
cnf(t26,plain,
meet(X1,meet(X2,join(meet(X1,X2),X3))) = meet(X1,X2),
inference(cp,[status(thm)],[t24,t20]) ).
cnf(t421,plain,
meet(X1,meet(X2,join(meet(X1,X2),X3))) = meet(X1,X2),
inference(orient,[status(thm)],[t26]) ).
cnf(t425,plain,
meet(X1,X2) = meet(X1,meet(X2,join(X3,meet(X1,X2)))),
inference(cp,[status(thm)],[t421,t66]) ).
cnf(t12958,plain,
meet(X1,meet(X2,join(X3,meet(X1,X2)))) = meet(X1,X2),
inference(orient,[status(thm)],[t425]) ).
cnf(t72,plain,
join(X1,join(X2,X3)) = join(X3,join(X1,X2)),
inference(cp,[status(thm)],[t69,t66]) ).
cnf(t320,plain,
join(X1,join(X2,X3)) = join(X3,join(X1,X2)),
inference(orient,[status(thm)],[t72]) ).
cnf(t325,plain,
X1 = meet(X1,join(X2,join(X3,X1))),
inference(cp,[status(thm)],[t20,t320]) ).
cnf(t1270,plain,
meet(X1,join(X2,join(X3,X1))) = X1,
inference(orient,[status(thm)],[t325]) ).
cnf(t73,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(cp,[status(thm)],[t69,t21]) ).
cnf(t178,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(orient,[status(thm)],[t73]) ).
cnf(t1272,plain,
X1 = meet(X1,join(X2,X1)),
inference(cp,[status(thm)],[t1270,t178]) ).
cnf(t1389,plain,
meet(X1,join(X2,X1)) = X1,
inference(orient,[status(thm)],[t1272]) ).
cnf(t229,plain,
join(sFlat1,meet(a,X1)) = join(b,a),
inference(cp,[status(thm)],[t226,t22]) ).
cnf(t68151,plain,
join(sFlat1,meet(a,X1)) = sFlat1,
inference(step,[status(thm)],[t229,t85]) ).
cnf(t274,plain,
join(sFlat1,meet(a,X1)) = sFlat1,
inference(orient,[status(thm)],[t68151]) ).
cnf(t68,plain,
meet(a,join(b,sFlat4)) = sFlat6,
inference(rw,[status(thm)],[t46]) ).
cnf(t68139,plain,
meet(a,join(sFlat4,b)) = sFlat6,
inference(step,[status(thm)],[t68,t66]) ).
cnf(t175,plain,
meet(a,join(sFlat4,b)) = sFlat6,
inference(orient,[status(thm)],[t68139]) ).
cnf(t275,plain,
sFlat1 = join(sFlat1,sFlat6),
inference(cp,[status(thm)],[t274,t175]) ).
cnf(t280,plain,
join(sFlat1,sFlat6) = sFlat1,
inference(orient,[status(thm)],[t275]) ).
cnf(t281,plain,
join(sFlat1,join(sFlat6,X1)) = join(sFlat1,X1),
inference(cp,[status(thm)],[t69,t280]) ).
cnf(t975,plain,
join(sFlat1,join(sFlat6,X1)) = join(sFlat1,X1),
inference(orient,[status(thm)],[t281]) ).
cnf(t1406,plain,
join(sFlat6,X1) = meet(join(sFlat6,X1),join(sFlat1,X1)),
inference(cp,[status(thm)],[t1389,t975]) ).
cnf(t68775,plain,
join(sFlat6,X1) = meet(join(sFlat1,X1),join(sFlat6,X1)),
inference(step,[status(thm)],[t1406,t23]) ).
cnf(t10644,plain,
meet(join(sFlat1,X1),join(sFlat6,X1)) = join(sFlat6,X1),
inference(orient,[status(thm)],[t68775]) ).
cnf(t27,plain,
meet(X1,meet(X2,X3)) = meet(X3,meet(X1,X2)),
inference(cp,[status(thm)],[t24,t23]) ).
cnf(t305,plain,
meet(X1,meet(X2,X3)) = meet(X3,meet(X1,X2)),
inference(orient,[status(thm)],[t27]) ).
cnf(t314,plain,
X1 = join(X1,meet(X2,meet(X3,X1))),
inference(cp,[status(thm)],[t22,t305]) ).
cnf(t1041,plain,
join(X1,meet(X2,meet(X3,X1))) = X1,
inference(orient,[status(thm)],[t314]) ).
cnf(t28,plain,
meet(X1,meet(X1,X2)) = meet(X1,X2),
inference(cp,[status(thm)],[t24,t19]) ).
cnf(t151,plain,
meet(X1,meet(X1,X2)) = meet(X1,X2),
inference(orient,[status(thm)],[t28]) ).
cnf(t1043,plain,
X1 = join(X1,meet(X2,X1)),
inference(cp,[status(thm)],[t1041,t151]) ).
cnf(t1142,plain,
join(X1,meet(X2,X1)) = X1,
inference(orient,[status(thm)],[t1043]) ).
cnf(t10686,plain,
join(sFlat6,meet(X1,sFlat1)) = meet(sFlat1,join(sFlat6,meet(X1,sFlat1))),
inference(cp,[status(thm)],[t10644,t1142]) ).
cnf(t62479,plain,
meet(sFlat1,join(sFlat6,meet(X1,sFlat1))) = join(sFlat6,meet(X1,sFlat1)),
inference(orient,[status(thm)],[t10686]) ).
cnf(t62489,plain,
meet(X1,sFlat1) = meet(X1,join(sFlat6,meet(X1,sFlat1))),
inference(cp,[status(thm)],[t12958,t62479]) ).
cnf(t62497,plain,
meet(X1,join(sFlat6,meet(X1,sFlat1))) = meet(X1,sFlat1),
inference(orient,[status(thm)],[t62489]) ).
cnf(t70163,plain,
meet(sFlat4,join(sFlat8,meet(X1,sFlat1))) = meet(sFlat3,meet(sFlat6,join(sFlat8,meet(X1,join(sFlat6,a))))),
inference(step,[status(thm)],[t67744,t62497]) ).
cnf(t70164,plain,
meet(sFlat4,join(sFlat8,meet(X1,sFlat1))) = meet(sFlat4,join(sFlat8,meet(X1,join(sFlat6,a)))),
inference(step,[status(thm)],[t70163,t8704]) ).
cnf(t48,plain,
a = join(a,sFlat6),
inference(cp,[status(thm)],[t22,t46]) ).
cnf(t68123,plain,
a = join(sFlat6,a),
inference(step,[status(thm)],[t48,t66]) ).
cnf(t103,plain,
join(sFlat6,a) = a,
inference(orient,[status(thm)],[t68123]) ).
cnf(t70165,plain,
meet(sFlat4,join(sFlat8,meet(X1,sFlat1))) = meet(sFlat4,join(sFlat8,meet(X1,a))),
inference(step,[status(thm)],[t70164,t103]) ).
cnf(t67829,plain,
meet(sFlat4,join(sFlat8,meet(X1,a))) = meet(sFlat4,join(sFlat8,meet(X1,sFlat1))),
inference(orient,[status(thm)],[t70165]) ).
cnf(t64,plain,
c = join(c,sFlat2),
inference(cp,[status(thm)],[t22,t62]) ).
cnf(t68127,plain,
c = join(sFlat2,c),
inference(step,[status(thm)],[t64,t66]) ).
cnf(t119,plain,
join(sFlat2,c) = c,
inference(orient,[status(thm)],[t68127]) ).
cnf(t120,plain,
sFlat2 = meet(sFlat2,c),
inference(cp,[status(thm)],[t20,t119]) ).
cnf(t143,plain,
meet(sFlat2,c) = sFlat2,
inference(orient,[status(thm)],[t120]) ).
cnf(t144,plain,
meet(sFlat2,meet(c,X1)) = meet(sFlat2,X1),
inference(cp,[status(thm)],[t24,t143]) ).
cnf(t689,plain,
meet(sFlat2,meet(c,X1)) = meet(sFlat2,X1),
inference(orient,[status(thm)],[t144]) ).
cnf(t690,plain,
meet(sFlat2,a) = meet(sFlat2,sFlat7),
inference(cp,[status(thm)],[t689,t58]) ).
cnf(t708,plain,
meet(sFlat2,a) = meet(sFlat2,sFlat7),
inference(orient,[status(thm)],[t690]) ).
cnf(t166,plain,
meet(sFlat1,meet(c,X1)) = meet(sFlat2,X1),
inference(cp,[status(thm)],[t24,t164]) ).
cnf(t728,plain,
meet(sFlat1,meet(c,X1)) = meet(sFlat2,X1),
inference(orient,[status(thm)],[t166]) ).
cnf(t729,plain,
meet(sFlat2,a) = meet(sFlat1,sFlat7),
inference(cp,[status(thm)],[t728,t58]) ).
cnf(t68208,plain,
meet(sFlat2,sFlat7) = meet(sFlat1,sFlat7),
inference(step,[status(thm)],[t729,t708]) ).
cnf(t68209,plain,
meet(sFlat2,sFlat7) = sFlat7,
inference(step,[status(thm)],[t68208,t539]) ).
cnf(t735,plain,
meet(sFlat2,sFlat7) = sFlat7,
inference(orient,[status(thm)],[t68209]) ).
cnf(t68210,plain,
meet(sFlat2,a) = sFlat7,
inference(step,[status(thm)],[t708,t735]) ).
cnf(t736,plain,
meet(sFlat2,a) = sFlat7,
inference(orient,[status(thm)],[t68210]) ).
cnf(t67830,plain,
meet(sFlat4,join(sFlat8,meet(sFlat2,sFlat1))) = meet(sFlat4,join(sFlat8,sFlat7)),
inference(cp,[status(thm)],[t67829,t736]) ).
cnf(t70166,plain,
meet(sFlat4,join(sFlat8,meet(sFlat1,sFlat2))) = meet(sFlat4,join(sFlat8,sFlat7)),
inference(step,[status(thm)],[t67830,t23]) ).
cnf(t165,plain,
meet(sFlat1,c) = meet(sFlat1,sFlat2),
inference(cp,[status(thm)],[t151,t164]) ).
cnf(t68138,plain,
sFlat2 = meet(sFlat1,sFlat2),
inference(step,[status(thm)],[t165,t164]) ).
cnf(t169,plain,
meet(sFlat1,sFlat2) = sFlat2,
inference(orient,[status(thm)],[t68138]) ).
cnf(t70167,plain,
meet(sFlat4,join(sFlat8,sFlat2)) = meet(sFlat4,join(sFlat8,sFlat7)),
inference(step,[status(thm)],[t70166,t169]) ).
cnf(t70168,plain,
meet(sFlat4,join(sFlat2,sFlat8)) = meet(sFlat4,join(sFlat8,sFlat7)),
inference(step,[status(thm)],[t70167,t66]) ).
cnf(t31,plain,
meet(X1,X2) = join(meet(X1,X2),meet(X1,meet(X2,X3))),
inference(cp,[status(thm)],[t22,t24]) ).
cnf(t902,plain,
join(meet(X1,X2),meet(X1,meet(X2,X3))) = meet(X1,X2),
inference(orient,[status(thm)],[t31]) ).
cnf(t932,plain,
meet(X1,X2) = join(meet(X1,X2),meet(X2,meet(X3,X1))),
inference(cp,[status(thm)],[t902,t305]) ).
cnf(t13477,plain,
join(meet(X1,X2),meet(X2,meet(X3,X1))) = meet(X1,X2),
inference(orient,[status(thm)],[t932]) ).
cnf(t56,plain,
b = join(b,sFlat0),
inference(cp,[status(thm)],[t22,t54]) ).
cnf(t68125,plain,
b = join(sFlat0,b),
inference(step,[status(thm)],[t56,t66]) ).
cnf(t111,plain,
join(sFlat0,b) = b,
inference(orient,[status(thm)],[t68125]) ).
cnf(t113,plain,
join(sFlat0,join(b,X1)) = join(b,X1),
inference(cp,[status(thm)],[t69,t111]) ).
cnf(t345,plain,
join(sFlat0,join(b,X1)) = join(b,X1),
inference(orient,[status(thm)],[t113]) ).
cnf(t346,plain,
join(b,a) = join(sFlat0,sFlat1),
inference(cp,[status(thm)],[t345,t85]) ).
cnf(t68156,plain,
sFlat1 = join(sFlat0,sFlat1),
inference(step,[status(thm)],[t346,t85]) ).
cnf(t350,plain,
join(sFlat0,sFlat1) = sFlat1,
inference(orient,[status(thm)],[t68156]) ).
cnf(t351,plain,
sFlat0 = meet(sFlat0,sFlat1),
inference(cp,[status(thm)],[t20,t350]) ).
cnf(t353,plain,
meet(sFlat0,sFlat1) = sFlat0,
inference(orient,[status(thm)],[t351]) ).
cnf(t13792,plain,
meet(sFlat1,X1) = join(meet(sFlat1,X1),meet(X1,sFlat0)),
inference(cp,[status(thm)],[t13477,t353]) ).
cnf(t13957,plain,
join(meet(sFlat1,X1),meet(X1,sFlat0)) = meet(sFlat1,X1),
inference(orient,[status(thm)],[t13792]) ).
cnf(t13981,plain,
meet(sFlat1,X1) = join(meet(sFlat1,X1),meet(sFlat0,X1)),
inference(cp,[status(thm)],[t13957,t23]) ).
cnf(t68854,plain,
meet(sFlat1,X1) = join(meet(sFlat0,X1),meet(sFlat1,X1)),
inference(step,[status(thm)],[t13981,t66]) ).
cnf(t14950,plain,
join(meet(sFlat0,X1),meet(sFlat1,X1)) = meet(sFlat1,X1),
inference(orient,[status(thm)],[t68854]) ).
cnf(t167,plain,
sFlat1 = join(sFlat1,sFlat2),
inference(cp,[status(thm)],[t22,t164]) ).
cnf(t172,plain,
join(sFlat1,sFlat2) = sFlat1,
inference(orient,[status(thm)],[t167]) ).
cnf(t173,plain,
join(sFlat1,join(sFlat2,X1)) = join(sFlat1,X1),
inference(cp,[status(thm)],[t69,t172]) ).
cnf(t973,plain,
join(sFlat1,join(sFlat2,X1)) = join(sFlat1,X1),
inference(orient,[status(thm)],[t173]) ).
cnf(t1407,plain,
join(sFlat2,X1) = meet(join(sFlat2,X1),join(sFlat1,X1)),
inference(cp,[status(thm)],[t1389,t973]) ).
cnf(t68780,plain,
join(sFlat2,X1) = meet(join(sFlat1,X1),join(sFlat2,X1)),
inference(step,[status(thm)],[t1407,t23]) ).
cnf(t10744,plain,
meet(join(sFlat1,X1),join(sFlat2,X1)) = join(sFlat2,X1),
inference(orient,[status(thm)],[t68780]) ).
cnf(t241,plain,
join(sFlat8,join(b,X1)) = join(sFlat7,join(b,X1)),
inference(cp,[status(thm)],[t237,t178]) ).
cnf(t68184,plain,
join(sFlat8,join(b,X1)) = join(sFlat8,X1),
inference(step,[status(thm)],[t241,t237]) ).
cnf(t492,plain,
join(sFlat8,join(b,X1)) = join(sFlat8,X1),
inference(orient,[status(thm)],[t68184]) ).
cnf(t494,plain,
join(sFlat8,a) = join(sFlat8,sFlat1),
inference(cp,[status(thm)],[t492,t85]) ).
cnf(t68185,plain,
join(sFlat1,sFlat7) = join(sFlat8,sFlat1),
inference(step,[status(thm)],[t494,t250]) ).
cnf(t68186,plain,
join(sFlat1,sFlat7) = join(sFlat1,sFlat8),
inference(step,[status(thm)],[t68185,t66]) ).
cnf(t498,plain,
join(sFlat1,sFlat8) = join(sFlat1,sFlat7),
inference(orient,[status(thm)],[t68186]) ).
cnf(t68194,plain,
join(sFlat1,sFlat8) = sFlat1,
inference(step,[status(thm)],[t498,t541]) ).
cnf(t544,plain,
join(sFlat1,sFlat8) = sFlat1,
inference(orient,[status(thm)],[t68194]) ).
cnf(t10778,plain,
join(sFlat2,sFlat8) = meet(sFlat1,join(sFlat2,sFlat8)),
inference(cp,[status(thm)],[t10744,t544]) ).
cnf(t10819,plain,
meet(sFlat1,join(sFlat2,sFlat8)) = join(sFlat2,sFlat8),
inference(orient,[status(thm)],[t10778]) ).
cnf(t15013,plain,
meet(sFlat1,join(sFlat2,sFlat8)) = join(meet(sFlat0,join(sFlat2,sFlat8)),join(sFlat2,sFlat8)),
inference(cp,[status(thm)],[t14950,t10819]) ).
cnf(t68855,plain,
join(sFlat2,sFlat8) = join(meet(sFlat0,join(sFlat2,sFlat8)),join(sFlat2,sFlat8)),
inference(step,[status(thm)],[t15013,t10819]) ).
cnf(t112,plain,
sFlat0 = meet(sFlat0,b),
inference(cp,[status(thm)],[t20,t111]) ).
cnf(t139,plain,
meet(sFlat0,b) = sFlat0,
inference(orient,[status(thm)],[t112]) ).
cnf(t140,plain,
meet(sFlat0,meet(b,X1)) = meet(sFlat0,X1),
inference(cp,[status(thm)],[t24,t139]) ).
cnf(t681,plain,
meet(sFlat0,meet(b,X1)) = meet(sFlat0,X1),
inference(orient,[status(thm)],[t140]) ).
cnf(t240,plain,
join(sFlat8,b) = join(sFlat7,b),
inference(cp,[status(thm)],[t237,t21]) ).
cnf(t68147,plain,
join(sFlat8,b) = sFlat8,
inference(step,[status(thm)],[t240,t95]) ).
cnf(t247,plain,
join(sFlat8,b) = sFlat8,
inference(orient,[status(thm)],[t68147]) ).
cnf(t1299,plain,
b = meet(b,join(X1,sFlat8)),
inference(cp,[status(thm)],[t1270,t247]) ).
cnf(t1688,plain,
meet(b,join(X1,sFlat8)) = b,
inference(orient,[status(thm)],[t1299]) ).
cnf(t1691,plain,
meet(sFlat0,join(X1,sFlat8)) = meet(sFlat0,b),
inference(cp,[status(thm)],[t681,t1688]) ).
cnf(t68263,plain,
meet(sFlat0,join(X1,sFlat8)) = sFlat0,
inference(step,[status(thm)],[t1691,t139]) ).
cnf(t1747,plain,
meet(sFlat0,join(X1,sFlat8)) = sFlat0,
inference(orient,[status(thm)],[t68263]) ).
cnf(t68856,plain,
join(sFlat2,sFlat8) = join(sFlat0,join(sFlat2,sFlat8)),
inference(step,[status(thm)],[t68855,t1747]) ).
cnf(t188,plain,
join(sFlat0,join(sFlat2,X1)) = join(sFlat3,X1),
inference(cp,[status(thm)],[t69,t186]) ).
cnf(t379,plain,
join(sFlat0,join(sFlat2,X1)) = join(sFlat3,X1),
inference(orient,[status(thm)],[t188]) ).
cnf(t68857,plain,
join(sFlat2,sFlat8) = join(sFlat3,sFlat8),
inference(step,[status(thm)],[t68856,t379]) ).
cnf(t243,plain,
join(sFlat8,X1) = join(sFlat7,join(X1,b)),
inference(cp,[status(thm)],[t237,t66]) ).
cnf(t500,plain,
join(sFlat7,join(X1,b)) = join(sFlat8,X1),
inference(orient,[status(thm)],[t243]) ).
cnf(t74,plain,
join(X1,join(meet(X1,X2),X3)) = join(X1,X3),
inference(cp,[status(thm)],[t69,t22]) ).
cnf(t996,plain,
join(X1,join(meet(X1,X2),X3)) = join(X1,X3),
inference(orient,[status(thm)],[t74]) ).
cnf(t999,plain,
join(X1,X2) = join(X1,join(X2,meet(X1,X3))),
inference(cp,[status(thm)],[t996,t66]) ).
cnf(t1934,plain,
join(X1,join(X2,meet(X1,X3))) = join(X1,X2),
inference(orient,[status(thm)],[t999]) ).
cnf(t3077,plain,
join(sFlat3,b) = join(sFlat3,sFlat5),
inference(cp,[status(thm)],[t1934,t3069]) ).
cnf(t3099,plain,
join(sFlat3,b) = join(sFlat3,sFlat5),
inference(orient,[status(thm)],[t3077]) ).
cnf(t3100,plain,
join(sFlat8,sFlat3) = join(sFlat7,join(sFlat3,sFlat5)),
inference(cp,[status(thm)],[t500,t3099]) ).
cnf(t68374,plain,
join(sFlat3,sFlat8) = join(sFlat7,join(sFlat3,sFlat5)),
inference(step,[status(thm)],[t3100,t66]) ).
cnf(t75,plain,
join(X1,join(X2,X3)) = join(join(X2,X1),X3),
inference(cp,[status(thm)],[t69,t66]) ).
cnf(t68155,plain,
join(X1,join(X2,X3)) = join(X2,join(X1,X3)),
inference(step,[status(thm)],[t75,t69]) ).
cnf(t331,plain,
join(X1,join(X2,X3)) = join(X2,join(X1,X3)),
inference(orient,[status(thm)],[t68155]) ).
cnf(t68375,plain,
join(sFlat3,sFlat8) = join(sFlat3,join(sFlat7,sFlat5)),
inference(step,[status(thm)],[t68374,t331]) ).
cnf(t68376,plain,
join(sFlat3,sFlat8) = join(sFlat3,join(sFlat5,sFlat7)),
inference(step,[status(thm)],[t68375,t66]) ).
cnf(t3161,plain,
join(sFlat3,join(sFlat5,sFlat7)) = join(sFlat3,sFlat8),
inference(orient,[status(thm)],[t68376]) ).
cnf(t3072,plain,
join(sFlat8,meet(sFlat3,a)) = join(sFlat8,sFlat5),
inference(cp,[status(thm)],[t492,t3069]) ).
cnf(t68371,plain,
join(sFlat8,meet(sFlat3,a)) = join(sFlat5,sFlat8),
inference(step,[status(thm)],[t3072,t66]) ).
cnf(t91,plain,
b = meet(b,sFlat5),
inference(cp,[status(thm)],[t20,t90]) ).
cnf(t68129,plain,
b = meet(sFlat5,b),
inference(step,[status(thm)],[t91,t23]) ).
cnf(t128,plain,
meet(sFlat5,b) = b,
inference(orient,[status(thm)],[t68129]) ).
cnf(t130,plain,
sFlat5 = join(sFlat5,b),
inference(cp,[status(thm)],[t22,t128]) ).
cnf(t148,plain,
join(sFlat5,b) = sFlat5,
inference(orient,[status(thm)],[t130]) ).
cnf(t502,plain,
join(sFlat8,sFlat5) = join(sFlat7,sFlat5),
inference(cp,[status(thm)],[t500,t148]) ).
cnf(t68187,plain,
join(sFlat5,sFlat8) = join(sFlat7,sFlat5),
inference(step,[status(thm)],[t502,t66]) ).
cnf(t68188,plain,
join(sFlat5,sFlat8) = join(sFlat5,sFlat7),
inference(step,[status(thm)],[t68187,t66]) ).
cnf(t510,plain,
join(sFlat5,sFlat8) = join(sFlat5,sFlat7),
inference(orient,[status(thm)],[t68188]) ).
cnf(t68372,plain,
join(sFlat8,meet(sFlat3,a)) = join(sFlat5,sFlat7),
inference(step,[status(thm)],[t68371,t510]) ).
cnf(t3131,plain,
join(sFlat8,meet(sFlat3,a)) = join(sFlat5,sFlat7),
inference(orient,[status(thm)],[t68372]) ).
cnf(t68564,plain,
join(sFlat8,sFlat4) = join(sFlat5,sFlat7),
inference(step,[status(thm)],[t3131,t8552]) ).
cnf(t8571,plain,
join(sFlat8,sFlat4) = join(sFlat5,sFlat7),
inference(rw,[status(thm)],[t68564]) ).
cnf(t68643,plain,
join(sFlat4,sFlat8) = join(sFlat5,sFlat7),
inference(step,[status(thm)],[t8571,t66]) ).
cnf(t8842,plain,
join(sFlat5,sFlat7) = join(sFlat4,sFlat8),
inference(orient,[status(thm)],[t68643]) ).
cnf(t68650,plain,
join(sFlat3,join(sFlat4,sFlat8)) = join(sFlat3,sFlat8),
inference(step,[status(thm)],[t3161,t8842]) ).
cnf(t8864,plain,
join(sFlat3,join(sFlat4,sFlat8)) = join(sFlat3,sFlat8),
inference(rw,[status(thm)],[t68650]) ).
cnf(t8911,plain,
join(sFlat3,join(sFlat4,sFlat8)) = join(sFlat3,sFlat8),
inference(orient,[status(thm)],[t8864]) ).
cnf(t214,plain,
meet(sFlat7,join(sFlat4,b)) = meet(c,sFlat6),
inference(cp,[status(thm)],[t213,t175]) ).
cnf(t68202,plain,
meet(sFlat7,join(sFlat4,b)) = meet(sFlat6,c),
inference(step,[status(thm)],[t214,t23]) ).
cnf(t220,plain,
meet(sFlat7,X1) = meet(c,meet(X1,a)),
inference(cp,[status(thm)],[t213,t23]) ).
cnf(t416,plain,
meet(c,meet(X1,a)) = meet(sFlat7,X1),
inference(orient,[status(thm)],[t220]) ).
cnf(t104,plain,
sFlat6 = meet(sFlat6,a),
inference(cp,[status(thm)],[t20,t103]) ).
cnf(t135,plain,
meet(sFlat6,a) = sFlat6,
inference(orient,[status(thm)],[t104]) ).
cnf(t419,plain,
meet(sFlat7,sFlat6) = meet(c,sFlat6),
inference(cp,[status(thm)],[t416,t135]) ).
cnf(t68174,plain,
meet(sFlat6,sFlat7) = meet(c,sFlat6),
inference(step,[status(thm)],[t419,t23]) ).
cnf(t68175,plain,
meet(sFlat6,sFlat7) = meet(sFlat6,c),
inference(step,[status(thm)],[t68174,t23]) ).
cnf(t472,plain,
meet(sFlat6,c) = meet(sFlat6,sFlat7),
inference(orient,[status(thm)],[t68175]) ).
cnf(t68203,plain,
meet(sFlat7,join(sFlat4,b)) = meet(sFlat6,sFlat7),
inference(step,[status(thm)],[t68202,t472]) ).
cnf(t660,plain,
meet(sFlat7,join(sFlat4,b)) = meet(sFlat6,sFlat7),
inference(orient,[status(thm)],[t68203]) ).
cnf(t699,plain,
meet(X1,X2) = meet(X1,meet(X2,join(X1,X3))),
inference(cp,[status(thm)],[t695,t23]) ).
cnf(t1912,plain,
meet(X1,meet(X2,join(X1,X3))) = meet(X1,X2),
inference(orient,[status(thm)],[t699]) ).
cnf(t691,plain,
meet(sFlat2,meet(a,X1)) = meet(sFlat2,meet(sFlat7,X1)),
inference(cp,[status(thm)],[t689,t213]) ).
cnf(t1835,plain,
meet(sFlat2,meet(a,X1)) = meet(sFlat2,meet(sFlat7,X1)),
inference(orient,[status(thm)],[t691]) ).
cnf(t730,plain,
meet(sFlat2,meet(a,X1)) = meet(sFlat1,meet(sFlat7,X1)),
inference(cp,[status(thm)],[t728,t213]) ).
cnf(t68282,plain,
meet(sFlat2,meet(sFlat7,X1)) = meet(sFlat1,meet(sFlat7,X1)),
inference(step,[status(thm)],[t730,t1835]) ).
cnf(t1886,plain,
meet(sFlat2,meet(sFlat7,X1)) = meet(sFlat1,meet(sFlat7,X1)),
inference(orient,[status(thm)],[t68282]) ).
cnf(t68283,plain,
meet(sFlat2,meet(a,X1)) = meet(sFlat1,meet(sFlat7,X1)),
inference(step,[status(thm)],[t1835,t1886]) ).
cnf(t1887,plain,
meet(sFlat2,meet(a,X1)) = meet(sFlat1,meet(sFlat7,X1)),
inference(orient,[status(thm)],[t68283]) ).
cnf(t76,plain,
join(X1,X2) = meet(join(X1,X2),join(X1,join(X2,X3))),
inference(cp,[status(thm)],[t20,t69]) ).
cnf(t6095,plain,
meet(join(X1,X2),join(X1,join(X2,X3))) = join(X1,X2),
inference(orient,[status(thm)],[t76]) ).
cnf(t52,plain,
a = join(a,sFlat9),
inference(cp,[status(thm)],[t22,t50]) ).
cnf(t68124,plain,
a = join(sFlat9,a),
inference(step,[status(thm)],[t52,t66]) ).
cnf(t107,plain,
join(sFlat9,a) = a,
inference(orient,[status(thm)],[t68124]) ).
cnf(t6199,plain,
join(X1,sFlat9) = meet(join(X1,sFlat9),join(X1,a)),
inference(cp,[status(thm)],[t6095,t107]) ).
cnf(t6276,plain,
meet(join(X1,sFlat9),join(X1,a)) = join(X1,sFlat9),
inference(orient,[status(thm)],[t6199]) ).
cnf(t6280,plain,
join(sFlat6,sFlat9) = meet(join(sFlat6,sFlat9),a),
inference(cp,[status(thm)],[t6276,t103]) ).
cnf(t68467,plain,
join(sFlat6,sFlat9) = meet(a,join(sFlat6,sFlat9)),
inference(step,[status(thm)],[t6280,t23]) ).
cnf(t6290,plain,
meet(a,join(sFlat6,sFlat9)) = join(sFlat6,sFlat9),
inference(orient,[status(thm)],[t68467]) ).
cnf(t6293,plain,
meet(sFlat1,meet(sFlat7,join(sFlat6,sFlat9))) = meet(sFlat2,join(sFlat6,sFlat9)),
inference(cp,[status(thm)],[t1887,t6290]) ).
cnf(t1277,plain,
X1 = meet(X1,join(X2,join(X1,X3))),
inference(cp,[status(thm)],[t1270,t320]) ).
cnf(t2028,plain,
meet(X1,join(X2,join(X1,X3))) = X1,
inference(orient,[status(thm)],[t1277]) ).
cnf(t417,plain,
meet(sFlat7,sFlat8) = meet(c,sFlat9),
inference(cp,[status(thm)],[t416,t154]) ).
cnf(t96,plain,
sFlat7 = meet(sFlat7,sFlat8),
inference(cp,[status(thm)],[t20,t95]) ).
cnf(t131,plain,
meet(sFlat7,sFlat8) = sFlat7,
inference(orient,[status(thm)],[t96]) ).
cnf(t68172,plain,
sFlat7 = meet(c,sFlat9),
inference(step,[status(thm)],[t417,t131]) ).
cnf(t68173,plain,
sFlat7 = meet(sFlat9,c),
inference(step,[status(thm)],[t68172,t23]) ).
cnf(t469,plain,
meet(sFlat9,c) = sFlat7,
inference(orient,[status(thm)],[t68173]) ).
cnf(t470,plain,
sFlat9 = join(sFlat9,sFlat7),
inference(cp,[status(thm)],[t22,t469]) ).
cnf(t68178,plain,
sFlat9 = join(sFlat7,sFlat9),
inference(step,[status(thm)],[t470,t66]) ).
cnf(t476,plain,
join(sFlat7,sFlat9) = sFlat9,
inference(orient,[status(thm)],[t68178]) ).
cnf(t2056,plain,
sFlat7 = meet(sFlat7,join(X1,sFlat9)),
inference(cp,[status(thm)],[t2028,t476]) ).
cnf(t2333,plain,
meet(sFlat7,join(X1,sFlat9)) = sFlat7,
inference(orient,[status(thm)],[t2056]) ).
cnf(t68482,plain,
meet(sFlat1,sFlat7) = meet(sFlat2,join(sFlat6,sFlat9)),
inference(step,[status(thm)],[t6293,t2333]) ).
cnf(t68483,plain,
sFlat7 = meet(sFlat2,join(sFlat6,sFlat9)),
inference(step,[status(thm)],[t68482,t539]) ).
cnf(t6862,plain,
meet(sFlat2,join(sFlat6,sFlat9)) = sFlat7,
inference(orient,[status(thm)],[t68483]) ).
cnf(t6863,plain,
meet(sFlat6,sFlat2) = meet(sFlat6,sFlat7),
inference(cp,[status(thm)],[t1912,t6862]) ).
cnf(t68484,plain,
meet(sFlat2,sFlat6) = meet(sFlat6,sFlat7),
inference(step,[status(thm)],[t6863,t23]) ).
cnf(t6872,plain,
meet(sFlat6,sFlat7) = meet(sFlat2,sFlat6),
inference(orient,[status(thm)],[t68484]) ).
cnf(t68487,plain,
meet(sFlat7,join(sFlat4,b)) = meet(sFlat2,sFlat6),
inference(step,[status(thm)],[t660,t6872]) ).
cnf(t6875,plain,
meet(sFlat7,join(sFlat4,b)) = meet(sFlat2,sFlat6),
inference(orient,[status(thm)],[t68487]) ).
cnf(t68592,plain,
meet(sFlat7,sFlat5) = meet(sFlat2,sFlat6),
inference(step,[status(thm)],[t6875,t8667]) ).
cnf(t8690,plain,
meet(sFlat7,sFlat5) = meet(sFlat2,sFlat6),
inference(rw,[status(thm)],[t68592]) ).
cnf(t68658,plain,
meet(sFlat5,sFlat7) = meet(sFlat2,sFlat6),
inference(step,[status(thm)],[t8690,t23]) ).
cnf(t134,plain,
meet(sFlat4,meet(a,X1)) = meet(sFlat4,X1),
inference(cp,[status(thm)],[t24,t133]) ).
cnf(t667,plain,
meet(sFlat4,meet(a,X1)) = meet(sFlat4,X1),
inference(orient,[status(thm)],[t134]) ).
cnf(t668,plain,
meet(sFlat4,join(sFlat4,b)) = meet(sFlat4,sFlat6),
inference(cp,[status(thm)],[t667,t175]) ).
cnf(t68206,plain,
sFlat4 = meet(sFlat4,sFlat6),
inference(step,[status(thm)],[t668,t20]) ).
cnf(t671,plain,
meet(sFlat4,sFlat6) = sFlat4,
inference(orient,[status(thm)],[t68206]) ).
cnf(t1078,plain,
sFlat6 = join(sFlat6,meet(X1,sFlat4)),
inference(cp,[status(thm)],[t1041,t671]) ).
cnf(t1237,plain,
join(sFlat6,meet(X1,sFlat4)) = sFlat6,
inference(orient,[status(thm)],[t1078]) ).
cnf(t8517,plain,
meet(sFlat4,X1) = meet(sFlat3,meet(X1,a)),
inference(cp,[status(thm)],[t8483,t23]) ).
cnf(t8728,plain,
meet(sFlat3,meet(X1,a)) = meet(sFlat4,X1),
inference(orient,[status(thm)],[t8517]) ).
cnf(t215,plain,
meet(sFlat7,a) = meet(c,a),
inference(cp,[status(thm)],[t213,t19]) ).
cnf(t68145,plain,
meet(sFlat7,a) = sFlat7,
inference(step,[status(thm)],[t215,t58]) ).
cnf(t224,plain,
meet(sFlat7,a) = sFlat7,
inference(orient,[status(thm)],[t68145]) ).
cnf(t8735,plain,
meet(sFlat4,sFlat7) = meet(sFlat3,sFlat7),
inference(cp,[status(thm)],[t8728,t224]) ).
cnf(t1916,plain,
meet(sFlat4,sFlat7) = meet(sFlat4,meet(sFlat6,sFlat7)),
inference(cp,[status(thm)],[t1912,t660]) ).
cnf(t1926,plain,
meet(sFlat4,meet(sFlat6,sFlat7)) = meet(sFlat4,sFlat7),
inference(orient,[status(thm)],[t1916]) ).
cnf(t68489,plain,
meet(sFlat4,meet(sFlat2,sFlat6)) = meet(sFlat4,sFlat7),
inference(step,[status(thm)],[t1926,t6872]) ).
cnf(t6887,plain,
meet(sFlat4,meet(sFlat2,sFlat6)) = meet(sFlat4,sFlat7),
inference(rw,[status(thm)],[t68489]) ).
cnf(t68490,plain,
meet(sFlat2,meet(sFlat4,sFlat6)) = meet(sFlat4,sFlat7),
inference(step,[status(thm)],[t6887,t315]) ).
cnf(t68491,plain,
meet(sFlat2,sFlat4) = meet(sFlat4,sFlat7),
inference(step,[status(thm)],[t68490,t671]) ).
cnf(t6888,plain,
meet(sFlat4,sFlat7) = meet(sFlat2,sFlat4),
inference(orient,[status(thm)],[t68491]) ).
cnf(t68598,plain,
meet(sFlat2,sFlat4) = meet(sFlat3,sFlat7),
inference(step,[status(thm)],[t8735,t6888]) ).
cnf(t384,plain,
join(sFlat3,meet(sFlat2,X1)) = join(sFlat0,sFlat2),
inference(cp,[status(thm)],[t379,t22]) ).
cnf(t68198,plain,
join(sFlat3,meet(sFlat2,X1)) = sFlat3,
inference(step,[status(thm)],[t384,t186]) ).
cnf(t642,plain,
join(sFlat3,meet(sFlat2,X1)) = sFlat3,
inference(orient,[status(thm)],[t68198]) ).
cnf(t738,plain,
sFlat3 = join(sFlat3,sFlat7),
inference(cp,[status(thm)],[t642,t735]) ).
cnf(t740,plain,
join(sFlat3,sFlat7) = sFlat3,
inference(orient,[status(thm)],[t738]) ).
cnf(t1392,plain,
sFlat7 = meet(sFlat7,sFlat3),
inference(cp,[status(thm)],[t1389,t740]) ).
cnf(t68255,plain,
sFlat7 = meet(sFlat3,sFlat7),
inference(step,[status(thm)],[t1392,t23]) ).
cnf(t1426,plain,
meet(sFlat3,sFlat7) = sFlat7,
inference(orient,[status(thm)],[t68255]) ).
cnf(t68599,plain,
meet(sFlat2,sFlat4) = sFlat7,
inference(step,[status(thm)],[t68598,t1426]) ).
cnf(t8747,plain,
meet(sFlat2,sFlat4) = sFlat7,
inference(orient,[status(thm)],[t68599]) ).
cnf(t8754,plain,
sFlat6 = join(sFlat6,sFlat7),
inference(cp,[status(thm)],[t1237,t8747]) ).
cnf(t8783,plain,
join(sFlat6,sFlat7) = sFlat6,
inference(orient,[status(thm)],[t8754]) ).
cnf(t8784,plain,
sFlat7 = meet(sFlat7,sFlat6),
inference(cp,[status(thm)],[t1389,t8783]) ).
cnf(t68632,plain,
sFlat7 = meet(sFlat6,sFlat7),
inference(step,[status(thm)],[t8784,t23]) ).
cnf(t68633,plain,
sFlat7 = meet(sFlat2,sFlat6),
inference(step,[status(thm)],[t68632,t6872]) ).
cnf(t8810,plain,
meet(sFlat2,sFlat6) = sFlat7,
inference(orient,[status(thm)],[t68633]) ).
cnf(t68659,plain,
meet(sFlat5,sFlat7) = sFlat7,
inference(step,[status(thm)],[t68658,t8810]) ).
cnf(t8893,plain,
meet(sFlat5,sFlat7) = sFlat7,
inference(orient,[status(thm)],[t68659]) ).
cnf(t8897,plain,
sFlat5 = join(sFlat5,sFlat7),
inference(cp,[status(thm)],[t22,t8893]) ).
cnf(t68660,plain,
sFlat5 = join(sFlat4,sFlat8),
inference(step,[status(thm)],[t8897,t8842]) ).
cnf(t8927,plain,
join(sFlat4,sFlat8) = sFlat5,
inference(orient,[status(thm)],[t68660]) ).
cnf(t68669,plain,
join(sFlat3,sFlat5) = join(sFlat3,sFlat8),
inference(step,[status(thm)],[t8911,t8927]) ).
cnf(t8955,plain,
join(sFlat3,sFlat5) = join(sFlat3,sFlat8),
inference(rw,[status(thm)],[t68669]) ).
cnf(t8973,plain,
join(sFlat3,sFlat8) = join(sFlat3,sFlat5),
inference(orient,[status(thm)],[t8955]) ).
cnf(t1822,plain,
meet(sFlat6,join(join(sFlat4,b),X1)) = meet(a,join(sFlat4,b)),
inference(cp,[status(thm)],[t1817,t20]) ).
cnf(t68288,plain,
meet(sFlat6,join(sFlat4,join(b,X1))) = meet(a,join(sFlat4,b)),
inference(step,[status(thm)],[t1822,t69]) ).
cnf(t68289,plain,
meet(sFlat6,join(sFlat4,join(b,X1))) = sFlat6,
inference(step,[status(thm)],[t68288,t175]) ).
cnf(t1957,plain,
meet(sFlat6,join(sFlat4,join(b,X1))) = sFlat6,
inference(orient,[status(thm)],[t68289]) ).
cnf(t1959,plain,
sFlat6 = meet(sFlat6,join(sFlat4,join(X1,b))),
inference(cp,[status(thm)],[t1957,t66]) ).
cnf(t3043,plain,
meet(sFlat6,join(sFlat4,join(X1,b))) = sFlat6,
inference(orient,[status(thm)],[t1959]) ).
cnf(t3045,plain,
sFlat6 = meet(sFlat6,join(sFlat4,sFlat5)),
inference(cp,[status(thm)],[t3043,t148]) ).
cnf(t3052,plain,
meet(sFlat6,join(sFlat4,sFlat5)) = sFlat6,
inference(orient,[status(thm)],[t3045]) ).
cnf(t149,plain,
join(sFlat5,join(b,X1)) = join(sFlat5,X1),
inference(cp,[status(thm)],[t69,t148]) ).
cnf(t712,plain,
join(sFlat5,join(b,X1)) = join(sFlat5,X1),
inference(orient,[status(thm)],[t149]) ).
cnf(t3071,plain,
join(sFlat5,meet(sFlat3,a)) = join(sFlat5,sFlat5),
inference(cp,[status(thm)],[t712,t3069]) ).
cnf(t68370,plain,
join(sFlat5,meet(sFlat3,a)) = sFlat5,
inference(step,[status(thm)],[t3071,t21]) ).
cnf(t3126,plain,
join(sFlat5,meet(sFlat3,a)) = sFlat5,
inference(orient,[status(thm)],[t68370]) ).
cnf(t68565,plain,
join(sFlat5,sFlat4) = sFlat5,
inference(step,[status(thm)],[t3126,t8552]) ).
cnf(t8572,plain,
join(sFlat5,sFlat4) = sFlat5,
inference(rw,[status(thm)],[t68565]) ).
cnf(t68578,plain,
join(sFlat4,sFlat5) = sFlat5,
inference(step,[status(thm)],[t8572,t66]) ).
cnf(t8632,plain,
join(sFlat4,sFlat5) = sFlat5,
inference(orient,[status(thm)],[t68578]) ).
cnf(t68581,plain,
meet(sFlat6,sFlat5) = sFlat6,
inference(step,[status(thm)],[t3052,t8632]) ).
cnf(t8645,plain,
meet(sFlat6,sFlat5) = sFlat6,
inference(rw,[status(thm)],[t68581]) ).
cnf(t68582,plain,
meet(sFlat5,sFlat6) = sFlat6,
inference(step,[status(thm)],[t8645,t23]) ).
cnf(t8651,plain,
meet(sFlat5,sFlat6) = sFlat6,
inference(orient,[status(thm)],[t68582]) ).
cnf(t8655,plain,
join(sFlat5,X1) = join(sFlat5,join(X1,sFlat6)),
inference(cp,[status(thm)],[t1934,t8651]) ).
cnf(t9330,plain,
join(sFlat5,join(X1,sFlat6)) = join(sFlat5,X1),
inference(orient,[status(thm)],[t8655]) ).
cnf(t1155,plain,
sFlat6 = join(sFlat6,sFlat4),
inference(cp,[status(thm)],[t1142,t671]) ).
cnf(t68242,plain,
sFlat6 = join(sFlat4,sFlat6),
inference(step,[status(thm)],[t1155,t66]) ).
cnf(t1183,plain,
join(sFlat4,sFlat6) = sFlat6,
inference(orient,[status(thm)],[t68242]) ).
cnf(t6203,plain,
join(X1,sFlat4) = meet(join(X1,sFlat4),join(X1,sFlat6)),
inference(cp,[status(thm)],[t6095,t1183]) ).
cnf(t12264,plain,
meet(join(X1,sFlat4),join(X1,sFlat6)) = join(X1,sFlat4),
inference(orient,[status(thm)],[t6203]) ).
cnf(t81,plain,
sFlat0 = meet(sFlat0,sFlat3),
inference(cp,[status(thm)],[t20,t80]) ).
cnf(t123,plain,
meet(sFlat0,sFlat3) = sFlat0,
inference(orient,[status(thm)],[t81]) ).
cnf(t124,plain,
meet(sFlat0,meet(sFlat3,X1)) = meet(sFlat0,X1),
inference(cp,[status(thm)],[t24,t123]) ).
cnf(t360,plain,
meet(sFlat0,meet(sFlat3,X1)) = meet(sFlat0,X1),
inference(orient,[status(thm)],[t124]) ).
cnf(t1167,plain,
meet(sFlat3,X1) = join(meet(sFlat3,X1),meet(sFlat0,X1)),
inference(cp,[status(thm)],[t1142,t360]) ).
cnf(t68442,plain,
meet(sFlat3,X1) = join(meet(sFlat0,X1),meet(sFlat3,X1)),
inference(step,[status(thm)],[t1167,t66]) ).
cnf(t5384,plain,
join(meet(sFlat0,X1),meet(sFlat3,X1)) = meet(sFlat3,X1),
inference(orient,[status(thm)],[t68442]) ).
cnf(t1413,plain,
join(sFlat2,X1) = meet(join(sFlat2,X1),join(sFlat3,X1)),
inference(cp,[status(thm)],[t1389,t379]) ).
cnf(t5904,plain,
meet(join(sFlat2,X1),join(sFlat3,X1)) = join(sFlat2,X1),
inference(orient,[status(thm)],[t1413]) ).
cnf(t8499,plain,
meet(sFlat4,join(sFlat4,b)) = meet(sFlat3,sFlat6),
inference(cp,[status(thm)],[t8483,t175]) ).
cnf(t68556,plain,
sFlat4 = meet(sFlat3,sFlat6),
inference(step,[status(thm)],[t8499,t20]) ).
cnf(t8535,plain,
meet(sFlat3,sFlat6) = sFlat4,
inference(orient,[status(thm)],[t68556]) ).
cnf(t8541,plain,
sFlat3 = join(sFlat3,sFlat4),
inference(cp,[status(thm)],[t22,t8535]) ).
cnf(t8574,plain,
join(sFlat3,sFlat4) = sFlat3,
inference(orient,[status(thm)],[t8541]) ).
cnf(t8575,plain,
join(sFlat2,sFlat4) = meet(join(sFlat2,sFlat4),sFlat3),
inference(cp,[status(thm)],[t5904,t8574]) ).
cnf(t68698,plain,
join(sFlat2,sFlat4) = meet(sFlat3,join(sFlat2,sFlat4)),
inference(step,[status(thm)],[t8575,t23]) ).
cnf(t9431,plain,
meet(sFlat3,join(sFlat2,sFlat4)) = join(sFlat2,sFlat4),
inference(orient,[status(thm)],[t68698]) ).
cnf(t9432,plain,
meet(sFlat3,join(sFlat2,sFlat4)) = join(meet(sFlat0,join(sFlat2,sFlat4)),join(sFlat2,sFlat4)),
inference(cp,[status(thm)],[t5384,t9431]) ).
cnf(t68699,plain,
join(sFlat2,sFlat4) = join(meet(sFlat0,join(sFlat2,sFlat4)),join(sFlat2,sFlat4)),
inference(step,[status(thm)],[t9432,t9431]) ).
cnf(t55,plain,
meet(b,meet(a,X1)) = meet(sFlat0,X1),
inference(cp,[status(thm)],[t24,t54]) ).
cnf(t193,plain,
meet(b,meet(a,X1)) = meet(sFlat0,X1),
inference(orient,[status(thm)],[t55]) ).
cnf(t194,plain,
meet(sFlat0,join(sFlat4,b)) = meet(b,sFlat6),
inference(cp,[status(thm)],[t193,t175]) ).
cnf(t68200,plain,
meet(sFlat0,join(sFlat4,b)) = meet(sFlat6,b),
inference(step,[status(thm)],[t194,t23]) ).
cnf(t199,plain,
meet(sFlat0,X1) = meet(b,meet(X1,a)),
inference(cp,[status(thm)],[t193,t23]) ).
cnf(t394,plain,
meet(b,meet(X1,a)) = meet(sFlat0,X1),
inference(orient,[status(thm)],[t199]) ).
cnf(t397,plain,
meet(sFlat0,sFlat6) = meet(b,sFlat6),
inference(cp,[status(thm)],[t394,t135]) ).
cnf(t68166,plain,
meet(sFlat0,sFlat6) = meet(sFlat6,b),
inference(step,[status(thm)],[t397,t23]) ).
cnf(t406,plain,
meet(sFlat6,b) = meet(sFlat0,sFlat6),
inference(orient,[status(thm)],[t68166]) ).
cnf(t68201,plain,
meet(sFlat0,join(sFlat4,b)) = meet(sFlat0,sFlat6),
inference(step,[status(thm)],[t68200,t406]) ).
cnf(t656,plain,
meet(sFlat0,join(sFlat4,b)) = meet(sFlat0,sFlat6),
inference(orient,[status(thm)],[t68201]) ).
cnf(t348,plain,
sFlat0 = meet(sFlat0,join(b,X1)),
inference(cp,[status(thm)],[t20,t345]) ).
cnf(t586,plain,
meet(sFlat0,join(b,X1)) = sFlat0,
inference(orient,[status(thm)],[t348]) ).
cnf(t589,plain,
sFlat0 = meet(sFlat0,join(X1,b)),
inference(cp,[status(thm)],[t586,t66]) ).
cnf(t813,plain,
meet(sFlat0,join(X1,b)) = sFlat0,
inference(orient,[status(thm)],[t589]) ).
cnf(t68226,plain,
sFlat0 = meet(sFlat0,sFlat6),
inference(step,[status(thm)],[t656,t813]) ).
cnf(t818,plain,
sFlat0 = meet(sFlat0,sFlat6),
inference(rw,[status(thm)],[t68226]) ).
cnf(t819,plain,
meet(sFlat0,sFlat6) = sFlat0,
inference(orient,[status(thm)],[t818]) ).
cnf(t5406,plain,
meet(sFlat3,sFlat6) = join(sFlat0,meet(sFlat3,sFlat6)),
inference(cp,[status(thm)],[t5384,t819]) ).
cnf(t5463,plain,
join(sFlat0,meet(sFlat3,sFlat6)) = meet(sFlat3,sFlat6),
inference(orient,[status(thm)],[t5406]) ).
cnf(t68557,plain,
join(sFlat0,sFlat4) = meet(sFlat3,sFlat6),
inference(step,[status(thm)],[t5463,t8535]) ).
cnf(t68558,plain,
join(sFlat0,sFlat4) = sFlat4,
inference(step,[status(thm)],[t68557,t8535]) ).
cnf(t8551,plain,
join(sFlat0,sFlat4) = sFlat4,
inference(rw,[status(thm)],[t68558]) ).
cnf(t8585,plain,
join(sFlat0,sFlat4) = sFlat4,
inference(orient,[status(thm)],[t8551]) ).
cnf(t8589,plain,
sFlat0 = meet(sFlat0,join(X1,sFlat4)),
inference(cp,[status(thm)],[t2028,t8585]) ).
cnf(t9123,plain,
meet(sFlat0,join(X1,sFlat4)) = sFlat0,
inference(orient,[status(thm)],[t8589]) ).
cnf(t68700,plain,
join(sFlat2,sFlat4) = join(sFlat0,join(sFlat2,sFlat4)),
inference(step,[status(thm)],[t68699,t9123]) ).
cnf(t68701,plain,
join(sFlat2,sFlat4) = join(sFlat3,sFlat4),
inference(step,[status(thm)],[t68700,t379]) ).
cnf(t68702,plain,
join(sFlat2,sFlat4) = sFlat3,
inference(step,[status(thm)],[t68701,t8574]) ).
cnf(t9443,plain,
join(sFlat2,sFlat4) = sFlat3,
inference(orient,[status(thm)],[t68702]) ).
cnf(t12265,plain,
join(sFlat2,sFlat4) = meet(sFlat3,join(sFlat2,sFlat6)),
inference(cp,[status(thm)],[t12264,t9443]) ).
cnf(t68797,plain,
sFlat3 = meet(sFlat3,join(sFlat2,sFlat6)),
inference(step,[status(thm)],[t12265,t9443]) ).
cnf(t12277,plain,
meet(sFlat3,join(sFlat2,sFlat6)) = sFlat3,
inference(orient,[status(thm)],[t68797]) ).
cnf(t12278,plain,
join(sFlat2,sFlat6) = join(join(sFlat2,sFlat6),sFlat3),
inference(cp,[status(thm)],[t1142,t12277]) ).
cnf(t68798,plain,
join(sFlat2,sFlat6) = join(sFlat2,join(sFlat6,sFlat3)),
inference(step,[status(thm)],[t12278,t69]) ).
cnf(t68799,plain,
join(sFlat2,sFlat6) = join(sFlat2,join(sFlat3,sFlat6)),
inference(step,[status(thm)],[t68798,t66]) ).
cnf(t383,plain,
join(sFlat3,join(sFlat2,X1)) = join(sFlat0,join(sFlat2,X1)),
inference(cp,[status(thm)],[t379,t178]) ).
cnf(t68219,plain,
join(sFlat2,join(sFlat3,X1)) = join(sFlat0,join(sFlat2,X1)),
inference(step,[status(thm)],[t383,t331]) ).
cnf(t68220,plain,
join(sFlat2,join(sFlat3,X1)) = join(sFlat3,X1),
inference(step,[status(thm)],[t68219,t379]) ).
cnf(t771,plain,
join(sFlat2,join(sFlat3,X1)) = join(sFlat3,X1),
inference(orient,[status(thm)],[t68220]) ).
cnf(t68800,plain,
join(sFlat2,sFlat6) = join(sFlat3,sFlat6),
inference(step,[status(thm)],[t68799,t771]) ).
cnf(t12288,plain,
join(sFlat3,sFlat6) = join(sFlat2,sFlat6),
inference(orient,[status(thm)],[t68800]) ).
cnf(t12289,plain,
join(sFlat5,sFlat3) = join(sFlat5,join(sFlat2,sFlat6)),
inference(cp,[status(thm)],[t9330,t12288]) ).
cnf(t68801,plain,
join(sFlat3,sFlat5) = join(sFlat5,join(sFlat2,sFlat6)),
inference(step,[status(thm)],[t12289,t66]) ).
cnf(t68802,plain,
join(sFlat3,sFlat5) = join(sFlat5,sFlat2),
inference(step,[status(thm)],[t68801,t9330]) ).
cnf(t68803,plain,
join(sFlat3,sFlat5) = join(sFlat2,sFlat5),
inference(step,[status(thm)],[t68802,t66]) ).
cnf(t12305,plain,
join(sFlat3,sFlat5) = join(sFlat2,sFlat5),
inference(orient,[status(thm)],[t68803]) ).
cnf(t68806,plain,
join(sFlat3,sFlat8) = join(sFlat2,sFlat5),
inference(step,[status(thm)],[t8973,t12305]) ).
cnf(t12308,plain,
join(sFlat3,sFlat8) = join(sFlat2,sFlat5),
inference(orient,[status(thm)],[t68806]) ).
cnf(t68858,plain,
join(sFlat2,sFlat8) = join(sFlat2,sFlat5),
inference(step,[status(thm)],[t68857,t12308]) ).
cnf(t15049,plain,
join(sFlat2,sFlat8) = join(sFlat2,sFlat5),
inference(orient,[status(thm)],[t68858]) ).
cnf(t70169,plain,
meet(sFlat4,join(sFlat2,sFlat5)) = meet(sFlat4,join(sFlat8,sFlat7)),
inference(step,[status(thm)],[t70168,t15049]) ).
cnf(t8637,plain,
sFlat4 = meet(sFlat4,join(X1,sFlat5)),
inference(cp,[status(thm)],[t2028,t8632]) ).
cnf(t9134,plain,
meet(sFlat4,join(X1,sFlat5)) = sFlat4,
inference(orient,[status(thm)],[t8637]) ).
cnf(t70170,plain,
sFlat4 = meet(sFlat4,join(sFlat8,sFlat7)),
inference(step,[status(thm)],[t70169,t9134]) ).
cnf(t70171,plain,
sFlat4 = meet(sFlat4,join(sFlat7,sFlat8)),
inference(step,[status(thm)],[t70170,t66]) ).
cnf(t180,plain,
join(sFlat7,b) = join(sFlat7,sFlat8),
inference(cp,[status(thm)],[t178,t95]) ).
cnf(t68140,plain,
sFlat8 = join(sFlat7,sFlat8),
inference(step,[status(thm)],[t180,t95]) ).
cnf(t183,plain,
join(sFlat7,sFlat8) = sFlat8,
inference(orient,[status(thm)],[t68140]) ).
cnf(t70172,plain,
sFlat4 = meet(sFlat4,sFlat8),
inference(step,[status(thm)],[t70171,t183]) ).
cnf(t8732,plain,
meet(sFlat4,sFlat8) = meet(sFlat3,sFlat9),
inference(cp,[status(thm)],[t8728,t154]) ).
cnf(t8766,plain,
meet(sFlat4,sFlat8) = meet(sFlat3,sFlat9),
inference(orient,[status(thm)],[t8732]) ).
cnf(t70173,plain,
sFlat4 = meet(sFlat3,sFlat9),
inference(step,[status(thm)],[t70172,t8766]) ).
cnf(t67866,plain,
meet(sFlat3,sFlat9) = sFlat4,
inference(orient,[status(thm)],[t70173]) ).
cnf(t67881,plain,
sFlat8 = join(sFlat8,sFlat4),
inference(cp,[status(thm)],[t848,t67866]) ).
cnf(t70210,plain,
sFlat8 = join(sFlat4,sFlat8),
inference(step,[status(thm)],[t67881,t66]) ).
cnf(t70211,plain,
sFlat8 = sFlat5,
inference(step,[status(thm)],[t70210,t8927]) ).
cnf(t67930,plain,
sFlat8 = sFlat5,
inference(orient,[status(thm)],[t70211]) ).
cnf(t70212,plain,
join(sFlat7,b) = sFlat5,
inference(step,[status(thm)],[t95,t67930]) ).
cnf(t67931,plain,
join(sFlat7,b) = sFlat5,
inference(orient,[status(thm)],[t70212]) ).
cnf(goal_0,negated_conjecture,
meet(a,join(b,meet(a,join(meet(a,b),meet(c,join(a,b)))))) != meet(a,join(b,meet(a,c))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
meet(a,join(b,meet(a,join(meet(b,a),meet(c,join(a,b)))))) != meet(a,join(b,meet(a,c))),
inference(rw,[status(thm)],[goal_0,t23]) ).
cnf(g0_1,plain,
meet(a,join(b,meet(a,join(sFlat0,meet(c,join(a,b)))))) != meet(a,join(b,meet(a,c))),
inference(rw,[status(thm)],[g0_0,t54]) ).
cnf(g0_2,plain,
meet(a,join(b,meet(a,join(sFlat0,meet(c,join(b,a)))))) != meet(a,join(b,meet(a,c))),
inference(rw,[status(thm)],[g0_1,t66]) ).
cnf(g0_3,plain,
meet(a,join(b,meet(a,join(sFlat0,meet(c,sFlat1))))) != meet(a,join(b,meet(a,c))),
inference(rw,[status(thm)],[g0_2,t85]) ).
cnf(g0_4,plain,
meet(a,join(b,meet(a,join(sFlat0,meet(sFlat1,c))))) != meet(a,join(b,meet(a,c))),
inference(rw,[status(thm)],[g0_3,t23]) ).
cnf(g0_5,plain,
meet(a,join(b,meet(a,join(sFlat0,sFlat2)))) != meet(a,join(b,meet(a,c))),
inference(rw,[status(thm)],[g0_4,t164]) ).
cnf(g0_6,plain,
meet(a,join(b,meet(a,sFlat3))) != meet(a,join(b,meet(a,c))),
inference(rw,[status(thm)],[g0_5,t186]) ).
cnf(g0_7,plain,
meet(a,join(b,meet(sFlat3,a))) != meet(a,join(b,meet(a,c))),
inference(rw,[status(thm)],[g0_6,t23]) ).
cnf(g0_8,plain,
meet(a,join(b,sFlat4)) != meet(a,join(b,meet(a,c))),
inference(rw,[status(thm)],[g0_7,t8552]) ).
cnf(g0_9,plain,
meet(a,join(sFlat4,b)) != meet(a,join(b,meet(a,c))),
inference(rw,[status(thm)],[g0_8,t66]) ).
cnf(g0_10,plain,
meet(a,sFlat5) != meet(a,join(b,meet(a,c))),
inference(rw,[status(thm)],[g0_9,t8667]) ).
cnf(g0_11,plain,
meet(a,sFlat5) != meet(a,join(b,meet(c,a))),
inference(rw,[status(thm)],[g0_10,t23]) ).
cnf(g0_12,plain,
meet(a,sFlat5) != meet(a,join(b,sFlat7)),
inference(rw,[status(thm)],[g0_11,t58]) ).
cnf(g0_13,plain,
meet(a,sFlat5) != meet(a,join(sFlat7,b)),
inference(rw,[status(thm)],[g0_12,t66]) ).
cnf(g0_14,plain,
meet(a,sFlat5) != meet(a,sFlat5),
inference(rw,[status(thm)],[g0_13,t67931]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_14]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LAT159-1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.10/0.37 % Computer : n013.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Wed Sep 23 20:24:21 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 198.54/27.78 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 198.54/27.78 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------