%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : SWW438-1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n011.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 03:09:08 PM UTC 2026
% Result : Unsatisfiable 0.32s 20.64s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW438-1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.34 % Computer : n011.cluster.edu
% 0.08/0.34 % Model : x86_64 x86_64
% 0.08/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.34 % Memory : 8046.5625MB
% 0.08/0.34 % OS : Linux 6.8.0-71-generic
% 0.08/20.42 % CPULimit : 300
% 0.08/20.42 % WCLimit : 300
% 0.08/20.42 % DateTime : Mon Sep 21 09:53:22 UTC 2026
% 0.08/20.42 % CPUTime :
% 0.08/20.43 % Drodi V4.1.1
% 0.32/20.64 % Refutation found
% 0.32/20.64 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 0.32/20.64 % SZS output start CNFRefutation for theBenchmark
% 0.32/20.64 fof(f1,axiom,(
% 0.32/20.64 (![S,T,Sigma]: (sep(S,sep(T,Sigma)) = sep(T,sep(S,Sigma)) ))),
% 0.32/20.64 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.32/20.64 fof(f2,axiom,(
% 0.32/20.64 (![X,Sigma]: (sep(lseg(X,X),Sigma) = Sigma ))),
% 0.32/20.64 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.32/20.64 fof(f7,axiom,(
% 0.32/20.64 (![X,Y,Z,Sigma]: (( ~ heap(sep(lseg(X,Y),sep(lseg(X,Z),Sigma)))| X = Y| X = Z ) ))),
% 0.32/20.64 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.32/20.64 fof(f14,hypothesis,(
% 0.32/20.64 x3 != x10 ),
% 0.32/20.64 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.32/20.64 fof(f15,hypothesis,(
% 0.32/20.64 x3 != x14 ),
% 0.32/20.64 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.32/20.64 fof(f21,hypothesis,(
% 0.32/20.64 x14 != x16 ),
% 0.32/20.64 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.32/20.64 fof(f27,hypothesis,(
% 0.32/20.64 heap(sep(lseg(x14,x12),sep(lseg(x2,x13),sep(lseg(x13,x6),sep(lseg(x13,x8),sep(lseg(x10,x2),sep(lseg(x10,x3),sep(lseg(x7,x2),sep(lseg(x7,x16),sep(lseg(x3,x14),sep(lseg(x11,x4),sep(lseg(x6,x14),sep(lseg(x6,x16),emp))))))))))))) ),
% 0.32/20.65 file('/export/starexec/sandbox2/benchmark/theBenchmark.p')).
% 0.32/20.65 fof(f29,plain,(
% 0.32/20.65 ![X0,X1,X2]: (sep(X0,sep(X1,X2))=sep(X1,sep(X0,X2)))),
% 0.32/20.65 inference(cnf_transformation,[status(thm)],[f1])).
% 0.32/20.65 fof(f30,plain,(
% 0.32/20.65 ![X0,X1]: (sep(lseg(X0,X0),X1)=X1)),
% 0.32/20.65 inference(cnf_transformation,[status(thm)],[f2])).
% 0.32/20.65 fof(f37,plain,(
% 0.32/20.65 ![X,Z]: ((![Y]: ((![Sigma]: ~heap(sep(lseg(X,Y),sep(lseg(X,Z),Sigma))))|X=Y))|X=Z)),
% 0.32/20.65 inference(miniscoping,[status(thm)],[f7])).
% 0.32/20.65 fof(f38,plain,(
% 0.32/20.65 ![X0,X1,X2,X3]: (~heap(sep(lseg(X0,X1),sep(lseg(X0,X2),X3)))|X0=X1|X0=X2)),
% 0.32/20.65 inference(cnf_transformation,[status(thm)],[f37])).
% 0.32/20.65 fof(f49,plain,(
% 0.32/20.65 ~x3=x10),
% 0.32/20.65 inference(cnf_transformation,[status(thm)],[f14])).
% 0.32/20.65 fof(f50,plain,(
% 0.32/20.65 ~x3=x14),
% 0.32/20.65 inference(cnf_transformation,[status(thm)],[f15])).
% 0.32/20.65 fof(f56,plain,(
% 0.32/20.65 ~x14=x16),
% 0.32/20.65 inference(cnf_transformation,[status(thm)],[f21])).
% 0.32/20.65 fof(f62,plain,(
% 0.32/20.65 heap(sep(lseg(x14,x12),sep(lseg(x2,x13),sep(lseg(x13,x6),sep(lseg(x13,x8),sep(lseg(x10,x2),sep(lseg(x10,x3),sep(lseg(x7,x2),sep(lseg(x7,x16),sep(lseg(x3,x14),sep(lseg(x11,x4),sep(lseg(x6,x14),sep(lseg(x6,x16),emp)))))))))))))),
% 0.32/20.65 inference(cnf_transformation,[status(thm)],[f27])).
% 0.32/20.65 fof(f135,plain,(
% 0.32/20.65 ![X0,X1,X2,X3,X4]: (~heap(sep(lseg(X0,X1),sep(X2,sep(lseg(X0,X3),X4))))|X0=X1|X0=X3)),
% 0.32/20.65 inference(paramodulation,[status(thm)],[f29,f38])).
% 0.32/20.65 fof(f138,plain,(
% 0.32/20.65 ![X0,X1,X2,X3,X4]: (~heap(sep(X0,sep(lseg(X1,X2),sep(lseg(X1,X3),X4))))|X1=X2|X1=X3)),
% 0.32/20.65 inference(paramodulation,[status(thm)],[f29,f135])).
% 0.32/20.65 fof(f153,plain,(
% 0.32/20.65 ![X0,X1,X2,X3,X4,X5]: (~heap(sep(X0,sep(lseg(X1,X2),sep(X3,sep(lseg(X1,X4),X5)))))|X1=X2|X1=X4)),
% 0.32/20.65 inference(paramodulation,[status(thm)],[f29,f138])).
% 0.32/20.65 fof(f171,plain,(
% 0.32/20.65 ![X0,X1,X2,X3,X4,X5]: (~heap(sep(X0,sep(X1,sep(lseg(X2,X3),sep(lseg(X2,X4),X5)))))|X2=X3|X2=X4)),
% 0.32/20.65 inference(paramodulation,[status(thm)],[f29,f153])).
% 0.32/20.65 fof(f177,plain,(
% 0.32/20.65 ![X0,X1,X2,X3,X4,X5,X6]: (~heap(sep(X0,sep(lseg(X1,X2),sep(X3,sep(X4,sep(lseg(X1,X5),X6))))))|X1=X2|X1=X5)),
% 0.32/20.65 inference(paramodulation,[status(thm)],[f29,f153])).
% 0.32/20.65 fof(f190,plain,(
% 0.32/20.65 ![X0,X1,X2,X3,X4,X5,X6]: (~heap(sep(X0,sep(X1,sep(lseg(X2,X3),sep(X4,sep(lseg(X2,X5),X6))))))|X2=X3|X2=X5)),
% 0.32/20.65 inference(paramodulation,[status(thm)],[f29,f171])).
% 0.32/20.65 fof(f249,plain,(
% 0.32/20.65 ![X0,X1,X2,X3,X4,X5,X6,X7]: (~heap(sep(X0,sep(lseg(X1,X2),sep(X3,sep(X4,sep(X5,sep(lseg(X1,X6),X7)))))))|X1=X2|X1=X6)),
% 0.32/20.65 inference(paramodulation,[status(thm)],[f29,f177])).
% 0.32/20.65 fof(f258,plain,(
% 0.32/20.65 ![X0,X1,X2,X3,X4,X5,X6]: (~heap(sep(X0,sep(X1,sep(X2,sep(lseg(X3,X4),sep(lseg(X3,X5),X6))))))|X3=X4|X3=X5)),
% 0.32/20.65 inference(paramodulation,[status(thm)],[f29,f190])).
% 0.32/20.65 fof(f279,plain,(
% 0.32/20.65 ![X0,X1,X2,X3,X4,X5,X6,X7]: (~heap(sep(X0,sep(X1,sep(X2,sep(lseg(X3,X4),sep(X5,sep(lseg(X3,X6),X7)))))))|X3=X4|X3=X6)),
% 0.32/20.65 inference(paramodulation,[status(thm)],[f29,f258])).
% 0.32/20.65 fof(f315,plain,(
% 0.32/20.65 ![X0,X1,X2,X3,X4,X5,X6,X7,X8]: (~heap(sep(X0,sep(lseg(X1,X2),sep(X3,sep(X4,sep(X5,sep(X6,sep(lseg(X1,X7),X8))))))))|X1=X2|X1=X7)),
% 0.32/20.65 inference(paramodulation,[status(thm)],[f29,f249])).
% 0.32/20.65 fof(f345,plain,(
% 0.32/20.65 ![X0,X1,X2,X3,X4,X5,X6,X7]: (~heap(sep(X0,sep(X1,sep(X2,sep(X3,sep(lseg(X4,X5),sep(lseg(X4,X6),X7)))))))|X4=X5|X4=X6)),
% 0.32/20.65 inference(paramodulation,[status(thm)],[f29,f279])).
% 0.32/20.65 fof(f353,plain,(
% 0.32/20.65 x10=x2|x10=x3),
% 0.32/20.65 inference(resolution,[status(thm)],[f345,f62])).
% 0.32/20.65 fof(f372,plain,(
% 0.32/20.65 x10=x2),
% 0.32/20.65 inference(forward_subsumption_resolution,[status(thm)],[f353,f49])).
% 0.32/20.65 fof(f419,plain,(
% 0.32/20.65 ![X0,X1,X2,X3,X4,X5,X6,X7,X8,X9]: (~heap(sep(X0,sep(lseg(X1,X2),sep(X3,sep(X4,sep(X5,sep(X6,sep(X7,sep(lseg(X1,X8),X9)))))))))|X1=X2|X1=X8)),
% 0.32/20.65 inference(paramodulation,[status(thm)],[f29,f315])).
% 0.32/20.65 fof(f829,plain,(
% 0.32/20.65 heap(sep(lseg(x14,x12),sep(lseg(x2,x13),sep(lseg(x13,x6),sep(lseg(x13,x8),sep(lseg(x10,x2),sep(lseg(x2,x3),sep(lseg(x7,x2),sep(lseg(x7,x16),sep(lseg(x3,x14),sep(lseg(x11,x4),sep(lseg(x6,x14),sep(lseg(x6,x16),emp)))))))))))))),
% 0.32/20.65 inference(backward_demodulation,[status(thm)],[f372,f62])).
% 0.32/20.65 fof(f831,plain,(
% 0.32/20.65 ~x3=x2),
% 0.32/20.65 inference(backward_demodulation,[status(thm)],[f372,f49])).
% 0.32/20.65 fof(f832,plain,(
% 0.32/20.65 heap(sep(lseg(x14,x12),sep(lseg(x2,x13),sep(lseg(x13,x6),sep(lseg(x13,x8),sep(lseg(x2,x2),sep(lseg(x2,x3),sep(lseg(x7,x2),sep(lseg(x7,x16),sep(lseg(x3,x14),sep(lseg(x11,x4),sep(lseg(x6,x14),sep(lseg(x6,x16),emp)))))))))))))),
% 0.32/20.65 inference(forward_demodulation,[status(thm)],[f372,f829])).
% 0.32/20.65 fof(f833,plain,(
% 0.32/20.65 heap(sep(lseg(x14,x12),sep(lseg(x2,x13),sep(lseg(x13,x6),sep(lseg(x13,x8),sep(lseg(x2,x3),sep(lseg(x7,x2),sep(lseg(x7,x16),sep(lseg(x3,x14),sep(lseg(x11,x4),sep(lseg(x6,x14),sep(lseg(x6,x16),emp))))))))))))),
% 0.32/20.65 inference(forward_demodulation,[status(thm)],[f30,f832])).
% 0.32/20.65 fof(f834,plain,(
% 0.32/20.65 x2=x13|x2=x3),
% 0.32/20.65 inference(resolution,[status(thm)],[f833,f177])).
% 0.32/20.65 fof(f837,plain,(
% 0.32/20.65 heap(sep(lseg(x14,x12),sep(lseg(x2,x13),sep(lseg(x13,x6),sep(lseg(x2,x3),sep(lseg(x13,x8),sep(lseg(x7,x2),sep(lseg(x7,x16),sep(lseg(x3,x14),sep(lseg(x11,x4),sep(lseg(x6,x14),sep(lseg(x6,x16),emp))))))))))))),
% 0.32/20.65 inference(paramodulation,[status(thm)],[f29,f833])).
% 0.32/20.65 fof(f842,plain,(
% 0.32/20.65 x2=x13),
% 0.32/20.65 inference(forward_subsumption_resolution,[status(thm)],[f834,f831])).
% 0.32/20.65 fof(f856,plain,(
% 0.32/20.65 heap(sep(lseg(x14,x12),sep(lseg(x2,x13),sep(lseg(x13,x6),sep(lseg(x2,x3),sep(lseg(x2,x8),sep(lseg(x7,x2),sep(lseg(x7,x16),sep(lseg(x3,x14),sep(lseg(x11,x4),sep(lseg(x6,x14),sep(lseg(x6,x16),emp))))))))))))),
% 0.32/20.65 inference(backward_demodulation,[status(thm)],[f842,f837])).
% 0.32/20.65 fof(f857,plain,(
% 0.32/20.65 heap(sep(lseg(x14,x12),sep(lseg(x2,x13),sep(lseg(x13,x6),sep(lseg(x2,x8),sep(lseg(x2,x3),sep(lseg(x7,x2),sep(lseg(x7,x16),sep(lseg(x3,x14),sep(lseg(x11,x4),sep(lseg(x6,x14),sep(lseg(x6,x16),emp))))))))))))),
% 0.32/20.65 inference(backward_demodulation,[status(thm)],[f842,f833])).
% 0.32/20.65 fof(f860,plain,(
% 0.32/20.65 heap(sep(lseg(x14,x12),sep(lseg(x2,x2),sep(lseg(x13,x6),sep(lseg(x2,x3),sep(lseg(x2,x8),sep(lseg(x7,x2),sep(lseg(x7,x16),sep(lseg(x3,x14),sep(lseg(x11,x4),sep(lseg(x6,x14),sep(lseg(x6,x16),emp))))))))))))),
% 0.32/20.65 inference(forward_demodulation,[status(thm)],[f842,f856])).
% 0.32/20.65 fof(f861,plain,(
% 0.32/20.65 heap(sep(lseg(x14,x12),sep(lseg(x13,x6),sep(lseg(x2,x3),sep(lseg(x2,x8),sep(lseg(x7,x2),sep(lseg(x7,x16),sep(lseg(x3,x14),sep(lseg(x11,x4),sep(lseg(x6,x14),sep(lseg(x6,x16),emp)))))))))))),
% 0.32/20.65 inference(forward_demodulation,[status(thm)],[f30,f860])).
% 0.32/20.65 fof(f862,plain,(
% 0.32/20.65 heap(sep(lseg(x14,x12),sep(lseg(x2,x6),sep(lseg(x2,x3),sep(lseg(x2,x8),sep(lseg(x7,x2),sep(lseg(x7,x16),sep(lseg(x3,x14),sep(lseg(x11,x4),sep(lseg(x6,x14),sep(lseg(x6,x16),emp)))))))))))),
% 0.32/20.65 inference(forward_demodulation,[status(thm)],[f842,f861])).
% 0.32/20.65 fof(f863,plain,(
% 0.32/20.65 heap(sep(lseg(x14,x12),sep(lseg(x2,x2),sep(lseg(x13,x6),sep(lseg(x2,x8),sep(lseg(x2,x3),sep(lseg(x7,x2),sep(lseg(x7,x16),sep(lseg(x3,x14),sep(lseg(x11,x4),sep(lseg(x6,x14),sep(lseg(x6,x16),emp))))))))))))),
% 0.32/20.65 inference(forward_demodulation,[status(thm)],[f842,f857])).
% 0.32/20.65 fof(f864,plain,(
% 0.32/20.65 heap(sep(lseg(x14,x12),sep(lseg(x13,x6),sep(lseg(x2,x8),sep(lseg(x2,x3),sep(lseg(x7,x2),sep(lseg(x7,x16),sep(lseg(x3,x14),sep(lseg(x11,x4),sep(lseg(x6,x14),sep(lseg(x6,x16),emp)))))))))))),
% 0.32/20.65 inference(forward_demodulation,[status(thm)],[f30,f863])).
% 0.32/20.65 fof(f865,plain,(
% 0.32/20.65 heap(sep(lseg(x14,x12),sep(lseg(x2,x6),sep(lseg(x2,x8),sep(lseg(x2,x3),sep(lseg(x7,x2),sep(lseg(x7,x16),sep(lseg(x3,x14),sep(lseg(x11,x4),sep(lseg(x6,x14),sep(lseg(x6,x16),emp)))))))))))),
% 0.32/20.65 inference(forward_demodulation,[status(thm)],[f842,f864])).
% 0.32/20.65 fof(f867,plain,(
% 0.32/20.65 x2=x6|x2=x3),
% 0.32/20.65 inference(resolution,[status(thm)],[f862,f138])).
% 0.32/20.65 fof(f869,plain,(
% 0.32/20.65 x2=x3|x2=x8),
% 0.32/20.65 inference(resolution,[status(thm)],[f862,f171])).
% 0.32/20.65 fof(f873,plain,(
% 0.32/20.65 x2=x6),
% 0.32/20.65 inference(forward_subsumption_resolution,[status(thm)],[f867,f831])).
% 0.32/20.65 fof(f874,plain,(
% 0.32/20.65 x2=x8),
% 0.32/20.65 inference(forward_subsumption_resolution,[status(thm)],[f869,f831])).
% 0.32/20.65 fof(f878,plain,(
% 0.32/20.65 ~x3=x6),
% 0.32/20.65 inference(backward_demodulation,[status(thm)],[f873,f831])).
% 0.32/20.65 fof(f887,plain,(
% 0.32/20.65 x6=x8),
% 0.32/20.65 inference(forward_demodulation,[status(thm)],[f873,f874])).
% 0.32/20.65 fof(f888,plain,(
% 0.32/20.65 heap(sep(lseg(x14,x12),sep(lseg(x6,x6),sep(lseg(x2,x8),sep(lseg(x2,x3),sep(lseg(x7,x2),sep(lseg(x7,x16),sep(lseg(x3,x14),sep(lseg(x11,x4),sep(lseg(x6,x14),sep(lseg(x6,x16),emp)))))))))))),
% 0.32/20.65 inference(forward_demodulation,[status(thm)],[f873,f865])).
% 0.32/20.65 fof(f889,plain,(
% 0.32/20.65 heap(sep(lseg(x14,x12),sep(lseg(x2,x8),sep(lseg(x2,x3),sep(lseg(x7,x2),sep(lseg(x7,x16),sep(lseg(x3,x14),sep(lseg(x11,x4),sep(lseg(x6,x14),sep(lseg(x6,x16),emp))))))))))),
% 0.32/20.65 inference(forward_demodulation,[status(thm)],[f30,f888])).
% 0.32/20.65 fof(f890,plain,(
% 0.32/20.65 heap(sep(lseg(x14,x12),sep(lseg(x6,x8),sep(lseg(x2,x3),sep(lseg(x7,x2),sep(lseg(x7,x16),sep(lseg(x3,x14),sep(lseg(x11,x4),sep(lseg(x6,x14),sep(lseg(x6,x16),emp))))))))))),
% 0.32/20.65 inference(forward_demodulation,[status(thm)],[f873,f889])).
% 0.32/20.65 fof(f891,plain,(
% 0.32/20.65 heap(sep(lseg(x14,x12),sep(lseg(x6,x6),sep(lseg(x2,x3),sep(lseg(x7,x2),sep(lseg(x7,x16),sep(lseg(x3,x14),sep(lseg(x11,x4),sep(lseg(x6,x14),sep(lseg(x6,x16),emp))))))))))),
% 0.32/20.65 inference(forward_demodulation,[status(thm)],[f887,f890])).
% 0.32/20.65 fof(f892,plain,(
% 0.32/20.65 heap(sep(lseg(x14,x12),sep(lseg(x2,x3),sep(lseg(x7,x2),sep(lseg(x7,x16),sep(lseg(x3,x14),sep(lseg(x11,x4),sep(lseg(x6,x14),sep(lseg(x6,x16),emp)))))))))),
% 0.32/20.65 inference(forward_demodulation,[status(thm)],[f30,f891])).
% 0.32/20.65 fof(f893,plain,(
% 0.32/20.65 heap(sep(lseg(x14,x12),sep(lseg(x6,x3),sep(lseg(x7,x2),sep(lseg(x7,x16),sep(lseg(x3,x14),sep(lseg(x11,x4),sep(lseg(x6,x14),sep(lseg(x6,x16),emp)))))))))),
% 0.32/20.65 inference(forward_demodulation,[status(thm)],[f873,f892])).
% 0.32/20.65 fof(f894,plain,(
% 0.32/20.65 heap(sep(lseg(x14,x12),sep(lseg(x6,x3),sep(lseg(x7,x6),sep(lseg(x7,x16),sep(lseg(x3,x14),sep(lseg(x11,x4),sep(lseg(x6,x14),sep(lseg(x6,x16),emp)))))))))),
% 0.32/20.65 inference(forward_demodulation,[status(thm)],[f873,f893])).
% 0.32/20.65 fof(f895,plain,(
% 0.32/20.65 x6=x3|x6=x14),
% 0.32/20.65 inference(resolution,[status(thm)],[f894,f315])).
% 0.32/20.65 fof(f896,plain,(
% 0.32/20.65 x6=x3|x6=x16),
% 0.32/20.65 inference(resolution,[status(thm)],[f894,f419])).
% 0.32/20.65 fof(f1520,plain,(
% 0.32/20.65 x6=x14),
% 0.32/20.65 inference(forward_subsumption_resolution,[status(thm)],[f895,f878])).
% 0.32/20.65 fof(f1525,plain,(
% 0.32/20.65 x14=x3|x6=x16),
% 0.32/20.65 inference(forward_demodulation,[status(thm)],[f1520,f896])).
% 0.32/20.65 fof(f1526,plain,(
% 0.32/20.65 x14=x3|x14=x16),
% 0.32/20.65 inference(forward_demodulation,[status(thm)],[f1520,f1525])).
% 0.32/20.65 fof(f1530,plain,(
% 0.32/20.65 ~x14=x14),
% 0.32/20.65 inference(backward_demodulation,[status(thm)],[f1531,f56])).
% 0.32/20.65 fof(f1531,plain,(
% 0.32/20.65 x14=x16),
% 0.32/20.65 inference(forward_subsumption_resolution,[status(thm)],[f1526,f50])).
% 0.32/20.65 fof(f1532,plain,(
% 0.32/20.65 $false),
% 0.32/20.65 inference(trivial_equality_resolution,[status(thm)],[f1530])).
% 0.32/20.65 % SZS output end CNFRefutation for theBenchmark.p
% 0.32/20.67 % Elapsed time: 0.233709 seconds
% 0.32/20.67 % CPU time: 1.619886 seconds
% 0.32/20.67 % Total memory used: 124.690 MB
% 0.32/20.67 % Net memory used: 123.156 MB
%------------------------------------------------------------------------------