%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : LAT013-1 : TPTP v9.3.1. Released v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/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:08 PM UTC 2026
% Result : Unsatisfiable 64.12s 8.55s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT013-1 : TPTP v9.3.1. Released v2.2.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n009.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Sun Sep 20 23:06:13 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.38 % Drodi V4.1.1
% 64.12/8.55 % Refutation found
% 64.12/8.55 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 64.12/8.55 % SZS output start CNFRefutation for theBenchmark
% 64.12/8.55 fof(f1,axiom,(
% 64.12/8.55 (![X,Y,Z]: (join(X,meet(Y,meet(X,Z))) = X ))),
% 64.12/8.55 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 64.12/8.55 fof(f2,axiom,(
% 64.12/8.55 (![X,Y,Z]: (meet(X,join(Y,join(X,Z))) = X ))),
% 64.12/8.55 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 64.12/8.55 fof(f3,axiom,(
% 64.12/8.55 (![X,Y,Z]: (join(join(meet(X,Y),meet(Y,Z)),Y) = Y ))),
% 64.12/8.55 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 64.12/8.55 fof(f4,axiom,(
% 64.12/8.55 (![X,Y,Z]: (meet(meet(join(X,Y),join(Y,Z)),Y) = Y ))),
% 64.12/8.55 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 64.12/8.55 fof(f5,negated_conjecture,(
% 64.12/8.55 meet(meet(a,b),c) != meet(a,meet(b,c)) ),
% 64.12/8.55 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 64.12/8.55 fof(f6,plain,(
% 64.12/8.55 ![X0,X1,X2]: (join(X0,meet(X1,meet(X0,X2)))=X0)),
% 64.12/8.55 inference(cnf_transformation,[status(thm)],[f1])).
% 64.12/8.55 fof(f7,plain,(
% 64.12/8.55 ![X0,X1,X2]: (meet(X0,join(X1,join(X0,X2)))=X0)),
% 64.12/8.55 inference(cnf_transformation,[status(thm)],[f2])).
% 64.12/8.55 fof(f8,plain,(
% 64.12/8.55 ![X0,X1,X2]: (join(join(meet(X0,X1),meet(X1,X2)),X1)=X1)),
% 64.12/8.55 inference(cnf_transformation,[status(thm)],[f3])).
% 64.12/8.55 fof(f9,plain,(
% 64.12/8.55 ![X0,X1,X2]: (meet(meet(join(X0,X1),join(X1,X2)),X1)=X1)),
% 64.12/8.55 inference(cnf_transformation,[status(thm)],[f4])).
% 64.12/8.55 fof(f10,plain,(
% 64.12/8.55 ~meet(meet(a,b),c)=meet(a,meet(b,c))),
% 64.12/8.55 inference(cnf_transformation,[status(thm)],[f5])).
% 64.12/8.55 fof(f16,plain,(
% 64.12/8.55 ![X0,X1]: (meet(join(X0,X1),X1)=X1)),
% 64.12/8.55 inference(paramodulation,[status(thm)],[f7,f9])).
% 64.12/8.55 fof(f17,plain,(
% 64.12/8.55 ![X0,X1]: (join(X0,meet(X0,X1))=X0)),
% 64.12/8.55 inference(paramodulation,[status(thm)],[f16,f6])).
% 64.12/8.55 fof(f20,plain,(
% 64.12/8.55 ![X0,X1,X2,X3]: (join(meet(join(X0,X1),join(X1,X2)),meet(X3,X1))=meet(join(X0,X1),join(X1,X2)))),
% 64.12/8.55 inference(paramodulation,[status(thm)],[f9,f6])).
% 64.12/8.55 fof(f21,plain,(
% 64.12/8.55 ![X0,X1]: (join(X0,meet(X1,X0))=X0)),
% 64.12/8.55 inference(paramodulation,[status(thm)],[f7,f6])).
% 64.12/8.55 fof(f22,plain,(
% 64.12/8.55 ![X0,X1,X2]: (meet(X0,meet(X1,meet(X0,X2)))=meet(X1,meet(X0,X2)))),
% 64.12/8.55 inference(paramodulation,[status(thm)],[f6,f16])).
% 64.12/8.55 fof(f23,plain,(
% 64.12/8.55 ![X0,X1]: (meet(X0,join(X1,X0))=X0)),
% 64.12/8.55 inference(paramodulation,[status(thm)],[f6,f7])).
% 64.12/8.55 fof(f25,plain,(
% 64.12/8.55 ![X0,X1,X2,X3]: (meet(meet(X0,join(meet(X1,meet(X0,X2)),X3)),meet(X1,meet(X0,X2)))=meet(X1,meet(X0,X2)))),
% 64.12/8.55 inference(paramodulation,[status(thm)],[f6,f9])).
% 64.12/8.55 fof(f30,plain,(
% 64.12/8.55 ![X0,X1]: (join(meet(X0,X1),X1)=X1)),
% 64.12/8.55 inference(paramodulation,[status(thm)],[f6,f8])).
% 64.12/8.55 fof(f36,plain,(
% 64.12/8.55 ![X0,X1,X2,X3]: (join(join(meet(X0,meet(join(X1,X2),join(X2,X3))),X2),meet(join(X1,X2),join(X2,X3)))=meet(join(X1,X2),join(X2,X3)))),
% 64.12/8.55 inference(paramodulation,[status(thm)],[f9,f8])).
% 64.12/8.55 fof(f39,plain,(
% 64.12/8.55 ![X0,X1]: (meet(X0,join(X0,X1))=X0)),
% 64.12/8.55 inference(paramodulation,[status(thm)],[f8,f7])).
% 64.12/8.55 fof(f42,plain,(
% 64.12/8.55 ![X0,X1,X2,X3]: (meet(meet(join(X0,join(meet(X1,X2),meet(X2,X3))),X2),join(meet(X1,X2),meet(X2,X3)))=join(meet(X1,X2),meet(X2,X3)))),
% 64.12/8.55 inference(paramodulation,[status(thm)],[f8,f9])).
% 64.12/8.55 fof(f80,plain,(
% 64.12/8.55 ![X0,X1]: (join(join(X0,X1),X0)=join(X0,X1))),
% 64.12/8.55 inference(paramodulation,[status(thm)],[f39,f21])).
% 64.12/8.55 fof(f86,plain,(
% 64.12/8.55 ![X0,X1]: (meet(X0,meet(X1,X0))=meet(X1,X0))),
% 64.12/8.55 inference(paramodulation,[status(thm)],[f21,f16])).
% 64.12/8.55 fof(f95,plain,(
% 64.12/8.55 ![X0,X1]: (join(X0,join(X1,X0))=join(X1,X0))),
% 64.12/8.55 inference(paramodulation,[status(thm)],[f23,f30])).
% 64.12/8.55 fof(f101,plain,(
% 64.12/8.55 ![X0,X1,X2]: (meet(meet(X0,X1),join(X2,X1))=meet(X0,X1))),
% 64.12/8.55 inference(paramodulation,[status(thm)],[f30,f7])).
% 64.12/8.55 fof(f116,plain,(
% 64.12/8.55 ![X0,X1]: (meet(meet(X0,X1),X0)=meet(X0,X1))),
% 64.12/8.55 inference(paramodulation,[status(thm)],[f17,f23])).
% 64.12/8.55 fof(f299,plain,(
% 64.12/8.55 ![X0,X1,X2,X3]: (meet(meet(join(X0,X1),join(X1,X2)),meet(X3,X1))=meet(X3,X1))),
% 64.12/8.55 inference(paramodulation,[status(thm)],[f20,f16])).
% 64.12/8.55 fof(f491,plain,(
% 64.12/8.55 ![X0,X1]: (join(meet(X0,X1),X0)=join(X0,meet(X0,X1)))),
% 64.12/8.55 inference(paramodulation,[status(thm)],[f17,f95])).
% 64.12/8.55 fof(f507,plain,(
% 64.12/8.55 ![X0,X1,X2]: (meet(meet(join(X0,X1),join(X2,X1)),X1)=X1)),
% 64.12/8.55 inference(paramodulation,[status(thm)],[f95,f9])).
% 64.12/8.55 fof(f517,plain,(
% 64.12/8.55 ![X0,X1]: (join(meet(X0,X1),X0)=X0)),
% 64.12/8.55 inference(forward_demodulation,[status(thm)],[f17,f491])).
% 64.12/8.55 fof(f537,plain,(
% 64.12/8.55 ![X0,X1,X2]: (meet(meet(X0,X1),meet(X1,meet(X0,X2)))=meet(X1,meet(X0,X2)))),
% 64.12/8.55 inference(paramodulation,[status(thm)],[f517,f25])).
% 64.12/8.55 fof(f551,plain,(
% 64.12/8.55 ![X0,X1,X2]: (meet(meet(X0,X1),join(X2,X0))=meet(X0,X1))),
% 64.12/8.55 inference(paramodulation,[status(thm)],[f517,f7])).
% 64.12/8.55 fof(f565,plain,(
% 64.12/8.55 ![X0,X1,X2]: (meet(X0,meet(join(X1,X0),join(X0,X2)))=meet(meet(join(X1,X0),join(X0,X2)),X0))),
% 64.12/8.55 inference(paramodulation,[status(thm)],[f9,f116])).
% 64.12/8.55 fof(f592,plain,(
% 64.12/8.55 ![X0,X1,X2]: (meet(X0,meet(join(X1,X0),join(X0,X2)))=X0)),
% 64.12/8.55 inference(forward_demodulation,[status(thm)],[f9,f565])).
% 64.12/8.55 fof(f744,plain,(
% 64.12/8.55 ![X0,X1,X2]: (meet(X0,meet(join(X1,X0),join(X2,X0)))=X0)),
% 64.12/8.55 inference(paramodulation,[status(thm)],[f95,f592])).
% 64.12/8.55 fof(f808,plain,(
% 64.12/8.55 ![X0,X1,X2]: (meet(meet(X0,join(X1,meet(X2,X0))),meet(X2,X0))=meet(X2,X0))),
% 64.12/8.55 inference(paramodulation,[status(thm)],[f21,f507])).
% 64.12/8.55 fof(f875,plain,(
% 64.12/8.55 ![X0,X1,X2]: (meet(X0,meet(join(X0,X1),join(X2,X0)))=X0)),
% 64.12/8.55 inference(paramodulation,[status(thm)],[f80,f744])).
% 64.12/8.55 fof(f1275,plain,(
% 64.12/8.55 ![X0,X1,X2]: (meet(meet(X0,X1),join(X0,X2))=meet(X0,X1))),
% 64.12/8.55 inference(paramodulation,[status(thm)],[f80,f551])).
% 64.12/8.55 fof(f2035,plain,(
% 64.12/8.55 ![X0,X1]: (join(join(X0,X1),meet(join(X0,X1),join(X1,X0)))=meet(join(X0,X1),join(X1,X0)))),
% 64.12/8.55 inference(paramodulation,[status(thm)],[f875,f36])).
% 64.12/8.55 fof(f2162,plain,(
% 64.12/8.55 ![X0,X1]: (join(X0,X1)=meet(join(X0,X1),join(X1,X0)))),
% 64.12/8.55 inference(forward_demodulation,[status(thm)],[f17,f2035])).
% 64.12/8.55 fof(f2656,plain,(
% 64.12/8.55 ![X0,X1]: (meet(join(X0,X1),join(X1,X0))=meet(join(X1,X0),join(X0,X1)))),
% 64.12/8.55 inference(paramodulation,[status(thm)],[f2162,f86])).
% 64.12/8.55 fof(f2713,plain,(
% 64.12/8.55 ![X0,X1]: (join(X0,X1)=meet(join(X1,X0),join(X0,X1)))),
% 64.12/8.55 inference(forward_demodulation,[status(thm)],[f2162,f2656])).
% 64.12/8.55 fof(f2715,plain,(
% 64.12/8.55 ![X0,X1]: (join(X0,X1)=join(X1,X0))),
% 64.12/8.55 inference(paramodulation,[status(thm)],[f2162,f2713])).
% 64.12/8.55 fof(f4919,plain,(
% 64.12/8.55 ![X0,X1]: (meet(meet(X0,X1),meet(X1,X0))=meet(X1,X0))),
% 64.12/8.55 inference(paramodulation,[status(thm)],[f17,f808])).
% 64.12/8.55 fof(f5275,plain,(
% 64.12/8.55 ![X0,X1]: (meet(meet(meet(X0,X1),meet(X1,X0)),meet(X0,X1))=meet(meet(X1,X0),meet(X0,X1)))),
% 64.12/8.55 inference(paramodulation,[status(thm)],[f4919,f4919])).
% 64.12/8.55 fof(f5313,plain,(
% 64.12/8.55 ![X0,X1,X2]: (meet(meet(X0,X1),join(meet(X1,X0),X2))=meet(meet(X1,X0),meet(X0,X1)))),
% 64.12/8.55 inference(paramodulation,[status(thm)],[f4919,f1275])).
% 64.12/8.55 fof(f5315,plain,(
% 64.12/8.55 ![X0,X1,X2]: (meet(meet(X0,X1),join(X2,meet(X1,X0)))=meet(meet(X1,X0),meet(X0,X1)))),
% 64.12/8.55 inference(paramodulation,[status(thm)],[f4919,f551])).
% 64.12/8.55 fof(f5324,plain,(
% 64.12/8.55 ![X0,X1]: (join(meet(X0,X1),meet(X1,X0))=meet(X0,X1))),
% 64.12/8.55 inference(paramodulation,[status(thm)],[f4919,f17])).
% 64.12/8.55 fof(f5360,plain,(
% 64.12/8.55 ![X0,X1]: (meet(meet(X0,X1),meet(X1,X0))=meet(meet(X1,X0),meet(X0,X1)))),
% 64.12/8.55 inference(forward_demodulation,[status(thm)],[f116,f5275])).
% 64.12/8.55 fof(f5361,plain,(
% 64.12/8.55 ![X0,X1]: (meet(X0,X1)=meet(meet(X0,X1),meet(X1,X0)))),
% 64.12/8.55 inference(forward_demodulation,[status(thm)],[f4919,f5360])).
% 64.12/8.55 fof(f5437,plain,(
% 64.12/8.55 ![X0,X1,X2]: (meet(meet(X0,X1),join(meet(X1,X0),X2))=meet(X0,X1))),
% 64.12/8.55 inference(forward_demodulation,[status(thm)],[f4919,f5313])).
% 64.12/8.55 fof(f5440,plain,(
% 64.12/8.55 ![X0,X1,X2]: (meet(meet(X0,X1),join(X2,meet(X1,X0)))=meet(X0,X1))),
% 64.12/8.55 inference(forward_demodulation,[status(thm)],[f4919,f5315])).
% 64.12/8.55 fof(f5455,plain,(
% 64.12/8.55 ![X0,X1]: (meet(X0,X1)=meet(X1,X0))),
% 64.12/8.55 inference(paramodulation,[status(thm)],[f4919,f5361])).
% 64.12/8.55 fof(f5548,plain,(
% 64.12/8.55 ![X0,X1,X2,X3]: (meet(meet(join(X0,join(meet(meet(X1,X2),meet(X2,X1)),meet(meet(X2,X1),X3))),meet(X2,X1)),join(meet(X1,X2),meet(meet(X2,X1),X3)))=join(meet(meet(X1,X2),meet(X2,X1)),meet(meet(X2,X1),X3)))),
% 64.12/8.55 inference(paramodulation,[status(thm)],[f5361,f42])).
% 64.12/8.55 fof(f5575,plain,(
% 64.12/8.55 ~meet(c,meet(a,b))=meet(a,meet(b,c))),
% 64.12/8.55 inference(backward_demodulation,[status(thm)],[f5455,f10])).
% 64.12/8.55 fof(f5971,plain,(
% 64.12/8.55 ![X0,X1,X2,X3]: (meet(join(meet(X0,X1),meet(meet(X1,X0),X2)),meet(join(X3,join(meet(meet(X0,X1),meet(X1,X0)),meet(meet(X1,X0),X2))),meet(X1,X0)))=join(meet(meet(X0,X1),meet(X1,X0)),meet(meet(X1,X0),X2)))),
% 64.12/8.55 inference(forward_demodulation,[status(thm)],[f5455,f5548])).
% 64.12/8.55 fof(f5972,plain,(
% 64.12/8.55 ![X0,X1,X2,X3]: (meet(join(meet(X0,X1),meet(meet(X1,X0),X2)),meet(meet(X1,X0),join(X3,join(meet(meet(X0,X1),meet(X1,X0)),meet(meet(X1,X0),X2)))))=join(meet(meet(X0,X1),meet(X1,X0)),meet(meet(X1,X0),X2)))),
% 64.12/8.55 inference(forward_demodulation,[status(thm)],[f5455,f5971])).
% 64.12/8.55 fof(f5973,plain,(
% 64.12/8.55 ![X0,X1,X2,X3]: (meet(join(meet(X0,X1),meet(meet(X1,X0),X2)),meet(meet(X1,X0),join(X3,join(meet(X0,X1),meet(meet(X1,X0),X2)))))=join(meet(meet(X0,X1),meet(X1,X0)),meet(meet(X1,X0),X2)))),
% 64.12/8.55 inference(forward_demodulation,[status(thm)],[f5361,f5972])).
% 64.12/8.55 fof(f5974,plain,(
% 64.12/8.55 ![X0,X1,X2,X3]: (meet(join(meet(X0,X1),meet(meet(X1,X0),X2)),meet(meet(X1,X0),join(X3,join(meet(X0,X1),meet(meet(X1,X0),X2)))))=join(meet(X0,X1),meet(meet(X1,X0),X2)))),
% 64.12/8.55 inference(forward_demodulation,[status(thm)],[f5361,f5973])).
% 64.12/8.55 fof(f6134,plain,(
% 64.12/8.55 ![X0,X1,X2,X3]: (meet(meet(meet(X0,X1),join(meet(X1,X0),X2)),meet(X3,meet(X1,X0)))=meet(X3,meet(X1,X0)))),
% 64.12/8.55 inference(paramodulation,[status(thm)],[f5324,f299])).
% 64.12/8.55 fof(f6161,plain,(
% 64.12/8.55 ![X0,X1,X2]: (meet(meet(X0,X1),meet(join(X2,meet(X0,X1)),meet(X1,X0)))=meet(X0,X1))),
% 64.12/8.55 inference(paramodulation,[status(thm)],[f5324,f744])).
% 64.12/8.55 fof(f6265,plain,(
% 64.12/8.55 ![X0,X1,X2]: (meet(meet(X0,X1),meet(X2,meet(X1,X0)))=meet(X2,meet(X1,X0)))),
% 64.12/8.55 inference(forward_demodulation,[status(thm)],[f5437,f6134])).
% 64.12/8.55 fof(f6302,plain,(
% 64.12/8.55 ![X0,X1,X2]: (meet(join(X0,meet(X1,X2)),meet(X2,X1))=meet(X1,X2))),
% 64.12/8.55 inference(forward_demodulation,[status(thm)],[f6265,f6161])).
% 64.12/8.55 fof(f6303,plain,(
% 64.12/8.55 ![X0,X1,X2]: (meet(meet(X0,X1),join(X2,meet(X1,X0)))=meet(X1,X0))),
% 64.12/8.55 inference(forward_demodulation,[status(thm)],[f5455,f6302])).
% 64.12/8.55 fof(f6795,plain,(
% 64.12/8.55 ![X0,X1]: (meet(meet(X0,X1),X1)=meet(X1,X0))),
% 64.12/8.55 inference(paramodulation,[status(thm)],[f17,f6303])).
% 64.12/8.55 fof(f6796,plain,(
% 64.12/8.55 ![X0,X1]: (meet(meet(X0,X1),X0)=meet(X1,X0))),
% 64.12/8.55 inference(paramodulation,[status(thm)],[f21,f6303])).
% 64.12/8.55 fof(f6942,plain,(
% 64.12/8.55 ![X0,X1]: (meet(X0,meet(X1,X0))=meet(X0,X1))),
% 64.12/8.55 inference(forward_demodulation,[status(thm)],[f5455,f6795])).
% 64.12/8.55 fof(f6943,plain,(
% 64.12/8.55 ![X0,X1]: (meet(X0,meet(X0,X1))=meet(X1,X0))),
% 64.12/8.55 inference(forward_demodulation,[status(thm)],[f5455,f6796])).
% 64.12/8.55 fof(f8460,plain,(
% 64.12/8.55 ![X0,X1,X2,X3]: (meet(meet(X0,X1),join(X2,join(meet(X1,X0),X3)))=meet(meet(X0,X1),join(meet(X1,X0),X3)))),
% 64.12/8.55 inference(paramodulation,[status(thm)],[f5437,f101])).
% 64.12/8.55 fof(f8622,plain,(
% 64.12/8.55 ![X0,X1,X2]: (meet(join(meet(X0,X1),meet(meet(X1,X0),X2)),meet(X1,X0))=join(meet(X0,X1),meet(meet(X1,X0),X2)))),
% 64.12/8.55 inference(backward_demodulation,[status(thm)],[f8623,f5974])).
% 64.12/8.55 fof(f8623,plain,(
% 64.12/8.55 ![X0,X1,X2,X3]: (meet(meet(X0,X1),join(X2,join(meet(X1,X0),X3)))=meet(X0,X1))),
% 64.12/8.55 inference(forward_demodulation,[status(thm)],[f5437,f8460])).
% 64.12/8.55 fof(f8627,plain,(
% 64.12/8.55 ![X0,X1,X2]: (meet(meet(X0,X1),join(meet(X1,X0),meet(meet(X0,X1),X2)))=join(meet(X1,X0),meet(meet(X0,X1),X2)))),
% 64.12/8.55 inference(forward_demodulation,[status(thm)],[f5455,f8622])).
% 64.12/8.55 fof(f8629,plain,(
% 64.12/8.55 ![X0,X1,X2]: (meet(X0,X1)=join(meet(X1,X0),meet(meet(X0,X1),X2)))),
% 64.12/8.55 inference(forward_demodulation,[status(thm)],[f5437,f8627])).
% 64.12/8.55 fof(f9401,plain,(
% 64.12/8.55 ![X0,X1,X2,X3]: (meet(meet(meet(X0,X1),X2),meet(X2,meet(X0,X1)))=meet(X2,meet(meet(X0,X1),join(X3,meet(X1,X0)))))),
% 64.12/8.55 inference(paramodulation,[status(thm)],[f5440,f537])).
% 64.12/8.55 fof(f9412,plain,(
% 64.12/8.55 ![X0,X1,X2]: (meet(meet(X0,X1),meet(X1,meet(X2,X0)))=meet(X1,meet(X0,meet(X0,X2))))),
% 64.12/8.55 inference(paramodulation,[status(thm)],[f6943,f537])).
% 64.12/8.55 fof(f9463,plain,(
% 64.12/8.55 ![X0,X1,X2]: (join(meet(X0,X1),meet(X1,meet(X0,X2)))=meet(X0,X1))),
% 64.12/8.55 inference(paramodulation,[status(thm)],[f537,f17])).
% 64.12/8.55 fof(f9527,plain,(
% 64.12/8.55 ![X0,X1,X2,X3]: (meet(meet(X0,X1),X2)=meet(X2,meet(meet(X0,X1),join(X3,meet(X1,X0)))))),
% 64.12/8.55 inference(forward_demodulation,[status(thm)],[f5361,f9401])).
% 64.12/8.55 fof(f9528,plain,(
% 64.12/8.55 ![X0,X1,X2]: (meet(meet(X0,X1),X2)=meet(X2,meet(X1,X0)))),
% 64.12/8.55 inference(forward_demodulation,[status(thm)],[f6303,f9527])).
% 64.12/8.55 fof(f9549,plain,(
% 64.12/8.55 ![X0,X1,X2]: (meet(meet(X0,X1),meet(X1,meet(X2,X0)))=meet(X1,meet(X2,X0)))),
% 64.12/8.55 inference(forward_demodulation,[status(thm)],[f6943,f9412])).
% 64.12/8.55 fof(f10101,plain,(
% 64.12/8.55 ![X0,X1,X2]: (meet(X0,X1)=join(meet(X1,X0),meet(X1,meet(X0,X2))))),
% 64.12/8.55 inference(paramodulation,[status(thm)],[f537,f8629])).
% 64.12/8.55 fof(f10201,plain,(
% 64.12/8.55 ![X0,X1,X2]: (meet(meet(meet(X0,X1),X2),meet(X1,X0))=meet(meet(X0,X1),X2))),
% 64.12/8.55 inference(paramodulation,[status(thm)],[f8629,f1275])).
% 64.12/8.55 fof(f10468,plain,(
% 64.12/8.55 ![X0,X1,X2]: (meet(meet(X0,X1),meet(X2,meet(X1,X0)))=meet(meet(X1,X0),X2))),
% 64.12/8.55 inference(forward_demodulation,[status(thm)],[f9528,f10201])).
% 64.12/8.55 fof(f10565,plain,(
% 64.12/8.55 ![X0,X1,X2]: (join(meet(X0,X1),meet(X1,meet(X2,X0)))=meet(X0,X1))),
% 64.12/8.55 inference(paramodulation,[status(thm)],[f6943,f9463])).
% 64.12/8.55 fof(f10807,plain,(
% 64.12/8.55 ![X0,X1,X2]: (meet(X0,meet(X1,X0))=join(meet(meet(X1,X0),X0),meet(X0,meet(X1,X2))))),
% 64.12/8.55 inference(paramodulation,[status(thm)],[f537,f10101])).
% 64.12/8.55 fof(f10977,plain,(
% 64.12/8.55 ![X0,X1,X2]: (meet(X0,X1)=join(meet(meet(X1,X0),X0),meet(X0,meet(X1,X2))))),
% 64.12/8.55 inference(forward_demodulation,[status(thm)],[f6942,f10807])).
% 64.12/8.55 fof(f10978,plain,(
% 64.12/8.55 ![X0,X1,X2]: (meet(X0,X1)=join(meet(X0,meet(X0,X1)),meet(X0,meet(X1,X2))))),
% 64.12/8.55 inference(forward_demodulation,[status(thm)],[f9528,f10977])).
% 64.12/8.55 fof(f10979,plain,(
% 64.12/8.55 ![X0,X1,X2]: (meet(X0,X1)=join(meet(X1,X0),meet(X0,meet(X1,X2))))),
% 64.12/8.55 inference(forward_demodulation,[status(thm)],[f6943,f10978])).
% 64.12/8.55 fof(f11570,plain,(
% 64.12/8.55 ![X0,X1,X2]: (join(meet(meet(X0,X1),meet(X0,X2)),meet(X2,meet(X0,X1)))=meet(meet(X0,X1),meet(X0,X2)))),
% 64.12/8.55 inference(paramodulation,[status(thm)],[f537,f10565])).
% 64.12/8.55 fof(f11625,plain,(
% 64.12/8.55 ![X0,X1,X2]: (meet(meet(meet(X0,X1),X2),meet(X1,X2))=meet(meet(X0,X1),X2))),
% 64.12/8.55 inference(paramodulation,[status(thm)],[f10565,f5440])).
% 64.12/8.55 fof(f11710,plain,(
% 64.12/8.55 ![X0,X1,X2]: (join(meet(X0,meet(X1,X2)),meet(meet(X1,X2),meet(X1,X0)))=meet(meet(X1,X2),meet(X1,X0)))),
% 64.12/8.55 inference(forward_demodulation,[status(thm)],[f2715,f11570])).
% 64.12/8.55 fof(f11715,plain,(
% 64.12/8.55 ![X0,X1,X2]: (meet(X0,meet(X1,X2))=meet(meet(X1,X2),meet(X1,X0)))),
% 64.12/8.55 inference(forward_demodulation,[status(thm)],[f10565,f11710])).
% 64.12/8.55 fof(f11763,plain,(
% 64.12/8.55 ![X0,X1,X2]: (meet(meet(X0,X1),meet(X1,meet(X2,X0)))=meet(meet(X2,X0),X1))),
% 64.12/8.55 inference(forward_demodulation,[status(thm)],[f9528,f11625])).
% 64.12/8.55 fof(f11922,plain,(
% 64.12/8.55 ![X0,X1,X2]: (meet(meet(meet(X0,X1),X2),meet(X2,X0))=meet(meet(X0,X1),X2))),
% 64.12/8.55 inference(paramodulation,[status(thm)],[f10979,f5440])).
% 64.12/8.55 fof(f12054,plain,(
% 64.12/8.55 ![X0,X1,X2]: (meet(meet(X0,X1),meet(X0,meet(X1,X2)))=meet(meet(X1,X2),X0))),
% 64.12/8.55 inference(forward_demodulation,[status(thm)],[f9528,f11922])).
% 64.12/8.55 fof(f12055,plain,(
% 64.12/8.55 ![X0,X1,X2]: (meet(meet(X0,X1),meet(X2,X0))=meet(meet(X0,X1),X2))),
% 64.12/8.55 inference(forward_demodulation,[status(thm)],[f11715,f12054])).
% 64.12/8.55 fof(f12778,plain,(
% 64.12/8.55 ![X0,X1,X2]: (meet(X0,meet(X1,meet(X1,X2)))=meet(meet(X2,X1),meet(X1,X0)))),
% 64.12/8.55 inference(paramodulation,[status(thm)],[f6943,f11715])).
% 64.12/8.55 fof(f12781,plain,(
% 64.12/8.55 ![X0,X1,X2]: (meet(X0,meet(X1,meet(X2,X1)))=meet(meet(X2,X1),meet(X1,X0)))),
% 64.12/8.55 inference(paramodulation,[status(thm)],[f86,f11715])).
% 64.12/8.55 fof(f12796,plain,(
% 64.12/8.55 ![X0,X1,X2,X3]: (meet(meet(X0,X1),meet(meet(X0,X2),X3))=meet(meet(meet(X0,X2),X3),meet(X1,meet(X0,X2))))),
% 64.12/8.55 inference(paramodulation,[status(thm)],[f11715,f11715])).
% 64.12/8.55 fof(f12812,plain,(
% 64.12/8.55 ![X0,X1,X2]: (meet(meet(X0,X1),meet(X1,X2))=meet(meet(X1,X2),meet(X1,X0)))),
% 64.12/8.55 inference(paramodulation,[status(thm)],[f6942,f11715])).
% 64.12/8.55 fof(f12835,plain,(
% 64.12/8.55 ![X0,X1,X2]: (meet(meet(X0,meet(X0,X1)),meet(X2,meet(X0,X1)))=meet(meet(X0,X1),meet(X0,X2)))),
% 64.12/8.55 inference(paramodulation,[status(thm)],[f11715,f537])).
% 64.12/8.55 fof(f12852,plain,(
% 64.12/8.55 ![X0,X1,X2,X3]: (meet(meet(X0,X1),meet(X0,X2))=join(meet(X1,meet(X0,X2)),meet(meet(X0,X2),meet(meet(X0,X1),X3))))),
% 64.12/8.55 inference(paramodulation,[status(thm)],[f11715,f10101])).
% 64.12/8.55 fof(f12940,plain,(
% 64.12/8.55 ![X0,X1,X2]: (meet(meet(X0,X1),meet(X1,X2))=meet(meet(X0,X1),X2))),
% 64.12/8.55 inference(backward_demodulation,[status(thm)],[f12943,f11763])).
% 64.12/8.55 fof(f12942,plain,(
% 64.12/8.55 ![X0,X1,X2]: (meet(meet(X0,X1),meet(X1,X2))=meet(X2,meet(X0,X1)))),
% 64.12/8.55 inference(backward_demodulation,[status(thm)],[f12943,f9549])).
% 64.12/8.55 fof(f12943,plain,(
% 64.12/8.55 ![X0,X1,X2]: (meet(X0,meet(X1,X2))=meet(meet(X1,X2),meet(X2,X0)))),
% 64.12/8.55 inference(forward_demodulation,[status(thm)],[f6943,f12778])).
% 64.12/8.55 fof(f12946,plain,(
% 64.12/8.55 ![X0,X1,X2]: (meet(X0,meet(X1,X2))=meet(meet(X2,X1),meet(X1,X0)))),
% 64.12/8.55 inference(forward_demodulation,[status(thm)],[f6942,f12781])).
% 64.12/8.55 fof(f12971,plain,(
% 64.12/8.55 ![X0,X1,X2,X3]: (meet(meet(X0,X1),meet(meet(X0,X2),X3))=meet(meet(meet(X0,X2),X3),X1))),
% 55.88/8.66 inference(forward_demodulation,[status(thm)],[f12055,f12796])).
% 55.88/8.66 fof(f13002,plain,(
% 55.88/8.66 ![X0,X1,X2]: (meet(X0,meet(X1,X2))=meet(meet(X1,X0),meet(X1,X2)))),
% 55.88/8.66 inference(forward_demodulation,[status(thm)],[f12946,f12812])).
% 55.88/8.66 fof(f13036,plain,(
% 55.88/8.66 ![X0,X1,X2]: (meet(meet(X0,X1),meet(X2,meet(X1,X0)))=meet(meet(X1,X0),meet(X1,X2)))),
% 55.88/8.66 inference(forward_demodulation,[status(thm)],[f6943,f12835])).
% 55.88/8.66 fof(f13037,plain,(
% 55.88/8.66 ![X0,X1,X2]: (meet(meet(X0,X1),X2)=meet(meet(X0,X1),meet(X0,X2)))),
% 55.88/8.66 inference(forward_demodulation,[status(thm)],[f10468,f13036])).
% 55.88/8.66 fof(f13318,plain,(
% 55.88/8.66 ![X0,X1,X2]: (meet(meet(X0,X1),X2)=meet(X1,meet(X0,X2)))),
% 55.88/8.66 inference(forward_demodulation,[status(thm)],[f13002,f13037])).
% 55.88/8.66 fof(f13357,plain,(
% 55.88/8.66 ![X0,X1,X2,X3]: (meet(X0,meet(X1,X2))=join(meet(X2,meet(X1,X0)),meet(meet(X1,X0),meet(meet(X1,X2),X3))))),
% 55.88/8.66 inference(forward_demodulation,[status(thm)],[f11715,f12852])).
% 55.88/8.66 fof(f13358,plain,(
% 55.88/8.66 ![X0,X1,X2,X3]: (meet(X0,meet(X1,X2))=join(meet(X2,meet(X1,X0)),meet(meet(meet(X1,X2),X3),X0)))),
% 55.88/8.66 inference(forward_demodulation,[status(thm)],[f12971,f13357])).
% 55.88/8.66 fof(f13359,plain,(
% 55.88/8.66 ![X0,X1,X2,X3]: (meet(X0,meet(X1,X2))=join(meet(X2,meet(X1,X0)),meet(X3,meet(meet(X1,X2),X0))))),
% 55.88/8.66 inference(forward_demodulation,[status(thm)],[f13318,f13358])).
% 55.88/8.66 fof(f13360,plain,(
% 55.88/8.66 ![X0,X1,X2,X3]: (meet(X0,meet(X1,X2))=join(meet(X2,meet(X1,X0)),meet(X3,meet(X2,meet(X1,X0)))))),
% 55.88/8.66 inference(forward_demodulation,[status(thm)],[f13318,f13359])).
% 55.88/8.66 fof(f13361,plain,(
% 55.88/8.66 ~meet(b,meet(a,c))=meet(a,meet(b,c))),
% 55.88/8.66 inference(backward_demodulation,[status(thm)],[f13364,f5575])).
% 55.88/8.66 fof(f13364,plain,(
% 55.88/8.66 ![X0,X1,X2]: (meet(X0,meet(X1,X2))=meet(X2,meet(X1,X0)))),
% 55.88/8.66 inference(forward_demodulation,[status(thm)],[f21,f13360])).
% 55.88/8.66 fof(f13563,plain,(
% 55.88/8.66 ![X0,X1,X2]: (meet(X0,meet(X1,meet(X0,X2)))=meet(meet(X1,X0),X2))),
% 55.88/8.66 inference(forward_demodulation,[status(thm)],[f13318,f12940])).
% 55.88/8.66 fof(f13564,plain,(
% 55.88/8.66 ![X0,X1,X2]: (meet(X0,meet(X1,X2))=meet(meet(X0,X1),X2))),
% 55.88/8.66 inference(forward_demodulation,[status(thm)],[f22,f13563])).
% 55.88/8.66 fof(f13566,plain,(
% 55.88/8.66 ![X0,X1,X2]: (meet(X0,meet(X1,meet(X1,X2)))=meet(X2,meet(X0,X1)))),
% 55.88/8.66 inference(forward_demodulation,[status(thm)],[f13564,f12942])).
% 55.88/8.66 fof(f13567,plain,(
% 55.88/8.66 ![X0,X1,X2]: (meet(X0,meet(X1,X2))=meet(X1,meet(X0,X2)))),
% 55.88/8.66 inference(forward_demodulation,[status(thm)],[f6943,f13566])).
% 55.88/8.66 fof(f14149,plain,(
% 55.88/8.66 ~meet(a,meet(b,c))=meet(a,meet(b,c))),
% 55.88/8.66 inference(forward_demodulation,[status(thm)],[f13567,f13361])).
% 55.88/8.66 fof(f14150,plain,(
% 55.88/8.66 $false),
% 55.88/8.66 inference(trivial_equality_resolution,[status(thm)],[f14149])).
% 55.88/8.66 % SZS output end CNFRefutation for theBenchmark.p
% 42.58/9.87 % Elapsed time: 9.272146 seconds
% 42.58/9.87 % CPU time: 32.923066 seconds
% 42.58/9.87 % Total memory used: 219.926 MB
% 42.58/9.87 % Net memory used: 216.320 MB
%------------------------------------------------------------------------------