%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : MVA011-1 : TPTP v9.3.1. Released v8.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n003.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 02:14:21 PM UTC 2026
% Result : Unsatisfiable 67.84s 10.53s
% Output : CNFRefutation 67.84s
% Verified :
% SZS Type : Refutation
% Derivation depth : 113
% Number of leaves : 19
% Syntax : Number of clauses : 491 ( 491 unt; 0 nHn; 7 RR)
% Number of literals : 491 ( 490 equ; 4 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 : 8 ( 8 usr; 2 con; 0-2 aty)
% Number of variables : 961 ( 174 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t14,axiom,
meet(rd(join(op(X1,X2),X3),X2),X1) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t38,plain,
meet(rd(join(op(X1,X2),X3),X2),X1) = X1,
inference(orient,[status(thm)],[t14]) ).
cnf(t56,plain,
meet(rd(join(op(X1,X2),X3),X2),X1) = X1,
inference(rw,[status(thm)],[t38]) ).
cnf(t6,axiom,
meet(X1,X2) = meet(X2,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t85,plain,
meet(X1,X2) = meet(X2,X1),
inference(orient,[status(thm)],[t6]) ).
cnf(t144756,plain,
meet(X1,rd(join(op(X1,X2),X3),X2)) = X1,
inference(step,[status(thm)],[t56,t85]) ).
cnf(t4,axiom,
join(X1,X2) = join(X2,X1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t52,plain,
join(X1,X2) = join(X2,X1),
inference(orient,[status(thm)],[t4]) ).
cnf(t144757,plain,
meet(X1,rd(join(X3,op(X1,X2)),X2)) = X1,
inference(step,[status(thm)],[t144756,t52]) ).
cnf(t203,plain,
meet(X1,rd(join(X2,op(X1,X3)),X3)) = X1,
inference(orient,[status(thm)],[t144757]) ).
cnf(t9,axiom,
join(op(X1,meet(ld(X1,X2),X3)),X2) = X2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t20,plain,
join(op(X1,meet(ld(X1,X2),X3)),X2) = X2,
inference(orient,[status(thm)],[t9]) ).
cnf(t55,plain,
join(op(X1,meet(ld(X1,X2),X3)),X2) = X2,
inference(rw,[status(thm)],[t20]) ).
cnf(t144752,plain,
join(X2,op(X1,meet(ld(X1,X2),X3))) = X2,
inference(step,[status(thm)],[t55,t52]) ).
cnf(t144753,plain,
join(X2,op(X1,meet(X3,ld(X1,X2)))) = X2,
inference(step,[status(thm)],[t144752,t85]) ).
cnf(t162,plain,
join(X1,op(X2,meet(X3,ld(X2,X1)))) = X1,
inference(orient,[status(thm)],[t144753]) ).
cnf(t17,axiom,
op(op(X1,ld(X1,unit)),ld(ld(X2,unit),unit)) = at(X1,X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t15,axiom,
op(op(X1,X2),X3) = op(X1,op(X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t101,plain,
op(op(X1,X2),X3) = op(X1,op(X2,X3)),
inference(orient,[status(thm)],[t15]) ).
cnf(t144739,plain,
op(X1,op(ld(X1,unit),ld(ld(X2,unit),unit))) = at(X1,X2),
inference(step,[status(thm)],[t17,t101]) ).
cnf(t102,plain,
op(X1,op(ld(X1,unit),ld(ld(X2,unit),unit))) = at(X1,X2),
inference(orient,[status(thm)],[t144739]) ).
cnf(t10,axiom,
join(op(meet(X1,rd(X2,X3)),X3),X2) = X2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t21,plain,
join(op(meet(X1,rd(X2,X3)),X3),X2) = X2,
inference(orient,[status(thm)],[t10]) ).
cnf(t58,plain,
join(op(meet(X1,rd(X2,X3)),X3),X2) = X2,
inference(rw,[status(thm)],[t21]) ).
cnf(t144767,plain,
join(X2,op(meet(X1,rd(X2,X3)),X3)) = X2,
inference(step,[status(thm)],[t58,t52]) ).
cnf(t331,plain,
join(X1,op(meet(X2,rd(X1,X3)),X3)) = X1,
inference(orient,[status(thm)],[t144767]) ).
cnf(t2,axiom,
op(X1,unit) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t44,plain,
op(X1,unit) = X1,
inference(orient,[status(thm)],[t2]) ).
cnf(t332,plain,
X1 = join(X1,meet(X2,rd(X1,unit))),
inference(cp,[status(thm)],[t331,t44]) ).
cnf(t347,plain,
join(X1,meet(X2,rd(X1,unit))) = X1,
inference(orient,[status(thm)],[t332]) ).
cnf(t12,axiom,
meet(ld(X1,join(op(X1,X2),X3)),X2) = X2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t31,plain,
meet(ld(X1,join(op(X1,X2),X3)),X2) = X2,
inference(orient,[status(thm)],[t12]) ).
cnf(t57,plain,
meet(ld(X1,join(op(X1,X2),X3)),X2) = X2,
inference(rw,[status(thm)],[t31]) ).
cnf(t144761,plain,
meet(X2,ld(X1,join(op(X1,X2),X3))) = X2,
inference(step,[status(thm)],[t57,t85]) ).
cnf(t144762,plain,
meet(X2,ld(X1,join(X3,op(X1,X2)))) = X2,
inference(step,[status(thm)],[t144761,t52]) ).
cnf(t279,plain,
meet(X1,ld(X2,join(X3,op(X2,X1)))) = X1,
inference(orient,[status(thm)],[t144762]) ).
cnf(t343,plain,
X1 = meet(X1,ld(meet(X2,rd(X3,X1)),X3)),
inference(cp,[status(thm)],[t279,t331]) ).
cnf(t454,plain,
meet(X1,ld(meet(X2,rd(X3,X1)),X3)) = X1,
inference(orient,[status(thm)],[t343]) ).
cnf(t3,axiom,
op(unit,X1) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t48,plain,
op(unit,X1) = X1,
inference(orient,[status(thm)],[t3]) ).
cnf(t211,plain,
unit = meet(unit,rd(join(X1,X2),X2)),
inference(cp,[status(thm)],[t203,t48]) ).
cnf(t242,plain,
meet(unit,rd(join(X1,X2),X2)) = unit,
inference(orient,[status(thm)],[t211]) ).
cnf(t251,plain,
unit = meet(unit,rd(join(X1,X2),X1)),
inference(cp,[status(thm)],[t242,t52]) ).
cnf(t268,plain,
meet(unit,rd(join(X1,X2),X1)) = unit,
inference(orient,[status(thm)],[t251]) ).
cnf(t8,axiom,
join(join(X1,X2),X3) = join(X1,join(X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t144737,plain,
join(X3,join(X1,X2)) = join(X1,join(X2,X3)),
inference(step,[status(thm)],[t8,t52]) ).
cnf(t65,plain,
join(X1,join(X2,X3)) = join(X2,join(X3,X1)),
inference(orient,[status(thm)],[t144737]) ).
cnf(t269,plain,
unit = meet(unit,rd(join(X1,join(X2,X3)),X3)),
inference(cp,[status(thm)],[t268,t65]) ).
cnf(t407,plain,
meet(unit,rd(join(X1,join(X2,X3)),X3)) = unit,
inference(orient,[status(thm)],[t269]) ).
cnf(t1,axiom,
meet(X1,X1) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t22,plain,
meet(X1,X1) = X1,
inference(orient,[status(thm)],[t1]) ).
cnf(t350,plain,
X1 = join(X1,rd(X1,unit)),
inference(cp,[status(thm)],[t347,t22]) ).
cnf(t358,plain,
join(X1,rd(X1,unit)) = X1,
inference(orient,[status(thm)],[t350]) ).
cnf(t416,plain,
unit = meet(unit,rd(join(X1,X2),rd(X2,unit))),
inference(cp,[status(thm)],[t407,t358]) ).
cnf(t522,plain,
meet(unit,rd(join(X1,X2),rd(X2,unit))) = unit,
inference(orient,[status(thm)],[t416]) ).
cnf(t164,plain,
X1 = join(X1,meet(X2,ld(unit,X1))),
inference(cp,[status(thm)],[t162,t48]) ).
cnf(t172,plain,
join(X1,meet(X2,ld(unit,X1))) = X1,
inference(orient,[status(thm)],[t164]) ).
cnf(t173,plain,
X1 = join(X1,ld(unit,X1)),
inference(cp,[status(thm)],[t172,t22]) ).
cnf(t178,plain,
join(X1,ld(unit,X1)) = X1,
inference(orient,[status(thm)],[t173]) ).
cnf(t529,plain,
unit = meet(unit,rd(X1,rd(ld(unit,X1),unit))),
inference(cp,[status(thm)],[t522,t178]) ).
cnf(t605,plain,
meet(unit,rd(X1,rd(ld(unit,X1),unit))) = unit,
inference(orient,[status(thm)],[t529]) ).
cnf(t607,plain,
rd(ld(unit,X1),unit) = meet(rd(ld(unit,X1),unit),ld(unit,X1)),
inference(cp,[status(thm)],[t454,t605]) ).
cnf(t144856,plain,
rd(ld(unit,X1),unit) = meet(ld(unit,X1),rd(ld(unit,X1),unit)),
inference(step,[status(thm)],[t607,t85]) ).
cnf(t0,axiom,
join(X1,X1) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t18,plain,
join(X1,X1) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t206,plain,
X1 = meet(X1,rd(op(X1,X2),X2)),
inference(cp,[status(thm)],[t203,t18]) ).
cnf(t219,plain,
meet(X1,rd(op(X1,X2),X2)) = X1,
inference(orient,[status(thm)],[t206]) ).
cnf(t220,plain,
X1 = meet(X1,rd(X1,unit)),
inference(cp,[status(thm)],[t219,t44]) ).
cnf(t227,plain,
meet(X1,rd(X1,unit)) = X1,
inference(orient,[status(thm)],[t220]) ).
cnf(t144857,plain,
rd(ld(unit,X1),unit) = ld(unit,X1),
inference(step,[status(thm)],[t144856,t227]) ).
cnf(t1528,plain,
rd(ld(unit,X1),unit) = ld(unit,X1),
inference(orient,[status(thm)],[t144857]) ).
cnf(t1538,plain,
ld(unit,X1) = join(ld(unit,X1),meet(X2,ld(unit,X1))),
inference(cp,[status(thm)],[t347,t1528]) ).
cnf(t1563,plain,
join(ld(unit,X1),meet(X2,ld(unit,X1))) = ld(unit,X1),
inference(orient,[status(thm)],[t1538]) ).
cnf(t281,plain,
X1 = meet(X1,ld(X2,op(X2,X1))),
inference(cp,[status(thm)],[t279,t18]) ).
cnf(t292,plain,
meet(X1,ld(X2,op(X2,X1))) = X1,
inference(orient,[status(thm)],[t281]) ).
cnf(t296,plain,
X1 = meet(X1,ld(unit,X1)),
inference(cp,[status(thm)],[t292,t48]) ).
cnf(t304,plain,
meet(X1,ld(unit,X1)) = X1,
inference(orient,[status(thm)],[t296]) ).
cnf(t1564,plain,
ld(unit,X1) = join(ld(unit,X1),X1),
inference(cp,[status(thm)],[t1563,t304]) ).
cnf(t144860,plain,
ld(unit,X1) = join(X1,ld(unit,X1)),
inference(step,[status(thm)],[t1564,t52]) ).
cnf(t144861,plain,
ld(unit,X1) = X1,
inference(step,[status(thm)],[t144860,t178]) ).
cnf(t1585,plain,
ld(unit,X1) = X1,
inference(orient,[status(thm)],[t144861]) ).
cnf(t1591,plain,
at(unit,X1) = op(unit,op(unit,ld(ld(X1,unit),unit))),
inference(cp,[status(thm)],[t102,t1585]) ).
cnf(t144912,plain,
at(unit,X1) = op(unit,ld(ld(X1,unit),unit)),
inference(step,[status(thm)],[t1591,t48]) ).
cnf(t144913,plain,
at(unit,X1) = ld(ld(X1,unit),unit),
inference(step,[status(thm)],[t144912,t48]) ).
cnf(t1672,plain,
ld(ld(X1,unit),unit) = at(unit,X1),
inference(orient,[status(thm)],[t144913]) ).
cnf(t1681,plain,
unit = join(unit,op(ld(X1,unit),meet(X2,at(unit,X1)))),
inference(cp,[status(thm)],[t162,t1672]) ).
cnf(t79779,plain,
join(unit,op(ld(X1,unit),meet(X2,at(unit,X1)))) = unit,
inference(orient,[status(thm)],[t1681]) ).
cnf(t204,plain,
X1 = meet(X1,rd(X2,meet(X3,ld(X1,X2)))),
inference(cp,[status(thm)],[t203,t162]) ).
cnf(t393,plain,
meet(X1,rd(X2,meet(X3,ld(X1,X2)))) = X1,
inference(orient,[status(thm)],[t204]) ).
cnf(t144866,plain,
rd(X1,unit) = ld(unit,X1),
inference(step,[status(thm)],[t1528,t1585]) ).
cnf(t144867,plain,
rd(X1,unit) = X1,
inference(step,[status(thm)],[t144866,t1585]) ).
cnf(t1601,plain,
rd(X1,unit) = X1,
inference(rw,[status(thm)],[t144867]) ).
cnf(t1636,plain,
rd(X1,unit) = X1,
inference(orient,[status(thm)],[t1601]) ).
cnf(t1641,plain,
unit = meet(unit,ld(meet(X1,X2),X2)),
inference(cp,[status(thm)],[t454,t1636]) ).
cnf(t1694,plain,
meet(unit,ld(meet(X1,X2),X2)) = unit,
inference(orient,[status(thm)],[t1641]) ).
cnf(t1711,plain,
unit = meet(unit,ld(meet(X1,X2),X1)),
inference(cp,[status(thm)],[t1694,t85]) ).
cnf(t1734,plain,
meet(unit,ld(meet(X1,X2),X1)) = unit,
inference(orient,[status(thm)],[t1711]) ).
cnf(t13,axiom,
meet(meet(X1,X2),X3) = meet(X1,meet(X2,X3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t144738,plain,
meet(X3,meet(X1,X2)) = meet(X1,meet(X2,X3)),
inference(step,[status(thm)],[t13,t85]) ).
cnf(t87,plain,
meet(X1,meet(X2,X3)) = meet(X2,meet(X3,X1)),
inference(orient,[status(thm)],[t144738]) ).
cnf(t1735,plain,
unit = meet(unit,ld(meet(X1,meet(X2,X3)),X3)),
inference(cp,[status(thm)],[t1734,t87]) ).
cnf(t2007,plain,
meet(unit,ld(meet(X1,meet(X2,X3)),X3)) = unit,
inference(orient,[status(thm)],[t1735]) ).
cnf(t7,axiom,
meet(join(X1,X2),X1) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t25,plain,
meet(join(X1,X2),X1) = X1,
inference(orient,[status(thm)],[t7]) ).
cnf(t86,plain,
meet(join(X1,X2),X1) = X1,
inference(rw,[status(thm)],[t25]) ).
cnf(t144743,plain,
meet(X1,join(X1,X2)) = X1,
inference(step,[status(thm)],[t86,t85]) ).
cnf(t120,plain,
meet(X1,join(X1,X2)) = X1,
inference(orient,[status(thm)],[t144743]) ).
cnf(t2031,plain,
unit = meet(unit,ld(meet(X1,X2),join(X2,X3))),
inference(cp,[status(thm)],[t2007,t120]) ).
cnf(t2288,plain,
meet(unit,ld(meet(X1,X2),join(X2,X3))) = unit,
inference(orient,[status(thm)],[t2031]) ).
cnf(t2365,plain,
meet(X1,X2) = meet(meet(X1,X2),rd(join(X2,X3),unit)),
inference(cp,[status(thm)],[t393,t2288]) ).
cnf(t144954,plain,
meet(X1,X2) = meet(meet(X1,X2),join(X2,X3)),
inference(step,[status(thm)],[t2365,t1636]) ).
cnf(t2369,plain,
meet(meet(X1,X2),join(X2,X3)) = meet(X1,X2),
inference(orient,[status(thm)],[t144954]) ).
cnf(t165,plain,
X1 = join(X1,op(X2,ld(X2,X1))),
inference(cp,[status(thm)],[t162,t22]) ).
cnf(t182,plain,
join(X1,op(X2,ld(X2,X1))) = X1,
inference(orient,[status(thm)],[t165]) ).
cnf(t205,plain,
X1 = meet(X1,rd(X2,ld(X1,X2))),
inference(cp,[status(thm)],[t203,t182]) ).
cnf(t215,plain,
meet(X1,rd(X2,ld(X1,X2))) = X1,
inference(orient,[status(thm)],[t205]) ).
cnf(t2381,plain,
meet(X1,rd(X2,ld(X1,X2))) = meet(X1,join(rd(X2,ld(X1,X2)),X3)),
inference(cp,[status(thm)],[t2369,t215]) ).
cnf(t144989,plain,
X1 = meet(X1,join(rd(X2,ld(X1,X2)),X3)),
inference(step,[status(thm)],[t2381,t215]) ).
cnf(t144990,plain,
X1 = meet(X1,join(X3,rd(X2,ld(X1,X2)))),
inference(step,[status(thm)],[t144989,t52]) ).
cnf(t2770,plain,
meet(X1,join(X2,rd(X3,ld(X1,X3)))) = X1,
inference(orient,[status(thm)],[t144990]) ).
cnf(t11,axiom,
ld(rd(X1,join(X1,X2)),X1) = join(X1,X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t59,plain,
ld(rd(X1,join(X1,X2)),X1) = join(X1,X2),
inference(orient,[status(thm)],[t11]) ).
cnf(t167,plain,
X1 = join(X1,op(rd(X1,join(X1,X2)),meet(X3,join(X1,X2)))),
inference(cp,[status(thm)],[t162,t59]) ).
cnf(t2990,plain,
join(X1,op(rd(X1,join(X1,X2)),meet(X3,join(X1,X2)))) = X1,
inference(orient,[status(thm)],[t167]) ).
cnf(t5,axiom,
join(meet(X1,X2),X1) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t19,plain,
join(meet(X1,X2),X1) = X1,
inference(orient,[status(thm)],[t5]) ).
cnf(t54,plain,
join(meet(X1,X2),X1) = X1,
inference(rw,[status(thm)],[t19]) ).
cnf(t144740,plain,
join(X1,meet(X1,X2)) = X1,
inference(step,[status(thm)],[t54,t52]) ).
cnf(t108,plain,
join(X1,meet(X1,X2)) = X1,
inference(orient,[status(thm)],[t144740]) ).
cnf(t335,plain,
X1 = join(X1,op(rd(X1,X2),X2)),
inference(cp,[status(thm)],[t331,t22]) ).
cnf(t363,plain,
join(X1,op(rd(X1,X2),X2)) = X1,
inference(orient,[status(thm)],[t335]) ).
cnf(t366,plain,
X1 = meet(X1,ld(rd(X2,X1),X2)),
inference(cp,[status(thm)],[t279,t363]) ).
cnf(t373,plain,
meet(X1,ld(rd(X2,X1),X2)) = X1,
inference(orient,[status(thm)],[t366]) ).
cnf(t375,plain,
meet(X1,meet(ld(rd(X2,X1),X2),X3)) = meet(X3,X1),
inference(cp,[status(thm)],[t87,t373]) ).
cnf(t144802,plain,
meet(X1,meet(X3,ld(rd(X2,X1),X2))) = meet(X3,X1),
inference(step,[status(thm)],[t375,t85]) ).
cnf(t144803,plain,
meet(X1,meet(X3,ld(rd(X2,X1),X2))) = meet(X1,X3),
inference(step,[status(thm)],[t144802,t85]) ).
cnf(t934,plain,
meet(X1,meet(X2,ld(rd(X3,X1),X3))) = meet(X1,X2),
inference(orient,[status(thm)],[t144803]) ).
cnf(t114,plain,
join(X1,join(meet(X1,X2),X3)) = join(X3,X1),
inference(cp,[status(thm)],[t65,t108]) ).
cnf(t144748,plain,
join(X1,join(X3,meet(X1,X2))) = join(X3,X1),
inference(step,[status(thm)],[t114,t52]) ).
cnf(t144749,plain,
join(X1,join(X3,meet(X1,X2))) = join(X1,X3),
inference(step,[status(thm)],[t144748,t52]) ).
cnf(t142,plain,
join(X1,join(X2,meet(X1,X3))) = join(X1,X2),
inference(orient,[status(thm)],[t144749]) ).
cnf(t409,plain,
unit = meet(unit,rd(join(X1,X2),meet(X1,X3))),
inference(cp,[status(thm)],[t407,t142]) ).
cnf(t501,plain,
meet(unit,rd(join(X1,X2),meet(X1,X3))) = unit,
inference(orient,[status(thm)],[t409]) ).
cnf(t509,plain,
meet(X1,X2) = meet(meet(X1,X2),ld(unit,join(X1,X3))),
inference(cp,[status(thm)],[t454,t501]) ).
cnf(t971,plain,
meet(meet(X1,X2),ld(unit,join(X1,X3))) = meet(X1,X2),
inference(orient,[status(thm)],[t509]) ).
cnf(t144882,plain,
meet(meet(X1,X2),join(X1,X3)) = meet(X1,X2),
inference(step,[status(thm)],[t971,t1585]) ).
cnf(t1613,plain,
meet(meet(X1,X2),join(X1,X3)) = meet(X1,X2),
inference(rw,[status(thm)],[t144882]) ).
cnf(t1742,plain,
meet(meet(X1,X2),join(X1,X3)) = meet(X1,X2),
inference(orient,[status(thm)],[t1613]) ).
cnf(t245,plain,
unit = meet(unit,rd(X1,op(X2,ld(X2,X1)))),
inference(cp,[status(thm)],[t242,t182]) ).
cnf(t400,plain,
meet(unit,rd(X1,op(X2,ld(X2,X1)))) = unit,
inference(orient,[status(thm)],[t245]) ).
cnf(t456,plain,
op(X1,ld(X1,X2)) = meet(op(X1,ld(X1,X2)),ld(unit,X2)),
inference(cp,[status(thm)],[t454,t400]) ).
cnf(t144848,plain,
op(X1,ld(X1,X2)) = meet(ld(unit,X2),op(X1,ld(X1,X2))),
inference(step,[status(thm)],[t456,t85]) ).
cnf(t1281,plain,
meet(ld(unit,X1),op(X2,ld(X2,X1))) = op(X2,ld(X2,X1)),
inference(orient,[status(thm)],[t144848]) ).
cnf(t144878,plain,
meet(X1,op(X2,ld(X2,X1))) = op(X2,ld(X2,X1)),
inference(step,[status(thm)],[t1281,t1585]) ).
cnf(t1610,plain,
meet(X1,op(X2,ld(X2,X1))) = op(X2,ld(X2,X1)),
inference(rw,[status(thm)],[t144878]) ).
cnf(t1778,plain,
meet(X1,op(X2,ld(X2,X1))) = op(X2,ld(X2,X1)),
inference(orient,[status(thm)],[t1610]) ).
cnf(t1781,plain,
meet(X1,op(X2,ld(X2,X1))) = meet(op(X2,ld(X2,X1)),join(X1,X3)),
inference(cp,[status(thm)],[t1742,t1778]) ).
cnf(t145361,plain,
op(X2,ld(X2,X1)) = meet(op(X2,ld(X2,X1)),join(X1,X3)),
inference(step,[status(thm)],[t1781,t1778]) ).
cnf(t145362,plain,
op(X2,ld(X2,X1)) = meet(join(X1,X3),op(X2,ld(X2,X1))),
inference(step,[status(thm)],[t145361,t85]) ).
cnf(t28503,plain,
meet(join(X1,X2),op(X3,ld(X3,X1))) = op(X3,ld(X3,X1)),
inference(orient,[status(thm)],[t145362]) ).
cnf(t28547,plain,
join(X1,X2) = join(join(X1,X2),op(X3,ld(X3,X1))),
inference(cp,[status(thm)],[t108,t28503]) ).
cnf(t28644,plain,
join(join(X1,X2),op(X3,ld(X3,X1))) = join(X1,X2),
inference(orient,[status(thm)],[t28547]) ).
cnf(t28719,plain,
X1 = meet(X1,rd(join(X2,X3),ld(X1,X2))),
inference(cp,[status(thm)],[t203,t28644]) ).
cnf(t28723,plain,
meet(X1,rd(join(X2,X3),ld(X1,X2))) = X1,
inference(orient,[status(thm)],[t28719]) ).
cnf(t28753,plain,
X1 = meet(X1,rd(join(X2,X3),ld(X1,X3))),
inference(cp,[status(thm)],[t28723,t52]) ).
cnf(t28873,plain,
meet(X1,rd(join(X2,X3),ld(X1,X3))) = X1,
inference(orient,[status(thm)],[t28753]) ).
cnf(t1698,plain,
unit = meet(unit,ld(X1,ld(rd(X2,X1),X2))),
inference(cp,[status(thm)],[t1694,t373]) ).
cnf(t1845,plain,
meet(unit,ld(X1,ld(rd(X2,X1),X2))) = unit,
inference(orient,[status(thm)],[t1698]) ).
cnf(t1848,plain,
ld(rd(X1,X2),X1) = join(ld(rd(X1,X2),X1),op(X2,unit)),
inference(cp,[status(thm)],[t162,t1845]) ).
cnf(t144927,plain,
ld(rd(X1,X2),X1) = join(op(X2,unit),ld(rd(X1,X2),X1)),
inference(step,[status(thm)],[t1848,t52]) ).
cnf(t144928,plain,
ld(rd(X1,X2),X1) = join(X2,ld(rd(X1,X2),X1)),
inference(step,[status(thm)],[t144927,t44]) ).
cnf(t1851,plain,
join(X1,ld(rd(X2,X1),X2)) = ld(rd(X2,X1),X2),
inference(orient,[status(thm)],[t144928]) ).
cnf(t1853,plain,
meet(X1,X2) = meet(meet(X1,X2),ld(rd(X3,X1),X3)),
inference(cp,[status(thm)],[t1742,t1851]) ).
cnf(t3489,plain,
meet(meet(X1,X2),ld(rd(X3,X1),X3)) = meet(X1,X2),
inference(orient,[status(thm)],[t1853]) ).
cnf(t3520,plain,
X1 = join(X1,op(rd(X1,X2),meet(X2,X3))),
inference(cp,[status(thm)],[t162,t3489]) ).
cnf(t3560,plain,
join(X1,op(rd(X1,X2),meet(X2,X3))) = X1,
inference(orient,[status(thm)],[t3520]) ).
cnf(t60,plain,
join(X1,X1) = ld(rd(X1,X1),X1),
inference(cp,[status(thm)],[t59,t18]) ).
cnf(t144741,plain,
X1 = ld(rd(X1,X1),X1),
inference(step,[status(thm)],[t60,t18]) ).
cnf(t116,plain,
ld(rd(X1,X1),X1) = X1,
inference(orient,[status(thm)],[t144741]) ).
cnf(t118,plain,
at(X1,rd(unit,unit)) = op(X1,op(ld(X1,unit),ld(unit,unit))),
inference(cp,[status(thm)],[t102,t116]) ).
cnf(t1112,plain,
op(X1,op(ld(X1,unit),ld(unit,unit))) = at(X1,rd(unit,unit)),
inference(orient,[status(thm)],[t118]) ).
cnf(t144879,plain,
op(X1,op(ld(X1,unit),unit)) = at(X1,rd(unit,unit)),
inference(step,[status(thm)],[t1112,t1585]) ).
cnf(t144880,plain,
op(X1,ld(X1,unit)) = at(X1,rd(unit,unit)),
inference(step,[status(thm)],[t144879,t44]) ).
cnf(t1611,plain,
op(X1,ld(X1,unit)) = at(X1,rd(unit,unit)),
inference(rw,[status(thm)],[t144880]) ).
cnf(t16,axiom,
rd(X1,ld(join(X1,X2),X1)) = join(X1,X2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t62,plain,
rd(X1,ld(join(X1,X2),X1)) = join(X1,X2),
inference(orient,[status(thm)],[t16]) ).
cnf(t63,plain,
join(X1,X1) = rd(X1,ld(X1,X1)),
inference(cp,[status(thm)],[t62,t18]) ).
cnf(t144742,plain,
X1 = rd(X1,ld(X1,X1)),
inference(step,[status(thm)],[t63,t18]) ).
cnf(t119,plain,
rd(X1,ld(X1,X1)) = X1,
inference(orient,[status(thm)],[t144742]) ).
cnf(t1588,plain,
unit = rd(unit,unit),
inference(cp,[status(thm)],[t119,t1585]) ).
cnf(t1622,plain,
rd(unit,unit) = unit,
inference(orient,[status(thm)],[t1588]) ).
cnf(t144991,plain,
op(X1,ld(X1,unit)) = at(X1,unit),
inference(step,[status(thm)],[t1611,t1622]) ).
cnf(t2790,plain,
op(X1,ld(X1,unit)) = at(X1,unit),
inference(orient,[status(thm)],[t144991]) ).
cnf(t2799,plain,
op(X1,ld(X1,unit)) = meet(unit,at(X1,unit)),
inference(cp,[status(thm)],[t1778,t2790]) ).
cnf(t144992,plain,
at(X1,unit) = meet(unit,at(X1,unit)),
inference(step,[status(thm)],[t2799,t2790]) ).
cnf(t2828,plain,
meet(unit,at(X1,unit)) = at(X1,unit),
inference(orient,[status(thm)],[t144992]) ).
cnf(t3575,plain,
X1 = join(X1,op(rd(X1,unit),at(X2,unit))),
inference(cp,[status(thm)],[t3560,t2828]) ).
cnf(t145030,plain,
X1 = join(X1,op(X1,at(X2,unit))),
inference(step,[status(thm)],[t3575,t1636]) ).
cnf(t3592,plain,
join(X1,op(X1,at(X2,unit))) = X1,
inference(orient,[status(thm)],[t145030]) ).
cnf(t2796,plain,
op(X1,op(ld(X1,unit),X2)) = op(at(X1,unit),X2),
inference(cp,[status(thm)],[t101,t2790]) ).
cnf(t2919,plain,
op(X1,op(ld(X1,unit),X2)) = op(at(X1,unit),X2),
inference(orient,[status(thm)],[t2796]) ).
cnf(t2794,plain,
at(ld(X1,unit),unit) = op(ld(X1,unit),at(unit,X1)),
inference(cp,[status(thm)],[t2790,t1672]) ).
cnf(t2900,plain,
op(ld(X1,unit),at(unit,X1)) = at(ld(X1,unit),unit),
inference(orient,[status(thm)],[t2794]) ).
cnf(t2921,plain,
op(at(X1,unit),at(unit,X1)) = op(X1,at(ld(X1,unit),unit)),
inference(cp,[status(thm)],[t2919,t2900]) ).
cnf(t3411,plain,
op(at(X1,unit),at(unit,X1)) = op(X1,at(ld(X1,unit),unit)),
inference(orient,[status(thm)],[t2921]) ).
cnf(t144914,plain,
op(X1,op(ld(X1,unit),at(unit,X2))) = at(X1,X2),
inference(step,[status(thm)],[t102,t1672]) ).
cnf(t1682,plain,
op(X1,op(ld(X1,unit),at(unit,X2))) = at(X1,X2),
inference(rw,[status(thm)],[t144914]) ).
cnf(t145025,plain,
op(at(X1,unit),at(unit,X2)) = at(X1,X2),
inference(step,[status(thm)],[t1682,t2919]) ).
cnf(t3444,plain,
op(at(X1,unit),at(unit,X2)) = at(X1,X2),
inference(orient,[status(thm)],[t145025]) ).
cnf(t145026,plain,
at(X1,X1) = op(X1,at(ld(X1,unit),unit)),
inference(step,[status(thm)],[t3411,t3444]) ).
cnf(t3465,plain,
at(X1,X1) = op(X1,at(ld(X1,unit),unit)),
inference(rw,[status(thm)],[t145026]) ).
cnf(t3466,plain,
op(X1,at(ld(X1,unit),unit)) = at(X1,X1),
inference(orient,[status(thm)],[t3465]) ).
cnf(t3593,plain,
X1 = join(X1,at(X1,X1)),
inference(cp,[status(thm)],[t3592,t3466]) ).
cnf(t3609,plain,
join(X1,at(X1,X1)) = X1,
inference(orient,[status(thm)],[t3593]) ).
cnf(t28950,plain,
X1 = meet(X1,rd(X2,ld(X1,at(X2,X2)))),
inference(cp,[status(thm)],[t28873,t3609]) ).
cnf(t29064,plain,
meet(X1,rd(X2,ld(X1,at(X2,X2)))) = X1,
inference(orient,[status(thm)],[t28950]) ).
cnf(t29102,plain,
ld(X1,at(X2,X2)) = meet(ld(X1,at(X2,X2)),ld(X1,X2)),
inference(cp,[status(thm)],[t454,t29064]) ).
cnf(t145707,plain,
ld(X1,at(X2,X2)) = meet(ld(X1,X2),ld(X1,at(X2,X2))),
inference(step,[status(thm)],[t29102,t85]) ).
cnf(t52088,plain,
meet(ld(X1,X2),ld(X1,at(X2,X2))) = ld(X1,at(X2,X2)),
inference(orient,[status(thm)],[t145707]) ).
cnf(t52198,plain,
meet(X1,ld(rd(at(X2,X2),X1),X2)) = meet(X1,ld(rd(at(X2,X2),X1),at(X2,X2))),
inference(cp,[status(thm)],[t934,t52088]) ).
cnf(t145708,plain,
meet(X1,ld(rd(at(X2,X2),X1),X2)) = X1,
inference(step,[status(thm)],[t52198,t373]) ).
cnf(t52201,plain,
meet(X1,ld(rd(at(X2,X2),X1),X2)) = X1,
inference(orient,[status(thm)],[t145708]) ).
cnf(t52260,plain,
rd(at(X1,X1),X2) = meet(rd(at(X1,X1),X2),rd(X1,X2)),
inference(cp,[status(thm)],[t393,t52201]) ).
cnf(t145899,plain,
rd(at(X1,X1),X2) = meet(rd(X1,X2),rd(at(X1,X1),X2)),
inference(step,[status(thm)],[t52260,t85]) ).
cnf(t66030,plain,
meet(rd(X1,X2),rd(at(X1,X1),X2)) = rd(at(X1,X1),X2),
inference(orient,[status(thm)],[t145899]) ).
cnf(t66063,plain,
rd(X1,X2) = join(rd(X1,X2),rd(at(X1,X1),X2)),
inference(cp,[status(thm)],[t108,t66030]) ).
cnf(t66152,plain,
join(rd(X1,X2),rd(at(X1,X1),X2)) = rd(X1,X2),
inference(orient,[status(thm)],[t66063]) ).
cnf(t66227,plain,
rd(X1,X2) = join(rd(X1,X2),op(rd(rd(X1,X2),rd(X1,X2)),meet(X3,join(rd(X1,X2),rd(at(X1,X1),X2))))),
inference(cp,[status(thm)],[t2990,t66152]) ).
cnf(t1702,plain,
unit = meet(unit,ld(X1,rd(op(X1,X2),X2))),
inference(cp,[status(thm)],[t1694,t219]) ).
cnf(t1940,plain,
meet(unit,ld(X1,rd(op(X1,X2),X2))) = unit,
inference(orient,[status(thm)],[t1702]) ).
cnf(t1944,plain,
rd(op(X1,X2),X2) = join(rd(op(X1,X2),X2),op(X1,unit)),
inference(cp,[status(thm)],[t162,t1940]) ).
cnf(t144937,plain,
rd(op(X1,X2),X2) = join(op(X1,unit),rd(op(X1,X2),X2)),
inference(step,[status(thm)],[t1944,t52]) ).
cnf(t144938,plain,
rd(op(X1,X2),X2) = join(X1,rd(op(X1,X2),X2)),
inference(step,[status(thm)],[t144937,t44]) ).
cnf(t1947,plain,
join(X1,rd(op(X1,X2),X2)) = rd(op(X1,X2),X2),
inference(orient,[status(thm)],[t144938]) ).
cnf(t2791,plain,
at(op(X1,X2),unit) = op(X1,op(X2,ld(op(X1,X2),unit))),
inference(cp,[status(thm)],[t2790,t101]) ).
cnf(t30931,plain,
op(X1,op(X2,ld(op(X1,X2),unit))) = at(op(X1,X2),unit),
inference(orient,[status(thm)],[t2791]) ).
cnf(t1950,plain,
meet(X1,X2) = meet(meet(X1,X2),rd(op(X1,X3),X3)),
inference(cp,[status(thm)],[t1742,t1947]) ).
cnf(t4471,plain,
meet(meet(X1,X2),rd(op(X1,X3),X3)) = meet(X1,X2),
inference(orient,[status(thm)],[t1950]) ).
cnf(t4506,plain,
X1 = meet(X1,ld(meet(X2,X3),op(X2,X1))),
inference(cp,[status(thm)],[t454,t4471]) ).
cnf(t4554,plain,
meet(X1,ld(meet(X2,X3),op(X2,X1))) = X1,
inference(orient,[status(thm)],[t4506]) ).
cnf(t4570,plain,
X1 = meet(X1,ld(meet(X2,X3),op(X3,X1))),
inference(cp,[status(thm)],[t4554,t85]) ).
cnf(t4786,plain,
meet(X1,ld(meet(X2,X3),op(X3,X1))) = X1,
inference(orient,[status(thm)],[t4570]) ).
cnf(t223,plain,
unit = meet(unit,rd(X1,X1)),
inference(cp,[status(thm)],[t219,t48]) ).
cnf(t231,plain,
meet(unit,rd(X1,X1)) = unit,
inference(orient,[status(thm)],[t223]) ).
cnf(t4908,plain,
X1 = meet(X1,ld(unit,op(rd(X2,X2),X1))),
inference(cp,[status(thm)],[t4786,t231]) ).
cnf(t145070,plain,
X1 = meet(X1,op(rd(X2,X2),X1)),
inference(step,[status(thm)],[t4908,t1585]) ).
cnf(t4963,plain,
meet(X1,op(rd(X2,X2),X1)) = X1,
inference(orient,[status(thm)],[t145070]) ).
cnf(t364,plain,
unit = meet(unit,rd(X1,op(rd(X1,X2),X2))),
inference(cp,[status(thm)],[t242,t363]) ).
cnf(t487,plain,
meet(unit,rd(X1,op(rd(X1,X2),X2))) = unit,
inference(orient,[status(thm)],[t364]) ).
cnf(t489,plain,
op(rd(X1,X2),X2) = meet(op(rd(X1,X2),X2),ld(unit,X1)),
inference(cp,[status(thm)],[t454,t487]) ).
cnf(t144850,plain,
op(rd(X1,X2),X2) = meet(ld(unit,X1),op(rd(X1,X2),X2)),
inference(step,[status(thm)],[t489,t85]) ).
cnf(t1398,plain,
meet(ld(unit,X1),op(rd(X1,X2),X2)) = op(rd(X1,X2),X2),
inference(orient,[status(thm)],[t144850]) ).
cnf(t144877,plain,
meet(X1,op(rd(X1,X2),X2)) = op(rd(X1,X2),X2),
inference(step,[status(thm)],[t1398,t1585]) ).
cnf(t1609,plain,
meet(X1,op(rd(X1,X2),X2)) = op(rd(X1,X2),X2),
inference(rw,[status(thm)],[t144877]) ).
cnf(t1764,plain,
meet(X1,op(rd(X1,X2),X2)) = op(rd(X1,X2),X2),
inference(orient,[status(thm)],[t1609]) ).
cnf(t4964,plain,
X1 = op(rd(X1,X1),X1),
inference(cp,[status(thm)],[t4963,t1764]) ).
cnf(t5001,plain,
op(rd(X1,X1),X1) = X1,
inference(orient,[status(thm)],[t4964]) ).
cnf(t5002,plain,
op(rd(X1,X1),op(X1,X2)) = op(X1,X2),
inference(cp,[status(thm)],[t101,t5001]) ).
cnf(t5019,plain,
op(rd(X1,X1),op(X1,X2)) = op(X1,X2),
inference(orient,[status(thm)],[t5002]) ).
cnf(t30940,plain,
at(op(rd(X1,X1),op(X1,X2)),unit) = op(rd(X1,X1),op(op(X1,X2),ld(op(X1,X2),unit))),
inference(cp,[status(thm)],[t30931,t5019]) ).
cnf(t145715,plain,
at(op(X1,X2),unit) = op(rd(X1,X1),op(op(X1,X2),ld(op(X1,X2),unit))),
inference(step,[status(thm)],[t30940,t5019]) ).
cnf(t145716,plain,
at(op(X1,X2),unit) = op(rd(X1,X1),op(X1,op(X2,ld(op(X1,X2),unit)))),
inference(step,[status(thm)],[t145715,t101]) ).
cnf(t145717,plain,
at(op(X1,X2),unit) = op(rd(X1,X1),at(op(X1,X2),unit)),
inference(step,[status(thm)],[t145716,t30931]) ).
cnf(t54507,plain,
op(rd(X1,X1),at(op(X1,X2),unit)) = at(op(X1,X2),unit),
inference(orient,[status(thm)],[t145717]) ).
cnf(t54556,plain,
rd(op(rd(X1,X1),at(op(X1,X2),unit)),at(op(X1,X2),unit)) = join(rd(X1,X1),rd(at(op(X1,X2),unit),at(op(X1,X2),unit))),
inference(cp,[status(thm)],[t1947,t54507]) ).
cnf(t145718,plain,
rd(at(op(X1,X2),unit),at(op(X1,X2),unit)) = join(rd(X1,X1),rd(at(op(X1,X2),unit),at(op(X1,X2),unit))),
inference(step,[status(thm)],[t54556,t54507]) ).
cnf(t4569,plain,
X1 = meet(X1,ld(at(X2,unit),op(unit,X1))),
inference(cp,[status(thm)],[t4554,t2828]) ).
cnf(t145062,plain,
X1 = meet(X1,ld(at(X2,unit),X1)),
inference(step,[status(thm)],[t4569,t48]) ).
cnf(t4591,plain,
meet(X1,ld(at(X2,unit),X1)) = X1,
inference(orient,[status(thm)],[t145062]) ).
cnf(t4594,plain,
unit = meet(unit,ld(X1,ld(at(X2,unit),X1))),
inference(cp,[status(thm)],[t1694,t4591]) ).
cnf(t5115,plain,
meet(unit,ld(X1,ld(at(X2,unit),X1))) = unit,
inference(orient,[status(thm)],[t4594]) ).
cnf(t5123,plain,
ld(at(X1,unit),X2) = join(ld(at(X1,unit),X2),op(X2,unit)),
inference(cp,[status(thm)],[t162,t5115]) ).
cnf(t145075,plain,
ld(at(X1,unit),X2) = join(op(X2,unit),ld(at(X1,unit),X2)),
inference(step,[status(thm)],[t5123,t52]) ).
cnf(t145076,plain,
ld(at(X1,unit),X2) = join(X2,ld(at(X1,unit),X2)),
inference(step,[status(thm)],[t145075,t44]) ).
cnf(t5128,plain,
join(X1,ld(at(X2,unit),X1)) = ld(at(X2,unit),X1),
inference(orient,[status(thm)],[t145076]) ).
cnf(t5143,plain,
join(X1,ld(at(X2,unit),X1)) = rd(X1,ld(ld(at(X2,unit),X1),X1)),
inference(cp,[status(thm)],[t62,t5128]) ).
cnf(t145413,plain,
ld(at(X2,unit),X1) = rd(X1,ld(ld(at(X2,unit),X1),X1)),
inference(step,[status(thm)],[t5143,t5128]) ).
cnf(t33346,plain,
rd(X1,ld(ld(at(X2,unit),X1),X1)) = ld(at(X2,unit),X1),
inference(orient,[status(thm)],[t145413]) ).
cnf(t340,plain,
X1 = join(X1,op(meet(X2,X1),ld(X1,X1))),
inference(cp,[status(thm)],[t331,t119]) ).
cnf(t144771,plain,
X1 = join(X1,op(meet(X1,X2),ld(X1,X1))),
inference(step,[status(thm)],[t340,t85]) ).
cnf(t443,plain,
join(X1,op(meet(X1,X2),ld(X1,X1))) = X1,
inference(orient,[status(thm)],[t144771]) ).
cnf(t450,plain,
ld(X1,X1) = meet(ld(X1,X1),ld(meet(X1,X2),X1)),
inference(cp,[status(thm)],[t279,t443]) ).
cnf(t952,plain,
meet(ld(X1,X1),ld(meet(X1,X2),X1)) = ld(X1,X1),
inference(orient,[status(thm)],[t450]) ).
cnf(t1637,plain,
unit = meet(unit,join(X1,unit)),
inference(cp,[status(thm)],[t242,t1636]) ).
cnf(t1659,plain,
meet(unit,join(X1,unit)) = unit,
inference(orient,[status(thm)],[t1637]) ).
cnf(t3034,plain,
X1 = join(X1,op(rd(X1,join(X1,unit)),unit)),
inference(cp,[status(thm)],[t2990,t1659]) ).
cnf(t144998,plain,
X1 = join(X1,rd(X1,join(X1,unit))),
inference(step,[status(thm)],[t3034,t44]) ).
cnf(t3075,plain,
join(X1,rd(X1,join(X1,unit))) = X1,
inference(orient,[status(thm)],[t144998]) ).
cnf(t3080,plain,
unit = meet(unit,rd(X1,rd(X1,join(X1,unit)))),
inference(cp,[status(thm)],[t242,t3075]) ).
cnf(t3243,plain,
meet(unit,rd(X1,rd(X1,join(X1,unit)))) = unit,
inference(orient,[status(thm)],[t3080]) ).
cnf(t3251,plain,
rd(X1,join(X1,unit)) = meet(rd(X1,join(X1,unit)),ld(unit,X1)),
inference(cp,[status(thm)],[t454,t3243]) ).
cnf(t145006,plain,
rd(X1,join(X1,unit)) = meet(ld(unit,X1),rd(X1,join(X1,unit))),
inference(step,[status(thm)],[t3251,t85]) ).
cnf(t145007,plain,
rd(X1,join(X1,unit)) = meet(X1,rd(X1,join(X1,unit))),
inference(step,[status(thm)],[t145006,t1585]) ).
cnf(t3254,plain,
meet(X1,rd(X1,join(X1,unit))) = rd(X1,join(X1,unit)),
inference(orient,[status(thm)],[t145007]) ).
cnf(t3258,plain,
ld(X1,X1) = meet(ld(X1,X1),ld(rd(X1,join(X1,unit)),X1)),
inference(cp,[status(thm)],[t952,t3254]) ).
cnf(t145008,plain,
ld(X1,X1) = meet(ld(X1,X1),join(X1,unit)),
inference(step,[status(thm)],[t3258,t59]) ).
cnf(t3270,plain,
meet(ld(X1,X1),join(X1,unit)) = ld(X1,X1),
inference(orient,[status(thm)],[t145008]) ).
cnf(t3275,plain,
unit = meet(unit,ld(ld(X1,X1),join(X1,unit))),
inference(cp,[status(thm)],[t1694,t3270]) ).
cnf(t3351,plain,
meet(unit,ld(ld(X1,X1),join(X1,unit))) = unit,
inference(orient,[status(thm)],[t3275]) ).
cnf(t3359,plain,
join(X1,unit) = join(join(X1,unit),op(ld(X1,X1),unit)),
inference(cp,[status(thm)],[t162,t3351]) ).
cnf(t145015,plain,
join(X1,unit) = join(join(X1,unit),ld(X1,X1)),
inference(step,[status(thm)],[t3359,t44]) ).
cnf(t145016,plain,
join(X1,unit) = join(ld(X1,X1),join(X1,unit)),
inference(step,[status(thm)],[t145015,t52]) ).
cnf(t145017,plain,
join(X1,unit) = join(unit,join(ld(X1,X1),X1)),
inference(step,[status(thm)],[t145016,t65]) ).
cnf(t145018,plain,
join(X1,unit) = join(X1,join(unit,ld(X1,X1))),
inference(step,[status(thm)],[t145017,t65]) ).
cnf(t1852,plain,
ld(rd(X1,unit),X1) = join(unit,ld(X1,X1)),
inference(cp,[status(thm)],[t1851,t1636]) ).
cnf(t144929,plain,
ld(X1,X1) = join(unit,ld(X1,X1)),
inference(step,[status(thm)],[t1852,t1636]) ).
cnf(t1862,plain,
join(unit,ld(X1,X1)) = ld(X1,X1),
inference(orient,[status(thm)],[t144929]) ).
cnf(t145019,plain,
join(X1,unit) = join(X1,ld(X1,X1)),
inference(step,[status(thm)],[t145018,t1862]) ).
cnf(t3362,plain,
join(X1,ld(X1,X1)) = join(X1,unit),
inference(orient,[status(thm)],[t145019]) ).
cnf(t5129,plain,
ld(at(X1,unit),at(X1,unit)) = join(at(X1,unit),unit),
inference(cp,[status(thm)],[t5128,t3362]) ).
cnf(t145077,plain,
ld(at(X1,unit),at(X1,unit)) = join(unit,at(X1,unit)),
inference(step,[status(thm)],[t5129,t52]) ).
cnf(t2802,plain,
unit = join(unit,at(X1,unit)),
inference(cp,[status(thm)],[t182,t2790]) ).
cnf(t2817,plain,
join(unit,at(X1,unit)) = unit,
inference(orient,[status(thm)],[t2802]) ).
cnf(t145078,plain,
ld(at(X1,unit),at(X1,unit)) = unit,
inference(step,[status(thm)],[t145077,t2817]) ).
cnf(t5153,plain,
ld(at(X1,unit),at(X1,unit)) = unit,
inference(orient,[status(thm)],[t145078]) ).
cnf(t33348,plain,
ld(at(X1,unit),at(X1,unit)) = rd(at(X1,unit),ld(unit,at(X1,unit))),
inference(cp,[status(thm)],[t33346,t5153]) ).
cnf(t145414,plain,
unit = rd(at(X1,unit),ld(unit,at(X1,unit))),
inference(step,[status(thm)],[t33348,t5153]) ).
cnf(t145415,plain,
unit = rd(at(X1,unit),at(X1,unit)),
inference(step,[status(thm)],[t145414,t1585]) ).
cnf(t33369,plain,
rd(at(X1,unit),at(X1,unit)) = unit,
inference(orient,[status(thm)],[t145415]) ).
cnf(t145719,plain,
unit = join(rd(X1,X1),rd(at(op(X1,X2),unit),at(op(X1,X2),unit))),
inference(step,[status(thm)],[t145718,t33369]) ).
cnf(t145720,plain,
unit = join(rd(X1,X1),unit),
inference(step,[status(thm)],[t145719,t33369]) ).
cnf(t145721,plain,
unit = join(unit,rd(X1,X1)),
inference(step,[status(thm)],[t145720,t52]) ).
cnf(t1949,plain,
rd(op(unit,X1),X1) = join(unit,rd(X1,X1)),
inference(cp,[status(thm)],[t1947,t48]) ).
cnf(t144939,plain,
rd(X1,X1) = join(unit,rd(X1,X1)),
inference(step,[status(thm)],[t1949,t48]) ).
cnf(t1959,plain,
join(unit,rd(X1,X1)) = rd(X1,X1),
inference(orient,[status(thm)],[t144939]) ).
cnf(t145722,plain,
unit = rd(X1,X1),
inference(step,[status(thm)],[t145721,t1959]) ).
cnf(t54589,plain,
rd(X1,X1) = unit,
inference(orient,[status(thm)],[t145722]) ).
cnf(t145901,plain,
rd(X1,X2) = join(rd(X1,X2),op(unit,meet(X3,join(rd(X1,X2),rd(at(X1,X1),X2))))),
inference(step,[status(thm)],[t66227,t54589]) ).
cnf(t145902,plain,
rd(X1,X2) = join(rd(X1,X2),meet(X3,join(rd(X1,X2),rd(at(X1,X1),X2)))),
inference(step,[status(thm)],[t145901,t48]) ).
cnf(t145903,plain,
rd(X1,X2) = join(rd(X1,X2),meet(X3,rd(X1,X2))),
inference(step,[status(thm)],[t145902,t66152]) ).
cnf(t66284,plain,
join(rd(X1,X2),meet(X3,rd(X1,X2))) = rd(X1,X2),
inference(orient,[status(thm)],[t145903]) ).
cnf(t66294,plain,
rd(X1,ld(join(X1,X2),X1)) = join(join(X1,X2),meet(X3,rd(X1,ld(join(X1,X2),X1)))),
inference(cp,[status(thm)],[t66284,t62]) ).
cnf(t145904,plain,
join(X1,X2) = join(join(X1,X2),meet(X3,rd(X1,ld(join(X1,X2),X1)))),
inference(step,[status(thm)],[t66294,t62]) ).
cnf(t145905,plain,
join(X1,X2) = join(join(X1,X2),meet(X3,join(X1,X2))),
inference(step,[status(thm)],[t145904,t62]) ).
cnf(t66481,plain,
join(join(X1,X2),meet(X3,join(X1,X2))) = join(X1,X2),
inference(orient,[status(thm)],[t145905]) ).
cnf(t1704,plain,
unit = meet(unit,ld(X1,rd(X2,ld(X1,X2)))),
inference(cp,[status(thm)],[t1694,t215]) ).
cnf(t1989,plain,
meet(unit,ld(X1,rd(X2,ld(X1,X2)))) = unit,
inference(orient,[status(thm)],[t1704]) ).
cnf(t1993,plain,
rd(X1,ld(X2,X1)) = join(rd(X1,ld(X2,X1)),op(X2,unit)),
inference(cp,[status(thm)],[t162,t1989]) ).
cnf(t144943,plain,
rd(X1,ld(X2,X1)) = join(op(X2,unit),rd(X1,ld(X2,X1))),
inference(step,[status(thm)],[t1993,t52]) ).
cnf(t144944,plain,
rd(X1,ld(X2,X1)) = join(X2,rd(X1,ld(X2,X1))),
inference(step,[status(thm)],[t144943,t44]) ).
cnf(t1996,plain,
join(X1,rd(X2,ld(X1,X2))) = rd(X2,ld(X1,X2)),
inference(orient,[status(thm)],[t144944]) ).
cnf(t1998,plain,
meet(X1,X2) = meet(meet(X1,X2),rd(X3,ld(X1,X3))),
inference(cp,[status(thm)],[t1742,t1996]) ).
cnf(t6849,plain,
meet(meet(X1,X2),rd(X3,ld(X1,X3))) = meet(X1,X2),
inference(orient,[status(thm)],[t1998]) ).
cnf(t6897,plain,
X1 = join(X1,op(meet(X2,X3),ld(X2,X1))),
inference(cp,[status(thm)],[t331,t6849]) ).
cnf(t6900,plain,
join(X1,op(meet(X2,X3),ld(X2,X1))) = X1,
inference(orient,[status(thm)],[t6897]) ).
cnf(t6917,plain,
X1 = join(X1,op(meet(X2,X3),ld(X3,X1))),
inference(cp,[status(thm)],[t6900,t85]) ).
cnf(t6967,plain,
join(X1,op(meet(X2,X3),ld(X3,X1))) = X1,
inference(orient,[status(thm)],[t6917]) ).
cnf(t7028,plain,
X1 = join(X1,op(X2,ld(join(X2,X3),X1))),
inference(cp,[status(thm)],[t6967,t120]) ).
cnf(t7172,plain,
join(X1,op(X2,ld(join(X2,X3),X1))) = X1,
inference(orient,[status(thm)],[t7028]) ).
cnf(t7207,plain,
ld(join(X1,X2),X3) = meet(ld(join(X1,X2),X3),ld(X1,X3)),
inference(cp,[status(thm)],[t279,t7172]) ).
cnf(t145504,plain,
ld(join(X1,X2),X3) = meet(ld(X1,X3),ld(join(X1,X2),X3)),
inference(step,[status(thm)],[t7207,t85]) ).
cnf(t36815,plain,
meet(ld(X1,X2),ld(join(X1,X3),X2)) = ld(join(X1,X3),X2),
inference(orient,[status(thm)],[t145504]) ).
cnf(t36886,plain,
ld(X1,X2) = join(ld(X1,X2),ld(join(X1,X3),X2)),
inference(cp,[status(thm)],[t108,t36815]) ).
cnf(t36949,plain,
join(ld(X1,X2),ld(join(X1,X3),X2)) = ld(X1,X2),
inference(orient,[status(thm)],[t36886]) ).
cnf(t66594,plain,
join(ld(X1,X2),ld(join(X1,X3),X2)) = join(ld(X1,X2),meet(Y3,join(ld(X1,X2),ld(join(X1,X3),X2)))),
inference(cp,[status(thm)],[t66481,t36949]) ).
cnf(t145906,plain,
ld(X1,X2) = join(ld(X1,X2),meet(Y3,join(ld(X1,X2),ld(join(X1,X3),X2)))),
inference(step,[status(thm)],[t66594,t36949]) ).
cnf(t145907,plain,
ld(X1,X2) = join(ld(X1,X2),meet(Y3,ld(X1,X2))),
inference(step,[status(thm)],[t145906,t36949]) ).
cnf(t66880,plain,
join(ld(X1,X2),meet(X3,ld(X1,X2))) = ld(X1,X2),
inference(orient,[status(thm)],[t145907]) ).
cnf(t210,plain,
op(X1,X2) = meet(op(X1,X2),rd(join(X3,op(X1,op(X2,Y3))),Y3)),
inference(cp,[status(thm)],[t203,t101]) ).
cnf(t6301,plain,
meet(op(X1,X2),rd(join(X3,op(X1,op(X2,Y3))),Y3)) = op(X1,X2),
inference(orient,[status(thm)],[t210]) ).
cnf(t3568,plain,
X1 = join(X1,op(rd(X1,X2),op(rd(X2,X3),X3))),
inference(cp,[status(thm)],[t3560,t1764]) ).
cnf(t113403,plain,
join(X1,op(rd(X1,X2),op(rd(X2,X3),X3))) = X1,
inference(orient,[status(thm)],[t3568]) ).
cnf(t113417,plain,
X1 = join(X1,op(X1,op(rd(unit,X2),X2))),
inference(cp,[status(thm)],[t113403,t1636]) ).
cnf(t113533,plain,
join(X1,op(X1,op(rd(unit,X2),X2))) = X1,
inference(orient,[status(thm)],[t113417]) ).
cnf(t113618,plain,
op(X1,rd(unit,X2)) = meet(op(X1,rd(unit,X2)),rd(X1,X2)),
inference(cp,[status(thm)],[t6301,t113533]) ).
cnf(t146147,plain,
op(X1,rd(unit,X2)) = meet(rd(X1,X2),op(X1,rd(unit,X2))),
inference(step,[status(thm)],[t113618,t85]) ).
cnf(t113829,plain,
meet(rd(X1,X2),op(X1,rd(unit,X2))) = op(X1,rd(unit,X2)),
inference(orient,[status(thm)],[t146147]) ).
cnf(t113830,plain,
op(X1,rd(unit,X1)) = meet(unit,op(X1,rd(unit,X1))),
inference(cp,[status(thm)],[t113829,t54589]) ).
cnf(t114014,plain,
meet(unit,op(X1,rd(unit,X1))) = op(X1,rd(unit,X1)),
inference(orient,[status(thm)],[t113830]) ).
cnf(t114044,plain,
unit = join(unit,op(X1,rd(unit,X1))),
inference(cp,[status(thm)],[t108,t114014]) ).
cnf(t114185,plain,
join(unit,op(X1,rd(unit,X1))) = unit,
inference(orient,[status(thm)],[t114044]) ).
cnf(t114275,plain,
rd(unit,X1) = meet(rd(unit,X1),ld(X1,unit)),
inference(cp,[status(thm)],[t279,t114185]) ).
cnf(t114406,plain,
meet(rd(unit,X1),ld(X1,unit)) = rd(unit,X1),
inference(orient,[status(thm)],[t114275]) ).
cnf(t114470,plain,
ld(X1,unit) = join(ld(X1,unit),rd(unit,X1)),
inference(cp,[status(thm)],[t66880,t114406]) ).
cnf(t146148,plain,
ld(X1,unit) = join(rd(unit,X1),ld(X1,unit)),
inference(step,[status(thm)],[t114470,t52]) ).
cnf(t114545,plain,
join(rd(unit,X1),ld(X1,unit)) = ld(X1,unit),
inference(orient,[status(thm)],[t146148]) ).
cnf(t114597,plain,
ld(ld(X1,unit),unit) = join(rd(unit,ld(X1,unit)),at(unit,X1)),
inference(cp,[status(thm)],[t114545,t1672]) ).
cnf(t146166,plain,
at(unit,X1) = join(rd(unit,ld(X1,unit)),at(unit,X1)),
inference(step,[status(thm)],[t114597,t1672]) ).
cnf(t146167,plain,
at(unit,X1) = join(at(unit,X1),rd(unit,ld(X1,unit))),
inference(step,[status(thm)],[t146166,t52]) ).
cnf(t117972,plain,
join(at(unit,X1),rd(unit,ld(X1,unit))) = at(unit,X1),
inference(orient,[status(thm)],[t146167]) ).
cnf(t118082,plain,
X1 = meet(X1,at(unit,X1)),
inference(cp,[status(thm)],[t2770,t117972]) ).
cnf(t118096,plain,
meet(X1,at(unit,X1)) = X1,
inference(orient,[status(thm)],[t118082]) ).
cnf(t118163,plain,
unit = join(unit,op(ld(X1,unit),X1)),
inference(cp,[status(thm)],[t79779,t118096]) ).
cnf(t119109,plain,
join(unit,op(ld(X1,unit),X1)) = unit,
inference(orient,[status(thm)],[t118163]) ).
cnf(t119172,plain,
ld(X1,unit) = meet(ld(X1,unit),rd(unit,X1)),
inference(cp,[status(thm)],[t203,t119109]) ).
cnf(t146176,plain,
ld(X1,unit) = meet(rd(unit,X1),ld(X1,unit)),
inference(step,[status(thm)],[t119172,t85]) ).
cnf(t146177,plain,
ld(X1,unit) = rd(unit,X1),
inference(step,[status(thm)],[t146176,t114406]) ).
cnf(t120475,plain,
ld(X1,unit) = rd(unit,X1),
inference(orient,[status(thm)],[t146177]) ).
cnf(t1674,plain,
at(unit,ld(X1,unit)) = ld(at(unit,X1),unit),
inference(cp,[status(thm)],[t1672,t1672]) ).
cnf(t1685,plain,
at(unit,ld(X1,unit)) = ld(at(unit,X1),unit),
inference(orient,[status(thm)],[t1674]) ).
cnf(t146195,plain,
at(unit,rd(unit,X1)) = ld(at(unit,X1),unit),
inference(step,[status(thm)],[t1685,t120475]) ).
cnf(t146196,plain,
at(unit,rd(unit,X1)) = rd(unit,at(unit,X1)),
inference(step,[status(thm)],[t146195,t120475]) ).
cnf(t120615,plain,
at(unit,rd(unit,X1)) = rd(unit,at(unit,X1)),
inference(rw,[status(thm)],[t146196]) ).
cnf(t120935,plain,
at(unit,rd(unit,X1)) = rd(unit,at(unit,X1)),
inference(orient,[status(thm)],[t120615]) ).
cnf(t1701,plain,
unit = meet(unit,ld(X1,ld(X2,op(X2,X1)))),
inference(cp,[status(thm)],[t1694,t292]) ).
cnf(t1922,plain,
meet(unit,ld(X1,ld(X2,op(X2,X1)))) = unit,
inference(orient,[status(thm)],[t1701]) ).
cnf(t1926,plain,
ld(X1,op(X1,X2)) = join(ld(X1,op(X1,X2)),op(X2,unit)),
inference(cp,[status(thm)],[t162,t1922]) ).
cnf(t144935,plain,
ld(X1,op(X1,X2)) = join(op(X2,unit),ld(X1,op(X1,X2))),
inference(step,[status(thm)],[t1926,t52]) ).
cnf(t144936,plain,
ld(X1,op(X1,X2)) = join(X2,ld(X1,op(X1,X2))),
inference(step,[status(thm)],[t144935,t44]) ).
cnf(t1929,plain,
join(X1,ld(X2,op(X2,X1))) = ld(X2,op(X2,X1)),
inference(orient,[status(thm)],[t144936]) ).
cnf(t2442,plain,
meet(X1,X2) = meet(meet(X1,X2),ld(X3,op(X3,X2))),
inference(cp,[status(thm)],[t2369,t1929]) ).
cnf(t13854,plain,
meet(meet(X1,X2),ld(X3,op(X3,X2))) = meet(X1,X2),
inference(orient,[status(thm)],[t2442]) ).
cnf(t13951,plain,
meet(X1,join(X1,X2)) = meet(X1,ld(X3,op(X3,join(X1,X2)))),
inference(cp,[status(thm)],[t13854,t120]) ).
cnf(t145242,plain,
X1 = meet(X1,ld(X3,op(X3,join(X1,X2)))),
inference(step,[status(thm)],[t13951,t120]) ).
cnf(t14138,plain,
meet(X1,ld(X2,op(X2,join(X1,X3)))) = X1,
inference(orient,[status(thm)],[t145242]) ).
cnf(t14192,plain,
X1 = meet(X1,rd(op(X1,join(X2,X3)),X2)),
inference(cp,[status(thm)],[t393,t14138]) ).
cnf(t14199,plain,
meet(X1,rd(op(X1,join(X2,X3)),X2)) = X1,
inference(orient,[status(thm)],[t14192]) ).
cnf(t246,plain,
unit = meet(unit,rd(join(X1,X2),join(X2,meet(X1,X3)))),
inference(cp,[status(thm)],[t242,t142]) ).
cnf(t14955,plain,
meet(unit,rd(join(X1,X2),join(X2,meet(X1,X3)))) = unit,
inference(orient,[status(thm)],[t246]) ).
cnf(t15386,plain,
join(X1,meet(X2,X3)) = meet(join(X1,meet(X2,X3)),ld(unit,join(X2,X1))),
inference(cp,[status(thm)],[t454,t14955]) ).
cnf(t145550,plain,
join(X1,meet(X2,X3)) = meet(ld(unit,join(X2,X1)),join(X1,meet(X2,X3))),
inference(step,[status(thm)],[t15386,t85]) ).
cnf(t145551,plain,
join(X1,meet(X2,X3)) = meet(join(X2,X1),join(X1,meet(X2,X3))),
inference(step,[status(thm)],[t145550,t1585]) ).
cnf(t145552,plain,
join(X1,meet(X2,X3)) = meet(join(X1,X2),join(X1,meet(X2,X3))),
inference(step,[status(thm)],[t145551,t52]) ).
cnf(t41728,plain,
meet(join(X1,X2),join(X1,meet(X2,X3))) = join(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t145552]) ).
cnf(t4600,plain,
X1 = join(X1,op(at(X2,unit),X1)),
inference(cp,[status(thm)],[t162,t4591]) ).
cnf(t4619,plain,
join(X1,op(at(X2,unit),X1)) = X1,
inference(orient,[status(thm)],[t4600]) ).
cnf(t41806,plain,
join(X1,meet(op(at(X2,unit),X1),X3)) = meet(X1,join(X1,meet(op(at(X2,unit),X1),X3))),
inference(cp,[status(thm)],[t41728,t4619]) ).
cnf(t145561,plain,
join(X1,meet(X3,op(at(X2,unit),X1))) = meet(X1,join(X1,meet(op(at(X2,unit),X1),X3))),
inference(step,[status(thm)],[t41806,t85]) ).
cnf(t145562,plain,
join(X1,meet(X3,op(at(X2,unit),X1))) = X1,
inference(step,[status(thm)],[t145561,t120]) ).
cnf(t42532,plain,
join(X1,meet(X2,op(at(X3,unit),X1))) = X1,
inference(orient,[status(thm)],[t145562]) ).
cnf(t42556,plain,
at(unit,X1) = join(at(unit,X1),meet(X2,at(X3,X1))),
inference(cp,[status(thm)],[t42532,t3444]) ).
cnf(t43808,plain,
join(at(unit,X1),meet(X2,at(X3,X1))) = at(unit,X1),
inference(orient,[status(thm)],[t42556]) ).
cnf(t118123,plain,
at(unit,X1) = join(at(unit,X1),X1),
inference(cp,[status(thm)],[t43808,t118096]) ).
cnf(t146168,plain,
at(unit,X1) = join(X1,at(unit,X1)),
inference(step,[status(thm)],[t118123,t52]) ).
cnf(t118188,plain,
join(X1,at(unit,X1)) = at(unit,X1),
inference(orient,[status(thm)],[t146168]) ).
cnf(t118313,plain,
X1 = meet(X1,rd(op(X1,at(unit,X2)),X2)),
inference(cp,[status(thm)],[t14199,t118188]) ).
cnf(t128172,plain,
meet(X1,rd(op(X1,at(unit,X2)),X2)) = X1,
inference(orient,[status(thm)],[t118313]) ).
cnf(t146192,plain,
op(rd(unit,X1),at(unit,X1)) = at(ld(X1,unit),unit),
inference(step,[status(thm)],[t2900,t120475]) ).
cnf(t146193,plain,
op(rd(unit,X1),at(unit,X1)) = at(rd(unit,X1),unit),
inference(step,[status(thm)],[t146192,t120475]) ).
cnf(t120613,plain,
op(rd(unit,X1),at(unit,X1)) = at(rd(unit,X1),unit),
inference(rw,[status(thm)],[t146193]) ).
cnf(t122408,plain,
op(rd(unit,X1),at(unit,X1)) = at(rd(unit,X1),unit),
inference(orient,[status(thm)],[t120613]) ).
cnf(t128173,plain,
rd(unit,X1) = meet(rd(unit,X1),rd(at(rd(unit,X1),unit),X1)),
inference(cp,[status(thm)],[t128172,t122408]) ).
cnf(t28979,plain,
X1 = meet(X1,rd(X2,ld(X1,meet(X2,X3)))),
inference(cp,[status(thm)],[t28873,t108]) ).
cnf(t29106,plain,
meet(X1,rd(X2,ld(X1,meet(X2,X3)))) = X1,
inference(orient,[status(thm)],[t28979]) ).
cnf(t29171,plain,
ld(X1,meet(X2,X3)) = meet(ld(X1,meet(X2,X3)),ld(X1,X2)),
inference(cp,[status(thm)],[t454,t29106]) ).
cnf(t145709,plain,
ld(X1,meet(X2,X3)) = meet(ld(X1,X2),ld(X1,meet(X2,X3))),
inference(step,[status(thm)],[t29171,t85]) ).
cnf(t52412,plain,
meet(ld(X1,X2),ld(X1,meet(X2,X3))) = ld(X1,meet(X2,X3)),
inference(orient,[status(thm)],[t145709]) ).
cnf(t52609,plain,
meet(X1,ld(rd(meet(X2,X3),X1),X2)) = meet(X1,ld(rd(meet(X2,X3),X1),meet(X2,X3))),
inference(cp,[status(thm)],[t934,t52412]) ).
cnf(t145710,plain,
meet(X1,ld(rd(meet(X2,X3),X1),X2)) = X1,
inference(step,[status(thm)],[t52609,t373]) ).
cnf(t52612,plain,
meet(X1,ld(rd(meet(X2,X3),X1),X2)) = X1,
inference(orient,[status(thm)],[t145710]) ).
cnf(t52696,plain,
X1 = meet(X1,ld(rd(at(X2,unit),X1),unit)),
inference(cp,[status(thm)],[t52612,t2828]) ).
cnf(t52748,plain,
meet(X1,ld(rd(at(X2,unit),X1),unit)) = X1,
inference(orient,[status(thm)],[t52696]) ).
cnf(t52806,plain,
rd(at(X1,unit),X2) = meet(rd(at(X1,unit),X2),rd(unit,X2)),
inference(cp,[status(thm)],[t393,t52748]) ).
cnf(t145912,plain,
rd(at(X1,unit),X2) = meet(rd(unit,X2),rd(at(X1,unit),X2)),
inference(step,[status(thm)],[t52806,t85]) ).
cnf(t67708,plain,
meet(rd(unit,X1),rd(at(X2,unit),X1)) = rd(at(X2,unit),X1),
inference(orient,[status(thm)],[t145912]) ).
cnf(t146309,plain,
rd(unit,X1) = rd(at(rd(unit,X1),unit),X1),
inference(step,[status(thm)],[t128173,t67708]) ).
cnf(t128268,plain,
rd(at(rd(unit,X1),unit),X1) = rd(unit,X1),
inference(orient,[status(thm)],[t146309]) ).
cnf(t146197,plain,
rd(unit,ld(X1,unit)) = at(unit,X1),
inference(step,[status(thm)],[t1672,t120475]) ).
cnf(t146198,plain,
rd(unit,rd(unit,X1)) = at(unit,X1),
inference(step,[status(thm)],[t146197,t120475]) ).
cnf(t120616,plain,
rd(unit,rd(unit,X1)) = at(unit,X1),
inference(rw,[status(thm)],[t146198]) ).
cnf(t120839,plain,
rd(unit,rd(unit,X1)) = at(unit,X1),
inference(orient,[status(thm)],[t120616]) ).
cnf(t128269,plain,
rd(unit,rd(unit,X1)) = rd(at(at(unit,X1),unit),rd(unit,X1)),
inference(cp,[status(thm)],[t128268,t120839]) ).
cnf(t146391,plain,
at(unit,X1) = rd(at(at(unit,X1),unit),rd(unit,X1)),
inference(step,[status(thm)],[t128269,t120839]) ).
cnf(t144573,plain,
rd(at(at(unit,X1),unit),rd(unit,X1)) = at(unit,X1),
inference(orient,[status(thm)],[t146391]) ).
cnf(t144612,plain,
ld(rd(at(at(unit,X1),unit),rd(unit,X1)),at(at(unit,X1),unit)) = join(rd(unit,X1),ld(at(unit,X1),at(at(unit,X1),unit))),
inference(cp,[status(thm)],[t1851,t144573]) ).
cnf(t146392,plain,
ld(at(unit,X1),at(at(unit,X1),unit)) = join(rd(unit,X1),ld(at(unit,X1),at(at(unit,X1),unit))),
inference(step,[status(thm)],[t144612,t144573]) ).
cnf(t2798,plain,
ld(X1,op(X1,ld(X1,unit))) = join(ld(X1,unit),ld(X1,at(X1,unit))),
inference(cp,[status(thm)],[t1929,t2790]) ).
cnf(t145383,plain,
ld(X1,at(X1,unit)) = join(ld(X1,unit),ld(X1,at(X1,unit))),
inference(step,[status(thm)],[t2798,t2790]) ).
cnf(t31062,plain,
join(ld(X1,unit),ld(X1,at(X1,unit))) = ld(X1,at(X1,unit)),
inference(orient,[status(thm)],[t145383]) ).
cnf(t52536,plain,
ld(X1,X2) = join(ld(X1,X2),ld(X1,meet(X2,X3))),
inference(cp,[status(thm)],[t108,t52412]) ).
cnf(t53528,plain,
join(ld(X1,X2),ld(X1,meet(X2,X3))) = ld(X1,X2),
inference(orient,[status(thm)],[t52536]) ).
cnf(t53647,plain,
ld(X1,unit) = join(ld(X1,unit),ld(X1,at(X2,unit))),
inference(cp,[status(thm)],[t53528,t2828]) ).
cnf(t53942,plain,
join(ld(X1,unit),ld(X1,at(X2,unit))) = ld(X1,unit),
inference(orient,[status(thm)],[t53647]) ).
cnf(t145712,plain,
ld(X1,unit) = ld(X1,at(X1,unit)),
inference(step,[status(thm)],[t31062,t53942]) ).
cnf(t54039,plain,
ld(X1,unit) = ld(X1,at(X1,unit)),
inference(rw,[status(thm)],[t145712]) ).
cnf(t54040,plain,
ld(X1,at(X1,unit)) = ld(X1,unit),
inference(orient,[status(thm)],[t54039]) ).
cnf(t146190,plain,
ld(X1,at(X1,unit)) = rd(unit,X1),
inference(step,[status(thm)],[t54040,t120475]) ).
cnf(t120488,plain,
ld(X1,at(X1,unit)) = rd(unit,X1),
inference(orient,[status(thm)],[t146190]) ).
cnf(t146393,plain,
rd(unit,at(unit,X1)) = join(rd(unit,X1),ld(at(unit,X1),at(at(unit,X1),unit))),
inference(step,[status(thm)],[t146392,t120488]) ).
cnf(t146394,plain,
rd(unit,at(unit,X1)) = join(rd(unit,X1),rd(unit,at(unit,X1))),
inference(step,[status(thm)],[t146393,t120488]) ).
cnf(t2441,plain,
meet(X1,X2) = meet(meet(X1,X2),ld(rd(X3,X2),X3)),
inference(cp,[status(thm)],[t2369,t1851]) ).
cnf(t10445,plain,
meet(meet(X1,X2),ld(rd(X3,X2),X3)) = meet(X1,X2),
inference(orient,[status(thm)],[t2441]) ).
cnf(t10514,plain,
meet(X1,join(X1,X2)) = meet(X1,ld(rd(X3,join(X1,X2)),X3)),
inference(cp,[status(thm)],[t10445,t120]) ).
cnf(t145197,plain,
X1 = meet(X1,ld(rd(X3,join(X1,X2)),X3)),
inference(step,[status(thm)],[t10514,t120]) ).
cnf(t10679,plain,
meet(X1,ld(rd(X2,join(X1,X3)),X2)) = X1,
inference(orient,[status(thm)],[t145197]) ).
cnf(t10727,plain,
rd(X1,join(X2,X3)) = meet(rd(X1,join(X2,X3)),rd(X1,X2)),
inference(cp,[status(thm)],[t393,t10679]) ).
cnf(t145527,plain,
rd(X1,join(X2,X3)) = meet(rd(X1,X2),rd(X1,join(X2,X3))),
inference(step,[status(thm)],[t10727,t85]) ).
cnf(t39220,plain,
meet(rd(X1,X2),rd(X1,join(X2,X3))) = rd(X1,join(X2,X3)),
inference(orient,[status(thm)],[t145527]) ).
cnf(t39302,plain,
rd(X1,X2) = join(rd(X1,X2),rd(X1,join(X2,X3))),
inference(cp,[status(thm)],[t108,t39220]) ).
cnf(t39369,plain,
join(rd(X1,X2),rd(X1,join(X2,X3))) = rd(X1,X2),
inference(orient,[status(thm)],[t39302]) ).
cnf(t118228,plain,
rd(X1,X2) = join(rd(X1,X2),rd(X1,at(unit,X2))),
inference(cp,[status(thm)],[t39369,t118188]) ).
cnf(t139439,plain,
join(rd(X1,X2),rd(X1,at(unit,X2))) = rd(X1,X2),
inference(orient,[status(thm)],[t118228]) ).
cnf(t146395,plain,
rd(unit,at(unit,X1)) = rd(unit,X1),
inference(step,[status(thm)],[t146394,t139439]) ).
cnf(t144660,plain,
rd(unit,at(unit,X1)) = rd(unit,X1),
inference(orient,[status(thm)],[t146395]) ).
cnf(t146396,plain,
at(unit,rd(unit,X1)) = rd(unit,X1),
inference(step,[status(thm)],[t120935,t144660]) ).
cnf(t144661,plain,
at(unit,rd(unit,X1)) = rd(unit,X1),
inference(orient,[status(thm)],[t146396]) ).
cnf(goal_0,negated_conjecture,
at(unit,ld(x,unit)) != ld(x,unit),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
at(unit,rd(unit,x)) != ld(x,unit),
inference(rw,[status(thm)],[goal_0,t120475]) ).
cnf(g0_1,plain,
rd(unit,x) != ld(x,unit),
inference(rw,[status(thm)],[g0_0,t144661]) ).
cnf(g0_2,plain,
rd(unit,x) != rd(unit,x),
inference(rw,[status(thm)],[g0_1,t120475]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_2]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : MVA011-1 : TPTP v9.3.1. Released v8.1.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.09/0.36 % Computer : n003.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Thu Sep 24 01:35:50 UTC 2026
% 0.02/0.36 % CPUTime :
% 0.02/0.36 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 67.84/10.53 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 67.84/10.53 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------