%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : LAT153-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 : n002.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:36 PM UTC 2026
% Result : Unsatisfiable 253.99s 48.52s
% Output : CNFRefutation 253.99s
% Verified :
% SZS Type : Refutation
% Derivation depth : 69
% Number of leaves : 20
% Syntax : Number of clauses : 562 ( 562 unt; 0 nHn; 370 RR)
% Number of literals : 562 ( 561 equ; 20 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 : 282 ( 71 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(t95567,plain,
sFlat0 = meet(b,a),
inference(step,[status(thm)],[t9,t23]) ).
cnf(t56,plain,
meet(b,a) = sFlat0,
inference(orient,[status(thm)],[t95567]) ).
cnf(t2,axiom,
join(X1,X2) = join(X2,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t68,plain,
join(X1,X2) = join(X2,X1),
inference(orient,[status(thm)],[t2]) ).
cnf(t10,axiom,
sFlat1 = join(a,b),
introduced(definition) ).
cnf(t95574,plain,
sFlat1 = join(b,a),
inference(step,[status(thm)],[t10,t68]) ).
cnf(t87,plain,
join(b,a) = sFlat1,
inference(orient,[status(thm)],[t95574]) ).
cnf(t11,axiom,
sFlat2 = meet(c,join(a,b)),
introduced(definition) ).
cnf(t64,plain,
meet(c,join(a,b)) = sFlat2,
inference(orient,[status(thm)],[t11]) ).
cnf(t69,plain,
meet(c,join(a,b)) = sFlat2,
inference(rw,[status(thm)],[t64]) ).
cnf(t95596,plain,
meet(c,join(b,a)) = sFlat2,
inference(step,[status(thm)],[t69,t68]) ).
cnf(t95597,plain,
meet(c,sFlat1) = sFlat2,
inference(step,[status(thm)],[t95596,t87]) ).
cnf(t95598,plain,
meet(sFlat1,c) = sFlat2,
inference(step,[status(thm)],[t95597,t23]) ).
cnf(t166,plain,
meet(sFlat1,c) = sFlat2,
inference(orient,[status(thm)],[t95598]) ).
cnf(t12,axiom,
sFlat3 = join(meet(a,b),meet(c,join(a,b))),
introduced(definition) ).
cnf(t95571,plain,
sFlat3 = join(meet(b,a),meet(c,join(a,b))),
inference(step,[status(thm)],[t12,t23]) ).
cnf(t95572,plain,
sFlat3 = join(sFlat0,meet(c,join(a,b))),
inference(step,[status(thm)],[t95571,t56]) ).
cnf(t95573,plain,
sFlat3 = join(sFlat0,meet(c,join(b,a))),
inference(step,[status(thm)],[t95572,t68]) ).
cnf(t82,plain,
join(sFlat0,meet(c,join(b,a))) = sFlat3,
inference(orient,[status(thm)],[t95573]) ).
cnf(t95575,plain,
join(sFlat0,meet(c,sFlat1)) = sFlat3,
inference(step,[status(thm)],[t82,t87]) ).
cnf(t91,plain,
join(sFlat0,meet(c,sFlat1)) = sFlat3,
inference(rw,[status(thm)],[t95575]) ).
cnf(t95603,plain,
join(sFlat0,meet(sFlat1,c)) = sFlat3,
inference(step,[status(thm)],[t91,t23]) ).
cnf(t95604,plain,
join(sFlat0,sFlat2) = sFlat3,
inference(step,[status(thm)],[t95603,t166]) ).
cnf(t187,plain,
join(sFlat0,sFlat2) = sFlat3,
inference(orient,[status(thm)],[t95604]) ).
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(t95563,plain,
sFlat4 = meet(a,join(meet(b,a),meet(c,join(a,b)))),
inference(step,[status(thm)],[t13,t23]) ).
cnf(t44,plain,
meet(a,join(meet(b,a),meet(c,join(a,b)))) = sFlat4,
inference(orient,[status(thm)],[t95563]) ).
cnf(t45,plain,
meet(a,meet(join(meet(b,a),meet(c,join(a,b))),X1)) = meet(sFlat4,X1),
inference(cp,[status(thm)],[t24,t44]) ).
cnf(t95988,plain,
meet(a,meet(join(sFlat0,meet(c,join(a,b))),X1)) = meet(sFlat4,X1),
inference(step,[status(thm)],[t45,t56]) ).
cnf(t95989,plain,
meet(a,meet(join(sFlat0,meet(c,join(b,a))),X1)) = meet(sFlat4,X1),
inference(step,[status(thm)],[t95988,t68]) ).
cnf(t95990,plain,
meet(a,meet(join(sFlat0,meet(c,sFlat1)),X1)) = meet(sFlat4,X1),
inference(step,[status(thm)],[t95989,t87]) ).
cnf(t95991,plain,
meet(a,meet(join(sFlat0,meet(sFlat1,c)),X1)) = meet(sFlat4,X1),
inference(step,[status(thm)],[t95990,t23]) ).
cnf(t95992,plain,
meet(a,meet(join(sFlat0,sFlat2),X1)) = meet(sFlat4,X1),
inference(step,[status(thm)],[t95991,t166]) ).
cnf(t95993,plain,
meet(a,meet(sFlat3,X1)) = meet(sFlat4,X1),
inference(step,[status(thm)],[t95992,t187]) ).
cnf(t30,plain,
meet(X1,meet(X2,X3)) = meet(meet(X2,X1),X3),
inference(cp,[status(thm)],[t24,t23]) ).
cnf(t95616,plain,
meet(X1,meet(X2,X3)) = meet(X2,meet(X1,X3)),
inference(step,[status(thm)],[t30,t24]) ).
cnf(t320,plain,
meet(X1,meet(X2,X3)) = meet(X2,meet(X1,X3)),
inference(orient,[status(thm)],[t95616]) ).
cnf(t95994,plain,
meet(sFlat3,meet(a,X1)) = meet(sFlat4,X1),
inference(step,[status(thm)],[t95993,t320]) ).
cnf(t7699,plain,
meet(sFlat3,meet(a,X1)) = meet(sFlat4,X1),
inference(orient,[status(thm)],[t95994]) ).
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(t7717,plain,
meet(sFlat4,a) = meet(sFlat3,a),
inference(cp,[status(thm)],[t7699,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(t46,plain,
a = join(a,sFlat4),
inference(cp,[status(thm)],[t22,t44]) ).
cnf(t95584,plain,
a = join(sFlat4,a),
inference(step,[status(thm)],[t46,t68]) ).
cnf(t101,plain,
join(sFlat4,a) = a,
inference(orient,[status(thm)],[t95584]) ).
cnf(t102,plain,
sFlat4 = meet(sFlat4,a),
inference(cp,[status(thm)],[t20,t101]) ).
cnf(t135,plain,
meet(sFlat4,a) = sFlat4,
inference(orient,[status(thm)],[t102]) ).
cnf(t95998,plain,
sFlat4 = meet(sFlat3,a),
inference(step,[status(thm)],[t7717,t135]) ).
cnf(t7766,plain,
meet(sFlat3,a) = sFlat4,
inference(orient,[status(thm)],[t95998]) ).
cnf(t14,axiom,
sFlat5 = join(b,meet(a,join(meet(a,b),meet(c,join(a,b))))),
introduced(definition) ).
cnf(t95576,plain,
sFlat5 = join(b,meet(a,join(meet(b,a),meet(c,join(a,b))))),
inference(step,[status(thm)],[t14,t23]) ).
cnf(t95577,plain,
sFlat5 = join(b,meet(a,join(sFlat0,meet(c,join(a,b))))),
inference(step,[status(thm)],[t95576,t56]) ).
cnf(t95578,plain,
sFlat5 = join(b,meet(a,join(sFlat0,meet(c,join(b,a))))),
inference(step,[status(thm)],[t95577,t68]) ).
cnf(t95579,plain,
sFlat5 = join(b,meet(a,join(sFlat0,meet(c,sFlat1)))),
inference(step,[status(thm)],[t95578,t87]) ).
cnf(t95580,plain,
sFlat5 = join(b,meet(a,join(sFlat0,meet(sFlat1,c)))),
inference(step,[status(thm)],[t95579,t23]) ).
cnf(t92,plain,
join(b,meet(a,join(sFlat0,meet(sFlat1,c)))) = sFlat5,
inference(orient,[status(thm)],[t95580]) ).
cnf(t95599,plain,
join(b,meet(a,join(sFlat0,sFlat2))) = sFlat5,
inference(step,[status(thm)],[t92,t166]) ).
cnf(t170,plain,
join(b,meet(a,join(sFlat0,sFlat2))) = sFlat5,
inference(rw,[status(thm)],[t95599]) ).
cnf(t95813,plain,
join(b,meet(a,sFlat3)) = sFlat5,
inference(step,[status(thm)],[t170,t187]) ).
cnf(t95814,plain,
join(b,meet(sFlat3,a)) = sFlat5,
inference(step,[status(thm)],[t95813,t23]) ).
cnf(t2866,plain,
join(b,meet(sFlat3,a)) = sFlat5,
inference(orient,[status(thm)],[t95814]) ).
cnf(t96005,plain,
join(b,sFlat4) = sFlat5,
inference(step,[status(thm)],[t2866,t7766]) ).
cnf(t7787,plain,
join(b,sFlat4) = sFlat5,
inference(rw,[status(thm)],[t96005]) ).
cnf(t96021,plain,
join(sFlat4,b) = sFlat5,
inference(step,[status(thm)],[t7787,t68]) ).
cnf(t7846,plain,
join(sFlat4,b) = sFlat5,
inference(orient,[status(thm)],[t96021]) ).
cnf(t15,axiom,
sFlat6 = meet(a,join(b,meet(a,join(meet(a,b),meet(c,join(a,b)))))),
introduced(definition) ).
cnf(t95564,plain,
sFlat6 = meet(a,join(b,meet(a,join(meet(b,a),meet(c,join(a,b)))))),
inference(step,[status(thm)],[t15,t23]) ).
cnf(t95565,plain,
sFlat6 = meet(a,join(b,sFlat4)),
inference(step,[status(thm)],[t95564,t44]) ).
cnf(t48,plain,
meet(a,join(b,sFlat4)) = sFlat6,
inference(orient,[status(thm)],[t95565]) ).
cnf(t70,plain,
meet(a,join(b,sFlat4)) = sFlat6,
inference(rw,[status(thm)],[t48]) ).
cnf(t95601,plain,
meet(a,join(sFlat4,b)) = sFlat6,
inference(step,[status(thm)],[t70,t68]) ).
cnf(t177,plain,
meet(a,join(sFlat4,b)) = sFlat6,
inference(orient,[status(thm)],[t95601]) ).
cnf(t96029,plain,
meet(a,sFlat5) = sFlat6,
inference(step,[status(thm)],[t177,t7846]) ).
cnf(t7872,plain,
meet(a,sFlat5) = sFlat6,
inference(rw,[status(thm)],[t96029]) ).
cnf(t96092,plain,
meet(sFlat5,a) = sFlat6,
inference(step,[status(thm)],[t7872,t23]) ).
cnf(t8085,plain,
meet(sFlat5,a) = sFlat6,
inference(orient,[status(thm)],[t96092]) ).
cnf(t16,axiom,
sFlat7 = meet(a,c),
introduced(definition) ).
cnf(t95569,plain,
sFlat7 = meet(c,a),
inference(step,[status(thm)],[t16,t23]) ).
cnf(t60,plain,
meet(c,a) = sFlat7,
inference(orient,[status(thm)],[t95569]) ).
cnf(t17,axiom,
sFlat8 = join(b,meet(a,c)),
introduced(definition) ).
cnf(t95581,plain,
sFlat8 = join(b,meet(c,a)),
inference(step,[status(thm)],[t17,t23]) ).
cnf(t95582,plain,
sFlat8 = join(b,sFlat7),
inference(step,[status(thm)],[t95581,t60]) ).
cnf(t95583,plain,
sFlat8 = join(sFlat7,b),
inference(step,[status(thm)],[t95582,t68]) ).
cnf(t97,plain,
join(sFlat7,b) = sFlat8,
inference(orient,[status(thm)],[t95583]) ).
cnf(t18,axiom,
sFlat9 = meet(a,join(b,meet(a,c))),
introduced(definition) ).
cnf(t95566,plain,
sFlat9 = meet(a,join(b,meet(c,a))),
inference(step,[status(thm)],[t18,t23]) ).
cnf(t52,plain,
meet(a,join(b,meet(c,a))) = sFlat9,
inference(orient,[status(thm)],[t95566]) ).
cnf(t95570,plain,
meet(a,join(b,sFlat7)) = sFlat9,
inference(step,[status(thm)],[t52,t60]) ).
cnf(t63,plain,
meet(a,join(b,sFlat7)) = sFlat9,
inference(rw,[status(thm)],[t95570]) ).
cnf(t95592,plain,
meet(a,join(sFlat7,b)) = sFlat9,
inference(step,[status(thm)],[t63,t68]) ).
cnf(t95593,plain,
meet(a,sFlat8) = sFlat9,
inference(step,[status(thm)],[t95592,t97]) ).
cnf(t95594,plain,
meet(sFlat8,a) = sFlat9,
inference(step,[status(thm)],[t95593,t23]) ).
cnf(t156,plain,
meet(sFlat8,a) = sFlat9,
inference(orient,[status(thm)],[t95594]) ).
cnf(t50,plain,
a = join(a,sFlat6),
inference(cp,[status(thm)],[t22,t48]) ).
cnf(t95585,plain,
a = join(sFlat6,a),
inference(step,[status(thm)],[t50,t68]) ).
cnf(t105,plain,
join(sFlat6,a) = a,
inference(orient,[status(thm)],[t95585]) ).
cnf(t106,plain,
sFlat6 = meet(sFlat6,a),
inference(cp,[status(thm)],[t20,t105]) ).
cnf(t137,plain,
meet(sFlat6,a) = sFlat6,
inference(orient,[status(thm)],[t106]) ).
cnf(t138,plain,
meet(sFlat6,meet(a,X1)) = meet(sFlat6,X1),
inference(cp,[status(thm)],[t24,t137]) ).
cnf(t687,plain,
meet(sFlat6,meet(a,X1)) = meet(sFlat6,X1),
inference(orient,[status(thm)],[t138]) ).
cnf(t8,axiom,
meet(X1,join(X2,meet(X3,join(X4,meet(X3,join(X1,X2)))))) = 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(X4,meet(X3,join(X1,X2)))))) = meet(X1,join(X2,meet(X3,join(X1,X4)))),
inference(orient,[status(thm)],[t8]) ).
cnf(t67,plain,
meet(a,join(b,meet(c,join(a,X1)))) = meet(a,join(b,meet(c,join(X1,sFlat2)))),
inference(cp,[status(thm)],[t32,t64]) ).
cnf(t10256,plain,
meet(a,join(b,meet(c,join(a,X1)))) = meet(a,join(b,meet(c,join(X1,sFlat2)))),
inference(orient,[status(thm)],[t67]) ).
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(t10258,plain,
meet(a,join(b,meet(c,join(a,sFlat2)))) = meet(a,join(b,meet(c,a))),
inference(cp,[status(thm)],[t10256,t21]) ).
cnf(t98109,plain,
meet(a,join(b,meet(c,join(sFlat2,sFlat2)))) = meet(a,join(b,meet(c,a))),
inference(step,[status(thm)],[t10258,t10256]) ).
cnf(t98110,plain,
meet(a,join(b,meet(c,sFlat2))) = meet(a,join(b,meet(c,a))),
inference(step,[status(thm)],[t98109,t21]) ).
cnf(t98111,plain,
meet(a,join(b,meet(sFlat2,c))) = meet(a,join(b,meet(c,a))),
inference(step,[status(thm)],[t98110,t23]) ).
cnf(t66,plain,
c = join(c,sFlat2),
inference(cp,[status(thm)],[t22,t64]) ).
cnf(t95589,plain,
c = join(sFlat2,c),
inference(step,[status(thm)],[t66,t68]) ).
cnf(t121,plain,
join(sFlat2,c) = c,
inference(orient,[status(thm)],[t95589]) ).
cnf(t122,plain,
sFlat2 = meet(sFlat2,c),
inference(cp,[status(thm)],[t20,t121]) ).
cnf(t145,plain,
meet(sFlat2,c) = sFlat2,
inference(orient,[status(thm)],[t122]) ).
cnf(t98112,plain,
meet(a,join(b,sFlat2)) = meet(a,join(b,meet(c,a))),
inference(step,[status(thm)],[t98111,t145]) ).
cnf(t98113,plain,
meet(a,join(sFlat2,b)) = meet(a,join(b,meet(c,a))),
inference(step,[status(thm)],[t98112,t68]) ).
cnf(t31,plain,
meet(X1,X2) = join(meet(X1,X2),meet(X1,meet(X2,X3))),
inference(cp,[status(thm)],[t22,t24]) ).
cnf(t918,plain,
join(meet(X1,X2),meet(X1,meet(X2,X3))) = meet(X1,X2),
inference(orient,[status(thm)],[t31]) ).
cnf(t27,plain,
meet(X1,meet(X2,X3)) = meet(X3,meet(X1,X2)),
inference(cp,[status(thm)],[t24,t23]) ).
cnf(t310,plain,
meet(X1,meet(X2,X3)) = meet(X3,meet(X1,X2)),
inference(orient,[status(thm)],[t27]) ).
cnf(t948,plain,
meet(X1,X2) = join(meet(X1,X2),meet(X2,meet(X3,X1))),
inference(cp,[status(thm)],[t918,t310]) ).
cnf(t13689,plain,
join(meet(X1,X2),meet(X2,meet(X3,X1))) = meet(X1,X2),
inference(orient,[status(thm)],[t948]) ).
cnf(t146,plain,
meet(sFlat2,meet(c,X1)) = meet(sFlat2,X1),
inference(cp,[status(thm)],[t24,t145]) ).
cnf(t703,plain,
meet(sFlat2,meet(c,X1)) = meet(sFlat2,X1),
inference(orient,[status(thm)],[t146]) ).
cnf(t61,plain,
meet(c,meet(a,X1)) = meet(sFlat7,X1),
inference(cp,[status(thm)],[t24,t60]) ).
cnf(t214,plain,
meet(c,meet(a,X1)) = meet(sFlat7,X1),
inference(orient,[status(thm)],[t61]) ).
cnf(t221,plain,
meet(sFlat7,X1) = meet(c,meet(X1,a)),
inference(cp,[status(thm)],[t214,t23]) ).
cnf(t423,plain,
meet(c,meet(X1,a)) = meet(sFlat7,X1),
inference(orient,[status(thm)],[t221]) ).
cnf(t706,plain,
meet(sFlat2,meet(X1,a)) = meet(sFlat2,meet(sFlat7,X1)),
inference(cp,[status(thm)],[t703,t423]) ).
cnf(t1747,plain,
meet(sFlat2,meet(X1,a)) = meet(sFlat2,meet(sFlat7,X1)),
inference(orient,[status(thm)],[t706]) ).
cnf(t29,plain,
meet(X1,meet(join(X1,X2),X3)) = meet(X1,X3),
inference(cp,[status(thm)],[t24,t20]) ).
cnf(t709,plain,
meet(X1,meet(join(X1,X2),X3)) = meet(X1,X3),
inference(orient,[status(thm)],[t29]) ).
cnf(t1748,plain,
meet(sFlat2,meet(sFlat7,join(sFlat2,X1))) = meet(sFlat2,a),
inference(cp,[status(thm)],[t1747,t709]) ).
cnf(t168,plain,
meet(sFlat1,meet(c,X1)) = meet(sFlat2,X1),
inference(cp,[status(thm)],[t24,t166]) ).
cnf(t742,plain,
meet(sFlat1,meet(c,X1)) = meet(sFlat2,X1),
inference(orient,[status(thm)],[t168]) ).
cnf(t744,plain,
meet(sFlat2,meet(a,X1)) = meet(sFlat1,meet(sFlat7,X1)),
inference(cp,[status(thm)],[t742,t214]) ).
cnf(t705,plain,
meet(sFlat2,meet(a,X1)) = meet(sFlat2,meet(sFlat7,X1)),
inference(cp,[status(thm)],[t703,t214]) ).
cnf(t1736,plain,
meet(sFlat2,meet(a,X1)) = meet(sFlat2,meet(sFlat7,X1)),
inference(orient,[status(thm)],[t705]) ).
cnf(t95744,plain,
meet(sFlat2,meet(sFlat7,X1)) = meet(sFlat1,meet(sFlat7,X1)),
inference(step,[status(thm)],[t744,t1736]) ).
cnf(t1785,plain,
meet(sFlat2,meet(sFlat7,X1)) = meet(sFlat1,meet(sFlat7,X1)),
inference(orient,[status(thm)],[t95744]) ).
cnf(t96199,plain,
meet(sFlat1,meet(sFlat7,join(sFlat2,X1))) = meet(sFlat2,a),
inference(step,[status(thm)],[t1748,t1785]) ).
cnf(t704,plain,
meet(sFlat2,a) = meet(sFlat2,sFlat7),
inference(cp,[status(thm)],[t703,t60]) ).
cnf(t722,plain,
meet(sFlat2,a) = meet(sFlat2,sFlat7),
inference(orient,[status(thm)],[t704]) ).
cnf(t743,plain,
meet(sFlat2,a) = meet(sFlat1,sFlat7),
inference(cp,[status(thm)],[t742,t60]) ).
cnf(t95670,plain,
meet(sFlat2,sFlat7) = meet(sFlat1,sFlat7),
inference(step,[status(thm)],[t743,t722]) ).
cnf(t219,plain,
meet(sFlat7,join(a,X1)) = meet(c,a),
inference(cp,[status(thm)],[t214,t20]) ).
cnf(t95612,plain,
meet(sFlat7,join(a,X1)) = sFlat7,
inference(step,[status(thm)],[t219,t60]) ).
cnf(t267,plain,
meet(sFlat7,join(a,X1)) = sFlat7,
inference(orient,[status(thm)],[t95612]) ).
cnf(t268,plain,
sFlat7 = meet(sFlat7,join(X1,a)),
inference(cp,[status(thm)],[t267,t68]) ).
cnf(t538,plain,
meet(sFlat7,join(X1,a)) = sFlat7,
inference(orient,[status(thm)],[t268]) ).
cnf(t6,axiom,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t71,plain,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
inference(orient,[status(thm)],[t6]) ).
cnf(t89,plain,
join(b,join(a,X1)) = join(sFlat1,X1),
inference(cp,[status(thm)],[t71,t87]) ).
cnf(t227,plain,
join(b,join(a,X1)) = join(sFlat1,X1),
inference(orient,[status(thm)],[t89]) ).
cnf(t228,plain,
join(sFlat1,a) = join(b,a),
inference(cp,[status(thm)],[t227,t21]) ).
cnf(t95608,plain,
join(sFlat1,a) = sFlat1,
inference(step,[status(thm)],[t228,t87]) ).
cnf(t235,plain,
join(sFlat1,a) = sFlat1,
inference(orient,[status(thm)],[t95608]) ).
cnf(t540,plain,
sFlat7 = meet(sFlat7,sFlat1),
inference(cp,[status(thm)],[t538,t235]) ).
cnf(t95653,plain,
sFlat7 = meet(sFlat1,sFlat7),
inference(step,[status(thm)],[t540,t23]) ).
cnf(t545,plain,
meet(sFlat1,sFlat7) = sFlat7,
inference(orient,[status(thm)],[t95653]) ).
cnf(t95671,plain,
meet(sFlat2,sFlat7) = sFlat7,
inference(step,[status(thm)],[t95670,t545]) ).
cnf(t749,plain,
meet(sFlat2,sFlat7) = sFlat7,
inference(orient,[status(thm)],[t95671]) ).
cnf(t95672,plain,
meet(sFlat2,a) = sFlat7,
inference(step,[status(thm)],[t722,t749]) ).
cnf(t750,plain,
meet(sFlat2,a) = sFlat7,
inference(orient,[status(thm)],[t95672]) ).
cnf(t96200,plain,
meet(sFlat1,meet(sFlat7,join(sFlat2,X1))) = sFlat7,
inference(step,[status(thm)],[t96199,t750]) ).
cnf(t9807,plain,
meet(sFlat1,meet(sFlat7,join(sFlat2,X1))) = sFlat7,
inference(orient,[status(thm)],[t96200]) ).
cnf(t13736,plain,
meet(join(sFlat2,X1),sFlat1) = join(meet(join(sFlat2,X1),sFlat1),sFlat7),
inference(cp,[status(thm)],[t13689,t9807]) ).
cnf(t96290,plain,
meet(sFlat1,join(sFlat2,X1)) = join(meet(join(sFlat2,X1),sFlat1),sFlat7),
inference(step,[status(thm)],[t13736,t23]) ).
cnf(t96291,plain,
meet(sFlat1,join(sFlat2,X1)) = join(sFlat7,meet(join(sFlat2,X1),sFlat1)),
inference(step,[status(thm)],[t96290,t68]) ).
cnf(t96292,plain,
meet(sFlat1,join(sFlat2,X1)) = join(sFlat7,meet(sFlat1,join(sFlat2,X1))),
inference(step,[status(thm)],[t96291,t23]) ).
cnf(t14950,plain,
join(sFlat7,meet(sFlat1,join(sFlat2,X1))) = meet(sFlat1,join(sFlat2,X1)),
inference(orient,[status(thm)],[t96292]) ).
cnf(t74,plain,
join(X1,join(X2,X3)) = join(X3,join(X1,X2)),
inference(cp,[status(thm)],[t71,t68]) ).
cnf(t325,plain,
join(X1,join(X2,X3)) = join(X3,join(X1,X2)),
inference(orient,[status(thm)],[t74]) ).
cnf(t331,plain,
X1 = meet(X1,join(X2,join(X3,X1))),
inference(cp,[status(thm)],[t20,t325]) ).
cnf(t1282,plain,
meet(X1,join(X2,join(X3,X1))) = X1,
inference(orient,[status(thm)],[t331]) ).
cnf(t75,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(cp,[status(thm)],[t71,t21]) ).
cnf(t180,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(orient,[status(thm)],[t75]) ).
cnf(t1284,plain,
X1 = meet(X1,join(X2,X1)),
inference(cp,[status(thm)],[t1282,t180]) ).
cnf(t1400,plain,
meet(X1,join(X2,X1)) = X1,
inference(orient,[status(thm)],[t1284]) ).
cnf(t233,plain,
join(b,join(a,X1)) = join(b,join(sFlat1,X1)),
inference(cp,[status(thm)],[t180,t227]) ).
cnf(t95644,plain,
join(sFlat1,X1) = join(b,join(sFlat1,X1)),
inference(step,[status(thm)],[t233,t227]) ).
cnf(t77,plain,
join(X1,join(X2,X3)) = join(join(X2,X1),X3),
inference(cp,[status(thm)],[t71,t68]) ).
cnf(t95617,plain,
join(X1,join(X2,X3)) = join(X2,join(X1,X3)),
inference(step,[status(thm)],[t77,t71]) ).
cnf(t337,plain,
join(X1,join(X2,X3)) = join(X2,join(X1,X3)),
inference(orient,[status(thm)],[t95617]) ).
cnf(t95645,plain,
join(sFlat1,X1) = join(sFlat1,join(b,X1)),
inference(step,[status(thm)],[t95644,t337]) ).
cnf(t495,plain,
join(sFlat1,join(b,X1)) = join(sFlat1,X1),
inference(orient,[status(thm)],[t95645]) ).
cnf(t1420,plain,
join(b,X1) = meet(join(b,X1),join(sFlat1,X1)),
inference(cp,[status(thm)],[t1400,t495]) ).
cnf(t95916,plain,
join(b,X1) = meet(join(sFlat1,X1),join(b,X1)),
inference(step,[status(thm)],[t1420,t23]) ).
cnf(t5570,plain,
meet(join(sFlat1,X1),join(b,X1)) = join(b,X1),
inference(orient,[status(thm)],[t95916]) ).
cnf(t169,plain,
sFlat1 = join(sFlat1,sFlat2),
inference(cp,[status(thm)],[t22,t166]) ).
cnf(t174,plain,
join(sFlat1,sFlat2) = sFlat1,
inference(orient,[status(thm)],[t169]) ).
cnf(t5604,plain,
join(b,sFlat2) = meet(sFlat1,join(b,sFlat2)),
inference(cp,[status(thm)],[t5570,t174]) ).
cnf(t95923,plain,
join(sFlat2,b) = meet(sFlat1,join(b,sFlat2)),
inference(step,[status(thm)],[t5604,t68]) ).
cnf(t95924,plain,
join(sFlat2,b) = meet(sFlat1,join(sFlat2,b)),
inference(step,[status(thm)],[t95923,t68]) ).
cnf(t5666,plain,
meet(sFlat1,join(sFlat2,b)) = join(sFlat2,b),
inference(orient,[status(thm)],[t95924]) ).
cnf(t14951,plain,
meet(sFlat1,join(sFlat2,b)) = join(sFlat7,join(sFlat2,b)),
inference(cp,[status(thm)],[t14950,t5666]) ).
cnf(t96293,plain,
join(sFlat2,b) = join(sFlat7,join(sFlat2,b)),
inference(step,[status(thm)],[t14951,t5666]) ).
cnf(t99,plain,
join(sFlat7,join(b,X1)) = join(sFlat8,X1),
inference(cp,[status(thm)],[t71,t97]) ).
cnf(t238,plain,
join(sFlat7,join(b,X1)) = join(sFlat8,X1),
inference(orient,[status(thm)],[t99]) ).
cnf(t244,plain,
join(sFlat8,X1) = join(sFlat7,join(X1,b)),
inference(cp,[status(thm)],[t238,t68]) ).
cnf(t507,plain,
join(sFlat7,join(X1,b)) = join(sFlat8,X1),
inference(orient,[status(thm)],[t244]) ).
cnf(t96294,plain,
join(sFlat2,b) = join(sFlat8,sFlat2),
inference(step,[status(thm)],[t96293,t507]) ).
cnf(t96295,plain,
join(sFlat2,b) = join(sFlat2,sFlat8),
inference(step,[status(thm)],[t96294,t68]) ).
cnf(t14980,plain,
join(sFlat2,b) = join(sFlat2,sFlat8),
inference(orient,[status(thm)],[t96295]) ).
cnf(t58,plain,
b = join(b,sFlat0),
inference(cp,[status(thm)],[t22,t56]) ).
cnf(t95587,plain,
b = join(sFlat0,b),
inference(step,[status(thm)],[t58,t68]) ).
cnf(t113,plain,
join(sFlat0,b) = b,
inference(orient,[status(thm)],[t95587]) ).
cnf(t115,plain,
join(sFlat0,join(b,X1)) = join(b,X1),
inference(cp,[status(thm)],[t71,t113]) ).
cnf(t352,plain,
join(sFlat0,join(b,X1)) = join(b,X1),
inference(orient,[status(thm)],[t115]) ).
cnf(t353,plain,
join(b,a) = join(sFlat0,sFlat1),
inference(cp,[status(thm)],[t352,t87]) ).
cnf(t95618,plain,
sFlat1 = join(sFlat0,sFlat1),
inference(step,[status(thm)],[t353,t87]) ).
cnf(t357,plain,
join(sFlat0,sFlat1) = sFlat1,
inference(orient,[status(thm)],[t95618]) ).
cnf(t358,plain,
sFlat0 = meet(sFlat0,sFlat1),
inference(cp,[status(thm)],[t20,t357]) ).
cnf(t360,plain,
meet(sFlat0,sFlat1) = sFlat0,
inference(orient,[status(thm)],[t358]) ).
cnf(t14001,plain,
meet(sFlat1,X1) = join(meet(sFlat1,X1),meet(X1,sFlat0)),
inference(cp,[status(thm)],[t13689,t360]) ).
cnf(t14228,plain,
join(meet(sFlat1,X1),meet(X1,sFlat0)) = meet(sFlat1,X1),
inference(orient,[status(thm)],[t14001]) ).
cnf(t14251,plain,
meet(sFlat1,X1) = join(meet(sFlat1,X1),meet(sFlat0,X1)),
inference(cp,[status(thm)],[t14228,t23]) ).
cnf(t96303,plain,
meet(sFlat1,X1) = join(meet(sFlat0,X1),meet(sFlat1,X1)),
inference(step,[status(thm)],[t14251,t68]) ).
cnf(t15268,plain,
join(meet(sFlat0,X1),meet(sFlat1,X1)) = meet(sFlat1,X1),
inference(orient,[status(thm)],[t96303]) ).
cnf(t175,plain,
join(sFlat1,join(sFlat2,X1)) = join(sFlat1,X1),
inference(cp,[status(thm)],[t71,t174]) ).
cnf(t989,plain,
join(sFlat1,join(sFlat2,X1)) = join(sFlat1,X1),
inference(orient,[status(thm)],[t175]) ).
cnf(t1418,plain,
join(sFlat2,X1) = meet(join(sFlat2,X1),join(sFlat1,X1)),
inference(cp,[status(thm)],[t1400,t989]) ).
cnf(t96239,plain,
join(sFlat2,X1) = meet(join(sFlat1,X1),join(sFlat2,X1)),
inference(step,[status(thm)],[t1418,t23]) ).
cnf(t10619,plain,
meet(join(sFlat1,X1),join(sFlat2,X1)) = join(sFlat2,X1),
inference(orient,[status(thm)],[t96239]) ).
cnf(t242,plain,
join(sFlat8,join(b,X1)) = join(sFlat7,join(b,X1)),
inference(cp,[status(thm)],[t238,t180]) ).
cnf(t95646,plain,
join(sFlat8,join(b,X1)) = join(sFlat8,X1),
inference(step,[status(thm)],[t242,t238]) ).
cnf(t499,plain,
join(sFlat8,join(b,X1)) = join(sFlat8,X1),
inference(orient,[status(thm)],[t95646]) ).
cnf(t501,plain,
join(sFlat8,a) = join(sFlat8,sFlat1),
inference(cp,[status(thm)],[t499,t87]) ).
cnf(t239,plain,
join(sFlat8,a) = join(sFlat7,sFlat1),
inference(cp,[status(thm)],[t238,t87]) ).
cnf(t95610,plain,
join(sFlat8,a) = join(sFlat1,sFlat7),
inference(step,[status(thm)],[t239,t68]) ).
cnf(t251,plain,
join(sFlat8,a) = join(sFlat1,sFlat7),
inference(orient,[status(thm)],[t95610]) ).
cnf(t95647,plain,
join(sFlat1,sFlat7) = join(sFlat8,sFlat1),
inference(step,[status(thm)],[t501,t251]) ).
cnf(t95648,plain,
join(sFlat1,sFlat7) = join(sFlat1,sFlat8),
inference(step,[status(thm)],[t95647,t68]) ).
cnf(t505,plain,
join(sFlat1,sFlat8) = join(sFlat1,sFlat7),
inference(orient,[status(thm)],[t95648]) ).
cnf(t546,plain,
sFlat1 = join(sFlat1,sFlat7),
inference(cp,[status(thm)],[t22,t545]) ).
cnf(t547,plain,
join(sFlat1,sFlat7) = sFlat1,
inference(orient,[status(thm)],[t546]) ).
cnf(t95656,plain,
join(sFlat1,sFlat8) = sFlat1,
inference(step,[status(thm)],[t505,t547]) ).
cnf(t550,plain,
join(sFlat1,sFlat8) = sFlat1,
inference(orient,[status(thm)],[t95656]) ).
cnf(t10654,plain,
join(sFlat2,sFlat8) = meet(sFlat1,join(sFlat2,sFlat8)),
inference(cp,[status(thm)],[t10619,t550]) ).
cnf(t10693,plain,
meet(sFlat1,join(sFlat2,sFlat8)) = join(sFlat2,sFlat8),
inference(orient,[status(thm)],[t10654]) ).
cnf(t15333,plain,
meet(sFlat1,join(sFlat2,sFlat8)) = join(meet(sFlat0,join(sFlat2,sFlat8)),join(sFlat2,sFlat8)),
inference(cp,[status(thm)],[t15268,t10693]) ).
cnf(t96304,plain,
join(sFlat2,sFlat8) = join(meet(sFlat0,join(sFlat2,sFlat8)),join(sFlat2,sFlat8)),
inference(step,[status(thm)],[t15333,t10693]) ).
cnf(t114,plain,
sFlat0 = meet(sFlat0,b),
inference(cp,[status(thm)],[t20,t113]) ).
cnf(t141,plain,
meet(sFlat0,b) = sFlat0,
inference(orient,[status(thm)],[t114]) ).
cnf(t142,plain,
meet(sFlat0,meet(b,X1)) = meet(sFlat0,X1),
inference(cp,[status(thm)],[t24,t141]) ).
cnf(t695,plain,
meet(sFlat0,meet(b,X1)) = meet(sFlat0,X1),
inference(orient,[status(thm)],[t142]) ).
cnf(t241,plain,
join(sFlat8,b) = join(sFlat7,b),
inference(cp,[status(thm)],[t238,t21]) ).
cnf(t95609,plain,
join(sFlat8,b) = sFlat8,
inference(step,[status(thm)],[t241,t97]) ).
cnf(t248,plain,
join(sFlat8,b) = sFlat8,
inference(orient,[status(thm)],[t95609]) ).
cnf(t1311,plain,
b = meet(b,join(X1,sFlat8)),
inference(cp,[status(thm)],[t1282,t248]) ).
cnf(t1593,plain,
meet(b,join(X1,sFlat8)) = b,
inference(orient,[status(thm)],[t1311]) ).
cnf(t1596,plain,
meet(sFlat0,join(X1,sFlat8)) = meet(sFlat0,b),
inference(cp,[status(thm)],[t695,t1593]) ).
cnf(t95725,plain,
meet(sFlat0,join(X1,sFlat8)) = sFlat0,
inference(step,[status(thm)],[t1596,t141]) ).
cnf(t1655,plain,
meet(sFlat0,join(X1,sFlat8)) = sFlat0,
inference(orient,[status(thm)],[t95725]) ).
cnf(t96305,plain,
join(sFlat2,sFlat8) = join(sFlat0,join(sFlat2,sFlat8)),
inference(step,[status(thm)],[t96304,t1655]) ).
cnf(t189,plain,
join(sFlat0,join(sFlat2,X1)) = join(sFlat3,X1),
inference(cp,[status(thm)],[t71,t187]) ).
cnf(t386,plain,
join(sFlat0,join(sFlat2,X1)) = join(sFlat3,X1),
inference(orient,[status(thm)],[t189]) ).
cnf(t96306,plain,
join(sFlat2,sFlat8) = join(sFlat3,sFlat8),
inference(step,[status(thm)],[t96305,t386]) ).
cnf(t76,plain,
join(X1,join(meet(X1,X2),X3)) = join(X1,X3),
inference(cp,[status(thm)],[t71,t22]) ).
cnf(t1012,plain,
join(X1,join(meet(X1,X2),X3)) = join(X1,X3),
inference(orient,[status(thm)],[t76]) ).
cnf(t7714,plain,
meet(sFlat4,join(sFlat4,b)) = meet(sFlat3,sFlat6),
inference(cp,[status(thm)],[t7699,t177]) ).
cnf(t95995,plain,
sFlat4 = meet(sFlat3,sFlat6),
inference(step,[status(thm)],[t7714,t20]) ).
cnf(t7749,plain,
meet(sFlat3,sFlat6) = sFlat4,
inference(orient,[status(thm)],[t95995]) ).
cnf(t7759,plain,
join(sFlat3,X1) = join(sFlat3,join(sFlat4,X1)),
inference(cp,[status(thm)],[t1012,t7749]) ).
cnf(t8379,plain,
join(sFlat3,join(sFlat4,X1)) = join(sFlat3,X1),
inference(orient,[status(thm)],[t7759]) ).
cnf(t8088,plain,
meet(sFlat7,sFlat5) = meet(c,sFlat6),
inference(cp,[status(thm)],[t423,t8085]) ).
cnf(t96093,plain,
meet(sFlat5,sFlat7) = meet(c,sFlat6),
inference(step,[status(thm)],[t8088,t23]) ).
cnf(t96094,plain,
meet(sFlat5,sFlat7) = meet(sFlat6,c),
inference(step,[status(thm)],[t96093,t23]) ).
cnf(t426,plain,
meet(sFlat7,sFlat6) = meet(c,sFlat6),
inference(cp,[status(thm)],[t423,t137]) ).
cnf(t95636,plain,
meet(sFlat6,sFlat7) = meet(c,sFlat6),
inference(step,[status(thm)],[t426,t23]) ).
cnf(t95637,plain,
meet(sFlat6,sFlat7) = meet(sFlat6,c),
inference(step,[status(thm)],[t95636,t23]) ).
cnf(t479,plain,
meet(sFlat6,c) = meet(sFlat6,sFlat7),
inference(orient,[status(thm)],[t95637]) ).
cnf(t713,plain,
meet(X1,X2) = meet(X1,meet(X2,join(X1,X3))),
inference(cp,[status(thm)],[t709,t23]) ).
cnf(t1811,plain,
meet(X1,meet(X2,join(X1,X3))) = meet(X1,X2),
inference(orient,[status(thm)],[t713]) ).
cnf(t95745,plain,
meet(sFlat2,meet(a,X1)) = meet(sFlat1,meet(sFlat7,X1)),
inference(step,[status(thm)],[t1736,t1785]) ).
cnf(t1786,plain,
meet(sFlat2,meet(a,X1)) = meet(sFlat1,meet(sFlat7,X1)),
inference(orient,[status(thm)],[t95745]) ).
cnf(t78,plain,
join(X1,X2) = meet(join(X1,X2),join(X1,join(X2,X3))),
inference(cp,[status(thm)],[t20,t71]) ).
cnf(t5879,plain,
meet(join(X1,X2),join(X1,join(X2,X3))) = join(X1,X2),
inference(orient,[status(thm)],[t78]) ).
cnf(t54,plain,
a = join(a,sFlat9),
inference(cp,[status(thm)],[t22,t52]) ).
cnf(t95586,plain,
a = join(sFlat9,a),
inference(step,[status(thm)],[t54,t68]) ).
cnf(t109,plain,
join(sFlat9,a) = a,
inference(orient,[status(thm)],[t95586]) ).
cnf(t5983,plain,
join(X1,sFlat9) = meet(join(X1,sFlat9),join(X1,a)),
inference(cp,[status(thm)],[t5879,t109]) ).
cnf(t6064,plain,
meet(join(X1,sFlat9),join(X1,a)) = join(X1,sFlat9),
inference(orient,[status(thm)],[t5983]) ).
cnf(t6068,plain,
join(sFlat6,sFlat9) = meet(join(sFlat6,sFlat9),a),
inference(cp,[status(thm)],[t6064,t105]) ).
cnf(t95928,plain,
join(sFlat6,sFlat9) = meet(a,join(sFlat6,sFlat9)),
inference(step,[status(thm)],[t6068,t23]) ).
cnf(t6079,plain,
meet(a,join(sFlat6,sFlat9)) = join(sFlat6,sFlat9),
inference(orient,[status(thm)],[t95928]) ).
cnf(t6082,plain,
meet(sFlat1,meet(sFlat7,join(sFlat6,sFlat9))) = meet(sFlat2,join(sFlat6,sFlat9)),
inference(cp,[status(thm)],[t1786,t6079]) ).
cnf(t1289,plain,
X1 = meet(X1,join(X2,join(X1,X3))),
inference(cp,[status(thm)],[t1282,t325]) ).
cnf(t1922,plain,
meet(X1,join(X2,join(X1,X3))) = X1,
inference(orient,[status(thm)],[t1289]) ).
cnf(t424,plain,
meet(sFlat7,sFlat8) = meet(c,sFlat9),
inference(cp,[status(thm)],[t423,t156]) ).
cnf(t98,plain,
sFlat7 = meet(sFlat7,sFlat8),
inference(cp,[status(thm)],[t20,t97]) ).
cnf(t133,plain,
meet(sFlat7,sFlat8) = sFlat7,
inference(orient,[status(thm)],[t98]) ).
cnf(t95634,plain,
sFlat7 = meet(c,sFlat9),
inference(step,[status(thm)],[t424,t133]) ).
cnf(t95635,plain,
sFlat7 = meet(sFlat9,c),
inference(step,[status(thm)],[t95634,t23]) ).
cnf(t476,plain,
meet(sFlat9,c) = sFlat7,
inference(orient,[status(thm)],[t95635]) ).
cnf(t477,plain,
sFlat9 = join(sFlat9,sFlat7),
inference(cp,[status(thm)],[t22,t476]) ).
cnf(t95640,plain,
sFlat9 = join(sFlat7,sFlat9),
inference(step,[status(thm)],[t477,t68]) ).
cnf(t483,plain,
join(sFlat7,sFlat9) = sFlat9,
inference(orient,[status(thm)],[t95640]) ).
cnf(t1950,plain,
sFlat7 = meet(sFlat7,join(X1,sFlat9)),
inference(cp,[status(thm)],[t1922,t483]) ).
cnf(t2210,plain,
meet(sFlat7,join(X1,sFlat9)) = sFlat7,
inference(orient,[status(thm)],[t1950]) ).
cnf(t95942,plain,
meet(sFlat1,sFlat7) = meet(sFlat2,join(sFlat6,sFlat9)),
inference(step,[status(thm)],[t6082,t2210]) ).
cnf(t95943,plain,
sFlat7 = meet(sFlat2,join(sFlat6,sFlat9)),
inference(step,[status(thm)],[t95942,t545]) ).
cnf(t7064,plain,
meet(sFlat2,join(sFlat6,sFlat9)) = sFlat7,
inference(orient,[status(thm)],[t95943]) ).
cnf(t7065,plain,
meet(sFlat6,sFlat2) = meet(sFlat6,sFlat7),
inference(cp,[status(thm)],[t1811,t7064]) ).
cnf(t95944,plain,
meet(sFlat2,sFlat6) = meet(sFlat6,sFlat7),
inference(step,[status(thm)],[t7065,t23]) ).
cnf(t7076,plain,
meet(sFlat6,sFlat7) = meet(sFlat2,sFlat6),
inference(orient,[status(thm)],[t95944]) ).
cnf(t95945,plain,
meet(sFlat6,c) = meet(sFlat2,sFlat6),
inference(step,[status(thm)],[t479,t7076]) ).
cnf(t7077,plain,
meet(sFlat6,c) = meet(sFlat2,sFlat6),
inference(orient,[status(thm)],[t95945]) ).
cnf(t319,plain,
X1 = join(X1,meet(X2,meet(X3,X1))),
inference(cp,[status(thm)],[t22,t310]) ).
cnf(t1057,plain,
join(X1,meet(X2,meet(X3,X1))) = X1,
inference(orient,[status(thm)],[t319]) ).
cnf(t136,plain,
meet(sFlat4,meet(a,X1)) = meet(sFlat4,X1),
inference(cp,[status(thm)],[t24,t135]) ).
cnf(t681,plain,
meet(sFlat4,meet(a,X1)) = meet(sFlat4,X1),
inference(orient,[status(thm)],[t136]) ).
cnf(t682,plain,
meet(sFlat4,join(sFlat4,b)) = meet(sFlat4,sFlat6),
inference(cp,[status(thm)],[t681,t177]) ).
cnf(t95668,plain,
sFlat4 = meet(sFlat4,sFlat6),
inference(step,[status(thm)],[t682,t20]) ).
cnf(t685,plain,
meet(sFlat4,sFlat6) = sFlat4,
inference(orient,[status(thm)],[t95668]) ).
cnf(t1094,plain,
sFlat6 = join(sFlat6,meet(X1,sFlat4)),
inference(cp,[status(thm)],[t1057,t685]) ).
cnf(t1251,plain,
join(sFlat6,meet(X1,sFlat4)) = sFlat6,
inference(orient,[status(thm)],[t1094]) ).
cnf(t7773,plain,
meet(sFlat7,sFlat3) = meet(c,sFlat4),
inference(cp,[status(thm)],[t423,t7766]) ).
cnf(t96043,plain,
meet(sFlat3,sFlat7) = meet(c,sFlat4),
inference(step,[status(thm)],[t7773,t23]) ).
cnf(t391,plain,
join(sFlat3,meet(sFlat2,X1)) = join(sFlat0,sFlat2),
inference(cp,[status(thm)],[t386,t22]) ).
cnf(t95660,plain,
join(sFlat3,meet(sFlat2,X1)) = sFlat3,
inference(step,[status(thm)],[t391,t187]) ).
cnf(t657,plain,
join(sFlat3,meet(sFlat2,X1)) = sFlat3,
inference(orient,[status(thm)],[t95660]) ).
cnf(t752,plain,
sFlat3 = join(sFlat3,sFlat7),
inference(cp,[status(thm)],[t657,t749]) ).
cnf(t754,plain,
join(sFlat3,sFlat7) = sFlat3,
inference(orient,[status(thm)],[t752]) ).
cnf(t1403,plain,
sFlat7 = meet(sFlat7,sFlat3),
inference(cp,[status(thm)],[t1400,t754]) ).
cnf(t95717,plain,
sFlat7 = meet(sFlat3,sFlat7),
inference(step,[status(thm)],[t1403,t23]) ).
cnf(t1437,plain,
meet(sFlat3,sFlat7) = sFlat7,
inference(orient,[status(thm)],[t95717]) ).
cnf(t96044,plain,
sFlat7 = meet(c,sFlat4),
inference(step,[status(thm)],[t96043,t1437]) ).
cnf(t96045,plain,
sFlat7 = meet(sFlat4,c),
inference(step,[status(thm)],[t96044,t23]) ).
cnf(t427,plain,
meet(sFlat7,sFlat4) = meet(c,sFlat4),
inference(cp,[status(thm)],[t423,t135]) ).
cnf(t95638,plain,
meet(sFlat4,sFlat7) = meet(c,sFlat4),
inference(step,[status(thm)],[t427,t23]) ).
cnf(t95639,plain,
meet(sFlat4,sFlat7) = meet(sFlat4,c),
inference(step,[status(thm)],[t95638,t23]) ).
cnf(t481,plain,
meet(sFlat4,c) = meet(sFlat4,sFlat7),
inference(orient,[status(thm)],[t95639]) ).
cnf(t215,plain,
meet(sFlat7,join(sFlat4,b)) = meet(c,sFlat6),
inference(cp,[status(thm)],[t214,t177]) ).
cnf(t95664,plain,
meet(sFlat7,join(sFlat4,b)) = meet(sFlat6,c),
inference(step,[status(thm)],[t215,t23]) ).
cnf(t95665,plain,
meet(sFlat7,join(sFlat4,b)) = meet(sFlat6,sFlat7),
inference(step,[status(thm)],[t95664,t479]) ).
cnf(t674,plain,
meet(sFlat7,join(sFlat4,b)) = meet(sFlat6,sFlat7),
inference(orient,[status(thm)],[t95665]) ).
cnf(t1815,plain,
meet(sFlat4,sFlat7) = meet(sFlat4,meet(sFlat6,sFlat7)),
inference(cp,[status(thm)],[t1811,t674]) ).
cnf(t1825,plain,
meet(sFlat4,meet(sFlat6,sFlat7)) = meet(sFlat4,sFlat7),
inference(orient,[status(thm)],[t1815]) ).
cnf(t95949,plain,
meet(sFlat4,meet(sFlat2,sFlat6)) = meet(sFlat4,sFlat7),
inference(step,[status(thm)],[t1825,t7076]) ).
cnf(t7091,plain,
meet(sFlat4,meet(sFlat2,sFlat6)) = meet(sFlat4,sFlat7),
inference(rw,[status(thm)],[t95949]) ).
cnf(t95950,plain,
meet(sFlat2,meet(sFlat4,sFlat6)) = meet(sFlat4,sFlat7),
inference(step,[status(thm)],[t7091,t320]) ).
cnf(t95951,plain,
meet(sFlat2,sFlat4) = meet(sFlat4,sFlat7),
inference(step,[status(thm)],[t95950,t685]) ).
cnf(t7092,plain,
meet(sFlat4,sFlat7) = meet(sFlat2,sFlat4),
inference(orient,[status(thm)],[t95951]) ).
cnf(t95952,plain,
meet(sFlat4,c) = meet(sFlat2,sFlat4),
inference(step,[status(thm)],[t481,t7092]) ).
cnf(t7093,plain,
meet(sFlat4,c) = meet(sFlat2,sFlat4),
inference(orient,[status(thm)],[t95952]) ).
cnf(t96046,plain,
sFlat7 = meet(sFlat2,sFlat4),
inference(step,[status(thm)],[t96045,t7093]) ).
cnf(t7935,plain,
meet(sFlat2,sFlat4) = sFlat7,
inference(orient,[status(thm)],[t96046]) ).
cnf(t7940,plain,
sFlat6 = join(sFlat6,sFlat7),
inference(cp,[status(thm)],[t1251,t7935]) ).
cnf(t7981,plain,
join(sFlat6,sFlat7) = sFlat6,
inference(orient,[status(thm)],[t7940]) ).
cnf(t7982,plain,
sFlat7 = meet(sFlat7,sFlat6),
inference(cp,[status(thm)],[t1400,t7981]) ).
cnf(t96079,plain,
sFlat7 = meet(sFlat6,sFlat7),
inference(step,[status(thm)],[t7982,t23]) ).
cnf(t96080,plain,
sFlat7 = meet(sFlat2,sFlat6),
inference(step,[status(thm)],[t96079,t7076]) ).
cnf(t8006,plain,
meet(sFlat2,sFlat6) = sFlat7,
inference(orient,[status(thm)],[t96080]) ).
cnf(t96081,plain,
meet(sFlat6,c) = sFlat7,
inference(step,[status(thm)],[t7077,t8006]) ).
cnf(t8007,plain,
meet(sFlat6,c) = sFlat7,
inference(orient,[status(thm)],[t96081]) ).
cnf(t96095,plain,
meet(sFlat5,sFlat7) = sFlat7,
inference(step,[status(thm)],[t96094,t8007]) ).
cnf(t8095,plain,
meet(sFlat5,sFlat7) = sFlat7,
inference(orient,[status(thm)],[t96095]) ).
cnf(t8099,plain,
sFlat5 = join(sFlat5,sFlat7),
inference(cp,[status(thm)],[t22,t8095]) ).
cnf(t2869,plain,
join(sFlat8,meet(sFlat3,a)) = join(sFlat8,sFlat5),
inference(cp,[status(thm)],[t499,t2866]) ).
cnf(t95832,plain,
join(sFlat8,meet(sFlat3,a)) = join(sFlat5,sFlat8),
inference(step,[status(thm)],[t2869,t68]) ).
cnf(t93,plain,
b = meet(b,sFlat5),
inference(cp,[status(thm)],[t20,t92]) ).
cnf(t95591,plain,
b = meet(sFlat5,b),
inference(step,[status(thm)],[t93,t23]) ).
cnf(t130,plain,
meet(sFlat5,b) = b,
inference(orient,[status(thm)],[t95591]) ).
cnf(t132,plain,
sFlat5 = join(sFlat5,b),
inference(cp,[status(thm)],[t22,t130]) ).
cnf(t150,plain,
join(sFlat5,b) = sFlat5,
inference(orient,[status(thm)],[t132]) ).
cnf(t509,plain,
join(sFlat8,sFlat5) = join(sFlat7,sFlat5),
inference(cp,[status(thm)],[t507,t150]) ).
cnf(t95649,plain,
join(sFlat5,sFlat8) = join(sFlat7,sFlat5),
inference(step,[status(thm)],[t509,t68]) ).
cnf(t95650,plain,
join(sFlat5,sFlat8) = join(sFlat5,sFlat7),
inference(step,[status(thm)],[t95649,t68]) ).
cnf(t517,plain,
join(sFlat5,sFlat8) = join(sFlat5,sFlat7),
inference(orient,[status(thm)],[t95650]) ).
cnf(t95833,plain,
join(sFlat8,meet(sFlat3,a)) = join(sFlat5,sFlat7),
inference(step,[status(thm)],[t95832,t517]) ).
cnf(t2925,plain,
join(sFlat8,meet(sFlat3,a)) = join(sFlat5,sFlat7),
inference(orient,[status(thm)],[t95833]) ).
cnf(t96003,plain,
join(sFlat8,sFlat4) = join(sFlat5,sFlat7),
inference(step,[status(thm)],[t2925,t7766]) ).
cnf(t7785,plain,
join(sFlat8,sFlat4) = join(sFlat5,sFlat7),
inference(rw,[status(thm)],[t96003]) ).
cnf(t96054,plain,
join(sFlat4,sFlat8) = join(sFlat5,sFlat7),
inference(step,[status(thm)],[t7785,t68]) ).
cnf(t7951,plain,
join(sFlat5,sFlat7) = join(sFlat4,sFlat8),
inference(orient,[status(thm)],[t96054]) ).
cnf(t96096,plain,
sFlat5 = join(sFlat4,sFlat8),
inference(step,[status(thm)],[t8099,t7951]) ).
cnf(t8105,plain,
join(sFlat4,sFlat8) = sFlat5,
inference(orient,[status(thm)],[t96096]) ).
cnf(t8380,plain,
join(sFlat3,sFlat8) = join(sFlat3,sFlat5),
inference(cp,[status(thm)],[t8379,t8105]) ).
cnf(t8398,plain,
join(sFlat3,sFlat8) = join(sFlat3,sFlat5),
inference(orient,[status(thm)],[t8380]) ).
cnf(t1015,plain,
join(X1,X2) = join(X1,join(X2,meet(X1,X3))),
inference(cp,[status(thm)],[t1012,t68]) ).
cnf(t1832,plain,
join(X1,join(X2,meet(X1,X3))) = join(X1,X2),
inference(orient,[status(thm)],[t1015]) ).
cnf(t49,plain,
meet(a,meet(join(b,sFlat4),X1)) = meet(sFlat6,X1),
inference(cp,[status(thm)],[t24,t48]) ).
cnf(t95739,plain,
meet(a,meet(join(sFlat4,b),X1)) = meet(sFlat6,X1),
inference(step,[status(thm)],[t49,t68]) ).
cnf(t1718,plain,
meet(a,meet(join(sFlat4,b),X1)) = meet(sFlat6,X1),
inference(orient,[status(thm)],[t95739]) ).
cnf(t1723,plain,
meet(sFlat6,join(join(sFlat4,b),X1)) = meet(a,join(sFlat4,b)),
inference(cp,[status(thm)],[t1718,t20]) ).
cnf(t95750,plain,
meet(sFlat6,join(sFlat4,join(b,X1))) = meet(a,join(sFlat4,b)),
inference(step,[status(thm)],[t1723,t71]) ).
cnf(t95751,plain,
meet(sFlat6,join(sFlat4,join(b,X1))) = sFlat6,
inference(step,[status(thm)],[t95750,t177]) ).
cnf(t1856,plain,
meet(sFlat6,join(sFlat4,join(b,X1))) = sFlat6,
inference(orient,[status(thm)],[t95751]) ).
cnf(t1858,plain,
sFlat6 = meet(sFlat6,join(sFlat4,join(X1,b))),
inference(cp,[status(thm)],[t1856,t68]) ).
cnf(t2844,plain,
meet(sFlat6,join(sFlat4,join(X1,b))) = sFlat6,
inference(orient,[status(thm)],[t1858]) ).
cnf(t2846,plain,
sFlat6 = meet(sFlat6,join(sFlat4,sFlat5)),
inference(cp,[status(thm)],[t2844,t150]) ).
cnf(t2852,plain,
meet(sFlat6,join(sFlat4,sFlat5)) = sFlat6,
inference(orient,[status(thm)],[t2846]) ).
cnf(t151,plain,
join(sFlat5,join(b,X1)) = join(sFlat5,X1),
inference(cp,[status(thm)],[t71,t150]) ).
cnf(t726,plain,
join(sFlat5,join(b,X1)) = join(sFlat5,X1),
inference(orient,[status(thm)],[t151]) ).
cnf(t2868,plain,
join(sFlat5,meet(sFlat3,a)) = join(sFlat5,sFlat5),
inference(cp,[status(thm)],[t726,t2866]) ).
cnf(t95831,plain,
join(sFlat5,meet(sFlat3,a)) = sFlat5,
inference(step,[status(thm)],[t2868,t21]) ).
cnf(t2921,plain,
join(sFlat5,meet(sFlat3,a)) = sFlat5,
inference(orient,[status(thm)],[t95831]) ).
cnf(t96004,plain,
join(sFlat5,sFlat4) = sFlat5,
inference(step,[status(thm)],[t2921,t7766]) ).
cnf(t7786,plain,
join(sFlat5,sFlat4) = sFlat5,
inference(rw,[status(thm)],[t96004]) ).
cnf(t96017,plain,
join(sFlat4,sFlat5) = sFlat5,
inference(step,[status(thm)],[t7786,t68]) ).
cnf(t7829,plain,
join(sFlat4,sFlat5) = sFlat5,
inference(orient,[status(thm)],[t96017]) ).
cnf(t96020,plain,
meet(sFlat6,sFlat5) = sFlat6,
inference(step,[status(thm)],[t2852,t7829]) ).
cnf(t7845,plain,
meet(sFlat6,sFlat5) = sFlat6,
inference(rw,[status(thm)],[t96020]) ).
cnf(t96032,plain,
meet(sFlat5,sFlat6) = sFlat6,
inference(step,[status(thm)],[t7845,t23]) ).
cnf(t7880,plain,
meet(sFlat5,sFlat6) = sFlat6,
inference(orient,[status(thm)],[t96032]) ).
cnf(t7884,plain,
join(sFlat5,X1) = join(sFlat5,join(X1,sFlat6)),
inference(cp,[status(thm)],[t1832,t7880]) ).
cnf(t8780,plain,
join(sFlat5,join(X1,sFlat6)) = join(sFlat5,X1),
inference(orient,[status(thm)],[t7884]) ).
cnf(t28,plain,
meet(X1,meet(X1,X2)) = meet(X1,X2),
inference(cp,[status(thm)],[t24,t19]) ).
cnf(t153,plain,
meet(X1,meet(X1,X2)) = meet(X1,X2),
inference(orient,[status(thm)],[t28]) ).
cnf(t1059,plain,
X1 = join(X1,meet(X2,X1)),
inference(cp,[status(thm)],[t1057,t153]) ).
cnf(t1158,plain,
join(X1,meet(X2,X1)) = X1,
inference(orient,[status(thm)],[t1059]) ).
cnf(t1171,plain,
sFlat6 = join(sFlat6,sFlat4),
inference(cp,[status(thm)],[t1158,t685]) ).
cnf(t95704,plain,
sFlat6 = join(sFlat4,sFlat6),
inference(step,[status(thm)],[t1171,t68]) ).
cnf(t1198,plain,
join(sFlat4,sFlat6) = sFlat6,
inference(orient,[status(thm)],[t95704]) ).
cnf(t5987,plain,
join(X1,sFlat4) = meet(join(X1,sFlat4),join(X1,sFlat6)),
inference(cp,[status(thm)],[t5879,t1198]) ).
cnf(t12574,plain,
meet(join(X1,sFlat4),join(X1,sFlat6)) = join(X1,sFlat4),
inference(orient,[status(thm)],[t5987]) ).
cnf(t83,plain,
sFlat0 = meet(sFlat0,sFlat3),
inference(cp,[status(thm)],[t20,t82]) ).
cnf(t125,plain,
meet(sFlat0,sFlat3) = sFlat0,
inference(orient,[status(thm)],[t83]) ).
cnf(t126,plain,
meet(sFlat0,meet(sFlat3,X1)) = meet(sFlat0,X1),
inference(cp,[status(thm)],[t24,t125]) ).
cnf(t367,plain,
meet(sFlat0,meet(sFlat3,X1)) = meet(sFlat0,X1),
inference(orient,[status(thm)],[t126]) ).
cnf(t1183,plain,
meet(sFlat3,X1) = join(meet(sFlat3,X1),meet(sFlat0,X1)),
inference(cp,[status(thm)],[t1158,t367]) ).
cnf(t95903,plain,
meet(sFlat3,X1) = join(meet(sFlat0,X1),meet(sFlat3,X1)),
inference(step,[status(thm)],[t1183,t68]) ).
cnf(t5169,plain,
join(meet(sFlat0,X1),meet(sFlat3,X1)) = meet(sFlat3,X1),
inference(orient,[status(thm)],[t95903]) ).
cnf(t1424,plain,
join(sFlat2,X1) = meet(join(sFlat2,X1),join(sFlat3,X1)),
inference(cp,[status(thm)],[t1400,t386]) ).
cnf(t5685,plain,
meet(join(sFlat2,X1),join(sFlat3,X1)) = join(sFlat2,X1),
inference(orient,[status(thm)],[t1424]) ).
cnf(t7755,plain,
sFlat3 = join(sFlat3,sFlat4),
inference(cp,[status(thm)],[t22,t7749]) ).
cnf(t7788,plain,
join(sFlat3,sFlat4) = sFlat3,
inference(orient,[status(thm)],[t7755]) ).
cnf(t7789,plain,
join(sFlat2,sFlat4) = meet(join(sFlat2,sFlat4),sFlat3),
inference(cp,[status(thm)],[t5685,t7788]) ).
cnf(t96142,plain,
join(sFlat2,sFlat4) = meet(sFlat3,join(sFlat2,sFlat4)),
inference(step,[status(thm)],[t7789,t23]) ).
cnf(t8651,plain,
meet(sFlat3,join(sFlat2,sFlat4)) = join(sFlat2,sFlat4),
inference(orient,[status(thm)],[t96142]) ).
cnf(t8652,plain,
meet(sFlat3,join(sFlat2,sFlat4)) = join(meet(sFlat0,join(sFlat2,sFlat4)),join(sFlat2,sFlat4)),
inference(cp,[status(thm)],[t5169,t8651]) ).
cnf(t96143,plain,
join(sFlat2,sFlat4) = join(meet(sFlat0,join(sFlat2,sFlat4)),join(sFlat2,sFlat4)),
inference(step,[status(thm)],[t8652,t8651]) ).
cnf(t57,plain,
meet(b,meet(a,X1)) = meet(sFlat0,X1),
inference(cp,[status(thm)],[t24,t56]) ).
cnf(t194,plain,
meet(b,meet(a,X1)) = meet(sFlat0,X1),
inference(orient,[status(thm)],[t57]) ).
cnf(t195,plain,
meet(sFlat0,join(sFlat4,b)) = meet(b,sFlat6),
inference(cp,[status(thm)],[t194,t177]) ).
cnf(t95662,plain,
meet(sFlat0,join(sFlat4,b)) = meet(sFlat6,b),
inference(step,[status(thm)],[t195,t23]) ).
cnf(t200,plain,
meet(sFlat0,X1) = meet(b,meet(X1,a)),
inference(cp,[status(thm)],[t194,t23]) ).
cnf(t401,plain,
meet(b,meet(X1,a)) = meet(sFlat0,X1),
inference(orient,[status(thm)],[t200]) ).
cnf(t404,plain,
meet(sFlat0,sFlat6) = meet(b,sFlat6),
inference(cp,[status(thm)],[t401,t137]) ).
cnf(t95628,plain,
meet(sFlat0,sFlat6) = meet(sFlat6,b),
inference(step,[status(thm)],[t404,t23]) ).
cnf(t413,plain,
meet(sFlat6,b) = meet(sFlat0,sFlat6),
inference(orient,[status(thm)],[t95628]) ).
cnf(t95663,plain,
meet(sFlat0,join(sFlat4,b)) = meet(sFlat0,sFlat6),
inference(step,[status(thm)],[t95662,t413]) ).
cnf(t671,plain,
meet(sFlat0,join(sFlat4,b)) = meet(sFlat0,sFlat6),
inference(orient,[status(thm)],[t95663]) ).
cnf(t355,plain,
sFlat0 = meet(sFlat0,join(b,X1)),
inference(cp,[status(thm)],[t20,t352]) ).
cnf(t595,plain,
meet(sFlat0,join(b,X1)) = sFlat0,
inference(orient,[status(thm)],[t355]) ).
cnf(t598,plain,
sFlat0 = meet(sFlat0,join(X1,b)),
inference(cp,[status(thm)],[t595,t68]) ).
cnf(t828,plain,
meet(sFlat0,join(X1,b)) = sFlat0,
inference(orient,[status(thm)],[t598]) ).
cnf(t95688,plain,
sFlat0 = meet(sFlat0,sFlat6),
inference(step,[status(thm)],[t671,t828]) ).
cnf(t832,plain,
sFlat0 = meet(sFlat0,sFlat6),
inference(rw,[status(thm)],[t95688]) ).
cnf(t833,plain,
meet(sFlat0,sFlat6) = sFlat0,
inference(orient,[status(thm)],[t832]) ).
cnf(t5191,plain,
meet(sFlat3,sFlat6) = join(sFlat0,meet(sFlat3,sFlat6)),
inference(cp,[status(thm)],[t5169,t833]) ).
cnf(t5250,plain,
join(sFlat0,meet(sFlat3,sFlat6)) = meet(sFlat3,sFlat6),
inference(orient,[status(thm)],[t5191]) ).
cnf(t95996,plain,
join(sFlat0,sFlat4) = meet(sFlat3,sFlat6),
inference(step,[status(thm)],[t5250,t7749]) ).
cnf(t95997,plain,
join(sFlat0,sFlat4) = sFlat4,
inference(step,[status(thm)],[t95996,t7749]) ).
cnf(t7765,plain,
join(sFlat0,sFlat4) = sFlat4,
inference(rw,[status(thm)],[t95997]) ).
cnf(t7798,plain,
join(sFlat0,sFlat4) = sFlat4,
inference(orient,[status(thm)],[t7765]) ).
cnf(t7802,plain,
sFlat0 = meet(sFlat0,join(X1,sFlat4)),
inference(cp,[status(thm)],[t1922,t7798]) ).
cnf(t8288,plain,
meet(sFlat0,join(X1,sFlat4)) = sFlat0,
inference(orient,[status(thm)],[t7802]) ).
cnf(t96144,plain,
join(sFlat2,sFlat4) = join(sFlat0,join(sFlat2,sFlat4)),
inference(step,[status(thm)],[t96143,t8288]) ).
cnf(t96145,plain,
join(sFlat2,sFlat4) = join(sFlat3,sFlat4),
inference(step,[status(thm)],[t96144,t386]) ).
cnf(t96146,plain,
join(sFlat2,sFlat4) = sFlat3,
inference(step,[status(thm)],[t96145,t7788]) ).
cnf(t8663,plain,
join(sFlat2,sFlat4) = sFlat3,
inference(orient,[status(thm)],[t96146]) ).
cnf(t12575,plain,
join(sFlat2,sFlat4) = meet(sFlat3,join(sFlat2,sFlat6)),
inference(cp,[status(thm)],[t12574,t8663]) ).
cnf(t96253,plain,
sFlat3 = meet(sFlat3,join(sFlat2,sFlat6)),
inference(step,[status(thm)],[t12575,t8663]) ).
cnf(t12587,plain,
meet(sFlat3,join(sFlat2,sFlat6)) = sFlat3,
inference(orient,[status(thm)],[t96253]) ).
cnf(t12588,plain,
join(sFlat2,sFlat6) = join(join(sFlat2,sFlat6),sFlat3),
inference(cp,[status(thm)],[t1158,t12587]) ).
cnf(t96254,plain,
join(sFlat2,sFlat6) = join(sFlat2,join(sFlat6,sFlat3)),
inference(step,[status(thm)],[t12588,t71]) ).
cnf(t96255,plain,
join(sFlat2,sFlat6) = join(sFlat2,join(sFlat3,sFlat6)),
inference(step,[status(thm)],[t96254,t68]) ).
cnf(t390,plain,
join(sFlat3,join(sFlat2,X1)) = join(sFlat0,join(sFlat2,X1)),
inference(cp,[status(thm)],[t386,t180]) ).
cnf(t95681,plain,
join(sFlat2,join(sFlat3,X1)) = join(sFlat0,join(sFlat2,X1)),
inference(step,[status(thm)],[t390,t337]) ).
cnf(t95682,plain,
join(sFlat2,join(sFlat3,X1)) = join(sFlat3,X1),
inference(step,[status(thm)],[t95681,t386]) ).
cnf(t784,plain,
join(sFlat2,join(sFlat3,X1)) = join(sFlat3,X1),
inference(orient,[status(thm)],[t95682]) ).
cnf(t96256,plain,
join(sFlat2,sFlat6) = join(sFlat3,sFlat6),
inference(step,[status(thm)],[t96255,t784]) ).
cnf(t12597,plain,
join(sFlat3,sFlat6) = join(sFlat2,sFlat6),
inference(orient,[status(thm)],[t96256]) ).
cnf(t12598,plain,
join(sFlat5,sFlat3) = join(sFlat5,join(sFlat2,sFlat6)),
inference(cp,[status(thm)],[t8780,t12597]) ).
cnf(t96257,plain,
join(sFlat3,sFlat5) = join(sFlat5,join(sFlat2,sFlat6)),
inference(step,[status(thm)],[t12598,t68]) ).
cnf(t96258,plain,
join(sFlat3,sFlat5) = join(sFlat5,sFlat2),
inference(step,[status(thm)],[t96257,t8780]) ).
cnf(t96259,plain,
join(sFlat3,sFlat5) = join(sFlat2,sFlat5),
inference(step,[status(thm)],[t96258,t68]) ).
cnf(t12611,plain,
join(sFlat3,sFlat5) = join(sFlat2,sFlat5),
inference(orient,[status(thm)],[t96259]) ).
cnf(t96262,plain,
join(sFlat3,sFlat8) = join(sFlat2,sFlat5),
inference(step,[status(thm)],[t8398,t12611]) ).
cnf(t12614,plain,
join(sFlat3,sFlat8) = join(sFlat2,sFlat5),
inference(orient,[status(thm)],[t96262]) ).
cnf(t96307,plain,
join(sFlat2,sFlat8) = join(sFlat2,sFlat5),
inference(step,[status(thm)],[t96306,t12614]) ).
cnf(t15372,plain,
join(sFlat2,sFlat8) = join(sFlat2,sFlat5),
inference(orient,[status(thm)],[t96307]) ).
cnf(t96308,plain,
join(sFlat2,b) = join(sFlat2,sFlat5),
inference(step,[status(thm)],[t14980,t15372]) ).
cnf(t15373,plain,
join(sFlat2,b) = join(sFlat2,sFlat5),
inference(orient,[status(thm)],[t96308]) ).
cnf(t98114,plain,
meet(a,join(sFlat2,sFlat5)) = meet(a,join(b,meet(c,a))),
inference(step,[status(thm)],[t98113,t15373]) ).
cnf(t98115,plain,
meet(a,join(sFlat2,sFlat5)) = meet(a,join(b,sFlat7)),
inference(step,[status(thm)],[t98114,t60]) ).
cnf(t98116,plain,
meet(a,join(sFlat2,sFlat5)) = meet(a,join(sFlat7,b)),
inference(step,[status(thm)],[t98115,t68]) ).
cnf(t98117,plain,
meet(a,join(sFlat2,sFlat5)) = meet(a,sFlat8),
inference(step,[status(thm)],[t98116,t97]) ).
cnf(t98118,plain,
meet(a,join(sFlat2,sFlat5)) = meet(sFlat8,a),
inference(step,[status(thm)],[t98117,t23]) ).
cnf(t98119,plain,
meet(a,join(sFlat2,sFlat5)) = sFlat9,
inference(step,[status(thm)],[t98118,t156]) ).
cnf(t95320,plain,
meet(a,join(sFlat2,sFlat5)) = sFlat9,
inference(orient,[status(thm)],[t98119]) ).
cnf(t95326,plain,
meet(sFlat6,join(sFlat2,sFlat5)) = meet(sFlat6,sFlat9),
inference(cp,[status(thm)],[t687,t95320]) ).
cnf(t7882,plain,
sFlat5 = join(sFlat5,sFlat6),
inference(cp,[status(thm)],[t22,t7880]) ).
cnf(t7974,plain,
join(sFlat5,sFlat6) = sFlat5,
inference(orient,[status(thm)],[t7882]) ).
cnf(t7975,plain,
sFlat6 = meet(sFlat6,join(X1,sFlat5)),
inference(cp,[status(thm)],[t1282,t7974]) ).
cnf(t8529,plain,
meet(sFlat6,join(X1,sFlat5)) = sFlat6,
inference(orient,[status(thm)],[t7975]) ).
cnf(t98120,plain,
sFlat6 = meet(sFlat6,sFlat9),
inference(step,[status(thm)],[t95326,t8529]) ).
cnf(t158,plain,
meet(sFlat8,meet(a,X1)) = meet(sFlat9,X1),
inference(cp,[status(thm)],[t24,t156]) ).
cnf(t381,plain,
meet(sFlat8,meet(a,X1)) = meet(sFlat9,X1),
inference(orient,[status(thm)],[t158]) ).
cnf(t382,plain,
meet(sFlat9,join(sFlat4,b)) = meet(sFlat8,sFlat6),
inference(cp,[status(thm)],[t381,t177]) ).
cnf(t95694,plain,
meet(sFlat9,join(sFlat4,b)) = meet(sFlat6,sFlat8),
inference(step,[status(thm)],[t382,t23]) ).
cnf(t894,plain,
meet(sFlat9,join(sFlat4,b)) = meet(sFlat6,sFlat8),
inference(orient,[status(thm)],[t95694]) ).
cnf(t897,plain,
sFlat9 = join(sFlat9,meet(sFlat6,sFlat8)),
inference(cp,[status(thm)],[t22,t894]) ).
cnf(t985,plain,
join(sFlat9,meet(sFlat6,sFlat8)) = sFlat9,
inference(orient,[status(thm)],[t897]) ).
cnf(t1425,plain,
meet(sFlat6,sFlat8) = meet(meet(sFlat6,sFlat8),sFlat9),
inference(cp,[status(thm)],[t1400,t985]) ).
cnf(t95718,plain,
meet(sFlat6,sFlat8) = meet(sFlat6,meet(sFlat8,sFlat9)),
inference(step,[status(thm)],[t1425,t24]) ).
cnf(t157,plain,
meet(sFlat8,a) = meet(sFlat8,sFlat9),
inference(cp,[status(thm)],[t153,t156]) ).
cnf(t95595,plain,
sFlat9 = meet(sFlat8,sFlat9),
inference(step,[status(thm)],[t157,t156]) ).
cnf(t160,plain,
meet(sFlat8,sFlat9) = sFlat9,
inference(orient,[status(thm)],[t95595]) ).
cnf(t95719,plain,
meet(sFlat6,sFlat8) = meet(sFlat6,sFlat9),
inference(step,[status(thm)],[t95718,t160]) ).
cnf(t1439,plain,
meet(sFlat6,sFlat9) = meet(sFlat6,sFlat8),
inference(orient,[status(thm)],[t95719]) ).
cnf(t96027,plain,
meet(sFlat9,sFlat5) = meet(sFlat6,sFlat8),
inference(step,[status(thm)],[t894,t7846]) ).
cnf(t7870,plain,
meet(sFlat9,sFlat5) = meet(sFlat6,sFlat8),
inference(rw,[status(thm)],[t96027]) ).
cnf(t96113,plain,
meet(sFlat5,sFlat9) = meet(sFlat6,sFlat8),
inference(step,[status(thm)],[t7870,t23]) ).
cnf(t159,plain,
sFlat8 = join(sFlat8,sFlat9),
inference(cp,[status(thm)],[t22,t156]) ).
cnf(t163,plain,
join(sFlat8,sFlat9) = sFlat8,
inference(orient,[status(thm)],[t159]) ).
cnf(t1310,plain,
sFlat9 = meet(sFlat9,join(X1,sFlat8)),
inference(cp,[status(thm)],[t1282,t163]) ).
cnf(t1472,plain,
meet(sFlat9,join(X1,sFlat8)) = sFlat9,
inference(orient,[status(thm)],[t1310]) ).
cnf(t8114,plain,
sFlat9 = meet(sFlat9,sFlat5),
inference(cp,[status(thm)],[t1472,t8105]) ).
cnf(t96109,plain,
sFlat9 = meet(sFlat5,sFlat9),
inference(step,[status(thm)],[t8114,t23]) ).
cnf(t8137,plain,
meet(sFlat5,sFlat9) = sFlat9,
inference(orient,[status(thm)],[t96109]) ).
cnf(t96114,plain,
sFlat9 = meet(sFlat6,sFlat8),
inference(step,[status(thm)],[t96113,t8137]) ).
cnf(t8238,plain,
meet(sFlat6,sFlat8) = sFlat9,
inference(orient,[status(thm)],[t96114]) ).
cnf(t96115,plain,
meet(sFlat6,sFlat9) = sFlat9,
inference(step,[status(thm)],[t1439,t8238]) ).
cnf(t8239,plain,
meet(sFlat6,sFlat9) = sFlat9,
inference(orient,[status(thm)],[t96115]) ).
cnf(t98121,plain,
sFlat6 = sFlat9,
inference(step,[status(thm)],[t98120,t8239]) ).
cnf(t95369,plain,
sFlat9 = sFlat6,
inference(orient,[status(thm)],[t98121]) ).
cnf(t98122,plain,
meet(sFlat8,a) = sFlat6,
inference(step,[status(thm)],[t156,t95369]) ).
cnf(t95370,plain,
meet(sFlat8,a) = sFlat6,
inference(orient,[status(thm)],[t98122]) ).
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,t56]) ).
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,t68]) ).
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,t87]) ).
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,t166]) ).
cnf(g0_6,plain,
meet(a,join(b,meet(a,sFlat3))) != meet(a,join(b,meet(a,c))),
inference(rw,[status(thm)],[g0_5,t187]) ).
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,t7766]) ).
cnf(g0_9,plain,
meet(a,join(sFlat4,b)) != meet(a,join(b,meet(a,c))),
inference(rw,[status(thm)],[g0_8,t68]) ).
cnf(g0_10,plain,
meet(a,sFlat5) != meet(a,join(b,meet(a,c))),
inference(rw,[status(thm)],[g0_9,t7846]) ).
cnf(g0_11,plain,
meet(sFlat5,a) != meet(a,join(b,meet(a,c))),
inference(rw,[status(thm)],[g0_10,t23]) ).
cnf(g0_12,plain,
sFlat6 != meet(a,join(b,meet(a,c))),
inference(rw,[status(thm)],[g0_11,t8085]) ).
cnf(g0_13,plain,
sFlat6 != meet(a,join(b,meet(c,a))),
inference(rw,[status(thm)],[g0_12,t23]) ).
cnf(g0_14,plain,
sFlat6 != meet(a,join(b,sFlat7)),
inference(rw,[status(thm)],[g0_13,t60]) ).
cnf(g0_15,plain,
sFlat6 != meet(a,join(sFlat7,b)),
inference(rw,[status(thm)],[g0_14,t68]) ).
cnf(g0_16,plain,
sFlat6 != meet(a,sFlat8),
inference(rw,[status(thm)],[g0_15,t97]) ).
cnf(g0_17,plain,
sFlat6 != meet(sFlat8,a),
inference(rw,[status(thm)],[g0_16,t23]) ).
cnf(g0_18,plain,
sFlat6 != sFlat6,
inference(rw,[status(thm)],[g0_17,t95370]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_18]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LAT153-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/10.39 % Computer : n002.cluster.edu
% 0.10/10.39 % Model : x86_64 x86_64
% 0.10/10.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/10.39 % Memory : 8046.5625MB
% 0.10/10.39 % OS : Linux 6.8.0-71-generic
% 0.10/10.39 % CPULimit : 300
% 0.10/10.39 % WCLimit : 300
% 0.10/10.39 % DateTime : Wed Sep 23 20:26:47 UTC 2026
% 0.10/10.39 % CPUTime :
% 0.10/10.39 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 253.99/48.52 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 253.99/48.52 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------