%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : LAT009-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 : n015.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 4.87s 1.06s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT009-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.35 % Computer : n015.cluster.edu
% 0.10/0.35 % Model : x86_64 x86_64
% 0.10/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.35 % Memory : 8046.5625MB
% 0.10/0.35 % 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:09:21 UTC 2026
% 0.14/0.36 % CPUTime :
% 0.14/0.37 % Drodi V4.1.1
% 4.87/1.06 % Refutation found
% 4.87/1.06 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 4.87/1.06 % SZS output start CNFRefutation for theBenchmark
% 4.87/1.06 fof(f1,axiom,(
% 4.87/1.06 (![X]: (meet(X,X) = X ))),
% 4.87/1.06 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 4.87/1.06 fof(f2,axiom,(
% 4.87/1.06 (![X]: (join(X,X) = X ))),
% 4.87/1.06 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 4.87/1.06 fof(f3,axiom,(
% 4.87/1.06 (![X,Y]: (meet(X,join(X,Y)) = X ))),
% 4.87/1.06 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 4.87/1.06 fof(f4,axiom,(
% 4.87/1.06 (![X,Y]: (join(X,meet(X,Y)) = X ))),
% 4.87/1.06 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 4.87/1.06 fof(f5,axiom,(
% 4.87/1.06 (![X,Y]: (meet(X,Y) = meet(Y,X) ))),
% 4.87/1.06 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 4.87/1.06 fof(f6,axiom,(
% 4.87/1.06 (![X,Y]: (join(X,Y) = join(Y,X) ))),
% 4.87/1.06 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 4.87/1.06 fof(f7,axiom,(
% 4.87/1.06 (![X,Y,Z]: (meet(meet(X,Y),Z) = meet(X,meet(Y,Z)) ))),
% 4.87/1.06 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 4.87/1.06 fof(f8,axiom,(
% 4.87/1.06 (![X,Y,Z]: (join(join(X,Y),Z) = join(X,join(Y,Z)) ))),
% 4.87/1.06 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 4.87/1.06 fof(f9,axiom,(
% 4.87/1.06 (![X,Y,Z]: (join(meet(join(meet(X,Y),Z),Y),meet(Z,X)) = meet(join(meet(join(X,Y),Z),Y),join(Z,X)) ))),
% 4.87/1.06 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 4.87/1.06 fof(f10,negated_conjecture,(
% 4.87/1.06 join(a,meet(b,c)) != meet(join(a,b),join(a,c)) ),
% 4.87/1.06 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 4.87/1.06 fof(f11,plain,(
% 4.87/1.06 ![X0]: (meet(X0,X0)=X0)),
% 4.87/1.06 inference(cnf_transformation,[status(thm)],[f1])).
% 4.87/1.06 fof(f12,plain,(
% 4.87/1.06 ![X0]: (join(X0,X0)=X0)),
% 4.87/1.06 inference(cnf_transformation,[status(thm)],[f2])).
% 4.87/1.06 fof(f13,plain,(
% 4.87/1.06 ![X0,X1]: (meet(X0,join(X0,X1))=X0)),
% 4.87/1.06 inference(cnf_transformation,[status(thm)],[f3])).
% 4.87/1.06 fof(f14,plain,(
% 4.87/1.06 ![X0,X1]: (join(X0,meet(X0,X1))=X0)),
% 4.87/1.06 inference(cnf_transformation,[status(thm)],[f4])).
% 4.87/1.06 fof(f15,plain,(
% 4.87/1.06 ![X0,X1]: (meet(X0,X1)=meet(X1,X0))),
% 4.87/1.06 inference(cnf_transformation,[status(thm)],[f5])).
% 4.87/1.06 fof(f16,plain,(
% 4.87/1.06 ![X0,X1]: (join(X0,X1)=join(X1,X0))),
% 4.87/1.06 inference(cnf_transformation,[status(thm)],[f6])).
% 4.87/1.06 fof(f17,plain,(
% 4.87/1.06 ![X0,X1,X2]: (meet(meet(X0,X1),X2)=meet(X0,meet(X1,X2)))),
% 4.87/1.06 inference(cnf_transformation,[status(thm)],[f7])).
% 4.87/1.06 fof(f18,plain,(
% 4.87/1.06 ![X0,X1,X2]: (join(join(X0,X1),X2)=join(X0,join(X1,X2)))),
% 4.87/1.06 inference(cnf_transformation,[status(thm)],[f8])).
% 4.87/1.06 fof(f19,plain,(
% 4.87/1.06 ![X0,X1,X2]: (join(meet(join(meet(X0,X1),X2),X1),meet(X2,X0))=meet(join(meet(join(X0,X1),X2),X1),join(X2,X0)))),
% 4.87/1.06 inference(cnf_transformation,[status(thm)],[f9])).
% 4.87/1.06 fof(f20,plain,(
% 4.87/1.06 ~join(a,meet(b,c))=meet(join(a,b),join(a,c))),
% 4.87/1.06 inference(cnf_transformation,[status(thm)],[f10])).
% 4.87/1.06 fof(f35,plain,(
% 4.87/1.06 ![X0,X1]: (join(X0,meet(X1,X0))=X0)),
% 4.87/1.06 inference(paramodulation,[status(thm)],[f15,f14])).
% 4.87/1.06 fof(f38,plain,(
% 4.87/1.06 ![X0,X1]: (join(join(X0,X1),X0)=join(X0,X1))),
% 4.87/1.06 inference(paramodulation,[status(thm)],[f13,f35])).
% 4.87/1.06 fof(f44,plain,(
% 4.87/1.06 ![X0,X1]: (join(X0,join(X1,X0))=join(X0,X1))),
% 4.87/1.06 inference(forward_demodulation,[status(thm)],[f18,f38])).
% 4.87/1.06 fof(f49,plain,(
% 4.87/1.06 ~join(a,meet(b,c))=meet(join(a,b),join(c,a))),
% 4.87/1.06 inference(paramodulation,[status(thm)],[f16,f20])).
% 4.87/1.06 fof(f51,plain,(
% 4.87/1.06 ![X0,X1]: (meet(X0,join(X1,X0))=X0)),
% 4.87/1.06 inference(paramodulation,[status(thm)],[f16,f13])).
% 4.87/1.06 fof(f57,plain,(
% 4.87/1.06 ![X0,X1]: (meet(meet(X0,X1),X0)=meet(X0,X1))),
% 4.87/1.06 inference(paramodulation,[status(thm)],[f14,f51])).
% 4.87/1.06 fof(f65,plain,(
% 4.87/1.06 ![X0,X1]: (meet(X0,meet(X1,X0))=meet(X0,X1))),
% 4.87/1.06 inference(forward_demodulation,[status(thm)],[f17,f57])).
% 4.87/1.06 fof(f70,plain,(
% 4.87/1.06 ![X0,X1]: (join(X0,join(X0,X1))=join(X0,X1))),
% 4.87/1.06 inference(paramodulation,[status(thm)],[f16,f44])).
% 4.87/1.06 fof(f73,plain,(
% 4.87/1.06 ![X0,X1]: (meet(join(X0,X1),join(X1,X0))=join(X0,X1))),
% 4.87/1.06 inference(paramodulation,[status(thm)],[f44,f51])).
% 4.87/1.06 fof(f80,plain,(
% 4.87/1.06 ![X0,X1,X2]: (meet(X0,X1)=meet(X0,meet(X1,join(meet(X0,X1),X2))))),
% 4.87/1.06 inference(paramodulation,[status(thm)],[f13,f17])).
% 4.87/1.06 fof(f81,plain,(
% 4.87/1.06 ![X0,X1,X2]: (meet(X0,meet(X1,X2))=meet(X1,meet(X2,X0)))),
% 4.87/1.06 inference(paramodulation,[status(thm)],[f15,f17])).
% 4.87/1.06 fof(f85,plain,(
% 4.87/1.06 ![X0,X1,X2]: (meet(X0,X1)=meet(X0,meet(join(X2,X0),X1)))),
% 4.87/1.06 inference(paramodulation,[status(thm)],[f51,f17])).
% 4.87/1.06 fof(f86,plain,(
% 4.87/1.06 ![X0,X1,X2]: (meet(X0,X1)=meet(X0,meet(join(X0,X2),X1)))),
% 4.87/1.06 inference(paramodulation,[status(thm)],[f13,f17])).
% 4.87/1.06 fof(f87,plain,(
% 4.87/1.06 ![X0,X1,X2]: (meet(meet(X0,X1),X2)=meet(X1,meet(X0,X2)))),
% 4.87/1.06 inference(paramodulation,[status(thm)],[f15,f17])).
% 4.87/1.06 fof(f89,plain,(
% 4.87/1.06 ![X0,X1]: (meet(X0,X1)=meet(X0,meet(X0,X1)))),
% 4.87/1.06 inference(paramodulation,[status(thm)],[f11,f17])).
% 4.87/1.06 fof(f92,plain,(
% 4.87/1.06 ![X0,X1,X2]: (join(X0,meet(X1,meet(X2,X0)))=X0)),
% 4.87/1.06 inference(paramodulation,[status(thm)],[f17,f35])).
% 4.87/1.06 fof(f95,plain,(
% 4.87/1.06 ![X0,X1,X2]: (join(meet(X0,X1),meet(X0,meet(X1,X2)))=meet(X0,X1))),
% 4.87/1.06 inference(paramodulation,[status(thm)],[f17,f14])).
% 4.87/1.06 fof(f103,plain,(
% 4.87/1.06 ![X0,X1,X2]: (join(X0,X1)=join(X0,join(X1,meet(join(X0,X1),X2))))),
% 4.87/1.06 inference(paramodulation,[status(thm)],[f14,f18])).
% 4.87/1.06 fof(f109,plain,(
% 4.87/1.06 ![X0,X1,X2]: (join(X0,X1)=join(X0,join(meet(X2,X0),X1)))),
% 4.87/1.06 inference(paramodulation,[status(thm)],[f35,f18])).
% 4.87/1.06 fof(f111,plain,(
% 4.87/1.06 ![X0,X1,X2]: (join(join(X0,X1),X2)=join(X1,join(X0,X2)))),
% 4.87/1.06 inference(paramodulation,[status(thm)],[f16,f18])).
% 4.87/1.06 fof(f118,plain,(
% 4.87/1.06 ![X0,X1,X2]: (meet(X0,join(X1,join(X2,X0)))=X0)),
% 4.87/1.06 inference(paramodulation,[status(thm)],[f18,f51])).
% 4.87/1.06 fof(f142,plain,(
% 4.87/1.06 ![X0,X1]: (join(meet(X0,X1),meet(X1,X0))=meet(X0,X1))),
% 4.87/1.06 inference(paramodulation,[status(thm)],[f65,f35])).
% 4.87/1.06 fof(f227,plain,(
% 4.87/1.06 ![X0,X1,X2]: (join(X0,meet(meet(X1,X0),X2))=X0)),
% 4.87/1.06 inference(paramodulation,[status(thm)],[f15,f92])).
% 4.87/1.06 fof(f234,plain,(
% 4.87/1.06 ![X0,X1,X2]: (join(join(X0,X1),meet(X2,X0))=join(X0,X1))),
% 4.87/1.06 inference(paramodulation,[status(thm)],[f13,f92])).
% 4.87/1.06 fof(f245,plain,(
% 4.87/1.06 ![X0,X1,X2]: (join(X0,meet(X1,meet(X0,X2)))=X0)),
% 4.87/1.06 inference(forward_demodulation,[status(thm)],[f17,f227])).
% 4.87/1.06 fof(f248,plain,(
% 4.87/1.06 ![X0,X1,X2]: (join(X0,join(X1,meet(X2,X0)))=join(X0,X1))),
% 4.87/1.06 inference(forward_demodulation,[status(thm)],[f18,f234])).
% 4.87/1.06 fof(f257,plain,(
% 4.87/1.06 ![X0,X1,X2]: (meet(X0,join(join(X1,X0),X2))=X0)),
% 4.87/1.06 inference(paramodulation,[status(thm)],[f16,f118])).
% 4.87/1.06 fof(f262,plain,(
% 4.87/1.06 ![X0,X1,X2]: (meet(join(X0,X1),join(X2,join(X1,X0)))=join(X0,X1))),
% 4.87/1.06 inference(paramodulation,[status(thm)],[f44,f118])).
% 4.87/1.06 fof(f277,plain,(
% 4.87/1.06 ![X0,X1,X2]: (meet(X0,join(X1,join(X0,X2)))=X0)),
% 4.87/1.06 inference(forward_demodulation,[status(thm)],[f18,f257])).
% 4.87/1.06 fof(f374,plain,(
% 4.87/1.06 ![X0,X1,X2]: (meet(join(meet(X0,meet(X1,X2)),X1),X1)=join(meet(X0,meet(X1,X2)),X1))),
% 4.87/1.06 inference(paramodulation,[status(thm)],[f245,f73])).
% 4.87/1.06 fof(f375,plain,(
% 4.87/1.06 ![X0,X1,X2]: (meet(join(meet(X0,meet(X1,X2)),X2),X2)=join(meet(X0,meet(X1,X2)),X2))),
% 4.87/1.06 inference(paramodulation,[status(thm)],[f92,f73])).
% 4.87/1.06 fof(f376,plain,(
% 4.87/1.06 ![X0,X1]: (meet(join(meet(X0,X1),X1),X1)=join(meet(X0,X1),X1))),
% 4.87/1.06 inference(paramodulation,[status(thm)],[f35,f73])).
% 4.87/1.06 fof(f452,plain,(
% 4.87/1.06 ![X0,X1,X2]: (join(meet(join(X0,X1),X2),meet(X1,X2))=meet(join(X0,X1),X2))),
% 4.87/1.06 inference(paramodulation,[status(thm)],[f85,f35])).
% 4.87/1.06 fof(f487,plain,(
% 4.87/1.06 ![X0,X1,X2]: (join(meet(X0,join(meet(X1,X0),X2)),meet(X2,X1))=meet(join(meet(join(X1,X0),X2),X0),join(X2,X1)))),
% 4.87/1.06 inference(paramodulation,[status(thm)],[f15,f19])).
% 4.87/1.06 fof(f503,plain,(
% 4.87/1.06 ![X0,X1,X2]: (join(meet(join(meet(X0,X1),X2),meet(X1,X0)),meet(X2,X0))=meet(join(meet(join(X0,meet(X1,X0)),X2),meet(X1,X0)),join(X2,X0)))),
% 4.87/1.06 inference(paramodulation,[status(thm)],[f65,f19])).
% 4.87/1.06 fof(f510,plain,(
% 4.87/1.06 ![X0,X1]: (join(meet(join(X0,X1),X0),meet(X1,X0))=meet(join(meet(join(X0,X0),X1),X0),join(X1,X0)))),
% 4.87/1.06 inference(paramodulation,[status(thm)],[f11,f19])).
% 4.87/1.06 fof(f514,plain,(
% 4.87/1.06 ![X0,X1,X2]: (join(meet(join(meet(meet(X0,X1),X2),X0),X2),meet(X0,X1))=meet(join(meet(join(meet(X0,X1),X2),X0),X2),join(X0,meet(X0,X1))))),
% 4.87/1.06 inference(paramodulation,[status(thm)],[f89,f19])).
% 4.87/1.06 fof(f515,plain,(
% 4.87/1.06 ![X0,X1,X2]: (join(meet(join(meet(meet(X0,X1),X2),X1),X2),meet(X1,X0))=meet(join(meet(join(meet(X0,X1),X2),X1),X2),join(X1,meet(X0,X1))))),
% 4.87/1.06 inference(paramodulation,[status(thm)],[f65,f19])).
% 4.87/1.06 fof(f518,plain,(
% 4.87/1.06 ![X0,X1,X2]: (join(meet(join(meet(join(X0,X1),X2),X1),X2),X1)=meet(join(meet(join(join(X0,X1),X2),X1),X2),join(X1,join(X0,X1))))),
% 4.87/1.06 inference(paramodulation,[status(thm)],[f51,f19])).
% 4.87/1.06 fof(f519,plain,(
% 4.87/1.06 ![X0,X1,X2]: (join(meet(join(meet(join(X0,X1),X2),X0),X2),X0)=meet(join(meet(join(join(X0,X1),X2),X0),X2),join(X0,join(X0,X1))))),
% 4.87/1.06 inference(paramodulation,[status(thm)],[f13,f19])).
% 4.87/1.06 fof(f571,plain,(
% 4.87/1.06 ![X0,X1,X2]: (join(meet(join(meet(X0,X1),X2),meet(X1,X0)),meet(X2,X0))=meet(join(meet(X0,X2),meet(X1,X0)),join(X2,X0)))),
% 4.87/1.06 inference(forward_demodulation,[status(thm)],[f35,f503])).
% 4.87/1.06 fof(f576,plain,(
% 4.87/1.06 ![X0,X1]: (meet(join(X0,X1),X0)=meet(join(meet(join(X0,X0),X1),X0),join(X1,X0)))),
% 4.87/1.06 inference(forward_demodulation,[status(thm)],[f452,f510])).
% 4.87/1.06 fof(f577,plain,(
% 4.87/1.06 ![X0,X1]: (meet(join(X0,X1),X0)=meet(join(meet(X0,X1),X0),join(X1,X0)))),
% 4.87/1.06 inference(forward_demodulation,[status(thm)],[f12,f576])).
% 4.87/1.06 fof(f583,plain,(
% 4.87/1.06 ![X0,X1,X2]: (join(meet(join(meet(X0,meet(X1,X2)),X0),X2),meet(X0,X1))=meet(join(meet(join(meet(X0,X1),X2),X0),X2),join(X0,meet(X0,X1))))),
% 4.87/1.06 inference(forward_demodulation,[status(thm)],[f17,f514])).
% 4.87/1.06 fof(f584,plain,(
% 4.87/1.06 ![X0,X1,X2]: (join(meet(join(meet(X0,meet(X1,X2)),X0),X2),meet(X0,X1))=meet(join(meet(join(meet(X0,X1),X2),X0),X2),X0))),
% 4.87/1.06 inference(forward_demodulation,[status(thm)],[f14,f583])).
% 4.87/1.06 fof(f585,plain,(
% 4.87/1.06 ![X0,X1,X2]: (join(meet(join(meet(X0,meet(X1,X2)),X1),X2),meet(X1,X0))=meet(join(meet(join(meet(X0,X1),X2),X1),X2),join(X1,meet(X0,X1))))),
% 4.87/1.06 inference(forward_demodulation,[status(thm)],[f17,f515])).
% 4.87/1.06 fof(f586,plain,(
% 4.87/1.06 ![X0,X1,X2]: (join(meet(join(meet(X0,meet(X1,X2)),X1),X2),meet(X1,X0))=meet(join(meet(join(meet(X0,X1),X2),X1),X2),X1))),
% 4.87/1.06 inference(forward_demodulation,[status(thm)],[f35,f585])).
% 4.87/1.06 fof(f593,plain,(
% 4.87/1.06 ![X0,X1,X2]: (join(meet(join(meet(join(X0,X1),X2),X1),X2),X1)=meet(join(meet(join(X0,join(X1,X2)),X1),X2),join(X1,join(X0,X1))))),
% 4.87/1.06 inference(forward_demodulation,[status(thm)],[f18,f518])).
% 4.87/1.06 fof(f594,plain,(
% 4.87/1.06 ![X0,X1,X2]: (join(meet(join(meet(join(X0,X1),X2),X1),X2),X1)=meet(join(meet(join(X0,join(X1,X2)),X1),X2),join(X1,X0)))),
% 4.87/1.06 inference(forward_demodulation,[status(thm)],[f44,f593])).
% 4.87/1.06 fof(f595,plain,(
% 4.87/1.06 ![X0,X1,X2]: (join(meet(join(meet(join(X0,X1),X2),X0),X2),X0)=meet(join(meet(join(X0,join(X1,X2)),X0),X2),join(X0,join(X0,X1))))),
% 4.87/1.06 inference(forward_demodulation,[status(thm)],[f18,f519])).
% 4.87/1.06 fof(f596,plain,(
% 4.87/1.06 ![X0,X1,X2]: (join(meet(join(meet(join(X0,X1),X2),X0),X2),X0)=meet(join(meet(join(X0,join(X1,X2)),X0),X2),join(X0,X1)))),
% 4.87/1.06 inference(forward_demodulation,[status(thm)],[f70,f595])).
% 4.87/1.06 fof(f617,plain,(
% 4.87/1.06 ~join(a,meet(b,c))=meet(join(c,a),join(a,b))),
% 4.87/1.06 inference(paramodulation,[status(thm)],[f15,f49])).
% 4.87/1.06 fof(f670,plain,(
% 4.87/1.06 ![X0,X1,X2]: (join(meet(X0,join(meet(X1,X0),X2)),meet(X1,X0))=meet(X0,join(meet(X1,X0),X2)))),
% 4.87/1.06 inference(paramodulation,[status(thm)],[f80,f35])).
% 4.87/1.06 fof(f764,plain,(
% 4.87/1.06 ![X0,X1,X2]: (meet(join(meet(X0,X1),X2),join(X1,X2))=join(meet(X0,X1),X2))),
% 4.87/1.06 inference(paramodulation,[status(thm)],[f109,f51])).
% 4.87/1.06 fof(f805,plain,(
% 4.87/1.06 ![X0,X1]: (meet(join(X0,X1),X0)=join(meet(X0,X1),X0))),
% 4.87/1.06 inference(backward_demodulation,[status(thm)],[f764,f577])).
% 4.87/1.06 fof(f807,plain,(
% 4.87/1.06 ![X0,X1,X2]: (join(meet(meet(join(X0,meet(X1,X2)),X0),X2),meet(X0,X1))=meet(join(meet(join(meet(X0,X1),X2),X0),X2),X0))),
% 4.87/1.06 inference(backward_demodulation,[status(thm)],[f805,f584])).
% 4.87/1.06 fof(f815,plain,(
% 4.87/1.06 ![X0,X1,X2]: (join(meet(join(X0,meet(X1,X2)),meet(X0,X2)),meet(X0,X1))=meet(join(meet(join(meet(X0,X1),X2),X0),X2),X0))),
% 4.87/1.06 inference(forward_demodulation,[status(thm)],[f17,f807])).
% 4.87/1.06 fof(f920,plain,(
% 4.87/1.06 ![X0,X1,X2]: (join(join(X0,X1),X2)=join(join(X1,X0),join(X0,X2)))),
% 4.87/1.06 inference(paramodulation,[status(thm)],[f44,f111])).
% 4.87/1.06 fof(f924,plain,(
% 4.87/1.06 ![X0,X1,X2]: (join(X0,X1)=join(meet(X0,X2),join(X0,X1)))),
% 4.87/1.06 inference(paramodulation,[status(thm)],[f14,f111])).
% 4.87/1.06 fof(f973,plain,(
% 4.87/1.06 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(join(X0,X1),join(X1,X2)))),
% 4.87/1.06 inference(forward_demodulation,[status(thm)],[f111,f920])).
% 4.87/1.06 fof(f974,plain,(
% 4.87/1.06 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(X1,join(X0,join(X1,X2))))),
% 4.87/1.06 inference(forward_demodulation,[status(thm)],[f111,f973])).
% 4.87/1.06 fof(f1114,plain,(
% 4.87/1.06 ![X0,X1,X2]: (meet(X0,X1)=meet(X1,meet(X0,join(meet(X0,X1),X2))))),
% 4.87/1.06 inference(paramodulation,[status(thm)],[f13,f87])).
% 4.87/1.06 fof(f1128,plain,(
% 4.87/1.06 ![X0,X1,X2]: (meet(X0,X1)=meet(join(X0,X2),meet(X0,X1)))),
% 4.87/1.06 inference(paramodulation,[status(thm)],[f13,f87])).
% 4.87/1.06 fof(f1187,plain,(
% 4.87/1.06 ![X0,X1,X2]: (join(meet(X0,X1),meet(X0,X2))=meet(join(meet(join(meet(X0,X2),X1),X0),X1),X0))),
% 4.87/1.06 inference(backward_demodulation,[status(thm)],[f1128,f815])).
% 4.87/1.06 fof(f1217,plain,(
% 4.87/1.06 ![X0,X1,X2]: (join(X0,meet(join(meet(join(X0,X1),X2),X1),join(X2,X0)))=join(X0,meet(join(meet(X0,X1),X2),X1)))),
% 4.87/1.06 inference(paramodulation,[status(thm)],[f19,f248])).
% 4.87/1.06 fof(f1220,plain,(
% 4.87/1.06 ![X0,X1,X2,X3]: (join(X0,join(X1,join(X2,meet(X3,X0))))=join(X0,join(X1,X2)))),
% 4.87/1.06 inference(paramodulation,[status(thm)],[f18,f248])).
% 4.87/1.06 fof(f1251,plain,(
% 4.87/1.06 ![X0,X1,X2]: (meet(meet(X0,X1),join(X1,X2))=meet(X0,X1))),
% 4.87/1.06 inference(paramodulation,[status(thm)],[f248,f118])).
% 4.87/1.06 fof(f1292,plain,(
% 4.87/1.06 ![X0,X1,X2]: (meet(X0,meet(X1,join(X0,X2)))=meet(X1,X0))),
% 4.87/1.06 inference(forward_demodulation,[status(thm)],[f87,f1251])).
% 4.87/1.06 fof(f1320,plain,(
% 4.87/1.06 ![X0,X1,X2]: (meet(X0,join(X1,X2))=meet(join(X1,X2),meet(join(X2,X1),X0)))),
% 4.87/1.06 inference(paramodulation,[status(thm)],[f73,f81])).
% 4.87/1.06 fof(f1335,plain,(
% 4.87/1.06 ![X0,X1]: (meet(X0,X1)=meet(X1,meet(X1,X0)))),
% 4.87/1.06 inference(paramodulation,[status(thm)],[f11,f81])).
% 4.87/1.06 fof(f1393,plain,(
% 4.87/1.06 ![X0,X1,X2,X3]: (meet(X0,meet(X1,X2))=meet(X0,meet(X2,meet(join(X3,X0),X1))))),
% 4.87/1.06 inference(paramodulation,[status(thm)],[f81,f85])).
% 4.87/1.06 fof(f1615,plain,(
% 4.87/1.06 ![X0,X1]: (meet(join(meet(X0,X0),X1),X0)=meet(X0,X0))),
% 4.87/1.06 inference(paramodulation,[status(thm)],[f80,f1335])).
% 4.87/1.06 fof(f1625,plain,(
% 4.87/1.06 ![X0,X1,X2]: (meet(meet(X0,join(meet(X1,X0),X2)),X1)=meet(X1,meet(X1,X0)))),
% 4.87/1.06 inference(paramodulation,[status(thm)],[f80,f1335])).
% 4.87/1.06 fof(f1631,plain,(
% 4.87/1.06 ![X0,X1,X2]: (meet(join(X0,join(X1,X2)),X1)=meet(X1,X1))),
% 4.87/1.06 inference(paramodulation,[status(thm)],[f277,f1335])).
% 4.87/1.06 fof(f1633,plain,(
% 4.87/1.06 ![X0,X1]: (meet(join(X0,X1),X1)=meet(X1,X1))),
% 4.87/1.06 inference(paramodulation,[status(thm)],[f51,f1335])).
% 4.87/1.06 fof(f1658,plain,(
% 4.87/1.06 ![X0,X1,X2]: (join(meet(join(meet(meet(X0,X1),X2),X0),X2),meet(X1,X0))=meet(join(meet(join(meet(X0,X1),X2),X0),X2),join(X0,meet(X0,X1))))),
% 4.87/1.06 inference(paramodulation,[status(thm)],[f1335,f19])).
% 4.87/1.06 fof(f1674,plain,(
% 4.87/1.06 ![X0,X1]: (meet(join(X0,X1),X0)=meet(X0,X0))),
% 4.87/1.06 inference(forward_demodulation,[status(thm)],[f11,f1615])).
% 4.87/1.06 fof(f1676,plain,(
% 4.87/1.06 ![X0,X1,X2]: (join(meet(join(meet(join(X0,X1),X2),X0),X2),X0)=meet(join(X0,X2),join(X0,X1)))),
% 4.87/1.06 inference(backward_demodulation,[status(thm)],[f1682,f596])).
% 4.87/1.06 fof(f1682,plain,(
% 4.87/1.06 ![X0,X1]: (meet(join(X0,X1),X0)=X0)),
% 4.87/1.06 inference(forward_demodulation,[status(thm)],[f11,f1674])).
% 4.87/1.06 fof(f1696,plain,(
% 4.87/1.06 ![X0,X1,X2]: (meet(join(meet(X0,X1),X2),meet(X1,X0))=meet(X0,meet(X0,X1)))),
% 4.87/1.06 inference(forward_demodulation,[status(thm)],[f87,f1625])).
% 4.87/1.06 fof(f1697,plain,(
% 4.87/1.06 ![X0,X1,X2]: (join(meet(X0,X1),meet(X2,X1))=meet(join(meet(X1,X2),meet(X0,X1)),join(X2,X1)))),
% 4.87/1.06 inference(backward_demodulation,[status(thm)],[f1698,f571])).
% 4.87/1.06 fof(f1698,plain,(
% 4.87/1.06 ![X0,X1,X2]: (meet(join(meet(X0,X1),X2),meet(X1,X0))=meet(X1,X0))),
% 4.87/1.06 inference(forward_demodulation,[status(thm)],[f1335,f1696])).
% 4.87/1.06 fof(f1709,plain,(
% 4.87/1.06 ![X0,X1,X2]: (join(meet(join(meet(join(X0,X1),X2),X1),X2),X1)=meet(join(X1,X2),join(X1,X0)))),
% 4.87/1.06 inference(backward_demodulation,[status(thm)],[f1710,f594])).
% 4.87/1.06 fof(f1710,plain,(
% 4.87/1.06 ![X0,X1,X2]: (meet(join(X0,join(X1,X2)),X1)=X1)),
% 4.87/1.06 inference(forward_demodulation,[status(thm)],[f11,f1631])).
% 4.87/1.06 fof(f1713,plain,(
% 4.87/1.06 ![X0,X1,X2]: (X0=join(meet(X1,meet(X2,X0)),X0))),
% 4.87/1.06 inference(backward_demodulation,[status(thm)],[f1718,f375])).
% 4.87/1.06 fof(f1714,plain,(
% 4.87/1.06 ![X0,X1,X2]: (X0=join(meet(X1,meet(X0,X2)),X0))),
% 4.87/1.06 inference(backward_demodulation,[status(thm)],[f1718,f374])).
% 4.87/1.06 fof(f1715,plain,(
% 4.87/1.06 ![X0,X1]: (X0=join(meet(X1,X0),X0))),
% 4.87/1.06 inference(backward_demodulation,[status(thm)],[f1718,f376])).
% 4.87/1.06 fof(f1718,plain,(
% 4.87/1.06 ![X0,X1]: (meet(join(X0,X1),X1)=X1)),
% 4.87/1.06 inference(forward_demodulation,[status(thm)],[f11,f1633])).
% 4.87/1.06 fof(f1745,plain,(
% 4.87/1.06 ![X0,X1,X2]: (join(meet(join(meet(X0,meet(X1,X2)),X1),X2),meet(X0,X1))=meet(join(meet(join(meet(X1,X0),X2),X1),X2),join(X1,meet(X1,X0))))),
% 4.87/1.06 inference(forward_demodulation,[status(thm)],[f87,f1658])).
% 4.87/1.06 fof(f1746,plain,(
% 4.87/1.06 ![X0,X1,X2]: (join(meet(join(meet(X0,meet(X1,X2)),X1),X2),meet(X0,X1))=meet(join(meet(join(meet(X1,X0),X2),X1),X2),X1))),
% 4.87/1.06 inference(forward_demodulation,[status(thm)],[f14,f1745])).
% 4.87/1.06 fof(f1747,plain,(
% 4.87/1.06 ![X0,X1,X2]: (join(meet(join(meet(X0,meet(X1,X2)),X1),X2),meet(X0,X1))=join(meet(X1,X2),meet(X1,X0)))),
% 4.87/1.06 inference(forward_demodulation,[status(thm)],[f1187,f1746])).
% 4.87/1.06 fof(f1761,plain,(
% 4.87/1.06 ![X0,X1,X2]: (join(meet(X0,X1),meet(X2,X0))=join(meet(X0,X1),meet(X0,X2)))),
% 4.87/1.06 inference(backward_demodulation,[status(thm)],[f1714,f1747])).
% 4.87/1.06 fof(f1763,plain,(
% 4.87/1.06 ![X0,X1,X2]: (join(meet(X0,X1),meet(X0,X2))=meet(join(meet(join(meet(X2,X0),X1),X0),X1),X0))),
% 4.87/1.06 inference(backward_demodulation,[status(thm)],[f1714,f586])).
% 4.87/1.06 fof(f1831,plain,(
% 4.87/1.06 ![X0,X1]: (join(X0,X1)=join(join(X1,X0),join(X0,X1)))),
% 4.87/1.06 inference(paramodulation,[status(thm)],[f73,f1715])).
% 4.87/1.06 fof(f1836,plain,(
% 4.87/1.06 ![X0,X1,X2]: (meet(X0,join(meet(X1,X0),X2))=join(meet(X1,X0),meet(X0,join(meet(X1,X0),X2))))),
% 4.87/1.06 inference(paramodulation,[status(thm)],[f80,f1715])).
% 4.87/1.06 fof(f1874,plain,(
% 4.87/1.06 ![X0,X1]: (join(X0,X1)=join(X0,join(X1,join(X0,X1))))),
% 4.87/1.06 inference(forward_demodulation,[status(thm)],[f111,f1831])).
% 4.87/1.06 fof(f1875,plain,(
% 4.87/1.06 ![X0,X1]: (join(X0,X1)=join(X1,join(X0,X1)))),
% 4.87/1.06 inference(forward_demodulation,[status(thm)],[f974,f1874])).
% 4.87/1.06 fof(f1929,plain,(
% 4.87/1.06 ![X0,X1,X2]: (join(meet(join(meet(X0,X1),join(X0,X2)),X1),X0)=meet(join(meet(join(X0,X1),join(X0,X2)),X1),join(join(X0,X2),X0)))),
% 4.87/1.06 inference(paramodulation,[status(thm)],[f1682,f19])).
% 4.87/1.06 fof(f1953,plain,(
% 4.87/1.06 ![X0,X1,X2]: (join(meet(join(X0,X1),X2),X0)=meet(join(meet(join(X0,X2),join(X0,X1)),X2),join(join(X0,X1),X0)))),
% 4.87/1.06 inference(forward_demodulation,[status(thm)],[f924,f1929])).
% 4.87/1.06 fof(f1954,plain,(
% 4.87/1.06 ![X0,X1,X2]: (join(meet(join(X0,X1),X2),X0)=meet(join(meet(join(X0,X2),join(X0,X1)),X2),join(X1,join(X0,X0))))),
% 4.87/1.06 inference(forward_demodulation,[status(thm)],[f111,f1953])).
% 4.87/1.06 fof(f1955,plain,(
% 4.87/1.06 ![X0,X1,X2]: (join(meet(join(X0,X1),X2),X0)=meet(join(meet(join(X0,X2),join(X0,X1)),X2),join(X1,X0)))),
% 4.87/1.06 inference(forward_demodulation,[status(thm)],[f12,f1954])).
% 4.87/1.06 fof(f2011,plain,(
% 4.87/1.06 ![X0,X1,X2]: (join(meet(join(X0,X1),X0),meet(X1,join(X2,X0)))=meet(join(meet(join(join(X2,X0),X0),X1),X0),join(X1,join(X2,X0))))),
% 4.87/1.06 inference(paramodulation,[status(thm)],[f1718,f19])).
% 4.87/1.06 fof(f2035,plain,(
% 4.87/1.06 ![X0,X1,X2]: (join(X0,meet(X1,join(X2,X0)))=meet(join(meet(join(join(X2,X0),X0),X1),X0),join(X1,join(X2,X0))))),
% 4.87/1.06 inference(forward_demodulation,[status(thm)],[f1682,f2011])).
% 4.87/1.06 fof(f2036,plain,(
% 4.87/1.06 ![X0,X1,X2]: (join(X0,meet(X1,join(X2,X0)))=meet(join(meet(join(X0,join(X2,X0)),X1),X0),join(X1,join(X2,X0))))),
% 4.87/1.06 inference(forward_demodulation,[status(thm)],[f111,f2035])).
% 4.87/1.06 fof(f2037,plain,(
% 4.87/1.06 ![X0,X1,X2]: (join(X0,meet(X1,join(X2,X0)))=meet(join(meet(join(X0,X2),X1),X0),join(X1,join(X2,X0))))),
% 4.87/1.06 inference(forward_demodulation,[status(thm)],[f44,f2036])).
% 4.87/1.06 fof(f2085,plain,(
% 4.87/1.06 ![X0,X1,X2]: (join(meet(X0,meet(X1,X0)),meet(X0,X2))=meet(join(meet(join(X2,meet(X1,X0)),X0),meet(X1,X0)),join(X0,X2)))),
% 4.87/1.06 inference(paramodulation,[status(thm)],[f1713,f19])).
% 4.87/1.06 fof(f2118,plain,(
% 4.87/1.06 ![X0,X1,X2]: (join(meet(X0,X1),meet(X0,X2))=meet(join(meet(join(X2,meet(X1,X0)),X0),meet(X1,X0)),join(X0,X2)))),
% 4.87/1.07 inference(forward_demodulation,[status(thm)],[f65,f2085])).
% 4.87/1.07 fof(f2154,plain,(
% 4.87/1.07 ![X0,X1]: (join(X0,X1)=join(X1,join(X1,X0)))),
% 4.87/1.07 inference(paramodulation,[status(thm)],[f16,f1875])).
% 4.87/1.07 fof(f2248,plain,(
% 4.87/1.07 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(join(X1,X2),join(X1,join(X2,X0))))),
% 4.87/1.07 inference(paramodulation,[status(thm)],[f18,f2154])).
% 4.87/1.07 fof(f2306,plain,(
% 4.87/1.07 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(X2,join(X1,join(X1,join(X2,X0)))))),
% 4.87/1.07 inference(forward_demodulation,[status(thm)],[f111,f2248])).
% 4.87/1.07 fof(f2307,plain,(
% 4.87/1.07 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(X2,join(join(X2,X0),X1)))),
% 4.87/1.07 inference(forward_demodulation,[status(thm)],[f2154,f2306])).
% 4.87/1.07 fof(f2308,plain,(
% 4.87/1.07 ![X0,X1,X2]: (join(X0,join(X1,X2))=join(X2,join(X0,join(X2,X1))))),
% 4.87/1.07 inference(forward_demodulation,[status(thm)],[f111,f2307])).
% 4.87/1.07 fof(f2400,plain,(
% 4.87/1.07 ![X0,X1,X2]: (join(meet(X0,meet(X0,X1)),meet(X0,X2))=meet(join(meet(join(X2,meet(X0,X1)),X0),meet(X0,X1)),join(X0,X2)))),
% 4.87/1.07 inference(paramodulation,[status(thm)],[f1714,f19])).
% 4.87/1.07 fof(f2441,plain,(
% 4.87/1.07 ![X0,X1,X2]: (join(meet(X0,X1),meet(X1,X2))=meet(join(meet(join(X2,meet(X1,X0)),X1),meet(X1,X0)),join(X1,X2)))),
% 4.87/1.07 inference(forward_demodulation,[status(thm)],[f1335,f2400])).
% 4.87/1.07 fof(f2483,plain,(
% 4.87/1.07 ![X0,X1,X2]: (join(meet(join(X0,meet(X1,X2)),X1),meet(X1,X2))=meet(join(X0,meet(X1,X2)),X1))),
% 4.87/1.07 inference(paramodulation,[status(thm)],[f1718,f95])).
% 4.87/1.07 fof(f2499,plain,(
% 4.87/1.07 ![X0,X1,X2]: (join(meet(X0,join(X1,X2)),meet(X0,X2))=meet(X0,join(X1,X2)))),
% 4.87/1.07 inference(paramodulation,[status(thm)],[f1718,f95])).
% 4.87/1.07 fof(f2500,plain,(
% 4.87/1.07 ![X0,X1,X2]: (join(meet(X0,join(X1,X2)),meet(X0,X1))=meet(X0,join(X1,X2)))),
% 4.87/1.07 inference(paramodulation,[status(thm)],[f1682,f95])).
% 4.87/1.07 fof(f2568,plain,(
% 4.87/1.07 ![X0,X1,X2]: (join(meet(X0,X1),meet(X1,X2))=meet(meet(join(X2,meet(X1,X0)),X1),join(X1,X2)))),
% 4.87/1.07 inference(backward_demodulation,[status(thm)],[f2483,f2441])).
% 4.87/1.07 fof(f2630,plain,(
% 4.87/1.07 ![X0,X1,X2]: (join(meet(X0,X1),meet(X1,X2))=meet(X1,meet(join(X2,meet(X1,X0)),join(X1,X2))))),
% 4.87/1.07 inference(forward_demodulation,[status(thm)],[f87,f2568])).
% 4.87/1.07 fof(f2634,plain,(
% 4.87/1.07 ![X0,X1,X2]: (meet(X0,join(meet(X1,X0),X2))=meet(join(join(meet(X1,X0),X2),meet(X0,X1)),X0))),
% 4.87/1.07 inference(backward_demodulation,[status(thm)],[f2639,f1836])).
% 4.87/1.07 fof(f2639,plain,(
% 4.87/1.07 ![X0,X1,X2]: (join(meet(X0,X1),meet(X1,X2))=meet(join(X2,meet(X1,X0)),X1))),
% 4.87/1.07 inference(forward_demodulation,[status(thm)],[f1292,f2630])).
% 4.87/1.07 fof(f2640,plain,(
% 4.87/1.07 ![X0,X1,X2]: (meet(X0,join(meet(X1,X0),X2))=meet(join(X2,join(meet(X1,X0),meet(X0,X1))),X0))),
% 4.87/1.07 inference(forward_demodulation,[status(thm)],[f111,f2634])).
% 4.87/1.07 fof(f2643,plain,(
% 4.87/1.07 ![X0,X1,X2]: (join(meet(X0,X1),meet(X0,X2))=meet(join(meet(X0,join(meet(X1,X0),X2)),meet(X1,X0)),join(X0,X2)))),
% 4.87/1.07 inference(backward_demodulation,[status(thm)],[f2645,f2118])).
% 4.87/1.07 fof(f2645,plain,(
% 4.87/1.07 ![X0,X1,X2]: (meet(X0,join(meet(X1,X0),X2))=meet(join(X2,meet(X1,X0)),X0))),
% 4.87/1.07 inference(forward_demodulation,[status(thm)],[f142,f2640])).
% 4.87/1.07 fof(f2649,plain,(
% 4.87/1.07 ![X0,X1,X2]: (join(meet(X0,X1),meet(X0,X2))=meet(meet(X0,join(meet(X1,X0),X2)),join(X0,X2)))),
% 4.87/1.07 inference(forward_demodulation,[status(thm)],[f670,f2643])).
% 4.87/1.07 fof(f2650,plain,(
% 4.87/1.07 ![X0,X1,X2]: (join(meet(X0,X1),meet(X0,X2))=meet(join(meet(X1,X0),X2),meet(X0,join(X0,X2))))),
% 4.87/1.07 inference(forward_demodulation,[status(thm)],[f87,f2649])).
% 4.87/1.07 fof(f2652,plain,(
% 4.87/1.07 ![X0,X1,X2]: (meet(join(meet(join(X0,X1),X2),X0),X2)=meet(X2,join(X0,X1)))),
% 4.87/1.07 inference(backward_demodulation,[status(thm)],[f2666,f2500])).
% 4.87/1.07 fof(f2653,plain,(
% 4.87/1.07 ![X0,X1,X2]: (meet(join(meet(join(X0,X1),X2),X1),X2)=meet(X2,join(X0,X1)))),
% 4.87/1.07 inference(backward_demodulation,[status(thm)],[f2666,f2499])).
% 4.87/1.07 fof(f2662,plain,(
% 4.87/1.07 ![X0,X1,X2]: (meet(join(meet(X0,X1),X2),X1)=meet(join(meet(join(meet(X2,X1),X0),X1),X0),X1))),
% 4.87/1.07 inference(backward_demodulation,[status(thm)],[f2666,f1763])).
% 4.87/1.07 fof(f2663,plain,(
% 4.87/1.07 ![X0,X1,X2]: (join(meet(X0,X1),meet(X2,X0))=meet(join(meet(X1,X0),X2),X0))),
% 4.87/1.07 inference(backward_demodulation,[status(thm)],[f2666,f1761])).
% 4.87/1.07 fof(f2666,plain,(
% 4.87/1.07 ![X0,X1,X2]: (join(meet(X0,X1),meet(X0,X2))=meet(join(meet(X1,X0),X2),X0))),
% 4.87/1.07 inference(forward_demodulation,[status(thm)],[f13,f2650])).
% 4.87/1.07 fof(f2670,plain,(
% 4.87/1.07 ![X0,X1,X2]: (join(meet(X0,join(X1,X2)),X1)=meet(join(X1,X0),join(X1,X2)))),
% 4.87/1.07 inference(backward_demodulation,[status(thm)],[f2652,f1676])).
% 4.87/1.07 fof(f2671,plain,(
% 4.87/1.07 ![X0,X1,X2]: (join(meet(X0,join(X1,X2)),X2)=meet(join(X2,X0),join(X2,X1)))),
% 4.87/1.07 inference(backward_demodulation,[status(thm)],[f2653,f1709])).
% 4.87/1.07 fof(f2683,plain,(
% 4.87/1.07 ![X0,X1,X2]: (join(meet(X0,join(meet(X1,X0),X2)),meet(X1,X2))=meet(join(meet(join(X2,X0),X1),X0),join(X1,X2)))),
% 4.87/1.07 inference(backward_demodulation,[status(thm)],[f2709,f19])).
% 4.87/1.07 fof(f2695,plain,(
% 4.87/1.07 ![X0,X1,X2]: (join(meet(X0,X1),meet(X0,X2))=meet(X0,join(meet(X2,X0),X1)))),
% 4.87/1.07 inference(backward_demodulation,[status(thm)],[f2709,f2666])).
% 4.87/1.07 fof(f2701,plain,(
% 4.87/1.07 ![X0,X1,X2]: (join(X0,meet(join(meet(join(X0,X1),X2),X1),join(X2,X0)))=join(X0,meet(X1,join(meet(X2,X1),X0))))),
% 4.87/1.07 inference(backward_demodulation,[status(thm)],[f2709,f1217])).
% 4.87/1.07 fof(f2709,plain,(
% 4.87/1.07 ![X0,X1,X2]: (meet(join(meet(X0,X1),X2),X1)=meet(X1,join(meet(X2,X1),X0)))),
% 4.87/1.07 inference(forward_demodulation,[status(thm)],[f2653,f2662])).
% 4.87/1.07 fof(f2715,plain,(
% 4.87/1.07 ![X0,X1,X2]: (join(meet(X0,X1),meet(X2,X1))=meet(meet(X1,join(meet(X0,X1),X2)),join(X2,X1)))),
% 4.87/1.07 inference(backward_demodulation,[status(thm)],[f2716,f1697])).
% 4.87/1.07 fof(f2716,plain,(
% 4.87/1.07 ![X0,X1,X2]: (join(meet(X0,X1),meet(X2,X0))=meet(X0,join(meet(X2,X0),X1)))),
% 4.87/1.07 inference(forward_demodulation,[status(thm)],[f2709,f2663])).
% 4.87/1.07 fof(f2737,plain,(
% 4.87/1.07 ![X0,X1,X2]: (join(meet(X0,X1),meet(X2,X1))=meet(join(meet(X0,X1),X2),meet(X1,join(X2,X1))))),
% 4.87/1.07 inference(forward_demodulation,[status(thm)],[f87,f2715])).
% 4.87/1.07 fof(f2738,plain,(
% 4.87/1.07 ![X0,X1,X2]: (join(meet(X0,X1),meet(X2,X1))=meet(join(meet(X0,X1),X2),X1))),
% 4.87/1.07 inference(forward_demodulation,[status(thm)],[f51,f2737])).
% 4.87/1.07 fof(f2744,plain,(
% 4.87/1.07 ![X0,X1,X2]: (join(meet(X0,X1),meet(X2,X1))=meet(X1,join(meet(X2,X1),X0)))),
% 4.87/1.07 inference(forward_demodulation,[status(thm)],[f2709,f2738])).
% 4.87/1.07 fof(f2757,plain,(
% 4.87/1.07 ![X0,X1,X2]: (join(meet(meet(X0,X1),X0),meet(X2,X0))=meet(join(meet(join(X0,meet(X0,X1)),X2),meet(X0,X1)),join(X2,X0)))),
% 4.87/1.07 inference(paramodulation,[status(thm)],[f1714,f2683])).
% 4.87/1.07 fof(f2777,plain,(
% 4.87/1.07 ![X0,X1,X2]: (join(meet(X0,join(X0,X1)),meet(join(X0,X2),X1))=meet(join(meet(join(X1,X0),join(X0,X2)),X0),join(join(X0,X2),X1)))),
% 4.87/1.07 inference(paramodulation,[status(thm)],[f1682,f2683])).
% 4.87/1.07 fof(f2786,plain,(
% 4.87/1.07 ![X0,X1,X2]: (join(meet(meet(X0,X1),join(meet(X0,X1),X2)),meet(X0,X2))=meet(join(meet(join(X2,meet(X0,X1)),X0),meet(X0,X1)),join(X0,X2)))),
% 4.87/1.07 inference(paramodulation,[status(thm)],[f89,f2683])).
% 4.87/1.07 fof(f2797,plain,(
% 4.87/1.07 ![X0,X1,X2]: (join(meet(X0,join(meet(join(X1,X2),X0),X1)),X1)=meet(join(meet(join(X1,X0),join(X1,X2)),X0),join(join(X1,X2),X1)))),
% 4.87/1.07 inference(paramodulation,[status(thm)],[f1682,f2683])).
% 4.87/1.07 fof(f2817,plain,(
% 4.87/1.07 ![X0,X1,X2]: (join(join(meet(X0,X1),X2),meet(X0,X2))=join(join(meet(X0,X1),X2),meet(join(meet(join(X2,X1),X0),X1),join(X0,X2))))),
% 4.87/1.07 inference(paramodulation,[status(thm)],[f2683,f109])).
% 4.87/1.07 fof(f2824,plain,(
% 4.87/1.07 ![X0,X1,X2,X3]: (meet(meet(X0,join(meet(X1,X0),X2)),X3)=meet(meet(X0,join(meet(X1,X0),X2)),meet(meet(join(meet(join(X2,X0),X1),X0),join(X1,X2)),X3)))),
% 4.87/1.07 inference(paramodulation,[status(thm)],[f2683,f86])).
% 4.87/1.07 fof(f2837,plain,(
% 4.87/1.07 ![X0,X1,X2]: (meet(meet(X0,join(meet(X1,X0),X2)),meet(join(meet(join(X2,X0),X1),X0),join(X1,X2)))=meet(X0,join(meet(X1,X0),X2)))),
% 4.87/1.07 inference(paramodulation,[status(thm)],[f2683,f13])).
% 4.87/1.07 fof(f2852,plain,(
% 4.87/1.07 ![X0,X1,X2]: (meet(X0,join(meet(X1,X0),meet(X0,X2)))=meet(join(meet(join(X0,meet(X0,X2)),X1),meet(X0,X2)),join(X1,X0)))),
% 4.87/1.07 inference(forward_demodulation,[status(thm)],[f2744,f2757])).
% 4.87/1.07 fof(f2853,plain,(
% 4.87/1.07 ![X0,X1,X2]: (meet(X0,meet(join(X1,meet(X0,X2)),X0))=meet(join(meet(join(X0,meet(X0,X1)),X2),meet(X0,X1)),join(X2,X0)))),
% 4.87/1.07 inference(forward_demodulation,[status(thm)],[f2639,f2852])).
% 4.87/1.07 fof(f2854,plain,(
% 4.87/1.07 ![X0,X1,X2]: (meet(X0,join(X1,meet(X0,X2)))=meet(join(meet(join(X0,meet(X0,X1)),X2),meet(X0,X1)),join(X2,X0)))),
% 4.87/1.07 inference(forward_demodulation,[status(thm)],[f65,f2853])).
% 4.87/1.07 fof(f2855,plain,(
% 4.87/1.07 ![X0,X1,X2]: (meet(X0,join(X1,meet(X0,X2)))=meet(join(meet(X0,X2),meet(X0,X1)),join(X2,X0)))),
% 4.87/1.07 inference(forward_demodulation,[status(thm)],[f14,f2854])).
% 4.87/1.07 fof(f2856,plain,(
% 4.87/1.07 ![X0,X1,X2]: (meet(X0,join(X1,meet(X0,X2)))=meet(meet(X0,join(meet(X1,X0),X2)),join(X2,X0)))),
% 4.87/1.07 inference(forward_demodulation,[status(thm)],[f2695,f2855])).
% 4.87/1.07 fof(f2857,plain,(
% 4.87/1.07 ![X0,X1,X2]: (meet(X0,join(X1,meet(X0,X2)))=meet(join(meet(X1,X0),X2),meet(X0,join(X2,X0))))),
% 4.87/1.07 inference(forward_demodulation,[status(thm)],[f87,f2856])).
% 4.87/1.07 fof(f2858,plain,(
% 4.87/1.07 ![X0,X1,X2]: (meet(X0,join(X1,meet(X0,X2)))=meet(join(meet(X1,X0),X2),X0))),
% 4.87/1.07 inference(forward_demodulation,[status(thm)],[f51,f2857])).
% 4.87/1.07 fof(f2952,plain,(
% 4.87/1.07 ![X0,X1,X2]: (join(X0,meet(join(X0,X1),X2))=meet(join(meet(join(X2,X0),join(X0,X1)),X0),join(join(X0,X1),X2)))),
% 4.87/1.07 inference(forward_demodulation,[status(thm)],[f13,f2777])).
% 4.87/1.07 fof(f2953,plain,(
% 4.87/1.07 ![X0,X1,X2]: (join(X0,meet(join(X0,X1),X2))=meet(meet(join(X0,join(X2,X0)),join(X0,X1)),join(join(X0,X1),X2)))),
% 4.87/1.07 inference(forward_demodulation,[status(thm)],[f2670,f2952])).
% 4.87/1.07 fof(f2954,plain,(
% 4.87/1.07 ![X0,X1,X2]: (join(X0,meet(join(X0,X1),X2))=meet(join(X0,X1),meet(join(X0,join(X2,X0)),join(join(X0,X1),X2))))),
% 4.87/1.07 inference(forward_demodulation,[status(thm)],[f87,f2953])).
% 4.87/1.07 fof(f2955,plain,(
% 4.87/1.07 ![X0,X1,X2]: (join(X0,meet(join(X0,X1),X2))=meet(join(X0,join(X2,X0)),join(X0,X1)))),
% 4.87/1.07 inference(forward_demodulation,[status(thm)],[f1292,f2954])).
% 4.87/1.07 fof(f2959,plain,(
% 4.87/1.07 ![X0,X1,X2]: (join(X0,meet(join(X0,X1),X2))=meet(join(X2,X0),join(X0,X1)))),
% 4.87/1.07 inference(forward_demodulation,[status(thm)],[f1875,f2955])).
% 4.87/1.07 fof(f2973,plain,(
% 4.87/1.07 ![X0,X1,X2]: (join(meet(X0,meet(X1,join(meet(X1,X0),X2))),meet(X1,X2))=meet(join(meet(join(X2,meet(X1,X0)),X1),meet(X1,X0)),join(X1,X2)))),
% 4.87/1.07 inference(forward_demodulation,[status(thm)],[f87,f2786])).
% 4.87/1.07 fof(f2974,plain,(
% 4.87/1.07 ![X0,X1,X2]: (join(meet(X0,X1),meet(X0,X2))=meet(join(meet(join(X2,meet(X0,X1)),X0),meet(X0,X1)),join(X0,X2)))),
% 4.87/1.07 inference(forward_demodulation,[status(thm)],[f1114,f2973])).
% 4.87/1.07 fof(f2975,plain,(
% 4.87/1.07 ![X0,X1,X2]: (meet(X0,join(meet(X1,X0),X2))=meet(join(meet(join(X1,meet(X0,X2)),X0),meet(X0,X2)),join(X0,X1)))),
% 4.87/1.07 inference(forward_demodulation,[status(thm)],[f2695,f2974])).
% 4.87/1.07 fof(f2976,plain,(
% 4.87/1.07 ![X0,X1,X2]: (meet(X0,join(meet(X1,X0),X2))=meet(meet(join(X2,meet(X0,join(X1,meet(X0,X2)))),X0),join(X0,X1)))),
% 4.87/1.07 inference(forward_demodulation,[status(thm)],[f2639,f2975])).
% 4.87/1.07 fof(f2977,plain,(
% 4.87/1.07 ![X0,X1,X2]: (meet(X0,join(meet(X1,X0),X2))=meet(X0,meet(join(X2,meet(X0,join(X1,meet(X0,X2)))),join(X0,X1))))),
% 4.87/1.07 inference(forward_demodulation,[status(thm)],[f87,f2976])).
% 4.87/1.07 fof(f2979,plain,(
% 4.87/1.07 ![X0,X1,X2]: (meet(X0,join(meet(X1,X0),X2))=meet(join(X2,meet(X0,join(X1,meet(X0,X2)))),X0))),
% 4.87/1.07 inference(forward_demodulation,[status(thm)],[f1292,f2977])).
% 4.87/1.07 fof(f3007,plain,(
% 4.87/1.07 ![X0,X1,X2]: (meet(join(X0,X1),join(X0,meet(join(X0,X2),X1)))=meet(join(meet(join(X0,X1),join(X0,X2)),X1),join(join(X0,X2),X0)))),
% 4.87/1.07 inference(forward_demodulation,[status(thm)],[f2671,f2797])).
% 4.87/1.07 fof(f3008,plain,(
% 4.87/1.07 ![X0,X1,X2]: (meet(join(X0,X1),meet(join(X1,X0),join(X0,X2)))=meet(join(meet(join(X0,X1),join(X0,X2)),X1),join(join(X0,X2),X0)))),
% 4.87/1.07 inference(forward_demodulation,[status(thm)],[f2959,f3007])).
% 4.87/1.07 fof(f3009,plain,(
% 4.87/1.07 ![X0,X1,X2]: (meet(join(X0,X1),join(X0,X2))=meet(join(meet(join(X0,X2),join(X0,X1)),X2),join(join(X0,X1),X0)))),
% 4.87/1.07 inference(forward_demodulation,[status(thm)],[f1320,f3008])).
% 4.87/1.07 fof(f3010,plain,(
% 4.87/1.07 ![X0,X1,X2]: (meet(join(X0,X1),join(X0,X2))=meet(join(meet(join(X0,X2),join(X0,X1)),X2),join(X1,join(X0,X0))))),
% 4.87/1.07 inference(forward_demodulation,[status(thm)],[f111,f3009])).
% 4.87/1.07 fof(f3011,plain,(
% 4.87/1.07 ![X0,X1,X2]: (join(meet(join(X0,X1),X2),X0)=meet(join(X0,X1),join(X0,X2)))),
% 4.87/1.07 inference(backward_demodulation,[status(thm)],[f3012,f1955])).
% 4.87/1.07 fof(f3012,plain,(
% 4.87/1.07 ![X0,X1,X2]: (meet(join(X0,X1),join(X0,X2))=meet(join(meet(join(X0,X2),join(X0,X1)),X2),join(X1,X0)))),
% 4.87/1.07 inference(forward_demodulation,[status(thm)],[f12,f3010])).
% 4.87/1.07 fof(f3065,plain,(
% 4.87/1.07 ![X0,X1,X2]: (join(X0,join(meet(X1,X2),meet(X1,X0)))=join(join(meet(X1,X2),X0),meet(join(meet(join(X0,X2),X1),X2),join(X1,X0))))),
% 4.87/1.07 inference(forward_demodulation,[status(thm)],[f111,f2817])).
% 4.87/1.07 fof(f3066,plain,(
% 4.87/1.07 ![X0,X1,X2]: (join(X0,meet(X1,X2))=join(join(meet(X1,X2),X0),meet(join(meet(join(X0,X2),X1),X2),join(X1,X0))))),
% 4.87/1.07 inference(forward_demodulation,[status(thm)],[f248,f3065])).
% 4.87/1.07 fof(f3067,plain,(
% 4.87/1.07 ![X0,X1,X2]: (join(X0,meet(X1,X2))=join(X0,join(meet(X1,X2),meet(join(meet(join(X0,X2),X1),X2),join(X1,X0)))))),
% 4.87/1.07 inference(forward_demodulation,[status(thm)],[f111,f3066])).
% 4.87/1.07 fof(f3075,plain,(
% 4.87/1.07 ![X0,X1,X2,X3]: (meet(join(meet(X0,X1),X2),meet(X1,X3))=meet(meet(X1,join(meet(X0,X1),X2)),meet(meet(join(meet(join(X2,X1),X0),X1),join(X0,X2)),X3)))),
% 4.87/1.07 inference(forward_demodulation,[status(thm)],[f87,f2824])).
% 4.87/1.07 fof(f3076,plain,(
% 4.87/1.07 ![X0,X1,X2,X3]: (meet(join(meet(X0,X1),X2),meet(X1,X3))=meet(join(meet(X0,X1),X2),meet(X1,meet(meet(join(meet(join(X2,X1),X0),X1),join(X0,X2)),X3))))),
% 4.87/1.07 inference(forward_demodulation,[status(thm)],[f87,f3075])).
% 4.87/1.07 fof(f3077,plain,(
% 4.87/1.07 ![X0,X1,X2,X3]: (meet(join(meet(X0,X1),X2),meet(X1,X3))=meet(join(meet(X0,X1),X2),meet(X1,meet(join(X0,X2),meet(join(meet(join(X2,X1),X0),X1),X3)))))),
% 4.87/1.07 inference(forward_demodulation,[status(thm)],[f87,f3076])).
% 4.87/1.07 fof(f3078,plain,(
% 4.87/1.07 ![X0,X1,X2,X3]: (meet(join(meet(X0,X1),X2),meet(X1,X3))=meet(join(meet(X0,X1),X2),meet(X1,meet(X3,join(X0,X2)))))),
% 4.87/1.07 inference(forward_demodulation,[status(thm)],[f1393,f3077])).
% 4.87/1.07 fof(f3111,plain,(
% 4.87/1.07 ![X0,X1,X2]: (meet(join(meet(X0,X1),X2),meet(X1,meet(join(meet(join(X2,X1),X0),X1),join(X0,X2))))=meet(X1,join(meet(X0,X1),X2)))),
% 4.87/1.07 inference(forward_demodulation,[status(thm)],[f87,f2837])).
% 4.87/1.07 fof(f3112,plain,(
% 4.87/1.07 ![X0,X1,X2]: (meet(join(meet(X0,X1),X2),meet(X1,join(meet(join(X2,X1),X0),X1)))=meet(X1,join(meet(X0,X1),X2)))),
% 4.87/1.07 inference(forward_demodulation,[status(thm)],[f3078,f3111])).
% 4.87/1.07 fof(f3113,plain,(
% 4.87/1.07 ![X0,X1,X2]: (meet(join(meet(X0,X1),X2),X1)=meet(X1,join(meet(X0,X1),X2)))),
% 4.87/1.07 inference(forward_demodulation,[status(thm)],[f51,f3112])).
% 4.87/1.07 fof(f3136,plain,(
% 4.87/1.07 ![X0,X1,X2]: (meet(X0,join(X1,meet(X0,X2)))=meet(join(X2,meet(X0,join(X1,meet(X0,X2)))),X0))),
% 4.87/1.07 inference(backward_demodulation,[status(thm)],[f3166,f2979])).
% 4.87/1.07 fof(f3142,plain,(
% 4.87/1.07 ![X0,X1,X2]: (join(meet(X0,X1),meet(X2,X1))=meet(X1,join(X2,meet(X1,X0))))),
% 4.87/1.07 inference(backward_demodulation,[status(thm)],[f3166,f2744])).
% 4.87/1.07 fof(f3149,plain,(
% 4.87/1.07 ![X0,X1,X2]: (join(X0,meet(join(meet(join(X0,X1),X2),X1),join(X2,X0)))=join(X0,meet(X1,join(X2,meet(X1,X0)))))),
% 4.87/1.07 inference(backward_demodulation,[status(thm)],[f3166,f2701])).
% 4.87/1.07 fof(f3165,plain,(
% 4.87/1.07 ![X0,X1,X2]: (join(meet(X0,join(X1,meet(X0,X2))),meet(X2,X1))=meet(join(meet(join(X1,X0),X2),X0),join(X2,X1)))),
% 4.87/1.07 inference(backward_demodulation,[status(thm)],[f3166,f487])).
% 4.87/1.07 fof(f3166,plain,(
% 4.87/1.07 ![X0,X1,X2]: (meet(X0,join(X1,meet(X0,X2)))=meet(X0,join(meet(X1,X0),X2)))),
% 4.87/1.07 inference(forward_demodulation,[status(thm)],[f2858,f3113])).
% 4.87/1.07 fof(f3174,plain,(
% 4.87/1.07 ![X0,X1,X2]: (join(X0,meet(X1,join(X2,X0)))=meet(meet(join(X0,X2),join(X0,X1)),join(X1,join(X2,X0))))),
% 4.87/1.07 inference(backward_demodulation,[status(thm)],[f3011,f2037])).
% 4.87/1.07 fof(f3215,plain,(
% 4.87/1.07 ![X0,X1,X2]: (join(X0,meet(X1,join(X2,X0)))=meet(join(X0,X1),meet(join(X0,X2),join(X1,join(X2,X0)))))),
% 4.87/1.07 inference(forward_demodulation,[status(thm)],[f87,f3174])).
% 4.87/1.07 fof(f3216,plain,(
% 4.87/1.07 ![X0,X1,X2]: (meet(join(X0,join(meet(join(X0,X1),X2),X1)),join(X0,X2))=join(X0,meet(X1,join(X2,meet(X1,X0)))))),
% 4.87/1.07 inference(backward_demodulation,[status(thm)],[f3220,f3149])).
% 4.87/1.07 fof(f3220,plain,(
% 4.87/1.07 ![X0,X1,X2]: (join(X0,meet(X1,join(X2,X0)))=meet(join(X0,X1),join(X0,X2)))),
% 4.87/1.07 inference(forward_demodulation,[status(thm)],[f262,f3215])).
% 4.87/1.07 fof(f3263,plain,(
% 4.87/1.07 ![X0,X1,X2]: (join(X0,join(X0,X1))=join(X0,join(join(X0,X1),meet(join(X1,X0),X2))))),
% 4.87/1.07 inference(paramodulation,[status(thm)],[f2154,f103])).
% 4.87/1.07 fof(f3350,plain,(
% 4.87/1.07 ![X0,X1,X2]: (join(X0,X1)=join(X1,join(join(X1,X0),meet(join(X0,X1),X2))))),
% 4.87/1.07 inference(forward_demodulation,[status(thm)],[f2154,f3263])).
% 4.87/1.07 fof(f3351,plain,(
% 4.87/1.07 ![X0,X1,X2]: (join(X0,X1)=join(X1,join(X0,join(X1,meet(join(X0,X1),X2)))))),
% 4.87/1.07 inference(forward_demodulation,[status(thm)],[f111,f3350])).
% 4.87/1.07 fof(f3352,plain,(
% 4.87/1.07 ![X0,X1,X2]: (meet(join(X0,X1),join(X0,X2))=join(X0,meet(X1,join(X2,meet(X1,X0)))))),
% 4.87/1.07 inference(backward_demodulation,[status(thm)],[f3353,f3216])).
% 4.87/1.07 fof(f3353,plain,(
% 4.87/1.07 ![X0,X1,X2]: (join(X0,X1)=join(X0,join(meet(join(X0,X1),X2),X1)))),
% 4.87/1.07 inference(forward_demodulation,[status(thm)],[f2308,f3351])).
% 4.87/1.07 fof(f3423,plain,(
% 4.87/1.07 ![X0,X1,X2]: (meet(X0,join(X1,meet(X0,X2)))=meet(meet(join(X2,X0),join(X2,X1)),X0))),
% 4.87/1.07 inference(backward_demodulation,[status(thm)],[f3352,f3136])).
% 4.87/1.07 fof(f3427,plain,(
% 4.87/1.07 ![X0,X1,X2]: (meet(X0,join(X1,meet(X0,X2)))=meet(join(X2,X1),meet(join(X2,X0),X0)))),
% 4.87/1.07 inference(forward_demodulation,[status(thm)],[f87,f3423])).
% 4.87/1.07 fof(f3442,plain,(
% 4.87/1.07 ![X0,X1,X2]: (join(meet(join(X0,X1),X2),meet(X0,X1))=meet(join(meet(join(X1,X2),X0),X2),join(X0,X1)))),
% 4.87/1.07 inference(backward_demodulation,[status(thm)],[f3481,f3165])).
% 4.87/1.07 fof(f3463,plain,(
% 4.87/1.07 ![X0,X1,X2]: (join(meet(X0,X1),meet(X2,X1))=meet(join(X0,X2),X1))),
% 4.87/1.07 inference(backward_demodulation,[status(thm)],[f3481,f3142])).
% 4.87/1.07 fof(f3481,plain,(
% 4.87/1.07 ![X0,X1,X2]: (meet(X0,join(X1,meet(X0,X2)))=meet(join(X2,X1),X0))),
% 4.87/1.07 inference(forward_demodulation,[status(thm)],[f1718,f3427])).
% 4.87/1.07 fof(f3538,plain,(
% 4.87/1.09 ![X0,X1,X2]: (join(X0,meet(X1,X2))=join(X0,join(meet(X1,X2),join(meet(join(X1,X0),X2),meet(X1,X0)))))),
% 4.87/1.09 inference(backward_demodulation,[status(thm)],[f3442,f3067])).
% 4.87/1.09 fof(f3611,plain,(
% 4.87/1.09 ![X0,X1,X2]: (join(X0,meet(X1,X2))=join(X0,join(meet(X1,X2),meet(join(X1,X0),X2))))),
% 4.87/1.09 inference(forward_demodulation,[status(thm)],[f1220,f3538])).
% 4.87/1.09 fof(f3612,plain,(
% 4.87/1.09 ![X0,X1,X2]: (join(X0,meet(X1,X2))=join(X0,meet(join(X1,join(X1,X0)),X2)))),
% 4.87/1.09 inference(forward_demodulation,[status(thm)],[f3463,f3611])).
% 4.87/1.09 fof(f3614,plain,(
% 4.87/1.09 ![X0,X1,X2]: (join(X0,meet(X1,X2))=meet(join(X2,X0),join(X0,X1)))),
% 4.87/1.09 inference(backward_demodulation,[status(thm)],[f3615,f2959])).
% 4.87/1.09 fof(f3615,plain,(
% 4.87/1.09 ![X0,X1,X2]: (join(X0,meet(X1,X2))=join(X0,meet(join(X0,X1),X2)))),
% 4.87/1.09 inference(forward_demodulation,[status(thm)],[f2154,f3612])).
% 4.87/1.09 fof(f3674,plain,(
% 4.87/1.09 ~join(a,meet(b,c))=join(a,meet(b,c))),
% 4.87/1.09 inference(backward_demodulation,[status(thm)],[f3614,f617])).
% 4.87/1.09 fof(f3729,plain,(
% 4.87/1.09 $false),
% 4.87/1.09 inference(trivial_equality_resolution,[status(thm)],[f3674])).
% 4.87/1.09 % SZS output end CNFRefutation for theBenchmark.p
% 12.27/2.30 % Elapsed time: 1.709417 seconds
% 12.27/2.30 % CPU time: 2.364123 seconds
% 12.27/2.30 % Total memory used: 31.579 MB
% 12.27/2.30 % Net memory used: 30.760 MB
%------------------------------------------------------------------------------