%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : LAT006-1 : TPTP v9.3.1. Released v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n009.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 : Thu Sep 24 01:03:07 PM UTC 2026
% Result : Unsatisfiable 6.04s 1.46s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT006-1 : TPTP v9.3.1. Released v2.2.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.61 % Computer : n009.cluster.edu
% 0.10/0.61 % Model : x86_64 x86_64
% 0.10/0.61 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.61 % Memory : 8046.5625MB
% 0.10/0.61 % OS : Linux 6.8.0-71-generic
% 0.10/0.61 % CPULimit : 300
% 0.10/0.61 % WCLimit : 300
% 0.10/0.61 % DateTime : Sun Sep 20 23:04:43 UTC 2026
% 0.10/0.61 % CPUTime :
% 0.10/0.62 % Drodi V4.1.1
% 6.04/1.46 % Refutation found
% 6.04/1.46 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 6.04/1.46 % SZS output start CNFRefutation for theBenchmark
% 6.04/1.46 fof(f1,axiom,(
% 6.04/1.46 (![X,Y]: (meet(X,join(X,Y)) = X ))),
% 6.04/1.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.04/1.46 fof(f2,axiom,(
% 6.04/1.46 (![X,Y,Z]: (meet(X,join(Y,Z)) = join(meet(Z,X),meet(Y,X)) ))),
% 6.04/1.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.04/1.46 fof(f3,negated_conjecture,(
% 6.04/1.46 meet(meet(a,b),c) != meet(a,meet(b,c)) ),
% 6.04/1.46 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 6.04/1.46 fof(f4,plain,(
% 6.04/1.46 ![X0,X1]: (meet(X0,join(X0,X1))=X0)),
% 6.04/1.46 inference(cnf_transformation,[status(thm)],[f1])).
% 6.04/1.46 fof(f5,plain,(
% 6.04/1.46 ![X0,X1,X2]: (meet(X0,join(X1,X2))=join(meet(X2,X0),meet(X1,X0)))),
% 6.04/1.46 inference(cnf_transformation,[status(thm)],[f2])).
% 6.04/1.46 fof(f6,plain,(
% 6.04/1.46 ~meet(meet(a,b),c)=meet(a,meet(b,c))),
% 6.04/1.46 inference(cnf_transformation,[status(thm)],[f3])).
% 6.04/1.46 fof(f12,plain,(
% 6.04/1.46 ![X0,X1,X2]: (meet(join(X0,X1),join(X2,X0))=join(X0,meet(X2,join(X0,X1))))),
% 6.04/1.46 inference(paramodulation,[status(thm)],[f4,f5])).
% 6.04/1.46 fof(f13,plain,(
% 6.04/1.46 ![X0,X1,X2]: (meet(join(X0,X1),join(X0,X2))=join(meet(X2,join(X0,X1)),X0))),
% 6.04/1.46 inference(paramodulation,[status(thm)],[f4,f5])).
% 6.04/1.46 fof(f14,plain,(
% 6.04/1.46 ![X0,X1,X2]: (meet(meet(X0,X1),meet(X1,join(X2,X0)))=meet(X0,X1))),
% 6.04/1.46 inference(paramodulation,[status(thm)],[f5,f4])).
% 6.04/1.46 fof(f17,plain,(
% 6.04/1.46 ![X0,X1]: (meet(meet(X0,X1),X1)=meet(X0,X1))),
% 6.04/1.46 inference(paramodulation,[status(thm)],[f4,f14])).
% 6.04/1.46 fof(f19,plain,(
% 6.04/1.46 ![X0,X1,X2,X3]: (meet(meet(X0,join(X1,X2)),join(meet(X2,X0),X3))=join(meet(X3,meet(X0,join(X1,X2))),meet(X2,X0)))),
% 6.04/1.46 inference(paramodulation,[status(thm)],[f14,f5])).
% 6.04/1.46 fof(f30,plain,(
% 6.04/1.46 ![X0,X1,X2]: (meet(X0,join(meet(X1,X0),X2))=join(meet(X2,X0),meet(X1,X0)))),
% 6.04/1.46 inference(paramodulation,[status(thm)],[f17,f5])).
% 6.04/1.46 fof(f31,plain,(
% 6.04/1.46 ![X0,X1,X2]: (meet(X0,join(X1,meet(X2,X0)))=join(meet(X2,X0),meet(X1,X0)))),
% 6.04/1.46 inference(paramodulation,[status(thm)],[f17,f5])).
% 6.04/1.46 fof(f33,plain,(
% 6.04/1.46 ![X0,X1,X2]: (meet(X0,join(meet(X1,X0),X2))=meet(X0,join(X1,X2)))),
% 6.04/1.46 inference(forward_demodulation,[status(thm)],[f5,f30])).
% 6.04/1.46 fof(f35,plain,(
% 6.04/1.46 ![X0,X1,X2]: (meet(X0,join(X1,meet(X2,X0)))=meet(X0,join(X1,X2)))),
% 6.04/1.46 inference(forward_demodulation,[status(thm)],[f5,f31])).
% 6.04/1.46 fof(f36,plain,(
% 6.04/1.46 ![X0,X1,X2]: (meet(X0,meet(X0,join(X1,X2)))=meet(X0,join(X2,meet(X1,X0))))),
% 6.04/1.46 inference(paramodulation,[status(thm)],[f5,f33])).
% 6.04/1.46 fof(f46,plain,(
% 6.04/1.46 ![X0,X1,X2]: (meet(X0,meet(X0,join(X1,X2)))=meet(X0,join(X2,X1)))),
% 6.04/1.46 inference(forward_demodulation,[status(thm)],[f35,f36])).
% 6.04/1.46 fof(f50,plain,(
% 6.04/1.46 ![X0,X1]: (join(X0,X1)=join(X0,meet(join(X0,X1),join(X0,X1))))),
% 6.04/1.46 inference(paramodulation,[status(thm)],[f4,f12])).
% 6.04/1.46 fof(f52,plain,(
% 6.04/1.46 ![X0,X1,X2,X3]: (meet(join(meet(X0,X1),X2),meet(X1,join(X0,X3)))=join(meet(X0,X1),meet(meet(X3,X1),join(meet(X0,X1),X2))))),
% 6.04/1.46 inference(paramodulation,[status(thm)],[f5,f12])).
% 6.04/1.46 fof(f62,plain,(
% 6.04/1.46 ![X0,X1]: (join(X0,X1)=join(X0,join(meet(X1,join(X0,X1)),X0)))),
% 6.04/1.46 inference(forward_demodulation,[status(thm)],[f13,f50])).
% 6.04/1.46 fof(f74,plain,(
% 6.04/1.46 ![X0,X1]: (meet(X0,X0)=meet(X0,join(X1,X0)))),
% 6.04/1.46 inference(paramodulation,[status(thm)],[f4,f46])).
% 6.04/1.46 fof(f84,plain,(
% 6.04/1.46 ![X0,X1]: (join(X0,X1)=join(X0,join(meet(X1,X1),X0)))),
% 6.04/1.46 inference(backward_demodulation,[status(thm)],[f74,f62])).
% 6.04/1.46 fof(f89,plain,(
% 6.04/1.46 ![X0]: (meet(X0,X0)=X0)),
% 6.04/1.46 inference(paramodulation,[status(thm)],[f4,f74])).
% 6.04/1.46 fof(f90,plain,(
% 6.04/1.46 ![X0,X1,X2]: (meet(meet(X0,X1),meet(X0,X1))=meet(meet(X0,X1),meet(X1,join(X0,X2))))),
% 6.04/1.46 inference(paramodulation,[status(thm)],[f5,f74])).
% 6.04/1.46 fof(f91,plain,(
% 6.04/1.46 ![X0,X1]: (meet(X0,X0)=meet(X0,join(X1,X0)))),
% 6.04/1.46 inference(paramodulation,[status(thm)],[f74,f33])).
% 6.04/1.46 fof(f102,plain,(
% 6.04/1.46 ![X0,X1]: (join(X0,X1)=join(X0,join(X1,X0)))),
% 6.04/1.46 inference(backward_demodulation,[status(thm)],[f89,f84])).
% 6.04/1.46 fof(f103,plain,(
% 6.04/1.46 ![X0,X1,X2]: (meet(X0,X1)=meet(meet(X0,X1),meet(X1,join(X0,X2))))),
% 6.04/1.46 inference(forward_demodulation,[status(thm)],[f89,f90])).
% 6.04/1.46 fof(f104,plain,(
% 6.04/1.46 ![X0,X1]: (X0=meet(X0,join(X1,X0)))),
% 6.04/1.46 inference(forward_demodulation,[status(thm)],[f89,f91])).
% 6.04/1.46 fof(f120,plain,(
% 6.04/1.46 ![X0,X1]: (meet(X0,join(X0,X1))=join(meet(X1,X0),X0))),
% 6.04/1.46 inference(paramodulation,[status(thm)],[f89,f5])).
% 6.04/1.46 fof(f121,plain,(
% 6.04/1.46 ![X0,X1]: (meet(X0,join(X1,X0))=join(X0,meet(X1,X0)))),
% 6.04/1.46 inference(paramodulation,[status(thm)],[f89,f5])).
% 6.04/1.46 fof(f126,plain,(
% 6.04/1.46 ![X0,X1]: (X0=join(meet(X1,X0),X0))),
% 6.04/1.46 inference(forward_demodulation,[status(thm)],[f4,f120])).
% 6.04/1.46 fof(f127,plain,(
% 6.04/1.46 ![X0,X1]: (X0=join(X0,meet(X1,X0)))),
% 6.04/1.46 inference(forward_demodulation,[status(thm)],[f104,f121])).
% 6.04/1.46 fof(f148,plain,(
% 6.04/1.46 ![X0,X1]: (join(X0,X1)=join(X1,join(X0,X1)))),
% 6.04/1.46 inference(paramodulation,[status(thm)],[f104,f126])).
% 6.04/1.46 fof(f149,plain,(
% 6.04/1.46 ![X0,X1]: (join(X0,X1)=join(X0,join(X0,X1)))),
% 6.04/1.46 inference(paramodulation,[status(thm)],[f4,f126])).
% 6.04/1.46 fof(f150,plain,(
% 6.04/1.46 ![X0]: (X0=join(X0,X0))),
% 6.04/1.46 inference(paramodulation,[status(thm)],[f89,f126])).
% 6.04/1.46 fof(f153,plain,(
% 6.04/1.46 ![X0,X1,X2]: (meet(X0,meet(X0,X1))=meet(X0,join(X1,meet(X2,X1))))),
% 6.04/1.46 inference(paramodulation,[status(thm)],[f126,f46])).
% 6.04/1.46 fof(f161,plain,(
% 6.04/1.46 ![X0,X1]: (meet(X0,meet(X0,X1))=meet(X0,X1))),
% 6.04/1.46 inference(forward_demodulation,[status(thm)],[f127,f153])).
% 6.04/1.46 fof(f166,plain,(
% 6.04/1.46 ![X0,X1]: (meet(X0,meet(X1,X0))=meet(X0,join(X1,meet(X1,X0))))),
% 6.04/1.46 inference(paramodulation,[status(thm)],[f150,f33])).
% 6.04/1.46 fof(f168,plain,(
% 6.04/1.46 ![X0,X1]: (meet(join(X0,X1),X0)=join(X0,meet(X0,join(X0,X1))))),
% 6.04/1.46 inference(paramodulation,[status(thm)],[f150,f12])).
% 6.04/1.46 fof(f174,plain,(
% 6.04/1.46 ![X0,X1]: (meet(X0,meet(X1,X0))=meet(X0,join(X1,X1)))),
% 6.04/1.46 inference(forward_demodulation,[status(thm)],[f35,f166])).
% 6.04/1.46 fof(f175,plain,(
% 6.04/1.46 ![X0,X1]: (meet(X0,meet(X1,X0))=meet(X0,X1))),
% 6.04/1.46 inference(forward_demodulation,[status(thm)],[f150,f174])).
% 6.04/1.46 fof(f176,plain,(
% 6.04/1.46 ![X0,X1]: (meet(join(X0,X1),X0)=join(X0,X0))),
% 6.04/1.46 inference(forward_demodulation,[status(thm)],[f4,f168])).
% 6.04/1.46 fof(f178,plain,(
% 6.04/1.46 ![X0,X1]: (meet(join(X0,X1),X0)=X0)),
% 6.04/1.46 inference(forward_demodulation,[status(thm)],[f150,f176])).
% 6.04/1.46 fof(f182,plain,(
% 6.04/1.46 ![X0,X1]: (meet(X0,meet(X1,X0))=meet(X1,X0))),
% 6.04/1.46 inference(paramodulation,[status(thm)],[f126,f178])).
% 6.04/1.46 fof(f306,plain,(
% 6.04/1.46 ![X0,X1,X2]: (meet(meet(X0,X1),join(meet(X0,X1),X2))=meet(meet(X0,X1),join(X0,X2)))),
% 6.04/1.46 inference(paramodulation,[status(thm)],[f161,f33])).
% 6.04/1.46 fof(f325,plain,(
% 6.04/1.46 ![X0,X1,X2]: (meet(X0,X1)=meet(meet(X0,X1),join(X0,X2)))),
% 6.04/1.46 inference(forward_demodulation,[status(thm)],[f4,f306])).
% 6.04/1.46 fof(f513,plain,(
% 6.04/1.46 ![X0,X1]: (join(X0,join(X1,X0))=join(X0,join(X0,X1)))),
% 6.04/1.46 inference(paramodulation,[status(thm)],[f102,f149])).
% 6.04/1.46 fof(f530,plain,(
% 6.04/1.46 ![X0,X1]: (join(X0,X1)=join(X1,join(X1,X0)))),
% 6.04/1.46 inference(forward_demodulation,[status(thm)],[f148,f513])).
% 6.04/1.46 fof(f614,plain,(
% 6.04/1.46 ![X0,X1]: (meet(meet(X0,X1),meet(X0,X1))=meet(meet(X0,X1),X0))),
% 6.04/1.46 inference(paramodulation,[status(thm)],[f161,f175])).
% 6.04/1.46 fof(f636,plain,(
% 6.04/1.46 ![X0,X1]: (meet(X0,X1)=meet(meet(X0,X1),X0))),
% 6.04/1.46 inference(forward_demodulation,[status(thm)],[f89,f614])).
% 6.04/1.46 fof(f712,plain,(
% 6.04/1.46 ![X0,X1,X2]: (meet(meet(X0,X1),join(meet(X0,X1),X2))=meet(meet(X0,X1),join(X1,X2)))),
% 6.04/1.46 inference(paramodulation,[status(thm)],[f182,f33])).
% 6.04/1.46 fof(f714,plain,(
% 6.04/1.46 ![X0,X1,X2]: (meet(meet(X0,X1),meet(meet(X0,X1),join(X2,X1)))=meet(X1,meet(X0,X1)))),
% 6.04/1.46 inference(paramodulation,[status(thm)],[f182,f14])).
% 6.04/1.46 fof(f744,plain,(
% 6.04/1.46 ![X0,X1,X2]: (meet(X0,X1)=meet(meet(X0,X1),join(X1,X2)))),
% 6.04/1.46 inference(forward_demodulation,[status(thm)],[f4,f712])).
% 6.04/1.46 fof(f746,plain,(
% 6.04/1.46 ![X0,X1,X2]: (meet(meet(X0,X1),join(X2,X1))=meet(X1,meet(X0,X1)))),
% 6.04/1.46 inference(forward_demodulation,[status(thm)],[f161,f714])).
% 6.04/1.46 fof(f749,plain,(
% 6.04/1.46 ![X0,X1,X2]: (meet(meet(X0,X1),join(X2,X1))=meet(X0,X1))),
% 6.04/1.46 inference(forward_demodulation,[status(thm)],[f182,f746])).
% 6.04/1.46 fof(f761,plain,(
% 6.04/1.46 ![X0,X1]: (meet(X0,meet(X1,X0))=meet(meet(X0,X1),X0))),
% 6.04/1.46 inference(paramodulation,[status(thm)],[f175,f636])).
% 6.04/1.46 fof(f776,plain,(
% 6.04/1.46 ![X0,X1]: (X0=join(X0,meet(X0,X1)))),
% 6.04/1.46 inference(paramodulation,[status(thm)],[f636,f127])).
% 6.04/1.46 fof(f777,plain,(
% 6.04/1.46 ![X0,X1]: (X0=join(meet(X0,X1),X0))),
% 6.04/1.46 inference(paramodulation,[status(thm)],[f636,f126])).
% 6.04/1.46 fof(f782,plain,(
% 6.04/1.46 ![X0,X1,X2]: (meet(X0,join(X1,meet(X0,X2)))=join(meet(X0,X2),meet(X1,X0)))),
% 6.04/1.46 inference(paramodulation,[status(thm)],[f636,f5])).
% 6.04/1.46 fof(f792,plain,(
% 6.04/1.46 ![X0,X1]: (meet(X0,X1)=meet(meet(X1,X0),X1))),
% 6.04/1.46 inference(forward_demodulation,[status(thm)],[f182,f761])).
% 6.04/1.46 fof(f1000,plain,(
% 6.04/1.46 ![X0,X1]: (meet(X0,meet(X1,X0))=meet(X0,meet(X0,X1)))),
% 6.04/1.46 inference(paramodulation,[status(thm)],[f792,f175])).
% 6.04/1.46 fof(f1009,plain,(
% 6.04/1.46 ![X0,X1,X2]: (meet(X0,join(X1,meet(X0,X2)))=join(meet(X2,X0),meet(X1,X0)))),
% 6.04/1.46 inference(paramodulation,[status(thm)],[f792,f5])).
% 6.04/1.46 fof(f1025,plain,(
% 6.04/1.46 ![X0,X1]: (meet(X0,X1)=meet(X1,meet(X1,X0)))),
% 6.04/1.46 inference(forward_demodulation,[status(thm)],[f182,f1000])).
% 6.04/1.46 fof(f1035,plain,(
% 6.04/1.46 ![X0,X1,X2]: (meet(X0,join(X1,X2))=join(meet(X0,X2),meet(X1,X0)))),
% 6.04/1.46 inference(backward_demodulation,[status(thm)],[f1036,f782])).
% 6.04/1.46 fof(f1036,plain,(
% 6.04/1.46 ![X0,X1,X2]: (meet(X0,join(X1,meet(X0,X2)))=meet(X0,join(X1,X2)))),
% 6.04/1.46 inference(forward_demodulation,[status(thm)],[f5,f1009])).
% 6.04/1.46 fof(f1263,plain,(
% 6.04/1.46 ![X0,X1,X2]: (meet(X0,meet(X1,X0))=meet(meet(X0,X1),join(X0,X2)))),
% 6.04/1.46 inference(paramodulation,[status(thm)],[f175,f325])).
% 6.04/1.46 fof(f1318,plain,(
% 6.04/1.46 ![X0,X1,X2]: (meet(X0,X1)=meet(meet(X1,X0),join(X1,X2)))),
% 6.04/1.46 inference(forward_demodulation,[status(thm)],[f182,f1263])).
% 6.04/1.46 fof(f1598,plain,(
% 6.04/1.46 ![X0,X1,X2]: (meet(X0,meet(X1,X0))=meet(meet(X0,X1),join(meet(X1,X0),X2)))),
% 6.04/1.46 inference(paramodulation,[status(thm)],[f175,f744])).
% 6.04/1.46 fof(f1663,plain,(
% 6.04/1.46 ![X0,X1,X2]: (meet(X0,X1)=meet(meet(X1,X0),join(meet(X0,X1),X2)))),
% 6.04/1.46 inference(forward_demodulation,[status(thm)],[f182,f1598])).
% 6.04/1.46 fof(f1750,plain,(
% 6.04/1.46 ![X0,X1,X2,X3]: (meet(meet(meet(X0,X1),join(X2,X1)),join(meet(X1,X0),X3))=join(meet(X3,meet(meet(X0,X1),join(X2,X1))),meet(X1,meet(X0,X1))))),
% 6.04/1.46 inference(paramodulation,[status(thm)],[f175,f19])).
% 6.04/1.46 fof(f1935,plain,(
% 6.04/1.46 ![X0,X1,X2,X3]: (meet(meet(X0,X1),join(meet(X1,X0),X2))=join(meet(X2,meet(meet(X0,X1),join(X3,X1))),meet(X1,meet(X0,X1))))),
% 6.04/1.46 inference(forward_demodulation,[status(thm)],[f749,f1750])).
% 6.04/1.46 fof(f1936,plain,(
% 6.04/1.46 ![X0,X1,X2,X3]: (meet(X0,X1)=join(meet(X2,meet(meet(X1,X0),join(X3,X0))),meet(X0,meet(X1,X0))))),
% 6.04/1.46 inference(forward_demodulation,[status(thm)],[f1663,f1935])).
% 6.04/1.46 fof(f1937,plain,(
% 6.04/1.46 ![X0,X1,X2]: (meet(X0,X1)=join(meet(X2,meet(X1,X0)),meet(X0,meet(X1,X0))))),
% 6.04/1.46 inference(forward_demodulation,[status(thm)],[f749,f1936])).
% 6.04/1.46 fof(f1938,plain,(
% 6.04/1.46 ![X0,X1,X2]: (meet(X0,X1)=meet(meet(X1,X0),join(X0,X2)))),
% 6.04/1.46 inference(forward_demodulation,[status(thm)],[f5,f1937])).
% 6.04/1.46 fof(f2344,plain,(
% 6.04/1.46 ![X0,X1,X2]: (meet(join(meet(X0,X1),X0),meet(X1,join(X0,X2)))=join(meet(X0,X1),meet(meet(X2,X1),X0)))),
% 6.04/1.46 inference(paramodulation,[status(thm)],[f777,f52])).
% 6.04/1.46 fof(f2533,plain,(
% 6.04/1.46 ![X0,X1,X2]: (meet(X0,meet(X1,join(X0,X2)))=join(meet(X0,X1),meet(meet(X2,X1),X0)))),
% 6.04/1.46 inference(forward_demodulation,[status(thm)],[f777,f2344])).
% 6.04/1.46 fof(f2534,plain,(
% 6.04/1.46 ![X0,X1,X2]: (meet(X0,meet(X1,join(X0,X2)))=meet(X0,join(meet(X2,X1),X1)))),
% 6.04/1.46 inference(forward_demodulation,[status(thm)],[f1035,f2533])).
% 6.04/1.46 fof(f2537,plain,(
% 6.04/1.46 ![X0,X1,X2]: (meet(X0,meet(X1,join(X0,X2)))=meet(X0,X1))),
% 6.04/1.46 inference(forward_demodulation,[status(thm)],[f126,f2534])).
% 6.04/1.46 fof(f3089,plain,(
% 6.04/1.46 ![X0,X1,X2]: (meet(X0,X1)=meet(meet(X1,X0),join(X2,X1)))),
% 6.04/1.46 inference(paramodulation,[status(thm)],[f530,f1318])).
% 6.04/1.46 fof(f3249,plain,(
% 6.04/1.46 ![X0,X1]: (meet(X0,X1)=meet(meet(X1,X0),X0))),
% 6.04/1.46 inference(paramodulation,[status(thm)],[f776,f1938])).
% 6.04/1.46 fof(f3555,plain,(
% 6.04/1.46 ![X0,X1,X2]: (meet(meet(X0,join(X1,X2)),X1)=meet(meet(X1,X0),meet(X0,join(X1,X2))))),
% 6.04/1.46 inference(paramodulation,[status(thm)],[f2537,f3249])).
% 6.04/1.46 fof(f3575,plain,(
% 6.04/1.46 ![X0,X1,X2]: (meet(X0,meet(X0,X1))=meet(X0,meet(X1,join(X0,X2))))),
% 6.04/1.46 inference(paramodulation,[status(thm)],[f2537,f161])).
% 6.04/1.46 fof(f3617,plain,(
% 6.04/1.46 ![X0,X1,X2]: (meet(meet(X0,join(X1,X2)),X1)=meet(X1,X0))),
% 6.04/1.46 inference(forward_demodulation,[status(thm)],[f103,f3555])).
% 6.04/1.46 fof(f3637,plain,(
% 6.04/1.46 ![X0,X1,X2]: (meet(X0,X1)=meet(X1,meet(X0,join(X1,X2))))),
% 6.04/1.46 inference(forward_demodulation,[status(thm)],[f1025,f3575])).
% 6.04/1.46 fof(f4145,plain,(
% 6.04/1.46 ![X0,X1,X2]: (meet(X0,meet(X1,X2))=meet(X0,meet(X2,X1)))),
% 6.04/1.46 inference(paramodulation,[status(thm)],[f3089,f2537])).
% 6.04/1.46 fof(f4536,plain,(
% 6.04/1.46 ![X0,X1,X2]: (meet(meet(X0,X1),meet(X2,X1))=meet(meet(X2,X1),X0))),
% 6.04/1.46 inference(paramodulation,[status(thm)],[f126,f3617])).
% 6.04/1.46 fof(f4708,plain,(
% 6.04/1.46 ![X0,X1,X2]: (meet(X0,meet(X1,X2))=meet(meet(X1,X2),meet(X0,X2)))),
% 6.04/1.51 inference(paramodulation,[status(thm)],[f126,f3637])).
% 6.04/1.51 fof(f4768,plain,(
% 6.04/1.51 ![X0,X1,X2]: (meet(X0,meet(X1,X2))=meet(meet(X0,X2),X1))),
% 6.04/1.51 inference(backward_demodulation,[status(thm)],[f4708,f4536])).
% 6.04/1.51 fof(f4797,plain,(
% 6.04/1.51 ~meet(a,meet(c,b))=meet(a,meet(b,c))),
% 6.04/1.51 inference(backward_demodulation,[status(thm)],[f4768,f6])).
% 6.04/1.51 fof(f5018,plain,(
% 6.04/1.51 $false),
% 6.04/1.51 inference(forward_subsumption_resolution,[status(thm)],[f4797,f4145])).
% 6.04/1.51 % SZS output end CNFRefutation for theBenchmark.p
% 117.98/26.21 % Elapsed time: 25.438554 seconds
% 117.98/26.21 % CPU time: 164.991490 seconds
% 117.98/26.21 % Total memory used: 103.803 GB
% 117.98/26.21 % Net memory used: 103.801 GB
%------------------------------------------------------------------------------