%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : LAT029-1 : TPTP v9.3.1. Released v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n019.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:02 PM UTC 2026
% Result : Unsatisfiable 5.42s 1.60s
% Output : Proof 5.42s
% Verified :
% SZS Type : Refutation
% Derivation depth : 85
% Number of leaves : 7
% Syntax : Number of formulae : 156 ( 152 unt; 0 def)
% Number of atoms : 168 ( 167 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 42 ( 30 ~; 12 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 5 ( 1 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 7 ( 7 usr; 4 con; 0-4 aty)
% Number of variables : 291 ( 75 sgn 24 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f0,axiom,
join(meet(X,Y),meet(X,join(X,Y))) = X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',wal_absorbtion_1) ).
fof(f0_nnf,plain,
! [X,Y] : join(meet(X,Y),meet(X,join(X,Y))) = X,
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
! [X,Y] : join(meet(X,Y),meet(X,join(X,Y))) = X,
inference(skolemisation,[status(esa)],[f0_nnf]) ).
cnf(c0,plain,
join(meet(X0,X1),meet(X0,join(X0,X1))) = X0,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(t3,plain,
join(meet(X1,X2),meet(X1,join(X1,X2))) = X1,
inference(equality_encoding,[status(esa)],[c0]) ).
cnf(t13,plain,
join(meet(X1,X2),meet(X1,join(X1,X2))) = X1,
inference(orient,[status(thm)],[t3]) ).
cnf(f1,axiom,
join(meet(X,X),meet(Y,join(X,X))) = X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',wal_absorbtion_2) ).
fof(f1_nnf,plain,
! [X,Y] : join(meet(X,X),meet(Y,join(X,X))) = X,
inference(nnf_transformation,[status(thm)],[f1]) ).
fof(f1_sk,plain,
! [X,Y] : join(meet(X,X),meet(Y,join(X,X))) = X,
inference(skolemisation,[status(esa)],[f1_nnf]) ).
cnf(c1,plain,
join(meet(X0,X0),meet(X1,join(X0,X0))) = X0,
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(t2,plain,
join(meet(X1,X1),meet(X2,join(X1,X1))) = X1,
inference(equality_encoding,[status(esa)],[c1]) ).
cnf(t20,plain,
join(meet(X1,X1),meet(X2,join(X1,X1))) = X1,
inference(orient,[status(thm)],[t2]) ).
cnf(f3,axiom,
meet(meet(join(X,Y),join(Z,X)),X) = X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',wal_absorbtion_4) ).
fof(f3_nnf,plain,
! [X,Y,Z] : meet(meet(join(X,Y),join(Z,X)),X) = X,
inference(nnf_transformation,[status(thm)],[f3]) ).
fof(f3_sk,plain,
! [X,Y,Z] : meet(meet(join(X,Y),join(Z,X)),X) = X,
inference(skolemisation,[status(esa)],[f3_nnf]) ).
cnf(c3,plain,
meet(meet(join(X0,X1),join(X2,X0)),X0) = X0,
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(t5,plain,
meet(meet(join(X1,X2),join(X3,X1)),X1) = X1,
inference(equality_encoding,[status(esa)],[c3]) ).
cnf(t7,plain,
meet(meet(join(X1,X2),join(X3,X1)),X1) = X1,
inference(orient,[status(thm)],[t5]) ).
cnf(f4,axiom,
join(join(meet(X,Y),meet(Z,X)),X) = X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',wal_absorbtion_5) ).
fof(f4_nnf,plain,
! [X,Y,Z] : join(join(meet(X,Y),meet(Z,X)),X) = X,
inference(nnf_transformation,[status(thm)],[f4]) ).
fof(f4_sk,plain,
! [X,Y,Z] : join(join(meet(X,Y),meet(Z,X)),X) = X,
inference(skolemisation,[status(esa)],[f4_nnf]) ).
cnf(c4,plain,
join(join(meet(X0,X1),meet(X2,X0)),X0) = X0,
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(t1,plain,
join(join(meet(X1,X2),meet(X3,X1)),X1) = X1,
inference(equality_encoding,[status(esa)],[c4]) ).
cnf(t26,plain,
join(join(meet(X1,X2),meet(X3,X1)),X1) = X1,
inference(orient,[status(thm)],[t1]) ).
cnf(t30,plain,
X1 = meet(meet(join(X1,X2),X1),X1),
inference(cp,[status(thm)],[t7,t26]) ).
cnf(t46,plain,
meet(meet(join(X1,X2),X1),X1) = X1,
inference(orient,[status(thm)],[t30]) ).
cnf(t52,plain,
meet(X1,X2) = meet(meet(X1,meet(X1,X2)),meet(X1,X2)),
inference(cp,[status(thm)],[t46,t13]) ).
cnf(t113,plain,
meet(meet(X1,meet(X1,X2)),meet(X1,X2)) = meet(X1,X2),
inference(orient,[status(thm)],[t52]) ).
cnf(f2,axiom,
join(meet(X,Y),meet(Y,join(X,Y))) = Y,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',wal_absorbtion_3) ).
fof(f2_nnf,plain,
! [X,Y] : join(meet(X,Y),meet(Y,join(X,Y))) = Y,
inference(nnf_transformation,[status(thm)],[f2]) ).
fof(f2_sk,plain,
! [X,Y] : join(meet(X,Y),meet(Y,join(X,Y))) = Y,
inference(skolemisation,[status(esa)],[f2_nnf]) ).
cnf(c2,plain,
join(meet(X0,X1),meet(X1,join(X0,X1))) = X1,
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(t4,plain,
join(meet(X1,X2),meet(X2,join(X1,X2))) = X2,
inference(equality_encoding,[status(esa)],[c2]) ).
cnf(t8,plain,
join(meet(X1,X2),meet(X2,join(X1,X2))) = X2,
inference(orient,[status(thm)],[t4]) ).
cnf(t51,plain,
meet(X1,X2) = meet(meet(X2,meet(X1,X2)),meet(X1,X2)),
inference(cp,[status(thm)],[t46,t8]) ).
cnf(t62,plain,
meet(meet(X1,meet(X2,X1)),meet(X2,X1)) = meet(X2,X1),
inference(orient,[status(thm)],[t51]) ).
cnf(t63,plain,
meet(meet(join(X1,X2),join(X3,X1)),X1) = meet(meet(X1,X1),meet(meet(join(X1,X2),join(X3,X1)),X1)),
inference(cp,[status(thm)],[t62,t7]) ).
cnf(t1581,plain,
X1 = meet(meet(X1,X1),meet(meet(join(X1,X2),join(X3,X1)),X1)),
inference(step,[status(thm)],[t63,t7]) ).
cnf(t1582,plain,
X1 = meet(meet(X1,X1),X1),
inference(step,[status(thm)],[t1581,t7]) ).
cnf(t73,plain,
meet(meet(X1,X1),X1) = X1,
inference(orient,[status(thm)],[t1582]) ).
cnf(t77,plain,
X1 = join(X1,meet(X1,join(meet(X1,X1),X1))),
inference(cp,[status(thm)],[t8,t73]) ).
cnf(t78,plain,
join(X1,meet(X1,join(meet(X1,X1),X1))) = X1,
inference(orient,[status(thm)],[t77]) ).
cnf(t79,plain,
X1 = meet(meet(X1,join(X2,X1)),X1),
inference(cp,[status(thm)],[t7,t78]) ).
cnf(t83,plain,
meet(meet(X1,join(X2,X1)),X1) = X1,
inference(orient,[status(thm)],[t79]) ).
cnf(t116,plain,
meet(meet(X1,join(X2,X1)),X1) = meet(meet(meet(X1,join(X2,X1)),X1),meet(meet(X1,join(X2,X1)),X1)),
inference(cp,[status(thm)],[t113,t83]) ).
cnf(t1585,plain,
X1 = meet(meet(meet(X1,join(X2,X1)),X1),meet(meet(X1,join(X2,X1)),X1)),
inference(step,[status(thm)],[t116,t83]) ).
cnf(t1586,plain,
X1 = meet(X1,meet(meet(X1,join(X2,X1)),X1)),
inference(step,[status(thm)],[t1585,t83]) ).
cnf(t1587,plain,
X1 = meet(X1,X1),
inference(step,[status(thm)],[t1586,t83]) ).
cnf(t133,plain,
meet(X1,X1) = X1,
inference(orient,[status(thm)],[t1587]) ).
cnf(t1589,plain,
join(X1,meet(X2,join(X1,X1))) = X1,
inference(step,[status(thm)],[t20,t133]) ).
cnf(t140,plain,
join(X1,meet(X2,join(X1,X1))) = X1,
inference(rw,[status(thm)],[t1589]) ).
cnf(t28,plain,
X1 = join(join(meet(X1,X2),X1),X1),
inference(cp,[status(thm)],[t26,t7]) ).
cnf(t40,plain,
join(join(meet(X1,X2),X1),X1) = X1,
inference(orient,[status(thm)],[t28]) ).
cnf(t135,plain,
X1 = join(join(X1,X1),X1),
inference(cp,[status(thm)],[t40,t133]) ).
cnf(t148,plain,
join(join(X1,X1),X1) = X1,
inference(orient,[status(thm)],[t135]) ).
cnf(t151,plain,
X1 = join(meet(join(X1,X1),X1),meet(X1,X1)),
inference(cp,[status(thm)],[t8,t148]) ).
cnf(t134,plain,
X1 = meet(join(X1,X1),X1),
inference(cp,[status(thm)],[t7,t133]) ).
cnf(t143,plain,
meet(join(X1,X1),X1) = X1,
inference(orient,[status(thm)],[t134]) ).
cnf(t1593,plain,
X1 = join(X1,meet(X1,X1)),
inference(step,[status(thm)],[t151,t143]) ).
cnf(t1594,plain,
X1 = join(X1,X1),
inference(step,[status(thm)],[t1593,t133]) ).
cnf(t152,plain,
join(X1,X1) = X1,
inference(orient,[status(thm)],[t1594]) ).
cnf(t1595,plain,
join(X1,meet(X2,X1)) = X1,
inference(step,[status(thm)],[t140,t152]) ).
cnf(t158,plain,
join(X1,meet(X2,X1)) = X1,
inference(orient,[status(thm)],[t1595]) ).
cnf(t162,plain,
X1 = join(meet(X1,meet(X2,X1)),meet(X1,X1)),
inference(cp,[status(thm)],[t13,t158]) ).
cnf(t1596,plain,
X1 = join(meet(X1,meet(X2,X1)),X1),
inference(step,[status(thm)],[t162,t133]) ).
cnf(t164,plain,
join(meet(X1,meet(X2,X1)),X1) = X1,
inference(orient,[status(thm)],[t1596]) ).
cnf(t166,plain,
meet(X1,meet(X2,X1)) = join(meet(meet(X1,meet(X2,X1)),X1),meet(meet(X1,meet(X2,X1)),X1)),
inference(cp,[status(thm)],[t13,t164]) ).
cnf(t1597,plain,
meet(X1,meet(X2,X1)) = meet(meet(X1,meet(X2,X1)),X1),
inference(step,[status(thm)],[t166,t152]) ).
cnf(t168,plain,
meet(meet(X1,meet(X2,X1)),X1) = meet(X1,meet(X2,X1)),
inference(orient,[status(thm)],[t1597]) ).
cnf(t161,plain,
meet(X1,X2) = meet(meet(meet(X1,X2),X2),meet(X1,X2)),
inference(cp,[status(thm)],[t83,t158]) ).
cnf(t190,plain,
meet(meet(meet(X1,X2),X2),meet(X1,X2)) = meet(X1,X2),
inference(orient,[status(thm)],[t161]) ).
cnf(t193,plain,
meet(join(X1,X2),X1) = meet(X1,meet(join(X1,X2),X1)),
inference(cp,[status(thm)],[t190,t46]) ).
cnf(t198,plain,
meet(X1,meet(join(X1,X2),X1)) = meet(join(X1,X2),X1),
inference(orient,[status(thm)],[t193]) ).
cnf(t205,plain,
meet(X1,meet(join(X1,X2),X1)) = meet(meet(join(X1,X2),X1),X1),
inference(cp,[status(thm)],[t168,t198]) ).
cnf(t1598,plain,
meet(join(X1,X2),X1) = meet(meet(join(X1,X2),X1),X1),
inference(step,[status(thm)],[t205,t198]) ).
cnf(t1599,plain,
meet(join(X1,X2),X1) = X1,
inference(step,[status(thm)],[t1598,t46]) ).
cnf(t211,plain,
meet(join(X1,X2),X1) = X1,
inference(orient,[status(thm)],[t1599]) ).
cnf(t216,plain,
meet(X1,X2) = meet(X2,meet(X1,X2)),
inference(cp,[status(thm)],[t211,t8]) ).
cnf(t222,plain,
meet(X1,meet(X2,X1)) = meet(X2,X1),
inference(orient,[status(thm)],[t216]) ).
cnf(t27,plain,
meet(join(X1,X2),join(X3,X1)) = join(join(X1,meet(Y3,meet(join(X1,X2),join(X3,X1)))),meet(join(X1,X2),join(X3,X1))),
inference(cp,[status(thm)],[t26,t7]) ).
cnf(t317,plain,
join(join(X1,meet(X2,meet(join(X1,X3),join(Y3,X1)))),meet(join(X1,X3),join(Y3,X1))) = meet(join(X1,X3),join(Y3,X1)),
inference(orient,[status(thm)],[t27]) ).
cnf(t215,plain,
join(meet(X1,X2),X1) = meet(X1,join(meet(X1,X2),X1)),
inference(cp,[status(thm)],[t211,t40]) ).
cnf(t237,plain,
meet(X1,join(meet(X1,X2),X1)) = join(meet(X1,X2),X1),
inference(orient,[status(thm)],[t215]) ).
cnf(t241,plain,
X1 = meet(join(meet(X1,X2),X1),X1),
inference(cp,[status(thm)],[t83,t237]) ).
cnf(t246,plain,
meet(join(meet(X1,X2),X1),X1) = X1,
inference(orient,[status(thm)],[t241]) ).
cnf(t254,plain,
join(meet(X1,X2),X1) = join(X1,meet(join(meet(X1,X2),X1),join(join(meet(X1,X2),X1),X1))),
inference(cp,[status(thm)],[t13,t246]) ).
cnf(t1607,plain,
join(meet(X1,X2),X1) = join(X1,meet(join(meet(X1,X2),X1),X1)),
inference(step,[status(thm)],[t254,t40]) ).
cnf(t1608,plain,
join(meet(X1,X2),X1) = join(X1,X1),
inference(step,[status(thm)],[t1607,t246]) ).
cnf(t1609,plain,
join(meet(X1,X2),X1) = X1,
inference(step,[status(thm)],[t1608,t152]) ).
cnf(t255,plain,
join(meet(X1,X2),X1) = X1,
inference(orient,[status(thm)],[t1609]) ).
cnf(t256,plain,
join(X1,X2) = join(X1,join(X1,X2)),
inference(cp,[status(thm)],[t255,t211]) ).
cnf(t261,plain,
join(X1,join(X1,X2)) = join(X1,X2),
inference(orient,[status(thm)],[t256]) ).
cnf(t262,plain,
X1 = join(meet(X1,join(X1,X2)),meet(X1,join(X1,X2))),
inference(cp,[status(thm)],[t13,t261]) ).
cnf(t1610,plain,
X1 = meet(X1,join(X1,X2)),
inference(step,[status(thm)],[t262,t152]) ).
cnf(t263,plain,
meet(X1,join(X1,X2)) = X1,
inference(orient,[status(thm)],[t1610]) ).
cnf(t265,plain,
meet(X1,X2) = meet(meet(X1,X2),X1),
inference(cp,[status(thm)],[t263,t255]) ).
cnf(t268,plain,
meet(meet(X1,X2),X1) = meet(X1,X2),
inference(orient,[status(thm)],[t265]) ).
cnf(t269,plain,
meet(meet(join(X1,X2),join(X3,X1)),X1) = meet(X1,meet(join(X1,X2),join(X3,X1))),
inference(cp,[status(thm)],[t268,t7]) ).
cnf(t1613,plain,
X1 = meet(X1,meet(join(X1,X2),join(X3,X1))),
inference(step,[status(thm)],[t269,t7]) ).
cnf(t303,plain,
meet(X1,meet(join(X1,X2),join(X3,X1))) = X1,
inference(orient,[status(thm)],[t1613]) ).
cnf(t225,plain,
X1 = join(meet(X2,X1),meet(X1,join(X1,meet(X2,X1)))),
inference(cp,[status(thm)],[t13,t222]) ).
cnf(t1605,plain,
X1 = join(meet(X2,X1),meet(X1,X1)),
inference(step,[status(thm)],[t225,t158]) ).
cnf(t1606,plain,
X1 = join(meet(X2,X1),X1),
inference(step,[status(thm)],[t1605,t133]) ).
cnf(t230,plain,
join(meet(X1,X2),X2) = X2,
inference(orient,[status(thm)],[t1606]) ).
cnf(t1611,plain,
meet(X1,join(X2,X1)) = X1,
inference(step,[status(thm)],[t83,t268]) ).
cnf(t272,plain,
meet(X1,join(X2,X1)) = X1,
inference(rw,[status(thm)],[t1611]) ).
cnf(t278,plain,
meet(X1,join(X2,X1)) = X1,
inference(orient,[status(thm)],[t272]) ).
cnf(t280,plain,
join(X1,X2) = join(X2,join(X1,X2)),
inference(cp,[status(thm)],[t230,t278]) ).
cnf(t291,plain,
join(X1,join(X2,X1)) = join(X2,X1),
inference(orient,[status(thm)],[t280]) ).
cnf(t304,plain,
X1 = meet(X1,meet(join(X2,X1),join(X3,X1))),
inference(cp,[status(thm)],[t303,t291]) ).
cnf(t458,plain,
meet(X1,meet(join(X2,X1),join(X3,X1))) = X1,
inference(orient,[status(thm)],[t304]) ).
cnf(t266,plain,
join(X1,X2) = join(join(X1,X2),X1),
inference(cp,[status(thm)],[t158,t263]) ).
cnf(t287,plain,
join(join(X1,X2),X1) = join(X1,X2),
inference(orient,[status(thm)],[t266]) ).
cnf(t467,plain,
X1 = meet(X1,meet(join(X2,X1),join(X1,X3))),
inference(cp,[status(thm)],[t458,t287]) ).
cnf(t571,plain,
meet(X1,meet(join(X2,X1),join(X1,X3))) = X1,
inference(orient,[status(thm)],[t467]) ).
cnf(t595,plain,
meet(join(X1,X2),join(X2,X1)) = join(join(X1,X2),meet(join(X1,X2),join(X2,X1))),
inference(cp,[status(thm)],[t317,t571]) ).
cnf(t270,plain,
X1 = join(X1,meet(X1,X2)),
inference(cp,[status(thm)],[t158,t268]) ).
cnf(t273,plain,
join(X1,meet(X1,X2)) = X1,
inference(orient,[status(thm)],[t270]) ).
cnf(t1618,plain,
meet(join(X1,X2),join(X2,X1)) = join(X1,X2),
inference(step,[status(thm)],[t595,t273]) ).
cnf(t596,plain,
meet(join(X1,X2),join(X2,X1)) = join(X1,X2),
inference(orient,[status(thm)],[t1618]) ).
cnf(t600,plain,
meet(join(X1,X2),join(X2,X1)) = meet(join(X2,X1),join(X1,X2)),
inference(cp,[status(thm)],[t222,t596]) ).
cnf(t1619,plain,
join(X1,X2) = meet(join(X2,X1),join(X1,X2)),
inference(step,[status(thm)],[t600,t596]) ).
cnf(t1620,plain,
join(X1,X2) = join(X2,X1),
inference(step,[status(thm)],[t1619,t596]) ).
cnf(t611,plain,
join(X1,X2) = join(X2,X1),
inference(orient,[status(thm)],[t1620]) ).
cnf(t292,plain,
X1 = meet(meet(join(X2,X1),join(X3,X1)),X1),
inference(cp,[status(thm)],[t7,t291]) ).
cnf(t408,plain,
meet(meet(join(X1,X2),join(X3,X2)),X2) = X2,
inference(orient,[status(thm)],[t292]) ).
cnf(t410,plain,
meet(X1,X2) = meet(meet(X2,join(X3,meet(X1,X2))),meet(X1,X2)),
inference(cp,[status(thm)],[t408,t158]) ).
cnf(t1467,plain,
meet(meet(X1,join(X2,meet(X3,X1))),meet(X3,X1)) = meet(X3,X1),
inference(orient,[status(thm)],[t410]) ).
cnf(t1468,plain,
meet(X1,X2) = meet(meet(X2,X1),meet(X1,X2)),
inference(cp,[status(thm)],[t1467,t273]) ).
cnf(t1518,plain,
meet(meet(X1,X2),meet(X2,X1)) = meet(X2,X1),
inference(orient,[status(thm)],[t1468]) ).
cnf(t1521,plain,
meet(meet(X1,X2),meet(X2,X1)) = meet(meet(meet(X2,X1),meet(X1,X2)),meet(X2,X1)),
inference(cp,[status(thm)],[t1518,t1518]) ).
cnf(t1627,plain,
meet(X2,X1) = meet(meet(meet(X2,X1),meet(X1,X2)),meet(X2,X1)),
inference(step,[status(thm)],[t1521,t1518]) ).
cnf(t1628,plain,
meet(X2,X1) = meet(meet(X2,X1),meet(X1,X2)),
inference(step,[status(thm)],[t1627,t268]) ).
cnf(t1629,plain,
meet(X2,X1) = meet(X1,X2),
inference(step,[status(thm)],[t1628,t1518]) ).
cnf(t1546,plain,
meet(X1,X2) = meet(X2,X1),
inference(orient,[status(thm)],[t1629]) ).
cnf(t0,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t33,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t0]) ).
cnf(f5,negated_conjecture,
( join(b,a) != join(a,b)
| join(a,a) != a
| meet(b,a) != meet(a,b)
| meet(a,a) != a ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_normal_axioms) ).
fof(f5_nnf,plain,
( join(b,a) != join(a,b)
| join(a,a) != a
| meet(b,a) != meet(a,b)
| meet(a,a) != a ),
inference(nnf_transformation,[status(thm)],[f5]) ).
fof(f5_sk,plain,
( join(b,a) != join(a,b)
| join(a,a) != a
| meet(b,a) != meet(a,b)
| meet(a,a) != a ),
inference(skolemisation,[status(esa)],[f5_nnf]) ).
cnf(c5,plain,
( join(b,a) != join(a,b)
| join(a,a) != a
| meet(b,a) != meet(a,b)
| meet(a,a) != a ),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c5]) ).
cnf(g0_0,plain,
true != ifeq(meet(a,a),a,ifeq(meet(b,a),meet(a,b),ifeq(join(a,a),a,ifeq(join(b,a),join(a,b),false,true),true),true),true),
inference(rw,[status(thm)],[goal_0]) ).
cnf(g0_1,plain,
true != ifeq(meet(a,a),a,ifeq(meet(b,a),meet(a,b),ifeq(join(a,a),a,ifeq(join(b,a),join(b,a),false,true),true),true),true),
inference(rw,[status(thm)],[g0_0,t611]) ).
cnf(g0_2,plain,
true != ifeq(meet(a,a),a,ifeq(meet(b,a),meet(a,b),ifeq(join(a,a),a,ifeq(join(a,b),join(b,a),false,true),true),true),true),
inference(rw,[status(thm)],[g0_1,t611]) ).
cnf(g0_3,plain,
true != ifeq(meet(a,a),a,ifeq(meet(b,a),meet(b,a),ifeq(join(a,a),a,ifeq(join(a,b),join(b,a),false,true),true),true),true),
inference(rw,[status(thm)],[g0_2,t1546]) ).
cnf(g0_4,plain,
true != ifeq(meet(a,a),a,ifeq(join(a,a),a,ifeq(join(a,b),join(b,a),false,true),true),true),
inference(rw,[status(thm)],[g0_3,t33]) ).
cnf(g0_5,plain,
true != ifeq(meet(a,a),a,ifeq(join(a,a),a,ifeq(join(a,b),join(a,b),false,true),true),true),
inference(rw,[status(thm)],[g0_4,t611]) ).
cnf(g0_6,plain,
true != ifeq(meet(a,a),a,ifeq(join(a,a),a,ifeq(join(b,a),join(a,b),false,true),true),true),
inference(rw,[status(thm)],[g0_5,t611]) ).
cnf(g0_7,plain,
true != ifeq(meet(a,a),a,ifeq(a,a,ifeq(join(b,a),join(a,b),false,true),true),true),
inference(rw,[status(thm)],[g0_6,t152]) ).
cnf(g0_8,plain,
true != ifeq(meet(a,a),a,ifeq(a,a,ifeq(join(b,a),join(b,a),false,true),true),true),
inference(rw,[status(thm)],[g0_7,t611]) ).
cnf(g0_9,plain,
true != ifeq(meet(a,a),a,ifeq(a,a,false,true),true),
inference(rw,[status(thm)],[g0_8,t33]) ).
cnf(g0_10,plain,
true != ifeq(meet(a,a),a,false,true),
inference(rw,[status(thm)],[g0_9,t33]) ).
cnf(g0_11,plain,
true != ifeq(a,a,false,true),
inference(rw,[status(thm)],[g0_10,t133]) ).
cnf(g0_12,plain,
true != false,
inference(rw,[status(thm)],[g0_11,t33]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_12]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LAT029-1 : TPTP v9.3.1. Released v2.2.0.
% 0.00/0.03 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.08/0.58 % Computer : n019.cluster.edu
% 0.08/0.58 % Model : x86_64 x86_64
% 0.08/0.58 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.58 % Memory : 8046.5625MB
% 0.08/0.58 % OS : Linux 6.8.0-71-generic
% 0.08/0.59 % CPULimit : 300
% 0.08/0.59 % WCLimit : 300
% 0.08/0.59 % DateTime : Wed Sep 23 20:03:53 UTC 2026
% 0.08/0.59 % CPUTime :
% 0.08/0.59 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 5.42/1.60 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 5.42/1.60 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------